42.54 Higher codimension gysin… to 42.58 Rational intersection…

Section42.54 Higher codimension gysin homomorphisms#

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

Tag 0FBJ, a lemma

Tag 0FBJ in the Stacks Project.

Stacks.Chow.VirtualNormalBundle.baseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleBaseChange.lean, line 522.

Stacks 0FBJ. For a cartesian square of schemes whose horizontal arrows i : Z ⟶ X and i' : Z' ⟶ X' are immersions, the pullback g^* 𝒩 of a virtual normal bundle 𝒩 for Z in X is a virtual normal bundle for Z' in X': it is finite locally free, and the surjection (g^* 𝒩)^∨ ⟶ 𝒞_{Z'/X'} is the composite of the base-change isomorphism (g^* 𝒩)^∨ ≅ g^* (𝒩^∨), the pullback of the given surjection, and the surjection g^* 𝒞_{Z/X} ⟶ 𝒞_{Z'/X'} of [Stacks Project, Tag 0473].

def VirtualNormalBundle.baseChange {Z X Z' X' : Scheme.{u}} (i : Z ⟶ X) (i' : Z' ⟶ X')
    [IsImmersion i] [IsImmersion i'] (g : Z' ⟶ Z) (f : X' ⟶ X)
    (sq : IsPullback i' g f i) (N : VirtualNormalBundle i) : VirtualNormalBundle i'

Tag 0FBK, a lemma

Tag 0FBK in the Stacks Project.

Stacks.Chow.completedVirtualNormalGysinClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedVirtualNormalBundleClass.lean, line 251. The attribute's comment: “the bivariant class c(Z → X, 𝒩) ∈ A^*(Z → X)^∧ of a virtual normal bundle 𝒩 of arbitrary rank for a closed immersion Z → X”.

Stacks 0FBK, the class c(Z ⟶ X, 𝒩) ∈ A^*(Z ⟶ X)^∧ of a virtual normal bundle 𝒩 of arbitrary rank for a closed immersion i : Z ⟶ X. On a connected component Z_a of Z, on which 𝒩 has constant rank r_a, it is the class c(Z_a ⟶ U_a, 𝒩|_{Z_a}) ∘ (U_a ⟶ X_b)^* of degree r_a, for the open U_a = X_b ∖ i(Z ∖ Z_a) of the connected component X_b of X containing i(Z_a), through which Z_a ⟶ X_b factors as the closed immersion Z_a ⟶ U_a cut out by the base change of i.

def completedVirtualNormalGysinClass (𝒩 : VirtualNormalBundle i) :
    completedBivariantGroup C (gysinSystemOfInvertible C) sZ sX i hi

Stacks.Chow.completedBivariantRestriction_completedVirtualNormalGysinClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedVirtualNormalBundleClassBaseChange.lean, line 1345. The attribute's comment: “base change: the restriction of c(Z → X, 𝒩) ∈ A^(Z → X)^∧ along X' → X is c(Z ×_X X' → X', g^𝒩), for 𝒩 of arbitrary rank”.

Stacks 0FBK, the base-change clause, for a virtual normal sheaf of arbitrary rank. For f : X' ⟶ X locally of finite type, the restriction (Stacks 0F9Z) of c(Z ⟶ X, 𝒩) ∈ A^*(Z ⟶ X)^∧ along f is c(Z ×_X X' ⟶ X', g^*𝒩), for the virtual normal sheaf g^*𝒩 of Stacks 0FBJ. Both are read degree by degree (Stacks 0FE0), and in each degree the cap operations agree by Stacks.Chow.completedVirtualNormalGysinClass_cap_baseChange.

theorem completedBivariantRestriction_completedVirtualNormalGysinClass (C : ChowSituation.{u})
    {Z X X' : Scheme.{u}} (sZ : Z ⟶ C.S) [LocallyOfFiniteType sZ] (sX : X ⟶ C.S)
    [LocallyOfFiniteType sX] (i : Z ⟶ X) [IsClosedImmersion i] (hi : i ≫ sX = sZ)
    (f : X' ⟶ X) [LocallyOfFiniteType f] (𝒩 : VirtualNormalBundle i) :
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI : IsLocallyNoetherian X' := LocallyOfFiniteType.isLocallyNoetherian (f ≫ sX)
    haveI : IsLocallyNoetherian (pullback i f) :=
      LocallyOfFiniteType.isLocallyNoetherian (pullback.fst i f ≫ sZ)
    completedBivariantRestrictionViaSequence C sZ sX i hi f
        (completedVirtualNormalGysinClass C sZ sX i hi 𝒩) =
      completedVirtualNormalGysinClass C (pullback.fst i f ≫ sZ) (f ≫ sX) (pullback.snd i f)
        (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f)
        (baseChangeVirtualNormalBundle i f 𝒩)

Stacks.Chow.IsVirtualNormalGysinClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleClass.lean, line 312. The attribute's comment: “the characterizing relation p^ ∘ c = ι_ ∘ j^ ∘ C of the construction, on a degree-r bivariant class for r the rank of 𝒩, with ι_ j^* C carried as E (Stacks 0F9J, 0FBG, 0FBH absent) and the flat pullback of the bundle projection carried as π (Stacks 0B78 holds at the other pullback); the bivariance laws and the Stacks 0FBJ base change are not proved”.

Stacks 0FBK. The relation p^* ∘ c(Z ⟶ X, 𝒩) = ι_* ∘ j^* ∘ C that the construction preceding Stacks 0FBK defines the class by, written on cap operations: on every test scheme g : T ⟶ X and in every degree, capping with c and then applying the flat pullback π of the bundle projection is capping with the class E = ι_* ∘ j^* ∘ C.

The construction's own formulation is that c ∩ α is the unique β with p^* β = ι_* j^* (C ∩ α), which is this equality together with the injectivity of π of Stacks 02TY. The class c ranges over A^r(Z ⟶ X) for r the constant rank of 𝒩, which is the last clause of Stacks 0FBK.

The virtual normal bundle enters through the setting argument _P, which is what restricts the relation to the situation of Stacks 0FBK: it may be formed only when i admits a virtual normal bundle of constant rank r whose vector bundle projection is q. The relation itself is a condition on c alone, so _P does not occur in it.

def IsVirtualNormalGysinClass (_P : VirtualNormalBundleProjection i q r)
    (c : BivariantClass C G sZ sX i hi (r : ℤ)) : Prop

Stacks.Chow.eq_of_isVirtualNormalGysinClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleClass.lean, line 324. The attribute's comment: “uniqueness: the characterizing relation determines the class in A^r(Z ⟶ X), given injectivity of π (Stacks 02TY)”.

Stacks 0FBK. The relation determines the class: two bivariant classes of degree r for Z ⟶ X which both satisfy it are equal. This is what makes c(Z ⟶ X, 𝒩) well defined, and it is the content of the construction that does not depend on the class existing. Only injectivity of π is used, which is the half of Stacks 02TY that the uniqueness assertion of the construction rests on.

theorem eq_of_isVirtualNormalGysinClass (P : VirtualNormalBundleProjection i q r)
    (hπ : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective (π g k))
    {c c' : BivariantClass C G sZ sX i hi (r : ℤ)}
    (h : IsVirtualNormalGysinClass C G sZ sX sN i hi q hq r e E π P c)
    (h' : IsVirtualNormalGysinClass C G sZ sX sN i hi q hq r e E π P c') : c = c'

Stacks.Chow.virtualNormalGysinCap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleClass.lean, line 339. The attribute's comment: “the prescribed cap operation α ↦ β of the construction, as the inverse of π (Stacks 02TY) applied to the cap operation of E”.

The cap operation the construction preceding Stacks 0FBK prescribes: α ↦ β where β is the unique class with p^* β = ι_* j^* (C ∩ α), that is (p^*)^{-1} ∘ (ι_* ∘ j^* ∘ C). The inverse exists by Stacks 02TY, carried as bijectivity of π.

def virtualNormalGysinCap
    (hπ : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Bijective (π g k))
    {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ) :
    chowGroup C (g ≫ sX) k →+ chowGroup C (pullback.fst i g ≫ sZ) (k - (r : ℤ))

Stacks.Chow.pi_virtualNormalGysinCap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleClass.lean, line 351. The attribute's comment: “the prescribed cap operation satisfies the characterizing relation”.

The prescribed cap operation satisfies the characterizing relation, p^* β = ι_* j^* (C ∩ α). So the relation is a consistent condition on cap operations, and the only thing a bivariant class satisfying it adds to the prescribed operation is bivariance.

theorem pi_virtualNormalGysinCap
    (hπ : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Bijective (π g k))
    {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
    (α : chowGroup C (g ≫ sX) k) :
    π g k (virtualNormalGysinCap C G sZ sX sN i hi q hq r e E π hπ g k α) = E.cap g k α

Stacks.Chow.isVirtualNormalGysinClass_iff_cap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleClass.lean, line 366. The attribute's comment: “the relation holds exactly for a class whose cap operation is the prescribed one”.

Stacks 0FBK. A bivariant class of degree r for Z ⟶ X satisfies the characterizing relation exactly when its cap operation is the prescribed one. Together with Stacks.Chow.eq_of_isVirtualNormalGysinClass this says that the construction leaves no freedom: the class, if it exists, is the bivariant class whose cap operation is Stacks.Chow.virtualNormalGysinCap.

theorem isVirtualNormalGysinClass_iff_cap_eq (P : VirtualNormalBundleProjection i q r)
    (hπ : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Bijective (π g k))
    (c : BivariantClass C G sZ sX i hi (r : ℤ)) :
    IsVirtualNormalGysinClass C G sZ sX sN i hi q hq r e E π P c ↔
      ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
        (α : chowGroup C (g ≫ sX) k),
        c.cap g k α = virtualNormalGysinCap C G sZ sX sN i hi q hq r e E π hπ g k α

Stacks.Chow.virtualNormalGysinClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleClass.lean, line 528. The attribute's comment: “the bivariant element of A^r(Z ⟶ X) prescribed by the construction, with its proper-pushforward law proved from the same law for E and Stacks 02RG for the bundle base-change square; the flat and Gysin transport laws are carried as named hypotheses, as for the library's own rank class at Tag 0ESW”.

Stacks 0FBK. The bivariant class c(Z ⟶ X, 𝒩) ∈ A^r(Z ⟶ X) of the construction preceding Stacks 0FBK: the prescribed cap operation (p^*)^{-1} ∘ (ι_* ∘ j^* ∘ C) together with the three naturality laws of Stacks 0B76.

The proper-pushforward law is proved, from the corresponding law of E and Stacks.Chow.PiProperNaturality: this is the source's "since both ι_* ∘ j^* ∘ C and p^* are bivariant", carried out. The flat and Gysin laws are carried as hypotheses, in the idiom the library uses for its own rank class at Stacks 0ESW.

The library is not of one mind about attaching a @[stacks] attribute to a class that carries laws this way, and the choice made here is deliberate. The rank class of Stacks 0ESW is tagged, with the carrying disclosed in its key; the first Chern class built the same way in StacksFrontier.AlgebraicGeometry.Chow.Bivariant.FirstChernClass is deliberately left untagged, under a section heading saying so. The attribute below follows the rank class: what it claims is the statement as written, hypotheses included, and the hypotheses are named in the signature and disclosed in the key, so nothing is hidden by tagging it. A reader who prefers the stricter convention loses only the attribute, not the mathematics.

Its cap operation satisfies the characterizing relation, by Stacks.Chow.isVirtualNormalGysinClass_virtualNormalGysinClass, so by Stacks.Chow.eq_of_isVirtualNormalGysinClass it is the class of the construction.

def virtualNormalGysinClass (_P : VirtualNormalBundleProjection i q r)
    (hpp : ProperPushforwardDescends C)
    (hπ : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Bijective (π g k))
    (hproper : PiProperNaturality C sZ sN i q r e π)
    (hflat : TransportFlatNaturality C G sZ sX sN i hi q hq r e E π hπ)
    (hgysin : TransportGysinNaturality C G sZ sX sN i hi q hq r e E π hπ) :
    BivariantClass C G sZ sX i hi (r : ℤ)

Stacks.Chow.isVirtualNormalGysinClass_virtualNormalGysinClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleClass.lean, line 559. The attribute's comment: “the constructed element of A^r(Z ⟶ X) satisfies the characterizing relation, hence is the one the construction prescribes”.

Stacks 0FBK. The constructed class satisfies the characterizing relation p^* ∘ c = ι_* ∘ j^* ∘ C. With Stacks.Chow.eq_of_isVirtualNormalGysinClass this identifies it as the class c(Z ⟶ X, 𝒩) of the construction, and not merely as some element of A^r(Z ⟶ X).

theorem isVirtualNormalGysinClass_virtualNormalGysinClass
    (P : VirtualNormalBundleProjection i q r) (hpp : ProperPushforwardDescends C)
    (hπ : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Bijective (π g k))
    (hproper : PiProperNaturality C sZ sN i q r e π)
    (hflat : TransportFlatNaturality C G sZ sX sN i hi q hq r e E π hπ)
    (hgysin : TransportGysinNaturality C G sZ sX sN i hi q hq r e E π hπ) :
    IsVirtualNormalGysinClass C G sZ sX sN i hi q hq r e E π P
      (virtualNormalGysinClass C G sZ sX sN i hi q hq r e E π P hpp hπ hproper hflat hgysin)

Stacks.Chow.virtualNormalBundleClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleClassConstruction.lean, line 356. The attribute's comment: “the bivariant class c(Z → X, 𝒩) ∈ A^r(Z → X) of a virtual normal bundle 𝒩 of constant rank r for a closed immersion Z → X”.

Stacks 0FBK, the class c(Z ⟶ X, 𝒩) ∈ A^r(Z ⟶ X) of a virtual normal bundle 𝒩 of constant rank r for a closed immersion i : Z ⟶ X: the unique bivariant class with p^* ∘ c = ι_* ∘ j^* ∘ C, the division of Stacks.Chow.virtualNormalConeClass by the flat pullback p^* along the bundle projection.

def virtualNormalBundleClass (𝒩 : VirtualNormalBundle i) (r : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} 𝒩.bundle r] :
    BivariantClass C (gysinSystemOfInvertible C) sZ sX i hi (r : ℤ)

Stacks.Chow.projectionPullbackClass_comp_virtualNormalBundleClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleClassConstruction.lean, line 381. The attribute's comment: “the construction: p^ ∘ c(Z → X, 𝒩) = i_ ∘ j^* ∘ C in A⁰(N → X), for 𝒩 of constant rank r”.

Stacks 0FBK, the defining relation p^* ∘ c(Z ⟶ X, 𝒩) = ι_* ∘ j^* ∘ C, as an equality of bivariant classes in A⁰(N ⟶ X): the composite (Stacks 0B75) of the class with the flat pullback along the bundle projection is the class ι_* ∘ j^* ∘ C, read in degree -r + r = 0.

theorem projectionPullbackClass_comp_virtualNormalBundleClass (𝒩 : VirtualNormalBundle i) (r : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} 𝒩.bundle r] :
    bivariantCompositeOfInvertible C (𝒩.projection ≫ sZ) sZ sX 𝒩.projection i rfl hi (-(r : ℤ))
        r (𝒩.projectionPullbackClass C sZ i r) (virtualNormalBundleClass C sZ sX i hi 𝒩 r) =
      BivariantClass.copy C (gysinSystemOfInvertible C) (𝒩.projection ≫ sZ) sX rfl
        (comp_comp_structureMorphism_eq rfl hi) (comp_comp_structureMorphism_eq rfl hi)
        (by ring : (0 : ℤ) = -(r : ℤ) + r) (virtualNormalConeClass C sZ sX i hi 𝒩)

Stacks.Chow.eq_virtualNormalBundleClass_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleClassConstruction.lean, line 395. The attribute's comment: “uniqueness: c(Z → X, 𝒩) is the only class in A^r(Z → X) with p^ ∘ c = i_ ∘ j^* ∘ C (Stacks 02TY)”.

Stacks 0FBK, uniqueness: a bivariant class c ∈ A^r(Z ⟶ X) is c(Z ⟶ X, 𝒩) exactly when p^* ∘ c = ι_* ∘ j^* ∘ C.

theorem eq_virtualNormalBundleClass_iff (𝒩 : VirtualNormalBundle i) (r : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} 𝒩.bundle r]
    (c : BivariantClass C (gysinSystemOfInvertible C) sZ sX i hi (r : ℤ)) :
    c = virtualNormalBundleClass C sZ sX i hi 𝒩 r ↔
      bivariantCompositeOfInvertible C (𝒩.projection ≫ sZ) sZ sX 𝒩.projection i rfl hi
          (-(r : ℤ)) r (𝒩.projectionPullbackClass C sZ i r) c =
        BivariantClass.copy C (gysinSystemOfInvertible C) (𝒩.projection ≫ sZ) sX rfl
          (comp_comp_structureMorphism_eq rfl hi) (comp_comp_structureMorphism_eq rfl hi)
          (by ring : (0 : ℤ) = -(r : ℤ) + r) (virtualNormalConeClass C sZ sX i hi 𝒩)

Stacks.Chow.cap_eq_of_isVirtualNormalGysinRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleGysinClass.lean, line 245. The attribute's comment: “the defining relation i_ ∘ j^ ∘ C = p^ ∘ c(Z → X, 𝒩) determines the cap operations of the class, operation by operation; p^ is carried as a bivariant class for the projection of the vector bundle of 𝒩 (Stacks 0B78 being absent) and its bijectivity (Stacks 02TY) as the injectivity the argument uses, the class i_ ∘ j^ ∘ C is carried too (the deformation space of Stacks 0FBH and the class of Stacks 0F9J being absent), and the relation is expressed by the composition characterization of Stacks 0FE0, no composite of bivariant classes being constructed in this repository; neither the existence of the class nor the base-change compatibility of Stacks 0FBJ is proved”.

Stacks 0FBK. The relation i_* ∘ j^* ∘ C = p^* ∘ c(Z ⟶ X, 𝒩) determines the cap operations of c(Z ⟶ X, 𝒩): on every test scheme and in every degree, two bivariant classes satisfying it cap the same way. Here p : N = 𝐕(𝒩^∨) ⟶ Z is the projection of the vector bundle of the virtual normal bundle, flat stands for its flat pullback p^* and b for i_* ∘ j^* ∘ C, and the hypothesis on flat is the injectivity of Stacks 02TY.

theorem cap_eq_of_isVirtualNormalGysinRelation (hinj : flat.CapInjective)
    (h : IsBivariantClassComposition C G (N.projection ≫ sZ) sZ sX N.projection i rfl hi hpp p q
      flat c b)
    (h' : IsBivariantClassComposition C G (N.projection ≫ sZ) sZ sX N.projection i rfl hi hpp p q
      flat c' b)
    {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
    (α : chowGroup C (t ≫ sX) k) :
    c.cap t k α = c'.cap t k α

Stacks.Chow.eq_of_isVirtualNormalGysinRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleGysinClass.lean, line 267. The attribute's comment: “the defining relation i_ ∘ j^ ∘ C = p^ ∘ c(Z → X, 𝒩) determines the class in A^q(Z → X), the case q = r being the rank-r clause; p^ is carried as a bivariant class for the projection of the vector bundle of 𝒩 (Stacks 0B78 being absent) and its bijectivity (Stacks 02TY) as the injectivity the argument uses, the class i_ ∘ j^ ∘ C is carried too (the deformation space of Stacks 0FBH and the class of Stacks 0F9J being absent), and the relation is expressed by the composition characterization of Stacks 0FE0, no composite of bivariant classes being constructed in this repository; neither the existence of the class nor the base-change compatibility of Stacks 0FBJ is proved”.

Stacks 0FBK. The class c(Z ⟶ X, 𝒩) attached to an immersion with a virtual normal bundle is determined by the relation i_* ∘ j^* ∘ C = p^* ∘ c(Z ⟶ X, 𝒩): two bivariant classes of the same degree for i that both satisfy it are equal. This is the step the source calls legitimate because p^* is bijective on Chow groups, and injectivity is all it uses.

theorem eq_of_isVirtualNormalGysinRelation (hinj : flat.CapInjective)
    (h : IsBivariantClassComposition C G (N.projection ≫ sZ) sZ sX N.projection i rfl hi hpp p q
      flat c b)
    (h' : IsBivariantClassComposition C G (N.projection ≫ sZ) sZ sX N.projection i rfl hi hpp p q
      flat c' b) :
    c = c'

Stacks.Chow.diagonalVirtualNormalGysinClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/IntersectionProduct.lean, line 337. The attribute's comment: “the class of the construction, instantiated at the diagonal of X: the degree-r bivariant class of X ⟶ X ×_k X attached to a virtual normal bundle of constant rank r, with the same carried hypotheses as Stacks.Chow.virtualNormalGysinClass except Stacks 02S2, which is supplied by Stacks.Chow.properPushforwardDescends and is not carried”.

Stacks Project, Tag 0FBK. The Gysin class c(X ⟶ X ×_k X, 𝒩) ∈ A^r(X ⟶ X ×_k X) of the diagonal, produced by the construction of Stacks 0FBK from a virtual normal bundle of constant rank r for the diagonal. For X smooth over the base the diagonal is a regular immersion by Stacks.Chow.isRegularImmersion_diagonal_of_smooth, and its virtual normal bundle is the conormal bundle, of rank the relative dimension.

This is the class the definitions of Stacks.Chow.intersectionProduct carry, so feeding it in discharges that hypothesis; Stacks.Chow.intersectionProductOfVirtualNormalBundle does so.

The instance of Stacks 02S2 that the construction of Stacks 0FBK needs is not a hypothesis here: it is supplied by Stacks.Chow.properPushforwardDescends, which proves that statement outright.

def diagonalVirtualNormalGysinClass (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π) :
    BivariantClass C G sX (selfProductStructure C sX) (pullback.diagonal sX)
      (diagonal_comp_selfProductStructure C sX) (r : ℤ)

Stacks.Chow.VirtualNormalBundle.bivariantRestriction_virtualNormalClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/BaseChange.lean, line 850. The attribute's comment: “compatibility with base change at constant rank r: for X' → X locally of finite type, c(Z ×_X X' → X', g^*𝒩) = res(c(Z → X, 𝒩)) in A^r(Z ×_X X' → X') (Stacks 0FBJ, 0F9Z)”.

Compatibility with base change: for a closed immersion i : Z ⟶ X, a virtual normal bundle 𝒩 for i of constant rank r and h : X' ⟶ X locally of finite type, the class c(Z' ⟶ X', 𝒩') of the virtual normal bundle 𝒩' = g^*𝒩 for Z' = Z ×_X X' ⟶ X' is the restriction of c(Z ⟶ X, 𝒩).

theorem bivariantRestriction_virtualNormalClass :
    bivariantRestrictionOfInvertible C sZ sX i hZ h (r : ℤ) (𝒩.virtualNormalClass C sX sZ hZ r) =
      (𝒩.baseChangeAlong (IsPullback.of_hasPullback i h).flip).virtualNormalClass C (h ≫ sX)
        (pullback.fst i h ≫ sZ) (pullbackSnd_comp_structureMorphism_eq C sZ sX i hZ h) r

Stacks.Chow.VirtualNormalBundle.completedClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/Components.lean, line 249. The attribute's comment: “the class c(Z → X, 𝒩) ∈ A^*(Z → X)^∧ of a virtual normal bundle of arbitrary rank; its degree p part restricts on each connected component Z_k to c(Z_k → W_k, 𝒩|Z_k) of the construction when 𝒩 has rank p there, and to zero otherwise”.

Stacks 0FBK. The class c(Z ⟶ X, 𝒩) ∈ A^*(Z ⟶ X)^∧ of a virtual normal bundle whose rank need not be constant: the element of the completed bivariant group of Stacks 0FE0 whose degree p part is the class c_p ∈ A^p(Z ⟶ X) restricting to c(Z_k ⟶ W_k, 𝒩|_{Z_k}) on every connected component Z_k on which 𝒩 has rank p, and to zero on the others. The schemes Z and X are locally Noetherian, being locally of finite type over the base.

def completedClass : completedBivariantGroup C (gysinSystemOfInvertible C) sZ sX i hZ

Stacks.Chow.VirtualNormalBundle.virtualNormalClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/Construction.lean, line 183. The attribute's comment: “the construction at constant rank r: the class c(Z → X, 𝒩) ∈ A^r(Z → X), the quotient of ι_ ∘ j^ ∘ C by p^*, which is bijective on Chow groups (Stacks 02TY)”.

Stacks 0FBK, the construction: the class c(Z ⟶ X, 𝒩) ∈ A^r(Z ⟶ X) of a virtual normal bundle of constant rank r for a closed immersion: the bivariant class with p^* ∘ c(Z ⟶ X, 𝒩) = ι_* ∘ j^* ∘ C, that is, c(Z ⟶ X, 𝒩) ∩ α is the unique β with p^* β = ι_* j^*(C ∩ α).

def virtualNormalClass :
    BivariantClass C (gysinSystemOfInvertible C) sZ sX i hZ r

Stacks.Chow.VirtualNormalBundle.isBivariantClassComposition_virtualNormalClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/Construction.lean, line 215. The attribute's comment: “the construction at constant rank r: p^ ∘ c(Z → X, 𝒩) = ι_ ∘ j^* ∘ C as an identity of bivariant classes in A⁰(N → X)”.

Stacks 0FBK, the characterizing relation p^* ∘ c(Z ⟶ X, 𝒩) = ι_* ∘ j^* ∘ C, as an identity of bivariant classes in A⁰(N ⟶ X) (Stacks 0FE0).

theorem isBivariantClassComposition_virtualNormalClass :
    haveI := 𝒩.locallyOfFiniteType_projection r
    haveI := 𝒩.flat_projection r
    IsBivariantClassComposition C (gysinSystemOfInvertible C) (𝒩.proj ≫ sZ)
      sZ sX 𝒩.proj i rfl hZ (properPushforwardDescends C) (-(r : ℤ)) r
      (𝒩.pullbackClass C sZ r) (𝒩.virtualNormalClass C sX sZ hZ r)
      (𝒩.pushforwardClass C sX sZ hZ r)

Stacks.Chow.VirtualNormalBundle.eq_virtualNormalClass_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/Statement.lean, line 69. The attribute's comment: “(1), constant rank r: c(Z → X, 𝒩) ∈ A^r(Z → X) exists and is the unique class with p^ ∘ c = ι_ ∘ j^* ∘ C”.

Stacks 0FBK (1), constant rank. For 𝒩 of constant rank r, with p : N ⟶ Z the vector bundle of 𝒩, C ∈ A^0(W_∞ ⟶ X) the class of Stacks 0F9J, j : C_ZX ⟶ W_∞ and ι : C_ZX ⟶ N, a class c ∈ A^r(Z ⟶ X) satisfies p^* ∘ c = ι_* ∘ j^* ∘ C (read on T ×_X N for every T ⟶ X locally of finite type) if and only if it is the class c(Z ⟶ X, 𝒩) of the construction; such a class exists because p^* is bijective on Chow groups (Stacks 02TY).

theorem eq_virtualNormalClass_iff (r : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} 𝒩.bundle r]
    (c : BivariantClass C (gysinSystemOfInvertible C) sZ sX i hZ r) :
    c = 𝒩.virtualNormalClass C sX sZ hZ r ↔
      ∀ {T : Scheme.{u}} (t : T ⟶ X) [LocallyOfFiniteType t] (k : ℤ)
        (α : chowGroup C (t ≫ sX) k),
        haveI := 𝒩.locallyOfFiniteType_projection r
        haveI := 𝒩.flat_projection r
        middleCap C (gysinSystemOfInvertible C) (𝒩.proj ≫ sZ) sZ 𝒩.proj i
            rfl (-(r : ℤ)) (𝒩.pullbackClass C sZ r) t (k - r) (c.cap t k α) =
          chowGroupDegreeEquiv C (pullback.fst (𝒩.proj ≫ i) t ≫ (𝒩.proj ≫ sZ))
            (by ring : k - (-(r : ℤ) + r) = k - r - -(r : ℤ))
            ((𝒩.pushforwardClass C sX sZ hZ r).cap t k α)

Stacks.Chow.VirtualNormalBundle.restriction_completedClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/Statement.lean, line 91. The attribute's comment: “(1): the degree p part of c(Z → X, 𝒩) ∈ A^*(Z → X)^∧ restricts on each connected component Z_k to the class of the construction for 𝒩|Z_k if 𝒩 has rank p there, else to zero”.

Stacks 0FBK (1). The degree p part of c(Z ⟶ X, 𝒩) ∈ A^*(Z ⟶ X)^∧, restricted to the piece Z_k ⟶ W_k of a connected component Z_k of Z (Stacks 0FDZ), is the class c(Z_k ⟶ W_k, 𝒩|_{Z_k}) of the construction when 𝒩 has rank p on Z_k, and zero otherwise.

theorem restriction_completedClass (p : ℤ) (k : _root_.ConnectedComponents Z) :
    haveI := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    bivariantPieceRestrictionOfInvertible C sZ sX i hZ p Z.connectedComponentOpens
        (componentAmbient i) id (le_preimage_componentAmbient i) k
        (completedBivariantSequenceOfInvertible C sZ sX i hZ (𝒩.completedClass C sX sZ hZ) p) =
      𝒩.componentFamily C sX sZ hZ p k

Stacks.Chow.VirtualNormalBundle.eq_completedClass_of_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/Statement.lean, line 108. The attribute's comment: “(1), uniqueness: c(Z → X, 𝒩) is the only element of A^*(Z → X)^∧ with these restrictions to the connected components”.

Stacks 0FBK (1), uniqueness. c(Z ⟶ X, 𝒩) is the only element of A^*(Z ⟶ X)^∧ whose degree p parts restrict on the connected components of Z to the classes of the construction in the degree of the rank of 𝒩, and to zero in the other degrees.

theorem eq_completedClass_of_restriction
    (c : completedBivariantGroup C (gysinSystemOfInvertible C) sZ sX i hZ) :
    haveI := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    (∀ (p : ℤ) (k : _root_.ConnectedComponents Z),
      bivariantPieceRestrictionOfInvertible C sZ sX i hZ p Z.connectedComponentOpens
          (componentAmbient i) id (le_preimage_componentAmbient i) k
          (completedBivariantSequenceOfInvertible C sZ sX i hZ c p) =
        𝒩.componentFamily C sX sZ hZ p k) →
      c = 𝒩.completedClass C sX sZ hZ

Stacks.Chow.VirtualNormalBundle.baseChange_completedClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/Statement.lean, line 136. The attribute's comment: “(2): c(Z' → X', g^𝒩) = res(c(Z → X, 𝒩)) in A^(Z' → X')^∧ for every X' → X locally of finite type”.

Stacks 0FBK (2), compatibility with base change. For h : X' ⟶ X locally of finite type, Z' = Z ×_X X' and the virtual normal bundle 𝒩' = g^*𝒩 of Stacks 0FBJ for Z' ⟶ X', c(Z' ⟶ X', 𝒩') is the restriction res(c(Z ⟶ X, 𝒩)) of Stacks 0F9Z, on the completed groups of Stacks 0FE0.

theorem baseChange_completedClass {X' : Scheme.{u}} (h : X' ⟶ X) [LocallyOfFiniteType h] :
    haveI := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI := LocallyOfFiniteType.isLocallyNoetherian (h ≫ sX)
    haveI := LocallyOfFiniteType.isLocallyNoetherian (pullback.fst i h ≫ sZ)
    (𝒩.baseChangePullback h).completedClass C (h ≫ sX) (pullback.fst i h ≫ sZ)
        (pullbackSnd_comp_structureMorphism_eq C sZ sX i hZ h) =
      completedBivariantRestrictionOfInvertible C sZ sX i hZ h (𝒩.completedClass C sX sZ hZ)

Stacks.Chow.VirtualNormalBundle.completedClass_of_constantRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/Statement.lean, line 155. The attribute's comment: “(3): for 𝒩 of constant rank r, c(Z → X, 𝒩) lies in A^r(Z → X): its degree r part is the class of the construction and its other parts vanish”.

Stacks 0FBK (3). If 𝒩 has constant rank r, then c(Z ⟶ X, 𝒩) ∈ A^r(Z ⟶ X): its degree r part is the class c(Z ⟶ X, 𝒩) of the construction (the unique class with p^* ∘ c = ι_* ∘ j^* ∘ C) and its other parts vanish.

theorem completedClass_of_constantRank (r : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} 𝒩.bundle r] (p : ℤ) :
    haveI := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    completedBivariantSequenceOfInvertible C sZ sX i hZ (𝒩.completedClass C sX sZ hZ) p =
      if h : (r : ℤ) = p then h ▸ 𝒩.virtualNormalClass C sX sZ hZ r else 0

Tag 0FBL, a lemma

Tag 0FBL in the Stacks Project.

Stacks.Chow.completedVirtualNormalGysinClass_eq_of_isTopChernComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedVirtualNormalSubbundle.lean, line 259. The attribute's comment: “c(Z → X, N) = c_top(E) ∘ c(Z → X, N') in A^*(Z → X)^∧ for a short exact sequence 0 → N' → N → E → 0 of finite locally free modules of arbitrary rank whose surjection factors through that of N'”.

Stacks 0FBL. Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S, let i : Z ⟶ X be a closed subscheme with virtual normal sheaf 𝒩, and let 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free 𝒪_Z-modules, of arbitrary ranks, such that the conormal surjection σ : 𝒩^∨ ⟶ 𝒞_{Z/X} factors as σ' ∘ (𝒩^∨ ⟶ (𝒩')^∨) through that of 𝒩'. Then

c(Z ⟶ X, 𝒩) = c_top(ℰ) ∘ c(Z ⟶ X, 𝒩')

in the completed bivariant group A^*(Z ⟶ X)^∧ of Stacks 0FE0, for the classes of Stacks 0FBK, the top Chern class of Stacks 0FA4 and the composition on completions; the composite is a class for 𝟙 Z ≫ i = i.

On a connected component Z_a of Z both sides are concentrated in the degree r_a of 𝒩, and there this is Stacks 0FBL at constant rank for Z_a ⟶ U_a composed with (U_a ⟶ X_b)^*.

theorem completedVirtualNormalGysinClass_eq_of_isTopChernComposition
    (w : inc ≫ pr = 0) (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (hsigma : dualMap inc ≫ 𝒩'.surjection = 𝒩.surjection) :
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    completedVirtualNormalGysinClass C sZ sX i hi 𝒩 =
      completedBivariantGroup.copy C (Category.id_comp i) _ hi
        (completedBivariantCompositeOfInvertible C sZ sZ sX (𝟙 Z) i (Category.id_comp sZ) hi
          (topChernClassOfInvertible C sZ Eb)
          (completedVirtualNormalGysinClass C sZ sX i hi 𝒩'))

Stacks.Chow.virtualNormalGysinCap_eq_topChernCap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalSubbundle.lean, line 347. The attribute's comment: “c(Z -> X, N) = c_top(E) composed with c(Z -> X, N') for a short exact sequence 0 -> N' -> N -> E -> 0 of finite locally free O_Z-modules of constant ranks m', m, e whose conormal surjection factors. The short exact sequence IS consumed: it gives m = m' + e, which is what puts the two sides in the same Chow group. Both classes are the ones CHARACTERIZED by Tag 0FBK, neither being constructed in this repository, and the composite is spelled by the top Chern cap rule at Fin.last e as Tag 0FAA spells it. CARRIED: Tag 0FAA at the base changes of the two bundle projections (SubbundleGysinTopChernStep) -- 0FAA is proved only over the base scheme for the canonical bundles, with no identification of a base-changed vector bundle with the bundle of a pulled-back module; the geometric consequence of the tag's own factoring hypothesis, i_ = j_ composed with i'_* (SubbundleGysinFactorization), Tags 0637, 0FBH and 0F9J being absent. THE TAG'S SHEAF-LEVEL FACTORING HYPOTHESIS IS PRESENT AS _hsigma BUT UNUSED: the proof runs on that carried geometric consequence instead. Also carried: Tag 02TY injectivity only, Tag 02S1 descent, Tag 0B7G as this directory's standing cap-rule parameter”.

Stacks 0FBL, on cap operations. Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S, let i : Z ⟶ X be a closed subscheme with virtual normal sheaf 𝒩 of constant rank m, and let 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free 𝒪_Z-modules of constant ranks m', m and e whose inclusion dualizes to a factorization σ = σ' ∘ (𝒩^∨ ⟶ (𝒩')^∨) of the conormal surjection of 𝒩 through that of 𝒩'. Then, for the classes c = c(Z ⟶ X, 𝒩) and c' = c(Z ⟶ X, 𝒩') of Stacks 0FBK,

c ∩ α = c_top(ℰ) ∩ (c' ∩ α)

on every test scheme g : T ⟶ X, in every degree and for every α ∈ A_k(T). Since a bivariant class is determined by its cap operations (Stacks.Chow.BivariantClass.ext), this is the tag's equality c(Z ⟶ X, 𝒩) = c_top(ℰ) ∘ c(Z ⟶ X, 𝒩') of bivariant classes; see Stacks.Chow.virtualNormalGysinClass_eq_of_isTopChernComposition.

theorem virtualNormalGysinCap_eq_topChernCap_comp
    (w : inc ≫ pr = 0) (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (_hsigma : dualMap inc ≫ P'.normalBundle.surjection = P.normalBundle.surjection) (x : Z)
    (hinj : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C sZ sN i q hq m P.flat P.relativeDimension hdesc g k))
    (hfactor : SubbundleGysinFactorization C G sZ sX sN sN' i hi q q' hq hq' j hj E E')
    (hstep : SubbundleGysinTopChernStep C sZ sN sN' i q q' hq hq' j hj m m' e Eb cap hdesc P P')
    {c : BivariantClass C G sZ sX i hi (m : ℤ)}
    {c' : BivariantClass C G sZ sX i hi (m' : ℤ)}
    (hc : IsVirtualNormalGysinClass C G sZ sX sN i hi q hq m 0 E
      (bundleFlatPullback C sZ sN i q hq m P.flat P.relativeDimension hdesc) P c)
    (hc' : IsVirtualNormalGysinClass C G sZ sX sN' i hi q' hq' m' 0 E'
      (bundleFlatPullback C sZ sN' i q' hq' m' P'.flat P'.relativeDimension hdesc) P' c')
    {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
    (α : chowGroup C (g ≫ sX) k) :
    c.cap g k α =
      chowGroupDegreeEquiv C (pullback.fst i g ≫ sZ)
        (subbundleVirtualNormalDegree_eq P P' Eb inc pr w hseq x k)
        (subbundleTopChernCap C sZ i m' e Eb cap g k (c'.cap g k α))

Stacks.Chow.virtualNormalGysinClass_eq_of_isTopChernComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalSubbundle.lean, line 391. The attribute's comment: “c(Z -> X, N) = c_top(E) composed with c(Z -> X, N') for a short exact sequence 0 -> N' -> N -> E -> 0 of finite locally free O_Z-modules of constant ranks m', m, e whose conormal surjection factors. The short exact sequence IS consumed: it gives m = m' + e, which is what puts the two sides in the same Chow group. Read as an equality of classes in A^m(Z -> X) via BivariantClass.ext. Both classes are the ones CHARACTERIZED by Tag 0FBK, neither being constructed in this repository, and the composite is spelled by the top Chern cap rule at Fin.last e as Tag 0FAA spells it. CARRIED: Tag 0FAA at the base changes of the two bundle projections (SubbundleGysinTopChernStep) -- 0FAA is proved only over the base scheme for the canonical bundles, with no identification of a base-changed vector bundle with the bundle of a pulled-back module; the geometric consequence of the tag's own factoring hypothesis, i_ = j_ composed with i'_* (SubbundleGysinFactorization), Tags 0637, 0FBH and 0F9J being absent. THE TAG'S SHEAF-LEVEL FACTORING HYPOTHESIS IS PRESENT AS _hsigma BUT UNUSED: the proof runs on that carried geometric consequence instead. Also carried: Tag 02TY injectivity only, Tag 02S1 descent, Tag 0B7G as this directory's standing cap-rule parameter”.

Stacks 0FBL, as an equality in A^m(Z ⟶ X). If d is a bivariant class of degree m for i : Z ⟶ X whose cap operation is cap with c(Z ⟶ X, 𝒩') followed by c_top(ℰ), that is if d is the composite c_top(ℰ) ∘ c(Z ⟶ X, 𝒩'), then d = c(Z ⟶ X, 𝒩).

The composite is described by its cap operation, in the idiom of Stacks.Chow.IsBivariantClassComposition.

theorem virtualNormalGysinClass_eq_of_isTopChernComposition
    (w : inc ≫ pr = 0) (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (hsigma : dualMap inc ≫ P'.normalBundle.surjection = P.normalBundle.surjection) (x : Z)
    (hinj : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C sZ sN i q hq m P.flat P.relativeDimension hdesc g k))
    (hfactor : SubbundleGysinFactorization C G sZ sX sN sN' i hi q q' hq hq' j hj E E')
    (hstep : SubbundleGysinTopChernStep C sZ sN sN' i q q' hq hq' j hj m m' e Eb cap hdesc P P')
    {c d : BivariantClass C G sZ sX i hi (m : ℤ)}
    {c' : BivariantClass C G sZ sX i hi (m' : ℤ)}
    (hc : IsVirtualNormalGysinClass C G sZ sX sN i hi q hq m 0 E
      (bundleFlatPullback C sZ sN i q hq m P.flat P.relativeDimension hdesc) P c)
    (hc' : IsVirtualNormalGysinClass C G sZ sX sN' i hi q' hq' m' 0 E'
      (bundleFlatPullback C sZ sN' i q' hq' m' P'.flat P'.relativeDimension hdesc) P' c')
    (hd : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ)
      (α : chowGroup C (g ≫ sX) k),
      d.cap g k α =
        chowGroupDegreeEquiv C (pullback.fst i g ≫ sZ)
          (subbundleVirtualNormalDegree_eq P P' Eb inc pr w hseq x k)
          (subbundleTopChernCap C sZ i m' e Eb cap g k (c'.cap g k α))) :
    d = c

Stacks.Chow.VirtualNormalBundle.completedClass_eq_topChernClassCompleted_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/SubbundleCompleted.lean, line 544. The attribute's comment: “c(Z → X, 𝒩) = c_top(ℰ) ∘ c(Z → X, 𝒩') in A^*(Z → X)^∧, for a short exact sequence 0 → 𝒩' → 𝒩 → ℰ → 0 of finite locally free O_Z-modules along which σ factors through σ' : (𝒩')^∨ → C_{Z/X}; ranks arbitrary, c(Z → X, -) the completed classes of Tag 0FBK, c_top(ℰ) the completed class of Tag 0FA4, ∘ the composition of Tag 0FE0”.

Stacks 0FBL. Let i : Z ⟶ X be a closed immersion with virtual normal sheaf 𝒩, let 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free 𝒪_Z-modules, and let σ' : (𝒩')^∨ ⟶ 𝒞_{Z/X} be such that σ = σ' ∘ (𝒩^∨ ⟶ (𝒩')^∨). Then

c(Z ⟶ X, 𝒩) = c_top(ℰ) ∘ c(Z ⟶ X, 𝒩') in A^*(Z ⟶ X)^∧,

where c(Z ⟶ X, -) is the class of Stacks 0FBK, c_top(ℰ) ∈ A^*(Z)^∧ the top Chern class of Stacks 0FA4, ∘ the composition A^*(Z)^∧ × A^*(Z ⟶ X)^∧ ⟶ A^*(Z ⟶ X)^∧ of Stacks 0FE0, and the composite, a class for 𝟙 Z ≫ i, is read at i.

theorem completedClass_eq_topChernClassCompleted_comp :
    haveI := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    𝒩.completedClass C sX sZ hZ =
      completedBivariantGroupCongr C (gysinSystemOfInvertible C) sZ sX (Category.id_comp i)
        (comp_comp_structureMorphism_eq (Category.id_comp sZ) hZ) hZ
        (completedBivariantCompositeOfInvertible C sZ sZ sX (𝟙 Z) i (Category.id_comp sZ) hZ
          (topChernClassCompleted C sZ E).1
          ((𝒩.ofFactor N' inc σ' hσ).completedClass C sX sZ hZ))

Tag 0FV7, a lemma

Tag 0FV7 in the Stacks Project.

Stacks.Chow.completedVirtualNormalGysinRestriction_eq_of_isTopChernComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedVirtualNormalRestrictionExcess.lean, line 71. The attribute's comment: “res(c(Z → X, N)) = c_top(E) ∘ c(Z' → X', N') in A^(Z' → X')^∧, for a cartesian square of closed immersions (the chosen fibre product Z' = Z ×_X X', where restriction lives), virtual normal sheaves N, N' of arbitrary rank, and a short exact sequence 0 → N' → g^N → E → 0 of finite locally free modules whose dual square against the conormal sheaves commutes”.

Stacks 0FV7. Let Z' = Z ×_X X' be the chosen base change of a closed immersion i : Z ⟶ X along f : X' ⟶ X, both locally of finite type over the base, let 𝒩 be a virtual normal sheaf for Z ⊂ X and 𝒩' one for Z' ⟶ X', of arbitrary ranks, and let 0 ⟶ 𝒩' ⟶ g^*𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free 𝒪_{Z'}-modules such that the square of hcomm commutes. Then

res(c(Z ⟶ X, 𝒩)) = c_top(ℰ) ∘ c(Z' ⟶ X', 𝒩')

in A^*(Z' ⟶ X')^∧, for the classes of Stacks 0FBK, the top Chern class of Stacks 0FA4 and the composition on completions (a class for 𝟙 ≫ (Z' ⟶ X')).

theorem completedVirtualNormalGysinRestriction_eq_of_isTopChernComposition
    (w : inc ≫ pr = 0) (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (hcomm : pullbackDualMap (pullback.fst i f) N.bundle ≫
        dualMap inc ≫ 𝒩'.surjection =
      (modulePullback (pullback.fst i f).toLRSHom.toShHom).map N.surjection ≫
        Stacks.Immersion.immersionConormalSheafMap (pullback.snd i f) i (pullback.fst i f) f
          (Stacks.Immersion.toShHom_square (isPullback_pullbackSnd i f).w)) :
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI : IsLocallyNoetherian X' := LocallyOfFiniteType.isLocallyNoetherian (f ≫ sX)
    haveI : IsLocallyNoetherian (pullback i f) :=
      LocallyOfFiniteType.isLocallyNoetherian (pullback.fst i f ≫ sZ)
    completedBivariantRestrictionViaSequence C sZ sX i hi f
        (completedVirtualNormalGysinClass C sZ sX i hi N) =
      completedBivariantGroup.copy C (Category.id_comp (pullback.snd i f)) _
        (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f)
        (completedBivariantCompositeOfInvertible C (pullback.fst i f ≫ sZ)
          (pullback.fst i f ≫ sZ) (f ≫ sX) (𝟙 _) (pullback.snd i f) (Category.id_comp _)
          (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f)
          (topChernClassOfInvertible C (pullback.fst i f ≫ sZ) Eb)
          (completedVirtualNormalGysinClass C (pullback.fst i f ≫ sZ) (f ≫ sX) (pullback.snd i f)
            (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) 𝒩'))

Stacks.Chow.virtualNormalGysinRestrictionCap_eq_topChernCap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBaseChangeExcess.lean, line 294. The attribute's comment: “res(c(Z -> X, N)) = c_top(E) composed with c(Z' -> X', N') for a cartesian square of closed immersions and a short exact sequence 0 -> N' -> g^N -> E -> 0 of finite locally free O_{Z'}-modules of constant ranks m', m, e whose dual square against the conormal sheaves commutes. The square is the CHOSEN fibre product, which is where Stacks 0F9Z lives in this repository (bivariantRestriction), every cartesian square being canonically isomorphic to it. The commuting square IS consumed: it yields the factorization hypothesis of Stacks 0FBL for g^N, which is dualMap_comp_surjection_eq_baseChange_surjection. The pulled-back sheaf is the virtual normal sheaf of Stacks 0FBJ, and its constant rank is PROVED, not assumed. CARRIED: the Stacks 0FBJ base-change clause of Stacks 0FBK as hbase -- that res(c) satisfies the characterizing relation for g^*N, the source's first proof step, which is recorded as not proved in this repository (Stacks 0637, 0FBH, 0F9J absent); and the hypotheses of Stacks 0FBL, unchanged (Stacks 0FAA at the base-changed bundle projections as hstep, the geometric consequence of the factorization as hfactor, Stacks 02TY injectivity as hinj, Stacks 0B7G as this directory's cap-rule parameter)”.

Stacks 0FV7, on cap operations. Let (S, δ) be the base situation of chapter 42, let

Z' --i'--→ X'
|          |
g          f
↓          ↓
Z  --i---→ X

be the cartesian square of the chosen fibre product Z' = Z ×_X X' of a closed immersion i : Z ⟶ X along f : X' ⟶ X, both locally of finite type over S. Let 𝒩 be a virtual normal sheaf for Z ⊂ X of constant rank m, let 𝒩' be one for Z' ⟶ X' of constant rank m', and let

0 ⟶ 𝒩' ⟶ g^*𝒩 ⟶ ℰ ⟶ 0

be a short exact sequence of finite locally free 𝒪_{Z'}-modules with ℰ of constant rank e, such that the square of hcomm commutes. Then, for c = c(Z ⟶ X, 𝒩) and c' = c(Z' ⟶ X', 𝒩') the classes of Stacks 0FBK,

res(c) ∩ α = c_top(ℰ) ∩ (c' ∩ α)

on every test scheme g₀ : T ⟶ X', in every degree and for every α ∈ A_k(T).

The identification of res(c) with c(Z' ⟶ X', g^*𝒩) by Stacks 0FBK is the hypothesis hbase.

theorem virtualNormalGysinRestrictionCap_eq_topChernCap_comp
    (w : inc ≫ pr = 0) (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (hcomm : pullbackDualMap (pullback.fst i f) N.bundle ≫
        dualMap inc ≫ P'.normalBundle.surjection =
      (modulePullback (pullback.fst i f).toLRSHom.toShHom).map N.surjection ≫
        Stacks.Immersion.immersionConormalSheafMap (pullback.snd i f) i (pullback.fst i f) f
          (Stacks.Immersion.toShHom_square (isPullback_pullbackSnd i f).w))
    (x : ↥(pullback i f))
    (hinj : ∀ {T : Scheme.{u}} (g₀ : T ⟶ X') [LocallyOfFiniteType g₀] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C (pullback.fst i f ≫ sZ) sNbig (pullback.snd i f) q hq m hflat hrd
          hdesc g₀ k))
    (hfactor : SubbundleGysinFactorization C G (pullback.fst i f ≫ sZ) (f ≫ sX) sNbig sNsub
      (pullback.snd i f) (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) q q' hq hq' j hj
      E E')
    (hstep : SubbundleGysinTopChernStep C (pullback.fst i f ≫ sZ) sNbig sNsub (pullback.snd i f)
      q q' hq hq' j hj m m' e Eb cap hdesc
      (baseChangeVirtualNormalProjection i f N m hrank q hflat hrd) P')
    {c : BivariantClass C G sZ sX i hi (m : ℤ)}
    {c' : BivariantClass C G (pullback.fst i f ≫ sZ) (f ≫ sX) (pullback.snd i f)
      (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) (m' : ℤ)}
    (hbase : IsVirtualNormalGysinClass C G (pullback.fst i f ≫ sZ) (f ≫ sX) sNbig
      (pullback.snd i f) (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) q hq m 0 E
      (bundleFlatPullback C (pullback.fst i f ≫ sZ) sNbig (pullback.snd i f) q hq m hflat hrd
        hdesc)
      (baseChangeVirtualNormalProjection i f N m hrank q hflat hrd)
      (bivariantRestriction C G sZ sX i hi f (m : ℤ) hgys c))
    (hbase' : IsVirtualNormalGysinClass C G (pullback.fst i f ≫ sZ) (f ≫ sX) sNsub
      (pullback.snd i f) (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) q' hq' m' 0 E'
      (bundleFlatPullback C (pullback.fst i f ≫ sZ) sNsub (pullback.snd i f) q' hq' m' P'.flat
        P'.relativeDimension hdesc)
      P' c')
    {T : Scheme.{u}} (g₀ : T ⟶ X') [LocallyOfFiniteType g₀] (k : ℤ)
    (α : chowGroup C (g₀ ≫ (f ≫ sX)) k) :
    (bivariantRestriction C G sZ sX i hi f (m : ℤ) hgys c).cap g₀ k α =
      chowGroupDegreeEquiv C (pullback.fst (pullback.snd i f) g₀ ≫ (pullback.fst i f ≫ sZ))
        (subbundleVirtualNormalDegree_eq
          (baseChangeVirtualNormalProjection i f N m hrank q hflat hrd) P' Eb inc pr w hseq x k)
        (subbundleTopChernCap C (pullback.fst i f ≫ sZ) (pullback.snd i f) m' e Eb cap g₀ k
          (c'.cap g₀ k α))

Stacks.Chow.virtualNormalGysinRestriction_eq_of_isTopChernComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBaseChangeExcess.lean, line 362. The attribute's comment: “res(c(Z -> X, N)) = c_top(E) composed with c(Z' -> X', N'), read as an equality of classes in A^m(Z' -> X') via BivariantClass.ext, for a cartesian square of closed immersions and a short exact sequence 0 -> N' -> g^N -> E -> 0 of finite locally free O_{Z'}-modules of constant ranks m', m, e whose dual square against the conormal sheaves commutes. The square is the CHOSEN fibre product, which is where Stacks 0F9Z lives in this repository (bivariantRestriction), every cartesian square being canonically isomorphic to it. The commuting square IS consumed: it yields the factorization hypothesis of Stacks 0FBL for g^N. The pulled-back sheaf is the virtual normal sheaf of Stacks 0FBJ, and its constant rank is PROVED, not assumed. CARRIED: the Stacks 0FBJ base-change clause of Stacks 0FBK as hbase, the source's first proof step, recorded as not proved in this repository (Stacks 0637, 0FBH, 0F9J absent); and the hypotheses of Stacks 0FBL, unchanged (Stacks 0FAA at the base-changed bundle projections as hstep, the geometric consequence of the factorization as hfactor, Stacks 02TY injectivity as hinj, Stacks 0B7G as this directory's cap-rule parameter)”.

Stacks 0FV7, as an equality in A^m(Z' ⟶ X'). If d is a bivariant class of degree m for Z' ⟶ X' whose cap operation is cap with c(Z' ⟶ X', 𝒩') followed by c_top(ℰ), that is if d is the composite c_top(ℰ) ∘ c(Z' ⟶ X', 𝒩'), then d = res(c(Z ⟶ X, 𝒩)).

The composite is described by its cap operation, in the idiom of Stacks.Chow.IsBivariantClassComposition.

theorem virtualNormalGysinRestriction_eq_of_isTopChernComposition
    (w : inc ≫ pr = 0) (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (hcomm : pullbackDualMap (pullback.fst i f) N.bundle ≫
        dualMap inc ≫ P'.normalBundle.surjection =
      (modulePullback (pullback.fst i f).toLRSHom.toShHom).map N.surjection ≫
        Stacks.Immersion.immersionConormalSheafMap (pullback.snd i f) i (pullback.fst i f) f
          (Stacks.Immersion.toShHom_square (isPullback_pullbackSnd i f).w))
    (x : ↥(pullback i f))
    (hinj : ∀ {T : Scheme.{u}} (g₀ : T ⟶ X') [LocallyOfFiniteType g₀] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C (pullback.fst i f ≫ sZ) sNbig (pullback.snd i f) q hq m hflat hrd
          hdesc g₀ k))
    (hfactor : SubbundleGysinFactorization C G (pullback.fst i f ≫ sZ) (f ≫ sX) sNbig sNsub
      (pullback.snd i f) (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) q q' hq hq' j hj
      E E')
    (hstep : SubbundleGysinTopChernStep C (pullback.fst i f ≫ sZ) sNbig sNsub (pullback.snd i f)
      q q' hq hq' j hj m m' e Eb cap hdesc
      (baseChangeVirtualNormalProjection i f N m hrank q hflat hrd) P')
    {c : BivariantClass C G sZ sX i hi (m : ℤ)}
    {c' : BivariantClass C G (pullback.fst i f ≫ sZ) (f ≫ sX) (pullback.snd i f)
      (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) (m' : ℤ)}
    {d : BivariantClass C G (pullback.fst i f ≫ sZ) (f ≫ sX) (pullback.snd i f)
      (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) (m : ℤ)}
    (hbase : IsVirtualNormalGysinClass C G (pullback.fst i f ≫ sZ) (f ≫ sX) sNbig
      (pullback.snd i f) (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) q hq m 0 E
      (bundleFlatPullback C (pullback.fst i f ≫ sZ) sNbig (pullback.snd i f) q hq m hflat hrd
        hdesc)
      (baseChangeVirtualNormalProjection i f N m hrank q hflat hrd)
      (bivariantRestriction C G sZ sX i hi f (m : ℤ) hgys c))
    (hbase' : IsVirtualNormalGysinClass C G (pullback.fst i f ≫ sZ) (f ≫ sX) sNsub
      (pullback.snd i f) (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) q' hq' m' 0 E'
      (bundleFlatPullback C (pullback.fst i f ≫ sZ) sNsub (pullback.snd i f) q' hq' m' P'.flat
        P'.relativeDimension hdesc)
      P' c')
    (hd : ∀ {T : Scheme.{u}} (g₀ : T ⟶ X') [LocallyOfFiniteType g₀] (k : ℤ)
      (α : chowGroup C (g₀ ≫ (f ≫ sX)) k),
      d.cap g₀ k α =
        chowGroupDegreeEquiv C (pullback.fst (pullback.snd i f) g₀ ≫ (pullback.fst i f ≫ sZ))
          (subbundleVirtualNormalDegree_eq
            (baseChangeVirtualNormalProjection i f N m hrank q hflat hrd) P' Eb inc pr w hseq x k)
          (subbundleTopChernCap C (pullback.fst i f ≫ sZ) (pullback.snd i f) m' e Eb cap g₀ k
            (c'.cap g₀ k α))) :
    d = bivariantRestriction C G sZ sX i hi f (m : ℤ) hgys c

Stacks.Chow.VirtualNormalBundle.completedBivariantRestriction_completedClass_eq_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/ExcessBaseChange.lean, line 174. The attribute's comment: “res(c(Z → X, 𝒩)) = c_top(ℰ) ∘ c(Z' → X', 𝒩') in A^(Z' → X')^∧ for the cartesian square Z' = Z ×_X X' of a closed immersion i along X' → X locally of finite type, virtual normal sheaves 𝒩 for Z ⊂ X and 𝒩' for Z' ⊂ X', and a short exact sequence 0 → 𝒩' → g^𝒩 → ℰ → 0 of finite locally free O_{Z'}-modules whose dual square against the conormal sheaves commutes; ranks arbitrary, c the completed classes of Tag 0FBK, res on completed groups, c_top(ℰ) of Tag 0FA4, ∘ the composition of Tag 0FE0”.

Stacks 0FV7. Let i : Z ⟶ X be a closed immersion of schemes locally of finite type over the base, h : X' ⟶ X locally of finite type, and Z' = Z ×_X X' with its closed immersion i' : Z' ⟶ X' and projection g : Z' ⟶ Z. Let 𝒩 be a virtual normal sheaf for Z ⊂ X and 𝒩' one for Z' ⊂ X', and let 0 ⟶ 𝒩' ⟶ g^*𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free 𝒪_{Z'}-modules such that the square g^*𝒩^∨ ⟶ (𝒩')^∨ ⟶ 𝒞_{Z'/X'} = g^*𝒩^∨ ⟶ g^*𝒞_{Z/X} ⟶ 𝒞_{Z'/X'} commutes (hcomm). Then

res(c(Z ⟶ X, 𝒩)) = c_top(ℰ) ∘ c(Z' ⟶ X', 𝒩') in A^*(Z' ⟶ X')^∧,

where c(-, -) are the classes of Stacks 0FBK, res the restriction of Stacks 0F9Z on the completed groups, c_top(ℰ) ∈ A^*(Z')^∧ the top Chern class of Stacks 0FA4 and ∘ the composition of Stacks 0FE0; the composite, a class for 𝟙 Z' ≫ i', is read at i'. No rank is assumed constant.

The proof is the source's: Stacks 0FBK gives res(c(Z ⟶ X, 𝒩)) = c(Z' ⟶ X', g^*𝒩), the commuting square says that the conormal surjection of g^*𝒩 factors through σ' along the dual of 𝒩' ⟶ g^*𝒩, and Stacks 0FBL concludes.

theorem completedBivariantRestriction_completedClass_eq_comp :
    haveI := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI := LocallyOfFiniteType.isLocallyNoetherian (h ≫ sX)
    haveI := LocallyOfFiniteType.isLocallyNoetherian (pullback.fst i h ≫ sZ)
    completedBivariantRestrictionOfInvertible C sZ sX i hZ h (𝒩.completedClass C sX sZ hZ) =
      completedBivariantGroupCongr C (gysinSystemOfInvertible C) (pullback.fst i h ≫ sZ)
        (h ≫ sX) (Category.id_comp (pullback.snd i h))
        (comp_comp_structureMorphism_eq (Category.id_comp _)
          (pullbackSnd_comp_structureMorphism_eq C sZ sX i hZ h))
        (pullbackSnd_comp_structureMorphism_eq C sZ sX i hZ h)
        (completedBivariantCompositeOfInvertible C (pullback.fst i h ≫ sZ)
          (pullback.fst i h ≫ sZ) (h ≫ sX) (𝟙 _) (pullback.snd i h) (Category.id_comp _)
          (pullbackSnd_comp_structureMorphism_eq C sZ sX i hZ h)
          (topChernClassCompleted C (pullback.fst i h ≫ sZ) E).1
          (𝒩'.completedClass C (h ≫ sX) (pullback.fst i h ≫ sZ)
            (pullbackSnd_comp_structureMorphism_eq C sZ sX i hZ h)))

Tag 0FBM, a lemma

Tag 0FBM in the Stacks Project.

Stacks.Chow.completedVirtualNormalGysinCap_fundamentalChowClass_excess, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedExcessIntersectionFormula.lean, line 347. The attribute's comment: “c(Z → X, N) ∩ [Y]_n = c_top(E) ∩ [Z ×_X Y]_{n-r} in CH_(Z ×_X Y), for N a virtual normal sheaf of arbitrary rank, c(Z → X, N) ∈ A^(Z → X)^∧, Z ×_X Y → Y regular with conormal sheaf of constant rank r, E the excess normal sheaf, and dim_δ(Y) ≤ n; stated degree by degree”.

Let i : Z ⟶ X be a closed immersion of schemes locally of finite type over the base with a virtual normal sheaf 𝒩 (Stacks 0FBQ), of arbitrary rank, and let g : Y ⟶ X be locally of finite type such that the base change i' : Z' = Z ×_X Y ⟶ Y is a regular closed immersion whose conormal sheaf 𝒞_{Z'/Y} has constant rank r. Let ℰ be the excess normal sheaf, 0 ⟶ ℰ^∨ ⟶ 𝒩^∨|_{Z'} ⟶ 𝒞_{Z'/Y} ⟶ 0. If dim_δ(Y) ≤ n then

c(Z ⟶ X, 𝒩) ∩ [Y]_n = c_top(ℰ) ∩ [Z']_{n - r}

in CH_*(Z ×_X Y), for the class c(Z ⟶ X, 𝒩) ∈ A^*(Z ⟶ X)^∧ of Stacks 0FBK (Stacks.Chow.completedVirtualNormalGysinClass) and the top Chern class of Stacks 0FA4: in degree n - (r + e) the degree-(r + e) part of the left-hand side is the cap product of [Z']_{n - r} with the degree-e part of c_top(ℰ) (Stacks.Chow.topChernCap), and in degree n - p for p < r the left-hand side vanishes, as the right-hand side does.

theorem completedVirtualNormalGysinCap_fundamentalChowClass_excess
    (hreg : IsRegularImmersion i') (r : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (conormalModule i') r]
    (n : ℤ) (hY : schemeDeltaDimension C (g ≫ sX) ≤ (n : EInt)) :
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI : SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (𝒩.baseChange i i' g' g sq).excessNormalSheaf :=
      (𝒩.baseChange i i' g' g sq).isFiniteLocallyFree_excessNormalSheaf
        (SheafOfModules.IsFiniteLocallyFreeOfRank.isFiniteLocallyFree _ r)
    (∀ e : ℕ, (completedBivariantSequenceOfInvertible C sZ sX i hi
        (completedVirtualNormalGysinClass C sZ sX i hi 𝒩) ((r + e : ℕ) : ℤ)).cap g n
          (fundamentalChowClass C (g ≫ sX) n) =
        chowPushforwardOfIso C sZ' (pullback.fst i g ≫ sZ) sq.flip.isoPullback.hom
          (isoPullback_hom_comp_structureMorphism C sZ sX sq hi sZ' hi') (n - ((r + e : ℕ) : ℤ))
          (chowGroupDegreeEquiv C sZ' (by push_cast; ring)
            (topChernCap C sZ' (𝒩.baseChange i i' g' g sq).excessNormalSheaf (n - (r : ℤ)) e
              (fundamentalChowClass C sZ' (n - (r : ℤ)))))) ∧
      ∀ p : ℤ, p < r → (completedBivariantSequenceOfInvertible C sZ sX i hi
        (completedVirtualNormalGysinClass C sZ sX i hi 𝒩) p).cap g n
          (fundamentalChowClass C (g ≫ sX) n) = 0

Stacks.Chow.virtualNormalGysinCap_fundamentalChowClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/ExcessIntersection.lean, line 429. The attribute's comment: “at vanishing excess, where c_top(ℰ) = 1: c(Z ⟶ X, 𝒩) ∩ [Y]_n = [Z ×_X Y]_{n-m} for the class of Stacks 0FBK, proved from its characterizing relation; carried: ι_* j^* C on [Y]_n — 0F9J, 02TB and most of 0FBG and 0FBH are proved, but the map j : C_ZX ⟶ W_∞ is not, needing clauses (4) and (5) of 0FBG and condition (3) of 063M; see the implementation notes — injectivity of p^* (02TY), the δ-dim bound”.

Stacks 0FBM at vanishing excess. In the situation of the virtual normal sheaf, let g : Y ⟶ X be locally of finite type and assume that Z ×_X Y ⟶ Y is cut out by a regular sequence of length m, so that the excess normal sheaf vanishes and c_top(ℰ) = 1. If dim_δ(Z ×_X Y) ≤ n - m then

c(Z ⟶ X, 𝒩) ∩ [Y]_n = [Z ×_X Y]_{n - m}

in A_{n-m}(Z ×_X Y), for the class c of Stacks 0FBK, that is for any bivariant class of degree m satisfying the characterizing relation of that tag against the genuine flat pullback Stacks.Chow.bundleFlatPullback of the bundle projection.

The proof is the source's: the relation says p^*(c ∩ [Y]_n) = (ι_* ∘ j^* ∘ C) ∩ [Y]_n, the right-hand side is the fundamental class of N ×_X Y — the hypothesis hcone — and the left-hand side is p^* of the candidate, which is that same fundamental class by Stacks.Chow.bundleFlatPullbackChow_fundamentalChowClass; now divide by p^*.

See the implementation notes for what hcone, hinj and hdim are and why none of them is this conclusion.

theorem virtualNormalGysinCap_fundamentalChowClass
    (hinj : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C sZ sN i q hq m P.flat P.relativeDimension hdesc g k))
    {c : BivariantClass C G sZ sX i hi (m : ℤ)}
    (hc : IsVirtualNormalGysinClass C G sZ sX sN i hi q hq m 0 E
      (bundleFlatPullback C sZ sN i q hq m P.flat P.relativeDimension hdesc) P c)
    {Y : Scheme.{u}} (g : Y ⟶ X) [LocallyOfFiniteType g] (n : ℤ)
    (hdim : schemeDeltaDimension C (pullback.fst i g ≫ sZ) ≤ ((n - (m : ℤ) : ℤ) : EInt))
    (hcone : chowGroupDegreeEquiv C (pullback.fst (q ≫ i) g ≫ sN)
        (by omega : n - (0 : ℤ) = (n - (m : ℤ)) + (m : ℤ))
        (E.cap g n (fundamentalChowClass C (g ≫ sX) n)) =
      fundamentalChowClass C (pullback.fst (q ≫ i) g ≫ sN) ((n - (m : ℤ)) + (m : ℤ))) :
    c.cap g n (fundamentalChowClass C (g ≫ sX) n) =
      fundamentalChowClass C (pullback.fst i g ≫ sZ) (n - (m : ℤ))

Stacks.Chow.virtualNormalGysinCap_fundamentalChowClass_excess, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/ExcessIntersection.lean, line 478. The attribute's comment: “with excess: c(Z ⟶ X, 𝒩) ∩ [Y]_n = c_top(ℰ) ∩ [Z ×_X Y]_{n-r}, the normal cone given as a rank-r sub-bundle CN (063M) and c_top(ℰ) as the map cTop — Stacks.Chow.topChernClass of 0FA4 is proved, but assembled from the higher Chern classes, which are carried here as elsewhere in this directory; carried also: Stacks 0FAA for CN ⟶ N ×_X Y, proved at the constructed bundles of a short exact sequence but not at an arbitrary sub-bundle”.

Stacks 0FBM. In the situation of the virtual normal sheaf, let g : Y ⟶ X be locally of finite type, assume Z ×_X Y ⟶ Y is a regular closed immersion whose conormal sheaf has constant rank r, and let ℰ be the excess normal sheaf, of rank m - r. If dim_δ(Y) = n then

c(Z ⟶ X, 𝒩) ∩ [Y]_n = c_top(ℰ) ∩ [Z ×_X Y]_{n - r}

in A_{n-m}(Z ×_X Y).

The regular immersion and the excess sheaf enter through the data they produce: the normal cone C_{Z ×_X Y} Y is a vector bundle CN of rank r over Z ×_X Y, by the identification 𝒞_{*} = Sym(𝒞) of Stacks 063M, embedded in N ×_X Y over Z ×_X Y by ιC and pC; and the cap product with c_top(ℰ) is the additive map cTop, of degree m - r by its typing. See the implementation notes.

Besides the three hypotheses of Stacks.Chow.virtualNormalGysinCap_fundamentalChowClass the proof carries one statement, hexcess, which is Stacks 0FAA for the embedding CN ⟶ N ×_X Y of vector bundles over Z ×_X Y: ι_* (p')^* α = p^*(c_top(ℰ) ∩ α). That lemma is proved, as Stacks.Chow.subbundleEmbedding_pushforward_flatPullback_eq_topChernCap, but at the canonical constructed bundles of a short exact sequence rather than at an arbitrary sub-bundle CN, so it does not discharge the hypothesis as stated here; see the implementation notes. It is a formula in A_*(N ×_X Y), one bundle level above this conclusion, and mentions no bivariant class for Z ⟶ X.

theorem virtualNormalGysinCap_fundamentalChowClass_excess
    (hinj : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C sZ sN i q hq m P.flat P.relativeDimension hdesc g k))
    {c : BivariantClass C G sZ sX i hi (m : ℤ)}
    (hc : IsVirtualNormalGysinClass C G sZ sX sN i hi q hq m 0 E
      (bundleFlatPullback C sZ sN i q hq m P.flat P.relativeDimension hdesc) P c)
    {Y : Scheme.{u}} (g : Y ⟶ X) [LocallyOfFiniteType g] (n : ℤ) (r : ℕ)
    (hdim : schemeDeltaDimension C (pullback.fst i g ≫ sZ) ≤ ((n - (r : ℤ) : ℤ) : EInt))
    {CN : Scheme.{u}} (ιC : CN ⟶ pullback (q ≫ i) g) [IsClosedImmersion ιC]
    (pC : CN ⟶ pullback i g) [LocallyOfFiniteType pC] [AlgebraicGeometry.Flat pC]
    (hpC : AlgebraicGeometry.RelativeDimension pC r)
    (hCN : ιC ≫ bundleTestBaseChange i q g = pC)
    (cTop : chowGroup C (pullback.fst i g ≫ sZ) (n - (r : ℤ)) →+
      chowGroup C (pullback.fst i g ≫ sZ) (n - (m : ℤ)))
    (hcone : chowGroupDegreeEquiv C (pullback.fst (q ≫ i) g ≫ sN)
        (by omega : n - (0 : ℤ) = (n - (r : ℤ)) + (r : ℤ))
        (E.cap g n (fundamentalChowClass C (g ≫ sX) n)) =
      chowPushforwardOfIsClosedImmersion C (pC ≫ (pullback.fst i g ≫ sZ))
        (pullback.fst (q ≫ i) g ≫ sN) ιC
        (by rw [← bundleTestBaseChange_comp_structureMorphism i q sZ sN hq g,
          ← Category.assoc, hCN]) ((n - (r : ℤ)) + (r : ℤ))
        (fundamentalChowClass C (pC ≫ (pullback.fst i g ≫ sZ)) ((n - (r : ℤ)) + (r : ℤ))))
    (hexcess : ∀ α : chowGroup C (pullback.fst i g ≫ sZ) (n - (r : ℤ)),
      chowGroupDegreeEquiv C (pullback.fst (q ≫ i) g ≫ sN)
          (by omega : (n - (m : ℤ)) + (m : ℤ) = (n - (r : ℤ)) + (r : ℤ))
          (bundleFlatPullbackChow C sZ sN i q hq m P.flat P.relativeDimension hdesc g
            (n - (m : ℤ)) (cTop α)) =
        chowPushforwardOfIsClosedImmersion C (pC ≫ (pullback.fst i g ≫ sZ))
          (pullback.fst (q ≫ i) g ≫ sN) ιC
          (by rw [← bundleTestBaseChange_comp_structureMorphism i q sZ sN hq g,
            ← Category.assoc, hCN]) ((n - (r : ℤ)) + (r : ℤ))
          (flatPullbackChow C (pC ≫ (pullback.fst i g ≫ sZ)) (pullback.fst i g ≫ sZ) pC rfl r hpC
            (n - (r : ℤ))
            (hdesc (pC ≫ (pullback.fst i g ≫ sZ)) (pullback.fst i g ≫ sZ) pC rfl r hpC
              (n - (r : ℤ))) α)) :
    c.cap g n (fundamentalChowClass C (g ≫ sX) n) =
      cTop (fundamentalChowClass C (pullback.fst i g ≫ sZ) (n - (r : ℤ)))

Tag 0FEA, a lemma

Tag 0FEA in the Stacks Project.

Stacks.Chow.virtualNormalGysinClass_cap_fundamentalChowClass_of_isCohenMacaulayLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalCapCohenMacaulay.lean, line 67.

Stacks 0FEA. Let (S, δ) be as in Stacks 02QL, let X be locally of finite type over S, let 𝒩 be a virtual normal sheaf for a closed subscheme i : Z ⟶ X (Stacks 0FBQ), and let g : Y ⟶ X be locally of finite type. Given integers r and n, assume

1. 𝒩 is locally free of rank r,
2. every irreducible component of Y has δ-dimension n,
3. dim_δ(Z ×_X Y) ≤ n - r, and
4. 𝒪_{Y, ξ} is Cohen–Macaulay for every ξ ∈ Z ×_X Y with δ(ξ) = n - r.

Then c(Z ⟶ X, 𝒩) ∩ [Y]_n = [Z ×_X Y]_{n - r} in CH_{n - r}(Z ×_X Y).

The proof is the source's: at the points of Z ×_X Y of δ-dimension n - r the ideal of Z ×_X Y is generated by a regular sequence of length r, so Z ×_X Y ⟶ Y is a regular closed immersion of codimension r near them, where the excess normal sheaf vanishes and Stacks 0FBM (Stacks.Chow.virtualNormalGysinClass_capRegularFormula) applies; this is Stacks.Chow.BivariantClass.cap_fundamentalChowClass_eq_of_capRegularFormula.

theorem virtualNormalGysinClass_cap_fundamentalChowClass_of_isCohenMacaulayLocalRing
    [LocallyOfFiniteType i] {n : ℤ} {Y : Scheme.{u}} (g : Y ⟶ X) [LocallyOfFiniteType g]
    (hY : ∀ W : irreducibleComponents Y,
      deltaDimension C (g ≫ sX)
        ⟨W, W.2.1, isClosed_of_mem_irreducibleComponents (W : Set Y) W.2⟩ = n)
    (hZY : schemeDeltaDimension C (pullback.snd i g ≫ (g ≫ sX)) ≤ ((n - r : ℤ) : EInt))
    (hCM : ∀ ξ : (pullback i g : Scheme.{u}),
      relativeDimension C.dimensionFunction (g ≫ sX) ((pullback.snd i g).base ξ) = n - r →
      letI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian (g ≫ sX)
      IsCohenMacaulayLocalRing (Y.presheaf.stalk ((pullback.snd i g).base ξ))) :
    (virtualNormalBundleClass C sZ sX i hi 𝒩 r).cap g n (fundamentalChowClass C (g ≫ sX) n) =
      fundamentalChowClass C (pullback.fst i g ≫ sZ) (n - r)

Stacks.Chow.isRegular_of_isCohenMacaulayLocalRing_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalCapFundamental.lean, line 238. The attribute's comment: “the regular sequence of the proof: hypotheses (1)-(4) force the ideal of Z ×_X Y in 𝒪_{Y, ξ} to be generated by a regular sequence of length r at every point of Z ×_X Y of δ-dimension n - r. The cap product c(Z ⟶ X, 𝒩) ∩ [Y]_n is NOT stated, Stacks 0FBK having no carrier here. See the implementation notes”.

Stacks 0FEA, the regular sequence of the proof. Let (S, δ) be as in Stacks 02QL, let X be locally of finite type over S, let i : Z ⟶ X be a closed subscheme and let g : Y ⟶ X be locally of finite type. Assume

• every irreducible component of Y has δ-dimension n (hypothesis (2)),
• dim_δ(Z ×_X Y) ≤ n - r (hypothesis (3)),
• ξ ∈ Z ×_X Y has δ(ξ) = n - r and 𝒪_{Y, ξ} is Cohen–Macaulay (hypothesis (4)), and
• the ideal of Z ×_X Y in 𝒪_{Y, ξ} is generated by a list xs of r elements, which is what hypothesis (1) provides.

Then xs is a regular sequence. Equivalently: Z ×_X Y is cut out of Y by a regular sequence of length r at every point of δ-dimension n - r, which is what the source establishes before invoking the excess intersection formula of Stacks 0FBM to conclude c(Z ⟶ X, 𝒩) ∩ [Y]_n = [Z ×_X Y]_{n - r}. See the implementation notes for why that conclusion is not stated.

theorem isRegular_of_isCohenMacaulayLocalRing_stalk (C : ChowSituation.{u})
    {X Y Z : Scheme.{u}} (sX : X ⟶ C.S) [LocallyOfFiniteType sX]
    (i : Z ⟶ X) [IsClosedImmersion i] (g : Y ⟶ X) [LocallyOfFiniteType g] {n : ℤ} {r : ℕ}
    (hY : ∀ W : irreducibleComponents Y,
      deltaDimension C (g ≫ sX)
        ⟨W, W.2.1, isClosed_of_mem_irreducibleComponents (W : Set Y) W.2⟩ = n)
    (hZY : schemeDeltaDimension C (pullback.snd i g ≫ (g ≫ sX)) ≤ ((n - r : ℤ) : EInt))
    (ξ : (pullback i g : Scheme.{u}))
    (hξ : relativeDimension C.dimensionFunction (g ≫ sX) ((pullback.snd i g).base ξ) = n - r)
    (hCM : letI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian (g ≫ sX)
      IsCohenMacaulayLocalRing (Y.presheaf.stalk ((pullback.snd i g).base ξ)))
    (xs : List (Y.presheaf.stalk ((pullback.snd i g).base ξ))) (hlen : xs.length = r)
    (hxs : Ideal.ofList xs = RingHom.ker ((pullback.snd i g).stalkMap ξ).hom) :
    RingTheory.Sequence.IsRegular (Y.presheaf.stalk ((pullback.snd i g).base ξ)) xs

Tag 0FBN, a lemma

Tag 0FBN in the Stacks Project.

Stacks.Chow.gysinBivariantClass_eq_virtualNormalBundleClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/DivisorVirtualNormalBundleClass.lean, line 334.

Stacks 0FBN. Let (S, δ) be as in Situation 02QL, let X be locally of finite type over S and let (ℒ, s, i : D ⟶ X) be a triple as in Definition 02T8. The Gysin homomorphism i^*, viewed as an element of A^1(D ⟶ X) (Stacks 0B79, Stacks.Chow.gysinBivariantClass), is the bivariant class c(D ⟶ X, 𝒩) ∈ A^1(D ⟶ X) of Stacks 0FBK (Stacks.Chow.virtualNormalBundleClass) constructed using 𝒩 = i^*ℒ viewed as a virtual normal sheaf for D in X (Stacks.Chow.zeroSchemeVirtualNormalBundle, with the canonical surjection (i^*ℒ)^∨ ⟶ 𝒞_{D/X}).

This is Stacks.Chow.gysinBivariantClass_eq_virtualNormalBundleClass_of_iso, which holds for any surjection (i^*ℒ)^∨ ⟶ 𝒞_{D/X}, at the canonical one.

theorem gysinBivariantClass_eq_virtualNormalBundleClass :
    (gysinBivariantClass C sX L s).1 =
      virtualNormalBundleClass C (gysinTripleInclusion L s ≫ sX) sX (gysinTripleInclusion L s)
        rfl (zeroSchemeVirtualNormalBundle L s) 1

Stacks.Chow.gysinBivariantCap_eq_virtualNormalGysinCap_of_offDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/DivisorVirtualNormalClass.lean, line 262. The attribute's comment: “the case of a test scheme not contained in D: the value of the virtual normal class there, which is Tag 0FBM at vanishing excess. The Gysin side of this case is carried; see Stacks.Chow.gysinBivariantClass_eq_virtualNormalGysinClass”.

The first case of the proof of Stacks 0FBN. On an integral test scheme Y not contained in the divisor, the Gysin cap operation and the cap operation of c(D ⟶ X, 𝒩) both send [Y]_n to the fundamental class of D ×_X Y in degree n - 1.

The Gysin value is the carried Stacks.Chow.GysinCapFundamentalOffDivisor; the value of c(D ⟶ X, 𝒩) is Stacks 0FBM at vanishing excess, Stacks.Chow.virtualNormalGysinCap_fundamentalChowClass, whose three hypotheses — the injectivity of Stacks 02TY, the value of ι_* ∘ j^* ∘ C on the fundamental class, and the δ-dimension bound — appear here as hinj, hcone and hdim.

theorem gysinBivariantCap_eq_virtualNormalGysinCap_of_offDivisor
    (hinj : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C (gysinTripleInclusion L s ≫ sX) sNB (gysinTripleInclusion L s) q hq
          1 P.flat P.relativeDimension hdesc g k))
    {c : BivariantClass C G (gysinTripleInclusion L s ≫ sX) sX (gysinTripleInclusion L s) rfl
      ((1 : ℕ) : ℤ)}
    (hc : IsVirtualNormalGysinClass C G (gysinTripleInclusion L s ≫ sX) sX sNB
      (gysinTripleInclusion L s) rfl q hq 1 0 E
      (bundleFlatPullback C (gysinTripleInclusion L s ≫ sX) sNB (gysinTripleInclusion L s) q hq 1
        P.flat P.relativeDimension hdesc) P c)
    (hoff : GysinCapFundamentalOffDivisor C G sX L s)
    {Y : Scheme.{u}} (g : Y ⟶ X) [LocallyOfFiniteType g] [IsIntegral Y] (n : ℤ)
    (hY : ¬ ∃ h : Y ⟶ (Stacks.Divisors.zeroScheme X L s).subscheme,
      h ≫ gysinTripleInclusion L s = g)
    (hdim : schemeDeltaDimension C
        (pullback.fst (gysinTripleInclusion L s) g ≫ (gysinTripleInclusion L s ≫ sX)) ≤
      ((n - ((1 : ℕ) : ℤ) : ℤ) : EInt))
    (hcone : chowGroupDegreeEquiv C
        (pullback.fst (q ≫ gysinTripleInclusion L s) g ≫ sNB)
        (by omega : n - (0 : ℤ) = (n - ((1 : ℕ) : ℤ)) + ((1 : ℕ) : ℤ))
        (E.cap g n (fundamentalChowClass C (g ≫ sX) n)) =
      fundamentalChowClass C (pullback.fst (q ≫ gysinTripleInclusion L s) g ≫ sNB)
        ((n - ((1 : ℕ) : ℤ)) + ((1 : ℕ) : ℤ))) :
    gysinBivariantCap C G sX L s g n (fundamentalChowClass C (g ≫ sX) n) =
      c.cap g n (fundamentalChowClass C (g ≫ sX) n)

Stacks.Chow.gysinBivariantClass_eq_virtualNormalGysinClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/DivisorVirtualNormalClass.lean, line 317. The attribute's comment: “the Gysin homomorphism i^ of a triple (L, s, i : D -> X) as in Definition 02T8 and the virtual normal class c(D -> X, i^L) of Tag 0FBK agree in A^1(D -> X). Both classes are the ones CHARACTERIZED by their tags (Tag 0B79 via IsGysinBivariantClass, Tag 0FBK via IsVirtualNormalGysinClass), neither being constructed here; the virtual normal sheaf is data with its module identified with i^L, the canonical surjection C_{D/X} = (i^L)^v being absent. THE TAG IS NOT FULLY CLOSED. Proved: the Tag 02UC reduction to integral test schemes, and for a test scheme NOT contained in D the value of the virtual normal class, which is Tag 0FBM at vanishing excess. CARRIED: the value of the Gysin homomorphism on a fundamental class in BOTH cases (Definition 02T8 and Tag 02TB are proved only at a closed subscheme of the test scheme against an intersection cycle, not at the fundamental class of the base change D x_X Y), and the value of the virtual normal class in the case Y contained in D (Tag 0FBM at full excess). THE CONTAINED CASE IS THEREFORE DOCUMENTED BUT NOT DISCHARGED. Also carried: Tag 02TY injectivity and Tag 02S1 descent. The Tag 02UC used for the reduction to integral test schemes is unconditional”.

Stacks 0FBN. Let (S, δ) be the base situation of chapter 42, let X be locally of finite type over S and let (ℒ, s, i : D ⟶ X) be a triple as in Definition 02T8. Let 𝒩 = i^*ℒ, a virtual normal sheaf of rank one for D in X. Then the Gysin homomorphism i^*, viewed as an element of A^1(D ⟶ X) by Stacks 0B79, is the bivariant class c(D ⟶ X, 𝒩) of Stacks 0FBK.

The proof is the source's: by Stacks 02UC it is enough to compare the two classes on the fundamental class of every integral test scheme, and there the two cases of the source are Stacks.Chow.gysinBivariantCap_eq_virtualNormalGysinCap_of_offDivisor and the pair of carried values hon, hvn on an integral test scheme contained in D. See the implementation notes for what is carried in each case.

theorem gysinBivariantClass_eq_virtualNormalGysinClass
    (cTop : DivisorTopChernCapFamily C sX L s)
    (hinj : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C (gysinTripleInclusion L s ≫ sX) sNB (gysinTripleInclusion L s) q hq
          1 P.flat P.relativeDimension hdesc g k))
    (_hbundle : P.normalBundle.bundle =
      (Scheme.Modules.pullback (gysinTripleInclusion L s)).obj L)
    {gys c : BivariantClass C G (gysinTripleInclusion L s ≫ sX) sX (gysinTripleInclusion L s) rfl
      ((1 : ℕ) : ℤ)}
    (hgys : IsGysinBivariantClass C G sX L s gys)
    (hc : IsVirtualNormalGysinClass C G (gysinTripleInclusion L s ≫ sX) sX sNB
      (gysinTripleInclusion L s) rfl q hq 1 0 E
      (bundleFlatPullback C (gysinTripleInclusion L s ≫ sX) sNB (gysinTripleInclusion L s) q hq 1
        P.flat P.relativeDimension hdesc) P c)
    (hoff : GysinCapFundamentalOffDivisor C G sX L s)
    (hon : GysinCapFundamentalOnDivisor C G sX L s cTop)
    (hvn : VirtualNormalCapFundamentalOnDivisor C G sX L s cTop c)
    (hdim : ∀ {Y : Scheme.{u}} (g : Y ⟶ X) [LocallyOfFiniteType g] (n : ℤ),
      (¬ ∃ h : Y ⟶ (Stacks.Divisors.zeroScheme X L s).subscheme,
      h ≫ gysinTripleInclusion L s = g) →
      schemeDeltaDimension C
          (pullback.fst (gysinTripleInclusion L s) g ≫ (gysinTripleInclusion L s ≫ sX)) ≤
        ((n - ((1 : ℕ) : ℤ) : ℤ) : EInt))
    (hcone : ∀ {Y : Scheme.{u}} (g : Y ⟶ X) [LocallyOfFiniteType g] (n : ℤ),
      (¬ ∃ h : Y ⟶ (Stacks.Divisors.zeroScheme X L s).subscheme,
      h ≫ gysinTripleInclusion L s = g) →
      chowGroupDegreeEquiv C (pullback.fst (q ≫ gysinTripleInclusion L s) g ≫ sNB)
          (by omega : n - (0 : ℤ) = (n - ((1 : ℕ) : ℤ)) + ((1 : ℕ) : ℤ))
          (E.cap g n (fundamentalChowClass C (g ≫ sX) n)) =
        fundamentalChowClass C (pullback.fst (q ≫ gysinTripleInclusion L s) g ≫ sNB)
          ((n - ((1 : ℕ) : ℤ)) + ((1 : ℕ) : ℤ))) :
    gys = c

Tag 0FBP, a lemma

Tag 0FBP in the Stacks Project.

Stacks.Chow.virtualNormalGysinClass_bivariantCommute_of_subbundle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/VirtualNormalCommuting.lean, line 355. The attribute's comment: “with the factorization c(Z ⟶ X, 𝒩) = c_top(ℰ) ∘ c(Z ⟶ X, 𝒩') PROVED, by consuming Stacks 0FBL for a short exact sequence 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0. CARRIED: the centrality of the top Chern cap of ℰ for c (Stacks 02UA, formalized only against the projective bundle rule and not this directory's carried cap rule), and that c commutes with c(Z ⟶ X, 𝒩')”.

Stacks 0FBP with the factorization proved. Let i : Z ⟶ X be a closed subscheme with virtual normal sheaf 𝒩 of constant rank m, let 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free modules whose conormal surjection factors as Stacks 0FBL asks, let g : Y ⟶ X be locally of finite type and let c ∈ A^p(Y ⟶ X). If c commutes with c(Z ⟶ X, 𝒩') and the top Chern cap of ℰ is central for c, then c commutes with c(Z ⟶ X, 𝒩).

The factorization c(Z ⟶ X, 𝒩) = c_top(ℰ) ∘ c(Z ⟶ X, 𝒩') is not carried here: it is Stacks 0FBL, Stacks.Chow.virtualNormalGysinCap_eq_topChernCap_comp, and its hypotheses — the short exact sequence, the factoring of the conormal surjection, the injectivity of Stacks 02TY, and the two carried inputs of that tag — are threaded through. What is carried is the centrality of the top Chern cap, which is Stacks 02UA; the commutation with c(Z ⟶ X, 𝒩') is a hypothesis here and is discharged for a divisor in Stacks.Chow.virtualNormalGysinClass_bivariantCommute_of_divisor.

theorem virtualNormalGysinClass_bivariantCommute_of_subbundle
    (w : inc ≫ pr = 0) (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (hsigma : dualMap inc ≫ P'.normalBundle.surjection = P.normalBundle.surjection) (x : Z)
    (hinj : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C (i ≫ sX) sN i q hq m P.flat P.relativeDimension hdesc g k))
    (hfactor : SubbundleGysinFactorization C G (i ≫ sX) sX sN sN' i rfl q q' hq hq' j hj E E')
    (hstep : SubbundleGysinTopChernStep C (i ≫ sX) sN sN' i q q' hq hq' j hj m m' e Eb cap hdesc
      P P')
    {cN : BivariantClass C G (i ≫ sX) sX i rfl (m : ℤ)}
    {cN' : BivariantClass C G (i ≫ sX) sX i rfl (m' : ℤ)}
    (c : BivariantClass C G (f ≫ sX) sX f rfl p)
    (hcN : IsVirtualNormalGysinClass C G (i ≫ sX) sX sN i rfl q hq m 0 E
      (bundleFlatPullback C (i ≫ sX) sN i q hq m P.flat P.relativeDimension hdesc) P cN)
    (hcN' : IsVirtualNormalGysinClass C G (i ≫ sX) sX sN' i rfl q' hq' m' 0 E'
      (bundleFlatPullback C (i ≫ sX) sN' i q' hq' m' P'.flat P'.relativeDimension hdesc) P' cN')
    (hcentral : ExcessChernCapCommutesWithCap C G sX i f (m' : ℤ) (m : ℤ) p c
      (subbundleExcessChernOperator C sX i m m' e Eb cap P P' inc pr w hseq x))
    (hb : BivariantCommute C G sX i f (m' : ℤ) p cN' c) :
    BivariantCommute C G sX i f (m : ℤ) p cN c

Stacks.Chow.virtualNormalGysinClass_bivariantCommute_of_divisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Bivariant/VirtualNormalCommuting.lean, line 431. The attribute's comment: “the effective Cartier divisor case, the case the source's reduction lands in. PROVED by consuming Stacks 0FBL (the factorization through the rank-one subsheaf), 0FBN (that factor is the Gysin class i^) and 0FA3 (i^ commutes with c), with their own hypotheses threaded. CARRIED: only the centrality of the top Chern cap of ℰ, Stacks 02UA”.

Stacks 0FBP for an effective Cartier divisor, the case the source's reduction lands in. Let (𝓛, s, i : Z ⟶ X) be a triple as in Stacks 02T8, so that Z is the zero scheme of s and hence an effective Cartier divisor, let 𝒩 be a virtual normal sheaf for i of constant rank m, let 𝒩' = i^*𝓛 be the rank-one virtual normal sheaf of the divisor sitting inside 𝒩 with quotient the excess sheaf ℰ, let g : Y ⟶ X be locally of finite type and let c ∈ A^p(Y ⟶ X). Then c(Z ⟶ X, 𝒩) commutes with c.

This is the source's argument with everything but one input discharged. The factorization c(Z ⟶ X, 𝒩) = c_top(ℰ) ∘ c(Z ⟶ X, 𝒩') is Stacks 0FBL; the identification of the second factor with the Gysin homomorphism i^* of Stacks 0B79 is Stacks 0FBN, Stacks.Chow.gysinBivariantClass_eq_virtualNormalGysinClass; and the commutation of i^* with c is Stacks 0FA3, Stacks.Chow.gysinBivariantCommute, which derives it from the Gysin condition in the definition of a bivariant class. The one carried input is the centrality of the top Chern cap of ℰ, Stacks 02UA.

theorem virtualNormalGysinClass_bivariantCommute_of_divisor
    (w : inc ≫ pr = 0) (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (hsigma : dualMap inc ≫ P'.normalBundle.surjection = P.normalBundle.surjection)
    (x : (Stacks.Divisors.zeroScheme X L s).subscheme)
    (hinj : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C (gysinTripleInclusion L s ≫ sX) sN (gysinTripleInclusion L s) q hq
          m P.flat P.relativeDimension hdesc g k))
    (hinj' : ∀ {T : Scheme.{u}} (g : T ⟶ X) [LocallyOfFiniteType g] (k : ℤ),
      Function.Injective
        (bundleFlatPullback C (gysinTripleInclusion L s ≫ sX) sN' (gysinTripleInclusion L s) q'
          hq' 1 P'.flat P'.relativeDimension hdesc g k))
    (hfactor : SubbundleGysinFactorization C G (gysinTripleInclusion L s ≫ sX) sX sN sN'
      (gysinTripleInclusion L s) rfl q q' hq hq' j hj E E')
    (hstep : SubbundleGysinTopChernStep C (gysinTripleInclusion L s ≫ sX) sN sN'
      (gysinTripleInclusion L s) q q' hq hq' j hj m 1 e Eb cap hdesc P P')
    (cTop : DivisorTopChernCapFamily C sX L s)
    (hbundle : P'.normalBundle.bundle =
      (Scheme.Modules.pullback (gysinTripleInclusion L s)).obj L)
    (hG : G.IsNaturalUnderPullbackCompPushforward)
    {cN : BivariantClass C G (gysinTripleInclusion L s ≫ sX) sX (gysinTripleInclusion L s)
      rfl (m : ℤ)}
    {cN' gys : BivariantClass C G (gysinTripleInclusion L s ≫ sX) sX (gysinTripleInclusion L s)
      rfl ((1 : ℕ) : ℤ)}
    (c : BivariantClass C G (f ≫ sX) sX f rfl p)
    (hcN : IsVirtualNormalGysinClass C G (gysinTripleInclusion L s ≫ sX) sX sN
      (gysinTripleInclusion L s) rfl q hq m 0 E
      (bundleFlatPullback C (gysinTripleInclusion L s ≫ sX) sN (gysinTripleInclusion L s) q hq m
        P.flat P.relativeDimension hdesc) P cN)
    (hcN' : IsVirtualNormalGysinClass C G (gysinTripleInclusion L s ≫ sX) sX sN'
      (gysinTripleInclusion L s) rfl q' hq' 1 0 E'
      (bundleFlatPullback C (gysinTripleInclusion L s ≫ sX) sN' (gysinTripleInclusion L s) q'
        hq' 1 P'.flat P'.relativeDimension hdesc) P' cN')
    (hgys : IsGysinBivariantClass C G sX L s gys)
    (hoff : GysinCapFundamentalOffDivisor C G sX L s)
    (hon : GysinCapFundamentalOnDivisor C G sX L s cTop)
    (hvn : VirtualNormalCapFundamentalOnDivisor C G sX L s cTop cN')
    (hdim : ∀ {W : Scheme.{u}} (g : W ⟶ X) [LocallyOfFiniteType g] (n : ℤ),
      (¬ ∃ h : W ⟶ (Stacks.Divisors.zeroScheme X L s).subscheme,
        h ≫ gysinTripleInclusion L s = g) →
      schemeDeltaDimension C
          (pullback.fst (gysinTripleInclusion L s) g ≫ (gysinTripleInclusion L s ≫ sX)) ≤
        ((n - ((1 : ℕ) : ℤ) : ℤ) : EInt))
    (hcone : ∀ {W : Scheme.{u}} (g : W ⟶ X) [LocallyOfFiniteType g] (n : ℤ),
      (¬ ∃ h : W ⟶ (Stacks.Divisors.zeroScheme X L s).subscheme,
        h ≫ gysinTripleInclusion L s = g) →
      chowGroupDegreeEquiv C (pullback.fst (q' ≫ gysinTripleInclusion L s) g ≫ sN')
          (by omega : n - (0 : ℤ) = (n - ((1 : ℕ) : ℤ)) + ((1 : ℕ) : ℤ))
          (E'.cap g n (fundamentalChowClass C (g ≫ sX) n)) =
        fundamentalChowClass C (pullback.fst (q' ≫ gysinTripleInclusion L s) g ≫ sN')
          ((n - ((1 : ℕ) : ℤ)) + ((1 : ℕ) : ℤ)))
    (hcentral : ExcessChernCapCommutesWithCap C G sX (gysinTripleInclusion L s) f
      ((1 : ℕ) : ℤ) (m : ℤ) p c
      (subbundleExcessChernOperator C sX (gysinTripleInclusion L s) m 1 e Eb cap P P' inc pr w
        hseq x)) :
    BivariantCommute C G sX (gysinTripleInclusion L s) f (m : ℤ) p cN c

Stacks.Chow.VirtualNormalBundle.completedClass_bivariantCommute, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VirtualNormalClass/Commuting.lean, line 459. The attribute's comment: “c(Z → X, 𝒩) ∈ A^*(Z → X)^∧ of Tag 0FBK commutes (Remark 0FA2) with every c ∈ A^p(Y → X), Y → X locally of finite type: each homogeneous part c(Z → X, 𝒩)_n and c commute on every test scheme T → X; 𝒩 a virtual normal sheaf of arbitrary rank”.

Stacks 0FBP. Let (S, δ) be as in Situation 02QL, let X be a scheme locally of finite type over S, let Z ⊆ X be a closed subscheme with virtual normal sheaf 𝒩, let g : Y ⟶ X be locally of finite type and let c ∈ A^p(Y ⟶ X). Then c and the class c(Z ⟶ X, 𝒩) ∈ A^*(Z ⟶ X)^∧ of Stacks 0FBK commute in the sense of Remark 0FA2: for every degree n, the degree n part of c(Z ⟶ X, 𝒩) and c satisfy c(Z ⟶ X, 𝒩)_n ∩ (c ∩ α) = c ∩ (c(Z ⟶ X, 𝒩)_n ∩ α) in CH_{k-n-p}(Z ×_X Y ×_X T) for every α ∈ CH_k(T) and every T ⟶ X locally of finite type (Stacks.Chow.BivariantCommute). As commuting is additive in c, this is the commutation with every c ∈ A^*(Y ⟶ X).

The rank of 𝒩 is arbitrary. The class is Stacks.Chow.VirtualNormalBundle.completedClass, the class constructed in Stacks 0FBK from the class C of Stacks 0F9J, the normal cone and the vector bundle of 𝒩; Z lies over S through X.

theorem VirtualNormalBundle.completedClass_bivariantCommute (𝒩 : VirtualNormalBundle i)
    {Y : Scheme.{u}} (g : Y ⟶ X) [LocallyOfFiniteType g] (n p : ℤ)
    (c : BivariantClass C (gysinSystemOfInvertible C) (g ≫ sX) sX g rfl p) :
    haveI := LocallyOfFiniteType.isLocallyNoetherian (i ≫ sX)
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    BivariantCommute C (gysinSystemOfInvertible C) sX i g n p
      (completedBivariantSequenceOfInvertible C (i ≫ sX) sX i rfl
        (𝒩.completedClass C sX (i ≫ sX) rfl) n) c

Tag 0FEB, a lemma

Tag 0FEB in the Stacks Project.

Stacks.Chow.gysinBivariantCap_fundamentalChowClass_normalCone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/NormalConeZeroSectionGysin.lean, line 851. The attribute's comment: “PROVED, at the canonical Gysin system Stacks.Chow.canonicalGysinSystem (whose contained-component rule is the first Chern class of the restricted invertible module, Stacks 02SO), which is the o^* of the source. No hypothesis beyond the source's: X integral, locally of finite type over the base of delta-dimension n, Z and Y effective Cartier divisors with Z inside Y. The closed immersion C_ZY -> Y x_{o, C_YX} C_ZX that the source leaves implicit is constructed, as Stacks.Chow.normalConeToZeroFibre, the unique morphism with the two components the source names (Stacks.Chow.normalConeZeroSectionGysinRelation_hom_ext). The proof goes through the deformation to the normal cone D(Z in X) and Tags 0B73, 02TB, 02TA, 02T9 and 0C4U rather than through the blowups of Tag 0FBG used by the source.”.

Stacks Project, Tag 0FEB. Let (S, δ) be as in Situation 02QL, let X be an integral scheme locally of finite type over S of δ-dimension n, and let Z ⊆ Y ⊆ X be closed subschemes which are both effective Cartier divisors in X. Write o : Y ⟶ C_YX for the zero section of the normal line cone of Y in X. Then

`o^*[C_ZX]_n = [C_ZY]_{n-1}` in `CH_{n-1}(Y ×_{o, C_YX} C_ZX)`.

Here Y and Z are DY.subscheme and DZ.subscheme, Z ⊆ Y is hZY : DY ≤ DZ, o is Stacks.Conormal.normalConeZeroSection, the morphism C_ZX ⟶ C_YX is Stacks.Conormal.normalConeMapOfFactorization, o^* is the cap operation Stacks.Chow.gysinBivariantCap of the canonical Gysin system at the presentation of o(Y) by Stacks.Chow.zeroSectionDivisorSheaf and Stacks.Chow.zeroSectionDivisorSection, and the closed immersion C_ZY ⟶ Y ×_{o, C_YX} C_ZX is Stacks.Chow.normalConeToZeroFibre.

The proof is by the deformation to the normal cone M = D(Z ⊆ X), of δ-dimension at most n + 1. It carries the divisor Z(t⁻¹) ≅ C_ZX and the divisor E_Z, the inverse image of the strict transform E of Y in D(Y ⊆ X). On C_ZX the restriction of 𝒪(E_Z) with its canonical section is g^*𝒪(o(Y)) with its canonical section (Stacks 0C4U, as κ_Y⁻¹E = o(Y)), so the left-hand side is 1_{E_Z}|^* (t⁻¹)^*[M]_{n+1} (Stacks 02TB(1) and 02TA). By [Stacks, Tag 0B73] this is (t⁻¹)|^* 1_{E_Z}^*[M] = (t⁻¹)|^*[E_Z]; [E_Z] and [D(Z ⊆ Y)] differ by a cycle supported in Z(t⁻¹), on which the Gysin map of the trivial module kills it (Stacks 02T9); and (t⁻¹)|^*[D(Z ⊆ Y)] = [D(Z ⊆ Y) ∩ Z(t⁻¹)] = [C_ZY] by [Stacks, Tag 02TB].

theorem gysinBivariantCap_fundamentalChowClass_normalCone [IsIntegral X]
    (hn : schemeDeltaDimension C sX = (n : EInt)) :
    gysinBivariantCap C (canonicalGysinSystem C)
        (Stacks.Conormal.normalConeToBase DY.subschemeι ≫ DY.subschemeι ≫ sX)
        (zeroSectionDivisorSheaf DY) (zeroSectionDivisorSection DY)
        (Stacks.Conormal.normalConeMapOfFactorization DZ.subschemeι DY.subschemeι (inclusion hZY)
          (inclusion_subschemeι hZY)) n
        (fundamentalChowClass C
          (Stacks.Conormal.normalConeMapOfFactorization DZ.subschemeι DY.subschemeι
              (inclusion hZY) (inclusion_subschemeι hZY) ≫
            (Stacks.Conormal.normalConeToBase DY.subschemeι ≫ DY.subschemeι ≫ sX)) n) =
      QuotientAddGroup.mk'
        (rationalEquivalences C
          (pullback.fst
              (gysinTripleInclusion (zeroSectionDivisorSheaf DY) (zeroSectionDivisorSection DY))
              (Stacks.Conormal.normalConeMapOfFactorization DZ.subschemeι DY.subschemeι
                (inclusion hZY) (inclusion_subschemeι hZY)) ≫
            (gysinTripleInclusion (zeroSectionDivisorSheaf DY) (zeroSectionDivisorSection DY) ≫
              (Stacks.Conormal.normalConeToBase DY.subschemeι ≫ DY.subschemeι ≫ sX)))
          (n - 1))
        (cycleAssociatedToClosedSubscheme C
          (pullback.fst
              (gysinTripleInclusion (zeroSectionDivisorSheaf DY) (zeroSectionDivisorSection DY))
              (Stacks.Conormal.normalConeMapOfFactorization DZ.subschemeι DY.subschemeι
                (inclusion hZY) (inclusion_subschemeι hZY)) ≫
            (gysinTripleInclusion (zeroSectionDivisorSheaf DY) (zeroSectionDivisorSection DY) ≫
              (Stacks.Conormal.normalConeToBase DY.subschemeι ≫ DY.subschemeι ≫ sX)))
          (normalConeToZeroFibre DY DZ.subschemeι (inclusion hZY) (inclusion_subschemeι hZY))
          (n - 1))

Stacks.Chow.gysinBivariantClass_cap_normalCone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/NormalLineConeZeroSectionGysin.lean, line 598.

Stacks 0FEB. Let (S, δ) be as in Situation 02QL, let X be a scheme locally of finite type over S with dim_δ(X) ≤ n (the source: X integral of δ-dimension n), and let Z ⊆ Y ⊆ X be closed subschemes, iZY : Z ⟶ Y the inclusion, with Y an effective Cartier divisor in X (the source also asks it of Z; that is not used). Let o : Y ⟶ C_YX be the zero section of the normal line cone, o(Y) = D0 = normalConeZeroSectionIdeal iY (Stacks.Chow.ker_normalConeZeroSection), an effective Cartier divisor of C_YX (Stacks.Chow.isEffectiveCartierDivisor_normalConeZeroSectionIdeal), and let o^* ∈ A^1(Y ⟶ C_YX) be its Gysin class (Stacks 0B79, Stacks.Chow.gysinBivariantClass, for the canonical section of 𝒪(D0)). Let φ : C_ZX ⟶ C_YX be the canonical morphism of normal cones induced by ℐ_Y ⊆ ℐ_Z (Stacks.Chow.normalConeChangeOfCentreMap; on charts it is Spec Gr_{ℐ_Z} ⟶ Spec Gr_{ℐ_Y}). Then

o^*[C_ZX]_n = [C_ZY]_{n-1} in CH_{n-1}(Y ×_{o, C_YX} C_ZX),

where the fibre product is the base change of o(Y) ⊆ C_YX along φ (Stacks 0B6Y) and [C_ZY]_{n-1} is pushed forward along the closed immersion Stacks.Chow.normalConeToZeroSectionPullback, whose component to C_ZX is the comparison C_ZY ⟶ C_ZX of normal cones (Stacks.Chow.normalConeToZeroSectionPullback_snd).

theorem gysinBivariantClass_cap_normalCone {n : ℤ} (hZY : iZY ≫ iY = iZ)
    (hX : schemeDeltaDimension C sX ≤ (n : EInt)) :
    haveI := LocallyOfFiniteType.isLocallyNoetherian sX
    (gysinBivariantClass C (normalConeToX iY ≫ sX)
        (Stacks.Divisors.divisorSheaf (normalConeZeroSectionIdeal iY))
        (Stacks.Divisors.divisorSheafGlobalSection (normalConeZeroSectionIdeal iY))).1.cap
        (normalConeChangeOfCentreMap iZ iY (hZY ▸ Scheme.Hom.le_ker_comp iZY iY)) n
        (fundamentalChowClass C (normalConeChangeOfCentreMap iZ iY
          (hZY ▸ Scheme.Hom.le_ker_comp iZY iY) ≫ normalConeToX iY ≫ sX) n) =
      properChowPushforward C (normalConeToX iZY ≫ iY ≫ sX) _
        (normalConeToZeroSectionPullback iY iZ (hZY ▸ Scheme.Hom.le_ker_comp iZY iY) iZY
          (ker_eq_comap_ker_of_comp_eq iY iZ iZY hZY))
        (normalConeToZeroSectionPullback_toBase C sX iY iZ _ iZY _) (n - 1)
        (properPushforwardDescends C _ _ _ _ _)
        (fundamentalChowClass C (normalConeToX iZY ≫ iY ≫ sX) (n - 1))

Tag 0FEC, a lemma

Tag 0FEC in the Stacks Project.

Stacks.Chow.ConormalCompatibleVirtualNormalBundles, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedChernComposition.lean, line 101. The attribute's comment: “the hypothesis of the lemma: the three virtual normal bundles of Stacks 0FBQ for Z ⊆ Y ⊆ X, the short exact sequence of their duals, and its two commutative squares against the genuine conormal sequence of Stacks 062S; stated for immersions rather than closed subschemes, which is a generalization”.

For immersions i : Z ⟶ Y and j : Y ⟶ X, three virtual normal bundles — 𝒩 for Z ⊆ X, 𝒩' for Z ⊆ Y and 𝒩'' for Y ⊆ X — together with a short exact sequence

(𝒩'')^∨|_Z ⟶ 𝒩^∨ ⟶ (𝒩')^∨

of duals and the two commutative squares identifying it, through the structural surjections of the three virtual normal bundles, with the conormal sequence

𝒞_{Y/X}|_Z ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y}

of Stacks 062S.

structure ConormalCompatibleVirtualNormalBundles {Z Y X : Scheme.{u}} (i : Z ⟶ Y) (j : Y ⟶ X)
    [IsImmersion i] [IsImmersion j]

Stacks.Chow.localizedChernClass_cap_eq_bivariantCompositeCap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedChernComposition.lean, line 158. The attribute's comment: “the conclusion, reduced to the composition of bivariant classes and read on cap products; the localized Chern class c(Z ⟶ X, 𝒩) of Stacks 0FBK is not constructed in this repository and is carried as a parameter, as everywhere else here, so that the composition formula is a hypothesis”.

Granted that the class attached to 𝒩 composes the class attached to 𝒩' with the class attached to 𝒩'', its cap operation on a test scheme t : T ⟶ X is: cap with c(Y ⟶ X, 𝒩''), then cap with c(Z ⟶ Y, 𝒩'), then push forward along the associativity isomorphism (T ×_X Y) ×_Y Z ≅ T ×_X Z of pullbacks, the degrees k - (p + q) and (k - q) - p being identified.

theorem localizedChernClass_cap_eq_bivariantCompositeCap
    (hc : IsBivariantClassComposition C G sZ sY sX i j hi hj hpp p q
      (cloc sZ sY i hi D.bundleZY p) (cloc sY sX j hj D.bundleYX q)
      (cloc sZ sX (i ≫ j) (comp_comp_structureMorphism_eq hi hj) D.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 hi hj) D.bundleZX (p + q)).cap
          t k α) =
      bivariantCompositeCap C G sZ sY sX i j hi hj hpp p q (cloc sZ sY i hi D.bundleZY p)
        (cloc sY sX j hj D.bundleYX q) t k α

Stacks.Chow.eq_localizedChernClass_of_isBivariantClassComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedChernComposition.lean, line 178. The attribute's comment: “uniqueness: the composition formula determines c(Z ⟶ X, 𝒩), so the content of the lemma reduces to exhibiting the composite; the localized Chern class of Stacks 0FBK is carried as a parameter”.

Any bivariant class of degree p + q for Z ⟶ X that composes c(Z ⟶ Y, 𝒩') with c(Y ⟶ X, 𝒩'') is c(Z ⟶ X, 𝒩), provided the latter composes them.

theorem eq_localizedChernClass_of_isBivariantClassComposition
    (hc : IsBivariantClassComposition C G sZ sY sX i j hi hj hpp p q
      (cloc sZ sY i hi D.bundleZY p) (cloc sY sX j hj D.bundleYX q)
      (cloc sZ sX (i ≫ j) (comp_comp_structureMorphism_eq hi hj) D.bundleZX (p + q)))
    (c : BivariantClass C G sZ sX (i ≫ j) (comp_comp_structureMorphism_eq hi hj) (p + q))
    (hc' : IsBivariantClassComposition C G sZ sY sX i j hi hj hpp p q
      (cloc sZ sY i hi D.bundleZY p) (cloc sY sX j hj D.bundleYX q) c) :
    cloc sZ sX (i ≫ j) (comp_comp_structureMorphism_eq hi hj) D.bundleZX (p + q) = c

Stacks.Chow.completedVirtualNormalGysinClass_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/LocalizedChernCompositionClass.lean, line 103.

Stacks 0FEC. Let (S, δ) be as in Situation 02QL, let i : Z ⟶ Y and j : Y ⟶ X be closed immersions of schemes locally of finite type over S, and let 𝒩, 𝒩', 𝒩'' be virtual normal sheaves for Z ⊆ X, Z ⊆ Y and Y ⊆ X with a short exact sequence (𝒩'')^∨|_Z ⟶ 𝒩^∨ ⟶ (𝒩')^∨ whose two squares against the conormal sequence 𝒞_{Y/X}|_Z ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} commute (Stacks.Chow.ConormalCompatibleVirtualNormalBundles). Then

c(Z ⟶ X, 𝒩) = c(Z ⟶ Y, 𝒩') ∘ c(Y ⟶ X, 𝒩'') in A^*(Z ⟶ X)^∧,

for the classes of Stacks 0FBK (Stacks.Chow.completedVirtualNormalGysinClass) and the composition of Stacks 0FE0.

theorem completedVirtualNormalGysinClass_comp :
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    completedVirtualNormalGysinClass C sZ sX (i ≫ j) (comp_comp_structureMorphism_eq hi hj)
        D.bundleZX =
      completedBivariantCompositeOfInvertible C sZ sY sX i j hi hj
        (completedVirtualNormalGysinClass C sZ sY i hi D.bundleZY)
        (completedVirtualNormalGysinClass C sY sX j hj D.bundleYX)

Tag 0FBQ, a remark

Tag 0FBQ in the Stacks Project.

Stacks.Chow.completedCommutesWithEveryClass_completedVirtualNormalGysinClassOfOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedVirtualNormalCommuting.lean, line 72. The attribute's comment: “(3), counterparts: the counterpart of Lemma 0FBP, c(Z → X, 𝒩) ∈ A^(Z → X)^∧ commutes with every c ∈ A^(Y → X), for an immersion Z → X and 𝒩 of arbitrary rank”.

The counterpart of Stacks 0FBP for immersions (Stacks 0FBQ). For an immersion i : Z ⟶ X with a virtual normal bundle 𝒩 of arbitrary rank, the class c(Z ⟶ X, 𝒩) = c(Z ⟶ U, 𝒩) ∘ (U ⟶ X)^* ∈ A^*(Z ⟶ X)^∧ commutes with every bivariant class over X, degree by degree.

theorem completedCommutesWithEveryClass_completedVirtualNormalGysinClassOfOpen (i : Z ⟶ X)
    [IsImmersion i] (hi : i ≫ sX = sZ) (U : X.Opens) (i' : Z ⟶ U.toScheme) [IsClosedImmersion i']
    (hU : i' ≫ U.ι = i) (𝒩 : VirtualNormalBundle i) :
    completedCommutesWithEveryClass C sZ sX i hi
      (completedVirtualNormalGysinClassOfOpen C sZ sX i hi U i' hU 𝒩)

Stacks.Chow.completedBivariantTransport_completedBivariantRestriction_completedVirtualNormalGysinClassOfOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedVirtualNormalImmersionBaseChange.lean, line 199. The attribute's comment: “(3), counterparts: the counterpart of the base-change clause of Lemma 0FBK, the restriction of c(Z → X, 𝒩) ∈ A^(Z → X)^∧ along X' → X is c(Z' → X', g^𝒩), for a cartesian square of immersions and 𝒩 of arbitrary rank”.

The counterpart for immersions of the base-change clause of Stacks 0FBK, at arbitrary rank. For a cartesian square Z' = Z ×_X X' of immersions with f : X' ⟶ X locally of finite type, the restriction (Stacks 0F9Z) of c(Z ⟶ X, 𝒩) ∈ A^*(Z ⟶ X)^∧ along f, carried to Z' along Z ×_X X' ≅ Z', is c(Z' ⟶ X', g^*𝒩) ∈ A^*(Z' ⟶ X')^∧, with g^*𝒩 the virtual normal bundle of Stacks 0FBJ; the opens through which the two immersions factor as closed immersions are arbitrary. Both sides are read degree by degree (Stacks 0FE0), and in each degree the cap operations agree by Stacks.Chow.completedVirtualNormalGysinClassOfOpen_cap_baseChange.

theorem completedBivariantTransport_completedBivariantRestriction_completedVirtualNormalGysinClassOfOpen
    (V : X'.Opens) (iV : Z' ⟶ V.toScheme) [IsClosedImmersion iV] (hV : iV ≫ V.ι = i₂) :
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI : IsLocallyNoetherian Z' := LocallyOfFiniteType.isLocallyNoetherian sZ'
    haveI : IsLocallyNoetherian X' := LocallyOfFiniteType.isLocallyNoetherian (f ≫ sX)
    haveI : IsLocallyNoetherian (pullback i f) :=
      LocallyOfFiniteType.isLocallyNoetherian (pullback.fst i f ≫ sZ)
    completedBivariantTransport C (pullback.fst i f ≫ sZ) sZ' (f ≫ sX) (pullback.snd i f)
        (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) i₂ hi₂ sq.flip.isoPullback.symm
        sq.flip.isoPullback_inv_snd
        (completedBivariantRestrictionViaSequence C sZ sX i hi f
          (completedVirtualNormalGysinClassOfOpen C sZ sX i hi U i' hU 𝒩)) =
      completedVirtualNormalGysinClassOfOpen C sZ' (f ≫ sX) i₂ hi₂ V iV hV
        (𝒩.baseChange i i₂ g' f sq)

Stacks.Chow.completedVirtualNormalGysinRestrictionOfOpen_eq_of_isTopChernComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedVirtualNormalImmersionBaseChange.lean, line 332. The attribute's comment: “(3), counterparts: the counterpart of Lemma 0FV7, res(c(Z → X, N)) = c_top(E) ∘ c(Z' → X', N') in A^(Z' → X')^∧ for the chosen base change Z' = Z ×_X X' of an immersion, virtual normal bundles N, N' of arbitrary rank and a short exact sequence 0 → N' → g^N → E → 0 of finite locally free modules whose dual square against the conormal sheaves commutes”.

The counterpart of Stacks 0FV7 for immersions, at arbitrary rank. Let Z' = Z ×_X X' be the chosen base change of an immersion i : Z ⟶ X along f : X' ⟶ X, let 𝒩 be a virtual normal bundle for Z ⟶ X and 𝒩' one for Z' ⟶ X', of arbitrary ranks, and let 0 ⟶ 𝒩' ⟶ g^*𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free 𝒪_{Z'}-modules such that the square of hcomm commutes. Then

res(c(Z ⟶ X, 𝒩)) = c_top(ℰ) ∘ c(Z' ⟶ X', 𝒩')

in A^*(Z' ⟶ X')^∧, for the classes of Stacks 0FBQ (3) built from arbitrary opens through which the two immersions factor as closed immersions. By the counterpart of the base-change clause of Stacks 0FBK and the counterpart of Stacks 0FBL.

theorem completedVirtualNormalGysinRestrictionOfOpen_eq_of_isTopChernComposition (V : X'.Opens)
    (iV : pullback i f ⟶ V.toScheme) [IsClosedImmersion iV] (hV : iV ≫ V.ι = pullback.snd i f)
    (w : inc ≫ pr = 0) (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (hcomm : pullbackDualMap (pullback.fst i f) N.bundle ≫
        dualMap inc ≫ 𝒩'.surjection =
      (modulePullback (pullback.fst i f).toLRSHom.toShHom).map N.surjection ≫
        Stacks.Immersion.immersionConormalSheafMap (pullback.snd i f) i (pullback.fst i f) f
          (Stacks.Immersion.toShHom_square (isPullback_pullbackSnd i f).w)) :
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI : IsLocallyNoetherian X' := LocallyOfFiniteType.isLocallyNoetherian (f ≫ sX)
    haveI : IsLocallyNoetherian (pullback i f) :=
      LocallyOfFiniteType.isLocallyNoetherian (pullback.fst i f ≫ sZ)
    completedBivariantRestrictionViaSequence C sZ sX i hi f
        (completedVirtualNormalGysinClassOfOpen C sZ sX i hi U i' hU N) =
      completedBivariantGroup.copy C (Category.id_comp (pullback.snd i f)) _
        (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f)
        (completedBivariantCompositeOfInvertible C (pullback.fst i f ≫ sZ)
          (pullback.fst i f ≫ sZ) (f ≫ sX) (𝟙 _) (pullback.snd i f) (Category.id_comp _)
          (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f)
          (topChernClassOfInvertible C (pullback.fst i f ≫ sZ) Eb)
          (completedVirtualNormalGysinClassOfOpen C (pullback.fst i f ≫ sZ) (f ≫ sX)
            (pullback.snd i f) (pullbackSnd_comp_structureMorphism_eq C sZ sX i hi f) V iV hV
            𝒩'))

Stacks.Chow.completedVirtualNormalGysinClassOfOpen_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/CompletedVirtualNormalImmersionComposition.lean, line 250. The attribute's comment: “(3), counterparts: the counterpart of Lemma 0FEC, c(Z → X, 𝒩) = c(Z → Y, 𝒩') ∘ c(Y → X, 𝒩'') in A^*(Z → X)^∧ for immersions Z → Y → X and a conormal-compatible triple of virtual normal bundles of arbitrary rank”.

The counterpart of Stacks 0FEC for immersions, at arbitrary rank. Let Z ⟶ Y ⟶ X be immersions of schemes locally of finite type over the base, and let D be a conormal-compatible triple of virtual normal bundles 𝒩, 𝒩', 𝒩'' for Z ⊆ X, Z ⊆ Y and Y ⊆ X, of arbitrary (locally constant) ranks. Then

c(Z ⟶ X, 𝒩) = c(Z ⟶ Y, 𝒩') ∘ c(Y ⟶ X, 𝒩'') in A^*(Z ⟶ X)^∧,

for the classes of Stacks 0FBQ (3) built from arbitrary opens W, V, U in which the three immersions are closed.

theorem completedVirtualNormalGysinClassOfOpen_comp
    (W : X.Opens) (iW : Z ⟶ W.toScheme) [IsClosedImmersion iW] (hW : iW ≫ W.ι = i ≫ j)
    (V : Y.Opens) (iV : Z ⟶ V.toScheme) [IsClosedImmersion iV] (hV : iV ≫ V.ι = i)
    (U : X.Opens) (jU : Y ⟶ U.toScheme) [IsClosedImmersion jU] (hU : jU ≫ U.ι = j) :
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    completedVirtualNormalGysinClassOfOpen C sZ sX (i ≫ j) (comp_comp_structureMorphism_eq hi hj)
        W iW hW D.bundleZX =
      completedBivariantCompositeOfInvertible C sZ sY sX i j hi hj
        (completedVirtualNormalGysinClassOfOpen C sZ sY i hi V iV hV D.bundleZY)
        (completedVirtualNormalGysinClassOfOpen C sY sX j hj U jU hU D.bundleYX)

Stacks.Chow.VirtualNormalBundle, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundle.lean, line 39. The attribute's comment: “(2): a virtual normal bundle for an immersion”.

A virtual normal bundle for an immersion i : Z ⟶ X: a finite locally free 𝒪_Z-module together with a surjection from its dual onto the conormal sheaf 𝒞_{Z/X} of i.

structure VirtualNormalBundle {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]

Stacks.Chow.completedVirtualNormalGysinClassOfOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleImmersionClass.lean, line 149. The attribute's comment: “(3), the construction: c(Z → X, 𝒩) = c(Z → U, 𝒩) ∘ (U → X)^ in A^(Z → X)^∧ for a choice of an open U through which Z → X factors as a closed immersion, 𝒩 of arbitrary rank”.

Stacks 0FBQ (3), the construction, for a virtual normal bundle of arbitrary rank. For an immersion i : Z ⟶ X, an open subscheme U ⊆ X with i = i' ≫ ι_U and i' : Z ⟶ U a closed immersion, and a virtual normal bundle 𝒩 for i: the class

c(Z ⟶ U, 𝒩) ∘ (U ⟶ X)^* ∈ A^*(Z ⟶ X)^∧,

the composite on completions (Stacks 0FE0) of flat pullback along U ⟶ X (Stacks 0B78) with the class of Stacks 0FBK of 𝒩 in A^*(Z ⟶ U)^∧, read as a virtual normal bundle for i'.

def completedVirtualNormalGysinClassOfOpen (U : X.Opens) (i' : Z ⟶ U.toScheme)
    [IsClosedImmersion i'] (hU : i' ≫ U.ι = i) (𝒩 : VirtualNormalBundle i) :
    completedBivariantGroup C (gysinSystemOfInvertible C) sZ sX i hi

Stacks.Chow.completedVirtualNormalGysinClassOfOpen_independent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleImmersionClass.lean, line 483. The attribute's comment: “(3), the bivariant class c(Z → X, 𝒩) ∈ A^*(Z → X)^∧ does not depend on the choice of U, for 𝒩 of arbitrary rank”.

Stacks 0FBQ (3): the bivariant class c(Z ⟶ X, 𝒩) ∈ A^*(Z ⟶ X)^∧ does not depend on the choice of the open subscheme U, for a virtual normal bundle 𝒩 of arbitrary rank: two opens U₁, U₂ ⊆ X through which the immersion i factors as a closed immersion give the same class c(Z ⟶ U₁, 𝒩) ∘ (U₁ ⟶ X)^* = c(Z ⟶ U₂, 𝒩) ∘ (U₂ ⟶ X)^*.

theorem completedVirtualNormalGysinClassOfOpen_independent (U₁ U₂ : X.Opens)
    (i₁ : Z ⟶ U₁.toScheme) [IsClosedImmersion i₁] (h₁ : i₁ ≫ U₁.ι = i) (i₂ : Z ⟶ U₂.toScheme)
    [IsClosedImmersion i₂] (h₂ : i₂ ≫ U₂.ι = i) :
    completedVirtualNormalGysinClassOfOpen C sZ sX i hi U₁ i₁ h₁ 𝒩 =
      completedVirtualNormalGysinClassOfOpen C sZ sX i hi U₂ i₂ h₂ 𝒩

Stacks.Chow.completedVirtualNormalGysinClassOfOpen_cap_fundamentalChowClass_excess, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleImmersionCounterparts.lean, line 903. The attribute's comment: “(3), counterparts: the counterpart of Lemma 0FBM when the virtual normal bundle has unbounded rank, c(Z → X, N) ∩ [Y]_n = c_top(E) ∩ [Z ×_X Y]_{n-r} degree by degree in CH_, for an immersion Z → X, c(Z → X, N) ∈ A^(Z → X)^∧, Z ×_X Y → Y regular with conormal sheaf of constant rank r, E the excess normal sheaf and dim_δ(Y) ≤ n”.

The counterpart of Stacks 0FBM for immersions, at unbounded rank. Let i : Z ⟶ X be an immersion with a virtual normal bundle 𝒩 of arbitrary rank, and let g : Y ⟶ X be locally of finite type such that the base change i₂ : Z' = Z ×_X Y ⟶ Y is a regular immersion whose conormal sheaf has constant rank r; let ℰ be the excess normal sheaf. If dim_δ(Y) ≤ n then

c(Z ⟶ X, 𝒩) ∩ [Y]_n = c_top(ℰ) ∩ [Z']_{n - r}

degree by degree in CH_*(Z ×_X Y), for c(Z ⟶ X, 𝒩) = c(Z ⟶ U, 𝒩) ∘ (U ⟶ X)^* in A^*(Z ⟶ X)^∧: the degree-(r + e) part of the left side is the degree-e part of c_top(ℰ) capped with [Z']_{n - r} (Stacks.Chow.topChernCap), and the parts of degree p < r vanish. This is how the source reads the equality when the rank is unbounded on the connected components.

On V = g⁻¹(U) the immersion i₂ factors through the regular closed immersion Z' ⟶ V, the base change of Z ⟶ U, with the same conormal and excess normal sheaves, and [Y]_n restricts to [V]_n; so this is Stacks 0FBM at arbitrary rank (Stacks.Chow.completedVirtualNormalGysinCap_fundamentalChowClass_excess) for Z ⟶ U.

theorem completedVirtualNormalGysinClassOfOpen_cap_fundamentalChowClass_excess {Y Z' : Scheme.{u}}
    (g : Y ⟶ X) [LocallyOfFiniteType g] (i₂ : Z' ⟶ Y) [IsImmersion i₂] (g' : Z' ⟶ Z)
    (sq : IsPullback i₂ g' g i) (sZ' : Z' ⟶ C.S) [LocallyOfFiniteType sZ']
    (hi₂ : i₂ ≫ (g ≫ sX) = sZ') (hreg : IsRegularImmersion i₂) (r : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (conormalModule i₂) r]
    (n : ℤ) (hY : schemeDeltaDimension C (g ≫ sX) ≤ (n : EInt)) :
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    haveI : SheafOfModules.IsFiniteLocallyFree.{u, u, u}
        (𝒩.baseChange i i₂ g' g sq).excessNormalSheaf :=
      (𝒩.baseChange i i₂ g' g sq).isFiniteLocallyFree_excessNormalSheaf
        (SheafOfModules.IsFiniteLocallyFreeOfRank.isFiniteLocallyFree _ r)
    (∀ e : ℕ, (completedBivariantSequenceOfInvertible C sZ sX i hi
        (completedVirtualNormalGysinClassOfOpen C sZ sX i hi U i' hU 𝒩) ((r + e : ℕ) : ℤ)).cap g n
          (fundamentalChowClass C (g ≫ sX) n) =
        chowPushforwardOfIso C sZ' (pullback.fst i g ≫ sZ) sq.flip.isoPullback.hom
          (isoPullback_hom_comp_structureMorphism C sZ sX sq hi sZ' hi₂) (n - ((r + e : ℕ) : ℤ))
          (chowGroupDegreeEquiv C sZ' (by push_cast; ring)
            (topChernCap C sZ' (𝒩.baseChange i i₂ g' g sq).excessNormalSheaf (n - (r : ℤ)) e
              (fundamentalChowClass C sZ' (n - (r : ℤ)))))) ∧
      ∀ p : ℤ, p < r → (completedBivariantSequenceOfInvertible C sZ sX i hi
        (completedVirtualNormalGysinClassOfOpen C sZ sX i hi U i' hU 𝒩) p).cap g n
          (fundamentalChowClass C (g ≫ sX) n) = 0

Stacks.Chow.virtualNormalGysinClassOfOpen_cap_fundamentalChowClass_of_isCohenMacaulayLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleImmersionCounterparts.lean, line 1020. The attribute's comment: “(3), counterparts: the counterpart of Lemma 0FEA, c(Z → X, N) ∩ [Y]_n = [Z ×_X Y]_{n-r} for an immersion Z → X, N locally free of rank r, Y pure of δ-dimension n, dim_δ(Z ×_X Y) ≤ n - r and O_{Y,ξ} Cohen-Macaulay at the points of Z ×_X Y of δ = n - r”.

The counterpart of Stacks 0FEA for immersions. Let i : Z ⟶ X be an immersion with a virtual normal bundle 𝒩, let g : Y ⟶ X be locally of finite type, and given integers r and n assume

1. 𝒩 is locally free of rank r,
2. every irreducible component of Y has δ-dimension n,
3. dim_δ(Z ×_X Y) ≤ n - r, and
4. 𝒪_{Y, ξ} is Cohen–Macaulay for every ξ ∈ Z ×_X Y with δ(ξ) = n - r.

Then c(Z ⟶ X, 𝒩) ∩ [Y]_n = [Z ×_X Y]_{n - r}, for c(Z ⟶ X, 𝒩) = c(Z ⟶ U, 𝒩) ∘ (U ⟶ X)^*.

On V = g⁻¹(U) the four hypotheses hold for the closed immersion Z ⟶ U and V ⟶ U: the irreducible components of the open V are pure of δ-dimension n, Z ×_U V = Z ×_X Y, and the local rings of V are those of Y. So this is Stacks 0FEA (Stacks.Chow.virtualNormalGysinClass_cap_fundamentalChowClass_of_isCohenMacaulayLocalRing) for Z ⟶ U, and [Y]_n restricts to [V]_n.

theorem virtualNormalGysinClassOfOpen_cap_fundamentalChowClass_of_isCohenMacaulayLocalRing
    {n : ℤ} {Y : Scheme.{u}} (g : Y ⟶ X) [LocallyOfFiniteType g]
    (hY : ∀ W : irreducibleComponents Y,
      deltaDimension C (g ≫ sX)
        ⟨W, W.2.1, isClosed_of_mem_irreducibleComponents (W : Set Y) W.2⟩ = n)
    (hZY : schemeDeltaDimension C (pullback.snd i g ≫ (g ≫ sX)) ≤ ((n - r : ℤ) : EInt))
    (hCM : ∀ ξ : (pullback i g : Scheme.{u}),
      relativeDimension C.dimensionFunction (g ≫ sX) ((pullback.snd i g).base ξ) = n - r →
      letI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian (g ≫ sX)
      IsCohenMacaulayLocalRing (Y.presheaf.stalk ((pullback.snd i g).base ξ))) :
    (virtualNormalGysinClassOfOpen C sZ sX i hi U i' hU 𝒩 r).cap g n
        (fundamentalChowClass C (g ≫ sX) n) =
      fundamentalChowClass C (pullback.fst i g ≫ sZ) (n - r)

Stacks.Chow.completedVirtualNormalGysinClassOfOpen_eq_of_isTopChernComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleImmersionCounterparts.lean, line 1108. The attribute's comment: “(3), counterparts: the counterpart of Lemma 0FBL in A^*(Z → X)^∧, c(Z → X, N) = c_top(E) ∘ c(Z → X, N') for an immersion Z → X and a short exact sequence 0 → N' → N → E → 0 of finite locally free modules of arbitrary rank whose surjection factors through that of N'”.

The counterpart of Stacks 0FBL for immersions, at arbitrary rank. Let i : Z ⟶ X be an immersion with a virtual normal bundle 𝒩, and let 0 ⟶ 𝒩' ⟶ 𝒩 ⟶ ℰ ⟶ 0 be a short exact sequence of finite locally free 𝒪_Z-modules, of arbitrary ranks, such that the surjection σ : 𝒩^∨ ⟶ 𝒞_{Z/X} factors as σ' ∘ (𝒩^∨ ⟶ (𝒩')^∨) through that of 𝒩'. Then

c(Z ⟶ X, 𝒩) = c_top(ℰ) ∘ c(Z ⟶ X, 𝒩')

in A^*(Z ⟶ X)^∧, both classes built from the same open U. By Stacks 0FBL at arbitrary rank (Stacks.Chow.completedVirtualNormalGysinClass_eq_of_isTopChernComposition) for Z ⟶ U and the associativity of the composition on completions (Stacks 0FE0).

theorem completedVirtualNormalGysinClassOfOpen_eq_of_isTopChernComposition
    (w : inc ≫ pr = 0) (hseq : (ShortComplex.mk inc pr w).ShortExact)
    (hsigma : dualMap inc ≫ 𝒩'.surjection = 𝒩.surjection) :
    haveI : IsLocallyNoetherian Z := LocallyOfFiniteType.isLocallyNoetherian sZ
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian sX
    completedVirtualNormalGysinClassOfOpen C sZ sX i hi U i' hU 𝒩 =
      completedBivariantGroup.copy C (Category.id_comp i) _ hi
        (completedBivariantCompositeOfInvertible C sZ sZ sX (𝟙 Z) i (Category.id_comp sZ) hi
          (topChernClassOfInvertible C sZ Eb)
          (completedVirtualNormalGysinClassOfOpen C sZ sX i hi U i' hU 𝒩'))

Declarations registered for the tag:

• VirtualNormalBundle.baseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleImmersionCounterparts.lean, line 90 (StacksFrontier): “(3), counterparts: the counterpart of Lemma 0FBJ, g^*𝒩 is a virtual normal bundle for Z' → X' for a cartesian square whose horizontal arrows are immersions”.
• Stacks.Thickenings.immersionConormalSheaf, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Chow/BivariantLemmas/VirtualNormalBundleOpenFactor.lean, line 44 (StacksFrontier): “(1): the conormal sheaf of an immersion, Stacks 01R2”.

Sources

• Section 42.54, Tag 0FBI
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.VirtualNormalBundle.baseChange · Stacks.Chow.completedVirtualNormalGysinClass · Stacks.Chow.completedBivariantRestriction_completedVirtualNormalGysinClass · Stacks.Chow.IsVirtualNormalGysinClass · Stacks.Chow.eq_of_isVirtualNormalGysinClass · Stacks.Chow.virtualNormalGysinCap · Stacks.Chow.pi_virtualNormalGysinCap · Stacks.Chow.isVirtualNormalGysinClass_iff_cap_eq

Section42.55 Calculating some classes#

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

Tag 0FEE, a lemma

Tag 0FEE in the Stacks Project.

Stacks.Chow.homComponent_exteriorPowerChernAltProd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/ExteriorPowerChernAlternatingProduct.lean, line 184. The attribute's comment: “the whole lemma, for the library's Chern classes: c(wedge^n E) is the total Chern class totalChern of Stacks 0B7H, the product is the ordered product of units in the ring TotalChowClass = prod_{p >= 0} A^p(Y) of total Chow cohomology classes, and '= 1 - (r-1)! c_r(E) + ...' is the equality of homogeneous components in every degree <= r. The splitting principle is proved, not assumed: Stacks 02UL via exists_splittingMorphism_basechange_unconditional, the Chern roots of the exterior powers via 02UI and 02UJ (totalChern_exteriorPower_of_hasQuotients)”.

Stacks 0FEE. For a finite locally free module ℰ of rank r ≥ 1 on Y, the alternating product ∏_{n = 0}^{r} c(⋀ⁿ ℰ)^{(-1)ⁿ} of the total Chern classes of its exterior powers, in the ring ∏_{p ≥ 0} A^p(Y) of total Chow cohomology classes, agrees with 1 - (r - 1)! c_r(ℰ) in every degree ≤ r. The + … of the source is the part in degrees > r, on which nothing is asserted.

theorem homComponent_exteriorPowerChernAltProd (hr : r ≠ 0) {t : ℕ} (ht : t ≤ r) :
    TotalChowClass.homComponent t (exteriorPowerChernAltProd C sY V r : TotalChowClass C sY) =
      TotalChowClass.homComponent t
        (1 - (r - 1).factorial • TotalChowClass.homComponent r (totalChern C sY V r))

Stacks.Chow.homPart_altExteriorTotalChern, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/ExteriorPowerChernClasses.lean, line 722. The attribute's comment: “the lemma as stated, for every X locally of finite type over S and every finite locally free E of rank r >= 1, with no further hypothesis. The alternating product is altExteriorTotalChern C sX E r, the ordered product of the units totalChernUnit of the exterior powers in the ring TotalChowClass C sX of total Chow cohomology classes; c_i(E) is TotalChowClass.homComponent i (totalChern C sX E r). The + ... of the source is read as asserting nothing above degree r, as its proof does”.

Stacks 0FEE. Let ℰ be a finite locally free 𝒪_X-module of rank r ≥ 1. Then

∏_{n = 0}^{r} c(⋀ⁿ ℰ)^{(-1)ⁿ} = 1 - (r-1)! c_r(ℰ) + ⋯,

that is, the alternating product of the total Chern classes of the exterior powers of ℰ has vanishing parts in the degrees 1, …, r - 1 and the part -(r-1)! c_r(ℰ) in degree r; the part in degree 0 is 1, and the ⋯ of the source asserts nothing about the higher degrees. Here c_i(ℰ) = TotalChowClass.homComponent i (totalChern C sX ℰ r) is the bivariant Chern class of Stacks 0B7H in the ring ∏_p A^p(X) of total Chow cohomology classes.

By the splitting principle (Stacks 02UL, Stacks.Chow.TotalChowClass.eq_of_res_eq_of_hasInvertibleFiltration) it suffices to prove the identities after restriction along every h : T ⟶ X along which h^*ℰ has a filtration with invertible quotients. There c(⋀ⁿ h^*ℰ) = ∏_{#I = n} (1 + ∑_{i ∈ I} x_i) for the Chern roots x_i (Stacks.Chow.exists_chernRoots_exteriorPower), and the alternating product of these is computed by Stacks.Chow.homPart_alternatingProd_of_roots.

theorem homPart_altExteriorTotalChern (E : X.Modules) {r : ℕ}
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r] (hr : r ≠ 0) :
    (∀ n, 0 < n → n < r →
      TotalChowClass.homComponent n (altExteriorTotalChern C sX E r : TotalChowClass C sX) = 0) ∧
      TotalChowClass.homComponent r (altExteriorTotalChern C sX E r : TotalChowClass C sX) =
        -(Nat.factorial (r - 1) • TotalChowClass.homComponent r (totalChern C sX E r))

Stacks.Chow.altExteriorChernProduct_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SplittingPrinciple/ExteriorPowerChernProduct.lean, line 303. The attribute's comment: “the whole lemma, in the carried ring A^*(X)^∧ of Stacks 0FE0 where the inverses c(E)^{-1} exist. CARRIED: the Chern roots, i.e. the display c(wedge^n E) = prod_{i_1 < ... < i_n} (1 + x_{i_1} + ... + x_{i_n}) of the source proof, i.e. the splitting principle: Stacks 02UK, 02UL and the product form of 02UJ; see the module doc. The computation is proved”.

Stacks 0FEE. For ℰ locally free of rank r ≥ 1 with Chern roots t, the alternating product ∏_{n = 0}^{r} c(⋀ⁿ ℰ)^{(-1)ⁿ} has vanishing components in the degrees 1, …, r-1 and the component -(r-1)! c_r(ℰ) in degree r; nothing is asserted in higher degrees, which is the + … of the source.

theorem altExteriorChernProduct_apply (D : TotalChernClassSeries C G sX R) (E : X.Modules)
    {r : ℕ} [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r]
    (hr : r ≠ 0) (t : Fin r → chowCohomologyComponent C G sX 1)
    (hE : D.ch E = (∏ i, oneAddDegreeOne R (t i) : UnitalSeries R).1)
    (hwedge : ∀ n ≤ r, D.ch (Scheme.Modules.exteriorPower E (n : ℤ))
      = (rootTotalChern R t ((Finset.univ : Finset (Fin r)).powersetCard n)).1) :
    (∀ n, 0 < n → n < r → (altExteriorChernProduct D E r).1 n = 0) ∧
      (altExteriorChernProduct D E r).1 r
        = -(Nat.factorial (r - 1) • D.ch E r)

Tag 0FEF, a lemma

Tag 0FEF in the Stacks Project.

Stacks.Chow.ProjectiveCompletion.bivariantClass_zeroSecObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProjectiveCompletionChern/ZeroSectionBivariant.lean, line 534. The attribute's comment: “clause (2), as an equality of bivariant classes after composing with any c ∈ A^*(E → X₀)”.

Stacks 0FEF (2), as an equality of bivariant classes. Let π : E ⟶ X be the projective completion of a locally free module 𝒞 of rank r, i : X ⟶ E its zero section, j : C ⟶ E and p : C ⟶ X the inclusion and the structure morphism of the vector bundle C = Spec_X(Sym^*(𝒞)). For every s : X ⟶ X₀ and every bivariant class c ∈ A^q(E ⟶ X₀),

p^* ∘ π_* ∘ (c_r(i_*𝒪_X) ∘ c) = (-1)^{r-1} (r-1)! (j^* ∘ c) in A^q(C ⟶ X₀).

Here c_r(i_*𝒪_X) ∈ A^r(E) is the Chern class of Stacks 0F9E, ∘ the composition of Stacks 0B75, π_* the pushforward of Stacks 0EPK and p^* ∈ A^{-r}(C ⟶ X), j^* ∈ A^0(C ⟶ E) the flat pullback classes of Stacks 0B78; the two sides are classes for the equal morphisms p ≫ s = j ≫ π ≫ s and of the equal degrees -r + (r + q) = -0 + q, compared through the transport Stacks.Chow.BivariantClass.copy. This is the form in which the source composes the identity p^* ∘ π_* ∘ c_r(i_*𝒪_X) = (-1)^{r-1} (r-1)! j^* with a class on its right (Stacks 0FEG); by the extensionality of Stacks 0B76 it is checked on the caps, which are classes on the base changes E ×_{X₀} T = E ×_X (X ×_{X₀} T), where it is the cartesian-square form flatPullbackChow_properChowPushforward_perfectChernClass_of_isPullback of the second conclusion.

theorem bivariantClass_zeroSecObject {X₀ : Scheme.{u}} (sX₀ : X₀ ⟶ C.S) [LocallyOfFiniteType sX₀]
    (s : X ⟶ X₀) [LocallyOfFiniteType s] (hs : s ≫ sX₀ = sX) :
    haveI := locallyOfFiniteType_proj 𝒞 r
    haveI := flat_proj 𝒞 r
    haveI := locallyOfFiniteType_vectorBundleToBase 𝒞 r
    haveI := flat_vectorBundleToBase 𝒞 r
    ∀ {q : ℤ} (c : BivariantClass C (gysinSystemOfInvertible C) (proj 𝒞 ≫ sX) sX₀
      (proj 𝒞 ≫ s) (comp_comp_structureMorphism_eq rfl hs) q),
      bivariantCompositeOfInvertible C _ sX sX₀ _ s rfl hs (-(r : ℤ)) ((r : ℤ) + q)
          (flatPullbackBivariantClassOfInvertible C
            (Scheme.Modules.vectorBundleToBase X 𝒞 ≫ sX) sX _ rfl r
            (relativeDimension_vectorBundleToBase 𝒞 r))
          (canonicalBivariantProperPushforward C (proj 𝒞 ≫ sX) sX sX₀ (proj 𝒞) s rfl hs
            ((r : ℤ) + q)
            (BivariantClass.copy C (gysinSystemOfInvertible C) (proj 𝒞 ≫ sX) sX₀
              (Category.id_comp (proj 𝒞 ≫ s)) _ _ rfl
              (bivariantCompositeOfInvertible C (proj 𝒞 ≫ sX) (proj 𝒞 ≫ sX) sX₀ (𝟙 _)
                (proj 𝒞 ≫ s) (Category.id_comp _) (comp_comp_structureMorphism_eq rfl hs)
                (r : ℤ) q
                (perfectChernClass C (proj 𝒞 ≫ sX) (hasDefinedChernClasses_zeroSecObject 𝒞 r)
                  r) c))) =
        BivariantClass.copy C (gysinSystemOfInvertible C) _ sX₀ (incl_proj_comp 𝒞 r s) _
          (comp_comp_structureMorphism_eq rfl hs)
          (show -((0 : ℕ) : ℤ) + q = -(r : ℤ) + ((r : ℤ) + q) by push_cast; ring)
          ((((-1 : ℤ) ^ (r - 1) * ((r - 1).factorial : ℤ)) •
            bivariantCompositeOfInvertible C _ (proj 𝒞 ≫ sX) sX₀ (vectorBundleIncl 𝒞 r)
              (proj 𝒞 ≫ s) (vectorBundleIncl_comp_structure 𝒞 r C sX)
              (comp_comp_structureMorphism_eq rfl hs) (-((0 : ℕ) : ℤ)) q
              (flatPullbackBivariantClassOfInvertible C _ _ _
                (vectorBundleIncl_comp_structure 𝒞 r C sX) 0
                (relativeDimension_of_isOpenImmersion _)) c))

Stacks.Chow.ProjectiveCompletion.chernClasses_zeroSecObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ProjectiveCompletionChern/ZeroSectionProjection.lean, line 834. The attribute's comment: “both conclusions: (1) c_t(i_O_X) = 0 for t = 1, ..., r - 1; (2) p^ o pi_ o c_r(i_O_X) = (-1)^(r-1) (r-1)! j^, as an identity of operations at every test scheme E' -> E on which the left side is defined, namely every base change E' = E x_X X' of pi along f : X' -> X locally of finite type (any cartesian square), with C' = C x_E E' any cartesian square: p'^ pi'_ (c_r(i_O_X) cap alpha) = (-1)^(r-1) (r-1)! j'^ alpha for alpha in A_k(E'). In the bivariant conventions c_r(i_O_X) lies in A^r(E -> E) and the pushforward of 0EPK needs a class over a morphism factoring through pi, so the left side is not a composite of bivariant classes in A^0(C -> E); its operation exists exactly on these test schemes, which are those on which the source's proof compares the two sides”.

Stacks 0FEF. Let 𝒞 be a locally free 𝒪_X-module of rank r on X locally of finite type over the base of chapter 42, π : E = Proj_X(Sym^*(𝒞)[T]) ⟶ X its projective completion with zero section i : X ⟶ E, and j : C = Spec_X(Sym^*(𝒞)) ⟶ E, p : C ⟶ X the inclusion and the structure morphism of the vector bundle. Then

1. c_t(i_*𝒪_X) = 0 for t = 1, …, r - 1, and
2. p^* ∘ π_* ∘ c_r(i_*𝒪_X) = (-1)^{r-1} (r-1)! j^*, as operations on every test scheme g : E' ⟶ E on which the left-hand side is defined: for every cartesian square E' = E ×_X X' over f : X' ⟶ X locally of finite type, with π' : E' ⟶ X', every cartesian square C' = C ×_E E' with j' : C' ⟶ E', and every α ∈ A_k(E'), p'^* π'_*(c_r(i_*𝒪_X) ∩ α) = (-1)^{r-1} (r-1)! j'^* α in A_k(C'), where p' = π' ∘ j'.

The Chern classes are those of Stacks 0F9E of the perfect object i_*𝒪_X of D(𝒪_E), and c_r(i_*𝒪_X) ∩ α is the operation of c_r(i_*𝒪_X) ∈ A^r(E) on the test scheme g.

On the reading of (2). In the conventions of bivariant classes, c_r(i_*𝒪_X) ∈ A^r(E ⟶ E) and the pushforward π_* ∘ - of Stacks 0EPK applies to a class of A^*(E ⟶ Z) for a morphism E ⟶ Z factoring through π, so p^* ∘ π_* ∘ c_r(i_*𝒪_X) is not a composite of bivariant classes landing in A⁰(C ⟶ E). The operation it names is defined on those test schemes E' ⟶ E that are base changes of π, where π'_* exists, and these are the test schemes on which the proof of the source compares the two sides ("after replacing X by a scheme locally of finite type over X ... both sides have the same effect on α ∈ CH_*(E)"). Statement (2) is the identity of the two operations at every such test scheme.

theorem chernClasses_zeroSecObject :
    (letI := locallyOfFiniteType_proj_comp 𝒞 r C sX
      ∀ t : ℕ, 0 < t → t < r →
        perfectChernClass C (proj 𝒞 ≫ sX) (hasDefinedChernClasses_zeroSecObject 𝒞 r) t = 0) ∧
    ∀ {X' E' C' : Scheme.{u}} (f : X' ⟶ X) [LocallyOfFiniteType f] (g : E' ⟶ space 𝒞)
      (π' : E' ⟶ X') (hsq : IsPullback g π' (proj 𝒞) f)
      (q : C' ⟶ Scheme.Modules.vectorBundle X 𝒞) (j' : C' ⟶ E')
      (hsqC : IsPullback q j' (vectorBundleIncl 𝒞 r) g) (k : ℤ),
      haveI := locallyOfFiniteType_proj 𝒞 r
      haveI := flat_proj 𝒞 r
      haveI : LocallyOfFiniteType g := MorphismProperty.of_isPullback hsq.flip inferInstance
      haveI : LocallyOfFiniteType π' := MorphismProperty.of_isPullback hsq inferInstance
      haveI : Flat π' := MorphismProperty.of_isPullback hsq inferInstance
      haveI : IsProper π' := MorphismProperty.of_isPullback hsq inferInstance
      haveI : IsOpenImmersion j' := MorphismProperty.of_isPullback hsqC inferInstance
      ∀ α : chowGroup C (g ≫ proj 𝒞 ≫ sX) k,
      flatPullbackChow C (j' ≫ g ≫ proj 𝒞 ≫ sX) (f ≫ sX) (j' ≫ π')
          (incl_snd_comp_eq 𝒞 C sX hsq j') r (relativeDimension_incl_snd 𝒞 r hsq j') (k - r)
          (flatPullbackFactorsThroughRationalEquivalence_general C _ _ _
            (incl_snd_comp_eq 𝒞 C sX hsq j') r (relativeDimension_incl_snd 𝒞 r hsq j') (k - r))
          (properChowPushforward C (g ≫ proj 𝒞 ≫ sX) (f ≫ sX) π' (snd_comp_eq 𝒞 C sX hsq) (k - r)
            (properPushforwardFactorsThroughRationalEquivalence_of_isProper C _ _ _
              (snd_comp_eq 𝒞 C sX hsq) (k - r))
            ((perfectChernClass C (proj 𝒞 ≫ sX) (hasDefinedChernClasses_zeroSecObject 𝒞 r)).op
              g k r α)) =
        chowGroupCast C _ (show k + ((0 : ℕ) : ℤ) = k - r + r by push_cast; ring)
          (((-1 : ℤ) ^ (r - 1) * ((r - 1).factorial : ℤ)) •
            flatPullbackChow C _ (g ≫ proj 𝒞 ≫ sX) j' rfl 0
              (relativeDimension_of_isOpenImmersion _) k
              (flatPullbackFactorsThroughRationalEquivalence_general C _ _ _ rfl 0
                (relativeDimension_of_isOpenImmersion _) k) α)

Stacks.Chow.chernClass_pushforward_zeroSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ZeroSectionKoszul/ChernClassZeroSection.lean, line 260. The attribute's comment: “the whole lemma, for r ≥ 1 (the source's (r-1)! presupposes it): c_t(i_O_X) = 0 for 0 < t < r, and p^ ∘ π_ ∘ c_r(i_O_X) = (-1)^{r-1}(r-1)! j^ on every test scheme X' ×_X E ⟶ E, which are the test schemes on which the composite p^ ∘ π_* ∘ c_r is defined”.

Stacks 0FEF. Let X be locally of finite type over the base S of chapter 42, 𝒞 a finite locally free 𝒪_X-module of rank r ≥ 1, π : E = 𝐏(𝒞 ⊕ 𝒪_X) ⟶ X the projective completion, i : X = 𝐏(𝒪_X) ⟶ E the zero section, C = Spec_X(Sym(𝒞)) = V ⊆ E the complement of the divisor at infinity with its inclusion j and projection p : V ⟶ X. Then

• c_t(i_*𝒪_X) = 0 for t = 1, …, r - 1, and
• p^* ∘ π_* ∘ c_r(i_*𝒪_X) = (-1)^{r-1} (r-1)! j^* in A^0(C → E): for every test scheme q : X' ×_X E ⟶ E obtained from a morphism g : X' ⟶ X locally of finite type, with π' : X' ×_X E ⟶ X', V' = q⁻¹(V) and p' : V' ⟶ X', and every α ∈ CH_*(X' ×_X E), p'^*(π'_*(c_r(i_*𝒪_X) ∩ α)) = (-1)^{r-1} (r-1)! α|_{V'}; the test scheme 𝟙_E is stated separately.

The Chern classes of i_*𝒪_X are defined because it is resolved by the Koszul complex of π^*𝒞 ⊗ 𝒪_E(-1) ⟶ 𝒪_E (Stacks.ProjectiveCompletion.koszulResolutionZeroSection). The rank is taken positive, as the factor (r-1)! of the source presupposes.

Why the test schemes X' ×_X E are the whole of the second clause. The composite p^* ∘ π_* ∘ c_r(i_*𝒪_X) is not a composite of bivariant classes for C ⟶ E: π_* is proper pushforward along π' : E' ⟶ X', which exists only for a test scheme E' over E that is the pullback X' ×_X E of a scheme X' over X, and p^* is flat pullback along the bundle p' : X' ×_X C ⟶ X'. So the composite is an operation CH_*(X' ×_X E) ⟶ CH_*(X' ×_X C) for each X' ⟶ X locally of finite type, and the equality "in A^0(C → E)" with (-1)^{r-1}(r-1)! j^* asserts exactly that these operations agree with (-1)^{r-1}(r-1)! times restriction to X' ×_X C, for every such X'. This is the reduction the source makes in its proof ("after replacing X by a scheme locally of finite type over X, it suffices to prove that both sides have the same effect on an element α ∈ CH_*(E)"), and it is the third conjunct; the second is the case X' = X read on E itself rather than on X ×_X E.

theorem chernClass_pushforward_zeroSection (C : ChowSituation.{u}) {X : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (𝒞 : X.Modules) (r : ℕ)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} 𝒞 r]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} 𝒞] (hr : r ≠ 0) :
    haveI := flat_projectiveCompletionProj 𝒞 r
    haveI := locallyOfFiniteType_projectiveCompletionProj 𝒞 r
    (∀ t : ℕ, 0 < t → t < r →
      perfectChernClass C (projectiveCompletionProj 𝒞 ≫ sX)
        (hasDefinedChernClasses_pushforward_zeroSection 𝒞 r) t = 0) ∧
    (∀ (k : ℤ) (α : chowGroup C (𝟙 _ ≫ projectiveCompletionProj 𝒞 ≫ sX) (k + r)),
      chowGroupCast C ((complementOpen 𝒞).ι ≫ 𝟙 _ ≫ projectiveCompletionProj 𝒞 ≫ sX) (by ring)
        (bundlePullback C sX ((complementOpen 𝒞).ι ≫ 𝟙 _ ≫ projectiveCompletionProj 𝒞 ≫ sX)
        ((complementOpen 𝒞).ι ≫ projectiveCompletionProj 𝒞) (by simp) r
        (relativeDimension_complementOpen_ι_comp 𝒞 r) (k + r - r)
        (properChowPushforward C (𝟙 _ ≫ projectiveCompletionProj 𝒞 ≫ sX) sX
          (projectiveCompletionProj 𝒞) (by simp) (k + r - r)
          (properPushforwardFactorsThroughRationalEquivalence_of_isProper C _ sX _ (by simp) _)
          ((perfectChernClass C (projectiveCompletionProj 𝒞 ≫ sX)
            (hasDefinedChernClasses_pushforward_zeroSection 𝒞 r)).op (𝟙 _) (k + r) r α))) =
        ((-1 : ℤ) ^ (r - 1) * (Nat.factorial (r - 1) : ℤ)) •
          chowGroupOpensRestrictOfIsOpenImmersion C (𝟙 _ ≫ projectiveCompletionProj 𝒞 ≫ sX)
            (complementOpen 𝒞) (k + r) α) ∧
    (∀ {X' : Scheme.{u}} (sX' : X' ⟶ C.S) [LocallyOfFiniteType sX'] (g : X' ⟶ X)
      [LocallyOfFiniteType g] (hg : g ≫ sX = sX') (k : ℤ)
      (α : chowGroup C (pullback.snd g (projectiveCompletionProj 𝒞) ≫
        projectiveCompletionProj 𝒞 ≫ sX) (k + r)),
      chowGroupCast C _ (by ring) (bundlePullback C sX'
        ((complementOpenBaseChange g 𝒞).ι ≫ pullback.snd g (projectiveCompletionProj 𝒞) ≫
          projectiveCompletionProj 𝒞 ≫ sX)
        ((complementOpenBaseChange g 𝒞).ι ≫ pullback.fst g (projectiveCompletionProj 𝒞))
        (by rw [Category.assoc, pullback_fst_comp_eq_pullback_snd_comp C sX sX' g hg 𝒞]) r
        (relativeDimension_complementOpenBaseChange g 𝒞 r) (k + r - r)
        (properChowPushforward C
          (pullback.snd g (projectiveCompletionProj 𝒞) ≫ projectiveCompletionProj 𝒞 ≫ sX) sX'
          (pullback.fst g (projectiveCompletionProj 𝒞))
          (pullback_fst_comp_eq_pullback_snd_comp C sX sX' g hg 𝒞) (k + r - r)
          (properPushforwardFactorsThroughRationalEquivalence_of_isProper C _ sX' _
            (pullback_fst_comp_eq_pullback_snd_comp C sX sX' g hg 𝒞) _)
          ((perfectChernClass C (projectiveCompletionProj 𝒞 ≫ sX)
            (hasDefinedChernClasses_pushforward_zeroSection 𝒞 r)).op
            (pullback.snd g (projectiveCompletionProj 𝒞)) (k + r) r α))) =
        ((-1 : ℤ) ^ (r - 1) * (Nat.factorial (r - 1) : ℤ)) •
          chowGroupOpensRestrictOfIsOpenImmersion C
            (pullback.snd g (projectiveCompletionProj 𝒞) ≫ projectiveCompletionProj 𝒞 ≫ sX)
            (complementOpenBaseChange g 𝒞) (k + r) α)

Tag 0FEG, a lemma

Tag 0FEG in the Stacks Project.

Stacks.Chow.isRegularImmersionChernFormula_regularImmersionStructureSheafSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/RegularImmersionChernFormula.lean, line 111. The attribute's comment: “the whole lemma: c_t(Z → X, i_O_Z) = 0 for 0 < t < r and c_r(Z → X, i_O_Z) = (-1)^{r-1}(r-1)! c(Z → X, N), for X quasi-compact or with quasi-compact irreducible components and r ≥ 1 (presupposed by (r-1)!)”.

Let i : Z ⟶ X be a regular closed immersion of codimension r ≥ 1 of schemes locally of finite type over the base of chapter 42, with X quasi-compact or with quasi-compact irreducible components, and 𝒩 = 𝒞_{Z/X}^∨ its normal sheaf. Then c_t(Z ⟶ X, i_*𝒪_Z) = 0 for t = 1, …, r - 1 and c_r(Z ⟶ X, i_*𝒪_Z) = (-1)^{r-1}(r-1)! c(Z ⟶ X, 𝒩) in A^r(Z ⟶ X), the localized Chern classes being those of Definition 0FB5 (Stacks.Chow.LocalizedSituation.IsRegularImmersionChernFormula for the situation Stacks.Chow.regularImmersionStructureSheafSituation of i_*𝒪_Z). The codimension is positive, as the factor (r-1)! of the source presupposes.

theorem isRegularImmersionChernFormula_regularImmersionStructureSheafSituation (hr : 0 < r) :
    (regularImmersionStructureSheafSituation C sX i hreg hX 0).IsRegularImmersionChernFormula
      (isZeroOnComplement_regularImmersionStructureSheafSituation C sX i hreg hX 0) hreg hr

Tag 0FEH, a lemma

Tag 0FEH in the Stacks Project.

Stacks.Chow.regularImmersionStructureSheafSituation_capFundamentalClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/RegularImmersionChernFormula.lean, line 146. The attribute's comment: “all four parts, for X quasi-compact or with quasi-compact irreducible components, r ≥ 1 and dim_δ(X) ≤ n (the source's dim_δ(X) = n)”.

Let i : Z ⟶ X be a regular closed immersion of codimension r ≥ 1 of schemes locally of finite type over the base, X quasi-compact or with quasi-compact irreducible components, and dim_δ(X) ≤ n (the source's dim_δ(X) = n). Then

1. c_t(Z ⟶ X, i_*𝒪_Z) ∩ [X]_n = 0 for 1 ≤ t < r,
2. c_r(Z ⟶ X, i_*𝒪_Z) ∩ [X]_n = (-1)^{r-1}(r-1)! [Z]_{n-r},
3. ch_t(Z ⟶ X, i_*𝒪_Z) ∩ [X]_n = 0 for 0 ≤ t < r, and
4. ch_r(Z ⟶ X, i_*𝒪_Z) ∩ [X]_n = [Z]_{n-r},

with c_t(Z ⟶ X, i_*𝒪_Z) the class of Stacks 0FB2 for the situation in degree t.

theorem regularImmersionStructureSheafSituation_capFundamentalClass (hr : 0 < r) (n : ℤ)
    (hXn : schemeDeltaDimension C sX ≤ (n : EInt)) :
    (∀ (t : ℕ) (ht : 0 < t), t < r →
      capFundamentalClassAt C (gysinSystemOfInvertible C) (i ≫ sX) sX i rfl t n
        ((regularImmersionStructureSheafSituation C sX i hreg hX t).localizedChern
          (isFiniteLocallyFreeOfRankLTOnComplement_regularImmersionStructureSheafSituation C sX
            i hreg hX ht)) = 0) ∧
    capFundamentalClassAt C (gysinSystemOfInvertible C) (i ≫ sX) sX i rfl r n
        ((regularImmersionStructureSheafSituation C sX i hreg hX r).localizedChern
          (isFiniteLocallyFreeOfRankLTOnComplement_regularImmersionStructureSheafSituation C sX
            i hreg hX hr)) =
      ((-1 : ℤ) ^ (r - 1) * ((r - 1).factorial : ℤ)) • fundamentalChowClass C (i ≫ sX) (n - r) ∧
    (∀ t : ℕ, t < r →
      (capFundamentalClassAt C (gysinSystemOfInvertible C) (i ≫ sX) sX i rfl t
          n).toIntLinearMap.lTensor ℚ
        ((regularImmersionStructureSheafSituation C sX i hreg hX 0).localizedChernChar
          (isZeroOnComplement_regularImmersionStructureSheafSituation C sX i hreg hX 0) t) = 0) ∧
    (capFundamentalClassAt C (gysinSystemOfInvertible C) (i ≫ sX) sX i rfl r
        n).toIntLinearMap.lTensor ℚ
        ((regularImmersionStructureSheafSituation C sX i hreg hX 0).localizedChernChar
          (isZeroOnComplement_regularImmersionStructureSheafSituation C sX i hreg hX 0) r) =
      (1 : ℚ) ⊗ₜ[ℤ] fundamentalChowClass C (i ≫ sX) (n - r)

Sources

• Section 42.55, Tag 0FED
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.homComponent_exteriorPowerChernAltProd · Stacks.Chow.homPart_altExteriorTotalChern · Stacks.Chow.altExteriorChernProduct_apply · Stacks.Chow.ProjectiveCompletion.bivariantClass_zeroSecObject · Stacks.Chow.ProjectiveCompletion.chernClasses_zeroSecObject · Stacks.Chow.chernClass_pushforward_zeroSection · Stacks.Chow.isRegularImmersionChernFormula_regularImmersionStructureSheafSituation · Stacks.Chow.regularImmersionStructureSheafSituation_capFundamentalClass

Section42.56 An Adams operator#

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

Tag 0FEJ, a lemma

Tag 0FEJ in the Stacks Project.

AlgebraicGeometry.VectorBundleKZero.exists_secondAdamsOperator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperator.lean, line 555. The attribute's comment: “the ring map, its value on invertible modules and its compatibility with pullback, granted SquarePowersData: the filtration of Sym² and ⋀² along a short exact sequence and the two short exact sequences for the squares of a tensor product”.

Stacks Project, Tag 0FEJ. For a scheme X there is a ring map ψ² : K₀(Vect(X)) → K₀(Vect(X)) which sends [ℒ] to [ℒ^{⊗2}] when ℒ is invertible and is compatible with pullbacks. It is given on the class of a finite locally free module ℰ by ψ²([ℰ]) = [Sym² ℰ] - [⋀² ℰ].

The three clauses of the source are present: ψ² is a RingHom, the second conjunct is its value on an invertible module, and the third is its commutation with any ring map of Grothendieck rings realising pullback of finite locally free modules. The first conjunct records the construction ψ²([ℰ]) = [Sym² ℰ] - [⋀² ℰ].

The hypothesis SquarePowersData X is the geometric input of the source's proof: the filtration of the two squares along a short exact sequence and the two short exact sequences computing the squares of a tensor product, neither of which is available in the library. The value on an invertible module is not assumed; it is proved.

theorem exists_secondAdamsOperator (X : Scheme.{u}) (h : SquarePowersData X) :
    ∃ ψ : VectorBundleKZero X →+* VectorBundleKZero X,
      (∀ E : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
          ψ (classOf X E) =
            classOf X (secondSymmetricPower X E) - classOf X (secondExteriorPower X E)) ∧
        (∀ L : X.Modules,
          ∀ _ : Stacks.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L,
            ψ (classOf X L) = classOf X (Scheme.Modules.tensorObjRingedSpace X L L)) ∧
        (∀ (Y : Scheme.{u}) (f : Y ⟶ X) (hY : SquarePowersData Y)
            (p : VectorBundleKZero X →+* VectorBundleKZero Y),
          (∀ E : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
              p (classOf X E) = classOf Y ((Scheme.Modules.pullback f).obj E)) →
            (∀ E : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
              IsFiniteLocallyFree.{u, u, u} (R := Y.ringCatSheaf)
                ((Scheme.Modules.pullback f).obj E)) →
              ∀ a : VectorBundleKZero X, secondAdamsAddHom hY (p a) = p (ψ a))

AlgebraicGeometry.VectorBundleKZero.exists_secondAdamsOperator_pullbackRingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/VectorBundleKZeroPullback.lean, line 211. The attribute's comment: “the family of ring maps ψ²_X, its value on finite locally free and on invertible modules, and its compatibility with pullback ψ²_Y ∘ f^* = f^* ∘ ψ²_X for the pullback ring map f^* of K₀(Vect(-)) constructed here; no hypothesis”.

For every scheme X there is a ring map ψ²_X : K₀(Vect(X)) → K₀(Vect(X)) with ψ²_X([ℰ]) = [Sym² ℰ] - [⋀² ℰ] on finite locally free modules, ψ²_X([ℒ]) = [ℒ ⊗ ℒ] on invertible modules, and compatible with pullbacks: for every morphism f : Y ⟶ X, ψ²_Y ∘ f^* = f^* ∘ ψ²_X, where f^* is the pullback ring map pullbackRingHom f.

theorem exists_secondAdamsOperator_pullbackRingHom :
    ∃ ψ : ∀ X : Scheme.{u}, VectorBundleKZero X →+* VectorBundleKZero X,
      (∀ (X : Scheme.{u}) (E : X.Modules),
          IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
            ψ X (classOf X E) =
              classOf X (secondSymmetricPower X E) - classOf X (secondExteriorPower X E)) ∧
        (∀ (X : Scheme.{u}) (L : X.Modules),
          Stacks.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L →
            ψ X (classOf X L) = classOf X (Scheme.Modules.tensorObjRingedSpace X L L)) ∧
        (∀ {X Y : Scheme.{u}} (f : Y ⟶ X),
          (ψ Y).comp (pullbackRingHom f) = (pullbackRingHom f).comp (ψ X))

Tag 0FEK, a remark

Tag 0FEK in the Stacks Project.

Stacks.SecondAdamsPerfect.swapSquare_comp_swapSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfect.lean, line 150. The attribute's comment: “the switch of the two factors of a tensor square is an involution”.

The switch is an involution. This is the symmetry of the commutativity constraint, read at (L, L), and it is what makes the group {±1} act on L ⊗ L.

theorem swapSquare_comp_swapSquare (L : C) : swapSquare L ≫ swapSquare L = 𝟙 (L ⊗ L)

Stacks.SecondAdamsPerfect.swapSquareAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfect.lean, line 157. The attribute's comment: “the action of the group of units {±1} on the tensor square by switching the two factors”.

The action of the group {±1} on L ⊗ L by switching the factors: the unit 1 acts by the identity and the unit -1 by the switch, which is an involution.

def swapSquareAction (L : C) : ℤˣ →* End (L ⊗ L)

Stacks.SecondAdamsPerfect.invariantProjector_add_antiInvariantProjector, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfect.lean, line 198. The attribute's comment: “the invariant and anti-invariant projectors of the switch are complementary”.

The two projectors are complementary: their sum is the identity of L ⊗ L.

theorem invariantProjector_add_antiInvariantProjector :
    invariantProjector R L + antiInvariantProjector R L = 𝟙 (L ⊗ L)

Stacks.SecondAdamsPerfect.cls_tensorObj_eq_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfect.lean, line 342. The attribute's comment: “the class of the tensor square is the sum of the classes of the invariants and of the anti-invariants of the switch”.

[L ⊗ L] = [(L ⊗ L)^+] + [(L ⊗ L)^-] in the K-group: the invariants and the anti-invariants of the switch exhibit the tensor square as their biproduct, and the split triangle on a biproduct is distinguished.

theorem cls_tensorObj_eq_add (P : IdempotentSplitting (invariantProjector R L))
    (N : IdempotentSplitting (antiInvariantProjector R L)) :
    K0.cls (L ⊗ L) = K0.cls P.obj + K0.cls N.obj

Stacks.SecondAdamsPerfect.cls_sub_cls_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfect.lean, line 368. The attribute's comment: “the difference of the classes of the invariants and of the anti-invariants of the switch on the tensor square is a well-defined element of the K-group attached to the object; its additivity along distinguished triangles is not proved”.

The difference [(L ⊗ L)^+] - [(L ⊗ L)^-] is independent of the chosen invariants and anti-invariants, hence a well-defined element of the K-group attached to L. This is the value the second Adams operator of the source is to take on L.

theorem cls_sub_cls_eq (P P' : IdempotentSplitting (invariantProjector R L))
    (N N' : IdempotentSplitting (antiInvariantProjector R L)) :
    K0.cls P.obj - K0.cls N.obj = K0.cls P'.obj - K0.cls N'.obj

Stacks.SecondAdamsPerfect.derivedSwapSquare_comp_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfect.lean, line 404. The attribute's comment: “the switch of the two factors of the derived tensor square on a ringed space is an involution”.

The switch of the two factors of L ⊗^L_{O_X} L is an involution.

theorem derivedSwapSquare_comp_self (L : DerivedCategory (StructureSheafModules Rc)) :
    derivedSwapSquare Rc L ≫ derivedSwapSquare Rc L = 𝟙 (((derivedTensor Rc).obj L).obj L)

Stacks.SecondAdamsPerfect.derivedSwapSquareAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfect.lean, line 412. The attribute's comment: “the action of the group {±1} on the derived tensor square of an object of D(O_X) by switching the two factors”.

The action of the group {±1} on L ⊗^L_{O_X} L by switching the factors, in the derived category of a ringed space.

def derivedSwapSquareAction (L : DerivedCategory (StructureSheafModules Rc)) :
    ℤˣ →* End (((derivedTensor Rc).obj L).obj L)

AlgebraicGeometry.secondAdamsPerfect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfectKZero.lean, line 148. The attribute's comment: “the second Adams operator ψ² on K₀(D_perf(𝒪_X)), for any model of D(𝒪_X), as an additive endomorphism; its value on classes is secondAdamsPerfect_cls, and its well-definedness (additivity along distinguished triangles) is secondAdamsPerfect_distinguished”.

The second Adams operator ψ² on K₀(D_perf(𝒪_X)), for a scheme X on which 2 is invertible: the additive endomorphism sending the class of a perfect object L to [(L ⊗^L L)^+] - [(L ⊗^L L)^-] (secondAdamsPerfect_cls).

def secondAdamsPerfect (h2 : IsUnit (2 : Γ(X, ⊤))) :
    K0 𝒟ₚ →+ K0 𝒟ₚ

AlgebraicGeometry.exists_switchSplittings_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfectKZero.lean, line 160. The attribute's comment: “the invariants (L ⊗^L L)^+ and the anti-invariants (L ⊗^L L)^- of the switch on the derived tensor square of a perfect object exist, and are perfect for every choice”.

For a perfect object L of D(𝒪_X), with 2 invertible on X, the idempotents (𝟙 + σ)/2 and (𝟙 - σ)/2 of the switch σ of L ⊗^L L split, and the objects splitting them — the invariants (L ⊗^L L)^+ and the anti-invariants (L ⊗^L L)^- — are perfect, whichever splittings are taken.

theorem exists_switchSplittings_perfect (h2 : IsUnit (2 : Γ(X, ⊤))) (L : 𝒟ₚ) :
    letI := derivedMonoidal X.toRingedSpace.sheaf
    letI := derivedSymmetric X.toRingedSpace.sheaf
    haveI := isIso_two_smul_id X.toRingedSpace.sheaf (isUnit_two_presheaf_obj X h2)
    Nonempty (IdempotentSplitting
        (invariantIdempotent ((β_ L.obj L.obj).hom : L.obj ⊗ L.obj ⟶ _))) ∧
      Nonempty (IdempotentSplitting
        (antiInvariantIdempotent ((β_ L.obj L.obj).hom : L.obj ⊗ L.obj ⟶ _))) ∧
      (∀ s : IdempotentSplitting
        (invariantIdempotent ((β_ L.obj L.obj).hom : L.obj ⊗ L.obj ⟶ _)),
          IsPerfect (X := X.toRingedSpace) s.obj) ∧
      (∀ s : IdempotentSplitting
        (antiInvariantIdempotent ((β_ L.obj L.obj).hom : L.obj ⊗ L.obj ⟶ _)),
          IsPerfect (X := X.toRingedSpace) s.obj)

AlgebraicGeometry.secondAdamsPerfect_cls, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfectKZero.lean, line 185. The attribute's comment: “ψ²([L]) = [(L ⊗^L L)^+] - [(L ⊗^L L)^-] for every perfect L and every choice of the invariants and the anti-invariants of the switch”.

For a scheme X on which 2 is invertible and a perfect object L of D(𝒪_X), the second Adams operator sends the class of L to the class of the invariants minus the class of the anti-invariants of the switch on L ⊗^L L, for any choice of the two (which exist and are perfect by exists_switchSplittings_perfect).

theorem secondAdamsPerfect_cls (h2 : IsUnit (2 : Γ(X, ⊤))) (L : 𝒟ₚ) :
    letI := derivedMonoidal X.toRingedSpace.sheaf
    letI := derivedSymmetric X.toRingedSpace.sheaf
    haveI := isIso_two_smul_id X.toRingedSpace.sheaf (isUnit_two_presheaf_obj X h2)
    ∀ (sp : IdempotentSplitting
        (invariantIdempotent ((β_ L.obj L.obj).hom : L.obj ⊗ L.obj ⟶ _)))
      (sm : IdempotentSplitting
        (antiInvariantIdempotent ((β_ L.obj L.obj).hom : L.obj ⊗ L.obj ⟶ _)))
      (hp : IsPerfect (X := X.toRingedSpace) sp.obj) (hm : IsPerfect (X := X.toRingedSpace) sm.obj),
      secondAdamsPerfect X h2 (K0.cls L) = K0.cls (⟨sp.obj, hp⟩ : 𝒟ₚ) -
        K0.cls (⟨sm.obj, hm⟩ : 𝒟ₚ)

AlgebraicGeometry.secondAdamsPerfect_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfectKZero.lean, line 210. The attribute's comment: “well-definedness on K₀: [(L ⊗^L L)^+] - [(L ⊗^L L)^-] is additive along distinguished triangles of D_perf(𝒪_X), for every choice of invariants and anti-invariants”.

For a distinguished triangle L₁ ⟶ L₂ ⟶ L₃ ⟶ L₁[1] of D_perf(𝒪_X), 2 being invertible on X, and for any choices sᵢ^± of the invariants and the anti-invariants of the switch on Lᵢ ⊗^L Lᵢ,

[s₂^+] - [s₂^-] = ([s₁^+] - [s₁^-]) + ([s₃^+] - [s₃^-])

in K₀(D_perf(𝒪_X)).

theorem secondAdamsPerfect_distinguished (h2 : IsUnit (2 : Γ(X, ⊤)))
    (T : Triangle 𝒟ₚ) (hT : T ∈ distTriang _) :
    letI := derivedMonoidal X.toRingedSpace.sheaf
    letI := derivedSymmetric X.toRingedSpace.sheaf
    haveI := isIso_two_smul_id X.toRingedSpace.sheaf (isUnit_two_presheaf_obj X h2)
    ∀ (sp₁ : IdempotentSplitting
        (invariantIdempotent ((β_ T.obj₁.obj T.obj₁.obj).hom : T.obj₁.obj ⊗ T.obj₁.obj ⟶ _)))
      (sm₁ : IdempotentSplitting
        (antiInvariantIdempotent ((β_ T.obj₁.obj T.obj₁.obj).hom : T.obj₁.obj ⊗ T.obj₁.obj ⟶ _)))
      (sp₂ : IdempotentSplitting
        (invariantIdempotent ((β_ T.obj₂.obj T.obj₂.obj).hom : T.obj₂.obj ⊗ T.obj₂.obj ⟶ _)))
      (sm₂ : IdempotentSplitting
        (antiInvariantIdempotent ((β_ T.obj₂.obj T.obj₂.obj).hom : T.obj₂.obj ⊗ T.obj₂.obj ⟶ _)))
      (sp₃ : IdempotentSplitting
        (invariantIdempotent ((β_ T.obj₃.obj T.obj₃.obj).hom : T.obj₃.obj ⊗ T.obj₃.obj ⟶ _)))
      (sm₃ : IdempotentSplitting
        (antiInvariantIdempotent ((β_ T.obj₃.obj T.obj₃.obj).hom : T.obj₃.obj ⊗ T.obj₃.obj ⟶ _)))
      (hp₁ : IsPerfect (X := X.toRingedSpace) sp₁.obj)
      (hm₁ : IsPerfect (X := X.toRingedSpace) sm₁.obj)
      (hp₂ : IsPerfect (X := X.toRingedSpace) sp₂.obj)
      (hm₂ : IsPerfect (X := X.toRingedSpace) sm₂.obj)
      (hp₃ : IsPerfect (X := X.toRingedSpace) sp₃.obj)
      (hm₃ : IsPerfect (X := X.toRingedSpace) sm₃.obj),
      K0.cls (⟨sp₂.obj, hp₂⟩ : 𝒟ₚ) -
          K0.cls (⟨sm₂.obj, hm₂⟩ : 𝒟ₚ) =
        (K0.cls (⟨sp₁.obj, hp₁⟩ : 𝒟ₚ) -
          K0.cls (⟨sm₁.obj, hm₁⟩ : 𝒟ₚ)) +
        (K0.cls (⟨sp₃.obj, hp₃⟩ : 𝒟ₚ) -
          K0.cls (⟨sm₃.obj, hm₃⟩ : 𝒟ₚ))

AlgebraicGeometry.perfectKZeroSecondAdams, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SecondAdamsOperatorPerfectKZero.lean, line 250. The attribute's comment: “ψ² on K₀(X) = PerfectKZero X of Tag 0FDG: secondAdamsPerfect at the standard model of D(𝒪_X) that PerfectKZero is defined with”.

The second Adams operator on the group AlgebraicGeometry.PerfectKZero X = K₀(D_perf(𝒪_X)) of [Stacks, Tag 0FDG]: secondAdamsPerfect at the standard model of the derived category.

def perfectKZeroSecondAdams (h2 : IsUnit (2 : Γ(X, ⊤))) : PerfectKZero X →+ PerfectKZero X

Tag 0FV8, a lemma

Tag 0FV8 in the Stacks Project.

AlgebraicGeometry.VectorBundleKZero.exists_minusOneAdamsOperator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/MinusAdamsOperator.lean, line 411. The attribute's comment: “the ring map, its values on finite locally free modules and its compatibility with pullback”. References: SGA 6 VIII (3.4), “more general”.

The minus-one Adams operation. There is a ring endomorphism ψ^{-1} of K₀(Vect(X)) which sends the class of a finite locally free module to the class of its dual, and which commutes with duality along any ring map p : K₀(Vect(X)) → K₀(Vect(Y)) sending the class of a finite locally free module ℰ to the class of f^*ℰ, for a morphism f : Y ⟶ X.

theorem exists_minusOneAdamsOperator (X : Scheme.{u}) :
    ∃ ψ : VectorBundleKZero X →+* VectorBundleKZero X,
      (∀ M : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) M →
          ψ (classOf X M) = classOf X (dualSheaf X.toRingedSpace M)) ∧
        ∀ (Y : Scheme.{u}) (f : Y ⟶ X) (p : VectorBundleKZero X →+* VectorBundleKZero Y),
          (∀ M : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) M →
              p (classOf X M) = classOf Y ((Scheme.Modules.pullback f).obj M)) →
            ∀ a : VectorBundleKZero X,
              dualAddHom (dualPreservesFiniteLocallyFree Y) (dualShortExact Y) (p a) = p (ψ a)

Tag 0FEL, a remark

Tag 0FEL in the Stacks Project.

Stacks.Chow.totalChernKGroupMap_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/KGroupChernClass.lean, line 251.

Stacks 0FEL. Let X be locally of finite type over the base of chapter 42. The Chern class map c : K_0(Vect(X)) ⟶ ∏_{i ≥ 0} A^i(X):

1. sends a generator [ℰ], ℰ finite locally free of any rank, to c(ℰ) = 1 + c_1(ℰ) + c_2(ℰ) + …, whose degree-p component is the Chern class c_p(ℰ) of Stacks 0ESW and whose degree-0 component is 1;
2. is multiplicative, c(α + β) = c(α) c(β);
3. sends −[ℰ] to the formal inverse of c(ℰ), a two-sided inverse in ∏_{i ≥ 0} A^i(X);
4. is the only map with properties 1 and 2 (it is obtained "by extending multiplicatively").

It is well defined by the Whitney sum formula, Stacks 02UI (Stacks.Chow.totalChernClassOfModule_eq_mul_of_shortExact).

theorem totalChernKGroupMap_spec :
    (∀ (E : X.Modules) [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E],
      totalChernKGroupMap C sX (VectorBundleKZero.classOf X E) = totalChernClassOfModule C sX E ∧
        totalChernClassOfModule C sX E 0 = (1 : TotalChowClass C sX) 0 ∧
        ∀ p : ℕ, totalChernClassOfModule C sX E p = chernClassOfModule C sX E p) ∧
    (∀ α β : VectorBundleKZero X,
      totalChernKGroupMap C sX (α + β) = totalChernKGroupMap C sX α * totalChernKGroupMap C sX β) ∧
    (∀ (E : X.Modules) [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E],
      totalChernKGroupMap C sX (-VectorBundleKZero.classOf X E) *
          totalChernClassOfModule C sX E = 1 ∧
        totalChernClassOfModule C sX E *
          totalChernKGroupMap C sX (-VectorBundleKZero.classOf X E) = 1) ∧
    (∀ c : VectorBundleKZero X → TotalChowClass C sX,
      (∀ (E : X.Modules) [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E],
        c (VectorBundleKZero.classOf X E) = totalChernClassOfModule C sX E) →
      (∀ α β, c (α + β) = c α * c β) → c = totalChernKGroupMap C sX)

Stacks.Chow.chowCohomologySeries, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassKGroup.lean, line 185. The attribute's comment: “the target: the product over i >= 0 of the Chow cohomology groups A^i(X), with A^i(X) the group Stacks.Chow.chowCohomologyComponent of Stacks 0B7E”.

The target of Stacks 0FEL. The product ∏_{i ≥ 0} A^i(X) of the nonnegative-degree Chow cohomology groups of a scheme X locally of finite type over the base: a family (a_0, a_1, a_2, …) with a_i ∈ A^i(X), subject to no condition on its support.

The product and not the direct sum, and not the completion A^*(X)^∧ of Stacks 0FE0 either: the formal inverse of a total Chern class has a component in every degree in general, and that is the reason the source writes an infinite product.

abbrev chowCohomologySeries : Type (u + 1)

Stacks.Chow.chernClassKGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassKGroup.lean, line 665. The attribute's comment: “the map c : K_0(Vect(X)) -> prod_{i >= 0} A^i(X) itself, with K_0(Vect(X)) the Grothendieck group AlgebraicGeometry.VectorBundleKZero of Stacks 0FDK and A^i(X) the Chow cohomology Stacks.Chow.chowCohomologyComponent of Stacks 0B7E. CARRIED, as the two fields of the parameters R and D: (1) the ring structure of A^*(X)^∧, Stacks 0FE0 -- composition of bivariant classes, whose composite StacksDraft.AlgebraicGeometry.Chow.BivariantComposition .Class constructs as Stacks.Chow.bivariantComposite, though nothing here assembles the ring out of it -- namely a degreewise product A^i x A^j -> A^{i+j}, additive in each variable, a unit series, and associativity, commutativity and the unit law for the Cauchy product it defines; (2) the total Chern class series c(E) of each module; Stacks 0B7H is constructed here, as Stacks.Chow.chernClass, but relative to the Chern cap products of Stacks 0B7G that the characterization is read against (the parameter Stacks.Chow.HigherChernCapRule), which rest on Stacks 02U5 and 02U7 and are not formalized here; and (3) the Whitney sum formula c(E_2) = c(E_1) c(E_3) of Stacks 02UI in the source's product form, which is the well-definedness. The repository's Stacks 02UI, Stacks.Chow.chernCapOnChow_eq_sum_of_shortExact, is the relation read componentwise on Chow groups between cap products and does not give the product form: that deduction needs the bivariant Chern classes of Stacks 0B7H, the composition product of Stacks 0FE0 and the compatibility of the cap operation of a composite with the two cap operations; the first two are available, the degreewise product built from the composite and the last are not. NOT carried, and constructed here: the product prod_{i >= 0} A^i(X), the Cauchy product on it, the formal inverse of a series with constant term 1 and the proof that it inverts, the group of such series, and the map c with the three properties below”.

Stacks 0FEL. The Chern class map

c : K_0(Vect(X)) ⟶ ∏_{i ≥ 0} A^i(X),

sending the generator [ℰ] to c(ℰ) = 1 + c_1(ℰ) + c_2(ℰ) + … and extended multiplicatively; so −[ℰ] goes to the formal inverse c(ℰ)^{-1}, which is why the target is the infinite product. It is well defined by the Whitney sum formula of Stacks 02UI.

def chernClassKGroup (D : TotalChernClassSeries C G sX R) :
    AlgebraicGeometry.VectorBundleKZero X → chowCohomologySeries C G sX

Stacks.Chow.chernClassKGroup_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassKGroup.lean, line 682. The attribute's comment: “the multiplicativity -- extending multiplicatively -- of the map, which is its well-definedness on K_0(Vect(X)); the Whitney sum formula of Stacks 02UI is carried, see the attribute on Stacks.Chow.chernClassKGroup”.

The Chern class map is multiplicative, which is what "extending multiplicatively" means: the sum in K_0(Vect(X)) goes to the Cauchy product of series. This is the content Stacks 02UI supplies.

theorem chernClassKGroup_add (D : TotalChernClassSeries C G sX R)
    (α β : AlgebraicGeometry.VectorBundleKZero X) :
    chernClassKGroup D (α + β) =
      chowSeriesMul R.gradedMul (chernClassKGroup D α) (chernClassKGroup D β)

Stacks.Chow.chernClassKGroup_neg_classOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassKGroup.lean, line 710. The attribute's comment: “the clause that -[E] is sent to the formal inverse c(E)^{-1}, which is why the target is an infinite product; the formal inverse is constructed here by the recursion Stacks.Chow.ChowCohomologySeriesRing.formalInverse_succ and is not carried”.

Stacks 0FEL, the last clause of the remark. −[ℰ] is sent to the formal inverse c(ℰ)^{-1}: its coefficients are given by the recursion of Stacks.Chow.ChowCohomologySeriesRing.formalInverse_succ, which is not supported in finitely many degrees in general, and the Cauchy product of c([ℰ]) with it is the unit series. This is why the target of the map is the infinite product ∏_{i ≥ 0} A^i(X) rather than a finite sum.

theorem chernClassKGroup_neg_classOf (D : TotalChernClassSeries C G sX R) (E : X.Modules) :
    chernClassKGroup D (-AlgebraicGeometry.VectorBundleKZero.classOf X E) =
        R.formalInverse (D.ch E) ∧
      chowSeriesMul R.gradedMul (D.ch E)
        (chernClassKGroup D (-AlgebraicGeometry.VectorBundleKZero.classOf X E)) = R.one

Tag 0FEM, a remark

Tag 0FEM in the Stacks Project.

AlgebraicGeometry.VectorBundleKZero.existsUnique_ringHom_of_tensorMultiplicative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernCharacterKGroup.lean, line 43. The attribute's comment: “the canonical ring map on K₀(Vect(X)) that the Chern character defines, and its uniqueness; additivity along short exact sequences (Tag 0F9C), multiplicativity on tensor products (Tag 0F9D) and the value on 𝒪_X are properties of the Chern character of a module and are hypotheses, and ∏_{i ≥ 0} A^i(X) ⊗ 𝐐 is read as an arbitrary ring, which it has no construction as in this repository”.

An assignment ℰ ↦ ch(ℰ) of an element of a ring R to each 𝒪_X-module which vanishes off the finite locally free modules, is additive along their short exact sequences and multiplicative on tensor products, and takes the value 1 on 𝒪_X, extends to a ring homomorphism on K₀(Vect(X)), and to exactly one. For the Chern character with values in ∏_{i ≥ 0} A^i(X) ⊗ 𝐐 this is the ring map ch : K₀(Vect(X)) ⟶ ∏_{i ≥ 0} A^i(X) ⊗ 𝐐.

theorem existsUnique_ringHom_of_tensorMultiplicative
    (hzero : ∀ M : X.Modules,
      ¬ IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) M → ch M = 0)
    (hadd : ∀ {E F G : X.Modules} (f : E ⟶ F) (g : F ⟶ G) (w : f ≫ g = 0),
      IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
        IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) F →
          IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) G →
            Mono f → Epi g → (ShortComplex.mk f g w).Exact → ch F = ch E + ch G)
    (hmul : ∀ M N : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) M →
      IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) N →
        ch (Scheme.Modules.tensorObjRingedSpace X M N) = ch M * ch N)
    (hone : ch (SheafOfModules.unit X.ringCatSheaf) = 1) :
    ∃! φ : VectorBundleKZero X →+* R,
      ∀ M : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) M →
        φ (classOf X M) = ch M

Stacks.Chow.chernCharacterRingHom_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/KGroupChernCharacter.lean, line 346.

Let X be locally of finite type over the base of chapter 42. The Chern character defines a canonical ring map

ch : K_0(Vect(X)) ⟶ ∏_{i ≥ 0} A^i(X) ⊗ 𝐐

(Stacks.Chow.chernCharacterRingHom, a ring homomorphism into the ring Stacks.Chow.instRingFullRationalChowCohomology) which

1. sends a generator [ℰ], ℰ finite locally free of any rank, to ch(ℰ), whose degree-p component is ch_p(ℰ) = P_p(ℰ)/p! (Stacks.Chow.moduleChernCharacterComponent);
2. is the only ring map with property 1 (it is obtained "by extending additively").

It is well defined by Stacks 0F9C (Stacks.Chow.moduleChernCharacter_eq_add_of_shortExact) and a ring map by Stacks 0F9D (Stacks.Chow.moduleChernCharacter_tensorObj).

theorem chernCharacterRingHom_spec :
    (∀ (E : X.Modules) [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E],
      chernCharacterRingHom C sX (VectorBundleKZero.classOf X E) = moduleChernCharacter C sX E ∧
        ∀ p : ℕ, chernCharacterRingHom C sX (VectorBundleKZero.classOf X E) p =
          ((Nat.factorial p : ℚ)⁻¹) ⊗ₜ[ℤ] modulePowerSumComponentArbitraryRank C sX E p) ∧
    (∀ φ : VectorBundleKZero X →+* fullRationalChowCohomology C (gysinSystemOfInvertible C) sX,
      (∀ (E : X.Modules) [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E],
        φ (VectorBundleKZero.classOf X E) = moduleChernCharacter C sX E) →
      φ = chernCharacterRingHom C sX)

Stacks.Chow.existsUnique_ringHom_chernCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/ChernCharacterMultiplicative.lean, line 288. The attribute's comment: “the remark as stated: the unique ring map K_0(Vect(X)) -> prod over i >= 0 of A^i(X) tensor Q sending [E] to ch(E), for every X locally of finite type over S, with no further hypothesis; the target is the ring Stacks.Chow.RationalTotalChowClass C sX (Cauchy product of the products A^i(X) x A^j(X) -> A^{i+j}(X) of Stacks 0B75, tensored with Q), ch(E) is Stacks.Chow.rationalTotalChernCharacter (components P_p(E)/p!, E of arbitrary rank), and the map is Stacks.Chow.rationalTotalChernCharacterRingHom; additivity is Stacks 0F9C and multiplicativity Stacks 0F9D, both proved”.

Stacks 0FEM. The Chern character defines a canonical ring map

ch : K_0(Vect(X)) ⟶ ∏_{i ≥ 0} A^i(X) ⊗ 𝐐:

there is a unique ring homomorphism sending the class of every finite locally free 𝒪_X-module ℰ, of arbitrary rank, to its Chern character ch(ℰ) = (P_p(ℰ)/p!)_{p ≥ 0}. It is Stacks.Chow.rationalTotalChernCharacterRingHom.

theorem existsUnique_ringHom_chernCharacter :
    ∃! φ : VectorBundleKZero X →+* RationalTotalChowClass C sX,
      ∀ (E : X.Modules) [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E],
        φ (VectorBundleKZero.classOf X E) = rationalTotalChernCharacter C sX E

Tag 0FEN, a lemma

Tag 0FEN in the Stacks Project.

Stacks.Chow.chernClassKGroup_secondAdams, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperatorChernScaling.lean, line 620. The attribute's comment: “the first equation, c_i(psi^2(alpha)) = 2^i c_i(alpha), for every alpha in K_0(Vect(X)); psi^2 is AlgebraicGeometry.VectorBundleKZero.secondAdamsRingHom of Stacks 0FEJ and c is Stacks.Chow.chernClassKGroup of Stacks 0FEL, so the parameters R, D and hX are the data those two already carry. CARRIED in addition: (1) the splitting principle of Stacks 02UL, not formalized in this repository, as Stacks.Chow.HasSecondAdamsSplitting -- a family of morphisms p_r : P_r -> X, jointly injective on each A^i(X), along each of which [E] becomes a sum of classes of invertible modules, together with the restriction map of Stacks 0B7F and its multiplicativity and Chern class compatibility (which Stacks 0B7F does not formalize, needing the composition product of Stacks 0FE0) and the functoriality of K_0(Vect(-)) (which this repository does not construct, as the notes of StacksFrontier.AlgebraicGeometry.Chow.SecondAdamsOperator record); the family rather than a single morphism is what keeps modules of non-constant rank in scope, since the source reduces to constant rank over the rank loci (Stacks 0ESW) before applying Stacks 02UL; and (2) Stacks 02U0 and Stacks 02SZ, the vanishing of c_j of an invertible module above degree 1 and the additivity c_1(L tensor L) = 2 c_1(L), with Stacks 01CT (1), as Stacks.Chow.InvertibleChernClassData -- properties of the bivariant Chern classes of Stacks 0B7H, which this repository characterizes but does not construct. NOT carried, and proved here: that the 2^i-scaling of A^i(X) is a ring endomorphism of the product (the source's first step, which is what reduces the lemma to additive generators), the base case c(L tensor L) = 1 + 2 c_1(L), the value psi^2([L]) = [L tensor L] (proved in Stacks 0FEJ), the computation of c(psi^2(alpha)) on a sum of classes of invertible modules, and the descent along the pullback”.

Stacks Project, Tag 0FEN, the first equation. Let (S, δ) be as in Stacks 02QL, let X be locally of finite type over S, let ψ² be the second Adams operation of Stacks 0FEJ and let c be the Chern class map of Stacks 0FEL. Then

c_i(ψ²(α)) = 2^i c_i(α)

for every α ∈ K_0(Vect(X)) and every i ≥ 0.

The parameters R, D and hX are the data Stacks 0FEL and Stacks 0FEJ already carry; hsplit is the splitting principle of Stacks 02UL, which the source's proof uses and which this repository does not have, in the shape Stacks.Chow.SecondAdamsSplitting records. The scaling map is not assumed to be a ring map, the base case is not assumed, and the descent is proved.

theorem chernClassKGroup_secondAdams {D : TotalChernClassSeries C G sX R}
    (hX : SquarePowersData X)
    (hsplit : ∀ E : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
      HasSecondAdamsSplitting C G sX R D hX E)
    (α : VectorBundleKZero X) (i : ℕ) :
    chernClassKGroup D (secondAdamsRingHom hX α) i =
      ((2 : ℕ) ^ i) • chernClassKGroup D α i

Stacks.Chow.chernCharacterKGroup_secondAdams, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperatorChernScaling.lean, line 704. The attribute's comment: “the second equation, ch_i(psi^2(alpha)) = 2^i ch_i(alpha), for every alpha in K_0(Vect(X)); ch is Stacks.Chow.chernCharacterKGroup, the Chern character of Stacks 0FEM written out as ch_p(alpha) = P_p(c_1(alpha), ..., c_p(alpha))/p! in the product over p >= 0 of A^p(X) tensor Q, which is the library's Stacks.Chow.fullRationalChowCohomology. It is deduced from the first equation rather than proved by a second splitting argument. CARRIED in addition to what the first equation carries: the power sums P_p themselves, as Stacks.Chow.NewtonPowerSums, with their additivity for the Cauchy product (Stacks 0F9C) and their weighted homogeneity of degree p -- Stacks.Chow.powerSumClassArbitraryRank of Stacks 0ESX assembles the power sums over the rank loci from a quantified family rather than from a polynomial expression, so neither property can be read off here. The weighted homogeneity is a combinatorial property of P_p alone, with no geometry in it”.

Stacks Project, Tag 0FEN, the second equation. In the situation of Stacks.Chow.chernClassKGroup_secondAdams, with ch the Chern character of Stacks 0FEM,

ch_i(ψ²(α)) = 2^i ch_i(α)

for every α ∈ K_0(Vect(X)) and every i ≥ 0.

This is deduced from the first equation in its series form, Stacks.Chow.chernClassKGroup_secondAdams_eq_chowSeriesScale, together with the weighted homogeneity of the Newton power sums: ch_i is P_i(c_1, …, c_i)/i! and P_i is weighted homogeneous of degree i. No second splitting argument is needed.

theorem chernCharacterKGroup_secondAdams {D : TotalChernClassSeries C G sX R}
    (N : NewtonPowerSums C G sX R) (hX : SquarePowersData X)
    (hsplit : ∀ E : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
      HasSecondAdamsSplitting C G sX R D hX E)
    (α : VectorBundleKZero X) (i : ℕ) :
    chernCharacterKGroup (D := D) N (secondAdamsRingHom hX α) i =
      ((2 : ℕ) ^ i) • chernCharacterKGroup (D := D) N α i

Stacks.Chow.chernClass_chernCharacter_secondAdams, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChernClassArbitraryRank/SecondAdamsChernScaling.lean, line 513.

Let (S, δ) be as in Situation 02QL and let X be locally of finite type over S. Let ψ² be the second Adams operator of Stacks 0FEJ (AlgebraicGeometry.VectorBundleKZero.secondAdamsRingHom at AlgebraicGeometry.VectorBundleKZero.squarePowersData X), and let c and ch be the maps of Stacks 0FEL and Stacks 0FEM (Stacks.Chow.totalChernKGroupMap, into ∏_{i ≥ 0} A^i(X), and Stacks.Chow.chernCharacterRingHom, into ∏_{i ≥ 0} A^i(X) ⊗ 𝐐). Then for every α ∈ K_0(Vect(X)) and every i

c_i(ψ²(α)) = 2^i c_i(α) and ch_i(ψ²(α)) = 2^i ch_i(α),

the subscript i being the component in A^i(X), resp. A^i(X) ⊗ 𝐐.

theorem chernClass_chernCharacter_secondAdams (α : VectorBundleKZero X) (i : ℕ) :
    totalChernKGroupMap C sX
        (VectorBundleKZero.secondAdamsRingHom (VectorBundleKZero.squarePowersData X) α) i =
      (2 ^ i : ℤ) • totalChernKGroupMap C sX α i ∧
    chernCharacterRingHom C sX
        (VectorBundleKZero.secondAdamsRingHom (VectorBundleKZero.squarePowersData X) α) i =
      (2 ^ i : ℤ) • chernCharacterRingHom C sX α i

Stacks.Chow.chernCharacterVectorBundle_secondAdams, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/SecondAdamsChernCharacter.lean, line 245. The attribute's comment: “the ch_i equation: ch_p(ψ²(α)) = 2^p ch_p(α), for every α ∈ K_0(Vect(X)) and every X locally of finite type over S, with no further hypothesis: ψ² is AlgebraicGeometry.VectorBundleKZero.secondAdamsRingHom (Stacks 0FEJ) and ch is Stacks.Chow.chernCharacterVectorBundle (Stacks 0FEM), with values in A^p(X) ⊗ Q”.

Stacks Project, Tag 0FEN, the second equation. Let (S, δ) be as in Situation 42.7.1 and let X be locally of finite type over S. For every α ∈ K_0(Vect(X)) and every p ≥ 0,

ch_p(ψ²(α)) = 2^p ch_p(α) in A^p(X) ⊗ 𝐐,

where ψ² is the second Adams operation of Stacks 0FEJ and ch the Chern character of Stacks 0FEM.

theorem chernCharacterVectorBundle_secondAdams (a : VectorBundleKZero X) (p : ℕ) :
    chernCharacterVectorBundle C sX (secondAdamsRingHom (squarePowersData X) a) p =
      (2 ^ p : ℚ) • chernCharacterVectorBundle C sX a p

Stacks.Chow.totalChernKClass_secondAdams, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/SecondAdamsTotalChern.lean, line 475. The attribute's comment: “the c_i equation: c_i(ψ²(α)) = 2^i c_i(α) in A^i(X), for every α ∈ K_0(Vect(X)) and every X locally of finite type over S, with no further hypothesis: ψ² is AlgebraicGeometry.VectorBundleKZero.secondAdamsRingHom (Stacks 0FEJ) and c is the total Chern class map of Remark 0FEL, Stacks.Chow.totalChernKClass, constructed here for modules of arbitrary rank”.

Stacks Project, Tag 0FEN, the first equation. Let (S, δ) be as in Situation 42.7.1 and let X be locally of finite type over S. For every α ∈ K_0(Vect(X)) and every i ≥ 0,

c_i(ψ²(α)) = 2^i c_i(α) in A^i(X),

where ψ² is the second Adams operation of Stacks 0FEJ and c the total Chern class of Remark 0FEL (Stacks.Chow.totalChernKClass).

theorem totalChernKClass_secondAdams (a : VectorBundleKZero X) (i : ℕ) :
    totalChernKClass C sX (secondAdamsRingHom (squarePowersData X) a) i =
      (2 ^ i : ℤ) • totalChernKClass C sX a i

Tag 0FEP, a remark

Tag 0FEP in the Stacks Project.

AlgebraicGeometry.supportedPerfectEulerHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/PerfectToSupportedCoherent.lean, line 166. The attribute's comment: “the homomorphism K_0(D_{Z, perf}(O_X)) → K_0(Coh_Z(X)). Two departures from the source, both recorded in the module docstring: the value on a class is the alternating sum ∑_n (-1)^n [H^n(E)] rather than [⊕_n H^{2n}(E)] - [⊕_n H^{2n+1}(E)] (the same element of K_0, but the identification of the two expressions is NOT proved here), and X is assumed Noetherian regular, the hypotheses of Stacks 0FER, rather than merely locally Noetherian, because the global coherence and boundedness of the cohomology sheaves used here come from the converse half of Stacks 0FDC. The identification K_0(Coh_Z(X)) = K'_0(Z) is Stacks 0FDT and is NOT covered”.

The homomorphism K_0(D_{Z, perf}(𝒪_X)) → K_0(Coh_Z(X)). Let X be a Noetherian regular scheme and Z ⊂ X a closed subscheme. Taking the alternating sum of the cohomology sheaves of a perfect complex supported on Z defines a homomorphism from the K-group of D_{Z, perf}(𝒪_X) to the Grothendieck group of coherent 𝒪_X-modules supported on Z.

def supportedPerfectEulerHom :
    Pretriangulated.K0 (supportedPerfectDerivedCategory i) →+ KZero (SupportedCoherentModules i)

AlgebraicGeometry.supportedPerfectEulerHom_cls, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/PerfectToSupportedCoherent.lean, line 174. The attribute's comment: “the defining property of the homomorphism, in the alternating-sum form”.

The homomorphism K_0(D_{Z, perf}(𝒪_X)) → K_0(Coh_Z(X)) sends the class of a perfect complex E supported on Z to the alternating sum ∑_n (-1)^n [H^n(E)] of the classes of its cohomology sheaves.

theorem supportedPerfectEulerHom_cls (E : supportedPerfectDerivedCategory i) :
    supportedPerfectEulerHom i hX (Pretriangulated.K0.cls E) =
      eulerClass (supportedPerfectDerivedCategory i) (SupportedCoherentModules i)
        (supportedPerfectHomology i hX) E

AlgebraicGeometry.SupportedCoherentModules, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedCoherent.lean, line 67. The attribute's comment: “supported_coherent”.

The full subcategory of coherent sheaves supported on Z.

abbrev SupportedCoherentModules {X Z : Scheme.{u}}
    (i : Z ⟶ X) [IsClosedImmersion i]

AlgebraicGeometry.supportedCoherentIsSerreClass, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedCoherent.lean, line 98. The attribute's comment: “supported_coherent”.

Coherent sheaves supported on a closed subscheme form a Serre subcategory.

instance supportedCoherentIsSerreClass {X Z : Scheme.{u}}
    [IsLocallyNoetherian X] (i : Z ⟶ X) [IsClosedImmersion i] :
    (supportedCoherentProperty i).IsSerreClass

AlgebraicGeometry.supportedPerfectEulerHom', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedCoherentPerfectKGroup.lean, line 346. The attribute's comment: “the homomorphism K_0(D_{Z, perf}(O_X)) → K_0(Coh_Z(X)), with Coh_Z(X) spelled as a weak Serre subcategory of all O_X-modules. As for the nested spelling: the value on a class is the alternating sum ∑_n (-1)^n [H^n(E)] rather than the source's [⊕_n H^{2n}(E)] - [⊕_n H^{2n+1}(E)], the same element of K_0 but the identification of the two expressions is NOT proved; and X is Noetherian regular, the hypotheses of Stacks 0FER, rather than locally Noetherian. The identification K_0(Coh_Z(X)) = K'_0(Z) is Stacks 0FDT and is NOT covered”.

The homomorphism K_0(D_{Z, perf}(𝒪_X)) → K_0(Coh_Z(X)) of [Stacks, Tag 0FEP], in the unnested spelling of Coh_Z(X): the alternating sum of the classes of the cohomology sheaves of a perfect complex supported on Z.

def supportedPerfectEulerHom' :
    Pretriangulated.K0 (supportedPerfectDerivedCategory i) →+
      KZero (coherentSupportedProperty i).FullSubcategory

AlgebraicGeometry.supportedPerfectEulerHom'_cls, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedCoherentPerfectKGroup.lean, line 355. The attribute's comment: “the defining property of the homomorphism, in the alternating-sum form”.

[Stacks, Tag 0FEP]. The homomorphism K_0(D_{Z, perf}(𝒪_X)) → K_0(Coh_Z(X)) sends the class of a perfect complex supported on Z to the alternating sum of the classes of its cohomology sheaves.

theorem supportedPerfectEulerHom'_cls (E : supportedPerfectDerivedCategory i) :
    supportedPerfectEulerHom' i hX (Pretriangulated.K0.cls E) =
      eulerClass (supportedPerfectDerivedCategory i)
        (coherentSupportedProperty i).FullSubcategory (supportedPerfectHomology' i hX) E

AlgebraicGeometry.supportedPerfectCohomologyHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedPerfectCohomologyHom.lean, line 427. The attribute's comment: “the homomorphism K_0(D_{Z, perf}(O_X)) → K_0(Coh_Z(X)) for X locally Noetherian and Z ⊂ X a closed subscheme; its defining property is supportedPerfectCohomologyHom_cls”.

The homomorphism K_0(D_{Z, perf}(𝒪_X)) → K_0(Coh_Z(X)) of [Stacks, Tag 0FEP]. Let X be a locally Noetherian scheme and Z ⊂ X a closed subscheme. The rule E ↦ [⊕_{i ∈ ℤ} H^{2i}(E)] - [⊕_{i ∈ ℤ} H^{2i + 1}(E)] is additive on distinguished triangles of D_{Z, perf}(𝒪_X), hence defines a homomorphism of groups; its value on the class of E is supportedPerfectCohomologyHom_cls.

def supportedPerfectCohomologyHom :
    Pretriangulated.K0 (supportedPerfectDerivedCategory.{u, d} i) →+
      KZero (SupportedCoherentModules i)

AlgebraicGeometry.supportedPerfectCohomologyHom_cls, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedPerfectCohomologyHom.lean, line 445. The attribute's comment: “the defining property: [E] ↦ [⊕_{i ∈ ℤ} H^{2i}(E)] - [⊕_{i ∈ ℤ} H^{2i+1}(E)], the direct sums taken in Mod(O_X)”.

The defining property of the homomorphism of [Stacks, Tag 0FEP]. The class of a perfect complex E with cohomology sheaves supported on Z is sent to [⊕_{i ∈ ℤ} H^{2i}(E)] - [⊕_{i ∈ ℤ} H^{2i + 1}(E)], the direct sums being taken in the category of 𝒪_X-modules (evenHomologySupported_obj_obj, oddHomologySupported_obj_obj).

theorem supportedPerfectCohomologyHom_cls (E : supportedPerfectDerivedCategory.{u, d} i) :
    supportedPerfectCohomologyHom i (Pretriangulated.K0.cls E) =
      KZero.mk _ (evenHomologySupported i E) - KZero.mk _ (oddHomologySupported i E)

AlgebraicGeometry.supportedPerfectCohomologyHomToCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedPerfectCohomologyHom.lean, line 454. The attribute's comment: “the same homomorphism with target K'_0(Z) = K_0(Coh(Z)), through the identification K_0(Coh_Z(X)) = K'_0(Z) of Stacks 0FDT”.

The homomorphism of [Stacks, Tag 0FEP] with target K'_0(Z) = K_0(Coh(𝒪_Z)), through the identification K_0(Coh(𝒪_Z)) ≅ K_0(Coh_Z(X)) of [Stacks, Tag 0FDT].

def supportedPerfectCohomologyHomToCoherent :
    Pretriangulated.K0 (supportedPerfectDerivedCategory.{u, d} i) →+
      KZero (Stacks.SheafOfModules.CoherentModules Z.ringCatSheaf)

AlgebraicGeometry.supportedPerfect_isStrictlyFull_isTriangulated_isSaturated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedPerfectCohomologyHom.lean, line 504. The attribute's comment: “D_{Z, perf}(O_X) is a strictly full, saturated, triangulated subcategory of D(O_X): closed under isomorphisms, triangulated, stable under retracts, hence saturated”. References: SGA 6 I (5.8.4), “5.8.4 a), special case”.

D_{Z, perf}(𝒪_X) is a strictly full, saturated, triangulated subcategory of D(𝒪_X). The perfect complexes of 𝒪_X-modules whose cohomology sheaves are set-theoretically supported on Z form a property of objects which is closed under isomorphisms, triangulated, and stable under retracts, hence saturated (closed under direct summands).

theorem supportedPerfect_isStrictlyFull_isTriangulated_isSaturated :
    let P : ObjectProperty (DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)) :=
      fun K => RingedSpace.IsPerfect K ∧
        ∀ n : ℤ, SheafOfModules.supp
          ((DerivedCategory.homologyFunctor (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)
            n).obj K) ⊆ Set.range i.base
    P.IsClosedUnderIsomorphisms ∧ P.IsTriangulated ∧ P.IsStableUnderRetracts ∧
      P.IsSaturated

Stacks.AlgebraicGeometry.PerfectCohomology.isCoherent_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentComplex/LocallyFiniteCohomology.lean, line 65. The attribute's comment: “locally_finite_cohomology”.

Every cohomology module of a perfect object on a locally Noetherian scheme is coherent.

theorem isCoherent_homology (X : Scheme.{u}) [IsLocallyNoetherian X]
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)]
    (K : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace))
    (hK : RingedSpace.IsPerfect (X := X.toRingedSpace) K) (n : ℤ) :
    _root_.SheafOfModules.IsCoherent
      ((DerivedCategory.homologyFunctor
        (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace) n).obj K)

Stacks.AlgebraicGeometry.PerfectCohomology.locally_finite_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/PseudoCoherentComplex/LocallyFiniteCohomology.lean, line 80. The attribute's comment: “locally_finite_cohomology”.

Near every point only finitely many cohomology modules of a perfect object have nonempty support.

theorem locally_finite_homology (X : Scheme.{u})
    [HasDerivedCategory.{d} (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)]
    (K : DerivedCategory (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace))
    (hK : RingedSpace.IsPerfect (X := X.toRingedSpace) K) (x : X) :
    ∃ U : X.Opens, x ∈ U ∧
      {n : ℤ | ∃ y : X, y ∈ U ∧ y ∈ SheafOfModules.supp
        ((DerivedCategory.homologyFunctor
          (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace) n).obj K)}.Finite

Declarations registered for the tag:

• AlgebraicGeometry.supportedPerfectDerivedCategory, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedPerfectComplexes.lean, line 30 (StacksFrontier): “supported_perfect_complexes”.

Tag 0FEQ, a remark

Tag 0FEQ in the Stacks Project.

AlgebraicGeometry.coherentToSupportedPerfectHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/CoherentToSupportedPerfect.lean, line 259.

Stacks Project, Tag 0FEQ. Let i : Z ⟶ X be a closed immersion of schemes with X regular. There is a canonical homomorphism K₀(Coh(𝒪_Z)) → K₀(D_{Z, perf}(𝒪_X)) taking the class of a coherent 𝒪_Z-module ℱ to the class of its direct image placed in degree zero.

The source is the Grothendieck group of the abelian category of coherent 𝒪_Z-modules and the target is the K-group of the triangulated category of perfect complexes on X supported on the closed subset underlying Z. The map is well defined because the direct image of a short exact sequence of coherent modules is short exact, hence gives a distinguished triangle of the three degree-zero complexes.

def coherentToSupportedPerfectHom :
    KZero (Stacks.SheafOfModules.CoherentModules Z.ringCatSheaf) →+
      Pretriangulated.K0 (supportedPerfectDerivedCategory i)

AlgebraicGeometry.coherentToSupportedPerfectHom_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/CoherentToSupportedPerfect.lean, line 269.

Stacks Project, Tag 0FEQ. The canonical homomorphism K₀(Coh(𝒪_Z)) → K₀(D_{Z, perf}(𝒪_X)) takes the class of a coherent 𝒪_Z-module ℱ to the class of the perfect complex (i_*ℱ)[0].

theorem coherentToSupportedPerfectHom_mk
    (F : Stacks.SheafOfModules.CoherentModules Z.ringCatSheaf) :
    coherentToSupportedPerfectHom i hX (KZero.mk _ F) =
      Pretriangulated.K0.cls (singlePushforwardSupportedPerfect i hX F)

AlgebraicGeometry.coherentToSupportedPerfectHomGeneral, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/CoherentToSupportedPerfectGeneral.lean, line 137.

Stacks Project, Tag 0FEQ. Let i : Z ⟶ X be a closed immersion of schemes with X regular. There is a canonical homomorphism K₀(Coh(𝒪_Z)) → K₀(D_{Z, perf}(𝒪_X)) taking the class of a coherent 𝒪_Z-module ℱ to the class of its direct image placed in degree zero.

The source is the Grothendieck group of the abelian category of coherent 𝒪_Z-modules and the target is the K-group of the triangulated category of perfect complexes on X supported on the closed subset underlying Z. The map is well defined because the direct image of a short exact sequence of coherent modules is short exact, hence gives a distinguished triangle of the three degree-zero complexes.

def coherentToSupportedPerfectHomGeneral
    [HasDerivedCategory.{w} (OXMod.{u, u} X.toRingedSpace)] :
    KZero (Stacks.SheafOfModules.CoherentModules Z.ringCatSheaf) →+
      Pretriangulated.K0 (supportedPerfectDerivedCategory i)

AlgebraicGeometry.coherentToSupportedPerfectHomGeneral_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/CoherentToSupportedPerfectGeneral.lean, line 148.

Stacks Project, Tag 0FEQ. The canonical homomorphism K₀(Coh(𝒪_Z)) → K₀(D_{Z, perf}(𝒪_X)) takes the class of a coherent 𝒪_Z-module ℱ to the class of the perfect complex (i_*ℱ)[0].

theorem coherentToSupportedPerfectHomGeneral_mk
    [HasDerivedCategory.{w} (OXMod.{u, u} X.toRingedSpace)]
    (F : Stacks.SheafOfModules.CoherentModules Z.ringCatSheaf) :
    coherentToSupportedPerfectHomGeneral i hX (KZero.mk _ F) =
      Pretriangulated.K0.cls (singlePushforwardSupportedPerfectGeneral i hX F)

Tag 0FER, a lemma

Tag 0FER in the Stacks Project.

AlgebraicGeometry.coherentToSupportedPerfectHom_mutuallyInverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/CoherentSupportedPerfectKGroupIso.lean, line 239.

Stacks Project, Tag 0FER. Let X be a Noetherian regular scheme and i : Z ⟶ X a closed immersion. The homomorphism K'_0(Z) = K_0(Coh(𝒪_Z)) → K_0(D_{Z, perf}(𝒪_X)), [ℱ] ↦ [(i_*ℱ)[0]], of [Stacks, Tag 0FEQ] and the homomorphism K_0(D_{Z, perf}(𝒪_X)) → K'_0(Z), [E] ↦ [⊕_n H^{2n}(E)] - [⊕_n H^{2n+1}(E)], of [Stacks, Tag 0FEP] are mutually inverse.

theorem coherentToSupportedPerfectHom_mutuallyInverse :
    (supportedPerfectCohomologyHomToCoherent i).comp (coherentToSupportedPerfectHom i hX) =
        AddMonoidHom.id _ ∧
      (coherentToSupportedPerfectHom i hX).comp (supportedPerfectCohomologyHomToCoherent i) =
        AddMonoidHom.id _

AlgebraicGeometry.coherentKZeroEquivSupportedPerfectKZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/CoherentSupportedPerfectKGroupIso.lean, line 255. The attribute's comment: “the resulting identification K'_0(Z) = K_0(D_{Z, perf}(O_X))”.

Stacks Project, Tag 0FER, as an isomorphism: K'_0(Z) ≃+ K_0(D_{Z, perf}(𝒪_X)) for a closed subscheme Z of a Noetherian regular scheme X, given by the mutually inverse homomorphisms of [Stacks, Tag 0FEQ] and [Stacks, Tag 0FEP].

def coherentKZeroEquivSupportedPerfectKZero :
    KZero (Stacks.SheafOfModules.CoherentModules Z.ringCatSheaf) ≃+
      Pretriangulated.K0 (supportedPerfectDerivedCategory i)

AlgebraicGeometry.supportedPerfectEulerHom_comp_coherentToSupportedPerfectHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/PerfectToSupportedCoherent.lean, line 210. The attribute's comment: “the round trip K_0(Coh(Z)) → K_0(D_{Z, perf}(O_X)) → K_0(Coh_Z(X)) is the comparison homomorphism of Stacks 0FDT, which is step (1) of the source's proof ('the composite is the identity'), stated without the 0FDT identification because that identification is not available. What is NOT covered: step (2), surjectivity of K_0(Coh(Z)) → K_0(D_{Z, perf}(O_X)), which the source gets from the truncation triangles together with the finite filtration of a coherent module supported on Z by O_Z-modules; and therefore NOT the conclusion that the two maps are mutually inverse”.

Let X be a Noetherian regular scheme and Z ⊂ X a closed subscheme. The composite of coherentToSupportedPerfectHom : K_0(Coh(𝒪_Z)) → K_0(D_{Z, perf}(𝒪_X)) with supportedPerfectEulerHom : K_0(D_{Z, perf}(𝒪_X)) → K_0(Coh_Z(X)) is the comparison homomorphism coherentToSupportedCoherentKZeroHom : K_0(Coh(𝒪_Z)) → K_0(Coh_Z(X)) of direct image.

theorem supportedPerfectEulerHom_comp_coherentToSupportedPerfectHom :
    (supportedPerfectEulerHom i hX).comp (coherentToSupportedPerfectHom i hX) =
      coherentToSupportedCoherentKZeroHom i

AlgebraicGeometry.supportedPerfectEulerHom'_comp_supportedCoherentToPerfectHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedCoherentPerfectKGroup.lean, line 383. The attribute's comment: “the identity K_0(Coh_Z(X)) → K_0(D_{Z, perf}(O_X)) → K_0(Coh_Z(X)); the identification K_0(Coh_Z(X)) = K'_0(Z) of Stacks 0FDT, under which this is the source's statement about K_0(Coh(Z)), is NOT covered”.

The first of the two inverse identities of [Stacks, Tag 0FER]. Taking the alternating sum of the cohomology sheaves of a coherent module supported on Z, placed in degree zero, returns the class of that module: the only nonvanishing cohomology sheaf is the module itself, in degree zero.

theorem supportedPerfectEulerHom'_comp_supportedCoherentToPerfectHom :
    (supportedPerfectEulerHom' i hX).comp (supportedCoherentToPerfectHom i hX) =
      AddMonoidHom.id (KZero (coherentSupportedProperty i).FullSubcategory)

AlgebraicGeometry.supportedCoherentToPerfectHom_comp_supportedPerfectEulerHom', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedCoherentPerfectKGroup.lean, line 425. The attribute's comment: “the identity K_0(D_{Z, perf}(O_X)) → K_0(Coh_Z(X)) → K_0(D_{Z, perf}(O_X)); with supportedPerfectEulerHom'_comp_supportedCoherentToPerfectHom this is the source's 'mutually inverse', EXCEPT that the source's left hand side is K'_0(Z) = K_0(Coh(Z)) and here it is K_0(Coh_Z(X)); the identification of the two is Stacks 0FDT and is NOT covered”.

The two homomorphisms of [Stacks, Tag 0FEP] and [Stacks, Tag 0FEQ] are mutually inverse, so K_0(Coh_Z(X)) = K_0(D_{Z, perf}(𝒪_X)): the alternating sum of cohomology sheaves and the placement of a coherent module supported on Z in degree zero compose to the identity in this direction, and supportedPerfectEulerHom'_comp_supportedCoherentToPerfectHom is the other direction.

theorem supportedCoherentToPerfectHom_comp_supportedPerfectEulerHom' :
    (supportedCoherentToPerfectHom i hX).comp (supportedPerfectEulerHom' i hX) =
      AddMonoidHom.id (Pretriangulated.K0 (supportedPerfectDerivedCategory i))

Tag 0FES, a remark

Tag 0FES in the Stacks Project.

Stacks.Chow.localizedChernClassKMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedChernClassKMap.lean, line 232.

Stacks 0FES: the localized Chern class map c(Z ⟶ X, -) : K₀(D_{Z,perf}(𝒪_X)) ⟶ A⁰(X) × ∏_{i ≥ 1} Aⁱ(Z ⟶ X), for X locally of finite type over S with quasi-compact irreducible components (for instance X quasi-compact) and a closed immersion i : Z ⟶ X: the homomorphism from K₀(D_{Z,perf}(𝒪_X)), written multiplicatively, to the ring A⁽¹⁾(Z ⟶ X) with the product of Remark 0FA0, sending [E] to c(Z ⟶ X, E) = 1 + c₁(Z ⟶ X, E) + c₂(Z ⟶ X, E) + ⋯ (Stacks.Chow.localizedChernClassKMap_cls), extended multiplicatively (Stacks.Chow.localizedChernClassKMap_add). It is well defined by Lemma 0FBD (Stacks.Chow.supportedTotalLocalizedChern_triangle).

def localizedChernClassKMap :
    Multiplicative (K0 (supportedPerfectDerivedCategory i)) →*
      localizedBivariantGrading C (gysinSystemOfInvertible C) (i ≫ a) a i rfl 1

Stacks.Chow.localizedChernClassKMap_cls, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedChernClassKMap.lean, line 240. The attribute's comment: “the value c(Z → X, E) = 1 + c_1(Z → X, E) + ⋯ on a generator [E]”.

Stacks 0FES, the value on a generator: c(Z ⟶ X, [E]) = c(Z ⟶ X, E).

theorem localizedChernClassKMap_cls (E : supportedPerfectDerivedCategory i) :
    localizedChernClassKMap C a hX (Multiplicative.ofAdd (K0.cls E)) =
      supportedTotalLocalizedChern C a hX E

Stacks.Chow.localizedChernClassKMap_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedChernClassKMap.lean, line 248. The attribute's comment: “the map is extended multiplicatively: c(Z → X, α + β) = c(Z → X, α) c(Z → X, β)”.

Stacks 0FES, multiplicativity: c(Z ⟶ X, α + β) = c(Z ⟶ X, α) c(Z ⟶ X, β) in A⁽¹⁾(Z ⟶ X).

theorem localizedChernClassKMap_add (α β : K0 (supportedPerfectDerivedCategory i)) :
    localizedChernClassKMap C a hX (Multiplicative.ofAdd (α + β)) =
      localizedChernClassKMap C a hX (Multiplicative.ofAdd α) *
        localizedChernClassKMap C a hX (Multiplicative.ofAdd β)

Tag 0FET, a remark

Tag 0FET in the Stacks Project.

Stacks.Chow.localizedChernCharKMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedChernCharacterKMap.lean, line 227.

The localized Chern character map of Stacks 0FET ch(Z ⟶ X, -) : K₀(D_{Z,perf}(𝒪_X)) ⟶ ∏_{p ≥ 0} A^p(Z ⟶ X) ⊗ 𝐐, for X with quasi-compact irreducible components: [E] ↦ ch(Z ⟶ X, E), extended additively. It is well defined because the localized Chern character is additive along distinguished triangles (Lemma 0FBE, Stacks.Chow.supportedLocalizedChernChar_triangle).

def localizedChernCharKMap :
    K0 (supportedPerfectDerivedCategory i) →+
      ∀ p : ℕ, TensorProduct ℤ ℚ (BivariantClass C (gysinSystemOfInvertible C) (i ≫ a) a i rfl
        (p : ℤ))

Stacks.Chow.localizedChernCharKMap_cls, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedChernCharacterKMap.lean, line 236. The attribute's comment: “localized_chern_character_k_map: the generator [E] is sent to ch(Z → X, E), and the map is the additive extension”.

The localized Chern character map on a class: [E] ↦ ch(Z ⟶ X, E).

theorem localizedChernCharKMap_cls (E : supportedPerfectDerivedCategory i) :
    localizedChernCharKMap C a hX (K0.cls E) = supportedLocalizedChernChar C a hX E

Stacks.Chow.exists_localizedChernCharKMap_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedChernCharacterKMap.lean, line 329. The attribute's comment: “localized_chern_character_k_finite_support: for X quasi-compact the image lies in A^*(Z → X) ⊗ Q, every value having finitely many nonzero components”.

If X is quasi-compact, the localized Chern character map takes values in A^*(Z ⟶ X) ⊗ 𝐐: every value has only finitely many nonzero components.

theorem exists_localizedChernCharKMap_eq_zero (x : K0 (supportedPerfectDerivedCategory i)) :
    ∃ N, ∀ p ≥ N, localizedChernCharKMap C a hX x p = 0

Stacks.Chow.localizedChernCharKMap_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/LocalizedChern/LocalizedChernCharacterRing.lean, line 249. The attribute's comment: “localized_chern_character_k_multiplicative: ch(Z → X, αβ) = ch(Z → X, α) ch(Z → X, β), the product on K_0(D_{Z,perf}(O_X)) being derived tensor product (0FDN) and that on ∏ A^p(Z → X) ⊗ Q the Cauchy product of the products res(c) ∘ c' of 0FA0”.

The localized Chern character map is multiplicative. For X with quasi-compact irreducible components and α, β ∈ K₀(D_{Z,perf}(𝒪_X)), multiplied by the derived tensor product (Remark 0FDN),

ch(Z ⟶ X, α β) = ch(Z ⟶ X, α) ch(Z ⟶ X, β)

in ∏_{p ≥ 0} A^p(Z ⟶ X) ⊗ 𝐐 (Stacks.Chow.rationalSupportedProductMul).

theorem localizedChernCharKMap_mul (x y : K0 (supportedPerfectDerivedCategory i)) :
    localizedChernCharKMap C a hX (x * y) =
      rationalSupportedProductMul C a i (localizedChernCharKMap C a hX x)
        (localizedChernCharKMap C a hX y)

Tag 0FEU, a remark

Tag 0FEU in the Stacks Project.

AlgebraicGeometry.supportedPerfectDerivedCategory_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedPerfectWholeScheme.lean, line 100. The attribute's comment: “supported_perfect”.

Stacks 0FEU. Perfect objects of the derived category supported on the whole scheme are exactly the perfect objects: D_{X, perf}(O_X) = D_perf(O_X).

theorem supportedPerfectDerivedCategory_id (X : Scheme.{u}) :
    supportedPerfectDerivedCategory (𝟙 X) = PerfectDerivedCategory X

AlgebraicGeometry.supportedPerfectKZeroEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedPerfectWholeScheme.lean, line 111. The attribute's comment: “k_group”.

Stacks 0FEU. The K-group of perfect complexes supported on the whole scheme is the Grothendieck group K_0(X) = K_0(D_perf(O_X)) of the scheme.

noncomputable def supportedPerfectKZeroEquiv (X : Scheme.{u}) :
    Pretriangulated.K0 (supportedPerfectDerivedCategory (𝟙 X)) ≃+
      Pretriangulated.K0 (PerfectDerivedCategory X)

AlgebraicGeometry.supportedPerfectKZeroEquiv_cls, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/SupportedPerfectWholeScheme.lean, line 163. The attribute's comment: “k_group”.

Stacks 0FEU. The identification of K-groups takes the class of a perfect complex supported on the whole scheme to the class of the same complex in K_0(D_perf(O_X)).

theorem supportedPerfectKZeroEquiv_cls (X : Scheme.{u})
    (K : supportedPerfectDerivedCategory (𝟙 X)) :
    supportedPerfectKZeroEquiv X (Pretriangulated.K0.cls K) =
      Pretriangulated.K0.cls (⟨K.obj, K.property.1⟩ : PerfectDerivedCategory X)

Stacks.Chow.perfectKZeroChernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/WholeSchemeChernMaps.lean, line 417. The attribute's comment: “the map c : K_0(X) -> prod A^i(X), [E] |-> c(E) extended multiplicatively, built directly from Definition 0F9E and Lemma 0F9F as the remark allows; X has quasi-compact irreducible components”.

Stacks 0FEU, the Chern class map c : K_0(X) ⟶ ∏_{i ≥ 0} A^i(X), sending [E] to the total Chern class c(E) of Stacks 0F9E and sums to products.

def perfectKZeroChernClass (α : K0 (PerfectDerivedCategory X)) : TotalChowClass C sX

Stacks.Chow.perfectKZeroChernCharacter, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/WholeSchemeChernMaps.lean, line 440. The attribute's comment: “the map ch : K_0(X) -> prod A^i(X) tensor Q, [E] |-> ch(E) extended additively, built directly from Definition 0F9E and Lemma 0F9F as the remark allows”.

Stacks 0FEU, the Chern character ch : K_0(X) ⟶ ∏_{i ≥ 0} A^i(X) ⊗ 𝐐, additive and sending [E] to ch(E); well defined by Stacks 0F9F.

def perfectKZeroChernCharacter :
    K0 (PerfectDerivedCategory X) →+ fullRationalChowCohomology C (gysinSystemOfInvertible C) sX

Stacks.Chow.perfectKZero_chernMaps_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/AdamsOperator/WholeSchemeChernMaps.lean, line 488. The attribute's comment: “the whole remark: D_{X,perf} = D_perf, K_0(D_{X,perf}) = K_0(X), the maps c and ch on K_0(X), and the commutativity of both triangles with K_0(Vect(X)) -> K_0(X)”.

Stacks 0FEU. Let X be locally of finite type over the base of chapter 42, with quasi-compact irreducible components (e.g. X quasi-compact). Then

1. D_{X, perf}(𝒪_X) = D_perf(𝒪_X), and K_0(D_{X, perf}(𝒪_X)) ≅ K_0(D_perf(𝒪_X)) = K_0(X) compatibly with classes of objects;
2. the Chern classes give c : K_0(X) ⟶ ∏ A^i(X), [E] ↦ c(E), with c(α + β) = c(α) c(β);
3. the Chern character gives the additive ch : K_0(X) ⟶ ∏ A^i(X) ⊗ 𝐐, [E] ↦ ch(E);
4. c composed with K_0(Vect(X)) ⟶ K_0(X) is the map c of Stacks 0FEL; and
5. ch composed with K_0(Vect(X)) ⟶ K_0(X) is the map ch of Stacks 0FEM.

theorem perfectKZero_chernMaps_spec :
    AlgebraicGeometry.supportedPerfectDerivedCategory (𝟙 X) = PerfectDerivedCategory X ∧
    (∀ K : AlgebraicGeometry.supportedPerfectDerivedCategory (𝟙 X),
      AlgebraicGeometry.supportedPerfectKZeroEquiv X (K0.cls K) =
        K0.cls (⟨K.obj, K.property.1⟩ : PerfectDerivedCategory X)) ∧
    (∀ (E : PerfectDerivedCategory X) (hE : HasDefinedChernClasses E.obj),
      perfectKZeroChernClass C sX hqc (K0.cls E) = perfectChernClass C sX hE) ∧
    (∀ α β : K0 (PerfectDerivedCategory X), perfectKZeroChernClass C sX hqc (α + β) =
      perfectKZeroChernClass C sX hqc α * perfectKZeroChernClass C sX hqc β) ∧
    (∀ (E : PerfectDerivedCategory X) (hE : HasDefinedChernClasses E.obj),
      perfectKZeroChernCharacter C sX hqc (K0.cls E) = perfectChernCharacter C sX hE) ∧
    (∀ α : VectorBundleKZero X, perfectKZeroChernClass C sX hqc (vectorBundleKZeroToPerfect X α) =
      totalChernKGroupMap C sX α) ∧
    (perfectKZeroChernCharacter C sX hqc).comp (vectorBundleKZeroToPerfect X) =
      (chernCharacterRingHom C sX).toAddMonoidHom

Sources

• Section 42.56, Tag 0FEI
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.VectorBundleKZero.exists_secondAdamsOperator · AlgebraicGeometry.VectorBundleKZero.exists_secondAdamsOperator_pullbackRingHom · Stacks.SecondAdamsPerfect.swapSquare_comp_swapSquare · Stacks.SecondAdamsPerfect.swapSquareAction · Stacks.SecondAdamsPerfect.invariantProjector_add_antiInvariantProjector · Stacks.SecondAdamsPerfect.cls_tensorObj_eq_add · Stacks.SecondAdamsPerfect.cls_sub_cls_eq · Stacks.SecondAdamsPerfect.derivedSwapSquare_comp_self

Section42.57 Chow groups and K-groups revisited#

Section 42.57 of the Stacks Project, Tag 0FEV. 1 tag here is carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FEW, a proposition

Tag 0FEW in the Stacks Project.

Stacks.Chow.chowToGradedCoherentKZero_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChowHomologyCoherentKZero.lean, line 109. The attribute's comment: “injectivity of the canonical map CH_k(X) ⊗ 𝐐 ⟶ gr_k K'₀(X) ⊗ 𝐐; the composition K'₀(X) → K₀(D_{X, perf}(𝒪_Y)) → A^*(X ⟶ Y) ⊗ 𝐐 → CH_*(X) ⊗ 𝐐, the canonical maps of Lemma 42.23.4, and the two conditions (1) and (2) that the proof establishes for the composition and reduces the proposition to, are hypotheses: none of the three legs of the composition is constructed in this repository, A^* carrying no multiplication”.

The canonical map CH_k(X) ⊗ 𝐐 ⟶ gr_k K'₀(X) ⊗ 𝐐 is injective, for a homomorphism ch : K'₀(X) → CH_*(X) ⊗ 𝐐 such that the class of a coherent module whose support has delta-dimension at most j has vanishing components in degrees above j (hch_triangular), and the degree k component of a lift to F_k K'₀(X) of cls k α is 1 ⊗ α (hch_diagonal).

theorem chowToGradedCoherentKZero_injective
    (ch : CoherentKZero X →+ DirectSum ℤ fun j => TensorProduct ℤ ℚ (chowGroup C f j))
    (hch_triangular : ∀ (j j' : ℤ) (F : CoherentModulesDimLE C f j), j < j' →
      ch (KZero.mk _ F.obj) j' = 0)
    (cls : ∀ j : ℤ, chowGroup C f j →+ gradedCoherentKZero C f j) (k : ℤ)
    (hch_diagonal : ∀ (α : chowGroup C f k) (x : coherentKZeroFiltration C f k),
      toGradedCoherentKZero C f k x = cls k α →
        ch (x : CoherentKZero X) k = (1 : ℚ) ⊗ₜ[ℤ] α) :
    Function.Injective
      (TensorProduct.map (LinearMap.id : ℚ →ₗ[ℤ] ℚ) (cls k).toIntLinearMap)

Stacks.Chow.rationalCoherentKZeroToChowHomology_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChowHomologyCoherentKZero.lean, line 156. The attribute's comment: “surjectivity of the composition K'₀(X) ⊗ 𝐐 → CH_*(X) ⊗ 𝐐; as for the injectivity statement in this file the composition, the canonical maps of Lemma 42.23.4 and the two conditions (1) and (2) that the proof establishes for the composition are hypotheses, none of the three legs of the composition being constructed in this repository; the injectivity of the composition is not proved, needing the surjectivity of the canonical maps and hence the unformalized half of Tag 02S9”.

A homomorphism ch : K'₀(X) → CH_*(X) ⊗ 𝐐 satisfying the conditions hch_triangular and hch_diagonal of Stacks.Chow.chowToGradedCoherentKZero_injective (the latter in every degree) becomes surjective after tensoring the source with 𝐐, provided δ_{X/S} is bounded below.

theorem rationalCoherentKZeroToChowHomology_surjective
    (ch : CoherentKZero X →+ DirectSum ℤ fun j => TensorProduct ℤ ℚ (chowGroup C f j))
    (hch_triangular : ∀ (j j' : ℤ) (F : CoherentModulesDimLE C f j), j < j' →
      ch (KZero.mk _ F.obj) j' = 0)
    (cls : ∀ j : ℤ, chowGroup C f j →+ gradedCoherentKZero C f j)
    (hch_diagonal : ∀ (k : ℤ) (α : chowGroup C f k) (x : coherentKZeroFiltration C f k),
      toGradedCoherentKZero C f k x = cls k α →
        ch (x : CoherentKZero X) k = (1 : ℚ) ⊗ₜ[ℤ] α)
    (lo : ℤ) (hlo : ∀ x : X, lo ≤ relativeDimension C.dimensionFunction f x) :
    Function.Surjective (ch.toIntLinearMap.liftBaseChange ℚ)

Stacks.Chow.bijective_liftBaseChange_coherentChowCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/ChowCoherentIsomorphism.lean, line 213. The attribute's comment: “the whole proposition: the map K'_0(X) ⊗ Q → CH_*(X) ⊗ Q, [F] ↦ ch(X → Y, F[0]) ∩ [Y], is bijective, and CH_k(X) ⊗ Q → gr_k K'_0(X) ⊗ Q is bijective for every k, for a closed immersion X → Y of schemes locally of finite type over S with Y regular and quasi-compact, (S, δ) as in Situation 02QL”.

Stacks 0FEW. Let (S, δ) be as in Situation 02QL and let i : X ⟶ Y be a closed immersion of schemes locally of finite type over S, with Y regular and quasi-compact. Then the composition K'₀(X) ⟶ K₀(D_{X, perf}(𝒪_Y)) ⟶ A^*(X ⟶ Y) ⊗ 𝐐 ⟶ CH_*(X) ⊗ 𝐐, [ℱ] ↦ ch(X ⟶ Y, ℱ[0]) ∩ [Y], induces an isomorphism K'₀(X) ⊗ 𝐐 ≅ CH_*(X) ⊗ 𝐐; moreover the canonical map CH_k(X) ⊗ 𝐐 ⟶ gr_k K'₀(X) ⊗ 𝐐 is an isomorphism for every k.

Surjectivity and the "moreover" are conditions (1) and (2) of the source's proof (Stacks.Chow.surjective_liftBaseChange_coherentChowCharacter, Stacks.Chow.bijective_rTensor_chowToGradedCoherentKZero_of_isClosedImmersion); injectivity is Stacks.Chow.injective_liftBaseChange_coherentChowCharacter.

theorem bijective_liftBaseChange_coherentChowCharacter :
    haveI := isNoetherian_of_isClosedImmersion_of_compactSpace C a i
    Function.Bijective ((coherentChowCharacter C a i hY).toIntLinearMap.liftBaseChange ℚ) ∧
      ∀ k : ℤ, Function.Bijective (TensorProduct.map (LinearMap.id : ℚ →ₗ[ℤ] ℚ)
        (chowToGradedCoherentKZero C (i ≫ a) k).toIntLinearMap)

Sources

• Section 42.57, Tag 0FEV
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.chowToGradedCoherentKZero_injective · Stacks.Chow.rationalCoherentKZeroToChowHomology_surjective · Stacks.Chow.bijective_liftBaseChange_coherentChowCharacter

Section42.58 Rational intersection products on regular schemes#

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

Tag 0FEX, the section

Tag 0FEX in the Stacks Project.

Stacks.Chow.rationalIntersectionProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionProduct.lean, line 224. The attribute's comment: “the construction of the section: for X as in 0FEY (Noetherian, equivalently quasi-compact, given locally of finite type over S), α · β = ch(α') ∩ β with α' the unique class with ch(α') ∩ [X] = α; CH^(X) ⊗ Q is CH_(X) ⊗ Q, the internal direct sum of the codimension pieces codimensionChowSubmodule”.

The intersection product of Stacks Section 0FEX on CH_*(X) ⊗ 𝐐, for X Noetherian (equivalently quasi-compact), regular, of finite type over S, with affine diagonal and δ_{X/S} bounded: α · β = ch(α') ∩ β, where α' ∈ K_0(Vect(X)) ⊗ 𝐐 is the unique class with ch(α') ∩ [X] = α (Stacks 0FEY, Stacks.Chow.bijective_flip_rationalChernCharacterCap).

def rationalIntersectionProduct : CHQ →ₗ[ℚ] CHQ →ₗ[ℚ] CHQ

Stacks.Chow.rationalIntersectionProduct_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionProduct.lean, line 262. The attribute's comment: “the product of the section is symmetric: α · β = β · α, for X as in 0FEY”.

The product is commutative (Section 0FEX: "this is a symmetric pairing"), the operators ch(α') ∩ - pairwise commuting.

theorem rationalIntersectionProduct_comm (α β : CHQ) :
    rationalIntersectionProduct hX hb α β = rationalIntersectionProduct hX hb β α

Stacks.Chow.rationalIntersectionProduct_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionProduct.lean, line 271. The attribute's comment: “the product of the section is associative: (α · β) · γ = α · (β · γ), for X as in 0FEY”.

The product is associative (Section 0FEX): both bracketings of α · β · γ are ch(α') ∩ ch(β') ∩ ch(γ') ∩ [X], up to reordering the commuting operators.

theorem rationalIntersectionProduct_assoc (α β γ : CHQ) :
    rationalIntersectionProduct hX hb (rationalIntersectionProduct hX hb α β) γ =
      rationalIntersectionProduct hX hb α (rationalIntersectionProduct hX hb β γ)

Stacks.Chow.rationalIntersectionProduct_eq_rationalChernCharacterComponentCap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionProduct.lean, line 396. The attribute's comment: “the defining formula of the section: for α ∈ CH^i(X) ⊗ Q with ch(α') ∩ [X] = α, α · β = ch(α') ∩ β = ch_i(α') ∩ β, for X as in 0FEY”.

The product of a class of codimension i is computed by ch_i (Section 0FEX). If α = ch(α') ∩ [X] lies in CH^i(X) ⊗ 𝐐 then α · β = ch_i(α') ∩ β, the definition of the source.

theorem rationalIntersectionProduct_eq_rationalChernCharacterComponentCap
    {i : ℕ} {α : CHQ} (hα : α ∈ codimensionChowSubmodule C sX i)
    {a : ℚ ⊗[ℤ] VectorBundleKZero X}
    (ha : rationalChernCharacterCap C sX a (rationalFundamentalClass C sX) = α) (β : CHQ) :
    rationalIntersectionProduct hX hb α β = rationalChernCharacterComponentCap C sX i a β

Stacks.Chow.rationalIntersectionProduct_mem_codimensionChowSubmodule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionProduct.lean, line 424. The attribute's comment: “the product of the section is graded: CH^i(X) ⊗ Q · CH^j(X) ⊗ Q ⊆ CH^{i+j}(X) ⊗ Q, for X as in 0FEY”.

The product is graded by codimension (Section 0FEX: α · β ∈ CH^{i+j}(X) ⊗ 𝐐): CH^i(X) ⊗ 𝐐 · CH^j(X) ⊗ 𝐐 ⊆ CH^{i+j}(X) ⊗ 𝐐.

theorem rationalIntersectionProduct_mem_codimensionChowSubmodule
    {i j : ℕ} {α β : CHQ} (hα : α ∈ codimensionChowSubmodule C sX i)
    (hβ : β ∈ codimensionChowSubmodule C sX j) :
    rationalIntersectionProduct hX hb α β ∈ codimensionChowSubmodule C sX (i + j)

Stacks.Chow.existsUnique_rationalIntersectionProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionRing.lean, line 107. The attribute's comment: “the closing reformulation of the section: for X as in 0FEY, there is a unique commutative, associative intersection product on CH^(X) ⊗ Q compatible with the grading such that K_0(Vect(X)) ⊗ Q → CH^(X) ⊗ Q is a ring isomorphism, and it is the product of the section”.

For X as in Stacks 0FEY (Noetherian, equivalently quasi-compact, regular, of finite type over S, with affine diagonal and δ_{X/S} bounded), rationalIntersectionProduct is the unique bilinear product on CH^*(X) ⊗ 𝐐 = CH_*(X) ⊗ 𝐐 which is commutative, associative, graded by the codimension pieces codimensionChowSubmodule, and for which α' ↦ ch(α') ∩ [X] is multiplicative, that is, an isomorphism of rings.

theorem existsUnique_rationalIntersectionProduct :
    ∃! μ : CHQ →ₗ[ℚ] CHQ →ₗ[ℚ] CHQ,
      (∀ a b, μ (rationalChernCharacterCap C sX a (rationalFundamentalClass C sX))
          (rationalChernCharacterCap C sX b (rationalFundamentalClass C sX)) =
        rationalChernCharacterCap C sX (a * b) (rationalFundamentalClass C sX)) ∧
      (∀ α β, μ α β = μ β α) ∧ (∀ α β γ, μ (μ α β) γ = μ α (μ β γ)) ∧
      ∀ {i j : ℕ} {α β : CHQ}, α ∈ codimensionChowSubmodule C sX i →
        β ∈ codimensionChowSubmodule C sX j → μ α β ∈ codimensionChowSubmodule C sX (i + j)

Stacks.Chow.rationalChernCharacterAlgEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionRing.lean, line 193. The attribute's comment: “the closing sentence of the section: for X as in 0FEY, K_0(Vect(X)) ⊗ Q → CH^*(X) ⊗ Q, α' ↦ ch(α') ∩ [X], is an isomorphism of rings for the product of the section”.

The map of Stacks 0FEY is an isomorphism of rings: for X as in Stacks 0FEY, α' ↦ ch(α') ∩ [X] is an isomorphism of 𝐐-algebras from K_0(Vect(X)) ⊗ 𝐐 onto the rational Chow ring CH^*(X) ⊗ 𝐐 = CH_*(X) ⊗ 𝐐 with the product rationalIntersectionProduct.

def rationalChernCharacterAlgEquiv :
    ℚ ⊗[ℤ] VectorBundleKZero X ≃ₐ[ℚ] RationalIntersectionRing hX hb

Stacks.Chow.rationalSecondAdams_eq_smul_of_rationalChernCharacterCap_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/SecondAdamsChernCharacter.lean, line 318. The attribute's comment: “the eigenvalue statement of the section: for X as in 0FEY, α ∈ CH^i(X) ⊗ Q and α' ∈ K_0(Vect(X)) ⊗ Q with ch(α') ∩ [X] = α, ψ²(α') = 2^i α', where ψ² is the second Adams operation of 0FEJ extended Q-linearly (Stacks.Chow.rationalSecondAdams); proved from 0FEN (Stacks.Chow.chernCharacterVectorBundle_secondAdams) and the uniqueness in 0FEY, as in the source”.

Stacks Project, Section 0FEX: the class answering to a cycle class of codimension i is a 2^i-eigenvector of ψ². Let X be as in Stacks 0FEY (Noetherian, equivalently quasi-compact, regular, of finite type over S, with affine diagonal and δ_{X/S} bounded). If α ∈ CH^i(X) ⊗ 𝐐 and α' ∈ K_0(Vect(X)) ⊗ 𝐐 is the (unique, by Stacks 0FEY) class with ch(α') ∩ [X] = α, then ψ²(α') = 2^i α'.

theorem rationalSecondAdams_eq_smul_of_rationalChernCharacterCap_mem (hX : IsRegular X)
    (hb : ∃ lo hi : ℤ, ∀ x : X, lo ≤ relativeDimension C.dimensionFunction sX x ∧
      relativeDimension C.dimensionFunction sX x ≤ hi)
    {i : ℕ} {a : ℚ ⊗[ℤ] VectorBundleKZero X}
    (ha : rationalChernCharacterCap C sX a (rationalFundamentalClass C sX) ∈
      codimensionChowSubmodule C sX i) :
    rationalSecondAdams X a = (2 ^ i : ℚ) • a

Stacks.Chow.rationalChernCharacterVectorBundle_eq_zero_of_rationalChernCharacterCap_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/SecondAdamsChernCharacter.lean, line 367. The attribute's comment: “the vanishing statement of the section: for X as in 0FEY, α ∈ CH^i(X) ⊗ Q and α' ∈ K_0(Vect(X)) ⊗ Q with ch(α') ∩ [X] = α, ch_j(α') = 0 in A^j(X) ⊗ Q for every j ≠ i, from ψ²(α') = 2^i α' and 0FEN, as in the source”.

Stacks Project, Section 0FEX: the components of ch(α') off the codimension vanish. For X as in Stacks 0FEY, α ∈ CH^i(X) ⊗ 𝐐 and α' ∈ K_0(Vect(X)) ⊗ 𝐐 with ch(α') ∩ [X] = α, one has ch_j(α') = 0 in A^j(X) ⊗ 𝐐 for every j ≠ i.

theorem rationalChernCharacterVectorBundle_eq_zero_of_rationalChernCharacterCap_mem
    (hX : IsRegular X)
    (hb : ∃ lo hi : ℤ, ∀ x : X, lo ≤ relativeDimension C.dimensionFunction sX x ∧
      relativeDimension C.dimensionFunction sX x ≤ hi)
    {i : ℕ} {a : ℚ ⊗[ℤ] VectorBundleKZero X}
    (ha : rationalChernCharacterCap C sX a (rationalFundamentalClass C sX) ∈
      codimensionChowSubmodule C sX i) {j : ℕ} (hj : j ≠ i) :
    rationalChernCharacterVectorBundle C sX a j = 0

Stacks.Chow.rationalChernCharacterComponentCap_rationalFundamentalClass_of_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/SecondAdamsChernCharacter.lean, line 392. The attribute's comment: “the consequence the section draws from the vanishing statement: for X as in 0FEY, α ∈ CH^i(X) ⊗ Q and α' ∈ K_0(Vect(X)) ⊗ Q with ch(α') ∩ [X] = α, ch_{i'}(α') ∩ [X] = 0 for i' ≠ i and ch_i(α') ∩ [X] = α”.

Stacks Project, Section 0FEX: ch_{i'}(α') ∩ [X] = 0 for i' ≠ i and ch_i(α') ∩ [X] = α. For X as in Stacks 0FEY, α ∈ CH^i(X) ⊗ 𝐐 and α' ∈ K_0(Vect(X)) ⊗ 𝐐 with ch(α') ∩ [X] = α, the components of ch(α') other than the i-th cap [X] to zero, and the i-th one caps [X] to α.

theorem rationalChernCharacterComponentCap_rationalFundamentalClass_of_mem (hX : IsRegular X)
    (hb : ∃ lo hi : ℤ, ∀ x : X, lo ≤ relativeDimension C.dimensionFunction sX x ∧
      relativeDimension C.dimensionFunction sX x ≤ hi)
    {i : ℕ} {a : ℚ ⊗[ℤ] VectorBundleKZero X}
    (ha : rationalChernCharacterCap C sX a (rationalFundamentalClass C sX) ∈
      codimensionChowSubmodule C sX i) :
    (∀ j : ℕ, j ≠ i →
        rationalChernCharacterComponentCap C sX j a (rationalFundamentalClass C sX) = 0) ∧
      rationalChernCharacterComponentCap C sX i a (rationalFundamentalClass C sX) =
        rationalChernCharacterCap C sX a (rationalFundamentalClass C sX)

Tag 0FEY, a lemma

Tag 0FEY in the Stacks Project.

Stacks.Chow.bijective_rationalChernCharacterCapFundamentalClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RationalIntersection/RationalIntersectionProduct.lean, line 180. The attribute's comment: “the whole lemma: for X quasi-compact, regular, of finite type over S, with affine diagonal and δ_{X/S} bounded, α ↦ ch(α) ∩ [X], K_0(Vect(X)) ⊗ Q → A^(X) ⊗ Q → CH_(X) ⊗ Q, is bijective; ch is the ring map of 0FEM into ∏_p A^p(X) ⊗ Q, whose cap with [X] is a finite sum since δ_{X/S} is bounded”.

Stacks Project, Tag 0FEY. Let (S, δ) be as in Situation 42.7.1 and let X be a quasi-compact regular scheme of finite type over S with affine diagonal and δ_{X/S} bounded. Then the composition

K_0(Vect(X)) ⊗ 𝐐 ⟶ ∏_p A^p(X) ⊗ 𝐐 ⟶ CH_*(X) ⊗ 𝐐, α ↦ ch(α) ∩ [X],

of the Chern character of Remark 0FEM and the map c ↦ c ∩ [X] is bijective.

The map is Stacks.Chow.rationalChernCharacterCapFundamentalClass, the sum over p of ch_p(α) ∩ [X] (Stacks.Chow.rationalChernCharacterCapFundamentalClass_eq_sum). The proof is Stacks.Chow.bijective_rationalChernCharacterCapFundamentalClass_of_chernFormula (Proposition 0FEW for X = Y, Remark 0FEU) applied to Lemma 0FEG (Stacks.Chow.isRegularImmersionChernFormula_of_compactSpace).

theorem bijective_rationalChernCharacterCapFundamentalClass [CompactSpace X] (hX : IsRegular X)
    (hb : ∃ lo hi : ℤ, ∀ x : X, lo ≤ relativeDimension C.dimensionFunction sX x ∧
      relativeDimension C.dimensionFunction sX x ≤ hi) :
    haveI := isNoetherian_of_compactSpace sX
    Function.Bijective (rationalChernCharacterCapFundamentalClass C sX)

Sources

• Section 42.58, Tag 0FEX
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.rationalIntersectionProduct · Stacks.Chow.rationalIntersectionProduct_comm · Stacks.Chow.rationalIntersectionProduct_assoc · Stacks.Chow.rationalIntersectionProduct_eq_rationalChernCharacterComponentCap · Stacks.Chow.rationalIntersectionProduct_mem_codimensionChowSubmodule · Stacks.Chow.existsUnique_rationalIntersectionProduct · Stacks.Chow.rationalChernCharacterAlgEquiv · Stacks.Chow.rationalSecondAdams_eq_smul_of_rationalChernCharacterCap_mem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.