# Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

# 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₁} [] {D : Type u₂} [] (G : ) {P : C} {X : C} {Y : C} (f : P X) (g : P Y) :

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.

Instances For
def CategoryTheory.Limits.mapIsLimitOfPreservesOfIsLimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {P : C} {X : C} {Y : C} (f : P X) (g : P Y) :

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

Instances For
def CategoryTheory.Limits.isLimitOfReflectsOfMapIsLimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {P : C} {X : C} {Y : C} (f : P X) (g : P Y) (l : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (G.map f) (G.map g))) :

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

Instances For
def CategoryTheory.Limits.isLimitOfHasBinaryProductOfPreservesLimit {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) (Y : C) :
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.

Instances For
def CategoryTheory.Limits.PreservesLimitPair.ofIsoProdComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)] [i : ] :

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

Instances For
def CategoryTheory.Limits.PreservesLimitPair.iso {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)] :
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.

Instances For
@[simp]
theorem CategoryTheory.Limits.PreservesLimitPair.iso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)] :
def CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv {C : Type u₁} [] {D : Type u₂} [] (G : ) {P : C} {X : C} {Y : C} (f : X P) (g : Y P) :

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.

Instances For
def CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {P : C} {X : C} {Y : C} (f : X P) (g : Y P) :

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

Instances For
def CategoryTheory.Limits.isColimitOfReflectsOfMapIsColimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {P : C} {X : C} {Y : C} (f : X P) (g : Y P) (l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (G.map f) (G.map g))) :

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

Instances For
def CategoryTheory.Limits.isColimitOfHasBinaryCoproductOfPreservesColimit {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) (Y : C) :
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.

Instances For
def CategoryTheory.Limits.PreservesColimitPair.ofIsoCoprodComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)] :

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

Instances For
def CategoryTheory.Limits.PreservesColimitPair.iso {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)] :
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.

Instances For
@[simp]
theorem CategoryTheory.Limits.PreservesColimitPair.iso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryCoproduct (G.obj X) (G.obj Y)] :