Grothendieck abelian categories have enough injectives

Let C be a Grothendieck abelian category. In this file, we formalize the theorem by Grothendieck that C has enough injectives.

We recall that injective objects can be characterized in terms of lifting properties (see the file Preadditive.Injective.LiftingProperties): an object I : C is injective iff the morphism I ⟶ 0 has the right lifting property with respect to all monomorphisms.

The main technical lemma in this file is the lemma generatingMonomorphisms_rlp which states that if G is a generator of C, then a morphism X ⟶ Y has the right lifting property with respect to the inclusions of subobjects of G iff it has the right lifting property with respect to all monomorphisms. Then, we can apply the small object argument to the family of morphisms generatingMonomorphisms G which consists of the inclusions of subobjects of G. When it is applied to the morphism X ⟶ 0, the factorization given by the small object is a factorization X ⟶ I ⟶ 0 where I is injective (because I ⟶ 0 has the expected right lifting properties), and X ⟶ I is a monomorphism because it is a transfinite composition of monomorphisms (this uses the axiom AB5).

The proof of the technical lemma generatingMonomorphisms_rlp that was formalized is not exactly the same as in the mathematical literature. Assume that p : X ⟶ Y has the lifting property with respect to monomorphisms in the family generatingMonomorphisms G. We would like to show that p has the right lifting property with respect to any monomorphism i : A ⟶ B. In various sources, given a commutative square with i on the left and p on the right, the ordered set of subobjects A' of B containing A equipped with a lifting A' ⟶ X is introduced. The existence of a lifting B ⟶ X is usually obtained by applying Zorn's lemma in this situation. Here, we split the argument into two separate facts:

• any monomorphism A ⟶ B is a transfinite composition of pushouts of monomorphisms in generatingMonomorphisms G (see generatingMonomorphisms.exists_transfiniteCompositionOfShape);
• the class of morphisms that have the left lifting property with respect to p is stable under transfinite composition (see the file SmallObject.TransfiniteCompositionLifting).

References

• [Alexander Grothendieck, Sur quelques points d'algèbre homologique][grothendieck-1957]

def CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms {C : Type u} [Category.{v, u} C] (G : C) : MorphismProperty C

Given an object G : C, this is the family of morphisms in C given by the inclusions of all subobjects of G. If G is a separator, and C is a Grothendieck abelian category, then any monomorphism in C is a transfinite composition of pushouts of monomorphisms in this family (see generatingMonomorphisms.exists_transfiniteCompositionOfShape).

Equations

• CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G = CategoryTheory.MorphismProperty.ofHoms fun (X : CategoryTheory.Subobject G) => X.arrow

instance CategoryTheory.IsGrothendieckAbelian.instIsSmallGeneratingMonomorphismsOfSmallSubobject {C : Type u} [Category.{v, u} C] (G : C) [Small.{w, max u v} (Subobject G)] : MorphismProperty.IsSmall.{w, v, u} (generatingMonomorphisms G)

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_le_monomorphisms {C : Type u} [Category.{v, u} C] (G : C) : generatingMonomorphisms G ≤ MorphismProperty.monomorphisms C

theorem CategoryTheory.IsGrothendieckAbelian.isomorphisms_le_pushouts_generatingMonomorphisms {C : Type u} [Category.{v, u} C] (G : C) [Limits.HasZeroMorphisms C] : MorphismProperty.isomorphisms C ≤ (generatingMonomorphisms G).pushouts

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_pushouts {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X Y : C} (p : X ⟶ Y) [Mono p] (hp : ¬IsIso p) : ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'), CategoryStruct.comp i p' = p

If p : X ⟶ Y is a monomorphism that is not an isomorphism, there exists a subobject X' of Y containing X (but different from X) such that the inclusion X ⟶ X' is a pushout of a monomorphism in the family generatingMonomorphisms G.

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} (A : Subobject X) (hA : A ≠ ⊤) : ∃ (A' : Subobject X) (h : A < A'), (generatingMonomorphisms G).pushouts (A.ofLE A' ⋯)

noncomputable def CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} (A : Subobject X) : Subobject X

Assuming G : C is a generator, X : C, and A : Subobject X, this is a subobject of X which is ⊤ if A = ⊤, and otherwise it is a larger subobject given by the lemma exists_larger_subobject. The inclusion of A in largerSubobject hG A is a pushout of a monomorphism in the family generatingMonomorphisms G (see pushouts_ofLE_le_largerSubobject).

Equations

• CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG A = if hA : A = ⊤ then ⊤ else ⋯.choose

@[simp]

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject_top {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) (X : C) : largerSubobject hG ⊤ = ⊤

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.lt_largerSubobject {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} (A : Subobject X) (hA : A ≠ ⊤) : A < largerSubobject hG A

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.le_largerSubobject {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} (A : Subobject X) : A ≤ largerSubobject hG A

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.pushouts_ofLE_le_largerSubobject {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} (A : Subobject X) : (generatingMonomorphisms G).pushouts (A.ofLE (largerSubobject hG A) ⋯)

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} [IsGrothendieckAbelian.{w, v, u} C] (A₀ : Subobject X) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] (hJ : HasCardinalLT (Subobject X) (Cardinal.mk J)) : ∃ (j : J), transfiniteIterate (largerSubobject hG) j A₀ = ⊤

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} [IsGrothendieckAbelian.{w, v, u} C] (A₀ : Subobject X) : ∃ (o : Ordinal.{w}) (j : o.toType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤

noncomputable def CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} [IsGrothendieckAbelian.{w, v, u} C] (A₀ : Subobject X) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] : Functor J (MonoOver X)

Let C be a Grothendieck abelian category with a generator (hG), X : C, A₀ : Subobject X. Let J be a well ordered type. This is the functor J ⥤ MonoOver X which corresponds to the evaluation at A₀ of the transfinite iteration of the map largerSubobject hG : Subobject X → Subobject X.

Equations

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

@[simp]

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} [IsGrothendieckAbelian.{w, v, u} C] (A₀ : Subobject X) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {j j' : J} (f : j ⟶ j') : (functorToMonoOver hG A₀ J).map f = MonoOver.homMk ((transfiniteIterate (largerSubobject hG) j A₀).ofLE (transfiniteIterate (largerSubobject hG) j' A₀) ⋯) ⋯

@[simp]

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} [IsGrothendieckAbelian.{w, v, u} C] (A₀ : Subobject X) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] (j : J) : (functorToMonoOver hG A₀ J).obj j = MonoOver.mk' (transfiniteIterate (largerSubobject hG) j A₀).arrow

@[reducible, inline]

noncomputable abbrev CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functor {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} [IsGrothendieckAbelian.{w, v, u} C] (A₀ : Subobject X) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] : Functor J C

The functor J ⥤ C induced by functorToMonoOver hG A₀ J : J ⥤ MonoOver X.

Equations

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

instance CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.instIsWellOrderContinuousFunctor {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} [IsGrothendieckAbelian.{w, v, u} C] (A₀ : Subobject X) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] : (functor hG A₀ J).IsWellOrderContinuous

noncomputable def CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeMapFromBot {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} [IsGrothendieckAbelian.{w, v, u} C] (A₀ : Subobject X) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] (j : J) : (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (↑(Set.Iic j)) ((functor hG A₀ J).map (homOfLE ⋯))

For any j, the map (functor hG A₀ J).map (homOfLE bot_le : ⊥ ⟶ j) is a transfinite composition of pushouts of monomorphisms in the family generatingMonomorphisms G.

Equations

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

noncomputable def CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeOfEqTop {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} [IsGrothendieckAbelian.{w, v, u} C] {A : C} {f : A ⟶ X} [Mono f] {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {j : J} (hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤) : (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (↑(Set.Iic j)) f

If transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤, then the monomorphism f is a transfinite composition of pushouts of monomorphisms in the family generatingMonomorphisms G.

Equations

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

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_transfiniteCompositionOfShape {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] (hG : IsSeparator G) {X : C} [IsGrothendieckAbelian.{w, v, u} C] {A : C} (f : A ⟶ X) [Mono f] : ∃ (J : Type w) (x : LinearOrder J) (x_1 : OrderBot J) (x_2 : SuccOrder J) (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Let C be a Grothendieck abelian category. Assume that G : C is a generator of C. Then, any morphism in C is a transfinite composition of pushouts of monomorphisms in the family generatingMonomorphisms G which consists of the inclusions of the subobjects of G.

theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms_rlp {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] (hG : IsSeparator G) : (generatingMonomorphisms G).rlp = (MorphismProperty.monomorphisms C).rlp

instance CategoryTheory.IsGrothendieckAbelian.instHasSmallObjectArgumentGeneratingMonomorphisms {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] : (generatingMonomorphisms G).HasSmallObjectArgument

theorem CategoryTheory.IsGrothendieckAbelian.llp_rlp_monomorphisms {C : Type u} [Category.{v, u} C] {G : C} [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] (hG : IsSeparator G) : (MorphismProperty.monomorphisms C).rlp.llp = MorphismProperty.monomorphisms C

instance CategoryTheory.IsGrothendieckAbelian.instHasFunctorialFactorizationMonomorphismsRlp {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] : (MorphismProperty.monomorphisms C).HasFunctorialFactorization (MorphismProperty.monomorphisms C).rlp

@[reducible, inline]

noncomputable abbrev CategoryTheory.IsGrothendieckAbelian.monoMapFactorizationDataRlp {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] {X Y : C} (f : X ⟶ Y) : (MorphismProperty.monomorphisms C).MapFactorizationData (MorphismProperty.monomorphisms C).rlp f

A (functorial) factorization of any morphisms in a Grothendieck abelian category as a monomorphism followed by a morphism which has the right lifting property with respect to all monomorphisms.

Equations

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

instance CategoryTheory.IsGrothendieckAbelian.instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] {X Y : C} (f : X ⟶ Y) : Mono (monoMapFactorizationDataRlp f).i

instance CategoryTheory.IsGrothendieckAbelian.instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] {X : C} : Injective (monoMapFactorizationDataRlp 0).Z

instance CategoryTheory.IsGrothendieckAbelian.enoughInjectives {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] : EnoughInjectives C

A Grothendieck abelian category has enough injectives.

Stacks Tag 079H