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

Equations

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

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 : J) => G.map (g j))

The property of preserving products expressed in terms of fans.

Equations

• CategoryTheory.Limits.isLimitFanMkObjOfIsLimit G f g t = (CategoryTheory.Limits.isLimitMapConeFanMkEquiv G f g) (CategoryTheory.Limits.isLimitOfPreserves G t)

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 : J) => G.map (g j))) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk P g)

The property of reflecting products expressed in terms of fans.

Equations

• CategoryTheory.Limits.isLimitOfIsLimitFanMkObj G f g t = CategoryTheory.Limits.isLimitOfReflects G ((CategoryTheory.Limits.isLimitMapConeFanMkEquiv G f g).symm t)

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

Equations

• CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit G f = CategoryTheory.Limits.isLimitFanMkObjOfIsLimit G f (CategoryTheory.Limits.Pi.π f) (CategoryTheory.Limits.productIsProduct f)

theorem CategoryTheory.Limits.PreservesProduct.of_iso_comparison {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 : 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 : J) => G.obj (f j)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] : G.obj (∏ᶜ f) ≅ ∏ᶜ fun (j : 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.

Equations

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

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

theorem CategoryTheory.Limits.instIsIsoPiComparison {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 : 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 : 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.

Equations

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

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 : J) => G.map (g j))

The property of preserving coproducts expressed in terms of cofans.

Equations

• CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit G f g t = (CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv G f g) (CategoryTheory.Limits.isColimitOfPreserves G t)

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 : J) => G.map (g j))) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk P g)

The property of reflecting coproducts expressed in terms of cofans.

Equations

• CategoryTheory.Limits.isColimitOfIsColimitCofanMkObj G f g t = CategoryTheory.Limits.isColimitOfReflects G ((CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv G f g).symm t)

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

Equations

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

theorem CategoryTheory.Limits.PreservesCoproduct.of_iso_comparison {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 : 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 : J) => G.obj (f j)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] : G.obj (∐ f) ≅ ∐ fun (j : 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.

Equations

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

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

theorem CategoryTheory.Limits.instIsIsoSigmaComparison {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 : J) => G.obj (f j)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] : CategoryTheory.IsIso (CategoryTheory.Limits.sigmaComparison G f)

theorem CategoryTheory.Limits.preservesLimitsOfShape_of_discrete {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} (F : CategoryTheory.Functor C D) [∀ (f : J → C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F

If F preserves the limit of every Discrete.functor f, it preserves all limits of shape Discrete J.

theorem CategoryTheory.Limits.preservesColimitsOfShape_of_discrete {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} (F : CategoryTheory.Functor C D) [∀ (f : J → C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) F] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F

If F preserves the colimit of every Discrete.functor f, it preserves all colimits of shape Discrete J.