42.48 Gysin at infinity to 42.53 Blowing up at infinity

Section42.48 Gysin at infinity #

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

Tag 0F9J, a lemma

Tag 0F9J in the Stacks Project.

Stacks.Chow.gysinCapOfLift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinity.lean, line 270. The attribute's comment: “construction of the cap operation from a lift and a zero-scheme presentation”.

The cap operation C ∩ - : A_k(T) ⟶ A_k(W_∞ ×_X T) built from a choice of lift: given a homomorphism lift : A_k(T) ⟶ A_{k+1}(W ×_X T) and a presentation of the base-changed fibre at infinity as the zero scheme of a global section s of an invertible module L on W ×_X T, it is i_∞^* ∘ lift, where i_∞^* is the Gysin map of s followed by the identification e of that zero scheme with W_∞ ×_X T.

def gysinCapOfLift (C : ChowSituation.{u}) (G : GysinSystem C) {X W T : Scheme.{u}}
    (f : X ⟶ C.S) [LocallyOfFiniteType f] (b : W ⟶ projectiveLineProduct f)
    [LocallyOfFiniteType (modificationProjection f b)]
    [LocallyOfFiniteType (modificationProjectionAtInfinity f b)]
    (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
    (L : (modificationBaseChange f b g).Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible (modificationBaseChange f b g).sheaf.obj
      (modificationBaseChange f b g).ringCatSheaf.property L]
    (s : Γ(L, ⊤))
    (e : (Stacks.Divisors.zeroScheme (modificationBaseChange f b g) L s).subscheme ≅
      pullback (modificationProjectionAtInfinity f b) g)
    (he : e.hom ≫ modificationInfinityBaseChangeOver f b g =
      modificationZeroSchemeOver C f b g L s)
    (lift : chowGroup C (g ≫ f) k →+ chowGroup C (modificationBaseChangeOver f b g) (k + 1)) :
    chowGroup C (g ≫ f) k →+ chowGroup C (modificationInfinityBaseChangeOver f b g) k

Stacks.Chow.gysinCapOfLift_eq_of_gysin_pushforward_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinity.lean, line 315. The attribute's comment: “independence of the chosen lift”.

Two lifts whose difference is pushed forward from the fibre at infinity give the same cap operation, as soon as the Gysin map of s kills everything pushed forward from the fibre at infinity.

theorem gysinCapOfLift_eq_of_gysin_pushforward_eq_zero (C : ChowSituation.{u})
    (G : GysinSystem C) {X W T : Scheme.{u}} (f : X ⟶ C.S) [LocallyOfFiniteType f]
    (b : W ⟶ projectiveLineProduct f) [LocallyOfFiniteType (modificationProjection f b)]
    [LocallyOfFiniteType (modificationProjectionAtInfinity f b)]
    (g : T ⟶ X) [LocallyOfFiniteType g] [IsProper (modificationInfinityBaseChange f b g)]
    (k : ℤ) (L : (modificationBaseChange f b g).Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible (modificationBaseChange f b g).sheaf.obj
      (modificationBaseChange f b g).ringCatSheaf.property L]
    (s : Γ(L, ⊤))
    (e : (Stacks.Divisors.zeroScheme (modificationBaseChange f b g) L s).subscheme ≅
      pullback (modificationProjectionAtInfinity f b) g)
    (he : e.hom ≫ modificationInfinityBaseChangeOver f b g =
      modificationZeroSchemeOver C f b g L s)
    (lift lift' : chowGroup C (g ≫ f) k →+
      chowGroup C (modificationBaseChangeOver f b g) (k + 1))
    (hfac : ProperPushforwardFactorsThroughRationalEquivalence C
      (modificationInfinityBaseChangeOver f b g) (modificationBaseChangeOver f b g)
      (modificationInfinityBaseChange f b g) (modificationInfinityBaseChange_over f b g) (k + 1))
    (hvanish : ∀ γ : chowGroup C (modificationInfinityBaseChangeOver f b g) (k + 1),
      G.onChow (modificationBaseChangeOver f b g) L s k
        (properChowPushforward C (modificationInfinityBaseChangeOver f b g)
          (modificationBaseChangeOver f b g) (modificationInfinityBaseChange f b g)
          (modificationInfinityBaseChange_over f b g) (k + 1) hfac γ) = 0)
    (hdiff : ∀ α : chowGroup C (g ≫ f) k,
      ∃ γ : chowGroup C (modificationInfinityBaseChangeOver f b g) (k + 1),
        lift α - lift' α =
          properChowPushforward C (modificationInfinityBaseChangeOver f b g)
            (modificationBaseChangeOver f b g) (modificationInfinityBaseChange f b g)
            (modificationInfinityBaseChange_over f b g) (k + 1) hfac γ) :
    gysinCapOfLift C G f b g k L s e he lift =
      gysinCapOfLift C G f b g k L s e he lift'

Stacks.Chow.GysinAtInfinityData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinity.lean, line 360. The attribute's comment: “statement: the canonical class in A⁰(W_∞ ⟶ X) and its pushforward identity”.

The conclusion of the Gysin-at-infinity lemma, for a proper morphism b : W ⟶ 𝐏¹_X which is an isomorphism over the standard affine chart 𝐀¹_X: a degree-zero bivariant class C ∈ A⁰(W_∞ ⟶ X) for the fibre at infinity, together with the identity i_{∞,*}(C ∩ α) = i_{0,*} α on every test scheme locally of finite type over X.

structure GysinAtInfinityData (C : ChowSituation.{u}) (G : GysinSystem C) {X W : Scheme.{u}}
    (f : X ⟶ C.S) [LocallyOfFiniteType f] (b : W ⟶ projectiveLineProduct f) [IsProper b]
    (_hA : IsIso (pullback.snd b (projectiveLineAffineChart f)))

Stacks.Chow.GysinAtInfinity.gysinAtInfinity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinity/Statement.lean, line 109.

Stacks 0F9J. Let X be locally of finite type over the base of chapter 42 and let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, with fibre at infinity i_∞ : W_∞ ⟶ W. The class C = gysinAtInfinityClass ∈ A⁰(W_∞ ⟶ X)

is constructed as in the source: C ∩ α = i_∞^* β for every lift β of α;

is canonical: it is the only class with that property;

satisfies i_{∞,*}(C ∩ α) = i_{0,*} α on every test scheme T ⟶ X locally of finite type, that is, for α ∈ A_k(X) and similarly after any base change by X' ⟶ X locally of finite type; here i_0 and i_∞ are the base changes of the section at zero and of the inclusion of the fibre at infinity.

theorem gysinAtInfinity :
    IsGysinAtInfinityCap C f b hA (gysinAtInfinityClass C f b hA) ∧
      (∀ c, IsGysinAtInfinityCap C f b hA c → c = gysinAtInfinityClass C f b hA) ∧
      haveI := hA
      ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (g ≫ f) k),
        properChowPushforward C (modificationInfinityBaseChangeOver f b g)
            (modificationBaseChangeOver f b g) (modificationInfinityBaseChange f b g)
            (modificationInfinityBaseChange_over f b g) k
            (properPushforwardFactorsThroughRationalEquivalence_of_isProper C _ _ _ _ k)
            (Eq.mp (congrArg (chowGroup C (modificationInfinityBaseChangeOver f b g))
              (sub_zero k)) ((gysinAtInfinityClass C f b hA).cap g k α)) =
          properChowPushforward C (g ≫ f) (modificationBaseChangeOver f b g)
            (modificationSectionAtZeroBaseChange f b inferInstance
              (modificationSectionAtZero_comp f b) g)
            (modificationSectionAtZeroBaseChange_over f b g inferInstance
              (modificationSectionAtZero_comp f b)) k
            (properPushforwardFactorsThroughRationalEquivalence_of_isProper C _ _ _ _ k) α

Stacks.Chow.gysinAtInfinityClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityClass.lean, line 64. The attribute's comment: “the canonical bivariant class C in A⁰(W_∞ ⟶ X)”.

Stacks 0F9J, the class at infinity. The degree-zero bivariant class C ∈ A⁰(W_∞ ⟶ X) whose cap operation on a test scheme T ⟶ X is α ↦ i_∞^* β for a lift β of α to W ×_X T (Stacks.Chow.gysinCapAtInfinity).

def gysinAtInfinityClass :
    BivariantClass C (gysinSystemOfInvertible C) (modificationProjectionAtInfinity f b ≫ f) f
      (modificationProjectionAtInfinity f b) rfl 0

Stacks.Chow.gysinAtInfinityData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityClass.lean, line 112. The attribute's comment: “the class C in A⁰(W_∞ ⟶ X) with i_{∞,}(C ∩ α) = i_{0,} α, built from the cap operation i_∞^* of a lift and its three bivariance laws”.

Stacks 0F9J. The class at infinity C ∈ A⁰(W_∞ ⟶ X) of Stacks.Chow.gysinAtInfinityClass together with the identity i_{∞,*}(C ∩ α) = i_{0,*} α on every test scheme locally of finite type over X (Stacks.Chow.chowPushforward_gysinCapOfLift).

def gysinAtInfinityData : GysinAtInfinityData C (gysinSystemOfInvertible C) f b hA

Stacks.Chow.gysinCapAtInfinity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityLift.lean, line 702. The attribute's comment: “the cap operation of the class at infinity on a test scheme: i_∞^* of a lift”.

Stacks 0F9J, the cap operation. C ∩ - : A_k(T) ⟶ A_k(W_∞ ×_X T), α ↦ i_∞^* β for a lift β of α (Stacks.Chow.IsModificationLift). A lift is chosen; by Stacks.Chow.gysinCapAtInfinity_eq_of_isModificationLift the value is the same for every lift, and that independence is what makes the operation additive.

def gysinCapAtInfinity :
    chowGroup C (g ≫ f) k →+ chowGroup C (modificationInfinityBaseChangeOver f b g) k

Stacks.Chow.gysinCapAtInfinity_eq_of_isModificationLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityLift.lean, line 726. The attribute's comment: “independence of the chosen lift: C ∩ α = i_∞^* β for every lift β of α”.

Stacks 0F9J, independence of the chosen lift. The cap operation is i_∞^* β for every lift β of α: two lifts differ by a class supported on the fibre at infinity (Stacks 02RX), and the Gysin map at infinity kills such classes because the normal bundle of the divisor at infinity is trivial (Remark 0B6Z).

theorem gysinCapAtInfinity_eq_of_isModificationLift (α : chowGroup C (g ≫ f) k)
    (β : chowGroup C (modificationBaseChangeOver f b g) (k + 1))
    (hβ : IsModificationLift C f b hA g k α β) :
    gysinCapAtInfinity C f b hA g k α = modificationInfinityGysin C f b g k β

Stacks.Chow.GysinAtInfinityCapPresentation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityPresentation.lean, line 56. The attribute's comment: “the construction of the class at infinity, as a presentation of its cap operation by a lift and a Gysin step”.

A presentation of the cap operation of the Gysin class at infinity C ∈ A⁰(W_∞ ⟶ X) as the composite of a lift with the Gysin map of the divisor at infinity: on every test scheme g : T ⟶ X locally of finite type and in every degree k, additive maps lift : CH_k(T) ⟶ CH_{k+1}(W ×_X T) and gysinStep : CH_{k+1}(W ×_X T) ⟶ CH_k(W_∞ ×_X T) with C ∩ α = gysinStep (lift α).

structure GysinAtInfinityCapPresentation (C : ChowSituation.{u}) (G : GysinSystem C)
    {X W : Scheme.{u}} (f : X ⟶ C.S) [LocallyOfFiniteType f]
    (b : W ⟶ projectiveLineProduct f) [IsProper b]
    (hA : IsIso (pullback.snd b (projectiveLineAffineChart f)))
    [LocallyOfFiniteType (modificationProjection f b)]
    [LocallyOfFiniteType (modificationProjectionAtInfinity f b)]
    (D : GysinAtInfinityData C G f b hA)

Stacks.Chow.chowPushforward_gysinCapOfLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityPushforward.lean, line 736. The attribute's comment: “the pushforward identity i_{∞,}(C ∩ α) = i_{0,} α on every test scheme locally of finite type over X”.

Stacks 0F9J, the pushforward identity. On every test scheme g : T ⟶ X locally of finite type, i_{∞,*}(C ∩ α) = i_{0,*} α in A_k(W ×_X T), for the cap operation Stacks.Chow.gysinCapAtInfinity of the class at infinity.

For a lift β of α, C ∩ α = i_∞^* β; the Gysin images i_∞^* β and i_0^* β have the same pushforward to W ×_X T, the divisors D_0 and D_∞ of 𝐏¹ being rationally equivalent (Stacks.Chow.modificationZeroGysin_eq_infinityGysin); and i_0^* β = α (Stacks.Chow.chowPushforward_zeroGysin_of_isModificationLift).

theorem chowPushforward_gysinCapOfLift
    (hA : IsIso (pullback.snd b (projectiveLineAffineChart f))) (k : ℤ)
    (α : chowGroup C (g ≫ f) k) :
    haveI := isClosedImmersion_modificationSectionAtZeroBaseChange f b g hA
    chowPushforwardOfIsClosedImmersion C (modificationInfinityBaseChangeOver f b g)
        (modificationBaseChangeOver f b g) (modificationInfinityBaseChange f b g)
        (modificationInfinityBaseChange_over f b g) k (gysinCapAtInfinity C f b hA g k α) =
      chowPushforwardOfIsClosedImmersion C (g ≫ f) (modificationBaseChangeOver f b g)
        (modificationSectionAtZeroBaseChange f b (isIso_modificationFibreAtZeroProjection f b hA)
          (modificationSectionAtZero_comp_projection f b hA) g)
        (modificationSectionAtZeroBaseChange_over f b g _ _) k α

Tag 0GUH, a lemma

Tag 0GUH in the Stacks Project.

Stacks.Chow.GysinAtInfinity.gysinAtInfinityClass_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinity/BaseChange.lean, line 583.

Stacks 0GUH. Let X be locally of finite type over the base of chapter 42, let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, and let C ∈ A⁰(W_∞ ⟶ X) be the class of Stacks 0F9J. Let q : X' ⟶ X be locally of finite type and let b' : W' = W ×_{𝐏¹_X} 𝐏¹_{X'} ⟶ 𝐏¹_{X'} be the base change of b, with fibre at infinity i'_∞ : W'_∞ ⟶ W' (the base change of i_∞). Then b' is again proper and an isomorphism over 𝐀¹_{X'}, and the class C' ∈ A⁰(W'_∞ ⟶ X') constructed as in Stacks 0F9J using b' is the restriction res(C) of Remark 0F9Z.

The restriction is a class for the chosen fibre product W_∞ ×_X X' ⟶ X'; it is read as a class for W'_∞ ⟶ X' along the canonical identification W_∞ ×_X X' ≅ W'_∞ over X'.

theorem gysinAtInfinityClass_baseChange
    (hA : IsIso (pullback.snd b (projectiveLineAffineChart f))) :
    haveI := hA
    gysinAtInfinityClass C (q ≫ f) (baseChangedModification f b q) inferInstance =
      bivariantTransport C (gysinSystemOfInvertible C)
        (pullback.fst (modificationProjectionAtInfinity f b) q ≫
          (modificationProjectionAtInfinity f b ≫ f))
        (modificationProjectionAtInfinity (q ≫ f) (baseChangedModification f b q) ≫ (q ≫ f))
        (q ≫ f) (pullback.snd (modificationProjectionAtInfinity f b) q)
        (pullbackSnd_comp_structureMorphism_eq C (modificationProjectionAtInfinity f b ≫ f) f
          (modificationProjectionAtInfinity f b) rfl q)
        (modificationProjectionAtInfinity (q ≫ f) (baseChangedModification f b q)) rfl
        (baseChangedInfinityIso f b q) (baseChangedInfinityIso_hom_comp f b q) 0
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (bivariantRestrictionOfInvertible C (modificationProjectionAtInfinity f b ≫ f) f
          (modificationProjectionAtInfinity f b) rfl q 0 (gysinAtInfinityClass C f b hA))

Stacks.Chow.gysinAtInfinity_baseChange_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityBaseChange.lean, line 263. The attribute's comment: “on cap operations: given the construction of Stacks 0F9J as a presentation of each cap operation by a lift and a Gysin step, and the compatibility of each of those two factors with the base change (the source's a similar statement holds for flat pullback and i_infty^*), the class constructed from the base-changed modification caps as the original one does”.

Stacks 0GUH, on cap operations, conditional on the construction of Stacks 0F9J for both modifications and its compatibility with base change.

For every test scheme g : T ⟶ X' locally of finite type, C' ∩ α = C ∩ α after the canonical identification W_∞ ×_X T ≅ W'_∞ ×_{X'} T of the two base changes of the fibre at infinity. This is the form the source's proof produces; the equality of bivariant classes asserted by the tag is Stacks.Chow.gysinAtInfinity_eq_bivariantTransport_bivariantRestriction.

theorem gysinAtInfinity_baseChange_cap
    (hlift : ∀ {T : Scheme.{u}} (g : T ⟶ X') [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (g ≫ (q ≫ f)) k),
      P'.lift g k α =
        chowPushforwardOfIso C (modificationBaseChangeOver f b (g ≫ q))
          (modificationBaseChangeOver (q ≫ f) b' g)
          (modificationBaseChangeComparison C f b q b' η hη g)
          (modificationBaseChangeComparison_comp_base C f b q b' η hη g) (k + 1)
          (P.lift (g ≫ q) k (chowGroupCongr C (Category.assoc g q f).symm k α)))
    (hgysinStep : ∀ {T : Scheme.{u}} (g : T ⟶ X') [LocallyOfFiniteType g] (k : ℤ)
        (β : chowGroup C (modificationBaseChangeOver f b (g ≫ q)) (k + 1)),
      P'.gysinStep g k
          (chowPushforwardOfIso C (modificationBaseChangeOver f b (g ≫ q))
            (modificationBaseChangeOver (q ≫ f) b' g)
            (modificationBaseChangeComparison C f b q b' η hη g)
            (modificationBaseChangeComparison_comp_base C f b q b' η hη g) (k + 1) β) =
        chowPushforwardOfIso C (modificationInfinityBaseChangeOver f b (g ≫ q))
          (modificationInfinityBaseChangeOver (q ≫ f) b' g)
          (modificationInfinityBaseChangeComparison C f b q b' θ hθ g)
          (modificationInfinityBaseChangeComparison_comp_base C f b q b' θ hθ g) k
          (P.gysinStep (g ≫ q) k β))
    {T : Scheme.{u}} (g : T ⟶ X') [LocallyOfFiniteType g] (k : ℤ)
    (α : chowGroup C (g ≫ (q ≫ f)) k) :
    D'.bivariantClass.cap g k α =
      chowPushforwardOfIso C (modificationInfinityBaseChangeOver f b (g ≫ q))
        (modificationInfinityBaseChangeOver (q ≫ f) b' g)
        (modificationInfinityBaseChangeComparison C f b q b' θ hθ g)
        (modificationInfinityBaseChangeComparison_comp_base C f b q b' θ hθ g) (k - 0)
        (D.bivariantClass.cap (g ≫ q) k
          (chowGroupCongr C (Category.assoc g q f).symm k α))

Stacks.Chow.gysinAtInfinity_eq_bivariantTransport_bivariantRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityBaseChange.lean, line 345. The attribute's comment: “given the construction of Stacks 0F9J as a presentation of each cap operation by a lift and a Gysin step, and the compatibility of each of those two factors with the base change (the source's a similar statement holds for flat pullback and i_infty^*), together with the isomorphism case of Stacks 02TA for the Gysin system that Stacks 0F9Z needs”.

Stacks 0GUH. In the setting of Stacks 0F9J let q : X' ⟶ X be locally of finite type and let b' : W' ⟶ 𝐏¹_{X'} and i'_∞ : W'_∞ ⟶ W' be the base changes of b and i_∞. Then the class C' ∈ A⁰(W'_∞ ⟶ X') constructed as in Stacks 0F9J using b' is the restriction (Remark 0F9Z) of C: it equals Stacks.Chow.bivariantRestriction of C along q, carried along the identification W_∞ ×_X X' ≅ W'_∞ by Stacks.Chow.bivariantTransport.

The transport is needed only because Stacks.Chow.bivariantRestriction produces a class for the chosen fibre product W_∞ ×_X X' ⟶ X', whereas C' is a class for W'_∞ ⟶ X'; the tag identifies the two silently. Both constructions are the library's own.

The hypotheses are the base-change witnesses η, θ, the construction of Stacks 0F9J for both modifications, and the compatibility of each of its two factors with the base change; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.GysinAtInfinityBaseChange.

theorem gysinAtInfinity_eq_bivariantTransport_bivariantRestriction
    (hgys : G.IsNaturalUnderBaseChangeIso)
    (hlift : ∀ {T : Scheme.{u}} (g : T ⟶ X') [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (g ≫ (q ≫ f)) k),
      P'.lift g k α =
        chowPushforwardOfIso C (modificationBaseChangeOver f b (g ≫ q))
          (modificationBaseChangeOver (q ≫ f) b' g)
          (modificationBaseChangeComparison C f b q b' η hη g)
          (modificationBaseChangeComparison_comp_base C f b q b' η hη g) (k + 1)
          (P.lift (g ≫ q) k (chowGroupCongr C (Category.assoc g q f).symm k α)))
    (hgysinStep : ∀ {T : Scheme.{u}} (g : T ⟶ X') [LocallyOfFiniteType g] (k : ℤ)
        (β : chowGroup C (modificationBaseChangeOver f b (g ≫ q)) (k + 1)),
      P'.gysinStep g k
          (chowPushforwardOfIso C (modificationBaseChangeOver f b (g ≫ q))
            (modificationBaseChangeOver (q ≫ f) b' g)
            (modificationBaseChangeComparison C f b q b' η hη g)
            (modificationBaseChangeComparison_comp_base C f b q b' η hη g) (k + 1) β) =
        chowPushforwardOfIso C (modificationInfinityBaseChangeOver f b (g ≫ q))
          (modificationInfinityBaseChangeOver (q ≫ f) b' g)
          (modificationInfinityBaseChangeComparison C f b q b' θ hθ g)
          (modificationInfinityBaseChangeComparison_comp_base C f b q b' θ hθ g) k
          (P.gysinStep (g ≫ q) k β)) :
    D'.bivariantClass =
      bivariantTransport C G
        (pullback.fst (modificationProjectionAtInfinity f b) q ≫
          (modificationProjectionAtInfinity f b ≫ f))
        (modificationProjectionAtInfinity (q ≫ f) b' ≫ (q ≫ f)) (q ≫ f)
        (pullback.snd (modificationProjectionAtInfinity f b) q)
        (pullbackSnd_comp_structureMorphism_eq C (modificationProjectionAtInfinity f b ≫ f) f
          (modificationProjectionAtInfinity f b) rfl q)
        (modificationProjectionAtInfinity (q ≫ f) b') rfl θ hθ 0 hgys
        (bivariantRestriction C G (modificationProjectionAtInfinity f b ≫ f) f
          (modificationProjectionAtInfinity f b) rfl q 0 hgys D.bivariantClass)

Stacks.Chow.gysinAtInfinityClass_restrictedModification_eq_bivariantRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityRestrictedBaseChange.lean, line 288. The attribute's comment: “the class C' of Lemma 0F9J for the base change b' is the restriction of C”.

In the setting of Stacks 0F9J let q : X' ⟶ X be locally of finite type and let b' : W' = W ×_{𝐏¹_X} 𝐏¹_{X'} ⟶ 𝐏¹_{X'} and i'_∞ : W'_∞ ⟶ W' be the base changes of b and i_∞ (Stacks.Chow.GysinAtInfinity.baseChangedModification). Then the class C' ∈ A⁰(W'_∞ ⟶ X') of Stacks 0F9J for b' is the restriction (Remark 0F9Z) of C: it equals Stacks.Chow.bivariantRestriction of C along q, carried along the canonical identification W_∞ ×_X X' ≅ W'_∞ by Stacks.Chow.bivariantTransport.

theorem gysinAtInfinityClass_restrictedModification_eq_bivariantRestriction :
    gysinAtInfinityClass C (q ≫ f) (baseChangedModification f b q)
        (isIso_restrictedModification_affineChart f b q hA) =
      bivariantTransport C (gysinSystemOfInvertible C)
        (pullback.fst (modificationProjectionAtInfinity f b) q ≫
          (modificationProjectionAtInfinity f b ≫ f))
        (modificationProjectionAtInfinity (q ≫ f) (baseChangedModification f b q) ≫ (q ≫ f))
        (q ≫ f) (pullback.snd (modificationProjectionAtInfinity f b) q)
        (pullbackSnd_comp_structureMorphism_eq C (modificationProjectionAtInfinity f b ≫ f) f
          (modificationProjectionAtInfinity f b) rfl q)
        (modificationProjectionAtInfinity (q ≫ f) (baseChangedModification f b q)) rfl
        (restrictedModificationInfinityIso f b q)
        (restrictedModificationInfinityIso_hom_projection f b q) 0
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (bivariantRestriction C (gysinSystemOfInvertible C)
          (modificationProjectionAtInfinity f b ≫ f) f (modificationProjectionAtInfinity f b) rfl
          q 0 (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
          (gysinAtInfinityClass C f b hA))

Tag 0FAQ, a lemma

Tag 0FAQ in the Stacks Project.

Stacks.Chow.gysinAtInfinityClass_properPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/GysinAtInfinityClassProperPushforward.lean, line 206. The attribute's comment: “g_{∞,*} ∘ C' = C for the canonical classes of Lemma 0F9J”.

Stacks 0FAQ. Let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, and let g : W' ⟶ W be proper and an isomorphism over 𝐀¹_X. Let C' ∈ A⁰(W'_∞ ⟶ X) and C ∈ A⁰(W_∞ ⟶ X) be the classes of Stacks 0F9J for b ∘ g and for b (Stacks.Chow.gysinAtInfinityClass). Then g_{∞,*} ∘ C' = C, the left side being the proper pushforward of Stacks 0EPK along g_∞ : W'_∞ ⟶ W_∞.

theorem gysinAtInfinityClass_properPushforward :
    bivariantProperPushforwardOfInvertible C (modificationProjectionAtInfinity f (g ≫ b) ≫ f)
        (modificationProjectionAtInfinity f b ≫ f) f (modificationFibreAtInfinityMap f b g)
        (modificationProjectionAtInfinity f b) (modificationFibreAtInfinityMap_comp_over f b g)
        rfl 0
        ((gysinAtInfinityClass C f (g ≫ b)
            (isIso_pullbackSnd_comp_projectiveLineAffineChart f b g hA hg)).congrHom
          (modificationProjectionAtInfinity_comp_eq f b g)
          (comp_comp_structureMorphism_eq (modificationFibreAtInfinityMap_comp_over f b g) rfl)) =
      gysinAtInfinityClass C f b hA

Stacks.Chow.GysinAtInfinity.properPushforward_gysinAtInfinityClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinity/ProperModification.lean, line 606.

Stacks 0FAQ. Let X be locally of finite type over the base of chapter 42, let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, and let g : W' ⟶ W be proper and an isomorphism over 𝐀¹_X, that is, over b⁻¹(𝐀¹_X). Let C' ∈ A⁰(W'_∞ ⟶ X) and C ∈ A⁰(W_∞ ⟶ X) be the classes of Stacks 0F9J for b ∘ g and for b. Then

g_{∞,*} ∘ C' = C in A⁰(W_∞ ⟶ X),

where g_∞ : W'_∞ ⟶ W_∞ is the restriction of g and the left side is the proper pushforward of Stacks 0EPK. The class C' is read for the morphism g_∞ ≫ (W_∞ ⟶ X), which equals the structure morphism W'_∞ ⟶ X, through Stacks.Chow.BivariantClass.copy.

theorem properPushforward_gysinAtInfinityClass
    (hA : IsIso (pullback.snd b (projectiveLineAffineChart f)))
    (hg : IsIso (pullback.snd g (chartInclusion f b))) :
    haveI := hA
    haveI := hg
    canonicalBivariantProperPushforward C (modificationProjectionAtInfinity f (g ≫ b) ≫ f)
        (modificationProjectionAtInfinity f b ≫ f) f (infinityMap f b g)
        (modificationProjectionAtInfinity f b)
        (by rw [← Category.assoc, infinityMap_comp_projection]) rfl 0
        (BivariantClass.copy C (canonicalGysinSystem C)
          (modificationProjectionAtInfinity f (g ≫ b) ≫ f) f
          (infinityMap_comp_projection f b g).symm rfl
          (by rw [infinityMap_comp_projection]) rfl
          (gysinAtInfinityClass C f (g ≫ b) (isIso_pullbackSnd_comp f b g))) =
      gysinAtInfinityClass C f b hA

Tag 0FAR, a lemma

Tag 0FAR in the Stacks Project.

Stacks.Chow.GysinAtInfinity.gysinAtInfinity_retraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinity/RetractionClass.lean, line 738. The attribute's comment: “C ∘ (W_∞ → X)_ ∘ i_∞^ = i_∞^: as bivariant classes over W, res(C) ∘ (i_∞, ∘ i_∞^) = Γ_ ∘ i_∞^ in A¹(W_∞ ×_X W → W), on every test scheme W' → W; and as the operation β ↦ C ∩ (W_∞ → X)_ i_∞^* β on A_{k+1}(W ×_X T) for T → X”.

Stacks 0FAR. Let X be locally of finite type over the base of chapter 42, let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, let i_∞ : W_∞ ⟶ W be the fibre at infinity, p : W ⟶ X the projection and C ∈ A⁰(W_∞ ⟶ X) the class of Stacks 0F9J. Then C ∘ (W_∞ ⟶ X)_* ∘ i_∞^* = i_∞^*, in the two readings of the module docstring:

as bivariant classes over W, valid on every test scheme W' ⟶ W: res(C) ∘ (i_{∞,*} ∘ i_∞^*) = Γ_* ∘ i_∞^* in A¹(W_∞ ×_X W ⟶ W), with res the restriction of Stacks 0F9Z along p, i_∞^* the Gysin class of Stacks 0B79, the pushforwards those of Stacks 0EPK along i_∞ and along the graph Γ : W_∞ ⟶ W_∞ ×_X W, and ∘ that of Stacks 0B75;

as the operation of the source on the test schemes W ×_X T, T ⟶ X locally of finite type: for β ∈ A_{k+1}(W ×_X T), C ∩ (W_∞ ×_X T ⟶ T)_*(i_∞^* β) = i_∞^* β in A_k(W_∞ ×_X T), with C ∩ - landing in degree k - 0, identified with k.

theorem gysinAtInfinity_retraction :
    bivariantCompositeOfInvertible C
        (pullback.fst (modificationProjectionAtInfinity f b) (modificationProjection f b) ≫
          (modificationProjectionAtInfinity f b ≫ f))
        (modificationProjection f b ≫ f) (modificationProjection f b ≫ f)
        (pullback.snd (modificationProjectionAtInfinity f b) (modificationProjection f b)) (𝟙 W)
        (pullbackSnd_comp_structureMorphism_eq C (modificationProjectionAtInfinity f b ≫ f) f
          (modificationProjectionAtInfinity f b) rfl (modificationProjection f b))
        (Category.id_comp _) 0 1
        (bivariantRestrictionOfInvertible C (modificationProjectionAtInfinity f b ≫ f) f
          (modificationProjectionAtInfinity f b) rfl (modificationProjection f b) 0
          (gysinAtInfinityClass C f b hA))
        (infinityGysinPushforwardClass C f b) =
      BivariantClass.copy C (gysinSystemOfInvertible C) _ _ (Category.comp_id _).symm _ _
        (zero_add 1).symm (infinityGraphPushforwardClass C f b) ∧
    ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
      (β : chowGroup C (testStr C f (modificationProjection f b) g) (k + 1)),
      (gysinAtInfinityClass C f b hA).cap g k
          (properChowPushforward C (modificationInfinityBaseChangeOver f b g) (g ≫ f)
            (pullback.snd (modificationProjectionAtInfinity f b) g)
            (modificationInfinityBaseChange_snd_over f b g) k
            (properPushforwardDescends C _ _ _ _ _) (infinityGysin C f b g k β)) =
        chowGroupDegreeEquiv C _ (sub_zero k).symm (infinityGysin C f b g k β)

Stacks.Chow.gysinCapOfLift_chowPush_modificationInfinityGysin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/GysinAtInfinityRestriction.lean, line 679. The attribute's comment: “C ∘ (W_∞ ⟶ X)_ ∘ i_∞^ = i_∞^*, on every test scheme T ⟶ X”.

In the situation of Stacks 0F9J, C ∘ (W_∞ ⟶ X)_* ∘ i_∞^* = i_∞^*, on every test scheme g : T ⟶ X: for β ∈ A_{k+1}(W ×_X T), the cap operation of the class C of Stacks 0F9J on the pushforward of i_∞^* β along W_∞ ×_X T ⟶ T is i_∞^* β. The identity of bivariant classes is the case g = 𝟙 X.

theorem gysinCapOfLift_chowPush_modificationInfinityGysin (k : ℤ)
    (β : chowGroup C (modificationBaseChangeOver f b g) (k + 1)) :
    gysinCapAtInfinity C f b hA g k
        (chowPush C (modificationInfinityBaseChangeOver f b g) (g ≫ f)
          (pullback.snd (modificationProjectionAtInfinity f b) g)
          (modificationInfinityBaseChange_snd_over f b g) k
          (modificationInfinityGysin C f b g k β)) =
      modificationInfinityGysin C f b g k β

Tag 0FAS, a lemma

Tag 0FAS in the Stacks Project.

Stacks.Chow.GysinAtInfinity.gysinAtInfinityClass_comp_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinity/Commuting.lean, line 789.

Stacks 0FAS. Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S, let b : W ⟶ 𝐏¹_X be a proper morphism which is an isomorphism over 𝐀¹_X, and let C ∈ A⁰(W_∞ ⟶ X) be the class of Stacks 0F9J. Let fY : Y ⟶ X be a morphism locally of finite type and c ∈ A^p(Y ⟶ X). Then

C ∘ c = c ∘ C in A^p(W_∞ ×_X Y ⟶ X).

Here, as in Remark 0FA2, C ∘ c = res(C) ∘ c with res(C) ∈ A⁰(W_∞ ×_X Y ⟶ Y) the restriction of C along fY (Stacks 0F9Z), and c ∘ C = res(c) ∘ C with res(c) ∈ A^p(Y ×_X W_∞ ⟶ W_∞) the restriction of c along W_∞ ⟶ X; the second composite lives on Y ×_X W_∞ and in degree p + 0, and is read on W_∞ ×_X Y through the canonical isomorphism and in degree 0 + p. The bivariant classes are those of Stacks 0B76, Stacks.Chow.BivariantChowClass, and C is Stacks.Chow.GysinAtInfinity.gysinAtInfinityClass read through the bridge Stacks.Chow.BivariantChowClass.equivBivariantClass.

theorem gysinAtInfinityClass_comp_comm {sY : Y ⟶ C.S} [LocallyOfFiniteType sY]
    (hY : fY ≫ f = sY) (c : BivariantChowClass C sY f fY hY p) :
    ((BivariantChowClass.equivBivariantClass.symm (gysinAtInfinityClass C f b hA)).restrict fY
        hY).comp c =
      (((c.restrict (modificationProjectionAtInfinity f b) rfl).comp
          (BivariantChowClass.equivBivariantClass.symm (gysinAtInfinityClass C f b hA))).degreeCongr
        (add_comm p 0)).transport
        (comp_comp_structureMorphism_eq (BivariantChowClass.restrict_structure_eq rfl fY hY) hY)
        (pullbackSymmetry fY (modificationProjectionAtInfinity f b))
        (pullbackSymmetry_hom_comp_snd_comp (modificationProjectionAtInfinity f b) fY)

Stacks.Chow.gysinAtInfinity_bivariantCommute, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityCommuting.lean, line 206. The attribute's comment: “given the construction of Stacks 0F9J as a presentation of the cap operation of C by a lift and a Gysin step, and the naturality of each of those two factors under c (the first being the source's step that c ∩ β lifts c ∩ α, resting on Stacks 02RC and 02RX; the second being condition (3) of Stacks 0B76 for c at the divisor at infinity, which needs Stacks 0B6Y to instantiate)”.

Stacks 0FAS, conditional on the construction of Stacks 0F9J and its two naturality properties under c.

In the setting of Stacks 0F9J, let fY : Y ⟶ X be locally of finite type and let c ∈ A^p(Y ⟶ X). Then the canonical class C ∈ A⁰(W_∞ ⟶ X) and c commute, in the sense of Remark 0FA2: C ∩ (c ∩ α) = c ∩ (C ∩ α) for every α ∈ CH_k(T) and every test scheme t : T ⟶ X locally of finite type, the two sides being compared by the canonical isomorphism W_∞ ×_X (Y ×_X T) ≅ Y ×_X (W_∞ ×_X T).

The hypotheses are the source's own proof steps, and none of them is the conclusion:

P, a Stacks.Chow.GysinAtInfinityCapPresentation, is the construction of Stacks 0F9J: C ∩ - = i_∞^* ∘ lift. It is needed because the pushforward identity recorded by Stacks.Chow.GysinAtInfinityData does not determine C.

hlift is "c ∩ β is a lift of c ∩ α", a statement about the lift alone.

hgysinStep is condition (3) of Stacks 0B76 for c at the divisor at infinity, a statement about the Gysin step alone; it is Stacks.Chow.BivariantClass.gysin_naturality modulo the zero-scheme base-change identification of Stacks 0B6Y, which this repository lacks.

See the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.GysinAtInfinityCommuting.

theorem gysinAtInfinity_bivariantCommute
    (hlift : ∀ {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
        (α : chowGroup C (t ≫ f) k),
      P.lift (pullback.fst fY t ≫ fY) (k - p)
          (chowGroupCongr C (Category.assoc (pullback.fst fY t) fY f).symm (k - p)
            (c.cap t k α)) =
        chowGroupDegreeEquiv C (modificationBaseChangeOver f b (pullback.fst fY t ≫ fY))
          (by ring : k + 1 - p = k - p + 1)
          (commuteCapTransport C G f fY (modificationProjection f b) p c t (k + 1)
            (P.lift t k α)))
    (hgysinStep : ∀ {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
        (β : chowGroup C (modificationBaseChangeOver f b t) (k + 1)),
      P.gysinStep (pullback.fst fY t ≫ fY) (k - p)
          (chowGroupDegreeEquiv C (modificationBaseChangeOver f b (pullback.fst fY t ≫ fY))
            (by ring : k + 1 - p = k - p + 1)
            (commuteCapTransport C G f fY (modificationProjection f b) p c t (k + 1) β)) =
        commuteCapTransport C G f fY (modificationProjectionAtInfinity f b) p c t k
          (P.gysinStep t k β)) :
    BivariantCommute C G f (modificationProjectionAtInfinity f b) fY 0 p D.bivariantClass c

Stacks.Chow.gysinAtInfinity_commuteCompositeCap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinAtInfinityCommuting.lean, line 255. The attribute's comment: “the displayed equality C ∘ c = c ∘ C of the tag, on cap operations, under the same hypotheses as gysinAtInfinity_bivariantCommute”.

Stacks 0FAS in the displayed form of the tag: C ∘ c = c ∘ C in A^p(W_∞ ×_X Y ⟶ X), read on cap operations.

This is Stacks.Chow.gysinAtInfinity_bivariantCommute pushed through the equivalence of Remark 0FA2, Stacks.Chow.bivariantCommute_iff_commuteCompositeCap_eq: the cap operations of the two composites res(C) ∘ c and res(c) ∘ C agree under the canonical identification W_∞ ×_X Y ≅ Y ×_X W_∞ of their sources and the equality 0 + p = p + 0 of their degrees. The hypothesis hgys is the isomorphism case of Stacks 02TA for the Gysin system, which Stacks.Chow.bivariantRestriction (Stacks 0F9Z) needs in order to be a bivariant class; the Stacks 02S2 hypothesis of Stacks.Chow.bivariantCompositeCap is discharged by Stacks.Chow.properPushforwardDescends.

theorem gysinAtInfinity_commuteCompositeCap_eq (hgys : G.IsNaturalUnderBaseChangeIso)
    (hlift : ∀ {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
        (α : chowGroup C (t ≫ f) k),
      P.lift (pullback.fst fY t ≫ fY) (k - p)
          (chowGroupCongr C (Category.assoc (pullback.fst fY t) fY f).symm (k - p)
            (c.cap t k α)) =
        chowGroupDegreeEquiv C (modificationBaseChangeOver f b (pullback.fst fY t ≫ fY))
          (by ring : k + 1 - p = k - p + 1)
          (commuteCapTransport C G f fY (modificationProjection f b) p c t (k + 1)
            (P.lift t k α)))
    (hgysinStep : ∀ {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
        (β : chowGroup C (modificationBaseChangeOver f b t) (k + 1)),
      P.gysinStep (pullback.fst fY t ≫ fY) (k - p)
          (chowGroupDegreeEquiv C (modificationBaseChangeOver f b (pullback.fst fY t ≫ fY))
            (by ring : k + 1 - p = k - p + 1)
            (commuteCapTransport C G f fY (modificationProjection f b) p c t (k + 1) β)) =
        commuteCapTransport C G f fY (modificationProjectionAtInfinity f b) p c t k
          (P.gysinStep t k β))
    {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
    (α : chowGroup C (t ≫ f) k) :
    chowPushforwardOfIso C
        (pullback.fst (pullback.snd (modificationProjectionAtInfinity f b) fY ≫ fY) t ≫
          (pullback.fst (modificationProjectionAtInfinity f b) fY ≫
            (modificationProjectionAtInfinity f b ≫ f)))
        (pullback.fst (pullback.snd fY (modificationProjectionAtInfinity f b) ≫
            modificationProjectionAtInfinity f b) t ≫
          (pullback.fst fY (modificationProjectionAtInfinity f b) ≫ (fY ≫ f)))
        (compositeComparisonHom (modificationProjectionAtInfinity f b) fY t)
        (compositeComparisonHom_comp_structureMorphism C f
          (modificationProjectionAtInfinity f b) fY t) (k - p - 0)
        (commuteCompositeCap C G f (modificationProjectionAtInfinity f b) fY 0 p
          D.bivariantClass c hgys (properPushforwardDescends C) t k α) =
      chowGroupDegreeEquiv C
        (pullback.fst (pullback.snd fY (modificationProjectionAtInfinity f b) ≫
            modificationProjectionAtInfinity f b) t ≫
          (pullback.fst fY (modificationProjectionAtInfinity f b) ≫ (fY ≫ f)))
        (by ring : k - 0 - p = k - p - 0)
        (commuteCompositeCap C G f fY (modificationProjectionAtInfinity f b) p 0 c
          D.bivariantClass hgys (properPushforwardDescends C) t k α)

Stacks.Chow.nonhomogeneousBivariantTransport_compositeOfInvertible_gysinAtInfinityClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Commutation.lean, line 155. The attribute's comment: “C ∘ c = c ∘ C in A^(W_∞ ×_X Y → X), for every c in A^(Y → X)”.

Let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, let C ∈ A⁰(W_∞ ⟶ X) be the class of Stacks 0F9J, let fY : Y ⟶ X be locally of finite type and let c ∈ A^*(Y ⟶ X). Then

C ∘ c = c ∘ C in A^*(W_∞ ×_X Y ⟶ X),

where C ∘ c = res(C) ∘ c and c ∘ C = res(c) ∘ C, the latter a class for Y ×_X W_∞ ⟶ X carried to W_∞ ×_X Y along the symmetry of the fibre product.

theorem nonhomogeneousBivariantTransport_compositeOfInvertible_gysinAtInfinityClass
    (c : nonhomogeneousBivariantGroup C (gysinSystemOfInvertible C) (fY ≫ f) f fY rfl) :
    nonhomogeneousBivariantTransport C (gysinSystemOfInvertible C)
        (pullback.fst fY (modificationProjectionAtInfinity f b) ≫ (fY ≫ f))
        (pullback.fst (modificationProjectionAtInfinity f b) fY ≫
          (modificationProjectionAtInfinity f b ≫ f)) f
        (pullback.snd fY (modificationProjectionAtInfinity f b) ≫
          modificationProjectionAtInfinity f b)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C (fY ≫ f) f fY rfl _) rfl)
        (pullback.snd (modificationProjectionAtInfinity f b) fY ≫ fY)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C _ f (modificationProjectionAtInfinity f b) rfl
            fY) rfl)
        (pullbackSymmetry fY (modificationProjectionAtInfinity f b))
        (by simp [pullback.condition])
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (nonhomogeneousBivariantCompositeOfInvertible C
          (pullback.fst fY (modificationProjectionAtInfinity f b) ≫ (fY ≫ f))
          (modificationProjectionAtInfinity f b ≫ f) f
          (pullback.snd fY (modificationProjectionAtInfinity f b))
          (modificationProjectionAtInfinity f b)
          (pullbackSnd_comp_structureMorphism_eq C (fY ≫ f) f fY rfl _) rfl
          (nonhomogeneousBivariantRestriction C (gysinSystemOfInvertible C) (fY ≫ f) f fY rfl
            (modificationProjectionAtInfinity f b)
            (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c)
          (DirectSum.of _ 0 (gysinAtInfinityClass C f b hA))) =
      nonhomogeneousBivariantCompositeOfInvertible C
        (pullback.fst (modificationProjectionAtInfinity f b) fY ≫
          (modificationProjectionAtInfinity f b ≫ f)) (fY ≫ f) f
        (pullback.snd (modificationProjectionAtInfinity f b) fY) fY
        (pullbackSnd_comp_structureMorphism_eq C _ f (modificationProjectionAtInfinity f b) rfl
          fY) rfl
        (DirectSum.of _ 0 (bivariantRestriction C (gysinSystemOfInvertible C)
          (modificationProjectionAtInfinity f b ≫ f) f (modificationProjectionAtInfinity f b) rfl
          fY 0 (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
          (gysinAtInfinityClass C f b hA))) c

Sources

LeanStacks.Chow.gysinCapOfLift · Stacks.Chow.gysinCapOfLift_eq_of_gysin_pushforward_eq_zero · Stacks.Chow.GysinAtInfinityData · Stacks.Chow.GysinAtInfinity.gysinAtInfinity · Stacks.Chow.gysinAtInfinityClass · Stacks.Chow.gysinAtInfinityData · Stacks.Chow.gysinCapAtInfinity · Stacks.Chow.gysinCapAtInfinity_eq_of_isModificationLift

Section42.49 Preparation for localized Chern classes #

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

Tag 0F9K, a lemma

Tag 0F9K in the Stacks Project.

Stacks.Chow.GysinAtInfinity.properPushforward_localizedPowerSumClassAtInfinity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedPowerSumAtInfinity.lean, line 310. The attribute's comment: “the classes P'_p: the class P'_p(Q) = (E ⟶ Z)_ ∘ P'_p(Q|_E) ∘ C in A^p(Z ⟶ X), for Q|_T zero, satisfies (Z ⟶ X)_ ∘ P'_p(Q) = P_p(Q|_{X × {0}})”.

Stacks 0F9K, for the classes P'_p. Let X be locally of finite type over the base of chapter 42, let Z ⊆ X be a closed subscheme, let b : W ⟶ 𝐏¹_X be a proper morphism which is an isomorphism over 𝐀¹_X (assumption (A1)), and let Q ∈ D(𝒪_W) be a perfect object whose Chern classes are defined (assumption (A0)). Let T ⊆ W_∞ be a closed subscheme containing all points of W_∞ lying over X \ Z such that Q|_T is zero (assumption (A2)). Then the class P'_p(Q) = (E ⟶ Z)_* ∘ P'_p(Q|_E) ∘ C ∈ A^p(Z ⟶ X) satisfies

(Z ⟶ X)_* ∘ P'_p(Q) = P_p(Q|_{X × {0}})

in A^p(X), where X × {0} is identified with X by the section at zero and (Z ⟶ X)_* ∘ - is the pushforward of Stacks 0EPK.

theorem properPushforward_localizedPowerSumClassAtInfinity
    (hV : ∀ w, (modificationProjectionAtInfinity f b).base w ∉ Set.range jZ.base →
      w ∈ Set.range iV.base)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      iV.toLRSHom.toShHom).obj (restrictionAtInfinity f b Q))) :
    properPushforwardLocalizedPowerSumClassAtInfinity C hA jZ hQ perfect hV hzero =
      powerSumAtZero C f b hA hQ p

Stacks.Chow.modificationPowerSum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Preparation.lean, line 124. The attribute's comment: “the class P'_p(Q) in A^p(Z ⟶ X), for Q|_T zero”.

The class P'_p(Q) of Stacks 0F9K. Let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, let Z ⊆ X be closed, let Q ∈ D(𝒪_W) have defined Chern classes, and let T ⊆ W_∞ be closed, contain every point of W_∞ over X ∖ Z, and be such that Q|_T is zero. The class is (E ⟶ Z)_* ∘ P'_p(Q|_E) ∘ C ∈ A^p(Z ⟶ X), where E = W_∞ ×_X Z, P'_p(Q|_E) is the extension of P_p(Q)|_E along the closed cover W_∞ = T ∪ E, and C is the class of Stacks 0F9J (Stacks.Chow.gysinAtInfinityData).

def modificationPowerSum
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q)) :
    BivariantClass C (gysinSystemOfInvertible C) (z ≫ f) f z rfl p

Stacks.Chow.modificationChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Preparation.lean, line 141. The attribute's comment: “the class c'_p(Q) in A^p(Z ⟶ X), for Q|_T finite locally free of rank < p in degree 0”.

The class c'_p(Q) of Stacks 0F9K. Let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, let Z ⊆ X be closed, let Q ∈ D(𝒪_W) have defined Chern classes, and let T ⊆ W_∞ be closed, contain every point of W_∞ over X ∖ Z, and be such that Q|_T is finite locally free of rank < p in degree 0. The class is (E ⟶ Z)_* ∘ c'_p(Q|_E) ∘ C ∈ A^p(Z ⟶ X), where E = W_∞ ×_X Z, c'_p(Q|_E) is the extension of c_p(Q)|_E along the closed cover W_∞ = T ∪ E, and C is the class of Stacks 0F9J (Stacks.Chow.gysinAtInfinityData).

def modificationChernClass
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hrank : ∃ M : T.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) :
    BivariantClass C (gysinSystemOfInvertible C) (z ≫ f) f z rfl p

Stacks.Chow.properPushforwardChowCohomology_modificationPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Preparation.lean, line 157. The attribute's comment: “the case of P'_p: (Z ⟶ X)_* ∘ P'_p(Q) = P_p(Q|_{X × {0}})”.

In the situation of Stacks.Chow.modificationPowerSum, (Z ⟶ X)_* ∘ P'_p(Q) = P_p(Q|_{X × {0}}) in A^p(X), where (Z ⟶ X)_* ∘ - is the pushforward of Stacks 0EPK and Q|_{X × {0}} is the derived pullback of Q along the section at zero i_0 : X ⟶ W.

theorem properPushforwardChowCohomology_modificationPowerSum
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q)) :
    properPushforwardChowCohomology C f (z ≫ f) z rfl
        (modificationPowerSum C f b hA z t hQ p hT hzero) =
      perfectPowerSumComponent C f (hQ.derivedPullback
        (modificationSectionAtZero f b (isIso_modificationFibreAtZeroProjection f b hA))) p

Stacks.Chow.properPushforwardChowCohomology_modificationChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Preparation.lean, line 181. The attribute's comment: “the case of c'_p: (Z ⟶ X)_* ∘ c'_p(Q) = c_p(Q|_{X × {0}})”.

In the situation of Stacks.Chow.modificationChernClass, (Z ⟶ X)_* ∘ c'_p(Q) = c_p(Q|_{X × {0}}) in A^p(X), where (Z ⟶ X)_* ∘ - is the pushforward of Stacks 0EPK and Q|_{X × {0}} is the derived pullback of Q along the section at zero i_0 : X ⟶ W.

theorem properPushforwardChowCohomology_modificationChernClass
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hrank : ∃ M : T.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) :
    properPushforwardChowCohomology C f (z ≫ f) z rfl
        (modificationChernClass C f b hA z t hQ p hT hrank) =
      perfectChernClass C f (hQ.derivedPullback
        (modificationSectionAtZero f b (isIso_modificationFibreAtZeroProjection f b hA))) p

Declarations registered for the tag:

Stacks.Chow.GysinAtInfinity.properPushforward_localizedChernClassAtInfinity, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedPowerSumAtInfinity.lean, line 421 (StacksFrontier): “the classes c'_p: the class c'_p(Q) = (E ⟶ Z)_ ∘ c'_p(Q|_E) ∘ C in A^p(Z ⟶ X), for Q|_T finite locally free of rank < p in degree 0, satisfies (Z ⟶ X)_ ∘ c'_p(Q) = c_p(Q|_{X × {0}})”.

Tag 0GUI, a lemma

Tag 0GUI in the Stacks Project.

Stacks.Chow.GysinAtInfinity.localizedChernClassAtInfinity_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedClassAtInfinityBaseChange.lean, line 717. The attribute's comment: “the classes c'_p: c'_p(Q') built as in Stacks 0F9K from b', Q' and T' is the restriction of c'_p(Q)”.

Stacks 0GUI, for the Chern classes. In the situation of Stacks 0F9K, with Q|_T finite locally free of rank < p in degree 0, let q : X' ⟶ X be a morphism locally of finite type. Let Z' = Z ×_X X', b' : W' = W ×_{𝐏¹_X} 𝐏¹_{X'} ⟶ 𝐏¹_{X'} and T' = T ×_{W_∞} W'_∞ ⊆ W'_∞ be the base changes of Z, b and T, and let Q' = (W' ⟶ W)^*Q. Then b', Q' and T' satisfy the assumptions of Stacks 0F9K, and the class c'_p(Q') ∈ A^p(Z' ⟶ X') constructed as in Stacks 0F9K using b', Q' and T' is the restriction (Remark 0F9Z) of c'_p(Q) ∈ A^p(Z ⟶ X).

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

theorem localizedChernClassAtInfinity_baseChange
    (hV : ∀ w, (modificationProjectionAtInfinity f b).base w ∉ Set.range jZ.base →
      w ∈ Set.range iV.base)
    (hres : RestrictionIsLocallyFreeOfRankLT f b iV Q p) :
    localizedChernClassAtInfinity C (haveI := hA; isIso_baseChangedModification_chart f b q)
        (pullback.snd jZ q)
        (hasDefinedChernClasses_derivedPullback (pullback.fst b (familyBaseChange f q)) hQ)
        (baseChange_mem_range f b jZ iV q hV)
        (restrictionIsLocallyFreeOfRankLT_baseChange f b iV q hres) =
      bivariantTransport C (gysinSystemOfInvertible C) (pullback.fst jZ q ≫ jZ ≫ f)
        (pullback.snd jZ q ≫ q ≫ f) (q ≫ f) (pullback.snd jZ q)
        (pullbackSnd_comp_structureMorphism_eq C (jZ ≫ f) f jZ rfl q) (pullback.snd jZ q) rfl
        (Iso.refl _) (Category.id_comp _) (p : ℤ)
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (bivariantRestrictionOfInvertible C (jZ ≫ f) f jZ rfl q (p : ℤ)
          (localizedChernClassAtInfinity C hA jZ hQ hV hres))

Stacks.Chow.GysinAtInfinity.localizedPowerSumClassAtInfinity_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedClassAtInfinityBaseChange.lean, line 766. The attribute's comment: “the classes P'_p: P'_p(Q') built as in Stacks 0F9K from b', Q' and T' is the restriction of P'_p(Q)”.

Stacks 0GUI, for the classes P_p. In the situation of Stacks 0F9K, with Q|_T zero, let q : X' ⟶ X be a morphism locally of finite type. Let Z' = Z ×_X X', b' : W' = W ×_{𝐏¹_X} 𝐏¹_{X'} ⟶ 𝐏¹_{X'} and T' = T ×_{W_∞} W'_∞ ⊆ W'_∞ be the base changes of Z, b and T, and let Q' = (W' ⟶ W)^*Q. Then b', Q' and T' satisfy the assumptions of Stacks 0F9K, and the class P'_p(Q') ∈ A^p(Z' ⟶ X') constructed as in Stacks 0F9K using b', Q' and T' is the restriction (Remark 0F9Z) of P'_p(Q) ∈ A^p(Z ⟶ X), read with the structure morphism Z' ⟶ X' ⟶ S as in localizedChernClassAtInfinity_baseChange.

theorem localizedPowerSumClassAtInfinity_baseChange
    (perfect : RingedSpace.IsPerfect.{u, u + 1} (X := W.toRingedSpace) Q)
    (hV : ∀ w, (modificationProjectionAtInfinity f b).base w ∉ Set.range jZ.base →
      w ∈ Set.range iV.base)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      iV.toLRSHom.toShHom).obj (restrictionAtInfinity f b Q))) :
    localizedPowerSumClassAtInfinity C (haveI := hA; isIso_baseChangedModification_chart f b q)
        (pullback.snd jZ q)
        (hasDefinedChernClasses_derivedPullback (pullback.fst b (familyBaseChange f q)) hQ)
        (RingedSpace.KFlatDerivedPullback.isPerfect_derivedPullback _ Q perfect)
        (baseChange_mem_range f b jZ iV q hV) (isZero_restriction_baseChange f b iV q hzero)
        (p := p) =
      bivariantTransport C (gysinSystemOfInvertible C) (pullback.fst jZ q ≫ jZ ≫ f)
        (pullback.snd jZ q ≫ q ≫ f) (q ≫ f) (pullback.snd jZ q)
        (pullbackSnd_comp_structureMorphism_eq C (jZ ≫ f) f jZ rfl q) (pullback.snd jZ q) rfl
        (Iso.refl _) (Category.id_comp _) (p : ℤ)
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (bivariantRestrictionOfInvertible C (jZ ≫ f) f jZ rfl q (p : ℤ)
          (localizedPowerSumClassAtInfinity C hA jZ hQ perfect hV hzero (p := p)))

Stacks.Chow.bivariantRestriction_modificationPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/ModificationBaseChange.lean, line 457. The attribute's comment: “the case of P'_p: the class P'_p(Q') of Lemma 0F9K for the base change is the restriction of P'_p(Q)”.

In the setting of Stacks 0F9K let h : X' ⟶ X be locally of finite type, let b' : W' = W ×_{𝐏¹_X} 𝐏¹_{X'} ⟶ 𝐏¹_{X'} and Z' = Z ×_X X' be the base changes, and set Q' = (W' ⟶ W)^* Q. Then the class P'_p(Q') ∈ A^p(Z' ⟶ X') constructed as in Stacks 0F9K from b', Q' and any closed T' ⊆ W'_∞ with the properties used there (for instance the base change of T) is the restriction (Remark 0F9Z) of P'_p(Q) ∈ A^p(Z ⟶ X).

theorem bivariantRestriction_modificationPowerSum
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hT' : ∀ w, modificationProjectionAtInfinity (h ≫ f) (baseChangedModification f b h) w ∉
      Set.range (pullback.snd z h) → w ∈ Set.range t')
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q))
    (hzero' : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (t' ≫ modificationInclusionAtInfinity (h ≫ f)
        (baseChangedModification f b h)).toLRSHom.toShHom).obj
      ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (pullback.fst b (familyBaseChange f h)).toLRSHom.toShHom).obj Q))) :
    bivariantClassCongrBase C (gysinSystemOfInvertible C) (pullback.snd z h)
        (pullbackSnd_comp_structureMorphism_eq C (z ≫ f) f z rfl h).symm rfl
        (hv := pullbackSnd_comp_structureMorphism_eq C (z ≫ f) f z rfl h) (hv' := rfl) p
        (bivariantRestriction C (gysinSystemOfInvertible C) (z ≫ f) f z rfl h p
          (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
          (modificationPowerSum C f b hA z t hQ p hT hzero)) =
      modificationPowerSum C (h ≫ f) (baseChangedModification f b h)
        (isIso_restrictedModification_affineChart f b h hA) (pullback.snd z h) t'
        (hQ.derivedPullback (pullback.fst b (familyBaseChange f h))) p hT' hzero'

Stacks.Chow.bivariantRestriction_modificationChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/ModificationBaseChange.lean, line 493. The attribute's comment: “the case of c'_p: the class c'_p(Q') of Lemma 0F9K for the base change is the restriction of c'_p(Q)”.

In the setting of Stacks 0F9K let h : X' ⟶ X be locally of finite type, let b' : W' = W ×_{𝐏¹_X} 𝐏¹_{X'} ⟶ 𝐏¹_{X'} and Z' = Z ×_X X' be the base changes, and set Q' = (W' ⟶ W)^* Q. Then the class c'_p(Q') ∈ A^p(Z' ⟶ X') constructed as in Stacks 0F9K from b', Q' and any closed T' ⊆ W'_∞ with the properties used there (for instance the base change of T) is the restriction (Remark 0F9Z) of c'_p(Q) ∈ A^p(Z ⟶ X).

theorem bivariantRestriction_modificationChernClass
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hT' : ∀ w, modificationProjectionAtInfinity (h ≫ f) (baseChangedModification f b h) w ∉
      Set.range (pullback.snd z h) → w ∈ Set.range t')
    (hrank : ∃ M : T.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q ≅
          (DerivedCategory.singleFunctor _ 0).obj M))
    (hrank' : ∃ M : T'.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t' ≫ modificationInclusionAtInfinity (h ≫ f)
          (baseChangedModification f b h)).toLRSHom.toShHom).obj
        ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          (pullback.fst b (familyBaseChange f h)).toLRSHom.toShHom).obj Q) ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) :
    bivariantClassCongrBase C (gysinSystemOfInvertible C) (pullback.snd z h)
        (pullbackSnd_comp_structureMorphism_eq C (z ≫ f) f z rfl h).symm rfl
        (hv := pullbackSnd_comp_structureMorphism_eq C (z ≫ f) f z rfl h) (hv' := rfl) p
        (bivariantRestriction C (gysinSystemOfInvertible C) (z ≫ f) f z rfl h p
          (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
          (modificationChernClass C f b hA z t hQ p hT hrank)) =
      modificationChernClass C (h ≫ f) (baseChangedModification f b h)
        (isIso_restrictedModification_affineChart f b h hA) (pullback.snd z h) t'
        (hQ.derivedPullback (pullback.fst b (familyBaseChange f h))) p hT' hrank'

Tag 0FAU, a lemma

Tag 0FAU in the Stacks Project.

Stacks.Chow.localizedModificationClass_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Modification.lean, line 396. The attribute's comment: “first assertion: P'_p(Q), resp. c'_p(Q), is independent of the closed subscheme T, for a general class q in place of P_p(Q), resp. c_p(Q)”.

The localized class does not depend on T, for a general class. Two closed subschemes T, T' ⊆ W_∞ containing every point of W_∞ over X ∖ Z, over both of which q vanishes, give the same localized class; for q = P_p(Q), resp. q = c_p(Q), this is the independence of P'_p(Q), resp. c'_p(Q), of the choice of T.

theorem localizedModificationClass_eq {T' : Scheme.{u}} (t' : T' ⟶ modificationFibreAtInfinity f b)
    [IsClosedImmersion t']
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hT' : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t')
    (hq : BivariantClass.VanishesOver q (t ≫ modificationInclusionAtInfinity f b))
    (hq' : BivariantClass.VanishesOver q (t' ≫ modificationInclusionAtInfinity f b)) :
    localizedModificationClass D z t hT hq = localizedModificationClass D z t' hT' hq'

Stacks.Chow.modificationPowerSum_eq_of_modification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/ModificationComparison.lean, line 853. The attribute's comment: “second assertion, for P'_p: for g : W' ⟶ W proper with b ∘ g an isomorphism over A^1_X (as when g is one), P'_p(g^*Q) = P'_p(Q)”.

The second assertion of Stacks 0FAU, for P'_p. Let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, let g : W' ⟶ W be proper with b' = b ∘ g an isomorphism over 𝐀¹_X (as it is when g is one, Stacks.Chow.isIso_pullbackSnd_comp_projectiveLineAffineChart), and set Q' = Lg^*Q. Then P'_p(Q') = P'_p(Q) in A^p(Z ⟶ X), the left side built from b', Q' and any closed T' ⊆ W'_∞ with the properties of Stacks 0F9K, the right side from b, Q and T ⊆ W_∞.

theorem modificationPowerSum_eq_of_modification
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hT' : ∀ w, modificationProjectionAtInfinity f b' w ∉ Set.range z → w ∈ Set.range t')
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q))
    (hzero' : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (t' ≫ modificationInclusionAtInfinity f b').toLRSHom.toShHom).obj
        ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g.toLRSHom.toShHom).obj Q))) :
    modificationPowerSum C f b' hA' z t' (hQ.derivedPullback g) p hT' hzero' =
      modificationPowerSum C f b hA z t hQ p hT hzero

Stacks.Chow.modificationChernClass_eq_of_modification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/ModificationComparison.lean, line 880. The attribute's comment: “second assertion, for c'_p: for g : W' ⟶ W proper with b ∘ g an isomorphism over A^1_X (as when g is one), c'_p(g^*Q) = c'_p(Q)”.

The second assertion of Stacks 0FAU, for c'_p. Let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, let g : W' ⟶ W be proper with b' = b ∘ g an isomorphism over 𝐀¹_X (as it is when g is one, Stacks.Chow.isIso_pullbackSnd_comp_projectiveLineAffineChart), and set Q' = Lg^*Q. Then c'_p(Q') = c'_p(Q) in A^p(Z ⟶ X), the left side built from b', Q' and any closed T' ⊆ W'_∞ with the properties of Stacks 0F9K, the right side from b, Q and T ⊆ W_∞.

theorem modificationChernClass_eq_of_modification
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hT' : ∀ w, modificationProjectionAtInfinity f b' w ∉ Set.range z → w ∈ Set.range t')
    (hrank : ∃ M : T.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q ≅
          (DerivedCategory.singleFunctor _ 0).obj M))
    (hrank' : ∃ M : T'.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t' ≫ modificationInclusionAtInfinity f b').toLRSHom.toShHom).obj
          ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g.toLRSHom.toShHom).obj Q) ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) :
    modificationChernClass C f b' hA' z t' (hQ.derivedPullback g) p hT' hrank' =
      modificationChernClass C f b hA z t hQ p hT hrank

Stacks.Chow.GysinAtInfinity.localizedPowerSumAtInfinity_invariance, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedClassAtInfinity/Chern.lean, line 707. The attribute's comment: “the P'_p(Q) half: independence of the choice of the closed subscheme T, and P'_p(Q) = P'_p(Q') for a proper g : W' ⟶ W which is an isomorphism over 𝐀¹_X and Q' = g^*Q”.

Stacks 0FAU, for P'_p(Q). In the situation of Stacks 0F9K — X locally of finite type over S, Z ⊆ X closed, b : W ⟶ 𝐏¹_X proper and an isomorphism over 𝐀¹_X (A1), Q ∈ D(𝒪_W) perfect with Chern classes defined (A0) — the class P'_p(Q) ∈ A^p(Z ⟶ X)

is independent of the choice of the closed subscheme T ⊆ W_∞ containing all points of W_∞ lying over X \ Z with Q|_T = 0 (A2);

is unchanged when b is replaced by b ∘ g and Q by Q' = g^*Q, for g : W' ⟶ W proper and an isomorphism over 𝐀¹_X: T' = g^{-1}(T) satisfies (A2) for b ∘ g and Q', so that P'_p(Q') is defined, and P'_p(Q) = P'_p(Q'), the right side computed with any closed subscheme T' ⊆ W'_∞ satisfying (A2) for b ∘ g and Q'.

theorem localizedPowerSumAtInfinity_invariance
    (perfect : RingedSpace.IsPerfect.{u, u + 1} (X := W.toRingedSpace) Q)
    (hQ : HasDefinedChernClasses Q) (p : ℕ) :
    (∀ {T₁ : Scheme.{u}} (iT₁ : T₁ ⟶ modificationFibreAtInfinity f b) [IsClosedImmersion iT₁]
      (hT₁ : ∀ w : modificationFibreAtInfinity f b,
        (modificationProjectionAtInfinity f b).base w ∉ Set.range iZ.base →
          w ∈ Set.range iT₁.base)
      (hzero₁ : IsZero (restrictToInfinity C f b Q iT₁))
      {T₂ : Scheme.{u}} (iT₂ : T₂ ⟶ modificationFibreAtInfinity f b) [IsClosedImmersion iT₂]
      (hT₂ : ∀ w : modificationFibreAtInfinity f b,
        (modificationProjectionAtInfinity f b).base w ∉ Set.range iZ.base →
          w ∈ Set.range iT₂.base)
      (hzero₂ : IsZero (restrictToInfinity C f b Q iT₂)),
      localizedPowerSumClassAtInfinity (p := p) C hA iZ hQ perfect hT₁ hzero₁ =
        localizedPowerSumClassAtInfinity (p := p) C hA iZ hQ perfect hT₂ hzero₂) ∧
    (∀ {T : Scheme.{u}} (iT : T ⟶ modificationFibreAtInfinity f b) [IsClosedImmersion iT]
      (hT : ∀ w : modificationFibreAtInfinity f b,
        (modificationProjectionAtInfinity f b).base w ∉ Set.range iZ.base → w ∈ Set.range iT.base)
      (hzero : IsZero (restrictToInfinity C f b Q iT))
      {W' : Scheme.{u}} (g : W' ⟶ W) [IsProper g]
      (hg : IsIso (pullback.snd g (chartInclusion f b))),
      ((∀ w : modificationFibreAtInfinity f (g ≫ b),
          (modificationProjectionAtInfinity f (g ≫ b)).base w ∉ Set.range iZ.base →
            w ∈ Set.range (pullback.snd iT (infinityMap f b g)).base) ∧
        IsZero (restrictToInfinity C f (g ≫ b)
          ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g.toLRSHom.toShHom).obj Q)
          (pullback.snd iT (infinityMap f b g)))) ∧
      ∀ {T' : Scheme.{u}} (iT' : T' ⟶ modificationFibreAtInfinity f (g ≫ b))
        [IsClosedImmersion iT']
        (hT' : ∀ w : modificationFibreAtInfinity f (g ≫ b),
          (modificationProjectionAtInfinity f (g ≫ b)).base w ∉ Set.range iZ.base →
            w ∈ Set.range iT'.base)
        (hzero' : IsZero (restrictToInfinity C f (g ≫ b)
          ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g.toLRSHom.toShHom).obj Q)
          iT')),
        haveI := hA
        haveI := hg
        localizedPowerSumClassAtInfinity (p := p) C (isIso_pullbackSnd_comp f b g) iZ
            (hasDefinedChernClasses_derivedPullback g hQ)
            (RingedSpace.KFlatDerivedPullback.isPerfect_derivedPullback g.toLRSHom.toShHom Q
              perfect)
            hT' hzero' =
          localizedPowerSumClassAtInfinity (p := p) C hA iZ hQ perfect hT hzero)

Stacks.Chow.GysinAtInfinity.localizedChernClassAtInfinity_invariance, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedClassAtInfinity/Chern.lean, line 772. The attribute's comment: “the c'_p(Q) half: independence of the choice of the closed subscheme T, and c'_p(Q) = c'_p(Q') for a proper g : W' ⟶ W which is an isomorphism over 𝐀¹_X and Q' = g^*Q”.

Stacks 0FAU, for c'_p(Q). In the situation of Stacks 0F9K — X locally of finite type over S, Z ⊆ X closed, b : W ⟶ 𝐏¹_X proper and an isomorphism over 𝐀¹_X (A1), Q ∈ D(𝒪_W) perfect with Chern classes defined (A0) — the class c'_p(Q) ∈ A^p(Z ⟶ X)

is independent of the choice of the closed subscheme T ⊆ W_∞ containing all points of W_∞ lying over X \ Z with Q|_T isomorphic to a finite locally free 𝒪_T-module of rank < p in degree 0 (A2);

is unchanged when b is replaced by b ∘ g and Q by Q' = g^*Q, for g : W' ⟶ W proper and an isomorphism over 𝐀¹_X: T' = g^{-1}(T) satisfies (A2) for b ∘ g and Q', so that c'_p(Q') is defined, and c'_p(Q) = c'_p(Q'), the right side computed with any closed subscheme T' ⊆ W'_∞ satisfying (A2) for b ∘ g and Q'.

Perfectness of Q is a hypothesis of the source; the construction of c'_p(Q) does not use it.

theorem localizedChernClassAtInfinity_invariance
    (_perfect : RingedSpace.IsPerfect.{u, u + 1} (X := W.toRingedSpace) Q)
    (hQ : HasDefinedChernClasses Q) (p : ℕ) :
    (∀ {T₁ : Scheme.{u}} (iT₁ : T₁ ⟶ modificationFibreAtInfinity f b) [IsClosedImmersion iT₁]
      (hT₁ : ∀ w : modificationFibreAtInfinity f b,
        (modificationProjectionAtInfinity f b).base w ∉ Set.range iZ.base →
          w ∈ Set.range iT₁.base)
      (hsmall₁ : RestrictionIsLocallyFreeOfRankLT f b iT₁ Q p)
      {T₂ : Scheme.{u}} (iT₂ : T₂ ⟶ modificationFibreAtInfinity f b) [IsClosedImmersion iT₂]
      (hT₂ : ∀ w : modificationFibreAtInfinity f b,
        (modificationProjectionAtInfinity f b).base w ∉ Set.range iZ.base →
          w ∈ Set.range iT₂.base)
      (hsmall₂ : RestrictionIsLocallyFreeOfRankLT f b iT₂ Q p),
      localizedChernClassAtInfinity C hA iZ hQ hT₁ hsmall₁ =
        localizedChernClassAtInfinity C hA iZ hQ hT₂ hsmall₂) ∧
    (∀ {T : Scheme.{u}} (iT : T ⟶ modificationFibreAtInfinity f b) [IsClosedImmersion iT]
      (hT : ∀ w : modificationFibreAtInfinity f b,
        (modificationProjectionAtInfinity f b).base w ∉ Set.range iZ.base → w ∈ Set.range iT.base)
      (hsmall : RestrictionIsLocallyFreeOfRankLT f b iT Q p)
      {W' : Scheme.{u}} (g : W' ⟶ W) [IsProper g]
      (hg : IsIso (pullback.snd g (chartInclusion f b))),
      ((∀ w : modificationFibreAtInfinity f (g ≫ b),
          (modificationProjectionAtInfinity f (g ≫ b)).base w ∉ Set.range iZ.base →
            w ∈ Set.range (pullback.snd iT (infinityMap f b g)).base) ∧
        RestrictionIsLocallyFreeOfRankLT f (g ≫ b) (pullback.snd iT (infinityMap f b g))
          ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g.toLRSHom.toShHom).obj Q)
          p) ∧
      ∀ {T' : Scheme.{u}} (iT' : T' ⟶ modificationFibreAtInfinity f (g ≫ b))
        [IsClosedImmersion iT']
        (hT' : ∀ w : modificationFibreAtInfinity f (g ≫ b),
          (modificationProjectionAtInfinity f (g ≫ b)).base w ∉ Set.range iZ.base →
            w ∈ Set.range iT'.base)
        (hsmall' : RestrictionIsLocallyFreeOfRankLT f (g ≫ b) iT'
          ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g.toLRSHom.toShHom).obj Q)
          p),
        haveI := hA
        haveI := hg
        localizedChernClassAtInfinity C (isIso_pullbackSnd_comp f b g) iZ
            (hasDefinedChernClasses_derivedPullback g hQ) hT' hsmall' =
          localizedChernClassAtInfinity C hA iZ hQ hT hsmall)

Tag 0FAV, a lemma

Tag 0FAV in the Stacks Project.

Stacks.Chow.GysinAtInfinity.gysinAtInfinity_comp_localizedChernClassAtInfinity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BabyLocalizedChern/LocalizedChernGysinCommute.lean, line 516.

Stacks 0FAV. Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S, let Z ⊆ X be a closed subscheme, let b : W ⟶ 𝐏¹_X be a proper morphism which is an isomorphism over 𝐀¹_X (assumption (A1)), and let Q ∈ D(𝒪_W) be a perfect object whose Chern classes are defined (assumption (A0)). Let T ⊆ W_∞ be a closed subscheme containing all points of W_∞ lying over X \ Z such that Q|_T is isomorphic to a finite locally free 𝒪_T-module of rank < p sitting in cohomological degree 0 (assumption (A2), in the case of the lemma). Let C ∈ A⁰(W_∞ ⟶ X) be the class of Stacks 0F9J and c'_p(Q) ∈ A^p(Z ⟶ X) the class of Stacks 0F9K. Then

C ∘ c_p(Q|_{X × {0}}) = C ∘ (Z ⟶ X)_* ∘ c'_p(Q) = c_p(Q|_{W_∞}) ∘ C

in A^p(W_∞ ⟶ X). Here X × {0} is identified with X by the section at zero, the classes c_p are those of Stacks 0GUD, the composites are those of Stacks 0B75 read at W_∞ ⟶ X in degree 0 + p, and (Z ⟶ X)_* ∘ c'_p(Q) ∈ A^p(X) is the pushforward of Stacks 0EPK.

theorem gysinAtInfinity_comp_localizedChernClassAtInfinity
    (hA : IsIso (pullback.snd b (projectiveLineAffineChart f)))
    (jZ : Z ⟶ X) [IsClosedImmersion jZ]
    (iV : V ⟶ modificationFibreAtInfinity f b) [IsClosedImmersion iV]
    (hV : ∀ w, (modificationProjectionAtInfinity f b).base w ∉ Set.range jZ.base →
      w ∈ Set.range iV.base)
    {Q : DerivedCategory W.Modules}
    (_perfect : RingedSpace.IsPerfect.{u, u + 1} (X := W.toRingedSpace) Q)
    (hQ : HasDefinedChernClasses Q) (p : ℕ)
    (hres : RestrictionIsLocallyFreeOfRankLT f b iV Q p) :
    bivariantCompositeIdRightHom C (gysinSystemOfInvertible C) f
        (modificationProjectionAtInfinity f b)
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (gysinSystemOfInvertible_isNaturalUnderPullbackCompPushforward C) (p : ℤ) 0
        (gysinAtInfinityClass C f b hA) (chernClassAtZero C f b hA hQ p) =
      bivariantCompositeIdRightHom C (gysinSystemOfInvertible C) f
        (modificationProjectionAtInfinity f b)
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (gysinSystemOfInvertible_isNaturalUnderPullbackCompPushforward C) (p : ℤ) 0
        (gysinAtInfinityClass C f b hA)
        (properPushforwardLocalizedChernClassAtInfinity C hA jZ hQ hV hres) ∧
    bivariantCompositeIdRightHom C (gysinSystemOfInvertible C) f
        (modificationProjectionAtInfinity f b)
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (gysinSystemOfInvertible_isNaturalUnderPullbackCompPushforward C) (p : ℤ) 0
        (gysinAtInfinityClass C f b hA)
        (properPushforwardLocalizedChernClassAtInfinity C hA jZ hQ hV hres) =
      bivariantCompositeIdLeftHom C (gysinSystemOfInvertible C) f
        (modificationProjectionAtInfinity f b)
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (gysinSystemOfInvertible_isNaturalUnderPullbackCompPushforward C) (p : ℤ) 0
        (gysinAtInfinityClass C f b hA) (chernClassAtInfinity C f b hQ p)

Stacks.Chow.gysinAtInfinityClass_comp_modificationChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/GysinAtInfinityRestriction.lean, line 547. The attribute's comment: “C ∘ c_p(Q|_{X × {0}}) = C ∘ (Z ⟶ X)_* ∘ c'_p(Q) = c_p(Q|_{W_∞}) ∘ C, for Q|_T finite locally free of rank < p in degree 0, the composites read in A^p(W_∞ ⟶ X)”.

In the situation of Stacks 0F9K, let Q|_T be finite locally free of rank < p in degree 0, and let C ∈ A⁰(W_∞ ⟶ X) be the class of Stacks 0F9J (Stacks.Chow.gysinAtInfinityClass). Then

C ∘ c_p(Q|_{X × {0}}) = C ∘ (Z ⟶ X)_* ∘ c'_p(Q) = c_p(Q|_{W_∞}) ∘ C in A^p(W_∞ ⟶ X),

where c'_p(Q) is Stacks.Chow.modificationChernClass, Q|_{X × {0}} and Q|_{W_∞} are the derived pullbacks of Q along the section at zero and the inclusion of the fibre at infinity, and ∘ is the composition of Stacks 0B75. The composites, of degrees 0 + p and p + 0 for W_∞ ⟶ X ⟶ X and W_∞ ⟶ W_∞ ⟶ X, are read as classes of degree p for W_∞ ⟶ X.

theorem gysinAtInfinityClass_comp_modificationChernClass
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hrank : ∃ M : T.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) :
    BivariantClass.copy C (gysinSystemOfInvertible C) (modificationProjectionAtInfinity f b ≫ f) f
        (Category.comp_id (modificationProjectionAtInfinity f b))
        (comp_comp_structureMorphism_eq rfl (Category.id_comp f)) rfl (zero_add (p : ℤ))
        (bivariantCompositeOfInvertible C (modificationProjectionAtInfinity f b ≫ f) f f
          (modificationProjectionAtInfinity f b) (𝟙 X) rfl (Category.id_comp f) 0 p
          (gysinAtInfinityClass C f b hA)
          (perfectChernClass C f (hQ.derivedPullback
            (modificationSectionAtZero f b (isIso_modificationFibreAtZeroProjection f b hA))) p)) =
      BivariantClass.copy C (gysinSystemOfInvertible C) (modificationProjectionAtInfinity f b ≫ f)
        f (Category.comp_id (modificationProjectionAtInfinity f b))
        (comp_comp_structureMorphism_eq rfl (Category.id_comp f)) rfl (zero_add (p : ℤ))
        (bivariantCompositeOfInvertible C (modificationProjectionAtInfinity f b ≫ f) f f
          (modificationProjectionAtInfinity f b) (𝟙 X) rfl (Category.id_comp f) 0 p
          (gysinAtInfinityClass C f b hA)
          (properPushforwardChowCohomology C f (z ≫ f) z rfl
            (modificationChernClass C f b hA z t hQ p hT hrank))) ∧
    BivariantClass.copy C (gysinSystemOfInvertible C) (modificationProjectionAtInfinity f b ≫ f) f
        (Category.comp_id (modificationProjectionAtInfinity f b))
        (comp_comp_structureMorphism_eq rfl (Category.id_comp f)) rfl (zero_add (p : ℤ))
        (bivariantCompositeOfInvertible C (modificationProjectionAtInfinity f b ≫ f) f f
          (modificationProjectionAtInfinity f b) (𝟙 X) rfl (Category.id_comp f) 0 p
          (gysinAtInfinityClass C f b hA)
          (properPushforwardChowCohomology C f (z ≫ f) z rfl
            (modificationChernClass C f b hA z t hQ p hT hrank))) =
      BivariantClass.copy C (gysinSystemOfInvertible C)
        (modificationProjectionAtInfinity f b ≫ f) f
        (Category.id_comp (modificationProjectionAtInfinity f b))
        (comp_comp_structureMorphism_eq (Category.id_comp _) rfl) rfl (add_zero (p : ℤ))
        (bivariantCompositeOfInvertible C (modificationProjectionAtInfinity f b ≫ f)
          (modificationProjectionAtInfinity f b ≫ f) f (𝟙 _)
          (modificationProjectionAtInfinity f b) (Category.id_comp _) rfl p 0
          (perfectChernClass C (modificationProjectionAtInfinity f b ≫ f)
            (hQ.derivedPullback (modificationInclusionAtInfinity f b)) p)
          (gysinAtInfinityClass C f b hA))

Tag 0FAW, a lemma

Tag 0FAW in the Stacks Project.

Stacks.Chow.nonhomogeneousBivariantTransport_compositeOfInvertible_modificationPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Commutation.lean, line 379. The attribute's comment: “for P'_p: P'_p(Q) ∘ c = c ∘ P'_p(Q) in A^(Y ×_X Z → X), for every c in A^(Y → X)”.

In the situation of Stacks 0F9K with Q|_T zero, let g : Y ⟶ X be locally of finite type and let c ∈ A^*(Y ⟶ X). Then

P'_p(Q) ∘ c = c ∘ P'_p(Q) in A^*(Y ×_X Z ⟶ X),

where P'_p(Q) ∘ c = res(P'_p(Q)) ∘ c is a class for Z ×_X Y ⟶ X, carried to Y ×_X Z along the symmetry of the fibre product, and c ∘ P'_p(Q) = res(c) ∘ P'_p(Q).

theorem nonhomogeneousBivariantTransport_compositeOfInvertible_modificationPowerSum
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q))
    (c : nonhomogeneousBivariantGroup C (gysinSystemOfInvertible C) (g ≫ f) f g rfl) :
    nonhomogeneousBivariantTransport C (gysinSystemOfInvertible C) (pullback.fst z g ≫ (z ≫ f))
        (pullback.fst g z ≫ (g ≫ f)) f (pullback.snd z g ≫ g)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C (z ≫ f) f z rfl g) rfl)
        (pullback.snd g z ≫ z)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C (g ≫ f) f g rfl z) rfl)
        (pullbackSymmetry z g) (by simp [pullback.condition])
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (nonhomogeneousBivariantCompositeOfInvertible C (pullback.fst z g ≫ (z ≫ f)) (g ≫ f) f
          (pullback.snd z g) g
          (pullbackSnd_comp_structureMorphism_eq C (z ≫ f) f z rfl g) rfl
          (DirectSum.of _ (p : ℤ)
            (bivariantRestriction C (gysinSystemOfInvertible C) (z ≫ f) f z rfl g p
              (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
              (modificationPowerSum C f b hA z t hQ p hT hzero))) c) =
      nonhomogeneousBivariantCompositeOfInvertible C (pullback.fst g z ≫ (g ≫ f)) (z ≫ f) f
        (pullback.snd g z) z
        (pullbackSnd_comp_structureMorphism_eq C (g ≫ f) f g rfl z) rfl
        (nonhomogeneousBivariantRestriction C (gysinSystemOfInvertible C) (g ≫ f) f g rfl z
          (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c)
        (DirectSum.of _ (p : ℤ) (modificationPowerSum C f b hA z t hQ p hT hzero))

Stacks.Chow.nonhomogeneousBivariantTransport_compositeOfInvertible_modificationChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Commutation.lean, line 422. The attribute's comment: “for c'_p: c'_p(Q) ∘ c = c ∘ c'_p(Q) in A^(Y ×_X Z → X), for every c in A^(Y → X)”.

In the situation of Stacks 0F9K with Q|_T finite locally free of rank < p in degree 0, let g : Y ⟶ X be locally of finite type and let c ∈ A^*(Y ⟶ X). Then

c'_p(Q) ∘ c = c ∘ c'_p(Q) in A^*(Y ×_X Z ⟶ X),

where c'_p(Q) ∘ c = res(c'_p(Q)) ∘ c is a class for Z ×_X Y ⟶ X, carried to Y ×_X Z along the symmetry of the fibre product, and c ∘ c'_p(Q) = res(c) ∘ c'_p(Q).

theorem nonhomogeneousBivariantTransport_compositeOfInvertible_modificationChernClass
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hrank : ∃ M : T.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q ≅
          (DerivedCategory.singleFunctor _ 0).obj M))
    (c : nonhomogeneousBivariantGroup C (gysinSystemOfInvertible C) (g ≫ f) f g rfl) :
    nonhomogeneousBivariantTransport C (gysinSystemOfInvertible C) (pullback.fst z g ≫ (z ≫ f))
        (pullback.fst g z ≫ (g ≫ f)) f (pullback.snd z g ≫ g)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C (z ≫ f) f z rfl g) rfl)
        (pullback.snd g z ≫ z)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C (g ≫ f) f g rfl z) rfl)
        (pullbackSymmetry z g) (by simp [pullback.condition])
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
        (nonhomogeneousBivariantCompositeOfInvertible C (pullback.fst z g ≫ (z ≫ f)) (g ≫ f) f
          (pullback.snd z g) g
          (pullbackSnd_comp_structureMorphism_eq C (z ≫ f) f z rfl g) rfl
          (DirectSum.of _ (p : ℤ)
            (bivariantRestriction C (gysinSystemOfInvertible C) (z ≫ f) f z rfl g p
              (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
              (modificationChernClass C f b hA z t hQ p hT hrank))) c) =
      nonhomogeneousBivariantCompositeOfInvertible C (pullback.fst g z ≫ (g ≫ f)) (z ≫ f) f
        (pullback.snd g z) z
        (pullbackSnd_comp_structureMorphism_eq C (g ≫ f) f g rfl z) rfl
        (nonhomogeneousBivariantRestriction C (gysinSystemOfInvertible C) (g ≫ f) f g rfl z
          (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c)
        (DirectSum.of _ (p : ℤ) (modificationChernClass C f b hA z t hQ p hT hrank))

Stacks.Chow.GysinAtInfinity.localizedPowerSumAtInfinity_comp_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedClassAtInfinity/Commuting.lean, line 333. The attribute's comment: “the classes P'_p: P'_p(Q) ∘ c = c ∘ P'_p(Q) for every bivariant class c”.

Stacks 0FAW, for the classes P'_p. Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S, let Z ⊆ X be a closed subscheme, let b : W ⟶ 𝐏¹_X be a proper morphism which is an isomorphism over 𝐀¹_X (A1), let Q ∈ D(𝒪_W) be perfect with defined Chern classes (A0), and let T ⊆ W_∞ be a closed subscheme containing all points of W_∞ lying over X \ Z with Q|_T zero (A2). Let fY : Y ⟶ X be locally of finite type and c ∈ A^r(Y ⟶ X). Then

P'_p(Q) ∘ c = c ∘ P'_p(Q) in A^{p+r}(Y ×_X Z ⟶ X),

where P'_p(Q) ∈ A^p(Z ⟶ X) is the class of Stacks 0F9K. As in Remark 0FA2 (and Stacks 0FAS), P'_p(Q) ∘ c = res(P'_p(Q)) ∘ c with res(P'_p(Q)) ∈ A^p(Z ×_X Y ⟶ Y) the restriction along fY (Remark 0F9Z), and c ∘ P'_p(Q) = res(c) ∘ P'_p(Q) with res(c) ∈ A^r(Y ×_X Z ⟶ Z); the second composite is read on Z ×_X Y through the canonical isomorphism and in degree p + r. The bivariant classes are those of Stacks 0B76, Stacks.Chow.BivariantChowClass.

theorem localizedPowerSumAtInfinity_comp_comm
    (perfect : RingedSpace.IsPerfect.{u, u + 1} (X := W.toRingedSpace) Q)
    (hQ : HasDefinedChernClasses Q)
    (hT : ∀ w : modificationFibreAtInfinity f b,
      (modificationProjectionAtInfinity f b).base w ∉ Set.range iZ.base → w ∈ Set.range iT.base)
    (p : ℕ) (hzero : IsZero (restrictToInfinity C f b Q iT)) {r : ℤ} {sY : Y ⟶ C.S}
    [LocallyOfFiniteType sY] (hY : fY ≫ f = sY) (c : BivariantChowClass C sY f fY hY r) :
    ((BivariantChowClass.equivBivariantClass.symm
        (localizedPowerSumClassAtInfinity (p := p) C hA iZ hQ perfect hT
          hzero)).restrict fY hY).comp c =
      (((c.restrict iZ rfl).comp (BivariantChowClass.equivBivariantClass.symm
          (localizedPowerSumClassAtInfinity (p := p) C hA iZ hQ perfect hT hzero))).degreeCongr
        (add_comm r (p : ℤ))).transport
        (comp_comp_structureMorphism_eq (BivariantChowClass.restrict_structure_eq rfl fY hY) hY)
        (pullbackSymmetry fY iZ) (pullbackSymmetry_hom_comp_snd_comp iZ fY)

Stacks.Chow.GysinAtInfinity.localizedChernClassAtInfinity_comp_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedClassAtInfinity/Commuting.lean, line 366. The attribute's comment: “the classes c'_p: c'_p(Q) ∘ c = c ∘ c'_p(Q) for every bivariant class c”.

Stacks 0FAW, for the classes c'_p. Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S, let Z ⊆ X be a closed subscheme, let b : W ⟶ 𝐏¹_X be a proper morphism which is an isomorphism over 𝐀¹_X (A1), let Q ∈ D(𝒪_W) be perfect with defined Chern classes (A0), and let T ⊆ W_∞ be a closed subscheme containing all points of W_∞ lying over X \ Z with Q|_T isomorphic to a finite locally free 𝒪_T-module of rank < p sitting in cohomological degree 0 (A2). Let fY : Y ⟶ X be locally of finite type and c ∈ A^r(Y ⟶ X). Then

c'_p(Q) ∘ c = c ∘ c'_p(Q) in A^{p+r}(Y ×_X Z ⟶ X),

where c'_p(Q) ∈ A^p(Z ⟶ X) is the class of Stacks 0F9K, the composites being read as in Stacks.Chow.GysinAtInfinity.localizedPowerSumAtInfinity_comp_comm.

theorem localizedChernClassAtInfinity_comp_comm
    (_perfect : RingedSpace.IsPerfect.{u, u + 1} (X := W.toRingedSpace) Q)
    (hQ : HasDefinedChernClasses Q)
    (hT : ∀ w : modificationFibreAtInfinity f b,
      (modificationProjectionAtInfinity f b).base w ∉ Set.range iZ.base → w ∈ Set.range iT.base)
    (p : ℕ)
    (hsmall : RestrictionIsLocallyFreeOfRankLT f b iT Q p)
    {r : ℤ} {sY : Y ⟶ C.S} [LocallyOfFiniteType sY] (hY : fY ≫ f = sY)
    (c : BivariantChowClass C sY f fY hY r) :
    ((BivariantChowClass.equivBivariantClass.symm
        (localizedChernClassAtInfinity C hA iZ hQ hT hsmall)).restrict fY hY).comp c =
      (((c.restrict iZ rfl).comp (BivariantChowClass.equivBivariantClass.symm
          (localizedChernClassAtInfinity C hA iZ hQ hT hsmall))).degreeCongr
        (add_comm r (p : ℤ))).transport
        (comp_comp_structureMorphism_eq (BivariantChowClass.restrict_structure_eq rfl fY hY) hY)
        (pullbackSymmetry fY iZ) (pullbackSymmetry_hom_comp_snd_comp iZ fY)

Tag 0FAX, a lemma

Tag 0FAX in the Stacks Project.

Stacks.Chow.modificationPowerSum_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/PreparationNewton.lean, line 123. 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 0F9K, assume that Q|_T is zero, so that c'_p(Q) is defined for every p ≥ 1. Then the classes P'_p(Q) ∈ A^p(Z ⟶ X) are Newton's polynomials in the classes c'_i(Q), with the multiplication of Stacks 0FA0 ((c, c') ↦ res(c) ∘ c', Stacks.Chow.supportedMul):

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

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

theorem modificationPowerSum_succ (q : ℕ) :
    modificationPowerSum C f b hA z t hQ (q + 1) hT hzero =
      ∑ j ∈ (Finset.range q).attach, ((-1 : ℤ) ^ (j : ℕ)) •
          bivariantClassDegreeCongr C _ (z ≫ f) f z rfl
            (newton_degree_eq (Finset.mem_range.mp j.2))
            (supportedMul C (z ≫ f) f z rfl
              (modificationChernClassOfIsZero C f b hA z t hQ hT hzero ((j : ℕ) + 1)
                (Nat.succ_pos _))
              (modificationPowerSum C f b hA z t hQ (q - j) hT hzero)) +
        ((-1 : ℤ) ^ q * ((q : ℤ) + 1)) •
          modificationChernClassOfIsZero C f b hA z t hQ hT hzero (q + 1) (Nat.succ_pos _)

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

In the situation of Stacks 0F9K, with Q|_T zero,

P'_1 = c'_1,

P'_2 = c'_1² - 2c'_2,

P'_3 = c'_1³ - 3c'_1c'_2 + 3c'_3,

P'_4 = c'_1⁴ - 4c'_1²c'_2 + 4c'_1c'_3 + 2c'_2² - 4c'_4

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

theorem modificationPowerSum_first_four :
    let c := fun i (hi : 0 < i) =>
      modificationChernClassOfIsZero C f b hA z t hQ hT hzero i hi
    let m := fun {a b : ℤ} (x : BivariantClass C (gysinSystemOfInvertible C) (z ≫ f) f z rfl a)
      (y : BivariantClass C (gysinSystemOfInvertible C) (z ≫ f) f z rfl b) =>
        supportedMul C (z ≫ f) f z rfl x y
    let P := fun q => modificationPowerSum C f b hA z t hQ q hT hzero
    let d := fun {a b : ℤ} (h : a = b) =>
      bivariantClassDegreeCongr C (gysinSystemOfInvertible C) (z ≫ f) f z 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 0FAY, a lemma

Tag 0FAY in the Stacks Project.

Stacks.Chow.modificationTotalChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/PreparationWhitney.lean, line 220. The attribute's comment: “the class c^(p)(Q) in A^(p)(Z → X)”.

The class c^{(p)}(Q) ∈ A^{(p)}(Z ⟶ X) of Stacks 0FAY. In the situation of Stacks 0F9K (Stacks.Chow.modificationChernClass), with Q|_T isomorphic to a finite locally free module of rank < p placed in degree 0,

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

its component in a degree 0 ≤ i < p is c_i(Q|_{X × {0}}) ∈ A^i(X), with Q|_{X × {0}} the derived pullback along the section at zero, in a negative degree it is 0, and in a degree i ≥ p it is the class c'_i(Q) ∈ A^i(Z ⟶ X) of Stacks 0F9K, which is defined since a rank < p is a rank < i.

def modificationTotalChernClass (p : ℕ)
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hrank : ∃ M : T.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) :
    localizedBivariantGrading C (gysinSystemOfInvertible C) (z ≫ f) f z rfl p

Stacks.Chow.modificationTotalChernClass_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/PreparationWhitney.lean, line 304. The attribute's comment: “c^(p+p')(Q ⊕ Q') = c^(p)(Q) c^(p')(Q') in A^(p+p')(Z → X), with the multiplication of 0FA0”.

In the situation of Stacks 0F9K, let Q, Q' ∈ D(𝒪_W) have defined Chern classes, with Q|_T and Q'|_T isomorphic to finite locally free modules of ranks < p and < p' placed in degree 0. Then

c^{(p+p')}(Q ⊕ Q') = c^{(p)}(Q) c^{(p')}(Q') in A^{(p+p')}(Z ⟶ X),

with the classes of Stacks.Chow.modificationTotalChernClass and the multiplication of Stacks 0FA0 (Stacks.Chow.localizedGradingMul). The hypothesis on (Q ⊕ Q')|_T, under which c^{(p+p')}(Q ⊕ Q') is defined, follows from those on Q|_T and Q'|_T (Stacks.Chow.exists_isFiniteLocallyFreeOfRankLT_derivedPullback_biprod), and so does the definedness of the Chern classes of Q ⊕ Q' (Stacks.Chow.hasDefinedChernClasses_biprod). Perfectness of Q, Q' is not used, only that their Chern classes are defined.

theorem modificationTotalChernClass_biprod
    (hrank : ∃ M : T.Modules, IsFiniteLocallyFreeOfRankLT M p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q ≅
          (DerivedCategory.singleFunctor _ 0).obj M))
    (hrank' : ∃ M : T.Modules, IsFiniteLocallyFreeOfRankLT M p' ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q' ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) :
    modificationTotalChernClass C f b hA z t (hasDefinedChernClasses_biprod hQ hQ') (p + p') hT
        (exists_isFiniteLocallyFreeOfRankLT_derivedPullback_biprod _ hrank hrank') =
      localizedGradingMul C (z ≫ f) f z rfl
        (modificationTotalChernClass C f b hA z t hQ p hT hrank)
        (modificationTotalChernClass C f b hA z t hQ' p' hT hrank')

Tag 0FAZ, a lemma

Tag 0FAZ in the Stacks Project.

Stacks.Chow.modificationPowerSum_biprod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/PreparationSum.lean, line 66.

Stacks 0FAZ. In the situation of Stacks 0F9K, let Q, Q' ∈ D(𝒪_W) have defined Chern classes, and let T ⊆ W_∞ be closed, contain every point of W_∞ lying over X ∖ Z, and be such that Q|_T and Q'|_T are zero. Then the classes P'_p(Q), P'_p(Q'), P'_p(Q ⊕ Q') of A^p(Z ⟶ X) constructed in Stacks 0F9K (Stacks.Chow.modificationPowerSum) satisfy P'_p(Q ⊕ Q') = P'_p(Q) + P'_p(Q').

theorem modificationPowerSum_biprod (hQ : HasDefinedChernClasses Q)
    (hQ' : HasDefinedChernClasses Q') (p : ℕ)
    (hT : ∀ w, modificationProjectionAtInfinity f b w ∉ Set.range z → w ∈ Set.range t)
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q))
    (hzero' : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (t ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj Q')) :
    modificationPowerSum C f b hA z t (hasDefinedChernClasses_biprod hQ hQ') p hT
        (isZero_derivedPullback_biprod _ hzero hzero') =
      modificationPowerSum C f b hA z t hQ p hT hzero +
        modificationPowerSum C f b hA z t hQ' p hT hzero'

Sources

LeanStacks.Chow.GysinAtInfinity.properPushforward_localizedPowerSumClassAtInfinity · Stacks.Chow.modificationPowerSum · Stacks.Chow.modificationChernClass · Stacks.Chow.properPushforwardChowCohomology_modificationPowerSum · Stacks.Chow.properPushforwardChowCohomology_modificationChernClass · Stacks.Chow.GysinAtInfinity.properPushforward_localizedChernClassAtInfinity · Stacks.Chow.GysinAtInfinity.localizedChernClassAtInfinity_baseChange · Stacks.Chow.GysinAtInfinity.localizedPowerSumClassAtInfinity_baseChange

Section42.50 Localized Chern classes #

Section 42.50 of the Stacks Project, Tag 0FB0. 9 tags here are carried by 24 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GUJ, a situation

Tag 0GUJ in the Stacks Project.

Stacks.Chow.LocalizedSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedChernData.lean, line 95.

The standing situation for the localized Chern classes and localized Chern character components of chapter 42 of the Stacks Project: a scheme locally of finite type over the base, a closed subscheme, a perfect object of the derived category of the ambient scheme which away from the closed subscheme is zero or a finite locally free module of rank below the chosen degree (the data Stacks.Chow.LocalizedChernData), and one of the four finiteness alternatives of the source.

structure LocalizedSituation extends LocalizedChernData.{u}

Stacks.Chow.LocalizedChernSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedChernSetup.lean, line 154.

The standing situation for the localized Chern classes and localized Chern character components of chapter 42 of the Stacks Project: a scheme locally of finite type over the base, a closed subscheme, a perfect object of the derived category of the ambient scheme which away from the closed subscheme is zero or a finite locally free module of rank below the chosen degree, and one of four finiteness alternatives.

structure LocalizedChernSituation

Tag 0FB2, a lemma

Tag 0FB2 in the Stacks Project.

Stacks.Chow.LocalizedSituation.localizedPowerSum, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Localized.lean, line 289. The attribute's comment: “P_p(Z → X, E) ∈ A^p(Z → X), when E|_{X ∖ Z} is zero”.

The localized class P_p(Z ⟶ X, E) ∈ A^p(Z ⟶ X) of Stacks 0FB2 and Definition 0FB5 (1), when E|_{X ∖ Z} is zero, for every p ≥ 0: the class P'_p(Q) of Stacks 0F9K for the graph construction b : W ⟶ 𝐏¹_X, Q of E and the open and closed T' ⊆ T ⊆ W_∞ on which Q is zero, where T ⊆ W_∞ is the closed subscheme of Stacks 0F90 (3), (4). The Chern classes of Q are defined in Situation 0GUJ (Stacks.Chow.LocalizedSituation.hasDefinedChernClasses_graphObject, from condition (3)).

abbrev localizedPowerSum (h : S.IsZeroOnComplement) (p : ℕ) :
    BivariantClass S.base (gysinSystemOfInvertible S.base) (S.i ≫ S.a) S.a S.i rfl p

Stacks.Chow.LocalizedSituation.localizedChern, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Localized.lean, line 306. The attribute's comment: “c_p(Z → X, E) ∈ A^p(Z → X), when E|_{X ∖ Z} is finite locally free of rank < p in degree 0”.

The localized Chern class c_p(Z ⟶ X, E) ∈ A^p(Z ⟶ X) of Stacks 0FB2 and Definition 0FB5 (2), when E|_{X ∖ Z} is finite locally free of rank < p in degree 0: the class c'_p(Q) of Stacks 0F9K for the graph construction b : W ⟶ 𝐏¹_X, Q of E and the open and closed T' ⊆ T ⊆ W_∞ on which Q is finite locally free of rank < p in degree 0, where T ⊆ W_∞ is the closed subscheme of Stacks 0F90 (3), (4). The Chern classes of Q are defined in Situation 0GUJ (Stacks.Chow.LocalizedSituation.hasDefinedChernClasses_graphObject, from condition (3)).

abbrev localizedChern (h : S.IsFiniteLocallyFreeOfRankLTOnComplement) :
    BivariantClass S.base (gysinSystemOfInvertible S.base) (S.i ≫ S.a) S.a S.i rfl S.p

Stacks.Chow.LocalizedSituation.properPushforwardChowCohomology_localizedPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Localized.lean, line 330. The attribute's comment: “i_* ∘ P_p(Z → X, E) = P_p(E), when E|_{X ∖ Z} is zero”.

i_* ∘ P_p(Z ⟶ X, E) = P_p(E) (Stacks 0FB2, equation 0FB1) as bivariant classes on X, with ∘ the pushforward of Stacks 0EPK, when E|_{X ∖ Z} is zero.

theorem properPushforwardChowCohomology_localizedPowerSum (h : S.IsZeroOnComplement) (p : ℕ) :
    properPushforwardChowCohomology S.base S.a (S.i ≫ S.a) S.i rfl (S.localizedPowerSum h p) =
      perfectPowerSumComponent S.base S.a S.hasDefinedChernClasses_E p

Stacks.Chow.LocalizedSituation.properPushforwardChowCohomology_localizedChern, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Localized.lean, line 343. The attribute's comment: “i_* ∘ c_p(Z → X, E) = c_p(E), when E|_{X ∖ Z} is finite locally free of rank < p in degree 0”.

i_* ∘ c_p(Z ⟶ X, E) = c_p(E) (Stacks 0FB2, equation 0FB1) as bivariant classes on X, with ∘ the pushforward of Stacks 0EPK, when E|_{X ∖ Z} is finite locally free of rank < p in degree 0.

theorem properPushforwardChowCohomology_localizedChern
    (h : S.IsFiniteLocallyFreeOfRankLTOnComplement) :
    properPushforwardChowCohomology S.base S.a (S.i ≫ S.a) S.i rfl (S.localizedChern h) =
      perfectChernClass S.base S.a S.hasDefinedChernClasses_E S.p

Tag 0FB5, a definition

Tag 0FB5 in the Stacks Project.

Stacks.Chow.LocalizedSituation.localizedPowerSum, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Localized.lean, line 289. The attribute's comment: “(1): P_p(Z → X, E) for every p ≥ 0, when E|_{X ∖ Z} is zero”.

The localized class P_p(Z ⟶ X, E) ∈ A^p(Z ⟶ X) of Stacks 0FB2 and Definition 0FB5 (1), when E|_{X ∖ Z} is zero, for every p ≥ 0: the class P'_p(Q) of Stacks 0F9K for the graph construction b : W ⟶ 𝐏¹_X, Q of E and the open and closed T' ⊆ T ⊆ W_∞ on which Q is zero, where T ⊆ W_∞ is the closed subscheme of Stacks 0F90 (3), (4). The Chern classes of Q are defined in Situation 0GUJ (Stacks.Chow.LocalizedSituation.hasDefinedChernClasses_graphObject, from condition (3)).

abbrev localizedPowerSum (h : S.IsZeroOnComplement) (p : ℕ) :
    BivariantClass S.base (gysinSystemOfInvertible S.base) (S.i ≫ S.a) S.a S.i rfl p

Stacks.Chow.LocalizedSituation.localizedChern, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Localized.lean, line 306. The attribute's comment: “(2): the localized pth Chern class c_p(Z → X, E), when E|_{X ∖ Z} is finite locally free of rank < p in degree 0”.

The localized Chern class c_p(Z ⟶ X, E) ∈ A^p(Z ⟶ X) of Stacks 0FB2 and Definition 0FB5 (2), when E|_{X ∖ Z} is finite locally free of rank < p in degree 0: the class c'_p(Q) of Stacks 0F9K for the graph construction b : W ⟶ 𝐏¹_X, Q of E and the open and closed T' ⊆ T ⊆ W_∞ on which Q is finite locally free of rank < p in degree 0, where T ⊆ W_∞ is the closed subscheme of Stacks 0F90 (3), (4). The Chern classes of Q are defined in Situation 0GUJ (Stacks.Chow.LocalizedSituation.hasDefinedChernClasses_graphObject, from condition (3)).

abbrev localizedChern (h : S.IsFiniteLocallyFreeOfRankLTOnComplement) :
    BivariantClass S.base (gysinSystemOfInvertible S.base) (S.i ≫ S.a) S.a S.i rfl S.p

Stacks.Chow.LocalizedSituation.localizedChernChar, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Localized.lean, line 317. The attribute's comment: “(1): the localized Chern character ch(Z → X, E) = Σ_p P_p(Z → X, E)/p! in Π_{p ≥ 0} A^p(Z → X) ⊗ Q, when E|_{X ∖ Z} is zero”.

The localized Chern character ch(Z ⟶ X, E) = ∑_p P_p(Z ⟶ X, E)/p! of Definition 0FB5 (1), when E|_{X ∖ Z} is zero, as an element of ∏_{p ≥ 0} A^p(Z ⟶ X) ⊗ 𝐐, built from Stacks.Chow.LocalizedSituation.localizedPowerSum.

abbrev localizedChernChar (h : S.IsZeroOnComplement) (p : ℕ) :
    TensorProduct ℤ ℚ
      (BivariantClass S.base (gysinSystemOfInvertible S.base) (S.i ≫ S.a) S.a S.i rfl (p : ℤ))

Tag 0FB3, a lemma

Tag 0FB3 in the Stacks Project.

Stacks.Chow.LocalizedSituation.bivariantRestriction_localizedPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedRestriction.lean, line 549. The attribute's comment: “for P_p: the class P_p(Z' → X', E') of Lemma 0FB2 for X', Z' = f^{-1}(Z) and E' = f^*E is the restriction (Remark 0F9Z) of P_p(Z → X, E)”.

In Situation 0GUJ with E|_{X ∖ Z} zero, let f : X' ⟶ X be locally of finite type, E' = Lf^*E and Z' = f^{-1}(Z) = Z ×_X X'. Then the class P_p(Z' ⟶ X', E') ∈ A^p(Z' ⟶ X') of Stacks 0FB2, constructed from X', Z', E' (the situation Stacks.Chow.LocalizedSituation.pullback), is the restriction (Remark 0F9Z) of P_p(Z ⟶ X, E) ∈ A^p(Z ⟶ X).

theorem bivariantRestriction_localizedPowerSum (h : S.IsZeroOnComplement) (p : ℕ) :
    bivariantClassCongrBase S.base (gysinSystemOfInvertible S.base) (Limits.pullback.snd S.i f)
        (pullbackSnd_comp_structureMorphism_eq S.base (S.i ≫ S.a) S.a S.i rfl f).symm rfl
        (hv := pullbackSnd_comp_structureMorphism_eq S.base (S.i ≫ S.a) S.a S.i rfl f)
        (hv' := rfl) p
        (bivariantRestriction S.base (gysinSystemOfInvertible S.base) (S.i ≫ S.a) S.a S.i rfl f p
          (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso S.base)
          (S.localizedPowerSum h p)) =
      (S.pullback f).localizedPowerSum h.pullback p

Stacks.Chow.LocalizedSituation.bivariantRestriction_localizedChern, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedRestriction.lean, line 577. The attribute's comment: “for c_p: the class c_p(Z' → X', E') of Lemma 0FB2 for X', Z' = f^{-1}(Z) and E' = f^*E is the restriction (Remark 0F9Z) of c_p(Z → X, E)”.

In Situation 0GUJ with E|_{X ∖ Z} finite locally free of rank < p in degree 0, let f : X' ⟶ X be locally of finite type, E' = Lf^*E and Z' = f^{-1}(Z) = Z ×_X X'. Then the class c_p(Z' ⟶ X', E') ∈ A^p(Z' ⟶ X') of Stacks 0FB2, constructed from X', Z', E' (the situation Stacks.Chow.LocalizedSituation.pullback), is the restriction (Remark 0F9Z) of c_p(Z ⟶ X, E) ∈ A^p(Z ⟶ X).

theorem bivariantRestriction_localizedChern (h : S.IsFiniteLocallyFreeOfRankLTOnComplement) :
    bivariantClassCongrBase S.base (gysinSystemOfInvertible S.base) (Limits.pullback.snd S.i f)
        (pullbackSnd_comp_structureMorphism_eq S.base (S.i ≫ S.a) S.a S.i rfl f).symm rfl
        (hv := pullbackSnd_comp_structureMorphism_eq S.base (S.i ≫ S.a) S.a S.i rfl f)
        (hv' := rfl) S.p
        (bivariantRestriction S.base (gysinSystemOfInvertible S.base) (S.i ≫ S.a) S.a S.i rfl f
          S.p (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso S.base)
          (S.localizedChern h)) =
      (S.pullback f).localizedChern h.pullback

Tag 0GUK, a remark

Tag 0GUK in the Stacks Project.

Stacks.Chow.LocalizedChernData.localizedPowerSum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/DefinedChernClasses.lean, line 589. The attribute's comment: “P_p(Z → X, E) in A^p(Z → X) for E perfect with E|_{X ∖ Z} zero whose Chern classes are defined, by descent (0GUC) of the classes of 0FB2 along an envelope; in Situation 0GUJ it is the class of 0FB2 (localizedPowerSum_toLocalizedChernData)”.

The localized class P_p(Z ⟶ X, E) ∈ A^p(Z ⟶ X) when the Chern classes of E are defined (Remark 0GUK), when E|_{X ∖ Z} is zero, for every degree p: the unique class whose restriction along the envelope g : Y ⟶ X of a presentation of E by a locally bounded complex of finite locally free modules is the class P_p(Z ×_X Y ⟶ Y, Lg^*E) of Stacks 0FB2 (Stacks 0GUC). In Situation 0GUJ it is the class of Stacks 0FB2 (Stacks.Chow.LocalizedSituation.localizedPowerSum_toLocalizedChernData).

def localizedPowerSum (hE : HasDefinedChernClasses D.E) (h : D.IsZeroOnComplement) (p : ℕ) :
    BivariantClass D.base (gysinSystemOfInvertible D.base) (D.i ≫ D.a) D.a D.i rfl p

Stacks.Chow.LocalizedChernData.localizedChern, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/DefinedChernClasses.lean, line 623. The attribute's comment: “c_p(Z → X, E) in A^p(Z → X) for E perfect with E|_{X ∖ Z} finite locally free of rank < p in degree 0 whose Chern classes are defined, by descent (0GUC) of the classes of 0FB2 along an envelope; in Situation 0GUJ it is the class of 0FB2 (localizedChern_toLocalizedChernData)”.

The localized Chern class c_p(Z ⟶ X, E) ∈ A^p(Z ⟶ X) when the Chern classes of E are defined (Remark 0GUK), when E|_{X ∖ Z} is finite locally free of rank < p in degree 0: the unique class whose restriction along the envelope g : Y ⟶ X of a presentation of E is the class c_p(Z ×_X Y ⟶ Y, Lg^*E) of Stacks 0FB2 (Stacks 0GUC). In Situation 0GUJ it is the class of Stacks 0FB2 (Stacks.Chow.LocalizedSituation.localizedChern_toLocalizedChernData).

def localizedChern (hE : HasDefinedChernClasses D.E)
    (h : D.IsFiniteLocallyFreeOfRankLTOnComplement) :
    BivariantClass D.base (gysinSystemOfInvertible D.base) (D.i ≫ D.a) D.a D.i rfl D.p

Stacks.Chow.LocalizedChernData.localizedChernChar, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/DefinedChernClasses.lean, line 633. The attribute's comment: “the localized Chern character ch(Z → X, E) = Σ_p P_p(Z → X, E)/p! of 0FB5 (1) for E perfect with E|_{X ∖ Z} zero whose Chern classes are defined”.

The localized Chern character ch(Z ⟶ X, E) = ∑_p P_p(Z ⟶ X, E)/p! when the Chern classes of E are defined (Definition 0FB5 (1) and Remark 0GUK), when E|_{X ∖ Z} is zero, as an element of ∏_{p ≥ 0} A^p(Z ⟶ X) ⊗ 𝐐.

def localizedChernChar (hE : HasDefinedChernClasses D.E) (h : D.IsZeroOnComplement) (p : ℕ) :
    TensorProduct ℤ ℚ
      (BivariantClass D.base (gysinSystemOfInvertible D.base) (D.i ≫ D.a) D.a D.i rfl (p : ℤ))

Stacks.Chow.LocalizedSituation.localizedPowerSum_toLocalizedChernData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/DefinedChernClasses.lean, line 912. The attribute's comment: “the extension agrees with the definition: in Situation 0GUJ the class P_p(Z → X, E) of the remark is the class of 0FB2”.

In Situation 0GUJ the class of Remark 0GUK is the class P_p(Z ⟶ X, E) of Stacks 0FB2: both restrict to P_p(Z ×_X Y ⟶ Y, Lg^*E) along an envelope (Stacks 0FB3), and the uniqueness in Stacks 0GUC applies.

theorem localizedPowerSum_toLocalizedChernData (h : S.IsZeroOnComplement) (p : ℕ) :
    S.toLocalizedChernData.localizedPowerSum S.hasDefinedChernClasses_E h p =
      S.localizedPowerSum h p

Stacks.Chow.LocalizedSituation.localizedChern_toLocalizedChernData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/DefinedChernClasses.lean, line 939. The attribute's comment: “the extension agrees with the definition: in Situation 0GUJ the class c_p(Z → X, E) of the remark is the class of 0FB2”.

In Situation 0GUJ the class of Remark 0GUK is the class c_p(Z ⟶ X, E) of Stacks 0FB2, as Stacks.Chow.LocalizedSituation.localizedPowerSum_toLocalizedChernData.

theorem localizedChern_toLocalizedChernData (h : S.IsFiniteLocallyFreeOfRankLTOnComplement) :
    S.toLocalizedChernData.localizedChern S.hasDefinedChernClasses_E h =
      S.localizedChern h

Tag 0FB4, a lemma

Tag 0FB4 in the Stacks Project.

Stacks.Chow.LocalizedSituation.localizedPowerSum_cap_chowPush, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedCap.lean, line 213. The attribute's comment: “P_p(Z ⟶ X, E) ∩ i_* α = P_p(E|_Z) ∩ α, after every base change”.

Stacks 0FB4, for P_p(Z ⟶ X, E). In Situation 0GUJ, when E|_{X ∖ Z} is zero, P_p(Z ⟶ X, E) ∩ i_* α = P_p(E|_Z) ∩ α for α ∈ CH_*(Z), and similarly after every base change: on every test scheme g : T ⟶ X, the cap product of P_p(Z ⟶ X, E) with a class pushed forward from T ×_X Z is the operation of P_p(Li^*E) ∈ A^p(Z) on it. This is the first formula of the characterization of Stacks 0F9H. The Chern classes of Li^*E are defined by Stacks 0GUE (5), from those of E (Stacks.Chow.LocalizedSituation.hasDefinedChernClasses_E).

theorem localizedPowerSum_cap_chowPush (h : S.IsZeroOnComplement) (p : ℕ)
    {T : Scheme.{u}} (g : T ⟶ S.X) [LocallyOfFiniteType g] (k : ℤ)
    (α : chowGroup S.base (pullback.fst S.i g ≫ (S.i ≫ S.a)) k) :
    (S.localizedPowerSum h p).cap g k
        (chowPush S.base _ _ (pullback.snd S.i g) (pullbackSnd_comp_structureMorphism rfl g) k
          α) =
      (perfectPowerSumComponent S.base (S.i ≫ S.a)
          (hasDefinedChernClasses_of_derivedPullback S.i _ S.E S.hasDefinedChernClasses_E
            (Iso.refl _)) p).idRule S.base (S.i ≫ S.a)
        (gysinSystemOfInvertible S.base) (pullback.fst S.i g) k α

Stacks.Chow.LocalizedSituation.localizedChern_cap_chowPush, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedCap.lean, line 239. The attribute's comment: “c_p(Z ⟶ X, E) ∩ i_* α = c_p(E|_Z) ∩ α, after every base change”.

Stacks 0FB4, for c_p(Z ⟶ X, E). In Situation 0GUJ, when E|_{X ∖ Z} is finite locally free of rank < p in degree 0, c_p(Z ⟶ X, E) ∩ i_* α = c_p(E|_Z) ∩ α for α ∈ CH_*(Z), and similarly after every base change: on every test scheme g : T ⟶ X, the cap product of c_p(Z ⟶ X, E) with a class pushed forward from T ×_X Z is the operation of c_p(Li^*E) ∈ A^p(Z) on it. This is the first formula of the characterization of Stacks 0F9H. The Chern classes of Li^*E are defined by Stacks 0GUE (5), from those of E (Stacks.Chow.LocalizedSituation.hasDefinedChernClasses_E).

theorem localizedChern_cap_chowPush (h : S.IsFiniteLocallyFreeOfRankLTOnComplement)
    {T : Scheme.{u}} (g : T ⟶ S.X) [LocallyOfFiniteType g] (k : ℤ)
    (α : chowGroup S.base (pullback.fst S.i g ≫ (S.i ≫ S.a)) k) :
    (S.localizedChern h).cap g k
        (chowPush S.base _ _ (pullback.snd S.i g) (pullbackSnd_comp_structureMorphism rfl g) k
          α) =
      (perfectChernClass S.base (S.i ≫ S.a)
          (hasDefinedChernClasses_of_derivedPullback S.i _ S.E S.hasDefinedChernClasses_E
            (Iso.refl _)) S.p).idRule S.base (S.i ≫ S.a)
        (gysinSystemOfInvertible S.base) (pullback.fst S.i g) k α

Tag 0FB6, a lemma

Tag 0FB6 in the Stacks Project.

Stacks.Chow.LocalizedSituation.localizedPowerSum_capVanishesOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedCap.lean, line 264. The attribute's comment: “P_p(Z ⟶ X, E) ∩ α = 0 for α supported away from Z, after every base change”.

Stacks 0FB6, for P_p(Z ⟶ X, E). In Situation 0GUJ, when E|_{X ∖ Z} is zero: if α ∈ CH_k(X) has support disjoint from Z, then P_p(Z ⟶ X, E) ∩ α = 0, and similarly after every base change: the class caps to zero over every z : V ⟶ X whose image is disjoint from Z. This is the second formula of the characterization of Stacks 0F9H.

theorem localizedPowerSum_capVanishesOver (h : S.IsZeroOnComplement) (p : ℕ)
    {V : Scheme.{u}} (z : V ⟶ S.X) (hz : Disjoint (Set.range z) (Set.range S.i)) :
    (S.localizedPowerSum h p).CapVanishesOver z

Stacks.Chow.LocalizedSituation.localizedChern_capVanishesOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedCap.lean, line 275. The attribute's comment: “c_p(Z ⟶ X, E) ∩ α = 0 for α supported away from Z, after every base change”.

Stacks 0FB6, for c_p(Z ⟶ X, E). In Situation 0GUJ, when E|_{X ∖ Z} is finite locally free of rank < p in degree 0: if α ∈ CH_k(X) has support disjoint from Z, then c_p(Z ⟶ X, E) ∩ α = 0, and similarly after every base change: the class caps to zero over every z : V ⟶ X whose image is disjoint from Z. This is the second formula of the characterization of Stacks 0F9H.

theorem localizedChern_capVanishesOver (h : S.IsFiniteLocallyFreeOfRankLTOnComplement)
    {V : Scheme.{u}} (z : V ⟶ S.X) (hz : Disjoint (Set.range z) (Set.range S.i)) :
    (S.localizedChern h).CapVanishesOver z

Tag 0FB7, a lemma

Tag 0FB7 in the Stacks Project.

Stacks.Chow.LocalizedSituation.localizedPowerSum_withLargerClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LargerClosedSubscheme.lean, line 530. The attribute's comment: “for P_p”.

Stacks 0FB7 (Lemma 42.50.8), for P_p. In Situation 0GUJ with E|_{X ∖ Z} zero, let Z ⊆ Z' ⊆ X be closed, with j : Z ⟶ Z'. Then P_p(Z' ⟶ X, E) = (Z ⟶ Z')_* ∘ P_p(Z ⟶ X, E) in A^p(Z' ⟶ X), with ∘ as in Stacks 0EPK; the class P_p(Z' ⟶ X, E) is that of the situation Stacks.Chow.LocalizedSituation.withLargerClosed for Z'.

theorem localizedPowerSum_withLargerClosed (h : S.IsZeroOnComplement) (p : ℕ) :
    (S.withLargerClosed i' j hj).localizedPowerSum h.withLargerClosed p =
      bivariantProperPushforwardOfInvertible S.base (S.i ≫ S.a) (i' ≫ S.a) S.a j i'
        (by rw [← Category.assoc, hj]) rfl p
        ((S.localizedPowerSum h p).congrHom hj.symm (by rw [hj]))

Stacks.Chow.LocalizedSituation.localizedChern_withLargerClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LargerClosedSubscheme.lean, line 546. The attribute's comment: “for c_p”.

Stacks 0FB7 (Lemma 42.50.8), for c_p. In Situation 0GUJ with E|_{X ∖ Z} finite locally free of rank < p in degree 0, let Z ⊆ Z' ⊆ X be closed, with j : Z ⟶ Z'. Then c_p(Z' ⟶ X, E) = (Z ⟶ Z')_* ∘ c_p(Z ⟶ X, E) in A^p(Z' ⟶ X), with ∘ as in Stacks 0EPK; the class c_p(Z' ⟶ X, E) is that of the situation Stacks.Chow.LocalizedSituation.withLargerClosed for Z'.

theorem localizedChern_withLargerClosed (h : S.IsFiniteLocallyFreeOfRankLTOnComplement) :
    (S.withLargerClosed i' j hj).localizedChern h.withLargerClosed =
      bivariantProperPushforwardOfInvertible S.base (S.i ≫ S.a) (i' ≫ S.a) S.a j i'
        (by rw [← Category.assoc, hj]) rfl S.p
        ((S.localizedChern h).congrHom hj.symm (by rw [hj]))

Tag 0FB8, a lemma

Tag 0FB8 in the Stacks Project.

Stacks.Chow.LocalizedSituation.closedCoverPowerSum_eq_localizedPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedClosedCover.lean, line 779. The attribute's comment: “for P_p: P'_p(E₂) = P_p(X₂ → X, E) when E|_{X₁} is zero”.

Stacks 0FB8, for P_p. Let X = X₁ ∪ X₂ be a closed cover, let E be a perfect object of D(𝒪_X) whose restriction to X₁ is zero, and let (X, X₂, E) satisfy the finiteness condition (3) of Situation 0GUJ, i.e. form a situation S with S.Z = X₂. Then the class P'_p(E|_{X₂}) ∈ A^p(X₂ ⟶ X) of Stacks 0F9H agrees with the localized class P_p(X₂ ⟶ X, E) of Definition 0FB5. Condition (2) of Situation 0GUJ for X₂ is Stacks.Chow.LocalizedSituation.isZeroOnComplement_of_isZero_derivedPullback, and the vanishing of E|_{X₂} on X₁ ∩ X₂ is that of E|_{X₁}.

By Stacks 0BCD E vanishes on an open U ⊇ X₁; let Z be the reduced closed subscheme on X ∖ U, so that Z ⊆ X₂ and Z ∩ X₁ = ∅. By Stacks 0FB7 P_p(X₂ ⟶ X, E) is pushed forward from P_p(Z ⟶ X, E), which kills the classes from X₁ by Stacks 0FB6; and it caps the classes from X₂ as P_p(E|_{X₂}) does by Stacks 0FB4. Uniqueness in Stacks 0F9H concludes.

theorem closedCoverPowerSum_eq_localizedPowerSum
    (hzero : IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      i₁.toLRSHom.toShHom).obj (S.E : DerivedCategory S.X.Modules))) (p : ℕ) :
    closedCoverPowerSum S.base S.a i₁ S.i (S.i ≫ S.a) rfl
        (S.hasDefinedChernClasses_E.derivedPullback S.i) p hcover
        (isZero_derivedPullback_of_isZero_of_comp_eq pullback.condition hzero) =
      S.localizedPowerSum (S.isZeroOnComplement_of_isZero_derivedPullback i₁ hcover hzero) p

Stacks.Chow.LocalizedSituation.closedCoverChernClass_eq_localizedChern, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedClosedCover.lean, line 818. The attribute's comment: “for c_p: c'_p(E₂) = c_p(X₂ → X, E) when E|_{X₁} is finite locally free of rank < p in degree 0”.

Stacks 0FB8, for c_p. Let X = X₁ ∪ X₂ be a closed cover, let E be a perfect object of D(𝒪_X) whose restriction to X₁ is a finite locally free module of rank < p placed in degree 0, and let (X, X₂, E) satisfy the finiteness condition (3) of Situation 0GUJ, i.e. form a situation S with S.Z = X₂ and S.p = p. Then the class c'_p(E|_{X₂}) ∈ A^p(X₂ ⟶ X) of Stacks 0F9H agrees with the localized Chern class c_p(X₂ ⟶ X, E) of Definition 0FB5. Condition (2) of Situation 0GUJ for X₂ is Stacks.Chow.LocalizedSituation.isFiniteLocallyFreeOfRankLTOnComplement_of_iso_singleFunctor, and the hypothesis of Stacks 0F9H on E|_{X₂} along X₁ ∩ X₂ is the restriction of that on E|_{X₁}.

By Stacks 0BCD E is a finite locally free module of rank < p in degree 0 on an open U ⊇ X₁; let Z be the reduced closed subscheme on X ∖ U, so that Z ⊆ X₂ and Z ∩ X₁ = ∅. By Stacks 0FB7 c_p(X₂ ⟶ X, E) is pushed forward from c_p(Z ⟶ X, E), which kills the classes from X₁ by Stacks 0FB6; and it caps the classes from X₂ as c_p(E|_{X₂}) does by Stacks 0FB4. Uniqueness in Stacks 0F9H concludes.

theorem closedCoverChernClass_eq_localizedChern
    (hrank : ∃ M : X₁.Modules, IsFiniteLocallyFreeOfRankLT M S.p ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        i₁.toLRSHom.toShHom).obj (S.E : DerivedCategory S.X.Modules) ≅
          (DerivedCategory.singleFunctor _ 0).obj M)) :
    closedCoverChernClass S.base S.a i₁ S.i (S.i ≫ S.a) rfl
        (S.hasDefinedChernClasses_E.derivedPullback S.i) S.p hcover
        (exists_isFiniteLocallyFreeOfRankLT_derivedPullback_pullbackSnd i₁ S.i hrank) =
      S.localizedChern
        (S.isFiniteLocallyFreeOfRankLTOnComplement_of_iso_singleFunctor i₁ hcover hrank)

Sources

LeanStacks.Chow.LocalizedSituation · Stacks.Chow.LocalizedChernSituation · Stacks.Chow.LocalizedSituation.localizedPowerSum · Stacks.Chow.LocalizedSituation.localizedChern · Stacks.Chow.LocalizedSituation.properPushforwardChowCohomology_localizedPowerSum · Stacks.Chow.LocalizedSituation.properPushforwardChowCohomology_localizedChern · Stacks.Chow.LocalizedSituation.localizedChernChar · Stacks.Chow.LocalizedSituation.bivariantRestriction_localizedPowerSum

Section42.51 Two technical lemmas #

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

Tag 0FE7, a lemma

Tag 0FE7 in the Stacks Project.

Stacks.Chow.supportedComposite_modificationChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedComposite.lean, line 503. The attribute's comment: “the statement for c': c'_{p_n}(Q_n) ∘ ⋯ ∘ c'_{p_1}(Q_1) = (W_{n,∞} ∩ ⋯ ∩ W_{1,∞} → Z_n ∩ ⋯ ∩ Z_1)_* ∘ c'_{p_n}(Q_n|_{W_{n,∞}}) ∘ ⋯ ∘ c'_{p_1}(Q_1|_{W_{1,∞}}) ∘ C, for every sequence of indices i_1, …, i_n”.

Composites of the classes c'. Let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, and for every index i let Z_i ⊆ X and T_i ⊆ W_∞ be closed, Q_i ∈ D(𝒪_W) perfect with defined Chern classes and p_i ≥ 0, such that the hypotheses of Stacks 0F9K hold for b, Z_i, Q_i, T_i, p_i (T_i contains every point of W_∞ over X ∖ Z_i and Q_i|_{T_i} is finite locally free of rank < p_i in degree 0), Q_i|_{W ∖ W_i} is finite locally free of rank < p_i in degree 0 for W_i = b^{-1}(𝐏¹_{Z_i}) = W ×_X Z_i, and Q_i satisfies condition (3) of Situation 0GUJ. Then for every sequence of indices i_1, …, i_n (n ≥ 1; the list L = [i_n, …, i_2] and the first index i_1)

c'\_\{p\_\{i\_n}}(Q\_\{i\_n}) ∘ ⋯ ∘ c'\_\{p\_\{i\_1}}(Q\_\{i\_1}) = (W\_\{i\_n,∞} ∩ ⋯ ∩ W\_\{i\_1,∞} ⟶ Z\_\{i\_n} ∩ ⋯ ∩ Z\_\{i\_1})\_* ∘ c'\_\{p\_\{i\_n}}(Q\_\{i\_n}|\_\{W\_\{i\_n,∞}}) ∘ ⋯ ∘ c'\_\{p\_\{i\_1}}(Q\_\{i\_1}|\_\{W\_\{i\_1,∞}}) ∘ C

in A^{p_{i_n} + ⋯ + p_{i_1}}(Z_{i_n} ∩ ⋯ ∩ Z_{i_1} ⟶ X). Here c'_p(Q) is the class of Stacks 0F9K (Stacks.Chow.modificationChernClass), c'_p(Q|_{W_{i,∞}}) that of Stacks 0F9H (Stacks.Chow.modificationInfinityChernClass), C the class of Stacks 0F9J, the composites are the products of classes supported on closed subschemes of Stacks 0FE5 (Stacks.Chow.supportedComposite, Stacks.Chow.modificationInfinityComposite), and the right side is Stacks.Chow.modificationLocalization.

theorem supportedComposite_modificationChernClass
    (hrank : ∀ i, ∃ M : (T i).Modules, IsFiniteLocallyFreeOfRankLT M (p i) ∧
      Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (t i ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj (Q i) ≅
          (DerivedCategory.singleFunctor _ 0).obj M))
    (hperf : ∀ i, Cohomology.PerfectComplexes.IsPerfect (X := W.toRingedSpace) (Q i))
    (hres : ∀ i, ∃ M : OXMod.{u, u, u} (W.toRingedSpace.restrict
          (modificationComplementOpens b (z i)).isOpenEmbedding),
        IsFiniteLocallyFreeOfRankLT M (p i) ∧
          Nonempty ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
            (W.toRingedSpace.ofRestrict (modificationComplementOpens b (z i)).isOpenEmbedding)).obj
              (Q i) ≅ (DerivedCategory.singleFunctor _ 0).obj M))
    (hfin : ∀ i, LocalizedChernFiniteness C (modificationProjection f b ≫ f) (Q i)) (i₁ : ι)
    (L : List ι) :
    supportedComposite z C f (fun i ↦ (p i : ℤ))
        (fun i ↦ modificationChernClass C f b hA (z i) (t i) (hQ i) (p i) (hT i) (hrank i)) i₁ L =
      modificationLocalization C f b hA (iteratedIntersection z i₁ L).2
        (modificationInfinityComposite z C f (fun i ↦ (p i : ℤ)) b
          (fun i ↦ modificationInfinityChernClass C f b (z i) (t i) (hT i) (hQ i) (p i) (hrank i))
          i₁ L)

Stacks.Chow.supportedComposite_modificationPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedComposite.lean, line 544. The attribute's comment: “the statement for P': P'_{p_n}(Q_n) ∘ ⋯ ∘ P'_{p_1}(Q_1) = (W_{n,∞} ∩ ⋯ ∩ W_{1,∞} → Z_n ∩ ⋯ ∩ Z_1)_* ∘ P'_{p_n}(Q_n|_{W_{n,∞}}) ∘ ⋯ ∘ P'_{p_1}(Q_1|_{W_{1,∞}}) ∘ C, for every sequence of indices i_1, …, i_n”.

Composites of the classes P'. In the situation of Stacks.Chow.supportedComposite_modificationChernClass, with Q_i|_{T_i} and Q_i|_{W ∖ W_i} zero instead of finite locally free of rank < p_i, for every sequence of indices i_1, …, i_n (n ≥ 1)

P'\_\{p\_\{i\_n}}(Q\_\{i\_n}) ∘ ⋯ ∘ P'\_\{p\_\{i\_1}}(Q\_\{i\_1}) = (W\_\{i\_n,∞} ∩ ⋯ ∩ W\_\{i\_1,∞} ⟶ Z\_\{i\_n} ∩ ⋯ ∩ Z\_\{i\_1})\_* ∘ P'\_\{p\_\{i\_n}}(Q\_\{i\_n}|\_\{W\_\{i\_n,∞}}) ∘ ⋯ ∘ P'\_\{p\_\{i\_1}}(Q\_\{i\_1}|\_\{W\_\{i\_1,∞}}) ∘ C

in A^{p_{i_n} + ⋯ + p_{i_1}}(Z_{i_n} ∩ ⋯ ∩ Z_{i_1} ⟶ X), with P'_p(Q) the class of Stacks 0F9K (Stacks.Chow.modificationPowerSum) and P'_p(Q|_{W_{i,∞}}) that of Stacks 0F9H (Stacks.Chow.modificationInfinityPowerSum).

theorem supportedComposite_modificationPowerSum
    (hzero : ∀ i, IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
      (t i ≫ modificationInclusionAtInfinity f b).toLRSHom.toShHom).obj (Q i)))
    (hperf : ∀ i, Cohomology.PerfectComplexes.IsPerfect (X := W.toRingedSpace) (Q i))
    (hres : ∀ i, IsZero ((Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (W.toRingedSpace.ofRestrict (modificationComplementOpens b (z i)).isOpenEmbedding)).obj
          (Q i)))
    (hfin : ∀ i, LocalizedChernFiniteness C (modificationProjection f b ≫ f) (Q i)) (i₁ : ι)
    (L : List ι) :
    supportedComposite z C f (fun i ↦ (p i : ℤ))
        (fun i ↦ modificationPowerSum C f b hA (z i) (t i) (hQ i) (p i) (hT i) (hzero i)) i₁ L =
      modificationLocalization C f b hA (iteratedIntersection z i₁ L).2
        (modificationInfinityComposite z C f (fun i ↦ (p i : ℤ)) b
          (fun i ↦ modificationInfinityPowerSum C f b (z i) (t i) (hT i) (hQ i) (p i) (hzero i))
          i₁ L)

Tag 0FE8, a lemma

Tag 0FE8 in the Stacks Project.

Stacks.Chow.LocalizedSituation.modificationChernClass_eq_localizedChern, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedModificationComparison.lean, line 745. The attribute's comment: “for c_p: c'_p(Q) = c_p(Z → X, F) when Q|_{b^{-1}(A^1_X)} is the pullback of F and F|_{X ∖ Z} is finite locally free of rank < p in degree 0”.

In Situation 0GUJ, let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, let Q ∈ D(𝒪_W) be perfect, and let T ⊆ W_∞ be closed, contain every point of W_∞ lying over X ∖ Z, and be such that Q|_T is finite locally free of rank < p in degree 0. Assume that Q|_{b^{-1}(𝐀¹_X)} is the pullback of F, that F|_{X ∖ Z} is finite locally free of rank < p in degree 0, and that Q on W satisfies condition (3) of Situation 0GUJ, so that the Chern classes of Q are defined (Stacks.Chow.hasDefinedChernClasses_of_localizedChernFiniteness, assumption (A0) of Stacks 0F9K). Then the class c'_p(Q) of Stacks 0F9K is the localized Chern class c_p(Z ⟶ X, F) of Stacks 0FB2.

theorem modificationChernClass_eq_localizedChern
    (hT : ∀ w, modificationProjectionAtInfinity S.a b w ∉ Set.range S.i → w ∈ Set.range t)
    (hrank : ∃ M : T.Modules, IsFiniteLocallyFreeOfRankLT M S.p ∧
      Nonempty ((derivedPullback (t ≫ modificationInclusionAtInfinity S.a b).toLRSHom.toShHom).obj
        Q ≅ (DerivedCategory.singleFunctor _ 0).obj M))
    (h : S.IsFiniteLocallyFreeOfRankLTOnComplement) :
    modificationChernClass S.base S.a b hA S.i t
        (hasDefinedChernClasses_of_localizedChernFiniteness S.base _ Q hQp hfin) S.p hT hrank =
      S.localizedChern h

Stacks.Chow.LocalizedSituation.modificationPowerSum_eq_localizedPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedModificationComparison.lean, line 842. The attribute's comment: “for P_p: P'_p(Q) = P_p(Z → X, F) when Q|_{b^{-1}(A^1_X)} is the pullback of F and F|_{X ∖ Z} is zero”.

In Situation 0GUJ, let b : W ⟶ 𝐏¹_X be proper and an isomorphism over 𝐀¹_X, let Q ∈ D(𝒪_W) be perfect, and let T ⊆ W_∞ be closed, contain every point of W_∞ lying over X ∖ Z, and be such that Q|_T is zero. Assume that Q|_{b^{-1}(𝐀¹_X)} is the pullback of F, that F|_{X ∖ Z} is zero, and that Q on W satisfies condition (3) of Situation 0GUJ, so that the Chern classes of Q are defined (Stacks.Chow.hasDefinedChernClasses_of_localizedChernFiniteness, assumption (A0) of Stacks 0F9K). Then the class P'_p(Q) of Stacks 0F9K is the localized class P_p(Z ⟶ X, F) of Stacks 0FB2.

theorem modificationPowerSum_eq_localizedPowerSum (p : ℕ)
    (hT : ∀ w, modificationProjectionAtInfinity S.a b w ∉ Set.range S.i → w ∈ Set.range t)
    (hzero : IsZero ((derivedPullback
      (t ≫ modificationInclusionAtInfinity S.a b).toLRSHom.toShHom).obj Q))
    (h : S.IsZeroOnComplement) :
    modificationPowerSum S.base S.a b hA S.i t
        (hasDefinedChernClasses_of_localizedChernFiniteness S.base _ Q hQp hfin) p hT hzero =
      S.localizedPowerSum h p

Sources

LeanStacks.Chow.supportedComposite_modificationChernClass · Stacks.Chow.supportedComposite_modificationPowerSum · Stacks.Chow.LocalizedSituation.modificationChernClass_eq_localizedChern · Stacks.Chow.LocalizedSituation.modificationPowerSum_eq_localizedPowerSum

Section42.52 Properties of localized Chern classes #

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

Tag 0FBA, a lemma

Tag 0FBA in the Stacks Project.

Stacks.Chow.LocalizedSituation.localizedPowerSum_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedNewton.lean, line 125. The attribute's comment: “In Situation 0GUJ with E|_{X ∖ Z} zero: Newton's recursion P_{q+1} = ∑_{j<q} (-1)^j c_{j+1} P_{q-j} + (-1)^q (q+1) c_{q+1} for every q ≥ 0, products in the algebra A^{(1)}(Z → X) of 0FA0; it gives P_1 = c_1, P_2 = c_1² - 2c_2, P_3 = c_1³ - 3c_1c_2 + 3c_3 and so on, the whole lemma”.

In Situation 0GUJ assume E|_{X ∖ Z} is zero. Then the localized classes P_p(Z ⟶ X, E) ∈ A^p(Z ⟶ X) of Stacks 0FB2 are Newton's polynomials in the localized Chern classes c_i(Z ⟶ X, E) (defined for every i ≥ 1, the zero module having rank < i), with the multiplication of the algebra A^{(1)}(Z ⟶ X) of Stacks 0FA0 ((c, c') ↦ res(c) ∘ c', Stacks.Chow.supportedMul):

P_{q+1} = ∑_{j < q} (-1)^j c_{j+1} P_{q-j} + (-1)^q (q + 1) c_{q+1}

for every q ≥ 0. This is the recursion defining the universal power-sum polynomials, so P_1 = c_1, P_2 = c_1² - 2c_2, P_3 = c_1³ - 3c_1c_2 + 3c_3, and so on. The summand c_{j+1} P_{q-j} lies in A^{(j+1)+(q-j)}(Z ⟶ X), read in degree q + 1.

Here P_p(Z ⟶ X, E) is Stacks.Chow.LocalizedSituation.localizedPowerSum and c_i(Z ⟶ X, E) is Stacks.Chow.LocalizedSituation.localizedChernClassOfIsZero, the class Stacks.Chow.LocalizedSituation.localizedChern for the situation in degree i; both are formed in Situation 0GUJ, condition (3) making the Chern classes of the object Q of the graph construction defined (Stacks.Chow.LocalizedSituation.hasDefinedChernClasses_graphObject, Stacks 0GUE).

theorem localizedPowerSum_succ (q : ℕ) :
    S.localizedPowerSum h (q + 1) =
      ∑ j ∈ (Finset.range q).attach, ((-1 : ℤ) ^ (j : ℕ)) •
          bivariantClassDegreeCongr S.base _ (S.i ≫ S.a) S.a S.i rfl
            (newton_degree_eq (Finset.mem_range.mp j.2))
            (supportedMul S.base (S.i ≫ S.a) S.a S.i rfl
              (localizedChernClassOfIsZero h (Nat.succ_pos (j : ℕ)))
              (S.localizedPowerSum h (q - j))) +
        ((-1 : ℤ) ^ q * ((q : ℤ) + 1)) • localizedChernClassOfIsZero h (Nat.succ_pos q)

Tag 0FBB, a lemma

Tag 0FBB in the Stacks Project.

Stacks.Chow.LocalizedSituation.nonhomogeneousBivariantTransport_compositeOfInvertible_localizedPowerSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Commutation.lean, line 570. The attribute's comment: “for P_p(Z → X, E), when E|_(X ∖ Z) is zero: P_p(Z → X, E) ∘ c = c ∘ P_p(Z → X, E) in A^(Y ×_X Z → X), for every c in A^(Y → X)”.

In Situation 0GUJ with E|_{X ∖ Z} zero, let g : Y ⟶ X be locally of finite type and let c ∈ A^*(Y ⟶ X). Then

P_p(Z ⟶ X, E) ∘ c = c ∘ P_p(Z ⟶ X, E) in A^*(Y ×_X Z ⟶ X),

where P_p(Z ⟶ X, E) ∘ c = res(P_p(Z ⟶ X, E)) ∘ c is a class for Z ×_X Y ⟶ X, carried to Y ×_X Z along the symmetry of the fibre product, and c ∘ P_p(Z ⟶ X, E) is res(c) ∘ P_p(Z ⟶ X, E). The class is P'_p(Q) of Stacks 0F9K for the graph construction, so this is Stacks.Chow.nonhomogeneousBivariantTransport_compositeOfInvertible_modificationPowerSum.

theorem nonhomogeneousBivariantTransport_compositeOfInvertible_localizedPowerSum
    (h : S.IsZeroOnComplement) (p : ℕ)
    (c : nonhomogeneousBivariantGroup S.base (gysinSystemOfInvertible S.base) (g ≫ S.a) S.a g
      rfl) :
    nonhomogeneousBivariantTransport S.base (gysinSystemOfInvertible S.base)
        (pullback.fst S.i g ≫ (S.i ≫ S.a)) (pullback.fst g S.i ≫ (g ≫ S.a)) S.a
        (pullback.snd S.i g ≫ g)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq S.base (S.i ≫ S.a) S.a S.i rfl g) rfl)
        (pullback.snd g S.i ≫ S.i)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq S.base (g ≫ S.a) S.a g rfl S.i) rfl)
        (pullbackSymmetry S.i g) (by simp [pullback.condition])
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso S.base)
        (nonhomogeneousBivariantCompositeOfInvertible S.base (pullback.fst S.i g ≫ (S.i ≫ S.a))
          (g ≫ S.a) S.a (pullback.snd S.i g) g
          (pullbackSnd_comp_structureMorphism_eq S.base (S.i ≫ S.a) S.a S.i rfl g) rfl
          (DirectSum.of _ (p : ℤ)
            (bivariantRestriction S.base (gysinSystemOfInvertible S.base) (S.i ≫ S.a) S.a S.i rfl
              g p (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso S.base)
              (S.localizedPowerSum h p))) c) =
      nonhomogeneousBivariantCompositeOfInvertible S.base (pullback.fst g S.i ≫ (g ≫ S.a))
        (S.i ≫ S.a) S.a (pullback.snd g S.i) S.i
        (pullbackSnd_comp_structureMorphism_eq S.base (g ≫ S.a) S.a g rfl S.i) rfl
        (nonhomogeneousBivariantRestriction S.base (gysinSystemOfInvertible S.base) (g ≫ S.a) S.a
          g rfl S.i (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso S.base) c)
        (DirectSum.of _ (p : ℤ) (S.localizedPowerSum h p))

Stacks.Chow.LocalizedSituation.nonhomogeneousBivariantTransport_compositeOfInvertible_localizedChern, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/Commutation.lean, line 621. The attribute's comment: “for c_p(Z → X, E), when E|_(X ∖ Z) is finite locally free of rank < p in degree 0: c_p(Z → X, E) ∘ c = c ∘ c_p(Z → X, E) in A^(Y ×_X Z → X), for every c in A^(Y → X)”.

In Situation 0GUJ with E|_{X ∖ Z} finite locally free of rank < p in degree 0, let g : Y ⟶ X be locally of finite type and let c ∈ A^*(Y ⟶ X). Then

c_p(Z ⟶ X, E) ∘ c = c ∘ c_p(Z ⟶ X, E) in A^*(Y ×_X Z ⟶ X),

where c_p(Z ⟶ X, E) ∘ c = res(c_p(Z ⟶ X, E)) ∘ c is a class for Z ×_X Y ⟶ X, carried to Y ×_X Z along the symmetry of the fibre product, and c ∘ c_p(Z ⟶ X, E) is res(c) ∘ c_p(Z ⟶ X, E). The class is c'_p(Q) of Stacks 0F9K for the graph construction, so this is Stacks.Chow.nonhomogeneousBivariantTransport_compositeOfInvertible_modificationChernClass.

theorem nonhomogeneousBivariantTransport_compositeOfInvertible_localizedChern
    (h : S.IsFiniteLocallyFreeOfRankLTOnComplement)
    (c : nonhomogeneousBivariantGroup S.base (gysinSystemOfInvertible S.base) (g ≫ S.a) S.a g
      rfl) :
    nonhomogeneousBivariantTransport S.base (gysinSystemOfInvertible S.base)
        (pullback.fst S.i g ≫ (S.i ≫ S.a)) (pullback.fst g S.i ≫ (g ≫ S.a)) S.a
        (pullback.snd S.i g ≫ g)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq S.base (S.i ≫ S.a) S.a S.i rfl g) rfl)
        (pullback.snd g S.i ≫ S.i)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq S.base (g ≫ S.a) S.a g rfl S.i) rfl)
        (pullbackSymmetry S.i g) (by simp [pullback.condition])
        (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso S.base)
        (nonhomogeneousBivariantCompositeOfInvertible S.base (pullback.fst S.i g ≫ (S.i ≫ S.a))
          (g ≫ S.a) S.a (pullback.snd S.i g) g
          (pullbackSnd_comp_structureMorphism_eq S.base (S.i ≫ S.a) S.a S.i rfl g) rfl
          (DirectSum.of _ (S.p : ℤ)
            (bivariantRestriction S.base (gysinSystemOfInvertible S.base) (S.i ≫ S.a) S.a S.i rfl
              g S.p (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso S.base)
              (S.localizedChern h))) c) =
      nonhomogeneousBivariantCompositeOfInvertible S.base (pullback.fst g S.i ≫ (g ≫ S.a))
        (S.i ≫ S.a) S.a (pullback.snd g S.i) S.i
        (pullbackSnd_comp_structureMorphism_eq S.base (g ≫ S.a) S.a g rfl S.i) rfl
        (nonhomogeneousBivariantRestriction S.base (gysinSystemOfInvertible S.base) (g ≫ S.a) S.a
          g rfl S.i (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso S.base) c)
        (DirectSum.of _ (S.p : ℤ) (S.localizedChern h))

Tag 0FBC, a remark

Tag 0FBC in the Stacks Project.

Stacks.Chow.totalLocalizedChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/TotalLocalizedChernClass.lean, line 101.

Stacks 0FBC. The total localized Chern class

c⁽ᵖ⁾(Z ⟶ X, E) = 1 + c₁(E) + … + c_{p-1}(E) + c_p(Z ⟶ X, E) + c_{p+1}(Z ⟶ X, E) + …

of a situation for localized Chern classes: the element of A⁽ᵖ⁾(Z ⟶ X) whose component in a degree 0 ≤ i < p is the ordinary Chern class c i of E, whose component in a degree i ≥ p is the localized Chern class cloc i, and whose components in the negative degrees vanish.

def totalLocalizedChernClass :
    localizedBivariantGrading T.base G (T.i ≫ T.a) T.a T.i rfl T.p

Stacks.Chow.totalLocalizedChernClass_fst_of_nonneg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/TotalLocalizedChernClass.lean, line 108. The attribute's comment: “the graded pieces in the degrees below the cutoff”.

In a degree 0 ≤ i < p the component of c⁽ᵖ⁾(Z ⟶ X, E) is the ordinary Chern class c_i(E) of E; in degree 0 that is c₀(E) = 1.

theorem totalLocalizedChernClass_fst_of_nonneg {i : ℤ} (hi : i < (T.p : ℤ)) (h0 : 0 ≤ i) :
    (totalLocalizedChernClass T G c cloc).1 ⟨i, hi⟩ = c ⟨i, h0⟩

Stacks.Chow.totalLocalizedChernClass_fst_of_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/TotalLocalizedChernClass.lean, line 115. The attribute's comment: “the vanishing of the graded pieces in the negative degrees”.

In a negative degree the component of c⁽ᵖ⁾(Z ⟶ X, E) vanishes, the source's display having no term there.

theorem totalLocalizedChernClass_fst_of_neg {i : ℤ} (hi : i < (T.p : ℤ)) (h0 : i < 0) :
    (totalLocalizedChernClass T G c cloc).1 ⟨i, hi⟩ = 0

Stacks.Chow.totalLocalizedChernClass_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/TotalLocalizedChernClass.lean, line 122. The attribute's comment: “the graded pieces in the degrees from the cutoff onward”.

In a degree i ≥ p the component of c⁽ᵖ⁾(Z ⟶ X, E) is the localized Chern class c_i(Z ⟶ X, E).

theorem totalLocalizedChernClass_snd (i : {i : ℤ // (T.p : ℤ) ≤ i}) :
    (totalLocalizedChernClass T G c cloc).2 i = cloc i

Stacks.Chow.LocalizedChernData.totalLocalizedChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/TotalLocalizedChernClassData.lean, line 60.

The total localized Chern class

c⁽ᵖ⁾(Z ⟶ X, E) = 1 + c₁(E) + … + c_{p-1}(E) + c_p(Z ⟶ X, E) + c_{p+1}(Z ⟶ X, E) + …

of the data of a localized Chern class: the element of A⁽ᵖ⁾(Z ⟶ X) whose component in a degree 0 ≤ i < p is the ordinary Chern class c i of E, whose component in a degree i ≥ p is the localized Chern class cloc i, and whose components in the negative degrees vanish.

def LocalizedChernData.totalLocalizedChernClass (T : LocalizedChernData.{u})
    (G : GysinSystem T.base)
    (c : (i : {i : ℤ // 0 ≤ i}) →
      BivariantClass T.base G T.a T.a (𝟙 T.X) (Category.id_comp T.a) i.1)
    (cloc : (i : {i : ℤ // (T.p : ℤ) ≤ i}) →
      BivariantClass T.base G (T.i ≫ T.a) T.a T.i rfl i.1) :
    localizedBivariantGrading T.base G (T.i ≫ T.a) T.a T.i rfl T.p

Stacks.Chow.LocalizedChernData.totalLocalizedChernClass_fst_of_nonneg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/TotalLocalizedChernClassData.lean, line 78. The attribute's comment: “the graded pieces in the degrees below the cutoff”.

In a degree 0 ≤ i < p the component of c⁽ᵖ⁾(Z ⟶ X, E) is the ordinary Chern class c_i(E) of E; in degree 0 that is c₀(E) = 1.

theorem LocalizedChernData.totalLocalizedChernClass_fst_of_nonneg {i : ℤ} (hi : i < (T.p : ℤ))
    (h0 : 0 ≤ i) :
    (LocalizedChernData.totalLocalizedChernClass T G c cloc).1 ⟨i, hi⟩ = c ⟨i, h0⟩

Stacks.Chow.LocalizedChernData.totalLocalizedChernClass_fst_of_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/TotalLocalizedChernClassData.lean, line 85. The attribute's comment: “the vanishing of the graded pieces in the negative degrees”.

In a negative degree the component of c⁽ᵖ⁾(Z ⟶ X, E) vanishes.

theorem LocalizedChernData.totalLocalizedChernClass_fst_of_neg {i : ℤ} (hi : i < (T.p : ℤ))
    (h0 : i < 0) :
    (LocalizedChernData.totalLocalizedChernClass T G c cloc).1 ⟨i, hi⟩ = 0

Stacks.Chow.LocalizedChernData.totalLocalizedChernClass_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/TotalLocalizedChernClassData.lean, line 93. The attribute's comment: “the graded pieces in the degrees from the cutoff onward”.

In a degree i ≥ p the component of c⁽ᵖ⁾(Z ⟶ X, E) is the localized Chern class c_i(Z ⟶ X, E).

theorem LocalizedChernData.totalLocalizedChernClass_snd (i : {i : ℤ // (T.p : ℤ) ≤ i}) :
    (LocalizedChernData.totalLocalizedChernClass T G c cloc).2 i = cloc i

Tag 0FBD, a lemma

Tag 0FBD in the Stacks Project.

Stacks.Chow.LocalizedChernData.totalLocalizedChern_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/WhitneyLocalized.lean, line 991.

Stacks 0FBD. Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S, let Z ⟶ X be a closed immersion and let E₁ ⟶ E₂ ⟶ E₃ ⟶ E₁[1] be a distinguished triangle of perfect objects of D(𝒪_X). Assume (1) E₁|_{X ∖ Z} and E₃|_{X ∖ Z} are finite locally free of rank < p₁ and < p₃ placed in degree 0, and (2) one of: (a) X is quasi-compact, (b) X has quasi-compact irreducible components, (c) E₃ ⟶ E₁[1] is represented by a map of locally bounded complexes of finite locally free 𝒪_X-modules, (d) the same holds for Lf^*E₃ ⟶ Lf^*E₁[1] after an envelope f : Y ⟶ X. These are stated as the hypothesis hc, in the source's order (a), (b), (c), (d). Then

c⁽ᵖ¹⁺ᵖ³⁾(Z ⟶ X, E₂) = c⁽ᵖ¹⁾(Z ⟶ X, E₁) c⁽ᵖ³⁾(Z ⟶ X, E₃) in A⁽ᵖ¹⁺ᵖ³⁾(Z ⟶ X),

with the classes of Remark 0FBC (Stacks.Chow.LocalizedChernData.totalLocalizedChern) and the multiplication of Remark 0FA0 (Stacks.Chow.localizedGradingMul). That the statement makes sense, i.e. that E₂|_{X ∖ Z} is finite locally free of rank < p₁ + p₃ in degree 0 and that the Chern classes of E₁, E₂, E₃ are defined, is Stacks.Chow.LocalizedChernData.exists_isFiniteLocallyFreeOfRankLT_restrict_obj₂ and Stacks.Chow.hasDefinedChernClasses_triangle_of_mor₃. This is the output cutoff r = p₁ + p₃ of Stacks.Chow.LocalizedChernData.totalLocalizedChern_triangle_eq_cutoffMul.

theorem totalLocalizedChern_triangle
    (a : E₁ ⟶ E₂) (b : E₂ ⟶ E₃) (c : E₃ ⟶ E₁⟦(1 : ℤ)⟧) (hT : Triangle.mk a b c ∈ distTriang _)
    (r₁ : (∃ M : OXMod.{u, u, u} (D.X.toRingedSpace.restrict (⟨(Set.range D.i.base)ᶜ,
      D.i.isClosedEmbedding.isClosed_range.isOpen_compl⟩ : D.X.Opens).isOpenEmbedding),
      IsFiniteLocallyFreeOfRankLT M p₁ ∧
        Nonempty ((derivedPullback (D.X.toRingedSpace.ofRestrict (⟨(Set.range D.i.base)ᶜ,
          D.i.isClosedEmbedding.isClosed_range.isOpen_compl⟩ :
            D.X.Opens).isOpenEmbedding)).obj E₁ ≅ (DerivedCategory.singleFunctor _ 0).obj M)))
    (r₃ : (∃ M : OXMod.{u, u, u} (D.X.toRingedSpace.restrict (⟨(Set.range D.i.base)ᶜ,
      D.i.isClosedEmbedding.isClosed_range.isOpen_compl⟩ : D.X.Opens).isOpenEmbedding),
      IsFiniteLocallyFreeOfRankLT M p₃ ∧
        Nonempty ((derivedPullback (D.X.toRingedSpace.ofRestrict (⟨(Set.range D.i.base)ᶜ,
          D.i.isClosedEmbedding.isClosed_range.isOpen_compl⟩ :
            D.X.Opens).isOpenEmbedding)).obj E₃ ≅ (DerivedCategory.singleFunctor _ 0).obj M)))
    (hc : CompactSpace D.X ∨ (∀ T ∈ irreducibleComponents D.X, IsCompact T) ∨
      HasMapPresentation c ∨ HasEnvelopeMapPresentation c) :
    totalLocalizedChern (D := D.withObject E₂ (p₁ + p₃) h₂
        (D.exists_isFiniteLocallyFreeOfRankLT_restrict_obj₂ a b c hT (by omega) r₁ r₃))
        (hasDefinedChernClasses_triangle_of_mor₃ D.base D.a h₁ h₂ h₃ hT
          (hasTriangleChernCondition_of_conditions hc)).2.1
        (D.isFiniteLocallyFreeOfRankLTOnComplement_withObject _) =
      localizedGradingMul D.base (D.i ≫ D.a) D.a D.i rfl
        (totalLocalizedChern (D := D.withObject E₁ p₁ h₁ r₁)
          (hasDefinedChernClasses_triangle_of_mor₃ D.base D.a h₁ h₂ h₃ hT
            (hasTriangleChernCondition_of_conditions hc)).1
          (D.isFiniteLocallyFreeOfRankLTOnComplement_withObject r₁))
        (totalLocalizedChern (D := D.withObject E₃ p₃ h₃ r₃)
          (hasDefinedChernClasses_triangle_of_mor₃ D.base D.a h₁ h₂ h₃ hT
            (hasTriangleChernCondition_of_conditions hc)).2.2
          (D.isFiniteLocallyFreeOfRankLTOnComplement_withObject r₃))

Tag 0FBE, a lemma

Tag 0FBE in the Stacks Project.

Stacks.Chow.LocalizedChernData.localizedPowerSum_localizedChernChar_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/WhitneyLocalized.lean, line 1155.

Stacks 0FBE. Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S, let Z ⟶ X be a closed immersion and let E₁ ⟶ E₂ ⟶ E₃ ⟶ E₁[1] be a distinguished triangle of perfect objects of D(𝒪_X). Assume (1) E₁|_{X ∖ Z} and E₃|_{X ∖ Z} are zero, and (2) one of the conditions (a)–(d) of Stacks 0FBD on E₃ ⟶ E₁[1], stated as the hypothesis hc in the source's order: (a) X is quasi-compact, (b) X has quasi-compact irreducible components, (c) E₃ ⟶ E₁[1] is represented by a map of locally bounded complexes of finite locally free 𝒪_X-modules, (d) the same holds for Lf^*E₃ ⟶ Lf^*E₁[1] after an envelope f : Y ⟶ X. Then

P_p(Z ⟶ X, E₂) = P_p(Z ⟶ X, E₁) + P_p(Z ⟶ X, E₃) for all p,

and consequently ch(Z ⟶ X, E₂) = ch(Z ⟶ X, E₁) + ch(Z ⟶ X, E₃), in every degree p, for the classes of Remark 0GUK (Stacks.Chow.LocalizedChernData.localizedPowerSum, Stacks.Chow.LocalizedChernData.localizedChernChar). The case p = 0 is included.

The localized classes P_p(Z ⟶ X, E) are defined for p ≥ 0 (Definition 0FB5); the source's p ∈ 𝐙 ranges over those.

theorem localizedPowerSum_localizedChernChar_triangle
    (a : E₁ ⟶ E₂) (b : E₂ ⟶ E₃) (c : E₃ ⟶ E₁⟦(1 : ℤ)⟧) (hT : Triangle.mk a b c ∈ distTriang _)
    (z₁ : IsZero ((derivedPullback (D.X.toRingedSpace.ofRestrict (⟨(Set.range D.i.base)ᶜ,
      D.i.isClosedEmbedding.isClosed_range.isOpen_compl⟩ : D.X.Opens).isOpenEmbedding)).obj E₁))
    (z₃ : IsZero ((derivedPullback (D.X.toRingedSpace.ofRestrict (⟨(Set.range D.i.base)ᶜ,
      D.i.isClosedEmbedding.isClosed_range.isOpen_compl⟩ : D.X.Opens).isOpenEmbedding)).obj E₃))
    (hc : CompactSpace D.X ∨ (∀ T ∈ irreducibleComponents D.X, IsCompact T) ∨
      HasMapPresentation c ∨ HasEnvelopeMapPresentation c) :
    (∀ p : ℕ,
      (D.withZeroObject E₂ h₂ (D.isZero_restrict_obj₂ a b c hT z₁ z₃)).localizedPowerSum
          (hasDefinedChernClasses_triangle_of_mor₃ D.base D.a h₁ h₂ h₃ hT
            (hasTriangleChernCondition_of_conditions hc)).2.1
          (D.isZero_restrict_obj₂ a b c hT z₁ z₃) p =
        (D.withZeroObject E₁ h₁ z₁).localizedPowerSum
            (hasDefinedChernClasses_triangle_of_mor₃ D.base D.a h₁ h₂ h₃ hT
              (hasTriangleChernCondition_of_conditions hc)).1 z₁ p +
          (D.withZeroObject E₃ h₃ z₃).localizedPowerSum
            (hasDefinedChernClasses_triangle_of_mor₃ D.base D.a h₁ h₂ h₃ hT
              (hasTriangleChernCondition_of_conditions hc)).2.2 z₃ p) ∧
      ∀ p : ℕ,
        (D.withZeroObject E₂ h₂ (D.isZero_restrict_obj₂ a b c hT z₁ z₃)).localizedChernChar
            (hasDefinedChernClasses_triangle_of_mor₃ D.base D.a h₁ h₂ h₃ hT
              (hasTriangleChernCondition_of_conditions hc)).2.1
            (D.isZero_restrict_obj₂ a b c hT z₁ z₃) p =
          (D.withZeroObject E₁ h₁ z₁).localizedChernChar
              (hasDefinedChernClasses_triangle_of_mor₃ D.base D.a h₁ h₂ h₃ hT
                (hasTriangleChernCondition_of_conditions hc)).1 z₁ p +
            (D.withZeroObject E₃ h₃ z₃).localizedChernChar
              (hasDefinedChernClasses_triangle_of_mor₃ D.base D.a h₁ h₂ h₃ hT
                (hasTriangleChernCondition_of_conditions hc)).2.2 z₃ p

Tag 0FBF, a lemma

Tag 0FBF in the Stacks Project.

Stacks.Chow.LocalizedSituation.localizedPowerSum_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedDerivedTensor.lean, line 157. The attribute's comment: “the formula for P_p(Z_1 cap Z_2 -> X, F_1 tensor^L F_2), with Z_1 cap Z_2 = Z_1 x_X Z_2 and the products those of 0FE5 (supportedIntersectionMul). The source leaves implicit in which sense F_1 tensor^L F_2 satisfies (3) of 0GUJ in the mixed cases ((c) for one factor and (d) for the other, or (d) for both with different X'); the classes of F_1 tensor^L F_2 are those of Remark 0GUK, defined for every perfect object with defined Chern classes, which covers them.”.

The localized power sums of a derived tensor product. In Situation 02QL let X be locally of finite type over S, let Z₁, Z₂ ⊆ X be closed subschemes and let F₁, F₂ ∈ D(𝒪_X) be perfect with F_i|_{X ∖ Z_i} zero and satisfying condition (3) of Situation 0GUJ. Then

P_p(Z₁ ∩ Z₂ ⟶ X, F₁ ⊗^L F₂) = ∑_{p₁ + p₂ = p} C(p, p₁) P_{p₁}(Z₁ ⟶ X, F₁) P_{p₂}(Z₂ ⟶ X, F₂)

in A^p(Z₁ ∩ Z₂ ⟶ X), the class of F₁ ⊗^L F₂ being that of Remark 0GUK; the source leaves implicit in which sense F₁ ⊗^L F₂ satisfies condition (3) in the mixed cases of alternatives (c) and (d), which the classes of Remark 0GUK cover.

theorem localizedPowerSum_derivedTensor (p : ℕ) :
    (LocalizedChernData.derivedTensorOfIsZero C a i₁ i₂ hF₁ hF₂ h₁ h₂ 0).localizedPowerSum
        (hasDefinedChernClasses_derivedTensor
          (ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 0).hasDefinedChernClasses_E
          (ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 0).hasDefinedChernClasses_E)
        (isZero_derivedTensor_compl_pullback i₁ i₂ hF₁ hF₂ h₁ h₂) p =
      ∑ q ∈ (antidiagonal p).attach, (p.choose q.1.1 : ℤ) •
        bivariantClassDegreeCongr C _ _ _ _ rfl (by have := mem_antidiagonal.1 q.2; omega)
          (supportedIntersectionMul C a i₁ i₂ (IsPullback.of_hasPullback i₁ i₂) _ rfl
            ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 0).localizedPowerSum h₁ q.1.1)
            ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 0).localizedPowerSum h₂ q.1.2))

Stacks.Chow.LocalizedSituation.localizedChern_one_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedDerivedTensor.lean, line 187. The attribute's comment: “the formula for c_1(Z_1 cap Z_2 -> X, F_1 tensor^L F_2), r_i = P_0(Z_i -> X, F_i); the product r_2 c_1(Z_1 -> X, F_1) is taken for Z_1 cap Z_2 presented as Z_2 x_X Z_1 through the flipped square. The source leaves implicit in which sense F_1 tensor^L F_2 satisfies (3) of 0GUJ in the mixed cases ((c) for one factor and (d) for the other, or (d) for both with different X'); the classes of F_1 tensor^L F_2 are those of Remark 0GUK, defined for every perfect object with defined Chern classes, which covers them.”.

The first localized Chern class of a derived tensor product. In the situation of Stacks.Chow.LocalizedSituation.localizedPowerSum_derivedTensor, with r_i = P_0(Z_i ⟶ X, F_i),

c_1(Z₁ ∩ Z₂ ⟶ X, F₁ ⊗^L F₂) = r₁ c_1(Z₂ ⟶ X, F₂) + r₂ c_1(Z₁ ⟶ X, F₁)

in A^1(Z₁ ∩ Z₂ ⟶ X), the class of F₁ ⊗^L F₂ being that of Remark 0GUK.

theorem localizedChern_one_derivedTensor :
    (LocalizedChernData.derivedTensorOfIsZero C a i₁ i₂ hF₁ hF₂ h₁ h₂ 1).localizedChern
        (hasDefinedChernClasses_derivedTensor
          (ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 0).hasDefinedChernClasses_E
          (ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 0).hasDefinedChernClasses_E)
        (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _
          (isZero_derivedTensor_compl_pullback i₁ i₂ hF₁ hF₂ h₁ h₂) one_pos) =
      bivariantClassDegreeCongr C _ _ _ _ rfl (by norm_num)
          (supportedIntersectionMul C a i₁ i₂ (IsPullback.of_hasPullback i₁ i₂) _ rfl
            ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 0).localizedPowerSum h₁ 0)
            ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 1).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₂
                one_pos))) +
        bivariantClassDegreeCongr C _ _ _ _ rfl (by norm_num)
          (supportedIntersectionMul C a i₂ i₁ (IsPullback.of_hasPullback i₁ i₂).flip _
            pullback.condition
            ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 0).localizedPowerSum h₂ 0)
            ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 1).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₁
                one_pos)))

Stacks.Chow.LocalizedSituation.localizedChern_two_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedDerivedTensor.lean, line 237. The attribute's comment: “the formula for c_2(Z_1 cap Z_2 -> X, F_1 tensor^L F_2); the squares are the products res(c) o c of 0FA0 (supportedMul), C(r_i, 2) is the class of x |-> C(chi_{F_i}(x), 2) (LocalizedChernData.rankChoose), and (r_1 r_2 - 1) c c' is read as (r_1 r_2)(c c') - c c'. The source's 'and so on for higher Chern classes' is not formalized. The source leaves implicit in which sense F_1 tensor^L F_2 satisfies (3) of 0GUJ in the mixed cases ((c) for one factor and (d) for the other, or (d) for both with different X'); the classes of F_1 tensor^L F_2 are those of Remark 0GUK, defined for every perfect object with defined Chern classes, which covers them.”.

The second localized Chern class of a derived tensor product. In the situation of Stacks.Chow.LocalizedSituation.localizedPowerSum_derivedTensor, with r_i = P_0(Z_i ⟶ X, F_i), γ_{i,p} = c_p(Z_i ⟶ X, F_i) and C(r_i, 2) the class Stacks.Chow.LocalizedChernData.rankChoose,

c\_2(Z₁ ∩ Z₂ ⟶ X, F₁ ⊗^L F₂) = r₁ γ\_\{2,2} + r₂ γ\_\{1,2} + C(r₁, 2) γ\_\{2,1}² + ((r₁ r₂) (γ\_\{2,1} γ\_\{1,1}) - γ\_\{2,1} γ\_\{1,1}) + C(r₂, 2) γ\_\{1,1}²

in A^2(Z₁ ∩ Z₂ ⟶ X), the class of F₁ ⊗^L F₂ being that of Remark 0GUK. The products of a class supported on Z₂ with one supported on Z₁ are taken for Z₁ ∩ Z₂ presented as Z₂ ×_X Z₁ through the flipped square, and the squares are the products of Stacks.Chow.supportedMul.

theorem localizedChern_two_derivedTensor :
    (LocalizedChernData.derivedTensorOfIsZero C a i₁ i₂ hF₁ hF₂ h₁ h₂ 2).localizedChern
        (hasDefinedChernClasses_derivedTensor
          (ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 0).hasDefinedChernClasses_E
          (ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 0).hasDefinedChernClasses_E)
        (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _
          (isZero_derivedTensor_compl_pullback i₁ i₂ hF₁ hF₂ h₁ h₂) two_pos) =
      bivariantClassDegreeCongr C _ _ _ _ rfl (by norm_num)
          (supportedIntersectionMul C a i₁ i₂ (IsPullback.of_hasPullback i₁ i₂) _ rfl
            ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 0).localizedPowerSum h₁ 0)
            ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 2).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₂
                two_pos))) +
        bivariantClassDegreeCongr C _ _ _ _ rfl (by norm_num)
          (supportedIntersectionMul C a i₂ i₁ (IsPullback.of_hasPullback i₁ i₂).flip _
            pullback.condition
            ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 0).localizedPowerSum h₂ 0)
            ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 2).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₁
                two_pos))) +
        bivariantClassDegreeCongr C _ _ _ _ rfl (by norm_num)
          (supportedIntersectionMul C a i₁ i₂ (IsPullback.of_hasPullback i₁ i₂) _ rfl
            ((LocalizedChernData.ofIsZero C a i₁ F₁ hF₁ h₁ 0).rankChoose h₁ 2 two_pos)
            (supportedMul C (i₂ ≫ a) a i₂ rfl ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 1).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₂
                one_pos))
              ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 1).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₂
                one_pos)))) +
        (bivariantClassDegreeCongr C _ _ _ _ rfl (by norm_num)
            (supportedMul C ((pullback.snd i₁ i₂ ≫ i₂) ≫ a) a (pullback.snd i₁ i₂ ≫ i₂) rfl
              (supportedIntersectionMul C a i₁ i₂ (IsPullback.of_hasPullback i₁ i₂) _ rfl
                ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 0).localizedPowerSum h₁ 0)
                ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 0).localizedPowerSum h₂ 0))
              (supportedIntersectionMul C a i₂ i₁ (IsPullback.of_hasPullback i₁ i₂).flip _
            pullback.condition
                ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 1).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₂
                one_pos))
                ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 1).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₁
                one_pos)))) -
          bivariantClassDegreeCongr C _ _ _ _ rfl (by norm_num)
            (supportedIntersectionMul C a i₂ i₁ (IsPullback.of_hasPullback i₁ i₂).flip _
            pullback.condition
              ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 1).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₂
                one_pos))
              ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 1).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₁
                one_pos)))) +
        bivariantClassDegreeCongr C _ _ _ _ rfl (by norm_num)
          (supportedIntersectionMul C a i₂ i₁ (IsPullback.of_hasPullback i₁ i₂).flip _
            pullback.condition
            ((LocalizedChernData.ofIsZero C a i₂ F₂ hF₂ h₂ 0).rankChoose h₂ 2 two_pos)
            (supportedMul C (i₁ ≫ a) a i₁ rfl ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 1).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₁
                one_pos))
              ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 1).localizedChern
              (LocalizedChernData.isFiniteLocallyFreeOfRankLTOnComplement_ofIsZero C a _ _ _ h₁
                one_pos))))

Stacks.Chow.LocalizedSituation.localizedChernChar_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedDerivedTensor.lean, line 328. The attribute's comment: “the formula ch(Z_1 cap Z_2 -> X, F_1 tensor^L F_2) = ch(Z_1 -> X, F_1) ch(Z_2 -> X, F_2), read degree by degree in prod_p A^p(Z_1 cap Z_2 -> X) tensor Q. The source leaves implicit in which sense F_1 tensor^L F_2 satisfies (3) of 0GUJ in the mixed cases ((c) for one factor and (d) for the other, or (d) for both with different X'); the classes of F_1 tensor^L F_2 are those of Remark 0GUK, defined for every perfect object with defined Chern classes, which covers them.”.

The localized Chern character of a derived tensor product. In the situation of Stacks.Chow.LocalizedSituation.localizedPowerSum_derivedTensor,

ch(Z₁ ∩ Z₂ ⟶ X, F₁ ⊗^L F₂) = ch(Z₁ ⟶ X, F₁) ch(Z₂ ⟶ X, F₂)

in ∏_p A^p(Z₁ ∩ Z₂ ⟶ X) ⊗ 𝐐, read in each degree p: the component of degree p of the left side is ∑_{p₁ + p₂ = p} ch_{p₁}(Z₁ ⟶ X, F₁) ch_{p₂}(Z₂ ⟶ X, F₂), the degree p component of the product, with the products of Stacks.Chow.rationalSupportedIntersectionMul. The Chern character of F₁ ⊗^L F₂ is that of Remark 0GUK.

theorem localizedChernChar_derivedTensor (p : ℕ) :
    (LocalizedChernData.derivedTensorOfIsZero C a i₁ i₂ hF₁ hF₂ h₁ h₂ 0).localizedChernChar
        (hasDefinedChernClasses_derivedTensor
          (ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 0).hasDefinedChernClasses_E
          (ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 0).hasDefinedChernClasses_E)
        (isZero_derivedTensor_compl_pullback i₁ i₂ hF₁ hF₂ h₁ h₂) p =
      ∑ q ∈ (antidiagonal p).attach,
        rationalBivariantClassDegreeCongr C _ _ _ _ rfl (by have := mem_antidiagonal.1 q.2; omega)
          (rationalSupportedIntersectionMul C a i₁ i₂ (IsPullback.of_hasPullback i₁ i₂) _ rfl
            ((ofIsZero C a i₁ F₁ hF₁ h₁ hfin₁ 0).localizedChernChar h₁ q.1.1)
            ((ofIsZero C a i₂ F₂ hF₂ h₂ hfin₂ 0).localizedChernChar h₂ q.1.2))

Sources

LeanStacks.Chow.LocalizedSituation.localizedPowerSum_succ · Stacks.Chow.LocalizedSituation.nonhomogeneousBivariantTransport_compositeOfInvertible_localizedPowerSum · Stacks.Chow.LocalizedSituation.nonhomogeneousBivariantTransport_compositeOfInvertible_localizedChern · Stacks.Chow.totalLocalizedChernClass · Stacks.Chow.totalLocalizedChernClass_fst_of_nonneg · Stacks.Chow.totalLocalizedChernClass_fst_of_neg · Stacks.Chow.totalLocalizedChernClass_snd · Stacks.Chow.LocalizedChernData.totalLocalizedChernClass

Section42.53 Blowing up at infinity #

Section 42.53 of the Stacks Project, Tag 0FBG. 3 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FBG, the section

Tag 0FBG in the Stacks Project.

Stacks.Chow.blowupAtInfinity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 220. The attribute's comment: “the scheme W, the blowup of 𝐏¹_X in the centre ∞(Z)”.

The deformation space W of Stacks 0FBG: the blowup of 𝐏¹_X in the centre ∞(Z).

def blowupAtInfinity : Scheme.{u}

Stacks.Chow.blowupAtInfinityToLine, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 225. The attribute's comment: “the structure morphism b : W ⟶ 𝐏¹_X of the blowup at infinity”.

The structure morphism b : W ⟶ 𝐏¹_X of the blowup at infinity.

def blowupAtInfinityToLine : blowupAtInfinity ℐ ⟶ relativeProjectiveLine X

Stacks.Chow.exceptionalIdealAtInfinity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 235. The attribute's comment: “the exceptional divisor E ⊆ W of the blowup at infinity”.

The ideal of the exceptional divisor E ⊆ W: the inverse image of the centre ∞(Z) along b.

def exceptionalIdealAtInfinity : (blowupAtInfinity ℐ).IdealSheafData

Stacks.Chow.fibreIdealAtInfinity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 241. The attribute's comment: “the fibre at infinity W_∞ ⊆ W, the inverse image of (𝐏¹_X)_∞ under b”.

The ideal of the fibre at infinity W_∞ ⊆ W: the inverse image along b of the divisor at infinity (𝐏¹_X)_∞.

def fibreIdealAtInfinity : (blowupAtInfinity ℐ).IdealSheafData

Stacks.Chow.fibreIdealAtInfinity_le_exceptionalIdealAtInfinity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 252. The attribute's comment: “E ⊆ W_∞ as closed subschemes of W”.

E is contained in W_∞: the centre ∞(Z) contains the divisor at infinity, so its inverse image along b does too.

theorem fibreIdealAtInfinity_le_exceptionalIdealAtInfinity :
    fibreIdealAtInfinity ℐ ≤ exceptionalIdealAtInfinity ℐ

Stacks.Chow.isEffectiveCartierDivisor_fibreIdealAtInfinity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 261. The attribute's comment: “W_∞ is an effective Cartier divisor on W”.

The fibre at infinity W_∞ is an effective Cartier divisor on W: the divisor at infinity of 𝐏¹_X is one, and the inverse image of an effective Cartier divisor under a blowup is again one.

theorem isEffectiveCartierDivisor_fibreIdealAtInfinity :
    Stacks.Divisors.IsEffectiveCartierDivisor (fibreIdealAtInfinity ℐ)

Stacks.Chow.exists_isEffectiveCartierDivisor_fibreIdealAtInfinity_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 271. The attribute's comment: “W_∞ is the sum of E and a second effective Cartier divisor on W”.

The fibre at infinity decomposes as W_∞ = D + E. Both E and W_∞ are effective Cartier divisors on W and E ⊆ W_∞, so W_∞ is the sum of E and a third effective Cartier divisor D, written in the ideal-sheaf presentation ℐ_{W_∞} = ℐ_E · ℐ_D. That D is the divisor X' is Stacks.Chow.eq_strictTransformIdealAtInfinity_of_mul_eq.

theorem exists_isEffectiveCartierDivisor_fibreIdealAtInfinity_eq :
    ∃ D : (blowupAtInfinity ℐ).IdealSheafData,
      Stacks.Divisors.IsEffectiveCartierDivisor D ∧
        fibreIdealAtInfinity ℐ = exceptionalIdealAtInfinity ℐ * D

Stacks.Chow.blowUpToBlowupAtInfinity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 295. The attribute's comment: “the closed immersion X' ⟶ W of the square, X' the blowup of X in Z”.

The closed immersion X' ⟶ W of the commutative square of Stacks 0FBG: the blowup X' of X in Z is the classifying morphism of X' ⟶ X ⟶ 𝐏¹_X for the centre ∞(Z).

def blowUpToBlowupAtInfinity : blowUp ℐ ⟶ blowupAtInfinity ℐ

Stacks.Chow.blowUpToBlowupAtInfinity_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 309. The attribute's comment: “commutativity of the square X' ⟶ W ⟶ 𝐏¹_X = X' ⟶ X ⟶ 𝐏¹_X”.

The square of Stacks 0FBG commutes: X' ⟶ W ⟶ 𝐏¹_X equals X' ⟶ X ⟶ 𝐏¹_X.

theorem blowUpToBlowupAtInfinity_comp :
    blowUpToBlowupAtInfinity ℐ ≫ blowupAtInfinityToLine ℐ =
      blowUpToBase ℐ ≫ lineInfinitySection X

Stacks.Chow.comap_exceptionalIdealAtInfinity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 325. The attribute's comment: “(3): X' ∩ E is the exceptional divisor of X' ⟶ X”.

Stacks 0FBG, assertion (3). The inverse image of the exceptional divisor E ⊆ W on X' is the exceptional divisor of the blowup X' ⟶ X of X in Z; that is, X' ∩ E is the exceptional divisor of X' ⟶ X.

theorem comap_exceptionalIdealAtInfinity :
    (exceptionalIdealAtInfinity ℐ).comap (blowUpToBlowupAtInfinity ℐ) = exceptionalIdeal ℐ

Stacks.Chow.lineToBlowupAtInfinity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 370. The attribute's comment: “(8): the closed immersion 𝐏¹_Z ⟶ W”.

Stacks 0FBG, assertion (8), the morphism. The closed immersion 𝐏¹_Z ⟶ W: the classifying morphism for the centre ∞(Z) of the inclusion 𝐏¹_Z ⟶ 𝐏¹_X, along which ∞(Z) pulls back to the divisor at infinity of 𝐏¹_Z.

def lineToBlowupAtInfinity :
    relativeProjectiveLine ℐ.subscheme ⟶ blowupAtInfinity ℐ

Stacks.Chow.lineToBlowupAtInfinity_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 383. The attribute's comment: “(8): the composite of 𝐏¹_Z ⟶ W with b is the inclusion 𝐏¹_Z ⟶ 𝐏¹_X”.

Stacks 0FBG, assertion (8), the triangle. The composite of 𝐏¹_Z ⟶ W with b is the inclusion morphism 𝐏¹_Z ⟶ 𝐏¹_X.

theorem lineToBlowupAtInfinity_comp :
    lineToBlowupAtInfinity ℐ ≫ blowupAtInfinityToLine ℐ =
      projectiveLineBaseChange ℐ.subschemeι

Stacks.Chow.isIso_blowupAtInfinityToLine_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreBlowup.lean, line 421. The attribute's comment: “(1): b is an isomorphism over 𝐀¹_X ∪ 𝐏¹_{X ∖ Z}”.

Stacks 0FBG, assertion (1). The blowup at infinity is an isomorphism over 𝐀¹_X ∪ 𝐏¹_{X ∖ Z}: that open misses the centre, and a blowup is an isomorphism over the complement of its centre.

theorem isIso_blowupAtInfinityToLine_restrict :
    IsIso (blowupAtInfinityToLine ℐ ∣_ isomorphismLocusAtInfinity ℐ)

Stacks.Chow.fibreIdealAtInfinity_eq_mul_strictTransformIdealAtInfinity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreDivisor.lean, line 524. The attribute's comment: “(4): W_∞ = X' + E as effective Cartier divisors on W”.

W_∞ = X' + E as effective Cartier divisors on W, in the ideal-sheaf presentation ℐ_{W_∞} = ℐ_E · ℐ_{X'}.

theorem fibreIdealAtInfinity_eq_mul_strictTransformIdealAtInfinity :
    fibreIdealAtInfinity ℐ =
      exceptionalIdealAtInfinity ℐ * strictTransformIdealAtInfinity ℐ

Stacks.Chow.isEffectiveCartierDivisor_strictTransformIdealAtInfinity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreDivisor.lean, line 532. The attribute's comment: “(2): X' is an effective Cartier divisor on W”.

The strict transform X' is an effective Cartier divisor on W.

theorem isEffectiveCartierDivisor_strictTransformIdealAtInfinity :
    Stacks.Divisors.IsEffectiveCartierDivisor (strictTransformIdealAtInfinity ℐ)

Stacks.Conormal.projectivizedNormalCone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/ProjectivizedNormalCone.lean, line 84. The attribute's comment: “the scheme Proj_Z(C_{Z/X,*}) of clause (6), as a relative Proj over Z”.

The projectivized normal cone P_ZX = Proj_Z(𝒞_{Z/X,*}) of an immersion i : Z ⟶ X: the relative Proj over Z of the conormal algebra. This is the scheme appearing in clause (6) of [Stacks, Tag 0FBG].

def projectivizedNormalCone : Scheme.{u}

Tag 0FBH, an item

Tag 0FBH in the Stacks Project.

Stacks.Chow.support_compl_strictTransformIdealOnExceptional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreNormalCone.lean, line 110. The attribute's comment: “E ∖ (X' ∩ E) = E ∖ X' as open subschemes of E”.

The open subscheme E ∖ (X' ∩ E) of the exceptional divisor is the inverse image of the open W ∖ X', so E ∖ (X' ∩ E) = E ∖ X'.

theorem support_compl_strictTransformIdealOnExceptional :
    (strictTransformIdealOnExceptional ℐ).support.compl =
      (exceptionalIdealAtInfinity ℐ).subschemeι ⁻¹ᵁ
        (strictTransformIdealAtInfinity ℐ).support.compl

Stacks.Chow.mem_pow_infinityChartIdeal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreNormalCone.lean, line 229. The attribute's comment: “the powers of J = (I, s): the coefficient of s^j lies in I^(m-j)”.

The powers of J = (I, s). A polynomial lies in Jᵐ exactly when its coefficient of sʲ lies in I^(m - j) for every j, so Jᵐ = Iᵐ ⊕ sI^(m-1) ⊕ ⋯ ⊕ sᵐA ⊕ s^(m+1)A ⊕ ⋯.

theorem mem_pow_infinityChartIdeal_iff {I : Ideal A} {m : ℕ} {f : A[X]} :
    f ∈ infinityChartIdeal I ^ m ↔ ∀ j, f.coeff j ∈ I ^ (m - j)

Stacks.Chow.infinityChartMk_mem_fibreIdeal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreNormalCone.lean, line 386. The attribute's comment: “on D₊(S) the ideal (s) consists of the fractions p/s^N with p in J^(N+1)”.

s cuts the chart down to the associated graded ring. The fraction p/sᴺ on the chart A[s][J/s] is divisible by s exactly when p lies in J^(N+1).

theorem infinityChartMk_mem_fibreIdeal_iff {I : Ideal A} {N : ℕ} {q : A[X]}
    (hq : q ∈ infinityChartIdeal I ^ N) :
    infinityChartMk I N q hq ∈ infinityChartFibreIdeal I ↔
      q ∈ infinityChartIdeal I ^ (N + 1)

Stacks.Chow.conormalEquivInfinityChartFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreNormalCone.lean, line 738. The attribute's comment: “the quotient of A[s][J/s] by s is the conormal algebra of I in A”.

The quotient of the affine blowup algebra A[s][J/s], J = (I, s), by the element s cutting out the exceptional divisor is the conormal algebra A/I ⊕ I/I² ⊕ I²/I³ ⊕ ⋯ of I in A.

def conormalEquivInfinityChartFibre (I : Ideal A) :
    AssociatedGraded.gradedRing I ≃+*
      (infinityChartAlgebra I ⧸ infinityChartFibreIdeal I)

Stacks.Chow.normalConeToExceptionalDivisor_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreNormalConeIso.lean, line 811. The attribute's comment: “E ∖ X' = E ∖ (X' ∩ E) = Spec_Z(C_{Z/X,*}) = C_ZX: an open immersion C_ZX → E with image E ∖ (X' ∩ E) = E ∖ X', over X”.

Let Z ⊆ X be the closed subscheme of a quasi-coherent ideal i.ker, let W be the blowup of 𝐏¹_X in ∞(Z), with exceptional divisor E and strict transform X' of X. Then

E ∖ X' = E ∖ (X' ∩ E) = Spec_Z(𝒞_{Z/X,*}) = C_ZX:

the morphism normalConeToExceptionalDivisor : C_ZX ⟶ E is an open immersion whose image is E ∖ (X' ∩ E), which is the inverse image E ∖ X' of W ∖ X', and it is a morphism over X (so the identification is one of schemes over Z).

theorem normalConeToExceptionalDivisor_spec :
    IsOpenImmersion (normalConeToExceptionalDivisor i) ∧
      (normalConeToExceptionalDivisor i).opensRange =
        (strictTransformIdealOnExceptional i.ker).support.compl ∧
      (strictTransformIdealOnExceptional i.ker).support.compl =
        (exceptionalIdealAtInfinity i.ker).subschemeι ⁻¹ᵁ
          (strictTransformIdealAtInfinity i.ker).support.compl ∧
      normalConeToExceptionalDivisor i ≫ (exceptionalIdealAtInfinity i.ker).subschemeι ≫
          blowupAtInfinityToBase i.ker =
        Stacks.Conormal.normalConeToBase i ≫ i

Stacks.Chow.normalConeToFibreAtInfinity_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreNormalConeIso.lean, line 872. The attribute's comment: “the open immersion j : C_ZX → W_∞ of 0FBK: image W_∞ ∖ X', through E, over X”.

The morphism j : C_ZX ⟶ W_∞ of Stacks 0FBK is an open immersion with image W_∞ ∖ X', it factors through the exceptional divisor as C_ZX ≅ E ∖ X' ⊆ E, and it lies over X: C_ZX ⟶ W_∞ ⟶ X is C_ZX ⟶ Z ⟶ X.

theorem normalConeToFibreAtInfinity_spec :
    IsOpenImmersion (normalConeToFibreAtInfinity i f) ∧
      (normalConeToFibreAtInfinity i f).opensRange =
        modificationFibreAtInfinityComplStrictTransform i.ker f ∧
      normalConeToFibreAtInfinity i f ≫
          modificationInclusionAtInfinity f (blowupAtInfinityToProjectiveLineProduct i.ker f) =
        normalConeToExceptionalDivisor i ≫ (exceptionalIdealAtInfinity i.ker).subschemeι ∧
      normalConeToFibreAtInfinity i f ≫
          modificationProjectionAtInfinity f (blowupAtInfinityToProjectiveLineProduct i.ker f) =
        Stacks.Conormal.normalConeToBase i ≫ i

Tag 0FE9, an item

Tag 0FE9 in the Stacks Project.

Stacks.Chow.lineToBlowupAtInfinity_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/InfinityCentreLineAtInfinity.lean, line 233. The attribute's comment: “a closed immersion P¹_Z → W over P¹_X whose base change by ∞ is Z → C_ZX → E → W_∞, the first arrow the vertex of the cone”.

Let Z ⊆ X be the closed subscheme of the closed immersion i, let b : W ⟶ 𝐏¹_X be the blowup of 𝐏¹_X in ∞(Z), with exceptional divisor E and fibre at infinity W_∞. Then lineToBlowupAtInfinity : 𝐏¹_Z ⟶ W is a closed immersion, its composite with b is the inclusion 𝐏¹_Z ⟶ 𝐏¹_X, and its base change by ∞ (along W_∞ ⟶ W, with (𝐏¹_Z)_∞ = Z) is the composite Z ⟶ C_ZX ⟶ E ⟶ W_∞ of the vertex of the normal cone, the open immersion C_ZX ⟶ E and the inclusion E ⊆ W_∞.

theorem lineToBlowupAtInfinity_spec :
    IsClosedImmersion (lineToBlowupAtInfinity i.ker) ∧
      lineToBlowupAtInfinity i.ker ≫ blowupAtInfinityToLine i.ker =
        projectiveLineBaseChange i.ker.subschemeι ∧
      IsPullback (i.toImage ≫ lineInfinitySection i.ker.subscheme)
        (normalConeZeroSection i ≫ normalConeToExceptionalDivisor i ≫
          Scheme.IdealSheafData.inclusion
            (fibreIdealAtInfinity_le_exceptionalIdealAtInfinity i.ker))
        (lineToBlowupAtInfinity i.ker) (fibreIdealAtInfinity i.ker).subschemeι

Sources

LeanStacks.Chow.blowupAtInfinity · Stacks.Chow.blowupAtInfinityToLine · Stacks.Chow.exceptionalIdealAtInfinity · Stacks.Chow.fibreIdealAtInfinity · Stacks.Chow.fibreIdealAtInfinity_le_exceptionalIdealAtInfinity · Stacks.Chow.isEffectiveCartierDivisor_fibreIdealAtInfinity · Stacks.Chow.exists_isEffectiveCartierDivisor_fibreIdealAtInfinity_eq · Stacks.Chow.blowUpToBlowupAtInfinity

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

42.48 Gysin at infinity to 42.53 Blowing up at infinity

Section42.48 Gysin at infinity#

Tag 0F9J, a lemma

Tag 0GUH, a lemma

Tag 0FAQ, a lemma

Tag 0FAR, a lemma

Tag 0FAS, a lemma

Sources

Section42.49 Preparation for localized Chern classes#

Tag 0F9K, a lemma

Tag 0GUI, a lemma

Tag 0FAU, a lemma

Tag 0FAV, a lemma

Tag 0FAW, a lemma

Tag 0FAX, a lemma

Tag 0FAY, a lemma

Tag 0FAZ, a lemma

Sources

Section42.50 Localized Chern classes#

Tag 0GUJ, a situation

Tag 0FB2, a lemma

Tag 0FB5, a definition

Tag 0FB3, a lemma

Tag 0GUK, a remark

Tag 0FB4, a lemma

Tag 0FB6, a lemma

Tag 0FB7, a lemma

Tag 0FB8, a lemma

Sources

Section42.51 Two technical lemmas#

Tag 0FE7, a lemma

Tag 0FE8, a lemma

Sources

Section42.52 Properties of localized Chern classes#

Tag 0FBA, a lemma

Tag 0FBB, a lemma

Tag 0FBC, a remark

Tag 0FBD, a lemma

Tag 0FBE, a lemma

Tag 0FBF, a lemma

Sources

Section42.53 Blowing up at infinity#

Tag 0FBG, the section

Tag 0FBH, an item

Tag 0FE9, an item

Sources

Section42.48 Gysin at infinity #

Section42.49 Preparation for localized Chern classes #

Section42.50 Localized Chern classes #

Section42.51 Two technical lemmas #

Section42.52 Properties of localized Chern classes #

Section42.53 Blowing up at infinity #