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, let f : X ⟶ Y be a morphism of schemes locally of finite type over S and let p ∈ ℤ. A rule assigning to every locally of finite type g : Y' ⟶ Y and every k a 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 of Y' ×_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, let f : X ⟶ Y be a morphism of schemes locally of finite type over S and let p ∈ ℤ. A rule assigning to every morphism Y' ⟶ Y locally of finite type and every k a map c ∩ - : A_k(Y') ⟶ A_{k-p}(Y' ×_Y X), satisfying conditions (1) and (2) of Stacks 0B76 and condition (3) whenever ℒ'|_{D'} ≅ 𝒪_{D'} — a Stacks.Chow.WeakCapRule read against the canonical Gysin system — is a bivariant class: an element of A^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 over Y vanishes.

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 by c, 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 over Y exactly 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: c is zero; c ∩ [Y'] = 0 for every integral scheme Y' locally of finite type over Y; and every such Y' admits a proper birational Y'' ⟶ Y' with c ∩ [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 Y vanishes.

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 Y exactly 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: c is zero; c ∩ [Y'] = 0 for every integral scheme Y' locally of finite type over Y; and every such Y' admits a proper birational Y'' ⟶ Y' with c ∩ [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 degree p for the restrictions f_i : X_i ⟶ Y_{a(i)}: on a test scheme g : T ⟶ Y it sends α ∈ A_k(T) to the unique class in A_{k-p}(X ×_Y T) whose restriction to the i-th piece X_i ×_{Y_{a(i)}} T_{a(i)} is c_i ∩ α|_{T_{a(i)}}.

It is well defined because the Chow groups of X ×_Y T decompose along those pieces, by Stacks.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_i of a bivariant class c of degree p for f : X ⟶ Y to the piece f_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.bivariantPieceRestriction with its Gysin compatibility discharged by Stacks.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 degree p for f : X ⟶ Y is the same thing as a family of bivariant classes of degree p for the restrictions f_i : X_i ⟶ Y_{a(i)}.

This is Stacks.Chow.bivariantPieceEquiv with all three of its Gysin compatibilities discharged, by Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpenImmersion, Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpensRestriction and Stacks.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 class c of degree p for f : X ⟶ Y to the piece f_i : X_i ⟶ Y_{a(i)}: on a test scheme g : T ⟶ Y_{a(i)} it is the cap operation of c at g ≫ (Y_{a(i)} ⟶ Y), restricted along the open immersion X_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 p for f : X ⟶ Y are equal as soon as, for every test scheme g : T ⟶ Y and every k, their cap operations agree after restriction to each piece X_i ×_Y T of X ×_Y T.

The pieces of X ×_Y T are the preimages of the pieces of X under the projection, a decomposition into open and closed subschemes by Stacks.Chow.IsClopenDecomposition.preimage, so restriction to them is jointly injective on CH_{k-p}(X ×_Y T) by Stacks.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 b followed by cap with a, 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 morphism f : X ⟶ Y of schemes locally of finite type over the base: the product, over the connected components X_i of X, of the graded groups A^*(X_i ⟶ Y_{a(i)}) of bivariant classes for the restriction of f to X_i and the connected component of Y it 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 component X_i of X it is the restriction of 1 ∈ A^0(X) to X_i, placed in degree 0. By Stacks.Chow.completedIdentityClass_apply_heq that restriction is 1 ∈ 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 tuples c = (c_0, c_1, c_2, …) such that for every connected component X_i of X the image of c_p in A^p(X_i ⟶ Y_{a(i)}) vanishes for almost all p — at the Gysin system of the first Chern class rule of an invertible module.

This is Stacks.Chow.completedBivariantSubgroup with the Gysin compatibility it carries discharged, by Stacks.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_completedBivariantSequence with the three Gysin compatibilities of Stacks 0FDZ discharged, by Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpenImmersion, Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpensRestriction and Stacks.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.completedBivariantGroupEquiv with the three Gysin compatibilities of Stacks 0FDZ discharged, by Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpenImmersion, Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderOpensRestriction and Stacks.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.completedBivariantComposite with both Gysin compatibilities of Stacks 0B75 discharged, by Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderBaseChangeIso and Stacks.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 c is concentrated in degree p on the component X_i and d is concentrated in degree q on the component Y_{a(i)}, then the composite is concentrated in degree p + q on X_i and is there the composite bivariant class Stacks.Chow.bivariantCompositeOfInvertible of 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 scheme X locally of finite type over the base: the completed bivariant group of the identity of X. Its multiplication is Stacks.Chow.completedBivariantComposite at f = g = 𝟙 X, and Stacks.Chow.completedBivariantGroupEquiv reads it as the group of tuples in ∏_p A^p(X) that vanish in almost all degrees on each connected component of X.

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 ⟶ Y be a morphism of schemes locally of finite type over the base of chapter 42, let g : Y' ⟶ Y be an envelope and write X' = X ×_Y Y'. Let c' ∈ A^p(X' ⟶ Y'). If the two restrictions res₁(c') = res₂(c') in A^p(X' ×_X X' ⟶ Y' ×_Y Y') agree, then there is a unique c ∈ A^p(X ⟶ Y) whose restriction res(c) along g is c'.

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 ∩ π^*α) = 0 in A_{k+(r-1)-s}(X),

for L the twist O_P(1) of the projective bundle. Nothing is assumed beyond the geometry of the bundle: π is flat, proper and of relative dimension r - 1 over the base, which for the projective bundle of a finite locally free module of rank r is Stacks 02TX (Stacks.RelativeProj.isProper_projectiveBundleToBase, Stacks.RelativeProj.locallyOfFiniteType_projectiveBundleToBase and Stacks.SymGraded.relativeDimension_freeProjectiveBundleToBase), and L is an invertible module on P, 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 with c₁(L) are Stacks.Chow.invertibleChernCap, and Stacks 02S2 for the pushforward is Stacks.Chow.properPushforwardFactorsThroughRationalEquivalence_of_isProper. The vanishing itself is the dimension count of Stacks.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 ⟶ X of a module of rank n + 1, α ∈ A_k(X) and s ≤ n, the class π_*(c₁(𝒪_P(1))^s ∩ π^*α) ∈ A_{k+n-s}(X) is 0 if s < n and is α if s = 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 X be locally of finite type over the base S of chapter 42, ℰ a finite locally free 𝒪_X-module of rank r and (π : 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 every k.

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 X be locally of finite type over the base of chapter 42, let ℰ be a finite locally free sheaf of rank zero on X and let p : E = Spec_X(Sym(ℰ)) ⟶ X be the associated vector bundle. Then p^* : A_k(X) ⟶ A_k(E) is bijective for every k.

The bundle is the relative spectrum of Sym(ℰ), which is the tag's own object; Stacks.Chow.isAffineSpaceBundle_vectorBundleToBase supplies the local triviality that Stacks.Chow.flatPullbackChow_bijective_of_isAffineSpaceBundle_zero needs, and the flatness, local finite type and relative dimension of p come 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 by Stacks.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, let X be locally of finite type over S, let ℰ be a finite locally free 𝒪_X-module of rank r and let p : E = \underline{\Spec}(\Sym^*(ℰ)) ⟶ X be 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 is Stacks.Chow.flatPullbackChow_injective_vectorBundleToBase. The instance [E.IsQuasicoherent], which the construction of 𝐕(ℰ) takes, restricts nothing: a finite locally free module is quasi-coherent, by Stacks.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 X be locally of finite type over the base of chapter 42, let ℰ be a finite locally free 𝒪_X-module of rank r and let p : Spec_X(Sym(ℰ)) ⟶ X be its vector bundle. Then flat pullback p^* : A_k(X) ⟶ A_{k+r}(Spec_X(Sym(ℰ))) is bijective for every k.

This is Stacks.Chow.flatPullbackChow_bijective_vectorBundleToBase, stated with the flat pullback Stacks.Chow.flatPullbackChow and 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 X be locally of finite type over the base of chapter 42, let ℰ be a finite locally free sheaf of rank 0 on X and let p : E ⟶ X be the associated vector bundle. Then p^* : CH_k(X) ⟶ CH_{k+0}(E) is bijective, which is the assertion of Stacks 02TY for r = 0.

The bundle projection is carried as an affine-space bundle of rank zero, p being Zariski-locally on X the projection 𝔸^0_U ⟶ U; a rank-zero vector bundle projection has that property. Such a p is an isomorphism, so the assertion is Stacks.Chow.flatPullbackChow_bijective_of_isIso. The instance of Stacks 02S1 needed to write the map down is not an extra assumption: it is supplied by Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_of_isIso.

Neither half is proved here for r ≥ 1. The source proof forms the projective space bundle P = P(ℰ ⊕ 𝒪_X) with its tautological invertible sheaf, identifies 𝒪_P(D) = 𝒪_P(1) for the divisor D = Z(s) at infinity by Stacks 01X0, writes E as P ∖ D, and then runs the localization sequence of Stacks 02RX against the projective bundle formula of Stacks 02TX for P and for D.

Of those inputs Stacks 02TR is proved, in both of its equalities and at Chow level for an arbitrary class: Stacks.Chow.gysinChowOfInvertible_flatPullbackChow gives i^* p^* α = (p|_D)^* α and Stacks.Chow.firstChernClassCapChow_flatPullbackChow gives c₁(ℒ) ∩ p^* α = i_*((p|_D)^* α) (StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierFlatPullbackChow.lean:385, 463, with the cycle-level forms at StacksFrontier/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.ProjectiveBundleRelationInjective and Stacks.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 the r ≥ 1 case 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 rank r on X and an integer n, there are classes c_i ∈ A_{n-i}(X), 0 ≤ i ≤ r, with c_0 = [X] and ∑_{i=0}^{r} (-1)^i c₁(𝒪_{𝐏(ℰ)}(1))^i ∩ π^*c_{r-i} = 0, and exactly one such family. Here [X] = [X]_n is the fundamental cycle of Stacks 02QU; the source takes X integral and n = 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 rank r on X, c_i(ℰ) ∩ [X] = c_i ∈ A_{n-i}(X): the i-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 r on X, c(ℰ) ∩ [X] = c_0(ℰ) ∩ [X] + … + c_r(ℰ) ∩ [X] in A_*(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:

  • ProjectiveBundleChernRelation registered with add_to_stacks in 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-r finite locally free module. The tag labels the displayed equation, which is this condition, so it is carried by the definition naming it; Stacks.Chow.IsChernCapFamily conjoins it with c₀ = α.”.
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, let X be locally of finite type over S, integral and of delta-dimension n, and let L be an invertible 𝒪_X-module. Then the first Chern class of L in the sense of Stacks 02U0 — the member c_1 of the family of clause (1), read on the projective bundle of L, which is X itself with projection 𝟙 X and twist L — equals the Weil divisor class of L of Stacks 02SJ (2).

The proof is the source's. At r = 1 the relation 02U1 reads c₁(L) ∩ π^*c_0 = π^*c_1 on the bundle; the bundle is X and π is the identity, so its flat pullback is the identity (Stacks.Chow.flatPullbackChow_id) and the relation says c_1 = c₁(L) ∩ c_0. The normalisation c_0 = [X] turns the right-hand side into the cap product of Stacks 02SO on the fundamental cycle, which is the Weil divisor class by Stacks.Chow.firstChernClassCapOfInvertible_fundamentalCycle_eq_firstChernClassCapFundamental.

The twist operator is Stacks.Chow.invertibleChernCapOperator of L, the source's O_{𝐏(L)}(1) = L, built from Stacks 02TI for L (Stacks.Chow.firstChernClassCap_factors); the family D of 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 X be locally of finite type over the base of a Chow situation, integral of delta-dimension n, and let ℒ be an invertible 𝒪_X-module, so of rank one. The first Chern class c_1(ℒ) ∩ [X] ∈ A_{n-1}(X) of Stacks 02U0, defined by the relation c₁(𝒪_{𝐏(ℒ)}(1)) ∩ π^*c_0 = π^*c_1 with c_0 = [X] on the projective bundle of ℒ, is the Weil divisor class c₁(ℒ) ∩ [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 rank r, 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 ⟶ X of delta-dimension k, c_j(ℰ) ∩ [W] = i_*(c_j(i^*ℰ) ∩ [W]), with the class c_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-dimension k, 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 a k-cycle, presented by a locally finite family of integral closed subschemes i_t : W_t ⟶ X of delta-dimension k, and let γ_t be any cycle on W_t representing c_j(i_t^*ℰ) ∩ [W_t], the class of Stacks 02U0. Then

  1. i_{t,*} γ_t represents c_j(ℰ) ∩ [W_t] for every t;
  2. the locally finite sum ∑ n_t i_{t,*} γ_t is a cycle on X;
  3. every cycle β with these coefficients represents c_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 k determines 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 rank r on X, with projective bundle (π : 𝐏(ℰ) ⟶ X, 𝒪_{𝐏(ℰ)}(1)), and let α be a k-cycle on X. The classes c_j(ℰ) ∩ α ∈ A_{k-j}(X) of Stacks 02U5 satisfy α_0 = [α] and ∑_{i=0}^{r} (-1)^i c₁(𝒪_{𝐏(ℰ)}(1))^i ∩ π^*(α_{r-i}) = 0 in 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 equivalent k-cycles on X, then the Chern class cap products of α and of β agree: c_j(ℰ) ∩ α = c_j(ℰ) ∩ β in A_{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 hfac that 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 through A_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 c is the family of Chern class cap products of α ∈ A_k(X) for p^*ℰ and e is the family of Chern class cap products of p_*α ∈ A_k(Y) for ℰ, then e_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 c satisfies the relation over Y and has p_*α in degree k, so the uniqueness of Stacks 02U6 identifies it with e.

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 ⟶ Y be a proper morphism of schemes locally of finite type over S, ℰ finite locally free of rank r on Y and α a k-cycle on X. Then p_*(c_j(p^*ℰ) ∩ α) = c_j(ℰ) ∩ p_*α in A_{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 hinjX of the projective-bundle relation over X and the compatibility hcompat of its summands with flat pullback. If c is the family of Chern class cap products of α ∈ A_k(Y) for ℰ and e is the family of Chern class cap products of f^*α ∈ A_{k+d}(X) for f^*ℰ, then e_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 ⟶ Y be a flat morphism of relative dimension d between schemes locally of finite type over S, ℰ finite locally free of rank r on Y and α a k-cycle on Y. Then f^*(c_j(ℰ) ∩ α) = c_j(f^*ℰ) ∩ f^*α in A_{k+d-j}(X). The source takes d = 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 ⟶ X flat of relative dimension d over the base, ℰ of rank r on X and ℰ' ≅ f^*ℰ,

c_j(ℰ') ∩ f^*α = f^*(c_j(ℰ) ∩ α),

as a heterogeneous equality: the two sides lie in A_{(k+d)-j}(Y) and A_{(k-j)+d}(Y). The flat pullbacks are those of Stacks.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 rank r on X and let (ℒ, s, i : D ⟶ X) be as in Definition 02T8. Let α ∈ A_{k+1}(X), let a be a cycle representing α and b a cycle representing i^*α ∈ A_k(D). Then for every 0 ≤ j ≤ r

c_j(ℰ|_D) ∩ b = i^*(c_j(ℰ) ∩ a) in A_{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 rank r on Y and let (ℒ, s, i : D ⟶ Y) be a triple as in Definition 02T8. Then for every 0 ≤ j ≤ r and every α ∈ A_{k+1}(Y)

c_j(ℰ|_D) ∩ i^*α = i^*(c_j(ℰ) ∩ α) in A_{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 rank r on X and 0 ≤ j ≤ r, the rule assigning to f : X' ⟶ X the operation c_j(f^*ℰ) ∩ - : A_k(X') ⟶ A_{k-j}(X') is a bivariant class of degree j: the class c_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 rank r on X and 0 ≤ j ≤ r, the rule assigning to f : X' ⟶ X the operation c_j(f^*ℰ) ∩ - : A_k(X') ⟶ A_{k-j}(X') of Stacks 02U5 is a bivariant class of degree j: a class c ∈ A^j(X) with c ∩ [α] = c_j(f^*ℰ) ∩ α for every f : X' ⟶ X and every k-cycle α on X', the cap operation being read on X' through the identification X ×_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. For 0 ≤ i ≤ r, the i-th Chern class c_i(ℰ) ∈ A^i(X) of a module ℰ that is finite locally free of rank r: it is the bivariant class of degree i for 𝟙 X constructed in Stacks 0B7H, namely the rule assigning to f : X' ⟶ X the operation c_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 rank r: the formal sum of the r + 1 Chern classes of Stacks 0B7H, viewed as a nonhomogeneous bivariant class on X, that is, as an element of A^*(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 rank r on X and 0 ≤ i ≤ r, the i-th Chern class c_i(ℰ) ∈ A^i(X): the bivariant class of degree i for 𝟙 X constructed in Stacks 0B7H, which assigns to f : X' ⟶ X the operation c_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 rank r on X, the total Chern class c(ℰ) = c_0(ℰ) + c_1(ℰ) + ⋯ + c_r(ℰ): the formal sum of the r + 1 Chern classes of Stacks 0B7H, viewed as a nonhomogeneous bivariant class on X, that is, as an element of A^*(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 of f^*ℰ: if d is the family of Chern class cap products of α ∈ A_k(T) for ℰ|_T and e is the family of Chern class cap products of c ∩ α ∈ A_{k-p}(T ×_X X') for the pullback of ℰ, then e_j = c ∩ d_j, that is

c_j(f^*ℰ) ∩ (c ∩ α) = c ∩ (c_j(ℰ) ∩ α),

which is the identity c ∘ c_j(ℰ) = c_j(f^*ℰ) ∘ c of the tag, read on the test scheme g.

The proof is the one in the source: the cap product of c with d satisfies the relation downstairs and has c ∩ α in degree k - p, so the uniqueness of Stacks 02U6 identifies it with e.

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(ℰ) ∩ α) in A_{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(ℰ) ∩ α))_i satisfies the relation of Stacks 02U6 over X for the class c_j(ℱ) ∩ α, because capping with c_j(ℱ) carries each summand of the relation to itself, and its zeroth member is c_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' ⟶ X be locally of finite type, let c ∈ A^p(X' ⟶ X) and let ℰ be finite locally free of rank r on X. Then for 0 ≤ j ≤ r

c ∘ c_j(ℰ) = c_j(f^*ℰ) ∘ c in A^{p+j}(X' ⟶ X),

the composites being those of Stacks 0B75, classes for the equal morphisms f ≫ 𝟙 X and 𝟙 X' ≫ f of the equal degrees p + j and j + 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 rank r is in the center of A^*(X): for every c ∈ A^q(X),

c · c_j(ℰ) = c_j(ℰ) · c,

the two products lying in A^{q+j}(X) and A^{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 rank r, let f : X' ⟶ X be locally of finite type and let c ∈ A^p(X' ⟶ X) be a bivariant class. Then

c ∘ c_j(ℰ) = c_j(f^*ℰ) ∘ c in A^{p+j}(X' ⟶ X),

with c_j(ℰ) ∈ A^j(X) and c_j(f^*ℰ) ∈ A^j(X') the bivariant Chern classes of Stacks 0B7H. The left side is a class for f ≫ 𝟙 X of degree p + j; the right side, a class for 𝟙 X' ≫ f of degree j + p, is read as one for f ≫ 𝟙 X of degree p + j along the identity of X'.

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 class c_j(ℰ) ∈ A^j(X) of a locally free 𝒪_X-module of rank r lies in the center of the Chow cohomology ring A^*(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:

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 class c_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 on X_r is c_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-r locus is c_n(E|_{X_r}), and is zero when r < 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-r locus, c_n(E) acts by the already defined operation c_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 scheme X locally of finite type over S and a finite locally free 𝒪_X-module ℰ such that c_p(ℰ) ≠ 0 for infinitely many p.

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 of X by 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 scheme f : X' ⟶ X along which f^*ℰ has constant rank r — for instance the part X'_r of any test scheme lying over X_r — the class c_p(ℰ) acts by the already defined operation c_p(f^*ℰ) ∩ - of Stacks 0B7H, which is zero when p > 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' ⟶ X locally of finite type, with the induced decomposition X' = ∐ X'_r, X'_r = g⁻¹(X_r), the class c_p(ℰ) preserves the decomposition CH_*(X') = ∏_r CH_*(X'_r) and acts on the factor CH_*(X'_r) by the already defined operation c_p(ℰ|_{X'_r}) ∩ - of Stacks 0B7H (zero for p > r): restricting c_p(ℰ) ∩ α to X'_r gives c_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 locus X_r is the Chern class c_p(ℰ|_{X_r}) of Stacks 0B7H (zero when p > r), and it is the only such class: under A^p(X) = ∏_r A^p(X_r) it is the product of the classes c_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 degree p part is the Chern class c_p(ℰ) for p ≥ 0 (and zero for p < 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 to r · 1 on each rank locus X_r, and it is the only class of A^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' ⟶ X along which f^*ℰ has constant rank r — for instance the part X'_r of any test scheme lying over X_r — the class r(ℰ) acts as multiplication by r.

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' ⟶ X locally of finite type, with the induced decomposition X' = ∐ X'_r, the class r(ℰ) sends (α_r) ∈ ∏_r CH_*(X'_r) to (r α_r): restricting r(ℰ) ∩ α to X'_r gives r · (α|_{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 ring A^*(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 of A^*(X): on each rank locus X_r it restricts to r · 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-r factor by multiplication by r.

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-r locus is r times 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-r locus, capping with r(E) is multiplication by r.

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 E on a scheme X is locally constant, the loci X_r where the rank is r are open and closed, pairwise disjoint and cover X, and E is free of rank r on a neighbourhood of every point of X_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 ℰ on X, for the decomposition X = ∐ X_r by the rank of ℰ: the element of the completed bivariant group of Stacks 0FE0 whose image (c_p)_p ∈ ∏_p A^p(X) has, under A^p(X) = ∏_r A^p(X_r) of Stacks 0FDZ, the component c_r(ℰ|_{X_r}) in A^r(X_r) and zero in A^p(X_r) for p ≠ 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_r are nonempty, the top Chern class c_top(ℰ) = Σ_r c_r(ℰ|_{X_r}) ∈ A^*(X) = ⊕ A^*(X_r): the element of the graded group A^*(X) = ⊕_p A^p(X) that is the sum, over the ranks r that occur, of a class of degree r, and whose degree p part has, under A^p(X) = ∏_r A^p(X_r) of Stacks 0FDZ, the component c_r(ℰ|_{X_r}) in A^r(X_r) and zero in A^p(X_r) for p ≠ 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 module E on X, as an element of the completed bivariant group A^*(X)^∧: on a connected component X_i of X the rank of E is a constant r, and there the class is the r-th Chern class c i of E|_{X_i}, placed in degree r.

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 E has rank r the top Chern class is the r-th Chern class, in degree r: a connected component X_i lies in the locus of the rank r of E on it, and the degree-r part of c_top(E) there is c_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 E has rank r, the degree-p part of c_top(E) vanishes for every p ≠ 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_r are nonempty, then only finitely many degrees occur in the top Chern class, so it lies in the ordinary graded group A^*(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 on X, when only finitely many of the loci X_r are nonempty: the sum, over the ranks r that occur, of the degree-r part 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 of c_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 E has rank r, the component of the finite sum Σ_r c_r(E|_{X_r}) in degree r is the r-th Chern class: a connected component X_i lies in the locus of the rank r of E on it, and the degree-r component of the sum there is c_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 which E has rank r, its degree-p component vanishes for every p ≠ 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 module E on X, as an element of ∏_{p ≥ 0} A^p(X): its degree-p component is the class equal, on the locus X_p where E has rank p, to the p-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 module E on X, as an element of the completed bivariant group A^*(X)^∧: on a connected component X_i of X the rank of E is a constant r, and there the class is the restriction to X_i of the degree-r component of c_top(E) — that is, of the r-th Chern class of Stacks 0ESW, by Stacks.Chow.topChernClassOfInvertible_rankStratum — placed in degree r.

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 E has rank r the top Chern class is the r-th Chern class, in degree r: a connected component X_i lies in the locus of the rank r of E on it, and the degree-r part of c_top(E) there is the restriction to X_i of the Chern class c_r(E) of Stacks 0ESW, that is c_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 E has rank r, the degree-p part of c_top(E) vanishes for every p ≠ 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_r are nonempty, then only finitely many degrees occur in the top Chern class, so it lies in the ordinary graded group A^*(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 on X, when only finitely many of the loci X_r are nonempty: the sum, over the ranks r that occur, of the degree-r part 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 of c_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 E has rank r, the component of the finite sum Σ_r c_r(E|_{X_r}) in degree r is the r-th Chern class: a connected component X_i lies in the locus of the rank r of E on it, and the degree-r component of the sum there is the restriction of c_r(E), that is c_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 which E has rank r, its degree-p component vanishes for every p ≠ 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 rank r and ℒ 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 degree i separately, as Stacks.Chow.TotalChowClass.totalChern_sheafTensor_degree states.

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 rank r, let ℒ be invertible and let α be an n-cycle on X. Then for every m ≤ 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 ℰ along c₁(ℒ) ∩ -.

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 X be locally of finite type over the base and let 0 ⟶ 𝒪_X ⟶ ℰ ⟶ ℱ ⟶ 0 be a short exact sequence of 𝒪_X-modules with ℰ, ℱ finite locally free of ranks r, 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, the c_j being 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 ⟶ ℰ ⟶ ℱ ⟶ 0

be a short exact sequence of finite locally free modules on X with ℰ of rank r + 2 and ℱ of rank r + 1. Then for every k and every class α ∈ A_k(X),

c_{r+2}(ℰ) ∩ α = 0 in A_{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: hc and he are 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_general and is not an argument. The projective bundles themselves, their twists O_P(1) and O_Q(1), the closed immersion ι, the injectivity half of Stacks 02TX over P and the summandwise form hcompat of 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 ⟶ ℰ ⟶ ℱ ⟶ 0

be a short exact sequence of finite locally free modules on X with ℰ of rank r + 2 and ℱ of rank r + 1. Then for every k, every class α ∈ A_k(X) and every j ≤ r + 1,

c_j(ℰ) ∩ α = c_j(ℱ) ∩ α in A_{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 at Stacks.Chow.chernCap_top_eq_zero, Stacks 02S1 for the two projections again being supplied from Stacks.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₃ ⟶ 0 of finite locally free modules with S.X₁ invertible, S.X₂ of rank r + 1 and S.X₃ of rank r, and for every n-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 every i ≤ r. Summing over i and expanding c(S.X₁) = 1 + c₁(S.X₁) this is the relation c(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 hbinom is the input: the equality of the binomial transform of the Chern cap products of S.X₂ at r + 1 with that of S.X₃ at r, along c₁ of the inverse of the invertible subsheaf. That equality is what Stacks 02UD gives for the twists of S.X₂ and S.X₃ by S.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 X be locally of finite type over the base and let 0 ⟶ ℒ ⟶ ℰ ⟶ ℱ ⟶ 0 be a short exact sequence of 𝒪_X-modules with ℒ invertible and ℰ, ℱ finite locally free of ranks r, 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₃ ⟶ 0 of finite locally free modules of ranks r₁, r₁ + r₂ and r₂, for every class α ∈ A_k(X) and every m,

c_m(S.X₂) ∩ α = ∑_{i + j = m} c_i(S.X₁) ∩ (c_j(S.X₃) ∩ α) in A_{k-m}(X),

the sum being taken over j ≤ m with i = m - j, and the i-th Chern class read as zero above the rank. Assembling these over m and expanding the product, this is the relation c(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 hbase and hsplit are 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 of S.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 X be locally of finite type over the base and let 0 ⟶ ℰ₁ ⟶ ℰ ⟶ ℰ₂ ⟶ 0 be a short exact sequence of 𝒪_X-modules with ℰ₁, ℰ₂ finite locally free of ranks r₁, r₂; then ℰ is finite locally free of rank r₁ + r₂ (Stacks.Chow.GenuineChern.isFiniteLocallyFreeOfRank_of_shortExact), and the total Chern classes satisfy

c(ℰ) = c(ℰ₁) c(ℰ₂) in A^*(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_r be finite locally free of rank r with a filtration whose successive quotients are the invertible modules L 0, …, L (r-1), presented as the tower of short exact sequences 0 ⟶ L j ⟶ Q_{j+1} ⟶ Q_j ⟶ 0. Then for every n-cycle α and every k ≥ 1

c_k(ℰ) ∩ α = e_k(c₁(L 0), …, c₁(L (r-1))) ∩ ⟦α⟧

in A_{n-k}(X), the k-th elementary symmetric function of the first Chern class cap operations of the quotients applied to the class of α. This is the coefficient of degree k in the product formula c(ℰ) = ∏_i (1 + c₁(ℒ_i)) of the source.

The normalisation hnorm is asked for only at the rank-zero bottom Q_0 of the tower: in degree zero a binomial transform is its own zeroth entry, so hbinom already 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 degrees k ≥ 1, and for the inputs hbinom, chern and hfac.

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 X be locally of finite type over the base, let ℒ_1, …, ℒ_r be 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 rank r (Stacks.Chow.isFiniteLocallyFreeOfRank_of_filtration), and, setting x_i = c_1(ℒ_i),

c(ℰ) = ∏_{i=1}^r (1 + x_i) in A^*(X).

The filtration is indexed by Fin (r + 1) and the invertible modules by Fin r, so that ℒ i is 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 scheme X proper 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 identification A_0(S) = ℤ of Stacks.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 to 1.

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.cycleDegree of 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}), where dim_k Γ(Z_i, 𝒪_{Z_i}) is the degree of Z_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, with c₁(ℰ) ∩ - the operation of Stacks 02U5 at the Chern classes of Stacks 02U0 and deg the 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 is 1, so c₁ = 0, and GenuineChern.firstChernCapOnCycles is 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]_1 is 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 k be a field, let X be a proper scheme over k and let Z ⊆ X be a closed subscheme of dimension d. 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], and deg the degree of zero cycles of [Stacks, Tag 0AZ1], for the Chow groups over Spec k with 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]_n of a scheme whose relative dimension function has a dimension decomposition: the family whose nth coordinate is the class in CH_n(X_n) of the cycle associated to the piece X_n itself.

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, let X be locally of finite type over S and let ℰ_i, i ∈ I finite, be finite locally free 𝒪_X-modules of ranks r_i. There is a flat proper morphism π : P ⟶ X of relative dimension d = ∑_i binom(r_i, 2) such that

  1. the flat pullback π^* : A_k(X) ⟶ A_{k+d}(P) of Stacks 0FVK is injective in every degree, and
  2. each π^*ℰ_i has a filtration of length r_i whose successive quotients are invertible 𝒪_P-modules.

The relative dimension is ∑_i binom(r_i, 2) and not ∑_i (r_i - 1): splitting a rank-r module takes r - 1 layers, of relative dimensions r - 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 ⟶ X with Y locally of finite type over the base there is a flat proper morphism π_Y : P_Y ⟶ Y of the same relative dimension d = ∑_i binom(r_i, 2) along which flat pullback on Chow groups is injective in every degree, and such that each π_Y^* f^* ℰ_i has a filtration of length r_i with invertible successive quotients.

This is the splitting principle run over Y on the modules f^*ℰ_i, whose ranks are the r_i because finite local freeness of given rank is stable under pullback. It does not assert that P_Y is Y ×_X P for the P of Stacks.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 X be locally of finite type over the base S of C and let ℰ_i, i ∈ I finite, be finite locally free 𝒪_X-modules of constant ranks r_i. There is a flat proper morphism π : P ⟶ X of relative dimension d = ∑_i binom(r_i, 2) such that

  1. the flat pullback π^* : A_k(X) ⟶ A_{k+d}(P) is injective in every degree, and
  2. each π^*ℰ_i has a filtration of length r_i whose 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 X be locally of finite type over the base S of C and let ℰ_i, i ∈ I finite, be finite locally free 𝒪_X-modules of constant ranks r_i. There is a single flat proper morphism π : P ⟶ X of relative dimension d = ∑_i binom(r_i, 2) such that

  1. for any f : Y ⟶ X with Y locally 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
  2. each π^*ℰ_i has a filtration of length r_i whose 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, X locally of finite type over S and ℰ_i (i ∈ I, I finite) finite locally free 𝒪_X-modules of ranks r_i. There is a morphism π : P ⟶ X which is

  • projective (Stacks 01W8), flat, and of relative dimension d = ∑_i binom(r_i, 2),

such that

  1. for every morphism f : Y ⟶ X with Y locally of finite type over S, the flat pullback π_Y^* : CH_k(Y) ⟶ CH_{k+d}(Y ×_X P) along the base change of π is injective for every k (Stacks.Chow.UniversallyChowInjective), and
  2. each π^*ℰ_i has 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, X locally of finite type over S and ℰ_i (i ∈ I, I finite) finite locally free 𝒪_X-modules of ranks r_i. There is a morphism π : P ⟶ X which is

  • projective (Stacks 01W8), flat, and of relative dimension d = ∑_i binom(r_i, 2),

such that

  1. for every morphism f : Y ⟶ X with Y locally of finite type over S, the flat pullback π_Y^* : CH_k(Y) ⟶ CH_{k+d}(Y ×_X P) along the base change of π is injective for every k (Stacks.Chow.UniversallyChowInjective), and
  2. each π^*ℰ_i has 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, let X be locally of finite type over S and let ℰ_i, i ∈ I finite, be finite locally free 𝒪_X-modules of ranks r_i. There is a flat proper morphism π : P ⟶ X of relative dimension d = ∑_i binom(r_i, 2), along which flat pullback on Chow groups is injective in every degree, such that

  1. for every morphism f : Y ⟶ X with Y locally of finite type over S the flat pullback π_Y^* : A_k(Y) ⟶ A_{k+d}(Y ×_X P) along the base change π_Y : Y ×_X P ⟶ Y is injective in every degree, and
  2. each π^*ℰ_i has a filtration of length r_i whose successive quotients are invertible 𝒪_P-modules.

The morphism is the iterated projective bundle (Stacks.Chow.BundleStep.ofProjectiveBundle); clause (1) is carried through the iteration as Stacks.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 ⟶ X of 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, let X be locally of finite type over S and let ℰ_i, i ∈ I finite, be finite locally free 𝒪_X-modules of ranks r_i. Then there is a splitting morphism T, flat and proper of relative dimension d = ∑_i binom(r_i, 2), with injective flat pullback on Chow groups in every degree, splitting every ℰ_i, and satisfying Stacks.Chow.IsBundleTower: it is the identity of X or 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, X locally of finite type over S and ℰ_i (i ∈ I, finite) finite locally free 𝒪_X-modules of ranks r_i. The morphism π : P ⟶ X built in the proof of Stacks 02UL — flat and proper of relative dimension d = ∑_i binom(r_i, 2), with injective flat pullback on Chow groups, such that each π^*ℰ_i has a filtration with invertible successive quotients — has the further properties

  1. π 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 bundles Stacks.Chow.bundle), and
  2. there are invertible 𝒪_P-modules L_1, …, L_d such 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 rank r on a scheme X locally of finite type over the base and every 0 ≤ i ≤ r,

c_i(ℰ^∨) = (-1)^i c_i(ℰ)

in A^i(X), the group of bivariant classes of degree i for 𝟙 X of Stacks 0B76, for the Chern classes Stacks.Chow.GenuineChern.chernClass of 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 by c_i(g^*(ℰ^∨)) ∩ - on every test scheme g : T ⟶ X. Integer multiples of bivariant classes are pointwise on cap products, so the left side is (-1)^i (c_i(g^*ℰ) ∩ -), and that is c_i(g^*(ℰ^∨)) ∩ - by Stacks.Chow.GenuineChern.chernCap_dualSheaf applied to g^*ℰ, once the base-change isomorphism of Tag 0GMX identifies g^*(ℰ^∨) 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 scheme X locally of finite type over the base, of rank not necessarily constant, and every i ≥ 0,

c_i(ℰ^∨) = (-1)^i c_i(ℰ)

in A^i(X), for the Chern classes Stacks.Chow.SectionZeroScheme.chernClassOfLocallyFree of 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); on X_r the identity is the constant-rank case Stacks.Chow.GenuineChern.chernClass_dualSheaf together with (ℰ^∨)|_{X_r} ≅ (ℰ|_{X_r})^∨, and for i > r both 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 rank r with a filtration whose successive quotients are the invertible modules ℒ_0, …, ℒ_{r-1}, and let ℰ^∨ be finite locally free of rank r with the dual filtration, whose successive quotients ℳ_j are tensor inverses of the ℒ_j. Both filtrations are presented as the towers of short exact sequences 0 ⟶ ℒ_j ⟶ ℰ_{j+1} ⟶ ℰ_j ⟶ 0 and 0 ⟶ ℳ_j ⟶ ℰ^∨_{j+1} ⟶ ℰ^∨_j ⟶ 0 that Stacks 02UJ consumes. Then for every n-cycle α and every i

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 rank r on X,

c_i(ℰ^∨) = (-1)^i c_i(ℰ)

in A^i(X), for every i, where c_i(-) is the degree-i part of the total Chern class, the bivariant Chern class of Stacks 0B7H, and ℰ^∨ is the dual sheaf SheafHom(ℰ, 𝒪_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 on X, of arbitrary rank,

c_i(ℰ^∨) = (-1)^i c_i(ℰ)

in A^i(X), for every i, where c_i(-) is the degree-i part of the total Chern class of Stacks 0ESW, which on the locus where ℰ has rank r is 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 r be finite locally free of rank r with a filtration whose successive quotients are the invertible modules ℒ_i = L i, let ℱ = F s be finite locally free of rank s with a filtration whose successive quotients are the invertible modules 𝒩_j = N j, and let the tower T be a filtration of ℰ ⊗_{𝒪_X} ℱ of length r·s whose (i·s+j)-th successive quotient is ℒ_i ⊗_{𝒪_X} 𝒩_j, which is the lexicographic filtration of the source. Then for every n-cycle α

c₁(ℰ ⊗ ℱ) ∩ α = s·(c₁(ℰ) ∩ α) + r·(c₁(ℱ) ∩ α)

in A_{n-1}(X), which is the identity c₁(ℰ ⊗ ℱ) = r·c₁(ℱ) + s·c₁(ℰ) of the source read against α. The rank hypotheses enter as the lengths r and s of the two filtrations, as the rank r·s of 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 every n-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 identity c₂(ℰ ⊗ ℱ) = 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 is r·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, which Stacks.Chow.firstChernCapSum_eq_chernClassCapExt_one identifies with c₁ ∩ -; 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 which c₁(ℱ)² 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 X be locally of finite type over the base and ℰ, ℱ finite locally free 𝒪_X-modules of ranks r and s. 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 X be locally of finite type over the base and ℰ, ℱ finite locally free 𝒪_X-modules of ranks r and s. 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_i being the bivariant Chern classes of Stacks 0B7H and the products those of the ring A^*(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 ranks r and s,

c₁(ℰ ⊗_{𝒪_X} ℱ) = r·c₁(ℱ) + s·c₁(ℰ)

in the commutative ring Stacks.Chow.chernSubring generated 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 ranks r and s,

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.chernSubring generated by the Chern classes, the squares and the cross term being honest products there. The cross-term coefficient is r·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 ranks r and s on X locally of finite type over S,

c₁(ℰ ⊗ ℱ) = r·c₁(ℱ) + s·c₁(ℰ)

in the ring of total Chow cohomology classes of X, where c₁(-) 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 ranks r and s on X locally of finite type over S,

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, where c_i(-) is the degree-i part of the total Chern class, the Chern class of Stacks 0B7H. The coefficient of the cross term is r·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 on X, of rank not necessarily constant, and P ∈ 𝐙[r, c₁, c₂, c₃, …],

P(ℰ) = P(r(ℰ), c₁(ℰ), c₂(ℰ), c₃(ℰ), …),

the evaluation of P at the rank r(ℰ) and the Chern classes c_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; for P homogeneous of degree p the class lies in A^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). For P ∈ 𝐙[r, c₁, c₂, …] homogeneous of degree p for the grading in which r has degree 0 and c_i has degree i, the class P(ℰ) is homogeneous of degree p: all its components outside A^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 morphism h : Y' ⟶ X over which h^*ℰ has constant rank s — for instance the inclusion of a piece where the rank of ℰ is s — the class P(ℰ) restricts to P evaluated at the integer s and the Chern classes of Stacks 0B7H of the module h^*ℰ of rank s. Relations among the classes P(ℰ) 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 is Stacks.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 on X, of rank not necessarily constant,

c₂(𝓗om(ℰ, ℰ)) = P(ℰ), P = 2 r c₂ - (r - 1) c₁²,

in A^2(X), where c₂ is the Chern class of Stacks 0ESW and P(ℰ) the class of Stacks 0FA7. The proof is the source's: 𝓗om(ℰ, ℰ) ≅ ℰ ⊗ ℰ^∨ (Stacks 0FNV), and Stacks 0FA5 and 0FA6 on the parts of X where 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 on X, 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 on X, 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 is r.

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 U on which a local free presentation of ℰ trivialises it on a finite index set, and there ℰ^∨ is free on the same index set by freeIsoDualSheafOver.

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 p is the universal power-sum polynomial precisely when substituting elementary symmetric polynomials in any n ≥ p variables gives the sum of their pth 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 variables cᵢ.

The variable indexed by i : ℕ+ has weight i. Thus the value is packaged as a weighted-homogeneous polynomial of degree p. For p + 1, the displayed recursion is Newton's formula Pₚ₊₁ = ∑ᵢ₌₁ᵖ (-1)ⁱ⁻¹ cᵢ Pₚ₊₁₋ᵢ + (-1)ᵖ (p + 1) cₚ₊₁.

noncomputable def powerSumPolynomial (p : ℕ) :
    weightedHomogeneousSubmodule ℤ (fun i : ℕ+ => (i : ℕ)) p
Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.