42.44 Chern classes and sections to 42.47 A baby case of localized…

Section42.44 Chern classes and sections#

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

Tag 0FA9, a lemma

Tag 0FA9 in the Stacks Project.

Stacks.Chow.cap_fundamentalCycle_eq_zeroSchemeCycle_of_isChernClassBivariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassOfSection.lean, line 244. The attribute's comment: “The statement is the source's in full: all four of its hypotheses are present and none is weakened. What is supplied unconditionally is the first step of the source's proof, the reduction to the case X = X': the cap operation of a bivariant class satisfying the characterization of Tag 0B7H is identified, after transport along the base-change isomorphism, with the cap product formed on the test scheme with the pulled-back module. The reduced case itself is carried as the declared hypothesis hreduced; the source obtains it by induction on r, whose base case r = 1 is Tag 02SQ -- proved here as Stacks.ChernCap42.firstChernClassCapOfInvertible_closedSubscheme_eq_zeroScheme -- and whose step r > 1 needs the projective space bundle formula of Tag 02TX, the decomposition of CH_*(P) making flat pullback along the projection injective. Only the flatness and relative-dimension clauses of Tag 02TX are carried in this repository, so that formula is not available and the rest of this directory carries it as a hypothesis wherever it is needed. The cap product with the higher Chern classes is the parameter Stacks.Chow.HigherChernCapRule standing in for Tag 0B7G, which is not formalized, as in every other file of this directory. The source's hypothesis that f^*E has constant rank r is read as constant rank r on X, which is what forming c_r(E) requires in this encoding.”.

[Stacks, Tag 0FA9]. Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S, let ℰ be a finite locally free 𝒪_X-module of constant rank r, let f : X' ⟶ X be locally of finite type and let s ∈ Γ(X', f^*ℰ). Assume dim_δ(X') = n, that dim_δ(Z(s)) ≤ n - r, and that for every generic point ξ ∈ Z(s) with δ(ξ) = n - r the ideal of Z(s) in 𝒪_{X', ξ} is generated by a regular sequence of length r. Then

c_r(ℰ) ∩ [X']_n = [Z(s)]_{n - r} in CH_{n - r}(X'),

where c_r(ℰ) is read as a bivariant class c for 𝟙 X satisfying the characterization Stacks.Chow.IsChernClassBivariant of Stacks 0B7H, and its cap product against the Chow group of X' is transported from X ×_X X' to X' along the base-change isomorphism, as the defining conditions of a bivariant class require.

This is the source's statement together with the first step of its proof: the reduction to the case X = X' using that c_r(ℰ) is a bivariant class. The reduced case Stacks.Chow.TopChernCapEqZeroScheme is the hypothesis hreduced; the source proves it by induction on r from Stacks 02SQ and the projective space bundle formula of Stacks 02TX, and the latter is not carried in this repository.

theorem cap_fundamentalCycle_eq_zeroSchemeCycle_of_isChernClassBivariant
    (C : ChowSituation.{u}) {X X' : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (E : X.Modules) (r : ℕ)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r]
    (G : GysinSystem C) (cap : HigherChernCapRule C r)
    (c : BivariantClass C G sX sX (𝟙 X) (Category.id_comp sX) ((Fin.last r : Fin (r + 1)) : ℤ))
    (hc : IsChernClassBivariant C sX E r G cap
      (pullbackPreservesRank_of_isFiniteLocallyFreeOfRank E r) (Fin.last r) c)
    (f : X' ⟶ X) [LocallyOfFiniteType f]
    (s : Γ((Scheme.Modules.pullback f).obj E, ⊤)) (n : ℤ)
    (hX' : schemeDeltaDimension C (f ≫ sX) = (n : EInt))
    (hZ : schemeDeltaDimension C
        ((zeroSchemeOfSection X' ((Scheme.Modules.pullback f).obj E) s).subschemeι ≫ (f ≫ sX)) ≤
      ((n - (r : ℤ) : ℤ) : EInt))
    (hreg : IsRegularZeroSchemeSequence C (f ≫ sX) ((Scheme.Modules.pullback f).obj E) s r
      (n - (r : ℤ)))
    (hreduced : TopChernCapEqZeroScheme C (f ≫ sX) r cap ((Scheme.Modules.pullback f).obj E)
      (AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback f E r) s n) :
    chowPushforwardOfIso C (pullback.fst (𝟙 X) f ≫ sX) (f ≫ sX) (identityBaseChangeIso f).hom
        (identityBaseChangeIso_hom_comp_base C sX f) (n - ((Fin.last r : Fin (r + 1)) : ℤ))
        (c.cap f n (QuotientAddGroup.mk' (rationalEquivalences C (f ≫ sX) n)
          (cycleAssociatedToClosedSubscheme C (f ≫ sX) (𝟙 X') n))) =
      QuotientAddGroup.mk' (rationalEquivalences C (f ≫ sX) (n - (r : ℤ)))
        (cycleAssociatedToClosedSubscheme C (f ≫ sX)
          (zeroSchemeOfSection X' ((Scheme.Modules.pullback f).obj E) s).subschemeι
          (n - (r : ℤ)))

Stacks.Chow.topChernCapEqZeroScheme_rank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassOfSection.lean, line 391. The attribute's comment: “the reduced case X = X' of the tag at rank one, which is the base case of the induction on r by which the source proves it. What is supplied unconditionally is the passage from Tag 02SQ -- proved here as Stacks.ChernCap42.firstChernClassCapOfInvertible_closedSubscheme_eq_zeroScheme -- to the statement Stacks.Chow.TopChernCapEqZeroScheme that the two carriers of this tag above take as their hypothesis hreduced: Tag 02SQ is stated for a closed immersion with the invertible module on the ambient scheme, so this reads it at the identity of X' by transporting the section and the zero scheme along the pullback-by-the-identity isomorphism of modules, and matches the two degree conventions. Three things are assumed. hcap is Tag 02U5 at j = 1, the identification of the cap product parameter Stacks.Chow.HigherChernCapRule -- which stands in for the unformalized Tag 0B7G, as in every other file of this directory -- with the first Chern class cap product of Tag 02SO; an arbitrary cap rule pins nothing, exactly as recorded in StacksFrontier.AlgebraicGeometry.Chow.ChernClassTwist and StacksFrontier.AlgebraicGeometry.Chow.ChernWhitney.FilteredAdditivity. hs is the stalk-injectivity hypothesis of Tag 02SQ itself, which the source derives from the regular-sequence hypothesis of this tag at length one; that derivation is not carried out here, so hreg is unused. hinv and hinv' are invertibility of the rank-one module and of its pullback along the identity, which is clause 1 of Tag 0B8M. The step r > 1 of the induction is not covered at all: it needs the projective space bundle formula of Tag 02TX, of which only the flatness and relative-dimension clauses are carried in this repository.”.

[Stacks, Tag 0FA9], the reduced case at r = 1. The hypothesis hreduced of the two theorems above, at a module F of rank one on X', discharged from Stacks 02SQ.

Stacks 02SQ is stated for a closed immersion i : Y ⟶ X with the invertible module on the ambient scheme X and the section taken in Γ(Y, i^*L), so using it at i = 𝟙 X' means transporting the section across AlgebraicGeometry.Scheme.Modules.pullbackId: t is the section of (𝟙 X')^*F corresponding to s under that isomorphism, and ht says so. The zero schemes of s and of t then agree by AlgebraicGeometry.zeroScheme_eq_of_iso, and Z(s) of this file is the zero scheme of Stacks 02OQ by Stacks.Chow.zeroSchemeOfSection_eq_zeroScheme.

hs is the third hypothesis of Stacks 02SQ, injectivity of multiplication by t on the stalk at the generic point of every component of Z(t) of δ-dimension k. The source derives it from the regular-sequence hypothesis Stacks.Chow.IsRegularZeroSchemeSequence, which at r = 1 says that the ideal of Z(s) in that local ring is generated by a single nonzerodivisor; that derivation is not carried out here, so hs is assumed and hreg is unused. See the implementation notes of this file.

theorem topChernCapEqZeroScheme_rank_one
    (C : ChowSituation.{u}) {X' : Scheme.{u}} (q : X' ⟶ C.S) [LocallyOfFiniteType q]
    (cap : HigherChernCapRule C 1) (F : X'.Modules)
    (hF : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F 1)
    (hinv : AlgebraicGeometry.SheafOfModules.IsInvertible X'.sheaf.obj
      X'.ringCatSheaf.property F)
    (hinv' : AlgebraicGeometry.SheafOfModules.IsInvertible X'.sheaf.obj
      X'.ringCatSheaf.property ((Scheme.Modules.pullback (𝟙 X')).obj F))
    (s : Γ(F, ⊤)) (k : ℤ)
    (t : ((Scheme.Modules.pullback (𝟙 X')).obj F).sections)
    (ht : Scheme.Modules.Hom.app ((Scheme.Modules.pullbackId X').app F).hom ⊤
      (t.eval (Opposite.op ⊤)) = s)
    (hs : ∀ ξ : genericPoints (Stacks.Divisors.zeroScheme X'
        ((Scheme.Modules.pullback (𝟙 X')).obj F) (t.eval (Opposite.op ⊤))).subscheme,
      relativeDimension C.dimensionFunction (𝟙 X' ≫ q)
          ((Stacks.Divisors.zeroScheme X' ((Scheme.Modules.pullback (𝟙 X')).obj F)
            (t.eval (Opposite.op ⊤))).subschemeι ξ.1) = k →
        Function.Injective (ConcreteCategory.hom
          ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u}
            ((Stacks.Divisors.zeroScheme X' ((Scheme.Modules.pullback (𝟙 X')).obj F)
              (t.eval (Opposite.op ⊤))).subschemeι ξ.1)).map
            ((Scheme.Modules.toPresheaf X').map
              (((Scheme.Modules.pullback (𝟙 X')).obj F).unitHomEquiv.symm t)))))
    (hcap : IsFirstChernCapAtRankOne C q cap F hF hinv k) :
    TopChernCapEqZeroScheme C q 1 cap F hF s (k + 1)

Stacks.Chow.cap_fundamentalCycle_eq_zeroSchemeCycle_rank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassOfSection.lean, line 462. The attribute's comment: “the tag at rank one, with the hypothesis hreduced of the two carriers above DISCHARGED rather than assumed: the reduced case X = X' is supplied at rank one by Stacks.Chow.topChernCapEqZeroScheme_rank_one from Tag 02SQ, which is proved. So for a module of rank one this is the source's statement with the source's hypotheses, together with the whole of the source's proof -- the Tag 0B7H reduction of the first carrier above, composed with the base case of the induction. Three assumptions remain, all of them recorded on Stacks.Chow.topChernCapEqZeroScheme_rank_one: Tag 02U5 at j = 1, identifying the cap product parameter standing in for the unformalized Tag 0B7G with the first Chern class cap product of Tag 02SO; the stalk-injectivity hypothesis of Tag 02SQ, which the source derives from this tag's regular-sequence hypothesis at length one; and invertibility of the rank-one module and of its pullback along the identity, which is clause 1 of Tag 0B8M. Rank r > 1 is not covered: that step of the induction needs the projective space bundle formula of Tag 02TX, of which only the flatness and relative-dimension clauses are carried in this repository.”.

[Stacks, Tag 0FA9] at rank one, with no reduced case assumed. The first theorem of this file specialised to a module E of rank one, with its hypothesis hreduced discharged by Stacks.Chow.topChernCapEqZeroScheme_rank_one. So this is a genuine instance of the tag: the only inputs left are the characterization of c₁(E) as a bivariant class (Stacks 0B7H), the three dimension and regularity hypotheses of the tag, and the three assumptions described at Stacks.Chow.topChernCapEqZeroScheme_rank_one.

theorem cap_fundamentalCycle_eq_zeroSchemeCycle_rank_one
    (C : ChowSituation.{u}) {X X' : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (E : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E 1]
    (G : GysinSystem C) (cap : HigherChernCapRule C 1)
    (c : BivariantClass C G sX sX (𝟙 X) (Category.id_comp sX) ((Fin.last 1 : Fin 2) : ℤ))
    (hc : IsChernClassBivariant C sX E 1 G cap
      (pullbackPreservesRank_of_isFiniteLocallyFreeOfRank E 1) (Fin.last 1) c)
    (f : X' ⟶ X) [LocallyOfFiniteType f]
    (s : Γ((Scheme.Modules.pullback f).obj E, ⊤)) (k : ℤ)
    (hinv : AlgebraicGeometry.SheafOfModules.IsInvertible X'.sheaf.obj
      X'.ringCatSheaf.property ((Scheme.Modules.pullback f).obj E))
    (hinv' : AlgebraicGeometry.SheafOfModules.IsInvertible X'.sheaf.obj
      X'.ringCatSheaf.property
      ((Scheme.Modules.pullback (𝟙 X')).obj ((Scheme.Modules.pullback f).obj E)))
    (t : ((Scheme.Modules.pullback (𝟙 X')).obj
      ((Scheme.Modules.pullback f).obj E)).sections)
    (ht : Scheme.Modules.Hom.app
      ((Scheme.Modules.pullbackId X').app ((Scheme.Modules.pullback f).obj E)).hom ⊤
      (t.eval (Opposite.op ⊤)) = s)
    (hs : ∀ ξ : genericPoints (Stacks.Divisors.zeroScheme X'
        ((Scheme.Modules.pullback (𝟙 X')).obj ((Scheme.Modules.pullback f).obj E))
        (t.eval (Opposite.op ⊤))).subscheme,
      relativeDimension C.dimensionFunction (𝟙 X' ≫ (f ≫ sX))
          ((Stacks.Divisors.zeroScheme X'
            ((Scheme.Modules.pullback (𝟙 X')).obj ((Scheme.Modules.pullback f).obj E))
            (t.eval (Opposite.op ⊤))).subschemeι ξ.1) = k →
        Function.Injective (ConcreteCategory.hom
          ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u}
            ((Stacks.Divisors.zeroScheme X'
              ((Scheme.Modules.pullback (𝟙 X')).obj ((Scheme.Modules.pullback f).obj E))
              (t.eval (Opposite.op ⊤))).subschemeι ξ.1)).map
            ((Scheme.Modules.toPresheaf X').map
              (((Scheme.Modules.pullback (𝟙 X')).obj
                ((Scheme.Modules.pullback f).obj E)).unitHomEquiv.symm t)))))
    (hcap : IsFirstChernCapAtRankOne C (f ≫ sX) cap ((Scheme.Modules.pullback f).obj E)
      (AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback f E 1) hinv k)
    (hX' : schemeDeltaDimension C (f ≫ sX) = ((k + 1 : ℤ) : EInt))
    (hZ : schemeDeltaDimension C
        ((zeroSchemeOfSection X' ((Scheme.Modules.pullback f).obj E) s).subschemeι ≫ (f ≫ sX)) ≤
      ((k + 1 - (1 : ℤ) : ℤ) : EInt))
    (hreg : IsRegularZeroSchemeSequence C (f ≫ sX) ((Scheme.Modules.pullback f).obj E) s 1
      (k + 1 - (1 : ℤ))) :
    chowPushforwardOfIso C (pullback.fst (𝟙 X) f ≫ sX) (f ≫ sX) (identityBaseChangeIso f).hom
        (identityBaseChangeIso_hom_comp_base C sX f)
        (k + 1 - ((Fin.last 1 : Fin 2) : ℤ))
        (c.cap f (k + 1) (QuotientAddGroup.mk' (rationalEquivalences C (f ≫ sX) (k + 1))
          (cycleAssociatedToClosedSubscheme C (f ≫ sX) (𝟙 X') (k + 1)))) =
      QuotientAddGroup.mk' (rationalEquivalences C (f ≫ sX) (k + 1 - (1 : ℤ)))
        (cycleAssociatedToClosedSubscheme C (f ≫ sX)
          (zeroSchemeOfSection X' ((Scheme.Modules.pullback f).obj E) s).subschemeι
          (k + 1 - (1 : ℤ)))

Stacks.Chow.totalChernOfFiniteLocallyFree_cap_fundamentalCycle_eq_zeroSchemeCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassOfSection/TotalChern.lean, line 77. The attribute's comment: “c_r(E) cap [X']_n = [Z(s)]_{n-r} for E finite locally free on X with f^*E of constant rank r on X', c_r(E) the degree-r component of the Chern class of Tag 0ESW capped on the test scheme f, and with dim X' at most n.”.

[Stacks, Tag 0FA9]. Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S, let ℰ be a finite locally free 𝒪_X-module, let f : X' ⟶ X be locally of finite type such that f^*ℰ has constant rank r, and let s ∈ Γ(X', f^*ℰ). Assume dim_δ(X') ≤ n, that dim_δ(Z(s)) ≤ n - r, and that for every generic point ξ ∈ Z(s) with δ(ξ) = n - r the ideal of Z(s) in 𝒪_{X', ξ} is generated by a regular sequence of length r. Then

c_r(ℰ) ∩ [X']_n = [Z(s)]_{n - r} in CH_{n - r}(X'),

where c_r(ℰ) ∈ A^r(X) is the degree-r component of the total Chern class Stacks.Chow.totalChernOfFiniteLocallyFree and c_r(ℰ) ∩ - is its cap operation on the test scheme f.

theorem totalChernOfFiniteLocallyFree_cap_fundamentalCycle_eq_zeroSchemeCycle
    (C : ChowSituation.{u}) {X X' : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (E : X.Modules) [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E] (r : ℕ)
    (f : X' ⟶ X) [LocallyOfFiniteType f]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      ((Scheme.Modules.pullback f).obj E) r]
    (s : Γ((Scheme.Modules.pullback f).obj E, ⊤)) (n : ℤ)
    (hX' : schemeDeltaDimension C (f ≫ sX) ≤ (n : EInt))
    (hZ : schemeDeltaDimension C
        ((RegularSectionSequence.zeroScheme X' ((Scheme.Modules.pullback f).obj E) s).subschemeι ≫
          (f ≫ sX)) ≤
      ((n - (r : ℤ) : ℤ) : EInt))
    (hreg : IsRegularSequenceOnZeroScheme C (f ≫ sX) ((Scheme.Modules.pullback f).obj E) s r
      (n - (r : ℤ))) :
    chowPushforwardOfIso C (pullback.fst (𝟙 X) f ≫ sX) (f ≫ sX) (identityBaseChangeIso f).hom
        (identityBaseChangeIso_hom_comp_base C sX f) (n - (r : ℤ))
        ((totalChernOfFiniteLocallyFree C sX E r).cap f n
          (QuotientAddGroup.mk' (rationalEquivalences C (f ≫ sX) n)
            (cycleAssociatedToClosedSubscheme C (f ≫ sX) (𝟙 X') n))) =
      QuotientAddGroup.mk' (rationalEquivalences C (f ≫ sX) (n - (r : ℤ)))
        (cycleAssociatedToClosedSubscheme C (f ≫ sX)
          (RegularSectionSequence.zeroScheme X' ((Scheme.Modules.pullback f).obj E) s).subschemeι
          (n - (r : ℤ)))

Stacks.Chow.SectionZeroScheme.chernClassOfLocallyFree_cap_fundamental_eq_zeroSchemeCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SectionZeroScheme/TopChernClassCap.lean, line 49. The attribute's comment: “c_r(E) ∩ [X']_n = [Z(s)]_{n-r} under dim_δ(X') = n, f^*E of constant rank r, dim_δ(Z(s)) ≤ n - r and the regular-sequence condition at the generic points of Z(s) of δ-dimension n - r”.

[Stacks, Tag 0FA9]. Let ℰ be finite locally free on X, f : X' ⟶ X locally of finite type and s a section of f^*ℰ with zero scheme Z(s). If dim_δ(X') = n, f^*ℰ has constant rank r, dim_δ(Z(s)) ≤ n - r and at every generic point ξ of Z(s) with δ(ξ) = n - r the ideal of Z(s) in 𝒪_{X', ξ} is generated by a regular sequence of length r, then c_r(ℰ) ∩ [X']_n = [Z(s)]_{n - r} in CH_{n - r}(X'), where c_r(ℰ) ∈ A^r(X) is the Chern class of Stacks 0ESW.

theorem chernClassOfLocallyFree_cap_fundamental_eq_zeroSchemeCycle (C : ChowSituation.{u})
    {X X' : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (E : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E]
    (f : X' ⟶ X) [LocallyOfFiniteType f] (r : ℕ)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      ((Scheme.Modules.pullback f).obj E) r]
    (s : Γ((Scheme.Modules.pullback f).obj E, ⊤)) (n : ℤ)
    (hX' : schemeDeltaDimension C (f ≫ sX) = (n : EInt))
    (hZ : schemeDeltaDimension C
        ((zeroSchemeOfSection X' ((Scheme.Modules.pullback f).obj E) s).subschemeι ≫ (f ≫ sX)) ≤
      ((n - (r : ℤ) : ℤ) : EInt))
    (hreg : IsRegularZeroSchemeSequence C (f ≫ sX) ((Scheme.Modules.pullback f).obj E) s r
      (n - (r : ℤ))) :
    (chernClassOfLocallyFree E C sX r).idRule C sX (gysinSystemOfInvertible C) f n
        (QuotientAddGroup.mk' (rationalEquivalences C (f ≫ sX) n)
          (cycleAssociatedToClosedSubscheme C (f ≫ sX) (𝟙 X') n)) =
      QuotientAddGroup.mk' (rationalEquivalences C (f ≫ sX) (n - (r : ℤ)))
        (cycleAssociatedToClosedSubscheme C (f ≫ sX)
          (zeroSchemeOfSection X' ((Scheme.Modules.pullback f).obj E) s).subschemeι
          (n - (r : ℤ)))
Tag 0FAA, a lemma

Tag 0FAA in the Stacks Project.

Stacks.Chow.dualBundleFlatPullback_eq_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SubbundleTopChern/CanonicalFlatPullback.lean, line 336. The attribute's comment: “the flat pullback p^* of the statement: the flat pullback along a projection of locally constant relative dimension, assembled over a decomposition of X into open and closed pieces of constant rank, does not depend on the decomposition”.

The piecewise flat pullback does not depend on the decomposition. Over any decomposition X = ∐ U_i into open and closed pieces on which ℱ has constant rank, the piecewise flat pullback Stacks.Chow.dualBundleFlatPullback is the canonical flat pullback p^*.

theorem dualBundleFlatPullback_eq_canonical {I : Type u} (U : I → X.Opens)
    (hU : IsClopenDecomposition U) (ρ : I → ℕ)
    (hρ : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      ((Scheme.Modules.pullback (U i).ι).obj F) (ρ i)) (β : ∀ m : ℤ, chowGroup C sX m) :
    dualBundleFlatPullback C sX F U hU ρ hρ β = canonicalDualBundleFlatPullback C sX F β

Stacks.Chow.canonicalDualBundleFlatPullback_eq_dualBundlePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SubbundleTopChern/CanonicalFlatPullback.lean, line 364. The attribute's comment: “the flat pullback p^ of the statement: when the module has constant rank r, p^ is the flat pullback of relative dimension r along the projection (Tag 02S1)”.

For ℱ of constant rank r, p^* is the flat pullback of relative dimension r. The degree d part of p^*β is p^*(β_{d-r}) for the flat pullback p^* : A_{d-r}(X) ⟶ A_d(𝐕(ℱ^∨)) of Stacks 02S1 along the projection, which is flat of relative dimension r.

theorem canonicalDualBundleFlatPullback_eq_dualBundlePullback (r : ℕ)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} F r]
    (β : ∀ m : ℤ, chowGroup C sX m) (d : ℤ) :
    canonicalDualBundleFlatPullback C sX F β d =
      chowGroupCast C _ (show d - (r : ℤ) + (r : ℤ) = d by ring)
        (dualBundlePullback C sX F r (d - r) (β (d - r)))

Stacks.Chow.subbundleEmbedding_pushforward_canonicalDualBundleFlatPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SubbundleTopChern/CanonicalFlatPullback.lean, line 420. The attribute's comment: “i_(p')^alpha = p^(c_top(E) cap alpha) in prod_d CH_d(N), for a short exact sequence 0 -> N' -> N -> E -> 0 of finite locally free modules of arbitrary (locally constant) ranks and alpha in CH_k(X); p^, (p')^* are the flat pullbacks along the projections, which have locally constant relative dimension, c_top(E) is the class of Tag 0FA4 and c_top(E) cap alpha the element of prod_m CH_m(X) with degree m part c_top(E)_{k-m} cap alpha”.

Stacks 0FAA. Let 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free 𝒪_X-modules, let i : N' = Spec_X(Sym((𝒩')^∨)) ⟶ N = Spec_X(Sym(𝒩^∨)) be the closed embedding and p' : N' ⟶ X, p : N ⟶ X the projections. For α ∈ A_k(X),

i_*(p')^*α = p^*(c_top(ℰ) ∩ α) in ∏_d A_d(N).

The ranks are only locally constant, so p and p' have locally constant relative dimension and both sides live in ∏_d A_d(N). Here (p')^* and p^* are the flat pullbacks Stacks.Chow.canonicalDualBundleFlatPullback: the unique families whose restriction over every open of constant rank r is the flat pullback of relative dimension r of Stacks 02S1 (Stacks.Chow.isDualBundleFlatPullback_iff), equal to that flat pullback when the rank is constant (Stacks.Chow.canonicalDualBundleFlatPullback_eq_dualBundlePullback). The class c_top(ℰ) ∩ α ∈ ∏_m A_m(X) is the cap product with the top Chern class of Stacks 0FA4 (Stacks.Chow.topChernCapFamily), and α is read in ∏_m A_m(X) in degree k.

theorem subbundleEmbedding_pushforward_canonicalDualBundleFlatPullback (k : ℤ)
    (α : chowGroup C sX k) :
    haveI := isClosedImmersion_subbundleEmbedding_of_shortExact N' N E inc pr w hseq
    (fun d ↦ chowPushforwardOfIsClosedImmersion C (dualVectorBundleToBase N' ≫ sX)
        (dualVectorBundleToBase N ≫ sX) (subbundleEmbedding N' N inc)
        (subbundleEmbedding_comp_base N' N sX inc) d
        (canonicalDualBundleFlatPullback C sX N' (homogeneousChowFamily C sX k α) d)) =
      canonicalDualBundleFlatPullback C sX N (topChernCapFamily C sX E k α)

Stacks.Chow.isClosedImmersion_subbundleEmbedding_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SubbundleTopChern/RankOne.lean, line 106. The attribute's comment: “the closed embedding i : N' = Spec_X(Sym((N')^dual)) -> N = Spec_X(Sym(N^dual)) of the statement, for a short exact sequence of finite locally free modules of arbitrary ranks”.

Stacks 0FAA, the closed embedding. For a short exact sequence 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0 of finite locally free 𝒪_X-modules, of arbitrary ranks, the morphism i : N' = Spec_X(Sym((𝒩')^∨)) ⟶ N = Spec_X(Sym(𝒩^∨)) is a closed immersion: it is the base change of the zero section of 𝐕(ℰ^∨), a section of a separated morphism.

theorem isClosedImmersion_subbundleEmbedding_of_shortExact :
    IsClosedImmersion (subbundleEmbedding N' N inc)

Stacks.Chow.isClosedImmersion_subbundleEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SubbundleTopChernClass.lean, line 286. The attribute's comment: “the closed embedding i : N' = Spec_X(Sym((N')^dual)) -> N = Spec_X(Sym(N^dual)) of the tag's setup. The morphism is the canonical one -- Stacks.Chow.subbundleEmbedding, the relative spectrum of Sym applied to the dual of the given inclusion -- and the short exact sequence is consumed, not carried: it is what makes the dual N^dual -> (N')^dual surjective, by Tag 0FV8 (Stacks.AlgebraicGeometry.ReflexiveModules.epi_dualMap_of_shortExact). What is assumed is the general lemma Stacks.Chow.VectorBundleEpiClosedImmersion, that a surjection of quasi-coherent modules induces a closed immersion of the associated vector bundles; nothing in this repository relates AlgebraicGeometry.Scheme.Modules.vectorBundleMap to AlgebraicGeometry.IsClosedImmersion, so that general statement is carried as a named hypothesis rather than proved.”.

[Stacks, Tag 0FAA], the closed embedding of the tag's setup. Given a short exact sequence 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0 of finite locally free 𝒪_X-modules, the canonical morphism i : N' = Spec_X(Sym((𝒩')^∨)) ⟶ N = Spec_X(Sym(𝒩^∨)) is a closed immersion.

The sequence is used through Stacks.Chow.epi_dualMap_of_subbundleShortExact: it makes the dual 𝒩^∨ ⟶ (𝒩')^∨ surjective, and a surjection of modules gives a closed immersion of vector bundles, which is the hypothesis hci.

theorem isClosedImmersion_subbundleEmbedding (hci : VectorBundleEpiClosedImmersion.{u})
    (inc : N' ⟶ N) (pr : N ⟶ E) (w : inc ≫ pr = 0)
    (hseq : (ShortComplex.mk inc pr w).ShortExact) :
    IsClosedImmersion (subbundleEmbedding N' N inc)

Stacks.Chow.subbundleEmbedding_pushforward_flatPullback_eq_topChernCap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SubbundleTopChernClass.lean, line 445. The attribute's comment: “the tag's equality i_(p')^alpha = p^(c_top(E) cap alpha) in CH_{k+r'}(N), for a short exact sequence of finite locally free modules of CONSTANT ranks r', r, e -- the case the source reduces to in the first line of its proof, c_top being by definition (Tag 0FA4) assembled from the Chern classes of the restrictions to the constant-rank loci. The morphisms i, p, p' are the canonical constructed ones, not quantified: p and p' are Stacks.Chow.dualVectorBundleToBase, the projections of the relative spectra of the symmetric algebras on the duals, and i is Stacks.Chow.subbundleEmbedding, the relative spectrum of Sym of the dual of the given inclusion. The short exact sequence is CONSUMED twice: through Tag 0FV8 it makes the dual N^dual -> (N')^dual surjective and hence i a closed immersion (so that i_ exists at all), and through rank additivity it gives r = r' + e, which is what puts the two sides of the equality in the same Chow group. Three things are assumed, each named. hstep is the equality i_(p')^alpha = c_top(p^E) cap p^alpha in CH_(N) that the source derives from Tag 0FA9 applied to the canonical global section of p^E, whose vanishing scheme is N'; that section is not constructed in this repository, the flat-pullback formula for the cycle of a prime cycle is not available, and Tag 0FA9 itself is formalized only with its reduced case assumed and only at rank one. hflat is Tag 02U8, the compatibility of the cap product with flat pullback along p, which is the step from hstep to the tag's own equality. The general lemma that a surjection of quasi-coherent modules gives a closed immersion of vector bundles is assumed as Stacks.Chow.VectorBundleEpiClosedImmersion. Flatness, local finite type and the relative dimension of the two bundle projections are carried as hypotheses, Tag 02TY being absent, and the two instances of Tag 02S1 for flat pullback are quantified over. The cap product with the higher Chern classes is the standing parameter Stacks.Chow.HigherChernCapRule of this directory for Tag 0B7G, as in the carriers of Tag 0FA9.”.

[Stacks, Tag 0FAA]. Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S and let 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free 𝒪_X-modules, of constant ranks r', r and e. Let i : N' = Spec_X(Sym((𝒩')^∨)) ⟶ N = Spec_X(Sym(𝒩^∨)) be the canonical closed embedding and p' : N' ⟶ X, p : N ⟶ X the structure morphisms. Then for α ∈ CH_k(X)

i_*(p')^*α = p^*(c_top(ℰ) ∩ α)

in CH_{k+r'}(N), the two degrees k + r' and (k - e) + r agreeing because r = r' + e.

All of i, p, p' are the canonical constructed morphisms: p and p' are Stacks.Chow.dualVectorBundleToBase, i.e. AlgebraicGeometry.Scheme.Modules.vectorBundleToBase of the dual sheaves, and i is Stacks.Chow.subbundleEmbedding, i.e. AlgebraicGeometry.Scheme.Modules.vectorBundleMap of the dual of the inclusion. The short exact sequence is consumed twice: it makes i a closed immersion, through Stacks.Chow.epi_dualMap_of_subbundleShortExact, and it gives the degree identity Stacks.Chow.subbundleDegree_eq without which the equality is not even a well-formed statement.

The two named hypotheses are the source's own two steps: hstep is the equality Tag 0FA9 gives on N for the canonical section of p^*ℰ, and hflat is the flat-pullback compatibility of the Chern classes, Tag 02U8. See the implementation notes of this file for what each of them needs and why it is not available here.

theorem subbundleEmbedding_pushforward_flatPullback_eq_topChernCap
    (inc : N' ⟶ N) (pr : N ⟶ E) (w : inc ≫ pr = 0)
    (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (hci : VectorBundleEpiClosedImmersion.{u}) (x : X)
    (hstep : SubbundleChernCapStep C sX N' N E r' r e hp' hp cap k inc
      (isClosedImmersion_subbundleEmbedding N' N E hci inc pr w hseq))
    (hflat : TopChernCapFlatPullbackOfBundle C sX N E r e hp cap k)
    (hfac' : FlatPullbackFactorsThroughRationalEquivalence C
      (dualVectorBundleToBase N' ≫ sX) sX (dualVectorBundleToBase N') rfl r' hp' k)
    (hfac : FlatPullbackFactorsThroughRationalEquivalence C
      (dualVectorBundleToBase N ≫ sX) sX (dualVectorBundleToBase N) rfl r hp k)
    (hfacp : FlatPullbackFactorsThroughRationalEquivalence C
      (dualVectorBundleToBase N ≫ sX) sX (dualVectorBundleToBase N) rfl r hp (k - (e : ℤ)))
    (α : chowGroup C sX k) :
    letI := isClosedImmersion_subbundleEmbedding N' N E hci inc pr w hseq
    chowPushforwardOfIsClosedImmersion C (dualVectorBundleToBase N' ≫ sX)
        (dualVectorBundleToBase N ≫ sX) (subbundleEmbedding N' N inc)
        (subbundleEmbedding_comp_base N' N sX inc) (k + (r' : ℤ))
        (flatPullbackChow C (dualVectorBundleToBase N' ≫ sX) sX (dualVectorBundleToBase N') rfl
          r' hp' k hfac' α) =
      Eq.mp (congrArg (chowGroup C (dualVectorBundleToBase N ≫ sX))
          (subbundleDegree_eq N' N E r' r e inc pr w hseq x k))
        (flatPullbackChow C (dualVectorBundleToBase N ≫ sX) sX (dualVectorBundleToBase N) rfl r
          hp (k - (e : ℤ)) hfacp (cap sX E k (Fin.last e) α))

Stacks.Chow.subbundleEmbeddingRestrict_pushforward_flatPullback_eq_topChernCap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SubbundleTopChernClass/ArbitraryRank.lean, line 187. The attribute's comment: “For a short exact sequence of finite locally free modules of arbitrary ranks: on every open U of X where N' and E have constant ranks r' and e, with p' and p restricted to the parts of N' and N over U (flat of relative dimensions r' and r' + e), i restricted to them, and c_top(E) the top Chern class of Tag 0FA4 acting by its degree-e part.”.

Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S and let 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free 𝒪_X-modules. Let i : N' = Spec_X(Sym((𝒩')^∨)) ⟶ N = Spec_X(Sym(𝒩^∨)) be the canonical closed embedding and p' : N' ⟶ X, p : N ⟶ X the structure morphisms. Then for α ∈ CH_k(X)

i_*(p')^*α = p^*(c_top(ℰ) ∩ α),

c_top(ℰ) being the top Chern class of Stacks 0FA4.

The ranks of 𝒩' and ℰ are locally constant and the flat pullbacks are taken where they are constant: for every open U ⊆ X on which 𝒩' has rank r' and ℰ has rank e, the projections restrict to flat morphisms p'⁻¹(U) ⟶ X and p⁻¹(U) ⟶ X of relative dimensions r' and r' + e, i restricts to the closed embedding p'⁻¹(U) ⟶ p⁻¹(U), c_top(ℰ) acts by its degree-e part (Stacks.Chow.topChernCap), and the identity holds in CH_{k+r'}(p⁻¹(U)) = CH_{(k-e)+(r'+e)}(p⁻¹(U)). Taking for U the pieces of the decomposition of X by the ranks of 𝒩' and ℰ, this is the identity of the tag in CH_*(N) = ∏_U CH_*(p⁻¹(U)).

theorem subbundleEmbeddingRestrict_pushforward_flatPullback_eq_topChernCap (U : X.Opens)
    (r' e : ℕ) (hN' : U ≤ rankLocus N' r') (hE : U ≤ rankLocus E e) (k : ℤ)
    (α : chowGroup C sX k) :
    letI := isFiniteLocallyFreeOfRank_pullback_ι_of_le_rankLocus N' U r' hN'
    letI := isFiniteLocallyFreeOfRank_pullback_ι_of_shortExact N' N E inc pr w hseq U r' e hN'
      hE
    letI := isClosedImmersion_subbundleEmbeddingRestrict N' N inc U E pr w hseq
    letI := locallyOfFiniteType_dualVectorBundleRestrict N' U r'
    letI := flat_dualVectorBundleRestrict N' U r'
    letI := locallyOfFiniteType_dualVectorBundleRestrict N U (r' + e)
    letI := flat_dualVectorBundleRestrict N U (r' + e)
    chowPushforwardOfIsClosedImmersion C
        (((dualVectorBundleToBase N' ⁻¹ᵁ U).ι ≫ dualVectorBundleToBase N') ≫ sX)
        (((dualVectorBundleToBase N ⁻¹ᵁ U).ι ≫ dualVectorBundleToBase N) ≫ sX)
        (subbundleEmbeddingRestrict N' N inc U)
        (subbundleEmbeddingRestrict_comp_base N' N inc U sX) (k + (r' : ℤ))
        (flatPullbackChow C (((dualVectorBundleToBase N' ⁻¹ᵁ U).ι ≫ dualVectorBundleToBase N') ≫ sX)
          sX ((dualVectorBundleToBase N' ⁻¹ᵁ U).ι ≫ dualVectorBundleToBase N') rfl r'
          (relativeDimension_dualVectorBundleRestrict N' U r') k
          (flatPullbackDescends C _ _ _ _ _ _ _) α) =
      Eq.mp (congrArg (chowGroup C
          (((dualVectorBundleToBase N ⁻¹ᵁ U).ι ≫ dualVectorBundleToBase N) ≫ sX))
          (by push_cast; ring))
        (flatPullbackChow C (((dualVectorBundleToBase N ⁻¹ᵁ U).ι ≫ dualVectorBundleToBase N) ≫ sX)
          sX ((dualVectorBundleToBase N ⁻¹ᵁ U).ι ≫ dualVectorBundleToBase N) rfl (r' + e)
          (relativeDimension_dualVectorBundleRestrict N U (r' + e)) (k - (e : ℤ))
          (flatPullbackDescends C _ _ _ _ _ _ _) (topChernCap C sX E k e α))
Sources

Section42.45 The Chern character and tensor products#

Section 42.45 of the Stacks Project, Tag 02UM. 4 tags here are carried by 18 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0ESX, a remark

Tag 0ESX in the Stacks Project.

Stacks.Chow.fullChernCharacter, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/ChernCharacter.lean, line 225. The attribute's comment: “the full Chern character of a finite locally free module of not necessarily constant rank as an element of the product ∏_{p ≥ 0} (A^p(X) ⊗ 𝐐), assembled over the rank loci from the constant-rank power sums P_p(c_1(E|X_r), …, c_p(E|X_r)) that the remark recalls from Tags 0ESW, 0FA7 and 0F9C; those are carried as a quantified family, the multiplication of A^*(X) — composition of bivariant classes, Tag 0FE0 — not being constructed in this library”.

The full Chern character ch(E) = (ch_0(E), ch_1(E), ch_2(E), …) of a finite locally free module whose rank need not be constant, as an element of the product ∏_{p ≥ 0} (A^p(X) ⊗ 𝐐).

def fullChernCharacter : fullRationalChowCohomology C G sX

Stacks.Chow.rationalCap_chernCharacterComponent_eq_zero_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/ChernCharacter.lean, line 257. The attribute's comment: “the vanishing of the components ch_p(E) for p above the dimension d of X, by Tag 0FDX, read on the test schemes of dimension at most d as the library's form of that tag allows; the splitting principle of the source is not needed, that form being a delta-dimension count, and neither is quasi-compactness of X”.

For d < p the class ch_p(E) caps every rational Chow class of a test scheme of dimension at most d to zero.

theorem rationalCap_chernCharacterComponent_eq_zero_of_topologicalKrullDim_le (d p : ℕ)
    (hp : d < p) {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g]
    (hT : topologicalKrullDim T ≤ (d : WithBot ℕ∞)) (k : ℤ)
    (α : chowGroup C (g ≫ sX) k) :
    rationalCap C G sX (p : ℤ) g k α
      (chernCharacterComponent C G sX E hgysO hgysR hgysC P p) = 0

Stacks.Chow.gradedChernCharacter_eq_fullChernCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/ChernCharacter.lean, line 334. The attribute's comment: “the membership ch(E) ∈ A^*(X) ⊗ 𝐐 for X of dimension at most d: the full Chern character is the image of the finite sum ⊕_{p ≤ d} ch_p(E). The vanishing of the components above d is a hypothesis: the library's Tag 0FDX reaches only the test schemes of dimension at most d, and by Tag 02UC the remaining ones are what the equality ch_p(E) = 0 in A^p(X) ⊗ 𝐐 needs. Quasi-compactness of X is not assumed, being unused by the library's form of Tag 0FDX”.

If the components of the Chern character vanish in the degrees above d, then the full Chern character lies in A^*(X) ⊗ 𝐐: it is the image of the finite sum ⊕_{p ≤ d} ch_p(E) under the inclusion of the direct sum into the product ∏_{p ≥ 0} (A^p(X) ⊗ 𝐐).

theorem gradedChernCharacter_eq_fullChernCharacter (d : ℕ)
    (hvan : ∀ p : ℕ, d < p →
      chernCharacterComponent C G sX E hgysO hgysR hgysC P p = 0) :
    (fun p : ℕ ↦ gradedChernCharacter C G sX E hgysO hgysR hgysC P d p) =
      fullChernCharacter C G sX E hgysO hgysR hgysC P

Stacks.Chow.moduleChernCharacter_apply_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/ChernCharacterLocallyFree.lean, line 392. The attribute's comment: “the components ch_p(E) = P_p(E)/p! ∈ A^p(X) ⊗ Q of the Chern character of a finite locally free module of not necessarily constant rank, with P_p of 0F9B evaluated at the rank and Chern classes of 0ESW (0FA7), so that ch(E) ∈ ∏_{p ≥ 0} (A^p(X) ⊗ Q)”.

Stacks 0ESX, the Chern character of a module of arbitrary rank. For a finite locally free module ℰ whose rank need not be constant, the Chern character ch(ℰ) = (ch_0(ℰ), ch_1(ℰ), …) ∈ ∏_{p ≥ 0} (A^p(X) ⊗ 𝐐) (Stacks.Chow.moduleChernCharacter) has components ch_p(ℰ) = P_p(ℰ)/p!, where P_p(ℰ) ∈ A^p(X) is the power sum of Stacks 0F9B (with P_0 = r) evaluated at the rank r(ℰ) and the Chern classes c_i(ℰ) of Stacks 0ESW, as in Stacks 0FA7.

theorem moduleChernCharacter_apply_eq (p : ℕ) :
    moduleChernCharacter C sX E p =
      ((Nat.factorial p : ℚ)⁻¹) ⊗ₜ[ℤ]
        chernPolynomialComponent C sX E p (powerSumChernPolynomial p)

Stacks.Chow.exists_gradedRationalChowCohomology_eq_moduleChernCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/ChernCharacterLocallyFree.lean, line 428. The attribute's comment: “for X quasi-compact with dim(X) < ∞, ch(E) ∈ A^*(X) ⊗ Q: the full Chern character is the image of an element of ⊕_p (A^p(X) ⊗ Q)”.

Stacks 0ESX, the finite-dimensional case. If X is quasi-compact and dim X < ∞, then ch(ℰ) ∈ A^*(X) ⊗ 𝐐: the full Chern character is the image of an element of the direct sum ⊕_{p ≥ 0} (A^p(X) ⊗ 𝐐) under its inclusion into the product.

theorem exists_gradedRationalChowCohomology_eq_moduleChernCharacter [CompactSpace X]
    (hdim : topologicalKrullDim X < ⊤) :
    ∃ y : gradedRationalChowCohomology C (gysinSystemOfInvertible C) sX,
      ∀ p : ℕ, y p = moduleChernCharacter C sX E p

Declarations registered for the tag:

Tag 0F9C, a lemma

Tag 0F9C in the Stacks Project.

Stacks.Chow.modulePowerSumComponentArbitraryRank_eq_add_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/BivariantPowerSumShortExact.lean, line 278. The attribute's comment: “the source's more precise equality P_p(E) = P_p(E_1) + P_p(E_2), stated where the source states it: IN A^p(X), the degree-p Chow cohomology of Tag 0B7E at the Gysin system of the first Chern class of an invertible module (Stacks.Chow.chowCohomologyComponent). A^*(X) = prod_{q >= 0} A^q(X) is the RING Stacks.Chow.TotalChowClass, whose product is the Cauchy product of the compositions A^i(X) x A^j(X) -> A^{i+j}(X) of Tag 0B75 (Stacks.Chow.TotalChowClass.instRing), so a polynomial in the Chern classes of a module is itself a bivariant class here; the Chern classes are the bivariant classes of Tag 0B7H, Stacks.Chow.GenuineChern.chernClass, assembled into Stacks.Chow.totalChern. P_p is CONSTRUCTED, by the Newton recurrence of Tag 0F9B (AlgebraicGeometry.newtonPowerSum) applied to the homogeneous components of the total Chern class with the rank as degree-zero term, so P_0(E) is the rank as in the source's recursion. THE RANKS ARE ARBITRARY, exactly as in the source: only that the three terms are finite locally free is assumed, no rank is named, and the rank of a finite locally free module is locally constant, so X is decomposed into the open and closed loci where each rank is constant (Stacks.Chow.rankLocus) and the class is assembled over them by Tag 0FDZ as Stacks.Chow.modulePowerSumArbitraryRank; Stacks.Chow.res_modulePowerSumArbitraryRank_of_constantRank identifies its restriction along any morphism of constant rank with the constant-rank power sum there, and the identity is read on a decomposition refining the rank decompositions of E_1 and of E_2. No filtration and no splitting of the sequence is supposed: the pulled-back sequence stays short exact with no flatness, a short exact sequence with finite locally free quotient being locally split. The splitting principle of the source is used only through the two results of the chapter it proves, both available here with no extra hypotheses: Tag 02UI on total classes (Stacks.Chow.totalChern_shortExact) and the commutativity of Chern classes of Tag 02UA (Stacks.Chow.commute_homComponent_totalChern). PROVED HERE: that those two give the additivity of every power sum, which is Newton's identities read as the single equation c . nu(c) = D(c) for the derivation D multiplying the index-m component by m”.

Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S and let 0 ⟶ ℰ₁ ⟶ ℰ ⟶ ℰ₂ ⟶ 0 be a short exact sequence of finite locally free 𝒪_X-modules. Then for every p

P_p(ℰ) = P_p(ℰ₁) + P_p(ℰ₂) in A^p(X),

where P_p is the universal power-sum polynomial of Stacks 0F9B evaluated at the Chern classes. No constancy of the ranks is assumed.

theorem modulePowerSumComponentArbitraryRank_eq_add_of_shortExact (p : ℕ) :
    modulePowerSumComponentArbitraryRank C sX S.X₂ p =
      modulePowerSumComponentArbitraryRank C sX S.X₁ p +
        modulePowerSumComponentArbitraryRank C sX S.X₃ p

Stacks.Chow.moduleChernCharacter_eq_add_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/BivariantPowerSumShortExact.lean, line 325. The attribute's comment: “the headline equality ch(E) = ch(E_1) + ch(E_2) for a short exact sequence 0 -> E_1 -> E -> E_2 -> 0 of finite locally free O_X-modules over X locally of finite type over the base of Situation 02QL. THE RANKS ARE ARBITRARY, exactly as in the source: only that the three terms are finite locally free is assumed and no rank is named. ch_p(F) = P_p(F)/p! is Stacks.Chow.moduleChernCharacterComponent, an element of A^p(X) tensor Q (Stacks.Chow.rationalChowCohomologyComponent) where A^p(X) is the degree-p Chow cohomology of Tag 0B7E -- the RATIONAL BIVARIANT group, not a ring of cap operators; the integral identity it is divided by holds in A^p(X) itself, in the bivariant ring A^*(X) = Stacks.Chow.TotalChowClass. ch(F) itself is Stacks.Chow.moduleChernCharacter, the family (ch_0(F), ch_1(F), ...) in the product prod_{p >= 0} (A^p(X) tensor Q), which is the home Tag 0ESX gives the Chern character, the degree in which it is concentrated being governed by a rank that is unbounded in general; addition there is degreewise, so an equality of two such families is an equality of Chern characters read in every degree at once, and Stacks.Chow.moduleChernCharacterComponent_eq_add_of_shortExact is that reading. It is derived from the source's more precise equality, Stacks.Chow.modulePowerSumComponentArbitraryRank_eq_add_of_shortExact, by dividing by p!: the division of a sum by a scalar is term by term, so unlike Tag 0F9D no binomial coefficient intervenes. The splitting principle is NOT redone here; it enters only through Tag 02UI on total classes (Stacks.Chow.totalChern_shortExact) and the commutativity of Chern classes of Tag 02UA”.

Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S and let 0 ⟶ ℰ₁ ⟶ ℰ ⟶ ℰ₂ ⟶ 0 be a short exact sequence of finite locally free 𝒪_X-modules. Then

ch(ℰ) = ch(ℰ₁) + ch(ℰ₂).

Both sides lie in ∏_{p ≥ 0} (A^p(X) ⊗ 𝐐), the rational Chow cohomology of X in which Stacks 0ESX places the Chern character.

theorem moduleChernCharacter_eq_add_of_shortExact :
    moduleChernCharacter C sX S.X₂ =
      moduleChernCharacter C sX S.X₁ + moduleChernCharacter C sX S.X₃

Stacks.Chow.powerSumOfFiniteLocallyFree_eq_add_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PowerSumComplex.lean, line 244. The attribute's comment: “the precise form: P_p(E) = P_p(E_1) + P_p(E_2) in A^p(X), for every p >= 0, for a short exact sequence of finite locally free modules of arbitrary ranks; P_p is the polynomial of Stacks 0F9B in the Chern classes of Stacks 0B7H, assembled over the rank loci (Stacks 0ESW, 0FA7)”.

Stacks 0F9C. For a short exact sequence 0 ⟶ ℰ₁ ⟶ ℰ ⟶ ℰ₂ ⟶ 0 of finite locally free 𝒪_X-modules, of ranks that need not be constant, P_p(ℰ) = P_p(ℰ₁) + P_p(ℰ₂) for every p.

theorem powerSumOfFiniteLocallyFree_eq_add_of_shortExact (S : ShortComplex X.Modules)
    (hS : S.ShortExact) [h₁ : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} S.X₁]
    [h₃ : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} S.X₃] (p : ℕ) :
    haveI := GenuineChern.isFiniteLocallyFree_of_shortExact S hS h₁ h₃
    powerSumOfFiniteLocallyFree C sX S.X₂ p =
      powerSumOfFiniteLocallyFree C sX S.X₁ p + powerSumOfFiniteLocallyFree C sX S.X₃ p

Stacks.Chow.chernCharacterOfFiniteLocallyFree_eq_add_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PowerSumComplex.lean, line 284. The attribute's comment: “ch(E) = ch(E_1) + ch(E_2), read in every degree p as ch_p = P_p/p! in A^p(X) ⊗ Q, for a short exact sequence of finite locally free modules of arbitrary ranks”.

Stacks 0F9C for the Chern character: ch(ℰ) = ch(ℰ₁) + ch(ℰ₂), degree by degree, for a short exact sequence of finite locally free modules of arbitrary ranks.

theorem chernCharacterOfFiniteLocallyFree_eq_add_of_shortExact (S : ShortComplex X.Modules)
    (hS : S.ShortExact) [h₁ : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} S.X₁]
    [h₃ : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} S.X₃] (p : ℕ) :
    haveI := GenuineChern.isFiniteLocallyFree_of_shortExact S hS h₁ h₃
    chernCharacterOfFiniteLocallyFree C sX S.X₂ p =
      chernCharacterOfFiniteLocallyFree C sX S.X₁ p +
        chernCharacterOfFiniteLocallyFree C sX S.X₃ p

Stacks.Chow.powerSumCap_append, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/PowerSumCapProducts.lean, line 335. The attribute's comment: “componentwise on cap products, and conditional. CORRECTION OF FORM: the source states P_p(E) = P_p(E_1) + P_p(E_2) in A^p(X) for a short exact sequence 0 -> E_1 -> E -> E_2 -> 0 of finite locally free O_X-modules, and ch(E) = ch(E_1) + ch(E_2) after dividing by p!. There is no bivariant ring here, so the identity is read degree by degree against a fixed cycle: for every n, every alpha in CycleGroup C p n and every p >= 0, P_p(E) cap alpha = P_p(E_1) cap alpha + P_p(E_2) cap alpha in A_{n-p}(X), each product of Chern classes being a COMPOSITE of operations on Chow groups, as Stacks 0FA6 reads c_1(F)^2. The module documentation gives both reasons. The division by p! is omitted only because it is a scalar. CARRIED: the three filtrations with invertible quotients L_i, N_j, M_k, Stacks 02TI for each quotient (hfacL, hfacN, hfacM), and hsub, hquot identifying the M_k with the L_i followed by the N_j -- the source's reduction of the short exact sequence, which it gets from Stacks 02UL and the injectivity of pi^* and which cannot be performed here. The Stacks 02UJ data needed to read the operator as P_p of the Chern classes of the module itself is carried not here but by Stacks.Chow.powerSumCap_one_eq_chernClassCapExt and Stacks.Chow.chernClassCapExt_one_append. PROVED HERE: the formal computation the source omits, in every degree and for every pair of ranks, as Stacks.Chow.powerSumRec_append; no commutativity is used, so Stacks 02TJ is not carried”.

Stacks 0F9C, componentwise on cap products. Let 0 → ℰ₁ → ℰ → ℰ₂ → 0 be a short exact sequence of finite locally free 𝒪_X-modules, ℰ₁ of rank r with a filtration whose successive quotients are the invertible modules ℒ_i = L i, ℰ₂ of rank s with quotients 𝒩_j = N j, and ℰ of rank r + s with the filtration obtained by juxtaposing them, whose quotients ℳ_k are the ℒ_i followed by the 𝒩_j. Then for every n-cycle α and every p ≥ 0

P_p(ℰ) ∩ α = P_p(ℰ₁) ∩ α + P_p(ℰ₂) ∩ α

in A_{n-p}(X), which is the identity P_p(ℰ) = P_p(ℰ₁) + P_p(ℰ₂) of the source read against α, and ch(ℰ) = ch(ℰ₁) + ch(ℰ₂) after dividing by p!. In degree one it is c₁(ℰ) ∩ α = c₁(ℰ₁) ∩ α + c₁(ℰ₂) ∩ α, which is Stacks.Chow.chernClassCapExt_one_append; in degree zero it is r + s = r + s.

theorem powerSumCap_append (hsub : ∀ i : Fin r, M (Fin.castAdd s i) ≅ L i)
    (hquot : ∀ j : Fin s, M (Fin.natAdd r j) ≅ N j) (k : ℕ) (α : chowGroup C p n) :
    powerSumCap C p n M hfacM k α
      = powerSumCap C p n L hfacL k α + powerSumCap C p n N hfacN k α

Stacks.Chow.chernClassCapExt_one_append, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/PowerSumCapProducts.lean, line 368. The attribute's comment: “the degree-one case, entirely in Chern class cap products, and conditional. P_1 being c_1 (AlgebraicGeometry.coe_powerSumPolynomial_one), the identity P_p(E) = P_p(E_1) + P_p(E_2) reads c_1(E) cap alpha = c_1(E_1) cap alpha + c_1(E_2) cap alpha in A_{n-1}(X), for every n and every alpha in CycleGroup C p n, where E_1, E, E_2 are the tops of the three filtrations and the three terms are the cap products of Stacks 02U5 on those modules themselves. Read degree by degree for the reason given on Stacks.Chow.powerSumCap_append, of which this is the degree-one case and whose reduction it carries: the three filtrations as the towers Stacks 02UJ consumes, with hsub and hquot. ALSO CARRIED, each an input of Stacks 02UJ itself: chernE, chern1, chern2, the Stacks 02U0 component data; hnormE, hnorm1, hnorm2, the Stacks 02U0 normalisation c_0 = 1 along each tower; hbinomE, hbinom1, hbinom2, the equality of binomial transforms that Stacks 02UD gives once Stacks 02UG is applied; and hfacL, hfacN, hfacM, Stacks 02TI for c_1 of each quotient. Stacks 02TJ is NOT carried: the degree-one computation needs no commutativity”.

Stacks 0F9C in degree one, entirely in Chern class cap products. In the situation of Stacks.Chow.powerSumCap_append, with ℰ₁ = Q₁ r, ℰ₂ = Q₂ s and ℰ = Q (r + s) the tops of the three filtrations, for every n-cycle α

c₁(ℰ) ∩ α = c₁(ℰ₁) ∩ α + c₁(ℰ₂) ∩ α

in A_{n-1}(X). This is the degree-one case of Stacks 0F9C, P_1 being c_1, with no power-sum operator left in the statement: the three terms are the Chern class cap products of Stacks 02U5 on the three modules themselves.

Each of the three sides is rewritten into its power-sum form by Stacks.Chow.powerSumCap_one_eq_chernClassCapExt, which is Stacks 02UJ in degree one, and the identity is then Stacks.Chow.powerSumCap_append in degree one.

theorem chernClassCapExt_one_append (hsub : ∀ i : Fin r, M (Fin.castAdd s i) ≅ L i)
    (hquot : ∀ j : Fin s, M (Fin.natAdd r j) ≅ N j)
    (QE : ℕ → X.Modules) (subE : ∀ k : Fin (r + s), M k ⟶ QE ((k : ℕ) + 1))
    (projE : ∀ k : Fin (r + s), QE ((k : ℕ) + 1) ⟶ QE (k : ℕ))
    (hzeroE : ∀ k : Fin (r + s), subE k ≫ projE k = 0)
    (hexactE : ∀ k : Fin (r + s), (ShortComplex.mk (subE k) (projE k) (hzeroE k)).ShortExact)
    (hrankE : ∀ m : ℕ, m ≤ r + s → PullbackPreservesRank (QE m) m)
    (chernE : ∀ m : ℕ, ChernClassCycleRule C m)
    (Q₁ : ℕ → X.Modules) (sub₁ : ∀ i : Fin r, L i ⟶ Q₁ ((i : ℕ) + 1))
    (proj₁ : ∀ i : Fin r, Q₁ ((i : ℕ) + 1) ⟶ Q₁ (i : ℕ))
    (hzero₁ : ∀ i : Fin r, sub₁ i ≫ proj₁ i = 0)
    (hexact₁ : ∀ i : Fin r, (ShortComplex.mk (sub₁ i) (proj₁ i) (hzero₁ i)).ShortExact)
    (hrank₁ : ∀ m : ℕ, m ≤ r → PullbackPreservesRank (Q₁ m) m)
    (chern₁ : ∀ m : ℕ, ChernClassCycleRule C m)
    (Q₂ : ℕ → X.Modules) (sub₂ : ∀ j : Fin s, N j ⟶ Q₂ ((j : ℕ) + 1))
    (proj₂ : ∀ j : Fin s, Q₂ ((j : ℕ) + 1) ⟶ Q₂ (j : ℕ))
    (hzero₂ : ∀ j : Fin s, sub₂ j ≫ proj₂ j = 0)
    (hexact₂ : ∀ j : Fin s, (ShortComplex.mk (sub₂ j) (proj₂ j) (hzero₂ j)).ShortExact)
    (hrank₂ : ∀ m : ℕ, m ≤ s → PullbackPreservesRank (Q₂ m) m)
    (chern₂ : ∀ m : ℕ, ChernClassCycleRule C m) (α : CycleGroup C p n)
    (hnormE : ∀ (m : ℕ) (hm : m ≤ r + s),
      chernClassCapExt C p n (QE m) m (hrankE m hm) (chernE m) 0 α =
        cycleClassDegreeZero C p n α)
    (hbinomE : ∀ k : Fin (r + s), ∀ i ≤ (k : ℕ) + 1,
      binomialTransform (inverseFirstChernCapStep C p n (M k) (hfacM k)) ((k : ℕ) + 1)
          (chernCapFamily C p n (QE ((k : ℕ) + 1)) ((k : ℕ) + 1) (hrankE ((k : ℕ) + 1) k.isLt)
            (chernE ((k : ℕ) + 1)) α) i =
        binomialTransform (inverseFirstChernCapStep C p n (M k) (hfacM k)) (k : ℕ)
          (chernCapFamily C p n (QE (k : ℕ)) (k : ℕ) (hrankE (k : ℕ) k.isLt.le)
            (chernE (k : ℕ)) α) i)
    (hnorm₁ : ∀ (m : ℕ) (hm : m ≤ r),
      chernClassCapExt C p n (Q₁ m) m (hrank₁ m hm) (chern₁ m) 0 α =
        cycleClassDegreeZero C p n α)
    (hbinom₁ : ∀ i : Fin r, ∀ t ≤ (i : ℕ) + 1,
      binomialTransform (inverseFirstChernCapStep C p n (L i) (hfacL i)) ((i : ℕ) + 1)
          (chernCapFamily C p n (Q₁ ((i : ℕ) + 1)) ((i : ℕ) + 1) (hrank₁ ((i : ℕ) + 1) i.isLt)
            (chern₁ ((i : ℕ) + 1)) α) t =
        binomialTransform (inverseFirstChernCapStep C p n (L i) (hfacL i)) (i : ℕ)
          (chernCapFamily C p n (Q₁ (i : ℕ)) (i : ℕ) (hrank₁ (i : ℕ) i.isLt.le)
            (chern₁ (i : ℕ)) α) t)
    (hnorm₂ : ∀ (m : ℕ) (hm : m ≤ s),
      chernClassCapExt C p n (Q₂ m) m (hrank₂ m hm) (chern₂ m) 0 α =
        cycleClassDegreeZero C p n α)
    (hbinom₂ : ∀ j : Fin s, ∀ t ≤ (j : ℕ) + 1,
      binomialTransform (inverseFirstChernCapStep C p n (N j) (hfacN j)) ((j : ℕ) + 1)
          (chernCapFamily C p n (Q₂ ((j : ℕ) + 1)) ((j : ℕ) + 1) (hrank₂ ((j : ℕ) + 1) j.isLt)
            (chern₂ ((j : ℕ) + 1)) α) t =
        binomialTransform (inverseFirstChernCapStep C p n (N j) (hfacN j)) (j : ℕ)
          (chernCapFamily C p n (Q₂ (j : ℕ)) (j : ℕ) (hrank₂ (j : ℕ) j.isLt.le)
            (chern₂ (j : ℕ)) α) t) :
    chernClassCapExt C p n (QE (r + s)) (r + s) (hrankE (r + s) le_rfl) (chernE (r + s)) 1 α
      = chernClassCapExt C p n (Q₁ r) r (hrank₁ r le_rfl) (chern₁ r) 1 α
        + chernClassCapExt C p n (Q₂ s) s (hrank₂ s le_rfl) (chern₂ s) 1 α
Tag 0F9D, a lemma

Tag 0F9D in the Stacks Project.

Stacks.Chow.totalChernCharacterArbitraryRank_tensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/BivariantChernCharacter.lean, line 186. The attribute's comment: “the headline equality ch(E_1 tensor E_2) = ch(E_1) ch(E_2), with hypotheses EXACTLY the source's: Situation 02QL as the ChowSituation C, X locally of finite type over its base, and E_1, E_2 finite locally free O_X-modules -- NO rank is assumed, the predicate being AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree and not ...OfRank. The equality IS read in A^*(X) tensor Q: Stacks.Chow.rationalTotalChowClass is the ring Stacks.Chow.TotalChowClass of total Chow cohomology classes -- the product over q >= 0 of the groups A^q(X) of Stacks 0B7E, whose multiplication is the Cauchy product of the compositions of bivariant classes of Stacks 0B75 -- tensored over Z with Q so that p! is invertible, so each product ch_{p_1}(E_1) ch_{p_2}(E_2) is a composition of bivariant classes with rational coefficients. ch_p(F) = P_p(F)/p! is Stacks.Chow.chernCharacterComponentArbitraryRank and ch(F) itself is Stacks.Chow.totalChernCharacterArbitraryRank, the formal power series whose degree-p coefficient is ch_p(F): PowerSeries A is the product over p of copies of A under convolution, which is the home Stacks 0ESX gives the Chern character, the rank of F being unbounded, so an equality of these series is an equality of Chern characters in every degree at once and Stacks.Chow.chernCharacterComponentArbitraryRank_tensorObj is that reading. It is derived from the source's more precise equality, Stacks.Chow.modulePowerSumArbitraryRank_tensorObj, by dividing by p!: the binomial coefficient disappears because C(p, p_1)/p! = 1/(p_1! p_2!) when p_1 + p_2 = p, which is Nat.add_choose_mul_factorial_mul_factorial. The rank decomposition and the splitting principle are PERFORMED by the cited theorem, not supposed; see its note”.

Stacks 0F9D, the headline identity. Let (S, δ) be the situation of Stacks 02QL, let X be locally of finite type over S and let ℰ₁ and ℰ₂ be finite locally free 𝒪_X-modules, of no assumed rank. Then

ch(ℰ₁ ⊗_{𝒪_X} ℰ₂) = ch(ℰ₁) ch(ℰ₂).

Both sides are power series over the rational bivariant ring A^*(X) ⊗ 𝐐 whose degree-p coefficient is ch_p = P_p/p!; multiplying two such series convolves their coefficients, so this single identity is Stacks.Chow.chernCharacterComponentArbitraryRank_tensorObj in every degree at once, and that in turn is Stacks.Chow.modulePowerSumArbitraryRank_tensorObj divided by p!.

theorem totalChernCharacterArbitraryRank_tensorObj :
    totalChernCharacterArbitraryRank C sX (Scheme.Modules.tensorObj E₁ E₂)
      = totalChernCharacterArbitraryRank C sX E₁ * totalChernCharacterArbitraryRank C sX E₂

Stacks.Chow.modulePowerSumArbitraryRank_tensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/BivariantTensorPowerSum.lean, line 228. The attribute's comment: “the source's more precise identity P_p(E_1 tensor E_2) = sum over p_1 + p_2 = p of binom(p, p_1) P_{p_1}(E_1) P_{p_2}(E_2), with hypotheses EXACTLY the source's: Situation 02QL as the ChowSituation C, X locally of finite type over its base, and E_1, E_2 finite locally free O_X-modules -- NO rank is assumed, the predicate being AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree and not ...OfRank. The identity is read IN THE BIVARIANT RING: Stacks.Chow.TotalChowClass is the product over q >= 0 of the Chow cohomology groups A^q(X) of Stacks 0B7E, whose multiplication is the Cauchy product of the composites of bivariant classes of Stacks 0B75 and whose unit is the identity class of Stacks 0FBS, so each product P_{p_1}(E_1) P_{p_2}(E_2) is a composition of bivariant classes and not a composite of cap operators; Stacks.Chow.modulePowerSumComponentArbitraryRank_tensorObj reads the same identity in the single group A^p(X). P_p(F) is Stacks.Chow.modulePowerSumArbitraryRank, Newton's recursion of Stacks 0F9B (AlgebraicGeometry.newtonPowerSum, which is the universal power-sum polynomial of that tag by AlgebraicGeometry.newtonPowerSum_eq_powerSumOfChernClasses) applied to the bivariant Chern classes c_i(F) of Stacks 0B7H, Stacks.Chow.GenuineChern.chernClass, assembled over the rank loci of F by Stacks 0FDZ. THE RANK DECOMPOSITION IS PERFORMED, not assumed: the rank of a finite locally free module is locally constant (Stacks.Chow.moduleRank), its loci are open and closed and cover X (Stacks.Chow.isClopenDecomposition_rankLociFamily), the identity for two modules is read on the common refinement of their two decompositions (Stacks.Chow.eq_of_res_eq_of_constantModuleRanks), on a member of which E_1 tensor E_2 has constant rank r * s by Stacks 02U9, and restriction of total classes is a ring homomorphism. The constant-rank case is Stacks.Chow.modulePowerSum_tensorObj, obtained from Stacks.Chow.powerSumChernElem_tensorObj -- where the splitting principle of Stacks 02UL is performed -- read on EVERY test scheme g : T -> X for the pullbacks g^E_1, g^E_2 at once, which is what Stacks 0B76 needs for a bivariant class. The division by p! is omitted only because it is a scalar; Stacks.Chow.totalChernCharacterArbitraryRank_tensorObj performs it”.

Stacks 0F9D, the source's more precise identity, in the bivariant ring. Let (S, δ) be the situation of Stacks 02QL, let X be locally of finite type over S and let ℰ₁ and ℰ₂ be finite locally free 𝒪_X-modules, of no assumed rank. Then for every p ≥ 0

P_p(ℰ₁ ⊗_{𝒪_X} ℰ₂) = ∑_{p₁ + p₂ = p} C(p, p₁) P_{p₁}(ℰ₁) P_{p₂}(ℰ₂)

in ∏_{q ≥ 0} A^q(X), the bivariant ring of X, whose multiplication is the composition of bivariant classes of Stacks 0B75. In degree zero the identity reads rk(ℰ₁ ⊗ ℰ₂) = rk(ℰ₁) rk(ℰ₂) and in degree one c₁(ℰ₁ ⊗ ℰ₂) = rk(ℰ₂) c₁(ℰ₁) + rk(ℰ₁) c₁(ℰ₂), both as locally constant functions on X.

theorem modulePowerSumArbitraryRank_tensorObj (p : ℕ) :
    modulePowerSumArbitraryRank C sX (Scheme.Modules.tensorObj E₁ E₂) p
      = ∑ q ∈ Finset.HasAntidiagonal.antidiagonal p,
          (p.choose q.1 : TotalChowClass C sX) *
            (modulePowerSumArbitraryRank C sX E₁ q.1 *
              modulePowerSumArbitraryRank C sX E₂ q.2)

Stacks.Chow.modulePowerSumComponentArbitraryRank_tensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/BivariantTensorPowerSum.lean, line 278. The attribute's comment: “the same identity P_p(E_1 tensor E_2) = sum over p_1 + p_2 = p of binom(p, p_1) P_{p_1}(E_1) P_{p_2}(E_2) read as an equality of two elements of the SINGLE GROUP A^p(X) = Stacks.Chow.chowCohomologyComponent of Stacks 0B7E at the Gysin system Stacks.Chow.gysinSystemOfInvertible of the genuine first Chern class, which is where the source states it. Hypotheses EXACTLY the source's: Situation 02QL as C, X locally of finite type over its base, E_1 and E_2 finite locally free with NO rank assumed. Each product on the right is formed in the bivariant ring Stacks.Chow.TotalChowClass, i.e. is a Cauchy product of the compositions of bivariant classes of Stacks 0B75, read in degree p, so the right-hand side is a sum over the antidiagonal of p of elements of A^p(X), which is the shape the source displays; the degree-p component of Stacks.Chow.modulePowerSumArbitraryRank is Stacks.Chow.modulePowerSumComponentArbitraryRank by definition. See Stacks.Chow.modulePowerSumArbitraryRank_tensorObj for the same identity in every degree at once and for how the rank decomposition and the splitting principle are performed”.

Stacks 0F9D, the source's more precise identity, read in A^p(X). An equality of two elements of the Chow cohomology group A^p(X) of Stacks 0B7E: the class P_p(ℰ₁ ⊗ ℰ₂) is the sum over p₁ + p₂ = p of the classes C(p, p₁) P_{p₁}(ℰ₁) P_{p₂}(ℰ₂) of A^p(X), each formed by the composition of bivariant classes of Stacks 0B75 inside the bivariant ring and read in degree p. This is Stacks.Chow.modulePowerSumArbitraryRank_tensorObj in degree p, the components of a finite sum of total classes being the sum of their components.

theorem modulePowerSumComponentArbitraryRank_tensorObj (p : ℕ) :
    modulePowerSumComponentArbitraryRank C sX (Scheme.Modules.tensorObj E₁ E₂) p
      = ∑ q ∈ Finset.HasAntidiagonal.antidiagonal p,
          ((p.choose q.1 : TotalChowClass C sX) *
            (modulePowerSumArbitraryRank C sX E₁ q.1 *
              modulePowerSumArbitraryRank C sX E₂ q.2)) p

Stacks.Chow.powerSumOfFiniteLocallyFree_sheafTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PowerSumTensor.lean, line 68. The attribute's comment: “the lemma as stated, for finite locally free E_1, E_2 of arbitrary ranks and every p >= 0, with no further hypothesis: P_p(E_1 tensor E_2) = sum over p_1 + p_2 = p of C(p, p_1) P_{p_1}(E_1) P_{p_2}(E_2), in the ring TotalChowClass C sX of total Chow cohomology classes (whose degree-p component is A^p(X)); P_p is the power sum of Stacks 0F9B assembled over the rank loci, powerSumOfFiniteLocallyFree. The form ch(E_1 tensor E_2) = ch(E_1) ch(E_2) is Stacks.Chow.chernCharacterOfModule_sheafTensor”.

Stacks 0F9D. For finite locally free 𝒪_X-modules ℰ and ℱ, of arbitrary ranks,

P_p(ℰ ⊗ ℱ) = ∑_{p₁ + p₂ = p} C(p, p₁) · P_{p₁}(ℰ) · P_{p₂}(ℱ)

in the ring of total Chow cohomology classes of X, for every p ≥ 0. Along a morphism over which both modules have constant rank this is Stacks.Chow.powerSumTotal_sheafTensor, and such morphisms detect total classes (Stacks.Chow.TotalChowClass.eq_of_res_eq_of_constantRank₂).

theorem powerSumOfFiniteLocallyFree_sheafTensor (p : ℕ) :
    haveI : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (R := X.ringCatSheaf) _ :=
        isFiniteLocallyFree_tensor hE hF
    powerSumOfFiniteLocallyFree C sX (((sheafTensor X.sheaf).obj E).obj F) p =
      ∑ q ∈ antidiagonal p, (p.choose q.1 : ℤ) •
        (powerSumOfFiniteLocallyFree C sX E q.1 * powerSumOfFiniteLocallyFree C sX F q.2)

Stacks.Chow.rationalTotalChernCharacter_sheafTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/ChernCharacterMultiplicative.lean, line 138. The attribute's comment: “the Chern character form ch(E_1 tensor E_2) = ch(E_1) ch(E_2), for finite locally free E_1, E_2 of arbitrary ranks, with no further hypothesis, in the ring Stacks.Chow.RationalTotalChowClass C sX = prod over p >= 0 of A^p(X) tensor Q with its Cauchy product; ch(E) is the family of the ch_p(E) = P_p(E)/p!”.

Stacks 0F9D for the Chern character: ch(ℰ ⊗ ℱ) = ch(ℰ) · ch(ℱ) in ∏_{p ≥ 0} A^p(X) ⊗ 𝐐, for finite locally free modules of arbitrary ranks.

In degree m both sides are computed on the lifts ∑_{p ≤ m} P_p/p! of the two Chern characters to 𝐐 ⊗ ∏_q A^q(X) (Stacks.Chow.RationalTotalChowClass.mul_apply_eq); P_p(ℰ) P_q(ℱ) is homogeneous of degree p + q, and the identity is Stacks.Chow.powerSumOfFiniteLocallyFree_sheafTensor divided by m!.

theorem rationalTotalChernCharacter_sheafTensor :
    haveI : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (R := X.ringCatSheaf) _ :=
        isFiniteLocallyFree_tensor hE hF
    rationalTotalChernCharacter C sX (((sheafTensor X.sheaf).obj E).obj F) =
      rationalTotalChernCharacter C sX E * rationalTotalChernCharacter C sX F

Stacks.Chow.powerSumCap_lexFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/PowerSumCapProducts.lean, line 493. The attribute's comment: “componentwise on cap products, and conditional. CORRECTION OF FORM: the source states P_p(E_1 tensor E_2) = sum over p_1 + p_2 = p of C(p, p_1) P_{p_1}(E_1) P_{p_2}(E_2) in A^p(X), and ch(E_1 tensor E_2) = ch(E_1) ch(E_2) after dividing by p!. There is no bivariant ring here, so the identity is read degree by degree against a fixed cycle, in A_{n-p}(X) for every n, every alpha in CycleGroup C p n and every p >= 0; every product of classes -- P_{p_1}(E_1) P_{p_2}(E_2) and the products inside each P_p -- is a COMPOSITE of operations on Chow groups, as Stacks 0FA6 reads c_1(F)^2. The module documentation gives both reasons. The division by p! is omitted only because it is a scalar. CARRIED: the three filtrations with invertible quotients, Stacks 02TI for each quotient (hfacL, hfacN, hfacM), and hquot, the source's lexicographic identification M_{is+j} iso L_i tensor N_j, which the source gets from Stacks 02UL and the injectivity of pi^ and which cannot be performed here; and Stacks 02TJ as hcommLN, genuinely needed because the binomial theorem applies to x_i + y_j only when those commute -- the members of one family need NOT commute among themselves, so hcommLL and hcommNN are not carried. Reading the operator as P_p of the Chern classes of the module itself uses the Stacks 02UJ data, carried by Stacks.Chow.powerSumCap_one_eq_chernClassCapExt. PROVED HERE: the formal computation the source omits, in every degree and for every pair of ranks, as Stacks.Chow.powerSumRec_lexFamily”.

Stacks 0F9D, componentwise on cap products. Let ℰ₁ be finite locally free of rank r with a filtration whose successive quotients are the invertible modules ℒ_i = L i, let ℰ₂ be finite locally free of rank s with quotients 𝒩_j = N j, and let the filtration of ℰ₁ ⊗_{𝒪_X} ℰ₂ be the lexicographic one of the source, of length r·s, whose (i·s+j)-th quotient is ℒ_i ⊗ 𝒩_j. Then for every n-cycle α and every p ≥ 0

P_p(ℰ₁ ⊗ ℰ₂) ∩ α = ∑_{p₁ + p₂ = p} C(p, p₁) · (P_{p₁}(ℰ₁) ∘ P_{p₂}(ℰ₂)) ∩ α

in A_{n-p}(X), which is the identity P_p(ℰ₁ ⊗ ℰ₂) = ∑_{p₁+p₂=p} C(p,p₁) P_{p₁}(ℰ₁) P_{p₂}(ℰ₂) of the source read against α, and ch(ℰ₁ ⊗ ℰ₂) = ch(ℰ₁) · ch(ℰ₂) after dividing by p!, the binomial coefficients being what p! = p₁! · p₂! · C(p, p₁) absorbs. Each product P_{p₁}(ℰ₁) · P_{p₂}(ℰ₂) is a composite of operations on Chow groups, as c₁(ℱ)² is in Stacks 0FA6. In degree one, P_0 being the rank, the identity is s·(c₁(ℰ₁) ∩ α) + r·(c₁(ℰ₂) ∩ α), the first displayed identity of Stacks 0FA6.

theorem powerSumCap_lexFamily
    (hquot : ∀ (i : Fin r) (j : Fin s),
      M (finLexIndex i j) ≅ Scheme.Modules.tensorObj (L i) (N j))
    (hcommLN : ∀ (a : Fin r) (b : Fin s),
      FirstChernCapStepsCommute C p n (L a) (N b) (hfacL a) (hfacN b))
    (k : ℕ) (α : chowGroup C p n) :
    powerSumCap C p n M hfacM k α
      = ∑ q ∈ Finset.antidiagonal k, k.choose q.1 •
          evalChowGraded C p n α k
            (powerSumShift C p n L hfacL q.1 * powerSumShift C p n N hfacN q.2)
Tag 0FAB, a lemma

Tag 0FAB in the Stacks Project.

Stacks.Chow.moduleChernCharacterComponent_dualSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/DualChernCharacter.lean, line 115. The attribute's comment: “ch_i(E^dual) = (-1)^i ch_i(E) in A^i(X) tensor Q for every i >= 0, X locally of finite type over the base of Situation 02QL and E a finite locally free O_X-module of arbitrary (not necessarily constant) rank, E^dual = SheafHom(E, O_X). ch_i(E) = P_i(E)/i! is Stacks.Chow.moduleChernCharacterComponent, built from the bivariant Chern classes of Tag 0B7H; the proof is Tag 0FA5 (Stacks.Chow.GenuineChern.chernClass_dualSheaf) on each rank locus. Nothing is carried.”.

Stacks 0FAB. Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S and let ℰ be a finite locally free 𝒪_X-module with dual ℰ^∨. Then

ch_i(ℰ^∨) = (-1)^i ch_i(ℰ) in A^i(X) ⊗ 𝐐

for every i ≥ 0.

theorem moduleChernCharacterComponent_dualSheaf (i : ℕ) :
    haveI := Stacks.AlgebraicGeometry.ReflexiveModules.isFiniteLocallyFree_dualSheaf E hE
    moduleChernCharacterComponent C sX (dualSheaf E) i =
      ((-1 : ℤ) ^ i) • moduleChernCharacterComponent C sX E i
Sources

Section42.46 Chern classes and the derived category#

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

Tag 0ESZ, a lemma

Tag 0ESZ in the Stacks Project.

Stacks.Chow.totalChernClassComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComplex.lean, line 554. The attribute's comment: “the total Chern class c(E^bullet) of a complex of finite locally free modules bounded in a range of degrees, with no constant-rank hypothesis; the total Chern class of a module, Tag 0B7H, and the multiplication of A^*(X), Tag 0FE0, are carried as the parameters R and D, whose field ch_shortExact is the Whitney sum formula of Tag 02UI, exactly as in Stacks.Chow.chernClassKGroup; the locally bounded case is not delivered”.

Stacks 0ESZ. The total Chern class c(ℰ^•) = ∏_n c(ℰ^n)^{(-1)^n} of a complex of finite locally free modules bounded in the degrees a, …, a + k, as an element of the group of series with constant term 1 inside ∏_{p ≥ 0} A^p(X); the negative exponents are the formal inverses of Stacks 0FEL. No rank is assumed constant.

def totalChernClassComplex (D : TotalChernClassSeries C Gy sX R)
    (P : CochainComplex X.Modules ℤ) (a : ℤ) (k : ℕ) : UnitalSeries R

Stacks.Chow.totalChernClassComplex_eq_prod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComplex.lean, line 563. The attribute's comment: “the defining formula c(E^bullet) = prod_n c(E^n)^{(-1)^n} of the section, the inverses being the formal inverses of Tag 0FEL”.

Stacks 0ESZ. The total Chern class of a complex is the alternating product ∏_n c(ℰ^n)^{(-1)^n} of the total Chern classes of its terms, which is the formula of the source.

theorem totalChernClassComplex_eq_prod (D : TotalChernClassSeries C Gy sX R)
    (P : CochainComplex X.Modules ℤ) (a : ℤ) (k : ℕ) :
    totalChernClassComplex C Gy sX D P a k =
      ∏ i ∈ Finset.range (k + 1),
        (⟨D.ch (P.X (a + (i : ℤ))), D.ch_apply_zero (P.X (a + (i : ℤ)))⟩ : UnitalSeries R) ^
          ((a + (i : ℤ)).negOnePow : ℤ)

Stacks.Chow.totalChernClassComplex_eq_of_cohomologyComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComplex.lean, line 582. The attribute's comment: “the independence of the representative for the total Chern class. CARRIED: the degreewise data the source's proof extracts from an isomorphism in D(O_X) -- finite local freeness of the kernels and images (Tag 0F8J), the identification of the cohomology modules, and Schanuel's lemma (Tag 00O3) -- together with the reductions of Tags 02UC and 0ESR”.

Stacks 0ESZ. The total Chern class of a complex of finite locally free modules depends only on the cohomology modules of the complex. Two complexes representing the same object of D(𝒪_X) have the same cohomology modules, and this is the form in which the independence of the representative is delivered here; see the implementation notes of this file.

theorem totalChernClassComplex_eq_of_cohomologyComparison (D : TotalChernClassSeries C Gy sX R)
    {P Q : CochainComplex X.Modules ℤ} {a : ℤ} {k : ℕ}
    (S : BoundedComplexSplitting X P a k) (T : BoundedComplexSplitting X Q a k)
    (cmp : ComplexCohomologyComparison S T) :
    totalChernClassComplex C Gy sX D P a k = totalChernClassComplex C Gy sX D Q a k

Stacks.Chow.powerSumClassComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComplex.lean, line 645. The attribute's comment: “the class P_p(E^bullet) of a complex of finite locally free modules bounded in a range of degrees, with no constant-rank hypothesis; the constant-rank power sums P_p(E) of Tag 0F9B and their additivity, Tag 0F9C, are carried as the parameter W, as in Stacks.Chow.powerSumClassArbitraryRank; the locally bounded case is not delivered”.

Stacks 0ESZ. The class P_p(ℰ^•) = ∑_n (-1)^n P_p(ℰ^n) ∈ A^p(X) of a complex of finite locally free modules bounded in the degrees a, …, a + k. No rank is assumed constant.

def powerSumClassComplex (W : PowerSumClassRule C Gy sX) (P : CochainComplex X.Modules ℤ)
    (a : ℤ) (k : ℕ) (p : ℕ) : chowCohomologyComponent C Gy sX (p : ℤ)

Stacks.Chow.powerSumClassComplex_eq_sum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComplex.lean, line 652. The attribute's comment: “the defining formula P_p(E^bullet) = sum_n (-1)^n P_p(E^n) of the section”.

Stacks 0ESZ. The class P_p of a complex is the alternating sum of the classes P_p of its terms, which is the formula of the source.

theorem powerSumClassComplex_eq_sum (W : PowerSumClassRule C Gy sX)
    (P : CochainComplex X.Modules ℤ) (a : ℤ) (k : ℕ) (p : ℕ) :
    powerSumClassComplex C Gy sX W P a k p =
      ∑ i ∈ Finset.range (k + 1),
        ((a + (i : ℤ)).negOnePow : ℤ) • W.cls (P.X (a + (i : ℤ))) p

Stacks.Chow.powerSumClassComplex_eq_of_cohomologyComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComplex.lean, line 669. The attribute's comment: “the independence of the representative for P_p. CARRIED: the degreewise data the source's proof extracts from an isomorphism in D(O_X) -- finite local freeness of the kernels and images (Tag 0F8J), the identification of the cohomology modules, and Schanuel's lemma (Tag 00O3) -- together with the reductions of Tags 02UC and 0ESR”.

Stacks 0ESZ. The class P_p of a complex of finite locally free modules depends only on the cohomology modules of the complex. Two complexes representing the same object of D(𝒪_X) have the same cohomology modules, and this is the form in which the independence of the representative is delivered here; see the implementation notes of this file.

theorem powerSumClassComplex_eq_of_cohomologyComparison (W : PowerSumClassRule C Gy sX)
    {P Q : CochainComplex X.Modules ℤ} {a : ℤ} {k : ℕ}
    (S : BoundedComplexSplitting X P a k) (T : BoundedComplexSplitting X Q a k)
    (cmp : ComplexCohomologyComparison S T) (p : ℕ) :
    powerSumClassComplex C Gy sX W P a k p = powerSumClassComplex C Gy sX W Q a k p

Stacks.Chow.chernCharacterComplexComponent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComplex.lean, line 683. The attribute's comment: “the Chern character component ch_p(E^bullet) = P_p(E^bullet)/p! of a complex of finite locally free modules bounded in a range of degrees, with no constant-rank hypothesis; the constant-rank power sums and their additivity, Tag 0F9C, are carried as the parameter W; the locally bounded case is not delivered”.

Stacks 0ESZ. The degree-p component ch_p(ℰ^•) = P_p(ℰ^•)/p! ∈ A^p(X) ⊗ 𝐐 of the Chern character of a complex of finite locally free modules bounded in the degrees a, …, a + k.

def chernCharacterComplexComponent (W : PowerSumClassRule C Gy sX)
    (P : CochainComplex X.Modules ℤ) (a : ℤ) (k : ℕ) (p : ℕ) :
    rationalChowCohomologyComponent C Gy sX (p : ℤ)

Stacks.Chow.chernCharacterComplexComponent_eq_of_cohomologyComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComplex.lean, line 696. The attribute's comment: “the independence of the representative for the Chern character. CARRIED: the degreewise data the source's proof extracts from an isomorphism in D(O_X) -- finite local freeness of the kernels and images (Tag 0F8J), the identification of the cohomology modules, and Schanuel's lemma (Tag 00O3) -- together with the reductions of Tags 02UC and 0ESR”.

Stacks 0ESZ. The Chern character of a complex of finite locally free modules depends only on the cohomology modules of the complex. Two complexes representing the same object of D(𝒪_X) have the same cohomology modules, and this is the form in which the independence of the representative is delivered here; see the implementation notes of this file.

theorem chernCharacterComplexComponent_eq_of_cohomologyComparison (W : PowerSumClassRule C Gy sX)
    {P Q : CochainComplex X.Modules ℤ} {a : ℤ} {k : ℕ}
    (S : BoundedComplexSplitting X P a k) (T : BoundedComplexSplitting X Q a k)
    (cmp : ComplexCohomologyComparison S T) (p : ℕ) :
    chernCharacterComplexComponent C Gy sX W P a k p =
      chernCharacterComplexComponent C Gy sX W Q a k p

Stacks.Chow.totalChernClassComplexLocallyBounded, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComplexLocallyBounded.lean, line 137. The attribute's comment: “the locally bounded case, on a quasi-compact scheme: the total Chern class of a locally bounded complex of finite locally free modules, which the bounded-window construction of this tag in Stacks.Chow.ChernClassComplex does not deliver; the total Chern class of a module (Tag 0B7H) and the multiplication of A^*(X) (Tag 0FE0) are carried as the parameters R and D exactly as there”.

Stacks 0ESZ. The total Chern class c(ℰ^•) = ∏_n c(ℰ^n)^{(-1)^n} of a locally bounded complex of finite locally free modules on a quasi-compact scheme, as an element of the group of series with constant term 1 inside ∏_{p ≥ 0} A^p(X). Such a complex vanishes outside a single global window of degrees, and the class is the bounded-window class of Stacks 0ESZ on one.

def totalChernClassComplexLocallyBounded (D : TotalChernClassSeries C Gy sX R)
    (P : CochainComplex X.Modules ℤ) (hP : IsLocallyBoundedFiniteLocallyFree P) :
    UnitalSeries R

Stacks.Chow.powerSumClassComplexLocallyBounded, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComplexLocallyBounded.lean, line 174. The attribute's comment: “the locally bounded case, on a quasi-compact scheme: the class P_p of a locally bounded complex of finite locally free modules, which the bounded-window construction of this tag in Stacks.Chow.ChernClassComplex does not deliver; the constant-rank power sums P_p(E) of Tag 0F9B and their additivity, Tag 0F9C, are carried as the parameter W exactly as there”.

Stacks 0ESZ. The class P_p(ℰ^•) = ∑_n (-1)^n P_p(ℰ^n) ∈ A^p(X) of a locally bounded complex of finite locally free modules on a quasi-compact scheme. Such a complex vanishes outside a single global window of degrees, and the class is the bounded-window class of Stacks 0ESZ on one.

def powerSumClassComplexLocallyBounded (W : PowerSumClassRule C Gy sX)
    (P : CochainComplex X.Modules ℤ) (hP : IsLocallyBoundedFiniteLocallyFree P) (p : ℕ) :
    chowCohomologyComponent C Gy sX (p : ℤ)

Stacks.Chow.complexChern, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/ComplexChernClass.lean, line 186. The attribute's comment: “the class c(E^bullet) in prod_{p >= 0} A^p(Y) of a locally bounded complex of finite locally free modules -- the generalization the lemma refers to: no rank is assumed constant, the complex is only locally bounded, and Y is not assumed quasi-compact”.

The total Chern class of a locally bounded complex of finite locally free modules. On the rank locus Y_ρ the complex is bounded with constant ranks ρ, and there the class is c(P|_{Y_ρ}) = ∏_n c(P^n|_{Y_ρ})^{(-1)^n}; these classes are assembled into a total class on Y by Stacks 0FDZ in every degree.

def complexChern : TotalChowClass C sY

Stacks.Chow.complexPowerSumComponent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DerivedChernClasses.lean, line 425. The attribute's comment: “the class P_p(E^bullet) in A^p(Y) of a locally bounded complex of finite locally free modules, as the universal power sum of Tag 0F9B applied to c(E^bullet) -- the degree-zero member being the alternating rank class”.

The class P_p(ℰ^•) ∈ A^p(Y), the degree-p component of Stacks.Chow.complexPowerSum.

def complexPowerSumComponent (p : ℕ) :
    chowCohomologyComponent C (gysinSystemOfInvertible C) sY (p : ℤ)

Stacks.Chow.complexChernCharacter, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DerivedChernClasses.lean, line 446. The attribute's comment: “the class ch(E^bullet) in prod_{p >= 0} (A^p(Y) tensor Q) of a locally bounded complex of finite locally free modules, componentwise as ch_p = P_p/p! as the source reads it”.

The Chern character ch(ℰ^•) ∈ ∏_{p ≥ 0} (A^p(Y) ⊗ 𝐐) of a locally bounded complex of finite locally free modules, the family of its components.

def complexChernCharacter : fullRationalChowCohomology C (gysinSystemOfInvertible C) sY

Stacks.Chow.complexPowerSumComponent_eq_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DerivedChernClasses.lean, line 478. The attribute's comment: “the independence of the choice of the complex for P_p(E^bullet) in A^p(Y)”.

Stacks 0ESZ for P_p ∈ A^p(Y).

theorem complexPowerSumComponent_eq_of_iso
    (e : DerivedCategory.Q.obj P ≅ DerivedCategory.Q.obj P') (p : ℕ) :
    complexPowerSumComponent C sY hP p = complexPowerSumComponent C sY hP' p

Stacks.Chow.complexChernCharacter_eq_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DerivedChernClasses.lean, line 497. The attribute's comment: “the independence of the choice of the complex for ch(E^bullet)”.

Stacks 0ESZ for the Chern character, as the family ch(ℰ^•) ∈ ∏_{p ≥ 0} (A^p(Y) ⊗ 𝐐).

theorem complexChernCharacter_eq_of_iso
    (e : DerivedCategory.Q.obj P ≅ DerivedCategory.Q.obj P') :
    complexChernCharacter C sY hP = complexChernCharacter C sY hP'

Stacks.Chow.complexChern_eq_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/Independence.lean, line 282. The attribute's comment: “the independence of the choice of the complex for c(E^bullet), at the hypotheses of the source: two locally bounded complexes of finite locally free modules representing one object of D(O_Y), no rank assumed constant and Y not assumed quasi-compact”.

Stacks 0ESZ for the total Chern class. Let Y be locally of finite type over the base of chapter 42 and let P, P' be locally bounded complexes of finite locally free 𝒪_Y-modules representing the same object of D(𝒪_Y). Then their total Chern classes c(P), c(P') ∈ ∏_{p ≥ 0} A^p(Y) are equal.

The proof is the source's. By Stacks 02UC it suffices to compare the operations of the two classes on the fundamental class of a proper birational modification of every integral scheme T locally of finite type over Y (Stacks.Chow.TotalChowClass.eq_of_op_fundamentalChowClass_eq). Over T the pulled-back complexes are bounded with constant ranks, after the admissible blowup of Stacks 0ESR the cohomology of the pulled-back object is perfect of Tor dimension at most one, and there the two classes agree by Stacks 0F8J, Schanuel's lemma and the Whitney sum formula (Stacks.Chow.exists_isBirational_op_complexChern_eq_of_iso).

theorem complexChern_eq_of_iso (e : DerivedCategory.Q.obj P ≅ DerivedCategory.Q.obj P') :
    complexChern C sY hP = complexChern C sY hP'

Stacks.Chow.powerSumComplex_eq_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PowerSumIndependence.lean, line 208. The attribute's comment: “the classes P_p(E^bullet) of a locally bounded complex of finite locally free modules, ranks varying, depend only on its object of D(O_Y)”.

Let P, P' be locally bounded complexes of finite locally free 𝒪_Y-modules representing the same object of D(𝒪_Y). Then P_p(P) = P_p(P') ∈ A^p(Y) for every p.

theorem powerSumComplex_eq_of_iso (e : DerivedCategory.Q.obj P ≅ DerivedCategory.Q.obj P')
    (p : ℕ) : powerSumComplex C sY hP p = powerSumComplex C sY hP' p

Stacks.Chow.chernCharacterComplex_eq_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PowerSumIndependence.lean, line 219. The attribute's comment: “the Chern character ch(E^bullet) = sum_p P_p(E^bullet)/p! of a locally bounded complex of finite locally free modules, ranks varying, depends only on its object of D(O_Y)”.

ch_p(P) = ch_p(P') ∈ A^p(Y) ⊗ 𝐐 for locally bounded complexes P, P' of finite locally free modules representing the same object of D(𝒪_Y).

theorem chernCharacterComplex_eq_of_iso (e : DerivedCategory.Q.obj P ≅ DerivedCategory.Q.obj P')
    (p : ℕ) : chernCharacterComplex C sY hP p = chernCharacterComplex C sY hP' p
Tag 0GUD, a lemma

Tag 0GUD in the Stacks Project.

Stacks.Chow.eq_of_restriction_eq_totalChernClassComplexLocallyBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/EnvelopeUniqueness.lean, line 216. The attribute's comment: “the uniqueness half for the total Chern class c(E), read on the coefficients of the series of Tag 0ESZ; the existence of the classes is not constructed here, and the hypothesis is taken at one envelope presentation rather than at all of them, which is stronger”.

Stacks 0GUD, uniqueness for the total Chern class. Let E be an object of D(𝒪_X) and let H be an envelope presentation of it, Stacks 0F9E (1), whose source is quasi-compact. Two families c, d of Chow cohomology classes of X whose restrictions along the envelope of H are the coefficients of the total Chern class c(P) of the presenting complex are equal.

The existence of such a family is not proved: see the implementation notes of this file. The hypothesis is taken at the single presentation H rather than at every presentation of E, so this is stronger than the uniqueness clause of the tag.

theorem eq_of_restriction_eq_totalChernClassComplexLocallyBounded
    (H : EnvelopePresentation E) [LocallyOfFiniteType H.f] [CompactSpace H.Y]
    {R : ChowCohomologySeriesRing C G (H.f ≫ sX)} (D : TotalChernClassSeries C G (H.f ≫ sX) R)
    {c d : ∀ p : ℕ, chowCohomologyComponent C G sX (p : ℤ)}
    (hc : ∀ p : ℕ, chowCohomologyRestriction C G sX H.f (p : ℤ) hgys (c p) =
      (totalChernClassComplexLocallyBounded C G (H.f ≫ sX) D H.P H.locallyBounded).1 p)
    (hd : ∀ p : ℕ, chowCohomologyRestriction C G sX H.f (p : ℤ) hgys (d p) =
      (totalChernClassComplexLocallyBounded C G (H.f ≫ sX) D H.P H.locallyBounded).1 p) :
    c = d

Stacks.Chow.eq_of_restriction_eq_powerSumClassComplexLocallyBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/EnvelopeUniqueness.lean, line 240. The attribute's comment: “the uniqueness half for the power sums P_p(E), the classes of Tag 0ESZ; the existence of the classes is not constructed here, and the hypothesis is taken at one envelope presentation rather than at all of them, which is stronger”.

Stacks 0GUD, uniqueness for the power sums. Let E be an object of D(𝒪_X) and let H be an envelope presentation of it, Stacks 0F9E (1), whose source is quasi-compact. Two families c, d of Chow cohomology classes of X whose restrictions along the envelope of H are the classes P_p(P) of the presenting complex are equal.

The existence of such a family is not proved: see the implementation notes of this file. The hypothesis is taken at the single presentation H rather than at every presentation of E, so this is stronger than the uniqueness clause of the tag.

theorem eq_of_restriction_eq_powerSumClassComplexLocallyBounded
    (H : EnvelopePresentation E) [LocallyOfFiniteType H.f] [CompactSpace H.Y]
    (W : PowerSumClassRule C G (H.f ≫ sX))
    {c d : ∀ p : ℕ, chowCohomologyComponent C G sX (p : ℤ)}
    (hc : ∀ p : ℕ, chowCohomologyRestriction C G sX H.f (p : ℤ) hgys (c p) =
      powerSumClassComplexLocallyBounded C G (H.f ≫ sX) W H.P H.locallyBounded p)
    (hd : ∀ p : ℕ, chowCohomologyRestriction C G sX H.f (p : ℤ) hgys (d p) =
      powerSumClassComplexLocallyBounded C G (H.f ≫ sX) W H.P H.locallyBounded p) :
    c = d

Stacks.Chow.eq_of_restriction_eq_chernCharacterComplexLocallyBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/EnvelopeUniqueness.lean, line 266. The attribute's comment: “the uniqueness half for the Chern character ch(E), read componentwise as ch_p = P_p/p! with the classes P_p of Tag 0ESZ; the existence of the classes is not constructed here, and the hypothesis is taken at one envelope presentation rather than at all of them, which is stronger”.

Stacks 0GUD, uniqueness for the Chern character. Let E be an object of D(𝒪_X) and let H be an envelope presentation of it, Stacks 0F9E (1), whose source is quasi-compact. Two families c, d of rational Chow cohomology classes of X whose restrictions along the envelope of H are the components ch_p(P) = P_p(P)/p! of the Chern character of the presenting complex are equal.

The existence of such a family is not proved: see the implementation notes of this file. The hypothesis is taken at the single presentation H rather than at every presentation of E, so this is stronger than the uniqueness clause of the tag.

theorem eq_of_restriction_eq_chernCharacterComplexLocallyBounded
    (H : EnvelopePresentation E) [LocallyOfFiniteType H.f] [CompactSpace H.Y]
    (W : PowerSumClassRule C G (H.f ≫ sX))
    {c d : ∀ p : ℕ, rationalChowCohomologyComponent C G sX (p : ℤ)}
    (hc : ∀ p : ℕ, rationalChowCohomologyRestriction C G sX H.f (p : ℤ) hgys (c p) =
      ((Nat.factorial p : ℚ)⁻¹) ⊗ₜ[ℤ]
        powerSumClassComplexLocallyBounded C G (H.f ≫ sX) W H.P H.locallyBounded p)
    (hd : ∀ p : ℕ, rationalChowCohomologyRestriction C G sX H.f (p : ℤ) hgys (d p) =
      ((Nat.factorial p : ℚ)⁻¹) ⊗ₜ[ℤ]
        powerSumClassComplexLocallyBounded C G (H.f ≫ sX) W H.P H.locallyBounded p) :
    c = d

Stacks.Chow.existsUnique_perfectPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectPowerSum.lean, line 274. The attribute's comment: “P_p(E): the unique class of A^p(X) restricting along the envelope of every presentation (f, E^bullet) of E to P_p(E^bullet), independent of f and E^bullet”.

Uniqueness of the power sums. Let E be a perfect object of D(𝒪_X) whose Chern classes are defined. For every p there is a unique class P_p(E) ∈ A^p(X) whose restriction along the envelope f : Y ⟶ X of every presentation (f, 𝓔^•) of E is the class P_p(𝓔^•) of Lemma 0ESZ, which on the locus where the terms have constant ranks is ∑ (-1)^n P_p(𝓔^n) (Stacks.Chow.res_complexPowerSum_complexRankLocus). The class is Stacks.Chow.perfectPowerSumComponent.

theorem existsUnique_perfectPowerSum (p : ℕ) :
    ∃! x : chowCohomologyComponent C (gysinSystemOfInvertible C) sX (p : ℤ),
      ∀ H : EnvelopePresentation E,
        chowCohomologyRestriction C (gysinSystemOfInvertible C) sX H.f (p : ℤ)
            (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) x =
          complexPowerSumComponent C (H.f ≫ sX) H.locallyBounded p

Stacks.Chow.existsUnique_perfectChernCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectPowerSum.lean, line 341. The attribute's comment: “ch(E): for every p the unique class of A^p(X) ⊗ Q restricting along the envelope of every presentation (f, E^bullet) of E to ch_p(E^bullet) = P_p(E^bullet)/p!, independent of f and E^bullet”.

Uniqueness of the Chern character. Let E be a perfect object of D(𝒪_X) whose Chern classes are defined. For every p there is a unique class ch_p(E) ∈ A^p(X) ⊗ 𝐐 whose rational restriction along the envelope f : Y ⟶ X of every presentation (f, 𝓔^•) of E is the component ch_p(𝓔^•) = P_p(𝓔^•)/p! of the Chern character of 𝓔^• (Lemma 0ESZ). The class is Stacks.Chow.perfectChernCharacterComponent, and the family (ch_p(E))_p is ch(E) ∈ ∏_{p ≥ 0} A^p(X) ⊗ 𝐐.

theorem existsUnique_perfectChernCharacter (p : ℕ) :
    ∃! x : rationalChowCohomologyComponent C (gysinSystemOfInvertible C) sX (p : ℤ),
      ∀ H : EnvelopePresentation E,
        rationalChowCohomologyRestriction C (gysinSystemOfInvertible C) sX H.f (p : ℤ)
            (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) x =
          complexChernCharacterComponent C (H.f ≫ sX) H.locallyBounded p

Declarations registered for the tag:

Tag 0F9E, a definition

Tag 0F9E in the Stacks Project.

Stacks.Chow.HasDefinedChernClasses, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/Defined.lean, line 80. The attribute's comment: “clause (1): the condition under which the Chern classes of a perfect object are defined”.

Stacks 0F9E (1). The Chern classes of an object E of D(𝒪_X) are defined when some envelope f : Y ⟶ X has Lf^*E isomorphic to a locally bounded complex of finite locally free 𝒪_Y-modules.

def HasDefinedChernClasses {X : Scheme.{u}} (E : DerivedCategory X.Modules) : Prop

Stacks.Chow.perfectPowerSumComponent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DerivedChernClasses.lean, line 600. The attribute's comment: “clause (2), the class P_p(E) in A^p(X): the universal power sum of Tag 0F9B applied to c(E), with the alternating rank class r(E) as its degree-zero member. It restricts to P_p(E^bullet) along the envelope of every presentation, which is the property Tag 0GUD defines it by (Stacks.Chow.res_perfectPowerSumComponent)”.

The class P_p(E) ∈ A^p(X) of Stacks 0F9E (2), the degree-p component of Stacks.Chow.perfectPowerSum.

def perfectPowerSumComponent (hE : HasDefinedChernClasses E) (p : ℕ) :
    chowCohomologyComponent C (gysinSystemOfInvertible C) sX (p : ℤ)

Stacks.Chow.perfectChernCharacter, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DerivedChernClasses.lean, line 619. The attribute's comment: “clause (2), the class ch(E) in prod_{p >= 0} (A^p(X) tensor Q), componentwise as ch_p(E) = P_p(E)/p! as the source reads it”.

The Chern character ch(E) ∈ ∏_{p ≥ 0} (A^p(X) ⊗ 𝐐) of a perfect object whose Chern classes are defined, Stacks 0F9E (2), the family of its components.

def perfectChernCharacter (hE : HasDefinedChernClasses E) :
    fullRationalChowCohomology C (gysinSystemOfInvertible C) sX

Stacks.Chow.perfectChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/EnvelopeChern.lean, line 210. The attribute's comment: “clause (2) for c(E): the class c(E) in prod_{p >= 0} A^p(X), carrying c_p(E) in degree p, for an object of D(O_X) whose Chern classes are defined in the sense of clause (1). Stacks.Chow.res_perfectChernClass pins it down at every envelope presentation, which is how Lemma 0GUD characterizes it. The two further classes clause (2) names are ch(E) (Stacks.Chow.perfectChernCharacter) and P_p(E) (Stacks.Chow.perfectPowerSumComponent)”.

The total Chern class c(E) of an object whose Chern classes are defined, Stacks 0F9E (2): the class of Stacks 0GUD, the unique total class of X whose restriction along the envelope of a presentation of E is the total Chern class of the presenting complex. Its degree-p component is c_p(E).

def perfectChernClass (hE : HasDefinedChernClasses E) : TotalChowClass C sX
Tag 0GUE, a lemma

Tag 0GUE in the Stacks Project.

Stacks.Chow.hasDefinedChernClasses_of_envelope, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/Criteria.lean, line 69. The attribute's comment: “clause (1): the envelope condition of Tag 0F9E (1) itself”.

Stacks 0GUE (1). If some envelope f : Y ⟶ X has Lf^*E isomorphic to a locally bounded complex of finite locally free 𝒪_Y-modules, then the Chern classes of E are defined.

theorem hasDefinedChernClasses_of_envelope {X Y : Scheme.{u}} (f : Y ⟶ X)
    (hf : IsEnvelope f) (E : DerivedCategory X.Modules) (P : CochainComplex Y.Modules ℤ)
    (hP : IsLocallyBoundedFiniteLocallyFree P)
    (hrep : Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      f.toLRSHom.toShHom).obj E ≅ DerivedCategory.Q.obj P)) :
    HasDefinedChernClasses E

Stacks.Chow.hasDefinedChernClasses_of_bounded_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/Criteria.lean, line 95. The attribute's comment: “clause (2): a bounded complex of finite locally free modules representing E”.

Stacks 0GUE (2). If E is represented by a bounded complex of finite locally free 𝒪_X-modules, then the Chern classes of E are defined: the identity of X is an envelope and L(𝟙 X)^* ≅ 𝟭.

theorem hasDefinedChernClasses_of_bounded_isFiniteLocallyFree {X : Scheme.{u}}
    (E : DerivedCategory X.Modules) (P : CochainComplex X.Modules ℤ)
    (hP : CochainComplex.bounded X.Modules P)
    (hflf : ∀ n : ℤ, SheafOfModules.IsFiniteLocallyFree
      (R := structureSheafOfRings X.toRingedSpace) (P.X n))
    (hrep : Nonempty (DerivedCategory.Q.obj P ≅ E)) :
    HasDefinedChernClasses E

Stacks.Chow.hasDefinedChernClasses_of_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/Criteria.lean, line 116. The attribute's comment: “clause (5): E is the derived pullback of an object whose Chern classes are defined”.

Stacks 0GUE (5). If E is isomorphic to the derived pullback of an object E' whose Chern classes are defined, then the Chern classes of E are defined: the base change of an envelope of E' is an envelope, and the degreewise pullback of a locally bounded complex of finite locally free modules is one again and computes the derived pullback.

At i = Iso.refl this is the well-definedness that clause (2) of Stacks 0FAC presupposes when it writes c_p(Lg^*E).

theorem hasDefinedChernClasses_of_derivedPullback {X X' : Scheme.{u}} (g : X ⟶ X')
    (E : DerivedCategory X.Modules) (E' : DerivedCategory X'.Modules)
    (hE' : HasDefinedChernClasses E')
    (i : E ≅ (Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      g.toLRSHom.toShHom).obj E') :
    HasDefinedChernClasses E

Stacks.Chow.hasDefinedChernClasses_of_isCompact_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/CriteriaComponents.lean, line 231. The attribute's comment: “clause (3): the irreducible components of X are quasi-compact. The conclusion is the full one: the Chern classes of E are defined, i.e. there is an envelope f : Y -> X with Lf^*E isomorphic in D(O_Y) to a locally bounded complex of finite locally free O_Y-modules, which is Tag 0F9E (1). The hypotheses are exactly the source's: the base situation of Tag 02QL, X locally of finite type over its base, E perfect, and the irreducible components of X quasi-compact”.

[Stacks, Tag 0GUE] clause (3). Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S with quasi-compact irreducible components, and let E be a perfect object of D(𝒪_X). Then the Chern classes of E are defined: there is an envelope f : Y ⟶ X such that Lf^*E is isomorphic in D(𝒪_Y) to a locally bounded complex of finite locally free 𝒪_Y-modules.

X is locally Noetherian, the base being locally Noetherian and X locally of finite type over it, so Stacks.Chow.exists_isEnvelope_sigma_of_isCompact_irreducibleComponents supplies an envelope ∐ W ⟶ X whose summands are Noetherian — hence quasi-compact and quasi-separated — with the resolution property and affine diagonal. Then Stacks.Chow.exists_isLocallyBoundedFiniteLocallyFree_iso_derivedPullback_sigma represents Lf^*E, which is clause (1) of the source.

Every hypothesis is a hypothesis of the source: the Chow situation, X locally of finite type over its base, E perfect, and quasi-compactness of the irreducible components of X. Local Noetherianity, the envelope, the summands' resolution property and affine diagonal, and the complex are all derived.

theorem hasDefinedChernClasses_of_isCompact_irreducibleComponents
    (C : ChowSituation.{u}) {X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (hqc : ∀ Z ∈ irreducibleComponents X, IsCompact Z)
    (E : DerivedCategory X.Modules) (hE : IsPerfect (X := X.toRingedSpace) E) :
    HasDefinedChernClasses E

Stacks.Chow.hasDefinedChernClasses_of_compactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/CriteriaQuasiCompact.lean, line 126. The attribute's comment: “clause (4): X is quasi-compact. The conclusion is the full one: the Chern classes of E are defined, i.e. there is an envelope f : Y ⟶ X with Lf^*E isomorphic in D(O_Y) to a locally bounded complex of finite locally free O_Y-modules, which is Tag 0F9E (1). The hypotheses are exactly the source's: the base situation of Tag 02QL, X locally of finite type over its base, E perfect, and X quasi-compact”.

[Stacks, Tag 0GUE] clause (4). Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S and quasi-compact, and let E be a perfect object of D(𝒪_X). Then the Chern classes of E are defined: there is an envelope f : Y ⟶ X such that Lf^*E is isomorphic in D(𝒪_Y) to a locally bounded complex of finite locally free 𝒪_Y-modules.

X is Noetherian, the base being locally Noetherian, hence quasi-separated, so [Stacks, Tag 0GTU] gives an envelope f : Y ⟶ X with Y carrying an ample family of invertible modules; Y is Noetherian because f is proper, has the resolution property by Stacks.Chow.hasResolutionProperty_of_isAmpleFamily_of_isNoetherian, and therefore has affine diagonal by the Noetherian case of [Stacks, Tag 0F8C]. Then Stacks.Chow.hasDefinedChernClasses_of_resolutionProperty_envelope applies.

Every hypothesis is a hypothesis of the source: the Chow situation, X locally of finite type over its base, perfectness of E, and quasi-compactness of X. Quasi-separatedness, Noetherianity, the envelope, the ample family, the resolution property and the affine diagonal are all derived.

theorem hasDefinedChernClasses_of_compactSpace
    (C : ChowSituation.{u}) {X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    [CompactSpace X] (E : DerivedCategory X.Modules)
    (hE : IsPerfect (X := X.toRingedSpace) E) :
    HasDefinedChernClasses E
Tag 0GUF, a lemma

Tag 0GUF in the Stacks Project.

Stacks.Chow.powerSumClass_eq_of_envelopePresentation_modification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComputedOnModification.lean, line 146. The attribute's comment: “the characteristic class clause res(c_p(E)) = c_p(E^bullet), in the power sum reading P_p of Tag 0ESZ, for the lift a : W' -> Y of the modification to the envelope, so that res is along the g' = a . f of the tag. CARRIED: the family P_p(E) itself, which this repository does not construct -- it is taken as a family restricting along the envelope to P_p of the presenting complex, the hypothesis of the Tag 0GUD uniqueness theorems and the only expression here for 'c is the family of Chern classes of E'; the base change compatibility of the power sum data, which Stacks.Chow.PowerSumClassRule does not record; and the identification of a^E_Y^. with a representative of L(g')^E. NOT DELIVERED: the total Chern class reading, which needs the multiplicativity of the restriction map, Tag 0FE0 hence Tag 0B6Y, not formalized here; and the refinement that on an integral W' the pulled back complex has terms of constant rank. The geometric half of the tag is Stacks 0GUF on AlgebraicGeometry.IsEnvelope.exists_properBirational_modification”.

Stacks 0GUF, the characteristic class clause, for the power sums. Let E be an object of D(𝒪_X) and let H be an envelope presentation of it, Stacks 0F9E (1), with presenting complex ℰ_Y^• = H.P vanishing outside the degrees w, …, w + k. Let a : W' ⟶ Y be the lift to the envelope of a modification of a morphism g : W ⟶ X, as produced by AlgebraicGeometry.IsEnvelope.exists_properBirational_modification, so that the morphism g' : W' ⟶ X of the source is a ≫ H.f.

If a family c of Chow cohomology classes of X restricts along the envelope to the power sums of the presenting complex — which is this repository's expression for c being the family of power sum classes P_p(E) of E, and is the hypothesis of Stacks.Chow.eq_of_restriction_eq_powerSumClassComplexLocallyBounded — then its restriction along g' = a ≫ H.f is the power sum class of the pulled back complex a^*ℰ_Y^•:

res_{g'}(P_p(E)) = P_p(a^*ℰ_Y^•).

This is the source's chain res_{g'}(c_p(E)) = res_a(res_f(c_p(E))) = res_a(c_p(ℰ_Y^•)) = c_p(a^*ℰ_Y^•). See the implementation notes of this file for what stands in for c_p(E), why the power sums and not the total Chern class, and what the statement does not deliver.

theorem powerSumClass_eq_of_envelopePresentation_modification (H : EnvelopePresentation E)
    [LocallyOfFiniteType H.f] {V : Scheme.{u}} (a : V ⟶ H.Y) [LocallyOfFiniteType a]
    (W : PowerSumClassRule C G (H.f ≫ sX)) (Wa : PowerSumClassRule C G (a ≫ (H.f ≫ sX)))
    (hW : PowerSumClassRule.IsBaseChangeCompatible C G (H.f ≫ sX) a hgys W Wa)
    (w : ℤ) (k : ℕ)
    (hflf : ∀ i ∈ Finset.range (k + 1),
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} (R := H.Y.ringCatSheaf)
        (H.P.X (w + (i : ℤ))))
    {c : ∀ p : ℕ, chowCohomologyComponent C G sX (p : ℤ)}
    (hc : ∀ p : ℕ, chowCohomologyRestriction C G sX H.f (p : ℤ) hgys (c p) =
      powerSumClassComplex C G (H.f ≫ sX) W H.P w k p)
    (p : ℕ) :
    chowCohomologyRestriction C G sX (a ≫ H.f) (p : ℤ) hgys (c p) =
      powerSumClassComplex C G (a ≫ (H.f ≫ sX)) Wa
        (((Scheme.Modules.pullback a).mapHomologicalComplex (ComplexShape.up ℤ)).obj H.P)
        w k p

Stacks.Chow.chernCharacter_eq_of_envelopePresentation_modification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassComputedOnModification.lean, line 230. The attribute's comment: “the characteristic class clause res(c_p(E)) = c_p(E^bullet), in the Chern character reading ch_p = P_p/p! of Tag 0ESZ, for the lift a : W' -> Y of the modification to the envelope, so that res is along the g' = a . f of the tag. CARRIED: the family ch_p(E) itself, which this repository does not construct -- it is taken as a family restricting along the envelope to ch_p of the presenting complex, the hypothesis of the Tag 0GUD uniqueness theorem; the base change compatibility of the power sum data; and the identification of a^E_Y^. with a representative of L(g')^E. NOT DELIVERED: the total Chern class reading, which needs the multiplicativity of the restriction map, Tag 0FE0 hence Tag 0B6Y”.

Stacks 0GUF, the characteristic class clause, for the Chern character. The Chern character reading of res(c_p(E)) = c_p(ℰ^•): for a family c of rational Chow cohomology classes of X restricting along the envelope of a presentation to the components ch_p(ℰ_Y^•) = P_p(ℰ_Y^•)/p!, the restriction of c p along g' = a ≫ H.f is ch_p(a^*ℰ_Y^•).

The hypothesis is the one of Stacks.Chow.eq_of_restriction_eq_chernCharacterComplexLocallyBounded, the Stacks 0GUD uniqueness theorem for the Chern character, read at a bounded window; see the implementation notes of this file.

theorem chernCharacter_eq_of_envelopePresentation_modification (H : EnvelopePresentation E)
    [LocallyOfFiniteType H.f] {V : Scheme.{u}} (a : V ⟶ H.Y) [LocallyOfFiniteType a]
    (W : PowerSumClassRule C G (H.f ≫ sX)) (Wa : PowerSumClassRule C G (a ≫ (H.f ≫ sX)))
    (hW : PowerSumClassRule.IsBaseChangeCompatible C G (H.f ≫ sX) a hgys W Wa)
    (w : ℤ) (k : ℕ)
    (hflf : ∀ i ∈ Finset.range (k + 1),
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} (R := H.Y.ringCatSheaf)
        (H.P.X (w + (i : ℤ))))
    {c : ∀ p : ℕ, rationalChowCohomologyComponent C G sX (p : ℤ)}
    (hc : ∀ p : ℕ, rationalChowCohomologyRestriction C G sX H.f (p : ℤ) hgys (c p) =
      chernCharacterComplexComponent C G (H.f ≫ sX) W H.P w k p)
    (p : ℕ) :
    rationalChowCohomologyRestriction C G sX (a ≫ H.f) (p : ℤ) hgys (c p) =
      chernCharacterComplexComponent C G (a ≫ (H.f ≫ sX)) Wa
        (((Scheme.Modules.pullback a).mapHomologicalComplex (ComplexShape.up ℤ)).obj H.P)
        w k p

Stacks.Chow.exists_properBirational_res_perfectChernClass_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectChernOnModification.lean, line 120. The attribute's comment: “the full lemma: an integral W' with b : W' -> W proper birational, a bounded complex E^bullet of finite locally free O_{W'}-modules of constant ranks representing L(g')^*E for g' = b . g, and res_{g'}(c_p(E)) = c_p(E^bullet) in A^p(W') for the Chern classes c_p(E) of Tag 0F9E (2), Stacks.Chow.perfectChernClass. The perfectness of E is not needed”.

Stacks 0GUF. Let X be locally of finite type over the base and let E be an object of D(𝒪_X) whose Chern classes are defined. For g : W ⟶ X locally of finite type with W integral there are an integral scheme W' and a proper birational morphism b : W' ⟶ W such that, for g' = b ≫ g, the derived pullback L(g')^*E is represented by a bounded complex ℰ^• of finite locally free 𝒪_{W'}-modules of constant ranks ρ, and

res_{g'}(c_p(E)) = c_p(ℰ^•) in A^p(W') for every p,

where c_p(E) is the degree-p component of the total Chern class c(E) of Stacks 0F9E (2) and c_p(ℰ^•) that of ∏_n c(ℰ^n)^{(-1)^n}.

Perfectness of E is not used: the Chern classes being defined is the only hypothesis on E the construction needs.

theorem exists_properBirational_res_perfectChernClass_eq (hE : HasDefinedChernClasses E)
    {W : Scheme.{u}} [IsIntegral W] (g : W ⟶ X) [LocallyOfFiniteType g] :
    ∃ (W' : Scheme.{u}) (b : W' ⟶ W) (_ : IsIntegral W') (_ : IsProper b),
      IsBirational b ∧
      ∃ (ℰ : CochainComplex W'.Modules ℤ) (ρ : ℤ →₀ ℕ)
        (hρ : ∀ n,
          AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (ℰ.X n) (ρ n)),
        (∃ lo hi : ℤ, ∀ n, (n < lo ∨ hi < n) → IsZero (ℰ.X n)) ∧
        Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          (b ≫ g).toLRSHom.toShHom).obj E ≅ DerivedCategory.Q.obj ℰ) ∧
        ∀ p : ℕ, chowCohomologyRestriction C (gysinSystemOfInvertible C) sX (b ≫ g) (p : ℤ)
            (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
            (perfectChernClass C sX hE p) =
          complexChernBounded C ((b ≫ g) ≫ sX) ℰ ρ hρ p

AlgebraicGeometry.IsEnvelope.exists_properBirational_modification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChowGroupsEnvelopes/BirationalModification.lean, line 189. The attribute's comment: “existence of the proper birational modification factoring through an envelope”.

Stacks 0GUF, the modification and the factorization. Let f : Y ⟶ X be an envelope and let g : W ⟶ X be a morphism with W integral. Then there are an integral scheme W', a proper birational morphism b : W' ⟶ W and a morphism a : W' ⟶ Y with b ≫ g = a ≫ f.

theorem IsEnvelope.exists_properBirational_modification {X Y W : Scheme.{u}}
    {f : Y ⟶ X} (hf : IsEnvelope f) (g : W ⟶ X) [IsIntegral W] :
    ∃ (W' : Scheme.{u}) (b : W' ⟶ W) (a : W' ⟶ Y),
      IsIntegral W' ∧ IsProper b ∧ IsBirational b ∧ b ≫ g = a ≫ f
Tag 0FAC, a lemma

Tag 0FAC in the Stacks Project.

Stacks.Chow.nonhomogeneousBivariantGroupCongr_compositeOfInvertible_perfectChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/BivariantCommute.lean, line 713. The attribute's comment: “(2): c ∘ c_p(E) = c_p(Lg^E) ∘ c in A^(X' → X), for every c in A^*(X' → X), the Chern classes of Stacks 0F9E (2) and the composition of Stacks 0B75 at the Gysin system of the first Chern class of an invertible module, extended additively to the graded groups”.

Stacks 0FAC (2). Let X be locally of finite type over the base, let E ∈ D(𝒪_X) be perfect with Chern classes defined, let g : X' ⟶ X be locally of finite type and let c ∈ A^*(X' ⟶ X). Then for every p

c ∘ c_p(E) = c_p(Lg^*E) ∘ c in A^*(X' ⟶ X),

the composites being those of Stacks 0B75, extended additively to the graded groups; they are classes for the morphisms g ≫ 𝟙 X and 𝟙 X' ≫ g, both read as classes for g.

theorem nonhomogeneousBivariantGroupCongr_compositeOfInvertible_perfectChernClass
    (c : nonhomogeneousBivariantGroup C (gysinSystemOfInvertible C) sX' sX g hg) (p : ℕ) :
    nonhomogeneousBivariantGroupCongr C (gysinSystemOfInvertible C) sX' sX (Category.comp_id g)
        (comp_comp_structureMorphism_eq hg (Category.id_comp sX)) hg
        (nonhomogeneousBivariantCompositeOfInvertible C sX' sX sX g (𝟙 X) hg
          (Category.id_comp sX) c (DirectSum.of _ (p : ℤ) (perfectChernClass C sX hE p))) =
      nonhomogeneousBivariantGroupCongr C (gysinSystemOfInvertible C) sX' sX (Category.id_comp g)
        (comp_comp_structureMorphism_eq (Category.id_comp sX') hg) hg
        (nonhomogeneousBivariantCompositeOfInvertible C sX' sX' sX (𝟙 X') g
          (Category.id_comp sX') hg
          (DirectSum.of _ (p : ℤ) (perfectChernClass C sX' (hE.derivedPullback g) p)) c)

Stacks.Chow.nonhomogeneousBivariantGroupCongr_compositeOfInvertible_perfectChernClass_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/BivariantCommute.lean, line 747. The attribute's comment: “(1): c_p(E) is in the center of A^(X), c · c_p(E) = c_p(E) · c for every c in A^(X), the product being the composition of Stacks 0B75 at the Gysin system of the first Chern class of an invertible module, extended additively to the graded groups, and the Chern classes of Stacks 0F9E (2)”.

Stacks 0FAC (1). Let E ∈ D(𝒪_X) be perfect with Chern classes defined. Then c_p(E) is in the center of A^*(X): for every c ∈ A^*(X),

c · c_p(E) = c_p(E) · c,

the product of A^*(X) being the composition of Stacks 0B75, extended additively to the graded groups, of classes for 𝟙 X ≫ 𝟙 X, read as a class for 𝟙 X; on homogeneous classes it is Stacks.Chow.BivariantClass.mulId.

theorem nonhomogeneousBivariantGroupCongr_compositeOfInvertible_perfectChernClass_comm
    (c : nonhomogeneousBivariantGroup C (gysinSystemOfInvertible C) sX sX (𝟙 X)
      (Category.id_comp sX)) (p : ℕ) :
    nonhomogeneousBivariantGroupCongr C (gysinSystemOfInvertible C) sX sX
        (Category.comp_id (𝟙 X))
        (comp_comp_structureMorphism_eq (Category.id_comp sX) (Category.id_comp sX))
        (Category.id_comp sX)
        (nonhomogeneousBivariantCompositeOfInvertible C sX sX sX (𝟙 X) (𝟙 X) (Category.id_comp sX)
          (Category.id_comp sX) c (DirectSum.of _ (p : ℤ) (perfectChernClass C sX hE p))) =
      nonhomogeneousBivariantGroupCongr C (gysinSystemOfInvertible C) sX sX
        (Category.comp_id (𝟙 X))
        (comp_comp_structureMorphism_eq (Category.id_comp sX) (Category.id_comp sX))
        (Category.id_comp sX)
        (nonhomogeneousBivariantCompositeOfInvertible C sX sX sX (𝟙 X) (𝟙 X) (Category.id_comp sX)
          (Category.id_comp sX) (DirectSum.of _ (p : ℤ) (perfectChernClass C sX hE p)) c)

Stacks.Chow.comp_perfectChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectChernCentral.lean, line 412. The attribute's comment: “(2): c ∘ c_p(E) = c_p(Lg^E) ∘ c in A^(X' → X) for every g : X' → X locally of finite type and every bivariant class c in A^q(X' → X) of Stacks 0B76”.

Let E ∈ D(𝒪_X) be perfect with defined Chern classes, let g : X' ⟶ X be locally of finite type and let c ∈ A^q(X' ⟶ X) be a bivariant class. Then

c ∘ c_p(E) = c_p(Lg^*E) ∘ c in A^{q+p}(X' ⟶ X),

with c_p(E) ∈ A^p(X) and c_p(Lg^*E) ∈ A^p(X'). The left side is a class for g ≫ 𝟙 X of degree q + p; the right side, a class for 𝟙 X' ≫ g of degree p + q, is read as one for g ≫ 𝟙 X of degree q + p along the identity of X'.

theorem comp_perfectChernClass
    (_perfect : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) E)
    (hE : HasDefinedChernClasses E) (p : ℕ) (g : X' ⟶ X) (hg : g ≫ sX = sX') {q : ℤ}
    (c : BivariantChowClass C sX' sX g hg q) :
    c.comp (BivariantChowClass.equivBivariantClass.symm (perfectChernClass C sX hE p)) =
      (((BivariantChowClass.equivBivariantClass.symm
          (perfectChernClass C sX' (hasDefinedChernClasses_derivedPullback g hE)
            p)).comp c).degreeCongr (add_comm (p : ℤ) q)).transport
        (comp_comp_structureMorphism_eq hg (Category.id_comp sX)) (Iso.refl X') (by simp)

Stacks.Chow.perfectChernClass_mem_center, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectChernCentral.lean, line 429. The attribute's comment: “(1): c_p(E) is in the center of the Chow cohomology ring A^*(X) of Stacks 0B7E”.

Let E ∈ D(𝒪_X) be perfect with defined Chern classes. Then c_p(E) ∈ A^p(X) lies in the center of the Chow cohomology ring A^*(X).

theorem perfectChernClass_mem_center
    (_perfect : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) E)
    (hE : HasDefinedChernClasses E) (p : ℕ) :
    letI : Ring (chowCohomology C (gysinSystemOfInvertible C) sX) :=
      chowCohomologyRingOfInvertible C sX
    DirectSum.of (fun q : ℤ ↦ chowCohomologyComponent C (gysinSystemOfInvertible C) sX q)
        (p : ℤ) (perfectChernClass C sX hE p) ∈
      Subring.center (chowCohomology C (gysinSystemOfInvertible C) sX)
Tag 0F9F, a lemma

Tag 0F9F in the Stacks Project.

Stacks.Chow.hasDefinedChernClasses_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/Triangle.lean, line 242. The attribute's comment: “the Chern classes of E₁, E₂, E₃ are defined”.

Stacks 0F9F, definedness. Let E₁ ⟶ E₂ ⟶ E₃ ⟶ E₁[1] be a distinguished triangle of perfect objects of D(𝒪_X) satisfying one of the conditions of Stacks 0F9F. Then the Chern classes of E₁, E₂ and E₃ are defined.

theorem hasDefinedChernClasses_triangle :
    HasDefinedChernClasses T.obj₁ ∧ HasDefinedChernClasses T.obj₂ ∧
      HasDefinedChernClasses T.obj₃

Stacks.Chow.perfectChernClass_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/Triangle.lean, line 253. The attribute's comment: “c(E₂) = c(E₁) c(E₃)”.

Stacks 0F9F, the total Chern class. Under the hypotheses of Stacks 0F9F, c(E₂) = c(E₁) c(E₃).

theorem perfectChernClass_triangle (d₁ : HasDefinedChernClasses T.obj₁)
    (d₂ : HasDefinedChernClasses T.obj₂) (d₃ : HasDefinedChernClasses T.obj₃) :
    perfectChernClass C sX d₂ = perfectChernClass C sX d₁ * perfectChernClass C sX d₃

Stacks.Chow.perfectChernCharacter_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/Triangle.lean, line 262. The attribute's comment: “ch(E₂) = ch(E₁) + ch(E₃), in every degree”.

Stacks 0F9F, the Chern character. Under the hypotheses of Stacks 0F9F, ch(E₂) = ch(E₁) + ch(E₃), in every degree p.

theorem perfectChernCharacter_triangle (d₁ : HasDefinedChernClasses T.obj₁)
    (d₂ : HasDefinedChernClasses T.obj₂) (d₃ : HasDefinedChernClasses T.obj₃) (p : ℕ) :
    perfectChernCharacterComponent C sX d₂ p =
      perfectChernCharacterComponent C sX d₁ p + perfectChernCharacterComponent C sX d₃ p

Stacks.Chow.perfectPowerSum_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/Triangle.lean, line 272. The attribute's comment: “P_p(E₂) = P_p(E₁) + P_p(E₃)”.

Stacks 0F9F, the power sums. Under the hypotheses of Stacks 0F9F, P_p(E₂) = P_p(E₁) + P_p(E₃) for every p.

theorem perfectPowerSum_triangle (d₁ : HasDefinedChernClasses T.obj₁)
    (d₂ : HasDefinedChernClasses T.obj₂) (d₃ : HasDefinedChernClasses T.obj₃) (p : ℕ) :
    perfectPowerSum C sX d₂ p = perfectPowerSum C sX d₁ p + perfectPowerSum C sX d₃ p

Stacks.Chow.hasDefinedChernClasses_and_additive_of_envelope, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/TriangleAdditivity.lean, line 118. The attribute's comment: “condition (1): there is an envelope f : Y -> X such that Lf^E_1 -> Lf^E_2 is represented by a map of locally bounded complexes of finite locally free O_Y-modules. The conclusion is the whole one: the Chern classes of E_1, E_2 and E_3 are defined, c(E_2) = c(E_1)c(E_3), ch(E_2) = ch(E_1) + ch(E_3) and P_p(E_2) = P_p(E_1) + P_p(E_3), the last two read componentwise in A^p(X) tensor Q and in A^p(X) as the source reads them. Perfectness of the three objects is a standing hypothesis of the source that no step of this proof uses, so it is omitted, exactly as for the criteria of Tag 0GUE”.

Stacks 0F9F under condition (1) of the source. Let T be a distinguished triangle of D(𝒪_X). If there is an envelope f : Y ⟶ X such that Lf^*T.mor₁ : Lf^*E₁ ⟶ Lf^*E₂ is represented by a map α : 𝓔₁^• ⟶ 𝓔₂^• of locally bounded complexes of finite locally free 𝒪_Y-modules, then the Chern classes of E₁, E₂, E₃ are defined and

c(E₂) = c(E₁) c(E₃), ch_p(E₂) = ch_p(E₁) + ch_p(E₃), P_p(E₂) = P_p(E₁) + P_p(E₃).

The cone of α is a locally bounded complex of finite locally free modules representing Lf^*E₃, so f together with 𝓔₁^•, 𝓔₂^• and C(α)^• presents all three objects, and each identity is the corresponding identity for those complexes.

theorem hasDefinedChernClasses_and_additive_of_envelope
    (T : Triangle (DerivedCategory X.Modules))
    (hT : T ∈ distTriang (DerivedCategory X.Modules))
    {Y : Scheme.{u}} (f : Y ⟶ X) (hf : IsEnvelope f)
    {P₁ P₂ : CochainComplex Y.Modules ℤ} (α : P₁ ⟶ P₂)
    (h₁ : IsLocallyBoundedFiniteLocallyFree P₁) (h₂ : IsLocallyBoundedFiniteLocallyFree P₂)
    (e₁ : (Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      f.toLRSHom.toShHom).obj T.obj₁ ≅ DerivedCategory.Q.obj P₁)
    (e₂ : (Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      f.toLRSHom.toShHom).obj T.obj₂ ≅ DerivedCategory.Q.obj P₂)
    (hα : e₁.hom ≫ DerivedCategory.Q.map α =
      (Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        f.toLRSHom.toShHom).map T.mor₁ ≫ e₂.hom) :
    TriangleChernAdditive C sX T

Stacks.Chow.hasDefinedChernClasses_and_additive_of_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/TriangleAdditivity.lean, line 185. The attribute's comment: “condition (2): E_1 -> E_2 is represented by a map of locally bounded complexes of finite locally free O_X-modules. The conclusion is the whole one: the Chern classes of E_1, E_2 and E_3 are defined, c(E_2) = c(E_1)c(E_3), ch(E_2) = ch(E_1) + ch(E_3) and P_p(E_2) = P_p(E_1) + P_p(E_3), the last two read componentwise in A^p(X) tensor Q and in A^p(X) as the source reads them. Perfectness of the three objects is a standing hypothesis of the source that no step of this proof uses, so it is omitted, exactly as for the criteria of Tag 0GUE”.

Stacks 0F9F under condition (2) of the source. If the first map T.mor₁ : E₁ ⟶ E₂ of a distinguished triangle of D(𝒪_X) is itself represented by a map α : 𝓔₁^• ⟶ 𝓔₂^• of locally bounded complexes of finite locally free 𝒪_X-modules, then the Chern classes of E₁, E₂, E₃ are defined and

c(E₂) = c(E₁) c(E₃), ch_p(E₂) = ch_p(E₁) + ch_p(E₃), P_p(E₂) = P_p(E₁) + P_p(E₃).

This is condition (1) for the envelope 𝟙 X, which is proper and completely decomposed; the square identifying α with T.mor₁ transports along the naturality of L(𝟙 X)^* ≅ 𝟭.

theorem hasDefinedChernClasses_and_additive_of_map
    (T : Triangle (DerivedCategory X.Modules))
    (hT : T ∈ distTriang (DerivedCategory X.Modules))
    {P₁ P₂ : CochainComplex X.Modules ℤ} (α : P₁ ⟶ P₂)
    (h₁ : IsLocallyBoundedFiniteLocallyFree P₁) (h₂ : IsLocallyBoundedFiniteLocallyFree P₂)
    (i₁ : T.obj₁ ≅ DerivedCategory.Q.obj P₁) (i₂ : T.obj₂ ≅ DerivedCategory.Q.obj P₂)
    (hα : i₁.hom ≫ DerivedCategory.Q.map α = T.mor₁ ≫ i₂.hom) :
    TriangleChernAdditive C sX T

Stacks.Chow.triangleChernAdditive_of_isCompact_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/TriangleAdditivityComponents.lean, line 351. The attribute's comment: “condition (3): the irreducible components of X are quasi-compact. The conclusion is the whole one: the Chern classes of E_1, E_2 and E_3 are defined, c(E_2) = c(E_1)c(E_3), ch(E_2) = ch(E_1) + ch(E_3) and P_p(E_2) = P_p(E_1) + P_p(E_3), the last two read componentwise in A^p(X) tensor Q and in A^p(X) as the source reads them. The hypotheses are exactly the source's: the base situation of Tag 02QL, X locally of finite type over its base, the distinguished triangle, perfectness of E_1 and E_2, and the irreducible components of X quasi-compact. Perfectness of E_3 is a standing hypothesis of the source that no step of this proof uses, so it is omitted, exactly as for conditions (1), (2) and (4)”.

[Stacks, Tag 0F9F] under condition (3) of the source. Let T be a distinguished triangle of D(𝒪_X) whose first two objects are perfect and let the irreducible components of X, which is locally of finite type over the base of the Chow situation, be quasi-compact. Then the Chern classes of E₁, E₂, E₃ are defined and

c(E₂) = c(E₁) c(E₃), ch_p(E₂) = ch_p(E₁) + ch_p(E₃), P_p(E₂) = P_p(E₁) + P_p(E₃).

X is locally Noetherian, the base being locally Noetherian and X locally of finite type over it, so Stacks.Chow.exists_isEnvelope_sigma_of_isCompact_irreducibleComponents supplies an envelope ∐ W ⟶ X whose summands are Noetherian — hence quasi-compact and quasi-separated — with the resolution property and affine diagonal. On such a source Stacks.Chow.exists_boundedFiniteLocallyFree_sigma_of_isPerfect presents Lf^*E₁ and Lf^*E₂ by complexes whose summandwise restrictions are bounded complexes of finite locally free modules, and Stacks.Chow.exists_isLocallyBoundedFiniteLocallyFree_square_sigma represents Lf^*E₁ ⟶ Lf^*E₂ by a map of locally bounded complexes of finite locally free modules together with the commuting square. That is condition (1) of the source, in the shape Stacks.Chow.hasDefinedChernClasses_and_additive_of_envelope asks for.

Every hypothesis is a hypothesis of the source: the Chow situation, X locally of finite type over its base, the distinguished triangle, perfectness of E₁ and E₂, and quasi-compactness of the irreducible components of X. Local Noetherianity, the envelope, the summands' resolution property and affine diagonal, the two complexes and the map between them are all derived. Perfectness of E₃ is a standing hypothesis of the source that no step of this proof uses, so it is omitted.

theorem triangleChernAdditive_of_isCompact_irreducibleComponents
    (C : ChowSituation.{u}) {X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (T : Triangle (DerivedCategory X.Modules)) (hT : T ∈ distTriang (DerivedCategory X.Modules))
    (h₁ : IsPerfect (X := X.toRingedSpace) T.obj₁)
    (h₂ : IsPerfect (X := X.toRingedSpace) T.obj₂)
    (hqc : ∀ Z ∈ irreducibleComponents X, IsCompact Z) :
    TriangleChernAdditive C sX T

Stacks.Chow.triangleChernAdditive_of_compactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/TriangleAdditivityQuasiCompact.lean, line 147. The attribute's comment: “condition (4): X is quasi-compact. The conclusion is the whole one: the Chern classes of E_1, E_2 and E_3 are defined, c(E_2) = c(E_1)c(E_3), ch(E_2) = ch(E_1) + ch(E_3) and P_p(E_2) = P_p(E_1) + P_p(E_3), the last two read componentwise in A^p(X) tensor Q and in A^p(X) as the source reads them. Perfectness of E_3 is a standing hypothesis of the source that no step of this proof uses, so it is omitted, exactly as for conditions (1) and (2)”.

[Stacks, Tag 0F9F] under condition (4) of the source. Let T be a distinguished triangle of D(𝒪_X) whose first two objects are perfect and let X, which is locally of finite type over the base of the Chow situation, be quasi-compact. Then the Chern classes of E₁, E₂, E₃ are defined and

c(E₂) = c(E₁) c(E₃), ch_p(E₂) = ch_p(E₁) + ch_p(E₃), P_p(E₂) = P_p(E₁) + P_p(E₃).

X is Noetherian, the base being locally Noetherian, hence quasi-separated, so [Stacks, Tag 0GTU] gives an envelope f : Y ⟶ X with Y carrying an ample family of invertible modules; Y is Noetherian because f is proper, has the resolution property by Stacks.Chow.hasResolutionProperty_of_isAmpleFamily_of_isNoetherian, and therefore has affine diagonal by the Noetherian case of [Stacks, Tag 0F8C]. That is condition (1) of the source, in the shape Stacks.Chow.triangleChernAdditive_of_resolutionProperty_envelope asks for.

Every hypothesis is a hypothesis of the source: the Chow situation, X locally of finite type over its base, the distinguished triangle, perfectness of E₁ and E₂, and quasi-compactness of X. Quasi-separatedness, Noetherianity, the envelope, the ample family, the resolution property and the affine diagonal are all derived. Perfectness of E₃ is a standing hypothesis of the source that no step of this proof uses, so it is omitted.

theorem triangleChernAdditive_of_compactSpace
    (C : ChowSituation.{u}) {X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    [CompactSpace X]
    (T : Triangle (DerivedCategory X.Modules)) (hT : T ∈ distTriang (DerivedCategory X.Modules))
    (h₁ : IsPerfect (X := X.toRingedSpace) T.obj₁)
    (h₂ : IsPerfect (X := X.toRingedSpace) T.obj₂) :
    TriangleChernAdditive C sX T
Tag 0FAD, a remark

Tag 0FAD in the Stacks Project.

Stacks.Chow.perfectPowerSum_eq_aeval, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectNewtonIdentities.lean, line 191. The attribute's comment: “P_p(E) is the exact same expression in the Chern classes of E as in the case of vector bundles: the power-sum polynomial P_p of 0F9B evaluated at c_1(E), ..., c_p(E), p >= 1”.

Newton's identities for a perfect object, Remark 0FAD. For p ≥ 1 the class P_p(E) is the universal power-sum polynomial P_p of Stacks 0F9B evaluated at the Chern classes of E — the same expression in the Chern classes as for a finite locally free module. The polynomial is evaluated in the commutative subring of A^*(X) generated by the Chern classes of E.

theorem perfectPowerSum_eq_aeval (p : ℕ) (hp : 0 < p) :
    perfectPowerSum C sX hE p =
      (MvPolynomial.aeval (perfectChernSub C sX hE)
        (powerSumPolynomial p : MvPolynomial ℕ+ ℤ) : TotalChowClass C sX)

Stacks.Chow.perfectPowerSum_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectNewtonIdentities.lean, line 206. The attribute's comment: “the first displayed formula P_1(E) = c_1(E)”.

P_1(E) = c_1(E), Remark 0FAD.

theorem perfectPowerSum_one :
    perfectPowerSum C sX hE 1 = perfectChernComponent C sX hE 1

Stacks.Chow.perfectPowerSum_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectNewtonIdentities.lean, line 213. The attribute's comment: “the second displayed formula P_2(E) = c_1(E)^2 - 2c_2(E)”.

P_2(E) = c_1(E)^2 - 2 c_2(E), Remark 0FAD.

theorem perfectPowerSum_two :
    perfectPowerSum C sX hE 2 =
      perfectChernComponent C sX hE 1 ^ 2 - 2 * perfectChernComponent C sX hE 2

Stacks.Chow.perfectPowerSum_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectNewtonIdentities.lean, line 222. The attribute's comment: “the third displayed formula P_3(E) = c_1(E)^3 - 3c_1(E)c_2(E) + 3c_3(E)”.

P_3(E) = c_1(E)^3 - 3 c_1(E) c_2(E) + 3 c_3(E), Remark 0FAD.

theorem perfectPowerSum_three :
    perfectPowerSum C sX hE 3 =
      perfectChernComponent C sX hE 1 ^ 3 -
        3 * perfectChernComponent C sX hE 1 * perfectChernComponent C sX hE 2 +
        3 * perfectChernComponent C sX hE 3

Stacks.Chow.perfectPowerSum_four, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectNewtonIdentities.lean, line 235. The attribute's comment: “the fourth displayed formula P_4(E) = c_1(E)^4 - 4c_1(E)^2c_2(E) + 4c_1(E)c_3(E) + 2c_2(E)^2 - 4c_4(E)”.

P_4(E) = c_1(E)^4 - 4 c_1(E)^2 c_2(E) + 4 c_1(E) c_3(E) + 2 c_2(E)^2 - 4 c_4(E), Remark 0FAD.

theorem perfectPowerSum_four :
    perfectPowerSum C sX hE 4 =
      perfectChernComponent C sX hE 1 ^ 4 -
        4 * perfectChernComponent C sX hE 1 ^ 2 * perfectChernComponent C sX hE 2 +
        4 * perfectChernComponent C sX hE 1 * perfectChernComponent C sX hE 3 +
        2 * perfectChernComponent C sX hE 2 ^ 2 - 4 * perfectChernComponent C sX hE 4

Stacks.Chow.perfectPowerSum_zero_and_perfectChernCharacterComponent_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectNewtonIdentities.lean, line 248. The attribute's comment: “the bivariant class P_0(E) = r(E) = ch_0(E)”.

P_0(E) = r(E) = ch_0(E), Remark 0FAD: the degree-zero power sum and the degree-zero component of the Chern character are the rank of E.

theorem perfectPowerSum_zero_and_perfectChernCharacterComponent_zero :
    perfectPowerSum C sX hE 0 = perfectRankClass C sX hE ∧
      perfectChernCharacterComponent C sX hE 0 = (1 : ℚ) ⊗ₜ[ℤ] perfectRankClass C sX hE 0

Stacks.Chow.log_perfectChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectNewtonIdentities.lean, line 340. The attribute's comment: “formally taking the logarithm: log(c(E)) = sum_p (-1)^{p-1} P_p(E)/p, read in A^p(X) tensor Q degree by degree, the degree-p part of log c(E) being sum_{k=1}^p (-1)^{k-1} (c(E) - 1)^k / k”.

The logarithmic identity for a perfect object. In A^p(X) ⊗ 𝐐,

∑_{k = 1}^{p} (-1)^{k-1} (c(E) - 1)^k / k = (-1)^{p-1} P_p(E) / p,

the left hand side being the degree-p part of log c(E) (the terms with k > p vanish in degree p: Stacks.Chow.pow_perfectChernClass_sub_one_apply_of_lt). So log c(E) = ∑_p (-1)^{p-1} P_p(E) / p, Remark 0FAD.

theorem log_perfectChernClass (p : ℕ) :
    ∑ k ∈ Finset.Icc 1 p, ((-1 : ℚ) ^ (k - 1) / k) ⊗ₜ[ℤ]
        ((perfectChernClass C sX hE - 1) ^ k) p =
      ((-1 : ℚ) ^ (p - 1) / p) ⊗ₜ[ℤ] perfectPowerSumComponent C sX hE p

Stacks.Chow.exists_perfectChernClass_eq_perfectPowerSum_zero_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectNewtonIdentities.lean, line 540. The attribute's comment: “the bivariant class P_0(E) = r(E) cannot be recovered from the Chern class c(E): on every nonempty X, c(O_X[0]) = c(0) = 1 while r(O_X[0]) = 1 differs from r(0) = 0”.

The rank of a perfect object is not determined by its total Chern class, Remark 0FAD: on every nonempty X there are perfect objects E and F whose Chern classes are defined, with c(E) = c(F) but P_0(E) = r(E) ≠ r(F) = P_0(F). Namely E = 𝒪_X[0] and F = 0[0]: both have total Chern class 1, and their ranks are 1 and 0.

theorem exists_perfectChernClass_eq_perfectPowerSum_zero_ne [Nonempty X] :
    ∃ (E F : DerivedCategory X.Modules)
      (_ : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) E)
      (_ : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) F)
      (hE : HasDefinedChernClasses E) (hF : HasDefinedChernClasses F),
      perfectChernClass C sX hE = perfectChernClass C sX hF ∧
        perfectPowerSum C sX hE 0 ≠ perfectPowerSum C sX hF 0

Stacks.Chow.eq_of_chowCohomologyRestriction_eq_of_envelopePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/SplittingPrinciple.lean, line 148. The attribute's comment: “the splitting principle: a relation between bivariant classes on X may be checked after restriction along the envelope of a presentation, restriction along an envelope being injective”.

Stacks 0FAD. A relation between Chow cohomology classes on X may be proved after restricting along the envelope f : Y ⟶ X of a presentation of E: two classes of degree p on X whose restrictions to A^p(Y) agree are equal.

theorem eq_of_chowCohomologyRestriction_eq_of_envelopePresentation (C : ChowSituation.{u})
    (G : GysinSystem C) {X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    {E : DerivedCategory X.Modules} (H : EnvelopePresentation E) (p : ℤ)
    (hgys : G.IsNaturalUnderBaseChangeIso) {c d : chowCohomologyComponent C G sX p} :
    letI : IsProper H.f := H.envelope.isProper
    letI : LocallyOfFiniteType H.f := IsProper.toLocallyOfFiniteType
    chowCohomologyRestriction C G sX H.f p hgys c =
        chowCohomologyRestriction C G sX H.f p hgys d →
      c = d

Stacks.Chow.eq_of_forall_chowCohomologyRestriction_eq_of_hasDefinedChernClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/SplittingPrinciple.lean, line 167. The attribute's comment: “the splitting principle with the choice of envelope left open: the Chern classes of E being defined, a relation between bivariant classes on X follows from the relation after restriction along the envelope of every presentation”.

Stacks 0FAD. The same reduction with the envelope left to be chosen, as in the source: if the Chern classes of E are defined, then two Chow cohomology classes of degree p on X whose restrictions agree along the envelope of every presentation of E are equal.

theorem eq_of_forall_chowCohomologyRestriction_eq_of_hasDefinedChernClasses
    (C : ChowSituation.{u}) (G : GysinSystem C) {X : Scheme.{u}} (sX : X ⟶ C.S)
    [LocallyOfFiniteType sX] {E : DerivedCategory X.Modules} (hE : HasDefinedChernClasses E)
    (p : ℤ) (hgys : G.IsNaturalUnderBaseChangeIso) {c d : chowCohomologyComponent C G sX p}
    (h : ∀ H : EnvelopePresentation E,
      letI : IsProper H.f := H.envelope.isProper
      letI : LocallyOfFiniteType H.f := IsProper.toLocallyOfFiniteType
      chowCohomologyRestriction C G sX H.f p hgys c =
        chowCohomologyRestriction C G sX H.f p hgys d) :
    c = d

Stacks.Chow.exists_splitCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/SplittingPrinciplePerfect.lean, line 739. The attribute's comment: “the splitting principle: for every envelope f : Y -> X and complex E^bullet representing Lf^E there are split charts (the connected component of each point of Y, where E^bullet is bounded of fixed ranks, followed by the splitting morphism of 02UL filtering each term by invertible modules L_{n,j}), restriction to all of them is injective on A^(X), and on them c(E) = prod_{n even} (1 + x_{n,j}) prod_{n odd} (1 + x_{n,j})^{-1} and P_p(E) = sum_{n even} x_{n,j}^p - sum_{n odd} x_{n,j}^p with x_{n,j} = c_1(L_{n,j})”.

Let (S, δ), X and E be as in Definition 0F9E, the Chern classes of E being defined, and choose an envelope f : Y ⟶ X and a locally bounded complex ℰ^• of finite locally free 𝒪_Y-modules representing Lf^*E. Then there is a split chart π_y : P_y ⟶ V_y at every point y ∈ Y: over the connected component V_y of y, where ℰ^• is a bounded complex of finite locally free modules of fixed ranks, π_y is the splitting morphism of Stacks 02UL, along which each ℰ^n acquires a filtration with invertible successive quotients ℒ_{n,j}. For such a choice of charts:

  1. a relation between total Chow cohomology classes on X — in particular between the classes c_p(E) and P_p(E) — may be checked after restriction to all the charts: restriction A^*(X) ⟶ ∏_y A^*(P_y) is injective;
  2. with x_{n,j} = c_1(ℒ_{n,j}), on each chart c(E) = ∏_{n even} ∏_j (1 + x_{n,j}) · (∏_{n odd} ∏_j (1 + x_{n,j}))^{-1}, the factor 1 + x_{n,j} = c(ℒ_{n,j}) being a unit;
  3. with x_{n,j} = c_1(ℒ_{n,j}), on each chart P_p(E) = ∑_{n even} ∑_j x_{n,j}^p - ∑_{n odd} ∑_j x_{n,j}^p for every p ≥ 0.

Here c(E) and P_p(E) are the classes of Definition 0F9E (2).

theorem exists_splitCharts (hE : HasDefinedChernClasses E) (H : EnvelopePresentation E) :
    ∃ χ : ∀ y : H.Y, SplitChart C sX H y,
      Function.Injective (fun (c : TotalChowClass C sX) (y : H.Y) ↦ (χ y).res c) ∧
      (∀ y n j, ((χ y).rootFactor n j : TotalChowClass C (χ y).T.sP) = 1 + (χ y).root n j) ∧
      (∀ y, (χ y).res (perfectChernClass C sX hE) =
        ↑(((((complexRank H.locallyBounded y).support.sort (· ≤ ·)).filter fun n ↦ Even n).map
            fun n ↦ (List.ofFn ((χ y).rootFactor n)).prod).prod *
          (((((complexRank H.locallyBounded y).support.sort (· ≤ ·)).filter
            fun n ↦ ¬ Even n).map fun n ↦ (List.ofFn ((χ y).rootFactor n)).prod).prod)⁻¹)) ∧
      ∀ y (p : ℕ), (χ y).res (perfectPowerSum C sX hE p) =
        (∑ n ∈ (complexRank H.locallyBounded y).support with Even n,
            ∑ j, (χ y).root n j ^ p) -
          ∑ n ∈ (complexRank H.locallyBounded y).support with ¬ Even n,
            ∑ j, (χ y).root n j ^ p
Tag 0FAE, a lemma

Tag 0FAE in the Stacks Project.

Stacks.Chow.hasDefinedChernClasses_derivedDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DualChernClasses.lean, line 358. The attribute's comment: “the Chern classes of the derived dual are defined, which is what makes the assertion of the lemma well-typed”.

The Chern classes of the derived dual of a perfect object are defined as soon as those of the object are, [Stacks, Tag 0F9E] (1) for E^∨: dualize an envelope presentation of E.

This is what makes the assertion of [Stacks, Tag 0FAE] well-typed, the classes c_p, P_p and ch_p of [Stacks, Tag 0F9E] (2) being defined only under that hypothesis.

theorem hasDefinedChernClasses_derivedDual
    (hE : Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E)
    (h : HasDefinedChernClasses E) :
    HasDefinedChernClasses (Stacks.Chow.derivedDual E)

Stacks.Chow.perfectChernClass_apply_derivedDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DualChernClasses.lean, line 399. The attribute's comment: “the Chern classes: c_p(E-dual) = (-1)^p c_p(E) in A^p(X)”.

c_p(E^∨) = (-1)^p c_p(E) in A^p(X), the first conclusion of [Stacks, Tag 0FAE].

theorem perfectChernClass_apply_derivedDual
    (hE : Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E)
    (h : HasDefinedChernClasses E) (p : ℕ) :
    perfectChernClass C sX (hasDefinedChernClasses_derivedDual hE h) p =
      ((-1 : ℤ) ^ p) • perfectChernClass C sX h p

Stacks.Chow.perfectPowerSumComponent_derivedDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DualChernClasses.lean, line 428. The attribute's comment: “the power-sum classes: P_p(E-dual) = (-1)^p P_p(E) in A^p(X)”.

P_p(E^∨) = (-1)^p P_p(E) in A^p(X), the second conclusion of [Stacks, Tag 0FAE].

theorem perfectPowerSumComponent_derivedDual
    (hE : Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E)
    (h : HasDefinedChernClasses E) (p : ℕ) :
    perfectPowerSumComponent C sX (hasDefinedChernClasses_derivedDual hE h) p =
      ((-1 : ℤ) ^ p) • perfectPowerSumComponent C sX h p

Stacks.Chow.perfectChernCharacterComponent_derivedDual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DualChernClasses.lean, line 441. The attribute's comment: “the Chern character: ch_p(E-dual) = (-1)^p ch_p(E) in A^p(X) tensor Q”.

ch_p(E^∨) = (-1)^p ch_p(E) in A^p(X) ⊗ 𝐐, the third conclusion of [Stacks, Tag 0FAE]. The Chern character component is P_p/p!, so the sign passes through the tensor factor.

theorem perfectChernCharacterComponent_derivedDual
    (hE : Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E)
    (h : HasDefinedChernClasses E) (p : ℕ) :
    perfectChernCharacterComponent C sX (hasDefinedChernClasses_derivedDual hE h) p =
      ((-1 : ℤ) ^ p) • perfectChernCharacterComponent C sX h p
Tag 0FAF, a lemma

Tag 0FAF in the Stacks Project.

Stacks.Chow.perfectChernClass_derivedTwist_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectTwist.lean, line 253.

The Chern classes of a twist. Let X be locally of finite type over the base of chapter 42, let E be a perfect object of D(𝒪_X) whose Chern classes are defined and which has constant rank r, and let ℒ be an invertible 𝒪_X-module. Then

c_i(E ⊗ ℒ) = ∑_{j=0}^{i} binom(r - i + j, j) c_{i-j}(E) c_1(ℒ)^j

in A^i(X), where c_{i-j}(E) is the component of degree i - j of the total Chern class and the product is that of Chow cohomology.

theorem perfectChernClass_derivedTwist_apply (perfect : RingedSpace.IsPerfect.{u, u + 1} E)
    (definedChernClasses : HasDefinedChernClasses E) (r : ℤ)
    (constantRank : ∀ x : X, DerivedFibreBetti.chiDerivedFibre X E
      (DerivedFibreBetti.isPseudoCoherent_of_isPerfect E perfect) x = r) (i : ℕ) :
    perfectChernClass C sX (hasDefinedChernClasses_derivedTwist definedChernClasses L) i =
      ∑ j ∈ range (i + 1), Ring.choose (r - i + j) j •
        (TotalChowClass.homComponent (i - j) (perfectChernClass C sX definedChernClasses) *
          TotalChowClass.firstChernTotal C sX L ^ j) i
Tag 0FAG, a lemma

Tag 0FAG in the Stacks Project.

Stacks.Chow.perfectChernClass_derivedTensor_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DerivedTensor.lean, line 349. The attribute's comment: “the formula for c_1(E tensor^L F), for objects E, F of D(O_X) whose Chern classes are defined; perfectness is not needed. The rank r(E) is the class P_0(E) = perfectPowerSum C sX hE 0 in A^0(X), not assumed constant, and r(E) c_1(F) is the product in the ring TotalChowClass C sX of total Chow cohomology classes. E tensor^L F is the derived tensor product derivedTensorProductFunctor of Stacks 06YU”.

The first Chern class of a derived tensor product. For objects E, F of D(𝒪_X) whose Chern classes are defined,

c₁(E ⊗^L F) = r(E) c₁(F) + r(F) c₁(E)

in A^*(X), where r(E) = P_0(E) is the rank and c₁ the degree-one part of the total Chern class.

theorem perfectChernClass_derivedTensor_one :
    TotalChowClass.homComponent 1 (perfectChernClass C sX hEF) =
      perfectPowerSum C sX hE 0 * TotalChowClass.homComponent 1 (perfectChernClass C sX hF) +
        perfectPowerSum C sX hF 0 * TotalChowClass.homComponent 1 (perfectChernClass C sX hE)

Stacks.Chow.perfectPowerSum_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DerivedTensor.lean, line 395. The attribute's comment: “the precise form P_p(E tensor^L F) = sum over p_1 + p_2 = p of C(p, p_1) P_{p_1}(E) P_{p_2}(F) in A^p(X), for every p >= 0, for objects E, F of D(O_X) whose Chern classes are defined (perfectness is not needed); P_p is perfectPowerSum of Stacks 0GUD, P_0 being the rank, and the products are those of TotalChowClass C sX. The statement ch(E tensor F) = ch(E) ch(F) in A^*(X) tensor Q is the consequence of this identity obtained by dividing by p!, which is not stated separately”.

The power sums of a derived tensor product. For objects E, F of D(𝒪_X) whose Chern classes are defined and every p ≥ 0,

P_p(E ⊗^L F) = ∑_{p₁ + p₂ = p} C(p, p₁) P_{p₁}(E) P_{p₂}(F)

in A^p(X), the power sums P_0 being the ranks; dividing by p! this is ch(E ⊗^L F) = ch(E) ch(F).

theorem perfectPowerSum_derivedTensor (p : ℕ) :
    perfectPowerSum C sX hEF p =
      ∑ q ∈ antidiagonal p, (p.choose q.1 : ℤ) •
        (perfectPowerSum C sX hE q.1 * perfectPowerSum C sX hF q.2)

Stacks.Chow.perfectChernClass_derivedTensor_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/DerivedTensor.lean, line 440. The attribute's comment: “the formula for c_2(E tensor^L F), for perfect objects E, F of D(O_X) whose Chern classes are defined, the ranks being arbitrary locally constant functions. r(E) is the class P_0(E) = perfectPowerSum C sX hE 0 in A^0(X); the binomial coefficient C(r(E), 2) is read as the class ofLocallyConstant of the locally constant function x |-> Ring.choose (chi_E(x)) 2, chi_E the derived-fibre Euler characteristic, whose own class is r(E) by perfectPowerSum_zero_eq_ofLocallyConstant; on the open and closed subscheme where E has rank r these are the integers r and C(r, 2), as in Remark 0FA7. The products are those of TotalChowClass C sX, written in the order of the source. The source's 'and so on for higher Chern classes' is not a precise assertion and is not formalized”.

The second Chern class of a derived tensor product. For perfect objects E, F of D(𝒪_X) whose Chern classes are defined,

c₂(E ⊗^L F) = r(E) c₂(F) + r(F) c₂(E) + C(r(E), 2) c₁(F)² + (r(E) r(F) - 1) c₁(F) c₁(E) + C(r(F), 2) c₁(E)²

in A^*(X), where r(E) = P_0(E) is the rank and C(r(E), 2) is the class of the locally constant function x ↦ C(χ_E(x), 2), χ_E being the Euler characteristic of the derived fibre of E, whose class is r(E) (Stacks.Chow.perfectPowerSum_zero_eq_ofLocallyConstant).

theorem perfectChernClass_derivedTensor_two (perfectE : RingedSpace.IsPerfect.{u, u + 1} E)
    (perfectF : RingedSpace.IsPerfect.{u, u + 1} F) :
    TotalChowClass.homComponent 2 (perfectChernClass C sX hEF) =
      perfectPowerSum C sX hE 0 * TotalChowClass.homComponent 2 (perfectChernClass C sX hF) +
        perfectPowerSum C sX hF 0 * TotalChowClass.homComponent 2 (perfectChernClass C sX hE) +
        ofLocallyConstant C sX ((perfectRank E perfectE).map fun k ↦ Ring.choose k 2) *
          TotalChowClass.homComponent 1 (perfectChernClass C sX hF) ^ 2 +
        (perfectPowerSum C sX hE 0 * perfectPowerSum C sX hF 0 - 1) *
          (TotalChowClass.homComponent 1 (perfectChernClass C sX hF) *
            TotalChowClass.homComponent 1 (perfectChernClass C sX hE)) +
        ofLocallyConstant C sX ((perfectRank F perfectF).map fun k ↦ Ring.choose k 2) *
          TotalChowClass.homComponent 1 (perfectChernClass C sX hE) ^ 2

Stacks.Chow.exists_tensorSplitCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectTensorChernClasses.lean, line 228. The attribute's comment: “and so on for higher Chern classes: the splitting-principle statement the proof reduces the lemma to. On tensor split charts of any two envelope presentations of E and F -- the connected component of a point of the common envelope followed by one splitting morphism of 02UL for the terms of both presenting complexes -- restriction is injective on A^*(X), c(E) and c(F) are the products of (1 + x)^{(-1)^n} and (1 + y)^{(-1)^m} over their Chern roots, and c(E tensor^L F) is the product of (1 + x + y)^{(-1)^n (-1)^m} over all pairs of roots, as lists of signed roots via Stacks.Chow.TotalChowClass.rootProd and Stacks.Chow.rootTensor”.

The Chern roots of E ⊗^𝐋 F are the sums of the Chern roots of E and F. For presentations of E and F on envelopes there are tensor split charts at every point of their common envelope, restriction to all of them is injective on A^*(X), and on each of them, with x_{n,j} the Chern roots of E and y_{m,k} those of F,

c(E) = ∏ (1 + x_{n,j})^{(-1)^n}, c(F) = ∏ (1 + y_{m,k})^{(-1)^m}, c(E ⊗^𝐋 F) = ∏ (1 + x_{n,j} + y_{m,k})^{(-1)^n (-1)^m},

so every Chern class of E ⊗^𝐋 F is the universal expression in the Chern roots of E and F.

theorem exists_tensorSplitCharts (hE : HasDefinedChernClasses E) (hF : HasDefinedChernClasses F)
    (H : EnvelopePresentation E) (H' : EnvelopePresentation F) :
    ∃ χ : ∀ y : (H.tensorLeft H').Y, TensorSplitChart C sX H H' y,
      Function.Injective
        (fun (c : TotalChowClass C sX) (y : (H.tensorLeft H').Y) ↦ (χ y).left.res c) ∧
      (∀ y, (χ y).left.res (perfectChernClass C sX hE) =
        ((TotalChowClass.rootProd (χ y).rootsLeft : (TotalChowClass C (χ y).T.sP)ˣ) :
          TotalChowClass C (χ y).T.sP)) ∧
      (∀ y, (χ y).left.res (perfectChernClass C sX hF) =
        ((TotalChowClass.rootProd (χ y).rootsRight : (TotalChowClass C (χ y).T.sP)ˣ) :
          TotalChowClass C (χ y).T.sP)) ∧
      ∀ y, (χ y).left.res (perfectChernClass C sX (hasDefinedChernClasses_derivedTensor hE hF)) =
        ((TotalChowClass.rootProd (rootTensor (χ y).rootsLeft (χ y).rootsRight) :
          (TotalChowClass C (χ y).T.sP)ˣ) : TotalChowClass C (χ y).T.sP)

Stacks.Chow.homComponent_one_perfectChernClass_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectTensorChernClasses.lean, line 254. The attribute's comment: “the first displayed formula c_1(E tensor^L F) = r(E) c_1(F) + r(F) c_1(E), as classes homogeneous of degree one in the bivariant ring A^*(X) = Stacks.Chow.TotalChowClass, with r = Stacks.Chow.perfectRankClass and c_1 the degree-one homogeneous component of Stacks.Chow.perfectChernClass; the Chern classes of E tensor^L F are defined by Stacks.Chow.hasDefinedChernClasses_derivedTensor. Perfectness of E and F is not used”.

c₁(E ⊗^𝐋 F) = r(E) c₁(F) + r(F) c₁(E) in A^*(X).

theorem homComponent_one_perfectChernClass_derivedTensor (hE : HasDefinedChernClasses E)
    (hF : HasDefinedChernClasses F) :
    TotalChowClass.homComponent 1
        (perfectChernClass C sX (hasDefinedChernClasses_derivedTensor hE hF)) =
      perfectRankClass C sX hE * TotalChowClass.homComponent 1 (perfectChernClass C sX hF) +
        perfectRankClass C sX hF * TotalChowClass.homComponent 1 (perfectChernClass C sX hE)

Stacks.Chow.homComponent_two_perfectChernClass_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectTensorChernClasses.lean, line 278. The attribute's comment: “the second displayed formula c_2(E tensor^L 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, as classes homogeneous of degree two in the bivariant ring A^*(X) = Stacks.Chow.TotalChowClass, the products being compositions of bivariant classes, in the order of the source. r is Stacks.Chow.perfectRankClass and binom(r, 2) is Stacks.Chow.perfectRankChooseClass ... 2, the class which is binom(n, 2) on the open and closed locus where the rank of the perfect object is n; E and F perfect as in the source”.

c₂(E ⊗^𝐋 F) = r(E) c₂(F) + r(F) c₂(E) + C(r(E), 2) c₁(F)² + (r(E) r(F) - 1) c₁(F) c₁(E) + C(r(F), 2) c₁(E)² in A^*(X).

theorem homComponent_two_perfectChernClass_derivedTensor
    (perfectE : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) E)
    (perfectF : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) F)
    (hE : HasDefinedChernClasses E) (hF : HasDefinedChernClasses F) :
    TotalChowClass.homComponent 2
        (perfectChernClass C sX (hasDefinedChernClasses_derivedTensor hE hF)) =
      perfectRankClass C sX hE * TotalChowClass.homComponent 2 (perfectChernClass C sX hF) +
        perfectRankClass C sX hF * TotalChowClass.homComponent 2 (perfectChernClass C sX hE) +
        perfectRankChooseClass C sX perfectE 2 *
          TotalChowClass.homComponent 1 (perfectChernClass C sX hF) ^ 2 +
        (perfectRankClass C sX hE * perfectRankClass C sX hF - 1) *
          (TotalChowClass.homComponent 1 (perfectChernClass C sX hF) *
            TotalChowClass.homComponent 1 (perfectChernClass C sX hE)) +
        perfectRankChooseClass C sX perfectF 2 *
          TotalChowClass.homComponent 1 (perfectChernClass C sX hE) ^ 2

Stacks.Chow.perfectChernClass_derivedTensor_apply_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectTensorChernClasses.lean, line 317. The attribute's comment: “the first displayed formula read in the single group A^1(X): c_1(E tensor^L F) in A^1(X), the degree-one component of Stacks.Chow.perfectChernClass, is the degree-one component of r(E) c_1(F) + r(F) c_1(E)”.

The class c₁(E ⊗^𝐋 F) ∈ A¹(X) is the degree-one component of r(E) c₁(F) + r(F) c₁(E).

theorem perfectChernClass_derivedTensor_apply_one (hE : HasDefinedChernClasses E)
    (hF : HasDefinedChernClasses F) :
    perfectChernClass C sX (hasDefinedChernClasses_derivedTensor hE hF) 1 =
      (perfectRankClass C sX hE * TotalChowClass.homComponent 1 (perfectChernClass C sX hF) +
        perfectRankClass C sX hF * TotalChowClass.homComponent 1 (perfectChernClass C sX hE))
        1

Stacks.Chow.perfectChernClass_derivedTensor_apply_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectTensorChernClasses.lean, line 333. The attribute's comment: “the second displayed formula read in the single group A^2(X): c_2(E tensor^L F) in A^2(X), the degree-two component of Stacks.Chow.perfectChernClass, is the degree-two component of 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; E and F perfect as in the source”.

The class c₂(E ⊗^𝐋 F) ∈ A²(X) is the degree-two component of r(E) c₂(F) + r(F) c₂(E) + C(r(E), 2) c₁(F)² + (r(E) r(F) - 1) c₁(F) c₁(E) + C(r(F), 2) c₁(E)².

theorem perfectChernClass_derivedTensor_apply_two
    (perfectE : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) E)
    (perfectF : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) F)
    (hE : HasDefinedChernClasses E) (hF : HasDefinedChernClasses F) :
    perfectChernClass C sX (hasDefinedChernClasses_derivedTensor hE hF) 2 =
      (perfectRankClass C sX hE * TotalChowClass.homComponent 2 (perfectChernClass C sX hF) +
        perfectRankClass C sX hF * TotalChowClass.homComponent 2 (perfectChernClass C sX hE) +
        perfectRankChooseClass C sX perfectE 2 *
          TotalChowClass.homComponent 1 (perfectChernClass C sX hF) ^ 2 +
        (perfectRankClass C sX hE * perfectRankClass C sX hF - 1) *
          (TotalChowClass.homComponent 1 (perfectChernClass C sX hF) *
            TotalChowClass.homComponent 1 (perfectChernClass C sX hE)) +
        perfectRankChooseClass C sX perfectF 2 *
          TotalChowClass.homComponent 1 (perfectChernClass C sX hE) ^ 2 : TotalChowClass C sX)
        2

Stacks.Chow.perfectPowerSumComponent_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectTensorChernClasses.lean, line 356. The attribute's comment: “the more precise statement read in the single group A^p(X), which is where the source states it: P_p(E tensor^L F) in A^p(X) (Stacks.Chow.perfectPowerSumComponent) is the degree-p component of the sum over p_1 + p_2 = p of binom(p, p_1) P_{p_1}(E) P_{p_2}(F)”.

P_p(E ⊗^𝐋 F) ∈ A^p(X) is the degree-p component of ∑_{p₁ + p₂ = p} C(p, p₁) P_{p₁}(E) P_{p₂}(F).

theorem perfectPowerSumComponent_derivedTensor (hE : HasDefinedChernClasses E)
    (hF : HasDefinedChernClasses F) (p : ℕ) :
    perfectPowerSumComponent C sX (hasDefinedChernClasses_derivedTensor hE hF) p =
      ∑ q ∈ antidiagonal p, ((p.choose q.1 : TotalChowClass C sX) *
        (perfectPowerSum C sX hE q.1 * perfectPowerSum C sX hF q.2)) p

Stacks.Chow.perfectTotalChernCharacter_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectTensorChernClasses.lean, line 446. The attribute's comment: “similarly, ch(E tensor^L F) = ch(E) ch(F) in A^(X) tensor Q: Stacks.Chow.rationalTotalChowClass is the bivariant ring A^(X) tensored over Z with Q, and ch is the power series over it whose coefficient of degree p is P_p/p!, which read in A^p(X) tensor Q is ch_p of Tag 0F9E (Stacks.Chow.map_coeff_perfectTotalChernCharacter); the identity is the more precise one for P_p divided by p!. Perfectness of E and F is not used”.

The Chern character is multiplicative: ch(E ⊗^𝐋 F) = ch(E) ch(F) in A^*(X) ⊗ 𝐐.

theorem perfectTotalChernCharacter_derivedTensor (hE : HasDefinedChernClasses E)
    (hF : HasDefinedChernClasses F) :
    perfectTotalChernCharacter C sX (hasDefinedChernClasses_derivedTensor hE hF) =
      perfectTotalChernCharacter C sX hE * perfectTotalChernCharacter C sX hF

Stacks.Chow.perfectChernClasses_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectTensorChernClasses.lean, line 481. The attribute's comment: “the whole statement, as one conjunction of the parts registered separately in this module: the Chern classes of E tensor^L F are defined; the formulas for c_1 and c_2 in A^(X); the splitting-principle form of 'and so on for higher Chern classes' (Chern roots x + y with product signs on injective tensor split charts of any presentations); ch(E tensor^L F) = ch(E) ch(F) in A^(X) tensor Q; and P_p(E tensor^L F) = sum of binom(p, p_1) P_{p_1}(E) P_{p_2}(F) in A^p(X) for every p, under exactly the source's hypotheses”.

In Situation 02QL let X be locally of finite type over S and let E, F be perfect objects of D(𝒪_X) whose Chern classes are defined. Then the Chern classes of E ⊗^𝐋 F are defined, and in A^*(X)

  • c₁(E ⊗^𝐋 F) = r(E) c₁(F) + r(F) c₁(E);
  • `c₂(E ⊗^𝐋 F) = r(E) c₂(F) + r(F) c₂(E) + C(r(E), 2) c₁(F)² + (r(E) r(F) - 1) c₁(F) c₁(E)
  • C(r(F), 2) c₁(E)²`;
  • "and so on for higher Chern classes": on tensor split charts of any presentations, on which restriction is injective, the Chern roots of E ⊗^𝐋 F are the sums x + y of those of E and F, with the product signs;
  • ch(E ⊗^𝐋 F) = ch(E) ch(F) in A^*(X) ⊗ 𝐐;
  • more precisely P_p(E ⊗^𝐋 F) = ∑_{p₁ + p₂ = p} C(p, p₁) P_{p₁}(E) P_{p₂}(F) in A^p(X).
theorem perfectChernClasses_derivedTensor
    (perfectE : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) E)
    (perfectF : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) F)
    (hE : HasDefinedChernClasses E) (hF : HasDefinedChernClasses F) :
    HasDefinedChernClasses (((derivedTensorProductFunctor X.sheaf).obj E).obj F) ∧
    TotalChowClass.homComponent 1
        (perfectChernClass C sX (hasDefinedChernClasses_derivedTensor hE hF)) =
      perfectRankClass C sX hE * TotalChowClass.homComponent 1 (perfectChernClass C sX hF) +
        perfectRankClass C sX hF * TotalChowClass.homComponent 1 (perfectChernClass C sX hE) ∧
    TotalChowClass.homComponent 2
        (perfectChernClass C sX (hasDefinedChernClasses_derivedTensor hE hF)) =
      perfectRankClass C sX hE * TotalChowClass.homComponent 2 (perfectChernClass C sX hF) +
        perfectRankClass C sX hF * TotalChowClass.homComponent 2 (perfectChernClass C sX hE) +
        perfectRankChooseClass C sX perfectE 2 *
          TotalChowClass.homComponent 1 (perfectChernClass C sX hF) ^ 2 +
        (perfectRankClass C sX hE * perfectRankClass C sX hF - 1) *
          (TotalChowClass.homComponent 1 (perfectChernClass C sX hF) *
            TotalChowClass.homComponent 1 (perfectChernClass C sX hE)) +
        perfectRankChooseClass C sX perfectF 2 *
          TotalChowClass.homComponent 1 (perfectChernClass C sX hE) ^ 2 ∧
    (∀ (H : EnvelopePresentation E) (H' : EnvelopePresentation F),
      ∃ χ : ∀ y : (H.tensorLeft H').Y, TensorSplitChart C sX H H' y,
        Function.Injective (fun (c : TotalChowClass C sX) (y : (H.tensorLeft H').Y) ↦
          (χ y).left.res c) ∧
        (∀ y, (χ y).left.res (perfectChernClass C sX hE) =
          ((TotalChowClass.rootProd (χ y).rootsLeft : (TotalChowClass C (χ y).T.sP)ˣ) :
            TotalChowClass C (χ y).T.sP)) ∧
        (∀ y, (χ y).left.res (perfectChernClass C sX hF) =
          ((TotalChowClass.rootProd (χ y).rootsRight : (TotalChowClass C (χ y).T.sP)ˣ) :
            TotalChowClass C (χ y).T.sP)) ∧
        ∀ y, (χ y).left.res (perfectChernClass C sX (hasDefinedChernClasses_derivedTensor hE hF)) =
          ((TotalChowClass.rootProd (rootTensor (χ y).rootsLeft (χ y).rootsRight) :
            (TotalChowClass C (χ y).T.sP)ˣ) : TotalChowClass C (χ y).T.sP)) ∧
    perfectTotalChernCharacter C sX (hasDefinedChernClasses_derivedTensor hE hF) =
      perfectTotalChernCharacter C sX hE * perfectTotalChernCharacter C sX hF ∧
    ∀ p : ℕ, perfectPowerSumComponent C sX (hasDefinedChernClasses_derivedTensor hE hF) p =
      ∑ q ∈ antidiagonal p, ((p.choose q.1 : TotalChowClass C sX) *
        (perfectPowerSum C sX hE q.1 * perfectPowerSum C sX hF q.2)) p
Sources

Section42.47 A baby case of localized Chern classes#

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

Tag 0F9H, a lemma

Tag 0F9H in the Stacks Project.

Stacks.Chow.existsUnique_localizedChernClassOfClosedCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedChernClass.lean, line 125. The attribute's comment: “the class c'_p(E₂) ∈ A^p(X₂ ⟶ X), existence and uniqueness of the bivariant class characterized by the two identities on every base change X' ⟶ X, for E₂|_{X₁ ∩ X₂} finite locally free of rank < p in degree 0”.

Stacks 0F9H, for the Chern classes. Let X be locally of finite type over S, let i_j : X_j ⟶ X be closed immersions with X = X₁ ∪ X₂ set theoretically, and let E₂ be a perfect object of D(𝒪_{X₂}) whose Chern classes are defined and such that E₂|_{X₁ ∩ X₂} is isomorphic to a finite locally free 𝒪_{X₁ ∩ X₂}-module of rank < p sitting in cohomological degree 0. Then there is a unique bivariant class c'_p(E₂) ∈ A^p(X₂ ⟶ X) such that, on every test scheme g : X' ⟶ X locally of finite type, with i'_j : X'_j = X_j ×_X X' ⟶ X',

c'_p(E₂) ∩ i'_{2,*} α₂ = c_p(E₂) ∩ α₂ and c'_p(E₂) ∩ i'_{1,*} α₁ = 0

for all α_j ∈ CH_k(X'_j); it is Stacks.Chow.localizedChernClassOfClosedCover.

theorem existsUnique_localizedChernClassOfClosedCover
    (_perfect : RingedSpace.IsPerfect.{u, u + 1} (X := X₂.toRingedSpace) E₂)
    (hres : ∃ M : (pullback i₁ i₂).Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂ ≅
        (DerivedCategory.singleFunctor (pullback i₁ i₂).Modules 0).obj M)) :
    ∃! c : BivariantClass C (gysinSystemOfInvertible C) (i₂ ≫ sX) sX i₂ rfl (p : ℤ),
      (∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (pullback.fst i₂ g ≫ i₂ ≫ sX) k),
        c.cap g k (chowPush C (pullback.fst i₂ g ≫ i₂ ≫ sX) (g ≫ sX) (pullback.snd i₂ g)
            (pullbackSnd_comp_structureMorphism_eq C (i₂ ≫ sX) sX i₂ rfl g) k α) =
          (perfectChernClass C (i₂ ≫ sX) hE₂ p).idRule C (i₂ ≫ sX) (gysinSystemOfInvertible C)
            (pullback.fst i₂ g) k α) ∧
      (∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (pullback.fst i₁ g ≫ i₁ ≫ sX) k),
        c.cap g k (chowPush C (pullback.fst i₁ g ≫ i₁ ≫ sX) (g ≫ sX) (pullback.snd i₁ g)
            (pullbackSnd_comp_structureMorphism_eq C (i₁ ≫ sX) sX i₁ rfl g) k α) = 0)

Stacks.Chow.existsUnique_localizedPowerSumOfClosedCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedChernClass.lean, line 179. The attribute's comment: “the class P'_p(E₂) ∈ A^p(X₂ ⟶ X), existence and uniqueness of the bivariant class characterized by the two identities on every base change X' ⟶ X, for E₂|_{X₁ ∩ X₂} zero”.

Stacks 0F9H, for the classes P_p. Let X be locally of finite type over S, let i_j : X_j ⟶ X be closed immersions with X = X₁ ∪ X₂ set theoretically, and let E₂ be a perfect object of D(𝒪_{X₂}) whose Chern classes are defined and whose restriction E₂|_{X₁ ∩ X₂} is zero. Then there is a unique bivariant class P'_p(E₂) ∈ A^p(X₂ ⟶ X) such that, on every test scheme g : X' ⟶ X locally of finite type, with i'_j : X'_j = X_j ×_X X' ⟶ X',

P'_p(E₂) ∩ i'_{2,*} α₂ = P_p(E₂) ∩ α₂ and P'_p(E₂) ∩ i'_{1,*} α₁ = 0

for all α_j ∈ CH_k(X'_j); it is Stacks.Chow.localizedPowerSumOfClosedCover. Here P_p(E₂) is the class of Definition 0F9E (2), Stacks.Chow.perfectPowerSumComponent: the class of Stacks 0GUD which restricts along every envelope presentation (f, 𝓔^•) of E₂ to ∑ (-1)^n P_p(𝓔^n) (Stacks.Chow.existsUnique_perfectPowerSum).

theorem existsUnique_localizedPowerSumOfClosedCover
    (perfect : RingedSpace.IsPerfect.{u, u + 1} (X := X₂.toRingedSpace) E₂)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂)) :
    ∃! c : BivariantClass C (gysinSystemOfInvertible C) (i₂ ≫ sX) sX i₂ rfl (p : ℤ),
      (∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (pullback.fst i₂ g ≫ i₂ ≫ sX) k),
        c.cap g k (chowPush C (pullback.fst i₂ g ≫ i₂ ≫ sX) (g ≫ sX) (pullback.snd i₂ g)
            (pullbackSnd_comp_structureMorphism_eq C (i₂ ≫ sX) sX i₂ rfl g) k α) =
          (perfectPowerSumComponent C (i₂ ≫ sX) hE₂ p).idRule C (i₂ ≫ sX)
            (gysinSystemOfInvertible C) (pullback.fst i₂ g) k α) ∧
      (∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (pullback.fst i₁ g ≫ i₁ ≫ sX) k),
        c.cap g k (chowPush C (pullback.fst i₁ g ≫ i₁ ≫ sX) (g ≫ sX) (pullback.snd i₁ g)
            (pullbackSnd_comp_structureMorphism_eq C (i₁ ≫ sX) sX i₁ rfl g) k α) = 0)

Stacks.Chow.closedCoverPowerSum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCase.lean, line 148. The attribute's comment: “the class P'_p(E₂) in A^p(X₂ ⟶ X), for E₂ restricting to zero on X₁ ∩ X₂”.

Let i₁ : X₁ ⟶ X and i₂ : X₂ ⟶ X be closed immersions whose images cover X, and let E₂ ∈ D(𝒪_{X₂}) have defined Chern classes and restrict to zero on X₁ ×_X X₂. The class P'_p(E₂) ∈ A^p(X₂ ⟶ X) is the extension of P_p(E₂) ∈ A^p(X₂) along the closed cover (Stacks.Chow.closedCoverExtension): on a test scheme T ⟶ X, writing a class as j_{1,*} α₁ + j_{2,*} α₂ along the base-changed cover, P'_p(E₂) ∩ α = P_p(E₂) ∩ α₂.

def closedCoverPowerSum (hcover : Set.range i₁ ∪ Set.range i₂ = Set.univ)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂)) :
    BivariantClass C (gysinSystemOfInvertible C) sX₂ sX i₂ hi₂ p

Stacks.Chow.closedCoverChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCase.lean, line 163. The attribute's comment: “the class c'_p(E₂) in A^p(X₂ ⟶ X), for E₂ restricting on X₁ ∩ X₂ to a finite locally free module of rank < p in degree 0”.

Let i₁ : X₁ ⟶ X and i₂ : X₂ ⟶ X be closed immersions whose images cover X, and let E₂ ∈ D(𝒪_{X₂}) have defined Chern classes and restrict on X₁ ×_X X₂ to a finite locally free module of rank < p in degree 0. The class c'_p(E₂) ∈ A^p(X₂ ⟶ X) is the extension of c_p(E₂) ∈ A^p(X₂) along the closed cover (Stacks.Chow.closedCoverExtension): on a test scheme T ⟶ X, writing a class as j_{1,*} α₁ + j_{2,*} α₂ along the base-changed cover, c'_p(E₂) ∩ α = c_p(E₂) ∩ α₂.

def closedCoverChernClass (hcover : Set.range i₁ ∪ Set.range i₂ = Set.univ)
    (hrank : ∃ M : (pullback i₁ i₂).Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂ ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) :
    BivariantClass C (gysinSystemOfInvertible C) sX₂ sX i₂ hi₂ p

Stacks.Chow.isClosedCoverExtension_closedCoverPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCase.lean, line 184. The attribute's comment: “the two formulas P'_p(E₂) ∩ i_{2,} α₂ = P_p(E₂) ∩ α₂ and P'_p(E₂) ∩ i_{1,} α₁ = 0, after every base change”.

On every test scheme g : T ⟶ X locally of finite type, P'_p(E₂) caps the classes pushed forward from T ×_X X₂ as P_p(E₂) does, and kills the classes pushed forward from T ×_X X₁: P'_p(E₂) ∩ i_{2,*} α₂ = P_p(E₂) ∩ α₂ and P'_p(E₂) ∩ i_{1,*} α₁ = 0.

theorem isClosedCoverExtension_closedCoverPowerSum :
    IsClosedCoverExtension C (gysinSystemOfInvertible C) sX i₁ i₂ sX₂ hi₂
      (perfectPowerSumComponent C sX₂ hE₂ p)
      (closedCoverPowerSum C sX i₁ i₂ sX₂ hi₂ hE₂ p hcover hzero)

Stacks.Chow.eq_closedCoverPowerSum_of_isClosedCoverExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCase.lean, line 195. The attribute's comment: “uniqueness: P'_p(E₂) is the only class satisfying the two formulas after every base change”.

A class of A^p(X₂ ⟶ X) satisfying the two formulas c ∩ i_{2,*} α₂ = P_p(E₂) ∩ α₂ and c ∩ i_{1,*} α₁ = 0 after every base change is P'_p(E₂).

theorem eq_closedCoverPowerSum_of_isClosedCoverExtension
    {c : BivariantClass C (gysinSystemOfInvertible C) sX₂ sX i₂ hi₂ p}
    (hc : IsClosedCoverExtension C (gysinSystemOfInvertible C) sX i₁ i₂ sX₂ hi₂
      (perfectPowerSumComponent C sX₂ hE₂ p) c) :
    c = closedCoverPowerSum C sX i₁ i₂ sX₂ hi₂ hE₂ p hcover hzero

Stacks.Chow.isClosedCoverExtension_closedCoverChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCase.lean, line 217. The attribute's comment: “the two formulas c'_p(E₂) ∩ i_{2,} α₂ = c_p(E₂) ∩ α₂ and c'_p(E₂) ∩ i_{1,} α₁ = 0, after every base change”.

On every test scheme g : T ⟶ X locally of finite type, c'_p(E₂) caps the classes pushed forward from T ×_X X₂ as c_p(E₂) does, and kills the classes pushed forward from T ×_X X₁: c'_p(E₂) ∩ i_{2,*} α₂ = c_p(E₂) ∩ α₂ and c'_p(E₂) ∩ i_{1,*} α₁ = 0.

theorem isClosedCoverExtension_closedCoverChernClass :
    IsClosedCoverExtension C (gysinSystemOfInvertible C) sX i₁ i₂ sX₂ hi₂
      (perfectChernClass C sX₂ hE₂ p)
      (closedCoverChernClass C sX i₁ i₂ sX₂ hi₂ hE₂ p hcover hrank)

Stacks.Chow.eq_closedCoverChernClass_of_isClosedCoverExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCase.lean, line 228. The attribute's comment: “uniqueness: c'_p(E₂) is the only class satisfying the two formulas after every base change”.

A class of A^p(X₂ ⟶ X) satisfying the two formulas c ∩ i_{2,*} α₂ = c_p(E₂) ∩ α₂ and c ∩ i_{1,*} α₁ = 0 after every base change is c'_p(E₂).

theorem eq_closedCoverChernClass_of_isClosedCoverExtension
    {c : BivariantClass C (gysinSystemOfInvertible C) sX₂ sX i₂ hi₂ p}
    (hc : IsClosedCoverExtension C (gysinSystemOfInvertible C) sX i₁ i₂ sX₂ hi₂
      (perfectChernClass C sX₂ hE₂ p) c) :
    c = closedCoverChernClass C sX i₁ i₂ sX₂ hi₂ hE₂ p hcover hrank
Tag 0FAH, a lemma

Tag 0FAH in the Stacks Project.

Stacks.Chow.eq_of_isClosedCoverLocalizedClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/ClosedCoverLocalizedClass.lean, line 284. The attribute's comment: “the conclusion in full: the class of Stacks 0F9H in A^p(X_2 -> X) does not depend on the choice of X_1, in the form that two bivariant classes with the characterizing property of Stacks 0F9H for the covers X = X_1 cup X_2 and X = X_1' cup X_2 and for the same class on X_2 are equal. CARRIED, because the Chern classes of a perfect object are not constructed in this repository (only the uniqueness half of Stacks 0GUD is formalized): the class on X_2 that the localized class caps as is a parameter kappa in A^p(X_2), covering the P_p(E_2) and c_p(E_2) halves of the source at once, and the two localized classes are parameters satisfying the characterizing property of Stacks 0F9H rather than its output. NOT NEEDED, since that property is all the source's proof uses: that E_2 is perfect, that its Chern classes are defined, and that its restriction to X_1 cap X_2 resp. X_1' cap X_2 is zero resp. finite locally free of rank < p in degree 0.”.

Stacks 0FAH. The localized class of Stacks 0F9H does not depend on the choice of X₁: if c has the characterizing property for the cover X = X₁ ∪ X₂ and c' has it for the cover X = X₁' ∪ X₂, both with the same class κ ∈ A^p(X₂), then c = c'.

By Stacks 02UC it is enough that c - c' kill the fundamental class of every integral scheme T locally of finite type over X. Such a T is irreducible and covered by the base changes of the two closed subschemes of whichever cover, so for each cover one of the two pieces is the whole of T; being a surjective closed immersion into a reduced scheme that piece is an isomorphism, and [T] is the pushforward of the fundamental class of the piece. If the X₂-piece fills T then both classes cap [T] to κ ∩ [T]; otherwise the X₁-piece and the X₁'-piece both fill T, and both classes cap [T] to zero.

theorem eq_of_isClosedCoverLocalizedClass
    (hcover : Set.range i₁.base ∪ Set.range i₂.base = Set.univ)
    (hcover' : Set.range i₁'.base ∪ Set.range i₂.base = Set.univ)
    {κ : chowCohomologyComponent C G sX₂ p} {c c' : BivariantClass C G sX₂ sX i₂ hi₂ p}
    (hc : IsClosedCoverLocalizedClass C G sX sX₁ sX₂ i₁ hi₁ i₂ hi₂ p κ c)
    (hc' : IsClosedCoverLocalizedClass C G sX sX₁' sX₂ i₁' hi₁' i₂ hi₂ p κ c') :
    c = c'
Tag 0GUG, a lemma

Tag 0GUG in the Stacks Project.

Stacks.Chow.localizedChernClassOfClosedCover_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedChernBaseChange.lean, line 460. The attribute's comment: “the classes c'_p: c'_p(E'₂) built from X' = X'₁ ∪ X'₂ and E'₂ is the restriction of c'_p(E₂)”.

Stacks 0GUG, for the Chern classes. In the situation of Stacks 0F9H, with E₂|_{X₁ ∩ X₂} finite locally free of rank < p in degree 0, let q : X' ⟶ X be locally of finite type, let X' = X'₁ ∪ X'₂ with X'_j = X_j ×_X X', and let E'₂ = (X'₂ ⟶ X₂)^* E₂. Then E'₂ satisfies the hypotheses of Stacks 0F9H for this cover, and the class c'_p(E'₂) ∈ A^p(X'₂ ⟶ X') constructed by Stacks 0F9H from X' = X'₁ ∪ X'₂ and E'₂ is the restriction (Remark 0F9Z) of c'_p(E₂) ∈ A^p(X₂ ⟶ X).

The restriction is a class for X₂ ×_X X' ⟶ X' whose source carries the structure morphism X₂ ×_X X' ⟶ X₂ ⟶ S, while the class of Stacks 0F9H at X' carries X'₂ ⟶ X' ⟶ S; the two are equal, and the restriction is read with the second one by Stacks.Chow.bivariantTransport along the identity.

theorem localizedChernClassOfClosedCover_baseChange
    (hres : ∃ M : (pullback i₁ i₂).Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂ ≅
        (DerivedCategory.singleFunctor (pullback i₁ i₂).Modules 0).obj M)) :
    localizedChernClassOfClosedCover C (q ≫ sX) (pullback.snd i₁ q) (pullback.snd i₂ q)
        (range_pullbackSnd_union_range_pullbackSnd i₁ i₂ hcover q)
        (hasDefinedChernClasses_baseChange i₂ hE₂ q) p
        (exists_iso_single_baseChange i₁ i₂ p q hres) =
      bivariantTransport C (gysinSystemOfInvertible C) (pullback.fst i₂ q ≫ i₂ ≫ sX)
        (pullback.snd i₂ q ≫ q ≫ sX) (q ≫ sX) (pullback.snd i₂ q)
        (pullbackSnd_comp_structureMorphism_eq C (i₂ ≫ sX) sX i₂ rfl q)
        (pullback.snd i₂ q) rfl (Iso.refl _) (Category.id_comp _) (p : ℤ)
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (bivariantRestrictionOfInvertible C (i₂ ≫ sX) sX i₂ rfl q (p : ℤ)
          (localizedChernClassOfClosedCover C sX i₁ i₂ hcover hE₂ p hres))

Stacks.Chow.localizedPowerSumOfClosedCover_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedChernBaseChange.lean, line 490. The attribute's comment: “the classes P'_p: P'_p(E'₂) built from X' = X'₁ ∪ X'₂ and E'₂ is the restriction of P'_p(E₂)”.

Stacks 0GUG, for the classes P_p. In the situation of Stacks 0F9H, with E₂ perfect and E₂|_{X₁ ∩ X₂} zero, let q : X' ⟶ X be locally of finite type, let X' = X'₁ ∪ X'₂ with X'_j = X_j ×_X X', and let E'₂ = (X'₂ ⟶ X₂)^* E₂. Then E'₂ satisfies the hypotheses of Stacks 0F9H for this cover, and the class P'_p(E'₂) ∈ A^p(X'₂ ⟶ X') constructed by Stacks 0F9H from X' = X'₁ ∪ X'₂ and E'₂ is the restriction (Remark 0F9Z) of P'_p(E₂) ∈ A^p(X₂ ⟶ X), read with the structure morphism X'₂ ⟶ X' ⟶ S as in Stacks.Chow.localizedChernClassOfClosedCover_baseChange.

theorem localizedPowerSumOfClosedCover_baseChange
    (perfect : RingedSpace.IsPerfect.{u, u + 1} (X := X₂.toRingedSpace) E₂)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂)) :
    localizedPowerSumOfClosedCover C (q ≫ sX) (pullback.snd i₁ q) (pullback.snd i₂ q)
        (range_pullbackSnd_union_range_pullbackSnd i₁ i₂ hcover q)
        (hasDefinedChernClasses_baseChange i₂ hE₂ q) p (isPerfect_baseChange i₂ q perfect)
        (isZero_baseChange i₁ i₂ q hzero) =
      bivariantTransport C (gysinSystemOfInvertible C) (pullback.fst i₂ q ≫ i₂ ≫ sX)
        (pullback.snd i₂ q ≫ q ≫ sX) (q ≫ sX) (pullback.snd i₂ q)
        (pullbackSnd_comp_structureMorphism_eq C (i₂ ≫ sX) sX i₂ rfl q)
        (pullback.snd i₂ q) rfl (Iso.refl _) (Category.id_comp _) (p : ℤ)
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (bivariantRestrictionOfInvertible C (i₂ ≫ sX) sX i₂ rfl q (p : ℤ)
          (localizedPowerSumOfClosedCover C sX i₁ i₂ hcover hE₂ p perfect hzero))
Tag 0F9I, a lemma

Tag 0F9I in the Stacks Project.

Stacks.Chow.pushforward_localizedPowerSumOfClosedCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/PushforwardLocalizedClass.lean, line 156. The attribute's comment: “the classes P'_p: i_{2,*} ∘ P'_p(E₂) = P_p(E) for E|_{X₁} zero”.

Stacks 0F9I, for the classes P_p. Let X be locally of finite type over S, let i_j : X_j ⟶ X be closed immersions with X = X₁ ∪ X₂ set theoretically, and let E be a perfect object of D(𝒪_X) whose Chern classes are defined and whose restriction E|_{X₁} is zero. Then E₂ = E|_{X₂} satisfies the hypotheses of Stacks 0F9H with E₂|_{X₁ ∩ X₂} zero, and

i_{2,*} ∘ P'_p(E₂) = P_p(E) in A^p(X),

where P'_p(E₂) ∈ A^p(X₂ ⟶ X) is the class of Stacks 0F9H (Stacks.Chow.localizedPowerSumOfClosedCover), i_{2,*} ∘ - is the pushforward of Stacks 0EPK and P_p(E) is the class of Definition 0F9E (2).

theorem pushforward_localizedPowerSumOfClosedCover
    (perfect : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) E)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      i₁.toLRSHom.toShHom).obj E)) :
    canonicalBivariantProperPushforward C (i₂ ≫ sX) sX sX i₂ (𝟙 X) rfl (Category.id_comp sX)
        (p : ℤ)
        (bivariantClassCongr C (gysinSystemOfInvertible C) (i₂ ≫ sX) sX
          (Category.comp_id i₂).symm rfl
          (comp_comp_structureMorphism_eq rfl (Category.id_comp sX)) (p : ℤ)
          (localizedPowerSumOfClosedCover C sX i₁ i₂ hcover
            (hasDefinedChernClasses_derivedPullback i₂ hE) p
            (isPerfect_restriction i₂ perfect)
            (isZero_restriction_intersection i₁ i₂ hzero))) =
      perfectPowerSumComponent C sX hE p

Stacks.Chow.pushforward_localizedChernClassOfClosedCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/PushforwardLocalizedClass.lean, line 192. The attribute's comment: “the classes c'_p: i_{2,*} ∘ c'_p(E₂) = c_p(E) for E|_{X₁} finite locally free of rank < p in degree 0”.

Stacks 0F9I, for the Chern classes. Let X be locally of finite type over S, let i_j : X_j ⟶ X be closed immersions with X = X₁ ∪ X₂ set theoretically, and let E be a perfect object of D(𝒪_X) whose Chern classes are defined and whose restriction E|_{X₁} is isomorphic to a finite locally free 𝒪_{X₁}-module of rank < p sitting in cohomological degree 0. Then E₂ = E|_{X₂} satisfies the hypotheses of Stacks 0F9H with E₂|_{X₁ ∩ X₂} finite locally free of rank < p in degree 0, and

i_{2,*} ∘ c'_p(E₂) = c_p(E) in A^p(X),

where c'_p(E₂) ∈ A^p(X₂ ⟶ X) is the class of Stacks 0F9H (Stacks.Chow.localizedChernClassOfClosedCover), i_{2,*} ∘ - is the pushforward of Stacks 0EPK and c_p(E) is the class of Definition 0F9E (2).

theorem pushforward_localizedChernClassOfClosedCover
    (_perfect : RingedSpace.IsPerfect.{u, u + 1} (X := X.toRingedSpace) E)
    (hres : ∃ M : X₁.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          i₁.toLRSHom.toShHom).obj E ≅ (DerivedCategory.singleFunctor X₁.Modules 0).obj M)) :
    canonicalBivariantProperPushforward C (i₂ ≫ sX) sX sX i₂ (𝟙 X) rfl (Category.id_comp sX)
        (p : ℤ)
        (bivariantClassCongr C (gysinSystemOfInvertible C) (i₂ ≫ sX) sX
          (Category.comp_id i₂).symm rfl
          (comp_comp_structureMorphism_eq rfl (Category.id_comp sX)) (p : ℤ)
          (localizedChernClassOfClosedCover C sX i₁ i₂ hcover
            (hasDefinedChernClasses_derivedPullback i₂ hE) p
            (exists_iso_single_restriction_intersection i₁ i₂ p hres))) =
      perfectChernClass C sX hE p

Stacks.Chow.properPushforwardChowCohomology_closedCoverPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCase.lean, line 268. The attribute's comment: “the case of P'_p: i_{2,*} ∘ P'_p(E₂) = P_p(E) for E₂ = E|_{X₂} and E|_{X₁} zero”.

Let i₁ : X₁ ⟶ X and i₂ : X₂ ⟶ X be closed immersions whose images cover X, and let E ∈ D(𝒪_X) have defined Chern classes and restrict to zero on X₁. Let E₂ = E|_{X₂} be as in Stacks 0F9H: it restricts to zero on X₁ ×_X X₂, and its Chern classes are defined by Stacks.Chow.HasDefinedChernClasses.derivedPullback. Then i_{2,*} ∘ P'_p(E₂) = P_p(E) in A^p(X), with i_{2,*} ∘ - the pushforward of Stacks 0EPK.

theorem properPushforwardChowCohomology_closedCoverPowerSum
    (hcover : Set.range i₁ ∪ Set.range i₂ = Set.univ)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      i₁.toLRSHom.toShHom).obj E))
    (hzero₂ : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (pullback.snd i₁ i₂).toLRSHom.toShHom).obj
        ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          i₂.toLRSHom.toShHom).obj E))) :
    properPushforwardChowCohomology C sX (i₂ ≫ sX) i₂ rfl
        (closedCoverPowerSum C sX i₁ i₂ (i₂ ≫ sX) rfl (hE.derivedPullback i₂) p hcover
          hzero₂) =
      perfectPowerSumComponent C sX hE p

Stacks.Chow.properPushforwardChowCohomology_closedCoverChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCase.lean, line 295. The attribute's comment: “the case of c'_p: i_{2,*} ∘ c'_p(E₂) = c_p(E) for E₂ = E|_{X₂} and E|_{X₁} finite locally free of rank < p in degree 0”.

Let i₁ : X₁ ⟶ X and i₂ : X₂ ⟶ X be closed immersions whose images cover X, and let E ∈ D(𝒪_X) have defined Chern classes and restrict on X₁ to a finite locally free module of rank < p in degree 0. Let E₂ = E|_{X₂} be as in Stacks 0F9H: it restricts on X₁ ×_X X₂ to a finite locally free module of rank < p in degree 0, and its Chern classes are defined by Stacks.Chow.HasDefinedChernClasses.derivedPullback. Then i_{2,*} ∘ c'_p(E₂) = c_p(E) in A^p(X), with i_{2,*} ∘ - the pushforward of Stacks 0EPK.

theorem properPushforwardChowCohomology_closedCoverChernClass
    (hcover : Set.range i₁ ∪ Set.range i₂ = Set.univ)
    (hrank : ∃ M : X₁.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        i₁.toLRSHom.toShHom).obj E ≅ (DerivedCategory.singleFunctor _ 0).obj M))
    (hrank₂ : ∃ M : (pullback i₁ i₂).Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (pullback.snd i₁ i₂).toLRSHom.toShHom).obj
          ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
            i₂.toLRSHom.toShHom).obj E) ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) :
    properPushforwardChowCohomology C sX (i₂ ≫ sX) i₂ rfl
        (closedCoverChernClass C sX i₁ i₂ (i₂ ≫ sX) rfl (hE.derivedPullback i₂) p hcover
          hrank₂) =
      perfectChernClass C sX hE p
Tag 0FAI, a lemma

Tag 0FAI in the Stacks Project.

Stacks.Chow.canonicalBivariantProperPushforward_localizedPowerSumOfClosedCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/ShrinkLocalizedClass.lean, line 202. The attribute's comment: “the classes P'_p: (X₂' ⟶ X₂)_* ∘ P'_p(E₂|_{X₂'}) = P'_p(E₂) for E₂|_{X₁' ∩ X₂} zero”.

Stacks 0FAI, for the classes P_p. In the situation of Stacks 0F9H — closed immersions i_j : X_j ⟶ X with X = X₁ ∪ X₂ set theoretically, and E₂ ∈ D(𝒪_{X₂}) perfect with defined Chern classes and E₂|_{X₁ ∩ X₂} zero — let X₂' ⊂ X₂ and X₁ ⊂ X₁' ⊂ X be closed subschemes with X = X₁' ∪ X₂' set theoretically, and assume E₂|_{X₁' ∩ X₂} is zero. Then

(X₂' ⟶ X₂)_* ∘ P'_p(E₂|_{X₂'}) = P'_p(E₂) in A^p(X₂ ⟶ X),

where P'_p(E₂|_{X₂'}) ∈ A^p(X₂' ⟶ X) is the class of Stacks 0F9H for the cover X = X₁' ∪ X₂' (Stacks.Chow.localizedPowerSumOfClosedCover), P'_p(E₂) the one for X = X₁ ∪ X₂, and (X₂' ⟶ X₂)_* ∘ - the proper pushforward of Stacks 0EPK.

theorem canonicalBivariantProperPushforward_localizedPowerSumOfClosedCover
    (hcover : Set.range i₁.base ∪ Set.range i₂.base = Set.univ)
    (perfect : RingedSpace.IsPerfect.{u, u + 1} (X := X₂.toRingedSpace) E₂)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂))
    (_hX₁ : ∃ ι : X₁ ⟶ X₁', ι ≫ i₁' = i₁)
    (hcover' : Set.range i₁'.base ∪ Set.range (j ≫ i₂).base = Set.univ)
    (hzero' : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (pullback.snd i₁' i₂).toLRSHom.toShHom).obj E₂)) :
    canonicalBivariantProperPushforward C ((j ≫ i₂) ≫ sX) (i₂ ≫ sX) sX j i₂
        (Category.assoc j i₂ sX).symm rfl (p : ℤ)
        (localizedPowerSumOfClosedCover C sX i₁' (j ≫ i₂) hcover'
          (hasDefinedChernClasses_derivedPullback j hE₂) p (isPerfect_shrink j perfect)
          (isZero_shrink i₁' i₂ j hzero')) =
      localizedPowerSumOfClosedCover C sX i₁ i₂ hcover hE₂ p perfect hzero

Stacks.Chow.canonicalBivariantProperPushforward_localizedChernClassOfClosedCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/ShrinkLocalizedClass.lean, line 254. The attribute's comment: “the classes c'_p: (X₂' ⟶ X₂)_* ∘ c'_p(E₂|_{X₂'}) = c'_p(E₂) for E₂|_{X₁' ∩ X₂} finite locally free of rank < p in degree 0”.

Stacks 0FAI, for the Chern classes. In the situation of Stacks 0F9H — closed immersions i_j : X_j ⟶ X with X = X₁ ∪ X₂ set theoretically, and E₂ ∈ D(𝒪_{X₂}) perfect with defined Chern classes and E₂|_{X₁ ∩ X₂} isomorphic to a finite locally free module of rank < p in degree 0 — let X₂' ⊂ X₂ and X₁ ⊂ X₁' ⊂ X be closed subschemes with X = X₁' ∪ X₂' set theoretically, and assume E₂|_{X₁' ∩ X₂} is isomorphic to a finite locally free module of rank < p placed in degree 0. Then

(X₂' ⟶ X₂)_* ∘ c'_p(E₂|_{X₂'}) = c'_p(E₂) in A^p(X₂ ⟶ X),

where c'_p(E₂|_{X₂'}) ∈ A^p(X₂' ⟶ X) is the class of Stacks 0F9H for the cover X = X₁' ∪ X₂' (Stacks.Chow.localizedChernClassOfClosedCover), c'_p(E₂) the one for X = X₁ ∪ X₂, and (X₂' ⟶ X₂)_* ∘ - the proper pushforward of Stacks 0EPK.

theorem canonicalBivariantProperPushforward_localizedChernClassOfClosedCover
    (hcover : Set.range i₁.base ∪ Set.range i₂.base = Set.univ)
    (_perfect : RingedSpace.IsPerfect.{u, u + 1} (X := X₂.toRingedSpace) E₂)
    (hres : ∃ M : (pullback i₁ i₂).Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂ ≅
        (DerivedCategory.singleFunctor (pullback i₁ i₂).Modules 0).obj M))
    (_hX₁ : ∃ ι : X₁ ⟶ X₁', ι ≫ i₁' = i₁)
    (hcover' : Set.range i₁'.base ∪ Set.range (j ≫ i₂).base = Set.univ)
    (hres' : ∃ M : (pullback i₁' i₂).Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          (pullback.snd i₁' i₂).toLRSHom.toShHom).obj E₂ ≅
        (DerivedCategory.singleFunctor (pullback i₁' i₂).Modules 0).obj M)) :
    canonicalBivariantProperPushforward C ((j ≫ i₂) ≫ sX) (i₂ ≫ sX) sX j i₂
        (Category.assoc j i₂ sX).symm rfl (p : ℤ)
        (localizedChernClassOfClosedCover C sX i₁' (j ≫ i₂) hcover'
          (hasDefinedChernClasses_derivedPullback j hE₂) p
          (exists_iso_single_shrink i₁' i₂ j p hres')) =
      localizedChernClassOfClosedCover C sX i₁ i₂ hcover hE₂ p hres
Tag 0FAJ, a lemma

Tag 0FAJ in the Stacks Project.

Stacks.Chow.comp_localizedChernClassOfClosedCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedChernComposite.lean, line 181. The attribute's comment: “the classes c'_p: c ∘ c'_p(E₂) = c'_p(Lf₂^*E₂) ∘ c for every bivariant class c in A^r(Y → X), f : Y → X locally of finite type, the composites read as in Remark 0FA2”.

Stacks 0FAJ, for the classes c'_p. Let X be locally of finite type over S, let i_j : X_j ⟶ X be closed immersions with X = X₁ ∪ X₂ set theoretically, and let E₂ ∈ D(𝒪_{X₂}) be an object whose Chern classes are defined and whose restriction to X₁ ∩ X₂ is isomorphic to a finite locally free module of rank < p in degree 0, so that Stacks 0F9H gives c'_p(E₂) ∈ A^p(X₂ ⟶ X). Let f : Y ⟶ X be locally of finite type and c ∈ A^r(Y ⟶ X). Then

c ∘ c'_p(E₂) = c'_p(Lf₂^*E₂) ∘ c,

where f₂ : X₂ ×_X Y ⟶ X₂ is the base change of f and c'_p(Lf₂^*E₂) ∈ A^p(X₂ ×_X Y ⟶ Y) is the class of Stacks 0F9H for the cover of Y by the base changes X_j ×_X Y and the derived pullback Lf₂^*E₂ (which satisfies the hypotheses of Stacks 0F9H by Stacks.Chow.hasDefinedChernClasses_baseChange and Stacks.Chow.exists_iso_single_baseChange). The left side is res(c) ∘ c'_p(E₂), a class for Y ×_X X₂ ⟶ X of degree r + p; the right side, a class for X₂ ×_X Y ⟶ X of degree p + r, is read on Y ×_X X₂ through the symmetry of the fibre product. Perfectness of E₂, assumed in Stacks 0F9H, is not used for c'_p.

theorem comp_localizedChernClassOfClosedCover
    (hres : ∃ M : (pullback i₁ i₂).Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂ ≅
        (DerivedCategory.singleFunctor (pullback i₁ i₂).Modules 0).obj M))
    (c : BivariantChowClass C (f ≫ sX) sX f rfl r) :
    (c.restrict i₂ rfl).comp (BivariantChowClass.equivBivariantClass.symm
        (localizedChernClassOfClosedCover C sX i₁ i₂ hcover hE₂ p hres)) =
      (((BivariantChowClass.equivBivariantClass.symm
          (localizedChernClassOfClosedCover C (f ≫ sX) (pullback.snd i₁ f) (pullback.snd i₂ f)
            (range_pullbackSnd_union_range_pullbackSnd i₁ i₂ hcover f)
            (hasDefinedChernClasses_baseChange i₂ hE₂ f) p
            (exists_iso_single_baseChange i₁ i₂ p f hres))).comp c).degreeCongr
        (add_comm (p : ℤ) r)).transport
        (comp_comp_structureMorphism_eq (BivariantChowClass.restrict_structure_eq rfl i₂ rfl) rfl)
        (pullbackSymmetry i₂ f) (pullbackSymmetry_hom_comp_snd_comp f i₂)

Stacks.Chow.comp_localizedPowerSumOfClosedCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedChernComposite.lean, line 216. The attribute's comment: “the classes P'_p: c ∘ P'_p(E₂) = P'_p(Lf₂^*E₂) ∘ c for every bivariant class c in A^r(Y → X), f : Y → X locally of finite type, the composites read as in Remark 0FA2”.

Stacks 0FAJ, for the classes P'_p. Let X be locally of finite type over S, let i_j : X_j ⟶ X be closed immersions with X = X₁ ∪ X₂ set theoretically, and let E₂ ∈ D(𝒪_{X₂}) be a perfect object whose Chern classes are defined and whose restriction to X₁ ∩ X₂ is zero, so that Stacks 0F9H gives P'_p(E₂) ∈ A^p(X₂ ⟶ X). Let f : Y ⟶ X be locally of finite type and c ∈ A^r(Y ⟶ X). Then

c ∘ P'_p(E₂) = P'_p(Lf₂^*E₂) ∘ c,

where f₂ : X₂ ×_X Y ⟶ X₂ is the base change of f and P'_p(Lf₂^*E₂) ∈ A^p(X₂ ×_X Y ⟶ Y) is the class of Stacks 0F9H for the cover of Y by the base changes X_j ×_X Y and the derived pullback Lf₂^*E₂, the composites being read as in Stacks.Chow.comp_localizedChernClassOfClosedCover.

theorem comp_localizedPowerSumOfClosedCover
    (perfect : RingedSpace.IsPerfect.{u, u + 1} (X := X₂.toRingedSpace) E₂)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂))
    (c : BivariantChowClass C (f ≫ sX) sX f rfl r) :
    (c.restrict i₂ rfl).comp (BivariantChowClass.equivBivariantClass.symm
        (localizedPowerSumOfClosedCover C sX i₁ i₂ hcover hE₂ p perfect hzero)) =
      (((BivariantChowClass.equivBivariantClass.symm
          (localizedPowerSumOfClosedCover C (f ≫ sX) (pullback.snd i₁ f) (pullback.snd i₂ f)
            (range_pullbackSnd_union_range_pullbackSnd i₁ i₂ hcover f)
            (hasDefinedChernClasses_baseChange i₂ hE₂ f) p (isPerfect_baseChange i₂ f perfect)
            (isZero_baseChange i₁ i₂ f hzero))).comp c).degreeCongr
        (add_comm (p : ℤ) r)).transport
        (comp_comp_structureMorphism_eq (BivariantChowClass.restrict_structure_eq rfl i₂ rfl) rfl)
        (pullbackSymmetry i₂ f) (pullbackSymmetry_hom_comp_snd_comp f i₂)

Stacks.Chow.nonhomogeneousBivariantTransport_compositeOfInvertible_closedCoverPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseCommute.lean, line 674. The attribute's comment: “for P'_p: c ∘ P'_p(E₂) = P'_p(Lf₂^E₂) ∘ c in A^(Y₂ → X), for every c in A^*(Y → X)”.

Let i₁ : X₁ ⟶ X, i₂ : X₂ ⟶ X be closed immersions covering X, let E₂ ∈ D(𝒪_{X₂}) have defined Chern classes and restrict to zero on X₁ ∩ X₂, let f : Y ⟶ X be locally of finite type and let c ∈ A^*(Y ⟶ X). Then

c ∘ P'_p(E₂) = P'_p(Lf₂^*E₂) ∘ c in A^*(Y₂ ⟶ X),

where Y₂ = X₂ ×_X Y, f₂ : Y₂ ⟶ X₂ is the base change of f, P'_p(Lf₂^*E₂) ∈ A^p(Y₂ ⟶ Y) is the class of Stacks 0F9H for the base-changed cover of Y, and c ∘ P'_p(E₂) is the composite of the restriction of c to X₂ with P'_p(E₂), carried from Y ×_X X₂ to Y₂.

theorem nonhomogeneousBivariantTransport_compositeOfInvertible_closedCoverPowerSum
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂))
    (c : nonhomogeneousBivariantGroup C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl) :
    nonhomogeneousBivariantTransport C (gysinSystemOfInvertible C)
        (pullback.fst f i₂ ≫ (f ≫ sX)) (pullback.fst i₂ f ≫ (i₂ ≫ sX)) sX
        (pullback.snd f i₂ ≫ i₂)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C (f ≫ sX) sX f rfl i₂) rfl)
        (pullback.snd i₂ f ≫ f)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C (i₂ ≫ sX) sX i₂ rfl f) rfl)
        (pullbackSymmetry f i₂) (by simp [pullback.condition])
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (nonhomogeneousBivariantCompositeOfInvertible C (pullback.fst f i₂ ≫ (f ≫ sX)) (i₂ ≫ sX)
          sX (pullback.snd f i₂) i₂
          (pullbackSnd_comp_structureMorphism_eq C (f ≫ sX) sX f rfl i₂) rfl
          (nonhomogeneousBivariantRestriction C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl i₂
            (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c)
          (DirectSum.of _ (p : ℤ)
            (closedCoverPowerSum C sX i₁ i₂ (i₂ ≫ sX) rfl hE₂ p hcover hzero))) =
      nonhomogeneousBivariantCompositeOfInvertible C (pullback.fst i₂ f ≫ (i₂ ≫ sX)) (f ≫ sX) sX
        (pullback.snd i₂ f) f
        (pullbackSnd_comp_structureMorphism_eq C (i₂ ≫ sX) sX i₂ rfl f) rfl
        (DirectSum.of _ (p : ℤ)
          (closedCoverPowerSum C (f ≫ sX) (pullback.snd i₁ f) (pullback.snd i₂ f)
            (pullback.fst i₂ f ≫ (i₂ ≫ sX))
            (pullbackSnd_comp_structureMorphism_eq C (i₂ ≫ sX) sX i₂ rfl f)
            (hE₂.derivedPullback (pullback.fst i₂ f)) p
            (range_pullbackSnd_union_eq_univ i₁ i₂ hcover f)
            (isZero_derivedPullback_of_isZero_of_comp_eq
              (pullbackLift_comp_pullbackSnd_eq_pullbackSnd_comp_pullbackFst i₁ i₂ f) hzero)))
        c

Stacks.Chow.nonhomogeneousBivariantTransport_compositeOfInvertible_closedCoverChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseCommute.lean, line 725. The attribute's comment: “for c'_p: c ∘ c'_p(E₂) = c'_p(Lf₂^E₂) ∘ c in A^(Y₂ → X), for every c in A^*(Y → X)”.

Let i₁ : X₁ ⟶ X, i₂ : X₂ ⟶ X be closed immersions covering X, let E₂ ∈ D(𝒪_{X₂}) have defined Chern classes and restrict on X₁ ∩ X₂ to a finite locally free module of rank < p in degree 0, let f : Y ⟶ X be locally of finite type and let c ∈ A^*(Y ⟶ X). Then

c ∘ c'_p(E₂) = c'_p(Lf₂^*E₂) ∘ c in A^*(Y₂ ⟶ X),

where Y₂ = X₂ ×_X Y, f₂ : Y₂ ⟶ X₂ is the base change of f, c'_p(Lf₂^*E₂) ∈ A^p(Y₂ ⟶ Y) is the class of Stacks 0F9H for the base-changed cover of Y, and c ∘ c'_p(E₂) is the composite of the restriction of c to X₂ with c'_p(E₂), carried from Y ×_X X₂ to Y₂.

theorem nonhomogeneousBivariantTransport_compositeOfInvertible_closedCoverChernClass
    (hrank : ∃ M : (pullback i₁ i₂).Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂ ≅
          (DerivedCategory.singleFunctor _ 0).obj M))
    (c : nonhomogeneousBivariantGroup C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl) :
    nonhomogeneousBivariantTransport C (gysinSystemOfInvertible C)
        (pullback.fst f i₂ ≫ (f ≫ sX)) (pullback.fst i₂ f ≫ (i₂ ≫ sX)) sX
        (pullback.snd f i₂ ≫ i₂)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C (f ≫ sX) sX f rfl i₂) rfl)
        (pullback.snd i₂ f ≫ f)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C (i₂ ≫ sX) sX i₂ rfl f) rfl)
        (pullbackSymmetry f i₂) (by simp [pullback.condition])
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (nonhomogeneousBivariantCompositeOfInvertible C (pullback.fst f i₂ ≫ (f ≫ sX)) (i₂ ≫ sX)
          sX (pullback.snd f i₂) i₂
          (pullbackSnd_comp_structureMorphism_eq C (f ≫ sX) sX f rfl i₂) rfl
          (nonhomogeneousBivariantRestriction C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl i₂
            (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c)
          (DirectSum.of _ (p : ℤ)
            (closedCoverChernClass C sX i₁ i₂ (i₂ ≫ sX) rfl hE₂ p hcover hrank))) =
      nonhomogeneousBivariantCompositeOfInvertible C (pullback.fst i₂ f ≫ (i₂ ≫ sX)) (f ≫ sX) sX
        (pullback.snd i₂ f) f
        (pullbackSnd_comp_structureMorphism_eq C (i₂ ≫ sX) sX i₂ rfl f) rfl
        (DirectSum.of _ (p : ℤ)
          (closedCoverChernClass C (f ≫ sX) (pullback.snd i₁ f) (pullback.snd i₂ f)
            (pullback.fst i₂ f ≫ (i₂ ≫ sX))
            (pullbackSnd_comp_structureMorphism_eq C (i₂ ≫ sX) sX i₂ rfl f)
            (hE₂.derivedPullback (pullback.fst i₂ f)) p
            (range_pullbackSnd_union_eq_univ i₁ i₂ hcover f)
            (exists_isFiniteLocallyFreeOfRankLT_derivedPullback_of_comp_eq
              (pullbackLift_comp_pullbackSnd_eq_pullbackSnd_comp_pullbackFst i₁ i₂ f) hrank)))
        c
Tag 0FAK, a lemma

Tag 0FAK in the Stacks Project.

Stacks.Chow.closedCoverPowerSum_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseLemmas.lean, line 124. The attribute's comment: “Newton's recursion P'_{p+1} = ∑_{j<p} (-1)^j c'_{j+1} P'_{p-j} + (-1)^p (p+1) c'_{p+1}, for every p ≥ 0, with the multiplication of 0FA0; it determines every displayed identity and the ones after it (and so on)”.

In the situation of Stacks 0F9H, assume that E₂ restricts to zero on X₁ ∩ X₂, so that c'_p(E₂) is defined for every p ≥ 1. Then the classes P'_p(E₂) ∈ A^p(X₂ ⟶ X) are Newton's polynomials in the classes c'_i(E₂), with the multiplication of Stacks 0FA0 ((c, c') ↦ res(c) ∘ c', Stacks.Chow.supportedMul):

P'_{p+1}(E₂) = ∑_{j < p} (-1)^j c'_{j+1}(E₂) P'_{p-j}(E₂) + (-1)^p (p + 1) c'_{p+1}(E₂)

for every p ≥ 0. This is the recursion defining the universal power-sum polynomials of Stacks 0F9B, so P'_1 = c'_1, P'_2 = c'_1² - 2c'_2, P'_3 = c'_1³ - 3c'_1c'_2 + 3c'_3, and so on. The summand c'_{j+1} P'_{p-j} lies in A^{(j+1)+(p-j)}(X₂ ⟶ X), read in degree p + 1.

theorem closedCoverPowerSum_succ (q : ℕ) :
    closedCoverPowerSum C sX i₁ i₂ sX₂ hi₂ hE₂ (q + 1) hcover hzero =
      ∑ j ∈ (Finset.range q).attach, ((-1 : ℤ) ^ (j : ℕ)) •
          bivariantClassDegreeCongr C _ sX₂ sX i₂ hi₂ (newton_degree_eq (Finset.mem_range.mp j.2))
            (supportedMul C sX₂ sX i₂ hi₂
              (closedCoverChernClassOfIsZero C sX i₁ i₂ sX₂ hi₂ hE₂ hcover hzero ((j : ℕ) + 1)
                (Nat.succ_pos _))
              (closedCoverPowerSum C sX i₁ i₂ sX₂ hi₂ hE₂ (q - j) hcover hzero)) +
        ((-1 : ℤ) ^ q * ((q : ℤ) + 1)) •
          closedCoverChernClassOfIsZero C sX i₁ i₂ sX₂ hi₂ hE₂ hcover hzero (q + 1)
            (Nat.succ_pos _)

Stacks.Chow.closedCoverPowerSum_first_four, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseLemmas.lean, line 167. The attribute's comment: “the four displayed identities, with the multiplication of 0FA0”.

In the situation of Stacks 0F9H, with E₂ restricting to zero on X₁ ∩ X₂,

  • P'_1 = c'_1,
  • P'_2 = c'_1² - 2c'_2,
  • P'_3 = c'_1³ - 3c'_1c'_2 + 3c'_3,
  • P'_4 = c'_1⁴ - 4c'_1²c'_2 + 4c'_1c'_3 + 2c'_2² - 4c'_4

in A^p(X₂ ⟶ X), with the multiplication (c, c') ↦ res(c) ∘ c' of Stacks 0FA0 (Stacks.Chow.supportedMul), products bracketed to the right and read in the degree of the left-hand side. The general case ("and so on") is Stacks.Chow.closedCoverPowerSum_succ.

theorem closedCoverPowerSum_first_four :
    let c := fun i (hi : 0 < i) =>
      closedCoverChernClassOfIsZero C sX i₁ i₂ (i₂ ≫ sX) rfl hE₂ hcover hzero i hi
    let m := fun {a b : ℤ} (x : BivariantClass C (gysinSystemOfInvertible C) (i₂ ≫ sX) sX i₂ rfl a)
      (y : BivariantClass C (gysinSystemOfInvertible C) (i₂ ≫ sX) sX i₂ rfl b) =>
        supportedMul C (i₂ ≫ sX) sX i₂ rfl x y
    let P := fun q => closedCoverPowerSum C sX i₁ i₂ (i₂ ≫ sX) rfl hE₂ q hcover hzero
    let d := fun {a b : ℤ} (h : a = b) =>
      bivariantClassDegreeCongr C (gysinSystemOfInvertible C) (i₂ ≫ sX) sX i₂ rfl h
    P 1 = c 1 (by norm_num) ∧
    P 2 = d (by norm_num) (m (c 1 (by norm_num)) (c 1 (by norm_num))) -
      (2 : ℤ) • c 2 (by norm_num) ∧
    P 3 = d (by norm_num) (m (c 1 (by norm_num)) (d (by norm_num : (1 : ℤ) + 1 = 2)
        (m (c 1 (by norm_num)) (c 1 (by norm_num))))) -
      (3 : ℤ) • d (by norm_num) (m (c 1 (by norm_num)) (c 2 (by norm_num))) +
      (3 : ℤ) • c 3 (by norm_num) ∧
    P 4 = d (by norm_num) (m (c 1 (by norm_num)) (d (by norm_num : (1 : ℤ) + 2 = 3)
        (m (c 1 (by norm_num)) (d (by norm_num : (1 : ℤ) + 1 = 2)
          (m (c 1 (by norm_num)) (c 1 (by norm_num))))))) -
      (4 : ℤ) • d (by norm_num) (m (c 1 (by norm_num)) (d (by norm_num : (1 : ℤ) + 2 = 3)
        (m (c 1 (by norm_num)) (c 2 (by norm_num))))) +
      (4 : ℤ) • d (by norm_num) (m (c 1 (by norm_num)) (c 3 (by norm_num))) +
      (2 : ℤ) • d (by norm_num) (m (c 2 (by norm_num)) (c 2 (by norm_num))) -
      (4 : ℤ) • c 4 (by norm_num)
Tag 0FAL, a lemma

Tag 0FAL in the Stacks Project.

Stacks.Chow.closedCoverTotalChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseWhitney.lean, line 438. The attribute's comment: “the class c^(p)(E) in A^(p)(X₂ → X)”.

The class c^{(p)}(E) ∈ A^{(p)}(X₂ ⟶ X). Let i₁ : X₁ ⟶ X, i₂ : X₂ ⟶ X be closed immersions whose images cover X, and let E ∈ D(𝒪_X) have defined Chern classes, with (E|_{X₂})|_{X₁ ∩ X₂} isomorphic to a finite locally free module of rank < p placed in degree 0. Then

c^{(p)}(E) = 1 + c_1(E) + … + c_{p-1}(E) + c'_p(E|_{X₂}) + c'_{p+1}(E|_{X₂}) + …:

its component in a degree 0 ≤ i < p is c_i(E) ∈ A^i(X), in a negative degree it is 0, and in a degree i ≥ p it is the class c'_i(E|_{X₂}) ∈ A^i(X₂ ⟶ X) of Stacks 0F9H (Stacks.Chow.closedCoverChernClass), which is defined since a rank < p is a rank < i.

def closedCoverTotalChernClass {E : DerivedCategory X.Modules} (hE : HasDefinedChernClasses E)
    (p : ℕ)
    (hrank : ∃ M : (pullback i₁ i₂).Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (pullback.snd i₁ i₂).toLRSHom.toShHom).obj
          ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
            i₂.toLRSHom.toShHom).obj E) ≅ (DerivedCategory.singleFunctor _ 0).obj M)) :
    localizedBivariantGrading C (gysinSystemOfInvertible C) (i₂ ≫ sX) sX i₂ rfl p

Stacks.Chow.closedCoverTotalChernClass_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseWhitney.lean, line 551. The attribute's comment: “CORRECTED: hypothesis (2) is imposed on E|_{X₁}, F|_{X₁} (as written, on X₁ ∩ X₂, it is false: X = ℙ¹ ⊔ pt, E = 𝒪(1)² on ℙ¹ and 0 on pt, F = 0, p = q = 1, where the degree-1 components are c₁(E) ≠ 0 and 0)”.

Let i₁ : X₁ ⟶ X, i₂ : X₂ ⟶ X be closed immersions with X = X₁ ∪ X₂ set-theoretically, and let E, F ∈ D(𝒪_X) have defined Chern classes, with E|_{X₁} and F|_{X₁} isomorphic to finite locally free 𝒪_{X₁}-modules of rank < p and < q placed in degree 0. Then

c^{(p+q)}(E ⊕ F) = c^{(p)}(E) c^{(q)}(F) in A^{(p+q)}(X₂ ⟶ X),

with the multiplication of Stacks 0FA0 (Stacks.Chow.localizedGradingMul). The hypotheses of Stacks 0F9H on E|_{X₂}, F|_{X₂} and (E ⊕ F)|_{X₂}, under which the classes c^{(·)} are defined, follow from these (Stacks.Chow.exists_isFiniteLocallyFreeOfRankLT_derivedPullback_pullbackSnd, Stacks.Chow.exists_isFiniteLocallyFreeOfRankLT_derivedPullback_biprod), and so does the definedness of the Chern classes of E ⊕ F (Stacks.Chow.hasDefinedChernClasses_biprod).

The correction. The source assumes in (2) that the restrictions E|_{X₁ ∩ X₂} and F|_{X₁ ∩ X₂} are finite locally free of rank < p, < q (calling them 𝒪_{X₁}-modules). As written, on X₁ ∩ X₂, the statement is false: let X = X₁ ⊔ X₂ be a disjoint union of X₁ = ℙ¹_k over a field and a point X₂, so that (2) is vacuous; take E = 𝒪(1)^{⊕ 2} on X₁ and 0 on X₂, F = 0 and p = q = 1. In degree 1 < p + q the component of c^{(2)}(E ⊕ F) is c_1(E) ≠ 0, while that of c^{(1)}(E) c^{(1)}(F) is (i_{2,*} c'_1(E|_{X₂})) · 1 + 1 · (i_{2,*} c'_1(0)) = 0. The hypothesis on X₁, to which the phrase "𝒪_{X₁}-modules" points, is the one Stacks 0F9I needs to compare the pushed classes i_{2,*} c'_i(E|_{X₂}) with c_i(E), and with it the statement holds. Perfectness of E, F is not used, only that their Chern classes are defined.

theorem closedCoverTotalChernClass_biprod
    (hrankE : ∃ M : X₁.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        i₁.toLRSHom.toShHom).obj E ≅ (DerivedCategory.singleFunctor _ 0).obj M))
    (hrankF : ∃ M : X₁.Modules, IsFiniteLocallyFreeOfRankLT M q ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        i₁.toLRSHom.toShHom).obj F ≅ (DerivedCategory.singleFunctor _ 0).obj M)) :
    closedCoverTotalChernClass C sX i₁ i₂ hcover (hasDefinedChernClasses_biprod hE hF) (p + q)
        (exists_isFiniteLocallyFreeOfRankLT_derivedPullback_pullbackSnd i₁ i₂
          (exists_isFiniteLocallyFreeOfRankLT_derivedPullback_biprod i₁ hrankE hrankF)) =
      localizedGradingMul C (i₂ ≫ sX) sX i₂ rfl
        (closedCoverTotalChernClass C sX i₁ i₂ hcover hE p
          (exists_isFiniteLocallyFreeOfRankLT_derivedPullback_pullbackSnd i₁ i₂ hrankE))
        (closedCoverTotalChernClass C sX i₁ i₂ hcover hF q
          (exists_isFiniteLocallyFreeOfRankLT_derivedPullback_pullbackSnd i₁ i₂ hrankF))
Tag 0FAM, a lemma

Tag 0FAM in the Stacks Project.

Stacks.Chow.closedCoverPowerSum_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseLemmas.lean, line 320.

Let i₁ : X₁ ⟶ X, i₂ : X₂ ⟶ X be closed immersions with X = X₁ ∪ X₂ set-theoretically, and let E, F ∈ D(𝒪_{X₂}) have defined Chern classes and restrict to zero on X₁ ∩ X₂. Then P'_p(E ⊕ F) = P'_p(E) + P'_p(F) in A^p(X₂ ⟶ X) for every p ≥ 0, with P'_p the classes of Stacks 0F9H. (The Chern classes of E ⊕ F are defined and it restricts to zero on X₁ ∩ X₂, so P'_p(E ⊕ F) is defined; perfectness of E, F is not needed.)

theorem closedCoverPowerSum_biprod {E F : DerivedCategory X₂.Modules}
    (hE : HasDefinedChernClasses E) (hF : HasDefinedChernClasses F)
    (hzE : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E))
    (hzF : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (pullback.snd i₁ i₂).toLRSHom.toShHom).obj F)) (p : ℕ) :
    closedCoverPowerSum C sX i₁ i₂ sX₂ hi₂ (hasDefinedChernClasses_biprod hE hF) p hcover
        (isZero_derivedPullback_biprod (pullback.snd i₁ i₂) hzE hzF) =
      closedCoverPowerSum C sX i₁ i₂ sX₂ hi₂ hE p hcover hzE +
        closedCoverPowerSum C sX i₁ i₂ sX₂ hi₂ hF p hcover hzF
Tag 0FAN, a lemma

Tag 0FAN in the Stacks Project.

Stacks.Chow.closedCoverChernClass_derivedTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseLemmas.lean, line 415.

In the situation of Stacks 0F9H — E₂ ∈ D(𝒪_{X₂}) perfect with defined Chern classes, restricting on X₁ ∩ X₂ to a finite locally free module of rank < p placed in degree 0 — assume that E₂ has constant rank 0, and let ℒ be an invertible 𝒪_X-module. Then the restriction of E₂ to X₁ ∩ X₂ is zero (hzero in the statement, by the assumption on the rank), so c'_i(E₂) and c'_i(E₂ ⊗ ℒ) are defined for every i ≥ 1, and

c'_i(E₂ ⊗ ℒ) = ∑_{j=0}^{i-1} binom(-i + j, j) c'_{i-j}(E₂) c_1(ℒ)^j

in A^i(X₂ ⟶ X). Here E₂ ⊗ ℒ is the twist of E₂ by ℒ|_{X₂} (Stacks 0FAF), c_1(ℒ)^j ∈ A^j(X), and the product A^{i-j}(X₂ ⟶ X) × A^j(X) ⟶ A^i(X₂ ⟶ X) is the first multiplication of Stacks 0FA0 (Stacks.Chow.supportedRightComp), the summand being read in degree i.

theorem closedCoverChernClass_derivedTwist {E₂ : DerivedCategory X₂.Modules}
    (perfect : RingedSpace.IsPerfect.{u, u + 1} E₂) (hE₂ : HasDefinedChernClasses E₂)
    (constantRank : ∀ x : X₂, DerivedFibreBetti.chiDerivedFibre X₂ E₂
      (DerivedFibreBetti.isPseudoCoherent_of_isPerfect E₂ perfect) x = 0) {p : ℕ}
    (hrank : ∃ M : (pullback i₁ i₂).Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (pullback.snd i₁ i₂).toLRSHom.toShHom).obj E₂ ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) (i : ℕ) (hi : 0 < i) :
    haveI := isInvertible_pullback i₂ L
    let hzero := DerivedFibreBetti.isZero_derivedPullback_of_chiDerivedFibre_eq_zero
      (pullback.snd i₁ i₂) E₂ perfect constantRank hrank
    closedCoverChernClassOfIsZero C sX i₁ i₂ (i₂ ≫ sX) rfl
        (hasDefinedChernClasses_derivedTwist hE₂ ((Scheme.Modules.pullback i₂).obj L)) hcover
        (isZero_derivedPullback_derivedTwist (pullback.snd i₁ i₂) _ hzero) i hi =
      ∑ j ∈ (Finset.range i).attach, Ring.choose (-(i : ℤ) + (j : ℕ)) (j : ℕ) •
        bivariantClassDegreeCongr C _ (i₂ ≫ sX) sX i₂ rfl
          (twist_degree_eq (Finset.mem_range.mp j.2))
          (supportedRightComp C (i₂ ≫ sX) sX i₂ rfl
            (closedCoverChernClassOfIsZero C sX i₁ i₂ (i₂ ≫ sX) rfl hE₂ hcover hzero (i - j)
              (by have := Finset.mem_range.mp j.2; omega))
            ((TotalChowClass.firstChernTotal C sX L ^ (j : ℕ)) (j : ℕ)))
Tag 0FE5, a lemma

Tag 0FE5 in the Stacks Project.

Stacks.Chow.closedCoverPowerSum_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseTensor.lean, line 1056. The attribute's comment: “the formula P'_p((E tensor^L E')|_(X_2 cap X'_2)) = sum over p_1 + p_2 = p of C(p, p_1) chi_(p_1) chi'_(p_2) in A^p(X_2 cap X'_2 -> X), for every p >= 0, with E, E' perfect with defined Chern classes as in the source. The closed cover of X on which the left hand side is the class of 0F9H is X = Y cup (X_2 cap X'_2) with Y the reduced closed subscheme on |X_1| cup |X'_1| (reducedUnionIdeal); the vanishing of (E tensor^L E')|_(Y cap X_2 cap X'_2) that 0F9H needs is proved (isZero_derivedPullback_derivedTensor_reducedUnion, by derived Nakayama on the derived fibres), for E, E' perfect as in the source. The source's Y = (X_1 cap X'_1) cup (X_1 cap X'_2) cup (X_2 cap X'_1) has the same underlying set; by 0FAH the class does not depend on the choice. The product of a class on X_2 and a class on X'_2 is supportedIntersectionMul, res(c_1) o c_2 for the restriction of 0F9Z and the composition of 0B75”.

Stacks 0FE5 for P'_p. Let X = X₁ ∪ X₂ = X₁' ∪ X₂' be two closed covers and let E, E' ∈ D(𝒪_X) be perfect objects whose Chern classes are defined and which restrict to zero on X₁ and X₁'. Write χ_p = P'_p(E|_{X₂}) and χ'_p = P'_p(E'|_{X₂'}) for the classes of Stacks 0F9H. Let Y ⊆ X be the reduced closed subscheme with underlying set X₁ ∪ X₁' (Stacks.Chow.reducedUnionIdeal); then X = Y ∪ (X₂ ∩ X₂'), and E ⊗^L E' restricts to zero on Y ∩ (X₂ ∩ X₂'), so the class of Stacks 0F9H of (E ⊗^L E')|_{X₂ ∩ X₂'} along X = Y ∪ (X₂ ∩ X₂') is defined; by Stacks 0FAH it does not depend on the choice of Y. Then

P'_p((E ⊗^L E')|_{X₂ ∩ X₂'}) = ∑_{p₁ + p₂ = p} C(p, p₁) χ_{p₁} χ'_{p₂}

in A^p(X₂ ∩ X₂' ⟶ X), with the product of Stacks.Chow.supportedIntersectionMul, each summand read in degree p.

theorem closedCoverPowerSum_derivedTensor (perfectE : RingedSpace.IsPerfect.{u, u + 1} E)
    (perfectE' : RingedSpace.IsPerfect.{u, u + 1} E') (p : ℕ) :
    closedCoverPowerSum C sX (reducedUnionIdeal i₁ j₁).subschemeι (pullback.snd i₂ j₂ ≫ j₂) _ rfl
        ((hasDefinedChernClasses_derivedTensor hE hE').derivedPullback _) p
        (range_union_range_reducedUnionIdeal i₁ i₂ j₁ j₂ hcover hcover')
        (isZero_derivedPullback_derivedTensor_reducedUnion i₁ i₂ j₁ j₂ hzero hzero' perfectE
          perfectE') =
      ∑ q ∈ (antidiagonal p).attach, (p.choose q.1.1 : ℤ) •
        bivariantClassDegreeCongr C _ _ sX _ rfl
          (by have := mem_antidiagonal.1 q.2; omega)
          (supportedIntersectionMul C sX i₂ j₂ (IsPullback.of_hasPullback i₂ j₂) _ rfl
            (closedCoverPowerSumRestrict C sX i₁ i₂ hcover hE hzero q.1.1)
            (closedCoverPowerSumRestrict C sX j₁ j₂ hcover' hE' hzero' q.1.2))

Stacks.Chow.closedCoverChernClass_derivedTensor_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseTensor.lean, line 1096. The attribute's comment: “the formula c'_1((E tensor^L E')|_(X_2 cap X'_2)) = r gamma'_1 + r' gamma_1 in A^1(X_2 cap X'_2 -> X), with E, E' perfect with defined Chern classes as in the source. The closed cover of X on which the left hand side is the class of 0F9H is X = Y cup (X_2 cap X'_2) with Y the reduced closed subscheme on |X_1| cup |X'_1| (reducedUnionIdeal); the vanishing of (E tensor^L E')|_(Y cap X_2 cap X'_2) that 0F9H needs is proved (isZero_derivedPullback_derivedTensor_reducedUnion, by derived Nakayama on the derived fibres), for E, E' perfect as in the source. The source's Y = (X_1 cap X'_1) cup (X_1 cap X'_2) cup (X_2 cap X'_1) has the same underlying set; by 0FAH the class does not depend on the choice. Products are supportedIntersectionMul, res(c_1) o c_2, landing in the class group of X_2 x_X X'_2 -> X for both orders of the factors”.

Stacks 0FE5 for c'_1. Let X = X₁ ∪ X₂ = X₁' ∪ X₂' be two closed covers and let E, E' ∈ D(𝒪_X) be perfect objects whose Chern classes are defined and which restrict to zero on X₁ and X₁'. Write r = P'_0(E|_{X₂}), r' = P'_0(E'|_{X₂'}), γ_1 = c'_1(E|_{X₂}) and γ'_1 = c'_1(E'|_{X₂'}) for the classes of Stacks 0F9H. Let Y ⊆ X be the reduced closed subscheme with underlying set X₁ ∪ X₁' (Stacks.Chow.reducedUnionIdeal); then X = Y ∪ (X₂ ∩ X₂'), and E ⊗^L E' restricts to zero on Y ∩ (X₂ ∩ X₂'), so the class of Stacks 0F9H of (E ⊗^L E')|_{X₂ ∩ X₂'} along X = Y ∪ (X₂ ∩ X₂') is defined; by Stacks 0FAH it does not depend on the choice of Y. Then

c'_1((E ⊗^L E')|_{X₂ ∩ X₂'}) = r γ'_1 + r' γ_1

in A^1(X₂ ∩ X₂' ⟶ X), with the product of Stacks.Chow.supportedIntersectionMul (for r' γ_1 along the pullback square with the two factors exchanged), each summand read in degree 1.

theorem closedCoverChernClass_derivedTensor_one (perfectE : RingedSpace.IsPerfect.{u, u + 1} E)
    (perfectE' : RingedSpace.IsPerfect.{u, u + 1} E') :
    closedCoverChernClassOfIsZero C sX (reducedUnionIdeal i₁ j₁).subschemeι
        (pullback.snd i₂ j₂ ≫ j₂) _ rfl
        ((hasDefinedChernClasses_derivedTensor hE hE').derivedPullback _)
        (range_union_range_reducedUnionIdeal i₁ i₂ j₁ j₂ hcover hcover')
        (isZero_derivedPullback_derivedTensor_reducedUnion i₁ i₂ j₁ j₂ hzero hzero' perfectE
          perfectE') 1 one_pos =
      bivariantClassDegreeCongr C _ _ sX _ rfl (by norm_num)
          (supportedIntersectionMul C sX i₂ j₂ (IsPullback.of_hasPullback i₂ j₂) _ rfl
            (closedCoverPowerSumRestrict C sX i₁ i₂ hcover hE hzero 0)
            (closedCoverChernClassRestrict C sX j₁ j₂ hcover' hE' hzero' 1 one_pos)) +
        bivariantClassDegreeCongr C _ _ sX _ rfl (by norm_num)
          (supportedIntersectionMul C sX j₂ i₂ (IsPullback.of_hasPullback i₂ j₂).flip _
            pullback.condition
            (closedCoverPowerSumRestrict C sX j₁ j₂ hcover' hE' hzero' 0)
            (closedCoverChernClassRestrict C sX i₁ i₂ hcover hE hzero 1 one_pos))

Stacks.Chow.closedCoverChernClass_derivedTensor_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/BabyCaseTensor.lean, line 1148. The attribute's comment: “the formula for c'_2((E tensor^L E')|_(X_2 cap X'_2)) in A^2(X_2 cap X'_2 -> X), with E, E' perfect with defined Chern classes as in the source. The closed cover of X on which the left hand side is the class of 0F9H is X = Y cup (X_2 cap X'_2) with Y the reduced closed subscheme on |X_1| cup |X'_1| (reducedUnionIdeal); the vanishing of (E tensor^L E')|_(Y cap X_2 cap X'_2) that 0F9H needs is proved (isZero_derivedPullback_derivedTensor_reducedUnion, by derived Nakayama on the derived fibres), for E, E' perfect as in the source. The source's Y = (X_1 cap X'_1) cup (X_1 cap X'_2) cup (X_2 cap X'_1) has the same underlying set; by 0FAH the class does not depend on the choice. C(r, 2) is read as closedCoverRankChoose: the 0F9H extension of the restriction to X_2 of the class ofLocallyConstant of x |-> C(chi_E(x), 2), chi_E the derived-fibre Euler characteristic whose class is r(E) = P_0(E), exactly as 0FAG reads C(r(E), 2); it vanishes on X_1 because chi_E does, and C(r, 1) = r. The term (r r' - 1) gamma'_1 gamma_1 is read as (r r')(gamma'_1 gamma_1) - gamma'_1 gamma_1, since 1 is not a class supported on X_2 cap X'_2; products of classes supported on X_2 and X'_2 are supportedIntersectionMul, products of classes on one support are supportedMul (0FA0). The source's 'and so on for higher Chern classes' is not a precise assertion and is not formalized”.

Stacks 0FE5 for c'_2. Let X = X₁ ∪ X₂ = X₁' ∪ X₂' be two closed covers and let E, E' ∈ D(𝒪_X) be perfect objects whose Chern classes are defined and which restrict to zero on X₁ and X₁'. Write r = P'_0(E|_{X₂}), r' = P'_0(E'|_{X₂'}), γ_p = c'_p(E|_{X₂}) and γ'_p = c'_p(E'|_{X₂'}) for the classes of Stacks 0F9H, and C(r, 2), C(r', 2) for the classes Stacks.Chow.closedCoverRankChoose. Let Y ⊆ X be the reduced closed subscheme with underlying set X₁ ∪ X₁' (Stacks.Chow.reducedUnionIdeal); then X = Y ∪ (X₂ ∩ X₂'), and E ⊗^L E' restricts to zero on Y ∩ (X₂ ∩ X₂'), so the class of Stacks 0F9H of (E ⊗^L E')|_{X₂ ∩ X₂'} along X = Y ∪ (X₂ ∩ X₂') is defined; by Stacks 0FAH it does not depend on the choice of Y. Then

c'\_2((E ⊗^L E')|\_\{X₂ ∩ X₂'}) = r γ'\_2 + r' γ\_2 + C(r, 2) (γ'\_1)² + ((r r') (γ'\_1 γ\_1) - γ'\_1 γ\_1) + C(r', 2) γ\_1²

in A^2(X₂ ∩ X₂' ⟶ X). The products of a class on X₂ and a class on X₂' are those of Stacks.Chow.supportedIntersectionMul, the squares (γ'_1)², γ_1² and the product of r r' with γ'_1 γ_1 are the third multiplication of Stacks 0FA0 (Stacks.Chow.supportedMul), and each summand is read in degree 2.

theorem closedCoverChernClass_derivedTensor_two (perfectE : RingedSpace.IsPerfect.{u, u + 1} E)
    (perfectE' : RingedSpace.IsPerfect.{u, u + 1} E') :
    closedCoverChernClassOfIsZero C sX (reducedUnionIdeal i₁ j₁).subschemeι
        (pullback.snd i₂ j₂ ≫ j₂) _ rfl
        ((hasDefinedChernClasses_derivedTensor hE hE').derivedPullback _)
        (range_union_range_reducedUnionIdeal i₁ i₂ j₁ j₂ hcover hcover')
        (isZero_derivedPullback_derivedTensor_reducedUnion i₁ i₂ j₁ j₂ hzero hzero' perfectE
          perfectE') 2 two_pos =
      (bivariantClassDegreeCongr C _ _ sX _ rfl (by norm_num)
          (supportedIntersectionMul C sX i₂ j₂ (IsPullback.of_hasPullback i₂ j₂) _ rfl
            (closedCoverPowerSumRestrict C sX i₁ i₂ hcover hE hzero 0)
            (closedCoverChernClassRestrict C sX j₁ j₂ hcover' hE' hzero' 2 two_pos)) +
        bivariantClassDegreeCongr C _ _ sX _ rfl (by norm_num)
          (supportedIntersectionMul C sX j₂ i₂ (IsPullback.of_hasPullback i₂ j₂).flip _
            pullback.condition
            (closedCoverPowerSumRestrict C sX j₁ j₂ hcover' hE' hzero' 0)
            (closedCoverChernClassRestrict C sX i₁ i₂ hcover hE hzero 2 two_pos)) +
        bivariantClassDegreeCongr C _ _ sX _ rfl (by norm_num)
          (supportedIntersectionMul C sX i₂ j₂ (IsPullback.of_hasPullback i₂ j₂) _ rfl
            (closedCoverRankChoose C sX i₁ i₂ perfectE hcover hzero 2 two_pos)
            (supportedMul C (j₂ ≫ sX) sX j₂ rfl
              (closedCoverChernClassRestrict C sX j₁ j₂ hcover' hE' hzero' 1 one_pos)
              (closedCoverChernClassRestrict C sX j₁ j₂ hcover' hE' hzero' 1 one_pos))) +
        (bivariantClassDegreeCongr C _ _ sX _ rfl (by norm_num)
            (supportedMul C ((pullback.snd i₂ j₂ ≫ j₂) ≫ sX) sX (pullback.snd i₂ j₂ ≫ j₂) rfl
              (supportedIntersectionMul C sX i₂ j₂ (IsPullback.of_hasPullback i₂ j₂) _ rfl
                (closedCoverPowerSumRestrict C sX i₁ i₂ hcover hE hzero 0)
                (closedCoverPowerSumRestrict C sX j₁ j₂ hcover' hE' hzero' 0))
              (supportedIntersectionMul C sX j₂ i₂ (IsPullback.of_hasPullback i₂ j₂).flip _
                pullback.condition
                (closedCoverChernClassRestrict C sX j₁ j₂ hcover' hE' hzero' 1 one_pos)
                (closedCoverChernClassRestrict C sX i₁ i₂ hcover hE hzero 1 one_pos))) -
          bivariantClassDegreeCongr C _ _ sX _ rfl (by norm_num)
            (supportedIntersectionMul C sX j₂ i₂ (IsPullback.of_hasPullback i₂ j₂).flip _
              pullback.condition
              (closedCoverChernClassRestrict C sX j₁ j₂ hcover' hE' hzero' 1 one_pos)
              (closedCoverChernClassRestrict C sX i₁ i₂ hcover hE hzero 1 one_pos))) +
        bivariantClassDegreeCongr C _ _ sX _ rfl (by norm_num)
          (supportedIntersectionMul C sX j₂ i₂ (IsPullback.of_hasPullback i₂ j₂).flip _
            pullback.condition
            (closedCoverRankChoose C sX j₁ j₂ perfectE' hcover' hzero' 2 two_pos)
            (supportedMul C (i₂ ≫ sX) sX i₂ rfl
              (closedCoverChernClassRestrict C sX i₁ i₂ hcover hE hzero 1 one_pos)
              (closedCoverChernClassRestrict C sX i₁ i₂ hcover hE hzero 1 one_pos))))
Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.