48.22 Dualizing modules to 48.31 Preliminaries to…

Section48.22 Dualizing modules#

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

Tag 0AWH, the section

Tag 0AWH in the Stacks Project.

Stacks.Duality.IsDualizingModuleOf.shift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleInvertibleTwist.lean, line 231. The attribute's comment: “the first half of the section's second warning: the dualizing complex is not unique. A shift of a dualizing complex is a dualizing complex, not isomorphic to it for a nonzero shift, with the same dualizing module in the shifted degree”.

Stacks Project, Tag 0AWH. The dualizing complex is not unique. If ω is a dualizing module of the dualizing complex K, realized in degree n, then for every integer k the shifted complex K⟦k⟧ is again a dualizing complex, its dualizing module is realized in degree n - k and is isomorphic to ω, and for k ≠ 0 the complex K⟦k⟧ is not isomorphic to K.

theorem IsDualizingModuleOf.shift [HasDerivedCategory.{w} X.Modules] {ω : X.Modules}
    {K : DerivedCategory X.Modules} {n : ℤ} (h : IsDualizingModuleOf ω K n) (k : ℤ) :
    IsDualizingModuleOf ((DerivedCategory.homologyFunctor X.Modules (n - k)).obj (K⟦k⟧))
        (K⟦k⟧) (n - k) ∧
      Nonempty ((DerivedCategory.homologyFunctor X.Modules (n - k)).obj (K⟦k⟧) ≅ ω) ∧
      (k ≠ 0 → IsEmpty (K⟦k⟧ ≅ K))

Stacks.Duality.IsDualizingModuleOf.exists_isInvertibleModule_iso_sheafTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleInvertibleTwist.lean, line 270. The attribute's comment: “the second half of the section's second warning: the dualizing module is unique up to tensoring by an invertible module. Stated for a connected locally Noetherian scheme: on a disconnected one two dualizing complexes can shift by different amounts on different components and their dualizing modules then need not differ by a twist (counterexample Spec k disjoint union Spec k in the module documentation). The relation between the two complexes is proved, from Tag 0ATP and Tag 0FPG, not assumed”.

Stacks Project, Tag 0AWH. On a connected locally Noetherian scheme the dualizing module is unique up to tensoring by an invertible module: if ω is a dualizing module of the dualizing complex K and ω' one of the dualizing complex K', there is an invertible 𝒪_X-module ℒ with ω' ≅ ω ⊗_{𝒪_X} ℒ.

theorem IsDualizingModuleOf.exists_isInvertibleModule_iso_sheafTensor [ConnectedSpace X]
    [HasDerivedCategory.{w} X.Modules] {ω ω' : X.Modules} {K K' : DerivedCategory X.Modules}
    {n n' : ℤ} (h : IsDualizingModuleOf ω K n) (h' : IsDualizingModuleOf ω' K' n') :
    ∃ ℒ : X.Modules, Stacks.SheafOfModules.Tensor.IsInvertibleModule X.sheaf ℒ ∧
      Nonempty (ω' ≅ ((Stacks.SheafOfModules.Tensor.sheafTensor X.sheaf).obj ω).obj ℒ)

Stacks.Duality.isDualizingModuleOf_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleMaximalDimension.lean, line 191. The attribute's comment: “the definition the section states: omega_X = H^n(omega_X^bullet) with n the smallest integer such that H^n(omega_X^bullet) is nonzero, for a dualizing complex on a (locally) Noetherian scheme; IsDualizingModuleOf omega K n holds exactly when K is a dualizing complex, n is the least element of the set of degrees with nonzero cohomology, and omega is the cohomology sheaf in degree n”.

Stacks Project, Tag 0AWH, the definition. Let X be a locally Noetherian scheme and K a dualizing complex on X. Let n be the smallest integer such that H^n(K) is nonzero; then H^n(K) is the dualizing module ω_X. This is what Stacks.Duality.IsDualizingModuleOf ω K n says: it holds exactly when K is a dualizing complex, n is the least degree with nonzero cohomology, and ω = H^n(K).

theorem isDualizingModuleOf_iff {X : Scheme.{u}} [IsLocallyNoetherian X]
    [HasDerivedCategory.{w} X.Modules] (ω : X.Modules) (K : DerivedCategory X.Modules) (n : ℤ) :
    IsDualizingModuleOf ω K n ↔ IsDualizingComplex K ∧
      IsLeast {i : ℤ | ¬ IsZero ((DerivedCategory.homologyFunctor X.Modules i).obj K)} n ∧
      ω = (DerivedCategory.homologyFunctor X.Modules n).obj K

Stacks.Duality.isGreatest_neg_of_isDualizingModuleOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleMaximalDimension.lean, line 212. The attribute's comment: “the section's identification of the degree: -n is the maximal value of the dimension function attached to omega_X^bullet (Tag 0AWF), where n is the least degree in which the dualizing complex has nonvanishing cohomology. The dimension function is associatedShiftFunction K, which Tag 0AWF (isUniversallyCatenary_and_isDimensionFunction_associatedShiftFunction) shows is the normalizing shift of the derived stalks and a dimension function. Stated for a locally Noetherian scheme, which contains the source's Noetherian case”.

Stacks Project, Tag 0AWH. Let X be a locally Noetherian scheme and let ω be a dualizing module of the dualizing complex K, realized in degree n, the least degree in which K has nonvanishing cohomology. Then -n is the maximal value of the dimension function attached to K by [Stacks, Tag 0AWF], the function δ = associatedShiftFunction K with ω^•_{X,x}⟦-δ(x)⟧ a normalized dualizing complex over 𝒪_{X,x}.

theorem isGreatest_neg_of_isDualizingModuleOf {X : Scheme.{u}} [IsLocallyNoetherian X]
    [HasDerivedCategory.{w} X.Modules] {ω : X.Modules} {K : DerivedCategory X.Modules} {n : ℤ}
    (hω : IsDualizingModuleOf ω K n) :
    IsGreatest (Set.range (associatedShiftFunction K)) (-n)

Stacks.Duality.IsDualizingModuleOf.restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleRestriction.lean, line 64. The attribute's comment: “the section's first warning: the integer n may change on passing to an open U, and then the restriction of omega_X to U is not omega_U. The degree can only go up, the two modules agree when it does not change, and when it changes the restriction is zero while omega_U is not”.

Stacks Project, Tag 0AWH, the first warning. Let ω be a dualizing module of the dualizing complex K on X, realized in degree n, let U ⊆ X be open and let ω_U be a dualizing module of the restriction K|_U, realized in degree n_U. Then n ≤ n_U; if n = n_U then ω|_U ≅ ω_U; and if the degree changes, n < n_U, then ω|_U is zero while ω_U is not, so ω|_U is not isomorphic to ω_U.

theorem IsDualizingModuleOf.restrict {ω : X.Modules} {K : DerivedCategory X.Modules} {n : ℤ}
    (h : IsDualizingModuleOf ω K n) (U : X.Opens) [HasDerivedCategory.{w'} U.toScheme.Modules]
    {ωU : U.toScheme.Modules} {nU : ℤ}
    (hU : IsDualizingModuleOf ωU
      ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj K) nU) :
    n ≤ nU ∧ (n = nU → Nonempty ((Scheme.Modules.restrictFunctor U.ι).obj ω ≅ ωU)) ∧
      (n < nU → IsZero ((Scheme.Modules.restrictFunctor U.ι).obj ω) ∧ ¬ IsZero ωU ∧
        IsEmpty ((Scheme.Modules.restrictFunctor U.ι).obj ω ≅ ωU))

Stacks.Duality.IsDualizingModuleOf.restrict_of_associatedShiftFunction_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleRestriction.lean, line 150. The attribute's comment: “the section's closing remark on the first warning: if the dimension function attached to omega_X^bullet (Tag 0AWF) maps every generic point of X to the same integer, the degree does not change on a nonempty open U and omega_X restricted to U is omega_U”.

Stacks Project, Tag 0AWH, the closing remark on the first warning. If the dimension function attached to K ([Stacks, Tag 0AWF]) takes the same value at every generic point of X, then the degree of the dualizing module does not change on passing to a nonempty open U ⊆ X, and the restriction of the dualizing module of K is the dualizing module of K|_U.

theorem IsDualizingModuleOf.restrict_of_associatedShiftFunction_genericPoints
    {ω : X.Modules} {K : DerivedCategory X.Modules} {n : ℤ}
    (h : IsDualizingModuleOf ω K n)
    (hgen : ∃ c : ℤ, ∀ ξ ∈ genericPoints X, associatedShiftFunction K ξ = c)
    (U : X.Opens) (hne : (U : Set X).Nonempty) [HasDerivedCategory.{w'} U.toScheme.Modules]
    {ωU : U.toScheme.Modules} {nU : ℤ}
    (hU : IsDualizingModuleOf ωU
      ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj K) nU) :
    nU = n ∧ Nonempty ((Scheme.Modules.restrictFunctor U.ι).obj ω ≅ ωU)

Tag 0AWI, an example

Tag 0AWI in the Stacks Project.

Stacks.Duality.isDualizingModuleOf_relativeDualizingModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/DualizingModuleProperCharts.lean, line 96.

Stacks Project, Tag 0AWI (Example 48.22.1). Let S be affine with A = Γ(S, ⊤) a Noetherian local ring, ω_S^• modelled on S by a normalized dualizing complex ω_A^•, f : X ⟶ S proper and ω_X^• = f^!ω_S^• = a(ω_S^•). Then ω_X = H^{-dim X}(ω_X^•) is a coherent sheaf, and, X being nonempty, a dualizing module: ω_X^• is a dualizing complex and -dim X is the least degree in which it has nonzero cohomology.

theorem isDualizingModuleOf_relativeDualizingModule
    (f : X ⟶ S) [IsProper f] (ωS : quasiCoherentDerivedCategory S)
    (ω : DerivedCategory (ModuleCat.{u} Γ(S, ⊤)))
    (hω : Dualizing.IsNormalizedDualizingComplex.{u, u} ω)
    (hmodel : IsTildeModelOnAnyModel ωS.obj ⊤ (isAffineOpen_top S) ω) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    (relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        ωS).IsCoherent ∧
      (Nonempty X → IsDualizingModuleOf
        (relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f) ωS)
        (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
          ωS).obj (-(natDim X : ℤ)))

Stacks.Duality.isCoherent_relativeDualizingModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/ModuleCoherence.lean, line 76. The attribute's comment: “coherence, given the dualizing-complex clause as hypothesis”.

The "coherence" half of [Stacks, Tag 0AWI], reduced to its "dualizing complex" half. The relative dualizing module ω_X = H^{-dim X}(f^! ω_Y) is coherent as soon as the relative dualizing complex f^! ω_Y is a dualizing complex on X.

theorem isCoherent_relativeDualizingModule {X Y : Scheme.{u}} [IsLocallyNoetherian X] (f : X ⟶ Y)
    (hpush : ∀ (K : quasiCoherentDerivedCategory X) (i : ℤ),
      ((DerivedCategory.homologyFunctor Y.Modules i).obj
        ((derivedPushforward f).obj K.obj)).IsQuasicoherent)
    [(quasiCoherentDerivedPushforward f hpush).IsLeftAdjoint]
    (ωY : quasiCoherentDerivedCategory Y)
    (h : IsDualizingComplex (relativeDualizingComplex f hpush ωY).obj) :
    _root_.SheafOfModules.IsCoherent (relativeDualizingModule f hpush ωY)

Stacks.Duality.relativeDualizingModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingModule.lean, line 138. The attribute's comment: “relative dualizing module: definition only”.

The relative dualizing module ω_X = H^{-dim(X)}(ω_X^•) of [Stacks, Tag 0AWI]: the cohomology sheaf of the relative dualizing complex in degree minus the dimension of X.

def relativeDualizingModule (ωY : quasiCoherentDerivedCategory Y) : X.Modules

Tag 0AWJ, an example

Tag 0AWJ in the Stacks Project.

Stacks.Duality.normalizedDualizingModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleOverField.lean, line 117. The attribute's comment: “the definition: omega_X = H^{-dim X}(omega_X^bullet) for the complex normalized relative to k[0]”.

The dualizing module ω_X = H^{-dim(X)}(ω_X^•) of [Stacks, Tag 0AWJ]: the cohomology sheaf in degree minus the dimension of X of a complex normalized relative to a chosen complex on the base. Over a field, with ω_S^• = k[0], this is the customary dualizing module of an equidimensional scheme of finite type over k.

def normalizedDualizingModule (𝒩 : Normalized A hp ωS 𝒰) : X.Modules

Stacks.Duality.normalizedUpperShriekOverField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleOverField.lean, line 224. The attribute's comment: “the second assertion: for X separated over k the normalized complex is f^! O_{Spec k}. RESTRICTED: the upper-shriek formalism of Stacks 0A9Y/0ATX/0ATY is the parameter UpperShriek, pending its landing”.

[Stacks, Tag 0AWJ] For X separated and of finite type over a field k with structure morphism f : X ⟶ Spec(k), the complex f^!𝒪_{Spec(k)} is normalized relative to k[0]: this is the identification ω_X^• = f^!𝒪_{Spec(k)} the example records, by [Stacks, Tag 0AUE].

def normalizedUpperShriekOverField {ι : Type w} (𝒰 : SeparatedCovering p ι) :
    Normalized A (isFiniteTypeOverNoetherian_of_field p)
      (DerivedPushforward.derivedStructureSheaf (Spec (.of k))).obj 𝒰

Stacks.Duality.isDualizingComplex_normalizedDualizingComplex_of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/DualizingModuleOverFieldNagata.lean, line 62. The attribute's comment: “omega_X^bullet, the dualizing complex normalized relative to k[0]”.

[Stacks, Tag 0AWJ], the complex ω_X^•. For X of finite type over a field k, the dualizing complex ω_X^• normalized relative to k[0] (k[0] being a dualizing complex on Spec(k)) is a dualizing complex, and it is unique up to unique isomorphism: any complex normalized relative to k[0] is isomorphic to it by exactly one isomorphism compatible with the normalizations.

theorem isDualizingComplex_normalizedDualizingComplex_of_field :
    haveI := (isFiniteTypeOverNoetherian_of_field p).source_noetherian
    IsDualizingComplex (normalizedDualizingComplex (isFiniteTypeOverNoetherian_of_field p)
        (derivedStructureSheafPlus (Spec (.of k)))
        (isDualizingComplex_derivedStructureSheafPlus_of_field k)).complex.obj.obj ∧
    ∀ 𝒦 : NormalizedOnOpens UpperShriek.nagata (isFiniteTypeOverNoetherian_of_field p)
        (derivedStructureSheafPlus (Spec (.of k))),
      ∃! e : (normalizedDualizingComplex (isFiniteTypeOverNoetherian_of_field p)
          (derivedStructureSheafPlus (Spec (.of k)))
          (isDualizingComplex_derivedStructureSheafPlus_of_field k)).complex ≅ 𝒦.complex,
        ∀ (W : X.Opens) (hW : IsShriekable (W.ι ≫ p)),
          (UpperShriek.nagata.shriek W.ι
              ((isFiniteTypeOverNoetherian_of_field p).isShriekable_ι W)).mapIso e ≪≫
            𝒦.localIso W hW =
          (normalizedDualizingComplex (isFiniteTypeOverNoetherian_of_field p)
            (derivedStructureSheafPlus (Spec (.of k)))
            (isDualizingComplex_derivedStructureSheafPlus_of_field k)).localIso W hW

Stacks.Duality.dualizingModuleOfCompactifications_nagata_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/DualizingModuleOverFieldNagata.lean, line 88. The attribute's comment: “omega_X = H^{-dim X}(omega_X^bullet)”.

[Stacks, Tag 0AWJ], the module ω_X. For X of finite type over a field k, the dualizing module ω_X is H^{-dim(X)}(ω_X^•), the cohomology sheaf in degree minus the dimension of X of the dualizing complex normalized relative to k[0].

theorem dualizingModuleOfCompactifications_nagata_eq :
    dualizingModuleOfCompactifications nagataCompactification p =
      (DerivedCategory.homologyFunctor X.Modules
        (-(ENat.toNat ((topologicalKrullDim X).getD 0) : ℤ))).obj
        (normalizedDualizingComplex (isFiniteTypeOverNoetherian_of_field p)
          (derivedStructureSheafPlus (Spec (.of k)))
          (isDualizingComplex_derivedStructureSheafPlus_of_field k)).complex.obj.obj

Stacks.Duality.existsUnique_iso_upperShriekPlus_of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/DualizingModuleOverFieldNagata.lean, line 104. The attribute's comment: “for X separated over k, omega_X^bullet = f^! O_{Spec k}”.

[Stacks, Tag 0AWJ], the separated case. If X is separated and of finite type over a field k, then ω_X^• = f^! 𝒪_{Spec(k)}, f : X ⟶ Spec(k) being the structure morphism and f^! the upper shriek functor of [Stacks, Tag 0A9Y] at any compactification j of f: there is exactly one isomorphism ω_X^• ≅ f^!_j 𝒪_{Spec(k)} which, followed by the comparison with the Nagata compactification, carries the normalization of ω_X^• on each open W separated over k to the canonical (f^! 𝒪_{Spec(k)})|_W ≅ (W → Spec(k))^! 𝒪_{Spec(k)}.

theorem existsUnique_iso_upperShriekPlus_of_field [IsSeparated p]
    (j : CompactificationOf (Over.mk p)) :
    haveI := isNoetherian_spec_of_field k
    ∃! e : (normalizedDualizingComplex (isFiniteTypeOverNoetherian_of_field p)
        (derivedStructureSheafPlus (Spec (.of k)))
        (isDualizingComplex_derivedStructureSheafPlus_of_field k)).complex ≅
      (upperShriekPlus (ftsHomOf p (isShriekable_of_field p).separatedFiniteType
        (isSeparatedFiniteType_id _) (Category.comp_id p)) j).obj
        (derivedStructureSheafPlus (Spec (.of k))),
      ∀ (W : X.Opens) (hW : IsShriekable (W.ι ≫ p)),
        (UpperShriek.nagata.shriek W.ι
            ((isFiniteTypeOverNoetherian_of_field p).isShriekable_ι W)).mapIso
            (e ≪≫ (DominatingCompactification.upperShriekPlusIso (ftsHomOf p
              (isShriekable_of_field p).separatedFiniteType (isSeparatedFiniteType_id _)
              (Category.comp_id p)) j
              (nagataCompactification p (isShriekable_of_field p))).app
              (derivedStructureSheafPlus (Spec (.of k)))) ≪≫
          upperShriekLocalIso UpperShriek.nagata (isFiniteTypeOverNoetherian_of_field p)
            (isShriekable_of_field p) (derivedStructureSheafPlus (Spec (.of k))) hW =
        (normalizedDualizingComplex (isFiniteTypeOverNoetherian_of_field p)
          (derivedStructureSheafPlus (Spec (.of k)))
          (isDualizingComplex_derivedStructureSheafPlus_of_field k)).localIso W hW

Stacks.Duality.normalizedDualizingComplexIsoRelativeDualizingComplexOfField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/DualizingModuleOverFieldNagata.lean, line 134. The attribute's comment: “for X proper over k, omega_X^bullet = a(O_{Spec k}), the complex of Example 0AWI”.

[Stacks, Tag 0AWJ], the proper case: ω_X^• = a(𝒪_{Spec(k)}). If X is proper over a field k, the dualizing complex normalized relative to k[0] is the twisted inverse image a(𝒪_{Spec(k)}) of [Stacks, Tag 0A9E], that is, the relative dualizing complex f^! ω_S^• of [Stacks, Tag 0AWI] for S = Spec(k) and ω_S^• = k[0].

def normalizedDualizingComplexIsoRelativeDualizingComplexOfField [IsProper p] :
    haveI := isNoetherian_spec_of_field k
    haveI := (isFiniteTypeOverNoetherian_of_field p).source_noetherian
    (normalizedDualizingComplex (isFiniteTypeOverNoetherian_of_field p)
        (derivedStructureSheafPlus (Spec (.of k)))
        (isDualizingComplex_derivedStructureSheafPlus_of_field k)).complex.obj ≅
      relativeDualizingComplex p (isQuasicoherent_homology_derivedPushforward_of_qcqs p)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))

Stacks.Duality.dualizingModuleOfCompactifications_nagata_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/DualizingModuleOverFieldNagata.lean, line 159. The attribute's comment: “for X proper over k, this is a special case of Example 0AWI”.

[Stacks, Tag 0AWJ], the proper case is a special case of [Stacks, Tag 0AWI]. If X is proper over a field k, then ω_X is the relative dualizing module of [Stacks, Tag 0AWI] for S = Spec(k) and ω_S^• = k[0] (a normalized dualizing complex over the local ring k); hence ω_X is coherent and, X being nonempty, a dualizing module: ω_X^• is a dualizing complex and -dim(X) is the least degree in which it has nonzero cohomology.

theorem dualizingModuleOfCompactifications_nagata_of_isProper [IsProper p] :
    haveI := isNoetherian_spec_of_field k
    haveI := (isFiniteTypeOverNoetherian_of_field p).source_noetherian
    Nonempty (dualizingModuleOfCompactifications nagataCompactification p ≅
        relativeDualizingModule p (isQuasicoherent_homology_derivedPushforward_of_qcqs p)
          (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))) ∧
      (dualizingModuleOfCompactifications nagataCompactification p).IsCoherent ∧
      (Nonempty X → IsDualizingModuleOf
        (dualizingModuleOfCompactifications nagataCompactification p)
        (normalizedDualizingComplex (isFiniteTypeOverNoetherian_of_field p)
          (derivedStructureSheafPlus (Spec (.of k)))
          (isDualizingComplex_derivedStructureSheafPlus_of_field k)).complex.obj.obj
        (-(natDim X : ℤ)))

Tag 0AWK, a lemma

Tag 0AWK in the Stacks Project.

Stacks.Duality.IsDualizingModuleOf.isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleOfComplex.lean, line 60. The attribute's comment: “coherence”.

A dualizing module on a connected Noetherian scheme is a coherent 𝒪_X-module: it is a cohomology sheaf of a dualizing complex, and those are coherent.

theorem IsDualizingModuleOf.isCoherent {X : Scheme.{u}} [IsNoetherian X] [ConnectedSpace X]
    [HasDerivedCategory.{w} X.Modules] {ω : X.Modules} {K : DerivedCategory X.Modules} {n : ℤ}
    (h : IsDualizingModuleOf ω K n) : _root_.SheafOfModules.IsCoherent ω

Stacks.Duality.IsDualizingModuleOf.sheafHasPropertySk_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleSupportSerre.lean, line 87. The attribute's comment: “Serre's condition (S₂), granted that at every point the stalk either vanishes or is the canonical module of the local ring”.

Stacks Project, Tag 0AWK. The dualizing module of a dualizing complex on a connected Noetherian scheme satisfies Serre's condition (S₂): at a point where its stalk is the canonical module of the local ring the depth bound for canonical modules applies, and at a point where the stalk vanishes the condition is empty.

public theorem IsDualizingModuleOf.sheafHasPropertySk_two {X : Scheme.{u}} [IsNoetherian X]
    [ConnectedSpace X] [HasDerivedCategory.{w} X.Modules] {ω : X.Modules}
    {K : DerivedCategory X.Modules} {n : ℤ} (h : IsDualizingModuleOf ω K n)
    (hstalk : ∀ x : X,
      Subsingleton ↑(TopCat.Presheaf.stalk
          (SheafOfModules.val
            (R := structureSheafRing
              X.toRingedSpace)
            ((DerivedCategory.homologyFunctor X.Modules n).obj K)).presheaf x) ∨
        ∃ (L : DerivedCategory (ModuleCat.{u} (X.presheaf.stalk x))) (d : ℕ),
          _root_.Dualizing.IsNormalizedDualizingComplex.{u, u} L ∧
            ringKrullDim (X.presheaf.stalk x) = (d : WithBot ℕ∞) ∧
              Nonempty (↑(TopCat.Presheaf.stalk
                  (SheafOfModules.val
                    (R := structureSheafRing
                      X.toRingedSpace)
                    ((DerivedCategory.homologyFunctor X.Modules n).obj K)).presheaf x) ≃ₗ[
                  X.presheaf.stalk x]
                ↑((DerivedCategory.homologyFunctor (ModuleCat.{u} (X.presheaf.stalk x))
                  (-(d : ℤ))).obj L))) :
    SheafHasPropertySk X ω 2

Stacks.Duality.IsDualizingModuleOf.supp_eq_and_isCoherent_and_sheafHasPropertySk_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleSupportSerreFull.lean, line 247.

Stacks Project, Tag 0AWK. Let X be a connected Noetherian scheme and let ω be a dualizing module on X, the cohomology sheaf of a dualizing complex K in the leftmost degree n in which K has nonvanishing cohomology. Then the support of ω is the union of the irreducible components of maximal dimension with respect to any dimension function δ, and ω is a coherent 𝒪_X-module having property (S₂).

theorem IsDualizingModuleOf.supp_eq_and_isCoherent_and_sheafHasPropertySk_two
    [ConnectedSpace X] (h : IsDualizingModuleOf ω K n) :
    (∀ δ : DimensionFunction X,
      (⟨ω.val, ω.isSheaf⟩ : RingedSpace.ModuleSheaf.{u} X.toRingedSpace).supp =
        {x : X | ∃ ξ ∈ genericPoints X, x ∈ closure {ξ} ∧
          ∀ η ∈ genericPoints X, δ η ≤ δ ξ}) ∧
      _root_.SheafOfModules.IsCoherent ω ∧ SheafHasPropertySk X ω 2

Tag 0AWN, a lemma

Tag 0AWN in the Stacks Project.

Stacks.Duality.vanishing_and_support_relativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/ProperOverLocalBaseCharts.lean, line 92.

Stacks Project, Tag 0AWN (Lemma 48.22.4). Let S be affine with A = Γ(S, ⊤) a Noetherian local ring, ω_S^• the complex associated to a normalized dualizing complex ω_A^•, f : X ⟶ S proper, ω_X^• = f^!ω_S^• = a(ω_S^•) and ω_X = H^{-dim X}(ω_X^•) ([Stacks, Tag 0AWI]). Then 1. H^i(ω_X^•) ≠ 0 implies i ∈ {-dim X, …, 0}; 2. the support of H^i(ω_X^•) has dimension at most -i; 3. Supp(ω_X) is the union of the irreducible components of dimension dim X; 4. ω_X (which is coherent) has property (S₂).

theorem vanishing_and_support_relativeDualizingComplex
    (f : X ⟶ S) [IsProper f] (ωS : quasiCoherentDerivedCategory S)
    (ω : DerivedCategory (ModuleCat.{u} Γ(S, ⊤)))
    (hω : Dualizing.IsNormalizedDualizingComplex.{u, u} ω)
    (hmodel : IsTildeModelOnAnyModel ωS.obj ⊤ (isAffineOpen_top S) ω) :
    let L := (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
      ωS).obj
    (∀ i : ℤ, ¬ Limits.IsZero ((DerivedCategory.homologyFunctor X.Modules i).obj L) →
      i ≤ 0 ∧ (((-i).toNat : ℕ) : WithBot ℕ∞) ≤ topologicalKrullDim X) ∧
    (∀ i : ℤ, topologicalKrullDim (_root_.SheafOfModules.supp
        ((DerivedCategory.homologyFunctor X.Modules i).obj L)) ≤
      if i ≤ 0 then (((-i).toNat : ℕ) : WithBot ℕ∞) else ⊥) ∧
    (relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        ωS).IsCoherent ∧
    SheafHasPropertySk X (relativeDualizingModule f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f) ωS) 2 ∧
    _root_.SheafOfModules.supp (relativeDualizingModule f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f) ωS) =
      ⋃₀ {C ∈ irreducibleComponents X | topologicalKrullDim C = topologicalKrullDim X}

Stacks.Duality.supp_relativeDualizingModule_eq_topDimensionalComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/VanishingAndSupport.lean, line 291. The attribute's comment: “part (3): Supp(omega_X) is the union of the components of dimension dim(X). RESTRICTED: two explicit hypotheses. hloc is the local description of omega_X^bullet, a Stacks.Duality.HasNormalizedStalks; see part (1) for what it records and why. hcomp is a statement about a catenary Noetherian scheme with no dualizing complex in it -- that a point satisfies dim(closure {x}) + dim(O_{X,x}) = dim(X) exactly when it lies on an irreducible component of dimension dim(X); its analogue over a Noetherian local ring is the catenary step inside Dualizing.support_canonicalModule of Tag 0AWE, but the scheme-level statement is not proved here. The dualizing content is proved and is unconditional given hloc: supp_relativeDualizingModule_eq_setOf identifies Supp(omega_X) with the locus where that equality holds, by the lower degree bound of Tag 0A7U and the nonvanishing of the canonical module of Tag 0A7V on the stalk”.

Stacks Project, Tag 0AWN, part (3). Let X/A with ω_X^• and ω_X be as in [Stacks, Tag 0AWI]. Then Supp(ω_X) is the union of the irreducible components of X of dimension dim(X), given the hypothesis hcomp that a point x satisfies dim(closure {x}) + dim(𝒪_{X,x}) = dim(X) exactly when it lies on an irreducible component of X of dimension dim(X).

theorem supp_relativeDualizingModule_eq_topDimensionalComponents
    (hloc : HasNormalizedStalks (relativeDualizingComplex f hpush ωY).obj n)
    (hcomp : ∀ x : X, topologicalKrullDim (closure ({x} : Set X)) +
          ringKrullDim (X.presheaf.stalk x) = (n : WithBot ℕ∞) ↔
        x ∈ ⋃₀ {C ∈ irreducibleComponents X | topologicalKrullDim C = (n : WithBot ℕ∞)}) :
    _root_.SheafOfModules.supp (relativeDualizingModule f hpush ωY) =
      ⋃₀ {C ∈ irreducibleComponents X | topologicalKrullDim C = (n : WithBot ℕ∞)}

Tag 0AWP, a lemma

Tag 0AWP in the Stacks Project.

Stacks.Duality.dualizingModuleRepresentableBy, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/VanishingResults/DualizingModuleRepresentabilityLocalBase.lean, line 994. The attribute's comment: “the whole lemma, in the setting of Example 0AWI with omega_X^bullet the twisted inverse image of omega_S^bullet (the relative dualizing complex of the 0AWI definition) and omega_A = H^{-dim A}(omega_A^bullet); the functor is represented on all quasi-coherent modules, which contain the coherent ones, and d may be any upper bound for dim(X_s) with dim(X) = d + dim(A)”.

[Stacks, Tag 0AWP]. Let (A, 𝔪, κ) be a Noetherian local ring and let ω_S^• be an object of D_QCoh(𝒪_{Spec A}) corresponding to a normalized dualizing complex ω_A^•. Let f : X ⟶ Spec A be proper, ω_X^• = f^×ω_S^• and ω_X = H^{-dim(X)}(ω_X^•), as in Example [Stacks, Tag 0AWI]. Let d bound the dimension of the closed fibre X_s and suppose dim(X) = d + dim(A). Then ω_X represents the functor

ℱ ↦ Hom_A(H^d(X, ℱ), ω_A), ω_A = H^{-dim(A)}(ω_A^•),

on the quasi-coherent 𝒪_X-modules — so in particular on the coherent ones.

The represented functor is ℱ ↦ Hom_A(H^d(X, ℱ), ω_A) with H^d(X, ℱ) the classical sheaf cohomology with its A-module structure, and the representation is Stacks.Duality.dualizingModuleHomAddEquiv, natural by Stacks.Duality.dualizingModuleHomAddEquiv_naturality. Nothing is carried: part (1) of [Stacks, Tag 0AWN], the vanishing of H^i(ω_X^•) below -dim(X) that the source's first equality needs, is Stacks.Duality.isGE_relativeDualizingComplex_of_closedFibre_dim_le.

def dualizingModuleRepresentableBy :
    (((SheafOfModules.isQuasicoherent X.ringCatSheaf).ι ⋙
        Stacks.LocalCohomology.cohomologyOverBaseFunctor.{u, u} A f d).op ⋙
      yoneda.obj ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-(e : ℤ))).obj
        ((derivedGlobalSectionsQuasicoherent (CommRingCat.of A)).obj ωS))).RepresentableBy
      (⟨relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f) ωS,
        isQuasicoherent_relativeDualizingModule f
          (isQuasicoherent_homology_derivedPushforward_of_qcqs f) ωS⟩ :
        (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory)

Sources

• Section 48.22, Tag 0AWH
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Duality.IsDualizingModuleOf.shift · Stacks.Duality.IsDualizingModuleOf.exists_isInvertibleModule_iso_sheafTensor · Stacks.Duality.isDualizingModuleOf_iff · Stacks.Duality.isGreatest_neg_of_isDualizingModuleOf · Stacks.Duality.IsDualizingModuleOf.restrict · Stacks.Duality.IsDualizingModuleOf.restrict_of_associatedShiftFunction_genericPoints · Stacks.Duality.isDualizingModuleOf_relativeDualizingModule · Stacks.Duality.isCoherent_relativeDualizingModule

Section48.23 Cohen-Macaulay schemes#

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

Tag 0AWT, a lemma

Tag 0AWT in the Stacks Project.

Stacks.Duality.sheafIsCohenMacaulay_homology_of_concentrated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CohenMacaulayDualizingModule.lean, line 161. The attribute's comment: “the dualizing module is Cohen--Macaulay, at an arbitrary degree of concentration”.

Stacks Project, Tag 0AWT, the Cohen--Macaulayness of the dualizing module. If the cohomology of a dualizing complex on a locally Noetherian scheme is concentrated in the single degree n, then H^n of it is a Cohen--Macaulay 𝒪_X-module in the sense of [Stacks, Tag 0343].

public theorem sheafIsCohenMacaulay_homology_of_concentrated {X : Scheme.{u}}
    [IsLocallyNoetherian X] [HasDerivedCategory.{w} X.Modules]
    (K : DerivedCategory X.Modules) (hK : IsDualizingComplex K) (n : ℤ)
    (hn : ∀ i : ℤ, i ≠ n → IsZero ((DerivedCategory.homologyFunctor X.Modules i).obj K)) :
    AlgebraicGeometry.SheafIsCohenMacaulay X
      ((DerivedCategory.homologyFunctor X.Modules n).obj K)

Stacks.Duality.exists_coherent_cohenMacaulay_iso_single_of_connected, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CohenMacaulayDualizingModule.lean, line 193. The attribute's comment: “the final assertion, in full”.

Stacks Project, Tag 0AWT, the final assertion, in full. If X is connected and Cohen--Macaulay then there is an integer n and a coherent Cohen--Macaulay 𝒪_X-module ω_X = H^n(ω_X^•) with ω_X^• = ω_X[-n].

This is Stacks.Duality.exists_coherent_iso_single_of_connected together with the Cohen--Macaulayness clause of the source, which that statement omits.

public theorem exists_coherent_cohenMacaulay_iso_single_of_connected {X : Scheme.{u}}
    [IsLocallyNoetherian X] [ConnectedSpace X] [HasDerivedCategory.{w} X.Modules]
    (K : DerivedCategory X.Modules) (hK : IsDualizingComplex K)
    (hX : AlgebraicGeometry.IsCohenMacaulay X) :
    ∃ n : ℤ, _root_.SheafOfModules.IsCoherent
        ((DerivedCategory.homologyFunctor X.Modules n).obj K) ∧
      AlgebraicGeometry.SheafIsCohenMacaulay X
        ((DerivedCategory.homologyFunctor X.Modules n).obj K) ∧
      Nonempty (K ≅ (DerivedCategory.singleFunctor X.Modules n).obj
        ((DerivedCategory.homologyFunctor X.Modules n).obj K))

Stacks.Duality.isOpen_setOf_isCohenMacaulayLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CohenMacaulayLocus.lean, line 380. The attribute's comment: “clause (3), the Cohen--Macaulay locus is open”.

Stacks Project, Tag 0AWT, clause (3), openness. On a locally Noetherian scheme carrying a dualizing complex, the set of points whose local ring is Cohen–Macaulay is open.

public theorem isOpen_setOf_isCohenMacaulayLocalRing {X : Scheme.{u}} [IsLocallyNoetherian X]
    [HasDerivedCategory.{w} X.Modules] (K : DerivedCategory X.Modules)
    (hK : IsDualizingComplex K) :
    IsOpen {x : X | IsCohenMacaulayLocalRing (X.presheaf.stalk x)}

Stacks.Duality.isCohenMacaulay_cohenMacaulayLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CohenMacaulayLocus.lean, line 426. The attribute's comment: “clause (3), the Cohen--Macaulay locus is Cohen--Macaulay”.

Stacks Project, Tag 0AWT, clause (3), the locus is Cohen–Macaulay. The open subscheme of points with Cohen–Macaulay local ring is a Cohen–Macaulay scheme.

public theorem isCohenMacaulay_cohenMacaulayLocus {X : Scheme.{u}} [IsLocallyNoetherian X]
    [HasDerivedCategory.{w} X.Modules] (K : DerivedCategory X.Modules)
    (hK : IsDualizingComplex K) :
    AlgebraicGeometry.IsCohenMacaulay (cohenMacaulayLocus K hK).toScheme

Stacks.Duality.isCohenMacaulayLocalRing_stalk_iff_concentrated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CohenMacaulayLocus.lean, line 571. The attribute's comment: “clause (2), the stalkwise criterion”.

Stacks Project, Tag 0AWT, clause (2). On a locally Noetherian scheme carrying a dualizing complex K, the local ring at x is Cohen–Macaulay exactly when the derived stalk K_x has a single nonzero cohomology module.

public theorem isCohenMacaulayLocalRing_stalk_iff_concentrated {X : Scheme.{u}}
    [IsLocallyNoetherian X] [HasDerivedCategory.{w} X.Modules]
    (K : DerivedCategory X.Modules) (hK : IsDualizingComplex K) (x : X)
    [HasDerivedCategory.{w} (ModuleCat.{u} (X.presheaf.stalk x))] :
    IsCohenMacaulayLocalRing (X.presheaf.stalk x) ↔
      ∃ n : ℤ, ∀ i : ℤ, i ≠ n → Limits.IsZero ((DerivedCategory.homologyFunctor
        (ModuleCat.{u} (X.presheaf.stalk x)) i).obj
        ((AlgebraicGeometry.derivedStalkFunctor x).obj K))

Stacks.Duality.isCohenMacaulay_iff_locally_unique_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CohenMacaulayLocus.lean, line 701. The attribute's comment: “clause (1), locally a single nonzero cohomology sheaf, read stalkwise”.

Stacks Project, Tag 0AWT, clause (1). A locally Noetherian scheme carrying a dualizing complex K is Cohen–Macaulay exactly when K locally has a single nonzero cohomology sheaf: every point has an open neighbourhood on which, for all but one degree, the cohomology sheaves of K have vanishing stalks.

Vanishing of all the stalks over an open is vanishing of the restricted sheaf there, by [Stacks, Tag 01AG] (AlgebraicGeometry.SheafOfModules.isZero_iff_forall_isZero_stalkFunctor_obj), so this is the source's "ω_X^• locally has a unique nonzero cohomology sheaf".

public theorem isCohenMacaulay_iff_locally_unique_homology {X : Scheme.{u}}
    [IsLocallyNoetherian X] [HasDerivedCategory.{w} X.Modules]
    (K : DerivedCategory X.Modules) (hK : IsDualizingComplex K) :
    AlgebraicGeometry.IsCohenMacaulay X ↔
      ∀ x : X, ∃ V : X.Opens, x ∈ V ∧ ∃ n : ℤ, ∀ i : ℤ, i ≠ n → ∀ y ∈ V,
        Subsingleton
          (((DerivedCategory.homologyFunctor X.Modules i).obj K).presheaf.stalk y)

Tag 0AWU, a lemma

Tag 0AWU in the Stacks Project.

Stacks.Duality.isCohenMacaulay_of_exists_coherent_dualizingModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CohenMacaulaySchemeOfDualizingModule.lean, line 158.

Let X be a locally Noetherian scheme. If there exists a coherent sheaf ω_X such that ω_X[0] is a dualizing complex on X, then X is a Cohen–Macaulay scheme.

theorem isCohenMacaulay_of_exists_coherent_dualizingModule
    (h : ∃ omegaX : X.Modules, _root_.SheafOfModules.IsCoherent omegaX ∧
      IsDualizingComplex ((DerivedCategory.singleFunctor X.Modules 0).obj omegaX)) :
    AlgebraicGeometry.IsCohenMacaulay X

Tag 0C0Z, a lemma

Tag 0C0Z in the Stacks Project.

Stacks.Duality.isCohenMacaulayAt_iff_exists_unique_nonzero_homology_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekChartConsequences.lean, line 87.

Let S be Noetherian, f : X ⟶ Y a flat morphism of FTS S and x ∈ X. Then f is Cohen–Macaulay at x if and only if f^!𝒪_Y has a unique nonzero cohomology sheaf in a neighbourhood of x.

theorem isCohenMacaulayAt_iff_exists_unique_nonzero_homology_upperShriek [Flat f.left]
    (x : X.left) :
    f.left.IsCohenMacaulayAt (isLocallyNoetherian_fiber_left f) x ↔
      ∃ W : X.left.Opens, x ∈ W ∧ ∃ n : ℤ,
        ¬ IsZero ((Scheme.Modules.restrictFunctor W.ι).obj
          ((DerivedCategory.homologyFunctor X.left.Modules n).obj
            (relativeDualizingComplexObj f j))) ∧
        ∀ i : ℤ, i ≠ n → IsZero ((Scheme.Modules.restrictFunctor W.ι).obj
          ((DerivedCategory.homologyFunctor X.left.Modules i).obj
            (relativeDualizingComplexObj f j)))

Tag 0C10, a remark

Tag 0C10 in the Stacks Project.

Stacks.Duality.NormalizedOnOpens.nonempty_iso_pullback_tensor_shift_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedCohenMacaulayTwistNagata.lean, line 56. The attribute's comment: “Similar results hold for X and Y of finite type over S, not necessarily separated, with complexes normalized relative to omega_S: omega_X = Lf^* omega_Y (x) omega_{X/Y}[d]”.

[Stacks, Tag 0C10], last sentence, the complexes. Let S be Noetherian with a dualizing complex ω_S^• and f : X ⟶ Y a separated Cohen–Macaulay morphism of relative dimension d between schemes of finite type over S, not necessarily separated over S. For dualizing complexes ω_X^•, ω_Y^• normalized relative to ω_S^• and ω_{X/Y} = H^{-d}(f^! 𝒪_Y), ω_X^• ≅ Lf^* ω_Y^• ⊗ᴸ ω_{X/Y}[d].

theorem nonempty_iso_pullback_tensor_shift_nagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) (hf : IsShriekable f)
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS)
    (hCM : haveI := hf.target_noetherian
      (ftsHomOf f hf.separatedFiniteType (isSeparatedFiniteType_id Y)
        (Category.comp_id f)).left.IsCohenMacaulay (isLocallyNoetherian_fiber_left _))
    (d : ℕ) (hd : ∀ x : X, topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) =
      (d : WithBot ℕ∞)) :
    haveI := hf.target_noetherian
    Nonempty (𝒦X.complex.obj ≅ ((quasiCoherentDerivedTensor X).obj
        ((quasiCoherentDerivedPullback' f).obj 𝒦Y.complex.obj)).obj
          (relativeDualizingSheafShift (ftsHomOf f hf.separatedFiniteType
            (isSeparatedFiniteType_id Y) (Category.comp_id f)) (nagataCompactification f hf)
            hCM d hd))

Stacks.Duality.NormalizedOnOpens.exists_homology_iso_pullback_tensor_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedCohenMacaulayTwistNagata.lean, line 82. The attribute's comment: “Similar results hold for X and Y of finite type over S, not necessarily separated, with complexes normalized relative to omega_S: omega_X = f^* omega_Y (x) omega_{X/Y} for connected Cohen-Macaulay schemes”.

[Stacks, Tag 0C10], last sentence, the dualizing modules. In the situation of nonempty_iso_pullback_tensor_shift_nagata, if moreover Y is connected and Cohen–Macaulay, the normalized complexes ω_Y^• and ω_X^• are concentrated in single degrees m and m - d, and their cohomology sheaves ω_Y, ω_X there satisfy ω_X ≅ f^* ω_Y ⊗ ω_{X/Y}.

theorem exists_homology_iso_pullback_tensor_nagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) (hf : IsShriekable f)
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS)
    (hCM : haveI := hf.target_noetherian
      (ftsHomOf f hf.separatedFiniteType (isSeparatedFiniteType_id Y)
        (Category.comp_id f)).left.IsCohenMacaulay (isLocallyNoetherian_fiber_left _))
    (d : ℕ) (hd : ∀ x : X, topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) =
      (d : WithBot ℕ∞))
    [ConnectedSpace Y] (hY : AlgebraicGeometry.IsCohenMacaulay Y) :
    haveI := hf.target_noetherian
    ∃ m : ℤ,
      (∀ i : ℤ, i ≠ m → IsZero ((DerivedCategory.homologyFunctor Y.Modules i).obj
        𝒦Y.complex.obj.obj)) ∧
      (∀ i : ℤ, i ≠ m - d → IsZero ((DerivedCategory.homologyFunctor X.Modules i).obj
        𝒦X.complex.obj.obj)) ∧
      Nonempty ((DerivedCategory.homologyFunctor X.Modules (m - d)).obj 𝒦X.complex.obj.obj ≅
        ((Stacks.SheafOfModules.Tensor.sheafTensor X.sheaf).obj
          ((Scheme.Modules.pullback f).obj
            ((DerivedCategory.homologyFunctor Y.Modules m).obj 𝒦Y.complex.obj.obj))).obj
          (relativeDualizingSheaf (ftsHomOf f hf.separatedFiniteType
            (isSeparatedFiniteType_id Y) (Category.comp_id f)) (nagataCompactification f hf)
            d))

Stacks.Duality.nonempty_upperShriek_iso_pullback_tensor_shift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekCohenMacaulayTwistIso.lean, line 58. The attribute's comment: “f^!K = Lf^*K (x) omega_{X/Y}[d] for K in D^+_QCoh”.

Stacks Project, Tag 0C10, the canonical isomorphism. For a Cohen–Macaulay morphism f : X ⟶ Y of FTS S of relative dimension d and K ∈ D⁺_QCoh(𝒪_Y), f^!K ≅ Lf^*K ⊗ᴸ ω_{X/Y}[d], through μ_{f,K} of Tag 0B6U.

theorem nonempty_upperShriek_iso_pullback_tensor_shift
    (hCM : f.left.IsCohenMacaulay (isLocallyNoetherian_fiber_left f)) (d : ℕ)
    (hd : ∀ x : X.left,
      topologicalKrullDimAt (f.left.fiber (f.left x)) (f.left.asFiber x) = (d : WithBot ℕ∞))
    (K : quasiCoherentDerivedCategory Y.left) (hK : DerivedCategoryB.IsBoundedBelow K.obj) :
    Nonempty ((upperShriek f j).obj K ≅
      ((quasiCoherentDerivedTensor X.left).obj
        ((quasiCoherentDerivedPullback' f.left).obj K)).obj
          (relativeDualizingSheafShift f j hCM d hd))

Stacks.Duality.nonempty_upperShriek_comp_iso_pullback_tensor_shift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekCohenMacaulayTwistIso.lean, line 74. The attribute's comment: “omega_X = Lf^* omega_Y (x) omega_{X/Y}[d]”.

Stacks Project, Tag 0C10, "in particular". For πY : Y ⟶ T, πX = f ≫ πY and ω_T ∈ D⁺_QCoh(𝒪_T) (for instance a dualizing complex), with ω_Y = πY^!ω_T and ω_X = πX^!ω_T: ω_X ≅ Lf^*ω_Y ⊗ᴸ ω_{X/Y}[d].

theorem nonempty_upperShriek_comp_iso_pullback_tensor_shift
    (hCM : f.left.IsCohenMacaulay (isLocallyNoetherian_fiber_left f)) (d : ℕ)
    (hd : ∀ x : X.left,
      topologicalKrullDimAt (f.left.fiber (f.left x)) (f.left.asFiber x) = (d : WithBot ℕ∞))
    {T : FTS S} (πY : Y ⟶ T) (πX : X ⟶ T) (hπ : f ≫ πY = πX)
    (jY : CompactificationOf (Over.mk πY.left)) (jX : CompactificationOf (Over.mk πX.left))
    (ωT : quasiCoherentDerivedCategory T.left) (hωT : DerivedCategoryB.IsBoundedBelow ωT.obj) :
    Nonempty ((upperShriek πX jX).obj ωT ≅
      ((quasiCoherentDerivedTensor X.left).obj
        ((quasiCoherentDerivedPullback' f.left).obj ((upperShriek πY jY).obj ωT))).obj
          (relativeDualizingSheafShift f j hCM d hd))

Stacks.Duality.exists_homology_upperShriek_comp_iso_pullback_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekCohenMacaulayTwistIso.lean, line 94. The attribute's comment: “omega_X = f^* omega_Y (x) omega_{X/Y} for connected Cohen-Macaulay schemes”.

Stacks Project, Tag 0C10, the dualizing modules. If moreover ω_T is a dualizing complex and Y is connected and Cohen–Macaulay, then ω_Y^• and ω_X^• are concentrated in single degrees m and m - d, and their cohomology sheaves ω_Y, ω_X there satisfy ω_X ≅ f^*ω_Y ⊗ ω_{X/Y}. (Connectedness and Cohen–Macaulayness of X are not needed.)

theorem exists_homology_upperShriek_comp_iso_pullback_tensor
    (hCM : f.left.IsCohenMacaulay (isLocallyNoetherian_fiber_left f)) (d : ℕ)
    (hd : ∀ x : X.left,
      topologicalKrullDimAt (f.left.fiber (f.left x)) (f.left.asFiber x) = (d : WithBot ℕ∞))
    {T : FTS S} (πY : Y ⟶ T) (πX : X ⟶ T) (hπ : f ≫ πY = πX)
    (jY : CompactificationOf (Over.mk πY.left)) (jX : CompactificationOf (Over.mk πX.left))
    (ωT : quasiCoherentDerivedCategory T.left) (hωT : IsDualizingComplex ωT.obj)
    [ConnectedSpace Y.left] (hY : AlgebraicGeometry.IsCohenMacaulay Y.left) :
    ∃ m : ℤ,
      (∀ i : ℤ, i ≠ m → IsZero ((DerivedCategory.homologyFunctor Y.left.Modules i).obj
        ((upperShriek πY jY).obj ωT).obj)) ∧
      (∀ i : ℤ, i ≠ m - d → IsZero ((DerivedCategory.homologyFunctor X.left.Modules i).obj
        ((upperShriek πX jX).obj ωT).obj)) ∧
      Nonempty ((DerivedCategory.homologyFunctor X.left.Modules (m - d)).obj
          ((upperShriek πX jX).obj ωT).obj ≅
        ((Stacks.SheafOfModules.Tensor.sheafTensor X.left.sheaf).obj
          ((Scheme.Modules.pullback f.left).obj
            ((DerivedCategory.homologyFunctor Y.left.Modules m).obj
              ((upperShriek πY jY).obj ωT).obj))).obj (relativeDualizingSheaf f j d))

Sources

• Section 48.23, Tag 0AWQ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Duality.sheafIsCohenMacaulay_homology_of_concentrated · Stacks.Duality.exists_coherent_cohenMacaulay_iso_single_of_connected · Stacks.Duality.isOpen_setOf_isCohenMacaulayLocalRing · Stacks.Duality.isCohenMacaulay_cohenMacaulayLocus · Stacks.Duality.isCohenMacaulayLocalRing_stalk_iff_concentrated · Stacks.Duality.isCohenMacaulay_iff_locally_unique_homology · Stacks.Duality.isCohenMacaulay_of_exists_coherent_dualizingModule · Stacks.Duality.isCohenMacaulayAt_iff_exists_unique_nonzero_homology_upperShriek

Section48.24 Gorenstein schemes#

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

Tag 0AWV, the section

Tag 0AWV in the Stacks Project.

AlgebraicGeometry.isGorenstein_Spec_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/AffineCharacterization.lean, line 60. The attribute's comment: “the definition makes sense: for a Noetherian ring R, Spec R is a Gorenstein scheme if and only if R is a Gorenstein ring”.

The definition of a Gorenstein scheme agrees with that of a Gorenstein ring (Section 0AWV). For a Noetherian ring R, the scheme Spec R is Gorenstein if and only if R is a Gorenstein ring, i.e. all of its local rings are Gorenstein.

theorem isGorenstein_Spec_iff (R : CommRingCat.{u}) [IsNoetherianRing R] :
    IsGorenstein (Spec R) ↔ Dualizing.IsGorensteinRing R

Declarations registered for the tag:

• AlgebraicGeometry.IsGorenstein, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/AffineCharacterization.lean, line 43 (StacksFrontier): “the definition of the section: a scheme is Gorenstein if it is locally Noetherian and all of its local rings are Gorenstein”.

Tag 0AWW, a definition

Tag 0AWW in the Stacks Project.

AlgebraicGeometry.IsGorenstein, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/Basic.lean, line 43.

A scheme is Gorenstein if it is locally Noetherian and all of its local rings are Gorenstein.

public class IsGorenstein (X : Scheme.{u}) : Prop extends IsLocallyNoetherian X

Tag 0C00, a lemma

Tag 0C00 in the Stacks Project.

AlgebraicGeometry.isCohenMacaulay_of_isGorenstein, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/CohenMacaulay.lean, line 37.

Stacks Project, Tag 0C00. Every Gorenstein scheme is Cohen–Macaulay.

public theorem isCohenMacaulay_of_isGorenstein (X : Scheme.{u}) [IsGorenstein X] :
    IsCohenMacaulay X

Tag 0DWG, a lemma

Tag 0DWG in the Stacks Project.

AlgebraicGeometry.isGorenstein_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/Regular.lean, line 36.

Stacks Project, Tag 0DWG. Every regular scheme is Gorenstein.

public theorem isGorenstein_of_isRegular (X : Scheme.{u}) (hX : IsRegular X) :
    IsGorenstein X

Tag 0BFQ, a lemma

Tag 0BFQ in the Stacks Project.

Stacks.Duality.isGorenstein_iff_isInvertible_dualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/DualizingInvertible.lean, line 214. The attribute's comment: “(1)(a): X is Gorenstein iff its dualizing complex is invertible in D(O_X)”.

Stacks Project, Tag 0BFQ, clause (1)(a). A locally Noetherian scheme X carrying a dualizing complex ω_X^• is Gorenstein if and only if ω_X^• is an invertible object of D(𝒪_X).

public theorem isGorenstein_iff_isInvertible_dualizingComplex [IsLocallyNoetherian X]
    (K : DerivedCategory X.Modules) (hK : IsDualizingComplex K) :
    AlgebraicGeometry.IsGorenstein X ↔
      letI := Scheme.Modules.derivedMonoidal X
      MonoidalCategory.IsInvertible K

Stacks.Duality.isGorenstein_iff_hasInvertibleDualizingModelOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/InvertibleDualizing.lean, line 140. The attribute's comment: “(1)(a): Gorenstein iff the dualizing complex is locally a shift of the structure ring, read at the affine-local models”.

A locally Noetherian scheme carrying a dualizing complex is Gorenstein exactly when, at every affine open, that complex is the associated sheaf of a dualizing complex over the ring of sections which is locally a shifted unit — an invertible module in a single degree, locally on the affine open.

By [Stacks, Tag 0FNT] the condition on the model says that it is an invertible object of D(Γ(X, U)); see Stacks.Duality.isGorenstein_iff_isInvertible_dualizingModel.

public theorem isGorenstein_iff_hasInvertibleDualizingModelOn (K : DerivedCategory X.Modules)
    (hK : IsDualizingComplex K) :
    AlgebraicGeometry.IsGorenstein X ↔
      ∀ (U : X.Opens) (hU : IsAffineOpen U), HasInvertibleDualizingModelOn K U hU

Stacks.Duality.isGorenstein_iff_isInvertible_dualizingModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/InvertibleDualizing.lean, line 175. The attribute's comment: “(1)(a): Gorenstein iff the dualizing complex is an invertible object, read at the affine-local models”.

A locally Noetherian scheme carrying a dualizing complex is Gorenstein exactly when, at every affine open, that complex is the associated sheaf of a dualizing complex over the ring of sections which is an invertible object of its derived category, for the canonical derived tensor product of [Stacks, Tag 0FNQ].

This is Stacks.Duality.isGorenstein_iff_hasInvertibleDualizingModelOn rewritten through [Stacks, Tag 0FNT].

public theorem isGorenstein_iff_isInvertible_dualizingModel (K : DerivedCategory X.Modules)
    (hK : IsDualizingComplex K) :
    AlgebraicGeometry.IsGorenstein X ↔
      ∀ (U : X.Opens) (hU : IsAffineOpen U),
        letI : IsNoetherianRing Γ(X, U) := IsLocallyNoetherian.component_noetherian ⟨U, hU⟩
        letI := HasDerivedCategory.standard U.toScheme.Modules
        letI := HasDerivedCategory.standard (ModuleCat.{u} Γ(X, U))
        letI := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory
          Γ(X, U)).choose
        ∃ ω : DerivedCategory (ModuleCat.{u} Γ(X, U)),
          Dualizing.IsDualizingComplex ω ∧
            MonoidalCategory.IsInvertible ω ∧
              Nonempty ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj K ≅
                (tilde.functor Γ(X, U) ⋙
                  Scheme.Modules.restrictFunctor hU.isoSpec.hom).mapDerivedCategory.obj ω)

Stacks.Duality.exists_isOpen_isGorenstein, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/Locus.lean, line 140. The attribute's comment: “(1)(c): the Gorenstein locus is an open Gorenstein subscheme”.

Stacks Project, Tag 0BFQ, clause (1)(c). On a locally Noetherian scheme carrying a dualizing complex, U = {x ∈ X | 𝒪_{X,x} is Gorenstein} is open and, as an open subscheme, is a Gorenstein scheme.

public theorem exists_isOpen_isGorenstein (K : DerivedCategory X.Modules)
    (hK : IsDualizingComplex K) :
    ∃ hU : IsOpen {x : X | Dualizing.IsGorensteinLocalRing (X.presheaf.stalk x)},
      AlgebraicGeometry.IsGorenstein (Scheme.Opens.toScheme (X := X) ⟨_, hU⟩)

Stacks.Duality.isGorensteinLocalRing_stalk_iff_isInvertible_localizedDualizing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/StalkInvertibleDualizing.lean, line 88. The attribute's comment: “(1)(b): the local ring at a point is Gorenstein iff the dualizing complex localized at that point is invertible, read at the affine-local models”.

Let X be a locally Noetherian scheme, U an affine open and x a point of U. For every dualizing complex ω over Γ(X, U), the local ring of X at x is Gorenstein exactly when the derived localization of ω at the prime x defines is an invertible object of the derived category of that localization.

public theorem isGorensteinLocalRing_stalk_iff_isInvertible_localizedDualizing
    {U : X.Opens} (hU : IsAffineOpen U) (x : U) :
    letI : IsNoetherianRing Γ(X, U) := IsLocallyNoetherian.component_noetherian ⟨U, hU⟩
    letI := HasDerivedCategory.standard (ModuleCat.{u} Γ(X, U))
    letI : (hU.primeIdealOf x).asIdeal.IsPrime := (hU.primeIdealOf x).isPrime
    letI := HasDerivedCategory.standard
      (ModuleCat.{u} (Localization.AtPrime (hU.primeIdealOf x).asIdeal))
    letI := Dualizing.derivedCategoryMonoidal.{u, u}
      (Localization.AtPrime (hU.primeIdealOf x).asIdeal)
    ∀ ω : DerivedCategory (ModuleCat.{u} Γ(X, U)), Dualizing.IsDualizingComplex ω →
      (Dualizing.IsGorensteinLocalRing (X.presheaf.stalk x.1) ↔
        MonoidalCategory.IsInvertible
          ((StacksDraft.PseudoCoherence.derivedExtensionScalars
              (algebraMap Γ(X, U)
                (Localization.AtPrime (hU.primeIdealOf x).asIdeal))).obj ω))

Stacks.Duality.isGorensteinLocalRing_stalk_iff_isInvertible_localizedDualizingModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/StalkInvertibleDualizing.lean, line 130. The attribute's comment: “(1)(b): the local ring at a point is Gorenstein iff the dualizing complex of the scheme, localized at that point, is invertible, read at the affine-local models”.

Let K be a dualizing complex on a locally Noetherian scheme X, and x a point of an affine open U. The local ring of X at x is Gorenstein exactly when K has a dualizing model on U whose derived localization at the prime of x is invertible.

public theorem isGorensteinLocalRing_stalk_iff_isInvertible_localizedDualizingModel
    (K : DerivedCategory X.Modules) (hK : IsDualizingComplex K)
    {U : X.Opens} (hU : IsAffineOpen U) (x : U) :
    letI : IsNoetherianRing Γ(X, U) := IsLocallyNoetherian.component_noetherian ⟨U, hU⟩
    letI := HasDerivedCategory.standard U.toScheme.Modules
    letI := HasDerivedCategory.standard (ModuleCat.{u} Γ(X, U))
    letI : (hU.primeIdealOf x).asIdeal.IsPrime := (hU.primeIdealOf x).isPrime
    letI := HasDerivedCategory.standard
      (ModuleCat.{u} (Localization.AtPrime (hU.primeIdealOf x).asIdeal))
    letI := Dualizing.derivedCategoryMonoidal.{u, u}
      (Localization.AtPrime (hU.primeIdealOf x).asIdeal)
    Dualizing.IsGorensteinLocalRing (X.presheaf.stalk x.1) ↔
      ∃ ω : DerivedCategory (ModuleCat.{u} Γ(X, U)),
        Dualizing.IsDualizingComplex ω ∧
          Nonempty ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj K ≅
            (tilde.functor Γ(X, U) ⋙
              Scheme.Modules.restrictFunctor hU.isoSpec.hom).mapDerivedCategory.obj ω) ∧
            MonoidalCategory.IsInvertible
              ((StacksDraft.PseudoCoherence.derivedExtensionScalars
                  (algebraMap Γ(X, U)
                    (Localization.AtPrime (hU.primeIdealOf x).asIdeal))).obj ω)

Stacks.Duality.isGorensteinLocalRing_stalk_iff_isInvertible_derivedStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/StalkwiseInvertible.lean, line 185. The attribute's comment: “(1)(b): the local ring at a point is Gorenstein iff the derived stalk of the dualizing complex is invertible”.

On a locally Noetherian scheme carrying a dualizing complex K, the local ring at x is Gorenstein exactly when the derived stalk K_x is an invertible object of D(𝒪_{X,x}).

public theorem isGorensteinLocalRing_stalk_iff_isInvertible_derivedStalk
    [HasDerivedCategory.{u + 1} X.Modules] (K : DerivedCategory X.Modules)
    (hK : IsDualizingComplex K) (x : X) :
    letI := HasDerivedCategory.standard (ModuleCat.{u} (X.presheaf.stalk x))
    letI := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory
      (X.presheaf.stalk x)).choose
    Dualizing.IsGorensteinLocalRing (X.presheaf.stalk x) ↔
      MonoidalCategory.IsInvertible ((AlgebraicGeometry.derivedStalkFunctor x).obj K)

Stacks.Duality.exists_isDualizingComplex_iff_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/StructureSheafDualizing.lean, line 84. The attribute's comment: “(2): a Gorenstein scheme has a dualizing complex iff its structure sheaf is one”.

A Gorenstein scheme has a dualizing complex if and only if its structure sheaf, placed in degree zero, is a dualizing complex.

public theorem exists_isDualizingComplex_iff_unit [AlgebraicGeometry.IsGorenstein X]
    [HasDerivedCategory.{w} X.Modules] :
    (∃ K : DerivedCategory X.Modules, IsDualizingComplex K) ↔
      IsDualizingComplex ((DerivedCategory.singleFunctor X.Modules 0).obj
        (SheafOfModules.unit X.ringCatSheaf))

Tag 0BVA, a lemma

Tag 0BVA in the Stacks Project.

AlgebraicGeometry.isGorenstein_of_isLocalCompleteIntersectionMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/LocalCompleteIntersection.lean, line 118.

A local complete intersection morphism whose target is a Gorenstein scheme has Gorenstein source.

public theorem isGorenstein_of_isLocalCompleteIntersectionMorphism {X Y : Scheme.{u}} (f : Y ⟶ X)
    (hf : IsLocalCompleteIntersectionMorphism f) (hX : IsGorenstein X) : IsGorenstein Y

Tag 0C01, a lemma

Tag 0C01 in the Stacks Project.

AlgebraicGeometry.isGorenstein_isLocal_syntomic, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Gorenstein.lean, line 71.

Stacks Project, Tag 0C01. Being Gorenstein is local for syntomic coverings.

instance isGorenstein_isLocal_syntomic :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => IsGorenstein X)
      (Scheme.precoverage @Syntomic)

Sources

• Section 48.24, Tag 0AWV
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isGorenstein_Spec_iff · AlgebraicGeometry.IsGorenstein · AlgebraicGeometry.isCohenMacaulay_of_isGorenstein · AlgebraicGeometry.isGorenstein_of_isRegular · Stacks.Duality.isGorenstein_iff_isInvertible_dualizingComplex · Stacks.Duality.isGorenstein_iff_hasInvertibleDualizingModelOn · Stacks.Duality.isGorenstein_iff_isInvertible_dualizingModel · Stacks.Duality.exists_isOpen_isGorenstein

Section48.25 Gorenstein morphisms#

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

Tag 0C03, a lemma

Tag 0C03 in the Stacks Project.

AlgebraicGeometry.isGorensteinLocalRing_stalk_iff_of_essFiniteType_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/FieldExtension.lean, line 306. The attribute's comment: “finitely generated field extension”.

Stacks Project, Tag 0C03. Gorensteinness of local rings is unchanged after a finitely generated extension of the ground field of a locally Noetherian scheme.

public theorem isGorensteinLocalRing_stalk_iff_of_essFiniteType_fieldExtension
    (k K : Type u) [Field k] [Field K] [Algebra k K] [Algebra.EssFiniteType k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [IsLocallyNoetherian X] (x : X)
    (x' : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}))
    (hx' : (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base x' = x) :
    letI : IsLocallyNoetherian
        (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}) :=
      (AlgebraicGeometry.isLocallyNoetherian_baseChange_iff k K X f).mp inferInstance
    Dualizing.IsGorensteinLocalRing (X.presheaf.stalk x) ↔
      Dualizing.IsGorensteinLocalRing
        ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}).presheaf.stalk
          x')

AlgebraicGeometry.isGorensteinLocalRing_stalk_iff_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinSchemes/FieldExtension.lean, line 389. The attribute's comment: “arbitrary field extension for a locally finite type scheme”.

Stacks Project, Tag 0C03. Gorensteinness of local rings is unchanged after an arbitrary extension of the ground field when the scheme is locally of finite type over that field.

public theorem isGorensteinLocalRing_stalk_iff_of_locallyOfFiniteType
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] (x : X)
    (x' : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}))
    (hx' : (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base x' = x) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    Dualizing.IsGorensteinLocalRing (X.presheaf.stalk x) ↔
      Dualizing.IsGorensteinLocalRing
        ((pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u}).presheaf.stalk
          x')

Tag 0C04, a definition

Tag 0C04 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.IsGorensteinAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Basic.lean, line 38. The attribute's comment: “part (1)”.

A scheme morphism with locally Noetherian fibres is Gorenstein at x if it is flat at x and the local ring of the fibre over f x is Gorenstein.

public abbrev IsGorensteinAt {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) (x : X) : Prop

AlgebraicGeometry.Scheme.Hom.IsGorenstein, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Basic.lean, line 48. The attribute's comment: “part (2)”.

A scheme morphism with locally Noetherian fibres is Gorenstein when it is Gorenstein at every point of the source.

public abbrev IsGorenstein {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) : Prop

Tag 0C05, a lemma

Tag 0C05 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isGorenstein_iff_flat_and_isGorenstein_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Fibres.lean, line 70.

A morphism of schemes with locally Noetherian fibres is Gorenstein if and only if it is flat and all of its fibres are Gorenstein schemes.

public theorem isGorenstein_iff_flat_and_isGorenstein_fiber
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) :
    IsGorenstein f hf ↔ Flat f ∧ ∀ y : Y, AlgebraicGeometry.IsGorenstein (f.fiber y)

Tag 0C06, a lemma

Tag 0C06 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isCohenMacaulay_of_isGorenstein, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/CohenMacaulay.lean, line 46.

Stacks Project, Tag 0C06. A Gorenstein morphism is Cohen--Macaulay.

public theorem isCohenMacaulay_of_isGorenstein
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) (h : IsGorenstein f hf) :
    IsCohenMacaulay f hf

Tag 0C15, a lemma

Tag 0C15 in the Stacks Project.

AlgebraicGeometry.isGorenstein_of_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Syntomic.lean, line 110. The attribute's comment: “a syntomic morphism is Gorenstein”.

Stacks 0C15. A syntomic morphism of schemes is a Gorenstein morphism.

public theorem isGorenstein_of_syntomic {X S : Scheme.{u}} (f : X ⟶ S) (hf : Syntomic f) :
    f.IsGorenstein (isLocallyNoetherian_fiber_of_syntomic hf)

AlgebraicGeometry.isGorenstein_of_flat_of_isLocalCompleteIntersectionMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Syntomic.lean, line 120. The attribute's comment: “a flat local complete intersection morphism is Gorenstein”.

Stacks 0C15. A flat local complete intersection morphism of schemes is a Gorenstein morphism; this is the second formulation of the lemma, equivalent to the first by Stacks 069K.

public theorem isGorenstein_of_flat_of_isLocalCompleteIntersectionMorphism {X S : Scheme.{u}}
    (f : X ⟶ S) (hflat : Flat f) (hlci : IsLocalCompleteIntersectionMorphism f) :
    f.IsGorenstein (isLocallyNoetherian_fiber_of_syntomic
      (syntomic_of_flat_of_isLocalCompleteIntersectionMorphism hflat hlci))

AlgebraicGeometry.syntomic_le_gorensteinWithLocallyNoetherianFibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/SyntomicMorphismProperty.lean, line 62. The attribute's comment: “a syntomic morphism is Gorenstein, as an inclusion of morphism properties”.

Stacks 0C15. A syntomic morphism of schemes is a Gorenstein morphism: the syntomic morphisms are contained in the morphism property of having locally Noetherian fibres and being Gorenstein.

public theorem syntomic_le_gorensteinWithLocallyNoetherianFibers :
    (@Syntomic : MorphismProperty Scheme.{u}) ≤ gorensteinWithLocallyNoetherianFibers

AlgebraicGeometry.flat_inf_lci_le_gorensteinWithLocallyNoetherianFibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/SyntomicMorphismProperty.lean, line 71. The attribute's comment: “a flat lci morphism is Gorenstein, as an inclusion of morphism properties”.

Stacks 0C15. A flat local complete intersection morphism of schemes is a Gorenstein morphism: the meet of flatness and being a local complete intersection morphism is contained in the morphism property of having locally Noetherian fibres and being Gorenstein. This is the second formulation of the lemma, equivalent to the first by Stacks 069K.

public theorem flat_inf_lci_le_gorensteinWithLocallyNoetherianFibers :
    (@Flat ⊓ @IsLocalCompleteIntersectionMorphism : MorphismProperty Scheme.{u}) ≤
      gorensteinWithLocallyNoetherianFibers

Tag 0C11, a lemma

Tag 0C11 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isGorensteinAt_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Composition.lean, line 208. The attribute's comment: “part (1)”.

Gorensteinness at a point is preserved by composition.

public theorem isGorensteinAt_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
    (hg : ∀ z : Z, IsLocallyNoetherian (g.fiber z))
    (hfg : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z)) (x : X)
    (hfx : IsGorensteinAt f hf x) (hgy : IsGorensteinAt g hg (f x)) :
    IsGorensteinAt (f ≫ g) hfg x

AlgebraicGeometry.Scheme.Hom.isGorenstein_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Composition.lean, line 218. The attribute's comment: “part (2)”.

The composite of Gorenstein morphisms is Gorenstein.

public theorem isGorenstein_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
    (hg : ∀ z : Z, IsLocallyNoetherian (g.fiber z))
    (hfg : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z))
    (hF : IsGorenstein f hf) (hG : IsGorenstein g hg) :
    IsGorenstein (f ≫ g) hfg

AlgebraicGeometry.Scheme.Hom.isGorensteinAt_left_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Composition.lean, line 229. The attribute's comment: “part (3), first morphism”.

If a composite is Gorenstein at a point and the first map is flat there, then the first map is Gorenstein at that point.

public theorem isGorensteinAt_left_of_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
    (hg : ∀ z : Z, IsLocallyNoetherian (g.fiber z))
    (hfg : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z)) (x : X)
    (hcomp : IsGorensteinAt (f ≫ g) hfg x)
    (hflat : IsFlatAt f.toLRSHom.toShHom x) :
    IsGorensteinAt f hf x

AlgebraicGeometry.Scheme.Hom.isGorensteinAt_right_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Composition.lean, line 241. The attribute's comment: “part (3), second morphism”.

If a composite is Gorenstein at a point and the first map is flat there, then the second map is Gorenstein at the image point.

public theorem isGorensteinAt_right_of_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
    (hg : ∀ z : Z, IsLocallyNoetherian (g.fiber z))
    (hfg : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z)) (x : X)
    (hcomp : IsGorensteinAt (f ≫ g) hfg x)
    (hflat : IsFlatAt f.toLRSHom.toShHom x) :
    IsGorensteinAt g hg (f x)

AlgebraicGeometry.Scheme.Hom.isGorenstein_left_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Composition.lean, line 252. The attribute's comment: “part (4), first morphism”.

If the composite is Gorenstein and the first map is flat, the first map is Gorenstein.

public theorem isGorenstein_left_of_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
    (hg : ∀ z : Z, IsLocallyNoetherian (g.fiber z))
    (hfg : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z))
    (hcomp : IsGorenstein (f ≫ g) hfg) (hflat : Flat f) :
    IsGorenstein f hf

AlgebraicGeometry.Scheme.Hom.isGorensteinAt_image_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Composition.lean, line 263. The attribute's comment: “part (4), second morphism on the image”.

If the composite is Gorenstein and the first map is flat, the second map is Gorenstein at each point in the image of the first.

public theorem isGorensteinAt_image_of_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
    (hg : ∀ z : Z, IsLocallyNoetherian (g.fiber z))
    (hfg : ∀ z : Z, IsLocallyNoetherian ((f ≫ g).fiber z))
    (hcomp : IsGorenstein (f ≫ g) hfg) (hflat : Flat f) (x : X) :
    IsGorensteinAt g hg (f x)

Tag 0C12, a lemma

Tag 0C12 in the Stacks Project.

Stacks.Duality.isGorensteinLocalRing_stalk_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Dualizing.lean, line 135. The attribute's comment: “Gorenstein local rings of the base”.

Stacks Project, Tag 0C12. The local ring of the base at any point in the image of a flat morphism of locally Noetherian schemes with Gorenstein source is Gorenstein.

The map of local rings 𝒪_{Y, f x} → 𝒪_{X, x} induced by a flat morphism is a flat local homomorphism of Noetherian local rings, so isGorensteinLocalRing_of_flat applies.

theorem isGorensteinLocalRing_stalk_of_flat {X Y : Scheme.{u}} (f : X ⟶ Y)
    [AlgebraicGeometry.IsGorenstein X] [IsLocallyNoetherian Y] [Flat f] (x : X) :
    Dualizing.IsGorensteinLocalRing (Y.presheaf.stalk (f x))

Stacks.Duality.isGorenstein_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphismOfFlat.lean, line 85. The attribute's comment: “Gorenstein morphism”.

Stacks Project, Tag 0C12. A flat morphism of locally Noetherian schemes with Gorenstein source is a Gorenstein morphism.

The local Noetherianity of the fibres that Scheme.Hom.IsGorenstein requires is supplied here rather than assumed: it follows from local Noetherianity of the source.

theorem isGorenstein_of_flat {X Y : Scheme.{u}} (f : X ⟶ Y)
    [AlgebraicGeometry.IsGorenstein X] [IsLocallyNoetherian Y] [Flat f] :
    ∃ hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y),
      AlgebraicGeometry.Scheme.Hom.IsGorenstein f hf

Tag 0C07, a lemma

Tag 0C07 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isGorensteinAt_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/BaseChange.lean, line 298. The attribute's comment: “part (1)”.

Stacks Project, Tag 0C07 (1). Gorensteinness at a point is preserved under a base change locally of finite type.

public theorem isGorensteinAt_pullback {X Y Y' : Scheme.{u}}
    (f : X ⟶ Y) (g : Y' ⟶ Y) [LocallyOfFiniteType g]
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) (x' : (pullback f g : Scheme.{u}))
    (h : IsGorensteinAt f hf ((pullback.fst f g).base x')) :
    IsGorensteinAt (pullback.snd f g)
      (fun y' => isLocallyNoetherian_fiber_pullback f g hf y') x'

AlgebraicGeometry.Scheme.Hom.isGorensteinAt_of_pullback_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/BaseChange.lean, line 320. The attribute's comment: “part (2)”.

Stacks Project, Tag 0C07 (2). Gorensteinness descends from a base change locally of finite type when the original morphism is flat at the point in question.

public theorem isGorensteinAt_of_pullback_of_flat {X Y Y' : Scheme.{u}}
    (f : X ⟶ Y) (g : Y' ⟶ Y) [LocallyOfFiniteType g]
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) (x' : (pullback f g : Scheme.{u}))
    (hflat : IsFlatAt f.toLRSHom.toShHom ((pullback.fst f g).base x'))
    (h : IsGorensteinAt (pullback.snd f g)
      (fun y' => isLocallyNoetherian_fiber_pullback f g hf y') x') :
    IsGorensteinAt f hf ((pullback.fst f g).base x')

AlgebraicGeometry.Scheme.Hom.isGorensteinAt_of_pullback_of_flat_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/BaseChange.lean, line 342. The attribute's comment: “part (3)”.

Stacks Project, Tag 0C07 (3). Gorensteinness descends from a base change locally of finite type that is flat at the image of the point in the new base.

public theorem isGorensteinAt_of_pullback_of_flat_base {X Y Y' : Scheme.{u}}
    (f : X ⟶ Y) (g : Y' ⟶ Y) [LocallyOfFiniteType g]
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) (x' : (pullback f g : Scheme.{u}))
    (hflat : IsFlatAt g.toLRSHom.toShHom ((pullback.snd f g).base x'))
    (h : IsGorensteinAt (pullback.snd f g)
      (fun y' => isLocallyNoetherian_fiber_pullback f g hf y') x') :
    IsGorensteinAt f hf ((pullback.fst f g).base x')

Tag 0E0Q, a lemma

Tag 0E0Q in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.setOf_isGorensteinAt_pullback_eq_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/BaseChange.lean, line 457.

Stacks Project, Tag 0E0Q. Let f : X ⟶ Y be flat and locally of finite type, and let g : Y' ⟶ Y be an arbitrary morphism. Then the set of points of X ×_Y Y' at which the base change of f along g is Gorenstein is the inverse image, under the projection to X, of the set of points of X at which f is Gorenstein; that is, formation of the Gorenstein locus of f commutes with arbitrary base change.

public theorem setOf_isGorensteinAt_pullback_eq_preimage {X Y Y' : Scheme.{u}}
    (f : X ⟶ Y) (g : Y' ⟶ Y) [Flat f] [LocallyOfFiniteType f]
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y))
    (hf' : ∀ y' : Y', IsLocallyNoetherian ((pullback.snd f g).fiber y')) :
    {x' : (pullback f g : Scheme.{u}) | IsGorensteinAt (pullback.snd f g) hf' x'} =
      (pullback.fst f g).base ⁻¹' {x : X | IsGorensteinAt f hf x}

AlgebraicGeometry.Scheme.Hom.setOf_isGorensteinAt_pullback_eq_preimage_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/BaseChangeLocus.lean, line 55.

Let f : X ⟶ Y be flat and locally of finite type and let g : Y' ⟶ Y be an arbitrary morphism of schemes. Then the set of points of X ×_Y Y' at which the base change of f along g is Gorenstein is the inverse image, under the projection to X, of the set of points of X at which f is Gorenstein: formation of the Gorenstein locus of f commutes with arbitrary base change. The locally Noetherian fibres that the Gorenstein-at-a-point predicate needs as data are theorems here, so nothing is assumed beyond flatness of f and its being locally of finite type.

public theorem setOf_isGorensteinAt_pullback_eq_preimage_of_locallyOfFiniteType
    {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y) [Flat f] [LocallyOfFiniteType f] :
    {x' : (pullback f g : Scheme.{u}) |
        IsGorensteinAt (pullback.snd f g)
          (fun y' => LocallyOfFiniteType.isLocallyNoetherian
            ((pullback.snd f g).fiberToSpecResidueField y')) x'} =
      (pullback.fst f g).base ⁻¹'
        {x : X |
          IsGorensteinAt f
            (fun y => LocallyOfFiniteType.isLocallyNoetherian
              (f.fiberToSpecResidueField y)) x}

Tag 0C08, a lemma

Tag 0C08 in the Stacks Project.

Stacks.Duality.isGorensteinAt_iff_isGorensteinFiberStalkAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/FibreStalkCriterion.lean, line 52. The attribute's comment: “proof chain (1) ↔ (2); (2)↔…↔(6) needs 0A9Y, 0BZZ, 0BFQ invertibility”.

Stacks Project, Tag 0C08, the first equivalence of its proof. A flat morphism with locally Noetherian fibres is Gorenstein at a point exactly when the local ring of its fibre through that point is Gorenstein.

theorem isGorensteinAt_iff_isGorensteinFiberStalkAt (f : X ⟶ Y)
    (hf : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) [Flat f] (x : X) :
    f.IsGorensteinAt hf x ↔ IsGorensteinFiberStalkAt f hf x

Stacks.Duality.isGorensteinAt_iff_exists_isInvertible_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekChartConsequences.lean, line 54.

Let S be Noetherian, f : X ⟶ Y a flat morphism of FTS S and x ∈ X. Then f is Gorenstein at x if and only if f^!𝒪_Y is isomorphic to an invertible object in a neighbourhood of x. In particular the set of points where f is Gorenstein is open in X. Here f^! is computed at any compactification j.

theorem isGorensteinAt_iff_exists_isInvertible_upperShriek [Flat f.left] :
    (∀ x : X.left, f.left.IsGorensteinAt (isLocallyNoetherian_fiber_left f) x ↔
      ∃ W : X.left.Opens, x ∈ W ∧
        letI := Scheme.Modules.derivedMonoidal W.toScheme
        MonoidalCategory.IsInvertible
          ((Scheme.Modules.restrictFunctor W.ι).mapDerivedCategory.obj
            (relativeDualizingComplexObj f j))) ∧
      IsOpen {x : X.left | f.left.IsGorensteinAt (isLocallyNoetherian_fiber_left f) x}

Tag 0C09, a lemma

Tag 0C09 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isGorensteinAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/AffineSpace.lean, line 72. The attribute's comment: “the equivalence of (1), (2), (3) and (4)”.

Stacks Project, Tag 0C09. Let f : X ⟶ S be flat and locally of finite presentation, let x ∈ X and let d = dim_x(X_{f x}). The following are equivalent: 1. f is Gorenstein at x; 2. there are an open neighbourhood U of x and a locally quasi-finite morphism U ⟶ 𝔸ᵈ_S over S which is Gorenstein at x; 3. there are an open neighbourhood U of x and a locally quasi-finite Gorenstein morphism U ⟶ 𝔸ᵈ_S over S; 4. every S-morphism g : U ⟶ 𝔸ᵈ_S from an open neighbourhood U of x which is quasi-finite at x is Gorenstein at x.

theorem isGorensteinAt_tfae {X S : Scheme.{u}} (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] (x : X) (d : ℕ)
    (hd : topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = (d : WithBot ℕ∞)) :
    List.TFAE [
      f.IsGorensteinAt (isLocallyNoetherian_fiber_of_locallyOfFinitePresentation f) x,
      ∃ (U : X.Opens) (hx : x ∈ U) (g : U.toScheme ⟶ AffineSpace (ULift.{u} (Fin d)) S)
          (hg : g ≫ (AffineSpace (ULift.{u} (Fin d)) S ↘ S) = U.ι ≫ f),
        (LocallyOfFiniteType g ∧ LocallyQuasiFinite g) ∧
          g.IsGorensteinAt (isLocallyNoetherian_fiber_of_comp_eq hg) ⟨x, hx⟩,
      ∃ (U : X.Opens) (_ : x ∈ U) (g : U.toScheme ⟶ AffineSpace (ULift.{u} (Fin d)) S)
          (hg : g ≫ (AffineSpace (ULift.{u} (Fin d)) S ↘ S) = U.ι ≫ f),
        (LocallyOfFiniteType g ∧ LocallyQuasiFinite g) ∧
          g.IsGorenstein (isLocallyNoetherian_fiber_of_comp_eq hg),
      ∀ (U : X.Opens) (hx : x ∈ U) (g : U.toScheme ⟶ AffineSpace (ULift.{u} (Fin d)) S)
          (hg : g ≫ (AffineSpace (ULift.{u} (Fin d)) S ↘ S) = U.ι ≫ f),
        AlgebraicGeometry.quasiFiniteAt g ⟨x, hx⟩ →
          g.IsGorensteinAt (isLocallyNoetherian_fiber_of_comp_eq hg) ⟨x, hx⟩]

AlgebraicGeometry.Scheme.Hom.isOpen_setOf_isGorensteinAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/OpenLocus.lean, line 279. The attribute's comment: “the set of points where f is Gorenstein is open in X”.

Stacks Project, Tag 0C09, last assertion. For a flat morphism of schemes f : X ⟶ S locally of finite presentation, the set of points of X at which f is Gorenstein is open.

theorem isOpen_setOf_isGorensteinAt {X S : Scheme.{u}} (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] :
    IsOpen {x : X | IsGorensteinAt f
      (isLocallyNoetherian_fiber_of_locallyOfFinitePresentation f) x}

Tag 0C0A, a lemma

Tag 0C0A in the Stacks Project.

AlgebraicGeometry.gorensteinWithLocallyNoetherianFibers_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Locality.lean, line 130. The attribute's comment: “local in the fppf topology on the target”.

Stacks Project, Tag 0C0A. Having locally Noetherian fibres and being Gorenstein is local on the target for the fppf topology.

public instance gorensteinWithLocallyNoetherianFibers_isLocalAtTarget_fppf :
    (gorensteinWithLocallyNoetherianFibers : MorphismProperty Scheme.{u}).IsLocalAtTarget
      Scheme.fppfPrecoverage

AlgebraicGeometry.gorensteinWithLocallyNoetherianFibers_isLocalAtSource_syntomic, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GorensteinMorphisms/Locality.lean, line 188. The attribute's comment: “local in the syntomic topology on the source”.

Stacks Project, Tag 0C0A. Having locally Noetherian fibres and being Gorenstein is local on the source for the syntomic topology.

public instance gorensteinWithLocallyNoetherianFibers_isLocalAtSource_syntomic :
    (gorensteinWithLocallyNoetherianFibers : MorphismProperty Scheme.{u}).IsLocalAtSource
      (Scheme.precoverage (@Syntomic : MorphismProperty Scheme.{u}))

Sources

• Section 48.25, Tag 0C02
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isGorensteinLocalRing_stalk_iff_of_essFiniteType_fieldExtension · AlgebraicGeometry.isGorensteinLocalRing_stalk_iff_of_locallyOfFiniteType · AlgebraicGeometry.Scheme.Hom.IsGorensteinAt · AlgebraicGeometry.Scheme.Hom.IsGorenstein · AlgebraicGeometry.Scheme.Hom.isGorenstein_iff_flat_and_isGorenstein_fiber · AlgebraicGeometry.Scheme.Hom.isCohenMacaulay_of_isGorenstein · AlgebraicGeometry.isGorenstein_of_syntomic · AlgebraicGeometry.isGorenstein_of_flat_of_isLocalCompleteIntersectionMorphism

Section48.26 More on dualizing complexes#

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

Tag 0E4N, a lemma

Tag 0E4N in the Stacks Project.

Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_syntomic_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/DualizingComplexPullbackCriterion.lean, line 103. The attribute's comment: “case (1): f syntomic and surjective”.

Stacks Project, Tag 0E4N, case (1). Let f : X ⟶ Y be a syntomic surjective morphism of locally Noetherian schemes and let K be an object of D_QCoh(𝒪_Y). Then K is a dualizing complex on Y if and only if Lf^*K is a dualizing complex on X.

theorem isDualizingComplex_iff_derivedPullback_of_syntomic_of_surjective [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] (f : X ⟶ Y) [Surjective f] (hf : Syntomic f)
    (K : DerivedCategory Y.Modules)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor Y.Modules i).obj K).IsQuasicoherent) :
    IsDualizingComplex K ↔
      IsDualizingComplex
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          f.toLRSHom.toShHom).obj K)

Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_flat_lci_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/DualizingComplexPullbackCriterion.lean, line 123. The attribute's comment: “case (2): f a surjective flat local complete intersection morphism”.

Stacks Project, Tag 0E4N, case (2). Let f : X ⟶ Y be a surjective flat local complete intersection morphism of locally Noetherian schemes and let K be an object of D_QCoh(𝒪_Y). Then K is a dualizing complex on Y if and only if Lf^*K is a dualizing complex on X.

A flat local complete intersection morphism is syntomic ([Stacks, Tag 069K]), so this is case (1).

theorem isDualizingComplex_iff_derivedPullback_of_flat_lci_of_surjective [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] (f : X ⟶ Y) [Surjective f] [Flat f]
    (hlci : IsLocalCompleteIntersectionMorphism f) (K : DerivedCategory Y.Modules)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor Y.Modules i).obj K).IsQuasicoherent) :
    IsDualizingComplex K ↔
      IsDualizingComplex
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          f.toLRSHom.toShHom).obj K)

Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_isGorenstein_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/DualizingComplexPullbackCriterion.lean, line 142. The attribute's comment: “case (3): f a surjective Gorenstein morphism of finite type”.

Stacks Project, Tag 0E4N, case (3). Let f : X ⟶ Y be a surjective Gorenstein morphism of finite type of locally Noetherian schemes and let K be an object of D_QCoh(𝒪_Y). Then K is a dualizing complex on Y if and only if Lf^*K is a dualizing complex on X.

At an affine pair V ⊆ f⁻¹(U) on which f is still surjective, f.appLE U V is faithfully flat of finite type with Gorenstein fibre rings (Scheme.Hom.isGorensteinRing_fiber_appLE), and the ring-level statement is [Stacks, Tag 0E4D] case (3).

theorem isDualizingComplex_iff_derivedPullback_of_isGorenstein_of_surjective
    [IsLocallyNoetherian X] [IsLocallyNoetherian Y] (f : X ⟶ Y) [Surjective f] [QuasiCompact f]
    [LocallyOfFiniteType f]
    (hGor : Scheme.Hom.IsGorenstein f (isLocallyNoetherian_fiber_of_locallyOfFiniteType f))
    (K : DerivedCategory Y.Modules)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor Y.Modules i).obj K).IsQuasicoherent) :
    IsDualizingComplex K ↔
      IsDualizingComplex
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          f.toLRSHom.toShHom).obj K)

Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/DualizingComplexSyntomicDescent.lean, line 501. The attribute's comment: “variant: case (1) with a polynomial presentation p, the invertibility hInv and the tensor formula hTensor at each affine pair as explicit parameters; the tag is Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_syntomic_of_surjective”.

Stacks Project, Tag 0E4N, case (1). Let f : X ⟶ Y be a syntomic surjection of locally Noetherian schemes and let K be an object of D_QCoh(𝒪_Y). Then K is a dualizing complex on Y if and only if Lf^*K is a dualizing complex on X.

Over an affine open U ⊆ Y and an affine open V ⊆ f⁻¹(U) on which f is still surjective the condition becomes the ring-level statement [Stacks, Tag 0E4D] for f.appLE U V, which is syntomic and surjective on spectra; the two sides are compared by the affine comparison square of [Stacks, Tag 08DW] and the globalisation is [Stacks, Tag 0A86].

theorem isDualizingComplex_iff_derivedPullback_of_syntomic [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] (f : X ⟶ Y) [Surjective f] (hf : Syntomic f)
    (p : ∀ (U : Y.affineOpens) (V : X.affineOpens) (hVU : V.1 ≤ f ⁻¹ᵁ U.1),
      Dualizing.PolynomialPresentation (f.appLE U.1 V.1 hVU).hom)
    (hInv : ∀ (U : Y.affineOpens) (V : X.affineOpens) (hVU : V.1 ≤ f ⁻¹ᵁ U.1),
      letI : IsNoetherianRing Γ(Y, U.1) := IsLocallyNoetherian.component_noetherian U
      letI : IsNoetherianRing Γ(X, V.1) := IsLocallyNoetherian.component_noetherian V
      letI := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory
        Γ(X, V.1)).choose
      MonoidalCategory.IsInvertible (Dualizing.relativeDualizingUnit (p U V hVU)))
    (hTensor : ∀ (U : Y.affineOpens) (V : X.affineOpens) (hVU : V.1 ≤ f ⁻¹ᵁ U.1)
      (M : DerivedCategory (ModuleCat.{u} Γ(Y, U.1))),
      letI : IsNoetherianRing Γ(Y, U.1) := IsLocallyNoetherian.component_noetherian U
      letI : IsNoetherianRing Γ(X, V.1) := IsLocallyNoetherian.component_noetherian V
      letI := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory
        Γ(X, V.1)).choose
      Nonempty ((p U V hVU).upperShriekFunctor.{u, u}.obj M ≅
        ((derivedExtensionScalarsGeneral.{u, u, u}
            (f.appLE U.1 V.1 hVU).hom).functor.obj M) ⊗
          Dualizing.relativeDualizingUnit (p U V hVU)))
    (K : DerivedCategory Y.Modules)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor Y.Modules i).obj K).IsQuasicoherent) :
    IsDualizingComplex K ↔
      IsDualizingComplex ((derivedPullback f.toLRSHom.toShHom).obj K)

Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_flat_lci, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/DualizingComplexSyntomicDescent.lean, line 549. The attribute's comment: “variant: case (2) with a polynomial presentation p, the invertibility hInv and the tensor formula hTensor at each affine pair as explicit parameters; the tag is Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_flat_lci_of_surjective”.

Stacks Project, Tag 0E4N, case (2). Let f : X ⟶ Y be a surjective flat local complete intersection morphism of locally Noetherian schemes and let K be an object of D_QCoh(𝒪_Y). Then K is a dualizing complex on Y if and only if Lf^*K is a dualizing complex on X.

A flat local complete intersection morphism is syntomic by [Stacks, Tag 069K], so this is case (1).

theorem isDualizingComplex_iff_derivedPullback_of_flat_lci [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] (f : X ⟶ Y) [Surjective f] [Flat f]
    (hlci : IsLocalCompleteIntersectionMorphism f)
    (p : ∀ (U : Y.affineOpens) (V : X.affineOpens) (hVU : V.1 ≤ f ⁻¹ᵁ U.1),
      Dualizing.PolynomialPresentation (f.appLE U.1 V.1 hVU).hom)
    (hInv : ∀ (U : Y.affineOpens) (V : X.affineOpens) (hVU : V.1 ≤ f ⁻¹ᵁ U.1),
      letI : IsNoetherianRing Γ(Y, U.1) := IsLocallyNoetherian.component_noetherian U
      letI : IsNoetherianRing Γ(X, V.1) := IsLocallyNoetherian.component_noetherian V
      letI := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory
        Γ(X, V.1)).choose
      MonoidalCategory.IsInvertible (Dualizing.relativeDualizingUnit (p U V hVU)))
    (hTensor : ∀ (U : Y.affineOpens) (V : X.affineOpens) (hVU : V.1 ≤ f ⁻¹ᵁ U.1)
      (M : DerivedCategory (ModuleCat.{u} Γ(Y, U.1))),
      letI : IsNoetherianRing Γ(Y, U.1) := IsLocallyNoetherian.component_noetherian U
      letI : IsNoetherianRing Γ(X, V.1) := IsLocallyNoetherian.component_noetherian V
      letI := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory
        Γ(X, V.1)).choose
      Nonempty ((p U V hVU).upperShriekFunctor.{u, u}.obj M ≅
        ((derivedExtensionScalarsGeneral.{u, u, u}
            (f.appLE U.1 V.1 hVU).hom).functor.obj M) ⊗
          Dualizing.relativeDualizingUnit (p U V hVU)))
    (K : DerivedCategory Y.Modules)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor Y.Modules i).obj K).IsQuasicoherent) :
    IsDualizingComplex K ↔
      IsDualizingComplex ((derivedPullback f.toLRSHom.toShHom).obj K)

Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_gorenstein, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/DualizingComplexSyntomicDescent.lean, line 589. The attribute's comment: “variant: case (3) with a polynomial presentation p, the fibre-ring Gorenstein property hGorRing and the tensor formula hTensor at each affine pair as explicit parameters; the tag is Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_isGorenstein_of_surjective”.

Stacks Project, Tag 0E4N, case (3). Let f : X ⟶ Y be a surjective Gorenstein morphism of finite type of locally Noetherian schemes and let K be an object of D_QCoh(𝒪_Y). Then K is a dualizing complex on Y if and only if Lf^*K is a dualizing complex on X.

A Gorenstein morphism is flat, and of finite type over a locally Noetherian target it is of finite presentation, so the reduction to affine pairs of case (1) applies verbatim; at an affine pair the ring-level statement is [Stacks, Tag 0E4D] case (3).

theorem isDualizingComplex_iff_derivedPullback_of_gorenstein [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] (f : X ⟶ Y) [Surjective f] [QuasiCompact f] [LocallyOfFiniteType f]
    (hF : ∀ y : Y, IsLocallyNoetherian (f.fiber y)) (hGor : Scheme.Hom.IsGorenstein f hF)
    (p : ∀ (U : Y.affineOpens) (V : X.affineOpens) (hVU : V.1 ≤ f ⁻¹ᵁ U.1),
      letI : Algebra Γ(Y, U.1) Γ(X, V.1) := (f.appLE U.1 V.1 hVU).hom.toAlgebra
      Dualizing.PolynomialPresentation (algebraMap Γ(Y, U.1) Γ(X, V.1)))
    (hGorRing : ∀ (U : Y.affineOpens) (V : X.affineOpens) (hVU : V.1 ≤ f ⁻¹ᵁ U.1)
      (q : Ideal Γ(Y, U.1)) [q.IsPrime],
      letI : Algebra Γ(Y, U.1) Γ(X, V.1) := (f.appLE U.1 V.1 hVU).hom.toAlgebra
      letI := Dualizing.isNoetherianRing_baseChange q.ResidueField (p U V hVU)
      Dualizing.IsGorensteinRing (q.Fiber Γ(X, V.1)))
    (hTensor : ∀ (U : Y.affineOpens) (V : X.affineOpens) (hVU : V.1 ≤ f ⁻¹ᵁ U.1)
      (M : DerivedCategory (ModuleCat.{u} Γ(Y, U.1))),
      letI : IsNoetherianRing Γ(Y, U.1) := IsLocallyNoetherian.component_noetherian U
      letI : IsNoetherianRing Γ(X, V.1) := IsLocallyNoetherian.component_noetherian V
      letI : Algebra Γ(Y, U.1) Γ(X, V.1) := (f.appLE U.1 V.1 hVU).hom.toAlgebra
      letI := (DerivedCategory.Invertible.derivedCategory_symmetricMonoidalCategory
        Γ(X, V.1)).choose
      Nonempty ((p U V hVU).upperShriekFunctor.{u, u}.obj M ≅
        ((derivedExtensionScalarsGeneral.{u, u, u}
            (algebraMap Γ(Y, U.1) Γ(X, V.1))).functor.obj M) ⊗
          Dualizing.relativeDualizingUnit (p U V hVU)))
    (K : DerivedCategory Y.Modules)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor Y.Modules i).obj K).IsQuasicoherent) :
    IsDualizingComplex K ↔
      IsDualizingComplex ((derivedPullback f.toLRSHom.toShHom).obj K)

Sources

• Section 48.26, Tag 0E4M
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Duality.isDualizingComplex_iff_derivedPullback_of_syntomic_of_surjective · Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_flat_lci_of_surjective · Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_isGorenstein_of_surjective · Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_syntomic · Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_flat_lci · Stacks.Duality.isDualizingComplex_iff_derivedPullback_of_gorenstein

Section48.27 Duality for proper schemes over fields#

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

Tag 0FVV, a lemma

Tag 0FVV in the Stacks Project.

Stacks.Duality.dualityEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/Duality.lean, line 364. The attribute's comment: “part (5): the isomorphisms Ext^i_X(K, ω_X) = Hom_k(H^{-i}(X, K), k)”.

The duality isomorphisms. Let X be a proper scheme over a field k and ω_X^• = a(𝒪_{Spec k}) its relative dualizing complex. For K in D_QCoh(𝒪_X) and every i there is a k-linear isomorphism Ext^i_X(K, ω_X^•) ≅ Hom_k(H^{-i}(X, K), k), sending α to t ∘ H^{-i}(X, α) with t : H⁰(X, ω_X^•) ⟶ k the trace (Stacks.Duality.traceOverField); it is natural in K (Stacks.Duality.dualityEquiv_comp) and compatible with shifts and distinguished triangles (Stacks.Duality.dualityEquiv_shiftedHomComp, Stacks.Duality.dualityEquiv_triangle).

def dualityEquiv (K : quasiCoherentDerivedCategory X) (i : ℤ) :
    letI := Scheme.linearOver f
    DerivedCategory.Ext K.obj (ωX).obj i ≃ₗ[k]
      ((DerivedCategory.homologyFunctor (ModuleCat k) (-i)).obj
        ((derivedGlobalSectionsOver f).obj K.obj) →ₗ[k] k)

Stacks.Duality.dualityEquiv_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/Duality.lean, line 386. The attribute's comment: “part (5): the isomorphisms are functorial in K”.

Part (5) of [Stacks, Tag 0FVV], functoriality. The duality isomorphisms are natural in K: for g : K ⟶ L in D(𝒪_X) and α ∈ Ext^i_X(L, ω_X^•), the linear form attached to g ≫ α is the one attached to α precomposed with H^{-i}(X, g).

theorem dualityEquiv_comp (K L : quasiCoherentDerivedCategory X) (i : ℤ) (g : K.obj ⟶ L.obj)
    (α : DerivedCategory.Ext L.obj (ωX).obj i)
    (x : (DerivedCategory.homologyFunctor (ModuleCat k) (-i)).obj
      ((derivedGlobalSectionsOver f).obj K.obj)) :
    letI := Scheme.linearOver f
    dualityEquiv f K i (g ≫ α) x =
      dualityEquiv f L i α
        ((DerivedCategory.homologyFunctor (ModuleCat k) (-i)).map
          ((derivedGlobalSectionsOver f).map g) x)

Stacks.Duality.dualityEquiv_shiftedHomComp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/Duality.lean, line 406. The attribute's comment: “part (5): compatibility with shifts and distinguished triangles”.

Part (5) of [Stacks, Tag 0FVV], compatibility with shifted morphisms. For β ∈ Ext^j_X(L, K) and α ∈ Ext^i_X(K, ω_X^•), the linear form on H^{-(i+j)}(X, L) attached to the product β.comp α ∈ Ext^{i+j}_X(L, ω_X^•) is the one attached to α precomposed with the map H^{-(i+j)}(X, L) ⟶ H^{-i}(X, K) induced by β. Taking for β the identity of K⟦n⟧ gives compatibility with shifts (Stacks.Duality.dualityLinearMap_shift), and taking for β the third morphism of a distinguished triangle gives compatibility with its connecting maps (Stacks.Duality.dualityLinearMap_triangle).

theorem dualityEquiv_shiftedHomComp (K L : quasiCoherentDerivedCategory X) {i j c : ℤ}
    (β : DerivedCategory.Ext L.obj K.obj j) (α : DerivedCategory.Ext K.obj (ωX).obj i)
    (h : i + j = c)
    (x : (DerivedCategory.homologyFunctor (ModuleCat k) (-c)).obj
      ((derivedGlobalSectionsOver f).obj L.obj)) :
    letI := Scheme.linearOver f
    dualityEquiv f L c (β.comp α h) x =
      dualityEquiv f K i α ((HX).shiftMap β (-c) (-i) (by omega) x)

Stacks.Duality.dualityLinearMap_shift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/Duality.lean, line 423. The attribute's comment: “part (5): compatibility with shifts”.

Compatibility of the duality map with shifts. Under Ext^\{i+n}\_X(K⟦n⟧, ω\_X^•) = Ext^i\_X(K, ω\_X^•) (composition with the identity of K⟦n⟧, an element of Ext^n\_X(K⟦n⟧, K)) and the canonical isomorphism H^{-(i+n)}(X, K⟦n⟧) ≅ H^{-i}(X, K), the duality maps of K⟦n⟧ and of K agree.

theorem dualityLinearMap_shift (K : DerivedCategory X.Modules) (i n : ℤ)
    (α : DerivedCategory.Ext K (ωX).obj i)
    (x : (DerivedCategory.homologyFunctor (ModuleCat k) (-(i + n))).obj
      ((derivedGlobalSectionsOver f).obj (K⟦n⟧))) :
    letI := Scheme.linearOver f
    dualityLinearMap f (K⟦n⟧) (i + n)
        (ShiftedHom.comp (𝟙 (K⟦n⟧)) α rfl) x =
      dualityLinearMap f K i α
        (((HX).shiftIso n (-(i + n)) (-i) (by omega)).hom.app K x)

Stacks.Duality.dualityLinearMap_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/Duality.lean, line 441. The attribute's comment: “part (5): compatibility with distinguished triangles”.

Compatibility of the duality map with distinguished triangles. For a triangle K ⟶ L ⟶ M ⟶ K⟦1⟧ of D(𝒪_X), the duality maps intertwine composition with its third morphism, Ext^i_X(K, ω_X^•) ⟶ Ext^{i+1}_X(M, ω_X^•), and the connecting morphism H^{-(i+1)}(X, M) ⟶ H^{-i}(X, K) of the long exact cohomology sequence.

theorem dualityLinearMap_triangle (T : Pretriangulated.Triangle (DerivedCategory X.Modules))
    (i : ℤ) (α : DerivedCategory.Ext T.obj₁ (ωX).obj i)
    (x : (DerivedCategory.homologyFunctor (ModuleCat k) (-(i + 1))).obj
      ((derivedGlobalSectionsOver f).obj T.obj₃)) :
    letI := Scheme.linearOver f
    dualityLinearMap f T.obj₃ (i + 1)
        (ShiftedHom.comp (T.mor₃ : DerivedCategory.Ext T.obj₃ T.obj₁ 1) α rfl) x =
      dualityLinearMap f T.obj₁ i α
        ((HX).homologySequenceδ T (-(i + 1)) (-i) (by omega) x)

Stacks.Duality.isDualizingComplex_relativeDualizingComplex_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/DualizingComplex.lean, line 75. The attribute's comment: “existence: ω_X^• = a(O_{Spec k}) is a dualizing complex”.

[Stacks, Tag 0FVV], existence. For X proper over a field k, the complex ω_X^• = a(𝒪_{Spec k}) is a dualizing complex on X.

theorem isDualizingComplex_relativeDualizingComplex_of_isProper :
    letI := LocallyOfFiniteType.isLocallyNoetherian f
    IsDualizingComplex (relativeDualizingComplex f
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
      (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))).obj

Stacks.Duality.le_zero_and_le_dim_of_not_isZero_homology_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/DualizingComplex.lean, line 85. The attribute's comment: “part (1): H^i(ω_X^•) is nonzero only for i ∈ [-dim X, 0]”.

[Stacks, Tag 0FVV], part (1). H^i(ω_X^•) is nonzero only for i ∈ [-dim X, 0].

theorem le_zero_and_le_dim_of_not_isZero_homology_of_isProper (i : ℤ)
    (hi : ¬ Limits.IsZero ((DerivedCategory.homologyFunctor X.Modules i).obj
      (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))).obj)) :
    i ≤ 0 ∧ (((-i).toNat : ℕ) : WithBot ℕ∞) ≤ topologicalKrullDim X

Stacks.Duality.relativeDualizingModule_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/DualizingComplex.lean, line 97. The attribute's comment: “part (2): ω_X is a coherent (S₂)-module supported on the components of dimension dim X”.

[Stacks, Tag 0FVV], part (2). ω_X = H^{-dim X}(ω_X^•) is a coherent module with property (S₂) whose support is the union of the irreducible components of dimension dim X.

theorem relativeDualizingModule_of_isProper :
    (relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))).IsCoherent ∧
    SheafHasPropertySk X (relativeDualizingModule f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))) 2 ∧
    _root_.SheafOfModules.supp (relativeDualizingModule f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))) =
      ⋃₀ {C ∈ irreducibleComponents X | topologicalKrullDim C = topologicalKrullDim X}

Stacks.Duality.topologicalKrullDim_supp_homology_le_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/DualizingComplex.lean, line 113. The attribute's comment: “part (3): dim Supp H^i(ω_X^•) ≤ -i”.

[Stacks, Tag 0FVV], part (3). The support of H^i(ω_X^•) has dimension at most -i (and is empty for i > 0).

theorem topologicalKrullDim_supp_homology_le_of_isProper (i : ℤ) :
    topologicalKrullDim (_root_.SheafOfModules.supp
        ((DerivedCategory.homologyFunctor X.Modules i).obj
          (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
            (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))).obj)) ≤
      if i ≤ 0 then (((-i).toNat : ℕ) : WithBot ℕ∞) else ⊥

Stacks.Duality.exists_nontrivial_stalk_homology_iff_depth_le_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/DualizingComplex.lean, line 126. The attribute's comment: “part (4): H^i(ω_{X,x}^•) ⊕ … ⊕ H^0(ω_{X,x}^•) ≠ 0 iff depth(O_{X,x}) ≤ -i, at closed points”.

[Stacks, Tag 0FVV], part (4). For x ∈ X closed, one of H^i(ω_{X,x}^•), …, H^0(ω_{X,x}^•) is nonzero if and only if depth(𝒪_{X,x}) ≤ -i.

theorem exists_nontrivial_stalk_homology_iff_depth_le_of_isProper {x : X}
    (hx : IsClosed ({x} : Set X)) (i : ℤ) :
    (∃ j : ℤ, i ≤ j ∧ j ≤ 0 ∧ Nontrivial (moduleStalkAtPoint
        ((DerivedCategory.homologyFunctor X.Modules j).obj
          (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
            (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))).obj) x)) ↔
      i ≤ 0 ∧ Module.depth (X.presheaf.stalk x) (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (X.presheaf.stalk x) ≤ ((-i).toNat : ℕ∞)

Stacks.Duality.dualizingModuleHomEquivOfIsProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/DualizingComplex.lean, line 150. The attribute's comment: “part (6): Hom(F, ω_X) = Hom_k(H^{dim X}(X, F), k) for F quasi-coherent”.

[Stacks, Tag 0FVV], part (6). For F quasi-coherent on X there is a k-linear isomorphism Hom_X(F, ω_X) ≅ Hom_k(H^{dim X}(X, F), k), natural in F (Stacks.Duality.dualizingModuleHomEquivOfIsProper_comp).

def dualizingModuleHomEquivOfIsProper (F : X.Modules) [F.IsQuasicoherent] :
    letI := Scheme.linearOver f
    (F ⟶ relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (CommRingCat.of k)))) ≃ₗ[k]
      (cohomologyOverField k f F (ENat.toNat ((topologicalKrullDim X).getD 0)) →ₗ[k] k)

Stacks.Duality.dualizingModuleHomEquivOfIsProper_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/DualizingComplex.lean, line 160. The attribute's comment: “part (6): the isomorphisms are functorial in F”.

[Stacks, Tag 0FVV], part (6), functoriality. The isomorphisms of part (6) are natural in the quasi-coherent module F.

theorem dualizingModuleHomEquivOfIsProper_comp {F G : X.Modules} [F.IsQuasicoherent]
    [G.IsQuasicoherent] (φ : F ⟶ G)
    (v : G ⟶ relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (CommRingCat.of k))))
    (x : cohomologyOverField k f F (ENat.toNat ((topologicalKrullDim X).getD 0))) :
    letI := Scheme.linearOver f
    dualizingModuleHomEquivOfIsProper f F (φ ≫ v) x =
      dualizingModuleHomEquivOfIsProper f G v
        ((cohomologyOverFieldFunctor k f (ENat.toNat ((topologicalKrullDim X).getD 0))).map
          φ x)

Stacks.Duality.boundedCoherent_relativeDualizingComplex_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/DualizingComplexCharacterization.lean, line 57. The attribute's comment: “footnote to part (5): ω_X^• is in D^b_Coh(O_X)”.

[Stacks, Tag 0FVV], footnote to part (5): ω_X^• lies in D^b_Coh(𝒪_X). Its cohomology sheaves are coherent ([Stacks, Tag 0A89]) and vanish outside [-dim X, 0] (part (1)).

theorem boundedCoherent_relativeDualizingComplex_of_isProper :
    DerivedCategoryB.derivedCategoryBBounded (A := X.Modules) (isCoherentSheaf X)
      (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))).obj

Stacks.Duality.existsUnique_iso_relativeDualizingComplex_of_quasiCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/DualizingComplexCharacterization.lean, line 127. The attribute's comment: “footnote to part (5): the isomorphisms characterize ω_X^• in D_QCoh(O_X) up to unique isomorphism”.

[Stacks, Tag 0FVV], footnote to part (5): the duality isomorphisms characterize ω_X^• in D_QCoh(𝒪_X) up to unique isomorphism. If ω ∈ D_QCoh(𝒪_X) has bijections Hom(K, ω) ≃ Hom_k(H⁰(X, K), k) natural in K ∈ D_QCoh(𝒪_X), then exactly one isomorphism ω ≅ ω_X^• carries them to the duality isomorphisms of ω_X^• (degree zero of part (5)).

theorem existsUnique_iso_relativeDualizingComplex_of_quasiCoherent
    (ω : quasiCoherentDerivedCategory X)
    (φ : ∀ K : quasiCoherentDerivedCategory X, (K.obj ⟶ ω.obj) ≃
      ((DerivedCategory.homologyFunctor (ModuleCat k) 0).obj
        ((derivedGlobalSectionsOver f).obj K.obj) ⟶ ModuleCat.of k k))
    (hφ : ∀ {K L : quasiCoherentDerivedCategory X} (g : K.obj ⟶ L.obj) (α : L.obj ⟶ ω.obj),
      φ K (g ≫ α) =
        (DerivedCategory.homologyFunctor (ModuleCat k) 0).map
          ((derivedGlobalSectionsOver f).map g) ≫ φ L α) :
    ∃! e : ω.obj ≅ (relativeDualizingComplex f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))).obj,
      ∀ (K : quasiCoherentDerivedCategory X) (α : K.obj ⟶ ω.obj),
        (DerivedCategory.homologyFunctor (ModuleCat k) 0).map
          ((derivedGlobalSectionsOver f).map (α ≫ e.hom)) ≫ traceOverField f = φ K α

Stacks.Duality.existsUnique_iso_relativeDualizingComplex_of_boundedCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/DualizingComplexCharacterization.lean, line 156. The attribute's comment: “footnote to part (5): ω_X^• is characterized by the isomorphisms for K in D^b_Coh(O_X)”.

[Stacks, Tag 0FVV], footnote to part (5): it suffices to consider K ∈ D^b_Coh(𝒪_X). If ω ∈ D^b_Coh(𝒪_X) has bijections Hom(K, ω) ≃ Hom_k(H⁰(X, K), k) natural in K ∈ D^b_Coh(𝒪_X), then exactly one isomorphism ω ≅ ω_X^• carries them to the duality isomorphisms of ω_X^•; this uses that ω_X^• lies in D^b_Coh(𝒪_X) (Stacks.Duality.boundedCoherent_relativeDualizingComplex_of_isProper).

theorem existsUnique_iso_relativeDualizingComplex_of_boundedCoherent
    (ω : DerivedCategory X.Modules)
    (hω : DerivedCategoryB.derivedCategoryBBounded (A := X.Modules) (isCoherentSheaf X) ω)
    (φ : ∀ K : DerivedCategory X.Modules,
      DerivedCategoryB.derivedCategoryBBounded (A := X.Modules) (isCoherentSheaf X) K →
      ((K ⟶ ω) ≃ ((DerivedCategory.homologyFunctor (ModuleCat k) 0).obj
        ((derivedGlobalSectionsOver f).obj K) ⟶ ModuleCat.of k k)))
    (hφ : ∀ {K L : DerivedCategory X.Modules}
      (hK : DerivedCategoryB.derivedCategoryBBounded (A := X.Modules) (isCoherentSheaf X) K)
      (hL : DerivedCategoryB.derivedCategoryBBounded (A := X.Modules) (isCoherentSheaf X) L)
      (g : K ⟶ L) (α : L ⟶ ω),
      φ K hK (g ≫ α) =
        (DerivedCategory.homologyFunctor (ModuleCat k) 0).map
          ((derivedGlobalSectionsOver f).map g) ≫ φ L hL α) :
    ∃! e : ω ≅ (relativeDualizingComplex f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))).obj,
      ∀ (K : DerivedCategory X.Modules)
        (hK : DerivedCategoryB.derivedCategoryBBounded (A := X.Modules) (isCoherentSheaf X) K)
        (α : K ⟶ ω),
        (DerivedCategory.homologyFunctor (ModuleCat k) 0).map
          ((derivedGlobalSectionsOver f).map (α ≫ e.hom)) ≫ traceOverField f = φ K hK α

Stacks.Duality.nonempty_relativeDualizingComplex_iso_and_relativeDualizingModule_iso_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/SmoothDualizingModule.lean, line 81. The attribute's comment: “part (7): for X smooth of relative dimension d over k, ω_X^• ≅ ∧^d Ω_{X/k}[d] and ω_X ≅ ∧^d Ω_{X/k}”.

[Stacks, Tag 0FVV], part (7). Let X be proper over a field k, with ω_X^• = a(𝒪_{Spec k}). If X ⟶ Spec k is smooth of relative dimension d, then ω_X^• ≅ ∧^d Ω_{X/k}[d] and ω_X ≅ ∧^d Ω_{X/k}.

theorem nonempty_relativeDualizingComplex_iso_and_relativeDualizingModule_iso_of_smooth
    {k : Type u} [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] (d : ℕ)
    [SmoothOfRelativeDimension d f] :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    Nonempty ((relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))).obj ≅
      (DerivedCategory.singleFunctor X.Modules (-d)).obj
        (Scheme.Modules.exteriorPower (Scheme.Hom.relativeDifferentials f) d)) ∧
    Nonempty (relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k))) ≅
      Scheme.Modules.exteriorPower (Scheme.Hom.relativeDifferentials f) d)

Tag 0FVW, a remark

Tag 0FVW in the Stacks Project.

Stacks.Duality.dualityEquiv_id_eq_traceOverField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/TracePairing.lean, line 190. The attribute's comment: “the identity of ω_X^• corresponds via 0FVV (5) to the trace t : H^0(X, ω_X^•) → k”.

The identity of ω_X^• corresponds to the trace. Under the isomorphism of part (5) of [Stacks, Tag 0FVV] in degree zero, Hom(ω_X^•, ω_X^•) ≅ Hom_k(H⁰(X, ω_X^•), k), the identity of ω_X^• is sent to the trace t : H⁰(X, ω_X^•) ⟶ k.

theorem dualityEquiv_id_eq_traceOverField :
    letI := Scheme.linearOver f
    dualityEquiv f ωX 0 (ShiftedHom.mk₀ (0 : ℤ) rfl (𝟙 (ωX).obj)) = (traceOverField f).hom

Stacks.Duality.dualityEquiv_mk₀_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/TracePairing.lean, line 202. The attribute's comment: “the degree-zero pairing Hom_X(K, ω_X^•) × H^0(X, K) → k, (α, β) ↦ t(α(β))”.

The degree-zero pairing. For K in D_QCoh(𝒪_X), the identification Hom(K, ω_X^•) ≅ H⁰(X, K)^∨ of part (5) of [Stacks, Tag 0FVV] is the pairing (α, β) ↦ t(α(β)), where α(β) is the image of β ∈ H⁰(X, K) under the map H⁰(X, K) ⟶ H⁰(X, ω_X^•) induced by α.

theorem dualityEquiv_mk₀_apply (K : quasiCoherentDerivedCategory X) (α : K.obj ⟶ (ωX).obj)
    (β : (H⁰).obj ((derivedGlobalSectionsOver f).obj K.obj)) :
    letI := Scheme.linearOver f
    dualityEquiv f K 0 (ShiftedHom.mk₀ (0 : ℤ) rfl α) β =
      (traceOverField f).hom (((H⁰).map ((derivedGlobalSectionsOver f).map α)).hom β)

Stacks.Duality.dualityEquiv_apply_eq_traceOverField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/TracePairing.lean, line 217. The attribute's comment: “the pairing Ext^i_X(K, ω_X^•) × H^{-i}(X, K) → k, (α, β) ↦ t(α(β)), with α a morphism K[-i] → ω_X^• and β in H^0(X, K[-i])”.

The pairing in degree i. For K in D_QCoh(𝒪_X) and i ∈ ℤ, the identification Ext^i_X(K, ω_X^•) ≅ H^{-i}(X, K)^∨ of part (5) of [Stacks, Tag 0FVV] is the pairing (α, β) ↦ t(α(β)): here α is regarded as a morphism K⟦-i⟧ ⟶ ω_X^• (extShiftHom), β as an element of H⁰(X, K⟦-i⟧) ≅ H^{-i}(X, K), and α(β) ∈ H⁰(X, ω_X^•) is the image of β under the map that α induces on H⁰(X, -).

theorem dualityEquiv_apply_eq_traceOverField (K : quasiCoherentDerivedCategory X) (i : ℤ)
    (α : DerivedCategory.Ext K.obj (ωX).obj i)
    (β : (DerivedCategory.homologyFunctor (ModuleCat k) (-i)).obj
      ((derivedGlobalSectionsOver f).obj K.obj)) :
    letI := Scheme.linearOver f
    dualityEquiv f K i α β =
      (traceOverField f).hom (((H⁰).map ((derivedGlobalSectionsOver f).map (extShiftHom α))).hom
        ((((HX).shiftIso (-i) 0 (-i) (add_zero _)).inv.app K.obj).hom β))

Stacks.Duality.bijective_dualityLinearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/TracePairing.lean, line 247. The attribute's comment: “the pairing identifies Ext^i_X(K, ω_X^•) with the k-linear dual of H^{-i}(X, K)”.

The pairing is nondegenerate on one side. For K in D_QCoh(𝒪_X) and every i, the pairing (α, β) ↦ t(α(β)) of Ext^i_X(K, ω_X^•) with H^{-i}(X, K) identifies Ext^i_X(K, ω_X^•) with the k-linear dual of H^{-i}(X, K).

theorem bijective_dualityLinearMap (K : quasiCoherentDerivedCategory X) (i : ℤ) :
    letI := Scheme.linearOver f
    Function.Bijective (dualityLinearMap f K.obj i)

Stacks.Duality.exists_not_bijective_dualityLinearMap_flip, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/TracePairing.lean, line 282. The attribute's comment: “the 'not vice versa' clause: on X = Spec k some K in D_QCoh has H^0(X, K) → Hom_X(K, ω_X^•)^∨ not bijective”.

The pairing is in general not nondegenerate on the other side (the clause "but in general not vice versa" of [Stacks, Tag 0FVW]). For every field k, on the proper scheme X = Spec k there is an object K of D_QCoh(𝒪_X) for which the other-side map H⁰(X, K) ⟶ Hom_X(K, ω_X^•)^∨, β ↦ (α ↦ t(α(β))), is not bijective: take for K the object with RΓ(X, K) = k^{(ℕ)}[0] ([Stacks, Tag 06Z0]), whose H⁰(X, K) = k^{(ℕ)} is infinite dimensional, so that the evaluation map into its double dual is not surjective.

theorem exists_not_bijective_dualityLinearMap_flip (k : Type u) [Field k] :
    ∃ K : quasiCoherentDerivedCategory (Spec (.of k)),
      letI := Scheme.linearOver (𝟙 (Spec (.of k)))
      ¬ Function.Bijective (dualityLinearMap (𝟙 (Spec (.of k))) K.obj 0).flip

Stacks.Duality.finiteDimensional_and_isPerfPair_of_coherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/TracePairing.lean, line 315. The attribute's comment: “K in D^b_Coh: Hom_X(K, ω_X^•), Ext^i_X(K, ω_X^•), H^i(X, K) are finite dimensional and the pairings are perfect”.

The coherent case. For K in D^b_Coh(𝒪_X), the k-vector spaces Hom_X(K, ω_X^•), Ext^i_X(K, ω_X^•) and H^n(X, K) are finite dimensional, and for every i the pairing Ext^i_X(K, ω_X^•) × H^{-i}(X, K) ⟶ k, (α, β) ↦ t(α(β)), is perfect.

theorem finiteDimensional_and_isPerfPair_of_coherent (K : DerivedCategory X.Modules)
    (hK : DerivedCategoryB.derivedCategoryBBounded (fun M : X.Modules => M.IsCoherent) K) :
    letI := Scheme.linearOver f
    FiniteDimensional k (K ⟶ (ωX).obj) ∧
      (∀ i : ℤ, FiniteDimensional k (DerivedCategory.Ext K (ωX).obj i)) ∧
      (∀ n : ℤ, FiniteDimensional k ((DerivedCategory.homologyFunctor (ModuleCat k) n).obj
        ((derivedGlobalSectionsOver f).obj K))) ∧
      ∀ i : ℤ, (dualityLinearMap f K i).IsPerfPair

Tag 0FVX, a remark

Tag 0FVX in the Stacks Project.

Stacks.Duality.coherentTracePairing_isPerfPair_and_dualMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/CoherentTracePairing.lean, line 114.

[Stacks, Tag 0FVX]. Let X be a proper scheme over a field k, ω_X^• and t : H⁰(X, ω_X^•) ⟶ k as in [Stacks, Tag 0FVW], and i ∈ ℤ. 1. For a coherent 𝒪_X-module ℱ, Ext^i_X(ℱ, ω_X^•) and H^{-i}(X, ℱ) are finite dimensional and the pairing ⟨α, β⟩ = t(α(β)) between them (α regarded as a morphism ℱ[-i] ⟶ ω_X^•, β as an element of H⁰(X, ℱ[-i])) is perfect. 2. For a homomorphism φ : ℱ ⟶ 𝒢 of coherent 𝒪_X-modules, ⟨α ∘ φ, β⟩ = ⟨α, φ(β)⟩ for α ∈ Ext^i_X(𝒢, ω_X^•) and β ∈ H^{-i}(X, ℱ). 3. For a homomorphism φ : ℱ ⟶ 𝒢 of quasi-coherent 𝒪_X-modules, the map Ext^i_X(𝒢, ω_X^•) ⟶ Ext^i_X(ℱ, ω_X^•) induced by φ is, via the identifications of Ext^i_X(-, ω_X^•) with H^{-i}(X, -)^∨ given by the pairings, the k-linear dual of the map H^{-i}(X, ℱ) ⟶ H^{-i}(X, 𝒢) induced by φ.

theorem coherentTracePairing_isPerfPair_and_dualMap (i : ℤ) :
    letI := Scheme.linearOver f
    (∀ F : X.Modules, F.IsCoherent →
      FiniteDimensional k (DerivedCategory.Ext ((single₀).obj F) (ωX).obj i) ∧
      FiniteDimensional k ((DerivedCategory.homologyFunctor (ModuleCat k) (-i)).obj
        ((derivedGlobalSectionsOver f).obj ((single₀).obj F))) ∧
      (dualityLinearMap f ((single₀).obj F) i).IsPerfPair ∧
      ∀ (α : DerivedCategory.Ext ((single₀).obj F) (ωX).obj i)
        (β : (DerivedCategory.homologyFunctor (ModuleCat k) (-i)).obj
          ((derivedGlobalSectionsOver f).obj ((single₀).obj F))),
        dualityLinearMap f ((single₀).obj F) i α β =
          (traceOverField f).hom
            (((H⁰).map ((derivedGlobalSectionsOver f).map (extShiftHom α))).hom
              ((((HX).shiftIso (-i) 0 (-i) (add_zero _)).inv.app ((single₀).obj F)).hom β))) ∧
    (∀ (F G : X.Modules) (φ : F ⟶ G), F.IsCoherent → G.IsCoherent →
      ∀ (α : DerivedCategory.Ext ((single₀).obj G) (ωX).obj i)
        (β : (DerivedCategory.homologyFunctor (ModuleCat k) (-i)).obj
          ((derivedGlobalSectionsOver f).obj ((single₀).obj F))),
        dualityLinearMap f ((single₀).obj F) i ((single₀).map φ ≫ α) β =
          dualityLinearMap f ((single₀).obj G) i α
            (((DerivedCategory.homologyFunctor (ModuleCat k) (-i)).map
              ((derivedGlobalSectionsOver f).map ((single₀).map φ))).hom β)) ∧
    ∀ (F G : X.Modules) (φ : F ⟶ G) (hF : F.IsQuasicoherent) (hG : G.IsQuasicoherent),
      (dualityEquiv f (singleQuasiCoherent F hF 0) i).toLinearMap ∘ₗ
          extPrecompLinearMap f ((single₀).map φ) i =
        ((DerivedCategory.homologyFunctor (ModuleCat k) (-i)).map
            ((derivedGlobalSectionsOver f).map ((single₀).map φ))).hom.dualMap ∘ₗ
          (dualityEquiv f (singleQuasiCoherent G hG 0) i).toLinearMap

Tag 0FVY, a lemma

Tag 0FVY in the Stacks Project.

Stacks.Duality.isPerfPair_dualityCupPairing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/PerfectPairing.lean, line 324. References: SGA 4½ Fonctions L (3.7), “special case”.

[Stacks, Tag 0FVY]. Let X be a proper scheme over a field k, with structure morphism f : X ⟶ Spec k, let ω_X^• be its dualizing complex of [Stacks, Tag 0FVV] and t : H⁰(X, ω_X^•) ⟶ k the trace of [Stacks, Tag 0FVW]. Let E ∈ D(𝒪_X) be perfect. Then for every i the pairing

Hⁱ(X, ω_X^• ⊗^𝐋 E^∨) × H⁻ⁱ(X, E) ⟶ k, (ξ, η) ↦ t((1 ⊗ ε)(ξ ∪ η))

is perfect: both spaces are finite-dimensional k-vector spaces and the pairing is a perfect pairing (LinearMap.IsPerfPair: each side is identified with the k-linear dual of the other). Here ∪ is the cup product of Cohomology, Section 0FKU (cupPairing at the canonical global cup product), E^∨ = R𝓗om(E, 𝒪_X) and ε : E^∨ ⊗^𝐋 E ⟶ 𝒪_X is the evaluation of Cohomology, Example 0FPC, and 1 ⊗ ε : (ω_X^• ⊗^𝐋 E^∨) ⊗^𝐋 E ⟶ ω_X^• is followed by the unit constraint (dualityCupPairing). The cohomology groups are the Γ(X, 𝒪_X)-modules of hypercohomology with the scalars restricted along k ⟶ Γ(X, 𝒪_X), and t is Stacks.Duality.traceOverField read on them (traceStd).

theorem isPerfPair_dualityCupPairing
    (hE : Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E) (i : ℤ) :
    FiniteDimensional k ((ModuleCat.restrictScalars.{u} (globalRingHom f)).obj
        (cohomologyModule (tensorDual X.toRingedSpace (dualizingComplexStd f) E) i)) ∧
      FiniteDimensional k
        ((ModuleCat.restrictScalars.{u} (globalRingHom f)).obj (cohomologyModule E (-i))) ∧
      (dualityCupPairing f E i).IsPerfPair

Tag 0FVZ, a lemma

Tag 0FVZ in the Stacks Project.

Stacks.Duality.isDualizingModuleOf_relativeDualizingModule_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/CohenMacaulay.lean, line 184. The attribute's comment: “part (1): ω_X is a dualizing module on X (Section 0AWH)”.

[Stacks, Tag 0FVZ], part (1). Let X be a proper scheme over a field k which is Cohen--Macaulay and equidimensional of dimension d. The module ω_X of [Stacks, Tag 0FVV] is a dualizing module on X in the sense of [Stacks, Section 0AWH]: ω_X^• is a dualizing complex, -d is the least degree in which it has nonzero cohomology, and ω_X = H^{-d}(ω_X^•).

theorem isDualizingModuleOf_relativeDualizingModule_of_isProper
    (hCM : AlgebraicGeometry.IsCohenMacaulay X) (hequi : TopologicalSpace.Equidimensional X)
    (d : ℕ) (hd : topologicalKrullDim X = d) :
    letI := LocallyOfFiniteType.isLocallyNoetherian f
    IsDualizingModuleOf ωM (ωX).obj (-(d : ℤ))

Stacks.Duality.relativeDualizingModule_isCoherent_cohenMacaulay_supp_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/CohenMacaulay.lean, line 218. The attribute's comment: “part (2): ω_X is a coherent Cohen-Macaulay module whose support is X”.

[Stacks, Tag 0FVZ], part (2). Let X be a proper scheme over a field k which is Cohen--Macaulay and equidimensional of dimension d. The module ω_X of [Stacks, Tag 0FVV] is a coherent Cohen--Macaulay 𝒪_X-module whose support is X.

theorem relativeDualizingModule_isCoherent_cohenMacaulay_supp_of_isProper
    (hCM : AlgebraicGeometry.IsCohenMacaulay X) (hequi : TopologicalSpace.Equidimensional X)
    (d : ℕ) (hd : topologicalKrullDim X = d) :
    (ωM).IsCoherent ∧ AlgebraicGeometry.SheafIsCohenMacaulay X ωM ∧
      _root_.SheafOfModules.supp ωM = Set.univ

Stacks.Duality.dualityEquivShiftOfIsProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/CohenMacaulay.lean, line 246. The attribute's comment: “part (3): the isomorphisms Ext^i_X(K, ω_X[d]) = Hom_k(H^{-i}(X, K), k)”.

[Stacks, Tag 0FVZ], part (3), the isomorphisms. Let X be a proper scheme over a field k which is Cohen--Macaulay and equidimensional of dimension d. For K in D_QCoh(𝒪_X) and every i there is a k-linear isomorphism Ext^i_X(K, ω_X[d]) ≅ Hom_k(H^{-i}(X, K), k). It is part (5) of [Stacks, Tag 0FVV] (Stacks.Duality.dualityEquiv) read through ω_X^• ≅ ω_X[d] (Stacks.Duality.relativeDualizingComplexIsoShiftOfIsProper); it is natural in K (Stacks.Duality.dualityEquivShiftOfIsProper_comp) and compatible with shifts and distinguished triangles (Stacks.Duality.dualityEquivShiftOfIsProper_shiftedHomComp, Stacks.Duality.dualityEquivShiftOfIsProper_shift, Stacks.Duality.dualityEquivShiftOfIsProper_triangle).

def dualityEquivShiftOfIsProper (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hequi : TopologicalSpace.Equidimensional X) (d : ℕ) (hd : topologicalKrullDim X = d)
    (K : quasiCoherentDerivedCategory X) (i : ℤ) :
    letI := Scheme.linearOver f
    DerivedCategory.Ext K.obj (((DerivedCategory.singleFunctor X.Modules 0).obj ωM)⟦(d : ℤ)⟧) i
      ≃ₗ[k] ((DerivedCategory.homologyFunctor (ModuleCat k) (-i)).obj
        ((derivedGlobalSectionsOver f).obj K.obj) →ₗ[k] k)

Stacks.Duality.dualityEquivShiftOfIsProper_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/CohenMacaulay.lean, line 277. The attribute's comment: “part (3): the isomorphisms are functorial in K”.

[Stacks, Tag 0FVZ], part (3), functoriality. The isomorphisms of part (3) are natural in K: for g : K ⟶ L and α ∈ Ext^i_X(L, ω_X[d]), the linear form attached to g ≫ α is the one attached to α precomposed with H^{-i}(X, g).

theorem dualityEquivShiftOfIsProper_comp (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hequi : TopologicalSpace.Equidimensional X) (d : ℕ) (hd : topologicalKrullDim X = d)
    (K L : quasiCoherentDerivedCategory X) (i : ℤ) (g : K.obj ⟶ L.obj)
    (α : DerivedCategory.Ext L.obj
      (((DerivedCategory.singleFunctor X.Modules 0).obj ωM)⟦(d : ℤ)⟧) i)
    (x : (DerivedCategory.homologyFunctor (ModuleCat k) (-i)).obj
      ((derivedGlobalSectionsOver f).obj K.obj)) :
    letI := Scheme.linearOver f
    dualityEquivShiftOfIsProper f hCM hequi d hd K i (g ≫ α) x =
      dualityEquivShiftOfIsProper f hCM hequi d hd L i α
        ((DerivedCategory.homologyFunctor (ModuleCat k) (-i)).map
          ((derivedGlobalSectionsOver f).map g) x)

Stacks.Duality.dualityEquivShiftOfIsProper_shiftedHomComp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/CohenMacaulay.lean, line 308. The attribute's comment: “part (3): compatibility with shifts and distinguished triangles”.

[Stacks, Tag 0FVZ], part (3), compatibility with shifted morphisms. For β ∈ Ext^j_X(L, K) and α ∈ Ext^i_X(K, ω_X[d]), the linear form on H^{-(i+j)}(X, L) attached to β.comp α ∈ Ext^{i+j}_X(L, ω_X[d]) is the one attached to α precomposed with the map H^{-(i+j)}(X, L) ⟶ H^{-i}(X, K) induced by β. This contains the compatibility with shifts (Stacks.Duality.dualityEquivShiftOfIsProper_shift) and with distinguished triangles (Stacks.Duality.dualityEquivShiftOfIsProper_triangle).

theorem dualityEquivShiftOfIsProper_shiftedHomComp (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hequi : TopologicalSpace.Equidimensional X) (d : ℕ) (hd : topologicalKrullDim X = d)
    (K L : quasiCoherentDerivedCategory X) {i j c : ℤ}
    (β : DerivedCategory.Ext L.obj K.obj j)
    (α : DerivedCategory.Ext K.obj
      (((DerivedCategory.singleFunctor X.Modules 0).obj ωM)⟦(d : ℤ)⟧) i)
    (h : i + j = c)
    (x : (DerivedCategory.homologyFunctor (ModuleCat k) (-c)).obj
      ((derivedGlobalSectionsOver f).obj L.obj)) :
    letI := Scheme.linearOver f
    dualityEquivShiftOfIsProper f hCM hequi d hd L c (β.comp α h) x =
      dualityEquivShiftOfIsProper f hCM hequi d hd K i α
        ((HX).shiftMap β (-c) (-i) (by omega) x)

Stacks.Duality.dualityEquivShiftOfIsProper_shift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/CohenMacaulay.lean, line 328. The attribute's comment: “part (3): compatibility with shifts”.

[Stacks, Tag 0FVZ], part (3), compatibility with shifts. Under Ext^{i+n}_X(K⟦n⟧, ω_X[d]) = Ext^i_X(K, ω_X[d]) (composition with the identity of K⟦n⟧) and H^{-(i+n)}(X, K⟦n⟧) ≅ H^{-i}(X, K), the isomorphisms of K⟦n⟧ and of K agree.

theorem dualityEquivShiftOfIsProper_shift (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hequi : TopologicalSpace.Equidimensional X) (d : ℕ) (hd : topologicalKrullDim X = d)
    (K : quasiCoherentDerivedCategory X) (i n : ℤ)
    (α : DerivedCategory.Ext K.obj
      (((DerivedCategory.singleFunctor X.Modules 0).obj ωM)⟦(d : ℤ)⟧) i)
    (x : (DerivedCategory.homologyFunctor (ModuleCat k) (-(i + n))).obj
      ((derivedGlobalSectionsOver f).obj (K.obj⟦n⟧))) :
    letI := Scheme.linearOver f
    dualityEquivShiftOfIsProper f hCM hequi d hd
        ⟨K.obj⟦n⟧, ObjectProperty.le_shift _ n K.obj K.property⟩ (i + n)
        (ShiftedHom.comp (𝟙 (K.obj⟦n⟧)) α rfl) x =
      dualityEquivShiftOfIsProper f hCM hequi d hd K i α
        (((HX).shiftIso n (-(i + n)) (-i) (by omega)).hom.app K.obj x)

Stacks.Duality.dualityEquivShiftOfIsProper_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/CohenMacaulay.lean, line 349. The attribute's comment: “part (3): compatibility with distinguished triangles”.

[Stacks, Tag 0FVZ], part (3), compatibility with distinguished triangles. For a triangle K ⟶ L ⟶ M ⟶ K⟦1⟧ in D_QCoh(𝒪_X), the isomorphisms intertwine composition with its third morphism, Ext^i_X(K, ω_X[d]) ⟶ Ext^{i+1}_X(M, ω_X[d]), and the connecting morphism H^{-(i+1)}(X, M) ⟶ H^{-i}(X, K) of the long exact cohomology sequence.

theorem dualityEquivShiftOfIsProper_triangle (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hequi : TopologicalSpace.Equidimensional X) (d : ℕ) (hd : topologicalKrullDim X = d)
    (T : Pretriangulated.Triangle (DerivedCategory X.Modules))
    (h₁ : DerivedCategoryB.derivedCategoryB (A := X.Modules)
      (SheafOfModules.isQuasicoherent X.ringCatSheaf) T.obj₁)
    (h₃ : DerivedCategoryB.derivedCategoryB (A := X.Modules)
      (SheafOfModules.isQuasicoherent X.ringCatSheaf) T.obj₃)
    (i : ℤ)
    (α : DerivedCategory.Ext T.obj₁
      (((DerivedCategory.singleFunctor X.Modules 0).obj ωM)⟦(d : ℤ)⟧) i)
    (x : (DerivedCategory.homologyFunctor (ModuleCat k) (-(i + 1))).obj
      ((derivedGlobalSectionsOver f).obj T.obj₃)) :
    letI := Scheme.linearOver f
    dualityEquivShiftOfIsProper f hCM hequi d hd ⟨T.obj₃, h₃⟩ (i + 1)
        (ShiftedHom.comp (T.mor₃ : DerivedCategory.Ext T.obj₃ T.obj₁ 1) α rfl) x =
      dualityEquivShiftOfIsProper f hCM hequi d hd ⟨T.obj₁, h₁⟩ i α
        ((HX).homologySequenceδ T (-(i + 1)) (-i) (by omega) x)

Stacks.Duality.dualizingModuleExtEquivOfIsProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/CohenMacaulay.lean, line 379. The attribute's comment: “part (4): Ext^{d-i}(F, ω_X) = Hom_k(H^i(X, F), k) for F quasi-coherent”.

[Stacks, Tag 0FVZ], part (4). Let X be a proper scheme over a field k which is Cohen--Macaulay and equidimensional of dimension d. For F a quasi-coherent 𝒪_X-module there are k-linear isomorphisms Ext^{d-i}_X(F, ω_X) ≅ Hom_k(H^i(X, F), k), natural in F (Stacks.Duality.dualizingModuleExtEquivOfIsProper_comp). It is part (3) for K = F[0] in degree -i, through Ext^{d-i}(F[0], ω_X[0]) = Ext^{-i}(F[0], ω_X[d]) and H^{-(-i)}(X, F[0]) = H^i(X, F).

def dualizingModuleExtEquivOfIsProper (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hequi : TopologicalSpace.Equidimensional X) (d : ℕ) (hd : topologicalKrullDim X = d)
    (F : X.Modules) [F.IsQuasicoherent] (i : ℕ) :
    letI := Scheme.linearOver f
    Abelian.zExt F ωM ((d : ℤ) - i) ≃ₗ[k] (cohomologyOverField k f F i →ₗ[k] k)

Stacks.Duality.dualizingModuleExtEquivOfIsProper_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/CohenMacaulay.lean, line 396. The attribute's comment: “part (4): the isomorphisms are functorial in F”.

[Stacks, Tag 0FVZ], part (4), functoriality. The isomorphisms of part (4) are natural in the quasi-coherent module F: for φ : F ⟶ G and α ∈ Ext^{d-i}_X(G, ω_X), the linear form attached to φ ≫ α is the one attached to α precomposed with H^i(X, φ).

theorem dualizingModuleExtEquivOfIsProper_comp (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hequi : TopologicalSpace.Equidimensional X) (d : ℕ) (hd : topologicalKrullDim X = d)
    {F G : X.Modules} [F.IsQuasicoherent] [G.IsQuasicoherent] (φ : F ⟶ G) (i : ℕ)
    (α : Abelian.zExt G ωM ((d : ℤ) - i)) (x : cohomologyOverField k f F i) :
    letI := Scheme.linearOver f
    dualizingModuleExtEquivOfIsProper f hCM hequi d hd F i
        ((DerivedCategory.singleFunctor X.Modules 0).map φ ≫ α) x =
      dualizingModuleExtEquivOfIsProper f hCM hequi d hd G i α
        ((cohomologyOverFieldFunctor k f i).map φ x)

Tag 0FW0, a remark

Tag 0FW0 in the Stacks Project.

Stacks.Duality.serrePairing_isPerfPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/SerreDualityLocallyFree.lean, line 599.

[Stacks, Tag 0FW0]. Let X be a proper Cohen--Macaulay scheme over a field k which is equidimensional of dimension d, let ω_X^• and ω_X be as in [Stacks, Tag 0FVV], so that ω_X^• = ω_X[d] by [Stacks, Tag 0FVZ], and let t : Hᵈ(X, ω_X) ⟶ k be the trace of [Stacks, Tag 0FVW] (Stacks.Duality.topTrace). Let ℰ be a finite locally free 𝒪_X-module with dual ℰ^∨. Then for all i + j = d the pairing

Hⁱ(X, ω_X ⊗_{𝒪_X} ℰ^∨) × Hʲ(X, ℰ) ⟶ k, (ξ, η) ↦ t((1 ⊗ ε)(ξ ∪ η))

(Stacks.Duality.serrePairing) is perfect, where ∪ is the cup product of Cohomology, Section 0FKU and ε : ℰ^∨ ⊗_{𝒪_X} ℰ ⟶ 𝒪_X is the evaluation map.

theorem serrePairing_isPerfPair (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hequi : TopologicalSpace.Equidimensional X) (d : ℕ) (hd : topologicalKrullDim X = d)
    (E : X.Modules) (hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E)
    (i j : ℤ) (hij : i + j = d) :
    (serrePairing f hCM hequi d hd E i j hij).IsPerfPair

Tag 0FW1, a lemma

Tag 0FW1 in the Stacks Project.

Stacks.Duality.nonempty_iso_relativeDualizing_of_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/ChangeOfField.lean, line 293. The attribute's comment: “(1): ω_X^• and ω_X are as in 0FVV for a factorization X → Spec k' → Spec k”.

Let X be proper over a field k with structure morphism f, and suppose f factors as f' ≫ g with f' : X ⟶ Spec k' for a field k'. Then ω_X^• and ω_X of [Stacks, Tag 0FVV] for f are isomorphic to those constructed for f'.

theorem nonempty_iso_relativeDualizing_of_factorization {k' : Type u} [Field k']
    (f' : X ⟶ Spec (.of k')) (g : Spec (.of k') ⟶ Spec (.of k)) (h : f' ≫ g = f) :
    haveI : IsProper f' := haveI : IsProper (f' ≫ g) := h ▸ ‹IsProper f›; IsProper.of_comp f' g
    Nonempty (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k))) ≅
      relativeDualizingComplex f' (isQuasicoherent_homology_derivedPushforward_of_qcqs f')
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k')))) ∧
    Nonempty (relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k))) ≅
      relativeDualizingModule f' (isQuasicoherent_homology_derivedPushforward_of_qcqs f')
        (DerivedPushforward.derivedStructureSheaf (Spec (.of k'))))

Stacks.Duality.nonempty_iso_relativeDualizing_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperOverField/ChangeOfField.lean, line 312. The attribute's comment: “(2): the pullbacks of ω_X^• and ω_X to X_K are as in 0FVV for X_K → Spec K”.

Let X be proper over a field k with structure morphism f, let K/k be a field extension and X_K = X ×_{Spec k} Spec K, with projections g' : X_K ⟶ X and f_K : X_K ⟶ Spec K. Then the pullbacks L(g')^* ω_X^• and (g')^* ω_X are isomorphic to the dualizing complex and module of [Stacks, Tag 0FVV] constructed for f_K.

theorem nonempty_iso_relativeDualizing_baseChange (K : Type u) [Field K] [Algebra k K] :
    Nonempty ((quasiCoherentDerivedPullback'
        (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K))))).obj
          (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
            (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))) ≅
      relativeDualizingComplex (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k K))))
        (isQuasicoherent_homology_derivedPushforward_of_qcqs _)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of K)))) ∧
    Nonempty ((Scheme.Modules.pullback
        (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K))))).obj
          (relativeDualizingModule f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
            (DerivedPushforward.derivedStructureSheaf (Spec (.of k)))) ≅
      relativeDualizingModule (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap k K))))
        (isQuasicoherent_homology_derivedPushforward_of_qcqs _)
        (DerivedPushforward.derivedStructureSheaf (Spec (.of K))))

Sources

• Section 48.27, Tag 0FVU
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Duality.dualityEquiv · Stacks.Duality.dualityEquiv_comp · Stacks.Duality.dualityEquiv_shiftedHomComp · Stacks.Duality.dualityLinearMap_shift · Stacks.Duality.dualityLinearMap_triangle · Stacks.Duality.isDualizingComplex_relativeDualizingComplex_of_isProper · Stacks.Duality.le_zero_and_le_dim_of_not_isZero_homology_of_isProper · Stacks.Duality.relativeDualizingModule_of_isProper

Section48.28 Relative dualizing complexes#

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

Tag 0E2T, a definition

Tag 0E2T in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplex.lean, line 149.

Stacks 0E2T. A relative dualizing complex for a flat, locally finitely presented morphism f : X ⟶ S, relative to an open W ⊆ X ×_S X through which the relative diagonal factors as a closed immersion Δ : X ⟶ W: a pair (K, ξ) consisting of an object K of D(𝒪_X) and a map ξ : Δ_*𝒪_X ⟶ L pr₁^*K|_W in D(𝒪_W) such that K is S-perfect and ξ defines an isomorphism of Δ_*𝒪_X with R SheafHom_{𝒪_W}(Δ_*𝒪_X, L pr₁^*K|_W).

The derived tensor product over the inverse-image ringed space is the family of certificates Dten, as in the definition of relative perfectness.

structure IsRelativeDualizingComplex [Flat f] [LocallyOfFinitePresentation f]
    (Dten : ∀ U : TopologicalSpace.Opens
        (RingedSpace.inverseImage S.toRingedSpace f.base).carrier,
      RingedSpace.CertifiedDerivedSheafTensoring.{d', u}
        ((RingedSpace.inverseImage S.toRingedSpace f.base).restrict U.isOpenEmbedding))
    (D : DiagonalOpen f) (K : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (ξ : D.diagonalObject ⟶ D.derivedPullbackProj K) : Prop

AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingPair, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingPair.lean, line 101.

Stacks 0E2T. A relative dualizing complex for a flat, locally finitely presented morphism f : X ⟶ S, relative to an open W ⊆ X ×_S X through which the relative diagonal factors as a closed immersion Δ : X ⟶ W: a pair (K, ξ) consisting of an object K of D(𝒪_X) and a map ξ : Δ_*𝒪_X ⟶ L pr₁^*K|_W in D(𝒪_W) such that K is S-perfect (Stacks 0DI0) and ξ defines an isomorphism of Δ_*𝒪_X with R SheafHom_{𝒪_W}(Δ_*𝒪_X, L pr₁^*K|_W).

structure IsRelativeDualizingPair [Flat f] [LocallyOfFinitePresentation f]
    (D : DiagonalOpen f) (K : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (ξ : D.diagonalObject ⟶ D.derivedPullbackProj K) : Prop

Tag 0E2U, a lemma

Tag 0E2U in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isRelativeDualizingComplex_derivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexAffineRestriction.lean, line 172. The attribute's comment: “variant: for an arbitrary family of certified tensorings, given the Tor-dimension clause of Tag 0DI2 at every object and an affine diagonal comparison datum; the tag is AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.isRelativeDualizingComplex_derivedSections”.

Stacks 0E2U. Let f : X ⟶ S be flat and locally of finite presentation and let (K, ξ) be a relative dualizing complex for f relative to an open W ⊆ X ×_S X through which the relative diagonal factors as a closed immersion. Let U ⊆ X be an affine open lying over an affine open V ⊆ S, and put R = Γ(S, V) and A = Γ(X, U), an R-algebra through f. Then RΓ(U, K), the object of D(A) corresponding to K|_U under Stacks 06Z0, is a relative dualizing complex for R → A in the sense of Stacks 0E2C.

Two cited inputs are carried. hTor is the Tor-dimension clause of Stacks 0DI2, at every object of D(𝒪_X): the affine comparison of Stacks 0DHY part (2) together with the affine-locality assembly that the Tor-dimension half of Stacks 0DI2 still lacks. cmp is the affine comparison of Δ_*𝒪_X, L pr₁^* and R SheafHom_{𝒪_W} at a chart of W over A ⊗_R A, that is Stacks 08DW part (2) and Stacks 0A6H (3)(a). The pseudo-coherence clause and the condition on ξ are proved. The statement at the source's hypotheses, at the derived tensor product of Stacks 06YU, is isRelativeDualizingComplex_derivedSections in the namespace AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.

theorem isRelativeDualizingComplex_derivedSections [Flat f] [LocallyOfFinitePresentation f]
    (Dten : ∀ U : TopologicalSpace.Opens
        (RingedSpace.inverseImage S.toRingedSpace f.base).carrier,
      RingedSpace.CertifiedDerivedSheafTensoring.{d', u}
        ((RingedSpace.inverseImage S.toRingedSpace f.base).restrict U.isOpenEmbedding))
    (D : DiagonalOpen f) (K : DerivedCategory X.Modules)
    (ξ : D.diagonalObject ⟶ D.derivedPullbackProj K)
    (hK : IsRelativeDualizingComplex f Dten D K ξ)
    {U : X.Opens} (hU : IsAffineOpen U) {V : S.Opens} (hV : IsAffineOpen V)
    (hUV : U ≤ f ⁻¹ᵁ V)
    [Algebra ↑Γ(S, V) ↑Γ(X, U)] [Module.Flat ↑Γ(S, V) ↑Γ(X, U)]
    [Algebra.FinitePresentation ↑Γ(S, V) ↑Γ(X, U)]
    (_halg : algebraMap ↑Γ(S, V) ↑Γ(X, U) = (f.appLE V U hUV).hom)
    (hTor : ∀ E : DerivedCategory X.Modules,
      RingedSpace.LocallyHasFiniteTorDimension
          (RingedSpace.inverseImage S.toRingedSpace f.base) Dten
          ((derivedScalarRestriction f).obj E) →
        StacksDraft.TorAmplitude.HasFiniteTorDimension
          (CochainComplex.DerivedTensor.canonicalDerivedTensorProduct ↑Γ(S, V)).tensor
          (StacksDraft.TorAmplitude.canonicalTensorComparison ↑Γ(S, V))
          (StacksDraft.TorAmplitude.canonicalTensorIsLeftDerived ↑Γ(S, V))
          ((ModuleCat.restrictScalars (algebraMap ↑Γ(S, V) ↑Γ(X, U))).mapDerivedCategory.obj
            ((derivedSectionsUnbounded X U).obj E)))
    (cmp : D.AffineDiagonalComparison U ↑Γ(S, V)) :
    Dualizing.IsRelativeDualizingComplex ↑Γ(S, V) ↑Γ(X, U)
      ((derivedSectionsUnbounded X U).obj K)

AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.isRelativeDualizingComplex_derivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexAffineSections.lean, line 267.

Stacks 0E2U. Let f : X ⟶ S be flat and locally of finite presentation and let (K, ξ) be a relative dualizing complex for f (Stacks 0E2T), relative to an open W ⊆ X ×_S X through which the relative diagonal factors as a closed immersion. Let U ⊆ X be an affine open lying over an affine open V ⊆ S, and put R = Γ(S, V) and A = Γ(X, U), an R-algebra through f. Then RΓ(U, K), the object of D(A) corresponding to K|_U under Stacks 06Z0, is a relative dualizing complex for R → A in the sense of Stacks 0E2C.

S-perfectness is read at the derived tensor product of Stacks 06YU on the open subspaces of (X, f⁻¹𝒪_S), as in Stacks 0DI2.

theorem isRelativeDualizingComplex_derivedSections {D : DiagonalOpen f}
    {K : DerivedCategory X.Modules} {ξ : D.diagonalObject ⟶ D.derivedPullbackProj K}
    (hK : IsRelativeDualizingComplex f
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base)) D K ξ)
    {U : X.Opens} (hU : IsAffineOpen U) {V : S.Opens} (hV : IsAffineOpen V)
    (hUV : U ≤ f ⁻¹ᵁ V) :
    letI : Algebra Γ(S, V) Γ(X, U) := (f.appLE V U hUV).hom.toAlgebra
    letI : Module.Flat Γ(S, V) Γ(X, U) := moduleFlat_appLE f hV hU hUV rfl
    letI : Algebra.FinitePresentation Γ(S, V) Γ(X, U) :=
      algebraFinitePresentation_appLE f hV hU hUV rfl
    Dualizing.IsRelativeDualizingComplex Γ(S, V) Γ(X, U)
      ((derivedSectionsUnbounded X U).obj K)

Tag 0E2V, a lemma

Tag 0E2V in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.isIso_derivedSheafHomothety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexEndomorphisms.lean, line 208.

Stacks 0E2V. Let f : X ⟶ S be flat and locally of finite presentation and let (K, ξ) be a relative dualizing complex for f (Stacks 0E2T), relative to an open W ⊆ X ×_S X through which the relative diagonal factors as a closed immersion. Then the homothety 𝒪_X ⟶ R𝓗om_{𝒪_X}(K, K) is an isomorphism.

S-perfectness is read at the derived tensor product of Stacks 06YU on the open subspaces of (X, f⁻¹𝒪_S), as in Stacks 0DI2 and Stacks 0E2U. The proof is the source's: on every compatible pair of affine opens RΓ(U, K) is a relative dualizing complex for Γ(S, V) → Γ(X, U) by Stacks 0E2U, and the algebraic case is Stacks 0E2G.

theorem isIso_derivedSheafHomothety {D : DiagonalOpen f}
    {K : DerivedCategory X.Modules} {ξ : D.diagonalObject ⟶ D.derivedPullbackProj K}
    (hK : IsRelativeDualizingComplex f
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base)) D K ξ) :
    IsIso (Stacks.SheafOfModules.derivedSheafHomothety X.sheaf K)

Tag 0E2W, a lemma

Tag 0E2W in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.existsUnique_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexUniqueIso.lean, line 48.

Stacks 0E2W. Let f : X ⟶ S be flat and locally of finite presentation, and let W be an open of X ×_S X through which the relative diagonal factors as a closed immersion Δ : X ⟶ W. If (K, ξ) and (L, η) are relative dualizing complexes on X/S relative to W (Stacks 0E2T), then there is a unique isomorphism α : K ≅ L sending ξ to η, that is with ξ ≫ L pr₁^*α|_W = η.

theorem existsUnique_iso {D : DiagonalOpen f}
    {K L : DerivedCategory (OXMod.{u, u} X.toRingedSpace)}
    {ξ : D.diagonalObject ⟶ D.derivedPullbackProj K}
    {η : D.diagonalObject ⟶ D.derivedPullbackProj L}
    (hK : IsRelativeDualizingComplex f
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base)) D K ξ)
    (hL : IsRelativeDualizingComplex f
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base)) D L η) :
    ∃! α : K ≅ L, ξ ≫ D.derivedPullbackProjMap α.hom = η

Tag 0E2X, a lemma

Tag 0E2X in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.exists_isRelativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexExistence.lean, line 1025.

Stacks 0E2X. Let f : X ⟶ S be flat and locally of finite presentation. There exists a relative dualizing complex (K, ξ) (Stacks 0E2T), relative to any open W ⊆ X ×_S X through which the relative diagonal factors as a closed immersion: K ∈ D(𝒪_X) is S-perfect and ξ : Δ_*𝒪_X ⟶ L pr₁^*K|_W defines an isomorphism Δ_*𝒪_X ≅ R SheafHom_{𝒪_W}(Δ_*𝒪_X, L pr₁^*K|_W).

S-perfectness is read at a family Dten of derived tensor products on the open subspaces of (X, f⁻¹𝒪_S) whose underived tensor products are those of sheaves of modules, so that it is Stacks 0DI0 (AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_iff_isRelativelyPerfect).

The derived categories of the inverse-image ringed spaces (X, f⁻¹𝒪_S)|_U are those of CategoryTheory.HasDerivedCategory.standard, the model at which the chart step (Stacks 0E2F read through Stacks 0E2U, exists_isRelativeDualizingComplex_chart), the restriction of relative dualizing complexes and Stacks 0E2W are stated. They cannot be left arbitrary: the Tor clause of S-perfectness is read on (derivedScalarRestriction f).obj K in the chosen model of D(f⁻¹𝒪_S), and carrying it from one model to another needs the comparison of the two models of the derived category, which the library does not provide.

theorem exists_isRelativeDualizingComplex [Flat f] [LocallyOfFinitePresentation f]
    (Dten : ∀ U : TopologicalSpace.Opens
        (RingedSpace.inverseImage S.toRingedSpace f.base).carrier,
      RingedSpace.CertifiedDerivedSheafTensoring
        ((RingedSpace.inverseImage S.toRingedSpace f.base).restrict U.isOpenEmbedding))
    (hD : IsGenuineRelativeTensorFamily f Dten) (D : DiagonalOpen f) :
    ∃ (K : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
      (ξ : D.diagonalObject ⟶ D.derivedPullbackProj K),
      IsRelativeDualizingComplex f Dten D K ξ

Tag 0E2Y, a lemma

Tag 0E2Y in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexBaseChangeTheorem.lean, line 154. The attribute's comment: “As in the source's proof, W' is any diagonal open of f' with (g' × g')(W') ⊆ W, and w : W' ⟶ W is the induced morphism.”.

Stacks 0E2Y: base change of a relative dualizing complex. Let X' = X ×_S S' with projections g' : X' ⟶ X and f' : X' ⟶ S', f flat and locally of finite presentation, and let (K, ξ) be a relative dualizing complex for f relative to a diagonal open W. For a diagonal open W' of f' with (g' × g')(W') ⊆ W and w : W' ⟶ W the induced morphism, set K' = L(g')^*K and let ξ' be the derived base change of ξ: Lw^*ξ read through Lw^*Δ_*𝒪_X = Δ'_*𝒪_{X'} (the base change of Δ_* across the Tor independent diagonal square) and transitivity of derived pullback. Then (K', ξ') is a relative dualizing complex for f' relative to W'.

theorem baseChange (hpb : IsPullback g' f' f g) {D : DiagonalOpen f}
    {K : DerivedCategory X.Modules} {ξ : D.diagonalObject ⟶ D.derivedPullbackProj K}
    (hK : IsRelativeDualizingComplex f
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base)) D K ξ)
    (D' : DiagonalOpen f') (w : D'.W ⟶ D.W)
    (hw : w ≫ D.ι = D'.ι ≫ pullbackMapOfIsPullback hpb) :
    haveI : Flat f' := MorphismProperty.of_isPullback (P := @Flat) hpb (inferInstance : Flat f)
    haveI : LocallyOfFinitePresentation f' :=
      MorphismProperty.of_isPullback (P := @LocallyOfFinitePresentation) hpb
        (inferInstance : LocallyOfFinitePresentation f)
    IsRelativeDualizingComplex f'
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S'.toRingedSpace f'.base)) D'
      (DiagonalOpen.baseChangeComplex g' K)
      (D.baseChangeDiagonalMap D' g' w (DiagonalOpen.proj_baseChange hpb D D' w hw)
        (DiagonalOpen.baseChangeDiagonalIso hpb D D' w hw) K ξ)

Tag 0E2Z, a lemma

Tag 0E2Z in the Stacks Project.

Stacks.Duality.isRelativeDualizingComplex_relativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexOfProperFlat.lean, line 61.

Stacks Project, Tag 0E2Z. Let S be a quasi-compact and quasi-separated scheme and let f : X ⟶ S be a proper, flat morphism of finite presentation. The relative dualizing complex ω_{X/S}^• = a(𝒪_S) of [Stacks, Remark 0B6S] (Stacks.Duality.StandardModel.relativeDualizingComplex) together with the map ξ : Δ_*𝒪_X ⟶ L pr₁^*ω_{X/S}^• coming from the isomorphism 𝒪_X ≅ c(L pr₁^*ω_{X/S}^•) of [Stacks, Tag 0E2Q] (Stacks.Duality.relativeDualizingComplexDiagonalMap) is a relative dualizing complex in the sense of [Stacks, Definition 0E2T], for the open W = X ×_S X (the morphism being separated) and the derived tensor product of sheaves of modules.

Of finite presentation is LocallyOfFinitePresentation f together with the quasi-compactness and quasi-separatedness that properness includes.

theorem isRelativeDualizingComplex_relativeDualizingComplex {X S : Scheme.{u}} (f : X ⟶ S)
    [CompactSpace S] [QuasiSeparatedSpace S] [IsProper f] [Flat f]
    [LocallyOfFinitePresentation f] :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    haveI : CompactSpace (pullback f f : Scheme.{u}) :=
      QuasiCompact.compactSpace_of_compactSpace (pullback.fst f f)
    haveI : QuasiSeparatedSpace (pullback f f : Scheme.{u}) :=
      quasiSeparatedSpace_of_quasiSeparated (pullback.fst f f)
    @Scheme.Hom.IsRelativeDualizingComplex X S f (HasDerivedCategory.standard _)
      (fun _ => HasDerivedCategory.standard _) _ _
      (@RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base) (fun _ => HasDerivedCategory.standard _))
      (Scheme.Hom.DiagonalOpen.ofIsSeparated f) (StandardModel.relativeDualizingComplex f).obj
      (relativeDualizingComplexDiagonalMap f)

Tag 0E4P, a remark

Tag 0E4P in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.relativeDualizingComplex_baseChange_twistedInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexProperFlatBaseChange.lean, line 193.

Relative dualizing complexes and base change. Let f : X ⟶ S be flat, proper and of finite presentation, and let W be a diagonal open of f. There is a relative dualizing complex (ω_{X/S}^•, ξ) for f relative to W (Stacks 0E2X), and for every such pair, every morphism g : S' ⟶ S with S' quasi-compact and quasi-separated, with base change f' : X' ⟶ S' and projection g' : X' ⟶ X, and every diagonal open W' of f' mapped into W by g' × g', there is a unique isomorphism ω_{X'/S'}^• = a'(𝒪_{S'}) ≅ L(g')^*ω_{X/S}^• compatible with the map of Equation 0E2Q (restricted to W') and the derived base change L(g')^*ξ of Stacks 0E2Y.

theorem relativeDualizingComplex_baseChange_twistedInverseImage {X S : Scheme.{u}} (f : X ⟶ S)
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f] (D : DiagonalOpen f) :
    (∃ (K : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
      (ξ : D.diagonalObject ⟶ D.derivedPullbackProj K),
      IsRelativeDualizingComplex f (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base)) D K ξ) ∧
    ∀ (K : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
      (ξ : D.diagonalObject ⟶ D.derivedPullbackProj K),
      IsRelativeDualizingComplex f (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage S.toRingedSpace f.base)) D K ξ →
      ∀ {X' S' : Scheme.{u}} [CompactSpace S'] [QuasiSeparatedSpace S'] {g : S' ⟶ S}
        {g' : X' ⟶ X} {f' : X' ⟶ S'} (hpb : IsPullback g' f' f g)
        (D' : DiagonalOpen f') (w : D'.W ⟶ D.W)
        (hw : w ≫ D.ι = D'.ι ≫ pullbackMapOfIsPullback hpb),
        haveI : IsProper f' := MorphismProperty.of_isPullback (P := @IsProper) hpb inferInstance
        haveI : Flat f' := MorphismProperty.of_isPullback (P := @Flat) hpb inferInstance
        haveI : LocallyOfFinitePresentation f' :=
          MorphismProperty.of_isPullback (P := @LocallyOfFinitePresentation) hpb inferInstance
        haveI : CompactSpace X' := QuasiCompact.compactSpace_of_compactSpace f'
        haveI : QuasiSeparatedSpace X' := quasiSeparatedSpace_of_quasiSeparated f'
        haveI : CompactSpace (pullback f' f' : Scheme.{u}) :=
          QuasiCompact.compactSpace_of_compactSpace (pullback.fst f' f')
        haveI : QuasiSeparatedSpace (pullback f' f' : Scheme.{u}) :=
          quasiSeparatedSpace_of_quasiSeparated (pullback.fst f' f')
        ∃! φ : (Stacks.Duality.StandardModel.relativeDualizingComplex f').obj ≅
            DiagonalOpen.baseChangeComplex g' K,
          (DiagonalOpen.ofIsSeparated f').restrictDiagonalMap D' D'.ι
              (DiagonalOpen.comp_ι_ofIsSeparated f' D')
              (Stacks.Duality.StandardModel.relativeDualizingComplex f').obj
              (Stacks.Duality.relativeDualizingComplexDiagonalMap f') ≫
              D'.derivedPullbackProjMap φ.hom =
            D.baseChangeDiagonalMap D' g' w (DiagonalOpen.proj_baseChange hpb D D' w hw)
              (DiagonalOpen.baseChangeDiagonalIso hpb D D' w hw) K ξ

Tag 0E9W, a lemma

Tag 0E9W in the Stacks Project.

Stacks.Duality.exists_isRelativeDualizingComplex_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekRelativeDualizing.lean, line 269.

Stacks Project, Tag 0E9W. In Situation 48.16.1 (S Noetherian), let f : X ⟶ Y be a flat morphism of FTS S, with f^! computed at any compactification j. Then f^!𝒪_Y is the first component of a relative dualizing complex for X over Y (Definition 0E2T): for every open W ⊆ X ×_Y X through which the diagonal factors as a closed immersion Δ : X ⟶ W there is ξ : Δ_*𝒪_X ⟶ L pr₁^* f^!𝒪_Y|_W making (f^!𝒪_Y, ξ) a relative dualizing complex.

theorem exists_isRelativeDualizingComplex_upperShriek (D : f.left.DiagonalOpen) :
    letI := locallyOfFinitePresentation_left f
    ∃ ξ : D.diagonalObject ⟶ D.derivedPullbackProj (relativeDualizingComplexObj f j),
      Scheme.Hom.IsRelativeDualizingComplex.{u + 1, u} f.left
        (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily _) D
        (relativeDualizingComplexObj f j) ξ

Tag 0E30, a lemma

Tag 0E30 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexComposite.lean, line 97.

Stacks 0E30. Let f : Y ⟶ X and g : X ⟶ S be flat and locally of finite presentation, and let (K, ξ) and (M, η) be relative dualizing complexes for g and f. Then (M ⊗ᴸ Lf^*K, ζ) is a relative dualizing complex for f ≫ g, for a suitable ζ, on the diagonal open W' = Dg.comp Df of the source's proof.

The source's proof applies Stacks 0E2N with tensor factor Lq^*M over 𝒪_{Y ×_S Y}, which needs Tor amplitude of Lq^*M over 𝒪_{Y ×_S Y}; this fails for X = S = Spec k, Y = Spec B, B Artinian non-Gorenstein, M = ω_B. The proof here uses instead the Tor amplitude of Lq^*M relative to f × f, as the algebraic version 0E2H does over A ⊗_R A.

theorem IsRelativeDualizingComplex.comp {X Y S : Scheme.{u}} (g : X ⟶ S) (f : Y ⟶ X)
    [Flat g] [LocallyOfFinitePresentation g] [Flat f] [LocallyOfFinitePresentation f]
    {Dg : DiagonalOpen g} {K : DerivedCategory X.Modules}
    {ξ : Dg.diagonalObject ⟶ Dg.derivedPullbackProj K}
    (hK : IsRelativeDualizingComplex g (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily _)
      Dg K ξ)
    {Df : DiagonalOpen f} {M : DerivedCategory Y.Modules}
    {η : Df.diagonalObject ⟶ Df.derivedPullbackProj M}
    (hM : IsRelativeDualizingComplex f (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily _)
      Df M η) :
    ∃ ζ, IsRelativeDualizingComplex (f ≫ g)
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily _) (Dg.comp Df)
      (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor
        Y.toRingedSpace.sheaf).obj M).obj
        ((derivedPullback f.toLRSHom.toShHom).obj K)) ζ

Sources

• Section 48.28, Tag 0E2S
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex · AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingPair · AlgebraicGeometry.Scheme.Hom.isRelativeDualizingComplex_derivedSections · AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.isRelativeDualizingComplex_derivedSections · AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.isIso_derivedSheafHomothety · AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.existsUnique_iso · AlgebraicGeometry.Scheme.Hom.exists_isRelativeDualizingComplex · AlgebraicGeometry.Scheme.Hom.IsRelativeDualizingComplex.baseChange

Section48.29 The fundamental class of an lci morphism#

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

Tag 0E9Y, a lemma

Tag 0E9Y in the Stacks Project.

Stacks.Duality.isIso_stalkMap_locallyRingedSpaceDeterminantMap_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/FundamentalClassDeterminantSource.lean, line 617.

[Stacks, Tag 0E9Y]. Let X be a locally ringed space and E₁ --α--> E₀ --π--> F ⟶ 0 an exact sequence of O_X-modules with E₁ and E₀ finite locally free of ranks r₁ and r₀. The canonical map ⋀^{r₀ - r₁} F ⟶ ⋀^{r₁}(E₁^∨) ⊗ ⋀^{r₀} E₀ is an isomorphism on the stalk at x if and only if F is locally free of rank r₀ - r₁ on an open neighbourhood of x: that is, r₀ - r₁ is a natural number and F is free of that rank on some open U ∋ x.

theorem isIso_stalkMap_locallyRingedSpaceDeterminantMap_iff [Epi π]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E₁ r₁]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E₀ r₀]
    (x : ↥Y.toRingedSpace.carrier) :
    IsIso (AlgebraicGeometry.SheafOfModules.stalkMap
        (toRingCat (Opens.grothendieckTopology ↥Y.toRingedSpace.carrier) Y.toRingedSpace.sheaf) x
        (locallyRingedSpaceDeterminantMap Y α π hαπ hS r₁ r₀)) ↔
      r₁ ≤ r₀ ∧ ∃ U : Opens ↥Y.toRingedSpace.carrier, x ∈ U ∧
        ∃ t : LocallyFreeRank.Trivialization Y.toRingedSpace.carrier
          (LocallyFreeRank.toRingSheaf Y.toRingedSpace.carrier Y.toRingedSpace.sheaf) F U,
          Nonempty (t.ι ≃ Fin (r₀ - r₁))

Tag 0E9Z, a lemma

Tag 0E9Z in the Stacks Project.

Stacks.Duality.ClosedOpenProperFactorization.exists_fundamentalClass_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekLocalCompleteIntersection/Decomposition.lean, line 258.

Let S be Noetherian and f : X ⟶ Y a local complete intersection morphism of FTS S which factors as an immersion ι : X ⟶ P followed by a proper smooth morphism g : P ⟶ Y; let f^! be computed at any compactification j of f. Then there is a locally constant function r on X such that ω_{X/Y} = H^{-r}(f^!𝒪_Y) is the only nonzero cohomology sheaf of f^!𝒪_Y (the stalk of H^k(f^!𝒪_Y) at x is nonzero exactly for k = -r(x)), and a map ∧^r Ω_{X/Y} ⟶ ω_{X/Y} whose stalk at x is an isomorphism exactly when f is smooth at x.

As r is only locally constant, the map is given on each piece of a decomposition of X into pairwise disjoint open and closed subschemes covering X on which r is constant.

theorem exists_fundamentalClass_of_isLocalCompleteIntersection
    (hlci : IsLocalCompleteIntersectionMorphism f.left) (j : CompactificationOf (Over.mk f.left)) :
    ∃ r : X.left → ℤ, IsLocallyConstant r ∧
      (∀ (x : X.left) (k : ℤ),
        Nontrivial ↑((upperShriekHomology f j k).presheaf.stalk x) ↔ k = -r x) ∧
      ∃ (A : Type) (V : A → X.left.Opens) (n : A → ℤ),
        (∀ a, IsClosed (V a : Set X.left)) ∧ Pairwise (Function.onFun Disjoint V) ∧ (⨆ a, V a) = ⊤ ∧
        (∀ a, ∀ x ∈ V a, r x = n a) ∧
        ∀ a, ∃ φ : (Scheme.Modules.restrictFunctor (V a).ι).obj
            (Scheme.Modules.exteriorPower (Scheme.Hom.relativeDifferentials f.left) (n a)) ⟶
          (Scheme.Modules.restrictFunctor (V a).ι).obj (upperShriekHomology f j (-n a)),
          ∀ x : (V a).toScheme, IsIso (AlgebraicGeometry.SheafOfModules.stalkMap
              (CategoryTheory.Sheaf.toRingCat (Opens.grothendieckTopology
                ↥(V a).toScheme.toLocallyRingedSpace.toRingedSpace.carrier)
                (V a).toScheme.toLocallyRingedSpace.toRingedSpace.sheaf) x φ) ↔
            InfinitesimalLifting.SmoothAt f.left ((V a).ι x)

Tag 0EA0, a lemma

Tag 0EA0 in the Stacks Project.

Stacks.Duality.SmoothLocus.exists_map_exteriorPower_isIso_of_smoothAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekLocalCompleteIntersection/SmoothLocus.lean, line 409.

Stacks Project, Tag 0EA0. Let S be Noetherian, f : X ⟶ Y a morphism of FTS S and r ≥ 0. Assume 1. Y is Cohen–Macaulay, 2. f factors as an immersion ι : X ⟶ P followed by a smooth proper g : P ⟶ Y, 3. f is Koszul at every x ∈ X with dim 𝒪_{X,x} ≤ 1, and 4. trdeg_{κ(f(ξ))} κ(ξ) = r at every generic point ξ of an irreducible component of X.

Then, with ω_{X/Y} = H^{-r}(f^!𝒪_Y) (f^! at any compactification j), there is a map ∧^r Ω_{X/Y} ⟶ ω_{X/Y} which is an isomorphism at every point where f is smooth.

Two steps of the source's proof are corrected. The locally constant function of [Stacks, Tag 0E9Z] on the local complete intersection locus U is r only on the pieces where it equals r (in general it is r - dim 𝒪_{Y,f(ξ)} at generic points ξ); every smooth point lies on such a piece, and on the others ω_{X/Y} vanishes and the map is taken to be zero. The extension across X ∖ U by [Stacks, Tag 0E9I] needs depth(ω_{X/Y,x}) ≥ 2 there; the (S₂) property of [Stacks, Tag 0E9V] does not give this alone, and it is proved as min(2, dim 𝒪_{X,x}) ≤ depth(ω_{X/Y,x}) (Stacks.Duality.min_two_ringKrullDim_le_moduleDepth_modulesStalk_homology_upperShriek).

theorem exists_map_exteriorPower_isIso_of_smoothAt {S : Scheme.{u}} [IsNoetherian S]
    {X Y : FTS S} (f : X ⟶ Y) (r : ℕ) (hY : AlgebraicGeometry.IsCohenMacaulay Y.left)
    {P : Scheme.{u}} (ι : X.left ⟶ P) [IsImmersion ι] (g : P ⟶ Y.left) [Smooth g] [IsProper g]
    (hfac : ι ≫ g = f.left)
    (hK : ∀ x : X.left, ringKrullDim (X.left.presheaf.stalk x) ≤ 1 → KoszulAt f.left x)
    (htr : ∀ ξ : X.left, closure {ξ} ∈ irreducibleComponents X.left →
      Stacks.Chow.residueTrdeg f.left ξ = (r : Cardinal))
    (j : CompactificationOf (Over.mk f.left)) :
    ∃ φ : Scheme.Modules.exteriorPower (Scheme.Hom.relativeDifferentials f.left) (r : ℤ) ⟶
        upperShriekHomology f j (-(r : ℤ)),
      ∀ x : X.left, InfinitesimalLifting.SmoothAt f.left x →
        IsIso (AlgebraicGeometry.SheafOfModules.stalkMap
          (Sheaf.toRingCat (Opens.grothendieckTopology
            ↥X.left.toLocallyRingedSpace.toRingedSpace.carrier)
            X.left.toLocallyRingedSpace.toRingedSpace.sheaf) x φ)

Sources

• Section 48.29, Tag 0E9X
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Duality.isIso_stalkMap_locallyRingedSpaceDeterminantMap_iff · Stacks.Duality.ClosedOpenProperFactorization.exists_fundamentalClass_of_isLocalCompleteIntersection · Stacks.Duality.SmoothLocus.exists_map_exteriorPower_isIso_of_smoothAt

Section48.30 Extension by zero for coherent modules#

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

Tag 0G2H, a lemma

Tag 0G2H in the Stacks Project.

AlgebraicGeometry.DeligneSystem.isIso_restrictionNatTrans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemCoreCoherent.lean, line 124.

Stacks Project, Tag 0G2H. Let j : U ⟶ X be an open immersion of Noetherian schemes and let (K_n) be a Deligne system with value K on U. Then the canonical restriction transformation

colim_n Mor_X(K_n, -) ⟶ Mor_U(K, (-)|_U)

is an isomorphism: colim_n Hom_X(K_n, L) = Hom_U(K, L|_U) for every L in D^b_{Coh}(𝒪_X).

This is AlgebraicGeometry.DeligneSystem.isIso_restrictionNatTrans_of_core with its hypothesis hcore supplied by AlgebraicGeometry.DeligneSystem.restrictionLifting_truncGELE.

public theorem isIso_restrictionNatTrans (K : BoundedCoherentDerived U)
    (e : D.system ⋙ restrictBoundedCoherent j ≅
      (Functor.const ℕᵒᵖ).obj ((boundedCoherentDerived U).ι.obj K)) :
    IsIso (D.restrictionNatTrans K e)

Tag 0G4K, a lemma

Tag 0G4K in the Stacks Project.

AlgebraicGeometry.DeligneSystem.nonempty_isColimit_restrictionHomCocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemRestrictionLifting.lean, line 257.

Stacks Project, Tag 0G4K. The result of [Stacks, Tag 0G2H] holds even for L in D^+_{Coh}(𝒪_X). Let j : U ⟶ X be an open immersion of Noetherian schemes, let (K_n) be a Deligne system, identified on U by e with the constant system at K, and let L be an object of D(𝒪_X) that is cohomologically bounded below with coherent cohomology sheaves. Then

colim_n Hom_X(K_n, L) = Hom_U(K, L|_U),

the map being the canonical one: the cocone of CategoryTheory.restrictionHomCocone, which sends g : K_n ⟶ L to K ≅ K_n|_U ⟶ L|_U, is a colimit cocone.

This is AlgebraicGeometry.DeligneSystem.restrictionLifting_of_derivedCategoryBPlus read through CategoryTheory.RestrictionLifting.isColimitRestrictionHomCocone. Nothing is assumed.

public theorem nonempty_isColimit_restrictionHomCocone (K : BoundedCoherentDerived U)
    (e : D.system ⋙ restrictBoundedCoherent j ≅
      (Functor.const ℕᵒᵖ).obj ((boundedCoherentDerived U).ι.obj K))
    (L : DerivedCategory X.Modules)
    (hL : DerivedCategoryB.derivedCategoryBPlus (fun M : X.Modules => M.IsCoherent) L) :
    Nonempty (IsColimit (restrictionHomCocone (D.system ⋙ (boundedCoherentDerived X).ι)
      (Scheme.Modules.restrictFunctor j).mapDerivedCategory L
      ((boundedCoherentDerived U).ι.obj K) e))

Tag 0G4L, a lemma

Tag 0G4L in the Stacks Project.

AlgebraicGeometry.DeligneSystem.exists_restrictIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemExistence.lean, line 88. The attribute's comment: “(2)”.

Stacks Project, Tag 0G4L (2). Let j : U ⟶ X be an open immersion of Noetherian schemes. Given K in D^b_{Coh}(𝒪_U), there exists a Deligne system (K_n) such that (K_n|_U) is constant with value K.

As in the source, K is the restriction of a bounded complex 𝓕^• of coherent 𝒪_X-modules (AlgebraicGeometry.exists_bounded_isCoherent_complex_restrict_Q_iso, which rests on Stacks 0G48 and Stacks 0FDB), the ideal sheaf is that of the reduced closed complement of U, and the Deligne system is (𝓘^n𝓕^•), AlgebraicGeometry.DeligneTriangle.deligneSystemOfComplex.

public theorem exists_restrictIso (j : U ⟶ X) [IsOpenImmersion j] [IsNoetherian X]
    (K : BoundedCoherentDerived U) :
    ∃ D : DeligneSystem j, Nonempty (D.system ⋙ restrictBoundedCoherent j ≅
      (Functor.const ℕᵒᵖ).obj ((boundedCoherentDerived U).ι.obj K))

AlgebraicGeometry.DeligneSystem.Value.proHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemHom.lean, line 394. The attribute's comment: “lift_morphisms; the identification of 0G2H supplied as data”.

Stacks Project, Tag 0G4L(1). Let j : U ⟶ X be an open immersion of Noetherian schemes, let (K_n) and (L_m) be Deligne systems and let K and L be the values of the constant systems (K_n|_U) and (L_m|_U). Then every morphism α : K ⟶ L on U is the restriction of a unique morphism of pro-systems (K_n) ⟶ (L_m) in D^b_{Coh}(𝒪_X).

This is the argument of the source: morphisms of pro-systems are the morphisms of the pro-objects they determine (Stacks 0G2X, which is CategoryTheory.ProSeq.ofHomEquiv), that is lim_m colim_n Hom_X(K_n, L_m); by Stacks 0G2H each term of the limit is Hom_U(K, L_m|_U), and (L_m|_U) is the constant system at L, so the limit is over a constant diagram on a connected index category and equals Hom_U(K, L).

public def proHomEquiv :
    (D.proObject ⟶ E.proObject) ≃
      ((boundedCoherentDerived U).ι.obj V.obj ⟶
        (boundedCoherentDerived U).ι.obj W.obj)

AlgebraicGeometry.DeligneSystem.existsUnique_proHom_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemProMorphisms.lean, line 252. The attribute's comment: “(1)”.

Stacks Project, Tag 0G4L (1). Let j : U ⟶ X be an open immersion of Noetherian schemes, let (K_n) and (L_m) be Deligne systems and let K and L be the values of the constant systems (K_n|_U) and (L_m|_U), through the identifications eD and eE. Given a morphism α : K ⟶ L of D(𝒪_U), there is a unique morphism of pro-systems ξ : (K_n) ⟶ (L_m) of D^b_{Coh}(𝒪_X) whose restriction to U is α: for every m, and every representative g : K_n ⟶ L_m of the m-th component of ξ in colim_n Hom_X(K_n, L_m), the restriction K ≅ K_n|_U ⟶ L_m|_U of g is K ⟶ L ≅ L_m|_U.

Morphisms of pro-systems are transformations of the functors they corepresent (Stacks 0G2X), which by Stacks 0G2H are Hom_U(L, (-)|_U) and Hom_U(K, (-)|_U).

public theorem existsUnique_proHom_restrict (α : K ⟶ L) :
    ∃! ξ : D.proObject ⟶ E.proObject,
      ∀ (m n : ℕ) (g : D.system.obj (op n) ⟶ E.system.obj (op m)),
        proHomComponent ξ m = Pro.seqStage D.system g →
          eD.inv.app (op n) ≫ (restrictBoundedCoherent j).map g = α ≫ eE.inv.app (op m)

AlgebraicGeometry.DeligneSystem.existsUnique_proIso_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemProMorphisms.lean, line 303. The attribute's comment: “(3)”.

Stacks Project, Tag 0G4L (3). Let j : U ⟶ X be an open immersion of Noetherian schemes. The pro-object of a Deligne system with value K (part (2)) is unique up to unique isomorphism as a pro-object: for Deligne systems (K_n) and (K'_n) whose restrictions to U are identified, by eD and eE, with the constant system at K, there is a unique isomorphism of pro-objects (K_n) ≅ (K'_n) whose restriction to U is the identity of K: for every m, and every representative g : K_n ⟶ K'_m of the m-th component of its forward morphism, the restriction K ≅ K_n|_U ⟶ K'_m|_U of g is K ≅ K'_m|_U.

This follows from part (1): the morphisms restricting to the identity in the two directions compose to morphisms restricting to the identity, which are the identities.

public theorem existsUnique_proIso_restrict
    (eD : D.system ⋙ restrictBoundedCoherent j ≅ (Functor.const ℕᵒᵖ).obj K)
    (eE : E.system ⋙ restrictBoundedCoherent j ≅ (Functor.const ℕᵒᵖ).obj K) :
    ∃! i : D.proObject ≅ E.proObject,
      ∀ (m n : ℕ) (g : D.system.obj (op n) ⟶ E.system.obj (op m)),
        proHomComponent i.hom m = Pro.seqStage D.system g →
          eD.inv.app (op n) ≫ (restrictBoundedCoherent j).map g = eE.inv.app (op m)

Tag 0G4M, a lemma

Tag 0G4M in the Stacks Project.

AlgebraicGeometry.DeligneTriangle.exists_deligneSystem_distTriang_boundedCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemTriangleExtensionCoherent.lean, line 475.

Stacks Project, Tag 0G4M. Let j : U ⟶ X be an open immersion of Noetherian schemes and let

K ⟶ L ⟶ M ⟶ K[1]

be a distinguished triangle of D^b_{Coh}(𝒪_U). Then there is an inverse system of distinguished triangles

K_n ⟶ L_n ⟶ M_n ⟶ K_n[1]

in D^b_{Coh}(𝒪_X) such that (K_n), (L_n) and (M_n) are Deligne systems and such that the restriction of these distinguished triangles to U is isomorphic to the distinguished triangle one started with.

The system is the one of AlgebraicGeometry.DeligneTriangle.exists_deligneSystem_distTriang_derived, the cone triangles of a coherent complex model of K ⟶ L, lifted to D^b_{Coh}(𝒪_X) by AlgebraicGeometry.DeligneTriangle.exists_triangleFunctor_lift; the identifications of its vertex systems and of its restriction to U are transported back along the fully faithful inclusions of D^b_{Coh}.

public theorem exists_deligneSystem_distTriang_boundedCoherent (j : U ⟶ X) [IsOpenImmersion j]
    [IsNoetherian X]
    (T : Triangle (BoundedCoherentDerived U)) (hT : T ∈ distTriang (BoundedCoherentDerived U)) :
    ∃ (DK DL DM : DeligneSystem j) (TX : ℕᵒᵖ ⥤ Triangle (BoundedCoherentDerived X)),
      (∀ n : ℕᵒᵖ, TX.obj n ∈ distTriang (BoundedCoherentDerived X)) ∧
      Nonempty (TX ⋙ Triangle.π₁ ≅ DK.system) ∧
      Nonempty (TX ⋙ Triangle.π₂ ≅ DL.system) ∧
      Nonempty (TX ⋙ Triangle.π₃ ≅ DM.system) ∧
      Nonempty (TX ⋙ (restrictBoundedCoherentLift j).mapTriangle ≅
        (Functor.const ℕᵒᵖ).obj T)

Tag 0G4N, a remark

Tag 0G4N in the Stacks Project.

CategoryTheory.extensionByZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroFunctor.lean, line 80. The attribute's comment: “the functor Rj_!, for a Deligne-system assignment supplied as data”.

Stacks Project, Tag 0G4N. Sending an object K of 𝒞 to the pro-object of the inverse sequence assigned to it determines a functor Rj_! : 𝒞 ⥤ Pro-𝒟. Its functor of points at K is L ↦ Mor_𝒞(K, j^* L).

public def extensionByZero : 𝒞 ⥤ ProSeq 𝒟

CategoryTheory.extensionByZeroHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroFunctor.lean, line 99. The attribute's comment: “the left adjointness of Rj_! to j^*”.

Stacks Project, Tag 0G4N, the left adjointness of Rj_! to j^*: morphisms of pro-objects from Rj_! K to the constant pro-object at L are the morphisms K ⟶ j^* L.

public def extensionByZeroHomEquiv (K : 𝒞) (L : 𝒟) :
    ((extensionByZero jstar A).obj K ⟶ ProSeq.const.obj L) ≃ (K ⟶ jstar.obj L)

AlgebraicGeometry.extensionByZeroOpenImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroOpenImmersion.lean, line 275. The attribute's comment: “the functor Rj_!”.

The extension by zero Rj_! : D^b_{Coh}(𝒪_U) ⥤ Pro-D^b_{Coh}(𝒪_X) along an open immersion j of Noetherian schemes, [Stacks, Tag 0G4N]: it sends K to the pro-object of a Deligne system with value K, the one of the assignment AlgebraicGeometry.DeligneSystem.values. Its functor of points at K is L ↦ Hom_U(K, L|_U). The value at K is the pro-object of any Deligne system with value K, by AlgebraicGeometry.DeligneSystem.Value.extensionByZeroIso, and on morphisms it is computed on any morphism of inverse systems restricting to the given one, by CategoryTheory.extensionByZero_map_comp_comparison.

public def extensionByZeroOpenImmersion :
    BoundedCoherentDerived U ⥤ ProSeq (BoundedCoherentDerived X)

AlgebraicGeometry.DeligneSystem.Value.extensionByZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroOpenImmersion.lean, line 389. The attribute's comment: “Rj_! K is the pro-object of any Deligne system with value K”.

Rj_! K is the pro-object of any Deligne system with value K. Both have the functor of points L ↦ Hom_U(K, L|_U), by [Stacks, Tag 0G2H]; the identification is the restriction map.

public def extensionByZeroIso : D.proObject ≅ (extensionByZeroOpenImmersion j).obj V.obj

AlgebraicGeometry.extensionByZeroOpenImmersionHomIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroOpenImmersion.lean, line 425. The attribute's comment: “Rj_! is left adjoint to j^*”.

Stacks Project, Tag 0G4N, adjointness. Rj_! is "left adjoint" to j^* : D^b_{Coh}(𝒪_X) ⥤ D^b_{Coh}(𝒪_U): morphisms of pro-objects from Rj_! K to the constant pro-object at L are the morphisms K ⟶ L|_U,

Hom_{Pro}(Rj_! K, L) = Hom_U(K, L|_U),

naturally in K and in L. Both sides are the functor of points of Rj_! K at L, which is colim_n Hom_X(K_n, L) for a Deligne system (K_n) with restriction K, and the identification with Hom_U(K, L|_U) is Stacks 0G2H.

public def extensionByZeroOpenImmersionHomIso :
    (extensionByZeroOpenImmersion j).op ⋙ coyoneda ⋙
        (Functor.whiskeringLeft _ _ _).obj ProSeq.const ≅
      coyoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (restrictBoundedCoherentLift j)

AlgebraicGeometry.extensionByZeroOpenImmersion_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroOpenImmersion.lean, line 463. The attribute's comment: “Rj_! is exact”.

Stacks Project, Tag 0G4N, exactness. Let K ⟶ L ⟶ M ⟶ K[1] be a distinguished triangle T of D^b_{Coh}(𝒪_U). Then there is an inverse system of distinguished triangles K_n ⟶ L_n ⟶ M_n ⟶ K_n[1] of D^b_{Coh}(𝒪_X), with an identification e of its restriction to U with the constant system at T, whose vertex systems (K_n), (L_n), (M_n) are Deligne systems, and such that Rj_! sends T to its pro-system: the comparison maps

Rj_! K ⟶ (K_n), Rj_! L ⟶ (L_n), Rj_! M ⟶ (M_n), Rj_!(K[1]) ⟶ (K_n[1])

induced by e are isomorphisms of pro-objects, and they carry Rj_! of the three maps of T to the morphisms of pro-systems induced by the three maps of the triangles.

The system is the one of Stacks 0G4M; the comparison maps are isomorphisms by Stacks 0G2H, which holds for the vertex systems because they are Deligne systems, and for (K_n[1]) because it holds for (K_n).

public theorem extensionByZeroOpenImmersion_exact (T : Triangle (BoundedCoherentDerived U))
    (hT : T ∈ distTriang (BoundedCoherentDerived U)) :
    ∃ (TX : ℕᵒᵖ ⥤ Triangle (BoundedCoherentDerived X))
      (e : TX ⋙ (restrictBoundedCoherentLift j).mapTriangle ≅ (Functor.const ℕᵒᵖ).obj T),
      (∀ n, TX.obj n ∈ distTriang (BoundedCoherentDerived X)) ∧
      (∃ D : DeligneSystem j, Nonempty (TX ⋙ Triangle.π₁ ≅ D.system)) ∧
      (∃ D : DeligneSystem j, Nonempty (TX ⋙ Triangle.π₂ ≅ D.system)) ∧
      (∃ D : DeligneSystem j, Nonempty (TX ⋙ Triangle.π₃ ≅ D.system)) ∧
      IsIso (extensionByZeroComparison _ (DeligneSystem.values j).toAssignment
        (mapTriangleConstIsoπ₁ _ e)) ∧
      IsIso (extensionByZeroComparison _ (DeligneSystem.values j).toAssignment
        (mapTriangleConstIsoπ₂ _ e)) ∧
      IsIso (extensionByZeroComparison _ (DeligneSystem.values j).toAssignment
        (mapTriangleConstIsoπ₃ _ e)) ∧
      IsIso (extensionByZeroComparison _ (DeligneSystem.values j).toAssignment
        (mapTriangleConstIsoShiftπ₁ _ e)) ∧
      (extensionByZeroOpenImmersion j).map T.mor₁ ≫
          extensionByZeroComparison _ (DeligneSystem.values j).toAssignment
            (mapTriangleConstIsoπ₂ _ e) =
        extensionByZeroComparison _ (DeligneSystem.values j).toAssignment
            (mapTriangleConstIsoπ₁ _ e) ≫
          ProSeq.ofMap (Functor.whiskerLeft TX Triangle.π₁Toπ₂) ∧
      (extensionByZeroOpenImmersion j).map T.mor₂ ≫
          extensionByZeroComparison _ (DeligneSystem.values j).toAssignment
            (mapTriangleConstIsoπ₃ _ e) =
        extensionByZeroComparison _ (DeligneSystem.values j).toAssignment
            (mapTriangleConstIsoπ₂ _ e) ≫
          ProSeq.ofMap (Functor.whiskerLeft TX Triangle.π₂Toπ₃) ∧
      (extensionByZeroOpenImmersion j).map T.mor₃ ≫
          extensionByZeroComparison _ (DeligneSystem.values j).toAssignment
            (mapTriangleConstIsoShiftπ₁ _ e) =
        extensionByZeroComparison _ (DeligneSystem.values j).toAssignment
            (mapTriangleConstIsoπ₃ _ e) ≫
          ProSeq.ofMap (Functor.whiskerLeft TX Triangle.π₃Toπ₁)

Tag 0G4Q, a lemma

Tag 0G4Q in the Stacks Project.

CategoryTheory.DeligneSystemValues.proIsoDeligne_π₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemTriangles.lean, line 583. The attribute's comment: “for a Deligne-system assignment supplied as data, including the colimit identification of Stacks 0G2H as its isColimit field”.

Let j^* : 𝒟 ⥤ 𝒞 be a triangulated functor with a Deligne system assignment, and let K_n ⟶ L_n ⟶ M_n ⟶ K_n[1] be an inverse system of distinguished triangles in 𝒟. If (K_n) and (M_n) are pro-isomorphic to Deligne systems, then so is (L_n).

public theorem DeligneSystemValues.proIsoDeligne_π₂ {jstar : 𝒟 ⥤ 𝒞} [jstar.Additive]
    [jstar.CommShift ℤ] [jstar.IsTriangulated] (A : DeligneSystemValues jstar)
    (T : ℕᵒᵖ ⥤ Triangle 𝒟) (hT : ∀ n, T.obj n ∈ distTriang 𝒟)
    (hK : A.ProIsoDeligne (T ⋙ Triangle.π₁)) (hM : A.ProIsoDeligne (T ⋙ Triangle.π₃)) :
    A.ProIsoDeligne (T ⋙ Triangle.π₂)

AlgebraicGeometry.DeligneSystem.proIsoDeligneSystem_π₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemTrianglesCoherent.lean, line 45.

Let j : U ⟶ X be an open immersion of Noetherian schemes and let K_n ⟶ L_n ⟶ M_n ⟶ K_n[1] be an inverse system of distinguished triangles in D^b_{Coh}(𝒪_X). If (K_n) and (M_n) are pro-isomorphic to Deligne systems, then so is (L_n).

public theorem proIsoDeligneSystem_π₂ (T : ℕᵒᵖ ⥤ Triangle (BoundedCoherentDerived X))
    (hT : ∀ n, T.obj n ∈ distTriang (BoundedCoherentDerived X))
    (hK : ProIsoDeligneSystem j (T ⋙ Triangle.π₁))
    (hM : ProIsoDeligneSystem j (T ⋙ Triangle.π₃)) :
    ProIsoDeligneSystem j (T ⋙ Triangle.π₂)

Tag 0G4R, a lemma

Tag 0G4R in the Stacks Project.

AlgebraicGeometry.idealPowerComplexSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/IdealPowerComplex.lean, line 146. The attribute's comment: “transition maps only. This supplies the canonical maps … → H^p(I³F) → H^p(I²F) → H^p(IF) → H^p(F) of the statement, for an arbitrary scheme and an arbitrary complex of module sheaves. The Artin-Rees part of the tag — the constant c > 0, the inclusion of the image of H^p(I^nF) → H^p(F) in I^(n-c)H^p(F), the maps back, and the resulting pro-isomorphism — is not proved here and needs Noetherianness and coherence.”.

Stacks Project, Tag 0G4R (transition maps). The ideal-power subcomplexes I^n F exist and carry their canonical compatible inclusions. Taking cohomology in any degree gives the maps ⋯ → H^p(I³F) → H^p(I²F) → H^p(IF) → H^p(F).

public noncomputable def idealPowerComplexSystem {X : Scheme.{u}}
    (I : X.IdealSheafData) (F : CochainComplex X.Modules ℤ) :
    IdealPowerComplexSystem I F

Stacks.Duality.cohomologyIdealPowersProIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/IdealPowerCohomologyProIso.lean, line 166. The attribute's comment: “the pro-isomorphism, packaged as a ProIso of the two inverse sequences n ↦ H^p(I^n F^•) and n ↦ I^n H^p(F^•); the underlying data and its equations are Stacks.Duality.cohomologyIdealPowers_proIsomorphic.”.

[Stacks, Tag 0G4R] as a ProIso. Let X be a Noetherian scheme, 𝓘 ⊆ 𝒪_X a quasi-coherent sheaf of ideals and 𝓕^• a complex of coherent 𝒪_X-modules. The inverse sequence n ↦ H^p(𝓘^n𝓕^•) and the inverse sequence n ↦ 𝓘^n H^p(𝓕^•) are pro-isomorphic, in the explicit "up to refinement" form ProIso: with c the Artin-Rees constant of Stacks.Duality.cohomologyIdealPowers_proIsomorphic, both reindexings are m ↦ m + c, the forward maps are the factorizations H^p(𝓘^{m+c}𝓕^•) ⟶ 𝓘^m H^p(𝓕^•) and the backward maps are the comparisons 𝓘^{m+c} H^p(𝓕^•) ⟶ H^p(𝓘^m𝓕^•).

This is the form a pro-isomorphism is consumed in by CategoryTheory.RestrictionLifting.of_proIso, which is how the core case of [Stacks, Tag 0G2H] is transported from the ideal powers of the cohomology to the cohomology of the ideal powers.

theorem cohomologyIdealPowersProIso [IsNoetherian X] (hF : TermsCoherent F)
    (S : IdealPowerComplexSystem I F) :
    Nonempty (ProIso (cohomologySystem S p) (idealPowerSystem I (F.homology p)))

Stacks.Duality.cohomologyIdealPowers_proIsomorphic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/IdealPowerCohomologyProIsomorphism.lean, line 844. The attribute's comment: “the pro-isomorphism half, for schemes, with no boundedness assumed on the complex: the constant c > 0, the factorization of H^p(𝓘^n𝓕^•) → H^p(𝓕^•) through 𝓘^(n-c)H^p(𝓕^•) (the image containment), the canonical map 𝓘^nH^p(𝓕^•) → H^p(𝓘^(n-c)𝓕^•), the two composites, and the resulting explicit isomorphism of pro-objects via the shift n ↦ n + c. The canonical maps … → H^p(𝓘^2𝓕^•) → H^p(𝓘𝓕^•) → H^p(𝓕^•) that the tag asserts first are the ones carried by AlgebraicGeometry.IdealPowerComplexSystem, constructed unconditionally by AlgebraicGeometry.idealPowerComplexSystem.”.

Stacks 0G4R, pro-isomorphism half. Let X be a Noetherian scheme, 𝓘 ⊆ 𝒪_X a quasi-coherent sheaf of ideals and 𝓕^• a complex of coherent 𝒪_X-modules. Write 𝓗 = H^p(𝓕^•) and 𝓗_n = H^p(𝓘^n𝓕^•). There is a c > 0 such that for n ≥ c the map 𝓗_n → 𝓗 factors through 𝓘^(n-c)𝓗, there is a canonical 𝓘^n𝓗 → 𝓗_(n-c), and the two composites are the canonical maps; consequently (𝓗_n) and (𝓘^n𝓗) are isomorphic as pro-objects, by the explicit cofinal shift n ↦ n + c.

theorem cohomologyIdealPowers_proIsomorphic [IsNoetherian X]
    (hF : ∀ i : ℤ, _root_.SheafOfModules.IsCoherent (F.X i))
    (S : IdealPowerComplexSystem I F) :
    ∃ (τ : ∀ m n : ℕ, n ≤ m → (S.cohomology m p ⟶ S.cohomology n p)),
      (∀ n : ℕ, τ n n le_rfl = 𝟙 (S.cohomology n p)) ∧
      (∀ (k m n : ℕ) (hkm : m ≤ k) (hmn : n ≤ m),
        τ k m hkm ≫ τ m n hmn = τ k n (hmn.trans hkm)) ∧
      (∀ n : ℕ, τ (n + 1) n (Nat.le_succ n) = S.cohomologyTransition n p) ∧
      (∀ (m n : ℕ) (hmn : n ≤ m),
        τ m n hmn ≫ S.cohomologyToOriginal n p = S.cohomologyToOriginal m p) ∧
      ∃ c : ℕ, 0 < c ∧
        ∃ (ρ : ∀ n : ℕ, c ≤ n → (S.cohomology n p ⟶
                ((Stacks.Algebraization.idealPowerMultiple I (n - c)
                  (F.homology p)).toSheafOfModules : X.Modules)))
          (ψ : ∀ n : ℕ, c ≤ n →
                (((Stacks.Algebraization.idealPowerMultiple I n
                  (F.homology p)).toSheafOfModules : X.Modules) ⟶ S.cohomology (n - c) p)),
          (∀ (n : ℕ) (hn : c ≤ n), ρ n hn ≫
              subι (Stacks.Algebraization.idealPowerMultiple I (n - c) (F.homology p)) =
            S.cohomologyToOriginal n p) ∧
          (∀ (n : ℕ) (hn : c ≤ n), ψ n hn ≫ S.cohomologyToOriginal (n - c) p =
            subι (Stacks.Algebraization.idealPowerMultiple I n (F.homology p))) ∧
          (∀ (m n : ℕ) (hmn : n ≤ m) (hm : c ≤ m) (hn : c ≤ n),
            τ m n hmn ≫ ρ n hn = ρ m hm ≫
              subHom (idealPowerMultiple_antitone I (F.homology p)
                (Nat.sub_le_sub_right hmn c))) ∧
          (∀ (m n : ℕ) (hmn : n ≤ m) (hm : c ≤ m) (hn : c ≤ n),
            subHom (idealPowerMultiple_antitone I (F.homology p) hmn) ≫ ψ n hn =
              ψ m hm ≫ τ (m - c) (n - c) (Nat.sub_le_sub_right hmn c)) ∧
          (∀ (n : ℕ) (hn : 2 * c ≤ n),
            ρ n (by omega) ≫ ψ (n - c) (by omega) = τ n (n - c - c) (by omega)) ∧
          (∀ (n : ℕ) (hn : 2 * c ≤ n),
            ψ n (by omega) ≫ ρ (n - c) (by omega) =
              subHom (idealPowerMultiple_antitone I (F.homology p)
                (show n - c - c ≤ n by omega))) ∧
          ∃ (forward : ∀ m : ℕ, (S.cohomology (m + c) p ⟶
                  ((Stacks.Algebraization.idealPowerMultiple I m
                    (F.homology p)).toSheafOfModules : X.Modules)))
            (backward : ∀ m : ℕ,
                  (((Stacks.Algebraization.idealPowerMultiple I (m + c)
                    (F.homology p)).toSheafOfModules : X.Modules) ⟶ S.cohomology m p)),
            (∀ m : ℕ, forward m ≫
                subι (Stacks.Algebraization.idealPowerMultiple I m (F.homology p)) =
              S.cohomologyToOriginal (m + c) p) ∧
            (∀ m : ℕ, backward m ≫ S.cohomologyToOriginal m p =
              subι (Stacks.Algebraization.idealPowerMultiple I (m + c) (F.homology p))) ∧
            (∀ (m m' : ℕ) (h : m ≤ m'),
              τ (m' + c) (m + c) (Nat.add_le_add_right h c) ≫ forward m =
                forward m' ≫ subHom (idealPowerMultiple_antitone I (F.homology p) h)) ∧
            (∀ (m m' : ℕ) (h : m ≤ m'),
              subHom (idealPowerMultiple_antitone I (F.homology p)
                  (Nat.add_le_add_right h c)) ≫ backward m = backward m' ≫ τ m' m h) ∧
            (∀ m : ℕ, forward (m + c) ≫ backward m =
              τ (m + c + c) m (by omega)) ∧
            (∀ m : ℕ, backward (m + c) ≫ forward m =
              subHom (idealPowerMultiple_antitone I (F.homology p)
                (show m ≤ m + c + c by omega)))

Tag 0G4S, a lemma

Tag 0G4S in the Stacks Project.

AlgebraicGeometry.DeligneSystem.proIsoDeligneSystem_iff_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemCohomology.lean, line 203.

Stacks Project, Tag 0G4S. Let j : U ⟶ X be an open immersion of Noetherian schemes and 𝓘 ⊆ 𝒪_X a quasi-coherent sheaf of ideals with V(𝓘) = X ∖ U. Let a ≤ b be integers and (K_n) an inverse system of D^b_{Coh}(𝒪_X) such that H^i(K_n) = 0 for i ∉ [a, b]. The following are equivalent:

1. (K_n) is pro-isomorphic to a Deligne system;
2. for every p ∈ ℤ there exists a coherent 𝒪_X-module 𝓕 such that the pro-systems (H^p(K_n)) and (𝓘^n𝓕) are pro-isomorphic.

(1) ⇒ (2) is AlgebraicGeometry.DeligneSystem.exists_proIso_homology_of_proIso, from [Stacks, Tag 0G4R]; (2) ⇒ (1) is AlgebraicGeometry.DeligneSystem.proIsoDeligneSystem_of_homology, from [Stacks, Tag 0G4Q]. The ideal 𝓘 of (2) is any one cutting out X ∖ U.

public theorem proIsoDeligneSystem_iff_homology (I : X.IdealSheafData)
    (hI : (I.support : Set X) = (Set.range j.base)ᶜ) {a b : ℤ}
    (hab : a ≤ b) (K : ℕᵒᵖ ⥤ BoundedCoherentDerived X)
    (hK : ∀ (n : ℕ) (i : ℤ), i < a ∨ b < i →
      IsZero ((DerivedCategory.homologyFunctor X.Modules i).obj
        ((boundedCoherentDerived X).ι.obj (K.obj (op n))))) :
    ProIsoDeligneSystem j K ↔
      ∀ p : ℤ, ∃ F : X.Modules, F.IsCoherent ∧
        Nonempty (ProSeq.of ((K ⋙ (boundedCoherentDerived X).ι) ⋙
          DerivedCategory.homologyFunctor X.Modules p) ≅
            ProSeq.of (Stacks.Duality.idealPowerSystem I F))

CategoryTheory.DeligneSystemValues.proIsoDeligne_of_truncGELE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemTruncation.lean, line 201. The attribute's comment: “(2) implies (1) only, and with (2) in the equivalent form that each one-degree truncation system (τ^{≥p}τ^{≤p}K_n) is pro-isomorphic to a Deligne system, for a Deligne-system assignment and a t-structure supplied as data. (1) implies (2) is not proved: it is Stacks 0G4R, whose Artin-Rees content the library does not have.”.

Stacks Project, Tag 0G4S, the implication (2) ⇒ (1). Let j^* : 𝒟 ⥤ 𝒞 be a triangulated functor with a Deligne system assignment, t a t-structure on 𝒟, and (K_n) an inverse sequence of 𝒟 whose terms lie in the degree range [a, b]. If each one-degree truncation τ^{≥p}τ^{≤p}K_n, for a ≤ p ≤ b, is pro-isomorphic to a Deligne system, then (K_n) is.

public theorem DeligneSystemValues.proIsoDeligne_of_truncGELE {jstar : 𝒟 ⥤ 𝒞} [jstar.Additive]
    [jstar.CommShift ℤ] [jstar.IsTriangulated] (A : DeligneSystemValues jstar)
    (t : TStructure 𝒟) {a b : ℤ} (hab : a ≤ b) (K : ℕᵒᵖ ⥤ 𝒟)
    (hGE : ∀ n, t.IsGE (K.obj n) a) (hLE : ∀ n, t.IsLE (K.obj n) b)
    (H : ∀ p : ℤ, a ≤ p → p ≤ b → A.ProIsoDeligne (K ⋙ t.truncGELE p p)) :
    A.ProIsoDeligne K

Tag 0G4T, a lemma

Tag 0G4T in the Stacks Project.

AlgebraicGeometry.proIsoDeligneSystem_iff_forall_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DeligneSystemCovering.lean, line 271.

Stacks Project, Tag 0G4T. Let j : U → X be an open immersion of Noetherian schemes, let (K_n) be an inverse system in D^b_{Coh}(𝒪_X) and let X = W_1 ∪ … ∪ W_r be a finite open covering. Then (K_n) is pro-isomorphic to a Deligne system if and only if, for each i, the restriction (K_n|_{W_i}) is pro-isomorphic to a Deligne system with respect to the open immersion U ∩ W_i → W_i.

The covering is any family W : ι → X.Opens indexed by a finite type, with ⨆ i, W i = ⊤; the open immersion U ∩ W_i → W_i is the restriction j ∣_ W i of j.

public theorem proIsoDeligneSystem_iff_forall_restrict (j : U ⟶ X) [IsOpenImmersion j]
    [IsNoetherian X] (F : ℕᵒᵖ ⥤ BoundedCoherentDerived X) {ι : Type*} [Finite ι]
    (W : ι → X.Opens) (hW : ⨆ i, W i = ⊤) :
    ProIsoDeligneSystem j F ↔
      ∀ i, ProIsoDeligneSystem (j ∣_ W i) (F ⋙ restrictBoundedCoherentLift (W i).ι)

Tag 0G4U, a lemma

Tag 0G4U in the Stacks Project.

AlgebraicGeometry.exists_deligneSystem_proIso_derivedTensorIdealPowerSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/DerivedTensorIdealPowerDeligne.lean, line 159.

Stacks Project, Tag 0G4U. Let j : U ⟶ X be an open immersion of Noetherian schemes, let 𝓘 ⊆ 𝒪_X be a quasi-coherent sheaf of ideals with V(𝓘) = X ∖ U, and let K be in D^b_{Coh}(𝒪_X). Then the inverse system (K ⊗^L_{𝒪_X} 𝓘^n)_n is pro-isomorphic to a Deligne system whose restriction to U is constant with value K|_U.

The derived tensor product is that of [Stacks, Tag 06YU] (AlgebraicGeometry.derivedTensorIdealPowerSystem), and the pro-isomorphism is one of pro-objects of D(𝒪_X): the terms K ⊗^L 𝓘^n are not in D^b_{Coh}(𝒪_X) in general. The Deligne system produced is (𝓘^n 𝓕^•) for a bounded complex 𝓕^• of coherent modules representing K, with the given ideal sheaf 𝓘.

public theorem exists_deligneSystem_proIso_derivedTensorIdealPowerSystem (j : U ⟶ X)
    [IsOpenImmersion j] [IsNoetherian X] (I : X.IdealSheafData)
    (hI : (I.support : Set X) = (Set.range j.base)ᶜ) (K : BoundedCoherentDerived X) :
    ∃ D : DeligneSystem j,
      Nonempty (D.system ⋙ restrictBoundedCoherent j ≅
        (Functor.const ℕᵒᵖ).obj ((restrictBoundedCoherent j).obj K)) ∧
      Nonempty (ProSeq.of (derivedTensorIdealPowerSystem I K.obj) ≅
        ProSeq.of (D.system ⋙ (boundedCoherentDerived X).ι))

Sources

• Section 48.30, Tag 0G2G
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.DeligneSystem.isIso_restrictionNatTrans · AlgebraicGeometry.DeligneSystem.nonempty_isColimit_restrictionHomCocone · AlgebraicGeometry.DeligneSystem.exists_restrictIso · AlgebraicGeometry.DeligneSystem.Value.proHomEquiv · AlgebraicGeometry.DeligneSystem.existsUnique_proHom_restrict · AlgebraicGeometry.DeligneSystem.existsUnique_proIso_restrict · AlgebraicGeometry.DeligneTriangle.exists_deligneSystem_distTriang_boundedCoherent · CategoryTheory.extensionByZero

Section48.31 Preliminaries to compactly supported cohomology#

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

Tag 0G4W, a lemma

Tag 0G4W in the Stacks Project.

CategoryTheory.baseChangeShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/BaseChangeShriek.lean, line 111. The attribute's comment: “the Deligne system assignments, the adjunctions Rg_ ⊣ g^! and Rf_ ⊣ f^!, and the compatibility (j')^ ∘ g^! ≅ f^! ∘ j^ coming from Tags 0ATX and 0AU0, supplied as data”.

Stacks Project, Tag 0G4W. Let f : X ⟶ Y be a proper morphism of Noetherian schemes, let V ⊆ Y be open and let U = f^{-1}(V), with j : U ⟶ X, j' : V ⟶ Y the open immersions and g : U ⟶ V the induced morphism. There is a canonical isomorphism

Rj'_! ∘ Rg_* ≅ Rf_* ∘ Rj_!

of functors D^b_{Coh}(𝒪_U) ⥤ Pro-D^b_{Coh}(𝒪_Y).

The isomorphism is constructed, not merely asserted: on functors of points it is the chain of adjunctions CategoryTheory.baseChangeShriekPoints, which is the source's second proof.

public def baseChangeShriek :
    gstar ⋙ extensionByZero jV A' ≅ extensionByZero jU A ⋙ ProSeq.pushforward adjf

AlgebraicGeometry.extensionByZeroProperBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/BaseChangeShriekProper.lean, line 66.

Stacks Project, Tag 0G4W. Let f : X ⟶ Y be a proper morphism of Noetherian schemes, let V ⊆ Y be open and let U = f⁻¹(V), with j : U ⟶ X, j' : V ⟶ Y the open immersions and g : U ⟶ V the restriction of f. There is a canonical isomorphism

Rj'_! ∘ Rg_* ≅ Rf_* ∘ Rj_!

of functors D^b_{Coh}(𝒪_U) ⥤ Pro-D^b_{Coh}(𝒪_Y), where Rj_!, Rj'_! are the extensions by zero of [Stacks, Tag 0G4N] and Rf_* acts on pro-objects termwise.

This is the source's first proof: for a Deligne system (K_n) with value K the system (Rf_* K_n) is pro-isomorphic to a Deligne system (AlgebraicGeometry.proIsoDeligneSystem_properPushforward), and its restriction to V is constant with value Rg_* K by flat base change, so by the uniqueness of Deligne systems (Stacks 0G2H) it represents Rj'_! Rg_* K; this identification is natural in K (CategoryTheory.baseChangeShriekOfLifting).

public def extensionByZeroProperBaseChangeIso {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f]
    [IsNoetherian X] [IsNoetherian Y] (V : Y.Opens) :
    properPushforwardBoundedCoherent (f ∣_ V) ⋙ extensionByZeroOpenImmersion V.ι ≅
      extensionByZeroOpenImmersion (f ⁻¹ᵁ V).ι ⋙
        ProSeq.map (properPushforwardBoundedCoherent f)

Tag 0G4X, a lemma

Tag 0G4X in the Stacks Project.

CategoryTheory.compactificationShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/BaseChangeShriek.lean, line 133. The attribute's comment: “the Deligne system assignments, the adjunction Rf_ ⊣ f^!, and the compatibility j^ ≅ f^! ∘ (j')^* coming from Tags 0ATX and 0AU0, supplied as data”.

Stacks Project, Tag 0G4X. Let j : U ⟶ X be an open immersion of Noetherian schemes and let j' : U ⟶ X' be a compactification of U over X, with structure morphism f : X' ⟶ X. There is a canonical isomorphism

Rj_! ≅ Rf_* ∘ R(j')_!

of functors D^b_{Coh}(𝒪_U) ⥤ Pro-D^b_{Coh}(𝒪_X).

This is CategoryTheory.baseChangeShriek for the open j(U) ⊆ X and the identity U ⟶ U: the compatibility it needs becomes j^* ≅ f^! ⋙ (j')^*, which holds for a compactification because f^! is local on the source and f ∘ j' = j is an open immersion.

public def compactificationShriek {jX' : 𝒟 ⥤ 𝒞} (A₁ : DeligneSystemAssignment jX')
    {jX : 𝒟' ⥤ 𝒞} (A₂ : DeligneSystemAssignment jX)
    (κ' : jX ≅ fshriek ⋙ jX') :
    extensionByZero jX A₂ ≅ extensionByZero jX' A₁ ⋙ ProSeq.pushforward adjf

AlgebraicGeometry.extensionByZeroCompactificationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/CompactificationShriek.lean, line 291.

Stacks Project, Tag 0G4X. Let j : U ⟶ X be an open immersion of Noetherian schemes and let j' : U ⟶ X' be a compactification of U over X, with structure morphism f : X' ⟶ X (f proper, j' an open immersion and j = f ∘ j'). Then there is a canonical isomorphism

Rj_! ≅ Rf_* ∘ R(j')_!

of functors D^b_{Coh}(𝒪_U) ⥤ Pro-D^b_{Coh}(𝒪_X), where Rj_! and R(j')_! are the extensions by zero of [Stacks, Tag 0G4N] and Rf_* acts on pro-objects termwise.

The proof is the source's. Let X'' ⊆ X' be the scheme-theoretic closure of j', with j'' : U ⟶ X'' and f' : X'' ⟶ X' (AlgebraicGeometry.CompactificationOf.closure). As U is dense in X'', [Stacks, Tag 0ATU] (c) gives j''(U) = f'⁻¹(j'(U)) = (f ∘ f')⁻¹(j(U)), so the case AlgebraicGeometry.compactificationShriekOfPreimage of [Stacks, Tag 0G4W] gives Rf'_* ∘ Rj''_! ≅ Rj'_! and R(f ∘ f')_* ∘ Rj''_! ≅ Rj_!; and R(f ∘ f')_* ≅ Rf_* ∘ Rf'_* (AlgebraicGeometry.properPushforwardBoundedCoherentCompIso).

public def extensionByZeroCompactificationIso :
    extensionByZeroOpenImmersion j ≅
      extensionByZeroOpenImmersion c.immersion ⋙
        ProSeq.map (properPushforwardBoundedCoherent c.toBase)

Tag 0G4Y, a remark

Tag 0G4Y in the Stacks Project.

CategoryTheory.restrictionHomNatTrans, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroCovariance.lean, line 105. The attribute's comment: “the restriction map Hom_U(K, L|_U) → Hom_{U'}(K|_{U'}, L|_{U'}) of the display, as a transformation functorial in L”.

The displayed arrow of [Stacks, Tag 0G4Y]: the restriction map

Hom_U(K, L|_U) ⟶ Hom_{U'}(K|_{U'}, L|_{U'}),

sending α to i^* α followed by the identification e : j^* ⋙ i^* ≅ j'^*, read as a transformation of the functors L ↦ Hom_𝒞(K, j^* L) and L ↦ Hom_{𝒞'}(i^* K, j'^* L). Its naturality in L is the functoriality in L that the source uses to pin the canonical map down.

public def restrictionHomNatTrans (K : 𝒞) :
    jstar ⋙ coyoneda.obj (op K) ⟶ jstar' ⋙ coyoneda.obj (op (istar.obj K))

CategoryTheory.extensionByZeroCovariance, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroCovariance.lean, line 147. The attribute's comment: “the canonical map Rj'_!(K|_{U'}) ⟶ Rj_! K, with the functoriality in K as its naturality; the Deligne-system assignments on both sides supplied as data”.

Stacks Project, Tag 0G4Y. Let X ⊃ U ⊃ U' be open subschemes of a Noetherian scheme, let j : U ⟶ X, j' : U' ⟶ X and i : U' ⟶ U be the inclusions. There is a canonical map

Rj'_!(K|_{U'}) ⟶ Rj_! K

in Pro-D^b_{Coh}(𝒪_X), functorial for K in D^b_{Coh}(𝒪_U). Here it is produced as a transformation i^* ⋙ Rj'_! ⟶ Rj_! of functors 𝒞 ⥤ Pro-𝒟, so that the functoriality in K is its naturality.

A morphism of pro-objects is a transformation of their functors of points in the opposite direction, which is the appeal to [Stacks, Tag 0G2X] in the source; the transformation used is the restriction map CategoryTheory.restrictionHomNatTrans, whose naturality in L is the functoriality in L of the display.

public def extensionByZeroCovariance :
    istar ⋙ extensionByZero jstar' A' ⟶ extensionByZero jstar A

CategoryTheory.extensionByZeroHomEquiv_covariance, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroCovariance.lean, line 183. The attribute's comment: “the display: composing with the canonical map is the restriction map Hom_U(K, L|_U) → Hom_{U'}(K|_{U'}, L|_{U'})”.

The characterising property of the canonical map of [Stacks, Tag 0G4Y]. Under the adjointness bijections of [Stacks, Tag 0G4N], composing a morphism Rj_! K ⟶ L with the canonical map Rj'_!(K|_{U'}) ⟶ Rj_! K is the restriction map of the display:

Hom_{Pro}(Rj_! K, L) = Hom_U(K, L|_U) → Hom_{U'}(K|_{U'}, L|_{U'}) = Hom_{Pro}(Rj'_!(K|_{U'}), L)

This is the equality the source asks the canonical map to satisfy; by CategoryTheory.extensionByZeroCovariance_app_eq it determines the map.

public lemma extensionByZeroHomEquiv_covariance (K : 𝒞) (L : 𝒟)
    (f : (extensionByZero jstar A).obj K ⟶ ProSeq.const.obj L) :
    extensionByZeroHomEquiv jstar' A' (istar.obj K) L
        ((extensionByZeroCovariance jstar jstar' istar e A A').app K ≫ f) =
      istar.map (extensionByZeroHomEquiv jstar A K L f) ≫ e.hom.app L

CategoryTheory.extensionByZeroCovariance_app_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroCovariance.lean, line 210. The attribute's comment: “the canonical map is the only one inducing the restriction map on morphisms into constant pro-objects, which is the appeal to Tag 0G2X”.

The canonical map of [Stacks, Tag 0G4Y] is the unique map with its characterising property. This is what the appeal to [Stacks, Tag 0G2X] in the source provides: a morphism of pro-objects Rj'_!(K|_{U'}) ⟶ Rj_! K is determined by the induced map Hom_{Pro}(Rj_! K, L) → Hom_{Pro}(Rj'_!(K|_{U'}), L), functorially in L, so requiring that map to be the restriction map of the display leaves exactly one choice.

public lemma extensionByZeroCovariance_app_eq (K : 𝒞)
    (g : (extensionByZero jstar' A').obj (istar.obj K) ⟶ (extensionByZero jstar A).obj K)
    (hg : ∀ (L : 𝒟) (f : (extensionByZero jstar A).obj K ⟶ ProSeq.const.obj L),
      extensionByZeroHomEquiv jstar' A' (istar.obj K) L (g ≫ f) =
        istar.map (extensionByZeroHomEquiv jstar A K L f) ≫ e.hom.app L) :
    g = (extensionByZeroCovariance jstar jstar' istar e A A').app K

AlgebraicGeometry.extensionByZeroOpenCovariance, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroOpenCovariance.lean, line 113. The attribute's comment: “the canonical map Rj'_!(K|_{U'}) ⟶ Rj_! K, functorial in K”.

Stacks Project, Tag 0G4Y. Let X ⊃ U ⊃ U' be open subschemes of a Noetherian scheme X and let j : U ⟶ X, j' : U' ⟶ X be the inclusions. There is a canonical map

Rj'_!(K|_{U'}) ⟶ Rj_! K

in Pro-D^b_{Coh}(𝒪_X), functorial for K in D^b_{Coh}(𝒪_U): a transformation i^* ⋙ Rj'_! ⟶ Rj_! of functors D^b_{Coh}(𝒪_U) ⥤ Pro-D^b_{Coh}(𝒪_X), where i : U' ⟶ U is the inclusion and Rj_!, Rj'_! are the functors AlgebraicGeometry.extensionByZeroOpenImmersion.

It induces, on morphisms into a constant pro-object L, the restriction map Hom_U(K, L|_U) → Hom_{U'}(K|_{U'}, L|_{U'}) (AlgebraicGeometry.extensionByZeroOpenHomEquiv_covariance), it is the only map doing so (AlgebraicGeometry.extensionByZeroOpenCovariance_app_eq), and it is given by the inclusions (𝓘')^n 𝓕^• ⊆ 𝓘^n 𝓕^• (AlgebraicGeometry.extensionByZeroOpenCovariance_conj_eq_ofMap).

public def extensionByZeroOpenCovariance :
    restrictBoundedCoherentLift (X.homOfLE h) ⋙ extensionByZeroOpenImmersion U'.ι ⟶
      extensionByZeroOpenImmersion U.ι

AlgebraicGeometry.extensionByZeroOpenHomEquiv_covariance, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroOpenCovariance.lean, line 137. The attribute's comment: “the display: composing with the canonical map is the restriction map Hom_U(K, L|_U) → Hom_{U'}(K|_{U'}, L|_{U'})”.

The display of [Stacks, Tag 0G4Y]. Under the identifications Hom_{Pro}(Rj_! K, L) = Hom_U(K, L|_U) of [Stacks, Tag 0G2H], composing with the canonical map Rj'_!(K|_{U'}) ⟶ Rj_! K is the restriction map Hom_U(K, L|_U) → Hom_{U'}(K|_{U'}, L|_{U'}).

public lemma extensionByZeroOpenHomEquiv_covariance
    (K : BoundedCoherentDerived U.toScheme) (L : BoundedCoherentDerived X)
    (f : (extensionByZeroOpenImmersion U.ι).obj K ⟶ ProSeq.const.obj L) :
    extensionByZeroHomEquiv _ (DeligneSystem.values U'.ι).toAssignment
        ((restrictBoundedCoherentLift (X.homOfLE h)).obj K) L
        ((extensionByZeroOpenCovariance h).app K ≫ f) =
      (restrictBoundedCoherentLift (X.homOfLE h)).map
          (extensionByZeroHomEquiv _ (DeligneSystem.values U.ι).toAssignment K L f) ≫
        (restrictBoundedCoherentLiftHomOfLEIso h).hom.app L

AlgebraicGeometry.extensionByZeroOpenCovariance_app_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroOpenCovariance.lean, line 154. The attribute's comment: “the canonical map is the only one inducing the restriction map on morphisms into constant pro-objects, which is the appeal to Tag 0G2X”.

The canonical map of [Stacks, Tag 0G4Y] is the only one with the property of the display. A morphism Rj'_!(K|_{U'}) ⟶ Rj_! K of pro-objects which induces the restriction map on morphisms into every constant pro-object is the canonical map; this is the appeal to [Stacks, Tag 0G2X] in the source.

public lemma extensionByZeroOpenCovariance_app_eq
    (K : BoundedCoherentDerived U.toScheme)
    (g : (extensionByZeroOpenImmersion U'.ι).obj
        ((restrictBoundedCoherentLift (X.homOfLE h)).obj K) ⟶
      (extensionByZeroOpenImmersion U.ι).obj K)
    (hg : ∀ (L : BoundedCoherentDerived X)
      (f : (extensionByZeroOpenImmersion U.ι).obj K ⟶ ProSeq.const.obj L),
      extensionByZeroHomEquiv _ (DeligneSystem.values U'.ι).toAssignment
          ((restrictBoundedCoherentLift (X.homOfLE h)).obj K) L (g ≫ f) =
        (restrictBoundedCoherentLift (X.homOfLE h)).map
            (extensionByZeroHomEquiv _ (DeligneSystem.values U.ι).toAssignment K L f) ≫
          (restrictBoundedCoherentLiftHomOfLEIso h).hom.app L) :
    g = (extensionByZeroOpenCovariance h).app K

AlgebraicGeometry.extensionByZeroOpenCovariance_conj_eq_ofMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/ExtensionByZeroOpenCovariance.lean, line 353. The attribute's comment: “the explicit construction: the canonical map is given by the maps K'_n = (𝓘')^n 𝓕^• ⟶ 𝓘^n 𝓕^• = K_n coming from the inclusions (𝓘')^n ⊆ 𝓘^n”.

The explicit construction of [Stacks, Tag 0G4Y]. Let 𝓕^• be a bounded complex of coherent 𝒪_X-modules whose restriction to U represents K, and let 𝓘' ⊆ 𝓘 be quasi-coherent sheaves of ideals with V(𝓘) = X ∖ U and V(𝓘') = X ∖ U'. Then Rj_! K and Rj'_!(K|_{U'}) are represented by the inverse systems K_n = 𝓘^n 𝓕^• and K'_n = (𝓘')^n 𝓕^• (AlgebraicGeometry.DeligneSystem.Value.extensionByZeroIso), and under these identifications the canonical map Rj'_!(K|_{U'}) ⟶ Rj_! K is given by the maps K'_n ⟶ K_n coming from the inclusions (𝓘')^n ⊆ 𝓘^n.

The reduction to 𝓘' ⊆ 𝓘 is Stacks.AlgebraicGeometry.IdealPower.support_sup_eq_left, and such complexes exist by AlgebraicGeometry.exists_bounded_isCoherent_complex_restrict_Q_iso; such ideals exist, e.g. the vanishing ideals of the closed complements.

public theorem extensionByZeroOpenCovariance_conj_eq_ofMap :
    (DeligneSystem.ofComplexValue (j := U'.ι) I' hI' F hFge hFle hFcoh _
          (restrictValueIsoOfLE h F K φ)).extensionByZeroIso.hom ≫
        (extensionByZeroOpenCovariance h).app K ≫
        (DeligneSystem.ofComplexValue (j := U.ι) I hI F hFge hFle hFcoh K
          φ).extensionByZeroIso.inv =
      ProSeq.ofMap (idealPowerSystemCompare F hFge hFle hFcoh hI hI' hle)

Stacks.AlgebraicGeometry.IdealPower.support_sup_eq_left, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/IdealPowerComplexComparison.lean, line 79. The attribute's comment: “the reduction to 𝓘' ⊆ 𝓘 of the explicit construction: replacing 𝓘 by 𝓘 + 𝓘' leaves the vanishing locus unchanged”.

Replacing a quasi-coherent sheaf of ideals by its sum with one whose vanishing locus is larger does not change the vanishing locus. In [Stacks, Tag 0G4Y] this is the step that lets one assume 𝓘' ⊆ 𝓘: there V(𝓘) = X ∖ U and V(𝓘') = X ∖ U' with U' ⊆ U, so V(𝓘 + 𝓘') = V(𝓘), while 𝓘' ≤ 𝓘 + 𝓘'.

public lemma support_sup_eq_left {I I' : X.IdealSheafData} (h : I.support ≤ I'.support) :
    (I ⊔ I').support = I.support

AlgebraicGeometry.IdealPowerComplexSystem.compareHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/IdealPowerComplexComparison.lean, line 177. The attribute's comment: “the maps K'_n = (𝓘')^n 𝓕^• ⟶ 𝓘^n 𝓕^• = K_n of the explicit construction, induced by the inclusions (𝓘')^n ⊆ 𝓘^n”.

The maps K'_n ⟶ K_n of the explicit construction in [Stacks, Tag 0G4Y]. For 𝓘' ≤ 𝓘 the inclusions (𝓘')^n • 𝓕^i ⊆ 𝓘^n • 𝓕^i assemble into a map of complexes

(𝓘')^n 𝓕^• ⟶ 𝓘^n 𝓕^•.

The source writes K'_n = (𝓘')^n 𝓕^• and K_n = 𝓘^n 𝓕^• and describes its canonical map Rj'_!(K|_{U'}) ⟶ Rj_! K as being given by these maps.

public def compareHom (S' : IdealPowerComplexSystem I F) (S : IdealPowerComplexSystem J F)
    (h : I ≤ J) (n : ℕ) : S'.complex n ⟶ S.complex n

AlgebraicGeometry.IdealPowerComplexSystem.compareHom_comp_inclusion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/IdealPowerComplexComparison.lean, line 203. The attribute's comment: “the maps K'_n ⟶ K_n of the explicit construction are the inclusions read inside 𝓕^•, which is what pins them down”.

The comparison map of [Stacks, Tag 0G4Y] is the inclusion, read inside 𝓕^•. Composing K'_n ⟶ K_n with the inclusion of K_n into 𝓕^• gives the inclusion of K'_n. Since the inclusions are termwise monomorphisms, this characterises the comparison map.

public lemma compareHom_comp_inclusion (S' : IdealPowerComplexSystem I F)
    (S : IdealPowerComplexSystem J F) (h : I ≤ J) (n : ℕ) :
    S'.compareHom S h n ≫ S.inclusion n = S'.inclusion n

AlgebraicGeometry.IdealPowerComplexSystem.compareHom_comp_transition, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ExtensionZeroCoherent/IdealPowerComplexComparison.lean, line 213. The attribute's comment: “the maps K'_n ⟶ K_n of the explicit construction commute with the transitions, so they are a map of the inverse systems (K'_n) ⟶ (K_n)”.

The comparison maps of [Stacks, Tag 0G4Y] form a map of inverse systems. They commute with the transitions K'_{n+1} ⟶ K'_n and K_{n+1} ⟶ K_n of the two ideal-power filtrations.

public lemma compareHom_comp_transition (S' : IdealPowerComplexSystem I F)
    (S : IdealPowerComplexSystem J F) (h : I ≤ J) (n : ℕ) :
    S'.transition n ≫ S'.compareHom S h n = S'.compareHom S h (n + 1) ≫ S.transition n

Sources

• Section 48.31, Tag 0G4V
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.baseChangeShriek · AlgebraicGeometry.extensionByZeroProperBaseChangeIso · CategoryTheory.compactificationShriek · AlgebraicGeometry.extensionByZeroCompactificationIso · CategoryTheory.restrictionHomNatTrans · CategoryTheory.extensionByZeroCovariance · CategoryTheory.extensionByZeroHomEquiv_covariance · CategoryTheory.extensionByZeroCovariance_app_eq

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.