42.35 Lemmas on bivariant… to 42.43 The splitting principle
Section42.35 Lemmas on bivariant classes#
Section 42.35 of the Stacks Project, Tag 0FDY. 6 tags here are carried by 26 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0B7A, a lemma
Tag 0B7A in the Stacks Project.
Stacks.Chow.VeryWeakCapRule.cap_eq_zero_of_isCycleGysinNatural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VeryWeakBivariantCriterion.lean, line 792.
Stacks 0B7A, the very weak form of Fulton's Theorem 17.1. Let
(S, δ)be as in Situation 02QL, letf : X ⟶ Ybe a morphism of schemes locally of finite type overSand letp ∈ ℤ. A rule assigning to every locally of finite typeg : Y' ⟶ Yand everyka map
c ∩ - : Z_k(Y') ⟶ A_{k-p}(X'),X' = Y' ×_Y X,which satisfies condition (3) of Definition 0B76 whenever the invertible module restricts trivially to the divisor, factors through rational equivalence: it kills every cycle rationally equivalent to zero.
A cycle
αrationally equivalent to zero is the total fibre difference of a locally finite family of integral closed subschemes ofY' ×_S 𝐏¹_S(Stacks 02S4 part (4)); soαis the difference of the two section Gysin images of the cycleβthat family presents (Stacks.Chow.sub_gysinCycleMapAlong_sections_eq_of_familyFibreDifference), and the two sections are effective Cartier divisors with trivial normal bundle, so condition (3) applies at both and gives the same value (Stacks.Chow.cap_gysinCycleMapAlong_zeroSection_eq_infinitySection_of_isCycleGysinNatural).
theorem VeryWeakCapRule.cap_eq_zero_of_isCycleGysinNatural (C : ChowSituation.{u})
{X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
(sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : X ⟶ Y) [LocallyOfFiniteType f]
(hf : f ≫ sY = sX) (p : ℤ) (c : VeryWeakCapRule C sX sY f hf p)
(hc : c.IsCycleGysinNatural) {T : Scheme.{u}}
(g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ) (α : CycleGroup C (g ≫ sY) k)
(hα : α ∈ rationalEquivalences C (g ≫ sY) k) :
c.cap g k α = 0
Stacks.Chow.VeryWeakCapRule.capChowOfCycleGysin, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VeryWeakBivariantCriterion.lean, line 818. The attribute's comment: “the operation descended to Chow groups”.
Stacks 0B7A. The operation
c ∩ -of a very weak cap rule satisfying condition (3) read on cycles, descended to Chow groups:A_k(Y') ⟶ A_{k-p}(X').
def VeryWeakCapRule.capChowOfCycleGysin (C : ChowSituation.{u}) {X Y : Scheme.{u}}
(sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
(f : X ⟶ Y) [LocallyOfFiniteType f] (hf : f ≫ sY = sX) (p : ℤ)
(c : VeryWeakCapRule C sX sY f hf p) (hc : c.IsCycleGysinNatural) {T : Scheme.{u}}
(g : T ⟶ Y) [LocallyOfFiniteType g]
(k : ℤ) : chowGroup C (g ≫ sY) k →+ chowGroup C (pullback.fst f g ≫ sX) (k - p)
Tag 0F9A, a lemma
Tag 0F9A in the Stacks Project.
Stacks.Chow.WeakCapRule.toBivariantClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/WeakBivariantCriterionProof.lean, line 668.
[Stacks, Tag 0F9A], a weak form of Fulton's Theorem 17.1. Let
(S, δ)be as in Situation 02QL, letf : X ⟶ Ybe a morphism of schemes locally of finite type overSand letp ∈ ℤ. A rule assigning to every morphismY' ⟶ Ylocally of finite type and everyka mapc ∩ - : A_k(Y') ⟶ A_{k-p}(Y' ×_Y X), satisfying conditions (1) and (2) of Stacks 0B76 and condition (3) wheneverℒ'|_{D'} ≅ 𝒪_{D'}— aStacks.Chow.WeakCapRuleread against the canonical Gysin system — is a bivariant class: an element ofA^p(X ⟶ Y)with the same cap operation (Stacks.Chow.WeakCapRule.toBivariantClass_cap).
def WeakCapRule.toBivariantClass (w : WeakCapRule C (canonicalGysinSystem C) sX sY f hf p) :
CanonicalBivariantClass C sX sY f hf p
Tag 02UC, a lemma
Tag 02UC in the Stacks Project.
Stacks.Chow.BivariantClass.eq_zero_iff_capsIntegralFundamentalClassesToZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Vanishing.lean, line 726. The attribute's comment: “(1) ⇔ (2)”.
Stacks 02UC, (1)
⇔(2). A bivariant class is zero exactly when its cap product with the fundamental class of every integral scheme locally of finite type overYvanishes.
theorem BivariantClass.eq_zero_iff_capsIntegralFundamentalClassesToZero
(c : BivariantClass C G sX sY f hf p) :
c = 0 ↔ c.CapsIntegralFundamentalClassesToZero C G sX sY f hf p
Stacks.Chow.BivariantClass.capsIntegralFundamentalClassesToZero_of_hasBirationalModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Vanishing.lean, line 739. The attribute's comment: “(3) ⇒ (2)”.
Stacks 02UC, (3)
⇒(2). If some proper birational modification of each integral test scheme has its fundamental class killed byc, then so has the test scheme itself: the modification pushes its fundamental class forward to the fundamental class, and capping with a bivariant class commutes with proper pushforward.
theorem BivariantClass.capsIntegralFundamentalClassesToZero_of_hasBirationalModification
{c : BivariantClass C G sX sY f hf p}
(hc : c.HasBirationalModificationCappingToZero C G sX sY f hf p) :
c.CapsIntegralFundamentalClassesToZero C G sX sY f hf p
Stacks.Chow.BivariantClass.capsIntegralFundamentalClassesToZero_iff_hasBirationalModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Vanishing.lean, line 754. The attribute's comment: “(2) ⇔ (3)”.
Stacks 02UC, (2)
⇔(3). A bivariant class kills the fundamental class of every integral scheme locally of finite type overYexactly when each such scheme admits a proper birational modification whose fundamental class it kills.
theorem BivariantClass.capsIntegralFundamentalClassesToZero_iff_hasBirationalModification
(c : BivariantClass C G sX sY f hf p) :
c.CapsIntegralFundamentalClassesToZero C G sX sY f hf p ↔
c.HasBirationalModificationCappingToZero C G sX sY f hf p
Stacks.Chow.BivariantClass.eq_zero_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Vanishing.lean, line 766. The attribute's comment: “all three clauses”.
Stacks 02UC. For a bivariant class
c ∈ A^p(X ⟶ Y)the following are equivalent:cis zero;c ∩ [Y'] = 0for every integral schemeY'locally of finite type overY; and every suchY'admits a proper birationalY'' ⟶ Y'withc ∩ [Y''] = 0.
theorem BivariantClass.eq_zero_tfae (c : BivariantClass C G sX sY f hf p) :
[c = 0, c.CapsIntegralFundamentalClassesToZero C G sX sY f hf p,
c.HasBirationalModificationCappingToZero C G sX sY f hf p].TFAE
Stacks.Chow.BivariantClass.eq_zero_iff_capsIntegral_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/VanishingUnconditional.lean, line 121. The attribute's comment: “(1) ⇔ (2) for A^p(X ⟶ Y) itself: the bivariant group read at the canonical Gysin system Stacks.Chow.gysinSystemOfInvertible, which is constructed outright, so no Gysin system is assumed”.
A bivariant class for the canonical Gysin system is zero exactly when its cap product with the fundamental class of every integral scheme locally of finite type over
Yvanishes.
theorem BivariantClass.eq_zero_iff_capsIntegral_canonical :
c = 0 ↔
c.CapsIntegralFundamentalClassesToZero C (gysinSystemOfInvertible C) sX sY f hf p
Stacks.Chow.BivariantClass.capsIntegral_iff_hasBirationalModification_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/VanishingUnconditional.lean, line 134. The attribute's comment: “(2) ⇔ (3) for A^p(X ⟶ Y) itself: the bivariant group read at the canonical Gysin system Stacks.Chow.gysinSystemOfInvertible, which is constructed outright, so no Gysin system is assumed”.
A bivariant class for the canonical Gysin system kills the fundamental class of every integral scheme locally of finite type over
Yexactly when each such scheme admits a proper birational modification whose fundamental class it kills.
theorem BivariantClass.capsIntegral_iff_hasBirationalModification_canonical :
c.CapsIntegralFundamentalClassesToZero C (gysinSystemOfInvertible C) sX sY f hf p ↔
c.HasBirationalModificationCappingToZero C (gysinSystemOfInvertible C) sX sY f hf p
Stacks.Chow.BivariantClass.eq_zero_tfae_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/VanishingUnconditional.lean, line 146. The attribute's comment: “all three clauses for A^p(X ⟶ Y) itself: the bivariant group read at the canonical Gysin system Stacks.Chow.gysinSystemOfInvertible, which is constructed outright, so no Gysin system is assumed”.
For a bivariant class
c ∈ A^p(X ⟶ Y)for the canonical Gysin system the following are equivalent:cis zero;c ∩ [Y'] = 0for every integral schemeY'locally of finite type overY; and every suchY'admits a proper birationalY'' ⟶ Y'withc ∩ [Y''] = 0.
theorem BivariantClass.eq_zero_tfae_canonical :
[c = 0, c.CapsIntegralFundamentalClassesToZero C (gysinSystemOfInvertible C) sX sY f hf p,
c.HasBirationalModificationCappingToZero C (gysinSystemOfInvertible C)
sX sY f hf p].TFAE
Tag 0FDZ, a lemma
Tag 0FDZ in the Stacks Project.
Stacks.Chow.bivariantPieceAssemblyCap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantDisjoint/PieceAssembly/AssembledCap.lean, line 92. The attribute's comment: “the cap operation assembled from a family of bivariant classes on the pieces”.
Stacks 0FDZ. The cap operation assembled from a family
(c_i)of bivariant classes of degreepfor the restrictionsf_i : X_i ⟶ Y_{a(i)}: on a test schemeg : T ⟶ Yit sendsα ∈ A_k(T)to the unique class inA_{k-p}(X ×_Y T)whose restriction to thei-th pieceX_i ×_{Y_{a(i)}} T_{a(i)}isc_i ∩ α|_{T_{a(i)}}.It is well defined because the Chow groups of
X ×_Y Tdecompose along those pieces, byStacks.Chow.chowGroupPullbackPieceEquiv.
def bivariantPieceAssemblyCap
(c : ∀ i, BivariantClass C G ((UX i).ι ≫ sX) ((UY (a i)).ι ≫ sY)
(pieceMap f UX UY a ha i)
(pieceMap_comp_pieceStructureMorphism C sX sY f hf UX UY a ha i) p)
{T : Scheme.{u}} (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ) :
chowGroup C (g ≫ sY) k →+ chowGroup C (pullback.fst f g ≫ sX) (k - p)
Stacks.Chow.bivariantPieceRestrictionOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantDisjoint/PieceGysinSystemOfInvertible.lean, line 517. The attribute's comment: “the restriction of a bivariant class to a piece, at the Gysin system of the first Chern class rule, with the open-immersion case of Stacks 02TA discharged”.
Stacks 0FDZ. The restriction
c_iof a bivariant classcof degreepforf : X ⟶ Yto the piecef_i : X_i ⟶ Y_{a(i)}of a disjoint union decomposition, at the Gysin system of the first Chern class rule of an invertible module.This is
Stacks.Chow.bivariantPieceRestrictionwith its Gysin compatibility discharged byStacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpenImmersion, so it assumes nothing.
def bivariantPieceRestrictionOfInvertible (i : I)
(c : BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p) :
BivariantClass C (gysinSystemOfInvertible C) ((UX i).ι ≫ sX) ((UY (a i)).ι ≫ sY)
(pieceMap f UX UY a ha i)
(pieceMap_comp_structureMorphism C sX sY f hf UX UY a ha i) p
Stacks.Chow.bivariantPieceRestrictionHomOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantDisjoint/PieceGysinSystemOfInvertible.lean, line 530. The attribute's comment: “the map from A^p(X ⟶ Y) to the product over the pieces, at the Gysin system of the first Chern class rule, with the open-immersion case of Stacks 02TA discharged”.
Stacks 0FDZ. The map
A^p(X ⟶ Y) ⟶ ∏_{i ∈ I} A^p(X_i ⟶ Y_{a(i)})of the tag at the Gysin system of the first Chern class rule of an invertible module, with no Gysin compatibility assumed.
def bivariantPieceRestrictionHomOfInvertible :
BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p →+
∀ i, BivariantClass C (gysinSystemOfInvertible C) ((UX i).ι ≫ sX) ((UY (a i)).ι ≫ sY)
(pieceMap f UX UY a ha i)
(pieceMap_comp_structureMorphism C sX sY f hf UX UY a ha i) p
Stacks.Chow.bivariantPieceEquivOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantDisjoint/PieceGysinSystemOfInvertible.lean, line 550. The attribute's comment: “A^p(X ⟶ Y) = ∏_i A^p(X_i ⟶ Y_{a(i)}) at the Gysin system of the first Chern class rule, with all three Gysin compatibilities discharged”.
Stacks 0FDZ.
A^p(X ⟶ Y) = ∏_{i ∈ I} A^p(X_i ⟶ Y_{a(i)})at the Gysin system of the first Chern class rule of an invertible module: a bivariant class of degreepforf : X ⟶ Yis the same thing as a family of bivariant classes of degreepfor the restrictionsf_i : X_i ⟶ Y_{a(i)}.This is
Stacks.Chow.bivariantPieceEquivwith all three of its Gysin compatibilities discharged, byStacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpenImmersion,Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpensRestrictionandStacks.Chow.gysinSystemOfInvertible_isNaturalUnderPullbackComp. Nothing remains assumed: the Gysin system itself carries no hypothesis either.
def bivariantPieceEquivOfInvertible (hX : IsClopenDecomposition UX) :
BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p ≃+
∀ i, BivariantClass C (gysinSystemOfInvertible C) ((UX i).ι ≫ sX) ((UY (a i)).ι ≫ sY)
(pieceMap f UX UY a ha i)
(pieceMap_comp_pieceStructureMorphism C sX sY f hf UX UY a ha i) p
Stacks.Chow.bivariantPieceRestrictionCap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantDisjoint/PieceRestriction.lean, line 477. The attribute's comment: “the cap operation of the restriction of a bivariant class to a piece”.
Stacks 0FDZ. The cap operation
c_i ∩ -of the restriction of a bivariant classcof degreepforf : X ⟶ Yto the piecef_i : X_i ⟶ Y_{a(i)}: on a test schemeg : T ⟶ Y_{a(i)}it is the cap operation ofcatg ≫ (Y_{a(i)} ⟶ Y), restricted along the open immersionX_i ×_{Y_{a(i)}} T ⟶ X ×_Y T.
def bivariantPieceRestrictionCap (c : BivariantClass C G sX sY f hf p) {T : Scheme.{u}}
(g : T ⟶ (UY (a i) : Scheme.{u})) [LocallyOfFiniteType g] (k : ℤ) :
chowGroup C (g ≫ ((UY (a i)).ι ≫ sY)) k →+
chowGroup C (pullback.fst (pieceMap f UX UY a ha i) g ≫ ((UX i).ι ≫ sX)) (k - p)
Stacks.Chow.BivariantClass.eq_of_clopenRestrict_cap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantDisjoint/PieceUniqueness.lean, line 77. The attribute's comment: “injectivity: a bivariant class is determined by its restrictions to the pieces”.
Stacks 0FDZ, injectivity. Two bivariant classes of degree
pforf : X ⟶ Yare equal as soon as, for every test schemeg : T ⟶ Yand everyk, their cap operations agree after restriction to each pieceX_i ×_Y TofX ×_Y T.The pieces of
X ×_Y Tare the preimages of the pieces ofXunder the projection, a decomposition into open and closed subschemes byStacks.Chow.IsClopenDecomposition.preimage, so restriction to them is jointly injective onCH_{k-p}(X ×_Y T)byStacks.Chow.chowGroupClopenEquiv.
theorem BivariantClass.eq_of_clopenRestrict_cap_eq {c d : BivariantClass C G sX sY f hf p}
(h : ∀ {T : Scheme.{u}} (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ)
(α : chowGroup C (g ≫ sY) k) (i : I),
chowGroupRestrict C (pullback.fst f g ≫ sX)
((pullback.fst f g ⁻¹ᵁ UX i).ι ≫ (pullback.fst f g ≫ sX))
(pullback.fst f g ⁻¹ᵁ UX i).ι rfl (k - p) (c.cap g k α) =
chowGroupRestrict C (pullback.fst f g ≫ sX)
((pullback.fst f g ⁻¹ᵁ UX i).ι ≫ (pullback.fst f g ≫ sX))
(pullback.fst f g ⁻¹ᵁ UX i).ι rfl (k - p) (d.cap g k α)) :
c = d
Tag 0FE0, a remark
Tag 0FE0 in the Stacks Project.
Stacks.Chow.isBivariantClassComposition_bivariantCompositeOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/GysinSystemOfInvertible.lean, line 184. The attribute's comment: “the composite class satisfies the composition formula, at the Gysin system of the first Chern class rule, with both cases of Stacks 02TA discharged”.
The composite class at the Gysin system of the first Chern class rule is the composite: on every test scheme its cap operation is cap with
bfollowed by cap witha, pushed forward along the associativity isomorphism of pullbacks.
theorem isBivariantClassComposition_bivariantCompositeOfInvertible
(a : BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p)
(b : BivariantClass C (gysinSystemOfInvertible C) sY sZ g hg q) :
IsBivariantClassComposition C (gysinSystemOfInvertible C) sX sY sZ f g hf hg
(properPushforwardDescends C) p q a b
(bivariantCompositeOfInvertible C sX sY sZ f g hf hg p q a b)
Stacks.Chow.completedBivariantGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedGroup.lean, line 68. The attribute's comment: “completed_bivariant_group”.
Stacks 0FE0. The completed bivariant group
A^*(X ⟶ Y)^∧of a morphismf : X ⟶ Yof schemes locally of finite type over the base: the product, over the connected componentsX_iofX, of the graded groupsA^*(X_i ⟶ Y_{a(i)})of bivariant classes for the restriction offtoX_iand the connected component ofYit lands in. The degree support is finite on each component but need not be bounded across components.
abbrev completedBivariantGroup (C : ChowSituation.{u}) (G : GysinSystem C) {X Y : Scheme.{u}}
(sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
(f : X ⟶ Y) [LocallyOfFiniteType f] (hf : f ≫ sY = sX) : Type (u + 1)
Stacks.Chow.completedIdentityClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedIdentity.lean, line 274. The attribute's comment: “the unit 1 of the completed bivariant cohomology ring A^*(X)^∧”.
The unit
1 ∈ A^*(X)^∧of the completed bivariant cohomology ring: on the connected componentX_iofXit is the restriction of1 ∈ A^0(X)toX_i, placed in degree0. ByStacks.Chow.completedIdentityClass_apply_heqthat restriction is1 ∈ A^0(X_i).
def completedIdentityClass : completedChowCohomology C (gysinSystemOfInvertible C) sX
Stacks.Chow.completedBivariantSubgroupOfInvertible, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/Completion.lean, line 472. The attribute's comment: “the almost-vanishing tuples inside the product of the bivariant groups, at the Gysin system of the first Chern class rule, with the Gysin compatibility discharged”.
Stacks 0FE0. The subgroup of
∏_p A^p(X ⟶ Y)the tag describes — the tuplesc = (c_0, c_1, c_2, …)such that for every connected componentX_iofXthe image ofc_pinA^p(X_i ⟶ Y_{a(i)})vanishes for almost allp— at the Gysin system of the first Chern class rule of an invertible module.This is
Stacks.Chow.completedBivariantSubgroupwith the Gysin compatibility it carries discharged, byStacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpenImmersion. Nothing remains assumed: the Gysin system itself carries no hypothesis either.
abbrev completedBivariantSubgroupOfInvertible :
AddSubgroup (∀ p : ℤ, BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p)
Stacks.Chow.range_completedBivariantSequenceOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/Completion.lean, line 499. The attribute's comment: “the image of the completed group is the almost-vanishing tuples, at the Gysin system of the first Chern class rule, with all three Gysin compatibilities discharged”.
Stacks 0FE0. The image of
A^*(X ⟶ Y)^∧in∏_p A^p(X ⟶ Y)is exactly the subgroup of tuples that vanish in almost all degrees on each connected component, at the Gysin system of the first Chern class rule of an invertible module.This is
Stacks.Chow.range_completedBivariantSequencewith the three Gysin compatibilities of Stacks 0FDZ discharged, byStacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpenImmersion,Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpensRestrictionandStacks.Chow.gysinSystemOfInvertible_isNaturalUnderPullbackComp. Nothing remains assumed: the Gysin system itself carries no hypothesis either.
theorem range_completedBivariantSequenceOfInvertible :
(completedBivariantSequenceOfInvertible C sX sY f hf).range =
completedBivariantSubgroupOfInvertible C sX sY f hf
Stacks.Chow.completedBivariantGroupEquivOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/Completion.lean, line 517. The attribute's comment: “the completed group is the group of almost-vanishing tuples, at the Gysin system of the first Chern class rule, with all three Gysin compatibilities discharged”.
Stacks 0FE0. The completed bivariant group is the group of almost-vanishing tuples in
∏_p A^p(X ⟶ Y), at the Gysin system of the first Chern class rule of an invertible module.This is
Stacks.Chow.completedBivariantGroupEquivwith the three Gysin compatibilities of Stacks 0FDZ discharged, byStacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpenImmersion,Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpensRestrictionandStacks.Chow.gysinSystemOfInvertible_isNaturalUnderPullbackComp. Nothing remains assumed: the Gysin system itself carries no hypothesis either.
def completedBivariantGroupEquivOfInvertible :
completedBivariantGroup C (gysinSystemOfInvertible C) sX sY f hf ≃+
completedBivariantSubgroup C (gysinSystemOfInvertible C) sX sY f hf
(gysinSystemOfInvertible_isNaturalUnderOpenImmersion C)
Stacks.Chow.completedBivariantCompositeOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/Completion.lean, line 636. The attribute's comment: “the composition extended to the completed bivariant groups, at the Gysin system of the first Chern class rule, with both Gysin compatibilities discharged”.
Stacks 0FE0. The composition
A^*(X ⟶ Y)^∧ × A^*(Y ⟶ Z)^∧ ⟶ A^*(X ⟶ Z)^∧extending the composition of Stacks 0B75 to the completions, at the Gysin system of the first Chern class rule of an invertible module.This is
Stacks.Chow.completedBivariantCompositewith both Gysin compatibilities of Stacks 0B75 discharged, byStacks.Chow.gysinSystemOfInvertible_isNaturalUnderBaseChangeIsoandStacks.Chow.gysinSystemOfInvertible_isNaturalUnderPullbackCompPushforward. Nothing remains assumed: the Gysin system itself carries no hypothesis either.
def completedBivariantCompositeOfInvertible
(c : completedBivariantGroup C (gysinSystemOfInvertible C) sX sY f hf)
(d : completedBivariantGroup C (gysinSystemOfInvertible C) sY sZ g hg) :
completedBivariantGroup C (gysinSystemOfInvertible C) sX sZ (f ≫ g)
(comp_comp_structureMorphism_eq hf hg)
Stacks.Chow.completedBivariantCompositeOfInvertible_of_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/Completion.lean, line 653. The attribute's comment: “the composition on the completions extends the composition of homogeneous classes, at the Gysin system of the first Chern class rule, with both Gysin compatibilities discharged”.
Stacks 0FE0. The composition on the completions extends the composition of Stacks 0B75, with nothing assumed: at the Gysin system of the first Chern class rule, if
cis concentrated in degreepon the componentX_ianddis concentrated in degreeqon the componentY_{a(i)}, then the composite is concentrated in degreep + qonX_iand is there the composite bivariant classStacks.Chow.bivariantCompositeOfInvertibleof Stacks 0B75.
theorem completedBivariantCompositeOfInvertible_of_of
(c : completedBivariantGroup C (gysinSystemOfInvertible C) sX sY f hf)
(d : completedBivariantGroup C (gysinSystemOfInvertible C) sY sZ g hg)
(i : ConnectedComponents X) (p q : ℤ) (hc : c i = DirectSum.of _ p (c i p))
(hd : d (f.continuous.connectedComponentsMap i) =
DirectSum.of _ q (d (f.continuous.connectedComponentsMap i) q)) :
completedBivariantCompositeOfInvertible C sX sY sZ f g hf hg c d i =
DirectSum.of _ (p + q)
(completedBivariantCompositeTransport C (gysinSystemOfInvertible C) sX sY sZ f g hf hg
i (p + q)
(bivariantCompositeOfInvertible C _ _ _ _ _ _ _ p q (c i p)
(d (f.continuous.connectedComponentsMap i) q)))
Stacks.Chow.completedChowCohomology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/Completion.lean, line 679. The attribute's comment: “the completed bivariant cohomology ring A^*(X)^∧ of a scheme”.
Stacks 0FE0. The completed bivariant cohomology ring
A^*(X)^∧ = A^*(X ⟶ X)^∧of a schemeXlocally of finite type over the base: the completed bivariant group of the identity ofX. Its multiplication isStacks.Chow.completedBivariantCompositeatf = g = 𝟙 X, andStacks.Chow.completedBivariantGroupEquivreads it as the group of tuples in∏_p A^p(X)that vanish in almost all degrees on each connected component ofX.
abbrev completedChowCohomology (C : ChowSituation.{u}) (G : GysinSystem C) {X : Scheme.{u}}
(sX : X ⟶ C.S) [LocallyOfFiniteType sX] : Type (u + 1)
Tag 0GUC, a lemma
Tag 0GUC in the Stacks Project.
Stacks.Chow.existsUnique_bivariantRestriction_eq_of_isEnvelope, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/EnvelopeDescentExistence.lean, line 168.
Stacks 0GUC. Let
f : X ⟶ Ybe a morphism of schemes locally of finite type over the base of chapter 42, letg : Y' ⟶ Ybe an envelope and writeX' = X ×_Y Y'. Letc' ∈ A^p(X' ⟶ Y'). If the two restrictionsres₁(c') = res₂(c')inA^p(X' ×_X X' ⟶ Y' ×_Y Y')agree, then there is a uniquec ∈ A^p(X ⟶ Y)whose restrictionres(c)alonggisc'.Bivariant classes are taken against the Gysin system of the first Chern class of an invertible module.
theorem existsUnique_bivariantRestriction_eq_of_isEnvelope (C : ChowSituation.{u})
{X Y Y' : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
[LocallyOfFiniteType sY] (f : X ⟶ Y) [LocallyOfFiniteType f] (comm : f ≫ sY = sX)
(g : Y' ⟶ Y) (envelope : IsEnvelope g) (p : ℤ) :
letI : IsProper g := envelope.isProper
∀ c' : BivariantClass C (gysinSystemOfInvertible C) (pullback.fst f g ≫ sX) (g ≫ sY)
(pullback.snd f g) (pullbackSnd_comp_structureMorphism_eq C sX sY f comm g) p,
envelopeDescentRes₁ C (gysinSystemOfInvertible C) sX sY f comm g p
(gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c' =
envelopeDescentRes₂ C (gysinSystemOfInvertible C) sX sY f comm g p
(gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c' →
∃! c : BivariantClass C (gysinSystemOfInvertible C) sX sY f comm p,
bivariantRestriction C (gysinSystemOfInvertible C) sX sY f comm g p
(gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c = c'
Sources
Section42.36 Projective space bundle formula#
Section 42.36 of the Stacks Project, Tag 02TV. 3 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02TW, a lemma
Tag 02TW in the Stacks Project.
Stacks.Chow.projectiveBundleProjection_twist_eq_zero_of_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleProjectionFormula.lean, line 502. The attribute's comment: “vanishing below the fibre dimension: the assertion for s < r - 1, with no hypothesis. The projective bundle enters as a flat, proper morphism of relative dimension r - 1 over the base (Stacks 02TX) and its twist as an invertible module; Stacks 02S1 for the flat pullback, Stacks 02SO and 02TI for the cap product and Stacks 02S2 for the pushforward are all supplied from this development. The top fibre power, that the pushforward at s = r - 1 is α itself, is NOT proved here. What it still needs is the mapping-in half of the universal property of relative Proj, Stacks 01O4, to produce the section Z -> pi^-1(Z) whose image the r - 1 sections cut out; the other two ingredients the source's proof uses are now available, Stacks 02TM unconditionally and the rational sections of O_P(1) as Stacks.ProjectiveBundleTwist.twistSectionGerm”.
Stacks 02TW, vanishing below the fibre dimension, with no hypothesis. For
s < r - 1,
π_*(c₁(L)^s ∩ π^*α) = 0inA_{k+(r-1)-s}(X),for
Lthe twistO_P(1)of the projective bundle. Nothing is assumed beyond the geometry of the bundle:πis flat, proper and of relative dimensionr - 1over the base, which for the projective bundle of a finite locally free module of rankris Stacks 02TX (Stacks.RelativeProj.isProper_projectiveBundleToBase,Stacks.RelativeProj.locallyOfFiniteType_projectiveBundleToBaseandStacks.SymGraded.relativeDimension_freeProjectiveBundleToBase), andLis an invertible module onP, which the twist is.The three inputs the operation is built from are all theorems here: Stacks 02S1 for the flat pullback is
Stacks.Chow.projectiveBundleFlatPullbackFactors, Stacks 02SO and 02TI for the cap withc₁(L)areStacks.Chow.invertibleChernCap, and Stacks 02S2 for the pushforward isStacks.Chow.properPushforwardFactorsThroughRationalEquivalence_of_isProper. The vanishing itself is the dimension count ofStacks.Chow.properChowPushforward_iteratedChernCapOnChow_flatPullbackChow_eq_zero.
theorem projectiveBundleProjection_twist_eq_zero_of_lt (L : P.Modules)
[AlgebraicGeometry.SheafOfModules.IsInvertible P.sheaf.obj P.ringCatSheaf.property L]
(s : ℕ) (hs : s < r - 1) (k : ℤ) (α : chowGroup C sX k) :
projectiveBundleProjection C sX sP π hsP r hπ
(projectiveBundleFlatPullbackFactors C sX sP π hsP r hπ)
(invertibleChernCap C sP L) s k α = 0
Stacks.Chow.projectiveBundle_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProjectiveBundleFormula/Formula.lean, line 149.
For the projective bundle
π : P ⟶ Xof a module of rankn + 1,α ∈ A_k(X)ands ≤ n, the classπ_*(c₁(𝒪_P(1))^s ∩ π^*α) ∈ A_{k+n-s}(X)is0ifs < nand isαifs = n.
theorem projectiveBundle_projection (s : ℕ) (hs : s ≤ n) (k m : ℤ) (h : k + n = m + s)
(α : chowGroup C sX k) :
letI := AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.isFiniteLocallyFree E
(n + 1)
letI := flat_bundleProj E n
letI := locallyOfFiniteType_bundleProj E n
bundleProjection C sX (bundleProj E ≫ sX) (bundleProj E) rfl n
(relativeDimension_bundleProj E n) (invCap C (bundleProj E ≫ sX) (bundleTwist E)) s k m
h α =
if hsn : s = n then chowGroupCast C sX (by subst hsn; omega) α else 0
Tag 02TX, a lemma
Tag 02TX in the Stacks Project.
Stacks.Chow.projectiveBundle_formula, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProjectiveBundleFormula/Formula.lean, line 168.
The projective space bundle formula for the projective bundle of a module of rank
n + 1: the map⨁_{i ≤ n} A_{k+i}(X) ⟶ A_{k+n}(P),(α_i) ↦ ∑_i c₁(𝒪_P(1))^i ∩ π^*α_i, is bijective.
theorem projectiveBundle_formula (k : ℤ) :
letI := AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.isFiniteLocallyFree E
(n + 1)
letI := flat_bundleProj E n
letI := locallyOfFiniteType_bundleProj E n
Function.Bijective (bundleMap C sX (bundleProj E ≫ sX) (bundleProj E) rfl n
(relativeDimension_bundleProj E n) (invCap C (bundleProj E ≫ sX) (bundleTwist E)) k)
Stacks.Chow.bijective_projectiveBundleFormulaMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProjectiveBundleFormula/FormulaOfRank.lean, line 121. References: SGA 7 XVII (5.3), “more general”.
The projective space bundle formula. Let
Xbe locally of finite type over the baseSof chapter 42,ℰa finite locally free𝒪_X-module of rankrand(π : P ⟶ X, 𝒪_P(1))its projective bundle. Then the map⨁_{i = 0}^{r - 1} A_{k+i}(X) ⟶ A_{k+r-1}(P),(α_i) ↦ ∑_i c₁(𝒪_P(1))^i ∩ π^*α_i, is an isomorphism, for everyk.
theorem bijective_projectiveBundleFormulaMap (k : ℤ) :
Function.Bijective (projectiveBundleFormulaMap E r C sX k)
Tag 02TY, a lemma
Tag 02TY in the Stacks Project.
Stacks.Chow.flatPullbackChow_bijective_vectorBundleToBase_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/VectorBundleAffineSpaceBundle.lean, line 262. The attribute's comment: “the isomorphism in rank zero, the bundle now the relative spectrum of the symmetric algebra of a finite locally free sheaf of rank zero rather than an abstract affine-space bundle”.
Stacks 02TY in rank zero, for the relative spectrum of the symmetric algebra. Let
Xbe locally of finite type over the base of chapter 42, letℰbe a finite locally free sheaf of rank zero onXand letp : E = Spec_X(Sym(ℰ)) ⟶ Xbe the associated vector bundle. Thenp^* : A_k(X) ⟶ A_k(E)is bijective for everyk.The bundle is the relative spectrum of
Sym(ℰ), which is the tag's own object;Stacks.Chow.isAffineSpaceBundle_vectorBundleToBasesupplies the local triviality thatStacks.Chow.flatPullbackChow_bijective_of_isAffineSpaceBundle_zeroneeds, and the flatness, local finite type and relative dimension ofpcome from it as well. The instance of Stacks 02S1 that writes the map down is not an extra assumption: a rank-zero bundle projection is an isomorphism, so it is produced byStacks.Chow.flatPullbackFactorsThroughRationalEquivalence_of_isIso.
theorem flatPullbackChow_bijective_vectorBundleToBase_zero (C : ChowSituation.{u})
{X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (E : X.Modules)
[E.IsQuasicoherent]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E 0] (k : ℤ) :
letI _ := locallyOfFiniteType_vectorBundleToBase E 0
letI _ := flat_vectorBundleToBase E 0
letI _ := isIso_vectorBundleToBase_zero E
Function.Bijective (flatPullbackChow C
(Scheme.Modules.vectorBundleToBase X E ≫ sX) sX
(Scheme.Modules.vectorBundleToBase X E) rfl 0
(relativeDimension_vectorBundleToBase E 0) k
(flatPullbackFactorsThroughRationalEquivalence_of_isIso C
(Scheme.Modules.vectorBundleToBase X E ≫ sX) sX
(Scheme.Modules.vectorBundleToBase X E) rfl
(relativeDimension_vectorBundleToBase E 0) k))
Stacks.Chow.flatPullbackChow_bijective_vectorBundleToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/VectorBundleChowBijective.lean, line 340.
[Stacks, Tag 02TY]. Let
(S, δ)be as in Situation 02QL, letXbe locally of finite type overS, letℰbe a finite locally free𝒪_X-module of rankrand letp : E = \underline{\Spec}(\Sym^*(ℰ)) ⟶ Xbe the associated vector bundle. Then
p^* : A_k(X) ⟶ A_{k+r}(E)is an isomorphism for every
k.Surjectivity is [Stacks, Tag 02TT] for the affine-space bundle
p; injectivity isStacks.Chow.flatPullbackChow_injective_vectorBundleToBase. The instance[E.IsQuasicoherent], which the construction of𝐕(ℰ)takes, restricts nothing: a finite locally free module is quasi-coherent, byStacks.AlgebraicGeometry.CoherenceCriteria.isQuasicoherent_of_isFiniteLocallyFree, and the instance is a proposition.
theorem flatPullbackChow_bijective_vectorBundleToBase {X : Scheme.{u}} (sX : X ⟶ C.S)
[LocallyOfFiniteType sX] (E : X.Modules) [E.IsQuasicoherent] (r : ℕ)
[SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r] (k : ℤ) :
letI := locallyOfFiniteType_vectorBundleToBase E r
letI := flat_vectorBundleToBase E r
Function.Bijective (flatPullbackChowOfRelativeDimension C
(Scheme.Modules.vectorBundleToBase X E ≫ sX) sX (Scheme.Modules.vectorBundleToBase X E)
rfl r (relativeDimension_vectorBundleToBase E r) k)
Stacks.Chow.flatPullbackChow_bijective_vectorBundleToBase_factorsGeneral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/VectorBundleFlatPullback.lean, line 121.
Stacks 02TY. Let
Xbe locally of finite type over the base of chapter 42, letℰbe a finite locally free𝒪_X-module of rankrand letp : Spec_X(Sym(ℰ)) ⟶ Xbe its vector bundle. Then flat pullbackp^* : A_k(X) ⟶ A_{k+r}(Spec_X(Sym(ℰ)))is bijective for everyk.This is
Stacks.Chow.flatPullbackChow_bijective_vectorBundleToBase, stated with the flat pullbackStacks.Chow.flatPullbackChowand without the instance[E.IsQuasicoherent], which a finite locally free module satisfies (Stacks.AlgebraicGeometry.CoherenceCriteria.isQuasicoherent_of_isFiniteLocallyFree).
theorem flatPullbackChow_bijective_vectorBundleToBase_factorsGeneral (C : ChowSituation.{u})
{X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (E : X.Modules) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r] (k : ℤ) :
letI := AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.isFiniteLocallyFree E r
letI _ := locallyOfFiniteType_vectorBundleToBase E r
letI _ := flat_vectorBundleToBase E r
Function.Bijective (flatPullbackChow C
(Scheme.Modules.vectorBundleToBase X E ≫ sX) sX
(Scheme.Modules.vectorBundleToBase X E) rfl r
(relativeDimension_vectorBundleToBase E r) k
(flatPullbackFactorsThroughRationalEquivalence_general C _ sX _ rfl r _ k))
Stacks.Chow.flatPullbackChow_bijective_of_isAffineSpaceBundle_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/VectorBundlePullbackIso.lean, line 149. The attribute's comment: “the isomorphism in rank zero, the projection carried as an affine-space bundle of rank zero rather than as the relative spectrum of a symmetric algebra”.
Stacks 02TY in rank zero. Let
Xbe locally of finite type over the base of chapter 42, letℰbe a finite locally free sheaf of rank0onXand letp : E ⟶ Xbe the associated vector bundle. Thenp^* : CH_k(X) ⟶ CH_{k+0}(E)is bijective, which is the assertion of Stacks 02TY forr = 0.The bundle projection is carried as an affine-space bundle of rank zero,
pbeing Zariski-locally onXthe projection𝔸^0_U ⟶ U; a rank-zero vector bundle projection has that property. Such apis an isomorphism, so the assertion isStacks.Chow.flatPullbackChow_bijective_of_isIso. The instance of Stacks 02S1 needed to write the map down is not an extra assumption: it is supplied byStacks.Chow.flatPullbackFactorsThroughRationalEquivalence_of_isIso.Neither half is proved here for
r ≥ 1. The source proof forms the projective space bundleP = P(ℰ ⊕ 𝒪_X)with its tautological invertible sheaf, identifies𝒪_P(D) = 𝒪_P(1)for the divisorD = Z(s)at infinity by Stacks 01X0, writesEasP ∖ D, and then runs the localization sequence of Stacks 02RX against the projective bundle formula of Stacks 02TX forPand forD.Of those inputs Stacks 02TR is proved, in both of its equalities and at Chow level for an arbitrary class:
Stacks.Chow.gysinChowOfInvertible_flatPullbackChowgivesi^* p^* α = (p|_D)^* αandStacks.Chow.firstChernClassCapChow_flatPullbackChowgivesc₁(ℒ) ∩ p^* α = i_*((p|_D)^* α)(StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierFlatPullbackChow.lean:385, 463, with the cycle-level forms atStacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierFlatPullback.lean:178, 241, 289).What is still missing is Stacks 02TX, which is not proved in this repository — it is available only as the two hypotheses
Stacks.Chow.ProjectiveBundleRelationInjectiveandStacks.Chow.ProjectiveBundleRelationSurjective. Its surjectivity half alone is Stacks 02TT, which is itself proved here only in relative dimension zero, and it may not be carried as a hypothesis, being a conjunct of the conclusion. So ther ≥ 1case remains out of reach, but on account of 02TX and 02TT, not of 02TR.
theorem flatPullbackChow_bijective_of_isAffineSpaceBundle_zero (C : ChowSituation.{u})
{X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
[LocallyOfFiniteType sY] (f : X ⟶ Y) [LocallyOfFiniteType f] [AlgebraicGeometry.Flat f]
(hbase : f ≫ sY = sX) (hf : AlgebraicGeometry.RelativeDimension f 0)
(hbundle : IsAffineSpaceBundle f 0) (k : ℤ)
(hfac : FlatPullbackFactorsThroughRationalEquivalence C sX sY f hbase 0 hf k) :
Function.Bijective (flatPullbackChow C sX sY f hbase 0 hf k hfac)
Sources
Section42.37 The Chern classes of a vector bundle#
Section 42.37 of the Stacks Project, Tag 02TZ. 3 tags here are carried by 5 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02U0, a definition
Tag 02U0 in the Stacks Project.
Stacks.Chow.existsUnique_isChernClassFundamentalFamilyOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProjectiveBundleFormula/ChernClassesOfRank.lean, line 189. The attribute's comment: “part (1)”.
Stacks 02U0, part (1). For a module
ℰof rankronXand an integern, there are classesc_i ∈ A_{n-i}(X),0 ≤ i ≤ r, withc_0 = [X]and∑_{i=0}^{r} (-1)^i c₁(𝒪_{𝐏(ℰ)}(1))^i ∩ π^*c_{r-i} = 0, and exactly one such family. Here[X] = [X]_nis the fundamental cycle of Stacks 02QU; the source takesXintegral andn = dim_δ(X), which is not needed.
theorem existsUnique_isChernClassFundamentalFamilyOfRank (n : ℤ) :
∃! c : ∀ i : Fin (r + 1), chowGroup C sX (n - (i : ℤ)),
IsChernCapFamilyOfRank E r C sX n
(QuotientAddGroup.mk' (rationalEquivalences C sX n)
(cycleAssociatedToClosedSubscheme C sX (𝟙 X) n)) c
Stacks.Chow.chernClassFundamentalOfRank, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProjectiveBundleFormula/ChernClassesOfRank.lean, line 199. The attribute's comment: “part (2)”.
Stacks 02U0, part (2). The
i-th Chern class of a moduleℰof rankronX,c_i(ℰ) ∩ [X] = c_i ∈ A_{n-i}(X): thei-th member of the family of part (1).
def chernClassFundamentalOfRank (n : ℤ) (i : Fin (r + 1)) : chowGroup C sX (n - (i : ℤ))
Stacks.Chow.totalChernClassFundamentalOfRank, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProjectiveBundleFormula/ChernClassesOfRank.lean, line 221. The attribute's comment: “part (3)”.
Stacks 02U0, part (3). The total Chern class of a module of rank
ronX,c(ℰ) ∩ [X] = c_0(ℰ) ∩ [X] + … + c_r(ℰ) ∩ [X]inA_*(X) = ⊕_k A_k(X).
def totalChernClassFundamentalOfRank (n : ℤ) : ⨁ k : ℤ, chowGroup C sX k
Tag 02U1, an equation
Tag 02U1 in the Stacks Project.
Declarations registered for the tag:
ProjectiveBundleChernRelationregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleRelation.lean, line 294 (StacksFrontier): “Equation 42.37.1.1, the displayed relation of clause (1) of Definition 02U0:∑_{i=0}^{r} (-1)^i c₁(O_P(1))^i ∩ π^*c_{r-i} = 0, the condition on a family of Chow classes that Definition 02U0 solves to define the Chern classes of a rank-rfinite locally free module. The tag labels the displayed equation, which is this condition, so it is carried by the definition naming it;Stacks.Chow.IsChernCapFamilyconjoins it withc₀ = α.”.
Tag 02U2, a lemma
Tag 02U2 in the Stacks Project.
Stacks.Chow.chernClassCapFundamental_one_eq_firstChernClassCapFundamental, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDivisorClass.lean, line 313. The attribute's comment: “the projective bundle of the rank-one module L is the pair (X, 𝟙 X) and its twist O_P(1) is L itself, so the twist operator is CONSTRUCTED from L rather than assumed. The family of clause (1) of Stacks 02U0 is quantified over as a datum, its existence needing the surjectivity half of Stacks 02TX; it is not an assumption about the classes compared”.
Stacks 02U2. Let
(S, δ)be the base situation of chapter 42, letXbe locally of finite type overS, integral and of delta-dimensionn, and letLbe an invertible𝒪_X-module. Then the first Chern class ofLin the sense of Stacks 02U0 — the memberc_1of the family of clause (1), read on the projective bundle ofL, which isXitself with projection𝟙 Xand twistL— equals the Weil divisor class ofLof Stacks 02SJ (2).The proof is the source's. At
r = 1the relation 02U1 readsc₁(L) ∩ π^*c_0 = π^*c_1on the bundle; the bundle isXandπis the identity, so its flat pullback is the identity (Stacks.Chow.flatPullbackChow_id) and the relation saysc_1 = c₁(L) ∩ c_0. The normalisationc_0 = [X]turns the right-hand side into the cap product of Stacks 02SO on the fundamental cycle, which is the Weil divisor class byStacks.Chow.firstChernClassCapOfInvertible_fundamentalCycle_eq_firstChernClassCapFundamental.The twist operator is
Stacks.Chow.invertibleChernCapOperatorofL, the source'sO_{𝐏(L)}(1) = L, built from Stacks 02TI forL(Stacks.Chow.firstChernClassCap_factors); the familyDof clause (1) of Stacks 02U0 is a datum, quantified over rather than chosen. It is not an assumption about the two classes being compared.
theorem chernClassCapFundamental_one_eq_firstChernClassCapFundamental
(D : ChernClassFundamentalFamily C p p (𝟙 X) (Category.id_comp p) 1
(relativeDimension_identity X) (flatPullbackFactorsThroughRationalEquivalence_id C p)
(invertibleChernCapOperator C p L (firstChernClassCap_factors C p L)) n) :
chernClassCapFundamental C p p (𝟙 X) (Category.id_comp p) 1
(relativeDimension_identity X) (flatPullbackFactorsThroughRationalEquivalence_id C p)
(invertibleChernCapOperator C p L (firstChernClassCap_factors C p L)) n D ⟨1, by omega⟩ =
firstChernClassCapFundamental C p n hn L
Stacks.Chow.chernClassFundamentalOfRank_one_eq_firstChernClassCapFundamental, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProjectiveBundleFormula/ChernClassRankOne.lean, line 58.
Stacks 02U2. Let
Xbe locally of finite type over the base of a Chow situation, integral of delta-dimensionn, and letℒbe an invertible𝒪_X-module, so of rank one. The first Chern classc_1(ℒ) ∩ [X] ∈ A_{n-1}(X)of Stacks 02U0, defined by the relationc₁(𝒪_{𝐏(ℒ)}(1)) ∩ π^*c_0 = π^*c_1withc_0 = [X]on the projective bundle ofℒ, is the Weil divisor classc₁(ℒ) ∩ [X]of Stacks 02SJ.
theorem chernClassFundamentalOfRank_one_eq_firstChernClassCapFundamental :
letI := Stacks.ModuleDescent.isFiniteLocallyFreeOfRank_one_of_isInvertible X L inferInstance
chowGroupCast C p (show n - ((1 : Fin (1 + 1)) : ℤ) = n - 1 by simp)
(chernClassFundamentalOfRank L 1 C p n 1) =
firstChernClassCapFundamental C p n hn L
Sources
Section42.38 Intersecting with Chern classes#
Section 42.38 of the Stacks Project, Tag 02U4. 11 tags here are carried by 68 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02U5, a definition
Tag 02U5 in the Stacks Project.
Stacks.Chow.GenuineChern.chernCapOnCycles, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapOnCycles.lean, line 100. The attribute's comment: “the operation”.
Stacks 02U5. Intersection with the
j-th Chern class of a finite locally free module of rankr,c_j(ℰ) ∩ - : Z_k(X) ⟶ A_{k-j}(X), for the Chern classes of Stacks 02U0: the coefficientwise extension of[W] ↦ i_*(c_j(i^*ℰ) ∩ [W]).
def chernCapOnCycles (k : ℤ) (j : Fin (r + 1)) :
CycleGroup C sX k →+ chowGroup C sX (k - (j : ℤ))
Stacks.Chow.GenuineChern.chernCapOnCycles_integral_cycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapOnCycles.lean, line 109. The attribute's comment: “clause (1)”.
Stacks 02U5, clause (1), on Chow groups: for an integral closed subscheme
i : W ⟶ Xof delta-dimensionk,c_j(ℰ) ∩ [W] = i_*(c_j(i^*ℰ) ∩ [W]), with the classc_j(i^*ℰ) ∩ [W]of Stacks 02U0.
theorem chernCapOnCycles_integral_cycle (k : ℤ) (j : Fin (r + 1)) (W : X.IdealSheafData)
(hW : IsIntegral W.subscheme)
(hDim : schemeDeltaDimension C (W.subschemeι ≫ sX) = (k : EInt)) :
chernCapOnCycles C sX E r k j (cycleAssociatedToClosedSubscheme C sX W.subschemeι k) =
haveI := AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback W.subschemeι E r
properChowPushforward C (W.subschemeι ≫ sX) sX W.subschemeι rfl (k - (j : ℤ))
(properPushforwardFactorsThroughRationalEquivalence_of_isProper C _ sX _ rfl _)
(chernClassFundamentalOfRank ((Scheme.Modules.pullback W.subschemeι).obj E) r C
(W.subschemeι ≫ sX) k j)
Stacks.Chow.GenuineChern.chernCapOnCycles_finsum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapOnCycles.lean, line 128. The attribute's comment: “clause (2)”.
Stacks 02U5, clause (2), at the level of cycles: on a locally finite presentation
α = ∑ n_t [W_t]by integral closed subschemes of delta-dimensionk,c_j(ℰ) ∩ αis the class of∑ n_t i_{t,*}(c_j(i_t^*ℰ) ∩ [W_t]), for representatives of the classes of Stacks 02U0.
theorem chernCapOnCycles_finsum (k : ℤ) (j : Fin (r + 1)) {J : Type u}
(W : J → X.IdealSheafData) (hW : ∀ t, IsIntegral (W t).subscheme)
(hDim : ∀ t, schemeDeltaDimension C ((W t).subschemeι ≫ sX) = (k : EInt))
(hLocal : LocallyFinite fun t ↦ ((W t).support : Set X)) (n : J → ℤ)
(α : CycleGroup C sX k)
(hα : ∀ x : X, α.1 x = ∑ᶠ t : J, n t *
(cycleAssociatedToClosedSubscheme C sX (W t).subschemeι k).1 x) :
∃ β : CycleGroup C sX (k - (j : ℤ)),
chernCapOnCycles C sX E r k j α = QuotientAddGroup.mk β ∧
∀ x : X, β.1 x = ∑ᶠ t : J, n t *
(chernClassComponentCycle C sX E r
(fun g ↦ AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback g E r) k j
(chernCycleRule C r) (W t) (hW t) (hDim t)).1 x
Stacks.Chow.GenuineChern.chernCapOnCycles_locallyFiniteSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapOnCyclesLocallyFiniteSum.lean, line 137. The attribute's comment: “clause (2)”.
Stacks 02U5, clause (2). Let
α = ∑ n_t [W_t]be ak-cycle, presented by a locally finite family of integral closed subschemesi_t : W_t ⟶ Xof delta-dimensionk, and letγ_tbe any cycle onW_trepresentingc_j(i_t^*ℰ) ∩ [W_t], the class of Stacks 02U0. Then
i_{t,*} γ_trepresentsc_j(ℰ) ∩ [W_t]for everyt;- the locally finite sum
∑ n_t i_{t,*} γ_tis a cycle onX;- every cycle
βwith these coefficients representsc_j(ℰ) ∩ α;that is,
c_j(ℰ) ∩ α = ∑ n_t c_j(ℰ) ∩ [W_t], independently of the representatives.
theorem chernCapOnCycles_locallyFiniteSum (k : ℤ) (j : Fin (r + 1)) {J : Type u}
(W : J → X.IdealSheafData) (hW : ∀ t, IsIntegral (W t).subscheme)
(hDim : ∀ t, schemeDeltaDimension C ((W t).subschemeι ≫ sX) = (k : EInt))
(hLocal : LocallyFinite fun t ↦ ((W t).support : Set X)) (n : J → ℤ)
(α : CycleGroup C sX k)
(hα : ∀ x : X, α.1 x = ∑ᶠ t : J, n t *
(cycleAssociatedToClosedSubscheme C sX (W t).subschemeι k).1 x)
(γ : ∀ t, CycleGroup C ((W t).subschemeι ≫ sX) (k - (j : ℤ)))
(hγ : ∀ t, haveI := AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback (W t).subschemeι E r
QuotientAddGroup.mk' (rationalEquivalences C ((W t).subschemeι ≫ sX) (k - (j : ℤ))) (γ t) =
chernClassFundamentalOfRank ((Scheme.Modules.pullback (W t).subschemeι).obj E) r C
((W t).subschemeι ≫ sX) k j) :
(∀ t, QuotientAddGroup.mk' (rationalEquivalences C sX (k - (j : ℤ)))
(properPushforward C ((W t).subschemeι ≫ sX) sX (W t).subschemeι rfl (k - (j : ℤ))
(γ t)) =
chernCapOnCycles C sX E r k j (cycleAssociatedToClosedSubscheme C sX (W t).subschemeι k)) ∧
(∃ β : CycleGroup C sX (k - (j : ℤ)), ∀ x : X, β.1 x = ∑ᶠ t : J, n t *
(properPushforward C ((W t).subschemeι ≫ sX) sX (W t).subschemeι rfl (k - (j : ℤ))
(γ t)).1 x) ∧
∀ β : CycleGroup C sX (k - (j : ℤ)), (∀ x : X, β.1 x = ∑ᶠ t : J, n t *
(properPushforward C ((W t).subschemeι ≫ sX) sX (W t).subschemeι rfl (k - (j : ℤ))
(γ t)).1 x) →
chernCapOnCycles C sX E r k j α = QuotientAddGroup.mk β
Tag 02U6, a lemma
Tag 02U6 in the Stacks Project.
Stacks.Chow.exists_isChernCapFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleExistence.lean, line 157. The attribute's comment: “existence; carries the projective bundle as a flat morphism of relative dimension r - 1 with a first Chern class cap operator for its twist (Stacks 01O4, 02SO, 02TI), Stacks 02S1 for its projection, and the surjectivity half of Stacks 02TX”.
Granted the surjectivity of the projective space bundle map of Stacks 02TX, every class
α ∈ A_k(X)has a family of Chern class cap products: classesα_j ∈ A_{k-j}(X)withα_0 = αsatisfying the projective-bundle relation.
theorem exists_isChernCapFamily
(hsurj : ProjectiveBundleRelationSurjective C sX sP π hsP r hπ hfac twist) (k : ℤ)
(α : chowGroup C sX k) :
∃ c : ∀ j : Fin (r + 1), chowGroup C sX (k - (j : ℤ)),
IsChernCapFamily C sX sP π hsP r hπ hfac twist k α c
Stacks.Chow.existsUnique_isChernCapFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleExistence.lean, line 183. The attribute's comment: “existence and uniqueness together; carries the projective bundle as a flat morphism of relative dimension r - 1 with a first Chern class cap operator for its twist (Stacks 01O4, 02SO, 02TI), Stacks 02S1 for its projection, and both halves of Stacks 02TX”.
Granted both halves of Stacks 02TX, a class
α ∈ A_k(X)has exactly one family of Chern class cap products.
theorem existsUnique_isChernCapFamily
(hinj : ProjectiveBundleRelationInjective C sX sP π hsP r hπ hfac twist)
(hsurj : ProjectiveBundleRelationSurjective C sX sP π hsP r hπ hfac twist) (k : ℤ)
(α : chowGroup C sX k) :
∃! c : ∀ j : Fin (r + 1), chowGroup C sX (k - (j : ℤ)),
IsChernCapFamily C sX sP π hsP r hπ hfac twist k α c
Stacks.Chow.eq_of_isChernCapFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleRelation.lean, line 356. The attribute's comment: “uniqueness; carries the projective bundle as a flat morphism of relative dimension r - 1 with a first Chern class cap operator for its twist (Stacks 01O4, 02SO, 02TI), Stacks 02S1 for its projection, and the injectivity half of Stacks 02TX”.
Stacks 02U6, uniqueness. Granted the injectivity of the projective space bundle map of Stacks 02TX, there is at most one family of Chern class cap products of a given class: the relation together with the value in degree
kdetermines every member.This is the engine of the section: Stacks 02U7, 02U8, 02U9 and 0B7G are each proved by transporting the relation along an operation and appealing to this uniqueness.
theorem eq_of_isChernCapFamily (hinj : ProjectiveBundleRelationInjective C sX sP π hsP r hπ hfac
twist) (k : ℤ) (α : chowGroup C sX k)
{c d : ∀ j : Fin (r + 1), chowGroup C sX (k - (j : ℤ))}
(hc : IsChernCapFamily C sX sP π hsP r hπ hfac twist k α c)
(hd : IsChernCapFamily C sX sP π hsP r hπ hfac twist k α d) : c = d
Stacks.Chow.GenuineChern.isChernCapFamilyOfRank_chernCapOnCycles, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapOnCyclesCharacterization.lean, line 74.
Stacks 02U6. Let
ℰbe finite locally free of rankronX, with projective bundle(π : 𝐏(ℰ) ⟶ X, 𝒪_{𝐏(ℰ)}(1)), and letαbe ak-cycle onX. The classesc_j(ℰ) ∩ α ∈ A_{k-j}(X)of Stacks 02U5 satisfyα_0 = [α]and∑_{i=0}^{r} (-1)^i c₁(𝒪_{𝐏(ℰ)}(1))^i ∩ π^*(α_{r-i}) = 0in the Chow group of𝐏(ℰ), and they are the only family(α_j)_{0 ≤ j ≤ r},α_j ∈ A_{k-j}(X), doing so.
theorem isChernCapFamilyOfRank_chernCapOnCycles (k : ℤ) (α : CycleGroup C sX k) :
IsChernCapFamilyOfRank E r C sX k (QuotientAddGroup.mk' (rationalEquivalences C sX k) α)
(fun j ↦ chernCapOnCycles C sX E r k j α) ∧
∀ c : ∀ j : Fin (r + 1), chowGroup C sX (k - (j : ℤ)),
IsChernCapFamilyOfRank E r C sX k (QuotientAddGroup.mk' (rationalEquivalences C sX k) α)
c → c = fun j ↦ chernCapOnCycles C sX E r k j α
Tag 02U7, a lemma
Tag 02U7 in the Stacks Project.
Stacks.Chow.isChernCapFamily_rationallyEquivalent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleRelation.lean, line 391. The attribute's comment: “carries the projective bundle as a flat morphism of relative dimension r - 1 with a first Chern class cap operator for its twist (Stacks 01O4, 02SO, 02TI), Stacks 02S1 for its projection, the injectivity half of Stacks 02TX, and the cap products of Stacks 02U5 as families satisfying the characterization of Stacks 02U6”.
Stacks 02U7. If
αandβare rationally equivalentk-cycles onX, then the Chern class cap products ofαand ofβagree:c_j(ℰ) ∩ α = c_j(ℰ) ∩ βinA_{k-j}(X).The Stacks proof is exactly this: the two families are determined by the same equation in the Chow group of the projective bundle, which relies on flat pullback being compatible with rational equivalence, Stacks 02S1 — here the hypothesis
hfacthat produces the flat pullback of Stacks 0FVK in the first place.
theorem isChernCapFamily_rationallyEquivalent
(hinj : ProjectiveBundleRelationInjective C sX sP π hsP r hπ hfac twist) (k : ℤ)
(α β : CycleGroup C sX k) (hαβ : RationallyEquivalent C sX k α β)
{c d : ∀ j : Fin (r + 1), chowGroup C sX (k - (j : ℤ))}
(hc : IsChernCapFamily C sX sP π hsP r hπ hfac twist k
(QuotientAddGroup.mk' (rationalEquivalences C sX k) α) c)
(hd : IsChernCapFamily C sX sP π hsP r hπ hfac twist k
(QuotientAddGroup.mk' (rationalEquivalences C sX k) β) d) : c = d
Stacks.Chow.GenuineChern.chernCapOnCycles_eq_of_rationallyEquivalent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapOnCyclesDescent.lean, line 390.
Stacks 02U7. Rationally equivalent
k-cycles have the same cap products with the Chern classes: the operation of Stacks 02U5 factors throughA_k(X).
theorem chernCapOnCycles_eq_of_rationallyEquivalent (k : ℤ) (j : Fin (r + 1))
(α β : CycleGroup C sX k) (h : RationallyEquivalent C sX k α β) :
chernCapOnCycles C sX E r k j α = chernCapOnCycles C sX E r k j β
Tag 02U9, a lemma
Tag 02U9 in the Stacks Project.
Stacks.Chow.isChernCapFamily_properPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleProperPushforward.lean, line 214. The attribute's comment: “carries both projective bundles as flat morphisms of relative dimension r - 1 with first Chern class cap operators for their twists (Stacks 01O4, 02SO, 02TI), Stacks 02S1 for their projections, a proper morphism between the two bundles lying over p, the injectivity half of Stacks 02TX over the target, the compatibility of the summands of the relation with proper pushforward (Stacks 02SU and Stacks 02RG), and the cap products of Stacks 02U5 as families satisfying the characterization of Stacks 02U6”.
Stacks 02U9. Proper pushforward commutes with the Chern class cap products: if
cis the family of Chern class cap products ofα ∈ A_k(X)forp^*ℰandeis the family of Chern class cap products ofp_*α ∈ A_k(Y)forℰ, thene_j = p_*(c_j), that is
c_j(ℰ) ∩ p_*α = p_*(c_j(p^*ℰ) ∩ α).The proof is the one in the source: the proper pushforward of
csatisfies the relation overYand hasp_*αin degreek, so the uniqueness of Stacks 02U6 identifies it withe.
theorem isChernCapFamily_properPushforward
(hinjY : ProjectiveBundleRelationInjective C sY sPY πY hsPY r hπY hfacY twistY)
(hcompat : ChernTermsCompatibleWithPushforward C sX sY sPX sPY πX hsPX πY hsPY r hπX hπY
hfacX hfacY twistX twistY p hp p' hp') (k : ℤ)
(α : chowGroup C sX k) (c : ∀ j : Fin (r + 1), chowGroup C sX (k - (j : ℤ)))
(e : ∀ j : Fin (r + 1), chowGroup C sY (k - (j : ℤ)))
(hc : IsChernCapFamily C sX sPX πX hsPX r hπX hfacX twistX k α c)
(he : IsChernCapFamily C sY sPY πY hsPY r hπY hfacY twistY k
(properChowPushforward C sX sY p hp k
(properPushforwardFactorsThroughRationalEquivalence_of_isProper C sX sY p hp k) α) e) :
e = properPushforwardChernFamily C sX sY r p hp k c
Stacks.Chow.GenuineChern.properChowPushforward_chernCapOnCycles, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapOnCyclesCharacterization.lean, line 90.
Stacks 02U9. Let
p : X ⟶ Ybe a proper morphism of schemes locally of finite type overS,ℰfinite locally free of rankronYandαak-cycle onX. Thenp_*(c_j(p^*ℰ) ∩ α) = c_j(ℰ) ∩ p_*αinA_{k-j}(Y).
theorem properChowPushforward_chernCapOnCycles {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) (E : Y.Modules) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r] (k : ℤ)
(j : Fin (r + 1)) (α : CycleGroup C sX k) :
haveI := AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback p E r
properChowPushforward C sX sY p hp (k - (j : ℤ))
(properPushforwardFactorsThroughRationalEquivalence_of_isProper C sX sY p hp _)
(chernCapOnCycles C sX ((Scheme.Modules.pullback p).obj E) r k j α) =
chernCapOnCycles C sY E r k j (properPushforward C sX sY p hp k α)
Tag 02U8, a lemma
Tag 02U8 in the Stacks Project.
Stacks.Chow.isChernCapFamily_flatPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleFlatPullback.lean, line 202. The attribute's comment: “carries both projective bundles as flat morphisms of relative dimension r - 1 with first Chern class cap operators for their twists (Stacks 01O4, 02SO, 02TI), Stacks 02S1 for the three flat morphisms, the injectivity half of Stacks 02TX over X, the compatibility of the summands with flat pullback (Stacks 02SS and 02RD), and the cap products of Stacks 02U5 as families satisfying the characterization of Stacks 02U6”.
Flat pullback commutes with the Chern class cap products. Assume the injectivity
hinjXof the projective-bundle relation overXand the compatibilityhcompatof its summands with flat pullback. Ifcis the family of Chern class cap products ofα ∈ A_k(Y)forℰandeis the family of Chern class cap products off^*α ∈ A_{k+d}(X)forf^*ℰ, thene_j = f^*(c_j), that is
c_j(f^*ℰ) ∩ f^*α = f^*(c_j(ℰ) ∩ α).
theorem isChernCapFamily_flatPullback
(hinjX : ProjectiveBundleRelationInjective C sX sPX πX hsPX r hπX hfacX twistX)
(hcompat : ChernTermsCompatibleWithFlatPullback C sX sY sPX sPY πX hsPX πY hsPY r hπX hπY
hfacX hfacY twistX twistY f hf d hd hfacf f' hf' hd' hfacf') (k : ℤ)
(α : chowGroup C sY k) (c : ∀ j : Fin (r + 1), chowGroup C sY (k - (j : ℤ)))
(e : ∀ j : Fin (r + 1), chowGroup C sX (k + (d : ℤ) - (j : ℤ)))
(hc : IsChernCapFamily C sY sPY πY hsPY r hπY hfacY twistY k α c)
(he : IsChernCapFamily C sX sPX πX hsPX r hπX hfacX twistX (k + (d : ℤ))
(flatPullbackChow C sX sY f hf d hd k (hfacf k) α) e) :
e = flatPullbackChernFamily C sX sY r f hf d hd hfacf k c
Stacks.Chow.GenuineChern.flatPullbackChow_chernCapOnCycles, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapOnCyclesCharacterization.lean, line 112.
Stacks 02U8. Let
f : X ⟶ Ybe a flat morphism of relative dimensiondbetween schemes locally of finite type overS,ℰfinite locally free of rankronYandαak-cycle onY. Thenf^*(c_j(ℰ) ∩ α) = c_j(f^*ℰ) ∩ f^*αinA_{k+d-j}(X). The source takesd = r; the relative dimension is arbitrary here.
theorem flatPullbackChow_chernCapOnCycles {X Y : Scheme.{u}} (sX : X ⟶ C.S)
[LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : X ⟶ Y)
[LocallyOfFiniteType f] [Flat f] (hf : f ≫ sY = sX) (d : ℕ)
(hd : AlgebraicGeometry.RelativeDimension f d) (E : Y.Modules) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r] (k : ℤ)
(j : Fin (r + 1)) (α : CycleGroup C sY k) :
haveI := AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback f E r
flatPullbackChow C sX sY f hf d hd (k - (j : ℤ))
(flatPullbackFactorsThroughRationalEquivalence_general C sX sY f hf d hd _)
(chernCapOnCycles C sY E r k j α) =
chowGroupCast C sX (by ring)
(chernCapOnCycles C sX ((Scheme.Modules.pullback f).obj E) r (k + d) j
(flatPullback C sX sY f hf d hd k α))
Stacks.Chow.GenuineChern.chernCap_flatPullback_heq_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapRuleFlatGeneral.lean, line 46. The attribute's comment: “Stated for a module on Y identified with the pullback of E, as a heterogeneous equality between the Chow groups of the two equal degrees (k + d) - j and (k - j) + d.”.
Stacks 02U8 for the cap products of Stacks 02U6, in every rank. For
f : Y ⟶ Xflat of relative dimensiondover the base,ℰof rankronXandℰ' ≅ f^*ℰ,
c_j(ℰ') ∩ f^*α = f^*(c_j(ℰ) ∩ α),as a heterogeneous equality: the two sides lie in
A_{(k+d)-j}(Y)andA_{(k-j)+d}(Y). The flat pullbacks are those ofStacks.Chow.flatPullbackChow, through the factorization through rational equivalence that holds in every degree.
theorem chernCap_flatPullback_heq_general {X Y : Scheme.{u}} (sX : X ⟶ C.S)
[LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : Y ⟶ X)
[LocallyOfFiniteType f] [Flat f] (hf : f ≫ sX = sY) (d : ℕ)
(hd : AlgebraicGeometry.RelativeDimension f d) (E : X.Modules) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r]
(E' : Y.Modules)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E' r]
(eE : E' ≅ (Scheme.Modules.pullback f).obj E) (k : ℤ) (j : Fin (r + 1))
(α : chowGroup C sX k) :
chernCap C r sY E' (k + d) j (flatPullbackChow C sY sX f hf d hd k
(flatPullbackFactorsThroughRationalEquivalence_general C sY sX f hf d hd k) α) ≍
flatPullbackChow C sY sX f hf d hd (k - (j : ℤ))
(flatPullbackFactorsThroughRationalEquivalence_general C sY sX f hf d hd _)
(chernCap C r sX E k j α)
Tag 0B7G, a lemma
Tag 0B7G in the Stacks Project.
Stacks.Chow.GenuineChern.chernCapOnCycles_gysin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapOnCyclesGysin.lean, line 63.
Stacks 0B7G. Let
ℰbe finite locally free of rankronXand let(ℒ, s, i : D ⟶ X)be as in Definition 02T8. Letα ∈ A_{k+1}(X), letabe a cycle representingαandba cycle representingi^*α ∈ A_k(D). Then for every0 ≤ j ≤ r
c_j(ℰ|_D) ∩ b = i^*(c_j(ℰ) ∩ a)inA_{k-j}(D),for the Gysin map of Stacks 02TO and intersection with Chern classes of Stacks 02U5; that is,
c_j(ℰ|_D) ∩ i^*α = i^*(c_j(ℰ) ∩ α).
theorem chernCapOnCycles_gysin (E : X.Modules) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r] (k : ℤ)
(j : Fin (r + 1)) (α : chowGroup C sX (k + 1)) (a : CycleGroup C sX (k + 1))
(ha : QuotientAddGroup.mk' (rationalEquivalences C sX (k + 1)) a = α)
(b : CycleGroup C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ sX) k)
(hb : QuotientAddGroup.mk'
(rationalEquivalences C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ sX) k) b =
gysinChowOfInvertible C sX k L s α) :
letI := AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback
(Stacks.Divisors.zeroScheme X L s).subschemeι E r
chernCapOnCycles C ((Stacks.Divisors.zeroScheme X L s).subschemeι ≫ sX)
((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme X L s).subschemeι).obj E) r k j b =
gysinChowOfInvertible C sX (k - (j : ℤ)) L s
(chowGroupCast C sX (show k + 1 - (j : ℤ) = k - (j : ℤ) + 1 by omega)
(chernCapOnCycles C sX E r (k + 1) j a))
Stacks.Chow.GenuineChern.chernCap_gysin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/CapRuleGysin.lean, line 240.
Stacks 0B7G. Let
ℰbe finite locally free of rankronYand let(ℒ, s, i : D ⟶ Y)be a triple as in Definition 02T8. Then for every0 ≤ j ≤ rand everyα ∈ A_{k+1}(Y)
c_j(ℰ|_D) ∩ i^*α = i^*(c_j(ℰ) ∩ α)inA_{k-j}(D),for the Chern class cap products of Stacks 02U6 and the Gysin map of Stacks 02TO.
theorem chernCap_gysin (E : Y.Modules) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r] (k : ℤ)
(j : Fin (r + 1)) (α : chowGroup C sY (k + 1)) :
letI := AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback
(Stacks.Divisors.zeroScheme Y L s).subschemeι E r
chernCap C r ((Stacks.Divisors.zeroScheme Y L s).subschemeι ≫ sY)
((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme Y L s).subschemeι).obj E) k j
(gysinChowOfInvertible C sY k L s α) =
gysinChowOfInvertible C sY (k - (j : ℤ)) L s
(chowGroupCast C sY (show k + 1 - (j : ℤ) = k - (j : ℤ) + 1 by omega)
(chernCap C r sY E (k + 1) j α))
Tag 0B7H, a lemma
Tag 0B7H in the Stacks Project.
Stacks.Chow.GenuineChern.chernClassBivariantClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/BivariantChernClass.lean, line 77.
For a finite locally free module
ℰof rankronXand0 ≤ j ≤ r, the rule assigning tof : X' ⟶ Xthe operationc_j(f^*ℰ) ∩ - : A_k(X') ⟶ A_{k-j}(X')is a bivariant class of degreej: the classc_j(ℰ) ∈ A^j(X)together with its characterization.
def chernClassBivariantClass :
{c : BivariantClass C (gysinSystemOfInvertible C) sX sX (𝟙 X) (Category.id_comp sX) (j : ℤ) //
IsChernClassBivariant C sX F r (gysinSystemOfInvertible C) (chernCap C r)
(pullbackPreservesRank_of_isFiniteLocallyFreeOfRank F r) j c}
Stacks.Chow.GenuineChern.chernClassBivariantClassOnCycles, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/BivariantChernClassOnCycles.lean, line 62.
Stacks 0B7H. For a locally free module
ℰof rankronXand0 ≤ j ≤ r, the rule assigning tof : X' ⟶ Xthe operationc_j(f^*ℰ) ∩ - : A_k(X') ⟶ A_{k-j}(X')of Stacks 02U5 is a bivariant class of degreej: a classc ∈ A^j(X)withc ∩ [α] = c_j(f^*ℰ) ∩ αfor everyf : X' ⟶ Xand everyk-cycleαonX', the cap operation being read onX'through the identificationX ×_X X' ≅ X'.
def chernClassBivariantClassOnCycles :
{c : BivariantClass C (gysinSystemOfInvertible C) sX sX (𝟙 X) (Category.id_comp sX) (j : ℤ) //
∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
(α : CycleGroup C (g ≫ sX) k),
letI := AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback g F r
chowPushforwardOfIso C (pullback.fst (𝟙 X) g ≫ sX) (g ≫ sX)
(identityBaseChangeIso g).hom (identityBaseChangeIso_hom_comp_base C sX g)
(k - (j : ℤ)) (c.cap g k (QuotientAddGroup.mk' (rationalEquivalences C (g ≫ sX) k) α)) =
chernCapOnCycles C (g ≫ sX) ((Scheme.Modules.pullback g).obj F) r k j α}
Tag 0FE1, a definition
Tag 0FE1 in the Stacks Project.
Stacks.Chow.chernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/TotalChernClassOfModule.lean, line 127. The attribute's comment: “c_i(E) is the degree-i bivariant class of Stacks 0B7H”.
Stacks 0FE1, the
i-th Chern class. For0 ≤ i ≤ r, thei-th Chern classc_i(ℰ) ∈ A^i(X)of a moduleℰthat is finite locally free of rankr: it is the bivariant class of degreeifor𝟙 Xconstructed in Stacks 0B7H, namely the rule assigning tof : X' ⟶ Xthe operationc_i(f^*ℰ) ∩ - : CH_k(X') ⟶ CH_{k-i}(X').
def chernClass (i : Fin (r + 1)) :
BivariantClass C G sX sX (𝟙 X) (Category.id_comp sX) (i : ℤ)
Stacks.Chow.totalChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/TotalChernClassOfModule.lean, line 165. The attribute's comment: “c(E) = c_0(E) + ... + c_r(E) is the formal sum of the c_i(E)”.
Stacks 0FE1, the total Chern class. The total Chern class
c(ℰ) = c_0(ℰ) + c_1(ℰ) + ⋯ + c_r(ℰ)of a moduleℰthat is finite locally free of rankr: the formal sum of ther + 1Chern classes of Stacks 0B7H, viewed as a nonhomogeneous bivariant class onX, that is, as an element ofA^*(X ⟶ X) = ⊕_p A^p(X ⟶ X).
def totalChernClass : nonhomogeneousBivariantGroup C G sX sX (𝟙 X) (Category.id_comp sX)
Stacks.Chow.canonicalChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/TotalChernClassOfModule.lean, line 101. The attribute's comment: “c_i(E) ∈ A^i(X), the degree-i bivariant class of Stacks 0B7H, with the genuine cap products of Stacks 02U6 and the canonical Gysin system; nothing assumed”.
Stacks 0FE1, the
i-th Chern class. For a moduleℰthat is finite locally free of rankronXand0 ≤ i ≤ r, thei-th Chern classc_i(ℰ) ∈ A^i(X): the bivariant class of degreeifor𝟙 Xconstructed in Stacks 0B7H, which assigns tof : X' ⟶ Xthe operationc_i(f^*ℰ) ∩ - : A_k(X') ⟶ A_{k-i}(X')of Stacks 02U6. It lives in the group of Stacks 0B76 at the canonical Gysin system, and every naturality fact the construction needs is proved.
def canonicalChernClass (i : Fin (r + 1)) :
CanonicalBivariantClass C sX sX (𝟙 X) (Category.id_comp sX) (i : ℤ)
Stacks.Chow.canonicalTotalChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/TotalChernClassOfModule.lean, line 144. The attribute's comment: “c(E) = c_0(E) + ... + c_r(E), the formal sum of the c_i(E) as a nonhomogeneous bivariant class on X, with the genuine cap products and the canonical Gysin system; nothing assumed”.
Stacks 0FE1, the total Chern class. For a module
ℰthat is finite locally free of rankronX, the total Chern classc(ℰ) = c_0(ℰ) + c_1(ℰ) + ⋯ + c_r(ℰ): the formal sum of ther + 1Chern classes of Stacks 0B7H, viewed as a nonhomogeneous bivariant class onX, that is, as an element ofA^*(X ⟶ X) = ⊕_p A^p(X ⟶ X)at the canonical Gysin system. Nothing is assumed.
def canonicalTotalChernClass :
nonhomogeneousBivariantGroup C (canonicalGysinSystem C) sX sX (𝟙 X) (Category.id_comp sX)
Tag 02UA, a lemma
Tag 02UA in the Stacks Project.
Stacks.Chow.isChernCapFamily_bivariantClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleBivariantClass.lean, line 342. The attribute's comment: “clause (2), read on a test scheme; carries both projective bundles as flat morphisms of relative dimension r - 1 with first Chern class cap operators for their twists (01O4, 02SO, 02TI, 02S1), the injectivity half of 02TX downstairs, the compatibility of the summands with the cap product of the bivariant class (0B7B), and 02U5 as 02U6-families”.
Stacks 02UA (2). A bivariant class carries the Chern class cap products of
ℰto those off^*ℰ: ifdis the family of Chern class cap products ofα ∈ A_k(T)forℰ|_Tandeis the family of Chern class cap products ofc ∩ α ∈ A_{k-p}(T ×_X X')for the pullback ofℰ, thene_j = c ∩ d_j, that is
c_j(f^*ℰ) ∩ (c ∩ α) = c ∩ (c_j(ℰ) ∩ α),which is the identity
c ∘ c_j(ℰ) = c_j(f^*ℰ) ∘ cof the tag, read on the test schemeg.The proof is the one in the source: the cap product of
cwithdsatisfies the relation downstairs and hasc ∩ αin degreek - p, so the uniqueness of Stacks 02U6 identifies it withe.
theorem isChernCapFamily_bivariantClass
(hinj' : ProjectiveBundleRelationInjective C (pullback.fst f g ≫ sX')
(pullback.fst f (πT ≫ g) ≫ sX') πT' hsPT' r hπT' hfacT' twistT')
(hcompat : ChernTermsCompatibleWithBivariantClass C G sX' sX f hf p c g πT hsPT πT' hsPT' r
hπT hπT' hfacT hfacT' twistT twistT') (k : ℤ) (α : chowGroup C (g ≫ sX) k)
(d : ∀ j : Fin (r + 1), chowGroup C (g ≫ sX) (k - (j : ℤ)))
(e : ∀ j : Fin (r + 1), chowGroup C (pullback.fst f g ≫ sX') (k - p - (j : ℤ)))
(hd : IsChernCapFamily C (g ≫ sX) ((πT ≫ g) ≫ sX) πT hsPT r hπT hfacT twistT k α d)
(he : IsChernCapFamily C (pullback.fst f g ≫ sX') (pullback.fst f (πT ≫ g) ≫ sX') πT' hsPT'
r hπT' hfacT' twistT' (k - p) (c.cap g k α) e) :
e = bivariantChernFamily C G sX' sX f hf p c g r k d
Stacks.Chow.chernCapOnChow_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleBivariantClass.lean, line 435. The attribute's comment: “the 'in particular' clause, for the cap products of Stacks 02U6; carries both projective bundles of F and that of E as flat morphisms of relative dimension one less than the rank, with first Chern class cap operators for their twists (01O4, 02SO, 02TI, 02S1), both halves of 02TX, and the commutation of c_j(F) with the summands of E's relation (02SS and 02U8)”.
The "in particular" of Stacks 02UA. The Chern class cap products of two finite locally free modules commute:
c_i(ℰ) ∩ (c_j(ℱ) ∩ α) = c_j(ℱ) ∩ (c_i(ℰ) ∩ α)inA_{k-j-i}(X)for every
α ∈ A_k(X), which is the displayed identity of the tag.The proof is the one in the source, with
c = c_j(ℱ) ∩ -playing the role of the bivariant class of clause (2): the family(c_j(ℱ) ∩ (c_i(ℰ) ∩ α))_isatisfies the relation of Stacks 02U6 overXfor the classc_j(ℱ) ∩ α, because capping withc_j(ℱ)carries each summand of the relation to itself, and its zeroth member isc_j(ℱ) ∩ α; so the uniqueness of Stacks 02U6 identifies it with the family(c_i(ℰ) ∩ (c_j(ℱ) ∩ α))_i.
theorem chernCapOnChow_comm
(hinj : ProjectiveBundleRelationInjective C sX sP π hsP r hπ hfac twist)
(hsurj : ProjectiveBundleRelationSurjective C sX sP π hsP r hπ hfac twist)
(hcompat : ChernTermsCompatibleWithChernCap C sX sP sQ sQP π hsP r hπ hfac twist ρ hsQ s hρ
hfacQ twistQ ρP hsQP hρP hfacQP twistQP hinjQ hsurjQ hinjQP hsurjQP j)
(k : ℤ) (α : chowGroup C sX k) (i : Fin (r + 1)) :
chernCapOnChow C sX sP π hsP r hπ hfac twist hinj hsurj (k - (j : ℤ)) i
(chernCapOnChow C sX sQ ρ hsQ s hρ hfacQ twistQ hinjQ hsurjQ k j α) =
chowGroupCast C sX (show k - (i : ℤ) - (j : ℤ) = k - (j : ℤ) - (i : ℤ) from by omega)
(chernCapOnChow C sX sQ ρ hsQ s hρ hfacQ twistQ hinjQ hsurjQ (k - (i : ℤ)) j
(chernCapOnChow C sX sP π hsP r hπ hfac twist hinj hsurj k i α))
Stacks.Chow.BivariantClass.heq_bivariantCompositeOfInvertible_chernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleBivariantClassGenuine.lean, line 386. The attribute's comment: “(2), for a homogeneous c in A^p(X' -> X), the bivariant Chern classes of Stacks 0B7H and the composition of Stacks 0B75 at the Gysin system of the first Chern class of an invertible module; the two composites are classes for f ≫ 𝟙 X and 𝟙 X' ≫ f of degrees p + j and j + p, whence the heterogeneous equality”.
Stacks 02UA (2). Let
f : X' ⟶ Xbe locally of finite type, letc ∈ A^p(X' ⟶ X)and letℰbe finite locally free of rankronX. Then for0 ≤ j ≤ r
c ∘ c_j(ℰ) = c_j(f^*ℰ) ∘ cinA^{p+j}(X' ⟶ X),the composites being those of Stacks 0B75, classes for the equal morphisms
f ≫ 𝟙 Xand𝟙 X' ≫ fof the equal degreesp + jandj + p.
theorem BivariantClass.heq_bivariantCompositeOfInvertible_chernClass
(c : BivariantClass C (gysinSystemOfInvertible C) sX' sX f hf p) (F : X.Modules) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F r]
(j : Fin (r + 1)) :
letI := pullbackPreservesRank_of_isFiniteLocallyFreeOfRank F r f
bivariantCompositeOfInvertible C sX' sX sX f (𝟙 X) hf (Category.id_comp sX) p j c
(GenuineChern.chernClass C sX F r j) ≍
bivariantCompositeOfInvertible C sX' sX' sX (𝟙 X') f (Category.id_comp sX') hf j p
(GenuineChern.chernClass C sX' ((Scheme.Modules.pullback f).obj F) r j) c
Stacks.Chow.BivariantClass.heq_mulId_chernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassHigher/ProjectiveBundleBivariantClassGenuine.lean, line 408. The attribute's comment: “(1), for the product of A^*(X) given by the composition of Stacks 0B75 at the Gysin system of the first Chern class of an invertible module, against every homogeneous c in A^q(X); the two products have degrees q + j and j + q, whence the heterogeneous equality”.
Stacks 02UA (1). The Chern class
c_j(ℰ) ∈ A^j(X)of a finite locally free module of rankris in the center ofA^*(X): for everyc ∈ A^q(X),
c · c_j(ℰ) = c_j(ℰ) · c,the two products lying in
A^{q+j}(X)andA^{j+q}(X).
theorem BivariantClass.heq_mulId_chernClass {q : ℤ}
(c : BivariantClass C (gysinSystemOfInvertible C) sX sX (𝟙 X) (Category.id_comp sX) q)
(F : X.Modules) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F r]
(j : Fin (r + 1)) :
c.mulId C sX (GenuineChern.chernClass C sX F r j) ≍
(GenuineChern.chernClass C sX F r j).mulId C sX c
Stacks.Chow.GenuineChern.comp_chernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/BivariantChernCentral.lean, line 124. The attribute's comment: “(2): c ∘ c_j(E) = c_j(f^*E) ∘ c in A^{p+j}(X' → X) for every f : X' → X locally of finite type and every bivariant class c in A^p(X' → X) of Stacks 0B76”.
Stacks 02UA (2). Let
ℰbe a locally free𝒪_X-module of rankr, letf : X' ⟶ Xbe locally of finite type and letc ∈ A^p(X' ⟶ X)be a bivariant class. Then
c ∘ c_j(ℰ) = c_j(f^*ℰ) ∘ cinA^{p+j}(X' ⟶ X),with
c_j(ℰ) ∈ A^j(X)andc_j(f^*ℰ) ∈ A^j(X')the bivariant Chern classes of Stacks 0B7H. The left side is a class forf ≫ 𝟙 Xof degreep + j; the right side, a class for𝟙 X' ≫ fof degreej + p, is read as one forf ≫ 𝟙 Xof degreep + jalong the identity ofX'.
theorem comp_chernClass {X' : Scheme.{u}} {sX' : X' ⟶ C.S} [LocallyOfFiniteType sX']
(F : X.Modules) (r : ℕ) [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F r]
(j : Fin (r + 1)) (f : X' ⟶ X) (hf : f ≫ sX = sX') {p : ℤ}
(c : BivariantChowClass C sX' sX f hf p) :
letI := AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback f F r
c.comp (BivariantChowClass.equivBivariantClass.symm (chernClass C sX F r j)) =
(((BivariantChowClass.equivBivariantClass.symm
(chernClass C sX' ((Scheme.Modules.pullback f).obj F) r j)).comp c).degreeCongr
(add_comm (j : ℤ) p)).transport (comp_comp_structureMorphism_eq hf (Category.id_comp sX))
(Iso.refl X') (by simp)
Stacks.Chow.GenuineChern.chernClass_mem_center, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/BivariantChernCentral.lean, line 229. The attribute's comment: “(1): c_j(E) in A^j(X) is in the center of the Chow cohomology ring A^*(X) of Stacks 0B7E, for the bivariant Chern class of Stacks 0B7H”.
Stacks 02UA (1). The
j-th Chern classc_j(ℰ) ∈ A^j(X)of a locally free𝒪_X-module of rankrlies in the center of the Chow cohomology ringA^*(X)of Stacks 0B7E.
theorem chernClass_mem_center (F : X.Modules) (r : ℕ)
[SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F r] (j : Fin (r + 1)) :
letI : Ring (chowCohomology C (gysinSystemOfInvertible C) sX) :=
chowCohomologyRingOfInvertible C sX
DirectSum.of (fun q : ℤ ↦ chowCohomologyComponent C (gysinSystemOfInvertible C) sX q) (j : ℤ)
(chernClass C sX F r j) ∈
Subring.center (chowCohomology C (gysinSystemOfInvertible C) sX)
Declarations registered for the tag:
Stacks.Chow.GenuineChern.chernCap_chernCap_comm, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/BivariantChernCentral.lean, line 252 (StacksFrontier): “the 'in particular': c_i(E) ∩ c_j(F) ∩ α = c_j(F) ∩ c_i(E) ∩ α in CH_{k-i-j}(X) for locally free E, F of ranks r, s and every α in CH_k(X)”.
Tag 0ESW, a remark
Tag 0ESW in the Stacks Project.
Stacks.Chow.chernClassArbitraryRank, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/Basic.lean, line 294. The attribute's comment: “chern_classes_arbitrary_rank; the constant-rank Chern classes the remark cites enter as a quantified family; the classes of Tag 0B7H themselves are Stacks.Chow.GenuineChern.chernClassBivariantClass”.
Stacks 0ESW. The
n-th Chern classc_n(E) ∈ A^n(X)of a finite locally free module of not necessarily constant rank: the class which preserves the product decomposition of Chow cohomology along the rank loci and whose component onX_risc_n(E|_{X_r}).
def chernClassArbitraryRank (n : ℕ) : chowCohomologyComponent C G sX (n : ℤ)
Stacks.Chow.rankLocusRestriction_chernClassArbitraryRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/Basic.lean, line 301. The attribute's comment: “chern_classes_arbitrary_rank; the constant-rank Chern classes the remark cites enter as a quantified family; the classes of Tag 0B7H themselves are Stacks.Chow.GenuineChern.chernClassBivariantClass”.
Stacks 0ESW. The component of
c_n(E)on the rank-rlocus isc_n(E|_{X_r}), and is zero whenr < n.
theorem rankLocusRestriction_chernClassArbitraryRank (n r : ℕ) :
rankLocusRestriction C G sX E hgysO (n : ℤ)
(chernClassArbitraryRank C G sX E hgysO hgysR hgysC cc n) r =
rankLocusChernFamily C G sX E cc n r
Stacks.Chow.isChernClassBivariant_rankLocusRestriction_chernClassArbitraryRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/Basic.lean, line 311. The attribute's comment: “chern_classes_arbitrary_rank; the constant-rank Chern classes the remark cites enter as a quantified family; the classes of Tag 0B7H themselves are Stacks.Chow.GenuineChern.chernClassBivariantClass”.
Stacks 0ESW. On the rank-
rlocus,c_n(E)acts by the already defined operationc_n(E|_{X_r}) ∩ -: its component there satisfies the characterization of Stacks 0B7H for the restricted module.
theorem isChernClassBivariant_rankLocusRestriction_chernClassArbitraryRank
(hcc : ∀ (r : ℕ) (j : Fin (r + 1)),
IsChernClassBivariant C ((rankLocus E r).ι ≫ sX)
((Scheme.Modules.pullback (rankLocus E r).ι).obj E) r G (caps r) (hrank r) j (cc r j))
(n r : ℕ) (h : n ≤ r) :
IsChernClassBivariant C ((rankLocus E r).ι ≫ sX)
((Scheme.Modules.pullback (rankLocus E r).ι).obj E) r G (caps r) (hrank r)
⟨n, Nat.lt_succ_of_le h⟩
(rankLocusRestriction C G sX E hgysO (n : ℤ)
(chernClassArbitraryRank C G sX E hgysO hgysR hgysC cc n) r)
Stacks.Chow.eq_chernClassArbitraryRank_of_rankLocusRestriction_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/Basic.lean, line 329. The attribute's comment: “chern_classes_arbitrary_rank; the constant-rank Chern classes the remark cites enter as a quantified family; the classes of Tag 0B7H themselves are Stacks.Chow.GenuineChern.chernClassBivariantClass”.
Stacks 0ESW.
c_n(E)is the only class with these components, so the definition does not depend on the way the family is assembled.
theorem eq_chernClassArbitraryRank_of_rankLocusRestriction_eq (n : ℕ)
{c : chowCohomologyComponent C G sX (n : ℤ)}
(h : ∀ r : ℕ, rankLocusRestriction C G sX E hgysO (n : ℤ) c r =
rankLocusChernFamily C G sX E cc n r) :
c = chernClassArbitraryRank C G sX E hgysO hgysR hgysC cc n
Stacks.Chow.exists_infinite_chernClassOfLocallyFree_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/InfinitelyManyChernClasses.lean, line 398. The attribute's comment: “it may happen that c_p(E) is nonzero for infinitely many p”.
The Chern classes of a module of non-constant rank can be nonzero in infinitely many degrees. There are a base situation
(S, δ)of chapter 42, a schemeXlocally of finite type overSand a finite locally free𝒪_X-moduleℰsuch thatc_p(ℰ) ≠ 0for infinitely manyp.
theorem exists_infinite_chernClassOfLocallyFree_ne_zero :
∃ (C : ChowSituation.{u}) (X : Scheme.{u}) (sX : X ⟶ C.S) (_ : LocallyOfFiniteType sX)
(E : X.Modules) (_ : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E),
{p : ℕ | SectionZeroScheme.chernClassOfLocallyFree E C sX p ≠ 0}.Infinite
Stacks.Chow.SectionZeroScheme.rankLocusChowCohomologyEquivOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/LocallyFreeRemark.lean, line 82. The attribute's comment: “A^p(X) = ∏_r A^p(X_r) for the rank decomposition X = ∐ X_r of a finite locally free module (via 0FDZ), at the Gysin system of the first Chern class rule, nothing assumed”.
Stacks 0ESW, the decomposition of Chow cohomology.
A^p(X) = ∏_{r ≥ 0} A^p(X_r)for the decomposition ofXby the rank ofℰ: restriction to the rank loci is an isomorphism onto the product (Stacks 0FDZ).
def rankLocusChowCohomologyEquivOfInvertible (p : ℤ) :
chowCohomologyComponent C (gysinSystemOfInvertible C) sX p ≃+
∀ r : ℕ, chowCohomologyComponent C (gysinSystemOfInvertible C) ((rankLocus E r).ι ≫ sX) p
Stacks.Chow.SectionZeroScheme.idRule_chernClassOfLocallyFree_of_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/LocallyFreeRemark.lean, line 178. The attribute's comment: “c_p(E) acts on the factors X'_r by the already defined operations c_p(E|_{X'_r}) ∩ -: on every test scheme along which E has constant rank r the operation of c_p(E) is the cap product c_p(f^*E) ∩ - of 0B7H (zero for p > r)”.
Stacks 0ESW, the operation of
c_p(ℰ). On a test schemef : X' ⟶ Xalong whichf^*ℰhas constant rankr— for instance the partX'_rof any test scheme lying overX_r— the classc_p(ℰ)acts by the already defined operationc_p(f^*ℰ) ∩ -of Stacks 0B7H, which is zero whenp > r.
theorem idRule_chernClassOfLocallyFree_of_rank (r p : ℕ) {X' : Scheme.{u}} (f : X' ⟶ X)
[LocallyOfFiniteType f]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback f).obj E) r] (k : ℤ) (α : chowGroup C (f ≫ sX) k) :
(chernClassOfLocallyFree E C sX p).idRule C sX (gysinSystemOfInvertible C) f k α =
if h : p ≤ r then
GenuineChern.chernCap C r (f ≫ sX) ((Scheme.Modules.pullback f).obj E) k
⟨p, Nat.lt_succ_of_le h⟩ α
else 0
Stacks.Chow.SectionZeroScheme.chowGroupRestrict_idRule_chernClassOfLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/LocallyFreeRemark.lean, line 255. The attribute's comment: “explicit form: for every X' → X locally of finite type, c_p(E) preserves the decomposition CH_(X') = ∏_r CH_(X'_r) and acts on the factor X'_r by c_p(E|_{X'_r}) ∩ -”.
Stacks 0ESW, explicitly. For a test scheme
g : X' ⟶ Xlocally of finite type, with the induced decompositionX' = ∐ X'_r,X'_r = g⁻¹(X_r), the classc_p(ℰ)preserves the decompositionCH_*(X') = ∏_r CH_*(X'_r)and acts on the factorCH_*(X'_r)by the already defined operationc_p(ℰ|_{X'_r}) ∩ -of Stacks 0B7H (zero forp > r): restrictingc_p(ℰ) ∩ αtoX'_rgivesc_p(ℰ|_{X'_r}) ∩ (α|_{X'_r}).
theorem chowGroupRestrict_idRule_chernClassOfLocallyFree (r p : ℕ) {X' : Scheme.{u}}
(g : X' ⟶ X) [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ sX) k) :
haveI := isFiniteLocallyFreeOfRank_pullback_preimage_rankLocus E g r
chowGroupRestrict C (g ≫ sX) (((g ⁻¹ᵁ rankLocus E r).ι ≫ g) ≫ sX) (g ⁻¹ᵁ rankLocus E r).ι
(Category.assoc _ _ _).symm ((k : ℤ) - (p : ℤ))
((chernClassOfLocallyFree E C sX p).idRule C sX (gysinSystemOfInvertible C) g k α) =
if h : p ≤ r then
GenuineChern.chernCap C r (((g ⁻¹ᵁ rankLocus E r).ι ≫ g) ≫ sX)
((Scheme.Modules.pullback ((g ⁻¹ᵁ rankLocus E r).ι ≫ g)).obj E) k
⟨p, Nat.lt_succ_of_le h⟩
(chowGroupRestrict C (g ≫ sX) (((g ⁻¹ᵁ rankLocus E r).ι ≫ g) ≫ sX)
(g ⁻¹ᵁ rankLocus E r).ι (Category.assoc _ _ _).symm k α)
else 0
Stacks.Chow.SectionZeroScheme.chernClassOfLocallyFree_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/LocallyFreeRemark.lean, line 288. The attribute's comment: “c_p(E) ∈ A^p(X) as the product of the classes c_p(E|_{X_r}) ∈ A^p(X_r) of 0B7H under A^p(X) = ∏_r A^p(X_r): existence and uniqueness of the class with these restrictions”.
Stacks 0ESW, the Chern classes of a module of non-constant rank.
c_p(ℰ) ∈ A^p(X)is the class whose restriction to every rank locusX_ris the Chern classc_p(ℰ|_{X_r})of Stacks 0B7H (zero whenp > r), and it is the only such class: underA^p(X) = ∏_r A^p(X_r)it is the product of the classesc_p(ℰ|_{X_r}).
theorem chernClassOfLocallyFree_spec (p : ℕ) :
(∀ r : ℕ, haveI := isFiniteLocallyFreeOfRank_pullback_rankLocus E r
chowCohomologyRestriction C (gysinSystemOfInvertible C) sX (rankLocus E r).ι (p : ℤ)
(gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
(chernClassOfLocallyFree E C sX p) =
if h : p ≤ r then
GenuineChern.chernClass C ((rankLocus E r).ι ≫ sX)
((Scheme.Modules.pullback (rankLocus E r).ι).obj E) r ⟨p, Nat.lt_succ_of_le h⟩
else 0) ∧
∀ c : chowCohomologyComponent C (gysinSystemOfInvertible C) sX (p : ℤ),
(∀ r : ℕ, haveI := isFiniteLocallyFreeOfRank_pullback_rankLocus E r
chowCohomologyRestriction C (gysinSystemOfInvertible C) sX (rankLocus E r).ι (p : ℤ)
(gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c =
if h : p ≤ r then
GenuineChern.chernClass C ((rankLocus E r).ι ≫ sX)
((Scheme.Modules.pullback (rankLocus E r).ι).obj E) r ⟨p, Nat.lt_succ_of_le h⟩
else 0) →
c = chernClassOfLocallyFree E C sX p
Stacks.Chow.SectionZeroScheme.totalChernClassCompleted, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/LocallyFreeRemark.lean, line 398. The attribute's comment: “the total Chern class c(E) = c_0(E) + c_1(E) + ... as an element of the completed bivariant cohomology ring A^*(X)^∧ of 0FE0”.
Stacks 0ESW, the total Chern class. The total Chern class
c(ℰ) = c_0(ℰ) + c_1(ℰ) + c_2(ℰ) + … ∈ A^*(X)^∧of a finite locally free module of arbitrary rank: the element of the completed bivariant group of Stacks 0FE0 whose degreeppart is the Chern classc_p(ℰ)forp ≥ 0(and zero forp < 0).
def totalChernClassCompleted :
letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
{c : completedBivariantGroup C (gysinSystemOfInvertible C) sX sX (𝟙 X) (Category.id_comp sX) //
completedBivariantSequenceOfInvertible C sX sX (𝟙 X) (Category.id_comp sX) c =
totalChernComponent C sX E}
Stacks.Chow.SectionZeroScheme.rankClassOfLocallyFree_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/LocallyFreeRemark.lean, line 443. The attribute's comment: “the rank r(E) ∈ A^0(X): the class whose restriction to each X_r is r times the unit of A^0(X_r), existence and uniqueness”.
Stacks 0ESW, the rank as the unique class with the given restrictions.
r(ℰ)restricts tor · 1on each rank locusX_r, and it is the only class ofA^0(X)doing so.
theorem rankClassOfLocallyFree_spec :
(∀ r : ℕ, chowCohomologyRestriction C (gysinSystemOfInvertible C) sX (rankLocus E r).ι 0
(gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) (rankClassOfLocallyFree C sX E) =
(r : ℤ) • bivariantIdentityClassOfInvertible C ((rankLocus E r).ι ≫ sX)) ∧
∀ c : chowCohomologyComponent C (gysinSystemOfInvertible C) sX 0,
(∀ r : ℕ, chowCohomologyRestriction C (gysinSystemOfInvertible C) sX (rankLocus E r).ι 0
(gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c =
(r : ℤ) • bivariantIdentityClassOfInvertible C ((rankLocus E r).ι ≫ sX)) →
c = rankClassOfLocallyFree C sX E
Stacks.Chow.SectionZeroScheme.idRule_rankClassOfLocallyFree_of_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/LocallyFreeRemark.lean, line 469. The attribute's comment: “the rank r(E) ∈ A^0(X) is the bivariant operation sending (α_r) to (r α_r): on every test scheme along which E has constant rank r it acts as multiplication by r”.
Stacks 0ESW, the operation of the rank. On a test scheme
f : X' ⟶ Xalong whichf^*ℰhas constant rankr— for instance the partX'_rof any test scheme lying overX_r— the classr(ℰ)acts as multiplication byr.
theorem idRule_rankClassOfLocallyFree_of_rank (r : ℕ) {X' : Scheme.{u}} (f : X' ⟶ X)
[LocallyOfFiniteType f]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback f).obj E) r] (k : ℤ) (α : chowGroup C (f ≫ sX) k) :
(rankClassOfLocallyFree C sX E).idRule C sX (gysinSystemOfInvertible C) f k α =
(r : ℤ) • identityCapRule C sX f k α
Stacks.Chow.SectionZeroScheme.chowGroupRestrict_idRule_rankClassOfLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/LocallyFreeRemark.lean, line 493. The attribute's comment: “explicit form of the rank: r(E) is the bivariant operation sending (α_r) ∈ ∏_r CH_*(X'_r) to (r α_r), for every X' → X locally of finite type”.
Stacks 0ESW, the rank explicitly. For a test scheme
g : X' ⟶ Xlocally of finite type, with the induced decompositionX' = ∐ X'_r, the classr(ℰ)sends(α_r) ∈ ∏_r CH_*(X'_r)to(r α_r): restrictingr(ℰ) ∩ αtoX'_rgivesr · (α|_{X'_r}).
theorem chowGroupRestrict_idRule_rankClassOfLocallyFree (r : ℕ) {X' : Scheme.{u}}
(g : X' ⟶ X) [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ sX) k) :
chowGroupRestrict C (g ≫ sX) (((g ⁻¹ᵁ rankLocus E r).ι ≫ g) ≫ sX) (g ⁻¹ᵁ rankLocus E r).ι
(Category.assoc _ _ _).symm (k - 0)
((rankClassOfLocallyFree C sX E).idRule C sX (gysinSystemOfInvertible C) g k α) ≍
(r : ℤ) • chowGroupRestrict C (g ≫ sX) (((g ⁻¹ᵁ rankLocus E r).ι ≫ g) ≫ sX)
(g ⁻¹ᵁ rankLocus E r).ι (Category.assoc _ _ _).symm k α
Stacks.Chow.SectionZeroScheme.chernClassOfLocallyFree_mem_center, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/LocallyFreeRemark.lean, line 568. The attribute's comment: “c_p(E) is in the center of A^*(X), for E of non-constant rank”.
Stacks 0ESW, centrality of the Chern classes. For a finite locally free module
ℰof arbitrary rank,c_p(ℰ) ∈ A^p(X)lies in the center of the Chow cohomology ringA^*(X)of Stacks 0B7E: on each rank locus it restricts to a Chern class of Stacks 0B7H, which is central by Stacks 02UA, or to zero.
theorem chernClassOfLocallyFree_mem_center (p : ℕ) :
DirectSum.of (fun q : ℤ ↦ chowCohomologyComponent C (gysinSystemOfInvertible C) sX q) (p : ℤ)
(chernClassOfLocallyFree E C sX p) ∈
Subring.center (chowCohomology C (gysinSystemOfInvertible C) sX)
Stacks.Chow.SectionZeroScheme.rankClassOfLocallyFree_mem_center, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/LocallyFreeRemark.lean, line 592. The attribute's comment: “r(E) is in the center of A^*(X)”.
Stacks 0ESW, centrality of the rank.
r(ℰ) ∈ A^0(X)lies in the center ofA^*(X): on each rank locusX_rit restricts tor · 1.
theorem rankClassOfLocallyFree_mem_center :
DirectSum.of (fun q : ℤ ↦ chowCohomologyComponent C (gysinSystemOfInvertible C) sX q) 0
(rankClassOfLocallyFree C sX E) ∈
Subring.center (chowCohomology C (gysinSystemOfInvertible C) sX)
Stacks.Chow.rankBivariantClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/RankClass.lean, line 215. The attribute's comment: “rank_bivariant_class; the flat transport axiom of Stacks 0B76 is proved here, and only the Gysin transport axiom is carried, as for the library's own first Chern class at Tag 0FDW”.
Stacks 0ESW. The rank
r(E) ∈ A^0(X)of a finite locally free module whose rank need not be constant: the bivariant class which preserves the product decomposition of the Chow groups along the rank loci and acts on the rank-rfactor by multiplication byr.
def rankBivariantClass : chowCohomologyComponent C G sX 0
Stacks.Chow.rankLocusRestriction_rankBivariantClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/RankClass.lean, line 224. The attribute's comment: “rank_bivariant_class; the flat transport axiom of Stacks 0B76 is proved here, and only the Gysin transport axiom is carried, as for the library's own first Chern class at Tag 0FDW”.
Stacks 0ESW. The component of
r(E)on the rank-rlocus isrtimes the unit.
theorem rankLocusRestriction_rankBivariantClass (r : ℕ) :
rankLocusRestriction C G sX E hgysO 0
(rankBivariantClass C G sX E hgysO hgysR hgysC hgysin) r =
(r : ℤ) • chowCohomologyOne C ((rankLocus E r).ι ≫ sX) G
(transportFlatNaturality_rankLocus C sX E r) (hgysin r)
Stacks.Chow.rankBivariantClass_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/RankClass.lean, line 236. The attribute's comment: “rank_bivariant_class; the flat transport axiom of Stacks 0B76 is proved here, and only the Gysin transport axiom is carried, as for the library's own first Chern class at Tag 0FDW”.
Stacks 0ESW.
r(E)sends(α_r)to(r α_r): on a test scheme over the rank-rlocus, capping withr(E)is multiplication byr.
theorem rankBivariantClass_cap (r : ℕ) {T : Scheme.{u}}
(g : T ⟶ (rankLocus E r : Scheme.{u})) [LocallyOfFiniteType g] (k : ℤ)
(α : chowGroup C (g ≫ ((rankLocus E r).ι ≫ sX)) k) :
chowPushforwardOfIso C
(pullback.fst (𝟙 (rankLocus E r : Scheme.{u})) g ≫ ((rankLocus E r).ι ≫ sX))
(g ≫ ((rankLocus E r).ι ≫ sX)) (identityBaseChangeIso g).hom
(identityBaseChangeIso_hom_comp_base C ((rankLocus E r).ι ≫ sX) g) (k - 0)
((rankLocusRestriction C G sX E hgysO 0
(rankBivariantClass C G sX E hgysO hgysR hgysC hgysin) r).cap g k α) =
(r : ℤ) • chowGroupDegreeEquiv C (g ≫ ((rankLocus E r).ι ≫ sX))
(by omega : k = k - 0) α
Stacks.Chow.eq_rankBivariantClass_of_rankLocusRestriction_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/RankClass.lean, line 256. The attribute's comment: “rank_bivariant_class; the flat transport axiom of Stacks 0B76 is proved here, and only the Gysin transport axiom is carried, as for the library's own first Chern class at Tag 0FDW”.
Stacks 0ESW.
r(E)is the only degree-zero class with those components.
theorem eq_rankBivariantClass_of_rankLocusRestriction_eq
{c : chowCohomologyComponent C G sX 0}
(h : ∀ r : ℕ, rankLocusRestriction C G sX E hgysO 0 c r =
(r : ℤ) • chowCohomologyOne C ((rankLocus E r).ι ≫ sX) G
(transportFlatNaturality_rankLocus C sX E r) (hgysin r)) :
c = rankBivariantClass C G sX E hgysO hgysR hgysC hgysin
AlgebraicGeometry.Scheme.Modules.rankDecomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/RankDecomposition.lean, line 114. The attribute's comment: “the decomposition X = ∐ X_r of a scheme by the rank of a finite locally free module: the rank is locally constant, the loci are open and closed, pairwise disjoint and covering, and the module is free of rank r near each point of X_r. The Chern classes c_p(E) ∈ A^p(X) of a module of non-constant rank, the total Chern class in the completed bivariant group, the rank class r(E) ∈ A^0(X) and the centrality of c_p(E) and r(E) in A^*(X) are not covered”.
The rank of a finite locally free module
Eon a schemeXis locally constant, the lociX_rwhere the rank israre open and closed, pairwise disjoint and coverX, andEis free of rankron a neighbourhood of every point ofX_r.
theorem rankDecomposition :
IsLocallyConstant ⇑(finiteLocallyFreeRank E) ∧
(∀ r : ℕ, IsClopen (rankStratum E r : Set X)) ∧
(∀ r s : ℕ, r ≠ s → Disjoint (rankStratum E r) (rankStratum E s)) ∧
(⨆ r : ℕ, rankStratum E r) = ⊤ ∧
∀ (r : ℕ) (x : X), x ∈ rankStratum E r →
∃ (V : X.Opens) (_ : x ∈ V) (_ : V ≤ rankStratum E r) (I : Type u),
Nonempty (I ≃ Fin r) ∧
Nonempty (SheafOfModules.free.{u} I ≅ (toRingSheafModule E).over V)
Tag 0FA4, a remark
Tag 0FA4 in the Stacks Project.
Stacks.Chow.topChernClassCompleted, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/TopChernClass.lean, line 351. The attribute's comment: “general case: c_top(E) = ∏ c_r(E|_{X_r}) ∈ ∏ A^r(X_r) ⊂ A^*(X)^∧”.
Stacks 0FA4, general case. The top Chern class
c_top(ℰ) = ∏_r c_r(ℰ|_{X_r}) ∈ ∏_r A^r(X_r) ⊂ A^*(X)^∧of a finite locally free moduleℰonX, for the decompositionX = ∐ X_rby the rank ofℰ: the element of the completed bivariant group of Stacks 0FE0 whose image(c_p)_p ∈ ∏_p A^p(X)has, underA^p(X) = ∏_r A^p(X_r)of Stacks 0FDZ, the componentc_r(ℰ|_{X_r})inA^r(X_r)and zero inA^p(X_r)forp ≠ r.
def topChernClassCompleted :
letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
{c : completedBivariantGroup C (gysinSystemOfInvertible C) sX sX (𝟙 X) (Category.id_comp sX) //
(∀ r : ℕ, rankLocusRestriction C (gysinSystemOfInvertible C) sX E
(gysinSystemOfInvertible_isNaturalUnderOpenImmersion C) (r : ℤ)
(completedBivariantSequenceOfInvertible C sX sX (𝟙 X) (Category.id_comp sX) c r) r =
rankLocusTopChernClass C sX E r) ∧
∀ (p : ℤ) (r : ℕ), (r : ℤ) ≠ p →
rankLocusRestriction C (gysinSystemOfInvertible C) sX E
(gysinSystemOfInvertible_isNaturalUnderOpenImmersion C) p
(completedBivariantSequenceOfInvertible C sX sX (𝟙 X) (Category.id_comp sX) c p) r =
0}
Stacks.Chow.topChernClassOfFinite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/TopChernClass.lean, line 407. The attribute's comment: “finite case: c_top(E) = Σ_r c_r(E|_{X_r}) ∈ A^(X) = ⊕ A^(X_r)”.
Stacks 0FA4, finite case. If only finitely many of the rank loci
X_rare nonempty, the top Chern classc_top(ℰ) = Σ_r c_r(ℰ|_{X_r}) ∈ A^*(X) = ⊕ A^*(X_r): the element of the graded groupA^*(X) = ⊕_p A^p(X)that is the sum, over the ranksrthat occur, of a class of degreer, and whose degreeppart has, underA^p(X) = ∏_r A^p(X_r)of Stacks 0FDZ, the componentc_r(ℰ|_{X_r})inA^r(X_r)and zero inA^p(X_r)forp ≠ r.
def topChernClassOfFinite (hfin : {r : ℕ | (rankLocus E r : Set X).Nonempty}.Finite) :
{c : nonhomogeneousBivariantGroup C (gysinSystemOfInvertible C) sX sX (𝟙 X)
(Category.id_comp sX) //
c = ∑ r ∈ hfin.toFinset, DirectSum.of _ (r : ℤ) (c r) ∧
(∀ r : ℕ, rankLocusRestriction C (gysinSystemOfInvertible C) sX E
(gysinSystemOfInvertible_isNaturalUnderOpenImmersion C) (r : ℤ) (c r) r =
rankLocusTopChernClass C sX E r) ∧
∀ (p : ℤ) (r : ℕ), (r : ℤ) ≠ p →
rankLocusRestriction C (gysinSystemOfInvertible C) sX E
(gysinSystemOfInvertible_isNaturalUnderOpenImmersion C) p (c p) r = 0}
Stacks.Chow.topChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClass.lean, line 209. The attribute's comment: “completed top Chern class”.
Stacks 0FA4. The top Chern class
c_top(E) = Σ_r c_r(E|_{X_r})of a finite locally free moduleEonX, as an element of the completed bivariant groupA^*(X)^∧: on a connected componentX_iofXthe rank ofEis a constantr, and there the class is ther-th Chern classc iofE|_{X_i}, placed in degreer.
def topChernClass : completedBivariantGroup C G sX sX (𝟙 X) (Category.id_comp sX)
Stacks.Chow.topChernClass_rankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClass.lean, line 216. The attribute's comment: “rank-locus Chern component”.
Stacks 0FA4. On the locus where
Ehas rankrthe top Chern class is ther-th Chern class, in degreer: a connected componentX_ilies in the locus of the rankrofEon it, and the degree-rpart ofc_top(E)there isc_r(E|_{X_i}).
theorem topChernClass_rankStratum (i : ConnectedComponents X) :
X.connectedComponentOpens i ≤
Scheme.Modules.rankStratum E (Scheme.Modules.rankOnConnectedComponent E i) ∧
topChernClass C G sX E c i (Scheme.Modules.rankOnConnectedComponent E i : ℤ) = c i
Stacks.Chow.topChernClass_of_ne_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClass.lean, line 227. The attribute's comment: “off-rank vanishing”.
Stacks 0FA4. The top Chern class has no component in a degree other than the rank: on a connected component on which
Ehas rankr, the degree-ppart ofc_top(E)vanishes for everyp ≠ r.
theorem topChernClass_of_ne_rank (i : ConnectedComponents X) (p : ℤ)
(h : p ≠ (Scheme.Modules.rankOnConnectedComponent E i : ℤ)) :
topChernClass C G sX E c i p = 0
Stacks.Chow.finite_degrees_topChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClass.lean, line 236. The attribute's comment: “finite-rank-locus case”.
Stacks 0FA4. If only finitely many of the loci
X_rare nonempty, then only finitely many degrees occur in the top Chern class, so it lies in the ordinary graded groupA^*(X)inside its completion.
theorem finite_degrees_topChernClass
(hfin : {r : ℕ | (Scheme.Modules.rankStratum E r : Set X).Nonempty}.Finite) :
{p : ℤ | ∃ i : ConnectedComponents X, topChernClass C G sX E c i p ≠ 0}.Finite
Stacks.Chow.topChernClassFinite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClass.lean, line 271. The attribute's comment: “ordinary finite top Chern class”.
Stacks 0FA4. The top Chern class
c_top(E) = Σ_r c_r(E|_{X_r})as an ordinary nonhomogeneous bivariant class onX, when only finitely many of the lociX_rare nonempty: the sum, over the ranksrthat occur, of the degree-rpart of the top Chern class.
def topChernClassFinite
(hfin : {r : ℕ | (Scheme.Modules.rankStratum E r : Set X).Nonempty}.Finite) :
nonhomogeneousBivariantGroup C G sX sX (𝟙 X) (Category.id_comp sX)
Stacks.Chow.topChernClassFinite_component, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClass.lean, line 314. The attribute's comment: “finite-class canonical image”.
Stacks 0FA4. The finite sum
Σ_r c_r(E|_{X_r})has the completed top Chern class as its image under the identification of Stacks 0FDZ: in every degree and on every connected component, its restriction is the corresponding part ofc_top(E).
theorem topChernClassFinite_component
(hfin : {r : ℕ | (Scheme.Modules.rankStratum E r : Set X).Nonempty}.Finite) (p : ℤ)
(i : ConnectedComponents X) :
connectedComponentBivariantEquiv C G sX p hgysO hgysR hgysC
(topChernClassFinite C G sX E c hgysO hgysR hgysC hfin p) i =
topChernClass C G sX E c i p
Stacks.Chow.topChernClassFinite_rankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClass.lean, line 337. The attribute's comment: “finite-sum rank component”.
Stacks 0FA4. On the locus where
Ehas rankr, the component of the finite sumΣ_r c_r(E|_{X_r})in degreeris ther-th Chern class: a connected componentX_ilies in the locus of the rankrofEon it, and the degree-rcomponent of the sum there isc_r(E|_{X_i}).
theorem topChernClassFinite_rankStratum
(hfin : {r : ℕ | (Scheme.Modules.rankStratum E r : Set X).Nonempty}.Finite)
(i : ConnectedComponents X) :
X.connectedComponentOpens i ≤
Scheme.Modules.rankStratum E (Scheme.Modules.rankOnConnectedComponent E i) ∧
connectedComponentBivariantEquiv C G sX
(Scheme.Modules.rankOnConnectedComponent E i : ℤ) hgysO hgysR hgysC
(topChernClassFinite C G sX E c hgysO hgysR hgysC hfin
(Scheme.Modules.rankOnConnectedComponent E i : ℤ)) i = c i
Stacks.Chow.topChernClassFinite_of_ne_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClass.lean, line 355. The attribute's comment: “finite-sum off-rank component”.
Stacks 0FA4. The finite sum
Σ_r c_r(E|_{X_r})has no component in a degree other than the rank: on a connected component on whichEhas rankr, its degree-pcomponent vanishes for everyp ≠ r.
theorem topChernClassFinite_of_ne_rank
(hfin : {r : ℕ | (Scheme.Modules.rankStratum E r : Set X).Nonempty}.Finite)
(i : ConnectedComponents X) (p : ℤ)
(h : p ≠ (Scheme.Modules.rankOnConnectedComponent E i : ℤ)) :
connectedComponentBivariantEquiv C G sX p hgysO hgysR hgysC
(topChernClassFinite C G sX E c hgysO hgysR hgysC hfin p) i = 0
Stacks.Chow.topChernTotalClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClassOfInvertible.lean, line 136. The attribute's comment: “top Chern class in the product of the Chow cohomology groups”.
The top Chern class
c_top(E) = Σ_r c_r(E|_{X_r})of a finite locally free moduleEonX, as an element of∏_{p ≥ 0} A^p(X): its degree-pcomponent is the class equal, on the locusX_pwhereEhas rankp, to thep-th Chern class of Stacks 0ESW, and to zero on every other rank locus. It is assembled along the rank decomposition by Stacks 0FDZ.
def topChernTotalClass : TotalChowClass C sX
Stacks.Chow.topChernClassOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClassOfInvertible.lean, line 289. The attribute's comment: “completed top Chern class”.
The top Chern class
c_top(E) = Σ_r c_r(E|_{X_r})of a finite locally free moduleEonX, as an element of the completed bivariant groupA^*(X)^∧: on a connected componentX_iofXthe rank ofEis a constantr, and there the class is the restriction toX_iof the degree-rcomponent ofc_top(E)— that is, of ther-th Chern class of Stacks 0ESW, byStacks.Chow.topChernClassOfInvertible_rankStratum— placed in degreer.
def topChernClassOfInvertible :
completedBivariantGroup C (gysinSystemOfInvertible C) sX sX (𝟙 X) (Category.id_comp sX)
Stacks.Chow.topChernClassOfInvertible_rankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClassOfInvertible.lean, line 301. The attribute's comment: “rank-locus Chern component”.
On the locus where
Ehas rankrthe top Chern class is ther-th Chern class, in degreer: a connected componentX_ilies in the locus of the rankrofEon it, and the degree-rpart ofc_top(E)there is the restriction toX_iof the Chern classc_r(E)of Stacks 0ESW, that isc_r(E|_{X_i}).
theorem topChernClassOfInvertible_rankStratum (i : _root_.ConnectedComponents X) :
X.connectedComponentOpens i ≤
Scheme.Modules.rankStratum E (Scheme.Modules.rankOnConnectedComponent E i) ∧
topChernClassOfInvertible C sX E i (Scheme.Modules.rankOnConnectedComponent E i : ℤ) =
bivariantConnectedComponentRestriction C (gysinSystemOfInvertible C) sX sX (𝟙 X)
(Category.id_comp sX) _ (gysinSystemOfInvertible_isNaturalUnderOpenImmersion C)
(totalChernOfFiniteLocallyFree C sX E (Scheme.Modules.rankOnConnectedComponent E i))
i
Stacks.Chow.topChernClassOfInvertible_of_ne_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClassOfInvertible.lean, line 316. The attribute's comment: “off-rank vanishing”.
The top Chern class has no component in a degree other than the rank: on a connected component on which
Ehas rankr, the degree-ppart ofc_top(E)vanishes for everyp ≠ r.
theorem topChernClassOfInvertible_of_ne_rank (i : _root_.ConnectedComponents X) (p : ℤ)
(h : p ≠ (Scheme.Modules.rankOnConnectedComponent E i : ℤ)) :
topChernClassOfInvertible C sX E i p = 0
Stacks.Chow.finite_degrees_topChernClassOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClassOfInvertible.lean, line 324. The attribute's comment: “finite-rank-locus case”.
If only finitely many of the loci
X_rare nonempty, then only finitely many degrees occur in the top Chern class, so it lies in the ordinary graded groupA^*(X)inside its completion.
theorem finite_degrees_topChernClassOfInvertible
(hfin : {r : ℕ | (Scheme.Modules.rankStratum E r : Set X).Nonempty}.Finite) :
{p : ℤ | ∃ i : _root_.ConnectedComponents X,
topChernClassOfInvertible C sX E i p ≠ 0}.Finite
Stacks.Chow.topChernClassFiniteOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClassOfInvertible.lean, line 389. The attribute's comment: “ordinary finite top Chern class”.
The top Chern class
c_top(E) = Σ_r c_r(E|_{X_r})as an ordinary nonhomogeneous bivariant class onX, when only finitely many of the lociX_rare nonempty: the sum, over the ranksrthat occur, of the degree-rpart of the top Chern class.
def topChernClassFiniteOfInvertible
(hfin : {r : ℕ | (Scheme.Modules.rankStratum E r : Set X).Nonempty}.Finite) :
nonhomogeneousBivariantGroup C (gysinSystemOfInvertible C) sX sX (𝟙 X)
(Category.id_comp sX)
Stacks.Chow.topChernClassFiniteOfInvertible_component, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClassOfInvertible.lean, line 422. The attribute's comment: “finite-class canonical image”.
The finite sum
Σ_r c_r(E|_{X_r})has the completed top Chern class as its image under the identification of Stacks 0FDZ: in every degree and on every connected component, its restriction is the corresponding part ofc_top(E).
theorem topChernClassFiniteOfInvertible_component
(hfin : {r : ℕ | (Scheme.Modules.rankStratum E r : Set X).Nonempty}.Finite) (p : ℤ)
(i : _root_.ConnectedComponents X) :
bivariantConnectedComponentRestriction C (gysinSystemOfInvertible C) sX sX (𝟙 X)
(Category.id_comp sX) p (gysinSystemOfInvertible_isNaturalUnderOpenImmersion C)
(topChernClassFiniteOfInvertible C sX E hfin p) i =
topChernClassOfInvertible C sX E i p
Stacks.Chow.topChernClassFiniteOfInvertible_rankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClassOfInvertible.lean, line 444. The attribute's comment: “finite-sum rank component”.
On the locus where
Ehas rankr, the component of the finite sumΣ_r c_r(E|_{X_r})in degreeris ther-th Chern class: a connected componentX_ilies in the locus of the rankrofEon it, and the degree-rcomponent of the sum there is the restriction ofc_r(E), that isc_r(E|_{X_i}).
theorem topChernClassFiniteOfInvertible_rankStratum
(hfin : {r : ℕ | (Scheme.Modules.rankStratum E r : Set X).Nonempty}.Finite)
(i : _root_.ConnectedComponents X) :
X.connectedComponentOpens i ≤
Scheme.Modules.rankStratum E (Scheme.Modules.rankOnConnectedComponent E i) ∧
bivariantConnectedComponentRestriction C (gysinSystemOfInvertible C) sX sX (𝟙 X)
(Category.id_comp sX) _ (gysinSystemOfInvertible_isNaturalUnderOpenImmersion C)
(topChernClassFiniteOfInvertible C sX E hfin
(Scheme.Modules.rankOnConnectedComponent E i : ℤ)) i =
bivariantConnectedComponentRestriction C (gysinSystemOfInvertible C) sX sX (𝟙 X)
(Category.id_comp sX) _ (gysinSystemOfInvertible_isNaturalUnderOpenImmersion C)
(totalChernOfFiniteLocallyFree C sX E (Scheme.Modules.rankOnConnectedComponent E i))
i
Stacks.Chow.topChernClassFiniteOfInvertible_of_ne_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TopChernClassOfInvertible.lean, line 465. The attribute's comment: “finite-sum off-rank component”.
The finite sum
Σ_r c_r(E|_{X_r})has no component in a degree other than the rank: on a connected component on whichEhas rankr, its degree-pcomponent vanishes for everyp ≠ r.
theorem topChernClassFiniteOfInvertible_of_ne_rank
(hfin : {r : ℕ | (Scheme.Modules.rankStratum E r : Set X).Nonempty}.Finite)
(i : _root_.ConnectedComponents X) (p : ℤ)
(h : p ≠ (Scheme.Modules.rankOnConnectedComponent E i : ℤ)) :
bivariantConnectedComponentRestriction C (gysinSystemOfInvertible C) sX sX (𝟙 X)
(Category.id_comp sX) p (gysinSystemOfInvertible_isNaturalUnderOpenImmersion C)
(topChernClassFiniteOfInvertible C sX E hfin p) i = 0
Sources
Section42.39 Polynomial relations among Chern classes#
Section 42.39 of the Stacks Project, Tag 02UB. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02UD, a lemma
Tag 02UD in the Stacks Project.
Stacks.Chow.TotalChowClass.totalChern_sheafTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/TwistFormula.lean, line 513. The attribute's comment: “Equation (02UE) in A^*(X), as the single identity c(E tensor L) = T_{r,c_1(L)}(c(E)) of total Chow cohomology classes, under the source's hypotheses and no others. It is Equation (02UE) in each degree i by Stacks.Chow.TotalChowClass.totalChern_sheafTensor_degree”.
Stacks 02UD for total classes: for
ℰfinite locally free of rankrandℒinvertible,c(ℰ ⊗ ℒ) = T_{r,c₁(ℒ)}(c(ℰ)), that is,c_i(ℰ ⊗ ℒ) = ∑_{j=0}^{i} binom(r - i + j, j) c_{i-j}(ℰ) c₁(ℒ)^j.This is the identity of Stacks 02UD in the Chow cohomology of
Y. It holds in every degreeiseparately, asStacks.Chow.TotalChowClass.totalChern_sheafTensor_degreestates.
theorem totalChern_sheafTensor (E : Y.Modules) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r] :
-- `totalChern` reads the rank of a `Y.Modules`, so it asks for the twist's rank at
-- `Y.ringCatSheaf`, while `GenuineChern.isFiniteLocallyFreeOfRank_sheafTensor` states it at
-- the native `Tensor.ringSheaf Y.sheaf`. The two are the same sheaf of rings, but only
-- after unfolding the `Tensor.ringSheaf` def, which instance search does not do, so the
-- twist's rank is handed over by name at the spelling the statement needs.
letI : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
(R := Y.ringCatSheaf)
(((Stacks.SheafOfModules.Tensor.sheafTensor Y.sheaf).obj E).obj L) r :=
GenuineChern.isFiniteLocallyFreeOfRank_sheafTensor E r L
totalChern C sY (((Stacks.SheafOfModules.Tensor.sheafTensor Y.sheaf).obj E).obj L) r =
twist (r : ℤ) (firstChernTotal C sY L) (totalChern C sY E r)
Stacks.Chow.chernCapFamily_tensorObj_eq_binomialTransform, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassTwist.lean, line 487. The attribute's comment: “the two relations of Stacks 02U6 are hypotheses, hrelEL being the one already transported along the comparison of projective bundles of Stacks 02NC, and so is their uniqueness (the injectivity half of Stacks 02TX); the conclusion is the identity capped with an arbitrary cycle, the source's identity in the ring A^(X) being unstateable here (there is no multiplication on bivariant classes) and the source itself reducing it to this form by Stacks 02UC. Carried besides: hcomm (commutativity of the two first Chern class cap operators on the bundle, Stacks 02UA), hpull (flat pullback carries c_1(L) to c_1(pi^L), Stacks 02SS and 02RD), h0 (the zeroth cap products of E and of E tensor L both being the class of alpha, Stacks 02U5 (1) at j = 0), the Stacks 02U0 data chernE and chernEL, the rank of E tensor L, and Stacks 02TI for c_1(L) as hfac”.
Stacks 02UD. Let
ℰbe a finite locally free𝒪_X-module of rankr, letℒbe invertible and letαbe ann-cycle onX. Then for everym ≤ r
c_m(ℰ ⊗ ℒ) ∩ α = ∑_{j=0}^{m} binom(r - m + j, j) c₁(ℒ)^j ∩ (c_{m-j}(ℰ) ∩ α)in
A_{n-m}(X), the right-hand side being the binomial transform of the Chern class cap products ofℰalongc₁(ℒ) ∩ -.The relation of Stacks 02U6 on the projective bundle of
ℰis carried forℰand, transported along the comparison𝐏(ℰ) ≅ 𝐏(ℰ ⊗ ℒ)of Stacks 02NC, forℰ ⊗ ℒ; so is its uniqueness, which is the injectivity half of Stacks 02TX. See the module documentation.
theorem chernCapFamily_tensorObj_eq_binomialTransform (twist twistL : ChernCapOperator C sP)
(n : ℤ) (E L : X.Modules)
[AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
(hrankE : PullbackPreservesRank E r)
(hrankEL : PullbackPreservesRank (Scheme.Modules.tensorObjRingedSpace X E L) r)
(chernE chernEL : ChernClassCycleRule C r) (hfac : InvertibleChernCapDescends C sX L)
(α : CycleGroup C sX n)
(hcomm : ∀ i,
(ChernCapOperator.towerStep C sP twist (bundleRelationDegree r n) (i + 1)).comp
(ChernCapOperator.towerStep C sP twistL (bundleRelationDegree r n) i) =
(ChernCapOperator.towerStep C sP twistL (bundleRelationDegree r n) (i + 1)).comp
(ChernCapOperator.towerStep C sP twist (bundleRelationDegree r n) i))
(hpull : ∀ i,
(projectiveBundleTowerPullback C sX sP π hsP r hπ hfacπ n (i + 1)).comp
(firstChernCapStep C sX n L hfac i) =
(ChernCapOperator.towerStep C sP twistL (bundleRelationDegree r n) i).comp
(projectiveBundleTowerPullback C sX sP π hsP r hπ hfacπ n i))
(h0 : chernCapFamily C sX n (Scheme.Modules.tensorObjRingedSpace X E L) r hrankEL chernEL α 0 =
chernCapFamily C sX n E r hrankE chernE α 0)
(hrelE : alternatingTowerSum
(ChernCapOperator.towerStep C sP twist (bundleRelationDegree r n)) r
(towerPullback (projectiveBundleTowerPullback C sX sP π hsP r hπ hfacπ n)
(chernCapFamily C sX n E r hrankE chernE α)) = 0)
(hrelEL : alternatingTowerSum
(fun j => ChernCapOperator.towerStep C sP twist (bundleRelationDegree r n) j +
ChernCapOperator.towerStep C sP twistL (bundleRelationDegree r n) j) r
(towerPullback (projectiveBundleTowerPullback C sX sP π hsP r hπ hfacπ n)
(chernCapFamily C sX n (Scheme.Modules.tensorObjRingedSpace X E L) r hrankEL
chernEL α)) = 0)
(huniq : ∀ d : (∀ j : ℕ, chowGroup C sX (n - (j : ℤ))), d 0 = 0 →
alternatingTowerSum
(fun j => ChernCapOperator.towerStep C sP twist (bundleRelationDegree r n) j +
ChernCapOperator.towerStep C sP twistL (bundleRelationDegree r n) j) r
(towerPullback (projectiveBundleTowerPullback C sX sP π hsP r hπ hfacπ n) d) = 0 →
∀ m ≤ r, d m = 0)
{m : ℕ} (hm : m ≤ r) :
chernCapFamily C sX n (Scheme.Modules.tensorObjRingedSpace X E L) r hrankEL chernEL α m =
binomialTransform (firstChernCapStep C sX n L hfac) r
(chernCapFamily C sX n E r hrankE chernE α) m
Sources
Section42.40 Additivity of Chern classes#
Section 42.40 of the Stacks Project, Tag 02UF. 4 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02UG, a lemma
Tag 02UG in the Stacks Project.
Stacks.Chow.chernClass_eq_of_shortExact_of_iso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernWhitney/InvertibleSubsheaf.lean, line 162. The attribute's comment: “c_r(E) = 0 and c_j(E) = c_j(F) for j = 0, ..., r - 1 in the Chow cohomology ring A^*(X) of Stacks 0B7E, for a short exact sequence 0 -> O_X -> E -> F -> 0 on X locally of finite type over the base with E, F finite locally free of ranks r, r - 1; c_j is the bivariant Chern class of Stacks 0B7H in A^j(X)”.
Stacks 02UG. Let
Xbe locally of finite type over the base and let0 ⟶ 𝒪_X ⟶ ℰ ⟶ ℱ ⟶ 0be a short exact sequence of𝒪_X-modules withℰ,ℱfinite locally free of ranksr,r - 1. Then
c_r(ℰ) = 0,c_j(ℰ) = c_j(ℱ),j = 0, …, r - 1,in the Chow cohomology ring
A^*(X) = ⨁_p A^p(X)of Stacks 0B7E, thec_jbeing the bivariant Chern classes of Stacks 0B7H placed in their degree.
theorem chernClass_eq_of_shortExact_of_iso_unit (S : ShortComplex Y.Modules) (hS : S.ShortExact)
(e : S.X₁ ≅ SheafOfModules.unit Y.ringCatSheaf) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₂ r]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₃ (r - 1)] :
DirectSum.of (fun p ↦ chowCohomologyComponent C (gysinSystemOfInvertible C) sY p) (r : ℤ)
(GenuineChern.chernClass C sY S.X₂ r (Fin.last r)) = 0 ∧
∀ j : Fin r,
DirectSum.of (fun p ↦ chowCohomologyComponent C (gysinSystemOfInvertible C) sY p)
(j : ℤ) (GenuineChern.chernClass C sY S.X₂ r j.castSucc) =
DirectSum.of (fun p ↦ chowCohomologyComponent C (gysinSystemOfInvertible C) sY p)
(j : ℤ) (GenuineChern.chernClass C sY S.X₃ (r - 1) ⟨j, by omega⟩)
Stacks.Chow.chernCap_top_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernWhitney/TrivialSubsheaf.lean, line 338. The attribute's comment: “the vanishing c_{r+2}(E) cap alpha = 0, stated degreewise on the cap products of 02U5 rather than in A^*(X), which has no multiplication here; ranks r + 2 and r + 1, so the source's r = 1 is excluded; bundles, twists, iota, 02TX injectivity and 02TR+02SU are inputs”.
Stacks 02UG, the vanishing of the top Chern class, on cap products. Let
0 ⟶ O_X ⟶ ℰ ⟶ ℱ ⟶ 0be a short exact sequence of finite locally free modules on
Xwithℰof rankr + 2andℱof rankr + 1. Then for everykand every classα ∈ A_k(X),
c_{r+2}(ℰ) ∩ α = 0inA_{k-r-2}(X).The cap products are the members of families satisfying the characterization of Stacks 02U6, which is how they exist in this repository at all:
hcandheare those families forℰand forℱ. The proof is the proof of the source: the family ofℱextended by zero satisfies the relation over the bundle ofℰ, by Stacks 02TR and 02SU, and the uniqueness of Stacks 02U6 identifies it with the family ofℰ, whose top member is therefore zero.Stacks 02S1 for the two projections is supplied from
Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_generaland is not an argument. The projective bundles themselves, their twistsO_P(1)andO_Q(1), the closed immersionι, the injectivity half of Stacks 02TX overPand the summandwise formhcompatof Stacks 02TR and 02SU are arguments, because Stacks 02TX and the representability of the twists (Stacks 01O4) are not in this repository; see the module documentation.
theorem chernCap_top_eq_zero
(hinj : ProjectiveBundleRelationInjective C sX sP π hsP (r + 2) hπ
(flatPullbackFactorsThroughRationalEquivalence_general C sP sX π hsP (r + 2 - 1) hπ)
twistP)
(hcompat : ChernTermsCompatibleWithTrivialSubbundle C sX sP sQ π hsP ϖ hsQ r hπ hϖ
(flatPullbackFactorsThroughRationalEquivalence_general C sP sX π hsP (r + 2 - 1) hπ)
(flatPullbackFactorsThroughRationalEquivalence_general C sQ sX ϖ hsQ (r + 1 - 1) hϖ)
twistP twistQ ι hι)
(_S : ShortComplex X.Modules)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} _S.X₂ (r + 2)]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} _S.X₃ (r + 1)]
(_hunit : _S.X₁ ≅ (SheafOfModules.unit X.ringCatSheaf : X.Modules))
(_hexact : _S.ShortExact) (k : ℤ) (α : chowGroup C sX k)
(c : ∀ j : Fin (r + 3), chowGroup C sX (k - (j : ℤ)))
(e : ∀ j : Fin (r + 2), chowGroup C sX (k - (j : ℤ)))
(hc : IsChernCapFamily C sX sP π hsP (r + 2) hπ
(flatPullbackFactorsThroughRationalEquivalence_general C sP sX π hsP (r + 2 - 1) hπ)
twistP k α c)
(he : IsChernCapFamily C sX sQ ϖ hsQ (r + 1) hϖ
(flatPullbackFactorsThroughRationalEquivalence_general C sQ sX ϖ hsQ (r + 1 - 1) hϖ)
twistQ k α e) :
c (Fin.last (r + 2)) = 0
Stacks.Chow.chernCap_castSucc_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernWhitney/TrivialSubsheaf.lean, line 383. The attribute's comment: “the agreement c_j(E) cap alpha = c_j(F) cap alpha for j <= r + 1, stated degreewise on the cap products of 02U5 rather than in A^*(X), which has no multiplication here; ranks r + 2 and r + 1; bundles, twists, iota, 02TX and 02TR+02SU are inputs”.
Stacks 02UG, the agreement of the lower Chern classes, on cap products. Let
0 ⟶ O_X ⟶ ℰ ⟶ ℱ ⟶ 0be a short exact sequence of finite locally free modules on
Xwithℰof rankr + 2andℱof rankr + 1. Then for everyk, every classα ∈ A_k(X)and everyj ≤ r + 1,
c_j(ℰ) ∩ α = c_j(ℱ) ∩ αinA_{k-j}(X).As for the vanishing above, the cap products are the members of families satisfying the characterization of Stacks 02U6, and the proof is the uniqueness of that characterization applied to the family of
ℱextended by zero. The inputs are the ones listed atStacks.Chow.chernCap_top_eq_zero, Stacks 02S1 for the two projections again being supplied fromStacks.Chow.flatPullbackFactorsThroughRationalEquivalence_general.
theorem chernCap_castSucc_eq
(hinj : ProjectiveBundleRelationInjective C sX sP π hsP (r + 2) hπ
(flatPullbackFactorsThroughRationalEquivalence_general C sP sX π hsP (r + 2 - 1) hπ)
twistP)
(hcompat : ChernTermsCompatibleWithTrivialSubbundle C sX sP sQ π hsP ϖ hsQ r hπ hϖ
(flatPullbackFactorsThroughRationalEquivalence_general C sP sX π hsP (r + 2 - 1) hπ)
(flatPullbackFactorsThroughRationalEquivalence_general C sQ sX ϖ hsQ (r + 1 - 1) hϖ)
twistP twistQ ι hι)
(_S : ShortComplex X.Modules)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} _S.X₂ (r + 2)]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} _S.X₃ (r + 1)]
(_hunit : _S.X₁ ≅ (SheafOfModules.unit X.ringCatSheaf : X.Modules))
(_hexact : _S.ShortExact) (k : ℤ) (α : chowGroup C sX k)
(c : ∀ j : Fin (r + 3), chowGroup C sX (k - (j : ℤ)))
(e : ∀ j : Fin (r + 2), chowGroup C sX (k - (j : ℤ)))
(hc : IsChernCapFamily C sX sP π hsP (r + 2) hπ
(flatPullbackFactorsThroughRationalEquivalence_general C sP sX π hsP (r + 2 - 1) hπ)
twistP k α c)
(he : IsChernCapFamily C sX sQ ϖ hsQ (r + 1) hϖ
(flatPullbackFactorsThroughRationalEquivalence_general C sQ sX ϖ hsQ (r + 1 - 1) hϖ)
twistQ k α e) (j : Fin (r + 2)) :
c j.castSucc = e j
Tag 02UH, a lemma
Tag 02UH in the Stacks Project.
Stacks.Chow.chernClassCapExt_succ_eq_add_firstChernCap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernWhitney/CapProductRelation.lean, line 212. The attribute's comment: “CORRECTION OF FORM: the source states c(E) = c(L)c(F) in the bivariant ring A^*(X). That product is not stated here, and cannot be: this development has no ring structure on bivariant classes and no total Chern class, because Chern classes are built as operations CycleGroup C p k -> chowGroup C p (k - j) on X's own cycles (Stacks 02U5) rather than as bivariant classes over all Y -> X -- the source's formulation needs proper pushforward on Chow groups, Stacks 0GU8, which this repository does not have. What is proved instead is the componentwise identity c_{i+1}(E) = c_{i+1}(F) + c₁(L)c_i(F) that the source's own proof reduces the product to, for every n and every cycle alpha in CycleGroup C p n. Carried: hbinom (the equality of binomial transforms that Stacks 02UD at the twists by the inverse of the invertible subsheaf gives once Stacks 02UG is applied to them), the Stacks 02U0 data chernE and chernF, and Stacks 02TI for c₁ of the subsheaf as hfac”.
Stacks 02UH, componentwise on cap products. For a short exact sequence
0 ⟶ S.X₁ ⟶ S.X₂ ⟶ S.X₃ ⟶ 0of finite locally free modules withS.X₁invertible,S.X₂of rankr + 1andS.X₃of rankr, and for everyn-cycleα,
c_{i+1}(S.X₂) ∩ α = c_{i+1}(S.X₃) ∩ α + c₁(S.X₁) ∩ (c_i(S.X₃) ∩ α)in
A_{n-i-1}(X), for everyi ≤ r. Summing overiand expandingc(S.X₁) = 1 + c₁(S.X₁)this is the relationc(S.X₂) = c(S.X₁) · c(S.X₃)of the source; see the module documentation for why the product form cannot be written here.The hypothesis
hbinomis the input: the equality of the binomial transform of the Chern cap products ofS.X₂atr + 1with that ofS.X₃atr, alongc₁of the inverse of the invertible subsheaf. That equality is what Stacks 02UD gives for the twists ofS.X₂andS.X₃byS.X₁^{⊗ -1}once Stacks 02UG has identified the two twisted sheaves' Chern classes, and neither of those tags is proved in this repository.
theorem chernClassCapExt_succ_eq_add_firstChernCap (C : ChowSituation.{u}) {X : Scheme.{u}}
(p : X ⟶ C.S) [LocallyOfFiniteType p] (n : ℤ) (S : ShortComplex X.Modules)
(_hS : S.ShortExact)
[AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property S.X₁]
(r : ℕ) (hrankE : PullbackPreservesRank S.X₂ (r + 1))
(hrankF : PullbackPreservesRank S.X₃ r) (chernE : ChernClassCycleRule C (r + 1))
(chernF : ChernClassCycleRule C r) (hfac : InvertibleChernCapDescends C p S.X₁)
(α : CycleGroup C p n) (i : ℕ) (hi : i + 1 ≤ r + 1)
(hbinom : ∀ m ≤ r + 1,
binomialTransform (inverseFirstChernCapStep C p n S.X₁ hfac) (r + 1)
(chernCapFamily C p n S.X₂ (r + 1) hrankE chernE α) m =
binomialTransform (inverseFirstChernCapStep C p n S.X₁ hfac) r
(chernCapFamily C p n S.X₃ r hrankF chernF α) m) :
chernClassCapExt C p n S.X₂ (r + 1) hrankE chernE (i + 1) α =
chernClassCapExt C p n S.X₃ r hrankF chernF (i + 1) α +
firstChernCapStep C p n S.X₁ hfac i
(chernClassCapExt C p n S.X₃ r hrankF chernF i α)
Stacks.Chow.totalChernClassCohomology_eq_mul_of_shortExact_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernWhitney/InvertibleSubsheaf.lean, line 189. The attribute's comment: “c(E) = c(L) c(F) in the Chow cohomology ring A^(X) of Stacks 0B7E, for a short exact sequence 0 -> L -> E -> F -> 0 on X locally of finite type over the base with L invertible and E, F finite locally free of ranks r, r - 1; c(G) is the sum in A^(X) of the bivariant Chern classes c_j(G) of Stacks 0B7H”.
Stacks 02UH. Let
Xbe locally of finite type over the base and let0 ⟶ ℒ ⟶ ℰ ⟶ ℱ ⟶ 0be a short exact sequence of𝒪_X-modules withℒinvertible andℰ,ℱfinite locally free of ranksr,r - 1. Then
c(ℰ) = c(ℒ) c(ℱ)in the Chow cohomology ring
A^*(X)of Stacks 0B7E,ℒbeing finite locally free of rank one (Stacks 0B8M). This is the Whitney sum formula, Stacks 02UI, for a subsheaf of rank one.
theorem totalChernClassCohomology_eq_mul_of_shortExact_of_isInvertible
(S : ShortComplex Y.Modules) (hS : S.ShortExact)
[AlgebraicGeometry.SheafOfModules.IsInvertible Y.sheaf.obj Y.ringCatSheaf.property S.X₁]
(r : ℕ) [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₂ r]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₃ (r - 1)] :
letI := chowCohomologyRingOfInvertible C sY
haveI := GenuineChern.isFiniteLocallyFreeOfRank_one_of_isInvertible S.X₁
totalChernClassCohomology C sY S.X₂ r =
totalChernClassCohomology C sY S.X₁ 1 * totalChernClassCohomology C sY S.X₃ (r - 1)
Tag 02UI, a lemma
Tag 02UI in the Stacks Project.
Stacks.Chow.chernCapOnChow_eq_sum_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernWhitney/ShortExactSequence.lean, line 419. The attribute's comment: “CORRECTION OF FORM: the source states c(E) = c(E₁)c(E₂) in the bivariant ring A^*(X). That product is not stated here, and cannot be: this development has no ring structure on bivariant classes and no total Chern class, for the reasons recorded on Stacks 02UH in StacksFrontier.AlgebraicGeometry.Chow.ChernWhitney.CapProductRelation -- Chern classes are built as operations on X's own cycles rather than as bivariant classes over all Y -> X, and the source's formulation needs proper pushforward on Chow groups, Stacks 0GU8, which this repository does not have. What is proved instead is the componentwise identity c_m(E) cap alpha = sum over i + j = m of c_i(E₁) cap (c_j(E₂) cap alpha), at arbitrary ranks r₁ of E₁ and r₂ of E₂, for every k and every class alpha in A_k(X) -- which is what the product says once it is expanded, and is the reduction the source's own proof performs. Carried: cap, the Chern cap products on Chow groups of Stacks 0B7G (built there from Stacks 02U5 and Stacks 02U7, neither of which is in this repository); hbase, the relation when E₁ has rank at most one, whose rank-one case is Stacks 02UH -- proved in this repository, but in the vocabulary of the cap product on cycles and under its own carried hypotheses, so it does not supply this statement -- and whose rank-zero case needs the normalisation c_0 = 1 of Stacks 02U0 together with invariance of the cap products under an isomorphism of modules, neither of which holds of a cap rule that is itself a parameter; and hsplit, the splitting datum of the source's induction, namely the projective space bundle of E₁ with its flat pullback injective (Stacks 02TX) and compatible with the cap products (Stacks 02U8), its twist (Stacks 01O4), and the three short exact sequences the source forms on it. The rank of the middle term is an instance hypothesis rather than derived, as it is for Stacks 02UH; AlgebraicGeometry.SheafOfModules.rank_add_of_shortExact shows r₁ + r₂ is its only possible value. NOT carried, and proved here: the associativity of the convolution, the descent along the injective pullback, and the induction on r₁ itself”.
Stacks 02UI, componentwise on cap products. For a short exact sequence
0 ⟶ S.X₁ ⟶ S.X₂ ⟶ S.X₃ ⟶ 0of finite locally free modules of ranksr₁,r₁ + r₂andr₂, for every classα ∈ A_k(X)and everym,
c_m(S.X₂) ∩ α = ∑_{i + j = m} c_i(S.X₁) ∩ (c_j(S.X₃) ∩ α)inA_{k-m}(X),the sum being taken over
j ≤ mwithi = m - j, and thei-th Chern class read as zero above the rank. Assembling these overmand expanding the product, this is the relationc(S.X₂) = c(S.X₁) · c(S.X₃)of the source; see the module documentation for why the product form cannot be written here.The hypotheses
hbaseandhsplitare the inputs: the relation for a sub-module of rank at most one, whose rank-one case is Stacks 02UH, and the splitting datum of the source's induction, which carries the projective space bundle ofS.X₁together with Stacks 02TX and Stacks 02U8.
theorem chernCapOnChow_eq_sum_of_shortExact (C : ChowSituation.{u})
(cap : ∀ r : ℕ, HigherChernCapRule C r)
(hbase : ∀ r₁ ≤ 1, WhitneyChernRelation C cap r₁) (hsplit : HasChernSplitting C cap)
{T : Scheme.{u}} (q : T ⟶ C.S) [LocallyOfFiniteType q] (S : ShortComplex T.Modules)
(hS : S.ShortExact) (r₁ r₂ : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₁ r₁]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₂ (r₁ + r₂)]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₃ r₂]
(k : ℤ) (m : ℕ) (α : chowGroup C q k) :
chernCapFamilyOnChow C cap q S.X₂ (r₁ + r₂) k m α =
∑ j : Fin (m + 1),
gradedDegreeCast (chowGroup C q)
(show k - (j.val : ℤ) - ((m - j.val : ℕ) : ℤ) = k - (m : ℤ) from by
have := j.isLt; omega)
(chernCapFamilyOnChow C cap q S.X₁ r₁ (k - (j.val : ℤ)) (m - j.val)
(chernCapFamilyOnChow C cap q S.X₃ r₂ k (j.val) α))
Stacks.Chow.totalChernClassCohomology_eq_mul_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernWhitney/WhitneyChowCohomology.lean, line 223. The attribute's comment: “c(E) = c(E₁) c(E₂) in the Chow cohomology ring A^(X) of Stacks 0B7E, for a short exact sequence 0 -> E₁ -> E -> E₂ -> 0 on X locally of finite type over the base with E₁, E₂ finite locally free of ranks r₁, r₂ (E is then finite locally free of rank r₁ + r₂); c(F) is the sum in A^(X) of the bivariant Chern classes c_j(F) of Stacks 0B7H”.
Stacks 02UI, the Whitney sum formula. Let
Xbe locally of finite type over the base and let0 ⟶ ℰ₁ ⟶ ℰ ⟶ ℰ₂ ⟶ 0be a short exact sequence of𝒪_X-modules withℰ₁,ℰ₂finite locally free of ranksr₁,r₂; thenℰis finite locally free of rankr₁ + r₂(Stacks.Chow.GenuineChern.isFiniteLocallyFreeOfRank_of_shortExact), and the total Chern classes satisfy
c(ℰ) = c(ℰ₁) c(ℰ₂)inA^*(X).
theorem totalChernClassCohomology_eq_mul_of_shortExact (S : ShortComplex Y.Modules)
(hS : S.ShortExact) (r₁ r₂ : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₁ r₁]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} S.X₃ r₂] :
letI := chowCohomologyRingOfInvertible C sY
haveI := GenuineChern.isFiniteLocallyFreeOfRank_of_shortExact S hS r₁ r₂ ‹_› ‹_›
totalChernClassCohomology C sY S.X₂ (r₁ + r₂) =
totalChernClassCohomology C sY S.X₁ r₁ * totalChernClassCohomology C sY S.X₃ r₂
Tag 02UJ, a lemma
Tag 02UJ in the Stacks Project.
Stacks.Chow.chernClassCapExt_eq_elemSymmChernCap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernWhitney/FilteredAdditivity.lean, line 275. The attribute's comment: “the degree-k coefficients of c(E) = prod (1 + c_1(L_i)), stated on the cap products of 02U5 for k >= 1 rather than as a product in A^*(X), which has no multiplication here; the filtration enters as the tower of its quotients; 02U0, 02TI, 02UD+02UG are inputs”.
Stacks 02UJ, componentwise on cap products. Let
ℰ = Q_rbe finite locally free of rankrwith a filtration whose successive quotients are the invertible modulesL 0, …, L (r-1), presented as the tower of short exact sequences0 ⟶ L j ⟶ Q_{j+1} ⟶ Q_j ⟶ 0. Then for everyn-cycleαand everyk ≥ 1
c_k(ℰ) ∩ α = e_k(c₁(L 0), …, c₁(L (r-1))) ∩ ⟦α⟧in
A_{n-k}(X), thek-th elementary symmetric function of the first Chern class cap operations of the quotients applied to the class ofα. This is the coefficient of degreekin the product formulac(ℰ) = ∏_i (1 + c₁(ℒ_i))of the source.The normalisation
hnormis asked for only at the rank-zero bottomQ_0of the tower: in degree zero a binomial transform is its own zeroth entry, sohbinomalready identifies the degree-zero cap products of consecutive members, and the normalisation at every stage — in particular atℰ = Q_r— follows by induction. See the module documentation for why the product itself cannot be written here, for why the assertion is made in degreesk ≥ 1, and for the inputshbinom,chernandhfac.
theorem chernClassCapExt_eq_elemSymmChernCap (Q : ℕ → X.Modules)
(sub : ∀ j : Fin r, L j ⟶ Q ((j : ℕ) + 1)) (proj : ∀ j : Fin r, Q ((j : ℕ) + 1) ⟶ Q (j : ℕ))
(hzero : ∀ j : Fin r, sub j ≫ proj j = 0)
(hexact : ∀ j : Fin r, (ShortComplex.mk (sub j) (proj j) (hzero j)).ShortExact)
(hrank : ∀ m : ℕ, m ≤ r → PullbackPreservesRank (Q m) m)
(chern : ∀ m : ℕ, ChernClassCycleRule C m) (α : CycleGroup C p n)
(hnorm : chernClassCapExt C p n (Q 0) 0 (hrank 0 (Nat.zero_le r)) (chern 0) 0 α =
cycleClassDegreeZero C p n α)
(hbinom : ∀ j : Fin r, ∀ i ≤ (j : ℕ) + 1,
binomialTransform (inverseFirstChernCapStep C p n (L j) (hfac j)) ((j : ℕ) + 1)
(chernCapFamily C p n (Q ((j : ℕ) + 1)) ((j : ℕ) + 1) (hrank ((j : ℕ) + 1) j.isLt)
(chern ((j : ℕ) + 1)) α) i =
binomialTransform (inverseFirstChernCapStep C p n (L j) (hfac j)) (j : ℕ)
(chernCapFamily C p n (Q (j : ℕ)) (j : ℕ) (hrank (j : ℕ) j.isLt.le)
(chern (j : ℕ)) α) i)
(k : ℕ) (_hk : 1 ≤ k) :
chernClassCapExt C p n (Q r) r (hrank r le_rfl) (chern r) k α =
elemSymmChernCap C p n L hfac r le_rfl k
(QuotientAddGroup.mk' (rationalEquivalences C p n) α)
Stacks.Chow.totalChernClassCohomology_eq_prod_of_filtration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernWhitney/FiltrationChowCohomology.lean, line 249. The attribute's comment: “c(E) = prod_{i=1}^r (1 + c_1(L_i)) in the Chow cohomology ring A^*(X) of Stacks 0B7E, for E with a filtration 0 = E_0 ⊂ E_1 ⊂ ... ⊂ E_r = E by subobjects with E_i/E_{i-1} ≅ L_i invertible, on X locally of finite type over the base; c_1(L_i) is the class of Stacks 0B77 and E is shown to be finite locally free of rank r”.
Stacks 02UJ. Let
Xbe locally of finite type over the base, letℒ_1, …, ℒ_rbe invertible𝒪_X-modules and letℰbe an𝒪_X-module with a filtration by submodules
0 = ℰ_0 ⊂ ℰ_1 ⊂ ℰ_2 ⊂ … ⊂ ℰ_r = ℰsuch thatℰ_i/ℰ_{i-1} ≅ ℒ_i.Then
ℰis finite locally free of rankr(Stacks.Chow.isFiniteLocallyFreeOfRank_of_filtration), and, settingx_i = c_1(ℒ_i),
c(ℰ) = ∏_{i=1}^r (1 + x_i)inA^*(X).The filtration is indexed by
Fin (r + 1)and the invertible modules byFin r, so thatℒ iis the quotientℰ_{i+1}/ℰ_i; the product is(1 + x_1)(1 + x_2) ⋯ (1 + x_r)in this order.
theorem totalChernClassCohomology_eq_prod_of_filtration (r : ℕ) (E : Y.Modules)
(L : Fin r → Y.Modules)
[∀ i, AlgebraicGeometry.SheafOfModules.IsInvertible Y.sheaf.obj Y.ringCatSheaf.property (L i)]
(F : Fin (r + 1) → Subobject E) (hF : Monotone F) (h0 : F 0 = ⊥) (hr : F (Fin.last r) = ⊤)
(e : ∀ i : Fin r,
cokernel (Subobject.ofLE (F i.castSucc) (F i.succ) (hF i.castSucc_le_succ)) ≅ L i) :
letI := chowCohomologyRingOfInvertible C sY
haveI := isFiniteLocallyFreeOfRank_of_filtration E L F hF h0 hr e
totalChernClassCohomology C sY E r =
(List.ofFn fun i ↦ 1 + DirectSum.of
(fun p ↦ chowCohomologyComponent C (gysinSystemOfInvertible C) sY p) 1
(GenuineChern.firstChernClass C sY (L i))).prod
Sources
Section42.41 Degrees of zero cycles#
Section 42.41 of the Stacks Project, Tag 0AZ0. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0AZ1, a definition
Tag 0AZ1 in the Stacks Project.
Stacks.Chow.chowDegree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/DegreeHomomorphism.lean, line 67. The attribute's comment: “the degree homomorphism”.
Stacks Project, Tag 0AZ1. The degree homomorphism
A_0(X) ⟶ ℤon the zeroth Chow group of a schemeXproper over a one-point base with vanishing dimension function — the spectrum of a field.This is the definition of Stacks 0AZ1 verbatim: proper pushforward
p_* : A_0(X) ⟶ A_0(S)of Stacks 0GU8, which exists by Stacks 02S2 (Stacks.Chow.properPushforwardFactorsThroughRationalEquivalence_of_isProper), composed with the identificationA_0(S) = ℤofStacks.Chow.chowGroupBaseEquivInt, which sends the fundamental cycle of the base to one.
def chowDegree (s : C.S) : chowGroup C p 0 →+ ℤ
Stacks.Chow.chowGroupBaseEquivInt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/ZeroCycleDegree.lean, line 213. The attribute's comment: “the identification of the Chow group of the base with the integers”.
For a one-point base with vanishing dimension function — the spectrum of a field — the degree of a zero cycle is an isomorphism
A_0(S) ≅ ℤ, sending the fundamental cycle to1.
def chowGroupBaseEquivInt (s : C.S) : chowGroup C (𝟙 C.S) 0 ≃+ ℤ
Tag 0AZ2, a lemma
Tag 0AZ2 in the Stacks Project.
Stacks.Chow.cycleDegree_eq_sum_finrank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/ZeroCycleDegreeFormula.lean, line 170.
The degree
Stacks.Chow.cycleDegreeof a zero cycle on a scheme proper over a field, presented as a finite sumα = ∑ n_i [Z_i]over integral closed subschemes of delta-dimension zero, is∑ n_i dim_k Γ(Z_i, 𝒪_{Z_i}), wheredim_k Γ(Z_i, 𝒪_{Z_i})is the degree ofZ_i → Spec(k).
theorem cycleDegree_eq_sum_finrank [IsProper p] (s : (fieldChowSituation k).S)
(α : CycleGroup (fieldChowSituation k) p 0) {J : Type*} [Fintype J]
(W : J → X.IdealSheafData) (hW : ∀ i, IsIntegral (W i).subscheme) (n : J → ℤ)
(hDim : ∀ i, schemeDeltaDimension (fieldChowSituation k) ((W i).subschemeι ≫ p) = (0 : EInt))
(hα : α.1 = ∑ i, @Function.locallyFinsuppWithin.single X _ ℤ (Classical.decEq X) _
(genericPointOf (W i) (hW i)) (n i)) :
cycleDegree (fieldChowSituation k) p s α =
∑ i : J, n i *
(letI : Algebra k Γ((W i).subscheme, ⊤) :=
((Scheme.ΓSpecIso (.of k)).inv ≫ ((W i).subschemeι ≫ p).appTop).hom.toAlgebra
(Module.finrank k Γ((W i).subscheme, ⊤) : ℤ))
Tag 0AZ3, a lemma
Tag 0AZ3 in the Stacks Project.
AlgebraicGeometry.curveDegree_eq_chowDegree_firstChernCapOnCycles_fundamental, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/RiemannRochGenuine.lean, line 305.
Equation [Stacks, Tag 0BRY], in the orientation of the source:
deg(ℰ) = deg(c₁(ℰ) ∩ [X]_1)forℰfinite locally free of constant rank on a proper scheme of dimension at most one over a field, withc₁(ℰ) ∩ -the operation of Stacks 02U5 at the Chern classes of Stacks 02U0 anddegthe degree of Stacks 0AZ1.Two conventions are fixed here. In rank zero Stacks 02U5 defines no
c₁; the total Chern class of a module of rank zero is1, soc₁ = 0, andGenuineChern.firstChernCapOnCyclesis zero there by definition. The operation of Stacks 02U5 extends[W] ↦ i_*(c₁(i^*ℰ) ∩ [W])over cycles through representatives of the classes of Stacks 02U0 (GenuineChern.chowRep); the choice does not matter here, since[X]_1is a finite sum of fundamental cycles of one-dimensional components and on each the class is the one of Stacks 02U0 (GenuineChern.chernCapOnCycles_integral_cycle).
theorem curveDegree_eq_chowDegree_firstChernCapOnCycles_fundamental
(hdim : topologicalKrullDim X ≤ 1) (E : X.Modules) (r : ℕ)
[SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r] :
curveDegree k p hdim E r =
chowDegree (fieldChowSituation k) (fieldChowSituation_dimensionFunction_eq_zero k) p
(IsLocalRing.closedPoint k)
(chowGroupCast (fieldChowSituation k) p (show (1 : ℤ) - 1 = 0 by simp)
(GenuineChern.firstChernCapOnCycles (fieldChowSituation k) p E r 1
(cycleAssociatedToClosedSubscheme (fieldChowSituation k) p (𝟙 X) 1)))
Tag 0BFI, a lemma
Tag 0BFI in the Stacks Project.
AlgebraicGeometry.intersectionNumber_eq_chowDegree_iteratedFirstChernCap_and_ample, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/NumericalIntersections/ChowDegree.lean, line 1155.
Let
kbe a field, letXbe a proper scheme overkand letZ ⊆ Xbe a closed subscheme of dimensiond. For invertible𝒪_X-modules𝓛_1, …, 𝓛_d,
(𝓛_1 ⋯ 𝓛_d · Z) = deg(c₁(𝓛_1) ∩ ⋯ ∩ c₁(𝓛_d) ∩ [Z]_d),and in particular, for an ample invertible
𝒪_X-module𝓛,
deg_𝓛(Z) = deg(c₁(𝓛)^d ∩ [Z]_d).Here
(𝓛_1 ⋯ 𝓛_d · Z)is the intersection number of [Stacks, Tag 0BEP],deg_𝓛(Z)the degree of [Stacks, Tag 0BEW], anddegthe degree of zero cycles of [Stacks, Tag 0AZ1], for the Chow groups overSpec kwith its zero dimension function.
theorem intersectionNumber_eq_chowDegree_iteratedFirstChernCap_and_ample {X Z : Scheme.{u}}
(f : X ⟶ Spec (.of k)) [IsProper f] (i : Z ⟶ X) [IsClosedImmersion i] (d : ℕ)
(dimZ : topologicalKrullDim Z = d) :
(∀ (L : Fin d → X.Modules) [∀ j, SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L j)],
intersectionNumber k f i d dimZ.le L =
chowDegree (fieldChowSituation k) (fieldChowSituation_dimensionFunction_eq_zero k) f
(IsLocalRing.closedPoint k)
(iteratedFirstChernCap k f L
(QuotientAddGroup.mk' (rationalEquivalences (fieldChowSituation k) f d)
(cycleAssociatedToClosedSubscheme (fieldChowSituation k) f i d)))) ∧
(∀ (L : X.Modules) [SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L]
(ample : Scheme.Modules.IsAmple X L),
degreeWithRespectTo k f i d dimZ L ample =
chowDegree (fieldChowSituation k) (fieldChowSituation_dimensionFunction_eq_zero k) f
(IsLocalRing.closedPoint k)
(iteratedFirstChernCap k f (fun _ : Fin d => L)
(QuotientAddGroup.mk' (rationalEquivalences (fieldChowSituation k) f d)
(cycleAssociatedToClosedSubscheme (fieldChowSituation k) f i d))))
Sources
Section42.42 Cycles of given codimension#
Section 42.42 of the Stacks Project, Tag 0FE2. 2 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0FE3, a lemma
Tag 0FE3 in the Stacks Project.
Stacks.Chow.IsLocallyEquidimensional.of_isCohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Codimension/CohenMacaulayCase.lean, line 46. The attribute's comment: “cohen_macaulay_case”.
Stacks 0FE3. The relative dimension function of a Cohen--Macaulay scheme locally of finite type over the base of a Chow situation is locally equidimensional: at each point, all irreducible components through it have the same relative dimension at their generic points.
theorem IsLocallyEquidimensional.of_isCohenMacaulay (B : ChowSituation.{u}) (X : Scheme.{u})
(f : X ⟶ B.S) [LocallyOfFiniteType f] (hX : IsCohenMacaulay X) :
IsLocallyEquidimensional (relativeDimension B.dimensionFunction f)
Stacks.Chow.HasDimensionDecomposition.of_isCohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Codimension/CohenMacaulayCase.lean, line 70. The attribute's comment: “cohen_macaulay_case”.
Stacks 0FE3. A Cohen--Macaulay scheme locally of finite type over the base of a Chow situation decomposes into open and closed subschemes of constant relative dimension.
theorem HasDimensionDecomposition.of_isCohenMacaulay (B : ChowSituation.{u}) (X : Scheme.{u})
(f : X ⟶ B.S) [LocallyOfFiniteType f] (hX : IsCohenMacaulay X) :
HasDimensionDecomposition (relativeDimension B.dimensionFunction f)
Stacks.Chow.IsLocallyPureDimensional.of_isCohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Codimension/CohenMacaulayCase.lean, line 79. The attribute's comment: “cohen_macaulay_case”.
Stacks 0FE3. The relative dimension function of a Cohen--Macaulay scheme locally of finite type over the base of a Chow situation is locally pure dimensional.
theorem IsLocallyPureDimensional.of_isCohenMacaulay (B : ChowSituation.{u}) (X : Scheme.{u})
(f : X ⟶ B.S) [LocallyOfFiniteType f] (hX : IsCohenMacaulay X) :
IsLocallyPureDimensional (relativeDimension B.dimensionFunction f)
Stacks.Chow.locallyEquidimensional_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Codimension/Equidimensional.lean, line 182. The attribute's comment: “equivalent_conditions”.
Stacks 0FE3. For an integer-valued function on a locally Noetherian scheme, having a decomposition into pure-dimensional open and closed subschemes, being locally pure dimensional, and being locally equidimensional are equivalent.
theorem locallyEquidimensional_tfae (X : Scheme.{u}) [IsLocallyNoetherian X] (δ : X → ℤ) :
List.TFAE [
HasDimensionDecomposition δ,
IsLocallyPureDimensional δ,
IsLocallyEquidimensional δ]
Stacks.Chow.HasDimensionDecomposition.of_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Codimension/NormalCase.lean, line 96. The attribute's comment: “normal_case”.
Stacks 0FE3. A locally Noetherian normal scheme decomposes into open and closed subschemes on whose irreducible components any given integer-valued function is constant at the generic points, the constant being the index of the piece.
theorem HasDimensionDecomposition.of_isNormal (X : Scheme.{u}) [IsLocallyNoetherian X]
[IsNormal X] (δ : X → ℤ) : HasDimensionDecomposition δ
Stacks.Chow.IsLocallyPureDimensional.of_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Codimension/NormalCase.lean, line 130. The attribute's comment: “normal_case”.
Stacks 0FE3. On a locally Noetherian normal scheme every integer-valued function is locally pure dimensional.
theorem IsLocallyPureDimensional.of_isNormal (X : Scheme.{u}) [IsLocallyNoetherian X]
[IsNormal X] (δ : X → ℤ) : IsLocallyPureDimensional δ
Stacks.Chow.IsLocallyEquidimensional.of_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Codimension/NormalCase.lean, line 137. The attribute's comment: “normal_case”.
Stacks 0FE3. On a locally Noetherian normal scheme every integer-valued function is locally equidimensional.
theorem IsLocallyEquidimensional.of_isNormal (X : Scheme.{u}) [IsLocallyNoetherian X]
[IsNormal X] (δ : X → ℤ) : IsLocallyEquidimensional δ
Tag 0FE4, a remark
Tag 0FE4 in the Stacks Project.
Stacks.Chow.fundamentalClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Codimension/FundamentalClass.lean, line 60. The attribute's comment: “fundamental_class”.
Stacks 0FE4. The fundamental class
[X] = ∑_n [X_n]_nof a scheme whose relative dimension function has a dimension decomposition: the family whosenth coordinate is the class inCH_n(X_n)of the cycle associated to the pieceX_nitself.
def fundamentalClass (C : ChowSituation.{u}) {X : Scheme.{u}} (f : X ⟶ C.S)
[LocallyOfFiniteType f]
(h : HasDimensionDecomposition (relativeDimension C.dimensionFunction f)) :
degreeZeroChowGroup C f h
Sources
Section42.43 The splitting principle#
Section 42.43 of the Stacks Project, Tag 02UK. 6 tags here are carried by 38 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02UL, a lemma
Tag 02UL in the Stacks Project.
Stacks.Chow.exists_splittingMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/FlagBundle.lean, line 461. The attribute's comment: “clauses (1) and (2) over X itself, for a finite collection of finite locally free modules of constant ranks, with relative dimension d = sum of binom(r_i, 2). Carries the projective bundle of a finite locally free module of rank m+1 as a BundleStep, i.e. as Stacks 02TX for flatness, properness (Stacks 0800) and relative dimension m, Stacks 02S1 for the descent of flat pullback to Chow groups, Stacks 01O4, 02SO and 02TI for c_1(O_P(1)) cap -, the injectivity half of Stacks 02TX for the projective space bundle map, and Stacks 0B3V for the tautological short exact sequence with locally free kernel of rank m. Injectivity of pi^* itself is NOT carried: it is derived from the 02TX bundle map. The source says projective; only properness is carried through the tower, because IsProjectiveMorphism of the identity needs the identification of P^0_X with X, which this repository lacks. Clause (1) after a base change is exists_splittingMorphism_basechange”.
Stacks 02UL, the splitting principle. Let
(S, δ)be the situation of Stacks 02QL, letXbe locally of finite type overSand letℰ_i,i ∈ Ifinite, be finite locally free𝒪_X-modules of ranksr_i. There is a flat proper morphismπ : P ⟶ Xof relative dimensiond = ∑_i binom(r_i, 2)such that
- the flat pullback
π^* : A_k(X) ⟶ A_{k+d}(P)of Stacks 0FVK is injective in every degree, and- each
π^*ℰ_ihas a filtration of lengthr_iwhose successive quotients are invertible𝒪_P-modules.The relative dimension is
∑_i binom(r_i, 2)and not∑_i (r_i - 1): splitting a rank-rmodule takesr - 1layers, of relative dimensionsr - 1, r - 2, …, 1.
theorem exists_splittingMorphism (C : ChowSituation.{u})
(step : ∀ {Y : Scheme.{u}} (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (F : Y.Modules) (m : ℕ),
AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F (m + 1) →
BundleStep C sY F m)
{X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (I : Type) [Fintype I]
(E : I → X.Modules) (r : I → ℕ)
(hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (E i) (r i)) :
∃ T : SplittingMorphism C sX (∑ i, (r i).choose 2),
∀ i, Stacks.WeilCohomology.HasInvertibleFiltration T.P
((Scheme.Modules.pullback T.π).obj (E i)) (r i)
Stacks.Chow.exists_splittingMorphism_basechange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/FlagBundle.lean, line 495. The attribute's comment: “clause (1) after a base change, in the WEAKENED form that for EACH f : Y -> X there is a morphism P_Y -> Y with the same relative dimension, the same filtrations and injectivity in every degree. It is NOT asserted that P_Y is the fibre product Y x_X P of the single morphism delivered by exists_splittingMorphism, so this is weaker than clause (1) of the source. The reason is NOT that the base-change comparison of projective bundles is missing: the comparison projectiveBundleBaseChange and the cartesianness of its square (isPullback_projectiveBundleBaseChange) are both proved in this repository, untagged, and relative dimension is stable under base change by Stacks 02NK. What is missing is Stacks 02S1 for the base-changed projections (never derived for a base change here), base-change compatibility of the carried BundleStep, and the identification of the base change of the tower with the tower of base changes. Carries the same BundleStep operator as exists_splittingMorphism”.
Stacks 02UL, clause (1) after an arbitrary base change. For every
f : Y ⟶ XwithYlocally of finite type over the base there is a flat proper morphismπ_Y : P_Y ⟶ Yof the same relative dimensiond = ∑_i binom(r_i, 2)along which flat pullback on Chow groups is injective in every degree, and such that eachπ_Y^* f^* ℰ_ihas a filtration of lengthr_iwith invertible successive quotients.This is the splitting principle run over
Yon the modulesf^*ℰ_i, whose ranks are ther_ibecause finite local freeness of given rank is stable under pullback. It does not assert thatP_YisY ×_X Pfor thePofStacks.Chow.exists_splittingMorphism, and that is a genuine weakening of clause (1).
theorem exists_splittingMorphism_basechange (C : ChowSituation.{u})
(step : ∀ {Y : Scheme.{u}} (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (F : Y.Modules) (m : ℕ),
AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F (m + 1) →
BundleStep C sY F m)
{X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (I : Type) [Fintype I]
(E : I → X.Modules) (r : I → ℕ)
(hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (E i) (r i))
{Y : Scheme.{u}} (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : Y ⟶ X) :
∃ T : SplittingMorphism C sY (∑ i, (r i).choose 2),
∀ i, Stacks.WeilCohomology.HasInvertibleFiltration T.P
((Scheme.Modules.pullback T.π).obj ((Scheme.Modules.pullback f).obj (E i))) (r i)
Stacks.Chow.exists_splittingMorphism_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/FlagBundleUnconditional.lean, line 564. The attribute's comment: “clauses (1) and (2) over X itself, for a finite collection of finite locally free modules of constant ranks r_i, with relative dimension d = sum of binom(r_i, 2), and NOTHING CARRIED: the only hypotheses are that each module is finite locally free of constant rank r_i. The layer of the tower is the projective bundle of the module itself, Stacks.Chow.bundleStep, so every fact about it that the parametrised form exists_splittingMorphism takes in its step argument is PROVED here: Stacks 02TX for flatness and relative dimension m of the projection (Stacks.Chow.flat_bundleProj, Stacks.Chow.relativeDimension_bundleProj -- for an arbitrary module of constant rank, not only for a free one), Stacks 0800 for properness (Stacks.Chow.isProper_bundleProj), Stacks 02S1 for the descent of flat pullback to Chow groups (Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_general, with nothing carried), Stacks 01O4, 02SO and 02TI for c_1(O_P(1)) cap - (Stacks.Chow.bundleTwist with Stacks.Chow.invCap), the injectivity half of Stacks 02TX for the projective space bundle map (Stacks.Chow.projectiveBundleRelationInjective_of_bundleMap at Stacks.Chow.projectiveBundle_formula), and Stacks 0B3V for the tautological short exact sequence with locally free kernel of rank m (Stacks.Chow.shortExact_bundleTautological, Stacks.Chow.isFiniteLocallyFreeOfRank_kernel_bundleTautological, including the rank-one end m = 0 where the kernel has rank zero). Injectivity of pi^* itself is derived from the 02TX bundle map, not assumed. WEAKENED IN ONE WORD: the source says the morphism is projective and only properness is delivered, because IsProjectiveMorphism of the identity of X needs the identification of P^0_X with X, which this repository lacks. Clause (1) of the source quantifies over every f : Y -> X, and that full form is exists_splittingMorphism_basechange_uniform, which is about the single morphism this theorem delivers”.
The splitting principle. Let
Xbe locally of finite type over the baseSofCand letℰ_i,i ∈ Ifinite, be finite locally free𝒪_X-modules of constant ranksr_i. There is a flat proper morphismπ : P ⟶ Xof relative dimensiond = ∑_i binom(r_i, 2)such that
- the flat pullback
π^* : A_k(X) ⟶ A_{k+d}(P)is injective in every degree, and- each
π^*ℰ_ihas a filtration of lengthr_iwhose successive quotients are invertible𝒪_P-modules.
theorem exists_splittingMorphism_unconditional (C : ChowSituation.{u}) {X : Scheme.{u}}
(sX : X ⟶ C.S) [LocallyOfFiniteType sX] (I : Type) [Fintype I] (E : I → X.Modules)
(r : I → ℕ)
(hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (E i) (r i)) :
∃ T : SplittingMorphism C sX (∑ i, (r i).choose 2),
∀ i, Stacks.WeilCohomology.HasInvertibleFiltration T.P
((Scheme.Modules.pullback T.π).obj (E i)) (r i)
Stacks.Chow.exists_splittingMorphism_basechange_uniform, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/FlagBundleUnconditional.lean, line 614. The attribute's comment: “clauses (1) and (2) for a finite collection of finite locally free modules of constant ranks r_i, with relative dimension d = sum of binom(r_i, 2), and with clause (1) in the form the source states it: ONE morphism pi : P -> X, and for EVERY f : Y -> X injectivity in every degree of the flat pullback along the base change of that pi, which is Stacks.Chow.BaseChangeInjective quantified over every cartesian square over pi and f. The only hypotheses are the source's: each module finite locally free of constant rank r_i. Clause (1) is proved through the iteration -- base case the identity of X, whose base change is an isomorphism; inductive step the splitting of the base change of a composite by CategoryTheory.IsPullback.of_bot together with Stacks 02RD for a composite pullback, the base-changed layer being the projective bundle of the pulled-back module by Stacks.ProjectiveBundle.isPullback_baseChangeHom and its pullback injective by the injectivity half of Stacks 02TX. The single word of the tag delivered more weakly is projective, delivered as proper: IsProjectiveMorphism of the identity of X needs the identification of P^0_X with X, which this repository lacks”.
The splitting principle with injectivity after every base change. Let
Xbe locally of finite type over the baseSofCand letℰ_i,i ∈ Ifinite, be finite locally free𝒪_X-modules of constant ranksr_i. There is a single flat proper morphismπ : P ⟶ Xof relative dimensiond = ∑_i binom(r_i, 2)such that
- for any
f : Y ⟶ XwithYlocally of finite type over the base, the flat pullbackπ_Y^* : A_k(Y) ⟶ A_{k+d}(Y ×_X P)along the base change ofπis injective in every degree, and- each
π^*ℰ_ihas a filtration of lengthr_iwhose successive quotients are invertible𝒪_P-modules.
theorem exists_splittingMorphism_basechange_uniform (C : ChowSituation.{u}) {X : Scheme.{u}}
(sX : X ⟶ C.S) [LocallyOfFiniteType sX] (I : Type) [Fintype I] (E : I → X.Modules)
(r : I → ℕ)
(hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (E i) (r i)) :
∃ T : SplittingMorphism C sX (∑ i, (r i).choose 2),
BaseChangeInjective C sX T.π (∑ i, (r i).choose 2) ∧
∀ i, Stacks.WeilCohomology.HasInvertibleFiltration T.P
((Scheme.Modules.pullback T.π).obj (E i)) (r i)
Stacks.Chow.exists_splittingMorphism_isProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/SplittingProjective.lean, line 181.
Stacks 02UL (the splitting principle). Let
(S, δ)be as in Situation 02QL,Xlocally of finite type overSandℰ_i(i ∈ I,Ifinite) finite locally free𝒪_X-modules of ranksr_i. There is a morphismπ : P ⟶ Xwhich is
- projective (Stacks 01W8), flat, and of relative dimension
d = ∑_i binom(r_i, 2),such that
- for every morphism
f : Y ⟶ XwithYlocally of finite type overS, the flat pullbackπ_Y^* : CH_k(Y) ⟶ CH_{k+d}(Y ×_X P)along the base change ofπis injective for everyk(Stacks.Chow.UniversallyChowInjective), and- each
π^*ℰ_ihas a filtration whose successive quotientsℒ_{i,1}, …, ℒ_{i,r_i}are invertible𝒪_P-modules;moreover the restriction map
A^*(X) ⟶ A^*(P)of Stacks 0B7F is injective.
theorem exists_splittingMorphism_isProjective (C : ChowSituation.{u}) {X : Scheme.{u}}
(sX : X ⟶ C.S) [LocallyOfFiniteType sX] (I : Type) [Fintype I] (E : I → X.Modules)
(r : I → ℕ)
(hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (E i) (r i)) :
∃ T : SplittingMorphism C sX (∑ i, (r i).choose 2),
IsProjective T.π ∧ Flat T.π ∧
AlgebraicGeometry.RelativeDimension T.π (∑ i, (r i).choose 2) ∧
UniversallyChowInjective C T.π (∑ i, (r i).choose 2) T.relDim ∧
(∀ i, Stacks.WeilCohomology.HasInvertibleFiltration T.P
((Scheme.Modules.pullback T.π).obj (E i)) (r i)) ∧
∀ (G : GysinSystem C) (hgys : G.IsNaturalUnderBaseChangeIso),
Function.Injective (chowCohomologyTotalRestriction C G sX T.π hgys)
Stacks.Chow.exists_splittingMorphism_isProjective_ofInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/SplittingProjectiveOfInvertible.lean, line 77.
Stacks 02UL (the splitting principle). Let
(S, δ)be as in Situation 02QL,Xlocally of finite type overSandℰ_i(i ∈ I,Ifinite) finite locally free𝒪_X-modules of ranksr_i. There is a morphismπ : P ⟶ Xwhich is
- projective (Stacks 01W8), flat, and of relative dimension
d = ∑_i binom(r_i, 2),such that
- for every morphism
f : Y ⟶ XwithYlocally of finite type overS, the flat pullbackπ_Y^* : CH_k(Y) ⟶ CH_{k+d}(Y ×_X P)along the base change ofπis injective for everyk(Stacks.Chow.UniversallyChowInjective), and- each
π^*ℰ_ihas a filtration whose successive quotientsℒ_{i,1}, …, ℒ_{i,r_i}are invertible𝒪_P-modules;moreover the restriction map
res : A^*(X) ⟶ A^*(P)of Stacks 0B7F,Stacks.Chow.chowCohomologyTotalRestrictionRingOfInvertible, is injective. Nothing is assumed beyond the hypotheses of the tag.
theorem exists_splittingMorphism_isProjective_ofInvertible (C : ChowSituation.{u})
{X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (I : Type) [Fintype I]
(E : I → X.Modules) (r : I → ℕ)
(hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (E i) (r i)) :
∃ T : SplittingMorphism C sX (∑ i, (r i).choose 2),
IsProjective T.π ∧ Flat T.π ∧
AlgebraicGeometry.RelativeDimension T.π (∑ i, (r i).choose 2) ∧
UniversallyChowInjective C T.π (∑ i, (r i).choose 2) T.relDim ∧
(∀ i, Stacks.WeilCohomology.HasInvertibleFiltration T.P
((Scheme.Modules.pullback T.π).obj (E i)) (r i)) ∧
Function.Injective (chowCohomologyTotalRestrictionRingOfInvertible C sX T.π)
Stacks.Chow.exists_splittingMorphism_universal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/Unconditional.lean, line 439. The attribute's comment: “both clauses, clause (1) in the source's form: for every f : Y -> X, with Y locally of finite type over S by an arbitrary structure morphism, flat pullback along the base change Y x_X P -> Y is injective in every degree. Relative dimension d = sum of binom(r_i, 2). The source says projective; the morphism delivered is flat and proper (each layer is a projective bundle, proper by Stacks 0800), but H-projectivity of the tower is not proved”.
Stacks 02UL, the splitting principle. Let
(S, δ)be the situation of Stacks 02QL, letXbe locally of finite type overSand letℰ_i,i ∈ Ifinite, be finite locally free𝒪_X-modules of ranksr_i. There is a flat proper morphismπ : P ⟶ Xof relative dimensiond = ∑_i binom(r_i, 2), along which flat pullback on Chow groups is injective in every degree, such that
- for every morphism
f : Y ⟶ XwithYlocally of finite type overSthe flat pullbackπ_Y^* : A_k(Y) ⟶ A_{k+d}(Y ×_X P)along the base changeπ_Y : Y ×_X P ⟶ Yis injective in every degree, and- each
π^*ℰ_ihas a filtration of lengthr_iwhose successive quotients are invertible𝒪_P-modules.The morphism is the iterated projective bundle (
Stacks.Chow.BundleStep.ofProjectiveBundle); clause (1) is carried through the iteration asStacks.Chow.UniversallyInjectiveFlatPullback.
theorem exists_splittingMorphism_universal (C : ChowSituation.{u}) {X : Scheme.{u}}
(sX : X ⟶ C.S) [LocallyOfFiniteType sX] (I : Type) [Fintype I] (E : I → X.Modules)
(r : I → ℕ)
(hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (E i) (r i)) :
∃ T : SplittingMorphism C sX (∑ i, (r i).choose 2),
(∀ {Y : Scheme.{u}} (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : Y ⟶ X) (k : ℤ),
Function.Injective (flatPullbackChow C (pullback.fst f T.π ≫ sY) sY (pullback.fst f T.π)
rfl (∑ i, (r i).choose 2)
(AlgebraicGeometry.RelativeDimension.of_isPullback
(IsPullback.of_hasPullback f T.π).flip T.relDim) k
(flatPullbackFactorsThroughRationalEquivalence_general C _ _ _ _ _ _ _))) ∧
∀ i, Stacks.WeilCohomology.HasInvertibleFiltration T.P
((Scheme.Modules.pullback T.π).obj (E i)) (r i)
Tag 0FVE, a remark
Tag 0FVE in the Stacks Project.
Stacks.Chow.exists_splittingMorphism_isBundleTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/ProjectiveBundleTower.lean, line 174. The attribute's comment: “clause (1) only: the 02UL morphism is a constant-rank projective bundle tower”.
The morphism
π : P ⟶ Xof Stacks 02UL is a finite composition of projective space bundles associated to locally free modules of finite constant rank.Let
(S, δ)be the situation of Stacks 02QL, letXbe locally of finite type overSand letℰ_i,i ∈ Ifinite, be finite locally free𝒪_X-modules of ranksr_i. Then there is a splitting morphismT, flat and proper of relative dimensiond = ∑_i binom(r_i, 2), with injective flat pullback on Chow groups in every degree, splitting everyℰ_i, and satisfyingStacks.Chow.IsBundleTower: it is the identity ofXor the projection of one layer𝐏(ℰ)withℰfinite locally free of constant rank, composed with such a tower over𝐏(ℰ).
theorem exists_splittingMorphism_isBundleTower (C : ChowSituation.{u})
(step : ∀ {Y : Scheme.{u}} (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (F : Y.Modules) (m : ℕ),
AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F (m + 1) →
BundleStep C sY F m)
{X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (I : Type) [Fintype I]
(E : I → X.Modules) (r : I → ℕ)
(hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (E i) (r i)) :
∃ T : SplittingMorphism C sX (∑ i, (r i).choose 2),
IsBundleTower C sX (∑ i, (r i).choose 2) T ∧
∀ i, Stacks.WeilCohomology.HasInvertibleFiltration T.P
((Scheme.Modules.pullback T.π).obj (E i)) (r i)
Stacks.Chow.exists_splittingMorphism_isProjectiveBundleTower_recoversByCaps, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/SplittingTowerRecovery.lean, line 590.
Stacks 0FVE. Let
(S, δ)be as in Situation 02QL,Xlocally of finite type overSandℰ_i(i ∈ I, finite) finite locally free𝒪_X-modules of ranksr_i. The morphismπ : P ⟶ Xbuilt in the proof of Stacks 02UL — flat and proper of relative dimensiond = ∑_i binom(r_i, 2), with injective flat pullback on Chow groups, such that eachπ^*ℰ_ihas a filtration with invertible successive quotients — has the further properties
πis a finite composition of projective space bundles associated to finite locally free modules of constant rank (Stacks.Chow.IsProjectiveBundleTower, whose layers are the actual projective bundlesStacks.Chow.bundle), and- there are invertible
𝒪_P-modulesL_1, …, L_dsuch that, withξ_j = c₁(L_j), everyα ∈ CH_k(X)satisfiesα = π_*(ξ_1 ∩ ⋯ ∩ ξ_d ∩ π^*α).
theorem exists_splittingMorphism_isProjectiveBundleTower_recoversByCaps (C : ChowSituation.{u})
{X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (I : Type) [Fintype I]
(E : I → X.Modules) (r : I → ℕ)
(hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (E i) (r i)) :
∃ T : SplittingMorphism C sX (∑ i, (r i).choose 2),
(∀ i, Stacks.WeilCohomology.HasInvertibleFiltration T.P
((Scheme.Modules.pullback T.π).obj (E i)) (r i)) ∧
IsProjectiveBundleTower C sX (∑ i, (r i).choose 2) T ∧
∃ (Ls : List (InvertibleModule T.P)) (hLs : Ls.length = ∑ i, (r i).choose 2),
∀ (k : ℤ) (α : chowGroup C sX k),
properChowPushforward C T.sP sX T.π T.hsP k
(properPushforwardFactorsThroughRationalEquivalence_of_isProper C T.sP sX T.π
T.hsP k)
(iteratedChernCapOnChow C T.sP (invCapList C T.sP Ls) k
(chowGroupCast C T.sP (by rw [length_invCapList, hLs])
(T.pullbackChow k α))) = α
Tag 0FA5, a lemma
Tag 0FA5 in the Stacks Project.
Stacks.Chow.GenuineChern.chernClass_dualSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/ChernClassDual.lean, line 396. The attribute's comment: “THE BIVARIANT AND UNCONDITIONAL FORM, an ADDITIONAL carrier -- the registration that already stood, Stacks.Chow.chernClassCapExt_eq_zsmul_of_dualFiltration, states the rule in the cycle vocabulary and carries two complete filtrations plus six further hypotheses, and Stacks.Chow.HasDualChernSignRule (which carries no attribute) states it as an assumed Prop on a carried total Chern class series; neither is superseded, because the three speak about three different renderings of c_i in this repository. WHAT IS PROVED HERE: for every scheme X locally of finite type over the base of chapter 42, every finite locally free O_X-module E of rank r, and every i with 0 <= i <= r, the equality c_i(E^dual) = (-1)^i c_i(E) of BIVARIANT CLASSES in A^i(X) -- the group of bivariant classes of degree i for the identity of X, Tag 0B76 -- at the Chern classes Stacks.Chow.GenuineChern.chernClass of Tag 0B7H. HYPOTHESES: exactly the rank, i.e. E is finite locally free of rank r, plus X locally of finite type over the base. NOTHING ELSE IS CARRIED: no filtration of E and no filtration of E^dual, no splitting datum, no normalisation c_0 = 1, no binomial-transform equality, and no assumed compatibility of the cap products with flat pullback -- the last of these is now proved in this repository (Stacks.Chow.GenuineChern.intertwines_chernFamily, Tag 02U8), which is what makes the source's reduction performable. The source's first paragraph -- choose pi : P -> X as in Tag 02UL, use injectivity of pi^ to reduce to a filtered E, dualise the filtration -- is replaced by an induction on r through the projective bundle P(E) of E alone: the tautological sequence 0 -> F -> pi^E -> O(1) -> 0 has F finite locally free of rank r-1, its dual is short exact by the exactness of duality (Tag 0FV8), and the Whitney sum formula of Tag 02UI (unconditional here) computes both total Chern classes upstairs. This avoids the obstruction recorded at Stacks.Chow.chernClassCapExt_eq_zsmul_of_dualFiltration, namely that the filtration delivered by Tag 02UL is an inductive Prop from which the tower of modules Tag 02UJ takes as input cannot be eliminated: no filtration is ever needed, only one short exact sequence per inductive step. The rank of the dual is Stacks.AlgebraicGeometry.ReflexiveModules.isFiniteLocallyFreeOfRank_dualSheaf (the dual-at-a-constant-rank clause of Tag 0FA7), which is what lets c_i(E^dual) be written at all. The dual is Stacks.AlgebraicGeometry.ReflexiveModules.dualSheaf, SheafHom(E, O_X) itself, and not a chosen tensor inverse. Also proved here, degreewise on cap products, is Stacks.Chow.GenuineChern.chernCap_dualSheaf, the same identity for the cap products of Tag 02U6”.
Stacks 0FA5, bivariantly and unconditionally. For a finite locally free
𝒪_X-moduleℰof rankron a schemeXlocally of finite type over the base and every0 ≤ i ≤ r,
c_i(ℰ^∨) = (-1)^i c_i(ℰ)in
A^i(X), the group of bivariant classes of degreeifor𝟙 Xof Stacks 0B76, for the Chern classesStacks.Chow.GenuineChern.chernClassof Stacks 0B7H.A bivariant class satisfying the characterization of Stacks 0B7H is unique (
Stacks.Chow.eq_of_isChernClassBivariant), so it suffices to check that(-1)^i c_i(ℰ)caps byc_i(g^*(ℰ^∨)) ∩ -on every test schemeg : T ⟶ X. Integer multiples of bivariant classes are pointwise on cap products, so the left side is(-1)^i (c_i(g^*ℰ) ∩ -), and that isc_i(g^*(ℰ^∨)) ∩ -byStacks.Chow.GenuineChern.chernCap_dualSheafapplied tog^*ℰ, once the base-change isomorphism of Tag 0GMX identifiesg^*(ℰ^∨)with(g^*ℰ)^∨.
theorem chernClass_dualSheaf {X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
(E : X.Modules) (r : ℕ)
[hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r]
(j : Fin (r + 1)) :
haveI := Stacks.AlgebraicGeometry.ReflexiveModules.isFiniteLocallyFreeOfRank_dualSheaf E r hE
chernClass C sX (dualSheaf E) r j = ((-1 : ℤ) ^ (j : ℕ)) • chernClass C sX E r j
Stacks.Chow.SectionZeroScheme.chernClassOfLocallyFree_dualSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SectionZeroScheme/ArbitraryRankDual.lean, line 151. The attribute's comment: “c_i(E^dual) = (-1)^i c_i(E) in A^i(X) for every finite locally free E (rank not necessarily constant) and every i >= 0, at the Chern classes of Tag 0ESW built from those of Tag 0B7H”.
Stacks 0FA5. For a finite locally free
𝒪_X-moduleℰon a schemeXlocally of finite type over the base, of rank not necessarily constant, and everyi ≥ 0,
c_i(ℰ^∨) = (-1)^i c_i(ℰ)in
A^i(X), for the Chern classesStacks.Chow.SectionZeroScheme.chernClassOfLocallyFreeof Stacks 0ESW, built from the bivariant Chern classes of Stacks 0B7H on the rank loci.Both sides are compared on the rank loci of
ℰ, which are those ofℰ^∨(Stacks.Chow.SectionZeroScheme.rankLocus_dualSheaf); onX_rthe identity is the constant-rank caseStacks.Chow.GenuineChern.chernClass_dualSheaftogether with(ℰ^∨)|_{X_r} ≅ (ℰ|_{X_r})^∨, and fori > rboth sides restrict to zero.
theorem chernClassOfLocallyFree_dualSheaf (i : ℕ) :
haveI := isFiniteLocallyFree_dualSheaf E hE
chernClassOfLocallyFree (dualSheaf E) C sX i =
((-1 : ℤ) ^ i) • chernClassOfLocallyFree E C sX i
Stacks.Chow.chernClassCapExt_eq_zsmul_of_dualFiltration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/DualChernClasses.lean, line 248. The attribute's comment: “CORRECTION OF FORM: the source states c_i(E^dual) = (-1)^i c_i(E) in the bivariant ring A^i(X). This development has no bivariant ring and no total Chern class, for the reason recorded in the Stacks 02UH clause of StacksFrontier.AlgebraicGeometry.Chow.ChernWhitney.CapProductRelation, so -- exactly as for Stacks 02UJ, which this result is read on top of -- the identity is stated degree by degree as cap products against a fixed cycle: for every n, every alpha in CycleGroup C p n and every i >= 0, c_i(E^dual) cap alpha = (-1)^i times (c_i(E) cap alpha) in A_{n-i}(X). It holds for EVERY i and EVERY rank r; no degree and no rank is special-cased. WHAT IS CARRIED: the reduction of the source's first paragraph, i.e. the two filtrations themselves, as the towers of short exact sequences that Stacks 02UJ consumes -- for E with invertible quotients L_j, and for E^dual with quotients M_j satisfying L_j tensor M_j iso O_X, which is the source's E_{i-1}^perp/E_i^perp iso L_i^{tensor -1}. The source gets these from Stacks 02UL and the injectivity of pi^. That reduction CANNOT be performed in this repository, for two independent reasons: (1) Stacks 02UL is Stacks.Chow.exists_splittingMorphism and the filtration it delivers is Stacks.WeilCohomology.HasInvertibleFiltration, an inductive Prop, from which the tower of modules and maps that Stacks 02UJ needs -- which is data -- cannot be eliminated; (2) nothing in this repository states that the Chern class cap product commutes with flat pullback (the clause of Stacks 02U0 quoted as Stacks 02U1), so injectivity of pi^ has no identity on P to descend to X. ALSO CARRIED, each of them an input of Stacks 02UJ itself and carried there for the same reason: chern and chernDual, the Stacks 02U0 component data in every rank; hnorm and hnormDual, the Stacks 02U0 normalisation c_0 = 1 along each tower; hbinom and hbinomDual, the equality of binomial transforms that Stacks 02UD gives once Stacks 02UG is applied, neither of which is proved here; and hfacL, hfacM, Stacks 02TI for c_1 of each quotient. NOT CARRIED, i.e. proved here: the line-bundle case c_1(L^{tensor -1}) = -c_1(L), deduced from the two clauses of Stacks 02SP as firstChernCapStep_eq_neg_of_tensorObj_iso_unit and absent from this repository before this file; and the formal computation the source omits, e_k(-x) = (-1)^k e_k(x), proved for every degree and every length as elemSymmChernCap_eq_zsmul_of_neg_steps. The dual is given as a tensor inverse rather than as Stacks.SheafOfModules.dualSheaf; by Stacks 0B8K the two agree up to isomorphism and c_1 depends only on the isomorphism class (firstChernClassCapOfInvertible_congr), so this is a change of spelling and not a weakening”.
Stacks 0FA5, componentwise on cap products. Let
ℰbe finite locally free of rankrwith a filtration whose successive quotients are the invertible modulesℒ_0, …, ℒ_{r-1}, and letℰ^∨be finite locally free of rankrwith the dual filtration, whose successive quotientsℳ_jare tensor inverses of theℒ_j. Both filtrations are presented as the towers of short exact sequences0 ⟶ ℒ_j ⟶ ℰ_{j+1} ⟶ ℰ_j ⟶ 0and0 ⟶ ℳ_j ⟶ ℰ^∨_{j+1} ⟶ ℰ^∨_j ⟶ 0that Stacks 02UJ consumes. Then for everyn-cycleαand everyi
c_i(ℰ^∨) ∩ α = (-1)^i • (c_i(ℰ) ∩ α)in
A_{n-i}(X), which is the sign rule of the source read degree by degree againstα.
theorem chernClassCapExt_eq_zsmul_of_dualFiltration
(hdual : ∀ j, Scheme.Modules.tensorObj (L j) (M j) ≅ SheafOfModules.unit X.ringCatSheaf)
(E EDual : ℕ → X.Modules)
(sub : ∀ j : Fin r, L j ⟶ E ((j : ℕ) + 1)) (proj : ∀ j : Fin r, E ((j : ℕ) + 1) ⟶ E (j : ℕ))
(hzero : ∀ j : Fin r, sub j ≫ proj j = 0)
(hexact : ∀ j : Fin r, (ShortComplex.mk (sub j) (proj j) (hzero j)).ShortExact)
(hrank : ∀ m : ℕ, m ≤ r → PullbackPreservesRank (E m) m)
(subDual : ∀ j : Fin r, M j ⟶ EDual ((j : ℕ) + 1))
(projDual : ∀ j : Fin r, EDual ((j : ℕ) + 1) ⟶ EDual (j : ℕ))
(hzeroDual : ∀ j : Fin r, subDual j ≫ projDual j = 0)
(hexactDual : ∀ j : Fin r,
(ShortComplex.mk (subDual j) (projDual j) (hzeroDual j)).ShortExact)
(hrankDual : ∀ m : ℕ, m ≤ r → PullbackPreservesRank (EDual m) m)
(chern chernDual : ∀ m : ℕ, ChernClassCycleRule C m) (α : CycleGroup C p n)
(hnorm : ∀ (m : ℕ) (hm : m ≤ r),
chernClassCapExt C p n (E m) m (hrank m hm) (chern m) 0 α = cycleClassDegreeZero C p n α)
(hnormDual : ∀ (m : ℕ) (hm : m ≤ r),
chernClassCapExt C p n (EDual m) m (hrankDual m hm) (chernDual m) 0 α =
cycleClassDegreeZero C p n α)
(hbinom : ∀ j : Fin r, ∀ i ≤ (j : ℕ) + 1,
binomialTransform (inverseFirstChernCapStep C p n (L j) (hfacL j)) ((j : ℕ) + 1)
(chernCapFamily C p n (E ((j : ℕ) + 1)) ((j : ℕ) + 1) (hrank ((j : ℕ) + 1) j.isLt)
(chern ((j : ℕ) + 1)) α) i =
binomialTransform (inverseFirstChernCapStep C p n (L j) (hfacL j)) (j : ℕ)
(chernCapFamily C p n (E (j : ℕ)) (j : ℕ) (hrank (j : ℕ) j.isLt.le)
(chern (j : ℕ)) α) i)
(hbinomDual : ∀ j : Fin r, ∀ i ≤ (j : ℕ) + 1,
binomialTransform (inverseFirstChernCapStep C p n (M j) (hfacM j)) ((j : ℕ) + 1)
(chernCapFamily C p n (EDual ((j : ℕ) + 1)) ((j : ℕ) + 1)
(hrankDual ((j : ℕ) + 1) j.isLt) (chernDual ((j : ℕ) + 1)) α) i =
binomialTransform (inverseFirstChernCapStep C p n (M j) (hfacM j)) (j : ℕ)
(chernCapFamily C p n (EDual (j : ℕ)) (j : ℕ) (hrankDual (j : ℕ) j.isLt.le)
(chernDual (j : ℕ)) α) i)
(k : ℕ) :
chernClassCapExt C p n (EDual r) r (hrankDual r le_rfl) (chernDual r) k α =
((-1 : ℤ) ^ k) • chernClassCapExt C p n (E r) r (hrank r le_rfl) (chern r) k α
Stacks.Chow.homPart_totalChern_dualSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/DualTotalChern.lean, line 282. The attribute's comment: “constant rank: for every X locally of finite type over S, every finite locally free E of rank r and every i, with no further hypothesis. c_i(E) is the degree-i part TotalChowClass.homComponent i (totalChern C sX E r) of the total Chern class in the ring TotalChowClass C sX of total Chow cohomology classes, the bivariant Chern class of Stacks 0B7H, and E^dual is the dual sheaf Stacks.AlgebraicGeometry.ReflexiveModules.dualSheaf E = SheafHom(E, O_X)”.
Stacks 0FA5, constant rank: for
ℰfinite locally free of rankronX,
c_i(ℰ^∨) = (-1)^i c_i(ℰ)in
A^i(X), for everyi, wherec_i(-)is the degree-ipart of the total Chern class, the bivariant Chern class of Stacks 0B7H, andℰ^∨is the dual sheafSheafHom(ℰ, 𝒪_X).
theorem homPart_totalChern_dualSheaf (E : X.Modules) (r : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r] (i : ℕ) :
TotalChowClass.homComponent i (totalChern C sX (dualSheaf E) r) =
((-1 : ℤ) ^ i) • TotalChowClass.homComponent i (totalChern C sX E r)
Stacks.Chow.homPart_totalChernOfFiniteLocallyFree_dualSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/DualTotalChern.lean, line 320. The attribute's comment: “the lemma as stated, for every X locally of finite type over S, every finite locally free E (rank not assumed constant) and every i, with no further hypothesis. c_i(E) is the degree-i part of totalChernOfFiniteLocallyFree C sX E, the total Chern class of Stacks 0ESW in the ring TotalChowClass C sX of total Chow cohomology classes, and E^dual is the dual sheaf Stacks.AlgebraicGeometry.ReflexiveModules.dualSheaf E = SheafHom(E, O_X)”.
Stacks 0FA5: for
ℰfinite locally free onX, of arbitrary rank,
c_i(ℰ^∨) = (-1)^i c_i(ℰ)in
A^i(X), for everyi, wherec_i(-)is the degree-ipart of the total Chern class of Stacks 0ESW, which on the locus whereℰhas rankris the bivariant Chern class of Stacks 0B7H.
theorem homPart_totalChernOfFiniteLocallyFree_dualSheaf (E : X.Modules)
[hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E] (i : ℕ) :
haveI := Stacks.AlgebraicGeometry.ReflexiveModules.isFiniteLocallyFree_dualSheaf E hE
TotalChowClass.homComponent i (totalChernOfFiniteLocallyFree C sX (dualSheaf E)) =
((-1 : ℤ) ^ i) • TotalChowClass.homComponent i (totalChernOfFiniteLocallyFree C sX E)
Tag 0FA6, a lemma
Tag 0FA6 in the Stacks Project.
Stacks.Chow.chernClassCapExt_tensorObj_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/TensorChernClasses.lean, line 982. The attribute's comment: “the first displayed identity, componentwise on cap products, and conditional. CORRECTION OF FORM: the source states c_1(E tensor F) = r c_1(F) + s c_1(E) in the bivariant ring A^(X). This development has no bivariant ring and no total Chern class, for the reason recorded in the Stacks 02UH clause of StacksFrontier.AlgebraicGeometry.Chow.ChernWhitney.CapProductRelation, so -- exactly as for Stacks 02UJ and Stacks 0FA5, which this result is read on top of -- the identity is stated degree by degree as cap products against a fixed cycle: for every n and every alpha in CycleGroup C p n, c_1(E tensor F) cap alpha = s times (c_1(E) cap alpha) plus r times (c_1(F) cap alpha) in A_{n-1}(X). The module on the left is the library's canonical tensor product AlgebraicGeometry.Scheme.Modules.tensorObj of the two bundles, identified with the top of the tensor filtration by the hypothesis hTop. WHAT IS CARRIED: the reduction of the source's proof to the filtered case, i.e. the three filtrations themselves, as the towers of short exact sequences that Stacks 02UJ consumes -- for E with invertible quotients L_i, for F with invertible quotients N_j, and for E tensor F with quotients M_k, together with hquot, the source's lexicographic identification M_{is+j} iso L_i tensor N_j. The source gets these from Stacks 02UL and the injectivity of pi^, and that reduction CANNOT be performed in this repository, for the two independent reasons recorded in the Stacks 0FA5 clause of StacksFrontier.AlgebraicGeometry.Chow.SplittingPrinciple.DualChernClasses: Stacks 02UL is formalized as Stacks.Chow.exists_splittingMorphism and delivers Stacks.WeilCohomology.HasInvertibleFiltration, an inductive Prop from which the tower of modules and maps that Stacks 02UJ needs -- which is data -- cannot be eliminated; and nothing in this repository states that the Chern class cap product commutes with flat pullback (the clause of Stacks 02U0 quoted as Stacks 02U1), so injectivity of pi^ has no identity on P to descend to X. ALSO CARRIED, each of them an input of Stacks 02UJ itself and carried there for the same reason: chernE, chernF, chernT, the Stacks 02U0 component data in every rank; hnormE, hnormF, hnormT, the Stacks 02U0 normalisation c_0 = 1 along each tower; hbinomE, hbinomF, hbinomT, the equality of binomial transforms that Stacks 02UD gives once Stacks 02UG is applied, neither of which is proved here; hfacL, hfacN, hfacM, Stacks 02TI for c_1 of each quotient; and hrankTensor, the rank-preservation of the tensor product in rank rs, carried exactly as StacksFrontier.AlgebraicGeometry.Chow.ChernClassTwist carries hrankEL for a twist -- the rank multiplicativity of a tensor product has no library presence in the PullbackPreservesRank form the cap products need. NOT CARRIED, i.e. proved here: Stacks 02SP for the descended operations, firstChernCapStep_eq_add_of_iso_tensorObj, giving c_1(L tensor N) cap - = c_1(L) cap - + c_1(N) cap -, which is absent from this repository before this file; and the degree-one half of the formal computation the source omits, namely that the sum over the lexicographic family of the rs operations c_1(L_i) + c_1(N_j) is s times the sum of the c_1(L_i) plus r times the sum of the c_1(N_j), proved for every r and every s as sum_range_lexFamily. Stacks 02TJ is NOT needed for this identity and is NOT carried: sum_range_lexFamily is proved for an arbitrary ring. It is carried by the degree-two identity chernClassCapExt_tensorObj_two, where it is genuinely needed”.
Stacks 0FA6, the first displayed identity, componentwise on cap products. Let
ℰ = E rbe finite locally free of rankrwith a filtration whose successive quotients are the invertible modulesℒ_i = L i, letℱ = F sbe finite locally free of rankswith a filtration whose successive quotients are the invertible modules𝒩_j = N j, and let the towerTbe a filtration ofℰ ⊗_{𝒪_X} ℱof lengthr·swhose(i·s+j)-th successive quotient isℒ_i ⊗_{𝒪_X} 𝒩_j, which is the lexicographic filtration of the source. Then for everyn-cycleα
c₁(ℰ ⊗ ℱ) ∩ α = s·(c₁(ℰ) ∩ α) + r·(c₁(ℱ) ∩ α)in
A_{n-1}(X), which is the identityc₁(ℰ ⊗ ℱ) = r·c₁(ℱ) + s·c₁(ℰ)of the source read againstα. The rank hypotheses enter as the lengthsrandsof the two filtrations, as the rankr·sof the tensor product, and as the two coefficients.
theorem chernClassCapExt_tensorObj_one
(hnormE : ∀ (m : ℕ) (hm : m ≤ r),
chernClassCapExt C p n (E m) m (hrankE m hm) (chernE m) 0 α = cycleClassDegreeZero C p n α)
(hbinomE : ∀ i : Fin r, ∀ t ≤ (i : ℕ) + 1,
binomialTransform (inverseFirstChernCapStep C p n (L i) (hfacL i)) ((i : ℕ) + 1)
(chernCapFamily C p n (E ((i : ℕ) + 1)) ((i : ℕ) + 1) (hrankE ((i : ℕ) + 1) i.isLt)
(chernE ((i : ℕ) + 1)) α) t =
binomialTransform (inverseFirstChernCapStep C p n (L i) (hfacL i)) (i : ℕ)
(chernCapFamily C p n (E (i : ℕ)) (i : ℕ) (hrankE (i : ℕ) i.isLt.le)
(chernE (i : ℕ)) α) t)
(hnormF : ∀ (m : ℕ) (hm : m ≤ s),
chernClassCapExt C p n (F m) m (hrankF m hm) (chernF m) 0 α = cycleClassDegreeZero C p n α)
(hbinomF : ∀ j : Fin s, ∀ t ≤ (j : ℕ) + 1,
binomialTransform (inverseFirstChernCapStep C p n (N j) (hfacN j)) ((j : ℕ) + 1)
(chernCapFamily C p n (F ((j : ℕ) + 1)) ((j : ℕ) + 1) (hrankF ((j : ℕ) + 1) j.isLt)
(chernF ((j : ℕ) + 1)) α) t =
binomialTransform (inverseFirstChernCapStep C p n (N j) (hfacN j)) (j : ℕ)
(chernCapFamily C p n (F (j : ℕ)) (j : ℕ) (hrankF (j : ℕ) j.isLt.le)
(chernF (j : ℕ)) α) t)
(hnormT : ∀ (m : ℕ) (hm : m ≤ r * s),
chernClassCapExt C p n (T m) m (hrankT m hm) (chernT m) 0 α = cycleClassDegreeZero C p n α)
(hbinomT : ∀ k : Fin (r * s), ∀ t ≤ (k : ℕ) + 1,
binomialTransform (inverseFirstChernCapStep C p n (M k) (hfacM k)) ((k : ℕ) + 1)
(chernCapFamily C p n (T ((k : ℕ) + 1)) ((k : ℕ) + 1) (hrankT ((k : ℕ) + 1) k.isLt)
(chernT ((k : ℕ) + 1)) α) t =
binomialTransform (inverseFirstChernCapStep C p n (M k) (hfacM k)) (k : ℕ)
(chernCapFamily C p n (T (k : ℕ)) (k : ℕ) (hrankT (k : ℕ) k.isLt.le)
(chernT (k : ℕ)) α) t)
(hquot : ∀ (i : Fin r) (j : Fin s),
M (finLexIndex i j) ≅ Scheme.Modules.tensorObj (L i) (N j))
(hTop : T (r * s) = Scheme.Modules.tensorObj (E r) (F s))
(hrankTensor : PullbackPreservesRank (Scheme.Modules.tensorObj (E r) (F s)) (r * s)) :
chernClassCapExt C p n (Scheme.Modules.tensorObj (E r) (F s)) (r * s) hrankTensor
(chernT (r * s)) 1 α
= (s : ℤ) • chernClassCapExt C p n (E r) r (hrankE r le_rfl) (chernE r) 1 α
+ (r : ℤ) • chernClassCapExt C p n (F s) s (hrankF s le_rfl) (chernF s) 1 α
Stacks.Chow.chernClassCapExt_tensorObj_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/TensorChernClasses.lean, line 1091. The attribute's comment: “the second displayed identity, componentwise on cap products, and conditional. CORRECTION OF FORM: the source states c_2(E tensor F) = r c_2(F) + s c_2(E) + binom(r,2) c_1(F)^2 + (rs - 1) c_1(F) c_1(E) + binom(s,2) c_1(E)^2 in the bivariant ring A^(X). This development has no bivariant ring and no total Chern class, for the reason recorded in the Stacks 02UH clause of StacksFrontier.AlgebraicGeometry.Chow.ChernWhitney.CapProductRelation, so -- exactly as for Stacks 02UJ and Stacks 0FA5, which this result is read on top of -- the identity is stated degree by degree as cap products against a fixed cycle: for every n and every alpha in CycleGroup C p n, c_2(E tensor F) cap alpha = s times (c_2(E) cap alpha) plus r times (c_2(F) cap alpha) plus binom(r,2) times (c_1(F) cap (c_1(F) cap alpha)) plus (rs - 1) times (c_1(E) cap (c_1(F) cap alpha)) plus binom(s,2) times (c_1(E) cap (c_1(E) cap alpha)) in A_{n-2}(X). The cross-term coefficient is rs - 1, as in the source, and NOT rs. The five summands appear in a different order from the source's; addition is commutative. Each squared or mixed term is a COMPOSITE of operations rather than a product of classes, with the outer factor the descended operation firstChernCapSum -- the sum of the Stacks 02TI operations of the quotients of the relevant filtration, identified with c_1 cap - by firstChernCapSum_eq_chernClassCapExt_one -- and the inner factor the Stacks 02U5 cap product itself: the cap products of Stacks 02U5 go from cycles to Chow classes and so cannot be iterated, and there is no ring in which c_1(F)^2 would be a class. The module on the left is the library's canonical tensor product AlgebraicGeometry.Scheme.Modules.tensorObj of the two bundles, identified with the top of the tensor filtration by the hypothesis hTop. WHAT IS CARRIED: exactly what chernClassCapExt_tensorObj_one carries, and for the same reasons -- the three filtrations as the towers Stacks 02UJ consumes together with hquot, the source's lexicographic identification M_{is+j} iso L_i tensor N_j, because the reduction via Stacks 02UL and the injectivity of pi^ cannot be performed in this repository; the Stacks 02U0 data chern and normalisations hnorm; the binomial-transform agreements hbinom that Stacks 02UD and Stacks 02UG would give; Stacks 02TI for c_1 of each quotient as hfac; and hrankTensor, the rank-preservation of the tensor product in rank rs, which has no library presence in the PullbackPreservesRank form the cap products need and is carried exactly as StacksFrontier.AlgebraicGeometry.Chow.ChernClassTwist carries hrankEL for a twist. ADDITIONALLY CARRIED here, and not by the degree-one identity: Stacks 02TJ, as hcommLL, hcommNN and hcommLN, the commutativity of the first Chern class cap operations of the quotients. This repository proves Stacks 02TJ only with Stacks 02TH carried as a hypothesis (Stacks.Chow.firstChernClassCapOnChowOfInvertible_comm) and at a different presentation of the descended operation, so the statement itself is carried. It is genuinely needed: the source works in a commutative ring, and without commutativity the degree-two elementary symmetric function of the lexicographic family does not collapse -- the cancellation that turns the block-dependent coefficient s(i+1) - 1 into the constant rs - 1 is exactly a commutation. NOT CARRIED, i.e. proved here: Stacks 02SP for the descended operations (firstChernCapStep_eq_add_of_iso_tensorObj), absent from this repository before this file; and the whole of the formal computation the source omits, in degree two and for every r and every s, as esymRec_block_increment, esymRec_two_block and esymRec_two_tensor”.
Stacks 0FA6, the second displayed identity, componentwise on cap products. In the situation of
Stacks.Chow.chernClassCapExt_tensorObj_one, for everyn-cycleα
c₂(ℰ ⊗ ℱ) ∩ α = s·(c₂(ℰ) ∩ α) + r·(c₂(ℱ) ∩ α) + C(r,2)·(c₁(ℱ) ∩ (c₁(ℱ) ∩ α)) + (r·s − 1)·(c₁(ℰ) ∩ (c₁(ℱ) ∩ α)) + C(s,2)·(c₁(ℰ) ∩ (c₁(ℰ) ∩ α))in
A_{n-2}(X), which is the identityc₂(ℰ ⊗ ℱ) = r·c₂(ℱ) + s·c₂(ℰ) + C(r,2)·c₁(ℱ)² + (r·s − 1)·c₁(ℱ)·c₁(ℰ) + C(s,2)·c₁(ℰ)²of the source read againstα, its five summands in a different order. The coefficient of the cross term isr·s − 1.The outer first Chern class of each of the three iterated terms is
Stacks.Chow.firstChernCapSum, the sum of the first Chern class cap operations of the quotients of the corresponding filtration, whichStacks.Chow.firstChernCapSum_eq_chernClassCapExt_oneidentifies withc₁ ∩ -; the inner one is the Chern class cap product of Stacks 02U5 itself. Writing the squares this way is forced: the cap products of Stacks 02U5 go from cycles to Chow classes, so they cannot be iterated, and this development has no bivariant ring in whichc₁(ℱ)²would be a class.
theorem chernClassCapExt_tensorObj_two
(hnormE : ∀ (m : ℕ) (hm : m ≤ r),
chernClassCapExt C p n (E m) m (hrankE m hm) (chernE m) 0 α = cycleClassDegreeZero C p n α)
(hbinomE : ∀ i : Fin r, ∀ t ≤ (i : ℕ) + 1,
binomialTransform (inverseFirstChernCapStep C p n (L i) (hfacL i)) ((i : ℕ) + 1)
(chernCapFamily C p n (E ((i : ℕ) + 1)) ((i : ℕ) + 1) (hrankE ((i : ℕ) + 1) i.isLt)
(chernE ((i : ℕ) + 1)) α) t =
binomialTransform (inverseFirstChernCapStep C p n (L i) (hfacL i)) (i : ℕ)
(chernCapFamily C p n (E (i : ℕ)) (i : ℕ) (hrankE (i : ℕ) i.isLt.le)
(chernE (i : ℕ)) α) t)
(hnormF : ∀ (m : ℕ) (hm : m ≤ s),
chernClassCapExt C p n (F m) m (hrankF m hm) (chernF m) 0 α = cycleClassDegreeZero C p n α)
(hbinomF : ∀ j : Fin s, ∀ t ≤ (j : ℕ) + 1,
binomialTransform (inverseFirstChernCapStep C p n (N j) (hfacN j)) ((j : ℕ) + 1)
(chernCapFamily C p n (F ((j : ℕ) + 1)) ((j : ℕ) + 1) (hrankF ((j : ℕ) + 1) j.isLt)
(chernF ((j : ℕ) + 1)) α) t =
binomialTransform (inverseFirstChernCapStep C p n (N j) (hfacN j)) (j : ℕ)
(chernCapFamily C p n (F (j : ℕ)) (j : ℕ) (hrankF (j : ℕ) j.isLt.le)
(chernF (j : ℕ)) α) t)
(hnormT : ∀ (m : ℕ) (hm : m ≤ r * s),
chernClassCapExt C p n (T m) m (hrankT m hm) (chernT m) 0 α = cycleClassDegreeZero C p n α)
(hbinomT : ∀ k : Fin (r * s), ∀ t ≤ (k : ℕ) + 1,
binomialTransform (inverseFirstChernCapStep C p n (M k) (hfacM k)) ((k : ℕ) + 1)
(chernCapFamily C p n (T ((k : ℕ) + 1)) ((k : ℕ) + 1) (hrankT ((k : ℕ) + 1) k.isLt)
(chernT ((k : ℕ) + 1)) α) t =
binomialTransform (inverseFirstChernCapStep C p n (M k) (hfacM k)) (k : ℕ)
(chernCapFamily C p n (T (k : ℕ)) (k : ℕ) (hrankT (k : ℕ) k.isLt.le)
(chernT (k : ℕ)) α) t)
(hquot : ∀ (i : Fin r) (j : Fin s),
M (finLexIndex i j) ≅ Scheme.Modules.tensorObj (L i) (N j))
(hcommLL : ∀ a b : Fin r, FirstChernCapStepsCommute C p n (L a) (L b) (hfacL a) (hfacL b))
(hcommNN : ∀ a b : Fin s, FirstChernCapStepsCommute C p n (N a) (N b) (hfacN a) (hfacN b))
(hcommLN : ∀ (a : Fin r) (b : Fin s),
FirstChernCapStepsCommute C p n (L a) (N b) (hfacL a) (hfacN b))
(hTop : T (r * s) = Scheme.Modules.tensorObj (E r) (F s))
(hrankTensor : PullbackPreservesRank (Scheme.Modules.tensorObj (E r) (F s)) (r * s)) :
chernClassCapExt C p n (Scheme.Modules.tensorObj (E r) (F s)) (r * s) hrankTensor
(chernT (r * s)) 2 α
= (s : ℤ) • chernClassCapExt C p n (E r) r (hrankE r le_rfl) (chernE r) 2 α
+ (r : ℤ) • chernClassCapExt C p n (F s) s (hrankF s le_rfl) (chernF s) 2 α
+ (r.choose 2 : ℤ) • firstChernCapSum C p n N hfacN 1
(chernClassCapExt C p n (F s) s (hrankF s le_rfl) (chernF s) 1 α)
+ ((r : ℤ) * s - 1) • firstChernCapSum C p n L hfacL 1
(chernClassCapExt C p n (F s) s (hrankF s le_rfl) (chernF s) 1 α)
+ (s.choose 2 : ℤ) • firstChernCapSum C p n L hfacL 1
(chernClassCapExt C p n (E r) r (hrankE r le_rfl) (chernE r) 1 α)
Stacks.Chow.chernClass_tensorObj_one_chowCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/TensorChernClassesBivariant.lean, line 308. The attribute's comment: “the first displayed identity c_1(E tensor F) = r c_1(F) + s c_1(E), in the Chow cohomology ring A^(X) of Stacks 0B7E at the bivariant Chern classes of Stacks 0B7H, for X locally of finite type over the base and E, F finite locally free of ranks r and s; nothing else is assumed. The tensor product is AlgebraicGeometry.Scheme.Modules.tensorObj, of rank rs by Stacks 02U9. The same identity in the ring of total classes prod_p A^p(X) is Stacks.Chow.totalChern_tensorObj_homComponent_one”.
Stacks 0FA6, the first displayed identity. Let
Xbe locally of finite type over the base andℰ,ℱfinite locally free𝒪_X-modules of ranksrands. Then
c₁(ℰ ⊗ ℱ) = r c₁(ℱ) + s c₁(ℰ)in the Chow cohomology ring
A^*(X)of Stacks 0B7E,c₁being the bivariant Chern class of Stacks 0B7H.
theorem chernClass_tensorObj_one_chowCohomology (E F : X.Modules) (r s : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F s] :
chernClassChowCohomology C sX (Scheme.Modules.tensorObj E F) (r * s) 1
= r • chernClassChowCohomology C sX F s 1 + s • chernClassChowCohomology C sX E r 1
Stacks.Chow.chernClass_tensorObj_two_chowCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/TensorChernClassesBivariant.lean, line 334. The attribute's comment: “the second displayed identity c_2(E tensor F) = r c_2(F) + s c_2(E) + binom(r,2) c_1(F)^2 + (rs - 1) c_1(F) c_1(E) + binom(s,2) c_1(E)^2, in the Chow cohomology ring A^(X) of Stacks 0B7E at the bivariant Chern classes of Stacks 0B7H, the products being the multiplication of A^(X), for X locally of finite type over the base and E, F finite locally free of ranks r and s; nothing else is assumed. The coefficient rs - 1 is an integer. The tensor product is AlgebraicGeometry.Scheme.Modules.tensorObj, of rank r*s by Stacks 02U9. The same identity in the ring of total classes prod_p A^p(X) is Stacks.Chow.totalChern_tensorObj_homComponent_two”.
Stacks 0FA6, the second displayed identity. Let
Xbe locally of finite type over the base andℰ,ℱfinite locally free𝒪_X-modules of ranksrands. Then
c₂(ℰ ⊗ ℱ) = r c₂(ℱ) + s c₂(ℰ) + C(r,2) c₁(ℱ)² + (rs − 1) c₁(ℱ) c₁(ℰ) + C(s,2) c₁(ℰ)²in the Chow cohomology ring
A^*(X)of Stacks 0B7E,c_ibeing the bivariant Chern classes of Stacks 0B7H and the products those of the ringA^*(X).
theorem chernClass_tensorObj_two_chowCohomology (E F : X.Modules) (r s : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F s] :
letI := chowCohomologyRingOfInvertible C sX
chernClassChowCohomology C sX (Scheme.Modules.tensorObj E F) (r * s) 2
= r • chernClassChowCohomology C sX F s 2 + s • chernClassChowCohomology C sX E r 2
+ r.choose 2 • chernClassChowCohomology C sX F s 1 ^ 2
+ ((r * s : ℤ) - 1) •
(chernClassChowCohomology C sX F s 1 * chernClassChowCohomology C sX E r 1)
+ s.choose 2 • chernClassChowCohomology C sX E r 1 ^ 2
Stacks.Chow.chernClassSub_tensorObj_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/TensorChernClassesTotal.lean, line 330. The attribute's comment: “the first displayed identity, with nothing assumed beyond the two ranks. CORRECTION OF FORM: the source states c_1(E tensor F) = r c_1(F) + s c_1(E) in the bivariant ring A^*(X). Here the identity is stated in Stacks.Chow.chernSubring, the commutative ring generated by the Chern classes inside the ring of graded cap families, in which Stacks.Chow.chernClassSub C sX E r i is c_i(E); it is the same identity read in that realisation, and both sides are elements of one commutative ring, so the coefficients r and s are ring elements and not scalar actions. The module on the left is the library's canonical tensor product AlgebraicGeometry.Scheme.Modules.tensorObj. The source's reduction to the filtered case is PERFORMED, not assumed: Stacks 02UL is Stacks.Chow.exists_splittingMorphism_unconditional, proved from the flag bundle of StacksFrontier.AlgebraicGeometry.Chow.SplittingPrinciple.FlagBundle; the Chern roots of the three modules on the bundle are Stacks.Chow.hasChernRoots_of_hasQuotients and Stacks.Chow.hasChernRoots_tensorObj_of_hasQuotients, which get their filtrations from Stacks.Chow.exists_hasQuotients_of_hasInvertibleFiltration; and the descent along the flat pullback, injective by clause (1) of Stacks 02UL, is Stacks.Chow.eq_of_intertwines, fed by Stacks 02U8 in the form Stacks.Chow.GenuineChern.intertwines_chernFamily. The formal computation the source omits is proved in full, for every r and every s, as Stacks.Chow.esymmOfRoots_lex_one, via the bridge Stacks.Chow.esymmOfRoots_eq_esymRec from the unordered families of AlgebraicGeometry.HasChernRoots to the Pascal recursion Stacks.Chow.esymRec. Stacks 02TJ is not needed in degree one: Stacks.Chow.sum_range_lexFamily is proved for an arbitrary ring”.
Stacks 0FA6, the first displayed identity. For
ℰandℱfinite locally free of constant ranksrands,
c₁(ℰ ⊗_{𝒪_X} ℱ) = r·c₁(ℱ) + s·c₁(ℰ)in the commutative ring
Stacks.Chow.chernSubringgenerated by the Chern classes. Nothing is assumed beyond the two ranks: the source's reduction to a pair of filtrations with invertible quotients is performed, by the flag bundle of Stacks 02UL and the injectivity of the flat pullback it provides.
theorem chernClassSub_tensorObj_one (E F : X.Modules) (r s : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F s] :
chernClassSub C sX (Scheme.Modules.tensorObj E F) (r * s) 1
= (s : chernSubring C sX) * chernClassSub C sX E r 1
+ (r : chernSubring C sX) * chernClassSub C sX F s 1
Stacks.Chow.chernClassSub_tensorObj_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/TensorChernClassesTotal.lean, line 436. The attribute's comment: “the second displayed identity, with nothing assumed beyond the two ranks. CORRECTION OF FORM: the source states c_2(E tensor F) = r c_2(F) + s c_2(E) + binom(r,2) c_1(F)^2 + (rs - 1) c_1(F) c_1(E) + binom(s,2) c_1(E)^2 in the bivariant ring A^(X). Here the identity is stated in Stacks.Chow.chernSubring, the commutative ring generated by the Chern classes inside the ring of graded cap families, in which Stacks.Chow.chernClassSub C sX E r i is c_i(E); it is the same identity read in that realisation, and because that ring is commutative the two squares and the cross term are honest products of classes rather than composites of operations. The cross-term coefficient is rs - 1, as in the source, and NOT rs; the five summands appear in a different order from the source's, and addition is commutative. The module on the left is the library's canonical tensor product AlgebraicGeometry.Scheme.Modules.tensorObj. The source's reduction to the filtered case is PERFORMED, not assumed, by exactly the route recorded on Stacks.Chow.chernClassSub_tensorObj_one: the flag bundle of Stacks 02UL as Stacks.Chow.exists_splittingMorphism_unconditional, the Chern roots on the bundle as Stacks.Chow.hasChernRoots_tensorObj_of_hasQuotients, and the descent along the injective flat pullback as Stacks.Chow.eq_of_intertwines fed by Stacks 02U8. Stacks 02TJ, the commutativity the degree-two collapse needs -- the cancellation turning the block-dependent coefficient s(i+1) - 1 into the constant rs - 1 -- comes from the ring Stacks.Chow.chernSubring being commutative, which is Stacks.Chow.isMulCommutative_chernSubring, and is not an input here. The formal computation the source omits is proved in full, for every r and every s, as Stacks.Chow.esymmOfRoots_lex_two, which reads Stacks.Chow.esymRec_two_tensor through the bridge Stacks.Chow.esymmOfRoots_eq_esymRec”.
Stacks 0FA6, the second displayed identity. For
ℰandℱfinite locally free of constant ranksrands,
c₂(ℰ ⊗\_\{𝒪\_X} ℱ) = r·c₂(ℱ) + s·c₂(ℰ) + C(r,2)·c₁(ℱ)² + (r·s − 1)·c₁(ℰ)·c₁(ℱ) + C(s,2)·c₁(ℰ)²in the commutative ring
Stacks.Chow.chernSubringgenerated by the Chern classes, the squares and the cross term being honest products there. The cross-term coefficient isr·s − 1. Nothing is assumed beyond the two ranks.
theorem chernClassSub_tensorObj_two (E F : X.Modules) (r s : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r]
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F s] :
chernClassSub C sX (Scheme.Modules.tensorObj E F) (r * s) 2
= (s : chernSubring C sX) * chernClassSub C sX E r 2
+ (r : chernSubring C sX) * chernClassSub C sX F s 2
+ (r.choose 2 : chernSubring C sX) * chernClassSub C sX F s 1 ^ 2
+ ((r : chernSubring C sX) * s - 1) *
(chernClassSub C sX E r 1 * chernClassSub C sX F s 1)
+ (s.choose 2 : chernSubring C sX) * chernClassSub C sX E r 1 ^ 2
Stacks.Chow.totalChern_sheafTensor_degree_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/TensorChernRelations.lean, line 727. The attribute's comment: “the first displayed identity, for every X locally of finite type over S and all finite locally free E and F of ranks r and s, with no further hypothesis. The identity is read in the ring TotalChowClass C sX of total Chow cohomology classes, the product over p of the A^p(X) of Stacks 0B7E with the product of Stacks 0B75; every term of the identity is homogeneous, so it lies in the source's A^*(X). c_1(E) is the degree-one part TotalChowClass.homComponent 1 (totalChern C sX E r) of the total Chern class, the bivariant Chern class of Stacks 0B7H in degree one, and E tensor F is the sheaf tensor product Stacks.SheafOfModules.Tensor.sheafTensor, of rank r * s”.
Stacks 0FA6, the first displayed identity. For
ℰandℱfinite locally free of ranksrandsonXlocally of finite type overS,
c₁(ℰ ⊗ ℱ) = r·c₁(ℱ) + s·c₁(ℰ)in the ring of total Chow cohomology classes of
X, wherec₁(-)is the degree-one part of the total Chern class, the first Chern class of Stacks 0B7H.
theorem totalChern_sheafTensor_degree_one :
letI : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
(R := X.ringCatSheaf) _ _ :=
isFiniteLocallyFreeOfRank_tensor hE hF
TotalChowClass.homComponent 1 (totalChern C sX (((sheafTensor X.sheaf).obj E).obj F) (r * s)) =
(r : ℤ) • TotalChowClass.homComponent 1 (totalChern C sX F s) +
(s : ℤ) • TotalChowClass.homComponent 1 (totalChern C sX E r)
Stacks.Chow.totalChern_sheafTensor_degree_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/TensorChernRelations.lean, line 753. The attribute's comment: “the second displayed identity, for every X locally of finite type over S and all finite locally free E and F of ranks r and s, with no further hypothesis, the cross-term coefficient being rs - 1 as in the source. The identity is read in the ring TotalChowClass C sX of total Chow cohomology classes, the product over p of the A^p(X) of Stacks 0B7E with the product of Stacks 0B75; every term of the identity is homogeneous, so it lies in the source's A^(X). c_i(E) is the degree-i part TotalChowClass.homComponent i (totalChern C sX E r) of the total Chern class, the bivariant Chern class of Stacks 0B7H in degree i, the squares and the product are products in that ring, and E tensor F is the sheaf tensor product Stacks.SheafOfModules.Tensor.sheafTensor, of rank r * s”.
Stacks 0FA6, the second displayed identity. For
ℰandℱfinite locally free of ranksrandsonXlocally of finite type overS,
c₂(ℰ ⊗ ℱ) = r·c₂(ℱ) + s·c₂(ℰ) + C(r,2)·c₁(ℱ)² + (r·s − 1)·c₁(ℱ)·c₁(ℰ) + C(s,2)·c₁(ℰ)²in the ring of total Chow cohomology classes of
X, wherec_i(-)is the degree-ipart of the total Chern class, the Chern class of Stacks 0B7H. The coefficient of the cross term isr·s − 1.
theorem totalChern_sheafTensor_degree_two :
letI : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
(R := X.ringCatSheaf) _ _ :=
isFiniteLocallyFreeOfRank_tensor hE hF
TotalChowClass.homComponent 2 (totalChern C sX (((sheafTensor X.sheaf).obj E).obj F) (r * s)) =
(r : ℤ) • TotalChowClass.homComponent 2 (totalChern C sX F s) +
(s : ℤ) • TotalChowClass.homComponent 2 (totalChern C sX E r) +
(r.choose 2 : ℤ) • TotalChowClass.homComponent 1 (totalChern C sX F s) ^ 2 +
((r : ℤ) * s - 1) • (TotalChowClass.homComponent 1 (totalChern C sX F s) *
TotalChowClass.homComponent 1 (totalChern C sX E r)) +
(s.choose 2 : ℤ) • TotalChowClass.homComponent 1 (totalChern C sX E r) ^ 2
Tag 0FA7, a remark
Tag 0FA7 in the Stacks Project.
Stacks.Chow.chernPolynomialClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/ChernPolynomial.lean, line 446. The attribute's comment: “the class P(E) = P(r(E), c_1(E), c_2(E), ...) for P in Z[r, c_1, c_2, ...] and E finite locally free of rank not necessarily constant, at the rank and Chern classes of Tag 0ESW; it lies in A^p(X) for P homogeneous of degree p by Stacks.Chow.chernPolynomialClass_isHomogeneous”.
Stacks 0FA7, the class
P(ℰ). Forℰfinite locally free onX, of rank not necessarily constant, andP ∈ 𝐙[r, c₁, c₂, c₃, …],
P(ℰ) = P(r(ℰ), c₁(ℰ), c₂(ℰ), c₃(ℰ), …),the evaluation of
Pat the rankr(ℰ)and the Chern classesc_i(ℰ)of Stacks 0ESW in the ring∏_{q ≥ 0} A^q(X)of total classes. These classes commute pairwise (Stacks.Chow.commute_chernVariable), so the evaluation is a ring homomorphism; forPhomogeneous of degreepthe class lies inA^p(X)(Stacks.Chow.chernPolynomialClass_isHomogeneous).
def chernPolynomialClass : ChernPolynomial →+* TotalChowClass C sX
Stacks.Chow.chernPolynomialClass_isHomogeneous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/ChernPolynomial.lean, line 468. The attribute's comment: “P(E) lies in A^p(X) for P homogeneous of degree p in the graded ring Z[r, c_1, c_2, ...] (r of degree 0, c_i of degree i), for every finite locally free E of rank not necessarily constant”.
Stacks 0FA7,
P(ℰ) ∈ A^p(X). ForP ∈ 𝐙[r, c₁, c₂, …]homogeneous of degreepfor the grading in whichrhas degree0andc_ihas degreei, the classP(ℰ)is homogeneous of degreep: all its components outsideA^p(X)vanish.
theorem chernPolynomialClass_isHomogeneous {p : ℕ} {P : ChernPolynomial}
(hP : P ∈ ChernPolynomial.homogeneousSubmodule p) :
(chernPolynomialClass C sX E P).IsHomogeneous p
Stacks.Chow.res_chernPolynomialClass_of_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/ChernPolynomial.lean, line 519. The attribute's comment: “relations among the P(E) may be proved locally on X: along a morphism over which E has constant rank s, P(E) restricts to P(s, c_1, c_2, ...) of the pullback, at the Chern classes of Tag 0B7H”.
Stacks 0FA7, working locally on
X. Along a morphismh : Y' ⟶ Xover whichh^*ℰhas constant ranks— for instance the inclusion of a piece where the rank ofℰiss— the classP(ℰ)restricts toPevaluated at the integersand the Chern classes of Stacks 0B7H of the moduleh^*ℰof ranks. Relations among the classesP(ℰ)may therefore be checked on the pieces of constant rank, as the remark says.
theorem res_chernPolynomialClass_of_rank {Y' : Scheme.{u}} {sY' : Y' ⟶ C.S}
[LocallyOfFiniteType sY'] (h : Y' ⟶ X) [LocallyOfFiniteType h] (hs : h ≫ sX = sY') (s : ℕ)
[AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
((Scheme.Modules.pullback h).obj E) s] (P : ChernPolynomial) :
TotalChowClass.res h hs (chernPolynomialClass C sX E P) =
chernPolynomialClassOfRank C sY' ((Scheme.Modules.pullback h).obj E) s P
Stacks.Chow.homComponent_totalChernClassOfModule_dualSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/NonconstantRankRelations.lean, line 238. The attribute's comment: “the identity of Tag 0FA5 for modules of nonconstant rank: c_i(E^dual) = (-1)^i c_i(E), at the Chern classes of Tag 0ESW, read in the ring of total classes; the same identity in A^i(X) is Stacks.Chow.SectionZeroScheme.chernClassOfLocallyFree_dualSheaf”.
Stacks 0FA5 in nonconstant rank, in the ring of total classes:
c_i(ℰ^∨) = (-1)^i c_i(ℰ)for the Chern classes of Stacks 0ESW. This isStacks.Chow.SectionZeroScheme.chernClassOfLocallyFree_dualSheaf.
theorem homComponent_totalChernClassOfModule_dualSheaf (i : ℕ) :
haveI := isFiniteLocallyFree_dualSheaf E hE
TotalChowClass.homComponent i (totalChernClassOfModule C sX (dualSheaf E)) =
((-1 : ℤ) ^ i) • TotalChowClass.homComponent i (totalChernClassOfModule C sX E)
Stacks.Chow.chernClassOfLocallyFree_sheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/NonconstantRankRelations.lean, line 342. The attribute's comment: “the example c_2(SheafHom(E, E)) = P(E) with P = 2 r c_2 - (r - 1) c_1^2, in A^2(X), for E finite locally free of rank not necessarily constant, at the Chern classes of Tag 0ESW”.
The example of Stacks 0FA7: for
ℰfinite locally free onX, of rank not necessarily constant,
c₂(𝓗om(ℰ, ℰ)) = P(ℰ),P = 2 r c₂ - (r - 1) c₁²,in
A^2(X), wherec₂is the Chern class of Stacks 0ESW andP(ℰ)the class of Stacks 0FA7. The proof is the source's:𝓗om(ℰ, ℰ) ≅ ℰ ⊗ ℰ^∨(Stacks 0FNV), and Stacks 0FA5 and 0FA6 on the parts ofXwhere the rank ofℰis constant.
theorem chernClassOfLocallyFree_sheafHom :
haveI := isFiniteLocallyFree_sheafHom E
SectionZeroScheme.chernClassOfLocallyFree
(Stacks.SheafOfModules.OnSpace.sheafHom X.toRingedSpace E E) C sX 2 =
chernPolynomialComponent C sX E 2 sheafEndChernPolynomial
Stacks.Chow.chernClassOfLocallyFree_tensorObj_one_chowCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/NonconstantRankRelations.lean, line 437. The attribute's comment: “the first identity of Tag 0FA6 for modules of nonconstant rank, in the Chow cohomology ring A^*(X): c_1(E tensor F) = r(E) c_1(F) + r(F) c_1(E), at the rank and Chern classes of Tag 0ESW”.
Stacks 0FA6, the first identity, in nonconstant rank, in
A^*(X)(Stacks 0FA7). Forℰ,ℱfinite locally free onX, of ranks not necessarily constant,
c₁(ℰ ⊗ ℱ) = r(ℰ) c₁(ℱ) + r(ℱ) c₁(ℰ)in the Chow cohomology ring
A^*(X)of Stacks 0B7E, at the rank classes and Chern classes of Stacks 0ESW.
theorem chernClassOfLocallyFree_tensorObj_one_chowCohomology :
letI := chowCohomologyRingOfInvertible C sX
chernClassOfLocallyFreeChowCohomology C sX (Scheme.Modules.tensorObj E F) 1 =
rankChowCohomology C sX E * chernClassOfLocallyFreeChowCohomology C sX F 1 +
rankChowCohomology C sX F * chernClassOfLocallyFreeChowCohomology C sX E 1
Stacks.Chow.chernClassOfLocallyFree_tensorObj_two_chowCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/NonconstantRankRelations.lean, line 468. The attribute's comment: “the second identity of Tag 0FA6 for modules of nonconstant rank, in the Chow cohomology ring A^*(X): c_2(E tensor F) = r(E) c_2(F) + r(F) c_2(E) + binom(r(E),2) c_1(F)^2 + (r(E) r(F) - 1) c_1(F) c_1(E) + binom(r(F),2) c_1(E)^2, at the rank and Chern classes of Tag 0ESW, binom(r(E),2) being the class which is binom(r,2) where the rank is r”.
Stacks 0FA6, the second identity, in nonconstant rank, in
A^*(X)(Stacks 0FA7). Forℰ,ℱfinite locally free onX, of ranks not necessarily constant,
c₂(ℰ ⊗ ℱ) = r(ℰ) c₂(ℱ) + r(ℱ) c₂(ℰ) + (r(ℰ) choose 2) c₁(ℱ)² + (r(ℰ) r(ℱ) - 1) c₁(ℱ) c₁(ℰ) + (r(ℱ) choose 2) c₁(ℰ)²in the Chow cohomology ring
A^*(X)of Stacks 0B7E, at the rank classes and Chern classes of Stacks 0ESW,(r(ℰ) choose 2)being the class which is(r choose 2)where the rank isr.
theorem chernClassOfLocallyFree_tensorObj_two_chowCohomology :
letI := chowCohomologyRingOfInvertible C sX
chernClassOfLocallyFreeChowCohomology C sX (Scheme.Modules.tensorObj E F) 2 =
rankChowCohomology C sX E * chernClassOfLocallyFreeChowCohomology C sX F 2 +
rankChowCohomology C sX F * chernClassOfLocallyFreeChowCohomology C sX E 2 +
rankChooseTwoChowCohomology C sX E * chernClassOfLocallyFreeChowCohomology C sX F 1 ^ 2 +
(rankChowCohomology C sX E * rankChowCohomology C sX F - 1) *
(chernClassOfLocallyFreeChowCohomology C sX F 1 *
chernClassOfLocallyFreeChowCohomology C sX E 1) +
rankChooseTwoChowCohomology C sX F *
chernClassOfLocallyFreeChowCohomology C sX E 1 ^ 2
Stacks.AlgebraicGeometry.ReflexiveModules.isFiniteLocallyFree_dualSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/DualFiniteLocallyFree.lean, line 92. The attribute's comment: “dual_nonconstant_rank”.
Stacks Project, Tag 0FA7, the clause on the dual. The dual
ℰ^∨ = SheafHom(ℰ, 𝒪_X)of a finite locally free module on a scheme is finite locally free. The rank ofℰis not assumed constant.Every point has a neighbourhood
Uon which a local free presentation ofℰtrivialises it on a finite index set, and thereℰ^∨is free on the same index set byfreeIsoDualSheafOver.
theorem isFiniteLocallyFree_dualSheaf {X : Scheme.{u}} (E : X.Modules)
(hE : SheafOfModules.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E) :
SheafOfModules.IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) (dualSheaf E)
Tag 0F9B, an example
Tag 0F9B in the Stacks Project.
AlgebraicGeometry.degreeZeroPowerSum, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/ChernGrading.lean, line 69. The attribute's comment: “degree_zero_power_sum”.
The zeroth power-sum polynomial is the rank variable
r.
noncomputable abbrev degreeZeroPowerSum : ChernPolynomial
AlgebraicGeometry.coe_powerSumPolynomial_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/FirstFourPowerSums.lean, line 38. The attribute's comment: “first_four_power_sums”.
The first power-sum polynomial is
c₁.
theorem coe_powerSumPolynomial_one :
(powerSumPolynomial 1 : MvPolynomial ℕ+ ℤ) = X (1 : ℕ+)
AlgebraicGeometry.coe_powerSumPolynomial_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/FirstFourPowerSums.lean, line 44. The attribute's comment: “first_four_power_sums”.
The second power-sum polynomial is
c₁² - 2c₂.
theorem coe_powerSumPolynomial_two :
(powerSumPolynomial 2 : MvPolynomial ℕ+ ℤ) =
X (1 : ℕ+) ^ 2 - 2 * X (2 : ℕ+)
AlgebraicGeometry.coe_powerSumPolynomial_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/FirstFourPowerSums.lean, line 52. The attribute's comment: “first_four_power_sums”.
The third power-sum polynomial is
c₁³ - 3c₁c₂ + 3c₃.
theorem coe_powerSumPolynomial_three :
(powerSumPolynomial 3 : MvPolynomial ℕ+ ℤ) =
X (1 : ℕ+) ^ 3 - 3 * X (1 : ℕ+) * X (2 : ℕ+) + 3 * X (3 : ℕ+)
AlgebraicGeometry.coe_powerSumPolynomial_four, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/FirstFourPowerSums.lean, line 60. The attribute's comment: “first_four_power_sums”.
The fourth power-sum polynomial is
c₁⁴ - 4c₁²c₂ + 4c₁c₃ + 2c₂² - 4c₄.
theorem coe_powerSumPolynomial_four :
(powerSumPolynomial 4 : MvPolynomial ℕ+ ℤ) =
X (1 : ℕ+) ^ 4 - 4 * X (1 : ℕ+) ^ 2 * X (2 : ℕ+) +
4 * X (1 : ℕ+) * X (3 : ℕ+) + 2 * X (2 : ℕ+) ^ 2 - 4 * X (4 : ℕ+)
AlgebraicGeometry.log_one_add_universalChernClassSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/LogarithmicIdentity.lean, line 592. The attribute's comment: “logarithmic_identity”.
In the completed rational graded ring, the logarithm of the universal total Chern class is the signed generating series of the universal power-sum polynomials.
public theorem log_one_add_universalChernClassSum :
PowerSeries.subst universalChernClassSum (PowerSeries.log ℚ) = powerSumSeries
AlgebraicGeometry.eq_powerSumPolynomial_iff_eval_esymm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/PowerSumCharacterization.lean, line 127. The attribute's comment: “power_sum_characterization”.
A weighted-homogeneous integral polynomial of positive degree
pis the universal power-sum polynomial precisely when substituting elementary symmetric polynomials in anyn ≥ pvariables gives the sum of theirpth powers.
public theorem eq_powerSumPolynomial_iff_eval_esymm
(p : ℕ) (hp : 1 ≤ p)
(Q : weightedHomogeneousSubmodule ℤ (fun i : ℕ+ => (i : ℕ)) p) :
Q = powerSumPolynomial p ↔
∀ n : ℕ, p ≤ n →
eval₂Hom C (fun i : ℕ+ => esymm (Fin n) ℤ (i : ℕ))
(Q : MvPolynomial ℕ+ ℤ) =
psum (Fin n) ℤ p
AlgebraicGeometry.powerSumPolynomial, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/PowerSumPolynomials.lean, line 58. The attribute's comment: “power_sum_polynomials”.
The universal power-sum polynomial
Pₚin the Chern-class variablescᵢ.The variable indexed by
i : ℕ+has weighti. Thus the value is packaged as a weighted-homogeneous polynomial of degreep. Forp + 1, the displayed recursion is Newton's formulaPₚ₊₁ = ∑ᵢ₌₁ᵖ (-1)ⁱ⁻¹ cᵢ Pₚ₊₁₋ᵢ + (-1)ᵖ (p + 1) cₚ₊₁.
noncomputable def powerSumPolynomial (p : ℕ) :
weightedHomogeneousSubmodule ℤ (fun i : ℕ+ => (i : ℕ)) p
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.