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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {P : C} {X : C} {Y : C} (f : P ⟶ X) (g : P ⟶ Y) : CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.BinaryFan.mk f g)) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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.

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

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

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

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

def CategoryTheory.Limits.isLimitOfHasBinaryProductOfPreservesLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (G.map CategoryTheory.Limits.prod.fst) (G.map CategoryTheory.Limits.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.

def CategoryTheory.Limits.PreservesLimitPair.ofIsoProdComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison G X Y)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.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.

@[simp]

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

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

def CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {P : C} {X : C} {Y : C} (f : X ⟶ P) (g : Y ⟶ P) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.BinaryCofan.mk f g)) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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.

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

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

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

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

def CategoryTheory.Limits.isColimitOfHasBinaryCoproductOfPreservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) G] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (G.map CategoryTheory.Limits.coprod.inl) (G.map CategoryTheory.Limits.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.

def CategoryTheory.Limits.PreservesColimitPair.ofIsoCoprodComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison G X Y)] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.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.

@[simp]

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

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