42.31 Relative effective… to 42.34 Chow cohomology and the…

Section42.31 Relative effective Cartier divisors #

Section 42.31 of the Stacks Project, Tag 02TP. 1 tag here is carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02TR, a lemma

Tag 02TR in the Stacks Project.

Stacks.Chow.gysinChowOfInvertible_canonicalSection_flatPullbackChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierChow.lean, line 190. The attribute's comment: “first equality i^ p^ α = (p|_D)^* α, for p of relative dimension r + 1 (relative dimension 0 is gysinChowOfInvertible_canonicalSection_flatPullbackChow_of_relativeDimension_zero)”.

Stacks 02TR, first equality. Let p : X ⟶ Y be flat of relative dimension r + 1 between schemes locally of finite type over the base, let i : D ⟶ X be a relative effective Cartier divisor on X/Y and let i^* be the Gysin map of the canonical section of 𝒪_X(D), whose zero scheme is D (Stacks 01X0). Then p|_D is flat of relative dimension r and

i^* p^* α = (p|_D)^* α in CH_{k+1+r}(D) for every α ∈ CH_{k+1}(Y).

theorem gysinChowOfInvertible_canonicalSection_flatPullbackChow (r : ℕ)
    (hp : AlgebraicGeometry.RelativeDimension p (r + 1)) (α : chowGroup C sY (k + 1)) :
    haveI : Stacks.Divisors.IsEffectiveCartierDivisor D := hD.1
    haveI : Flat (D.subschemeι ≫ p) := hD.2
    zeroScheme_divisorSheafGlobalSection D ▸
      gysinChowOfInvertible C sX (k + 1 + (r : ℤ)) (Stacks.Divisors.divisorSheaf D)
        (Stacks.Divisors.divisorSheafGlobalSection D)
        (chowGroupCast C sX (degree_flatPullback_succ k r)
          (flatPullbackChowOfRelativeDimension C sX sY p hbase (r + 1) hp (k + 1) α)) =
      flatPullbackChowOfRelativeDimension C (D.subschemeι ≫ sX) sY (D.subschemeι ≫ p)
        (by rw [Category.assoc, hbase]) r
        (Stacks.Divisors.relativeDimension_subschemeι_comp_of_isRelativeEffectiveCartierDivisor
          p r hp D hD) (k + 1) α

Stacks.Chow.firstChernClassCapChow_divisorSheaf_flatPullbackChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierChow.lean, line 238. The attribute's comment: “second equality c_1(O_X(D)) ∩ p^ α = i_((p|_D)^* α), for p of relative dimension r + 1 (relative dimension 0 is firstChernClassCapChow_divisorSheaf_flatPullbackChow_of_relativeDimension_zero)”.

Stacks 02TR, second equality. In the situation of Stacks.Chow.gysinChowOfInvertible_canonicalSection_flatPullbackChow, with ℒ = 𝒪_X(D),

c₁(ℒ) ∩ p^* α = i_*((p|_D)^* α) in CH_{k+1+r}(X) for every α ∈ CH_{k+1}(Y).

theorem firstChernClassCapChow_divisorSheaf_flatPullbackChow (r : ℕ)
    (hp : AlgebraicGeometry.RelativeDimension p (r + 1)) (α : chowGroup C sY (k + 1)) :
    haveI : Stacks.Divisors.IsEffectiveCartierDivisor D := hD.1
    haveI : Flat (D.subschemeι ≫ p) := hD.2
    firstChernClassCapChow C (k + 1 + (r : ℤ)) sX (Stacks.Divisors.divisorSheaf D)
        (chowGroupCast C sX (degree_flatPullback_succ k r)
          (flatPullbackChowOfRelativeDimension C sX sY p hbase (r + 1) hp (k + 1) α)) =
      properChowPushforward C (D.subschemeι ≫ sX) sX D.subschemeι rfl (k + 1 + (r : ℤ))
        (properPushforwardFactorsThroughRationalEquivalence_of_isProper C _ sX _ rfl _)
        (flatPullbackChowOfRelativeDimension C (D.subschemeι ≫ sX) sY (D.subschemeι ≫ p)
          (by rw [Category.assoc, hbase]) r
          (Stacks.Divisors.relativeDimension_subschemeι_comp_of_isRelativeEffectiveCartierDivisor
            p r hp D hD) (k + 1) α)

Stacks.Chow.gysinChowOfInvertible_canonicalSection_flatPullbackChow_of_relativeDimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierChow.lean, line 272. The attribute's comment: “first equality, for p of relative dimension 0: D is empty, so CH_k(D) = 0 and i^ p^ α = 0”.

Stacks 02TR in relative dimension zero, first equality. If p has relative dimension 0 then a relative effective Cartier divisor D on X/Y is empty, so CH_k(D) = 0 and i^* p^* α = 0 for every α ∈ CH_{k+1}(Y).

theorem gysinChowOfInvertible_canonicalSection_flatPullbackChow_of_relativeDimension_zero
    (hp : AlgebraicGeometry.RelativeDimension p 0) (α : chowGroup C sY (k + 1)) :
    haveI : Stacks.Divisors.IsEffectiveCartierDivisor D := hD.1
    (zeroScheme_divisorSheafGlobalSection D ▸
      gysinChowOfInvertible C sX k (Stacks.Divisors.divisorSheaf D)
        (Stacks.Divisors.divisorSheafGlobalSection D)
        (chowGroupCast C sX (show k + 1 + ((0 : ℕ) : ℤ) = k + 1 by simp)
          (flatPullbackChowOfRelativeDimension C sX sY p hbase 0 hp (k + 1) α)) :
        chowGroup C (D.subschemeι ≫ sX) k) = 0

Stacks.Chow.firstChernClassCapChow_divisorSheaf_flatPullbackChow_of_relativeDimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierChow.lean, line 289. The attribute's comment: “second equality, for p of relative dimension 0: D is empty, so c_1(O_X(D)) ∩ p^ α = i_(0) = 0”.

Stacks 02TR in relative dimension zero, second equality. If p has relative dimension 0 then a relative effective Cartier divisor D on X/Y is empty, so i_*((p|_D)^* α) = 0 and c₁(𝒪_X(D)) ∩ p^* α = 0 for every α ∈ CH_{k+1}(Y).

theorem firstChernClassCapChow_divisorSheaf_flatPullbackChow_of_relativeDimension_zero
    (hp : AlgebraicGeometry.RelativeDimension p 0) (α : chowGroup C sY (k + 1)) :
    haveI : Stacks.Divisors.IsEffectiveCartierDivisor D := hD.1
    firstChernClassCapChow C k sX (Stacks.Divisors.divisorSheaf D)
        (chowGroupCast C sX (show k + 1 + ((0 : ℕ) : ℤ) = k + 1 by simp)
          (flatPullbackChowOfRelativeDimension C sX sY p hbase 0 hp (k + 1) α)) = 0

Stacks.Chow.gysinHomomorphismOfInvertible_flatPullback_primeCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierFlatPullback.lean, line 179. The attribute's comment: “first equality, on the fundamental cycle of an integral closed subscheme”.

Stacks 02TR, first equality, on an integral component. Let p : X ⟶ Y be flat of relative dimension r + 1 over the base scheme of chapter 42, let i : D ⟶ X be a relative effective Cartier divisor on X/Y presented as the zero scheme of a section s of an invertible module L, and let W ⊆ Y be an integral closed subscheme of delta-dimension k + 1. Then

i^* p^* [W]_{k+1} = (p|_D)^* [W]_{k+1} in A_{k+1+r}(D).

The relative dimension hq of D ⟶ Y is a parameter; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.RelativeEffectiveCartierFlatPullback. The flatness of D ⟶ Y is both the second conjunct of hD and an instance binder, because stating (p|_D)^* needs it before hD is available.

theorem gysinHomomorphismOfInvertible_flatPullback_primeCycle
    (C : ChowSituation.{u}) {X Y : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (p : X ⟶ Y) [LocallyOfFiniteType p] [Flat p] (hbase : p ≫ sY = sX) (r : ℕ)
    (hp : AlgebraicGeometry.RelativeDimension p (r + 1)) (k : ℤ) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : L.sections)
    [Flat ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)]
    (hD : Stacks.Divisors.IsRelativeEffectiveCartierDivisor p
      (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))))
    (hq : AlgebraicGeometry.RelativeDimension
      ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p) r)
    (W : Y.IdealSheafData) (hWint : IsIntegral W.subscheme)
    (hWdim : schemeDeltaDimension C (W.subschemeι ≫ sY) = ((k + 1 : ℤ) : EInt))
    (hcast : k + 1 + ((r + 1 : ℕ) : ℤ) = k + 1 + (r : ℤ) + 1) :
    gysinHomomorphismOfInvertible C sX (k + 1 + (r : ℤ)) L (s.eval (.op ⊤))
        (hcast ▸ flatPullback C sX sY p hbase (r + 1) hp (k + 1)
          (cycleAssociatedToClosedSubscheme C sY W.subschemeι (k + 1))) =
      QuotientAddGroup.mk
        (flatPullback C
          ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sY
          ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)
          (by rw [Category.assoc, hbase]) r hq (k + 1)
          (cycleAssociatedToClosedSubscheme C sY W.subschemeι (k + 1)))

Stacks.Chow.effectiveCartierIntersectionOfInvertible_flatPullback_primeCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierFlatPullback.lean, line 242. The attribute's comment: “second equality, as intersection with D, on a fundamental cycle”.

Stacks 02TR, second equality, on an integral component, as intersection with D. In the situation of Stacks.Chow.gysinHomomorphismOfInvertible_flatPullback_primeCycle,

D · p^* [W]_{k+1} = i_* ((p|_D)^* [W]_{k+1}) in A_{k+1+r}(X),

where D · − is intersection with the effective Cartier divisor D (Stacks 02T8). The source writes the left side as c₁(ℒ) ∩ p^* α; that form is Stacks.Chow.firstChernClassCapOfInvertible_flatPullback_primeCycle below, one rewrite of this through Stacks 02T9.

theorem effectiveCartierIntersectionOfInvertible_flatPullback_primeCycle
    (C : ChowSituation.{u}) {X Y : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (p : X ⟶ Y) [LocallyOfFiniteType p] [Flat p] (hbase : p ≫ sY = sX) (r : ℕ)
    (hp : AlgebraicGeometry.RelativeDimension p (r + 1)) (k : ℤ) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : L.sections)
    [Flat ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)]
    (hD : Stacks.Divisors.IsRelativeEffectiveCartierDivisor p
      (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))))
    (hq : AlgebraicGeometry.RelativeDimension
      ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p) r)
    (W : Y.IdealSheafData) (hWint : IsIntegral W.subscheme)
    (hWdim : schemeDeltaDimension C (W.subschemeι ≫ sY) = ((k + 1 : ℤ) : EInt))
    (hcast : k + 1 + ((r + 1 : ℕ) : ℤ) = k + 1 + (r : ℤ) + 1) :
    effectiveCartierIntersectionOfInvertible C sX (k + 1 + (r : ℤ)) L (s.eval (.op ⊤)) hD.1
        (hcast ▸ flatPullback C sX sY p hbase (r + 1) hp (k + 1)
          (cycleAssociatedToClosedSubscheme C sY W.subschemeι (k + 1))) =
      properChowPushforward C
        ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sX
        (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι rfl (k + 1 + (r : ℤ))
        (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
          (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι C
          ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sX rfl
          (k + 1 + (r : ℤ)))
        (QuotientAddGroup.mk
          (flatPullback C
            ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sY
            ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)
            (by rw [Category.assoc, hbase]) r hq (k + 1)
            (cycleAssociatedToClosedSubscheme C sY W.subschemeι (k + 1))))

Stacks.Chow.firstChernClassCapOfInvertible_flatPullback_primeCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierFlatPullback.lean, line 290. The attribute's comment: “second equality, in the c₁(L) ∩ − form, on a fundamental cycle”.

Stacks 02TR, second equality, on an integral component. In the situation of Stacks.Chow.gysinHomomorphismOfInvertible_flatPullback_primeCycle,

c₁(L) ∩ p^* [W]_{k+1} = i_* ((p|_D)^* [W]_{k+1}) in A_{k+1+r}(X),

the source's second equality: the left side is the cap product of Stacks 02SO and L is canonically 𝒪_X(D), the divisor being the zero scheme of s.

This is Stacks.Chow.effectiveCartierIntersectionOfInvertible_flatPullback_primeCycle read through Stacks 02T9, in the form Stacks.Chow.effectiveCartierIntersectionOfInvertible_eq_firstChernClassCapOfInvertible.

theorem firstChernClassCapOfInvertible_flatPullback_primeCycle
    (C : ChowSituation.{u}) {X Y : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (p : X ⟶ Y) [LocallyOfFiniteType p] [Flat p] (hbase : p ≫ sY = sX) (r : ℕ)
    (hp : AlgebraicGeometry.RelativeDimension p (r + 1)) (k : ℤ) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : L.sections)
    [Flat ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)]
    (hD : Stacks.Divisors.IsRelativeEffectiveCartierDivisor p
      (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))))
    (hq : AlgebraicGeometry.RelativeDimension
      ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p) r)
    (W : Y.IdealSheafData) (hWint : IsIntegral W.subscheme)
    (hWdim : schemeDeltaDimension C (W.subschemeι ≫ sY) = ((k + 1 : ℤ) : EInt))
    (hcast : k + 1 + ((r + 1 : ℕ) : ℤ) = k + 1 + (r : ℤ) + 1) :
    firstChernClassCapOfInvertible C sX (k + 1 + (r : ℤ)) L
        (hcast ▸ flatPullback C sX sY p hbase (r + 1) hp (k + 1)
          (cycleAssociatedToClosedSubscheme C sY W.subschemeι (k + 1))) =
      properChowPushforward C
        ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sX
        (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι rfl (k + 1 + (r : ℤ))
        (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
          (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι C
          ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sX rfl
          (k + 1 + (r : ℤ)))
        (QuotientAddGroup.mk
          (flatPullback C
            ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sY
            ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)
            (by rw [Category.assoc, hbase]) r hq (k + 1)
            (cycleAssociatedToClosedSubscheme C sY W.subschemeι (k + 1))))

Stacks.Chow.gysinChowOfInvertible_flatPullbackChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierFlatPullbackChow.lean, line 332. The attribute's comment: “first equality, for an arbitrary class in A_{k+1}(Y)”.

Let p : X ⟶ Y be flat of relative dimension r + 1 over the base scheme of chapter 42 and let i : D ⟶ X be a relative effective Cartier divisor on X/Y, presented as the zero scheme of a section s of an invertible module L. Then for every class α ∈ A_{k+1}(Y)

i^* p^* α = (p|_D)^* α in A_{k+r}(D),

for the Gysin pullback of Stacks 02TO and the flat pullbacks of Stacks 02S1 on Chow groups, p|_D having relative dimension r by AlgebraicGeometry.relativeDimension_of_isRelativeEffectiveCartierDivisor.

theorem gysinChowOfInvertible_flatPullbackChow (C : ChowSituation.{u}) {X Y : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (p : X ⟶ Y) [LocallyOfFiniteType p] [Flat p] (hbase : p ≫ sY = sX) (r : ℕ)
    (hp : AlgebraicGeometry.RelativeDimension p (r + 1)) (k : ℤ) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : L.sections)
    [Flat ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)]
    (hD : Stacks.Divisors.IsRelativeEffectiveCartierDivisor p
      (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))))
    (hcast : k + 1 + ((r + 1 : ℕ) : ℤ) = k + 1 + (r : ℤ) + 1)
    (α : chowGroup C sY (k + 1)) :
    gysinChowOfInvertible C sX (k + 1 + (r : ℤ)) L (s.eval (.op ⊤))
        (hcast ▸ flatPullbackChowOfRelativeDimension C sX sY p hbase (r + 1) hp (k + 1) α) =
      flatPullbackChowOfRelativeDimension C
        ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sY
        ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)
        (by rw [Category.assoc, hbase]) r
        (AlgebraicGeometry.relativeDimension_of_isRelativeEffectiveCartierDivisor p r hp
          (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))) hD) (k + 1) α

Stacks.Chow.firstChernClassCapChow_flatPullbackChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeEffectiveCartierFlatPullbackChow.lean, line 405. The attribute's comment: “second equality, for an arbitrary class in A_{k+1}(Y)”.

In the situation of Stacks.Chow.gysinChowOfInvertible_flatPullbackChow, for every class α ∈ A_{k+1}(Y)

c₁(L) ∩ p^* α = i_* ((p|_D)^* α) in A_{k+r}(X),

the cap product being the descended operation of Stacks 02TI, with D the zero scheme of s, so that L is 𝒪_X(D).

theorem firstChernClassCapChow_flatPullbackChow (C : ChowSituation.{u}) {X Y : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (p : X ⟶ Y) [LocallyOfFiniteType p] [Flat p] (hbase : p ≫ sY = sX) (r : ℕ)
    (hp : AlgebraicGeometry.RelativeDimension p (r + 1)) (k : ℤ) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : L.sections)
    [Flat ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)]
    (hD : Stacks.Divisors.IsRelativeEffectiveCartierDivisor p
      (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))))
    (hcast : k + 1 + ((r + 1 : ℕ) : ℤ) = k + 1 + (r : ℤ) + 1)
    (α : chowGroup C sY (k + 1)) :
    firstChernClassCapChow C (k + 1 + (r : ℤ)) sX L
        (hcast ▸ flatPullbackChowOfRelativeDimension C sX sY p hbase (r + 1) hp (k + 1) α) =
      properChowPushforward C
        ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sX
        (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι rfl (k + 1 + (r : ℤ))
        (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
          (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι C
          ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sX rfl
          (k + 1 + (r : ℤ)))
        (flatPullbackChowOfRelativeDimension C
          ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ sX) sY
          ((Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))).subschemeι ≫ p)
          (by rw [Category.assoc, hbase]) r
          (AlgebraicGeometry.relativeDimension_of_isRelativeEffectiveCartierDivisor p r hp
            (Stacks.Divisors.zeroScheme X L (s.eval (.op ⊤))) hD) (k + 1) α)

Sources

LeanStacks.Chow.gysinChowOfInvertible_canonicalSection_flatPullbackChow · Stacks.Chow.firstChernClassCapChow_divisorSheaf_flatPullbackChow · Stacks.Chow.gysinChowOfInvertible_canonicalSection_flatPullbackChow_of_relativeDimension_zero · Stacks.Chow.firstChernClassCapChow_divisorSheaf_flatPullbackChow_of_relativeDimension_zero · Stacks.Chow.gysinHomomorphismOfInvertible_flatPullback_primeCycle · Stacks.Chow.effectiveCartierIntersectionOfInvertible_flatPullback_primeCycle · Stacks.Chow.firstChernClassCapOfInvertible_flatPullback_primeCycle · Stacks.Chow.gysinChowOfInvertible_flatPullbackChow

Section42.32 Affine bundles #

Section 42.32 of the Stacks Project, Tag 02TS. 8 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02TT, a lemma

Tag 02TT in the Stacks Project.

Stacks.Chow.flatPullbackChow_surjective_isAffineSpaceBundle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/AffineBundleSurjectivity.lean, line 149.

Let (S, δ) be the base situation of chapter 42, let X and Y be locally of finite type over S and let f : X ⟶ Y be flat of relative dimension r such that every point of Y has an open neighbourhood U over which f is the projection 𝔸^r_U ⟶ U. Then f^* : A_k(Y) ⟶ A_{k+r}(X) is surjective for every k.

theorem flatPullbackChow_surjective_isAffineSpaceBundle (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : X ⟶ Y)
    [LocallyOfFiniteType f] [AlgebraicGeometry.Flat f] (r : ℕ)
    (hf : AlgebraicGeometry.RelativeDimension f r) (hbundle : IsAffineSpaceBundle f r) (k : ℤ) :
    Function.Surjective (flatPullbackChowOfRelativeDimension C (f ≫ sY) sY f rfl r hf k)

Stacks.Chow.flatPullbackChow_surjective_of_isAffineSpaceBundle_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/Unconditional.lean, line 99.

Stacks 02TT. Let (S, δ) be the base situation of chapter 42, let X and Y be locally of finite type over S, and let f : X ⟶ Y be flat of relative dimension r such that every point of Y has an open neighbourhood U over which f is identified with the projection U × 𝔸^r ⟶ U. Then f^* : A_k(Y) ⟶ A_{k+r}(X) is surjective for every k ∈ ℤ.

theorem flatPullbackChow_surjective_of_isAffineSpaceBundle_unconditional (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : X ⟶ Y)
    [LocallyOfFiniteType f] [Flat f] (r : ℕ) (hf : AlgebraicGeometry.RelativeDimension f r)
    (hbundle : IsAffineSpaceBundle f r) (k : ℤ) :
    Function.Surjective (flatPullbackChow C (f ≫ sY) sY f rfl r hf k
      (flatPullbackFactorsThroughRationalEquivalence_general C (f ≫ sY) sY f rfl r hf k))

Tag 0B74, a lemma

Tag 0B74 in the Stacks Project.

Stacks.Chow.flatPullbackChow_injective_of_gysinRetracts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/LineBundleChow.lean, line 292. The attribute's comment: “injectivity only, from the zero section and Stacks 02TR”.

Stacks 0B74, the injectivity half. Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S, let ℒ be an invertible 𝒪_X-module and let p : L = \underline{\Spec}(\Sym^*(ℒ)) ⟶ X be the associated line bundle. Then

p^* : A_k(X) ⟶ A_{k+1}(L)

is injective for every k.

This is the source's argument: the zero section o : X ⟶ L satisfies p ∘ o = 𝟙_X (Stacks.LineBundle.Situation.zeroSection_comp_totalSpaceToBase) and its image is a relative effective Cartier divisor on L/X, so Stacks 02TR gives o^* ∘ p^* = \mathrm{id} and p^* is split injective. The retraction is Stacks.Chow.gysin_flatPullbackChow_zeroSection; the hypotheses gysin and h02TR are Stacks 02TR on Chow groups, and hfac is Stacks 02S1 at relative dimension one, both carried for the reasons recorded in the module documentation.

theorem flatPullbackChow_injective_of_gysinRetracts
    (h02TR : GysinRetractsFlatPullbackChow C sX (D.totalSpaceToBase ≫ sX) sX
      D.totalSpaceToBase rfl hp (𝟙 D.X) (Category.id_comp sX) (relativeDimension_identity D.X) k
      hfac (flatPullbackFactorsThroughRationalEquivalence_id C sX k) gysin) :
    Function.Injective
      (flatPullbackChow C (D.totalSpaceToBase ≫ sX) sX D.totalSpaceToBase rfl 1 hp k hfac)

Stacks.Chow.flatPullbackChow_totalSpaceToBase_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/LineBundleChowBijective.lean, line 59.

Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S, let ℒ be an invertible 𝒪_X-module and let p : L = \underline{\Spec}(\Sym^*(ℒ)) ⟶ X be the associated line bundle. Then

p^* : A_k(X) ⟶ A_{k+1}(L)

is an isomorphism for every k.

theorem flatPullbackChow_totalSpaceToBase_bijective (k : ℤ) :
    Function.Bijective
      (flatPullbackChowOfRelativeDimension C (D.totalSpaceToBase ≫ sX) sX D.totalSpaceToBase
        rfl 1 D.relativeDimension_totalSpaceToBase k)

Tag 02TU, a remark

Tag 02TU in the Stacks Project.

Stacks.Chow.flatPullbackChow_bijective_vectorBundle_and_affineSpaceBundle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/BundlePullbackIsomorphism.lean, line 63. The attribute's comment: “the whole remark: both assertions”.

Remark 02TU. Let (S, δ) be as in Situation 02QL.

If X is locally of finite type over S, ℰ is a finite locally free 𝒪_X-module of rank r and p : E ⟶ X is its vector bundle, then p^* : A_k(X) ⟶ A_{k+r}(E) is an isomorphism for every k (Lemma 02TY).

If X, Y are locally of finite type over S and f : X ⟶ Y is flat of relative dimension r and Zariski-locally on Y the projection U × 𝔸^r ⟶ U, as in Lemma 02TT, then f^* : A_k(Y) ⟶ A_{k+r}(X) is an isomorphism for every k (Remark 0GUB).

theorem flatPullbackChow_bijective_vectorBundle_and_affineSpaceBundle (C : ChowSituation.{u}) :
    (∀ {X : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (E : X.Modules)
      [E.IsQuasicoherent] (r : ℕ) [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r]
      (k : ℤ),
      letI := locallyOfFiniteType_vectorBundleToBase E r
      letI := flat_vectorBundleToBase E r
      Function.Bijective (flatPullbackChowOfRelativeDimension C
        (Scheme.Modules.vectorBundleToBase X E ≫ sX) sX (Scheme.Modules.vectorBundleToBase X E)
        rfl r (relativeDimension_vectorBundleToBase E r) k)) ∧
    (∀ {X Y : Scheme.{u}} (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : X ⟶ Y)
      [LocallyOfFiniteType f] [Flat f] (r : ℕ) (hf : AlgebraicGeometry.RelativeDimension f r)
      (_ : IsAffineSpaceBundle f r) (k : ℤ),
      Function.Bijective (flatPullbackChowOfRelativeDimension C (f ≫ sY) sY f rfl r hf k))

Declarations registered for the tag:

Stacks.Chow.flatPullbackChow_bijective_vectorBundleToBase, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/BundlePullbackIsomorphism.lean, line 45 (StacksFrontier): “first assertion: flat pullback along the vector bundle of a finite locally free module of rank r is an isomorphism of Chow groups in every degree (Lemma 02TY)”.
Stacks.Chow.flatPullbackChow_bijective_of_isAffineSpaceBundle, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/BundlePullbackIsomorphism.lean, line 49 (StacksFrontier): “second assertion: flat pullback along a morphism which is Zariski-locally on the target the projection U × A^r to U is an isomorphism of Chow groups in every degree (Remark 0GUB); flatness and relative dimension r follow from the local triviality”.

Tag 0F96, a lemma

Tag 0F96 in the Stacks Project.

Stacks.LineBundle.Situation.isRelativeEffectiveCartierDivisor_ker_zeroSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/AffineSpaceBundleSmooth.lean, line 112. The attribute's comment: “(1), the zero section is a relative effective Cartier divisor”.

The image of the zero section of a line bundle is a relative effective Cartier divisor, part of clause (1) of [Stacks, Tag 0F96]. The projection of the total space is smooth of relative dimension one, and the closed subscheme cut out by the zero section is finite locally free over the base because the projection restricts on it to the comparison isomorphism with the base; so [Stacks, Tag 0B9D] applies.

theorem Situation.isRelativeEffectiveCartierDivisor_ker_zeroSection (D : Situation.{u}) :
    Stacks.Divisors.IsRelativeEffectiveCartierDivisor D.totalSpaceToBase
      D.zeroSection.ker

Stacks.Chow.zeroSectionGysinChow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/ZeroSectionGysin.lean, line 210. The attribute's comment: “part (3)”.

Stacks 0F96, clause (3). The image o(X) of the zero section of a line bundle p : L ⟶ X is an effective Cartier divisor on L, so it has a Gysin map; composed with the identification of o(X) with X it is

o^* : \CH_{k + 1}(L) ⟶ \CH_k(X).

The divisor is presented as clause (1) presents it, the zero scheme of the tautological global section of p^*(ℒ^{⊗ -1}), and the Gysin map of a zero scheme is the unconditional [Stacks, Tag 02TO] on Chow groups. That the divisor is an effective Cartier divisor — the clause's justification — is Stacks.LineBundle.Situation.isRelativeEffectiveCartierDivisor_zeroScheme_tautologicalSectionBase; it is a theorem here and so is not taken as a hypothesis.

def zeroSectionGysinChow (k : ℤ) :
    chowGroup C (D.totalSpaceToBase ≫ sX) (k + 1) →+ chowGroup C sX k

Stacks.Chow.zeroSectionGysinChow_comp_flatPullbackChowOfRelativeDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/ZeroSectionGysinRetraction.lean, line 248. The attribute's comment: “part (4)”.

Stacks 0F96, clause (4). The source's phrasing: the composite

o^* p^* : \CH_k(X) ⟶ \CH_k(X)

is the identity map. This is Stacks.Chow.zeroSectionGysinChow_flatPullbackChowOfRelativeDimension read as an equality of homomorphisms; the two are interchangeable, both sides of the equality being determined by their values.

theorem zeroSectionGysinChow_comp_flatPullbackChowOfRelativeDimension (k : ℤ) :
    (zeroSectionGysinChow C D sX k).comp
        (flatPullbackChowOfRelativeDimension C (D.totalSpaceToBase ≫ sX) sX D.totalSpaceToBase
          rfl 1 D.relativeDimension_totalSpaceToBase k) =
      AddMonoidHom.id (chowGroup C sX k)

Stacks.Chow.zeroSectionChowPushforward_eq_neg_flatPullbackChow_firstChernClassCapChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/ZeroSectionProjectionFormula.lean, line 352. The attribute's comment: “part (5)”.

Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S, let ℒ be an invertible 𝒪_X-module and let p : L ⟶ X be the associated line bundle with zero section o : X ⟶ L. Then

o_* α = - p^*(c₁(ℒ) ∩ α) in A_{k+1}(L) for every α ∈ A_{k+1}(X).

Here c₁(ℒ) ∩ - on A_{k+1}(X) is firstChernClassCapChow C k, and the flat pullback, which lands in A_{k + ((1 : ℕ) : ℤ)}(L), is transported to A_{k+1}(L) by Stacks.Chow.chowGroupCast.

theorem zeroSectionChowPushforward_eq_neg_flatPullbackChow_firstChernClassCapChow (k : ℤ)
    (α : chowGroup C sX (k + 1)) :
    zeroSectionChowPushforward C D sX (k + 1) α =
      -chowGroupCast C (D.totalSpaceToBase ≫ sX)
        (show k + ((1 : ℕ) : ℤ) = k + 1 from by simp)
        (flatPullbackChowOfRelativeDimension C (D.totalSpaceToBase ≫ sX) sX D.totalSpaceToBase
          rfl 1 D.relativeDimension_totalSpaceToBase k (firstChernClassCapChow C k sX D.L α))

Stacks.Chow.zeroSectionChowPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/ZeroSectionPushforward.lean, line 64. The attribute's comment: “part (2)”.

The proper pushforward on Chow groups along the zero section o : X ⟶ L of a line bundle,

o_* : \CH_k(X) ⟶ \CH_k(L).

def zeroSectionChowPushforward (k : ℤ) :
    chowGroup C sX k →+ chowGroup C (D.totalSpaceToBase ≫ sX) k

Stacks.Chow.zeroSectionGysinChow_zeroSectionChowPushforward_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/ZeroSectionSelfIntersection.lean, line 239. The attribute's comment: “part (6)”. References: SGA 5 VII (9.2), “special case”.

Stacks 0F96, clause (6). The Gysin map of the zero section of a line bundle p : L ⟶ X composed with the pushforward along it is intersection with the first Chern class of ℒ, with a minus sign:

o^* o_* α = - c₁(ℒ) ∩ α,

a map \CH_{k+1}(X) ⟶ \CH_k(X).

Both maps of the composite are the maps of clauses (2) and (3), Stacks.Chow.zeroSectionChowPushforward and Stacks.Chow.zeroSectionGysinChow, and the only hypothesis is theirs, that X be locally of finite type over S. The right hand side is the cap product of [Stacks, Tag 02SO] on a cycle representative, which is what makes it unconditional; see the module documentation.

The proof is the source's: the self-intersection formula [Stacks, Tag 0F95] for the divisor o(X) on L, whose module is p^*(ℒ^{⊗ -1}) by clause (1), followed by the identification of the restriction of that module with ℒ^{⊗ -1} and by [Stacks, Tag 02SP] in the form c₁(ℒ^{⊗ -1}) ∩ α = -(c₁(ℒ) ∩ α), which is where the sign comes from.

theorem zeroSectionGysinChow_zeroSectionChowPushforward_mk (k : ℤ)
    (α : CycleGroup C sX (k + 1)) :
    zeroSectionGysinChow C D sX k
        (zeroSectionChowPushforward C D sX (k + 1)
          (QuotientAddGroup.mk' (rationalEquivalences C sX (k + 1)) α)) =
      -firstChernClassCapOfInvertible C sX k D.L α

Stacks.Chow.zeroSectionGysinChow_comp_zeroSectionChowPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/ZeroSectionSelfIntersection.lean, line 328. The attribute's comment: “part (6)”.

Stacks 0F96, clause (6). The source's phrasing: the composite

o^* o_* : \CH_{k+1}(X) ⟶ \CH_k(X)

is the map α ↦ - c₁(ℒ) ∩ α, as an equality of homomorphisms read on cycle representatives. Every Chow class is the class of a cycle, so this and Stacks.Chow.zeroSectionGysinChow_zeroSectionChowPushforward_mk are interchangeable.

theorem zeroSectionGysinChow_comp_zeroSectionChowPushforward (k : ℤ) :
    ((zeroSectionGysinChow C D sX k).comp
          (zeroSectionChowPushforward C D sX (k + 1))).comp
        (QuotientAddGroup.mk' (rationalEquivalences C sX (k + 1))) =
      -firstChernClassCapOfInvertible C sX k D.L

Stacks.LineBundle.Situation.isRegularSection_tautologicalSectionBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/LineBundle/TautologicalSectionBaseRegular.lean, line 54. The attribute's comment: “part (1), the section is regular”.

The tautological global section of p^*(L^{⊗ -1}) is a regular section, that is, multiplication by it is injective.

theorem Situation.isRegularSection_tautologicalSectionBase :
    AlgebraicGeometry.IsRegularSection D.totalSpace.sheaf.obj
      D.totalSpace.ringCatSheaf.property D.tautologicalSectionBaseSections

Stacks.LineBundle.Situation.zeroScheme_tautologicalSectionBase_eq_ker_zeroSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/LineBundle/ZeroSectionZeroScheme.lean, line 190. The attribute's comment: “part (1), the zero scheme”.

Clause (1) of [Stacks, Tag 0F96], the zero scheme. Let L be an invertible module on a scheme X, let p : Tot(L) ⟶ X be the associated line bundle and let o : X ⟶ Tot(L) be its zero section. Then the closed subscheme o(X) of Tot(L) is the zero scheme of the tautological global section of p^*(L^{⊗ -1}).

The hypotheses of [Stacks, Tag 0B74] that X be locally of finite type over a base scheme with a dimension function are not needed and are omitted: clause (1) is a statement about the line bundle alone.

theorem Situation.zeroScheme_tautologicalSectionBase_eq_ker_zeroSection :
    Stacks.Divisors.zeroScheme D.totalSpace D.basePullbackInverse D.tautologicalSectionBase =
      D.zeroSection.ker

Stacks.LineBundle.Situation.isRegularSection_tautologicalSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/LineBundle/ZeroSectionZeroScheme.lean, line 214. The attribute's comment: “part (1), the section is regular”.

Clause (1) of [Stacks, Tag 0F96], regularity of the section. The tautological global section of p^*(L^{⊗ -1}) is a regular section, that is, multiplication by it is injective: its zero scheme is the image of the zero section, which is an effective Cartier divisor on the total space by [Stacks, Tag 0B9D].

theorem Situation.isRegularSection_tautologicalSection :
    AlgebraicGeometry.IsRegularSection D.totalSpace.sheaf.obj
      D.totalSpace.ringCatSheaf.property
      (SheafOfModules.unitHomEquiv D.pullbackInverse D.tautologicalSectionHom)

Tag 0F97, a lemma

Tag 0F97 in the Stacks Project.

Stacks.Chow.TensorZeroScheme.pullbackTensorSection_proj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TensorZeroScheme/Basic.lean, line 279. The attribute's comment: “the construction and conditions (1), (3); (2) and (4)-(7) not proved here”.

The pullback p^*s of the section to the zero scheme L of z₁ ⊗ z₂ - q^*s, read in p^*L₁ ⊗ p^*L₂, is the product s₁ ⊗ s₂ of the two restricted fibre coordinates.

theorem pullbackTensorSection_proj :
    pullbackTensorSection (proj Y L₁ L₂ s) L₁ L₂ s =
      tensorSectionsAt (spaceIdeal Y L₁ L₂ s).subscheme.sheaf.obj
        (spaceIdeal Y L₁ L₂ s).subscheme.ringCatSheaf.property (op ⊤)
        ((Scheme.Modules.pullback (proj Y L₁ L₂ s)).obj L₁)
        ((Scheme.Modules.pullback (proj Y L₁ L₂ s)).obj L₂)
        (section₁ Y L₁ L₂ s) (section₂ Y L₁ L₂ s)

Stacks.Chow.TensorZeroScheme.exists_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TensorZeroScheme/DecompositionExistence.lean, line 100.

[Stacks, Tag 0F97]. Let Y be a scheme, L₁, L₂ invertible 𝒪_Y-modules, s a global section of L₁ ⊗ L₂ and i : D → Y its zero scheme. There is a commutative diagram D₁ → L ← D₂ over D → Y ← D, with p : L ⟶ Y, and sections sᵢ of p^*Lᵢ such that p^*s = s₁ ⊗ s₂; p is of finite type and flat of relative dimension 1; Dᵢ is the zero scheme of sᵢ; Dᵢ ≅ \underline{\Spec}(\Sym^*(L_{3-i}^{⊗ -1})|_D) over D; p^{-1}D = D₁ ∪ D₂; D₁ ∩ D₂ ⟶ D is an isomorphism; and D₁ ∩ D₂ ⟶ Dᵢ is the zero section of the line bundle Dᵢ ⟶ D (the record Stacks.Chow.TensorZeroScheme.Decomposition). Moreover the formation of the diagram and of the sections commutes with arbitrary base change (Stacks.Chow.TensorZeroScheme.Decomposition.IsStableUnderBaseChange).

theorem exists_decomposition : ∃ R : Decomposition Y L₁ L₂ s, R.IsStableUnderBaseChange

Tag 0F98, a lemma

Tag 0F98 in the Stacks Project.

Stacks.Chow.TensorZeroScheme.gysinChowBranch₁_flatPullbackChowProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundle/ZeroSectionBranchChowIdentity.lean, line 200.

In the situation of [Stacks, Tag 0F97],

i₁^* p^* α = p₁^* i^* α in A_{k+1}(D₁) for every α ∈ A_{k+1}(Y).

theorem gysinChowBranch₁_flatPullbackChowProj (α : Stacks.Chow.chowGroup C sY (k + 1)) :
    gysinChowBranch₁ C Y L₁ L₂ s R sY (k + 1)
        (flatPullbackChowProj C Y L₁ L₂ s R sY (k + 1) α) =
      flatPullbackChowProj₁ C Y L₁ L₂ s R sY k (gysinChowZeroIdeal C Y L₁ L₂ s sY k α)

Tag 0F99, a lemma

Tag 0F99 in the Stacks Project.

Stacks.Chow.TensorZeroScheme.exists_principalReduction_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TensorZeroScheme/PrincipalReductionExistence.lean, line 531.

[Stacks, Tag 0F99]. For a scheme X locally of finite type over the base situation of chapter 42 and a triple (ℒ, s, i : D ⟶ X) as in [Stacks, Tag 02T8] there is a commutative square

D' --i'--> X' |p |g D --i--> X

such that p and g are of finite type and flat of relative dimension 1, p^* : A_k(D) ⟶ A_{k+1}(D') is injective for all k, D' ⊆ X' is the zero scheme of a global section of 𝒪_{X'}, and p^*i^* = (i')^*g^*; and these properties remain true after arbitrary base change by morphisms Y ⟶ X locally of finite type.

theorem exists_principalReduction_isStableUnderBaseChange :
    ∃ R : PrincipalReduction C sX L s, R.IsStableUnderBaseChange

Tag 0GUB, a remark

Tag 0GUB in the Stacks Project.

Stacks.Chow.flatPullbackChow_bijective_of_isAffineSpaceBundle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AffineBundleInjective/Bijectivity.lean, line 89.

Stacks 0GUB. Let (S, δ) be as in Situation 02QL, let Y be locally of finite type over S, let r ≥ 0 and let f : X ⟶ Y be a morphism of schemes such that every point of Y lies in an open V ⊆ Y with f⁻¹(V) ≅ V × 𝔸^r as schemes over V. Then flat pullback

f^* : CH_k(Y) ⟶ CH_{k+r}(X)

is an isomorphism for every k. The morphism f is locally of finite type, flat and of relative dimension r because it is so locally on Y; these are not hypotheses but consequences of the local triviality, recorded through letI.

theorem flatPullbackChow_bijective_of_isAffineSpaceBundle (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : X ⟶ Y) (r : ℕ)
    (hbundle : IsAffineSpaceBundle f r) (k : ℤ) :
    letI := locallyOfFiniteType_of_isAffineSpaceBundle f r hbundle
    letI := flat_of_isAffineSpaceBundle f r hbundle
    Function.Bijective (flatPullbackChowOfRelativeDimension C (f ≫ sY) sY f rfl r
      (relativeDimension_of_isAffineSpaceBundle f r hbundle) k)

Sources

LeanStacks.Chow.flatPullbackChow_surjective_isAffineSpaceBundle · Stacks.Chow.flatPullbackChow_surjective_of_isAffineSpaceBundle_unconditional · Stacks.Chow.flatPullbackChow_injective_of_gysinRetracts · Stacks.Chow.flatPullbackChow_totalSpaceToBase_bijective · Stacks.Chow.flatPullbackChow_bijective_vectorBundle_and_affineSpaceBundle · Stacks.Chow.flatPullbackChow_bijective_vectorBundleToBase · Stacks.Chow.flatPullbackChow_bijective_of_isAffineSpaceBundle · Stacks.LineBundle.Situation.isRelativeEffectiveCartierDivisor_ker_zeroSection

Section42.33 Bivariant intersection theory #

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

Tag 0B75, the section

Tag 0B75 in the Stacks Project.

Stacks.Chow.bivariantComposite_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Associativity.lean, line 188. The attribute's comment: “the composition of bivariant classes is associative: for a ∈ A^p(X ⟶ Y), b ∈ A^q(Y ⟶ Z) and c ∈ A^r(Z ⟶ W) the triple composites (a ∘ b) ∘ c and a ∘ (b ∘ c) agree in A^{p+q+r}(X ⟶ W), the degrees (p + q) + r and p + (q + r) being the same integer written two ways”.

The composition of bivariant classes is associative: for a ∈ A^p(X ⟶ Y), b ∈ A^q(Y ⟶ Z) and c ∈ A^r(Z ⟶ W) the two triple composites (a ∘ b) ∘ c and a ∘ (b ∘ c) agree in A^{p+q+r}(X ⟶ W), the equality being heterogeneous because the two sides are indexed by (p + q) + r and p + (q + r) [Stacks, Tag 0B75].

theorem bivariantComposite_assoc (hgys : G.IsNaturalUnderBaseChangeIso)
    (hgysc : G.IsNaturalUnderPullbackCompPushforward) :
    bivariantComposite C G sX sZ sW (f ≫ g) h (comp_comp_structureMorphism_eq hf hg) hh (p + q) r
        (bivariantComposite C G sX sY sZ f g hf hg p q a b hgys hgysc) c hgys hgysc ≍
      bivariantComposite C G sX sY sW f (g ≫ h) hf (comp_comp_structureMorphism_eq hg hh) p
        (q + r) a (bivariantComposite C G sY sZ sW g h hg hh q r b c hgys hgysc) hgys hgysc

Stacks.Chow.bivariantCompositeBilinear_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Associativity.lean, line 203. The attribute's comment: “the bilinear composition A^p(X ⟶ Y) × A^q(Y ⟶ Z) ⟶ A^{p+q}(X ⟶ Z) is associative”.

Associativity of the composition, read on the bilinear map Stacks.Chow.bivariantCompositeBilinear that bundles it [Stacks, Tag 0B75].

theorem bivariantCompositeBilinear_assoc (hgys : G.IsNaturalUnderBaseChangeIso)
    (hgysc : G.IsNaturalUnderPullbackCompPushforward) :
    bivariantCompositeBilinear C G sX sZ sW (f ≫ g) h (comp_comp_structureMorphism_eq hf hg) hh
          (p + q) r hgys hgysc
        (bivariantCompositeBilinear C G sX sY sZ f g hf hg p q hgys hgysc a b) c ≍
      bivariantCompositeBilinear C G sX sY sW f (g ≫ h) hf
        (comp_comp_structureMorphism_eq hg hh) p (q + r) hgys hgysc a
        (bivariantCompositeBilinear C G sY sZ sW g h hg hh q r hgys hgysc b c)

Stacks.Chow.bivariantComposite_add_left', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Bilinearity.lean, line 56. The attribute's comment: “the bilinearity of the composition, additivity in the first argument”.

Additivity of the composition in the first argument: (a + a') ∘ b = a ∘ b + a' ∘ b.

theorem bivariantComposite_add_left' (a a' : BivariantClass C G sX sY f hf p)
    (b : BivariantClass C G sY sZ g hg q) :
    bivariantComposite C G sX sY sZ f g hf hg p q (a + a') b hgys hgysc =
      bivariantComposite C G sX sY sZ f g hf hg p q a b hgys hgysc +
        bivariantComposite C G sX sY sZ f g hf hg p q a' b hgys hgysc

Stacks.Chow.bivariantComposite_add_right', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Bilinearity.lean, line 70. The attribute's comment: “the bilinearity of the composition, additivity in the second argument”.

Additivity of the composition in the second argument: a ∘ (b + b') = a ∘ b + a ∘ b'.

theorem bivariantComposite_add_right' (a : BivariantClass C G sX sY f hf p)
    (b b' : BivariantClass C G sY sZ g hg q) :
    bivariantComposite C G sX sY sZ f g hf hg p q a (b + b') hgys hgysc =
      bivariantComposite C G sX sY sZ f g hf hg p q a b hgys hgysc +
        bivariantComposite C G sX sY sZ f g hf hg p q a b' hgys hgysc

Stacks.Chow.bivariantComposite_neg_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Bilinearity.lean, line 84. The attribute's comment: “the bilinearity of the composition, negation in the first argument”.

The composition negates in its first argument: (-a) ∘ b = -(a ∘ b).

theorem bivariantComposite_neg_left (a : BivariantClass C G sX sY f hf p)
    (b : BivariantClass C G sY sZ g hg q) :
    bivariantComposite C G sX sY sZ f g hf hg p q (-a) b hgys hgysc =
      -bivariantComposite C G sX sY sZ f g hf hg p q a b hgys hgysc

Stacks.Chow.bivariantComposite_neg_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Bilinearity.lean, line 95. The attribute's comment: “the bilinearity of the composition, negation in the second argument”.

The composition negates in its second argument: a ∘ (-b) = -(a ∘ b).

theorem bivariantComposite_neg_right (a : BivariantClass C G sX sY f hf p)
    (b : BivariantClass C G sY sZ g hg q) :
    bivariantComposite C G sX sY sZ f g hf hg p q a (-b) hgys hgysc =
      -bivariantComposite C G sX sY sZ f g hf hg p q a b hgys hgysc

Stacks.Chow.bivariantComposite_zero_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Bilinearity.lean, line 106. The attribute's comment: “the bilinearity of the composition, the zero class on the left”.

The composite of the zero class with any class is zero.

theorem bivariantComposite_zero_left (b : BivariantClass C G sY sZ g hg q) :
    bivariantComposite C G sX sY sZ f g hf hg p q 0 b hgys hgysc = 0

Stacks.Chow.bivariantComposite_zero_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Bilinearity.lean, line 114. The attribute's comment: “the bilinearity of the composition, the zero class on the right”.

The composite of any class with the zero class is zero.

theorem bivariantComposite_zero_right (a : BivariantClass C G sX sY f hf p) :
    bivariantComposite C G sX sY sZ f g hf hg p q a 0 hgys hgysc = 0

Stacks.Chow.bivariantCompositeAddHomLeft, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Bilinearity.lean, line 124. The attribute's comment: “the bilinearity of the composition: the partial map in the first argument as a homomorphism of groups”.

Composition with a fixed class b ∈ A^q(Y ⟶ Z) on the right, as a homomorphism A^p(X ⟶ Y) ⟶ A^{p+q}(X ⟶ Z) of groups.

def bivariantCompositeAddHomLeft (b : BivariantClass C G sY sZ g hg q) :
    BivariantClass C G sX sY f hf p →+
      BivariantClass C G sX sZ (f ≫ g) (comp_comp_structureMorphism_eq hf hg) (p + q)

Stacks.Chow.bivariantCompositeAddHomRight, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Bilinearity.lean, line 135. The attribute's comment: “the bilinearity of the composition: the partial map in the second argument as a homomorphism of groups”.

Composition with a fixed class a ∈ A^p(X ⟶ Y) on the left, as a homomorphism A^q(Y ⟶ Z) ⟶ A^{p+q}(X ⟶ Z) of groups.

def bivariantCompositeAddHomRight (a : BivariantClass C G sX sY f hf p) :
    BivariantClass C G sY sZ g hg q →+
      BivariantClass C G sX sZ (f ≫ g) (comp_comp_structureMorphism_eq hf hg) (p + q)

Stacks.Chow.bivariantComposite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Class.lean, line 134. The attribute's comment: “the composite bivariant class, assembled from its cap operation and the three naturality conditions of Stacks 0B76”.

The composite a ∘ b ∈ A^{p+q}(X ⟶ Z) of bivariant classes a ∈ A^p(X ⟶ Y) and b ∈ A^q(Y ⟶ Z): the bivariant class of degree p + q for f ≫ g whose cap operation is α ↦ a ∩ (b ∩ α), that is, Stacks.Chow.bivariantCompositeCap read through the transport of Chow groups along k - q - p = k - (p + q) [Stacks, Tag 0B75].

def bivariantComposite (hgys : G.IsNaturalUnderBaseChangeIso)
    (hgysc : G.IsNaturalUnderPullbackCompPushforward) :
    BivariantClass C G sX sZ (f ≫ g) (comp_comp_structureMorphism_eq hf hg) (p + q)

Stacks.Chow.bivariantCompositeBilinear, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Class.lean, line 260. The attribute's comment: “the composition of bivariant classes is bilinear”.

The composition A^p(X ⟶ Y) × A^q(Y ⟶ Z) ⟶ A^{p+q}(X ⟶ Z) as a bilinear map, that is, Stacks.Chow.bivariantComposite bundled through its additivity in each argument [Stacks, Tag 0B75].

def bivariantCompositeBilinear (hgys : G.IsNaturalUnderBaseChangeIso)
    (hgysc : G.IsNaturalUnderPullbackCompPushforward) :
    BivariantClass C G sX sY f hf p →+
      BivariantClass C G sY sZ g hg q →+
        BivariantClass C G sX sZ (f ≫ g) (comp_comp_structureMorphism_eq hf hg) (p + q)

Stacks.Chow.bivariantCompositeOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/GysinSystemOfInvertible.lean, line 157. The attribute's comment: “the composite bivariant class at the Gysin system of the first Chern class rule, with both cases of Stacks 02TA discharged”.

The composite a ∘ b ∈ A^{p+q}(X ⟶ Z) of bivariant classes at the Gysin system of the first Chern class rule of an invertible module.

def bivariantCompositeOfInvertible
    (a : BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p)
    (b : BivariantClass C (gysinSystemOfInvertible C) sY sZ g hg q) :
    BivariantClass C (gysinSystemOfInvertible C) sX sZ (f ≫ g)
      (comp_comp_structureMorphism_eq hf hg) (p + q)

Stacks.Chow.bivariantCompositeBilinearOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/GysinSystemOfInvertible.lean, line 170. The attribute's comment: “the composition as a bilinear map, at the Gysin system of the first Chern class rule, with both cases of Stacks 02TA discharged”.

The composition A^p(X ⟶ Y) × A^q(Y ⟶ Z) ⟶ A^{p+q}(X ⟶ Z) of bivariant classes as a bilinear map, at the Gysin system of the first Chern class rule.

def bivariantCompositeBilinearOfInvertible :
    BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p →+
      BivariantClass C (gysinSystemOfInvertible C) sY sZ g hg q →+
        BivariantClass C (gysinSystemOfInvertible C) sX sZ (f ≫ g)
          (comp_comp_structureMorphism_eq hf hg) (p + q)

Stacks.Chow.bivariantCompositeCap_proper_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Naturality.lean, line 597. The attribute's comment: “the proper-pushforward condition of the composite”.

The proper-pushforward condition of Stacks 0B76 for the composite of two bivariant classes: the cap operation α ↦ a ∩ (b ∩ α) commutes with proper pushforward along a morphism of test schemes. The condition for b moves the pushforward past the inner cap and onto the middle base change T' ×_Z Y ⟶ T ×_Z Y, and the outer cap operation's condition moves it past the outer cap.

theorem bivariantCompositeCap_proper_naturality {T T' : Scheme.{u}} (t : T ⟶ Z)
    [LocallyOfFiniteType t] (h : T' ⟶ T) [IsProper h]
    (h' : pullback (f ≫ g) (h ≫ t) ⟶ pullback (f ≫ g) t)
    (sq : IsPullback (pullback.snd (f ≫ g) (h ≫ t)) h' h (pullback.snd (f ≫ g) t))
    (hfst : h' ≫ pullback.fst (f ≫ g) t = pullback.fst (f ≫ g) (h ≫ t)) (k : ℤ)
    (α : chowGroup C ((h ≫ t) ≫ sZ) k) :
    letI : IsProper h' := MorphismProperty.of_isPullback sq (P := @IsProper) inferInstance
    bivariantCompositeCap C G sX sY sZ f g hf hg hpp p q a b t k
        (properChowPushforward C ((h ≫ t) ≫ sZ) (t ≫ sZ) h (by simp [Category.assoc]) k
          (hpp _ _ _ _ _) α) =
      properChowPushforward C (pullback.fst (f ≫ g) (h ≫ t) ≫ sX)
        (pullback.fst (f ≫ g) t ≫ sX) h' (by rw [← Category.assoc, hfst]) (k - q - p)
        (hpp _ _ _ _ _)
        (bivariantCompositeCap C G sX sY sZ f g hf hg hpp p q a b (h ≫ t) k α)

Declarations registered for the tag:

Stacks.Chow.instAddCommGroupBivariantClass registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/Naturality.lean, line 773 (StacksFrontier): “the abelian group of bivariant classes”.

Tag 0B76, a definition

Tag 0B76 in the Stacks Project.

Stacks.Chow.BivariantClass, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Basic.lean, line 250. The attribute's comment: “the group A^p(X ⟶ Y) of bivariant classes of degree p for f, stated against a GysinSystem supplying the first Chern class rule of Stacks 02SO and the vanishing of Stacks 02TO”.

Stacks 0B76. A bivariant class of degree p for f : X ⟶ Y: a rule assigning to every morphism g : T ⟶ Y locally of finite type and every k an additive map A_k(T) ⟶ A_{k-p}(T ×_Y X), natural for proper pushforward, for flat pullback of fixed relative dimension, and for the Gysin map of the zero scheme of a section of an invertible module. The group of all of them is denoted A^p(X ⟶ Y).

Stated against a Stacks.Chow.GysinSystem, which supplies the first Chern class rule of Stacks 02SO and the vanishing of Stacks 02TO; see the module docstring.

structure BivariantClass (C : ChowSituation.{u}) (G : GysinSystem C) {X Y : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (f : X ⟶ Y) [LocallyOfFiniteType f] (hf : f ≫ sY = sX) (p : ℤ)

Stacks.Chow.BivariantClass.ext, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Basic.lean, line 411. The attribute's comment: “extensionality: a bivariant class is determined by its cap operations”.

Stacks 0B76. Two bivariant classes agree as soon as all their cap operations agree.

theorem BivariantClass.ext {c d : BivariantClass C G sX sY f hf p}
    (h : ∀ {T : Scheme.{u}} (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ)
      (α : chowGroup C (g ≫ sY) k), c.cap g k α = d.cap g k α) : c = d

Stacks.Chow.BivariantClass.zero_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Basic.lean, line 534. The attribute's comment: “the zero of the group A^p(X ⟶ Y)”.

Stacks 0B76. The zero bivariant class caps to zero.

theorem BivariantClass.zero_cap {T : Scheme.{u}} (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ)
    (α : chowGroup C (g ≫ sY) k) :
    (0 : BivariantClass C G sX sY f hf p).cap g k α = 0

Stacks.Chow.BivariantClass.add_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Basic.lean, line 541. The attribute's comment: “addition in A^p(X ⟶ Y) is pointwise on cap products”.

Stacks 0B76. A sum of bivariant classes caps to the sum of their cap products.

theorem BivariantClass.add_cap (c d : BivariantClass C G sX sY f hf p) {T : Scheme.{u}}
    (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ sY) k) :
    (c + d).cap g k α = c.cap g k α + d.cap g k α

Stacks.Chow.BivariantClass.neg_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Basic.lean, line 548. The attribute's comment: “negation in A^p(X ⟶ Y) is pointwise on cap products”.

Stacks 0B76. A negated bivariant class caps to the negated cap product.

theorem BivariantClass.neg_cap (c : BivariantClass C G sX sY f hf p) {T : Scheme.{u}}
    (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ sY) k) :
    (-c).cap g k α = -c.cap g k α

Stacks.Chow.BivariantClass.sub_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Basic.lean, line 598. The attribute's comment: “subtraction in A^p(X ⟶ Y) is pointwise on cap products”.

Stacks 0B76. A difference of bivariant classes caps to the difference of their cap products.

theorem BivariantClass.sub_cap (c d : BivariantClass C G sX sY f hf p) {T : Scheme.{u}}
    (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ sY) k) :
    (c - d).cap g k α = c.cap g k α - d.cap g k α

Stacks.Chow.BivariantClass.nsmul_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Basic.lean, line 606. The attribute's comment: “natural multiples in A^p(X ⟶ Y) are pointwise on cap products”.

Stacks 0B76. A natural multiple of a bivariant class caps to that multiple of its cap product.

theorem BivariantClass.nsmul_cap (n : ℕ) (c : BivariantClass C G sX sY f hf p) {T : Scheme.{u}}
    (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ sY) k) :
    (n • c).cap g k α = n • c.cap g k α

Stacks.Chow.BivariantClass.zsmul_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Basic.lean, line 616. The attribute's comment: “integer multiples in A^p(X ⟶ Y) are pointwise on cap products”.

Stacks 0B76. An integer multiple of a bivariant class caps to that multiple of its cap product.

theorem BivariantClass.zsmul_cap (n : ℤ) (c : BivariantClass C G sX sY f hf p) {T : Scheme.{u}}
    (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ sY) k) :
    (n • c).cap g k α = n • c.cap g k α

Stacks.Chow.CanonicalBivariantClass, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Canonical.lean, line 116. The attribute's comment: “the group A^p(X ⟶ Y) of bivariant classes of degree p for f, with nothing assumed: the Gysin system is the canonical one, whose first Chern class rule is the rule of an invertible module and whose vanishing is Stacks 02TO, and the descent conditions Stacks 02S1 and 02S2 of the proper and flat axioms are discharged”.

Stacks 0B76. The group A^p(X ⟶ Y) of bivariant classes of degree p for a morphism f : X ⟶ Y of schemes locally of finite type over the base: a rule assigning to every morphism g : T ⟶ Y locally of finite type and every k an additive map A_k(T) ⟶ A_{k-p}(T ×_Y X), natural for proper pushforward, for flat pullback of fixed relative dimension, and for the Gysin map of the zero scheme of a section of an invertible module.

This is Stacks.Chow.BivariantClass read against Stacks.Chow.canonicalGysinSystem, with the abelian group structure of Stacks.Chow.BivariantClass.

abbrev CanonicalBivariantClass (C : ChowSituation.{u}) {X Y : Scheme.{u}} (sX : X ⟶ C.S)
    [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : X ⟶ Y)
    [LocallyOfFiniteType f] (hf : f ≫ sY = sX) (p : ℤ)

Stacks.Chow.BivariantClass.flat_naturality_of_relativeDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Canonical.lean, line 134. The attribute's comment: “the flat pullback axiom, with the descent condition Stacks 02S1 discharged; the relative dimension of the base change is assumed, Stacks 02NK being absent”.

Stacks 0B76 (2), with Stacks 02S1 discharged. Cap product with a bivariant class commutes with flat pullback of fixed relative dimension, the relative dimension of the base change being a hypothesis.

theorem BivariantClass.flat_naturality_of_relativeDimension (c : BivariantClass C G sX sY f hf p)
    {T T' : Scheme.{u}} (g : T ⟶ Y) [LocallyOfFiniteType g] (h : T' ⟶ T) [LocallyOfFiniteType h]
    [Flat h] (r : ℕ) (hr : AlgebraicGeometry.RelativeDimension h r)
    (h' : pullback f (h ≫ g) ⟶ pullback f g)
    (sq : IsPullback (pullback.snd f (h ≫ g)) h' h (pullback.snd f g))
    (hfst : h' ≫ pullback.fst f g = pullback.fst f (h ≫ g)) (k : ℤ) :
    letI : LocallyOfFiniteType h' :=
      MorphismProperty.of_isPullback sq (P := @LocallyOfFiniteType) inferInstance
    letI : Flat h' := MorphismProperty.of_isPullback sq (P := @Flat) inferInstance
    ∀ (hr' : AlgebraicGeometry.RelativeDimension h' r) (α : chowGroup C (g ≫ sY) k),
      HEq
        (c.cap (h ≫ g) (k + (r : ℤ))
          (flatPullbackChow C ((h ≫ g) ≫ sY) (g ≫ sY) h (by simp [Category.assoc]) r hr k
            (flatPullbackDescends C _ _ _ _ _ _ _) α))
        (flatPullbackChow C (pullback.fst f (h ≫ g) ≫ sX) (pullback.fst f g ≫ sX) h'
          (by rw [← Category.assoc, hfst]) r hr' (k - p)
          (flatPullbackDescends C _ _ _ _ _ _ _) (c.cap g k α))

Stacks.Chow.BivariantClass.gysin_naturality_gysinChowOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Canonical.lean, line 160. The attribute's comment: “the Gysin axiom for a class at the canonical Gysin system, stated for the unconditional Gysin map of Stacks 02TO and with the descent condition Stacks 02S2 discharged”.

Stacks 0B76 (3), for the canonical Gysin system. Cap product with a bivariant class read against Stacks.Chow.canonicalGysinSystem commutes with the unconditional Gysin map Stacks.Chow.gysinChowOfInvertible of Stacks 02TO, for every pulled-back divisor; the descent condition Stacks 02S2 for the identification of the base change of the zero scheme with the zero scheme of the pulled-back section is discharged.

theorem BivariantClass.gysin_naturality_gysinChowOfInvertible
    (c : CanonicalBivariantClass C sX sY f hf p) {T : Scheme.{u}} (g : T ⟶ Y)
    [LocallyOfFiniteType g] (L : T.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible T.sheaf.obj T.ringCatSheaf.property L]
    [AlgebraicGeometry.SheafOfModules.IsInvertible (pullback f g).sheaf.obj
      (pullback f g).ringCatSheaf.property ((Scheme.Modules.pullback (pullback.snd f g)).obj L)]
    (s : Γ(L, ⊤)) (k : ℤ) :
    let D := Stacks.Divisors.zeroScheme T L s
    let L' := (Scheme.Modules.pullback (pullback.snd f g)).obj L
    let s' := AlgebraicGeometry.pullbackGlobalSections (pullback.snd f g) L s
    let E := Stacks.Divisors.zeroScheme (pullback f g) L' s'
    ∀ (e : pullback f (D.subschemeι ≫ g) ≅ E.subscheme)
      (_he : e.hom ≫ E.subschemeι = bivariantBaseChangeMap f g D.subschemeι)
      (hbase : e.hom ≫ (E.subschemeι ≫ pullback.fst f g ≫ sX) =
        pullback.fst f (D.subschemeι ≫ g) ≫ sX)
      (α : chowGroup C (g ≫ sY) (k + 1)),
      properChowPushforward C (pullback.fst f (D.subschemeι ≫ g) ≫ sX)
          (E.subschemeι ≫ pullback.fst f g ≫ sX) e.hom hbase (k - p)
          (properPushforwardDescends C _ _ _ _ _)
          (c.cap (D.subschemeι ≫ g) k (gysinChowOfInvertible C (g ≫ sY) k L s α)) =
        gysinChowOfInvertible C (pullback.fst f g ≫ sX) (k - p) L' s'
          (Eq.mp (congrArg (chowGroup C (pullback.fst f g ≫ sX))
            (by omega : (k + 1) - p = (k - p) + 1)) (c.cap g (k + 1) α))

Stacks.Chow.BivariantChowClass, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Definition.lean, line 199. The attribute's comment: “a bivariant class of degree p for f, the elements of A^p(X → Y)”.

A bivariant class c of degree p for f : X ⟶ Y: a rule assigning to every morphism g : Y' ⟶ Y locally of finite type and every k a map c ∩ - : CH_k(Y') ⟶ CH_{k-p}(X'), X' = Y' ×_Y X, such that

for h : Y'' ⟶ Y' proper, c ∩ h_* α'' = h'_* (c ∩ α''), h' : X'' ⟶ X' its base change;

for h : Y'' ⟶ Y' flat, locally of finite type, of relative dimension r, c ∩ h^* α' = (h')^* (c ∩ α');

for an invertible module L on Y' with a global section s, zero scheme i : D = Z(s) ⟶ Y', and pullback (L', s', j : E = Z(s') ⟶ X') to X', c ∩ i^* α' = j^* (c ∩ α'), the scheme D ×_Y X being identified with E by Remark 0B6Y.

The group of all of them is A^p(X ⟶ Y).

structure BivariantChowClass (C : ChowSituation.{u}) {X Y : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (f : X ⟶ Y) (hf : f ≫ sY = sX) (p : ℤ)

Stacks.Chow.BivariantChowClass.equivBivariantClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Definition.lean, line 504. The attribute's comment: “bridge: A^p(X → Y) is BivariantClass at the Gysin system of the first Chern class”.

A bivariant class of degree p for f is the same thing as a Stacks.Chow.BivariantClass at the Gysin system Stacks.Chow.gysinSystemOfInvertible of the first Chern class; the cap operations correspond identically.

def equivBivariantClass :
    BivariantChowClass C sX sY f hf p ≃ BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p

Stacks.Chow.BivariantClass.proper_naturality_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/VanishingUnconditional.lean, line 61. The attribute's comment: “the proper pushforward axiom, with the descent condition Stacks 02S2 discharged”.

Capping with a bivariant class commutes with proper pushforward along a proper morphism h : T' ⟶ T of test schemes and its base change h', pushforward being taken with the descent of Stacks 02S2, Stacks.Chow.properPushforwardFactorsThroughRationalEquivalence_of_isProper.

theorem BivariantClass.proper_naturality_of_isProper (c : BivariantClass C G sX sY f hf p)
    {T T' : Scheme.{u}} (g : T ⟶ Y) [LocallyOfFiniteType g] (h : T' ⟶ T) [IsProper h]
    (h' : pullback f (h ≫ g) ⟶ pullback f g)
    (sq : IsPullback (pullback.snd f (h ≫ g)) h' h (pullback.snd f g))
    (hfst : h' ≫ pullback.fst f g = pullback.fst f (h ≫ g)) (k : ℤ)
    (α : chowGroup C ((h ≫ g) ≫ sY) k) :
    letI : IsProper h' := MorphismProperty.of_isPullback sq (P := @IsProper) inferInstance
    c.cap g k (properChowPushforward C ((h ≫ g) ≫ sY) (g ≫ sY) h
        (by simp [Category.assoc]) k
        (properPushforwardFactorsThroughRationalEquivalence_of_isProper C ((h ≫ g) ≫ sY)
          (g ≫ sY) h (by simp [Category.assoc]) k) α) =
      properChowPushforward C (pullback.fst f (h ≫ g) ≫ sX) (pullback.fst f g ≫ sX) h'
        (by rw [← Category.assoc, hfst]) (k - p)
        (properPushforwardFactorsThroughRationalEquivalence_of_isProper C
          (pullback.fst f (h ≫ g) ≫ sX) (pullback.fst f g ≫ sX) h'
          (by rw [← Category.assoc, hfst]) (k - p)) (c.cap (h ≫ g) k α)

Tag 0B78, a lemma

Tag 0B78 in the Stacks Project.

Stacks.Chow.flatPullbackBivariantCap_flat_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FlatPullback.lean, line 329. The attribute's comment: “the flat-pullback condition of Stacks 0B76 for the flat-pullback rule, from Stacks 02RD, with the Stacks 02S1 descent hypothesis bundled; the rule is Stacks.Chow.flatPullbackBivariantCap, and it is not assembled into a term of Stacks.Chow.BivariantClass here because the proper condition is Stacks 02RG and the Gysin condition is Stacks 0B71, neither of which this repository carries”.

Stacks 0B78. The flat-pullback condition of Stacks 0B76 for the rule of Stacks 0B78: the rule α ↦ (f')^* α commutes with flat pullback of fixed relative dimension along a morphism h : T' ⟶ T of test schemes.

The base change of f over T' followed by h, and the base change of h followed by the base change of f over T, are the same morphism T' ×_Y X ⟶ T, because the two cartesian squares paste; Stacks 02RD then traverses that morphism both ways. The two sides land in degrees (k + s) - (-r) and (k - (-r)) + s, so the identity is a heterogeneous equality, exactly as the corresponding field of Stacks.Chow.BivariantClass is.

theorem flatPullbackBivariantCap_flat_naturality {T T' : Scheme.{u}} (g : T ⟶ Y)
    [LocallyOfFiniteType g] (h : T' ⟶ T) [LocallyOfFiniteType h] [Flat h] (s : ℕ)
    (hs : AlgebraicGeometry.RelativeDimension h s)
    (h' : pullback f (h ≫ g) ⟶ pullback f g) [LocallyOfFiniteType h'] [Flat h']
    (sq : IsPullback (pullback.snd f (h ≫ g)) h' h (pullback.snd f g))
    (hfst : h' ≫ pullback.fst f g = pullback.fst f (h ≫ g)) (k : ℤ)
    (hs' : AlgebraicGeometry.RelativeDimension h' s)
    (hfac : FlatPullbackFactorsThroughRationalEquivalence C ((h ≫ g) ≫ sY) (g ≫ sY) h
      (by simp [Category.assoc]) s hs k)
    (hfac' : FlatPullbackFactorsThroughRationalEquivalence C (pullback.fst f (h ≫ g) ≫ sX)
      (pullback.fst f g ≫ sX) h' (by rw [← Category.assoc, hfst]) s hs' (k - -(r : ℤ)))
    (α : chowGroup C (g ≫ sY) k) :
    flatPullbackBivariantCap C sX sY f hf r hfr hfp (h ≫ g) (k + (s : ℤ))
          (flatPullbackChow C ((h ≫ g) ≫ sY) (g ≫ sY) h (by simp [Category.assoc]) s hs k
            hfac α) ≍
      flatPullbackChow C (pullback.fst f (h ≫ g) ≫ sX) (pullback.fst f g ≫ sX) h'
        (by rw [← Category.assoc, hfst]) s hs' (k - -(r : ℤ)) hfac'
        (flatPullbackBivariantCap C sX sY f hf r hfr hfp g k α)

Stacks.Chow.flatPullbackBivariantChowClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FlatPullbackChowClass.lean, line 72. The attribute's comment: “the flat-pullback rule as an element of A^{-r}(X → Y), the group of Stacks 0B76 whose three conditions use the genuine proper pushforward, flat pullback and Gysin map; its cap operation is flat pullback along the base change of f (flatPullbackBivariantChowClass_cap)”.

Stacks 0B78. For f : X ⟶ Y flat of relative dimension r between schemes locally of finite type over S, the rule which assigns to g : Y' ⟶ Y the flat pullback (f')^* : CH_k(Y') ⟶ CH_{k+r}(X ×_Y Y') along the base change of f is a bivariant class of degree -r, the class f^* ∈ A^{-r}(X ⟶ Y).

def flatPullbackBivariantChowClass : BivariantChowClass C sX sY f hf (-(r : ℤ))

Stacks.Chow.existsUnique_bivariantChowClass_cap_eq_flatPullbackChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FlatPullbackChowClassUnique.lean, line 74. The attribute's comment: “the flat-pullback rule is a bivariant class of degree -r, with nothing assumed: exactly one element of A^{-r}(X → Y), the group of Stacks 0B76 whose three conditions use the genuine proper pushforward, flat pullback and Gysin map, caps by (f')^*”.

Stacks 0B78. Let f : X ⟶ Y be flat of relative dimension r between schemes locally of finite type over S. The rule which assigns to g : Y' ⟶ Y the flat pullback (f')^* : CH_k(Y') ⟶ CH_{k+r}(X') along the base change f' : X' = X ×_Y Y' ⟶ Y' of f is a bivariant class of degree -r: there is exactly one c ∈ A^{-r}(X ⟶ Y) whose cap operation is that rule, read in degree k - (-r) = k + r.

theorem existsUnique_bivariantChowClass_cap_eq_flatPullbackChow :
    ∃! c : BivariantChowClass C sX sY f hf (-(r : ℤ)),
      ∀ {T : Scheme.{u}} (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (g ≫ sY) k),
        c.cap g k α =
          chowGroupDegreeEquiv C (pullback.fst f g ≫ sX) (by ring : k + (r : ℤ) = k - -(r : ℤ))
            (flatPullbackChow C (pullback.fst f g ≫ sX) (g ≫ sY) (pullback.snd f g)
              (pullbackSnd_comp_structureMorphism_eq C sX sY f hf g) r
              (relativeDimension_pullback_snd f g r hfr) k
              (flatPullbackFactorsThroughRationalEquivalence_general C _ _ _ _ _ _ _) α)

Stacks.Chow.exists_bivariantChowClass_cap_heq_flatPullbackChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FlatPullbackChowClassUnique.lean, line 97. The attribute's comment: “the flat-pullback rule (f')^* : CH_k(Y') → CH_{k+r}(X') is the cap operation of an element of A^{-r}(X → Y), with nothing assumed, read in degree k + r as the source writes it”.

Stacks 0B78, with the degree transport removed. For f : X ⟶ Y flat of relative dimension r, there is a bivariant class c ∈ A^{-r}(X ⟶ Y) whose cap operation on CH_k(Y') is the flat pullback (f')^* : CH_k(Y') ⟶ CH_{k+r}(X') along the base change of f, landing in degree k + r exactly as in the source. The two degrees k + r and k - (-r) are equal integers that are not the same term, so the identity is a heterogeneous equality.

theorem exists_bivariantChowClass_cap_heq_flatPullbackChow :
    ∃ c : BivariantChowClass C sX sY f hf (-(r : ℤ)),
      ∀ {T : Scheme.{u}} (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (g ≫ sY) k),
        c.cap g k α ≍
          flatPullbackChow C (pullback.fst f g ≫ sX) (g ≫ sY) (pullback.snd f g)
            (pullbackSnd_comp_structureMorphism_eq C sX sY f hf g) r
            (relativeDimension_pullback_snd f g r hfr) k
            (flatPullbackFactorsThroughRationalEquivalence_general C _ _ _ _ _ _ _) α

Stacks.Chow.existsUnique_bivariantClass_isBivariantFlatPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FlatPullbackChowClassUnique.lean, line 114. The attribute's comment: “exactly one bivariant class of degree -r, at the Gysin system of the first Chern class, satisfies the characterization Stacks.Chow.IsBivariantFlatPullback, with nothing assumed”.

Stacks 0B78 for Stacks.Chow.BivariantClass at the Gysin system of the first Chern class of an invertible module: exactly one bivariant class of degree -r for f caps by flat pullback along the base change of f, in the sense of Stacks.Chow.IsBivariantFlatPullback.

theorem existsUnique_bivariantClass_isBivariantFlatPullback :
    ∃! c : BivariantClass C (gysinSystemOfInvertible C) sX sY f hf (-(r : ℤ)),
      IsBivariantFlatPullback C (gysinSystemOfInvertible C) sX sY f hf r hfr
        (flatPullbackDescends C) c

Stacks.Chow.flatPullbackBivariantClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FlatPullbackClass.lean, line 493. The attribute's comment: “with Stacks 02S1 as hS1, Stacks 02RG as hRG and Stacks 0B71 as h71”.

Stacks 0B78. For f : X ⟶ Y flat of relative dimension r between schemes locally of finite type over the base, the rule which assigns to a test scheme g : T ⟶ Y the flat pullback A_k(T) ⟶ A_{k+r}(X ×_Y T) along the base change of f is a bivariant class of degree -r for f.

The three inputs of the source that this repository does not have are the named hypotheses hS1 (Stacks 02S1), hRG (Stacks 02RG) and h71 (Stacks 0B71, with the identification of Stacks 0B6Y). The fourth, Stacks 02RD, is proved here, as is Stacks 02NK; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.Bivariant.FlatPullbackClass.

def flatPullbackBivariantClass (hRG : ProperPushforwardFlatPullbackBaseChange C)
    (h71 : G.FlatPullbackNaturality r) :
    BivariantClass C G sX sY f hf (-(r : ℤ))

Stacks.Chow.flatPullbackBivariantCap_proper_naturality_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FlatPullbackProperPushforward.lean, line 72. The attribute's comment: “the proper-pushforward condition of Stacks 0B76 for the flat-pullback rule, with NOTHING ASSUMED: Stacks 02RG on Chow groups is the theorem Stacks.Chow.properPushforwardFlatPullbackBaseChange above, and the Stacks 02S1 descent along which the rule is formed is the theorem Stacks.Chow.flatPullbackDescends”.

The proper-pushforward condition of Stacks 0B76 (1) for the flat-pullback rule of Stacks 0B78: flat pullback along the base change of a flat f : X ⟶ Y of relative dimension r commutes with proper pushforward along a proper morphism h : T' ⟶ T of test schemes over Y.

theorem flatPullbackBivariantCap_proper_naturality_unconditional (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
    [LocallyOfFiniteType sY] (f : X ⟶ Y) [LocallyOfFiniteType f] [Flat f] (hf : f ≫ sY = sX)
    (r : ℕ) (hfr : AlgebraicGeometry.RelativeDimension f r) {T T' : Scheme.{u}} (g : T ⟶ Y)
    [LocallyOfFiniteType g] (h : T' ⟶ T) [IsProper h]
    (h' : pullback f (h ≫ g) ⟶ pullback f g) [IsProper h']
    (sq : IsPullback (pullback.snd f (h ≫ g)) h' h (pullback.snd f g))
    (hfst : h' ≫ pullback.fst f g = pullback.fst f (h ≫ g)) (k : ℤ)
    (hfac : ProperPushforwardFactorsThroughRationalEquivalence C ((h ≫ g) ≫ sY) (g ≫ sY) h
      (by simp [Category.assoc]) k)
    (hfac' : ProperPushforwardFactorsThroughRationalEquivalence C
      (pullback.fst f (h ≫ g) ≫ sX) (pullback.fst f g ≫ sX) h'
      (by rw [← Category.assoc, hfst]) (k - -(r : ℤ)))
    (α : chowGroup C ((h ≫ g) ≫ sY) k) :
    flatPullbackBivariantCap C sX sY f hf r hfr (flatPullbackDescends C) g k
        (properChowPushforward C ((h ≫ g) ≫ sY) (g ≫ sY) h (by simp [Category.assoc]) k hfac
          α) =
      properChowPushforward C (pullback.fst f (h ≫ g) ≫ sX) (pullback.fst f g ≫ sX) h'
        (by rw [← Category.assoc, hfst]) (k - -(r : ℤ)) hfac'
        (flatPullbackBivariantCap C sX sY f hf r hfr (flatPullbackDescends C) (h ≫ g) k α)

Stacks.Chow.flatPullbackBivariantClassOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FlatPullbackProperPushforward.lean, line 104. The attribute's comment: “the flat-pullback rule IS a bivariant class of degree -r, with NOTHING ASSUMED: the Stacks 02S1 descent is the theorem Stacks.Chow.flatPullbackDescends, Stacks 02RG on Chow groups is the theorem Stacks.Chow.properPushforwardFlatPullbackBaseChange above, and Stacks 0B71 with the identification of Stacks 0B6Y is the theorem Stacks.Chow.gysinSystemOfInvertible_flatPullbackNaturalityAtZeroSchemeComparison”.

For f : X ⟶ Y flat of relative dimension r between schemes locally of finite type over the base, the rule which assigns to a test scheme g : T ⟶ Y the flat pullback A_k(T) ⟶ A_{k+r}(X ×_Y T) along the base change of f, as a bivariant class of degree -r for f over the Gysin system Stacks.Chow.gysinSystemOfInvertible.

def flatPullbackBivariantClassOfInvertible (C : ChowSituation.{u}) {X Y : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : X ⟶ Y)
    [LocallyOfFiniteType f] [Flat f] (hf : f ≫ sY = sX) (r : ℕ)
    (hfr : AlgebraicGeometry.RelativeDimension f r) :
    BivariantClass C (gysinSystemOfInvertible C) sX sY f hf (-(r : ℤ))

Stacks.Chow.isBivariantFlatPullback_flatPullbackBivariantClassOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FlatPullbackProperPushforward.lean, line 138. The attribute's comment: “the class of the same tag constructed above satisfies the characterization Stacks.Chow.IsBivariantFlatPullback, with NOTHING ASSUMED, so that the uniqueness statement Stacks.Chow.eq_of_isBivariantFlatPullback is about a nonempty collection”.

The class Stacks.Chow.flatPullbackBivariantClassOfInvertible is the flat-pullback class in the sense of Stacks.Chow.IsBivariantFlatPullback: on every test scheme its cap operation is flat pullback along the base change of f.

theorem isBivariantFlatPullback_flatPullbackBivariantClassOfInvertible (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
    [LocallyOfFiniteType sY] (f : X ⟶ Y) [LocallyOfFiniteType f] [Flat f] (hf : f ≫ sY = sX)
    (r : ℕ) (hfr : AlgebraicGeometry.RelativeDimension f r) :
    IsBivariantFlatPullback C (gysinSystemOfInvertible C) sX sY f hf r hfr
      (flatPullbackDescends C) (flatPullbackBivariantClassOfInvertible C sX sY f hf r hfr)

Stacks.Chow.completedFlatPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedFlatPullback.lean, line 164. The attribute's comment: “flat pullback along a flat morphism whose relative dimension is constant on each connected component, in the completed bivariant group A^*(X → Y)^∧”.

f^* ∈ A^*(X ⟶ Y)^∧ for a flat morphism f (Stacks 0B78 on completions). For a flat morphism whose restriction to every connected component X_a of X has pure relative dimension r_a, the flat-pullback class in the completed bivariant group of Stacks 0FE0: on X_a it is the class of Stacks 0B78 of the restriction X_a ⟶ Y_{a'} of f, placed in degree -r_a. Every input of Stacks 0B78 is discharged.

def completedFlatPullback [IsLocallyNoetherian X] [IsLocallyNoetherian Y]
    (hrel : ∀ a : _root_.ConnectedComponents X,
      ∃ r : ℕ, AlgebraicGeometry.RelativeDimension (f.resConnectedComponent a) r) :
    completedBivariantGroup C (gysinSystemOfInvertible C) sX sY f hf

Tag 0B79, a lemma

Tag 0B79 in the Stacks Project.

Stacks.Chow.gysinBivariantClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/GysinClass.lean, line 540.

Let (𝓛, s, i : D ⟶ X) be a triple as in Definition 02T8 on a scheme X locally of finite type over the base. The rule assigning to every g : X' ⟶ X locally of finite type the Gysin map (i')^* : CH_k(X') ⟶ CH_{k-1}(D') of the pulled-back section, where D' = D ×_X X', is a bivariant class of degree 1 for i: the class below caps by that Gysin map on every test scheme.

def gysinBivariantClass :
    { c : BivariantClass C (gysinSystemOfInvertible C) (gysinTripleInclusion L s ≫ sX) sX
        (gysinTripleInclusion L s) rfl 1 //
      IsGysinBivariantClass C (gysinSystemOfInvertible C) sX L s c }

Tag 0EPK, a lemma

Tag 0EPK in the Stacks Project.

Stacks.Chow.isProper_bivariantPushforwardBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforward.lean, line 210. The attribute's comment: “properness of the base change of the proper morphism”.

Stacks 0EPK. The base change of a proper morphism along a test scheme is proper, so the rule of Stacks 0EPK can push forward along it.

instance isProper_bivariantPushforwardBaseChange {X Y Z T : Scheme.{u}} (f : X ⟶ Y) [IsProper f]
    (g : Y ⟶ Z) (t : T ⟶ Z) : IsProper (bivariantPushforwardBaseChange f g t)

Stacks.Chow.bivariantProperPushforwardCap_proper_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforward.lean, line 256. The attribute's comment: “the proper-pushforward axiom of the pushed-forward class”.

Stacks 0EPK. The proper-pushforward axiom of Stacks 0B76 for the rule of Stacks 0EPK: the cap operation α ↦ f'_*(c ∩ α) commutes with proper pushforward along a morphism of test schemes.

theorem bivariantProperPushforwardCap_proper_naturality {T T' : Scheme.{u}} (t : T ⟶ Z)
    [LocallyOfFiniteType t] (h : T' ⟶ T) [IsProper h]
    (h' : pullback g (h ≫ t) ⟶ pullback g t)
    (sq : IsPullback (pullback.snd g (h ≫ t)) h' h (pullback.snd g t))
    (hfst : h' ≫ pullback.fst g t = pullback.fst g (h ≫ t)) (k : ℤ)
    (α : chowGroup C ((h ≫ t) ≫ sZ) k) :
    letI : IsProper h' := MorphismProperty.of_isPullback sq (P := @IsProper) inferInstance
    bivariantProperPushforwardCap C G sX sY sZ f g hf hg hpp p c t k
        (properChowPushforward C ((h ≫ t) ≫ sZ) (t ≫ sZ) h (by simp [Category.assoc]) k
          (hpp _ _ _ _ _) α) =
      properChowPushforward C (pullback.fst g (h ≫ t) ≫ sY) (pullback.fst g t ≫ sY) h'
        (by rw [← Category.assoc, hfst]) (k - p) (hpp _ _ _ _ _)
        (bivariantProperPushforwardCap C G sX sY sZ f g hf hg hpp p c (h ≫ t) k α)

Stacks.Chow.eq_of_isBivariantProperPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforward.lean, line 319. The attribute's comment: “uniqueness of the pushed-forward class”.

Stacks 0EPK. The rule of Stacks 0EPK determines the pushed-forward class: two bivariant classes that both push c forward along f are equal.

theorem eq_of_isBivariantProperPushforward
    (h : IsBivariantProperPushforward C G sX sY sZ f g hf hg hpp p c d)
    (h' : IsBivariantProperPushforward C G sX sY sZ f g hf hg hpp p c d') : d = d'

Stacks.Chow.canonicalBivariantProperPushforwardCap_gysin_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardCanonical.lean, line 86. The attribute's comment: “the Gysin axiom of Stacks 0B76 for the rule α ↦ f'_*(c ∩ α)”.

Stacks 0EPK, the Gysin axiom. For c ∈ A^p(X ⟶ Z) and f proper, the rule α ↦ f'_*(c ∩ α) commutes with the Gysin map i^* of Stacks 02TO of the zero scheme of a section of an invertible module on a test scheme: pushing f'_*(c ∩ i^* α) to the zero scheme of the pulled-back section on T ×_Z Y gives i'^* f'_*(c ∩ α).

theorem canonicalBivariantProperPushforwardCap_gysin_naturality
    (c : CanonicalBivariantClass C sX sZ (f ≫ g) (comp_comp_structureMorphism_eq hf hg) p)
    {T : Scheme.{u}} (t : T ⟶ Z) [LocallyOfFiniteType t] (L : T.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible T.sheaf.obj T.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) (k : ℤ) :
    let D := Stacks.Divisors.zeroScheme T L s
    let L' := (Scheme.Modules.pullback (pullback.snd g t)).obj L
    let s' := AlgebraicGeometry.pullbackGlobalSections (pullback.snd g t) L s
    let E := Stacks.Divisors.zeroScheme (pullback g t) L' s'
    ∀ (e : pullback g (D.subschemeι ≫ t) ≅ E.subscheme)
      (_he : e.hom ≫ E.subschemeι = bivariantBaseChangeMap g t D.subschemeι)
      (hbase : e.hom ≫ (E.subschemeι ≫ pullback.fst g t ≫ sY) =
        pullback.fst g (D.subschemeι ≫ t) ≫ sY)
      (α : chowGroup C (t ≫ sZ) (k + 1)),
      properChowPushforward C (pullback.fst g (D.subschemeι ≫ t) ≫ sY)
          (E.subschemeι ≫ pullback.fst g t ≫ sY) e.hom hbase (k - p)
          (properPushforwardDescends C _ _ _ _ _)
          (bivariantProperPushforwardCap C (canonicalGysinSystem C) sX sY sZ f g hf hg
            (properPushforwardDescends C) p c (D.subschemeι ≫ t) k
            (gysinChowOfInvertible C (t ≫ sZ) k L s α)) =
        gysinChowOfInvertible C (pullback.fst g t ≫ sY) (k - p) L' s'
          (Eq.mp (congrArg (chowGroup C (pullback.fst g t ≫ sY))
              (by omega : (k + 1) - p = (k - p) + 1))
            (bivariantProperPushforwardCap C (canonicalGysinSystem C) sX sY sZ f g hf hg
              (properPushforwardDescends C) p c t (k + 1) α))

Stacks.Chow.canonicalBivariantProperPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardCanonical.lean, line 125.

Stacks 0EPK. For f : X ⟶ Y proper, g : Y ⟶ Z and c ∈ A^p(X ⟶ Z), the rule which to a test scheme t : T ⟶ Z assigns α ↦ f'_*(c ∩ α), with f' : T ×_Z X ⟶ T ×_Z Y the base change of f, is a bivariant class f_* ∘ c ∈ A^p(Y ⟶ Z). Its cap formula is Stacks.Chow.canonicalBivariantProperPushforward_cap.

def canonicalBivariantProperPushforward
    (c : CanonicalBivariantClass C sX sZ (f ≫ g) (comp_comp_structureMorphism_eq hf hg) p) :
    CanonicalBivariantClass C sY sZ g hg p

Stacks.Chow.existsUnique_canonicalBivariantProperPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardCanonical.lean, line 149. The attribute's comment: “existence and uniqueness of f_* ∘ c with its cap formula”.

Stacks 0EPK. For f : X ⟶ Y proper, g : Y ⟶ Z and c ∈ A^p(X ⟶ Z) there is exactly one bivariant class f_* ∘ c ∈ A^p(Y ⟶ Z) whose cap operation is α ↦ f'_*(c ∩ α) on every test scheme t : T ⟶ Z, with f' : T ×_Z X ⟶ T ×_Z Y the base change of f.

theorem existsUnique_canonicalBivariantProperPushforward
    (c : CanonicalBivariantClass C sX sZ (f ≫ g) (comp_comp_structureMorphism_eq hf hg) p) :
    ∃! d : CanonicalBivariantClass C sY sZ g hg p,
      ∀ {T : Scheme.{u}} (t : T ⟶ Z) [LocallyOfFiniteType t] (k : ℤ)
        (α : chowGroup C (t ≫ sZ) k),
        d.cap t k α =
          properChowPushforward C (pullback.fst (f ≫ g) t ≫ sX) (pullback.fst g t ≫ sY)
            (bivariantPushforwardBaseChange f g t)
            (bivariantPushforwardBaseChange_comp_structure hf g t) (k - p)
            (properPushforwardDescends C _ _ _ _ _) (c.cap t k α)

Stacks.Chow.bivariantProperPushforwardCap_flat_naturality_of_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardFlatPullback.lean, line 119. The attribute's comment: “the flat-pullback axiom of the pushed-forward class”.

Stacks 0EPK. The flat-pullback axiom of Stacks 0B76 for the rule of Stacks 0EPK: the cap operation α ↦ f'_*(c ∩ α) commutes with flat pullback of fixed relative dimension along a morphism of test schemes.

The degrees are (k + r) - p on the left and (k - p) + r on the right, the same integer written two ways, which is why the conclusion is an HEq.

theorem bivariantProperPushforwardCap_flat_naturality_of_factors {T T' : Scheme.{u}} (t : T ⟶ Z)
    [LocallyOfFiniteType t] (h : T' ⟶ T) [LocallyOfFiniteType h] [Flat h] (r : ℕ)
    (hr : AlgebraicGeometry.RelativeDimension h r)
    (h' : pullback g (h ≫ t) ⟶ pullback g t)
    (sq : IsPullback (pullback.snd g (h ≫ t)) h' h (pullback.snd g t))
    (hfst : h' ≫ pullback.fst g t = pullback.fst g (h ≫ t)) (k : ℤ)
    (hr' : letI : LocallyOfFiniteType h' :=
        MorphismProperty.of_isPullback sq (P := @LocallyOfFiniteType) inferInstance
      AlgebraicGeometry.RelativeDimension h' r)
    (hfac : FlatPullbackFactorsThroughRationalEquivalence C ((h ≫ t) ≫ sZ) (t ≫ sZ) h
      (by simp [Category.assoc]) r hr k)
    (hfac' : letI : LocallyOfFiniteType h' :=
          MorphismProperty.of_isPullback sq (P := @LocallyOfFiniteType) inferInstance
        letI : Flat h' := MorphismProperty.of_isPullback sq (P := @Flat) inferInstance
      FlatPullbackFactorsThroughRationalEquivalence C (pullback.fst g (h ≫ t) ≫ sY)
        (pullback.fst g t ≫ sY) h' (by rw [← Category.assoc, hfst]) r hr' (k - p))
    (α : chowGroup C (t ≫ sZ) k) :
    letI : LocallyOfFiniteType h' :=
      MorphismProperty.of_isPullback sq (P := @LocallyOfFiniteType) inferInstance
    letI : Flat h' := MorphismProperty.of_isPullback sq (P := @Flat) inferInstance
    bivariantProperPushforwardCap C G sX sY sZ f g hf hg hpp p c (h ≫ t) (k + (r : ℤ))
        (flatPullbackChow C ((h ≫ t) ≫ sZ) (t ≫ sZ) h (by simp [Category.assoc]) r hr k
          hfac α) ≍
      flatPullbackChow C (pullback.fst g (h ≫ t) ≫ sY) (pullback.fst g t ≫ sY) h'
        (by rw [← Category.assoc, hfst]) r hr' (k - p) hfac'
        (bivariantProperPushforwardCap C G sX sY sZ f g hf hg hpp p c t k α)

Stacks.Chow.bivariantProperPushforwardCap_proper_naturality_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardUnconditional.lean, line 70. The attribute's comment: “the proper-pushforward axiom of the pushed-forward class, with NOTHING ASSUMED: the descent of Stacks 02S2 is the theorem Stacks.Chow.properPushforwardDescends”.

The proper-pushforward axiom of Stacks 0B76 for the rule of Stacks 0EPK, with proper pushforward on Chow groups taken along the descent Stacks.Chow.properPushforwardDescends.

theorem bivariantProperPushforwardCap_proper_naturality_unconditional {T T' : Scheme.{u}}
    (t : T ⟶ Z) [LocallyOfFiniteType t] (h : T' ⟶ T) [IsProper h]
    (h' : pullback g (h ≫ t) ⟶ pullback g t)
    (sq : IsPullback (pullback.snd g (h ≫ t)) h' h (pullback.snd g t))
    (hfst : h' ≫ pullback.fst g t = pullback.fst g (h ≫ t)) (k : ℤ)
    (α : chowGroup C ((h ≫ t) ≫ sZ) k) :
    letI : IsProper h' := MorphismProperty.of_isPullback sq (P := @IsProper) inferInstance
    bivariantProperPushforwardCap C G sX sY sZ f g hf hg (properPushforwardDescends C) p c t k
        (properChowPushforward C ((h ≫ t) ≫ sZ) (t ≫ sZ) h (by simp [Category.assoc]) k
          (properPushforwardDescends C _ _ _ _ _) α) =
      properChowPushforward C (pullback.fst g (h ≫ t) ≫ sY) (pullback.fst g t ≫ sY) h'
        (by rw [← Category.assoc, hfst]) (k - p) (properPushforwardDescends C _ _ _ _ _)
        (bivariantProperPushforwardCap C G sX sY sZ f g hf hg (properPushforwardDescends C) p c
          (h ≫ t) k α)

Stacks.Chow.bivariantProperPushforwardCap_flat_naturality_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardUnconditional.lean, line 95. The attribute's comment: “the flat-pullback axiom of the pushed-forward class, with NOTHING ASSUMED: Stacks 02RG on Chow groups is the theorem Stacks.Chow.properPushforwardFlatPullbackBaseChange, and the two descents are Stacks.Chow.flatPullbackDescends and Stacks.Chow.properPushforwardDescends”.

The flat-pullback axiom of Stacks 0B76 for the rule of Stacks 0EPK, with flat pullback and proper pushforward on Chow groups taken along the descents Stacks.Chow.flatPullbackDescends and Stacks.Chow.properPushforwardDescends, and the relative dimension of the base change given by Stacks 02NK.

theorem bivariantProperPushforwardCap_flat_naturality_unconditional {T T' : Scheme.{u}}
    (t : T ⟶ Z) [LocallyOfFiniteType t] (h : T' ⟶ T) [LocallyOfFiniteType h] [Flat h] (r : ℕ)
    (hr : AlgebraicGeometry.RelativeDimension h r)
    (h' : pullback g (h ≫ t) ⟶ pullback g t)
    (sq : IsPullback (pullback.snd g (h ≫ t)) h' h (pullback.snd g t))
    (hfst : h' ≫ pullback.fst g t = pullback.fst g (h ≫ t)) (k : ℤ)
    (α : chowGroup C (t ≫ sZ) k) :
    letI : LocallyOfFiniteType h' :=
      MorphismProperty.of_isPullback sq (P := @LocallyOfFiniteType) inferInstance
    letI : Flat h' := MorphismProperty.of_isPullback sq (P := @Flat) inferInstance
    HEq
      (bivariantProperPushforwardCap C G sX sY sZ f g hf hg (properPushforwardDescends C) p c
        (h ≫ t) (k + (r : ℤ))
        (flatPullbackChow C ((h ≫ t) ≫ sZ) (t ≫ sZ) h (by simp [Category.assoc]) r hr k
          (flatPullbackDescends C _ _ _ _ _ _ _) α))
      (flatPullbackChow C (pullback.fst g (h ≫ t) ≫ sY) (pullback.fst g t ≫ sY) h'
        (by rw [← Category.assoc, hfst]) r
        (AlgebraicGeometry.RelativeDimension.of_isPullback sq hr) (k - p)
        (flatPullbackDescends C _ _ _ _ _ _ _)
        (bivariantProperPushforwardCap C G sX sY sZ f g hf hg (properPushforwardDescends C) p c t k
          α))

Stacks.Chow.bivariantProperPushforwardCap_gysin_naturality_ofInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardUnconditional.lean, line 142. The attribute's comment: “the Gysin axiom of the pushed-forward class at the Gysin system of the first Chern class rule, with NOTHING ASSUMED: Stacks 02TA for that Gysin system is a pair of theorems here, the identification is Stacks 0B6Y, and the descent of Stacks 02S2 is Stacks.Chow.properPushforwardDescends”.

The Gysin axiom of Stacks 0B76 for the rule of Stacks 0EPK at the Gysin system Stacks.Chow.gysinSystemOfInvertible of the first Chern class rule, with proper pushforward on Chow groups taken along the descent Stacks.Chow.properPushforwardDescends.

theorem bivariantProperPushforwardCap_gysin_naturality_ofInvertible {T : Scheme.{u}} (t : T ⟶ Z)
    [LocallyOfFiniteType t] (L : T.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible T.sheaf.obj T.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) (k : ℤ)
    (e : pullback g ((Stacks.Divisors.zeroScheme T L s).subschemeι ≫ t) ≅
      (Stacks.Divisors.zeroScheme (pullback g t)
        ((Scheme.Modules.pullback (pullback.snd g t)).obj L)
        (AlgebraicGeometry.pullbackGlobalSections (pullback.snd g t) L s)).subscheme)
    (he : e.hom ≫ (Stacks.Divisors.zeroScheme (pullback g t)
        ((Scheme.Modules.pullback (pullback.snd g t)).obj L)
        (AlgebraicGeometry.pullbackGlobalSections (pullback.snd g t) L s)).subschemeι =
      bivariantBaseChangeMap g t (Stacks.Divisors.zeroScheme T L s).subschemeι)
    (hbase : e.hom ≫ ((Stacks.Divisors.zeroScheme (pullback g t)
        ((Scheme.Modules.pullback (pullback.snd g t)).obj L)
        (AlgebraicGeometry.pullbackGlobalSections (pullback.snd g t) L s)).subschemeι ≫
        pullback.fst g t ≫ sY) =
      pullback.fst g ((Stacks.Divisors.zeroScheme T L s).subschemeι ≫ t) ≫ sY)
    (α : chowGroup C (t ≫ sZ) (k + 1)) :
    properChowPushforward C
        (pullback.fst g ((Stacks.Divisors.zeroScheme T L s).subschemeι ≫ t) ≫ sY)
        ((Stacks.Divisors.zeroScheme (pullback g t)
          ((Scheme.Modules.pullback (pullback.snd g t)).obj L)
          (AlgebraicGeometry.pullbackGlobalSections (pullback.snd g t) L s)).subschemeι ≫
          pullback.fst g t ≫ sY) e.hom hbase (k - p)
        (properPushforwardDescends C _ _ _ _ _)
        (bivariantProperPushforwardCap C (gysinSystemOfInvertible C) sX sY sZ f g hf hg
          (properPushforwardDescends C) p c
          ((Stacks.Divisors.zeroScheme T L s).subschemeι ≫ t) k
          ((gysinSystemOfInvertible C).onChow (t ≫ sZ) L s k α)) =
      (gysinSystemOfInvertible C).onChow (pullback.fst g t ≫ sY)
        ((Scheme.Modules.pullback (pullback.snd g t)).obj L)
        (AlgebraicGeometry.pullbackGlobalSections (pullback.snd g t) L s) (k - p)
        (Eq.mp (congrArg (chowGroup C (pullback.fst g t ≫ sY))
          (by omega : k + 1 - p = k - p + 1))
          (bivariantProperPushforwardCap C (gysinSystemOfInvertible C) sX sY sZ f g hf hg
            (properPushforwardDescends C) p c t (k + 1) α))

Stacks.Chow.bivariantProperPushforwardOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardUnconditional.lean, line 191. The attribute's comment: “the pushed-forward class f_* ∘ c itself, at the Gysin system of the first Chern class rule, with NOTHING ASSUMED: the rule of the lemma IS a bivariant class, so the three axioms of Stacks 0B76 for it are the three fields of this term, and Stacks 02RG, Stacks 02TA for this Gysin system and Stacks 02S2 are all theorems of this repository”.

The proper pushforward f_* ∘ c ∈ A^p(Y ⟶ Z) of a bivariant class c ∈ A^p(X ⟶ Z) along a proper f : X ⟶ Y, at the Gysin system of the first Chern class rule: the bivariant class whose cap operation is the rule α ↦ f'_*(c ∩ α) of Stacks.Chow.bivariantProperPushforwardCap.

def bivariantProperPushforwardOfInvertible :
    BivariantClass C (gysinSystemOfInvertible C) sY sZ g hg p

Stacks.Chow.isBivariantProperPushforward_bivariantProperPushforwardOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardUnconditional.lean, line 204. The attribute's comment: “the constructed class satisfies the characterization Stacks.Chow.IsBivariantProperPushforward of the same tag, with NOTHING ASSUMED, so the uniqueness statement is about a nonempty collection”.

The class Stacks.Chow.bivariantProperPushforwardOfInvertible caps by the rule α ↦ f'_*(c ∩ α), so it is the proper pushforward of c in the sense of Stacks.Chow.IsBivariantProperPushforward.

theorem isBivariantProperPushforward_bivariantProperPushforwardOfInvertible :
    IsBivariantProperPushforward C (gysinSystemOfInvertible C) sX sY sZ f g hf hg
      (properPushforwardDescends C) p c
      (bivariantProperPushforwardOfInvertible C sX sY sZ f g hf hg p c)

Stacks.Chow.exists_isBivariantProperPushforward_ofInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardUnconditional.lean, line 218. The attribute's comment: “existence of the pushed-forward class at the Gysin system of the first Chern class rule, with NOTHING ASSUMED”.

For a proper f : X ⟶ Y, a morphism g : Y ⟶ Z and a bivariant class c of degree p for f ≫ g against the Gysin system of the first Chern class rule, there is a bivariant class of degree p for g whose cap operation is α ↦ f'_*(c ∩ α).

theorem exists_isBivariantProperPushforward_ofInvertible :
    ∃ d : BivariantClass C (gysinSystemOfInvertible C) sY sZ g hg p,
      IsBivariantProperPushforward C (gysinSystemOfInvertible C) sX sY sZ f g hf hg
        (properPushforwardDescends C) p c d

Stacks.Chow.bivariantProperPushforwardExistsOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardUnconditional.lean, line 232. The attribute's comment: “the bundled existence statement at the Gysin system of the first Chern class rule, with NOTHING ASSUMED: Stacks 02RG on Chow groups and Stacks 02TA for this Gysin system are both theorems of this repository”.

The bundled existence statement Stacks.Chow.BivariantProperPushforwardExists of Stacks 0EPK holds at the Gysin system of the first Chern class rule.

theorem bivariantProperPushforwardExistsOfInvertible (C : ChowSituation.{u}) :
    BivariantProperPushforwardExists C (gysinSystemOfInvertible C)

Stacks.Chow.eq_of_isBivariantProperPushforward_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ProperPushforwardUnconditional.lean, line 243. The attribute's comment: “uniqueness of the pushed-forward class, with NOTHING ASSUMED: the descent of Stacks 02S2 is the theorem Stacks.Chow.properPushforwardDescends”.

Two bivariant classes that both push c forward along f, with proper pushforward on Chow groups taken along the descent Stacks.Chow.properPushforwardDescends, are equal.

theorem eq_of_isBivariantProperPushforward_unconditional {C : ChowSituation.{u}}
    {G : GysinSystem C} {X Y Z : Scheme.{u}} {sX : X ⟶ C.S} [LocallyOfFiniteType sX]
    {sY : Y ⟶ C.S} [LocallyOfFiniteType sY] {sZ : Z ⟶ C.S} [LocallyOfFiniteType sZ] {f : X ⟶ Y}
    [IsProper f] {g : Y ⟶ Z} [LocallyOfFiniteType g] {hf : f ≫ sY = sX} {hg : g ≫ sZ = sY}
    {p : ℤ} {c : BivariantClass C G sX sZ (f ≫ g) (comp_comp_structureMorphism_eq hf hg) p}
    {d d' : BivariantClass C G sY sZ g hg p}
    (h : IsBivariantProperPushforward C G sX sY sZ f g hf hg (properPushforwardDescends C) p c d)
    (h' : IsBivariantProperPushforward C G sX sY sZ f g hf hg (properPushforwardDescends C) p c
      d') : d = d'

Tag 0F9Z, a remark

Tag 0F9Z in the Stacks Project.

Stacks.Chow.chowCohomologyRestriction_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyFunctoriality.lean, line 44. The attribute's comment: “compatibility with compositions, for the restriction map on Chow cohomology of Tag 0B7F”.

The restriction map of Stacks 0B7F is compatible with composition: restricting a class on X along f : Y ⟶ X and then along a : W ⟶ Y gives the restriction along a ≫ f,

a^*(f^*(c)) = (a ≫ f)^*(c).

theorem chowCohomologyRestriction_comp (c : chowCohomologyComponent C G sX p) :
    chowCohomologyRestriction C G (f ≫ sX) a p hgys
        (chowCohomologyRestriction C G sX f p hgys c) =
      chowCohomologyRestriction C G sX (a ≫ f) p hgys c

Stacks.Chow.BivariantChowClass.restrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowRestriction.lean, line 165. The attribute's comment: “the restriction map A^p(X → Y) → A^p(X' → Y'), c ↦ res(c)”.

The restriction res(c) ∈ A^p(X' ⟶ Y'), X' = Y' ×_Y X, of a bivariant class c ∈ A^p(X ⟶ Y) along h : Y' ⟶ Y: a scheme Y'' locally of finite type over Y' is one over Y, and res(c) ∩ α'' = c ∩ α'' for α'' ∈ CH_k(Y'') (Stacks.Chow.BivariantChowClass.restrict_cap).

def restrict (c : BivariantChowClass C sX sY f hf p) :
    haveI := locallyOfFiniteType_of_structure sY h hh
    BivariantChowClass C (pullback.fst f h ≫ sX) sY' (pullback.snd f h)
      (restrict_structure_eq hf h hh) p

Stacks.Chow.BivariantChowClass.restrict_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowRestriction.lean, line 179. The attribute's comment: “res(c) ∩ α'' = c ∩ α''”.

res(c) ∩ α'' = c ∩ α'': for g : Y'' ⟶ Y' and α'' ∈ CH_k(Y''), the cap of the restriction is the cap of c at g ≫ h, read on (Y' ×_Y X) ×_{Y'} Y'' through the canonical isomorphism with Y'' ×_Y X.

theorem restrict_cap (c : BivariantChowClass C sX sY f hf p) {T : Scheme.{u}} (g : T ⟶ Y')
    [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ sY') k) :
    haveI := locallyOfFiniteType_of_structure sY h hh
    (c.restrict h hh).cap g k α =
      chowPushforwardOfIso C (pullback.fst f (g ≫ h) ≫ sX)
        (pullback.fst (pullback.snd f h) g ≫ (pullback.fst f h ≫ sX))
        (pullbackLeftPullbackSndIso f h g).inv (by simp) (k - p)
        (c.cap (g ≫ h) k (chowGroupCongr C (by rw [Category.assoc, hh]) k α))

Stacks.Chow.BivariantChowClass.restrict_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowRestriction.lean, line 217. The attribute's comment: “compatibility with compositions: res along Y'' → Y' after res along Y' → Y is res along Y'' → Y”.

Restriction is compatible with compositions of base changes: restricting c along h : Y' ⟶ Y and then along h' : Y'' ⟶ Y' is restricting c along h' ≫ h, the two classes agreeing after the canonical identification (X ×_Y Y') ×_{Y'} Y'' ≅ X ×_Y Y'' of their sources.

theorem restrict_restrict {Y'' : Scheme.{u}} {sY'' : Y'' ⟶ C.S} [LocallyOfFiniteType sY'']
    (h' : Y'' ⟶ Y') (hh' : h' ≫ sY' = sY'') (c : BivariantChowClass C sX sY f hf p) :
    haveI := locallyOfFiniteType_of_structure sY h hh
    haveI := locallyOfFiniteType_of_structure sY' h' hh'
    ((c.restrict h hh).restrict h' hh').transport
        (restrict_structure_eq hf (h' ≫ h) (by rw [Category.assoc, hh, hh']))
        (pullbackLeftPullbackSndIso f h h') (pullbackLeftPullbackSndIso_hom_snd f h h') =
      c.restrict (h' ≫ h) (by rw [Category.assoc, hh, hh'])

Stacks.Chow.BivariantChowClass.restrict_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowRestriction.lean, line 283. The attribute's comment: “compatibility with compositions: res(a ∘ b) = res(a) ∘ res(b)”.

Restriction is compatible with the composition of bivariant classes. For a ∈ A^p(X ⟶ Y), b ∈ A^q(Y ⟶ Z) and h : Z' ⟶ Z, write Y' = Y ×_Z Z' and X' = X ×_Y Y' = X ×_Z Z'; then res(a ∘ b) = res(a) ∘ res(b) in A^{p+q}(X' ⟶ Z'), where res(a) ∈ A^p(X ×_Y Y' ⟶ Y') is the restriction along Y' ⟶ Y and res(b) ∈ A^q(Y' ⟶ Z') the restriction along h. The two sources are identified by the canonical isomorphism X ×_Y (Y ×_Z Z') ≅ X ×_Z Z'.

theorem restrict_comp {Z' : Scheme.{u}} {sZ' : Z' ⟶ C.S} [LocallyOfFiniteType sZ'] (h : Z' ⟶ Z)
    (hh : h ≫ sZ = sZ') (a : BivariantChowClass C sX sY f hf p)
    (b : BivariantChowClass C sY sZ g hg q) :
    haveI := locallyOfFiniteType_of_structure sZ h hh
    ((a.restrict (pullback.fst g h) rfl).comp (b.restrict h hh)).transport
        (restrict_structure_eq (comp_comp_structureMorphism_eq hf hg) h hh)
        (pullbackRightPullbackFstIso g h f) (pullbackRightPullbackFstIso_hom_snd g h f) =
      (a.comp b).restrict h hh

Stacks.Chow.bivariantRestrictionCap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Restriction.lean, line 676. The attribute's comment: “the cap operation of the restriction”.

Stacks 0F9Z. The cap operation res(c) ∩ - of the restriction of a bivariant class c of degree p for f : X ⟶ Y along h : Y' ⟶ Y: on a test scheme g : T ⟶ Y' it is the cap operation of c at g ≫ h, pushed forward along the canonical isomorphism T ×_Y X ≅ (Y' ×_Y X) ×_{Y'} T.

def bivariantRestrictionCap (c : BivariantClass C G sX sY f hf p) {T : Scheme.{u}} (g : T ⟶ Y')
    [LocallyOfFiniteType g] (k : ℤ) :
    chowGroup C (g ≫ (h ≫ sY)) k →+
      chowGroup C (pullback.fst (pullback.snd f h) g ≫ (pullback.fst f h ≫ sX)) (k - p)

Stacks.Chow.bivariantRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Restriction.lean, line 1116.

Stacks 0F9Z. The restriction res(c) of a bivariant class c of degree p for f : X ⟶ Y along h : Y' ⟶ Y: the bivariant class of degree p for the base change X ×_Y Y' ⟶ Y' with res(c) ∩ α = c ∩ α. Together with Stacks.Chow.bivariantRestriction_add, _neg and _zero this is the restriction map A^p(X ⟶ Y) ⟶ A^p(X' ⟶ Y') of the tag.

The Gysin axiom of a restricted class is not a consequence of the axioms of c, so the construction carries the isomorphism case of Stacks 02TA for the Gysin system; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.Bivariant.Restriction.

def bivariantRestriction (hgys : G.IsNaturalUnderBaseChangeIso)
    (c : BivariantClass C G sX sY f hf p) :
    BivariantClass C G (pullback.fst f h ≫ sX) (h ≫ sY) (pullback.snd f h)
      (pullbackSnd_comp_structureMorphism_eq C sX sY f hf h) p

Stacks.Chow.bivariantRestrictionAddHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Restriction.lean, line 1243.

Stacks 0F9Z. The restriction map A^p(X ⟶ Y) ⟶ A^p(X' ⟶ Y') along h : Y' ⟶ Y, as a homomorphism of groups.

def bivariantRestrictionAddHom (hgys : G.IsNaturalUnderBaseChangeIso) :
    BivariantClass C G sX sY f hf p →+
      BivariantClass C G (pullback.fst f h ≫ sX) (h ≫ sY) (pullback.snd f h)
        (pullbackSnd_comp_structureMorphism_eq C sX sY f hf h) p

Stacks.Chow.bivariantRestrictionCap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Restriction.lean, line 1343. The attribute's comment: “compatibility with compositions, on cap operations”.

Stacks 0F9Z. Restriction of a bivariant class is compatible with composition of base changes: if c' is the restriction of c along h, then the restriction of c' along h' caps exactly as the restriction of c along h' ≫ h, after the canonical identification of the two iterated fibre products.

theorem bivariantRestrictionCap_comp (c : BivariantClass C G sX sY f hf p)
    (c' : BivariantClass C G (pullback.fst f h ≫ sX) (h ≫ sY) (pullback.snd f h)
      (pullbackSnd_comp_structureMorphism_eq C sX sY f hf h) p)
    (hc' : IsBivariantRestriction C G sX sY f hf h p c c') {T : Scheme.{u}} (g : T ⟶ Y'')
    [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ (h' ≫ (h ≫ sY))) k) :
    chowPushforwardOfIso C
        (pullback.fst (pullback.snd (pullback.snd f h) h') g ≫
          (pullback.fst (pullback.snd f h) h' ≫ (pullback.fst f h ≫ sX)))
        (pullback.fst (pullback.snd f (h' ≫ h)) g ≫ (pullback.fst f (h' ≫ h) ≫ sX))
        (iteratedRestrictionIso f h h' g).hom
        (iteratedRestrictionIso_hom_comp C sX f h h' g) (k - p)
        (bivariantRestrictionCap C G (pullback.fst f h ≫ sX) (h ≫ sY) (pullback.snd f h)
          (pullbackSnd_comp_structureMorphism_eq C sX sY f hf h) h' p c' g k α) =
      bivariantRestrictionCap C G sX sY f hf (h' ≫ h) p c g k
        (chowGroupCongr C (congrArg (g ≫ ·) (Category.assoc h' h sY).symm) k α)

Stacks.Chow.bivariantRestriction_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Restriction.lean, line 1380.

Stacks 0F9Z. Restriction is compatible with composition of base changes: restricting along h and then along h' agrees with restricting along h' ≫ h, after the canonical identification of the two iterated fibre products.

theorem bivariantRestriction_comp (hgys : G.IsNaturalUnderBaseChangeIso)
    (c : BivariantClass C G sX sY f hf p) {T : Scheme.{u}} (g : T ⟶ Y'')
    [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ (h' ≫ (h ≫ sY))) k) :
    chowPushforwardOfIso C
        (pullback.fst (pullback.snd (pullback.snd f h) h') g ≫
          (pullback.fst (pullback.snd f h) h' ≫ (pullback.fst f h ≫ sX)))
        (pullback.fst (pullback.snd f (h' ≫ h)) g ≫ (pullback.fst f (h' ≫ h) ≫ sX))
        (iteratedRestrictionIso f h h' g).hom
        (iteratedRestrictionIso_hom_comp C sX f h h' g) (k - p)
        ((bivariantRestriction C G (pullback.fst f h ≫ sX) (h ≫ sY) (pullback.snd f h)
          (pullbackSnd_comp_structureMorphism_eq C sX sY f hf h) h' p hgys
          (bivariantRestriction C G sX sY f hf h p hgys c)).cap g k α) =
      (bivariantRestriction C G sX sY f hf (h' ≫ h) p hgys c).cap g k
        (chowGroupCongr C (congrArg (g ≫ ·) (Category.assoc h' h sY).symm) k α)

Stacks.Chow.isBivariantTransport_bivariantComposite_bivariantRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/RestrictionOfComposite.lean, line 73. The attribute's comment: “the clause res(a ∘ b) = res(a) ∘ res(b): restriction commutes with the composition of bivariant classes of Tag 0B75, on cap operations, read through the comparison isomorphism of the two readings of the source fibre product. The compatibility with the composition of BASE CHANGES is the separate Stacks.Chow.bivariantRestrictionCap_comp”.

Stacks 0F9Z, compatibility with the composition of bivariant classes. The restriction of the composite a ∘ b of Stacks 0B75 along h : W ⟶ Z caps exactly as the composite of the restriction of a along pullback.fst g h with the restriction of b along h, read through the comparison isomorphism X ×_Y (Y ×_Z W) ≅ X ×_Z W of the two sources.

theorem isBivariantTransport_bivariantComposite_bivariantRestriction
    (hgys : G.IsNaturalUnderBaseChangeIso)
    (hgysc : G.IsNaturalUnderPullbackCompPushforward) :
    IsBivariantTransport C G (pullback.fst f (pullback.fst g h) ≫ sX)
      (pullback.fst (f ≫ g) h ≫ sX) (h ≫ sZ)
      (pullback.snd f (pullback.fst g h) ≫ pullback.snd g h)
      (comp_comp_structureMorphism_eq
        (pullbackSnd_comp_structureMorphism_eq C sX sY f hf (pullback.fst g h))
        (pullbackSnd_comp_structureMorphism_eq C sY sZ g hg h))
      (pullback.snd (f ≫ g) h)
      (pullbackSnd_comp_structureMorphism_eq C sX sZ (f ≫ g)
        (comp_comp_structureMorphism_eq hf hg) h)
      (pullbackRightPullbackFstIso g h f)
      (pullbackRightPullbackFstIso_hom_comp_snd f g h) (p + q)
      (bivariantComposite C G (pullback.fst f (pullback.fst g h) ≫ sX)
        (pullback.fst g h ≫ sY) (h ≫ sZ) (pullback.snd f (pullback.fst g h))
        (pullback.snd g h)
        (pullbackSnd_comp_structureMorphism_eq C sX sY f hf (pullback.fst g h))
        (pullbackSnd_comp_structureMorphism_eq C sY sZ g hg h) p q
        (bivariantRestriction C G sX sY f hf (pullback.fst g h) p hgys a)
        (bivariantRestriction C G sY sZ g hg h q hgys b) hgys hgysc)
      (bivariantRestriction C G sX sZ (f ≫ g) (comp_comp_structureMorphism_eq hf hg) h (p + q)
        hgys
        (bivariantComposite C G sX sY sZ f g hf hg p q a b hgys hgysc))

Stacks.Chow.bivariantTransport_bivariantComposite_bivariantRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/RestrictionOfComposite.lean, line 123. The attribute's comment: “the clause res(a ∘ b) = res(a) ∘ res(b) as an equality of bivariant classes, the composition being that of Tag 0B75 and the transport the comparison isomorphism of the two readings of the source fibre product”.

Stacks 0F9Z, compatibility with the composition of bivariant classes, as an identity of bivariant classes: the transport along X ×_Y (Y ×_Z W) ≅ X ×_Z W of the composite of the restrictions is the restriction of the composite.

theorem bivariantTransport_bivariantComposite_bivariantRestriction
    (hgys : G.IsNaturalUnderBaseChangeIso)
    (hgysc : G.IsNaturalUnderPullbackCompPushforward) :
    bivariantTransport C G (pullback.fst f (pullback.fst g h) ≫ sX)
        (pullback.fst (f ≫ g) h ≫ sX) (h ≫ sZ)
        (pullback.snd f (pullback.fst g h) ≫ pullback.snd g h)
        (comp_comp_structureMorphism_eq
          (pullbackSnd_comp_structureMorphism_eq C sX sY f hf (pullback.fst g h))
          (pullbackSnd_comp_structureMorphism_eq C sY sZ g hg h))
        (pullback.snd (f ≫ g) h)
        (pullbackSnd_comp_structureMorphism_eq C sX sZ (f ≫ g)
          (comp_comp_structureMorphism_eq hf hg) h)
        (pullbackRightPullbackFstIso g h f)
        (pullbackRightPullbackFstIso_hom_comp_snd f g h) (p + q) hgys
        (bivariantComposite C G (pullback.fst f (pullback.fst g h) ≫ sX)
          (pullback.fst g h ≫ sY) (h ≫ sZ) (pullback.snd f (pullback.fst g h))
          (pullback.snd g h)
          (pullbackSnd_comp_structureMorphism_eq C sX sY f hf (pullback.fst g h))
          (pullbackSnd_comp_structureMorphism_eq C sY sZ g hg h) p q
          (bivariantRestriction C G sX sY f hf (pullback.fst g h) p hgys a)
          (bivariantRestriction C G sY sZ g hg h q hgys b) hgys hgysc) =
      bivariantRestriction C G sX sZ (f ≫ g) (comp_comp_structureMorphism_eq hf hg) h (p + q)
        hgys (bivariantComposite C G sX sY sZ f g hf hg p q a b hgys hgysc)

Stacks.Chow.completedBivariantRestrictionViaSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedRestrictionFlatCommute.lean, line 579. The attribute's comment: “the restriction on the completed bivariant groups A^(X → Y)^∧ → A^(X' → Y')^∧”.

Stacks 0F9Z on completions. The restriction res : A^*(X ⟶ Y)^∧ ⟶ A^*(X ×_Y Y' ⟶ Y')^∧ of completed bivariant classes (Stacks 0FE0) along h : Y' ⟶ Y, at the Gysin system of the first Chern class rule: reading an element of the completed group as the tuple (c_p)_p of Stacks 0FE0, it is the tuple (res(c_p))_p of the restrictions of Stacks 0F9Z, which again vanishes in almost all degrees on each connected component.

def completedBivariantRestrictionViaSequence :
    completedBivariantGroup C (gysinSystemOfInvertible C) sX sY f hf →+
      completedBivariantGroup C (gysinSystemOfInvertible C) (pullback.fst f h ≫ sX) (h ≫ sY)
        (pullback.snd f h) (pullbackSnd_comp_structureMorphism_eq C sX sY f hf h)

Stacks.Chow.bivariantRestrictionOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/BaseChangeIsoGysinSystem.lean, line 236.

The restriction res(c) of a bivariant class c ∈ A^p(X ⟶ Y) along a morphism b : Y' ⟶ Y, for the Gysin system of the first Chern class rule of an invertible module: the bivariant class of degree p for the base change X ×_Y Y' ⟶ Y' with res(c) ∩ α = c ∩ α.

def bivariantRestrictionOfInvertible
    (c : BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p) :
    BivariantClass C (gysinSystemOfInvertible C) (pullback.fst f b ≫ sX) (b ≫ sY)
      (pullback.snd f b) (pullbackSnd_comp_structureMorphism_eq C sX sY f hf b) p

Stacks.Chow.bivariantRestrictionOfInvertible_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/BaseChangeIsoGysinSystem.lean, line 246.

The restriction caps by the cap operation of c: res(c) ∩ α = c ∩ α, after the canonical identification of the two fibre products.

theorem bivariantRestrictionOfInvertible_cap
    (c : BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p) {T : Scheme.{u}}
    (g : T ⟶ Y') [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ (b ≫ sY)) k) :
    (bivariantRestrictionOfInvertible C sX sY f hf b p c).cap g k α =
      bivariantRestrictionCap C (gysinSystemOfInvertible C) sX sY f hf b p c g k α

Stacks.Chow.bivariantRestrictionAddHomOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/BaseChangeIsoGysinSystem.lean, line 256.

The restriction map A^p(X ⟶ Y) ⟶ A^p(X' ⟶ Y') along b : Y' ⟶ Y, as a homomorphism of groups, for the Gysin system of the first Chern class rule of an invertible module.

def bivariantRestrictionAddHomOfInvertible :
    BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p →+
      BivariantClass C (gysinSystemOfInvertible C) (pullback.fst f b ≫ sX) (b ≫ sY)
        (pullback.snd f b) (pullbackSnd_comp_structureMorphism_eq C sX sY f hf b) p

Stacks.Chow.bivariantRestrictionOfInvertible_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Gysin42/BaseChangeIsoGysinSystem.lean, line 269.

Restriction is compatible with composition of base changes: restricting along b and then along b' agrees with restricting along b' ≫ b, after the canonical identification of the two iterated fibre products.

theorem bivariantRestrictionOfInvertible_comp
    (c : BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p) {T : Scheme.{u}}
    (g : T ⟶ Y'') [LocallyOfFiniteType g] (k : ℤ) (α : chowGroup C (g ≫ (b' ≫ (b ≫ sY))) k) :
    chowPushforwardOfIso C
        (pullback.fst (pullback.snd (pullback.snd f b) b') g ≫
          (pullback.fst (pullback.snd f b) b' ≫ (pullback.fst f b ≫ sX)))
        (pullback.fst (pullback.snd f (b' ≫ b)) g ≫ (pullback.fst f (b' ≫ b) ≫ sX))
        (iteratedRestrictionIso f b b' g).hom
        (iteratedRestrictionIso_hom_comp C sX f b b' g) (k - p)
        ((bivariantRestrictionOfInvertible C (pullback.fst f b ≫ sX) (b ≫ sY)
          (pullback.snd f b) (pullbackSnd_comp_structureMorphism_eq C sX sY f hf b) b' p
          (bivariantRestrictionOfInvertible C sX sY f hf b p c)).cap g k α) =
      (bivariantRestrictionOfInvertible C sX sY f hf (b' ≫ b) p c).cap g k
        (chowGroupCongr C (congrArg (g ≫ ·) (Category.assoc b' b sY).symm) k α)

Tag 0FA2, a remark

Tag 0FA2 in the Stacks Project.

Stacks.Chow.BivariantCommute, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Commuting.lean, line 282. The attribute's comment: “the definition of commuting bivariant classes”.

Two bivariant classes c₁ ∈ A^{p₁}(Z₁ ⟶ X) and c₂ ∈ A^{p₂}(Z₂ ⟶ X) commute when

c₁ ∩ c₂ ∩ α = c₂ ∩ c₁ ∩ α

for every morphism t : T ⟶ X locally of finite type and every α ∈ CH_k(T); this is the identity for every α ∈ CH_k(X) and after every base change X' ⟶ X locally of finite type.

The two sides live on the two iterated fibre products Z₁ ×_X (Z₂ ×_X T) and Z₂ ×_X (Z₁ ×_X T) and in the two degrees (k - p₂) - p₁ and (k - p₁) - p₂; they are compared by pushing the first forward along Stacks.Chow.commuteComparisonHom and transporting the second along the equality of degrees.

def BivariantCommute : Prop

Stacks.Chow.bivariantCommute_iff_commuteCompositeCap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Commuting.lean, line 416. The attribute's comment: “commuting is the equality of the two composites”.

Two bivariant classes commute if and only if the cap operations of the two composites res(c₁) ∘ c₂ and res(c₂) ∘ c₁ agree, under the canonical identification Z₁ ×_X Z₂ ≅ Z₂ ×_X Z₁ of their sources and the equality p₁ + p₂ = p₂ + p₁ of their degrees.

theorem bivariantCommute_iff_commuteCompositeCap_eq :
    BivariantCommute C G sX f₁ f₂ p₁ p₂ c₁ c₂ ↔
      ∀ {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
        (α : chowGroup C (t ≫ sX) k),
        chowPushforwardOfIso C
            (pullback.fst (pullback.snd f₁ f₂ ≫ f₂) t ≫ (pullback.fst f₁ f₂ ≫ (f₁ ≫ sX)))
            (pullback.fst (pullback.snd f₂ f₁ ≫ f₁) t ≫ (pullback.fst f₂ f₁ ≫ (f₂ ≫ sX)))
            (compositeComparisonHom f₁ f₂ t)
            (compositeComparisonHom_comp_structureMorphism C sX f₁ f₂ t) ((k - p₂) - p₁)
            (commuteCompositeCap C G sX f₁ f₂ p₁ p₂ c₁ c₂ hgys hpp t k α) =
          chowGroupDegreeEquiv C
            (pullback.fst (pullback.snd f₂ f₁ ≫ f₁) t ≫ (pullback.fst f₂ f₁ ≫ (f₂ ≫ sX)))
            (by ring : (k - p₁) - p₂ = (k - p₂) - p₁)
            (commuteCompositeCap C G sX f₂ f₁ p₂ p₁ c₂ c₁ hgys hpp t k α)

Stacks.Chow.bivariantCommute_iff_cap_eq_of_isBivariantClassComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Commuting.lean, line 439. The attribute's comment: “commuting is the equality of the two composite classes”.

If d₁ is the composite res(c₁) ∘ c₂ and d₂ is the composite res(c₂) ∘ c₁ in the sense of Stacks 0FE0, then c₁ and c₂ commute exactly when d₁ and d₂ agree under the canonical identification Z₁ ×_X Z₂ ≅ Z₂ ×_X Z₁.

theorem bivariantCommute_iff_cap_eq_of_isBivariantClassComposition
    (d₁ : BivariantClass C G (pullback.fst f₁ f₂ ≫ (f₁ ≫ sX)) sX (pullback.snd f₁ f₂ ≫ f₂)
      (comp_comp_structureMorphism_eq
        (pullbackSnd_comp_structureMorphism_eq C (f₁ ≫ sX) sX f₁ rfl f₂) rfl) (p₁ + p₂))
    (d₂ : BivariantClass C G (pullback.fst f₂ f₁ ≫ (f₂ ≫ sX)) sX (pullback.snd f₂ f₁ ≫ f₁)
      (comp_comp_structureMorphism_eq
        (pullbackSnd_comp_structureMorphism_eq C (f₂ ≫ sX) sX f₂ rfl f₁) rfl) (p₂ + p₁))
    (h₁ : IsBivariantClassComposition C G (pullback.fst f₁ f₂ ≫ (f₁ ≫ sX)) (f₂ ≫ sX) sX
      (pullback.snd f₁ f₂) f₂
      (pullbackSnd_comp_structureMorphism_eq C (f₁ ≫ sX) sX f₁ rfl f₂) rfl hpp p₁ p₂
      (bivariantRestriction C G (f₁ ≫ sX) sX f₁ rfl f₂ p₁ hgys c₁) c₂ d₁)
    (h₂ : IsBivariantClassComposition C G (pullback.fst f₂ f₁ ≫ (f₂ ≫ sX)) (f₁ ≫ sX) sX
      (pullback.snd f₂ f₁) f₁
      (pullbackSnd_comp_structureMorphism_eq C (f₂ ≫ sX) sX f₂ rfl f₁) rfl hpp p₂ p₁
      (bivariantRestriction C G (f₂ ≫ sX) sX f₂ rfl f₁ p₂ hgys c₂) c₁ d₂) :
    BivariantCommute C G sX f₁ f₂ p₁ p₂ c₁ c₂ ↔
      ∀ {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
        (α : chowGroup C (t ≫ sX) k),
        chowPushforwardOfIso C
            (pullback.fst (pullback.snd f₁ f₂ ≫ f₂) t ≫ (pullback.fst f₁ f₂ ≫ (f₁ ≫ sX)))
            (pullback.fst (pullback.snd f₂ f₁ ≫ f₁) t ≫ (pullback.fst f₂ f₁ ≫ (f₂ ≫ sX)))
            (compositeComparisonHom f₁ f₂ t)
            (compositeComparisonHom_comp_structureMorphism C sX f₁ f₂ t) ((k - p₂) - p₁)
            (chowGroupDegreeEquiv C
              (pullback.fst (pullback.snd f₁ f₂ ≫ f₂) t ≫ (pullback.fst f₁ f₂ ≫ (f₁ ≫ sX)))
              (by ring : k - (p₁ + p₂) = (k - p₂) - p₁) (d₁.cap t k α)) =
          chowGroupDegreeEquiv C
            (pullback.fst (pullback.snd f₂ f₁ ≫ f₁) t ≫ (pullback.fst f₂ f₁ ≫ (f₂ ≫ sX)))
            (by ring : k - (p₂ + p₁) = (k - p₂) - p₁) (d₂.cap t k α)

Stacks.Chow.bivariantCommute_iff_commuteCompositeOfInvertible_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/CommutingOfInvertible.lean, line 135. The attribute's comment: “commuting is the equality res(c₁) ∘ c₂ = res(c₂) ∘ c₁ of bivariant classes, at the canonical Gysin system, with nothing assumed”.

Stacks 0FA2. Two bivariant classes c₁ ∈ A^{p₁}(Z₁ ⟶ X) and c₂ ∈ A^{p₂}(Z₂ ⟶ X) at the Gysin system of the first Chern class rule commute if and only if

res(c₁) ∘ c₂ = res(c₂) ∘ c₁ in A^{p₁ + p₂}(Z₁ ×_X Z₂ ⟶ X),

where res(cᵢ) is the restriction of Stacks 0F9Z and ∘ the composition of Stacks 0B75. The right-hand side, a class in A^{p₂ + p₁}(Z₂ ×_X Z₁ ⟶ X), is read in A^{p₁ + p₂}(Z₁ ×_X Z₂ ⟶ X) through the symmetry of the fibre product and the equality of degrees.

theorem bivariantCommute_iff_commuteCompositeOfInvertible_eq
    (c₁ : BivariantClass C (gysinSystemOfInvertible C) (f₁ ≫ sX) sX f₁ rfl p₁)
    (c₂ : BivariantClass C (gysinSystemOfInvertible C) (f₂ ≫ sX) sX f₂ rfl p₂) :
    BivariantCommute C (gysinSystemOfInvertible C) sX f₁ f₂ p₁ p₂ c₁ c₂ ↔
      commuteCompositeOfInvertible C sX f₁ f₂ p₁ p₂ c₁ c₂ =
        bivariantClassDegreeCongr C (gysinSystemOfInvertible C)
          (pullback.fst f₁ f₂ ≫ (f₁ ≫ sX)) sX (pullback.snd f₁ f₂ ≫ f₂)
          (comp_comp_structureMorphism_eq
            (pullbackSnd_comp_structureMorphism_eq C (f₁ ≫ sX) sX f₁ rfl f₂) rfl)
          (add_comm p₂ p₁)
          (bivariantTransport C (gysinSystemOfInvertible C) (pullback.fst f₂ f₁ ≫ (f₂ ≫ sX))
            (pullback.fst f₁ f₂ ≫ (f₁ ≫ sX)) sX (pullback.snd f₂ f₁ ≫ f₁)
            (comp_comp_structureMorphism_eq
              (pullbackSnd_comp_structureMorphism_eq C (f₂ ≫ sX) sX f₂ rfl f₁) rfl)
            (pullback.snd f₁ f₂ ≫ f₂)
            (comp_comp_structureMorphism_eq
              (pullbackSnd_comp_structureMorphism_eq C (f₁ ≫ sX) sX f₁ rfl f₂) rfl)
            (pullbackSymmetry f₂ f₁)
            (by rw [pullbackSymmetry_hom_comp_snd_assoc, pullback.condition]) (p₂ + p₁)
            (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C)
            (commuteCompositeOfInvertible C sX f₂ f₁ p₂ p₁ c₂ c₁))

Tag 0FA3, an example

Tag 0FA3 in the Stacks Project.

Stacks.Chow.gysinBivariantClass_bivariantCommute, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/GysinClassCommuting.lean, line 70. The attribute's comment: “the Gysin class i^* of Stacks 0B79 commutes with every c ∈ A^p(Z → X), in the sense of Remark 0FA2”.

Stacks 0FA3. Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S, let (𝓛, s, i : D ⟶ X) be a triple as in Definition 02T8, let f : Z ⟶ X be locally of finite type and let c ∈ A^p(Z ⟶ X) be a bivariant class of Definition 0B76. Then the bivariant Gysin class i^* ∈ A^1(D ⟶ X) of Stacks 0B79 commutes with c in the sense of Remark 0FA2: i^* ∩ (c ∩ α) = c ∩ (i^* ∩ α) for every α ∈ CH_k(T) and every T ⟶ X locally of finite type, the two sides compared by the canonical isomorphism D ×_X (Z ×_X T) ≅ Z ×_X (D ×_X T).

This is a restatement of condition (3) of Definition 0B76 for c.

theorem gysinBivariantClass_bivariantCommute
    (c : BivariantChowClass C (f ≫ sX) sX f rfl p) :
    BivariantCommute C (gysinSystemOfInvertible C) sX (gysinTripleInclusion L s) f 1 p
      (gysinBivariantClass C sX L s).1 (BivariantChowClass.equivBivariantClass c)

Stacks.Chow.gysinBivariantClass_comp_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/GysinClassCommuting.lean, line 91. The attribute's comment: “res(i^) ∘ c = res(c) ∘ i^ in A^{1+p}(D ×_X Z → X), the form of Remark 0FA2 on composites”.

Stacks 0FA3, on composites. In the situation of Stacks.Chow.gysinBivariantClass_bivariantCommute, with i^* ∈ A^1(D ⟶ X) the bivariant Gysin class of Stacks 0B79 and c ∈ A^p(Z ⟶ X),

res(i^*) ∘ c = res(c) ∘ i^* in A^{1+p}(D ×_X Z ⟶ X),

which Remark 0FA2 identifies with the commutation of i^* and c. Here res(i^*) ∈ A^1(D ×_X Z ⟶ Z) and res(c) ∈ A^p(Z ×_X D ⟶ D) are the restrictions of Remark 0F9Z; the second composite lives on Z ×_X D and in degree p + 1, and is read on D ×_X Z through the canonical isomorphism and in degree 1 + p.

theorem gysinBivariantClass_comp_comm {sZ : Z ⟶ C.S} [LocallyOfFiniteType sZ]
    (hZ : f ≫ sX = sZ) (c : BivariantChowClass C sZ sX f hZ p) :
    ((BivariantChowClass.equivBivariantClass.symm (gysinBivariantClass C sX L s).1).restrict f
        hZ).comp c =
      (((c.restrict (gysinTripleInclusion L s) rfl).comp
          (BivariantChowClass.equivBivariantClass.symm
            (gysinBivariantClass C sX L s).1)).degreeCongr (add_comm p 1)).transport
        (comp_comp_structureMorphism_eq (BivariantChowClass.restrict_structure_eq rfl f hZ) hZ)
        (pullbackSymmetry f (gysinTripleInclusion L s))
        (pullbackSymmetry_hom_comp_snd_comp (gysinTripleInclusion L s) f)

Stacks.Chow.gysinBivariantCommute, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/GysinCommuting.lean, line 599.

Stacks 0FA3. Let (𝓛, s, i : D ⟶ X) be a triple as in Definition 02T8, let f : Z ⟶ X be locally of finite type and let c ∈ A^p(Z ⟶ X) be a bivariant class. Then the bivariant Gysin class c' ∈ A^1(D ⟶ X) of Stacks 0B79 commutes with c in the sense of Stacks 0FA2.

This is a restatement of condition (3) of Definition 0B76: the two iterated cap operations are the two sides of Stacks.Chow.BivariantClass.gysin_naturality for c at the divisor pulled back to the test scheme.

theorem gysinBivariantCommute (hG : G.IsNaturalUnderPullbackCompPushforward)
    (c : BivariantClass C G (f ≫ sX) sX f rfl p)
    (c' : BivariantClass C G (gysinTripleInclusion L s ≫ sX) sX (gysinTripleInclusion L s) rfl 1)
    (hc' : IsGysinBivariantClass C G sX L s c') :
    BivariantCommute C G sX (gysinTripleInclusion L s) f 1 p c' c

Tag 0FDU, a remark

Tag 0FDU in the Stacks Project.

Stacks.Chow.GeneralizedBivariantClass, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/Generalized.lean, line 155.

A generalized bivariant class of degree p for a diagram X --x--> Z <--y-- Y of schemes locally of finite type over the base: a rule assigning to every morphism z' : Z' ⟶ Z locally of finite type and every k an additive map A_k(Z' ×_Z Y) ⟶ A_{k-p}(X ×_Z Z'), natural for proper pushforward, for flat pullback of fixed relative dimension, and for the Gysin map of the zero scheme of a section of an invertible module on the test scheme, the Gysin maps being those of the Stacks.Chow.GysinSystem G. The group of all of them is denoted A^p(X ⟶ Z ⟵ Y).

structure GeneralizedBivariantClass (C : ChowSituation.{u}) (G : GysinSystem C)
    {X Y Z : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
    [LocallyOfFiniteType sY] (sZ : Z ⟶ C.S) [LocallyOfFiniteType sZ] (x : X ⟶ Z)
    [LocallyOfFiniteType x] (y : Y ⟶ Z) [LocallyOfFiniteType y] (hx : x ≫ sZ = sX)
    (hy : y ≫ sZ = sY) (p : ℤ)

Stacks.Chow.properPushforwardGeneralizedBivariantClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/GeneralizedProperPushforward.lean, line 496. The attribute's comment: “the example of the remark: for a proper f : X₂ ⟶ X₁, f_* ∈ A^0(X₁ ⟶ X₁ ⟵ X₂), at the canonical Gysin system gysinSystemOfInvertible, with NOTHING ASSUMED”.

For a proper morphism f : X₂ ⟶ X₁ of schemes locally of finite type over the base, proper pushforward is a generalized bivariant class of degree 0 for the diagram X₁ --id--> X₁ <--f-- X₂:

f_* ∈ A^0(X₁ ⟶ X₁ ⟵ X₂).

On a test scheme z' : Z' ⟶ X₁ its cap operation is proper pushforward A_k(Z' ×_{X₁} X₂) ⟶ A_k(X₁ ×_{X₁} Z') along the base change of f (Stacks.Chow.properPushforwardGeneralizedBivariantClass_cap). It is formed at the Gysin system of the first Chern class rule, Stacks.Chow.gysinSystemOfInvertible.

def properPushforwardGeneralizedBivariantClass :
    GeneralizedBivariantClass C (gysinSystemOfInvertible C) s₁ s₂ s₁ (𝟙 X₁) f
      (Category.id_comp s₁) hf 0

Stacks.Chow.properPushforwardGeneralizedBivariantClass_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/GeneralizedProperPushforward.lean, line 513. The attribute's comment: “the class f_* ∈ A^0(X₁ ⟶ X₁ ⟵ X₂) caps by proper pushforward along the base change of f”.

The cap operation of f_* ∈ A^0(X₁ ⟶ X₁ ⟵ X₂) on a test scheme z' : Z' ⟶ X₁ is proper pushforward along the base change Z' ×_{X₁} X₂ ⟶ X₁ ×_{X₁} Z' of f, read in degree k - 0.

theorem properPushforwardGeneralizedBivariantClass_cap {Z' : Scheme.{u}} (z' : Z' ⟶ X₁)
    [LocallyOfFiniteType z'] (k : ℤ) (α : chowGroup C (pullback.snd z' f ≫ s₂) k) :
    (properPushforwardGeneralizedBivariantClass C s₁ s₂ f hf).cap z' k α =
      chowGroupDegreeEquiv C (pullback.fst (𝟙 X₁) z' ≫ s₁) (sub_zero k).symm
        (properChowPushforward C (pullback.snd z' f ≫ s₂) (pullback.fst (𝟙 X₁) z' ≫ s₁)
          (generalizedProperPushforwardMap f z')
          (generalizedProperPushforwardMap_comp_structure C s₁ s₂ f hf z') k
          (properPushforwardDescends C _ _ _ _ _) α)

Sources

LeanStacks.Chow.bivariantComposite_assoc · Stacks.Chow.bivariantCompositeBilinear_assoc · Stacks.Chow.bivariantComposite_add_left' · Stacks.Chow.bivariantComposite_add_right' · Stacks.Chow.bivariantComposite_neg_left · Stacks.Chow.bivariantComposite_neg_right · Stacks.Chow.bivariantComposite_zero_left · Stacks.Chow.bivariantComposite_zero_right

Section42.34 Chow cohomology and the first Chern class #

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

Tag 0B7E, a definition

Tag 0B7E in the Stacks Project.

Stacks.Chow.chowCohomologyGRingOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyCompositionRing.lean, line 761. The attribute's comment: “the graded Z-algebra structure on A^*(X): composition of bivariant classes as the multiplication, with associativity, the unit 1 in A^0(X) and the two distributive laws, for the Gysin system of the genuine first Chern class rule and with no hypothesis on that system”.

The Chow cohomology of X as a graded ring, for the Gysin system Stacks.Chow.gysinSystemOfInvertible: the degree p component is A^p(X ⟶ X), the multiplication is Stacks.Chow.chowCohomologyGradedMul (composition of bivariant classes), the unit is Stacks.Chow.chowCohomologyGradedOne (the identity class 1 ∈ A^0(X)), and ℤ maps to the multiples of 1.

def chowCohomologyGRingOfInvertible :
    DirectSum.GRing fun p : ℤ ↦ chowCohomologyComponent C (gysinSystemOfInvertible C) sX p

Stacks.Chow.chowCohomologyRingOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyCompositionRing.lean, line 788. The attribute's comment: “the ring structure on the graded group A^*(X), with no hypothesis on the Gysin system”.

The Chow cohomology A^*(X) as a ring, for the Gysin system Stacks.Chow.gysinSystemOfInvertible.

def chowCohomologyRingOfInvertible :
    Ring (chowCohomology C (gysinSystemOfInvertible C) sX)

Stacks.Chow.chowCohomologyAlgebraOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyCompositionRing.lean, line 798. The attribute's comment: “the graded Z-algebra A^*(X), the Chow cohomology of X, with no hypothesis on the Gysin system”.

The Chow cohomology of X: the graded ℤ-algebra A^*(X) whose degree p component is A^p(X ⟶ X), for the Gysin system Stacks.Chow.gysinSystemOfInvertible.

def chowCohomologyAlgebraOfInvertible :
    @Algebra ℤ (chowCohomology C (gysinSystemOfInvertible C) sX) _
      (chowCohomologyRingOfInvertible C sX).toSemiring

Stacks.Chow.ChowCohomologyGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyRing.lean, line 72. The attribute's comment: “the degree p component A^p(X) = A^p(X → X) of the Chow cohomology: the bivariant classes of degree p of Stacks 0B76 for id_X”.

The group A^p(X) = A^p(X ⟶ X) of bivariant classes of degree p (Stacks 0B76) for the identity morphism of X.

abbrev ChowCohomologyGroup (p : ℤ) : Type (u + 1)

Stacks.Chow.ChowCohomologyGroup.instGRing, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyRing.lean, line 225. The attribute's comment: “the graded Z-algebra structure on A^*(X): the product of the degree p and q components is the composition A^p(X → X) × A^q(X → X) → A^{p+q}(X → X) of Stacks 0B75, associative and bilinear, with unit 1 ∈ A^0(X)”.

The family p ↦ A^p(X) is a graded ring: the product A^p(X) × A^q(X) ⟶ A^{p+q}(X) is the composition of bivariant classes of Stacks 0B75, which is associative and bilinear, with unit the class 1 ∈ A^0(X).

instance instGRing : DirectSum.GRing (ChowCohomologyGroup C sX)

Stacks.Chow.ChowCohomology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyRing.lean, line 279. The attribute's comment: “the Chow cohomology A^*(X): the graded Z-algebra ⊕_p A^p(X → X), with multiplication the composition of bivariant classes”.

The Chow cohomology A^*(X) of X: the graded ℤ-algebra ⊕_{p ∈ ℤ} A^p(X) whose degree p component is A^p(X ⟶ X), with the multiplication of Stacks.Chow.ChowCohomologyGroup.instGRing, composition of bivariant classes.

abbrev ChowCohomology : Type (u + 1)

Stacks.Chow.chowCohomologyComponent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/ChowCohomology.lean, line 73. The attribute's comment: “the degree p part”.

Stacks 0B7E. The degree p part A^p(X) of the Chow cohomology of a scheme X locally of finite type over the base: the group A^p(X ⟶ X) of bivariant classes of degree p for the identity morphism of X.

abbrev chowCohomologyComponent (C : ChowSituation.{u}) (G : GysinSystem C) {X : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (p : ℤ) : Type (u + 1)

Stacks.Chow.chowCohomology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/ChowCohomology.lean, line 81. The attribute's comment: “the graded group”.

Stacks 0B7E. The Chow cohomology A^*(X) of a scheme X locally of finite type over the base: the graded group whose degree p part is the group A^p(X ⟶ X) of bivariant classes of degree p for the identity morphism of X.

abbrev chowCohomology (C : ChowSituation.{u}) (G : GysinSystem C) {X : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] : Type (u + 1)

Tag 0B7F, a remark

Tag 0B7F in the Stacks Project.

Stacks.Chow.chowCohomologyRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomology.lean, line 484. The attribute's comment: “the canonical map”.

Stacks 0B7F. The restriction map res : A^p(Y) ⟶ A^p(Y') along a morphism f : Y' ⟶ Y of schemes locally of finite type over the base, a homomorphism of groups: the special case X = Y, f = 𝟙 Y of the restriction map of Stacks 0F9Z, followed by the transport of a bivariant class along the canonical isomorphism Y ×_Y Y' ≅ Y'. It is often written f^*.

The tag asserts more, namely that the induced map A^*(Y) ⟶ A^*(Y') of the graded groups is a map of ℤ-algebras. The multiplication is composition of bivariant classes, and the graded ring it makes of A^*(Y) is Stacks.Chow.chowCohomologyGRing of StacksFrontier.AlgebraicGeometry.Chow.Bivariant.ChowCohomologyCompositionRing, hypothesis-free for the Gysin system this repository constructs as Stacks.Chow.chowCohomologyGRingOfInvertible. Only the additive map is given here; that it respects that multiplication is Stacks.Chow.chowCohomologyRestriction_chowCohomologyRingMul of StacksFrontier.AlgebraicGeometry.Chow.Bivariant.ChowCohomologyMultiplicative, which assembles the ℤ-algebra map of the tag as Stacks.Chow.chowCohomologyTotalRestrictionAlgHomOfInvertible.

def chowCohomologyRestriction (hgys : G.IsNaturalUnderBaseChangeIso) :
    chowCohomologyComponent C G sY p →+ chowCohomologyComponent C G (f ≫ sY) p

Stacks.Chow.chowCohomologyRestriction_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomology.lean, line 497. The attribute's comment: “the cap formula for the canonical map”.

Stacks 0B7F. The restriction map on Chow cohomology satisfies the cap formula of Stacks 0F9Z: res(c) ∩ α = c ∩ α for every α ∈ CH_k(T) and every test scheme g : T ⟶ Y', both sides read in CH_{k-p}(T) through the canonical identifications Y' ×_{Y'} T ≅ T and Y ×_Y T ≅ T.

theorem chowCohomologyRestriction_cap (hgys : G.IsNaturalUnderBaseChangeIso)
    (c : chowCohomologyComponent C G sY p) {T : Scheme.{u}} (g : T ⟶ Y') [LocallyOfFiniteType g]
    (k : ℤ)
    (α : chowGroup C (g ≫ (f ≫ sY)) k) :
    chowPushforwardOfIso C (pullback.fst (𝟙 Y') g ≫ (f ≫ sY)) (g ≫ (f ≫ sY))
        (identityBaseChangeIso g).hom (identityBaseChangeIso_hom_comp_base C (f ≫ sY) g) (k - p)
        ((chowCohomologyRestriction C G sY f p hgys c).cap g k α) =
      chowPushforwardOfIso C (pullback.fst (𝟙 Y) (g ≫ f) ≫ sY) (g ≫ (f ≫ sY))
        (identityBaseChangeIso (g ≫ f)).hom
        (by rw [← Category.assoc]; exact identityBaseChangeIso_hom_comp_base C sY (g ≫ f))
        (k - p) (c.cap (g ≫ f) k (chowGroupCongr C (Category.assoc g f sY).symm k α))

Stacks.Chow.chowCohomologyTotalRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomology.lean, line 539. The attribute's comment: “the canonical map of graded groups”.

Stacks 0B7F. The restriction map res : A^*(Y) ⟶ A^*(Y') of the graded Chow cohomology groups along f : Y' ⟶ Y, a homomorphism of graded groups: the degreewise restriction map.

The tag asserts that this is a map of ℤ-algebras. The multiplication on A^* is composition of bivariant classes and the graded ring it produces is Stacks.Chow.chowCohomologyGRing of StacksFrontier.AlgebraicGeometry.Chow.Bivariant.ChowCohomologyCompositionRing. Only additivity is proved here; that this map respects that multiplication is Stacks.Chow.chowCohomologyTotalRestriction_mul of StacksFrontier.AlgebraicGeometry.Chow.Bivariant.ChowCohomologyMultiplicative, and the ℤ-algebra map of the tag is Stacks.Chow.chowCohomologyTotalRestrictionAlgHomOfInvertible there.

def chowCohomologyTotalRestriction (hgys : G.IsNaturalUnderBaseChangeIso) :
    chowCohomology C G sY →+ chowCohomology C G (f ≫ sY)

Stacks.Chow.chowCohomologyRestrictionOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/ChowCohomologyRestriction.lean, line 493. The attribute's comment: “the canonical map, at the Gysin system of the first Chern class rule, with nothing assumed beyond the tag's own hypotheses”.

Stacks 0B7F. The restriction map res : A^p(Y) ⟶ A^p(Y') along a morphism f : Y' ⟶ Y of schemes locally of finite type over the base, a homomorphism of groups, at the Gysin system of the first Chern class rule of an invertible module. It is often written f^*.

This is Stacks.Chow.chowCohomologyRestriction with its case of Stacks 02TA discharged, by Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderBaseChangeIso. Nothing is assumed: the Gysin system itself carries no hypothesis either, so the only hypotheses are those of the tag.

def chowCohomologyRestrictionOfInvertible :
    chowCohomologyComponent C (gysinSystemOfInvertible C) sY p →+
      chowCohomologyComponent C (gysinSystemOfInvertible C) (f ≫ sY) p

Stacks.Chow.chowCohomologyRestrictionOfInvertible_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/ChowCohomologyRestriction.lean, line 505. The attribute's comment: “the cap formula for the canonical map, at the Gysin system of the first Chern class rule, with nothing assumed beyond the tag's own hypotheses”.

Stacks 0B7F. The restriction map on Chow cohomology satisfies the cap formula of Stacks 0F9Z: res(c) ∩ α = c ∩ α for every α ∈ CH_k(T) and every test scheme g : T ⟶ Y', both sides read in CH_{k-p}(T) through the canonical identifications Y' ×_{Y'} T ≅ T and Y ×_Y T ≅ T. Nothing is assumed.

theorem chowCohomologyRestrictionOfInvertible_cap
    (c : chowCohomologyComponent C (gysinSystemOfInvertible C) sY p) {T : Scheme.{u}}
    (g : T ⟶ Y') [LocallyOfFiniteType g] (k : ℤ)
    (α : chowGroup C (g ≫ (f ≫ sY)) k) :
    chowPushforwardOfIso C (pullback.fst (𝟙 Y') g ≫ (f ≫ sY)) (g ≫ (f ≫ sY))
        (identityBaseChangeIso g).hom (identityBaseChangeIso_hom_comp_base C (f ≫ sY) g) (k - p)
        ((chowCohomologyRestrictionOfInvertible C sY f p c).cap g k α) =
      chowPushforwardOfIso C (pullback.fst (𝟙 Y) (g ≫ f) ≫ sY) (g ≫ (f ≫ sY))
        (identityBaseChangeIso (g ≫ f)).hom
        (by rw [← Category.assoc]; exact identityBaseChangeIso_hom_comp_base C sY (g ≫ f))
        (k - p) (c.cap (g ≫ f) k (chowGroupCongr C (Category.assoc g f sY).symm k α))

Stacks.Chow.chowCohomologyTotalRestrictionOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/ChowCohomologyRestriction.lean, line 528. The attribute's comment: “the canonical map of graded groups, at the Gysin system of the first Chern class rule, with nothing assumed beyond the tag's own hypotheses”.

Stacks 0B7F. The restriction map res : A^*(Y) ⟶ A^*(Y') of the graded Chow cohomology groups along f : Y' ⟶ Y, a homomorphism of graded groups, at the Gysin system of the first Chern class rule: the degreewise restriction map. Nothing is assumed.

That this graded map is a map of ℤ-algebras is the AddMonoidHom structure here and in each degree, together with Stacks.Chow.chowCohomologyRestrictionOfInvertible_mul and Stacks.Chow.chowCohomologyRestrictionOfInvertible_bivariantIdentityClass.

def chowCohomologyTotalRestrictionOfInvertible :
    chowCohomology C (gysinSystemOfInvertible C) sY →+
      chowCohomology C (gysinSystemOfInvertible C) (f ≫ sY)

Stacks.Chow.chowCohomologyRestrictionOfInvertible_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/ChowCohomologyRestriction.lean, line 558. The attribute's comment: “the canonical map is multiplicative: res(a ⬝ b) = res(a) ⬝ res(b), the multiplication on Chow cohomology being composition of bivariant classes -- at the Gysin system of the first Chern class rule, with nothing assumed beyond the tag's own hypotheses”.

Stacks 0B7F. The restriction map res : A^*(Y) ⟶ A^*(Y') along f : Y' ⟶ Y is multiplicative: res(a ⬝ b) = res(a) ⬝ res(b) for a ∈ A^p(Y) and b ∈ A^q(Y), the multiplication being composition of bivariant classes, Stacks 0B75. Nothing is assumed.

This is Stacks.Chow.chowCohomologyRestriction_mul with both of its cases of Stacks 02TA discharged, by Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderBaseChangeIso and Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderPullbackCompPushforward.

theorem chowCohomologyRestrictionOfInvertible_mul
    (a : chowCohomologyComponent C (gysinSystemOfInvertible C) sY p)
    (b : chowCohomologyComponent C (gysinSystemOfInvertible C) sY q) :
    chowCohomologyRestrictionOfInvertible C sY f (p + q)
        (chowCohomologyMulOfInvertible C sY p q a b) =
      chowCohomologyMulOfInvertible C (f ≫ sY) p q
        (chowCohomologyRestrictionOfInvertible C sY f p a)
        (chowCohomologyRestrictionOfInvertible C sY f q b)

Stacks.Chow.chowCohomologyRestrictionOfInvertible_bivariantIdentityClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/ChowCohomologyRestriction.lean, line 583. The attribute's comment: “the canonical map is unital: it carries the identity class 1 of A^0(Y) to the identity class of A^0(Y') -- at the Gysin system of the first Chern class rule, with nothing assumed beyond the tag's own hypotheses”.

Stacks 0B7F. The restriction map res : A^*(Y) ⟶ A^*(Y') along f : Y' ⟶ Y is unital: it carries the identity class 1 ∈ A^0(Y) of Stacks 0FBS to the identity class 1 ∈ A^0(Y'). Nothing is assumed.

This is Stacks.Chow.chowCohomologyRestriction_bivariantIdentityClass with its case of Stacks 02TA discharged by Stacks.Chow.gysinSystemOfInvertible_isNaturalUnderBaseChangeIso and its two Gysin axioms for the transported identity cap rule discharged by Stacks.Chow.IdentityCapRule.transportGysinNaturality — exactly the proofs Stacks.Chow.bivariantIdentityClassOfInvertible is built from, so the two identity classes in the statement are the unconditional ones.

theorem chowCohomologyRestrictionOfInvertible_bivariantIdentityClass :
    chowCohomologyRestrictionOfInvertible C sY f 0 (bivariantIdentityClassOfInvertible C sY) =
      bivariantIdentityClassOfInvertible C (f ≫ sY)

Stacks.Chow.chowCohomologyTotalRestrictionRingOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/ChowCohomologyRestriction.lean, line 686. The attribute's comment: “the canonical map res : A^(Y) → A^(Y') on the graded groups is a homomorphism for addition and for the multiplication of Stacks 0B75 -- at the Gysin system of the first Chern class rule, with nothing assumed beyond the tag's own hypotheses”.

Stacks 0B7F. The restriction map res : A^*(Y) ⟶ A^*(Y') along f : Y' ⟶ Y as a map of the ring structures of the graded Chow cohomology: a homomorphism for addition and for the multiplication of Stacks 0B75, at the Gysin system of the first Chern class rule. It is often written f^*.

Its underlying additive map is Stacks.Chow.chowCohomologyTotalRestrictionOfInvertible, and that it also carries 1 to 1 is Stacks.Chow.chowCohomologyTotalRestrictionRingOfInvertible_map_one just below; since an additive map between abelian groups is ℤ-linear, the two together are the whole of the tag's "map of ℤ-algebras". Nothing is assumed.

The proof reduces to the degreewise statement Stacks.Chow.chowCohomologyRestrictionOfInvertible_mul: multiplication on a DirectSum is bilinear, so both sides of res(x ⬝ y) = res(x) ⬝ res(y) are additive in x and in y and it is enough to check them on the summands.

def chowCohomologyTotalRestrictionRingOfInvertible :
    chowCohomology C (gysinSystemOfInvertible C) sY →ₙ+*
      chowCohomology C (gysinSystemOfInvertible C) (f ≫ sY)

Stacks.Chow.chowCohomologyTotalRestrictionRingOfInvertible_map_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantComposition/ChowCohomologyRestriction.lean, line 717. The attribute's comment: “the canonical map res : A^(Y) → A^(Y') on the graded groups carries the unit 1 of A^(Y) to the unit of A^(Y') -- at the Gysin system of the first Chern class rule, with nothing assumed beyond the tag's own hypotheses”.

Stacks 0B7F. The restriction map res : A^*(Y) ⟶ A^*(Y') carries the unit 1 of A^*(Y) to the unit of A^*(Y'): the unit of the graded ring is the identity class of Stacks 0FBS sitting in degree 0, and res carries it to the identity class of A^0(Y') by Stacks.Chow.chowCohomologyRestrictionOfInvertible_bivariantIdentityClass. Nothing is assumed.

theorem chowCohomologyTotalRestrictionRingOfInvertible_map_one :
    chowCohomologyTotalRestrictionRingOfInvertible C sY f 1 = 1

Stacks.Chow.chowCohomologyRestriction_chowCohomologyComposite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingProjectionFormula/RestrictionMultiplicative.lean, line 475. The attribute's comment: “the multiplicativity of the canonical map: res(c ∘ c') = res(c) ∘ res(c') for the multiplication of A^* that is composition of bivariant classes, which is the clause that the map of graded groups is a map of algebras”.

The restriction map of Stacks 0B7F is multiplicative: res(c ∘ c') = res(c) ∘ res(c') for the multiplication Stacks.Chow.chowCohomologyComposite of A^*, and so for the restriction Aⁱ(X) ⟶ Aⁱ(Z) of Stacks 0F9Z that the second pairing of Stacks 0FA0 is built from.

This is the clause of Stacks 0B7F asserting that res : A^*(Y) ⟶ A^*(Y') is a map of ℤ-algebras, for the multiplication of A^* that this repository has. It is also the first of the two inputs an associativity proof for the multiplication of Stacks 0FA0 needs: the degree n terms res(res(c) ∘ c') ∘ c'' and res(c) ∘ (res(c') ∘ c'') of the two groupings cannot be compared without it, however associative the composition of Stacks 0B75 is.

Both sides cap, on a test scheme g : T ⟶ Y', by capping with c' and then with c, both at test morphisms over Y obtained from g ≫ f; the two differ by an isomorphism of test schemes, which the proper-pushforward axiom of Stacks 0B76 for c absorbs.

theorem chowCohomologyRestriction_chowCohomologyComposite (i j : ℤ)
    (c : chowCohomologyComponent C G sY i) (c' : chowCohomologyComponent C G sY j) :
    chowCohomologyRestriction C G sY f (i + j) hgys
        (chowCohomologyComposite C G sY hgys hgysc i j c c') =
      chowCohomologyComposite C G (f ≫ sY) hgys hgysc i j
        (chowCohomologyRestriction C G sY f i hgys c)
        (chowCohomologyRestriction C G sY f j hgys c')

Tag 0B77, a lemma

Tag 0B77 in the Stacks Project.

Stacks.Chow.isFirstChernClassBivariant_firstChernClassBivariantCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FirstChernClassCanonical.lean, line 399.

The bivariant class Stacks.Chow.firstChernClassBivariantCanonical caps by c₁(g^*ℒ) ∩ - on every test scheme.

theorem isFirstChernClassBivariant_firstChernClassBivariantCanonical :
    IsFirstChernClassBivariant C sX (canonicalFirstChernCapRule C) L (canonicalGysinSystem C)
      (firstChernClassBivariantCanonical C sX L)

Stacks.Chow.GenuineChern.firstChernClassBivariantClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/FirstChernClassBivariant.lean, line 69.

For an invertible module ℒ on X, the rule assigning to f : X' ⟶ X the operation c₁(f^*ℒ) ∩ - : A_k(X') ⟶ A_{k-1}(X') is a bivariant class of degree 1: the class c₁(ℒ) ∈ A^1(X) together with the statement that it caps by c₁(f^*ℒ) ∩ - on every test scheme.

def firstChernClassBivariantClass :
    {c : BivariantClass C (gysinSystemOfInvertible C) sX sX (𝟙 X) (Category.id_comp sX) 1 //
      ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (g ≫ sX) k),
        c.idRule C sX (gysinSystemOfInvertible C) g k α =
          (invCap C (g ≫ sX) ((Scheme.Modules.pullback g).obj L)).capOnChow C (g ≫ sX) (k - 1)
            (chowGroupCast C (g ≫ sX) (by omega) α)}

Tag 0FDW, a definition

Tag 0FDW in the Stacks Project.

Stacks.Chow.firstChernClassBivariantCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FirstChernClassCanonical.lean, line 388.

The first Chern class c₁(ℒ) ∈ A^1(X) of an invertible module ℒ on a scheme X locally of finite type over the base, as a bivariant class of degree 1 for 𝟙 X at the canonical Gysin system.

def firstChernClassBivariantCanonical :
    BivariantClass C (canonicalGysinSystem C) sX sX (𝟙 X) (Category.id_comp sX) 1

Tag 0B7B, a lemma

Tag 0B7B in the Stacks Project.

Stacks.Chow.GenuineChern.comp_firstChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/BivariantFirstChernCentral.lean, line 75. The attribute's comment: “(2): c ∘ c_1(L) = c_1(f^*L) ∘ c in A^{p+1}(X' → X) for every f : X' → X locally of finite type and every bivariant class c in A^p(X' → X) of Stacks 0B76”.

Stacks 0B7B (2). Let ℒ be an invertible 𝒪_X-module, let f : X' ⟶ X be locally of finite type and let c ∈ A^p(X' ⟶ X) be a bivariant class. Then

c ∘ c₁(ℒ) = c₁(f^*ℒ) ∘ c in A^{p+1}(X' ⟶ X),

with c₁(ℒ) ∈ A^1(X) and c₁(f^*ℒ) ∈ A^1(X') the bivariant first Chern classes of Stacks 0B77. The left side is a class for f ≫ 𝟙 X of degree p + 1; the right side, a class for 𝟙 X' ≫ f of degree 1 + p, is read as one for f ≫ 𝟙 X of degree p + 1 along the identity of X'.

theorem comp_firstChernClass {X' : Scheme.{u}} {sX' : X' ⟶ C.S} [LocallyOfFiniteType sX']
    (L : X.Modules) [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (f : X' ⟶ X) (hf : f ≫ sX = sX') {p : ℤ} (c : BivariantChowClass C sX' sX f hf p) :
    haveI := isInvertible_pullback f L
    c.comp (BivariantChowClass.equivBivariantClass.symm (firstChernClass C sX L)) =
      (((BivariantChowClass.equivBivariantClass.symm
          (firstChernClass C sX' ((Scheme.Modules.pullback f).obj L))).comp c).degreeCongr
        (add_comm 1 p)).transport (comp_comp_structureMorphism_eq hf (Category.id_comp sX))
        (Iso.refl X') (by simp)

Stacks.Chow.GenuineChern.firstChernClass_mem_center, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/BivariantFirstChernCentral.lean, line 92. The attribute's comment: “(1): c_1(L) in A^1(X) is in the center of the Chow cohomology ring A^*(X) of Stacks 0B7E, for the bivariant first Chern class of Stacks 0B77”.

Stacks 0B7B (1). The first Chern class c₁(ℒ) ∈ A^1(X) of an invertible 𝒪_X-module lies in the center of the Chow cohomology ring A^*(X) of Stacks 0B7E. The ring structure is an @[instance_reducible] def and not an instance, which is why it is supplied by hand.

theorem firstChernClass_mem_center (L : X.Modules)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] :
    letI : Ring (chowCohomology C (gysinSystemOfInvertible C) sX) :=
      chowCohomologyRingOfInvertible C sX
    DirectSum.of (fun q : ℤ ↦ chowCohomologyComponent C (gysinSystemOfInvertible C) sX q) 1
        (firstChernClass C sX L) ∈
      Subring.center (chowCohomology C (gysinSystemOfInvertible C) sX)

Stacks.Chow.BivariantClass.heq_bivariantCompositeOfInvertible_firstChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/FirstChernClassCommute.lean, line 387. The attribute's comment: “(2), for a homogeneous c in A^q(X' -> X) and the composition of Stacks 0B75 at the Gysin system of the first Chern class of an invertible module; the two composites are classes for g ≫ 𝟙 X and 𝟙 X' ≫ g of degrees q + 1 and 1 + q, whence the heterogeneous equality”.

Stacks 0B7B (2). Let g : X' ⟶ X be locally of finite type, let c ∈ A^q(X' ⟶ X) and let ℒ be an invertible 𝒪_X-module. Then

c ∘ c₁(ℒ) = c₁(g^*ℒ) ∘ c in A^{q+1}(X' ⟶ X),

the composites being those of Stacks 0B75, classes for the equal morphisms g ≫ 𝟙 X and 𝟙 X' ≫ g of the equal degrees q + 1 and 1 + q.

theorem BivariantClass.heq_bivariantCompositeOfInvertible_firstChernClass
    (c : BivariantClass C (gysinSystemOfInvertible C) sX' sX g hg q) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] :
    haveI := GenuineChern.isInvertible_pullback g L
    bivariantCompositeOfInvertible C sX' sX sX g (𝟙 X) hg (Category.id_comp sX) q 1 c
        (GenuineChern.firstChernClass C sX L) ≍
      bivariantCompositeOfInvertible C sX' sX' sX (𝟙 X') g (Category.id_comp sX') hg 1 q
        (GenuineChern.firstChernClass C sX' ((Scheme.Modules.pullback g).obj L)) c

Stacks.Chow.BivariantClass.heq_mulId_firstChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GenuineChern/FirstChernClassCommute.lean, line 415. The attribute's comment: “(1), for the product of A^*(X) given by the composition of Stacks 0B75 at the Gysin system of the first Chern class of an invertible module, against every homogeneous c in A^q(X); the two products have degrees q + 1 and 1 + q, whence the heterogeneous equality”.

Stacks 0B7B (1). The first Chern class c₁(ℒ) ∈ A^1(X) of an invertible module is in the center of A^*(X): for every c ∈ A^q(X),

c · c₁(ℒ) = c₁(ℒ) · c,

the two products lying in A^{q+1}(X) and A^{1+q}(X).

theorem BivariantClass.heq_mulId_firstChernClass
    (c : BivariantClass C (gysinSystemOfInvertible C) sX sX (𝟙 X) (Category.id_comp sX) q)
    (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] :
    c.mulId C sX (GenuineChern.firstChernClass C sX L) ≍
      (GenuineChern.firstChernClass C sX L).mulId C sX c

Tag 0FDX, a lemma

Tag 0FDX in the Stacks Project.

Stacks.Chow.iteratedChernCapOnChow_ofFn_eq_zero_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCapDimensionInduction.lean, line 287. The attribute's comment: “the conclusion read on EVERY test scheme locally of finite type, with no bound on its dimension: the cap operation of the product of the d+1 first Chern classes annihilates every Chow class of every such test scheme. This is the clause the source's induction on d proves, and the one the dimension-counting proofs of ChernCapDimensionVanishing do not reach”.

Stacks 0FDX, on every test scheme locally of finite type.

Let X be locally of finite type over the base scheme of chapter 42, Noetherian, and carrying an ample invertible module A, and let dim X ≤ d. For invertible 𝒪_X-modules ℒ_1, …, ℒ_{d+1} and every test scheme u : T ⟶ X locally of finite type,

c₁(u^*ℒ_1) ∩ ⋯ ∩ c₁(u^*ℒ_{d+1}) ∩ α = 0 for every Chow class α of T.

No bound is placed on the dimension of T: this is the cap-level content of the vanishing of c₁(ℒ_1) ∘ ⋯ ∘ c₁(ℒ_{d+1}) in A^{d+1}(X), which by Stacks 02UC is exactly the vanishing of the cap operation on every such T, and it is what the source's induction on d establishes.

The proof is that induction. The base case d = 0 is Stacks.Chow.invCap_capOnChow_pullback_eq_zero_of_topologicalKrullDim_le_zero; the step is Stacks.Chow.iteratedChernCapOnChow_ofFn_succ_eq_zero_of_effectiveCartierDivisors applied to the two effective Cartier divisors Stacks 0AYM produces from ℒ_{d+2} and the ample module, with the inductive hypothesis transported to each of them along the closed immersion.

The ample invertible module is used only through Stacks 0AYM, and Noetherianness only through Stacks 0AYM and the dimension drop; both follow from the source's hypothesis that X be of finite type over the base, the base being locally Noetherian.

theorem iteratedChernCapOnChow_ofFn_eq_zero_of_topologicalKrullDim_le (d : ℕ) {X : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] [IsNoetherian X] (A : X.Modules)
    [Stacks.Ample.IsInvertibleModule X A] (hA : Stacks.Ample.IsAmple X A)
    (hdim : topologicalKrullDim X ≤ (d : WithBot ℕ∞)) (N : Fin (d + 1) → X.Modules)
    [∀ i, AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property (N i)]
    {T : Scheme.{u}} (u : T ⟶ X) [LocallyOfFiniteType u] (q : T ⟶ C.S) [LocallyOfFiniteType q]
    (hq : u ≫ sX = q) (k : ℤ)
    (α : chowGroup C q
      (k + ((List.ofFn fun i => invCap C q ((Scheme.Modules.pullback u).obj (N i))).length : ℤ))) :
    iteratedChernCapOnChow C q
      (List.ofFn fun i => invCap C q ((Scheme.Modules.pullback u).obj (N i))) k α = 0

Stacks.Chow.iteratedChernCapOnChow_eq_zero_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCapDimensionVanishing.lean, line 232. The attribute's comment: “the cap-product form on the test scheme X itself: a product of d+1 or more first Chern class cap operators annihilates every Chow class of X, for X locally of finite type over a Jacobson base whose dimension function vanishes at closed points and of topological dimension at most d. The product of first Chern classes is the iterated cap operation Stacks.Chow.iteratedChernCapOnChow on an arbitrary list of Stacks.Chow.ChernCapOperator, not a composite of bivariant classes: no such composite is constructed in this library, so the equality in A^{d+1}(X) that the source states has no term here. The ample invertible module of the source is not assumed, being used there only to reach Stacks 0AYM. Proved by a delta-dimension count — CH_k(X) is zero outside 0 ≤ k ≤ d — rather than by the induction on d of the source, so the same vanishing holds for every additive map of that bidegree”.

Stacks 0FDX, the cap-product form on X itself. Let X be locally of finite type over a Jacobson base whose dimension function vanishes at closed points, and let the topological dimension of X be at most d. Then any d + 1 (or more) first Chern class cap operators on X annihilate every Chow class of X:

c₁(L_1) ∩ ⋯ ∩ c₁(L_{d+1}) ∩ α = 0 in CH_k(X), for every α ∈ CH_{k + d + 1}(X).

The operation goes CH_{k + r}(X) ⟶ CH_k(X) with r = Os.length ≥ d + 1. For k < 0 the target vanishes, and for k ≥ 0 the source has degree k + r ≥ d + 1 > d and vanishes. So the proof is a delta-dimension count, not the induction on d of the source, and it establishes the same vanishing for every additive map of that bidegree.

theorem iteratedChernCapOnChow_eq_zero_of_topologicalKrullDim_le {X : Scheme.{u}} (p : X ⟶ C.S)
    [LocallyOfFiniteType p] {d : ℕ} (hd : topologicalKrullDim X ≤ (d : WithBot ℕ∞))
    (Os : List (ChernCapOperator C p)) (hlen : d + 1 ≤ Os.length) (k : ℤ)
    (α : chowGroup C p (k + (Os.length : ℤ))) :
    iteratedChernCapOnChow C p Os k α = 0

Stacks.Chow.firstChernCapTower_eq_zero_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCapDimensionVanishing.lean, line 289. The attribute's comment: “the conclusion for the product of the first Chern classes of the GIVEN invertible modules L_1, …, L_{d+1} on X: that product annihilates every Chow class of X, for X locally of finite type over a Jacobson base whose dimension function vanishes at closed points and of topological dimension at most d. The product is read as the composite of the Chow-group cap products Stacks.Chow.firstChernCapStep of the modules themselves — Stacks.Chow.firstChernCapTower — and NOT as an equality in A^{d+1}(X): no composite of bivariant classes is constructed in this library, so the source's conclusion has no term here. Carried: Stacks 02TI for each module, as the hypotheses InvertibleChernCapDescends, which by Stacks.Chow.firstChernClassCapFactorsThroughRationalEquivalence_iff are implied by the mere existence of the descended cap products and so are not a weakening. The ample invertible module of the source is not assumed, being used there only to reach Stacks 0AYM. Proved by a delta-dimension count — CH_k(X) is zero outside 0 ≤ k ≤ d — rather than by the induction on d of the source”.

Stacks 0FDX for the first Chern classes of given invertible modules. Let X be locally of finite type over a Jacobson base whose dimension function vanishes at closed points, and let the topological dimension of X be at most d. Then for every sequence L_1, L_2, … of invertible 𝒪_X-modules on X and every r ≥ d + 1,

c₁(L_1) ∩ ⋯ ∩ c₁(L_r) ∩ α = 0 in A_{n-r}(X), for every α ∈ A_n(X),

the product being the tower Stacks.Chow.firstChernCapTower of the cap products Stacks.Chow.firstChernCapStep of the L_i themselves.

The degree count: if n - r < 0 the target A_{n-r}(X) vanishes, and otherwise n ≥ r ≥ d + 1 > d, so the source A_n(X) vanishes.

theorem firstChernCapTower_eq_zero_of_topologicalKrullDim_le {X : Scheme.{u}} (p : X ⟶ C.S)
    [LocallyOfFiniteType p] {d : ℕ} (hd : topologicalKrullDim X ≤ (d : WithBot ℕ∞)) (n : ℤ)
    (L : ℕ → X.Modules)
    [∀ i, AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property (L i)]
    (hfac : ∀ i, InvertibleChernCapDescends C p (L i)) (r : ℕ) (hr : d + 1 ≤ r)
    (α : chowGroup C p (n - ((0 : ℕ) : ℤ))) :
    firstChernCapTower C p n L hfac r α = 0

Stacks.Chow.BivariantClass.cap_eq_zero_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCapDimensionVanishing.lean, line 316. The attribute's comment: “the conclusion read on the test schemes of dimension at most d: every bivariant class of degree at least d+1 caps every Chow class of such a test scheme to zero, for a Jacobson base whose dimension function vanishes at closed points. This covers the test scheme X itself but not the test schemes of dimension larger than d, so it does not give the equality c = 0 in A^{d+1}(X) that the source states; and the class c is arbitrary of that degree rather than a composite of first Chern classes, no composite of bivariant classes being constructed in this library”.

Stacks 0FDX on the test schemes of dimension at most d. A bivariant class of degree at least d + 1 caps every Chow class of every test scheme of topological dimension at most d to zero. Applied to a product of d + 1 first Chern classes on a scheme X of dimension d, and to the test scheme X itself, this is the conclusion of Stacks 0FDX read on that test scheme.

For a test scheme T of dimension at most d the source group CH_k(T) vanishes unless 0 ≤ k ≤ d, and in that range the target group has degree k - p ≤ d - (d + 1) < 0, so it vanishes by nonnegativity of the delta-dimension.

theorem BivariantClass.cap_eq_zero_of_topologicalKrullDim_le (G : GysinSystem C)
    {X Y : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S)
    [LocallyOfFiniteType sY] (f : X ⟶ Y) [LocallyOfFiniteType f] (hf : f ≫ sY = sX) {p : ℤ}
    (c : BivariantClass C G sX sY f hf p) {d : ℕ} (hp : (d : ℤ) + 1 ≤ p) {T : Scheme.{u}}
    (g : T ⟶ Y) [LocallyOfFiniteType g] (hT : topologicalKrullDim T ≤ (d : WithBot ℕ∞))
    (k : ℤ) (α : chowGroup C (g ≫ sY) k) :
    c.cap g k α = 0

Stacks.Chow.firstChernClassProduct_eq_zero_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/FirstChernClassProductVanishing.lean, line 168.

Stacks 0FDX. Let X be a scheme of finite type over the base scheme S of chapter 42 which has an ample invertible module A, and let dim X ≤ d. Then for invertible 𝒪_X-modules ℒ_1, …, ℒ_{d+1} on X

c₁(ℒ_1) ∘ ⋯ ∘ c₁(ℒ_{d+1}) = 0 in A^{d+1}(X),

the product being the composition of Stacks 0B75 of the bivariant first Chern classes of Stacks 0B77, at the Gysin system of the first Chern class rule.

theorem firstChernClassProduct_eq_zero_of_topologicalKrullDim_le [QuasiCompact sX]
    (A : X.Modules) [Stacks.Ample.IsInvertibleModule X A] (hA : Stacks.Ample.IsAmple X A)
    (d : ℕ) (hdim : topologicalKrullDim X ≤ (d : WithBot ℕ∞)) (L : Fin (d + 1) → X.Modules)
    [∀ i, AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property (L i)] :
    firstChernClassProduct C sX d L = 0

Tag 0FA0, a remark

Tag 0FA0 in the Stacks Project.

Stacks.Chow.localizedBivariantGrading, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGrading.lean, line 53. The attribute's comment: “localized_bivariant_grading”.

Stacks 0FA0. The group A⁽ᵖ⁾(Z ⟶ X) attached to a closed immersion f : Z ⟶ X of schemes locally of finite type over the base: operational Chow classes on X in the degrees below p, and bivariant classes for f in the degrees from p onward.

abbrev localizedBivariantGrading (C : ChowSituation.{u}) (G : GysinSystem C) {Z X : Scheme.{u}}
    (sZ : Z ⟶ C.S) [LocallyOfFiniteType sZ] (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (f : Z ⟶ X) [IsClosedImmersion f] (hf : f ≫ sX = sZ) (p : ℕ) : Type (u + 1)

Stacks.Chow.localizedBivariantGradingMulHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 620. The attribute's comment: “the multiplication of the remark's graded algebra as a biadditive map A^(p)(Z ⟶ X) ⟶ A^(q)(Z ⟶ X) ⟶ A^(r)(Z ⟶ X), which is its distributive law, at every p, q and every target r”.

Stacks 0FA0. The multiplication A⁽ᵖ⁾(Z ⟶ X) × A⁽ᑫ⁾(Z ⟶ X) ⟶ A⁽ʳ⁾(Z ⟶ X) of the remark as a biadditive map, at every p, q and every target r. This is the distributive law of the source's graded algebra, bundled: the underlying function is Stacks.Chow.localizedBivariantGradingMul and the additivity in each argument is Stacks.Chow.localizedBivariantGradingMul_add_left and _add_right.

def localizedBivariantGradingMulHom (p q r : ℕ) :
    localizedBivariantGrading C G (f ≫ sX) sX f rfl p →+
      localizedBivariantGrading C G (f ≫ sX) sX f rfl q →+
        localizedBivariantGrading C G (f ≫ sX) sX f rfl r

Stacks.Chow.localizedBivariantGradingMulMaxHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 635. The attribute's comment: “the multiplication A^(p)(Z ⟶ X) × A^(q)(Z ⟶ X) ⟶ A^(max(p,q))(Z ⟶ X) displayed in the remark as a biadditive map, for every p and q”.

Stacks 0FA0. The multiplication with the target A⁽ᵐᵃˣ⁽ᵖ⁼ᑫ⁾⁾(Z ⟶ X) the source displays, as a biadditive map.

def localizedBivariantGradingMulMaxHom (p q : ℕ) :
    localizedBivariantGrading C G (f ≫ sX) sX f rfl p →+
      localizedBivariantGrading C G (f ≫ sX) sX f rfl q →+
        localizedBivariantGrading C G (f ≫ sX) sX f rfl (max p q)

Stacks.Chow.localizedBivariantGradingInternalMulHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 645. The attribute's comment: “the multiplication internal to A^(p)(Z ⟶ X) of the remark's graded algebra as a biadditive map A^(p) ⟶ A^(p) ⟶ A^(p), which is its distributive law, for every p ≥ 0”.

Stacks 0FA0. The multiplication internal to A⁽ᵖ⁾(Z ⟶ X) — the product of the source's graded algebra — as a biadditive map, for every p ≥ 0.

def localizedBivariantGradingInternalMulHom (p : ℕ) :
    localizedBivariantGrading C G (f ≫ sX) sX f rfl p →+
      localizedBivariantGrading C G (f ≫ sX) sX f rfl p →+
        localizedBivariantGrading C G (f ≫ sX) sX f rfl p

Stacks.Chow.eq_localizedBivariantGradingMulHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 668. The attribute's comment: “uniqueness of the canonical multiplication as a biadditive map: a biadditive map satisfying the two finite-convolution formulas of the remark is the multiplication”.

Stacks 0FA0, uniqueness of the canonical multiplication as a biadditive map. A biadditive map whose components are the two finite convolutions of the source — the property Stacks.Chow.LocalizedGrading.IsMul — is Stacks.Chow.localizedBivariantGradingMulHom. This is Stacks.Chow.LocalizedGrading.IsMul.eq_localizedBivariantGradingMul read through Stacks.Chow.localizedBivariantGradingMulHom_apply; additivity is not used in the uniqueness, the component formulas already prescribing every value.

theorem eq_localizedBivariantGradingMulHom (p q r : ℕ)
    (M : localizedBivariantGrading C G (f ≫ sX) sX f rfl p →+
      localizedBivariantGrading C G (f ≫ sX) sX f rfl q →+
        localizedBivariantGrading C G (f ≫ sX) sX f rfl r)
    (hM : LocalizedGrading.IsMul C G sX f hRG hgysP hgys hgysc p q r fun a b ↦ M a b) :
    M = localizedBivariantGradingMulHom C G sX f hRG hgysP hgys hgysc p q r

Stacks.Chow.localizedBivariantGradingOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 822. The attribute's comment: “the unit of the remark's graded algebra on A^(p)(Z ⟶ X): the class 1 of A^0(X) in the degree 0 slot, which is a slot of A^(p)(Z ⟶ X) exactly for p ≥ 1”.

Stacks 0FA0, the unit of the graded algebra on A⁽ᵖ⁾(Z ⟶ X): the element whose degree 0 component is the class 1 ∈ A⁰(X) of Stacks 0FBS and whose components in the other degrees vanish.

For p ≥ 1 the degree 0 slot of A⁽ᵖ⁾(Z ⟶ X) is A⁰(X) and this is the unit; for p = 0 that slot is A⁰(Z ⟶ X), which holds no canonical class, and this element is zero there. Together with Stacks.Chow.localizedGrading_self_admissible_iff that makes p = 1 the one p at which the source's graded algebra on A⁽ᵖ⁾(Z ⟶ X) is unital.

def localizedBivariantGradingOne (p : ℕ) :
    localizedBivariantGrading C G (f ≫ sX) sX f rfl p

Stacks.Chow.localizedBivariantGradingInternalMul_one_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 1033. The attribute's comment: “the unit law of the remark's graded algebra on A^(p)(Z ⟶ X) for every p ≥ 1: the class 1 of A^0(X) placed in degree 0 is a left unit for the multiplication internal to A^(p)(Z ⟶ X), on all of A^(p)(Z ⟶ X)”.

Stacks 0FA0, the unit law of the graded algebra on A⁽ᵖ⁾(Z ⟶ X), for every p ≥ 1: multiplying by Stacks.Chow.localizedBivariantGradingOne on the left returns the element. The bound 1 ≤ p is what puts the degree 0 slot, where the unit sits, in A⁰(X); for p = 0 that slot is A⁰(Z ⟶ X) and holds no canonical class.

Degree by degree the product has a single surviving term, the one at i = 0: below the cutoff it is 1 · bₙ in A^*(X) (Stacks.Chow.chowCohomologyComposite_identityClass_left), and from the cutoff on it is the source's second pairing at the unit (Stacks.Chow.localizedMulChowBivariant_identityClass_left), which is res(1) ∘ bₙ = bₙ.

No hypothesis is imposed on b: the index range of the sums, Finset.Icc (min 0 n) (max 0 n), contains the one surviving index i = 0 in every degree (Stacks.Chow.zero_mem_Icc_min_max), so the law holds on all of A⁽ᵖ⁾(Z ⟶ X) — which is the group the source asserts the graded algebra on, negative-degree factors included. See the implementation notes of this module.

theorem localizedBivariantGradingInternalMul_one_left (p : ℕ) (hp : 1 ≤ p)
    (b : localizedBivariantGrading C G (f ≫ sX) sX f rfl p) :
    localizedBivariantGradingInternalMul C G sX f hRG hgysP hgys hgysc p
        (localizedBivariantGradingOne C G sX f hgysinX p) b = b

Stacks.Chow.localizedBivariantGradingInternalMul_one_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 1087. The attribute's comment: “the unit law of the remark's graded algebra on A^(p)(Z ⟶ X) on the right for every p ≥ 1: the class 1 of A^0(X) placed in degree 0 is a right unit for the multiplication internal to A^(p)(Z ⟶ X), on all of A^(p)(Z ⟶ X)”.

Stacks 0FA0, the unit law of the graded algebra on A⁽ᵖ⁾(Z ⟶ X) on the right, for every p ≥ 1: multiplying by Stacks.Chow.localizedBivariantGradingOne on the right returns the element. Together with Stacks.Chow.localizedBivariantGradingInternalMul_one_left this makes Stacks.Chow.localizedBivariantGradingOne a two-sided unit, and with the associativity of Stacks.Chow.localizedBivariantGradingInternalMul_assoc it is what Stacks.Chow.localizedBivariantGradingMonoid is assembled from.

Here the surviving term of the degree n component is the one at i = n, and the pairing that applies is the source's first one, Stacks.Chow.localizedMulBivariantChow_identityClass_right: bₙ ∘ 1 = bₙ.

This law is the sharp test of the index range of the sums: the component of b it has to return in degree n is carried by the term at i = n alone. The range Finset.Icc (min 0 n) (max 0 n) contains i = n in every degree (Stacks.Chow.self_mem_Icc_min_max), so the law needs no hypothesis on b and holds on all of A⁽ᵖ⁾(Z ⟶ X); under the narrower range 0 ≤ i ≤ n it would fail in every negative degree in which b has a nonzero component. See the implementation notes of this module.

theorem localizedBivariantGradingInternalMul_one_right (p : ℕ) (hp : 1 ≤ p)
    (b : localizedBivariantGrading C G (f ≫ sX) sX f rfl p) :
    localizedBivariantGradingInternalMul C G sX f hRG hgysP hgys hgysc p b
        (localizedBivariantGradingOne C G sX f hgysinX p) = b

Stacks.Chow.localizedBivariantGradingInternalMulHomOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 1163. The attribute's comment: “the multiplication internal to A^(p)(Z ⟶ X) of the remark's graded algebra as a biadditive map, which is its distributive law, at the Gysin system of the first Chern class rule with nothing assumed”.

Stacks 0FA0. The multiplication internal to A⁽ᵖ⁾(Z ⟶ X) of the remark's graded algebra as a biadditive map, at the Gysin system of the first Chern class rule, where nothing is assumed.

def localizedBivariantGradingInternalMulHomOfInvertible (p : ℕ) :
    localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p →+
      localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p →+
        localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p

Stacks.Chow.localizedBivariantGradingOneOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 1178. The attribute's comment: “the unit of the remark's graded algebra on A^(p)(Z ⟶ X), at the Gysin system of the first Chern class rule with nothing assumed”.

Stacks 0FA0, the unit of the graded algebra at the Gysin system of the first Chern class rule, where nothing is assumed: its degree 0 component is Stacks.Chow.bivariantIdentityClassOfInvertible.

def localizedBivariantGradingOneOfInvertible (p : ℕ) :
    localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p

Stacks.Chow.localizedBivariantGradingInternalMul_one_left_ofInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 1188. The attribute's comment: “the unit law of the remark's graded algebra on A^(p)(Z ⟶ X) for every p ≥ 1, on all of A^(p)(Z ⟶ X), at the Gysin system of the first Chern class rule with NOTHING ASSUMED”.

Stacks 0FA0, the unit law of the graded algebra on A⁽ᵖ⁾(Z ⟶ X) for every p ≥ 1 at the Gysin system of the first Chern class rule, where nothing at all is assumed: the law holds on all of A⁽ᵖ⁾(Z ⟶ X).

theorem localizedBivariantGradingInternalMul_one_left_ofInvertible (p : ℕ) (hp : 1 ≤ p)
    (b : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p) :
    localizedBivariantGradingInternalMulHomOfInvertible C sX f p
        (localizedBivariantGradingOneOfInvertible C sX f p) b = b

Stacks.Chow.localizedBivariantGradingInternalMul_one_right_ofInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingAlgebra.lean, line 1207. The attribute's comment: “the unit law of the remark's graded algebra on A^(p)(Z ⟶ X) on the right for every p ≥ 1: the class 1 of A^0(X) placed in degree 0 is a right unit for the multiplication internal to A^(p)(Z ⟶ X), on all of A^(p)(Z ⟶ X), at the Gysin system of the first Chern class rule with NOTHING ASSUMED”.

Stacks 0FA0, the unit law of the graded algebra on A⁽ᵖ⁾(Z ⟶ X) on the right, for every p ≥ 1 at the Gysin system of the first Chern class rule, where nothing at all is assumed: the law holds on all of A⁽ᵖ⁾(Z ⟶ X).

theorem localizedBivariantGradingInternalMul_one_right_ofInvertible (p : ℕ) (hp : 1 ≤ p)
    (b : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p) :
    localizedBivariantGradingInternalMulHomOfInvertible C sX f p b
        (localizedBivariantGradingOneOfInvertible C sX f p) = b

Stacks.Chow.localizedMulBivariantChow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 246. The attribute's comment: “the pairing A^i(Z ⟶ X) × A^j(X) ⟶ A^{i+j}(Z ⟶ X) of the remark, composition of bivariant classes”.

The first of the three pairings: A^i(Z ⟶ X) × A^j(X) ⟶ A^{i+j}(Z ⟶ X), composition of bivariant classes, read through the equality f ≫ 𝟙 X = f.

def localizedMulBivariantChow (i j : ℤ) (c : BivariantClass C G (f ≫ sX) sX f rfl i)
    (b : chowCohomologyComponent C G sX j) : BivariantClass C G (f ≫ sX) sX f rfl (i + j)

Stacks.Chow.localizedMulChowBivariant, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 322. The attribute's comment: “the pairing A^i(X) × A^j(Z ⟶ X) ⟶ A^{i+j}(Z ⟶ X) of the remark, the restriction A^i(X) ⟶ A^i(Z) of Stacks 0F9Z followed by composition”.

The second of the three pairings: A^i(X) × A^j(Z ⟶ X) ⟶ A^{i+j}(Z ⟶ X), the restriction Stacks.Chow.chowCohomologyRestriction : A^i(X) ⟶ A^i(Z) followed by the composition A^i(Z) × A^j(Z ⟶ X) ⟶ A^{i+j}(Z ⟶ X).

def localizedMulChowBivariant (i j : ℤ) (a : chowCohomologyComponent C G sX i)
    (c : BivariantClass C G (f ≫ sX) sX f rfl j) :
    BivariantClass C G (f ≫ sX) sX f rfl (i + j)

Stacks.Chow.localizedMulBivariant, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 359. The attribute's comment: “the pairing A^i(Z ⟶ X) × A^j(Z ⟶ X) ⟶ A^{i+j}(Z ⟶ X) of the remark, (c, c') ↦ res(c) ∘ c' for the restriction res of Stacks 0F9Z”.

The third of the three pairings: A^i(Z ⟶ X) × A^j(Z ⟶ X) ⟶ A^{i+j}(Z ⟶ X), sending (c, c') to res(c) ∘ c' for the restriction res = Stacks.Chow.closedImmersionChowCohomologyRestriction : A^i(Z ⟶ X) ⟶ A^i(Z).

def localizedMulBivariant (i j : ℤ) (c : BivariantClass C G (f ≫ sX) sX f rfl i)
    (c' : BivariantClass C G (f ≫ sX) sX f rfl j) :
    BivariantClass C G (f ≫ sX) sX f rfl (i + j)

Stacks.Chow.localizedBivariantGradingMul, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 469. The attribute's comment: “the canonical multiplication A^(p)(Z ⟶ X) × A^(q)(Z ⟶ X) ⟶ A^(r)(Z ⟶ X) of the remark at every p, q and every target r, assembled degreewise from the three pairings and the pushforward of Stacks 0EPK; its associativity, which the source omits, is localizedBivariantGradingMul_assoc”.

The multiplication A⁽ᵖ⁾(Z ⟶ X) × A⁽ᑫ⁾(Z ⟶ X) ⟶ A⁽ʳ⁾(Z ⟶ X) attached to a closed immersion f : Z ⟶ X of schemes locally of finite type over the base, at every p, q and every target r. Its degree n component is the sum over i ∈ Finset.Icc (min 0 n) (max 0 n) of the products of the degree i component of the first factor with the degree n - i component of the second: for n < r the localized factors are pushed forward to A^*(X) and the product is taken in A^*(X) (Stacks.Chow.localizedGradingMulAmbientTerm), and for n ≥ r the term is the one of the three pairings Stacks.Chow.localizedMulBivariantChow, Stacks.Chow.localizedMulChowBivariant, Stacks.Chow.localizedMulBivariant that applies, and 0 on the pairs i < p, n - i < q (Stacks.Chow.localizedGradingMulLocalizedTerm).

def localizedBivariantGradingMul (p q r : ℕ)
    (a : localizedBivariantGrading C G (f ≫ sX) sX f rfl p)
    (b : localizedBivariantGrading C G (f ≫ sX) sX f rfl q) :
    localizedBivariantGrading C G (f ≫ sX) sX f rfl r

Stacks.Chow.localizedBivariantGradingMulMax, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 482. The attribute's comment: “the multiplication A^(p)(Z ⟶ X) × A^(q)(Z ⟶ X) ⟶ A^(max(p,q))(Z ⟶ X) displayed in the remark, for every p and q”.

The multiplication A⁽ᵖ⁾(Z ⟶ X) × A⁽ᑫ⁾(Z ⟶ X) ⟶ A⁽ᵐᵃˣ⁽ᵖ⁼ᑫ⁾⁾(Z ⟶ X), for every p and q: Stacks.Chow.localizedBivariantGradingMul at r = max(p, q).

def localizedBivariantGradingMulMax (p q : ℕ)
    (a : localizedBivariantGrading C G (f ≫ sX) sX f rfl p)
    (b : localizedBivariantGrading C G (f ≫ sX) sX f rfl q) :
    localizedBivariantGrading C G (f ≫ sX) sX f rfl (max p q)

Stacks.Chow.localizedBivariantGradingInternalMul, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 493. The attribute's comment: “the multiplication internal to A^(p)(Z ⟶ X) of the remark's graded algebra, for every p ≥ 0; it is graded, and additive in each argument by localizedBivariantGradingMul_add_left and _add_right”.

The multiplication internal to A⁽ᵖ⁾(Z ⟶ X), for every p ≥ 0: Stacks.Chow.localizedBivariantGradingMul at r = p = q.

def localizedBivariantGradingInternalMul (p : ℕ)
    (a b : localizedBivariantGrading C G (f ≫ sX) sX f rfl p) :
    localizedBivariantGrading C G (f ≫ sX) sX f rfl p

Stacks.Chow.localizedBivariantGradingMul_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 507. The attribute's comment: “the finite-convolution formula for the degree n part of a product in a degree n below the cutoff of the target: the sum over i + j = n of the products of the degree i and degree j parts of the factors, pushed into A^*(X) by Stacks 0EPK and multiplied there”.

The component formula below the cutoff of the target. For n < r, the degree n component of a product is the finite convolution ∑ aᵢ · bₙ₋ᵢ over i ∈ Finset.Icc (min 0 n) (max 0 n), taken in A^*(X) (Stacks.Chow.localizedGradingMulAmbientTerm).

theorem localizedBivariantGradingMul_fst (p q r : ℕ)
    (a : localizedBivariantGrading C G (f ≫ sX) sX f rfl p)
    (b : localizedBivariantGrading C G (f ≫ sX) sX f rfl q) (n : {n : ℤ // n < (r : ℤ)}) :
    (localizedBivariantGradingMul C G sX f hRG hgysP hgys hgysc p q r a b).1 n =
      ∑ i ∈ Finset.Icc (min 0 n.1) (max 0 n.1),
        localizedGradingMulAmbientTerm C G sX f hRG hgysP hgys hgysc p q a b n.1 i

Stacks.Chow.localizedBivariantGradingMul_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 522. The attribute's comment: “the finite-convolution formula for the degree n part of a product in a degree n at or above the cutoff of the target: the sum over i + j = n of the products of the degree i and degree j parts of the factors under the three pairings of the remark”.

The component formula from the cutoff of the target on. For n ≥ r, the degree n component of a product is the finite convolution ∑ aᵢ · bₙ₋ᵢ over i ∈ Finset.Icc (min 0 n) (max 0 n), taken in A^*(Z ⟶ X) (Stacks.Chow.localizedGradingMulLocalizedTerm).

theorem localizedBivariantGradingMul_snd (p q r : ℕ)
    (a : localizedBivariantGrading C G (f ≫ sX) sX f rfl p)
    (b : localizedBivariantGrading C G (f ≫ sX) sX f rfl q) (n : {n : ℤ // (r : ℤ) ≤ n}) :
    (localizedBivariantGradingMul C G sX f hRG hgysP hgys hgysc p q r a b).2 n =
      ∑ i ∈ Finset.Icc (min 0 n.1) (max 0 n.1),
        localizedGradingMulLocalizedTerm C G sX f hgys hgysc p q a b n.1 i

Stacks.Chow.LocalizedGrading.IsMul.eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 556. The attribute's comment: “uniqueness of the canonical multiplication: the two finite-convolution formulas determine it degreewise, so any two maps satisfying them are equal”.

Uniqueness of the multiplication. Any two maps satisfying the two component formulas Stacks.Chow.LocalizedGrading.IsMul are equal; nothing else, not even additivity, is assumed of them.

theorem LocalizedGrading.IsMul.eq {p q r : ℕ}
    {M N : localizedBivariantGrading C G (f ≫ sX) sX f rfl p →
      localizedBivariantGrading C G (f ≫ sX) sX f rfl q →
      localizedBivariantGrading C G (f ≫ sX) sX f rfl r}
    (hM : LocalizedGrading.IsMul C G sX f hRG hgysP hgys hgysc p q r M)
    (hN : LocalizedGrading.IsMul C G sX f hRG hgysP hgys hgysc p q r N) : M = N

Stacks.Chow.localizedMulBivariantChowOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 943. The attribute's comment: “the pairing A^i(Z ⟶ X) × A^j(X) ⟶ A^{i+j}(Z ⟶ X) of the remark, at the Gysin system of the first Chern class rule, with nothing assumed”.

The first pairing A^i(Z ⟶ X) × A^j(X) ⟶ A^{i+j}(Z ⟶ X) at the Gysin system Stacks.Chow.gysinSystemOfInvertible, with no hypotheses.

def localizedMulBivariantChowOfInvertible (i j : ℤ)
    (c : BivariantClass C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl i)
    (b : chowCohomologyComponent C (gysinSystemOfInvertible C) sX j) :
    BivariantClass C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl (i + j)

Stacks.Chow.localizedMulChowBivariantOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 955. The attribute's comment: “the pairing A^i(X) × A^j(Z ⟶ X) ⟶ A^{i+j}(Z ⟶ X) of the remark, at the Gysin system of the first Chern class rule, with nothing assumed”.

The second pairing A^i(X) × A^j(Z ⟶ X) ⟶ A^{i+j}(Z ⟶ X) at the Gysin system Stacks.Chow.gysinSystemOfInvertible, with no hypotheses.

def localizedMulChowBivariantOfInvertible (i j : ℤ)
    (a : chowCohomologyComponent C (gysinSystemOfInvertible C) sX i)
    (c : BivariantClass C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl j) :
    BivariantClass C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl (i + j)

Stacks.Chow.localizedMulBivariantOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 967. The attribute's comment: “the pairing A^i(Z ⟶ X) × A^j(Z ⟶ X) ⟶ A^{i+j}(Z ⟶ X) of the remark, at the Gysin system of the first Chern class rule, with nothing assumed”.

The third pairing A^i(Z ⟶ X) × A^j(Z ⟶ X) ⟶ A^{i+j}(Z ⟶ X), (c, c') ↦ res(c) ∘ c', at the Gysin system Stacks.Chow.gysinSystemOfInvertible, with no hypotheses.

def localizedMulBivariantOfInvertible (i j : ℤ)
    (c : BivariantClass C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl i)
    (c' : BivariantClass C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl j) :
    BivariantClass C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl (i + j)

Stacks.Chow.localizedBivariantGradingMulOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 982. The attribute's comment: “the canonical multiplication A^(p)(Z ⟶ X) × A^(q)(Z ⟶ X) ⟶ A^(r)(Z ⟶ X) of the remark at every p, q and every target r, at the Gysin system of the first Chern class rule, with NOTHING ASSUMED: every Gysin compatibility is discharged there and Stacks 02RG on Chow groups, which the pushforward of Stacks 0EPK costs, is a theorem of this repository; its associativity, which the source omits, is localizedBivariantGradingMulOfInvertible_assoc”.

The multiplication A⁽ᵖ⁾(Z ⟶ X) × A⁽ᑫ⁾(Z ⟶ X) ⟶ A⁽ʳ⁾(Z ⟶ X), at every p, q and every target r, at the Gysin system Stacks.Chow.gysinSystemOfInvertible, with no hypotheses.

def localizedBivariantGradingMulOfInvertible (p q r : ℕ)
    (a : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p)
    (b : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl q) :
    localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl r

Stacks.Chow.localizedBivariantGradingMulMaxOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 997. The attribute's comment: “the multiplication A^(p)(Z ⟶ X) × A^(q)(Z ⟶ X) ⟶ A^(max(p,q))(Z ⟶ X) displayed in the remark, for every p and q, at the Gysin system of the first Chern class rule with nothing assumed”.

The multiplication A⁽ᵖ⁾(Z ⟶ X) × A⁽ᑫ⁾(Z ⟶ X) ⟶ A⁽ᵐᵃˣ⁽ᵖ⁼ᑫ⁾⁾(Z ⟶ X), for every p and q, at the Gysin system Stacks.Chow.gysinSystemOfInvertible, with no hypotheses.

def localizedBivariantGradingMulMaxOfInvertible (p q : ℕ)
    (a : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p)
    (b : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl q) :
    localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl (max p q)

Stacks.Chow.localizedBivariantGradingInternalMulOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingMultiplication.lean, line 1007. The attribute's comment: “the multiplication internal to A^(p)(Z ⟶ X) of the remark's graded algebra for every p ≥ 0, at the Gysin system of the first Chern class rule with nothing assumed”.

The multiplication internal to A⁽ᵖ⁾(Z ⟶ X), for every p ≥ 0, at the Gysin system Stacks.Chow.gysinSystemOfInvertible, with no hypotheses.

def localizedBivariantGradingInternalMulOfInvertible (p : ℕ)
    (a b : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p) :
    localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p

Stacks.Chow.localizedBivariantGradingMul_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingProjectionFormula/Associativity.lean, line 479. The attribute's comment: “associativity of the canonical multiplication A^(p)(Z ⟶ X) × A^(q)(Z ⟶ X) ⟶ A^(r)(Z ⟶ X) of the remark -- the verification the source omits -- for every triple of factors and every choice of intermediate targets r₁, r₂ and common target r with p + q + s ≤ r + 2, where every term of a triple product is one of the remark's three pairings; this covers the displayed target max(p,q) and the product internal to A^(p)(Z ⟶ X) of the graded algebra”.

Stacks 0FA0, associativity of the canonical multiplication A⁽ᵖ⁾(Z ⟶ X) × A⁽ᑫ⁾(Z ⟶ X) ⟶ A⁽ʳ⁾(Z ⟶ X): for a ∈ A⁽ᵖ⁾(Z ⟶ X), b ∈ A⁽ᑫ⁾(Z ⟶ X), c ∈ A⁽ˢ⁾(Z ⟶ X) the two groupings (a · b) · c and a · (b · c) of a triple product agree, at every pair of intermediate targets A⁽ʳ¹⁾(Z ⟶ X), A⁽ʳ²⁾(Z ⟶ X) and every common target A⁽ʳ⁾(Z ⟶ X) whose cutoffs satisfy the four inequalities below, which together come to p + q + s ≤ r + 2. This is "the verification that these multiplications are associative in a suitable sense" that the source omits, carried out in the range where every term of every grouping is one of the source's own three pairings — no pair of degrees the remark leaves unprescribed occurs. That covers every product the chapter forms: r₁ = max(p, q), the target the source displays (Stacks.Chow.localizedBivariantGradingMulMax), qualifies for min(p, q) ≤ 1, and so does r₁ = p + q, the target at which Stacks 0FAL and Stacks 0FAY state their products. The product internal to A⁽ᵖ⁾(Z ⟶ X) of the source's graded algebra, where all six targets are p ≤ 1, is the corollary Stacks.Chow.localizedBivariantGradingInternalMul_assoc; what associativity of that product would come to for p ≥ 2 is Stacks.Chow.localizedBivariantGradingInternalMul_singleLow_eq_zero_of_assoc.

It is an equality and not a heterogeneous equality because the common target r is a parameter; the degrees of the intermediate products are the arguments r₁, r₂, which the two groupings bracket differently. Degreewise the two sides are the same double convolution of the three factors' components written in the two decompositions (m, i - m, n - i) and (m, j, n - m - j) of the total degree n, and the proof is exactly the two pieces the implementation notes name: the reindexing Stacks.Chow.sum_Icc_diag_flip of that double convolution, and — term by term — the three instances of the associativity of Stacks 0B75 for the pairings, read through the transports the pairings carry by Stacks.Chow.bivariantClassDegreeCongr_eq_of_heq. Below the cutoff of the target both sides are the double convolution in A^*(X) (Stacks.Chow.localizedBivariantGradingMul_isAmbientConvolution) and the input is the associativity of the multiplication of A^*(X), Stacks.Chow.chowCohomologyComposite_assoc; at or above it one of the three pairings applies to each term, and where an intermediate product was read in A^*(X) the comparison also needs Stacks.Chow.localizedMulChowBivariant_localizedGradingPushforward_eq, that a localized factor may be pushed forward by Stacks 0EPK before it is multiplied on the left.

theorem localizedBivariantGradingMul_assoc (p q s r₁ r₂ r : ℕ) (h₁ : p + q ≤ r₁ + 1)
    (h₂ : r₁ + s ≤ r + 1) (h₃ : q + s ≤ r₂ + 1) (h₄ : p + r₂ ≤ r + 1)
    (a : localizedBivariantGrading C G (f ≫ sX) sX f rfl p)
    (b : localizedBivariantGrading C G (f ≫ sX) sX f rfl q)
    (c : localizedBivariantGrading C G (f ≫ sX) sX f rfl s) :
    localizedBivariantGradingMul C G sX f hRG hgysP hgys hgysc r₁ s r
        (localizedBivariantGradingMul C G sX f hRG hgysP hgys hgysc p q r₁ a b) c =
      localizedBivariantGradingMul C G sX f hRG hgysP hgys hgysc p r₂ r a
        (localizedBivariantGradingMul C G sX f hRG hgysP hgys hgysc q s r₂ b c)

Stacks.Chow.localizedBivariantGradingInternalMul_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingProjectionFormula/Associativity.lean, line 522. The attribute's comment: “associativity of the multiplication internal to A^(p)(Z ⟶ X) of the remark's graded algebra, for p ≤ 1, where no pair of degrees the remark leaves unprescribed occurs in a triple product”.

Stacks 0FA0, associativity of the multiplication internal to A⁽ᵖ⁾(Z ⟶ X), which is the associativity the source's "A⁽ᵖ⁾(Z ⟶ X) canonically comes equipped with the structure of a graded algebra" asks for, for p ≤ 1 — the p at which a triple product of the internal multiplication (Stacks.Chow.localizedBivariantGradingInternalMul, defined for every p ≥ 0) meets no pair of degrees the remark leaves unprescribed, Stacks.Chow.localizedGrading_self_admissible_iff. With Stacks.Chow.localizedBivariantGradingMul_add_left, Stacks.Chow.localizedBivariantGradingMul_add_right and the two unit laws Stacks.Chow.localizedBivariantGradingInternalMul_one_left and _one_right this completes the graded-algebra axioms for that product. For p ≥ 2 the content of associativity is Stacks.Chow.localizedBivariantGradingInternalMul_singleLow_eq_zero_of_assoc.

theorem localizedBivariantGradingInternalMul_assoc (p : ℕ) (hp : p ≤ 1)
    (a b c : localizedBivariantGrading C G (f ≫ sX) sX f rfl p) :
    localizedBivariantGradingInternalMul C G sX f hRG hgysP hgys hgysc p
        (localizedBivariantGradingInternalMul C G sX f hRG hgysP hgys hgysc p a b) c =
      localizedBivariantGradingInternalMul C G sX f hRG hgysP hgys hgysc p a
        (localizedBivariantGradingInternalMul C G sX f hRG hgysP hgys hgysc p b c)

Stacks.Chow.localizedBivariantGradingSemigroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingProjectionFormula/Associativity.lean, line 560. The attribute's comment: “the multiplicative structure of the remark's graded algebra on A^(p)(Z ⟶ X) as a bundled Semigroup, on all of A^(p)(Z ⟶ X) for p ≤ 1, where associativity of the internal product is proved: the multiplication of the remark together with its associativity, with no hypothesis beyond the Gysin compatibilities the product itself carries”.

Stacks 0FA0, the multiplicative structure of the remark's graded algebra on A⁽ᵖ⁾(Z ⟶ X) as a bundled Semigroup, on all of A⁽ᵖ⁾(Z ⟶ X) for p ≤ 1, which is where associativity of the internal product is proved. Nothing beyond the Gysin compatibilities of the product itself is assumed: the multiplication is Stacks.Chow.localizedBivariantGradingInternalMul, which is defined for every p ≥ 0, and the associativity is Stacks.Chow.localizedBivariantGradingInternalMul_assoc.

The unit of the algebra needs p ≥ 1, so the bundled Monoid is at p = 1: Stacks.Chow.localizedBivariantGradingMonoid.

def localizedBivariantGradingSemigroup (p : ℕ) (hp : p ≤ 1) :
    Semigroup (localizedBivariantGrading C G (f ≫ sX) sX f rfl p)

Stacks.Chow.localizedBivariantGradingMonoid, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingProjectionFormula/Associativity.lean, line 599. The attribute's comment: “the remark's graded algebra on A^(1)(Z ⟶ X) as a bundled Monoid -- the multiplication internal to A^(1)(Z ⟶ X), the class 1 of A^0(X) in degree 0 as its unit, associativity and the two unit laws -- at p = 1, where the unit's degree 0 slot is A^0(X) and associativity is proved, on all of A^(1)(Z ⟶ X)”.

Stacks 0FA0, the remark's graded algebra on A⁽¹⁾(Z ⟶ X) as a bundled Monoid: the multiplication internal to A⁽¹⁾(Z ⟶ X), its unit, and the three laws. This is the structure the source's "A⁽ᵖ⁾(Z ⟶ X) canonically comes equipped with the structure of a graded algebra" asserts on the multiplicative side. Its fields are Stacks.Chow.localizedBivariantGradingInternalMul, Stacks.Chow.localizedBivariantGradingOne, Stacks.Chow.localizedBivariantGradingInternalMul_assoc, Stacks.Chow.localizedBivariantGradingInternalMul_one_left and Stacks.Chow.localizedBivariantGradingInternalMul_one_right; the additive side of the algebra is the AddCommGroup the grading carries, with the distributive law Stacks.Chow.localizedBivariantGradingInternalMulHom.

p = 1 is where the three laws meet. The multiplication internal to A⁽ᵖ⁾(Z ⟶ X) is defined for every p ≥ 0 and the two unit laws hold for every p ≥ 1, the degree 0 slot where the unit sits being A⁰(X) exactly then; associativity is proved for p ≤ 1 (Stacks.Chow.localizedGrading_self_admissible_iff), and what it would come to for p ≥ 2 is Stacks.Chow.localizedBivariantGradingInternalMul_singleLow_eq_zero_of_assoc.

The carrier is all of A⁽¹⁾(Z ⟶ X), the group the source asserts the algebra on. That rests on the index range of the sums the product is formed from: a degree n component is the sum over Finset.Icc (min 0 n) (max 0 n), the pairs i + j = n whose two degrees both have the sign of n, and that range contains i = 0 and i = n in every degree (Stacks.Chow.zero_mem_Icc_min_max, Stacks.Chow.self_mem_Icc_min_max) — the two indices carrying the surviving term of a product with the unit on the left and on the right. The range is a reading of the source's ∑_{i + j = n}, which runs over an infinite index set; the reading and the witness that the index set is infinite with independent summands are in the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.BivariantLemmas.LocalizedGradingMultiplication.

def localizedBivariantGradingMonoid :
    Monoid (localizedBivariantGrading C G (f ≫ sX) sX f rfl 1)

Stacks.Chow.localizedBivariantGradingMulOfInvertible_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingProjectionFormula/Associativity.lean, line 629. The attribute's comment: “associativity of the canonical multiplication of the remark -- the verification the source omits -- at every choice of intermediate and common targets with p + q + s ≤ r + 2, at the Gysin system of the first Chern class rule, with NOTHING ASSUMED”.

Stacks 0FA0, associativity of the canonical multiplication at the Gysin system of the first Chern class rule, with nothing assumed: there every Gysin compatibility that Stacks 0F9Z, Stacks 0B75 and Stacks 0EPK carry for an arbitrary Gysin system is a theorem, and so is Stacks 02RG on Chow groups, which the pushforward of Stacks 0EPK costs. See Stacks.Chow.localizedBivariantGradingMul_assoc.

theorem localizedBivariantGradingMulOfInvertible_assoc (p q s r₁ r₂ r : ℕ) (h₁ : p + q ≤ r₁ + 1)
    (h₂ : r₁ + s ≤ r + 1) (h₃ : q + s ≤ r₂ + 1) (h₄ : p + r₂ ≤ r + 1)
    (a : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p)
    (b : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl q)
    (c : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl s) :
    localizedBivariantGradingMulOfInvertible C sX f r₁ s r
        (localizedBivariantGradingMulOfInvertible C sX f p q r₁ a b) c =
      localizedBivariantGradingMulOfInvertible C sX f p r₂ r a
        (localizedBivariantGradingMulOfInvertible C sX f q s r₂ b c)

Stacks.Chow.localizedBivariantGradingInternalMulOfInvertible_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedGradingProjectionFormula/Associativity.lean, line 651. The attribute's comment: “associativity of the multiplication internal to A^(p)(Z ⟶ X) of the remark's graded algebra, for p ≤ 1, at the Gysin system of the first Chern class rule with NOTHING ASSUMED”.

Stacks 0FA0, associativity of the multiplication internal to A⁽ᵖ⁾(Z ⟶ X) at the Gysin system of the first Chern class rule, with nothing assumed. This is the associativity of the source's graded algebra on A⁽ᵖ⁾(Z ⟶ X) for p ≤ 1, with no hypothesis of any kind beyond that bound.

theorem localizedBivariantGradingInternalMulOfInvertible_assoc (p : ℕ) (hp : p ≤ 1)
    (a b c : localizedBivariantGrading C (gysinSystemOfInvertible C) (f ≫ sX) sX f rfl p) :
    localizedBivariantGradingInternalMulOfInvertible C sX f p
        (localizedBivariantGradingInternalMulOfInvertible C sX f p a b) c =
      localizedBivariantGradingInternalMulOfInvertible C sX f p a
        (localizedBivariantGradingInternalMulOfInvertible C sX f p b c)

Tag 0FA1, a remark

Tag 0FA1 in the Stacks Project.

Stacks.Chow.bivariantRestrictionCap_id_eq_cap_properChowPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomology.lean, line 305.

Stacks 0FA1. For a closed immersion i : Z ⟶ X of schemes locally of finite type over the base and a bivariant class c of degree p for i, the restriction res(c) of c along i — a class of degree p for Z ×_X Z ⟶ Z, whose cap operation at the test scheme 𝟙 Z is read on Z through the canonical identification (Z ×_X Z) ×_Z Z ≅ Z — satisfies

res(c) ∩ α = c ∩ i_*α

in CH_{k-p}(Z) for every α ∈ CH_k(Z), the right-hand side being read on Z through the canonical identification X ×_X Z ≅ Z.

theorem bivariantRestrictionCap_id_eq_cap_properChowPushforward
    (c : BivariantClass C G sZ sX i hi p) (k : ℤ)
    (hfac : ProperPushforwardFactorsThroughRationalEquivalence C sZ sX i hi k)
    (α : chowGroup C sZ k) :
    chowPushforwardOfIso C (pullback.fst (pullback.snd i i) (𝟙 Z) ≫ (pullback.fst i i ≫ sZ)) sZ
        (selfPullbackIdIso i).inv (selfPullbackIdIso_inv_comp i sZ) (k - p)
        (bivariantRestrictionCap C G sZ sX i hi i p c (𝟙 Z) k
          (chowGroupCongr C (id_comp_comp_structureMorphism_eq C sZ sX i hi) k α)) =
      chowPushforwardOfIso C (pullback.fst i (𝟙 X) ≫ sZ) sZ (pullbackIdIso i).inv
        (pullbackIdIso_inv_comp i sZ) (k - p)
        (c.cap (𝟙 X) k (chowGroupCongr C (Category.id_comp sX).symm k
          (properChowPushforward C sZ sX i hi k hfac α)))

Stacks.Chow.bivariantRestriction_cap_id_eq_cap_properChowPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomology.lean, line 386. The attribute's comment: “for the restricted bivariant class”.

Stacks 0FA1 for the restricted class itself: the bivariant class Stacks.Chow.bivariantRestriction of c along the closed immersion i, read at the test scheme 𝟙 Z, satisfies res(c) ∩ α = c ∩ i_*α in CH_{k-p}(Z).

theorem bivariantRestriction_cap_id_eq_cap_properChowPushforward
    (hgys : G.IsNaturalUnderBaseChangeIso) (c : BivariantClass C G sZ sX i hi p) (k : ℤ)
    (hfac : ProperPushforwardFactorsThroughRationalEquivalence C sZ sX i hi k)
    (α : chowGroup C sZ k) :
    chowPushforwardOfIso C (pullback.fst (pullback.snd i i) (𝟙 Z) ≫ (pullback.fst i i ≫ sZ)) sZ
        (selfPullbackIdIso i).inv (selfPullbackIdIso_inv_comp i sZ) (k - p)
        ((bivariantRestriction C G sZ sX i hi i p hgys c).cap (𝟙 Z) k
          (chowGroupCongr C (id_comp_comp_structureMorphism_eq C sZ sX i hi) k α)) =
      chowPushforwardOfIso C (pullback.fst i (𝟙 X) ≫ sZ) sZ (pullbackIdIso i).inv
        (pullbackIdIso_inv_comp i sZ) (k - p)
        (c.cap (𝟙 X) k (chowGroupCongr C (Category.id_comp sX).symm k
          (properChowPushforward C sZ sX i hi k hfac α)))

Stacks.Chow.closedImmersionChowCohomologyRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomology.lean, line 404. The attribute's comment: “the restriction map to A^p(Z)”.

Stacks 0FA1. The restriction map res : A^p(Z ⟶ X) ⟶ A^p(Z) along a closed immersion i : Z ⟶ X, a homomorphism of groups: the restriction map of Stacks 0F9Z along i, followed by the transport of a bivariant class along the canonical isomorphism Z ×_X Z ≅ Z.

def closedImmersionChowCohomologyRestriction (hgys : G.IsNaturalUnderBaseChangeIso) :
    BivariantClass C G sZ sX i hi p →+ chowCohomologyComponent C G (i ≫ sX) p

Stacks.Chow.closedImmersionChowCohomologyRestriction_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomology.lean, line 424. The attribute's comment: “the cap formula for the restriction map to A^p(Z)”.

Stacks 0FA1. The restriction map res : A^p(Z ⟶ X) ⟶ A^p(Z) of a closed immersion satisfies res(c) ∩ α = c ∩ i_*α in CH_{k-p}(Z) for every α ∈ CH_k(Z), both sides being read on Z through the canonical identifications Z ×_Z Z ≅ Z and X ×_X Z ≅ Z.

theorem closedImmersionChowCohomologyRestriction_cap (hgys : G.IsNaturalUnderBaseChangeIso)
    (c : BivariantClass C G sZ sX i hi p) (k : ℤ)
    (hfac : ProperPushforwardFactorsThroughRationalEquivalence C sZ sX i hi k)
    (α : chowGroup C sZ k) :
    chowPushforwardOfIso C (pullback.fst (𝟙 Z) (𝟙 Z) ≫ (i ≫ sX)) sZ
        (identityBaseChangeIso (𝟙 Z)).hom
        (identityBaseChangeIso_id_comp_base C sZ sX i hi) (k - p)
        ((closedImmersionChowCohomologyRestriction C G sZ sX i hi p hgys c).cap (𝟙 Z) k
          (chowGroupCongr C (id_comp_comp_structureMorphism_eq C sZ sX i hi) k α)) =
      chowPushforwardOfIso C (pullback.fst i (𝟙 X) ≫ sZ) sZ (pullbackIdIso i).inv
        (pullbackIdIso_inv_comp i sZ) (k - p)
        (c.cap (𝟙 X) k (chowGroupCongr C (Category.id_comp sX).symm k
          (properChowPushforward C sZ sX i hi k hfac α)))

Stacks.Chow.bivariantRestrictionCap_id_eq_cap_properChowPushforward_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOfInvertible.lean, line 68.

For a Gysin system G, a closed immersion i : Z ⟶ X of schemes locally of finite type over the base and a bivariant class c of degree p for i, the restriction res(c) of c along i, read at the test scheme 𝟙 Z, satisfies

res(c) ∩ α = c ∩ i_*α

in CH_{k-p}(Z) for every α ∈ CH_k(Z).

theorem bivariantRestrictionCap_id_eq_cap_properChowPushforward_unconditional
    (c : BivariantClass C G sZ sX i hi p) (k : ℤ) (α : chowGroup C sZ k) :
    chowPushforwardOfIso C (pullback.fst (pullback.snd i i) (𝟙 Z) ≫ (pullback.fst i i ≫ sZ)) sZ
        (selfPullbackIdIso i).inv (selfPullbackIdIso_inv_comp i sZ) (k - p)
        (bivariantRestrictionCap C G sZ sX i hi i p c (𝟙 Z) k
          (chowGroupCongr C (id_comp_comp_structureMorphism_eq C sZ sX i hi) k α)) =
      chowPushforwardOfIso C (pullback.fst i (𝟙 X) ≫ sZ) sZ (pullbackIdIso i).inv
        (pullbackIdIso_inv_comp i sZ) (k - p)
        (c.cap (𝟙 X) k (chowGroupCongr C (Category.id_comp sX).symm k
          (properChowPushforward C sZ sX i hi k
            (properPushforwardFactorsThroughRationalEquivalence C sZ sX i hi k) α)))

Stacks.Chow.bivariantRestrictionOfInvertible_cap_id_eq_cap_properChowPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOfInvertible.lean, line 97. The attribute's comment: “for the restricted bivariant class, at the Gysin system of the first Chern class rule, with the isomorphism case of Stacks 02TA discharged”.

At the Gysin system of the first Chern class rule of an invertible module, the restriction res(c) of Stacks 0F9Z of a bivariant class c of degree p for the closed immersion i : Z ⟶ X — a class for Z ×_X Z ⟶ Z, read at the test scheme 𝟙 Z — satisfies

res(c) ∩ α = c ∩ i_*α

in CH_{k-p}(Z) for every α ∈ CH_k(Z).

theorem bivariantRestrictionOfInvertible_cap_id_eq_cap_properChowPushforward
    (c : BivariantClass C (gysinSystemOfInvertible C) sZ sX i hi p) (k : ℤ)
    (α : chowGroup C sZ k) :
    chowPushforwardOfIso C (pullback.fst (pullback.snd i i) (𝟙 Z) ≫ (pullback.fst i i ≫ sZ)) sZ
        (selfPullbackIdIso i).inv (selfPullbackIdIso_inv_comp i sZ) (k - p)
        ((bivariantRestriction C (gysinSystemOfInvertible C) sZ sX i hi i p
            (gysinSystemOfInvertible_isNaturalUnderBaseChangeIso C) c).cap (𝟙 Z) k
          (chowGroupCongr C (id_comp_comp_structureMorphism_eq C sZ sX i hi) k α)) =
      chowPushforwardOfIso C (pullback.fst i (𝟙 X) ≫ sZ) sZ (pullbackIdIso i).inv
        (pullbackIdIso_inv_comp i sZ) (k - p)
        (c.cap (𝟙 X) k (chowGroupCongr C (Category.id_comp sX).symm k
          (properChowPushforward C sZ sX i hi k
            (properPushforwardFactorsThroughRationalEquivalence C sZ sX i hi k) α)))

Stacks.Chow.closedImmersionChowCohomologyRestrictionOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOfInvertible.lean, line 118. The attribute's comment: “the restriction map to A^p(Z), at the Gysin system of the first Chern class rule, with the isomorphism case of Stacks 02TA discharged”.

The restriction map res : A^p(Z ⟶ X) ⟶ A^p(Z) along a closed immersion i : Z ⟶ X, as a group homomorphism, at the Gysin system of the first Chern class rule of an invertible module.

def closedImmersionChowCohomologyRestrictionOfInvertible :
    BivariantClass C (gysinSystemOfInvertible C) sZ sX i hi p →+
      chowCohomologyComponent C (gysinSystemOfInvertible C) (i ≫ sX) p

Stacks.Chow.closedImmersionChowCohomologyRestrictionOfInvertible_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOfInvertible.lean, line 133. The attribute's comment: “the cap formula for the restriction map to A^p(Z), at the Gysin system of the first Chern class rule, with the isomorphism case of Stacks 02TA discharged”.

At the Gysin system of the first Chern class rule of an invertible module, the restriction map res : A^p(Z ⟶ X) ⟶ A^p(Z) of a closed immersion i : Z ⟶ X satisfies

res(c) ∩ α = c ∩ i_*α

in CH_{k-p}(Z) for every α ∈ CH_k(Z), both sides being read on Z through the canonical identifications Z ×_Z Z ≅ Z and X ×_X Z ≅ Z.

theorem closedImmersionChowCohomologyRestrictionOfInvertible_cap
    (c : BivariantClass C (gysinSystemOfInvertible C) sZ sX i hi p) (k : ℤ)
    (α : chowGroup C sZ k) :
    chowPushforwardOfIso C (pullback.fst (𝟙 Z) (𝟙 Z) ≫ (i ≫ sX)) sZ
        (identityBaseChangeIso (𝟙 Z)).hom
        (identityBaseChangeIso_id_comp_base C sZ sX i hi) (k - p)
        ((closedImmersionChowCohomologyRestrictionOfInvertible C sZ sX i hi p c).cap (𝟙 Z) k
          (chowGroupCongr C (id_comp_comp_structureMorphism_eq C sZ sX i hi) k α)) =
      chowPushforwardOfIso C (pullback.fst i (𝟙 X) ≫ sZ) sZ (pullbackIdIso i).inv
        (pullbackIdIso_inv_comp i sZ) (k - p)
        (c.cap (𝟙 X) k (chowGroupCongr C (Category.id_comp sX).symm k
          (properChowPushforward C sZ sX i hi k
            (properPushforwardFactorsThroughRationalEquivalence C sZ sX i hi k) α)))

Sources

LeanStacks.Chow.chowCohomologyGRingOfInvertible · Stacks.Chow.chowCohomologyRingOfInvertible · Stacks.Chow.chowCohomologyAlgebraOfInvertible · Stacks.Chow.ChowCohomologyGroup · Stacks.Chow.ChowCohomologyGroup.instGRing · Stacks.Chow.ChowCohomology · Stacks.Chow.chowCohomologyComponent · Stacks.Chow.chowCohomology

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

42.31 Relative effective… to 42.34 Chow cohomology and the…

Section42.31 Relative effective Cartier divisors#

Tag 02TR, a lemma

Sources

Section42.32 Affine bundles#

Tag 02TT, a lemma

Tag 0B74, a lemma

Tag 02TU, a remark

Tag 0F96, a lemma

Tag 0F97, a lemma

Tag 0F98, a lemma

Tag 0F99, a lemma

Tag 0GUB, a remark

Sources

Section42.33 Bivariant intersection theory#

Tag 0B75, the section

Tag 0B76, a definition

Tag 0B78, a lemma

Tag 0B79, a lemma

Tag 0EPK, a lemma

Tag 0F9Z, a remark

Tag 0FA2, a remark

Tag 0FA3, an example

Tag 0FDU, a remark

Sources

Section42.34 Chow cohomology and the first Chern class#

Tag 0B7E, a definition

Tag 0B7F, a remark

Tag 0B77, a lemma

Tag 0FDW, a definition

Tag 0B7B, a lemma

Tag 0FDX, a lemma

Tag 0FA0, a remark

Tag 0FA1, a remark

Sources

Section42.31 Relative effective Cartier divisors #

Section42.32 Affine bundles #

Section42.33 Bivariant intersection theory #

Section42.34 Chow cohomology and the first Chern class #