47.20 Cohen-Macaulay rings to 47.27 Relative dualizing…
Section47.20 Cohen-Macaulay rings#
Section 47.20 of the Stacks Project, Tag 0DW4. 5 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0AWR, a lemma
Tag 0AWR in the Stacks Project.
Dualizing.depth_eq_least_nonzero_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayRings.lean, line 303.
Stacks Project, Tag 0AWR. The depth of a Noetherian local ring
Awith normalized dualizing complexω_Ais the leastδ ≥ 0withH^{-δ}(ω_A) ≠ 0.
public theorem depth_eq_least_nonzero_homology {A : Type u} [CommRing A] [IsNoetherianRing A]
[IsLocalRing A] (K : DerivedCategory (ModuleCat.{u} A))
(hK : IsNormalizedDualizingComplex.{u, 0} K) :
∃ δ : ℕ,
IsLeast
{i : ℕ |
¬ IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-(i : ℤ))).obj K)}
δ ∧
Module.depth A (IsLocalRing.maximalIdeal A) A = (δ : ℕ∞)
Tag 0AWS, a lemma
Tag 0AWS in the Stacks Project.
Dualizing.isCohenMacaulay_tfae_dualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayRings.lean, line 484. The attribute's comment: “equivalent conditions (1)--(3)”.
Stacks Project, Tag 0AWS, equivalent conditions (1)--(3). A Noetherian local ring is Cohen--Macaulay exactly when its normalized dualizing complex is concentrated in one degree, and exactly when it is its dualizing module placed in degree minus the dimension.
public theorem isCohenMacaulay_tfae_dualizingComplex {A : Type u} [CommRing A]
[IsNoetherianRing A] [IsLocalRing A] (K : DerivedCategory (ModuleCat.{u} A))
(hK : IsNormalizedDualizingComplex.{u, 0} K) :
List.TFAE
[ IsCohenMacaulayLocalRing A,
IsCohomologicallyConcentratedInOneDegree K,
Nonempty
(K ≅
(DerivedCategory.singleFunctor (ModuleCat.{u} A)
(-(localRingDimension A : ℤ))).obj (dualizingModule K)) ]
Dualizing.dualizingModule_isMaximalCohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayRings.lean, line 551. The attribute's comment: “the dualizing module is maximal Cohen--Macaulay”.
Stacks Project, Tag 0AWS, final assertion. Over a Cohen--Macaulay local ring, the dualizing module of a normalized dualizing complex is maximal Cohen--Macaulay.
public theorem dualizingModule_isMaximalCohenMacaulay {A : Type u} [CommRing A]
[IsNoetherianRing A] [IsLocalRing A] (K : DerivedCategory (ModuleCat.{u} A))
(hK : IsNormalizedDualizingComplex.{u, 0} K)
(hA : IsCohenMacaulayLocalRing A) :
Module.IsMaximalCohenMacaulay A (dualizingModule K)
Tag 0DW5, a lemma
Tag 0DW5 in the Stacks Project.
Dualizing.isCohenMacaulayRing_of_dualizingModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayFromModule.lean, line 180.
Stacks Project, Tag 0DW5. A Noetherian ring admitting a finite module whose degree-zero complex is a dualizing complex is Cohen--Macaulay.
theorem isCohenMacaulayRing_of_dualizingModule {A : Type u} [CommRing A] [IsNoetherianRing A]
(omega : ModuleCat.{max u v} A) [Module.Finite A omega]
(homega : IsDualizingComplex
((DerivedCategory.singleFunctor (ModuleCat.{max u v} A) 0).obj omega)) :
IsCohenMacaulayRing A
Tag 0EHS, a lemma
Tag 0EHS in the Stacks Project.
Dualizing.cohenMacaulayLocus_subset_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayRings.lean, line 929. The attribute's comment: “the locus is contained in the support”.
A Cohen--Macaulay localization of a module is nonzero, so its prime lies in the support.
public theorem cohenMacaulayLocus_subset_support
{A : Type u} [CommRing A]
{M : Type v} [AddCommGroup M] [Module A M] :
{p : PrimeSpectrum A |
Module.IsCohenMacaulayAtMaximalIdeal (Localization.AtPrime p.asIdeal)
(LocalizedModule.AtPrime p.asIdeal M)} ⊆ Module.support A M
Dualizing.isOpen_cohenMacaulayLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayRings.lean, line 955. The attribute's comment: “relative openness”.
Stacks Project, Tag 0EHS, openness. The Cohen--Macaulay locus of a finite module over a Noetherian ring with a dualizing complex is open in the support of the module.
public theorem isOpen_cohenMacaulayLocus
{A : Type u} [CommRing A] [IsNoetherianRing A]
{M : Type v} [AddCommGroup M] [Module A M] [Module.Finite A M]
(ω : DerivedCategory (ModuleCat.{w} A)) (hω : Dualizing.IsDualizingComplex ω) :
IsOpen {p : ↥(Module.support A M) |
Module.IsCohenMacaulayAtMaximalIdeal (Localization.AtPrime p.1.asIdeal)
(LocalizedModule.AtPrime p.1.asIdeal M)}
Dualizing.dense_cohenMacaulayLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayRings.lean, line 1010. The attribute's comment: “density”.
Stacks Project, Tag 0EHS, density. The Cohen--Macaulay locus of a finite module over a Noetherian ring is dense in the support of the module.
public theorem dense_cohenMacaulayLocus
{A : Type u} [CommRing A] [IsNoetherianRing A]
{M : Type v} [AddCommGroup M] [Module A M] [Module.Finite A M] :
Dense {p : ↥(Module.support A M) |
Module.IsCohenMacaulayAtMaximalIdeal (Localization.AtPrime p.1.asIdeal)
(LocalizedModule.AtPrime p.1.asIdeal M)}
Tag 0EHT, a lemma
Tag 0EHT in the Stacks Project.
Dualizing.isOpen_and_dense_setOf_isMaximalCohenMacaulay_of_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/CohenMacaulayLocus.lean, line 320.
Stacks Project, Tag 0EHT. For a Noetherian ring with a dualizing complex, the set of primes at which the local ring is Cohen--Macaulay is a dense open subset of the spectrum.
theorem isOpen_and_dense_setOf_isMaximalCohenMacaulay_of_isDualizingComplex
{A : Type u} [CommRing A] [IsNoetherianRing A]
(omega : DerivedCategory (ModuleCat.{max u v} A)) (homega : IsDualizingComplex omega) :
IsOpen {q : PrimeSpectrum A | Module.IsMaximalCohenMacaulay
(Localization.AtPrime q.asIdeal) (Localization.AtPrime q.asIdeal)} ∧
Dense {q : PrimeSpectrum A | Module.IsMaximalCohenMacaulay
(Localization.AtPrime q.asIdeal) (Localization.AtPrime q.asIdeal)}
Sources
Section47.21 Gorenstein rings#
Section 47.21 of the Stacks Project, Tag 0DW6. 9 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0DW7, a definition
Tag 0DW7 in the Stacks Project.
Dualizing.IsGorensteinLocalRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Gorenstein.lean, line 61. The attribute's comment: “(1)”.
A Noetherian local ring is Gorenstein when the ring as a complex concentrated in degree zero is a dualizing complex.
abbrev IsGorensteinLocalRing (A : Type u) [CommRing A] [IsNoetherianRing A]
[IsLocalRing A] : Prop
Dualizing.IsGorensteinRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Gorenstein.lean, line 69. The attribute's comment: “(2)”.
A Noetherian ring is Gorenstein when its localization at every prime ideal is a Gorenstein local ring.
abbrev IsGorensteinRing (A : Type u) [CommRing A] [IsNoetherianRing A] : Prop
Tag 0DW8, a lemma
Tag 0DW8 in the Stacks Project.
Dualizing.IsGorensteinRing.isCohenMacaulayRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinCohenMacaulay.lean, line 84.
A Gorenstein ring is Cohen--Macaulay: its localization at every prime is a Cohen--Macaulay local ring.
public theorem IsGorensteinRing.isCohenMacaulayRing (A : Type u) [CommRing A]
[IsNoetherianRing A] (hA : IsGorensteinRing A) : IsCohenMacaulayRing A
Tag 0AWX, a lemma
Tag 0AWX in the Stacks Project.
Dualizing.IsRegularLocalRing.isGorensteinLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Gorenstein.lean, line 464. The attribute's comment: “regular local rings”.
A regular local ring is Gorenstein.
public theorem IsRegularLocalRing.isGorensteinLocalRing (A : Type u) [CommRing A]
[IsRegularLocalRing A] : IsGorensteinLocalRing A
Dualizing.IsRegularRing.isGorensteinRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Gorenstein.lean, line 521. The attribute's comment: “regular rings”.
A regular ring is Gorenstein.
public theorem IsRegularRing.isGorensteinRing (A : Type u) [CommRing A]
[IsRegularRing A] : IsGorensteinRing A
Tag 0DW9, a lemma
Tag 0DW9 in the Stacks Project.
Dualizing.isGorensteinRing_iff_isInvertible_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinCriteria.lean, line 140. The attribute's comment: “(1)(a)”.
Stacks Project, Tag 0DW9 (1)(a). A Noetherian ring with a dualizing complex is Gorenstein exactly when that complex is invertible, for the canonical derived tensor product of [Stacks, Tag 0FNQ], which is available when the module universe is the ring's own.
theorem isGorensteinRing_iff_isInvertible_canonical
{A : Type u} [CommRing A] [IsNoetherianRing A]
(K : DerivedCategory (ModuleCat.{u} A))
(hK : Dualizing.IsDualizingComplex K) :
letI := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory A).choose
Dualizing.IsGorensteinRing A ↔ MonoidalCategory.IsInvertible K
Dualizing.isGorensteinRing_iff_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinCriteria.lean, line 170. The attribute's comment: “(1)(a) at a larger module universe”.
Stacks Project, Tag 0DW9 (1)(a), for a dualizing complex whose module universe is larger than the ring's. A Noetherian ring with a dualizing complex is Gorenstein if and only if that complex is invertible, the tensor product being the one transported along the coefficient equivalence; invertibility does not depend on which of the two is used.
theorem isGorensteinRing_iff_isInvertible
{A : Type u} [CommRing A] [IsNoetherianRing A]
(K : DerivedCategory (ModuleCat.{max u v} A))
(hK : Dualizing.IsDualizingComplex K) :
letI := derivedCategoryMonoidal.{u, v} A
IsGorensteinRing A ↔ MonoidalCategory.IsInvertible K
Dualizing.isOpen_gorensteinLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinOpenLocus.lean, line 196. The attribute's comment: “(1)(c)”.
Stacks Project, Tag 0DW9 (1)(c). If a Noetherian ring admits a dualizing complex, then the set of primes whose local ring is Gorenstein is open in the prime spectrum.
theorem isOpen_gorensteinLocus
{A : Type u} [CommRing A] [IsNoetherianRing A]
(K : DerivedCategory (ModuleCat.{v} A)) (hK : Dualizing.IsDualizingComplex K) :
IsOpen {p : PrimeSpectrum A |
Dualizing.IsGorensteinLocalRing (Localization.AtPrime p.asIdeal)}
Dualizing.exists_isDualizingComplex_iff_regularModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinRingDualizing.lean, line 181. The attribute's comment: “(2)”.
Stacks Project, Tag 0DW9 (2). A Noetherian Gorenstein ring has a dualizing complex if and only if the ring itself, placed in degree zero, is a dualizing complex.
theorem exists_isDualizingComplex_iff_regularModule
(A : Type u) [CommRing A] [IsNoetherianRing A]
(hA : IsGorensteinRing A) :
(∃ K : DerivedCategory (ModuleCat.{max u v} A), IsDualizingComplex K) ↔
IsDualizingComplex
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A A))
Dualizing.isGorensteinLocalRing_iff_isInvertible_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/LocalCriterionInvertible.lean, line 358. The attribute's comment: “(1)(b)”.
Stacks Project, Tag 0DW9 (1)(b). The localization of a Noetherian ring at a prime is Gorenstein if and only if the localization of a dualizing complex is invertible in the derived category of the localized ring.
theorem isGorensteinLocalRing_iff_isInvertible_localization
{A : Type u} [CommRing A] [IsNoetherianRing A]
(K : DerivedCategory (ModuleCat.{v} A))
(hK : IsDualizingComplex K)
(p : Ideal A) [p.IsPrime] :
let B := Localization.AtPrime p
letI := derivedCategoryMonoidal.{u, v} B
IsGorensteinLocalRing B ↔
MonoidalCategory.IsInvertible
((StacksDraft.PseudoCoherence.derivedExtensionScalars
(algebraMap A B)).obj K)
Tag 0BJI, a lemma
Tag 0BJI in the Stacks Project.
Dualizing.isGorensteinLocalRing_iff_residueField_ext_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Gorenstein.lean, line 866.
A Noetherian local ring is Gorenstein precisely when its Ext groups from the residue field to the regular module vanish in high degrees.
public theorem isGorensteinLocalRing_iff_residueField_ext_vanishing
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A] :
IsGorensteinLocalRing A ↔
∃ b : ℤ, ∀ i : ℤ, b < i →
Subsingleton
(DerivedCategory.Ext
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
(ModuleCat.of A (Shrink.{u} (A ⧸ IsLocalRing.maximalIdeal A))))
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A A)) i)
Tag 0BJJ, a lemma
Tag 0BJJ in the Stacks Project.
Stacks.Divisors.isGorenstein_subscheme_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/GorensteinEffectiveCartier.lean, line 70. The attribute's comment: “scheme-theoretic form: an effective Cartier divisor on a Gorenstein scheme”.
The closed subscheme cut out by an effective Cartier divisor on a Gorenstein scheme is Gorenstein.
public theorem isGorenstein_subscheme_of_isEffectiveCartierDivisor {X : Scheme.{u}}
[AlgebraicGeometry.IsGorenstein X] (D : X.IdealSheafData)
(hD : IsEffectiveCartierDivisor D) :
AlgebraicGeometry.IsGorenstein D.subscheme
Dualizing.isGorensteinLocalRing_quotient_span_singleton_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinRegularElement.lean, line 221.
Quotienting a Noetherian local ring by a nonzerodivisor in its maximal ideal preserves and reflects the Gorenstein property.
theorem isGorensteinLocalRing_quotient_span_singleton_iff
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
(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
IsGorensteinLocalRing A ↔ IsGorensteinLocalRing (A ⧸ Ideal.span {f})
Tag 0DWA, a lemma
Tag 0DWA in the Stacks Project.
Dualizing.isGorensteinRing_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinLocalCompleteIntersection.lean, line 340.
The target of a local complete intersection homomorphism from a Noetherian Gorenstein ring is Gorenstein.
public theorem isGorensteinRing_of_isLocalCompleteIntersection
{A : Type u} {B : Type v} [CommRing A] [CommRing B] [IsNoetherianRing A]
(f : A →+* B) (hf : f.IsLocalCompleteIntersection)
(hA : IsGorensteinRing A) :
letI := f.toAlgebra
letI : Algebra.FiniteType A B := hf.1
letI : IsNoetherianRing B := Algebra.FiniteType.isNoetherianRing A B
IsGorensteinRing B
Tag 0BJL, a lemma
Tag 0BJL in the Stacks Project.
Dualizing.isGorensteinLocalRing_iff_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/FlatLocalGorenstein.lean, line 567.
For a flat local homomorphism of Noetherian local rings, the target is Gorenstein if and only if the source and the closed fibre are Gorenstein.
public theorem isGorensteinLocalRing_iff_of_flat
(A : Type u) (B : Type v) [CommRing A] [CommRing B]
[IsNoetherianRing A] [IsNoetherianRing B] [IsLocalRing A] [IsLocalRing B]
[Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Flat A B] :
let I := (maximalIdeal A).map (algebraMap A B)
let _ : Nontrivial (B ⧸ I) :=
Ideal.Quotient.nontrivial_iff.mpr
(IsLocalRing.map_maximalIdeal_lt_top (algebraMap A B)).ne
let _ : IsLocalHom (Ideal.Quotient.mk I) :=
IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective
let _ : IsLocalRing (B ⧸ I) :=
IsLocalRing.of_surjective _ Ideal.Quotient.mk_surjective
IsGorensteinLocalRing B ↔
(IsGorensteinLocalRing A ∧
IsGorensteinLocalRing (B ⧸ I))
Tag 0EBT, a lemma
Tag 0EBT in the Stacks Project.
Dualizing.LocalDuality.isZero_tor_injectiveHull_residueField_of_ne_dimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/InjectiveHullTor.lean, line 378. The attribute's comment: “vanishing away from the dimension”.
For
(A, 𝔪, κ)a Noetherian local Gorenstein ring of dimensiondandEan injective hull ofκ, the groupTor_i^A(E, κ)vanishes for everyi ≠ d.
theorem isZero_tor_injectiveHull_residueField_of_ne_dimension
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
(hA : IsGorensteinLocalRing A) (d : ℕ) (hdim : ringKrullDim A = (d : WithBot ℕ∞))
(E : ModuleCat.{u} A)
(j : ModuleCat.of A (IsLocalRing.ResidueField A) ⟶ E) [Mono j]
(hj : Module.IsInjectiveHull j) (i : ℕ) (hi : i ≠ d) :
IsZero (((Tor (ModuleCat.{u} A) i).obj E).obj
(ModuleCat.of A (IsLocalRing.ResidueField A)))
Dualizing.LocalDuality.tor_injectiveHull_residueField_iso_of_eq_dimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/InjectiveHullTor.lean, line 394. The attribute's comment: “the Tor group in the dimension”.
For
(A, 𝔪, κ)a Noetherian local Gorenstein ring of dimensiondandEan injective hull ofκ, the groupTor_d^A(E, κ)is isomorphic toκ.
theorem tor_injectiveHull_residueField_iso_of_eq_dimension
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
(hA : IsGorensteinLocalRing A) (d : ℕ) (hdim : ringKrullDim A = (d : WithBot ℕ∞))
(E : ModuleCat.{u} A)
(j : ModuleCat.of A (IsLocalRing.ResidueField A) ⟶ E) [Mono j]
(hj : Module.IsInjectiveHull j) :
Nonempty ((((Tor (ModuleCat.{u} A) d).obj E).obj
(ModuleCat.of A (IsLocalRing.ResidueField A))) ≅
ModuleCat.of A (IsLocalRing.ResidueField A))
Sources
Section47.22 The ubiquity of dualizing complexes#
Section 47.22 of the Stacks Project, Tag 0DWB. 4 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0AWD, a lemma
Tag 0AWD in the Stacks Project.
Dualizing.isNormalizedDualizingComplex_extendScalars_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityDualizingComplexes/FlatBaseChange.lean, line 925.
Let
A → Bbe a flat local homomorphism of Noetherian local rings for which the maximal ideal ofAgenerates the maximal ideal ofB. Then the base change toBof a normalized dualizing complex overAis a normalized dualizing complex overB.
public theorem isNormalizedDualizingComplex_extendScalars_of_flat
{A : Type u} {B : Type w} [CommRing A] [CommRing B] [Algebra A B]
[Module.Flat A B] [IsNoetherianRing A] [IsNoetherianRing B]
[IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
(hmax : (IsLocalRing.maximalIdeal A).map (algebraMap A B) =
IsLocalRing.maximalIdeal B)
(K : DerivedCategory (ModuleCat.{max u v w} A))
(hK : IsNormalizedDualizingComplex.{u, max v w} K) :
IsNormalizedDualizingComplex.{w, max u v}
((ModuleCat.extendScalars.{u, w, max u v w}
(algebraMap A B)).mapDerivedCategory.obj K)
Tag 0DWC, a lemma
Tag 0DWC in the Stacks Project.
Dualizing.isDualizingComplex_extendScalars_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityDualizingComplexes/FlatBaseChange.lean, line 710.
Let
A → Bbe a flat map of Noetherian commutative rings. If the induced mapA/I → B/IBis bijective andIBis contained in the Jacobson radical ofB, then extending a dualizing complex fromAtoBgives a dualizing complex overB.
public theorem isDualizingComplex_extendScalars_of_flat
{A : Type u} {B : Type w} [CommRing A] [CommRing B] [Algebra A B]
[Module.Flat A B] [IsNoetherianRing A] [IsNoetherianRing B]
(I : Ideal A)
(hquotient : Function.Bijective
(Ideal.quotientMap (I.map (algebraMap A B)) (algebraMap A B)
Ideal.le_comap_map))
(hjacobson : I.map (algebraMap A B) ≤ Ring.jacobson B)
(K : DerivedCategory (ModuleCat.{v} A))
(hK : IsDualizingComplex K) :
IsDualizingComplex
((ModuleCat.extendScalars.{u, w, v} (algebraMap A B)).mapDerivedCategory.obj K)
Tag 0DWD, a lemma
Tag 0DWD in the Stacks Project.
Dualizing.isDualizingComplex_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityDualizingComplexes/AdicCompletion.lean, line 94. The attribute's comment: “ideal_adic_completion”.
Stacks Project, Tag 0DWD. The derived base change of a dualizing complex to the completion of a Noetherian ring along any ideal is a dualizing complex.
public theorem isDualizingComplex_adicCompletion
{A : Type u} [CommRing A] [IsNoetherianRing A]
(I : Ideal A) (K : DerivedCategory (ModuleCat.{v} A))
(hK : IsDualizingComplex K) :
IsDualizingComplex
(((ModuleCat.extendScalars.{u, u, v}
(algebraMap A (AdicCompletion I A))).mapDerivedCategory).obj K)
Dualizing.isDualizingComplex_completion_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityDualizingComplexes/CompletionHenselization.lean, line 87. The attribute's comment: “all three parts conjoined”.
Stacks Project, Tag 0DWD. Let
Abe a Noetherian ring, letI ⊆ Abe an ideal and letω_A^•be a dualizing complex. Then
ω_A^• ⊗_A A^his a dualizing complex on the henselization(A^h, I^h)of the pair(A, I),ω_A^• ⊗_A A^∧is a dualizing complex on theI-adic completionA^∧, and- if
Ais local, thenω_A^• ⊗_A A^h, resp.ω_A^• ⊗_A A^{sh}, is a dualizing complex on the henselization, resp. a strict henselization, ofA.The conjuncts are
Dualizing.isDualizingComplex_henselizationPair,Dualizing.isDualizingComplex_adicCompletion,Dualizing.isDualizingComplex_henselizationandDualizing.isDualizingComplex_strictHenselization, each of which carries the tag for its own part. As there, part (3) for a strict henselization is stated for a henselization ofAalong an arbitrary prescribed extensionκ(A) ⊆ Lof its residue field, which is a strict henselization exactly whenLis a separable algebraic closure ofκ(A).
theorem isDualizingComplex_completion_henselization
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(K : DerivedCategory (ModuleCat.{max u v w} A)) (hK : IsDualizingComplex K) :
(∀ (Ah : Type w) [CommRing Ah] [Algebra A Ah]
(hh : HenselianPair Ah (I.map (algebraMap A Ah)))
(hι : ∀ (B : Type (max u w)) (_ : CommRing B) (J : Ideal B),
HenselianPair B J →
∀ f : A →+* B, I ≤ J.comap f →
∃! g : Ah →+* B,
g.comp (algebraMap A Ah) = f ∧ I.map (algebraMap A Ah) ≤ J.comap g),
haveI : Module.Flat A Ah :=
(flat_henselization_and_bijective_quotientMap A I Ah hh hι).1
haveI : IsNoetherianRing Ah :=
(henselization_isNoetherian_and_completion_equiv A I Ah hh hι).2.1
IsDualizingComplex
((ModuleCat.extendScalars.{u, w, max u v w}
(algebraMap A Ah)).mapDerivedCategory.obj K)) ∧
IsDualizingComplex
((ModuleCat.extendScalars.{u, u, max u v w}
(algebraMap A (AdicCompletion I A))).mapDerivedCategory.obj K) ∧
∀ [IsLocalRing A],
(∀ (Ah : Type w) [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsHenselization A (ResidueField A) Ah],
haveI : Module.Flat A Ah := IsHenselization.flat (L := ResidueField A)
haveI : IsNoetherianRing Ah :=
isNoetherianRing_of_isHenselization (A := A) (B := Ah) (ResidueField A)
IsDualizingComplex
((ModuleCat.extendScalars.{u, w, max u v w}
(algebraMap A Ah)).mapDerivedCategory.obj K)) ∧
(∀ (L : Type t) [Field L] [Algebra (ResidueField A) L]
(Ash : Type w) [CommRing Ash] [IsLocalRing Ash] [Algebra A Ash]
[IsHenselization A L Ash],
haveI : Module.Flat A Ash := IsHenselization.flat (L := L)
haveI : IsNoetherianRing Ash :=
isNoetherianRing_of_isHenselization (A := A) (B := Ash) L
IsDualizingComplex
((ModuleCat.extendScalars.{u, w, max u v w}
(algebraMap A Ash)).mapDerivedCategory.obj K))
Dualizing.isDualizingComplex_henselizationPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityDualizingComplexes/Henselization.lean, line 96. The attribute's comment: “pair_henselization”.
Stacks Project, Tag 0DWD, part (1). The derived base change of a dualizing complex to the henselization
A^hof a pair(A, I)withANoetherian is a dualizing complex.
public theorem isDualizingComplex_henselizationPair
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(Ah : Type w) [CommRing Ah] [Algebra A Ah]
(hh : HenselianPair Ah (I.map (algebraMap A Ah)))
(hι : ∀ (B : Type (max u w)) (_ : CommRing B) (J : Ideal B),
HenselianPair B J →
∀ f : A →+* B, I ≤ J.comap f →
∃! g : Ah →+* B,
g.comp (algebraMap A Ah) = f ∧ I.map (algebraMap A Ah) ≤ J.comap g)
(K : DerivedCategory (ModuleCat.{v} A)) (hK : IsDualizingComplex K) :
haveI : Module.Flat A Ah :=
(flat_henselization_and_bijective_quotientMap A I Ah hh hι).1
haveI : IsNoetherianRing Ah :=
(henselization_isNoetherian_and_completion_equiv A I Ah hh hι).2.1
IsDualizingComplex
((ModuleCat.extendScalars.{u, w, v} (algebraMap A Ah)).mapDerivedCategory.obj K)
Dualizing.isDualizingComplex_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityDualizingComplexes/Henselization.lean, line 147. The attribute's comment: “local_henselization”.
Stacks Project, Tag 0DWD, part (3), the henselization. The derived base change of a dualizing complex to the henselization
A^hof a Noetherian local ringAis a dualizing complex.
public theorem isDualizingComplex_henselization
{A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
{Ah : Type w} [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsHenselization A (ResidueField A) Ah]
(K : DerivedCategory (ModuleCat.{v} A)) (hK : IsDualizingComplex K) :
haveI : Module.Flat A Ah := IsHenselization.flat (L := ResidueField A)
haveI : IsNoetherianRing Ah :=
isNoetherianRing_of_isHenselization (A := A) (B := Ah) (ResidueField A)
IsDualizingComplex
((ModuleCat.extendScalars.{u, w, v} (algebraMap A Ah)).mapDerivedCategory.obj K)
Dualizing.isDualizingComplex_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityDualizingComplexes/Henselization.lean, line 170. The attribute's comment: “local_strict_henselization”.
Stacks Project, Tag 0DWD, part (3), the strict henselization. The derived base change of a dualizing complex to a henselization
A^{sh}of a Noetherian local ringAalong a prescribed extensionκ ⊆ Lof its residue field — forLa separable algebraic closure ofκ, a strict henselization ofA— is a dualizing complex.
public theorem isDualizingComplex_strictHenselization
{A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
(L : Type t) [Field L] [Algebra (ResidueField A) L]
{Ash : Type w} [CommRing Ash] [IsLocalRing Ash] [Algebra A Ash]
[IsHenselization A L Ash]
(K : DerivedCategory (ModuleCat.{max u v w} A)) (hK : IsDualizingComplex K) :
haveI : Module.Flat A Ash := IsHenselization.flat (L := L)
haveI : IsNoetherianRing Ash :=
isNoetherianRing_of_isHenselization (A := A) (B := Ash) L
IsDualizingComplex
((ModuleCat.extendScalars.{u, w, max u v w}
(algebraMap A Ash)).mapDerivedCategory.obj K)
Tag 0BFR, a lemma
Tag 0BFR in the Stacks Project.
Dualizing.exists_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Ubiquity.lean, line 75. The attribute's comment: “fields”.
Stacks Project, Tag 0BFR (fields). Every field has a dualizing complex.
theorem exists_isDualizingComplex (k : Type u) [Field k] :
∃ K : DerivedCategory (ModuleCat.{u} k), IsDualizingComplex K
Dualizing.exists_isDualizingComplex_of_isDedekindDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Ubiquity.lean, line 130. The attribute's comment: “Dedekind domains”.
Stacks Project, Tag 0BFR (Dedekind domains). A Dedekind domain has a dualizing complex, namely the ring itself in degree zero.
theorem exists_isDualizingComplex_of_isDedekindDomain (A : Type u) [CommRing A]
[IsDedekindDomain A] :
∃ K : DerivedCategory (ModuleCat.{u} A), IsDualizingComplex K
Dualizing.exists_isDualizingComplex_int, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Ubiquity.lean, line 138. The attribute's comment: “the integers”.
Stacks Project, Tag 0BFR (the integers). The ring
ℤhas a dualizing complex, namelyℤ[0]: it is a Dedekind domain.
theorem exists_isDualizingComplex_int :
∃ K : DerivedCategory (ModuleCat.{0} ℤ), IsDualizingComplex K
Dualizing.exists_isDualizingComplex_of_isPrecomplete_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityCompleteLocal.lean, line 106. The attribute's comment: “Noetherian complete local rings”.
Stacks Project, Tag 0BFR, the class of Noetherian complete local rings. Such a ring has a dualizing complex; the complex produced is in fact normalized, by
Dualizing.exists_isNormalizedDualizingComplex_of_isPrecomplete_maximalIdeal.Completeness is precompleteness for the maximal ideal, as in [Stacks, Tag 07PJ]; see the implementation notes of this file.
public theorem exists_isDualizingComplex_of_isPrecomplete_maximalIdeal
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
[IsPrecomplete (IsLocalRing.maximalIdeal A) A] :
∃ K : DerivedCategory (ModuleCat.{u} A), IsDualizingComplex K
Dualizing.exists_isDualizingComplex_ubiquity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityFiveClasses.lean, line 95. The attribute's comment: “all five clauses conjoined”.
Stacks Project, Tag 0BFR. The following types of rings have a dualizing complex:
- fields,
- Noetherian complete local rings,
ℤ,- Dedekind domains,
- any ring obtained from a Noetherian ring with a dualizing complex by taking an algebra essentially of finite type, or by taking an ideal-adic completion, or by taking a henselization, or by taking a strict henselization.
The five conjuncts are
Dualizing.exists_isDualizingComplex,Dualizing.exists_isDualizingComplex_of_isPrecomplete_maximalIdeal,Dualizing.exists_isDualizingComplex_int,Dualizing.exists_isDualizingComplex_of_isDedekindDomainand, for clause (5), the five statementsDualizing.exists_isDualizingComplex_of_essentiallyOfFiniteType,Dualizing.exists_isDualizingComplex_adicCompletion,Dualizing.exists_isDualizingComplex_henselizationPair,Dualizing.exists_isDualizingComplex_henselizationandDualizing.exists_isDualizingComplex_strictHenselization; each carries the tag for its own clause. See the implementation notes of this file for the two places where the conjunction says more than the source.
theorem exists_isDualizingComplex_ubiquity :
(∀ (k : Type u) [Field k],
∃ K : DerivedCategory (ModuleCat.{u} k), IsDualizingComplex K) ∧
(∀ (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
[IsPrecomplete (IsLocalRing.maximalIdeal A) A],
∃ K : DerivedCategory (ModuleCat.{u} A), IsDualizingComplex K) ∧
(∃ K : DerivedCategory (ModuleCat.{0} ℤ), IsDualizingComplex K) ∧
(∀ (A : Type u) [CommRing A] [IsDedekindDomain A],
∃ K : DerivedCategory (ModuleCat.{u} A), IsDualizingComplex K) ∧
(∀ (A B : Type u) [CommRing A] [CommRing B] [IsNoetherianRing A] [Algebra A B],
IsEssentiallyOfFiniteType A B (algebraMap A B) →
(∃ K : DerivedCategory (ModuleCat.{u} A), IsDualizingComplex K) →
∃ (hB' : IsNoetherianRing B) (L : DerivedCategory (ModuleCat.{u} B)),
@IsDualizingComplex B _ hB' _ L) ∧
(∀ (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A),
(∃ K : DerivedCategory (ModuleCat.{u} A), IsDualizingComplex K) →
letI : IsNoetherianRing (AdicCompletion I A) := AdicCompletion.isNoetherianRing I
∃ L : DerivedCategory (ModuleCat.{u} (AdicCompletion I A)), IsDualizingComplex L) ∧
(∀ (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(Ah : Type w) [CommRing Ah] [Algebra A Ah]
(hh : HenselianPair Ah (I.map (algebraMap A Ah)))
(hι : ∀ (B : Type (max u w)) (_ : CommRing B) (J : Ideal B),
HenselianPair B J →
∀ f : A →+* B, I ≤ J.comap f →
∃! g : Ah →+* B,
g.comp (algebraMap A Ah) = f ∧ I.map (algebraMap A Ah) ≤ J.comap g),
(∃ K : DerivedCategory (ModuleCat.{v} A), IsDualizingComplex K) →
letI : IsNoetherianRing Ah :=
(henselization_isNoetherian_and_completion_equiv A I Ah hh hι).2.1
∃ L : DerivedCategory (ModuleCat.{max v w} Ah), IsDualizingComplex L) ∧
(∀ (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
(Ah : Type w) [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsLocalRing.IsHenselization A (IsLocalRing.ResidueField A) Ah],
(∃ K : DerivedCategory (ModuleCat.{v} A), IsDualizingComplex K) →
letI : IsNoetherianRing Ah :=
IsLocalRing.isNoetherianRing_of_isHenselization (A := A) (B := Ah)
(IsLocalRing.ResidueField A)
∃ L : DerivedCategory (ModuleCat.{max v w} Ah), IsDualizingComplex L) ∧
(∀ (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
(L : Type uL) [Field L] [Algebra (IsLocalRing.ResidueField A) L]
(Ash : Type w) [CommRing Ash] [IsLocalRing Ash] [Algebra A Ash]
[IsLocalRing.IsHenselization A L Ash],
(∃ K : DerivedCategory (ModuleCat.{max u v w} A), IsDualizingComplex K) →
letI : IsNoetherianRing Ash :=
IsLocalRing.isNoetherianRing_of_isHenselization (A := A) (B := Ash) L
∃ M : DerivedCategory (ModuleCat.{max u v w} Ash), IsDualizingComplex M)
Dualizing.exists_isDualizingComplex_of_essentiallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityStability.lean, line 78. The attribute's comment: “clause (5), algebras essentially of finite type”.
Stacks Project, Tag 0BFR, clause (5) for algebras essentially of finite type. If a Noetherian ring
Ahas a dualizing complex, then so does everyA-algebra essentially of finite type overA. This is the existence form of [Stacks, Tag 0A7K].
public theorem exists_isDualizingComplex_of_essentiallyOfFiniteType {A B : Type u} [CommRing A]
[CommRing B] [IsNoetherianRing A] [Algebra A B]
(hB : IsEssentiallyOfFiniteType A B (algebraMap A B))
(hA : ∃ K : DerivedCategory (ModuleCat.{u} A), IsDualizingComplex K) :
∃ (hB' : IsNoetherianRing B) (L : DerivedCategory (ModuleCat.{u} B)),
@IsDualizingComplex B _ hB' _ L
Dualizing.exists_isDualizingComplex_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityStability.lean, line 91. The attribute's comment: “clause (5), ideal-adic completions”.
Stacks Project, Tag 0BFR, clause (5) for ideal-adic completions. If a Noetherian ring
Ahas a dualizing complex, then so does itsI-adic completion for every idealI: the base change of the dualizing complex alongA → A^∧is one by [Stacks, Tag 0DWD] part (2).
public theorem exists_isDualizingComplex_adicCompletion {A : Type u} [CommRing A]
[IsNoetherianRing A] (I : Ideal A)
(hA : ∃ K : DerivedCategory (ModuleCat.{u} A), IsDualizingComplex K) :
letI : IsNoetherianRing (AdicCompletion I A) := AdicCompletion.isNoetherianRing I
∃ L : DerivedCategory (ModuleCat.{u} (AdicCompletion I A)), IsDualizingComplex L
Dualizing.exists_isDualizingComplex_henselizationPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityStability.lean, line 103. The attribute's comment: “clause (5), henselization of a pair”.
Stacks Project, Tag 0BFR, clause (5) for the henselization of a pair. If a Noetherian ring
Ahas a dualizing complex, then so does the henselizationA^hof a pair(A, I): the base change of the dualizing complex alongA → A^his one by [Stacks, Tag 0DWD] part (1).
public theorem exists_isDualizingComplex_henselizationPair
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(Ah : Type w) [CommRing Ah] [Algebra A Ah]
(hh : HenselianPair Ah (I.map (algebraMap A Ah)))
(hι : ∀ (B : Type (max u w)) (_ : CommRing B) (J : Ideal B),
HenselianPair B J →
∀ f : A →+* B, I ≤ J.comap f →
∃! g : Ah →+* B,
g.comp (algebraMap A Ah) = f ∧ I.map (algebraMap A Ah) ≤ J.comap g)
(hA : ∃ K : DerivedCategory (ModuleCat.{v} A), IsDualizingComplex K) :
letI : IsNoetherianRing Ah :=
(henselization_isNoetherian_and_completion_equiv A I Ah hh hι).2.1
∃ L : DerivedCategory (ModuleCat.{max v w} Ah), IsDualizingComplex L
Dualizing.exists_isDualizingComplex_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityStability.lean, line 123. The attribute's comment: “clause (5), henselization of a local ring”.
Stacks Project, Tag 0BFR, clause (5) for the henselization of a local ring. If a Noetherian local ring
Ahas a dualizing complex, then so does its henselization: the base change of the dualizing complex alongA → A^his one by [Stacks, Tag 0DWD] part (3).
public theorem exists_isDualizingComplex_henselization
(A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
(Ah : Type w) [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah]
[IsLocalRing.IsHenselization A (IsLocalRing.ResidueField A) Ah]
(hA : ∃ K : DerivedCategory (ModuleCat.{v} A), IsDualizingComplex K) :
letI : IsNoetherianRing Ah :=
IsLocalRing.isNoetherianRing_of_isHenselization (A := A) (B := Ah)
(IsLocalRing.ResidueField A)
∃ L : DerivedCategory (ModuleCat.{max v w} Ah), IsDualizingComplex L
Dualizing.exists_isDualizingComplex_strictHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UbiquityStability.lean, line 140. The attribute's comment: “clause (5), strict henselization of a local ring”.
Stacks Project, Tag 0BFR, clause (5) for a strict henselization of a local ring. If a Noetherian local ring
Ahas a dualizing complex, then so does any henselization ofAwith a prescribed residue field extensionL/κ(A)— in particular a strict henselization: the base change of the dualizing complex is one by [Stacks, Tag 0DWD] part (3).
public theorem exists_isDualizingComplex_strictHenselization
(A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
(L : Type uL) [Field L] [Algebra (IsLocalRing.ResidueField A) L]
(Ash : Type w) [CommRing Ash] [IsLocalRing Ash] [Algebra A Ash]
[IsLocalRing.IsHenselization A L Ash]
(hA : ∃ K : DerivedCategory (ModuleCat.{max u v w} A), IsDualizingComplex K) :
letI : IsNoetherianRing Ash :=
IsLocalRing.isNoetherianRing_of_isHenselization (A := A) (B := Ash) L
∃ M : DerivedCategory (ModuleCat.{max u v w} Ash), IsDualizingComplex M
Dualizing.exists_isDualizingComplex_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/FaltingsFiniteness.lean, line 103. The attribute's comment: “Noetherian complete local rings”.
Every Noetherian complete local ring has a dualizing complex. By the Cohen structure theorem the ring is a quotient of a power series ring in finitely many variables over a field or a Cohen ring; that power series ring is regular local, hence Gorenstein, so it is its own dualizing complex, and a dualizing complex is carried along a finite ring map by
Dualizing.isDualizingComplex_derivedHom_of_finite.
public theorem exists_isDualizingComplex_of_isAdicComplete (A : Type u) [CommRing A]
[IsNoetherianRing A] [IsLocalRing A] [IsAdicComplete (maximalIdeal A) A] :
∃ K : DerivedCategory (ModuleCat.{u} A), IsDualizingComplex K
Sources
Section47.23 Formal fibres#
Section 47.23 of the Stacks Project, Tag 0BJM. 3 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 0BJN, a lemma
Tag 0BJN in the Stacks Project.
Dualizing.isGorensteinRing_tensorProduct_of_essFiniteType_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinFieldExtension.lean, line 80. The attribute's comment: “gorenstein_field_extension”.
Stacks Project, Tag 0BJN, clause (A). Let
kbe a field,Ra Noetheriank-algebra andK/kan extension of fields which is finitely generated as a field extension. IfRis Gorenstein, thenR ⊗_k Kis Gorenstein.The extension
K/kis a localization of a global complete intersectionCoverk; base changingCalongk → Rgives a relative global complete intersectionR → R ⊗_k C, soR ⊗_k Cis Gorenstein by Tag 0DWA, andR ⊗_k Kis a localization ofR ⊗_k C.
public theorem isGorensteinRing_tensorProduct_of_essFiniteType_fieldExtension
{k : Type u} {R : Type v} {K : Type w}
[Field k] [CommRing R] [Field K] [Algebra k R] [Algebra k K]
[IsNoetherianRing R] [Algebra.EssFiniteType k K]
(hR : IsGorensteinRing R) :
letI : IsNoetherianRing (R ⊗[k] K) :=
Algebra.EssFiniteType.isNoetherianRing R (R ⊗[k] K)
IsGorensteinRing (R ⊗[k] K)
Dualizing.gorensteinProperty_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinFormalFibreAxioms.lean, line 198. The attribute's comment: “(B)”.
Stacks Project, Tag 0BJN, clause (B). The property of a map from a field to a Noetherian ring that its target is Gorenstein can be checked after localizing at every prime.
public theorem gorensteinProperty_localization (P : RingMapProperty.{u, u})
(hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
P (algebraMap k R) ↔ IsGorensteinRing R) :
∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
(∀ p : PrimeSpectrum R, P (algebraMap k (Localization.AtPrime p.asIdeal))) ↔
P (algebraMap k R)
Dualizing.gorensteinProperty_regularAscent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinFormalFibreAxioms.lean, line 211. The attribute's comment: “(C)”.
Stacks Project, Tag 0BJN, clause (C). For flat maps
A → B → Cof Noetherian rings withB → Cregular, if every fibre ofA → Bis Gorenstein then so is every fibre ofA → C.
public theorem gorensteinProperty_regularAscent (P : RingMapProperty.{u, u})
(hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
P (algebraMap k R) ↔ IsGorensteinRing R) :
∀ (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
[IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
[Module.Flat A B] [Module.Flat B C],
(∀ p : PrimeSpectrum A, P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) →
(∀ q : PrimeSpectrum B,
Algebra.IsGeometricallyRegular q.asIdeal.ResidueField (q.asIdeal.Fiber C)) →
∀ p : PrimeSpectrum A, P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))
Dualizing.gorensteinProperty_faithfullyFlatDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinFormalFibreAxioms.lean, line 268. The attribute's comment: “(D)”.
Stacks Project, Tag 0BJN, clause (D). For flat maps
A → B → Cof Noetherian rings withB → Cfaithfully flat, if every fibre ofA → Cis Gorenstein then so is every fibre ofA → B.
public theorem gorensteinProperty_faithfullyFlatDescent (P : RingMapProperty.{u, u})
(hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
P (algebraMap k R) ↔ IsGorensteinRing R) :
∀ (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
[IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
[Module.Flat A B] [Module.FaithfullyFlat B C],
(∀ p : PrimeSpectrum A, P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))) →
∀ p : PrimeSpectrum A, P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))
Dualizing.gorensteinProperty_groundFieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinFormalFibreAxioms.lean, line 295. The attribute's comment: “(E)”.
Stacks Project, Tag 0BJN, clause (E). Gorensteinness of the target is unchanged when the ground field is replaced by a separable algebraic extension of it inside the target: the condition does not refer to the ground field.
public theorem gorensteinProperty_groundFieldExtension (P : RingMapProperty.{u, u})
(hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
P (algebraMap k R) ↔ IsGorensteinRing R) :
∀ (k K R : Type u) [Field k] [Field K] [CommRing R]
[Algebra k K] [Algebra k R] [Algebra K R] [IsScalarTower k K R]
[IsNoetherianRing R] [Algebra.IsAlgebraic k K] [Algebra.IsSeparable k K],
P (algebraMap k R) → P (algebraMap K R)
Dualizing.gorensteinTarget_satisfies_formalFiberAxioms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinFormalFibreAxioms.lean, line 371. The attribute's comment: “all five clauses conjoined, stated through the RingMapProperty interface at the concrete property Dualizing.gorensteinTarget, whose value on a map is Gorensteinness of the target together with the Noetherian structure that Gorensteinness presupposes”.
Stacks Project, Tag 0BJN. Gorensteinness of the target of a map from a field to a Noetherian ring satisfies properties (A)--(E) of [Stacks, Tag 0BIR]: it is preserved by finitely generated field extension of the ground field, is detected by the localizations at the primes of the target, passes through a composition of flat maps whose second map is regular, descends through a faithfully flat second map, and is unchanged upon replacing the ground field by a separable algebraic extension of it inside the target. Gorensteinness of the target is the property
Dualizing.gorensteinTarget.
public theorem gorensteinTarget_satisfies_formalFiberAxioms :
(∀ (k K R : Type u) [Field k] [Field K] [CommRing R] [Algebra k K]
[Algebra k R] [IsNoetherianRing R] [Algebra.EssFiniteType k K],
gorensteinTarget.{u} (algebraMap k R) →
gorensteinTarget.{u}
(Algebra.TensorProduct.includeRight (R := k) (A := R) (B := K)).toRingHom) ∧
(∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
(∀ p : PrimeSpectrum R,
gorensteinTarget.{u} (algebraMap k (Localization.AtPrime p.asIdeal))) ↔
gorensteinTarget.{u} (algebraMap k R)) ∧
(∀ (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
[IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
[Module.Flat A B] [Module.Flat B C],
(∀ p : PrimeSpectrum A,
gorensteinTarget.{u} (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) →
(∀ q : PrimeSpectrum B,
Algebra.IsGeometricallyRegular q.asIdeal.ResidueField (q.asIdeal.Fiber C)) →
∀ p : PrimeSpectrum A,
gorensteinTarget.{u} (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))) ∧
(∀ (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
[IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
[Module.Flat A B] [Module.FaithfullyFlat B C],
(∀ p : PrimeSpectrum A,
gorensteinTarget.{u} (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))) →
∀ p : PrimeSpectrum A,
gorensteinTarget.{u} (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) ∧
(∀ (k K R : Type u) [Field k] [Field K] [CommRing R]
[Algebra k K] [Algebra k R] [Algebra K R] [IsScalarTower k K R]
[IsNoetherianRing R] [Algebra.IsAlgebraic k K] [Algebra.IsSeparable k K],
gorensteinTarget.{u} (algebraMap k R) → gorensteinTarget.{u} (algebraMap K R))
Declarations registered for the tag:
Dualizing.IsGorensteinRing, declared in the repository, registered withadd_to_stacksin StacksFrontier/RingTheory/Dualizing/FormalFibre.lean, line 62 (StacksFrontier): “gorenstein_local and gorenstein_ground_field: this predicate is defined by the condition at every prime localization and takes no ground field as input”.
Tag 0AWY, a lemma
Tag 0AWY in the Stacks Project.
Dualizing.isGorensteinRing_formalFibre_of_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/GorensteinFormalFibres.lean, line 287.
Stacks Project, Tag 0AWY. Every formal fibre of a Noetherian local ring admitting a dualizing complex is Gorenstein.
theorem isGorensteinRing_formalFibre_of_isDualizingComplex
(A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
(K : DerivedCategory (ModuleCat.{u} A)) (hK : IsDualizingComplex K)
(p : Ideal A) [p.IsPrime] :
∃ h : IsNoetherianRing (AdicCompletion (maximalIdeal A) A ⊗[A] p.ResidueField),
@IsGorensteinRing (AdicCompletion (maximalIdeal A) A ⊗[A] p.ResidueField)
inferInstance h
Tag 0BJP, a lemma
Tag 0BJP in the Stacks Project.
localCompleteIntersectionProperty_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/FormalFibreAxioms.lean, line 132. The attribute's comment: “(A)”.
Stacks Project, Tag 0BJP, clause (A). Being a local complete intersection is preserved by base change along a finitely generated extension of the ground field.
public theorem localCompleteIntersectionProperty_fieldExtension (P : RingMapProperty.{u, u})
(hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
P (algebraMap k R) ↔ IsLocalCompleteIntersectionRing R) :
∀ (k K R : Type u) [Field k] [Field K] [CommRing R] [Algebra k K]
[Algebra k R] [IsNoetherianRing R] [Algebra.EssFiniteType k K],
P (algebraMap k R) →
P (Algebra.TensorProduct.includeRight (R := k) (A := R) (B := K)).toRingHom
localCompleteIntersectionProperty_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/FormalFibreAxioms.lean, line 150. The attribute's comment: “(B)”.
Stacks Project, Tag 0BJP, clause (B). Being a local complete intersection can be checked after localizing at every prime.
public theorem localCompleteIntersectionProperty_localization (P : RingMapProperty.{u, u})
(hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
P (algebraMap k R) ↔ IsLocalCompleteIntersectionRing R) :
∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
(∀ p : PrimeSpectrum R, P (algebraMap k (Localization.AtPrime p.asIdeal))) ↔
P (algebraMap k R)
localCompleteIntersectionProperty_regularAscent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/FormalFibreAxioms.lean, line 172. The attribute's comment: “(C)”.
Stacks Project, Tag 0BJP, clause (C). For flat maps
A → B → Cof Noetherian rings withB → Cregular, if every fibre ofA → Bis a local complete intersection then so is every fibre ofA → C.The fibre of
A → Cat a prime𝔭is the base changeD = (κ(𝔭) ⊗_A B) ⊗_B Cof the fibre ofA → BalongB → C, which is flat, soLocalCompleteIntersection.isLocalCompleteIntersectionRing_of_flat_of_fiberreduces the claim to the fibres ofκ(𝔭) ⊗_A B → D. At a primeQofκ(𝔭) ⊗_A Blying over𝔮 ⊆ Bthat fibre isκ(Q) ⊗_{κ(𝔮)} (κ(𝔮) ⊗_B C); the extensionκ(𝔮) → κ(Q)is bijective, so the geometric regularity ofκ(𝔮) → κ(𝔮) ⊗_B Cmakes it regular, hence a local complete intersection.
public theorem localCompleteIntersectionProperty_regularAscent (P : RingMapProperty.{u, u})
(hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
P (algebraMap k R) ↔ IsLocalCompleteIntersectionRing R) :
∀ (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
[IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
[Module.Flat A B] [Module.Flat B C],
(∀ p : PrimeSpectrum A, P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) →
(∀ q : PrimeSpectrum B,
Algebra.IsGeometricallyRegular q.asIdeal.ResidueField (q.asIdeal.Fiber C)) →
∀ p : PrimeSpectrum A, P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))
localCompleteIntersectionProperty_faithfullyFlatDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/FormalFibreAxioms.lean, line 237. The attribute's comment: “(D)”.
Stacks Project, Tag 0BJP, clause (D). For flat maps
A → B → Cof Noetherian rings withB → Cfaithfully flat, if every fibre ofA → Cis a local complete intersection then so is every fibre ofA → B.The fibre of
A → Cat a prime𝔭is the base change alongB → Cof the fibre ofA → B, and that base change is faithfully flat, soLocalCompleteIntersection.isLocalCompleteIntersectionRing_of_faithfullyFlatapplies.
public theorem localCompleteIntersectionProperty_faithfullyFlatDescent
(P : RingMapProperty.{u, u})
(hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
P (algebraMap k R) ↔ IsLocalCompleteIntersectionRing R) :
∀ (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
[IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
[Module.Flat A B] [Module.FaithfullyFlat B C],
(∀ p : PrimeSpectrum A, P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))) →
∀ p : PrimeSpectrum A, P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))
localCompleteIntersectionProperty_groundFieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/FormalFibreAxioms.lean, line 265. The attribute's comment: “(E)”.
Stacks Project, Tag 0BJP, clause (E). Being a local complete intersection is unchanged when the ground field is replaced by a separable algebraic extension of it inside the target: the condition does not refer to the ground field.
public theorem localCompleteIntersectionProperty_groundFieldExtension (P : RingMapProperty.{u, u})
(hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
P (algebraMap k R) ↔ IsLocalCompleteIntersectionRing R) :
∀ (k K R : Type u) [Field k] [Field K] [CommRing R]
[Algebra k K] [Algebra k R] [Algebra K R] [IsScalarTower k K R]
[IsNoetherianRing R] [Algebra.IsAlgebraic k K] [Algebra.IsSeparable k K],
P (algebraMap k R) → P (algebraMap K R)
localCompleteIntersectionProperty_satisfies_formalFiberAxioms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCompleteIntersection/FormalFibreAxioms.lean, line 289.
Stacks 0BJP. The property of a map from a field to a Noetherian ring that its target is a local complete intersection satisfies properties (A)--(E) of [Stacks, Tag 0BIR]: it is preserved by finitely generated field extension, is local on the target, passes through a composition of flat maps when the second map is regular, descends through a faithfully flat second map, and is unchanged upon replacing the ground field by a separable algebraic extension.
The five clauses are
localCompleteIntersectionProperty_fieldExtension,localCompleteIntersectionProperty_localization,localCompleteIntersectionProperty_regularAscent,localCompleteIntersectionProperty_faithfullyFlatDescentandlocalCompleteIntersectionProperty_groundFieldExtension. The shape is that ofcohenMacaulayProperty_satisfies_formalFiberAxioms([Stacks, Tag 0BJ9]) and ofDualizing.gorensteinProperty_satisfies_formalFiberAxioms([Stacks, Tag 0BJN]).
public theorem localCompleteIntersectionProperty_satisfies_formalFiberAxioms
(P : RingMapProperty.{u, u})
(hP : ∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
P (algebraMap k R) ↔ IsLocalCompleteIntersectionRing R) :
(∀ (k K R : Type u) [Field k] [Field K] [CommRing R] [Algebra k K]
[Algebra k R] [IsNoetherianRing R] [Algebra.EssFiniteType k K],
P (algebraMap k R) →
P (Algebra.TensorProduct.includeRight (R := k) (A := R) (B := K)).toRingHom) ∧
(∀ (k R : Type u) [Field k] [CommRing R] [Algebra k R] [IsNoetherianRing R],
(∀ p : PrimeSpectrum R,
P (algebraMap k (Localization.AtPrime p.asIdeal))) ↔ P (algebraMap k R)) ∧
(∀ (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
[IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
[Module.Flat A B] [Module.Flat B C],
(∀ p : PrimeSpectrum A,
P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) →
(∀ q : PrimeSpectrum B,
Algebra.IsGeometricallyRegular q.asIdeal.ResidueField (q.asIdeal.Fiber C)) →
∀ p : PrimeSpectrum A,
P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))) ∧
(∀ (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
[Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
[IsNoetherianRing A] [IsNoetherianRing B] [IsNoetherianRing C]
[Module.Flat A B] [Module.FaithfullyFlat B C],
(∀ p : PrimeSpectrum A,
P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber C))) →
∀ p : PrimeSpectrum A,
P (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber B))) ∧
(∀ (k K R : Type u) [Field k] [Field K] [CommRing R]
[Algebra k K] [Algebra k R] [Algebra K R] [IsScalarTower k K R]
[IsNoetherianRing R] [Algebra.IsAlgebraic k K] [Algebra.IsSeparable k K],
P (algebraMap k R) → P (algebraMap K R))
Declarations registered for the tag:
LocalCompleteIntersection.isLocalCompleteIntersectionRing_iff, declared in the repository, registered withadd_to_stacksin StacksFrontier/RingTheory/Dualizing/FormalFibre.lean, line 51 (StacksFrontier): “localization”.LocalCompleteIntersection.IsLocalCompleteIntersectionRing, declared in the repository, registered withadd_to_stacksin StacksFrontier/RingTheory/Dualizing/FormalFibre.lean, line 53 (StacksFrontier): “ground_field_change”.
Sources
Section47.24 Upper shriek algebraically#
Section 47.24 of the Stacks Project, Tag 0BZI. 11 tags here are carried by 21 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BZJ, a lemma
Tag 0BZJ in the Stacks Project.
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/PolynomialEvalDualityProof.lean, line 146.
Stacks 0BZJ. The algebraic upper shriek functors attached to any two polynomial presentations of the same finite type homomorphism are naturally isomorphic, so
f^!is well defined up to isomorphism.This is
Dualizing.PolynomialPresentation.upperShriekFunctor_isowith its hypothesishBZHsupplied byDualizing.polynomialEvalDuality.
theorem nonempty_upperShriekFunctor_iso {R A : Type u} [CommRing R] [CommRing A]
(f : R →+* A) (p q : PolynomialPresentation f) :
Nonempty (p.upperShriekFunctor.{u, v} ≅ q.upperShriekFunctor.{u, v})
Tag 0BZK, a lemma
Tag 0BZK in the Stacks Project.
Dualizing.PolynomialPresentation.upperShriekFunctor_isBoundedBelow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/Bounded.lean, line 92. The attribute's comment: “(1), the statement that φ^! maps D⁺(R) into D⁺(A)”.
Algebraic upper shriek carries cohomologically bounded-below complexes to cohomologically bounded-below complexes.
theorem upperShriekFunctor_isBoundedBelow (p : PolynomialPresentation f)
{K : DerivedCategory (ModuleCat.{max v u} R)} (hK : DerivedCategoryB.IsBoundedBelow K) :
DerivedCategoryB.IsBoundedBelow (p.upperShriekFunctor.{u, v}.obj K)
Dualizing.PolynomialPresentation.upperShriekFunctor_derivedCategoryBPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/Bounded.lean, line 142. The attribute's comment: “(1), the statement that φ^! maps D⁺_Coh(R) into D⁺_Coh(A)”.
Algebraic upper shriek along a finite type homomorphism of Noetherian rings carries bounded-below complexes with coherent cohomology to bounded-below complexes with coherent cohomology.
theorem upperShriekFunctor_derivedCategoryBPlus [IsNoetherianRing R] [IsNoetherianRing A]
(p : PolynomialPresentation f) {K : DerivedCategory (ModuleCat.{max v u} R)}
(hK : DerivedCategoryB.derivedCategoryBPlus
(fun M : ModuleCat.{max v u} R ↦ Module.Finite R M) K) :
DerivedCategoryB.derivedCategoryBPlus
(fun M : ModuleCat.{max v u} A ↦ Module.Finite A M)
(p.upperShriekFunctor.{u, v}.obj K)
Dualizing.upperShriekFunctor_isBoundedAbove_of_isPerfectRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/Bounded.lean, line 295. The attribute's comment: “(2), the statement that φ^! maps D⁻(R) into D⁻(A)”.
Algebraic upper shriek along a perfect homomorphism of Noetherian rings carries cohomologically bounded-above complexes to cohomologically bounded-above complexes.
theorem upperShriekFunctor_isBoundedAbove_of_isPerfectRingMap
[IsNoetherianRing R] [IsNoetherianRing A] (p : PolynomialPresentation f)
(derivedTensor :
DerivedCategory (ModuleCat.{u} R) ⥤
DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
(comparison : ∀ N : ModuleCat.{u} R,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
(StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} R,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
(hf : letI : Algebra R A := f.toAlgebra
RingHom.IsPerfectRingMap R A derivedTensor comparison isLeftDerived)
{K : DerivedCategory (ModuleCat.{max v u} R)} (hK : DerivedCategoryB.IsBoundedAbove K) :
DerivedCategoryB.IsBoundedAbove (p.upperShriekFunctor.{u, v}.obj K)
Dualizing.upperShriekFunctor_derivedCategoryBMinus_of_isPerfectRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/Bounded.lean, line 321. The attribute's comment: “(2), the statement that φ^! maps D⁻_Coh(R) into D⁻_Coh(A)”.
Algebraic upper shriek along a perfect homomorphism of Noetherian rings carries bounded-above complexes with coherent cohomology to bounded-above complexes with coherent cohomology.
theorem upperShriekFunctor_derivedCategoryBMinus_of_isPerfectRingMap
[IsNoetherianRing R] [IsNoetherianRing A] (p : PolynomialPresentation f)
(derivedTensor :
DerivedCategory (ModuleCat.{u} R) ⥤
DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
(comparison : ∀ N : ModuleCat.{u} R,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
(StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} R,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
(hf : letI : Algebra R A := f.toAlgebra
RingHom.IsPerfectRingMap R A derivedTensor comparison isLeftDerived)
{K : DerivedCategory (ModuleCat.{max v u} R)}
(hK : DerivedCategoryB.derivedCategoryBMinus
(fun M : ModuleCat.{max v u} R ↦ Module.Finite R M) K) :
DerivedCategoryB.derivedCategoryBMinus
(fun M : ModuleCat.{max v u} A ↦ Module.Finite A M)
(p.upperShriekFunctor.{u, v}.obj K)
Dualizing.upperShriekFunctor_derivedCategoryBBounded_of_isPerfectRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/Bounded.lean, line 351. The attribute's comment: “(2), the statement that φ^! maps Dᵇ_Coh(R) into Dᵇ_Coh(A)”.
Algebraic upper shriek along a perfect homomorphism of Noetherian rings carries bounded complexes with coherent cohomology to bounded complexes with coherent cohomology.
theorem upperShriekFunctor_derivedCategoryBBounded_of_isPerfectRingMap
[IsNoetherianRing R] [IsNoetherianRing A] (p : PolynomialPresentation f)
(derivedTensor :
DerivedCategory (ModuleCat.{u} R) ⥤
DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
(comparison : ∀ N : ModuleCat.{u} R,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
(StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} R,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
(hf : letI : Algebra R A := f.toAlgebra
RingHom.IsPerfectRingMap R A derivedTensor comparison isLeftDerived)
{K : DerivedCategory (ModuleCat.{max v u} R)}
(hK : DerivedCategoryB.derivedCategoryBBounded
(fun M : ModuleCat.{max v u} R ↦ Module.Finite R M) K) :
DerivedCategoryB.derivedCategoryBBounded
(fun M : ModuleCat.{max v u} A ↦ Module.Finite A M)
(p.upperShriekFunctor.{u, v}.obj K)
Tag 0BZL, a lemma
Tag 0BZL in the Stacks Project.
Dualizing.PolynomialPresentation.upperShriekFunctor_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/Dualizing.lean, line 57.
Stacks Project, Tag 0BZL. Algebraic upper shriek along a finite type homomorphism of Noetherian rings carries a dualizing complex to a dualizing complex.
theorem upperShriekFunctor_isDualizingComplex [IsNoetherianRing R] [IsNoetherianRing A]
(p : PolynomialPresentation f) (K : DerivedCategory (ModuleCat.{u} R))
(hK : IsDualizingComplex K) :
IsDualizingComplex (p.upperShriekFunctor.{u, u}.obj K)
Tag 0BZN, a lemma
Tag 0BZN in the Stacks Project.
Dualizing.PolynomialPresentation.isIso_upperShriekFlatBaseChange_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/FlatBaseChangeIso.lean, line 228.
Let
Rbe Noetherian, letR → R'be flat, letφ : R → Abe of finite type, presented byp, and letφ' : R' → A' = R' ⊗_R Abe its base change. The flat-base-change mapφ^!(K) ⊗_A^L A' ⟶ (φ')^!(K ⊗_R^L R')ofDualizing.PolynomialPresentation.upperShriekFlatBaseChange, a natural transformation of functorsD(R) ⥤ D(A'), is an isomorphism at everyKinD⁺(R); hereφ^!is read atpand(φ')^!at its base change.
theorem PolynomialPresentation.isIso_upperShriekFlatBaseChange_app [IsNoetherianRing R]
(p : PolynomialPresentation (algebraMap R A)) (hf : (algebraMap R R').Flat)
(K : DerivedCategory (ModuleCat.{max v u} R)) (hK : DerivedCategoryB.IsBoundedBelow K) :
IsIso ((p.upperShriekFlatBaseChange.{u, v} (R' := R') hf).app K)
Tag 0BZR, a lemma
Tag 0BZR in the Stacks Project.
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_comp_iso_of_torIndependent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/TorIndependentBaseChangeIso.lean, line 385.
Stacks 0BZR. Let
R → R'be a ring homomorphism, letφ : R → Abe a perfect ring map such thatAandR'are Tor independent overR, and letφ' : R' → A' = R' ⊗_R Abe the induced map. Thenφ^!(K) ⊗_A^L A' ≅ (φ')^!(K ⊗_R^L R'), naturally inKinD(R).Here
φ^!is read at an arbitrary polynomial presentationpofφand(φ')^!at an arbitrary polynomial presentationp'ofφ', the two derived tensor products at arbitrary left-derived models of extension of scalars, perfectness ofφrelative to an arbitrary certified model of the derived tensor product onD(R), and the modules in an arbitrary universemax v u. The Noetherian hypotheses of the source are not needed.The isomorphism is the base-change map
Dualizing.PolynomialPresentation.upperShriekTorIndependentBaseChangeLargeatpand its base change, invertible byDualizing.PolynomialPresentation.isIso_upperShriekTorIndependentBaseChangeLarge, followed by the comparison of [stacks 0BZJ] between the base-changed presentation andp'.
theorem PolynomialPresentation.nonempty_upperShriekFunctor_comp_iso_of_torIndependent
(p : PolynomialPresentation (algebraMap R A))
(p' : PolynomialPresentation (algebraMap R' (TensorProduct R R' A)))
(derivedTensor :
DerivedCategory (ModuleCat.{u} R) ⥤
DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
(comparison : ∀ N : ModuleCat.{u} R,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
(StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} R,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
(hperf : RingHom.IsPerfectRingMap R A derivedTensor comparison isLeftDerived)
(hTor : TorIndependent R A R')
(bcR : DerivedCategory (ModuleCat.{max v u} R) ⥤ DerivedCategory (ModuleCat.{max v u} R'))
(cmpR : DerivedCategory.Q ⋙ bcR ⟶
(ModuleCat.extendScalars.{u, u, max v u} (algebraMap R R')).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(ldR : bcR.IsLeftDerivedFunctor cmpR
(HomologicalComplex.quasiIso (ModuleCat.{max v u} R) (ComplexShape.up ℤ)))
(bcT : DerivedCategory (ModuleCat.{max v u} A) ⥤
DerivedCategory (ModuleCat.{max v u} (TensorProduct R R' A)))
(cmpT : DerivedCategory.Q ⋙ bcT ⟶
(ModuleCat.extendScalars.{u, u, max v u}
(Algebra.TensorProduct.includeRight :
A →ₐ[R] TensorProduct R R' A).toRingHom).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(ldT : bcT.IsLeftDerivedFunctor cmpT
(HomologicalComplex.quasiIso (ModuleCat.{max v u} A) (ComplexShape.up ℤ))) :
Nonempty (p.upperShriekFunctor.{u, v} ⋙ bcT ≅ bcR ⋙ p'.upperShriekFunctor.{u, v})
Tag 0BZS, a lemma
Tag 0BZS in the Stacks Project.
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_comp_iso_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/FlatAlgebraBaseChangeIso.lean, line 257.
Stacks 0BZS. Let
Rbe a Noetherian ring andR → R'any homomorphism, letφ : R → Abe flat of finite type, presented byp, and letφ' : R' → A' = R' ⊗_R Abe the induced map, presented by anyp'. Then there is an isomorphism of functorsD(R) ⥤ D(A')φ^!(K) ⊗_A^L A' ≅ (φ')^!(K ⊗_R^L R'), natural inK, at every module universemax v u; the two derived tensor products are read at arbitrary left-derived models of extension of scalars.As in the source this is a special case of [stacks 0BZR],
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_comp_iso_of_torIndependent: over a Noetherian base a flat map of finite type is of finite presentation, hence perfect by [stacks 067J], and flatness ofAmakesAandR'Tor independent overR. The source's Noetherian hypothesis onR'is not needed.
theorem PolynomialPresentation.nonempty_upperShriekFunctor_comp_iso_of_flat
[IsNoetherianRing R]
(hflat : (algebraMap R A).Flat)
(p : PolynomialPresentation (algebraMap R A))
(p' : PolynomialPresentation (algebraMap R' (TensorProduct R R' A)))
(bcR : DerivedCategory (ModuleCat.{max v u} R) ⥤ DerivedCategory (ModuleCat.{max v u} R'))
(cmpR : DerivedCategory.Q ⋙ bcR ⟶
(ModuleCat.extendScalars.{u, u, max v u} (algebraMap R R')).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(ldR : bcR.IsLeftDerivedFunctor cmpR
(HomologicalComplex.quasiIso (ModuleCat.{max v u} R) (ComplexShape.up ℤ)))
(bcT : DerivedCategory (ModuleCat.{max v u} A) ⥤
DerivedCategory (ModuleCat.{max v u} (TensorProduct R R' A)))
(cmpT : DerivedCategory.Q ⋙ bcT ⟶
(ModuleCat.extendScalars.{u, u, max v u}
(Algebra.TensorProduct.includeRight :
A →ₐ[R] TensorProduct R R' A).toRingHom).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(ldT : bcT.IsLeftDerivedFunctor cmpT
(HomologicalComplex.quasiIso (ModuleCat.{max v u} A) (ComplexShape.up ℤ))) :
Nonempty (p.upperShriekFunctor.{u, v} ⋙ bcT ≅ bcR ⋙ p'.upperShriekFunctor.{u, v})
Tag 0BZT, a lemma
Tag 0BZT in the Stacks Project.
Dualizing.PolynomialPresentation.exists_upperShriekComp_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/CompositionFiniteType.lean, line 178.
Stacks Project, Tag 0BZT. Let
a : R →+* Aandb : A →+* Bbe homomorphisms of finite type withRNoetherian, letpbe any polynomial presentation ofa,qany polynomial presentation ofbandrany polynomial presentation ofb ∘ a. Then there is a transformation of functors
b^! ∘ a^! ⟶ (b ∘ a)^!upper shriek being read at
p, atqand atrand modules taken in any universemax v u, which is an isomorphism at every object ofD⁺(R). The Noetherian hypothesis is needed onRonly; it passes to the polynomial algebras, which is all the proof uses.It is
Dualizing.PolynomialPresentation.exists_upperShriekComp_isIso_of_isBoundedBelow, which states it at the induced presentationp.comp qof the composite, transported to an arbitraryralong the independence of the presentation, [Stacks, Tag 0BZJ],Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_iso.
theorem exists_upperShriekComp_of_finiteType [IsNoetherianRing R] {a : R →+* A} {b : A →+* B}
(p : PolynomialPresentation a)
(q : PolynomialPresentation b) (r : PolynomialPresentation (b.comp a)) :
∃ τ : p.upperShriekFunctor.{u, v} ⋙ q.upperShriekFunctor.{u, v} ⟶
r.upperShriekFunctor.{u, v},
∀ K : DerivedCategory (ModuleCat.{max v u} R), DerivedCategoryB.IsBoundedBelow K →
IsIso (τ.app K)
Tag 0C0G, a lemma
Tag 0C0G in the Stacks Project.
Dualizing.upperShriekFunctor_iso_derivedHom_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/Finite.lean, line 159. The attribute's comment: “for a finite φ of Noetherian rings, at an arbitrary polynomial presentation, at module universe equal to the ring universe”.
Stacks Project, Tag 0C0G for a finite
φ. Letφ : R →+* Abe a finite homomorphism and letpbe any polynomial presentation ofφ. Then the algebraic upper shriek functor ofpis the derived coextension-of-scalars functor
φ^! ≅ RHom_R(A, -) : D(R) ⥤ D(A)of [Stacks, Tag 0A70].
φfactors asR → C → Athrough a monic quotientC = R[T₀, …, Tₙ₋₁]/(f₀(T₀), …, fₙ₋₁(Tₙ₋₁))by a surjection (Dualizing.exists_monicIdeal_quotient_surjection). The bottom map isDualizing.nonempty_upperShriekFunctor_iso_derivedHom_monicIdeal, whose inputs — the weak regularity off₀(T₀), …, fₙ₋₁(Tₙ₋₁)and the finiteness, freeness and self-duality ofC— areMvPolynomial.isWeaklyRegular_ofFn_aeval_X_of_monicandDualizing.finite_free_selfDual_monicIdeal. The surjection is Tag 0C0G at an arbitrary presentation,Dualizing.upperShriekFunctor_iso_derivedHom_of_surjective, and the two halves are put together by [Stacks, Tag 0BZT] for a surjective second map (Dualizing.upperShriekFunctor_comp_of_surjective) and [Stacks, Tag 0C0F] (Dualizing.derivedHomCompIso).The module universe is the ring universe here, unlike in the surjective case: the computation of
ω_{C/R}and the tensor formula of [Stacks, Tag 0E4B] it is fed to are both stated at module universe equal to the ring universe.
theorem upperShriekFunctor_iso_derivedHom_of_finite (φ : R →+* A) (hφ : φ.Finite)
(p : PolynomialPresentation φ) :
Nonempty (p.upperShriekFunctor.{u, u} ≅ derivedHom.{u, u, u} φ)
Tag 0C0H, a lemma
Tag 0C0H in the Stacks Project.
Dualizing.upperShriekFunctor_iso_derivedTensorProduct_away_and_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/FlatEpimorphism.lean, line 585.
[Stacks, Tag 0C0H]. Let
Rbe a ring.
- For
f ∈ Randφ : R → R_fthe localization away fromf, the algebraic upper shriek functorφ^!, read at any polynomial presentation ofφ, is isomorphic to- ⊗_R^L R_f.- More generally, if
φ : R → R'is a ring map such thatSpec(R') → Spec(R)is an open immersion, thenφadmits a polynomial presentation, andφ^!read at any of them is isomorphic to- ⊗_R^L R'.Both hold at an arbitrary module universe.
- ⊗_R^L R'is derived tensor product overRwithR'in degree zero,Dualizing.derivedTensorProductOver;R_fis any localization ofRaway fromf. The source assumesRNoetherian, which neither clause needs. The first clause isDualizing.nonempty_upperShriekFunctor_iso_derivedTensorProduct_away, computed from [Stacks, Tag 0BZH] atR[x] → R[x]/(fx - 1)as in the source; the second isDualizing.nonempty_upperShriekFunctor_iso_derivedTensorProduct_of_isOpenImmersion.
theorem upperShriekFunctor_iso_derivedTensorProduct_away_and_of_isOpenImmersion
{R : Type u} [CommRing R] :
(∀ (f : R) (S : Type u) [CommRing S] [Algebra R S] [IsLocalization.Away f S]
(p : PolynomialPresentation (algebraMap R S)),
Nonempty (p.upperShriekFunctor.{u, v} ≅
derivedTensorProductOver.{u, v} (algebraMap R S) (Stacks0BZE.unitObject.{u, v} S))) ∧
∀ (R' : Type u) [CommRing R'] (φ : R →+* R'),
IsOpenImmersion (Spec.map (CommRingCat.ofHom φ)) →
Nonempty (PolynomialPresentation φ) ∧
∀ p : PolynomialPresentation φ, Nonempty (p.upperShriekFunctor.{u, v} ≅
derivedTensorProductOver.{u, v} φ (Stacks0BZE.unitObject.{u, v} R'))
Tag 0BZU, a lemma
Tag 0BZU in the Stacks Project.
Dualizing.PolynomialPresentation.upperShriekFunctor_iso_derivedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/DerivedTensor.lean, line 449. The attribute's comment: “at an arbitrary polynomial presentation and an arbitrary module universe”.
Stacks 0BZU. Let
φ : R → Abe a ring homomorphism, letpbe a polynomial presentation ofφwith polynomial algebraPand surjectionψ : P → A, and assumeAis a perfectP-module, which for a perfectφis Tag 068Y. Then the algebraic upper shriek functor ofpis derived tensor product overRwith the single objectφ^!(R)ofD(A):φ^!(K) = K ⊗_R^L φ^!(R), naturally inKinD(R).Perfectness of
AoverPis exactly the hypothesis of Tag 0BZE, and Tag 0BZE forψis the one external input of the argument: it identifiesRHom_P(A, -)with derived tensor product overPwithRHom_P(A, P). At the arbitrary module universemax v uof this statement that tag isDualizing.nonempty_derivedHom_iso_canonicalDerivedTensor_of_perfect_anyModuleUniverse.The rest is the cancellation of the intermediate
- ⊗_R^L Pby the iterated change of rings of Tag 08YU, the passage of the shift byninto the tensor factor through the universal property of the left derived functor, and the evaluation of that factor atRby the unitors of the tensor product of complexes.
public theorem upperShriekFunctor_iso_derivedTensorProduct
(p : PolynomialPresentation f)
(hp : letI : Module p.Poly A := Module.compHom A p.toRingHom
StacksDraft.Perfect.IsPerfectModule (R := p.Poly) A) :
letI : MonoidalCategoryStruct (ModuleCat.{max v u} R) :=
ModuleCat.liftedModuleMonoidalStruct.{u, max v u}
letI : MonoidalCategory (ModuleCat.{max v u} R) :=
ModuleCat.liftedModuleMonoidal.{u, max v u}
let R₀ := (DerivedCategory.singleFunctor (ModuleCat.{max v u} R) 0).obj
(MonoidalCategoryStruct.tensorUnit (ModuleCat.{max v u} R))
Nonempty (p.upperShriekFunctor.{u, v} ≅
derivedTensorProductOver.{u, v} f (p.upperShriekFunctor.{u, v}.obj R₀))
Dualizing.PolynomialPresentation.upperShriekFunctor_iso_derivedTensorProduct_of_isPerfectRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/DerivedTensor.lean, line 525. The attribute's comment: “for a perfect homomorphism of Noetherian rings, at an arbitrary polynomial presentation and an arbitrary module universe”.
Stacks 0BZU. Let
φ : R → Abe a perfect ring homomorphism and letpbe a polynomial presentation ofφ. Then the algebraic upper shriek functor ofpis derived tensor product overRwith the single objectφ^!(R)ofD(A):φ^!(K) = K ⊗_R^L φ^!(R), naturally inKinD(R). A flat homomorphism of finite type is perfect, so the hypothesis is not vacuous.Perfectness is taken in the form of
RingHom.IsPerfectRingMap, which is relative to a certified model of the derived tensor product onD(R); by Tag 068Y it gives perfectness ofAas a module over the polynomial algebra ofp, which is the hypothesis of Tag 0BZE. That is the only thingDualizing.PolynomialPresentation.upperShriekFunctor_iso_derivedTensorProductasks for, so this is exactly that statement with its perfectness rewritten.
public theorem upperShriekFunctor_iso_derivedTensorProduct_of_isPerfectRingMap
(p : PolynomialPresentation f)
(derivedTensor :
DerivedCategory (ModuleCat.{u} R) ⥤
DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
(comparison : ∀ N : ModuleCat.{u} R,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
(StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} R,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
(hf : letI : Algebra R A := f.toAlgebra
RingHom.IsPerfectRingMap R A derivedTensor comparison isLeftDerived) :
letI : MonoidalCategoryStruct (ModuleCat.{max v u} R) :=
ModuleCat.liftedModuleMonoidalStruct.{u, max v u}
letI : MonoidalCategory (ModuleCat.{max v u} R) :=
ModuleCat.liftedModuleMonoidal.{u, max v u}
let R₀ := (DerivedCategory.singleFunctor (ModuleCat.{max v u} R) 0).obj
(MonoidalCategoryStruct.tensorUnit (ModuleCat.{max v u} R))
Nonempty (p.upperShriekFunctor.{u, v} ≅
derivedTensorProductOver.{u, v} f (p.upperShriekFunctor.{u, v}.obj R₀))
Dualizing.PolynomialPresentation.tensorFormulaOfPerfect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/DerivedTensor.lean, line 673. The attribute's comment: “at an arbitrary polynomial presentation and an arbitrary module universe, with the tensor formula built as an isomorphism at a constructed tensor factor whose class in D(A) is the value of upper shriek at R”.
Stacks 0BZU with the isomorphism built, from perfectness alone. Let
φ : R → Abe a ring homomorphism andpa polynomial presentation ofφwhose polynomial algebra makesAa perfect module. Then the algebraic upper shriek functor ofpis derived tensor product overRwith a constructed complex whose class inD(A)isφ^!(R).This is
Dualizing.PolynomialPresentation.tensorFormulaOfDerivedHomIsoat the representative ofRHom_P(A, P)chosen byobjPreimage, with the isomorphism of Tag 0BZE there taken fromDualizing.nonempty_derivedHom_iso_canonicalDerivedTensor_of_perfect_anyModuleUniverse. That tag is available as a proposition rather than as data, because passing between two representatives of one object ofD(A)goes through a fraction, so the isomorphism is chosen; everything after the choice is a construction.
public def tensorFormulaOfPerfect
(p : PolynomialPresentation f)
(hp : letI : Module p.Poly A := Module.compHom A p.toRingHom
StacksDraft.Perfect.IsPerfectModule (R := p.Poly) A) :
TensorFormula.{u, v} p
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_iso_derivedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/DerivedTensorUnconditional.lean, line 134. The attribute's comment: “at an arbitrary polynomial presentation, at module universe equal to the ring universe; the same statement at an arbitrary module universe is Dualizing.PolynomialPresentation.upperShriekFunctor_iso_derivedTensorProduct”.
Stacks 0BZU, with no carried hypothesis. Let
φ : R → Abe a ring homomorphism andpa polynomial presentation of it whose polynomial algebra makesAa perfect module. Then the algebraic upper shriek functor ofpis derived tensor product overRwith the single objectφ^!(R)ofD(A).This is
Dualizing.PolynomialPresentation.upperShriekFunctor_iso_derivedTensorProductread at module universe equal to the ring universe, which is the generality the rest of this module works in; that statement holds at any module universe.
theorem nonempty_upperShriekFunctor_iso_derivedTensorProduct
(p : PolynomialPresentation f)
(hp : letI : Module p.Poly A := Module.compHom A p.toRingHom
StacksDraft.Perfect.IsPerfectModule.{u, u, u + 1} (R := p.Poly) A) :
letI : MonoidalCategoryStruct (ModuleCat.{u} R) :=
ModuleCat.liftedModuleMonoidalStruct.{u, u}
letI : MonoidalCategory (ModuleCat.{u} R) :=
ModuleCat.liftedModuleMonoidal.{u, u}
let R₀ := (DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
(MonoidalCategoryStruct.tensorUnit (ModuleCat.{u} R))
Nonempty (p.upperShriekFunctor.{u, u} ≅
derivedTensorProductOver.{u, u} f (p.upperShriekFunctor.{u, u}.obj R₀))
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_iso_derivedTensorProduct_of_isPerfectRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/DerivedTensorUnconditional.lean, line 165. The attribute's comment: “for a perfect homomorphism of Noetherian rings, at an arbitrary polynomial presentation, at module universe equal to the ring universe; the same statement at an arbitrary module universe is Dualizing.PolynomialPresentation.upperShriekFunctor_iso_derivedTensorProduct_of_isPerfectRingMap”.
Stacks 0BZU for a perfect homomorphism, with no carried hypothesis. Let
φ : R → Abe a perfect ring homomorphism andpa polynomial presentation of it. Then the algebraic upper shriek functor ofpis derived tensor product overRwith the single objectφ^!(R)ofD(A).This is the hypothesis shape of Stacks 0BZU itself: perfectness of
φ, in the form ofRingHom.IsPerfectRingMaprelative to a model of the derived tensor product onD(R), rather than perfectness ofAover the polynomial algebra ofp. Tag 068Y passes between the two, asRingHom.isPerfectModule_of_isPerfectRingMap, which is what feedsDualizing.PolynomialPresentation.nonempty_upperShriekFunctor_iso_derivedTensorProducthere. So this isDualizing.PolynomialPresentation.upperShriekFunctor_iso_derivedTensorProduct_of_isPerfectRingMapread at module universe equal to the ring universe.
theorem nonempty_upperShriekFunctor_iso_derivedTensorProduct_of_isPerfectRingMap
(p : PolynomialPresentation f)
(derivedTensor :
DerivedCategory (ModuleCat.{u} R) ⥤
DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
(comparison : ∀ N : ModuleCat.{u} R,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
(StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} R,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
(hf : letI : Algebra R A := f.toAlgebra
RingHom.IsPerfectRingMap R A derivedTensor comparison isLeftDerived) :
letI : MonoidalCategoryStruct (ModuleCat.{u} R) :=
ModuleCat.liftedModuleMonoidalStruct.{u, u}
letI : MonoidalCategory (ModuleCat.{u} R) :=
ModuleCat.liftedModuleMonoidal.{u, u}
let R₀ := (DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
(MonoidalCategoryStruct.tensorUnit (ModuleCat.{u} R))
Nonempty (p.upperShriekFunctor.{u, u} ≅
derivedTensorProductOver.{u, u} f (p.upperShriekFunctor.{u, u}.obj R₀))
Dualizing.PolynomialPresentation.tensorFormula, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/DerivedTensorUnconditional.lean, line 212. The attribute's comment: “at an arbitrary polynomial presentation, at module universe equal to the ring universe, with no carried hypothesis, and with the isomorphism built rather than shown to exist — at the constructed tensor factor of Tag 08YU, whose class in D(A) is the value of upper shriek at R rather than a prescribed representative of it”.
Stacks 0BZU with the isomorphism built, and no carried hypothesis. Same hypotheses as
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_iso_derivedTensorProduct, but the conclusion is data: a complex ofA-modules whose class inD(A)isφ^!(R)— byDualizing.PolynomialPresentation.TensorFormula.classIso— together with the isomorphism of the algebraic upper shriek functor ofpwith derived tensor product overRwith that complex.The two inputs are
Dualizing.derivedHomIsoCanonicalDerivedTensorOfPerfect, which is Tag 0BZE in the change-of-rings shape with the isomorphism built at the canonical Tate tensor factor, andDualizing.PolynomialPresentation.tensorFormulaOfDerivedHomIso, which turns such an isomorphism into the tensor formula. Neither extracts a witness from an existential.
def tensorFormula (p : PolynomialPresentation f)
(hp : letI : Module p.Poly A := Module.compHom A p.toRingHom
StacksDraft.Perfect.IsPerfectModule.{u, u, u + 1} (R := p.Poly) A) :
TensorFormula.{u, u} p
Tag 0E9L, a lemma
Tag 0E9L in the Stacks Project.
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_natIso_dualizingDerivedHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/FiniteTypeDualityFormula.lean, line 193. The attribute's comment: “in general: an arbitrary finite-type φ of Noetherian rings at an arbitrary polynomial presentation, as an isomorphism of functors on D_Coh(A), with no surjectivity and no projection-formula keystone”.
[Stacks, Tag 0E9L] for an arbitrary finite-type
φ, as an isomorphism of functors onD_Coh(A). Letφ : A →+* Bbe a homomorphism of finite type withANoetherian, letpbe any polynomial presentation ofφand letωbe a dualizing complex forA. Writeφ^!for the algebraic upper shriek functor ofp, putω_B = φ^!(ω),D_A(-) = RHom_A(-, ω)andD_B(-) = RHom_B(-, ω_B). Then
φ^!(K) ≅ D_B(D_A(K) ⊗_A^L B)as an isomorphism of functors on
D_Coh(A).No surjectivity, and no projection-formula keystone. The surjective case is
Dualizing.upperShriekFunctor_natIso_dualizingDerivedHom_of_surjective; the passage to a general finite-typeφis made here by reading that statement's engine — the tag for derived coextension of scalars along an arbitrary ring homomorphism — at the objectK ⊗_A^L Pover the polynomial algebra of the presentation, and feeding it the flat base change of derived Hom alongA → P. That base change is the unconditional [Stacks, Tag 0A6A], not the Tor-independent square of [Stacks, Tag 0BZM]; so unlike [Stacks, Tag 0BZT] in general (Dualizing.PolynomialPresentation.exists_upperShriekComp_of_finiteType) this carries noDualizing.KFlatAlgebraActionEq. See the module documentation for the chain.The derived base change
- ⊗_A^L Bis the chosen model; for an arbitrary model seeDualizing.PolynomialPresentation.nonempty_upperShriekFunctor_natIso_dualizingDerivedHom_model. The statement is aNonemptybecause the adjunction of [Stacks, Tag 0A70] that the engine consumes is itself only known to exist.
theorem nonempty_upperShriekFunctor_natIso_dualizingDerivedHom [IsNoetherianRing A]
(p : PolynomialPresentation φ) (ω : DerivedCategory (ModuleCat.{u} A))
(hω : IsDualizingComplex ω) :
Nonempty ((hasFiniteCohomology.{u, u} A).ι ⋙ p.upperShriekFunctor.{u, u} ≅
(hasFiniteCohomology.{u, u} A).ι ⋙ dualizingBaseChangeFunctor.{u, u} φ
(totalDerivedExtension φ) ω (p.upperShriekFunctor.{u, u}.obj ω))
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_natIso_dualizingDerivedHom_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/FiniteTypeDualityFormula.lean, line 254. The attribute's comment: “in general, at an arbitrary model of derived base change as well as an arbitrary polynomial presentation”.
[Stacks, Tag 0E9L] in general, at an arbitrary model of derived base change. This is
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_natIso_dualizingDerivedHomwith the chosen model of- ⊗_A^L Breplaced by an arbitrary one. Two models of derived extension of scalars alongφare isomorphic by uniqueness of the total left derived functor,CategoryTheory.Functor.leftDerivedNatIso, andDualizing.PolynomialPresentation.dualizingBaseChangeFunctorIsoOfModelIsocarries that isomorphism into the right-hand side of the tag.
theorem nonempty_upperShriekFunctor_natIso_dualizingDerivedHom_model [IsNoetherianRing A]
(p : PolynomialPresentation φ)
(E : CochainComplex.DerivedExtensionScalars.TotalDerivedExtensionScalars.{u, u, u,
u + 1, u + 1} φ)
(ω : DerivedCategory (ModuleCat.{u} A)) (hω : IsDualizingComplex ω) :
Nonempty ((hasFiniteCohomology.{u, u} A).ι ⋙ p.upperShriekFunctor.{u, u} ≅
(hasFiniteCohomology.{u, u} A).ι ⋙ dualizingBaseChangeFunctor.{u, u} φ E ω
(p.upperShriekFunctor.{u, u}.obj ω))
Sources
Section47.25 Relative dualizing complexes in the Noetherian case#
Section 47.25 of the Stacks Project, Tag 0E9M. 9 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BZV, a lemma
Tag 0BZV in the Stacks Project.
Dualizing.relativeDualizingComplexBaseChange_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingBaseChange.lean, line 227. The attribute's comment: “case (3), R → A perfect and A, R' Tor independent”.
Let
RandR'be Noetherian rings, letφ : R → Abe a perfect homomorphism presented byp, and letAandR'be Tor independent overR. Then the relative dualizing complex commutes with base change toR': there is an isomorphismω^•_{A/R} ⊗_A^L A' ≅ ω^•_{A'/R'}inD(A'), whereA' = R' ⊗_R Aand the derived tensor product is read at the given left-derived model of extension of scalars.Perfectness of
φisRingHom.IsPerfectRingMapat the given certified derived tensor product.
theorem relativeDualizingComplexBaseChange_of_isPerfect
[IsNoetherianRing R] [IsNoetherianRing R']
(p : PolynomialPresentation (algebraMap R A))
(derivedTensor :
DerivedCategory (ModuleCat.{u} R) ⥤
DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
(comparison : ∀ N : ModuleCat.{u} R,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
(StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} R,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
(hperf : RingHom.IsPerfectRingMap R A derivedTensor comparison isLeftDerived)
(hTor : TorIndependent R A R')
(bcT : DerivedCategory (ModuleCat.{u} A) ⥤
DerivedCategory (ModuleCat.{u} (TensorProduct R R' A)))
(cmpT : DerivedCategory.Q ⋙ bcT ⟶
(ModuleCat.extendScalars.{u, u, u}
(Algebra.TensorProduct.includeRight :
A →ₐ[R] TensorProduct R R' A).toRingHom).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(ldT : bcT.IsLeftDerivedFunctor cmpT
(HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ))) :
Nonempty (bcT.obj (p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R))) ≅
(p.baseChange (R' := R')).upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R') 0).obj (ModuleCat.of R' R')))
Dualizing.relativeDualizingComplexBaseChange_of_flatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingBaseChange.lean, line 286. The attribute's comment: “case (1), R → R' flat”.
Let
R → R'be a flat homomorphism of Noetherian rings and letφ : R → Abe of finite type, presented byp. Then the relative dualizing complex commutes with base change toR': there is an isomorphismω^•_{A/R} ⊗_A^L A' ≅ ω^•_{A'/R'}inD(A'), whereA' = R' ⊗_R Aand the derived tensor product is read at the given left-derived model of extension of scalars.
theorem relativeDualizingComplexBaseChange_of_flatBaseChange
[IsNoetherianRing R] [IsNoetherianRing R']
(p : PolynomialPresentation (algebraMap R A))
(hflat : (algebraMap R R').Flat)
(bcT : DerivedCategory (ModuleCat.{u} A) ⥤
DerivedCategory (ModuleCat.{u} (TensorProduct R R' A)))
(cmpT : DerivedCategory.Q ⋙ bcT ⟶
(ModuleCat.extendScalars.{u, u, u}
(Algebra.TensorProduct.includeRight :
A →ₐ[R] TensorProduct R R' A).toRingHom).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(ldT : bcT.IsLeftDerivedFunctor cmpT
(HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ))) :
Nonempty (bcT.obj (p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R))) ≅
(p.baseChange (R' := R')).upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R') 0).obj (ModuleCat.of R' R')))
Dualizing.relativeDualizingComplexBaseChange_of_flatAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingBaseChange.lean, line 333. The attribute's comment: “case (2), R → A flat”.
Let
RandR'be Noetherian rings and letφ : R → Abe flat and of finite type, presented byp. Then the relative dualizing complex commutes with base change toR': there is an isomorphismω^•_{A/R} ⊗_A^L A' ≅ ω^•_{A'/R'}inD(A'), whereA' = R' ⊗_R Aand the derived tensor product is read at the given left-derived model of extension of scalars.
theorem relativeDualizingComplexBaseChange_of_flatAlgebra
[IsNoetherianRing R] [IsNoetherianRing R']
(p : PolynomialPresentation (algebraMap R A))
(hflat : (algebraMap R A).Flat)
(bcT : DerivedCategory (ModuleCat.{u} A) ⥤
DerivedCategory (ModuleCat.{u} (TensorProduct R R' A)))
(cmpT : DerivedCategory.Q ⋙ bcT ⟶
(ModuleCat.extendScalars.{u, u, u}
(Algebra.TensorProduct.includeRight :
A →ₐ[R] TensorProduct R R' A).toRingHom).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(ldT : bcT.IsLeftDerivedFunctor cmpT
(HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ))) :
Nonempty (bcT.obj (p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R))) ≅
(p.baseChange (R' := R')).upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R') 0).obj (ModuleCat.of R' R')))
Tag 0BZW, a lemma
Tag 0BZW in the Stacks Project.
Dualizing.upperShriekFunctor_unit_derivedCategoryBBounded_of_isPerfectRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizing.lean, line 151. The attribute's comment: “(1)(a)”. References: SGA 5 III (6.2), “partial”.
Let
φ : R →+* Abe a perfect homomorphism of finite type of Noetherian rings. Then the relative dualizing complexω_{A/R} = φ^!(R)lies inDᵇ_Coh(A).Perfectness of
φisRingHom.IsPerfectRingMap, stated with a derived tensor product taken as input: the bifunctorderivedTensor, its comparisoncomparisonwith termwise tensoring, and the certificateisLeftDerivedthat each- ⊗ᴸ N[0]is a total left derived functor.
theorem upperShriekFunctor_unit_derivedCategoryBBounded_of_isPerfectRingMap
[IsNoetherianRing R] [IsNoetherianRing A] (p : PolynomialPresentation f)
(derivedTensor :
DerivedCategory (ModuleCat.{u} R) ⥤
DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
(comparison : ∀ N : ModuleCat.{u} R,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
(StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} R,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
(hf : letI : Algebra R A := f.toAlgebra
RingHom.IsPerfectRingMap R A derivedTensor comparison isLeftDerived) :
DerivedCategoryB.derivedCategoryBBounded
(fun N : ModuleCat.{max v u} A ↦ Module.Finite A N)
(p.upperShriekFunctor.{u, v}.obj
((DerivedCategory.singleFunctor (ModuleCat.{max v u} R) 0).obj
(ModuleCat.of R (ULift.{v} R))))
Dualizing.PolynomialPresentation.relativeDualizingComplex_hasFiniteTorDimension_of_isPerfectRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingFiniteTorDimension.lean, line 467. The attribute's comment: “(1)(b)”. References: SGA 5 III (6.2), “partial”.
[Stacks, Tag 0BZW] (1)(b). Let
φ : R →+* Abe a perfect homomorphism of finite type of Noetherian rings, presented byp. Then the relative dualizing complexω^•_{A/R} = φ^!(R)has finite Tor dimension as a complex ofR-modules.Perfectness of
φis perfectness ofAover the polynomial algebra of any presentation ([stacks 068Y],RingHom.isPerfectModule_of_isPerfectRingMap), and that is the hypothesis ofrelativeDualizingComplex_hasFiniteTorDimension_of_isPerfectModule.Perfectness of
φisRingHom.IsPerfectRingMap, which carries the derived tensor product it is stated with, as in [stacks 0BZK]; finite Tor dimension overRis read at the canonical certified derived tensor product, which is the one the definition of relative perfection ([stacks 0DHS]) is written with.
theorem relativeDualizingComplex_hasFiniteTorDimension_of_isPerfectRingMap
(p : PolynomialPresentation (algebraMap R A))
(derivedTensor :
DerivedCategory (ModuleCat.{u} R) ⥤
DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
(comparison : ∀ N : ModuleCat.{u} R,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
(StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} R,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
(hf : RingHom.IsPerfectRingMap R A derivedTensor comparison isLeftDerived) :
StacksDraft.TorAmplitude.HasFiniteTorDimension
(CochainComplex.DerivedTensor.canonicalDerivedTensorProduct R).tensor
(StacksDraft.TorAmplitude.canonicalTensorComparison R)
(StacksDraft.TorAmplitude.canonicalTensorIsLeftDerived R)
((ModuleCat.restrictScalars (algebraMap R A)).mapDerivedCategory.obj
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R))))
Dualizing.PolynomialPresentation.relativeDualizingComplex_isRelativelyPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingFiniteTorDimension.lean, line 542. The attribute's comment: “(2)(a)”.
[Stacks, Tag 0BZW] (2)(a). Let
φ : R → Abe a flat homomorphism of finite type of Noetherian rings, presented byp. Thenω^•_{A/R} = φ^!(R)is perfect relative toRin the sense of [stacks 0DHS].Nothing is carried. Relative perfection is by definition the conjunction of pseudo-coherence over
Aand finite Tor dimension overR: the first is [stacks 0BZW] (1)(a), available asDualizing.PolynomialPresentation.relativeDualizingComplex_isPseudoCoherent_of_flat, and the second is [stacks 0BZW] (1)(b), which isDualizing.PolynomialPresentation.relativeDualizingComplex_hasFiniteTorDimension_of_flatabove.This is the same statement as
Dualizing.PolynomialPresentation.relativeDualizingComplex_isRelativelyPerfect_of_flatofStacksFrontier.RingTheory.Dualizing.UpperShriek.RelativePerfection, which reaches it by the fibrewise criterion [stacks 0GHJ] and therefore carries the open projection-formula compatibilityDualizing.PolynomialPresentation.ProjectionCompatibilityat every residue field ofR. Here nothing is carried; both are kept, the two routes being independent.
theorem relativeDualizingComplex_isRelativelyPerfect
[IsNoetherianRing R] [IsNoetherianRing A]
(p : PolynomialPresentation (algebraMap R A)) (hflat : (algebraMap R A).Flat) :
letI : Module.Flat R A := RingHom.flat_algebraMap_iff.mp hflat
letI : Algebra.FinitePresentation R A :=
Algebra.FinitePresentation.of_finiteType.mp (RingHom.finiteType_algebraMap.mp p.finiteType)
PseudoCoherence.IsRelativelyPerfect.{u, u, u}
(CochainComplex.DerivedTensor.canonicalDerivedTensorProduct R).tensor
(StacksDraft.TorAmplitude.canonicalTensorComparison R)
(StacksDraft.TorAmplitude.canonicalTensorIsLeftDerived R)
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R)))
Dualizing.upperShriekFunctor_unit_isIso_derivedHomothety_of_isPerfectRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingProperties.lean, line 72. The attribute's comment: “(1)(c)”.
Stacks Project, Tag 0BZW (1)(c). Let
φ : R →+* Abe a perfect homomorphism of finite type of Noetherian rings, presented by an arbitrary polynomial presentationp. Then the canonical mapA ⟶ RHom_A(ω_{A/R}, ω_{A/R})of [Stacks, Tag 0A7C] — the derived homothety of the adjunction of [Stacks, Tag 0A63] atω_{A/R} = φ^!(R)— is an isomorphism.The source's proof: a perfect ring map is perfect through the polynomial algebra
Pof every presentation ([Stacks, Tag 068Y],RingHom.isPerfectModule_of_isPerfectRingMap), perfectness survives the universe lift to the module universe in which upper shriek is formed (StacksDraft.Perfect.isPerfectModule_ulift), and thenDualizing.upperShriekFunctor_unit_isIso_derivedHomothety_of_isPerfectModulereadsRHom_A(ω_{A/R}, ω_{A/R})inD(P)as the double dual ofAand concludes by [Stacks, Tag 07VI].Perfectness of
φisRingHom.IsPerfectRingMap, which carries the derived tensor product it is stated with, as in (1)(a). Noetherianity ofAis not needed by the proof.
theorem upperShriekFunctor_unit_isIso_derivedHomothety_of_isPerfectRingMap [IsNoetherianRing R]
(p : PolynomialPresentation f)
(derivedTensor :
DerivedCategory (ModuleCat.{u} R) ⥤
DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
(comparison : ∀ N : ModuleCat.{u} R,
DerivedCategory.Q ⋙
derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
(StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
(isLeftDerived : ∀ N : ModuleCat.{u} R,
(derivedTensor.flip.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
(comparison N)
(HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
(hf : letI : Algebra R A := f.toAlgebra
RingHom.IsPerfectRingMap R A derivedTensor comparison isLeftDerived) :
IsIso (derivedHomothety (StacksDraft.DerivedHom.derivedHomAdjunctionOverRing.{u, v} A)
(StacksDraft.DerivedHom.derivedTensorUnit.{u, v} A)
(StacksDraft.DerivedHom.derivedTensorUnitLeft.{u, v} A)
(p.upperShriekFunctor.{u, v}.obj
((DerivedCategory.singleFunctor (ModuleCat.{max v u} R) 0).obj
(ModuleCat.of R (ULift.{v} R)))))
Dualizing.isDualizingComplex_derivedExtensionScalars_relativeDualizing_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingProperties.lean, line 138. The attribute's comment: “(2)(b)”.
Stacks Project, Tag 0BZW (2)(b). Let
φ : R → Abe a flat homomorphism of finite type of Noetherian rings, presented by an arbitrary polynomial presentationp, and letR → kbe a homomorphism to a field. Then the derived base change ofω^•_{A/R} = φ^!(R)along the coprojectionA → k ⊗_R Ais a dualizing complex for the fibre ringk ⊗_R A.The source's proof: base change for the relative dualizing complex, [Stacks, Tag 0BZV] case (2) at
R' = k, identifies the derived base change withω^•_{A'/k}forA' = k ⊗_R A, which is a dualizing complex by [Stacks, Tag 0BZL]; this isDualizing.isDualizingComplex_derivedExtensionScalars_upperShriekFunctor_unit_of_field.
theorem isDualizingComplex_derivedExtensionScalars_relativeDualizing_of_flat
{R A : Type u} [CommRing R] [CommRing A] [IsNoetherianRing R] [IsNoetherianRing A]
[Algebra R A] (k : Type u) [Field k] [Algebra R k]
(p : PolynomialPresentation (algebraMap R A)) (hflat : (algebraMap R A).Flat) :
letI : IsNoetherianRing (TensorProduct R k A) := isNoetherianRing_baseChange k p
IsDualizingComplex
((CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, u}
(Algebra.TensorProduct.includeRight :
A →ₐ[R] TensorProduct R k A).toRingHom).functor.obj
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R))))
Tag 0E0P, a lemma
Tag 0E0P in the Stacks Project.
Dualizing.isDualizingComplex_derivedExtensionScalars_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingComplexes/FieldExtensionBaseChange.lean, line 123.
Stacks Project, Tag 0E0P. Let
k ⊆ Kbe an extension of fields and letAbe ak-algebra of finite type. The derived base change of a dualizing complex forAalongA → A_K = K ⊗_k Ais a dualizing complex forA_K.
theorem isDualizingComplex_derivedExtensionScalars_fieldExtension
{ω : DerivedCategory (ModuleCat.{u} A)}
(hω : letI : IsNoetherianRing A := Algebra.FiniteType.isNoetherianRing k A
IsDualizingComplex ω) :
letI : IsNoetherianRing (TensorProduct k K A) :=
Algebra.FiniteType.isNoetherianRing K (TensorProduct k K A)
IsDualizingComplex
((totalDerivedExtensionScalars.{u, u, u}
(Algebra.TensorProduct.includeRight :
A →ₐ[k] TensorProduct k K A).toRingHom).functor.obj ω)
Tag 0E4B, a lemma
Tag 0E4B in the Stacks Project.
Dualizing.PolynomialPresentation.isInvertible_upperShriekFunctor_obj_unit_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/CompleteIntersection.lean, line 475.
Stacks 0E4B, invertibility of the relative dualizing complex of a local complete intersection homomorphism. Let
φ : R → Abe a local complete intersection homomorphism withRNoetherian and letpbe any polynomial presentation ofφ. Thenω_{A/R} = φ^!(R)is an invertible object ofD(A).The kernel of one presentation is Koszul-regular by the definition of a local complete intersection, hence the kernel of every presentation is, by [Stacks, Tag 07CZ]; so
isInvertible_upperShriekFunctor_obj_unit_of_isKoszulRegularapplies top.
theorem isInvertible_upperShriekFunctor_obj_unit_of_isLocalCompleteIntersection
[IsNoetherianRing R] (p : PolynomialPresentation f)
(hf : f.IsLocalCompleteIntersection) :
letI : MonoidalCategoryStruct (ModuleCat.{u} R) :=
ModuleCat.liftedModuleMonoidalStruct.{u, u}
letI : MonoidalCategory (ModuleCat.{u} R) := ModuleCat.liftedModuleMonoidal.{u, u}
let R₀ := (DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
(MonoidalCategoryStruct.tensorUnit (ModuleCat.{u} R))
letI := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory A).choose
MonoidalCategory.IsInvertible (p.upperShriekFunctor.{u, u}.obj R₀)
Dualizing.PolynomialPresentation.upperShriekFunctor_iso_derivedTensorProduct_of_lci, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/CompleteIntersection.lean, line 504. The attribute's comment: “the formula φ^!(K) = K ⊗_R^L ω_{A/R}, at an arbitrary polynomial presentation and an arbitrary module universe”.
Stacks 0E4B, the formula for upper shriek. Let
φ : R → Abe a local complete intersection homomorphism and letpbe a polynomial presentation ofφ. Thenφ^!(K) = K ⊗_R^L ω_{A/R}withω_{A/R} = φ^!(R), naturally inKinD(R).A local complete intersection homomorphism is perfect by [Stacks, Tag 07EN], which is what the tensor formula of [Stacks, Tag 0BZU] asks for, and that formula asks for nothing else: the conclusion of [Stacks, Tag 0BZE] for the surjection of the presentation holds at the arbitrary module universe
max v uof this statement, byDualizing.nonempty_derivedHom_iso_canonicalDerivedTensor_of_perfect_anyModuleUniverse.
theorem upperShriekFunctor_iso_derivedTensorProduct_of_lci
(p : PolynomialPresentation f)
(hf : f.IsLocalCompleteIntersection) :
letI : MonoidalCategoryStruct (ModuleCat.{max v u} R) :=
ModuleCat.liftedModuleMonoidalStruct.{u, max v u}
letI : MonoidalCategory (ModuleCat.{max v u} R) :=
ModuleCat.liftedModuleMonoidal.{u, max v u}
let R₀ := (DerivedCategory.singleFunctor (ModuleCat.{max v u} R) 0).obj
(MonoidalCategoryStruct.tensorUnit (ModuleCat.{max v u} R))
Nonempty (p.upperShriekFunctor.{u, v} ≅
derivedTensorProductOver.{u, v} f (p.upperShriekFunctor.{u, v}.obj R₀))
Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_iso_derivedTensorProduct_of_lci, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/DerivedTensorUnconditional.lean, line 229. The attribute's comment: “the formula φ^!(K) = K ⊗_R^L ω_{A/R}, at an arbitrary polynomial presentation, at module universe equal to the ring universe; the same statement at an arbitrary module universe is Dualizing.PolynomialPresentation.upperShriekFunctor_iso_derivedTensorProduct_of_lci”.
Stacks 0E4B, with no carried hypothesis. Let
φ : R → Abe a local complete intersection homomorphism andpa polynomial presentation of it. Thenφ^!(K) = K ⊗_R^L ω_{A/R}withω_{A/R} = φ^!(R), naturally inK.This is
Dualizing.PolynomialPresentation.upperShriekFunctor_iso_derivedTensorProduct_of_lciread at module universe equal to the ring universe; that statement holds at any module universe.
theorem nonempty_upperShriekFunctor_iso_derivedTensorProduct_of_lci
(p : PolynomialPresentation f)
(hf : f.IsLocalCompleteIntersection) :
letI : MonoidalCategoryStruct (ModuleCat.{u} R) :=
ModuleCat.liftedModuleMonoidalStruct.{u, u}
letI : MonoidalCategory (ModuleCat.{u} R) :=
ModuleCat.liftedModuleMonoidal.{u, u}
let R₀ := (DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
(MonoidalCategoryStruct.tensorUnit (ModuleCat.{u} R))
Nonempty (p.upperShriekFunctor.{u, u} ≅
derivedTensorProductOver.{u, u} f (p.upperShriekFunctor.{u, u}.obj R₀))
Tag 0E4C, a lemma
Tag 0E4C in the Stacks Project.
Dualizing.isGorensteinRing_fiber_iff_isInvertible_upperShriekFunctor_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/GorensteinFibres.lean, line 379.
Stacks Project, Tag 0E4C. Let
φ : R → Abe a flat homomorphism of finite type of Noetherian rings. Then the fibresA ⊗_R κ(q)are Gorenstein for every primeq ⊆ Rif and only if the relative dualizing complexω^•_{A/R} = φ^!(R)is an invertible object ofD(A).The statement is made for an arbitrary polynomial presentation
pofφ, so it holds for every model ofφ^!.
theorem isGorensteinRing_fiber_iff_isInvertible_upperShriekFunctor_unit
{R A : Type u} [CommRing R] [CommRing A] [IsNoetherianRing R] [IsNoetherianRing A]
[Algebra R A] [Module.Flat R A] (p : PolynomialPresentation (algebraMap R A)) :
letI := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory A).choose
(∀ (q : Ideal R) [q.IsPrime], letI := isNoetherianRing_baseChange q.ResidueField p
IsGorensteinRing (q.Fiber A)) ↔
MonoidalCategory.IsInvertible
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R)))
Tag 0E9N, a lemma
Tag 0E9N in the Stacks Project.
Dualizing.PolynomialPresentation.upperShriekFunctor_localization_isNormalizedDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/Normalized.lean, line 421.
Let
φ : R → Abe a finite type homomorphism of Noetherian rings withRlocal, and letm ⊆ Abe a maximal ideal lying over the maximal ideal ofR. Ifω_Ris a normalized dualizing complex forR, thenφ^!(ω_R)_mis a normalized dualizing complex forA_m, for every polynomial presentation ofφ.
theorem PolynomialPresentation.upperShriekFunctor_localization_isNormalizedDualizingComplex
{R A : Type u} [CommRing R] [CommRing A] [IsNoetherianRing R] [IsNoetherianRing A]
[IsLocalRing R] {f : R →+* A} (p : PolynomialPresentation f)
(m : Ideal A) [m.IsMaximal] (hlies : m.comap f = IsLocalRing.maximalIdeal R)
(K : DerivedCategory (ModuleCat.{u} R)) (hK : IsNormalizedDualizingComplex.{u, u} K) :
IsNormalizedDualizingComplex.{u, u}
((StacksDraft.PseudoCoherence.derivedExtensionScalars
(algebraMap A (Localization.AtPrime m))).obj (p.upperShriekFunctor.{u, u}.obj K))
Tag 0E9P, a lemma
Tag 0E9P in the Stacks Project.
Dualizing.upperShriekFunctor_neg_relativeDimensionAt_le_of_nontrivial_localizedHomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/FibreDimensionBound.lean, line 422. The attribute's comment: “for the upper shriek functor of an arbitrary polynomial presentation of the homomorphism, the relative dualizing complex being well defined only up to isomorphism, and with the fibre dimension named by a hypothesis identifying it with a natural number”.
[Stacks, Tag 0E9P]. Let
R → Abe a finite type homomorphism of Noetherian rings, let𝔮 ⊂ Abe a prime and letdbe the dimension at𝔮of the fibre ofSpec(A) → Spec(R)over the prime below𝔮. If the localization at𝔮ofH^i(ω^•_{A/R})is nonzero then-d ≤ i. Hereω^•_{A/R} = f^!(R)is computed from an arbitrary polynomial presentation off.
theorem upperShriekFunctor_neg_relativeDimensionAt_le_of_nontrivial_localizedHomology
{R A : Type u} [CommRing R] [CommRing A] [IsNoetherianRing R] [IsNoetherianRing A]
[Algebra R A] (p : PolynomialPresentation (algebraMap R A))
(q : PrimeSpectrum A) (d : ℕ)
(hd : Algebra.relativeDimensionAt R q.asIdeal = (d : WithBot ℕ∞)) (i : ℤ) :
Nontrivial
(LocalizedModule q.asIdeal.primeCompl
((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
(ModuleCat.of R R))))) →
-(d : ℤ) ≤ i
Tag 0E9Q, a lemma
Tag 0E9Q in the Stacks Project.
Dualizing.upperShriekFunctor_relativeDimensionAt_bounds_of_nontrivial_localizedHomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/FibreDimensionBoundUpper.lean, line 238. The attribute's comment: “the local bounds: H^i(omega)_q nonzero implies -d <= i <= 0, d the dimension at q of the fibre through q, for the upper shriek functor of an arbitrary polynomial presentation of the homomorphism, the relative dualizing complex being well defined only up to isomorphism; the Tor amplitude clause is Dualizing.upperShriekFunctor_hasTorAmplitude_of_fiber_dimension_le”.
[Stacks, Tag 0E9Q], the local bounds. Let
R → Abe a flat finite type homomorphism of Noetherian rings, let𝔮 ⊂ Abe a prime and letdbe the dimension at𝔮of the fibre ofSpec(A) → Spec(R)over the prime below𝔮. If the localization at𝔮ofH^i(ω^•_{A/R})is nonzero then-d ≤ i ≤ 0. Hereω^•_{A/R} = f^!(R)is computed from an arbitrary polynomial presentation off.
theorem upperShriekFunctor_relativeDimensionAt_bounds_of_nontrivial_localizedHomology
{R A : Type u} [CommRing R] [IsNoetherianRing R] [CommRing A] [IsNoetherianRing A]
[Algebra R A] [Module.Flat R A] (p : PolynomialPresentation (algebraMap R A))
(q : PrimeSpectrum A) (d : ℕ)
(hd : Algebra.relativeDimensionAt R q.asIdeal = (d : WithBot ℕ∞)) (i : ℤ) :
Nontrivial
(LocalizedModule q.asIdeal.primeCompl
((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
(ModuleCat.of R R))))) →
-(d : ℤ) ≤ i ∧ i ≤ 0
Dualizing.upperShriekFunctor_hasTorAmplitude_of_fiber_dimension_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingTorAmplitude.lean, line 505. The attribute's comment: “the Tor amplitude clause: if all fibres of Spec(A) -> Spec(R) have dimension at most d then the relative dualizing complex has Tor amplitude in [-d, 0] over R; the relative dualizing complex is read at the upper shriek functor of an arbitrary polynomial presentation of the homomorphism, being well defined only up to isomorphism”.
[Stacks, Tag 0E9Q], the Tor amplitude clause. Let
R → Abe a flat finite type homomorphism of Noetherian rings. If all fibres ofSpec(A) → Spec(R)have dimension at mostd, thenω^•_{A/R}has Tor amplitude in[-d, 0]as a complex ofR-modules.Here
ω^•_{A/R} = f^!(R)is read at an arbitrary polynomial presentation ofR → A, being defined only up to isomorphism, and Tor amplitude is read at the canonical certified derived tensor product ofR. Nothing is carried. Following the source, the Tor test at a finitely presented moduleMis the cohomology ofω^•_{A/R} ⊗_R^L (R ⊕ M), a base change to a Noetherian ring whose fibres have dimension at mostd: that isDualizing.isZero_homology_totalDerivedExtensionScalars_upperShriekFunctor_of_lt, proved by computing the base change on a finite projective resolution ofAover the polynomial algebra, which needs no comparison ofA-linear structures; arbitrary modules are filtered colimits of finitely presented ones.
theorem upperShriekFunctor_hasTorAmplitude_of_fiber_dimension_le
{R A : Type u} [CommRing R] [CommRing A] [IsNoetherianRing R] [IsNoetherianRing A]
[Algebra R A] [Module.Flat R A] (p : PolynomialPresentation (algebraMap R A)) (d : ℕ)
(hd : ∀ 𝔭 : AlgebraicGeometry.Spec (.of R),
topologicalKrullDim ((AlgebraicGeometry.Spec.map
(CommRingCat.ofHom (algebraMap R A))).fiber 𝔭) ≤ (d : WithBot ℕ∞)) :
StacksDraft.TorAmplitude.HasTorAmplitude
(StacksDraft.TorAmplitude.canonicalCertifiedDerivedTensoring R).tensor
(StacksDraft.TorAmplitude.canonicalCertifiedDerivedTensoring R).comparison
(StacksDraft.TorAmplitude.canonicalCertifiedDerivedTensoring R).isLeftDerived
((ModuleCat.restrictScalars (algebraMap R A)).mapDerivedCategory.obj
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R))))
(-(d : ℤ)) 0
Tag 0E9R, a lemma
Tag 0E9R in the Stacks Project.
Dualizing.le_of_nontrivial_localizedModule_homology_relativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingCohenMacaulay.lean, line 814. The attribute's comment: “the vanishing H^i(ω_{A/R})_𝔭 = 0 for i < -r, in full”.
[Stacks, Tag 0E9R], the vanishing. Let
R → Abe a finite type homomorphism of Noetherian rings and let𝔭 ⊂ Rbe a prime. Assume thatR_𝔭is Cohen--Macaulay and thattrdeg_{κ(R ∩ 𝔮)} κ(𝔮) ≤ rfor every minimal prime𝔮 ⊂ A. Then
H^i(ω^•_{A/R})_𝔭 ≠ 0 ⟹ -r ≤ i.Here
ω^•_{A/R} = φ^!(R)is the relative dualizing complex, computed from an arbitrary polynomial presentationpofR → A(it is well defined only up to isomorphism, so the statement is made for every presentation), and the localization at𝔭is the localization of theA-module at the image ofR ∖ 𝔭.The proof does not go through a dualizing complex of
R_𝔭. At a prime𝔮 ⊂ Aover a prime contained in𝔭, the localization ofH^i(ω^•_{A/R})isExt^{i+n}_{P_𝔯}(A_𝔯, P_𝔯), whereP_𝔯is Cohen--Macaulay anddepth_{I}(P_𝔯) ≥ n - rby the dimension formula; seeDualizing.subsingleton_and_min_two_le_moduleDepth_localizedModule_homology_upperShriek.
theorem le_of_nontrivial_localizedModule_homology_relativeDualizingComplex
{R A : Type u} [CommRing R] [CommRing A] [IsNoetherianRing R] [IsNoetherianRing A]
[Algebra R A] (p : PolynomialPresentation (algebraMap R A)) (𝔭 : Ideal R) [𝔭.IsPrime]
(hCM : IsCohenMacaulayLocalRing (Localization.AtPrime 𝔭)) (r : ℕ)
(htrdeg : ∀ (q : Ideal A) [q.IsPrime], q ∈ minimalPrimes A →
letI := Ideal.ResidueField.algebraOfLiesOver (q.under R) q
Algebra.trdeg (q.under R).ResidueField q.ResidueField ≤ r)
(i : ℤ) :
Nontrivial (LocalizedModule (Submonoid.map (algebraMap R A) 𝔭.primeCompl)
((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R))))) →
-(r : ℤ) ≤ i
Dualizing.propertySkModule_localizedModule_homology_relativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingCohenMacaulay.lean, line 848. The attribute's comment: “the (S_2) clause, H^{-r}(ω_{A/R})_𝔭 is (S_2) as an A_𝔭-module, in full”.
[Stacks, Tag 0E9R], the
(S₂)clause. LetR → Abe a finite type homomorphism of Noetherian rings and let𝔭 ⊂ Rbe a prime. Assume thatR_𝔭is Cohen--Macaulay and thattrdeg_{κ(R ∩ 𝔮)} κ(𝔮) ≤ rfor every minimal prime𝔮 ⊂ A. ThenH^{-r}(ω^•_{A/R})_𝔭satisfies Serre's condition(S₂)as anA_𝔭-module, whereA_𝔭is the localization ofAat the image ofR ∖ 𝔭.As in
Dualizing.le_of_nontrivial_localizedModule_homology_relativeDualizingComplex,ω^•_{A/R} = φ^!(R)is computed from an arbitrary polynomial presentationp. At a prime𝔮ofA_𝔭, the module isExt^{n-r}_{P_𝔯}(A_𝔯, P_𝔯)withP_𝔯Cohen--Macaulay andn - r ≤ depth_I(P_𝔯), and such anExtsatisfies(S₂)(Dualizing.min_two_le_moduleDepth_ext_of_le_depth).
theorem propertySkModule_localizedModule_homology_relativeDualizingComplex
{R A : Type u} [CommRing R] [CommRing A] [IsNoetherianRing R] [IsNoetherianRing A]
[Algebra R A] (p : PolynomialPresentation (algebraMap R A)) (𝔭 : Ideal R) [𝔭.IsPrime]
(hCM : IsCohenMacaulayLocalRing (Localization.AtPrime 𝔭)) (r : ℕ)
(htrdeg : ∀ (q : Ideal A) [q.IsPrime], q ∈ minimalPrimes A →
letI := Ideal.ResidueField.algebraOfLiesOver (q.under R) q
Algebra.trdeg (q.under R).ResidueField q.ResidueField ≤ r) :
letI : Module.Finite A ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-(r : ℤ))).obj
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R)))) :=
finite_homology_upperShriekFunctor p _
PropertySkModule (Localization (Submonoid.map (algebraMap R A) 𝔭.primeCompl))
(LocalizedModule (Submonoid.map (algebraMap R A) 𝔭.primeCompl)
((DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-(r : ℤ))).obj
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R))))) 2
Sources
Section47.26 More on dualizing complexes#
Section 47.26 of the Stacks Project, Tag 0E49. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0E4A, a lemma
Tag 0E4A in the Stacks Project.
Dualizing.isDualizingComplex_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingComplexes/FaithfullyFlatDescent.lean, line 933.
Stacks Project, Tag 0E4A. If a complex becomes dualizing after faithfully flat base change between Noetherian rings, then it was already dualizing.
public theorem isDualizingComplex_of_faithfullyFlat
{A : Type u} {B : Type w} [CommRing A] [CommRing B]
[IsNoetherianRing A] [IsNoetherianRing B]
(f : A →+* B) (hf : f.FaithfullyFlat)
(K : DerivedCategory (ModuleCat.{max v u w} A))
(hK : IsDualizingComplex
((CochainComplex.DerivedExtensionScalars.derivedExtensionScalarsGeneral.{u, v, w}
f).functor.obj K)) :
IsDualizingComplex K
Tag 0E4D, a lemma
Tag 0E4D in the Stacks Project.
Dualizing.isDualizingComplex_iff_derivedExtensionScalars_of_syntomic_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingComplexes/SyntomicBaseChangeUnconditional.lean, line 322. The attribute's comment: “case (1): A → B syntomic and surjective on spectra”.
Stacks Project, Tag 0E4D, case (1). Let
φ : A → Bbe a syntomic homomorphism of Noetherian rings which is surjective on spectra. ThenKinD(A)is a dualizing complex forAif and only ifK ⊗_A^L Bis a dualizing complex forB.Descent is [Stacks, Tag 0E4A] through the faithful flatness that syntomicity and surjectivity on spectra give ([Stacks, Tag 07D3] and [Stacks, Tag 00HQ]). Ascent is [Stacks, Tag 0BZL] at a polynomial presentation of
φ, which exists because a syntomic map is of finite type, together with the two inputs proved above: syntomic is a local complete intersection, soDualizing.isInvertible_relativeDualizingUnit_of_isLocalCompleteIntersectionsupplies the invertibility ofω^•_{B/A}andDualizing.nonempty_upperShriekFunctor_obj_iso_derivedExtensionScalars_tensor_of_lcithe tensor formula.
theorem isDualizingComplex_iff_derivedExtensionScalars_of_syntomic_unconditional
(f : A →+* B) (hsyn : letI := f.toAlgebra; Algebra.Syntomic A B)
(hsurj : Function.Surjective (PrimeSpectrum.comap f))
(K : DerivedCategory (ModuleCat.{u} A)) :
IsDualizingComplex K ↔
IsDualizingComplex ((derivedExtensionScalarsGeneral.{u, u, u} f).functor.obj K)
Dualizing.isDualizingComplex_iff_derivedExtensionScalars_of_faithfullyFlat_lci_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingComplexes/SyntomicBaseChangeUnconditional.lean, line 344. The attribute's comment: “case (2): A → B faithfully flat and a local complete intersection”.
Stacks Project, Tag 0E4D, case (2). Let
φ : A → Bbe a faithfully flat local complete intersection homomorphism of Noetherian rings. ThenKinD(A)is a dualizing complex forAif and only ifK ⊗_A^L Bis a dualizing complex forB.Descent is [Stacks, Tag 0E4A] at the given faithful flatness. Ascent is [Stacks, Tag 0BZL] at a polynomial presentation of
φ, which exists because a local complete intersection is of finite type, together with the two inputs proved above fromhlci.
theorem isDualizingComplex_iff_derivedExtensionScalars_of_faithfullyFlat_lci_unconditional
(f : A →+* B) (hff : f.FaithfullyFlat)
(hlci : RingHom.IsLocalCompleteIntersection f) (K : DerivedCategory (ModuleCat.{u} A)) :
IsDualizingComplex K ↔
IsDualizingComplex ((derivedExtensionScalarsGeneral.{u, u, u} f).functor.obj K)
Dualizing.isDualizingComplex_iff_derivedExtensionScalars_of_gorensteinFibres_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingComplexes/SyntomicBaseChangeUnconditional.lean, line 365. The attribute's comment: “case (3): A → B faithfully flat of finite type with Gorenstein fibres”.
Stacks Project, Tag 0E4D, case (3). Let
A → Bbe a faithfully flat homomorphism of finite type of Noetherian rings and assume every fibreB ⊗_A κ(q)is Gorenstein. ThenKinD(A)is a dualizing complex forAif and only ifK ⊗_A^L Bis a dualizing complex forB.Descent is [Stacks, Tag 0E4A]. Ascent is [Stacks, Tag 0BZL] at a polynomial presentation
p, which exists by finite type, together with two inputs: the invertibility ofω^•_{B/A}, which comes from the Gorenstein fibres by [Stacks, Tag 0E4C], and the tensor formula, whose only input is perfectness ofBover the polynomial algebra ofp, supplied by the flatness contained inhffthroughDualizing.PolynomialPresentation.isPerfectModule_of_flat.
theorem isDualizingComplex_iff_derivedExtensionScalars_of_gorensteinFibres_unconditional
[Algebra A B] (hff : (algebraMap A B).FaithfullyFlat) [Algebra.FiniteType A B]
(hGor : ∀ (q : Ideal A) [q.IsPrime],
letI := Algebra.FiniteType.isNoetherianRing q.ResidueField (q.Fiber B)
IsGorensteinRing (q.Fiber B))
(K : DerivedCategory (ModuleCat.{u} A)) :
IsDualizingComplex K ↔
IsDualizingComplex
((derivedExtensionScalarsGeneral.{u, u, u} (algebraMap A B)).functor.obj K)
Tag 0E4E, a lemma
Tag 0E4E in the Stacks Project.
Dualizing.exists_isInjectiveHull_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Complex/More.lean, line 730.
Under a flat local homomorphism of Noetherian local rings whose target maximal ideal is extended from the source, the base change of an injective hull of the source residue field is an injective hull of the target residue field.
theorem exists_isInjectiveHull_tensorProduct
(A B E : Type u) [CommRing A] [CommRing B]
[IsLocalRing A] [IsLocalRing B] [IsNoetherianRing A] [IsNoetherianRing B]
[Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Flat A B]
(hmax : Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A) =
IsLocalRing.maximalIdeal B)
[AddCommGroup E] [Module A E]
(i : ModuleCat.of A (IsLocalRing.ResidueField A) ⟶ ModuleCat.of A E) [Mono i]
(hi : Module.IsInjectiveHull i) :
∃ j : ModuleCat.of B (IsLocalRing.ResidueField B) ⟶
ModuleCat.of B (TensorProduct A B E),
∃ _ : Mono j, Module.IsInjectiveHull j
Tag 0E4F, a lemma
Tag 0E4F in the Stacks Project.
Module.tensorProduct_injective_of_flat_of_map_comap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DualizingComplexes/InjectiveBaseChange.lean, line 574.
Stacks Project, Tag 0E4F. A flat map of Noetherian rings for which, locally at every prime of the target, that prime is generated by its contraction preserves injective modules under base change.
public theorem tensorProduct_injective_of_flat_of_map_comap_eq
{A : Type u} {B : Type v} [CommRing A] [CommRing B]
[IsNoetherianRing A] [IsNoetherianRing B] [Algebra A B] [Module.Flat A B]
(hprime : ∀ (q : Ideal B) [q.IsPrime],
Ideal.map (algebraMap A (Localization.AtPrime q))
(Ideal.comap (algebraMap A B) q) =
Ideal.map (algebraMap B (Localization.AtPrime q)) q)
(I : Type w) [AddCommGroup I] [Module A I] [Module.Injective A I] :
Module.Injective B (TensorProduct A B I)
Sources
Section47.27 Relative dualizing complexes#
Section 47.27 of the Stacks Project, Tag 0E2B. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0E2C, a definition
Tag 0E2C in the Stacks Project.
Dualizing.IsRelativeDualizingComplex, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/Relative.lean, line 152.
Stacks Project, Tag 0E2C. A relative dualizing complex for a flat, finitely presented map
R → Ais anR-perfect objectKofD(A)such thatRHom_{A ⊗[R] A}(A, K ⊗[A]ᴸ (A ⊗[R] A))is isomorphic toA.
structure IsRelativeDualizingComplex (R A : Type u) [CommRing R] [CommRing A]
[Algebra R A] [Module.Flat R A] [Algebra.FinitePresentation R A]
(K : DerivedCategory (ModuleCat.{u} A)) : Prop
Tag 0E2D, a lemma
Tag 0E2D in the Stacks Project.
Dualizing.IsRelativeDualizingComplex.nonempty_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/RelativeUniquenessTensor.lean, line 41.
Let
R → Abe a flat ring map of finite presentation. Any two relative dualizing complexes forR → Aare isomorphic.
theorem IsRelativeDualizingComplex.nonempty_iso {R A : Type u} [CommRing R] [CommRing A]
[Algebra R A] [Module.Flat R A] [Algebra.FinitePresentation R A]
{K L : DerivedCategory (ModuleCat.{u} A)}
(hK : IsRelativeDualizingComplex R A K) (hL : IsRelativeDualizingComplex R A L) :
Nonempty (K ≅ L)
Tag 0E2E, a lemma
Tag 0E2E in the Stacks Project.
Dualizing.PolynomialPresentation.relativeDualizingComplex_isRelativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/UpperShriek/RelativeDualizingDiagonal.lean, line 370.
Stacks Project, Tag 0E2E. Let
φ : R → Abe a flat homomorphism of finite type of Noetherian rings. Then the relative dualizing complexω^•_{A/R} = φ^!(R)is a relative dualizing complex in the sense of [stacks 0E2C]; hereφ^!is read atp, which is an arbitrary polynomial presentation ofφ.Relative perfection is [stacks 0BZW] (2)(a),
Dualizing.PolynomialPresentation.relativeDualizingComplex_isRelativelyPerfect, and the diagonal condition isDualizing.PolynomialPresentation.relativeDualizingComplex_diagonalDerivedHom, from flat base change [stacks 0BZN], the composition [stacks 0BZT] and the independence of the presentation [stacks 0BZJ]. Finite presentation ofφ, which [stacks 0E2C] is stated for, is not a hypothesis: a flat map of finite type of Noetherian rings is of finite presentation, and a polynomial presentation exists only for a map of finite type.
theorem relativeDualizingComplex_isRelativeDualizingComplex
[IsNoetherianRing R] [IsNoetherianRing A]
(p : PolynomialPresentation (algebraMap R A)) (hflat : (algebraMap R A).Flat) :
letI : Module.Flat R A := RingHom.flat_algebraMap_iff.mp hflat
letI : Algebra.FinitePresentation R A :=
Algebra.FinitePresentation.of_finiteType.mp (RingHom.finiteType_algebraMap.mp p.finiteType)
IsRelativeDualizingComplex R A
(p.upperShriekFunctor.{u, 0}.obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R)))
Tag 0E2F, a lemma
Tag 0E2F in the Stacks Project.
Dualizing.exists_isRelativeDualizingComplex_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/RelativeExistenceInputs.lean, line 206. The attribute's comment: “(1)”.
Stacks Project, Tag 0E2F (1). A flat ring map of finite presentation
R → Aadmits a relative dualizing complex.The source's proof: a Noetherian model
R₀ → A₀ofR → Ahas the relative dualizing complexφ₀^!(R₀)of [stacks 0E2E], and its derived base change toAis one by (2) at the model and transitivity of derived base change.
theorem exists_isRelativeDualizingComplex_of_flat (R A : Type u) [CommRing R] [CommRing A]
[Algebra R A] [Module.Flat R A] [Algebra.FinitePresentation R A] :
∃ K : DerivedCategory (ModuleCat.{u} A), IsRelativeDualizingComplex R A K
Dualizing.IsRelativeDualizingComplex.baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/RelativeExistenceInputs.lean, line 215. The attribute's comment: “(2)”.
Stacks Project, Tag 0E2F (2). Let
R → Abe a flat ring map of finite presentation,Ka relative dualizing complex forR → AandR → R'any ring map. ThenK' = K ⊗ᴸ_A (A ⊗_R R')is a relative dualizing complex forR' → A ⊗_R R'.
theorem IsRelativeDualizingComplex.baseChange {R A : Type u} [CommRing R] [CommRing A]
[Algebra R A] [Module.Flat R A] [Algebra.FinitePresentation R A]
{K : DerivedCategory (ModuleCat.{u} A)} (hK : IsRelativeDualizingComplex R A K)
(R' : Type u) [CommRing R'] [Algebra R R'] :
letI : Module.Flat R' (A ⊗[R] R') := flat_baseChange R A R'
letI : Algebra.FinitePresentation R' (A ⊗[R] R') :=
Algebra.FinitePresentation.equiv (baseChangeComm R A R')
IsRelativeDualizingComplex R' (A ⊗[R] R')
((CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, u}
(Algebra.TensorProduct.includeLeftRingHom : A →+* A ⊗[R] R')).functor.obj K)
Dualizing.IsRelativeDualizingComplex.span_derivedBaseChange_diagonalGenerator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/RelativeExistenceInputs.lean, line 235. The attribute's comment: “moreover clause”.
Stacks Project, Tag 0E2F, the "moreover" clause. Let
R → Abe flat of finite presentation,Ka relative dualizing complex forR → A, andξ : A ⟶ K ⊗ᴸ_A (A ⊗_R A)a generator of the cyclic moduleHom_{D(A ⊗_R A)}(A, K ⊗ᴸ_A (A ⊗_R A)). For everyR → R'the derived base change ofξalongA ⊗_R A → A' ⊗_{R'} A'generatesHom_{D(A' ⊗_{R'} A')}(A', K' ⊗ᴸ_{A'} (A' ⊗_{R'} A')), through any identificationseΔof the base change ofAwithA'andeMof the base change ofK ⊗ᴸ_A (A ⊗_R A)withK' ⊗ᴸ_{A'} (A' ⊗_{R'} A').
theorem IsRelativeDualizingComplex.span_derivedBaseChange_diagonalGenerator {R A : Type u}
[CommRing R] [CommRing A] [Algebra R A] [Module.Flat R A] [Algebra.FinitePresentation R A]
{K : DerivedCategory (ModuleCat.{u} A)} (hK : IsRelativeDualizingComplex R A K)
(R' : Type u) [CommRing R'] [Algebra R R']
(ξ : diagonalSingle R A ⟶ (diagonalDerivedExtension R A).obj K)
(hξ : Submodule.span (A ⊗[R] A) ({ξ} : Set _) = ⊤) :
letI : Module.Flat R' (A ⊗[R] R') := flat_baseChange R A R'
∀ (eΔ : (CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, u}
(envelopingBaseChangeRingHom R A R')).functor.obj (diagonalSingle R A) ≅
diagonalSingle R' (A ⊗[R] R'))
(eM : (CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, u}
(envelopingBaseChangeRingHom R A R')).functor.obj
((diagonalDerivedExtension R A).obj K) ≅
(diagonalDerivedExtension R' (A ⊗[R] R')).obj
((CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, u}
(Algebra.TensorProduct.includeLeftRingHom : A →+* A ⊗[R] R')).functor.obj K)),
Submodule.span ((A ⊗[R] R') ⊗[R'] (A ⊗[R] R'))
({eΔ.inv ≫ (CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, u}
(envelopingBaseChangeRingHom R A R')).functor.map ξ ≫ eM.hom} : Set _) = ⊤
Tag 0E2G, a lemma
Tag 0E2G in the Stacks Project.
Dualizing.isIso_relativeHomothety_of_isRelativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/RelativeHomothetyGeneral.lean, line 241.
Stacks Project, Tag 0E2G. Let
R → Abe a flat ring map of finite presentation and letKbe a relative dualizing complex forR → A([stacks 0E2C]). Then the canonical mapA ⟶ RHom_A(K, K)is an isomorphism.This is
Dualizing.isIso_relativeHomothety_of_isRelativeDualizingComplex_of_uniquenesswith the uniqueness of relative dualizing complexes supplied by [stacks 0E2D],Dualizing.IsRelativeDualizingComplex.nonempty_iso. The proof is the source's: reduction to a Noetherian model by [stacks 02JO], the Noetherian case through [stacks 0E2E], [stacks 0E2F] and [stacks 0BZW], and the passage to an arbitrary base by [stacks 0DHX]; see the module documentation.
theorem isIso_relativeHomothety_of_isRelativeDualizingComplex
{R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [Module.Flat R A]
[Algebra.FinitePresentation R A] (K : DerivedCategory (ModuleCat.{u} A))
(hK : IsRelativeDualizingComplex R A K) :
IsIso (relativeHomothety A K)
Tag 0E2H, a lemma
Tag 0E2H in the Stacks Project.
Dualizing.isRelativeDualizingComplex_derivedTensorProductOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/RelativeCompositionTag.lean, line 175.
Stacks 0E2H. Let
R → A → Bbe ring maps which are flat and of finite presentation, letK_{A/R}be a relative dualizing complex forR → AandK_{B/A}one forA → B. ThenK = K_{A/R} ⊗ᴸ_A K_{B/A}is a relative dualizing complex forR → B.Clause (1) of [stacks 0E2C] is
Dualizing.relativelyPerfectOverBase_derivedTensorProductOverand clause (2) follows from the isomorphism (★),Dualizing.diagonalQuotientDerivedHom_derivedTensorProductOver; see the module documentation.
theorem isRelativeDualizingComplex_derivedTensorProductOver
(KA : DerivedCategory (ModuleCat.{u} A)) (KB : DerivedCategory (ModuleCat.{u} B))
(hKA : IsRelativeDualizingComplex R A KA)
(hKB : IsRelativeDualizingComplex A B KB) :
letI : Module.Flat R B := Module.Flat.trans R A B
letI : Algebra.FinitePresentation R B := Algebra.FinitePresentation.trans R A B
IsRelativeDualizingComplex R B
((derivedTensorProductOver.{u, u} (algebraMap A B) KB).obj KA)
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.