Preserving binary products

Constructions to relate the notions of preserving binary products and reflecting binary products to concrete binary fans.

In particular, we show that ProdComparison G X Y is an isomorphism iff G preserves the product of X and Y.

def CategoryTheory.Limits.isLimitMapConeBinaryFanEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : P ⟶ X) (g : P ⟶ Y) : IsLimit (G.mapCone (BinaryFan.mk f g)) ≃ IsLimit (BinaryFan.mk (G.map f) (G.map g))

The map of a binary fan is a limit iff the fork consisting of the mapped morphisms is a limit. This essentially lets us commute BinaryFan.mk with Functor.mapCone.

Equations

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

def CategoryTheory.Limits.mapIsLimitOfPreservesOfIsLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : P ⟶ X) (g : P ⟶ Y) [PreservesLimit (pair X Y) G] (l : IsLimit (BinaryFan.mk f g)) : IsLimit (BinaryFan.mk (G.map f) (G.map g))

The property of preserving products expressed in terms of binary fans.

Equations

• CategoryTheory.Limits.mapIsLimitOfPreservesOfIsLimit G f g l = (CategoryTheory.Limits.isLimitMapConeBinaryFanEquiv G f g) (CategoryTheory.Limits.isLimitOfPreserves G l)

def CategoryTheory.Limits.isLimitOfReflectsOfMapIsLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : P ⟶ X) (g : P ⟶ Y) [ReflectsLimit (pair X Y) G] (l : IsLimit (BinaryFan.mk (G.map f) (G.map g))) : IsLimit (BinaryFan.mk f g)

The property of reflecting products expressed in terms of binary fans.

Equations

• CategoryTheory.Limits.isLimitOfReflectsOfMapIsLimit G f g l = CategoryTheory.Limits.isLimitOfReflects G ((CategoryTheory.Limits.isLimitMapConeBinaryFanEquiv G f g).symm l)

def CategoryTheory.Limits.isLimitOfHasBinaryProductOfPreservesLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryProduct X Y] [PreservesLimit (pair X Y) G] : IsLimit (BinaryFan.mk (G.map prod.fst) (G.map prod.snd))

If G preserves binary products and C has them, then the binary fan constructed of the mapped morphisms of the binary product cone is a limit.

Equations

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

theorem CategoryTheory.Limits.PreservesLimitPair.of_iso_prod_comparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryProduct X Y] [HasBinaryProduct (G.obj X) (G.obj Y)] [i : IsIso (prodComparison G X Y)] : PreservesLimit (pair X Y) G

If the product comparison map for G at (X,Y) is an isomorphism, then G preserves the pair of (X,Y).

def CategoryTheory.Limits.PreservesLimitPair.iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryProduct X Y] [HasBinaryProduct (G.obj X) (G.obj Y)] [PreservesLimit (pair X Y) G] : G.obj (X ⨯ Y) ≅ G.obj X ⨯ G.obj Y

If G preserves the product of (X,Y), then the product comparison map for G at (X,Y) is an isomorphism.

Equations

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

@[simp]

theorem CategoryTheory.Limits.PreservesLimitPair.iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryProduct X Y] [HasBinaryProduct (G.obj X) (G.obj Y)] [PreservesLimit (pair X Y) G] : (iso G X Y).hom = prodComparison G X Y

@[simp]

theorem CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryProduct X Y] [HasBinaryProduct (G.obj X) (G.obj Y)] [PreservesLimit (pair X Y) G] : CategoryStruct.comp (iso G X Y).inv (G.map prod.fst) = prod.fst

theorem CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryProduct X Y] [HasBinaryProduct (G.obj X) (G.obj Y)] [PreservesLimit (pair X Y) G] {Z : D} (h : G.obj X ⟶ Z) : CategoryStruct.comp (iso G X Y).inv (CategoryStruct.comp (G.map prod.fst) h) = CategoryStruct.comp prod.fst h

@[simp]

theorem CategoryTheory.Limits.PreservesLimitPair.iso_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryProduct X Y] [HasBinaryProduct (G.obj X) (G.obj Y)] [PreservesLimit (pair X Y) G] : CategoryStruct.comp (iso G X Y).inv (G.map prod.snd) = prod.snd

theorem CategoryTheory.Limits.PreservesLimitPair.iso_inv_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryProduct X Y] [HasBinaryProduct (G.obj X) (G.obj Y)] [PreservesLimit (pair X Y) G] {Z : D} (h : G.obj Y ⟶ Z) : CategoryStruct.comp (iso G X Y).inv (CategoryStruct.comp (G.map prod.snd) h) = CategoryStruct.comp prod.snd h

instance CategoryTheory.Limits.instIsIsoProdComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryProduct X Y] [HasBinaryProduct (G.obj X) (G.obj Y)] [PreservesLimit (pair X Y) G] : IsIso (prodComparison G X Y)

def CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : X ⟶ P) (g : Y ⟶ P) : IsColimit (G.mapCocone (BinaryCofan.mk f g)) ≃ IsColimit (BinaryCofan.mk (G.map f) (G.map g))

The map of a binary cofan is a colimit iff the cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute BinaryCofan.mk with Functor.mapCocone.

Equations

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

def CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : X ⟶ P) (g : Y ⟶ P) [PreservesColimit (pair X Y) G] (l : IsColimit (BinaryCofan.mk f g)) : IsColimit (BinaryCofan.mk (G.map f) (G.map g))

The property of preserving coproducts expressed in terms of binary cofans.

Equations

• CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit G f g l = (CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv G f g) (CategoryTheory.Limits.isColimitOfPreserves G l)

def CategoryTheory.Limits.isColimitOfReflectsOfMapIsColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : X ⟶ P) (g : Y ⟶ P) [ReflectsColimit (pair X Y) G] (l : IsColimit (BinaryCofan.mk (G.map f) (G.map g))) : IsColimit (BinaryCofan.mk f g)

The property of reflecting coproducts expressed in terms of binary cofans.

Equations

• CategoryTheory.Limits.isColimitOfReflectsOfMapIsColimit G f g l = CategoryTheory.Limits.isColimitOfReflects G ((CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv G f g).symm l)

def CategoryTheory.Limits.isColimitOfHasBinaryCoproductOfPreservesColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryCoproduct X Y] [PreservesColimit (pair X Y) G] : IsColimit (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr))

If G preserves binary coproducts and C has them, then the binary cofan constructed of the mapped morphisms of the binary product cocone is a colimit.

Equations

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

theorem CategoryTheory.Limits.PreservesColimitPair.of_iso_coprod_comparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryCoproduct X Y] [HasBinaryCoproduct (G.obj X) (G.obj Y)] [i : IsIso (coprodComparison G X Y)] : PreservesColimit (pair X Y) G

If the coproduct comparison map for G at (X,Y) is an isomorphism, then G preserves the pair of (X,Y).

def CategoryTheory.Limits.PreservesColimitPair.iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryCoproduct X Y] [HasBinaryCoproduct (G.obj X) (G.obj Y)] [PreservesColimit (pair X Y) G] : G.obj X ⨿ G.obj Y ≅ G.obj (X ⨿ Y)

If G preserves the coproduct of (X,Y), then the coproduct comparison map for G at (X,Y) is an isomorphism.

Equations

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

@[simp]

theorem CategoryTheory.Limits.PreservesColimitPair.iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryCoproduct X Y] [HasBinaryCoproduct (G.obj X) (G.obj Y)] [PreservesColimit (pair X Y) G] : (iso G X Y).hom = coprodComparison G X Y

instance CategoryTheory.Limits.instIsIsoCoprodComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryCoproduct X Y] [HasBinaryCoproduct (G.obj X) (G.obj Y)] [PreservesColimit (pair X Y) G] : IsIso (coprodComparison G X Y)