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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) {P : C} (g : (j : J) → P ⟶ f j) : IsLimit (G.mapCone (Fan.mk P g)) ≃ IsLimit (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [PreservesLimit (Discrete.functor f) G] {P : C} (g : (j : J) → P ⟶ f j) (t : IsLimit (Fan.mk P g)) : IsLimit (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [ReflectsLimit (Discrete.functor f) G] {P : C} (g : (j : J) → P ⟶ f j) (t : IsLimit (Fan.mk (G.obj P) fun (j : J) => G.map (g j))) : IsLimit (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [HasProduct f] [PreservesLimit (Discrete.functor f) G] : IsLimit (Fan.mk (G.obj (∏ᶜ f)) fun (j : J) => G.map (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [HasProduct f] [HasProduct fun (j : J) => G.obj (f j)] [i : IsIso (piComparison G f)] : PreservesLimit (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [HasProduct f] [HasProduct fun (j : J) => G.obj (f j)] [PreservesLimit (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [HasProduct f] [HasProduct fun (j : J) => G.obj (f j)] [PreservesLimit (Discrete.functor f) G] : (iso G f).hom = piComparison G f

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

def CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) {P : C} (g : (j : J) → f j ⟶ P) : IsColimit (G.mapCocone (Cofan.mk P g)) ≃ IsColimit (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [PreservesColimit (Discrete.functor f) G] {P : C} (g : (j : J) → f j ⟶ P) (t : IsColimit (Cofan.mk P g)) : IsColimit (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [ReflectsColimit (Discrete.functor f) G] {P : C} (g : (j : J) → f j ⟶ P) (t : IsColimit (Cofan.mk (G.obj P) fun (j : J) => G.map (g j))) : IsColimit (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [HasCoproduct f] [PreservesColimit (Discrete.functor f) G] : IsColimit (Cofan.mk (G.obj (∐ f)) fun (j : J) => G.map (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [HasCoproduct f] [HasCoproduct fun (j : J) => G.obj (f j)] [i : IsIso (sigmaComparison G f)] : PreservesColimit (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [HasCoproduct f] [HasCoproduct fun (j : J) => G.obj (f j)] [PreservesColimit (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {J : Type w} (f : J → C) [HasCoproduct f] [HasCoproduct fun (j : J) => G.obj (f j)] [PreservesColimit (Discrete.functor f) G] : (iso G f).inv = sigmaComparison G f

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

theorem CategoryTheory.Limits.preservesLimitsOfShape_of_discrete {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} (F : Functor C D) [∀ (f : J → C), PreservesLimit (Discrete.functor f) F] : PreservesLimitsOfShape (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} (F : Functor C D) [∀ (f : J → C), PreservesColimit (Discrete.functor f) F] : PreservesColimitsOfShape (Discrete J) F

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