From b075189856abd9c2aa316c87dc2d6c3687739fdf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 21 Feb 2025 13:27:04 +0000 Subject: [PATCH] feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 morphisms of the form `Y ⟶ G` for some subobject `Y` of `G`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> --- .../EnoughInjectives.lean | 157 +++++++++++++++++- 1 file changed, 153 insertions(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean index e866eca85f44e..e1f6fe38343e0 100644 --- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean +++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean @@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ import Mathlib.CategoryTheory.Abelian.CommSq -import Mathlib.CategoryTheory.Generator.Basic +import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject import Mathlib.CategoryTheory.MorphismProperty.IsSmall -import Mathlib.CategoryTheory.MorphismProperty.Limits +import Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition +import Mathlib.Order.TransfiniteIteration /-! # Grothendieck abelian categories have enough injectives @@ -28,8 +29,9 @@ namespace IsGrothendieckAbelian /-- 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, -we shall show (TODO) that any monomorphism in `C` is a transfinite composition -of pushouts of monomorphisms in this family. -/ +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`). -/ def generatingMonomorphisms (G : C) : MorphismProperty C := MorphismProperty.ofHoms (fun (X : Subobject G) ↦ X.arrow) @@ -100,6 +102,153 @@ lemma exists_larger_subobject {X : C} (A : Subobject X) (hA : A ≠ ⊤) : simp only [← cancel_mono p', assoc, fac, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow] +variable {X : C} + +open Classical in +/-- 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`). -/ +noncomputable def largerSubobject (A : Subobject X) : Subobject X := + if hA : A = ⊤ then ⊤ else (exists_larger_subobject hG A hA).choose + +variable (X) in +@[simp] +lemma largerSubobject_top : largerSubobject hG (⊤ : Subobject X) = ⊤ := dif_pos rfl + +lemma lt_largerSubobject (A : Subobject X) (hA : A ≠ ⊤) : + A < largerSubobject hG A := by + dsimp only [largerSubobject] + rw [dif_neg hA] + exact (exists_larger_subobject hG A hA).choose_spec.choose + +lemma le_largerSubobject (A : Subobject X) : + A ≤ largerSubobject hG A := by + by_cases hA : A = ⊤ + · subst hA + simp only [largerSubobject_top, le_refl] + · exact (lt_largerSubobject hG A hA).le + +lemma pushouts_ofLE_le_largerSubobject (A : Subobject X) : + (generatingMonomorphisms G).pushouts + (Subobject.ofLE _ _ (le_largerSubobject hG A)) := by + by_cases hA : A = ⊤ + · subst hA + have := (Subobject.isIso_arrow_iff_eq_top (largerSubobject hG (⊤ : Subobject X))).2 (by simp) + exact (MorphismProperty.arrow_mk_iso_iff _ + (Arrow.isoMk (asIso (Subobject.arrow _)) (asIso (Subobject.arrow _)) (by simp))).2 + (isomorphisms_le_pushouts_generatingMonomorphisms G (𝟙 X) + (MorphismProperty.isomorphisms.infer_property _)) + · refine (MorphismProperty.arrow_mk_iso_iff _ ?_).1 + (exists_larger_subobject hG A hA).choose_spec.choose_spec + exact Arrow.isoMk (Iso.refl _) + (Subobject.isoOfEq _ _ ((by simp [largerSubobject, dif_neg hA]))) + +variable [IsGrothendieckAbelian.{w} C] + +lemma top_mem_range (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₀ = ⊤ := + top_mem_range_transfiniteIterate (largerSubobject hG) A₀ (lt_largerSubobject hG) (by simp) + (fun h ↦ by simpa [hasCardinalLT_iff_cardinal_mk_lt] using hJ.of_injective _ h) + +lemma exists_ordinal (A₀ : Subobject X) : + ∃ (o : Ordinal.{w}) (j : o.toType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤ := by + let κ := Order.succ (Cardinal.mk (Shrink.{w} (Subobject X))) + have : OrderBot κ.ord.toType := Ordinal.toTypeOrderBot (by + simp only [ne_eq, Cardinal.ord_eq_zero] + apply Cardinal.succ_ne_zero) + exact ⟨κ.ord, top_mem_range hG A₀ (lt_of_lt_of_le (Order.lt_succ _) (by simp [κ]))⟩ + +section + +variable (A₀ : Subobject X) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] + [WellFoundedLT J] + +/-- 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`. -/ +@[simps] +noncomputable def functorToMonoOver : J ⥤ MonoOver X where + obj j := MonoOver.mk' (transfiniteIterate (largerSubobject hG) j A₀).arrow + map {j j'} f := MonoOver.homMk (Subobject.ofLE _ _ + (monotone_transfiniteIterate _ _ (le_largerSubobject hG) (leOfHom f))) + +/-- The functor `J ⥤ C` induced by `functorToMonoOver hG A₀ J : J ⥤ MonoOver X`. -/ +noncomputable abbrev functor : J ⥤ C := + functorToMonoOver hG A₀ J ⋙ MonoOver.forget _ ⋙ Over.forget _ + +instance : (functor hG A₀ J).IsWellOrderContinuous where + nonempty_isColimit m hm := ⟨by + have : Nonempty (Set.Iio m) := ⟨⟨⊥, Ne.bot_lt (by simpa using hm.not_isMin)⟩⟩ + let c := (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget _) + have : Mono c.pt.hom := by dsimp [c]; infer_instance + apply IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup + ((Set.principalSegIio m).monotone.functor ⋙ functorToMonoOver hG A₀ J) c + dsimp [c] + simp only [Subobject.mk_arrow] + exact transfiniteIterate_limit (largerSubobject hG) A₀ m hm⟩ + +variable {J} in +/-- 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`. -/ +noncomputable def transfiniteCompositionOfShapeMapFromBot (j : J) : + (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (Set.Iic j) + ((functor hG A₀ J).map (homOfLE bot_le : ⊥ ⟶ j)) where + F := (Set.initialSegIic j).monotone.functor ⋙ functor hG A₀ J + isoBot := Iso.refl _ + incl := + { app k := (functor hG A₀ J).map (homOfLE k.2) + naturality k k' h := by simp [MonoOver.forget] } + isColimit := colimitOfDiagramTerminal isTerminalTop _ + map_mem k hk := by + dsimp [MonoOver.forget] + convert pushouts_ofLE_le_largerSubobject hG + (transfiniteIterate (largerSubobject hG) k.1 A₀) using 2 + all_goals + rw [Set.Iic.succ_eq_of_not_isMax hk, + transfiniteIterate_succ _ _ _ (Set.not_isMax_coe _ hk)] + +end + +variable {A : C} {f : A ⟶ X} [Mono 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`. -/ +noncomputable def transfiniteCompositionOfShapeOfEqTop + {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 := by + let t := transfiniteIterate (largerSubobject hG) j (Subobject.mk f) + have := (Subobject.isIso_arrow_iff_eq_top t).2 hj + apply (transfiniteCompositionOfShapeMapFromBot hG (Subobject.mk f) j).ofArrowIso + refine Arrow.isoMk ((Subobject.isoOfEq _ _ (transfiniteIterate_bot _ _) ≪≫ + Subobject.underlyingIso f)) (asIso t.arrow) ?_ + dsimp [MonoOver.forget] + rw [assoc, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow, + Subobject.ofLE_arrow] + +variable (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`. -/ +lemma exists_transfiniteCompositionOfShape : + ∃ (J : Type w) (_ : LinearOrder J) (_ : OrderBot J) (_ : SuccOrder J) + (_ : WellFoundedLT J), + Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f) := by + obtain ⟨o, j, hj⟩ := exists_ordinal hG (Subobject.mk f) + letI : OrderBot o.toType := Ordinal.toTypeOrderBot (by + simpa only [← Ordinal.toType_nonempty_iff_ne_zero] using Nonempty.intro j) + exact ⟨_, _, _, _, _, ⟨transfiniteCompositionOfShapeOfEqTop hG hj⟩⟩ + end generatingMonomorphisms end IsGrothendieckAbelian