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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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).

Equations

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

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.

Equations

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

@[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

theorem CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst_assoc {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] {Z : D} (h : G.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv (CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.prod.fst) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h

@[simp]

theorem CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst {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.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv (G.map CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.prod.fst

theorem CategoryTheory.Limits.PreservesLimitPair.iso_inv_snd_assoc {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] {Z : D} (h : G.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv (CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.prod.snd) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h

@[simp]

theorem CategoryTheory.Limits.PreservesLimitPair.iso_inv_snd {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.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv (G.map CategoryTheory.Limits.prod.snd) = CategoryTheory.Limits.prod.snd

instance CategoryTheory.Limits.instIsIsoProdComparison {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)

Equations

• ⋯ = ⋯

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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).

Equations

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

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.

Equations

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

@[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.instIsIsoCoprodComparison {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)

Equations

• ⋯ = ⋯