19 Injectives

Chapter 19 of the Stacks Project, Injectives, Tag 01D4: the 14 sections of its 15 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 59 tags are carried by 150 declarations of the repository (all in StacksFrontier) and 9 registered declarations.

Section19.2 Baer's argument for modules #

Section 19.2 of the Stacks Project, Tag 05NM. 8 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05NN, an equation

Tag 05NN in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Limits.colimit.post registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch19.lean, line 20 (StacksFrontier).

Tag 05NR, a lemma

Tag 05NR in the Stacks Project.

Declarations registered for the tag:

HasCardinalLT.isCardinalPresentable registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch19.lean, line 22 (StacksFrontier).

Tag 05NS, a definition

Tag 05NS in the Stacks Project.

Stacks.Injectives.IsSmallWithRespectTo, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/SmallObject.lean, line 55.

An object A is α-small with respect to I if Hom(A, -) preserves the colimit of every α-indexed system all of whose transition morphisms belong to I.

abbrev IsSmallWithRespectTo {C : Type u} [Category.{v} C] (A : C)
    (I : MorphismProperty C) (α : Ordinal.{w}) : Prop

Tag 05NT, a proposition

Tag 05NT in the Stacks Project.

Stacks.Injectives.isSmallWithRespectTo_monomorphisms_of_mk_submodule_lt_cof, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/SmallWithRespectToInjections.lean, line 109.

Stacks 05NT. Let R be a ring, let M be an R-module and let κ be the cardinality of the set of submodules of M. If α is an ordinal whose cofinality is bigger than κ, then M is α-small with respect to injections, i.e. for every system (B_β)_{β ∈ α} of R-modules with injective transition maps the canonical map colim_β Hom(M, B_β) ⟶ Hom(M, colim_β B_β) is bijective.

theorem isSmallWithRespectTo_monomorphisms_of_mk_submodule_lt_cof
    {R : Type u} [Ring R] (M : ModuleCat.{u} R) (α : Ordinal.{u})
    (hα : Cardinal.mk (Submodule R M) < α.cof) :
    IsSmallWithRespectTo M (MorphismProperty.monomorphisms (ModuleCat.{u} R)) α

Tag 05NU, a lemma

Tag 05NU in the Stacks Project.

Declarations registered for the tag:

Module.Baer.iff_injective registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch19.lean, line 27 (StacksFrontier).

Tag 05NV, an equation

Tag 05NV in the Stacks Project.

baerE_lof, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/BaerPushout.lean, line 387. The attribute's comment: “the top horizontal arrow”.

The top horizontal arrow ⨁_{(a, φ)} a → M of the defining square of 𝐌(M), read on the summands: the element x of the ideal a, placed in the summand indexed by the pair (a, φ), is sent to φ x ∈ M. The direct sum over the sigma type I(M) = Σ a, Hom(a, M) realizes the iterated coproduct ⨁_a ⨁_{φ ∈ Hom(a, M)}.

theorem baerE_lof (a : Ideal R) (φ : a →ₗ[R] M) (x : a) :
    baerE R M (DirectSum.lof R (BaerIndex R M) (fun i => (i.1 : Type u)) ⟨a, φ⟩ x) = φ x

baerD_lof, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/BaerPushout.lean, line 397. The attribute's comment: “the left vertical arrow”.

The left vertical arrow ⨁_{(a, φ)} a → ⨁_{(a, φ)} R of the defining square of 𝐌(M), read on the summands: the element x of the ideal a, placed in the summand indexed by the pair (a, φ), is sent to the same element x, now viewed in the copy of R indexed by that same pair (a, φ).

theorem baerD_lof (a : Ideal R) (φ : a →ₗ[R] M) (x : a) :
    baerD R M (DirectSum.lof R (BaerIndex R M) (fun i => (i.1 : Type u)) ⟨a, φ⟩ x)
      = DirectSum.lof R (BaerIndex R M) (fun _ => R) ⟨a, φ⟩ (x : R)

baer_pushout_universal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/BaerPushout.lean, line 462. The attribute's comment: “the pushout defining 𝐌(M)”.

The module 𝐌(M), together with the canonical maps u_M : M → 𝐌(M) and v_M : T(M) → 𝐌(M), is the pushout of M ← S(M) → T(M): for every R-module N and every pair of maps f : M → N, g : T(M) → N making the outer square commute, there is a unique k : 𝐌(M) → N with k ∘ u_M = f and k ∘ v_M = g. Together with baer_pushout_square, baerE_lof and baerD_lof this says that the square
⨁_{(a, φ)} a  --e_M-->  M
     |                   |
    d_M                 u_M
     v                   v
⨁_{(a, φ)} R  --v_M-->  𝐌(M)
is the pushout square defining 𝐌(M).

theorem baer_pushout_universal (f : M →ₗ[R] N) (g : BaerT R M →ₗ[R] N)
    (h : f.comp (baerE R M) = g.comp (baerD R M)) :
    ∃! k : BaerM R M →ₗ[R] N, k.comp (baerUMap R M) = f ∧ k.comp (baerV R M) = g

Tag 05NW, a lemma

Tag 05NW in the Stacks Project.

baer_functorial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/BaerPushout.lean, line 287. The attribute's comment: “(1)”.

Statement 1 (Functoriality). The construction M ↦ (u_M : M → 𝐌(M)) is functorial: there is an assignment MMap on R-module morphisms χ : M → N, giving a map MMap χ : 𝐌(M) → 𝐌(N), such that

MMap id = id (identities are preserved);

MMap (χ' ∘ χ) = MMap χ' ∘ MMap χ (composition is preserved);

the maps u_M are a natural transformation 𝟭 ⟹ 𝐌, i.e. MMap χ ∘ u_M = u_N ∘ χ for every χ : M → N.

Here the morphism action MMap is quantified existentially, modelling "there is a functor 𝐌 with u a natural transformation from the identity to 𝐌".

theorem baer_functorial :
    ∃ MMap : ∀ {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N],
        (M →ₗ[R] N) → (BaerM R M →ₗ[R] BaerM R N),
      (∀ (M : Type u) [AddCommGroup M] [Module R M],
          MMap (LinearMap.id : M →ₗ[R] M) = LinearMap.id) ∧
      (∀ {M N P : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
          [AddCommGroup P] [Module R P] (χ : M →ₗ[R] N) (χ' : N →ₗ[R] P),
          MMap (χ'.comp χ) = (MMap χ').comp (MMap χ)) ∧
      (∀ {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
          (χ : M →ₗ[R] N),
          (MMap χ).comp (baerUMap R M) = (baerUMap R N).comp χ)

baer_uMap_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/BaerPushout.lean, line 344. The attribute's comment: “(2)”.

Statement 2 (Injectivity). The canonical map u_M : M → 𝐌(M) is injective.

theorem baer_uMap_injective : Function.Injective (baerUMap R M)

baer_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/BaerPushout.lean, line 366. The attribute's comment: “(3)”.

Statement 3 (Extension property). For every ideal a and R-module map φ : a → M, there is an R-module map φ' : R → 𝐌(M) with φ' |_a = u_M ∘ φ, i.e. φ' (a) = u_M (φ a) for all a ∈ a.

theorem baer_extension (a : Ideal R) (φ : a →ₗ[R] M) :
    ∃ φ' : R →ₗ[R] BaerM R M,
      φ'.comp a.subtype = (baerUMap R M).comp φ

Tag 05NX, a theorem

Tag 05NX in the Stacks Project.

Stacks.Injectives.baerIterateFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/BaerEmbedding.lean, line 131. The attribute's comment: “the functorial transfinite construction”.

M_α, functorially in M: the top stage of the transfinite iteration of the Baer construction through the ordinal α.

noncomputable def baerIterateFunctor (R : Type u) [CommRing R]
    (α : Ordinal.{u}) : ModuleCat.{u} R ⥤ ModuleCat.{u} R

Stacks.Injectives.baerIterateEmbedding, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/BaerEmbedding.lean, line 137. The attribute's comment: “the natural map to the iterate”.

The canonical natural map M ⟶ M_α.

noncomputable def baerIterateEmbedding (R : Type u) [CommRing R]
    (α : Ordinal.{u}) : 𝟭 (ModuleCat.{u} R) ⟶ baerIterateFunctor R α

Stacks.Injectives.baerIterate_injective_of_cofinality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/BaerEmbedding.lean, line 331. The attribute's comment: “injectivity of the target”.

If the cofinality of α exceeds the cardinality of the set of ideals of R, then the top stage M_α of the transfinite Baer iteration is an injective R-module.

theorem baerIterate_injective_of_cofinality
    (R : Type u) [CommRing R] (α : Ordinal.{u})
    (hα : Cardinal.mk (Ideal R) < α.cof) (M : ModuleCat.{u} R) :
    Injective ((baerIterateFunctor R α).obj M)

Stacks.Injectives.mono_baerIterateEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/BaerEmbedding.lean, line 360. The attribute's comment: “the natural embedding”.

The canonical natural map from a module to any transfinite Baer iterate is a monomorphism. Together with baerIterate_injective_of_cofinality, its components give functorial injective embeddings.

theorem mono_baerIterateEmbedding
    (R : Type u) [CommRing R] (α : Ordinal.{u}) (M : ModuleCat.{u} R) :
    Mono ((baerIterateEmbedding R α).app M)

Sources

LeanCategoryTheory.Limits.colimit.post · HasCardinalLT.isCardinalPresentable · Stacks.Injectives.IsSmallWithRespectTo · Stacks.Injectives.isSmallWithRespectTo_monomorphisms_of_mk_submodule_lt_cof · Module.Baer.iff_injective · baerE_lof · baerD_lof · baer_pushout_universal

Section19.3 G-modules #

Section 19.3 of the Stacks Project, Tag 04JE. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04JF, a lemma

Tag 04JF in the Stacks Project.

Stacks.Injectives.continuousModule_hasFunctorialInjectiveEmbeddings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Module/ContinuousGroupModules.lean, line 752.

Stacks Project, Tag 04JF. The category of R-modules with continuous G-action has functorial injective embeddings. In particular, taking R = ℤ gives this result for discrete G-modules.

theorem continuousModule_hasFunctorialInjectiveEmbeddings
    (R : Type u) [Ring R]
    (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    HasFunctorialInjectiveEmbeddings (ContinuousModule.{u, v, max u v w} R G)

Sources

LeanStacks.Injectives.continuousModule_hasFunctorialInjectiveEmbeddings

Section19.4 Abelian sheaves on a space #

Section 19.4 of the Stacks Project, Tag 01DF. 1 tag here is carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01DG, a lemma

Tag 01DG in the Stacks Project.

Stacks.Cohomology.abelianSheaf_enoughInjectives, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/GlobalSectionsDerived.lean, line 67. The attribute's comment: “enough injectives”. References: SGA 4 II (6.9), “site of opens of a space”; SGA 4 V (0.1.1), “sheaves on a space”.

The category of abelian sheaves on a topological space has enough injectives.

instance abelianSheaf_enoughInjectives (X : TopCat.{u}) :
    EnoughInjectives (TopCat.Sheaf AddCommGrpCat.{max u v} X)

Stacks.Cohomology.abelianSheaf_hasFunctorialInjectiveEmbeddings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/GlobalSectionsDerived.lean, line 75. The attribute's comment: “functorial injective embeddings”. References: SGA 4 II (6.9), “site of opens of a space”; SGA 4 V (0.1.1), “sheaves on a space”.

Abelian sheaves on a topological space admit functorial injective embeddings.

theorem abelianSheaf_hasFunctorialInjectiveEmbeddings (X : TopCat.{u}) :
    HasFunctorialInjectiveEmbeddings (TopCat.Sheaf AddCommGrpCat.{max u v} X)

Stacks.Injectives.abelianSheaf_enoughInjectives, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/AbelianSheavesOnSpace.lean, line 62. The attribute's comment: “enough injectives”.

Stacks 01DG. The category of abelian sheaves on a topological space has enough injectives.

instance abelianSheaf_enoughInjectives (X : TopCat.{u}) :
    EnoughInjectives (TopCat.Sheaf AddCommGrpCat.{max u v} X)

Stacks.Injectives.abelianSheaf_hasFunctorialInjectiveEmbeddings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/AbelianSheavesOnSpace.lean, line 78. The attribute's comment: “functorial injective embeddings”.

Stacks 01DG. Abelian sheaves on a topological space admit functorial injective embeddings.

theorem abelianSheaf_hasFunctorialInjectiveEmbeddings (X : TopCat.{u}) :
    HasFunctorialInjectiveEmbeddings (TopCat.Sheaf AddCommGrpCat.{max u v} X)

Stacks.Cohomology.LerayLowDegree.abelianSheafEnoughInjectives, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Leray/LowDegreeSequence.lean, line 87. The attribute's comment: “enough injectives”. References: SGA 4 II (6.9), “site of opens of a space”; SGA 4 V (0.1.1), “sheaves on a space”.

Abelian sheaves have enough injectives ([Stacks, Tag 01DG]), in any coefficient universe containing that of the space. The site Opens X is u-small, hence essentially small in the larger universe, and AddCommGrpCat is a Grothendieck abelian category there, so the sheaf category is Grothendieck abelian and therefore has enough injectives.

instance abelianSheafEnoughInjectives (X : TopCat.{u}) :
    EnoughInjectives (Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{max u v})

Sources

LeanStacks.Cohomology.abelianSheaf_enoughInjectives · Stacks.Cohomology.abelianSheaf_hasFunctorialInjectiveEmbeddings · Stacks.Injectives.abelianSheaf_enoughInjectives · Stacks.Injectives.abelianSheaf_hasFunctorialInjectiveEmbeddings · Stacks.Cohomology.LerayLowDegree.abelianSheafEnoughInjectives

Section19.5 Sheaves of modules on a ringed space #

Section 19.5 of the Stacks Project, Tag 01DH. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01DI, a lemma

Tag 01DI in the Stacks Project.

Stacks.Injectives.sheafOfModules_hasFunctorialInjectiveEmbeddings_of_space, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/ModulesOnRingedSpace.lean, line 39. The attribute's comment: “functorial injective embeddings”.

The category of sheaves of modules over a sheaf of rings on a topological space has functorial injective embeddings.

theorem sheafOfModules_hasFunctorialInjectiveEmbeddings_of_space :
    HasFunctorialInjectiveEmbeddings (SheafOfModules.{u} O)

Stacks.Injectives.sheafOfModules_enoughInjectives_of_space, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/ModulesOnRingedSpace.lean, line 46. The attribute's comment: “enough injectives”.

The category of sheaves of modules over a sheaf of rings on a topological space has enough injectives.

theorem sheafOfModules_enoughInjectives_of_space : EnoughInjectives (SheafOfModules.{u} O)

Sources

LeanStacks.Injectives.sheafOfModules_hasFunctorialInjectiveEmbeddings_of_space · Stacks.Injectives.sheafOfModules_enoughInjectives_of_space

Section19.6 Abelian presheaves on a category #

Section 19.6 of the Stacks Project, Tag 01DJ. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01DK, a proposition

Tag 01DK in the Stacks Project.

Stacks.Injectives.presheaf_hasFunctorialInjectiveEmbeddings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/AbelianPresheaves.lean, line 40.

The category of abelian presheaves on a category has functorial injective embeddings.

theorem presheaf_hasFunctorialInjectiveEmbeddings (C : Type u) [Category.{v} C] :
    HasFunctorialInjectiveEmbeddings (Cᵒᵖ ⥤ AddCommGrpCat.{max u v t})

Sources

LeanStacks.Injectives.presheaf_hasFunctorialInjectiveEmbeddings

Section19.7 Abelian Sheaves on a site #

Section 19.7 of the Stacks Project, Tag 01DL. 5 tags here are carried by 5 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01DM, a lemma

Tag 01DM in the Stacks Project.

Stacks.Injectives.SheafificationTowerFactorization.exists_extension_towerIota_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/SheafificationTowerFactorization.lean, line 428.

Let F be an abelian sheaf and α ≤ β a non-maximal stage of the tower, so that α + 1 ≤ β as well. Let ι : G₁ ⟶ G₂ be an injective (i.e. monomorphic) map of abelian sheaves and let f : G₁ ⟶ J_α(F) be a morphism. Then there is a morphism g : G₂ ⟶ J_{α+1}(F) making the square with the transition map ι_{α,α+1} : J_α(F) ⟶ J_{α+1}(F) commute, i.e. ι ≫ g = f ≫ ι_{α,α+1}.

theorem exists_extension_towerIota_succ (β : Ordinal.{u}) (α : Set.Iic β) (hα : ¬ IsMax α)
    (F : AbSheaf J) {G₁ G₂ : AbSheaf J} (ι : G₁ ⟶ G₂) [Mono ι]
    (f : G₁ ⟶ towerObj J β α F) :
    ∃ g : G₂ ⟶ towerObj J β (Order.succ α) F,
      ι ≫ g = f ≫ towerIota J β (Order.le_succ α) F

Tag 01DN, a lemma

Tag 01DN in the Stacks Project.

Stacks.Injectives.SheafificationTowerFactorization.exists_ordinal_towerFactorsThrough, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/SheafificationTowerFactorization.lean, line 835.

Let {G i}_{i : I} be a set of abelian sheaves on C. There is an ordinal β, depending only on J and the family {G i}, such that for every abelian sheaf F, every index i, and every morphism φ : G i → J_β(F), there is an ordinal α < β such that φ factors through J_α(F).

theorem exists_ordinal_towerFactorsThrough {I : Type u} (G : I → AbSheaf J) :
    ∃ β : Ordinal.{u},
      ∀ (F : AbSheaf J) (i : I) (φ : G i ⟶ towerTop J β F),
        ∃ (α : Set.Iic β) (h : (α : Ordinal) < β),
          TowerFactorsThrough J β
            (le_of_lt (show α < (⟨β, le_refl β⟩ : Set.Iic β) from h)) F (G i) φ

Tag 05NY, an equation

Tag 05NY in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Sheaf.freeYonedaHomEquiv registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Adjunction.lean, line 33 (StacksCore): “Mor_{Ab(C)}(Z_X^#, G) = G(X)”.

Tag 01DO, a lemma

Tag 01DO in the Stacks Project.

Stacks.Injectives.BaerCriterion.injective_of_extends_freeAbSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/BaerCriterion.lean, line 557.

Let 𝒥 be a sheaf of abelian groups such that for every object X of C, every abelian subsheaf S ⊆ Z_X^#, and every morphism φ : S → 𝒥, there exists a morphism ψ : Z_X^# → 𝒥 extending φ. Then 𝒥 is an injective sheaf of abelian groups.

theorem injective_of_extends_freeAbSheaf
    (𝒥 : Sheaf J Ab.{u})
    (H : ∀ (X : C) (S : AbelianSubsheaf J (freeAbSheaf J X)) (φ : S.sheaf ⟶ 𝒥),
      ∃ ψ : freeAbSheaf J X ⟶ 𝒥, Extends J S φ ψ) :
    IsInjectiveSheaf J 𝒥

Tag 01DP, a theorem

Tag 01DP in the Stacks Project.

CategoryTheory.Sheaf.hasFunctorialInjectiveEmbeddings_addCommGrpCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/FunctorialInjectiveEmbeddings.lean, line 111. The attribute's comment: “functorial injective embeddings”. References: SGA 4½ Arcata (1.6.3), “enough injectives”; SGA 4 V (0.1.1), “sheaves on a site”.

Stacks Project, Tag 01DP. The category of sheaves of abelian groups on a site has functorial injective embeddings in the sense of [Stacks, Tag 0139].

theorem hasFunctorialInjectiveEmbeddings_addCommGrpCat [HasSheafify J AddCommGrpCat.{w}]
    [EssentiallySmall.{w} C] :
    HasFunctorialInjectiveEmbeddings (Sheaf J AddCommGrpCat.{w})

CategoryTheory.Sheaf.enoughInjectives_addCommGrpCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/FunctorialInjectiveEmbeddings.lean, line 126. The attribute's comment: “enough injectives”. References: SGA 4½ Arcata (1.6.3), “enough injectives”; SGA 4 V (0.1.1), “sheaves on a site”; SGA 3 I (3.1.2), “special case”; SGA 4 I (7.13), “special case”; SGA 4 V (0.2.1), “special case”; SGA 4 V (2.5.2), “special case”.

Stacks Project, Tag 01DP. The category of sheaves of abelian groups on a site has enough injectives. This is deduced from the functorial statement hasFunctorialInjectiveEmbeddings_addCommGrpCat, as in the source.

theorem enoughInjectives_addCommGrpCat [HasSheafify J AddCommGrpCat.{w}]
    [EssentiallySmall.{w} C] :
    EnoughInjectives (Sheaf J AddCommGrpCat.{w})

Sources

LeanStacks.Injectives.SheafificationTowerFactorization.exists_extension_towerIota_succ · Stacks.Injectives.SheafificationTowerFactorization.exists_ordinal_towerFactorsThrough · CategoryTheory.Sheaf.freeYonedaHomEquiv · Stacks.Injectives.BaerCriterion.injective_of_extends_freeAbSheaf · CategoryTheory.Sheaf.hasFunctorialInjectiveEmbeddings_addCommGrpCat · CategoryTheory.Sheaf.enoughInjectives_addCommGrpCat

Section19.8 Modules on a ringed site #

Section 19.8 of the Stacks Project, Tag 01DQ. 5 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01DR, a lemma

Tag 01DR in the Stacks Project.

Stacks.Duality.shortExact_internalHomMapLeft_of_injective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Sweep/NormalSheafAsSheafExt.lean, line 382. The attribute's comment: “for sheaves of modules on a ringed space, against the sequence of a sheaf of ideals; the library's Stacks.Injectives.AbelianDual.dualFunctor_shortExact_of_injective is the statement for the abelian-sheaf internal Hom against an injective abelian sheaf instead”.

[Stacks, Tag 01DR] for sheaves of modules, on the ideal sequence. For an injective sheaf of 𝒪_Y-modules K the internal Hom 𝓗om_{𝒪_Y}(-, K) carries 0 ⟶ ℐ ⟶ 𝒪_Y ⟶ 𝒪_X ⟶ 0 to a short exact sequence

0 ⟶ 𝓗om(𝒪_X, K) ⟶ 𝓗om(𝒪_Y, K) ⟶ 𝓗om(ℐ, K) ⟶ 0.

Exactness at the middle term and the left-hand monomorphism are the left exactness of internal Hom in the first variable, [Stacks, Tag 0GMY] part (1); the right-hand epimorphism is where the injectivity of K is spent, through epi_internalHomMapLeft_ι.

public lemma shortExact_internalHomMapLeft_of_injective
    (K : SheafOfModules.{u}
      (SheafOfModules.Tensor.ringSheaf Y.sheaf)) [Injective K] :
    (ShortComplex.mk
      ((internalHomMapLeftNatTrans Y.sheaf (cokernel.π I.ι)).app K)
      ((internalHomMapLeftNatTrans Y.sheaf I.ι).app K)
      (by
        rw [← NatTrans.comp_app, internalHomMapLeftNatTrans_comp, cokernel.condition,
          internalHomMapLeftNatTrans_zero]
        rfl)).ShortExact

internalHom_exact_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/InternalHomExact.lean, line 897. References: SGA 4 V (4.10), “1), A = Z”.

Statement 1 (Stacks Tag 01DR, abelian-sheaf level). Let J be an injective abelian sheaf on a site (C, K). Then the contravariant internal-Hom functor ℋom(-, J) is exact: for every short exact sequence 0 → F' → F → F'' → 0 of abelian sheaves, encoded as a short complex S with S.ShortExact, the contravariantly induced short complex (ℋom(-, J)) ∘ Sᵒᵖ, i.e. 0 → ℋom(F'', J) → ℋom(F, J) → ℋom(F', J) → 0, is again short exact.

theorem internalHom_exact_of_injective (K : GrothendieckTopology C) [HasSheafify K Ab.{max u v}]
    (J : Sheaf K Ab.{max u v}) [Injective J]
    (S : ShortComplex (Sheaf K Ab.{max u v})) (hS : S.ShortExact) :
    (S.op.map (internalHomFunctor K J)).ShortExact

Stacks.Injectives.AbelianDual.dualFunctor_shortExact_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/InternalHomExact.lean, line 1248. The attribute's comment: “module-valued exactness”.

Stacks 01DR (Lemma 19.8.1), the statement itself. The functor F ↦ F^∨, with its natural O-module structure, is exact when J is an injective abelian sheaf: it carries a short exact sequence of sheaves of O-modules to a short exact sequence of sheaves of O-modules.

The source's proof is "this because J is an injective abelian sheaf", and that is exactly how this runs: exactness of the forgetful functor to abelian sheaves (Stacks 03DA) reduces the claim to internalHom_exact_of_injective above, which is where the injectivity of J is spent.

theorem dualFunctor_shortExact_of_injective
    [HasSheafify K Ab.{max u v}] [K.WEqualsLocallyBijective Ab.{max u v}]
    (O : Sheaf K CommRingCat.{max u v}) (J : Sheaf K Ab.{max u v}) [Injective J]
    (S : ShortComplex (SheafOfModules.{max u v} (underlyingRingSheaf O)))
    (hS : S.ShortExact) :
    letI := (dualFunctorData O J).preservesZero
    (S.op.map (dualFunctor O J)).ShortExact

Tag 01DS, a lemma

Tag 01DS in the Stacks Project.

Stacks.Injectives.DualEvaluation.evaluation_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/DualEvaluationMono.lean, line 330.

For every sheaf of O-modules F on a ringed site the evaluation map ev : F ⟶ (F^∨)^∨ into the double dual is a monomorphism, the dual being taken against the dualizing sheaf of the site.

theorem evaluation_mono (F : SheafOfModules.{u} (underlyingRingSheaf O)) :
    Mono (ev O (dualizingSheafOfRingedSite O) F)

Tag 01DT, a lemma

Tag 01DT in the Stacks Project.

Stacks.Injectives.DualEvaluation.injective_standardModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/StandardInjectiveModule.lean, line 221.

For every sheaf F of O-modules the standard module J(F) = Fr(F^∨)^∨ is an injective O-module.

theorem injective_standardModule (F : SheafOfModules.{u} (underlyingRingSheaf O)) :
    Injective (standardModule O Jab F)

Tag 01DU, a theorem

Tag 01DU in the Stacks Project.

Stacks.Injectives.sheafOfModules_hasFunctorialInjectiveEmbeddings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/ModulesOnRingedSite.lean, line 111.

Stacks Project, Tag 01DU. The category of sheaves of modules over a sheaf of rings on a site has functorial injective embeddings (and consequently enough injectives).

theorem sheafOfModules_hasFunctorialInjectiveEmbeddings
    {C : Type u} [SmallCategory C] (J : GrothendieckTopology C)
    (O : Sheaf J RingCat.{u}) :
    HasFunctorialInjectiveEmbeddings (SheafOfModules.{u} O)

Declarations registered for the tag:

CategoryTheory.IsGrothendieckAbelian.enoughInjectives registered with add_to_stacks in StacksFrontier/Homology/Injectives/Sheaf/ModulesOnRingedSite.lean, line 56 (StacksFrontier): “enough injectives”. References: SGA 3 I (5.3.1.1), “more general”; SGA 4 I (7.13); SGA 4 V (0.1.1); SGA 4 V (0.2.1); SGA 4 V (2.5.2), “more general”.

Tag 01DV, a proposition

Tag 01DV in the Stacks Project.

Stacks.Injectives.presheafOfModules_hasFunctorialInjectiveEmbeddings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/PresheavesOfModules.lean, line 198. References: SGA 3 I (3.1.2), “more general”.

Stacks Project, Tag 01DV. The category of presheaves of modules over a presheaf of rings has functorial injective embeddings (and consequently enough injectives).

theorem presheafOfModules_hasFunctorialInjectiveEmbeddings
    (C : Type u) [Category.{v} C] (R : Cᵒᵖ ⥤ RingCat.{w}) :
    HasFunctorialInjectiveEmbeddings (PresheafOfModules.{max u v w} R)

Sources

LeanStacks.Duality.shortExact_internalHomMapLeft_of_injective · internalHom_exact_of_injective · Stacks.Injectives.AbelianDual.dualFunctor_shortExact_of_injective · Stacks.Injectives.DualEvaluation.evaluation_mono · Stacks.Injectives.DualEvaluation.injective_standardModule · Stacks.Injectives.sheafOfModules_hasFunctorialInjectiveEmbeddings · CategoryTheory.IsGrothendieckAbelian.enoughInjectives · Stacks.Injectives.presheafOfModules_hasFunctorialInjectiveEmbeddings

Section19.9 Embedding abelian categories #

Section 19.9 of the Stacks Project, Tag 05PL. 5 tags here are carried by 27 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05PM, a lemma

Tag 05PM in the Stacks Project.

Stacks.Sites.EpiPretopology.exists_pretopology_epiCoverings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Pretopology/AbelianEpiCoverings.lean, line 111.

Statement 1 (Stacks Tag 05PM). The assignment U ↦ EpiCoverings U satisfies the three pretopology axioms and hence determines a pretopology on the abelian category 𝒜, with coverings given exactly by EpiCoverings.

theorem exists_pretopology_epiCoverings :
    ∃ K : Pretopology 𝒜, ∀ U : 𝒜, K.coverings U = EpiCoverings 𝒜 U

Tag 05PN, a lemma

Tag 05PN in the Stacks Project.

Stacks.Injectives.preadditiveYoneda_obj_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/EpiTopologyEmbedding.lean, line 101. The attribute's comment: “the embedding”.

Additive representable presheaves on an abelian category are sheaves for the topology generated by epimorphism covers.

theorem preadditiveYoneda_obj_isSheaf (X : 𝒜) :
    Presheaf.IsSheaf (epiPretopology 𝒜).toGrothendieck (preadditiveYoneda.obj X)

Stacks.Injectives.yonedaSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/EpiTopologyEmbedding.lean, line 161. The attribute's comment: “the embedding”.

The Yoneda functor from an abelian category to abelian sheaves for its epimorphism topology. Its underlying presheaf functor is definitionally the additive Yoneda functor.

noncomputable def yonedaSheaf :
    𝒜 ⥤ Sheaf (epiPretopology 𝒜).toGrothendieck AddCommGrpCat.{v}

Stacks.Injectives.yonedaSheaf_full, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/EpiTopologyEmbedding.lean, line 167. The attribute's comment: “the embedding”.

The Yoneda functor into abelian sheaves is full.

theorem yonedaSheaf_full : (yonedaSheaf 𝒜).Full

Stacks.Injectives.yonedaSheaf_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/EpiTopologyEmbedding.lean, line 173. The attribute's comment: “the embedding”.

The Yoneda functor into abelian sheaves is faithful.

theorem yonedaSheaf_faithful : (yonedaSheaf 𝒜).Faithful

Stacks.Injectives.yonedaSheaf_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/EpiTopologyEmbedding.lean, line 179. The attribute's comment: “the embedding”.

The Yoneda functor into abelian sheaves preserves finite limits.

theorem yonedaSheaf_preservesFiniteLimits : PreservesFiniteLimits (yonedaSheaf 𝒜)

Stacks.Injectives.yonedaSheaf_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/EpiTopologyEmbedding.lean, line 191. The attribute's comment: “the embedding”.

The Yoneda functor into abelian sheaves preserves finite colimits.

theorem yonedaSheaf_preservesFiniteColimits : PreservesFiniteColimits (yonedaSheaf 𝒜)

Stacks.Injectives.epiPretopology_hasEnoughPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/EpiTopologyEmbedding.lean, line 232. The attribute's comment: “enough points”.

The site on an abelian category whose covers are singleton epimorphisms has enough points.

theorem epiPretopology_hasEnoughPoints :
    GrothendieckTopology.HasConservativeFamily.{max u v}
      (epiPretopology 𝒜).toGrothendieck

Tag 05PP, a remark

Tag 05PP in the Stacks Project.

Stacks.Injectives.preservesFiniteLimits_sheafSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/DiagramChasing.lean, line 69. The attribute's comment: “diagram chasing: sections”.

Finite limits of abelian sheaves are computed sectionwise: taking sections over a fixed object is left exact.

theorem preservesFiniteLimits_sheafSections (U : Cᵒᵖ) :
    PreservesFiniteLimits ((sheafSections J AddCommGrpCat.{max u v}).obj U)

Stacks.Injectives.isLimit_of_forall_isLimit_sheafSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/DiagramChasing.lean, line 88. The attribute's comment: “diagram chasing: sections”.

A cone of abelian sheaves which becomes a limit cone after taking sections over every object is a limit cone.

noncomputable def isLimit_of_forall_isLimit_sheafSections {T : Type*} [Category T]
    {K : T ⥤ Sheaf J AddCommGrpCat.{max u v}} (c : Cone K)
    (h : ∀ U : Cᵒᵖ,
      IsLimit (((sheafSections J AddCommGrpCat.{max u v}).obj U).mapCone c)) :
    IsLimit c

Stacks.Injectives.mono_iff_forall_injective_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/DiagramChasing.lean, line 100. The attribute's comment: “diagram chasing: sections”.

A morphism of abelian sheaves is a monomorphism if and only if it is injective on sections over every object.

theorem mono_iff_forall_injective_app {F G : Sheaf J AddCommGrpCat.{max u v}} (f : F ⟶ G) :
    Mono f ↔ ∀ U : Cᵒᵖ, Function.Injective (f.hom.app U)

Stacks.Injectives.epi_iff_forall_exists_local_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/DiagramChasing.lean, line 109. The attribute's comment: “diagram chasing: sections”.

A morphism of abelian sheaves f : F ⟶ G is an epimorphism if and only if every section of G over an object U lifts along f on the arrows of some covering sieve of U.

theorem epi_iff_forall_exists_local_lift {F G : Sheaf J AddCommGrpCat.{max u v}} (f : F ⟶ G) :
    Epi f ↔ ∀ (U : C) (s : ToType (G.obj.obj (op U))),
      ∃ R : Sieve U, R ∈ J U ∧ ∀ ⦃V : C⦄ (g : V ⟶ U), R g →
        ∃ t : ToType (F.obj.obj (op V)), f.hom.app (op V) t = G.obj.map g.op s

Stacks.Injectives.exact_of_forall_exists_local_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/DiagramChasing.lean, line 129. The attribute's comment: “diagram chasing: sections”. References: SGA 4½ Arcata (1.6.3), “partial”.

A short complex of abelian sheaves is exact as soon as every section of its middle term annihilated by the second map lifts along the first map on the arrows of some covering sieve.

theorem exact_of_forall_exists_local_lift {S : ShortComplex (Sheaf J AddCommGrpCat.{max u v})}
    (h : ∀ (U : C) (a : ToType (S.X₂.obj.obj (op U))), S.g.hom.app (op U) a = 0 →
      ∃ R : Sieve U, R ∈ J U ∧ ∀ ⦃V : C⦄ (φ : V ⟶ U), R φ →
        ∃ b : ToType (S.X₁.obj.obj (op V)),
          S.f.hom.app (op V) b = S.X₂.obj.map φ.op a) :
    S.Exact

Stacks.Injectives.exact_iff_forall_sheafFiber_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/DiagramChasing.lean, line 165. The attribute's comment: “diagram chasing: stalks”.

Let {p_i} be a conservative family of points of a site. A short complex of abelian sheaves is exact if and only if the short complex of stalks at p_i is exact for every i.

theorem exact_iff_forall_sheafFiber_exact
    {P : ObjectProperty (GrothendieckTopology.Point.{max u v} J)}
    (hP : P.IsConservativeFamilyOfPoints)
    (S : ShortComplex (Sheaf J AddCommGrpCat.{max u v})) :
    S.Exact ↔ ∀ Φ : P.FullSubcategory,
      (S.map (Φ.obj.sheafFiber (A := AddCommGrpCat.{max u v}))).Exact

Stacks.Injectives.exists_conservativeFamily_exact_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/DiagramChasing.lean, line 182. The attribute's comment: “diagram chasing: stalks”.

On a site which has a conservative family of points (CategoryTheory.GrothendieckTopology.HasConservativeFamily) there is a conservative family of points on whose stalks the exactness of short complexes of abelian sheaves can be tested.

theorem exists_conservativeFamily_exact_iff (J : GrothendieckTopology C)
    (h : GrothendieckTopology.HasConservativeFamily.{max u v} J) :
    ∃ P : ObjectProperty (GrothendieckTopology.Point.{max u v} J),
      P.IsConservativeFamilyOfPoints ∧
      ∀ S : ShortComplex (Sheaf J AddCommGrpCat.{max u v}),
        (S.Exact ↔ ∀ Φ : P.FullSubcategory,
          (S.map (Φ.obj.sheafFiber (A := AddCommGrpCat.{max u v}))).Exact)

Tag 05PQ, a remark

Tag 05PQ in the Stacks Project.

exists_small_abelian_full_subcategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/SmallSubcategory/AbelianOnly.lean, line 277. The attribute's comment: “the small abelian subcategory”.

Stacks 05PQ, first assertion. Let 𝒜 be an abelian category — in particular one whose objects form a class — and let A : S → 𝒜 be a family of objects indexed by a set S. There is an object property P whose full subcategory 𝒜' = P.FullSubcategory has a set of objects, contains every A s, and admits an abelian structure for which the inclusion P.ι is additive and exact.

Nothing beyond Abelian 𝒜 is assumed; compare exists_small_abelian_subcategory_with_enough_injectives (Stacks 0010), which additionally assumes EnoughInjectives 𝒜 and produces a subcategory with enough injectives.

theorem exists_small_abelian_full_subcategory (A : S → 𝒜) :
    ∃ (P : ObjectProperty 𝒜),
      Small.{max v w} P.FullSubcategory ∧
      (∀ s, P (A s)) ∧
      ∃ (_ : Abelian P.FullSubcategory),
        P.ι.Additive ∧
        Nonempty (PreservesFiniteLimits P.ι) ∧
        Nonempty (PreservesFiniteColimits P.ι)

Stacks.Injectives.exists_small_abelian_subcategory_yonedaSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/BigCategoryDiagramChase.lean, line 71.

Stacks 05PQ. Let 𝒜 be an abelian category — in particular one whose objects form a class, so that Tag 05PN does not apply to 𝒜 itself — and let A : S → 𝒜 be a family of objects indexed by a set S. There is an object property P such that the full subcategory 𝒜' = P.FullSubcategory has a set of objects, contains every A s, and admits an abelian structure for which:

the inclusion P.ι : 𝒜' ⥤ 𝒜 is additive and exact, and

there is a full, faithful and exact functor from 𝒜' to the category of abelian sheaves on the epimorphism site of 𝒜', a site which has a conservative family of points.

The second item is Tag 05PN applied to 𝒜', and together with the first it is what lets a result in 𝒜 whose proof is a diagram chase be proved by chasing in abelian sheaves.

theorem exists_small_abelian_subcategory_yonedaSheaf (A : S → 𝒜) :
    ∃ (P : ObjectProperty 𝒜),
      Small.{max v w} P.FullSubcategory ∧
      (∀ s, P (A s)) ∧
      ∃ (_ : Abelian P.FullSubcategory),
        P.ι.Additive ∧
        Nonempty (PreservesFiniteLimits P.ι) ∧
        Nonempty (PreservesFiniteColimits P.ι) ∧
        ∃ F : P.FullSubcategory ⥤
            Sheaf (epiPretopology P.FullSubcategory).toGrothendieck AddCommGrpCat.{v},
          F.Full ∧ F.Faithful ∧
            Nonempty (PreservesFiniteLimits F) ∧ Nonempty (PreservesFiniteColimits F) ∧
            GrothendieckTopology.HasConservativeFamily.{max u v}
              (epiPretopology P.FullSubcategory).toGrothendieck

Tag 05PR, a remark

Tag 05PR in the Stacks Project.

Stacks.Injectives.oppEpiSheaf_enoughInjectives, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/FreydMitchell.lean, line 94. The attribute's comment: “Ab(C) has enough injectives”.

Stacks 05PR, first clause. Ab(C) has enough injectives.

theorem oppEpiSheaf_enoughInjectives : EnoughInjectives (oppEpiSheaf A)

Stacks.Injectives.oppEpiSheaf_exists_injective_coseparator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/FreydMitchell.lean, line 100. The attribute's comment: “Ab(C) has a cogenerator”.

Stacks 05PR, second clause: Ab(C) has a cogenerator. The source omits the details; here it comes from Ab(C) being a Grothendieck abelian category, which moreover makes the cogenerator injective.

theorem oppEpiSheaf_exists_injective_coseparator :
    ∃ G : oppEpiSheaf A, Injective G ∧ IsCoseparator G

Stacks.Injectives.oppEpiEmbedding_full, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/FreydMitchell.lean, line 110. The attribute's comment: “the embedding i : A ⥤ D”.

Stacks 05PR, third clause. The functor i : A ⥤ D is full.

theorem oppEpiEmbedding_full : (oppEpiEmbedding A).Full

Stacks.Injectives.oppEpiEmbedding_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/FreydMitchell.lean, line 117. The attribute's comment: “the embedding i : A ⥤ D”.

Stacks 05PR, third clause. The functor i : A ⥤ D is faithful.

theorem oppEpiEmbedding_faithful : (oppEpiEmbedding A).Faithful

Stacks.Injectives.oppEpiEmbedding_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/FreydMitchell.lean, line 124. The attribute's comment: “the embedding i : A ⥤ D”.

Stacks 05PR, third clause. The functor i : A ⥤ D is left exact.

theorem oppEpiEmbedding_preservesFiniteLimits :
    PreservesFiniteLimits (oppEpiEmbedding A)

Stacks.Injectives.oppEpiEmbedding_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/FreydMitchell.lean, line 131. The attribute's comment: “the embedding i : A ⥤ D”.

Stacks 05PR, third clause. The functor i : A ⥤ D is right exact.

theorem oppEpiEmbedding_preservesFiniteColimits :
    PreservesFiniteColimits (oppEpiEmbedding A)

Stacks.Injectives.oppEpiSheafOp_enoughProjectives, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/FreydMitchell.lean, line 138. The attribute's comment: “D has enough projectives”.

Stacks 05PR, fourth clause. D = Bᵒᵖ has enough projectives.

theorem oppEpiSheafOp_enoughProjectives : EnoughProjectives (oppEpiSheaf A)ᵒᵖ

Stacks.Injectives.oppEpiSheafOp_exists_projective_separator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/FreydMitchell.lean, line 142. The attribute's comment: “D has a projective generator”.

Stacks 05PR, fourth clause. D = Bᵒᵖ has a generator, hence a projective generator.

theorem oppEpiSheafOp_exists_projective_separator :
    ∃ P : (oppEpiSheaf A)ᵒᵖ, Projective P ∧ IsSeparator P

Stacks.Injectives.exists_projectiveSeparator_hom_fullyFaithful_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/FreydMitchell.lean, line 154. The attribute's comment: “the embedding into Hom_D(P, -) for a projective generator P”.

Stacks 05PR, last clause. There is a projective generator P of D = Bᵒᵖ such that

A ⟶ Mod_R, X ↦ Hom_D(P, X) with R = Mor_D(P, P)

is a fully faithful exact functor. This is the Freyd--Mitchell embedding theorem for a small abelian category, obtained along the route of Tag 05PR.

theorem exists_projectiveSeparator_hom_fullyFaithful_exact :
    ∃ P : (oppEpiSheaf A)ᵒᵖ, Projective P ∧ IsSeparator P ∧
      (oppEpiEmbedding A ⋙ preadditiveCoyonedaObj P).Full ∧
      (oppEpiEmbedding A ⋙ preadditiveCoyonedaObj P).Faithful ∧
      PreservesFiniteLimits (oppEpiEmbedding A ⋙ preadditiveCoyonedaObj P) ∧
      PreservesFiniteColimits (oppEpiEmbedding A ⋙ preadditiveCoyonedaObj P)

Stacks.Injectives.exists_ring_moduleEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Sheaf/FreydMitchell.lean, line 199.

The Freyd--Mitchell embedding theorem, in the form Tag 05PR retrieves it: for every abelian category A there are a ring R and a fully faithful exact functor A ⥤ Mod_R.

The functor produced here is X ↦ Hom_D(P, X) for a projective generator P of the opposite of the category of abelian sheaves on the epimorphism site of Aᵒᵖ, as in Tag 05PR. The conclusion is the same as Mathlib's CategoryTheory.Abelian.freyd_mitchell, which carries Tag 05PP and is proved instead through Gabriel--Popescu; what Tag 05PR asserts, and what this declaration records, is that the theorem is retrieved from Tag 05PN by the route above.

theorem exists_ring_moduleEmbedding (A : Type u) [Category.{v} A] [Abelian A] :
    ∃ (R : Type (max u v)) (_ : Ring R) (F : A ⥤ ModuleCat.{max u v} R),
      F.Full ∧ F.Faithful ∧ PreservesFiniteLimits F ∧ PreservesFiniteColimits F

Sources

LeanStacks.Sites.EpiPretopology.exists_pretopology_epiCoverings · Stacks.Injectives.preadditiveYoneda_obj_isSheaf · Stacks.Injectives.yonedaSheaf · Stacks.Injectives.yonedaSheaf_full · Stacks.Injectives.yonedaSheaf_faithful · Stacks.Injectives.yonedaSheaf_preservesFiniteLimits · Stacks.Injectives.yonedaSheaf_preservesFiniteColimits · Stacks.Injectives.epiPretopology_hasEnoughPoints

Section19.10 Grothendieck's AB conditions #

Section 19.10 of the Stacks Project, Tag 079A. 1 tag here is carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 079B, a definition

Tag 079B in the Stacks Project.

Stacks.Injectives.IsGenerator, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/GrothendieckAxioms/StacksConditions.lean, line 84. The attribute's comment: “generator”.

An object U of C is a generator if for every N ⊂ M with N ≠ M there is a morphism U ⟶ M which does not factor through N. A subobject N ⊂ M is given by a monomorphism i : N ⟶ M, and N ≠ M says that i is not an isomorphism.

Mathlib has no name for this condition; it uses CategoryTheory.IsSeparator instead, with which this agrees by Stacks.Injectives.isGenerator_iff_isSeparator.

def IsGenerator (U : C) : Prop

Stacks.Injectives.isGenerator_iff_subobject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/GrothendieckAxioms/StacksConditions.lean, line 92. The attribute's comment: “generator as a subobject condition”.

The definition of a generator, phrased with subobjects: U is a generator if and only if for every object M and every subobject N of M other than M itself there is a morphism U ⟶ M which does not factor through N.

theorem isGenerator_iff_subobject (U : C) :
    IsGenerator U ↔ ∀ (M : C) (N : Subobject M), N ≠ ⊤ →
      ∃ u : U ⟶ M, ∀ v : U ⟶ (N : C), v ≫ N.arrow ≠ u

Stacks.Injectives.isGenerator_iff_isSeparator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/GrothendieckAxioms/StacksConditions.lean, line 116. The attribute's comment: “generator is separator”.

A generator in the sense of the Stacks project is the same thing as a separator in the sense of Mathlib: morphisms out of U see every proper subobject if and only if they distinguish parallel morphisms.

From left to right: if f : X ⟶ Y is killed by every morphism U ⟶ X then every such morphism factors through ker f, which therefore cannot be a proper subobject of X, so f = 0. From right to left: if i : N ⟶ M is a monomorphism through which every morphism U ⟶ M factors, then every morphism U ⟶ M is killed by coker i ≠ 0, so i is an epimorphism and hence, C being balanced, an isomorphism.

theorem isGenerator_iff_isSeparator (U : C) : IsGenerator U ↔ IsSeparator U

Stacks.Injectives.isGrothendieckAbelian_iff_ab5_and_exists_isGenerator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/GrothendieckAxioms/StacksConditions.lean, line 151. The attribute's comment: “Grothendieck abelian category”.

An abelian category is a Grothendieck abelian category if it has AB5 and a generator. Both sides are expressed with Mathlib's vocabulary: AB5 at size v is CategoryTheory.AB5OfSize.{v, v}, and CategoryTheory.IsGrothendieckAbelian.{v} is Mathlib's class.

The equivalence is stated at w = v, for v the hom universe of C, because Mathlib's class carries the further requirement LocallySmall.{w} C, which has no counterpart in the Stacks definition and is vacuous exactly for that choice of w. The hypothesis that filtered colimits of size v exist is part of AB5 as the Stacks project states it, AB5 being AB3 together with exactness of filtered colimits; in Mathlib it is the instance argument of CategoryTheory.AB5OfSize, so it has to be assumed on both sides at once.

theorem isGrothendieckAbelian_iff_ab5_and_exists_isGenerator
    [HasFilteredColimitsOfSize.{v, v} C] :
    CategoryTheory.IsGrothendieckAbelian.{v} C ↔
      (CategoryTheory.AB5OfSize.{v, v} C ∧ ∃ U : C, IsGenerator U)

Sources

LeanStacks.Injectives.IsGenerator · Stacks.Injectives.isGenerator_iff_subobject · Stacks.Injectives.isGenerator_iff_isSeparator · Stacks.Injectives.isGrothendieckAbelian_iff_ab5_and_exists_isGenerator

Section19.11 Injectives in Grothendieck categories #

Section 19.11 of the Stacks Project, Tag 05AB. 7 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0E8N, a lemma

Tag 0E8N in the Stacks Project.

Stacks.Injectives.eventuallyConst_subobject_of_monotone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/EventuallyConstantChains.lean, line 79. The attribute's comment: “eventually constant”.

Stacks 0E8N. An increasing well-ordered chain of subobjects is eventually constant if the cofinality of the index order exceeds the number of morphisms from a separator to the ambient object.

theorem eventuallyConst_subobject_of_monotone {U X : C} (hU : IsSeparator U)
    {α : Type w} [LinearOrder α] [WellFoundedLT α]
    (hcof : Cardinal.lift.{w} (Cardinal.mk (U ⟶ X)) <
      Cardinal.lift.{v} (Order.cof α)) (f : α → Subobject X) (hf : Monotone f) :
    atTop.EventuallyConst f

Stacks.Injectives.eventuallyConst_subobject_of_antitone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/EventuallyConstantChains.lean, line 96. The attribute's comment: “eventually constant”.

Stacks 0E8N. A decreasing well-ordered chain of subobjects is eventually constant if the cofinality of the index order exceeds the number of morphisms from a separator to the ambient object.

theorem eventuallyConst_subobject_of_antitone {U X : C} (hU : IsSeparator U)
    {α : Type w} [LinearOrder α] [WellFoundedLT α]
    (hcof : Cardinal.lift.{w} (Cardinal.mk (U ⟶ X)) <
      Cardinal.lift.{v} (Order.cof α)) (f : α → Subobject X) (hf : Antitone f) :
    atTop.EventuallyConst f

Stacks.Injectives.mk_subobject_le_two_pow_mk_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/SubobjectCardinality.lean, line 64. The attribute's comment: “subobject cardinality”.

The collection of subobjects of an object has cardinality at most the cardinality of the power set of the morphisms to it from a separator.

theorem mk_subobject_le_two_pow_mk_hom {U X : C} (hU : IsSeparator U) :
    Cardinal.mk (Subobject X) ≤
      (2 : Cardinal.{max u v}) ^ Cardinal.lift.{u} (Cardinal.mk (U ⟶ X))

Stacks.Injectives.cardinality_le_hom_of_strictMono_subobject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/SubobjectCardinality.lean, line 191. The attribute's comment: “chain bound”.

A strictly increasing chain of subobjects has cardinality at most the cardinality of the set of morphisms from a separator to the ambient object.

theorem cardinality_le_hom_of_strictMono_subobject {U X : C} (hU : IsSeparator U)
    {ι : Type w} [LinearOrder ι] [WellFoundedLT ι]
    (f : ι → Subobject X) (hf : StrictMono f) :
    Cardinal.lift.{v} (Cardinal.mk ι) ≤ Cardinal.lift.{w} (Cardinal.mk (U ⟶ X))

Stacks.Injectives.cardinality_le_hom_of_strictAnti_subobject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/SubobjectCardinality.lean, line 206. The attribute's comment: “chain bound”.

A strictly decreasing chain of subobjects has cardinality at most the cardinality of the set of morphisms from a separator to the ambient object.

theorem cardinality_le_hom_of_strictAnti_subobject {U X : C} (hU : IsSeparator U)
    {ι : Type w} [LinearOrder ι] [WellFoundedLT ι]
    (f : ι → Subobject X) (hf : StrictAnti f) :
    Cardinal.lift.{v} (Cardinal.mk ι) ≤ Cardinal.lift.{w} (Cardinal.mk (U ⟶ X))

Tag 079C, a definition

Tag 079C in the Stacks Project.

Stacks.Injectives.Size.size, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/Defs.lean, line 41.

The size of an object M of an abelian category: the cardinality of the set of subobjects of M.

noncomputable def size {C : Type*} [Category C] [Abelian C] (M : C) : Cardinal

Tag 079D, a lemma

Tag 079D in the Stacks Project.

Stacks.Injectives.Size.size_X₁_le_size_X₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/Defs.lean, line 48.

For a short exact sequence 0 → M' → M → M'' → 0 in a Grothendieck abelian category, the size of M' is at most the size of M: there is an injection from the subobjects of M' into the subobjects of M, hence |M'| ≤ |M|.

theorem size_X₁_le_size_X₂ {C : Type*} [Category C] [Abelian C] [IsGrothendieckAbelian C]
    (S : ShortComplex C) (hS : S.ShortExact) :
    size S.X₁ ≤ size S.X₂

Stacks.Injectives.Size.size_X₃_le_size_X₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/Defs.lean, line 86.

For a short exact sequence 0 → M' → M → M'' → 0, the size of M'' is at most the size of M: there is an injection from the subobjects of M'' into the subobjects of M, hence |M''| ≤ |M|.

theorem size_X₃_le_size_X₂ {C : Type*} [Category C] [Abelian C] [IsGrothendieckAbelian C]
    (S : ShortComplex C) (hS : S.ShortExact) :
    size S.X₃ ≤ size S.X₂

Tag 079E, a lemma

Tag 079E in the Stacks Project.

Stacks.Injectives.exists_epi_coproduct_of_subobject_cardinality_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/BoundedSizeObjects.lean, line 102. The attribute's comment: “part (1)”.

If the cardinality of the set of subobjects of M is at most κ, then M is a quotient of a coproduct, indexed by a type of cardinality at most κ, of copies of the generator U.

theorem exists_epi_coproduct_of_subobject_cardinality_le (U M : C) (hU : IsSeparator U)
    (κ : Cardinal.{w})
    (hM : Cardinal.lift.{w} (Cardinal.mk (Subobject M)) ≤
      Cardinal.lift.{max u v} κ) :
    ∃ (ι : Type w), Cardinal.mk ι ≤ κ ∧
      ∃ (f : (∐ fun (_ : ι) => U) ⟶ M), Epi f

Stacks.Injectives.essentiallySmall_subobject_cardinality_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/BoundedSizeObjects.lean, line 113. The attribute's comment: “part (2)”.

For every cardinal κ, the objects whose sets of subobjects have cardinality at most κ have only a set of isomorphism classes.

theorem essentiallySmall_subobject_cardinality_le (κ : Cardinal.{w}) :
    ObjectProperty.EssentiallySmall.{w}
      (fun M : C => Cardinal.lift.{w} (Cardinal.mk (Subobject M)) ≤
        Cardinal.lift.{max u v} κ)

Tag 079F, a proposition

Tag 079F in the Stacks Project.

Stacks.Injectives.isSmallWithRespectTo_monomorphisms_of_hasCardinalLT_subobject_cof, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/SmallWithRespectToInjections.lean, line 76.

Stacks 079F. Let A be a Grothendieck abelian category, let M be an object of A and let κ = |M| be the cardinality of the set of subobjects of M. If α is an ordinal whose cofinality is bigger than κ, then M is α-small with respect to injections: for every system (B_β)_{β ∈ α} in A with monomorphic transition maps the canonical map colim_β Hom(M, B_β) ⟶ Hom(M, colim_β B_β) is bijective.

theorem isSmallWithRespectTo_monomorphisms_of_hasCardinalLT_subobject_cof
    {C : Type u} [Category.{v} C] [Abelian C] [IsGrothendieckAbelian.{w} C]
    (M : C) (α : Ordinal.{w}) (hM : HasCardinalLT (Subobject M) α.cof) :
    IsSmallWithRespectTo M (MorphismProperty.monomorphisms C) α

Tag 079G, a lemma

Tag 079G in the Stacks Project.

CategoryTheory.injective_iff_exists_extension_of_subobject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/DetectingMonomorphisms.lean, line 76.

Stacks Tag 079G. An object I of a Grothendieck abelian category is injective if and only if, for every subobject M of a separator G, every morphism M ⟶ I extends along M.arrow to a morphism G ⟶ I.

The forward implication is injectivity applied to the monomorphism M.arrow; the converse is the statement that the inclusions of the subobjects of a separator have the same right lifting property as all monomorphisms.

theorem injective_iff_exists_extension_of_subobject [Abelian C] [IsGrothendieckAbelian.{w} C]
    {G : C} (hG : IsSeparator G) (I : C) :
    Injective I ↔
      ∀ (M : Subobject G) (f : (M : C) ⟶ I), ∃ g : G ⟶ I, M.arrow ≫ g = f

CategoryTheory.exists_monomorphisms_injective_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/DetectingMonomorphisms.lean, line 98. The attribute's comment: “set-indexed form”.

Tag 079G in set-indexed form. A Grothendieck abelian category has a set T and, for each t : T, a monomorphism N t ⟶ N' t such that an object I is injective precisely when every morphism N t ⟶ I extends to N' t.

The family is the one of injective_iff_exists_extension_of_subobject: the inclusions of the subobjects of CategoryTheory.separator C, whose collection is w-small because a Grothendieck abelian category is well-powered. This is the shape in which Tags 0FSN and 0FSS consume Tag 079G.

theorem exists_monomorphisms_injective_iff (C : Type u) [Category.{v} C] [Abelian C]
    [IsGrothendieckAbelian.{w} C] :
    ∃ (T : Type w) (N N' : T → C) (i : ∀ t, N t ⟶ N' t),
      (∀ t, Mono (i t)) ∧
        ∀ I : C, Injective I ↔ ∀ (t : T) (f : N t ⟶ I), ∃ g : N' t ⟶ I, i t ≫ g = f

Tag 079H, a theorem

Tag 079H in the Stacks Project.

Stacks.Injectives.FunctorialEmbedding.hasFunctorialInjectiveEmbeddings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Preadditive/Injective/GrothendieckFunctorial.lean, line 107. The attribute's comment: “functorial form; Mathlib's enoughInjectives has the non-functorial half”. References: SGA 4 V (0.1.1), “enough injectives”.

Stacks Project, Tag 079H. A Grothendieck abelian category has functorial injective embeddings in the sense of [Stacks, Tag 0139].

theorem hasFunctorialInjectiveEmbeddings : HasFunctorialInjectiveEmbeddings C

Sources

LeanStacks.Injectives.eventuallyConst_subobject_of_monotone · Stacks.Injectives.eventuallyConst_subobject_of_antitone · Stacks.Injectives.mk_subobject_le_two_pow_mk_hom · Stacks.Injectives.cardinality_le_hom_of_strictMono_subobject · Stacks.Injectives.cardinality_le_hom_of_strictAnti_subobject · Stacks.Injectives.Size.size · Stacks.Injectives.Size.size_X₁_le_size_X₂ · Stacks.Injectives.Size.size_X₃_le_size_X₂

Section19.12 K-injectives in Grothendieck categories #

Section 19.12 of the Stacks Project, Tag 079I. 6 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 079J, a lemma

Tag 079J in the Stacks Project.

Stacks.Injectives.SmallSubobjectEpi.exists_subobject_epi_size_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Size/SmallSubobjectEpi.lean, line 259.

Let C be a Grothendieck abelian category with generator separator C. For every epimorphism π : M ⟶ N there is a subobject M' ⊆ M such that M'.arrow ≫ π is an epimorphism and size M' ≤ cardFn (separator C) (size N).

theorem exists_subobject_epi_size_le
    (M N : C) (π : M ⟶ N) [Epi π] :
    ∃ M' : Subobject M,
      Epi (M'.arrow ≫ π) ∧
      size ((M' : C)) ≤ cardFn (separator C) (size N)

Tag 079K, a lemma

Tag 079K in the Stacks Project.

Stacks.Injectives.acyclicComplexSizeBound, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/SmallAcyclicComplexes.lean, line 62. The attribute's comment: “the cardinal”.

A cardinal which uniformly bounds the sizes of the terms of the small bounded-above acyclic complexes: the supremum over n of the (n + 1)-st iterate of κ ↦ #(Subobject (∐_κ U)) at #(Subobject U), where U is the separator of C.

noncomputable def acyclicComplexSizeBound (C : Type u) [Category.{v} C] [Abelian C]
    [IsGrothendieckAbelian.{w} C] : Cardinal.{w}

Stacks.Injectives.exists_small_boundedAbove_acyclic_subcomplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/SmallAcyclicComplexes.lean, line 447. The attribute's comment: “part (1)”.

Every nonzero acyclic complex contains a nonzero bounded-above acyclic subcomplex whose terms have uniformly bounded size.

theorem exists_small_boundedAbove_acyclic_subcomplex
    (M : CochainComplex C ℤ) (hM : M.Acyclic) (hM₀ : ¬ IsZero M) :
    ∃ (N : CochainComplex C ℤ) (f : N ⟶ M),
      Mono f ∧
      ¬ IsZero N ∧
      N.Acyclic ∧
      (∃ a : ℤ, ∀ n : ℤ, a < n → IsZero (N.X n)) ∧
      ∀ n : ℤ, Cardinal.mk (Shrink.{w} (Subobject (N.X n))) ≤
        acyclicComplexSizeBound (C := C)

Stacks.Injectives.exists_epi_coproduct_small_boundedAbove_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/SmallAcyclicComplexes.lean, line 475. The attribute's comment: “part (2)”.

Every acyclic complex is an epimorphic image of a coproduct of bounded-above acyclic complexes whose terms have uniformly bounded size.

theorem exists_epi_coproduct_small_boundedAbove_acyclic
    (M : CochainComplex C ℤ) (hM : M.Acyclic) :
    ∃ (I : Type w) (N : I → CochainComplex C ℤ)
      (f : (∐ fun i ↦ N i) ⟶ M),
      Epi f ∧
      ∀ i : I,
        (N i).Acyclic ∧
        (∃ a : ℤ, ∀ n : ℤ, a < n → IsZero ((N i).X n)) ∧
        ∀ n : ℤ,
          Cardinal.mk (Shrink.{w} (Subobject ((N i).X n))) ≤
            acyclicComplexSizeBound (C := C)

Tag 079L, a lemma

Tag 079L in the Stacks Project.

Stacks.Injectives.isKInjective_of_small_boundedAbove_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/Criterion.lean, line 686.

A complex of injective objects is K-injective provided that all maps to it from bounded-above acyclic complexes within the uniform size bound are null-homotopic.

theorem isKInjective_of_small_boundedAbove_acyclic (I : CochainComplex C ℤ)
    (hI : ∀ n : ℤ, Injective (I.X n))
    (hvanish : ∀ (M : CochainComplex C ℤ), M.Acyclic →
      (∃ a : ℤ, ∀ n : ℤ, a < n → IsZero (M.X n)) →
      (∀ n : ℤ, Cardinal.mk (Shrink.{w} (Subobject (M.X n))) ≤
        acyclicComplexSizeBound (C := C)) →
      ∀ f : M ⟶ I, Nonempty (Homotopy f 0)) :
    I.IsKInjective

Stacks.Injectives.isKInjective_of_injective_of_small_boundedAbove_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/Criterion.lean, line 765.

A complex of injective objects in a Grothendieck abelian category is K-injective if every map to it in the homotopy category from a uniformly small bounded-above acyclic complex is zero.

theorem isKInjective_of_injective_of_small_boundedAbove_acyclic
    (I : CochainComplex C ℤ) [∀ n : ℤ, Injective (I.X n)]
    (hI : ∀ (M : CochainComplex C ℤ), M.Acyclic →
      (∃ a : ℤ, ∀ n : ℤ, a < n → IsZero (M.X n)) →
      (∀ n : ℤ, Cardinal.mk (Shrink.{w} (Subobject (M.X n))) ≤
        acyclicComplexSizeBound (C := C)) →
      ∀ f : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj M ⟶
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj I, f = 0) :
    I.IsKInjective

Tag 079M, a lemma

Tag 079M in the Stacks Project.

Stacks.Injectives.exists_functorial_termwise_mono_quasiIso_homotopy_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/FunctorialHomotopies.lean, line 46.

Stacks Project, Tag 079M. For a set of acyclic cochain complexes, there is a functorial termwise monomorphic quasi-isomorphism such that postcomposing any map from one of the given complexes makes that map null-homotopic.

theorem exists_functorial_termwise_mono_quasiIso_homotopy_zero
    {I : Type w} (K : I → CochainComplex C ℤ) (hK : ∀ i, (K i).Acyclic) :
    ∃ (F : CochainComplex C ℤ ⥤ CochainComplex C ℤ)
      (j : Functor.id (CochainComplex C ℤ) ⟶ F),
      (∀ (M : CochainComplex C ℤ) (n : ℤ), Mono ((j.app M).f n)) ∧
      (∀ M : CochainComplex C ℤ, QuasiIso (j.app M)) ∧
      ∀ (M : CochainComplex C ℤ) (i : I) (f : K i ⟶ M),
        homotopic C (ComplexShape.up ℤ) (f ≫ j.app M) 0

Tag 079N, a lemma

Tag 079N in the Stacks Project.

Stacks.Injectives.exists_functorialInjectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/Enlargement.lean, line 681.

A Grothendieck abelian category admits a functorial termwise monomorphic quasi-isomorphism from every cochain complex to one whose map in each degree factors through an injective subobject.

theorem exists_functorialInjectiveResolution [IsGrothendieckAbelian.{w} C] :
    Nonempty (FunctorialInjectiveResolution C)

Stacks.Injectives.FunctorialEnlargement.exists_functorialInjectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Spaltenstein/Enlargement.lean, line 685.

Stacks Project, Tag 079N. A Grothendieck abelian category admits a functorial injective enlargement of unbounded cochain complexes: a functor on CochainComplex C ℤ together with a natural inclusion which is a monomorphism in every degree, a quasi-isomorphism, and which in each degree factors through an injective subobject of the corresponding term of the enlargement.

This discharges the hypothesis of [Stacks, Tag 079P], which the tree states relative to exactly this datum.

theorem exists_functorialInjectiveResolution :
    Nonempty (Stacks.Injectives.KInjectiveResolution.FunctorialInjectiveResolution C)

Tag 079P, a theorem

Tag 079P in the Stacks Project.

Stacks.Injectives.exists_functorial_quasiIso_isKInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/FunctorialResolution.lean, line 1198. The attribute's comment: “existence and functoriality”.

Functorial K-injective resolutions exist in a Grothendieck abelian category.

theorem exists_functorial_quasiIso_isKInjective :
    Nonempty (FunctorialKInjectiveResolution C)

Stacks.Injectives.kInjectiveResolutionInclusion_quasiIso, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/FunctorialResolution.lean, line 1372. The attribute's comment: “quasi-isomorphism”.

The inclusion into the chosen K-injective resolution is a quasi-isomorphism.

noncomputable instance kInjectiveResolutionInclusion_quasiIso
    (M : CochainComplex C ℤ) :
    QuasiIso ((kInjectiveResolutionInclusion C).app M)

Stacks.Injectives.kInjectiveResolutionInclusion_f_mono, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/FunctorialResolution.lean, line 1379. The attribute's comment: “termwise monomorphism”.

The inclusion into the chosen K-injective resolution is termwise monic.

noncomputable instance kInjectiveResolutionInclusion_f_mono
    (M : CochainComplex C ℤ) (n : ℤ) :
    Mono (((kInjectiveResolutionInclusion C).app M).f n)

Stacks.Injectives.kInjectiveResolutionFunctor_obj_X_injective, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/FunctorialResolution.lean, line 1386. The attribute's comment: “injective terms”.

Every term of the chosen resolution is an injective object.

noncomputable instance kInjectiveResolutionFunctor_obj_X_injective
    (M : CochainComplex C ℤ) (n : ℤ) :
    Injective (((kInjectiveResolutionFunctor C).obj M).X n)

Stacks.Injectives.kInjectiveResolutionFunctor_obj_isKInjective, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/KInjective/FunctorialResolution.lean, line 1393. The attribute's comment: “K-injective target”.

The chosen resolution is K-injective.

noncomputable instance kInjectiveResolutionFunctor_obj_isKInjective
    (M : CochainComplex C ℤ) :
    ((kInjectiveResolutionFunctor C).obj M).IsKInjective

Stacks.Injectives.FunctorialEnlargement.exists_functorial_quasiIso_isKInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Spaltenstein/Enlargement.lean, line 706. The attribute's comment: “existence and functoriality”. References: SGA 2 VIII (1.4), “more general”.

Stacks Project, Tag 079P, unconditionally. Functorial K-injective resolutions exist in a Grothendieck abelian category: every complex M admits, functorially in M, a termwise monomorphic quasi-isomorphism into a K-injective complex with injective terms.

The tree proves this relative to the Tag 079N datum (exists_functorial_quasiIso_isKInjective_of_functorialInjectiveResolution); exists_functorialInjectiveResolution supplies the datum.

theorem exists_functorial_quasiIso_isKInjective :
    Nonempty (Stacks.Injectives.KInjectiveResolution.FunctorialKInjectiveResolution C)

Sources

LeanStacks.Injectives.SmallSubobjectEpi.exists_subobject_epi_size_le · Stacks.Injectives.acyclicComplexSizeBound · Stacks.Injectives.exists_small_boundedAbove_acyclic_subcomplex · Stacks.Injectives.exists_epi_coproduct_small_boundedAbove_acyclic · Stacks.Injectives.isKInjective_of_small_boundedAbove_acyclic · Stacks.Injectives.isKInjective_of_injective_of_small_boundedAbove_acyclic · Stacks.Injectives.exists_functorial_termwise_mono_quasiIso_homotopy_zero · Stacks.Injectives.exists_functorialInjectiveResolution

Section19.13 Additional remarks on Grothendieck abelian categories #

Section 19.13 of the Stacks Project, Tag 07D6. 12 tags here are carried by 49 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07D7, a lemma

Tag 07D7 in the Stacks Project.

Stacks.Injectives.isRepresentable_iff_preservesLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Representability.lean, line 78. References: SGA 4 I (8.12.7), “Grothendieck abelian”.

Let A be a Grothendieck abelian category and F : Aᵒᵖ ⥤ Set a functor. Then F is representable if and only if it commutes with colimits, that is, F (colim_i N_i) = lim_i F (N_i) for every diagram I ⥤ A.

theorem isRepresentable_iff_preservesLimits [Abelian C] [IsGrothendieckAbelian.{w} C]
    (F : Cᵒᵖ ⥤ Type w) : F.IsRepresentable ↔ PreservesLimitsOfSize.{w, w} F

Tag 07D8, a lemma

Tag 07D8 in the Stacks Project.

Stacks.Injectives.hasProducts_of_isGrothendieckAbelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/GrothendieckAxioms/StacksConditions.lean, line 175. References: SGA 4 V (0.1.1).

A Grothendieck abelian category has AB3*, that is, it has products. Mathlib's name for AB3* is CategoryTheory.Limits.HasProducts, so there is nothing left to define here.

The Stacks project deduces this from its criterion for representability of a functor on a Grothendieck abelian category: for a family M_i of objects the functor F = ∏ h_{M_i} commutes with colimits, so it is representable, and the representing object is the product of the family. Here we instead invoke CategoryTheory.IsGrothendieckAbelian.hasLimits, which gives all limits of size w at once.

theorem hasProducts_of_isGrothendieckAbelian [CategoryTheory.IsGrothendieckAbelian.{w} C] :
    HasProducts.{w} C

Tag 079Q, a remark

Tag 079Q in the Stacks Project.

Stacks.Injectives.kInjectiveResolutionHomMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/DerivedCategory/Existence.lean, line 96. The attribute's comment: “morphisms via a K-injective resolution”.

Derived morphisms into a complex L are computed by homotopy classes of maps into the chosen K-injective resolution of L.

theorem kInjectiveResolutionHomMap_bijective (K L : CochainComplex C ℤ) :
    Function.Bijective (kInjectiveResolutionHomMap C K L)

Stacks.Injectives.hasDerivedCategory_of_isGrothendieckAbelian, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/DerivedCategory/Existence.lean, line 119. The attribute's comment: “existence of the derived category”.

A Grothendieck abelian category which is locally small in the universe w admits a derived category whose morphism types lie in w.

noncomputable def hasDerivedCategory_of_isGrothendieckAbelian
    [inst_groth : IsGrothendieckAbelian.{w} C] :
    HasDerivedCategory.{w} C

Declarations registered for the tag:

instIsGrothendieckAbelianModuleCat registered with add_to_stacks in StacksFrontier/Homology/Injectives/DerivedCategory/Existence.lean, line 153 (StacksFrontier): “modules over a ring”.
SheafOfModules.instIsGrothendieckAbelian registered with add_to_stacks in StacksFrontier/Homology/Injectives/DerivedCategory/Existence.lean, line 154 (StacksFrontier): “sheaves of modules on a ringed site”. References: SGA 3 I (3.2.1), “special case”; SGA 4 II (6.7), “special case”; SGA 6 I (1.3), “partial”.

Tag 07D9, a lemma

Tag 07D9 in the Stacks Project.

Stacks.Injectives.isLimit_productFanInDerivedCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/DerivedCategory/KInjectiveProducts.lean, line 178. The attribute's comment: “termwise products of K-injective complexes”.

The termwise product of K-injective representatives represents their product in the unbounded derived category.

theorem isLimit_productFanInDerivedCategory {I : Type w}
    (K : I → CochainComplex A ℤ) (hK : ∀ i, (K i).IsKInjective) :
    Nonempty (IsLimit (productFanInDerivedCategory K))

Stacks.Injectives.derivedCategoryQ_preservesCoproducts, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/DerivedCategory/ProductsAndCoproducts.lean, line 109. The attribute's comment: “direct_sums_termwise”.

The localization functor from complexes to the unbounded derived category preserves direct sums; thus the image of the termwise direct sum of any family of complexes is its direct sum in the derived category.

instance derivedCategoryQ_preservesCoproducts [IsGrothendieckAbelian.{w} A] (I : Type w) :
    PreservesColimitsOfShape (Discrete I) (DerivedCategory.Q (C := A))

Stacks.Injectives.hasCoproducts_derivedCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/DerivedCategory/ProductsAndCoproducts.lean, line 137. The attribute's comment: “direct_sums_exist”.

The unbounded derived category of a Grothendieck abelian category has direct sums.

instance hasCoproducts_derivedCategory (A : Type u) [Category.{v} A] [Abelian A]
    [IsGrothendieckAbelian.{w} A] [HasDerivedCategory.{z} A] :
    HasCoproducts.{w} (DerivedCategory A)

Stacks.Injectives.hasProducts_derivedCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/DerivedCategory/ProductsAndCoproducts.lean, line 190. The attribute's comment: “products_exist”.

The unbounded derived category of a Grothendieck abelian category has arbitrary products.

instance hasProducts_derivedCategory (𝒜 : Type u) [Category.{v} 𝒜] [Abelian 𝒜]
    [IsGrothendieckAbelian.{w} 𝒜] [HasDerivedCategory.{w'} 𝒜] :
    HasProducts.{w} (DerivedCategory 𝒜)

Tag 08U1, a lemma

Tag 08U1 in the Stacks Project.

AlgebraicGeometry.RingedSite.isDerivedLimit_map_derivedGlobalSectionsOverUnbounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/UnboundedGlobalSections.lean, line 246. The attribute's comment: “for A-linear derived global sections on a ringed site”.

RΓ(𝒞, -) over a base ring commutes with R lim: A-linear derived global sections carry a derived inverse limit in D(𝒪) to a derived inverse limit in D(A).

This is [Stacks, Tag 08U1] for derivedGlobalSectionsOverUnbounded, through Stacks.Injectives.isDerivedLimit_map_rightDerivedFunctor: the functor is the right derived functor of moduleGlobalSectionsOver by derivedGlobalSectionsOverUnbounded_isRightDerivedFunctor, that functor preserves countable products, Mod(𝒪) is Grothendieck abelian and the countable products of ModuleCat A are exact. This is the site-and-base-ring form of [Stacks, Tag 0D6K], whose Γ(𝒞, -)-valued form is Stacks.Cohomology.DerivedGlobalSections.isDerivedLimit_map_derivedGlobalSections, and the ringed-site counterpart of [Stacks, Tag 0D60] for a ringed space, Stacks.Cohomology.DerivedSectionsOverBase.isDerivedLimit_map_derivedSectionsOver.

theorem isDerivedLimit_map_derivedGlobalSectionsOverUnbounded
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (ringSheaf X.O)))
    [HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
    (L : DerivedCategory (SheafOfModules.{u} (ringSheaf X.O)))
    (hL : Pretriangulated.IsDerivedLimit K L) :
    ∃ h : HasProduct
        (fun n : ℕ ↦ (derivedGlobalSectionsOverUnbounded X A ρ).obj (K.obj ⟨n⟩)),
      @Pretriangulated.IsDerivedLimit (DerivedCategory (ModuleCat.{u} A)) _ _ _ _ _ _
        (K ⋙ derivedGlobalSectionsOverUnbounded X A ρ) h
        ((derivedGlobalSectionsOverUnbounded X A ρ).obj L)

Stacks.Injectives.isDerivedLimit_map_rightDerivedFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/DerivedCategory/DerivedLimit.lean, line 299.

Stacks 08U1. The right derived functor of an additive functor from a Grothendieck abelian category to an abelian category with exact countable products carries every derived-limit triangle to a derived-limit triangle, if the functor preserves countable products. Its structural map is the image of the supplied p, followed by the canonical product comparison; hence its projections are RF.map (p ≫ Pi.π _ n).

theorem isDerivedLimit_map_rightDerivedFunctor (X : ℕᵒᵖ ⥤ DerivedCategory A)
    [HasProduct fun n : ℕ ↦ X.obj ⟨n⟩] (K : DerivedCategory A)
    (p : K ⟶ ∏ᶜ fun n : ℕ ↦ X.obj ⟨n⟩)
    (hK : ∃ δ : (∏ᶜ fun n : ℕ ↦ X.obj ⟨n⟩) ⟶ K⟦(1 : ℤ)⟧,
      Triangle.mk p (Pi.lift fun n : ℕ ↦ Pi.π (fun n : ℕ ↦ X.obj ⟨n⟩) n -
        Pi.π (fun n : ℕ ↦ X.obj ⟨n⟩) (n + 1) ≫
          X.map (homOfLE (Nat.le_succ n)).op) δ ∈ distTriang (DerivedCategory A)) :
    ∃ h : HasProduct (fun n : ℕ ↦ RF.obj (X.obj ⟨n⟩)),
      letI := h
      ∃ δ : (∏ᶜ fun n : ℕ ↦ RF.obj (X.obj ⟨n⟩)) ⟶ (RF.obj K)⟦(1 : ℤ)⟧,
        Triangle.mk (RF.map p ≫ piComparison RF (fun n : ℕ ↦ X.obj ⟨n⟩))
          (Pi.lift fun n : ℕ ↦ Pi.π (fun n : ℕ ↦ RF.obj (X.obj ⟨n⟩)) n -
            Pi.π (fun n : ℕ ↦ RF.obj (X.obj ⟨n⟩)) (n + 1) ≫
              RF.map (X.map (homOfLE (Nat.le_succ n)).op)) δ ∈
          distTriang (DerivedCategory B)

Tag 0BKI, a lemma

Tag 0BKI in the Stacks Project.

Stacks.Injectives.exists_filtered_quasiIso_isKInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/FilteredComplex/KInjectiveResolution.lean, line 951.

Stacks 0BKI. A filtered complex in a Grothendieck abelian category has a filtered resolution which is termwise injective and K-injective before and after taking any filtration step or filtration quotient, and the comparison maps on all of these complexes are quasi-isomorphisms.

theorem exists_filtered_quasiIso_isKInjective [IsGrothendieckAbelian.{w'} A]
    (K : CochainComplex.Filtered A) :
    ∃ (J : CochainComplex.Filtered A) (j : K ⟶ J),
      (∀ n : ℤ, Injective (J.X.X n)) ∧
      (∀ p n : ℤ, Injective ((J.filtration.obj (op p)).X n)) ∧
      (∀ p n : ℤ, Injective ((cokernel (J.filtration.ι.app (op p))).X n)) ∧
      (∀ (p p' : ℤ) (h : p ≤ p') n,
        Injective ((cokernel (J.filtration.diagram.map (opHomOfLE h))).X n)) ∧
      J.X.IsKInjective ∧
      (∀ p : ℤ, (J.filtration.obj (op p)).IsKInjective) ∧
      (∀ p : ℤ, (cokernel (J.filtration.ι.app (op p))).IsKInjective) ∧
      (∀ (p p' : ℤ) (h : p ≤ p'),
        (cokernel (J.filtration.diagram.map (opHomOfLE h))).IsKInjective) ∧
      QuasiIso j.hom ∧
      (∀ p : ℤ, QuasiIso (j.natTrans.app (op p))) ∧
      (∀ p : ℤ, QuasiIso (filtrationQuotientMap j p)) ∧
      ∀ (p p' : ℤ) (h : p ≤ p'), QuasiIso (filtrationSubquotientMap j h)

Tag 0G1X, a remark

Tag 0G1X in the Stacks Project.

Stacks.Injectives.extSpectralSequenceInto_isBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/SpectralSequenceIntoConvergence.lean, line 407. The attribute's comment: “ext_spectral_sequence_convergence”.

Stacks 0G1X, boundedness. If in every degree Ext^n(M, F^pK^•) vanishes for p ≫ 0 and maps bijectively onto Ext^n(M, K^•) for p ≪ 0, then the Ext spectral sequence into K^• is bounded: in each total degree only finitely many terms of its first page are nonzero.

theorem extSpectralSequenceInto_isBounded
    (hzero : ∀ n : ℤ, ∃ p₀ : ℤ, ∀ p : ℤ, p₀ ≤ p →
      Subsingleton (DerivedCategory.Ext M (DerivedCategory.Q.obj (K.filtration.obj (op p))) n))
    (hiso : ∀ n : ℤ, ∃ p₁ : ℤ, ∀ p : ℤ, p ≤ p₁ →
      Function.Bijective
        (extPostcomp M n (DerivedCategory.Q.map (K.filtration.ι.app (op p))))) :
    IsBounded (extSpectralSequenceInto.{w', w} M K).1

Stacks.Injectives.extSpectralSequenceInto_hasPageInfinityAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/SpectralSequenceIntoConvergence.lean, line 421. The attribute's comment: “ext_spectral_sequence_convergence”.

Stacks 0G1X, the infinity page exists. Under the same hypotheses the Ext spectral sequence into K^• stabilises at every bidegree.

theorem extSpectralSequenceInto_hasPageInfinityAt
    (hzero : ∀ n : ℤ, ∃ p₀ : ℤ, ∀ p : ℤ, p₀ ≤ p →
      Subsingleton (DerivedCategory.Ext M (DerivedCategory.Q.obj (K.filtration.obj (op p))) n))
    (hiso : ∀ n : ℤ, ∃ p₁ : ℤ, ∀ p : ℤ, p ≤ p₁ →
      Function.Bijective
        (extPostcomp M n (DerivedCategory.Q.map (K.filtration.ι.app (op p)))))
    (pq : ℤ × ℤ) :
    (extSpectralSequenceInto.{w', w} M K).1.HasPageInfinityAt pq

Stacks.Injectives.extSpectralSequenceInto_convergesToExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/SpectralSequenceIntoConvergence.lean, line 490. The attribute's comment: “ext_spectral_sequence_convergence”.

Stacks 0G1X, convergence. If in every degree Ext^n(M, F^pK^•) vanishes for p ≫ 0 and maps bijectively onto Ext^n(M, K^•) for p ≪ 0, then the Ext spectral sequence into K^• converges to Ext^{p + q}(M, K^•): the decreasing filtration Stacks.Injectives.extIntoFiltration of Ext^n(M, K^•) is finite, being ⊤ for p ≪ 0 and ⊥ for p ≫ 0, the spectral sequence has an infinity page everywhere, and E_∞^{p, q} ≅ F^p/F^{p + 1} in total degree n = p + q.

theorem extSpectralSequenceInto_convergesToExt
    (hzero : ∀ n : ℤ, ∃ p₀ : ℤ, ∀ p : ℤ, p₀ ≤ p →
      Subsingleton (DerivedCategory.Ext M (DerivedCategory.Q.obj (K.filtration.obj (op p))) n))
    (hiso : ∀ n : ℤ, ∃ p₁ : ℤ, ∀ p : ℤ, p ≤ p₁ →
      Function.Bijective
        (extPostcomp M n (DerivedCategory.Q.map (K.filtration.ι.app (op p))))) :
    let E := (extSpectralSequenceInto.{w', w} M K).1
    ∃ hF : ∀ n : ℤ, Antitone (extIntoFiltration M K n),
      (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ extIntoFiltration M K n a = ⊤ ∧
        extIntoFiltration M K n b = ⊥) ∧
      (∀ p q : ℤ, E.HasPageInfinityAt (p, q)) ∧
      ∀ p q : ℤ, Nonempty
        ((E.pageInfinity (p, q) : Type v) ≃+
          ((cokernel (Subobject.ofLE (extIntoFiltration M K (p + q) (p + 1))
              (extIntoFiltration M K (p + q) p)
              (hF (p + q) (by omega))) : AddCommGrpCat.{w}) : Type w))

Stacks.Injectives.extSpectralSequenceInto, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/SpectralSequenceIntoFilteredComplex.lean, line 107. The attribute's comment: “ext_spectral_sequence”. References: EGA 0 (13.7.3), “Ext functor case”.

Stacks 0G1X. For a filtered complex K^• of a Grothendieck abelian category and an object M of D(A), the cohomological spectral sequence (E_r, d_r)_{r ≥ 1} of the filtered Hom complex, bundled with the identifications E_1^{p,q} = Ext^{p+q}(M, gr^pK). Its differential on page r has bidegree (r, -r + 1) by the definition of CohomologicalSpectralSequence.

def extSpectralSequenceInto (M : DerivedCategory A) (K : CochainComplex.Filtered A) :
    Σ E : CohomologicalSpectralSequence AddCommGrpCat.{v} 1,
      ∀ p q : ℤ, ((E.page 1).X (p, q) : Type v) ≃+
        DerivedCategory.Ext M
          (DerivedCategory.Q.obj ((FilteredObject.gr p).obj K)) (p + q)

Tag 0G1Y, a remark

Tag 0G1Y in the Stacks Project.

Stacks.Injectives.nonempty_canonicalExtSpectralSequenceInto_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/SpectralSequenceIntoIndependence.lean, line 365. The attribute's comment: “representative_independence”.

Stacks 0G1Y, representative independence. Let A be a Grothendieck abelian category and let M and K be objects of D(A). The Ext spectral sequence of Tag 0G1X attached to the canonical truncation filtration F^pK^• = τ_{≤ -p}K^• of a complex K^• representing K does not depend on the choice of K^•: for any two complexes K₁^• and K₂^• representing K the two spectral sequences are isomorphic, so they have the same pages, differentials and page-turning isomorphisms from E₁ onward.

The two spectral sequences compared are the ones named Stacks.Injectives.canonicalExtSpectralSequenceInto M K₁ and Stacks.Injectives.canonicalExtSpectralSequenceInto M K₂, that name being by definition the Ext spectral sequence of Tag 0G1X applied to the canonical truncation filtration; it is written out here so that this file does not depend on the module which introduces it.

theorem nonempty_canonicalExtSpectralSequenceInto_iso (M : DerivedCategory A)
    (K : DerivedCategory A) (K₁ K₂ : CochainComplex A ℤ)
    (e₁ : DerivedCategory.Q.obj K₁ ≅ K) (e₂ : DerivedCategory.Q.obj K₂ ≅ K) :
    Nonempty ((extSpectralSequenceInto.{w', w} M
        (CochainComplex.canonicalTruncationFiltration K₁)).1 ≅
      (extSpectralSequenceInto.{w', w} M
        (CochainComplex.canonicalTruncationFiltration K₂)).1)

Stacks.Injectives.canonicalExtSpectralSequenceInto, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 116. The attribute's comment: “canonical_e1”.

Stacks 0G1Y. The Ext spectral sequence into the canonical truncation filtration F^pK^• = τ_{≤ -p}K^• of a cochain complex, a cohomological spectral sequence (E_r, d_r)_{r ≥ 1}.

def canonicalExtSpectralSequenceInto (M : DerivedCategory A) (K' : CochainComplex A ℤ) :
    CohomologicalSpectralSequence AddCommGrpCat.{v} 1

Stacks.Injectives.canonicalExtSpectralSequenceIntoE₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 141. The attribute's comment: “canonical_e1”. References: EGA 0 (11.4.3), “''E₂, T = Hom(M,-)”.

Stacks 0G1Y. For a representative K^• of K, the first page of the canonical Ext spectral sequence into K is E_1^{p, q} = Ext^{2p + q}(M, H^{-p}(K)). The degrees n = -p and m = 2p + q are arguments constrained by equations.

def canonicalExtSpectralSequenceIntoE₁ (M K : DerivedCategory A) (K' : CochainComplex A ℤ)
    (e : DerivedCategory.Q.obj K' ≅ K) (p q n m : ℤ) (hn : n = -p) (hm : m = 2 * p + q) :
    ((canonicalExtSpectralSequenceInto.{w', w} M K').page 1).X (p, q) ≃+
      DerivedCategory.Ext M ((DerivedCategory.singleFunctor A 0).obj
        ((DerivedCategory.homologyFunctor A n).obj K)) m

Stacks.Injectives.renumberedCanonicalExtSpectralSequenceInto, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 158. The attribute's comment: “renumbered_e2”.

Stacks 0G1Y. The canonical Ext spectral sequence into K, renumbered by (i, j) ↦ (-j, i + 2j) so that its first page becomes the second: a cohomological spectral sequence (E'_r, d'_r)_{r ≥ 2} whose differential on page r has bidegree (r, -r + 1).

def renumberedCanonicalExtSpectralSequenceInto (M : DerivedCategory A)
    (K' : CochainComplex A ℤ) :
    CohomologicalSpectralSequence AddCommGrpCat.{v} 2

Stacks.Injectives.renumberedCanonicalExtSpectralSequenceIntoE₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 166. The attribute's comment: “renumbered_e2”.

Stacks 0G1Y. For a representative K^• of K, the second page of the renumbered canonical Ext spectral sequence into K is (E'_2)^{i, j} = Ext^i(M, H^j(K)).

def renumberedCanonicalExtSpectralSequenceIntoE₂ (M K : DerivedCategory A)
    (K' : CochainComplex A ℤ) (e : DerivedCategory.Q.obj K' ≅ K) (i j : ℤ) :
    ((renumberedCanonicalExtSpectralSequenceInto.{w', w} M K').page 2).X (i, j) ≃+
      DerivedCategory.Ext M ((DerivedCategory.singleFunctor A 0).obj
        ((DerivedCategory.homologyFunctor A j).obj K)) i

Stacks.Injectives.stupidExtSpectralSequenceInto, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 180. The attribute's comment: “stupid_e1”.

Stacks 0G1Y. The Ext spectral sequence into the brutal truncation filtration F^pK^• = σ_{≥ p}K^• of a cochain complex, a cohomological spectral sequence (E_r, d_r)_{r ≥ 1}.

def stupidExtSpectralSequenceInto (M : DerivedCategory A) (K' : CochainComplex A ℤ) :
    CohomologicalSpectralSequence AddCommGrpCat.{v} 1

Stacks.Injectives.stupidExtSpectralSequenceIntoE₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 195. The attribute's comment: “stupid_e1”.

Stacks 0G1Y. The first page of the Ext spectral sequence of the brutal truncation filtration of K^• is E_1^{p, q} = Ext^q(M, K^p).

def stupidExtSpectralSequenceIntoE₁ (M : DerivedCategory A) (K' : CochainComplex A ℤ)
    (p q : ℤ) :
    ((stupidExtSpectralSequenceInto.{w', w} M K').page 1).X (p, q) ≃+
      DerivedCategory.Ext M ((DerivedCategory.singleFunctor A 0).obj (K'.X p)) q

Stacks.Injectives.stupidExtSpectralSequenceInto_isBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 272. The attribute's comment: “stupid_convergence”.

Stacks 0G1Y. If M is bounded above in the derived category and K^• is bounded below, the Ext spectral sequence of the brutal truncation filtration of K^• is bounded.

theorem stupidExtSpectralSequenceInto_isBounded (M : DerivedCategory A)
    (K' : CochainComplex A ℤ) (hM : DerivedCategory.TStructure.t.minus M)
    (hK : CochainComplex.plus A K') :
    IsBounded (stupidExtSpectralSequenceInto.{w', w} M K')

Stacks.Injectives.stupidExtSpectralSequenceInto_hasPageInfinityAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 282. The attribute's comment: “stupid_convergence”.

Stacks 0G1Y. Under the same hypotheses the brutal-truncation Ext spectral sequence has an infinity page at every bidegree.

theorem stupidExtSpectralSequenceInto_hasPageInfinityAt (M : DerivedCategory A)
    (K' : CochainComplex A ℤ) (hM : DerivedCategory.TStructure.t.minus M)
    (hK : CochainComplex.plus A K') (pq : ℤ × ℤ) :
    (stupidExtSpectralSequenceInto.{w', w} M K').HasPageInfinityAt pq

Stacks.Injectives.stupidExtSpectralSequenceInto_convergesToExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 296. The attribute's comment: “stupid_convergence”.

Stacks 0G1Y, convergence of the brutal-truncation spectral sequence. Under the same hypotheses it converges to Ext^{p + q}(M, K^•): the decreasing filtration Stacks.Injectives.extIntoFiltration of each Ext^n(M, K^•) is finite and the infinity page at (p, q) is its p-th graded piece in total degree p + q.

theorem stupidExtSpectralSequenceInto_convergesToExt (M : DerivedCategory A)
    (K' : CochainComplex A ℤ) (hM : DerivedCategory.TStructure.t.minus M)
    (hK : CochainComplex.plus A K') :
    let E := stupidExtSpectralSequenceInto.{w', w} M K'
    let F := extIntoFiltration M (CochainComplex.stupidTruncationFiltration K')
    ∃ hF : ∀ n : ℤ, Antitone (F n),
      (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ F n a = ⊤ ∧ F n b = ⊥) ∧
      (∀ p q : ℤ, E.HasPageInfinityAt (p, q)) ∧
      ∀ p q : ℤ, Nonempty
        ((E.pageInfinity (p, q) : Type v) ≃+
          ((Limits.cokernel (Subobject.ofLE (F (p + q) (p + 1)) (F (p + q) p)
              (hF (p + q) (by omega))) : AddCommGrpCat.{w}) : Type w))

Stacks.Injectives.canonicalExtSpectralSequenceInto_isBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 442. The attribute's comment: “canonical_convergence”.

Stacks 0G1Y, boundedness of the canonical spectral sequence. For M ∈ D^-(A) and K ∈ D^+(A) the Ext spectral sequence of the canonical truncation filtration of a complex representing K is bounded: in total degree d its first page E_1^{p, d - p} = Ext^{p + d}(M, H^{-p}(K)) vanishes unless -a - d ≤ p ≤ -b, where M lives in degrees ≤ a and K in degrees ≥ b.

theorem canonicalExtSpectralSequenceInto_isBounded (M K : DerivedCategory A)
    (K' : CochainComplex A ℤ) (e : DerivedCategory.Q.obj K' ≅ K)
    (hM : DerivedCategory.TStructure.t.minus M)
    (hK : DerivedCategory.TStructure.t.plus K) :
    IsBounded (canonicalExtSpectralSequenceInto.{w', w} M K')

Stacks.Injectives.canonicalExtSpectralSequenceInto_convergesToExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 482. The attribute's comment: “canonical_convergence”.

Stacks 0G1Y, convergence of the canonical spectral sequence. For M ∈ D^-(A) and K ∈ D^+(A) the Ext spectral sequence of the canonical truncation filtration converges to Ext^{p + q}(M, K): the decreasing filtration Stacks.Injectives.extIntoFiltration of each Ext^n(M, K) is finite and the infinity page at (p, q) is its p-th graded piece in total degree p + q.

theorem canonicalExtSpectralSequenceInto_convergesToExt (M K : DerivedCategory A)
    (K' : CochainComplex A ℤ) (e : DerivedCategory.Q.obj K' ≅ K)
    (hM : DerivedCategory.TStructure.t.minus M)
    (hK : DerivedCategory.TStructure.t.plus K) :
    let E := canonicalExtSpectralSequenceInto.{w', w} M K'
    let F := extIntoFiltration M (CochainComplex.canonicalTruncationFiltration K')
    ∃ hF : ∀ n : ℤ, Antitone (F n),
      (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ F n a = ⊤ ∧ F n b = ⊥) ∧
      (∀ p q : ℤ, E.HasPageInfinityAt (p, q)) ∧
      ∀ p q : ℤ, Nonempty
        ((E.pageInfinity (p, q) : Type v) ≃+
          ((Limits.cokernel (Subobject.ofLE (F (p + q) (p + 1)) (F (p + q) p)
              (hF (p + q) (by omega))) : AddCommGrpCat.{w}) : Type w))

Stacks.Injectives.renumberedCanonicalExtSpectralSequenceInto_isBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 503. The attribute's comment: “canonical_convergence”.

Stacks 0G1Y, boundedness after renumbering. For M ∈ D^-(A) and K ∈ D^+(A) the renumbered canonical Ext spectral sequence (E'_r, d'_r)_{r ≥ 2} is bounded.

theorem renumberedCanonicalExtSpectralSequenceInto_isBounded (M K : DerivedCategory A)
    (K' : CochainComplex A ℤ) (e : DerivedCategory.Q.obj K' ≅ K)
    (hM : DerivedCategory.TStructure.t.minus M)
    (hK : DerivedCategory.TStructure.t.plus K) :
    IsBounded (renumberedCanonicalExtSpectralSequenceInto.{w', w} M K')

Stacks.Injectives.renumberedCanonicalExtSpectralSequenceInto_convergesToExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/TruncationFiltrationSpectralSequences.lean, line 516. The attribute's comment: “canonical_convergence”.

Stacks 0G1Y, convergence after renumbering. For M ∈ D^-(A) and K ∈ D^+(A) the renumbered canonical Ext spectral sequence converges to Ext^{i + j}(M, K): the infinity page at (i, j) is the graded piece of Stacks.Injectives.extIntoFiltration from -j + 1 to -j in total degree i + j.

theorem renumberedCanonicalExtSpectralSequenceInto_convergesToExt (M K : DerivedCategory A)
    (K' : CochainComplex A ℤ) (e : DerivedCategory.Q.obj K' ≅ K)
    (hM : DerivedCategory.TStructure.t.minus M)
    (hK : DerivedCategory.TStructure.t.plus K) :
    let E := renumberedCanonicalExtSpectralSequenceInto.{w', w} M K'
    let F := extIntoFiltration M (CochainComplex.canonicalTruncationFiltration K')
    ∃ hF : ∀ n : ℤ, Antitone (F n),
      (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ F n a = ⊤ ∧ F n b = ⊥) ∧
      (∀ i j : ℤ, E.HasPageInfinityAt (i, j)) ∧
      ∀ i j : ℤ, Nonempty
        ((E.pageInfinity (i, j) : Type v) ≃+
          ((Limits.cokernel (Subobject.ofLE (F (i + j) (-j + 1)) (F (i + j) (-j))
              (hF (i + j) (by omega))) : AddCommGrpCat.{w}) : Type w))

Tag 0G1Z, a remark

Tag 0G1Z in the Stacks Project.

Stacks.Injectives.extSpectralSequence_isBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/ExtBoundedConvergence.lean, line 530. The attribute's comment: “boundedness”.

Stacks 0G1Z, boundedness. Under eventual vanishing and eventual comparison-isomorphism for Ext from the filtered quotients, the Ext spectral sequence is bounded.

public theorem extSpectralSequence_isBounded
    {A : Type u} [Category.{v} A] [Abelian A]
    [IsGrothendieckAbelian.{w} A] [HasDerivedCategory.{w} A]
    (K : DerivedCategory A) (M : CochainComplex.Filtered A)
    (hzero : ∀ n : ℤ, ∃ p₀ : ℤ, ∀ p : ℤ, p ≤ p₀ →
      IsZero (AddCommGrpCat.of (DerivedCategory.Ext
        (DerivedCategory.Q.obj ((FilteredObject.quot (op p)).obj M)) K n)))
    (hiso : ∀ n : ℤ, ∃ p₁ : ℤ, ∀ p : ℤ, p₁ ≤ p →
      IsIso (extFromFilteredQuotient K M p n)) :
    IsBounded (extSpectralSequence K M).1

Stacks.Injectives.extSpectralSequence_convergesToExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/ExtBoundedConvergence.lean, line 548. The attribute's comment: “convergence”.

Stacks 0G1Z, convergence. Under eventual vanishing and eventual comparison-isomorphism for Ext from the filtered quotients, the Ext spectral sequence converges to the Ext groups from the underlying complex, with the canonical quotient-image filtration. The graded quotient at (p,q) is the step from -p to -p + 1.

public theorem extSpectralSequence_convergesToExt
    {A : Type u} [Category.{v} A] [Abelian A]
    [IsGrothendieckAbelian.{w} A] [HasDerivedCategory.{w} A]
    (K : DerivedCategory A) (M : CochainComplex.Filtered A)
    (hzero : ∀ n : ℤ, ∃ p₀ : ℤ, ∀ p : ℤ, p ≤ p₀ →
      IsZero (AddCommGrpCat.of (DerivedCategory.Ext
        (DerivedCategory.Q.obj ((FilteredObject.quot (op p)).obj M)) K n)))
    (hiso : ∀ n : ℤ, ∃ p₁ : ℤ, ∀ p : ℤ, p₁ ≤ p →
      IsIso (extFromFilteredQuotient K M p n)) :
    let E := (extSpectralSequence K M).1
    ∃ hF : ∀ n : ℤ, Monotone (extQuotientFiltration K M n),
      (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ extQuotientFiltration K M n a = ⊥ ∧
        extQuotientFiltration K M n b = ⊤) ∧
      (∀ p q : ℤ, E.HasPageInfinityAt (p, q)) ∧
      ∀ p q : ℤ, Nonempty
        (E.pageInfinity (p, q) ≅
          cokernel (Subobject.ofLE (extQuotientFiltration K M (p + q) (-p))
            (extQuotientFiltration K M (p + q) (-p + 1)) (hF (p + q) (by omega))))

Stacks.Injectives.extSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/SpectralSequenceOfFilteredComplex.lean, line 234. The attribute's comment: “spectral_sequence”.

Stacks 0G1Z. The Ext spectral sequence associated to a filtered complex M, bundled with the identifications E₁^{p,q} = Ext^{p+q}(gr^{-p} M, K). Its differential on page r has bidegree (r, -r + 1) by the definition of CohomologicalSpectralSequence.

noncomputable def extSpectralSequence
    {A : Type u} [Category.{v} A] [Abelian A]
    [IsGrothendieckAbelian.{w} A] [HasDerivedCategory.{w} A]
    (K : DerivedCategory A) (M : CochainComplex.Filtered A) :
    Σ E : CohomologicalSpectralSequence AddCommGrpCat.{w} 1,
      ∀ p q : ℤ,
        (E.page 1).X (p, q) ≅ AddCommGrpCat.of
          (DerivedCategory.Ext
            (DerivedCategory.Q.obj
              ((FilteredObject.gr (C := (CochainComplex A ℤ)) (-p)).obj M))
            K (p + q))

Tag 0G20, a remark

Tag 0G20 in the Stacks Project.

Stacks.Injectives.renumberedCanonicalExtSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/CanonicalExtConvergence.lean, line 80. The attribute's comment: “renumbered_e2”.

0G20 renumbered_e2, declaration 1.

public noncomputable def renumberedCanonicalExtSpectralSequence
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    {M K : DerivedCategory A} {M' : CochainComplex A ℤ}
    {e : DerivedCategory.Q.obj M' ≅ M}
    (S : CanonicalExtSpectralSequence M K M' e) :
    CohomologicalSpectralSequence AddCommGrpCat.{w} 2

Stacks.Injectives.renumberedCanonicalExtSpectralSequence_page_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/CanonicalExtConvergence.lean, line 91. The attribute's comment: “renumbered_e2”.

0G20 renumbered_e2, declaration 2.

public theorem renumberedCanonicalExtSpectralSequence_page_two
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    {M K : DerivedCategory A} {M' : CochainComplex A ℤ}
    {e : DerivedCategory.Q.obj M' ≅ M}
    (S : CanonicalExtSpectralSequence M K M' e) (i j : ℤ) :
    Nonempty
      (((renumberedCanonicalExtSpectralSequence S).page 2).X (i, j) ≅
        AddCommGrpCat.of
          (DerivedCategory.Ext ((DerivedCategory.singleFunctor A 0).obj
            ((DerivedCategory.homologyFunctor A (-j)).obj M)) K i))

Stacks.Injectives.canonicalExtSpectralSequence_isBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/CanonicalExtConvergence.lean, line 277. The attribute's comment: “canonical_convergence”.

Stacks 0G20, boundedness before renumbering. For M ∈ D⁻(A) and K ∈ D⁺(A), the canonical Ext spectral sequence is bounded.

public theorem canonicalExtSpectralSequence_isBounded
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    {M K : DerivedCategory A} {M' : CochainComplex A ℤ}
    {e : DerivedCategory.Q.obj M' ≅ M}
    (S : CanonicalExtSpectralSequence M K M' e)
    (hM : (DerivedCategory.TStructure.t (C := A)).minus M)
    (hK : (DerivedCategory.TStructure.t (C := A)).plus K) :
    IsBounded S.spectralSequence

Stacks.Injectives.canonicalExtSpectralSequence_convergesToExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/CanonicalExtConvergence.lean, line 309. The attribute's comment: “canonical_convergence”.

Stacks 0G20, convergence before renumbering. For M ∈ D⁻(A) and K ∈ D⁺(A), the canonical Ext spectral sequence converges to Ext^(p+q)(M, K), with filtration index -p.

public theorem canonicalExtSpectralSequence_convergesToExt
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    {M K : DerivedCategory A} {M' : CochainComplex A ℤ}
    {e : DerivedCategory.Q.obj M' ≅ M}
    (S : CanonicalExtSpectralSequence M K M' e)
    (hM : (DerivedCategory.TStructure.t (C := A)).minus M)
    (hK : (DerivedCategory.TStructure.t (C := A)).plus K) :
    let E := S.spectralSequence
    ∃ hF : ∀ n : ℤ, Monotone (canonicalExtFiltration S n),
      (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ canonicalExtFiltration S n a = ⊥ ∧
        canonicalExtFiltration S n b = ⊤) ∧
      (∀ p q : ℤ, E.HasPageInfinityAt (p, q)) ∧
      ∀ p q : ℤ, Nonempty
      (E.pageInfinity (p, q) ≅
          cokernel (Subobject.ofLE (canonicalExtFiltration S (p + q) (-p))
            (canonicalExtFiltration S (p + q) (-p + 1)) (hF (p + q) (by omega))))

Stacks.Injectives.renumberedCanonicalExtSpectralSequence_isBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/CanonicalExtConvergence.lean, line 358. The attribute's comment: “canonical_convergence”.

Stacks 0G20, boundedness after renumbering. For M ∈ D⁻(A) and K ∈ D⁺(A), the renumbered canonical Ext spectral sequence is bounded.

public theorem renumberedCanonicalExtSpectralSequence_isBounded
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    {M K : DerivedCategory A} {M' : CochainComplex A ℤ}
    {e : DerivedCategory.Q.obj M' ≅ M}
    (S : CanonicalExtSpectralSequence M K M' e)
    (hM : (DerivedCategory.TStructure.t (C := A)).minus M)
    (hK : (DerivedCategory.TStructure.t (C := A)).plus K) :
    IsBounded
      (renumberedCanonicalExtSpectralSequence S)

Stacks.Injectives.renumberedCanonicalExtSpectralSequence_convergesToExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/CanonicalExtConvergence.lean, line 375. The attribute's comment: “canonical_convergence”.

Stacks 0G20, convergence after renumbering. For M ∈ D⁻(A) and K ∈ D⁺(A), the renumbered canonical Ext spectral sequence converges to Ext^(i+j)(M, K), with filtration index j.

public theorem renumberedCanonicalExtSpectralSequence_convergesToExt
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    {M K : DerivedCategory A} {M' : CochainComplex A ℤ}
    {e : DerivedCategory.Q.obj M' ≅ M}
    (S : CanonicalExtSpectralSequence M K M' e)
    (hM : (DerivedCategory.TStructure.t (C := A)).minus M)
    (hK : (DerivedCategory.TStructure.t (C := A)).plus K) :
    let E := renumberedCanonicalExtSpectralSequence S
    ∃ hF : ∀ n : ℤ, Monotone (canonicalExtFiltration S n),
      (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ canonicalExtFiltration S n a = ⊥ ∧
        canonicalExtFiltration S n b = ⊤) ∧
      (∀ i j : ℤ, E.HasPageInfinityAt (i, j)) ∧
      ∀ i j : ℤ, Nonempty
        (E.pageInfinity (i, j) ≅
          cokernel (Subobject.ofLE (canonicalExtFiltration S (i + j) j)
            (canonicalExtFiltration S (i + j) (j + 1)) (hF (i + j) (by omega))))

Stacks.Injectives.isBounded_canonicalExtSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/CanonicalExtConvergence.lean, line 414. The attribute's comment: “canonical_convergence”.

Stacks 0G20, boundedness of the canonical Ext spectral sequence. For M ∈ D⁻(A) and K ∈ D⁺(A), the Ext spectral sequence of the canonical truncation filtration F^p M^• = τ_{≤ -p} M^• of a complex M^• representing M is bounded. This is canonicalExtSpectralSequence_isBounded at the filtration itself.

public theorem isBounded_canonicalExtSpectralSequence
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    (M K : DerivedCategory A) (M' : CochainComplex A ℤ)
    (e : DerivedCategory.Q.obj M' ≅ M)
    (hM : (DerivedCategory.TStructure.t (C := A)).minus M)
    (hK : (DerivedCategory.TStructure.t (C := A)).plus K) :
    IsBounded (canonicalExtSpectralSequence M K M' e).spectralSequence

Stacks.Injectives.convergesToExt_canonicalExtSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/CanonicalExtConvergence.lean, line 430. The attribute's comment: “canonical_convergence”.

Stacks 0G20, convergence of the canonical Ext spectral sequence. For M ∈ D⁻(A) and K ∈ D⁺(A), the Ext spectral sequence of the canonical truncation filtration F^p M^• = τ_{≤ -p} M^• of a complex M^• representing M converges to Ext^{p+q}(M, K), with filtration index -p. This is canonicalExtSpectralSequence_convergesToExt at the filtration itself.

public theorem convergesToExt_canonicalExtSpectralSequence
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    (M K : DerivedCategory A) (M' : CochainComplex A ℤ)
    (e : DerivedCategory.Q.obj M' ≅ M)
    (hM : (DerivedCategory.TStructure.t (C := A)).minus M)
    (hK : (DerivedCategory.TStructure.t (C := A)).plus K) :
    let S := canonicalExtSpectralSequence M K M' e
    let E := S.spectralSequence
    ∃ hF : ∀ n : ℤ, Monotone (canonicalExtFiltration S n),
      (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ canonicalExtFiltration S n a = ⊥ ∧
        canonicalExtFiltration S n b = ⊤) ∧
      (∀ p q : ℤ, E.HasPageInfinityAt (p, q)) ∧
      ∀ p q : ℤ, Nonempty
      (E.pageInfinity (p, q) ≅
          cokernel (Subobject.ofLE (canonicalExtFiltration S (p + q) (-p))
            (canonicalExtFiltration S (p + q) (-p + 1)) (hF (p + q) (by omega))))

Stacks.Injectives.stupidExtSpectralSequence_isBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/CanonicalExtConvergence.lean, line 548. The attribute's comment: “stupid_convergence”.

Stacks 0G20, boundedness of the brutal-truncation Ext spectral sequence. If K ∈ D⁺(A) and the cochain complex M^• is bounded above, the Ext spectral sequence of the filtration F^p M^• = σ_{≥ p} M^• is bounded.

public theorem stupidExtSpectralSequence_isBounded
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    (K : DerivedCategory A) (M' : CochainComplex A ℤ)
    (hK : (DerivedCategory.TStructure.t (C := A)).plus K)
    (hM : CochainComplex.minus A M') :
    IsBounded (stupidExtSpectralSequence K M')

Stacks.Injectives.stupidExtSpectralSequence_convergesToExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/SpectralSequence/CanonicalExtConvergence.lean, line 563. The attribute's comment: “stupid_convergence”.

Stacks 0G20, convergence of the brutal-truncation Ext spectral sequence. If K ∈ D⁺(A) and the cochain complex M^• is bounded above, the Ext spectral sequence of the filtration F^p M^• = σ_{≥ p} M^• converges to Ext^{p+q}(M^•, K), the Ext groups of the object M of the derived category represented by M^•, with filtration index -p.

public theorem stupidExtSpectralSequence_convergesToExt
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    (K : DerivedCategory A) (M' : CochainComplex A ℤ)
    (hK : (DerivedCategory.TStructure.t (C := A)).plus K)
    (hM : CochainComplex.minus A M') :
    let E := stupidExtSpectralSequence K M'
    ∃ hF : ∀ n : ℤ, Monotone
        (extQuotientFiltration K (CochainComplex.stupidTruncationFiltration M') n),
      (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧
        extQuotientFiltration K (CochainComplex.stupidTruncationFiltration M') n a = ⊥ ∧
        extQuotientFiltration K (CochainComplex.stupidTruncationFiltration M') n b = ⊤) ∧
      (∀ p q : ℤ, E.HasPageInfinityAt (p, q)) ∧
      ∀ p q : ℤ, Nonempty
        (E.pageInfinity (p, q) ≅
          cokernel (Subobject.ofLE
            (extQuotientFiltration K
              (CochainComplex.stupidTruncationFiltration M') (p + q) (-p))
            (extQuotientFiltration K
              (CochainComplex.stupidTruncationFiltration M') (p + q) (-p + 1))
            (hF (p + q) (by omega))))

Stacks.Injectives.canonicalExtSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/CanonicalSpectralSequence.lean, line 142. The attribute's comment: “canonical_e1”.

Stacks 0G20, the canonical truncation filtration. Let A be a Grothendieck abelian category and let M, K ∈ D(A). Every cochain complex representing M, filtered by F^p M^• = τ_{≤ -p} M^•, gives a cohomological spectral sequence whose first page is E₁^{p,q} = Ext^{2p+q}(H^p(M), K).

noncomputable def canonicalExtSpectralSequence
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    (M K : DerivedCategory A) (M' : CochainComplex A ℤ)
    (e : DerivedCategory.Q.obj M' ≅ M) :
    CanonicalExtSpectralSequence M K M' e

Stacks.Injectives.exists_canonicalExtSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/CanonicalSpectralSequence.lean, line 169. The attribute's comment: “canonical_e1”.

Stacks 0G20, the canonical truncation filtration. Let A be a Grothendieck abelian category and let M, K ∈ D(A). Every cochain complex representing M, filtered by F^p M^• = τ_{≤ -p} M^•, gives a cohomological spectral sequence whose first page is E₁^{p,q} = Ext^{2p+q}(H^p(M), K). This is canonicalExtSpectralSequence forgetting the construction.

theorem exists_canonicalExtSpectralSequence
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    (M K : DerivedCategory A) (M' : CochainComplex A ℤ)
    (e : DerivedCategory.Q.obj M' ≅ M) :
    Nonempty (CanonicalExtSpectralSequence M K M' e)

Stacks.Injectives.stupidExtSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/CanonicalSpectralSequence.lean, line 182. The attribute's comment: “stupid_e1”.

Stacks 0G20, the brutal truncation filtration. The Ext spectral sequence of the filtration F^p M^• = σ_{≥ p} M^• of a cochain complex M^•, a cohomological spectral sequence (E_r, d_r)_{r ≥ 1}. It is definitionally the construction of Tag 0G1Z applied to that filtered complex, so every page, differential and page-turning isomorphism is specified.

noncomputable def stupidExtSpectralSequence
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    (K : DerivedCategory A) (M' : CochainComplex A ℤ) :
    CohomologicalSpectralSequence AddCommGrpCat.{w} 1

Stacks.Injectives.stupidExtSpectralSequenceE₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/CanonicalSpectralSequence.lean, line 195. The attribute's comment: “stupid_e1”.

Stacks 0G20, the brutal truncation filtration. The first page of the Ext spectral sequence of the filtration F^p M^• = σ_{≥ p} M^• is E₁^{p,q} = Ext^q(M^{-p}, K).

The index is -p, not p: the first page at (p, q) is Ext^{p+q} of the graded piece gr^{-p}M^• = M^{-p}[p], and the shift moves p + q down to q.

noncomputable def stupidExtSpectralSequenceE₁
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A]
    (K : DerivedCategory A) (M' : CochainComplex A ℤ) (p q : ℤ) :
    ((stupidExtSpectralSequence K M').page 1).X (p, q) ≅
      AddCommGrpCat.of (DerivedCategory.Ext
        ((DerivedCategory.singleFunctor A 0).obj (M'.X (-p))) K q)

Stacks.Injectives.canonicalExtSpectralSequence_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/Ext/CanonicalSpectralSequence.lean, line 420. The attribute's comment: “representative_independence”.

The canonical-truncation Ext spectral sequence is independent of the choice of complex representing M, as a spectral sequence from E₁ onward.

theorem canonicalExtSpectralSequence_iso
    {A : Type u} [Category.{v} A] [Abelian A] [HasDerivedCategory.{w} A]
    [IsGrothendieckAbelian.{w} A] (M K : DerivedCategory A)
    (M₁ M₂ : CochainComplex A ℤ)
    (e₁ : DerivedCategory.Q.obj M₁ ≅ M) (e₂ : DerivedCategory.Q.obj M₂ ≅ M)
    (S₁ : CanonicalExtSpectralSequence M K M₁ e₁)
    (S₂ : CanonicalExtSpectralSequence M K M₂ e₂) :
    Nonempty (S₁.spectralSequence ≅ S₂.spectralSequence)

Tag 0ESJ, a lemma

Tag 0ESJ in the Stacks Project.

Stacks.Injectives.exists_filteredComplex_representation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/FilteredComplex/InverseSystemRepresentation.lean, line 989.

Let A be a Grothendieck abelian category, E an object of D(A), and F an inverse system of objects of D(A) indexed by ℤᵒᵖ together with a compatible family of maps φ from F to the constant system at E. Then there is a filtered cochain complex K whose underlying complex represents E, whose derived filtration diagram is isomorphic to F, and whose filtration inclusions induce the maps φ.

theorem exists_filteredComplex_representation
    (E : DerivedCategory A) (F : ℤᵒᵖ ⥤ DerivedCategory A)
    (φ : F ⟶ (Functor.const ℤᵒᵖ).obj E) :
    ∃ (K : CochainComplex.Filtered A)
      (e : DerivedCategory.Q.obj K.X ≅ E)
      (η : K.filtration.diagram ⋙ DerivedCategory.Q ≅ F),
      ∀ i : ℤᵒᵖ,
        DerivedCategory.Q.map (K.filtration.ι.app i) ≫ e.hom =
          η.hom.app i ≫ φ.app i

Tag 0ESK, a lemma

Tag 0ESK in the Stacks Project.

Stacks.Injectives.exists_bifilteredComplex_representation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Grothendieck/BifilteredRepresentation.lean, line 208.

Stacks 0ESK. Two inverse systems of objects of the derived category of a Grothendieck abelian category, each with a compatible family of maps to one object E, can be represented by two filtrations of a single cochain complex.

theorem exists_bifilteredComplex_representation
    (E : DerivedCategory A)
    (F F' : ℤᵒᵖ ⥤ DerivedCategory A)
    (φ : F ⟶ (Functor.const ℤᵒᵖ).obj E)
    (φ' : F' ⟶ (Functor.const ℤᵒᵖ).obj E) :
    ∃ (K : CochainComplex.Filtered A)
      (filtration' : Filtration K.X ℤᵒᵖ)
      (e : DerivedCategory.Q.obj K.X ≅ E)
      (η : K.filtration.diagram ⋙ DerivedCategory.Q ≅ F)
      (η' : filtration'.diagram ⋙ DerivedCategory.Q ≅ F'),
      (∀ i : ℤᵒᵖ,
        DerivedCategory.Q.map (K.filtration.ι.app i) ≫ e.hom =
          η.hom.app i ≫ φ.app i) ∧
      (∀ i : ℤᵒᵖ,
        DerivedCategory.Q.map (filtration'.ι.app i) ≫ e.hom =
          η'.hom.app i ≫ φ'.app i)

Sources

LeanStacks.Injectives.isRepresentable_iff_preservesLimits · Stacks.Injectives.hasProducts_of_isGrothendieckAbelian · Stacks.Injectives.kInjectiveResolutionHomMap_bijective · Stacks.Injectives.hasDerivedCategory_of_isGrothendieckAbelian · instIsGrothendieckAbelianModuleCat · SheafOfModules.instIsGrothendieckAbelian · Stacks.Injectives.isLimit_productFanInDerivedCategory · Stacks.Injectives.derivedCategoryQ_preservesCoproducts

Section19.14 The Gabriel-Popescu theorem #

Section 19.14 of the Stacks Project, Tag 0F5R. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0F5S, a lemma

Tag 0F5S in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.IsGrothendieckAbelian.tensorObjPreadditiveCoyonedaObjAdjunction registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch19.lean, line 24 (StacksFrontier): “the left adjoint - ⊗ G of Hom(G, -) into right End(G)-modules”.

Tag 0F5T, a lemma

Tag 0F5T in the Stacks Project.

Stacks.Injectives.mono_homEquiv_symm_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/GabrielPopescuMono.lean, line 29.

Let G be a separator of a Grothendieck abelian category. If a map of (End G)ᵐᵒᵖ-modules f : M ⟶ Hom(G, A) is a monomorphism, equivalently injective, then the map M ⊗ G ⟶ A adjoint to it is a monomorphism as well.

theorem mono_homEquiv_symm_of_mono (G : C) (hG : IsSeparator G)
    {M : ModuleCat (End G)ᵐᵒᵖ} {A : C} (f : M ⟶ (preadditiveCoyonedaObj G).obj A) (hf : Mono f) :
    Mono (((tensorObjPreadditiveCoyonedaObjAdjunction G).homEquiv M A).symm f)

Tag 0F5U, a theorem

Tag 0F5U in the Stacks Project.

Stacks.Injectives.preadditiveCoyonedaObjFullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/GabrielPopescuEmbedding.lean, line 32. The attribute's comment: “(2) for the constructed functor Hom(G, -)”.

Let G be a separator of a Grothendieck abelian category C. The embedding Hom(G, -) : C ⥤ Mod (End G)ᵐᵒᵖ is fully faithful.

noncomputable def preadditiveCoyonedaObjFullyFaithful (G : C) (hG : IsSeparator G) :
    (preadditiveCoyonedaObj G).FullyFaithful

Stacks.Injectives.preservesFiniteLimits_and_preservesFiniteColimits_tensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/GabrielPopescuEmbedding.lean, line 43. The attribute's comment: “(3) for the constructed functor - ⊗ G”.

Let G be a separator of a Grothendieck abelian category C. The left adjoint - ⊗ G : Mod (End G)ᵐᵒᵖ ⥤ C of the embedding Hom(G, -) is exact: it preserves finite limits, and it preserves finite colimits because it is a left adjoint.

theorem preservesFiniteLimits_and_preservesFiniteColimits_tensorObj (G : C)
    (hG : IsSeparator G) :
    PreservesFiniteLimits (tensorObj G) ∧ PreservesFiniteColimits (tensorObj G)

Stacks.Injectives.gabriel_popescu, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/GabrielPopescuEmbedding.lean, line 52.

The Gabriel--Popescu theorem. For a Grothendieck abelian category C there is a possibly noncommutative ring R together with functors G : C ⥤ Mod R and F : Mod R ⥤ C such that F is left adjoint to G, G is fully faithful, and F is exact.

theorem gabriel_popescu (C : Type u) [Category.{v} C] [Abelian C]
    [IsGrothendieckAbelian.{v} C] :
    ∃ (R : Type v) (_ : Ring R) (G : C ⥤ ModuleCat.{v} R) (F : ModuleCat.{v} R ⥤ C),
      Nonempty (F ⊣ G) ∧ G.Full ∧ G.Faithful ∧
        PreservesFiniteLimits F ∧ PreservesFiniteColimits F

Declarations registered for the tag:

CategoryTheory.IsGrothendieckAbelian.tensorObjPreadditiveCoyonedaObjAdjunction registered with add_to_stacks in StacksFrontier/Homology/Injectives/GabrielPopescuEmbedding.lean, line 26 (StacksFrontier): “(1) for the constructed functors: - ⊗ G is left adjoint to Hom(G, -)”.

Tag 0F5V, a lemma

Tag 0F5V in the Stacks Project.

Stacks.Injectives.exists_derivedGabrielPopescuData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/GabrielPopescu.lean, line 270.

Stacks 0F5V (Gabriel--Popescu on derived categories). The Gabriel--Popescu embedding of a Grothendieck abelian category admits a fully faithful right derived functor. Its left adjoint is induced by the exact Gabriel--Popescu left adjoint, and the counit is an isomorphism.

theorem exists_derivedGabrielPopescuData (G : C) (hG : IsSeparator G) :
    Nonempty (DerivedGabrielPopescuData G hG)

Sources

LeanCategoryTheory.IsGrothendieckAbelian.tensorObjPreadditiveCoyonedaObjAdjunction · Stacks.Injectives.mono_homEquiv_symm_of_mono · Stacks.Injectives.preadditiveCoyonedaObjFullyFaithful · Stacks.Injectives.preservesFiniteLimits_and_preservesFiniteColimits_tensorObj · Stacks.Injectives.gabriel_popescu · Stacks.Injectives.exists_derivedGabrielPopescuData

Section19.15 Brown representability and Grothendieck abelian categories #

Section 19.15 of the Stacks Project, Tag 0F5W. 2 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0F5X, a lemma

Tag 0F5X in the Stacks Project.

Stacks.Injectives.isRepresentable_of_isGrothendieckAbelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/BrownRepresentability.lean, line 454.

Stacks 0F5X (Brown representability for Grothendieck abelian categories). Let A be a Grothendieck abelian category and H : D(A) ⥤ Ab a contravariant cohomological functor which transforms direct sums into products. Then H is representable.

public theorem isRepresentable_of_isGrothendieckAbelian (A : Type u) [Category.{v} A] [Abelian A]
    [IsGrothendieckAbelian.{max w u v} A] [HasDerivedCategory.{z} A]
    (H : (DerivedCategory A)ᵒᵖ ⥤ AddCommGrpCat.{max u v}) [H.IsHomological]
    [∀ J : Type (max w u v), PreservesLimitsOfShape (Discrete J) H] :
    (H ⋙ forget AddCommGrpCat).IsRepresentable

Tag 0F5Y, a proposition

Tag 0F5Y in the Stacks Project.

Stacks.Injectives.exists_exact_rightAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/BrownRepresentability.lean, line 478.

Stacks 0F5Y. Let A be a Grothendieck abelian category and D a triangulated category. An exact functor F : D(A) ⥤ D which transforms direct sums into direct sums has an exact right adjoint: a functor G, an adjunction F ⊣ G, and a commutation of G with the shift making G triangulated.

public theorem exists_exact_rightAdjoint (A : Type u) [Category.{v} A] [Abelian A]
    [IsGrothendieckAbelian.{max w u v} A] [HasDerivedCategory.{z} A]
    (D : Type u') [Category.{max u v} D] [HasZeroObject D] [HasShift D ℤ] [Preadditive D]
    [∀ n : ℤ, (shiftFunctor D n).Additive] [Pretriangulated D]
    (F : DerivedCategory A ⥤ D) [F.CommShift ℤ] [F.IsTriangulated]
    [∀ J : Type (max w u v), PreservesColimitsOfShape (Discrete J) F] :
    ∃ (G : D ⥤ DerivedCategory A) (_ : F ⊣ G) (commShift : G.CommShift ℤ),
      let := commShift
      G.IsTriangulated

Stacks.Injectives.exists_exact_rightAdjoint_of_isGrothendieckAbelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Injectives/BrownRepresentabilityRightAdjoint.lean, line 121. The attribute's comment: “A Grothendieck abelian relative to its morphism universe, direct sums indexed by it; the base exists_exact_rightAdjoint assumes IsGrothendieckAbelian at the object universe, which no nonzero category satisfies”.

[Stacks, Tag 0F5Y]. Let A be a Grothendieck abelian category and D a pretriangulated category. An exact functor F : D(A) ⥤ D which transforms direct sums into direct sums, and whose morphism groups Hom(F W, Y) are small, has an exact right adjoint: a functor G, an adjunction F ⊣ G, and a commutation of G with the shift making G triangulated.

Here A is Grothendieck abelian relative to its morphism universe v and the direct sums are indexed by Type v. The smallness of Hom(F W, Y) is the source's standing convention that morphisms form sets, read at that universe. It is also necessary: if F ⊣ G, then Hom(F W, Y) ≃ Hom(W, G Y), and the derived category of A is locally Type v-small.

theorem exists_exact_rightAdjoint_of_isGrothendieckAbelian
    (hsmall : ∀ (W : DerivedCategory A) (Y : D), Small.{v} (F.obj W ⟶ Y)) :
    ∃ (G : D ⥤ DerivedCategory A) (_ : F ⊣ G) (commShift : G.CommShift ℤ),
      letI := commShift
      G.IsTriangulated

Sources

LeanStacks.Injectives.isRepresentable_of_isGrothendieckAbelian · Stacks.Injectives.exists_exact_rightAdjoint · Stacks.Injectives.exists_exact_rightAdjoint_of_isGrothendieckAbelian

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

19 Injectives

Section19.2 Baer's argument for modules#

Tag 05NN, an equation

Tag 05NR, a lemma

Tag 05NS, a definition

Tag 05NT, a proposition

Tag 05NU, a lemma

Tag 05NV, an equation

Tag 05NW, a lemma

Tag 05NX, a theorem

Sources

Section19.3 G-modules#

Tag 04JF, a lemma

Sources

Section19.4 Abelian sheaves on a space#

Tag 01DG, a lemma

Sources

Section19.5 Sheaves of modules on a ringed space#

Tag 01DI, a lemma

Sources

Section19.6 Abelian presheaves on a category#

Tag 01DK, a proposition

Sources

Section19.7 Abelian Sheaves on a site#

Tag 01DM, a lemma

Tag 01DN, a lemma

Tag 05NY, an equation

Tag 01DO, a lemma

Tag 01DP, a theorem

Sources

Section19.8 Modules on a ringed site#

Tag 01DR, a lemma

Tag 01DS, a lemma

Tag 01DT, a lemma

Tag 01DU, a theorem

Tag 01DV, a proposition

Sources

Section19.9 Embedding abelian categories#

Tag 05PM, a lemma

Tag 05PN, a lemma

Tag 05PP, a remark

Tag 05PQ, a remark

Tag 05PR, a remark

Sources

Section19.10 Grothendieck's AB conditions#

Tag 079B, a definition

Sources

Section19.11 Injectives in Grothendieck categories#

Tag 0E8N, a lemma

Tag 079C, a definition

Tag 079D, a lemma

Tag 079E, a lemma

Tag 079F, a proposition

Tag 079G, a lemma

Tag 079H, a theorem

Sources

Section19.12 K-injectives in Grothendieck categories#

Tag 079J, a lemma

Tag 079K, a lemma

Tag 079L, a lemma

Tag 079M, a lemma

Tag 079N, a lemma

Tag 079P, a theorem

Sources

Section19.13 Additional remarks on Grothendieck abelian categories#

Tag 07D7, a lemma

Tag 07D8, a lemma

Tag 079Q, a remark

Tag 07D9, a lemma

Tag 08U1, a lemma

Tag 0BKI, a lemma

Tag 0G1X, a remark

Tag 0G1Y, a remark

Tag 0G1Z, a remark

Tag 0G20, a remark

Tag 0ESJ, a lemma

Tag 0ESK, a lemma

Sources

Section19.14 The Gabriel-Popescu theorem#

Tag 0F5S, a lemma

Section19.2 Baer's argument for modules #

Section19.3 G-modules #

Section19.4 Abelian sheaves on a space #

Section19.5 Sheaves of modules on a ringed space #

Section19.6 Abelian presheaves on a category #

Section19.7 Abelian Sheaves on a site #

Section19.8 Modules on a ringed site #

Section19.9 Embedding abelian categories #

Section19.10 Grothendieck's AB conditions #

Section19.11 Injectives in Grothendieck categories #

Section19.12 K-injectives in Grothendieck categories #

Section19.13 Additional remarks on Grothendieck abelian categories #

Section19.14 The Gabriel-Popescu theorem #

Section19.15 Brown representability and Grothendieck abelian categories #