From b1febe05a4b1dc8104363bed865df1f5290c458a Mon Sep 17 00:00:00 2001
From: dagurtomas <dagurtomas@gmail.com>
Date: Mon, 18 Nov 2024 12:06:00 +0000
Subject: [PATCH 1/3] feat(CategoryTheory): split up a product into a binary
 product

---
 .../CategoryTheory/Limits/Shapes/PiProd.lean  | 69 +++++++++++++++++++
 1 file changed, 69 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean b/Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
new file mode 100644
index 0000000000000..73a34990f647b
--- /dev/null
+++ b/Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2024 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
+import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
+import Mathlib.CategoryTheory.Limits.Shapes.Products
+/-!
+
+# A product as a binary product
+
+We write a product indexed by `I` as a binary product of the products indexed by a subset of `I`
+and its complement.
+
+-/
+
+namespace CategoryTheory.Limits
+
+variable {C I : Type*} [Category C] {X Y : I → C}
+  (f : (i : I) → X i ⟶ Y i) (P : I → Prop) [∀ i, Decidable (P i)]
+  [HasProduct X] [HasProduct Y]
+  [HasProduct (fun (i : {x : I // P x}) ↦ X i.val)]
+  [HasProduct (fun (i : {x : I // ¬ (P x)}) ↦ X i.val)]
+  [HasProduct (fun (i : {x : I // P x}) ↦ Y i.val)]
+  [HasProduct (fun (i : {x : I // ¬ (P x)}) ↦ Y i.val)]
+
+variable (X) in
+/--
+The projection maps of a product to the products indexed by a subset and its complement, as a
+binary fan.
+-/
+noncomputable def Pi.binaryFanOfProp : BinaryFan (∏ᶜ (fun (i : {x : I // P x}) ↦ X i.val))
+    (∏ᶜ (fun (i : {x : I // ¬ (P x)}) ↦ X i.val)) :=
+  BinaryFan.mk (P := ∏ᶜ X) (Pi.map' Subtype.val fun _ ↦ 𝟙 _)
+    (Pi.map' Subtype.val fun _ ↦ 𝟙 _)
+
+variable (X) in
+/--
+A product indexed by `I` is a binary product of the products indexed by a subset of `I` and its
+complement.
+-/
+noncomputable def Pi.binaryFanOfPropIsLimit : IsLimit (Pi.binaryFanOfProp X P) :=
+  BinaryFan.isLimitMk
+    (fun s ↦ Pi.lift fun b ↦ if h : (P b) then
+      s.π.app ⟨WalkingPair.left⟩ ≫ Pi.π (fun (i : {x : I // P x}) ↦ X i.val) ⟨b, h⟩ else
+      s.π.app ⟨WalkingPair.right⟩ ≫ Pi.π (fun (i : {x : I // ¬ (P x)}) ↦ X i.val) ⟨b, h⟩)
+    (by aesop) (by aesop)
+    (fun _ _ h₁ h₂ ↦ Pi.hom_ext _ _ fun b ↦ by
+      by_cases h : (P b)
+      · simp [← h₁, dif_pos h]
+      · simp [← h₂, dif_neg h])
+
+lemma hasBinaryProduct_of_products : HasBinaryProduct (∏ᶜ (fun (i : {x : I // P x}) ↦ X i.val))
+    (∏ᶜ (fun (i : {x : I // ¬ (P x)}) ↦ X i.val)) :=
+  ⟨Pi.binaryFanOfProp X P, Pi.binaryFanOfPropIsLimit X P⟩
+
+attribute [local instance] hasBinaryProduct_of_products
+
+lemma Pi.map_eq_prod_map : Pi.map f =
+    ((Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd _ _)).hom ≫
+      prod.map (Pi.map (fun (i : {x : I // P x}) ↦ f i.val))
+      (Pi.map (fun (i : {x : I // ¬ (P x)}) ↦ f i.val)) ≫
+        ((Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd _ _)).inv := by
+  rw [← Category.assoc, Iso.eq_comp_inv]
+  dsimp only [IsLimit.conePointUniqueUpToIso, binaryFanOfProp, prodIsProd]
+  apply prod.hom_ext
+  all_goals aesop_cat
+
+end CategoryTheory.Limits

From b612588e2a216fa0edf86599d1ab86657e327368 Mon Sep 17 00:00:00 2001
From: dagurtomas <dagurtomas@gmail.com>
Date: Mon, 18 Nov 2024 12:06:17 +0000
Subject: [PATCH 2/3] mk_all

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 9dbb62dd6373b..2f33d9b1b9280 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1830,6 +1830,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Kernels
 import Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
 import Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
 import Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
+import Mathlib.CategoryTheory.Limits.Shapes.PiProd
 import Mathlib.CategoryTheory.Limits.Shapes.Products
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq

From 6326a1a71840a70a5e6374e01f13f8e94325d679 Mon Sep 17 00:00:00 2001
From: dagurtomas <dagurtomas@gmail.com>
Date: Mon, 18 Nov 2024 13:39:56 +0000
Subject: [PATCH 3/3] remove unnecessary parentheses

---
 Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean b/Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
index 73a34990f647b..6027232e5928d 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
@@ -20,9 +20,9 @@ variable {C I : Type*} [Category C] {X Y : I → C}
   (f : (i : I) → X i ⟶ Y i) (P : I → Prop) [∀ i, Decidable (P i)]
   [HasProduct X] [HasProduct Y]
   [HasProduct (fun (i : {x : I // P x}) ↦ X i.val)]
-  [HasProduct (fun (i : {x : I // ¬ (P x)}) ↦ X i.val)]
+  [HasProduct (fun (i : {x : I // ¬ P x}) ↦ X i.val)]
   [HasProduct (fun (i : {x : I // P x}) ↦ Y i.val)]
-  [HasProduct (fun (i : {x : I // ¬ (P x)}) ↦ Y i.val)]
+  [HasProduct (fun (i : {x : I // ¬ P x}) ↦ Y i.val)]
 
 variable (X) in
 /--
@@ -30,7 +30,7 @@ The projection maps of a product to the products indexed by a subset and its com
 binary fan.
 -/
 noncomputable def Pi.binaryFanOfProp : BinaryFan (∏ᶜ (fun (i : {x : I // P x}) ↦ X i.val))
-    (∏ᶜ (fun (i : {x : I // ¬ (P x)}) ↦ X i.val)) :=
+    (∏ᶜ (fun (i : {x : I // ¬ P x}) ↦ X i.val)) :=
   BinaryFan.mk (P := ∏ᶜ X) (Pi.map' Subtype.val fun _ ↦ 𝟙 _)
     (Pi.map' Subtype.val fun _ ↦ 𝟙 _)
 
@@ -41,17 +41,17 @@ complement.
 -/
 noncomputable def Pi.binaryFanOfPropIsLimit : IsLimit (Pi.binaryFanOfProp X P) :=
   BinaryFan.isLimitMk
-    (fun s ↦ Pi.lift fun b ↦ if h : (P b) then
+    (fun s ↦ Pi.lift fun b ↦ if h : P b then
       s.π.app ⟨WalkingPair.left⟩ ≫ Pi.π (fun (i : {x : I // P x}) ↦ X i.val) ⟨b, h⟩ else
-      s.π.app ⟨WalkingPair.right⟩ ≫ Pi.π (fun (i : {x : I // ¬ (P x)}) ↦ X i.val) ⟨b, h⟩)
+      s.π.app ⟨WalkingPair.right⟩ ≫ Pi.π (fun (i : {x : I // ¬ P x}) ↦ X i.val) ⟨b, h⟩)
     (by aesop) (by aesop)
     (fun _ _ h₁ h₂ ↦ Pi.hom_ext _ _ fun b ↦ by
-      by_cases h : (P b)
+      by_cases h : P b
       · simp [← h₁, dif_pos h]
       · simp [← h₂, dif_neg h])
 
 lemma hasBinaryProduct_of_products : HasBinaryProduct (∏ᶜ (fun (i : {x : I // P x}) ↦ X i.val))
-    (∏ᶜ (fun (i : {x : I // ¬ (P x)}) ↦ X i.val)) :=
+    (∏ᶜ (fun (i : {x : I // ¬ P x}) ↦ X i.val)) :=
   ⟨Pi.binaryFanOfProp X P, Pi.binaryFanOfPropIsLimit X P⟩
 
 attribute [local instance] hasBinaryProduct_of_products
@@ -59,7 +59,7 @@ attribute [local instance] hasBinaryProduct_of_products
 lemma Pi.map_eq_prod_map : Pi.map f =
     ((Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd _ _)).hom ≫
       prod.map (Pi.map (fun (i : {x : I // P x}) ↦ f i.val))
-      (Pi.map (fun (i : {x : I // ¬ (P x)}) ↦ f i.val)) ≫
+      (Pi.map (fun (i : {x : I // ¬ P x}) ↦ f i.val)) ≫
         ((Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd _ _)).inv := by
   rw [← Category.assoc, Iso.eq_comp_inv]
   dsimp only [IsLimit.conePointUniqueUpToIso, binaryFanOfProp, prodIsProd]