Exactness of colimits

In this file, we shall study exactness properties of colimits. First, we translate the assumption that colim : (J ⥤ C) ⥤ C preserves monomorphisms (resp. preserves epimorphisms, resp. is exact) into statements involving arbitrary cocones instead of the ones given by the colimit API. We also show that when an inductive system involves only monomorphisms, then the "inclusion" morphism into the colimit is also a monomorphism (assuming J is filtered and C satisfies AB5).

theorem CategoryTheory.Limits.colim.map_mono' {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] [HasColimitsOfShape J C] [colim.PreservesMonomorphisms] {X₁ X₂ : Functor J C} (φ : X₁ ⟶ X₂) [Mono φ] {c₁ : Cocone X₁} (hc₁ : IsColimit c₁) {c₂ : Cocone X₂} (hc₂ : IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (hf : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) f = CategoryStruct.comp (φ.app j) (c₂.ι.app j)) : Mono f

Assume that colim : (J ⥤ C) ⥤ C preserves monomorphisms, and φ : X₁ ⟶ X₂ is a monomorphism in J ⥤ C, then if f : c₁.pt ⟶ c₂.pt is a morphism between the points of colimit cocones for X₁ and X₂ in such a way that f idenfities to colim.map φ, then f is a monomorphism.

theorem CategoryTheory.Limits.colim.map_epi' {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] {X₁ X₂ : Functor J C} (φ : X₁ ⟶ X₂) [∀ (j : J), Epi (φ.app j)] (c₁ : Cocone X₁) {c₂ : Cocone X₂} (hc₂ : IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (hf : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) f = CategoryStruct.comp (φ.app j) (c₂.ι.app j)) : Epi f

Assume that φ : X₁ ⟶ X₂ is a natural transformation in J ⥤ C which consists of epimorphisms, then if f : c₁.pt ⟶ c₂.pt is a morphism between the points of cocones c₁ and c₂ for X₁ and X₂, in such a way that c₂ is colimit and f is compatible with φ, then f is an epimorphism.

theorem CategoryTheory.Limits.IsColimit.mono_ι_app_of_isFiltered {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] {X : Functor J C} [∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)] {c : Cocone X} (hc : IsColimit c) [IsFiltered J] (j₀ : J) [HasColimitsOfShape (Under j₀) C] [colim.PreservesMonomorphisms] : Mono (c.ι.app j₀)

Assume that a functor X : J ⥤ C maps any morphism to a monomorphism, that J is filtered. Then the "inclusion" map c.ι.app j₀ of a colimit cocone for X is a monomorphism if colim : (Under j₀ ⥤ C) ⥤ C preserves monomorphisms (e.g. when C satisfies AB5).

def CategoryTheory.Limits.colim.mapShortComplex {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] [HasZeroMorphisms C] (S : ShortComplex (Functor J C)) {c₁ : Cocone S.X₁} (hc₁ : IsColimit c₁) (c₂ : Cocone S.X₂) (c₃ : Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt) (g : c₂.pt ⟶ c₃.pt) (hf : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) f = CategoryStruct.comp (S.f.app j) (c₂.ι.app j)) (hg : ∀ (j : J), CategoryStruct.comp (c₂.ι.app j) g = CategoryStruct.comp (S.g.app j) (c₃.ι.app j)) : ShortComplex C

Given S : ShortCompex (J ⥤ C) and (colimit) cocones for S.X₁, S.X₂, S.X₃ equipped with suitable data, this is the induced short complex c₁.pt ⟶ c₂.pt ⟶ c₃.pt.

Equations

• CategoryTheory.Limits.colim.mapShortComplex S hc₁ c₂ c₃ f g hf hg = CategoryTheory.ShortComplex.mk f g ⋯

@[simp]

theorem CategoryTheory.Limits.colim.mapShortComplex_f {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] [HasZeroMorphisms C] (S : ShortComplex (Functor J C)) {c₁ : Cocone S.X₁} (hc₁ : IsColimit c₁) (c₂ : Cocone S.X₂) (c₃ : Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt) (g : c₂.pt ⟶ c₃.pt) (hf : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) f = CategoryStruct.comp (S.f.app j) (c₂.ι.app j)) (hg : ∀ (j : J), CategoryStruct.comp (c₂.ι.app j) g = CategoryStruct.comp (S.g.app j) (c₃.ι.app j)) : (mapShortComplex S hc₁ c₂ c₃ f g hf hg).f = f

@[simp]

theorem CategoryTheory.Limits.colim.mapShortComplex_g {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] [HasZeroMorphisms C] (S : ShortComplex (Functor J C)) {c₁ : Cocone S.X₁} (hc₁ : IsColimit c₁) (c₂ : Cocone S.X₂) (c₃ : Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt) (g : c₂.pt ⟶ c₃.pt) (hf : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) f = CategoryStruct.comp (S.f.app j) (c₂.ι.app j)) (hg : ∀ (j : J), CategoryStruct.comp (c₂.ι.app j) g = CategoryStruct.comp (S.g.app j) (c₃.ι.app j)) : (mapShortComplex S hc₁ c₂ c₃ f g hf hg).g = g

@[simp]

theorem CategoryTheory.Limits.colim.mapShortComplex_X₃ {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] [HasZeroMorphisms C] (S : ShortComplex (Functor J C)) {c₁ : Cocone S.X₁} (hc₁ : IsColimit c₁) (c₂ : Cocone S.X₂) (c₃ : Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt) (g : c₂.pt ⟶ c₃.pt) (hf : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) f = CategoryStruct.comp (S.f.app j) (c₂.ι.app j)) (hg : ∀ (j : J), CategoryStruct.comp (c₂.ι.app j) g = CategoryStruct.comp (S.g.app j) (c₃.ι.app j)) : (mapShortComplex S hc₁ c₂ c₃ f g hf hg).X₃ = c₃.pt

@[simp]

theorem CategoryTheory.Limits.colim.mapShortComplex_X₁ {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] [HasZeroMorphisms C] (S : ShortComplex (Functor J C)) {c₁ : Cocone S.X₁} (hc₁ : IsColimit c₁) (c₂ : Cocone S.X₂) (c₃ : Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt) (g : c₂.pt ⟶ c₃.pt) (hf : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) f = CategoryStruct.comp (S.f.app j) (c₂.ι.app j)) (hg : ∀ (j : J), CategoryStruct.comp (c₂.ι.app j) g = CategoryStruct.comp (S.g.app j) (c₃.ι.app j)) : (mapShortComplex S hc₁ c₂ c₃ f g hf hg).X₁ = c₁.pt

@[simp]

theorem CategoryTheory.Limits.colim.mapShortComplex_X₂ {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] [HasZeroMorphisms C] (S : ShortComplex (Functor J C)) {c₁ : Cocone S.X₁} (hc₁ : IsColimit c₁) (c₂ : Cocone S.X₂) (c₃ : Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt) (g : c₂.pt ⟶ c₃.pt) (hf : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) f = CategoryStruct.comp (S.f.app j) (c₂.ι.app j)) (hg : ∀ (j : J), CategoryStruct.comp (c₂.ι.app j) g = CategoryStruct.comp (S.g.app j) (c₃.ι.app j)) : (mapShortComplex S hc₁ c₂ c₃ f g hf hg).X₂ = c₂.pt

theorem CategoryTheory.Limits.colim.exact_mapShortComplex {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] [HasZeroMorphisms C] {S : ShortComplex (Functor J C)} (hS : S.Exact) {c₁ : Cocone S.X₁} (hc₁ : IsColimit c₁) {c₂ : Cocone S.X₂} (hc₂ : IsColimit c₂) {c₃ : Cocone S.X₃} (hc₃ : IsColimit c₃) (f : c₁.pt ⟶ c₂.pt) (g : c₂.pt ⟶ c₃.pt) (hf : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) f = CategoryStruct.comp (S.f.app j) (c₂.ι.app j)) (hg : ∀ (j : J), CategoryStruct.comp (c₂.ι.app j) g = CategoryStruct.comp (S.g.app j) (c₃.ι.app j)) : (mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact

Assuming HasExactColimitsOfShape J C, this lemma rephrases the exactness of the functor colim : (J ⥤ C) ⥤ C by saying that if S : ShortComplex (J ⥤ C) is exact, then the short complex obtained by taking the colimits is exact, where we allow the replacement of the chosen colimit cocones of the colimit API by arbitrary colimit cocones.