62 Relative Cycles

Chapter 62 of the Stacks Project, Relative Cycles, Tag 0H4B: the 13 sections of its 17 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 76 tags are carried by 152 declarations of the repository (all in StacksFrontier).

Section62.3 Cycles relative to fields#

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

Tag 0H4E, the section

Tag 0H4E in the Stacks Project.

Stacks.Chow.injective_baseChangeCyclePullback_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ChangeBaseScheme/Injective.lean, line 169. The attribute's comment: “the base change map on cycle groups along a field extension, and its injectivity”.

Stacks Project, Section 0H4E. For a scheme X locally of finite type over a field k and an arbitrary extension K/k of fields, the base-change homomorphism Z_r(X) ⟶ Z_r(X_K) on cycle groups is injective. The extension is not assumed algebraic, nor even of finite type.

theorem injective_baseChangeCyclePullback_fieldExtension (k K : Type u) [Field k] [Field K]
    [Algebra k K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k)) [LocallyOfFiniteType f]
    (r : ℤ) :
    Function.Injective (baseChangeCyclePullback (fieldExtensionBaseChangeSituation k K) f r)

Tag 0H4F, a lemma

Tag 0H4F in the Stacks Project.

Stacks.Chow.componentMultiplicity_baseChange_eq_one_or_char_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/BaseFieldExtension.lean, line 430.

The multiplicity of an irreducible component of the base change of an integral scheme locally of finite type over a field along a field extension is one or, in positive characteristic, a power of the characteristic.

theorem componentMultiplicity_baseChange_eq_one_or_char_pow
    {k K : Type u} [Field k] [Field K] [Algebra k K]
    {Z : Scheme.{u}} (f : Z ⟶ Spec (.of k)) [IsIntegral Z]
    [LocallyOfFiniteType f]
    (ξ : genericPoints
      (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme)) :
    let ZK : Scheme := pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K)))
    componentMultiplicity (𝟙 ZK) ξ = 1 ∨
      (ringChar k ≠ 0 ∧
        ∃ n : ℕ, componentMultiplicity (𝟙 ZK) ξ = (ringChar k : ℤ) ^ n)

Tag 0H4G, a lemma

Tag 0H4G in the Stacks Project.

Stacks.Chow.baseChangeCyclePullback_perfectClosure_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/PerfectClosureCycles.lean, line 309. The attribute's comment: “injectivity”.

For an algebraic scheme X over a field k, the base-change homomorphism Z_r(X) ⟶ Z_r(X_{k^perf}) to the perfect closure of k is injective.

theorem baseChangeCyclePullback_perfectClosure_injective (k : Type u) [Field k] (r : ℕ)
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k)) [LocallyOfFiniteType f]
    [QuasiCompact f] :
    Function.Injective
      (baseChangeCyclePullback (perfectClosureBaseChangeSituation k) f (r : ℤ))

Stacks.Chow.isElementPowerTorsion_cokernel_baseChangeCyclePullback_perfectClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/PerfectClosureCycles.lean, line 322. The attribute's comment: “p-power torsion cokernel”.

For an algebraic scheme X over a field k of characteristic p > 0, the cokernel of the base-change homomorphism Z_r(X) ⟶ Z_r(X_{k^perf}) to the perfect closure of k is a p-power torsion module.

theorem isElementPowerTorsion_cokernel_baseChangeCyclePullback_perfectClosure (k : Type u)
    [Field k] (p : ℕ) [CharP k p] (hp : 0 < p) (r : ℕ) {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of k)) [LocallyOfFiniteType f] [QuasiCompact f] :
    IsElementPowerTorsion ℤ
      (CycleGroup (perfectClosureBaseChangeSituation k).baseChange
          (pullback.snd f (perfectClosureBaseChangeSituation k).g)
          ((r : ℤ) + (perfectClosureBaseChangeSituation k).c) ⧸
        (baseChangeCyclePullback (perfectClosureBaseChangeSituation k) f (r : ℤ)).range)
      (p : ℤ)

Sources

• Section 62.3, Tag 0H4E
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.injective_baseChangeCyclePullback_fieldExtension · Stacks.Chow.componentMultiplicity_baseChange_eq_one_or_char_pow · Stacks.Chow.baseChangeCyclePullback_perfectClosure_injective · Stacks.Chow.isElementPowerTorsion_cokernel_baseChangeCyclePullback_perfectClosure

Section62.4 Specialization of cycles#

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

Tag 0H4H, the section

Tag 0H4H in the Stacks Project.

Stacks.Chow.specializationMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Specialization.lean, line 327. The attribute's comment: “the specialization map sp_{X/R}”.

Stacks 0H4H. The specialization map sp_{X/R} : Z_r(X_K) ⟶ Z_r(X_κ) of a scheme locally of finite type over a discrete valuation ring R, from the cycles on the generic fibre to the cycles on the closed fibre. The generic fibre is the scheme-theoretic fibre over the generic point of Spec R, whose residue field is the fraction field K, and the closed fibre is the one over the closed point, whose residue field is κ.

def specializationMap (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    {X : Scheme.{u}} (sX : X ⟶ Spec (.of R)) [LocallyOfFiniteType sX] (r : ℕ) :
    FiberCycleGroup sX (genericPoint (Spec (.of R))) r →+
      FiberCycleGroup sX (IsLocalRing.closedPoint R) r

Tag 0H4I, a lemma

Tag 0H4I in the Stacks Project.

Stacks.Chow.topologicalKrullDim_supp_fiberModule_closedPoint_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleSpecialization/SpecializationFormula.lean, line 595. The attribute's comment: “the dimension bound on the special fibre”.

Stacks Project, Tag 0H4I. Let R be a discrete valuation ring with fraction field K and residue field kappa, let X be a scheme locally of finite type over R, let r >= 0 and let F be a coherent O_X-module flat over R. If dim(Supp(F_K)) <= r, then dim(Supp(F_kappa)) <= r.

theorem topologicalKrullDim_supp_fiberModule_closedPoint_le
    (hflat : AlgebraicGeometry.IsFlatOver f.toLRSHom.toShHom F) (r : ℕ)
    (hK : topologicalKrullDim (SheafOfModules.supp
      ((Scheme.Modules.pullback (f.fiberι (genericPoint (Spec (.of R))))).obj F)) ≤
        (r : WithBot ℕ∞)) :
    topologicalKrullDim (SheafOfModules.supp
      ((Scheme.Modules.pullback (f.fiberι (IsLocalRing.closedPoint R))).obj F)) ≤
      (r : WithBot ℕ∞)

Stacks.Chow.specializationCycle_familyAssociatedToModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleSpecialization/SpecializationFormula.lean, line 613. The attribute's comment: “the specialization formula”.

Stacks Project, Tag 0H4I. Let R be a discrete valuation ring with fraction field K and residue field kappa, let X be a scheme locally of finite type over R, let r >= 0 and let F be a coherent O_X-module flat over R with dim(Supp(F_K)) <= r. Then the specialization map sp_{X/R} : Z_r(X_K) -> Z_r(X_kappa) carries [F_K]_r to [F_kappa]_r: the member over the generic point of the family of cycles [F/X/Spec R]_r specializes to its member over the closed point.

theorem specializationCycle_familyAssociatedToModule
    (hflat : AlgebraicGeometry.IsFlatOver f.toLRSHom.toShHom F) (r : ℕ)
    (hK : topologicalKrullDim (SheafOfModules.supp
      ((Scheme.Modules.pullback (f.fiberι (genericPoint (Spec (.of R))))).obj F)) ≤
        (r : WithBot ℕ∞)) :
    specializationCycle f r
        (familyAssociatedToModule f F r
          (topologicalKrullDim_supp_fiberModule_le_of_genericFibre f F hflat r hK)
          (genericPoint (Spec (.of R)))) =
      familyAssociatedToModule f F r
        (topologicalKrullDim_supp_fiberModule_le_of_genericFibre f F hflat r hK)
        (IsLocalRing.closedPoint R)

Tag 0H4J, a lemma

Tag 0H4J in the Stacks Project.

Stacks.Chow.topologicalKrullDim_supp_fiberClosedSubscheme_closedPoint_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatCycleClasses.lean, line 181. The attribute's comment: “the dimension bound on the special fibre, for the support of i_* 𝒪_Z”.

Stacks Project, Lemma 0H4J, the dimension clause for the support of i_* 𝒪_Z. Let R be a discrete valuation ring with fraction field K and residue field κ, let Y be locally of finite type over R, let r ≥ 0 and let Z ⊆ Y be a closed subscheme flat over R. If dim(Supp((i_* 𝒪_Z)_K)) ≤ r, then dim(Supp((i_* 𝒪_Z)_κ)) ≤ r.

With 𝒪_Z for the module this is the dimension clause of Tag 0H4I; it is the tag's own statement dim(Z_K) ≤ r ⟹ dim(Z_κ) ≤ r read through Stacks.Chow.topologicalKrullDim_pullback_fiberι_eq_supp, which is what Stacks.Chow.topologicalKrullDim_pullback_fiberClosedSubscheme_closedPoint_le below does.

theorem topologicalKrullDim_supp_fiberClosedSubscheme_closedPoint_le {r : ℕ} {R : Type u}
    [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {Y Z : Scheme.{u}}
    (p : Y ⟶ Spec (.of R)) [LocallyOfFiniteType p] (i : Z ⟶ Y) [IsClosedImmersion i]
    [Flat (i ≫ p)]
    (hK : topologicalKrullDim (SheafOfModules.supp
      ((Scheme.Modules.pullback (p.fiberι (genericPoint (Spec (.of R))))).obj
        (structureSheafPushforward i))) ≤ (r : WithBot ℕ∞)) :
    topologicalKrullDim (SheafOfModules.supp
      ((Scheme.Modules.pullback (p.fiberι (IsLocalRing.closedPoint R))).obj
        (structureSheafPushforward i))) ≤ (r : WithBot ℕ∞)

Stacks.Chow.specializationCycle_familyAssociatedToClosedSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatCycleClasses.lean, line 206. The attribute's comment: “the specialization formula for the family of i_* 𝒪_Z”.

Stacks Project, Lemma 0H4J, the specialization formula for the family of i_* 𝒪_Z. Let R be a discrete valuation ring with fraction field K and residue field κ, let Y be locally of finite type over R, let r ≥ 0 and let Z ⊆ Y be a closed subscheme flat over R with dim(Supp((i_* 𝒪_Z)_K)) ≤ r. Then the specialization map sp_{Y/R} carries the member of [i_* 𝒪_Z/Y/Spec R]_r over the generic point to its member over the closed point.

With 𝒪_Z for the module this is the specialization clause of Tag 0H4I; the bound on every fibre that the family [Z/Y/Spec R]_r consumes comes from the bound on the generic fibre by Stacks.Chow.topologicalKrullDim_supp_fiberModule_le_of_genericFibre. The tag's own formula sp_{Y/R}([Z_K]_r) = [Z_κ]_r, for the family [Z/Y/Spec R]_r of the closed subscheme itself, is Stacks.Chow.specializationCycle_familyAssociatedToClosedSubscheme_of_genericFibre below.

theorem specializationCycle_familyAssociatedToClosedSubscheme {r : ℕ} {R : Type u} [CommRing R]
    [IsDomain R] [IsDiscreteValuationRing R] {Y Z : Scheme.{u}} (p : Y ⟶ Spec (.of R))
    [LocallyOfFiniteType p] (i : Z ⟶ Y) [IsClosedImmersion i] [Flat (i ≫ p)]
    (hK : topologicalKrullDim (SheafOfModules.supp
      ((Scheme.Modules.pullback (p.fiberι (genericPoint (Spec (.of R))))).obj
        (structureSheafPushforward i))) ≤ (r : WithBot ℕ∞)) :
    specializationCycle p r
        (familyAssociatedToModule p (structureSheafPushforward i) r
          (topologicalKrullDim_supp_fiberModule_le_of_genericFibre p
            (structureSheafPushforward i) (isFlatOver_pushforwardStructureSheaf i p) r hK)
          (genericPoint (Spec (.of R)))) =
      familyAssociatedToModule p (structureSheafPushforward i) r
        (topologicalKrullDim_supp_fiberModule_le_of_genericFibre p
          (structureSheafPushforward i) (isFlatOver_pushforwardStructureSheaf i p) r hK)
        (IsLocalRing.closedPoint R)

Stacks.Chow.topologicalKrullDim_pullback_fiberClosedSubscheme_closedPoint_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatCycleClasses.lean, line 265. The attribute's comment: “the dimension bound on the special fibre”.

Stacks Project, Lemma 0H4J. Let R be a discrete valuation ring with fraction field K and residue field κ, let Y be locally of finite type over R, let r ≥ 0 and let Z ⊆ Y be a closed subscheme flat over R. If dim(Z_K) ≤ r, then dim(Z_κ) ≤ r.

This is the previous bound at the closed point of Spec R.

theorem topologicalKrullDim_pullback_fiberClosedSubscheme_closedPoint_le {r : ℕ} {R : Type u}
    [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {Y Z : Scheme.{u}}
    (p : Y ⟶ Spec (.of R)) [LocallyOfFiniteType p] (i : Z ⟶ Y) [IsClosedImmersion i]
    [Flat (i ≫ p)]
    (hK : topologicalKrullDim (pullback i (p.fiberι (genericPoint (Spec (.of R)))) :
      Scheme.{u}) ≤ (r : WithBot ℕ∞)) :
    topologicalKrullDim (pullback i (p.fiberι (IsLocalRing.closedPoint R)) :
      Scheme.{u}) ≤ (r : WithBot ℕ∞)

Stacks.Chow.specializationCycle_familyAssociatedToClosedSubscheme_of_genericFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatCycleClasses.lean, line 287. The attribute's comment: “the specialization formula”.

Stacks Project, Lemma 0H4J. Let R be a discrete valuation ring with fraction field K and residue field κ, let Y be locally of finite type over R, let r ≥ 0 and let Z ⊆ Y be a closed subscheme flat over R with dim(Z_K) ≤ r. Then the specialization homomorphism sp_{Y/R} of Section 0H4H carries [Z_K]_r to [Z_κ]_r.

This is the proof of the source: the family [Z/Y/Spec R]_r of the closed subscheme is the family [i_* 𝒪_Z/Y/Spec R]_r of its structure sheaf by Chow Homology, Lemma 42.10.3, which is Stacks.Chow.familyAssociatedToClosedSubscheme_eq_familyAssociatedToModule, and for that family the formula is the specialization clause of Tag 0H4I. The bound on every fibre that the identification consumes comes from the bound on the generic fibre by Stacks.Chow.topologicalKrullDim_pullback_fiberι_le_of_genericFibre.

theorem specializationCycle_familyAssociatedToClosedSubscheme_of_genericFibre {r : ℕ}
    {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {Y Z : Scheme.{u}}
    (p : Y ⟶ Spec (.of R)) [LocallyOfFiniteType p] (i : Z ⟶ Y) [IsClosedImmersion i]
    [Flat (i ≫ p)]
    (hK : topologicalKrullDim (pullback i (p.fiberι (genericPoint (Spec (.of R)))) :
      Scheme.{u}) ≤ (r : WithBot ℕ∞)) :
    specializationCycle p r
        (familyAssociatedToClosedSubscheme p i r (genericPoint (Spec (.of R)))) =
      familyAssociatedToClosedSubscheme p i r (IsLocalRing.closedPoint R)

Tag 0H4K, a lemma

Tag 0H4K in the Stacks Project.

Stacks.Chow.baseChangeFiberCycleOfEq_comp_specializationCycleHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SpecializationBaseChange.lean, line 645.

Stacks Project, Tag 0H4K. Let R'/R be an extension of discrete valuation rings, inducing a fraction field extension K'/K and a residue field extension κ'/κ, let X be locally of finite type over R and let X' = X_{R'}. For r ≥ 0 the square formed by the specialization homomorphisms sp_{X/R} : Z_r(X_K) ⟶ Z_r(X_κ) and sp_{X'/R'} : Z_r(X'_{K'}) ⟶ Z_r(X'_{κ'}) of Section 0H4H and the base change maps of Section 0H4E commutes.

The integral-subscheme case is Stacks.Chow.specializationCompatibleWithBaseChange and the passage from it to an arbitrary cycle is Stacks.Chow.baseChangeFiberCycleOfEq_comp_specializationCycleHom_of_generator.

theorem baseChangeFiberCycleOfEq_comp_specializationCycleHom :
    (baseChangeSpecialFibreCycle R' f r).comp (specializationCycleHom f r) =
      (specializationCycleHom (pullback.snd f (specMapAlgebraMap R R')) r).comp
        (baseChangeGenericFibreCycle R' f r)

Tag 0H4L, a lemma

Tag 0H4L in the Stacks Project.

Stacks.Chow.fiberCycleFlatPullback_comp_specializationCycleHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SpecializationFlatPullback.lean, line 188.

Stacks Project, Lemma 0H4L. Let R be a discrete valuation ring with fraction field K and residue field κ, let X be a scheme locally of finite type over R, and let p : X' ⟶ X be a morphism which is locally of finite type, flat and of relative dimension e. Then for r ≥ 0 the square formed by the specialization homomorphisms sp_{X/R} : Z_r(X_K) ⟶ Z_r(X_κ) and sp_{X'/R} : Z_{r+e}(X'_K) ⟶ Z_{r+e}(X'_κ) of Section 0H4H and the flat pullbacks Z_r(X_K) ⟶ Z_{r+e}(X'_K), Z_r(X_κ) ⟶ Z_{r+e}(X'_κ) of Section 0H4N commutes.

The integral-subscheme case is Stacks.Chow.specializationCycle_fiberCycleFlatPullback_integralGenericCycle. The passage from it to an arbitrary cycle is the regrouping below: the coefficient of sp_{X'/R} of a flat pullback is a locally finite sum over the points of X'_K, which is summed along the fibres of X'_K ⟶ X_K and each fibre identified with the corresponding term of the flat pullback of sp_{X/R}.

theorem fiberCycleFlatPullback_comp_specializationCycleHom :
    (fiberCycleFlatPullback f fX' p hp e he (IsLocalRing.closedPoint R) r).comp
        (specializationCycleHom f r) =
      (specializationCycleHom fX' (r + e)).comp
        (fiberCycleFlatPullback f fX' p hp e he (genericPoint (Spec (.of R))) r)

Stacks.Chow.specializationCycle_baseChangedFiberCycleFlatPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SpecializationFlatPullback.lean, line 289. The attribute's comment: “for the base change of the flat morphism to the spectrum of a discrete valuation ring over the base”.

Stacks Project, Lemma 0H4L for the base change of a flat morphism of the source to the spectrum of a discrete valuation ring over the base. This is the shape in which the valuative condition of Definition 0H50 compares the two members of a flat pullback of a family of cycles on fibres: Stacks.Chow.baseChangedFiberCycleFlatPullback is flat pullback along the base change of j, which is again flat, locally of finite type and of relative dimension e.

theorem specializationCycle_baseChangedFiberCycleFlatPullback {X S U : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (fU : U ⟶ S) [LocallyOfFiniteType fU] (j : U ⟶ X)
    [LocallyOfFiniteType j] [Flat j] (h : j ≫ f = fU) (e : ℕ)
    (he : AlgebraicGeometry.RelativeDimension j e) {R : Type u} [CommRing R] [IsDomain R]
    [IsDiscreteValuationRing R] (g : Spec (.of R) ⟶ S) (r : ℕ)
    (c : FiberCycleGroup (pullback.snd f g) (genericPoint (Spec (.of R))) r) :
    baseChangedFiberCycleFlatPullback f fU j h e he g (IsLocalRing.closedPoint R) r
        (specializationCycle (pullback.snd f g) r c) =
      specializationCycle (pullback.snd fU g) (r + e)
        (baseChangedFiberCycleFlatPullback f fU j h e he g
          (genericPoint (Spec (.of R))) r c)

Stacks.Chow.specializationCycle_fiberCycleRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SpecializationRestriction.lean, line 271. The attribute's comment: “open immersions”.

The specialization map commutes with restriction to an open subscheme of the source: for j : U ⟶ X an open immersion of schemes locally of finite type over a discrete valuation ring R, restricting an r-cycle on the generic fibre of X to the generic fibre of U and then specializing is the same as specializing and then restricting to the special fibre of U.

theorem specializationCycle_fiberCycleRestrict {R : Type u} [CommRing R] [IsDomain R]
    [IsDiscreteValuationRing R] {X U : Scheme.{u}} (f : X ⟶ Spec (.of R))
    [LocallyOfFiniteType f] (fU : U ⟶ Spec (.of R)) [LocallyOfFiniteType fU] (j : U ⟶ X)
    [IsOpenImmersion j] (h : j ≫ f = fU) (r : ℕ)
    (c : FiberCycleGroup f (genericPoint (Spec (.of R))) r) :
    specializationCycle fU r
        (fiberCycleRestrict f fU j h (genericPoint (Spec (.of R))) r c) =
      fiberCycleRestrict f fU j h (IsLocalRing.closedPoint R) r (specializationCycle f r c)

Tag 0H4M, a lemma

Tag 0H4M in the Stacks Project.

Stacks.Chow.specializationCycle_properPushforwardFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedImmersion.lean, line 267. The attribute's comment: “specialization commutes with pushforward along a closed immersion”.

Specialization of cycles over a discrete valuation ring commutes with pushforward along a closed immersion over that ring: pushing the specialization of a cycle on the generic fibre forward along the morphism of closed fibres gives the specialization of its pushforward along the morphism of generic fibres.

theorem specializationCycle_properPushforwardFamily
    (c : FiberCycleGroup sX (genericPoint (Spec (.of R))) r) :
    fiberProperPushforward sX sY i hi (IsLocalRing.closedPoint R) r (specializationCycle sX r c) =
      specializationCycle sY r
        (fiberProperPushforward sX sY i hi (genericPoint (Spec (.of R))) r c)

Stacks.Chow.specializationCycle_fiberProperPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SpecializationProperPushforward.lean, line 362. The attribute's comment: “the square of the specialization maps and the proper pushforwards commutes”.

Stacks 0H4M. Let R be a discrete valuation ring with fraction field K and residue field κ, let f : X ⟶ Y be a proper morphism of schemes locally of finite type over R and let r ≥ 0. The square formed by the specialization maps sp_{X/R} : Z_r(X_K) ⟶ Z_r(X_κ) and sp_{Y/R} : Z_r(Y_K) ⟶ Z_r(Y_κ) and the proper pushforwards along the morphisms f_K and f_κ induced by f on the generic and the closed fibres commutes.

theorem specializationCycle_fiberProperPushforward (sX : X ⟶ Spec (.of R))
    [LocallyOfFiniteType sX] (sY : Y ⟶ Spec (.of R)) [LocallyOfFiniteType sY] (f : X ⟶ Y)
    [IsProper f] (hf : f ≫ sY = sX) (r : ℕ)
    (c : FiberCycleGroup sX (genericPoint (Spec (.of R))) r) :
    fiberProperPushforward sX sY f hf (IsLocalRing.closedPoint R) r
        (specializationCycle sX r c) =
      specializationCycle sY r
        (fiberProperPushforward sX sY f hf (genericPoint (Spec (.of R))) r c)

Stacks.Chow.properPushforward_specializationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SpecializationProperPushforward.lean, line 412. The attribute's comment: “the square, read on the specialization map sp_{X/R} of Stacks 0H4H”.

Stacks 0H4M, read on the specialization map sp_{X/R} of Stacks 0H4H: the square formed by sp_{X/R}, sp_{Y/R} and the proper pushforwards along the morphisms induced by f on the generic and the closed fibres commutes.

theorem properPushforward_specializationMap (R : Type u) [CommRing R] [IsDomain R]
    [IsDiscreteValuationRing R] {X Y : Scheme.{u}} (sX : X ⟶ Spec (.of R))
    [LocallyOfFiniteType sX] (sY : Y ⟶ Spec (.of R)) [LocallyOfFiniteType sY] (f : X ⟶ Y)
    [IsProper f] (hf : f ≫ sY = sX) (r : ℕ)
    (α : FiberCycleGroup sX (genericPoint (Spec (.of R))) r) :
    fiberProperPushforward sX sY f hf (IsLocalRing.closedPoint R) r
        (specializationMap R sX r α) =
      specializationMap R sY r
        (fiberProperPushforward sX sY f hf (genericPoint (Spec (.of R))) r α)

Sources

• Section 62.4, Tag 0H4H
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.specializationMap · Stacks.Chow.topologicalKrullDim_supp_fiberModule_closedPoint_le · Stacks.Chow.specializationCycle_familyAssociatedToModule · Stacks.Chow.topologicalKrullDim_supp_fiberClosedSubscheme_closedPoint_le · Stacks.Chow.specializationCycle_familyAssociatedToClosedSubscheme · Stacks.Chow.topologicalKrullDim_pullback_fiberClosedSubscheme_closedPoint_le · Stacks.Chow.specializationCycle_familyAssociatedToClosedSubscheme_of_genericFibre · Stacks.Chow.baseChangeFiberCycleOfEq_comp_specializationCycleHom

Section62.5 Families of cycles on fibres#

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

Tag 0H4N, the section

Tag 0H4N in the Stacks Project.

Stacks.Chow.flatPullbackFamily, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatPullbackFamily.lean, line 162. The attribute's comment: “flat pullback of a family of cycles on fibres”.

Stacks Project, Section 0H4N. The flat pullback j^*α of a family α of r-cycles on the fibres of X/S along a flat morphism j : U ⟶ X of schemes over S, locally of finite type and of relative dimension e: the family of (r+e)-cycles on the fibres of U/S whose member over s is the flat pullback of α_s along U_s ⟶ X_s.

def flatPullbackFamily {X S U : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] (fU : U ⟶ S)
    [LocallyOfFiniteType fU] (j : U ⟶ X) [LocallyOfFiniteType j] [Flat j] (h : j ≫ f = fU)
    (e : ℕ) (he : AlgebraicGeometry.RelativeDimension j e) (r : ℕ) (α : FamilyOfCycles f r) :
    FamilyOfCycles fU (r + e)

Tag 0H4P, a lemma

Tag 0H4P in the Stacks Project.

Stacks.Chow.baseChangeFamily_baseChangeFamily_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Compatibilities.lean, line 98. The attribute's comment: “part (1): base change is functorial”.

Stacks Project, Tag 0H4P, part (1). Base change of families of cycles on fibres is functorial: base changing a family α of r-cycles on the fibres of X/S along g : S' ⟶ S and then along h : S'' ⟶ S' is base changing it along h ≫ g, the two families being identified through the canonical isomorphism (X ×_S S') ×_{S'} S'' ≅ X ×_S S''.

theorem baseChangeFamily_baseChangeFamily_comp {X S S' S'' : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (g : S' ⟶ S) (h : S'' ⟶ S') (r : ℕ) (α : FamilyOfCycles f r) :
    baseChangeFamily (pullback.snd f g) h r (baseChangeFamily f g r α) =
      fun u => fiberCycleRestrict (pullback.snd f (h ≫ g)) (pullback.snd (pullback.snd f g) h)
        (pullbackLeftPullbackSndIso f g h).hom (pullbackLeftPullbackSndIso_hom_snd f g h) u r
        (baseChangeFamily f (h ≫ g) r α u)

Stacks.Chow.restrictedFamily_eq_flatPullbackFamily_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Compatibilities.lean, line 150. The attribute's comment: “part (2): restriction is base change followed by flat pullback”.

Stacks Project, Tag 0H4P, part (2). Restriction of families of cycles on fibres is a combination of base change and flat pullback: for open subschemes U ⊆ X and V ⊆ S with f(U) ⊆ V, the restriction α|_U of a family α of r-cycles on the fibres of X/S is the flat pullback, along the open immersion U ⟶ X ×_S V (flat of relative dimension zero), of the base change of α along V ⟶ S.

theorem restrictedFamily_eq_flatPullbackFamily_baseChangeFamily (r : ℕ)
    (α : FamilyOfCycles f r) :
    (restrictedFamily f fU j i h r α).1 =
      flatPullbackFamily (pullback.snd f i) fU (pullback.lift j fU h) (pullback.lift_snd _ _ _) 0
        (relativeDimension_of_isOpenImmersion _) r (baseChangeFamily f i r α)

Stacks.Chow.baseChangeFamily_flatPullbackFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Compatibilities.lean, line 183. The attribute's comment: “part (3): flat pullback commutes with base change”.

Stacks Project, Tag 0H4P, part (3). Flat pullback of families of cycles on fibres commutes with base change: for a flat morphism j : U ⟶ X over S, locally of finite type and of relative dimension e, and a morphism g : T ⟶ S, the base change of j^*α along g is the flat pullback of g^*α along the base change U ×_S T ⟶ X ×_S T of j.

theorem baseChangeFamily_flatPullbackFamily {X S U T : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (fU : U ⟶ S) [LocallyOfFiniteType fU] (j : U ⟶ X)
    [LocallyOfFiniteType j] [Flat j] (h : j ≫ f = fU) (e : ℕ)
    (he : AlgebraicGeometry.RelativeDimension j e) (g : T ⟶ S) (r : ℕ)
    (α : FamilyOfCycles f r) :
    baseChangeFamily fU g (r + e) (flatPullbackFamily f fU j h e he r α) =
      flatPullbackFamily (pullback.snd f g) (pullback.snd fU g) (pullbackRestrict f fU j h g)
        (pullbackRestrict_snd f fU j h g) e (relativeDimension_pullbackRestrict f fU j h g he) r
        (baseChangeFamily f g r α)

Stacks.Chow.flatPullbackFamily_flatPullbackFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Compatibilities.lean, line 258. The attribute's comment: “part (4): flat pullback is functorial”.

Stacks Project, Tag 0H4P, part (4). Flat pullback of families of cycles on fibres is functorial: for flat morphisms j : U ⟶ X and k : V ⟶ U over S, locally of finite type and of relative dimensions e and e', pulling a family α of r-cycles on the fibres of X/S back along j and then along k is pulling it back along k ≫ j, which has relative dimension e' + e.

The two families are families of cycles of the dimensions (r + e) + e' and r + (e' + e), which are equal but not definitionally so; the statement is the equality of the underlying cycles on every fibre of V/S.

theorem flatPullbackFamily_flatPullbackFamily {X S U V : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (fU : U ⟶ S) [LocallyOfFiniteType fU] (fV : V ⟶ S)
    [LocallyOfFiniteType fV] (j : U ⟶ X) [LocallyOfFiniteType j] [Flat j] (k : V ⟶ U)
    [LocallyOfFiniteType k] [Flat k] (h : j ≫ f = fU) (hk : k ≫ fU = fV) (e e' : ℕ)
    (he : AlgebraicGeometry.RelativeDimension j e)
    (he' : AlgebraicGeometry.RelativeDimension k e') (r : ℕ) (α : FamilyOfCycles f r) (s : S) :
    (flatPullbackFamily fU fV k hk e' he' (r + e) (flatPullbackFamily f fU j h e he r α) s :
        AlgebraicCycle (fV.fiber s) ℤ) =
      (flatPullbackFamily f fV (k ≫ j) (by rw [Category.assoc, h, hk]) (e' + e)
        (AlgebraicGeometry.RelativeDimension.comp_of_flat k j he' he) r α s :
          AlgebraicCycle (fV.fiber s) ℤ)

Stacks.Chow.baseChangeFamily_properPushforwardFamily_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Compatibilities.lean, line 326. The attribute's comment: “part (5): proper pushforward commutes with base change”.

Stacks Project, Tag 0H4P, part (5). Proper pushforward of families of cycles on fibres commutes with base change: for a proper morphism f : X ⟶ Y of schemes locally of finite type over S and a morphism g : S' ⟶ S, the base change of f_*α along g is the pushforward of g^*α along the base change X ×_S S' ⟶ Y ×_S S' of f.

theorem baseChangeFamily_properPushforwardFamily_of_isProper (r : ℕ) (α : FamilyOfCycles sX r) :
    baseChangeFamily sY g r (properPushforwardFamily sX sY f hf r α) =
      properPushforwardFamily (pullback.snd sX g) (pullback.snd sY g)
        (baseChangeMap sX sY f hf g) (baseChangeMap_snd sX sY f hf g) r
        (baseChangeFamily sX g r α)

Stacks.Chow.properPushforwardFamily_properPushforwardFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Compatibilities.lean, line 391. The attribute's comment: “part (6): proper pushforward is functorial”.

Stacks Project, Tag 0H4P, part (6). Proper pushforward of families of cycles on fibres is functorial: for proper morphisms f₁ : X ⟶ Y and f₂ : Y ⟶ Z of schemes locally of finite type over S, pushing a family of r-cycles on the fibres of X/S forward along f₁ and then along f₂ is pushing it forward along f₁ ≫ f₂.

theorem properPushforwardFamily_properPushforwardFamily {S X Y Z : Scheme.{u}} (sX : X ⟶ S)
    [LocallyOfFiniteType sX] (sY : Y ⟶ S) [LocallyOfFiniteType sY] (sZ : Z ⟶ S)
    [LocallyOfFiniteType sZ] (f₁ : X ⟶ Y) [IsProper f₁] (f₂ : Y ⟶ Z) [IsProper f₂]
    (hf₁ : f₁ ≫ sY = sX) (hf₂ : f₂ ≫ sZ = sY) (r : ℕ) (α : FamilyOfCycles sX r) :
    properPushforwardFamily sY sZ f₂ hf₂ r (properPushforwardFamily sX sY f₁ hf₁ r α) =
      properPushforwardFamily sX sZ (f₁ ≫ f₂) (by rw [Category.assoc, hf₂, hf₁]) r α

Stacks.Chow.flatPullbackFamily_properPushforwardFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Compatibilities.lean, line 447. The attribute's comment: “part (7): proper pushforward commutes with flat pullback”.

Stacks Project, Tag 0H4P, part (7). Proper pushforward of families of cycles on fibres commutes with flat pullback: for a proper morphism f : X ⟶ Y and a flat morphism g : Y' ⟶ Y of relative dimension e of schemes locally of finite type over S, with base changes f' : X ×_Y Y' ⟶ Y' and g' : X ×_Y Y' ⟶ X, one has g^*(f_*α) = f'_*((g')^*α) for every family α of r-cycles on the fibres of X/S.

theorem flatPullbackFamily_properPushforwardFamily (e : ℕ)
    (he : AlgebraicGeometry.RelativeDimension g e) (r : ℕ) (α : FamilyOfCycles sX r) :
    flatPullbackFamily sY sY' g hg e he r (properPushforwardFamily sX sY f hf r α) =
      properPushforwardFamily (pullback.fst f g ≫ sX) sY' (pullback.snd f g)
        (pullback_snd_comp_eq_fst_comp sX sY sY' f hf g hg) (r + e)
        (flatPullbackFamily sX (pullback.fst f g ≫ sX) (pullback.fst f g) rfl e
          (AlgebraicGeometry.RelativeDimension.of_isPullback (IsPullback.of_hasPullback f g).flip
            he) r α)

Tag 0H4Q, an example

Tag 0H4Q in the Stacks Project.

Stacks.Chow.familyAssociatedToModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleFamily.lean, line 161. The attribute's comment: “the associated family”.

Stacks 0H4Q. The family [F/X/S]_r of r-cycles on the fibres of f attached to a quasi-coherent module F of finite type whose support on every fibre has dimension at most r: its member over s is the cycle [F_s]_r associated to the pullback of F to the fibre over s.

def familyAssociatedToModule (f : X ⟶ S) [LocallyOfFiniteType f] (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] (r : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤
        (r : WithBot ℕ∞)) :
    FamilyOfCycles f r

Stacks.Chow.familyAssociatedToModule_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleFamily.lean, line 175. The attribute's comment: “fibrewise formula”.

Stacks 0H4Q. The member of [F/X/S]_r over a point s of the base is the cycle [F_s]_r associated to the pullback of F to the fibre over s.

theorem familyAssociatedToModule_apply (f : X ⟶ S) [LocallyOfFiniteType f] (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] (r : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤
        (r : WithBot ℕ∞)) (s : S) :
    familyAssociatedToModule f F r hdim s =
      cycleAssociatedToCoherentSheaf (fieldChowSituation (S.residueField s))
        (f.fiberToSpecResidueField s) ((Scheme.Modules.pullback (f.fiberι s)).obj F) (r : ℤ)
        (fiberModule_schemeDeltaDimension_le f F r hdim s)

Tag 0H4R, a lemma

Tag 0H4R in the Stacks Project.

Stacks.Chow.supportDimension_le_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleBaseChange.lean, line 126. The attribute's comment: “module_base_change, residue-field-isomorphism case: dimension bound”.

Stacks Project, Tag 0H4R. The dimension bound on the fibrewise supports of a quasi-coherent module of finite type survives base change along a morphism that induces an isomorphism on every residue field: the support on the fibre over t is the inverse image of the support on the fibre over g t along an isomorphism of fibres.

theorem supportDimension_le_of_baseChange (f : X ⟶ S) [LocallyOfFiniteType f] (g : S' ⟶ S)
    (hres : ∀ t : S', IsIso (g.residueFieldMap t)) (F : X.Modules) [F.IsFiniteType] (r : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤ (r : WithBot ℕ∞)) :
    ∀ t : S', topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback ((pullback.snd f g).fiberι t)).obj
        ((Scheme.Modules.pullback (pullback.fst f g)).obj F))) ≤ (r : WithBot ℕ∞)

Stacks.Chow.familyAssociatedToModule_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleBaseChange.lean, line 148. The attribute's comment: “module_base_change, residue-field-isomorphism case”.

Stacks Project, Tag 0H4R. Base change along a morphism g that induces an isomorphism on every residue field carries the family of cycles associated to a quasi-coherent module of finite type to the family associated to the base-changed module. Coefficientwise: the base change preserves the multiplicity of the module and the relative dimension of a point of the fibre, and the support of the base-changed module on a fibre over t is the inverse image of the support of the original one on the fibre over g t.

theorem familyAssociatedToModule_baseChange (f : X ⟶ S) [LocallyOfFiniteType f] (g : S' ⟶ S)
    (hres : ∀ t : S', IsIso (g.residueFieldMap t)) (F : X.Modules) [F.IsFiniteType]
    [F.IsQuasicoherent] (r : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤ (r : WithBot ℕ∞)) :
    baseChangeFamilyOfResidueIso f g hres r (familyAssociatedToModule f F r hdim) =
      familyAssociatedToModule (pullback.snd f g)
        ((Scheme.Modules.pullback (pullback.fst f g)).obj F) r
        (supportDimension_le_of_baseChange f g hres F r hdim)

Stacks.Chow.supportDimension_le_of_flatPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleFlatPullback.lean, line 93. The attribute's comment: “module_flat_pullback: dimension bound”.

Stacks Project, Tag 0H4R. The fibrewise support dimension bound on a quasi-coherent module of finite type passes to its pullback along a flat morphism j : U ⟶ X of schemes over S, locally of finite type and of relative dimension e, with r replaced by r + e: on the fibre over s this is the support dimension bound of Stacks 02RE, part (2), for the induced morphism U_s ⟶ X_s, which is again flat of relative dimension e.

theorem supportDimension_le_of_flatPullback (f : X ⟶ S) [LocallyOfFiniteType f] (fU : U ⟶ S)
    [LocallyOfFiniteType fU] (j : U ⟶ X) [LocallyOfFiniteType j] [Flat j] (h : j ≫ f = fU)
    (e : ℕ) (he : AlgebraicGeometry.RelativeDimension j e) (F : X.Modules) [F.IsFiniteType]
    [F.IsQuasicoherent] (r : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤
        (r : WithBot ℕ∞)) :
    ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (fU.fiberι s)).obj
        ((Scheme.Modules.pullback j).obj F))) ≤ ((r + e : ℕ) : WithBot ℕ∞)

Stacks.Chow.familyAssociatedToModule_flatPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleFlatPullback.lean, line 137. The attribute's comment: “module_flat_pullback”.

Stacks Project, Tag 0H4R. The flat pullback of the family [F/X/S]_r of cycles associated to a quasi-coherent module of finite type, along a flat morphism j : U ⟶ X of schemes over S which is locally of finite type and of relative dimension e, is the family [j^*F/U/S]_{r+e} associated to the pulled-back module.

On the fibre over s the morphism U_s ⟶ X_s induced by j is flat, locally of finite type and of relative dimension e, so Stacks 02RE, part (2), identifies the flat pullback of the cycle [F_s]_r with the cycle of the pullback of F_s; that pullback is the restriction of j^*F to the fibre of f_U, the two orders of pulling F back being compared by the pullback-composition isomorphism.

theorem familyAssociatedToModule_flatPullback (f : X ⟶ S) [LocallyOfFiniteType f] (fU : U ⟶ S)
    [LocallyOfFiniteType fU] (j : U ⟶ X) [LocallyOfFiniteType j] [Flat j] (h : j ≫ f = fU)
    (e : ℕ) (he : AlgebraicGeometry.RelativeDimension j e) (F : X.Modules) [F.IsFiniteType]
    [F.IsQuasicoherent] (r : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤
        (r : WithBot ℕ∞)) :
    flatPullbackFamily f fU j h e he r (familyAssociatedToModule f F r hdim) =
      familyAssociatedToModule fU ((Scheme.Modules.pullback j).obj F) (r + e)
        (supportDimension_le_of_flatPullback f fU j h e he F r hdim)

Stacks.Chow.supportDimension_le_of_baseChange_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleGeneralBaseChange.lean, line 102. The attribute's comment: “module_base_change, arbitrary morphism of bases: dimension bound”.

Stacks Project, Tag 0H4R. The fibrewise support dimension bound on a quasi-coherent module of finite type survives base change along an arbitrary morphism of bases: the fibre of X ×_S S' ⟶ S' over t is the base change of the fibre of f over g t along the residue field extension κ(t)/κ(g t), the support of the pulled-back module on it is the inverse image of the support on the fibre over g t, and no point of the former has larger delta-dimension than its image.

theorem supportDimension_le_of_baseChange_general (f : X ⟶ S) [LocallyOfFiniteType f]
    (g : S' ⟶ S) (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent] (r : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤
        (r : WithBot ℕ∞)) :
    ∀ t : S', topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback ((pullback.snd f g).fiberι t)).obj
        ((Scheme.Modules.pullback (pullback.fst f g)).obj F))) ≤ (r : WithBot ℕ∞)

Stacks.Chow.familyAssociatedToModule_baseChange_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleGeneralBaseChange.lean, line 138. The attribute's comment: “module_base_change, arbitrary morphism of bases”.

Stacks Project, Tag 0H4R. Base change of the family [F/X/S]_r of cycles associated to a quasi-coherent module of finite type along an arbitrary morphism g : S' ⟶ S of bases is the family associated to the pulled-back module.

The fibre of X ×_S S' ⟶ S' over a point t is the base change of the fibre of f over g t along the residue field extension κ(t)/κ(g t). That extension is flat and the dimension shift of the associated base change of Chow situations vanishes, so Stacks 0FVI part (2) applies and identifies the base change of the cycle [F_{g t}]_r with the cycle of the base-changed module; transporting the result along the canonical isomorphism of fibres, which is an open immersion, changes neither multiplicities nor relative dimensions.

theorem familyAssociatedToModule_baseChange_general (f : X ⟶ S) [LocallyOfFiniteType f]
    (g : S' ⟶ S) (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent] (r : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤
        (r : WithBot ℕ∞)) :
    baseChangeFamily f g r (familyAssociatedToModule f F r hdim) =
      familyAssociatedToModule (pullback.snd f g)
        ((Scheme.Modules.pullback (pullback.fst f g)).obj F) r
        (supportDimension_le_of_baseChange_general f g F r hdim)

Stacks.Chow.supportDimension_le_of_openRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleRestriction.lean, line 187. The attribute's comment: “module_restriction: dimension bound”.

Stacks Project, Tag 0H4R. The dimension bound on the fibrewise supports of a quasi-coherent module of finite type survives restriction of both the source and the base to compatible open subschemes: the support on the fibre of fU over t is the inverse image of the support on the fibre of f over i t along an open immersion of fibres.

theorem supportDimension_le_of_openRestriction {X S U V : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (fU : U ⟶ V) [LocallyOfFiniteType fU] (j : U ⟶ X)
    [IsOpenImmersion j] (i : V ⟶ S) [IsOpenImmersion i] (h : j ≫ f = fU ≫ i) (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] (r : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤ (r : WithBot ℕ∞)) :
    ∀ t : V, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (fU.fiberι t)).obj
        ((Scheme.Modules.pullback j).obj F))) ≤ (r : WithBot ℕ∞)

Stacks.Chow.familyAssociatedToModule_openRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleRestriction.lean, line 207. The attribute's comment: “module_restriction”.

Stacks Project, Tag 0H4R. The restriction to U/V of the family of cycles associated to a quasi-coherent module of finite type is the family associated to the module restricted to U. Coefficientwise: restriction preserves the multiplicity of the module and the relative dimension of a point of the fibre, and the support of the restricted module on a fibre of fU is the inverse image of the support of the original one.

theorem familyAssociatedToModule_openRestriction {X S U V : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (fU : U ⟶ V) [LocallyOfFiniteType fU] (j : U ⟶ X)
    [IsOpenImmersion j] (i : V ⟶ S) [IsOpenImmersion i] (h : j ≫ f = fU ≫ i) (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] (r : ℕ)
    (hdim : ∀ s : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ≤ (r : WithBot ℕ∞)) :
    (restrictedFamily f fU j i h r (familyAssociatedToModule f F r hdim)).1 =
      familyAssociatedToModule fU ((Scheme.Modules.pullback j).obj F) r
        (supportDimension_le_of_openRestriction f fU j i h F r hdim)

Tag 0H4S, an example

Tag 0H4S in the Stacks Project.

Stacks.Chow.familyAssociatedToClosedSubscheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedSubschemeFamily.lean, line 113. The attribute's comment: “the associated family”.

The family [Z/X/S]_r of r-cycles on the fibres of f attached to a closed subscheme i : Z ⟶ X whose fibres have dimension at most r: its member over s is the cycle [Z_s]_r of the inverse image of Z in the fibre over s.

def familyAssociatedToClosedSubscheme (f : X ⟶ S) [LocallyOfFiniteType f] {Z : Scheme.{u}}
    (i : Z ⟶ X) [IsClosedImmersion i] (r : ℕ) : FamilyOfCycles f r

Stacks.Chow.familyAssociatedToClosedSubscheme_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedSubschemeFamily.lean, line 121. The attribute's comment: “fibrewise formula”.

The member of [Z/X/S]_r over a point s of the base is the cycle [Z_s]_r of the inverse image of Z in the fibre over s.

theorem familyAssociatedToClosedSubscheme_apply (f : X ⟶ S) [LocallyOfFiniteType f]
    {Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i] (r : ℕ) (s : S) :
    familyAssociatedToClosedSubscheme f i r s =
      cycleAssociatedToClosedSubscheme (fieldChowSituation (S.residueField s))
        (f.fiberToSpecResidueField s) (fiberClosedImmersion f i s) (r : ℤ)

Tag 0H4T, a lemma

Tag 0H4T in the Stacks Project.

Stacks.Chow.familyAssociatedToClosedSubscheme_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedSubschemeBaseChange.lean, line 100. The attribute's comment: “base change”.

Stacks Project, Tag 0H4T (base change). The construction of Example 0H4S is compatible with base change: let f : X ⟶ S be locally of finite type, let i : Z ⟶ X be a closed subscheme with dim(Z_s) ≤ r for every s ∈ S, and let g : S' ⟶ S be an arbitrary morphism of schemes. Then the base change of the family [Z/X/S]_r along g is the family attached to the inverse image Z ×_X (X ×_S S') of Z in X ×_S S'.

With F = i_* 𝒪_Z the family [Z/X/S]_r is [F/X/S]_r by Chow Homology, Lemma 02QY, read on each fibre, so this is the base-change clause of Lemma 0H4R applied to F, together with the identification of the inverse image of F with the direct image of the structure sheaf of the base change of Z.

theorem familyAssociatedToClosedSubscheme_baseChange (f : X ⟶ S) [LocallyOfFiniteType f]
    (g : S' ⟶ S) (i : Z ⟶ X) [IsClosedImmersion i] (r : ℕ)
    (hZ : ∀ s : S, topologicalKrullDim (pullback i (f.fiberι s) : Scheme.{u}) ≤
      (r : WithBot ℕ∞)) :
    baseChangeFamily f g r (familyAssociatedToClosedSubscheme f i r) =
      familyAssociatedToClosedSubscheme (pullback.snd f g)
        (pullback.snd i (pullback.fst f g)) r

Stacks.Chow.familyAssociatedToClosedSubscheme_flatPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedSubschemeFlatPullback.lean, line 79. The attribute's comment: “flat pullback”.

The construction of Example 0H4S is compatible with flat pullback: let f : X ⟶ S be locally of finite type, let i : Z ⟶ X be a closed subscheme with dim(Z_s) ≤ r for every s ∈ S, and let j : U ⟶ X be flat, locally of finite type and of relative dimension e, a morphism of schemes over S through j ≫ f = f_U. Then the flat pullback of the family [Z/X/S]_r along j is the family [Z ×_X U / U / S]_{r+e} attached to the scheme-theoretic inverse image of Z in U.

theorem familyAssociatedToClosedSubscheme_flatPullback (f : X ⟶ S) [LocallyOfFiniteType f]
    (fU : U ⟶ S) [LocallyOfFiniteType fU] (j : U ⟶ X) [LocallyOfFiniteType j] [Flat j]
    (h : j ≫ f = fU) (e : ℕ) (he : AlgebraicGeometry.RelativeDimension j e) (i : Z ⟶ X)
    [IsClosedImmersion i] (r : ℕ)
    (hZ : ∀ s : S, topologicalKrullDim (pullback i (f.fiberι s) : Scheme.{u}) ≤
      (r : WithBot ℕ∞)) :
    flatPullbackFamily f fU j h e he r (familyAssociatedToClosedSubscheme f i r) =
      familyAssociatedToClosedSubscheme fU (pullback.snd i j) (r + e)

Stacks.Chow.familyAssociatedToClosedSubscheme_openRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedSubschemeRestriction.lean, line 347. The attribute's comment: “restriction”.

Stacks Project, Tag 0H4T (restriction). The construction of Example 0H4S is compatible with restriction: let f : X ⟶ S be locally of finite type, let i : Z ⟶ X be a closed subscheme with dim(Z_s) ≤ r for every s ∈ S, and let j : U ⟶ X and i' : V ⟶ S be open subschemes with fU : U ⟶ V making the square commute. Then the restriction of the family [Z/X/S]_r to the fibres of U/V is the family [Z ∩ U / U / V]_r attached to the closed subscheme Z ∩ U = Z ×_X U of U.

Coefficientwise: restriction preserves the multiplicity of a component of a fibre of Z and the relative dimension of a point of a fibre, and a component of Z_{i' t} contributes to the restricted family exactly when it meets U_t. The comparison over a single point t of V needs the dimension bound only over i' t; that is Stacks.Chow.familyAssociatedToClosedSubscheme_openRestriction_apply.

theorem familyAssociatedToClosedSubscheme_openRestriction (f : X ⟶ S) [LocallyOfFiniteType f]
    (fU : U ⟶ V) [LocallyOfFiniteType fU] (j : U ⟶ X) [IsOpenImmersion j] (i' : V ⟶ S)
    [IsOpenImmersion i'] (h : j ≫ f = fU ≫ i') (i : Z ⟶ X) [IsClosedImmersion i] (r : ℕ)
    (hdim : ∀ s : S,
      topologicalKrullDim ↥(pullback i (f.fiberι s)) ≤ (r : WithBot ℕ∞)) :
    (restrictedFamily f fU j i' h r (familyAssociatedToClosedSubscheme f i r)).1 =
      familyAssociatedToClosedSubscheme fU (pullback.fst j i) r

Tag 0H4U, a remark

Tag 0H4U in the Stacks Project.

Stacks.Chow.supportOfFamily, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Basic.lean, line 89. The attribute's comment: “support_of_a_family_of_cycles”.

The support of a family of cycles on the fibres of f: the union in X of the images of the supports of its members.

def supportOfFamily {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] {r : ℕ}
    (α : FamilyOfCycles f r) : Set X

Stacks.Chow.exists_family_support_not_closed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NonclosedSupport.lean, line 77.

Stacks Project, Tag 0H4U. The support of a family of cycles on fibres need not be closed in the total space.

theorem exists_family_support_not_closed :
    ∃ (X S : Scheme.{u}) (f : X ⟶ S) (h : LocallyOfFiniteType f),
      letI : LocallyOfFiniteType f := h
      ∃ (r : ℕ) (α : FamilyOfCycles f r), ¬ IsClosed (supportOfFamily f α)

Tag 0H4V, a lemma

Tag 0H4V in the Stacks Project.

Stacks.Chow.supportOfFamily_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/BaseChangeSupport.lean, line 204. The attribute's comment: “base change”.

Stacks Project, Tag 0H4V, the base-change clause. Taking the support of a family of cycles on the fibres is compatible with base change: the support of g^*α is the inverse image of the support of α along the projection X ×_S S' ⟶ X.

theorem supportOfFamily_baseChangeFamily {X S S' : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (g : S' ⟶ S) (r : ℕ) (α : FamilyOfCycles f r) :
    supportOfFamily (pullback.snd f g) (baseChangeFamily f g r α) =
      pullback.fst f g ⁻¹' supportOfFamily f α

Stacks.Chow.supportOfFamily_flatPullbackFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatPullbackSupport.lean, line 160. The attribute's comment: “flat pullback”.

Stacks Project, Tag 0H4V, the flat pullback clause. Taking the support of a family of cycles on the fibres is compatible with flat pullback: the support of j^*α is the inverse image of the support of α along j.

theorem supportOfFamily_flatPullbackFamily {X S U : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (fU : U ⟶ S) (j : U ⟶ X) [LocallyOfFiniteType j] [Flat j]
    (hj : j ≫ f = fU) (e : ℕ) (he : AlgebraicGeometry.RelativeDimension j e) (r : ℕ)
    (α : FamilyOfCycles f r) :
    letI : LocallyOfFiniteType fU := hj ▸ (inferInstance : LocallyOfFiniteType (j ≫ f))
    supportOfFamily fU (flatPullbackFamily f fU j hj e he r α) = j ⁻¹' supportOfFamily f α

Stacks.Chow.image_supportOfFamily_restrictedFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/RestrictionSupport.lean, line 47. The attribute's comment: “support_restriction”.

The support of a restricted family of cycles, mapped back into the original total space, is the intersection of the original support with the open subscheme.

theorem image_supportOfFamily_restrictedFamily
    {X S U V : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] (fU : U ⟶ V)
    (j : U ⟶ X) [IsOpenImmersion j] (i : V ⟶ S) [IsOpenImmersion i]
    (h : j ≫ f = fU ≫ i) (r : ℕ) (α : FamilyOfCycles f r) :
    letI : LocallyOfFiniteType fU := by
      let : LocallyOfFiniteType (fU ≫ i) := h ▸ inferInstance
      exact locallyOfFiniteType_of_comp fU i
    j '' (supportOfFamily fU (restrictedFamily f fU j i h r α).1) =
      Set.range j ∩ supportOfFamily f α

Tag 0H4W, a lemma

Tag 0H4W in the Stacks Project.

AlgebraicGeometry.exists_preimage_preserving_residueField_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/TrdegLift.lean, line 98. The attribute's comment: “part (1)”. References: SGA 2 XIV (2.1.1), “special case”.

Let f : X ⟶ S be locally of finite type, let g : S' ⟶ S be surjective and let f' : X' ⟶ S' be the base change of f. A point x : X whose residue field has transcendence degree r over the residue field of f x has a preimage in X' whose residue field has transcendence degree r over the residue field of its image in S'.

public theorem exists_preimage_preserving_residueField_trdeg {p : X' ⟶ X} {f' : X' ⟶ S'}
    {f : X ⟶ S} {g : S' ⟶ S} (hpb : IsPullback p f' f g) [LocallyOfFiniteType f] [Surjective g]
    (r : ℕ) (x : X)
    (hr : letI := (f.residueFieldMap x).hom.toAlgebra
      Algebra.trdeg ↥(S.residueField (f x)) ↥(X.residueField x) = r) :
    ∃ (x' : X') (_hx : p x' = x),
      letI := (f'.residueFieldMap x').hom.toAlgebra
      Algebra.trdeg ↥(S'.residueField (f' x')) ↥(X'.residueField x') = r

AlgebraicGeometry.exists_common_preimage_preserving_residueField_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimensionBaseChange/TrdegLift.lean, line 260. The attribute's comment: “part (2)”.

In the situation of AlgebraicGeometry.exists_preimage_preserving_residueField_trdeg, let S'' be the self-intersection S' ×_S S' of the base change, with projections q₁ and q₂, and let f'' : X'' ⟶ S'' be the base change of f to S'', with projections p₁ and p₂ to X' exhibiting X'' as X' ×_X X'. Two preimages x₁' and x₂' of x of the same relative transcendence degree r are the two images of a point of X'' whose residue field again has transcendence degree r over the residue field of its image in S''.

public theorem exists_common_preimage_preserving_residueField_trdeg {p : X' ⟶ X} {f' : X' ⟶ S'}
    {f : X ⟶ S} {g : S' ⟶ S} {q₁ q₂ : S'' ⟶ S'} {p₁ p₂ : X'' ⟶ X'} {f'' : X'' ⟶ S''}
    (hX' : IsPullback p f' f g) (hS'' : IsPullback q₁ q₂ g g)
    (hX''₁ : IsPullback p₁ f'' f' q₁) (hX''₂ : IsPullback p₂ f'' f' q₂)
    (hXX : IsPullback p₁ p₂ p p) [LocallyOfFiniteType f] (r : ℕ) (x : X) (x₁' x₂' : X')
    (hr : letI := (f.residueFieldMap x).hom.toAlgebra
      Algebra.trdeg ↥(S.residueField (f x)) ↥(X.residueField x) = r)
    (hx₁ : p x₁' = x) (hx₂ : p x₂' = x)
    (hr₁ : letI := (f'.residueFieldMap x₁').hom.toAlgebra
      Algebra.trdeg ↥(S'.residueField (f' x₁')) ↥(X'.residueField x₁') = r)
    (hr₂ : letI := (f'.residueFieldMap x₂').hom.toAlgebra
      Algebra.trdeg ↥(S'.residueField (f' x₂')) ↥(X'.residueField x₂') = r) :
    ∃ x'' : X'', p₁ x'' = x₁' ∧ p₂ x'' = x₂' ∧
      (letI := (f''.residueFieldMap x'').hom.toAlgebra
       Algebra.trdeg ↥(S''.residueField (f'' x'')) ↥(X''.residueField x'') = r)

Tag 0H4X, a lemma

Tag 0H4X in the Stacks Project.

Stacks.Chow.baseChangeFamily_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/BaseChange.lean, line 729. The attribute's comment: “injectivity of base change on families of cycles on fibres”.

Base change of families of r-cycles on the fibres of X / S along a surjective morphism g : S' ⟶ S is injective: if g^*α₁ = g^*α₂ then α₁ = α₂.

theorem baseChangeFamily_injective (f : X ⟶ S) [LocallyOfFiniteType f] (g : S' ⟶ S)
    [Surjective g] (r : ℕ) (α₁ α₂ : FamilyOfCycles f r)
    (h : baseChangeFamily f g r α₁ = baseChangeFamily f g r α₂) :
    α₁ = α₂

Stacks.Chow.existsUnique_familyOfCycles_baseChangeFamily_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Descent.lean, line 485. The attribute's comment: “descent of a family of cycles on fibres along a morphism with separable residue field extensions”.

Stacks Project, Tag 0H4X (2). Let f : X ⟶ S be locally of finite type, let r ≥ 0, let g : S' ⟶ S be a morphism such that every point of S has a preimage in S' whose residue field extension is separable, and let X' = X ×_S S'. Given a family α' of r-cycles on the fibres of X' / S' whose two pullbacks to the double overlap S'' = S' ×_S S' agree as families of r-cycles on the fibres of S'' ×_S X / S'', there is a unique family α of r-cycles on the fibres of X / S with g^*α = α'.

theorem existsUnique_familyOfCycles_baseChangeFamily_eq (f : X ⟶ S) [LocallyOfFiniteType f]
    (g : S' ⟶ S) (hg : HasSeparableResidueFieldPoints g) (r : ℕ)
    (α' : FamilyOfCycles (pullback.snd f g) r)
    (hα' : ∀ (t : (pullback g g : Scheme.{u}))
      (x : (pullback.snd (pullback.snd f g) (pullback.fst g g)).fiber t),
      (baseChangeFamily (pullback.snd f g) (pullback.fst g g) r α' t :
          AlgebraicCycle ((pullback.snd (pullback.snd f g) (pullback.fst g g)).fiber t) ℤ) x =
        (baseChangeFamily (pullback.snd f g) (pullback.snd g g) r α' t :
            AlgebraicCycle ((pullback.snd (pullback.snd f g) (pullback.snd g g)).fiber t) ℤ)
          ((overlapFiberComparison f g t).hom x)) :
    ∃! α : FamilyOfCycles f r, baseChangeFamily f g r α = α'

Tag 0H4Y, a lemma

Tag 0H4Y in the Stacks Project.

Stacks.Chow.baseChangeFamilyOfCyclesAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/BaseChange.lean, line 291. The attribute's comment: “the additive equivalence”.

Base change along a morphism that is bijective on points and induces isomorphisms of residue fields identifies the groups of families of cycles on the fibres.

def baseChangeFamilyOfCyclesAddEquiv
    {X S S' : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (g : S' ⟶ S) (hg : Function.Bijective g)
    (hres : ∀ t : S', IsIso (g.residueFieldMap t)) (r : ℕ) :
    FamilyOfCycles f r ≃+ FamilyOfCycles (pullback.snd f g) r

Stacks.Chow.baseChangeFamilyOfCyclesAddEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/BaseChange.lean, line 302. The attribute's comment: “the coefficient formula”.

The base-changed family has, on each fibre, the coefficients of the original family transported along the canonical map of fibres.

theorem baseChangeFamilyOfCyclesAddEquiv_apply
    {X S S' : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (g : S' ⟶ S) (hg : Function.Bijective g)
    (hres : ∀ t : S', IsIso (g.residueFieldMap t)) (r : ℕ)
    (α : FamilyOfCycles f r) (t : S') (x : (pullback.snd f g).fiber t) :
    ((baseChangeFamilyOfCyclesAddEquiv f g hg hres r α) t :
      AlgebraicCycle ((pullback.snd f g).fiber t) ℤ) x =
        (α (g t) : AlgebraicCycle (f.fiber (g t)) ℤ)
          (restrictedFiberMap f (pullback.snd f g) (pullback.fst f g) g
            pullback.condition t x)

Sources

• Section 62.5, Tag 0H4N
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.flatPullbackFamily · Stacks.Chow.baseChangeFamily_baseChangeFamily_comp · Stacks.Chow.restrictedFamily_eq_flatPullbackFamily_baseChangeFamily · Stacks.Chow.baseChangeFamily_flatPullbackFamily · Stacks.Chow.flatPullbackFamily_flatPullbackFamily · Stacks.Chow.baseChangeFamily_properPushforwardFamily_of_isProper · Stacks.Chow.properPushforwardFamily_properPushforwardFamily · Stacks.Chow.flatPullbackFamily_properPushforwardFamily

Section62.6 Relative cycles#

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

Tag 0H50, a definition

Tag 0H50 in the Stacks Project.

Stacks.Chow.IsRelativeCycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Relative.lean, line 53. The attribute's comment: “relative r-cycles”.

A family α of r-cycles on the fibres of X/S is a relative r-cycle when for every discrete valuation ring R and every morphism g : Spec R ⟶ S the specialization of the generic member of the base change g^*α is its closed member: sp_{X'/S'}(α_η) = α_0.

def IsRelativeCycle {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (r : ℕ) (α : FamilyOfCycles f r) : Prop

Stacks.Chow.relativeCycles, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Relative.lean, line 88. The attribute's comment: “the group z(X/S, r)”.

The group z(X/S, r) of relative r-cycles on X/S: the subgroup of the group of families of r-cycles on the fibres of X/S cut out by the valuative condition.

def relativeCycles {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (r : ℕ) : AddSubgroup (FamilyOfCycles f r)

Tag 0H51, a lemma

Tag 0H51 in the Stacks Project.

Stacks.Chow.isRelativeCycle_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/BaseChangeRelative.lean, line 91. The attribute's comment: “base change along an arbitrary morphism of locally Noetherian bases”.

Stacks Project, Lemma 0H51, the base change clause. The base change of a relative r-cycle along an arbitrary morphism g : S' ⟶ S of locally Noetherian schemes is a relative r-cycle on X ×_S S' over S'.

theorem isRelativeCycle_baseChangeFamily {X S S' : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] [IsLocallyNoetherian S'] (g : S' ⟶ S)
    (r : ℕ) {α : FamilyOfCycles f r} (hα : IsRelativeCycle f r α) :
    IsRelativeCycle (pullback.snd f g) r (baseChangeFamily f g r α)

Stacks.Chow.isRelativeCycle_flatPullbackFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatPullbackDescent.lean, line 237. The attribute's comment: “flat pullback along a flat morphism of relative dimension e”.

Stacks Project, Lemma 0H51, the flat pullback clause. Let f : X ⟶ S be locally of finite type with S locally Noetherian and let j : U ⟶ X be a flat morphism, locally of finite type and of relative dimension e, with j ≫ f = f_U. Then the flat pullback j^*α of a relative r-cycle α on X/S is a relative (r + e)-cycle on U/S.

The valuative condition for j^*α at a morphism g : Spec R ⟶ S from the spectrum of a discrete valuation ring is the valuative condition for α at g, pulled back along the base change of j: base change of the base scheme commutes with flat pullback by Lemma 0H4P part (3), Stacks.Chow.baseChangeFamily_flatPullbackFamily, and specialization commutes with flat pullback by Lemma 0H4L, Stacks.Chow.specializationCycle_baseChangedFiberCycleFlatPullback.

No surjectivity is involved; this is the single-morphism statement whose family form is the forward direction of Stacks.Chow.isRelativeCycle_iff_forall_flatPullbackFamily below.

theorem isRelativeCycle_flatPullbackFamily {X S U : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (fU : U ⟶ S) [LocallyOfFiniteType fU]
    (j : U ⟶ X) [LocallyOfFiniteType j] [Flat j] (hj : j ≫ f = fU) (e : ℕ)
    (he : AlgebraicGeometry.RelativeDimension j e) (r : ℕ) {α : FamilyOfCycles f r}
    (hα : IsRelativeCycle f r α) :
    IsRelativeCycle fU (r + e) (flatPullbackFamily f fU j hj e he r α)

Stacks.Chow.isRelativeCycle_restrictedFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/GysinAction.lean, line 169. The attribute's comment: “restriction to open subschemes of the source and of the base”.

Stacks Project, Lemma 0H51, restriction to open subschemes of the source and of the base. For open immersions j : U ⟶ X and i : V ⟶ S with j ≫ f = fU ≫ i, the restriction to U/V of a relative r-cycle on X/S is a relative r-cycle.

The restriction is the base change along i, restricted along the open immersion U ⟶ X ×_S V over V: the base change along an open immersion changes no coefficient, the residue fields being equal, and the fibre maps factor through the fibres of X ×_S V (Stacks.Chow.fiberRestrict_pullbackLift_comp_restrictedFiberMap). Both operations preserve relative cycles.

theorem isRelativeCycle_restrictedFamily {X S U V : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (fU : U ⟶ V) [LocallyOfFiniteType fU]
    (j : U ⟶ X) [IsOpenImmersion j] (i : V ⟶ S) [IsOpenImmersion i] (h : j ≫ f = fU ≫ i)
    (r : ℕ) {α : FamilyOfCycles f r} (hα : IsRelativeCycle f r α) :
    letI : IsLocallyNoetherian V := isLocallyNoetherian_of_isOpenImmersion i
    IsRelativeCycle fU r (restrictedFamily f fU j i h r α).1

Stacks.Chow.isRelativeCycle_properPushforwardFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ProperPushforwardRelative.lean, line 40. The attribute's comment: “proper pushforward”.

Let S be locally Noetherian, let sX : X ⟶ S and sY : Y ⟶ S be locally of finite type, let q : X ⟶ Y be proper with q ≫ sY = sX and let r ≥ 0. The proper pushforward q_*α of a relative r-cycle α on X/S is a relative r-cycle on Y/S.

theorem isRelativeCycle_properPushforwardFamily {X Y S : Scheme.{u}} (sX : X ⟶ S)
    [LocallyOfFiniteType sX] (sY : Y ⟶ S) [LocallyOfFiniteType sY] [IsLocallyNoetherian S]
    (q : X ⟶ Y) [IsProper q] (hq : q ≫ sY = sX) (r : ℕ) {α : FamilyOfCycles sX r}
    (hα : IsRelativeCycle sX r α) :
    IsRelativeCycle sY r (properPushforwardFamily sX sY q hq r α)

Stacks.Chow.isRelativeCycle_fiberCycleRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SpecializationRestriction.lean, line 447. The attribute's comment: “restriction along an open immersion of the source”.

The restriction of a relative r-cycle on X/S to an open subscheme U ⊆ X, taken over the same base, is a relative r-cycle on U/S.

theorem isRelativeCycle_fiberCycleRestrict {X S U : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (fU : U ⟶ S) [LocallyOfFiniteType fU]
    (j : U ⟶ X) [IsOpenImmersion j] (h : j ≫ f = fU) (r : ℕ) {α : FamilyOfCycles f r}
    (hα : IsRelativeCycle f r α) :
    IsRelativeCycle fU r (fun s => fiberCycleRestrict f fU j h s r (α s))

Tag 0H52, a lemma

Tag 0H52 in the Stacks Project.

Stacks.Chow.isRelativeCycle_iff_forall_isRelativeCycle_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/HDescent.lean, line 497.

Stacks Project, Lemma 0H52. Let S be locally Noetherian, let f : X ⟶ S be locally of finite type, let r ≥ 0 and let α be a family of r-cycles on the fibres of X/S. Let {g i : S' i ⟶ S} be an h covering. Then α is a relative r-cycle if and only if each base change (g i)^*α is a relative r-cycle.

This is Stacks.Chow.isRelativeCycle_iff_forall_baseChangeFamily with its two inputs supplied: the two-step base change compatibility by Stacks.Chow.specializationCycle_baseChangeFamily_baseChangeFamily_iff and the descent along an extension of discrete valuation rings by Stacks.Chow.specializationCycle_baseChangeFamily_of_isExtension.

theorem isRelativeCycle_iff_forall_isRelativeCycle_baseChangeFamily {X S : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFiniteType f] [IsLocallyNoetherian S] (r : ℕ) (α : FamilyOfCycles f r)
    {I : Type v} (S' : I → Scheme.{u}) (g : ∀ i, S' i ⟶ S) (hg : IsHCovering S' g) :
    IsRelativeCycle f r α ↔
      ∀ i, @IsRelativeCycle _ _ (pullback.snd f (g i)) _ (hg.isLocallyNoetherian i) r
        (baseChangeFamily f (g i) r α)

Tag 0H53, a lemma

Tag 0H53 in the Stacks Project.

Stacks.Chow.isRelativeCycle_iff_forall_flatPullbackFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatPullbackDescent.lean, line 265. The attribute's comment: “both directions, for a jointly surjective family of flat morphisms of relative dimension e”.

Stacks Project, Lemma 0H53. Let f : X ⟶ S be a morphism of schemes with S locally Noetherian and f locally of finite type, let r, e ≥ 0 and let α be a family of r-cycles on the fibres of X/S. Let {f_i : X_i ⟶ X} be a jointly surjective family of flat morphisms, locally of finite type and of relative dimension e. Then α is a relative r-cycle if and only if every flat pullback f_i^*α is a relative (r+e)-cycle.

The proof is the one in the source. Both directions are read off after base change to the spectrum of a discrete valuation ring: there the valuative identity for f_i^*α is the identity sp(f_{i,η}^*α_η) = f_{i,0}^*α_0, and base change of a flat pullback (Stacks.Chow.baseChangeFamily_flatPullbackFamily_apply, Lemma 0H4P part (3)) with the commutation of specialization and flat pullback (Stacks.Chow.specializationCycle_baseChangedFiberCycleFlatPullback, Lemma 0H4L) turns it into f_{i,0}^*(sp(α_η)) = f_{i,0}^*α_0. That is implied by the valuative identity for α, which gives the forward direction, and implies it because the f_{i,0}^* are jointly injective by Stacks.Chow.eq_of_forall_baseChangedFiberCycleFlatPullback, which gives the converse.

theorem isRelativeCycle_iff_forall_flatPullbackFamily {Idx : Type v} {X S : Scheme.{u}}
    {Y : Idx → Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] [IsLocallyNoetherian S]
    (p : ∀ i, Y i ⟶ X) [∀ i, LocallyOfFiniteType (p i)] [∀ i, Flat (p i)]
    (fY : ∀ i, Y i ⟶ S) [∀ i, LocallyOfFiniteType (fY i)] (hY : ∀ i, p i ≫ f = fY i) (e : ℕ)
    (he : ∀ i, AlgebraicGeometry.RelativeDimension (p i) e)
    (hsurj : ∀ x : X, ∃ i, ∃ y : Y i, (p i).base y = x) (r : ℕ) (α : FamilyOfCycles f r) :
    IsRelativeCycle f r α ↔
      ∀ i, IsRelativeCycle (fY i) (r + e)
        (flatPullbackFamily f (fY i) (p i) (hY i) e (he i) r α)

Tag 0H54, a lemma

Tag 0H54 in the Stacks Project.

Stacks.Chow.isRelativeCycle_iff_isRelativeCycle_properPushforwardFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedImmersion.lean, line 530.

Let S be a locally Noetherian scheme, let i : X ⟶ Y be a closed immersion of schemes locally of finite type over S, let r ≥ 0 and let α be a family of r-cycles on the fibres of X/S. Then α is a relative r-cycle on X/S if and only if i_*α is a relative r-cycle on Y/S.

theorem isRelativeCycle_iff_isRelativeCycle_properPushforwardFamily [IsLocallyNoetherian S]
    (α : FamilyOfCycles sX r) :
    IsRelativeCycle sX r α ↔
      IsRelativeCycle sY r (properPushforwardFamily sX sY i hi r α)

Tag 0H55, a lemma

Tag 0H55 in the Stacks Project.

Stacks.Chow.IsRelativeCycle.eq_iff_eq_of_mem_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/GenericFibres.lean, line 111.

Stacks Project, Lemma 0H55. Let S be a locally Noetherian scheme, let f : X ⟶ S be locally of finite type and let r ≥ 0. Two relative r-cycles on X/S are equal if and only if their members over the generic points of the irreducible components of S agree.

theorem IsRelativeCycle.eq_iff_eq_of_mem_genericPoints {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (r : ℕ) {α β : FamilyOfCycles f r}
    (hα : IsRelativeCycle f r α) (hβ : IsRelativeCycle f r β) :
    α = β ↔ ∀ η ∈ genericPoints ↥S, α η = β η

Tag 0H56, a lemma

Tag 0H56 in the Stacks Project.

Stacks.Chow.isRelativeCycle_familyAssociatedToModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatCycleClasses.lean, line 125. The attribute's comment: “the source's hypothesis that the module is flat over the base in dimensions at least r, Stacks Definition 0CWG, written out as the dimension bound on the non-flat locus”.

Stacks Project, Lemma 0H56. Let S be locally Noetherian, let f : X ⟶ S be locally of finite type and let F be a quasi-coherent 𝒪_X-module of finite type whose fibrewise support has dimension at most r. If F is flat over S in dimensions ≥ r, then [F/X/S]_r is a relative r-cycle on X/S.

Flatness over S in dimensions ≥ r is spelled out as Stacks Definition 0CWG defines it: for every point s of S the locus in the fibre X_s where F fails to be flat over S has dimension less than r.

theorem isRelativeCycle_familyAssociatedToModule {r : ℕ} {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (F : X.Modules) [F.IsFiniteType]
    [F.IsQuasicoherent]
    (hF : ∀ s : S, topologicalKrullDim
      ↥{y : f.fiber s | ¬ IsFlatOverAt f.toLRSHom.toShHom F (f.fiberι s y)} < (r : WithBot ℕ∞))
    (hdim : FiberSupportDimensionLE f F r) :
    IsRelativeCycle f r (familyAssociatedToModule f F r hdim)

Tag 0H57, a lemma

Tag 0H57 in the Stacks Project.

Stacks.Chow.isRelativeCycle_familyAssociatedToClosedSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatCycleClasses.lean, line 158. The attribute's comment: “the source's hypothesis that the structure sheaf is flat over the base in dimensions at least r, Stacks Definition 0CWG, written out as the dimension bound on the non-flat locus”.

Stacks Project, Lemma 0H57. Let S be locally Noetherian, let f : X ⟶ S be locally of finite type and let i : Z ⟶ X be a closed immersion. If the structure sheaf of Z, viewed on X, is flat over S in dimensions ≥ r and its fibrewise support has dimension at most r, then [Z/X/S]_r is a relative r-cycle on X/S.

This is the proof of the source: the cycle of a closed subscheme is the cycle of its structure sheaf by Tag 02QY, so Tag 0H56 applies to the direct image of that structure sheaf.

Flatness over S in dimensions ≥ r is spelled out as Stacks Definition 0CWG defines it: for every point s of S the locus in the fibre X_s where i_* 𝒪_Z fails to be flat over S has dimension less than r.

theorem isRelativeCycle_familyAssociatedToClosedSubscheme {r : ℕ} {X S Z : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFiniteType f] [IsLocallyNoetherian S] (i : Z ⟶ X)
    [IsClosedImmersion i] [(structureSheafPushforward i).IsFiniteType]
    [(structureSheafPushforward i).IsQuasicoherent]
    (hZ : ∀ s : S, topologicalKrullDim
      ↥{y : f.fiber s | ¬ IsFlatOverAt f.toLRSHom.toShHom (structureSheafPushforward i)
        (f.fiberι s y)} < (r : WithBot ℕ∞))
    (hdim : FiberSupportDimensionLE f (structureSheafPushforward i) r) :
    IsRelativeCycle f r (familyAssociatedToModule f (structureSheafPushforward i) r hdim)

Tag 0H58, an equation

Tag 0H58 in the Stacks Project.

Stacks.Chow.relativeCycleClassMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatCycleClasses.lean, line 350. The attribute's comment: “the homomorphism into z(X/S, r)”.

Stacks Project, Equation 0H58. Let S be locally Noetherian, let f : X ⟶ S be locally of finite type and let r ≥ 0. The cycle-class homomorphism from the free abelian group on Hilb(X/S, r) to the group z(X/S, r) of relative r-cycles on X/S, sending ∑ nᵢ [Zᵢ] to ∑ nᵢ [Zᵢ/X/S]_r. It refines the homomorphism of Tag 0H6V, whose values are families of r-cycles on fibres, by cutting its codomain down to the relative cycles: each [Zᵢ/X/S]_r is a relative r-cycle by Lemma 0H57.

The source takes f of finite type; quasi-compactness of f is not needed, so it is not assumed. Under the source's hypotheses the members of Hilb(X/S, r) are exactly the closed subschemes flat and of relative dimension at most r over S, by Stacks.Chow.HilbertCycleDatum.ofFlat.

def relativeCycleClassMap {r : ℕ} {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] :
    FreeAbelianGroup (HilbertCycleDatum f r) →+ relativeCycles f r

Stacks.Chow.relativeCycleClassMap_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatCycleClasses.lean, line 358. The attribute's comment: “on generators”.

Stacks Project, Equation 0H58. On a generator the cycle-class homomorphism into z(X/S, r) is the family of cycles [Z/X/S]_r of the closed subscheme.

theorem relativeCycleClassMap_of {r : ℕ} {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (Z : HilbertCycleDatum f r) :
    (relativeCycleClassMap f (FreeAbelianGroup.of Z)).1 = Z.cycleFamily f

Stacks.Chow.relativeCycleClassMap_val, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/FlatCycleClasses.lean, line 367. The attribute's comment: “compatibility with the homomorphism of Tag 0H6V”.

Stacks Project, Equation 0H58. The cycle-class homomorphism into z(X/S, r) is the homomorphism of Tag 0H6V followed by the inclusion of the relative cycles into the families of r-cycles on fibres.

theorem relativeCycleClassMap_val {r : ℕ} {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S]
    (α : FreeAbelianGroup (HilbertCycleDatum f r)) :
    (relativeCycleClassMap f α).1 = cycleClassMap f r α

Tag 0H59, a lemma

Tag 0H59 in the Stacks Project.

Stacks.Chow.exists_isProper_isCompletelyDecomposed_relativeCycleClassMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/CycleClassProperCover.lean, line 485.

Let f : X ⟶ S be a finite type morphism of schemes with S Noetherian, let r ≥ 0 and let α be a relative r-cycle on X/S. Then there is a proper, completely decomposed (Definition 0GTI) morphism g : S' ⟶ S from a Noetherian scheme S' such that g^*α is in the image of the cycle class map FreeAbelianGroup (Hilb(X ×_S S' / S', r)) ⟶ z(X ×_S S' / S', r) of Equation 0H58.

theorem exists_isProper_isCompletelyDecomposed_relativeCycleClassMap_eq {X S : Scheme.{u}}
    [IsNoetherian S] (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f] (r : ℕ)
    (α : relativeCycles f r) :
    ∃ (S' : Scheme.{u}) (g : S' ⟶ S) (_ : IsNoetherian S'), IsProper g ∧
      IsCompletelyDecomposed g ∧
      ∃ c : FreeAbelianGroup (HilbertCycleDatum (pullback.snd f g) r),
        (relativeCycleClassMap (pullback.snd f g) c : FamilyOfCycles (pullback.snd f g) r) =
          baseChangeFamily f g r α

Tag 0H5A, a lemma

Tag 0H5A in the Stacks Project.

Stacks.Chow.surjective_relativeCycleClassMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/DvrCycleClasses.lean, line 515. The attribute's comment: “finite type is the source's hypothesis, stated as locally of finite type plus quasi-compact”.

Stacks Project, Lemma 0H5A. Let f : X ⟶ Spec R be a morphism of finite type with R a discrete valuation ring and let r ≥ 0. Then the cycle-class homomorphism of Equation 0H58 is surjective: every relative r-cycle on X/Spec R is a combination of the classes [Z/X/S]_r of members of Hilb(X/Spec R, r).

A relative r-cycle is determined by its member over the generic point of Spec R by Tag 0H55, and that member is the generic member of a cycle class by Stacks.Chow.exists_cycleClassMap_apply_genericPoint_eq.

theorem surjective_relativeCycleClassMap {r : ℕ} {R : Type u} [CommRing R] [IsDomain R]
    [IsDiscreteValuationRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [LocallyOfFiniteType f]
    [QuasiCompact f] :
    Function.Surjective (relativeCycleClassMap (r := r) f)

Tag 0H5B, a lemma

Tag 0H5B in the Stacks Project.

Stacks.Chow.isClopen_supportOfFamily_of_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SmoothSupportClopen.lean, line 290. The attribute's comment: “the support is clopen once membership is invariant along specializations”.

Stacks Project, Lemma 0H5B, reduction step. The support of a family of r-cycles on the fibres of a morphism locally of finite type over a locally Noetherian base is open and closed in the total space as soon as membership in it is unchanged along every specialization of points of the total space.

This is the step of the source which replaces local constancy of the coefficient function x ↦ n_x by its invariance along specializations: the total space is locally Noetherian, being locally of finite type over a locally Noetherian base, and on a locally Noetherian scheme a subset invariant along specializations is open and closed.

theorem isClopen_supportOfFamily_of_specializes {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] {r : ℕ} (α : FamilyOfCycles f r)
    (hα : ∀ x y : X, x ⤳ y → (x ∈ supportOfFamily f α ↔ y ∈ supportOfFamily f α)) :
    IsClopen (supportOfFamily f α)

Stacks.Chow.isClopen_irreducibleComponent_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SmoothSupportClopen.lean, line 347. The attribute's comment: “components of a smooth scheme over a field are open and closed”. References: SGA 7 VIII (5.2), “special case”.

Stacks Project, Lemma 0H5B, geometric step. On a scheme smooth over a field every irreducible component is open and closed, so it is an open subscheme and is itself smooth over the field. This is what makes the unique component of a smooth fibre through a point reduced after any extension of the base field.

theorem isClopen_irreducibleComponent_of_smooth {k : Type u} [Field k] {Y : Scheme.{u}}
    (p : Y ⟶ Spec (.of k)) [Smooth p] (y : Y) : IsClopen (irreducibleComponent y)

Stacks.Chow.isLocallyConstant_of_specializes_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SmoothSupportClopen.lean, line 363. The attribute's comment: “the reduction of local constancy of the fibrewise coefficient function to its invariance along specializations; not that invariance itself”.

Stacks Project, Lemma 0H5B, topological reduction for a function. A function on a quasi-sober locally Noetherian space whose value is unchanged along every specialization is locally constant: membership in each of its fibres is unchanged along specializations, hence each fibre is open.

This is the sentence of the source which replaces local constancy of the coefficient function x ↦ n_x by the implication x' ⤳ x → n_{x'} = n_x.

theorem isLocallyConstant_of_specializes_eq {A : Type u} [TopologicalSpace A] [QuasiSober A]
    {β : Type*} (hA : IsLocallyNoetherianSpace A) {n : A → β}
    (hn : ∀ x y : A, x ⤳ y → n x = n y) : IsLocallyConstant n

Stacks.Chow.isClopen_tsupport_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SmoothSupportClopen.lean, line 450. The attribute's comment: “the support of a cycle of top relative dimension on a scheme smooth over a field is open and closed; neither the statement over a general base nor local constancy of the fibrewise coefficient function”.

Stacks Project, Lemma 0H5B over the spectrum of a field. The support of a cycle of relative dimension k on a scheme smooth over a field is open and closed, provided every generic point of an irreducible component has relative dimension k; that proviso is what being smooth of relative dimension k supplies.

Such a cycle is supported on generic points of irreducible components, and on a scheme smooth over a field the closure of a set of such points is a union of connected components.

theorem isClopen_tsupport_of_smooth {k : Type u} [Field k] {Y : Scheme.{u}}
    (p : Y ⟶ Spec (.of k)) [Smooth p] (j : ℤ)
    (hgen : ∀ ξ ∈ genericPoints ↥Y,
      relativeDimension (fieldChowSituation k).dimensionFunction p ξ = j)
    (c : CycleGroup (fieldChowSituation k) p j) :
    IsClopen (tsupport (c.1 : AlgebraicCycle Y ℤ))

Stacks.Chow.isClopen_supportOfFamily_of_smoothOfRelativeDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SmoothSupportSpecialization.lean, line 541.

Stacks Project, Lemma 0H5B. Let S be a locally Noetherian scheme, let f : X ⟶ S be smooth of relative dimension r and let α be a relative r-cycle on X/S. Then the support of α is open and closed in X.

By the reduction step it suffices to know that membership in the support is unchanged along every specialization x ⤳ y of points of X. Such a specialization is realized by the generic-to-closed specialization on the spectrum of a discrete valuation ring R mapping to X, and the base change X ×_S Spec R ⟶ Spec R — again smooth of relative dimension r — carries a section through which the two points are seen. The valuative condition applies there, and compatibility of supports with base change transports the conclusion back to X.

theorem isClopen_supportOfFamily_of_smoothOfRelativeDimension {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (r : ℕ) [SmoothOfRelativeDimension r f]
    (α : FamilyOfCycles f r) (hα : IsRelativeCycle f r α) :
    IsClopen (supportOfFamily f α)

Tag 0H5C, a lemma

Tag 0H5C in the Stacks Project.

Stacks.Chow.isClosed_setOf_fiberCycle_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EqualityLocus.lean, line 576.

Stacks Project, Lemma 0H5C. Let f : X ⟶ S be a morphism of schemes with S locally Noetherian and f locally of finite type, let r ≥ 0 and let α, β ∈ z(X/S, r). Then the set E = {s ∈ S : α_s = β_s} is closed in S.

With γ = α - β, the set E is the vanishing locus of the relative cycle γ. It is stable under specialization, and every point η ∉ E has an open neighbourhood containing no point of E specializing from η (Stacks.Chow.exists_isOpen_forall_specializes_ne_zero); on a locally Noetherian space these two properties make E closed.

theorem isClosed_setOf_fiberCycle_eq {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] {r : ℕ} (α β : relativeCycles f r) :
    IsClosed {s : S | (α : FamilyOfCycles f r) s = (β : FamilyOfCycles f r) s}

Tag 0H5D, a lemma

Tag 0H5D in the Stacks Project.

Stacks.Chow.nonempty_isColimit_relativeCyclesCocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/LimitColimit.lean, line 234.

Stacks Project, Lemma 0H5D. Let S = lim_{i ∈ I} S_i be the limit of a cofiltered system of Noetherian schemes with affine transition morphisms, let i₀ ∈ I and let X₀ ⟶ S_{i₀} be of finite type; for a stage a ≥ i₀ put X_a = X₀ ×_{S_{i₀}} S_a, and put X = X₀ ×_{S_{i₀}} S. If S is Noetherian, then z(X/S, r) = colim_{a ≥ i₀} z(X_a/S_a, r), the transition maps being base change of relative r-cycles: the cocone Stacks.Chow.relativeCyclesCocone of base changes along the projections S ⟶ S_a is a colimit in the category of abelian groups.

theorem nonempty_isColimit_relativeCyclesCocone {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u}) [∀ {i j : I} (v : i ⟶ j), IsAffineHom (D.map v)]
    [∀ i, IsNoetherian (D.obj i)] (c : Cone D) (hc : IsLimit c) [IsNoetherian c.pt] {i₀ : I}
    {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ D.obj i₀) [LocallyOfFiniteType f₀] [QuasiCompact f₀] (r : ℕ) :
    Nonempty (IsColimit (relativeCyclesCocone D c f₀ r))

Tag 0H5E, a lemma

Tag 0H5E in the Stacks Project.

Stacks.Chow.relativeCyclesAddEquivOfIsThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedImmersion.lean, line 656. The attribute's comment: “the bijection i_* : z(X/S, r) → z(X'/S, r) of relative r-cycles”.

Let S be a locally Noetherian scheme and let i : X ⟶ Y be a thickening of schemes locally of finite type over S. For r ≥ 0 proper pushforward along i is an additive equivalence z(X/S, r) ≃ z(Y/S, r) of groups of relative r-cycles.

def relativeCyclesAddEquivOfIsThickening (hthick : Stacks.Thickenings.IsThickening i) (r : ℕ) :
    ↥(relativeCycles sX r) ≃+ ↥(relativeCycles sY r)

Stacks.Chow.relativeCyclesAddEquivOfIsThickening_coe, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedImmersion.lean, line 676. The attribute's comment: “the equivalence is the fibrewise proper pushforward of families of cycles”.

The additive equivalence of relative r-cycles attached to a thickening is proper pushforward: the family of fibrewise cycles underlying the image of α is the fibrewise proper pushforward of the family underlying α.

theorem relativeCyclesAddEquivOfIsThickening_coe
    (hthick : Stacks.Thickenings.IsThickening i) (r : ℕ) (α : ↥(relativeCycles sX r)) :
    (relativeCyclesAddEquivOfIsThickening sX sY i hi hthick r α).1 =
      properPushforwardFamily sX sY i hi r α.1

Tag 0H5F, a lemma

Tag 0H5F in the Stacks Project.

Stacks.Chow.relativeCyclesRestrictEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/RestrictionBijection.lean, line 461. The attribute's comment: “restriction is a bijection z(X/S, r) → z(U/S, r)”.

Stacks Project, Lemma 0H5F. Let S be a locally Noetherian scheme, let X be a scheme locally of finite type over S, let r ≥ 0 and let j : U ⟶ X be an open immersion over S such that the complement of U has relative dimension < r over S, that is dim(X_s \ U_s) < r for all s ∈ S. Then restriction is a bijection z(X/S, r) ⟶ z(U/S, r).

The inverse is extension by zero, not a chosen section: fibrewise, the cycle on X_s keeps the coefficients of the cycle on U_s and vanishes off U_s.

def relativeCyclesRestrictEquiv {X S U : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (fU : U ⟶ S) [LocallyOfFiniteType fU] (j : U ⟶ X)
    [IsOpenImmersion j] (h : j ≫ f = fU) (r : ℕ)
    (hdim : ComplementFibreDimensionLT f fU j h r) :
    relativeCycles f r ≃+ relativeCycles fU r

Tag 0H5G, a lemma

Tag 0H5G in the Stacks Project.

Stacks.Chow.relativeCyclesAddEquivOfUniversalHomeomorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/BaseChangeSubintegral.lean, line 363. The attribute's comment: “the bijection z(X/S, r) → z(X'/S', r) determined by base change”.

Stacks Project, Lemma 0H5G. Let g : S' ⟶ S be a universal homeomorphism of locally Noetherian schemes which induces isomorphisms on all residue fields, let f : X ⟶ S be locally of finite type, let X' = S' ×_S X and let r ≥ 0. Base change along g is an additive equivalence z(X/S, r) ≃ z(X'/S', r) of groups of relative r-cycles.

def relativeCyclesAddEquivOfUniversalHomeomorphism
    (hres : ∀ t : S', IsIso (g.residueFieldMap t)) (r : ℕ) :
    ↥(relativeCycles f r) ≃+ ↥(relativeCycles (pullback.snd f g) r)

Stacks.Chow.relativeCyclesAddEquivOfUniversalHomeomorphism_coe, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/BaseChangeSubintegral.lean, line 390. The attribute's comment: “the bijection is base change of families of cycles on fibres”.

Stacks Project, Lemma 0H5G. The additive equivalence of relative r-cycles attached to a universal homeomorphism inducing isomorphisms on all residue fields is base change: the family of fibrewise cycles underlying the image of α is the base change of the family underlying α.

theorem relativeCyclesAddEquivOfUniversalHomeomorphism_coe
    (hres : ∀ t : S', IsIso (g.residueFieldMap t)) (r : ℕ) (α : ↥(relativeCycles f r)) :
    (relativeCyclesAddEquivOfUniversalHomeomorphism f g hres r α).1 =
      baseChangeFamily f g r α.1

Sources

• Section 62.6, Tag 0H4Z
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.IsRelativeCycle · Stacks.Chow.relativeCycles · Stacks.Chow.isRelativeCycle_baseChangeFamily · Stacks.Chow.isRelativeCycle_flatPullbackFamily · Stacks.Chow.isRelativeCycle_restrictedFamily · Stacks.Chow.isRelativeCycle_properPushforwardFamily · Stacks.Chow.isRelativeCycle_fiberCycleRestrict · Stacks.Chow.isRelativeCycle_iff_forall_isRelativeCycle_baseChangeFamily

Section62.7 Equidimensional relative cycles#

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

Tag 0H5I, a definition

Tag 0H5I in the Stacks Project.

Stacks.Chow.IsEquidimensional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EquidimensionalCycles.lean, line 89. The attribute's comment: “the equidimensionality condition”.

A family of r-cycles on the fibres of f is equidimensional when its support is contained in a closed subset of X whose relative dimension over S is at most r.

def IsEquidimensional {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (r : ℕ) (α : FamilyOfCycles f r) : Prop

Stacks.Chow.equidimensionalRelativeCycles, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EquidimensionalCycles.lean, line 461. The attribute's comment: “the group z_equi(X/S, r) of equidimensional relative r-cycles”.

The group z_equi(X/S, r) of equidimensional relative r-cycles on X/S: the subgroup of the group of families of r-cycles on the fibres of X/S whose members are the relative r-cycles whose support is contained in a closed subset of X of relative dimension at most r over S.

def equidimensionalRelativeCycles {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (r : ℕ) : AddSubgroup (FamilyOfCycles f r)

Tag 0H5J, an example

Tag 0H5J in the Stacks Project.

Stacks.Chow.NotEquidimensional.exampleFamily, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NotEquidimensional.lean, line 430. The attribute's comment: “the family of 0-cycles of the example”.

Stacks Project, Tag 0H5J. The family of 0-cycles on the fibres of Spec k[x, y, t] ⟶ Spec k[x, y] of Suslin--Voevodsky's example.

def exampleFamily (k : Type u) [Field k] : FamilyOfCycles (projection k) 0

Stacks.Chow.NotEquidimensional.exampleFamily_of_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NotEquidimensional.lean, line 436. The attribute's comment: “the first clause: the member of the family is zero when b = 0”.

Stacks Project, Tag 0H5J, first clause. The example family vanishes on the fibre over a point where the image of y is zero.

theorem exampleFamily_of_eq_zero (k : Type u) [Field k] (s : baseScheme k)
    (hb : yImage k s = 0) : exampleFamily k s = 0

Stacks.Chow.NotEquidimensional.exampleFamily_of_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NotEquidimensional.lean, line 445. The attribute's comment: “the second clause: the member of the family is [p] - [q] when b is nonzero”.

Stacks Project, Tag 0H5J, second clause. On a fibre where the image b of y is nonzero the member of the example family is the difference [p] - [q] of the κ(s)-rational points at t = a/b and at t = (a + b²)/b.

theorem exampleFamily_of_ne_zero (k : Type u) [Field k] (s : baseScheme k)
    (hb : yImage k s ≠ 0) :
    (exampleFamily k s : AlgebraicCycle ((projection k).fiber s) ℤ) =
      twoPointCycle (firstPoint k s) (secondPoint k s)

Stacks.Chow.NotEquidimensional.mem_closure_supportOfFamily_exampleFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NotEquidimensional.lean, line 523. The attribute's comment: “the closure of the support contains the whole fibre over the origin”.

Stacks Project, Tag 0H5J. The closure of the support of the example family contains the whole fibre over the origin, which is a line: the surface y·t = x lies in that closure and contains the fibre over the origin.

theorem mem_closure_supportOfFamily_exampleFamily (k : Type u) [Field k] (z : totalScheme k)
    (hz : projection k z = origin k) :
    z ∈ closure (supportOfFamily (projection k) (exampleFamily k))

Stacks.Chow.NotEquidimensional.not_isEquidimensional_exampleFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NotEquidimensional.lean, line 639. The attribute's comment: “the example family is not equidimensional”.

Stacks Project, Tag 0H5J. The example family of 0-cycles on the fibres of Spec k[x, y, t] ⟶ Spec k[x, y] is not equidimensional: a closed subset of X containing its support contains the whole fibre over the origin, which is a line, so that closed subset cannot have relative dimension 0 over the base.

theorem not_isEquidimensional_exampleFamily (k : Type u) [Field k] :
    ¬ IsEquidimensional (projection k) 0 (exampleFamily k)

Stacks.Chow.NotEquidimensional.isRelativeCycle_exampleFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NotEquidimensional.lean, line 1320. The attribute's comment: “the example family is a relative 0-cycle, compatible with specializations”.

Stacks Project, Tag 0H5J. The family α of Suslin--Voevodsky's example is a relative 0-cycle: it is compatible with specializations. Over a discrete valuation ring R with a morphism g : Spec R ⟶ S there are three cases. If b = 0 in the residue field of the generic point of Spec R then it also vanishes at the closed point, so both members of the base change are zero. If b ≠ 0 at the generic point but b = 0 at the closed point, then the translation t ↦ t + y of the affine line is the identity on the special fibre and carries the first of the two rational points to the second, so their fundamental cycles have the same specialization and the difference specializes to zero, which is the vanishing member at the closed point. If b ≠ 0 at the closed point then y is a unit of R, the value a/b lies in R and the two points of the generic fibre extend to closed sections of X ×_S Spec R over Spec R, whose values at the closed point are the two rational points of the special fibre; the specialization of the fundamental cycle of a section is the prime cycle of its closed value.

theorem isRelativeCycle_exampleFamily (k : Type u) [Field k] :
    IsRelativeCycle (projection k) 0 (exampleFamily k)

Stacks.Chow.NotEquidimensional.exists_isRelativeCycle_not_isEquidimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NotEquidimensional.lean, line 1458. The attribute's comment: “there exist relative r-cycles which are not equidimensional”.

Stacks Project, Tag 0H5J. There exist relative 0-cycles which are not equidimensional: Suslin--Voevodsky's family on Spec k[x, y, t] ⟶ Spec k[x, y] is one.

theorem exists_isRelativeCycle_not_isEquidimensional (k : Type u) [Field k] :
    ∃ α : FamilyOfCycles (projection k) 0,
      IsRelativeCycle (projection k) 0 α ∧ ¬ IsEquidimensional (projection k) 0 α

Tag 0H5K, a lemma

Tag 0H5K in the Stacks Project.

Stacks.Chow.isEquidimensional_restrictedFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EquidimensionalCycles.lean, line 115. The attribute's comment: “restriction”.

Restriction to compatible open subschemes of the source and the base preserves equidimensionality of a family of cycles on the fibres.

theorem isEquidimensional_restrictedFamily {X S U V : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (fU : U ⟶ V) (j : U ⟶ X) [IsOpenImmersion j]
    (i : V ⟶ S) [IsOpenImmersion i] (h : j ≫ f = fU ≫ i) (r : ℕ) (α : FamilyOfCycles f r)
    (hα : IsEquidimensional f r α) :
    letI : IsLocallyNoetherian V := isLocallyNoetherian_of_isOpenImmersion i
    letI : LocallyOfFiniteType fU := by
      let : LocallyOfFiniteType (fU ≫ i) := h ▸ inferInstance
      exact locallyOfFiniteType_of_comp fU i
    IsEquidimensional fU r (restrictedFamily f fU j i h r α).1

Stacks.Chow.isEquidimensional_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EquidimensionalDescent.lean, line 542. The attribute's comment: “base change”.

Stacks Project, Tag 0H5K, the base-change clause. The base change of an equidimensional family of r-cycles along an arbitrary morphism g : S' ⟶ S of the base is equidimensional: its support is the inverse image of the support of the original family, and the base change of a bounding closed subscheme bounds it and has the same relative dimension over S'.

theorem isEquidimensional_baseChangeFamily {X S S' : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (g : S' ⟶ S) [IsLocallyNoetherian S']
    (r : ℕ) (α : FamilyOfCycles f r) (hα : IsEquidimensional f r α) :
    IsEquidimensional (pullback.snd f g) r (baseChangeFamily f g r α)

Stacks.Chow.isEquidimensional_flatPullbackFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EquidimensionalDescent.lean, line 590. The attribute's comment: “flat pullback”.

Stacks Project, Tag 0H5K, the flat-pullback clause. The flat pullback of an equidimensional family of r-cycles along a morphism j : U ⟶ X of schemes over S which is flat, locally of finite type and of relative dimension e is an equidimensional family of (r + e)-cycles: the inverse image of a closed subscheme bounding the support of the original family bounds the support of the pullback, and its relative dimension over S is at most r + e because it maps to the bounding subscheme by a morphism of relative dimension e.

theorem isEquidimensional_flatPullbackFamily {X S U : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (fU : U ⟶ S) [LocallyOfFiniteType fU]
    (j : U ⟶ X) [LocallyOfFiniteType j] [Flat j] (h : j ≫ f = fU) (e : ℕ)
    (he : RelativeDimension j e) (r : ℕ) (α : FamilyOfCycles f r)
    (hα : IsEquidimensional f r α) :
    IsEquidimensional fU (r + e) (flatPullbackFamily f fU j h e he r α)

Tag 0H5L, a lemma

Tag 0H5L in the Stacks Project.

Stacks.Chow.isEquidimensional_iff_forall_restrictedFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EquidimensionalCycles.lean, line 293.

Equidimensionality of a family of cycles may be checked Zariski locally on X and on S: given open subschemes U t ⊆ X lying over open subschemes V t ⊆ S whose members cover X, the family is equidimensional exactly when each of its restrictions is.

theorem isEquidimensional_iff_forall_restrictedFamily {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (r : ℕ) (α : FamilyOfCycles f r)
    {ι : Type*} (U V : ι → Scheme.{u})
    (fU : ∀ t, U t ⟶ V t) (j : ∀ t, U t ⟶ X) (hj : ∀ t, IsOpenImmersion (j t))
    (i : ∀ t, V t ⟶ S) (hi : ∀ t, IsOpenImmersion (i t))
    (h : ∀ t, j t ≫ f = fU t ≫ i t)
    (hcover : ∀ x : X, ∃ (t : ι) (y : U t), j t y = x) :
    IsEquidimensional f r α ↔
      ∀ t : ι,
        letI : IsOpenImmersion (j t) := hj t
        letI : IsOpenImmersion (i t) := hi t
        letI : IsLocallyNoetherian (V t) := isLocallyNoetherian_of_isOpenImmersion (i t)
        letI : LocallyOfFiniteType (fU t) := by
          let : LocallyOfFiniteType (fU t ≫ i t) := h t ▸ inferInstance
          exact locallyOfFiniteType_of_comp (fU t) (i t)
        IsEquidimensional (fU t) r (restrictedFamily f (fU t) (j t) (i t) (h t) r α).1

Tag 0H5M, a lemma

Tag 0H5M in the Stacks Project.

Stacks.Chow.isEquidimensional_iff_forall_of_fppfCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EquidimensionalDescent.lean, line 367. The attribute's comment: “generalized: the families over the covering are an argument and enter only through their supports, so no relative-cycle condition is needed; isEquidimensional_iff_forall_baseChangeFamily instantiates them at the base changes themselves”.

The support form of Tag 0H5M: for an fppf covering {g i : T i ⟶ S} of the base, a family of r-cycles on the fibres of f : X ⟶ S is equidimensional exactly when each family on the fibres of X ×_S T i ⟶ T i whose support is the preimage of its support is equidimensional. The base changes of the family have that property, by the base-change clause of Tag 0H4V.

theorem isEquidimensional_iff_forall_of_fppfCovering {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (r : ℕ) (α : FamilyOfCycles f r)
    {I : Type v} {T : I → Scheme.{u}} (g : ∀ i, T i ⟶ S)
    (hg : Presieve.ofArrows T g ∈ Scheme.fppfPrecoverage S)
    (β : ∀ i, FamilyOfCycles (pullback.snd f (g i)) r)
    (hβ : ∀ i, supportOfFamily (pullback.snd f (g i)) (β i) =
      pullback.fst f (g i) ⁻¹' supportOfFamily f α) :
    letI (i : I) : IsLocallyNoetherian (T i) :=
      isLocallyNoetherian_of_mem_fppfPrecoverage g hg i
    (IsEquidimensional f r α ↔
      ∀ i, IsEquidimensional (pullback.snd f (g i)) r (β i))

Stacks.Chow.isEquidimensional_iff_forall_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EquidimensionalDescent.lean, line 395.

Stacks Project, Tag 0H5M. Equidimensionality of a family of r-cycles on the fibres of f : X ⟶ S is local for an fppf covering {g i : T i ⟶ S} of the base: the family is equidimensional exactly when every base change g i ^* α is.

theorem isEquidimensional_iff_forall_baseChangeFamily {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (r : ℕ) (α : FamilyOfCycles f r)
    {I : Type v} {T : I → Scheme.{u}} (g : ∀ i, T i ⟶ S)
    (hg : Presieve.ofArrows T g ∈ Scheme.fppfPrecoverage S) :
    letI (i : I) : IsLocallyNoetherian (T i) :=
      isLocallyNoetherian_of_mem_fppfPrecoverage g hg i
    (IsEquidimensional f r α ↔
      ∀ i, IsEquidimensional (pullback.snd f (g i)) r (baseChangeFamily f (g i) r α))

Tag 0H5N, a lemma

Tag 0H5N in the Stacks Project.

Stacks.Chow.isEquidimensional_iff_forall_flatPullbackFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EquidimensionalDescent.lean, line 522.

Stacks Project, Tag 0H5N. Equidimensionality of a family of r-cycles on the fibres of f : X ⟶ S can be checked after a jointly surjective family {fi i : Xi i ⟶ X} of flat morphisms locally of finite type of relative dimension e: the family is equidimensional exactly when every flat pullback fi i ^* α, a family of (r + e)-cycles on the fibres of Xi i ⟶ S, is.

theorem isEquidimensional_iff_forall_flatPullbackFamily {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (r e : ℕ) (α : FamilyOfCycles f r)
    {I : Type v} {Xi : I → Scheme.{u}} (fi : ∀ i, Xi i ⟶ X)
    [∀ i, LocallyOfFiniteType (fi i)] [∀ i, Flat (fi i)]
    (hdim : ∀ i, RelativeDimension (fi i) e)
    (hsurj : ∀ x : X, ∃ i, x ∈ Set.range (fi i)) :
    IsEquidimensional f r α ↔
      ∀ i, IsEquidimensional (fi i ≫ f) (r + e)
        (flatPullbackFamily f (fi i ≫ f) (fi i) rfl e (hdim i) r α)

Sources

• Section 62.7, Tag 0H5H
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.IsEquidimensional · Stacks.Chow.equidimensionalRelativeCycles · Stacks.Chow.NotEquidimensional.exampleFamily · Stacks.Chow.NotEquidimensional.exampleFamily_of_eq_zero · Stacks.Chow.NotEquidimensional.exampleFamily_of_ne_zero · Stacks.Chow.NotEquidimensional.mem_closure_supportOfFamily_exampleFamily · Stacks.Chow.NotEquidimensional.not_isEquidimensional_exampleFamily · Stacks.Chow.NotEquidimensional.isRelativeCycle_exampleFamily

Section62.8 Weightings and relative zero cycles#

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

Tag 0H5P, a lemma

Tag 0H5P in the Stacks Project.

Stacks.Chow.relativeCycleWeight, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Weighting.lean, line 59. The attribute's comment: “the construction of w_α preceding the lemma; none of the lemma's three claims”.

The function w_α : X → ℤ attached to a family α of 0-cycles on the fibres of f : X ⟶ S: the coefficient of α at a point x, taken on the scheme-theoretic fibre through x, times the inseparable degree [κ(x) : κ(f x)]_i.

def relativeCycleWeight {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (α : FamilyOfCycles f 0) : X → ℤ

Stacks.Chow.isWeighting_relativeCycleWeight, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/WeightingEquivalence.lean, line 58. The attribute's comment: “clause (1): the map attached to a relative zero-cycle is a weighting”.

Stacks Project, Tag 0H5P, clause (1). Let S be a locally Noetherian scheme and let f : X ⟶ S be a locally quasi-finite morphism of schemes. For α ∈ z(X/S, 0) the map w_α : X → ℤ is a weighting of f.

theorem isWeighting_relativeCycleWeight (α : relativeCycles f 0) :
    IsWeighting f (relativeCycleWeight f α.1)

Stacks.Chow.exists_relativeCycle_nsmul_eq_relativeCycleWeight, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/WeightingEquivalence.lean, line 81. The attribute's comment: “clause (2): every weighting is a positive integer multiple of one attached to a relative zero-cycle, for a quasi-compact source”.

Stacks Project, Tag 0H5P, clause (2). Let S be a locally Noetherian scheme, let f : X ⟶ S be a locally quasi-finite morphism of schemes and let X be quasi-compact. Given a weighting w : X → ℤ of f there is an integer n > 0 with n·w = w_α for some α ∈ z(X/S, 0).

theorem exists_relativeCycle_nsmul_eq_relativeCycleWeight [CompactSpace X] (w : X → ℤ)
    (hw : IsWeighting f w) :
    ∃ (n : ℕ) (α : relativeCycles f 0), 0 < n ∧
      ∀ x : X, (n : ℤ) * w x = relativeCycleWeight f α.1 x

Stacks.Chow.exists_relativeCycle_primePow_nsmul_eq_relativeCycleWeight, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/WeightingEquivalence.lean, line 94. The attribute's comment: “clause (3): over a scheme of characteristic p the multiple may be taken to be a power of p”.

Stacks Project, Tag 0H5P, clause (3). In the situation of clause (2), if S is a scheme over 𝔽_p for a prime p, then the integer n may be chosen to be a power of p.

theorem exists_relativeCycle_primePow_nsmul_eq_relativeCycleWeight [CompactSpace X] (p : ℕ)
    [Fact p.Prime] (σ : S ⟶ Spec (CommRingCat.of (ULift.{u} (ZMod p)))) (w : X → ℤ)
    (hw : IsWeighting f w) :
    ∃ (e : ℕ) (α : relativeCycles f 0), 0 < p ^ e ∧
      ∀ x : X, ((p ^ e : ℕ) : ℤ) * w x = relativeCycleWeight f α.1 x

Sources

• Chapter 62, Tag 0H4B
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.relativeCycleWeight · Stacks.Chow.isWeighting_relativeCycleWeight · Stacks.Chow.exists_relativeCycle_nsmul_eq_relativeCycleWeight · Stacks.Chow.exists_relativeCycle_primePow_nsmul_eq_relativeCycleWeight

Section62.9 Effective relative cycles#

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

Tag 0H5R, a definition

Tag 0H5R in the Stacks Project.

Stacks.Chow.IsEffectiveRelativeCycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EffectiveRelative.lean, line 55. The attribute's comment: “effectivity of a relative r-cycle”.

A relative r-cycle α on X/S is effective when for every point s of S the r-cycle α_s it carries on the scheme-theoretic fibre over s is an effective cycle.

def IsEffectiveRelativeCycle {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (r : ℕ) (α : ↥(relativeCycles f r)) : Prop

Stacks.Chow.effectiveRelativeCycles, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EffectiveRelative.lean, line 82. The attribute's comment: “the monoid z^eff(X/S, r)”.

The monoid z^eff(X/S, r) of effective relative r-cycles on X/S: the submonoid of the group z(X/S, r) of relative r-cycles consisting of those whose cycle on every fibre is effective.

def effectiveRelativeCycles {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (r : ℕ) : AddSubmonoid ↥(relativeCycles f r)

Tag 0H5S, a lemma

Tag 0H5S in the Stacks Project.

Stacks.Chow.isEffectiveFamily_restrictedFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Effective.lean, line 146. The attribute's comment: “restriction”.

Stacks Project, Tag 0H5S. The restriction of an effective family of r-cycles on the fibres of X/S to open subschemes U ⊆ X and V ⊆ S with f(U) ⊆ V is effective.

theorem isEffectiveFamily_restrictedFamily {X S U V : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (fU : U ⟶ V) (j : U ⟶ X)
    [IsOpenImmersion j] (i : V ⟶ S) [IsOpenImmersion i] (h : j ≫ f = fU ≫ i) (r : ℕ)
    (α : FamilyOfCycles f r) (hα : IsEffectiveFamily f r α) :
    letI : LocallyOfFiniteType fU := by
      let : LocallyOfFiniteType (fU ≫ i) := h ▸ inferInstance
      exact locallyOfFiniteType_of_comp fU i
    IsEffectiveFamily fU r (restrictedFamily f fU j i h r α).1

Stacks.Chow.isEffectiveFamily_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Effective.lean, line 592. The attribute's comment: “base change”.

Stacks Project, Tag 0H5S, base change. The base change of an effective family of r-cycles on the fibres of X/S along any morphism g : S' ⟶ S of bases is effective; no surjectivity of g is needed.

theorem isEffectiveFamily_baseChangeFamily {X S S' : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (g : S' ⟶ S) (r : ℕ)
    (α : FamilyOfCycles f r) (hα : IsEffectiveFamily f r α) :
    IsEffectiveFamily (pullback.snd f g) r (baseChangeFamily f g r α)

Stacks.Chow.isEffectiveFamily_flatPullbackFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Effective.lean, line 674. The attribute's comment: “flat pullback”.

Stacks Project, Tag 0H5S, flat pullback. The flat pullback of an effective family of r-cycles on the fibres of X/S along a flat morphism j : U ⟶ X of schemes over S, locally of finite type and of relative dimension e, is an effective family of (r+e)-cycles on the fibres of U/S.

theorem isEffectiveFamily_flatPullbackFamily {X S U : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (fU : U ⟶ S) [LocallyOfFiniteType fU]
    (j : U ⟶ X) [LocallyOfFiniteType j] [Flat j] (h : j ≫ f = fU) (e : ℕ)
    (he : AlgebraicGeometry.RelativeDimension j e) (r : ℕ) (α : FamilyOfCycles f r)
    (hα : IsEffectiveFamily f r α) :
    IsEffectiveFamily fU (r + e) (flatPullbackFamily f fU j h e he r α)

Stacks.Chow.isEffectiveFamily_properPushforwardFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Effective.lean, line 689. The attribute's comment: “proper pushforward”.

Stacks Project, Tag 0H5S, proper pushforward. The proper pushforward of an effective family of r-cycles on the fibres of X/S along a proper morphism p : X ⟶ Y of schemes over S is an effective family of r-cycles on the fibres of Y/S.

theorem isEffectiveFamily_properPushforwardFamily {X Y S : Scheme.{u}} (sX : X ⟶ S)
    [LocallyOfFiniteType sX] [IsLocallyNoetherian S] (sY : Y ⟶ S) [LocallyOfFiniteType sY]
    (p : X ⟶ Y) [IsProper p] (hp : p ≫ sY = sX) (r : ℕ) (α : FamilyOfCycles sX r)
    (hα : IsEffectiveFamily sX r α) :
    IsEffectiveFamily sY r (properPushforwardFamily sX sY p hp r α)

Tag 0H5T, a lemma

Tag 0H5T in the Stacks Project.

Stacks.Chow.isEffectiveFamily_iff_forall_restrictedFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Effective.lean, line 199.

Stacks Project, Tag 0H5T. Effectivity of a family of r-cycles on the fibres of X/S may be checked Zariski locally on X and on S: given open subschemes U a ⊆ X and V a ⊆ S with f(U a) ⊆ V a and with the U a covering X, the family is effective exactly when each of its restrictions is.

theorem isEffectiveFamily_iff_forall_restrictedFamily {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] {ι : Type v} {U V : ι → Scheme.{u}}
    (fU : ∀ a : ι, U a ⟶ V a) (j : ∀ a : ι, U a ⟶ X) [∀ a : ι, IsOpenImmersion (j a)]
    (i : ∀ a : ι, V a ⟶ S) [∀ a : ι, IsOpenImmersion (i a)]
    (h : ∀ a : ι, j a ≫ f = fU a ≫ i a) (hcover : ∀ x : X, ∃ a : ι, x ∈ Set.range (j a))
    (r : ℕ) (α : FamilyOfCycles f r) :
    letI : ∀ a : ι, LocallyOfFiniteType (fU a) := fun a => by
      let : LocallyOfFiniteType (fU a ≫ i a) := h a ▸ inferInstance
      exact locallyOfFiniteType_of_comp (fU a) (i a)
    IsEffectiveFamily f r α ↔
      ∀ a : ι, IsEffectiveFamily (fU a) r
        (restrictedFamily f (fU a) (j a) (i a) (h a) r α).1

Tag 0H5U, a lemma

Tag 0H5U in the Stacks Project.

Stacks.Chow.isEffectiveFamily_iff_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Effective.lean, line 611.

Stacks Project, Tag 0H5U. Let α be a family of r-cycles on the fibres of X/S and let g : S' ⟶ S be surjective. Then α is effective if and only if its base change g^*α is effective.

Effectivity is a condition on each coefficient separately, and a coefficient of g^*α is a coefficient of α times a multiplicity. The multiplicity is nonnegative, which gives the forward implication. For the converse, surjectivity supplies a point t of S' over a given point of S, and over t the fibre of the base change has a point lying over the chosen point of the fibre of f at which that multiplicity is nonzero, hence positive; so a negative coefficient of α would make a coefficient of g^*α negative.

theorem isEffectiveFamily_iff_baseChangeFamily {X S S' : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (g : S' ⟶ S) [Surjective g] (r : ℕ)
    (α : FamilyOfCycles f r) :
    IsEffectiveFamily f r α ↔
      IsEffectiveFamily (pullback.snd f g) r (baseChangeFamily f g r α)

Tag 0H5V, a lemma

Tag 0H5V in the Stacks Project.

Stacks.Chow.isEffectiveFamily_iff_forall_flatPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Effective.lean, line 547.

Stacks Project, Tag 0H5V. Let α be a family of r-cycles on the fibres of X/S and let {g i : X' i ⟶ X} be a jointly surjective family of flat morphisms, locally of finite type and of relative dimension e. If β i is the flat pullback of α along g i, then α is effective if and only if every β i is.

The fibres of g i ≫ f map to those of f by the base changes of the g i, again flat, locally of finite type and of relative dimension e, and jointly surjective on every fibre, so this is the fibrewise Stacks.Chow.isEffectiveFamily_iff_forall.

theorem isEffectiveFamily_iff_forall_flatPullback {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] {r e : ℕ} (α : FamilyOfCycles f r) {Idx : Type*}
    {X' : Idx → Scheme.{u}} (g : ∀ i, X' i ⟶ X) [∀ i, LocallyOfFiniteType (g i)]
    [∀ i, Flat (g i)] (hrel : ∀ i, AlgebraicGeometry.RelativeDimension (g i) e)
    (hsurj : ∀ x : X, ∃ i, ∃ x' : X' i, (g i).base x' = x)
    (β : ∀ i, FamilyOfCycles (g i ≫ f) (r + e))
    (hβ : ∀ (i : Idx) (s : S) (x : (g i ≫ f).fiber s),
      (β i s : AlgebraicCycle ((g i ≫ f).fiber s) ℤ) x =
        (α s : AlgebraicCycle (f.fiber s) ℤ) ((f.fiberMap (g i) s).base x) *
          flatPullbackWeight (fieldChowSituation (S.residueField s))
            ((g i ≫ f).fiberToSpecResidueField s) (f.fiberMap (g i) s)
            ((r : ℤ) + (e : ℤ)) x) :
    IsEffectiveFamily f r α ↔ ∀ i, IsEffectiveFamily (g i ≫ f) (r + e) (β i)

Tag 0H5W, a lemma

Tag 0H5W in the Stacks Project.

Stacks.Chow.isClosed_supportOfFamily_of_isEffectiveFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EffectiveSupportClosed.lean, line 332.

Stacks Project, Tag 0H5W. Let f : X ⟶ S be a morphism of schemes with S locally Noetherian and f locally of finite type, let r ≥ 0 be an integer and let α be a relative r-cycle on X/S. If α is effective then its support is closed in X.

theorem isClosed_supportOfFamily_of_isEffectiveFamily (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (r : ℕ) (α : FamilyOfCycles f r) (hα : IsRelativeCycle f r α)
    (heff : IsEffectiveFamily f r α) : IsClosed (supportOfFamily f α)

Tag 0H5X, a lemma

Tag 0H5X in the Stacks Project.

Stacks.Chow.isEquidimensional_of_isEffectiveFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EffectiveEquidimensional.lean, line 131.

Stacks Project, Tag 0H5X. Let f : X ⟶ S be a morphism of schemes with S locally Noetherian and f locally of finite type, let r ≥ 0 be an integer and let α be a relative r-cycle on X/S. If α is effective then α is equidimensional.

theorem isEquidimensional_of_isEffectiveFamily (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (r : ℕ) (α : FamilyOfCycles f r) (hα : IsRelativeCycle f r α)
    (heff : IsEffectiveFamily f r α) : IsEquidimensional f r α

Tag 0H5Y, a remark

Tag 0H5Y in the Stacks Project.

Stacks.Chow.effectiveRelativeCyclesFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/EffectiveFunctor.lean, line 163. The attribute's comment: “the functor S' ↦ z^eff(X'/S', r), X' = S' ×_S X, on schemes locally of finite type over S”.

The contravariant functor S' ↦ z^eff(X'/S', r), X' = S' ×_S X, on the category of schemes locally of finite type over S, the map attached to a morphism S'' ⟶ S' over S being base change of effective relative r-cycles.

def effectiveRelativeCyclesFunctor : (LocallyOfFiniteTypeOver S)ᵒᵖ ⥤ Type u

Stacks.Chow.not_isRepresentable_effectiveRelativeCyclesFunctor_specFieldExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NonRepresentable.lean, line 217. The attribute's comment: “the functor S' ↦ z^eff(X'/S', r) is not representable, the counter example the remark leaves to the reader, built from z(X'/S', r) = z(X'_red/S'_red, r)”.

Stacks Project, Remark 0H5Y. Let k be a field and let K/k be a finite purely inseparable extension of degree > 1, so that S = Spec k is Noetherian and f : X = Spec K ⟶ S is finite. The functor S' ↦ z^eff(X'/S', 0), X' = S' ×_S X, on schemes locally of finite type over S is not representable.

This is the reason the source gives, made into a counter example: relative cycles do not see nilpotents. If M represented the functor, the diagonal cycle ξ ∈ z^eff(X_K/Spec K, 0) would be a morphism Spec K ⟶ M whose two pullbacks to Spec K ×_k Spec K agree, because they agree on the reduction and base change to the reduction is injective; as Spec K ⟶ Spec k is an effective epimorphism, ξ would come from z^eff(X/S, 0). But the cycle ξ is one rational point with coefficient one, while every base change of a cycle along K/k has coefficients divisible by [K : k] at such a point.

theorem not_isRepresentable_effectiveRelativeCyclesFunctor_specFieldExt
    [IsPurelyInseparable k K] (hK : Module.finrank k K ≠ 1) :
    ¬ (effectiveRelativeCyclesFunctor (specFieldExt k K) 0).IsRepresentable

Stacks.Chow.exists_not_isRepresentable_effectiveRelativeCyclesFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NonRepresentable.lean, line 310. The attribute's comment: “the functor S' ↦ z^eff(X'/S', r) cannot be representable in general”.

Stacks Project, Remark 0H5Y. The functor S' ↦ z^eff(X'/S', r), X' = S' ×_S X, on schemes locally of finite type over S is not representable in general: there are a locally Noetherian scheme S, a morphism f : X ⟶ S locally of finite type and an r ≥ 0 for which it is not representable. One may take S = Spec 𝔽₂, X = A² and r = 0 (Stacks.Chow.SymPlane.not_isRepresentable).

theorem exists_not_isRepresentable_effectiveRelativeCyclesFunctor :
    ∃ (S X : Scheme.{u}) (f : X ⟶ S) (_ : LocallyOfFiniteType f) (_ : IsLocallyNoetherian S)
      (r : ℕ), ¬ (effectiveRelativeCyclesFunctor f r).IsRepresentable

Stacks.Chow.relativeCyclesAddEquivReductionReduction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ReducedInvariance.lean, line 233. The attribute's comment: “the invariance z(X/S, r) = z(X_red/S_red, r)”.

Stacks Project, Remark 0H5Y. z(X/S, r) = z(X_red/S_red, r): the group of relative r-cycles does not change when both the source and the base are replaced by their reductions. Base change along S_red ⟶ S identifies z(X/S, r) with z(X ×_S S_red / S_red, r) (Stacks.Chow.relativeCyclesAddEquivReduction), and X_red ⟶ X ×_S S_red is a thickening over S_red, along which proper pushforward identifies the groups of relative cycles (Tag 0H5E).

noncomputable def relativeCyclesAddEquivReductionReduction :
    ↥(relativeCycles f r) ≃+ ↥(relativeCycles (Scheme.reductionMap f) r)

Stacks.Chow.SymPlane.baseChange_quot_ne_alpha, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SymmetricSquarePlane.lean, line 475. The attribute's comment: “in characteristic 2 the cycle α on A² × A² does not descend to Sym²(A²): there is no cycle β whose pullback to W is α”.

Stacks Project, Remark 0H5Y, the characteristic 2 example: there is no cycle β. Let k be a field of characteristic 2, X = A²_k, W = X ×_k X and Sym²(X) = Spec B with B = k[u₁ + u₂, u₁u₂, v₁ + v₂, v₁v₂, u₁v₁ + u₂v₂]. No family β of 0-cycles on the fibres of X ×_k Sym²(X) ⟶ Sym²(X), in particular no relative 0-cycle, pulls back along the quotient morphism W ⟶ Sym²(X) to the cycle α with α_{(x₁, x₂)} = [x₁] + [x₂]: at the generic point η of the image V = Spec k[u₁², v₁²] of the diagonal the cycle β_η would be a 0-cycle on A²_{k(u₁², v₁²)} whose pullback to A²_{k(u₁, v₁)} is twice the rational point (u₁, v₁), which is impossible.

theorem baseChange_quot_ne_alpha
    (β : FamilyOfCycles (pullback.snd (planeHom k) (symObj k).obj.hom) 0) :
    baseChangeFamilyOfIsPullback (pullback.snd (planeHom k) (symObj k).obj.hom)
      (isPullback_overBaseChange (planeHom k) (quot k).hom) 0 β ≠ (alpha k).1.1

Stacks.Chow.SymPlane.not_isRepresentable_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SymmetricSquarePlane.lean, line 625. The attribute's comment: “in characteristic 2 the functor is not representable on any category of schemes of finite type over k containing W and the principal opens of W and of Sym²(X)”.

Stacks Project, Remark 0H5Y, the characteristic 2 example. Let k be a field of characteristic 2 and X = A²_k. On any full subcategory of the schemes of finite type over k containing W = X ×_k X and the principal open subschemes of W and of Sym²(X) = W/⟨σ⟩, the functor S' ↦ z^eff(S' ×_k X / S', 0) is not representable. Such is the category of weakly normal schemes of finite type over k (Stacks.Chow.SymPlane.not_isRepresentable_weaklyNormal), so replacing seminormality by weak normality does not make the functor representable when the base has points of positive characteristic.

If M represented the functor, the cycle α would be a morphism W ⟶ M invariant under the involution σ exchanging the factors, because α is; near the generic point of the image of the diagonal it would factor through W ⟶ Sym²(X), and the cycle β on Sym²(X) corresponding to the factorization would pull back to α. There is no such cycle (Stacks.Chow.SymPlane.map_quotAway_ne).

theorem not_isRepresentable_of_le (P : ObjectProperty (LocallyOfFiniteTypeOver (Spec (.of k))))
    (hW : P (squareObj k))
    (hP : ∀ h : sym k, h ≠ 0 → P (squareAwayObj k h) ∧ P (symAwayObj k h)) :
    ¬ (P.ι.op ⋙ effectiveRelativeCyclesFunctor (planeHom k) 0).IsRepresentable

Stacks.Chow.SymPlane.map_sym_diagonalRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SymmetricSquarePlane.lean, line 701. The attribute's comment: “the image of the diagonal in Sym²(X) is V = Spec k[u₁², v₁²]”.

The image of the diagonal in Sym²(X) is V = Spec k[u², v²], in characteristic 2: the coordinate ring of Sym²(X) restricts on the diagonal to k[u², v²].

theorem map_sym_diagonalRestriction :
    (sym k).map (diagonalRestriction k) =
      Algebra.adjoin k {(X 0 : MvPolynomial (Fin 2) k) ^ 2, X 1 ^ 2}

Stacks.Chow.SymPlane.not_isRepresentable_weaklyNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SymmetricSquarePlane.lean, line 827. The attribute's comment: “in characteristic 2 the functor is not representable on the category of weakly normal schemes of finite type over k”.

Stacks Project, Remark 0H5Y, the characteristic 2 example, on weakly normal schemes. Let k be a field of characteristic 2 and X = A²_k. Call a scheme weakly normal if every birational universal homeomorphism onto it has a section. On the category of weakly normal schemes of finite type over k the functor S' ↦ z^eff(S' ×_k X / S', 0) is not representable: W = X ×_k X is normal, hence weakly normal, Sym²(X) is normal, and so are their principal opens (Stacks.Chow.SymPlane.not_isRepresentable_of_le).

theorem not_isRepresentable_weaklyNormal :
    ¬ ((weaklyNormalOfFiniteType k).ι.op ⋙
      effectiveRelativeCyclesFunctor (planeHom k) 0).IsRepresentable

Stacks.Chow.SymPlane.mem_sym_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/SymmetricSquarePlaneRing.lean, line 337. The attribute's comment: “Sym²(X) = W/⟨σ⟩ is the spectrum of k[u₁ + u₂, u₁u₂, v₁ + v₂, v₁v₂, u₁v₁ + u₂v₂]”.

The invariants of the swap. In characteristic 2, an element of k[u₁, u₂, v₁, v₂] is fixed by the involution exchanging the two factors exactly when it lies in k[u₁ + u₂, u₁u₂, v₁ + v₂, v₁v₂, u₁v₁ + u₂v₂].

theorem mem_sym_iff (x : ring k) : x ∈ sym k ↔ swap k x = x

Sources

• Section 62.9, Tag 0H5Q
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.IsEffectiveRelativeCycle · Stacks.Chow.effectiveRelativeCycles · Stacks.Chow.isEffectiveFamily_restrictedFamily · Stacks.Chow.isEffectiveFamily_baseChangeFamily · Stacks.Chow.isEffectiveFamily_flatPullbackFamily · Stacks.Chow.isEffectiveFamily_properPushforwardFamily · Stacks.Chow.isEffectiveFamily_iff_forall_restrictedFamily · Stacks.Chow.isEffectiveFamily_iff_baseChangeFamily

Section62.10 Proper relative cycles#

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

Tag 0H61, a definition

Tag 0H61 in the Stacks Project.

Stacks.Chow.IsProperRelativeCycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ProperRelativeCycles.lean, line 135. The attribute's comment: “the predicate”.

Stacks Project, Definition 0H61. A family α of r-cycles on the fibres of X/S has proper support when its support is contained in a closed subset W ⊆ X proper over S; a relative r-cycle with this property is a proper relative cycle.

def IsProperRelativeCycle {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] (r : ℕ)
    (α : FamilyOfCycles f r) : Prop

Stacks.Chow.properRelativeCycles, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ProperRelativeCycles.lean, line 169. The attribute's comment: “the group c(X/S, r) of proper relative cycles”.

Stacks Project, Definition 0H61. The group c(X/S, r) of proper relative r-cycles on X/S: the subgroup of the group of families of r-cycles on the fibres of X/S whose members are the relative r-cycles with support contained in a closed subset proper over S.

def properRelativeCycles {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (r : ℕ) : AddSubgroup (FamilyOfCycles f r)

Tag 0H62, a lemma

Tag 0H62 in the Stacks Project.

Stacks.Chow.isProperRelativeCycle_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ProperRelativeCycles.lean, line 211.

Stacks Project, Lemma 0H62. Let S be locally Noetherian, let f : X ⟶ S be locally of finite type and let α be a relative r-cycle on X/S. If α is proper, then every base change of α along a morphism S' ⟶ S is proper.

theorem isProperRelativeCycle_baseChangeFamily {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (r : ℕ) {α : FamilyOfCycles f r}
    (hα : α ∈ properRelativeCycles f r) :
    ∀ (S' : Scheme.{u}) (g : S' ⟶ S),
      IsProperRelativeCycle (pullback.snd f g) r (baseChangeFamily f g r α)

Tag 0H63, a lemma

Tag 0H63 in the Stacks Project.

Stacks.Chow.isProperRelativeCycle_iff_forall_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ProperHDescent.lean, line 264.

Stacks Project, Lemma 0H63. Let S be locally Noetherian, let f : X ⟶ S be locally of finite type and let α be a family of r-cycles on the fibres of X/S. Let {g i : S i ⟶ S} be an h covering. Then α is a proper relative cycle if and only if each base change (g i)^*α is a proper relative cycle.

Properness of a relative cycle is a condition on its support alone, so neither the valuative condition defining a relative r-cycle nor any hypothesis on the members of the covering beyond the h-covering condition enters.

theorem isProperRelativeCycle_iff_forall_baseChangeFamily {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [IsLocallyNoetherian S] (r : ℕ) (α : FamilyOfCycles f r)
    {I : Type v} (S' : I → Scheme.{u}) (g : ∀ i, S' i ⟶ S) (hg : IsHCovering S' g) :
    IsProperRelativeCycle f r α ↔
      ∀ i, IsProperRelativeCycle (pullback.snd f (g i)) r (baseChangeFamily f (g i) r α)

Sources

• Section 62.10, Tag 0H60
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.IsProperRelativeCycle · Stacks.Chow.properRelativeCycles · Stacks.Chow.isProperRelativeCycle_baseChangeFamily · Stacks.Chow.isProperRelativeCycle_iff_forall_baseChangeFamily

Section62.12 Action on cycles#

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

Tag 0H66, a lemma

Tag 0H66 in the Stacks Project.

Stacks.Chow.cap_add_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ActionOnCycles.lean, line 450. The attribute's comment: “additivity in the family of fibre cycles”.

The action is additive in the family of fibre cycles.

theorem cap_add_left (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (s : Y ⟶ C.S) [LocallyOfFiniteType s]
    (f : X ⟶ Y) [LocallyOfFiniteType f] {r : ℕ}
    (α₁ α₂ : FamilyOfCycles f r)
    {e : ℤ} (β : CycleGroup C s e) :
    letI : LocallyOfFiniteType (f ≫ s) := inferInstance
    cap C s f (α₁ + α₂) β = cap C s f α₁ β + cap C s f α₂ β

Stacks.Chow.cap_add_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ActionOnCycles.lean, line 462. The attribute's comment: “additivity in the cycle on the base”.

The action is additive in the cycle on the base.

theorem cap_add_right (C : ChowSituation.{u})
    {X Y : Scheme.{u}} (s : Y ⟶ C.S) [LocallyOfFiniteType s]
    (f : X ⟶ Y) [LocallyOfFiniteType f] {r : ℕ}
    (α : FamilyOfCycles f r)
    {e : ℤ} (β₁ β₂ : CycleGroup C s e) :
    letI : LocallyOfFiniteType (f ≫ s) := inferInstance
    cap C s f α (β₁ + β₂) = cap C s f α β₁ + cap C s f α β₂

Tag 0H67, a lemma

Tag 0H67 in the Stacks Project.

Stacks.Chow.cycleGroupRestrict_cap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/RestrictionAction.lean, line 98.

Stacks Project, Tag 0H67. If U ⊆ X and V ⊆ Y are open and f(U) ⊆ V, then the restriction to U of the cycle α ∩ β is α|_U ∩ β|_V, the cycle obtained by letting the restriction of the family α to the fibres of U/V act on the restriction of β to V.

theorem cycleGroupRestrict_cap (C : ChowSituation.{u}) {X Y U V : Scheme.{u}}
    (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (sV : V ⟶ C.S) [LocallyOfFiniteType sV]
    (f : X ⟶ Y) [LocallyOfFiniteType f] (fU : U ⟶ V)
    (j : U ⟶ X) [IsOpenImmersion j] (i : V ⟶ Y) [IsOpenImmersion i]
    (hi : i ≫ sY = sV) (h : j ≫ f = fU ≫ i) (r : ℕ) (e : ℤ)
    (α : FamilyOfCycles f r) (β : CycleGroup C sY e) :
    letI : LocallyOfFiniteType fU := by
      let : LocallyOfFiniteType (fU ≫ i) := h ▸ inferInstance
      exact locallyOfFiniteType_of_comp fU i
    letI : LocallyOfFiniteType (f ≫ sY) := inferInstance
    letI : LocallyOfFiniteType (fU ≫ sV) := inferInstance
    cycleGroupRestrict C (f ≫ sY) (fU ≫ sV) j
        (by rw [← Category.assoc, h, Category.assoc, hi]) ((r : ℤ) + e)
        (cap C sY f α β) =
      cap C sV fU (restrictedFamily f fU j i h r α).1
        (cycleGroupRestrict C sY sV i hi e β)

Tag 0H68, a lemma

Tag 0H68 in the Stacks Project.

Stacks.Chow.cap_flatPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ActionBaseChange.lean, line 694. The attribute's comment: “compatibility with flat pullback”.

Stacks Project, Tag 0H68. Forming α ∩ β is compatible with flat pullback: if g : Y' ⟶ Y is flat, locally of finite type and of relative dimension c, if α' is the base change of the family α along g and β' the flat pullback of β, then the cycle α' ∩ β' on X ×_Y Y' is the flat pullback of α ∩ β along X ×_Y Y' ⟶ X.

theorem cap_flatPullback (C : ChowSituation.{u}) {X Y Y' : Scheme.{u}}
    (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : X ⟶ Y) [LocallyOfFiniteType f]
    (g : Y' ⟶ Y) [LocallyOfFiniteType g] [Flat g] (c : ℕ)
    (hg : AlgebraicGeometry.RelativeDimension g c) (r : ℕ) (e : ℤ)
    (α : FamilyOfCycles f r) (β : CycleGroup C sY e) :
    letI : LocallyOfFiniteType (f ≫ sY) := inferInstance
    letI : LocallyOfFiniteType (g ≫ sY) := inferInstance
    letI : LocallyOfFiniteType (pullback.snd f g ≫ g ≫ sY) := inferInstance
    (cap C (g ≫ sY) (pullback.snd f g) (baseChangeFamily f g r α)
          (flatPullback C (g ≫ sY) sY g rfl c hg e β) :
        AlgebraicCycle (pullback f g : Scheme.{u}) ℤ) =
      (flatPullback C (pullback.snd f g ≫ g ≫ sY) (f ≫ sY) (pullback.fst f g)
          (by rw [← Category.assoc, pullback.condition, Category.assoc]) c
          (AlgebraicGeometry.RelativeDimension.of_isPullback
            ((IsPullback.of_hasPullback f g).flip) hg) ((r : ℤ) + e) (cap C sY f α β) :
        AlgebraicCycle (pullback f g : Scheme.{u}) ℤ)

Stacks.Chow.cap_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ActionBaseChange.lean, line 739. The attribute's comment: “compatibility with flat base change”.

Stacks Project, Tag 0H68. Forming α ∩ β is compatible with flat base change: in the situation of Tag 0FVG, with α' the base change of the family α along Y' = Y ×_S S' ⟶ Y and β' = g^*β ∈ Z_{e + c}(Y') the base change of β, the cycle α' ∩ β' is the base change of α ∩ β, read along the canonical isomorphism of X ×_Y Y' with X' = X ×_S S'.

theorem cap_baseChange (B : FlatBaseChangeSituation.{u}) {X Y : Scheme.{u}}
    (sY : Y ⟶ B.base.S) [LocallyOfFiniteType sY] (f : X ⟶ Y) [LocallyOfFiniteType f]
    (r : ℕ) (e : ℤ) (α : FamilyOfCycles f r) (β : CycleGroup B.base sY e)
    (w : (pullback f (pullback.fst sY B.g) : Scheme.{u})) :
    letI : LocallyOfFiniteType (f ≫ sY) := inferInstance
    letI : LocallyOfFiniteType (pullback.snd sY B.g) := inferInstance
    letI : LocallyOfFiniteType (pullback.snd f (pullback.fst sY B.g)) := inferInstance
    (cap B.baseChange (pullback.snd sY B.g) (pullback.snd f (pullback.fst sY B.g))
          (baseChangeFamily f (pullback.fst sY B.g) r α)
          (baseChangeCyclePullback B sY e β) :
        AlgebraicCycle (pullback f (pullback.fst sY B.g) : Scheme.{u}) ℤ) w =
      (baseChangeCyclePullback B (f ≫ sY) ((r : ℤ) + e) (cap B.base sY f α β) :
        AlgebraicCycle (pullback (f ≫ sY) B.g : Scheme.{u}) ℤ)
        ((pullbackRightPullbackFstIso sY B.g f).hom.base w)

Tag 0H69, a lemma

Tag 0H69 in the Stacks Project.

Stacks.Chow.cap_familyAssociatedToModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/CapTensorPullback.lean, line 137.

Stacks Project, Tag 0H69. Let (S, δ) and f : X ⟶ Y be as in Section 0H65, let F be a coherent 𝒪_X-module whose support on every fibre of f has dimension at most r and let G be a coherent 𝒪_Y-module whose support has delta-dimension at most e. Set α = [F/X/Y]_r and β = [G]_e. If F is flat over Y then α ∩ β = [F ⊗_{𝒪_X} f^* G]_{r + e}.

theorem cap_familyAssociatedToModule (r : ℕ) (e : ℤ) (F : X.Modules) [F.IsCoherent]
    (hdim : ∀ y : Y, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι y)).obj F)) ≤ (r : WithBot ℕ∞))
    (hflat : IsFlatOver f.toLRSHom.toShHom F) (G : Y.Modules) [G.IsCoherent]
    (hGe : schemeDeltaDimension C ((reducedSupport G).subschemeι ≫ sY) ≤ (e : EInt)) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian (f ≫ sY)
    letI : F.IsFiniteType := isFiniteType_of_isCoherent F
    letI : F.IsQuasicoherent := isQuasicoherent_of_isCoherent F
    cap C sY f (familyAssociatedToModule f F r hdim)
        (cycleAssociatedToCoherentSheaf C sY G e hGe) =
      cycleAssociatedToCoherentSheaf C (f ≫ sY) (tensorPullback f F G) ((r : ℤ) + e)
        (schemeDeltaDimension_tensorPullback_le C sY f r e F hdim G hGe)

Tag 0H6A, a lemma

Tag 0H6A in the Stacks Project.

Stacks.Chow.cap_familyAssociatedToClosedSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/CapClosedSubscheme.lean, line 271.

Stacks Project, Tag 0H6A. Let (S, δ) and f : X ⟶ Y be as in Section 0H65. Let Z ⊆ X be a closed subscheme of relative dimension at most r over Y, so that the fibres Z_y = Z ×_X X_y have dimension at most r, and set α = [Z/X/Y]_r (Example 0H4S). Let W ⊆ Y be a closed subscheme of δ-dimension at most e and set β = [W]_e (Chow Homology, Definition 02QU). If Z is flat over Y, then α ∩ β = [Z ×_Y W]_{r + e}.

The proof is the special case F = 𝒪_Z, G = 𝒪_W of Stacks 0H69: the family α is the family of cycles attached to the coherent module i_* 𝒪_Z of Example 0H4Q, by Stacks.Chow.familyAssociatedToModule_pushforwardStructureSheaf; the cycle of a closed subscheme is the cycle of its structure sheaf (Stacks 02QY) on both sides; flatness of Z over Y is flatness of i_* 𝒪_Z over Y because a closed immersion is affine; and the projection formula together with base change identifies i_* 𝒪_Z ⊗_{𝒪_X} f^* j_* 𝒪_W with the structure sheaf of Z ×_Y W pushed forward to X.

theorem cap_familyAssociatedToClosedSubscheme (C : ChowSituation.{u}) {X Y Z W : Scheme.{u}}
    (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (f : X ⟶ Y) [LocallyOfFiniteType f] (r : ℕ) (e : ℤ)
    (i : Z ⟶ X) [IsClosedImmersion i] [Flat (i ≫ f)]
    (hZ : ∀ y : Y, topologicalKrullDim (pullback i (f.fiberι y) : Scheme.{u}) ≤ (r : WithBot ℕ∞))
    (j : W ⟶ Y) [IsClosedImmersion j]
    (hWe : schemeDeltaDimension C (j ≫ sY) ≤ (e : EInt)) :
    cap C sY f (familyAssociatedToClosedSubscheme f i r)
        (cycleAssociatedToClosedSubscheme C sY j e) =
      cycleAssociatedToClosedSubscheme C (f ≫ sY) (pullback.fst (i ≫ f) j ≫ i)
        ((r : ℤ) + e)

Tag 0H6B, a lemma

Tag 0H6B in the Stacks Project.

Stacks.Chow.properPushforward_cap_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ActionPushPull.lean, line 678.

Stacks Project, Tag 0H6B. Let (S, δ) be a Chow situation, let

X' --f--> X
|         |
v         v
Y' --g--> Y

be a cartesian square of schemes locally of finite type over S with g proper, realized by the fibre product X' = X ×_Y Y' with f = pullback.fst, let r ≥ 0 and e ∈ ℤ, let α be a family of r-cycles on the fibres of X/Y and let β' ∈ Z_e(Y'). Then

f_*(g^*α ∩ β') = α ∩ g_*β' in Z_{r + e}(X),

where ∩ is the action Stacks.Chow.cap and g^*α is the base change Stacks.Chow.baseChangeFamily of the family.

theorem properPushforward_cap_baseChangeFamily (C : ChowSituation.{u}) {X Y Y' : Scheme.{u}}
    (sX : X ⟶ C.S) [LocallyOfFiniteType sX] (sY : Y ⟶ C.S) [LocallyOfFiniteType sY]
    (sY' : Y' ⟶ C.S) [LocallyOfFiniteType sY'] (p : X ⟶ Y) [LocallyOfFiniteType p]
    (g : Y' ⟶ Y) [IsProper g] (hp : p ≫ sY = sX) (hg : g ≫ sY = sY') (r : ℕ) (e : ℤ)
    (α : FamilyOfCycles p r) (β' : CycleGroup C sY' e) :
    properPushforward C (pullback.snd p g ≫ sY') sX (pullback.fst p g)
        (pullbackFst_comp_eq_of_base g hp hg) ((r : ℤ) + e)
        (cap C sY' (pullback.snd p g) (baseChangeFamily p g r α) β') =
      hp ▸ cap C sY p α (properPushforward C sY' sY g hg e β')

Sources

• Section 62.12, Tag 0H65
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.cap_add_left · Stacks.Chow.cap_add_right · Stacks.Chow.cycleGroupRestrict_cap · Stacks.Chow.cap_flatPullback · Stacks.Chow.cap_baseChange · Stacks.Chow.cap_familyAssociatedToModule · Stacks.Chow.cap_familyAssociatedToClosedSubscheme · Stacks.Chow.properPushforward_cap_baseChangeFamily

Section62.13 Action on chow groups#

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

Tag 0H6D, a lemma

Tag 0H6D in the Stacks Project.

Stacks.Chow.properPushforward_gysinCycleMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinTrivialRestrictionPushforward.lean, line 367.

Stacks 0H6D. The Gysin map on cycles of Stacks 0B6Z commutes with proper pushforward: in the cartesian square of Stacks 0B6Y

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

attached to a triple (L, s, i : D ⟶ X) whose invertible module restricts trivially to the zero scheme D = Z(s), one has i^* f_* α' = g_* (i')^* α' in Z_k(D) for every α' ∈ Z_{k+1}(X').

The triviality of L'|_{D'} that the Gysin map on X' needs is not a hypothesis: it follows from the triviality of L|_D, by Stacks.Divisors.isTrivial_pullback_zeroScheme_pullbackGlobalSections.

theorem properPushforward_gysinCycleMap
    (htriv : AlgebraicGeometry.SheafOfModules.IsTrivial (zeroScheme X L s).subscheme.sheaf.obj
      (zeroScheme X L s).subscheme.ringCatSheaf.property
      ((Scheme.Modules.pullback (zeroScheme X L s).subschemeι).obj L))
    (α : CycleGroup C p' (k + 1)) :
    gysinCycleMap C p k L s htriv (properPushforward C p' p f hf (k + 1) α) =
      properPushforward C ((pullbackZeroScheme f L s).subschemeι ≫ p')
        ((zeroScheme X L s).subschemeι ≫ p) (zeroSchemePullbackMap f L s)
        (zeroSchemePullbackMap_comp_structureMorphism f L s p p' hf) k
        (gysinCycleMap C p' k ((Scheme.Modules.pullback f).obj L)
          (AlgebraicGeometry.pullbackGlobalSections f L s)
          (isTrivial_pullback_zeroScheme_pullbackGlobalSections f L s htriv) α)

Tag 0H6E, a lemma

Tag 0H6E in the Stacks Project.

Stacks.Chow.cap_baseChangeFamily_gysinCycleMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/GysinAction.lean, line 582.

Stacks Project, Tag 0H6E. Let (S, δ) be as in Section 0H65, let p : X ⟶ Y be a morphism of schemes locally of finite type over S, let r ≥ 0 and let α ∈ z(X/Y, r) be a relative r-cycle on X/Y. Let (L, s, i : D ⟶ Y) be as in Chow Homology, Definition 02T8: L an invertible module on Y, s a global section and i the closed immersion of its zero scheme D. Form the cartesian square of Chow Homology, Remark 0B6Y,

E = X ×_Y D --j--> X
     |             |
     v             v
     D    --i-->   Y

so that j presents E as the zero scheme of the pulled-back section p^* s of p^* L. If L|_D ≅ 𝒪_D, then for every e ∈ ℤ and every β ∈ Z_{e+1}(Y) i^*α ∩ i^*β = j^*(α ∩ β) in Z_{r+e}(E), where ∩ is the action of Section 0H65, i^*α the base change of α along i, and i^* : Z_{e+1}(Y) ⟶ Z_e(D) and j^* : Z_{r+e+1}(X) ⟶ Z_{r+e}(E) the Gysin maps on cycles of Chow Homology, Remark 0B6Z, the latter read along the presentation j of the zero scheme of p^* s (Stacks.Chow.gysinCycleMapAlong). The triviality of (p^* L)|_E that j^* needs is not a hypothesis: it follows from that of L|_D.

theorem cap_baseChangeFamily_gysinCycleMap (C : ChowSituation.{u}) {X Y : Scheme.{u}}
    (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (p : X ⟶ Y) [LocallyOfFiniteType p] (r : ℕ) (e : ℤ)
    (α : FamilyOfCycles p r)
    (hα : letI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
      IsRelativeCycle p r α)
    (L : Y.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible Y.sheaf.obj Y.ringCatSheaf.property L]
    (s : Γ(L, ⊤))
    (htriv : AlgebraicGeometry.SheafOfModules.IsTrivial
      (Stacks.Divisors.zeroScheme Y L s).subscheme.sheaf.obj
      (Stacks.Divisors.zeroScheme Y L s).subscheme.ringCatSheaf.property
      ((Scheme.Modules.pullback (Stacks.Divisors.zeroScheme Y L s).subschemeι).obj L))
    (β : CycleGroup C sY (e + 1)) :
    cap C ((Stacks.Divisors.zeroScheme Y L s).subschemeι ≫ sY)
        (pullback.snd p (Stacks.Divisors.zeroScheme Y L s).subschemeι)
        (baseChangeFamily p (Stacks.Divisors.zeroScheme Y L s).subschemeι r α)
        (gysinCycleMap C sY e L s htriv β) =
      gysinCycleMapAlong C (p ≫ sY)
        (pullback.snd p (Stacks.Divisors.zeroScheme Y L s).subschemeι ≫
          (Stacks.Divisors.zeroScheme Y L s).subschemeι ≫ sY) ((r : ℤ) + e)
        ((Scheme.Modules.pullback p).obj L) (pullbackGlobalSections p L s)
        (pullback.fst p (Stacks.Divisors.zeroScheme Y L s).subschemeι)
        (Stacks.Divisors.isTrivial_pullback_zeroScheme_pullbackGlobalSections p L s htriv)
        (by rw [← Category.assoc, pullback.condition, Category.assoc])
        (Stacks.Divisors.zeroScheme_pullback p L s).symm
        (cycleGroupCongr C (p ≫ sY) (by ring) (cap C sY p α β))

Tag 0H6F, a proposition

Tag 0H6F in the Stacks Project.

Stacks.Chow.exists_bivariantClass_cap_mk_eq_relativeCycleCap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/RelativeCycleGysin.lean, line 649.

Stacks Project, Proposition 0H6F. Let (S, δ) be as in Section 0H65, let p : X ⟶ Y be a morphism of schemes locally of finite type over S, let r ≥ 0 and let α ∈ z(X/Y, r) be a relative r-cycle on X/Y. The rule that to every morphism g : Y' ⟶ Y locally of finite type and every k ∈ ℤ associates the operation g^*α ∩ - : Z_k(Y') ⟶ Z_{r + k}(X'), X' = Y' ×_Y X (Stacks.Chow.relativeCycleCap), factors through rational equivalence to define a bivariant class c(α) ∈ A^{-r}(X ⟶ Y): there is a bivariant class of degree -r for p whose cap operation on every test scheme sends the class of a cycle β to the class of g^*α ∩ β. The class is Stacks.Chow.relativeCycleBivariantClass.

theorem exists_bivariantClass_cap_mk_eq_relativeCycleCap :
    ∃ c : BivariantClass C (gysinSystemOfInvertible C) (p ≫ sY) sY p rfl (-(r : ℤ)),
      ∀ {T : Scheme.{u}} (g : T ⟶ Y) [LocallyOfFiniteType g] (k : ℤ)
        (β : CycleGroup C (g ≫ sY) k),
        c.cap g k (QuotientAddGroup.mk' (rationalEquivalences C (g ≫ sY) k) β) =
          QuotientAddGroup.mk' (rationalEquivalences C (pullback.fst p g ≫ p ≫ sY) (k - -(r : ℤ)))
            (cycleGroupCongr C _ (by ring) (relativeCycleCap C sY p r α g k β))

Tag 0H6G, a remark

Tag 0H6G in the Stacks Project.

Stacks.Chow.CompatibleCycleCapRule.exists_relativeCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/CycleCapRuleRelative.lean, line 185.

Stacks Project, Tag 0H6G. Let (S, δ) be as in Section 0H65, let p : X ⟶ Y be a morphism of schemes locally of finite type over S and let r ≥ 0. Let c be a rule that to every morphism g : Y' ⟶ Y locally of finite type and every e ∈ ℤ associates an operation c ∩ - : Z_e(Y') ⟶ Z_{r+e}(X'), X' = Y' ×_Y X, compatible with proper pushforward, flat pullback, and Gysin maps as in Lemma 0H6E (Stacks.Chow.CompatibleCycleCapRule). Then there is a relative r-cycle α on X/Y such that c ∩ - = g^*α ∩ - for every such g, where g^*α ∩ - is Stacks.Chow.relativeCycleCap.

theorem CompatibleCycleCapRule.exists_relativeCycle (C : ChowSituation.{u}) {X Y : Scheme.{u}}
    (sY : Y ⟶ C.S) [LocallyOfFiniteType sY] (p : X ⟶ Y) [LocallyOfFiniteType p] (r : ℕ)
    (c : CompatibleCycleCapRule C sY p r) :
    letI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian sY
    ∃ α ∈ relativeCycles p r, ∀ {Y' : Scheme.{u}} (g : Y' ⟶ Y) [LocallyOfFiniteType g] (e : ℤ),
      c.cap g e = relativeCycleCap C sY p r α g e

Sources

• Section 62.13, Tag 0H6C
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.properPushforward_gysinCycleMap · Stacks.Chow.cap_baseChangeFamily_gysinCycleMap · Stacks.Chow.exists_bivariantClass_cap_mk_eq_relativeCycleCap · Stacks.Chow.CompatibleCycleCapRule.exists_relativeCycle

Section62.14 Composition of families of cycles on fibres#

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

Tag 0H6I, a lemma

Tag 0H6I in the Stacks Project.

Stacks.Chow.compFamily_add_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Composition.lean, line 260. The attribute's comment: “additivity in the family on X/Y”.

Stacks Project, Tag 0H6I. The composition of families of cycles on fibres is additive in the family on X/Y: (α₁ + α₂) ∘ β = α₁ ∘ β + α₂ ∘ β.

theorem compFamily_add_left (f : X ⟶ Y) [LocallyOfFiniteType f] (g : Y ⟶ S)
    [LocallyOfFiniteType g] (r e : ℕ) (α₁ α₂ : FamilyOfCycles f r) (β : FamilyOfCycles g e) :
    compFamily f g r e (α₁ + α₂) β = compFamily f g r e α₁ β + compFamily f g r e α₂ β

Stacks.Chow.compFamily_add_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Composition.lean, line 272. The attribute's comment: “additivity in the family on Y/S”.

Stacks Project, Tag 0H6I. The composition of families of cycles on fibres is additive in the family on Y/S: α ∘ (β₁ + β₂) = α ∘ β₁ + α ∘ β₂.

theorem compFamily_add_right (f : X ⟶ Y) [LocallyOfFiniteType f] (g : Y ⟶ S)
    [LocallyOfFiniteType g] (r e : ℕ) (α : FamilyOfCycles f r) (β₁ β₂ : FamilyOfCycles g e) :
    compFamily f g r e α (β₁ + β₂) = compFamily f g r e α β₁ + compFamily f g r e α β₂

Tag 0H6J, a lemma

Tag 0H6J in the Stacks Project.

Stacks.Chow.restrictedFamily_compFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Composition.lean, line 295.

Stacks Project, Tag 0H6J. If U ⊆ X, V ⊆ Y and W ⊆ S are open with f(U) ⊆ V and g(V) ⊆ W, then the restriction of the composition α ∘ β to U is the composition of the restriction of α to the fibres of U/V with the restriction of β to the fibres of V/W. The source's statement is the case W = S.

theorem restrictedFamily_compFamily {U V W : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (g : Y ⟶ S) [LocallyOfFiniteType g] (fU : U ⟶ V) (gV : V ⟶ W) (j : U ⟶ X)
    [IsOpenImmersion j] (i : V ⟶ Y) [IsOpenImmersion i] (k : W ⟶ S) [IsOpenImmersion k]
    (hU : j ≫ f = fU ≫ i) (hV : i ≫ g = gV ≫ k) (r e : ℕ) (α : FamilyOfCycles f r)
    (β : FamilyOfCycles g e) :
    letI : LocallyOfFiniteType fU := by
      let : LocallyOfFiniteType (fU ≫ i) := hU ▸ inferInstance
      exact locallyOfFiniteType_of_comp fU i
    letI : LocallyOfFiniteType gV := by
      let : LocallyOfFiniteType (gV ≫ k) := hV ▸ inferInstance
      exact locallyOfFiniteType_of_comp gV k
    (restrictedFamily (f ≫ g) (fU ≫ gV) j k (comp_restrictionSquare hU hV) (r + e)
        (compFamily f g r e α β)).1 =
      compFamily fU gV r e (restrictedFamily f fU j i hU r α).1
        (restrictedFamily g gV i k hV e β).1

Tag 0H6K, a lemma

Tag 0H6K in the Stacks Project.

Stacks.Chow.compFamily_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/CompositionBaseChange.lean, line 353.

The formation of the composition α ∘ β of a family of r-cycles on the fibres of X/Y with a family of e-cycles on the fibres of Y/S is compatible with an arbitrary base change h : S' ⟶ S: the composition of the base change of α along Y ×_S S' ⟶ Y with the base change of β along h is the base change of α ∘ β along h, read on the fibre over a point t of S' through the canonical identification of (X ×_Y (Y ×_S S'))_t with (X ×_S S')_t.

theorem compFamily_baseChangeFamily (r e : ℕ) (α : FamilyOfCycles f r)
    (β : FamilyOfCycles g e) :
    compFamily (pullback.snd f (pullback.fst g h)) (pullback.snd g h) r e
        (baseChangeFamily f (pullback.fst g h) r α) (baseChangeFamily g h e β) t =
      fiberCycleRestrict (pullback.snd (f ≫ g) h)
        (pullback.snd f (pullback.fst g h) ≫ pullback.snd g h)
        (pullbackRightPullbackFstIso g h f).hom
        (pullbackRightPullbackFstIso_hom_snd g h f) t (r + e)
        (baseChangeFamily (f ≫ g) h (r + e) (compFamily f g r e α β) t)

Tag 0H6L, a lemma

Tag 0H6L in the Stacks Project.

Stacks.Chow.compFamily_familyAssociatedToModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ModuleComposition.lean, line 419.

Stacks Project, Tag 0H6L. Let f : X ⟶ Y and g : Y ⟶ S be morphisms of schemes, both locally of finite type, and let r, e ≥ 0. Let F be a quasi-coherent 𝒪_X-module of finite type whose support on every fibre of f has dimension at most r, and let G be a quasi-coherent 𝒪_Y-module of finite type whose support on every fibre of g has dimension at most e. Set α = [F/X/Y]_r and β = [G/Y/S]_e. If F is flat over Y then α ∘ β = [F ⊗_{𝒪_X} f^* G/X/S]_{r + e}.

theorem compFamily_familyAssociatedToModule {X Y S : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] (g : Y ⟶ S) [LocallyOfFiniteType g] (r e : ℕ) (F : X.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent]
    (hF : ∀ y : Y, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (f.fiberι y)).obj F)) ≤ (r : WithBot ℕ∞))
    (hflat : IsFlatOver f.toLRSHom.toShHom F) (G : Y.Modules) [G.IsFiniteType]
    [G.IsQuasicoherent]
    (hG : ∀ t : S, topologicalKrullDim
      (SheafOfModules.supp ((Scheme.Modules.pullback (g.fiberι t)).obj G)) ≤ (e : WithBot ℕ∞)) :
    compFamily f g r e (familyAssociatedToModule f F r hF)
        (familyAssociatedToModule g G e hG) =
      familyAssociatedToModule (f ≫ g) (tensorPullback f F G) (r + e)
        (fibreDim_tensorPullback_le f g r e F hF G hG)

Tag 0H6M, a lemma

Tag 0H6M in the Stacks Project.

Stacks.Chow.compFamily_familyAssociatedToClosedSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedSubschemeComposition.lean, line 182.

Stacks Project, Tag 0H6M. Let f : X ⟶ Y and g : Y ⟶ S be morphisms of schemes, both locally of finite type, and let r, e ≥ 0. Let Z ⊆ X be a closed subscheme of relative dimension at most r over Y, so that the fibres Z_y = Z ×_X X_y have dimension at most r, and let W ⊆ Y be a closed subscheme of relative dimension at most e over S. Set α = [Z/X/Y]_r and β = [W/Y/S]_e (Example 0H4S). If Z is flat over Y then α ∘ β = [Z ×_Y W/X/S]_{r + e}.

theorem compFamily_familyAssociatedToClosedSubscheme {X Y S Z W : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] (g : Y ⟶ S) [LocallyOfFiniteType g] (r e : ℕ) (i : Z ⟶ X)
    [IsClosedImmersion i] [Flat (i ≫ f)]
    (hZ : ∀ y : Y, topologicalKrullDim (pullback i (f.fiberι y) : Scheme.{u}) ≤ (r : WithBot ℕ∞))
    (j : W ⟶ Y) [IsClosedImmersion j]
    (hW : ∀ t : S,
      topologicalKrullDim (pullback j (g.fiberι t) : Scheme.{u}) ≤ (e : WithBot ℕ∞)) :
    compFamily f g r e (familyAssociatedToClosedSubscheme f i r)
        (familyAssociatedToClosedSubscheme g j e) =
      familyAssociatedToClosedSubscheme (f ≫ g) (pullback.fst (i ≫ f) j ≫ i) (r + e)

Tag 0H6N, a lemma

Tag 0H6N in the Stacks Project.

Stacks.Chow.properPushforwardFamily_compFamily_baseChangeFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/CompositionPushPull.lean, line 294.

Stacks Project, Tag 0H6N. Let S be a scheme, let

X' --f--> X
|         |
v         v
Y' --g--> Y

be a cartesian square of schemes locally of finite type over S with g proper, realized by the fibre product X' = X ×_Y Y' with f = pullback.fst, let r, e ≥ 0, let α be a family of r-cycles on the fibres of X/Y and let β' be a family of e-cycles on the fibres of Y'/S. Then

f_*(g^*α ∘ β') = α ∘ g_*β'

as families of (r + e)-cycles on the fibres of X/S, where ∘ is the composition Stacks.Chow.compFamily, g^* is Stacks.Chow.baseChangeFamily and f_*, g_* are Stacks.Chow.properPushforwardFamily.

theorem properPushforwardFamily_compFamily_baseChangeFamily {X Y Y' S : Scheme.{u}}
    (sY : Y ⟶ S) [LocallyOfFiniteType sY] (sY' : Y' ⟶ S) [LocallyOfFiniteType sY']
    (p : X ⟶ Y) [LocallyOfFiniteType p] (g : Y' ⟶ Y) [IsProper g] (hg : g ≫ sY = sY')
    (r e : ℕ) (α : FamilyOfCycles p r) (β' : FamilyOfCycles sY' e) :
    properPushforwardFamily (pullback.snd p g ≫ sY') (p ≫ sY) (pullback.fst p g)
        (pullbackFst_comp_eq_of_base g rfl hg) (r + e)
        (compFamily (pullback.snd p g) sY' r e (baseChangeFamily p g r α) β') =
      compFamily p sY r e α (properPushforwardFamily sY' sY g hg e β')

Tag 0H6P, a lemma

Tag 0H6P in the Stacks Project.

Stacks.Chow.cap_compFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/Composition.lean, line 378.

Stacks Project, Tag 0H6P. Associativity of the action of families of cycles on fibres: for α a family of r-cycles on the fibres of X/Y, β a family of e-cycles on the fibres of Y/S and γ a d-cycle on S, we have (α ∘ β) ∩ γ = α ∩ (β ∩ γ) in Z_{r + e + d}(X). Each side carries its δ-dimension in its own type, so the relation is stated between the underlying cycles on X.

theorem cap_compFamily (C : ChowSituation.{u}) (sS : S ⟶ C.S) [LocallyOfFiniteType sS]
    (f : X ⟶ Y) [LocallyOfFiniteType f] (g : Y ⟶ S) [LocallyOfFiniteType g] (r e : ℕ) {d : ℤ}
    (α : FamilyOfCycles f r) (β : FamilyOfCycles g e) (γ : CycleGroup C sS d) :
    (cap C sS (f ≫ g) (compFamily f g r e α β) γ : AlgebraicCycle X ℤ) =
      (cap C (g ≫ sS) f α (cap C sS g β γ) : AlgebraicCycle X ℤ)

Sources

• Section 62.14, Tag 0H6H
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.compFamily_add_left · Stacks.Chow.compFamily_add_right · Stacks.Chow.restrictedFamily_compFamily · Stacks.Chow.compFamily_baseChangeFamily · Stacks.Chow.compFamily_familyAssociatedToModule · Stacks.Chow.compFamily_familyAssociatedToClosedSubscheme · Stacks.Chow.properPushforwardFamily_compFamily_baseChangeFamily · Stacks.Chow.cap_compFamily

Section62.15 Composition of relative cycles#

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

Tag 0H6R, a lemma

Tag 0H6R in the Stacks Project.

Stacks.Chow.isRelativeCycle_compFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/CompositionRelativeCyclesGeneral.lean, line 210.

Stacks Project, Lemma 0H6R. Let X --f--> Y --g--> S be morphisms of schemes, both locally of finite type, with S locally Noetherian, and let r, e ≥ 0. If α is a relative r-cycle on X/Y and β is a relative e-cycle on Y/S, then the composition α ∘ β is a relative (r + e)-cycle on X/S.

Y is locally Noetherian because it is locally of finite type over the locally Noetherian scheme S, which is what makes the hypothesis on α meaningful.

theorem isRelativeCycle_compFamily {X Y S : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (g : Y ⟶ S) [LocallyOfFiniteType g] [IsLocallyNoetherian S] (r e : ℕ)
    (α : FamilyOfCycles f r) (β : FamilyOfCycles g e) :
    letI : IsLocallyNoetherian Y := LocallyOfFiniteType.isLocallyNoetherian g
    IsRelativeCycle f r α → IsRelativeCycle g e β →
      IsRelativeCycle (f ≫ g) (r + e) (compFamily f g r e α β)

Tag 0H6S, a lemma

Tag 0H6S in the Stacks Project.

Stacks.Chow.compFamily_familyAssociatedToSelf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/ClosedSubschemeComposition.lean, line 240.

Stacks Project, Tag 0H6S. Let f : X ⟶ Y and g : Y ⟶ S be morphisms of schemes, both locally of finite type and flat, of relative dimension r resp. e. Then the composition [X/X/Y]_r ∘ [Y/Y/S]_e of the families of cycles on fibres attached to the closed subschemes X ⊆ X and Y ⊆ Y (Example 0H4S) is the family [X/X/S]_{r + e}. The equality is one of families of cycles on fibres, so the local Noetherian hypothesis on S, needed only to speak of the group z(X/S, r + e) containing them, is not used.

theorem compFamily_familyAssociatedToSelf {X Y S : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [Flat f] (g : Y ⟶ S) [LocallyOfFiniteType g] [Flat g] (r e : ℕ)
    (hf : AlgebraicGeometry.RelativeDimension f r)
    (hg : AlgebraicGeometry.RelativeDimension g e) :
    compFamily f g r e (familyAssociatedToClosedSubscheme f (𝟙 X) r)
        (familyAssociatedToClosedSubscheme g (𝟙 Y) e) =
      familyAssociatedToClosedSubscheme (f ≫ g) (𝟙 X) (r + e)

Sources

• Section 62.15, Tag 0H6Q
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.isRelativeCycle_compFamily · Stacks.Chow.compFamily_familyAssociatedToSelf

Section62.17 Relative cycles in the non-Noetherian case#

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

Tag 0H6V, an equation

Tag 0H6V in the Stacks Project.

Stacks.Chow.HilbertCycleDatum, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/HilbertCycleClass.lean, line 203. The attribute's comment: “the set Hilb(X/S, r)”.

A member of Hilb(X/S, r): a closed subscheme Z ⊆ X, given by its ideal sheaf, whose structure morphism Z ⟶ S is flat, of finite presentation, and of relative dimension at most r.

structure HilbertCycleDatum {X S : Scheme.{u}} (f : X ⟶ S) (r : ℕ)

Stacks.Chow.cycleClassMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/HilbertCycleClass.lean, line 265. The attribute's comment: “the homomorphism”.

The cycle-class homomorphism from the free abelian group on Hilb(X/S, r) to the families of r-cycles on the fibres of X/S, sending ∑ nᵢ [Zᵢ] to ∑ nᵢ [Zᵢ/X/S]_r.

def cycleClassMap {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f] (r : ℕ) :
    FreeAbelianGroup (HilbertCycleDatum f r) →+ FamilyOfCycles f r

Stacks.Chow.cycleClassMap_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/HilbertCycleClass.lean, line 272. The attribute's comment: “on generators”.

On a generator the cycle-class homomorphism is the family of cycles [Z/X/S]_r of the closed subscheme.

theorem cycleClassMap_of {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f]
    (r : ℕ) (Z : HilbertCycleDatum f r) :
    cycleClassMap f r (FreeAbelianGroup.of Z) = Z.cycleFamily f

Tag 0H6W, a lemma

Tag 0H6W in the Stacks Project.

Stacks.Chow.comesFromNoetherianBase_iff_hasCompletelyDecomposedCycleClassCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/RelativeCycles/NonNoetherianBase.lean, line 255.

Stacks Project, Lemma 0H6W. Let S be a quasi-compact and quasi-separated scheme, let f : X ⟶ S be a morphism of finite presentation, let r ≥ 0 and let α be a family of r-cycles on the fibres of X/S. The following are equivalent:

1. there are a cartesian square with right-hand column a finite type morphism X₀ ⟶ S₀ of Noetherian schemes and α₀ ∈ z(X₀/S₀, r) such that α is the base change of α₀ by S ⟶ S₀;
2. there is a completely decomposed proper morphism g : S' ⟶ S of finite presentation such that g^*α is in the image of the cycle class map of Tag 0H6V.

Finite presentation of f is spelled LocallyOfFinitePresentation, QuasiCompact and QuasiSeparated, as in the source.

theorem comesFromNoetherianBase_iff_hasCompletelyDecomposedCycleClassCover {X S : Scheme.{u}}
    [CompactSpace S] [QuasiSeparatedSpace S] (f : X ⟶ S) [LocallyOfFinitePresentation f]
    [QuasiCompact f] [QuasiSeparated f] (r : ℕ) (α : FamilyOfCycles f r) :
    ComesFromNoetherianBase f r α ↔ HasCompletelyDecomposedCycleClassCover f r α

Sources

• Section 62.17, Tag 0H6U
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Chow.HilbertCycleDatum · Stacks.Chow.cycleClassMap · Stacks.Chow.cycleClassMap_of · Stacks.Chow.comesFromNoetherianBase_iff_hasCompletelyDecomposedCycleClassCover

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.