50.17 Blowing up and de Rham… to 50.24 Relative Poincaré duality

Section50.17 Blowing up and de Rham cohomology #

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

Tag 0FUU, a lemma

Tag 0FUU in the Stacks Project.

Stacks.DeRham.isIso_formsDirectImageComparison_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupSmoothCentreForms.lean, line 310. The attribute's comment: “corrected form, clause (1): Ω^a_{X/S} ⟶ b_*Ω^a_{X'/S} is an isomorphism for every a ≥ 0, for f smooth and i a closed immersion of a scheme smooth over S whose image has EMPTY INTERIOR in X. The interior hypothesis is a correction: as stated (any closed immersion of S-smooth schemes) the clause is false when Z contains a nonempty open of X — for S = X = Z = Spec k the blowup is empty and 𝒪_X ⟶ 0 is not an isomorphism (counterexample Stacks.DeRham.exists_smooth_not_isIso_formsDirectImage, untagged). The blowup is AlgebraicGeometry.blowUpToBase i.ker”.

[Stacks, Tag 0FUU], clause (1), in corrected form. Let f : X ⟶ S be smooth, let i : Z ⟶ X be a closed immersion with Z smooth over S and with image of empty interior in X, and let b : X' ⟶ X be the blowing up of X along Z. Then for every a ≥ 0 the canonical map Ω^a_{X/S} ⟶ b_*Ω^a_{X'/S} is an isomorphism.

The hypothesis on the interior is a correction of the source. The source states the clause for every closed immersion of schemes smooth over S, and it is false when Z contains a non-empty open subset of X: for S = X = Z = Spec k the blowup is empty, and 𝒪_X ⟶ 0 is not an isomorphism (Stacks.DeRham.exists_smooth_not_isIso_formsDirectImage). The proof is the source's: the étale-local reduction to the coordinate model ([Stacks, Tag 0FUE]), with clause (1) of [Stacks, Tag 0FUR] there. Empty interior is exactly what makes the codimension n ≥ 1 on every chart.

theorem isIso_formsDirectImageComparison_blowUpToBase [IsClosedImmersion i] [Smooth f]
    [Smooth (i ≫ f)] (hint : interior (Set.range i.base) = ∅) (a : ℕ) :
    IsIso (formsDirectImageComparison (blowUpToBase i.ker) f (a : ℤ))

Stacks.DeRham.isIso_formsDirectImageComparison_exceptionalDivisorToCentre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupSmoothCentreForms.lean, line 334. The attribute's comment: “corrected form, clause (2): Ω^a_{Z/S} ⟶ p_*Ω^a_{E/S} is an isomorphism for every a ≥ 0, for f smooth and i a closed immersion of a scheme smooth over S whose image has EMPTY INTERIOR in X; E is the exceptional divisor of AlgebraicGeometry.blowUpToBase i.ker and p is AlgebraicGeometry.exceptionalDivisorToCentre i. The interior hypothesis is a correction: as stated the clause is false when Z contains a nonempty open of X — for S = X = Z = Spec k, E is empty and 𝒪_Z ⟶ 0 is not an isomorphism (counterexample Stacks.DeRham.exists_smooth_not_isIso_formsDirectImageComparison_blowUpToBase, untagged)”.

[Stacks, Tag 0FUU], clause (2), in corrected form. Let f : X ⟶ S be smooth, let i : Z ⟶ X be a closed immersion with Z smooth over S and with image of empty interior in X, let E be the exceptional divisor of the blowing up of X along Z, and let p : E ⟶ Z be its structure morphism. Then for every a ≥ 0 the canonical map Ω^a_{Z/S} ⟶ p_*Ω^a_{E/S} is an isomorphism.

As in clause (1), the hypothesis on the interior corrects the source: for S = X = Z = Spec k the exceptional divisor is empty and 𝒪_Z ⟶ 0 is not an isomorphism (Stacks.DeRham.exists_smooth_not_isIso_formsDirectImageComparison_blowUpToBase). The proof is the étale-local reduction of the source to clause (2) of [Stacks, Tag 0FUR], on the exceptional divisor of the coordinate model.

theorem isIso_formsDirectImageComparison_exceptionalDivisorToCentre [IsClosedImmersion i]
    [Smooth f] [Smooth (i ≫ f)] (hint : interior (Set.range i.base) = ∅) (a : ℕ) :
    IsIso (formsDirectImageComparison (exceptionalDivisorToCentre i) (i ≫ f) (a : ℤ))

Stacks.DeRham.isIso_blowupFormsDirectImage_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupSmoothCentreFormsAffine.lean, line 248. The attribute's comment: “clause (1), corrected: false as written when Z contains a nonempty open of X (counterexample Z = X = S = Spec k: the blowup is empty and O_X → b_*O = 0), so stated for Z containing no nonempty open of X (positive codimension everywhere)”.

[Stacks, Tag 0FUU], clause (1). Let f : X ⟶ S be smooth and let i : Z ⟶ X be a closed immersion with Z smooth over S, of positive codimension at every point, i.e. containing no nonempty open subset of X. Let b : X' ⟶ X be the blowing up of X along Z. Then for every a ≥ 0 the canonical map Ω^a_{X/S} ⟶ b_*Ω^a_{X'/S} is an isomorphism.

The positivity of the codimension is not stated in the source, and it is needed: where Z contains an open subset W of X the ideal of the centre vanishes on W, the blowup is empty over W (AlgebraicGeometry.isEmpty_blowUp_bot), and 𝒪_W = Ω^0_{W/S} ⟶ b_*Ω^0 = 0 is not an isomorphism — for instance for Z = X = S = Spec k. The source's proof reduces to the coordinate situation 𝐀^m_S ⊆ 𝐀^{m+n}_S of Section 50.16, where n ≥ 1, and that is exactly what the hypothesis provides in the charts of [Stacks, Tag 0FUE].

theorem isIso_blowupFormsDirectImage_of_smooth (hint : interior (Set.range i.base) = ∅) (a : ℕ) :
    IsIso (blowupFormsDirectImage i f (a : ℤ))

Stacks.DeRham.isIso_exceptionalFormsDirectImage_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupSmoothCentreFormsAffine.lean, line 276. The attribute's comment: “clause (2), corrected: false as written when Z contains a nonempty open of X (counterexample Z = X = S = Spec k: E is empty and O_Z → p_*O_E = 0), so stated for Z containing no nonempty open of X (positive codimension everywhere)”.

[Stacks, Tag 0FUU], clause (2). Let f : X ⟶ S be smooth and let i : Z ⟶ X be a closed immersion with Z smooth over S, of positive codimension at every point, i.e. containing no nonempty open subset of X. Let p : E ⟶ Z be the projection onto the centre of the exceptional divisor of the blowing up of X along Z. Then for every a ≥ 0 the canonical map Ω^a_{Z/S} ⟶ p_*Ω^a_{E/S} is an isomorphism.

As for clause (1), the positivity of the codimension is not stated in the source and is needed: for Z = X the exceptional divisor is empty and 𝒪_Z ⟶ p_*𝒪_E = 0 is not an isomorphism.

theorem isIso_exceptionalFormsDirectImage_of_smooth (hint : interior (Set.range i.base) = ∅)
    (a : ℕ) : IsIso (exceptionalFormsDirectImage i f (a : ℤ))

Stacks.DeRham.isIso_formsDirectImage_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupSmoothCentreFormsDirectImage.lean, line 566. The attribute's comment: “clauses (1) and (2) in every integer degree, for a centre whose ideal sheaf is an effective Cartier divisor — a divisorial centre, which for a closed immersion of schemes smooth over S means codimension one at every point of the centre (the empty centre qualifying vacuously). This is the degenerate case of the tag, proved for a nearly trivial reason: blowing up an effective Cartier divisor leaves the scheme unchanged (Stacks 0807), so b : X' ⟶ X is an isomorphism, and the exceptional divisor is the fibre product of the blowup with the centre, so p : E ⟶ Z is the base change of b along i and is an isomorphism too; each comparison is then the unit of the inverse image–direct image adjunction along an isomorphism followed by the direct image of a map which is an isomorphism by Stacks 0FLV. A centre of codimension two or more is NOT proved, in any degree: none of the content of the source's proof — the étale-local reduction of Stacks 0FUE to the coordinate situation 𝐀^m_S ⊆ 𝐀^{m+n}_S, and the computation of Stacks 0FUR there — is used. In the other direction this is more general than the source: the smoothness of f and of i ≫ f is not needed for a divisorial centre and is not assumed, and every integer degree is covered, not only a ≥ 0. Clause (3) is not included: the derived comparison of Rb_ ∘ j_ against i_ ∘ Rp_ has no carrier in this library, so clause (3) has no canonical map to be a statement about”.

[Stacks, Tag 0FUU], clauses (1) and (2), for a centre which is an effective Cartier divisor. Let i : Z ⟶ X be a closed immersion whose ideal sheaf is an effective Cartier divisor, let f : X ⟶ S be any morphism, let b : X' ⟶ X be the blowing up of X along Z, let E be its exceptional divisor and let p : E ⟶ Z be the structure morphism of E over the centre. Then in every degree the comparison maps

Ω^a_{X/S} ⟶ b_*Ω^a_{X'/S} and

Ω^a_{Z/S} ⟶ p_*Ω^a_{E/S}

are isomorphisms.

This is the degenerate case of the tag, and it is proved for a nearly trivial reason. Blowing up an effective Cartier divisor leaves the scheme unchanged ([Stacks, Tag 0807]), so b is an isomorphism; the exceptional divisor is the fibre product of the blowup with the centre, so p is the base change of b along i and is an isomorphism too. Each comparison is then the unit of the inverse image–direct image adjunction along an isomorphism, followed by the direct image of a map which is an isomorphism by [Stacks, Tag 0FLV].

For a closed immersion of schemes smooth over S the ideal of the centre is locally generated by a regular sequence, by [Stacks, Tag 0FUE], so the hypothesis here holds precisely when that sequence has length one at every point of the centre — the centre is a divisor, of codimension one wherever it is non-empty. The empty centre satisfies it vacuously, its ideal being the unit ideal. The source states the tag for a centre of arbitrary codimension, and nothing of its proof — the étale-local reduction of [Stacks, Tag 0FUE] to the coordinate situation 𝐀^m_S ⊆ 𝐀^{m+n}_S and the computation of [Stacks, Tag 0FUR] there — is used. Smoothness of f and of i ≫ f is not needed for this case and is not assumed.

theorem isIso_formsDirectImage_of_isEffectiveCartierDivisor {S X Z : Scheme.{u}} (f : X ⟶ S)
    (i : Z ⟶ X) [IsClosedImmersion i]
    (hi : Stacks.Divisors.IsEffectiveCartierDivisor i.ker) (a : ℤ) :
    IsIso (blowupFormsDirectImage i f a) ∧ IsIso (exceptionalFormsDirectImage i f a)

Stacks.DeRham.isIso_homology_blowupFormsDerivedComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupSmoothCentreFormsHigherDirectImage.lean, line 56. The attribute's comment: “clause (3): for f smooth and i a closed immersion of an S-smooth scheme, Rb_Ω^a_{X'/S} ⟶ i_Rp_*Ω^a_{E/S} is an isomorphism on cohomology sheaves in every degree q ≥ 1. No interior hypothesis is needed for this clause”.

[Stacks, Tag 0FUU], clause (3). Let f : X ⟶ S be smooth and i : Z ⟶ X a closed immersion with Z smooth over S, let b : X' ⟶ X be the blowing up along Z, E its exceptional divisor and p : E ⟶ Z the structure morphism. For every a ≥ 0 and every q ≥ 1 the comparison Rb_*Ω^a_{X'/S} ⟶ i_*Rp_*Ω^a_{E/S} (Stacks.DeRham.blowupFormsDerivedComparison) is an isomorphism on H^q.

theorem isIso_homology_blowupFormsDerivedComparison [IsClosedImmersion i] [Smooth f]
    [Smooth (i ≫ f)] (a : ℕ) {q : ℤ} (hq : 1 ≤ q) :
    IsIso ((DerivedCategory.homologyFunctor X.Modules q).map
      (blowupFormsDerivedComparison f i (a : ℤ)))

Stacks.DeRham.isIso_homology_blowupFormsRestrictionDerivedComparison_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupSmoothCentreFormsKernelVanishing.lean, line 381. The attribute's comment: “clause (3): Rb_Ω^a_{X'/S} ⟶ i_Rp_*Ω^a_{E/S} is an isomorphism on cohomology sheaves in every degree q ≥ 1, every a ≥ 0, for a closed immersion of schemes smooth over S of any codimension”.

[Stacks, Tag 0FUU], clause (3). Let f : X ⟶ S be smooth and let i : Z ⟶ X be a closed immersion with Z smooth over S. Let b : X' ⟶ X be the blowing up of X along Z, with exceptional divisor E and projection p : E ⟶ Z. Then for every a ≥ 0 the canonical map Rb_*Ω^a_{X'/S} ⟶ i_*Rp_*Ω^a_{E/S} is an isomorphism on cohomology sheaves in every degree q ≥ 1, at any models of the derived categories.

No hypothesis on the codimension is needed: where Z contains an open of X, the blowup and the exceptional divisor are empty there. The proof reduces, étale locally by [Stacks, Tag 0FUE], to the coordinate situation of Section 50.16, where it is clause (3) of [Stacks, Tag 0FUR].

theorem isIso_homology_blowupFormsRestrictionDerivedComparison_of_smooth (a : ℕ) (q : ℤ)
    (hq : 0 < q) :
    IsIso ((DerivedCategory.homologyFunctor _ q).map
      (blowupFormsRestrictionDerivedComparison f i (a : ℤ)))

Tag 0FUV, a lemma

Tag 0FUV in the Stacks Project.

Stacks.DeRham.BlowupTriangle.exists_distTriang, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupDeRhamTriangleSmooth.lean, line 76. The attribute's comment: “the distinguished triangle Ω^•_{X/S} → Rb_Ω^•_{X'/S} ⊕ i_Ω^•_{Z/S} → i_Rp_Ω^•_{E/S} → Ω^•_{X/S}[1] in D(X, f^{-1}O_S) whose four maps are the canonical ones, the sign of i_Ω^•_{Z/S} → i_Rp_*Ω^•_{E/S} reversed; Z ⊂ X closed, X and Z smooth over S, any codimension”.

The blowup triangle of de Rham complexes. Let f : X ⟶ S be smooth and let i : Z ⟶ X be a closed immersion with Z smooth over S, of any codimension. Let b : X' ⟶ X be the blowing up of X along Z, with exceptional divisor j : E ⟶ X' and projection p : E ⟶ Z. Then there is a distinguished triangle

Ω^•_{X/S} ⟶ Rb_*Ω^•_{X'/S} ⊕ i_*Ω^•_{Z/S} ⟶ i_*Rp_*Ω^•_{E/S} ⟶ Ω^•_{X/S}[1]

in D(X, f^{-1}𝒪_S) whose first map has components the canonical maps Ω^•_{X/S} ⟶ Rb_*Ω^•_{X'/S} and Ω^•_{X/S} ⟶ i_*Ω^•_{Z/S}, and whose second map has components the canonical map Rb_*Ω^•_{X'/S} ⟶ i_*Rp_*Ω^•_{E/S} and the negative of the canonical map i_*Ω^•_{Z/S} ⟶ i_*Rp_*Ω^•_{E/S}, for any models of the derived categories.

theorem exists_distTriang :
    ∃ δ : exceptionalDeRham f i ⟶ (deRham f)⟦(1 : ℤ)⟧,
      Triangle.mk (biprod.lift (toBlowUp f i) (toCentre f i))
        (biprod.desc (blowUpToExceptional f i) (-centreToExceptional f i)) δ ∈
          distTriang (DerivedCategory (ModuleSheaves (inverseImageBase f)))

Tag 0FUW, a proposition

Tag 0FUW in the Stacks Project.

Stacks.DeRham.BlowupTriangle.exists_retraction_toBlowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupDeRhamSplitting.lean, line 50. The attribute's comment: “f : X -> S smooth, i : Z -> X a closed immersion with Z smooth over S, b : X' -> X the blowing up along Z; if Z has positive codimension in X at every point (used in the weaker form that Z contains no nonempty open subset of X), then Omega_{X/S} -> Rb_*Omega_{X'/S} has a splitting in D(X, (X -> S)^{-1}O_S), for any models”.

[Stacks, Tag 0FUW]: the de Rham complex splits off along a blowing up with smooth centre. Let f : X ⟶ S be smooth, i : Z ⟶ X a closed immersion with Z smooth over S, and b : X' ⟶ X the blowing up of X along Z. If Z contains no nonempty open subset of X (in particular, if Z has positive codimension in X at every point), the canonical map Ω^•_{X/S} ⟶ Rb_*Ω^•_{X'/S} has a retraction in D(X, (X ⟶ S)⁻¹𝒪_S), for any models of the derived categories.

theorem exists_retraction_toBlowUp [Smooth f] [Smooth (i ≫ f)]
    [HasDerivedCategory.{w} (ModuleSheaves (inverseImageBase f))]
    [HasDerivedCategory.{w} (ModuleSheaves (inverseImageBase (blowupMap i ≫ f)))]
    (hint : interior (Set.range i.base) = ∅) :
    ∃ r : blowUpDeRham f i ⟶ deRham f, toBlowUp f i ≫ r = 𝟙 _

Tag 0G5I, a lemma

Tag 0G5I in the Stacks Project.

Stacks.RegularSequence.subsingleton_ext_pushforward_of_isRegularClosedImmersionOfCodim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularSequence/ExtVanishingImmersion.lean, line 261. References: SGA 4½ Cycle (2.2.1), “more general”.

Let i : Z ⟶ X be a closed immersion of schemes which is regular of codimension c, let F be an arbitrary 𝒪_Z-module and let E be a locally free 𝒪_X-module. Then Ext^q_{𝒪_X}(i_*F, E) = 0 for every q < c.

theorem subsingleton_ext_pushforward_of_isRegularClosedImmersionOfCodim {Z X : Scheme.{u}}
    (i : Z ⟶ X) [IsClosedImmersion i] (c : ℕ) (hi : IsRegularClosedImmersionOfCodim i c)
    (F : Z.Modules) (E : X.Modules) (hE : Scheme.Modules.IsLocallyFree E)
    (q : ℕ) (hq : q < c) :
    Subsingleton (Abelian.Ext ((Scheme.Modules.pushforward i).obj F) E q)

Tag 0G5J, a lemma

Tag 0G5J in the Stacks Project.

Stacks.DeRham.existsUnique_blowUpFormsRetraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupFormsDerivedRetraction.lean, line 259. The attribute's comment: “both clauses reduced to the two inputs the source uses, for the canonical map Ω^a_{X/S} ⟶ Rb_*Ω^a_{X'/S} in D(𝒪_X) constructed here. NOT proved: either input. hcone is the source's Tag 0FUU (3) + 0E7D + 0G5I vanishing, and Tag 0FUU is not proved here; hv is its twist isomorphism of Tags 0G5G and 0G5H, proved only for the coordinate model”.

Stacks Project, Tag 0G5J, granted its two inputs. Let f : X ⟶ S be smooth, let I cut out a closed subscheme of X smooth over S, and let b : X' ⟶ X be the blowing up of X along it. For a ≥ 0 there is exactly one arrow Rb_*Ω^a_{X'/S} ⟶ Ω^a_{X/S} in D(𝒪_X) whose composition with the canonical Ω^a_{X/S} ⟶ Rb_*Ω^a_{X'/S} is the identity, provided:

hcone: the third term Z of a distinguished triangle on the canonical map admits no nonzero morphism to Ω^a_{X/S}. This is the hypothesis discharged in the source by [Stacks, Tag 0FUU] part (3), [Stacks, Tag 0E7D] and [Stacks, Tag 0G5I].

hv: an invertible factorization of the canonical map. This is the hypothesis discharged in the source by the twist isomorphism of [Stacks, Tags 0G5G and 0G5H].

The two smoothness hypotheses are those of the setting of [Stacks, Tag 0FUT] and are not used by the proof.

theorem existsUnique_blowUpFormsRetraction [Smooth f] [Smooth (I.subschemeι ≫ f)] (a : ℕ)
    {Z : DerivedCategory X.Modules}
    {p : blowUpFormsObj f I (a : ℤ) ⟶ Z} {q : Z ⟶ (formsSingle f (a : ℤ))⟦(1 : ℤ)⟧}
    (hT : Triangle.mk (blowUpFormsDerivedDirectImage f I (a : ℤ)) p q ∈
      distTriang (DerivedCategory X.Modules))
    (hcone : ∀ g : Z ⟶ formsSingle f (a : ℤ), g = 0)
    {D : DerivedCategory X.Modules} (v : blowUpFormsObj f I (a : ℤ) ⟶ D)
    (hv : IsIso (blowUpFormsDerivedDirectImage f I (a : ℤ) ≫ v)) :
    ∃! r : blowUpFormsObj f I (a : ℤ) ⟶ formsSingle f (a : ℤ),
      blowUpFormsDerivedDirectImage f I (a : ℤ) ≫ r = 𝟙 (formsSingle f (a : ℤ))

Stacks.DeRham.existsUnique_blowUpFormsRetraction_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/BlowupFormsRetractionCorrected.lean, line 73. The attribute's comment: “corrected form: for f smooth and i : Z ⟶ X a closed immersion of a scheme smooth over S whose image has EMPTY INTERIOR in X, and b = blowUpToBase i.ker, for every a ≥ 0 there is a unique arrow Rb_Ω^a_{X'/S} ⟶ Ω^a_{X/S} in D(𝒪_X) whose composite with the canonical Ω^a_{X/S} ⟶ Rb_Ω^a_{X'/S} is the identity. The interior hypothesis is a correction: as stated the lemma is false when Z contains a nonempty open of X — for S = X = Z = Spec k the blowup is empty (Stacks.DeRham.isEmpty_blowUp_bot) and 𝒪_X ⟶ 0 has no retraction (counterexample of 0FUU: Stacks.DeRham.exists_smooth_not_isIso_formsDirectImageComparison_blowUpToBase)”.

[Stacks, Tag 0G5J], in corrected form. Let f : X ⟶ S be smooth, let i : Z ⟶ X be a closed immersion with Z smooth over S and with image of empty interior in X, and let b : X' ⟶ X be the blowing up of X along Z. For every a ≥ 0 there is exactly one arrow Rb_*Ω^a_{X'/S} ⟶ Ω^a_{X/S} in D(𝒪_X) whose composite with the canonical map Ω^a_{X/S} ⟶ Rb_*Ω^a_{X'/S} is the identity.

The hypothesis on the interior corrects the source: for S = X = Z = Spec k the blowup is empty and 𝒪_X ⟶ 0 has no retraction (Stacks.DeRham.exists_smooth_not_isIso_formsDirectImageComparison_blowUpToBase, Stacks.DeRham.isEmpty_blowUp_bot). The proof is the source's. Existence: the canonical map followed by Rb_* of the second map of [Stacks, Tag 0G5G] is the twist map of [Stacks, Tag 0G5H] for 𝒟 = Σ_c (c - 1)E_c, an isomorphism. Uniqueness: by [Stacks, Tag 0FUU] (3) the higher direct images are pushed forward from the centre, and [Stacks, Tags 0E7D and 0G5I] kill every map from the cone to Ω^a_{X/S}.

theorem existsUnique_blowUpFormsRetraction_blowUpToBase [IsClosedImmersion i] [Smooth f]
    [Smooth (i ≫ f)] (hint : interior (Set.range i.base) = ∅) (a : ℕ) :
    ∃! r : blowUpFormsObj f i.ker (a : ℤ) ⟶ formsSingle f (a : ℤ),
      blowUpFormsDerivedDirectImage f i.ker (a : ℤ) ≫ r = 𝟙 (formsSingle f (a : ℤ))

Sources

LeanStacks.DeRham.isIso_formsDirectImageComparison_blowUpToBase · Stacks.DeRham.isIso_formsDirectImageComparison_exceptionalDivisorToCentre · Stacks.DeRham.isIso_blowupFormsDirectImage_of_smooth · Stacks.DeRham.isIso_exceptionalFormsDirectImage_of_smooth · Stacks.DeRham.isIso_formsDirectImage_of_isEffectiveCartierDivisor · Stacks.DeRham.isIso_homology_blowupFormsDerivedComparison · Stacks.DeRham.isIso_homology_blowupFormsRestrictionDerivedComparison_of_smooth · Stacks.DeRham.BlowupTriangle.exists_distTriang

Section50.18 Comparing sheaves of differential forms #

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

Tag 0FL8, a lemma

Tag 0FL8 in the Stacks Project.

Stacks.DeRham.exists_funnyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/FunnyMap.lean, line 962. The attribute's comment: “top-wedge construction”.

The top-wedge construction descends to ⋀ᵖ(L / d(M⁻¹)), independently of both the retraction and the basis: there is a family of maps whose value on the image of every η : ⋀ᵖ L is funnyMapLift p n r π d b η.

theorem exists_funnyMap (n : ℕ)
    (i : K →ₗ[R] L) (π : L →ₗ[R] Mzero)
    (d : Mneg →ₗ[R] L) (dM : Mneg →ₗ[R] Mzero)
    (_hi : Function.Injective i) (_hexact : Function.Exact i π)
    (_hπ : Function.Surjective π) (_hsquare : π.comp d = dM)
    (_hzero : Nonempty (Module.Basis (Fin n) R Mzero))
    (_hneg : Nonempty (Module.Basis (Fin n) R Mneg)) :
    ∃ c : ∀ p : ℕ, (⋀[R]^p (L ⧸ LinearMap.range d)) →ₗ[R]
        (⋀[R]^p K) ⊗[R] twoTermDeterminant R n Mneg Mzero,
      ∀ (p : ℕ) (r : L →ₗ[R] K), r.comp i = LinearMap.id →
        ∀ (b : Module.Basis (Fin n) R Mneg) (η : ⋀[R]^p L),
          c p (exteriorPower.map p (LinearMap.range d).mkQ η) =
            funnyMapLift p n r π d b η

Stacks.DeRham.funnyMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/FunnyMap.lean, line 996. The attribute's comment: “canonical maps”.

The canonical maps cᵖ : ⋀ᵖ(L / d(M⁻¹)) → ⋀ᵖK ⊗ det(M⁻¹ → M⁰) attached to the exact two-term diagram, characterized by funnyMap_apply_lift.

noncomputable def funnyMap (n : ℕ)
    (i : K →ₗ[R] L) (π : L →ₗ[R] Mzero)
    (d : Mneg →ₗ[R] L) (dM : Mneg →ₗ[R] Mzero)
    (hi : Function.Injective i) (hexact : Function.Exact i π)
    (hπ : Function.Surjective π) (hsquare : π.comp d = dM)
    (hzero : Nonempty (Module.Basis (Fin n) R Mzero))
    (hneg : Nonempty (Module.Basis (Fin n) R Mneg)) :
    ∀ p : ℕ, (⋀[R]^p (L ⧸ LinearMap.range d)) →ₗ[R]
      (⋀[R]^p K) ⊗[R] twoTermDeterminant R n Mneg Mzero

Stacks.DeRham.funnyMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/FunnyMap.lean, line 1026. The attribute's comment: “restriction to K”.

Restricting the degree-p canonical map to K is tensoring with the determinant element.

theorem funnyMap_comp (n p : ℕ)
    (i : K →ₗ[R] L) (π : L →ₗ[R] Mzero)
    (d : Mneg →ₗ[R] L) (dM : Mneg →ₗ[R] Mzero)
    (hi : Function.Injective i) (hexact : Function.Exact i π)
    (hπ : Function.Surjective π) (hsquare : π.comp d = dM)
    (hzero : Nonempty (Module.Basis (Fin n) R Mzero))
    (hneg : Nonempty (Module.Basis (Fin n) R Mneg)) (ω : ⋀[R]^p K) :
    funnyMap n i π d dM hi hexact hπ hsquare hzero hneg p
        (exteriorPower.map p ((LinearMap.range d).mkQ.comp i) ω) =
      ω ⊗ₜ[R] twoTermDeterminantElement R dM hneg

Stacks.DeRham.funnyMap_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/FunnyMap.lean, line 1082. The attribute's comment: “degree zero”.

In degree zero, the canonical map takes 1 to the determinant element.

theorem funnyMap_zero (n : ℕ)
    (i : K →ₗ[R] L) (π : L →ₗ[R] Mzero)
    (d : Mneg →ₗ[R] L) (dM : Mneg →ₗ[R] Mzero)
    (hi : Function.Injective i) (hexact : Function.Exact i π)
    (hπ : Function.Surjective π) (hsquare : π.comp d = dM)
    (hzero : Nonempty (Module.Basis (Fin n) R Mzero))
    (hneg : Nonempty (Module.Basis (Fin n) R Mneg)) :
    funnyMap n i π d dM hi hexact hπ hsquare hzero hneg 0
        (exteriorPower.ιMulti R 0 (fun j ↦ Fin.elim0 j)) =
      (exteriorPower.ιMulti R 0 (fun j ↦ Fin.elim0 j)) ⊗ₜ[R]
        twoTermDeterminantElement R dM hneg

Stacks.DeRham.funnyMap_wedge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/FunnyMap.lean, line 1104. The attribute's comment: “wedge compatibility”.

The canonical maps commute with wedging on the left by an exterior power of K.

theorem funnyMap_wedge (n q p : ℕ)
    (i : K →ₗ[R] L) (π : L →ₗ[R] Mzero)
    (d : Mneg →ₗ[R] L) (dM : Mneg →ₗ[R] Mzero)
    (hi : Function.Injective i) (hexact : Function.Exact i π)
    (hπ : Function.Surjective π) (hsquare : π.comp d = dM)
    (hzero : Nonempty (Module.Basis (Fin n) R Mzero))
    (hneg : Nonempty (Module.Basis (Fin n) R Mneg))
    (ω : ⋀[R]^q K) (η : ⋀[R]^p (L ⧸ LinearMap.range d)) :
    funnyMap n i π d dM hi hexact hπ hsquare hzero hneg (q + p)
        (exteriorPower.wedgeMul (R := R) q p
          (exteriorPower.map q ((LinearMap.range d).mkQ.comp i) ω) η) =
      (exteriorPower.wedgeMul (R := R) q p ω).rTensor
        (twoTermDeterminant R n Mneg Mzero)
        (funnyMap n i π d dM hi hexact hπ hsquare hzero hneg p η)

Tag 0H9F, a lemma

Tag 0H9F in the Stacks Project.

Stacks.DeRham.funnyMap_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Complex/FunnyMapNaturality.lean, line 41.

The canonical maps Stacks.DeRham.funnyMap are natural for compatible morphisms of two-term diagrams, provided the two terms of the complex are carried isomorphically to their scalar extensions.

theorem funnyMap_naturality
    {K₁ L₁ N₁ Z₁ K₂ L₂ N₂ Z₂ : Type*}
    [AddCommGroup K₁] [Module R₁ K₁]
    [AddCommGroup L₁] [Module R₁ L₁]
    [AddCommGroup N₁] [Module R₁ N₁]
    [AddCommGroup Z₁] [Module R₁ Z₁]
    [AddCommGroup K₂] [Module R₂ K₂]
    [AddCommGroup L₂] [Module R₂ L₂]
    [AddCommGroup N₂] [Module R₂ N₂]
    [AddCommGroup Z₂] [Module R₂ Z₂]
    (n p : ℕ)
    (i₁ : K₁ →ₗ[R₁] L₁) (π₁ : L₁ →ₗ[R₁] Z₁)
    (d₁ : N₁ →ₗ[R₁] L₁) (dM₁ : N₁ →ₗ[R₁] Z₁)
    (i₂ : K₂ →ₗ[R₂] L₂) (π₂ : L₂ →ₗ[R₂] Z₂)
    (d₂ : N₂ →ₗ[R₂] L₂) (dM₂ : N₂ →ₗ[R₂] Z₂)
    (hi₁ : Function.Injective i₁) (hexact₁ : Function.Exact i₁ π₁)
    (hπ₁ : Function.Surjective π₁) (hsquare₁ : π₁.comp d₁ = dM₁)
    (hi₂ : Function.Injective i₂) (hexact₂ : Function.Exact i₂ π₂)
    (hπ₂ : Function.Surjective π₂) (hsquare₂ : π₂.comp d₂ = dM₂)
    (hZ₁ : Nonempty (Module.Basis (Fin n) R₁ Z₁))
    (hN₁ : Nonempty (Module.Basis (Fin n) R₁ N₁))
    (hZ₂ : Nonempty (Module.Basis (Fin n) R₂ Z₂))
    (hN₂ : Nonempty (Module.Basis (Fin n) R₂ N₂))
    (k : K₁ →ₛₗ[algebraMap R₁ R₂] K₂)
    (l : L₁ →ₛₗ[algebraMap R₁ R₂] L₂)
    (neg : N₁ →ₛₗ[algebraMap R₁ R₂] N₂)
    (zero : Z₁ →ₛₗ[algebraMap R₁ R₂] Z₂)
    (hki : ∀ x, l (i₁ x) = i₂ (k x))
    (hlπ : ∀ x, zero (π₁ x) = π₂ (l x))
    (hnd : ∀ x, l (d₁ x) = d₂ (neg x))
    (negBaseChange : TensorProduct R₁ R₂ N₁ ≃ₗ[R₂] N₂)
    (zeroBaseChange : TensorProduct R₁ R₂ Z₁ ≃ₗ[R₂] Z₂)
    (hnegBaseChange : ∀ x r, negBaseChange (r ⊗ₜ[R₁] x) = r • neg x)
    (hzeroBaseChange : ∀ x r, zeroBaseChange (r ⊗ₜ[R₁] x) = r • zero x)
    (onH : (⋀[R₁]^p (L₁ ⧸ LinearMap.range d₁)) →ₛₗ[algebraMap R₁ R₂]
      (⋀[R₂]^p (L₂ ⧸ LinearMap.range d₂)))
    (onK : (⋀[R₁]^p K₁) →ₛₗ[algebraMap R₁ R₂] (⋀[R₂]^p K₂))
    (onNegTop : (⋀[R₁]^n N₁) →ₛₗ[algebraMap R₁ R₂] (⋀[R₂]^n N₂))
    (onZeroTop : (⋀[R₁]^n Z₁) →ₛₗ[algebraMap R₁ R₂] (⋀[R₂]^n Z₂))
    (onNegDual : Module.Dual R₁ (⋀[R₁]^n N₁) →ₛₗ[algebraMap R₁ R₂]
      Module.Dual R₂ (⋀[R₂]^n N₂))
    (onDet : twoTermDeterminant R₁ n N₁ Z₁ →ₛₗ[algebraMap R₁ R₂]
      twoTermDeterminant R₂ n N₂ Z₂)
    (honH : ∀ x : Fin p → L₁,
      onH (exteriorPower.ιMulti R₁ p (fun j ↦ (LinearMap.range d₁).mkQ (x j))) =
        exteriorPower.ιMulti R₂ p (fun j ↦ (LinearMap.range d₂).mkQ (l (x j))))
    (honK : ∀ x : Fin p → K₁,
      onK (exteriorPower.ιMulti R₁ p x) =
        exteriorPower.ιMulti R₂ p (fun j ↦ k (x j)))
    (honNegTop : ∀ x : Fin n → N₁,
      onNegTop (exteriorPower.ιMulti R₁ n x) =
        exteriorPower.ιMulti R₂ n (fun j ↦ neg (x j)))
    (honZeroTop : ∀ x : Fin n → Z₁,
      onZeroTop (exteriorPower.ιMulti R₁ n x) =
        exteriorPower.ιMulti R₂ n (fun j ↦ zero (x j)))
    (honNegDual : ∀ (φ : Module.Dual R₁ (⋀[R₁]^n N₁)) (x : ⋀[R₁]^n N₁),
      onNegDual φ (onNegTop x) = algebraMap R₁ R₂ (φ x))
    (honDet : ∀ (z : ⋀[R₁]^n Z₁) (φ : Module.Dual R₁ (⋀[R₁]^n N₁)),
      onDet (z ⊗ₜ[R₁] φ) = onZeroTop z ⊗ₜ[R₂] onNegDual φ) :
    (TensorProduct.map onK onDet).comp
        (funnyMap n i₁ π₁ d₁ dM₁ hi₁ hexact₁ hπ₁ hsquare₁ hZ₁ hN₁ p) =
      (funnyMap n i₂ π₂ d₂ dM₂ hi₂ hexact₂ hπ₂ hsquare₂ hZ₂ hN₂ p).comp onH

Tag 0FL9, a remark

Tag 0FL9 in the Stacks Project.

Stacks.DeRham.presentationFunnyMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Complex/LocalDescription.lean, line 336. The attribute's comment: “canonical maps”.

The canonical maps on absolute differential forms associated to a square presentation of B over A which is a relative global complete intersection: Ω^p_{B⁄ℤ} → Ω^p_{A⁄ℤ} ⊗ det(NL_{B/A}).

noncomputable def presentationFunnyMap (p : ℕ) :
    (⋀[B]^p Ω[B⁄ℤ]) →ₗ[B]
      (⋀[B]^p (B ⊗[A] Ω[A⁄ℤ])) ⊗[B]
        twoTermDeterminant B n P.toExtension.Cotangent P.toExtension.CotangentSpace

Stacks.DeRham.presentationFunnyMap_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Complex/LocalDescription.lean, line 345. The attribute's comment: “degree zero”.

In degree zero the canonical map takes the unit to the determinant element of the relative naive cotangent complex.

theorem presentationFunnyMap_zero :
    presentationFunnyMap P 0 (exteriorPower.ιMulti B 0 (fun j ↦ Fin.elim0 j)) =
      (exteriorPower.ιMulti B 0 (fun j ↦ Fin.elim0 j)) ⊗ₜ[B]
        cotangentDeterminantElement P

Stacks.DeRham.presentationFunnyMap_wedge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Complex/LocalDescription.lean, line 354. The attribute's comment: “wedge compatibility”.

The canonical maps commute with wedging by a base-changed absolute differential form on A.

theorem presentationFunnyMap_wedge (q p : ℕ) (ω : ⋀[B]^q (B ⊗[A] Ω[A⁄ℤ]))
    (η : ⋀[B]^p Ω[B⁄ℤ]) :
    presentationFunnyMap P (q + p)
        (exteriorPower.wedgeMul (R := B) q p
          (exteriorPower.map q (KaehlerDifferential.mapBaseChange ℤ A B) ω) η) =
      (exteriorPower.wedgeMul (R := B) q p ω).rTensor
        (twoTermDeterminant B n P.toExtension.Cotangent P.toExtension.CotangentSpace)
        (presentationFunnyMap P p η)

Stacks.DeRham.presentationFunnyMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Complex/LocalDescription.lean, line 367. The attribute's comment: “composition with pullback”.

Composing the canonical map on forms with pullback from A is multiplication by the determinant element of the relative naive cotangent complex.

theorem presentationFunnyMap_comp (p : ℕ) (ω : ⋀[B]^p (B ⊗[A] Ω[A⁄ℤ])) :
    presentationFunnyMap P p
        (exteriorPower.map p (KaehlerDifferential.mapBaseChange ℤ A B) ω) =
      ω ⊗ₜ[B] cotangentDeterminantElement P

Algebra.isRelativeGlobalCompleteIntersection_of_quasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/QuasiFinite.lean, line 60. The attribute's comment: “the source's B is a relative global complete intersection over A, at the level of the algebra; the presentation-level form, which is what the rest of the remark uses, is Algebra.Presentation.isRelativeGlobalCompleteIntersection_of_quasiFinite”.

A quasi-finite A-algebra B admitting a presentation B = A[x_1, …, x_n]/(f_1, …, f_n) by as many relations as variables is a relative global complete intersection over A (Definition 00SP).

theorem isRelativeGlobalCompleteIntersection_of_quasiFinite {n : ℕ}
    (P : Algebra.Presentation A B (Fin n) (Fin n)) :
    Algebra.IsRelativeGlobalCompleteIntersection A B

Declarations registered for the tag:

Algebra.Presentation.exists_basis_cotangent_relation, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/DeRham/Complex/LocalDescription.lean, line 62 (StacksFrontier): “conormal basis”.
Stacks.DeRham.cotangentDiagram, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/DeRham/Complex/LocalDescriptionQuasiFinite.lean, line 31 (StacksFrontier): “the displayed diagram itself, instantiated at a square presentation which is a relative global complete intersection: the short exact sequence 0 -> B (x)_A Omega_{A/Z} -> B (x)_P Omega_{P/Z} -> Omega_{P/A} (x)_P B -> 0 of B-modules whose outer terms are free of rank n, the two-term complex out of the conormal module into it, the commuting square identifying that complex with the cotangent complex of the presentation, and the identification of the cokernel with Omega_{B/Z} under which the base-change map from Omega_{A/Z} becomes the quotient map. The type of such diagrams is the structure Stacks.DeRham.CotangentDiagram; this is the witness, so the diagram is exhibited and not just described”.
Algebra.Presentation.isRelativeGlobalCompleteIntersection_of_quasiFinite, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/CompleteIntersection/QuasiFinite.lean, line 39 (StacksFrontier): “the relative global complete intersection: the source's A → B quasi-finite is Algebra.QuasiFinite A B, which for an algebra with a finite presentation is its Definition 00PL, and B = A[x_1, …, x_n]/(f_1, …, f_n) is a presentation with Nat.card σ = Nat.card ι”.

Tag 0H9G, a lemma

Tag 0H9G in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.GarelMaps.subsingleton_isCompatible_detNLPullbackIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Comparison/Uniqueness.lean, line 881. The attribute's comment: “at most one collection c'^p satisfying 0H9C and 0H9D compatible with c through the square, using the 07HX maps and the 0FKB identification b^*det(NL_{Y/X}) = det(NL_{Y'/X'})”.

Stacks Project, Lemma 0H9G. Consider a commutative square b ≫ f = f' ≫ a of schemes which induces an isomorphism of Y' with an open subscheme of X' ×_X Y, with f locally quasi-finite and syntomic (so that f' is too), and maps c^p : Ω^p_{Y/ℤ} ⟶ f^*Ω^p_{X/ℤ} ⊗ det(NL_{Y/X}) satisfying (0H9C) and (0H9D). Then there is at most one collection of maps c'^p : Ω^p_{Y'/ℤ} ⟶ f'^*Ω^p_{X'/ℤ} ⊗ det(NL_{Y'/X'}) satisfying (0H9C) and (0H9D) for which the squares of the lemma commute, the right-hand vertical arrows using the maps b^*Ω^p_{Y/ℤ} ⟶ Ω^p_{Y'/ℤ} and a^*Ω^p_{X/ℤ} ⟶ Ω^p_{X'/ℤ} of Section 07HX and the identification b^*det(NL_{Y/X}) = det(NL_{Y'/X'}) of Section 0FKB.

theorem GarelMaps.subsingleton_isCompatible_detNLPullbackIso (w : b ≫ f = f' ≫ a)
    [IsOpenImmersion (pullback.lift b f' w)] (hf : Syntomic f) [LocallyQuasiFinite f]
    (c : f.GarelMaps (f.detNL hf)) :
    haveI := locallyQuasiFinite_of_isOpenImmersion_lift w
    c.IsNormalized (f.deltaNL hf) → c.IsMultiplicative →
      {c' : f'.GarelMaps (f'.detNL (syntomic_of_isOpenImmersion_lift w hf)) |
        c'.IsNormalized (f'.deltaNL (syntomic_of_isOpenImmersion_lift w hf)) ∧
          c'.IsMultiplicative ∧
          GarelMaps.IsCompatible w
            (detNLPullbackIso w hf (syntomic_of_isOpenImmersion_lift w hf)).hom c c'}.Subsingleton

Tag 0H9H, a lemma

Tag 0H9H in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.exists_garelMaps_isCompatible_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Comparison/LocalCompatibility.lean, line 73. The attribute's comment: “for every y' there are opens V' ∋ y', V, U', U of the square and maps c^p_{V/U}, c^p_{V'/U'} satisfying 0H9C and 0H9D compatible in the sense of 0H9G”.

Stacks Project, Lemma 0H9H. Let b ≫ f = f' ≫ a be a commutative square of schemes which induces an isomorphism of Y' with an open subscheme of X' ×_X Y, with f locally quasi-finite and syntomic. Then for every y' ∈ Y' there are opens V' ⊆ Y', V ⊆ Y, U' ⊆ X', U ⊆ X with y' ∈ V', f'(V') ⊆ U', b(V') ⊆ V, a(U') ⊆ U and f(V) ⊆ U, and maps c^p_{V/U} and c^p_{V'/U'} satisfying (0H9C) and (0H9D) which are compatible with the restricted square in the sense of Lemma 0H9G, through the identification b^*det(NL_{V/U}) = det(NL_{V'/U'}) of Lemma 0FKB.

theorem exists_garelMaps_isCompatible_resLE (w : b ≫ f = f' ≫ a)
    [IsOpenImmersion (pullback.lift b f' w)] (hf : Syntomic f) [LocallyQuasiFinite f] (y' : Y') :
    ∃ (V' : Y'.Opens) (V : Y.Opens) (U' : X'.Opens) (U : X.Opens) (e' : V' ≤ f' ⁻¹ᵁ U')
      (hV : V' ≤ b ⁻¹ᵁ V) (hU : U' ≤ a ⁻¹ᵁ U) (e : V ≤ f ⁻¹ᵁ U), y' ∈ V' ∧
      haveI := isOpenImmersion_lift_resLE_resLE w e e' hU hV
      haveI := locallyQuasiFinite_of_isOpenImmersion_lift (resLE_comp_resLE_eq w e e' hU hV)
      ∃ (c : (f.resLE U V e).GarelMaps
          ((f.resLE U V e).detNL (IsZariskiLocalAtSource.resLE (P := @Syntomic) e hf)))
        (c' : (f'.resLE U' V' e').GarelMaps ((f'.resLE U' V' e').detNL
          (syntomic_of_isOpenImmersion_lift (resLE_comp_resLE_eq w e e' hU hV)
            (IsZariskiLocalAtSource.resLE (P := @Syntomic) e hf)))),
        c.IsNormalized
            ((f.resLE U V e).deltaNL (IsZariskiLocalAtSource.resLE (P := @Syntomic) e hf)) ∧
          c.IsMultiplicative ∧
          c'.IsNormalized ((f'.resLE U' V' e').deltaNL
            (syntomic_of_isOpenImmersion_lift (resLE_comp_resLE_eq w e e' hU hV)
              (IsZariskiLocalAtSource.resLE (P := @Syntomic) e hf))) ∧
          c'.IsMultiplicative ∧
          GarelMaps.IsCompatible (resLE_comp_resLE_eq w e e' hU hV)
            (detNLPullbackIso (resLE_comp_resLE_eq w e e' hU hV)
              (IsZariskiLocalAtSource.resLE (P := @Syntomic) e hf)
              (syntomic_of_isOpenImmersion_lift (resLE_comp_resLE_eq w e e' hU hV)
                (IsZariskiLocalAtSource.resLE (P := @Syntomic) e hf))).hom c c'

Tag 0FLA, a lemma

Tag 0FLA in the Stacks Project.

AlgebraicGeometry.GarelRule.existsUnique_isNormalized_isMultiplicative_isCompatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Comparison/ExistenceBaseChange.lean, line 335. The attribute's comment: “the unique rule c^p_{Y/X} satisfying 0H9C, 0H9D and 0H9E, and its composition with f^*Ω^p_{X/Z} → Ω^p_{Y/Z} is multiplication by δ(NL_{Y/X})”.

There exists a unique rule that to every locally quasi-finite syntomic morphism of schemes f : Y ⟶ X assigns 𝒪_Y-module maps c^p_{Y/X} : Ω^p_{Y/ℤ} ⟶ f^*Ω^p_{X/ℤ} ⊗_{𝒪_Y} det(NL_{Y/X}) for p ≥ 0 satisfying (0H9C), (0H9D) and (0H9E). In particular, the composition of c^p_{Y/X} with f^*Ω^p_{X/ℤ} ⟶ Ω^p_{Y/ℤ} is multiplication by δ(NL_{Y/X}).

theorem existsUnique_isNormalized_isMultiplicative_isCompatible :
    (∃! c : GarelRule.{u}, c.IsNormalized ∧ c.IsMultiplicative ∧ c.IsCompatible) ∧
      ∀ c : GarelRule.{u}, c.IsNormalized → c.IsMultiplicative → c.IsCompatible →
        ∀ ⦃X Y : Scheme.{u}⦄ (f : Y ⟶ X) (hf : Syntomic f) (hq : LocallyQuasiFinite f) (p : ℕ),
          f.absoluteFormsMap p ≫ c f hf hq p =
            (ρ_ (f.pullbackForms p)).inv ≫ (f.pullbackForms p ◁
              Scheme.Modules.globalSectionHom (f.detNL hf) (haveI := hq; f.deltaNL hf))

Sources

LeanStacks.DeRham.exists_funnyMap · Stacks.DeRham.funnyMap · Stacks.DeRham.funnyMap_comp · Stacks.DeRham.funnyMap_zero · Stacks.DeRham.funnyMap_wedge · Stacks.DeRham.funnyMap_naturality · Stacks.DeRham.presentationFunnyMap · Stacks.DeRham.presentationFunnyMap_zero

Section50.19 Trace maps on de Rham complexes #

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

Tag 0FK7, an example

Tag 0FK7 in the Stacks Project.

AlgebraicGeometry.NoTraceOnOneForms.mem_A_iff_flip_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/TraceMapsDe/Basic.lean, line 199. The attribute's comment: “invariant ring”.

The three quadratic monomials generate precisely the simultaneous-negation invariants.

theorem mem_A_iff_flip_eq (p : B) : p ∈ A ↔ flip p = p

AlgebraicGeometry.NoTraceOnOneForms.A_normal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/TraceMapsDe/Basic.lean, line 243. The attribute's comment: “normal domain”.

The invariant ring is a normal domain.

theorem A_normal : IsNormalDomain A

AlgebraicGeometry.NoTraceOnOneForms.A_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/TraceMapsDe/Basic.lean, line 256. The attribute's comment: “finite type”.

The invariant ring is of finite type over ℂ.

theorem A_finiteType : Algebra.FiniteType ℂ A

AlgebraicGeometry.NoTraceOnOneForms.x_dy_flip_invariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/TraceMapsDe/Basic.lean, line 261. The attribute's comment: “invariant one-form”.

Simultaneously negating the variables fixes x dy.

theorem x_dy_flip_invariant :
    flip x • KaehlerDifferential.D ℂ B (flip y) =
      x • KaehlerDifferential.D ℂ B y

AlgebraicGeometry.NoTraceOnOneForms.two_mul_x_dy_not_mem_span, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/TraceMapsDe/Basic.lean, line 268. The attribute's comment: “failure of descent for one-forms”.

The form 2 x dy does not lie in the B-span of the differentials of x², xy and y².

theorem two_mul_x_dy_not_mem_span :
    (2 : B) • (x • KaehlerDifferential.D ℂ B y) ∉
      Submodule.span B
        ({KaehlerDifferential.D ℂ B (x * x),
          KaehlerDifferential.D ℂ B (x * y),
          KaehlerDifferential.D ℂ B (y * y)} : Set Ω[B⁄ℂ])

AlgebraicGeometry.NoTraceOnOneForms.two_mul_x_dy_not_mem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/TraceMapsDe/Basic.lean, line 353. The attribute's comment: “failure of the differential map to capture the invariant form”.

Twice the invariant one-form does not come from the invariant ring.

theorem two_mul_x_dy_not_mem_range :
    (2 : B) • (x • KaehlerDifferential.D ℂ B y) ∉
      LinearMap.range (KaehlerDifferential.map ℂ ℂ A B)

Tag 0FLB, a lemma

Tag 0FLB in the Stacks Project.

AlgebraicGeometry.existsUnique_formsTraceRule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormsTrace/Main.lean, line 43.

Stacks, Lemma 0FLB. There exists a unique rule that to every finite syntomic morphism of schemes f : Y ⟶ X assigns 𝒪_X-module maps Θ^p_{Y/X} : f_*Ω^p_{Y/ℤ} ⟶ Ω^p_{X/ℤ} such that (1) the composition with Ω^p_{X/ℤ} ⊗_{𝒪_X} f_*𝒪_Y → f_*Ω^p_{Y/ℤ} is id ⊗ Trace_f (FormsTraceRule.IsTrace, on local sections ω ⊗ b ↦ b · f^*ω), and (2) the rule is compatible with base change (FormsTraceRule.IsBaseChange). The rule is formsTraceRule.

theorem existsUnique_formsTraceRule :
    ∃! Θ : FormsTraceRule.{u}, Θ.IsTrace ∧ Θ.IsBaseChange

Tag 0FLC, a proposition

Tag 0FLC in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.formsTrace_isComplexMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormsTrace/Proposition.lean, line 59.

Stacks, Proposition 0FLC. Let f : Y ⟶ X be a finite syntomic morphism of schemes. The maps Θ^p_{Y/X} : f_*Ω^p_{Y/ℤ} ⟶ Ω^p_{X/ℤ} of Lemma 0FLB (formsTrace, the rule formsTraceRule of existsUnique_formsTraceRule) define a map of complexes f_*Ω^•_{Y/ℤ} ⟶ Ω^•_{X/ℤ}: on every open U of X, Θ^{p+1}(dη) = d Θ^p(η). Moreover:

in degree 0 it is Trace_f : f_*𝒪_Y ⟶ 𝒪_X, through Ω^0 ≅ 𝒪 on both sides;

Θ(ω ∧ η) = ω ∧ Θ(η) for local sections ω of Ω^q_{X/ℤ} and η of f_*Ω^p_{Y/ℤ} (ω acting on f_*Ω^•_{Y/ℤ} through f^*);

if f is a morphism over a base scheme S, i.e. for every g : X ⟶ S, the maps Θ^p_{Y/X} induce maps f_*Ω^p_{Y/S} ⟶ Ω^p_{X/S} (compatible with Θ^p_{Y/X} through the canonical surjections Ω^p_{·/ℤ} → Ω^p_{·/S}) forming a map of complexes.

theorem formsTrace_isComplexMap :
    haveI := AlgebraicGeometry.flat hf
    haveI := AlgebraicGeometry.locallyOfFinitePresentation hf
    -- a map of complexes
    (∀ (p : ℕ) (U : X.Opens) (η : Γ(absoluteDifferentialForms Y p, f ⁻¹ᵁ U)),
      (f.formsTrace hf (p + 1)).app U
          ((Y.toSpecZ.deRhamComplex.d p (p + 1)).val.app (op (f ⁻¹ᵁ U)) η) =
        (X.toSpecZ.deRhamComplex.d p (p + 1)).val.app (op U) ((f.formsTrace hf p).app U η)) ∧
    -- (1) degree zero is the trace
    f.formsTrace hf 0 ≫ (relativeDifferentialFormsZeroIso X.toSpecZ).hom =
      (Scheme.Modules.pushforward f).map (relativeDifferentialFormsZeroIso Y.toSpecZ).hom ≫
        f.finiteTrace ∧
    -- (2) linearity over the forms of `X`
    (∀ (q p : ℕ) (U : X.Opens) (ω : Γ(absoluteDifferentialForms X q, U))
      (η : Γ(absoluteDifferentialForms Y p, f ⁻¹ᵁ U)),
      (f.formsTrace hf (q + p)).app U
          ((eqToHom (congrArg (absoluteDifferentialForms Y) (Nat.cast_add q p).symm)).val.app
            (op (f ⁻¹ᵁ U)) (((absoluteDifferentialFormsAlgebra Y).mul q p).app (op (f ⁻¹ᵁ U))
              (f.absoluteFormsPullback q U ω) η)) =
        (eqToHom (congrArg (absoluteDifferentialForms X) (Nat.cast_add q p).symm)).val.app (op U)
          (((absoluteDifferentialFormsAlgebra X).mul q p).app (op U) ω
            ((f.formsTrace hf p).app U η))) ∧
    -- (3) the relative version over a base
    (∀ {S : Scheme.{u}} (g : X ⟶ S), ∃ ΘS : ∀ p : ℕ,
        (Scheme.Modules.pushforward f).obj (relativeDifferentialForms (f ≫ g) p) ⟶
          relativeDifferentialForms g p,
      (∀ p : ℕ, (Scheme.Modules.pushforward f).map ((f ≫ g).absoluteToRelativeFormsMap p) ≫
          ΘS p = f.formsTrace hf p ≫ g.absoluteToRelativeFormsMap p) ∧
      ∀ (p : ℕ) (U : X.Opens) (η : Γ(relativeDifferentialForms (f ≫ g) p, f ⁻¹ᵁ U)),
        (ΘS (p + 1)).app U (((f ≫ g).deRhamComplex.d p (p + 1)).val.app (op (f ⁻¹ᵁ U)) η) =
          (g.deRhamComplex.d p (p + 1)).val.app (op U) ((ΘS p).app U η))

Tag 0FLD, an example

Tag 0FLD in the Stacks Project.

AlgebraicGeometry.formsTrace_app_top_eq_frameTrace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormsTrace/MonogenicExample.lean, line 123. The attribute's comment: “the map Θ_{B/A} : Ω^•_B → Ω^•_A of the example is the map of Proposition 0FLC for Spec B → Spec A on global sections”.

Stacks, Example 0FLD: the map Θ_{B/A} is the one of Proposition 0FLC. Let B have a power basis of positive dimension over A, for instance B = A[x]/(f) with f monic of degree d ≥ 1. Then Spec B → Spec A is finite syntomic (isFinite_specMap_of_powerBasis, syntomic_specMap_of_powerBasis), and on global sections the map of de Rham complexes Θ_{Spec B/Spec A} given by Scheme.Hom.formsTrace is the trace map Θ_{B/A} = frameTrace A B on the forms of B: the global section of Ω^p_{Spec B/ℤ} corresponding to a p-form x of B goes to the global section of Ω^p_{Spec A/ℤ} corresponding to Θ_{B/A}(x) (with A, B identified with their rings of global sections by the canonical isomorphisms).

theorem formsTrace_app_top_eq_frameTrace (pb : PowerBasis A B) (hdim : 0 < pb.dim)
    [Algebra A Γ(Spec (.of A), ⊤)]
    [Algebra B Γ(Spec (.of B), Spec.map (CommRingCat.ofHom (algebraMap A B)) ⁻¹ᵁ ⊤)]
    (hA : algebraMap A Γ(Spec (.of A), ⊤) = (Scheme.ΓSpecIso (.of A)).inv.hom)
    (hB : algebraMap B Γ(Spec (.of B), Spec.map (CommRingCat.ofHom (algebraMap A B)) ⁻¹ᵁ ⊤) =
      (Scheme.ΓSpecIso (.of B)).inv.hom)
    (p : ℕ) (x : ⋀[B]^p Ω[B⁄ℤ]) :
    haveI := isFinite_specMap_of_powerBasis pb
    Scheme.absoluteFormsSectionsEquiv (Spec (.of A)) (isAffineOpen_top _) p
        (((Spec.map (CommRingCat.ofHom (algebraMap A B))).formsTrace
            (syntomic_specMap_of_powerBasis pb) p).app ⊤
          ((Scheme.absoluteFormsSectionsEquiv (Spec (.of B))
              ((isAffineOpen_top _).preimage (Spec.map (CommRingCat.ofHom (algebraMap A B))))
                p).symm
            (formsMap B Γ(Spec (.of B), Spec.map (CommRingCat.ofHom (algebraMap A B)) ⁻¹ᵁ ⊤) p
              x))) =
      formsMap A Γ(Spec (.of A), ⊤) p (frameTrace A B p x)

Stacks.FormsTrace.frameTrace_oneForm_D_root, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormsTrace/MonogenicExample.lean, line 179. The attribute's comment: “Θ(dt) = -da₁”.

Stacks, Example 0FLD: Θ(dt) = -da₁. Let f = x^d + ∑_{0 ≤ i < d} a_{d - i} x^i with d ≥ 1, let B ≅ A[x]/(f) and let t ∈ B be the image of x. Then the trace map Θ_{B/A} : Ω^•_B → Ω^•_A of Proposition 0FLC sends dt to -da₁.

theorem frameTrace_oneForm_D_root (hd : 1 ≤ d)
    (e : AdjoinRoot (monicOfCoefficients d a) ≃ₐ[A] B) :
    frameTrace A B 1
        (oneForm B Ω[B⁄ℤ] (D ℤ B (e (AdjoinRoot.root (monicOfCoefficients d a))))) =
      oneForm A Ω[A⁄ℤ] (-D ℤ A (a 1))

Stacks.FormsTrace.frameTrace_root_smul_oneForm_D_root, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormsTrace/MonogenicExample.lean, line 199. The attribute's comment: “Θ(t dt) = a₁ da₁ - da₂”.

Stacks, Example 0FLD: Θ(t dt) = a₁ da₁ - da₂. Let f = x^d + ∑_{0 ≤ i < d} a_{d - i} x^i with d ≥ 2, let B ≅ A[x]/(f) and let t ∈ B be the image of x. Then the trace map Θ_{B/A} of Proposition 0FLC sends t dt to a₁ da₁ - da₂.

theorem frameTrace_root_smul_oneForm_D_root (hd : 2 ≤ d)
    (e : AdjoinRoot (monicOfCoefficients d a) ≃ₐ[A] B) :
    frameTrace A B 1 (e (AdjoinRoot.root (monicOfCoefficients d a)) •
        oneForm B Ω[B⁄ℤ] (D ℤ B (e (AdjoinRoot.root (monicOfCoefficients d a))))) =
      oneForm A Ω[A⁄ℤ] (a 1 • D ℤ A (a 1) - D ℤ A (a 2))

Stacks.FormsTrace.frameTrace_root_sq_smul_oneForm_D_root, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormsTrace/MonogenicExample.lean, line 223. The attribute's comment: “Θ(t² dt) = -a₁² da₁ + a₁ da₂ + a₂ da₁ - da₃”.

Stacks, Example 0FLD: Θ(t² dt) = -a₁² da₁ + a₁ da₂ + a₂ da₁ - da₃. Let f = x^d + ∑_{0 ≤ i < d} a_{d - i} x^i with d ≥ 3, let B ≅ A[x]/(f) and let t ∈ B be the image of x. Then the trace map Θ_{B/A} of Proposition 0FLC sends t² dt to -a₁² da₁ + a₁ da₂ + a₂ da₁ - da₃ (and the source's "modulo calculation error" is not needed).

theorem frameTrace_root_sq_smul_oneForm_D_root (hd : 3 ≤ d)
    (e : AdjoinRoot (monicOfCoefficients d a) ≃ₐ[A] B) :
    frameTrace A B 1 (e (AdjoinRoot.root (monicOfCoefficients d a)) ^ 2 •
        oneForm B Ω[B⁄ℤ] (D ℤ B (e (AdjoinRoot.root (monicOfCoefficients d a))))) =
      oneForm A Ω[A⁄ℤ] (-(a 1 ^ 2 • D ℤ A (a 1)) + a 1 • D ℤ A (a 2) + a 2 • D ℤ A (a 1) -
        D ℤ A (a 3))

Stacks.FormsTrace.frameTrace_root_pow_smul_oneForm_D_root_X_pow_sub_C, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormsTrace/MonogenicExample.lean, line 285. The attribute's comment: “for f = x^d - a: Θ(t^i dt) = 0 for i = 0, …, d - 2”.

Stacks, Example 0FLD: for f = x^d - a, Θ(t^i dt) = 0 for i = 0, …, d - 2. Let B ≅ A[x]/(x^d - a) with d ≥ 1 and let t ∈ B be the image of x. Then the trace map Θ_{B/A} of Proposition 0FLC kills t^i dt for i + 1 < d.

theorem frameTrace_root_pow_smul_oneForm_D_root_X_pow_sub_C
    (e : AdjoinRoot (Polynomial.X ^ d - C a) ≃ₐ[A] B) {i : ℕ} (hi : i + 1 < d) :
    frameTrace A B 1 (e (AdjoinRoot.root (Polynomial.X ^ d - C a)) ^ i •
        oneForm B Ω[B⁄ℤ] (D ℤ B (e (AdjoinRoot.root (Polynomial.X ^ d - C a))))) = 0

Stacks.FormsTrace.frameTrace_root_pow_pred_smul_oneForm_D_root_X_pow_sub_C, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FormsTrace/MonogenicExample.lean, line 298. The attribute's comment: “for f = x^d - a: Θ(t^{d-1} dt) = da”.

Stacks, Example 0FLD: for f = x^d - a, Θ(t^{d-1} dt) = da. Let B ≅ A[x]/(x^d - a) with d ≥ 1 and let t ∈ B be the image of x. Then the trace map Θ_{B/A} of Proposition 0FLC sends t^{d-1} dt to da.

theorem frameTrace_root_pow_pred_smul_oneForm_D_root_X_pow_sub_C
    (e : AdjoinRoot (Polynomial.X ^ d - C a) ≃ₐ[A] B) :
    frameTrace A B 1 (e (AdjoinRoot.root (Polynomial.X ^ d - C a)) ^ (d - 1) •
        oneForm B Ω[B⁄ℤ] (D ℤ B (e (AdjoinRoot.root (Polynomial.X ^ d - C a))))) =
      oneForm A Ω[A⁄ℤ] (D ℤ A a)

Tag 0FW2, a lemma

Tag 0FW2 in the Stacks Project.

AlgebraicGeometry.relativeFrobenius_relativeFormsTrace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormsTrace/RelativeFrobenius.lean, line 132. References: SGA 5 XV (1.Proposition2), “Clause a), special case”.

Stacks, Lemma 0FW2. Let p be a prime number and let X → S be a smooth morphism of relative dimension d of schemes in characteristic p. Then:

the relative Frobenius F = F_{X/S} : X → X^{(p)} (Varieties, Definition 0CC9) is finite and syntomic; it is a morphism over S, F ≫ (X^{(p)} → S) = (X → S), so F_*Ω^•_{F ≫ g} is F_{X/S,*}Ω^•_{X/S};

the corresponding map Θ_{X/X^{(p)}} : F_{X/S,*}Ω^•_{X/S} → Ω^•_{X^{(p)}/S} of Proposition 0FLC (3) (AlgebraicGeometry.Scheme.Hom.relativeFormsTrace, a map of complexes by AlgebraicGeometry.Scheme.Hom.relativeFormsTrace_deRhamComplex_d) is zero in every degree k ≠ d;

in degree d it is a surjection (an epimorphism of sheaves of modules on X^{(p)}).

theorem relativeFrobenius_relativeFormsTrace :
    haveI := isFinite_relativeFrobenius S p hS X d
    IsFinite (relativeFrobenius S p hS X).left ∧ Syntomic (relativeFrobenius S p hS X).left ∧
      (relativeFrobenius S p hS X).left ≫ ((frobeniusTwist S p hS).obj X).hom = X.hom ∧
      (∀ k ≠ d, (relativeFrobenius S p hS X).left.relativeFormsTrace
          ((frobeniusTwist S p hS).obj X).hom (syntomic_relativeFrobenius S p hS X d) k = 0) ∧
      Epi ((relativeFrobenius S p hS X).left.relativeFormsTrace
          ((frobeniusTwist S p hS).obj X).hom (syntomic_relativeFrobenius S p hS X d) d)

Sources

LeanAlgebraicGeometry.NoTraceOnOneForms.mem_A_iff_flip_eq · AlgebraicGeometry.NoTraceOnOneForms.A_normal · AlgebraicGeometry.NoTraceOnOneForms.A_finiteType · AlgebraicGeometry.NoTraceOnOneForms.x_dy_flip_invariant · AlgebraicGeometry.NoTraceOnOneForms.two_mul_x_dy_not_mem_span · AlgebraicGeometry.NoTraceOnOneForms.two_mul_x_dy_not_mem_range · AlgebraicGeometry.existsUnique_formsTraceRule · AlgebraicGeometry.Scheme.Hom.formsTrace_isComplexMap

Section50.20 Poincaré duality #

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

Tag 0FW4, a lemma

Tag 0FW4 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.hodgeDuality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/HodgeCohomology/HodgeDuality.lean, line 922. The attribute's comment: “for X nonempty smooth proper over a field k, equidimensional of dimension d: there is t : H^d(X, Omega^d) -> k, unique up to precomposition with multiplication by a unit of H^0(X, O_X), such that every pairing H^q(X, Omega^p) x H^{d-q}(X, Omega^{d-p}) -> k, (xi, xi') |-> t(xi cup xi') is perfect”.

[Stacks, Tag 0FW4]. Let k be a field and X a nonempty smooth proper scheme over k, equidimensional of dimension d. There is a k-linear map t : Hᵈ(X, Ω^d_{X/k}) ⟶ k such that for all p, q the pairing H^q(X, Ω^p_{X/k}) × H^{d-q}(X, Ω^{d-p}_{X/k}) ⟶ k, (ξ, ξ') ↦ t(ξ ∪ ξ') is perfect, and t is unique up to precomposing with multiplication by a unit of H⁰(X, 𝒪_X): a linear map t' has the same property if and only if t' = t ∘ (u · -) for a unit u of H⁰(X, 𝒪_X), and that unit is unique. The map t is the trace read through ω_X ≅ Ω^d_{X/k} ([Stacks, Tag 0FVV], part (7)).

theorem hodgeDuality [Smooth f] [Nonempty X] (d : ℕ)
    (hequi : TopologicalSpace.Equidimensional X) (hd : topologicalKrullDim X = d) :
    ∃ t : sheafCohomology f (relativeDifferentialForms f d) d →ₗ[k] k,
      (∀ p q : ℤ, (hodgePairing f d t p q).IsPerfPair) ∧
      ∀ t' : sheafCohomology f (relativeDifferentialForms f d) d →ₗ[k] k,
        (∀ p q : ℤ, (hodgePairing f d t' p q).IsPerfPair) ↔
          ∃! u : (Γ(X, ⊤))ˣ, t' = t ∘ₗ cohomologySMul f (relativeDifferentialForms f d) d u

Tag 0FW5, a lemma

Tag 0FW5 in the Stacks Project.

AlgebraicGeometry.deRhamComplex_d_zero_app_top_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/PoincareDuality/BottomDifferential.lean, line 102.

The degree-zero de Rham differential of a smooth proper scheme over a field vanishes on global sections.

theorem deRhamComplex_d_zero_app_top_eq_zero (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [Smooth f] [IsProper f]
    (B : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology X.carrier)
      (SheafOfModules.moduleOfDifferentials.{u, u, u} (inverseImageStructureMap f)))
    (D : SheafOfModules.DeRhamDifferential B) :
    ((SheafOfModules.deRhamComplex B D).d 0 1).val.app (op ⊤) = 0

Tag 0FW6, a lemma

Tag 0FW6 in the Stacks Project.

AlgebraicGeometry.TopDegreeDifferential.rightDerived_map_deRham_d_eq_zero_of_isProper_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/PoincareDuality/TopDifferentialSpreadOut.lean, line 298. The attribute's comment: “for X smooth proper over a field k, equidimensional of dimension d, the map d : H^d(X, Omega^{d-1}_{X/k}) -> H^d(X, Omega^d_{X/k}) is zero”.

[Stacks, Tag 0FW6]. Let k be a field and X a smooth proper scheme over k, equidimensional of dimension d. Then the map d : Hᵈ(X, Ω^{d-1}_{X/k}) ⟶ Hᵈ(X, Ω^d_{X/k}) induced by the de Rham differential is zero. The dualizing module of a smooth proper scheme over a field is its sheaf of top forms by [Stacks, Tag 0FVV], part (7).

theorem rightDerived_map_deRham_d_eq_zero_of_isProper_of_smooth {k : Type u} [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f] [Smooth f]
    (hequi : TopologicalSpace.Equidimensional X) (d : ℕ)
    (hd : topologicalKrullDim X = (d : WithBot ℕ∞)) :
    ((sectionsFunctor X.carrier ⊤).rightDerived d).map
      ((SheafOfModules.toSheaf _).map (f.deRhamComplex.d (d - 1) d)) = 0

Tag 0FW7, a proposition

Tag 0FW7 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.deRhamPoincareDuality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/PoincareDuality/DeRhamPoincareDuality.lean, line 697. The attribute's comment: “for X nonempty smooth proper over a field k, equidimensional of dimension d: there is t : H^{2d}_dR(X/k) -> k, unique up to precomposition with multiplication by a unit of H^0(X, O_X), such that for all i the pairing H^i_dR(X/k) x H^{2d-i}_dR(X/k) -> k, (xi, xi') |-> t(xi cup xi') is perfect”.

Poincaré duality for de Rham cohomology ([Stacks, Tag 0FW7]). Let k be a field and X a nonempty smooth proper scheme over k, equidimensional of dimension d. There is a k-linear map t : H^{2d}_{dR}(X/k) ⟶ k such that for every i the pairing Hⁱ_{dR}(X/k) × H^{2d-i}_{dR}(X/k) ⟶ k, (ξ, ξ') ↦ t(ξ ∪ ξ') is perfect, and t is unique up to precomposing with multiplication by a unit of H⁰(X, 𝒪_X): a linear map t' has the same property if and only if t' = t(ξ ∪ -) for the class ξ ∈ H⁰_{dR}(X/k) of a unit u of H⁰(X, 𝒪_X) — H⁰_{dR}(X/k) = H⁰(X, 𝒪_X) through Ω^•_{X/k} ⟶ 𝒪_X[0] (bijective_deRhamCohomologyZeroToSections) — and that unit is unique.

The cup product is that of Section 0FM3 (AlgebraicGeometry.Scheme.Hom.deRhamCup, see deRhamCupBilinear_apply), defined for X with affine diagonal; a scheme proper over a field is separated, so it has affine diagonal.

theorem deRhamPoincareDuality [IsProper f] [Smooth f] [Nonempty X] (d : ℕ)
    (hequi : TopologicalSpace.Equidimensional X) (hdim : topologicalKrullDim X = d) :
    letI := AlgebraicGeometry.DeRhamTypeComplex.isAffineHom_diagonal_of_isProper f
    ∃ t : deRhamCohomologyOverField f ((d : ℤ) + d) →ₗ[k] k,
      (∀ i : ℤ, ((deRhamCupBilinear f i ((d : ℤ) + d - i) ((d : ℤ) + d) (by ring)).compr₂
        t).IsPerfPair) ∧
      ∀ t' : deRhamCohomologyOverField f ((d : ℤ) + d) →ₗ[k] k,
        (∀ i : ℤ, ((deRhamCupBilinear f i ((d : ℤ) + d - i) ((d : ℤ) + d) (by ring)).compr₂
          t').IsPerfPair) ↔
          ∃! u : (Γ(X, ⊤))ˣ, ∃ ξ : deRhamCohomologyOverField f 0,
            deRhamCohomologyZeroToSections f ξ = u ∧
              t' = t ∘ₗ deRhamCupBilinear f 0 ((d : ℤ) + d) ((d : ℤ) + d) (zero_add _) ξ

Sources

LeanAlgebraicGeometry.Scheme.Hom.hodgeDuality · AlgebraicGeometry.deRhamComplex_d_zero_app_top_eq_zero · AlgebraicGeometry.TopDegreeDifferential.rightDerived_map_deRham_d_eq_zero_of_isProper_of_smooth · AlgebraicGeometry.Scheme.Hom.deRhamPoincareDuality

Section50.21 Chern classes #

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

Tag 0FW9, a lemma

Tag 0FW9 in the Stacks Project.

Stacks.DeRhamChern.existsUnique_deRhamTotalChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/WeilCohomology/DeRhamTotalChernClass.lean, line 110. The attribute's comment: “there is a unique rule assigning to every quasi-compact and quasi-separated scheme X a total Chern class c^dR : K_0(Vect(X)) -> prod_{i >= 0} H^{2i}_dR(X/Z) with (1) c^dR(alpha + beta) = c^dR(alpha) c^dR(beta), (2) c^dR(f^alpha) = f^c^dR(alpha) for every morphism f : X -> X' of quasi-compact and quasi-separated schemes, (3) c^dR([L]) = 1 + c_1^dR(L) for L in Pic(X)”.

There is a unique rule which assigns to every quasi-compact and quasi-separated scheme X a total Chern class c^{dR} : K₀(Vect(X)) ⟶ ∏_{i ≥ 0} H^{2i}_{dR}(X/𝐙), read by components c X α i ∈ H^{2i}_{dR}(X/𝐙) in the even-degree ring, such that c(α + β) = c(α) c(β) (and c(0) = 1), c(f^*α) = f^*c(α) and c([ℒ]) = 1 + c₁^{dR}(ℒ) (Stacks.DeRhamChern.IsDeRhamTotalChernClass).

theorem existsUnique_deRhamTotalChernClass :
    ∃! c : ∀ X : (QCQSScheme (Spec (CommRingCat.of ℤ))).FullSubcategory,
        VectorBundleKZero ((QCQSScheme (Spec (CommRingCat.of ℤ))).ι.obj X).left → ℕ →
          evenDeRhamRing ((QCQSScheme (Spec (CommRingCat.of ℤ))).ι.obj X).hom,
      IsDeRhamTotalChernClass (QCQSScheme (Spec (CommRingCat.of ℤ))).ι c

Tag 0FWA, a remark

Tag 0FWA in the Stacks Project.

Stacks.DeRhamChern.exists_injective_pull_hasInvertibleFiltration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/WeilCohomology/DeRhamSplittingTwist.lean, line 61. The attribute's comment: “the analogue of Weil Cohomology Theories, Lemma 0FI7 (splitting principle) holds for de Rham Chern classes on quasi-compact and quasi-separated schemes: for a finite collection of locally free O_X-modules E_i of ranks r_i there is p : P -> X with p^ injective on (+)_i H^{2i}_dR(-/Z) and each p^E_i filtered with invertible successive quotients”.

Stacks Project, Tag 0FWA: the splitting principle for de Rham cohomology. Let X be a quasi-compact and quasi-separated scheme and let ℰ_i be a finite collection of locally free 𝒪_X-modules of ranks r_i. There is a morphism p : P ⟶ X of quasi-compact and quasi-separated schemes such that

p^* : ⨁_i H^{2i}_{dR}(X/𝐙) ⟶ ⨁_i H^{2i}_{dR}(P/𝐙) is injective,

each p^*ℰ_i has a filtration whose successive quotients ℒ_{i,1}, …, ℒ_{i,r_i} are invertible 𝒪_P-modules.

The projection is moreover flat. This is Tag 0FI7 in the de Rham situation of the proof of Tag 0FW9.

theorem exists_injective_pull_hasInvertibleFiltration
    (X : (QCQSScheme (Spec (CommRingCat.of ℤ))).FullSubcategory) (I : Type*) [Finite I]
    (E : I → ((QCQSScheme.toScheme (Spec (CommRingCat.of ℤ))).obj X).Modules) (r : I → ℕ)
    (hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{0, 0, 0} (E i) (r i)) :
    ∃ (P : (QCQSScheme (Spec (CommRingCat.of ℤ))).FullSubcategory) (p : P ⟶ X),
      Flat ((QCQSScheme.toScheme (Spec (CommRingCat.of ℤ))).map p) ∧
      Function.Injective (pull (QCQSScheme (Spec (CommRingCat.of ℤ))).ι p) ∧
      ∀ i, HasInvertibleFiltration ((QCQSScheme.toScheme (Spec (CommRingCat.of ℤ))).obj P)
        ((Scheme.Modules.pullback ((QCQSScheme.toScheme (Spec (CommRingCat.of ℤ))).map p)).obj
          (E i)) (r i)

Stacks.DeRhamChern.IsDeRhamTotalChernClass.apply_classOf_tensorObj_invertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/WeilCohomology/DeRhamSplittingTwist.lean, line 86. The attribute's comment: “the analogue of Weil Cohomology Theories, Lemma 0FI8 (chern classes of tensor products) holds for de Rham Chern classes on quasi-compact and quasi-separated schemes: for the de Rham total Chern class c^dR of Tag 0FW9, E finite locally free of constant rank r, L invertible and i <= r, c^dR_i(E (x) L) = sum_{j=0}^i binom(r-i+j, j) c^dR_{i-j}(E) cup c_1^dR(L)^j”.

Stacks Project, Tag 0FWA: the Chern classes of a twist for de Rham Chern classes. Let c^{dR} be the de Rham total Chern class of Tag 0FW9 (by that lemma there is exactly one rule with its three properties), let X be a quasi-compact and quasi-separated scheme, ℰ a finite locally free 𝒪_X-module of constant rank r and ℒ an invertible 𝒪_X-module. Then for i ≤ r

c^{dR}_i(ℰ ⊗ ℒ) = ∑_{j=0}^{i} binom(r - i + j, j) c^{dR}_{i-j}(ℰ) ∪ c₁^{dR}(ℒ)^j

in H^{2i}_{dR}(X/𝐙). This is Tag 0FI8 in the de Rham situation of the proof of Tag 0FW9.

theorem IsDeRhamTotalChernClass.apply_classOf_tensorObj_invertible
    {c : ∀ X : (QCQSScheme (Spec (CommRingCat.of ℤ))).FullSubcategory,
      VectorBundleKZero ((QCQSScheme (Spec (CommRingCat.of ℤ))).ι.obj X).left → ℕ →
        evenDeRhamRing ((QCQSScheme (Spec (CommRingCat.of ℤ))).ι.obj X).hom}
    (hc : IsDeRhamTotalChernClass (QCQSScheme (Spec (CommRingCat.of ℤ))).ι c)
    (X : (QCQSScheme (Spec (CommRingCat.of ℤ))).FullSubcategory)
    (E L : ((QCQSScheme (Spec (CommRingCat.of ℤ))).ι.obj X).left.Modules) (r : ℕ)
    (hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{0, 0, 0} E r)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible
      ((QCQSScheme (Spec (CommRingCat.of ℤ))).ι.obj X).left.presheaf
      ((QCQSScheme (Spec (CommRingCat.of ℤ))).ι.obj X).left.ringCatSheaf.2 L)
    (i : ℕ) (hi : i ≤ r) :
    c X (VectorBundleKZero.classOf _
        (Scheme.Modules.tensorObjRingedSpace
          ((QCQSScheme (Spec (CommRingCat.of ℤ))).ι.obj X).left E L)) i =
      ∑ j ∈ Finset.range (i + 1), (r - i + j).choose j •
        (c X (VectorBundleKZero.classOf _ E) (i - j) *
          c₁ (QCQSScheme (Spec (CommRingCat.of ℤ))).ι X
            (picardClassOf ((QCQSScheme (Spec (CommRingCat.of ℤ))).ι.obj X).left L hL) ^ j)

Tag 0FWB, a lemma

Tag 0FWB in the Stacks Project.

Stacks.DeRhamChern.existsUnique_deRhamChernCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/WeilCohomology/DeRhamChernCharacter.lean, line 74. The attribute's comment: “the unique rule ch^dR : K_0(Vect(X)) -> prod_i H^{2i}_dR(X/Q) on quasi-compact quasi-separated schemes X over Q, with (1) ch^dR a ring map, (2) f^ ch^dR = ch^dR f^ on all of K_0 for every morphism f : X' -> X of quasi-compact quasi-separated schemes over Q, (3) ch^dR([L]) = exp(c_1^dR(L)) for L in Pic(X); prod H^{2i} read as sequences of components in ⨁ H^{2j} with the i-th in H^{2i}. Proved from Tag 0FI9 at the standing situation sourceChernSetupRat, whose axioms are all proved: (1) Tag 0FM3, (2) the clopen splitting, (3) Tag 0FMD, (4) Proposition 0FMT, (5) Lemmas 0FMX and 0FMY, clauses (1)-(3)(c) of the category”.

Stacks Project, Tag 0FWB. There is a unique rule which assigns to every quasi-compact and quasi-separated scheme X over 𝐐 a Chern character ch^{dR} : K₀(Vect(X)) ⟶ ∏_{i ≥ 0} H^{2i}_{dR}(X/𝐐) such that (1) ch^{dR} is a ring map, (2) f^* ∘ ch^{dR} = ch^{dR} ∘ f^* for every morphism f : X' ⟶ X of quasi-compact and quasi-separated schemes over 𝐐, and (3) ch^{dR}([ℒ]) = exp(c₁^{dR}(ℒ)) for ℒ ∈ Pic(X).

An element of ∏_{i ≥ 0} H^{2i}_{dR}(X/𝐐) is the sequence of its components, the i-th read in ⨁_j H^{2j}_{dR}(X/𝐐) and lying in H^{2i}_{dR}(X/𝐐); the properties are Stacks.DeRhamChern.IsDeRhamChernCharacter. The proof is the source's: the category of quasi-compact and quasi-separated schemes over 𝐐 with A(X) = ⨁_i H^{2i}_{dR}(X/𝐐) satisfies the axioms of Section 45.12, and A(X) is a 𝐐-algebra, so Proposition 0FI9 applies.

theorem existsUnique_deRhamChernCharacter :
    ∃! ch : ∀ X : (QCQSScheme specRat).FullSubcategory,
        VectorBundleKZero X.obj.left → ℕ → evenDeRhamRing X.obj.hom,
      IsDeRhamChernCharacter (QCQSScheme specRat).ι ch

Sources

LeanStacks.DeRhamChern.existsUnique_deRhamTotalChernClass · Stacks.DeRhamChern.exists_injective_pull_hasInvertibleFiltration · Stacks.DeRhamChern.IsDeRhamTotalChernClass.apply_classOf_tensorObj_invertible · Stacks.DeRhamChern.existsUnique_deRhamChernCharacter

Section50.22 A Weil cohomology theory #

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

Tag 0FWD, a proposition

Tag 0FWD in the Stacks Project.

Stacks.WeilDeRham.exists_weilCohomologyTheory_deRham, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilDeRham/DeRhamWeilCohomologyTheory.lean, line 84. The attribute's comment: “de Rham cohomology over a field of characteristic zero is a Weil cohomology theory (Definition 0FI2, coefficients k), with data (D0)-(D3) those of de Rham cohomology: F(1) = k, H^ = H^_dR(-/k) with cup product and pullbacks, gamma from c_1^dR (0FIF), trace lambda of (A6)”.

Stacks Project, Proposition 0FWD: for a field k of characteristic zero, the functor X ↦ H^*_{dR}(X/k) on smooth projective schemes over k is a Weil cohomology theory over k with coefficients in k (Definition 0FI2).

Formulation: there is a Weil cohomology theory W : WeilCohomologyTheory k k (Definition 0FI2: data (D0) – (D3) satisfying (A), (B), (C) and condition (2) of Lemma 0FI0) whose data (D0) – (D3) are those of de Rham cohomology. These are h.toWeilData … for h a cohomological Chern character (Tag 0FIE) of the de Rham data deRhamFirstChernClassData k of Section 0FWC, so that * (D0) F(1) is k; * (D1) H^*(X) is H^*_{dR}(X/k), with its grading, cup product and pullbacks (W.H, W.grade, the ring structure and W.pull are those of deRhamFirstChernClassData k); * (D2) the cycle class map γ is the one of Lemma 0FIF built from the de Rham first Chern class c₁^{dR} (the Chern character ch is determined by c₁^{dR}, FirstChernClassData.existsUnique_isCohomologicalChernCharacter); * (D3) ∫_X is the trace map λ_X of axiom (A6), normalised by (1 ⊗ λ_X)γ([Δ]) = 1.

The proof assembles axioms (A1) – (A8) for de Rham cohomology and applies Proposition 0FIU.

theorem exists_weilCohomologyTheory_deRham [CharZero k] :
    ∃ W : WeilCohomologyTheory k k, ∃ ch,
      ∃ h : (deRhamFirstChernClassData k).IsCohomologicalChernCharacter ch,
        W.toWeilData = h.toWeilData coproductAxiom deRham_projectiveBundleAxiom
          (deRham_kunnethAxiom k) (deRham_traceAxiom h)

Tag 0FWE, a remark

Tag 0FWE in the Stacks Project.

Stacks.HodgeWeil.exists_weilCohomologyTheory_hodge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/HodgeWeil/HodgeWeilCohomologyTheory.lean, line 218. The attribute's comment: “part 1 (the first sentence): for k of characteristic zero, Hodge cohomology H^_Hodge(-/k) with c_1^Hodge is a Weil cohomology theory (Definition 0FI2, coefficients k), with data (D0)-(D3) those of Hodge cohomology: F(1) = k, H^ = H^*_Hodge(-/k) with cup product and pullbacks, gamma from c_1^Hodge (0FIF), trace lambda of (A6). Part 2 (the consequence) is degeneratesAt_one_of_finrank_grade_eq”.

Stacks Project, Remark 0FWE, part 1: for a field k of characteristic zero, Hodge cohomology X ↦ H^*_{Hodge}(X/k) = ⨁_{p, q} H^q(X, Ω^p_{X/k}) on smooth projective schemes over k, equipped with c₁^{Hodge}, determines a Weil cohomology theory over k with coefficients in k (Definition 0FI2).

Formulation, as for de Rham cohomology (Proposition 0FWD, Stacks.WeilDeRham.exists_weilCohomologyTheory_deRham): there is a Weil cohomology theory W : WeilCohomologyTheory k k (data (D0) – (D3) satisfying (A), (B), (C) and condition (2) of Lemma 0FI0) whose data are h.toWeilData … for a cohomological Chern character h (Tag 0FIE) of the Hodge data hodgeFirstChernClassData k, so that * (D0) F(1) is k; * (D1) H^*(X) is H^*_{Hodge}(X/k) graded by total degree, with its cup product and pullbacks; * (D2) the cycle class map γ is the one of Lemma 0FIF built from c₁^{Hodge} (the Chern character is determined by c₁^{Hodge}, FirstChernClassData.existsUnique_isCohomologicalChernCharacter); * (D3) ∫_X is the trace map λ_X of axiom (A6), normalised by (1 ⊗ λ_X)γ([Δ]) = 1.

The proof is the one of Proposition 0FWD: (A1) – (A8) for the Hodge data and Proposition 0FIU.

theorem exists_weilCohomologyTheory_hodge [CharZero k] :
    ∃ W : WeilCohomologyTheory k k, ∃ ch,
      ∃ h : (hodgeFirstChernClassData k).IsCohomologicalChernCharacter ch,
        W.toWeilData = h.toWeilData (hodge_coproductAxiom k) (hodge_projectiveBundleAxiom k)
          (hodge_kunnethAxiom k) (hodge_traceAxiom k h)

Stacks.HodgeWeil.degeneratesAt_one_of_finrank_grade_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/HodgeWeil/HodgeWeilCohomologyTheory.lean, line 260. The attribute's comment: “part 2 (the amusing consequence): over k of characteristic zero, if the betti numbers dim_F H^n(X) of Weil cohomology theories (any coefficient fields F of characteristic zero) do not depend on the theory, then for every smooth projective X over k the Hodge-to-de Rham spectral sequence (every brutal-truncation spectral sequence of the de Rham complex abutting to H^*_dR(X/k), 0FM7) degenerates at E_1. Part 1 is exists_weilCohomologyTheory_hodge”.

Stacks Project, Remark 0FWE, part 2 (the "amusing consequence"): let k be a field of characteristic zero. If the betti numbers of a Weil cohomology theory over k are independent of the chosen Weil cohomology theory, then the Hodge-to-de Rham spectral sequence degenerates at E_1.

Formulation: the hypothesis hbetti says that for any two Weil cohomology theories W, W' over k (Definition 0FI2), with coefficients in fields F, F' of characteristic zero, dim_F H^n_W(X) = dim_{F'} H^n_{W'}(X) for every smooth projective X over k and every n. The conclusion is that for every smooth projective X over k, every Hodge-to-de Rham spectral sequence E_1^{p, q} = H^q(X, Ω^p_{X/k}) ⟹ H^{p + q}_{dR}(X/k) of X (a brutal-truncation spectral sequence of Ω^•_{X/k} abutting to H^*_{dR}(X/k), which exists by Tag 0FM7) degenerates at E_1.

The proof: by part 1 (exists_weilCohomologyTheory_hodge) and Proposition 0FWD (Stacks.WeilDeRham.exists_weilCohomologyTheory_deRham), Hodge and de Rham cohomology are Weil cohomology theories with coefficients in k, so hbetti gives dim_k H^n_{Hodge}(X/k) = dim_k H^n_{dR}(X/k); as the Hodge groups are finite dimensional this is E_1-degeneration (degeneratesAt_one_of_finrank_hodgeGradeOf_eq).

theorem degeneratesAt_one_of_finrank_grade_eq [CharZero k]
    (hbetti : ∀ (F F' : Type u) [Field F] [CharZero F] [Field F'] [CharZero F']
      (W : WeilCohomologyTheory k F) (W' : WeilCohomologyTheory k F')
      (X : (SmoothProjectiveScheme k).FullSubcategory) (n : ℤ),
      Module.finrank F (W.grade X n) = Module.finrank F' (W'.grade X n))
    (X : (SmoothProjectiveScheme k).FullSubcategory)
    (S : StupidTruncationSpectralSequence (baseRingedSpace _)
      (deRhamComplexInt (X := X.obj.left.toRingedSpace) (formsAlgebras X.obj.hom)
        (deRhamDifferential (formsAlgebras X.obj.hom))))
    (hS : SpectralSequence.AbutsTo S.spectralSequence
      (deRhamCohomology (X := X.obj.left.toRingedSpace) (formsAlgebras X.obj.hom)
        (deRhamDifferential (formsAlgebras X.obj.hom)))) :
    S.spectralSequence.DegeneratesAt 1

Sources

LeanStacks.WeilDeRham.exists_weilCohomologyTheory_deRham · Stacks.HodgeWeil.exists_weilCohomologyTheory_hodge · Stacks.HodgeWeil.degeneratesAt_one_of_finrank_grade_eq

Section50.23 Gysin maps for closed immersions #

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

Tag 0G83, a remark

Tag 0G83 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.gysinMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinMapCutOut.lean, line 604. The attribute's comment: “the Gysin map γ^p_{f_1, …, f_c}, for the closed subscheme cut out by the equations: no hypothesis beyond the source's own, that the ideal sheaf of i is generated by f_1, …, f_c.”.

Stacks Project, Tag 0G83: the Gysin map. Let π : X ⟶ S be a morphism of schemes, let f₁, …, f_c ∈ Γ(X, 𝒪_X), and let i : Z ⟶ X be the closed subscheme they cut out, that is, let the ideal sheaf of i be generated by f₁, …, f_c. The Gysin map

γ^p_{f₁, …, f_c} : Ω^p_{Z/S} ⟶ ℋ^c_Z(Ω^{p+c}_{X/S})

is the unique morphism whose value on the restriction ω̃|_Z of a local p-form ω̃ on X is c_{f₁, …, f_c}(ω̃|_Z) ∧ d f₁ ∧ ⋯ ∧ d f_c. Both sheaves are read on X through the direct image along i, which is faithful; ℋ^c_Z is the local cohomology sheaf and c_{f₁, …, f_c} the canonical map of [Stacks, Tag 0G7Q].

The content is well-definedness, that is, independence of the chosen lift ω̃: the map gysinFormulaHom kills the kernel of restriction to Z, because a lift is determined up to ∑ f_j ω'_j + ∑ ω''_j ∧ d f_j — that is formKernelGeneratedByEquations_of_isCutOutByEquations, where the hypothesis on Z enters — and both kinds of term go to zero, the first by smulHom_comp_gysinFormulaHom, the second by exactFormWedgeHom_comp_gysinFormulaHom. The map is then the descent of gysinFormulaHom along the epimorphism formRestriction, taken constructively with CategoryTheory.Abelian.epiDesc.

def gysinMap (i : Z ⟶ X) [IsClosedImmersion i] (π : X ⟶ S) {c : ℕ}
    (f : Fin c → Γ(X, ⊤)) (p : ℕ)
    (hcut : Stacks.Gysin.IsCutOutByEquations i f) :
    (Scheme.Modules.pushforward i).obj (relativeDifferentialForms (i ≫ π) (p : ℤ)) ⟶
      pushforwardLocalCohomology f
        (relativeDifferentialForms π ((p : ℤ) + (c : ℤ)))

AlgebraicGeometry.Scheme.Hom.formRestriction_comp_gysinMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinMapCutOut.lean, line 619. The attribute's comment: “the formula γ^p(ω) = c_{f_1, …, f_c}(ω̃|_Z) ∧ d f_1 ∧ ⋯ ∧ d f_c, for the closed subscheme cut out by the equations, with no hypothesis beyond the source's own.”.

Stacks Project, Tag 0G83: the formula for the Gysin map. On the restriction ω̃|_Z of a local p-form ω̃ on X, the Gysin map takes the value c_{f₁, …, f_c}(ω̃|_Z) ∧ d f₁ ∧ ⋯ ∧ d f_c. This is the equation of the source, and it determines gysinMap because restriction to Z is an epimorphism.

theorem formRestriction_comp_gysinMap (i : Z ⟶ X) [IsClosedImmersion i]
    (π : X ⟶ S) {c : ℕ} (f : Fin c → Γ(X, ⊤)) (p : ℕ)
    (hcut : Stacks.Gysin.IsCutOutByEquations i f) :
    formRestriction i π (p : ℤ) ≫ gysinMap i π f p hcut = gysinFormulaHom π f (p : ℤ)

Tag 0G84, an equation

Tag 0G84 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Scheme.Hom.gysinMap, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/WedgeDifferential.lean, line 240 (StacksFrontier): “the displayed map γ^p_{f_1, …, f_c} : Ω^p_{Z/S} ⟶ ℋ^c_Z(Ω^{p+c}_{X/S}) of Remark 0G83, with both sheaves read on X through their direct images, that is as i_Ω^p_{Z/S} ⟶ i_ℋ^c_Z(Ω^{p+c}_{X/S}); both direct images are faithful, and no descent of either sheaf to Z is available, source and target being modules over different rings on Z. No hypothesis beyond the source's own, that the ideal sheaf of i is generated by f_1, …, f_c.”.

Tag 0G85, a lemma

Tag 0G85 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.gysinMapCommutesWithDeRham, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinMapDeRham.lean, line 326.

The Gysin map of [Stacks, Tag 0G83] is compatible with the de Rham differentials on Ω^•_{X/S} and Ω^•_{Z/S}: the square

i_*Ω^p_{Z/S} ⟶ i_*ℋ ᶜ_Z(Ω^{p+c}_{X/S}), i_*Ω^{p+1}_{Z/S} ⟶ i_*ℋ ᶜ_Z(Ω^{p+c+1}_{X/S})

of AlgebraicGeometry.Scheme.Hom.GysinMapCommutesWithDeRham commutes.

public theorem gysinMapCommutesWithDeRham (i : Z ⟶ X) [IsClosedImmersion i] (π : X ⟶ S) {c : ℕ}
    (f : Fin (c + 1) → Γ(X, ⊤)) (p : ℕ) (hcut : Stacks.Gysin.IsCutOutByEquations i f) :
    GysinMapCommutesWithDeRham i π f p hcut

AlgebraicGeometry.Scheme.Hom.gysinMap_comm_deRham, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinMapDeRhamAnyCount.lean, line 330.

Stacks Project, Tag 0G85. The Gysin map γ^p_{f₁, …, f_c} of [Stacks, Tag 0G83] is compatible with the de Rham differentials on Ω^•_{X/S} and Ω^•_{Z/S}, for every number c ≥ 0 of equations: the square

i_*Ω^p_{Z/S} ⟶ i_*ℋ ᶜ_Z(Ω^{p+c}_{X/S}), i_*Ω^{p+1}_{Z/S} ⟶ i_*ℋ ᶜ_Z(Ω^{p+c+1}_{X/S})

commutes, whose horizontal arrows are AlgebraicGeometry.Scheme.Hom.gysinMap in degrees p and p + 1 (read on underlying abelian sheaves, the second followed by the canonical identification of the degrees (p + 1) + c = p + c + 1), whose left vertical arrow is the de Rham differential of Z/S pushed forward along i, and whose right vertical arrow is the action of i_*ℋ ᶜ_Z on the de Rham differential of X/S given by [Stacks, Tag 0G74] part (2).

The square is checked after precomposition with the epimorphism of restriction of forms to Z, where the Gysin map becomes the Gysin formula, and there it is abelianSheaf_map_gysinFormulaHom_comm. The hypotheses are exactly those of gysinMap: i a closed immersion cut out by f : Fin c → Γ(X, ⊤), with c arbitrary — c = 0 included.

theorem gysinMap_comm_deRham (i : Z ⟶ X) [IsClosedImmersion i] (π : X ⟶ S) {c : ℕ}
    (f : Fin c → Γ(X, ⊤)) (p : ℕ) (hcut : Stacks.Gysin.IsCutOutByEquations i f) :
    (abelianSheaf X).map (gysinMap i π f p hcut) ≫
        pushforwardLocalCohomologyAbelianMap (isClosed_equationsClosedSet f) c
          (deRhamDifferentialAbHom π (p + c)) =
      pushforwardDeRhamDifferentialAbHom i π p ≫
        (abelianSheaf X).map (gysinMap i π f (p + 1) hcut ≫
          eqToHom (congrArg
            (fun k : ℤ => pushforwardLocalCohomology f (relativeDifferentialForms π k))
            (gysinAnyTargetDegree_eq c p)))

Declarations registered for the tag:

Stacks.Perfect.AbelianCechCokernelPassage.map_cokernelLastDifToSupport_abelian_square, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Perfect/SupportClosedSubset/AbelianCechCokernelPassage.lean, line 852 (StacksFrontier): “STEP (ii) ONLY. This is the square between the Cech cokernel and i_*H^c_T, carrying nothing beyond quasi-coherence of F and G and the two closed-set conditions. Steps (i) and (iii) are proved elsewhere in this development, and the tag itself is now proved and registered unsuffixed on AlgebraicGeometry.Scheme.Hom.gysinMapCommutesWithDeRham of StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinMapDeRham.lean. The identity this suffix used to name as outstanding, forgetIsoApp of AbelianSupportedEndoModelBridge.cokernelLastDifToPushforwardAbelianNatural_of_forgetIsoApp, is discharged by Stacks.Perfect.SupportedEndoForgetDegreewise.forgetIsoApp.”.

Tag 0G86, a lemma

Tag 0G86 in the Stacks Project.

Stacks.Gysin.existsUnique_gysinHom_of_conormalRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinConormalRankAny.lean, line 387.

Stacks Project, Tag 0G86: the canonical Gysin map of a closed immersion. Let π : X ⟶ S be a morphism of schemes and i : Z ⟶ X a closed immersion of finite presentation whose conormal sheaf is locally free of rank c. Then there is one map

γ^p : i_*Ω^p_{Z/S} ⟶ i_*ℋ^c_Z(Ω^{p+c}_{X/S})

which, over every open contained in an open on which c functions generate the ideal of Z, is the Gysin map γ^p_{f₁, …, f_c} of [Stacks, Tag 0G83] of those functions, and it is the only map with that property.

The rank is an arbitrary natural number. [Stacks, Tag 0G8A] says c ≥ 0 explicitly, so c = 0 is part of the statement and not a degenerate exclusion; it is the case in which Z is a clopen piece of X, by Stacks.Gysin.isClopen_range_base_of_conormalRank_zero, and in which a chart carries the empty family of equations. The hypotheses are exactly the tag's: no bound on c, and in particular neither c ≠ 0 nor a rank of the form d + 1.

The proof splits on c and nothing else does:

for c = d + 1, Stacks.Gysin.existsUnique_gysinHom_of_conormalRank_succ, the chart route through Stacks.Gysin.GysinChartData — the charts then cover X, because away from the closed subscheme the equations may be taken to generate the unit ideal;

for c = 0, existsUnique_gysinHom_of_conormalRank_zero, where the charts cover only the image and the gluing is run on the family augmented by its complement.

The charts are all the equation charts of Stacks.Gysin.EquationChart, which is what makes the conclusion quantify over every local family of c equations cutting out Z and not only over a chosen covering family.

theorem existsUnique_gysinHom_of_conormalRank (i : Z ⟶ X) [IsClosedImmersion i]
    [LocallyOfFinitePresentation i] (π : X ⟶ S) {c : ℕ} (p : ℕ) (hE : ConormalRank i c) :
    ∃! φ : pushforwardRelativeForms i π (p : ℤ) ⟶ gysinTarget i π c p,
      ∀ (a : EquationChart i c) (V : X.Opens) (hV : V ≤ a.ambient)
        (x : Γ(pushforwardRelativeForms i π (p : ℤ), V)),
        φ.app V x =
          chartLoc i π p a.ambient a.equations
            (isCutOutByEquationsOn_of_isGeneratedByOn i a.gen a.vanish)
            (equationsClosedSet_restrictEquations i a.ambient
              (isCutOutByEquationsOn_of_isGeneratedByOn i a.gen a.vanish)) V hV x

Tag 0G87, a lemma

Tag 0G87 in the Stacks Project.

Stacks.Gysin.gysinHom_comm_deRham_of_conormalRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinDeRhamConormalRank.lean, line 289.

Stacks Project, Tag 0G87: the Gysin map is compatible with the de Rham differentials.

Let π : X ⟶ S be a morphism of schemes and i : Z ⟶ X a closed immersion of finite presentation whose conormal sheaf is locally free of rank c — the hypotheses of [Stacks, Tag 0G86], and nothing more. Let γ and γ' be the Gysin maps of [Stacks, Tag 0G86] in the degrees p and p + 1, each characterised as that tag characterises it: over every open contained in an equation chart it is the Gysin map γ^p_{f₁, …, f_c} of [Stacks, Tag 0G83] of that chart's equations. Then the square

ℋ ᶜ_Z(d_{X/S}) ∘ γ^p = γ^{p+1} ∘ d_{Z/S}

commutes, on the sections over every open of X. The left vertical arrow is the relative de Rham differential of Z/S (Stacks.Gysin.pushforwardDeRham), the right one the action of i_*ℋ ᶜ_Z on the relative de Rham differential of X/S given by [Stacks, Tag 0G74] part (2) (Stacks.Gysin.gysinTargetDeRhamHom).

The rank is an arbitrary natural number, as [Stacks, Tag 0G86] states it and as [Stacks, Tag 0G8A] says explicitly (c ≥ 0). In particular c = 0 — the case in which Z is a clopen piece of X, by Stacks.Gysin.isClopen_range_base_of_conormalRank_zero, and in which an equation chart carries the empty family — is part of the statement and not a degenerate exclusion; neither c ≠ 0 nor a rank of the form d + 1 is assumed.

Both maps γ, γ' with these properties exist and are unique at every rank, by Stacks.Gysin.existsUnique_gysinHom_of_conormalRank, the registration of [Stacks, Tag 0G86]; the characterisations are stated here verbatim as they are there.

The proof splits on c and nothing else does:

for c = d + 1, gysinHom_comm_deRham_of_conormalRank_succ, the chart route — the charts then cover X, and the square at one chart family is gysinHom_comm_deRham_charts;

for c = 0, Stacks.Gysin.gysinHom_comm_deRham_of_conormalRank_zero, where the charts cover only the image of i and the square is glued on the family augmented by its complement.

theorem gysinHom_comm_deRham_of_conormalRank (i : Z ⟶ X) [IsClosedImmersion i]
    [LocallyOfFinitePresentation i] (π : X ⟶ S) {c : ℕ} (p : ℕ)
    (hE : ConormalRank i c)
    (γ : pushforwardRelativeForms i π (p : ℤ) ⟶ gysinTarget i π c p)
    (γ' : pushforwardRelativeForms i π ((p + 1 : ℕ) : ℤ) ⟶ gysinTarget i π c (p + 1))
    (hγ : ∀ (a : EquationChart i c) (V : X.Opens) (hV : V ≤ a.ambient)
      (x : Γ(pushforwardRelativeForms i π (p : ℤ), V)),
      γ.app V x =
        chartLoc i π p a.ambient a.equations
          (isCutOutByEquationsOn_of_isGeneratedByOn i a.gen a.vanish)
          (equationsClosedSet_restrictEquations i a.ambient
            (isCutOutByEquationsOn_of_isGeneratedByOn i a.gen a.vanish)) V hV x)
    (hγ' : ∀ (a : EquationChart i c) (V : X.Opens) (hV : V ≤ a.ambient)
      (x : Γ(pushforwardRelativeForms i π ((p + 1 : ℕ) : ℤ), V)),
      γ'.app V x =
        chartLoc i π (p + 1) a.ambient a.equations
          (isCutOutByEquationsOn_of_isGeneratedByOn i a.gen a.vanish)
          (equationsClosedSet_restrictEquations i a.ambient
            (isCutOutByEquationsOn_of_isGeneratedByOn i a.gen a.vanish)) V hV x)
    (V : X.Opens) (x : Γ(pushforwardRelativeForms i π (p : ℤ), V)) :
    abSectionsHom (gysinTargetDeRhamHom i π c p) V (γ.app V x) =
      γ'.app V (pushforwardDeRham i π p V x)

Tag 0G88, a lemma

Tag 0G88 in the Stacks Project.

Stacks.Gysin.conormalGysin_formRestriction_cupDegreeZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/ConormalWedgeProjectionRank.lean, line 449.

Stacks Project, Tag 0G88 at the canonical Gysin maps of [Stacks, Tag 0G86], with nothing assumed. The only hypotheses are the tag's own: i a closed immersion of finite presentation whose conormal sheaf is locally free of rank c.

c is an arbitrary natural number, as [Stacks, Tag 0G86] states it and as [Stacks, Tag 0G8A] says explicitly (c ≥ 0): the case c = 0, in which Z is a clopen piece of X by Stacks.Gysin.isClopen_range_base_of_conormalRank_zero and in which a chart carries the empty family of equations, is part of the statement and not a degenerate exclusion.

The maps are Stacks.DeRham.CohomologicalGysin.conormalGysinHom, the γ^p of [Stacks, Tag 0G86] itself, whose characterisation is Stacks.DeRham.CohomologicalGysin.conormalGysinHom_app; the degree comparison is the canonical transport, whose one equation is Stacks.Gysin.eqToHom_app_gysinWedgeOn_one.

theorem conormalGysin_formRestriction_cupDegreeZero [LocallyOfFinitePresentation i]
    (hE : ConormalRank i c) (q : ℕ) :
    (_root_.Hfunctor X.ringCatSheaf ⊤ q).map (formRestriction i π (p : ℤ)) ≫
        (_root_.Hfunctor X.ringCatSheaf ⊤ q).map
          (Stacks.DeRham.CohomologicalGysin.conormalGysinHom i π p hE) =
      Stacks.Cohomology.cupDegreeZero X.ringCatSheaf (conormalWedgePair i π c p)
        (conormalUnitClass i π
          (eqToHom (congrArg (relativeDifferentialForms π) (natCast_zero_add c)))
          (Stacks.DeRham.CohomologicalGysin.conormalGysinHom i π 0 hE)) q

Tag 0G89, a lemma

Tag 0G89 in the Stacks Project.

Stacks.Gysin.GysinBaseChange.gysinHom_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/Transverse.lean, line 503. The attribute's comment: “the Gysin square of a transverse cartesian square commutes, for the Gysin maps GysinChartData.gysinHom of Stacks 0G86; granted the right vertical arrow of Stacks 0G78 descended to degree c by the vanishing of Stacks 0G7N as the hypothesis B.tgt with B.tgt_res, the class-map base-change square of Stacks 0G7U as the hypothesis B.tgt_cls, hypotheses (2) and (3) of the statement -- the left square cartesian and the conormal comparison of Stacks 01R4 an isomorphism -- as the chart correspondence B.chart with B.chart_ambient and B.chart_equations, and the local liftability of relative forms coming from the conormal sequence of Stacks 01UZ as the hypothesis B.lift; none of these four is proved in this library”.

Stacks Project, Tag 0G89. For a transverse cartesian square the Gysin maps of [Stacks, Tag 0G86] on the two closed immersions fit into a commutative square: the base-change map on the targets applied to γ^p agrees with γ^p applied to the pullback of relative differential forms.

The commutativity is checked locally, which is what the source does: on a covering of the open by opens inside an equation chart over which the form lifts to the ambient scheme, it is gysinHom_baseChange_subschemeFormPullback; the target is a sheaf, so it holds over the open itself.

theorem gysinHom_baseChange (V : X.Opens) (x : Γ(pushforwardRelativeForms i π (p : ℤ), V)) :
    B.tgt V (D.gysinHom.app V x)
      = D'.gysinHom.app (g ⁻¹ᵁ V) (subschemeFormBaseChange i i' h g π π' t left_comm right_comm
          (p : ℤ) V x)

Stacks.Gysin.conormalGysinHom_comp_gysinBaseChangeTargetHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/TransverseGysinSquare.lean, line 208.

Stacks Project, Tag 0G89. Let c ≥ 0 and let
Z' ⟶ X' ⟶ S'
↓h    ↓g    ↓t
Z  ⟶ X  ⟶ S
be a commutative diagram of schemes such that

i : Z ⟶ X and i' : Z' ⟶ X' satisfy the assumptions of [Stacks, Tag 0G86]: closed immersions of finite presentation whose conormal sheaves are locally free of rank c (hE, hE');

the left square is cartesian (hcart);

the map h^*𝒞_{Z/X} ⟶ 𝒞_{Z'/X'} of [Stacks, Tag 01R4] is an isomorphism (_hconormal).

Then the Gysin maps γ^p of [Stacks, Tag 0G86] commute with the pullback of differential forms on the left and the base change arrow of [Stacks, Cohomology, Remark 0G78] on the right, descended to degree c by the vanishing of [Stacks, Tag 0G7N]. The square is stated on X: the left vertical arrow gysinBaseChangeSourceHom is the transpose of h^*Ω^p_{Z/S} ⟶ Ω^p_{Z'/S'} pushed forward, and the right vertical arrow gysinBaseChangeTargetHom is the transpose along g^* ⊣ g_* of the source's right vertical arrow, whose source is g^* of i_*ℋ^c_Z(Ω^{p+c}).

On hypothesis (3). It is the source's hypothesis and is kept as the binder _hconormal, but the proof does not consume it: given (2), the map of (3) is surjective (the ideal of Z' is generated by the pullback of the ideal of Z), and given (1) both sides are locally free of the same finite rank c, so a surjection between them is an isomorphism; in other words (3) is implied by (1) and (2). What the proof uses of the transversality is that the pulled-back equations g^♯f₁, …, g^♯f_c of an equation chart of Z cut out Z' over the preimage chart, Stacks.Gysin.EquationChart.ofIsPullback, which needs only (2).

theorem conormalGysinHom_comp_gysinBaseChangeTargetHom (hcart : IsPullback h i' i g)
    (right_comm : g ≫ π = π' ≫ t) {c : ℕ} (p : ℕ) (hE : ConormalRank i c)
    (hE' : ConormalRank i' c)
    (_hconormal : IsIso (Stacks.Immersion.immersionConormalSheafMap i' i h g
      (congrArg (fun k => k.toLRSHom.toShHom) hcart.w.symm))) :
    (conormalGysinHom i π p hE ≫ (conormalGysinTargetIso i π c p).hom) ≫
        gysinBaseChangeTargetHom i i' h g π π' t hcart right_comm p hE =
      gysinBaseChangeSourceHom i i' h g π π' t hcart.w right_comm (p : ℤ) ≫
        (modulePushforward g.toLRSHom.toShHom).map
          (conormalGysinHom i' π' p hE' ≫
            (conormalGysinTargetIso i' π' c p).hom)

Tag 0G8A, a remark

Tag 0G8A in the Stacks Project.

Stacks.DeRham.CohomologicalGysin.gysinHodgeFormsMapOfConormalRank, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/CohomologicalGysinHodgeConormal.lean, line 241.

Stacks Project, Tag 0G8A. Let π : X ⟶ S be a morphism of schemes and i : Z ⟶ X a closed immersion of finite presentation whose conormal sheaf is locally free of rank c — the hypotheses of [Stacks, Tag 0G86]. Let p ≥ 0 and assume

ℋ^j_Z(Ω^{p+c}_{X/S}) = 0 for j = 0, …, c - 1.

Then there is a map

γ^{p, q} : H^q(Z, Ω^p_{Z/S}) ⟶ H^{q + c}(X, Ω^{p + c}_{X/S})

for every q, obtained exactly as the source obtains it: the γ^p of [Stacks, Tag 0G86] followed by the passage ℋ^c_Z(ℱ) = R𝓗_Z(ℱ)[c], the identification H^q(Z, -) = H^q(X, i_*-) and the adjunction map i_*R𝓗_Z(ℱ) ⟶ ℱ.

The sheaf-level map is conormalGysinHom, the γ^p of [Stacks, Tag 0G86] itself — glued from the Gysin maps of [Stacks, Tag 0G83] of the local families of equations, not built from one global family — and the three remaining steps are gysinHodgeFormsMap, which performs them for an arbitrary sheaf-level Gysin map. The one identification in between is conormalGysinTargetIso, between two spellings of i_*ℋ^c_Z(Ω^{p+c}_{X/S}) that agree because the direct image along the inclusion of a closed subset is exact.

Nothing is assumed: both hypotheses of [Stacks, Tag 0G86] are consumed where the source consumes them, by Stacks.Gysin.existsUnique_gysinHom_of_conormalRank, the quasi-coherence of Ω^p_{Z/S} needed by [Stacks, Tag 089W] is proved inside gysinHodgeFormsMap, and hvan is the source's own vanishing hypothesis. The sufficient condition of [Stacks, Tag 0G7P] is not available here and is not used.

The rank is an arbitrary natural number, as the tag states it: [Stacks, Tag 0G8A] says c ≥ 0 explicitly. Nothing here needs c ≠ 0, because Stacks.Gysin.existsUnique_gysinHom_of_conormalRank supplies γ^p at every rank — it splits on c, the chart route of Stacks.Gysin.exists_gysinCharts handling c = d + 1 and Stacks.Gysin.existsUnique_gysinHom_of_conormalRank_zero handling c = 0, where the local families of equations are empty and the charts cover the image rather than X.

hvan is retained because it is the source's own hypothesis, not an artefact of the rank: at c = 0 it is vacuous in content — the degrees j < 0 carry none, by Stacks.DeRham.CohomologicalGysin.isZero_localCohomologySheafOfComplex_of_neg — and the construction consumes it uniformly.

What rank 0 forces, and what it does not. ConormalRank i 0 says exactly that the conormal sheaf of i vanishes, so the ideal sheaf vanishes on an affine neighbourhood of every point of Set.range i.base — Stacks.AlgebraicGeometry.ConormalEquations.exists_affineOpen_equations_of_conormalRank, read at c = 0, returns such a neighbourhood and it carries no hypothesis on c. Hence i is an isomorphism onto an open subscheme, which being also closed has clopen range. It does not force that range to be the whole of X: the identity satisfies ConormalRank i 0, and so does the inclusion of a proper clopen piece. The equations of the chapter cannot see the latter, by Stacks.Gysin.equationsClosedSet_eq_range: an empty family cutting out i in the sense of Stacks.Gysin.IsCutOutByEquations makes Set.range i.base the whole of X. That is why the c = 0 branch of [Stacks, Tag 0G86] is glued on the charts together with the complement of the image instead of on a Stacks.Gysin.GysinChartData.

def gysinHodgeFormsMapOfConormalRank (i : Z ⟶ X) [IsClosedImmersion i]
    [LocallyOfFinitePresentation i] (π : X ⟶ S) {c : ℕ} (p : ℕ)
    (hE : ConormalRank i c)
    (hvan : ∀ j : ℤ, j < (c : ℤ) →
      IsZero (localCohomologySheafOfComplex X.toRingedSpace (Set.range i.base)
        i.isClosedEmbedding.isClosed_range j ((singleFunctor _ (0 : ℤ)).obj
          (relativeDifferentialForms π ((p : ℤ) + (c : ℤ))))))
    (q : ℕ) :
    Hgroup Z.ringCatSheaf ⊤ q (relativeDifferentialForms (i ≫ π) (p : ℤ)) ⟶
      Hgroup X.ringCatSheaf ⊤ (q + c)
        (relativeDifferentialForms π ((p : ℤ) + (c : ℤ)))

Tag 0G8B, a lemma

Tag 0G8B in the Stacks Project.

Stacks.DeRham.GysinCohomologyDeRhamKoszul.koszulGysinCohomologyMap_comm_deRham, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinCohomologyDeRhamKoszul.lean, line 247.

Stacks Project, Tag 0G8B. Let π : X ⟶ S be a smooth morphism of schemes and let i : Z ⟶ X be as in [Stacks, Tag 0G86] — a closed immersion of finite presentation whose conormal sheaf is finite locally free of rank c — and Koszul-regular. The cohomological Gysin maps γ^{p, q} : H^q(X, i_*Ω^p_{Z/S}) ⟶ H^{q + c}(X, Ω^{p + c}_{X/S}) of [Stacks, Tag 0G8A] attached to the glued γ^p of [Stacks, Tag 0G86] are compatible with the de Rham differentials on Ω^•_{X/S} and Ω^•_{Z/S}: the square
H^q(X, i_*Ω^p_{Z/S}) ----γ^{p, q}----→ H^{q+c}(X, Ω^{p+c}_{X/S})
        ↓ d                                     ↓ d
H^q(X, i_*Ω^{p+1}_{Z/S}) --γ^{p+1, q}→ H^{q+c}(X, Ω^{p+c+1}_{X/S})
commutes, the verticals being the arrows the de Rham differentials induce on cohomology through Stacks.DeRham.GysinCohomologyDeRham.abelianHgroupMap.

The square itself is Stacks.DeRham.GysinCohomologyDeRhamConormal.conormalGysinCohomologyMap_comm_deRham, which assumes the vanishing of [Stacks, Tag 0G8A]; here that vanishing is supportVanishing_relativeDifferentialForms, derived from the hypotheses of this tag through [Stacks, Tag 0G7P], so that nothing beyond them is assumed. That the map the square is about is the tagged γ^{p, q} of [Stacks, Tag 0G8A] and not a second construction is Stacks.DeRham.GysinCohomologyDeRhamConormal.gysinHodgeFormsMapOfConormalRank_eq.

The rank is an arbitrary natural number, as [Stacks, Tag 0G86] states it and [Stacks, Tag 0G8A] says explicitly (c ≥ 0); neither c ≠ 0 nor a rank of the form d + 1 is assumed. Both inputs are already general: the vanishing supportVanishing_relativeDifferentialForms handles c = 0 separately — in degrees j < 0 there is nothing to vanish — and the square Stacks.DeRham.GysinCohomologyDeRhamConormal.conormalGysinCohomologyMap_comm_deRham rests on [Stacks, Tag 0G87] at an arbitrary rank, Stacks.Gysin.gysinHom_comm_deRham_of_conormalRank.

theorem koszulGysinCohomologyMap_comm_deRham (i : Z ⟶ X) [IsClosedImmersion i]
    [LocallyOfFinitePresentation i] (π : X ⟶ S) [Smooth π]
    (hkos : IsKoszulRegularImmersion i) {c : ℕ} (p q : ℕ)
    (hE : ConormalRank i c) :
    gysinCohomologyMap (Set.range i.base) (isClosed_range_base i) c
          (pushforwardRelativeForms i π (p : ℤ))
          (relativeDifferentialForms π ((p : ℤ) + (c : ℤ)))
          (supportVanishing_relativeDifferentialForms i π hkos c hE p)
          (conormalGysinHom i π p hE ≫ (conormalGysinTargetIso i π c p).hom) q ≫
        abelianHgroupMap X.toRingedSpace (0 : ℤ) ((q : ℤ) + (c : ℤ)) (q + c)
          (by omega) (ambientDeRhamShiftAbHom π c p) =
      abelianHgroupMap X.toRingedSpace (c : ℤ) ((q : ℤ) + (c : ℤ)) q
          (by omega) (pushforwardDeRhamDifferentialAbHom i π p) ≫
        gysinCohomologyMap (Set.range i.base) (isClosed_range_base i) c
          (pushforwardRelativeForms i π ((p + 1 : ℕ) : ℤ))
          (relativeDifferentialForms π (((p + 1 : ℕ) : ℤ) + (c : ℤ)))
          (supportVanishing_relativeDifferentialForms i π hkos c hE
            (p + 1))
          (conormalGysinHom i π (p + 1) hE ≫
            (conormalGysinTargetIso i π c (p + 1)).hom) q

Tag 0G8C, a lemma

Tag 0G8C in the Stacks Project.

Stacks.DeRham.GysinProjection.equationGysinCohomologyMap_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinCupProduct.lean, line 266. The attribute's comment: “the cohomological content of the proof, items (1), (2) and (4) of the source's list, for the Gysin map of a family of equations: gamma^{p,q} of the restriction of alpha to Z is the class with support of alpha wedge df_1 wedge ... wedge df_c over f_1 ... f_c with its support forgotten, proved with no hypothesis beyond the hker and hvan that Tag 0G8A already carries; the remaining identification of that class with alpha cup gamma^{0,0}(1) is Cohomology Tags 0G77 and 0G76 in the Hgroup presentation of the groups, which is absent here”.

The cohomological projection formula for the Gysin map of a family of equations. Let π : X ⟶ S, let f₁, …, f_c ∈ Γ(X, 𝒪_X) with c = n + 1 and let i : Z ⟶ X be the closed subscheme they cut out. Then the composite

H^q(X, Ω^p_{X/S}) --(restriction to Z)--> H^q(X, i_*Ω^p_{Z/S}) --γ^{p,q}--> H^{q+c}(X, Ω^{p+c})

is the composite

H^q(X, Ω^p_{X/S}) --(Gysin formula)--> H^{q+c}_Z(X, Ω^{p+c}) --(forget support)--> H^{q+c}(X, …),

the first arrow of the second composite being induced by the morphism of sheaves carrying a local p-form ω̃ to the class of ω̃ ∧ d f₁ ∧ ⋯ ∧ d f_c divided by f₁ ⋯ f_c.

This is the cohomological content of [Stacks, Tag 0G88] for the Gysin map of a family of equations, which is items (1), (2) and (4) of the source's proof of [Stacks, Tag 0G8C]: the sheaf-level projection formula is the formula clause of [Stacks, Tag 0G83], formRestriction_comp_gysinMapOfFormKernel, and the two factorisations are cohomologyMapOfModuleHom_comp and gysinCohomologyMap_eq. Nothing is assumed beyond the hypotheses hker and hvan that [Stacks, Tag 0G8A] already carries.

theorem equationGysinCohomologyMap_comp_eq (i : Z ⟶ X) [IsClosedImmersion i] (π : X ⟶ S) {n : ℕ}
    (f : Fin (n + 1) → Γ(X, ⊤)) (p : ℕ)
    [(relativeDifferentialForms π ((p : ℤ) + ((n + 1 : ℕ) : ℤ))).IsQuasicoherent]
    (hker : FormKernelGeneratedByEquations i π f (p : ℤ))
    (hvan : EquationSupportVanishes π f p) (q : ℕ) :
    cohomologyMapOfModuleHom X.toRingedSpace _ _ (n + 1) q (formRestriction i π (p : ℤ)) ≫
        equationGysinCohomologyMap i π f p hker hvan q =
      cohomologyMapOfModuleHom X.toRingedSpace _ _ (n + 1) q (gysinFormulaHom π f (p : ℤ)) ≫
        forgetSupportCohomology (equationsClosedSet f) (isClosed_equationsClosedSet f) (n + 1)
          (relativeDifferentialForms π ((p : ℤ) + ((n + 1 : ℕ) : ℤ))) hvan q

Stacks.DeRham.GysinCupHodge.gysinHodgeFormsMapOfConormalRank_hodgeRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinProjectionFormula.lean, line 386. The attribute's comment: “the full statement, at the source's hypotheses (pi smooth, i a Koszul regular closed immersion of finite presentation with conormal sheaf locally free of rank c), with the cup product of Cohomology Section 0FKU constructed and nothing assumed; stated with the sign: gamma^{p,q}(alpha|_Z) = (-1)^{qc} alpha cup gamma^{0,0}(1). The sign comes from this library's sign-free identification H^q(X, A) = H^{q+c}(R Gamma(X, A[-c])) of the bridge hgroupModuleShiftIso, where the source uses the Koszul-signed identification; it appears at totalCupPairing_shift₂. Under the Koszul-signed identification the formula is the source's gamma^{p,q}(alpha|_Z) = alpha cup gamma^{0,0}(1)”.

The Gysin map and the cup product [Stacks, Tag 0G8C]. Let π : X ⟶ S be smooth and i : Z ⟶ X a Koszul regular closed immersion of finite presentation whose conormal sheaf is locally free of rank c (hE). For α ∈ H^q(X, Ω^p_{X/S}), γ^{p,q}(α|_Z) = (-1)^{qc} α ∪ γ^{0,0}(1) in H^{q+c}(X, Ω^{p+c}_{X/S}).

Here α|_Z is hodgeRestriction i π p q α, γ^{a,b} is the Gysin map gysinHodgeFormsMapOfConormalRank of Tag 0G8A, whose vanishing hypothesis is proved from the smoothness of π and the Koszul regularity of i (supportVanishing_relativeDifferentialForms, Tag 0G7P), 1 ∈ H^0(Z, Ω^0_{Z/S}) is oneFormCohomologyClass, and ∪ is the cup product hodgeCupStructureSheaf of Cohomology, Section 0FKU. The cup product is stated on the modules H^m(RΓ(X, -)), so both sides are read through the bridge hgroupModuleShiftIso, an isomorphism.

The sign (-1)^{qc} comes from the identification H^q(X, A) ≅ H^{q+c}(RΓ(X, A[-c])) of the bridge, which is sign-free, where the source uses the Koszul-signed identification; it appears at Stacks.Cohomology.DerivedGlobalCupProduct.totalCupPairing_shift₂. Under the Koszul-signed identification this is the source's formula γ^{p,q}(α|_Z) = α ∪ γ^{0,0}(1).

theorem gysinHodgeFormsMapOfConormalRank_hodgeRestriction (i : Z ⟶ X) [IsClosedImmersion i]
    [LocallyOfFinitePresentation i] (π : X ⟶ S) [Smooth π] {c : ℕ} (hE : ConormalRank i c)
    (hK : IsKoszulRegularImmersion i) (p q : ℕ)
    (α : Hgroup X.ringCatSheaf ⊤ q (relativeDifferentialForms π (p : ℤ))) :
    (hgroupModuleShiftIso (X := X.toRingedSpace) (relativeDifferentialForms π ((p : ℤ) + (c : ℤ)))
        0 (q + c) ((q : ℤ) + (c : ℤ)) (by push_cast; ring)).hom
      ((Stacks.DeRham.CohomologicalGysin.gysinHodgeFormsMapOfConormalRank i π p hE
        (Stacks.DeRham.GysinCohomologyDeRhamKoszul.supportVanishing_relativeDifferentialForms
          i π hK c hE p) q).hom
        ((hodgeRestriction i π p q).hom α)) =
    ((q : ℤ) * (c : ℤ)).negOnePow •
      (hodgeCupStructureSheaf π p c q c).hom
        ((hgroupModuleShiftIso (X := X.toRingedSpace) (relativeDifferentialForms π (p : ℤ)) 0 q q
          (by simp)).hom α ⊗ₜ
        (hgroupModuleShiftIso (X := X.toRingedSpace) (relativeDifferentialForms π (c : ℤ)) 0 (0 + c)
          c (by push_cast; ring)).hom
          ((Hfunctor X.ringCatSheaf ⊤ (0 + c)).map
            (eqToHom (congrArg (relativeDifferentialForms π) (by push_cast; ring)))
            ((Stacks.DeRham.CohomologicalGysin.gysinHodgeFormsMapOfConormalRank i π 0 hE
              (Stacks.DeRham.GysinCohomologyDeRhamKoszul.supportVanishing_relativeDifferentialForms
                i π hK c hE 0) 0).hom
              (Stacks.DeRham.GysinProjection.oneFormCohomologyClass (i ≫ π)))))

Tag 0G8D, a lemma

Tag 0G8D in the Stacks Project.

Stacks.DeRham.GysinCohomologyBaseChange.conormalGysinCohomologyMap_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/CohomologicalBaseChangeTransverse.lean, line 289.

Stacks Project, Tag 0G8D. Let c ≥ 0 and let
Z' → X' → S'
↓h   ↓g    ↓t
Z  → X  → S
satisfy the assumptions of [Stacks, Tag 0G89]: Z → X and Z' → X' are closed immersions of finite presentation whose conormal sheaves are locally free of rank c, the left square is cartesian and h^*𝒞_{Z/X} → 𝒞_{Z'/X'} is an isomorphism. Assume in addition that X → S, X' → S' are smooth and Z → X, Z' → X' are Koszul regular immersions. Then
H^q(Z, Ω^p_{Z/S})  ----γ^{p,q}---→ H^{q+c}(X, Ω^{p+c}_{X/S})
       ↓                                    ↓
H^q(Z', Ω^p_{Z'/S'}) --γ^{p,q}---→ H^{q+c}(X', Ω^{p+c}_{X'/S'})
commutes, γ^{p,q} being the Gysin map of [Stacks, Tag 0G8A] at the γ^p of [Stacks, Tag 0G86].

The cohomology of the closed subschemes is read on the ambient schemes, H^q(X, i_*Ω^p_{Z/S}), which is how [Stacks, Tag 0G8A] constructs γ^{p,q} (and how the registered [Stacks, Tag 0G8B] reads it); the vertical maps are the pullback maps on cohomology of [Stacks, Tag 01F9] built from the canonical comparisons CohomologyPullbackComparison.canonical of [Stacks, Tag 01F8] and [Stacks, Tag 01EZ], at the g-maps of relative differential forms — on the left the pullback of forms along h, read on X (Stacks.Gysin.gysinBaseChangeSourceHom), on the right functoriality of Ω^{p+c} (Stacks.Gysin.formsBaseChangeHom). Both are the standard pullback maps, with the module placed in degree 0; that the placement degree does not matter is pullbackHgroup_canonical_eq.

Nothing is assumed beyond the source: the vanishing that [Stacks, Tag 0G8A] needs is derived from smoothness and Koszul regularity by [Stacks, Tag 0G7P]; the sheaf square is [Stacks, Tag 0G89] (Stacks.Gysin.conormalGysinHom_comp_gysinBaseChangeTargetHom, whose binder _hconormal is hypothesis (3) as the source states it); and the compatibility of the Gysin edge morphisms with pullback, [Stacks, Tag 0G78] and [Stacks, Tag 0G79], is gysinEdge_baseChange.

theorem conormalGysinCohomologyMap_pullback (i : Z ⟶ X) (i' : Z' ⟶ X') (h : Z' ⟶ Z)
    (g : X' ⟶ X) (π : X ⟶ S) (π' : X' ⟶ S') (t : S' ⟶ S)
    [IsClosedImmersion i] [LocallyOfFinitePresentation i]
    [IsClosedImmersion i'] [LocallyOfFinitePresentation i']
    {c : ℕ} (hE : ConormalRank i c) (hE' : ConormalRank i' c)
    (hcart : IsPullback h i' i g) (right_comm : g ≫ π = π' ≫ t)
    (hconormal : IsIso (Stacks.Immersion.immersionConormalSheafMap i' i h g
      (congrArg (fun k => k.toLRSHom.toShHom) hcart.w.symm)))
    [Smooth π] [Smooth π'] (hkos : IsKoszulRegularImmersion i)
    (hkos' : IsKoszulRegularImmersion i') (p q : ℕ) :
    gysinCohomologyMap (Set.range i.base) (isClosed_range_base i) c
          (pushforwardRelativeForms i π (p : ℤ))
          (relativeDifferentialForms π ((p : ℤ) + (c : ℤ)))
          (Stacks.DeRham.GysinCohomologyDeRhamKoszul.supportVanishing_relativeDifferentialForms
            i π hkos c hE p)
          (conormalGysinHom i π p hE ≫ (conormalGysinTargetIso i π c p).hom) q ≫
        pullbackHgroup (CohomologyPullbackComparison.canonical g.toLRSHom.toShHom) (0 : ℤ)
          ((q : ℤ) + (c : ℤ)) (q + c) (by omega)
          (formsBaseChangeHom g π π' t right_comm ((p : ℤ) + (c : ℤ)))
      = pullbackHgroup (CohomologyPullbackComparison.canonical g.toLRSHom.toShHom) (0 : ℤ)
          (q : ℤ) q (by omega)
          (gysinBaseChangeSourceHom i i' h g π π' t hcart.w right_comm (p : ℤ)) ≫
        gysinCohomologyMap (Set.range i'.base) (isClosed_range_base i') c
          (pushforwardRelativeForms i' π' (p : ℤ))
          (relativeDifferentialForms π' ((p : ℤ) + (c : ℤ)))
          (Stacks.DeRham.GysinCohomologyDeRhamKoszul.supportVanishing_relativeDifferentialForms
            i' π' hkos' c hE' p)
          (conormalGysinHom i' π' p hE' ≫ (conormalGysinTargetIso i' π' c p).hom) q

Tag 0G8E, a lemma

Tag 0G8E in the Stacks Project.

Stacks.DeRham.CohomologicalGysin.gysinHodgeFormsMapOfConormalRank_oneClass_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinPointClass.lean, line 219. The attribute's comment: “for X irreducible smooth proper over a field k of dimension d and Z the reduced closed subscheme of a k-rational point, the Gysin map H^0(Z, Omega^0_{Z/k}) -> H^d(X, Omega^d_{X/k}) of 0G8A sends 1 to a nonzero class”.

[Stacks, Tag 0G8E]. Let k be a field and X an irreducible smooth proper scheme over k of dimension d. Let i : Z ⟶ X be the reduced closed subscheme consisting of a single k-rational point, i.e. a closed immersion with Z ≅ Spec k over k. Then the image of 1 ∈ k = H^0(Z, 𝒪_Z) = H^0(Z, Ω^0_{Z/k}) under the Gysin map H^0(Z, Ω^0_{Z/k}) ⟶ H^d(X, Ω^d_{X/k}) of [Stacks, Tag 0G8A] is nonzero. The identification ω_X^• ≅ Ω^d_{X/k}[d] the argument uses is [Stacks, Tag 0FVV], part (7).

theorem gysinHodgeFormsMapOfConormalRank_oneClass_ne_zero (d : ℕ) [IsProper π] [Smooth π]
    [IrreducibleSpace X] (hd : topologicalKrullDim X = d) [IsIso (i ≫ π)] :
    haveI : SmoothOfRelativeDimension d π := smoothOfRelativeDimension_of_equidimensional k π
      (TopologicalSpace.Equidimensional.of_preirreducibleSpace X) d hd
    haveI : LocallyOfFinitePresentation i := locallyOfFinitePresentation_of_comp i π
    gysinHodgeFormsMapOfConormalRank i π (c := d) 0 (conormalRank_of_formallyUnramified i π d)
      (supportVanishing_of_formallyUnramified i π d 0) 0 (oneClass π i) ≠ 0

Sources

LeanAlgebraicGeometry.Scheme.Hom.gysinMap · AlgebraicGeometry.Scheme.Hom.formRestriction_comp_gysinMap · AlgebraicGeometry.Scheme.Hom.gysinMapCommutesWithDeRham · AlgebraicGeometry.Scheme.Hom.gysinMap_comm_deRham · Stacks.Perfect.AbelianCechCokernelPassage.map_cokernelLastDifToSupport_abelian_square · Stacks.Gysin.existsUnique_gysinHom_of_conormalRank · Stacks.Gysin.gysinHom_comm_deRham_of_conormalRank · Stacks.Gysin.conormalGysin_formRestriction_cupDegreeZero

Section50.24 Relative Poincaré duality #

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

Tag 0G8G, a situation

Tag 0G8G in the Stacks Project.

AlgebraicGeometry.RelativeDualitySituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/RelativePoincareDuality/Basic.lean, line 37.

A proper smooth morphism over a quasi-compact quasi-separated scheme, with all fibres nonempty and equidimensional of dimension n.

structure RelativeDualitySituation

Tag 0G8H, a lemma

Tag 0G8H in the Stacks Project.

AlgebraicGeometry.RelativeDualitySituation.structureSheafDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/RelativePoincareDuality/StructureSheafDirectImage.lean, line 68. The attribute's comment: “the three assertions: (1) f_O_X is a finite étale O_S-algebra (its relative Spec is finite étale over S); (2) locally on S, Rf_O_X = f_O_X ⊕ P in D(O_S) with P perfect of tor amplitude in [1, ∞); (3) d : f_O_X → f_*Ω_{X/S} is zero”.

In the relative duality situation f : X ⟶ S:

f_*𝒪_X is a finite étale 𝒪_S-algebra: the structure morphism of its relative spectrum is finite and étale;

locally on S, Rf_*𝒪_X ≅ f_*𝒪_X ⊕ P in D(𝒪_S) with P perfect of Tor amplitude in [1, ∞): every point of S has an open neighbourhood U over which this holds in D(𝒪_U);

the map d : f_*𝒪_X ⟶ f_*Ω_{X/S} is zero: the degree-zero de Rham differential vanishes on sections over f⁻¹V for every open V of S.

theorem structureSheafDirectImage (D : RelativeDualitySituation.{u}) :
    (letI := isQuasicoherent_pushforwardAlgebra_of_quasiCompact D.f;
      IsFinite (relativeSpecToBase (pushforwardAlgebra D.f)) ∧
        Etale (relativeSpecToBase (pushforwardAlgebra D.f))) ∧
    (∀ s : D.S, ∃ (U : D.S.Opens) (_ : s ∈ U)
      (P : DerivedCategory (StrictlyPerfect.OXMod.{u, u}
        (D.S.toRingedSpace.restrict U.isOpenEmbedding))),
      Stacks.Cohomology.PerfectComplexes.IsPerfect P ∧
      Stacks.Cohomology.TorAmplitude.HasTorAmplitudeGE
        (D.S.toRingedSpace.restrict U.isOpenEmbedding) P 1 ∧
      Nonempty ((RingedSpace.derivedRestrictModules D.S.toRingedSpace U).obj
          ((derivedPushforward D.f.toLRSHom.toShHom).obj
            (structureSheafDegreeZeroObj D.X)) ≅
        (DerivedCategory.singleFunctor _ 0).obj
          ((RingedSpace.restrictModules D.S.toRingedSpace U).obj
            ((Scheme.Modules.pushforward D.f).obj (Scheme.unitModule D.X))) ⊞ P)) ∧
    (∀ V : D.S.Opens, ((Scheme.Hom.deRhamComplex D.f).d 0 1).val.app (op (D.f ⁻¹ᵁ V)) = 0)

Tag 0G8I, a lemma

Tag 0G8I in the Stacks Project.

AlgebraicGeometry.RelativeDualitySituation.existsUnique_isRelativePoincareTrace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/RelativePoincareDuality/TraceFromModel.lean, line 102. The attribute's comment: “relative Poincaré duality trace: there is t : Rf_Omega^n[n] -> O_S, unique up to a unit of H^0(X, O_X), all of whose pairings Rf_Omega^p (x)^L Rf_*Omega^{n-p}[n] -> O_S are perfect pairings of perfect complexes”.

In the situation of relative Poincaré duality ([Stacks, Tag 0G8G]), f : X ⟶ S proper and smooth over a quasi-compact quasi-separated base, all of whose fibres are nonempty and equidimensional of dimension n, there is an 𝒪_S-module map t : Rf_*Ω^n_{X/S}[n] ⟶ 𝒪_S such that for all p the pairing Rf_*Ω^p_{X/S} ⊗^L Rf_*Ω^{n-p}_{X/S}[n] ⟶ 𝒪_S given by the relative cup product composed with t is a perfect pairing of perfect complexes, and t is unique up to precomposing with multiplication by a unit of H^0(X, 𝒪_X): the maps with this property are exactly the t ∘ u for u a unit of Γ(X, 𝒪_X).

theorem existsUnique_isRelativePoincareTrace :
    ∃ t : (Stacks.Duality.derivedPushforward D.f).obj ((D.f.formsInDegreeZero D.n)⟦(D.n : ℤ)⟧) ⟶
        (Stacks.Duality.derivedStructureSheafInDegree D.S 0).obj,
      D.IsRelativePoincareTrace t ∧ ∀ t', D.IsRelativePoincareTrace t' ↔
        ∃ u : (Γ(D.X, ⊤))ˣ, t' = D.f.formsShiftSMul D.n u ≫ t

Tag 0G8J, a lemma

Tag 0G8J in the Stacks Project.

Stacks.WeilDeRham.higherDirectImage_map_deRham_d_top_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilDeRham/TopDifferentialRelative.lean, line 71.

Stacks Project, Tag 0G8J. In the situation of relative Poincaré duality ([Stacks, Tag 0G8G]) — S quasi-compact and quasi-separated, f : X ⟶ S proper and smooth, all fibres nonempty and equidimensional of dimension n — the map d : Rⁿf_*Ω^{n-1}_{X/S} ⟶ Rⁿf_*Ωⁿ_{X/S} induced by the de Rham differential is zero.

theorem higherDirectImage_map_deRham_d_top_eq_zero (D : RelativeDualitySituation.{u}) :
    (Stacks.Cohomology.AbelianSheaf.higherDirectImage D.f.base D.n).map
      ((SheafOfModules.toSheaf _).map (D.f.deRhamComplex.d (D.n - 1) D.n)) = 0

Tag 0G8K, a proposition

Tag 0G8K in the Stacks Project.

AlgebraicGeometry.RelativeDualitySituation.existsUnique_deRhamPoincareTrace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/RelativePoincareDuality/DeRhamTrace/Main.lean, line 168. The attribute's comment: “relative Poincaré duality for de Rham cohomology: there is t : R^{2n}f_Omega^. -> O_S, unique up to a unit of H^0(X, O_X), such that (xi, xi') |-> t(xi cup xi') is a perfect pairing Rf_Omega^. (x)^L Rf_*Omega^.[2n] -> O_S of perfect complexes”.

[Stacks, Tag 0G8K]. In the situation of relative Poincaré duality ([Stacks, Tag 0G8G]): S quasi-compact and quasi-separated, f : X ⟶ S proper and smooth, all of whose fibres are nonempty and equidimensional of dimension n. There is an 𝒪_S-module map t : R^{2n}f_*Ω^•_{X/S} ⟶ 𝒪_S such that the pairing Rf_*Ω^•_{X/S} ⊗^L Rf_*Ω^•_{X/S}[2n] ⟶ 𝒪_S, (ξ, ξ') ↦ t(ξ ∪ ξ'), is a perfect pairing of perfect complexes (IsDeRhamPoincareTrace, read through the identification Hom(Rf_*(Ω^•[2n]), 𝒪_S) ≃ Hom(R^{2n}f_*Ω^•, 𝒪_S) of deRhamTraceEquiv, which holds as Rf_*(Ω^•[2n]) has no cohomology in positive degrees), and t is unique up to precomposing with multiplication by a unit of H^0(X, 𝒪_X): the maps with this property are exactly the t ∘ u for u a unit of Γ(X, 𝒪_X).

theorem existsUnique_deRhamPoincareTrace :
    ∃ t : D.deRhamTopCohomology ⟶ SheafOfModules.unit D.S.ringCatSheaf,
      D.IsDeRhamPoincareTrace (D.deRhamTraceEquiv.symm t) ∧
      ∀ t' : D.deRhamTopCohomology ⟶ SheafOfModules.unit D.S.ringCatSheaf,
        D.IsDeRhamPoincareTrace (D.deRhamTraceEquiv.symm t') ↔
          ∃ u : (Γ(D.X, ⊤))ˣ, t' = D.deRhamTopCohomologySMul (u : Γ(D.X, ⊤)) ≫ t

Sources

LeanAlgebraicGeometry.RelativeDualitySituation · AlgebraicGeometry.RelativeDualitySituation.structureSheafDirectImage · AlgebraicGeometry.RelativeDualitySituation.existsUnique_isRelativePoincareTrace · Stacks.WeilDeRham.higherDirectImage_map_deRham_d_top_eq_zero · AlgebraicGeometry.RelativeDualitySituation.existsUnique_deRhamPoincareTrace

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

50.17 Blowing up and de Rham… to 50.24 Relative Poincaré duality

Section50.17 Blowing up and de Rham cohomology#

Tag 0FUU, a lemma

Tag 0FUV, a lemma

Tag 0FUW, a proposition

Tag 0G5I, a lemma

Tag 0G5J, a lemma

Sources

Section50.18 Comparing sheaves of differential forms#

Tag 0FL8, a lemma

Tag 0H9F, a lemma

Tag 0FL9, a remark

Tag 0H9G, a lemma

Tag 0H9H, a lemma

Tag 0FLA, a lemma

Sources

Section50.19 Trace maps on de Rham complexes#

Tag 0FK7, an example

Tag 0FLB, a lemma

Tag 0FLC, a proposition

Tag 0FLD, an example

Tag 0FW2, a lemma

Sources

Section50.20 Poincaré duality#

Tag 0FW4, a lemma

Tag 0FW5, a lemma

Tag 0FW6, a lemma

Tag 0FW7, a proposition

Sources

Section50.21 Chern classes#

Tag 0FW9, a lemma

Tag 0FWA, a remark

Tag 0FWB, a lemma

Sources

Section50.22 A Weil cohomology theory#

Tag 0FWD, a proposition

Tag 0FWE, a remark

Sources

Section50.23 Gysin maps for closed immersions#

Tag 0G83, a remark

Tag 0G84, an equation

Tag 0G85, a lemma

Tag 0G86, a lemma

Tag 0G87, a lemma

Tag 0G88, a lemma

Tag 0G89, a lemma

Tag 0G8A, a remark

Tag 0G8B, a lemma

Tag 0G8C, a lemma

Tag 0G8D, a lemma

Tag 0G8E, a lemma

Sources

Section50.24 Relative Poincaré duality#

Tag 0G8G, a situation

Tag 0G8H, a lemma

Tag 0G8I, a lemma

Tag 0G8J, a lemma

Tag 0G8K, a proposition

Sources

Section50.17 Blowing up and de Rham cohomology #

Section50.18 Comparing sheaves of differential forms #

Section50.19 Trace maps on de Rham complexes #

Section50.20 Poincaré duality #

Section50.21 Chern classes #

Section50.22 A Weil cohomology theory #

Section50.23 Gysin maps for closed immersions #

Section50.24 Relative Poincaré duality #