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} [CategoryTheory.Category.{u_3, u_1} C] (X : I → C) (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct fun (i : { x : I // P x }) => X ↑i] [CategoryTheory.Limits.HasProduct fun (i : { x : I // ¬P x }) => X ↑i] : CategoryTheory.Limits.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} [CategoryTheory.Category.{u_3, u_1} C] (X : I → C) (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct fun (i : { x : I // P x }) => X ↑i] [CategoryTheory.Limits.HasProduct fun (i : { x : I // ¬P x }) => X ↑i] [(i : I) → Decidable (P i)] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Pi.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} [CategoryTheory.Category.{u_3, u_1} C] {X : I → C} (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct fun (i : { x : I // P x }) => X ↑i] [CategoryTheory.Limits.HasProduct fun (i : { x : I // ¬P x }) => X ↑i] : CategoryTheory.Limits.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} [CategoryTheory.Category.{u_3, u_1} C] {X Y : I → C} (f : (i : I) → X i ⟶ Y i) (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [CategoryTheory.Limits.HasProduct fun (i : { x : I // P x }) => X ↑i] [CategoryTheory.Limits.HasProduct fun (i : { x : I // ¬P x }) => X ↑i] [CategoryTheory.Limits.HasProduct fun (i : { x : I // P x }) => Y ↑i] [CategoryTheory.Limits.HasProduct fun (i : { x : I // ¬P x }) => Y ↑i] [(i : I) → Decidable (P i)] : CategoryTheory.Limits.Pi.map f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (CategoryTheory.Limits.prodIsProd (∏ᶜ fun (i : { x : I // P x }) => X ↑i) (∏ᶜ fun (i : { x : I // ¬P x }) => X ↑i))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.Pi.map fun (i : { x : I // P x }) => f ↑i) (CategoryTheory.Limits.Pi.map fun (i : { x : I // ¬P x }) => f ↑i)) ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (CategoryTheory.Limits.prodIsProd (∏ᶜ fun (i : { x : I // P x }) => Y ↑i) (∏ᶜ fun (i : { x : I // ¬P x }) => Y ↑i))).inv)