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.

noncomputable def CategoryTheory.Limits.Pi.binaryFanOfProp {C : Type u_1} {I : Type u_2} [Category.{u_3, u_1} C] (X : I → C) (P : I → Prop) [HasProduct X] [HasProduct fun (i : { x : I // P x }) => X ↑i] [HasProduct fun (i : { x : I // ¬P x }) => X ↑i] : BinaryFan (∏ᶜ fun (i : { x : I // P x }) => X ↑i) (∏ᶜ fun (i : { x : I // ¬P x }) => X ↑i)

The projection maps of a product to the products indexed by a subset and its complement, as a binary fan.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit {C : Type u_1} {I : Type u_2} [Category.{u_3, u_1} C] (X : I → C) (P : I → Prop) [HasProduct X] [HasProduct fun (i : { x : I // P x }) => X ↑i] [HasProduct fun (i : { x : I // ¬P x }) => X ↑i] [(i : I) → Decidable (P i)] : IsLimit (binaryFanOfProp X P)

A product indexed by I is a binary product of the products indexed by a subset of I and its complement.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.hasBinaryProduct_of_products {C : Type u_1} {I : Type u_2} [Category.{u_3, u_1} C] {X : I → C} (P : I → Prop) [HasProduct X] [HasProduct fun (i : { x : I // P x }) => X ↑i] [HasProduct fun (i : { x : I // ¬P x }) => X ↑i] : HasBinaryProduct (∏ᶜ fun (i : { x : I // P x }) => X ↑i) (∏ᶜ fun (i : { x : I // ¬P x }) => X ↑i)

theorem CategoryTheory.Limits.Pi.map_eq_prod_map {C : Type u_1} {I : Type u_2} [Category.{u_3, u_1} C] {X Y : I → C} (f : (i : I) → X i ⟶ Y i) (P : I → Prop) [HasProduct X] [HasProduct Y] [HasProduct fun (i : { x : I // P x }) => X ↑i] [HasProduct fun (i : { x : I // ¬P x }) => X ↑i] [HasProduct fun (i : { x : I // P x }) => Y ↑i] [HasProduct fun (i : { x : I // ¬P x }) => Y ↑i] [(i : I) → Decidable (P i)] : map f = CategoryStruct.comp ((binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun (i : { x : I // P x }) => X ↑i) (∏ᶜ fun (i : { x : I // ¬P x }) => X ↑i))).hom (CategoryStruct.comp (prod.map (map fun (i : { x : I // P x }) => f ↑i) (map fun (i : { x : I // ¬P x }) => f ↑i)) ((binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun (i : { x : I // P x }) => Y ↑i) (∏ᶜ fun (i : { x : I // ¬P x }) => Y ↑i))).inv)