Preserving products

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

In particular, we show that piComparison G f is an isomorphism iff G preserves the limit of f.

def CategoryTheory.Limits.isLimitMapConeFanMkEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) {P : C} (g : (j : J) → P ⟶ f j) : CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.Fan.mk P g)) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj P) fun j => G.map (g j))

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

def CategoryTheory.Limits.isLimitFanMkObjOfIsLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] {P : C} (g : (j : J) → P ⟶ f j) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk P g)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj P) fun j => G.map (g j))

The property of preserving products expressed in terms of fans.

def CategoryTheory.Limits.isLimitOfIsLimitFanMkObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Discrete.functor f) G] {P : C} (g : (j : J) → P ⟶ f j) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj P) fun j => G.map (g j))) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk P g)

The property of reflecting products expressed in terms of fans.

def CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj (∏ f)) fun j => G.map (CategoryTheory.Limits.Pi.π f j))

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

def CategoryTheory.Limits.PreservesProduct.ofIsoComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G

If pi_comparison G f is an isomorphism, then G preserves the limit of f.

def CategoryTheory.Limits.PreservesProduct.iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : G.obj (∏ f) ≅ ∏ fun j => G.obj (f j)

If G preserves limits, we have an isomorphism from the image of a product to the product of the images.

@[simp]

theorem CategoryTheory.Limits.PreservesProduct.iso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : (CategoryTheory.Limits.PreservesProduct.iso G f).hom = CategoryTheory.Limits.piComparison G f

instance CategoryTheory.Limits.instIsIsoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorPiObjPiObjPiComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)

def CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) {P : C} (g : (j : J) → f j ⟶ P) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.Cofan.mk P g)) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j))

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

def CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] {P : C} (g : (j : J) → f j ⟶ P) (t : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk P g)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j))

The property of preserving coproducts expressed in terms of cofans.

def CategoryTheory.Limits.isColimitOfIsColimitCofanMkObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Discrete.functor f) G] {P : C} (g : (j : J) → f j ⟶ P) (t : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j))) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk P g)

The property of reflecting coproducts expressed in terms of cofans.

def CategoryTheory.Limits.isColimitOfHasCoproductOfPreservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj (∐ f)) fun j => G.map (CategoryTheory.Limits.Sigma.ι f j))

If G preserves coproducts and C has them, then the cofan constructed of the mapped inclusion of a coproduct is a colimit.

def CategoryTheory.Limits.PreservesCoproduct.ofIsoComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.sigmaComparison G f)] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G

If sigma_comparison G f is an isomorphism, then G preserves the colimit of f.

def CategoryTheory.Limits.PreservesCoproduct.iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] : G.obj (∐ f) ≅ ∐ fun j => G.obj (f j)

If G preserves colimits, we have an isomorphism from the image of a coproduct to the coproduct of the images.

@[simp]

theorem CategoryTheory.Limits.PreservesCoproduct.inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] : (CategoryTheory.Limits.PreservesCoproduct.iso G f).inv = CategoryTheory.Limits.sigmaComparison G f

instance CategoryTheory.Limits.instIsIsoSigmaObjObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorSigmaObjSigmaComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.IsIso (CategoryTheory.Limits.sigmaComparison G f)