42.59 Gysin maps for local… to 42.67 Change of base scheme

Section42.59 Gysin maps for local complete intersection morphisms#

Section 42.59 of the Stacks Project, Tag 0FEZ. 13 tags here are carried by 35 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FF0, a lemma

Tag 0FF0 in the Stacks Project.

Stacks.Chow.ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/RegularImmersionGysinComposition.lean, line 300. The attribute's comment: “second assertion: the three normal bundles of a pair of regular immersions satisfy the hypothesis of Stacks 0FEC, by the short exact conormal sequence of Stacks 063N”.

Stacks 0FF0, the geometric input of the second assertion. The three normal bundles of a pair of regular immersions Z ⟶ Y ⟶ X of locally Noetherian schemes form a conormal-compatible triple in the sense of Stacks 0FEC: the sequence of their duals is the conormal sequence of Stacks 062S conjugated by the three reflexivity isomorphisms, it is short exact by Stacks 063N, and its two squares against the conormal sequence commute because the three structural surjections are the inverses of those isomorphisms.

def ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion :
    ConormalCompatibleVirtualNormalBundles i j

Stacks.Chow.localizedChernClass_cap_eq_bivariantCompositeCap_of_isRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/RegularImmersionGysinComposition.lean, line 357. The attribute's comment: “second assertion, (j ∘ i)^! = i^! ∘ j^! read on cap products, at the canonical normal bundles of the two regular immersions; the localized Chern class of Stacks 0FBK is a parameter and the composition formula of Stacks 0FEC is an input, exactly as in Stacks 0FEC”.

Stacks 0FF0, second assertion, read on cap products. For regular immersions i : Z ⟶ Y and j : Y ⟶ X of schemes locally of finite type over the base, equipped with their canonical normal bundles, the Gysin map of j ∘ i on a test scheme t : T ⟶ X is: cap with j^!, then cap with i^!, then push forward along the associativity isomorphism (T ×_X Y) ×_Y Z ≅ T ×_X Z of pullbacks.

This is Stacks 0FEC at the conormal-compatible triple of the two regular immersions, so the composition formula for the three parameterized classes of Stacks 0FBK is an input, as it is in the two theorems of Stacks 0FEC themselves.

theorem localizedChernClass_cap_eq_bivariantCompositeCap_of_isRegularImmersion
    (hc : IsBivariantClassComposition C G sZ sY sX i j hsi hsj hpp p q
      (cloc sZ sY i hsi
        (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleZY p)
      (cloc sY sX j hsj
        (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleYX q)
      (cloc sZ sX (i ≫ j) (comp_comp_structureMorphism_eq hsi hsj)
        (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleZX (p + q)))
    {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
    (α : chowGroup C (t ≫ sX) k) :
    chowGroupDegreeEquiv C (pullback.fst (i ≫ j) t ≫ sZ)
        (by ring : k - (p + q) = (k - q) - p)
        ((cloc sZ sX (i ≫ j) (comp_comp_structureMorphism_eq hsi hsj)
          (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleZX
          (p + q)).cap t k α) =
      bivariantCompositeCap C G sZ sY sX i j hsi hsj hpp p q
        (cloc sZ sY i hsi
          (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleZY p)
        (cloc sY sX j hsj
          (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleYX q)
        t k α

Stacks.Chow.localizedChernClass_eq_bivariantComposite_of_isRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/RegularImmersionGysinComposition.lean, line 394. The attribute's comment: “second assertion, (j ∘ i)^! = i^! ∘ j^! as an equality of bivariant classes, at the canonical normal bundles of the two regular immersions; the localized Chern class of Stacks 0FBK is a parameter and the composition formula of Stacks 0FEC is an input, exactly as in Stacks 0FEC”.

Stacks 0FF0, second assertion, as an equality of bivariant classes. For regular immersions i : Z ⟶ Y and j : Y ⟶ X of schemes locally of finite type over the base, equipped with their canonical normal bundles, the Gysin class of j ∘ i is the composite of Stacks 0B75 of the Gysin class of i with the Gysin class of j:

(j ∘ i)^! = i^! ∘ j^! in A^{p+q}(Z ⟶ X).

Both classes satisfy the composition formula of Stacks 0FEC — the composite by Stacks 0FE0 — and that formula determines the class, so they agree.

theorem localizedChernClass_eq_bivariantComposite_of_isRegularImmersion
    (hgys : G.IsNaturalUnderBaseChangeIso)
    (hgysc : G.IsNaturalUnderPullbackCompPushforward)
    (hc : IsBivariantClassComposition C G sZ sY sX i j hsi hsj hpp p q
      (cloc sZ sY i hsi
        (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleZY p)
      (cloc sY sX j hsj
        (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleYX q)
      (cloc sZ sX (i ≫ j) (comp_comp_structureMorphism_eq hsi hsj)
        (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleZX
        (p + q))) :
    cloc sZ sX (i ≫ j) (comp_comp_structureMorphism_eq hsi hsj)
        (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleZX
        (p + q) =
      bivariantComposite C G sZ sY sX i j hsi hsj p q
        (cloc sZ sY i hsi
          (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleZY p)
        (cloc sY sX j hsj
          (ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion i j hi hj).bundleYX q)
        hgys hgysc

Stacks.Chow.completedVirtualNormalGysinClassOfImmersion_comp_ofIsRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinMapComposition.lean, line 73. References: SGA 6 VIII (1.5), “special case”.

Stacks 0FF0. Let s : X ⟶ W and j : W ⟶ P be regular immersions of schemes locally of finite type over the base. Then s ≫ j is a regular immersion and

(j ∘ s)^! = s^! ∘ j^! in A^*(X ⟶ P)^∧,

where (−)^! is the class c(− , 𝒩) of Stacks 0FBQ (3) of the normal bundle 𝒩 = 𝒞^∨ of the regular immersion.

theorem completedVirtualNormalGysinClassOfImmersion_comp_ofIsRegularImmersion
    (C : ChowSituation.{u}) {X W P : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (sW : W ⟶ C.S) [LocallyOfFiniteType sW] (sP : P ⟶ C.S) [LocallyOfFiniteType sP]
    (s : X ⟶ W) (j : W ⟶ P) [IsImmersion s] [IsImmersion j] (hs : s ≫ sW = sX)
    (hj : j ≫ sP = sW) (hsr : IsRegularImmersion s) (hjr : IsRegularImmersion j) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    letI : IsLocallyNoetherian W := LocallyOfFiniteType.isLocallyNoetherian sW
    letI : IsLocallyNoetherian P := LocallyOfFiniteType.isLocallyNoetherian sP
    ∃ hr : IsRegularImmersion (s ≫ j),
      completedVirtualNormalGysinClassOfImmersion C sX sP (s ≫ j)
          (comp_comp_structureMorphism_eq hs hj)
          (VirtualNormalBundle.ofIsRegularImmersion (s ≫ j) hr) =
        completedBivariantCompositeOfInvertible C sX sW sP s j hs hj
          (completedVirtualNormalGysinClassOfImmersion C sX sW s hs
            (VirtualNormalBundle.ofIsRegularImmersion s hsr))
          (completedVirtualNormalGysinClassOfImmersion C sW sP j hj
            (VirtualNormalBundle.ofIsRegularImmersion j hjr))

Declarations registered for the tag:

Tag 0FF1, a lemma

Tag 0FF1 in the Stacks Project.

Stacks.Chow.completedBivariantCompositeOfInvertible_completedFlatPullbackOfSmooth_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/SectionOfSmooth.lean, line 118. The attribute's comment: “second assertion: 1 = s^! ∘ p^ in A^(X)^∧, the composite read as a completed class for 𝟙 X along s ≫ p = 𝟙 X”.

Let p : P ⟶ X be a smooth morphism of schemes locally of finite type over the base and s : X ⟶ P a section of p, a regular immersion by Stacks.AlgebraicGeometry.isRegularImmersion_of_smooth_section. Then

1 = s^! ∘ p^* in A^*(X)^∧,

for s^! = c(X ⟶ P, 𝒩_{X/P}) the class of Stacks 0FBQ (3) of the normal sheaf of s and p^* the flat pullback of Stacks 0B78; the composite, a class for s ≫ p, is read as a class for 𝟙 X = s ≫ p.

theorem completedBivariantCompositeOfInvertible_completedFlatPullbackOfSmooth_of_section :
    letI : IsImmersion s := Stacks.AlgebraicGeometry.isImmersion_of_comp_eq_id s p hs
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    letI : IsLocallyNoetherian P := LocallyOfFiniteType.isLocallyNoetherian sP
    completedBivariantGroup.copy C hs
        (comp_comp_structureMorphism_eq (comp_structureMorphism_of_comp_eq_id hp hs) hp)
        (Category.id_comp sX)
        (completedBivariantCompositeOfInvertible C sX sP sX s p
          (comp_structureMorphism_of_comp_eq_id hp hs) hp
          (completedVirtualNormalGysinClassOfImmersion C sX sP s
            (comp_structureMorphism_of_comp_eq_id hp hs)
            (VirtualNormalBundle.ofIsRegularImmersion s
              (Stacks.AlgebraicGeometry.isRegularImmersion_of_smooth_section p s hs)))
          (completedFlatPullbackOfSmooth C sP sX p hp)) =
      completedIdentityClass C sX

Declarations registered for the tag:

Tag 0FF2, a lemma

Tag 0FF2 in the Stacks Project.

Stacks.Chow.SmoothFactorization.isKoszulRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/FactorizationIndependence.lean, line 213. The attribute's comment: “regularity of the immersion of a factorization of an lci morphism, which the statement of Stacks 0FF2 leaves implicit; Stacks 069G enters through its repository form, so the Koszul case of Stacks 0693 is carried as hcompSmooth”. References: SGA 6 VIII (1.2).

Stacks 069G, for a factorization of a local complete intersection morphism. The immersion i : X ⟶ P of a factorization f = g ∘ i of a local complete intersection morphism f is a Koszul-regular immersion. This is what makes the Gysin class i^! of section 42.54 of the Stacks Project available, and it is the reason Stacks 0FF2 need not assume regularity of the immersion.

Stacks 069G is stated for an immersion of an open of the source; it is applied here to the top open and transported back along AlgebraicGeometry.Scheme.topIso. The Koszul case of Stacks 0693 is a hypothesis of Stacks 069G in this repository, hence of this statement.

theorem SmoothFactorization.isKoszulRegularImmersion
    (hcompSmooth : AlgebraicGeometry.KoszulRegularCompSmooth.{u}) (F : SmoothFactorization f)
    (hf : IsLocalCompleteIntersectionMorphism f) : IsKoszulRegularImmersion F.imm

Stacks.Chow.SmoothFactorization.exists_refines_both, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/FactorizationIndependence.lean, line 292. The attribute's comment: “the first step of the proof: any two immersion--smooth factorizations of f are refined by a common one, through P ×_Y P', which reduces the independence of f^! to the case of a single refinement p : P' ⟶ P”.

Stacks 0FF2, first step. Any two factorizations of f as an immersion followed by a smooth morphism are refined by a common one, namely the factorization through the fibre product of their intermediate schemes over Y. The independence of f^! therefore reduces to the case of a refining pair.

theorem SmoothFactorization.exists_refines_both :
    ∃ F'' : SmoothFactorization f, F''.Refines F ∧ F''.Refines F'

Stacks.Chow.SmoothFactorization.isKoszulRegularImmersion_refinementProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/FactorizationIndependence.lean, line 389. The attribute's comment: “the second step of the proof: the base change j of the immersion along the refinement is a Koszul-regular immersion, the Koszul-regular part of Stacks 067P; the regularity of i is the prerequisite hreg, supplied for an lci morphism by Stacks 069G”.

Stacks 0FF2, second step: regularity of j. The base change j : X ×_P P' ⟶ P' of the immersion i of F along the refinement p is a Koszul-regular immersion, by the Koszul-regular part of Stacks 067P: p is smooth, hence flat. For a local complete intersection morphism f the hypothesis on i is automatic, by Stacks.Chow.SmoothFactorization.isKoszulRegularImmersion.

theorem SmoothFactorization.isKoszulRegularImmersion_refinementProj
    (hreg : IsKoszulRegularImmersion F.imm) :
    IsKoszulRegularImmersion (F.refinementProj p)

Stacks.Chow.SmoothFactorization.isRegularImmersion_refinementSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/FactorizationIndependence.lean, line 400. The attribute's comment: “the second step of the proof: the section s = (1, i') of the smooth retraction p̄ : X ×_P P' ⟶ X is a regular immersion, Stacks 067R”.

Stacks 0FF2, second step: regularity of s. The section s = (1, i') of the smooth retraction p̄ is a regular immersion, by Stacks 067R. Together with the regularity of j this is what makes both Gysin classes in the Stacks Project's identity (i')^! = s^! ∘ j^! (Stacks 0FF0) available.

theorem SmoothFactorization.isRegularImmersion_refinementSection :
    IsRegularImmersion (F.refinementSection p hp)

Stacks.Chow.SmoothFactorization.exists_refinement_diagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/FactorizationIndependence.lean, line 416. The attribute's comment: “the second step of the proof, packaged for a refining pair: the cartesian square W = X ×_P P' with its smooth retraction p̄, the base change j of the immersion, and the section s of p̄ satisfying i' = s ≫ j, with j Koszul-regular and s regular; the regularity of the coarser immersion is the prerequisite hreg”.

Stacks 0FF2, second step, packaged. For a refining pair of factorizations of f, with the immersion of the coarser one Koszul-regular, the diagram of the second step of the proof of Stacks 0FF2 exists: a scheme W = X ×_P P', a smooth retraction p̄ : W ⟶ X, the base change j : W ⟶ P' of i along the refinement, and a section s : X ⟶ W of p̄ with s ≫ j = i', where j is a Koszul-regular immersion and s a regular immersion.

theorem SmoothFactorization.exists_refinement_diagram {F F' : SmoothFactorization f}
    (h : F'.Refines F) (hreg : IsKoszulRegularImmersion F.imm) :
    ∃ (W : Scheme.{u}) (pbar : W ⟶ X) (j : W ⟶ F'.ambient) (s : X ⟶ W),
      Smooth pbar ∧ s ≫ pbar = 𝟙 X ∧ s ≫ j = F'.imm ∧
        ∃ (hj : IsImmersion j) (hs : IsImmersion s),
          (letI := hj; IsKoszulRegularImmersion j) ∧ letI := hs; IsRegularImmersion s

Stacks.Chow.SmoothFactorization.gysinMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinMapComposition.lean, line 104.

Stacks 0FF2. Let f : X ⟶ Y be a local complete intersection morphism of schemes locally of finite type over the base. The Gysin map f^! = i^! ∘ g^* ∈ A^*(X ⟶ Y)^∧ of a factorization f = g ∘ i, i an immersion and g smooth (Stacks 0FF3), does not depend on the factorization.

theorem SmoothFactorization.gysinMap_eq (F F' : SmoothFactorization f)
    (hlci : IsLocalCompleteIntersectionMorphism f) :
    F.gysinMap C sX sY hf hlci = F'.gysinMap C sX sY hf hlci
Tag 0FF3, a definition

Tag 0FF3 in the Stacks Project.

Stacks.Chow.GysinMapExists, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection.lean, line 73. The attribute's comment: “the existence of the Gysin map”.

Stacks 0FF3. The Gysin map of a local complete intersection morphism f : X ⟶ Y of schemes locally of finite type over the base exists when f factors as an immersion i : X ⟶ P followed by a smooth morphism g : P ⟶ Y.

def GysinMapExists {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop

Stacks.Chow.SmoothFactorization.gysinMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/GysinMap.lean, line 83. The attribute's comment: “the Gysin map f^! = i^! ∘ g^ ∈ A^(X → Y)^∧ of a factorization f = g ∘ i, i an immersion and g smooth, of a local complete intersection morphism”.

Stacks 0FF3, the Gysin map of a factorization. For a local complete intersection morphism f : X ⟶ Y and a factorization f = g ∘ i with i : X ⟶ P an immersion and g : P ⟶ Y smooth, the class

f^! = i^! ∘ g^* ∈ A^*(X ⟶ Y)^∧,

the composite (Stacks 0FE0) of the class i^! = c(X ⟶ P, 𝒩_{X/P}) of the regular immersion i (Stacks 0FBK, 0FBQ (3)) with the flat pullback g^* of the smooth morphism g (Stacks 0B78).

def SmoothFactorization.gysinMap (F : SmoothFactorization f)
    (hlci : IsLocalCompleteIntersectionMorphism f) :
    completedBivariantGroup C (gysinSystemOfInvertible C) sX sY f hf

Stacks.Chow.lciGysinMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/GysinMap.lean, line 104. The attribute's comment: “the Gysin map f^! ∈ A^*(X → Y)^∧ of a local complete intersection morphism for which the Gysin map exists”.

Stacks 0FF3, the Gysin map f^! of a local complete intersection morphism f : X ⟶ Y of schemes locally of finite type over the base for which the Gysin map exists: the class i^! ∘ g^* of a chosen factorization f = g ∘ i. By Stacks 0FF2 it does not depend on the choice (Stacks.Chow.SmoothFactorization.gysinMap_eq_lciGysinMap).

def lciGysinMap (hlci : IsLocalCompleteIntersectionMorphism f) (h : GysinMapExists f) :
    completedBivariantGroup C (gysinSystemOfInvertible C) sX sY f hf

Stacks.Chow.lciGysinClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinClass.lean, line 174. The attribute's comment: “the Gysin map f^! = i^! ∘ g^ in A^(X → Y)^∧ of a local complete intersection morphism f = g ∘ i, g smooth, i an immersion: i^! = c(X → U, N_{X/U}) of Tag 0FBK for the regular closed immersion of X into the open U ⊆ P where i is closed, g^* the flat pullback of Tag 0B78 on each connected component, ∘ the completed composition of Tag 0FE0”.

The Gysin map f^! = i^! ∘ g^* ∈ A^*(X ⟶ Y)^∧ of a local complete intersection morphism f : X ⟶ Y of schemes locally of finite type over S, for a factorization F of f as an immersion i : X ⟶ P followed by a smooth morphism g : P ⟶ Y: the composite in the completed groups of the class i^! = c(X ⟶ U, 𝒩_{X/U}) of the normal sheaf of the regular closed immersion i' : X ⟶ U into the open U ⊆ P in which i is closed, and of the flat pullback (g|_U)^* along the smooth morphism g|_U.

def lciGysinClass :
    completedBivariantGroup C (gysinSystemOfInvertible C) sX sY f hfs
Tag 0FF4, a lemma

Tag 0FF4 in the Stacks Project.

Stacks.Chow.lciGysinMap_eq_completedFlatPullbackOfFlatLCI, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinFlat.lean, line 381. The attribute's comment: “f^! = f^ in the completed bivariant group A^(X → Y)^∧, the relative dimension of the flat morphism f being only locally constant”.

Stacks 0FF4. Let f : X ⟶ Y be a local complete intersection morphism of schemes locally of finite type over the base for which the Gysin map exists. If f is flat, its Gysin map f^! ∈ A^*(X ⟶ Y)^∧ (Stacks 0FF3) is the flat-pullback class f^* of Stacks 0B78, read in the completed bivariant group because the relative dimension of f is only locally constant.

theorem lciGysinMap_eq_completedFlatPullbackOfFlatLCI [Flat f]
    (hlci : IsLocalCompleteIntersectionMorphism f) (h : GysinMapExists f) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    letI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
    lciGysinMap C sX sY hf hlci h = completedFlatPullbackOfFlatLCI C sX sY f hf hlci
Tag 0FF5, a lemma

Tag 0FF5 in the Stacks Project.

Stacks.Chow.GysinMapExists.left_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/Factorization.lean, line 78. The attribute's comment: “the Gysin map exists for the first factor of the composite”.

Stacks 0FF5, first assertion. If the Gysin map exists for a composite f ≫ g, then it exists for f.

Given a factorization f ≫ g = i ≫ q with i : X ⟶ P an immersion and q : P ⟶ Z smooth, the morphism X ⟶ P ×_Z Y induced by i and f is an immersion, because composing it with the projection to P returns i, and the projection P ×_Z Y ⟶ Y is smooth, being a base change of q. Their composite is f.

theorem GysinMapExists.left_of_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (h : GysinMapExists (f ≫ g)) : GysinMapExists f

Stacks.Chow.lciGysinMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinMapComposition.lean, line 135.

Stacks 0FF5. Let f : X ⟶ Y and g : Y ⟶ Z be local complete intersection morphisms of schemes locally of finite type over the base, and assume the Gysin map exists for g ∘ f and for g (Stacks 0FF3). Then the Gysin map exists for f, and

(g ∘ f)^! = f^! ∘ g^! in A^*(X ⟶ Z)^∧.

(g ∘ f is a local complete intersection morphism by Stacks 069J.)

theorem lciGysinMap_comp (hlf : IsLocalCompleteIntersectionMorphism f)
    (hlg : IsLocalCompleteIntersectionMorphism g) (hgf : GysinMapExists (f ≫ g))
    (hG : GysinMapExists g) :
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    ∃ hF : GysinMapExists f,
      lciGysinMap C sX sZ (comp_comp_structureMorphism_eq hf hg)
          (isLocalCompleteIntersectionMorphism_comp f g hlf hlg) hgf =
        completedBivariantCompositeOfInvertible C sX sY sZ f g hf hg
          (lciGysinMap C sX sY hf hlf hF) (lciGysinMap C sY sZ hg hlg hG)
Tag 0FF6, a lemma

Tag 0FF6 in the Stacks Project.

Stacks.Chow.bivariantCommute_flatPullbackBivariantClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/FlatPullbackCommuting.lean, line 189. The attribute's comment: “the smooth half only: the flat-pullback bivariant class of Stacks 0B78 commutes with an arbitrary bivariant class. The i^! half of the factorization f = i ≫ g is excluded; it is Stacks 0FBP, which has no carrier here, as has every tag needed to build f^!”.

The smooth half of Stacks 0FF6. The flat-pullback bivariant class of Stacks 0B78 for a flat morphism f₁ : Z₁ ⟶ X of relative dimension r commutes, in the sense of Stacks 0FA2, with every bivariant class c₂ ∈ A^{p₂}(Z₂ ⟶ X).

This is the g^* half of the factorization f = i ≫ g by which the source proves Stacks 0FF6, and the source's reason is the one used here: it is immediate from the flat-pullback law of Stacks 0B76 (2) for c₂. The i^! half is Stacks 0FBP, which has no carrier in this repository; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.Bivariant.FlatPullbackCommuting.

theorem bivariantCommute_flatPullbackBivariantClass :
    BivariantCommute C G sX f₁ f₂ (-(r : ℤ)) p₂
      (flatPullbackBivariantClass C G (f₁ ≫ sX) sX f₁ rfl r hfr hS1 hRG h71) c₂

Stacks.Chow.completedCommutesWithEveryClass_completedBivariantRestriction_lciGysinMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/GysinMapCommutes.lean, line 98. The attribute's comment: “for every Y' → Y, the restriction res(f^!) ∈ A^*(X' → Y')^∧ of the Gysin map of a local complete intersection morphism commutes with every c ∈ A^q(Y'' → Y'), every Y'' → Y' and q”.

Stacks 0FF6. Let f : X ⟶ Y be a local complete intersection morphism of schemes locally of finite type over the base such that the Gysin map f^! ∈ A^*(X ⟶ Y)^∧ exists (Stacks 0FF3). For every g : Y' ⟶ Y locally of finite type, the restriction res(f^!) ∈ A^*(X' ⟶ Y')^∧ of f^! along g (Stacks 0F9Z), X' = X ×_Y Y', commutes with every bivariant class c ∈ A^q(Y'' ⟶ Y'), for every Y'' ⟶ Y' locally of finite type and every degree q, in the sense of Stacks 0FA2, degree by degree: every term of the tuple attached to res(f^!) by Stacks 0FE0 commutes with c.

theorem completedCommutesWithEveryClass_completedBivariantRestriction_lciGysinMap
    (hlci : IsLocalCompleteIntersectionMorphism f) (h : GysinMapExists f) {Y' : Scheme.{u}}
    (g : Y' ⟶ Y) [LocallyOfFiniteType g] :
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
    haveI : IsLocallyNoetherian Y' := LocallyOfFiniteType.isLocallyNoetherian (g ≫ sY)
    haveI : IsLocallyNoetherian (pullback f g) :=
      LocallyOfFiniteType.isLocallyNoetherian (pullback.fst f g ≫ sX)
    completedCommutesWithEveryClass C (pullback.fst f g ≫ sX) (g ≫ sY) (pullback.snd f g)
      (pullbackSnd_comp_structureMorphism_eq C sX sY f hf g)
      (completedBivariantRestrictionViaSequence C sX sY f hf g
        (lciGysinMap C sX sY hf hlci h))
Tag 0FF7, a lemma

Tag 0FF7 in the Stacks Project.

Stacks.Chow.lciGysinCap_fundamentalChowClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinFundamentalClass.lean, line 174. The attribute's comment: “δ-equidimensional case: f^![Y']_n = [X']_n' for f = i ≫ g, g smooth, with f^! characterized as i^! ∘ g^* (0FF3, 0FE0) and i^! by 0FBK; g^*[Y'] = [P ×_Y Y'] proved here; carried: 0FEA's regular-sequence step as vanishing excess (so hypothesis (4) is replaced by its consequence), 0FBM's hcone and hinj, 02S1, 02S2, 02RG, 0B71; no clopen reduction”.

The Gysin map of a local complete intersection on a fundamental class, δ-equidimensional case. Let f = i ≫ g with i : X ⟶ P an immersion carrying a virtual normal bundle of constant rank r and g : P ⟶ Y smooth of constant relative dimension d, and let g' : Y' ⟶ Y be a test scheme of δ-dimension at most n. Assume

  • ci satisfies the characterizing relation Stacks.Chow.IsVirtualNormalGysinClass for the virtual normal bundle of i, so that ci is the Gysin class i^! = c(X ⟶ P, 𝒩);
  • cf is the composite ci ∘ g^* in the sense of Stacks.Chow.IsBivariantClassComposition, so that cf is the Gysin map f^! = i^! ∘ g^*; and
  • dim_δ(X ×_Y Y') ≤ n + d - r.

Then f^![Y']_n = [X']_{n - (r + (-d))}.

theorem lciGysinCap_fundamentalChowClass
    (hinj : ∀ {T : Scheme.{u}} (t : T ⟶ P) [LocallyOfFiniteType t] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C sX sN i q hq r NP.flat NP.relativeDimension hdesc t k))
    {ci : BivariantClass C G sX sP i hi (r : ℤ)}
    (hci : IsVirtualNormalGysinClass C G sX sP sN i hi q hq r 0 E
      (bundleFlatPullback C sX sN i q hq r NP.flat NP.relativeDimension hdesc) NP ci)
    {cf : BivariantClass C G sX sY (i ≫ g) (comp_comp_structureMorphism_eq hi hg)
      ((r : ℤ) + -(d : ℤ))}
    (hcf : IsBivariantClassComposition C G sX sP sY i g hi hg hpp (r : ℤ) (-(d : ℤ)) ci
      (flatPullbackBivariantClass C G sP sY g hg d hgd hdesc hRG h71) cf)
    {Y' : Scheme.{u}} (g' : Y' ⟶ Y) [LocallyOfFiniteType g'] (n : ℤ)
    (hY' : schemeDeltaDimension C (g' ≫ sY) ≤ (n : EInt))
    (hX' : schemeDeltaDimension C (pullback.fst i (pullback.fst g g') ≫ sX) ≤
      (((n + (d : ℤ)) - (r : ℤ) : ℤ) : EInt))
    (hcone : chowGroupDegreeEquiv C (pullback.fst (q ≫ i) (pullback.fst g g') ≫ sN)
        (by omega : (n + (d : ℤ)) - (0 : ℤ) = ((n + (d : ℤ)) - (r : ℤ)) + (r : ℤ))
        (E.cap (pullback.fst g g') (n + (d : ℤ))
          (fundamentalChowClass C (pullback.fst g g' ≫ sP) (n + (d : ℤ)))) =
      fundamentalChowClass C (pullback.fst (q ≫ i) (pullback.fst g g') ≫ sN)
        (((n + (d : ℤ)) - (r : ℤ)) + (r : ℤ))) :
    cf.cap g' n (fundamentalChowClass C (g' ≫ sY) n) =
      fundamentalChowClass C (pullback.fst (i ≫ g) g' ≫ sX) (n - ((r : ℤ) + -(d : ℤ)))

Stacks.Chow.completedCapFundamentalClass_completedBivariantRestriction_lciGysinMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinFundamentalCycle.lean, line 536.

Stacks 0FF7. Consider a cartesian square X' = X ×_Y Y' of schemes locally of finite type over the base, with f : X ⟶ Y and its base change f' : X' ⟶ Y'. Assume

  1. f is a local complete intersection morphism for which the Gysin map f^! exists (Stacks 0FF3);
  2. X, X', Y, Y' satisfy the equivalent conditions of Stacks 0FE3, here as decompositions into open and closed pieces of constant δ-dimension;
  3. n_{x'} - n_{y'} = n_x - n_y for every x' ∈ X' with images x ∈ X, y' ∈ Y', y ∈ Y;
  4. 𝒪_{Y', f'(ξ)} is Cohen–Macaulay for every generic point ξ of X'.

Then f^![Y'] = [X'], for the fundamental classes of Stacks 0FE4. Here n_x is the common value of δ at the generic points of the irreducible components through x (Stacks 0FE3); it is constant on connected components, and equals the index of the piece of the decomposition containing the point (Stacks.Chow.relativeDimension_eq_componentDeltaDimension_of_mem_genericPoints), which is why it is written Stacks.Chow.componentDeltaDimension of the connected component of x. The cap product f^![Y'] is that of the restriction res(f^!) of Stacks 0F9Z on the completed groups of Stacks 0FE0 (Stacks.Chow.completedCapFundamentalClass), and both sides are read on the connected components of X', where [X'] is [X'_w]_{n_w} (Stacks.Chow.componentFundamentalClassDirectSum, Stacks.Chow.chowGroupRestrict_fundamentalClass).

The proof is the source's. For a factorization f = g ∘ i with i : X ⟶ P an immersion and g : P ⟶ Y smooth, f^! = i^! ∘ g^* is, on a connected component X_a of X, homogeneous of degree n_{f(X_a)} - n_{X_a}, the relative dimension of g and the rank of the normal sheaf of i being constant on the connected components (Stacks.Chow.SmoothFactorization.exists_hasCapFundamentalFormula_gysinMap); there g^*[T] = [P ×_Y T], the local rings of P ×_Y T are Cohen–Macaulay where needed, and Stacks 0FEA applies to i (Stacks.Chow.BivariantClass.capFundamentalFormula_bivariantCompositeOfInvertible). Restricting to Y' and to the connected components of X' is Stacks.Chow.completedCapFundamentalClass_restriction_of_hasCapFundamentalFormula.

theorem completedCapFundamentalClass_completedBivariantRestriction_lciGysinMap
    (hlci : IsLocalCompleteIntersectionMorphism f) (h : GysinMapExists f) {Y' : Scheme.{u}}
    (g : Y' ⟶ Y) [LocallyOfFiniteType g]
    (hX : HasDimensionDecomposition (relativeDimension C.dimensionFunction sX))
    (hY : HasDimensionDecomposition (relativeDimension C.dimensionFunction sY))
    (hX' : HasDimensionDecomposition
      (relativeDimension C.dimensionFunction (pullback.fst f g ≫ sX)))
    (hY' : HasDimensionDecomposition (relativeDimension C.dimensionFunction (g ≫ sY)))
    (hn : ∀ x : (pullback f g : Scheme.{u}),
      componentDeltaDimension C (pullback.fst f g ≫ sX) hX' (_root_.ConnectedComponents.mk x) -
          componentDeltaDimension C (g ≫ sY) hY'
            (_root_.ConnectedComponents.mk (pullback.snd f g x)) =
        componentDeltaDimension C sX hX (_root_.ConnectedComponents.mk (pullback.fst f g x)) -
          componentDeltaDimension C sY hY
            (_root_.ConnectedComponents.mk (f (pullback.fst f g x))))
    (hCM : haveI : IsLocallyNoetherian Y' := LocallyOfFiniteType.isLocallyNoetherian (g ≫ sY)
      ∀ ξ : (pullback f g : Scheme.{u}), ξ ∈ genericPoints (pullback f g : Scheme.{u}) →
        IsCohenMacaulayLocalRing (Y'.presheaf.stalk (pullback.snd f g ξ))) :
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
    haveI : IsLocallyNoetherian Y' := LocallyOfFiniteType.isLocallyNoetherian (g ≫ sY)
    haveI : IsLocallyNoetherian (pullback f g) :=
      LocallyOfFiniteType.isLocallyNoetherian (pullback.fst f g ≫ sX)
    completedCapFundamentalClass C (gysinSystemOfInvertible C) (pullback.fst f g ≫ sX) (g ≫ sY)
        (pullback.snd f g) (pullbackSnd_comp_structureMorphism_eq C sX sY f hf g) hY'
        (completedBivariantRestrictionViaSequence C sX sY f hf g (lciGysinMap C sX sY hf hlci h)) =
      componentFundamentalClassDirectSum C (pullback.fst f g ≫ sX) hX'
Tag 0FF8, a remark

Tag 0FF8 in the Stacks Project.

Stacks.Chow.bivariantCommute_flatPullbackBivariantClass_chernClassBivariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinChernClasses.lean, line 172. The attribute's comment: “part (a), the flat g^* factor only, in the commuting form of 0FA2: g^* commutes with the bivariant Chern class of 0B7H. res(c_j(E)) = c_j(g^*E) is NOT identified, the i^! factor is 0FBP (absent here), and the Chern character is not stated”.

Stacks 0FF8 (a), for the flat factor of the factorization. The flat-pullback bivariant class of Stacks 0B78 attached to a smooth morphism g : P ⟶ Y of relative dimension d commutes, in the sense of Stacks 0FA2, with the bivariant j-th Chern class c_j(ℰ) ∈ A^j(Y ⟶ Y) of Stacks 0B7H.

Stacks 0FF8 (a) asserts f^! ∘ c_j(ℰ) = c_j(f^*ℰ) ∘ f^! for the Gysin map of a local complete intersection morphism f = i ≫ g, citing Stacks 0FF6. Stacks 0FF6 is proved in the source by treating the two factors of the factorization separately, and its carrier in this repository, Stacks.Chow.bivariantCommute_flatPullbackBivariantClass, is the g^* factor. This is that carrier instantiated at the bivariant Chern class, which is the assembly Stacks 0FF8 performs. The i^! factor is Stacks 0FBP and has no carrier here; see the implementation notes.

Two further caveats on what this is. First, the statement is the commuting form of Stacks 0FA2 rather than the displayed composition f^! ∘ c_j(ℰ) = c_j(f^*ℰ) ∘ f^!; the two are equivalent by Stacks.Chow.bivariantCommute_iff_cap_eq_of_isBivariantClassComposition, but rewriting res(c_j(ℰ)) as the bivariant Chern class of g^*ℰ is a separate identification, which needs the pseudofunctoriality of pullback of modules against Stacks.Chow.HigherChernCapRule and is not carried out here. Second, the Chern character is not stated.

theorem bivariantCommute_flatPullbackBivariantClass_chernClassBivariant :
    BivariantCommute C G sY g (𝟙 Y) (-(d : ℤ)) (j : ℤ)
      (flatPullbackBivariantClass C G (g ≫ sY) sY g rfl d hgd hdesc hRG h71)
      (chernClassBivariantOverIdComp C sY E r G cap j hproper hflat hgysin hiso)

Stacks.Chow.lciGysinCap_fundamentalChowClass_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinChernClasses.lean, line 219. The attribute's comment: “part (b): f^![Y]_n = [X]_{n-(r-d)} on X itself, from 0FF7 at Y' = Y. The 0FE3 conditions enter as the two δ-dimension bounds and the Cohen-Macaulay hypothesis as the vanishing excess hcone, exactly as in 0FF7's carrier; no clopen reduction”.

Stacks 0FF8 (b). Let f = i ≫ g with i : X ⟶ P an immersion carrying a virtual normal bundle of constant rank r and g : P ⟶ Y smooth of constant relative dimension d, so that the Gysin map exists for f in the sense of Stacks 0FF3, and let f^! be the Gysin map, entering as a bivariant class cf characterized as i^! ∘ g^*. If dim_δ(Y) ≤ n and dim_δ(X ×_P (P ×_Y Y)) ≤ n + d - r, then

f^![Y]_n = [X]_{n - (r - d)}

in the Chow group of X itself.

This is Stacks.Chow.lciGysinCap_fundamentalChowClass, the δ-equidimensional case of Stacks 0FF7, at the test scheme g' = 𝟙 Y, followed by the identification of X ×_Y Y with X: the projection pullback.fst f (𝟙 Y) is an isomorphism, and pushforward along an isomorphism over the base carries a fundamental class to a fundamental class by Stacks.Chow.chowPushforwardOfIso_fundamentalChowClass.

The hypotheses are those of Stacks.Chow.lciGysinCap_fundamentalChowClass, whose implementation notes say what each one is and why none of them is the conclusion; see also the implementation notes above for how the Cohen-Macaulay hypothesis and the conditions of Stacks 0FE3 enter.

theorem lciGysinCap_fundamentalChowClass_id
    (hinj : ∀ {T : Scheme.{u}} (t : T ⟶ P) [LocallyOfFiniteType t] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C sX sN i q hq r NP.flat NP.relativeDimension hdesc t k))
    {ci : BivariantClass C G sX sP i hi (r : ℤ)}
    (hci : IsVirtualNormalGysinClass C G sX sP sN i hi q hq r 0 EC
      (bundleFlatPullback C sX sN i q hq r NP.flat NP.relativeDimension hdesc) NP ci)
    {cf : BivariantClass C G sX sY (i ≫ g) (comp_comp_structureMorphism_eq hi hg)
      ((r : ℤ) + -(d : ℤ))}
    (hcf : IsBivariantClassComposition C G sX sP sY i g hi hg hpp (r : ℤ) (-(d : ℤ)) ci
      (flatPullbackBivariantClass C G sP sY g hg d hgd hdesc hRG h71) cf)
    (n : ℤ) (hY : schemeDeltaDimension C (𝟙 Y ≫ sY) ≤ (n : EInt))
    (hX : schemeDeltaDimension C (pullback.fst i (pullback.fst g (𝟙 Y)) ≫ sX) ≤
      (((n + (d : ℤ)) - (r : ℤ) : ℤ) : EInt))
    (hcone : chowGroupDegreeEquiv C (pullback.fst (q ≫ i) (pullback.fst g (𝟙 Y)) ≫ sN)
        (by omega : (n + (d : ℤ)) - (0 : ℤ) = ((n + (d : ℤ)) - (r : ℤ)) + (r : ℤ))
        (EC.cap (pullback.fst g (𝟙 Y)) (n + (d : ℤ))
          (fundamentalChowClass C (pullback.fst g (𝟙 Y) ≫ sP) (n + (d : ℤ)))) =
      fundamentalChowClass C (pullback.fst (q ≫ i) (pullback.fst g (𝟙 Y)) ≫ sN)
        (((n + (d : ℤ)) - (r : ℤ)) + (r : ℤ))) :
    chowPushforwardOfIso C (pullback.fst (i ≫ g) (𝟙 Y) ≫ sX) sX
        (pullback.fst (i ≫ g) (𝟙 Y)) rfl (n - ((r : ℤ) + -(d : ℤ)))
        (cf.cap (𝟙 Y) n
          (chowGroupCongr C (Category.id_comp sY).symm n (fundamentalChowClass C sY n))) =
      fundamentalChowClass C sX (n - ((r : ℤ) + -(d : ℤ)))

Stacks.Chow.flatPullbackChow_chernCap_fundamentalChowClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinChernClasses.lean, line 290. The attribute's comment: “part (c), the flat g^* factor only: h^*(c_j(t^*E) ∩ [T]_n) = c_j((h ≫ t)^*E) ∩ [T']_{n+m} for h flat of relative dimension m — the Gysin map of a smooth h — from 02U8 (carried, as hflat) and 02RB. The lci f^! needs 0FBP, which is proved only with its own hypotheses carried — Stacks.Chow.virtualNormalGysinClass_bivariantCommute of Chow/Bivariant/VirtualNormalCommuting.lean assumes the 0FBL/0FBN factorization, the centrality of Stacks 02UA and the commutation of the second factor, and the reduction of 02UC and 02OS to a divisor is not carried out — so it is not usable here; no Chern character”.

Stacks 0FF8 (c), for the flat factor of the factorization. Let ℰ be finite locally free of rank r on Y, let t : T ⟶ Y be a test scheme with dim_δ(T) ≤ n, and let h : T' ⟶ T be flat of constant relative dimension m. Then

h^*(c_j(t^*ℰ) ∩ [T]_n) = c_j((h ≫ t)^*ℰ) ∩ [T']_{n+m},

the two sides sitting in the degrees (n - j) + m and (n + m) - j, which are the same integer written two ways.

This is Stacks 0FF8 (c) for the g^* factor of the factorization f = i ≫ g. For a smooth h the Gysin map of Stacks 0FF3 is flat pullback, by the factorization with i = 𝟙, so the display above is then literally h^!(c_j(ℰ) ∩ [T]) = c_j(h^*ℰ) ∩ [T']; the statement is proved in the flat generality that its two inputs support, which is the generality in which StacksFrontier.AlgebraicGeometry.Chow.Bivariant.FlatPullbackCommuting carries Stacks 0FF6. Those inputs are: part (b) for the factor, h^*[T]_n = [T']_{n+m}, which is Stacks 02RB on Chow groups, Stacks.Chow.flatPullbackChow_fundamentalChowClass; and part (a) for the factor, the commutation of the Chern class operations with flat pullback, Stacks 02U8, which is the hypothesis hflat carried here, exactly as Stacks.Chow.chernClassBivariant carries it. The lci case needs Stacks 0FBP; see the implementation notes. The Chern character is not stated.

Stacks.Chow.chernIdentityCapRule C sY E r cap hrank j is the rule α ↦ c_j(u^*ℰ) ∩ α on the Chow groups of each test scheme u : U ⟶ Y; it unfolds to cap (u ≫ sY) ((Scheme.Modules.pullback u).obj E) k j.

theorem flatPullbackChow_chernCap_fundamentalChowClass
    (hflat : IdentityCapRule.FlatNaturality C sY (j : ℤ)
      (chernIdentityCapRule C sY E r cap hrank j))
    {T T' : Scheme.{u}} (t : T ⟶ Y) [LocallyOfFiniteType t] (h : T' ⟶ T)
    [LocallyOfFiniteType h] [AlgebraicGeometry.Flat h] (m : ℕ)
    (hm : AlgebraicGeometry.RelativeDimension h m) (n : ℤ)
    (hdim : schemeDeltaDimension C (t ≫ sY) ≤ (n : EInt))
    (hfac : FlatPullbackFactorsThroughRationalEquivalence C ((h ≫ t) ≫ sY) (t ≫ sY) h
      (by simp [Category.assoc]) m hm n)
    (hfacj : FlatPullbackFactorsThroughRationalEquivalence C ((h ≫ t) ≫ sY) (t ≫ sY) h
      (by simp [Category.assoc]) m hm (n - (j : ℤ))) :
    chernIdentityCapRule C sY E r cap hrank j (h ≫ t) (n + (m : ℤ))
        (fundamentalChowClass C ((h ≫ t) ≫ sY) (n + (m : ℤ))) ≍
      flatPullbackChow C ((h ≫ t) ≫ sY) (t ≫ sY) h (by simp [Category.assoc]) m hm
        (n - (j : ℤ)) hfacj
        (chernIdentityCapRule C sY E r cap hrank j t n (fundamentalChowClass C (t ≫ sY) n))

Stacks.Chow.lciGysinClass_comp_chernClassOfModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinChernCommuting.lean, line 286. The attribute's comment: “first assertion: f^! ∘ c_i(E) = c_i(f^E) ∘ f^! for the Gysin map f^! of 0FF3 (lciGysinClass) and E finite locally free of any rank (c_i of 0ESW), stated in every graded part (f^!)_q of f^! in A^(X → Y)^∧; the right side is c_i(f^*E) itself, not res(c_i(E))”.

Stacks 0FF8, the Chern classes. Let f : X ⟶ Y be a local complete intersection morphism of schemes locally of finite type over S for which the Gysin map exists, with f^! the Gysin map of Stacks 0FF3 built from a factorization F of f, and let ℰ be a finite locally free 𝒪_Y-module of arbitrary rank. Then

f^! ∘ c_i(ℰ) = c_i(f^*ℰ) ∘ f^!,

stated, as an identity in the completed group A^*(X ⟶ Y)^∧ of Stacks 0FE0 is, degree by degree: for every q, (f^!)_q ∘ c_i(ℰ) = c_i(f^*ℰ) ∘ (f^!)_q in A^{q+i}(X ⟶ Y). The Chern classes are those of Stacks 0ESW.

theorem lciGysinClass_comp_chernClassOfModule (E : Y.Modules)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E] (i : ℕ) (q : ℤ) :
    haveI := isFiniteLocallyFree_pullback_of_isFiniteLocallyFree f E
    (lciGysinClassComponent C sX sY f hfs hf F q).comp
        (BivariantChowClass.equivBivariantClass.symm (chernClassOfModule C sY E i)) =
      (((BivariantChowClass.equivBivariantClass.symm
          (chernClassOfModule C sX ((Scheme.Modules.pullback f).obj E) i)).comp
            (lciGysinClassComponent C sX sY f hfs hf F q)).degreeCongr
        (add_comm (i : ℤ) q)).transport (comp_comp_structureMorphism_eq hfs (Category.id_comp sY))
        (Iso.refl X) (by simp)

Stacks.Chow.lciGysinClass_comp_chernCharacterOfModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinChernCommuting.lean, line 310. The attribute's comment: “first assertion, for the Chern character: f^! ∘ ch(E) = ch(f^E) ∘ f^! in A^(X → Y) ⊗ Q, stated for every graded part (f^!)_q of the Gysin map of 0FF3 and every component ch_p(E) = P_p(E)/p! of the Chern character of 0ESX, E finite locally free of any rank”.

Stacks 0FF8, the Chern character. In the situation of Stacks.Chow.lciGysinClass_comp_chernClassOfModule,

f^! ∘ ch(ℰ) = ch(f^*ℰ) ∘ f^!,

stated degree by degree: for every q and every p, (f^!)_q ∘ ch_p(ℰ) = ch_p(f^*ℰ) ∘ (f^!)_q in A^{q+p}(X ⟶ Y) ⊗ 𝐐, with ch_p(ℰ) = P_p(ℰ)/p! the Chern character of Stacks 0ESX (Stacks.Chow.chernCharacterOfModule) and the composites with a rational class the rational extensions of those of Stacks 0B75.

theorem lciGysinClass_comp_chernCharacterOfModule (E : Y.Modules)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E] (p : ℕ) (q : ℤ) :
    haveI := isFiniteLocallyFree_pullback_of_isFiniteLocallyFree f E
    LinearMap.lTensor ℚ ((lciGysinClassComponent C sX sY f hfs hf F q).compRightHom f hfs
        (p : ℤ)).toIntLinearMap (chernCharacterOfModule C sY E p) =
      LinearMap.lTensor ℚ ((lciGysinClassComponent C sX sY f hfs hf F q).compLeftHom f hfs
        (p : ℤ)).toIntLinearMap
        (chernCharacterOfModule C sX ((Scheme.Modules.pullback f).obj E) p)

Stacks.Chow.lciGysinClass_completedCap_chernClassOfModule_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinChernFundamentalClass.lean, line 325. The attribute's comment: “third assertion: f^!(c_i(E) ∩ [Y]) = c_i(f^*E) ∩ [X] for the Gysin map of Tag 0FF3, E finite locally free of any rank (c_i of Tag 0ESW), read on the connected components of X in every degree; only the Tag 0FE3 condition on Y is assumed”.

Stacks 0FF8, f^!(c_i(ℰ) ∩ [Y]) = c_i(f^*ℰ) ∩ [X]. Let f : X ⟶ Y be a local complete intersection morphism of schemes locally of finite type over S with Gysin map f^! of Stacks 0FF3 (built from a factorization F), let Y satisfy the equivalent conditions of Stacks 0FE3, and let ℰ be a finite locally free 𝒪_Y-module of any rank, with Chern classes c_i of Stacks 0ESW. Then

f^!(c_i(ℰ) ∩ [Y]) = c_i(f^*ℰ) ∩ [X],

the classes read on the connected components X_k of X (which determine a class on X, CH_n(X) = ∏_k CH_n(X_k)), in every degree n: c_i(ℰ) ∩ [Y] is the family (c_i(ℰ) ∩ [Y_j]_{m+i})_{j,m} (Stacks.Chow.componentClassCap), f^! acts on it by Stacks.Chow.completedCap, and [X] is read as the family of fundamental classes [X_k].

The source assumes X and Y satisfy the conditions of Stacks 0FE3, for example Y Cohen–Macaulay; only the condition on Y is used.

theorem lciGysinClass_completedCap_chernClassOfModule_cap
    (hY : HasDimensionDecomposition (relativeDimension C.dimensionFunction sY)) (i : ℕ)
    (k : _root_.ConnectedComponents X) (n : ℤ) :
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI := LocallyOfFiniteType.isLocallyNoetherian sY
    haveI := isFiniteLocallyFree_pullback_of_isFiniteLocallyFree f E
    completedCap C sX sY f hfs (lciGysinClass C sX sY f hfs hf F)
        (componentClassCap C sY i (chernClassOfModule C sY E i) (componentFundamentalClass C sY))
        k n =
      componentClassCap C sX i (chernClassOfModule C sX ((Scheme.Modules.pullback f).obj E) i)
        (componentFundamentalClass C sX) k n

Stacks.Chow.lciGysinClass_completedCap_chernCharacterOfModule_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinChernFundamentalClass.lean, line 362. The attribute's comment: “third assertion, for the Chern character: f^!(ch(E) ∩ [Y]) = ch(f^E) ∩ [X] in CH_(X) ⊗ Q, for every component ch_p(E) = P_p(E)/p! of Tag 0ESX, read on the connected components of X; only the Tag 0FE3 condition on Y is assumed”.

Stacks 0FF8, f^!(ch(ℰ) ∩ [Y]) = ch(f^*ℰ) ∩ [X]. In the situation of Stacks.Chow.lciGysinClass_completedCap_chernClassOfModule_cap, for every p,

f^!(ch_p(ℰ) ∩ [Y]) = ch_p(f^*ℰ) ∩ [X] in CH_*(X) ⊗ 𝐐,

with ch_p(ℰ) = P_p(ℰ)/p! the Chern character of Stacks 0ESX (Stacks.Chow.chernCharacterOfModule), the cap products of rational classes the rational extensions of the integral ones, and the classes read on the connected components as in the Chern class statement.

theorem lciGysinClass_completedCap_chernCharacterOfModule_cap
    (hY : HasDimensionDecomposition (relativeDimension C.dimensionFunction sY)) (p : ℕ) :
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI := LocallyOfFiniteType.isLocallyNoetherian sY
    haveI := isFiniteLocallyFree_pullback_of_isFiniteLocallyFree f E
    LinearMap.lTensor ℚ
        (completedCapHom C sX sY f hfs (lciGysinClass C sX sY f hfs hf F)).toIntLinearMap
        (LinearMap.lTensor ℚ
          (componentClassCapHom C sY p (componentFundamentalClass C sY)).toIntLinearMap
          (chernCharacterOfModule C sY E p)) =
      LinearMap.lTensor ℚ
        (componentClassCapHom C sX p (componentFundamentalClass C sX)).toIntLinearMap
        (chernCharacterOfModule C sX ((Scheme.Modules.pullback f).obj E) p)

Stacks.Chow.lciGysinCap_fundamentalChowClass_id_of_isVirtualNormalBundleClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinCompositeFundamentalClass.lean, line 237. The attribute's comment: “part (b): f^![Y]_n = [X]_{n-(r-d)} on X itself, from 0FF7 at Y' = Y. The 0FE3 conditions enter as the two δ-dimension bounds and the Cohen-Macaulay hypothesis as the vanishing excess hcone, exactly as in 0FF7's carrier; no clopen reduction”.

Stacks 0FF8 (b). Let f = i ≫ g with i : X ⟶ P an immersion carrying a virtual normal bundle of constant rank r and g : P ⟶ Y smooth of constant relative dimension d, so that the Gysin map exists for f in the sense of Stacks 0FF3, and let f^! be the Gysin map, entering as a bivariant class cf characterized as i^! ∘ g^*. If dim_δ(Y) ≤ n and dim_δ(X ×_P (P ×_Y Y)) ≤ n + d - r, then

f^![Y]_n = [X]_{n - (r - d)}

in the Chow group of X itself.

This is Stacks.Chow.lciGysinCap_fundamentalChowClass_of_isVirtualNormalBundleClass — a special case of Stacks 0FF7 for a class cf characterized as i^! ∘ g^*, with constant ranks and the excess vanishing as the hypothesis hcone; the full Stacks 0FF7, for the constructed Gysin map Stacks.Chow.lciGysinMap, is Stacks.Chow.completedCapFundamentalClass_completedBivariantRestriction_lciGysinMap — at the test scheme g' = 𝟙 Y, followed by the identification of X ×_Y Y with X: the projection pullback.fst f (𝟙 Y) is an isomorphism, and pushforward along an isomorphism over the base carries a fundamental class to a fundamental class by Stacks.Chow.chowPushforwardOfIso_fundamentalChowClass.

The hypotheses are those of Stacks.Chow.lciGysinCap_fundamentalChowClass_of_isVirtualNormalBundleClass, whose implementation notes say what each one is and why none of them is the conclusion; see also the implementation notes above for how the Cohen-Macaulay hypothesis and the conditions of Stacks 0FE3 enter.

theorem lciGysinCap_fundamentalChowClass_id_of_isVirtualNormalBundleClass
    {ci : BivariantClass C G sX sP i hi (r : ℤ)}
    (hci : IsVirtualNormalBundleClass C sX sP i hi G 𝒩 r ci)
    {cf : BivariantClass C G sX sY (i ≫ g) (comp_comp_structureMorphism_eq hi hg)
      ((r : ℤ) + -(d : ℤ))}
    (hcf : IsBivariantClassComposition C G sX sP sY i g hi hg hpp (r : ℤ) (-(d : ℤ)) ci
      cg cf)
    (n : ℤ) (hY : schemeDeltaDimension C (𝟙 Y ≫ sY) ≤ (n : EInt))
    (hX : schemeDeltaDimension C (pullback.fst i (pullback.fst g (𝟙 Y)) ≫ sX) ≤
      (((n + (d : ℤ)) - (r : ℤ) : ℤ) : EInt))
    (hcone : chowGroupDegreeEquiv C
        (pullback.fst (𝒩.projection ≫ i) (pullback.fst g (𝟙 Y)) ≫ 𝒩.projection ≫ sX)
        (by omega : (n + (d : ℤ)) - (0 : ℤ) = ((n + (d : ℤ)) - (r : ℤ)) + (r : ℤ))
        ((virtualNormalConeClass C sX sP i hi 𝒩).cap (pullback.fst g (𝟙 Y)) (n + (d : ℤ))
          (fundamentalChowClass C (pullback.fst g (𝟙 Y) ≫ sP) (n + (d : ℤ)))) =
      fundamentalChowClass C
        (pullback.fst (𝒩.projection ≫ i) (pullback.fst g (𝟙 Y)) ≫ 𝒩.projection ≫ sX)
        (((n + (d : ℤ)) - (r : ℤ)) + (r : ℤ))) :
    chowPushforwardOfIso C (pullback.fst (i ≫ g) (𝟙 Y) ≫ sX) sX
        (pullback.fst (i ≫ g) (𝟙 Y)) rfl (n - ((r : ℤ) + -(d : ℤ)))
        (cf.cap (𝟙 Y) n
          (chowGroupCongr C (Category.id_comp sY).symm n (fundamentalChowClass C sY n))) =
      fundamentalChowClass C sX (n - ((r : ℤ) + -(d : ℤ)))

Stacks.Chow.lciGysinClass_completedCapDegreeZero_fundamentalClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/LciGysinFundamentalClassFormula.lean, line 124. The attribute's comment: “second assertion: f^![Y] = [X] in CH^0(X) for X and Y satisfying the conditions of Tag 0FE3, with [X], [Y] the fundamental classes of Tag 0FE4 and f^! the Gysin map of Tag 0FF3; the source's example hypothesis that Y is Cohen-Macaulay is not needed”.

Stacks 0FF8 (b), f^![Y] = [X]. Let f : X ⟶ Y be a local complete intersection morphism of schemes locally of finite type over S with Gysin map f^! ∈ A^*(X ⟶ Y)^∧ of Stacks 0FF3 (built from a factorization F), and let X and Y satisfy the equivalent conditions of Stacks 0FE3. Then

f^![Y] = [X] in CH^0(X) = ∏_n CH_n(X_n),

with [X] = ∑_n [X_n]_n and [Y] the fundamental classes of Stacks 0FE4 and f^! ∩ - the cap product of the completed class on CH^0 (Stacks.Chow.completedCapDegreeZero).

The source adds "for example if Y is Cohen–Macaulay"; that is only a sufficient condition for the hypothesis of Stacks 0FE3 on Y, which is all that is assumed here. The hypothesis on X enters only to write [X] as an element of CH^0(X): the identity of the classes on the connected components, Stacks.Chow.lciGysinClass_completedCap_componentFundamentalClass, needs the hypothesis on Y alone.

theorem lciGysinClass_completedCapDegreeZero_fundamentalClass
    (hX : HasDimensionDecomposition (relativeDimension C.dimensionFunction sX))
    (hY : HasDimensionDecomposition (relativeDimension C.dimensionFunction sY)) :
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI := LocallyOfFiniteType.isLocallyNoetherian sY
    completedCapDegreeZero C sX hX sY f hfs hY (lciGysinClass C sX sY f hfs hf F)
        (fundamentalClass C sY hY) =
      fundamentalClass C sX hX
Tag 0FV9, a lemma

Tag 0FV9 in the Stacks Project.

Stacks.Chow.completedBivariantTransport_completedBivariantRestriction_lciGysinMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/BaseChangeExcessFormula.lean, line 193. The attribute's comment: “the whole lemma: for a cartesian square of schemes locally of finite type over S with f, f' local complete intersection morphisms and the Gysin map existing for f, the kernel C of H^{-1}((g')^NL_{X/Y}) → H^{-1}(NL_{X'/Y'}) is finite locally free, the Gysin map exists for f', and res(f^!) = c_top(C^∨) ∘ (f')^! in A^(X' → Y')^∧”.

Let g' ≫ f = f' ≫ g be a cartesian square of schemes locally of finite type over the base, with f and f' local complete intersection morphisms and the Gysin map of Stacks 0FF3 existing for f. Then the sheaf

𝒞 = Ker(H^{-1}((g')^*NL_{X/Y}) ⟶ H^{-1}(NL_{X'/Y'})),

for the base change map of Stacks 0FV5, is a finite locally free 𝒪_{X'}-module, the Gysin map exists for f', and

res(f^!) = c_top(𝒞^∨) ∘ (f')^! in A^*(X' ⟶ Y')^∧,

for the Gysin maps of Stacks 0FF3, the restriction of Stacks 0F9Z (carried from the chosen fibre product X ×_Y Y' to X' along the canonical isomorphism), the top Chern class of Stacks 0FA4 and the composition of Stacks 0FE0 (a class for 𝟙 ≫ f').

theorem completedBivariantTransport_completedBivariantRestriction_lciGysinMap
    (hlf : IsLocalCompleteIntersectionMorphism f) (hlf' : IsLocalCompleteIntersectionMorphism f')
    (hG : GysinMapExists f) :
    ∃ hC : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (kernel (HomologicalComplex.homologyMap
          (Stacks.NaiveCotangentFlatBaseChange.baseChangeMapOfComparison f f' g'
            (AlgebraicGeometry.BaseChangeStalk.baseRingComparison f f' g' g hsq.w)
            (AlgebraicGeometry.BaseChangeStalk.baseRingComparison_comp f f' g' g hsq.w)) (-1))),
      ∃ hG' : GysinMapExists f',
        haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
        haveI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
        haveI : IsLocallyNoetherian X' := LocallyOfFiniteType.isLocallyNoetherian sX'
        haveI : IsLocallyNoetherian Y' := LocallyOfFiniteType.isLocallyNoetherian (g ≫ sY)
        haveI : IsLocallyNoetherian (pullback f g) :=
          LocallyOfFiniteType.isLocallyNoetherian (pullback.fst f g ≫ sX)
        haveI : SheafOfModules.IsFiniteLocallyFree.{u, u, u} (dualSheaf (kernel
            (HomologicalComplex.homologyMap
              (Stacks.NaiveCotangentFlatBaseChange.baseChangeMapOfComparison f f' g'
                (AlgebraicGeometry.BaseChangeStalk.baseRingComparison f f' g' g hsq.w)
                (AlgebraicGeometry.BaseChangeStalk.baseRingComparison_comp f f' g' g hsq.w))
              (-1)))) :=
          isFiniteLocallyFree_dualSheaf_of_schemeOpens _ hC
        completedBivariantTransport C (pullback.fst f g ≫ sX) sX' (g ≫ sY) (pullback.snd f g)
            (pullbackSnd_comp_structureMorphism_eq C sX sY f hf g) f' hf' hsq.isoPullback.symm
            hsq.isoPullback_inv_snd
            (completedBivariantRestrictionViaSequence C sX sY f hf g
              (lciGysinMap C sX sY hf hlf hG)) =
          completedBivariantGroup.copy C (Category.id_comp f') _ hf'
            (completedBivariantCompositeOfInvertible C sX' sX' (g ≫ sY) (𝟙 X') f'
              (Category.id_comp sX') hf'
              (topChernClassOfInvertible C sX' (dualSheaf (kernel (HomologicalComplex.homologyMap
                (Stacks.NaiveCotangentFlatBaseChange.baseChangeMapOfComparison f f' g'
                  (AlgebraicGeometry.BaseChangeStalk.baseRingComparison f f' g' g hsq.w)
                  (AlgebraicGeometry.BaseChangeStalk.baseRingComparison_comp f f' g' g hsq.w))
                (-1)))))
              (lciGysinMap C sX' (g ≫ sY) hf' hlf' hG'))
Tag 0FVA, a lemma

Tag 0FVA in the Stacks Project.

Stacks.Chow.completedBivariantRestriction_lciGysinMap_blowUpToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/BlowupFormula.lean, line 90. The attribute's comment: “the whole lemma: for a regular closed immersion i : Z → X of schemes locally of finite type over S, the blowing up b : X' → X with centre Z, E = X' ×_X Z with π : E → Z, and the Gysin map existing for b, res(b^!) = c_top(F^∨) ∘ π^ in A^(E → Z)^∧, F the kernel of π^*C_{Z/X} → C_{E/X'}”.

The blow up formula. Let i : Z ⟶ X be a regular closed immersion of schemes locally of finite type over the base, b : X' ⟶ X the blowing up of X with centre Z, and E = X' ×_X Z with j : E ⟶ X' and π : E ⟶ Z. Assume that the Gysin map of Stacks 0FF3 exists for b (a local complete intersection morphism, Stacks 0BIQ). Then

res(b^!) = c_top(𝓕^∨) ∘ π^* in A^*(E ⟶ Z)^∧,

where 𝓕 is the kernel of the canonical map π^*𝒞_{Z/X} ⟶ 𝒞_{E/X'} (finite locally free, Stacks.Chow.isFiniteLocallyFree_blowupExcessConormal), res is the restriction of Stacks 0F9Z along i, c_top the top Chern class of Stacks 0FA4, π^* the flat pullback of the smooth morphism π and the composition that of Stacks 0FE0 (a class for 𝟙 ≫ π).

theorem completedBivariantRestriction_lciGysinMap_blowUpToBase (hi : IsRegularImmersion i)
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (hG : GysinMapExists (Stacks.Blowup.blowUpToBase i.ker)) :
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI := Stacks.Blowup.smooth_pullbackSnd_blowUpToBase i hi
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian (i ≫ sX)
    haveI : IsLocallyNoetherian (Stacks.Blowup.blowUp i.ker) :=
      LocallyOfFiniteType.isLocallyNoetherian (Stacks.Blowup.blowUpToBase i.ker ≫ sX)
    haveI : IsLocallyNoetherian (pullback (Stacks.Blowup.blowUpToBase i.ker) i) :=
      LocallyOfFiniteType.isLocallyNoetherian (pullback.fst (Stacks.Blowup.blowUpToBase i.ker) i ≫
        Stacks.Blowup.blowUpToBase i.ker ≫ sX)
    haveI : SheafOfModules.IsFiniteLocallyFree.{u, u, u} (blowupExcessConormal i) :=
      isFiniteLocallyFree_blowupExcessConormal i hi hG
    haveI : SheafOfModules.IsFiniteLocallyFree.{u, u, u} (dualSheaf (blowupExcessConormal i)) :=
      isFiniteLocallyFree_dualSheaf_of_schemeOpens _ inferInstance
    completedBivariantRestrictionViaSequence C (Stacks.Blowup.blowUpToBase i.ker ≫ sX) sX
        (Stacks.Blowup.blowUpToBase i.ker) rfl i
        (lciGysinMap C (Stacks.Blowup.blowUpToBase i.ker ≫ sX) sX rfl
          (Stacks.Blowup.isLocalCompleteIntersectionMorphism_blowUpToBase i hi) hG) =
      completedBivariantGroup.copy C (Category.id_comp (pullback.snd _ i)) _
        (pullbackSnd_comp_structureMorphism_eq C _ sX _ rfl i)
        (completedBivariantCompositeOfInvertible C
          (pullback.fst (Stacks.Blowup.blowUpToBase i.ker) i ≫
            Stacks.Blowup.blowUpToBase i.ker ≫ sX)
          (pullback.fst (Stacks.Blowup.blowUpToBase i.ker) i ≫
            Stacks.Blowup.blowUpToBase i.ker ≫ sX)
          (i ≫ sX) (𝟙 _) (pullback.snd (Stacks.Blowup.blowUpToBase i.ker) i) (Category.id_comp _)
          (pullbackSnd_comp_structureMorphism_eq C _ sX _ rfl i)
          (topChernClassOfInvertible C _ (dualSheaf (blowupExcessConormal i)))
          (completedFlatPullbackOfSmooth C _ (i ≫ sX)
            (pullback.snd (Stacks.Blowup.blowUpToBase i.ker) i)
            (pullbackSnd_comp_structureMorphism_eq C _ sX _ rfl i)))
Tag 0FF9, a lemma

Tag 0FF9 in the Stacks Project.

Stacks.Chow.isLocalCompleteIntersectionMorphism_and_lciGysinRational_rationalIntersectionProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionProduct.lean, line 513. The attribute's comment: “the whole lemma: for f : X → Y over S with X, Y quasi-compact, regular, of finite dimension, with affine diagonal, f is a local complete intersection morphism, and if the Gysin map of f exists then f^!(α · β) = f^!α · f^!β for the products of 0FEX on CH^(-) ⊗ Q = CH_(-) ⊗ Q”.

Stacks Project, Tag 0FF9. Let (S, δ) be as in Situation 42.7.1 and let f : X ⟶ Y be a morphism of schemes locally of finite type over S such that both X and Y are quasi-compact, regular, have affine diagonal, and finite dimension. Then f is a local complete intersection morphism, and if moreover the Gysin map exists for f, then

f^!(α · β) = f^!α · f^!β

for the intersection products of Section 0FEX, on CH^*(-) ⊗ 𝐐 = CH_*(-) ⊗ 𝐐.

theorem isLocalCompleteIntersectionMorphism_and_lciGysinRational_rationalIntersectionProduct
    [CompactSpace X] [CompactSpace Y] (hXreg : IsRegular X) (hYreg : IsRegular Y)
    (hXdim : topologicalKrullDim X ≠ ⊤) (hYdim : topologicalKrullDim Y ≠ ⊤) :
    IsLocalCompleteIntersectionMorphism f ∧
      ∀ (h : GysinMapExists f) (α β : DirectSum ℤ fun j : ℤ => ℚ ⊗[ℤ] chowGroup C sY j),
        haveI := isNoetherian_of_compactSpace sX
        haveI := isNoetherian_of_compactSpace sY
        haveI := locallyOfFiniteType_of_comp_eq hf
        lciGysinRational C sX sY hf
            (isLocalCompleteIntersectionMorphism_of_comp_eq_of_isRegular hf hXreg hYreg) h
            (rationalIntersectionProduct hYreg (exists_bounds_relativeDimension C sY hYdim) α β) =
          rationalIntersectionProduct hXreg (exists_bounds_relativeDimension C sX hXdim)
            (lciGysinRational C sX sY hf
              (isLocalCompleteIntersectionMorphism_of_comp_eq_of_isRegular hf hXreg hYreg) h α)
            (lciGysinRational C sX sY hf
              (isLocalCompleteIntersectionMorphism_of_comp_eq_of_isRegular hf hXreg hYreg) h
              β)
Tag 0FFA, a lemma

Tag 0FFA in the Stacks Project.

Stacks.Chow.isLocalCompleteIntersectionMorphism_and_projectionFormula_rationalIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionProduct.lean, line 581. The attribute's comment: “the whole lemma: for f : X → Y over S with X, Y quasi-compact, regular, of finite dimension, with affine diagonal, f is a local complete intersection morphism, and if the Gysin map of f exists and f is proper then f_(α · f^!β) = f_α · β for the products of 0FEX on CH^(-) ⊗ Q = CH_(-) ⊗ Q”.

Stacks Project, Tag 0FFA. Let (S, δ) be as in Situation 42.7.1 and let f : X ⟶ Y be a morphism of schemes locally of finite type over S such that both X and Y are quasi-compact, regular, have affine diagonal, and finite dimension. Then f is a local complete intersection morphism, and if moreover the Gysin map exists for f and f is proper, then

f_*(α · f^!β) = f_*α · β

for the intersection products of Section 0FEX, on CH^*(-) ⊗ 𝐐 = CH_*(-) ⊗ 𝐐.

theorem isLocalCompleteIntersectionMorphism_and_projectionFormula_rationalIntersection
    [CompactSpace X] [CompactSpace Y] (hXreg : IsRegular X) (hYreg : IsRegular Y)
    (hXdim : topologicalKrullDim X ≠ ⊤) (hYdim : topologicalKrullDim Y ≠ ⊤) :
    IsLocalCompleteIntersectionMorphism f ∧
      ∀ [IsProper f] (h : GysinMapExists f)
        (α : DirectSum ℤ fun j : ℤ => ℚ ⊗[ℤ] chowGroup C sX j)
        (β : DirectSum ℤ fun j : ℤ => ℚ ⊗[ℤ] chowGroup C sY j),
        haveI := isNoetherian_of_compactSpace sX
        haveI := isNoetherian_of_compactSpace sY
        rationalProperChowPushforward C sX sY hf
            (rationalIntersectionProduct hXreg (exists_bounds_relativeDimension C sX hXdim) α
              (lciGysinRational C sX sY hf
                (isLocalCompleteIntersectionMorphism_of_comp_eq_of_isRegular hf hXreg hYreg) h
                β)) =
          rationalIntersectionProduct hYreg (exists_bounds_relativeDimension C sY hYdim)
            (rationalProperChowPushforward C sX sY hf α) β
Sources
LeanStacks.Chow.ConormalCompatibleVirtualNormalBundles.ofIsRegularImmersion · Stacks.Chow.localizedChernClass_cap_eq_bivariantCompositeCap_of_isRegularImmersion · Stacks.Chow.localizedChernClass_eq_bivariantComposite_of_isRegularImmersion · Stacks.Chow.completedVirtualNormalGysinClassOfImmersion_comp_ofIsRegularImmersion · Stacks.AlgebraicGeometry.isRegularImmersion_comp · Stacks.Chow.completedBivariantCompositeOfInvertible_completedFlatPullbackOfSmooth_of_section · Stacks.AlgebraicGeometry.isRegularImmersion_of_smooth_section · Stacks.Chow.SmoothFactorization.isKoszulRegularImmersion

Section42.60 Gysin maps for diagonals#

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

Tag 0FBR, the section

Tag 0FBR in the Stacks Project.

Stacks.Chow.isRegularImmersion_diagonal_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalGysin.lean, line 50. The attribute's comment: “the diagonal of a smooth morphism is a regular immersion”. References: SGA 6 VII (1.10), “special case”; SGA 6 VIII (1.3), “special case”.

The diagonal Δ : X ⟶ X ×_Y X of a smooth morphism is a regular immersion.

theorem isRegularImmersion_diagonal_of_smooth [Smooth f] :
    Stacks.AlgebraicGeometry.RegularIdealSheaf.IsRegularImmersion (pullback.diagonal f)

Stacks.Chow.gysinMapExists_diagonal_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalGysin.lean, line 57. The attribute's comment: “the Gysin map Δ^! is available for the diagonal”.

The Gysin map exists for the diagonal of a smooth morphism, in the sense of Stacks 0FF3.

theorem gysinMapExists_diagonal_of_smooth [Smooth f] :
    GysinMapExists (pullback.diagonal f)

Stacks.Chow.diagonalGysinClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalGysinClass.lean, line 158. The attribute's comment: “the Gysin class Δ^! ∈ A^d(X → X ×_Y X) of the diagonal of a smooth morphism of constant relative dimension d”.

Stacks 0FBR, the Gysin class Δ^! ∈ A^d(Y ⟶ Y ×_Z Y) of the diagonal of a smooth morphism g : Y ⟶ Z of constant relative dimension d: the class c(Y ⟶ Y ×_Z Y, 𝒩) of Stacks 0FBQ (3) of the normal bundle 𝒩 of the diagonal (Stacks 0FEZ), at the open subscheme U = (pullback.diagonal g).coborderRange in which the diagonal is closed. It is c(Y ⟶ U, 𝒩) ∘ ι^* by Stacks.Chow.diagonalGysinClass_eq_bivariantCompositeOfInvertible.

def diagonalGysinClass :
    BivariantClass C (gysinSystemOfInvertible C)
      (pullback.diagonal g ≫ (pullback.fst g g ≫ sY)) (pullback.fst g g ≫ sY)
      (pullback.diagonal g) rfl d

Stacks.Chow.isFiniteLocallyFreeOfRank_diagonalVirtualNormalBundle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalVirtualNormalBundle.lean, line 286. The attribute's comment: “constant relative dimension d: the normal bundle of the diagonal has rank d”.

Stacks Project, Section 42.60 (Tag 0FBR), the degree. For f smooth of constant relative dimension d, the normal bundle of the diagonal is finite locally free of rank d; this is why the Gysin class Δ^! lies in A^d(Y ⟶ Y ×_Z Y).

theorem isFiniteLocallyFreeOfRank_diagonalVirtualNormalBundle [Smooth f] {d : ℕ}
    (hd : RelativeDimension f d) :
    AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      (diagonalVirtualNormalBundle f).bundle d
Tag 0FBS, a lemma

Tag 0FBS in the Stacks Project.

Stacks.Chow.diagonalGysinClass_compFlatPullbackEqOne_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalGysinClassUnit.lean, line 375. The attribute's comment: “Δ^! ∘ pr_1^* = 1 in A^0(X), on cap operations, for the first projection”.

Stacks 0FBS for the first projection: Δ^! ∘ pr_1^* = 1 in A^0(Y). For g : Y ⟶ Z smooth of relative dimension d, capping the flat pullback along pr_1 : Y ×_Z Y ⟶ Y with the Gysin class Δ^! of the diagonal is the identity on the Chow groups of every test scheme over Y.

theorem diagonalGysinClass_compFlatPullbackEqOne_fst :
    (diagonalGysinClass C sY g hd).CompFlatPullbackEqOne (pullback.fst g g) rfl
      (pullback.diagonal_fst g) (relativeDimension_pullback_fst_self g hd)

Stacks.Chow.diagonalGysinClass_compFlatPullbackEqOne_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalGysinClassUnit.lean, line 388. The attribute's comment: “Δ^! ∘ pr_2^* = 1 in A^0(X), on cap operations, for the second projection”.

Stacks 0FBS for the second projection: Δ^! ∘ pr_2^* = 1 in A^0(Y). For g : Y ⟶ Z smooth of relative dimension d, with Z over the base compatibly with Y, capping the flat pullback along pr_2 : Y ×_Z Y ⟶ Y with the Gysin class Δ^! of the diagonal is the identity on the Chow groups of every test scheme over Y.

theorem diagonalGysinClass_compFlatPullbackEqOne_snd (sZ : Z ⟶ C.S) [LocallyOfFiniteType sZ]
    (hg : g ≫ sZ = sY) :
    (diagonalGysinClass C sY g hd).CompFlatPullbackEqOne (pullback.snd g g)
      (smoothShift_pullback_snd_comp_structureMorphism C sY sZ g hg) (pullback.diagonal_snd g)
      (relativeDimension_pullback_snd g g d hd)

Stacks.Chow.bivariantIdentityClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalGysinIdentity.lean, line 284. The attribute's comment: “the right-hand side: the unit 1 ∈ A^0(X) of Stacks 0B76, built with the proper and flat axioms discharged and the Gysin axiom of Stacks 0B76 for its cap operation carried as a hypothesis; the Gysin classes Δ^! and pr_i^! of the left-hand side cannot be written down here, their three inputs — Stacks 0FBK, 0B78 and a construction of the composition of Stacks 0B75 — all being absent from this repository”.

Stacks 0FBS, the right-hand side. The identity bivariant class 1 ∈ A^0(X): the bivariant class of degree 0 for 𝟙 X whose operation on every test scheme g : T ⟶ X is the identity of A_k(T), carried to the chosen pullback X ×_X T along the canonical isomorphism.

The Gysin axiom of Stacks 0B76 is the hypothesis hgysin; it is literally the gysin_naturality field of Stacks.Chow.BivariantClass for this cap operation, hence the weakest hypothesis that produces the class, and it is a Prop, so the class does not depend on which proof is supplied. See the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.DiagonalGysinIdentity.

def bivariantIdentityClass (G : GysinSystem C)
    (hgysin : IdentityCapRule.TransportGysinNaturality C sX 0 (identityCapRule C sX) G) :
    BivariantClass C G sX sX (𝟙 X) (Category.id_comp sX) 0

Stacks.Chow.eq_bivariantIdentityClass_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalGysinIdentity.lean, line 334. The attribute's comment: “the conclusion, reduced to an identification: a degree-0 class for 𝟙 X equals the unit 1 ∈ A^0(X) exactly when it acts as the identity on every test scheme; the composite Δ^! ∘ pr_i^! itself is not constructed, the Gysin classes needing Stacks 0FBK, 0B78 and a construction of the composition of Stacks 0B75”.

Stacks 0FBS, the identification with 1. A bivariant class of degree 0 for 𝟙 X is the identity class exactly when the operation it induces on every test scheme is the identity.

This is what the conclusion of Stacks 0FBS asserts of Δ^! ∘ pr_i^!, and the direction that matters for the tag is the one from right to left: a composite acting as the identity on Chow groups is the class 1. Uniqueness comes from Stacks.Chow.BivariantClass.eq_of_pushforward_cap_eq, pushforward along the base-change isomorphism being a bijection of Chow groups.

theorem eq_bivariantIdentityClass_iff (G : GysinSystem C)
    (hgysin : IdentityCapRule.TransportGysinNaturality C sX 0 (identityCapRule C sX) G)
    (c : BivariantClass C G sX sX (𝟙 X) (Category.id_comp sX) 0) :
    c = bivariantIdentityClass C sX G hgysin ↔
      ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (g ≫ sX) k),
        chowPushforwardOfIso C (pullback.fst (𝟙 X) g ≫ sX) (g ≫ sX)
            (identityBaseChangeIso g).hom (identityBaseChangeIso_hom_comp_base C sX g) (k - 0)
            (c.cap g k α) =
          identityCapRule C sX g k α

Stacks.Chow.gysinMapExists_fst_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalGysinIdentity.lean, line 389. The attribute's comment: “a geometric input: the Gysin map of the first projection X ×_Y X ⟶ X is available, the projection being smooth by base change; the class pr_1^! itself is not constructed, needing Stacks 0FBK, 0B78 and a construction of the composition of Stacks 0B75”.

Stacks 0FBS, the geometric input for the first projection. The Gysin map of Stacks 0FF3 is available for pr_1 : X ×_Y X ⟶ X, which is smooth because f is and smoothness is stable under base change. Together with CategoryTheory.Limits.pullback.diagonal_fst, which says Δ ≫ pr_1 = 𝟙 X, and Stacks.Chow.gysinMapExists_diagonal_of_smooth, this is the geometric content the source proof of Stacks 0FBS uses.

theorem gysinMapExists_fst_of_smooth {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] :
    GysinMapExists (pullback.fst f f)

Stacks.Chow.gysinMapExists_snd_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalGysinIdentity.lean, line 399. The attribute's comment: “a geometric input: the Gysin map of the second projection X ×_Y X ⟶ X is available, the projection being smooth by base change; the class pr_2^! itself is not constructed, needing Stacks 0FBK, 0B78 and a construction of the composition of Stacks 0B75”.

Stacks 0FBS, the geometric input for the second projection. The Gysin map of Stacks 0FF3 is available for pr_2 : X ×_Y X ⟶ X, which is smooth by base change; and CategoryTheory.Limits.pullback.diagonal_snd says Δ ≫ pr_2 = 𝟙 X.

theorem gysinMapExists_snd_of_smooth {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] :
    GysinMapExists (pullback.snd f f)

Stacks.Chow.copy_cap_heq_bivariantCompositeCap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/DiagonalGysinIdentity.lean, line 429. The attribute's comment: “the left-hand side, read in A^0(X): the transport along Δ ≫ pr_i = 𝟙 X of a bivariant class witnessing the composition of one for Δ with one for pr_i in total degree 0 caps by the composite operation; the Gysin classes Δ^! and pr_i^! are carried as arbitrary bivariant classes, since Stacks 0FBK, 0B78 and a construction of the composition of Stacks 0B75 are all absent from this repository”.

Stacks 0FBS, the left-hand side. Let pr : X ×_Y X ⟶ X be a projection, so that Δ ≫ pr = 𝟙 X, let a ∈ A^p(X ⟶ X ×_Y X) be a bivariant class for the diagonal — the slot Δ^! occupies — and let b ∈ A^q(X ×_Y X ⟶ X) be one for the projection, the slot pr^! occupies, with p + q = 0. If c witnesses that it is the composition of a and b, then the class in A^0(X ⟶ X) that c becomes under Δ ≫ pr = 𝟙 X caps by the composite operation a ∩ (b ∩ -).

With Stacks.Chow.eq_bivariantIdentityClass_iff this says that Δ^! ∘ pr^! = 1 holds exactly when the composite operation acts as the identity on the Chow groups of every test scheme; and by Stacks.Chow.eq_of_isBivariantClassComposition there is at most one class c witnessing the composition, so no generality is lost by carrying it as a hypothesis.

theorem copy_cap_heq_bivariantCompositeCap
    (a : BivariantClass C G sX sP (pullback.diagonal f) hΔ p)
    (b : BivariantClass C G sP sX pr hpr q)
    (c : BivariantClass C G sX sX (pullback.diagonal f ≫ pr)
      (comp_comp_structureMorphism_eq hΔ hpr) (p + q))
    (hc : IsBivariantClassComposition C G sX sP sX (pullback.diagonal f) pr hΔ hpr hpp p q a b c)
    {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
    (α : chowGroup C (t ≫ sX) k) :
    HEq ((BivariantClass.copy C G sX sX hdiag (comp_comp_structureMorphism_eq hΔ hpr)
          (Category.id_comp sX) hpq c).cap t k α)
      (bivariantCompositeCap C G sX sP sX (pullback.diagonal f) pr hΔ hpr hpp p q a b t k α)
Tag 0FBT, a proposition

Tag 0FBT in the Stacks Project.

Stacks.Chow.smoothRelativeDimensionShiftEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SmoothChowCohomology.lean, line 79. The attribute's comment: “g^! read as the flat pullback g^* of the smooth morphism g; bivariant classes are those of the Gysin system of invertible modules, Stacks.Chow.gysinSystemOfInvertible”.

Stacks 0FBT. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of schemes locally of finite type over S, with g smooth of relative dimension d. Then c ↦ c ∘ g^* is an isomorphism

A^p(X ⟶ Y) ≃ A^{p-d}(X ⟶ Z),

with inverse c' ↦ res(Δ^!) ∘ res(c'), where Δ^! is the Gysin class of the diagonal of g (Stacks 0FBR). For a smooth g the Gysin map g^! of Stacks 0FEZ is the flat pullback g^*.

def smoothRelativeDimensionShiftEquiv :
    BivariantClass C (gysinSystemOfInvertible C) sX sY f hf p ≃+
      BivariantClass C (gysinSystemOfInvertible C) sX sZ (f ≫ g)
        (comp_comp_structureMorphism_eq hf hg) (p - d)
Sources
LeanStacks.Chow.isRegularImmersion_diagonal_of_smooth · Stacks.Chow.gysinMapExists_diagonal_of_smooth · Stacks.Chow.diagonalGysinClass · Stacks.Chow.isFiniteLocallyFreeOfRank_diagonalVirtualNormalBundle · Stacks.Chow.diagonalGysinClass_compFlatPullbackEqOne_fst · Stacks.Chow.diagonalGysinClass_compFlatPullbackEqOne_snd · Stacks.Chow.bivariantIdentityClass · Stacks.Chow.eq_bivariantIdentityClass_iff

Section42.61 Exterior product#

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

Tag 0FBV, a lemma

Tag 0FBV in the Stacks Project.

Stacks.Chow.exteriorProduct_mem_rationalEquivalences_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductRationalEquivalence.lean, line 521. The attribute's comment: “well defined in the second variable, unconditionally”.

The exterior product of an n-cycle on X with an m-cycle on Y which is rationally equivalent to zero is rationally equivalent to zero.

theorem exteriorProduct_mem_rationalEquivalences_right (C : ChowSituation.{u}) [Subsingleton C.S]
    [IsIntegral C.S] [JacobsonSpace C.S]
    (hδ : ∀ s : C.S, IsClosed ({s} : Set C.S) → C.dimensionFunction s = 0)
    {X Y : Scheme.{u}} (f : X ⟶ C.S) [LocallyOfFiniteType f] (g : Y ⟶ C.S)
    [LocallyOfFiniteType g] (n m : ℤ)
    (α : CycleGroup C f n) {β : CycleGroup C g m} (hβ : β ∈ rationalEquivalences C g m) :
    exteriorProduct C f g n m α β ∈ rationalEquivalences C (pullback.fst f g ≫ f) (n + m)

Stacks.Chow.exteriorProduct_mem_rationalEquivalences_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductRationalEquivalence.lean, line 618. The attribute's comment: “well defined in the first variable, unconditionally”.

The exterior product of an n-cycle on X which is rationally equivalent to zero with an m-cycle on Y is rationally equivalent to zero.

theorem exteriorProduct_mem_rationalEquivalences_left (C : ChowSituation.{u}) [Subsingleton C.S]
    [IsIntegral C.S] [JacobsonSpace C.S]
    (hδ : ∀ s : C.S, IsClosed ({s} : Set C.S) → C.dimensionFunction s = 0)
    {X Y : Scheme.{u}} (f : X ⟶ C.S) [LocallyOfFiniteType f] (g : Y ⟶ C.S)
    [LocallyOfFiniteType g] (n m : ℤ)
    {α : CycleGroup C f n} (hα : α ∈ rationalEquivalences C f n) (β : CycleGroup C g m) :
    exteriorProduct C f g n m α β ∈ rationalEquivalences C (pullback.fst f g ≫ f) (n + m)

Stacks.Chow.chowExteriorProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductRationalEquivalence.lean, line 707.

The exterior product on Chow groups,

× : CH_n(X) ⊗_ℤ CH_m(Y) ⟶ CH_{n+m}(X ×_k Y),

for X and Y locally of finite type over a field: the exterior product of cycles, Stacks.Chow.exteriorProduct, read modulo rational equivalence.

def chowExteriorProduct (C : ChowSituation.{u}) [Subsingleton C.S] [IsIntegral C.S]
    [JacobsonSpace C.S] (hδ : ∀ s : C.S, IsClosed ({s} : Set C.S) → C.dimensionFunction s = 0)
    {X Y : Scheme.{u}} (f : X ⟶ C.S) [LocallyOfFiniteType f] (g : Y ⟶ C.S)
    [LocallyOfFiniteType g] (n m : ℤ) :
    TensorProduct ℤ (chowGroup C f n) (chowGroup C g m) →+
      chowGroup C (pullback.fst f g ≫ f) (n + m)
Tag 0FBW, a lemma

Tag 0FBW in the Stacks Project.

Stacks.Chow.bivariantToBaseEval, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOverField.lean, line 186. The attribute's comment: “the canonical map A^p(X → Spec k) → CH_{-p}(X), cap product with the fundamental class of the point”.

Stacks 0FBW. The canonical map A^p(X ⟶ Spec k) ⟶ CH_{-p}(X): cap product with the fundamental class of the point, read through the collapse of X ×_{Spec k} Spec k onto X along its first projection. It is injective by Stacks.Chow.bivariantToBaseEval_injective; surjectivity is not proved here, see the implementation notes of this module.

def bivariantToBaseEval : bivariantToBase C G sX p →+ chowGroup C sX (-p)

Stacks.Chow.bivariantToBaseEval_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOverField.lean, line 303. The attribute's comment: “injectivity of the canonical identification, for the base being the spectrum of a field; hS1 is Stacks 02S1 and hfund is Stacks 02NK with Stacks 02R4”.

Stacks 0FBW, injectivity. The canonical map A^p(X ⟶ Spec k) ⟶ CH_{-p}(X) of Stacks 0FBW is injective: a bivariant class of degree p for the structure morphism of X is determined by its cap product with the fundamental class of the point. Surjectivity is not proved here; see the implementation notes of this module.

theorem bivariantToBaseEval_injective
    [Subsingleton C.S] [IsIntegral C.S] (hS1 : FlatPullbackDescends C)
    (hfund : IntegralFundamentalClassIsFlatPullback C hS1) :
    Function.Injective (bivariantToBaseEval C G sX p)

Stacks.Chow.bivariantToBaseEval_bijective_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOverFieldIso.lean, line 412. The attribute's comment: “the canonical map A^p(X → Spec k) → CH_{-p}(X), c ↦ c ∩ [Spec k], is bijective”.

Let k be a field and X a scheme locally of finite type over k. For every p ∈ ℤ the canonical map A^p(X ⟶ Spec k) ⟶ CH_{-p}(X), c ↦ c ∩ [Spec k], is bijective. Here A^p(X ⟶ Spec k) is the group of bivariant classes of degree p for the structure morphism (Stacks 0B76), read at the Gysin system of the first Chern class of an invertible module, and the cap product with the fundamental class of the point is read on X through the first projection X ×_{Spec k} Spec k ≅ X.

theorem bivariantToBaseEval_bijective_field (p : ℤ) :
    Function.Bijective
      (bivariantToBaseEval (fieldChowSituation k)
        (gysinSystemOfInvertible (fieldChowSituation k)) sX p)

Stacks.Chow.bivariantToBaseEquivField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOverFieldIso.lean, line 426. The attribute's comment: “the canonical identification A^p(X → Spec k) = CH_{-p}(X) as an isomorphism of groups”.

The canonical identification A^p(X ⟶ Spec k) = CH_{-p}(X) over a field, as an isomorphism of abelian groups: cap product with the fundamental class of the point.

def bivariantToBaseEquivField (p : ℤ) :
    bivariantToBase (fieldChowSituation k) (gysinSystemOfInvertible (fieldChowSituation k)) sX p ≃+
      chowGroup (fieldChowSituation k) sX (-p)

Stacks.Chow.bivariantChowClassToBaseEquivField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOverFieldIso.lean, line 446. The attribute's comment: “the canonical identification A^p(X → Spec k) = CH_{-p}(X), c ↦ c ∩ [Spec k], for the bivariant group of Stacks 0B76 whose cap operations are maps”.

For the bivariant group A^p(X ⟶ Spec k) of Stacks 0B76 in the form Stacks.Chow.BivariantChowClass, whose cap operations are plain maps, cap product with the fundamental class of the point is an isomorphism A^p(X ⟶ Spec k) ≃ CH_{-p}(X).

def bivariantChowClassToBaseEquivField (p : ℤ) :
    BivariantChowClass (fieldChowSituation k) sX (𝟙 (fieldChowSituation k).S) sX
        (Category.comp_id sX) p ≃+
      chowGroup (fieldChowSituation k) sX (-p)

Stacks.Chow.bivariantToBaseEval_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOverFieldSurjective.lean, line 246. The attribute's comment: “surjectivity of the canonical identification; hEPK is Stacks 0EPK, hgen is the generation of Chow homology by proper pushforwards of flat pullbacks of the class of the point (Stacks 02UC with Stacks 02R4), hS1 is Stacks 02S1, hpp is Stacks 02S2, hRG is Stacks 02RG and h71 is Stacks 0B71 in every relative dimension”.

The canonical map A^p(X ⟶ Spec k) ⟶ CH_{-p}(X), cap product with the fundamental class of the point, is surjective. The hypotheses are the existence of proper pushforwards of bivariant classes (hEPK, Stacks 0EPK), the generation of CH_{-p}(X) by proper pushforwards of flat pullbacks of [Spec k] (hgen), the descent of flat pullback and proper pushforward to Chow groups (hS1, hpp), Stacks 02RG (hRG) and Stacks 0B71 in every relative dimension (h71).

theorem bivariantToBaseEval_surjective (hS1 : FlatPullbackDescends C)
    (hRG : ProperPushforwardFlatPullbackBaseChange C) (hpp : ProperPushforwardDescends C)
    (h71 : ∀ r : ℕ, G.FlatPullbackNaturality r)
    (hEPK : BivariantProperPushforwardExists C G)
    (hgen : ChowClassesGeneratedByBaseFlatPullbacks C hS1 hpp) :
    Function.Surjective (bivariantToBaseEval C G sX p)

Stacks.Chow.bivariantToBaseEval_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOverFieldSurjective.lean, line 270. The attribute's comment: “the canonical identification A^p(X → Spec k) = CH_{-p}(X), for the base being the spectrum of a field; hEPK is Stacks 0EPK, hgen is Stacks 02R4, hS1 is Stacks 02S1, hpp is Stacks 02S2, hRG is Stacks 02RG, h71 is Stacks 0B71 and hfund is Stacks 02NK with Stacks 02R4”.

The canonical map A^p(X ⟶ Spec k) ⟶ CH_{-p}(X) is bijective when the base has one point and is integral, that is, is the spectrum of a field: cap product with the fundamental class of the point identifies the bivariant classes of degree p for the structure morphism of X with the Chow homology of X in degree -p. The hypotheses are those of Stacks.Chow.bivariantToBaseEval_injective and Stacks.Chow.bivariantToBaseEval_surjective.

theorem bivariantToBaseEval_bijective
    [Subsingleton C.S] [IsIntegral C.S] (hS1 : FlatPullbackDescends C)
    (hfund : IntegralFundamentalClassIsFlatPullback C hS1)
    (hRG : ProperPushforwardFlatPullbackBaseChange C) (hpp : ProperPushforwardDescends C)
    (h71 : ∀ r : ℕ, G.FlatPullbackNaturality r)
    (hEPK : BivariantProperPushforwardExists C G)
    (hgen : ChowClassesGeneratedByBaseFlatPullbacks C hS1 hpp) :
    Function.Bijective (bivariantToBaseEval C G sX p)

Stacks.Chow.bivariantToBaseEval_bijective_of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOverFieldUnconditional.lean, line 383. The attribute's comment: “the bivariant classes are those of the Gysin system of invertible modules, Stacks.Chow.gysinSystemOfInvertible”.

Stacks 0FBW. Let X be locally of finite type over a field k. Cap product with the fundamental class of the point, A^p(X ⟶ Spec k) ⟶ CH_{-p}(X), is bijective.

theorem bivariantToBaseEval_bijective_of_field :
    Function.Bijective (bivariantToBaseEval (fieldChowSituation k)
      (gysinSystemOfInvertible (fieldChowSituation k)) sX p)

Stacks.Chow.bivariantToBaseEquivOfField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/ChowCohomologyOverFieldUnconditional.lean, line 398. The attribute's comment: “the bivariant classes are those of the Gysin system of invertible modules, Stacks.Chow.gysinSystemOfInvertible”.

Stacks 0FBW. For X locally of finite type over a field k, the identification A^p(X ⟶ Spec k) ≃ CH_{-p}(X), c ↦ c ∩ [Spec k], as an isomorphism of groups.

def bivariantToBaseEquivOfField :
    bivariantToBase (fieldChowSituation k) (gysinSystemOfInvertible (fieldChowSituation k)) sX p ≃+
      chowGroup (fieldChowSituation k) sX (-p)
Tag 0FBX, a lemma

Tag 0FBX in the Stacks Project.

Stacks.Chow.bivariantCommute_bivariantToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/PointClassCommuting.lean, line 649. The attribute's comment: “a bivariant class towards the point commutes with every bivariant class, in the form of Stacks 0FA2, for the base being the spectrum of a field; hfund, hEPK and hgen are the prerequisites of Stacks 0FBW, hS1 is Stacks 02S1, hpp is Stacks 02S2, hRG is Stacks 02RG, h71 is Stacks 0B71 and hgys is the isomorphism case of Stacks 02TA”.

Stacks 0FBX. Let c ∈ A^p(X ⟶ S) be a bivariant class towards the point and let c' ∈ A^q(Y ⟶ Z) be an arbitrary bivariant class, for an arbitrary morphism f : Y ⟶ Z of schemes locally of finite type over the base. Then the base change of c to Z and c' commute, in the sense of Stacks 0FA2.

The proof is the source's. By Stacks 0FBW the map c ↦ c ∩ [Spec k] is a bijection of A^p(X ⟶ S) with CH_{-p}(X), and CH_{-p}(X) is generated by proper pushforwards of flat pullbacks of the class of the point; so c is a ℤ-combination of classes g\_* ∘ (flat pullback). Commuting with c' is preserved by ℤ-combinations, so it is enough to treat one such class. Its base change to Z is again a proper pushforward of a flat-pullback class, by Stacks.Chow.isBivariantProperPushforward_bivariantToBaseRestriction; that flat-pullback class commutes with c' by the flat law of Stacks 0B76, which is Stacks.Chow.bivariantCommute_flatPullbackBivariantClass; and proper pushforward preserves commuting by Stacks.Chow.bivariantCommute_of_isBivariantProperPushforward.

Nothing here assumes that c and c' commute, nor that any other pair of classes does; the hypotheses are the prerequisites of Stacks 0FBW together with the descent statements this part of the library quantifies rather than parameterizes.

theorem bivariantCommute_bivariantToBase [Subsingleton C.S] [IsIntegral C.S]
    (c : bivariantToBase C G sX p)
    (c' : BivariantClass C G (f ≫ sZ) sZ f rfl q)
    (hpp : ProperPushforwardDescends C) (hS1 : FlatPullbackDescends C)
    (hRG : ProperPushforwardFlatPullbackBaseChange C)
    (h71 : ∀ r : ℕ, G.FlatPullbackNaturality r)
    (hEPK : BivariantProperPushforwardExists C G)
    (hgen : ChowClassesGeneratedByBaseFlatPullbacks C hS1 hpp)
    (hfund : IntegralFundamentalClassIsFlatPullback C hS1) :
    BivariantCommute C G sZ (pullback.snd sX sZ) f p q
      (bivariantToBaseRestrictionHom C G sX sZ p hgys c) c'

Stacks.Chow.bivariantToBase_commuteCompositeCap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/PointClassCommuting.lean, line 722. The attribute's comment: “the equality of the two composites c ∘ c' = c' ∘ c of the tag, as operations on every test Chow group; the hypotheses are those of Stacks.Chow.bivariantCommute_bivariantToBase”.

Stacks 0FBX, in the shape the tag states it. The two composites c ∘ c' and c' ∘ c, both bivariant classes of degree p + q for X ×_S Y ⟶ Z, agree as operations on every test Chow group, under the canonical identification of their sources and the equality p + q = q + p of their degrees.

This is Stacks.Chow.bivariantCommute_bivariantToBase read through Stacks.Chow.bivariantCommute_iff_commuteCompositeCap_eq, the equivalence of Stacks 0FA2 between commuting and the equality of the two composites.

theorem bivariantToBase_commuteCompositeCap_eq [Subsingleton C.S] [IsIntegral C.S]
    (c : bivariantToBase C G sX p)
    (c' : BivariantClass C G (f ≫ sZ) sZ f rfl q)
    (hpp : ProperPushforwardDescends C) (hS1 : FlatPullbackDescends C)
    (hRG : ProperPushforwardFlatPullbackBaseChange C)
    (h71 : ∀ r : ℕ, G.FlatPullbackNaturality r)
    (hEPK : BivariantProperPushforwardExists C G)
    (hgen : ChowClassesGeneratedByBaseFlatPullbacks C hS1 hpp)
    (hfund : IntegralFundamentalClassIsFlatPullback C hS1) :
    ∀ {T : Scheme.{u}} (t : T ⟶ Z) [LocallyOfFiniteType t] (k : ℤ)
      (α : chowGroup C (t ≫ sZ) k),
      chowPushforwardOfIso C
          (pullback.fst (pullback.snd (pullback.snd sX sZ) f ≫ f) t ≫
            (pullback.fst (pullback.snd sX sZ) f ≫ (pullback.snd sX sZ ≫ sZ)))
          (pullback.fst (pullback.snd f (pullback.snd sX sZ) ≫ pullback.snd sX sZ) t ≫
            (pullback.fst f (pullback.snd sX sZ) ≫ (f ≫ sZ)))
          (compositeComparisonHom (pullback.snd sX sZ) f t)
          (compositeComparisonHom_comp_structureMorphism C sZ (pullback.snd sX sZ) f t)
          ((k - q) - p)
          (commuteCompositeCap C G sZ (pullback.snd sX sZ) f p q
            (bivariantToBaseRestrictionHom C G sX sZ p hgys c) c' hgys hpp t k α) =
        chowGroupDegreeEquiv C
          (pullback.fst (pullback.snd f (pullback.snd sX sZ) ≫ pullback.snd sX sZ) t ≫
            (pullback.fst f (pullback.snd sX sZ) ≫ (f ≫ sZ)))
          (by ring : (k - p) - q = (k - q) - p)
          (commuteCompositeCap C G sZ f (pullback.snd sX sZ) q p c'
            (bivariantToBaseRestrictionHom C G sX sZ p hgys c) hgys hpp t k α)

Stacks.Chow.BivariantChowClass.comp_comm_of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/PointClassCommutingField.lean, line 773. The attribute's comment: “c ∘ c' = c' ∘ c in A^{p+q}(X ×_k Y → Z) for c ∈ A^p(X → Spec k) and c' ∈ A^q(Y → Z), the composites read as in Stacks 0FA2”.

Stacks 0FBX. Let k be a field and let X be a scheme locally of finite type over k. Let c ∈ A^p(X ⟶ Spec k). Let f : Y ⟶ Z be a morphism of schemes locally of finite type over k and let c' ∈ A^q(Y ⟶ Z). Then c ∘ c' = c' ∘ c in A^{p+q}(X ×_k Y ⟶ Z).

Here c ∘ c' = res(c) ∘ c' with res(c) ∈ A^p(X ×_k Y ⟶ Y) the restriction of c along Y ⟶ Spec k, and c' ∘ c = res(c') ∘ res(c) with res(c) ∈ A^p(X ×_k Z ⟶ Z) the restriction of c along Z ⟶ Spec k and res(c') ∈ A^q(Y ×_Z (X ×_k Z) ⟶ X ×_k Z) the restriction of c' along X ×_k Z ⟶ Z (Stacks 0F9Z, 0FA2). The second composite lives on Y ×_Z (X ×_k Z) and in degree q + p; it is read on X ×_k Y through the canonical isomorphism and in degree p + q.

theorem BivariantChowClass.comp_comm_of_field
    (c : BivariantChowClass (fieldChowSituation k) sX (𝟙 (fieldChowSituation k).S) sX
      (Category.comp_id sX) p)
    (c' : BivariantChowClass (fieldChowSituation k) sY sZ f hf q) :
    (c.restrict sY (Category.comp_id sY)).comp c' =
      (((c'.restrict (pullback.snd sX sZ)
          (BivariantChowClass.restrict_structure_eq (Category.comp_id sX) sZ
            (Category.comp_id sZ))).comp
        (c.restrict sZ (Category.comp_id sZ))).degreeCongr (add_comm q p)).transport
        (comp_comp_structureMorphism_eq
          (BivariantChowClass.restrict_structure_eq (Category.comp_id sX) sY
            (Category.comp_id sY)) hf)
        (pointClassCompositeIso (fieldChowSituation k) sX sZ f hf)
        (pointClassCompositeIso_hom_comp (fieldChowSituation k) sX sZ f hf)
Tag 0FBY, a remark

Tag 0FBY in the Stacks Project.

Stacks.Chow.commutesExteriorProductCapAt_fundamentalChowClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductCapCommuting.lean, line 643. The attribute's comment: “the equation α × (c ∩ β) = c ∩ (α × β) of the tag, for α the fundamental class of an integral scheme X flat of relative dimension d over the base — NOT for a general α ∈ CH_n(X), for which the missing inputs are recorded in the module notes; carries Stacks 02S1 as hfp, Stacks 02RG on Chow groups as hRG, and Stacks 0B71 with the identification of Stacks 0B6Y as h71, these being exactly the hypotheses of Stacks 0B78 in this repository”.

Stacks 0FBY for the fundamental class of an integral scheme flat over the base. Let the base be the spectrum of a field, let X be integral and flat over it of relative dimension d, let u : Y ⟶ Z be a morphism of schemes locally of finite type over the base and let c ∈ A^p(Y ⟶ Z) be a bivariant class. Then for every β ∈ CH_m(Z)

[X] × (c ∩ β) = c ∩ ([X] × β)

in CH_{d + (m - p)}(X ×_S Y), where [X] ∈ CH_d(X) is the fundamental class of X and the two sides are read through the canonical identifications of Stacks.Chow.exteriorProductCap and Stacks.Chow.capExteriorProduct.

The first variable is a fundamental class and not a general α ∈ CH_n(X); see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.ExteriorProductCapCommuting for what the general case needs and for why it is unavailable here.

The proof replaces [X] × - by the cap operation of the flat-pullback class of Stacks 0B78 for the structure morphism of X, whose base change to Z is the flat-pullback class for pr_Z : X ×_S Z ⟶ Z, and that class commutes with c by the smooth half of Stacks 0FF6. The commuting identity is then instantiated at the test scheme 𝟙 Z and both of its sides are transported to X ×_S Y.

theorem commutesExteriorProductCapAt_fundamentalChowClass
    (c : BivariantClass C G sY sZ u hu p)
    (hfr : AlgebraicGeometry.RelativeDimension sX d)
    (hd : relativeDimension C.dimensionFunction sX (genericPoint X) = (d : ℤ))
    (hRG : ProperPushforwardFlatPullbackBaseChange C) (h71 : G.FlatPullbackNaturality d) :
    CommutesExteriorProductCapAt C hδ G sX sY sZ u hu p c (d : ℤ) m
      (fundamentalChowClass C sX (d : ℤ))

Stacks.Chow.commutesExteriorProductCap_of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductCapCommutingEveryCap.lean, line 889. The attribute's comment: “the bivariant classes are those of the Gysin system of invertible modules, Stacks.Chow.gysinSystemOfInvertible”.

Stacks 0FBY over a field. Let k be a field, X locally of finite type over k, u : Y ⟶ Z a morphism of schemes locally of finite type over k, and c ∈ A^p(Y ⟶ Z). Then

α × (c ∩ β) = c ∩ (α × β) in CH_{n + (m - p)}(X ×_k Y)

for every α ∈ CH_n(X) and every β ∈ CH_m(Z).

theorem commutesExteriorProductCap_of_field (n m : ℤ) :
    CommutesExteriorProductCap (fieldChowSituation k) (fun _ _ ↦ rfl)
      (gysinSystemOfInvertible (fieldChowSituation k)) sX sY sZ u hu p c n m

Stacks.Chow.commutesExteriorProductCap_of_subsingleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductCapCommutingGeneral.lean, line 429. The attribute's comment: “α × (c ∩ β) = c ∩ (α × β) in CH_*(X ×_S Y), over a base which is a point with dimension function zero (in particular Spec k), for bivariant classes at any Gysin system”.

Stacks 0FBY over a point. Let the base be a point with dimension function zero, for instance the spectrum of a field, let X be locally of finite type over it, let u : Y ⟶ Z be a morphism of schemes locally of finite type over it and let c ∈ A^p(Y ⟶ Z) be a bivariant class for any Gysin system. Then for all α ∈ CH_n(X) and β ∈ CH_m(Z)

α × (c ∩ β) = c ∩ (α × β) in CH_{n + (m - p)}(X ×_S Y).

Write α = ∑ₓ nₓ [closure {x}]. Then α × β is the locally finite sum over the points x of the support of α of the pushforwards along closure {x} ×_S Z ⟶ X ×_S Z of the flat pullbacks of nₓ β along the flat projections closure {x} ×_S Z ⟶ Z. Capping with c commutes with each of these flat pullbacks by the flat-pullback axiom of Stacks 0B76, and with the locally finite sum by Stacks.Chow.BivariantClass.cap_chowGroupCongr_mk_eq_mk_of_locallyFinite; the result is the corresponding decomposition of α × (c ∩ β).

theorem commutesExteriorProductCap_of_subsingleton (c : BivariantClass C G sY sZ u hu p)
    (n m : ℤ) : CommutesExteriorProductCap C hδ G sX sY sZ u hu p c n m

Stacks.Chow.exteriorProductCap_eq_capExteriorProduct_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductCapCommutingGeneral.lean, line 571. The attribute's comment: “α × (c' ∩ β) = c' ∩ (α × β) in CH_*(X ×_k Y), for k a field and c' ∈ A^q(Y → Z) of Stacks 0B76”.

Stacks 0FBY. Let k be a field, let X be a scheme locally of finite type over k, let u : Y ⟶ Z be a morphism of schemes locally of finite type over k and let c' ∈ A^q(Y ⟶ Z). Then for α ∈ CH_n(X) and β ∈ CH_m(Z)

α × (c' ∩ β) = c' ∩ (α × β) in CH_{n + (m - q)}(X ×_k Y).

Here A^q(Y ⟶ Z) is the group of bivariant classes of Stacks 0B76, the exterior product is that of Stacks 0FBV, and the two sides are those of Stacks.Chow.exteriorProductCap and Stacks.Chow.capExteriorProduct: c' ∩ β is read on Y ≅ Y ×_Z Z, and c' ∩ (α × β) is the cap at the test scheme X ×_k Z ⟶ Z, read on X ×_k Y ≅ Y ×_Z (X ×_k Z).

theorem exteriorProductCap_eq_capExteriorProduct_field
    (c' : BivariantChowClass (fieldChowSituation k) sY sZ u hu q) (n m : ℤ)
    (α : chowGroup (fieldChowSituation k) sX n) (β : chowGroup (fieldChowSituation k) sZ m) :
    haveI := BivariantChowClass.locallyOfFiniteType_of_structure sZ u hu
    exteriorProductCap (fieldChowSituation k) (fun _ _ ↦ rfl)
        (gysinSystemOfInvertible (fieldChowSituation k)) sX sY sZ u hu q
        (BivariantChowClass.equivBivariantClass c') n m α β =
      capExteriorProduct (fieldChowSituation k) (fun _ _ ↦ rfl)
        (gysinSystemOfInvertible (fieldChowSituation k)) sX sY sZ u hu q
        (BivariantChowClass.equivBivariantClass c') n m α β
Tag 0FBZ, a lemma

Tag 0FBZ in the Stacks Project.

Stacks.Chow.chowExteriorProduct_assoc_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductAssociativity.lean, line 1105.

Stacks 0FBZ. The exterior product on Chow groups is associative. Let k be a field, let X, Y and Z be schemes locally of finite type over k and let a ∈ CH_n(X), b ∈ CH_m(Y), c ∈ CH_l(Z). Then

(a × b) × c = a × (b × c)

in CH_{n + m + l}(X ×_k Y ×_k Z).

The two sides are formed on the two bracketings of the triple product and in the two bracketings of the degree, so the left-hand side is carried into the group of the right-hand side by pushforward along the associator Stacks.Chow.tripleProductAssoc, which is an isomorphism over the base by Stacks.Chow.tripleProductAssoc_hom_comp_base, followed by Stacks.Chow.chowGroupDegreeEquiv for the degrees (n + m) + l and n + (m + l). Both of those transports are the identity on cycle coefficients, so what is asserted is the source's identity.

On classes of cycles it is Stacks.Chow.exteriorProduct_assoc, the cycle-level identity, read modulo rational equivalence. Nothing is assumed beyond the base being the spectrum of a field: the exterior product on Chow groups, Stacks.Chow.chowExteriorProduct, is itself unconditional over such a base, the instances of Stacks 02S1 that make it well defined being discharged inside it by Stacks.Chow.flatPullbackFactorsThroughRationalEquivalenceOnPointClosureFibres_holds.

theorem chowExteriorProduct_assoc_unconditional (k : Type u) [Field k] {X Y Z : Scheme.{u}}
    (f : X ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType f]
    (g : Y ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType g]
    (h : Z ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType h] (n m l : ℤ)
    (a : chowGroup (fieldChowSituation k) f n)
    (b : chowGroup (fieldChowSituation k) g m)
    (c : chowGroup (fieldChowSituation k) h l) :
    chowGroupDegreeEquiv (fieldChowSituation k)
        (pullback.fst f (pullback.fst g h ≫ g) ≫ f) (add_assoc n m l)
        (chowPushforwardOfIso (fieldChowSituation k)
          (pullback.fst (pullback.fst f g ≫ f) h ≫ pullback.fst f g ≫ f)
          (pullback.fst f (pullback.fst g h ≫ g) ≫ f) (tripleProductAssoc f g h).hom
          (tripleProductAssoc_hom_comp_base f g h) (n + m + l)
          (chowExteriorProduct (fieldChowSituation k) (fun _ _ ↦ rfl)
            (pullback.fst f g ≫ f) h (n + m) l
            (TensorProduct.tmul ℤ
              (chowExteriorProduct (fieldChowSituation k) (fun _ _ ↦ rfl) f g n m
                (TensorProduct.tmul ℤ a b)) c))) =
      chowExteriorProduct (fieldChowSituation k) (fun _ _ ↦ rfl) f (pullback.fst g h ≫ g) n
        (m + l)
        (TensorProduct.tmul ℤ a
          (chowExteriorProduct (fieldChowSituation k) (fun _ _ ↦ rfl) g h m l
            (TensorProduct.tmul ℤ b c)))

Stacks.Chow.chowExteriorProduct_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductAssociativity.lean, line 1176.

Stacks 0FBZ. The exterior product on Chow groups is associative. Let k be a field, let X, Y and Z be schemes locally of finite type over k and let a ∈ CH_n(X), b ∈ CH_m(Y), c ∈ CH_l(Z). Then

(a × b) × c = a × (b × c)

in CH_{n + m + l}(X ×_k Y ×_k Z).

The two sides are formed on the two bracketings of the triple product and in the two bracketings of the degree, so the left-hand side is carried into the group of the right-hand side by pushforward along the associator Stacks.Chow.tripleProductAssoc, which is an isomorphism over the base by Stacks.Chow.tripleProductAssoc_hom_comp_base, followed by Stacks.Chow.chowGroupDegreeEquiv for the degrees (n + m) + l and n + (m + l). Both of those transports are the identity on cycle coefficients, so what is asserted is the source's identity.

On classes of cycles it is Stacks.Chow.exteriorProduct_assoc, the cycle-level identity, read modulo rational equivalence. Stacks 02S1 is assumed, in the bundled form Stacks.Chow.FlatPullbackDescends; it is what makes the exterior product on Chow groups exist at all, see Stacks.Chow.chowExteriorProduct.

theorem chowExteriorProduct_assoc (k : Type u) [Field k]
    (hfp : FlatPullbackDescends (fieldChowSituation k)) {X Y Z : Scheme.{u}}
    (f : X ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType f]
    (g : Y ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType g]
    (h : Z ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType h] (n m l : ℤ)
    (a : chowGroup (fieldChowSituation k) f n)
    (b : chowGroup (fieldChowSituation k) g m)
    (c : chowGroup (fieldChowSituation k) h l) :
    chowGroupDegreeEquiv (fieldChowSituation k)
        (pullback.fst f (pullback.fst g h ≫ g) ≫ f) (add_assoc n m l)
        (chowPushforwardOfIso (fieldChowSituation k)
          (pullback.fst (pullback.fst f g ≫ f) h ≫ pullback.fst f g ≫ f)
          (pullback.fst f (pullback.fst g h ≫ g) ≫ f) (tripleProductAssoc f g h).hom
          (tripleProductAssoc_hom_comp_base f g h) (n + m + l)
          (chowExteriorProduct (fieldChowSituation k) (fun _ _ ↦ rfl)
            (pullback.fst f g ≫ f) h (n + m) l
            (TensorProduct.tmul ℤ
              (chowExteriorProduct (fieldChowSituation k) (fun _ _ ↦ rfl) f g n m
                (TensorProduct.tmul ℤ a b)) c))) =
      chowExteriorProduct (fieldChowSituation k) (fun _ _ ↦ rfl) f (pullback.fst g h ≫ g) n
        (m + l)
        (TensorProduct.tmul ℤ a
          (chowExteriorProduct (fieldChowSituation k) (fun _ _ ↦ rfl) g h m l
            (TensorProduct.tmul ℤ b c)))

Stacks.Chow.totalChowExteriorProduct_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductTotalAssociativity.lean, line 156.

Stacks 0FBZ. Exterior product is associative. Let k be a field, let X, Y, Z be schemes locally of finite type over k, and let α ∈ CH_*(X), β ∈ CH_*(Y), γ ∈ CH_*(Z). Then (α × β) × γ = α × (β × γ) in CH_*(X ×_k Y ×_k Z), the left-hand side being carried from (X ×_k Y) ×_k Z to X ×_k (Y ×_k Z) by pushforward along the associator of the fibre product.

theorem totalChowExteriorProduct_assoc (k : Type u) [Field k] {X Y Z : Scheme.{u}}
    (f : X ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType f]
    (g : Y ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType g]
    (h : Z ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType h]
    (α : DirectSum ℤ fun n : ℤ ↦ chowGroup (fieldChowSituation k) f n)
    (β : DirectSum ℤ fun m : ℤ ↦ chowGroup (fieldChowSituation k) g m)
    (γ : DirectSum ℤ fun l : ℤ ↦ chowGroup (fieldChowSituation k) h l) :
    totalChowPushforwardOfIso (fieldChowSituation k)
        (pullback.fst (pullback.fst f g ≫ f) h ≫ pullback.fst f g ≫ f)
        (pullback.fst f (pullback.fst g h ≫ g) ≫ f) (tripleProductAssoc f g h).hom
        (tripleProductAssoc_hom_comp_base f g h)
        (totalChowExteriorProduct (fieldChowSituation k) (dimensionFunction_eq_zero_of_isClosed k)
          (pullback.fst f g ≫ f) h
          (totalChowExteriorProduct (fieldChowSituation k)
            (dimensionFunction_eq_zero_of_isClosed k) f g α β) γ) =
      totalChowExteriorProduct (fieldChowSituation k) (dimensionFunction_eq_zero_of_isClosed k) f
        (pullback.fst g h ≫ g) α
        (totalChowExteriorProduct (fieldChowSituation k)
          (dimensionFunction_eq_zero_of_isClosed k) g h β γ)
Sources
LeanStacks.Chow.exteriorProduct_mem_rationalEquivalences_right · Stacks.Chow.exteriorProduct_mem_rationalEquivalences_left · Stacks.Chow.chowExteriorProduct · Stacks.Chow.bivariantToBaseEval · Stacks.Chow.bivariantToBaseEval_injective · Stacks.Chow.bivariantToBaseEval_bijective_field · Stacks.Chow.bivariantToBaseEquivField · Stacks.Chow.bivariantChowClassToBaseEquivField

Section42.62 Intersection products#

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

Tag 0FC0, the section

Tag 0FC0 in the Stacks Project.

Stacks.Chow.diagonalGysinProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionProduct.lean, line 226. The attribute's comment: “the product Δ^!(α × β), on the pullback of the diagonal rather than on Y ×_X Z, with the Gysin class Δ^! of the diagonal carried as c (Stacks 0FBR and 0FBK supply it; no product is assumed); the exterior product's instances of Stacks 02S1 are supplied by the general case of Stacks 02S1, Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_general, and are not carried; no property of the product is proved”.

Stacks Project, Tag 0FC0. The Gysin pullback Δ^!(α × β) of the exterior product along the diagonal of X, read on the pullback (Y ×_k Z) ×_{X ×_k X} X of the diagonal. This is the intersection product of Stacks 0FC0 before the identification of that pullback with Y ×_X Z; Stacks.Chow.intersectionProduct performs the identification.

It is an additive map out of CH_n(Y) ⊗_ℤ CH_m(Z), so the product it defines is ℤ-bilinear by construction; Stacks.Chow.intersectionProductBilin is that bilinear form.

The Gysin class c of the diagonal is a hypothesis: it is a single element of A^d(X ⟶ X ×_k X) depending on X alone, and it is produced from smoothness of X by Stacks.Chow.isRegularImmersion_diagonal_of_smooth together with the construction of Stacks 0FBK, which Stacks.Chow.diagonalVirtualNormalGysinClass carries out. The instances of Stacks 02S1 that the exterior product needs are not hypotheses: they are supplied by Stacks.Chow.flatPullbackFactorsThroughRationalEquivalenceOnPointClosureFibres_holds, hence ultimately by the general case of Stacks 02S1.

def diagonalGysinProduct :
    TensorProduct ℤ (chowGroup C (a ≫ sX) n) (chowGroup C (b ≫ sX) m) →+
      chowGroup C (pullback.fst (pullback.diagonal sX) (exteriorToSelfProduct C sX a b) ≫ sX)
        (n + m - d)

Stacks.Chow.intersectionProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionProduct.lean, line 257. The attribute's comment: “the intersection product α · β = Δ^!(α × β) in CH_{n+m-d}(Y ×_X Z), with Δ^! carried as c (Stacks 0FBR and 0FBK supply it; no product is assumed); the exterior product's instances of Stacks 02S1 are supplied by Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_general and the Stacks 02S2 instance for the pushforward along Y ×_X Z = (Y ×_k Z) ×_{X ×_k X} X by Stacks.Chow.properPushforwardDescends, so neither is carried; no property of the product is proved”.

Stacks Project, Tag 0FC0. The intersection product

· : CH_n(Y) ⊗_ℤ CH_m(Z) ⟶ CH_{n+m-d}(Y ×_X Z)

of Stacks 0FC0, for Y and Z locally of finite type over a scheme X whose diagonal has a Gysin class of degree d. It is the Gysin pullback of the exterior product along the diagonal, Stacks.Chow.diagonalGysinProduct, pushed forward along the identification (Y ×_k Z) ×_{X ×_k X} X ≅ Y ×_X Z the source uses.

The pushforward is along an isomorphism, so the only instance of Stacks 02S2 it needs is the one that lets proper pushforward descend to Chow groups, and that is supplied here by Stacks.Chow.properPushforwardDescends rather than assumed. The instances of Stacks 02S1 the exterior product needs are likewise supplied, by Stacks.Chow.flatPullbackFactorsThroughRationalEquivalenceOnPointClosureFibres_holds. The only hypothesis of the product is therefore the Gysin class c of the diagonal.

def intersectionProduct :
    TensorProduct ℤ (chowGroup C (a ≫ sX) n) (chowGroup C (b ≫ sX) m) →+
      chowGroup C (pullback.fst a b ≫ (a ≫ sX)) (n + m - d)

Stacks.Chow.intersectionProduct_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionProduct.lean, line 270. The attribute's comment: “the defining formula α · β = Δ^!(α × β) of the product, unfolded”.

Stacks Project, Tag 0FC0. The defining formula of the intersection product: it is the Gysin pullback of the exterior product along the diagonal, carried to Y ×_X Z.

theorem intersectionProduct_apply
    (t : TensorProduct ℤ (chowGroup C (a ≫ sX) n) (chowGroup C (b ≫ sX) m)) :
    intersectionProduct C hδ G sX a b d c n m t =
      properChowPushforward C
        (pullback.fst (pullback.diagonal sX) (exteriorToSelfProduct C sX a b) ≫ sX)
        (pullback.fst a b ≫ (a ≫ sX)) (pullbackDiagonalMapIdIso a b sX).hom
        (pullbackDiagonalMapIdIso_hom_comp_structure C sX a b) (n + m - d)
        (properPushforwardDescends C _ _ _ _ _)
        (c.cap (exteriorToSelfProduct C sX a b) (n + m)
          (chowGroupCongr C (exteriorToSelfProduct_comp_selfProductStructure C sX a b).symm
            (n + m) (chowExteriorProduct C hδ (a ≫ sX) (b ≫ sX) n m t)))

Stacks.Chow.intersectionProductBilin, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionProduct.lean, line 291. The attribute's comment: “the product as the bilinear map α ↦ β ↦ α · β, bilinear by construction, with the same carried hypotheses as Stacks.Chow.intersectionProduct”.

Stacks Project, Tag 0FC0. The intersection product as a ℤ-bilinear map

CH_n(Y) → CH_m(Z) → CH_{n+m-d}(Y ×_X Z),

which is the shape α · β is used in. Bilinearity is free: the product is an additive map out of the tensor product by construction.

def intersectionProductBilin :
    chowGroup C (a ≫ sX) n →ₗ[ℤ] chowGroup C (b ≫ sX) m →ₗ[ℤ]
      chowGroup C (pullback.fst a b ≫ (a ≫ sX)) (n + m - d)

Stacks.Chow.intersectionProductBilin_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionProduct.lean, line 299. The attribute's comment: “the bilinear form evaluates to the product on a pure tensor”.

Stacks Project, Tag 0FC0. The bilinear form of the product agrees with the product.

theorem intersectionProductBilin_apply
    (α : chowGroup C (a ≫ sX) n) (β : chowGroup C (b ≫ sX) m) :
    intersectionProductBilin C hδ G sX a b d c n m α β =
      intersectionProduct C hδ G sX a b d c n m (TensorProduct.tmul ℤ α β)

Stacks.Chow.intersectionProductOfVirtualNormalBundle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionProduct.lean, line 362. The attribute's comment: “the product α · β = Δ^!(α × β) with Δ^! the class of the diagonal built by the Stacks 0FBK construction, so no bivariant class is carried; that construction's inputs (the Stacks 0FBQ datum, Stacks 02TY bijectivity, the flat and Gysin transport laws) remain carried, while Stacks 02S1 is supplied by Stacks.Chow.flatPullbackFactorsThroughRationalEquivalence_general and Stacks 02S2 by Stacks.Chow.properPushforwardDescends, neither being carried, and no property of the product is proved”.

Stacks Project, Tag 0FC0. The intersection product of Stacks 0FC0 formed with the Gysin class of the diagonal that the construction of Stacks 0FBK produces, so that no bivariant class is assumed: the degree of the product is the rank r of the virtual normal bundle of the diagonal, which for X smooth is its relative dimension.

def intersectionProductOfVirtualNormalBundle
    (P : VirtualNormalBundleProjection (pullback.diagonal sX) q r)
    (hπ : ∀ {T : Scheme.{u}} (g : T ⟶ (pullback sX sX : Scheme.{u})) [LocallyOfFiniteType g]
      (k : ℤ), Function.Bijective (π g k))
    (hproper : PiProperNaturality C sX sN (pullback.diagonal sX) q r e π)
    (hflat : TransportFlatNaturality C G sX (selfProductStructure C sX) sN
      (pullback.diagonal sX) (diagonal_comp_selfProductStructure C sX) q hq r e E π hπ)
    (hgysin : TransportGysinNaturality C G sX (selfProductStructure C sX) sN
      (pullback.diagonal sX) (diagonal_comp_selfProductStructure C sX) q hq r e E π hπ)
    (n m : ℤ) :
    TensorProduct ℤ (chowGroup C (a ≫ sX) n) (chowGroup C (b ≫ sX) m) →+
      chowGroup C (pullback.fst a b ≫ (a ≫ sX)) (n + m - (r : ℤ))

Stacks.Chow.intersectionProductOfVirtualNormalBundleClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionProductVirtualNormalBundle.lean, line 63. The attribute's comment: “the product α · β = Δ^!(α × β) with Δ^! the class c(X → X ×_k X, 𝒩) of Stacks 0FBK for a virtual normal bundle 𝒩 of the diagonal; no property of the product is proved here”.

The intersection product α · β = Δ^!(α × β) formed with the Gysin class Δ^! = c(X ⟶ X ×_k X, 𝒩) of the diagonal; its degree is the rank r of the virtual normal bundle 𝒩.

def intersectionProductOfVirtualNormalBundleClass (n m : ℤ) :
    TensorProduct ℤ (chowGroup C (a ≫ sX) n) (chowGroup C (b ≫ sX) m) →+
      chowGroup C (pullback.fst a b ≫ (a ≫ sX)) (n + m - (r : ℤ))
Tag 0FC1, a lemma

Tag 0FC1 in the Stacks Project.

Stacks.Chow.isAssociativeIntersectionProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TripleIntersectionProduct.lean, line 656. The attribute's comment: “associativity (α·β)·γ = α·(β·γ) of the Stacks 0FC0 product over a field, via the source's five-step chain; 0FBZ comes from this repository and the chain's fibre-product identification is proved here; carried are 0FBY in both variables (only its fundamental-class case is carried here) and 0FBP (needs the class half of 0FBJ), plus 02S1 and 02S2”.

Stacks Project, Tag 0FC1. Associativity of the intersection product of Stacks 0FC0: for X a scheme over a field k whose diagonal carries a Gysin class Δ^! of degree d, and Y, Z, W locally of finite type over X,

(α · β) · γ = α · (β · γ) in CH_*(Y ×_X Z ×_X W),

read through the associator of the triple fibre product over X and the matching of the two degrees, which is Stacks.Chow.IsAssociativeIntersectionProduct.

This is the source's chain of five equalities. The two instances of Stacks 0FBY are carried, as Stacks.Chow.CommutesDiagonalCapExteriorFirst and Stacks.Chow.CommutesDiagonalCapExteriorSecond — the repository's one carrier of that tag is the fundamental-class case and does not cover either of them — and Stacks 0FBP is carried as Stacks.Chow.DiagonalGysinCommuteOnTripleProduct, whose carriers here would apply but for the class half of Stacks 0FBJ. The docstrings of those three say exactly what they assume and why none of them is this conclusion. Stacks 0FBZ, associativity of the exterior product, is proved in this repository and is consumed here as Stacks.Chow.chowExteriorProduct_assoc; Stacks 0F9Z is free, the cap operation of Stacks.Chow.BivariantClass being indexed by an arbitrary test morphism, so that Δ₁₂^! and Δ₂₃^! are cap operations of Δ^! itself and no triple self-product of X is needed; and the fibre-product identification the chain runs on is proved above, as Stacks.Chow.pullbackDiagonalExteriorTestIso with its two instances Stacks.Chow.firstPartialDiagonalPullbackIso and Stacks.Chow.secondPartialDiagonalPullbackIso.

theorem isAssociativeIntersectionProduct
    (hfirst : CommutesDiagonalCapExteriorFirst k G hpp sX a b g d Dc n m l)
    (hsecond : CommutesDiagonalCapExteriorSecond k G hpp sX a b g d Dc n m l)
    (hcommute : DiagonalGysinCommuteOnTripleProduct k G hpp sX a b g d Dc n m l) :
    IsAssociativeIntersectionProduct (fieldChowSituation k) (fun _ _ ↦ rfl) G sX a b g d Dc
      n m l hpp

Stacks.Chow.isAssociativeIntersectionProduct_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/TripleIntersectionProductExterior.lean, line 1216. The attribute's comment: “the whole statement: associativity (α·β)·γ = α·(β·γ) in CH_*(Y ×_X Z ×_X W) of the Stacks 0FC0 product for X smooth over a field of arbitrary dimension, Y, Z, W locally of finite type over X and arbitrary α, β, γ, the product Δ^!(α × β) formed with the Gysin class of the diagonal on the open and closed parts of X of constant dimension, as in Section 0FC0”.

Stacks 0FC1. Let k be a field, X smooth over k of arbitrary, not necessarily constant, dimension, and Y, Z, W locally of finite type over X. The intersection product α · β = Δ^!(α × β) of Stacks 0FC0 is formed with the Gysin class of the diagonal of Stacks 0FBR part by part, over the open and closed parts X_d of X of dimension d (Stacks.Chow.dimPartOverIntersectionProduct): for α ∈ CH_n(Y) and β ∈ CH_m(Z), α · β has component α|_{Y_d} · β|_{Z_d} ∈ CH_{n+m-d}(Y_d ×_{X_d} Z_d) over X_d, where Y_d = a⁻¹(X_d), Z_d = b⁻¹(X_d) are the parts of Y and Z over X_d. Then for γ ∈ CH_l(W)

(α · β) · γ = α · (β · γ) in CH_*(Y ×_X Z ×_X W),

component by component, read through the associator of the triple fibre product over X_d and the matching of the degrees (n + m - d) + l - d = n + (m + l - d) - d.

theorem isAssociativeIntersectionProduct_canonical
    (α : chowGroup (fieldChowSituation k) (a ≫ sX) n)
    (β : chowGroup (fieldChowSituation k) (b ≫ sX) m)
    (γ : chowGroup (fieldChowSituation k) (g ≫ sX) l) :
    (fun d : ℕ ↦ chowGroupDegreeEquiv (fieldChowSituation k)
        (pullback.fst (dimPartOverHom sX a d)
            (pullback.fst (dimPartOverHom sX b d) (dimPartOverHom sX g d) ≫
              dimPartOverHom sX b d) ≫
          (dimPartOverHom sX a d ≫ partBase sX d))
        (intersectionProductAssocDegree n m l d)
        (properChowPushforward (fieldChowSituation k)
          (pullback.fst (pullback.fst (dimPartOverHom sX a d) (dimPartOverHom sX b d) ≫
              dimPartOverHom sX a d) (dimPartOverHom sX g d) ≫
            ((pullback.fst (dimPartOverHom sX a d) (dimPartOverHom sX b d) ≫
              dimPartOverHom sX a d) ≫ partBase sX d))
          (pullback.fst (dimPartOverHom sX a d)
              (pullback.fst (dimPartOverHom sX b d) (dimPartOverHom sX g d) ≫
                dimPartOverHom sX b d) ≫
            (dimPartOverHom sX a d ≫ partBase sX d))
          (tripleProductAssoc (dimPartOverHom sX a d) (dimPartOverHom sX b d)
            (dimPartOverHom sX g d)).hom
          (tripleProductAssoc_hom_comp_structureMorphism (fieldChowSituation k) (partBase sX d)
            (dimPartOverHom sX a d) (dimPartOverHom sX b d) (dimPartOverHom sX g d))
          ((n + m - d) + l - d) (properPushforwardDescends (fieldChowSituation k) _ _ _ _ _)
          (μ (fun d ↦ pullback.fst (dimPartOverHom sX a d) (dimPartOverHom sX b d) ≫
              dimPartOverHom sX a d) (fun d ↦ dimPartOverHom sX g d)
            (fun d : ℕ ↦ n + m - d) (fun _ ↦ l)
            (fun d ↦ chowGroupCongr (fieldChowSituation k)
              (Category.assoc (pullback.fst (dimPartOverHom sX a d) (dimPartOverHom sX b d))
                (dimPartOverHom sX a d) (partBase sX d)).symm (n + m - d)
              (μ (fun d ↦ dimPartOverHom sX a d) (fun d ↦ dimPartOverHom sX b d) (fun _ ↦ n)
                (fun _ ↦ m) res[a, n, α] res[b, m, β] d))
            res[g, l, γ] d))) =
      μ (fun d ↦ dimPartOverHom sX a d)
        (fun d ↦ pullback.fst (dimPartOverHom sX b d) (dimPartOverHom sX g d) ≫
          dimPartOverHom sX b d) (fun _ ↦ n) (fun d : ℕ ↦ m + l - d) res[a, n, α]
        (fun d ↦ chowGroupCongr (fieldChowSituation k)
          (Category.assoc (pullback.fst (dimPartOverHom sX b d) (dimPartOverHom sX g d))
            (dimPartOverHom sX b d) (partBase sX d)).symm (m + l - d)
          (μ (fun d ↦ dimPartOverHom sX b d) (fun d ↦ dimPartOverHom sX g d) (fun _ ↦ m)
            (fun _ ↦ l) res[b, m, β] res[g, l, γ] d))
Tag 0FC2, a lemma

Tag 0FC2 in the Stacks Project.

Stacks.Chow.chowCohomologyCapFundamentalClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/SmoothCapFundamentalIso.lean, line 178. The attribute's comment: “the map A^p(X) → CH_{d-p}(X), c ↦ c ∩ [X]_d, for an arbitrary degree d over a general Chow situation; neither its bijectivity nor the compatibility of composition with the intersection product is covered”.

Stacks 0FC2. The map A^p(X) ⟶ CH_{d-p}(X) of Stacks 0FC2: cap product of a bivariant class for the identity of X with the fundamental class [X]_d, read through the collapse of X ×_X X onto X along its first projection.

For X smooth over a field and equidimensional of dimension d the source asserts that this map is an isomorphism. Neither that assertion nor the compatibility of composition with the intersection product is proved here; what is proved is the reduction of injectivity in Stacks.Chow.chowCohomologyCapFundamentalClass_injective_iff. See the implementation notes of this module.

def chowCohomologyCapFundamentalClass :
    chowCohomologyComponent C G sX p →+ chowGroup C sX (d - p)

Stacks.Chow.chowCohomologyCapFundamentalClass_injective_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/SmoothCapFundamentalIso.lean, line 224. The attribute's comment: “injectivity of the map c ↦ c ∩ [X]_d, reduced by Stacks 02UC to the statement that a class killing [X]_d kills the fundamental class of every integral scheme locally of finite type over X; the surjectivity of the map and the compatibility of composition with the intersection product are not covered”.

Stacks 0FC2, injectivity reduced to Stacks 02UC. The map A^p(X) ⟶ CH_{d-p}(X) of Stacks 0FC2 is injective exactly when every bivariant class killing the fundamental class [X]_d kills the fundamental class of every integral scheme locally of finite type over X.

This is the whole of what Stacks 02UC contributes to the injectivity half of Stacks 0FC2, and the right-hand side is the statement that remains: in the source it is obtained by factoring the map through A^{p-d}(X ⟶ Spec k) using Stacks 0FBT, which is not available here. The equivalence is not vacuous in either direction — the forward implication uses that the zero class kills every fundamental class, the backward one uses Stacks 02UC proper.

theorem chowCohomologyCapFundamentalClass_injective_iff :
    Function.Injective (chowCohomologyCapFundamentalClass C G sX d p) ↔
      ∀ c : chowCohomologyComponent C G sX p,
        c.cap (𝟙 X) d (selfFundamentalClass C sX d) = 0 →
          c.CapsIntegralFundamentalClassesToZero C G sX sX (𝟙 X) (Category.id_comp sX) p

Stacks.Chow.chowCohomologyCapFundamentalClass_injective_iff_hasBirationalModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/SmoothCapFundamentalIso.lean, line 245. The attribute's comment: “injectivity of the map c ↦ c ∩ [X]_d, reduced by clause (3) of Stacks 02UC to the existence of proper birational modifications capping to zero; the surjectivity of the map and the compatibility of composition with the intersection product are not covered”.

Stacks 0FC2, injectivity reduced to clause (3) of Stacks 02UC. The same reduction as Stacks.Chow.chowCohomologyCapFundamentalClass_injective_iff, with the criterion read through the birational form of Stacks 02UC: it is enough that every integral scheme locally of finite type over X admit a proper birational modification whose fundamental class the class kills.

theorem chowCohomologyCapFundamentalClass_injective_iff_hasBirationalModification :
    Function.Injective (chowCohomologyCapFundamentalClass C G sX d p) ↔
      ∀ c : chowCohomologyComponent C G sX p,
        c.cap (𝟙 X) d (selfFundamentalClass C sX d) = 0 →
          c.HasBirationalModificationCappingToZero C G sX sX (𝟙 X) (Category.id_comp sX) p

Stacks.Chow.chowCohomologyCapFundamentalClass_bijective_of_smooth_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SmoothChowCohomology.lean, line 150. The attribute's comment: “first clause; equidimensional of dimension d read as of constant relative dimension d over k; bivariant classes are those of the Gysin system of invertible modules”.

Stacks 0FC2, first clause. Let X be smooth over a field k, of constant relative dimension d, that is equidimensional of dimension d. Then

A^p(X) ⟶ CH_{d-p}(X), c ↦ c ∩ [X]_d

is bijective.

theorem chowCohomologyCapFundamentalClass_bijective_of_smooth_field (p : ℤ) :
    Function.Bijective (chowCohomologyCapFundamentalClass (fieldChowSituation k)
      (gysinSystemOfInvertible (fieldChowSituation k)) sX d p)

Stacks.Chow.chowCohomologyCapFundamentalClass_mulId_of_smooth_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SmoothChowCohomology.lean, line 167. The attribute's comment: “second clause, with the intersection product of Stacks 0FC0 formed with the Gysin class Δ^! of the diagonal; equidimensional of dimension d read as of constant relative dimension d over k”.

Stacks 0FC2, second clause. Let X be smooth over a field k, of constant relative dimension d. Via Θ : A^p(X) ⟶ CH_{d-p}(X), c ↦ c ∩ [X]_d, composition of bivariant classes becomes the intersection product of Stacks 0FC0 formed with the Gysin class Δ^! of the diagonal (Stacks 0FBR):

Θ(a · b) = Θ(a) · Θ(b).

theorem chowCohomologyCapFundamentalClass_mulId_of_smooth_field (p q : ℤ)
    (a : chowCohomologyComponent (fieldChowSituation k)
      (gysinSystemOfInvertible (fieldChowSituation k)) sX p)
    (b : chowCohomologyComponent (fieldChowSituation k)
      (gysinSystemOfInvertible (fieldChowSituation k)) sX q) :
    chowCohomologyCapFundamentalClass (fieldChowSituation k)
        (gysinSystemOfInvertible (fieldChowSituation k)) sX d (p + q)
        (a.mulId (fieldChowSituation k) sX b) =
      chowGroupDegreeEquiv (fieldChowSituation k) sX
        (by ring : ((d : ℤ) - p) + (d - q) - d = d - (p + q))
        (chowGroupSelfProductUnitCollapse (fieldChowSituation k) sX
          (((d : ℤ) - p) + (d - q) - d)
          (intersectionProduct (fieldChowSituation k) (fun _ _ ↦ rfl)
            (gysinSystemOfInvertible (fieldChowSituation k)) sX (𝟙 X) (𝟙 X) d
            (bivariantClassCongrBase (fieldChowSituation k)
              (gysinSystemOfInvertible (fieldChowSituation k)) (pullback.diagonal sX)
              (diagonal_comp_selfProductStructure (fieldChowSituation k) sX) rfl d
              (diagonalGysinClass (fieldChowSituation k) sX sX hd))
            ((d : ℤ) - p) ((d : ℤ) - q)
            (chowGroupCongr (fieldChowSituation k) (Category.id_comp sX).symm ((d : ℤ) - p)
              (chowCohomologyCapFundamentalClass (fieldChowSituation k)
                (gysinSystemOfInvertible (fieldChowSituation k)) sX d p a) ⊗ₜ[ℤ]
              chowGroupCongr (fieldChowSituation k) (Category.id_comp sX).symm ((d : ℤ) - q)
                (chowCohomologyCapFundamentalClass (fieldChowSituation k)
                  (gysinSystemOfInvertible (fieldChowSituation k)) sX d q b))))
Tag 0FFB, a lemma

Tag 0FFB in the Stacks Project.

Stacks.Chow.GysinMapExists.of_smooth_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/Factorization.lean, line 98. The attribute's comment: “the Gysin map exists for a morphism of schemes smooth over the base”.

Stacks 0FFB and Stacks 0FFC, first assertion. The Gysin map exists for a morphism f : X ⟶ Y over a base S whose source is smooth over S.

Indeed f ≫ sY is the structure morphism sX : X ⟶ S, for which the Gysin map exists because a smooth morphism is its own factorization through the identity of its source. Over a field this is the assertion of Stacks 0FFB and of Stacks 0FFC that the Gysin map exists for a morphism of schemes smooth over the field; smoothness of the target is not needed.

theorem GysinMapExists.of_smooth_source {X Y S : Scheme.{u}} (f : X ⟶ Y) (sY : Y ⟶ S)
    (sX : X ⟶ S) [Smooth sX] (hbase : f ≫ sY = sX) : GysinMapExists f

Stacks.Chow.codimensionGysin_codimensionIntersectionProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/SmoothIntersectionProductMixed.lean, line 975. The attribute's comment: “the whole statement for a morphism f of schemes smooth over a field, of arbitrary dimension: its Gysin map f^! exists and f^!(α · β) = f^!α · f^!β, for f^! the Gysin map of f itself acting part by part and products formed part by part on the open and closed parts of constant dimension”.

Stacks 0FFB: f^!(α · β) = f^!α · f^!β. Let f : X ⟶ Y be a morphism of schemes smooth over a field k, of arbitrary and not necessarily constant dimension. Then f is a local complete intersection morphism for which the Gysin map f^! of Stacks 0FF3 exists (AlgebraicGeometry.isLocalCompleteIntersectionMorphism_of_smooth_of_smooth, Stacks.Chow.GysinMapExists.of_smooth_source), and for α ∈ CH^i(Y) and β ∈ CH^j(Y)

f^!(α · β) = f^!α · f^!β in CH^{i+j}(X),

for f^! the Gysin map of f acting on classes graded by codimension (Stacks.Chow.codimensionGysin) and the intersection product Stacks.Chow.codimensionIntersectionProduct of Stacks 0FC0, formed part by part on the open and closed parts of X and Y of constant dimension.

Both sides are compared on each piece X_{d,e}, where f^! is the Gysin map of f restricted to X_{d,e} and Y_e (Stacks.Chow.dimPartPieceGysinClass): the left is f^!(α_e · β_e); the right is the restriction of a product on X_d, which is the product of the restrictions (Stacks.Chow.chowGroupRestrict_selfIntersectionProduct_canonical); and the two agree by the source's argument (Stacks.Chow.BivariantClass.capTargetHom_selfIntersectionProduct), whose inputs Stacks 0FF7 and Stacks 0FF6 for f^! on the piece are Stacks.Chow.dimPartPieceGysinClass_capTargetHom_fundamentalChowClass and Stacks.Chow.dimPartPieceGysinClass_bivariantCommute.

theorem codimensionGysin_codimensionIntersectionProduct
    (i j : ℤ) (α : codimensionChowGroup k sY i) (β : codimensionChowGroup k sY j) :
    codimensionGysin sX sY hf (i + j) (codimensionIntersectionProduct k sY i j α β) =
      codimensionIntersectionProduct k sX i j (codimensionGysin sX sY hf i α)
        (codimensionGysin sX sY hf j β)
Tag 0FFC, a lemma

Tag 0FFC in the Stacks Project.

Stacks.Chow.GysinMapExists.of_smooth_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/Factorization.lean, line 98. The attribute's comment: “the Gysin map exists for a morphism of schemes smooth over the base”.

Stacks 0FFB and Stacks 0FFC, first assertion. The Gysin map exists for a morphism f : X ⟶ Y over a base S whose source is smooth over S.

Indeed f ≫ sY is the structure morphism sX : X ⟶ S, for which the Gysin map exists because a smooth morphism is its own factorization through the identity of its source. Over a field this is the assertion of Stacks 0FFB and of Stacks 0FFC that the Gysin map exists for a morphism of schemes smooth over the field; smoothness of the target is not needed.

theorem GysinMapExists.of_smooth_source {X Y S : Scheme.{u}} (f : X ⟶ Y) (sY : Y ⟶ S)
    (sX : X ⟶ S) [Smooth sX] (hbase : f ≫ sY = sX) : GysinMapExists f

Stacks.Chow.properChowPushforward_dimensionCodimensionIntersectionProduct_codimensionGysin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/SmoothIntersectionProductMixed.lean, line 1053. The attribute's comment: “the whole statement for a proper morphism f of schemes smooth over a field, of arbitrary dimension: its Gysin map f^! exists and f_*(α · f^!β) = f_*α · β, for f^! the Gysin map of f itself acting part by part and products formed part by part on the open and closed parts of constant dimension”.

Stacks 0FFC: the projection formula f_*(α · f^!β) = f_*α · β. Let f : X ⟶ Y be a proper morphism of schemes smooth over a field k, of arbitrary and not necessarily constant dimension. Then the Gysin map f^! of Stacks 0FF3 exists (Stacks.Chow.GysinMapExists.of_smooth_source), and for α ∈ CH_n(X) and β ∈ CH^j(Y)

f_*(α · f^!β) = f_*α · β in CH_{n-j}(Y),

for f^! the Gysin map of f acting on classes graded by codimension (Stacks.Chow.codimensionGysin) and the intersection product Stacks.Chow.dimensionCodimensionIntersectionProduct of Stacks 0FC0, formed part by part on the open and closed parts of X and Y of constant dimension.

Both sides are compared on each part Y_e of Y, where f_* becomes the pushforward from f⁻¹(Y_e). Writing β_e = c ∩ [Y_e]_e (Stacks 0FC2), one has γ · β_e = c ∩ γ and c ∩ f_*α = f_*(res(c) ∩ α) (Stacks.Chow.chowCohomologyCap_properChowPushforward_restriction), and α · f^!β = res(c) ∩ α on f⁻¹(Y_e), checked on each piece X_{d,e}: there f^!β_e = res(c) ∩ [X_{d,e}]_d by Stacks 0FF6 and Stacks 0FF7 for the Gysin map of f restricted to the piece (Stacks.Chow.BivariantClass.capTargetHom_chowCohomologyCapFundamentalClass_heq, Stacks.Chow.dimPartPieceGysinClass_bivariantCommute, Stacks.Chow.dimPartPieceGysinClass_capTargetHom_fundamentalChowClass), and α · (res(c) ∩ [X_{d,e}]_d) = res(c) ∩ α by Stacks 0FC2 and the symmetry of the product.

theorem properChowPushforward_dimensionCodimensionIntersectionProduct_codimensionGysin
    (n j : ℤ) (α : chowGroup (fieldChowSituation k) sX n) (β : codimensionChowGroup k sY j) :
    properChowPushforward (fieldChowSituation k) sX sY f hf (n - j)
        (properPushforwardDescends _ _ _ _ _ _)
        (dimensionCodimensionIntersectionProduct k sX n j α (codimensionGysin sX sY hf j β)) =
      dimensionCodimensionIntersectionProduct k sY n j
        (properChowPushforward (fieldChowSituation k) sX sY f hf n
          (properPushforwardDescends _ _ _ _ _ _) α) β
Tag 0FFD, a lemma

Tag 0FFD in the Stacks Project.

Stacks.Chow.Intersection.selfIntersectionProduct_diagonalGysinClass_mk_of_cohenMacaulayAtIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Intersection/CohenMacaulayIntersectionProduct.lean, line 1036.

Stacks Project, Tag 0FFD. Let k be a field, let X be an integral scheme smooth over k of dimension dX, and let Y, Z ⊆ X be integral closed subschemes of dimensions dY and dZ. Put d = dY + dZ - dX, and assume

  1. dim(Y ∩ Z) ≤ d, and
  2. 𝒪_{Y,ξ} and 𝒪_{Z,ξ} are Cohen–Macaulay for every ξ ∈ Y ∩ Z with δ(ξ) = d.

Then [Y] · [Z] = [Y ∩ Z]_d in CH_d(X), where the intersection product Stacks.Chow.selfIntersectionProduct is formed with the Gysin class Δ^! of the diagonal of X ⟶ Spec k (Stacks 0FBR), and Y ∩ Z = Y ×_X Z is the scheme-theoretic intersection.

This is the source's proof: Y ×_k Z is pure of dimension dY + dZ, its local rings at the points of Y ∩ Z of δ-dimension d are Cohen–Macaulay by Stacks 045J, and Stacks 0FEA for Δ^! (Stacks.Chow.diagonalGysinClass_capCohenMacaulayFormula, from Stacks 0FBM at vanishing excess for its closed factor) gives Δ^! ∩ [Y ×_k Z] = [Y ∩ Z]_d. Hypothesis (1) is stated as dim(Y ∩ Z) + dX ≤ dY + dZ, which is dim(Y ∩ Z) ≤ d without the subtraction.

theorem selfIntersectionProduct_diagonalGysinClass_mk_of_cohenMacaulayAtIntersection
    {X Y Z : Scheme.{u}} (p : X ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType p] [Smooth p]
    [IsIntegral X] (i : Y ⟶ X) [IsClosedImmersion i] [IsIntegral Y] (j : Z ⟶ X)
    [IsClosedImmersion j] [IsIntegral Z] (dX dY dZ : ℕ) (d : ℤ)
    (hXdim : topologicalKrullDim X = (dX : WithBot ℕ∞))
    (hYdim : topologicalKrullDim Y = (dY : WithBot ℕ∞))
    (hZdim : topologicalKrullDim Z = (dZ : WithBot ℕ∞)) (hd : (dY : ℤ) + dZ - dX = d)
    (hIntDim : topologicalKrullDim ↑(pullback i j) + (dX : WithBot ℕ∞) ≤
      (dY : WithBot ℕ∞) + (dZ : WithBot ℕ∞))
    (hCM : CohenMacaulayAtIntersection k p i j d) :
    chowGroupDegreeEquiv (fieldChowSituation k) p hd
        (selfIntersectionProduct (fieldChowSituation k)
          (Stacks.Chow.fieldChowSituation_dimensionFunction_of_isClosed k)
          (Stacks.WeilCohomology.fieldGysinSystem k) p dX
          (diagonalGysinClassOverField k p
            (relativeDimension_of_isIntegral_of_topologicalKrullDim_eq k p hXdim)) dY dZ
          (QuotientAddGroup.mk (cycleAssociatedToClosedSubscheme (fieldChowSituation k) p i dY))
          (QuotientAddGroup.mk
            (cycleAssociatedToClosedSubscheme (fieldChowSituation k) p j dZ))) =
      QuotientAddGroup.mk (cycleAssociatedToClosedSubscheme (fieldChowSituation k) p
        (pullback.fst i j ≫ i) d)

Stacks.Chow.Intersection.diagonalPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Intersection/CohenMacaulayProperIntersection.lean, line 198. The attribute's comment: “the scheme-theoretic identification Y ∩ Z = X ×_{Δ, X ×_k X} (Y ×_k Z)”.

Stacks Project, Tag 0FFD. The scheme-theoretic identification Y ∩ Z = X ×_{Δ, X ×_k X} (Y ×_k Z) used by the source to recognise the source of the Gysin class as the intersection. It is the pullback square of Stacks 01KR expressing that Y ×_X Z ⟶ Y ×_k Z is the base change of the diagonal along Y ×_k Z ⟶ X ×_k X.

def diagonalPullbackIso (p : X ⟶ Spec (.of k)) (i : Y ⟶ X) (j : Z ⟶ X) :
    (diagonalPullback p i j) ≅ (pullback i j : Scheme.{u})

Stacks.Chow.Intersection.gysinFormulaHypotheses_of_cohenMacaulayAtIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Intersection/CohenMacaulayProperIntersection.lean, line 287. The attribute's comment: “the reduction of the lemma to Stacks 0FEA: the identification of the intersection with the diagonal pullback, and hypotheses (2), (3) and (4) of 0FEA at the diagonal of X → Spec k. Neither the conclusion [Y]·[Z] = [Y ∩ Z]_d nor 0FEA itself is stated; carries ProductStalkCohenMacaulay for Stacks 045J. The docstring says what is covered in full”.

Stacks Project, Tag 0FFD. Let k be a field, let X be an integral scheme smooth over k of dimension dX, and let Y, Z ⊆ X be integral closed subschemes of dimensions dY and dZ. Put d = dY + dZ - dX. Assume

  1. dim (Y ∩ Z) ≤ d, and
  2. 𝒪_{Y,ξ} and 𝒪_{Z,ξ} are Cohen–Macaulay for every ξ ∈ Y ∩ Z with δ(ξ) = d.

Then the hypotheses of the higher-codimension Gysin formula of Stacks 0FEA hold for the diagonal Δ : X ⟶ X ×_k X and the morphism Y ×_k Z ⟶ X ×_k X, which is what the source's proof establishes before quoting that formula to conclude [Y] · [Z] = [Y ∩ Z]_d.

What this theorem covers of Stacks 0FFD, and what it does not: it is the reduction of the lemma to Stacks 0FEA, namely the identification Y ∩ Z = X ×_{Δ, X ×_k X} (Y ×_k Z) together with the verification of hypotheses (2), (3) and (4) of 0FEA at the diagonal of X ⟶ Spec k. The conclusion [Y] · [Z] = [Y ∩ Z]_d is not stated, and neither is Stacks 0FEA itself, for the reason recorded in the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.DiagonalGysin. Hypothesis (1) of 0FEA concerns the virtual normal sheaf 𝒯_{X/k} of Stacks 0FBQ rather than the situation (X, Y, Z), so it is not among the clauses verified here. The scheme-level form of Stacks 045J that the source uses at exactly this point is taken as the hypothesis ProductStalkCohenMacaulay; it is proved in productStalkCohenMacaulay, and gysinFormulaHypotheses_of_cohenMacaulayAtIntersection' is this statement with that hypothesis discharged.

theorem gysinFormulaHypotheses_of_cohenMacaulayAtIntersection (k : Type u) [Field k]
    {X Y Z : Scheme.{u}} (p : X ⟶ Spec (.of k)) [Smooth p] [IsIntegral X]
    (i : Y ⟶ X) [IsClosedImmersion i] [IsIntegral Y]
    (j : Z ⟶ X) [IsClosedImmersion j] [IsIntegral Z]
    (dX dY dZ d : ℕ)
    (_hXdim : topologicalKrullDim X = (dX : WithBot ℕ∞))
    (hYdim : topologicalKrullDim Y = (dY : WithBot ℕ∞))
    (hZdim : topologicalKrullDim Z = (dZ : WithBot ℕ∞))
    (_hd : dY + dZ = dX + d)
    (hIntDim : topologicalKrullDim ↑(pullback i j) ≤ (d : WithBot ℕ∞))
    (hCM : CohenMacaulayAtIntersection k p i j (d : ℤ))
    (hAscent : ProductStalkCohenMacaulay k p i j) :
    GysinFormulaHypotheses k p i j dY dZ d

Stacks.Chow.Intersection.gysinFormulaHypotheses_of_cohenMacaulayAtIntersection', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Intersection/CohenMacaulayProperIntersection.lean, line 425. The attribute's comment: “the reduction of the lemma to Stacks 0FEA from hypotheses (1) and (2) alone: the identification of the intersection with the diagonal pullback, and hypotheses (2), (3) and (4) of 0FEA at the diagonal of X → Spec k. Nothing is carried. Neither the conclusion [Y]·[Z] = [Y ∩ Z]_d nor 0FEA itself is stated, and hypothesis (1) of 0FEA, about the virtual normal sheaf, is not among the clauses. The docstring says what is covered in full”.

Stacks Project, Tag 0FFD. Let k be a field, let X be an integral scheme smooth over k of dimension dX, and let Y, Z ⊆ X be integral closed subschemes of dimensions dY and dZ. Put d = dY + dZ - dX. Assume

  1. dim (Y ∩ Z) ≤ d, and
  2. 𝒪_{Y,ξ} and 𝒪_{Z,ξ} are Cohen–Macaulay for every ξ ∈ Y ∩ Z with δ(ξ) = d.

Then the hypotheses of the higher-codimension Gysin formula of Stacks 0FEA hold for the diagonal Δ : X ⟶ X ×_k X and the morphism Y ×_k Z ⟶ X ×_k X, which is what the source's proof establishes before quoting that formula to conclude [Y] · [Z] = [Y ∩ Z]_d.

This is Stacks.Chow.Intersection.gysinFormulaHypotheses_of_cohenMacaulayAtIntersection with its carried hypothesis ProductStalkCohenMacaulay discharged by Stacks.Chow.Intersection.productStalkCohenMacaulay, so hypotheses (1) and (2) of the source are the only ones it takes. It states no more than that theorem does: the conclusion [Y] · [Z] = [Y ∩ Z]_d is not stated, and neither is Stacks 0FEA itself, for the reason recorded in the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.DiagonalGysin; and hypothesis (1) of 0FEA, which concerns the virtual normal sheaf 𝒯_{X/k} of Stacks 0FBQ rather than the situation (X, Y, Z), is not among the clauses verified here.

public theorem gysinFormulaHypotheses_of_cohenMacaulayAtIntersection' (k : Type u) [Field k]
    {X Y Z : Scheme.{u}} (p : X ⟶ Spec (.of k)) [Smooth p] [IsIntegral X]
    (i : Y ⟶ X) [IsClosedImmersion i] [IsIntegral Y]
    (j : Z ⟶ X) [IsClosedImmersion j] [IsIntegral Z]
    (dX dY dZ d : ℕ)
    (hXdim : topologicalKrullDim X = (dX : WithBot ℕ∞))
    (hYdim : topologicalKrullDim Y = (dY : WithBot ℕ∞))
    (hZdim : topologicalKrullDim Z = (dZ : WithBot ℕ∞))
    (hd : dY + dZ = dX + d)
    (hIntDim : topologicalKrullDim ↑(pullback i j) ≤ (d : WithBot ℕ∞))
    (hCM : CohenMacaulayAtIntersection k p i j (d : ℤ)) :
    GysinFormulaHypotheses k p i j dY dZ d
Tag 0FFE, a lemma

Tag 0FFE in the Stacks Project.

Stacks.Chow.intersectionProduct_fundamentalChowClass_eq_pushforward_regularImmersionGysin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinLocalCompleteIntersection/RegularImmersionIntersectionProduct.lean, line 363. The attribute's comment: “the whole statement for a regular closed immersion i : Y → X with X smooth over a field, of arbitrary dimension, and Y equidimensional of dimension e: α · [Y]_e = i_*(i^!(α)) for every j and every α ∈ CH^j(X), the classes graded by codimension on the open and closed parts X_d of X of constant dimension, both sides in CH_{e-j}(X); i^! is the Gysin map of i itself acting part by part, and the product is formed part by part on the X_d”.

Stacks 0FFE: α · [Y]_e = i_*(i^!α). Let k be a field, let X be a scheme smooth over k, of arbitrary and not necessarily constant dimension, and let i : Y ⟶ X be a regular closed immersion with Y equidimensional of dimension e. Then for every α ∈ CH^j(X)

α · i_*[Y]_e = i_*(i^!α) in CH_{e-j}(X),

for · the intersection product of Section 0FC0, formed part by part on the open and closed parts X_d of X of constant dimension (Stacks.Chow.codimensionDimensionIntersectionProduct), [Y]_e the fundamental class of Stacks 0FE4, i_* proper pushforward, and i^! the Gysin map of Stacks 0FF3 of i acting part by part (Stacks.Chow.regularImmersionGysin).

Both sides are compared on each part X_d. Writing α_d = c ∩ [X_d]_d (Stacks 0FC2), the source's chain i\_*(i^!(c ∩ [X\_d]\_d)) = i\_*(c ∩ i^![X\_d]\_d) = i\_*(c ∩ [Y\_d]\_e) = c ∩ i\_*[Y\_d]\_e = α\_d · [Y\_d]\_e is Stacks 0FF6 (Stacks.Chow.regularImmersionPartGysinClass_commutesWithEveryClass), Stacks 0FF7 (Stacks.Chow.regularImmersionPartGysinClass_capTargetHom_fundamentalChowClass), the projection formula of a bivariant class (Stacks.Chow.chowCohomologyCap_properChowPushforward_restriction) and Stacks 0FC2 (Stacks.WeilCohomology.canonicalDiagonalClassFamily_capEqProduct). See the module documentation for the grading.

theorem intersectionProduct_fundamentalChowClass_eq_pushforward_regularImmersionGysin
    (hreg : Stacks.AlgebraicGeometry.RegularIdealSheaf.IsRegularImmersion i) (e : ℕ)
    (hY : RelativeDimension (i ≫ sX) e) (j : ℤ) (α : codimensionChowGroup k sX j) :
    codimensionDimensionIntersectionProduct k sX j e α
        (properChowPushforward (fieldChowSituation k) (i ≫ sX) sX i rfl e
          (properPushforwardDescends _ _ _ _ _ _)
          (fundamentalChowClass (fieldChowSituation k) (i ≫ sX) e)) =
      properChowPushforward (fieldChowSituation k) (i ≫ sX) sX i rfl (e - j)
        (properPushforwardDescends _ _ _ _ _ _) (regularImmersionGysin sX i hreg e j α)

Stacks.Chow.intersectionProduct_fundamentalChowClass_eq_pushforward_gysin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionProductRegularImmersion.lean, line 426. The attribute's comment: “alpha . i_[Y]_e = i_(i^!(alpha)), with the product of Tag 0FC0 at a = b = identity and i^! the Gysin class CHARACTERIZED by Tag 0FBK for a virtual normal bundle of rank r, the lci Gysin map not being constructed in this repository. e = d - r is FORCED by the degrees of the two sides, so nothing is lost by not binding e separately; equidimensionality of Y is the delta-dimension bound dim_delta(Y) <= e, which is WEAKER than a generic-point equality, and equidimensionality of X is not assumed, entering only through the degree of the carried diagonal class. CARRIED: the i^! half of Tag 0FF6, which is Tag 0FBP, as h0FBP; and clauses (1) and (2) of Tag 0FC2 as hA and h0FC2, neither being formalized -- 0FC2 is formalized only as the map c |-> c cap [X]_d plus injectivity reductions. PROVED here: i^![X]_d = [Y]_e (Tag 0FBM at vanishing excess, g = identity) and c cap i_beta = i_(c cap beta) (Tag 0B76 clause (1) at the test scheme identity), and the chain combining them with the three carried clauses. Also carried: 0FBM's hinj (Tag 02TY) and hcone, Tags 02S1 and 02S2, and the side conditions Tag 0FBV and 0FC0 already carry. THE TAG'S REGULARITY HYPOTHESIS IS PRESENT AS _hreg BUT UNUSED, being encoded in the virtual normal projection together with vanishing excess. The source's reduction of a non-equidimensional smooth X to its clopen constant-dimension pieces is NOT carried out, that sum being a statement about graded CH_*(X); the same limitation the tree records for 0FF7”.

Stacks 0FFE. Let i : Y ⟶ X be a closed immersion of schemes locally of finite type over the base, carrying a virtual normal bundle of constant rank r, let cd be a Gysin class of the diagonal of X of degree d — the class Δ^! through which Stacks 0FC0 defines the intersection product, of degree d for X smooth and equidimensional of dimension d — and let ci be the Gysin class i^! of Stacks 0FBK for i. Let α = c ∩ [X]_d for a bivariant class c ∈ A^p(X), and let Y have delta-dimension at most e = d - r. Then

α · i_*[Y]_e = i_*(i^!(α)) in CH_{e-p}(X),

the two sides being read on X through the collapse of X ×_X X and through the transport between the two ways of writing their common degree.

The proof is the source's: h0FC2 replaces the product by c ∩ -, Stacks.Chow.chowCohomologyCap_properChowPushforward moves i_* across c ∩ -, Stacks.Chow.closedImmersionBivariantCap_fundamentalChowClass identifies i^![X]_d with [Y]_e, and h0FBP moves i^! across c ∩ -. See the implementation notes for what each hypothesis is, and why neither carried hypothesis is the conclusion.

theorem intersectionProduct_fundamentalChowClass_eq_pushforward_gysin
    (c : chowCohomologyComponent C G sX p)
    (hinj : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C (i ≫ sX) sN i q hq r NP.flat NP.relativeDimension hdesc g k))
    {ci : BivariantClass C G (i ≫ sX) sX i rfl (r : ℤ)}
    (hci : IsVirtualNormalGysinClass C G (i ≫ sX) sX sN i rfl q hq r 0 E
      (bundleFlatPullback C (i ≫ sX) sN i q hq r NP.flat NP.relativeDimension hdesc) NP ci)
    (hY : schemeDeltaDimension C (i ≫ sX) ≤ ((d - (r : ℤ) : ℤ) : EInt))
    (_hreg : Stacks.AlgebraicGeometry.RegularIdealSheaf.IsRegularImmersion i)
    (hcone : chowGroupDegreeEquiv C (pullback.fst (q ≫ i) (𝟙 X) ≫ sN)
        (by omega : d - (0 : ℤ) = (d - (r : ℤ)) + (r : ℤ))
        (E.cap (𝟙 X) d (fundamentalChowClass C (𝟙 X ≫ sX) d)) =
      fundamentalChowClass C (pullback.fst (q ≫ i) (𝟙 X) ≫ sN) ((d - (r : ℤ)) + (r : ℤ)))
    (α : chowGroup C sX (d - p))
    (hα : chowCohomologyCap C G sX p c d (fundamentalChowClass C sX d) = α)
    (h0FBP : ∀ (k : ℤ) (x : chowGroup C sX k),
      closedImmersionBivariantCap C G sX i (r : ℤ) ci (k - p)
          (chowCohomologyCap C G sX p c k x) =
        chowGroupDegreeEquiv C (i ≫ sX) (by ring : k - (r : ℤ) - p = k - p - (r : ℤ))
          (chowCohomologyCapOnSubscheme C G sX i p c (k - (r : ℤ))
            (closedImmersionBivariantCap C G sX i (r : ℤ) ci k x)))
    (h0FC2 : ∀ β : chowGroup C sX (d - (r : ℤ)),
      chowGroupSelfProductUnitCollapse C sX ((d - p) + (d - (r : ℤ)) - d)
          (intersectionProduct C hδ G sX (𝟙 X) (𝟙 X) d cd (d - p) (d - (r : ℤ))
            (TensorProduct.tmul ℤ (chowGroupCongr C (Category.id_comp sX).symm (d - p) α)
              (chowGroupCongr C (Category.id_comp sX).symm (d - (r : ℤ)) β))) =
        chowGroupDegreeEquiv C sX
          (by ring : (d - (r : ℤ)) - p = (d - p) + (d - (r : ℤ)) - d)
          (chowCohomologyCap C G sX p c (d - (r : ℤ)) β)) :
    chowGroupSelfProductUnitCollapse C sX ((d - p) + (d - (r : ℤ)) - d)
        (intersectionProduct C hδ G sX (𝟙 X) (𝟙 X) d cd (d - p) (d - (r : ℤ))
          (TensorProduct.tmul ℤ (chowGroupCongr C (Category.id_comp sX).symm (d - p) α)
            (chowGroupCongr C (Category.id_comp sX).symm (d - (r : ℤ))
              (properChowPushforward C (i ≫ sX) sX i rfl (d - (r : ℤ)) (hpp _ _ _ _ _)
                (fundamentalChowClass C (i ≫ sX) (d - (r : ℤ))))))) =
      chowGroupDegreeEquiv C sX (by ring : (d - p) - (r : ℤ) = (d - p) + (d - (r : ℤ)) - d)
        (properChowPushforward C (i ≫ sX) sX i rfl ((d - p) - (r : ℤ)) (hpp _ _ _ _ _)
          (closedImmersionBivariantCap C G sX i (r : ℤ) ci (d - p) α))
Tag 0FFF, a lemma

Tag 0FFF in the Stacks Project.

Stacks.Chow.codimensionRationalChowEquiv_codimensionIntersectionProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionProduct.lean, line 918. The attribute's comment: “the whole lemma: for X smooth over k, quasi-compact, with affine diagonal, the identification CH^(X) ⊗ Q ≅ CH_(X) ⊗ Q carries the product of 0FC0 tensored with Q, (q ⊗ α)(q' ⊗ β) = qq' ⊗ α · β, to the product of 0FEX”.

Stacks Project, Tag 0FFF. Let k be a field and let X be a smooth scheme over k which is quasi-compact and has affine diagonal. Then the intersection product of Section 0FC0 on CH^*(X) agrees after tensoring with 𝐐 with the intersection product of Section 0FEX: the identification CH^*(X) ⊗ 𝐐 = (⨁_i CH^i(X)) ⊗ 𝐐 ≅ CH_*(X) ⊗ 𝐐 (Stacks.Chow.codimensionRationalChowEquiv) carries the product (q ⊗ α) · (q' ⊗ β) = qq' ⊗ α · β of CH^*(X) ⊗ 𝐐, with α · β ∈ CH^{i+j}(X) the product of Section 0FC0 (Stacks.Chow.codimensionIntersectionProduct) for α ∈ CH^i(X) and β ∈ CH^j(X), to the product of Section 0FEX.

theorem codimensionRationalChowEquiv_codimensionIntersectionProduct [CompactSpace X]
    [IsAffineHom (pullback.diagonal (terminal.from X))] (i j : ℤ) (q q' : ℚ)
    (a : codimensionChowGroup k sX i) (b : codimensionChowGroup k sX j) :
    haveI := isNoetherian_of_compactSpace sX
    codimensionRationalChowEquiv k sX ((q * q') ⊗ₜ[ℤ]
        DirectSum.of (codimensionChowGroup k sX) (i + j)
          (codimensionIntersectionProduct k sX i j a b)) =
      rationalIntersectionProduct (isRegular_of_smooth_over_field sX)
        (exists_bounds_relativeDimension_fieldChowSituation k sX)
        (codimensionRationalChowEquiv k sX (q ⊗ₜ[ℤ] DirectSum.of (codimensionChowGroup k sX) i a))
        (codimensionRationalChowEquiv k sX
          (q' ⊗ₜ[ℤ] DirectSum.of (codimensionChowGroup k sX) j b))
Sources
LeanStacks.Chow.diagonalGysinProduct · Stacks.Chow.intersectionProduct · Stacks.Chow.intersectionProduct_apply · Stacks.Chow.intersectionProductBilin · Stacks.Chow.intersectionProductBilin_apply · Stacks.Chow.intersectionProductOfVirtualNormalBundle · Stacks.Chow.intersectionProductOfVirtualNormalBundleClass · Stacks.Chow.isAssociativeIntersectionProduct

Section42.63 Exterior product over Dedekind domains#

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

Tag 0FC4, a lemma

Tag 0FC4 in the Stacks Project.

Stacks.Chow.exteriorProductDedekindTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekind/ChowGroups.lean, line 147. The attribute's comment: “the map CH_n(X) ⊗_ℤ CH_m(Y) → CH_{n+m-1}(X ×_S Y) is well defined, given that the cycle-level exterior product carries rational equivalences to rational equivalences in each variable (the step the source proves with the bivariant classes of Stacks 0B78, 0B79 and 0B75, none of which is in this repository)”.

The exterior product over a Dedekind base as a map out of the tensor product,

× : CH_n(X) ⊗_ℤ CH_m(Y) ⟶ CH_{n+m-1}(X ×_S Y),

determined by [X'] ⊗ [Y'] ↦ [X' ×_S Y']_{n+m-1} on integral closed subschemes X' ⊆ X and Y' ⊆ Y of delta-dimensions n and m with one of them dominating an irreducible component of the base, and by [X'] ⊗ [Y'] ↦ 0 when neither does, given that the cycle-level exterior product respects rational equivalence in each variable (hfac).

def exteriorProductDedekindTensor :
    TensorProduct ℤ (chowGroup C f n) (chowGroup C g m) →+
      chowGroup C (pullback.fst f g ≫ f) (n + m - 1)

Stacks.Chow.existsUnique_exteriorProductDedekindChowTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekind/RationalEquivalence.lean, line 926.

Let (S, δ) be as in Stacks section 42.63 — locally the spectrum of a Dedekind domain, with δ = 0 at closed points and δ = 1 elsewhere — and let X, Y be locally of finite type over S. The map × : CH_n(X) ⊗_ℤ CH_m(Y) ⟶ CH_{n+m-1}(X ×_S Y) is well defined: there is exactly one additive map out of the tensor product sending [α] ⊗ [β] to the class of the exterior product α × β of the two cycles.

theorem existsUnique_exteriorProductDedekindChowTensor (hC : IsDedekindChowBase C) :
    ∃! F : TensorProduct ℤ (chowGroup C f n) (chowGroup C g m) →+
        chowGroup C (pullback.fst f g ≫ f) (n + m - 1),
      ∀ (α : CycleGroup C f n) (β : CycleGroup C g m),
        F (TensorProduct.tmul ℤ (QuotientAddGroup.mk' (rationalEquivalences C f n) α)
            (QuotientAddGroup.mk' (rationalEquivalences C g m) β)) =
          QuotientAddGroup.mk' (rationalEquivalences C (pullback.fst f g ≫ f) (n + m - 1))
            (exteriorProductDedekindCycles C f g n m α β)

Stacks.Chow.IsDedekindChowBase.exteriorProductFactorsThroughRationalEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekind/RespectsRationalEquivalence.lean, line 1224. The attribute's comment: “the exterior product of cycles over a Dedekind base is compatible with rational equivalence in each variable; the source's bivariant classes i_* ∘ (p')^* and i_* ∘ (p')^* ∘ c are read on cycles as a flat pullback and a flat pullback of the Gysin map of a principal divisor with trivial normal bundle”.

Stacks 0FC4. Over a Dedekind base the exterior product of cycles carries rational equivalences to rational equivalences in each variable, for all X, Y locally of finite type over the base and all n, m. This discharges the hypothesis of Stacks.Chow.exteriorProductDedekindTensor.

theorem IsDedekindChowBase.exteriorProductFactorsThroughRationalEquivalence
    (hS : IsDedekindChowBase C) : ExteriorProductFactorsThroughRationalEquivalence C f g n m

Stacks.Chow.IsDedekindChowBase.exteriorProductChow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekind/RespectsRationalEquivalence.lean, line 1242. The attribute's comment: “the map CH_n(X) ⊗_ℤ CH_m(Y) → CH_{n+m-1}(X ×_S Y) is well defined, unconditionally”.

Stacks 0FC4. The exterior product on Chow groups over a Dedekind base,

× : CH_n(X) ⊗_ℤ CH_m(Y) ⟶ CH_{n+m-1}(X ×_S Y),

well defined with no hypothesis beyond the base being as in Stacks section 42.63. It is Stacks.Chow.exteriorProductDedekindTensor with its compatibility with rational equivalence supplied by Stacks.Chow.IsDedekindChowBase.exteriorProductFactorsThroughRationalEquivalence; on a pure tensor of the classes of integral closed subschemes X' and Y' of delta-dimensions n and m it is the class of [X' ×_S Y']_{n+m-1} when one of them dominates an irreducible component of the base and zero otherwise.

def IsDedekindChowBase.exteriorProductChow (hS : IsDedekindChowBase C) :
    TensorProduct ℤ (chowGroup C f n) (chowGroup C g m) →+
      chowGroup C (pullback.fst f g ≫ f) (n + m - 1)
Tag 0FC5, a lemma

Tag 0FC5 in the Stacks Project.

Stacks.Chow.bivariantChowClassCapBaseFundamentalClass_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekind/ChowCohomology.lean, line 120. The attribute's comment: “the canonical map A^p(X → S) → CH_{1-p}(X), c ↦ c ∩ [S]₁, is bijective; the components of S are curves, as in Example 02QN (for S the spectrum of a field the statement fails)”.

Bivariant classes towards a Dedekind base are Chow classes. Let (S, δ) be as in Stacks section 42.63 — locally the spectrum of a Dedekind domain, with δ = 0 at the closed points and δ = 1 elsewhere — every irreducible component of S being of dimension one, and let X be a scheme locally of finite type over S. For every p ∈ ℤ the canonical map A^p(X ⟶ S) ⟶ CH_{1-p}(X), c ↦ c ∩ [S]₁, is bijective. Here A^p(X ⟶ S) is the group of bivariant classes of Stacks 0B76 for the structure morphism of X, and c ∩ [S]₁ is read on X through X ×_S S ≅ X.

theorem bivariantChowClassCapBaseFundamentalClass_bijective :
    Function.Bijective (bivariantChowClassCapBaseFundamentalClass sX p)

Stacks.Chow.chowCohomologyDedekindEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekind/ChowCohomology.lean, line 134. The attribute's comment: “the canonical identification A^p(X → S) = CH_{1-p}(X) as an isomorphism of groups, c ↦ c ∩ [S]₁, with inverse α ↦ c_α; the components of S are curves, as in Example 02QN”.

The canonical identification A^p(X ⟶ S) = CH_{1-p}(X) over a Dedekind base whose irreducible components are curves, as an isomorphism of groups: c ↦ c ∩ [S]₁. Its inverse sends α to the class c_α with c_α ∩ α' = α × α' (chowCohomologyDedekindEquiv_symm).

def chowCohomologyDedekindEquiv (p : ℤ) (hC : IsDedekindChowBase C)
    (hdim : ∀ Z : irreducibleComponents C.S, topologicalKrullDim (Z : Set C.S) = 1) :
    BivariantChowClass C sX (𝟙 C.S) sX (Category.comp_id sX) p ≃+ chowGroup C sX (1 - p)

Stacks.Chow.bivariantCapBaseFundamentalClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekindBivariant.lean, line 69. The attribute's comment: “the canonical map A^p(X → S) → CH_{1-p}(X), c ↦ c ∩ [S]₁; the source's assertion that it is bijective is not proved here”.

The canonical map A^p(X → S) → CH_{1-p}(X), sending a bivariant class c of degree p for the structure morphism X ⟶ S to c ∩ [S]₁, read on X through the isomorphism X ×_S S ⟶ X.

def bivariantCapBaseFundamentalClass :
    BivariantClass C G sX (𝟙 C.S) sX (Category.comp_id sX) p →+ chowGroup C sX (1 - p)

Stacks.Chow.bivariantCapBaseFundamentalClass_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekindBivariantIdentification.lean, line 1130. The attribute's comment: “corrected form: the base is assumed to have no zero-dimensional component (Stacks.Chow.HasNoZeroDimensionalComponent, every closed point a proper specialization); the source admits such components, a field being a Dedekind domain, and for S = Spec k the map c ↦ c ∩ [S]₁ is zero while A^0(S → S) contains 1. Bivariant classes are those of the Gysin system of invertible modules, Stacks.Chow.gysinSystemOfInvertible”.

Stacks 0FC5, corrected form. Let (S, δ) be a base as in section 42.63 of the Stacks Project with no zero-dimensional component, and let X be locally of finite type over S. Then c ↦ c ∩ [S]₁ is a bijection A^p(X → S) → CH_{1-p}(X) for every p ∈ ℤ.

The hypothesis hS1 is the correction. A field is a Dedekind domain, so the source's statement also admits a component Spec k of S with δ ≡ 0, and there it fails: [S]₁ restricts to [Spec k]₁ = 0, so the map kills the nonzero class 1 ∈ A^0(Spec k → S).

theorem bivariantCapBaseFundamentalClass_bijective (hS : IsDedekindChowBase C)
    (hS1 : HasNoZeroDimensionalComponent C) :
    Function.Bijective
      (bivariantCapBaseFundamentalClass C (gysinSystemOfInvertible C) sX p)

Stacks.Chow.bivariantCapBaseFundamentalClassEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekindBivariantIdentification.lean, line 1142. The attribute's comment: “corrected form: the base is assumed to have no zero-dimensional component (Stacks.Chow.HasNoZeroDimensionalComponent); the identification A^p(X → S) = CH_{1-p}(X) as an isomorphism of groups, at the Gysin system of invertible modules”.

Stacks 0FC5, corrected form, as an isomorphism of groups: over a base as in section 42.63 with no zero-dimensional component, A^p(X → S) ≃+ CH_{1-p}(X), c ↦ c ∩ [S]₁.

def bivariantCapBaseFundamentalClassEquiv (hS : IsDedekindChowBase C)
    (hS1 : HasNoZeroDimensionalComponent C) :
    BivariantClass C (gysinSystemOfInvertible C) sX (𝟙 C.S) sX (Category.comp_id sX) p ≃+
      chowGroup C sX (1 - p)

Stacks.Chow.exists_isExteriorProductOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekindRepresentation/InverseMap.lean, line 116. The attribute's comment: “corrected form: the inverse α ↦ c_α acts by exterior product, c_α ∩ α' = α × α'”.

Stacks 0FC5, the inverse map, corrected form. Over a base as in section 42.63 with no zero-dimensional component, every α ∈ CH_{1-p}(X) is c_α ∩ [S]₁ for a bivariant class c_α ∈ A^p(X → S) acting by exterior product with α, c_α ∩ α' = α × α'; by Stacks.Chow.bivariantCapBaseFundamentalClass_injective it is unique.

theorem exists_isExteriorProductOverBase (hS : IsDedekindChowBase C)
    (hS1 : HasNoZeroDimensionalComponent C) (α : chowGroup C sX (1 - p)) :
    ∃ c : BivariantClass C (gysinSystemOfInvertible C) sX (𝟙 C.S) sX (Category.comp_id sX) p,
      IsExteriorProductOverBase C (gysinSystemOfInvertible C) sX (1 - p) p α c ∧
        bivariantCapBaseFundamentalClass C (gysinSystemOfInvertible C) sX p c = α
Tag 0FC6, a lemma

Tag 0FC6 in the Stacks Project.

Stacks.Chow.bivariantCommuteOverBase_of_isChowOperationGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/CommuteOverDedekindBase.lean, line 515. The attribute's comment: “the commutation c ∘ c' = c' ∘ c, read on the cap operations of the two composites, for c an integral combination of flat pullbacks towards the base, the generators of the presentation in the proof of Stacks 0FC5 other than proper pushforwards and Gysin maps; given Stacks 02S1 for every flat morphism over the base”.

Stacks 0FC6. Let (S, δ) be as in Stacks section 42.63, let X be a scheme locally of finite type over S and let c ∈ A^p(X ⟶ S). Let Y ⟶ Z be a morphism of schemes locally of finite type over S and let c' ∈ A^q(Y ⟶ Z). Then c ∘ c' = c' ∘ c: capping with c and capping with c' may be performed in either order, the two results being read on the two iterated fibre products X ×_S (Y ×_Z T) and Y ×_Z (X ×_S T) of a test scheme through the canonical comparison isomorphism.

theorem bivariantCommuteOverBase_of_isChowOperationGenerated
    (hfd : ∀ {A B : Scheme.{u}} (sA : A ⟶ C.S) [LocallyOfFiniteType sA]
      (sB : B ⟶ C.S) [LocallyOfFiniteType sB] (v : A ⟶ B) [LocallyOfFiniteType v] [Flat v]
      (hv : v ≫ sB = sA) (r : ℕ) (hr : AlgebraicGeometry.RelativeDimension v r) (k : ℤ),
      FlatPullbackFactorsThroughRationalEquivalence C sA sB v hv r hr k)
    (hgen : IsChowOperationGenerated C G sX p c) :
    BivariantCommuteOverBase C G sX sZ w p q c c'

Stacks.Chow.bivariantCommuteOverBase_of_isDedekindChowBase_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/CommuteOverDedekindBaseGeneral.lean, line 818. The attribute's comment: “the commutation c ∘ c' = c' ∘ c read on the cap operations of the two composites (Stacks.Chow.BivariantCommuteOverBase), for the bivariant classes of the Gysin system of invertible modules Stacks.Chow.gysinSystemOfInvertible”.

Let (S, δ) be as in section 42.63 of the Stacks Project, let X be a scheme locally of finite type over S and let c ∈ A^p(X ⟶ S). Let Y ⟶ Z be a morphism of schemes locally of finite type over S and let c' ∈ A^q(Y ⟶ Z). Then c ∘ c' = c' ∘ c: capping with c and capping with c' may be performed in either order, the two results being read on X ×_S (Y ×_Z T) and Y ×_Z (X ×_S T) through the canonical comparison isomorphism.

theorem bivariantCommuteOverBase_of_isDedekindChowBase_general (hS : IsDedekindChowBase C)
    {Y Z : Scheme.{u}} (sZ : Z ⟶ C.S) [LocallyOfFiniteType sZ] (w : Y ⟶ Z)
    [LocallyOfFiniteType w] (q : ℤ)
    (c : BivariantClass C (gysinSystemOfInvertible C) sX (𝟙 C.S) sX (Category.comp_id sX) p)
    (c' : BivariantClass C (gysinSystemOfInvertible C) (w ≫ sZ) sZ w rfl q) :
    BivariantCommuteOverBase C (gysinSystemOfInvertible C) sX sZ w p q c c'

Stacks.Chow.bivariantCommuteOverBase_of_isChowOperationProperGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/CommuteOverDedekindBaseProper.lean, line 365. The attribute's comment: “the commutation c ∘ c' = c' ∘ c, read on the cap operations of the two composites, for a c in the subgroup of A^p(X ⟶ S) generated by the flat pullbacks towards the base and by their proper pushforwards: of the generators the proof of Stacks 0FC5 exhibits this covers flat pullback, proper pushforward and integral combinations and not the Gysin maps; given Stacks 02S1 for flat and 02S2 for proper maps over the base”.

Stacks 0FC6. Let (S, δ) be as in Stacks section 42.63, let X be a scheme locally of finite type over S and let c ∈ A^p(X ⟶ S). Let Y ⟶ Z be a morphism of schemes locally of finite type over S and let c' ∈ A^q(Y ⟶ Z). Then c ∘ c' = c' ∘ c: capping with c and capping with c' may be performed in either order, the two results being read on the two iterated fibre products X ×_S (Y ×_Z T) and Y ×_Z (X ×_S T) of a test scheme through the canonical comparison isomorphism.

theorem bivariantCommuteOverBase_of_isChowOperationProperGenerated
    (hfd : ∀ {A B : Scheme.{u}} (sA : A ⟶ C.S) [LocallyOfFiniteType sA]
      (sB : B ⟶ C.S) [LocallyOfFiniteType sB] (v : A ⟶ B) [LocallyOfFiniteType v] [Flat v]
      (hv : v ≫ sB = sA) (r : ℕ) (hr : AlgebraicGeometry.RelativeDimension v r) (k : ℤ),
      FlatPullbackFactorsThroughRationalEquivalence C sA sB v hv r hr k)
    (hgen : IsChowOperationProperGenerated C G hpp sX p c) :
    BivariantCommuteOverBase C G sX sZ w p q c c'

Stacks.Chow.BivariantChowClass.comp_comm_of_isDedekindChowBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekind/CommuteCompositeGeneral.lean, line 304. The attribute's comment: “c ∘ c' = c' ∘ c in A^{p+q}(X ×_S Y → Z) for c ∈ A^p(X → S) and c' ∈ A^q(Y → Z), the composites read as in Stacks 0FA2”.

Stacks 0FC6. Let (S, δ) be as in Stacks section 42.63 — locally the spectrum of a Dedekind domain, with δ = 0 at the closed points and δ = 1 elsewhere. Let X be a scheme locally of finite type over S and c ∈ A^p(X ⟶ S). Let f : Y ⟶ Z be a morphism of schemes locally of finite type over S and c' ∈ A^q(Y ⟶ Z). Then c ∘ c' = c' ∘ c in A^{p+q}(X ×_S Y ⟶ Z).

Here c ∘ c' = res(c) ∘ c' with res(c) ∈ A^p(X ×_S Y ⟶ Y) the restriction of c along Y ⟶ S, and c' ∘ c = res(c') ∘ res(c) with res(c) ∈ A^p(X ×_S Z ⟶ Z) the restriction of c along Z ⟶ S and res(c') ∈ A^q(Y ×_Z (X ×_S Z) ⟶ X ×_S Z) the restriction of c' along X ×_S Z ⟶ Z (Stacks 0F9Z, 0FA2). The second composite lives on Y ×_Z (X ×_S Z) and in degree q + p; it is read on X ×_S Y through the canonical isomorphism and in degree p + q.

theorem BivariantChowClass.comp_comm_of_isDedekindChowBase (hC : IsDedekindChowBase C)
    (c : BivariantChowClass C sX (𝟙 C.S) sX (Category.comp_id sX) p)
    (c' : BivariantChowClass C sY sZ f hf q) :
    (c.restrict sY (Category.comp_id sY)).comp c' =
      (((c'.restrict (pullback.snd sX sZ)
          (BivariantChowClass.restrict_structure_eq (Category.comp_id sX) sZ
            (Category.comp_id sZ))).comp
        (c.restrict sZ (Category.comp_id sZ))).degreeCongr (add_comm q p)).transport
        (comp_comp_structureMorphism_eq
          (BivariantChowClass.restrict_structure_eq (Category.comp_id sX) sY
            (Category.comp_id sY)) hf)
        (pointClassCompositeIso C sX sZ f hf) (pointClassCompositeIso_hom_comp C sX sZ f hf)
Tag 0FC7, a remark

Tag 0FC7 in the Stacks Project.

Stacks.Chow.exteriorProductDedekindChowTensor_cap_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekind/CapCommute.lean, line 801.

The exterior product over a Dedekind base commutes with capping. Let (S, δ) be as in Stacks section 42.63 — locally the spectrum of a Dedekind domain, with δ = 0 at the closed points and δ = 1 elsewhere — let X be locally of finite type over S, let Y ⟶ Z be a morphism of schemes locally of finite type over S and let c' ∈ A^q(Y ⟶ Z). Then for α ∈ CH_n(X) and β ∈ CH_m(T), t : T ⟶ Z a test scheme,

α × (c' ∩ β) = c' ∩ (α × β),

the left hand side living on X ×_S (Y ×_Z T) and the right hand side on Y ×_Z (X ×_S T), compared through the canonical isomorphism Stacks.Chow.mixedCommuteHom, and in the degrees n + (m - q) - 1 and (n + m - 1) - q. The source's statement is the case T = Z. The exterior product is the map of Stacks 0FC4 and c' ranges over the whole group A^q(Y ⟶ Z) of Stacks 0B76.

theorem exteriorProductDedekindChowTensor_cap_comm {T : Scheme.{u}} (t : T ⟶ Z)
    [LocallyOfFiniteType t] (α : chowGroup C sX n) (β : chowGroup C (t ≫ sZ) m) :
    chowPushforwardOfIso C (pullback.fst sX (pullback.fst w t ≫ (w ≫ sZ)) ≫ sX)
        (pullback.fst w (pullback.snd sX (t ≫ sZ) ≫ t) ≫ (w ≫ sZ))
        (mixedCommuteHom sX sZ w t) (mixedCommuteHom_comp_structureMorphism sX sZ w t)
        (n + (m - q) - 1)
        (exteriorProductDedekindChowTensor C sX (pullback.fst w t ≫ (w ≫ sZ)) n (m - q) hC
          (α ⊗ₜ[ℤ] c'.cap t m β)) =
      chowGroupDegreeEquiv C (pullback.fst w (pullback.snd sX (t ≫ sZ) ≫ t) ≫ (w ≫ sZ))
        (by ring : (n + m - 1) - q = n + (m - q) - 1)
        (c'.cap (pullback.snd sX (t ≫ sZ) ≫ t) (n + m - 1)
          (chowGroupCongr C
            (by rw [Category.assoc]; exact pullback.condition (f := sX) (g := t ≫ sZ))
            (n + m - 1)
            (exteriorProductDedekindChowTensor C sX (t ≫ sZ) n m hC (α ⊗ₜ[ℤ] β))))

Stacks.Chow.exteriorProductDedekindChow_cap_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekindCapCommute.lean, line 123. The attribute's comment: “the identity α × (c' ∩ β) = c' ∩ (α × β), given a bivariant class acting by exterior product with α (the inverse direction of Stacks 0FC5, absent here) and given the conclusion of Stacks 0FC6 for it, together with the rational-equivalence descent of the exterior product that Stacks 0FC4 is carried with here”.

Stacks 0FC7. Exterior product with α ∈ CH_n(X) commutes with capping by c' ∈ A^q(Y ⟶ Z): for a test scheme t : T ⟶ Z and β ∈ CH_m(T),

α × (c' ∩ β) = c' ∩ (α × β)

on X ×_S Y ×_Z T, the two iterated fibre products being compared through Stacks.Chow.mixedCommuteHom.

The hypotheses are the two inputs the remark names: hrep is the existence of the class c = c_α of Stacks 0FC5 acting by exterior product with α, and h0FC6 is the commutation of that class with c', which is the conclusion of Stacks 0FC6. See the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.ExteriorProductDedekindCapCommute.

theorem exteriorProductDedekindChow_cap_comm (hp : p = 1 - n)
    (hrep : IsExteriorProductOverBase C G sX n p α c)
    (h0FC6 : BivariantCommuteOverBase C G sX sZ w p q c c')
    {T : Scheme.{u}} (t : T ⟶ Z) [LocallyOfFiniteType t] (m : ℤ)
    (hfacY : ExteriorProductFactorsThroughRationalEquivalence C sX
      (pullback.fst w t ≫ (w ≫ sZ)) n (m - q))
    (hfacT : ExteriorProductFactorsThroughRationalEquivalence C sX (t ≫ sZ) n m)
    (β : chowGroup C (t ≫ sZ) m) :
    chowPushforwardOfIso C (pullback.fst sX (pullback.fst w t ≫ (w ≫ sZ)) ≫ sX)
        (pullback.fst w (pullback.snd sX (t ≫ sZ) ≫ t) ≫ (w ≫ sZ))
        (mixedCommuteHom sX sZ w t) (mixedCommuteHom_comp_structureMorphism sX sZ w t)
        (n + (m - q) - 1)
        (exteriorProductDedekindChow C sX (pullback.fst w t ≫ (w ≫ sZ)) n (m - q) hfacY α
          (c'.cap t m β)) =
      chowGroupDegreeEquiv C (pullback.fst w (pullback.snd sX (t ≫ sZ) ≫ t) ≫ (w ≫ sZ))
        (by ring : (n + m - 1) - q = n + (m - q) - 1)
        (c'.cap (pullback.snd sX (t ≫ sZ) ≫ t) (n + m - 1)
          (chowGroupCongr C
            (by rw [Category.assoc]; exact pullback.condition (f := sX) (g := t ≫ sZ))
            (n + m - 1) (exteriorProductDedekindChow C sX (t ≫ sZ) n m hfacT α β)))

Stacks.Chow.exteriorProductDedekindChow_cap_comm_of_isDedekindChowBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekindCapCommuteGeneral.lean, line 351. The attribute's comment: “the whole statement α × (c' ∩ β) = c' ∩ (α × β), at every test scheme T → Z, for every base as in section 42.63, including bases with zero-dimensional components (spectra of fields), for the bivariant classes of the Gysin system of invertible modules Stacks.Chow.gysinSystemOfInvertible; the exterior product is that of Stacks 0FC4, its descent discharged by Stacks.Chow.IsDedekindChowBase.exteriorProductFactorsThroughRationalEquivalence”.

Stacks 0FC7. Let (S, δ) be as in section 42.63 of the Stacks Project, let X be locally of finite type over S and α ∈ CH_n(X), let Y ⟶ Z be a morphism of schemes locally of finite type over S and c' ∈ A^q(Y ⟶ Z). Then for every test scheme t : T ⟶ Z and β ∈ CH_m(T),

α × (c' ∩ β) = c' ∩ (α × β)

on X ×_S Y ×_Z T, the two iterated fibre products being compared through Stacks.Chow.mixedCommuteHom, the exterior product being that of Stacks 0FC4.

Write α = c ∩ [S]₁ + [a₀] with c ∩ [S₀]₀ = 0 and a₀ supported over the zero-dimensional locus (Stacks.Chow.exists_bivariantCapBaseFundamentalClass_add_mk_eq). The exterior product with [a₀] vanishes, c acts by exterior product with c ∩ [S]₁, and c commutes with c' by Stacks 0FC6 (Stacks.Chow.bivariantCommuteOverBase_of_isDedekindChowBase_general), so Stacks.Chow.exteriorProductDedekindChow_cap_comm applies.

theorem exteriorProductDedekindChow_cap_comm_of_isDedekindChowBase (hS : IsDedekindChowBase C)
    {X Y Z : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sZ : Z ⟶ C.S)
    [LocallyOfFiniteType sZ] (w : Y ⟶ Z) [LocallyOfFiniteType w] (n q : ℤ) (α : chowGroup C sX n)
    (c' : BivariantClass C (gysinSystemOfInvertible C) (w ≫ sZ) sZ w rfl q)
    {T : Scheme.{u}} (t : T ⟶ Z) [LocallyOfFiniteType t] (m : ℤ) (β : chowGroup C (t ≫ sZ) m) :
    chowPushforwardOfIso C (pullback.fst sX (pullback.fst w t ≫ (w ≫ sZ)) ≫ sX)
        (pullback.fst w (pullback.snd sX (t ≫ sZ) ≫ t) ≫ (w ≫ sZ))
        (mixedCommuteHom sX sZ w t) (mixedCommuteHom_comp_structureMorphism sX sZ w t)
        (n + (m - q) - 1)
        (exteriorProductDedekindChow C sX (pullback.fst w t ≫ (w ≫ sZ)) n (m - q)
          (hS.exteriorProductFactorsThroughRationalEquivalence sX _ n (m - q)) α
          (c'.cap t m β)) =
      chowGroupDegreeEquiv C (pullback.fst w (pullback.snd sX (t ≫ sZ) ≫ t) ≫ (w ≫ sZ))
        (by ring : (n + m - 1) - q = n + (m - q) - 1)
        (c'.cap (pullback.snd sX (t ≫ sZ) ≫ t) (n + m - 1)
          (chowGroupCongr C
            (by rw [Category.assoc]; exact pullback.condition (f := sX) (g := t ≫ sZ))
            (n + m - 1) (exteriorProductDedekindChow C sX (t ≫ sZ) n m
              (hS.exteriorProductFactorsThroughRationalEquivalence sX (t ≫ sZ) n m) α β)))
Tag 0FC8, a lemma

Tag 0FC8 in the Stacks Project.

Stacks.Chow.exteriorProductDedekindChow_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekind/Associativity.lean, line 212. The attribute's comment: “associativity on Chow groups, together with the associator of the triple fibre product over the base and the agreement of the two iterated delta-dimensions; the cycle-level identity is a hypothesis, since it needs the multiplicity of a point of a triple fibre product to factor through the two iterated double products, which this repository does not have”.

Stacks 0FC8. Associativity of the exterior product over a Dedekind base, on Chow groups: for Chow classes a, b, c the two iterated exterior products agree after transport along the associator of the triple fibre product and along the equality of the two iterated delta-dimensions.

Proved from the cycle-level identity hassoc, which is the step the source leaves to "associativity of fibre product of schemes"; see the implementation notes of StacksFrontier.AlgebraicGeometry.Chow.ExteriorProductDedekind.Associativity for why that step is not formal. The remaining hypotheses are the Stacks 0FC4 descent conditions for the three exterior products involved and the Stacks 02S2 condition for the pushforward along the associator, exactly as everywhere else in this repository.

theorem exteriorProductDedekindChow_assoc
    (hXY : ExteriorProductFactorsThroughRationalEquivalence C f' g' n m)
    (hXYZ : ExteriorProductFactorsThroughRationalEquivalence C
      (pullback.fst f' g' ≫ f') h' (n + m - 1) l)
    (hYZ : ExteriorProductFactorsThroughRationalEquivalence C g' h' m l)
    (hXYZ' : ExteriorProductFactorsThroughRationalEquivalence C f'
      (pullback.fst g' h' ≫ g') n (m + l - 1))
    (hpf : ProperPushforwardFactorsThroughRationalEquivalence C
      (pullback.fst (pullback.fst f' g' ≫ f') h' ≫ (pullback.fst f' g' ≫ f'))
      (pullback.fst f' (pullback.fst g' h' ≫ g') ≫ f')
      (tripleFibreProductAssoc f' g' h').hom
      (tripleFibreProductAssoc_hom_structureMorphism f' g' h')
      (n + m - 1 + l - 1))
    (hassoc : IsExteriorProductDedekindAssociative C f' g' h' n m l)
    (α : CycleGroup C f' n) (β : CycleGroup C g' m) (γ : CycleGroup C h' l) :
    exteriorProductDedekind_degree_assoc n m l ▸
        properChowPushforward C
          (pullback.fst (pullback.fst f' g' ≫ f') h' ≫ (pullback.fst f' g' ≫ f'))
          (pullback.fst f' (pullback.fst g' h' ≫ g') ≫ f')
          (tripleFibreProductAssoc f' g' h').hom
          (tripleFibreProductAssoc_hom_structureMorphism f' g' h')
          (n + m - 1 + l - 1) hpf
          (exteriorProductDedekindChow C (pullback.fst f' g' ≫ f') h' (n + m - 1) l hXYZ
            (exteriorProductDedekindChow C f' g' n m hXY
              (QuotientAddGroup.mk' (rationalEquivalences C f' n) α)
              (QuotientAddGroup.mk' (rationalEquivalences C g' m) β))
            (QuotientAddGroup.mk' (rationalEquivalences C h' l) γ)) =
      exteriorProductDedekindChow C f' (pullback.fst g' h' ≫ g') n (m + l - 1) hXYZ'
        (QuotientAddGroup.mk' (rationalEquivalences C f' n) α)
        (exteriorProductDedekindChow C g' h' m l hYZ
          (QuotientAddGroup.mk' (rationalEquivalences C g' m) β)
          (QuotientAddGroup.mk' (rationalEquivalences C h' l) γ))

Stacks.Chow.exteriorProductDedekindChow_assoc_of_isDedekindChowBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ExteriorProductDedekind/AssociativityCycles.lean, line 1169.

Associativity of the exterior product. Let (S, δ) be as in Stacks section 42.63, let X, Y, Z be locally of finite type over S, and let a ∈ CH_n(X), b ∈ CH_m(Y), c ∈ CH_l(Z). Then (a × b) × c = a × (b × c) in CH_*(X ×_S Y ×_S Z).

The two sides live on the two bracketings (X ×_S Y) ×_S Z and X ×_S (Y ×_S Z) of the triple fibre product and in the two spellings (n + m - 1) + l - 1 and n + (m + l - 1) - 1 of the same delta-dimension, so the left side is carried across by proper pushforward along the associator of the fibre product and by the equality of the two degrees.

theorem exteriorProductDedekindChow_assoc_of_isDedekindChowBase (hC : IsDedekindChowBase C)
    (a : chowGroup C f n) (b : chowGroup C g m) (c : chowGroup C h l) :
    exteriorProductDedekind_degree_assoc n m l ▸
        properChowPushforward C
          (pullback.fst (pullback.fst f g ≫ f) h ≫ (pullback.fst f g ≫ f))
          (pullback.fst f (pullback.fst g h ≫ g) ≫ f)
          (tripleFibreProductAssoc f g h).hom
          (tripleFibreProductAssoc_hom_structureMorphism f g h)
          (n + m - 1 + l - 1)
          (properPushforwardFactorsThroughRationalEquivalence_of_isClosedImmersion
            (tripleFibreProductAssoc f g h).hom C _ _
            (tripleFibreProductAssoc_hom_structureMorphism f g h) (n + m - 1 + l - 1))
          (exteriorProductDedekindChow C (pullback.fst f g ≫ f) h (n + m - 1) l
            (exteriorProductFactorsThroughRationalEquivalence_of_isDedekindChowBase C
              (pullback.fst f g ≫ f) h (n + m - 1) l hC)
            (exteriorProductDedekindChow C f g n m
              (exteriorProductFactorsThroughRationalEquivalence_of_isDedekindChowBase C f g n m hC)
              a b) c) =
      exteriorProductDedekindChow C f (pullback.fst g h ≫ g) n (m + l - 1)
        (exteriorProductFactorsThroughRationalEquivalence_of_isDedekindChowBase C f
          (pullback.fst g h ≫ g) n (m + l - 1) hC) a
        (exteriorProductDedekindChow C g h m l
          (exteriorProductFactorsThroughRationalEquivalence_of_isDedekindChowBase C g h m l hC)
          b c)
Sources
LeanStacks.Chow.exteriorProductDedekindTensor · Stacks.Chow.existsUnique_exteriorProductDedekindChowTensor · Stacks.Chow.IsDedekindChowBase.exteriorProductFactorsThroughRationalEquivalence · Stacks.Chow.IsDedekindChowBase.exteriorProductChow · Stacks.Chow.bivariantChowClassCapBaseFundamentalClass_bijective · Stacks.Chow.chowCohomologyDedekindEquiv · Stacks.Chow.bivariantCapBaseFundamentalClass · Stacks.Chow.bivariantCapBaseFundamentalClass_bijective

Section42.64 Intersection products over Dedekind domains#

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

Tag 0FCA, a lemma

Tag 0FCA in the Stacks Project.

Stacks.Chow.IsDedekindChowBase.intersectionProduct_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionProductDedekindAssociativity.lean, line 635. The attribute's comment: “the whole statement (α·β)·γ = α·(β·γ) in CH_*(Y ×_X Z ×_X W) for X smooth over a base as in section 42.63 (zero-dimensional components allowed), of arbitrary relative dimension, Y, Z, W locally of finite type over X and arbitrary α, β, γ; the product is Δ^!(α × β) with Δ^! the Gysin class of the diagonal of Stacks 0FBR and × the exterior product of Stacks 0FC4, formed on the open and closed parts of X of constant relative dimension as in section 42.64, bivariant classes those of Stacks.Chow.gysinSystemOfInvertible”.

Stacks 0FCA. Let (S, δ) be as in section 42.63: S locally Noetherian with an open covering by spectra of Dedekind domains, δ = 0 at closed points and δ = 1 elsewhere. Let X be smooth over S, of arbitrary and not necessarily constant relative dimension, and let Y, Z, W be locally of finite type over X. As section 42.64 prescribes, the intersection product α · β = Δ^!(α × β) is formed over the open and closed parts X_e of X where X ⟶ S has relative dimension e (Stacks.WeilCohomology.dimPart), with the Gysin class Δ^! ∈ A^e(X_e ⟶ X_e ×_S X_e) of the diagonal of Stacks 0FBR: for α ∈ CH_n(Y) and β ∈ CH_m(Z) its component over X_e is α|_{Y_e} · β|_{Z_e} ∈ CH_{n+m-1-e}(Y_e ×_{X_e} Z_e), where Y_e = a⁻¹(X_e) and Z_e = b⁻¹(X_e) are the parts of Y and Z over X_e (Stacks.Chow.chowGroupDimPartOver). Then for γ ∈ CH_l(W)

(α · β) · γ = α · (β · γ) in CH_*(Y ×_X Z ×_X W),

component by component, read through the associator of the triple fibre product over X_e and the matching of the degrees (n + m - 1 - e) + l - 1 - e and n + (m + l - 1 - e) - 1 - e.

theorem IsDedekindChowBase.intersectionProduct_assoc [Smooth sX] (n m l : ℤ)
    (α : chowGroup C (a ≫ sX) n) (β : chowGroup C (b ≫ sX) m) (γ : chowGroup C (g ≫ sX) l)
    (e : ℕ) :
    chowGroupDegreeEquiv C
        (pullback.fst π[a, e] (pullback.fst π[b, e] π[g, e] ≫ π[b, e]) ≫ (π[a, e] ≫ X[e]))
        (by ring : n + m - 1 - e + l - 1 - e = n + (m + l - 1 - e) - 1 - e)
        (properChowPushforward C
          (pullback.fst (pullback.fst π[a, e] π[b, e] ≫ π[a, e]) π[g, e] ≫
            ((pullback.fst π[a, e] π[b, e] ≫ π[a, e]) ≫ X[e]))
          (pullback.fst π[a, e] (pullback.fst π[b, e] π[g, e] ≫ π[b, e]) ≫ (π[a, e] ≫ X[e]))
          (tripleProductAssoc π[a, e] π[b, e] π[g, e]).hom
          (tripleProductAssoc_hom_comp_structureMorphism C X[e] π[a, e] π[b, e] π[g, e])
          (n + m - 1 - e + l - 1 - e) (properPushforwardDescends C _ _ _ _ _)
          (hS.intersectionProduct (gysinSystemOfInvertible C) X[e]
            (pullback.fst π[a, e] π[b, e] ≫ π[a, e]) π[g, e] e Δ[e] (n + m - 1 - e) l
            (chowGroupCongr C (Category.assoc (pullback.fst π[a, e] π[b, e]) π[a, e] X[e]).symm
              (n + m - 1 - e)
              (hS.intersectionProduct (gysinSystemOfInvertible C) X[e] π[a, e] π[b, e] e Δ[e] n m
                (res[a, e, n, α] ⊗ₜ[ℤ] res[b, e, m, β])) ⊗ₜ[ℤ] res[g, e, l, γ]))) =
      hS.intersectionProduct (gysinSystemOfInvertible C) X[e] π[a, e]
        (pullback.fst π[b, e] π[g, e] ≫ π[b, e]) e Δ[e] n (m + l - 1 - e)
        (res[a, e, n, α] ⊗ₜ[ℤ]
          chowGroupCongr C (Category.assoc (pullback.fst π[b, e] π[g, e]) π[b, e] X[e]).symm
            (m + l - 1 - e)
            (hS.intersectionProduct (gysinSystemOfInvertible C) X[e] π[b, e] π[g, e] e Δ[e] m l
              (res[b, e, m, β] ⊗ₜ[ℤ] res[g, e, l, γ])))
Tag 0FCB, a lemma

Tag 0FCB in the Stacks Project.

Stacks.Chow.IsDedekindChowBase.chowCohomologyCapFundamentalClass_bijective_of_smooth_of_equidimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SmoothChowCohomologyDedekind.lean, line 160. The attribute's comment: “first clause, in full: S as in section 42.63 with field components allowed, X smooth over S and equidimensional of dimension d (every irreducible component of δ-dimension d); bivariant classes are those of the Gysin system of invertible modules, Stacks.Chow.gysinSystemOfInvertible”.

Stacks 0FCB, first clause. Let (S, δ) be a base as in section 42.63 of the Stacks Project (locally the spectrum of a Dedekind domain, fields allowed; δ = 0 at closed points and 1 elsewhere), and let X be smooth over S, equidimensional of dimension d: every irreducible component of X has δ-dimension d. Then

A^p(X) ⟶ CH_{d-p}(X), c ↦ c ∩ [X]_d,

is an isomorphism for every p ∈ ℤ.

theorem chowCohomologyCapFundamentalClass_bijective_of_smooth_of_equidimensional (d : ℕ)
    (hd : ∀ V : irreducibleComponents X,
      deltaDimension C sX ⟨V, V.2.1, isClosed_of_mem_irreducibleComponents _ V.2⟩ = d)
    (p : ℤ) :
    Function.Bijective
      (chowCohomologyCapFundamentalClass C (gysinSystemOfInvertible C) sX d p)

Stacks.Chow.IsDedekindChowBase.chowGroupRestrict_chowCohomologyCapFundamentalClass_mulId, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SmoothChowCohomologyDedekind.lean, line 237. The attribute's comment: “second clause, corrected form: Θ(a · b) = Θ(a) · Θ(b) on the part X₁ of X over the one-dimensional part of S (all of X when S has no zero-dimensional component), with the intersection product of section 42.64 formed with the Gysin class Δ^! of the diagonal; over a zero-dimensional component the clause is false as stated, see Stacks.Chow.not_chowCohomologyCapFundamentalClass_mulId_fieldChowSituation; S as in section 42.63 with field components allowed, X smooth and equidimensional of dimension e + 1”.

Stacks 0FCB, second clause, corrected form: over the one-dimensional part of the base. Let (S, δ) be a base as in section 42.63 (field components allowed), and let X be smooth over S and equidimensional of dimension e + 1. Write X₁ ⊆ X for the open and closed part over the one-dimensional part S₁ of S; it is smooth of relative dimension e over S. Then via Θ : c ↦ c ∩ [X]_{e+1} composition of bivariant classes turns into the intersection product of section 42.64 on X₁, formed with the Gysin class Δ^! of the diagonal of X₁ (Stacks 0FBR):

Θ(a · b)|_{X₁} = Θ(a)|_{X₁} · Θ(b)|_{X₁}.

When S has no zero-dimensional component, X₁ = X. Over the zero-dimensional part the clause is false as stated, the exterior product of section 42.63 vanishing there identically (Stacks.Chow.not_chowCohomologyCapFundamentalClass_mulId_fieldChowSituation); for X equidimensional of dimension 0 the part X₁ is empty.

theorem chowGroupRestrict_chowCohomologyCapFundamentalClass_mulId (e : ℕ)
    (hd : ∀ V : irreducibleComponents X,
      deltaDimension C sX ⟨V, V.2.1, isClosed_of_mem_irreducibleComponents _ V.2⟩ = e + 1)
    (p q : ℤ) (a : chowCohomologyComponent C (gysinSystemOfInvertible C) sX p)
    (b : chowCohomologyComponent C (gysinSystemOfInvertible C) sX q) :
    chowGroupRestrict C sX ((hS.oneDimensionalPartPreimage sX).ι ≫ sX)
        (hS.oneDimensionalPartPreimage sX).ι rfl ((e : ℤ) + 1 - (p + q))
        (chowCohomologyCapFundamentalClass C (gysinSystemOfInvertible C) sX (e + 1) (p + q)
          (a.mulId C sX b)) =
      chowGroupDegreeEquiv C ((hS.oneDimensionalPartPreimage sX).ι ≫ sX)
        (by ring : ((e : ℤ) + 1 - p) + ((e : ℤ) + 1 - q) - 1 - e = (e + 1) - (p + q))
        (chowGroupSelfProductUnitCollapse C ((hS.oneDimensionalPartPreimage sX).ι ≫ sX)
          (((e : ℤ) + 1 - p) + ((e : ℤ) + 1 - q) - 1 - e)
          (hS.intersectionProduct (gysinSystemOfInvertible C)
            ((hS.oneDimensionalPartPreimage sX).ι ≫ sX) (𝟙 _) (𝟙 _) e
            (bivariantClassCongrBase C (gysinSystemOfInvertible C)
              (pullback.diagonal ((hS.oneDimensionalPartPreimage sX).ι ≫ sX))
              (diagonal_comp_selfProductStructure C ((hS.oneDimensionalPartPreimage sX).ι ≫ sX))
              rfl e (diagonalGysinClass C ((hS.oneDimensionalPartPreimage sX).ι ≫ sX)
                ((hS.oneDimensionalPartPreimage sX).ι ≫ sX)
                (hS.relativeDimension_oneDimensionalPartPreimage sX e hd)))
            ((e : ℤ) + 1 - p) ((e : ℤ) + 1 - q)
            (chowGroupCongr C (Category.id_comp _).symm ((e : ℤ) + 1 - p)
              (chowGroupRestrict C sX ((hS.oneDimensionalPartPreimage sX).ι ≫ sX)
                (hS.oneDimensionalPartPreimage sX).ι rfl ((e : ℤ) + 1 - p)
                (chowCohomologyCapFundamentalClass C (gysinSystemOfInvertible C) sX (e + 1) p a))
              ⊗ₜ[ℤ] chowGroupCongr C (Category.id_comp _).symm ((e : ℤ) + 1 - q)
                (chowGroupRestrict C sX ((hS.oneDimensionalPartPreimage sX).ι ≫ sX)
                  (hS.oneDimensionalPartPreimage sX).ι rfl ((e : ℤ) + 1 - q)
                  (chowCohomologyCapFundamentalClass C (gysinSystemOfInvertible C) sX (e + 1) q
                    b)))))
Sources
LeanStacks.Chow.IsDedekindChowBase.intersectionProduct_assoc · Stacks.Chow.IsDedekindChowBase.chowCohomologyCapFundamentalClass_bijective_of_smooth_of_equidimensional · Stacks.Chow.IsDedekindChowBase.chowGroupRestrict_chowCohomologyCapFundamentalClass_mulId

Section42.67 Change of base scheme#

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

Tag 0FVG, a situation

Tag 0FVG in the Stacks Project.

Stacks.Chow.FlatBaseChangeSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/Basic.lean, line 34.

A flat morphism between two bases for Chow homology whose dimension functions differ by a fixed integer on the generic points of the irreducible components of every fibre.

structure FlatBaseChangeSituation
Tag 0FVH, a lemma

Tag 0FVH in the Stacks Project.

Stacks.Chow.deltaDimension_component_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/BaseChangeComponentDimension.lean, line 148.

In the flat base-change situation of Stacks 0FVG, if X is integral and locally of finite type over S with dim_δ(X) = k, then every irreducible component of the base change X ×_S S' has delta-dimension k + c.

theorem deltaDimension_component_baseChange (B : FlatBaseChangeSituation.{u})
    {X : Scheme.{u}} (f : X ⟶ B.base.S) [LocallyOfFiniteType f] [IsIntegral X]
    (k : ℤ) (hk : schemeDeltaDimension B.base f = (k : EInt))
    (Z : irreducibleComponents (pullback f B.g : Scheme.{u})) :
    deltaDimension B.baseChange (pullback.snd f B.g)
        ⟨Z, Z.2.1,
          isClosed_of_mem_irreducibleComponents
            (Z : Set (pullback f B.g : Scheme.{u})) Z.2⟩ =
      k + B.c
Tag 0FVI, a lemma

Tag 0FVI in the Stacks Project.

Stacks.Chow.schemeDeltaDimension_baseChange_closedSubscheme_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/Dimension.lean, line 245. The attribute's comment: “part (1): dimension bound”.

Stacks 0FVI, part (1), dimension bound. In the flat base-change situation of Stacks 0FVG, the base change Z' = Z ×_X X' of a closed subscheme Z ⊆ X of delta-dimension at most k is a closed subscheme of X' = X ×_S S' of delta-dimension at most k + c.

theorem schemeDeltaDimension_baseChange_closedSubscheme_le (B : FlatBaseChangeSituation.{u})
    {X Z : Scheme.{u}} (f : X ⟶ B.base.S) [LocallyOfFiniteType f] (i : Z ⟶ X)
    [IsClosedImmersion i] {k : ℤ}
    (hZ : schemeDeltaDimension B.base (i ≫ f) ≤ (k : EInt)) :
    schemeDeltaDimension B.baseChange
        (pullback.snd i (pullback.fst f B.g) ≫ pullback.snd f B.g) ≤ ((k + B.c : ℤ) : EInt)

Stacks.Chow.schemeDeltaDimension_baseChange_support_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/Dimension.lean, line 264. The attribute's comment: “part (2): support dimension bound”.

Stacks 0FVI, part (2), dimension bound. In the flat base-change situation of Stacks 0FVG, if a coherent sheaf on X has support of delta-dimension at most k, then the support of its base change to X' = X ×_S S' has delta-dimension at most k + c.

Every point of the support of the base change lies over the support of the sheaf, so part (1) for the reduced support bounds the relative dimension there.

theorem schemeDeltaDimension_baseChange_support_le (B : FlatBaseChangeSituation.{u})
    {X : Scheme.{u}} (f : X ⟶ B.base.S) [LocallyOfFiniteType f] (F : X.Modules)
    [F.IsCoherent] {k : ℤ}
    (hFk : schemeDeltaDimension B.base ((reducedSupport F).subschemeι ≫ f) ≤ (k : EInt)) :
    letI : IsLocallyNoetherian (pullback f B.g : Scheme.{u}) :=
      LocallyOfFiniteType.isLocallyNoetherian (pullback.snd f B.g)
    letI : ((Scheme.Modules.pullback (pullback.fst f B.g)).obj F).IsCoherent :=
      AlgebraicGeometry.isCoherent_pullback (pullback.fst f B.g) F
    schemeDeltaDimension B.baseChange
        ((reducedSupport ((Scheme.Modules.pullback (pullback.fst f B.g)).obj F)).subschemeι ≫
          pullback.snd f B.g) ≤ ((k + B.c : ℤ) : EInt)

Stacks.Chow.baseChangeCyclePullback_cycleAssociatedToCoherentSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/Dimension.lean, line 379. The attribute's comment: “part (2): cycle identity”.

Stacks 0FVI, part (2), cycle identity. In the flat base-change situation of Stacks 0FVG, the base change of the cycle of a coherent sheaf F on X whose support has delta-dimension at most k is the cycle of the base change of F:

g^*[F]_k = [F']_{k + c}.

The two sides are compared at one point x' of X' at a time. If x' has relative dimension other than k + c both vanish, the left one because the base-change multiplicity is formed only in that degree. If x' lies off the support of F' then its image lies off the support of F, since the support of a pullback is the inverse image of the support, so the coefficient of [F]_k already vanishes there. In the remaining case the relative dimension of the image is forced to be exactly k, because it is at most k on the support of F while the relative dimension of x' exceeds it by at most c; the two multiplicities are then length_A M * length_B (B / 𝔪_A B) and length_B (B ⊗_A M) for A = 𝒪_{X, x}, B = 𝒪_{X', x'} and M = F_x, equal by Stacks 02M1.

theorem baseChangeCyclePullback_cycleAssociatedToCoherentSheaf (B : FlatBaseChangeSituation.{u})
    {X : Scheme.{u}} (f : X ⟶ B.base.S) [LocallyOfFiniteType f] (F : X.Modules) [F.IsCoherent]
    (k : ℤ) (hFk : schemeDeltaDimension B.base ((reducedSupport F).subschemeι ≫ f) ≤ (k : EInt)) :
    letI : IsLocallyNoetherian (pullback f B.g : Scheme.{u}) :=
      LocallyOfFiniteType.isLocallyNoetherian (pullback.snd f B.g)
    letI : ((Scheme.Modules.pullback (pullback.fst f B.g)).obj F).IsCoherent :=
      AlgebraicGeometry.isCoherent_pullback (pullback.fst f B.g) F
    baseChangeCyclePullback B f k (cycleAssociatedToCoherentSheaf B.base f F k hFk) =
      cycleAssociatedToCoherentSheaf B.baseChange (pullback.snd f B.g)
        ((Scheme.Modules.pullback (pullback.fst f B.g)).obj F) (k + B.c)
        (schemeDeltaDimension_baseChange_support_le B f F hFk)

Stacks.Chow.baseChangeCyclePullback_cycleAssociatedToClosedSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/Dimension.lean, line 496. The attribute's comment: “part (1): cycle identity”.

Stacks 0FVI, part (1), cycle identity. In the flat base-change situation of Stacks 0FVG, the base change of the cycle of a closed subscheme Z ⊆ X of delta-dimension at most k is the cycle of the base change Z' = Z ×_X X':

g^*[Z]_k = [Z']_{k + c}.

By Stacks 02QY both cycles are cycles of coherent sheaves, namely of i_* 𝒪_Z and of i'_* 𝒪_{Z'}, so part (2) reduces the claim to the flat base change of i_* 𝒪_Z being i'_* 𝒪_{Z'}.

theorem baseChangeCyclePullback_cycleAssociatedToClosedSubscheme (B : FlatBaseChangeSituation.{u})
    {X Z : Scheme.{u}} (f : X ⟶ B.base.S) [LocallyOfFiniteType f] (i : Z ⟶ X)
    [IsClosedImmersion i] (k : ℤ)
    (hZ : schemeDeltaDimension B.base (i ≫ f) ≤ (k : EInt)) :
    baseChangeCyclePullback B f k (cycleAssociatedToClosedSubscheme B.base f i k) =
      cycleAssociatedToClosedSubscheme B.baseChange (pullback.snd f B.g)
        (pullback.snd i (pullback.fst f B.g)) (k + B.c)

Declarations registered for the tag:

Tag 0FVJ, a lemma

Tag 0FVJ in the Stacks Project.

Stacks.Chow.baseChangeCyclePullback_maps_rationalEquivalences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/ChowPullback.lean, line 291. The attribute's comment: “preservation of rational equivalence”.

Stacks Project, Tag 0FVJ, preservation of rational equivalence. In a flat base-change situation with dimension shift c, the base-change homomorphism on cycle groups carries k-cycles rationally equivalent to zero on X to (k + c)-cycles rationally equivalent to zero on X' = X ×_S S'.

By Stacks 02S4 part (4) such a cycle is the total fibre difference of a locally finite family of integral closed subschemes of X ×_S 𝐏¹_S, each of relative dimension k + 1 at its generic points and contained in neither distinguished section. Its base change is the total fibre difference of the base-changed family, which is again locally finite, and each member of the base-changed family satisfies the hypotheses of Stacks 02S5 over the new base: the dimension bounds are those of StacksFrontier.AlgebraicGeometry.Chow.ChangeBaseScheme.FamilyDimension, and the condition on associated points holds because the projection to the original member is flat. The individual equivalences are summed by Stacks.Chow.rationallyEquivalentToZero_finsum, the carriers of the members forming a locally finite family.

theorem baseChangeCyclePullback_maps_rationalEquivalences (k : ℤ) :
    rationalEquivalences B.base f k ≤
      (rationalEquivalences B.baseChange (pullback.snd f B.g) (k + B.c)).comap
        (baseChangeCyclePullback B f k)

Stacks.Chow.baseChangeChowPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/ChowPullback.lean, line 348. The attribute's comment: “induced map on Chow groups”.

Stacks Project, Tag 0FVJ, the map on Chow groups. The homomorphism g^* : CH_k(X) ⟶ CH_{k+c}(X ×_S S') induced on Chow groups by the base-change homomorphism on cycle groups, which preserves rational equivalence by Stacks.Chow.baseChangeCyclePullback_maps_rationalEquivalences.

def baseChangeChowPullback (k : ℤ) :
    chowGroup B.base f k →+ chowGroup B.baseChange (pullback.snd f B.g) (k + B.c)
Tag 0FVK, a lemma

Tag 0FVK in the Stacks Project.

Stacks.Chow.flat_relativeDimension_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FlatPullback.lean, line 135. The attribute's comment: “flatness and relative dimension of the base-changed morphism”.

Stacks 0FVK. In a flat base-change situation, the base change of a morphism locally of finite type and flat of relative dimension r is again locally of finite type and flat of relative dimension r.

Flatness and local finite type are stable under base change, and the relative dimension is Stacks 02NK.

theorem flat_relativeDimension_baseChange (B : FlatBaseChangeSituation.{u}) {Y X : Scheme.{u}}
    (sY : Y ⟶ B.base.S) (sX : X ⟶ B.base.S) (f : Y ⟶ X) [LocallyOfFiniteType f] [Flat f]
    (f' : (pullback sY B.g : Scheme.{u}) ⟶ (pullback sX B.g : Scheme.{u}))
    (hsq : IsPullback (pullback.fst sY B.g) f' f (pullback.fst sX B.g))
    (r : ℕ) (hf : AlgebraicGeometry.RelativeDimension f r) :
    letI : LocallyOfFiniteType f' :=
      MorphismProperty.of_isPullback hsq (P := @LocallyOfFiniteType) inferInstance
    Flat f' ∧ AlgebraicGeometry.RelativeDimension f' r

Stacks.Chow.baseChange_flatPullback_cycles, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FlatPullback.lean, line 419. The attribute's comment: “commuting diagram of cycle groups”.

Stacks 0FVK. The square of cycle groups commutes: base change after flat pullback is flat pullback after base change, as homomorphisms Z_k(X) ⟶ Z_{k+c+r}(Y').

The two composites land in cycle groups of degree (k + r) + c and (k + c) + r, so the statement is heterogeneous; its content is the coefficient identity Stacks.Chow.baseChangeCyclePullback_flatPullback_apply.

theorem baseChange_flatPullback_cycles
    (B : FlatBaseChangeSituation.{u}) {Y X : Scheme.{u}}
    (sY : Y ⟶ B.base.S) [LocallyOfFiniteType sY] (sX : X ⟶ B.base.S) [LocallyOfFiniteType sX]
    (f : Y ⟶ X) [LocallyOfFiniteType f] [Flat f] (hbase : f ≫ sX = sY)
    (f' : (pullback sY B.g : Scheme.{u}) ⟶ (pullback sX B.g : Scheme.{u}))
    [LocallyOfFiniteType f'] [Flat f']
    (hbase' : f' ≫ pullback.snd sX B.g = pullback.snd sY B.g)
    (hcomm : pullback.fst sY B.g ≫ f = f' ≫ pullback.fst sX B.g)
    (r : ℕ) (hf : AlgebraicGeometry.RelativeDimension f r)
    (hf' : AlgebraicGeometry.RelativeDimension f' r) (k : ℤ) :
    HEq ((baseChangeCyclePullback B sY (k + (r : ℤ))).comp
          (flatPullback B.base sY sX f hbase r hf k))
      ((flatPullback B.baseChange (pullback.snd sY B.g) (pullback.snd sX B.g) f' hbase' r hf'
          (k + B.c)).comp (baseChangeCyclePullback B sX k))

Stacks.Chow.baseChange_flatPullback_chow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FlatPullback.lean, line 446. The attribute's comment: “commuting diagram of Chow groups”.

Stacks 0FVK. The square of Chow groups commutes: base change after flat pullback is flat pullback after base change, as homomorphisms A_k(X) ⟶ A_{k+c+r}(Y').

This is the image of Stacks.Chow.baseChange_flatPullback_cycles under the quotient maps, which is why the source says it suffices to prove the square of cycle groups.

theorem baseChange_flatPullback_chow
    (B : FlatBaseChangeSituation.{u}) {Y X : Scheme.{u}}
    (sY : Y ⟶ B.base.S) [LocallyOfFiniteType sY] (sX : X ⟶ B.base.S) [LocallyOfFiniteType sX]
    (f : Y ⟶ X) [LocallyOfFiniteType f] [Flat f] (hbase : f ≫ sX = sY)
    (f' : (pullback sY B.g : Scheme.{u}) ⟶ (pullback sX B.g : Scheme.{u}))
    [LocallyOfFiniteType f'] [Flat f']
    (hbase' : f' ≫ pullback.snd sX B.g = pullback.snd sY B.g)
    (hcomm : pullback.fst sY B.g ≫ f = f' ≫ pullback.fst sX B.g)
    (r : ℕ) (hf : AlgebraicGeometry.RelativeDimension f r)
    (hf' : AlgebraicGeometry.RelativeDimension f' r) (k : ℤ) :
    HEq ((flatBaseChangeChowPullback B sY (k + (r : ℤ))
            (baseChangeFactorsThroughRationalEquivalence B sY (k + (r : ℤ)))).comp
          (flatPullbackChow B.base sY sX f hbase r hf k
            (flatPullbackFactorsThroughRationalEquivalence_general B.base sY sX f hbase r hf k)))
      ((flatPullbackChow B.baseChange (pullback.snd sY B.g) (pullback.snd sX B.g) f' hbase' r hf'
          (k + B.c)
          (flatPullbackFactorsThroughRationalEquivalence_general B.baseChange
            (pullback.snd sY B.g) (pullback.snd sX B.g) f' hbase' r hf' (k + B.c))).comp
        (flatBaseChangeChowPullback B sX k
          (baseChangeFactorsThroughRationalEquivalence B sX k)))
Tag 0FVL, a lemma

Tag 0FVL in the Stacks Project.

Stacks.Chow.isProper_baseChangeMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/ProperPushforward.lean, line 131. The attribute's comment: “properness of the base change”.

Stacks Project, Tag 0FVL, properness of the base change. In a flat base change of Chow situations, the morphism f' : Y ×_S S' ⟶ X ×_S S' induced by a proper morphism f : Y ⟶ X is proper, because it is a base change of f and properness is stable under base change.

theorem isProper_baseChangeMorphism [IsProper f] : IsProper (baseChangeMorphism B sX f)

Stacks.Chow.properPushforward_baseChangeCyclePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/ProperPushforward.lean, line 309. The attribute's comment: “the cycle square”.

Stacks Project, Tag 0FVL, the cycle square. In a flat base change of Chow situations, proper pushforward commutes with the base-change map on cycle groups: for f : Y ⟶ X proper over the base S, the square whose horizontal maps are g^* : Z_k(Y) ⟶ Z_{k+c}(Y') and g^* : Z_k(X) ⟶ Z_{k+c}(X') and whose vertical maps are f_* and f'_* commutes.

Both routes are additive, and a cycle agrees, on the part of its support lying over a single point x of X', with a finite sum of prime cycles: that part is the intersection of the support with the fibre of the proper morphism f over the image of x, hence finite, and both routes read the coefficient at x only off that part. So it suffices to treat a prime cycle, which is the fundamental cycle of the reduced closure of a point and so is covered by the case of a closed subscheme.

Coherence of the direct image of a coherent module under a proper morphism to a locally Noetherian scheme is Stacks.Chow.forall_properDirectImageIsCoherent, the first assertion of Stacks 02O5.

theorem properPushforward_baseChangeCyclePullback
    [LocallyOfFiniteType sX] [IsProper f] (k : ℤ)
    (z : CycleGroup B.base (f ≫ sX) k) :
    letI : IsProper (baseChangeMorphism B sX f) := isProper_baseChangeMorphism B sX f
    properPushforward B.baseChange (pullback.snd (f ≫ sX) B.g) (pullback.snd sX B.g)
        (baseChangeMorphism B sX f) (baseChangeMorphism_comp_snd B sX f) (k + B.c)
        (baseChangeCyclePullback B (f ≫ sX) k z) =
      baseChangeCyclePullback B sX k (properPushforward B.base (f ≫ sX) sX f rfl k z)

Stacks.Chow.properChowPushforward_baseChangeChowPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/ProperPushforward.lean, line 418. The attribute's comment: “the Chow square, in the generality of every Chow base-change map induced by the cycle-level one of Tag 0FVJ; instantiated at that map, with nothing left to supply, by properChowPushforward_baseChangeChowPullback_of_baseChangeChowPullback below”.

Stacks Project, Tag 0FVL, the Chow square. In a flat base change of Chow situations, proper pushforward commutes with the base-change map on Chow groups: for f : Y ⟶ X proper over the base S, the square whose horizontal maps are g^* : CH_k(Y) ⟶ CH_{k+c}(Y') and g^* : CH_k(X) ⟶ CH_{k+c}(X') and whose vertical maps are f_* and f'_* commutes.

Every class is the class of a cycle, and on classes of cycles both routes are the class of the corresponding route on cycles, so this follows from the cycle square.

The base-change map on Chow groups is a parameter gChow of this statement rather than a fixed map, constrained by hgChow to be induced by the base-change map on cycle groups. This is a generality, not an assumption: quantifying over every such map is stronger than the source's statement, and the map itself exists, so Stacks.Chow.properChowPushforward_baseChangeChowPullback_of_baseChangeChowPullback below instantiates this at the base-change map of Stacks 0FVJ and is unconditional. Coherence of the direct image of a coherent module under a proper morphism to a locally Noetherian scheme is Stacks.Chow.forall_properDirectImageIsCoherent, the first assertion of Stacks 02O5.

theorem properChowPushforward_baseChangeChowPullback
    [LocallyOfFiniteType sX] [IsProper f] (k : ℤ)
    (gChow : ∀ {W : Scheme.{u}} (sW : W ⟶ B.base.S) [LocallyOfFiniteType sW] (j : ℤ),
      chowGroup B.base sW j →+ chowGroup B.baseChange (pullback.snd sW B.g) (j + B.c))
    (hgChow : ∀ {W : Scheme.{u}} (sW : W ⟶ B.base.S) [LocallyOfFiniteType sW] (j : ℤ)
      (a : CycleGroup B.base sW j),
      gChow sW j (QuotientAddGroup.mk' (rationalEquivalences B.base sW j) a) =
        QuotientAddGroup.mk' (rationalEquivalences B.baseChange (pullback.snd sW B.g) (j + B.c))
          (baseChangeCyclePullback B sW j a))
    (w : chowGroup B.base (f ≫ sX) k) :
    letI : IsProper (baseChangeMorphism B sX f) := isProper_baseChangeMorphism B sX f
    properChowPushforward B.baseChange (pullback.snd (f ≫ sX) B.g) (pullback.snd sX B.g)
        (baseChangeMorphism B sX f) (baseChangeMorphism_comp_snd B sX f) (k + B.c)
        (properPushforwardFactorsThroughRationalEquivalence_of_isProper B.baseChange
          (pullback.snd (f ≫ sX) B.g) (pullback.snd sX B.g) (baseChangeMorphism B sX f)
          (baseChangeMorphism_comp_snd B sX f) (k + B.c))
        (gChow (f ≫ sX) k w) =
      gChow sX k (properChowPushforward B.base (f ≫ sX) sX f rfl k
        (properPushforwardFactorsThroughRationalEquivalence_of_isProper B.base (f ≫ sX) sX f rfl
          k) w)

Stacks.Chow.properChowPushforward_baseChangeChowPullback_of_baseChangeChowPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/ProperPushforward.lean, line 460. The attribute's comment: “the Chow square for the base-change map of Tag 0FVJ”.

Stacks Project, Tag 0FVL, the Chow square for the base-change map of Stacks 0FVJ. In a flat base change of Chow situations, proper pushforward commutes with the base-change map g^* : CH_k(X) ⟶ CH_{k+c}(X ×_S S') of Stacks 0FVJ: for f : Y ⟶ X proper over the base S, the square whose horizontal maps are those base-change maps for Y and for X and whose vertical maps are f_* and f'_* commutes.

This is the Chow square with its Chow base-change map supplied rather than assumed: the map is Stacks.Chow.baseChangeChowPullback, and it meets the characterization of the general statement because Stacks.Chow.baseChangeChowPullback_mk says it sends the class of a cycle to the class of the base change of that cycle. Coherence of the direct image of a coherent module under a proper morphism to a locally Noetherian scheme is Stacks.Chow.forall_properDirectImageIsCoherent, the first assertion of Stacks 02O5.

theorem properChowPushforward_baseChangeChowPullback_of_baseChangeChowPullback
    [LocallyOfFiniteType sX] [IsProper f] (k : ℤ)
    (w : chowGroup B.base (f ≫ sX) k) :
    letI : IsProper (baseChangeMorphism B sX f) := isProper_baseChangeMorphism B sX f
    properChowPushforward B.baseChange (pullback.snd (f ≫ sX) B.g) (pullback.snd sX B.g)
        (baseChangeMorphism B sX f) (baseChangeMorphism_comp_snd B sX f) (k + B.c)
        (properPushforwardFactorsThroughRationalEquivalence_of_isProper B.baseChange
          (pullback.snd (f ≫ sX) B.g) (pullback.snd sX B.g) (baseChangeMorphism B sX f)
          (baseChangeMorphism_comp_snd B sX f) (k + B.c))
        (baseChangeChowPullback B (f ≫ sX) k w) =
      baseChangeChowPullback B sX k (properChowPushforward B.base (f ≫ sX) sX f rfl k
        (properPushforwardFactorsThroughRationalEquivalence_of_isProper B.base (f ≫ sX) sX f rfl
          k) w)
Tag 0FVM, a lemma

Tag 0FVM in the Stacks Project.

Stacks.Chow.baseChange_firstChernClassCapChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FirstChernClass.lean, line 562.

[Stacks, Tag 0FVM]. In the flat base-change situation of [Stacks, Tag 0FVG] let X be locally of finite type over S, let X' = X ×_S S' be the base change by S' ⟶ S, and let ℒ be an invertible 𝒪_X-module with base change ℒ' on X'. Then the square

CH_{k+1}(X) --g^*--> CH_{k+1+c}(X') |c₁(ℒ) ∩ - |c₁(ℒ') ∩ - CH_k(X) --g^*--> CH_{k+c}(X')

of Chow groups commutes, g^* being the base-change map of [Stacks, Tag 0FVJ].

The cap product of [Stacks, Tag 02TI] is indexed by the degree of its value, so the top row is written at k + 1; the source states the square for every k ∈ ℤ, so nothing is lost. The transport between the two spellings (k + 1) + c and (k + c) + 1 of the degree of the base change of the top-left corner is Stacks.Chow.chowGroupCast. The module ℒ' is (D.baseChange g).L, which is the pullback g^*ℒ by Stacks.LineBundle.Situation.baseChange_L.

Proof. Let p : Tot(ℒ) ⟶ X be the line bundle attached to ℒ with zero section o. By clause (5) of [Stacks, Tag 0F96], o_*α = -p^*(c₁(ℒ) ∩ α). Applying g^* and using [Stacks, Tag 0FVL] on o and [Stacks, Tag 0FVK] on p turns this into

õ_*(g^*α) = -p̃^*(g^*(c₁(ℒ) ∩ α))

on the fibre product Tot(ℒ) ×_S S', where õ and p̃ are the base changes of o and p. On the other hand Stacks.Chow.zeroSectionBaseChange_chowPushforward_eq_neg — clause (5) for ℒ', transported along Tot(ℒ') ≅ Tot(ℒ) ×_S S' — gives

õ_*(g^*α) = -p̃^*(c₁(ℒ') ∩ g^*α).

So p̃^* takes the same value on the two classes to be identified, and p̃^* is injective by Stacks.Chow.injective_flatPullbackChow_totalSpaceBaseChangeMorphism.

theorem baseChange_firstChernClassCapChow (k : ℤ) (α : chowGroup B.base sX (k + 1)) :
    firstChernClassCapChow B.baseChange (k + B.c) (pullback.snd sX B.g)
        (baseChangeSituation B D sX).L
        (chowGroupCast B.baseChange (pullback.snd sX B.g)
          (show k + 1 + B.c = k + B.c + 1 from by omega)
          (baseChangeChowPullback B sX (k + 1) α)) =
      baseChangeChowPullback B sX k (firstChernClassCapChow B.base k sX D.L α)
Tag 0FVN, a lemma

Tag 0FVN in the Stacks Project.

Stacks.Chow.baseChange_chowCohomologyCap_chernClassOfLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/GenuineChernClasses.lean, line 307.

[Stacks, Tag 0FVN]. Let g : S' ⟶ S be a flat base change of Chow situations with dimension shift c ([Stacks, Tag 0FVG]), let X be locally of finite type over S with base change X' = X ×_S S', and let ℰ be a finite locally free 𝒪_X-module of rank r with base change ℰ' on X'. Then for every i the square

CH_k(X) --g^*--> CH_{k+c}(X') |c_i(ℰ) ∩ - |c_i(ℰ') ∩ - CH_{k-i}(X) --g^*--> CH_{k+c-i}(X')

commutes, where c_i ∈ A^i is the Chern class of [Stacks, Tag 0ESW], built from the classes of [Stacks, Tag 0B7H] (zero for i > r), and g^* is the map of [Stacks, Tag 0FVJ]. For i ≤ r the cap products are those of [Stacks, Tag 02U6] (Stacks.Chow.baseChange_chernCap).

theorem baseChange_chowCohomologyCap_chernClassOfLocallyFree (i : ℕ) (k : ℤ)
    (α : chowGroup B.base sX k) :
    letI := AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.isFiniteLocallyFree E r
    haveI := AlgebraicGeometry.isFiniteLocallyFreeOfRank_pullback (pullback.fst sX B.g) E r
    letI := AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.isFiniteLocallyFree
      ((Scheme.Modules.pullback (pullback.fst sX B.g)).obj E) r
    chowCohomologyCap B.baseChange (gysinSystemOfInvertible B.baseChange) (pullback.snd sX B.g)
        (i : ℤ)
        (SectionZeroScheme.chernClassOfLocallyFree
          ((Scheme.Modules.pullback (pullback.fst sX B.g)).obj E) B.baseChange
          (pullback.snd sX B.g) i) (k + B.c) (baseChangeChowPullback B sX k α) =
      chowGroupCast B.baseChange (pullback.snd sX B.g)
        (show k - (i : ℤ) + B.c = k + B.c - (i : ℤ) from by omega)
        (baseChangeChowPullback B sX (k - (i : ℤ))
          (chowCohomologyCap B.base (gysinSystemOfInvertible B.base) sX (i : ℤ)
            (SectionZeroScheme.chernClassOfLocallyFree E B.base sX i) k α))
Tag 0FVP, a lemma

Tag 0FVP in the Stacks Project.

Stacks.Chow.composed_dimensionFunction_eq_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FlatBaseChangeComposition.lean, line 209. The attribute's comment: “part (1): the composite dimension shift is the sum of the two shifts”.

Stacks Project, Tag 0FVP, part (1). For composable flat base changes of Chow situations with dimension shifts B.c and c', every generic point s'' of the fibre of g' ≫ B.g over s satisfies δ''(s'') = δ(s) + (B.c + c').

theorem composed_dimensionFunction_eq_add (s : B.base.S)
    (s'' : genericPoints ((g' ≫ B.g) ⁻¹' {s} : Set C.S)) :
    C.dimensionFunction s''.1.1 = B.base.dimensionFunction s + (B.c + c')

Stacks.Chow.baseChangeCyclePullbackSquare_comp_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FlatBaseChangeComposition.lean, line 396. The attribute's comment: “part (2): pullback on cycle groups respects composition, coefficientwise”.

Stacks Project, Tag 0FVP, part (2). The pullbacks on cycle groups of two composable flat base changes compose to the pullback of the composite, read coefficientwise.

Both composites send a cycle z to a multiple of the coefficient of z at the image point x of the given point, the factor depending only on the point. If x does not have relative dimension k then every k-cycle vanishes there and both sides are zero. Otherwise the fundamental cycle of the reduced closure of x is a k-cycle with coefficient one at x, so the two factors agree by Stacks.Chow.comp_cycleAssociatedToClosedSubscheme_coeff.

theorem baseChangeCyclePullbackSquare_comp_apply (k : ℤ) (z : CycleGroup B.base f k) (y : Y'') :
    (baseChangeCyclePullbackSquare (FlatBaseChangeSituation.second B C g' c' hg') q sq' (k + B.c)
        (baseChangeCyclePullbackSquare B f sq k z)).1 y =
      (baseChangeCyclePullbackSquare (FlatBaseChangeSituation.comp B C g' c' hg') f
        (sq'.paste_horiz sq) k z).1 y

Stacks.Chow.baseChangeCyclePullbackSquare_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FlatBaseChangeComposition.lean, line 437. The attribute's comment: “part (2): pullback on cycle groups respects composition”.

Stacks Project, Tag 0FVP, part (2). The pullbacks on cycle groups of two composable flat base changes compose to the pullback of the composite.

theorem baseChangeCyclePullbackSquare_comp (k : ℤ) :
    (baseChangeCyclePullbackSquare (FlatBaseChangeSituation.second B C g' c' hg') q sq'
          (k + B.c)).comp (baseChangeCyclePullbackSquare B f sq k) =
      ((cycleGroupCongrDegree C q'
          (show k + (B.c + c') = k + B.c + c' from (add_assoc k B.c c').symm)).toAddMonoidHom).comp
        (baseChangeCyclePullbackSquare (FlatBaseChangeSituation.comp B C g' c' hg') f
          (sq'.paste_horiz sq) k)

Stacks.Chow.baseChangeChowPullbackSquare_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FlatBaseChangeComposition.lean, line 453. The attribute's comment: “part (3): pullback on Chow groups respects composition”.

Stacks Project, Tag 0FVP, part (3). The pullbacks on Chow groups of two composable flat base changes compose to the pullback of the composite: both are induced by the corresponding pullbacks on cycle groups, which compose by Stacks.Chow.baseChangeCyclePullbackSquare_comp.

theorem baseChangeChowPullbackSquare_comp (k : ℤ) :
    (baseChangeChowPullbackSquare (FlatBaseChangeSituation.second B C g' c' hg') q sq'
          (k + B.c)).comp (baseChangeChowPullbackSquare B f sq k) =
      ((chowGroupCongrDegree C q'
          (show k + (B.c + c') = k + B.c + c' from (add_assoc k B.c c').symm)).toAddMonoidHom).comp
        (baseChangeChowPullbackSquare (FlatBaseChangeSituation.comp B C g' c' hg') f
          (sq'.paste_horiz sq) k)
Tag 0FVQ, a lemma

Tag 0FVQ in the Stacks Project.

Stacks.Chow.FilteredBaseChangeSystem.exists_stageChowPullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FilteredLimitChow.lean, line 346. The attribute's comment: “Chow groups, surjectivity: every k-cycle class on X' comes from some X_i”.

Stacks Project, Tag 0FVQ, surjectivity for Chow groups. Every k-cycle class on X' is the image of a k-cycle class on X_i for some finite stage i.

theorem exists_stageChowPullback_eq (k : ℤ)
    (α : chowGroup s.limitBaseChange.baseChange
      (pullback.snd s.X.hom s.limitBaseChange.g) k) :
    ∃ (i : I) (β : chowGroup (s.stageSituation i)
      (pullback.snd s.X.hom (s.stageToBase i)) k),
      s.stageChowPullback i k β = α

Stacks.Chow.FilteredBaseChangeSystem.exists_transitionChowPullback_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FilteredLimitChow.lean, line 626. The attribute's comment: “Chow groups, eventual injectivity: a k-cycle class on X_j killed by base change to X' is killed by some transition X_i -> X_j”.

Stacks Project, Tag 0FVQ, eventual injectivity for Chow groups. A k-cycle class on X_j whose image in CH_k(X') vanishes is annihilated by the comparison homomorphism along some transition X_i ⟶ X_j.

theorem exists_transitionChowPullback_eq_zero (j : I) (k : ℤ)
    (β : chowGroup (s.stageSituation j) (pullback.snd s.X.hom (s.stageToBase j)) k)
    (hβ : s.stageChowPullback j k β = 0) :
    ∃ (i : I) (f : i ⟶ j), s.transitionChowPullback f k β = 0

Stacks.Chow.FilteredBaseChangeSystem.exists_stageCyclePullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FilteredLimitCycles.lean, line 374. The attribute's comment: “cycle groups, surjectivity: every k-cycle on X' is the image of a k-cycle on X_i”.

Stacks Project, Tag 0FVQ, surjectivity for cycle groups. Every k-cycle on X' is the image of a k-cycle on X_i for some finite stage i.

Since X' is quasi-compact the cycle has finite support, so it is a finite integral combination of fundamental cycles of integral closed subschemes of X'. Each of those descends to a finite stage by Stacks.Chow.FilteredBaseChangeSystem.exists_stage_cycleAssociatedToClosedSubscheme, and the index category being cofiltered, one stage serves for all of them at once.

theorem exists_stageCyclePullback_eq (k : ℤ)
    (z : CycleGroup s.limitBaseChange.baseChange (pullback.snd s.X.hom s.limitBaseChange.g) k) :
    ∃ (i : I) (w : CycleGroup (s.stageSituation i) (pullback.snd s.X.hom (s.stageToBase i)) k),
      s.stageCyclePullback i k w = z

Stacks.Chow.FilteredBaseChangeSystem.exists_transitionCyclePullback_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FilteredLimitCycles.lean, line 448. The attribute's comment: “cycle groups, eventual injectivity: a k-cycle on X_j killed by base change to X' is killed by some transition X_i -> X_j”.

Stacks Project, Tag 0FVQ, eventual injectivity for cycle groups. A k-cycle on X_j whose image in Z_k(X') vanishes is annihilated by the transition to some finite stage X_i ⟶ X_j.

A point of X_j carrying a nonzero coefficient cannot lie in the image of X': otherwise the base-changed cycle would have a nonzero coefficient at a generic point of the inverse image of the reduced closure of that point, by Stacks.Chow.eq_zero_of_baseChangeCyclePullback_eq_zero_of_mem_range. The cycle has finite support because X_j is quasi-compact, and X' is the limit of the X_i along affine transition morphisms, so finitely many points outside the image of X' are already outside the image of a single X_i; every coefficient of the transition of the cycle to that stage is a coefficient of the cycle at a point of that image, hence vanishes.

theorem exists_transitionCyclePullback_eq_zero (j : I) (k : ℤ)
    (z : CycleGroup (s.stageSituation j) (pullback.snd s.X.hom (s.stageToBase j)) k)
    (hz : s.stageCyclePullback j k z = 0) :
    ∃ (i : I) (f : i ⟶ j), s.transitionCyclePullback f k z = 0

Stacks.Chow.FilteredBaseChangeSystem.exists_projectiveLineStageCyclePullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/FilteredLimitProjectiveLine.lean, line 294. The attribute's comment: “cycle groups, surjectivity for the projective line family”.

Stacks Project, Tag 0FVQ, surjectivity for the projective-line family. Every k-cycle on X' ×_{S'} 𝐏¹_{S'} is the image of a k-cycle on X_i ×_{S_i} 𝐏¹_{S_i} for some finite stage i.

theorem exists_projectiveLineStageCyclePullback_eq (k : ℤ)
    (z : CycleGroup s.limitBaseChange.baseChange
      (pullback.fst (pullback.snd s.X.hom s.limitBaseChange.g)
        (relativeProjectiveLine s.limitBaseChange.baseChange.S ↘
          s.limitBaseChange.baseChange.S) ≫ pullback.snd s.X.hom s.limitBaseChange.g) k) :
    ∃ (i : I) (c : CycleGroup (s.stageSituation i)
      (pullback.fst (pullback.snd s.X.hom (s.stageToBase i))
        (relativeProjectiveLine (s.diagram.obj i) ↘ s.diagram.obj i) ≫
          pullback.snd s.X.hom (s.stageToBase i)) k),
      s.projectiveLineStageCyclePullback i k c = z
Sources
LeanStacks.Chow.FlatBaseChangeSituation · Stacks.Chow.deltaDimension_component_baseChange · Stacks.Chow.schemeDeltaDimension_baseChange_closedSubscheme_le · Stacks.Chow.schemeDeltaDimension_baseChange_support_le · Stacks.Chow.baseChangeCyclePullback_cycleAssociatedToCoherentSheaf · Stacks.Chow.baseChangeCyclePullback_cycleAssociatedToClosedSubscheme · AlgebraicGeometry.isCoherent_pullback · Stacks.Chow.baseChangeCyclePullback_maps_rationalEquivalences

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.