47.2 Essential surjections and… to 47.18 The local duality theorem

Section47.2 Essential surjections and injections #

Section 47.2 of the Stacks Project, Tag 08XI. 4 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08XJ, a definition

Tag 08XJ in the Stacks Project.

Module.IsEssentialEpi, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Essential.lean, line 71. The attribute's comment: “essential_surjection”.

A morphism is an essential epimorphism if it is an epimorphism and the direct image of every proper subobject of its source is proper.

abbrev IsEssentialEpi {C : Type u} [Category.{v} C] [HasImages C] {X Y : C} (f : X ⟶ Y) : Prop

Module.IsEssentialMono, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Essential.lean, line 77. The attribute's comment: “essential_injection”.

A monomorphism is essential if every nonzero subobject of its codomain has nonzero intersection with its image.

abbrev IsEssentialMono {𝒜 : Type u} [Category.{v} 𝒜] [HasZeroObject 𝒜] [HasPullbacks 𝒜]
    {A B : 𝒜} (i : A ⟶ B) [Mono i] : Prop

Tag 08XK, a lemma

Tag 08XK in the Stacks Project.

Module.isEssentialEpi_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Essential.lean, line 112. The attribute's comment: “essential_surjection_comp”.

The composite of two essential epimorphisms is an essential epimorphism.

theorem isEssentialEpi_comp [HasImages 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C}
    (hf : IsEssentialEpi f) (hg : IsEssentialEpi g) : IsEssentialEpi (f ≫ g)

Module.isEssentialMono_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Essential.lean, line 137. The attribute's comment: “essential_extension_trans”.

The composite of two essential monomorphisms is essential.

theorem isEssentialMono_comp {A B C : 𝒜} (i : A ⟶ B) (j : B ⟶ C) [Mono i] [Mono j]
    (hi : IsEssentialMono i) (hj : IsEssentialMono j) : IsEssentialMono (i ≫ j)

Module.isEssentialMono_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Essential.lean, line 155. The attribute's comment: “essential_extension_intersection”.

The intersection of an essential subobject with another subobject is essential in that subobject.

theorem isEssentialMono_pullback {B : 𝒜} (A C : Subobject B) (hA : IsEssentialMono A.arrow) :
    IsEssentialMono ((Subobject.pullback C.arrow).obj A).arrow

Module.essentialEpi_epiDesc_cokernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Essential.lean, line 258. The attribute's comment: “essential_surjection_quotient”.

The quotient of an essential epimorphism by the image of the kernel of an epimorphism with the same source remains an essential epimorphism.

theorem essentialEpi_epiDesc_cokernel (hf : IsEssentialEpi f) :
    IsEssentialEpi
      (Abelian.epiDesc q (f ≫ cokernel.π (kernel.ι q ≫ f))
        (by simpa only [Category.assoc] using
          (cokernel.condition (kernel.ι q ≫ f))))

Tag 08XL, a lemma

Tag 08XL in the Stacks Project.

Module.isEssentialMono_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Essential.lean, line 375.

A compatible filtered system of essential embeddings of a module induces an essential embedding into its colimit.

theorem isEssentialMono_colimit {R : Type u} [Ring R]
    {J : Type v} [SmallCategory J] [IsFiltered J]
    (M : ModuleCat.{max v w u, u} R)
    (E : Functor J (ModuleCat.{max v w u, u} R)) [HasColimit E]
    (ι : (Functor.const J).obj M ⟶ E)
    (hι : ∀ j, ∃ h : Mono (ι.app j),
      let _ : Mono (ι.app j) := h
      IsEssentialMono (ι.app j))
    (j : J) :
    ∃ h : Mono (ι.app j ≫ colimit.ι E j),
      let _ : Mono (ι.app j ≫ colimit.ι E j) := h
      IsEssentialMono (ι.app j ≫ colimit.ι E j)

Tag 08XM, a lemma

Tag 08XM in the Stacks Project.

Module.isEssentialMono_subtype_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Essential.lean, line 232.

A submodule inclusion is essential if and only if every nonzero element of the ambient module has a nonzero scalar multiple lying in the submodule.

theorem isEssentialMono_subtype_iff {R : Type u} [Ring R]
    {N : ModuleCat.{v} R} (M : Submodule R N) :
    IsEssentialMono (ModuleCat.ofHom M.subtype) ↔
      ∀ x : N, x ≠ 0 → ∃ f : R, (f • x ∈ M ∧ f • x ≠ 0)

Sources

LeanModule.IsEssentialEpi · Module.IsEssentialMono · Module.isEssentialEpi_comp · Module.isEssentialMono_comp · Module.isEssentialMono_pullback · Module.essentialEpi_epiDesc_cokernel · Module.isEssentialMono_colimit · Module.isEssentialMono_subtype_iff

Section47.3 Injective modules #

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

Tag 08XP, a lemma

Tag 08XP in the Stacks Project.

Declarations registered for the tag:

Module.Injective.pi registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch47.lean, line 19 (StacksFrontier).

Tag 08XQ, a lemma

Tag 08XQ in the Stacks Project.

Module.Injective.restrictScalars_of_flat', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Injective/ChangeOfRings.lean, line 63.

Stacks 08XQ. Let R → S be a flat ring map. If E is an injective S-module, then E is injective as an R-module.

theorem restrictScalars_of_flat' (R : Type*) {S E : Type v} [CommRing R] [CommRing S]
    [Algebra R S] [Module.Flat R S] [AddCommGroup E] [Module R E] [Module S E]
    [IsScalarTower R S E] (h : Module.Injective S E) : Module.Injective R E

Tag 08YV, a lemma

Tag 08YV in the Stacks Project.

Module.Injective.of_isEpi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/Ring/Epi/RestrictionOfScalars.lean, line 94.

Let R → S be an epimorphism of rings and let E be an S-module. If E is injective as an R-module, then E is an injective S-module.

An S-linear map into E out of an S-module is in particular R-linear, so it extends R-linearly along an injective S-linear map, and that extension is S-linear because R → S is an epimorphism.

theorem Module.Injective.of_isEpi (R : Type*) {S E : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsEpi R S] [AddCommGroup E] [Module R E] [Module S E]
    [IsScalarTower R S E] (h : Module.Injective R E) : Module.Injective S E

Tag 08XR, a lemma

Tag 08XR in the Stacks Project.

Dualizing.injective_coextendScalars_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomFinite.lean, line 86.

Stacks 08XR. For a ring map f : A →+* B and an injective A-module M, the B-module Hom_A(B, M) is injective. Indeed coextension of scalars is right adjoint to restriction of scalars, which is exact and in particular preserves monomorphisms.

theorem injective_coextendScalars_obj (f : A →+* B) (M : ModuleCat.{max v u} A) [Injective M] :
    Injective ((ModuleCat.coextendScalars.{u, u, max v u} f).obj M)

Tag 08XS, a lemma

Tag 08XS in the Stacks Project.

Module.injective_iff_eq_of_essential_extension, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 608. The attribute's comment: “characterization inside an injective module”.

A submodule of an injective module is injective if and only if it has no proper essential extension inside the ambient module.

lemma injective_iff_eq_of_essential_extension
    (R : Type u) [Ring R] (I : Type v) [AddCommGroup I] [Module R I]
    [Module.Injective R I] (E : Submodule R I) :
    Module.Injective R E ↔
      ∀ (E' : Submodule R I) (h : E ≤ E'),
        let i := ModuleCat.ofHom (Submodule.inclusion h)
        letI : Mono i := (ModuleCat.mono_iff_injective i).mpr
          (Submodule.inclusion_injective h)
        IsEssentialMono i → E = E'

Module.injective_iff_isIso_essentialMono, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 721. The attribute's comment: “intrinsic characterization”.

A module is injective if and only if every essential monomorphism from it is an isomorphism.

lemma injective_iff_isIso_essentialMono
    (R : Type u) [Ring R] (Q : Type v) [AddCommGroup Q] [Module R Q] :
    Module.Injective R Q ↔
      ∀ (E' : ModuleCat.{v} R) (i : ModuleCat.of R Q ⟶ E') [Mono i],
        IsEssentialMono i → IsIso i

Tag 08XT, an example

Tag 08XT in the Stacks Project.

Module.bijective_hom_localizationAtPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Injective.lean, line 156. The attribute's comment: “canonical identification of Hom modules”.

For any module, maps into the localization at a prime are exactly the maps from its localized module, via canonical precomposition.

theorem bijective_hom_localizationAtPrime
    {R : Type u} [CommRing R] (p : Ideal R) [p.IsPrime]
    (M : Type v) [AddCommGroup M] [Module R M] :
    Function.Bijective
      (fun f : LocalizedModule.AtPrime p M →ₗ[Localization.AtPrime p]
          Localization.AtPrime p =>
        (f.restrictScalars R).comp (LocalizedModule.mkLinearMap p.primeCompl M))

Module.injective_localizationAtPrime_of_minimal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Injective.lean, line 186. The attribute's comment: “injectivity at a minimal prime”.

The localization of a reduced ring at a minimal prime is injective as an R-module.

theorem injective_localizationAtPrime_of_minimal
    {R : Type u} [CommRing R] [IsReduced R] (p : Ideal R)
    [p.IsPrime] (hp : p ∈ minimalPrimes R) :
    Module.Injective R (Localization.AtPrime p)

Tag 08XV, a lemma

Tag 08XV in the Stacks Project.

Module.directSum_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Injective.lean, line 381.

An arbitrary direct sum of injective modules over a Noetherian ring is injective.

theorem directSum_injective
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    {ι : Type v} (M : ι → Type (max v w)) [∀ i, AddCommGroup (M i)]
    [∀ i, Module R (M i)] [∀ i, Module.Injective R (M i)]
    : Module.Injective R (⨁ i, M i)

Tag 0A6I, a lemma

Tag 0A6I in the Stacks Project.

AlgebraicGeometry.AffineExt.hasInjectiveAmplitude_extD_locMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedTilde/AffineExt/InjectiveAmplitude.lean, line 52. The attribute's comment: “injective amplitude is preserved by localization”.

Injective amplitude is preserved by localization. Over a Noetherian ring R, if L in D(R) has injective amplitude in [a, b], then L ⊗_R R_f has injective amplitude in [a, b] over R_f.

A bounded complex of injective R-modules representing L is carried degreewise, and in the same degrees, to a bounded complex of injective R_f-modules representing L ⊗_R R_f: the terms stay injective by [Stacks, Tag 0A6I], the bounds are preserved because an additive functor carries zero objects to zero objects, and the complex still represents the localization because extension of scalars along a localization is exact.

theorem hasInjectiveAmplitude_extD_locMap (R : CommRingCat.{u}) [IsNoetherianRing R]
    (L : DerivedCategory (ModuleCat.{u} R)) (a b : ℤ) (f : R)
    (hL : StacksDraft.InjectiveDimension.HasInjectiveAmplitude L a b) :
    StacksDraft.InjectiveDimension.HasInjectiveAmplitude ((extD (locMap R f)).obj L) a b

Declarations registered for the tag:

Module.injective_of_isLocalizedModule registered with add_to_stacks in StacksFrontier/Algebra/Module/InjectiveHull/Localization.lean, line 14 (StacksFrontier).

Tag 08XW, a lemma

Tag 08XW in the Stacks Project.

Module.injective_iSup_torsionBy_pow, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/IndecomposableInjective.lean, line 634. The attribute's comment: “part (1)”. References: SGA 2 IV (2.2), “principal ideal case”.

The submodule of an injective module consisting of the elements annihilated by some power of f is injective. This is part (1) of Stacks Project, Tag 08XW.

lemma injective_iSup_torsionBy_pow (f : R) :
    Module.Injective R (⨆ n : ℕ, Submodule.torsionBy R I (f ^ n) : Submodule R I)

Module.injective_primaryComponent, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/IndecomposableInjective.lean, line 727. The attribute's comment: “part (2)”. References: SGA 2 IV (2.2).

The submodule of an injective module consisting of the elements annihilated by some power of J is injective. This is part (2) of Stacks Project, Tag 08XW.

lemma injective_primaryComponent (J : Ideal R) :
    Module.Injective R (Ideal.primaryComponent I J)

Tag 0A6J, a lemma

Tag 0A6J in the Stacks Project.

Module.tensorProduct_polynomial_hasInjectiveDimensionLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Injective.lean, line 877.

Stacks Project, Tag 0A6J. Extending an injective module over a Noetherian ring to the one-variable polynomial ring gives a module of injective dimension at most one.

theorem tensorProduct_polynomial_hasInjectiveDimensionLE
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (E : Type v) [AddCommGroup E] [Module A E] [Module.Injective A E] :
    HasInjectiveDimensionLE
      (ModuleCat.of (Polynomial A) (TensorProduct A (Polynomial A) E)) 1

Sources

LeanModule.Injective.pi · Module.Injective.restrictScalars_of_flat' · Module.Injective.of_isEpi · Dualizing.injective_coextendScalars_obj · Module.injective_iff_eq_of_essential_extension · Module.injective_iff_isIso_essentialMono · Module.bijective_hom_localizationAtPrime · Module.injective_localizationAtPrime_of_minimal

Section47.4 Projective covers #

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

Tag 08XY, a definition

Tag 08XY in the Stacks Project.

Module.IsProjectiveCover, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/ProjectiveCover.lean, line 63.

A morphism is a projective cover if its source is projective and it is an essential epimorphism.

abbrev IsProjectiveCover {P M : C} (f : P ⟶ M) : Prop

Tag 08XZ, a lemma

Tag 08XZ in the Stacks Project.

Module.isProjectiveCover_unique, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/ProjectiveCover.lean, line 70.

Two projective covers of the same object are isomorphic over that object.

lemma isProjectiveCover_unique {C : Type u} [Category.{v} C] [Abelian C] {P P' M : C}
    (f : P ⟶ M) (g : P' ⟶ M) (hf : IsProjectiveCover f) (hg : IsProjectiveCover g) :
    ∃ e : P ≅ P', e.hom ≫ g = f

Tag 08Y0, a lemma

Tag 08Y0 in the Stacks Project.

Module.exists_projectiveCover_of_finite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/ProjectiveCover.lean, line 132.

A finite module over a local ring has a projective cover.

lemma exists_projectiveCover_of_finite
    (R : Type u) [CommRing R] [IsLocalRing R]
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    ∃ (P : ModuleCat.{max u v} R)
      (f : P ⟶ ModuleCat.of R (Shrink.{max u v} M)),
      IsProjectiveCover f

Sources

LeanModule.IsProjectiveCover · Module.isProjectiveCover_unique · Module.exists_projectiveCover_of_finite

Section47.5 Injective hulls #

Section 47.5 of the Stacks Project, Tag 08Y1. 9 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08Y2, a definition

Tag 08Y2 in the Stacks Project.

Module.IsInjectiveHull, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 80.

An injective hull is an essential monomorphism into an injective object.

abbrev IsInjectiveHull {𝒜 : Type u} [Category.{v} 𝒜]
    [Limits.HasZeroObject 𝒜] [Limits.HasPullbacks 𝒜] {M I : 𝒜} (i : M ⟶ I) [Mono i] : Prop

Tag 08Y3, a lemma

Tag 08Y3 in the Stacks Project.

Module.exists_isInjectiveHull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 693.

Every module over a ring has an injective hull.

theorem exists_isInjectiveHull (R : Type u) [Ring R]
    (M : ModuleCat.{max v u} R) :
    ∃ (I : ModuleCat.{max v u} R) (i : M ⟶ I) (h : Mono i),
      let _ : Mono i := h
      IsInjectiveHull i

Tag 08Y4, a lemma

Tag 08Y4 in the Stacks Project.

Module.mono_of_isEssentialMono_of_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 165. The attribute's comment: “injective_extension”.

A morphism which is monic on an essential subobject is a monomorphism.

theorem mono_of_isEssentialMono_of_comp_eq {C : Type u} [Category.{v} C] [Abelian C]
    {M E N J : C} (i : M ⟶ E) [Mono i] (hi : IsEssentialMono i) (φ : M ⟶ N) [Mono φ]
    (j : N ⟶ J) [Mono j] (ψ : E ⟶ J) (hψ : i ≫ ψ = φ ≫ j) : Mono ψ

Module.isIso_of_isInjectiveHull_of_isEssentialMono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 173. The attribute's comment: “essential_extension_iso”.

A morphism between injective hulls which extends an essential monomorphism is an isomorphism.

theorem isIso_of_isInjectiveHull_of_isEssentialMono
    {C : Type u} [Category.{v} C] [Abelian C]
    {M E N E' : C} (i : M ⟶ E) (j : N ⟶ E')
    [Mono i] [Mono j]
    (hi : IsInjectiveHull i)
    (hj : IsInjectiveHull j)
    (phi : M ⟶ N) [Mono phi]
    (hphi : IsEssentialMono phi)
    (psi : E ⟶ E') (hpsi : i ≫ psi = phi ≫ j) :
    IsIso psi

Module.isIso_of_isInjectiveHull_of_extends_iso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 197. The attribute's comment: “iso_extension”.

A morphism between injective hulls which extends an isomorphism of the embedded modules is an isomorphism.

lemma isIso_of_isInjectiveHull_of_extends_iso
    {C : Type u} [Category.{v} C] [Abelian C] {M N E E' : C}
    (i : M ⟶ E) (j : N ⟶ E') [Mono i] [Mono j]
    (hi : IsInjectiveHull i)
    (hj : IsInjectiveHull j)
    (e : M ≅ N) (f : E ⟶ E')
    (comm : i ≫ f = e.hom ≫ j) :
    IsIso f

Module.exists_iso_of_isInjectiveHull, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 210. The attribute's comment: “unique_up_to_iso”.

Any two injective hulls of an object are isomorphic compatibly with their embeddings of that object.

lemma exists_iso_of_isInjectiveHull {𝒜 : Type u} [Category.{v} 𝒜]
    [Abelian 𝒜]
    {M I J : 𝒜} (i : M ⟶ I) (j : M ⟶ J) [Mono i] [Mono j]
    (hi : IsInjectiveHull i) (hj : IsInjectiveHull j) :
    ∃ e : I ≅ J, i ≫ e.hom = j

Module.exists_iso_biprod_of_isInjectiveHull, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 223. The attribute's comment: “splits_in_injective”.

An injective hull is a direct summand of any injective module containing the original module, compatibly with the two embeddings.

lemma exists_iso_biprod_of_isInjectiveHull
    {R : Type u} [Ring R] {M E I : ModuleCat.{v} R}
    (i : M ⟶ E) [Mono i] (hi : IsInjectiveHull i)
    (j : M ⟶ I) [Mono j] [CategoryTheory.Injective I] :
    ∃ I' : ModuleCat.{v} R, ∃ e : I ≅ E ⊞ I',
      j ≫ e.hom = i ≫ Limits.biprod.inl

Declarations registered for the tag:

CategoryTheory.Injective.factorThru registered with add_to_stacks in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 158 (StacksFrontier): “extend_map”.
CategoryTheory.Injective.comp_factorThru registered with add_to_stacks in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 159 (StacksFrontier): “extend_map”.

Tag 08Y5, an example

Tag 08Y5 in the Stacks Project.

Module.isInjectiveHull_fractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 247.

The canonical inclusion of a domain into its fraction field is an injective hull.

theorem isInjectiveHull_fractionRing
    (R : Type u) [CommRing R] [IsDomain R]
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] :
    let M : Submodule R K := (Algebra.linearMap R K).range
    let i : ModuleCat.of R M ⟶ ModuleCat.of R K :=
      ModuleCat.ofHom M.subtype
    letI : Mono i :=
      (ModuleCat.mono_iff_injective i).2 M.injective_subtype
    IsInjectiveHull i

Tag 08Y6, a definition

Tag 08Y6 in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Indecomposable registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch47.lean, line 22 (StacksFrontier): “for any category with zero morphisms and binary biproducts, e.g. an additive category”.

Tag 08Y7, a lemma

Tag 08Y7 in the Stacks Project.

Module.Subobject.isInjectiveHull_arrow_of_indecomposable, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/IndecomposableInjective.lean, line 78. The attribute's comment: “injective_hull”.

The inclusion of any nonzero submodule of an indecomposable injective module exhibits the ambient module as its injective hull.

lemma Subobject.isInjectiveHull_arrow_of_indecomposable
    (R : Type u) [Ring R] (E : ModuleCat.{v} R) [CategoryTheory.Injective E]
    (hE : Indecomposable E) (M : Subobject E) (hM : M ≠ ⊥) :
    IsInjectiveHull M.arrow

Module.Subobject.inf_ne_bot_of_indecomposable_injective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/IndecomposableInjective.lean, line 124. The attribute's comment: “nonzero_intersection”.

Two nonzero submodules of an indecomposable injective module have nonzero intersection.

lemma Subobject.inf_ne_bot_of_indecomposable_injective (R : Type u) [Ring R]
    (E : ModuleCat.{v} R) [CategoryTheory.Injective E] (hE : Indecomposable E)
    (A B : Subobject E) (hA : A ≠ ⊥) (hB : B ≠ ⊥) : A ⊓ B ≠ ⊥

Module.endomorphismRing_isLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/IndecomposableInjective.lean, line 220. The attribute's comment: “endomorphism_ring_local”.

The endomorphism ring of an indecomposable injective module is a (possibly noncommutative) local ring.

theorem endomorphismRing_isLocalRing
    {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E]
    [Module.Injective R E]
    (hE : Indecomposable (ModuleCat.of R E)) :
    IsLocalRing (Module.End R E)

Module.exists_maximalIdeal_endomorphismRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/IndecomposableInjective.lean, line 247. The attribute's comment: “endomorphism_ring_local”.

The maximal two-sided ideal of the endomorphism ring consists exactly of the endomorphisms with nonzero kernel, and every endomorphism outside it is invertible.

theorem exists_maximalIdeal_endomorphismRing
    {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E]
    [Module.Injective R E]
    (hE : Indecomposable (ModuleCat.of R E)) :
    ∃ I : Ideal (Module.End R E), I.IsTwoSided ∧ I.IsMaximal ∧
      (∀ φ : Module.End R E, φ ∈ I ↔ LinearMap.ker φ ≠ ⊥) ∧
      (∀ φ : Module.End R E, φ ∉ I → IsUnit φ)

Module.exists_prime_eq_zeroDivisorsOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/IndecomposableInjective.lean, line 311. The attribute's comment: “zero_divisors_prime”.

The set of zerodivisors on an indecomposable injective module is the underlying set of a prime ideal.

theorem exists_prime_eq_zeroDivisorsOn {R : Type u} [CommRing R]
    (E : ModuleCat.{v} R) [CategoryTheory.Injective E] (hE : Indecomposable E) :
    ∃ p : Ideal R, p.IsPrime ∧ (p : Set R) = {r : R | ∃ m : E, m ≠ 0 ∧ r • m = 0}

Module.exists_injective_localizationAtPrime_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/IndecomposableInjective.lean, line 331. The attribute's comment: “injective_over_localization”.

An indecomposable injective module is an injective module over the localization at its prime ideal of zerodivisors.

theorem exists_injective_localizationAtPrime_module
    {R : Type u} [CommRing R] (E : ModuleCat.{v} R) [CategoryTheory.Injective E]
    (hE : Indecomposable E) (p : Ideal R) (hp : p.IsPrime)
    (hpE : (p : Set R) = {r : R | ∃ m : E, m ≠ 0 ∧ r • m = 0}) :
    ∃ moduleStructure : Module (Localization.AtPrime p) E,
      letI := moduleStructure
      (∀ (r : R) (x : E), algebraMap R (Localization.AtPrime p) r • x = r • x) ∧
        CategoryTheory.Injective (ModuleCat.of (Localization.AtPrime p) E)

Tag 08Y8, a lemma

Tag 08Y8 in the Stacks Project.

Module.exists_isInjectiveHull_residueField_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/DirectSumDecomposition.lean, line 300. The attribute's comment: “localized_hull”.

The injective hull of R ⧸ p is naturally an injective hull of the residue field at p over Rₚ.

theorem exists_isInjectiveHull_residueField_localization
    {R : Type u} [CommRing R] (p : Ideal R) [p.IsPrime]
    (E : ModuleCat.{u} R) (i : ModuleCat.of R (R ⧸ p) ⟶ E) [Mono i]
    (hi : IsInjectiveHull i) :
    ∃ moduleStructure : Module (Localization.AtPrime p) E,
      letI := moduleStructure
      ∃ tower : IsScalarTower R (Localization.AtPrime p) E,
        letI := tower
        ∃ j : ModuleCat.of (Localization.AtPrime p) p.ResidueField ⟶
            ModuleCat.of (Localization.AtPrime p) E,
          ∃ monoJ : Mono j,
            letI := monoJ
            ModuleCat.ofHom
                ((LinearMap.restrictScalars R j.hom).comp
                  (LinearMap.restrictScalars R
                    (Algebra.linearMap (R ⧸ p) p.ResidueField))) = i ∧
              IsInjectiveHull j

Module.exists_isInjectiveHull_residueField_of_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/Existence.lean, line 296. The attribute's comment: “hull_of_residue_field”.

An injective hull of the quotient by a prime ideal is also an injective hull of the prime's residue field.

theorem exists_isInjectiveHull_residueField_of_quotient
    (R : Type u) [CommRing R] (p : Ideal R) [p.IsPrime]
    (E : ModuleCat.{max u v} R)
    (i : ModuleCat.of R (ULift.{v} (R ⧸ p)) ⟶ E) [Mono i]
    (hi : IsInjectiveHull i) :
    ∃ (j : ModuleCat.of R (ULift.{v} p.ResidueField) ⟶ E) (_ : Mono j),
      IsInjectiveHull j

Module.indecomposable_of_isInjectiveHull_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/IndecomposableInjective.lean, line 406. The attribute's comment: “indecomposable”.

The injective hull of the quotient by a prime ideal is indecomposable.

theorem indecomposable_of_isInjectiveHull_quotient
    {R : Type u} [CommRing R] (p : Ideal R) [p.IsPrime]
    {E : ModuleCat.{max v u} R}
    (i : ModuleCat.of R (ULift.{v} (R ⧸ p)) ⟶ E) [Mono i]
    (hi : IsInjectiveHull i) : Indecomposable E

Tag 08Y9, a lemma

Tag 08Y9 in the Stacks Project.

Module.exists_isInjectiveHull_residueField_of_indecomposable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/IndecomposableInjective.lean, line 502.

An indecomposable injective module over a Noetherian ring is an injective hull of the residue field at some prime ideal.

theorem exists_isInjectiveHull_residueField_of_indecomposable
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (E : ModuleCat.{v} R) [CategoryTheory.Injective E] (hE : Indecomposable E) :
    ∃ (p : PrimeSpectrum R) (K : ModuleCat.{v} R),
      Nonempty (K ≃ₗ[R] p.asIdeal.ResidueField) ∧
        ∃ (i : K ⟶ E) (_ : Mono i), IsInjectiveHull i

Tag 08YA, a proposition

Tag 08YA in the Stacks Project.

Module.exists_iso_directSum_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/DirectSumDecomposition.lean, line 646. The attribute's comment: “direct sum decomposition”.

An injective module over a Noetherian ring is isomorphic to a direct sum of indecomposable injective modules.

theorem exists_iso_directSum_of_injective
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (I : ModuleCat.{v} R) [CategoryTheory.Injective I] :
    ∃ (ι : Type v) (E : ι → ModuleCat.{v} R)
      (_ : I ≅ ModuleCat.of R (⨁ i, E i)),
      (∀ i, CategoryTheory.Injective (E i)) ∧ (∀ i, Indecomposable (E i))

Module.exists_residueField_injectiveHull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/InjectiveHull/Basic/DirectSumDecomposition.lean, line 744. The attribute's comment: “indecomposable injective modules”.

An indecomposable injective module over a Noetherian ring is an injective hull of the residue field at a prime ideal.

theorem exists_residueField_injectiveHull
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (E : ModuleCat.{v} R) [CategoryTheory.Injective E] (hE : Indecomposable E) :
    ∃ (p : Ideal R) (hp : p.IsPrime),
      letI := hp
      ∃ (K : ModuleCat.{v} R) (_ : K ≃ₗ[R] p.ResidueField)
        (i : K ⟶ E) (hi : Mono i),
        letI := hi
        IsInjectiveHull i

Sources

LeanModule.IsInjectiveHull · Module.exists_isInjectiveHull · Module.mono_of_isEssentialMono_of_comp_eq · Module.isIso_of_isInjectiveHull_of_isEssentialMono · Module.isIso_of_isInjectiveHull_of_extends_iso · Module.exists_iso_of_isInjectiveHull · Module.exists_iso_biprod_of_isInjectiveHull · CategoryTheory.Injective.factorThru

Section47.6 Duality over Artinian local rings #

Section 47.6 of the Stacks Project, Tag 08YW. 4 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08YX, a lemma

Tag 08YX in the Stacks Project.

Dualizing.length_linearMap_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Artinian.lean, line 284. The attribute's comment: “length equality”.

Stacks Project, Tag 08YX. Taking linear maps into an injective hull of the residue field preserves the length of a finite module.

public lemma length_linearMap_eq (hi : Module.IsInjectiveHull i)
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    Module.length R (M →ₗ[R] E) = Module.length R M

Dualizing.finite_of_isInjectiveHull_residueField, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Artinian.lean, line 293. The attribute's comment: “finiteness of the injective hull”.

Stacks Project, Tag 08YX. An injective hull of the residue field of an Artinian local ring is finite over the ring.

public lemma finite_of_isInjectiveHull_residueField
    (hi : Module.IsInjectiveHull i) : Module.Finite R E

Tag 08YY, a lemma

Tag 08YY in the Stacks Project.

Dualizing.evaluation_bijective_of_isInjectiveHull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Artinian.lean, line 356. The attribute's comment: “the evaluation map”.

Stacks Project, Tag 08YY. Evaluation into an injective hull of the residue field identifies every finite module over an Artinian local ring with its double dual.

public theorem evaluation_bijective_of_isInjectiveHull
    (R : Type u) [CommRing R] [IsArtinianRing R] [IsLocalRing R]
    (E : Type u) [AddCommGroup E] [Module R E]
    (i : ModuleCat.of R (IsLocalRing.ResidueField R) ⟶ ModuleCat.of R E)
    [Mono i] (hi : Module.IsInjectiveHull i)
    (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] :
    Function.Bijective
      (LinearMap.flip
        (LinearMap.id : (M →ₗ[R] E) →ₗ[R] (M →ₗ[R] E)))

Dualizing.algebraMap_end_bijective_of_isInjectiveHull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Artinian.lean, line 395. The attribute's comment: “the endomorphism ring”.

Stacks Project, Tag 08YY. The canonical scalar-action map from an Artinian local ring to the endomorphism ring of an injective hull of its residue field is bijective.

public theorem algebraMap_end_bijective_of_isInjectiveHull
    (R : Type u) [CommRing R] [IsArtinianRing R] [IsLocalRing R]
    (E : Type u) [AddCommGroup E] [Module R E]
    (i : ModuleCat.of R (IsLocalRing.ResidueField R) ⟶ ModuleCat.of R E)
    [Mono i] (hi : Module.IsInjectiveHull i) :
    Function.Bijective (algebraMap R (Module.End R E))

Tag 08YZ, a lemma

Tag 08YZ in the Stacks Project.

Dualizing.injectiveHullDual, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Artinian.lean, line 440. The attribute's comment: “the duality functor”.

Taking linear maps into the injective hull, contravariantly, on finite modules.

public def injectiveHullDual : (FGModuleCat.{u} R)ᵒᵖ ⥤ FGModuleCat.{u} R

Dualizing.injectiveHullDualEvaluation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Artinian.lean, line 455. The attribute's comment: “canonical evaluation transformation”.

The natural transformation with components the canonical evaluation maps m ↦ (f ↦ f m) into the E-valued double dual.

public def injectiveHullDualEvaluation :
    𝟭 (FGModuleCat.{u} R) ⟶
      opOp (FGModuleCat.{u} R) ⋙ (injectiveHullDual R E i hi).op ⋙
        injectiveHullDual R E i hi

Dualizing.injectiveHullDual_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Artinian.lean, line 491. The attribute's comment: “anti-equivalence”.

Stacks Project, Tag 08YZ. Linear duality with values in an injective hull of the residue field is an anti-equivalence of the category of finite modules with itself.

public theorem injectiveHullDual_isEquivalence :
    (injectiveHullDual R E i hi).IsEquivalence

Dualizing.injectiveHullDual_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Artinian.lean, line 508. The attribute's comment: “exactness: limits”.

Stacks Project, Tag 08YZ. The E-valued duality preserves finite limits, hence takes finite colimits of finite modules to finite limits.

public theorem injectiveHullDual_preservesFiniteLimits :
    PreservesFiniteLimits (injectiveHullDual R E i hi)

Dualizing.injectiveHullDual_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Artinian.lean, line 516. The attribute's comment: “exactness: colimits”.

Stacks Project, Tag 08YZ. The E-valued duality preserves finite colimits, hence takes finite limits of finite modules to finite colimits.

public theorem injectiveHullDual_preservesFiniteColimits :
    PreservesFiniteColimits (injectiveHullDual R E i hi)

Dualizing.injectiveHullDualEvaluation_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Artinian.lean, line 524. The attribute's comment: “canonical double-dual identification”.

The canonical evaluation maps give a natural isomorphism from the identity functor to the square of the E-valued duality.

public theorem injectiveHullDualEvaluation_isIso :
    IsIso (injectiveHullDualEvaluation R E i hi)

Tag 08Z0, a lemma

Tag 08Z0 in the Stacks Project.

Dualizing.dualTorsionEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualityArtinianLocal/Basic.lean, line 70. The attribute's comment: “the dual of ideal torsion”.

Stacks Project, Tag 08Z0. Restricting a functional to the elements of M killed by I induces the canonical identification of the quotient of the dual of M by I with the dual of that submodule.

noncomputable def dualTorsionEquiv
    (R : Type u) [CommRing R]
    (E : Type v) [AddCommGroup E] [Module R E] [Module.Injective R (ULift.{u} E)]
    (M : Type w) [AddCommGroup M] [Module R M]
    (I : Ideal R) (hI : I.FG) :
    { e : ((M →ₗ[R] E) ⧸ (I • (⊤ : Submodule R (M →ₗ[R] E)))) ≃ₗ[R]
        (Submodule.torsionBySet R M (I : Set R) →ₗ[R] E) //
      ∀ f : M →ₗ[R] E,
        e (Submodule.Quotient.mk f) =
          f.comp (Submodule.subtype (Submodule.torsionBySet R M (I : Set R))) }

Dualizing.dualQuotientEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualityArtinianLocal/Basic.lean, line 171. The attribute's comment: “the dual of the quotient by an ideal”.

Stacks Project, Tag 08Z0. Precomposing with the quotient map identifies the dual of M / I M with the submodule of functionals on M killed by I.

noncomputable def dualQuotientEquiv
    (R : Type u) [CommRing R]
    (E : Type v) [AddCommGroup E] [Module R E]
    (M : Type w) [AddCommGroup M] [Module R M]
    (I : Ideal R) :
    { e : ((M ⧸ (I • (⊤ : Submodule R M))) →ₗ[R] E) ≃ₗ[R]
        Submodule.torsionBySet R (M →ₗ[R] E) (I : Set R) //
      ∀ (f : (M ⧸ (I • (⊤ : Submodule R M))) →ₗ[R] E) (m : M),
        (e f : M →ₗ[R] E) m = f (Submodule.Quotient.mk m) }

Sources

LeanDualizing.length_linearMap_eq · Dualizing.finite_of_isInjectiveHull_residueField · Dualizing.evaluation_bijective_of_isInjectiveHull · Dualizing.algebraMap_end_bijective_of_isInjectiveHull · Dualizing.injectiveHullDual · Dualizing.injectiveHullDualEvaluation · Dualizing.injectiveHullDual_isEquivalence · Dualizing.injectiveHullDual_preservesFiniteLimits

Section47.7 Injective hull of the residue field #

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

Tag 08Z2, a lemma

Tag 08Z2 in the Stacks Project.

Dualizing.isInjectiveHull_kernelTorsion_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/PowerTorsionFiltration.lean, line 233.

Stacks Project, Tag 08Z2. For a surjective ring homomorphism, the submodule of an injective hull annihilated by the kernel is an injective hull over the quotient ring.

public theorem isInjectiveHull_kernelTorsion_of_surjective
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    (f : R →+* S) (hf : Function.Surjective f)
    {K : ModuleCat.{w} S} {E : ModuleCat.{w} R}
    (i : (ModuleCat.restrictScalars.{w} f).obj K ⟶ E) [Mono i]
    (hi : Module.IsInjectiveHull i) :
    Module.IsInjectiveHull (kernelTorsionInclusion f hf i)

Tag 08Z3, a lemma

Tag 08Z3 in the Stacks Project.

Dualizing.exists_injective_to_pi_injectiveHull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/PowerTorsionFiltration.lean, line 499.

Stacks Project, Tag 08Z3. A module which is power-torsion for the maximal ideal embeds in the direct sum of as many copies of an injective hull of the residue field as the dimension of its socle.

public theorem exists_injective_to_pi_injectiveHull
    (R : Type u) [CommRing R] [IsLocalRing R]
    (M : Type v) (E : Type u) [AddCommGroup M] [Module R M] [AddCommGroup E] [Module R E]
    (i : ModuleCat.of R (R ⧸ IsLocalRing.maximalIdeal R) ⟶ ModuleCat.of R E) [Mono i]
    (hi : Module.IsInjectiveHull i)
    (hM : ∀ x : M, ∃ e : ℕ, ∀ r ∈ (IsLocalRing.maximalIdeal R ^ e : Ideal R),
      r • x = 0)
    (n : ℕ)
    [Module.Finite (R ⧸ IsLocalRing.maximalIdeal R)
      (Submodule.torsionBySet R M (IsLocalRing.maximalIdeal R))]
    (hn : Module.finrank (R ⧸ IsLocalRing.maximalIdeal R)
      (Submodule.torsionBySet R M (IsLocalRing.maximalIdeal R)) = n) :
    ∃ f : M →ₗ[R] (Fin n → E), Function.Injective f

Tag 08Z4, a lemma

Tag 08Z4 in the Stacks Project.

Dualizing.maximalIdealPowTorsion_isInjectiveHull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/PowerTorsionFiltration.lean, line 379. The attribute's comment: “the submodules E_n”.

Stacks Project, Tag 08Z4. The submodule of an injective hull of the residue field annihilated by a positive power of the maximal ideal is an injective hull over the corresponding quotient ring. This is the canonical realization of the source's equality E_n = E[𝔪^(n + 1)].

public theorem maximalIdealPowTorsion_isInjectiveHull
    (R : Type u) [CommRing R] [IsLocalRing R]
    (K E : ModuleCat.{v} R) (e : IsLocalRing.ResidueField R ≃ₗ[R] K)
    (i : K ⟶ E) [Mono i]
    (hE : Module.IsInjectiveHull i) (n : ℕ) :
    let hK := residueFieldModelIsTorsionByMaximalIdealPow R K e n
    letI := hK.module
    let j := residueFieldToMaximalIdealPowTorsion R e i n
    letI : Mono (ModuleCat.ofHom j) :=
      (ModuleCat.mono_iff_injective _).2
        (residueFieldToMaximalIdealPowTorsion_injective R e i
          ((ModuleCat.mono_iff_injective i).1 (by infer_instance)) n)
    Module.IsInjectiveHull (ModuleCat.ofHom j)

Dualizing.iSup_maximalIdealPowTorsion_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/PowerTorsionFiltration.lean, line 461. The attribute's comment: “the union”.

Stacks Project, Tag 08Z4. The submodules annihilated by positive powers of the maximal ideal exhaust an injective hull of the residue field.

public theorem iSup_maximalIdealPowTorsion_eq_top
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (K E : ModuleCat.{v} R) (e : IsLocalRing.ResidueField R ≃ₗ[R] K)
    (i : K ⟶ E) [Mono i]
    (hE : Module.IsInjectiveHull i) :
    (⨆ n : ℕ, maximalIdealPowTorsion R E n) = ⊤

Tag 08Z5, a lemma

Tag 08Z5 in the Stacks Project.

Dualizing.exists_iso_injectiveHull_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/FlatComparison.lean, line 152.

Stacks Project, Tag 08Z5. Injective hulls of the residue fields of a flat local homomorphism with trivial closed fibre agree after restriction of scalars. The comparison isomorphism extends the induced identification of residue fields.

public theorem exists_iso_injectiveHull_residueField
    (R S : Type u) [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] [IsNoetherianRing R]
    [IsNoetherianRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)]
    (hflat : RingHom.Flat (algebraMap R S))
    (hclosed : Function.Bijective (closedFiberMap R S))
    {E_R : ModuleCat.{u} R} {E_S : ModuleCat.{u} S}
    (i_R : ModuleCat.of R (ResidueField R) ⟶ E_R)
    (i_S : ModuleCat.of S (ResidueField S) ⟶ E_S)
    [Mono i_R] [Mono i_S]
    (hR : Module.IsInjectiveHull i_R)
    (hS : Module.IsInjectiveHull i_S) :
    ∃ e : E_R ≅ (ModuleCat.restrictScalars (algebraMap R S)).obj E_S,
      i_R ≫ e.hom = residueFieldMap R S ≫
        (ModuleCat.restrictScalars (algebraMap R S)).map i_S

Tag 08Z6, a lemma

Tag 08Z6 in the Stacks Project.

Dualizing.endAlgEquivAdicCompletion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/Endomorphisms.lean, line 660.

Stacks Project, Tag 08Z6. The endomorphism ring of an injective hull of the residue field of a Noetherian local ring is canonically isomorphic to its completion.

public noncomputable def endAlgEquivAdicCompletion
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (E : Type u) [AddCommGroup E] [Module R E]
    (i : ModuleCat.of R (R ⧸ IsLocalRing.maximalIdeal R) ⟶ ModuleCat.of R E)
    [Mono i] (hi : Module.IsInjectiveHull i) :
    Module.End R E ≃ₐ[R] AdicCompletion (IsLocalRing.maximalIdeal R) R

Tag 08Z7, a lemma

Tag 08Z7 in the Stacks Project.

Dualizing.isArtinian_of_isInjectiveHull_residueField, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/ChainConditions.lean, line 240.

Stacks Project, Tag 08Z7. An injective hull of the residue field of a Noetherian local ring is an Artinian module.

public lemma isArtinian_of_isInjectiveHull_residueField
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (E : Type u) [AddCommGroup E] [Module R E]
    (i : ModuleCat.of R (IsLocalRing.ResidueField R) ⟶ ModuleCat.of R E)
    [Mono i] (hi : Module.IsInjectiveHull i) :
    IsArtinian R E

Tag 08Z8, a lemma

Tag 08Z8 in the Stacks Project.

Dualizing.isNoetherian_iff_module_finite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/ChainConditions.lean, line 283. The attribute's comment: “part (1): ascending chain condition and finite generation”.

Stacks Project, Tag 08Z8, part (1). Over a Noetherian ring, the ascending chain condition on submodules is equivalent to finite generation.

public lemma isNoetherian_iff_module_finite (R : Type u) [Ring R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    IsNoetherian R M ↔ Module.Finite R M

Dualizing.module_finite_iff_exists_finite_presentation, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/ChainConditions.lean, line 291. The attribute's comment: “part (1): finite presentation”.

Stacks Project, Tag 08Z8, part (1). A finite module over a Noetherian ring admits a presentation by two finite free modules.

public lemma module_finite_iff_exists_finite_presentation
    (R : Type u) [Ring R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    Module.Finite R M ↔
      ∃ (n m : ℕ) (f : (Fin n → R) →ₗ[R] M) (g : (Fin m → R) →ₗ[R] (Fin n → R)),
        Function.Surjective f ∧ Function.Exact g f

Dualizing.isArtinian_iff_powerTorsion_and_finiteSocle, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/ChainConditions.lean, line 379. The attribute's comment: “part (2): descending chain condition and torsion”.

Stacks Project, Tag 08Z8, part (2). A module has the descending chain condition exactly when it is maximal-ideal-power torsion and has finite-dimensional socle.

public lemma isArtinian_iff_powerTorsion_and_finiteSocle
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M] :
    IsArtinian R M ↔
      (IsIPowerTorsion R M (maximalIdeal R) ∧ HasFiniteSocle R M)

Dualizing.powerTorsion_and_finiteSocle_iff_exists_finite_copresentation, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/ChainConditions.lean, line 390. The attribute's comment: “part (2): finite copresentation”.

Stacks Project, Tag 08Z8, part (2). The torsion and finite-socle condition is equivalent to the existence of a copresentation by finite sums of an injective hull of the residue field.

public lemma powerTorsion_and_finiteSocle_iff_exists_finite_copresentation
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (E : Type u) [AddCommGroup E] [Module R E]
    (i : ResidueField R →ₗ[R] E) [Mono (ModuleCat.ofHom i)]
    (hi : Module.IsInjectiveHull (ModuleCat.ofHom i)) :
    (IsIPowerTorsion R M (maximalIdeal R) ∧ HasFiniteSocle R M) ↔
      ∃ (n m : ℕ) (f : M →ₗ[R] (Fin n → E))
        (g : (Fin n → E) →ₗ[R] (Fin m → E)),
        Function.Injective f ∧ Function.Exact f g

Tag 08Z9, a proposition

Tag 08Z9 in the Stacks Project.

Dualizing.isIso_matlisEvaluation_of_isArtinian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/Matlis.lean, line 1012. The attribute's comment: “biduality for modules with the descending chain condition”.

The canonical map to the double Matlis dual is an isomorphism for every module satisfying the descending chain condition.

public theorem isIso_matlisEvaluation_of_isArtinian
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    (E M : ModuleCat.{max u v} R)
    (i : residueFieldModule.{u, v} R ⟶ E) [Mono i]
    (hi : Module.IsInjectiveHull i) [IsArtinian R M] :
    IsIso ((matlisEvaluation R E).app M)

Dualizing.isIso_matlisEvaluation_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/Matlis.lean, line 1025. The attribute's comment: “biduality for modules with the ascending chain condition”.

The canonical map to the double Matlis dual is an isomorphism for every module satisfying the ascending chain condition.

public theorem isIso_matlisEvaluation_of_isNoetherian
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    (E M : ModuleCat.{max u v} R)
    (i : residueFieldModule.{u, v} R ⟶ E) [Mono i]
    (hi : Module.IsInjectiveHull i) [IsNoetherian R M] :
    IsIso ((matlisEvaluation R E).app M)

Dualizing.matlisDuality, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/Matlis.lean, line 1193. The attribute's comment: “anti-equivalence”. References: SGA 2 IV (5.1), “special case”.

Matlis duality (Stacks Project, Tag 08Z9). The canonical anti-equivalence between Artinian and Noetherian modules over a complete local Noetherian ring.

public noncomputable def matlisDuality
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    (E : ModuleCat.{max u v} R)
    (i : residueFieldModule.{u, v} R ⟶ E) [Mono i]
    (hi : Module.IsInjectiveHull i) :
    (ArtinianModules.{u, v} R)ᵒᵖ ≌ NoetherianModules.{u, v} R

Dualizing.matlisDualityFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/Matlis.lean, line 1206. The attribute's comment: “the anti-equivalence is induced by the Matlis dual functor”.

The functor underlying matlisDuality, after inclusion in all modules, is naturally isomorphic to Hom_R(-, E).

public noncomputable def matlisDualityFunctorIso
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    (E : ModuleCat.{max u v} R)
    (i : residueFieldModule.{u, v} R ⟶ E) [Mono i]
    (hi : Module.IsInjectiveHull i) :
    (matlisDuality R E i hi).functor ⋙
        ObjectProperty.ι (fun M : ModuleCat.{max u v} R ↦ IsNoetherian R M) ≅
      (ObjectProperty.ι (fun M : ModuleCat.{max u v} R ↦ IsArtinian R M)).op ⋙
        (linearYoneda R (ModuleCat.{max u v} R)).obj E

Declarations registered for the tag:

CategoryTheory.linearYoneda registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/Matlis.lean, line 119 (StacksFrontier): “the functor”.

Tag 0EGL, a remark

Tag 0EGL in the Stacks Project.

Dualizing.isArtinian_of_finite_matlisDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldHull/ChainConditions.lean, line 195.

Stacks Project, Tag 0EGL. A maximal-ideal-power torsion module whose Matlis dual is finite over the completion satisfies the descending chain condition.

public theorem isArtinian_of_finite_matlisDual
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (N : Type v) [AddCommGroup N] [Module R N]
    (E : Type u) [AddCommGroup E] [Module R E]
    (i : ModuleCat.of R (R ⧸ IsLocalRing.maximalIdeal R) ⟶ ModuleCat.of R E)
    [Mono i] (hi : Module.IsInjectiveHull i)
    (hN : IsIPowerTorsion R N (IsLocalRing.maximalIdeal R))
    (hfinite : letI := matlisDualAdicCompletionModule R N E i hi
      Module.Finite (AdicCompletion (IsLocalRing.maximalIdeal R) R) (N →ₗ[R] E)) :
    IsArtinian R N

Sources

LeanDualizing.isInjectiveHull_kernelTorsion_of_surjective · Dualizing.exists_injective_to_pi_injectiveHull · Dualizing.maximalIdealPowTorsion_isInjectiveHull · Dualizing.iSup_maximalIdealPowTorsion_eq_top · Dualizing.exists_iso_injectiveHull_residueField · Dualizing.endAlgEquivAdicCompletion · Dualizing.isArtinian_of_isInjectiveHull_residueField · Dualizing.isNoetherian_iff_module_finite

Section47.8 Deriving torsion #

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

Tag 0A6L, a lemma

Tag 0A6L in the Stacks Project.

Dualizing.derivedInclusion_adj_derivedPowerTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedTorsion.lean, line 878.

Stacks 0A6L. Local cohomology RΓ_I, as the named total right derived functor of the I-power-torsion-submodule functor, is right adjoint to the derived inclusion of the category of I-power-torsion modules into D(A). Its counit is induced by the underived torsion-submodule inclusion, compatibly with the total right derived unit.

theorem derivedInclusion_adj_derivedPowerTorsion
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG) :
    let P : ObjectProperty (ModuleCat.{max u v} A) := fun M ↦ IsIPowerTorsion A M I
    letI : P.IsSerreClass := isSerreClass_isIPowerTorsion I hI
    letI : PreservesFiniteLimits P.ι :=
      ObjectProperty.preservesFiniteLimits_ι_of_isWeakSerreClass P
    letI : PreservesFiniteColimits P.ι :=
      ObjectProperty.preservesFiniteColimits_ι_of_isWeakSerreClass P
    ∃ adj : P.ι.mapDerivedCategory ⊣ derivedPowerTorsion.{u, v} A I hI,
      IsCanonicalDerivedPowerTorsionCounit.{u, v} A I hI adj.counit

Tag 0954, a lemma

Tag 0954 in the Stacks Project.

Stacks.LocalCohomology.localCohomologyHomologyIsoColimitExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/TorsionColimit.lean, line 609. The attribute's comment: “cohomology-module identification”.

Stacks 0954. In every degree, local cohomology is the filtered colimit of the Ext modules from the quotients by powers of the ideal.

noncomputable def localCohomologyHomologyIsoColimitExt (I : Ideal R)
    (K : DerivedCategory (ModuleCat.{u} R)) (q : ℤ) :
    (ModuleCat.uliftFunctor.{u + 1} R).obj
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) q).obj (localCohomology R I K)) ≅
      colimit (extPowers R I K q)

Stacks.LocalCohomology.localCohomology_isHomotopyColimit_derivedHomPowers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/TorsionColimit.lean, line 640. The attribute's comment: “derived-category identification”.

Stacks 0954. Local cohomology is the homotopy colimit of the derived Hom complexes from the powers of the ideal.

theorem localCohomology_isHomotopyColimit_derivedHomPowers (I : Ideal R)
    (K : DerivedCategory (ModuleCat.{u} R)) :
    IsHomotopyColimit (derivedHomPowersOf R I K) (localCohomology R I K)

Tag 0A6M, a lemma

Tag 0A6M in the Stacks Project.

Dualizing.localCohomology_isZero_of_isIso_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivingTorsion/Vanishing.lean, line 93.

Stacks 0A6M. If some f ∈ I acts invertibly on K, then its local cohomology with support in V(I) is zero.

theorem localCohomology_isZero_of_isIso_smul
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (K : DerivedCategory (ModuleCat.{v} A))
    (f : A) (hf : f ∈ I) (hiso : IsIso (f • 𝟙 K)) :
    IsZero ((localCohomologyFunctor A I hI).obj K)

Tag 0A6N, an equation

Tag 0A6N in the Stacks Project.

Dualizing.powerTorsionComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedTorsion.lean, line 222.

Stacks 0A6N. The canonical functor from the derived category of I-power-torsion A-modules to the full subcategory of D(A) on the objects with I-power-torsion cohomology.

noncomputable def powerTorsionComparison
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG) :
    DerivedCategory (PowerTorsionModule A I hI) ⥤
      PowerTorsionDerivedCategory A I hI

Tag 0A6P, a lemma

Tag 0A6P in the Stacks Project.

Dualizing.bijective_derivedInclusion_map_singleFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedTorsion.lean, line 246. The attribute's comment: “part (1), the Hom comparison”.

The inclusion of power-torsion modules induces a bijection on derived morphisms between modules concentrated in degree zero.

theorem bijective_derivedInclusion_map_singleFunctor
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (M N : PowerTorsionModule.{u, v} A I hI) :
    let F := (powerTorsionModuleProperty A I hI).ι.mapDerivedCategory
    let X := (DerivedCategory.singleFunctor
      (PowerTorsionModule.{u, v} A I hI) 0).obj M
    let Y := (DerivedCategory.singleFunctor
      (PowerTorsionModule.{u, v} A I hI) 0).obj N
    Function.Bijective (fun f : X ⟶ Y ↦ F.map f)

Dualizing.bijective_mapExt_one_powerTorsionModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedTorsion.lean, line 361. The attribute's comment: “part (2), the Ext¹ comparison”.

Stacks 0A6P, Ext¹ comparison. The exact inclusion of the category of I-power-torsion modules into all A-modules induces a bijection on Ext¹.

theorem bijective_mapExt_one_powerTorsionModule
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (M N : PowerTorsionModule.{u, v} A I hI) :
    Function.Bijective
      ((powerTorsionModuleProperty A I hI).ι.mapExtAddHom M N 1)

Dualizing.exists_not_surjective_mapExt_two_powerTorsionModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionExtCounterexample.lean, line 344. The attribute's comment: “part (3)”.

Stacks 0A6P (3). The comparison map Ext²_{D(I^∞-torsion)}(M, N) ⟶ Ext²_{D(A)}(M, N) between I-power-torsion modules is not surjective in general: there is a commutative ring A, a finitely generated (indeed principal) ideal I, and I-power-torsion modules M and N for which the inclusion of the torsion category does not hit every class of Ext²_A(M, N).

Parts (1) and (2) of the source, that the comparison is bijective on Hom and on Ext¹, are Dualizing.bijective_derivedInclusion_map_singleFunctor and Dualizing.bijective_mapExt_one_powerTorsionModule.

theorem exists_not_surjective_mapExt_two_powerTorsionModule :
    ∃ (A : Type) (_ : CommRing A) (I : Ideal A) (hI : I.FG)
      (M N : PowerTorsionModule.{0, 0} A I hI),
      ¬ Function.Surjective
        ((powerTorsionModuleProperty A I hI).ι.mapExtAddHom M N 2)

Dualizing.exists_not_isEquivalence_powerTorsionComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionExtCounterexample.lean, line 361. The attribute's comment: “part (4)”.

Stacks 0A6P (4). The comparison functor of Stacks 0A6N, D(I^∞-torsion) ⟶ D_{I^∞-torsion}(A), is not an equivalence in general.

This is part (3) together with Dualizing.not_isEquivalence_powerTorsionComparison_of_not_surjective_mapExt: an equivalence would be bijective on Extⁿ in every degree.

theorem exists_not_isEquivalence_powerTorsionComparison :
    ∃ (A : Type) (_ : CommRing A) (I : Ideal A) (hI : I.FG),
      ¬ (powerTorsionComparison.{0, 0} A I hI).IsEquivalence

Dualizing.bijective_hom_and_ext_one_and_exists_not_surjective_ext_two_and_not_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionExtCounterexample.lean, line 385. The attribute's comment: “all four parts conjoined”.

Stacks 0A6P, all four parts. For every ring A, every finitely generated ideal I ⊆ A and all I-power-torsion A-modules M and N:

Hom_{D(A)}(M, N) = Hom_{D(I^∞-torsion)}(M, N);

Ext¹_{D(A)}(M, N) = Ext¹_{D(I^∞-torsion)}(M, N);

Ext²_{D(I^∞-torsion)}(M, N) ⟶ Ext²_{D(A)}(M, N) is not surjective in general;

the comparison functor D(I^∞-torsion) ⟶ D_{I^∞-torsion}(A) of Stacks 0A6N is not an equivalence in general.

Parts (1) and (2) are universally quantified and parts (3) and (4) are existential, exactly as in the source. The four conjuncts are Dualizing.bijective_derivedInclusion_map_singleFunctor, Dualizing.bijective_mapExt_one_powerTorsionModule, Dualizing.exists_not_surjective_mapExt_two_powerTorsionModule and Dualizing.exists_not_isEquivalence_powerTorsionComparison, each of which carries the tag for its own clause.

theorem bijective_hom_and_ext_one_and_exists_not_surjective_ext_two_and_not_isEquivalence :
    (∀ (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
        (M N : PowerTorsionModule.{u, v} A I hI),
        Function.Bijective fun f :
            (DerivedCategory.singleFunctor (PowerTorsionModule.{u, v} A I hI) 0).obj M ⟶
              (DerivedCategory.singleFunctor (PowerTorsionModule.{u, v} A I hI) 0).obj N ↦
          (powerTorsionModuleProperty A I hI).ι.mapDerivedCategory.map f) ∧
      (∀ (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
        (M N : PowerTorsionModule.{u, v} A I hI),
        Function.Bijective ((powerTorsionModuleProperty A I hI).ι.mapExtAddHom M N 1)) ∧
      (∃ (A : Type) (_ : CommRing A) (I : Ideal A) (hI : I.FG)
        (M N : PowerTorsionModule.{0, 0} A I hI),
        ¬ Function.Surjective
          ((powerTorsionModuleProperty A I hI).ι.mapExtAddHom M N 2)) ∧
      (∃ (A : Type) (_ : CommRing A) (I : Ideal A) (hI : I.FG),
        ¬ (powerTorsionComparison.{0, 0} A I hI).IsEquivalence)

Sources

LeanDualizing.derivedInclusion_adj_derivedPowerTorsion · Stacks.LocalCohomology.localCohomologyHomologyIsoColimitExt · Stacks.LocalCohomology.localCohomology_isHomotopyColimit_derivedHomPowers · Dualizing.localCohomology_isZero_of_isIso_smul · Dualizing.powerTorsionComparison · Dualizing.bijective_derivedInclusion_map_singleFunctor · Dualizing.bijective_mapExt_one_powerTorsionModule · Dualizing.exists_not_surjective_mapExt_two_powerTorsionModule

Section47.9 Local cohomology #

Section 47.9 of the Stacks Project, Tag 0952. 10 tags here are carried by 22 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0952, the section

Tag 0952 in the Stacks Project.

Stacks.LocalCohomology.powerTorsionComplexInjectiveResolutionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/ModelComparison/InjectiveResolution.lean, line 200. The attribute's comment: “RΓ_I(M) is the I-power-torsion subcomplex of an injective resolution”.

The I-power-torsion subcomplex of an injective resolution represents RΓ_I(M). Let A be a commutative ring, I ⊆ A a finitely generated ideal and M an A-module, and let M → J^• be a resolution of M by injective A-modules. Then the termwise I-power-torsion subcomplex ⋃_n J^•[I^n] represents derived I-power torsion RΓ_I(M) in D(A).

This is the computation that [Stacks, Tag 0952] is cited for. No Noetherian hypothesis is needed: a bounded-below complex of injectives is K-injective, and a right derived functor is computed by a K-injective resolution.

The isomorphism is the composite of: the identification of the two spellings of the termwise torsion subcomplex; the passage from the derived category to the homotopy category; the comparison of Γ_I on the homotopy category with its derived-category avatar; the unit of the total right derived functor RΓ_I at the K-injective complex J^•; the identification of Q(J^•) with M⟦0⟧; and the comparison functor of [Stacks, Tag 0A6N]. Every factor is invertible for formal reasons except the unit, which is invertible because J^• is K-injective.

def powerTorsionComplexInjectiveResolutionIso :
    DerivedCategory.Q.obj (Dualizing.powerTorsionComplex A I R.cocomplex) ≅
      derivedPowerTorsionObj.{u, u} A I hI M

Stacks.LocalCohomology.powerTorsionComplexComparison_comp_counit, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/ModelComparison/InjectiveResolution.lean, line 248. The attribute's comment: “the representation is compatible with the structure maps onto M”.

The comparison carries the structure map of RΓ_I(M) to the degreewise inclusion. Composing Stacks.LocalCohomology.powerTorsionComplexComparison with the structure map Stacks.LocalCohomology.derivedPowerTorsionObjCounit of RΓ_I(M) gives the degreewise inclusion Γ_I(J^•) ⟶ J^• of the termwise torsion subcomplex followed by the identification of Q(J^•) with M⟦0⟧.

This is the normalization of the counit of [Stacks, Tag 0A6L] read on the K-injective complex J^•.

lemma powerTorsionComplexComparison_comp_counit :
    powerTorsionComplexComparison A I hI M R ≫ derivedPowerTorsionObjCounit.{u, u} A I hI M =
      DerivedCategory.Q.map (powerTorsionComplexι A I R.cocomplex) ≫
        (injectiveResolutionIso A M R).hom

Declarations registered for the tag:

Dualizing.localCohomologyRightAdjoint, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/LocalCohomology/ModelComparison/InjectiveResolution.lean, line 339 (StacksFrontier): “the functor (47.9.0.1), right adjoint to the inclusion”.

Tag 0A6Q, an equation

Tag 0A6Q in the Stacks Project.

Dualizing.localCohomologyFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/Basic.lean, line 42. The attribute's comment: “the functor”.

Stacks 0A6Q. Local cohomology with support in V(I), valued in the full subcategory of derived objects with I-power-torsion cohomology.

noncomputable def localCohomologyFunctor
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG) :
    DerivedCategory (ModuleCat.{v} A) ⥤
      PowerTorsionDerivedCategory A I hI

Tag 0A6R, a lemma

Tag 0A6R in the Stacks Project.

Dualizing.localCohomologyRightAdjoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/RightAdjoint.lean, line 103. The attribute's comment: “local_cohomology_right_adjoint”.

Stacks 0A6R, local cohomology right adjoint. The inclusion of the derived category of objects with I-power-torsion cohomology has a right adjoint. This construction supplies the functor denoted RΓ_Z for Z = V(I).

noncomputable def localCohomologyRightAdjoint
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG) :
    Σ F : DerivedCategory (ModuleCat.{v} A) ⥤
        PowerTorsionDerivedCategory A I hI,
      (derivedPowerTorsionProperty A I hI).ι ⊣ F

Stacks.LocalCohomology.CechFormula.localCohomologyCechIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CechFormula/Basic.lean, line 330. The attribute's comment: “the Čech formula, functorially in K ∈ D(A); module universe = ring universe”.

Stacks 0A6R, the Čech formula. For a finitely generated ideal I = (f₁, …, f_r) of A, local cohomology RΓ_Z with Z = V(I) is, as a functor on D(A), the derived tensor product with the extended alternating Čech complex of f. Normalized by localCohomologyCechIso_comp_augmentation.

def localCohomologyCechIso (I : Ideal A) (hI : I.FG) (f : Fin r → A)
    (hf : Ideal.span (Set.range f) = I) :
    Dualizing.localCohomologyFunctor A I hI ⋙
        (Dualizing.derivedPowerTorsionProperty A I hI).ι ≅
      (canonicalDerivedTensorProductFunctor A).obj (cechRegularObject.{u, u} f)

Stacks.LocalCohomology.CechFormula.localCohomologyCechIso_comp_augmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CechFormula/Basic.lean, line 343. The attribute's comment: “normalization of the Čech formula against the local-cohomology counit”.

Stacks 0A6R, the normalization of the Čech formula. Composing it with the Čech comparison map gives the counit of the adjunction that defines local cohomology, which is what makes the isomorphism of localCohomologyCechIso the canonical one.

theorem localCohomologyCechIso_comp_augmentation (I : Ideal A) (hI : I.FG) (f : Fin r → A)
    (hf : Ideal.span (Set.range f) = I) :
    (localCohomologyCechIso A I hI f hf).hom ≫ cechTensorToId A f =
      (Dualizing.localCohomologyAdjunction A I hI).counit

Tag 0BJB, a lemma

Tag 0BJB in the Stacks Project.

Stacks.LocalCohomology.powerTorsionRestrictScalarsData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/RestrictScalars.lean, line 104. The attribute's comment: “the torsion-valued restriction functor”.

Restriction of scalars on power-torsion derived categories, together with its comparison to ordinary derived restriction after inclusion.

noncomputable def powerTorsionRestrictScalarsData
    {A : Type uA} {B : Type uB} [CommRing A] [CommRing B]
    (f : A →+* B) (I : Ideal A) (hI : I.FG) :
    Σ' F : Dualizing.PowerTorsionDerivedCategory B (I.map f) (hI.map f) ⥤
        Dualizing.PowerTorsionDerivedCategory A I hI,
      F ⋙ (Dualizing.derivedPowerTorsionProperty A I hI).ι ≅
        (Dualizing.derivedPowerTorsionProperty B (I.map f) (hI.map f)).ι ⋙
          (ModuleCat.restrictScalars.{max uA uB v} f).mapDerivedCategory

Stacks.LocalCohomology.localCohomologyRestrictScalarsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/RestrictScalars.lean, line 184. The attribute's comment: “the local-cohomology isomorphism”.

Stacks Project, Tag 0BJB. Local cohomology commutes with restriction of scalars, naturally in the derived B-module, as an isomorphism valued in the power-torsion derived category.

Both functors are right adjoint to K ↦ K ⊗ᴸ_A B on D_{I^∞-torsion}(A): for the left-hand side this is the composite of the local-cohomology adjunction over A with the extension–restriction adjunction, and for the right-hand side it is the composite of the local-cohomology adjunction over B with the restriction of the extension–restriction adjunction to the two power-torsion subcategories.

noncomputable def localCohomologyRestrictScalarsIso
    (f : A →+* B) (I : Ideal A) (hI : I.FG) :
    (ModuleCat.restrictScalars.{max uA uB v} f).mapDerivedCategory ⋙
        Dualizing.localCohomologyFunctor A I hI ≅
      Dualizing.localCohomologyFunctor B (I.map f) (hI.map f) ⋙
        powerTorsionRestrictScalars.{uA, uB, v} f I hI

Tag 0ALZ, a lemma

Tag 0ALZ in the Stacks Project.

Stacks.LocalCohomology.localCohomologyBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/BaseChange.lean, line 212.

Local cohomology with support in a finitely generated ideal commutes naturally with arbitrary derived extension of scalars.

def localCohomologyBaseChangeIso :
    Dualizing.localCohomologyFunctor A I hI ⋙
          (Dualizing.derivedPowerTorsionProperty A I hI).ι ⋙
          (derivedExtensionScalarsGeneral f).functor ≅
      (derivedExtensionScalarsGeneral f).functor ⋙
          Dualizing.localCohomologyFunctor B (I.map f) (hI.map f) ⋙
          (Dualizing.derivedPowerTorsionProperty B (I.map f) (hI.map f)).ι

Tag 0A6S, a lemma

Tag 0A6S in the Stacks Project.

Declarations registered for the tag:

Dualizing.localCohomology_isZero_of_isIso_smul, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/LocalCohomology/Vanishing.lean, line 31 (StacksFrontier).

Tag 0ALY, a lemma

Tag 0ALY in the Stacks Project.

Stacks.LocalCohomology.CechFormula.localCohomology_derivedTensorProduct_right, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CechFormula/TensorCompatibility.lean, line 189. The attribute's comment: “local cohomology on the right”.

Local cohomology of a derived tensor product is naturally the tensor product with local cohomology in the right variable.

def localCohomology_derivedTensorProduct_right
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG) :
    derivedTensorProductBifunctor A ⋙ localCohomologyEndofunctor A I hI ≅
      (Functor.prod (𝟭 _) (localCohomologyEndofunctor A I hI)) ⋙
        derivedTensorProductBifunctor A

Stacks.LocalCohomology.CechFormula.localCohomology_derivedTensorProduct_left, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CechFormula/TensorCompatibility.lean, line 199. The attribute's comment: “local cohomology on the left”.

Tensoring local cohomology in the right variable is naturally isomorphic to tensoring it in the left variable.

def localCohomology_derivedTensorProduct_left
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG) :
    (Functor.prod (𝟭 _) (localCohomologyEndofunctor A I hI)) ⋙
        derivedTensorProductBifunctor A ≅
      (Functor.prod (localCohomologyEndofunctor A I hI) (𝟭 _)) ⋙
        derivedTensorProductBifunctor A

Stacks.LocalCohomology.CechFormula.localCohomology_derivedTensorProduct_both, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CechFormula/TensorCompatibility.lean, line 212. The attribute's comment: “local cohomology in both factors”.

Applying local cohomology in both tensor factors is naturally equivalent to applying it in just the left factor.

def localCohomology_derivedTensorProduct_both
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG) :
    (Functor.prod (localCohomologyEndofunctor A I hI) (𝟭 _)) ⋙
        derivedTensorProductBifunctor A ≅
      (Functor.prod (localCohomologyEndofunctor A I hI)
        (localCohomologyEndofunctor A I hI)) ⋙
        derivedTensorProductBifunctor A

Stacks.LocalCohomology.CechFormula.derivedTensorProduct_mem_powerTorsion_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CechFormula/TensorCompatibility.lean, line 229. The attribute's comment: “torsion in the left factor”.

Tensoring on the right preserves a complex with I-power-torsion cohomology.

theorem derivedTensorProduct_mem_powerTorsion_left
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (K L : DerivedCategory (ModuleCat.{u} A))
    (hK : Dualizing.derivedPowerTorsionProperty A I hI K) :
    Dualizing.derivedPowerTorsionProperty A I hI
      ((derivedTensorProductBifunctor A).obj (K, L))

Stacks.LocalCohomology.CechFormula.derivedTensorProduct_mem_powerTorsion_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CechFormula/TensorCompatibility.lean, line 243. The attribute's comment: “torsion in the right factor”.

Tensoring on the left preserves a complex with I-power-torsion cohomology.

theorem derivedTensorProduct_mem_powerTorsion_right
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (K L : DerivedCategory (ModuleCat.{u} A))
    (hL : Dualizing.derivedPowerTorsionProperty A I hI L) :
    Dualizing.derivedPowerTorsionProperty A I hI
      ((derivedTensorProductBifunctor A).obj (K, L))

Tag 0BJC, a lemma

Tag 0BJC in the Stacks Project.

Dualizing.localCohomology_comp_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/Composition.lean, line 213. The attribute's comment: “the target of the composition of the local cohomology functors”.

[Stacks, Tag 0BJC]. Local cohomology supported on V(J) of an object with I-power-torsion cohomology has (I + J)-power-torsion cohomology, because V(I + J) = V(I) ∩ V(J).

theorem localCohomology_comp_torsion (A : Type u) [CommRing A] (I J : Ideal A)
    (hI : I.FG) (hJ : J.FG) (K : PowerTorsionDerivedCategory A I hI) :
    derivedPowerTorsionProperty A (I + J) (Submodule.FG.sup hI hJ)
      (((derivedPowerTorsionProperty A I hI).ι ⋙ localCohomologyFunctor A J hJ ⋙
        (derivedPowerTorsionProperty A J hJ).ι).obj K)

Dualizing.localCohomologyCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/Composition.lean, line 245. The attribute's comment: “the composition of the local cohomology functors”.

[Stacks, Tag 0BJC]. RΓ_Y ∘ RΓ_Z = RΓ_{Y ∩ Z} for Z = V(I) and Y = V(J): iterated local cohomology is local cohomology supported on V(I) ∩ V(J) = V(I + J). Both functors are right adjoint to the inclusion of the objects with (I + J)-power-torsion cohomology into those with I-power-torsion cohomology, so they agree.

noncomputable def localCohomologyCompIso (A : Type u) [CommRing A] (I J : Ideal A)
    (hI : I.FG) (hJ : J.FG) :
    localCohomologyFunctor.{u, v} A I hI ⋙ localCohomologyOnPowerTorsion A I J hI hJ ≅
      localCohomologyFunctor A (I + J) (Submodule.FG.sup hI hJ)

Dualizing.spectralSequencePageTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/CompositionSpectralSequence.lean, line 246. The attribute's comment: “the second page of the spectral sequence”.

[Stacks, Tag 0BJC], the second page. At (p, q) the second page of the spectral sequence is H^p_Y(H^q_Z(K)), naturally in K: the q-th local cohomology module of K supported on Z = V(I), placed in degree zero, has its p-th local cohomology supported on Y = V(J) taken.

This is Stacks.Cohomology.LerayCard.pageTwoNatIsoDerived for Φ = RΓ_Y, precomposed with RΓ_Z; no Noetherian hypothesis and no comparison of models of local cohomology is involved.

def spectralSequencePageTwoIso (p q : ℤ) :
    spectralSequence.{u, v} A I J hI hJ ⋙ SpectralSequence.pageFunctor _ _ 2 2 ⋙
        HomologicalComplex.eval _ _ (p, q) ≅
      localCohomologyFunctorPlus.{u, v} A I hI ⋙
        DerivedCategory.Plus.homologyFunctor (ModuleCat.{v} A) q ⋙
          DerivedCategory.Plus.singleFunctor (ModuleCat.{v} A) 0 ⋙
            localCohomologyFunctorPlus.{u, v} A J hJ ⋙
              DerivedCategory.Plus.homologyFunctor (ModuleCat.{v} A) p

Dualizing.abutsTo_spectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/CompositionSpectralSequence.lean, line 269. The attribute's comment: “the convergence of the spectral sequence”.

[Stacks, Tag 0BJC], the convergence. For K in D⁺(A) the spectral sequence has an infinity page at every bidegree and the terms E_∞^{p, n-p} are the successive quotients of a finite decreasing filtration of H^n_{Y ∩ Z}(K).

Boundedness of the spectral object comes from Stacks.Cohomology.LerayTruncation.isBounded_cohomologySpectralObjectFunctor_obj, whose hypothesis is left t-exactness of RΓ_Y — that is Dualizing.isGE_localCohomologyFunctorPlus_obj. The abutment the generic theorem produces is H^n(RΓ_Y(RΓ_Z K)), and Dualizing.localCohomologyFunctorPlusCompIso identifies it with H^n_{Y ∩ Z}(K).

theorem abutsTo_spectralSequence (K : DerivedCategory.Plus (ModuleCat.{v} A)) :
    SpectralSequence.AbutsTo ((spectralSequence.{u, v} A I J hI hJ).obj K)
      (fun n : ℤ ↦ (DerivedCategory.Plus.homologyFunctor (ModuleCat.{v} A) n).obj
        ((localCohomologyFunctorPlus.{u, v} A (I + J) (Submodule.FG.sup hI hJ)).obj K))

Dualizing.localCohomology_comp_spectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/CompositionSpectralSequence.lean, line 305. The attribute's comment: “all five clauses conjoined; the two isomorphisms of functors appear as Nonempty, the isomorphisms themselves being the declarations that carry the tag for those clauses”.

Stacks 0BJC, all five clauses. Let A be a ring, let I, J ⊆ A be finitely generated ideals and set Z = V(I), Y = V(J). Then

Z ∩ Y = V(I + J);

RΓ_Y carries an object with I-power-torsion cohomology to one with (I + J)-power-torsion cohomology, so that RΓ_Y ∘ RΓ_Z is a functor D(A) → D_{(I + J)^∞-torsion}(A);

RΓ_Y ∘ RΓ_Z ≅ RΓ_{Y ∩ Z} as functors D(A) → D_{(I + J)^∞-torsion}(A);

for K in D⁺(A) the second page of the spectral sequence of the composition is E₂^{p, q} = H^p_Y(H^q_Z(K)), naturally in K; and

that spectral sequence abuts to H^{p + q}_{Y ∩ Z}(K).

Clauses (3) and (4) are isomorphisms of functors, so they appear here as Nonempty; the isomorphisms themselves are Dualizing.localCohomologyCompIso and Dualizing.spectralSequencePageTwoIso, each of which carries the tag for its own clause, as do PrimeSpectrum.zeroLocus_sup for (1), Dualizing.localCohomology_comp_torsion for (2) and Dualizing.abutsTo_spectralSequence for (5). Nothing here is Noetherian and no comparison of the two models of local cohomology is involved: everything is the coreflection model RΓ_{V(I)} of [Stacks, Tag 0A6Q].

theorem localCohomology_comp_spectralSequence :
    PrimeSpectrum.zeroLocus (I : Set A) ∩ PrimeSpectrum.zeroLocus (J : Set A) =
        PrimeSpectrum.zeroLocus ((I + J : Ideal A) : Set A) ∧
      (∀ K : PowerTorsionDerivedCategory.{u, v} A I hI,
        derivedPowerTorsionProperty A (I + J) (Submodule.FG.sup hI hJ)
          (((derivedPowerTorsionProperty A I hI).ι ⋙ localCohomologyFunctor A J hJ ⋙
            (derivedPowerTorsionProperty A J hJ).ι).obj K)) ∧
      Nonempty (localCohomologyFunctor.{u, v} A I hI ⋙
          localCohomologyOnPowerTorsion A I J hI hJ ≅
        localCohomologyFunctor A (I + J) (Submodule.FG.sup hI hJ)) ∧
      (∀ p q : ℤ, Nonempty (spectralSequence.{u, v} A I J hI hJ ⋙
          SpectralSequence.pageFunctor _ _ 2 2 ⋙ HomologicalComplex.eval _ _ (p, q) ≅
        localCohomologyFunctorPlus.{u, v} A I hI ⋙
          DerivedCategory.Plus.homologyFunctor (ModuleCat.{v} A) q ⋙
            DerivedCategory.Plus.singleFunctor (ModuleCat.{v} A) 0 ⋙
              localCohomologyFunctorPlus.{u, v} A J hJ ⋙
                DerivedCategory.Plus.homologyFunctor (ModuleCat.{v} A) p)) ∧
      ∀ K : DerivedCategory.Plus (ModuleCat.{v} A),
        SpectralSequence.AbutsTo ((spectralSequence.{u, v} A I J hI hJ).obj K)
          (fun n : ℤ ↦ (DerivedCategory.Plus.homologyFunctor (ModuleCat.{v} A) n).obj
            ((localCohomologyFunctorPlus.{u, v} A (I + J) (Submodule.FG.sup hI hJ)).obj K))

Declarations registered for the tag:

PrimeSpectrum.zeroLocus_sup registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/LocalCohomology.lean, line 403 (StacksFrontier): “intersection_of_zero_loci”. References: EGA I (1.1.2), “(iii), special case”; EGA I (1.1.5), “special case”.

Tag 0AM0, a lemma

Tag 0AM0 in the Stacks Project.

Dualizing.powerTorsionDerivedEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology.lean, line 332.

Stacks 0AM0. Flat base change and restriction of scalars are quasi-inverse on the derived categories of objects with power-torsion cohomology.

theorem powerTorsionDerivedEquivalence
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
    (I : Ideal A) (hI : I.FG) (hflat : Module.Flat A B)
    (hquot : Function.Bijective
      (Ideal.quotientMap (I.map (algebraMap A B)) (algebraMap A B)
        Ideal.le_comap_map)) :
    ∃ e : PowerTorsionDerivedCategory.{u, max u v w} A I hI ≌
        PowerTorsionDerivedCategory.{v, max u v w} B
          (I.map (algebraMap A B)) (Ideal.FG.map hI (algebraMap A B)),
      Nonempty (e.functor ⋙
          (derivedPowerTorsionProperty B (I.map (algebraMap A B))
            (Ideal.FG.map hI (algebraMap A B))).ι ≅
        (derivedPowerTorsionProperty A I hI).ι ⋙
          (CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, v, w}
            (algebraMap A B)).functor) ∧
      Nonempty (e.inverse ⋙ (derivedPowerTorsionProperty A I hI).ι ≅
        (derivedPowerTorsionProperty B (I.map (algebraMap A B))
          (Ideal.FG.map hI (algebraMap A B))).ι ⋙
          (ModuleCat.restrictScalars.{max u v w} (algebraMap A B)).mapDerivedCategory)

Tag 05EH, a lemma

Tag 05EH in the Stacks Project.

Dualizing.PowerTorsionBaseChange.bijective_extBaseChange_of_powerTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Ext.lean, line 913. The attribute's comment: “Ext”.

Stacks 05EH. The canonical scalar-extension map on Ext groups from an I-power-torsion module is bijective in every degree.

theorem bijective_extBaseChange_of_powerTorsion
    (I : Ideal A) (hI : I.FG) (hflat : Module.Flat A B)
    (hquot : Function.Bijective
      (Ideal.quotientMap (I.map (algebraMap A B)) (algebraMap A B)
        Ideal.le_comap_map))
    (M N : ModuleCat.{max uA (max uR uM)} A) (hM : IsIPowerTorsion A M I) (i : ℕ) :
    let F := ModuleCat.extendScalars.{uR, uA, max uA (max uR uM)} (algebraMap A B)
    letI : F.IsLeftAdjoint :=
      (ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA}
        (algebraMap A B)).isLeftAdjoint
    letI : PreservesFiniteLimits F :=
      preservesFiniteLimits_extendScalars_of_flat.{uR, uA, uM} A B hflat
    letI : F.Additive := F.additive_of_preserves_binary_products
    letI := CategoryTheory.HasExt.standard (ModuleCat.{max uA (max uR uM)} A)
    letI := CategoryTheory.HasExt.standard (ModuleCat.{max uA (max uR uM)} B)
    Function.Bijective (F.mapExtAddHom M N i)

Dualizing.PowerTorsionBaseChange.isIso_derivedHomBaseChangeMate_of_powerTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/PowerTorsionDerivedHom.lean, line 386. The attribute's comment: “derived Hom”.

Stacks 05EH. Derived Hom from a complex with I-power-torsion cohomology is unchanged under flat base change which is an isomorphism modulo I.

theorem isIso_derivedHomBaseChangeMate_of_powerTorsion
    (A : Type uR) (B : Type uA) [CommRing A] [CommRing B] [Algebra A B]
    (I : Ideal A) (hI : I.FG) (hflat : Module.Flat A B)
    (hquot : Function.Bijective
      (Ideal.quotientMap (I.map (algebraMap A B)) (algebraMap A B)
        Ideal.le_comap_map))
    :
    letI : (ModuleCat.extendScalars.{uR, uA, max uA (max uR uM)} (algebraMap A B)).IsLeftAdjoint :=
      (ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA}
        (algebraMap A B)).isLeftAdjoint
    letI : (ModuleCat.restrictScalars.{max uA (max uR uM), uR, uA}
        (algebraMap A B)).IsRightAdjoint :=
      (ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA}
        (algebraMap A B)).isRightAdjoint
    letI : (ModuleCat.restrictScalars.{max uA (max uR uM), uR, uA}
        (algebraMap A B)).IsLeftAdjoint :=
      (ModuleCat.restrictCoextendScalarsAdj.{max uR uM, uR, uA}
        (algebraMap A B)).isLeftAdjoint
    ∀ (F : DerivedCategory (ModuleCat.{max uA (max uR uM)} A) ⥤
      DerivedCategory (ModuleCat.{max uA (max uR uM)} B))
    (comparison : DerivedCategory.Q ⋙ F ⟶
      (ModuleCat.extendScalars.{uR, uA, max uA (max uR uM)} (algebraMap A B)).mapHomologicalComplex
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    [F.IsLeftDerivedFunctor comparison
      (HomologicalComplex.quasiIso (ModuleCat.{max uA (max uR uM)} A) (ComplexShape.up ℤ))]
    (K L : DerivedCategory (ModuleCat.{max uA (max uR uM)} A)),
    Dualizing.derivedPowerTorsionProperty A I hI K →
    IsIso ((Stacks.DerivedHom.ExtensionOfScalars.derivedHomBaseChangeMate.{uR, uA, uM}
      (algebraMap A B) F comparison).app (Opposite.op K, L))

Sources

LeanStacks.LocalCohomology.powerTorsionComplexInjectiveResolutionIso · Stacks.LocalCohomology.powerTorsionComplexComparison_comp_counit · Dualizing.localCohomologyRightAdjoint · Dualizing.localCohomologyFunctor · Stacks.LocalCohomology.CechFormula.localCohomologyCechIso · Stacks.LocalCohomology.CechFormula.localCohomologyCechIso_comp_augmentation · Stacks.LocalCohomology.powerTorsionRestrictScalarsData · Stacks.LocalCohomology.localCohomologyRestrictScalarsIso

Section47.10 Local cohomology for Noetherian rings #

Section 47.10 of the Stacks Project, Tag 0BJD. 4 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A6U, an equation

Tag 0A6U in the Stacks Project.

Dualizing.compareTorsionFunctors, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomologyDualizing/Basic.lean, line 159.

Stacks 0A6U. The canonical natural transformation from derived power torsion followed by the comparison functor to local cohomology with support in V(I).

noncomputable def compareTorsionFunctors
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG) :
    (derivedPowerTorsion.{u, v} A I hI ⋙
      powerTorsionComparison.{u, max u v} A I hI) ⟶
      localCohomologyFunctor.{u, max u v} A I hI

Tag 0955, a lemma

Tag 0955 in the Stacks Project.

Dualizing.TorsionCounit.isIso_derivedPowerTorsionCounit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/ModelComparison/Noetherian.lean, line 430. The attribute's comment: “part (1)”.

Stacks 0955, part (1). Let A be a Noetherian ring and I ⊆ A a finitely generated ideal. The counit RΓ_I(K) ⟶ K of [Stacks, Tag 0A6L] is an isomorphism at every object K of D(A) whose cohomology modules are I-power torsion.

The object is represented by a K-injective complex with injective terms, where the counit is the degreewise torsion inclusion.

theorem isIso_derivedPowerTorsionCounit_app
    (K : PowerTorsionDerivedCategory.{u, max u v} A I hI) :
    IsIso ((derivedPowerTorsionCounit.{u, v} A I hI).app K.obj)

Dualizing.TorsionCounit.isEquivalence_powerTorsionComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/ModelComparison/Noetherian.lean, line 458. The attribute's comment: “part (2)”.

Stacks 0955, part (2). For a Noetherian ring the comparison functor D(I^∞-torsion) ⥤ D_{I^∞-torsion}(A) of [Stacks, Tag 0A6N] is an equivalence.

theorem isEquivalence_powerTorsionComparison :
    (powerTorsionComparison.{u, max u v} A I hI).IsEquivalence

Dualizing.TorsionCounit.isIso_compareTorsionFunctors_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/ModelComparison/Noetherian.lean, line 549. The attribute's comment: “part (3)”.

Stacks 0955, part (3). Let A be a Noetherian ring and I ⊆ A a finitely generated ideal. The comparison RΓ_I ⟶ RΓ_Z of [Stacks, Tag 0A6U] is an isomorphism at every object of D(A), with no torsion or boundedness hypothesis.

Evaluate the naturality square of the comparison at the local cohomology counit c : ι(RΓ_Z(K)) ⟶ K. Its source has I-power-torsion cohomology, so the comparison is invertible there by part (1); RΓ_Z(c) is invertible because RΓ_Z is a coreflection; and RΓ_I(c) is invertible because the counit is universal among morphisms from torsion objects.

theorem isIso_compareTorsionFunctors_app
    (K : DerivedCategory (ModuleCat.{max u v} A)) :
    IsIso ((compareTorsionFunctors.{u, v} A I hI).app K)

Tag 0956, a lemma

Tag 0956 in the Stacks Project.

Stacks.LocalCohomology.extendedCechComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/ModelComparison/ExtendedCech.lean, line 157.

Stacks 0956. Let A be a Noetherian ring, let I = (f₁, …, f_r) be an ideal of A and let Z = V(I). For every A-module M there are canonical isomorphisms RΓ_I(M) ≅ C^•(f₁, …, f_r; M) ≅ RΓ_Z(M) in D(A), the middle term being the extended alternating Čech complex; the first carries the Čech augmentation to the structure map of RΓ_I(M) and the second carries the local-cohomology counit back to the Čech augmentation, which is what makes the pair canonical.

def extendedCechComparison (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
    {r : ℕ} (f : Fin r → A) (hIf : Ideal.span (Set.range f) = I)
    (M : ModuleCat.{max u v} A) :
    { e : (derivedPowerTorsionObj.{u, v} A I (Ideal.fg_of_isNoetherianRing I) M ≅
              extendedCechObject f M) ×
            (extendedCechObject f M ≅
              (localCohomologyOnModules.{u, max u v} A I
                (Ideal.fg_of_isNoetherianRing I)).obj M) //
        e.1.hom ≫ extendedCechAugmentationHom f M =
            derivedPowerTorsionObjCounit.{u, v} A I (Ideal.fg_of_isNoetherianRing I) M ∧
          e.2.hom ≫ (Dualizing.localCohomologyAdjunction A I
              (Ideal.fg_of_isNoetherianRing I)).counit.app
                ((DerivedCategory.singleFunctor (ModuleCat.{max u v} A) 0).obj M) =
            extendedCechAugmentationHom f M }

Tag 0957, a lemma

Tag 0957 in the Stacks Project.

Dualizing.localCohomologyOfRingBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomologyNoetherian/ChangeOfRings.lean, line 86. The attribute's comment: “base change on regular modules”.

Stacks 0957. Local cohomology of the regular module commutes with derived extension of scalars along a homomorphism of commutative rings, for a finitely generated ideal.

def localCohomologyOfRingBaseChangeIso (A B : Type uA) [CommRing A] [CommRing B]
    (f : A →+* B) (I : Ideal A) (hI : I.FG) :
    (derivedExtensionScalarsGeneral.{uA, 0, uA} f).functor.obj (localCohomologyOfRing A I hI) ≅
      localCohomologyOfRing B (I.map f) (hI.map f)

Dualizing.localCohomologyOfRingLiftedBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomologyNoetherian/ChangeOfRings.lean, line 129. The attribute's comment: “base change across universes”.

Stacks 0957. The change-of-rings isomorphism for local cohomology of the regular module, for two rings in independent universes, after transporting both regular modules into a common module universe.

def localCohomologyOfRingLiftedBaseChangeIso (A : Type uA) (B : Type uB) [CommRing A]
    [CommRing B] (f : A →+* B) (I : Ideal A) (hI : I.FG) :
    (derivedExtensionScalarsGeneral.{uA, max uA uB, uB} f).functor.obj
        (localCohomologyOfRingLifted.{uA, max uA uB} A I hI) ≅
      localCohomologyOfRingLifted.{uB, max uA uB} B (I.map f) (hI.map f)

Dualizing.derivedPowerTorsionOfRingBaseChangeIsoLocalCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomologyNoetherian/ChangeOfRingsTorsion.lean, line 142. The attribute's comment: “first equality: RΓ_I(A) ⊗ᴸ B = RΓ_Z(A) ⊗ᴸ B”.

Stacks 0957, the first equality. RΓ_I(A) ⊗ᴸ_A B ≅ RΓ_Z(A) ⊗ᴸ_A B: derived extension of scalars applied to the identification of the two torsion models over the Noetherian ring A.

def derivedPowerTorsionOfRingBaseChangeIsoLocalCohomology (A B : Type uA) [CommRing A]
    [CommRing B] [IsNoetherianRing A] (f : A →+* B) (I : Ideal A) (hI : I.FG) :
    (derivedExtensionScalarsGeneral.{uA, 0, uA} f).functor.obj
        (derivedPowerTorsionOfRing A I hI) ≅
      (derivedExtensionScalarsGeneral.{uA, 0, uA} f).functor.obj
        (localCohomologyOfRing A I hI)

Dualizing.localCohomologyOfRingIsoDerivedPowerTorsionOfRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomologyNoetherian/ChangeOfRingsTorsion.lean, line 155. The attribute's comment: “last equality: RΓ_Y(B) = RΓ_{IB}(B)”.

Stacks 0957, the last equality. RΓ_Y(B) ≅ RΓ_{IB}(B) for Y = V(IB): the identification of the two torsion models over the Noetherian ring B, read backwards at the ideal IB = Ideal.map f I.

def localCohomologyOfRingIsoDerivedPowerTorsionOfRing (A B : Type uA) [CommRing A] [CommRing B]
    [IsNoetherianRing B] (f : A →+* B) (I : Ideal A) (hI : I.FG) :
    localCohomologyOfRing B (I.map f) (hI.map f) ≅
      derivedPowerTorsionOfRing B (I.map f) (hI.map f)

Dualizing.derivedPowerTorsionOfRingBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomologyNoetherian/ChangeOfRingsTorsion.lean, line 169. The attribute's comment: “the four-term chain, composed, for two rings in one universe”.

Stacks 0957, the whole chain. For a homomorphism f : A → B of Noetherian rings and a finitely generated ideal I ⊆ A, there is an isomorphism RΓ_I(A) ⊗ᴸ_A B ≅ RΓ_{IB}(B) in D(B), obtained by composing the three isomorphisms of the source: the first equality, the change-of-rings isomorphism Dualizing.localCohomologyOfRingBaseChangeIso, and the last equality.

def derivedPowerTorsionOfRingBaseChangeIso (A B : Type uA) [CommRing A] [CommRing B]
    [IsNoetherianRing A] [IsNoetherianRing B] (f : A →+* B) (I : Ideal A) (hI : I.FG) :
    (derivedExtensionScalarsGeneral.{uA, 0, uA} f).functor.obj
        (derivedPowerTorsionOfRing A I hI) ≅
      derivedPowerTorsionOfRing B (I.map f) (hI.map f)

Dualizing.derivedPowerTorsionOfRingLiftedBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomologyNoetherian/ChangeOfRingsTorsion.lean, line 181. The attribute's comment: “the four-term chain, composed, across universes”.

Stacks 0957, the whole chain, for two rings in independent universes, after transporting both regular modules into a common module universe.

def derivedPowerTorsionOfRingLiftedBaseChangeIso (A : Type uA) (B : Type uB) [CommRing A]
    [CommRing B] [IsNoetherianRing A] [IsNoetherianRing B] (f : A →+* B) (I : Ideal A)
    (hI : I.FG) :
    (derivedExtensionScalarsGeneral.{uA, max uA uB, uB} f).functor.obj
        (derivedPowerTorsionOfRingLifted.{uA, max uA uB} A I hI) ≅
      derivedPowerTorsionOfRingLifted.{uB, max uA uB} B (I.map f) (hI.map f)

Sources

LeanDualizing.compareTorsionFunctors · Dualizing.TorsionCounit.isIso_derivedPowerTorsionCounit_app · Dualizing.TorsionCounit.isEquivalence_powerTorsionComparison · Dualizing.TorsionCounit.isIso_compareTorsionFunctors_app · Stacks.LocalCohomology.extendedCechComparison · Dualizing.localCohomologyOfRingBaseChangeIso · Dualizing.localCohomologyOfRingLiftedBaseChangeIso · Dualizing.derivedPowerTorsionOfRingBaseChangeIsoLocalCohomology

Section47.11 Depth #

Section 47.11 of the Stacks Project, Tag 0AVY. 6 tags here are carried by 15 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AVZ, a lemma

Tag 0AVZ in the Stacks Project.

ModuleCat.subsingleton_ext_of_lt_ideal_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DepthLemmas/Ext.lean, line 131. The attribute's comment: “Ext vanishing below depth for modules annihilated by an ideal power”. References: EGA 0 (16.4.4), “Ext^i(k”; SGA 2 III (2.2), “Clause (a), special case”; SGA 2 III (2.4), “(4)⇒(2)”; SGA 2 III (2.8), “Ext^i(k”; SGA 2 IV (5.3), “Ext^i_A(k, special case”.

Ext^i_R(N, M) vanishes below the I-depth of M for every finite module N annihilated by a power of I, not just for N = R ⧸ I: a power of I annihilating N forces the support of N into V(I), and Rees' theorem turns the vanishing of Ext^j_R(R/I, M) below the depth into an M-regular sequence in I long enough to kill Ext^i_R(N, M).

theorem ModuleCat.subsingleton_ext_of_lt_ideal_depth [IsNoetherianRing R] [Small.{v} R]
    (I : Ideal R) (M N : ModuleCat.{v} R) [Module.Finite R M] [Module.Finite R N]
    (hIM : I • (⊤ : Submodule R M) ≠ ⊤) {k : ℕ} (hk : I ^ k ≤ Module.annihilator R N) {i : ℕ}
    (hi : (i : ℕ∞) < Module.depth R I M) :
    Subsingleton (Ext N M i)

Module.subsingleton_ext_of_lt_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/DepthVanishing/DepthEqLocalCohomology.lean, line 79. The attribute's comment: “Ext vanishing below depth for modules annihilated by an ideal power”. References: SGA 2 III (2.2), “(a), Noetherian f.g.”; SGA 2 IV (5.3), “Ext^i(M,A)=0 for i<n”; SGA 2 III (3.3), “affine (iv)⇒(v)”.

Ext from a finite module annihilated by a power of I vanishes below the I-depth.

theorem subsingleton_ext_of_lt_depth
    (R : Type u) [CommRing R] [IsNoetherianRing R] [Small.{v} R]
    (I : Ideal R) (M N : ModuleCat.{v} R)
    [Module.Finite R M] [Module.Finite R N]
    (hIM : I • (⊤ : Submodule R M) ≠ ⊤)
    (hN : ∃ n : ℕ, I ^ n ≤ Module.annihilator R N)
    (i : ℕ) (hi : (i : ℕ∞) < Module.depth R I M) :
    Subsingleton (Ext N M i)

Stacks.LocalCohomology.depth_eq_sInf_nontrivial_localCohomologyWithSupportIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/DepthVanishing/DepthEqLocalCohomology.lean, line 417. The attribute's comment: “equality of depth and the first nonzero local-cohomology degree”.

Depth is the first degree with nonzero local cohomology supported on V(I).

theorem depth_eq_sInf_nontrivial_localCohomologyWithSupportIn
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (I : Ideal R) (M : ModuleCat.{max u v} R) [Module.Finite R M]
    (hIM : I • (⊤ : Submodule R M) ≠ ⊤) :
    Module.depth R I M =
      sInf {n : ℕ∞ | ∃ i : ℕ, n = (i : ℕ∞) ∧
      Nontrivial
          (localCohomologyWithSupportIn
            R (PrimeSpectrum.zeroLocus (I : Set R))
              ((DerivedCategory.singleFunctor (ModuleCat.{max u v} R) 0).obj M)
              (i : ℤ))}

Stacks.LocalCohomology.depth_eq_sInf_nontrivial_ext_and_localCohomology_and_subsingleton_ext, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/DepthVanishing/DepthEqLocalCohomology.lean, line 576. The attribute's comment: “the three-way equality and the moreover clause conjoined, with the local cohomology of the third quantity in the RΓ_{V(I)} model”. References: SGA 2 III (2.3), “special case”; SGA 2 III (2.4), “(2)⇔(4)”; SGA 2 IV (5.3), “Ext^i_A(k, special case”; SGA 2 VII (1.2), “(i) ⇔ (iii)”.

Let R be a Noetherian ring, I ⊆ R an ideal and M a finite R-module with IM ≠ M. Then the three integers of the source are equal — depth_I(M), the least i with Ext^i_R(R/I, M) ≠ 0, and the least i with H^i_{V(I)}(M) ≠ 0, each of the last two read as an infimum in ℕ∞ — and moreover Ext^i_R(N, M) = 0 for every i below depth_I(M) and every finite R-module N annihilated by a power of I.

The source's H^i_I(M), the cohomology of derived I-power torsion, is H^i_{V(I)}(M) here: the two agree because R is Noetherian, by Stacks.LocalCohomology.isIso_compareSectionsWithSupportLocalCohomology_app ([Stacks, Tag 0955]).

theorem depth_eq_sInf_nontrivial_ext_and_localCohomology_and_subsingleton_ext
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (I : Ideal R) (M : ModuleCat.{u} R) [Module.Finite R M]
    (hIM : I • (⊤ : Submodule R M) ≠ ⊤) :
    Module.depth R I M =
        sInf {n : ℕ∞ | ∃ i : ℕ, n = (i : ℕ∞) ∧
          Nontrivial (Abelian.Ext (ModuleCat.of R (Shrink.{u} (R ⧸ I))) M i)} ∧
      Module.depth R I M =
        sInf {n : ℕ∞ | ∃ i : ℕ, n = (i : ℕ∞) ∧
          Nontrivial (localCohomologyWithSupportIn R (PrimeSpectrum.zeroLocus (I : Set R))
            ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj M) (i : ℤ))} ∧
      ∀ (N : ModuleCat.{u} R) [Module.Finite R N], (∃ k : ℕ, I ^ k ≤ Module.annihilator R N) →
        ∀ i : ℕ, (i : ℕ∞) < Module.depth R I M → Subsingleton (Abelian.Ext N M i)

Declarations registered for the tag:

Module.depth_eq_sInf_nontrivial_ext, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/LocalCohomologyNoetherian/Depth.lean, line 197 (StacksFrontier): “equality of depth and the first nonzero Ext degree”.

Tag 0BUV, a lemma

Tag 0BUV in the Stacks Project.

Declarations registered for the tag:

Module.min_depth_le_depth_of_exact, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/Depth.lean, line 313 (StacksFrontier): “middle_depth_bound, quotient_depth_bound and submodule_depth_bound: the three conjuncts of this inequality”.

Tag 0BUW, a lemma

Tag 0BUW in the Stacks Project.

Declarations registered for the tag:

Module.depth_quotSMulTop_succ_eq_depth_and_exists_isRegular_append, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/Depth.lean, line 318 (StacksFrontier).

Tag 0BUX, a lemma

Tag 0BUX in the Stacks Project.

Dualizing.supportDim_quotient_add_depth_eq_supportDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Depth.lean, line 187. References: EGA 0 (16.5.9), “r = depth_p(M)”.

Stacks Project, Tag 0BUX. The depth of a finite Cohen--Macaulay module along a proper ideal is the drop in the dimension of its support on passing to the quotient by that ideal.

theorem supportDim_quotient_add_depth_eq_supportDim
    {R M : Type*} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [AddCommGroup M] [Module R M] [Module.Finite R M]
    (I : Ideal R) (hI : I ≠ ⊤) (hM : Module.IsCohenMacaulayAtMaximalIdeal R M) :
    Module.supportDim R (M ⧸ I • (⊤ : Submodule R M)) +
        (Module.depth R I M : WithBot ℕ∞) =
      Module.supportDim R M

Tag 0BUY, a lemma

Tag 0BUY in the Stacks Project.

Dualizing.ringKrullDim_fiber_le_depth_add_ringKrullDim_quotient_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Depth.lean, line 282.

Let R → S be a flat local homomorphism with Noetherian local target. If its closed fibre is Cohen--Macaulay, then the depth of S along an ideal I is at least the difference between the dimension of the closed fibre and that of its quotient by I.

theorem ringKrullDim_fiber_le_depth_add_ringKrullDim_quotient_of_flat
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    [IsNoetherianRing S] [IsLocalRing R] [IsLocalRing S]
    [Module.Flat R S] [IsLocalHom (algebraMap R S)] (I : Ideal S)
    (hCM : Module.IsCohenMacaulayAtMaximalIdeal S
      (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))) :
    I = ⊤ ∨
      ringKrullDim (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) ≤
        (Module.depth S I S : WithBot ℕ∞) +
        ringKrullDim
            (S ⧸ (Ideal.map (algebraMap R S) (maximalIdeal R) ⊔ I))

Tag 0AW0, a lemma

Tag 0AW0 in the Stacks Project.

Stacks.Duality.supportLocalCohomology_torsion_higher, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DivideByTorsion.lean, line 155. The attribute's comment: “part (2), higher cohomology of the torsion submodule”.

Stacks 0AW0, part (2). Higher local cohomology with support in V(I) of torsion vanishes: H^p_Z(M[I^∞]) = 0 for p > 0.

theorem supportLocalCohomology_torsion_higher
    (A : Type u) [CommRing A]
    (I : Ideal A) (hI : I.FG) (M : ModuleCat.{max u v} A)
    (p : ℤ) (hp : 0 < p) :
    IsZero ((supportLocalCohomology.{u, v} A I hI p).obj
      (ModuleCat.of A (Ideal.primaryComponent M I)))

Stacks.Duality.supportLocalCohomology_quotient_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DivideByTorsion.lean, line 325. The attribute's comment: “part (2), degree zero”.

Stacks 0AW0, part (2). Quotienting by I-power torsion kills zeroth local cohomology with support in V(I): H^0_Z(M/M[I^∞]) = 0.

theorem supportLocalCohomology_quotient_zero
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (M : ModuleCat.{max u v} A) :
    IsZero ((supportLocalCohomology.{u, v} A I hI 0).obj
      (ModuleCat.of A (M ⧸ Ideal.primaryComponent M I)))

Stacks.Duality.idealLocalCohomology_zero_iso_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionQuotient.lean, line 298. The attribute's comment: “H^0_I is the torsion submodule”.

Stacks 0AW0. The zeroth local cohomology H^0_I(M) of M for the I-power torsion theory is the I-power-torsion submodule M[I^∞] of M, by an isomorphism compatible with the canonical map of H^0_I(M) into M.

theorem idealLocalCohomology_zero_iso_torsion
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (M : ModuleCat.{max u v} A) :
    ∃ e : (idealLocalCohomology.{u, v} A I hI 0).obj M ≅
        ModuleCat.of A (Ideal.primaryComponent M I),
      e.hom ≫ ModuleCat.ofHom (Submodule.subtype (Ideal.primaryComponent M I)) =
        idealLocalCohomologyToModule.{u, v} A I hI M

Stacks.Duality.idealLocalCohomology_quotient_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionQuotient.lean, line 325. The attribute's comment: “part (1), degree zero”.

Stacks 0AW0, part (1). Quotienting by the I-power-torsion submodule kills the zeroth local cohomology for the I-power torsion theory: H^0_I(M/M[I^∞]) = 0.

theorem idealLocalCohomology_quotient_zero
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (M : ModuleCat.{max u v} A) :
    IsZero ((idealLocalCohomology.{u, v} A I hI 0).obj
      (ModuleCat.of A (M ⧸ Ideal.primaryComponent M I)))

Stacks.Duality.idealLocalCohomology_torsion_higher, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionQuotient.lean, line 344. The attribute's comment: “part (1), higher cohomology of the torsion submodule”.

Stacks 0AW0, part (1). Over a Noetherian ring the higher local cohomology of the I-power-torsion submodule vanishes for the I-power torsion theory: H^p_I(M[I^∞]) = 0 for p > 0.

The source states this for an arbitrary ring. The Noetherian hypothesis added here cannot be removed: for a finitely generated ideal of a non-Noetherian ring the assertion is false, by part (3) of [Stacks, Tag 0A6P]. See the module docstring.

theorem idealLocalCohomology_torsion_higher
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (I : Ideal A) (hI : I.FG) (M : ModuleCat.{max u v} A)
    (p : ℤ) (hp : 0 < p) :
    IsZero ((idealLocalCohomology.{u, v} A I hI p).obj
      (ModuleCat.of A (Ideal.primaryComponent M I)))

Stacks.Duality.idealLocalCohomology_quotient_map_higher, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionQuotient.lean, line 373. The attribute's comment: “part (1), higher cohomology of the quotient”.

Stacks 0AW0, part (1). Over a Noetherian ring the quotient map M ⟶ M/M[I^∞] induces an isomorphism H^p_I(M) ≅ H^p_I(M/M[I^∞]) in every positive degree.

The source states this for an arbitrary ring. The Noetherian hypothesis added here cannot be removed: taking an I-power-torsion M, so that M/M[I^∞] = 0, turns the assertion into the vanishing of Stacks.Duality.idealLocalCohomology_torsion_higher, which part (3) of [Stacks, Tag 0A6P] refutes over a non-Noetherian ring. See the module docstring.

theorem idealLocalCohomology_quotient_map_higher
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (I : Ideal A) (hI : I.FG) (M : ModuleCat.{max u v} A)
    (p : ℤ) (hp : 0 < p) :
    IsIso ((idealLocalCohomology.{u, v} A I hI p).map
      (ModuleCat.ofHom (Ideal.primaryComponent M I).mkQ))

Stacks.Duality.supportLocalCohomology_quotient_map_higher, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionQuotient.lean, line 420. The attribute's comment: “part (2), higher cohomology of the quotient”.

Stacks 0AW0, part (2). The quotient map M ⟶ M/M[I^∞] induces an isomorphism H^p_Z(M) ≅ H^p_Z(M/M[I^∞]) in every positive degree.

theorem supportLocalCohomology_quotient_map_higher
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (M : ModuleCat.{max u v} A) (p : ℤ) (hp : 0 < p) :
    IsIso ((supportLocalCohomology.{u, v} A I hI p).map
      (ModuleCat.ofHom (Ideal.primaryComponent M I).mkQ))

Stacks.Duality.idealLocalCohomology_zero_iso_supportLocalCohomology_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionQuotient.lean, line 439. The attribute's comment: “H^0_I = H^0_Z”.

Stacks 0AW0. For a finitely generated ideal I and Z = V(I) the two zeroth local cohomology modules agree, H^0_I(M) = H^0_Z(M), compatibly with their canonical maps down to M; the common value is the I-power-torsion submodule M[I^∞].

theorem idealLocalCohomology_zero_iso_supportLocalCohomology_zero
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (M : ModuleCat.{max u v} A) :
    ∃ e : (idealLocalCohomology.{u, v} A I hI 0).obj M ≅
        (supportLocalCohomology.{u, v} A I hI 0).obj M,
      e.hom ≫ supportLocalCohomologyToModule.{u, v} A I hI M =
        idealLocalCohomologyToModule.{u, v} A I hI M

Stacks.Duality.localCohomology_divide_by_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionQuotient.lean, line 472. The attribute's comment: “the preamble and both parts conjoined, with the Noetherian hypothesis that the two higher-degree clauses of part (1) require and the source lacks”.

Stacks 0AW0, the preamble and both parts. Let A be a ring, let I ⊆ A be a finitely generated ideal, let M be an A-module and let Z = V(I). Then H^0_I(M) = H^0_Z(M); the common value N is the I-power-torsion submodule M[I^∞], both identifications being compatible with the canonical maps down to M; and, writing M' = M/N,

H^0_I(M') = 0, H^p_I(M) = H^p_I(M') and H^p_I(N) = 0 for all p > 0;

H^0_Z(M') = 0, H^p_Z(M) = H^p_Z(M') and H^p_Z(N) = 0 for all p > 0.

The two higher-degree clauses of part (1) carry the hypothesis that A is Noetherian, which the source does not have, so this conjunction carries it too. That hypothesis cannot be dropped: part (3) of [Stacks, Tag 0A6P] refutes those two clauses for a finitely generated ideal of a non-Noetherian ring, by the argument in the module docstring. Everything else here — the preamble and the whole of part (2) — holds over an arbitrary ring, and is stated that way by the eight declarations this conjoins, each of which carries the tag for its own clause; they are listed in the module docstring and in that of StacksFrontier.AlgebraicGeometry.Duality.DivideByTorsion.

theorem localCohomology_divide_by_torsion
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) (hI : I.FG)
    (M : ModuleCat.{max u v} A) :
    (∃ e : (idealLocalCohomology.{u, v} A I hI 0).obj M ≅
        (supportLocalCohomology.{u, v} A I hI 0).obj M,
      e.hom ≫ supportLocalCohomologyToModule.{u, v} A I hI M =
        idealLocalCohomologyToModule.{u, v} A I hI M) ∧
    (∃ e : (idealLocalCohomology.{u, v} A I hI 0).obj M ≅
        ModuleCat.of A (Ideal.primaryComponent M I),
      e.hom ≫ ModuleCat.ofHom (Submodule.subtype (Ideal.primaryComponent M I)) =
        idealLocalCohomologyToModule.{u, v} A I hI M) ∧
    (IsZero ((idealLocalCohomology.{u, v} A I hI 0).obj
          (ModuleCat.of A (M ⧸ Ideal.primaryComponent M I))) ∧
        (∀ p : ℤ, 0 < p → IsIso ((idealLocalCohomology.{u, v} A I hI p).map
          (ModuleCat.ofHom (Ideal.primaryComponent M I).mkQ))) ∧
        ∀ p : ℤ, 0 < p → IsZero ((idealLocalCohomology.{u, v} A I hI p).obj
          (ModuleCat.of A (Ideal.primaryComponent M I)))) ∧
      (IsZero ((supportLocalCohomology.{u, v} A I hI 0).obj
          (ModuleCat.of A (M ⧸ Ideal.primaryComponent M I))) ∧
        (∀ p : ℤ, 0 < p → IsIso ((supportLocalCohomology.{u, v} A I hI p).map
          (ModuleCat.ofHom (Ideal.primaryComponent M I).mkQ))) ∧
        ∀ p : ℤ, 0 < p → IsZero ((supportLocalCohomology.{u, v} A I hI p).obj
          (ModuleCat.of A (Ideal.primaryComponent M I))))

Sources

LeanModuleCat.subsingleton_ext_of_lt_ideal_depth · Module.subsingleton_ext_of_lt_depth · Stacks.LocalCohomology.depth_eq_sInf_nontrivial_localCohomologyWithSupportIn · Stacks.LocalCohomology.depth_eq_sInf_nontrivial_ext_and_localCohomology_and_subsingleton_ext · Module.depth_eq_sInf_nontrivial_ext · Module.min_depth_le_depth_of_exact · Module.depth_quotSMulTop_succ_eq_depth_and_exists_isRegular_append · Dualizing.supportDim_quotient_add_depth_eq_supportDim

Section47.12 Torsion versus complete modules #

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

Tag 0A6W, a lemma

Tag 0A6W in the Stacks Project.

Dualizing.isIso_derivedCompletion_map_localCohomologyCounit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionComplete/CompletionAfterLocalCohomology.lean, line 184. The attribute's comment: “completion_after_local”.

Stacks 0A6W, completion after local cohomology. For a finitely generated ideal I of a commutative ring A and Z = V(I), the counit RΓ_Z(K) ⟶ K of the adjunction defining local cohomology becomes an isomorphism after derived I-completion; equivalently RΓ_Z(K)^∧ = K^∧ in D(A), naturally in K.

The statement holds for every reflection C of D(A) onto the derived I-complete objects, so it is independent of the chosen model of derived completion.

theorem isIso_derivedCompletion_map_localCohomologyCounit
    (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (C : DerivedCategory (ModuleCat.{v} A) ⥤ DerivedCompleteDerivedCategory A I)
    (hC : C ⊣ (derivedCompleteProperty A I).ι) (K : DerivedCategory (ModuleCat.{v} A)) :
    IsIso ((C ⋙ (derivedCompleteProperty A I).ι).map
      ((localCohomologyAdjunction A I hI).counit.app K))

Dualizing.isIso_localCohomology_map_derivedCompletionUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionComplete/LocalCohomologyAfterCompletion.lean, line 330. The attribute's comment: “local_after_completion”.

Stacks 0A6W, local cohomology after completion. For a finitely generated ideal I = (f₁, …, f_r) of a commutative ring A and Z = V(I), the derived-completion unit K ⟶ K^∧ induces an isomorphism RΓ_Z(K) ⟶ RΓ_Z(K^∧) in D(A), naturally in K.

theorem isIso_localCohomology_map_derivedCompletionUnit (I : Ideal A) (hI : I.FG)
    (f : Fin r → A) (hf : Ideal.span (Set.range f) = I)
    (K : DerivedCategory (ModuleCat.{u} A)) :
    IsIso (((localCohomologyRightAdjoint A I hI).1 ⋙
      (derivedPowerTorsionProperty A I hI).ι).map
        ((DerivedCompletion.derivedCompletionUnit A f).app K))

Tag 0A6X, a proposition

Tag 0A6X in the Stacks Project.

Dualizing.torsionCompleteEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionComplete/Equivalence.lean, line 291.

Stacks 0A6X. For a finitely generated ideal I of a commutative ring A and Z = V(I), derived I-completion and local cohomology with support in Z are quasi-inverse equivalences between the full subcategory of D(A) of complexes with I-power-torsion cohomology and the full subcategory of derived I-complete complexes. The two functors of the equivalence are identified with derived completion and local cohomology by natural isomorphisms, not merely objectwise.

def torsionCompleteEquivalence (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG) :
    Σ E : PowerTorsionDerivedCategory.{u, v} A I hI ≌ DerivedCompleteDerivedCategory A I,
      (E.functor ≅ ((derivedPowerTorsionProperty A I hI).ι ⋙ derivedCompletion A I hI)) ×
      (E.inverse ≅ ((derivedCompleteProperty A I).ι ⋙ localCohomologyFunctor A I hI))

Tag 0A6Y, a lemma

Tag 0A6Y in the Stacks Project.

Dualizing.derivedHomCompletionTorsionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionComplete/DerivedHomCompletionTorsion.lean, line 435.

For A a commutative ring, I a finitely generated ideal, Z = V(I), (-)^∧ derived I-adic completion and RΓ_Z local cohomology, the canonical isomorphism RHom_A(K^∧, L^∧) ≅ RHom_A(RΓ_Z(K), RΓ_Z(L)) in D(A).

def derivedHomCompletionTorsionIso (I : Ideal A) (hI : I.FG) (f : Fin r → A)
    (hf : Ideal.span (Set.range f) = I) (K L : DerivedCategory (ModuleCat.{u} A)) :
    (StacksDraft.DerivedHom.derivedHomAdjunction (R := A)).hom.obj
        (Opposite.op ((DerivedCompletion.derivedCompletionFunctor A f).obj K),
          (DerivedCompletion.derivedCompletionFunctor A f).obj L) ≅
      (StacksDraft.DerivedHom.derivedHomAdjunction (R := A)).hom.obj
        (Opposite.op ((localCohomologyEndofunctor A I hI).obj K),
          (localCohomologyEndofunctor A I hI).obj L)

Dualizing.derivedCompletionDerivedHomTorsionNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionComplete/DerivedHomCompletionTorsion.lean, line 592. The attribute's comment: “natural in the source object”.

For a finite family f generating an ideal I of a commutative ring A, with Z = V(I), there is an isomorphism RHom_A(-, L)^∧ ≅ RHom_A(RΓ_Z(-), RΓ_Z(L)) of contravariant functors on D(A).

def derivedCompletionDerivedHomTorsionNatIso (I : Ideal A) (hI : I.FG) (f : Fin r → A)
    (hf : Ideal.span (Set.range f) = I) (L : DerivedCategory (ModuleCat.{u} A)) :
    derivedHomInto A L ⋙ DerivedCompletion.derivedCompletionFunctor A f ≅
      (localCohomologyEndofunctor A I hI).op ⋙
        derivedHomInto A ((localCohomologyEndofunctor A I hI).obj L)

Tag 0EEW, a lemma

Tag 0EEW in the Stacks Project.

Stacks.Algebraization.isDerivedLimitWithProjections_completedLocalCohomologyNormalizedProjection_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionUnitLocalCohomology/NormalizedProjections.lean, line 241. The attribute's comment: “part (1) for the projections normalized against the completion unit”.

Stacks 0EEW, part (1), for the projections normalized against the completion unit. For a finite module over a Noetherian ring, RΓ_{V(J)}(M)^∧ is a derived limit of the tower n ↦ RΓ_{V(J)}(M/IⁿM) with the normalized projections — the cone whose composites with the completion unit are the maps induced by M ↠ M/IⁿM.

Stacks.Algebraization.isDerivedLimitWithProjections_completedLocalCohomologyNormalizedProjection reduces this to exhibiting one unit-normalized derived-limit cone, and Dualizing.exists_isDerivedLimitWithProjections_of_uliftAdicQuotientIso is one: Stacks 0922 supplies a reflection onto the derived I-complete objects whose unit induces the reduction maps of the tower n ↦ K ⊗ᴸ A/Iⁿ, the comparison with the tower of ordinary quotients is normalized, and two reflections onto the same subcategory agree compatibly with their units, so the cone transports to the reflection adicCompletionFunctor.

theorem isDerivedLimitWithProjections_completedLocalCohomologyNormalizedProjection_of_finite
    [IsNoetherianRing A] (I J : Ideal A) (hI : I.FG) (hJ : J.FG) (M : ModuleCat.{u} A)
    [Module.Finite A M] :
    NoetherianAdicCompletion.IsDerivedLimitWithProjections
      (Dualizing.adicQuotientLocalCohomologySystem A I J hJ M)
      ((adicCompletionFunctor A I hI).obj
        ((Dualizing.localCohomologyFunctor A J hJ).obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj M)).obj)
      (completedLocalCohomologyNormalizedProjection I J hI hJ M)

Dualizing.exists_isDerivedLimit_adicQuotientLocalCohomologySystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionComplete/CompletedLocalCohomologyLimit.lean, line 131. The attribute's comment: “the tower of local cohomologies has a derived limit”.

The tower n ↦ RΓ_Z(M/IⁿM) has a derived limit: countable products exist in D(A), so the difference map 1 - shift on the product of the terms sits in a distinguished triangle.

theorem exists_isDerivedLimit_adicQuotientLocalCohomologySystem (I J : Ideal A) (hJ : J.FG)
    (M : ModuleCat.{u} A) :
    ∃ K : DerivedCategory (ModuleCat.{u} A),
      IsDerivedLimit (adicQuotientLocalCohomologySystem A I J hJ M) K

Dualizing.exists_milnor_shortExact_of_isDerivedLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionComplete/CompletedLocalCohomologyLimit.lean, line 174. The attribute's comment: “the Milnor short exact sequence for the tower”.

Stacks 0EEW, part (2), for an arbitrary derived limit of the tower. The cohomology of a derived limit of n ↦ RΓ_Z(M/IⁿM) sits in a short exact sequence between the first derived limit R¹lim H^{r-1}_Z(M/IⁿM), presented as the cokernel of one minus shift, and the inverse limit lim Hʳ_Z(M/IⁿM). The inclusion is the connecting morphism of the presenting triangle and the projection is characterized by its composites with the limit projections.

theorem exists_milnor_shortExact_of_isDerivedLimit (I J : Ideal A) (hJ : J.FG)
    (M : ModuleCat.{u} A) (K : DerivedCategory (ModuleCat.{u} A))
    (hK : IsDerivedLimit (adicQuotientLocalCohomologySystem A I J hJ M) K) :
    let F := adicQuotientLocalCohomologySystem A I J hJ M
    let X : ℕ → DerivedCategory (ModuleCat.{u} A) := fun n ↦ F.obj (Opposite.op n)
    let d : (∏ᶜ X) ⟶ ∏ᶜ X := Pi.lift fun n : ℕ ↦
      Pi.π X n - Pi.π X (n + 1) ≫ F.map (homOfLE (Nat.le_succ n)).op
    ∃ (a : K ⟶ ∏ᶜ X) (b : (∏ᶜ X) ⟶ K⟦(1 : ℤ)⟧),
      let T := Pretriangulated.Triangle.mk a d b
      T ∈ distTriang (DerivedCategory (ModuleCat.{u} A)) ∧
        ∀ r : ℤ,
          let H := DerivedCategory.homologyFunctor (ModuleCat.{u} A) r
          let H₁ := DerivedCategory.homologyFunctor (ModuleCat.{u} A) (r - 1)
          let homologySystem : ℕᵒᵖ ⥤ ModuleCat.{u} A := F ⋙ H
          let shiftedHomologySystem : ℕᵒᵖ ⥤ ModuleCat.{u} A := F ⋙ H₁
          let P : ModuleCat.{u} A :=
            ∏ᶜ fun n : ℕ ↦ shiftedHomologySystem.obj (Opposite.op n)
          let δ : P ⟶ P := Pi.lift fun n : ℕ ↦
            Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (Opposite.op n)) n -
              Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (Opposite.op n)) (n + 1) ≫
                shiftedHomologySystem.map (homOfLE (Nat.le_succ n)).op
          ∃ (e : H₁.obj (∏ᶜ X) ≅ P)
            (i : cokernel δ ⟶ H.obj K) (q : H.obj K ⟶ limit homologySystem)
            (w : i ≫ q = 0),
            e.hom = piComparison H₁ X ∧
              cokernel.π δ ≫ i = e.inv ≫
                DerivedCategory.HomologySequence.δ T (r - 1) r ∧
              (∀ n : ℕ, q ≫ limit.π homologySystem (Opposite.op n) =
                H.map a ≫ H.map (Pi.π X n)) ∧
              (ShortComplex.mk i q w).ShortExact

Dualizing.isZero_homology_of_isDerivedLimit_of_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionComplete/CompletedLocalCohomologyLimit.lean, line 381. The attribute's comment: “vanishing in negative degrees”.

Stacks 0EEW, the negative-degree vanishing, for an arbitrary derived limit of the tower. A derived limit of n ↦ RΓ_Z(M/IⁿM) has no cohomology in negative degrees.

theorem isZero_homology_of_isDerivedLimit_of_neg (I J : Ideal A) (hJ : J.FG)
    (M : ModuleCat.{u} A) (K : DerivedCategory (ModuleCat.{u} A))
    (hK : IsDerivedLimit (adicQuotientLocalCohomologySystem A I J hJ M) K) (i : ℤ) (hi : i < 0) :
    IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj K)

Dualizing.isDerivedLimit_completedLocalCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionComplete/CompletedLocalCohomologyLimit.lean, line 421. The attribute's comment: “part (1): the derived I-adic completion of RΓ_J(M) is R lim RΓ_J(M/IⁿM)”.

Stacks 0EEW, part (1). The derived I-adic completion of RΓ_Z(M) is a derived limit of the tower n ↦ RΓ_Z(M/IⁿM).

The Čech formula for local cohomology replaces RΓ_Z by C(g) ⊗ᴸ -, where C(g) is the extended alternating Čech complex of a finite generating family of J. Derived I-adic completion of C(g) ⊗ᴸ M is the derived limit of the tower n ↦ (C(g) ⊗ᴸ M) ⊗ᴸ A/Iⁿ (Tag 0EET), and associativity of the derived tensor product rewrites that tower as n ↦ C(g) ⊗ᴸ (M ⊗ᴸ A/Iⁿ). The comparison with the tower of ordinary quotients n ↦ C(g) ⊗ᴸ (M/IⁿM) is a pro-isomorphism, because the fibres only carry the Tor modules Torᵢ(M, A/Iⁿ) and those are pro-zero over a Noetherian ring for a finite module (Tag 0911).

theorem isDerivedLimit_completedLocalCohomology [IsNoetherianRing A]
    (I J : Ideal A) (hI : I.FG) (hJ : J.FG) (M : ModuleCat.{u} A) [Module.Finite A M] :
    IsDerivedLimit (adicQuotientLocalCohomologySystem A I J hJ M)
      (completedLocalCohomology A I J hI hJ M)

Tag 0EEX, a lemma

Tag 0EEX in the Stacks Project.

Dualizing.exists_iso_homology_zero_completedLocalCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TorsionComplete/CompletedLocalCohomologyDegreeZero.lean, line 643.

Stacks 0EEX. Let I and J be ideals of a Noetherian ring A which is I-adically complete, let M be a finite A-module and Z = V(J). The degree-zero cohomology of the derived I-adic completion RΓ_Z(M)^∧ of local cohomology is the filtered colimit of H⁰_{V(J')}(M) over the ideals J' ⊆ J with V(J') ∩ V(I) = V(J) ∩ V(I).

The colimit is realized as the supremum P of the J'-power-torsion submodules Γ_{J'}(M) of M (each H⁰_{V(J')}(M) is Γ_{J'}(M) by Stacks.Duality.supportLocalCohomology_zero_iso_torsion; the index set is directed and the supremum is the union of its terms by Dualizing.iSup_primaryComponent_eq_supportTraceSubmodule). The isomorphism is the one induced by the comparison of Tag 0EEW with lim H⁰_Z(M/IⁿM): composing it with the inclusion into M and the projection to M/IⁿM gives the n-th limit projection followed by the canonical map H⁰_Z(M/IⁿM) ⟶ M/IⁿM. Tag 0EEW part (1), Dualizing.isDerivedLimit_completedLocalCohomology, identifies RΓ_Z(M)^∧ with the derived limit of the tower n ↦ RΓ_Z(M/IⁿM).

theorem exists_iso_homology_zero_completedLocalCohomology [IsNoetherianRing A]
    (I J : Ideal A) [IsAdicComplete I A] (M : ModuleCat.{u} A) [Module.Finite A M]
    (P : Submodule A M)
    (hP : P = ⨆ (J' : Ideal A) (_ : J' ≤ J)
      (_ : PrimeSpectrum.zeroLocus (J' : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A) =
        PrimeSpectrum.zeroLocus (J : Set A) ∩ PrimeSpectrum.zeroLocus (I : Set A)),
      Ideal.primaryComponent M J') :
    ∃ e : (DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).obj
        (completedLocalCohomology A I J I.fg_of_isNoetherianRing J.fg_of_isNoetherianRing M) ≅
          ModuleCat.of A P,
      ∀ n : ℕ, e.hom ≫ ModuleCat.ofHom P.subtype ≫
          ModuleCat.ofHom (I ^ n • (⊤ : Submodule A M)).mkQ =
        completedLocalCohomologyToLimit A I J J.fg_of_isNoetherianRing M _
            (isDerivedLimit_completedLocalCohomology A I J I.fg_of_isNoetherianRing
              J.fg_of_isNoetherianRing M) 0 ≫
          limit.π (adicQuotientLocalCohomologySystem A I J J.fg_of_isNoetherianRing M ⋙
            DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0) (Opposite.op n) ≫
          Stacks.Duality.supportLocalCohomologyToModule.{u, u} A J J.fg_of_isNoetherianRing
            ((adicQuotientModuleSystem A I M).obj
              (Opposite.op n))

Sources

LeanDualizing.isIso_derivedCompletion_map_localCohomologyCounit · Dualizing.isIso_localCohomology_map_derivedCompletionUnit · Dualizing.torsionCompleteEquivalence · Dualizing.derivedHomCompletionTorsionIso · Dualizing.derivedCompletionDerivedHomTorsionNatIso · Stacks.Algebraization.isDerivedLimitWithProjections_completedLocalCohomologyNormalizedProjection_of_finite · Dualizing.exists_isDerivedLimit_adicQuotientLocalCohomologySystem · Dualizing.exists_milnor_shortExact_of_isDerivedLimit

Section47.13 Trivial duality for a ring map #

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

Tag 0A70, a lemma

Tag 0A70 in the Stacks Project.

Dualizing.AnyModel.restrictScalarsDerived_adj_derivedHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomAnyModel.lean, line 141.

Stacks 0A70. Derived coextension of scalars RHom_A(B, -) is right adjoint to restriction of scalars from D(B) to D(A), for arbitrary chosen models of the two derived categories.

This is the model-generic form of Dualizing.restrictScalarsDerived_adj_derivedHom, which is silently specialised to HasDerivedCategory.standard; it is recovered from this by supplying that instance.

theorem restrictScalarsDerived_adj_derivedHom (f : A →+* B) :
    Nonempty ((ModuleCat.restrictScalars.{max v u u'} f).mapDerivedCategory ⊣
      derivedHom.{u, v, u', w, w'} f)

Tag 0C0F, a lemma

Tag 0C0F in the Stacks Project.

Dualizing.derivedHomCompIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDuality.lean, line 356.

For ring maps A → B → C, the composite RHom_B(C, -) ∘ RHom_A(B, -) is naturally isomorphic to RHom_A(C, -).

theorem derivedHomCompIso (f : A →+* B) (g : B →+* C) :
    Nonempty
      (derivedHom.{u, v} f ⋙ derivedHom.{u, v} g ≅
        derivedHom.{u, v} (g.comp f))

Tag 0A71, a lemma

Tag 0A71 in the Stacks Project.

Dualizing.restrictDerivedHomIsoDerivedHomAlong, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CoextendRestrictComparison/Constructed.lean, line 107. The attribute's comment: “derived Hom after restriction, with both derived functors constructed: RHom(B, -) is AnyModel.derivedHom, the total right derived functor of coextension of scalars, and RHom_A(B, -) is derivedHomAlong, that of Hom_A(B, -). Both rings in one universe, modules in max v u, arbitrary models of the two derived categories”.

Stacks 0A71, the displayed formula, with both derived functors constructed: φ_* RHom(B, K) = RHom_A(B, K), where φ_* : D(B) ⥤ D(A) is restriction of scalars.

Restricting the constructed derived coextension functor Dualizing.AnyModel.derivedHom f to D(A) is the constructed A-valued derived Hom functor Dualizing.derivedHomAlong f, by the unique isomorphism compatible with the two derived units. This is Dualizing.derivedCoextendScalarsCompDerivedRestrictScalarsIso with all four of its parameters discharged: RH, β by Dualizing.derivedHomAlong, Dualizing.derivedHomAlongUnit, and RF, α by Dualizing.AnyModel.derivedHom, Dualizing.AnyModel.derivedHomUnit.

def restrictDerivedHomIsoDerivedHomAlong (f : A →+* B) :
    { e : AnyModel.derivedHom.{u, v, u, wA, wB} f ⋙
          (ModuleCat.restrictScalars.{max v u} f).mapDerivedCategory ≅
        derivedHomAlong.{u, v, wA} f //
      restrictedDerivedUnit f (AnyModel.derivedHom.{u, v, u, wA, wB} f)
            (AnyModel.derivedHomUnit.{u, v, wA, wB} f) ≫
          Functor.whiskerLeft DerivedCategory.Qh e.hom =
        derivedHomAlongUnit.{u, v, wA} f }

Dualizing.derivedHomHomologyLinearEquivExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CoextendRestrictComparison/Constructed.lean, line 129. The attribute's comment: “cohomology as Ext, with the derived functor constructed: RHom(B, -) is AnyModel.derivedHom, the total right derived functor of coextension of scalars. Both rings in one universe, modules in max v u, arbitrary models of the two derived categories”.

Stacks 0A71, the "in particular" clause, with the derived functor constructed: R^q Hom(B, K) = Ext^q_A(B, K).

The cohomology of the constructed derived coextension functor Dualizing.AnyModel.derivedHom f, restricted to A-modules, is Ext^q_A(B, K), A-linearly, naturally in K and normalized by the derived unit. This is Dualizing.derivedCoextendScalarsHomologyLinearEquivExt with its parameters RF, α discharged by Dualizing.AnyModel.derivedHom and Dualizing.AnyModel.derivedHomUnit.

def derivedHomHomologyLinearEquivExt (f : A →+* B) :
    HomologyExtComparison f (AnyModel.derivedHom.{u, v, u, wA, wB} f)
      (AnyModel.derivedHomUnit.{u, v, wA, wB} f)

Dualizing.derivedCoextendScalarsCompDerivedRestrictScalarsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDualityRing/Basic.lean, line 247. The attribute's comment: “derived Hom after restriction, for arbitrary right derived functors RF of coextension of scalars and RH of Hom_A(B, -); the data RF, alpha, RH, beta is discharged by AnyModel.derivedHom with AnyModel.derivedHomUnit and derivedHomAlong with derivedHomAlongUnit, giving the unconditional restrictDerivedHomIsoDerivedHomAlong”.

Restricting derived coextension gives RHom_A(B, -), with the comparison uniquely specified by its compatibility with the derived units.

Both derived functors enter as arbitrary right derived functors presented by their universal properties, so the statement is independent of the models chosen for them. That data is discharged by Dualizing.AnyModel.derivedHom with Dualizing.AnyModel.derivedHomUnit on the left and by Dualizing.derivedHomAlong with Dualizing.derivedHomAlongUnit on the right, giving the unconditional Dualizing.restrictDerivedHomIsoDerivedHomAlong.

def derivedCoextendScalarsCompDerivedRestrictScalarsIso
    [RF.IsRightDerivedFunctor α (HomotopyCategory.quasiIso (ModuleCat.{max v u} A) (.up ℤ))]
    (RH : DerivedCategory (ModuleCat.{max v u} A) ⥤
      DerivedCategory (ModuleCat.{max v u} A))
    (β : homAlongToDerivedCategory f ⟶ DerivedCategory.Qh ⋙ RH)
    [RH.IsRightDerivedFunctor β (HomotopyCategory.quasiIso (ModuleCat.{max v u} A) (.up ℤ))] :
    { e : RF ⋙ (ModuleCat.restrictScalars.{max v u} f).mapDerivedCategory ≅ RH //
      restrictedDerivedUnit f RF α ≫ Functor.whiskerLeft DerivedCategory.Qh e.hom = β }

Dualizing.derivedCoextendScalarsHomologyLinearEquivExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDualityRing/Ext.lean, line 1024. The attribute's comment: “cohomology as Ext, for an arbitrary right derived functor RF of coextension of scalars; the data RF, alpha is discharged by AnyModel.derivedHom with AnyModel.derivedHomUnit, giving the unconditional derivedHomHomologyLinearEquivExt”.

The cohomology of derived coextension is Ext, naturally and compatibly with the derived unit (and hence with the restriction comparison).

Derived coextension enters as an arbitrary right derived functor presented by its universal property, so the statement is independent of the model chosen for it. That data is discharged by Dualizing.AnyModel.derivedHom with Dualizing.AnyModel.derivedHomUnit, giving the unconditional Dualizing.derivedHomHomologyLinearEquivExt.

def derivedCoextendScalarsHomologyLinearEquivExt
    [RF.IsRightDerivedFunctor α
      (HomotopyCategory.quasiIso (ModuleCat.{max v u} A) (.up ℤ))] :
    HomologyExtComparison f RF α

Tag 0A72, a lemma

Tag 0A72 in the Stacks Project.

Dualizing.isBoundedBelowCoherent_obj_rightDerivedCoextendScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CoextendRestrictComparison/A72.lean, line 61.

Derived coextension of scalars along a finite homomorphism of Noetherian rings sends bounded-below complexes with coherent cohomology to bounded-below complexes with coherent cohomology.

theorem isBoundedBelowCoherent_obj_rightDerivedCoextendScalars
    {A B : Type u} [CommRing A] [CommRing B] [IsNoetherianRing A] [IsNoetherianRing B]
    [HasDerivedCategory (ModuleCat.{max v u} A)] [HasDerivedCategory (ModuleCat.{max v u} B)]
    (f : A →+* B) (hf : f.Finite)
    (RF : DerivedCategory (ModuleCat.{max v u} A) ⥤ DerivedCategory (ModuleCat.{max v u} B))
    (alpha : (ModuleCat.coextendScalars f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RF)
    [RF.IsRightDerivedFunctor alpha
      (HomotopyCategory.quasiIso (ModuleCat.{max v u} A) (ComplexShape.up ℤ))]
    {K : DerivedCategory (ModuleCat.{max v u} A)}
    (hK : DerivedCategoryB.derivedCategoryBPlus
      (fun M : ModuleCat.{max v u} A ↦ Module.Finite A M) K) :
    DerivedCategoryB.derivedCategoryBPlus
      (fun M : ModuleCat.{max v u} B ↦ Module.Finite B M) (RF.obj K)

Tag 0BZB, a situation

Tag 0BZB in the Stacks Project.

Dualizing.DGAResolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolution.lean, line 109. The attribute's comment: “resolution data”.

Situation 0BZB. A differential graded resolution of a commutative R-algebra A: a differential graded R-algebra E together with a homomorphism to A, viewed as a differential graded algebra with zero differential in degree zero, which is a quasi-isomorphism, that is, an isomorphism on cohomology.

structure DGAResolution (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]

Dualizing.DGAResolution.derivedEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolution.lean, line 125. The attribute's comment: “ordinary derived equivalence”.

The horizontal equivalence of Situation 0BZB. Extension of scalars along the resolution, followed by the identification of differential graded modules over A in degree zero with complexes of A-modules, is an equivalence D(E, d) ≌ D(A).

noncomputable def derivedEquivalence :
    derivedCategory' S.E ≌ DerivedCategory (ModuleCat.{u} A)

Dualizing.DGAResolution.restrictionTriangle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolution.lean, line 133. The attribute's comment: “restriction triangle”.

The first diagram of Situation 0BZB commutes. Passing from D(A) to D(E, d) through the equivalence and then forgetting the E-action is restriction of scalars along R → A.

noncomputable def restrictionTriangle :
    S.derivedEquivalence.inverse ⋙ derivedForget S.E ≅
      (ModuleCat.restrictScalars.{u} (algebraMap R A)).mapDerivedCategory

Dualizing.DGAResolution.derivedExtension_comp_iso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolution.lean, line 269. The attribute's comment: “extension triangle, for an arbitrary left adjoint F of the forgetful functor; its data F, adjF is discharged by derivedExtensionToDGA and derivedExtensionToDGA_adj, giving the unconditional DGAResolution.derivedExtensionToDGA_comp_iso”.

The second diagram of Situation 0BZB commutes. Derived extension of scalars from D(R) to D(E, d) followed by the equivalence - ⊗_E^𝐋 A is derived extension of scalars - ⊗_R^𝐋 A : D(R) ⥤ D(A).

Derived extension of scalars to the resolution enters as an arbitrary left adjoint F of the forgetful functor, so the statement is independent of the model chosen for it. That data is discharged by Dualizing.derivedExtensionToDGA together with Dualizing.derivedExtensionToDGA_adj, giving the unconditional Dualizing.DGAResolution.derivedExtensionToDGA_comp_iso.

noncomputable def derivedExtension_comp_iso
    (F : DerivedCategory (ModuleCat.{u} R) ⥤ derivedCategory' S.E)
    (adjF : F ⊣ derivedForget S.E) :
    F ⋙ S.derivedEquivalence.functor ≅ ordinaryExtension (R := R) (A := A)

Dualizing.DGAResolution.derivedExtensionToDGA_comp_iso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolutionExtension.lean, line 105. The attribute's comment: “extension triangle, with the functor constructed”.

The second diagram of Situation 0BZB commutes, with no assumed functor. Derived extension of scalars - ⊗_R^𝐋 E : D(R) ⥤ D(E, d) followed by the horizontal equivalence - ⊗_E^𝐋 A : D(E, d) ⥤ D(A) is derived extension of scalars - ⊗_R^𝐋 A : D(R) ⥤ D(A).

This is Dualizing.DGAResolution.derivedExtension_comp_iso with its parameters F and adjF discharged by Dualizing.derivedExtensionToDGA and Dualizing.derivedExtensionToDGA_adj.

def derivedExtensionToDGA_comp_iso (S : Dualizing.DGAResolution R A) :
    derivedExtensionToDGA S.E ⋙ S.derivedEquivalence.functor ≅
      Dualizing.DGAResolution.ordinaryExtension (R := R) (A := A)

Declarations registered for the tag:

DifferentialGraded.Bimodule.derivedExtensionEquivalence, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolution.lean, line 99 (StacksFrontier): “horizontal equivalence”.

Tag 0BZC, a lemma

Tag 0BZC in the Stacks Project.

Dualizing.DGAResolution.derivedHom_comp_derivedEquivalence_iso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolution.lean, line 210.

Stacks 0BZC. In Situation 0BZB the functor R Hom(A, -) : D(R) ⥤ D(A) is the composition of R Hom(E, -) : D(R) ⥤ D(E, d) with the equivalence - ⊗_E^𝐋 A : D(E, d) ⥤ D(A).

The functor R Hom(E, -) enters as an arbitrary right adjoint G of the forgetful functor D(E, d) ⥤ D(R), which is what Tag 09LT says derived Hom out of E is; so the statement is independent of the model chosen for it.

noncomputable def derivedHom_comp_derivedEquivalence_iso
    (G : DerivedCategory (ModuleCat.{u} R) ⥤ derivedCategory' S.E)
    (adjG : derivedForget S.E ⊣ G) :
    Dualizing.derivedHom.{u, u, u} (algebraMap R A) ≅ G ⋙ S.derivedEquivalence.functor

Tag 0BZD, a lemma

Tag 0BZD in the Stacks Project.

Dualizing.derivedHomIsoGradedDualTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolution.lean, line 366.

Stacks 0BZD. Let (E, d) be a differential graded algebra over a commutative ring R — in Situation 0BZB, the algebra resolving the R-algebra A — and let N = Hom^•_R(E^•, R) be the graded dual of E^• over R, a differential graded (R, E)-bimodule. Assume that E^• is a compact object of D(R) and that N computes R Hom(E, R). Then R Hom(E, -) : D(R) ⥤ D(E, d) is isomorphic to K ↦ K ⊗_R^𝐋 N.

Here D(R) is the derived category of R viewed as a differential graded algebra concentrated in degree zero, which is the derived category of R-modules by DifferentialGradedModule.degreeZeroDerivedEquivalence; R Hom(E, -) is the right derived functor of Tag 09LI for the bimodule E, and - ⊗_R^𝐋 N the left derived functor of Tag 09LS.

The source deduces this as the case T = E of the second assertion of Tag 0BZ0, which is DifferentialGraded.Bimodule.derivedTensorHomDualFunctorIso; the two hypotheses above are exactly its two hypotheses for T = E.

noncomputable def derivedHomIsoGradedDualTensor
    (hcompact : IsCompactBimodule (resolvingBimodule E))
    (hdual : ComputesDerivedHom (resolvingBimodule E)) :
    (derivedHomData E (baseAlgebra R) (resolvingBimodule E).rightModule
        (resolvingBimodule E).leftAction).functor ≅
      Bimodule.derivedTensorFunctor (gradedDualBimodule E)

Tag 0BZE, a lemma

Tag 0BZE in the Stacks Project.

Dualizing.exists_derivedHom_iso_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomPerfectTensor.lean, line 216. The attribute's comment: “the functor R Hom(A, -) is derived tensoring over R with a differential graded (R, A)-bimodule whose class in D(A) is R Hom(A, R), read through the degree-zero equivalences”.

Stacks 0BZE. Let R → A be a map of commutative rings making A a perfect R-module. Then R Hom(A, -) : D(R) ⥤ D(A) is a derived tensor product: there is a differential graded (R, A)-bimodule M with R Hom(A, -) ≅ - ⊗_R^𝐋 M, whose class in D(A) is the value R Hom(A, R) of that functor at R. The two derived categories of the degree-zero world are the derived categories of R-modules and of A-modules through DifferentialGradedModule.degreeZeroDerivedEquivalence.

A Tate resolution of A over R exists for every R-algebra, along the tautological polynomial presentation; it puts us in Situation 0BZB. Perfectness of A makes the resolving bimodule compact in D(R), and the homogeneous pieces of a Tate resolution are free over R, which makes its graded dual compute R Hom(E^•, R). Both hypotheses of Stacks 0BZD hold, so Dualizing.DGAResolution.derivedHomIsoDerivedTensor applies.

theorem exists_derivedHom_iso_derivedTensor
    (hperf : StacksDraft.Perfect.IsPerfectModule.{u, u, u + 1} (R := R) A) :
    ∃ M : Bimodule (baseAlgebra R) (DifferentialGradedAlgebra.degreeZero R A),
      Nonempty (Dualizing.derivedHom.{u, u, u} (algebraMap R A) ≅
        derivedTensorBimoduleFunctor M) ∧
      Nonempty ((Dualizing.derivedHom.{u, u, u} (algebraMap R A)).obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R)) ≅
        (degreeZeroDerivedEquivalence (R := R) (A := A)).functor.obj
          ((toHomotopyCategory (DifferentialGradedAlgebra.degreeZero R A) ⋙
            (quasiIsomorphisms' (DifferentialGradedAlgebra.degreeZero R A)).Q).obj
              M.rightModule))

Dualizing.nonempty_derivedHom_iso_canonicalDerivedTensor_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDualityBundlePerfect.lean, line 76. The attribute's comment: “in the derived change-of-rings shape of Tag 06Y6, at module universe equal to the ring universe, with no carried hypothesis”.

Stacks 0BZE in the derived change-of-rings shape of Tag 06Y6. Let f : R → A make A a perfect R-module and let L be a complex of A-modules whose class in D(A) is the value RHom_R(A, R) of derived coextension of scalars at the free module of rank one. Then RHom_R(A, -) : D(R) ⥤ D(A) is the canonical derived change-of-rings tensor product of Stacks 06Y6 with L.

This is Dualizing.exists_derivedHom_iso_derivedTensor — Stacks 0BZE through a Tate resolution — carried across Dualizing.nonempty_derivedTensorBimoduleFunctor_iso_canonical and then across Stacks 0BYK to the chosen representative L. No hypothesis beyond the perfectness that Stacks 0BZE itself assumes.

theorem nonempty_derivedHom_iso_canonicalDerivedTensor_of_perfect (f : R →+* A)
    (hperf : letI := f.toAlgebra
      StacksDraft.Perfect.IsPerfectModule.{u, u, u + 1} (R := R) A)
    (L : CochainComplex (ModuleCat.{u} A) ℤ)
    (hL : Nonempty (DerivedCategory.Q.obj L ≅
      (Dualizing.derivedHom.{u, u} f).obj
        ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R)))) :
    letI := f.toAlgebra
    Nonempty (Dualizing.derivedHom.{u, u} f ≅
      (canonicalDerivedTensorChangeOfRings.{u, u, u} f L).F)

Dualizing.derivedHomIsoCanonicalDerivedTensorOfPerfect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDualityBundlePerfect.lean, line 137. The attribute's comment: “in the derived change-of-rings shape of Tag 06Y6, at module universe equal to the ring universe, with no carried hypothesis; the isomorphism is built, at the canonical tensor factor, rather than shown to exist at an arbitrary representative”.

Stacks 0BZE in the derived change-of-rings shape of Tag 06Y6, as data. For f : R → A making A a perfect R-module, RHom_R(A, -) : D(R) ⥤ D(A) is the canonical derived change-of-rings tensor product of Stacks 06Y6 with the canonical tensor factor Dualizing.canonicalDerivedHomTensorComplex f. No existential witness is chosen along the way: the Tate resolution is the named one, Dualizing.DGAResolution.derivedHomIsoDerivedTensor is a construction, and so is Dualizing.derivedTensorBimoduleFunctorIsoCanonical, so the isomorphism is a function of f and hperf.

Dualizing.nonempty_derivedHom_iso_canonicalDerivedTensor_of_perfect is the form stated at an arbitrary complex representing RHom_R(A, R); that form is a proposition because passing from this factor to another representative of the same object of D(A) goes through a fraction, in Dualizing.InvertibleKernel.derivedTensorIsoOfDerivedIso.

def derivedHomIsoCanonicalDerivedTensorOfPerfect (f : R →+* A)
    (hperf : letI := f.toAlgebra
      StacksDraft.Perfect.IsPerfectModule.{u, u, u + 1} (R := R) A) :
    letI := f.toAlgebra
    Dualizing.derivedHom.{u, u} f ≅
      (canonicalDerivedTensorChangeOfRings.{u, u, u} f
        (canonicalDerivedHomTensorComplex f)).F

Dualizing.nonempty_derivedHom_iso_canonicalDerivedTensor_of_perfect_anyModuleUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDualityBundlePerfectAnyModuleUniverse.lean, line 324. The attribute's comment: “in the derived change-of-rings shape of Tag 06Y6, at an arbitrary module universe above the ring universe, with no carried hypothesis”.

Stacks 0BZE in the derived change-of-rings shape of Tag 06Y6, at an arbitrary module universe. Let f : R → A make A a perfect R-module and let L be a complex of A-modules, in a universe max v u above the ring universe u, whose class in D(A) is the value RHom_R(A, R) of derived coextension of scalars at the free module of rank one on the lifted carrier. Then RHom_R(A, -) : D(R) ⥤ D(A) is the canonical derived change-of-rings tensor product of Stacks 06Y6 with L.

This is Dualizing.nonempty_derivedHom_iso_canonicalDerivedTensor_of_perfect — which holds at module universe equal to the ring universe, the generality of the differential graded chapter — renamed along ULift.ringEquiv, where the module universe max v u is the ring universe. All three functors involved are carried across that renaming: derived coextension of scalars by StacksDraft.DerivedRingEquivIso.derivedHomRingEquivIso, and derived extension of scalars together with the derived change-of-rings tensor product by StacksDraft.DerivedRingEquivIso.derivedTensorBundleRingEquivIsoOfFactorIso. The perfectness hypothesis is the one Stacks 0BZE itself assumes, read for the lifted rings by Dualizing.isPerfectModule_ulift_ringEquiv.

theorem nonempty_derivedHom_iso_canonicalDerivedTensor_of_perfect_anyModuleUniverse (f : R →+* A)
    (hperf : letI := f.toAlgebra
      StacksDraft.Perfect.IsPerfectModule.{u, u, u + 1} (R := R) A)
    (L : CochainComplex (ModuleCat.{max v u} A) ℤ)
    (hL : Nonempty (DerivedCategory.Q.obj L ≅
      (Dualizing.derivedHom.{u, v} f).obj
        ((DerivedCategory.singleFunctor (ModuleCat.{max v u} R) 0).obj
          (ModuleCat.of R (ULift.{max v u} R))))) :
    Nonempty (Dualizing.derivedHom.{u, v} f ≅
      (canonicalDerivedTensorChangeOfRings.{u, u, max v u} f L).F)

Dualizing.nonempty_restrictScalars_derivedHom_iso_derivedTensor_unitDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDualityPerfectObjectwise.lean, line 107. The attribute's comment: “objectwise and after restriction of scalars to the base”.

Stacks 0BZE, objectwise and after restriction of scalars. Let f : R → A be a homomorphism of commutative rings with A perfect as an R-module. For every object K of D(R), derived coextension of scalars R Hom(A, K) of Stacks 0A70, read in D(R) by restriction of scalars along f, is the derived tensor product of K with R Hom(A, R) read in the same way.

Perfectness is consumed, not recorded: it is the first case of the derived tensor--Hom diagonal of Stacks 0ATK, applied with the diagonal's internal-Hom source the module A placed in degree zero and read over R. The two vocabularies are reconciled by Dualizing.nonempty_modelHomIsoRestrictScalarsDerivedHom, which identifies the internal derived Hom of Stacks 0A63 out of that object with restricted derived coextension, and the tensor factor K ⊗ᴸ_R R is cut down by the right unitor of the derived tensor product.

Stacks 0BZE asserts more: an isomorphism of functors D(R) ⥤ D(A). Both of the missing steps — naturality of the comparison in K, and the identification of Stacks0BZE.comparison with the diagonal that would carry an isomorphism in D(R) up to D(A) — are discussed in this module's documentation. For the form of Stacks 0BZE that asserts the isomorphism of functors and carries those steps as hypotheses, see Stacks0BZE.cardIso of StacksFrontier.RingTheory.Dualizing.TrivialDualityKFlat; for the unconditional form, see Dualizing.exists_derivedHom_iso_derivedTensor of StacksFrontier.RingTheory.Dualizing.DerivedHomPerfectTensor.

theorem nonempty_restrictScalars_derivedHom_iso_derivedTensor_unitDual (f : R →+* A)
    (hperfect : letI := f.toAlgebra
      StacksDraft.Perfect.IsPerfectModule (R := R) A)
    (K : DerivedCategory (ModuleCat.{u} R)) :
    Nonempty
      ((ModuleCat.restrictScalars.{u} f).mapDerivedCategory.obj
          ((derivedHom.{u, u, u} f).obj K) ≅
        (Model.tensor R).obj
          (K, (ModuleCat.restrictScalars.{u} f).mapDerivedCategory.obj
            ((derivedHom.{u, u, u} f).obj
              (DerivedCategory.Q.obj
                ((CochainComplex.singleFunctor (ModuleCat.{u} R) 0).obj
                  (ModuleCat.of R R))))))

Tag 0BZH, a lemma

Tag 0BZH in the Stacks Project.

Dualizing.InvertibleKernel.conormal_invertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDualityInvertibleKernel.lean, line 137. The attribute's comment: “the conormal module I ⊗_R A is an invertible A-module”.

The conormal module of a surjection with invertible kernel is invertible. Invertibility is stable under base change, here along R → A itself.

This is the clause of [Stacks, Tag 0BZH] that calls I ⊗_R A an invertible A-module. Unlike the functor identification it needs nothing beyond the two hypotheses of the tag, and it holds at every module universe.

theorem conormal_invertible (hI : Module.Invertible R (RingHom.ker (algebraMap R A))) :
    Module.Invertible A (conormal.{u, v} R A)

Dualizing.InvertibleKernel.conormalInverse_tensor_conormal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDualityInvertibleKernel.lean, line 148. The attribute's comment: “N is the inverse of the invertible A-module I ⊗_R A”.

N is a tensor inverse of the conormal module: N ⊗_A (I ⊗_R A) ≅ A.

This is the clause of [Stacks, Tag 0BZH] that names N as the inverse of the invertible A-module I ⊗_R A; like Dualizing.InvertibleKernel.conormal_invertible it is unconditional and holds at every module universe.

def conormalInverse_tensor_conormal
    (hI : Module.Invertible R (RingHom.ker (algebraMap R A))) :
    conormalInverse.{u, v} R A ⊗[A] conormal.{u, v} R A ≃ₗ[A] A

Dualizing.InvertibleKernel.nonempty_derivedHom_iso_derivedTensor_conormalInverseShift_anyModuleUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDualityInvertibleKernelAnyModuleUniverse.lean, line 52. The attribute's comment: “at an arbitrary module universe above the ring universe, with no carried hypothesis”.

For a surjection f : R → A whose kernel is an invertible R-module, derived coextension of scalars RHom_R(A, -) : D(R) ⥤ D(A) is derived tensoring over R with the conormal inverse shift N[-1], for any model of the derived change-of-rings tensor product with that factor and at any module universe above the ring universe.

theorem nonempty_derivedHom_iso_derivedTensor_conormalInverseShift_anyModuleUniverse
    (f : R →+* A) (hf : Function.Surjective f)
    (hI : Module.Invertible R (RingHom.ker f)) :
    letI := f.toAlgebra
    ∀ T : DerivedTensorChangeOfRings f (conormalInverseShift.{u, v} R A),
      Nonempty (Dualizing.derivedHom.{u, v} f ≅ T.F)

Dualizing.InvertibleKernel.nonempty_derivedHom_iso_derivedTensor_conormalInverseShift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/PolynomialEvalDualityProof.lean, line 103. The attribute's comment: “at module universe equal to the ring universe, with no carried hypothesis”.

Stacks 0BZH. For a surjection f : R → A whose kernel is an invertible R-module, derived coextension of scalars RHom_R(A, -) : D(R) ⥤ D(A) is derived tensoring over R with the conormal inverse shift N[-1], at any model of the derived change-of-rings tensor product with that factor.

This is Dualizing.InvertibleKernel.nonempty_derivedHom_iso_canonicalDerivedTensor_conormalInverseShift transported to an arbitrary model along Dualizing.InvertibleKernel.derivedTensorIsoOfDerivedIso at the identity of the tensor factor.

theorem nonempty_derivedHom_iso_derivedTensor_conormalInverseShift (f : R →+* A)
    (hf : Function.Surjective f) (hI : Module.Invertible R (RingHom.ker f)) :
    letI := f.toAlgebra
    ∀ T : DerivedTensorChangeOfRings f (conormalInverseShift.{u, u} R A),
      Nonempty (Dualizing.derivedHom.{u, u} f ≅ T.F)

Sources

LeanDualizing.AnyModel.restrictScalarsDerived_adj_derivedHom · Dualizing.derivedHomCompIso · Dualizing.restrictDerivedHomIsoDerivedHomAlong · Dualizing.derivedHomHomologyLinearEquivExt · Dualizing.derivedCoextendScalarsCompDerivedRestrictScalarsIso · Dualizing.derivedCoextendScalarsHomologyLinearEquivExt · Dualizing.isBoundedBelowCoherent_obj_rightDerivedCoextendScalars · Dualizing.DGAResolution

Section47.14 Base change for trivial duality #

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

Tag 0E29, an equation

Tag 0E29 in the Stacks Project.

Dualizing.derivedHomBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDuality/BaseChange.lean, line 222.

The canonical base-change map RHom_R(A, -) ⊗ᴸ_A (A ⊗_R R') ⟶ RHom_{R'}(A ⊗_R R', - ⊗ᴸ_R R'), functorial in the object of D(R).

noncomputable def derivedHomBaseChange
    {R : Type uR} {A : Type uA} {R' : Type uRp} [CommRing R] [CommRing A] [CommRing R']
    [Algebra R A] [Algebra R R']
    (hTor : RingTheory.TorIndependence.TorIndependent R A R')
    (baseChangeR :
      DerivedCategory (ModuleCat.{max v uR uA uRp} R) ⥤
        DerivedCategory (ModuleCat.{max v uR uA uRp} R'))
    (comparisonR :
      DerivedCategory.Q ⋙ baseChangeR ⟶
        (ModuleCat.extendScalars.{uR, uRp, max v uR uA uRp}
          (algebraMap R R')).mapHomologicalComplex
          (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerivedR : baseChangeR.IsLeftDerivedFunctor comparisonR
      (HomologicalComplex.quasiIso (ModuleCat.{max v uR uA uRp} R) (ComplexShape.up ℤ)))
    (baseChangeA :
      DerivedCategory (ModuleCat.{max v uR uA uRp} A) ⥤
        DerivedCategory (ModuleCat.{max v uR uA uRp} (TensorProduct R A R')))
    (comparisonA :
      DerivedCategory.Q ⋙ baseChangeA ⟶
        (ModuleCat.extendScalars.{uA, max uA uRp, max v uR uA uRp}
          (algebraMap A (TensorProduct R A R'))).mapHomologicalComplex
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerivedA : baseChangeA.IsLeftDerivedFunctor comparisonA
      (HomologicalComplex.quasiIso (ModuleCat.{max v uR uA uRp} A) (ComplexShape.up ℤ)))
    :
    derivedHom.{uR, max v uRp, uA} (algebraMap R A) ⋙ baseChangeA ⟶
      baseChangeR ⋙ derivedHom.{uRp, max v uR, max uA uRp}
        (Algebra.TensorProduct.includeRight :
          R' →ₐ[R] TensorProduct R A R').toRingHom

Dualizing.derivedHomBaseChangeCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDuality/BaseChangeCanonical.lean, line 86. The attribute's comment: “at the constructed derived extensions of scalars; one universe for all rings”.

The canonical base-change map RHom_R(A, -) ⊗ᴸ_A (A ⊗_R R') ⟶ RHom_{R'}(A ⊗_R R', - ⊗ᴸ_R R') of [Stacks, Equation 47.14.0.1], functorial in the object of D(R), with the two derived extensions of scalars taken to be the constructed functor StacksDraft.PseudoCoherence.extendScalarsDerived rather than certified parameters.

All three rings and the module size live in the single universe u, which is the generality extendScalarsDerived is available in.

noncomputable def derivedHomBaseChangeCanonical
    {R : Type u} {A : Type u} {R' : Type u} [CommRing R] [CommRing A] [CommRing R']
    [Algebra R A] [Algebra R R']
    (hTor : RingTheory.TorIndependence.TorIndependent R A R') :
    derivedHom.{u, u, u} (algebraMap R A) ⋙
        extendScalarsDerived (algebraMap A (TensorProduct R A R')) ⟶
      extendScalarsDerived (algebraMap R R') ⋙ derivedHom.{u, u, u}
        (Algebra.TensorProduct.includeRight :
          R' →ₐ[R] TensorProduct R A R').toRingHom

Tag 0E2A, a lemma

Tag 0E2A in the Stacks Project.

Dualizing.isIso_derivedHomBaseChange_app_iff_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomBaseChange/Criterion.lean, line 220.

For R → A and R → R' with A and R' Tor independent over R, and A' = A ⊗_R R', the base-change morphism RHom_R(A, K) ⊗ᴸ_A A' ⟶ RHom_{R'}(A', K ⊗ᴸ_R R') of Stacks 0E29 is an isomorphism exactly when the morphism RHom_R(A, K) ⊗ᴸ_R R' ⟶ RHom_R(A, K ⊗ᴸ_R R') of Stacks 0BYN is, read over ULift R through the scalar equivalence of Stacks 0E1W.

theorem isIso_derivedHomBaseChange_app_iff_diagonal
    (K : DerivedCategory (ModuleCat.{max v uR uA uRp} R)) :
    IsIso ((derivedHomBaseChange.{uR, uA, uRp, v} hTor baseChangeR comparisonR isLeftDerivedR
        baseChangeA comparisonA isLeftDerivedA).app K) ↔
      (let E := Stacks.DerivedHom.ScalarTransportedInternalHom.scalarEquivalence.{uR, max v uR uA
        uRp} R
       IsIso (StacksDraft.DerivedHom.derivedTensorHomDiagonal
         (E.functor.obj ((DerivedCategory.singleFunctor (ModuleCat.{max v uR uA uRp} R) 0).obj
           ((ModuleCat.restrictScalars (algebraMap R R')).obj
             (ModuleCat.of R' (ULift.{max v uR uA} R')))))
         (E.functor.obj K)
         (E.functor.obj (derivedAlgebraSingle.{uR, uA, max v uRp} (algebraMap R A)))) : Prop)

Tag 0BZM, a lemma

Tag 0BZM in the Stacks Project.

Dualizing.isIso_derivedHomBaseChange_app_of_isModulePseudoCoherent_of_finiteTorDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDuality/BaseChangeIsomorphismFiniteTorDimension.lean, line 126.

Stacks 0BZM. Let R → A and R → R' be homomorphisms of commutative rings and A' = A ⊗_R R'. If A is pseudo-coherent as an R-module, R' has finite Tor dimension as an R-module, and A and R' are Tor independent over R, then the base-change morphism RHom_R(A, K) ⊗ᴸ_A A' ⟶ RHom_{R'}(A', K ⊗ᴸ_R R') of Stacks 0E29 is an isomorphism for every K in D⁺(R).

theorem isIso_derivedHomBaseChange_app_of_isModulePseudoCoherent_of_finiteTorDimension
    (hA : StacksDraft.PseudoCoherence.IsModulePseudoCoherent (R := R) A)
    (D : StacksDraft.TorAmplitude.CertifiedDerivedTensoring.{uR, max v uR uA uRp} R)
    (hFinite : StacksDraft.TorAmplitude.ModuleHasFiniteTorDimension D.tensor D.comparison
      D.isLeftDerived
      ((ModuleCat.restrictScalars (algebraMap R R')).obj
        (ModuleCat.of R' (ULift.{max v uR uA, uRp} R'))))
    (K : DerivedCategory (ModuleCat.{max v uR uA uRp} R))
    (hK : (DerivedCategory.TStructure.t (C := ModuleCat.{max v uR uA uRp} R)).plus K) :
    IsIso ((derivedHomBaseChange.{uR, uA, uRp, v} hTor baseChangeR comparisonR isLeftDerivedR
      baseChangeA comparisonA isLeftDerivedA).app K)

Tag 0BZP, a lemma

Tag 0BZP in the Stacks Project.

Dualizing.isIso_derivedHomBaseChange_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/TrivialDuality/BaseChangeIsomorphism.lean, line 233.

Stacks 0BZP. Let R → A and R → R' be homomorphisms of commutative rings and A' = A ⊗_R R'. If A is perfect as an R-module and A and R' are Tor independent over R, then the base-change morphism of Stacks 0E29 is invertible — as a natural transformation, hence at every object of D(R) and with no boundedness hypothesis.

The proof is that of the source. By Stacks 0E2A the restriction of the morphism along R' → A' is, up to isomorphisms of source and target, the derived-Hom base-change morphism of Stacks 0E1X at the algebra A; this is Dualizing.exists_restrictScalars_map_derivedHomBaseChange_app_eq. That morphism is invertible because A is perfect, by Stacks 0ATK (1), and restriction of scalars reflects isomorphisms.

theorem isIso_derivedHomBaseChange_of_isPerfect
    (hA : StacksDraft.Perfect.IsPerfectModule (R := R) A) :
    IsIso (derivedHomBaseChange.{uR, uA, uRp, v} hTor baseChangeR comparisonR isLeftDerivedR
      baseChangeA comparisonA isLeftDerivedA)

Sources

LeanDualizing.derivedHomBaseChange · Dualizing.derivedHomBaseChangeCanonical · Dualizing.isIso_derivedHomBaseChange_app_iff_diagonal · Dualizing.isIso_derivedHomBaseChange_app_of_isModulePseudoCoherent_of_finiteTorDimension · Dualizing.isIso_derivedHomBaseChange_of_isPerfect

Section47.15 Dualizing complexes #

Section 47.15 of the Stacks Project, Tag 0A7A. 12 tags here are carried by 21 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A7B, a definition

Tag 0A7B in the Stacks Project.

Dualizing.IsDualizingComplex, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Complex.lean, line 176. References: SGA 5 I (1.7), “affine/ring case”.

A dualizing complex over a Noetherian commutative ring is a derived object of finite injective dimension whose cohomology modules are finite and whose homothety map to its derived endomorphism complex is a quasi-isomorphism.

structure IsDualizingComplex {A : Type u} [CommRing A] [IsNoetherianRing A]
    [HasDerivedCategory.{w} (ModuleCat.{v} A)]
    (K : DerivedCategory (ModuleCat.{v} A)) : Prop

Tag 0G4H, a lemma

Tag 0G4H in the Stacks Project.

Dualizing.derivedHom_finiteCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomFiniteCohomology.lean, line 544. References: SGA 5 I (App.7.3), “affine case”.

Stacks 0G4H. Let A be a Noetherian ring and let K and L be objects of the derived category of A-modules whose cohomology modules are all finite. If L has finite injective dimension, then every cohomology module of RHom_A(K, L) is finite as well.

public theorem derivedHom_finiteCohomology
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (K L : DerivedCategory (ModuleCat.{max u v} A))
    (hK : DerivedCategoryB.derivedCategoryB
      (fun M : ModuleCat.{max u v} A => Module.Finite A M) K)
    (hL : DerivedCategoryB.derivedCategoryB
      (fun M : ModuleCat.{max u v} A => Module.Finite A M) L)
    (hLinj : StacksDraft.InjectiveDimension.HasFiniteInjectiveDimension L) :
    DerivedCategoryB.derivedCategoryB
      (fun M : ModuleCat.{max u v} A => Module.Finite A M)
      ((derivedHomAdjunctionOverRing A).hom.obj (.op K, L))

Tag 0A7C, a lemma

Tag 0A7C in the Stacks Project.

Dualizing.derivedBiduality, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomDuality/Duality.lean, line 181. The attribute's comment: “canonical biduality morphism”.

The canonical biduality morphisms, natural in the derived object. Each component is the canonical morphism K ⟶ RHom_A(RHom_A(K, ω), ω) of Dualizing.dualizingBidualityMor; naturality is Dualizing.bidualityMor_naturality at the adjunction of [stacks 0A63].

def derivedBiduality (ω : DerivedCategory (ModuleCat.{max u v} A)) :
    Functor.id (DerivedCategory (ModuleCat.{max u v} A)) ⟶
      opOp (DerivedCategory (ModuleCat.{max u v} A)) ⋙
        (dualizingDerivedHomFunctor.{u, v} A ω).op ⋙
          dualizingDerivedHomFunctor.{u, v} A ω

Dualizing.dualizingDerivedHom_biduality_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomDuality/Duality.lean, line 244. The attribute's comment: “canonical biduality”.

Canonical biduality is a natural isomorphism on objects with finite cohomology. Each component is invertible by Dualizing.isIso_dualizingBidualityMor_of_finiteCohomology, and a morphism of a full subcategory is invertible as soon as the underlying morphism is.

theorem dualizingDerivedHom_biduality_isIso
    (ω : DerivedCategory (ModuleCat.{max u v} A)) (hω : IsDualizingComplex ω) :
    IsIso (coherentDerivedBiduality.{u, v} A ω hω)

Dualizing.coherentDualizingDerivedHom_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomDuality/Duality.lean, line 266. The attribute's comment: “the anti-equivalence on coherent objects”. References: SGA 5 I (App.7.3), “affine case”.

Derived Hom into a dualizing complex is an anti-equivalence on the derived category of objects with finite cohomology, [stacks 0A7C].

theorem coherentDualizingDerivedHom_isEquivalence
    (ω : DerivedCategory (ModuleCat.{max u v} A)) (hω : IsDualizingComplex ω) :
    (coherentDualizingDerivedHomFunctor.{u, v} A ω hω).IsEquivalence

Dualizing.dualizingDerivedHom_plus_iff_minus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomDuality/Duality.lean, line 278. The attribute's comment: “exchange of bounded below and bounded above”.

On objects with finite cohomology, derived Hom into a dualizing complex exchanges bounded below with bounded above. The forward implication is the bound exchange Dualizing.dualizingDerivedHom_isLE_of_isGE; the converse applies the other bound exchange to RHom_A(K, ω) and transports the resulting bound along canonical biduality.

theorem dualizingDerivedHom_plus_iff_minus
    (ω : DerivedCategory (ModuleCat.{max u v} A)) (hω : IsDualizingComplex ω)
    (K : DerivedCategory (ModuleCat.{max u v} A))
    (hK : ∀ i : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{max u v} A) i).obj K)) :
    (DerivedCategory.TStructure.t).plus K ↔
      (DerivedCategory.TStructure.t).minus
        ((dualizingDerivedHomFunctor.{u, v} A ω).obj (Opposite.op K))

Dualizing.dualizingDerivedHom_minus_iff_plus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomDuality/Duality.lean, line 301. The attribute's comment: “exchange of bounded above and bounded below”.

On objects with finite cohomology, derived Hom into a dualizing complex exchanges bounded above with bounded below. The forward implication is the bound exchange Dualizing.dualizingDerivedHom_isGE_of_isLE; the converse applies the other bound exchange to RHom_A(K, ω) and transports the resulting bound along canonical biduality.

theorem dualizingDerivedHom_minus_iff_plus
    (ω : DerivedCategory (ModuleCat.{max u v} A)) (hω : IsDualizingComplex ω)
    (K : DerivedCategory (ModuleCat.{max u v} A))
    (hK : ∀ i : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{max u v} A) i).obj K)) :
    (DerivedCategory.TStructure.t).minus K ↔
      (DerivedCategory.TStructure.t).plus
        ((dualizingDerivedHomFunctor.{u, v} A ω).obj (Opposite.op K))

Dualizing.boundedCoherentDualizingDerivedHom_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomDuality/Duality.lean, line 376. The attribute's comment: “the bounded anti-equivalence”. References: SGA 5 I (App.7.3), “affine case”.

Derived Hom into a dualizing complex is an anti-equivalence on bounded objects with finite cohomology, [stacks 0A7C].

theorem boundedCoherentDualizingDerivedHom_isEquivalence
    (ω : DerivedCategory (ModuleCat.{max u v} A)) (hω : IsDualizingComplex ω) :
    (boundedCoherentDualizingDerivedHomFunctor.{u, v} A ω hω).IsEquivalence

Dualizing.nonempty_extIntoOmegaAtIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomDuality/ExtComparison.lean, line 428. The attribute's comment: “Ext–cohomology comparison”.

The Ext--cohomology comparison for derived Hom, natural in the source module. The ULift is necessary because derived morphisms live in a larger universe than the modules in the derived category. This comparison does not require ω to be dualizing.

public theorem nonempty_extIntoOmegaAtIso
    (ω : DerivedCategory (ModuleCat.{max u v} A)) (i : ℤ) :
    Nonempty (extIntoOmegaAt.{u, v} A ω i ≅
      (DerivedCategory.singleFunctor (ModuleCat.{max u v} A) 0).op ⋙
        dualizingDerivedHomFunctor.{u, v} A ω ⋙
          DerivedCategory.homologyFunctor (ModuleCat.{max u v} A) i ⋙
            ModuleCat.uliftFunctor.{max (u + 1) (v + 1), max u v} A)

Dualizing.dualizingDerivedHomFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingDerivedHom.lean, line 115. The attribute's comment: “the functor”.

The contravariant functor RHom_A(-, ω) defined using the canonical derived tensor--Hom adjunction.

public def dualizingDerivedHomFunctor
    (ω : DerivedCategory (ModuleCat.{max u v} A)) :
    (DerivedCategory (ModuleCat.{max u v} A))ᵒᵖ ⥤
      DerivedCategory (ModuleCat.{max u v} A)

Dualizing.dualizingDerivedHom_bounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingDerivedHom.lean, line 237. The attribute's comment: “preservation of bounded coherent objects”.

On objects with finite cohomology, derived Hom into a dualizing complex preserves cohomological boundedness.

public theorem dualizingDerivedHom_bounded [IsNoetherianRing A]
    (ω : DerivedCategory (ModuleCat.{max u v} A)) (hω : IsDualizingComplex ω)
    (K : DerivedCategory (ModuleCat.{max u v} A))
    (hK : ∀ i : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{max u v} A) i).obj K))
    (hK' : (DerivedCategory.TStructure.t).bounded K) :
    (DerivedCategory.TStructure.t).bounded
      ((dualizingDerivedHomFunctor.{u, v} A ω).obj (.op K))

Dualizing.dualizingDerivedHom_finiteCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingDerivedHom.lean, line 264. The attribute's comment: “preservation of coherent objects”.

Derived Hom into a dualizing complex has finite cohomology when its argument does.

This is Tag 0G4H specialized to a dualizing complex as target: a dualizing complex has finite cohomology and finite injective dimension, which are exactly the two hypotheses that tag puts on its second argument.

public theorem dualizingDerivedHom_finiteCohomology [IsNoetherianRing A]
    (ω : DerivedCategory (ModuleCat.{max u v} A)) (hω : IsDualizingComplex ω)
    (K : DerivedCategory (ModuleCat.{max u v} A))
    (hK : ∀ i : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{max u v} A) i).obj K)) :
    ∀ i : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{max u v} A) i).obj
        ((dualizingDerivedHomFunctor.{u, v} A ω).obj (.op K)))

Tag 0A7E, a lemma

Tag 0A7E in the Stacks Project.

Dualizing.isInvertible_obj_ring_of_linear_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Complexes/InvertibleImage/RingImageInvertible.lean, line 645.

Stacks 0A7E. An A-linear autoequivalence of the bounded derived category of complexes of A-modules with finite cohomology, an equivalence of categories with no compatibility with the shift or the triangulated structure assumed, sends the ring, placed in degree zero, to an invertible object of the unbounded derived category.

public theorem isInvertible_obj_ring_of_linear_isEquivalence [IsNoetherianRing A]
    (F : BoundedCoherentDerivedCategory A ⥤ BoundedCoherentDerivedCategory A)
    [F.IsEquivalence] [F.Linear A] :
    let m := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory A).choose
    letI := m
    MonoidalCategory.IsInvertible (F.obj (ringObject A)).obj

Tag 0A7F, a lemma

Tag 0A7F in the Stacks Project.

Dualizing.IsDualizingComplex.exists_iso_derivedTensorProduct_invertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Complexes/Uniqueness.lean, line 501. References: SGA 5 I (2.1), “affine case”.

Two dualizing complexes over a Noetherian ring differ by derived tensor product with an invertible object.

public theorem IsDualizingComplex.exists_iso_derivedTensorProduct_invertible
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    {K K' : DerivedCategory (ModuleCat.{max u v} A)}
    (hK : IsDualizingComplex K) (hK' : IsDualizingComplex K') :
    ∃ T : CochainComplex.DerivedTensor.DerivedTensorProductGeneral.{u, v} A,
      ∃ m : MonoidalCategory (DerivedCategory (ModuleCat.{max u v} A)),
        letI := m
        (Nonempty (MonoidalCategory.curriedTensor _ ≅ T.tensor) ∧
          Nonempty
          (𝟙_ (DerivedCategory (ModuleCat.{max u v} A)) ≅
            (DerivedCategory.singleFunctor (ModuleCat.{max u v} A) 0).obj
              (ModuleCat.of A (ULift.{v} A)))) ∧
          ∃ L : DerivedCategory (ModuleCat.{max u v} A),
            MonoidalCategory.IsInvertible L ∧
              Nonempty (K' ≅ (T.tensor.obj K).obj L)

Tag 0A7G, a lemma

Tag 0A7G in the Stacks Project.

Dualizing.isDualizingComplex_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Complex.lean, line 1024.

The derived extension of a dualizing complex along a localization is a dualizing complex over the localized ring.

theorem isDualizingComplex_localization {A : Type u} {B : Type w} [CommRing A] [CommRing B]
    [Algebra A B] [IsNoetherianRing A] (S : Submonoid A) [IsLocalization S B]
    (K : DerivedCategory (ModuleCat.{v} A)) (hK : IsDualizingComplex K) :
    @IsDualizingComplex (A := B) inferInstance
      (IsLocalization.isNoetherianRing S B inferInstance) inferInstance
      ((StacksDraft.PseudoCoherence.derivedExtensionScalars (algebraMap A B)).obj K)

Tag 0A7H, a lemma

Tag 0A7H in the Stacks Project.

Dualizing.isDualizingComplex_of_localizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalizationCriterion.lean, line 616.

Stacks Project, Tag 0A7H. A complex over a Noetherian ring is dualizing as soon as its derived localization at every member of a family of elements generating the unit ideal is a dualizing complex over the corresponding localization.

theorem isDualizingComplex_of_localizations [IsNoetherianRing A]
    {ι : Type w} (f : ι → A) (K : DerivedCategory (ModuleCat.{u} A))
    (hspan : Ideal.span (Set.range f) = ⊤)
    (hK : ∀ i, IsDualizingComplex ((localizationAwayFunctorAux.{u, u} (f i)).obj K)) :
    IsDualizingComplex K

Tag 0AX0, a lemma

Tag 0AX0 in the Stacks Project.

Dualizing.isDualizingComplex_derivedHom_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomothety/DerivedCoextensionIsDualizing.lean, line 187.

Stacks Project, Tag 0AX0. For a finite homomorphism of Noetherian rings and a dualizing complex ω over the source, RHom_A(B, ω) is a dualizing complex over B.

Noetherianity of B follows from that of A and finiteness of f, but it is a hypothesis here because Dualizing.IsDualizingComplex is only stated over a Noetherian ring, so the conclusion cannot be written down without it.

theorem isDualizingComplex_derivedHom_of_finite [IsNoetherianRing A] [IsNoetherianRing B]
    (f : A →+* B) (hf : f.Finite) (ω : DerivedCategory (ModuleCat.{max v u} A))
    (hω : IsDualizingComplex ω) :
    IsDualizingComplex ((derivedHom.{u, v, u} f).obj ω)

Tag 0A7I, a lemma

Tag 0A7I in the Stacks Project.

Dualizing.isDualizingComplex_derivedHom_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DerivedHomothety/DerivedCoextensionIsDualizing.lean, line 187. The attribute's comment: “the surjective case, a surjection being a finite ring map”.

Stacks Project, Tag 0AX0. For a finite homomorphism of Noetherian rings and a dualizing complex ω over the source, RHom_A(B, ω) is a dualizing complex over B.

Noetherianity of B follows from that of A and finiteness of f, but it is a hypothesis here because Dualizing.IsDualizingComplex is only stated over a Noetherian ring, so the conclusion cannot be written down without it.

theorem isDualizingComplex_derivedHom_of_finite [IsNoetherianRing A] [IsNoetherianRing B]
    (f : A →+* B) (hf : f.Finite) (ω : DerivedCategory (ModuleCat.{max v u} A))
    (hω : IsDualizingComplex ω) :
    IsDualizingComplex ((derivedHom.{u, v, u} f).obj ω)

Tag 0A7J, a lemma

Tag 0A7J in the Stacks Project.

Dualizing.polynomialBaseChange_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingComplexes/PolynomialBaseChange/IsDualizingComplex.lean, line 107.

A dualizing complex over a Noetherian ring remains dualizing after tensoring with the polynomial ring in one variable.

public theorem polynomialBaseChange_isDualizingComplex {A : Type u} [CommRing A]
    [IsNoetherianRing A] (K : DerivedCategory (ModuleCat.{v} A))
    (hK : IsDualizingComplex K) :
    IsDualizingComplex (polynomialBaseChange K)

Tag 0A7K, a proposition

Tag 0A7K in the Stacks Project.

Dualizing.exists_isDualizingComplex_of_isEssentiallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingComplexes/EssentiallyFiniteType.lean, line 61.

Stacks Project, Tag 0A7K. If a Noetherian ring A has a dualizing complex, then every A-algebra essentially of finite type over A has a dualizing complex.

theorem exists_isDualizingComplex_of_isEssentiallyOfFiniteType {A B : Type u} [CommRing A]
    [CommRing B] [IsNoetherianRing A] [Algebra A B]
    (hB : IsEssentiallyOfFiniteType A B (algebraMap A B))
    (K : DerivedCategory (ModuleCat.{u} A)) (hK : IsDualizingComplex K) :
    ∃ (hB' : IsNoetherianRing B) (L : DerivedCategory (ModuleCat.{u} B)),
      @IsDualizingComplex B _ hB' _ L

Tag 0A7L, a lemma

Tag 0A7L in the Stacks Project.

Dualizing.derivedHom_residueField_iso_shift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ResidueFieldShift.lean, line 279.

Stacks Project, Tag 0A7L. Derived Hom from the residue field at a maximal ideal into a dualizing complex is isomorphic to an integral shift of the residue field.

theorem derivedHom_residueField_iso_shift
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsDualizingComplex K)
    (m : Ideal A) (hm : m.IsMaximal) :
    ∃ n : ℤ, Nonempty
      ((derivedHom.{u, v, u} (Ideal.Quotient.mk m)).obj K ≅
        ((DerivedCategory.singleFunctor (ModuleCat.{max v u} (A ⧸ m)) 0).obj
          ((ModuleCat.uliftFunctor.{v} (A ⧸ m)).obj
            (ModuleCat.of (A ⧸ m) (A ⧸ m))))⟦n⟧)

Sources

LeanDualizing.IsDualizingComplex · Dualizing.derivedHom_finiteCohomology · Dualizing.derivedBiduality · Dualizing.dualizingDerivedHom_biduality_isIso · Dualizing.coherentDualizingDerivedHom_isEquivalence · Dualizing.dualizingDerivedHom_plus_iff_minus · Dualizing.dualizingDerivedHom_minus_iff_plus · Dualizing.boundedCoherentDualizingDerivedHom_isEquivalence

Section47.16 Dualizing complexes over local rings #

Section 47.16 of the Stacks Project, Tag 0A7M. 11 tags here are carried by 14 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A7M, the section

Tag 0A7M in the Stacks Project.

Declarations registered for the tag:

Dualizing.IsNormalizedDualizingComplex, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/NormalizedDualizingConvention.lean, line 46 (StacksFrontier): “the normalization convention RHom_A(κ, ω_A^•) = κ in degree zero”.
Dualizing.exists_isNormalizedDualizingComplex_shift, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/NormalizedDualizingConvention.lean, line 48 (StacksFrontier): “every dualizing complex over a Noetherian local ring is a shift of a normalized one”.
Dualizing.isNormalizedDualizingComplex_shift_iff_eq, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/NormalizedDualizingConvention.lean, line 50 (StacksFrontier): “the normalizing shift is unique”.

Tag 0AX1, a lemma

Tag 0AX1 in the Stacks Project.

Dualizing.isNormalizedDualizingComplex_derivedHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/NormalizedFiniteMap.lean, line 162.

Stacks Project, Tag 0AX1. If A → B is a finite local homomorphism of Noetherian local rings and K is a normalized dualizing complex over A, then RHom_A(B, K) is a normalized dualizing complex over B.

theorem isNormalizedDualizingComplex_derivedHom
    {A B : Type u} [CommRing A] [CommRing B]
    [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A] [IsNoetherianRing B]
    (f : A →+* B) [IsLocalHom f] (hf : f.Finite)
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex.{u, v} K) :
    IsNormalizedDualizingComplex.{u, v}
      ((derivedHom.{u, v} f).obj K)

Tag 0A7N, a lemma

Tag 0A7N in the Stacks Project.

Dualizing.isNormalizedDualizingComplex_derivedHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/NormalizedFiniteMap.lean, line 162. The attribute's comment: “the surjective case, a surjection of local rings being a finite local homomorphism”.

Stacks Project, Tag 0AX1. If A → B is a finite local homomorphism of Noetherian local rings and K is a normalized dualizing complex over A, then RHom_A(B, K) is a normalized dualizing complex over B.

theorem isNormalizedDualizingComplex_derivedHom
    {A B : Type u} [CommRing A] [CommRing B]
    [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A] [IsNoetherianRing B]
    (f : A →+* B) [IsLocalHom f] (hf : f.Finite)
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex.{u, v} K) :
    IsNormalizedDualizingComplex.{u, v}
      ((derivedHom.{u, v} f).obj K)

Tag 0A7P, a lemma

Tag 0A7P in the Stacks Project.

Dualizing.linearEquivalenceFiniteLengthIsoIdentity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Complex/Local.lean, line 888.

Every linear self-equivalence of finite-length modules over a Noetherian local ring is naturally isomorphic to the identity functor.

theorem linearEquivalenceFiniteLengthIsoIdentity
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (F : ObjectProperty.FullSubcategory (fun M : ModuleCat.{u} A => IsFiniteLength A M) ≌
      ObjectProperty.FullSubcategory (fun M : ModuleCat.{u} A => IsFiniteLength A M))
    [F.functor.Linear A] :
    Nonempty (F.functor ≅ 𝟭 (ObjectProperty.FullSubcategory
      (fun M : ModuleCat.{u} A => IsFiniteLength A M)))

Tag 0A7Q, a lemma

Tag 0A7Q in the Stacks Project.

Dualizing.derivedHomFiniteLengthIsoMatlisDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/FiniteLengthMatlisDuality/MatlisComparison.lean, line 764.

Stacks Project, Tag 0A7Q. Derived Hom into a normalized dualizing complex agrees naturally, on finite-length modules, with Matlis duality into an injective hull of the residue field.

public theorem derivedHomFiniteLengthIsoMatlisDual
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex K)
    (E : ModuleCat.{max v u} A)
    (i : (ModuleCat.uliftFunctor.{v} A).obj
      (ModuleCat.of A (IsLocalRing.ResidueField A)) ⟶ E) [Mono i]
    (hi : Module.IsInjectiveHull i) :
    Nonempty
      (derivedHomFiniteLengthFunctor A K ≅ matlisDualFiniteLengthFunctor A E)

Tag 0A7U, a lemma

Tag 0A7U in the Stacks Project.

Dualizing.depth_eq_least_nonzero_negative_ext, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DepthFromExt.lean, line 287. The attribute's comment: “depth_from_ext”.

Stacks Project, Tag 0A7U, part (3). For a nonzero finite module over a Noetherian local ring, depth is the least nonnegative integer δ for which Ext^(-δ)(M, ω_A^•) is nonzero.

public theorem depth_eq_least_nonzero_negative_ext
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    {M : Type (max v u)}
    [AddCommGroup M] [Module A M] [Module.Finite A M]
    (omega : DerivedCategory (ModuleCat.{max v u} A))
    (homega : IsNormalizedDualizingComplex omega)
    (hM : Nontrivial M) :
    ∃ delta : ℕ,
      IsLeast
          {i : ℕ |
            Nontrivial
              (DerivedCategory.Ext
                ((DerivedCategory.singleFunctor (ModuleCat.{max v u} A) 0).obj
                  (ModuleCat.of A M))
                omega (-(i : ℤ)))}
          delta ∧
        Module.depth A (IsLocalRing.maximalIdeal A) M = (delta : ℕ∞)

Dualizing.ext_degree_mem_Icc_of_nontrivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ExtDegreeBounds.lean, line 430. The attribute's comment: “ext_degree_bounds”. References: SGA 2 V (3.1), “(i)”.

Stacks Project, Tag 0A7U. For a nonzero finite module M of support dimension d, Ext from M into a normalized dualizing complex can be nonzero only in the integer degrees from -d through 0.

theorem ext_degree_mem_Icc_of_nontrivial
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    {M : Type (max v u)} [AddCommGroup M] [Module A M] [Module.Finite A M] [Nontrivial M]
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex K)
    (d : ℕ) (hd : Module.supportDim A M = (d : WithBot ℕ∞))
    (i : ℤ)
    (hi : Nontrivial
      (DerivedCategory.Ext
        ((DerivedCategory.singleFunctor (ModuleCat.{max v u} A) 0).obj
          (ModuleCat.of A M)) K i)) :
    i ∈ Set.Icc (-(d : ℤ)) 0

Dualizing.supportDim_ext_le_neg_degree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/ExtSupportBound.lean, line 357. The attribute's comment: “ext_support_bound”. References: SGA 2 V (3.1), “(ii)”.

Stacks Project, Tag 0A7U, support bound. If K is a normalized dualizing complex over a Noetherian local ring A and M is a nonzero finite A-module, then the support of Ext^i_A(M, K) has dimension at most -i for every integer i.

public theorem supportDim_ext_le_neg_degree
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A)) (M : Type (max v u))
    [AddCommGroup M] [Module A M] [Module.Finite A M] [Nontrivial M]
    (hK : IsNormalizedDualizingComplex K) (i : ℤ) :
    Module.supportDim A
        (DerivedCategory.Ext
          ((DerivedCategory.singleFunctor (ModuleCat.{max v u} A) 0).obj
            (ModuleCat.of A M)) K i) ≤
      if i ≤ 0 then (((Int.toNat (-i) : ℕ) : ℕ∞) : WithBot ℕ∞) else ⊥

Tag 0B5A, a lemma

Tag 0B5A in the Stacks Project.

Dualizing.isCohenMacaulay_iff_ext_concentrated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayCriterion.lean, line 287. The attribute's comment: “cm_criterion”.

Stacks Project, Tag 0B5A. For a nonzero finite module over a Noetherian local ring with normalized dualizing complex, Cohen--Macaulayness is equivalent to Ext into the dualizing complex being nonzero in at most one degree, and also to its being concentrated in degree minus the dimension of the support.

public theorem isCohenMacaulay_iff_ext_concentrated
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    {M : Type (max v u)} [AddCommGroup M] [Module A M] [Module.Finite A M] [Nontrivial M]
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex K) :
    List.TFAE [
      Module.IsCohenMacaulayAtMaximalIdeal A M,
      ∀ i j : ℤ,
        Nontrivial (DerivedCategory.Ext
          ((DerivedCategory.singleFunctor (ModuleCat.{max v u} A) 0).obj
            (ModuleCat.of A M)) K i) →
        Nontrivial (DerivedCategory.Ext
          ((DerivedCategory.singleFunctor (ModuleCat.{max v u} A) 0).obj
            (ModuleCat.of A M)) K j) → i = j,
      ∀ i : ℤ,
        ¬ (0 ≤ i ∧ Module.supportDim A M = ((i.toNat : ℕ∞) : WithBot ℕ∞)) →
          Subsingleton (DerivedCategory.Ext
            ((DerivedCategory.singleFunctor (ModuleCat.{max v u} A) 0).obj
              (ModuleCat.of A M)) K (-i))]

Dualizing.cohenMacaulayExtDuality, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayDuality.lean, line 1041. The attribute's comment: “cm_duality, that CM_d is anti-autoequivalent to itself”.

Cohen--Macaulay duality (Stacks Project, Tag 0B5A). For a normalized dualizing complex, Ext in degree minus the depth induces an anti-autoequivalence of the category of finite Cohen--Macaulay modules of that depth.

public noncomputable def cohenMacaulayExtDuality
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (omega : DerivedCategory (ModuleCat.{max u v} A))
    (homega : IsNormalizedDualizingComplex omega) (d : ℕ) :
    (CohenMacaulayModulesOfDepth.{u, max u v} A d)ᵒᵖ ≌
      CohenMacaulayModulesOfDepth.{u, max (u + 1) (v + 1)} A d

Dualizing.cohenMacaulayExtDuality_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayDuality.lean, line 1052. The attribute's comment: “cm_duality, that the anti-autoequivalence is M ↦ Ext^{-d}(M, ω)”.

The duality functor, after forgetting the Cohen--Macaulay condition, is naturally the canonical contravariant Ext^{-d} functor.

public theorem cohenMacaulayExtDuality_forget
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (omega : DerivedCategory (ModuleCat.{max u v} A))
    (homega : IsNormalizedDualizingComplex omega) (d : ℕ) :
    Nonempty
      ((cohenMacaulayExtDuality omega homega d).functor ⋙
          (IsCohenMacaulayModuleOfDepth.{u, max (u + 1) (v + 1)} A d).ι ≅
        (IsCohenMacaulayModuleOfDepth.{u, max u v} A d).ι.op ⋙
          extIntoDualizingComplex omega d)

Tag 0A7R, a lemma

Tag 0A7R in the Stacks Project.

Dualizing.nonempty_iso_single_injectiveHull_of_ringKrullDim_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/NormalizedZeroDimensional.lean, line 75.

Stacks Project, Tag 0A7R. A normalized dualizing complex over a zero-dimensional Noetherian local ring is an injective hull of the residue field placed in degree zero.

theorem nonempty_iso_single_injectiveHull_of_ringKrullDim_eq_zero
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex.{u, v} K) (hdim : ringKrullDim A = 0)
    (E : ModuleCat.{max v u} A)
    (i : (ModuleCat.uliftFunctor.{v} A).obj
      (ModuleCat.of A (IsLocalRing.ResidueField A)) ⟶ E) [Mono i]
    (hi : Module.IsInjectiveHull i) :
    Nonempty (K ≅ (DerivedCategory.singleFunctor (ModuleCat.{max v u} A) 0).obj E)

Tag 0A7S, a lemma

Tag 0A7S in the Stacks Project.

Dualizing.exists_distTriang_normalizedDualizing_quotient_finiteLengthIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/NormalizedFiniteLengthQuotient.lean, line 317.

Stacks Project, Tag 0A7S. If I is a finite-length ideal contained in the maximal ideal of a Noetherian local ring A, a normalized dualizing complex of A / I, restricted to A, fits into a distinguished triangle with the normalized dualizing complex of A and the degree-zero complex on Hom_A(I, E), for any injective hull E of the residue field.

theorem exists_distTriang_normalizedDualizing_quotient_finiteLengthIdeal
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex K)
    (I : Ideal A) (hI : I ≤ IsLocalRing.maximalIdeal A) (hIfl : IsFiniteLength A I)
    (E : ModuleCat.{max v u} A)
    (i : (ModuleCat.uliftFunctor.{v} A).obj
      (ModuleCat.of A (A ⧸ IsLocalRing.maximalIdeal A)) ⟶ E) [Mono i]
    (hi : Module.IsInjectiveHull i) :
    letI : Nontrivial (A ⧸ I) := Ideal.Quotient.nontrivial_iff.mpr
      (lt_of_le_of_lt hI
        (inferInstance : (IsLocalRing.maximalIdeal A).IsMaximal).lt_top).ne
    letI : IsLocalRing (A ⧸ I) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
    ∃ (KB : DerivedCategory (ModuleCat.{max v u} (A ⧸ I))),
      IsNormalizedDualizingComplex KB ∧
        ∃ (f : ((ModuleCat.restrictScalars (Ideal.Quotient.mk I)).mapDerivedCategory).obj KB ⟶ K)
          (g : K ⟶ (DerivedCategory.singleFunctor (ModuleCat.{max v u} A) 0).obj
            (ModuleCat.of A (I →ₗ[A] E)))
          (δ : (DerivedCategory.singleFunctor (ModuleCat.{max v u} A) 0).obj
              (ModuleCat.of A (I →ₗ[A] E)) ⟶
            (shiftFunctor (DerivedCategory (ModuleCat.{max v u} A)) (1 : ℤ)).obj
              (((ModuleCat.restrictScalars
                (Ideal.Quotient.mk I)).mapDerivedCategory).obj KB)),
          Triangle.mk f g δ ∈ distTriang (DerivedCategory (ModuleCat.{max v u} A))

Tag 0A7T, a lemma

Tag 0A7T in the Stacks Project.

Dualizing.exists_distinguishedTriangle_quotient_nonZeroDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/NormalizedRegularQuotient.lean, line 330.

Stacks Project, Tag 0A7T. Dividing a Noetherian local ring by a nonzerodivisor in its maximal ideal produces a normalized dualizing complex fitting into the distinguished triangle induced by multiplication by that element.

theorem exists_distinguishedTriangle_quotient_nonZeroDivisor
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex.{u, v} K)
    (f : A) (hf : f ∈ IsLocalRing.maximalIdeal A)
    (hfreg : f ∈ nonZeroDivisors A) :
    letI : Nontrivial (A ⧸ Ideal.span {f}) := Ideal.Quotient.nontrivial_iff.mpr
      (lt_of_le_of_lt (Ideal.span_le.2 (Set.singleton_subset_iff.mpr hf))
        (inferInstance : (IsLocalRing.maximalIdeal A).IsMaximal).lt_top).ne
    letI : IsLocalRing (A ⧸ Ideal.span {f}) :=
      IsLocalRing.of_surjective' (Ideal.Quotient.mk (Ideal.span {f}))
        Ideal.Quotient.mk_surjective
    ∃ (KB : DerivedCategory (ModuleCat.{max v u} (A ⧸ Ideal.span {f}))),
      IsNormalizedDualizingComplex.{u, v} KB ∧
        ∃ (i : ((ModuleCat.restrictScalars
              (Ideal.Quotient.mk (Ideal.span {f}))).mapDerivedCategory).obj KB ⟶ K)
          (δ : K ⟶ (shiftFunctor (DerivedCategory (ModuleCat.{max v u} A)) (1 : ℤ)).obj
            (((ModuleCat.restrictScalars
              (Ideal.Quotient.mk (Ideal.span {f}))).mapDerivedCategory).obj KB)),
          Triangle.mk i (f • 𝟙 K) δ ∈ distTriang (DerivedCategory (ModuleCat.{max v u} A))

Tag 0A7V, a lemma

Tag 0A7V in the Stacks Project.

Dualizing.nontrivial_localized_homology_iff_eq_neg_dimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/MinimalPrimeNonvanishing.lean, line 506.

Stacks Project, Tag 0A7V. Let A be a Noetherian local ring with a normalized dualizing complex K, and let p be a minimal prime of A with dim(A/p) = e. Then the localization at p of the cohomology module H^i(K) is nonzero if and only if i = -e.

theorem nontrivial_localized_homology_iff_eq_neg_dimension
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex.{u, v} K)
    (p : PrimeSpectrum A) (hp : IsMinimalPrime p.asIdeal) (e : ℕ)
    (hdim : ringKrullDim (A ⧸ p.asIdeal) = (e : WithBot ℕ∞)) (i : ℤ) :
    Nontrivial (LocalizedModule p.asIdeal.primeCompl
        ((DerivedCategory.homologyFunctor (ModuleCat.{max v u} A) i).obj K)) ↔
      i = -(e : ℤ)

Sources

LeanDualizing.IsNormalizedDualizingComplex · Dualizing.exists_isNormalizedDualizingComplex_shift · Dualizing.isNormalizedDualizingComplex_shift_iff_eq · Dualizing.isNormalizedDualizingComplex_derivedHom · Dualizing.linearEquivalenceFiniteLengthIsoIdentity · Dualizing.derivedHomFiniteLengthIsoMatlisDual · Dualizing.depth_eq_least_nonzero_negative_ext · Dualizing.ext_degree_mem_Icc_of_nontrivial

Section47.17 Dualizing complexes and dimension functions #

Section 47.17 of the Stacks Project, Tag 0A7W. 6 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A7W, the section

Tag 0A7W in the Stacks Project.

Dualizing.dualizingDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DimensionFunction.lean, line 119. The attribute's comment: “the function δ attached to a dualizing complex over a Noetherian ring”.

The dimension function of a dualizing complex K over a Noetherian ring A: the value at a prime p is the unique integer n for which the localization K_p, shifted by -n, is a normalized dualizing complex over A_p. The infimum is a device for naming that integer; it is attained and unique by Dualizing.dualizingDimension_eq_iff.

noncomputable def dualizingDimension {A : Type u} [CommRing A] [IsNoetherianRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A)) (p : PrimeSpectrum A) : ℤ

Dualizing.dualizingDimension_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DimensionFunction.lean, line 151. The attribute's comment: “δ(p) is the unique integer n with K_p⟦-n⟧ normalized over A_p”.

The defining property of the dimension function. A shift of the localization of a dualizing complex at a prime is normalized exactly when the shift is the value of the dimension function there.

theorem dualizingDimension_eq_iff {A : Type u} [CommRing A] [IsNoetherianRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A)) (hK : IsDualizingComplex K)
    (p : PrimeSpectrum A) (n : ℤ) :
    IsNormalizedDualizingComplex.{u, v}
        (((StacksDraft.PseudoCoherence.derivedExtensionScalars
          (algebraMap A (Localization.AtPrime p.asIdeal))).obj K)⟦-n⟧) ↔
      n = dualizingDimension.{u, v} K p

Tag 0A7X, a lemma

Tag 0A7X in the Stacks Project.

Dualizing.existsUnique_nontrivial_localized_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/MinimalPrimeNonvanishing.lean, line 533.

Stacks Project, Tag 0A7X. Let A be a Noetherian ring with a dualizing complex K and let p be a minimal prime of A. Then the localization at p of the cohomology module H^i(K) is nonzero for exactly one i.

theorem existsUnique_nontrivial_localized_homology
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (K : DerivedCategory (ModuleCat.{v} A)) (hK : IsDualizingComplex K)
    (p : Ideal A) [p.IsPrime] (hp : p ∈ minimalPrimes A) :
    ∃! i : ℤ, Nontrivial
      (LocalizedModule p.primeCompl
        ((DerivedCategory.homologyFunctor (ModuleCat.{v} A) i).obj K))

Tag 0A7Y, a lemma

Tag 0A7Y in the Stacks Project.

Dualizing.dualizingDimension_derivedHom_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DimensionFunctionSurjective.lean, line 756.

Stacks 0A7Y. For a surjection f : A → B of Noetherian rings and a dualizing complex K over A, the dimension function of the dualizing complex RHom_A(B, K) over B is the restriction of the dimension function of K along the induced closed immersion Spec B → Spec A.

The hypothesis of Dualizing.dualizingDimension_derivedHom_of_surjective_of_localizationComparison is discharged here: the localization at q of RHom_A(B, K) is RHom_{A_p}(B_q, K_p), where g : A_p → B_q is the surjection of local rings induced by f. Both sides are computed by one and the same complex of B_q-modules, namely the degreewise localization of the degreewise coextension of scalars of a bounded complex of injectives representing K; the identification of the two complexes is Dualizing.coextendExtendScalarsIso.

theorem dualizingDimension_derivedHom_of_surjective
    (f : A →+* B) (hf : Function.Surjective f)
    (K : DerivedCategory (ModuleCat.{max v u} A)) (hK : IsDualizingComplex K)
    (q : PrimeSpectrum B) :
    dualizingDimension.{u, v} ((derivedHom.{u, v} f).obj K) q
      = dualizingDimension.{u, v} K (PrimeSpectrum.comap f q)

Tag 0A7Z, a lemma

Tag 0A7Z in the Stacks Project.

Dualizing.dualizingDimension_eq_succ_of_isImmediateSpecialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DimensionFunctionSpecialization.lean, line 301. The attribute's comment: “δ(p) = δ(q) + 1 for an immediate specialization p ⤳ q”.

The dimension function of a dualizing complex drops by exactly one along an immediate specialization.

theorem dualizingDimension_eq_succ_of_isImmediateSpecialization
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A)) (hK : IsDualizingComplex K)
    {p q : PrimeSpectrum A} (himm : IsImmediateSpecialization p q) :
    dualizingDimension.{u, v} K p = dualizingDimension.{u, v} K q + 1

Dualizing.dualizingDimension_lt_of_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DimensionFunctionSpecialization.lean, line 392. The attribute's comment: “δ(q) < δ(p) for a non-trivial specialization p ⤳ q”.

The dimension function of a dualizing complex drops strictly along a non-trivial specialization.

theorem dualizingDimension_lt_of_specializes
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A)) (hK : IsDualizingComplex K)
    {p q : PrimeSpectrum A} (hpq : p ⤳ q) (hne : p ≠ q) :
    dualizingDimension.{u, v} K q < dualizingDimension.{u, v} K p

Dualizing.dualizingDimensionFunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DimensionFunctionSpecialization.lean, line 404. The attribute's comment: “the function δ of a dualizing complex is a dimension function on Spec A”.

The dimension function δ_K of a dualizing complex K over a Noetherian ring A, as a dimension function on Spec A.

def dualizingDimensionFunction {A : Type u} [CommRing A] [IsNoetherianRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A)) (hK : IsDualizingComplex K) :
    TopologicalSpace.DimensionFunction (PrimeSpectrum A)

Tag 0A80, a lemma

Tag 0A80 in the Stacks Project.

Dualizing.ringKrullDim_lt_top_of_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/FiniteDimension.lean, line 360. The attribute's comment: “of finite dimension”.

Stacks Project, Tag 0A80. A Noetherian ring admitting a dualizing complex has finite Krull dimension.

theorem ringKrullDim_lt_top_of_isDualizingComplex {A : Type u} [CommRing A] [IsNoetherianRing A]
    {K : DerivedCategory (ModuleCat.{u} A)} (hK : IsDualizingComplex K) :
    ringKrullDim A < ⊤

Dualizing.isUniversallyCatenary_of_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UniversallyCatenary.lean, line 110. The attribute's comment: “universally catenary”.

Stacks Project, Tag 0A80. A Noetherian ring admitting a dualizing complex is universally catenary: every algebra of finite type over it is catenary.

theorem isUniversallyCatenary_of_isDualizingComplex {A : Type u} [CommRing A] [IsNoetherianRing A]
    {K : DerivedCategory (ModuleCat.{u} A)} (hK : IsDualizingComplex K) :
    Ring.IsUniversallyCatenary A

Tag 0AWE, a lemma

Tag 0AWE in the Stacks Project.

Dualizing.support_canonicalModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CanonicalModule.lean, line 293. The attribute's comment: “(1): the support of ω_A is the union of the d-dimensional irreducible components”.

Let A be a Noetherian local ring with a normalized dualizing complex K, let d = dim(A) and let ω_A = H^{-d}(K). The support of ω_A is the union of the irreducible components of Spec(A) of dimension d.

theorem support_canonicalModule
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K : DerivedCategory (ModuleCat.{u} A)) (hK : IsNormalizedDualizingComplex.{u, u} K)
    (d : ℕ) (hd : ringKrullDim A = (d : WithBot ℕ∞)) :
    Module.support A ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-(d : ℤ))).obj K) =
      ⋃₀ {C ∈ irreducibleComponents (PrimeSpectrum A) |
        topologicalKrullDim C = (d : WithBot ℕ∞)}

Dualizing.propertySkModule_canonicalModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CanonicalModuleDepth.lean, line 603. The attribute's comment: “(2): the canonical module ω_A satisfies Serre's condition (S₂)”.

Let A be a Noetherian local ring with a normalized dualizing complex K, let d = dim(A) and let ω_A = H^{-d}(K). Then ω_A satisfies Serre's condition (S₂).

theorem propertySkModule_canonicalModule {A : Type u} [CommRing A] [IsNoetherianRing A]
    [IsLocalRing A] (K : DerivedCategory (ModuleCat.{u} A))
    (hK : IsNormalizedDualizingComplex.{u, u} K) :
    let d := (ringKrullDim A).unbotD 0 |>.toNat
    let ω := (DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-(d : ℤ))).obj K
    letI : Module.Finite A ω := hK.1.finiteCohomology (-(d : ℤ))
    PropertySkModule A ω 2

Sources

LeanDualizing.dualizingDimension · Dualizing.dualizingDimension_eq_iff · Dualizing.existsUnique_nontrivial_localized_homology · Dualizing.dualizingDimension_derivedHom_of_surjective · Dualizing.dualizingDimension_eq_succ_of_isImmediateSpecialization · Dualizing.dualizingDimension_lt_of_specializes · Dualizing.dualizingDimensionFunction · Dualizing.ringKrullDim_lt_top_of_isDualizingComplex

Section47.18 The local duality theorem #

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

Tag 0A82, a lemma

Tag 0A82 in the Stacks Project.

Dualizing.LocalDuality.exists_isInjectiveHull_homology_zero_localCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/NormalizedDualizingComplex/InjectiveHull.lean, line 663. The attribute's comment: “injective hull”.

The degree-zero local cohomology of a normalized dualizing complex at the closed point is an injective hull of the residue field.

public theorem exists_isInjectiveHull_homology_zero_localCohomology
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex K) :
    let m := IsLocalRing.maximalIdeal A
    let hm : m.FG := IsNoetherian.noetherian m
    let L := (derivedPowerTorsionProperty A m hm).ι.obj
      ((localCohomologyFunctor A m hm).obj K)
    let E := (DerivedCategory.homologyFunctor (ModuleCat.{max v u} A) 0).obj L
    ∃ (i : (ModuleCat.uliftFunctor.{v} A).obj
          (ModuleCat.of A (IsLocalRing.ResidueField A)) ⟶ E)
        (hi : Mono i),
      @Module.IsInjectiveHull (ModuleCat.{max v u} A) _ _ _ _ _ i hi

Dualizing.LocalDuality.nonempty_localCohomology_iso_single_homology_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/NormalizedDualizingComplex/InjectiveHull.lean, line 687. The attribute's comment: “concentration in degree zero”.

Local cohomology of a normalized dualizing complex at the closed point is its degree-zero cohomology module placed in degree zero.

public theorem nonempty_localCohomology_iso_single_homology_zero
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K : DerivedCategory (ModuleCat.{max v u} A))
    (hK : IsNormalizedDualizingComplex K) :
    let m := IsLocalRing.maximalIdeal A
    let hm : m.FG := IsNoetherian.noetherian m
    let L := (derivedPowerTorsionProperty A m hm).ι.obj
      ((localCohomologyFunctor A m hm).obj K)
    let E := (DerivedCategory.homologyFunctor (ModuleCat.{max v u} A) 0).obj L
    Nonempty (L ≅ (DerivedCategory.singleFunctor (ModuleCat.{max v u} A) 0).obj E)

Tag 0A83, a remark

Tag 0A83 in the Stacks Project.

Dualizing.LocalDuality.nonempty_localCohomology_iso_localCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/LocalDuality.lean, line 71. The attribute's comment: “the realization is independent of the normalized dualizing complex”.

Let (A, 𝔪, κ) be a Noetherian local ring and let Z = V(𝔪). If ω and ω' are normalized dualizing complexes for A, then RΓ_Z(ω) ≅ RΓ_Z(ω') in D(A).

public theorem nonempty_localCohomology_iso_localCohomology
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (ω ω' : DerivedCategory (ModuleCat.{max v u} A))
    (hω : IsNormalizedDualizingComplex.{u, v} ω)
    (hω' : IsNormalizedDualizingComplex.{u, v} ω') :
    Nonempty
      ((derivedPowerTorsionProperty A (IsLocalRing.maximalIdeal A)
              (IsNoetherian.noetherian _)).ι.obj
            ((localCohomologyFunctor A (IsLocalRing.maximalIdeal A)
              (IsNoetherian.noetherian _)).obj ω) ≅
          (derivedPowerTorsionProperty A (IsLocalRing.maximalIdeal A)
              (IsNoetherian.noetherian _)).ι.obj
            ((localCohomologyFunctor A (IsLocalRing.maximalIdeal A)
              (IsNoetherian.noetherian _)).obj ω'))

Dualizing.LocalDuality.injectiveHullUnitsMulEquivUnitsAdicCompletion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/LocalDuality.lean, line 101. The attribute's comment: “the automorphism group of an injective hull of the residue field is the units of the completion”.

Let (A, 𝔪, κ) be a Noetherian local ring and let i : κ ⟶ E present E as an injective hull of the residue field. The units of End_A(E) are the units of the 𝔪-adic completion A^∧ of A.

public def injectiveHullUnitsMulEquivUnitsAdicCompletion
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (E : Type u) [AddCommGroup E] [Module A E]
    (i : ModuleCat.of A (A ⧸ IsLocalRing.maximalIdeal A) ⟶ ModuleCat.of A E)
    [Mono i] (hi : Module.IsInjectiveHull i) :
    (Module.End A E)ˣ ≃* (AdicCompletion (IsLocalRing.maximalIdeal A) A)ˣ

Dualizing.IsNormalizedDualizingComplex.nonempty_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/NormalizedUniqueness.lean, line 108. The attribute's comment: “a normalized dualizing complex is unique up to isomorphism; stated at the ring's own module universe”.

A normalized dualizing complex over a Noetherian local ring is unique up to isomorphism. Two dualizing complexes differ by derived tensor product with an invertible object ([Stacks, Tag 0A7F]); over a local ring such an object is the ring placed in a single degree ([Stacks, Tag 0FNT]), so the two complexes differ by a shift; and the normalization convention of [Stacks, Tag 0A7M] admits exactly one normalizing shift, so that shift is zero.

This is the uniqueness half of the comparison made in [Stacks, Tag 0A83], whose other side — uniqueness of an injective hull of the residue field — is [Stacks, Tag 08Y4].

public theorem IsNormalizedDualizingComplex.nonempty_iso
    {A : Type u} [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    {ω ω' : DerivedCategory (ModuleCat.{u} A)}
    (hω : IsNormalizedDualizingComplex.{u, u} ω)
    (hω' : IsNormalizedDualizingComplex.{u, u} ω') :
    Nonempty (ω ≅ ω')

Dualizing.IsDualizingComplex.autMulEquivUnits, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/NormalizedUniqueness.lean, line 173. The attribute's comment: “the automorphism group of a dualizing complex is the group of units of the base ring; proved for every dualizing complex, not only a normalized one, and stated at the ring's own module universe”.

The automorphism group of a dualizing complex is the unit group of the base ring. Reading off the units of Dualizing.IsDualizingComplex.endAlgEquiv: an automorphism of ω in D(A) is multiplication by a unique unit of A.

This is the automorphism-group half of the comparison made in [Stacks, Tag 0A83]. The source states it for a normalized dualizing complex over a Noetherian local ring; no normalization and no local hypothesis are needed, so the statement here is more general. The other side of the comparison is Dualizing.LocalDuality.injectiveHullUnitsMulEquivUnitsAdicCompletion, where the automorphism group is instead the units of the 𝔪-adic completion.

public def IsDualizingComplex.autMulEquivUnits
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    {ω : DerivedCategory (ModuleCat.{u} A)} (hω : IsDualizingComplex ω) :
    Aut ω ≃* Aˣ

Declarations registered for the tag:

exists_isInjectiveHull_homology_zero_localCohomology registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/LocalCohomology/LocalDuality.lean, line 109 (StacksFrontier): “the opening sentence, that RΓ_Z(ω) is an injective hull of the residue field: the hull half, read from Stacks 0A82”.
nonempty_localCohomology_iso_single_homology_zero registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/LocalCohomology/LocalDuality.lean, line 113 (StacksFrontier): “the opening sentence, that RΓ_Z(ω) is an injective hull of the residue field placed in degree zero: the concentration half, read from Stacks 0A82”.
Module.exists_iso_of_isInjectiveHull, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/Dualizing/LocalCohomology/LocalDuality.lean, line 117 (StacksFrontier): “an injective hull of the residue field is unique up to isomorphism; proved for an arbitrary object of an arbitrary abelian category, which is Stacks 08Y4”.

Tag 0A84, a theorem

Tag 0A84 in the Stacks Project.

Dualizing.LocalDuality.nonempty_derivedCompletion_derivedHom_iso_derivedHom_injectiveHull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/LocalDuality.lean, line 145.

The local duality theorem. Let (A, 𝔪, κ) be a Noetherian local ring, let ω be a normalized dualizing complex, let i : κ ⟶ E be an injective hull of the residue field, and let Z = V(𝔪). Then derived 𝔪-adic completion of RHom_A(K, ω) is RHom_A(RΓ_Z(K), E[0]), for every K in D(A).

public theorem nonempty_derivedCompletion_derivedHom_iso_derivedHom_injectiveHull
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    {r : ℕ} (f : Fin r → A) (hf : Ideal.span (Set.range f) = IsLocalRing.maximalIdeal A)
    (ω : DerivedCategory (ModuleCat.{u} A))
    (hω : IsNormalizedDualizingComplex.{u, u} ω)
    {E : ModuleCat.{u} A}
    (i : (ModuleCat.uliftFunctor.{u} A).obj
      (ModuleCat.of A (IsLocalRing.ResidueField A)) ⟶ E)
    [Mono i] (hi : Module.IsInjectiveHull i)
    (K : DerivedCategory (ModuleCat.{u} A)) :
    Nonempty
      ((DerivedCompletion.derivedCompletionFunctor A f).obj
          ((derivedHomAdjunction (R := A)).hom.obj (Opposite.op K, ω)) ≅
        (derivedHomAdjunction (R := A)).hom.obj
          (Opposite.op ((derivedPowerTorsionProperty A (IsLocalRing.maximalIdeal A)
              (IsNoetherian.noetherian _)).ι.obj
            ((localCohomologyFunctor A (IsLocalRing.maximalIdeal A)
              (IsNoetherian.noetherian _)).obj K)),
            (DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj E))

Dualizing.LocalDuality.nonempty_localDualityNatIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/LocalDuality.lean, line 180. The attribute's comment: “natural in K”.

The local duality theorem, natural in K. Let (A, 𝔪, κ) be a Noetherian local ring, let ω be a normalized dualizing complex, let i : κ ⟶ E be an injective hull of the residue field, and let Z = V(𝔪). Then derived 𝔪-adic completion of RHom_A(-, ω) is RHom_A(RΓ_Z(-), E[0]), as an isomorphism of contravariant functors on D(A).

public theorem nonempty_localDualityNatIso
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    {r : ℕ} (f : Fin r → A) (hf : Ideal.span (Set.range f) = IsLocalRing.maximalIdeal A)
    (ω : DerivedCategory (ModuleCat.{u} A))
    (hω : IsNormalizedDualizingComplex.{u, u} ω)
    {E : ModuleCat.{u} A}
    (i : (ModuleCat.uliftFunctor.{u} A).obj
      (ModuleCat.of A (IsLocalRing.ResidueField A)) ⟶ E)
    [Mono i] (hi : Module.IsInjectiveHull i) :
    Nonempty (Dualizing.derivedHomInto A ω ⋙ DerivedCompletion.derivedCompletionFunctor A f ≅
      (Stacks.LocalCohomology.CechFormula.localCohomologyEndofunctor A
          (IsLocalRing.maximalIdeal A) (IsNoetherian.noetherian _)).op ⋙
        Dualizing.derivedHomInto A
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj E))

Tag 0AAK, a lemma

Tag 0AAK in the Stacks Project.

Dualizing.LocalDuality.nonempty_adicCompletion_ext_linearEquiv_linearMap_localCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/LocalDualityExt.lean, line 771. References: SGA 2 V (2.1), “Ext^{-i}≅Hom(H^i,E)”.

Let (A, 𝔪, κ) be a Noetherian local ring, let ω be a normalized dualizing complex, let ι : κ ⟶ E be an injective hull of the residue field, and let K be an object of D_Coh(A), that is, a complex all of whose cohomology modules are finite. Then the 𝔪-adic completion of Ext^{-i}_A(K, ω) is isomorphic to the module of A-linear maps from H^i_𝔪(K) to E. Local cohomology is RΓ_Z for Z = V(𝔪), and Ext^{-i}_A(K, ω) is Hom_{D(A)}(K, ω⟦-i⟧).

public theorem nonempty_adicCompletion_ext_linearEquiv_linearMap_localCohomology
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    {r : ℕ} (f : Fin r → A)
    (hf : Ideal.span (Set.range f) = IsLocalRing.maximalIdeal A)
    (ω : DerivedCategory (ModuleCat.{u} A))
    (hω : IsNormalizedDualizingComplex.{u, u} ω)
    (K : DerivedCategory (ModuleCat.{u} A))
    (hK : ∀ j : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) j).obj K))
    {E : ModuleCat.{u} A}
    (ι : (ModuleCat.uliftFunctor.{u} A).obj
      (ModuleCat.of A (IsLocalRing.ResidueField A)) ⟶ E)
    [Mono ι] (hι : Module.IsInjectiveHull ι) (i : ℤ) :
    Nonempty
      (AdicCompletion (IsLocalRing.maximalIdeal A)
          (DerivedCategory.Ext K ω (-i)) ≃ₗ[A]
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
            ((derivedPowerTorsionProperty A (IsLocalRing.maximalIdeal A)
                (IsNoetherian.noetherian _)).ι.obj
              ((localCohomologyFunctor A (IsLocalRing.maximalIdeal A)
                (IsNoetherian.noetherian _)).obj K)) →ₗ[A] E))

Dualizing.LocalDuality.exists_localDualityExtNatEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCohomology/LocalDualityExt.lean, line 878. The attribute's comment: “natural in K”.

Let (A, 𝔪, κ) be a Noetherian local ring, let ω be a normalized dualizing complex, let ι : κ ⟶ E be an injective hull of the residue field, and let Z = V(𝔪). For every integer i there is a family of A-linear isomorphisms

H^0(RHom_A(K, ω⟦-i⟧)^∧) ≅ Hom_A(H^i_Z(K), E)

indexed by the objects K of D(A), compatible with the maps induced by every morphism of D(A): local duality in its module form, natural in K.

The left-hand side is the degree-zero cohomology of the derived 𝔪-adic completion of RHom_A(K, ω⟦-i⟧), whose degree-zero cohomology is Ext^{-i}_A(K, ω); the right-hand side is the Matlis dual of the degree-i local cohomology module.

public theorem exists_localDualityExtNatEquiv
    [IsNoetherianRing A] [IsLocalRing A]
    {r : ℕ} (f : Fin r → A) (hf : Ideal.span (Set.range f) = IsLocalRing.maximalIdeal A)
    (ω : DerivedCategory (ModuleCat.{u} A))
    (hω : IsNormalizedDualizingComplex.{u, u} ω)
    {E : ModuleCat.{u} A}
    (ι : (ModuleCat.uliftFunctor.{u} A).obj
      (ModuleCat.of A (IsLocalRing.ResidueField A)) ⟶ E)
    [Mono ι] (hι : Module.IsInjectiveHull ι) (i : ℤ) :
    ∃ θ : ∀ K : DerivedCategory (ModuleCat.{u} A),
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).obj
            ((DerivedCompletion.derivedCompletionFunctor A f).obj
              ((StacksDraft.DerivedHom.derivedHomAdjunction (R := A)).hom.obj
                (Opposite.op K,
                  (CategoryTheory.shiftFunctor
                    (DerivedCategory (ModuleCat.{u} A)) (-i)).obj ω))) : Type u) ≃ₗ[A]
          (((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
              ((localCohomologyEndofunctor A (IsLocalRing.maximalIdeal A)
                (IsNoetherian.noetherian _)).obj K) : Type u) →ₗ[A] (E : Type u)),
      ∀ (K K' : DerivedCategory (ModuleCat.{u} A)) (g : K' ⟶ K)
        (x : ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).obj
          ((DerivedCompletion.derivedCompletionFunctor A f).obj
            ((StacksDraft.DerivedHom.derivedHomAdjunction (R := A)).hom.obj
              (Opposite.op K,
                (CategoryTheory.shiftFunctor
                  (DerivedCategory (ModuleCat.{u} A)) (-i)).obj ω))) : Type u)),
        θ K' (((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).map
              ((DerivedCompletion.derivedCompletionFunctor A f).map
                ((StacksDraft.DerivedHom.derivedHomAdjunction (R := A)).hom.map
                  (show (Opposite.op K, (CategoryTheory.shiftFunctor
                        (DerivedCategory (ModuleCat.{u} A)) (-i)).obj ω) ⟶
                      (Opposite.op K', (CategoryTheory.shiftFunctor
                        (DerivedCategory (ModuleCat.{u} A)) (-i)).obj ω) from
                    (g.op, 𝟙 _))))).hom x) =
          (θ K x).comp
            ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map
              ((localCohomologyEndofunctor A (IsLocalRing.maximalIdeal A)
                (IsNoetherian.noetherian _)).map g)).hom

Stacks.LocalCohomology.nonempty_adicCompletion_ext_linearEquiv_matlisDual_localCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/FaltingsAnnihilator/LocalDuality.lean, line 339. The attribute's comment: “the module form, with the support-closed-subset model of local cohomology in place of the torsion-complex model”.

Stacks Project, Tag 0AAK in the spelling of local cohomology with support in V(𝔪). Over a Noetherian local ring with a normalized dualizing complex, the 𝔪-adic completion of Ext^{-i}(K, ω) is the Matlis dual of H^i_{V(𝔪)}(K).

theorem nonempty_adicCompletion_ext_linearEquiv_matlisDual_localCohomology
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K ω : DerivedCategory (ModuleCat.{u} A))
    (hK : ∀ j : ℤ, Module.Finite A
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) j).obj K))
    (hω : Dualizing.IsNormalizedDualizingComplex ω)
    (E : ModuleCat.{u} A)
    (e : (ModuleCat.uliftFunctor.{u} A).obj
      (ModuleCat.of A (IsLocalRing.ResidueField A)) ⟶ E)
    [Mono e] (he : Module.IsInjectiveHull e) (i : ℤ) :
    Nonempty
      (AdicCompletion (maximalIdeal A) (DerivedCategory.Ext K ω (-i)) ≃ₗ[A]
        (localCohomologyWithSupportIn
          A (PrimeSpectrum.zeroLocus (maximalIdeal A : Set A)) K i →ₗ[A] E))

Stacks.LocalCohomology.nonempty_adicCompletion_ext_linearEquiv_matlisDual_localCohomologyPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/FaltingsAnnihilator/LocalDuality.lean, line 377. The attribute's comment: “the module form for a bounded-below complex, with the support-closed-subset model of local cohomology”.

Stacks Project, Tag 0AAK for a bounded-below complex.

theorem nonempty_adicCompletion_ext_linearEquiv_matlisDual_localCohomologyPlus
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (K : DerivedCategory.Plus (ModuleCat.{u} A))
    (ω : DerivedCategory (ModuleCat.{u} A))
    (hK : ∀ j : ℤ, Module.Finite A
      ((DerivedCategory.Plus.homologyFunctor (ModuleCat.{u} A) j).obj K))
    (hω : Dualizing.IsNormalizedDualizingComplex ω)
    (E : ModuleCat.{u} A)
    (e : (ModuleCat.uliftFunctor.{u} A).obj
      (ModuleCat.of A (IsLocalRing.ResidueField A)) ⟶ E)
    [Mono e] (he : Module.IsInjectiveHull e) (i : ℤ) :
    Nonempty
      (AdicCompletion (maximalIdeal A) (DerivedCategory.Ext K.obj ω (-i)) ≃ₗ[A]
        (localCohomologyWithSupportInPlus
          A (PrimeSpectrum.zeroLocus (maximalIdeal A : Set A)) K i →ₗ[A] E))

Stacks.LocalCohomology.nonempty_adicCompletion_localizedDualCohomology_linearEquiv_matlisDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/FaltingsAnnihilator/LocalDuality.lean, line 726. The attribute's comment: “local duality at an arbitrary prime of a Noetherian ring with a dualizing complex, reached from the local case through the normalizing shift of 0A7Z and flat base change of Ext; objectwise, with no naturality in the complex”.

Local duality at an arbitrary prime. Let A be Noetherian with dualizing complex ω and dimension function δ, let q be a prime, and let E be an injective hull of the residue field of A_q. For K in D⁺_{Coh}(A) and n + i = -δ(q), the qA_q-adic completion of H^n(RHom_A(K, ω))_q is the Matlis dual of H^i_{qA_q}(K_q).

This is [Stacks, Tag 0AAK] at a general prime: the localization ω_q⟦-δ(q)⟧ is a normalized dualizing complex over A_q by [Stacks, Tag 0A7Z], and flat base change identifies H^n(RHom_A(K, ω))_q with Ext^n_{A_q}(K_q, ω_q). It is the local-duality input to the proof of [Stacks, Tag 0EFX]. The two sides are isomorphic as A_q-modules for each K separately; no naturality in K is claimed, and 0AAK provides none.

theorem nonempty_adicCompletion_localizedDualCohomology_linearEquiv_matlisDual
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (q : PrimeSpectrum A) (K : DerivedCategory.Plus (ModuleCat.{u} A))
    (hK : ∀ i : ℤ, Module.Finite A
      ((DerivedCategory.Plus.homologyFunctor (ModuleCat.{u} A) i).obj K))
    (ω : DerivedCategory (ModuleCat.{u} A)) (hω : Dualizing.IsDualizingComplex ω)
    (E : ModuleCat.{u} (Localization.AtPrime q.asIdeal))
    (e : (ModuleCat.uliftFunctor.{u} (Localization.AtPrime q.asIdeal)).obj
      (ModuleCat.of (Localization.AtPrime q.asIdeal)
        (ResidueField (Localization.AtPrime q.asIdeal))) ⟶ E)
    [Mono e] (he : Module.IsInjectiveHull e)
    (n i : ℤ) (hni : n + i = -Dualizing.dualizingDimension ω q) :
    Nonempty
      (AdicCompletion (maximalIdeal (Localization.AtPrime q.asIdeal))
          (LocalizedModule q.asIdeal.primeCompl
            ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) n).obj
              ((Dualizing.dualizingDerivedHomFunctor.{u, u} A ω).obj (.op K.obj))))
          ≃ₗ[Localization.AtPrime q.asIdeal]
        (localCohomologyWithSupportInPlus (Localization.AtPrime q.asIdeal)
          (PrimeSpectrum.zeroLocus (maximalIdeal (Localization.AtPrime q.asIdeal) : Set _))
          (localizedComplex.{u, u} q K) i →ₗ[Localization.AtPrime q.asIdeal] E))

Sources

LeanDualizing.LocalDuality.exists_isInjectiveHull_homology_zero_localCohomology · Dualizing.LocalDuality.nonempty_localCohomology_iso_single_homology_zero · Dualizing.LocalDuality.nonempty_localCohomology_iso_localCohomology · Dualizing.LocalDuality.injectiveHullUnitsMulEquivUnitsAdicCompletion · Dualizing.IsNormalizedDualizingComplex.nonempty_iso · Dualizing.IsDualizingComplex.autMulEquivUnits · exists_isInjectiveHull_homology_zero_localCohomology · nonempty_localCohomology_iso_single_homology_zero

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

47.2 Essential surjections and… to 47.18 The local duality theorem

Section47.2 Essential surjections and injections#

Tag 08XJ, a definition

Tag 08XK, a lemma

Tag 08XL, a lemma

Tag 08XM, a lemma

Sources

Section47.3 Injective modules#

Tag 08XP, a lemma

Tag 08XQ, a lemma

Tag 08YV, a lemma

Tag 08XR, a lemma

Tag 08XS, a lemma

Tag 08XT, an example

Tag 08XV, a lemma

Tag 0A6I, a lemma

Tag 08XW, a lemma

Tag 0A6J, a lemma

Sources

Section47.4 Projective covers#

Tag 08XY, a definition

Tag 08XZ, a lemma

Tag 08Y0, a lemma

Sources

Section47.5 Injective hulls#

Tag 08Y2, a definition

Tag 08Y3, a lemma

Tag 08Y4, a lemma

Tag 08Y5, an example

Tag 08Y6, a definition

Tag 08Y7, a lemma

Tag 08Y8, a lemma

Tag 08Y9, a lemma

Tag 08YA, a proposition

Sources

Section47.6 Duality over Artinian local rings#

Tag 08YX, a lemma

Tag 08YY, a lemma

Tag 08YZ, a lemma

Tag 08Z0, a lemma

Sources

Section47.7 Injective hull of the residue field#

Tag 08Z2, a lemma

Tag 08Z3, a lemma

Tag 08Z4, a lemma

Tag 08Z5, a lemma

Tag 08Z6, a lemma

Tag 08Z7, a lemma

Tag 08Z8, a lemma

Tag 08Z9, a proposition

Tag 0EGL, a remark

Sources

Section47.8 Deriving torsion#

Tag 0A6L, a lemma

Tag 0954, a lemma

Tag 0A6M, a lemma

Tag 0A6N, an equation

Tag 0A6P, a lemma

Sources

Section47.9 Local cohomology#

Tag 0952, the section

Tag 0A6Q, an equation

Tag 0A6R, a lemma

Tag 0BJB, a lemma

Tag 0ALZ, a lemma

Tag 0A6S, a lemma

Tag 0ALY, a lemma

Tag 0BJC, a lemma

Tag 0AM0, a lemma

Tag 05EH, a lemma

Sources

Section47.10 Local cohomology for Noetherian rings#

Tag 0A6U, an equation

Tag 0955, a lemma

Tag 0956, a lemma

Tag 0957, a lemma

Sources

Section47.11 Depth#

Tag 0AVZ, a lemma

Tag 0BUV, a lemma

Section47.2 Essential surjections and injections #

Section47.3 Injective modules #

Section47.4 Projective covers #

Section47.5 Injective hulls #

Section47.6 Duality over Artinian local rings #

Section47.7 Injective hull of the residue field #

Section47.8 Deriving torsion #

Section47.9 Local cohomology #

Section47.10 Local cohomology for Noetherian rings #

Section47.11 Depth #

Section47.12 Torsion versus complete modules #

Section47.13 Trivial duality for a ring map #

Section47.14 Base change for trivial duality #

Section47.15 Dualizing complexes #

Section47.16 Dualizing complexes over local rings #

Section47.17 Dualizing complexes and dimension functions #

Section47.18 The local duality theorem #