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, letXbe locally of finite type overS, letℰbe a finite locally free𝒪_X-module of constant rankr, letf : X' ⟶ Xbe locally of finite type and lets ∈ Γ(X', f^*ℰ). Assumedim_δ(X') = n, thatdim_δ(Z(s)) ≤ n - r, and that for every generic pointξ ∈ Z(s)withδ(ξ) = n - rthe ideal ofZ(s)in𝒪_{X', ξ}is generated by a regular sequence of lengthr. Then
c_r(ℰ) ∩ [X']_n = [Z(s)]_{n - r}inCH_{n - r}(X'),where
c_r(ℰ)is read as a bivariant classcfor𝟙 Xsatisfying the characterizationStacks.Chow.IsChernClassBivariantof Stacks 0B7H, and its cap product against the Chow group ofX'is transported fromX ×_X X'toX'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 thatc_r(ℰ)is a bivariant class. The reduced caseStacks.Chow.TopChernCapEqZeroSchemeis the hypothesishreduced; the source proves it by induction onrfrom 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 hypothesishreducedof the two theorems above, at a moduleFof rank one onX', discharged from Stacks 02SQ.Stacks 02SQ is stated for a closed immersion
i : Y ⟶ Xwith the invertible module on the ambient schemeXand the section taken inΓ(Y, i^*L), so using it ati = 𝟙 X'means transporting the section acrossAlgebraicGeometry.Scheme.Modules.pullbackId:tis the section of(𝟙 X')^*Fcorresponding tosunder that isomorphism, andhtsays so. The zero schemes ofsand oftthen agree byAlgebraicGeometry.zeroScheme_eq_of_iso, andZ(s)of this file is the zero scheme of Stacks 02OQ byStacks.Chow.zeroSchemeOfSection_eq_zeroScheme.
hsis the third hypothesis of Stacks 02SQ, injectivity of multiplication byton the stalk at the generic point of every component ofZ(t)ofδ-dimensionk. The source derives it from the regular-sequence hypothesisStacks.Chow.IsRegularZeroSchemeSequence, which atr = 1says that the ideal ofZ(s)in that local ring is generated by a single nonzerodivisor; that derivation is not carried out here, sohsis assumed andhregis 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
Eof rank one, with its hypothesishreduceddischarged byStacks.Chow.topChernCapEqZeroScheme_rank_one. So this is a genuine instance of the tag: the only inputs left are the characterization ofc₁(E)as a bivariant class (Stacks 0B7H), the three dimension and regularity hypotheses of the tag, and the three assumptions described atStacks.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, letXbe locally of finite type overS, letℰbe a finite locally free𝒪_X-module, letf : X' ⟶ Xbe locally of finite type such thatf^*ℰhas constant rankr, and lets ∈ Γ(X', f^*ℰ). Assumedim_δ(X') ≤ n, thatdim_δ(Z(s)) ≤ n - r, and that for every generic pointξ ∈ Z(s)withδ(ξ) = n - rthe ideal ofZ(s)in𝒪_{X', ξ}is generated by a regular sequence of lengthr. Then
c_r(ℰ) ∩ [X']_n = [Z(s)]_{n - r}inCH_{n - r}(X'),where
c_r(ℰ) ∈ A^r(X)is the degree-rcomponent of the total Chern classStacks.Chow.totalChernOfFiniteLocallyFreeandc_r(ℰ) ∩ -is its cap operation on the test schemef.
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 onX,f : X' ⟶ Xlocally of finite type andsa section off^*ℰwith zero schemeZ(s). Ifdim_δ(X') = n,f^*ℰhas constant rankr,dim_δ(Z(s)) ≤ n - rand at every generic pointξofZ(s)withδ(ξ) = n - rthe ideal ofZ(s)in𝒪_{X', ξ}is generated by a regular sequence of lengthr, thenc_r(ℰ) ∩ [X']_n = [Z(s)]_{n - r}inCH_{n - r}(X'), wherec_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_iinto open and closed pieces on whichℱhas constant rank, the piecewise flat pullbackStacks.Chow.dualBundleFlatPullbackis the canonical flat pullbackp^*.
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 rankr,p^*is the flat pullback of relative dimensionr. The degreedpart ofp^*βisp^*(β_{d-r})for the flat pullbackp^* : A_{d-r}(X) ⟶ A_d(𝐕(ℱ^∨))of Stacks 02S1 along the projection, which is flat of relative dimensionr.
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 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0be a short exact sequence of finite locally free𝒪_X-modules, leti : N' = Spec_X(Sym((𝒩')^∨)) ⟶ N = Spec_X(Sym(𝒩^∨))be the closed embedding andp' : N' ⟶ X,p : N ⟶ Xthe projections. Forα ∈ A_k(X),
i_*(p')^*α = p^*(c_top(ℰ) ∩ α)in∏_d A_d(N).The ranks are only locally constant, so
pandp'have locally constant relative dimension and both sides live in∏_d A_d(N). Here(p')^*andp^*are the flat pullbacksStacks.Chow.canonicalDualBundleFlatPullback: the unique families whose restriction over every open of constant rankris the flat pullback of relative dimensionrof Stacks 02S1 (Stacks.Chow.isDualBundleFlatPullback_iff), equal to that flat pullback when the rank is constant (Stacks.Chow.canonicalDualBundleFlatPullback_eq_dualBundlePullback). The classc_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 degreek.
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 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0of finite locally free𝒪_X-modules, of arbitrary ranks, the morphismi : 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 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0of finite locally free𝒪_X-modules, the canonical morphismi : 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 hypothesishci.
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, letXbe locally of finite type overSand let0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0be a short exact sequence of finite locally free𝒪_X-modules, of constant ranksr',rande. Leti : N' = Spec_X(Sym((𝒩')^∨)) ⟶ N = Spec_X(Sym(𝒩^∨))be the canonical closed embedding andp' : N' ⟶ X,p : N ⟶ Xthe structure morphisms. Then forα ∈ CH_k(X)
i_*(p')^*α = p^*(c_top(ℰ) ∩ α)in
CH_{k+r'}(N), the two degreesk + r'and(k - e) + ragreeing becauser = r' + e.All of
i,p,p'are the canonical constructed morphisms:pandp'areStacks.Chow.dualVectorBundleToBase, i.e.AlgebraicGeometry.Scheme.Modules.vectorBundleToBaseof the dual sheaves, andiisStacks.Chow.subbundleEmbedding, i.e.AlgebraicGeometry.Scheme.Modules.vectorBundleMapof the dual of the inclusion. The short exact sequence is consumed twice: it makesia closed immersion, throughStacks.Chow.epi_dualMap_of_subbundleShortExact, and it gives the degree identityStacks.Chow.subbundleDegree_eqwithout which the equality is not even a well-formed statement.The two named hypotheses are the source's own two steps:
hstepis the equality Tag 0FA9 gives onNfor the canonical section ofp^*ℰ, andhflatis 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, letXbe locally of finite type overSand let0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0be a short exact sequence of finite locally free𝒪_X-modules. Leti : N' = Spec_X(Sym((𝒩')^∨)) ⟶ N = Spec_X(Sym(𝒩^∨))be the canonical closed embedding andp' : N' ⟶ X,p : N ⟶ Xthe 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 openU ⊆ Xon which𝒩'has rankr'andℰhas ranke, the projections restrict to flat morphismsp'⁻¹(U) ⟶ Xandp⁻¹(U) ⟶ Xof relative dimensionsr'andr' + e,irestricts to the closed embeddingp'⁻¹(U) ⟶ p⁻¹(U),c_top(ℰ)acts by its degree-epart (Stacks.Chow.topChernCap), and the identity holds inCH_{k+r'}(p⁻¹(U)) = CH_{(k-e)+(r'+e)}(p⁻¹(U)). Taking forUthe pieces of the decomposition ofXby the ranks of𝒩'andℰ, this is the identity of the tag inCH_*(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 < pthe classch_p(E)caps every rational Chow class of a test scheme of dimension at mostdto 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 inA^*(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 characterch(ℰ) = (ch_0(ℰ), ch_1(ℰ), …) ∈ ∏_{p ≥ 0} (A^p(X) ⊗ 𝐐)(Stacks.Chow.moduleChernCharacter) has componentsch_p(ℰ) = P_p(ℰ)/p!, whereP_p(ℰ) ∈ A^p(X)is the power sum of Stacks 0F9B (withP_0 = r) evaluated at the rankr(ℰ)and the Chern classesc_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
Xis quasi-compact anddim X < ∞, thench(ℰ) ∈ 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:
Stacks.Chow.moduleChernCharacter, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/ChernCharacterLocallyFree.lean, line 409 (StacksFrontier): “the full Chern character ch(E) ∈ ∏_{p ≥ 0} (A^p(X) ⊗ Q) of a finite locally free module of not necessarily constant rank, built from the genuine classes of 0B7H on the rank loci”.
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, letXbe locally of finite type overSand let0 ⟶ ℰ₁ ⟶ ℰ ⟶ ℰ₂ ⟶ 0be a short exact sequence of finite locally free𝒪_X-modules. Then for everyp
P_p(ℰ) = P_p(ℰ₁) + P_p(ℰ₂)inA^p(X),where
P_pis 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, letXbe locally of finite type overSand let0 ⟶ ℰ₁ ⟶ ℰ ⟶ ℰ₂ ⟶ 0be 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 ofXin 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 ⟶ ℰ₁ ⟶ ℰ ⟶ ℰ₂ ⟶ 0of finite locally free𝒪_X-modules, of ranks that need not be constant,P_p(ℰ) = P_p(ℰ₁) + P_p(ℰ₂)for everyp.
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 → ℰ₁ → ℰ → ℰ₂ → 0be a short exact sequence of finite locally free𝒪_X-modules,ℰ₁of rankrwith a filtration whose successive quotients are the invertible modulesℒ_i = L i,ℰ₂of rankswith quotients𝒩_j = N j, andℰof rankr + swith the filtration obtained by juxtaposing them, whose quotientsℳ_kare theℒ_ifollowed by the𝒩_j. Then for everyn-cycleαand everyp ≥ 0
P_p(ℰ) ∩ α = P_p(ℰ₁) ∩ α + P_p(ℰ₂) ∩ αin
A_{n-p}(X), which is the identityP_p(ℰ) = P_p(ℰ₁) + P_p(ℰ₂)of the source read againstα, andch(ℰ) = ch(ℰ₁) + ch(ℰ₂)after dividing byp!. In degree one it isc₁(ℰ) ∩ α = c₁(ℰ₁) ∩ α + c₁(ℰ₂) ∩ α, which isStacks.Chow.chernClassCapExt_one_append; in degree zero it isr + 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₂ sandℰ = Q (r + s)the tops of the three filtrations, for everyn-cycleα
c₁(ℰ) ∩ α = c₁(ℰ₁) ∩ α + c₁(ℰ₂) ∩ αin
A_{n-1}(X). This is the degree-one case of Stacks 0F9C,P_1beingc_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 thenStacks.Chow.powerSumCap_appendin 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, letXbe locally of finite type overSand 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-pcoefficient isch_p = P_p/p!; multiplying two such series convolves their coefficients, so this single identity isStacks.Chow.chernCharacterComponentArbitraryRank_tensorObjin every degree at once, and that in turn isStacks.Chow.modulePowerSumArbitraryRank_tensorObjdivided byp!.
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, letXbe locally of finite type overSand letℰ₁andℰ₂be finite locally free𝒪_X-modules, of no assumed rank. Then for everyp ≥ 0
P_p(ℰ₁ ⊗_{𝒪_X} ℰ₂) = ∑_{p₁ + p₂ = p} C(p, p₁) P_{p₁}(ℰ₁) P_{p₂}(ℰ₂)in
∏_{q ≥ 0} A^q(X), the bivariant ring ofX, whose multiplication is the composition of bivariant classes of Stacks 0B75. In degree zero the identity readsrk(ℰ₁ ⊗ ℰ₂) = rk(ℰ₁) rk(ℰ₂)and in degree onec₁(ℰ₁ ⊗ ℰ₂) = rk(ℰ₂) c₁(ℰ₁) + rk(ℰ₁) c₁(ℰ₂), both as locally constant functions onX.
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 groupA^p(X)of Stacks 0B7E: the classP_p(ℰ₁ ⊗ ℰ₂)is the sum overp₁ + p₂ = pof the classesC(p, p₁) P_{p₁}(ℰ₁) P_{p₂}(ℰ₂)ofA^p(X), each formed by the composition of bivariant classes of Stacks 0B75 inside the bivariant ring and read in degreep. This isStacks.Chow.modulePowerSumArbitraryRank_tensorObjin degreep, 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 everyp ≥ 0. Along a morphism over which both modules have constant rank this isStacks.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
mboth 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 degreep + q, and the identity isStacks.Chow.powerSumOfFiniteLocallyFree_sheafTensordivided bym!.
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 rankrwith a filtration whose successive quotients are the invertible modulesℒ_i = L i, letℰ₂be finite locally free of rankswith quotients𝒩_j = N j, and let the filtration ofℰ₁ ⊗_{𝒪_X} ℰ₂be the lexicographic one of the source, of lengthr·s, whose(i·s+j)-th quotient isℒ_i ⊗ 𝒩_j. Then for everyn-cycleαand everyp ≥ 0
P_p(ℰ₁ ⊗ ℰ₂) ∩ α = ∑_{p₁ + p₂ = p} C(p, p₁) · (P_{p₁}(ℰ₁) ∘ P_{p₂}(ℰ₂)) ∩ αin
A_{n-p}(X), which is the identityP_p(ℰ₁ ⊗ ℰ₂) = ∑_{p₁+p₂=p} C(p,p₁) P_{p₁}(ℰ₁) P_{p₂}(ℰ₂)of the source read againstα, andch(ℰ₁ ⊗ ℰ₂) = ch(ℰ₁) · ch(ℰ₂)after dividing byp!, the binomial coefficients being whatp! = p₁! · p₂! · C(p, p₁)absorbs. Each productP_{p₁}(ℰ₁) · P_{p₂}(ℰ₂)is a composite of operations on Chow groups, asc₁(ℱ)²is in Stacks 0FA6. In degree one,P_0being the rank, the identity iss·(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, letXbe locally of finite type overSand letℰbe a finite locally free𝒪_X-module with dualℰ^∨. Then
ch_i(ℰ^∨) = (-1)^i ch_i(ℰ)inA^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 degreesa, …, a + k, as an element of the group of series with constant term1inside∏_{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 degreesa, …, 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_pof a complex is the alternating sum of the classesP_pof 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_pof a complex of finite locally free modules depends only on the cohomology modules of the complex. Two complexes representing the same object ofD(𝒪_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-
pcomponentch_p(ℰ^•) = P_p(ℰ^•)/p! ∈ A^p(X) ⊗ 𝐐of the Chern character of a complex of finite locally free modules bounded in the degreesa, …, 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 term1inside∏_{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 isc(P|_{Y_ρ}) = ∏_n c(P^n|_{Y_ρ})^{(-1)^n}; these classes are assembled into a total class onYby 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-pcomponent ofStacks.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
Ybe locally of finite type over the base of chapter 42 and letP,P'be locally bounded complexes of finite locally free𝒪_Y-modules representing the same object ofD(𝒪_Y). Then their total Chern classesc(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
Tlocally of finite type overY(Stacks.Chow.TotalChowClass.eq_of_op_fundamentalChowClass_eq). OverTthe 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 ofD(𝒪_Y). ThenP_p(P) = P_p(P') ∈ A^p(Y)for everyp.
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 complexesP,P'of finite locally free modules representing the same object ofD(𝒪_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
Ebe an object ofD(𝒪_X)and letHbe an envelope presentation of it, Stacks 0F9E (1), whose source is quasi-compact. Two familiesc, dof Chow cohomology classes ofXwhose restrictions along the envelope ofHare the coefficients of the total Chern classc(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
Hrather than at every presentation ofE, 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
Ebe an object ofD(𝒪_X)and letHbe an envelope presentation of it, Stacks 0F9E (1), whose source is quasi-compact. Two familiesc, dof Chow cohomology classes ofXwhose restrictions along the envelope ofHare the classesP_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
Hrather than at every presentation ofE, 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
Ebe an object ofD(𝒪_X)and letHbe an envelope presentation of it, Stacks 0F9E (1), whose source is quasi-compact. Two familiesc, dof rational Chow cohomology classes ofXwhose restrictions along the envelope ofHare the componentsch_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
Hrather than at every presentation ofE, 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
Ebe a perfect object ofD(𝒪_X)whose Chern classes are defined. For everypthere is a unique classP_p(E) ∈ A^p(X)whose restriction along the envelopef : Y ⟶ Xof every presentation(f, 𝓔^•)ofEis the classP_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 isStacks.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
Ebe a perfect object ofD(𝒪_X)whose Chern classes are defined. For everypthere is a unique classch_p(E) ∈ A^p(X) ⊗ 𝐐whose rational restriction along the envelopef : Y ⟶ Xof every presentation(f, 𝓔^•)ofEis the componentch_p(𝓔^•) = P_p(𝓔^•)/p!of the Chern character of𝓔^•(Lemma 0ESZ). The class isStacks.Chow.perfectChernCharacterComponent, and the family(ch_p(E))_pisch(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:
Stacks.Chow.existsUnique_forall_res_eq_complexChern, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Chow/ChernClassDerived/PerfectPowerSum.lean, line 359 (StacksFrontier): “c(E): the unique class of the product of the A^p(X), p ≥ 0, restricting along the envelope of every presentation (f, E^bullet) of E to c(E^bullet), independent of f and E^bullet”.
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
EofD(𝒪_X)are defined when some envelopef : Y ⟶ XhasLf^*Eisomorphic 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-pcomponent ofStacks.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 ofXwhose restriction along the envelope of a presentation ofEis the total Chern class of the presenting complex. Its degree-pcomponent isc_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 ⟶ XhasLf^*Eisomorphic to a locally bounded complex of finite locally free𝒪_Y-modules, then the Chern classes ofEare 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
Eis represented by a bounded complex of finite locally free𝒪_X-modules, then the Chern classes ofEare defined: the identity ofXis an envelope andL(𝟙 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
Eis isomorphic to the derived pullback of an objectE'whose Chern classes are defined, then the Chern classes ofEare defined: the base change of an envelope ofE'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.reflthis is the well-definedness that clause (2) of Stacks 0FAC presupposes when it writesc_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, letXbe locally of finite type overSwith quasi-compact irreducible components, and letEbe a perfect object ofD(𝒪_X). Then the Chern classes ofEare defined: there is an envelopef : Y ⟶ Xsuch thatLf^*Eis isomorphic inD(𝒪_Y)to a locally bounded complex of finite locally free𝒪_Y-modules.
Xis locally Noetherian, the base being locally Noetherian andXlocally of finite type over it, soStacks.Chow.exists_isEnvelope_sigma_of_isCompact_irreducibleComponentssupplies an envelope∐ W ⟶ Xwhose summands are Noetherian — hence quasi-compact and quasi-separated — with the resolution property and affine diagonal. ThenStacks.Chow.exists_isLocallyBoundedFiniteLocallyFree_iso_derivedPullback_sigmarepresentsLf^*E, which is clause (1) of the source.Every hypothesis is a hypothesis of the source: the Chow situation,
Xlocally of finite type over its base,Eperfect, and quasi-compactness of the irreducible components ofX. 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, letXbe locally of finite type overSand quasi-compact, and letEbe a perfect object ofD(𝒪_X). Then the Chern classes ofEare defined: there is an envelopef : Y ⟶ Xsuch thatLf^*Eis isomorphic inD(𝒪_Y)to a locally bounded complex of finite locally free𝒪_Y-modules.
Xis Noetherian, the base being locally Noetherian, hence quasi-separated, so [Stacks, Tag 0GTU] gives an envelopef : Y ⟶ XwithYcarrying an ample family of invertible modules;Yis Noetherian becausefis proper, has the resolution property byStacks.Chow.hasResolutionProperty_of_isAmpleFamily_of_isNoetherian, and therefore has affine diagonal by the Noetherian case of [Stacks, Tag 0F8C]. ThenStacks.Chow.hasDefinedChernClasses_of_resolutionProperty_envelopeapplies.Every hypothesis is a hypothesis of the source: the Chow situation,
Xlocally of finite type over its base, perfectness ofE, and quasi-compactness ofX. 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
Ebe an object ofD(𝒪_X)and letHbe an envelope presentation of it, Stacks 0F9E (1), with presenting complexℰ_Y^• = H.Pvanishing outside the degreesw, …, w + k. Leta : W' ⟶ Ybe the lift to the envelope of a modification of a morphismg : W ⟶ X, as produced byAlgebraicGeometry.IsEnvelope.exists_properBirational_modification, so that the morphismg' : W' ⟶ Xof the source isa ≫ H.f.If a family
cof Chow cohomology classes ofXrestricts along the envelope to the power sums of the presenting complex — which is this repository's expression forcbeing the family of power sum classesP_p(E)ofE, and is the hypothesis ofStacks.Chow.eq_of_restriction_eq_powerSumClassComplexLocallyBounded— then its restriction alongg' = a ≫ H.fis the power sum class of the pulled back complexa^*ℰ_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 forc_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 familycof rational Chow cohomology classes ofXrestricting along the envelope of a presentation to the componentsch_p(ℰ_Y^•) = P_p(ℰ_Y^•)/p!, the restriction ofc palongg' = a ≫ H.fisch_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
Xbe locally of finite type over the base and letEbe an object ofD(𝒪_X)whose Chern classes are defined. Forg : W ⟶ Xlocally of finite type withWintegral there are an integral schemeW'and a proper birational morphismb : W' ⟶ Wsuch that, forg' = b ≫ g, the derived pullbackL(g')^*Eis represented by a bounded complexℰ^•of finite locally free𝒪_{W'}-modules of constant ranksρ, and
res_{g'}(c_p(E)) = c_p(ℰ^•)inA^p(W')for everyp,where
c_p(E)is the degree-pcomponent of the total Chern classc(E)of Stacks 0F9E (2) andc_p(ℰ^•)that of∏_n c(ℰ^n)^{(-1)^n}.Perfectness of
Eis not used: the Chern classes being defined is the only hypothesis onEthe 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 ⟶ Xbe an envelope and letg : W ⟶ Xbe a morphism withWintegral. Then there are an integral schemeW', a proper birational morphismb : W' ⟶ Wand a morphisma : W' ⟶ Ywithb ≫ 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
Xbe locally of finite type over the base, letE ∈ D(𝒪_X)be perfect with Chern classes defined, letg : X' ⟶ Xbe locally of finite type and letc ∈ A^*(X' ⟶ X). Then for everyp
c ∘ c_p(E) = c_p(Lg^*E) ∘ cinA^*(X' ⟶ X),the composites being those of Stacks 0B75, extended additively to the graded groups; they are classes for the morphisms
g ≫ 𝟙 Xand𝟙 X' ≫ g, both read as classes forg.
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. Thenc_p(E)is in the center ofA^*(X): for everyc ∈ 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 isStacks.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, letg : X' ⟶ Xbe locally of finite type and letc ∈ A^q(X' ⟶ X)be a bivariant class. Then
c ∘ c_p(E) = c_p(Lg^*E) ∘ cinA^{q+p}(X' ⟶ X),with
c_p(E) ∈ A^p(X)andc_p(Lg^*E) ∈ A^p(X'). The left side is a class forg ≫ 𝟙 Xof degreeq + p; the right side, a class for𝟙 X' ≫ gof degreep + q, is read as one forg ≫ 𝟙 Xof degreeq + palong the identity ofX'.
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. Thenc_p(E) ∈ A^p(X)lies in the center of the Chow cohomology ringA^*(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 ofD(𝒪_X)satisfying one of the conditions of Stacks 0F9F. Then the Chern classes ofE₁,E₂andE₃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 degreep.
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 everyp.
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
Tbe a distinguished triangle ofD(𝒪_X). If there is an envelopef : Y ⟶ Xsuch thatLf^*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 ofE₁,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 representingLf^*E₃, softogether with𝓔₁^•,𝓔₂^•andC(α)^•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 ofD(𝒪_X)is itself represented by a mapα : 𝓔₁^• ⟶ 𝓔₂^•of locally bounded complexes of finite locally free𝒪_X-modules, then the Chern classes ofE₁,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αwithT.mor₁transports along the naturality ofL(𝟙 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
Tbe a distinguished triangle ofD(𝒪_X)whose first two objects are perfect and let the irreducible components ofX, which is locally of finite type over the base of the Chow situation, be quasi-compact. Then the Chern classes ofE₁,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₃).
Xis locally Noetherian, the base being locally Noetherian andXlocally of finite type over it, soStacks.Chow.exists_isEnvelope_sigma_of_isCompact_irreducibleComponentssupplies an envelope∐ W ⟶ Xwhose summands are Noetherian — hence quasi-compact and quasi-separated — with the resolution property and affine diagonal. On such a sourceStacks.Chow.exists_boundedFiniteLocallyFree_sigma_of_isPerfectpresentsLf^*E₁andLf^*E₂by complexes whose summandwise restrictions are bounded complexes of finite locally free modules, andStacks.Chow.exists_isLocallyBoundedFiniteLocallyFree_square_sigmarepresentsLf^*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 shapeStacks.Chow.hasDefinedChernClasses_and_additive_of_envelopeasks for.Every hypothesis is a hypothesis of the source: the Chow situation,
Xlocally of finite type over its base, the distinguished triangle, perfectness ofE₁andE₂, and quasi-compactness of the irreducible components ofX. Local Noetherianity, the envelope, the summands' resolution property and affine diagonal, the two complexes and the map between them are all derived. Perfectness ofE₃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
Tbe a distinguished triangle ofD(𝒪_X)whose first two objects are perfect and letX, which is locally of finite type over the base of the Chow situation, be quasi-compact. Then the Chern classes ofE₁,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₃).
Xis Noetherian, the base being locally Noetherian, hence quasi-separated, so [Stacks, Tag 0GTU] gives an envelopef : Y ⟶ XwithYcarrying an ample family of invertible modules;Yis Noetherian becausefis proper, has the resolution property byStacks.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 shapeStacks.Chow.triangleChernAdditive_of_resolutionProperty_envelopeasks for.Every hypothesis is a hypothesis of the source: the Chow situation,
Xlocally of finite type over its base, the distinguished triangle, perfectness ofE₁andE₂, and quasi-compactness ofX. Quasi-separatedness, Noetherianity, the envelope, the ample family, the resolution property and the affine diagonal are all derived. Perfectness ofE₃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 ≥ 1the classP_p(E)is the universal power-sum polynomialP_pof Stacks 0F9B evaluated at the Chern classes ofE— the same expression in the Chern classes as for a finite locally free module. The polynomial is evaluated in the commutative subring ofA^*(X)generated by the Chern classes ofE.
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 ofE.
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-
ppart oflog c(E)(the terms withk > pvanish in degreep:Stacks.Chow.pow_perfectChernClass_sub_one_apply_of_lt). Solog 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
Xthere are perfect objectsEandFwhose Chern classes are defined, withc(E) = c(F)butP_0(E) = r(E) ≠ r(F) = P_0(F). NamelyE = 𝒪_X[0]andF = 0[0]: both have total Chern class1, and their ranks are1and0.
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
Xmay be proved after restricting along the envelopef : Y ⟶ Xof a presentation ofE: two classes of degreeponXwhose restrictions toA^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
Eare defined, then two Chow cohomology classes of degreeponXwhose restrictions agree along the envelope of every presentation ofEare 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, δ),XandEbe as in Definition 0F9E, the Chern classes ofEbeing defined, and choose an envelopef : Y ⟶ Xand a locally bounded complexℰ^•of finite locally free𝒪_Y-modules representingLf^*E. Then there is a split chartπ_y : P_y ⟶ V_yat every pointy ∈ Y: over the connected componentV_yofy, whereℰ^•is a bounded complex of finite locally free modules of fixed ranks,π_yis the splitting morphism of Stacks 02UL, along which eachℰ^nacquires a filtration with invertible successive quotientsℒ_{n,j}. For such a choice of charts:
- a relation between total Chow cohomology classes on
X— in particular between the classesc_p(E)andP_p(E)— may be checked after restriction to all the charts: restrictionA^*(X) ⟶ ∏_y A^*(P_y)is injective;- with
x_{n,j} = c_1(ℒ_{n,j}), on each chartc(E) = ∏_{n even} ∏_j (1 + x_{n,j}) · (∏_{n odd} ∏_j (1 + x_{n,j}))^{-1}, the factor1 + x_{n,j} = c(ℒ_{n,j})being a unit;- with
x_{n,j} = c_1(ℒ_{n,j}), on each chartP_p(E) = ∑_{n even} ∑_j x_{n,j}^p - ∑_{n odd} ∑_j x_{n,j}^pfor everyp ≥ 0.Here
c(E)andP_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 ofE.This is what makes the assertion of [Stacks, Tag 0FAE] well-typed, the classes
c_p,P_pandch_pof [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)inA^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)inA^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)inA^p(X) ⊗ 𝐐, the third conclusion of [Stacks, Tag 0FAE]. The Chern character component isP_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
Xbe locally of finite type over the base of chapter 42, letEbe a perfect object ofD(𝒪_X)whose Chern classes are defined and which has constant rankr, 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(ℒ)^jin
A^i(X), wherec_{i-j}(E)is the component of degreei - jof 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,FofD(𝒪_X)whose Chern classes are defined,
c₁(E ⊗^L F) = r(E) c₁(F) + r(F) c₁(E)in
A^*(X), wherer(E) = P_0(E)is the rank andc₁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,FofD(𝒪_X)whose Chern classes are defined and everyp ≥ 0,
P_p(E ⊗^L F) = ∑_{p₁ + p₂ = p} C(p, p₁) P_{p₁}(E) P_{p₂}(F)in
A^p(X), the power sumsP_0being the ranks; dividing byp!this isch(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,FofD(𝒪_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), wherer(E) = P_0(E)is the rank andC(r(E), 2)is the class of the locally constant functionx ↦ C(χ_E(x), 2),χ_Ebeing the Euler characteristic of the derived fibre ofE, whose class isr(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 ⊗^𝐋 Fare the sums of the Chern roots ofEandF. For presentations ofEandFon envelopes there are tensor split charts at every point of their common envelope, restriction to all of them is injective onA^*(X), and on each of them, withx_{n,j}the Chern roots ofEandy_{m,k}those ofF,
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 ⊗^𝐋 Fis the universal expression in the Chern roots ofEandF.
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)inA^*(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)²inA^*(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 ofr(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 ofr(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-pcomponent 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)inA^*(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
Xbe locally of finite type overSand letE,Fbe perfect objects ofD(𝒪_X)whose Chern classes are defined. Then the Chern classes ofE ⊗^𝐋 Fare defined, and inA^*(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 ⊗^𝐋 Fare the sumsx + yof those ofEandF, with the product signs;ch(E ⊗^𝐋 F) = ch(E) ch(F)inA^*(X) ⊗ 𝐐;- more precisely
P_p(E ⊗^𝐋 F) = ∑_{p₁ + p₂ = p} C(p, p₁) P_{p₁}(E) P_{p₂}(F)inA^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
Xbe locally of finite type overS, leti_j : X_j ⟶ Xbe closed immersions withX = X₁ ∪ X₂set theoretically, and letE₂be a perfect object ofD(𝒪_{X₂})whose Chern classes are defined and such thatE₂|_{X₁ ∩ X₂}is isomorphic to a finite locally free𝒪_{X₁ ∩ X₂}-module of rank< psitting in cohomological degree0. Then there is a unique bivariant classc'_p(E₂) ∈ A^p(X₂ ⟶ X)such that, on every test schemeg : X' ⟶ Xlocally of finite type, withi'_j : X'_j = X_j ×_X X' ⟶ X',
c'_p(E₂) ∩ i'_{2,*} α₂ = c_p(E₂) ∩ α₂andc'_p(E₂) ∩ i'_{1,*} α₁ = 0for all
α_j ∈ CH_k(X'_j); it isStacks.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. LetXbe locally of finite type overS, leti_j : X_j ⟶ Xbe closed immersions withX = X₁ ∪ X₂set theoretically, and letE₂be a perfect object ofD(𝒪_{X₂})whose Chern classes are defined and whose restrictionE₂|_{X₁ ∩ X₂}is zero. Then there is a unique bivariant classP'_p(E₂) ∈ A^p(X₂ ⟶ X)such that, on every test schemeg : X' ⟶ Xlocally of finite type, withi'_j : X'_j = X_j ×_X X' ⟶ X',
P'_p(E₂) ∩ i'_{2,*} α₂ = P_p(E₂) ∩ α₂andP'_p(E₂) ∩ i'_{1,*} α₁ = 0for all
α_j ∈ CH_k(X'_j); it isStacks.Chow.localizedPowerSumOfClosedCover. HereP_p(E₂)is the class of Definition 0F9E (2),Stacks.Chow.perfectPowerSumComponent: the class of Stacks 0GUD which restricts along every envelope presentation(f, 𝓔^•)ofE₂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₁ ⟶ Xandi₂ : X₂ ⟶ Xbe closed immersions whose images coverX, and letE₂ ∈ D(𝒪_{X₂})have defined Chern classes and restrict to zero onX₁ ×_X X₂. The classP'_p(E₂) ∈ A^p(X₂ ⟶ X)is the extension ofP_p(E₂) ∈ A^p(X₂)along the closed cover (Stacks.Chow.closedCoverExtension): on a test schemeT ⟶ X, writing a class asj_{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₁ ⟶ Xandi₂ : X₂ ⟶ Xbe closed immersions whose images coverX, and letE₂ ∈ D(𝒪_{X₂})have defined Chern classes and restrict onX₁ ×_X X₂to a finite locally free module of rank< pin degree0. The classc'_p(E₂) ∈ A^p(X₂ ⟶ X)is the extension ofc_p(E₂) ∈ A^p(X₂)along the closed cover (Stacks.Chow.closedCoverExtension): on a test schemeT ⟶ X, writing a class asj_{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 ⟶ Xlocally of finite type,P'_p(E₂)caps the classes pushed forward fromT ×_X X₂asP_p(E₂)does, and kills the classes pushed forward fromT ×_X X₁:P'_p(E₂) ∩ i_{2,*} α₂ = P_p(E₂) ∩ α₂andP'_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 formulasc ∩ i_{2,*} α₂ = P_p(E₂) ∩ α₂andc ∩ i_{1,*} α₁ = 0after every base change isP'_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 ⟶ Xlocally of finite type,c'_p(E₂)caps the classes pushed forward fromT ×_X X₂asc_p(E₂)does, and kills the classes pushed forward fromT ×_X X₁:c'_p(E₂) ∩ i_{2,*} α₂ = c_p(E₂) ∩ α₂andc'_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 formulasc ∩ i_{2,*} α₂ = c_p(E₂) ∩ α₂andc ∩ i_{1,*} α₁ = 0after every base change isc'_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₁: ifchas the characterizing property for the coverX = X₁ ∪ X₂andc'has it for the coverX = X₁' ∪ X₂, both with the same classκ ∈ A^p(X₂), thenc = c'.By Stacks 02UC it is enough that
c - c'kill the fundamental class of every integral schemeTlocally of finite type overX. Such aTis 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 ofT; 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 theX₂-piece fillsTthen both classes cap[T]toκ ∩ [T]; otherwise theX₁-piece and theX₁'-piece both fillT, 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< pin degree0, letq : X' ⟶ Xbe locally of finite type, letX' = X'₁ ∪ X'₂withX'_j = X_j ×_X X', and letE'₂ = (X'₂ ⟶ X₂)^* E₂. ThenE'₂satisfies the hypotheses of Stacks 0F9H for this cover, and the classc'_p(E'₂) ∈ A^p(X'₂ ⟶ X')constructed by Stacks 0F9H fromX' = X'₁ ∪ X'₂andE'₂is the restriction (Remark 0F9Z) ofc'_p(E₂) ∈ A^p(X₂ ⟶ X).The restriction is a class for
X₂ ×_X X' ⟶ X'whose source carries the structure morphismX₂ ×_X X' ⟶ X₂ ⟶ S, while the class of Stacks 0F9H atX'carriesX'₂ ⟶ X' ⟶ S; the two are equal, and the restriction is read with the second one byStacks.Chow.bivariantTransportalong 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, withE₂perfect andE₂|_{X₁ ∩ X₂}zero, letq : X' ⟶ Xbe locally of finite type, letX' = X'₁ ∪ X'₂withX'_j = X_j ×_X X', and letE'₂ = (X'₂ ⟶ X₂)^* E₂. ThenE'₂satisfies the hypotheses of Stacks 0F9H for this cover, and the classP'_p(E'₂) ∈ A^p(X'₂ ⟶ X')constructed by Stacks 0F9H fromX' = X'₁ ∪ X'₂andE'₂is the restriction (Remark 0F9Z) ofP'_p(E₂) ∈ A^p(X₂ ⟶ X), read with the structure morphismX'₂ ⟶ X' ⟶ Sas inStacks.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. LetXbe locally of finite type overS, leti_j : X_j ⟶ Xbe closed immersions withX = X₁ ∪ X₂set theoretically, and letEbe a perfect object ofD(𝒪_X)whose Chern classes are defined and whose restrictionE|_{X₁}is zero. ThenE₂ = E|_{X₂}satisfies the hypotheses of Stacks 0F9H withE₂|_{X₁ ∩ X₂}zero, and
i_{2,*} ∘ P'_p(E₂) = P_p(E)inA^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 andP_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
Xbe locally of finite type overS, leti_j : X_j ⟶ Xbe closed immersions withX = X₁ ∪ X₂set theoretically, and letEbe a perfect object ofD(𝒪_X)whose Chern classes are defined and whose restrictionE|_{X₁}is isomorphic to a finite locally free𝒪_{X₁}-module of rank< psitting in cohomological degree0. ThenE₂ = E|_{X₂}satisfies the hypotheses of Stacks 0F9H withE₂|_{X₁ ∩ X₂}finite locally free of rank< pin degree0, and
i_{2,*} ∘ c'_p(E₂) = c_p(E)inA^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 andc_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₁ ⟶ Xandi₂ : X₂ ⟶ Xbe closed immersions whose images coverX, and letE ∈ D(𝒪_X)have defined Chern classes and restrict to zero onX₁. LetE₂ = E|_{X₂}be as in Stacks 0F9H: it restricts to zero onX₁ ×_X X₂, and its Chern classes are defined byStacks.Chow.HasDefinedChernClasses.derivedPullback. Theni_{2,*} ∘ P'_p(E₂) = P_p(E)inA^p(X), withi_{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₁ ⟶ Xandi₂ : X₂ ⟶ Xbe closed immersions whose images coverX, and letE ∈ D(𝒪_X)have defined Chern classes and restrict onX₁to a finite locally free module of rank< pin degree0. LetE₂ = E|_{X₂}be as in Stacks 0F9H: it restricts onX₁ ×_X X₂to a finite locally free module of rank< pin degree0, and its Chern classes are defined byStacks.Chow.HasDefinedChernClasses.derivedPullback. Theni_{2,*} ∘ c'_p(E₂) = c_p(E)inA^p(X), withi_{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 immersionsi_j : X_j ⟶ XwithX = X₁ ∪ X₂set theoretically, andE₂ ∈ D(𝒪_{X₂})perfect with defined Chern classes andE₂|_{X₁ ∩ X₂}zero — letX₂' ⊂ X₂andX₁ ⊂ X₁' ⊂ Xbe closed subschemes withX = X₁' ∪ X₂'set theoretically, and assumeE₂|_{X₁' ∩ X₂}is zero. Then
(X₂' ⟶ X₂)_* ∘ P'_p(E₂|_{X₂'}) = P'_p(E₂)inA^p(X₂ ⟶ X),where
P'_p(E₂|_{X₂'}) ∈ A^p(X₂' ⟶ X)is the class of Stacks 0F9H for the coverX = X₁' ∪ X₂'(Stacks.Chow.localizedPowerSumOfClosedCover),P'_p(E₂)the one forX = 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 ⟶ XwithX = X₁ ∪ X₂set theoretically, andE₂ ∈ D(𝒪_{X₂})perfect with defined Chern classes andE₂|_{X₁ ∩ X₂}isomorphic to a finite locally free module of rank< pin degree0— letX₂' ⊂ X₂andX₁ ⊂ X₁' ⊂ Xbe closed subschemes withX = X₁' ∪ X₂'set theoretically, and assumeE₂|_{X₁' ∩ X₂}is isomorphic to a finite locally free module of rank< pplaced in degree0. Then
(X₂' ⟶ X₂)_* ∘ c'_p(E₂|_{X₂'}) = c'_p(E₂)inA^p(X₂ ⟶ X),where
c'_p(E₂|_{X₂'}) ∈ A^p(X₂' ⟶ X)is the class of Stacks 0F9H for the coverX = X₁' ∪ X₂'(Stacks.Chow.localizedChernClassOfClosedCover),c'_p(E₂)the one forX = 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. LetXbe locally of finite type overS, leti_j : X_j ⟶ Xbe closed immersions withX = X₁ ∪ X₂set theoretically, and letE₂ ∈ D(𝒪_{X₂})be an object whose Chern classes are defined and whose restriction toX₁ ∩ X₂is isomorphic to a finite locally free module of rank< pin degree0, so that Stacks 0F9H givesc'_p(E₂) ∈ A^p(X₂ ⟶ X). Letf : Y ⟶ Xbe locally of finite type andc ∈ A^r(Y ⟶ X). Then
c ∘ c'_p(E₂) = c'_p(Lf₂^*E₂) ∘ c,where
f₂ : X₂ ×_X Y ⟶ X₂is the base change offandc'_p(Lf₂^*E₂) ∈ A^p(X₂ ×_X Y ⟶ Y)is the class of Stacks 0F9H for the cover ofYby the base changesX_j ×_X Yand the derived pullbackLf₂^*E₂(which satisfies the hypotheses of Stacks 0F9H byStacks.Chow.hasDefinedChernClasses_baseChangeandStacks.Chow.exists_iso_single_baseChange). The left side isres(c) ∘ c'_p(E₂), a class forY ×_X X₂ ⟶ Xof degreer + p; the right side, a class forX₂ ×_X Y ⟶ Xof degreep + r, is read onY ×_X X₂through the symmetry of the fibre product. Perfectness ofE₂, assumed in Stacks 0F9H, is not used forc'_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. LetXbe locally of finite type overS, leti_j : X_j ⟶ Xbe closed immersions withX = X₁ ∪ X₂set theoretically, and letE₂ ∈ D(𝒪_{X₂})be a perfect object whose Chern classes are defined and whose restriction toX₁ ∩ X₂is zero, so that Stacks 0F9H givesP'_p(E₂) ∈ A^p(X₂ ⟶ X). Letf : Y ⟶ Xbe locally of finite type andc ∈ A^r(Y ⟶ X). Then
c ∘ P'_p(E₂) = P'_p(Lf₂^*E₂) ∘ c,where
f₂ : X₂ ×_X Y ⟶ X₂is the base change offandP'_p(Lf₂^*E₂) ∈ A^p(X₂ ×_X Y ⟶ Y)is the class of Stacks 0F9H for the cover ofYby the base changesX_j ×_X Yand the derived pullbackLf₂^*E₂, the composites being read as inStacks.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₂ ⟶ Xbe closed immersions coveringX, letE₂ ∈ D(𝒪_{X₂})have defined Chern classes and restrict to zero onX₁ ∩ X₂, letf : Y ⟶ Xbe locally of finite type and letc ∈ A^*(Y ⟶ X). Then
c ∘ P'_p(E₂) = P'_p(Lf₂^*E₂) ∘ cinA^*(Y₂ ⟶ X),where
Y₂ = X₂ ×_X Y,f₂ : Y₂ ⟶ X₂is the base change off,P'_p(Lf₂^*E₂) ∈ A^p(Y₂ ⟶ Y)is the class of Stacks 0F9H for the base-changed cover ofY, andc ∘ P'_p(E₂)is the composite of the restriction ofctoX₂withP'_p(E₂), carried fromY ×_X X₂toY₂.
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₂ ⟶ Xbe closed immersions coveringX, letE₂ ∈ D(𝒪_{X₂})have defined Chern classes and restrict onX₁ ∩ X₂to a finite locally free module of rank< pin degree0, letf : Y ⟶ Xbe locally of finite type and letc ∈ A^*(Y ⟶ X). Then
c ∘ c'_p(E₂) = c'_p(Lf₂^*E₂) ∘ cinA^*(Y₂ ⟶ X),where
Y₂ = X₂ ×_X Y,f₂ : Y₂ ⟶ X₂is the base change off,c'_p(Lf₂^*E₂) ∈ A^p(Y₂ ⟶ Y)is the class of Stacks 0F9H for the base-changed cover ofY, andc ∘ c'_p(E₂)is the composite of the restriction ofctoX₂withc'_p(E₂), carried fromY ×_X X₂toY₂.
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 onX₁ ∩ X₂, so thatc'_p(E₂)is defined for everyp ≥ 1. Then the classesP'_p(E₂) ∈ A^p(X₂ ⟶ X)are Newton's polynomials in the classesc'_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, soP'_1 = c'_1,P'_2 = c'_1² - 2c'_2,P'_3 = c'_1³ - 3c'_1c'_2 + 3c'_3, and so on. The summandc'_{j+1} P'_{p-j}lies inA^{(j+1)+(p-j)}(X₂ ⟶ X), read in degreep + 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 onX₁ ∩ 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'_4in
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") isStacks.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). Leti₁ : X₁ ⟶ X,i₂ : X₂ ⟶ Xbe closed immersions whose images coverX, and letE ∈ D(𝒪_X)have defined Chern classes, with(E|_{X₂})|_{X₁ ∩ X₂}isomorphic to a finite locally free module of rank< pplaced in degree0. 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 < pisc_i(E) ∈ A^i(X), in a negative degree it is0, and in a degreei ≥ pit is the classc'_i(E|_{X₂}) ∈ A^i(X₂ ⟶ X)of Stacks 0F9H (Stacks.Chow.closedCoverChernClass), which is defined since a rank< pis 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₂ ⟶ Xbe closed immersions withX = X₁ ∪ X₂set-theoretically, and letE, F ∈ D(𝒪_X)have defined Chern classes, withE|_{X₁}andF|_{X₁}isomorphic to finite locally free𝒪_{X₁}-modules of rank< pand< qplaced in degree0. Then
c^{(p+q)}(E ⊕ F) = c^{(p)}(E) c^{(q)}(F)inA^{(p+q)}(X₂ ⟶ X),with the multiplication of Stacks 0FA0 (
Stacks.Chow.localizedGradingMul). The hypotheses of Stacks 0F9H onE|_{X₂},F|_{X₂}and(E ⊕ F)|_{X₂}, under which the classesc^{(·)}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 ofE ⊕ F(Stacks.Chow.hasDefinedChernClasses_biprod).The correction. The source assumes in (2) that the restrictions
E|_{X₁ ∩ X₂}andF|_{X₁ ∩ X₂}are finite locally free of rank< p,< q(calling them𝒪_{X₁}-modules). As written, onX₁ ∩ X₂, the statement is false: letX = X₁ ⊔ X₂be a disjoint union ofX₁ = ℙ¹_kover a field and a pointX₂, so that (2) is vacuous; takeE = 𝒪(1)^{⊕ 2}onX₁and0onX₂,F = 0andp = q = 1. In degree1 < p + qthe component ofc^{(2)}(E ⊕ F)isc_1(E) ≠ 0, while that ofc^{(1)}(E) c^{(1)}(F)is(i_{2,*} c'_1(E|_{X₂})) · 1 + 1 · (i_{2,*} c'_1(0)) = 0. The hypothesis onX₁, to which the phrase "𝒪_{X₁}-modules" points, is the one Stacks 0F9I needs to compare the pushed classesi_{2,*} c'_i(E|_{X₂})withc_i(E), and with it the statement holds. Perfectness ofE,Fis 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₂ ⟶ Xbe closed immersions withX = X₁ ∪ X₂set-theoretically, and letE, F ∈ D(𝒪_{X₂})have defined Chern classes and restrict to zero onX₁ ∩ X₂. ThenP'_p(E ⊕ F) = P'_p(E) + P'_p(F)inA^p(X₂ ⟶ X)for everyp ≥ 0, withP'_pthe classes of Stacks 0F9H. (The Chern classes ofE ⊕ Fare defined and it restricts to zero onX₁ ∩ X₂, soP'_p(E ⊕ F)is defined; perfectness ofE,Fis 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 onX₁ ∩ X₂to a finite locally free module of rank< pplaced in degree0— assume thatE₂has constant rank0, and letℒbe an invertible𝒪_X-module. Then the restriction ofE₂toX₁ ∩ X₂is zero (hzeroin the statement, by the assumption on the rank), soc'_i(E₂)andc'_i(E₂ ⊗ ℒ)are defined for everyi ≥ 1, and
c'_i(E₂ ⊗ ℒ) = ∑_{j=0}^{i-1} binom(-i + j, j) c'_{i-j}(E₂) c_1(ℒ)^jin
A^i(X₂ ⟶ X). HereE₂ ⊗ ℒis the twist ofE₂byℒ|_{X₂}(Stacks 0FAF),c_1(ℒ)^j ∈ A^j(X), and the productA^{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 degreei.
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. LetX = X₁ ∪ X₂ = X₁' ∪ X₂'be two closed covers and letE,E' ∈ D(𝒪_X)be perfect objects whose Chern classes are defined and which restrict to zero onX₁andX₁'. Writeχ_p = P'_p(E|_{X₂})andχ'_p = P'_p(E'|_{X₂'})for the classes of Stacks 0F9H. LetY ⊆ Xbe the reduced closed subscheme with underlying setX₁ ∪ X₁'(Stacks.Chow.reducedUnionIdeal); thenX = Y ∪ (X₂ ∩ X₂'), andE ⊗^L E'restricts to zero onY ∩ (X₂ ∩ X₂'), so the class of Stacks 0F9H of(E ⊗^L E')|_{X₂ ∩ X₂'}alongX = Y ∪ (X₂ ∩ X₂')is defined; by Stacks 0FAH it does not depend on the choice ofY. 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 ofStacks.Chow.supportedIntersectionMul, each summand read in degreep.
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. LetX = X₁ ∪ X₂ = X₁' ∪ X₂'be two closed covers and letE,E' ∈ D(𝒪_X)be perfect objects whose Chern classes are defined and which restrict to zero onX₁andX₁'. Writer = 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. LetY ⊆ Xbe the reduced closed subscheme with underlying setX₁ ∪ X₁'(Stacks.Chow.reducedUnionIdeal); thenX = Y ∪ (X₂ ∩ X₂'), andE ⊗^L E'restricts to zero onY ∩ (X₂ ∩ X₂'), so the class of Stacks 0F9H of(E ⊗^L E')|_{X₂ ∩ X₂'}alongX = Y ∪ (X₂ ∩ X₂')is defined; by Stacks 0FAH it does not depend on the choice ofY. Then
c'_1((E ⊗^L E')|_{X₂ ∩ X₂'}) = r γ'_1 + r' γ_1in
A^1(X₂ ∩ X₂' ⟶ X), with the product ofStacks.Chow.supportedIntersectionMul(forr' γ_1along the pullback square with the two factors exchanged), each summand read in degree1.
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. LetX = X₁ ∪ X₂ = X₁' ∪ X₂'be two closed covers and letE,E' ∈ D(𝒪_X)be perfect objects whose Chern classes are defined and which restrict to zero onX₁andX₁'. Writer = 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, andC(r, 2),C(r', 2)for the classesStacks.Chow.closedCoverRankChoose. LetY ⊆ Xbe the reduced closed subscheme with underlying setX₁ ∪ X₁'(Stacks.Chow.reducedUnionIdeal); thenX = Y ∪ (X₂ ∩ X₂'), andE ⊗^L E'restricts to zero onY ∩ (X₂ ∩ X₂'), so the class of Stacks 0F9H of(E ⊗^L E')|_{X₂ ∩ X₂'}alongX = Y ∪ (X₂ ∩ X₂')is defined; by Stacks 0FAH it does not depend on the choice ofY. 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 onX₂and a class onX₂'are those ofStacks.Chow.supportedIntersectionMul, the squares(γ'_1)²,γ_1²and the product ofr r'withγ'_1 γ_1are the third multiplication of Stacks 0FA0 (Stacks.Chow.supportedMul), and each summand is read in degree2.
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.