42.19 Rational equivalence to 42.30 Gysin homomorphisms and…

Section42.19 Rational equivalence#

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

Tag 02RW, a definition

Tag 02RW in the Stacks Project.

Stacks.Chow.exists_principalDivisorFamilySum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DimensionFunction/PrincipalDivisorFamily.lean, line 110. The attribute's comment: “locally finite sums of principal divisors”.

Stacks 02RW. A locally finite family of integral closed subschemes of X of delta-dimension k + 1, each carrying a nonzero rational function, determines a cycle of delta-dimension k on X, whose coefficients are the locally finite sums of the coefficients of the pushed-forward principal divisors.

theorem exists_principalDivisorFamilySum (C : ChowSituation.{u}) {X : Scheme.{u}}
    (p : X ⟶ C.S) [LocallyOfFiniteType p] (k : ℤ) {J : Type u} (W : J → X.IdealSheafData)
    (hW : ∀ j, IsIntegral (W j).subscheme)
    (hDim : ∀ j, schemeDeltaDimension C ((W j).subschemeι ≫ p) = ((k + 1 : ℤ) : EInt))
    (hLocal : LocallyFinite fun j ↦ ((W j).support : Set X))
    (g : ∀ j, (rationalFunctions (W j).subscheme)ˣ) :
    ∃ α : CycleGroup C p k,
      ∀ x : X, α.1 x = principalDivisorFamilyCoefficient C p W hW g x

Stacks.Chow.IsRationallyEquivalentToZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalenceDefs.lean, line 330. The attribute's comment: “rationally equivalent to zero”.

Stacks 02RW. A k-cycle is rationally equivalent to zero when its coefficients are the locally finite sum of the pushforwards of the principal divisors of nonzero rational functions on a locally finite family of integral closed subschemes of delta-dimension k + 1.

def IsRationallyEquivalentToZero (C : ChowSituation.{u}) {X : Scheme.{u}} (p : X ⟶ C.S)
    [LocallyOfFiniteType p] (k : ℤ) (α : CycleGroup C p k) : Prop

Stacks.Chow.rationallyEquivalentToZero_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalenceDefs.lean, line 352. The attribute's comment: “zero family”.

Stacks 02RW. The zero cycle is rationally equivalent to zero, via the empty family.

theorem rationallyEquivalentToZero_zero (C : ChowSituation.{u}) {X : Scheme.{u}}
    (p : X ⟶ C.S) [LocallyOfFiniteType p] (k : ℤ) :
    IsRationallyEquivalentToZero C p k 0

Stacks.Chow.rationallyEquivalentToZero_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalenceDefs.lean, line 363. The attribute's comment: “closure under addition”.

Stacks 02RW. The sum of two cycles rationally equivalent to zero is rationally equivalent to zero, via the disjoint union of the two families.

theorem rationallyEquivalentToZero_add (C : ChowSituation.{u}) {X : Scheme.{u}}
    (p : X ⟶ C.S) [LocallyOfFiniteType p] (k : ℤ) {α β : CycleGroup C p k}
    (hα : IsRationallyEquivalentToZero C p k α)
    (hβ : IsRationallyEquivalentToZero C p k β) :
    IsRationallyEquivalentToZero C p k (α + β)

Stacks.Chow.rationallyEquivalentToZero_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalenceDefs.lean, line 386. The attribute's comment: “closure under negation”.

Stacks 02RW. The negative of a cycle rationally equivalent to zero is rationally equivalent to zero, via the inverses of the same rational functions.

theorem rationallyEquivalentToZero_neg (C : ChowSituation.{u}) {X : Scheme.{u}}
    (p : X ⟶ C.S) [LocallyOfFiniteType p] (k : ℤ) {α : CycleGroup C p k}
    (hα : IsRationallyEquivalentToZero C p k α) :
    IsRationallyEquivalentToZero C p k (-α)

Stacks.Chow.rationalEquivalences, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalenceDefs.lean, line 402. The attribute's comment: “cycles rationally equivalent to zero”.

Stacks 02RW. The subgroup of k-cycles rationally equivalent to zero.

def rationalEquivalences (C : ChowSituation.{u}) {X : Scheme.{u}} (p : X ⟶ C.S)
    [LocallyOfFiniteType p] (k : ℤ) : AddSubgroup (CycleGroup C p k)

Stacks.Chow.RationallyEquivalent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalenceDefs.lean, line 419. The attribute's comment: “rational equivalence”.

Stacks 02RW. Two k-cycles are rationally equivalent when their difference is a locally finite sum of pushforwards of principal divisors.

abbrev RationallyEquivalent (C : ChowSituation.{u}) {X : Scheme.{u}} (p : X ⟶ C.S)
    [LocallyOfFiniteType p] (k : ℤ) (α β : CycleGroup C p k) : Prop

Stacks.Chow.chowGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalenceDefs.lean, line 425. The attribute's comment: “Chow group”. References: SGA 6 XIV (4.1), “partial”.

Stacks 02RW. The Chow group A_k(X) of k-cycles modulo rational equivalence.

abbrev chowGroup (C : ChowSituation.{u}) {X : Scheme.{u}} (p : X ⟶ C.S)
    [LocallyOfFiniteType p] (k : ℤ) : Type u

Tag 0GU3, a remark

Tag 0GU3 in the Stacks Project.

Stacks.Chow.pointwiseDivisorDifferential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/PointwiseDivisor.lean, line 465. The attribute's comment: “pointwise_divisor_differential”.

Stacks 0GU3. The divisor differential from pointwise Milnor K₁-chains at the points of relative dimension k + 1 to pointwise Milnor K₀-chains at the points of relative dimension k: each Milnor K₁-class is read as a nonzero rational function on the closure of its point, and the differential is the locally finite sum of the pushed-forward principal divisors, transported to the pointwise description of cycles of Stacks 0GU2.

def pointwiseDivisorDifferential (k : ℤ) :
    PointwiseKOneGroup C p k →+ PointwiseCycleGroup C p k

Stacks.Chow.pointwiseDivisorDifferential_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/PointwiseDivisor.lean, line 474. The attribute's comment: “pointwise_divisor_differential”.

Stacks 0GU3. The divisor differential satisfies the coordinatewise divisor formula.

theorem pointwiseDivisorDifferential_spec (k : ℤ) :
    IsPointwiseDivisorDifferential C p k (pointwiseDivisorDifferential C p k)

Stacks.Chow.exists_pointwiseDivisorDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/PointwiseDivisor.lean, line 487. The attribute's comment: “pointwise_divisor_differential”.

Stacks 0GU3. There is a homomorphism from pointwise Milnor K₁-chains to pointwise Milnor K₀-chains satisfying the coordinatewise divisor formula.

theorem exists_pointwiseDivisorDifferential (k : ℤ) :
    ∃ d : PointwiseKOneGroup C p k →+ PointwiseCycleGroup C p k,
      IsPointwiseDivisorDifferential C p k d

Stacks.Chow.pointwiseChowClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/PointwisePresentation.lean, line 75. The attribute's comment: “the map from pointwise cycles to the Chow group”.

Stacks 0GU3. The class in the Chow group A_k(X) of a locally finite family of degree-zero Milnor K-classes at the points of relative dimension k: the cycle it names, modulo rational equivalence.

def pointwiseChowClass (k : ℤ) : PointwiseCycleGroup C p k →+ chowGroup C p k

Stacks.Chow.pointwiseChowClass_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/PointwisePresentation.lean, line 92. The attribute's comment: “surjectivity of the presentation”.

Stacks 0GU3. Every class in the Chow group A_k(X) is the class of a pointwise Milnor K₀ chain: the chain attached to any cycle representing it.

theorem pointwiseChowClass_surjective (k : ℤ) :
    Function.Surjective (pointwiseChowClass C p k)

Stacks.Chow.pointwiseDivisorDifferential_range_eq_ker_pointwiseChowClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/PointwisePresentation.lean, line 424. The attribute's comment: “exactness of the presentation”.

Stacks 0GU3. The presentation of the Chow group is exact in the middle: a pointwise Milnor K₀-chain is a pointwise divisor exactly when the cycle it names is rationally equivalent to zero.

theorem pointwiseDivisorDifferential_range_eq_ker_pointwiseChowClass (k : ℤ) :
    (pointwiseDivisorDifferential C p k).range = (pointwiseChowClass C p k).ker

Tag 02RX, a lemma

Tag 02RX in the Stacks Project.

Stacks.Chow.exists_rationallyEquivalent_properPushforward_of_cycleGroupRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/LocalizationSequence.lean, line 141. The attribute's comment: “lifting a rational equivalence from an open subscheme”.

Let V ⊆ X be an open subscheme and let i : Y ⟶ X be a closed immersion whose image is the complement of V. If two k-cycles on X become rationally equivalent after restriction to V, then they are rationally equivalent on X up to the pushforward of a k-cycle on Y.

theorem exists_rationallyEquivalent_properPushforward_of_cycleGroupRestrict
    (C : ChowSituation.{u}) {X Y : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (i : Y ⟶ X) [IsClosedImmersion i] (hi : i ≫ sX = sY)
    (V : X.Opens) (hcomplement : Set.range i.base = (Set.range V.ι.base)ᶜ)
    (k : ℤ) (α β : CycleGroup C sX k)
    (h : RationallyEquivalent C (V.ι ≫ sX) k
      (cycleGroupOpensRestrict C sX V k α) (cycleGroupOpensRestrict C sX V k β)) :
    ∃ γ : CycleGroup C sY k,
      RationallyEquivalent C sX k α (β + properPushforward C sY sX i hi k γ)

Stacks.Chow.surjective_chowGroupOpensRestrictOfIsOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/LocalizationSequence.lean, line 198. The attribute's comment: “surjectivity onto the Chow group of the open subscheme”.

The localization sequence of Chow groups is exact at A_k(V): restriction of k-cycle classes to an open subscheme V ⊆ X is surjective.

theorem surjective_chowGroupOpensRestrictOfIsOpenImmersion (C : ChowSituation.{u})
    {X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (V : X.Opens) (k : ℤ) :
    Function.Surjective (chowGroupOpensRestrictOfIsOpenImmersion C sX V k)

Stacks.Chow.exact_chowPushforward_chowGroupOpensRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/LocalizationSequence.lean, line 212. The attribute's comment: “exactness at the Chow group of the ambient scheme”.

The localization sequence of Chow groups is exact at A_k(X): for an open subscheme V ⊆ X and a closed immersion i : Y ⟶ X whose image is the complement of V, a k-cycle class on X restricts to zero on V exactly when it is the pushforward of a k-cycle class on Y.

theorem exact_chowPushforward_chowGroupOpensRestrict (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
    [LocallyOfFiniteType sY] (i : Y ⟶ X) [IsClosedImmersion i] (hi : i ≫ sX = sY)
    (V : X.Opens) (hcomplement : Set.range i.base = (Set.range V.ι.base)ᶜ) (k : ℤ) :
    Function.Exact (chowPushforwardOfIsClosedImmersion C sY sX i hi k)
      (chowGroupOpensRestrictOfIsOpenImmersion C sX V k)

Tag 0F94, a lemma

Tag 0F94 in the Stacks Project.

Stacks.Chow.exact_intersectionToSummandsChow_summandsToUnionChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/ClosedCoverExactSequence.lean, line 423. The attribute's comment: “exactness in the middle”.

The sequence of Chow groups of a union of two closed subschemes is exact in the middle: a pair of classes of k-cycles on the two closed subschemes has vanishing sum of pushforwards exactly when it comes from a class of k-cycles on the scheme-theoretic intersection.

theorem exact_intersectionToSummandsChow_summandsToUnionChow
    (hcover : I.support ⊔ J.support = ⊤) :
    Function.Exact (intersectionToSummandsChow C sX I J k) (summandsToUnionChow C sX I J k)

Stacks.Chow.surjective_summandsToUnionChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/ClosedCoverExactSequence.lean, line 435. The attribute's comment: “surjectivity”.

If two closed subschemes cover the ambient scheme set-theoretically, every class of k-cycles on it is the sum of the classes of the pushforwards of a k-cycle on each of them.

theorem surjective_summandsToUnionChow (hcover : I.support ⊔ J.support = ⊤) :
    Function.Surjective (summandsToUnionChow C sX I J k)

Stacks.Chow.surjective_chowPushforwardOfIsClosedImmersion_coprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/ClosedImmersionCoverExactSequence.lean, line 134. The attribute's comment: “surjectivity, for two arbitrary closed immersions”.

Stacks 0F94, surjectivity, for two closed immersions. If the images of two closed immersions j₁ : X₁ ⟶ X and j₂ : X₂ ⟶ X cover X, every class of k-cycles on X is the sum of the pushforwards of a class on X₁ and a class on X₂.

theorem surjective_chowPushforwardOfIsClosedImmersion_coprod
    (hcover : Set.range j₁ ∪ Set.range j₂ = Set.univ) :
    Function.Surjective ((chowPushforwardOfIsClosedImmersion C sX₁ sX j₁ hj₁ k).coprod
      (chowPushforwardOfIsClosedImmersion C sX₂ sX j₂ hj₂ k))

Stacks.Chow.exact_chowPushforwardOfIsClosedImmersion_prod_coprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/ClosedImmersionCoverExactSequence.lean, line 179. The attribute's comment: “exactness in the middle, for two arbitrary closed immersions”.

Stacks 0F94, exactness in the middle, for two closed immersions. If the images of two closed immersions j₁ : X₁ ⟶ X and j₂ : X₂ ⟶ X cover X, a pair of classes of k-cycles on X₁ and X₂ has vanishing sum of pushforwards exactly when it is the pair of pushforwards of a class on the fibre product X₁ ×_X X₂, the second one negated.

theorem exact_chowPushforwardOfIsClosedImmersion_prod_coprod
    (hcover : Set.range j₁ ∪ Set.range j₂ = Set.univ) :
    Function.Exact
      ((chowPushforwardOfIsClosedImmersion C (pullback.fst j₁ j₂ ≫ sX₁) sX₁
          (pullback.fst j₁ j₂) rfl k).prod
        (-chowPushforwardOfIsClosedImmersion C (pullback.fst j₁ j₂ ≫ sX₁) sX₂
          (pullback.snd j₁ j₂)
          (pullbackSnd_comp_structureMorphism_eq_fst C sX j₁ j₂ sX₁ sX₂ hj₁ hj₂)
          k))
      ((chowPushforwardOfIsClosedImmersion C sX₁ sX j₁ hj₁ k).coprod
        (chowPushforwardOfIsClosedImmersion C sX₂ sX j₂ hj₂ k))

Tag 02RZ, a remark

Tag 02RZ in the Stacks Project.

Stacks.Chow.rationallyEquivalent_finsum_of_closedSupports, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChowToolkit/ClosedImmersionCarrier.lean, line 250.

Stacks 02RZ, two-sided form. Rational equivalences on a locally finite family of closed subschemes of X may be summed: if cycles a i and b i on the closed subschemes T i are rationally equivalent for each i, and the cycles α, β on X are coefficientwise the locally finite sums of the pushforwards of the a i and of the b i, then α and β are rationally equivalent on X.

Both locally finite sums have finite support at each point, because the pushforward of a cycle on T i is supported on (T i).support and the family of those supports is locally finite. So they may be subtracted termwise, which exhibits α - β as the locally finite sum of the pushforwards of the a i - b i, each rationally equivalent to zero, and Stacks.Chow.rationallyEquivalentToZero_finsum_of_closedSupports applies.

theorem rationallyEquivalent_finsum_of_closedSupports (p : X ⟶ C.S)
    [LocallyOfFiniteType p] (k : ℤ) {I : Type u} (T : I → X.IdealSheafData)
    (hT : LocallyFinite fun i ↦ ((T i).support : Set X))
    (a b : ∀ i, CycleGroup C ((T i).subschemeι ≫ p) k)
    (hab : ∀ i, RationallyEquivalent C ((T i).subschemeι ≫ p) k (a i) (b i))
    {α β : CycleGroup C p k}
    (hα : ∀ x : X, α.1 x = ∑ᶠ i : I,
      (properPushforward C ((T i).subschemeι ≫ p) p (T i).subschemeι rfl k (a i)).1 x)
    (hβ : ∀ x : X, β.1 x = ∑ᶠ i : I,
      (properPushforward C ((T i).subschemeι ≫ p) p (T i).subschemeι rfl k (b i)).1 x) :
    RationallyEquivalent C p k α β

Sources

• Section 42.19, Tag 02RV
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.exists_principalDivisorFamilySum · Stacks.Chow.IsRationallyEquivalentToZero · Stacks.Chow.rationallyEquivalentToZero_zero · Stacks.Chow.rationallyEquivalentToZero_add · Stacks.Chow.rationallyEquivalentToZero_neg · Stacks.Chow.rationalEquivalences · Stacks.Chow.RationallyEquivalent · Stacks.Chow.chowGroup

Section42.20 Rational equivalence and push and pull#

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

Tag 0EPH, a lemma

Tag 0EPH in the Stacks Project.

Stacks.Chow.flatPullback_principalDivisor_eq_sum_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/FlatPullbackPrincipalDivisor.lean, line 1030.

Stacks 0EPH. Let C = (S, δ) be the base situation of chapter 42, let X and Y be locally of finite type over S with Y integral of delta-dimension k, and let f : X ⟶ Y be flat of relative dimension r. For a nonzero rational function g on Y,

f^* div_Y(g) = ∑_j n_j i_{j,*} div_{X_j}(g ∘ f|_{X_j})

as (k + r - 1)-cycles on X, where the sum is over the irreducible components X_j of X with their reduced structure and n_j is the multiplicity of X_j in the fundamental cycle [X]_{k + r}. The identity is read coefficientwise at a point x of X.

theorem flatPullback_principalDivisor_eq_sum_components (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
    [LocallyOfFiniteType sY] [IsIntegral Y] (f : X ⟶ Y) [LocallyOfFiniteType f] [Flat f]
    (hbase : f ≫ sY = sX) (r : ℕ) (hf : AlgebraicGeometry.RelativeDimension f r) {k : ℤ}
    (hY : schemeDeltaDimension C sY = (k : EInt)) (g : Y.functionField) (hg : g ≠ 0) (x : X) :
    (flatPullback C sX sY f hbase r hf (k - 1) (principalDivisorCycle C sY hY g)).1 x =
      ∑ᶠ W : irreducibleComponents X,
        (cycleAssociatedToClosedSubscheme C sX (𝟙 X) (k + (r : ℤ))).1 W.2.1.genericPoint *
          (letI : IsIntegral (integralComponentAt W.2.1.genericPoint).subscheme :=
             isIntegral_integralComponentAt _
           letI := isDominant_subschemeι_integralComponentAt_comp f W
           (properPushforward C ((integralComponentAt W.2.1.genericPoint).subschemeι ≫ sX) sX
             (integralComponentAt W.2.1.genericPoint).subschemeι rfl (k + (r : ℤ) - 1)
             (principalDivisorCycle C _
               (schemeDeltaDimension_integralComponentAt_comp C sX sY f hbase r hf hY W)
               (dominantFunctionFieldMap
                 ((integralComponentAt W.2.1.genericPoint).subschemeι ≫ f) g))).1 x)

Tag 02S1, a lemma

Tag 02S1 in the Stacks Project.

Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ClopenDecomposition/OpenImmersionPieces.lean, line 163. The attribute's comment: “flat pullback along an arbitrary open immersion preserves rational equivalence”.

Stacks 02S1 along an arbitrary open immersion. Flat pullback along an open immersion over the base carries cycles rationally equivalent to zero to cycles rationally equivalent to zero.

Flat pullback along an open immersion in relative dimension zero is restriction of cycles, by Stacks.Chow.cycleGroupRestrict_eq_flatPullback, up to a transport of the degree from k + 0 to k; the statement for restriction is Stacks.Chow.cycleGroupRestrict_mem_rationalEquivalences.

theorem flatPullbackFactorsThroughRationalEquivalence_of_isOpenImmersion :
    FlatPullbackFactorsThroughRationalEquivalence C sU sX j hj 0
      (relativeDimension_of_isOpenImmersion j) k

Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FlatPullback/GeneralRationalEquivalence.lean, line 159. The attribute's comment: “the general case: an arbitrary flat morphism of relative dimension r”.

Stacks 02S1. Flat pullback of k-cycles along a morphism f : X' ⟶ X of schemes locally of finite type over the base which is flat and locally of finite type of relative dimension r carries cycles rationally equivalent to zero to cycles rationally equivalent to zero.

A presentation ∑_j (i_j)_* div_{W_j}(g_j) of a rational equivalence on X by a locally finite family of integral closed subschemes W_j ⊆ X of delta-dimension k + 1 is pulled back term by term. The closed-immersion case of Stacks 02RG rewrites the pullback of each term as a pushforward from the scheme-theoretic inverse image f^{-1}(W_j) of a cycle on f^{-1}(W_j), which is rationally equivalent to zero there by the case of Stacks 02S1 for a principal divisor on an integral target. Those inverse images have as supports the preimages of the supports of the W_j, so they form a locally finite family by Stacks 02R9, and Stacks 02RZ sums the pushforwards into a single rational equivalence.

theorem flatPullbackFactorsThroughRationalEquivalence_general (C : ChowSituation.{u})
    {X' X : Scheme.{u}} (sX' : X' ⟶ C.S) [LocallyOfFiniteType sX'] (sX : X ⟶ C.S)
    [LocallyOfFiniteType sX] (f : X' ⟶ X) [LocallyOfFiniteType f] [Flat f]
    (hbase : f ≫ sX = sX') (r : ℕ) (hf : AlgebraicGeometry.RelativeDimension f r) (k : ℤ) :
    FlatPullbackFactorsThroughRationalEquivalence C sX' sX f hbase r hf k

Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_of_opensι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FlatPullback/OpenImmersionRationalEquivalence.lean, line 195. The attribute's comment: “flat pullback along an open immersion preserves rational equivalence”.

Stacks 02S1 along the inclusion of an open subscheme. Flat pullback of k-cycles along the inclusion of an open subscheme V ⊆ X carries cycles rationally equivalent to zero to cycles rationally equivalent to zero.

A presentation ∑_j (i_j)_* div(g_j) of a rational equivalence on X, by a locally finite family of integral closed subschemes W_j of delta-dimension k + 1, restricts to the presentation by the inverse images W_j ×_X V of those members whose generic point lies in V, carrying the restrictions of the g_j. The members whose generic point misses V are supported off V and contribute nothing there; the surviving inverse images are integral by Stacks.Chow.comap_integralComponentAt_of_isOpenImmersion, keep their delta-dimension by Stacks.Chow.schemeDeltaDimension_eq_of_isOpenImmersion, form a locally finite family because their supports are preimages, and their terms have the right coefficients by Stacks.Chow.principalDivisorPushforward_comap_opensι.

theorem flatPullbackFactorsThroughRationalEquivalence_of_opensι (C : ChowSituation.{u})
    {X : Scheme.{u}} (f : X ⟶ C.S) [LocallyOfFiniteType f] (V : X.Opens) (k : ℤ) :
    FlatPullbackFactorsThroughRationalEquivalence C (V.ι ≫ f) f V.ι rfl 0
      (relativeDimension_opensι V) k

Stacks.Chow.isRationallyEquivalentToZero_of_coe_eq_flatPullback_principalDivisorCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/FlatPullbackPrincipalDivisorEquivalence.lean, line 102. The attribute's comment: “the case of a principal divisor on an integral target”.

Stacks 02S1 for a principal divisor on an integral target. Let X and Y be locally of finite type over the base of chapter 42 with Y integral of delta-dimension k, let f : X ⟶ Y be flat of relative dimension r, and let g be a nonzero rational function on Y. Then the flat pullback f^* div_Y(g) of the principal divisor of g is rationally equivalent to zero, as a (k + r - 1)-cycle on X.

Stacks 0EPH writes that pullback as the locally finite sum ∑_j n_j (i_j)_* div_{X_j}(g) over the irreducible components X_j of X taken with their reduced structure. Each X_j is integral of delta-dimension k + r, so div_{X_j}(g) is rationally equivalent to zero on X_j by Stacks 02RW, and the multiplicity n_j is absorbed by the subgroup. The components form a locally finite family by Stacks 0BE1, so Stacks 02RZ sums the pushforwards into a single rational equivalence on X.

theorem isRationallyEquivalentToZero_of_coe_eq_flatPullback_principalDivisorCycle
    (C : ChowSituation.{u}) {X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] [IsIntegral Y] (f : X ⟶ Y)
    [LocallyOfFiniteType f] [Flat f] (hbase : f ≫ sY = sX) (r : ℕ)
    (hf : AlgebraicGeometry.RelativeDimension f r) {k j : ℤ}
    (hY : schemeDeltaDimension C sY = (k : EInt)) {g : Y.functionField} (hg : g ≠ 0)
    (hj : j = k + (r : ℤ) - 1) (α : CycleGroup C sX j)
    (hα : ∀ x : X, α.1 x =
      (flatPullback C sX sY f hbase r hf (k - 1) (principalDivisorCycle C sY hY g)).1 x) :
    IsRationallyEquivalentToZero C sX j α

Tag 02S2, a lemma

Tag 02S2 in the Stacks Project.

Stacks.Chow.properPushforwardFactorsThroughRationalEquivalence_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProperPushforwardPrincipal/GenericFibre.lean, line 337. The attribute's comment: “pushforward kills rational equivalence”.

Proper pushforward of k-cycles along a proper morphism over the base carries cycles rationally equivalent to zero to cycles rationally equivalent to zero.

theorem properPushforwardFactorsThroughRationalEquivalence_of_isProper (k : ℤ) :
    ProperPushforwardFactorsThroughRationalEquivalence C sX sY p hp k

Stacks.Chow.properPushforward_rationallyEquivalent_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProperPushforwardPrincipal/RationalEquivalenceUnconditional.lean, line 30.

Proper pushforward preserves rational equivalence of cycles: if α and β are rationally equivalent k-cycles on X and p : X ⟶ Y is proper over the base, then p_*α and p_*β are rationally equivalent k-cycles on Y.

theorem properPushforward_rationallyEquivalent_of_isProper (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
    [LocallyOfFiniteType sY] (p : X ⟶ Y) [IsProper p] (hp : p ≫ sY = sX) (k : ℤ)
    {α β : CycleGroup C sX k} (h : RationallyEquivalent C sX k α β) :
    RationallyEquivalent C sY k (properPushforward C sX sY p hp k α)
      (properPushforward C sX sY p hp k β)

Sources

• Section 42.20, Tag 02S0
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.flatPullback_principalDivisor_eq_sum_components · Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_of_isOpenImmersion · Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_general · Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_of_opensι · Stacks.Chow.isRationallyEquivalentToZero_of_coe_eq_flatPullback_principalDivisorCycle · Stacks.Chow.properPushforwardFactorsThroughRationalEquivalence_of_isProper · Stacks.Chow.properPushforward_rationallyEquivalent_of_isProper

Section42.21 Rational equivalence and the projective line#

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

Tag 02S4, a lemma

Tag 02S4 in the Stacks Project.

Stacks.Chow.zeroDivisor_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FamilyFibreDivisors/LocallyPrincipal.lean, line 120. The attribute's comment: “part (1): zero divisor”.

Stacks Project, Tag 02S4, part (1), for the zero divisor. If W is integral and is not contained in the image of the zero section, then the zero divisor of W is an effective Cartier divisor on W.

theorem zeroDivisor_isEffectiveCartierDivisor [IsIntegral W.subscheme]
    (h : ¬ Set.range W.subschemeι ⊆ Set.range (zeroSection f)) :
    Stacks.Divisors.IsEffectiveCartierDivisor (zeroDivisor f W)

Stacks.Chow.infinityDivisor_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FamilyFibreDivisors/LocallyPrincipal.lean, line 170. The attribute's comment: “part (1): infinity divisor”.

Stacks Project, Tag 02S4, part (1), for the infinity divisor. If W is integral and is not contained in the image of the infinity section, then the infinity divisor of W is an effective Cartier divisor on W.

theorem infinityDivisor_isEffectiveCartierDivisor [IsIntegral W.subscheme]
    (h : ¬ Set.range W.subschemeι ⊆ Set.range (infinitySection f)) :
    Stacks.Divisors.IsEffectiveCartierDivisor (infinityDivisor f W)

Stacks.Chow.exists_familyFibreDifferences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FibreCycles/FamilyFibreDifferenceExistence.lean, line 584. The attribute's comment: “part (4)”.

Stacks Project, Tag 02S4, part (4). A k-cycle rationally equivalent to zero is the total fibre difference of a locally finite family of integral closed subschemes of X ×_S 𝐏¹_S, each of relative dimension k + 1 at its generic points and contained in neither distinguished section.

This is the converse of part (3): the family is produced from the family of integral closed subschemes and rational functions witnessing rational equivalence, by replacing each member by the closure of the graph of its rational function, read inside X ×_S 𝐏¹_S. The index type is unchanged.

theorem exists_familyFibreDifferences (k : ℤ) (α : CycleGroup C f k)
    (hα : IsRationallyEquivalentToZero C f k α) :
    ∃ (J : Type u) (W : J → (projectiveLineProduct f).IdealSheafData)
      (hInt : ∀ j, IsIntegral (W j).subscheme)
      (hDim : ∀ j, ∀ ξ : genericPoints (W j).subscheme,
        relativeDimension C.dimensionFunction (familyBase f (W j)) ξ.1 = k + 1),
      (∀ j, ¬ Set.range (W j).subschemeι ⊆ Set.range (zeroSection f)) ∧
      (∀ j, ¬ Set.range (W j).subschemeι ⊆ Set.range (infinitySection f)) ∧
      LocallyFinite (fun j ↦ ((W j).support : Set (projectiveLineProduct f))) ∧
      (∀ x : X, α.1 x = familyFibreDifferenceCoefficient C f k W x)

Stacks.Chow.fibreCycles_rationallyEquivalent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProperPushforwardPrincipal/DimensionDropApplications.lean, line 221. The attribute's comment: “part (2)”.

Stacks 02S4 part (2), in the two-cycle form the tag states.

theorem fibreCycles_rationallyEquivalent
    (W : (projectiveLineProduct f).IdealSheafData) [IsIntegral W.subscheme]
    (hDim : ∀ ξ : genericPoints W.subscheme,
      relativeDimension C.dimensionFunction (familyBase f W) ξ.1 = k + 1)
    (h₀ : ¬ Set.range W.subschemeι ⊆ Set.range (zeroSection f))
    (hInf : ¬ Set.range W.subschemeι ⊆ Set.range (infinitySection f)) :
    RationallyEquivalent C f k
      (cycleAssociatedToClosedSubscheme C f (zeroFiber f W).subschemeι k)
      (cycleAssociatedToClosedSubscheme C f (infinityFiber f W).subschemeι k)

Stacks.Chow.familyFibreDifferencesRationallyEquivalentToZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProperPushforwardPrincipal/DimensionDropApplications.lean, line 236. The attribute's comment: “part (3)”.

Stacks 02S4 part (3). The family form, for a locally finite family of integral closed subschemes of X ×_S ℙ¹_S.

theorem familyFibreDifferencesRationallyEquivalentToZero :
    FamilyFibreDifferencesRationallyEquivalentToZero C f k

Tag 02S5, a lemma

Tag 02S5 in the Stacks Project.

Stacks.Chow.cycleAssociatedToFibres_rationallyEquivalent_of_isEmbeddedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FibreCycles/EmbeddedPointHypothesis.lean, line 206.

Stacks 02S5, with hypothesis (3) in the shape the source states it. For a closed subscheme Z ⊆ X ×_S 𝐏¹_S with dim_δ(Z) ≤ k + 1 and dim_δ(Z₀) ≤ k, dim_δ(Z_∞) ≤ k, the cycles of the two fibres are rationally equivalent on X as soon as

• hEmbedded, the source's hypothesis (3): every embedded point of Z either misses both distinguished sections or has relative dimension below k; and
• hGeneric, the clause the source omits: no irreducible component of Z of relative dimension exactly k has its generic point on a distinguished section.

hGeneric cannot be dropped — see the module documentation for an integral Z with no embedded points at all for which the conclusion fails. Together the two clauses give the hypothesis of Stacks.Chow.cycleAssociatedToFibres_rationallyEquivalent, by Stacks.Chow.sectionAvoidance_of_isEmbeddedPoint_of_genericPoints, and are given by it, by Stacks.Chow.mem_schemeAssociatedPoints_of_isEmbeddedPoint and AlgebraicGeometry.mem_schemeAssociatedPoints_of_isGenericPoint_irreducibleComponent.

theorem cycleAssociatedToFibres_rationallyEquivalent_of_isEmbeddedPoint
    (hZ : ∀ ζ : Z.subscheme,
      relativeDimension C.dimensionFunction (familyBase f Z) ζ ≤ k + 1)
    (h₀ : schemeDeltaDimension C ((zeroFiber f Z).subschemeι ≫ f) ≤ (k : EInt))
    (hInf : schemeDeltaDimension C ((infinityFiber f Z).subschemeι ≫ f) ≤ (k : EInt))
    (hEmbedded : ∀ ζ : Z.subscheme, AlgebraicGeometry.IsEmbeddedPoint Z.subscheme ζ →
      ((Z.subschemeι ζ ∉ Set.range (zeroSection f) ∧
          Z.subschemeι ζ ∉ Set.range (infinitySection f)) ∨
        relativeDimension C.dimensionFunction (familyBase f Z) ζ < k))
    (hGeneric : ∀ ζ : Z.subscheme, ζ ∈ genericPoints Z.subscheme →
      relativeDimension C.dimensionFunction (familyBase f Z) ζ = k →
      (Z.subschemeι ζ ∉ Set.range (zeroSection f) ∧
        Z.subschemeι ζ ∉ Set.range (infinitySection f))) :
    RationallyEquivalent C f k
      (cycleAssociatedToClosedSubscheme C f (zeroFiber f Z).subschemeι k)
      (cycleAssociatedToClosedSubscheme C f (infinityFiber f Z).subschemeι k)

Stacks.Chow.cycleAssociatedToFibres_rationallyEquivalent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProperPushforwardPrincipal/DimensionDropApplications.lean, line 258.

Stacks 02S5. For a closed subscheme Z ⊆ X ×_S ℙ¹_S whose relative dimension is at most k + 1, whose two fibres have delta-dimension at most k, and each of whose associated points either misses both distinguished sections or has relative dimension below k, the cycles of the two fibres are rationally equivalent on X.

Both inputs are now theorems: the decomposition rule is Stacks.Chow.fibreCycleComponentDecompositionRule and part (2) of Stacks 02S4 is Stacks.Chow.fibreCyclesRationallyEquivalentWithin.

The source states its hypothesis (3) for the embedded points of Z rather than for all of its associated points. That reading is strictly weaker and the lemma is false under it; the two differ exactly at the generic points of the irreducible components of Z of relative dimension k, which the source's proof silently assumes away when it reads dim(A/I) = 1 off δ(ξ) = k. Stacks.Chow.cycleAssociatedToFibres_rationallyEquivalent_of_isEmbeddedPoint (StacksFrontier/AlgebraicGeometry/Chow/FibreCycles/EmbeddedPointHypothesis.lean) states the hypothesis in the source's two-clause shape and documents the counterexample.

theorem cycleAssociatedToFibres_rationallyEquivalent
    (Z : (projectiveLineProduct f).IdealSheafData)
    (hZ : ∀ ζ : Z.subscheme,
      relativeDimension C.dimensionFunction (familyBase f Z) ζ ≤ k + 1)
    (h₀ : schemeDeltaDimension C ((zeroFiber f Z).subschemeι ≫ f) ≤ (k : EInt))
    (hInf : schemeDeltaDimension C ((infinityFiber f Z).subschemeι ≫ f) ≤ (k : EInt))
    (hAssociated : ∀ ζ : Z.subscheme,
      ζ ∈ Stacks.Divisors.schemeAssociatedPoints Z.subscheme →
      ((Z.subschemeι ζ ∉ Set.range (zeroSection f) ∧
          Z.subschemeι ζ ∉ Set.range (infinitySection f)) ∨
        relativeDimension C.dimensionFunction (familyBase f Z) ζ < k)) :
    RationallyEquivalent C f k
      (cycleAssociatedToClosedSubscheme C f (zeroFiber f Z).subschemeι k)
      (cycleAssociatedToClosedSubscheme C f (infinityFiber f Z).subschemeι k)

Tag 02S6, a lemma

Tag 02S6 in the Stacks Project.

Stacks.Chow.cycleAssociatedToCoherentFibres_rationallyEquivalent_of_decompositionRule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FibreCycles/CoherentFibreComparison.lean, line 345. The attribute's comment: “all three hypotheses and the conclusion, with hypothesis (3) quantified over every associated point of F, as the source's own proof of this lemma uses it ('since ξ is not an associated point of F by assumption (3)'). The published statement of the tag quantifies (3) over the embedded associated points only; that reading is false, by the counterexample in the module documentation, so it is not what is registered here”.

Stacks Tag 02S6. For a coherent sheaf F on X ×_S 𝐏¹_S whose support has relative dimension at most k + 1, whose two fibres have delta-dimension at most k, and each of whose associated points either misses both distinguished sections or has relative dimension below k, the cycles [F₀]_k and [F_∞]_k of the two fibres are rationally equivalent.

The two inputs are Stacks.Chow.coherentFibreCycleDecompositionRule, the claim in the source's proof, and Stacks.Chow.familyFibreDifferencesRationallyEquivalentToZero, Tag 02S4 part (3).

theorem cycleAssociatedToCoherentFibres_rationallyEquivalent_of_decompositionRule
    [F.IsCoherent]
    (hSupp : ∀ ξ : projectiveLineProduct f, ξ ∈ SheafOfModules.supp F →
      relativeDimension C.dimensionFunction (productBase f) ξ ≤ k + 1)
    (h₀ : schemeDeltaDimension C ((reducedSupport (zeroFibreModule f F)).subschemeι ≫ f)
      ≤ (k : EInt))
    (hInf : schemeDeltaDimension C ((reducedSupport (infinityFibreModule f F)).subschemeι ≫ f)
      ≤ (k : EInt))
    (hAssociated : ∀ ξ : projectiveLineProduct f, ξ ∈ Stacks.Divisors.associatedPoints F →
      ((ξ ∉ Set.range (zeroSection f) ∧ ξ ∉ Set.range (infinitySection f)) ∨
        relativeDimension C.dimensionFunction (productBase f) ξ < k)) :
    RationallyEquivalent C f k
      (cycleAssociatedToCoherentSheaf C f (zeroFibreModule f F) k h₀)
      (cycleAssociatedToCoherentSheaf C f (infinityFibreModule f F) k hInf)

Stacks.Chow.rationallyEquivalent_cycleAssociatedToCoherentSheaf_fibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FibreCycles/CoherentFibreRationalEquivalence.lean, line 59.

Stacks 02S6. Let F be a coherent sheaf on X ×_S 𝐏¹_S with dim_δ(Supp(F)) ≤ k + 1, with dim_δ(Supp(F₀)) ≤ k and dim_δ(Supp(F_∞)) ≤ k, and such that every associated point ξ of F lies outside the union of the two distinguished sections or has δ(ξ) < k. Then [F₀]_k and [F_∞]_k are rationally equivalent k-cycles on X.

The coherence of F₀ and F_∞, needed to form their cycles, is Stacks 0EBF and is supplied in the statement rather than assumed.

theorem rationallyEquivalent_cycleAssociatedToCoherentSheaf_fibres
    (F : (projectiveLineProduct f).Modules) [F.IsCoherent]
    (hSupp : schemeDeltaDimension C ((reducedSupport F).subschemeι ≫ productBase f) ≤
      ((k + 1 : ℤ) : EInt))
    (h₀ : haveI := isCoherent_zeroFibreModule C f F
      schemeDeltaDimension C ((reducedSupport (zeroFibreModule f F)).subschemeι ≫ f) ≤
        (k : EInt))
    (hInf : haveI := isCoherent_infinityFibreModule C f F
      schemeDeltaDimension C ((reducedSupport (infinityFibreModule f F)).subschemeι ≫ f) ≤
        (k : EInt))
    (hAssociated : ∀ ξ ∈ Stacks.Divisors.associatedPoints F,
      ξ ∉ Set.range (zeroSection f) ∪ Set.range (infinitySection f) ∨
        relativeDimension C.dimensionFunction (productBase f) ξ < k) :
    haveI := isCoherent_zeroFibreModule C f F
    haveI := isCoherent_infinityFibreModule C f F
    RationallyEquivalent C f k
      (cycleAssociatedToCoherentSheaf C f (zeroFibreModule f F) k h₀)
      (cycleAssociatedToCoherentSheaf C f (infinityFibreModule f F) k hInf)

Sources

• Section 42.21, Tag 02S3
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.zeroDivisor_isEffectiveCartierDivisor · Stacks.Chow.infinityDivisor_isEffectiveCartierDivisor · Stacks.Chow.exists_familyFibreDifferences · Stacks.Chow.fibreCycles_rationallyEquivalent · Stacks.Chow.familyFibreDifferencesRationallyEquivalentToZero · Stacks.Chow.cycleAssociatedToFibres_rationallyEquivalent_of_isEmbeddedPoint · Stacks.Chow.cycleAssociatedToFibres_rationallyEquivalent · Stacks.Chow.cycleAssociatedToCoherentFibres_rationallyEquivalent_of_decompositionRule

Section42.22 Chow groups and envelopes#

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

Tag 0GU5, a definition

Tag 0GU5 in the Stacks Project.

AlgebraicGeometry.IsEnvelope, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChowGroupsEnvelopes/Basic.lean, line 43.

An envelope is a proper, completely decomposed morphism of schemes.

abbrev IsEnvelope {X Y : Scheme.{u}} (f : Y ⟶ X) : Prop

Tag 0GU6, a lemma

Tag 0GU6 in the Stacks Project.

AlgebraicGeometry.isEnvelope_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChowGroupsEnvelopes/Stability.lean, line 34.

The composite of two envelopes of schemes is an envelope.

lemma isEnvelope_comp {X Y Z : Scheme.{u}} (f : Y ⟶ X) (g : Z ⟶ Y)
    (hf : IsEnvelope f) (hg : IsEnvelope g) : IsEnvelope (g ≫ f)

Tag 0GU7, a lemma

Tag 0GU7 in the Stacks Project.

AlgebraicGeometry.isEnvelope_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChowGroupsEnvelopes/Stability.lean, line 51.

Envelopes of schemes are stable under arbitrary base change.

instance isEnvelope_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (fun {X Y : Scheme.{u}} (f : X ⟶ Y) ↦ IsEnvelope f)

Tag 0GU8, a lemma

Tag 0GU8 in the Stacks Project.

Stacks.Chow.envelope_chow_comp_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChowGroupsEnvelopes/ExactSequence.lean, line 254. The attribute's comment: “the composite of the two maps is zero”.

Pushing a class on Y ×_X Y forward along the two projections, taking the difference and pushing forward along f gives zero.

theorem envelope_chow_comp_eq_zero (γ : chowGroup C (pullback.fst f f ≫ f ≫ sX) k) :
    properChowPushforward C (f ≫ sX) sX f rfl k
        (properPushforwardFactorsThroughRationalEquivalence C (f ≫ sX) sX f rfl k)
        (properChowPushforward C (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.fst f f) rfl k
            (properPushforwardFactorsThroughRationalEquivalence C
              (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.fst f f) rfl k) γ -
          properChowPushforward C (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.snd f f)
            (pullback_snd_comp_eq_pullback_fst_comp f sX) k
            (properPushforwardFactorsThroughRationalEquivalence C
              (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.snd f f)
              (pullback_snd_comp_eq_pullback_fst_comp f sX) k) γ) = 0

Stacks.Chow.envelope_chow_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChowGroupsEnvelopes/ExactSequence.lean, line 273. The attribute's comment: “exactness at the middle term”.

For an envelope f : Y ⟶ X a class in A_k(Y) pushes forward to zero in A_k(X) exactly when it is the difference of the pushforwards of a single class in A_k(Y ×_X Y) along the two projections.

theorem envelope_chow_exact (hcd : IsCompletelyDecomposed f) (β : chowGroup C (f ≫ sX) k) :
    properChowPushforward C (f ≫ sX) sX f rfl k
        (properPushforwardFactorsThroughRationalEquivalence C (f ≫ sX) sX f rfl k) β = 0 ↔
      ∃ γ : chowGroup C (pullback.fst f f ≫ f ≫ sX) k,
        β = properChowPushforward C (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.fst f f) rfl k
              (properPushforwardFactorsThroughRationalEquivalence C
                (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.fst f f) rfl k) γ -
            properChowPushforward C (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.snd f f)
              (pullback_snd_comp_eq_pullback_fst_comp f sX) k
              (properPushforwardFactorsThroughRationalEquivalence C
                (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.snd f f)
                (pullback_snd_comp_eq_pullback_fst_comp f sX) k) γ

Stacks.Chow.envelope_chow_exactSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChowGroupsEnvelopes/ExactSequence.lean, line 314. The attribute's comment: “the exact sequence of Chow groups of an envelope”.

For an envelope f : Y ⟶ X with the two projections p, q : Y ×_X Y ⟶ Y of its fibre square, the sequence

A_k(Y ×_X Y) --(p_* - q_*)--> A_k(Y) --f_*--> A_k(X) ⟶ 0

is exact for every k ∈ ℤ: the composite of the two maps is zero, a class killed by f_* is a difference p_* γ - q_* γ, and f_* is surjective.

theorem envelope_chow_exactSequence (hcd : IsCompletelyDecomposed f) :
    (∀ γ : chowGroup C (pullback.fst f f ≫ f ≫ sX) k,
        properChowPushforward C (f ≫ sX) sX f rfl k
          (properPushforwardFactorsThroughRationalEquivalence C (f ≫ sX) sX f rfl k)
          (properChowPushforward C (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.fst f f) rfl k
              (properPushforwardFactorsThroughRationalEquivalence C
                (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.fst f f) rfl k) γ -
            properChowPushforward C (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.snd f f)
              (pullback_snd_comp_eq_pullback_fst_comp f sX) k
              (properPushforwardFactorsThroughRationalEquivalence C
                (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.snd f f)
                (pullback_snd_comp_eq_pullback_fst_comp f sX) k) γ) = 0) ∧
      (∀ β : chowGroup C (f ≫ sX) k,
        properChowPushforward C (f ≫ sX) sX f rfl k
            (properPushforwardFactorsThroughRationalEquivalence C (f ≫ sX) sX f rfl k) β = 0 ↔
          ∃ γ : chowGroup C (pullback.fst f f ≫ f ≫ sX) k,
            β = properChowPushforward C (pullback.fst f f ≫ f ≫ sX) (f ≫ sX)
                  (pullback.fst f f) rfl k
                  (properPushforwardFactorsThroughRationalEquivalence C
                    (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.fst f f) rfl k) γ -
                properChowPushforward C (pullback.fst f f ≫ f ≫ sX) (f ≫ sX)
                  (pullback.snd f f) (pullback_snd_comp_eq_pullback_fst_comp f sX) k
                  (properPushforwardFactorsThroughRationalEquivalence C
                    (pullback.fst f f ≫ f ≫ sX) (f ≫ sX) (pullback.snd f f)
                    (pullback_snd_comp_eq_pullback_fst_comp f sX) k) γ) ∧
      Function.Surjective (properChowPushforward C (f ≫ sX) sX f rfl k
        (properPushforwardFactorsThroughRationalEquivalence C (f ≫ sX) sX f rfl k))

Sources

• Section 42.22, Tag 0GU4
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.IsEnvelope · AlgebraicGeometry.isEnvelope_comp · AlgebraicGeometry.isEnvelope_isStableUnderBaseChange · Stacks.Chow.envelope_chow_comp_eq_zero · Stacks.Chow.envelope_chow_exact · Stacks.Chow.envelope_chow_exactSequence

Section42.23 Chow groups and K-groups#

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

Tag 02S8, a lemma

Tag 02S8 in the Stacks Project.

Stacks.Chow.coherentModulesDimLE_isSerreClass, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/CoherentSupportDimension.lean, line 166.

Stacks 02S8. Coherent 𝒪_X-modules whose support has delta-dimension at most k form a Serre subcategory of the category of coherent 𝒪_X-modules.

noncomputable instance coherentModulesDimLE_isSerreClass (C : ChowSituation.{u}) (f : X ⟶ C.S)
    [LocallyOfFiniteType f] (k : ℤ) : (coherentModulesDimLE C f k).IsSerreClass

Tag 02S9, a lemma

Tag 02S9 in the Stacks Project.

Stacks.Chow.dimensionLayerCycleHom_integralComponentLayerClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerClassOfCycle.lean, line 126. The attribute's comment: “the map Z_k(X) → K₀(Coh_{≤k}/Coh_{≤k-1}) on a prime cycle: the class of 𝒪_Z has cycle [Z]”.

The cycle class homomorphism sends the class of 𝒪_Z to the cycle [Z] of the integral closed subscheme Z attached to a point of relative dimension k.

theorem dimensionLayerCycleHom_integralComponentLayerClass (x : X)
    (hx : relativeDimension C.dimensionFunction f x = k) :
    dimensionLayerCycleHom C f k (integralComponentLayerClass C f k x) =
      cycleAssociatedToClosedSubscheme C f (integralComponentAt x).subschemeι k

Stacks.Chow.dimensionLayerCycleHom_finsum_integralComponentLayerClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerClassOfCycle.lean, line 164. The attribute's comment: “the inverse identity [∑ n_Z 𝒪_Z]_k = ∑ n_Z[Z], for a k-cycle of finite support”.

The cycle of the class ∑ n_Z[𝒪_Z] attached to a k-cycle ∑ n_Z[Z] of finite support is ∑ n_Z[Z] again.

theorem dimensionLayerCycleHom_finsum_integralComponentLayerClass (α : CycleGroup C f k)
    (hα : (Function.support (α.1 : X → ℤ)).Finite) :
    dimensionLayerCycleHom C f k
        (∑ᶠ x : X, α.1 x • integralComponentLayerClass C f k x) = α

Stacks.Chow.mem_range_dimensionLayerCycleHom_of_finite_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerClassOfCycle.lean, line 196. The attribute's comment: “every k-cycle of finite support is in the image of K₀(Coh_{≤k}/Coh_{≤k-1}) → Z_k(X)”.

Every k-cycle with finite support is the cycle of a class in the Grothendieck group of the dimension layer, namely of the weighted sum of the classes of the structure sheaves of the integral closed subschemes it is supported on.

theorem mem_range_dimensionLayerCycleHom_of_finite_support (α : CycleGroup C f k)
    (hα : (Function.support (α.1 : X → ℤ)).Finite) :
    α ∈ (dimensionLayerCycleHom C f k).range

Stacks.Chow.dimensionLayerClassHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerClassOfCycle.lean, line 225. The attribute's comment: “the map Z_k(X) → K₀(Coh_{≤k}/Coh_{≤k-1}), ∑ n_Z[Z] ↦ ∑ n_Z[𝒪_Z], for X quasi-compact”.

The map Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) for X quasi-compact: a k-cycle ∑ n_Z[Z] is sent to ∑ n_Z[𝒪_Z], the coefficients weighting the classes of the structure sheaves of the integral closed subschemes occurring in the cycle.

def dimensionLayerClassHom :
    CycleGroup C f k →+ GrothendieckGroup (coherentDimensionQuotient C f (k - 1) k)

Stacks.Chow.dimensionLayerCycleHom_comp_dimensionLayerClassHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerClassOfCycle.lean, line 246. The attribute's comment: “the inverse identity Z_k(X) → K₀(Coh_{≤k}/Coh_{≤k-1}) → Z_k(X) = id, for X quasi-compact”.

For X quasi-compact, the composite Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) → Z_k(X) is the identity.

theorem dimensionLayerCycleHom_comp_dimensionLayerClassHom :
    (dimensionLayerCycleHom C f k).comp (dimensionLayerClassHom C f k) = AddMonoidHom.id _

Stacks.Chow.surjective_dimensionLayerCycleHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerClassOfCycle.lean, line 255. The attribute's comment: “surjectivity of K₀(Coh_{≤k}/Coh_{≤k-1}) → Z_k(X), for X quasi-compact”.

For X quasi-compact, every k-cycle is the cycle of a class in the Grothendieck group of the dimension layer.

theorem surjective_dimensionLayerCycleHom :
    Function.Surjective (dimensionLayerCycleHom C f k)

Stacks.Chow.dimensionLayerCycleHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleClass.lean, line 219. The attribute's comment: “the map K₀(Coh_{≤k}/Coh_{≤k-1}) → Z_k(X), F ↦ [F]_k”.

Stacks 02S9, the map K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) → Z_k(X), F ↦ [F]_k. The cycle class of a coherent 𝒪_X-module of support dimension at most k is additive along short exact sequences and vanishes on support dimension at most k - 1, so it descends to the Grothendieck group of the dimension layer.

def dimensionLayerCycleHom :
    GrothendieckGroup (coherentDimensionQuotient C f (k - 1) k) →+ CycleGroup C f k

Stacks.Chow.dimensionLayerCycleHom_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleClass.lean, line 230. The attribute's comment: “the formula F ↦ [F]_k for the map out of K₀(Coh_{≤k}/Coh_{≤k-1})”.

Stacks 02S9. The homomorphism K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) → Z_k(X) sends the class of the image of a coherent 𝒪_X-module F of support dimension at most k to the cycle [F]_k.

theorem dimensionLayerCycleHom_of (F : CoherentModulesDimLE C f k) :
    dimensionLayerCycleHom C f k
        (GrothendieckGroup.of
          ((lowerDimensionClass C f (k - 1) k).isoModSerre.Q.obj F)) =
      dimensionLayerCycle C f k F

Stacks.Chow.cycleDimensionLayerHom_dimensionLayerCycleHom_mutuallyInverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleEquiv.lean, line 407. The attribute's comment: “the two maps, given by their formulas, are mutually inverse isomorphisms”.

Stacks 02S9. Let X be locally of finite type over (S, δ). The maps Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)), ∑ n_Z[Z] ↦ [⨁_{n_Z > 0} 𝒪_Z^{⊕n_Z}] - [⨁_{n_Z < 0} 𝒪_Z^{⊕-n_Z}], and K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) → Z_k(X), F ↦ [F]_k, are mutually inverse isomorphisms.

The first two conjuncts are the formulas defining the two maps (the direct sums are the locally finite direct sums of Stacks.Chow.cycleStructureSheafDimLE), the last two the two composites being the identity.

theorem cycleDimensionLayerHom_dimensionLayerCycleHom_mutuallyInverse :
    (∀ c : CycleGroup C f k, cycleDimensionLayerHom C f k c =
      GrothendieckGroup.of ((lowerDimensionClass C f (k - 1) k).isoModSerre.Q.obj
          (cycleStructureSheafDimLE C f k (cyclePositivePart C f k c))) -
        GrothendieckGroup.of ((lowerDimensionClass C f (k - 1) k).isoModSerre.Q.obj
          (cycleStructureSheafDimLE C f k (cycleNegativePart C f k c)))) ∧
    (∀ F : CoherentModulesDimLE C f k, dimensionLayerCycleHom C f k
        (GrothendieckGroup.of ((lowerDimensionClass C f (k - 1) k).isoModSerre.Q.obj F)) =
      dimensionLayerCycle C f k F) ∧
    (dimensionLayerCycleHom C f k).comp (cycleDimensionLayerHom C f k) = AddMonoidHom.id _ ∧
    (cycleDimensionLayerHom C f k).comp (dimensionLayerCycleHom C f k) = AddMonoidHom.id _

Stacks.Chow.cycleGroupAddEquivDimensionLayer, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleEquiv.lean, line 426. The attribute's comment: “Z_k(X) ≃ K₀(Coh_{≤k}/Coh_{≤k-1}) by the two maps of the lemma”.

Stacks 02S9, as an isomorphism: the group of k-cycles on X and the Grothendieck group of the dimension layer Coh_{≤k}(X)/Coh_{≤k-1}(X), identified by the two mutually inverse maps ∑ n_Z[Z] ↦ [⨁_{n_Z > 0} 𝒪_Z^{⊕n_Z}] - [⨁_{n_Z < 0} 𝒪_Z^{⊕-n_Z}] and F ↦ [F]_k.

def cycleGroupAddEquivDimensionLayer :
    CycleGroup C f k ≃+ GrothendieckGroup (coherentDimensionQuotient C f (k - 1) k)

Stacks.Chow.cycleDimensionLayerHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleFromCycles.lean, line 699. The attribute's comment: “the map Z_k(X) → K₀(Coh_{≤k}/Coh_{≤k-1})”.

Stacks 02S9, the map Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)). A k-cycle ∑ n_Z[Z] is sent to [⨁_{n_Z > 0} 𝒪_Z^{⊕n_Z}] - [⨁_{n_Z < 0} 𝒪_Z^{⊕-n_Z}], the two locally finite direct sums being coherent 𝒪_X-modules whose support has delta-dimension at most k.

def cycleDimensionLayerHom (C : ChowSituation.{u}) {X : Scheme.{u}} (f : X ⟶ C.S)
    [LocallyOfFiniteType f] (k : ℤ) :
    CycleGroup C f k →+ GrothendieckGroup (coherentDimensionQuotient C f (k - 1) k)

Stacks.Chow.cycleDimensionLayerHom_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleFromCycles.lean, line 708. The attribute's comment: “the formula ∑ n_Z[Z] ↦ [⨁_{n_Z > 0} 𝒪_Z^{⊕n_Z}] - [⨁_{n_Z < 0} 𝒪_Z^{⊕-n_Z}]”.

Stacks 02S9. The homomorphism Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) sends a k-cycle ∑ n_Z[Z] to the difference of the classes of the direct sums of the structure sheaves of the integral closed subschemes occurring with positive, respectively negative, coefficient.

theorem cycleDimensionLayerHom_apply (C : ChowSituation.{u}) {X : Scheme.{u}} (f : X ⟶ C.S)
    [LocallyOfFiniteType f] (k : ℤ) (c : CycleGroup C f k) :
    cycleDimensionLayerHom C f k c =
      GrothendieckGroup.of ((lowerDimensionClass C f (k - 1) k).isoModSerre.Q.obj
          (cycleStructureSheafDimLE C f k (cyclePositivePart C f k c))) -
        GrothendieckGroup.of ((lowerDimensionClass C f (k - 1) k).isoModSerre.Q.obj
          (cycleStructureSheafDimLE C f k (cycleNegativePart C f k c)))

Stacks.Chow.dimensionLayerCycleHom_comp_cycleDimensionLayerHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleFromCycles.lean, line 992. The attribute's comment: “the composite Z_k(X) → K₀(Coh_{≤k}/Coh_{≤k-1}) → Z_k(X) is the identity”.

Stacks 02S9, one of the two inverse identities: the composite Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) → Z_k(X) of the two maps of Tag 02S9 is the identity.

On a cycle ∑ n_Z[Z] the two locally finite direct sums have cycles ∑_{n_Z > 0} n_Z[Z] and ∑_{n_Z < 0} (-n_Z)[Z], whose difference is the cycle one started with.

theorem dimensionLayerCycleHom_comp_cycleDimensionLayerHom (C : ChowSituation.{u})
    {X : Scheme.{u}} (f : X ⟶ C.S) [LocallyOfFiniteType f] (k : ℤ) :
    (dimensionLayerCycleHom C f k).comp (cycleDimensionLayerHom C f k) = AddMonoidHom.id _

Stacks.Chow.dimensionLayerCycleHom_cycleDimensionLayerHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleFromCycles.lean, line 1011. The attribute's comment: “[⨁_{n_Z > 0} 𝒪_Z^{⊕n_Z}]_k - [⨁_{n_Z < 0} 𝒪_Z^{⊕-n_Z}]_k = ∑ n_Z[Z]”.

Stacks 02S9. The cycle class of the element of K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) attached to a k-cycle is that cycle.

theorem dimensionLayerCycleHom_cycleDimensionLayerHom (C : ChowSituation.{u}) {X : Scheme.{u}}
    (f : X ⟶ C.S) [LocallyOfFiniteType f] (k : ℤ) (c : CycleGroup C f k) :
    dimensionLayerCycleHom C f k (cycleDimensionLayerHom C f k c) = c

Stacks.Chow.injective_cycleDimensionLayerHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleFromCycles.lean, line 1021. The attribute's comment: “injectivity of Z_k(X) → K₀(Coh_{≤k}/Coh_{≤k-1})”.

Stacks 02S9, half of the bijectivity. The map Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) is injective, the cycle class homomorphism being a left inverse of it.

theorem injective_cycleDimensionLayerHom (C : ChowSituation.{u}) {X : Scheme.{u}} (f : X ⟶ C.S)
    [LocallyOfFiniteType f] (k : ℤ) : Function.Injective (cycleDimensionLayerHom C f k)

Stacks.Chow.surjective_dimensionLayerCycleHom_of_cycleDimensionLayerHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleFromCycles.lean, line 1039. The attribute's comment: “surjectivity of K₀(Coh_{≤k}/Coh_{≤k-1}) → Z_k(X), with no quasi-compactness”.

Stacks 02S9, half of the bijectivity. The cycle class homomorphism K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) → Z_k(X) is surjective: every k-cycle is the cycle class of the element attached to it.

The same conclusion is proved, for a quasi-compact X, as Stacks.Chow.surjective_dimensionLayerCycleHom in StacksFrontier.AlgebraicGeometry.Chow.Degrees.DimensionLayerClassOfCycle, through the rival construction of the map of Tag 02S9 recorded in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerCycleClass.lean. The version here needs no quasi-compactness, the section it uses being Stacks.Chow.cycleDimensionLayerHom, which is defined for every X locally of finite type over the base; hence the name, and hence no quasi-compactness in the attribute below.

theorem surjective_dimensionLayerCycleHom_of_cycleDimensionLayerHom (C : ChowSituation.{u})
    {X : Scheme.{u}} (f : X ⟶ C.S)
    [LocallyOfFiniteType f] (k : ℤ) : Function.Surjective (dimensionLayerCycleHom C f k)

Stacks.Chow.cycleDimensionLayerHom_dimensionLayerCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerStructureSheafClass.lean, line 890. The attribute's comment: “[F] = ∑ m_ξ[Z_ξ] in K₀(Coh_{≤k}/Coh_{≤k-1}), for X Noetherian”.

On a Noetherian scheme, the class of a coherent 𝒪_X-module F of support dimension at most k in K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) is the image of its cycle [F]_k under the map Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)).

theorem cycleDimensionLayerHom_dimensionLayerCycle [IsNoetherian X]
    (F : CoherentModulesDimLE C f k) :
    cycleDimensionLayerHom C f k (dimensionLayerCycle C f k F) =
      GrothendieckGroup.of ((lowerDimensionClass C f (k - 1) k).isoModSerre.Q.obj F)

Stacks.Chow.cycleDimensionLayerHom_comp_dimensionLayerCycleHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerStructureSheafClass.lean, line 901. The attribute's comment: “K₀(Coh_{≤k}/Coh_{≤k-1}) → Z_k(X) → K₀ is the identity, for X Noetherian”.

On a Noetherian scheme, the composite K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) → Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) of the cycle map and the cycle class map is the identity.

theorem cycleDimensionLayerHom_comp_dimensionLayerCycleHom [IsNoetherian X] :
    (cycleDimensionLayerHom C f k).comp (dimensionLayerCycleHom C f k) = AddMonoidHom.id _

Stacks.Chow.surjective_cycleDimensionLayerHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerStructureSheafClass.lean, line 908. The attribute's comment: “surjectivity of Z_k(X) → K₀(Coh_{≤k}/Coh_{≤k-1}), for X Noetherian”.

On a Noetherian scheme, the map Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) is surjective.

theorem surjective_cycleDimensionLayerHom [IsNoetherian X] :
    Function.Surjective (cycleDimensionLayerHom C f k)

Stacks.Chow.bijective_cycleDimensionLayerHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerStructureSheafClass.lean, line 916. The attribute's comment: “bijectivity of Z_k(X) → K₀(Coh_{≤k}/Coh_{≤k-1}), for X Noetherian”.

On a Noetherian scheme, the map Z_k(X) → K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) is bijective, the cycle class homomorphism being a two-sided inverse.

theorem bijective_cycleDimensionLayerHom [IsNoetherian X] :
    Function.Bijective (cycleDimensionLayerHom C f k)

Stacks.Chow.cycleDimensionLayerEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerStructureSheafClass.lean, line 925. The attribute's comment: “Z_k(X) ≃ K₀(Coh_{≤k}/Coh_{≤k-1}), for X Noetherian”.

On a Noetherian scheme X, the group of k-cycles on X is the Grothendieck group of the dimension layer Coh_{≤k}(X)/Coh_{≤k-1}(X), by the two mutually inverse homomorphisms ∑ n_Z[Z] ↦ [⨁_{n_Z > 0} 𝒪_Z^{⊕n_Z}] - [⨁_{n_Z < 0} 𝒪_Z^{⊕-n_Z}] and F ↦ [F]_k.

def cycleDimensionLayerEquiv [IsNoetherian X] :
    CycleGroup C f k ≃+ GrothendieckGroup (coherentDimensionQuotient C f (k - 1) k)

Stacks.Chow.cycleDimensionLayerEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerStructureSheafClass.lean, line 933. The attribute's comment: “the formula for Z_k(X) ≃ K₀(Coh_{≤k}/Coh_{≤k-1}), for X Noetherian”.

On a Noetherian scheme, the identification of the group of k-cycles with the Grothendieck group of the dimension layer sends a cycle ∑ n_Z[Z] to [⨁_{n_Z > 0} 𝒪_Z^{⊕n_Z}] - [⨁_{n_Z < 0} 𝒪_Z^{⊕-n_Z}].

theorem cycleDimensionLayerEquiv_apply [IsNoetherian X] (c : CycleGroup C f k) :
    cycleDimensionLayerEquiv C f k c = cycleDimensionLayerHom C f k c

Stacks.Chow.cycleDimensionLayerEquiv_symm_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerStructureSheafClass.lean, line 941. The attribute's comment: “the inverse formula for Z_k(X) ≃ K₀, for X Noetherian”.

On a Noetherian scheme, the inverse of the identification of the group of k-cycles with the Grothendieck group of the dimension layer sends the class of a coherent module F to the cycle [F]_k.

theorem cycleDimensionLayerEquiv_symm_apply [IsNoetherian X]
    (x : GrothendieckGroup (coherentDimensionQuotient C f (k - 1) k)) :
    (cycleDimensionLayerEquiv C f k).symm x = dimensionLayerCycleHom C f k x

Tag 0FDR, a lemma

Tag 0FDR in the Stacks Project.

Stacks.Chow.finitePushforwardCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 78. The attribute's comment: “the functor π_* : Coh(X) ⥤ Coh(Y)”.

Direct image along a finite morphism to a locally Noetherian scheme, as a functor on coherent modules.

def finitePushforwardCoherent :
    Stacks.SheafOfModules.CoherentModules X.ringCatSheaf ⥤
      Stacks.SheafOfModules.CoherentModules Y.ringCatSheaf

Stacks.Chow.shortExact_map_finitePushforwardCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 155. The attribute's comment: “π_* is an exact functor on coherent sheaves”.

Direct image along a finite morphism carries a short exact sequence of coherent modules to a short exact sequence.

theorem shortExact_map_finitePushforwardCoherent
    ⦃S : ShortComplex (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)⦄
    (hS : S.ShortExact) : (S.map (finitePushforwardCoherent π)).ShortExact

Stacks.Chow.finitePushforwardCoherentHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 163. The attribute's comment: “the induced homomorphism K₀(Coh(X)) → K₀(Coh(Y))”.

The homomorphism K₀(Coh(X)) → K₀(Coh(Y)) induced by direct image along a finite morphism.

def finitePushforwardCoherentHom :
    GrothendieckGroup (Stacks.SheafOfModules.CoherentModules X.ringCatSheaf) →+
      GrothendieckGroup (Stacks.SheafOfModules.CoherentModules Y.ringCatSheaf)

Stacks.Chow.coherentModulesDimLE_finitePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 184. The attribute's comment: “π_* sends Coh_{≤k}(X) into Coh_{≤k}(Y)”.

The direct image along a finite morphism of a coherent module whose support has delta-dimension at most k again has support of delta-dimension at most k.

theorem coherentModulesDimLE_finitePushforward (C : ChowSituation.{u}) (sX : X ⟶ C.S)
    [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (π : X ⟶ Y) [IsFinite π]
    (hπ : π ≫ sY = sX) (k : ℤ)
    (F : Stacks.SheafOfModules.CoherentModules X.ringCatSheaf)
    (hF : coherentModulesDimLE C sX k F) :
    have : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
    coherentModulesDimLE C sY k ((finitePushforwardCoherent π).obj F)

Stacks.Chow.finitePushforwardDimLE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 201. The attribute's comment: “the functor π_* : Coh_{≤k}(X) ⥤ Coh_{≤k}(Y)”.

The restriction of π_* to the coherent modules whose support has delta-dimension at most k.

def finitePushforwardDimLE (C : ChowSituation.{u}) (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (π : X ⟶ Y) [IsFinite π] (hπ : π ≫ sY = sX)
    (k : ℤ) : CoherentModulesDimLE C sX k ⥤ CoherentModulesDimLE C sY k

Stacks.Chow.shortExact_map_finitePushforwardDimLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 250. The attribute's comment: “π_* is exact on Coh_{≤k}”.

Direct image along a finite morphism carries a short exact sequence of coherent modules of support dimension at most k to a short exact sequence.

theorem shortExact_map_finitePushforwardDimLE (C : ChowSituation.{u}) (sX : X ⟶ C.S)
    [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (π : X ⟶ Y) [IsFinite π]
    (hπ : π ≫ sY = sX) (k : ℤ) ⦃S : ShortComplex (CoherentModulesDimLE C sX k)⦄
    (hS : S.ShortExact) : (S.map (finitePushforwardDimLE C sX sY π hπ k)).ShortExact

Stacks.Chow.finitePushforwardDimLEHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 259. The attribute's comment: “the induced homomorphism K₀(Coh_{≤k}(X)) → K₀(Coh_{≤k}(Y))”.

The homomorphism K₀(Coh_{≤k}(X)) → K₀(Coh_{≤k}(Y)) induced by direct image along a finite morphism.

def finitePushforwardDimLEHom (C : ChowSituation.{u}) (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (π : X ⟶ Y) [IsFinite π] (hπ : π ≫ sY = sX)
    (k : ℤ) :
    GrothendieckGroup (CoherentModulesDimLE C sX k) →+
      GrothendieckGroup (CoherentModulesDimLE C sY k)

Stacks.Chow.dimensionLayerFinitePushforwardHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 309. The attribute's comment: “the induced homomorphism K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) → K₀(Coh_{≤k}(Y)/Coh_{≤k-1}(Y))”.

The homomorphism K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) → K₀(Coh_{≤k}(Y)/Coh_{≤k-1}(Y)) induced by direct image along a finite morphism.

def dimensionLayerFinitePushforwardHom (C : ChowSituation.{u}) (sX : X ⟶ C.S)
    [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (π : X ⟶ Y) [IsFinite π]
    (hπ : π ≫ sY = sX) (k : ℤ) :
    GrothendieckGroup (coherentDimensionQuotient C sX (k - 1) k) →+
      GrothendieckGroup (coherentDimensionQuotient C sY (k - 1) k)

Stacks.Chow.dimensionLayerFinitePushforwardHom_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 322. The attribute's comment: “the induced homomorphism on a layer sends [F] to [π_* F]”.

The homomorphism on the Grothendieck groups of the layers sends the class of the image of a module F of Coh_{≤k}(X) to the class of the image of π_* F.

theorem dimensionLayerFinitePushforwardHom_of (C : ChowSituation.{u}) (sX : X ⟶ C.S)
    [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (π : X ⟶ Y) [IsFinite π]
    (hπ : π ≫ sY = sX) (k : ℤ) (F : CoherentModulesDimLE C sX k) :
    dimensionLayerFinitePushforwardHom C sX sY π hπ k
        (GrothendieckGroup.of ((lowerDimensionClass C sX (k - 1) k).isoModSerre.Q.obj F)) =
      GrothendieckGroup.of ((lowerDimensionClass C sY (k - 1) k).isoModSerre.Q.obj
        ((finitePushforwardDimLE C sX sY π hπ k).obj F))

Stacks.Chow.properPushforwardHom_comp_dimensionLayerCycleHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 342. The attribute's comment: “commutativity of the right-hand square of the diagram”.

The cycle class homomorphism K₀(Coh_{≤k}/Coh_{≤k-1}) ⟶ Z_k commutes with direct image along a finite morphism on the source and proper pushforward of k-cycles on the target.

theorem properPushforwardHom_comp_dimensionLayerCycleHom (C : ChowSituation.{u}) (sX : X ⟶ C.S)
    [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (π : X ⟶ Y) [IsFinite π]
    (hπ : π ≫ sY = sX) (k : ℤ) :
    (properPushforwardHom C sX sY π hπ k).comp (dimensionLayerCycleHom C sX k) =
      (dimensionLayerCycleHom C sY k).comp
        (dimensionLayerFinitePushforwardHom C sX sY π hπ k)

Stacks.Chow.dimensionLayerFinitePushforwardHom_comp_cycleDimensionLayerHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 367. The attribute's comment: “commutativity of the left-hand square of the diagram, for Y Noetherian”.

For Y Noetherian, the homomorphism Z_k ⟶ K₀(Coh_{≤k}/Coh_{≤k-1}) commutes with proper pushforward of k-cycles on the source and direct image along the finite morphism π on the target.

theorem dimensionLayerFinitePushforwardHom_comp_cycleDimensionLayerHom (C : ChowSituation.{u})
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (π : X ⟶ Y) [IsFinite π] [IsNoetherian Y] (hπ : π ≫ sY = sX) (k : ℤ) :
    (dimensionLayerFinitePushforwardHom C sX sY π hπ k).comp (cycleDimensionLayerHom C sX k) =
      (cycleDimensionLayerHom C sY k).comp (properPushforwardHom C sX sY π hπ k)

Stacks.Chow.dimensionLayerFinitePushforwardHom_cycleDimensionLayerHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforward.lean, line 385. The attribute's comment: “the left-hand square of the diagram on a cycle, for Y Noetherian”.

For Y Noetherian, the element of the Grothendieck group of the layer over Y attached to the proper pushforward of a k-cycle c on X is the direct image along π of the element attached to c.

theorem dimensionLayerFinitePushforwardHom_cycleDimensionLayerHom (C : ChowSituation.{u})
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (π : X ⟶ Y) [IsFinite π] [IsNoetherian Y] (hπ : π ≫ sY = sX) (k : ℤ)
    (c : CycleGroup C sX k) :
    dimensionLayerFinitePushforwardHom C sX sY π hπ k (cycleDimensionLayerHom C sX k c) =
      cycleDimensionLayerHom C sY k (properPushforwardHom C sX sY π hπ k c)

Stacks.Chow.cycleDimensionLayerHom_comp_properPushforwardHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforwardSquare.lean, line 68. The attribute's comment: “commutativity of the left-hand square of the diagram”.

Stacks 0FDR, the left-hand square of the diagram. The homomorphism Z_k ⟶ K₀(Coh_{≤k}/Coh_{≤k-1}) of Stacks 02S9 commutes with proper pushforward of k-cycles on the source and direct image along the finite morphism π on the target.

As in the source, it follows from the right-hand square Stacks.Chow.properPushforwardHom_comp_dimensionLayerCycleHom because the two maps of Tag 02S9 are mutually inverse, over X and over Y, each being merely locally of finite type over the base.

theorem cycleDimensionLayerHom_comp_properPushforwardHom :
    (cycleDimensionLayerHom C sY k).comp (properPushforwardHom C sX sY π hπ k) =
      (dimensionLayerFinitePushforwardHom C sX sY π hπ k).comp
        (cycleDimensionLayerHom C sX k)

Stacks.Chow.cycleDimensionLayerHom_properPushforwardHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforwardSquare.lean, line 85. The attribute's comment: “the left-hand square of the diagram on a cycle”.

Stacks 0FDR, the left-hand square read on a cycle. The element of the Grothendieck group of the layer over Y attached to the proper pushforward of a k-cycle c on X is the direct image along π of the element attached to c.

theorem cycleDimensionLayerHom_properPushforwardHom (c : CycleGroup C sX k) :
    cycleDimensionLayerHom C sY k (properPushforwardHom C sX sY π hπ k c) =
      dimensionLayerFinitePushforwardHom C sX sY π hπ k (cycleDimensionLayerHom C sX k c)

Stacks.Chow.finitePushforward_dimensionLayer_diagram_commutes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DimensionLayerFinitePushforwardSquare.lean, line 95. The attribute's comment: “the maps of Tag 02S9 fit into a commutative diagram with π_*”.

Stacks 0FDR, the diagram. The maps of Stacks 02S9, Z_k ⟶ K₀(Coh_{≤k}/Coh_{≤k-1}) ⟶ Z_k, over X and over Y, together with proper pushforward of k-cycles on the two outer columns and direct image along π on the middle column, form a commutative diagram: both the left-hand and the right-hand square commute.

theorem finitePushforward_dimensionLayer_diagram_commutes :
    (cycleDimensionLayerHom C sY k).comp (properPushforwardHom C sX sY π hπ k) =
        (dimensionLayerFinitePushforwardHom C sX sY π hπ k).comp
          (cycleDimensionLayerHom C sX k) ∧
      (properPushforwardHom C sX sY π hπ k).comp (dimensionLayerCycleHom C sX k) =
        (dimensionLayerCycleHom C sY k).comp
          (dimensionLayerFinitePushforwardHom C sX sY π hπ k)

Tag 0FDS, a lemma

Tag 0FDS in the Stacks Project.

Stacks.Chow.chowToWideDimensionLayerHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/ChowToWideLayer.lean, line 97. The attribute's comment: “for a quasi-compact X; the cycle identity is formalized in the orientation [𝒪_X/fI]_k − [𝒪_X/I]_k = div(f), correcting the sign-inverted chain of the source”.

For a quasi-compact scheme X locally of finite type over the base scheme of a Chow situation there is a canonical homomorphism CH_k(X) ⟶ K₀(Coh_{≤k+1}(X)/Coh_{≤k-1}(X)) sending the class of a k-cycle ∑ n_Z[Z] to the class of [⨁_{n_Z > 0} 𝒪_Z^{⊕n_Z}] − [⨁_{n_Z < 0} 𝒪_Z^{⊕-n_Z}] in the wide dimension layer.

def chowToWideDimensionLayerHom (C : ChowSituation.{u}) {X : Scheme.{u}} (sX : X ⟶ C.S)
    [LocallyOfFiniteType sX] [CompactSpace X] (k : ℤ) :
    chowGroup C sX k →+ coherentDimensionKZero C sX (k - 1) (k + 1)

Stacks.Chow.chowToWideLayerHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/ChowToWideLayerGeneral.lean, line 386.

Stacks 0FDS. For a scheme X locally of finite type over the base of a Chow situation there is a canonical homomorphism CH_k(X) ⟶ K₀(Coh_{≤k+1}(X)/Coh_{≤k-1}(X)) induced by the map Z_k(X) ⟶ K₀(Coh_{≤k}(X)/Coh_{≤k-1}(X)) of Tag 02S9: it sends the class of a k-cycle c to the image of the class of c under the map widening the layer, see Stacks.Chow.chowToWideLayerHom_mk.

def chowToWideLayerHom (C : ChowSituation.{u}) (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (k : ℤ) : chowGroup C sX k →+ coherentDimensionKZero C sX (k - 1) (k + 1)

Tag 02SD, a remark

Tag 02SD in the Stacks Project.

Stacks.Chow.chowToCoherentQuotientHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/ChowToCoherentQuotient.lean, line 71. The attribute's comment: “the canonical map CH_k(X) → K₀(Coh(X)/Coh_{≤k-1}(X)), built from Lemma 0FDS”.

Stacks 02SD, the canonical map CH_k(X) → K₀(Coh(X)/Coh_{≤k-1}(X)) for X locally of finite type over the base of a Chow situation: the canonical map CH_k(X) → K₀(Coh_{≤k+1}(X)/Coh_{≤k-1}(X)) of Lemma 0FDS (Stacks.Chow.chowToWideLayerHom) followed by the canonical map K₀(Coh_{≤k+1}(X)/Coh_{≤k-1}(X)) → K₀(Coh(X)/Coh_{≤k-1}(X)) (Stacks.Chow.coherentDimensionToQuotientHom).

def chowToCoherentQuotientHom (C : ChowSituation.{u}) (f : X ⟶ C.S) [LocallyOfFiniteType f]
    (k : ℤ) : chowGroup C f k →+ coherentQuotientKZero C f (k - 1)

Stacks.Chow.coherentDimensionToQuotientHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/CoherentQuotientKGroup.lean, line 156. The attribute's comment: “the canonical map K₀(Coh_{≤b}/Coh_{≤a}) → K₀(Coh/Coh_{≤a})”.

The canonical map K₀(Coh_{≤b}(X)/Coh_{≤a}(X)) → K₀(Coh(X)/Coh_{≤a}(X)): the homomorphism of Grothendieck groups induced by the exact functor that drops the upper dimension bound.

def coherentDimensionToQuotientHom (C : ChowSituation.{u}) (f : X ⟶ C.S)
    [LocallyOfFiniteType f] (a b : ℤ) :
    coherentDimensionKZero C f a b →+ coherentQuotientKZero C f a

Stacks.Chow.chowToCoherentQuotientKZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/CoherentQuotientKGroup.lean, line 177. The attribute's comment: “the canonical map CH_k(X) → K₀(Coh/Coh_{≤k-1})”.

The canonical map CH_k(X) → K₀(Coh(X)/Coh_{≤k-1}(X)): the composite of a cycle class map φ : CH_k(X) → K₀(Coh_{≤k+1}(X)/Coh_{≤k-1}(X)) with the canonical map that drops the upper dimension bound.

def chowToCoherentQuotientKZero (C : ChowSituation.{u}) (f : X ⟶ C.S) [LocallyOfFiniteType f]
    (k : ℤ) (φ : chowGroup C f k →+ coherentDimensionKZero C f (k - 1) (k + 1)) :
    chowGroup C f k →+ coherentQuotientKZero C f (k - 1)

Tag 0FDT, a lemma

Tag 0FDT in the Stacks Project.

AlgebraicGeometry.coherentToSupportedCoherentKZeroHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedCoherentKGroup.lean, line 193. The attribute's comment: “the exact fully faithful inclusion functor Coh(Z) → Coh_Z(X) and the homomorphism K'_0(Z) = K_0(Coh(Z)) → K_0(Coh_Z(X)) that it induces. That this homomorphism is an isomorphism is NOT covered: the source inverts it by sending a coherent module F supported on Z to the class of the graded module of its I-adic filtration. The graded pieces of that filtration are available, as the short exact sequence with the coherence and support bound of Stacks.AlgebraicGeometry.IdealAdicFiltration; what is missing is a comparison between the support and coherence predicates used there and those defining SupportedCoherentModules, and the local finiteness of the filtration over a merely locally Noetherian scheme, the available finiteness input being quasi-compact”.

[Stacks, Tag 0FDT], the comparison homomorphism of K-groups. Let X be a locally Noetherian scheme and Z ⊂ X a closed subscheme. The exact inclusion functor Coh(𝒪_Z) ⥤ Coh_Z(X) induces a homomorphism K'_0(Z) = K_0(Coh(𝒪_Z)) → K_0(Coh_Z(X)) taking the class of a coherent 𝒪_Z-module to the class of its direct image.

def coherentToSupportedCoherentKZeroHom :
    KZero (Stacks.SheafOfModules.CoherentModules Z.ringCatSheaf) →+
      KZero (SupportedCoherentModules i)

AlgebraicGeometry.coherentToSupportedCoherentKZeroHom_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedCoherentKGroup.lean, line 202. The attribute's comment: “the defining property of the comparison homomorphism”.

[Stacks, Tag 0FDT]. The comparison homomorphism K_0(Coh(𝒪_Z)) → K_0(Coh_Z(X)) takes the class of a coherent 𝒪_Z-module ℱ to the class of its direct image i_*ℱ.

theorem coherentToSupportedCoherentKZeroHom_mk
    (F : Stacks.SheafOfModules.CoherentModules Z.ringCatSheaf) :
    coherentToSupportedCoherentKZeroHom i (KZero.mk _ F) =
      KZero.mk _ ((coherentToSupportedCoherent i).obj F)

AlgebraicGeometry.coherentToSupportedCoherentKZeroHom_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedCoherentKGroupIso/KZeroIso.lean, line 577. The attribute's comment: “the homomorphism K'_0(Z) = K_0(Coh(Z)) → K_0(Coh_Z(X)) induced by the exact inclusion functor is an isomorphism”.

[Stacks, Tag 0FDT]. Let X be a locally Noetherian scheme and Z ⊂ X a closed subscheme. The homomorphism K'_0(Z) = K_0(Coh(𝒪_Z)) → K_0(Coh_Z(X)) induced by the exact inclusion functor Coh(𝒪_Z) ⥤ Coh_Z(X) is an isomorphism.

theorem coherentToSupportedCoherentKZeroHom_bijective :
    Function.Bijective (coherentToSupportedCoherentKZeroHom i)

Sources

• Section 42.23, Tag 0FDQ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.coherentModulesDimLE_isSerreClass · Stacks.Chow.dimensionLayerCycleHom_integralComponentLayerClass · Stacks.Chow.dimensionLayerCycleHom_finsum_integralComponentLayerClass · Stacks.Chow.mem_range_dimensionLayerCycleHom_of_finite_support · Stacks.Chow.dimensionLayerClassHom · Stacks.Chow.dimensionLayerCycleHom_comp_dimensionLayerClassHom · Stacks.Chow.surjective_dimensionLayerCycleHom · Stacks.Chow.dimensionLayerCycleHom

Section42.24 The divisor associated to an invertible sheaf#

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

Tag 02SJ, a definition

Tag 02SJ in the Stacks Project.

Stacks.Chow.firstChernClassCapFundamental, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DivisorOfInvertibleSheaf.lean, line 90. The attribute's comment: “part (2): the Weil divisor class c₁(L) ∩ [X] in CH_{n-1}(X)”. References: SGA 5 VII (3.9), “partial”.

The Weil divisor class of an invertible module, Stacks 02SJ (2). On an integral scheme X of delta-dimension n, locally of finite type over the base of a Chow situation, the class

c₁(L) ∩ [X] ∈ CH_{n-1}(X)

of the divisor of zeros and poles of a nonzero meromorphic section of L.

An invertible module on an integral scheme has a regular meromorphic section with nonzero generic value (Stacks.ChernCap42.exists_isRegularMeromorphicSection_of_isIntegral), and the class of its divisor cycle does not depend on which one is taken; the characterizing equality is Stacks.Chow.firstChernClassCapFundamental_eq, which should be used in place of this definition.

def firstChernClassCapFundamental : chowGroup C p (n - 1)

Stacks.Chow.firstChernClassCapFundamental_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DivisorOfInvertibleSheaf.lean, line 106. The attribute's comment: “part (2): c₁(L) ∩ [X] is the class of div_L(s) for every nonzero regular meromorphic section s, so the definition does not depend on the chosen section”.

The Weil divisor class is the class of div_L(s) for every nonzero section, Stacks 02SJ (2). In CH_{n-1}(X) the class c₁(L) ∩ [X] is represented by the divisor cycle of any nonzero regular meromorphic section of L, not only by the one Stacks.Chow.firstChernClassCapFundamental chose. This is the well-definedness the source asserts.

The source's nonvanishing of s is not assumed: on an integral scheme it follows from regularity, by Stacks.Divisors.genericValue_ne_zero_of_isRegularMeromorphicSection. See the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.DivisorOfInvertibleSheaf.

theorem firstChernClassCapFundamental_eq
    (s : AlgebraicGeometry.MeromorphicSection X.sheaf L)
    (hs : AlgebraicGeometry.IsRegularMeromorphicSection X.sheaf L s) :
    firstChernClassCapFundamental C p n hn L =
      QuotientAddGroup.mk (divisorOfMeromorphicSectionCycle C p n hn L s hs)

Stacks.Chow.divisorOfMeromorphicSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/MeromorphicCascade/DivisorCycle.lean, line 88. The attribute's comment: “part (1): div_L(s) = ∑_Z ord_{Z, L}(s) [Z] as an element of Z_{n-1}(X), together with its coefficients”.

The divisor cycle of a regular meromorphic section, Stacks 02SJ (1). The Weil divisor div_L(s) of a regular meromorphic section of an invertible module on an integral scheme of delta-dimension n, read as a cycle of delta-dimension n - 1, together with its coefficient specification.

The coefficient at the generic point of a prime divisor Z is the order of vanishing ord_{Z, L}(s) of Stacks 02SF, and the coefficient at a point which is no prime divisor's generic point is zero; those are the two components of the subtype obligation, and they are available as Stacks.Chow.divisorOfMeromorphicSectionCycle_genericPoint and Stacks.Chow.divisorOfMeromorphicSectionCycle_eq_zero.

def divisorOfMeromorphicSection (C : ChowSituation.{u}) {X : Scheme.{u}} (p : X ⟶ C.S)
    [LocallyOfFiniteType p] [IsIntegral X] (n : ℤ)
    (hn : schemeDeltaDimension C p = (n : EInt)) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : AlgebraicGeometry.MeromorphicSection X.sheaf L)
    (hs : AlgebraicGeometry.IsRegularMeromorphicSection X.sheaf L s) :
    { c : CycleGroup C p (n - 1) // IsDivisorOfMeromorphicSectionCycle C p n L s hs c }

Tag 02SK, a lemma

Tag 02SK in the Stacks Project.

Stacks.ChernCap42.divisorOfMeromorphicSectionCycle_eq_cycleAssociatedToZeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCap42/DivisorOfSectionCycle.lean, line 279. The attribute's comment: “divisor cycle”.

Let X be an integral scheme locally of finite type over the base of chapter 42, of delta-dimension n, let L be an invertible 𝒪_X-module and let s be a nonzero global section of L. Then the divisor of s is the cycle of its zero scheme: div_L(s) = [Z(s)]_{n-1} in Z_{n-1}(X).

theorem divisorOfMeromorphicSectionCycle_eq_cycleAssociatedToZeroScheme (C : ChowSituation.{u})
    (p : X ⟶ C.S) [LocallyOfFiniteType p] [IsIntegral X] (n : ℤ)
    (hn : schemeDeltaDimension C p = (n : EInt)) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) (hs : s ≠ 0) :
    divisorOfMeromorphicSectionCycle C p n hn L (meromorphicSectionOfSection L s)
        (isRegularMeromorphicSection_of_ne_zero X L s hs) =
      cycleAssociatedToClosedSubscheme C p
        (Stacks.Divisors.zeroScheme X L s).subschemeι (n - 1)

Stacks.ChernCap42.firstChernClassCapOfInvertible_fundamentalCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCap42/DivisorOfSectionCycle.lean, line 405. The attribute's comment: “first Chern class”.

Let X be an integral scheme locally of finite type over the base of chapter 42, of delta-dimension n, let L be an invertible 𝒪_X-module and let s be a nonzero global section of L. Then the first Chern class of L capped with the fundamental cycle [X] of X, in degree n - 1 + 1, is the class of the cycle of the zero scheme of s: c₁(L) ∩ [X] = [Z(s)]_{n-1} in CH_{n-1}(X).

theorem firstChernClassCapOfInvertible_fundamentalCycle (C : ChowSituation.{u}) (p : X ⟶ C.S)
    [LocallyOfFiniteType p] [IsIntegral X] (n : ℤ)
    (hn : schemeDeltaDimension C p = (n : EInt)) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) (hs : s ≠ 0) :
    firstChernClassCapOfInvertible C p (n - 1) L
        (cycleAssociatedToClosedSubscheme C p (𝟙 X) (n - 1 + 1)) =
      QuotientAddGroup.mk (cycleAssociatedToClosedSubscheme C p
        (Stacks.Divisors.zeroScheme X L s).subschemeι (n - 1))

Tag 02SM, a lemma

Tag 02SM in the Stacks Project.

Stacks.Chow.mk_flatPullback_meromorphicDivisorCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/FlatPullbackMeromorphicDivisorIntegral.lean, line 143. The attribute's comment: “the flat pullback read on the divisor of a nonzero meromorphic section”.

Stacks 02SM. Let C = (S, δ) be the base situation of chapter 42, let X and Y be integral and locally of finite type over S with n = dim_δ(Y), and let f : X ⟶ Y be flat of relative dimension r. For an invertible module L on Y,

f^*(c₁(L) ∩ [Y]) = c₁(f^*L) ∩ [X]

in A_{n + r - 1}(X), where either side is the class of the divisor of a nonzero meromorphic section, read on Y and pulled back on the left and read on X on the right.

theorem mk_flatPullback_meromorphicDivisorCycle (hs : s ≠ 0) :
    (QuotientAddGroup.mk ((show (n : ℤ) - 1 + (r : ℤ) = n + (r : ℤ) - 1 by ring) ▸
          flatPullback C sX sY f hbase r hf (n - 1)
            (meromorphicDivisorCycleOfInvertible C sY hY L s).val) :
        chowGroup C sX (n + (r : ℤ) - 1)) =
      QuotientAddGroup.mk (meromorphicDivisorCycleOfInvertible C sX
        (schemeDeltaDimension_eq_add_of_flat C sX sY f hbase r hf hY)
        ((Scheme.Modules.pullback f).obj L) (genericStalkPullback f L s)).val

Sources

• Section 42.24, Tag 02SI
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.firstChernClassCapFundamental · Stacks.Chow.firstChernClassCapFundamental_eq · Stacks.Chow.divisorOfMeromorphicSection · Stacks.ChernCap42.divisorOfMeromorphicSectionCycle_eq_cycleAssociatedToZeroScheme · Stacks.ChernCap42.firstChernClassCapOfInvertible_fundamentalCycle · Stacks.Chow.mk_flatPullback_meromorphicDivisorCycle

Section42.25 Intersecting with an invertible sheaf#

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

Tag 02SO, a definition

Tag 02SO in the Stacks Project.

Stacks.Chow.firstChernClassCapOfInvertible, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernComponent/ClassRule.lean, line 103.

The first Chern class cap product Z_{k+1}(X) ⟶ A_k(X), α ↦ c₁(L) ∩ α, of an invertible module: Stacks.Chow.firstChernClassCap at the component rule of L.

abbrev firstChernClassCapOfInvertible : CycleGroup C p (k + 1) →+ chowGroup C p k

Stacks.Chow.firstChernClassCapOfInvertible_integral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InvertibleChernSpecialization.lean, line 110. The attribute's comment: “integral component formula”.

On the fundamental cycle of a single integral closed subscheme W ⊆ X of delta-dimension k + 1, the cap product of an invertible module is the proper Chow pushforward along W ⟶ X of the first Chern class of L|_W.

This is Stacks.Chow.firstChernClassCapOfInvertible_integral_cycle read through Stacks.Chow.properChowPushforward_mk. The instance of Stacks 02S2 that Stacks.Chow.properChowPushforward requires is discharged, W.subschemeι being a closed immersion.

theorem firstChernClassCapOfInvertible_integral (W : X.IdealSheafData)
    (hW : IsIntegral W.subscheme)
    (hDim : schemeDeltaDimension C (W.subschemeι ≫ p) = ((k + 1 : ℤ) : EInt)) :
    firstChernClassCapOfInvertible C p k L
        (cycleAssociatedToClosedSubscheme C p W.subschemeι (k + 1)) =
      properChowPushforward C (W.subschemeι ≫ p) p W.subschemeι rfl k
        (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion W.subschemeι C
          (W.subschemeι ≫ p) p rfl k)
        (firstChernComponentClass C p k L W hW hDim)

Stacks.Chow.firstChernClassCapOfInvertible_finsum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InvertibleChernSpecialization.lean, line 125. The attribute's comment: “locally finite component formula”.

The locally finite component formula for the cap product of an invertible module: on a presentation α = ∑ n_j [W_j] of a (k+1)-cycle, c₁(L) ∩ α is the class of ∑ n_j c₁(L) ∩ [W_j].

theorem firstChernClassCapOfInvertible_finsum {J : Type u} (W : J → X.IdealSheafData)
    (hW : ∀ j, IsIntegral (W j).subscheme)
    (hDim : ∀ j, schemeDeltaDimension C ((W j).subschemeι ≫ p) = ((k + 1 : ℤ) : EInt))
    (hLocal : LocallyFinite fun j ↦ ((W j).support : Set X)) (n : J → ℤ)
    (α : CycleGroup C p (k + 1))
    (hα : ∀ x : X, α.1 x = ∑ᶠ j : J, n j *
      (cycleAssociatedToClosedSubscheme C p (W j).subschemeι (k + 1)).1 x) :
    ∃ β : CycleGroup C p k,
      firstChernClassCapOfInvertible C p k L α = QuotientAddGroup.mk β ∧
      ∀ x : X, β.1 x = ∑ᶠ j : J, n j *
        (firstChernComponentCycle C p k (firstChernComponentCycleRule C p k L)
          (W j) (hW j) (hDim j)).1 x

Tag 02SP, a lemma

Tag 02SP in the Stacks Project.

Stacks.Chow.firstChernClassCapOfInvertible_tensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FirstChernClassTensor.lean, line 498. The attribute's comment: “additivity in the invertible module”.

Stacks 02SP. Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S and let L, N be invertible 𝒪_X-modules. Then

c₁(L) ∩ α + c₁(N) ∩ α = c₁(L ⊗_{𝒪_X} N) ∩ α

in A_k(X) for every α ∈ Z_{k+1}(X). The companion assertion of the same tag, c₁(𝒪_X) ∩ α = 0, is Stacks.Chow.firstChernClassCapOfInvertible_unit, deduced from this one through 𝒪_X ⊗_{𝒪_X} 𝒪_X ≅ 𝒪_X.

The cap product is the one of StacksFrontier.AlgebraicGeometry.Chow.ChernComponent.ClassRule; see the module documentation for why no @[stacks 02SO] attribute accompanies it.

theorem firstChernClassCapOfInvertible_tensorObj (α : CycleGroup C p (k + 1)) :
    firstChernClassCapOfInvertible C p k L α + firstChernClassCapOfInvertible C p k N α =
      firstChernClassCapOfInvertible C p k (Scheme.Modules.tensorObj L N) α

Stacks.Chow.firstChernClassCapOfInvertible_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FirstChernClassTensor.lean, line 515. The attribute's comment: “vanishing on the structure sheaf”.

Stacks 02SP. c₁(𝒪_X) ∩ α = 0 in A_k(X) for every α ∈ Z_{k+1}(X).

Additivity applied to L = N = 𝒪_X together with 𝒪_X ⊗_{𝒪_X} 𝒪_X ≅ 𝒪_X gives c₁(𝒪_X) ∩ α + c₁(𝒪_X) ∩ α = c₁(𝒪_X) ∩ α.

The companion assertion of the same tag is Stacks.Chow.firstChernClassCapOfInvertible_tensorObj.

theorem firstChernClassCapOfInvertible_unit (α : CycleGroup C p (k + 1)) :
    firstChernClassCapOfInvertible C p k (SheafOfModules.unit X.ringCatSheaf) α = 0

Tag 0EPI, a lemma

Tag 0EPI in the Stacks Project.

Stacks.Chow.zeroCycle_eq_sum_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/IntersectionInvertibleSheaf.lean, line 927.

Stacks 0EPI. Let (S, δ) be the base situation of chapter 42, let Y be locally of finite type over S, let L be an invertible 𝒪_Y-module and s a global section of L. Assume dim_δ(Y) ≤ k + 1, dim_δ(Z(s)) ≤ k, and that multiplication by s is injective on the stalk at the generic point of every component of Z(s) of delta-dimension k. Then the k-cycle of Z(s) is the sum of the k-cycles of the zero schemes of the restrictions of s to the components of Y of delta-dimension k + 1, weighted by their multiplicities in the fundamental cycle [Y]_{k + 1}.

theorem zeroCycle_eq_sum_components (C : ChowSituation.{u}) {Y : Scheme.{u}}
    (f : Y ⟶ C.S) [LocallyOfFiniteType f] (L : Y.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible Y.sheaf.obj Y.ringCatSheaf.property L]
    (s : L.sections) (k : ℤ)
    (hY : schemeDeltaDimension C f ≤ (k + 1 : EInt))
    (hD : schemeDeltaDimension C
      ((Stacks.Divisors.zeroScheme Y L (s.eval (op ⊤))).subschemeι ≫ f) ≤ (k : EInt))
    (hs : ∀ ξ : genericPoints (Stacks.Divisors.zeroScheme Y L (s.eval (op ⊤))).subscheme,
      relativeDimension C.dimensionFunction f
        ((Stacks.Divisors.zeroScheme Y L (s.eval (op ⊤))).subschemeι ξ.1) = k →
      Function.Injective (ConcreteCategory.hom
        ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u}
          ((Stacks.Divisors.zeroScheme Y L (s.eval (op ⊤))).subschemeι ξ.1)).map
          ((Scheme.Modules.toPresheaf Y).map (L.unitHomEquiv.symm s))))) :
    let D := Stacks.Divisors.zeroScheme Y L (s.eval (op ⊤))
    ∀ x : Y,
      (cycleAssociatedToClosedSubscheme C f D.subschemeι k).1 x =
        ∑ᶠ W : {W : irreducibleComponents Y //
            deltaDimension C f
              ⟨W.1, W.2.1, isClosed_of_mem_irreducibleComponents W.1 W.2⟩ = k + 1},
          (cycleAssociatedToClosedSubscheme C f (𝟙 Y) (k + 1)).1 W.1.2.1.genericPoint *
            (cycleAssociatedToClosedSubscheme C f
              ((Scheme.IdealSheafData.vanishingIdeal
                ⟨W.1.1, isClosed_of_mem_irreducibleComponents W.1.1 W.1.2⟩ ⊔ D).subschemeι)
              k).1 x

Tag 02SQ, a lemma

Tag 02SQ in the Stacks Project.

Stacks.ChernCap42.firstChernClassCapOfInvertible_closedSubscheme_eq_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCap42/ClosedSubschemeZeroCycle.lean, line 862.

Stacks 02SQ. Let (S, δ) be the base situation of chapter 42 of the Stacks Project, let X be locally of finite type over S, let L be an invertible 𝒪_X-module, let Y ⊆ X be a closed subscheme and let s be a global section of L|_Y. Assume dim_δ(Y) ≤ k + 1, that dim_δ(Z(s)) ≤ k, and that multiplication by s is injective on the local ring at the generic point of every component of Z(s) of δ-dimension k. Then

c₁(L) ∩ [Y]_{k + 1} = [Z(s)]_k in A_k(X).

The cycle [Z(s)]_k is read on X through the composite of the closed immersion of Z(s) into Y with that of Y into X.

theorem firstChernClassCapOfInvertible_closedSubscheme_eq_zeroScheme
    (s : ((Scheme.Modules.pullback i).obj L).sections)
    (hY : schemeDeltaDimension C (i ≫ p) ≤ (k + 1 : EInt))
    (hD : schemeDeltaDimension C
      ((Stacks.Divisors.zeroScheme Y ((Scheme.Modules.pullback i).obj L)
        (s.eval (op ⊤))).subschemeι ≫ (i ≫ p)) ≤ (k : EInt))
    (hs : ∀ ξ : genericPoints (Stacks.Divisors.zeroScheme Y
        ((Scheme.Modules.pullback i).obj L) (s.eval (op ⊤))).subscheme,
      relativeDimension C.dimensionFunction (i ≫ p)
        ((Stacks.Divisors.zeroScheme Y ((Scheme.Modules.pullback i).obj L)
          (s.eval (op ⊤))).subschemeι ξ.1) = k →
      Function.Injective (ConcreteCategory.hom
        ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u}
          ((Stacks.Divisors.zeroScheme Y ((Scheme.Modules.pullback i).obj L)
            (s.eval (op ⊤))).subschemeι ξ.1)).map
          ((Scheme.Modules.toPresheaf Y).map
            (((Scheme.Modules.pullback i).obj L).unitHomEquiv.symm s))))) :
    firstChernClassCapOfInvertible C p k L (cycleAssociatedToClosedSubscheme C p i (k + 1)) =
      QuotientAddGroup.mk (cycleAssociatedToClosedSubscheme C p
        ((Stacks.Divisors.zeroScheme Y ((Scheme.Modules.pullback i).obj L)
          (s.eval (op ⊤))).subschemeι ≫ i) k)

Sources

• Section 42.25, Tag 02SN
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.firstChernClassCapOfInvertible · Stacks.Chow.firstChernClassCapOfInvertible_integral · Stacks.Chow.firstChernClassCapOfInvertible_finsum · Stacks.Chow.firstChernClassCapOfInvertible_tensorObj · Stacks.Chow.firstChernClassCapOfInvertible_unit · Stacks.Chow.zeroCycle_eq_sum_components · Stacks.ChernCap42.firstChernClassCapOfInvertible_closedSubscheme_eq_zeroScheme

Section42.26 Intersecting with an invertible sheaf and push and pull#

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

Tag 0EPJ, a lemma

Tag 0EPJ in the Stacks Project.

Stacks.Chow.flatPullback_meromorphicDivisor_eq_sum_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/FlatPullbackMeromorphicSection.lean, line 186.

Stacks 0EPJ. Let C = (S, δ) be the base situation of chapter 42, let X and Y be locally of finite type over S with Y integral of delta-dimension n, and let f : X ⟶ Y be flat of relative dimension r. For an invertible module L on Y and a nonzero meromorphic section s of L,

f^* div_L(s) = ∑_i n_i i_{i,*} div_{f^*L|_{X_i}}(s_i)

as (n + r - 1)-cycles on X. The sum runs over the irreducible components X_i of X taken with their reduced structure — each of these has delta-dimension n + r by Stacks.Chow.schemeDeltaDimension_integralComponentAt_comp, so this is the sum over the components of delta-dimension n + r that the source writes — i_i : X_i ⟶ X is the inclusion, s_i is the pullback of s along f|_{X_i}, and n_i is the multiplicity of X_i in X, read as the coefficient of X_i in the fundamental cycle [X]_{n + r}.

The identity is read coefficientwise at a point x of X, because the irreducible components of a locally Noetherian scheme need not form a finite set: neither side is a finite sum of cycles, and at a fixed point of X only finitely many components contribute.

theorem flatPullback_meromorphicDivisor_eq_sum_components (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
    [LocallyOfFiniteType sY] [IsIntegral Y] (f : X ⟶ Y) [LocallyOfFiniteType f] [Flat f]
    (hbase : f ≫ sY = sX) (r : ℕ) (hf : AlgebraicGeometry.RelativeDimension f r) {n : ℤ}
    (hY : schemeDeltaDimension C sY = (n : EInt)) (L : Y.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.2 L]
    (s : L.presheaf.stalk (genericPoint Y)) (hs : s ≠ 0) (x : X) :
    letI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
    (flatPullback C sX sY f hbase r hf (n - 1)
        (meromorphicDivisorCycleOfInvertible C sY hY L s).val).1 x =
      ∑ᶠ W : irreducibleComponents X,
        (cycleAssociatedToClosedSubscheme C sX (𝟙 X) (n + (r : ℤ))).1 W.2.1.genericPoint *
          (letI : IsIntegral (integralComponentAt W.2.1.genericPoint).subscheme :=
             isIntegral_integralComponentAt _
           letI : IsLocallyNoetherian (integralComponentAt W.2.1.genericPoint).subscheme :=
             LocallyOfFiniteType.isLocallyNoetherian
               ((integralComponentAt W.2.1.genericPoint).subschemeι ≫ sX)
           letI := isDominant_subschemeι_integralComponentAt_comp f W
           letI := isInvertible_presheaf_pullback L
             ((integralComponentAt W.2.1.genericPoint).subschemeι ≫ f)
           (properPushforward C ((integralComponentAt W.2.1.genericPoint).subschemeι ≫ sX) sX
             (integralComponentAt W.2.1.genericPoint).subschemeι rfl (n + (r : ℤ) - 1)
             (meromorphicDivisorCycleOfInvertible C
               ((integralComponentAt W.2.1.genericPoint).subschemeι ≫ sX)
               (schemeDeltaDimension_integralComponentAt_comp C sX sY f hbase r hf hY W)
               ((Scheme.Modules.pullback
                 ((integralComponentAt W.2.1.genericPoint).subschemeι ≫ f)).obj L)
               (genericStalkPullback
                 ((integralComponentAt W.2.1.genericPoint).subschemeι ≫ f) L s)).val).1 x)

Tag 02SS, a lemma

Tag 02SS in the Stacks Project.

Stacks.Chow.flatNaturality_firstChernIdentityCapRule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FirstChernClassCanonical.lean, line 275. The attribute's comment: “the flat-pullback identity read for the identity cap rule of the canonical first Chern class cap product on the test schemes of X, i.e. the predicate IdentityCapRule.FlatNaturality that the bivariant class of Stacks 0B77 takes as its second naturality hypothesis, with no hypothesis of its own”.

The flat-pullback identity on the test schemes. For the canonical first Chern class cap product and test morphisms g : T ⟶ X and h : T' ⟶ T with h flat of relative dimension r,

c₁((h ∘ g)^*ℒ) ∩ h^*α = h^*(c₁(g^*ℒ) ∩ α),

the two sides sitting in the degrees (k + r) - 1 and (k - 1) + r. This is Stacks.Chow.IdentityCapRule.FlatNaturality for Stacks.Chow.firstChernIdentityCapRule at the canonical cap product.

theorem flatNaturality_firstChernIdentityCapRule :
    IdentityCapRule.FlatNaturality C sX 1
      (firstChernIdentityCapRule C sX (canonicalFirstChernCapRule C) L)

Stacks.Chow.flatPullback_firstChernCapOfInvertible_rationallyEquivalent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FlatPullback/InvertibleChernCapPullback.lean, line 52.

Intersecting with the first Chern class of an invertible module commutes with flat pullback: for f : X' ⟶ X flat of relative dimension r, an invertible module L on X and a (k+1)-cycle α on X, the cycle representing c₁(f^*L) ∩ f^*α and the flat pullback of the cycle representing c₁(L) ∩ α are rationally equivalent on X'.

theorem flatPullback_firstChernCapOfInvertible_rationallyEquivalent (α : CycleGroup C p (k + 1)) :
    RationallyEquivalent C (f ≫ p) (k + (r : ℤ))
      ((firstChernCapRule C (f ≫ p) (k + (r : ℤ))
          (firstChernComponentCycleRule C (f ≫ p) (k + (r : ℤ))
            ((Scheme.Modules.pullback f).obj L))).extendCycleGroup
        ((show k + 1 + (r : ℤ) = k + (r : ℤ) + 1 by omega) ▸
          flatPullback C (f ≫ p) p f rfl r hf (k + 1) α))
      (flatPullback C (f ≫ p) p f rfl r hf k
        ((firstChernCapRule C p k (firstChernComponentCycleRule C p k L)).extendCycleGroup α))

Tag 02ST, a lemma

Tag 02ST in the Stacks Project.

Stacks.Chow.properChowPushforward_firstChernClassCapOfInvertible_fundamentalCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDominantPushforward.lean, line 257. The attribute's comment: “second displayed equation”.

The second displayed equation of Stacks 02ST. Let X and Y be integral and locally of finite type over the base with dim_δ(X) = dim_δ(Y) = n, let f : X ⟶ Y be proper and dominant over the base and let L be an invertible 𝒪_Y-module. Then

f_*(c₁(f^*L) ∩ [X]) = [R(X) : R(Y)] c₁(L) ∩ [Y] = c₁(L) ∩ f_*[X]

in CH_{n-1}(Y), the two equalities being the two conjuncts below.

The proper pushforward on Chow groups carries no hypothesis: Stacks 02S2 is Stacks.Chow.properPushforwardFactorsThroughRationalEquivalence. The invertibility of f^*L is Stacks 0B8L, the instance Stacks.Divisors.pullback_isInvertible.

theorem properChowPushforward_firstChernClassCapOfInvertible_fundamentalCycle
    (C : ChowSituation.{u}) {X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] [IsIntegral X] [IsIntegral Y] {n : ℤ}
    (hnX : schemeDeltaDimension C sX = (n : EInt))
    (hnY : schemeDeltaDimension C sY = (n : EInt))
    (f : X ⟶ Y) [IsProper f] [IsDominant f] (hf : f ≫ sY = sX) (L : Y.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible Y.sheaf.obj Y.ringCatSheaf.property L] :
    letI : Algebra Y.functionField X.functionField := (dominantFunctionFieldMap f).toAlgebra
    properChowPushforward C sX sY f hf (n - 1)
          (properPushforwardFactorsThroughRationalEquivalence C sX sY f hf (n - 1))
          (firstChernClassCapOfInvertible C sX (n - 1) ((Scheme.Modules.pullback f).obj L)
            (cycleAssociatedToClosedSubscheme C sX (𝟙 X) (n - 1 + 1))) =
        (Module.finrank Y.functionField X.functionField : ℤ) •
          firstChernClassCapOfInvertible C sY (n - 1) L
            (cycleAssociatedToClosedSubscheme C sY (𝟙 Y) (n - 1 + 1)) ∧
      firstChernClassCapOfInvertible C sY (n - 1) L
          (properPushforward C sX sY f hf (n - 1 + 1)
            (cycleAssociatedToClosedSubscheme C sX (𝟙 X) (n - 1 + 1))) =
        (Module.finrank Y.functionField X.functionField : ℤ) •
          firstChernClassCapOfInvertible C sY (n - 1) L
            (cycleAssociatedToClosedSubscheme C sY (𝟙 Y) (n - 1 + 1))

Stacks.Chow.properPushforward_meromorphicDivisorCycleOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/MeromorphicDivisorPushforward.lean, line 191. The attribute's comment: “first displayed equation”.

The first displayed equation of Stacks 02ST. For a proper dominant morphism p : X ⟶ Y of integral schemes locally of finite type over the base with dim_δ(X) = dim_δ(Y) = n, an invertible 𝒪_Y-module L and a nonzero meromorphic section s of L, the proper pushforward of the divisor cycle of p^*s is [R(X) : R(Y)] times the divisor cycle of s, as cycles.

These are the hypotheses the source states the tag under; the rank-one hypothesis of Stacks.Chow.properPushforward_meromorphicDivisorCycle is discharged here by Stacks.Divisors.isTrivializedNear_of_isInvertible. The tag's second displayed equation, the first Chern class consequence, is in StacksFrontier.AlgebraicGeometry.Chow.ChernClassDominantPushforward, so the attribute names this clause explicitly; see the module documentation.

theorem properPushforward_meromorphicDivisorCycleOfInvertible (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
    [LocallyOfFiniteType sY] [IsIntegral X] [IsIntegral Y] [IsLocallyNoetherian X]
    [IsLocallyNoetherian Y] {n : ℤ}
    (hnX : schemeDeltaDimension C sX = (n : EInt))
    (hnY : schemeDeltaDimension C sY = (n : EInt))
    (p : X ⟶ Y) [IsProper p] [IsDominant p] (hp : p ≫ sY = sX) (L : Y.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.2 L]
    (s : L.presheaf.stalk (genericPoint Y)) (hs : s ≠ 0) :
    letI : Algebra Y.functionField X.functionField := (dominantFunctionFieldMap p).toAlgebra
    properPushforward C sX sY p hp (n - 1)
        (meromorphicDivisorCycle C sX hnX
          (fun x => (isTrivializedNear_of_isInvertible L (p.base x)).pullback)
          (genericStalkPullback p L s)).val =
      (Module.finrank Y.functionField X.functionField : ℤ) •
        (meromorphicDivisorCycle C sY hnY (isTrivializedNear_of_isInvertible L) s).val

Tag 02SU, a lemma

Tag 02SU in the Stacks Project.

Stacks.Chow.properNaturality_firstChernIdentityCapRule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FirstChernClassCanonical.lean, line 194. The attribute's comment: “the projection formula read for the identity cap rule of the canonical first Chern class cap product on the test schemes of X, i.e. the predicate IdentityCapRule.ProperNaturality that the bivariant class of Stacks 0B77 takes as its first naturality hypothesis, with no hypothesis of its own”.

The projection formula on the test schemes. For the canonical first Chern class cap product and test morphisms g : T ⟶ X and h : T' ⟶ T with h proper,

c₁(g^*ℒ) ∩ h_*α = h_*(c₁((h ∘ g)^*ℒ) ∩ α).

This is Stacks.Chow.IdentityCapRule.ProperNaturality for Stacks.Chow.firstChernIdentityCapRule at the canonical cap product.

theorem properNaturality_firstChernIdentityCapRule :
    IdentityCapRule.ProperNaturality C sX 1
      (firstChernIdentityCapRule C sX (canonicalFirstChernCapRule C) L)

Stacks.Chow.properChowPushforward_firstChernClassCapOfInvertible_of_isProper', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCapProperPushforward/Invertible.lean, line 268.

Stacks 02SU. Let p : X ⟶ Y be a proper morphism of schemes locally of finite type over the base scheme of chapter 42 and let ℒ be an invertible 𝒪_Y-module. Then for every (k+1)-cycle α on X

p_*(c₁(p^*ℒ) ∩ α) = c₁(ℒ) ∩ p_*α in A_k(Y).

theorem properChowPushforward_firstChernClassCapOfInvertible_of_isProper'
    (α : CycleGroup C sX (k + 1)) :
    letI := isInvertible_presheaf_modulePullback L p
    properChowPushforward C sX sY p hp k
        (properPushforwardFactorsThroughRationalEquivalence C sX sY p hp k)
        (firstChernClassCapOfInvertible C sX k ((Scheme.Modules.pullback p).obj L) α) =
      firstChernClassCapOfInvertible C sY k L
        (properPushforward C sX sY p hp (k + 1) α)

Stacks.Chow.properChowPushforward_firstChernClassCapOfInvertible_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCapPushforward/Proper.lean, line 471.

Stacks 02SU. Let p : X ⟶ Y be a proper morphism of schemes locally of finite type over the base scheme of chapter 42, and let ℒ be an invertible 𝒪_Y-module. Then for every (k+1)-cycle α on X

p_*(c₁(p^*ℒ) ∩ α) = c₁(ℒ) ∩ p_*α in A_k(Y).

The invertibility of p^*ℒ is Stacks 0B8L (Stacks.Divisors.pullback_isInvertible), and proper pushforward on Chow groups is defined by Stacks 02S2 (Stacks.Chow.properPushforwardFactorsThroughRationalEquivalence_of_isProper).

theorem properChowPushforward_firstChernClassCapOfInvertible_of_isProper
    (α : CycleGroup C sX (k + 1)) :
    properChowPushforward C sX sY p hp k
        (properPushforwardFactorsThroughRationalEquivalence_of_isProper C sX sY p hp k)
        (firstChernClassCapOfInvertible C sX k ((Scheme.Modules.pullback p).obj L) α) =
      firstChernClassCapOfInvertible C sY k L (properPushforward C sX sY p hp (k + 1) α)

Sources

• Section 42.26, Tag 0AYA
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.flatPullback_meromorphicDivisor_eq_sum_components · Stacks.Chow.flatNaturality_firstChernIdentityCapRule · Stacks.Chow.flatPullback_firstChernCapOfInvertible_rationallyEquivalent · Stacks.Chow.properChowPushforward_firstChernClassCapOfInvertible_fundamentalCycle · Stacks.Chow.properPushforward_meromorphicDivisorCycleOfInvertible · Stacks.Chow.properNaturality_firstChernIdentityCapRule · Stacks.Chow.properChowPushforward_firstChernClassCapOfInvertible_of_isProper' · Stacks.Chow.properChowPushforward_firstChernClassCapOfInvertible_of_isProper

Section42.27 The key formula#

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

Tag 0AYB, the section

Tag 0AYB in the Stacks Project.

Stacks.Chow.KeyFormulaSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/Situation.lean, line 169. The attribute's comment: “the situation preceding the key formula: two invertible modules with nonzero meromorphic sections, and a family of prime divisors with chosen local generators”.

The situation preceding the key formula, Stacks 0AYB. On an integral, locally Noetherian scheme X, two invertible 𝒪_X-modules L and N with nonzero meromorphic sections s and t, together with a locally finite family {Z_i} of prime divisors of X large enough that s generates L and t generates N at the generic point of every prime divisor outside the family, and, for each i, chosen generators s_i of L_{ξ_i} and t_i of N_{ξ_i} at the generic point ξ_i of Z_i.

The ratios f_i = s / s_i and g_i = t / t_i, the orders of vanishing, the restrictions s_i|_{Z_i} and t_i|_{Z_i} and the tame symbols ∂_{B_i}(f_i, g_i) are determined by these data, and are constructed from them below.

A meromorphic section is given by its value in the generic stalk, and is nonzero exactly when that value is; see the module documentation.

public structure KeyFormulaSituation (L N : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property N]

Tag 0AYC, a lemma

Tag 0AYC in the Stacks Project.

Stacks.Chow.KeyFormulaData.keyFormula_iff_forall_component_coheight_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/LocalReduction.lean, line 199. The attribute's comment: “the localization step of the source's proof: the equality of the two cycles is equivalent to the equality of their coefficients at the codimension-two points of the family”.

The key formula is local at the codimension-one points of the family. It holds if and only if its two coefficients agree at the image of every codimension-one point of every member Z_i.

This is the step of the source's proof that says "since we are proving the equality of cycles we may argue one coefficient at a time", and it is only that step. At such a point x the local ring 𝒪_{X, x} has dimension two, only the finitely many members of the family through x contribute to either side, and the source derives the resulting identity of coefficients from the Key Lemma Stacks 0EAX on 𝒪_{X, x}. That derivation is not carried out here: the identity of coefficients stands on the right hand side of the equivalence, so this declaration proves the equivalence and not the key formula.

Stacks 0EAX itself is proved, as Stacks.Chow.finsum_fracTameSymbolOrderAt_canonical_eq_zero. The step from it to the identity of coefficients goes through the dictionary between X and A = 𝒪_{X, x} described in the module documentation.

theorem keyFormula_iff_forall_component_coheight_one [LocallyOfFiniteType p] :
    D.KeyFormula C p ↔ ∀ (i : D.Index) (z : (D.component i).subscheme), Order.coheight z = 1 →
      D.leftCoeff C p ((D.component i).subschemeι.base z) =
        D.tameSymbolCoeff C p ((D.component i).subschemeι.base z)

Stacks.Chow.KeyFormulaSituation.keyFormula_toKeyFormulaData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/SituationKeyFormula.lean, line 806. The attribute's comment: “the key formula itself, for the sheaf-level situation of Stacks 0AYB: the difference of the two Chern-class cycles equals the sum of the principal divisors of the tame symbols”.

Stacks 0AYC for the situation of Stacks 0AYB. The key formula holds for the cycle-level data of the sheaf-level situation: the difference of the two Chern-class cycles is the locally finite sum of the principal divisors of the tame symbols ∂_{B_i}(f_i, g_i) on the members of the family.

At a codimension-two point x of a member of the family the two coefficients are compared by the local reciprocity law Stacks 0EAX on A = 𝒪_{X, x}, read at the pair of coordinates of s and t taken from trivializations of L and N near x: that sum vanishes, the members of the family carry all of it, and the difference between its summands and the summands of the right hand side of the key formula is the change-of-generator correction of Stacks 0EAN and Stacks 02SH, which is the left hand side. See the module documentation.

theorem keyFormula_toKeyFormulaData : (ℱ.toKeyFormulaData C p).KeyFormula C p

Tag 0GU9, a remark

Tag 0GU9 in the Stacks Project.

Stacks.Chow.pointwiseDivisorDifferential_comp_pointwiseMilnorBoundary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChowGroupOne.lean, line 161. The attribute's comment: “the complex of the tag: the composite of the tame-symbol differential of the tag with the divisor differential of Stacks 0GU3 is the zero homomorphism, so the three locally finite direct sums of Stacks 0GU2 -- the degree-two, degree-one and degree-zero Milnor K-groups of the residue fields at the points of relative dimension k + 2, k + 1 and k -- form a complex”.

Stacks 0GU9. The three locally finite direct sums of Milnor K-groups of the tag form a complex: the tame-symbol differential followed by the divisor differential of Stacks 0GU3 is the zero homomorphism.

This is the assertion of the tag. By Stacks.Chow.pointwiseDivisorDifferential_comp_pointwiseMilnorBoundary_of_forall it suffices to check it one point of relative dimension k + 2 and one point of relative dimension k at a time, which is Stacks.Chow.finsum_pointClosureOrdBoundaryTerm_eq_zero.

theorem pointwiseDivisorDifferential_comp_pointwiseMilnorBoundary (k : ℤ) :
    (pointwiseDivisorDifferential C p k).comp (pointwiseMilnorBoundary C p k) = 0

Stacks.Chow.pointwiseMilnorShortComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChowGroupOne.lean, line 183. The attribute's comment: “the complex of the tag, assembled as a short complex of abelian groups out of the three locally finite direct sums of Stacks 0GU2 and the two differentials, the vanishing of whose composite is its defining property”.

Stacks 0GU9. The complex of the tag, packaged as a short complex of abelian groups: the degree-two Milnor K-chains at the points of relative dimension k + 2, the degree-one chains at the points of relative dimension k + 1 and the degree-zero chains at the points of relative dimension k, with the tame-symbol differential and the divisor differential of Stacks 0GU3. Its zero field is Stacks.Chow.pointwiseDivisorDifferential_comp_pointwiseMilnorBoundary.

def pointwiseMilnorShortComplex (k : ℤ) : ShortComplex AddCommGrpCat.{u}

Stacks.Chow.pointwiseMilnorBoundary, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/PointwiseMilnorBoundary.lean, line 433. The attribute's comment: “the first differential of the complex of the tag, as a homomorphism of the locally finite direct sums of Stacks 0GU2: the degree-two Milnor K-chain group at the points of relative dimension k + 2 maps to the degree-one chain group at the points of relative dimension k + 1 by the rule whose coefficient at a point x' is the sum, over the points x of relative dimension k + 2 specializing to x', of the tame-symbol boundary of the class at x along the one-dimensional local ring of the closure of x at x'; both the finiteness of that sum and the local finiteness of the resulting family are proved, so the rule is a well defined additive map”.

Stacks 0GU9. The first differential of the complex of the tag: the homomorphism from the locally finite direct sum of the degree-two Milnor K-groups at the points of relative dimension k + 2 to the locally finite direct sum of the degree-one Milnor K-groups at the points of relative dimension k + 1 whose coefficient at x' is the sum, over the points x of relative dimension k + 2 specializing to x', of the tame-symbol boundaries ∂_{𝒪_{closure {x}, x'}} of the classes of the chain.

def pointwiseMilnorBoundary (k : ℤ) :
    PointwiseKTwoGroup C p k →+ PointwiseKOneGroup C p k

AlgebraicGeometry.milnorKTwoTameSymbol, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Symbols/MilnorBoundary.lean, line 161. The attribute's comment: “the construction of the local component of the first differential: the tame symbol of a one-dimensional Noetherian local domain, descended to a homomorphism from the degree-two Milnor K-group of its fraction field to the degree-one Milnor K-group of its residue field”.

Stacks Project, Tag 0GU9. The tame symbol ∂_A of a one-dimensional Noetherian local domain A with fraction field K, descended along the presentation of Milnor K-theory to a homomorphism K₂ᴹ(K) ⟶ K₁ᴹ(κ(A)). This is the local component of the first differential of the complex of the tag, the one written ∂_{𝒪_{W_x, x'}} there.

def milnorKTwoTameSymbol (hdim : ringKrullDim A = 1) :
    MilnorKTheory K 2 →+ MilnorKTheory (IsLocalRing.ResidueField A) 1

AlgebraicGeometry.sum_localMilnorBoundaryOrder_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Symbols/MilnorBoundary.lean, line 384. The attribute's comment: “the vanishing of the composite of the two differentials in its local algebraic form: for a two-dimensional Noetherian local domain, the orders along the quotients of the tame-symbol boundaries of an arbitrary degree-two Milnor K-class of the fraction field, summed over the height-one primes, give zero -- this is the displayed sum of the tag's proof, with the reduction to a pure symbol discharged; the fraction field is realized as FractionRing A, and the geometric indexing of that sum by the intermediate points, the locally finite chain groups and the three-term complex itself are not formalized here”.

Stacks Project, Tag 0GU9. Let A be a two-dimensional Noetherian local domain with fraction field K and let α be a class in the degree-two Milnor K-group of K. Summing, over the height-one primes 𝔮 of A, the order along A / 𝔮 of the tame-symbol boundary of α at 𝔮 gives zero.

This is the vanishing which the tag's argument reduces the composite of its two differentials to: at a point x'' of δ-dimension k lying on the integral closed subscheme W with generic point x of δ-dimension k + 2, the ring A is 𝒪_{W, x''}, its height-one primes are the intermediate points x' of δ-dimension k + 1, and the summand at 𝔮 is the coefficient ord_{𝒪_{closure {x'}, x''}}(∂_{𝒪_{W, x'}}(α)). The source reduces to a pure symbol by additivity and linearity before appealing to Stacks 0EAX; here the reduction is carried out, so the statement holds for every class of the Milnor K-group and not only for a pure symbol.

theorem sum_localMilnorBoundaryOrder_eq_zero (hdim : ringKrullDim A = 2)
    (α : MilnorKTheory (FractionRing A) 2) :
    (∑ᶠ q : {q : Ideal A // q.IsPrime ∧ q.height = 1},
      localMilnorBoundaryOrder hdim q α) = 0

Tag 0GUA, a remark

Tag 0GUA in the Stacks Project.

Stacks.Chow.milnorChainComap_pointwiseMilnorBoundary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChainBoundaryCompatible.lean, line 127. The attribute's comment: “the compatibility of the restriction map of the degreewise localization sequence of the tag with the FIRST boundary map of the complex of Stacks 0GU9, the tame-symbol differential: for an open immersion j into a scheme locally of finite type over a Chow situation, restriction of locally finite Milnor K-chains to the open subscheme carries the tame-symbol differential in relative dimensions k + 2 and k + 1 to the tame-symbol differential of the open subscheme. The companion square for the extension-by-zero map from the closed complement is Stacks.Chow.pointwiseMilnorBoundary_milnorChainExtend. The two squares for the SECOND boundary map, the divisor differential of Stacks 0GU3, are Stacks.Chow.milnorChainComap_pointwiseDivisorDifferential and Stacks.Chow.pointwiseDivisorDifferential_milnorChainExtend; the six-term exact sequence the snake lemma yields from all four is Stacks.Chow.milnorChowLocalization_exact”.

Stacks 0GUA for the first differential and the restriction map. Restriction of locally finite Milnor K-chains to an open subscheme commutes with the tame-symbol differential of Stacks 0GU9: the square formed by the two differentials and the two restriction maps, in Milnor degrees two and one, commutes.

theorem milnorChainComap_pointwiseMilnorBoundary (k : ℤ) :
    (pointwiseMilnorBoundary C (j ≫ p) k).comp
        (milnorChainComap C p j (injective_base_of_isOpenImmersion j)
          (bijective_residueFieldMap_openImmersion j) (k + 2) 2) =
      (milnorChainComap C p j (injective_base_of_isOpenImmersion j)
          (bijective_residueFieldMap_openImmersion j) (k + 1) 1).comp
        (pointwiseMilnorBoundary C p k)

Stacks.Chow.pointwiseMilnorBoundary_milnorChainExtend, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChainBoundaryCompatible.lean, line 254. The attribute's comment: “the compatibility of the extension-by-zero map of the degreewise localization sequence of the tag with the FIRST boundary map of the complex of Stacks 0GU9, the tame-symbol differential: for a closed immersion i into a scheme locally of finite type over a Chow situation, extension by zero of locally finite Milnor K-chains from the closed subscheme carries its tame-symbol differential in relative dimensions k + 2 and k + 1 to the tame-symbol differential of the ambient scheme. The companion square for the restriction map to the open complement is Stacks.Chow.milnorChainComap_pointwiseMilnorBoundary. The two squares for the SECOND boundary map, the divisor differential of Stacks 0GU3, are Stacks.Chow.milnorChainComap_pointwiseDivisorDifferential and Stacks.Chow.pointwiseDivisorDifferential_milnorChainExtend; the six-term exact sequence the snake lemma yields from all four is Stacks.Chow.milnorChowLocalization_exact”.

Stacks 0GUA for the first differential and the extension-by-zero map. Extension by zero of locally finite Milnor K-chains from a closed subscheme commutes with the tame-symbol differential of Stacks 0GU9.

theorem pointwiseMilnorBoundary_milnorChainExtend (k : ℤ) :
    (pointwiseMilnorBoundary C p k).comp
        (milnorChainExtend C p i (injective_base_of_isClosedImmersion i)
          (bijective_residueFieldMap_closedImmersion i) inferInstance (k + 2) 2) =
      (milnorChainExtend C p i (injective_base_of_isClosedImmersion i)
          (bijective_residueFieldMap_closedImmersion i) inferInstance (k + 1) 1).comp
        (pointwiseMilnorBoundary C (i ≫ p) k)

Stacks.Chow.milnorChainComap_pointwiseDivisorDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChainDivisorCompatible.lean, line 67. The attribute's comment: “the compatibility of the restriction map of the degreewise localization sequence of the tag with the SECOND boundary map of the complex of Stacks 0GU9, the divisor differential of Stacks 0GU3: for an open immersion j into a scheme locally of finite type over a Chow situation, restriction of locally finite Milnor K-chains to the open subscheme carries the divisor differential in relative dimensions k + 1 and k to the divisor differential of the open subscheme. The companion square for the extension-by-zero map from the closed complement is Stacks.Chow.pointwiseDivisorDifferential_milnorChainExtend”.

Stacks 0GUA for the second differential and the restriction map. Restriction of locally finite Milnor K-chains to an open subscheme commutes with the divisor differential of Stacks 0GU3: the square formed by the two differentials and the two restriction maps, in Milnor degrees one and zero, commutes.

theorem milnorChainComap_pointwiseDivisorDifferential (k : ℤ) :
    (pointwiseDivisorDifferential C (j ≫ p) k).comp
        (milnorChainComap C p j (injective_base_of_isOpenImmersion j)
          (bijective_residueFieldMap_openImmersion j) (k + 1) 1) =
      (milnorChainComap C p j (injective_base_of_isOpenImmersion j)
          (bijective_residueFieldMap_openImmersion j) k 0).comp
        (pointwiseDivisorDifferential C p k)

Stacks.Chow.pointwiseDivisorDifferential_milnorChainExtend, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChainDivisorCompatible.lean, line 147. The attribute's comment: “the compatibility of the extension-by-zero map of the degreewise localization sequence of the tag with the SECOND boundary map of the complex of Stacks 0GU9, the divisor differential of Stacks 0GU3: for a closed immersion i into a scheme locally of finite type over a Chow situation, extension by zero of locally finite Milnor K-chains from the closed subscheme carries its divisor differential in relative dimensions k + 1 and k to the divisor differential of the ambient scheme. The companion square for the restriction map to the open complement is Stacks.Chow.milnorChainComap_pointwiseDivisorDifferential”.

Stacks 0GUA for the second differential and the extension-by-zero map. Extension by zero of locally finite Milnor K-chains from a closed subscheme commutes with the divisor differential of Stacks 0GU3.

theorem pointwiseDivisorDifferential_milnorChainExtend (k : ℤ) :
    (pointwiseDivisorDifferential C p k).comp
        (milnorChainExtend C p i (injective_base_of_isClosedImmersion i)
          (bijective_residueFieldMap_closedImmersion i) inferInstance (k + 1) 1) =
      (milnorChainExtend C p i (injective_base_of_isClosedImmersion i)
          (bijective_residueFieldMap_closedImmersion i) inferInstance k 0).comp
        (pointwiseDivisorDifferential C (i ≫ p) k)

Stacks.Chow.milnorChainLocalizationComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChainLocalization.lean, line 576. The attribute's comment: “the degreewise localization sequence of the tag, for one relative dimension m and one Milnor degree n: the locally finite direct sums of Stacks 0GU2 for the closed subscheme, the ambient scheme and the complementary open subscheme, together with the extension-by-zero map from the closed subscheme and the restriction map to the open subscheme, as a short complex of abelian groups; its compatibility with the two boundary maps of Stacks 0GU9, and the six-term exact sequence the snake lemma yields from it, are proved not here but in Stacks.Chow.milnorChowLocalization_exact, Stacks.Chow.milnorChainComap_pointwiseMilnorBoundary, Stacks.Chow.pointwiseMilnorBoundary_milnorChainExtend, Stacks.Chow.milnorChainComap_pointwiseDivisorDifferential and Stacks.Chow.pointwiseDivisorDifferential_milnorChainExtend”.

Stacks 0GUA. The degreewise localization sequence of locally finite Milnor K-chains: the chains on the closed subscheme Y, on X and on the open subscheme U, with extension by zero from Y and restriction to U.

def milnorChainLocalizationComplex (hcomp : Set.range i.base = (Set.range j.base)ᶜ)
    (m : ℤ) (n : ℕ) : ShortComplex AddCommGrpCat.{u}

Stacks.Chow.milnorChainLocalizationSplitting, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChainLocalization.lean, line 597. The attribute's comment: “the splitting of the degreewise localization sequence of the tag: restriction to the closed subscheme retracts the extension by zero from it, extension by zero from the open subscheme sections the restriction to it, and the two resulting idempotents of the chains on the ambient scheme add up to the identity”.

Stacks 0GUA. The degreewise localization sequence is split: restriction to Y is a retraction of the extension by zero from Y, extension by zero from U is a section of the restriction to U, and the two composites add up to the identity.

def milnorChainLocalizationSplitting (hcomp : Set.range i.base = (Set.range j.base)ᶜ)
    (m : ℤ) (n : ℕ) :
    (milnorChainLocalizationComplex C p i j hcomp m n).Splitting

Stacks.Chow.milnorChainLocalization_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChainLocalization.lean, line 623. The attribute's comment: “the short exactness of the degreewise localization sequence of the tag, in one relative dimension and one Milnor degree: extension by zero from the closed subscheme is injective, restriction to the open subscheme is surjective, and the image of the first is the kernel of the second”.

Stacks 0GUA. The degreewise localization sequence is short exact: it is split, and a split short complex is short exact.

theorem milnorChainLocalization_shortExact
    (hcomp : Set.range i.base = (Set.range j.base)ᶜ) (m : ℤ) (n : ℕ) :
    (milnorChainLocalizationComplex C p i j hcomp m n).ShortExact

Stacks.Chow.milnorChainLocalization_shortExact_degrees, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChainLocalization.lean, line 675. The attribute's comment: “the three split short exact sequences of the tag, for i = 2, 1 and 0: for an open subscheme and a closed subscheme with complementary underlying set, the sequence of locally finite direct sums of the degree-i Milnor K-groups of the residue fields at the points of relative dimension k + i is short exact and split; the middle terms are exactly the three groups carrying the complex of Stacks 0GU9. Only the sequences themselves are proved here; their compatibility with the two boundary maps of that complex is proved in Stacks.Chow.milnorChainComap_pointwiseMilnorBoundary, Stacks.Chow.pointwiseMilnorBoundary_milnorChainExtend, Stacks.Chow.milnorChainComap_pointwiseDivisorDifferential and Stacks.Chow.pointwiseDivisorDifferential_milnorChainExtend, and the six-term exact sequence the snake lemma yields from them is Stacks.Chow.milnorChowLocalization_exact”.

Stacks 0GUA. The three split short exact sequences of the tag, for i = 2, 1, 0: the locally finite direct sums of degree-i Milnor K-groups at the points of relative dimension k + i, for the closed subscheme, the ambient scheme and the complementary open subscheme. By Stacks.Chow.milnorChainLocalizationComplex_X₂_two, Stacks.Chow.milnorChainLocalizationComplex_X₂_one and Stacks.Chow.milnorChainLocalizationComplex_X₂_zero the middle terms are the three groups that carry the complex of Stacks 0GU9.

theorem milnorChainLocalization_shortExact_degrees
    (hcomp : Set.range i.base = (Set.range j.base)ᶜ) (k : ℤ) :
    (milnorChainLocalizationComplex C p i j hcomp (k + 2) 2).ShortExact ∧
      (milnorChainLocalizationComplex C p i j hcomp (k + 1) 1).ShortExact ∧
      (milnorChainLocalizationComplex C p i j hcomp k 0).ShortExact

Stacks.Chow.milnorChowGroupOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChowGroupOne.lean, line 226. The attribute's comment: “the definition of the tag: the first higher Chow group CH^M_k(X, 1) is the homology in the middle of the complex of Stacks 0GU9, formed as the degree-one Milnor K-chains killed by the divisor differential of Stacks 0GU3 modulo the image of the tame-symbol differential of Stacks 0GU9, the latter lying in the former because that composite is the zero homomorphism; the localization property of the tag, namely the degreewise split short exact sequences attached to an open subscheme with reduced closed complement together with the six-term exact sequence the snake lemma yields from them, is not proved here but in Stacks.Chow.milnorChainLocalization_shortExact_degrees and Stacks.Chow.milnorChowLocalization_exact”.

Stacks 0GUA. The first higher Chow group CH^M_k(X, 1) of the tag: the homology in the middle of the complex of Stacks 0GU9, that is, the degree-one Milnor K-chains killed by the divisor differential of Stacks 0GU3 modulo those coming from a degree-two Milnor K-chain under the tame-symbol differential. The superscript of the tag distinguishes this group from the higher Chow groups of the literature.

def milnorChowGroupOne (k : ℤ) : Type u

Stacks.Chow.milnorChowLocalization_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalEquivalence/MilnorChowLocalizationSequence.lean, line 622. The attribute's comment: “the six-term exact sequence of the tag, the main claim of the remark: for an open subscheme V of a scheme X locally of finite type over a Chow situation and a closed immersion i of Y into X whose image is the complement of V, the sequence of the first higher Chow groups of Y, X and V, followed by the Chow groups of Y, X and V and ending in zero, is exact. The first two maps are induced on the first higher Chow groups of Stacks 0GU9 by the extension-by-zero and restriction maps of the degreewise localization sequence of the tag; the third is the connecting map of the snake lemma, formed from the splitting of that sequence; the last two are the proper pushforward along the closed immersion and the restriction to the open subscheme of Stacks 02RX”.

Stacks 0GUA. The six-term exact sequence

CH^M_k(Y, 1) ⟶ CH^M_k(X, 1) ⟶ CH^M_k(V, 1) ⟶ CH_k(Y) ⟶ CH_k(X) ⟶ CH_k(V) ⟶ 0

attached to an open subscheme V of X and a closed immersion i : Y ⟶ X with complementary image. The first three maps are those induced by the extension-by-zero and restriction maps of the degreewise localization sequence of the tag, together with the connecting map Stacks.Chow.milnorChowBoundary; the last two are the proper pushforward and the restriction to an open subscheme of Stacks 02RX, whose exactness and surjectivity are Stacks.Chow.exact_chowPushforward_chowGroupOpensRestrict and Stacks.Chow.surjective_chowGroupOpensRestrictOfIsOpenImmersion.

theorem milnorChowLocalization_exact (k : ℤ) :
    Function.Exact (milnorChowGroupOneExtend C p i k) (milnorChowGroupOneComap C p V k) ∧
      Function.Exact (milnorChowGroupOneComap C p V k) (milnorChowBoundary C p i V hcomp k) ∧
      Function.Exact (milnorChowBoundary C p i V hcomp k)
        (chowPushforwardOfIsClosedImmersion C (i ≫ p) p i rfl k) ∧
      Function.Exact (chowPushforwardOfIsClosedImmersion C (i ≫ p) p i rfl k)
        (chowGroupOpensRestrictOfIsOpenImmersion C p V k) ∧
      Function.Surjective (chowGroupOpensRestrictOfIsOpenImmersion C p V k)

Sources

• Section 42.27, Tag 0AYB
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.KeyFormulaSituation · Stacks.Chow.KeyFormulaData.keyFormula_iff_forall_component_coheight_one · Stacks.Chow.KeyFormulaSituation.keyFormula_toKeyFormulaData · Stacks.Chow.pointwiseDivisorDifferential_comp_pointwiseMilnorBoundary · Stacks.Chow.pointwiseMilnorShortComplex · Stacks.Chow.pointwiseMilnorBoundary · AlgebraicGeometry.milnorKTwoTameSymbol · AlgebraicGeometry.sum_localMilnorBoundaryOrder_eq_zero

Section42.28 Intersecting with an invertible sheaf and rational equivalence#

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

Tag 02TH, a lemma

Tag 02TH in the Stacks Project.

Stacks.Chow.firstChernClassCap_comm_of_keyFormula, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionCommutativity.lean, line 144. The attribute's comment: “granting the key formula 0AYC and the divisor cycles of 02SJ”.

The commutativity of Stacks 02TH, granting the key formula. On an integral scheme of delta-dimension k + 2, intersecting the divisor cycle of a nonzero meromorphic section of one invertible module with the first Chern class of the other gives the same class in A_k(X), in either order.

Granting the key formula of Stacks 0AYC for the data D, this is immediate: the two sides are represented by the two halves of its left hand side, so their difference is a locally finite sum of principal divisors on the prime divisors Z_i. The component rules of the two invertible modules, the key formula itself and the two divisor cycles with their presentations by the family {Z_i} are explicit parameters; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.IntersectionCommutativity.

The @[stacks 02TH] attribute sits on Stacks.Chow.firstChernClassCapOfInvertible_divisorCycle_comm, where every one of those parameters is discharged; this is the step its proof is made of.

theorem firstChernClassCap_comm_of_keyFormula (hKey : D.KeyFormula C p)
    (chernL chernN : FirstChernComponentCycleRule C p k)
    (hchernL : ∀ (i : D.Index) (hW : IsIntegral (D.component i).subscheme)
      (hDim : schemeDeltaDimension C ((D.component i).subschemeι ≫ p) = ((k + 1 : ℤ) : EInt)),
      (chernL (D.component i) hW hDim).1 = D.restrictedDivisorL i)
    (hchernN : ∀ (i : D.Index) (hW : IsIntegral (D.component i).subscheme)
      (hDim : schemeDeltaDimension C ((D.component i).subschemeι ≫ p) = ((k + 1 : ℤ) : EInt)),
      (chernN (D.component i) hW hDim).1 = D.restrictedDivisorN i)
    (divL divN : CycleGroup C p (k + 1))
    (hdivL : ∀ x : X, divL.1 x = ∑ᶠ i, D.orderL i *
      (cycleAssociatedToClosedSubscheme C p (D.component i).subschemeι (k + 1)).1 x)
    (hdivN : ∀ x : X, divN.1 x = ∑ᶠ i, D.orderN i *
      (cycleAssociatedToClosedSubscheme C p (D.component i).subschemeι (k + 1)).1 x) :
    firstChernClassCap C p k chernN divL = firstChernClassCap C p k chernL divN

Stacks.Chow.KeyFormulaSituation.firstChernClassCapOfInvertible_comm_weilDivisorCycleN, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/ChernCapComm.lean, line 69. The attribute's comment: “the identity for two invertible modules with nonzero meromorphic sections on an integral, locally Noetherian scheme of delta-dimension k + 2, with no hypothesis: the key formula of Stacks 0AYC is discharged by Stacks.Chow.KeyFormulaSituation.keyFormula_toKeyFormulaData and the two divisor cycles of Stacks 02SJ are the canonical ones of the two sections”.

Stacks 02TH for the two canonical divisor cycles. On an integral, locally Noetherian scheme of delta-dimension k + 2,

c₁(N) ∩ div_L(s) = c₁(L) ∩ div_N(t) in A_k(X),

where div_L(s) and div_N(t) are the divisor cycles of the two sections of the situation. No parameter besides the situation remains: the two presentations by the family that Stacks.Chow.KeyFormulaSituation.firstChernClassCapOfInvertible_comm asks for are Stacks.Chow.KeyFormulaSituation.weilDivisorAlgebraicCycle_weilDivisorN_apply, read on ℱ for div_N(t) and on ℱ.swap for div_L(s).

theorem firstChernClassCapOfInvertible_comm_weilDivisorCycleN
    (hn : schemeDeltaDimension C p = ((k + 2 : ℤ) : EInt)) :
    firstChernClassCapOfInvertible C p k N (ℱ.swap.weilDivisorCycleN C p hn) =
      firstChernClassCapOfInvertible C p k L (ℱ.weilDivisorCycleN C p hn)

Stacks.Chow.firstChernClassCapOfInvertible_divisorOfMeromorphicSection_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/ChernCapCommutativity.lean, line 92.

Stacks 02TH. Let X be integral and locally of finite type over the base scheme S of chapter 42, with dim_δ(X) = n, let L and N be invertible 𝒪_X-modules, and let s and t be nonzero (that is, regular) meromorphic sections of L and N. Writing α = div_L(s) and β = div_N(t) for their divisor cycles of Stacks 02SJ (1),

c₁(N) ∩ α = c₁(L) ∩ β in CH_{n-2}(X).

The cycles of degree n - 1 are read in degree (n - 2) + 1, the source of the cap product CH_{(n-2)+1} → CH_{n-2}, by Stacks.Chow.cycleGroupOfEq. The proof is the key formula of Stacks 0AYC, through Stacks.Chow.firstChernClassCapOfInvertible_divisorCycle_comm.

theorem firstChernClassCapOfInvertible_divisorOfMeromorphicSection_comm (n : ℤ)
    (hn : schemeDeltaDimension C p = (n : EInt)) (L N : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property N]
    (s : AlgebraicGeometry.MeromorphicSection X.sheaf L)
    (hs : AlgebraicGeometry.IsRegularMeromorphicSection X.sheaf L s)
    (t : AlgebraicGeometry.MeromorphicSection X.sheaf N)
    (ht : AlgebraicGeometry.IsRegularMeromorphicSection X.sheaf N t) :
    firstChernClassCapOfInvertible C p (n - 2) N
        (cycleGroupOfEq (by ring) (divisorOfMeromorphicSectionCycle C p n hn L s hs)) =
      firstChernClassCapOfInvertible C p (n - 2) L
        (cycleGroupOfEq (by ring) (divisorOfMeromorphicSectionCycle C p n hn N t ht))

Stacks.Chow.firstChernClassCapOfInvertible_divisorCycle_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/ChernCapDischarge.lean, line 497.

Stacks 02TH. Let X be integral and locally of finite type over the base scheme S of chapter 42, of delta-dimension k + 2, let L and N be invertible modules on X and let s and t be nonzero meromorphic sections of L and N. Writing α = div_L(s) and β = div_N(t) for their divisor cycles of Stacks 02SJ (1),

c₁(N) ∩ α = c₁(L) ∩ β in A_k(X).

Nothing is assumed beyond the source's hypotheses: the family of prime divisors and the local generators of the situation of Stacks 0AYB are produced by Stacks.Chow.keyFormulaSituationOf, the key formula of Stacks 0AYC for it is Stacks.Chow.KeyFormulaSituation.keyFormula_toKeyFormulaData, the component rules of Stacks 02SO are the canonical ones of Stacks.Chow.firstChernClassCapOfInvertible, and the two divisor cycles are presented by the family because a prime divisor outside it carries no order of vanishing. The source states the conclusion in CH_{n-2}(X) for dim_δ(X) = n; here n = k + 2.

theorem firstChernClassCapOfInvertible_divisorCycle_comm
    (hn : schemeDeltaDimension C p = ((k + 2 : ℤ) : EInt)) (L N : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property N]
    {s : L.presheaf.stalk (genericPoint X)} (hs : s ≠ 0)
    {t : N.presheaf.stalk (genericPoint X)} (ht : t ≠ 0) :
    firstChernClassCapOfInvertible C p k N (divisorCycleOfInvertibleSection C p hn L s) =
      firstChernClassCapOfInvertible C p k L (divisorCycleOfInvertibleSection C p hn N t)

Tag 02TI, a lemma

Tag 02TI in the Stacks Project.

Stacks.Chow.firstChernCapFactorsEverywhere_iff_killsPrincipalDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCapRationalEquivalenceReduction.lean, line 230. The attribute's comment: “the vanishing reduced to one principal divisor on an integral scheme”.

Stacks 02TI, reduced to its integral case. The cap product with the first Chern class of an invertible module factors through rational equivalence, for every scheme locally of finite type over the base and every invertible module on it, exactly when it kills the principal divisor of a nonzero rational function on an integral scheme of delta-dimension k + 2.

The reverse implication is the reduction step of the source's proof of Stacks 02TI; the forward implication holds because div_Z(f) is rationally equivalent to zero on Z itself, which is Stacks 02RW. So the delivered content of this tag is the reduction, and what remains of the tag is its integral case — the source's appeal to Stacks 02TH.

theorem firstChernCapFactorsEverywhere_iff_killsPrincipalDivisor :
    FirstChernCapFactorsEverywhere C k ↔ FirstChernCapKillsPrincipalDivisor C k

Stacks.Chow.firstChernClassCap_eq_zero_of_keyFormula, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionCommutativity.lean, line 192. The attribute's comment: “the integral case α = div_X(f), granting the key formula 0AYC”.

The integral case of Stacks 02TI. On an integral scheme of delta-dimension k + 2, intersecting the principal divisor of a rational function with the first Chern class of an invertible module gives zero in A_k(X).

This is Stacks 02TH applied with the second invertible module the structure sheaf 𝒪_X and its meromorphic section the rational function f: the chosen generators of 𝒪_X at the generic points ξ_i are then units, so the restricted divisors div_{𝒪_{Z_i}}(t_i|_{Z_i}) vanish, which is the hypothesis hzeroN, while the orders ord_{B_i}(f) presenting div_𝒪(f) = div_X(f) need not. The resulting class c₁(𝒪_X) ∩ div_L(s) vanishes by Stacks.Chow.firstChernClassCap_trivialChernComponentCycleRule, the second half of Stacks 02SP.

The proof of Stacks 02TI reduces its general statement to this case by proper pushforward along ⨿ W_j ⟶ X, which needs Stacks 02SU and through it the proper pushforward of Chow classes of Stacks 0GU8 and 02S2. That reduction is the one step not available here, which is why the general vanishing is a hypothesis in StacksFrontier.AlgebraicGeometry.Chow.IntersectionCommutativity.ChernCapDescent.

theorem firstChernClassCap_eq_zero_of_keyFormula (hKey : D.KeyFormula C p)
    (hzeroN : ∀ i : D.Index, D.restrictedDivisorN i = 0)
    (chernL : FirstChernComponentCycleRule C p k)
    (hchernL : ∀ (i : D.Index) (hW : IsIntegral (D.component i).subscheme)
      (hDim : schemeDeltaDimension C ((D.component i).subschemeι ≫ p) = ((k + 1 : ℤ) : EInt)),
      (chernL (D.component i) hW hDim).1 = D.restrictedDivisorL i)
    (divL divN : CycleGroup C p (k + 1))
    (hdivL : ∀ x : X, divL.1 x = ∑ᶠ i, D.orderL i *
      (cycleAssociatedToClosedSubscheme C p (D.component i).subschemeι (k + 1)).1 x)
    (hdivN : ∀ x : X, divN.1 x = ∑ᶠ i, D.orderN i *
      (cycleAssociatedToClosedSubscheme C p (D.component i).subschemeι (k + 1)).1 x) :
    firstChernClassCap C p k chernL divN = 0

Stacks.Chow.firstChernClassCapOnChow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionCommutativity/ChernCapDescent.lean, line 112. The attribute's comment: “the descended operation, granting the vanishing and the rule of 02SO”.

Stacks 02TI. Intersection with the first Chern class, descended to Chow groups, c₁(L) ∩ - : A_{k+1}(X) ⟶ A_k(X).

def firstChernClassCapOnChow
    (h : FirstChernClassCapFactorsThroughRationalEquivalence C p k chern) :
    chowGroup C p (k + 1) →+ chowGroup C p k

Stacks.Chow.firstChernCapFactorsEverywhere, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/ChernCapFactors.lean, line 156. The attribute's comment: “the factoring itself, with no hypothesis: capping with the first Chern class of an invertible module kills every cycle rationally equivalent to zero, for every scheme locally of finite type over the base and every module”.

Stacks 02TI, with no hypothesis. Intersecting with the first Chern class of an invertible module kills every (k+1)-cycle rationally equivalent to zero, whatever the scheme locally of finite type over the base and whatever the module.

This is the reduction of Stacks.Chow.firstChernCapFactorsEverywhere_iff_killsPrincipalDivisor supplied with its integral case.

theorem firstChernCapFactorsEverywhere : FirstChernCapFactorsEverywhere C k

Stacks.Chow.firstChernClassCapChow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/ChernCapFactors.lean, line 176. The attribute's comment: “the descended operation c_1(L) cap - : A_{k+1}(X) ⟶ A_k(X) the factoring produces, with no hypothesis”.

Stacks 02TI. Intersection with the first Chern class of an invertible module, as an operation c₁(L) ∩ - : A_{k+1}(X) ⟶ A_k(X) on Chow groups.

def firstChernClassCapChow : chowGroup C p (k + 1) →+ chowGroup C p k

Tag 02TJ, a lemma

Tag 02TJ in the Stacks Project.

Stacks.Chow.firstChernClassCapOnChowOfInvertible_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCapCommutativityInvertible.lean, line 408. The attribute's comment: “granted hkills, Stacks 02TI in the reduced form Stacks.Chow.FirstChernCapKillsPrincipalDivisor — the vanishing of the cap product on one principal divisor on an integral scheme, to which Stacks.Chow.firstChernCapFactorsEverywhere_iff_killsPrincipalDivisor shows Stacks 02TI is equivalent with no hypothesis — in each of the two degrees the composite uses; and hcomm, Stacks 02TH for the restrictions of the two modules to the integral closed subschemes of X of delta-dimension k + 2, as an equality of classes in A_k(W), which is the case the source reduces to. Those are the only two inputs: the four component rules of Stacks 02SO and the four separate instances of Stacks 02TI carried by Stacks.Chow.firstChernClassCapOnChow_comm are all discharged here, and the passage from the integral components to every class is proved rather than assumed”.

Stacks 02TJ. For two invertible modules ℒ and 𝒩 on a scheme X locally of finite type over the base, intersecting successively with the two first Chern classes is independent of the order: c₁(ℒ) ∩ c₁(𝒩) ∩ α = c₁(𝒩) ∩ c₁(ℒ) ∩ α in A_k(X) for α ∈ A_{k+1+1}(X).

The four descended operations are those of Stacks.Chow.firstChernClassCapOnChowOfInvertible, so Stacks 02TI enters only through its reduced input hkills, and Stacks 02TH only through the class-level hypothesis hcomm; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.ChernCapCommutativityInvertible.

theorem firstChernClassCapOnChowOfInvertible_comm
    (hkills : ∀ j : ℤ, FirstChernCapKillsPrincipalDivisor C j)
    (hcomm : FirstChernCapCommutesOnIntegralComponents C p k L N)
    (α : chowGroup C p (k + 1 + 1)) :
    firstChernClassCapOnChowOfInvertible C k (hkills k) p L
        (firstChernClassCapOnChowOfInvertible C (k + 1) (hkills (k + 1)) p N α) =
      firstChernClassCapOnChowOfInvertible C k (hkills k) p N
        (firstChernClassCapOnChowOfInvertible C (k + 1) (hkills (k + 1)) p L α)

Stacks.Chow.firstChernClassCapOnChowOfInvertible_comm_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/FirstChernCommOfInvertible.lean, line 77. The attribute's comment: “the commutativity itself, with no hypotheses beyond the source's. The four descended cap products are Stacks.Chow.firstChernClassCapOnChowOfInvertible, and the Stacks 02TI input each of them needs — the reduced form Stacks.Chow.FirstChernCapKillsPrincipalDivisor, the vanishing of the cap product on one principal divisor on an integral scheme, to which Stacks.Chow.firstChernCapFactorsEverywhere_iff_killsPrincipalDivisor shows Stacks 02TI is equivalent — is supplied in both degrees by Stacks.Chow.firstChernCapKillsPrincipalDivisor, which proves it outright. Stacks 02TH for the restrictions of the two modules to the integral closed subschemes of X of delta-dimension k + 2, as an equality of classes in A_k(W), which is what the source reduces to, is Stacks.Chow.GenuineChern.firstChernCapCommutesOnIntegralComponents, which proves it out of the key formula of Stacks 0AYC. The four cycle-level rules of Stacks 02SO and the four separate instances of Stacks 02TI that Stacks.Chow.firstChernClassCapOnChow_comm takes as inputs are all theorems here, and the passage from the integral subschemes to every class is proved too”.

Stacks 02TJ. For two invertible modules ℒ and 𝒩 on a scheme X locally of finite type over the base, intersecting successively with the two first Chern classes is independent of the order: c₁(ℒ) ∩ c₁(𝒩) ∩ α = c₁(𝒩) ∩ c₁(ℒ) ∩ α in A_k(X) for α ∈ A_{k+1+1}(X).

The four descended operations are those of Stacks.Chow.firstChernClassCapOnChowOfInvertible, whose Stacks 02TI input is supplied by Stacks.Chow.firstChernCapKillsPrincipalDivisor in each of the two degrees, and Stacks 02TH enters through Stacks.Chow.GenuineChern.firstChernCapCommutesOnIntegralComponents; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.ChernCapCommutativityInvertible.

theorem firstChernClassCapOnChowOfInvertible_comm_unconditional
    (α : chowGroup C p (k + 1 + 1)) :
    firstChernClassCapOnChowOfInvertible C k (firstChernCapKillsPrincipalDivisor C k) p L
        (firstChernClassCapOnChowOfInvertible C (k + 1)
          (firstChernCapKillsPrincipalDivisor C (k + 1)) p N α) =
      firstChernClassCapOnChowOfInvertible C k (firstChernCapKillsPrincipalDivisor C k) p N
        (firstChernClassCapOnChowOfInvertible C (k + 1)
          (firstChernCapKillsPrincipalDivisor C (k + 1)) p L α)

Stacks.Chow.firstChernCapStepsCommute, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/TensorPowerSumsDischarge.lean, line 245. The attribute's comment: “the identity for the degree-raising steps Stacks.Chow.firstChernCapStep that the Chern class power-sum operators of Stacks 0F9B are built from, with no hypothesis: it is Stacks.Chow.GenuineChern.firstChernClassCapChow_comm, which is the tag itself with nothing carried, transported along the equality of degrees n - i = (n - (i+1)) + 1 that separates the two presentations of c_1(L) cap -”.

Stacks 02TJ in the form the power-sum operators consume, with no hypothesis. For two invertible modules the degree-raising operations c₁(A) ∩ - and c₁(B) ∩ - of Stacks.Chow.firstChernCapStep commute, in every degree.

This is Stacks.Chow.GenuineChern.firstChernClassCapChow_comm — Stacks 02TJ with no hypothesis beyond the ones the tag states — transported to the presentation A_{n-i}(X) ⟶ A_{n-(i+1)}(X) of the same operation by Stacks.Chow.firstChernCapStep_apply. It discharges every hcommLN-style hypothesis of StacksFrontier.AlgebraicGeometry.Chow.SplittingPrinciple.TensorChernClasses.

theorem firstChernCapStepsCommute (hA : InvertibleChernCapDescends C p A)
    (hB : InvertibleChernCapDescends C p B) :
    FirstChernCapStepsCommute C p n A B hA hB

Sources

• Section 42.28, Tag 02TG
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.firstChernClassCap_comm_of_keyFormula · Stacks.Chow.KeyFormulaSituation.firstChernClassCapOfInvertible_comm_weilDivisorCycleN · Stacks.Chow.firstChernClassCapOfInvertible_divisorOfMeromorphicSection_comm · Stacks.Chow.firstChernClassCapOfInvertible_divisorCycle_comm · Stacks.Chow.firstChernCapFactorsEverywhere_iff_killsPrincipalDivisor · Stacks.Chow.firstChernClassCap_eq_zero_of_keyFormula · Stacks.Chow.firstChernClassCapOnChow · Stacks.Chow.firstChernCapFactorsEverywhere

Section42.29 Gysin homomorphisms#

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

Tag 02T8, a definition

Tag 02T8 in the Stacks Project.

Stacks.Chow.gysinHomomorphismOfInvertible, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernComponent/ClassRule.lean, line 132. The attribute's comment: “Gysin homomorphism”.

The Gysin homomorphism of the zero scheme of a global section s of an invertible module: Stacks.Chow.gysinHomomorphism at the first Chern class component rule of L.

abbrev gysinHomomorphismOfInvertible : CycleGroup C p (k + 1) →+
    chowGroup C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k

Stacks.Chow.gysinHomomorphismOfInvertible_of_not_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernComponent/ClassRule.lean, line 146. The attribute's comment: “integral component not contained in the zero scheme”.

The Gysin image of an integral closed subscheme not contained in the zero scheme is the class of its scheme-theoretic intersection with that zero scheme.

theorem gysinHomomorphismOfInvertible_of_not_le (W : X.IdealSheafData)
    (hW : IsIntegral W.subscheme)
    (hDim : schemeDeltaDimension C (W.subschemeι ≫ p) = ((k + 1 : ℤ) : EInt))
    (h : ¬ Stacks.Divisors.zeroScheme X L s ≤ W) :
    gysinHomomorphismOfInvertible C p k L s
        (cycleAssociatedToClosedSubscheme C p W.subschemeι (k + 1)) =
      QuotientAddGroup.mk
        (cycleAssociatedToClosedSubscheme C
          ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p)
          ((W.comap (Stacks.Divisors.zeroScheme X L s).subschemeι).subschemeι) k)

Stacks.Chow.gysinHomomorphismOfInvertible_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InvertibleChernSpecialization.lean, line 151. The attribute's comment: “integral component contained in the zero scheme”.

The Gysin image of an integral closed subscheme contained in the zero scheme of s is the proper Chow pushforward into that zero scheme of the first Chern class of L|_W.

The instance of Stacks 02S2 that Stacks.Chow.properChowPushforward requires is discharged, the inclusion of W into the zero scheme being a closed immersion.

theorem gysinHomomorphismOfInvertible_of_le (W : X.IdealSheafData)
    (hW : IsIntegral W.subscheme)
    (hDim : schemeDeltaDimension C (W.subschemeι ≫ p) = ((k + 1 : ℤ) : EInt))
    (h : Stacks.Divisors.zeroScheme X L s ≤ W) :
    gysinHomomorphismOfInvertible C p k L s
        (cycleAssociatedToClosedSubscheme C p W.subschemeι (k + 1)) =
      properChowPushforward C (W.subschemeι ≫ p)
        ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p)
        (Scheme.IdealSheafData.inclusion h) (by simp) k
        (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
          (Scheme.IdealSheafData.inclusion h) C (W.subschemeι ≫ p)
          ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) (by simp) k)
        (firstChernComponentClass C p k L W hW hDim)

Stacks.Chow.gysinHomomorphismOfInvertible_finsum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InvertibleChernSpecialization.lean, line 168. The attribute's comment: “locally finite component formula”.

The locally finite component formula for the Gysin map of an invertible module.

theorem gysinHomomorphismOfInvertible_finsum {J : Type u} (W : J → X.IdealSheafData)
    (hW : ∀ j, IsIntegral (W j).subscheme)
    (hDim : ∀ j, schemeDeltaDimension C ((W j).subschemeι ≫ p) = ((k + 1 : ℤ) : EInt))
    (hLocal : LocallyFinite fun j ↦ ((W j).support : Set X)) (n : J → ℤ)
    (α : CycleGroup C p (k + 1))
    (hα : ∀ x : X, α.1 x = ∑ᶠ j : J, n j *
      (cycleAssociatedToClosedSubscheme C p (W j).subschemeι (k + 1)).1 x) :
    ∃ β : CycleGroup C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k,
      gysinHomomorphismOfInvertible C p k L s α = QuotientAddGroup.mk β ∧
      ∀ x : (Stacks.Divisors.zeroScheme X L s).subscheme,
        β.1 x = ∑ᶠ j : J, n j *
          (gysinComponentCycle C p k L s (firstChernComponentClass C p k L)
            (W j) (hW j) (hDim j)).1 x

Stacks.Chow.effectiveCartierIntersectionOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InvertibleChernSpecialization.lean, line 187. The attribute's comment: “intersection with an effective Cartier divisor”.

Intersection with the zero scheme of s, when that zero scheme is an effective Cartier divisor, read as a class on the ambient scheme: the Gysin map of the zero scheme followed by proper Chow pushforward along its closed immersion into X.

def effectiveCartierIntersectionOfInvertible
    (hD : Stacks.Divisors.IsEffectiveCartierDivisor (Stacks.Divisors.zeroScheme X L s)) :
    CycleGroup C p (k + 1) →+ chowGroup C p k

Tag 0B70, a remark

Tag 0B70 in the Stacks Project.

Stacks.Chow.VirtualNormalTriple, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 86. The attribute's comment: “the triple (D, N, σ): D locally principal, N an invertible O_D-module, σ a surjection from the inverse of N onto the pullback of the ideal sheaf of D”.

Remark 0B70. A triple (D, 𝒩, σ) on a scheme X: a locally principal closed subscheme i : D ⟶ X, an invertible 𝒪_D-module 𝒩 (the virtual normal bundle of D in X) and a surjection σ : 𝒩^{⊗ -1} ⟶ i^*ℐ_D of 𝒪_D-modules.

structure VirtualNormalTriple (X : Scheme.{u})

Stacks.Chow.VirtualNormalTriple.normalIsoOfIsEffectiveCartier, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 175. The attribute's comment: “footnote: if D is an effective Cartier divisor, then N is isomorphic to the restriction of O_X(D) to D”.

The footnote of Remark 0B70. If D is an effective Cartier divisor, then 𝒩 ≅ 𝒪_X(D)|_D.

def normalIsoOfIsEffectiveCartier :
    T.N ≅ (Scheme.Modules.pullback T.D.subschemeι).obj (divisorSheaf T.D)

Stacks.Chow.virtualNormalGysinOfIdeal_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 427. The attribute's comment: “the construction generalizes Definition 02T8: for D = Z(s) and N isomorphic to the restriction of L the two Gysin maps are equal”.

The construction generalizes Definition 02T8. For the zero scheme D = Z(s) of a section s of an invertible module ℒ, and any invertible 𝒪_D-module 𝒩 ≅ ℒ|_D, the Gysin map of (D, 𝒩) is the Gysin map of Definition 02T8.

theorem virtualNormalGysinOfIdeal_zeroScheme (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) (N : (Stacks.Divisors.zeroScheme X L s).subscheme.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible
      (Stacks.Divisors.zeroScheme X L s).subscheme.sheaf.obj
      (Stacks.Divisors.zeroScheme X L s).subscheme.ringCatSheaf.property N]
    (ψ : N ≅ (Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X L s).subschemeι).obj L) :
    virtualNormalGysinOfIdeal C p k (Stacks.Divisors.zeroScheme X L s) N =
      gysinHomomorphismOfInvertible C p k L s

Stacks.Chow.VirtualNormalTriple.gysin, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 476. The attribute's comment: “the Gysin homomorphism i^* from (k+1)-cycles on X to CH_k(D) of a triple”.

Remark 0B70. The Gysin homomorphism i^* : Z_{k+1}(X) ⟶ A_k(D) of a triple (D, 𝒩, σ).

def gysin : CycleGroup C p (k + 1) →+ chowGroup C (T.D.subschemeι ≫ p) k

Stacks.Chow.VirtualNormalTriple.gysin_of_not_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 482. The attribute's comment: “rule (1)(a) of Definition 02T8 for a triple: W not contained in D”.

Remark 0B70, rule (1)(a) of Definition 02T8 for a triple. For an integral closed subscheme W ⊆ X of delta-dimension k + 1 with W ⊄ D, i^*[W] = [D ∩ W]_k.

theorem gysin_of_not_le (W : X.IdealSheafData) (hW : IsIntegral W.subscheme)
    (hDim : schemeDeltaDimension C (W.subschemeι ≫ p) = ((k + 1 : ℤ) : EInt)) (h : ¬ T.D ≤ W) :
    T.gysin C p k (cycleAssociatedToClosedSubscheme C p W.subschemeι (k + 1)) =
      QuotientAddGroup.mk
        (cycleAssociatedToClosedSubscheme C (T.D.subschemeι ≫ p)
          ((W.comap T.D.subschemeι).subschemeι) k)

Stacks.Chow.VirtualNormalTriple.gysin_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 494. The attribute's comment: “rule (1)(b) of Definition 02T8 for a triple: W contained in D, with c_1(N|_W)”.

Remark 0B70, rule (1)(b) of Definition 02T8 for a triple. For an integral closed subscheme W ⊆ D of delta-dimension k + 1, i^*[W] = i'_*(c₁(𝒩|_W) ∩ [W]), where i' : W ⟶ D is the induced closed immersion.

theorem gysin_of_le (W : X.IdealSheafData) (hW : IsIntegral W.subscheme)
    (hDim : schemeDeltaDimension C (W.subschemeι ≫ p) = ((k + 1 : ℤ) : EInt)) (h : T.D ≤ W) :
    T.gysin C p k (cycleAssociatedToClosedSubscheme C p W.subschemeι (k + 1)) =
      properChowPushforward C (W.subschemeι ≫ p) (T.D.subschemeι ≫ p)
        (Scheme.IdealSheafData.inclusion h) (by simp) k
        (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
          (Scheme.IdealSheafData.inclusion h) C (W.subschemeι ≫ p) (T.D.subschemeι ≫ p)
          (by simp) k)
        (virtualNormalChernClass C p k T.D T.N W hW hDim h)

Stacks.Chow.VirtualNormalTriple.gysin_finsum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 508. The attribute's comment: “rule (2) of Definition 02T8 for a triple: locally finite sums”.

Remark 0B70, rule (2) of Definition 02T8 for a triple. For α = ∑ n_j [W_j] locally finite, i^*α = ∑ n_j i^*[W_j].

theorem gysin_finsum {J : Type u} (W : J → X.IdealSheafData)
    (hW : ∀ j, IsIntegral (W j).subscheme)
    (hDim : ∀ j, schemeDeltaDimension C ((W j).subschemeι ≫ p) = ((k + 1 : ℤ) : EInt))
    (hLocal : LocallyFinite (fun j ↦ ((W j).support : Set X))) (n : J → ℤ)
    (α : CycleGroup C p (k + 1))
    (hα : ∀ x : X, α.1 x = ∑ᶠ j : J, n j *
      (cycleAssociatedToClosedSubscheme C p (W j).subschemeι (k + 1)).1 x) :
    ∃ β : CycleGroup C (T.D.subschemeι ≫ p) k,
      T.gysin C p k α = QuotientAddGroup.mk β ∧
      ∀ x : T.D.subscheme, β.1 x = ∑ᶠ j : J, n j *
        (gysinComponentCycleOfIdeal C p k (virtualNormalChernRule C p k T.D T.N) T.D
          (W j) (hW j) (hDim j)).1 x

Stacks.Chow.VirtualNormalTriple.nonempty_normalIso_of_isEffectiveCartier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 526. The attribute's comment: “footnote: if D is an effective Cartier divisor, then N is isomorphic to the restriction of O_X(D) to D”.

The footnote of Remark 0B70. If D is an effective Cartier divisor, then 𝒩 ≅ 𝒪_X(D)|_D.

theorem nonempty_normalIso_of_isEffectiveCartier (hD : IsEffectiveCartierDivisor T.D) :
    Nonempty (T.N ≅ (Scheme.Modules.pullback T.D.subschemeι).obj (divisorSheaf T.D))

Stacks.Chow.VirtualNormalTriple.gysin_heq_of_zeroScheme_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 536. The attribute's comment: “the construction generalizes Definition 02T8: agreement when D = Z(s) and N is the restriction of L”.

Remark 0B70: the construction generalizes Definition 02T8. If D = Z(s) for a global section s of an invertible 𝒪_X-module ℒ and 𝒩 ≅ ℒ|_D, the Gysin map of the triple is the Gysin map of Definition 02T8 of (ℒ, s).

theorem gysin_heq_of_zeroScheme_eq (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) (hz : Stacks.Divisors.zeroScheme X L s = T.D)
    (ψ : T.N ≅ (Scheme.Modules.pullback T.D.subschemeι).obj L) :
    HEq (T.gysin C p k) (gysinHomomorphismOfInvertible C p k L s)

Stacks.Chow.VirtualNormalTriple.gysin_heq_divisorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 547. The attribute's comment: “agreement with Definition 02T8 when D is an effective Cartier divisor”.

Remark 0B70 at an effective Cartier divisor. If D is an effective Cartier divisor (so that 𝒩 ≅ 𝒪_X(D)|_D by the footnote), the Gysin map of the triple is the Gysin map of Definition 02T8 of (𝒪_X(D), 1_D), whose zero scheme is D.

theorem gysin_heq_divisorSheaf (hD : IsEffectiveCartierDivisor T.D) :
    HEq (T.gysin C p k)
      (gysinHomomorphismOfInvertible C p k (divisorSheaf T.D) (divisorSheafGlobalSection T.D))

Stacks.Chow.VirtualNormalTriple.chowPushforwardOfIso_gysinHomomorphismOfInvertible_divisorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 581. The attribute's comment: “agreement with Definition 02T8 when D is an effective Cartier divisor, as an identity of Chow classes”.

Remark 0B70 at an effective Cartier divisor, as an identity of Chow classes: the Gysin map of Definition 02T8 of (𝒪_X(D), 1_D), transported along Z(1_D) = D, is the Gysin map of the triple.

theorem chowPushforwardOfIso_gysinHomomorphismOfInvertible_divisorSheaf
    (hD : IsEffectiveCartierDivisor T.D) (α : CycleGroup C p (k + 1)) :
    chowPushforwardOfIso C
        ((Stacks.Divisors.zeroScheme X (divisorSheaf T.D)
          (divisorSheafGlobalSection T.D)).subschemeι ≫ p) (T.D.subschemeι ≫ p)
        (eqToHom (congrArg Scheme.IdealSheafData.subscheme
          (@zeroScheme_canonicalSection X T.D hD)))
        (by rw [← Category.assoc, eqToHom_subscheme_comp_subschemeι _ _
          (@zeroScheme_canonicalSection X T.D hD)]) k
        (@gysinHomomorphismOfInvertible C X p _ k (divisorSheaf T.D)
          (@isInvertible_divisorSheaf X T.D hD) (divisorSheafGlobalSection T.D) α) =
      T.gysin C p k α

Stacks.Chow.virtualNormalTriple_remark, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalTripleGysin.lean, line 611. The attribute's comment: “the whole remark: the footnote, the Gysin homomorphism of a triple with the rules of Definition 02T8, and its agreement with Definition 02T8”.

Remark 0B70, all of its assertions together. Let X be locally of finite type over the base of a Chow situation (Situation 02QL) and let (D, 𝒩, σ) be a triple: D a locally principal closed subscheme, 𝒩 an invertible 𝒪_D-module and σ : 𝒩^{⊗ -1} ⟶ i^*ℐ_D a surjection. Then: * (footnote) if D is an effective Cartier divisor, 𝒩 ≅ 𝒪_X(D)|_D, and every effective Cartier divisor carries such a triple; * the Gysin homomorphism i^* : Z_{k+1}(X) ⟶ A_k(D) of the triple obeys the rules of Definition 02T8 with 𝒩 in place of ℒ|_D: i^*[W] = [D ∩ W]_k for W ⊄ D, i^*[W] = i'_*(c₁(𝒩|_W) ∩ [W]) for W ⊆ D, and i^*(∑ n_j [W_j]) = ∑ n_j i^*[W_j]; * it generalizes Definition 02T8: for D = Z(s) and 𝒩 ≅ ℒ|_D it is the Gysin map of (ℒ, s), and for D an effective Cartier divisor it is the Gysin map of (𝒪_X(D), 1_D).

theorem virtualNormalTriple_remark (C : ChowSituation.{u}) {X : Scheme.{u}} (p : X ⟶ C.S)
    [LocallyOfFiniteType p] :
    (∀ T : VirtualNormalTriple X, IsEffectiveCartierDivisor T.D →
      Nonempty (T.N ≅ (Scheme.Modules.pullback T.D.subschemeι).obj (divisorSheaf T.D))) ∧
    (∀ D : X.IdealSheafData, IsEffectiveCartierDivisor D →
      ∃ T : VirtualNormalTriple X, T.D = D) ∧
    (∀ (k : ℤ) (T : VirtualNormalTriple X) (W : X.IdealSheafData), IsIntegral W.subscheme →
      schemeDeltaDimension C (W.subschemeι ≫ p) = ((k + 1 : ℤ) : EInt) →
      ¬ T.D ≤ W →
      T.gysin C p k (cycleAssociatedToClosedSubscheme C p W.subschemeι (k + 1)) =
        QuotientAddGroup.mk
          (cycleAssociatedToClosedSubscheme C (T.D.subschemeι ≫ p)
            ((W.comap T.D.subschemeι).subschemeι) k)) ∧
    (∀ (k : ℤ) (T : VirtualNormalTriple X) (W : X.IdealSheafData) (hW : IsIntegral W.subscheme)
      (hDim : schemeDeltaDimension C (W.subschemeι ≫ p) = ((k + 1 : ℤ) : EInt))
      (h : T.D ≤ W),
      T.gysin C p k (cycleAssociatedToClosedSubscheme C p W.subschemeι (k + 1)) =
        properChowPushforward C (W.subschemeι ≫ p) (T.D.subschemeι ≫ p)
          (Scheme.IdealSheafData.inclusion h) (by simp) k
          (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
            (Scheme.IdealSheafData.inclusion h) C (W.subschemeι ≫ p) (T.D.subschemeι ≫ p)
            (by simp) k)
          (virtualNormalChernClass C p k T.D T.N W hW hDim h)) ∧
    (∀ (k : ℤ) (T : VirtualNormalTriple X) {J : Type u} (W : J → X.IdealSheafData)
      (hW : ∀ j, IsIntegral (W j).subscheme)
      (hDim : ∀ j, schemeDeltaDimension C ((W j).subschemeι ≫ p) = ((k + 1 : ℤ) : EInt)),
      LocallyFinite (fun j ↦ ((W j).support : Set X)) → ∀ (n : J → ℤ)
      (α : CycleGroup C p (k + 1)),
      (∀ x : X, α.1 x = ∑ᶠ j : J, n j *
        (cycleAssociatedToClosedSubscheme C p (W j).subschemeι (k + 1)).1 x) →
      ∃ β : CycleGroup C (T.D.subschemeι ≫ p) k,
        T.gysin C p k α = QuotientAddGroup.mk β ∧
        ∀ x : T.D.subscheme, β.1 x = ∑ᶠ j : J, n j *
          (gysinComponentCycleOfIdeal C p k (virtualNormalChernRule C p k T.D T.N) T.D
            (W j) (hW j) (hDim j)).1 x) ∧
    (∀ (k : ℤ) (T : VirtualNormalTriple X) (L : X.Modules)
      [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
      (s : Γ(L, ⊤)), Stacks.Divisors.zeroScheme X L s = T.D →
      (T.N ≅ (Scheme.Modules.pullback T.D.subschemeι).obj L) →
      HEq (T.gysin C p k) (gysinHomomorphismOfInvertible C p k L s)) ∧
    (∀ (k : ℤ) (T : VirtualNormalTriple X) [IsEffectiveCartierDivisor T.D],
      HEq (T.gysin C p k)
        (gysinHomomorphismOfInvertible C p k (divisorSheaf T.D)
          (divisorSheafGlobalSection T.D)))

Tag 02T9, a lemma

Tag 02T9 in the Stacks Project.

Stacks.Chow.properChowPushforward_gysinHomomorphismOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinPushforwardChernCap.lean, line 255.

Stacks 02T9. Pushing the Gysin class of the zero scheme i : D = Z(s) ⟶ X forward to X is capping with the first Chern class of L: i_* i^* α = c₁(L) ∩ α in A_k(X) for every α ∈ Z_{k+1}(X).

The vanishing of Stacks 02S2 that Stacks.Chow.properChowPushforward requires is supplied, not assumed, the zero scheme being a closed subscheme of X.

theorem properChowPushforward_gysinHomomorphismOfInvertible (α : CycleGroup C p (k + 1)) :
    properChowPushforward C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) p
        (Stacks.Divisors.zeroScheme X L s).subschemeι rfl k
        (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
          (Stacks.Divisors.zeroScheme X L s).subschemeι C
          ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) p rfl k)
        (gysinHomomorphismOfInvertible C p k L s α) =
      firstChernClassCapOfInvertible C p k L α

Stacks.Chow.effectiveCartierIntersection_divisorSheaf_eq_firstChernClassCapOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinPushforwardChernCap.lean, line 388. The attribute's comment: “in particular”.

Stacks 02T9, the "in particular" clause for a given effective Cartier divisor. For an effective Cartier divisor D on X, intersection with D — taken through the canonical section 1_D of 𝒪_X(D), whose zero scheme is D — is capping with c₁(𝒪_X(D)).

The effective Cartier hypothesis of Stacks.Chow.effectiveCartierIntersection is carried but unused by that construction, so transporting it along Z(1_D) = D (Stacks 01X0) costs nothing.

theorem effectiveCartierIntersection_divisorSheaf_eq_firstChernClassCapOfInvertible
    (D : X.IdealSheafData) [hD : Stacks.Divisors.IsEffectiveCartierDivisor D]
    (α : CycleGroup C p (k + 1)) :
    effectiveCartierIntersectionOfInvertible C p k (Stacks.Divisors.divisorSheaf D)
        (Stacks.Divisors.divisorSheafGlobalSection D)
        (isEffectiveCartierDivisor_zeroScheme_divisorSheaf D) α =
      firstChernClassCapOfInvertible C p k (Stacks.Divisors.divisorSheaf D) α

Tag 02TB, a lemma

Tag 02TB in the Stacks Project.

Stacks.Chow.gysinHomomorphismOfInvertible_cycleAssociatedToClosedSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinCartierIntersection/ClosedSubschemeCycle.lean, line 712. The attribute's comment: “part (1)”.

Intersecting a closed subscheme properly with a Cartier zero scheme computes its Gysin class.

theorem gysinHomomorphismOfInvertible_cycleAssociatedToClosedSubscheme
    (C : ChowSituation.{u}) {X : Scheme.{u}}
    (p : X ⟶ C.S) [LocallyOfFiniteType p] (k : ℤ)
    (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : L.sections) (Z : X.IdealSheafData)
    (hZ : schemeDeltaDimension C (Z.subschemeι ≫ p) ≤
      ((k + 1 : ℤ) : EInt))
    (hDZ : Stacks.Divisors.IsEffectiveCartierDivisor
      ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).comap Z.subschemeι)) :
    gysinHomomorphismOfInvertible C p k L (s.eval (.op ⊤))
        (cycleAssociatedToClosedSubscheme C p Z.subschemeι (k + 1)) =
      QuotientAddGroup.mk
        (cycleAssociatedToClosedSubscheme C
          ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)
          ((Z.comap (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι).subschemeι)
            k)

Stacks.Chow.schemeDeltaDimension_pullback_support_le_of_mono_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinCoherentSheaf.lean, line 1081. The attribute's comment: “part (2): support bound”.

The support of a coherent sheaf on which a Cartier section is regular loses at least one dimension upon restriction to the zero scheme.

theorem schemeDeltaDimension_pullback_support_le_of_mono_section
    (C : ChowSituation.{u}) {X : Scheme.{u}}
    (p : X ⟶ C.S) [LocallyOfFiniteType p] (k : ℤ)
    (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : L.sections) (F : X.Modules) [F.IsCoherent]
    (hF : schemeDeltaDimension C
      ((reducedSupport F).subschemeι ≫ p) ≤
        ((k + 1 : ℤ) : EInt))
    (hs : Mono (((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X.toRingedSpace)).presheaf, ((X.toRingedSpace)).IsSheaf⟩)).map (((𝟙 F), (L.unitHomEquiv.symm s)) : (_, _) ⟶ (_, _))))) :
    schemeDeltaDimension C
      ((@reducedSupport _
          ((Scheme.Modules.pullback
            (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι).obj F)
          (@AlgebraicGeometry.isCoherent_pullback
            (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subscheme X
            (LocallyOfFiniteType.isLocallyNoetherian
              ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p))
            (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι F
            inferInstance)).subschemeι ≫
        (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p) ≤ (k : EInt)

Stacks.Chow.gysinHomomorphismOfInvertible_cycleAssociatedToCoherentSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinCoherentSheaf.lean, line 1121. The attribute's comment: “part (2): Gysin formula”.

Gysin pullback of the associated cycle of a coherent sheaf on which the section is regular is the associated cycle of its restriction.

theorem gysinHomomorphismOfInvertible_cycleAssociatedToCoherentSheaf
    (C : ChowSituation.{u}) {X : Scheme.{u}}
    (p : X ⟶ C.S) [LocallyOfFiniteType p] (k : ℤ)
    (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : L.sections) (F : X.Modules) [F.IsCoherent]
    (hF : schemeDeltaDimension C
      ((reducedSupport F).subschemeι ≫ p) ≤
        ((k + 1 : ℤ) : EInt))
    (hs : Mono (((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X.toRingedSpace)).presheaf, ((X.toRingedSpace)).IsSheaf⟩)).map (((𝟙 F), (L.unitHomEquiv.symm s)) : (_, _) ⟶ (_, _))))) :
    gysinHomomorphismOfInvertible C p k L (s.eval (.op ⊤))
        (cycleAssociatedToCoherentSheaf C p F
          (k + 1) hF) =
      QuotientAddGroup.mk
        (@cycleAssociatedToCoherentSheaf _ C
          ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p) inferInstance
          ((Scheme.Modules.pullback
            (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι).obj F)
          (@AlgebraicGeometry.isCoherent_pullback
            (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subscheme X
            (LocallyOfFiniteType.isLocallyNoetherian
              ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p))
            (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι F
            inferInstance) k
          (by
            exact schemeDeltaDimension_pullback_support_le_of_mono_section
              C p k L s F hF hs))

Tag 0B6Z, a remark

Tag 0B6Z in the Stacks Project.

Stacks.Chow.gysinCycleMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinTrivialRestriction.lean, line 295. The attribute's comment: “the canonical map on cycles”.

The canonical Gysin map on cycles i^* : Z_{k+1}(X) ⟶ Z_k(D) attached to a section s of an invertible module whose restriction to the zero scheme D = Z(s) is trivial: the extension of the two rules of Stacks.Chow.gysinCycleMapComponent over locally finite presentations by integral closed subschemes. It does not depend on a trivialization of L|_D.

def gysinCycleMap
    (_htriv : AlgebraicGeometry.SheafOfModules.IsTrivial
      (Stacks.Divisors.zeroScheme X L s).subscheme.sheaf.obj
      (Stacks.Divisors.zeroScheme X L s).subscheme.ringCatSheaf.property
      ((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X L s).subschemeι).obj L)) :
    CycleGroup C p (k + 1) →+
      CycleGroup C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k

Stacks.Chow.gysinCycleMap_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinTrivialRestriction.lean, line 312. The attribute's comment: “vanishing on integral closed subschemes contained in the zero scheme”.

An integral closed subscheme contained in the zero scheme has zero image under the canonical map on cycles.

theorem gysinCycleMap_of_le (W : X.IdealSheafData) (hW : IsIntegral W.subscheme)
    (hDim : schemeDeltaDimension C (W.subschemeι ≫ p) = ((k + 1 : ℤ) : EInt))
    (h : Stacks.Divisors.zeroScheme X L s ≤ W) :
    gysinCycleMap C p k L s htriv
      (cycleAssociatedToClosedSubscheme C p W.subschemeι (k + 1)) = 0

Stacks.Chow.gysinCycleMap_of_not_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinTrivialRestriction.lean, line 325. The attribute's comment: “agreement with Stacks 02T8 off the zero scheme”.

The canonical map on cycles sends an integral closed subscheme W not contained in D to the fundamental cycle of the scheme-theoretic intersection W ∩ D.

theorem gysinCycleMap_of_not_le (W : X.IdealSheafData) (hW : IsIntegral W.subscheme)
    (hDim : schemeDeltaDimension C (W.subschemeι ≫ p) = ((k + 1 : ℤ) : EInt))
    (h : ¬ Stacks.Divisors.zeroScheme X L s ≤ W) :
    gysinCycleMap C p k L s htriv
        (cycleAssociatedToClosedSubscheme C p W.subschemeι (k + 1)) =
      cycleAssociatedToClosedSubscheme C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p)
        ((W.comap (Stacks.Divisors.zeroScheme X L s).subschemeι).subschemeι) k

Stacks.Chow.isGysinCycleMap_gysinCycleMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinTrivialRestriction.lean, line 356. The attribute's comment: “the locally finite component formula”.

The canonical map on cycles satisfies the locally finite component formula.

theorem isGysinCycleMap_gysinCycleMap :
    IsGysinCycleMap C p k L s (gysinCycleMap C p k L s htriv)

Stacks.Chow.eq_gysinCycleMap_of_isGysinCycleMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinTrivialRestriction.lean, line 365. The attribute's comment: “canonicity”.

Any additive map Z_{k+1}(X) ⟶ Z_k(D) satisfying the locally finite component formula is the canonical map on cycles.

theorem eq_gysinCycleMap_of_isGysinCycleMap
    (F : CycleGroup C p (k + 1) →+
      CycleGroup C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k)
    (hF : IsGysinCycleMap C p k L s F) :
    F = gysinCycleMap C p k L s htriv

Tag 0B6Y, a remark

Tag 0B6Y in the Stacks Project.

Stacks.Divisors.zeroScheme_pullback_comp_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ZeroSchemePullback/BaseChangeComparison.lean, line 68. The attribute's comment: “the zero scheme of a section pulled back along a composite does not depend on the factorization”.

Stacks 0B6Y. The zero scheme of a section pulled back to A depends only on the morphism A ⟶ T, not on a factorization of it: two factorizations q₁ ≫ q₂ = r₁ ≫ r₂ give equal zero schemes, both being the inverse image of Z(s) along that morphism.

theorem zeroScheme_pullback_comp_comp {A B B' T : Scheme.{u}} (q₁ : A ⟶ B) (q₂ : B ⟶ T)
    (r₁ : A ⟶ B') (r₂ : B' ⟶ T) (h : q₁ ≫ q₂ = r₁ ≫ r₂) (L : T.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible T.sheaf.obj T.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) :
    zeroScheme A ((Scheme.Modules.pullback q₁).obj ((Scheme.Modules.pullback q₂).obj L))
        (AlgebraicGeometry.pullbackGlobalSections q₁ ((Scheme.Modules.pullback q₂).obj L)
          (AlgebraicGeometry.pullbackGlobalSections q₂ L s)) =
      zeroScheme A ((Scheme.Modules.pullback r₁).obj ((Scheme.Modules.pullback r₂).obj L))
        (AlgebraicGeometry.pullbackGlobalSections r₁ ((Scheme.Modules.pullback r₂).obj L)
          (AlgebraicGeometry.pullbackGlobalSections r₂ L s))

Stacks.Divisors.zeroScheme_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ZeroSchemePullback/Basic.lean, line 109. The attribute's comment: “the pulled-back zero scheme”.

Stacks 0B6Y. The zero scheme of the pulled-back section is the scheme-theoretic inverse image of the zero scheme: Z(f^* s) = f⁻¹(Z(s)) as quasi-coherent ideal sheaves on X'.

Together with AlgebraicGeometry.Scheme.IdealSheafData.comapIso and its two projection identities this is the cartesian square Z(f^* s) ≅ X' ×_X Z(s) of the tag.

theorem zeroScheme_pullback {X X' : Scheme.{u}} (f : X' ⟶ X) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) :
    zeroScheme X' ((Scheme.Modules.pullback f).obj L) (pullbackGlobalSections f L s) =
      (zeroScheme X L s).comap f

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.IdealSheafData.comapIso registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Chow/ZeroSchemePullback/Basic.lean, line 159 (StacksFrontier): “the cartesian square”. References: EGA IV (19.4.1), “more general”.
• AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fst registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Chow/ZeroSchemePullback/Basic.lean, line 161 (StacksFrontier): “the pulled-back inclusion”. References: EGA I (4.4.1), “closed case”.
• AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_snd registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Chow/ZeroSchemePullback/Basic.lean, line 164 (StacksFrontier): “the map to the original zero scheme”.

Tag 02TA, a lemma

Tag 02TA in the Stacks Project.

Stacks.Chow.canonicalGysinSystem_isNaturalUnderInverseIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FirstChernClassCanonical.lean, line 370. The attribute's comment: “the inverse-isomorphism case of the naturality of the Gysin operation, for the canonical Gysin system of Stacks 02TO, with no hypothesis”.

The canonical Gysin system is natural under inverse isomorphisms: the inverse-isomorphism case of the naturality of the Gysin operation.

theorem canonicalGysinSystem_isNaturalUnderInverseIso (C : ChowSituation.{u}) :
    (canonicalGysinSystem C).IsNaturalUnderInverseIso

Stacks.Chow.canonicalGysinSystem_isNaturalUnderBaseChangeIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FirstChernClassCanonical.lean, line 378. The attribute's comment: “the base-change-isomorphism case of the naturality of the Gysin operation, for the canonical Gysin system of Stacks 02TO, with no hypothesis”.

The canonical Gysin system is natural under base-change isomorphisms: the base-change-isomorphism case of the naturality of the Gysin operation.

theorem canonicalGysinSystem_isNaturalUnderBaseChangeIso (C : ChowSituation.{u}) :
    (canonicalGysinSystem C).IsNaturalUnderBaseChangeIso

Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderBaseChangeIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/GysinSystemOfInvertible.lean, line 101. The attribute's comment: “the isomorphism case of the naturality of the Gysin operation of a Gysin system, for an invertible module pulled back from a test scheme to both schemes -- the form the Gysin axiom of a bivariant class quantifies over -- with no hypothesis”.

The Gysin system of the first Chern class rule of an invertible module is natural under pushforward along an isomorphism u : A ⟶ B of two schemes over a test scheme carrying the module, the module on A and on B being its pullbacks from the test scheme.

theorem gysinSystemOfInvertible_isNaturalUnderBaseChangeIso (C : ChowSituation.{u}) :
    (gysinSystemOfInvertible C).IsNaturalUnderBaseChangeIso

Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpensRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantDisjoint/PieceGysinSystemOfInvertible.lean, line 425. The attribute's comment: “the open-immersion case of the naturality of the Gysin operation of a Gysin system, for an invertible module on the ambient scheme: restriction along an open immersion over the base carries the Gysin map of Z(s) to the Gysin map of Z(u^*s) across the square of Remark 0B6Y, with no hypothesis”.

The open-immersion case of Stacks 02TA for the Gysin operation of a Gysin system, with the module on the ambient scheme. The Gysin system of the first Chern class rule of an invertible module is natural under restriction along an open immersion over the base, with no hypothesis.

Its Gysin operation is Stacks.Chow.gysinHomomorphismOnChowOfInvertible, so this is Stacks.Chow.chowGroupRestrict_gysinHomomorphismOnChowOfInvertible_of_eq, the open-immersion case of Stacks 0B71 at that map, after the quantified open immersion of the two zero schemes is identified with the morphism of Remark 0B6Y by Stacks.Chow.eq_zeroSchemePullbackHom.

theorem gysinSystemOfInvertible_isNaturalUnderOpensRestriction (C : ChowSituation.{u}) :
    (gysinSystemOfInvertible C).IsNaturalUnderOpensRestriction

Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantDisjoint/PieceGysinSystemOfInvertible.lean, line 465. The attribute's comment: “the open-immersion case of the naturality of the Gysin operation of a Gysin system, for an invertible module pulled back from a test scheme to both schemes -- the form the Gysin axiom of a bivariant class quantifies over -- with no hypothesis”.

The open-immersion case of Stacks 02TA for the Gysin operation of a Gysin system. The Gysin system of the first Chern class rule of an invertible module is natural under restriction along an open immersion u : A ⟶ B of schemes over a test scheme carrying the module, with no hypothesis.

The module on A is the pullback of the module on the test scheme, not the pullback along u of the module on B, so this is not the ambient-module form Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpensRestriction but its composite with the comparison of the two spellings, Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderPullbackComp: the quantified open immersion of the two zero schemes factors as the transport along Stacks.Chow.zeroScheme_pullback_pullback followed by the morphism of Remark 0B6Y, uniquely because the closed immersion of the zero scheme downstairs is a monomorphism.

theorem gysinSystemOfInvertible_isNaturalUnderOpenImmersion (C : ChowSituation.{u}) :
    (gysinSystemOfInvertible C).IsNaturalUnderOpenImmersion

Stacks.Chow.GenuineChern.gysinSystemOfInvertible_isNaturalUnderInverseIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/InverseIsoGysin.lean, line 64. The attribute's comment: “the inverse-isomorphism case of the naturality of the Gysin operation of a Gysin system, for the system of the first Chern class rule of an invertible module”.

The isomorphism case of Stacks 02TA for the Gysin system of the first Chern class rule, with the invertible module on the source of the isomorphism: for an isomorphism u : A ⟶ B over the base with inverse w, an invertible module L on A, a section s of it and a morphism j of zero schemes lying over u, the Gysin map of (w^*L, w^*s) on B applied to u_*α is j_* of the Gysin map of (L, s) on A applied to α.

Stacks 02TA for the proper morphism w and the module L on A itself, Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderProperPushforward, gives i^* w_* β = (j'')_* (i')^* β for the morphism j'' of Remark 0B6Y; at β = u_* α the left side collapses since u ≫ w = 𝟙, and j'' ≫ j = 𝟙 because j lies over u and a closed immersion is a monomorphism.

theorem gysinSystemOfInvertible_isNaturalUnderInverseIso (C : ChowSituation.{u}) :
    (gysinSystemOfInvertible C).IsNaturalUnderInverseIso

Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderProperPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/ProperPushforwardGysinSystem.lean, line 121. The attribute's comment: “the naturality of the Gysin operation of a Gysin system under pushforward along a general proper morphism”.

The Gysin system of the first Chern class rule of an invertible module is natural under pushforward along an arbitrary proper morphism over the base.

theorem gysinSystemOfInvertible_isNaturalUnderProperPushforward (C : ChowSituation.{u}) :
    (gysinSystemOfInvertible C).IsNaturalUnderProperPushforward

Stacks.Chow.gysinHomomorphismOfInvertible_properPushforward_of_gysinCompatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/ProperPushforwardInvertible.lean, line 274. The attribute's comment: “the identity i^ f_ α' = g_ (i')^ α' in A_k(Z(s)) over the square of Remark 0B6Y, for the Gysin map of an invertible module and a global section, with no hypothesis beyond properness of f and the commutativity of f over the base”.

Stacks 02TA. Gysin pullback through the zero scheme of a global section of an invertible module commutes with proper pushforward across the square of Remark 0B6Y:

i^* f_* α' = g_* (i')^* α' in A_k(Z(s)), for every α' ∈ Z_{k+1}(X').

Both Gysin maps are Stacks.Chow.gysinHomomorphismOfInvertible, functions of the invertible module and the section alone; the morphism g of Remark 0B6Y is Stacks.Chow.zeroSchemePullbackHom; and the instance of Stacks 02S2 that Stacks.Chow.properChowPushforward requires along g is supplied by Stacks.Chow.properPushforwardFactorsThroughRationalEquivalence. Nothing is assumed beyond the properness of f and the commutativity of f over the base.

Both sides are classes of cycles on Z(s), and the two cycles are rationally equivalent by Stacks.Chow.rationallyEquivalent_gysinRule_extendCycleGroup_properPushforward.

theorem gysinHomomorphismOfInvertible_properPushforward_of_gysinCompatible [IsProper f]
    (hf : f ≫ p = p') (α : CycleGroup C p' (k + 1)) :
    gysinHomomorphismOfInvertible C p k L s (properPushforward C p' p f hf (k + 1) α) =
      properChowPushforward C ((pullbackZeroScheme f L s).subschemeι ≫ p')
        ((zeroScheme X L s).subschemeι ≫ p) (zeroSchemePullbackHom f L s)
        (zeroSchemePullbackHom_comp f L s C p p' hf) k
        (properPushforwardFactorsThroughRationalEquivalence C
          ((pullbackZeroScheme f L s).subschemeι ≫ p')
          ((zeroScheme X L s).subschemeι ≫ p) (zeroSchemePullbackHom f L s)
          (zeroSchemePullbackHom_comp f L s C p p' hf) k)
        (gysinHomomorphismOfInvertible C p' k ((Scheme.Modules.pullback f).obj L)
          (AlgebraicGeometry.pullbackGlobalSections f L s) α)

Tag 0B71, a lemma

Tag 0B71 in the Stacks Project.

Stacks.Chow.gysinHomomorphismOfInvertible_flatPullback_cycleAssociatedToClosedSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/FlatPullbackInvertible.lean, line 220. The attribute's comment: “closed subscheme meeting the zero scheme properly; 02S1 along g carried”.

Stacks 0B71 on the fundamental cycle of a closed subscheme meeting the zero scheme properly. For a closed subscheme Z ⊆ X of delta-dimension at most k + 1 whose intersection with D = Z(s) is an effective Cartier divisor on Z, and whose inverse image f^{-1}Z meets D' = Z(f^*s) in the same way,

(i')^* f^* [Z]_{k+1} = g^* i^* [Z]_{k+1} in CH_{k+r}(D').

Here i^* and (i')^* are the Gysin maps Stacks.Chow.gysinHomomorphismOfInvertible of Stacks 02T8 for (L, s) and for (f^*L, f^*s), f^* is the flat pullback of cycles of Stacks 02RB, and g^* is the flat pullback on Chow groups of Stacks 0FVK along the comparison morphism Stacks.Chow.zeroSchemePullbackHom of Remark 0B6Y, whose flatness and relative dimension are supplied by the cartesian square and are not hypotheses. No first Chern class component rule is a parameter, and the invertibility of f^*L is an instance.

This is the first case of the source's proof, for an arbitrary closed subscheme rather than only an integral one. Carried: the vanishing of Stacks 02S1 along g, without which the right hand side does not exist, and the five side conditions of Stacks 02TB (1) and Stacks 02RB at the two schemes of the square; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.Gysin42.FlatPullbackInvertible.

theorem gysinHomomorphismOfInvertible_flatPullback_cycleAssociatedToClosedSubscheme
    (Z : X.IdealSheafData)
    (hZ : schemeDeltaDimension C (Z.subschemeι ≫ p) ≤ ((k + 1 : ℤ) : EInt))
    (hDZ : Stacks.Divisors.IsEffectiveCartierDivisor
      ((Stacks.Divisors.zeroScheme X L s).comap Z.subschemeι))
    (hZ' : schemeDeltaDimension C ((Z.comap f).subschemeι ≫ (f ≫ p)) ≤
      ((k + (r : ℤ) + 1 : ℤ) : EInt))
    (hDZ' : Stacks.Divisors.IsEffectiveCartierDivisor
      ((pullbackZeroScheme f L s).comap (Z.comap f).subschemeι))
    (hZD : schemeDeltaDimension C
      ((Z.comap (Stacks.Divisors.zeroScheme X L s).subschemeι).subschemeι ≫
        ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p)) ≤ (k : EInt))
    (hfac : FlatPullbackFactorsThroughRationalEquivalence C
      ((pullbackZeroScheme f L s).subschemeι ≫ (f ≫ p))
      ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) (zeroSchemePullbackHom f L s)
      (zeroSchemePullbackHom_comp f L s C p (f ≫ p) rfl) r
      (relativeDimension_zeroSchemePullbackHom f L s r hf) k) :
    gysinHomomorphismOfInvertible C (f ≫ p) (k + (r : ℤ))
        ((Scheme.Modules.pullback f).obj L) (pullbackGlobalSections f L s)
        ((show k + 1 + (r : ℤ) = k + (r : ℤ) + 1 by omega) ▸
          flatPullback C (f ≫ p) p f rfl r hf (k + 1)
            (cycleAssociatedToClosedSubscheme C p Z.subschemeι (k + 1))) =
      flatPullbackChow C ((pullbackZeroScheme f L s).subschemeι ≫ (f ≫ p))
        ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) (zeroSchemePullbackHom f L s)
        (zeroSchemePullbackHom_comp f L s C p (f ≫ p) rfl) r
        (relativeDimension_zeroSchemePullbackHom f L s r hf) k hfac
        (gysinHomomorphismOfInvertible C p k L s
          (cycleAssociatedToClosedSubscheme C p Z.subschemeι (k + 1)))

Stacks.Chow.gysinHomomorphismOfInvertible_flatPullback_of_invertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/FlatPullbackRationallyCompatible.lean, line 1260. The attribute's comment: “the Gysin map commutes with flat pullback, (i')^ f^ = g^ i^ on A_{k+r}(D'), with no hypothesis: the component identity is replaced by its rational-equivalence form, proved here, and the vanishing of 02S1 along g by the general theorem”.

Stacks 0B71 for an arbitrary cycle at the Gysin map of an invertible module, with no hypothesis. Gysin pullback through the zero scheme of a section of an invertible module commutes with flat pullback:

(i')^* f^* α = g^* i^* α in CH_{k+r}(D'), for every α ∈ Z_{k+1}(X).

This is Stacks.Chow.gysinHomomorphismOfInvertible_flatPullback with both of its remaining hypotheses discharged: the vanishing of Stacks 02S1 along g is Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_general, and the identity on integral components is replaced by its rational-equivalence form Stacks.Chow.gysinRationallyCompatibleWithFlatPullback_invertible, which is proved here. Both Gysin maps are Stacks.Chow.gysinHomomorphismOfInvertible, no component rule is a parameter, the invertibility of f^*L is an instance, and g is the canonical comparison morphism of Remark 0B6Y.

theorem gysinHomomorphismOfInvertible_flatPullback_of_invertible (α : CycleGroup C p (k + 1)) :
    gysinHomomorphismOfInvertible C (f ≫ p) (k + (r : ℤ)) ((Scheme.Modules.pullback f).obj L)
        (AlgebraicGeometry.pullbackGlobalSections f L s)
        ((show k + 1 + (r : ℤ) = k + (r : ℤ) + 1 by omega) ▸
          flatPullback C (f ≫ p) p f rfl r hf (k + 1) α) =
      flatPullbackChow C ((pullbackZeroScheme f L s).subschemeι ≫ (f ≫ p))
        ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) (zeroSchemePullbackHom f L s)
        (zeroSchemePullbackHom_comp f L s C p (f ≫ p) rfl) r
        (relativeDimension_zeroSchemePullbackHom f L s r hf) k
        (flatPullbackFactorsThroughRationalEquivalence_general C
          ((pullbackZeroScheme f L s).subschemeι ≫ (f ≫ p))
          ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) (zeroSchemePullbackHom f L s)
          (zeroSchemePullbackHom_comp f L s C p (f ≫ p) rfl) r
          (relativeDimension_zeroSchemePullbackHom f L s r hf) k)
        (gysinHomomorphismOfInvertible C p k L s α)

Sources

• Section 42.29, Tag 02T7
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.gysinHomomorphismOfInvertible · Stacks.Chow.gysinHomomorphismOfInvertible_of_not_le · Stacks.Chow.gysinHomomorphismOfInvertible_of_le · Stacks.Chow.gysinHomomorphismOfInvertible_finsum · Stacks.Chow.effectiveCartierIntersectionOfInvertible · Stacks.Chow.VirtualNormalTriple · Stacks.Chow.VirtualNormalTriple.normalIsoOfIsEffectiveCartier · Stacks.Chow.virtualNormalGysinOfIdeal_zeroScheme

Section42.30 Gysin homomorphisms and rational equivalence#

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

Tag 02TM, a lemma

Tag 02TM in the Stacks Project.

Stacks.Chow.effectiveCartierIntersection_eq_firstChernClassCap_of_keyFormula, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/ChernCapDivisor.lean, line 151. The attribute's comment: “after pushforward along E ⟶ X, granting the key formula 0AYC”.

Stacks 02TM, pushed forward to the ambient scheme. Let X be integral of delta-dimension k + 2, let E be an effective Cartier divisor on X and let N be an invertible module with a nonzero meromorphic section t. Then intersecting div_N(t) with E agrees with capping the fundamental cycle [E]_{k+1} with the first Chern class of N, in A_k(X).

This is the identity i^* div_N(t) = c₁(N|_E) ∩ [E]_{k+1} of the source after pushing forward along the closed immersion i : E ⟶ X, the right hand side being read on X through Stacks 02SU; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.Gysin42.ChernCapDivisor.

Intersection with E is capping with c₁(𝒪_X(E)) by Stacks 02T9, and the fundamental cycle [E]_{k+1} is the divisor cycle of the canonical section 1_E of 𝒪_X(E), presented by the family {Z_i} of the key formula through hfundamentalCycle. So the identity is the commutativity of Stacks 02TH for the pair (𝒪_X(E), N).

theorem effectiveCartierIntersection_eq_firstChernClassCap_of_keyFormula
    (hn : schemeDeltaDimension C p = ((k + 2 : ℤ) : EInt)) (E : X.IdealSheafData)
    [Stacks.Divisors.IsEffectiveCartierDivisor E] (D : KeyFormulaData X)
    (hKey : D.KeyFormula C p) (chernN : FirstChernComponentCycleRule C p k)
    (hchernE : ∀ (i : D.Index) (hW : IsIntegral (D.component i).subscheme)
      (hDim : schemeDeltaDimension C ((D.component i).subschemeι ≫ p) = ((k + 1 : ℤ) : EInt)),
      (firstChernComponentCycleRule C p k (Stacks.Divisors.divisorSheaf E)
        (D.component i) hW hDim).1 = D.restrictedDivisorL i)
    (hchernN : ∀ (i : D.Index) (hW : IsIntegral (D.component i).subscheme)
      (hDim : schemeDeltaDimension C ((D.component i).subschemeι ≫ p) = ((k + 1 : ℤ) : EInt)),
      (chernN (D.component i) hW hDim).1 = D.restrictedDivisorN i)
    (fundamentalCycle divN : CycleGroup C p (k + 1))
    (hfundamentalCycle : ∀ x : X, fundamentalCycle.1 x = ∑ᶠ i, D.orderL i *
      (cycleAssociatedToClosedSubscheme C p (D.component i).subschemeι (k + 1)).1 x)
    (hdivN : ∀ x : X, divN.1 x = ∑ᶠ i, D.orderN i *
      (cycleAssociatedToClosedSubscheme C p (D.component i).subschemeι (k + 1)).1 x) :
    effectiveCartierIntersectionOfInvertible C p k (Stacks.Divisors.divisorSheaf E)
        (Stacks.Divisors.divisorSheafGlobalSection E)
        (isEffectiveCartierDivisor_zeroScheme_divisorSheaf E) divN =
      firstChernClassCap C p k chernN fundamentalCycle

Stacks.Chow.gysinHomomorphismOfInvertible_eq_firstChernClassCapOfInvertible_of_keyFormula, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/ChernCapDivisor.lean, line 267. The attribute's comment: “the identity i^* div_N(t) = c₁(N|_D) ∩ [D]_{n-1} in A_{n-2}(D), the conclusion of the source, granting the rational equivalence KeyFormulaRationalEquivalenceOnDivisor that the key formula 0AYC exhibits on D — the last step of the source's proof — together with the divisor cycle div_N(t) of 02SJ and the fundamental cycle [D]_{n-1} read on D, each with its presentation by a locally finite family of integral closed subschemes of delta-dimension n-1, which is the second step of the source's proof”.

Stacks 02TM. Let X be integral of delta-dimension k + 2, let E be an effective Cartier divisor on X with closed immersion i : E ⟶ X, and let N be an invertible module on X with a nonzero meromorphic section t. Then

i^* div_N(t) = c₁(N|_E) ∩ [E]_{k+1} in A_k(E),

the identity of the source: the left hand side is the Gysin pullback of Stacks 02T8 along i, which takes its values in the Chow group of E, and the right hand side is the cap product of Stacks 02SO on E with the first Chern class of the restriction N|_E, applied to the fundamental cycle of E read as a cycle on E.

The divisor cycle div_N(t) of Stacks 02SJ and the fundamental cycle [E]_{k+1} are explicit parameters, each with the presentation the second step of the source's proof gives it: the first by the family {Z_i} of prime divisors of the key formula data D, with the orders ord_{B_i}(g_i), and the second by a locally finite family {V_j} of integral closed subschemes of E of delta-dimension k + 1, with multiplicities m_j. The remaining input is the rational equivalence Stacks.Chow.KeyFormulaRationalEquivalenceOnDivisor on E, which is the last step of the source's proof; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.Gysin42.ChernCapDivisor.

Given these, the two sides are computed on their presentations by the locally finite component formulas of Stacks 02T8 and 02SO, and the rational equivalence identifies the resulting two classes.

theorem gysinHomomorphismOfInvertible_eq_firstChernClassCapOfInvertible_of_keyFormula
    (hn : schemeDeltaDimension C p = ((k + 2 : ℤ) : EInt)) (E : X.IdealSheafData)
    [Stacks.Divisors.IsEffectiveCartierDivisor E] (N : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property N]
    (D : KeyFormulaData X) {J : Type u}
    (V : J → (Stacks.Divisors.zeroScheme X (Stacks.Divisors.divisorSheaf E)
      (Stacks.Divisors.divisorSheafGlobalSection E)).subscheme.IdealSheafData)
    (hV : ∀ j, IsIntegral (V j).subscheme)
    (hVdim : ∀ j, schemeDeltaDimension C ((V j).subschemeι ≫
        (Stacks.Divisors.zeroScheme X (Stacks.Divisors.divisorSheaf E)
          (Stacks.Divisors.divisorSheafGlobalSection E)).subschemeι ≫ p) =
      ((k + 1 : ℤ) : EInt))
    (hVlocal : LocallyFinite fun j ↦ ((V j).support :
      Set (Stacks.Divisors.zeroScheme X (Stacks.Divisors.divisorSheaf E)
        (Stacks.Divisors.divisorSheafGlobalSection E)).subscheme))
    (m : J → ℤ)
    (hKeyOnDivisor : KeyFormulaRationalEquivalenceOnDivisor C p hn E N D V hV hVdim m)
    (divN : CycleGroup C p (k + 1))
    (hdivN : ∀ x : X, divN.1 x = ∑ᶠ i, D.orderN i *
      (cycleAssociatedToClosedSubscheme C p (D.component i).subschemeι (k + 1)).1 x)
    (fundamentalCycle : CycleGroup C ((Stacks.Divisors.zeroScheme X
      (Stacks.Divisors.divisorSheaf E)
      (Stacks.Divisors.divisorSheafGlobalSection E)).subschemeι ≫ p) (k + 1))
    (hfundamentalCycle : ∀ z : (Stacks.Divisors.zeroScheme X
      (Stacks.Divisors.divisorSheaf E)
      (Stacks.Divisors.divisorSheafGlobalSection E)).subscheme,
      fundamentalCycle.1 z = ∑ᶠ j, m j *
        (cycleAssociatedToClosedSubscheme C ((Stacks.Divisors.zeroScheme X
            (Stacks.Divisors.divisorSheaf E)
            (Stacks.Divisors.divisorSheafGlobalSection E)).subschemeι ≫ p)
          (V j).subschemeι (k + 1)).1 z) :
    gysinHomomorphismOfInvertible C p k (Stacks.Divisors.divisorSheaf E)
        (Stacks.Divisors.divisorSheafGlobalSection E) divN =
      firstChernClassCapOfInvertible C ((Stacks.Divisors.zeroScheme X
          (Stacks.Divisors.divisorSheaf E)
          (Stacks.Divisors.divisorSheafGlobalSection E)).subschemeι ≫ p) k
        ((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X
          (Stacks.Divisors.divisorSheaf E)
          (Stacks.Divisors.divisorSheafGlobalSection E)).subschemeι).obj N)
        fundamentalCycle

Stacks.Chow.gysin_divisorOfMeromorphicSection_eq_firstChernClassCap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/DivisorChernComparison.lean, line 496.

Stacks 02TM. Let X be integral and locally of finite type over the base scheme S of chapter 42, with n = dim_δ(X), let i : D ⟶ X be an effective Cartier divisor, and let N be an invertible 𝒪_X-module with a nonzero (that is, regular) meromorphic section t. Then

i^* div_N(t) = c₁(N|_D) ∩ [D]_{n-1} in CH_{n-2}(D).

Here i^* is the Gysin homomorphism of Stacks 02T8 for the pair (𝒪_X(D), 1_D), whose zero scheme is D (Stacks.Divisors.zeroScheme_canonicalSection), so it takes values in the Chow group of D; div_N(t) is the divisor cycle of Stacks 02SJ (1); N|_D is the pullback of N along i; and [D]_{n-1} is the fundamental cycle of D, the cycle of D as a closed subscheme of itself. Cycles of degree n - 1 are read in degree (n - 2) + 1, the source of i^* and of the cap product into degree n - 2, by Stacks.Chow.cycleGroupOfEq.

theorem gysin_divisorOfMeromorphicSection_eq_firstChernClassCap (n : ℤ)
    (hn : schemeDeltaDimension C p = (n : EInt)) (E : X.IdealSheafData)
    [IsEffectiveCartierDivisor E] (N : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property N]
    (t : AlgebraicGeometry.MeromorphicSection X.sheaf N)
    (ht : AlgebraicGeometry.IsRegularMeromorphicSection X.sheaf N t) :
    gysinHomomorphismOfInvertible C p (n - 2) (divisorSheaf E) (divisorSheafGlobalSection E)
        (cycleGroupOfEq (by ring) (divisorOfMeromorphicSectionCycle C p n hn N t ht)) =
      firstChernClassCapOfInvertible C
        ((Stacks.Divisors.zeroScheme X (divisorSheaf E)
          (divisorSheafGlobalSection E)).subschemeι ≫ p) (n - 2)
        ((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X (divisorSheaf E)
          (divisorSheafGlobalSection E)).subschemeι).obj N)
        (cycleGroupOfEq (by ring) (fundamentalCycle C
          ((Stacks.Divisors.zeroScheme X (divisorSheaf E)
            (divisorSheafGlobalSection E)).subschemeι ≫ p) (n - 1)))

Tag 02TO, a lemma

Tag 02TO in the Stacks Project.

Stacks.Chow.gysinOfInvertibleDescends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/GysinSystemOfInvertible.lean, line 66. The attribute's comment: “the vanishing for every test datum at once, with no hypothesis: the bundled form of gysinOfInvertibleFactorsThroughRationalEquivalence”.

For every scheme locally of finite type over the base, every invertible module on it, every global section of that module and every degree, the Gysin map of the zero scheme of the section kills the cycles rationally equivalent to zero.

theorem gysinOfInvertibleDescends (C : ChowSituation.{u}) : GysinOfInvertibleDescends C

Stacks.Chow.gysinOfInvertibleFactorsThroughRationalEquivalence_of_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinRationalEquivalenceReduction.lean, line 208. The attribute's comment: “the Gysin map factors through rational equivalence, granted the single-component case the source's proof reduces to — the Gysin map kills the pushforward of div_V(f) for one integral V and one rational function f, which the source settles with Stacks 02TM, 02TI and 02SP. The reduction to that case, which the source performs with Stacks 02TA and 02S2, is proved”.

Stacks 02TO from its single-component case. If the Gysin map of the zero scheme of s kills the pushforward of the principal divisor of a rational function on each single integral closed subscheme of delta-dimension k + 2, with witnesses over that subscheme, then it kills every (k+1)-cycle rationally equivalent to zero — which is the vanishing of Stacks 02TO, and therefore, by Stacks.Chow.gysinHomomorphismOnChowOfInvertibleOfComponents, the descended map i^* : A_{k+1}(X) ⟶ A_k(D).

theorem gysinOfInvertibleFactorsThroughRationalEquivalence_of_components
    (h : GysinOfInvertibleKillsPrincipalDivisorOnComponent C p k L s) :
    GysinOfInvertibleFactorsThroughRationalEquivalence C p k L s

Stacks.Chow.gysinHomomorphismOnChowOfInvertibleOfComponents, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinRationalEquivalenceReduction.lean, line 228. The attribute's comment: “the descended map i^* : A_{k+1}(X) ⟶ A_k(D), granted the single-component case the source's proof reduces to, as in gysinOfInvertibleFactorsThroughRationalEquivalence_of_components”.

Stacks 02TO. The Gysin homomorphism of the zero scheme of a global section of an invertible module, descended to Chow groups,

i^* : A_{k+1}(X) ⟶ A_k(D),

granted the single-component datum. This is Stacks.Chow.gysinHomomorphismOnChowOfInvertible with its vanishing hypothesis supplied by Stacks.Chow.gysinOfInvertibleFactorsThroughRationalEquivalence_of_components, so it is a function of L, s and that datum alone, and Stacks.Chow.eq_gysinHomomorphismOnChowOfInvertible says it is the only homomorphism of Chow groups agreeing with the Gysin map on cycle representatives.

def gysinHomomorphismOnChowOfInvertibleOfComponents
    (h : GysinOfInvertibleKillsPrincipalDivisorOnComponent C p k L s) :
    chowGroup C p (k + 1) →+
      chowGroup C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k

Stacks.Chow.gysinOfInvertibleFactorsThroughRationalEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/GysinComponentDischarge.lean, line 837. The attribute's comment: “the Gysin map factors through rational equivalence, with no hypothesis: the single-component case the source's proof reduces to is proved here, as gysinOfInvertibleKillsPrincipalDivisorOnComponent, from the key formula 0AYC”.

Stacks 02TO, with no hypothesis. The Gysin homomorphism of the zero scheme of a global section of an invertible module kills every (k+1)-cycle rationally equivalent to zero.

The single-component case the source's proof reduces to is Stacks.Chow.gysinOfInvertibleKillsPrincipalDivisorOnComponent, proved above, and the reduction to it is Stacks.Chow.gysinOfInvertibleFactorsThroughRationalEquivalence_of_components.

theorem gysinOfInvertibleFactorsThroughRationalEquivalence :
    GysinOfInvertibleFactorsThroughRationalEquivalence C p k L s

Stacks.Chow.gysinChowOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/KeyFormula/GysinComponentDischarge.lean, line 853. The attribute's comment: “the descended map i^* : A_{k+1}(X) ⟶ A_k(D), with no hypothesis: the single-component datum is proved, in gysinOfInvertibleKillsPrincipalDivisorOnComponent”.

Stacks 02TO, with no hypothesis. The Gysin homomorphism of the zero scheme D = Z(s) of a global section of an invertible module, descended to Chow groups,

i^* : A_{k+1}(X) ⟶ A_k(D).

This is Stacks.Chow.gysinHomomorphismOnChowOfInvertibleOfComponents with its single-component datum supplied, and Stacks.Chow.eq_gysinHomomorphismOnChowOfInvertible says it is the only homomorphism of Chow groups agreeing with the Gysin map of Stacks 02T8 on cycle representatives.

def gysinChowOfInvertible : chowGroup C p (k + 1) →+
    chowGroup C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k

Tag 0F95, a lemma

Tag 0F95 in the Stacks Project.

Stacks.Chow.gysinHomomorphismOfInvertible_properPushforward_subschemeι, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/SelfIntersection.lean, line 280. The attribute's comment: “the identity i^ i_ α = c₁(L|_D) ∩ α in A_k(D), with i_* taken on cycles as in the source's proof, with no hypothesis”.

Stacks 0F95. For the Gysin map of the zero scheme of a global section of an invertible module L, the composite with the pushforward along i is intersection with the first Chern class of the restriction L|_D: i^* i_* α = c₁(L|_D) ∩ α in A_k(D).

Both operations are functions of L and s alone: the Gysin map is Stacks.Chow.gysinHomomorphismOfInvertible and the right hand side is the cap product Stacks.Chow.firstChernClassCapOfInvertible of the restricted module, which is invertible by Stacks 0B8L. No hypothesis is carried: the two first Chern class component rules agree up to rational equivalence on the integral components of D. The statement is exactly Stacks.Chow.gysinHomomorphismOfInvertible_properPushforward_zeroSchemeι, of which this is an alias.

alias gysinHomomorphismOfInvertible_properPushforward_subschemeι

Stacks.Chow.gysinHomomorphismOnChowOfInvertible_properChowPushforward_subschemeι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/SelfIntersection.lean, line 297. The attribute's comment: “the composite A_{k+1}(D) ⟶ A_k(D) of the descended operations, at any descent data h and hchernD; each is discharged by a theorem of this repository (Stacks 02TO and 02TI), so nothing is assumed”.

Stacks 0F95, on Chow groups. The composite i^* i_* : A_{k+1}(D) ⟶ A_k(D) of the two descended operations of an invertible module L and a section s is intersection with the first Chern class of L|_D.

The descended Gysin map is that of Stacks 02TO and the descended cap product that of Stacks 02TI, at descent data h and hchernD. Both are propositions proved in this repository, as Stacks.Chow.gysinOfInvertibleFactorsThroughRationalEquivalence and Stacks.Chow.firstChernClassCapFactorsThroughRationalEquivalence_firstChernComponentCycleRule, so the identity holds outright; with those proofs supplied it is Stacks.Chow.gysinChowOfInvertible_properChowPushforward_zeroSchemeι. The instance of Stacks 02S2 needed for i_* on Chow groups is discharged, i being a closed immersion.

theorem gysinHomomorphismOnChowOfInvertible_properChowPushforward_subschemeι
    (h : GysinOfInvertibleFactorsThroughRationalEquivalence C p k L s)
    (hchernD : FirstChernClassCapFactorsThroughRationalEquivalence C
      ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k
      (firstChernComponentCycleRule C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k
        ((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X L s).subschemeι).obj L)))
    (α : chowGroup C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) (k + 1)) :
    gysinHomomorphismOnChowOfInvertible C p k L s h
        (properChowPushforward C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) p
          (Stacks.Divisors.zeroScheme X L s).subschemeι rfl (k + 1)
          (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
            (Stacks.Divisors.zeroScheme X L s).subschemeι C
            ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) p rfl (k + 1)) α) =
      firstChernClassCapOnChow C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k
        (firstChernComponentCycleRule C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k
          ((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X L s).subschemeι).obj L))
        hchernD α

Stacks.Chow.gysinChowOfInvertible_comp_properChowPushforward_zeroSchemeι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/SelfIntersectionChow.lean, line 88.

Stacks 0F95. The composite of the proper pushforward along the zero scheme i : D = Z(s) ⟶ X of a global section of an invertible module with the Gysin map of that zero scheme is intersection with the first Chern class of the restriction L|_D:

i^* i_* α = c₁(L|_D) ∩ α in \CH_k(D), for α ∈ \CH_{k+1}(D).

All three maps are the operations on Chow groups: i_* is Tag 0GU8, whose vanishing hypothesis of Tag 02S2 is discharged by Stacks.Chow.properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion, i^* is the descended Gysin map Stacks.Chow.gysinChowOfInvertible of Tag 02TO and the right hand side is the descended cap product Stacks.Chow.firstChernClassCapChow of Tag 02TI, both of which are unconditional in this repository. No hypothesis is carried.

Every class is the class of a cycle, and on a cycle the identity is Stacks.Chow.gysinHomomorphismOfInvertible_properPushforward_zeroSchemeι.

theorem gysinChowOfInvertible_comp_properChowPushforward_zeroSchemeι :
    (gysinChowOfInvertible C p k L s).comp
        (properChowPushforward C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) p
          (Stacks.Divisors.zeroScheme X L s).subschemeι rfl (k + 1)
          (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
            (Stacks.Divisors.zeroScheme X L s).subschemeι C
            ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) p rfl (k + 1))) =
      firstChernClassCapChow C k ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p)
        ((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X L s).subschemeι).obj L)

Stacks.Chow.gysinChowOfInvertible_properChowPushforward_zeroSchemeι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/SelfIntersectionChow.lean, line 106.

Stacks 0F95, read on a class. This is Stacks.Chow.gysinChowOfInvertible_comp_properChowPushforward_zeroSchemeι evaluated at α, the source's "sends α to c₁(L|_D) ∩ α".

theorem gysinChowOfInvertible_properChowPushforward_zeroSchemeι
    (α : chowGroup C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) (k + 1)) :
    gysinChowOfInvertible C p k L s
        (properChowPushforward C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) p
          (Stacks.Divisors.zeroScheme X L s).subschemeι rfl (k + 1)
          (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
            (Stacks.Divisors.zeroScheme X L s).subschemeι C
            ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) p rfl (k + 1)) α) =
      firstChernClassCapChow C k ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p)
        ((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X L s).subschemeι).obj L) α

Stacks.Chow.gysinHomomorphismOfInvertible_properPushforward_zeroSchemeι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/SelfIntersectionFormula.lean, line 358. The attribute's comment: “the identity i^ i_ α = c₁(L|_D) ∩ α in A_k(D), with i_* taken on cycles as in the source's proof”. References: SGA 5 VII (9.2), “Codimension d = 1”.

The self-intersection formula. For the Gysin map of the zero scheme i : D = Z(s) ⟶ X of a global section of an invertible module L, the composite with the pushforward along i is intersection with the first Chern class of the restriction L|_D:

i^* i_* α = c₁(L|_D) ∩ α in A_k(D), for α ∈ Z_{k+1}(D).

Both operations are functions of L and s alone: the Gysin map is Stacks.Chow.gysinHomomorphismOfInvertible (Tag 02T8) and the right hand side is the cap product Stacks.Chow.firstChernClassCapOfInvertible (Tag 02SO) of the restricted module, which is invertible by Tag 0B8L. No hypothesis is carried; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.Gysin42.SelfIntersectionFormula.

theorem gysinHomomorphismOfInvertible_properPushforward_zeroSchemeι
    (α : CycleGroup C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) (k + 1)) :
    gysinHomomorphismOfInvertible C p k L s
        (properPushforward C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) p
          (Stacks.Divisors.zeroScheme X L s).subschemeι rfl (k + 1) α) =
      firstChernClassCapOfInvertible C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k
        ((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X L s).subschemeι).obj L) α

Tag 0B72, a lemma

Tag 0B72 in the Stacks Project.

Stacks.Chow.gysinNaturality_firstChernIdentityCapRule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FirstChernClassCanonical.lean, line 327. The attribute's comment: “the Gysin identity read for the identity cap rule of the canonical first Chern class cap product on the test schemes of X, i.e. the predicate IdentityCapRule.GysinNaturality that the bivariant class of Stacks 0B77 takes as its third naturality hypothesis, with no hypothesis of its own”.

The Gysin identity on the test schemes. For the canonical first Chern class cap product, a test morphism g : T ⟶ X, and an invertible module 𝒩 on T with a global section s and zero scheme i : D = Z(s) ⟶ T,

c₁((i ∘ g)^*ℒ) ∩ i^*α = i^*(c₁(g^*ℒ) ∩ α).

This is Stacks.Chow.IdentityCapRule.GysinNaturality for Stacks.Chow.firstChernIdentityCapRule at the canonical cap product and the canonical Gysin system.

theorem gysinNaturality_firstChernIdentityCapRule :
    IdentityCapRule.GysinNaturality C sX 1
      (firstChernIdentityCapRule C sX (canonicalFirstChernCapRule C) L)
      (canonicalGysinSystem C)

Stacks.Chow.GenuineChern.gysinChowOfInvertible_firstChernClassCapChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/GysinFirstChernCap.lean, line 82. The attribute's comment: “the identity i^ (c_1(N) cap a) = c_1(i^ N) cap i^* a on Chow groups, for every class a, stated for the descended operations of Stacks 02TO and 02TI that the library proves outright (gysinChowOfInvertible, firstChernClassCapChow); nothing about the Gysin map, the cap product or their descent is left over. The source proves the tag with the proof of Stacks 0B73 through Stacks 02TM on the integral components; here it is deduced from Stacks 0B73 itself for the pair (L, s) and the zero section of N, using Stacks 02T9 to read j_* j^* as the cap product and Stacks 02TA for the pushforward along Z(0) = X ⟶ X”.

Let ℒ be an invertible module on X with a global section s and zero scheme i : D = Z(s) ⟶ X, and let 𝒩 be an invertible module on X. Then Gysin pullback along i commutes with capping with the first Chern class of 𝒩:

i^*(c₁(𝒩) ∩ α) = c₁(i^*𝒩) ∩ i^*α in A_k(D), for every α ∈ A_{k+2}(X).

theorem gysinChowOfInvertible_firstChernClassCapChow (α : chowGroup C p (k + 1 + 1)) :
    gysinChowOfInvertible C p k L s (firstChernClassCapChow C (k + 1) p N α) =
      firstChernClassCapChow C k ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p)
        ((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X L s).subschemeι).obj N)
        (gysinChowOfInvertible C p (k + 1) L s α)

Stacks.Chow.gysinChowOfInvertible_firstChernClassCapChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/ChernCapGysinCommute.lean, line 167. The attribute's comment: “the identity i^(c_1(N) cap alpha) = c_1(i^ N) cap i^* alpha in A_k(D), for the Gysin map of Stacks 02TO and the cap product of Stacks 02TI, with no hypothesis”.

Stacks 0B72, with no hypothesis. For an invertible module ℒ with a global section s whose zero scheme is i : D = Z(s) ⟶ X, and a second invertible module 𝒩 on X, Gysin pullback along i commutes with capping with the first Chern class of 𝒩:

i^*(c₁(𝒩) ∩ α) = c₁(i^*𝒩) ∩ i^*α in A_k(D), for α ∈ A_{k+2}(X).

The Gysin map is the one of Stacks 02TO and the cap product the one of Stacks 02TI, both constructed in this repository with no hypothesis. Nothing is assumed: the cap product with c₁(𝒩) is itself the Gysin map of the zero section of 𝒩, so the identity is Stacks 0B73 for the pairs (ℒ, s) and (𝒩, 0), read through Stacks 02T9 on X and on D and Stacks 02TA across Z(0) ⟶ X. See the implementation notes.

theorem gysinChowOfInvertible_firstChernClassCapChow (α : chowGroup C p (k + 1 + 1)) :
    gysinChowOfInvertible C p k L s (firstChernClassCapChow C (k + 1) p N α) =
      firstChernClassCapChow C k ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p)
        (zeroSchemeRestrictModule L N s) (gysinChowOfInvertible C p (k + 1) L s α)

Tag 0B73, a lemma

Tag 0B73 in the Stacks Project.

Stacks.Chow.gysinChowOfInvertible_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinGysinKeyFormula.lean, line 1362.

Let (S, δ) be the base situation of chapter 42 of the Stacks Project, let X be locally of finite type over S, and let (L, s, i : D → X) and (L', s', i' : D' → X) be two triples as in Definition 02T8, so that D = Z(s) and D' = Z(s') are the zero schemes of the two sections. Write j : D ∩ D' → D and j' : D ∩ D' → D' for the two presentations of the scheme-theoretic intersection as a zero scheme — of the restriction of s' to D, and of the restriction of s to D' — and let e be an isomorphism between them over X. Then the diagram

  CH_k(X)  --i^*-->  CH_{k-1}(D)
     |                  |
  (i')^*               j^*
     v                  v
  CH_{k-1}(D') --(j')^*--> CH_{k-2}(D ∩ D')

commutes, each of the four maps being a Gysin map. The input degree is written (k + 1) + 1.

theorem gysinChowOfInvertible_comm
    (e : (zeroSchemeInter L L' s s').subscheme ≅ (zeroSchemeInter L' L s' s).subscheme)
    (he : e.hom ≫ (zeroSchemeInter L' L s' s).subschemeι ≫
        (Stacks.Divisors.zeroScheme X L' s').subschemeι =
      (zeroSchemeInter L L' s s').subschemeι ≫ (Stacks.Divisors.zeroScheme X L s).subschemeι)
    (α : chowGroup C p (k + 1 + 1)) :
    chowPushforwardOfIso C ((zeroSchemeInter L L' s s').subschemeι ≫
          (Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p)
        ((zeroSchemeInter L' L s' s).subschemeι ≫
          (Stacks.Divisors.zeroScheme X L' s').subschemeι ≫ p)
        e.hom (iso_zeroSchemeInter_comp_structureMorphism C p L L' s s' e he) k
        (gysinChowOfInvertible C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ p) k
          (zeroSchemeRestrictModule L L' s) (restrictSectionToZeroScheme L L' s s')
          (gysinChowOfInvertible C p (k + 1) L s α)) =
      gysinChowOfInvertible C ((Stacks.Divisors.zeroScheme X L' s').subschemeι ≫ p) k
        (zeroSchemeRestrictModule L' L s') (restrictSectionToZeroScheme L' L s' s)
        (gysinChowOfInvertible C p (k + 1) L' s' α)

Sources

• Section 42.30, Tag 02TK
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.effectiveCartierIntersection_eq_firstChernClassCap_of_keyFormula · Stacks.Chow.gysinHomomorphismOfInvertible_eq_firstChernClassCapOfInvertible_of_keyFormula · Stacks.Chow.gysin_divisorOfMeromorphicSection_eq_firstChernClassCap · Stacks.Chow.gysinOfInvertibleDescends · Stacks.Chow.gysinOfInvertibleFactorsThroughRationalEquivalence_of_components · Stacks.Chow.gysinHomomorphismOnChowOfInvertibleOfComponents · Stacks.Chow.gysinOfInvertibleFactorsThroughRationalEquivalence · Stacks.Chow.gysinChowOfInvertible

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.