82.2 Setup to 82.18 Intersecting with an…

Section82.2 Setup#

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

Tag 0EDT, a situation

Tag 0EDT in the Stacks Project.

AlgebraicGeometry.Space.BaseSpaceDimensionSituation.IsGood, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/Setup.lean, line 59. The attribute's comment: “good_space”.

Stacks 0EDT. An algebraic space over the fixed base is good when its structure morphism is quasi-separated and locally of finite type.

abbrev BaseSpaceDimensionSituation.IsGood (D : BaseSpaceDimensionSituation.{u})
    {X : (BigFppfOver D.site D.base D.base_mem)ᵒᵖ ⥤ Type u}
    (f : X ⟶ D.space) : Prop

Declarations registered for the tag:

Tag 0EDU, a remark

Tag 0EDU in the Stacks Project.

AlgebraicGeometry.Space.BaseSpaceDimensionSituation.stacksSober_points_of_isGood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/Decency.lean, line 104.

Stacks 0EDU. The point space of a good algebraic space over the base of Situation 0EDT is sober: every irreducible closed subset of it has a unique generic point.

A good algebraic space is decent, and the point space of a decent algebraic space is Kolmogorov by Stacks 03K3 and quasi-sober by Stacks 03K6.

theorem BaseSpaceDimensionSituation.stacksSober_points_of_isGood (f : X ⟶ D.space)
    (hgood : D.IsGood f) :
    StacksSober (points D.site D.base D.base_mem X)
Tag 0EDV, a remark

Tag 0EDV in the Stacks Project.

AlgebraicGeometry.Space.isIntegralSpace_iff_isReduced_and_irreducibleSpace_of_isGood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/IntegralGoodSpace.lean, line 97. The attribute's comment: “integral iff reduced and irreducible”.

Stacks 0EDV. A good algebraic space over the fixed base is integral exactly when it is reduced and its space of points is irreducible: the third condition of integrality, decency, holds for every good algebraic space.

theorem isIntegralSpace_iff_isReduced_and_irreducibleSpace_of_isGood (f : X ⟶ D.space)
    (hf : D.IsGood f) :
    IsIntegralSpace D.site D.base D.base_mem X ↔
      HasEtaleLocalProperty D.site D.base D.base_mem X (fun Y : Scheme.{u} => IsReduced Y) ∧
        IrreducibleSpace (points D.site D.base D.base_mem X)

AlgebraicGeometry.Space.existsUnique_integralClosedSubspace_isGenericPoint_of_isGood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/IntegralGoodSpace.lean, line 107. The attribute's comment: “unique integral closed subspace with a given generic point”.

Stacks 0EDV. Every point of a good algebraic space over the fixed base is the generic point of the set of points of exactly one integral closed subspace.

theorem existsUnique_integralClosedSubspace_isGenericPoint_of_isGood (f : X ⟶ D.space)
    (hf : D.IsGood f) (ξ : points D.site D.base D.base_mem X) :
    ∃! Z : IntegralClosedSubspace D.site D.base D.base_mem X,
      IsGenericPoint ξ
        (Set.range (pointsMap D.site D.base D.base_mem Z.subspace.toFunctor Z.subspace.ι))
Tag 0EDW, a lemma

Tag 0EDW in the Stacks Project.

AlgebraicGeometry.Space.deltaDimension_eq_inducedDimensionValue, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/JacobsonDeltaDimension.lean, line 396. The attribute's comment: “part (1): the common value is the induced delta function at the generic point”.

Stacks 0EDW, part (1). The common value is δ(ξ) = δ_{X/B}(ξ), for ξ the generic point of |Z|: the δ-dimension of Z is the value at ξ of the dimension function δ_{X/B} of Stacks 0EDN, the value of δ at the image of ξ plus the transcendence degree of ξ over that image, and it is a nonnegative integer.

theorem deltaDimension_eq_inducedDimensionValue :
    0 ≤ deltaDimension D sX Z ∧
      deltaDimension D sX Z = inducedDimensionValue D.site D.base D.base_mem D.delta sX
        (pointsMap D.site D.base D.base_mem Z.subspace.toFunctor Z.subspace.ι
          (Z.genericPoint D.site D.base D.base_mem))

AlgebraicGeometry.Space.codimension_singleton_eq_deltaDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/JacobsonDeltaDimension.lean, line 409. The attribute's comment: “part (3): the codimension of a closed point of the integral closed subspace is the value of the induced delta function at its generic point”.

Stacks 0EDW, parts (1) and (3). Over a Jacobson base whose dimension function vanishes at closed points, the codimension of a closed point of the set of points of an integral closed subspace Z of a good algebraic space is the δ-dimension of Z, the value of δ_{X/B} at the generic point of Z; in particular that integer is nonnegative.

theorem codimension_singleton_eq_deltaDimension
    (z : points D.site D.base D.base_mem Z.subspace.toFunctor)
    (hz : IsClosed ({z} : Set (points D.site D.base D.base_mem Z.subspace.toFunctor))) :
    0 ≤ deltaDimension D sX Z ∧
      codimension (⟨{z}, isIrreducible_singleton, hz⟩ :
          IrreducibleCloseds (points D.site D.base D.base_mem Z.subspace.toFunctor)) =
        ((deltaDimension D sX Z).toNat : ℕ∞)

AlgebraicGeometry.Space.topologicalKrullDim_points_eq_deltaDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/JacobsonDeltaDimension.lean, line 424. The attribute's comment: “part (2): the dimension of the set of points of the integral closed subspace is the value of the induced delta function at its generic point”.

Stacks 0EDW, parts (1) and (2). Over a Jacobson base whose dimension function vanishes at closed points, the dimension of the set of points of an integral closed subspace Z of a good algebraic space is the δ-dimension of Z, a nonnegative integer.

theorem topologicalKrullDim_points_eq_deltaDimension :
    0 ≤ deltaDimension D sX Z ∧
      topologicalKrullDim (points D.site D.base D.base_mem Z.subspace.toFunctor) =
        (((deltaDimension D sX Z).toNat : ℕ∞) : WithBot ℕ∞)

AlgebraicGeometry.Space.localRingDimension_eq_deltaDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/JacobsonDeltaDimension.lean, line 436. The attribute's comment: “part (4): the dimension of the local ring at a closed point is the value of the induced delta function at the generic point”.

Stacks 0EDW, parts (1) and (4). Over a Jacobson base whose dimension function vanishes at closed points, the dimension of the local ring of an integral closed subspace Z of a good algebraic space at a closed point of |Z| is the δ-dimension of Z, a nonnegative integer.

theorem localRingDimension_eq_deltaDimension
    (z : points D.site D.base D.base_mem Z.subspace.toFunctor)
    (hz : IsClosed ({z} : Set (points D.site D.base D.base_mem Z.subspace.toFunctor))) :
    0 ≤ deltaDimension D sX Z ∧
      localRingDimension D.site D.base D.base_mem z = ((deltaDimension D sX Z).toNat : ℕ∞)

AlgebraicGeometry.Space.ringKrullDim_etaleLocalRing_eq_deltaDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/JacobsonDeltaDimension.lean, line 450. The attribute's comment: “part (5): the dimension of the étale local ring at a geometric point above a closed point is the value of the induced delta function at the generic point”.

Stacks 0EDW, parts (1) and (5). Over a Jacobson base whose dimension function vanishes at closed points, the Krull dimension of the étale local ring of an integral closed subspace Z of a good algebraic space at a geometric point above a closed point of |Z| is the δ-dimension of Z, a nonnegative integer.

theorem ringKrullDim_etaleLocalRing_eq_deltaDimension
    (z : points D.site D.base D.base_mem Z.subspace.toFunctor)
    (hz : IsClosed ({z} : Set (points D.site D.base D.base_mem Z.subspace.toFunctor)))
    (zbar : GeometricPoint D.site D.base D.base_mem Z.subspace.toFunctor)
    (hzbar : zbar.LiesOver z) :
    0 ≤ deltaDimension D sX Z ∧
      ringKrullDim (etaleLocalRing D.site D.base D.base_mem Z.subspace.toFunctor zbar) =
        (((deltaDimension D sX Z).toNat : ℕ∞) : WithBot ℕ∞)
Tag 0EDX, a definition

Tag 0EDX in the Stacks Project.

AlgebraicGeometry.Space.deltaDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/Cycles.lean, line 252. The attribute's comment: “the δ-dimension of an integral closed subspace”.

Stacks 0EDX, for an integral closed subspace. The δ-dimension of an integral closed subspace Z of a good algebraic space X/B is the value of δ_{X/B} at the generic point of |Z|.

noncomputable def deltaDimension (D : BaseSpaceDimensionSituation.{u})
    {X : (BigFppfOver D.site D.base D.base_mem)ᵒᵖ ⥤ Type u} (sX : X ⟶ D.space)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem X) : ℤ

AlgebraicGeometry.Space.deltaDimensionIrreducible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/DeltaDimension.lean, line 103. The attribute's comment: “irreducible closed subsets”.

Stacks 0EDX. The δ-dimension of an irreducible closed subset of the space of points of a good algebraic space: the induced dimension function at the generic point of the subset.

noncomputable def deltaDimensionIrreducible (f : X ⟶ D.space) (hf : D.IsGood f)
    (T : IrreducibleCloseds (points D.site D.base D.base_mem X)) : ℤ

AlgebraicGeometry.Space.deltaDimensionClosed, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/DeltaDimension.lean, line 113. The attribute's comment: “closed subsets”.

Stacks 0EDX. The δ-dimension of an arbitrary closed subset of the space of points of a good algebraic space: the supremum, among the extended integers, of the δ-dimensions of its irreducible components.

noncomputable def deltaDimensionClosed (f : X ⟶ D.space) (hf : D.IsGood f)
    (T : Set (points D.site D.base D.base_mem X)) (hT : IsClosed T) : EInt

AlgebraicGeometry.Space.deltaDimensionSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/DeltaDimension.lean, line 124. The attribute's comment: “closed subspaces”.

Stacks 0EDX. The δ-dimension of a closed subspace of a good algebraic space: the δ-dimension of its set of points.

noncomputable def deltaDimensionSubspace (f : X ⟶ D.space) (hf : D.IsGood f) (Z : Subfunctor X)
    (hZ : IsClosedSubspace D.site D.base D.base_mem Z) : EInt
Sources

Section82.3 Cycles#

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

Tag 0EDZ, a definition

Tag 0EDZ in the Stacks Project.

AlgebraicGeometry.Space.cyclesOfDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/Cycles.lean, line 296. The attribute's comment: “parts (1) and (2): cycles and k-cycles”. References: EGA IV (21.6.1), “fixed δ-dimension k”.

Stacks 0EDZ, parts (1) and (2). The subgroup Z_k(X) of integer coefficient families on the integral closed subspaces of a good algebraic space X/B which are cycles — the point sets of the subspaces with nonzero coefficient form a locally finite collection of subsets of |X| — and are of δ-dimension k — every subspace with nonzero coefficient has δ-dimension k.

noncomputable def cyclesOfDimension (sX : X ⟶ D.space) (k : ℤ) :
    AddSubgroup (IntegralClosedSubspace D.site D.base D.base_mem X → ℤ)

AlgebraicGeometry.Space.CycleGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/Cycles.lean, line 340. The attribute's comment: “part (3): the abelian group of k-cycles”.

Stacks 0EDZ, part (3). The abelian group Z_k(X) of k-cycles on a good algebraic space X/B.

noncomputable abbrev CycleGroup (sX : X ⟶ D.space) (k : ℤ)
Sources

Section82.4 Multiplicities#

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

Tag 0EE1, a lemma

Tag 0EE1 in the Stacks Project.

AlgebraicGeometry.Space.geometricLength_eq_iff_forall_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricLengthPointIndependence.lean, line 168. The attribute's comment: “conditions (1) and (3)”.

Stacks 0EE1, conditions (1) and (3). The length of a quasi-coherent F at a geometric point x̄ is d exactly when the length of the Zariski stalk of φ^* F is d at the point of the chart under the chosen lift, for every small étale neighbourhood of x̄ whose chart is a scheme.

Every neighbourhood computes the same length (AlgebraicGeometry.Space.geometricLength_eq_chartZariskiLength), and there is one (AlgebraicGeometry.Space.nonempty_smallEtaleNeighborhood).

theorem geometricLength_eq_iff_forall_etaleChart {x : GeometricPoint B S hS X}
    (F : Modules.{u, u} B S hS X hX) [F.IsQuasicoherentOnSite] (d : ℕ∞) :
    geometricLength B S hS ⟨X, hX⟩ x F = d ↔
      ∀ V : SmallEtaleNeighborhood x,
        chartZariskiLength.{u, u} B S hS hX V.chart (chartPoint B S hS X V) F = d

AlgebraicGeometry.Space.geometricLength_eq_iff_exists_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricLengthPointIndependence.lean, line 185. The attribute's comment: “conditions (1) and (2)”.

Stacks 0EE1, conditions (1) and (2). The length of a quasi-coherent F at a geometric point x̄ is d exactly when the length of the Zariski stalk of φ^* F is d at the point of the chart under the chosen lift, for some small étale neighbourhood of x̄ whose chart is a scheme.

Together with AlgebraicGeometry.Space.geometricLength_eq_iff_forall_etaleChart this is the exchange of quantifiers which Stacks 0EE1 asserts: the length agrees on some étale scheme chart exactly when it agrees on every one.

theorem geometricLength_eq_iff_exists_etaleChart {x : GeometricPoint B S hS X}
    (F : Modules.{u, u} B S hS X hX) [F.IsQuasicoherentOnSite] (d : ℕ∞) :
    geometricLength B S hS ⟨X, hX⟩ x F = d ↔
      ∃ V : SmallEtaleNeighborhood x,
        chartZariskiLength.{u, u} B S hS hX V.chart (chartPoint B S hS X V) F = d

AlgebraicGeometry.Space.geometricLength_eq_of_image_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricLengthPointIndependence.lean, line 238. The attribute's comment: “independence of the chosen geometric point above a point of the space”.

Stacks 0EE1: the length at a geometric point does not depend on the geometric point. Let F be a quasi-coherent 𝒪_X-module and let x̄ and ȳ be geometric points of X lying over the same point x of |X|. Then F has the same length at x̄ as at ȳ. So the length of Stacks 0EE2 is a function of x, which is what makes that definition well posed.

The two points are dominated by a common third (AlgebraicGeometry.Space.GeometricPoint.exists_common_extension), and the length is unchanged along a domination (AlgebraicGeometry.Space.geometricLength_eq_of_dominates).

theorem geometricLength_eq_of_image_eq (x y : GeometricPoint B S hS X)
    (h : x.image = y.image) (F : Modules.{u, u} B S hS X hX)
    [F.IsQuasicoherentOnSite] :
    geometricLength B S hS ⟨X, hX⟩ x F = geometricLength B S hS ⟨X, hX⟩ y F

AlgebraicGeometry.Space.length_etaleLocalRing_eq_length_chartLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricStalkLength.lean, line 93. The attribute's comment: “the structure sheaf: lengths agree on an étale scheme chart”.

Stacks 0EE1 for the structure sheaf. The étale local ring of an algebraic space at a geometric point has the same length as the local ring of any étale scheme chart at a point over it. Since the chart is arbitrary, the two readings of Stacks 0EE1 — some chart and every chart — agree, and the common value is the length of 𝒪_{X, x̄}.

This is the case N = 𝒪_{U, u} of AlgebraicGeometry.Space.length_chartStalkBaseChange_obj, the base change 𝒪_{X, x̄} ⊗_{𝒪_{U, u}} 𝒪_{U, u} being 𝒪_{X, x̄}.

theorem length_etaleLocalRing_eq_length_chartLocalRing {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) :
    Module.length ↥(etaleLocalRing B S hS X x) ↥(etaleLocalRing B S hS X x) =
      Module.length ↥(chartLocalRing B S hS X V) ↥(chartLocalRing B S hS X V)

AlgebraicGeometry.Space.tfae_hasLengthAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LengthAtPoint.lean, line 200.

Stacks 0EE1 at a point x of |X|: conditions (1), (2) and (3) are equivalent. For a quasi-coherent 𝒪_X-module F, a point x ∈ |X| and d ∈ ℕ∞, the following are equivalent:

  1. length_{𝒪_{X, x̄}} F_{x̄} = d for a geometric point x̄ above x;
  2. for some étale morphism U → X with U a scheme and u ∈ U mapping to x, length_{𝒪_{U, u}} (F|_U)_u = d;
  3. for every étale morphism U → X with U a scheme and u ∈ U mapping to x, length_{𝒪_{U, u}} (F|_U)_u = d.

Condition (1) is AlgebraicGeometry.Space.HasLengthAt by definition, so this is the statement that AlgebraicGeometry.Space.HasLengthAt is "the equivalent conditions of Lemma 0EE1", as Stacks 0EE2 has it. Together with AlgebraicGeometry.Space.geometricLength_eq_of_image_eq (condition (1) does not depend on the geometric point chosen above x) this is the whole of Stacks 0EE1.

theorem tfae_hasLengthAt (F : Modules.{u, u} B S hS X hX) [F.IsQuasicoherentOnSite]
    (x : points B S hS X) (d : ℕ∞) :
    List.TFAE
      [∃ xbar : GeometricPoint B S hS X,
          xbar.LiesOver x ∧ geometricLength B S hS ⟨X, hX⟩ xbar F = d,
        ∃ (W : SmallEtale B S hS X) (u : chartScheme W), chartSchemeToPoints B S hS X W u = x ∧
          Module.length ((chartScheme W).presheaf.stalk u)
            (TopCat.Presheaf.stalk (C := AddCommGrpCat.{u})
              (restrictToChart B S hS hX F W).val.presheaf u) = d,
        ∀ (W : SmallEtale B S hS X) (u : chartScheme W), chartSchemeToPoints B S hS X W u = x →
          Module.length ((chartScheme W).presheaf.stalk u)
            (TopCat.Presheaf.stalk (C := AddCommGrpCat.{u})
              (restrictToChart B S hS hX F W).val.presheaf u) = d]
Tag 0EE2, a definition

Tag 0EE2 in the Stacks Project.

AlgebraicGeometry.Space.geometricLength, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricLength.lean, line 98. The attribute's comment: “at a geometric point; no declaration packages a chosen geometric point above a point of |X| together with the independence of Lemma 0EE1 (AlgebraicGeometry.Space.geometricLength_eq_of_image_eq) into the definition at a point of |X|”.

The length of an 𝒪_X-module at a geometric point. For an algebraic space X over a scheme S, a geometric point x̄ of X and an 𝒪_X-module F, this is the length of the stalk F_{x̄} of Stacks 05VQ as a module over the étale local ring 𝒪_{X, x̄} of Stacks 04KG, a value in ℕ∞ = {0, 1, 2, …, ∞}.

This is the quantity of condition (1) of Stacks 0EE1; Stacks 0EE2 defines "F has length d at a point x of |X|" to mean that this value is d for a geometric point above x, which by Stacks 0EE1 does not depend on the choice — proved, for a quasi-coherent F, as AlgebraicGeometry.Space.geometricLength_eq_of_image_eq in GeometricLengthPointIndependence.lean.

def geometricLength (X : AlgebraicSpaces B S hS) (x : GeometricPoint B S hS X.1)
    (F : Modules.{u, m} B S hS X.1 X.2) : ℕ∞

AlgebraicGeometry.Space.HasLengthAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LengthAtPoint.lean, line 102.

Stacks 0EE2: F has length d at x. For a quasi-coherent 𝒪_X-module F, a point x of |X| and d ∈ ℕ∞, this says that the stalk F_{x̄} has length d over the étale local ring 𝒪_{X, x̄} for a geometric point x̄ of X lying over x.

Stacks 0EE2 defines this as the equivalent conditions of Stacks 0EE1; the definition uses condition (1), which by that lemma does not depend on the choice of x̄ (AlgebraicGeometry.Space.geometricLength_eq_of_image_eq, so the condition holds for some x̄ above x iff for every one: AlgebraicGeometry.Space.hasLengthAt_iff_forall_geometricPoint) and is equivalent to conditions (2) and (3), the length of (F|_U)_u over 𝒪_{U, u} for some, respectively every, étale U → X from a scheme and u ∈ U over x (AlgebraicGeometry.Space.tfae_hasLengthAt).

def HasLengthAt (F : Modules.{u, u} B S hS X hX) [F.IsQuasicoherentOnSite]
    (x : points B S hS X) (d : ℕ∞) : Prop
Tag 0EE3, a lemma

Tag 0EE3 in the Stacks Project.

AlgebraicGeometry.Space.geometricLength_chartDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionGeometricLength.lean, line 450. The attribute's comment: “at a geometric point of the source, and for the direct image of modules along base change of étale scheme charts; the form at a point of the space is AlgebraicGeometry.Space.lengthAtPoint_chartDirectImage_iff of StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionLengthAtPoint.lean”.

Stacks 0EE3 for algebraic spaces, at a geometric point. Let f : X ⟶ Y be a closed immersion of algebraic spaces over a scheme S, let G be an 𝒪_X-module and let x̄ be a geometric point of X. Then f_*G has the same length at f(x̄) as G has at x̄.

The germ map 𝒪_{Y, f(x̄)} → 𝒪_{X, x̄} of a closed immersion is surjective (AlgebraicGeometry.Space.surjective_etaleLocalRingMap_of_isClosedImmersion) and the stalk of f_*G at f(x̄) is the stalk of G at x̄ semilinearly over it (AlgebraicGeometry.Space.geometricStalkPushforwardAddEquiv), so AlgebraicGeometry.Space.geometricLength_eq_of_surjective_of_addEquiv applies: restriction of scalars along a surjection does not change the lattice of submodules, hence not its length.

No quasi-coherence of G is assumed. The direct image is the one along base change of étale scheme charts; see the implementation notes of this file.

theorem geometricLength_chartDirectImage (f : X ⟶ Y) (hf : IsClosedImmersion B S hS f.hom)
    (x : GeometricPoint B S hS X.1) (G : Modules.{u, m} B S hS X.1 X.2) :
    geometricLength B S hS Y (geometricPointMap f.hom x)
        ((smallBaseChangeModulePushforward B S hS f hf.rep).obj G) =
      geometricLength B S hS X x G

AlgebraicGeometry.Space.geometricLength_chartDirectImage_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionGeometricLength.lean, line 470. The attribute's comment: “at a geometric point of the source, and for the direct image of modules along base change of étale scheme charts; the form at a point of the space is AlgebraicGeometry.Space.lengthAtPoint_chartDirectImage_iff of StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionLengthAtPoint.lean”.

Stacks 0EE3 for algebraic spaces, at a geometric point, in the iff form of the source: for every d in ℕ∞ = {0, 1, 2, …, ∞}, the module G has length d at the geometric point x̄ of X exactly when f_*G has length d at f(x̄).

This is AlgebraicGeometry.Space.geometricLength_chartDirectImage read as an equivalence.

theorem geometricLength_chartDirectImage_iff (f : X ⟶ Y)
    (hf : IsClosedImmersion B S hS f.hom) (x : GeometricPoint B S hS X.1)
    (G : Modules.{u, m} B S hS X.1 X.2) (d : ℕ∞) :
    geometricLength B S hS X x G = d ↔
      geometricLength B S hS Y (geometricPointMap f.hom x)
        ((smallBaseChangeModulePushforward B S hS f hf.rep).obj G) = d

AlgebraicGeometry.Space.lengthAtPoint_chartDirectImage_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionLengthAtPoint.lean, line 226. The attribute's comment: “at a point of the space, for the direct image of modules along base change of étale scheme charts”.

Stacks 0EE3 at a point of the space. Let f : X ⟶ Y be a closed immersion of algebraic spaces over a scheme S, let G be a quasi-coherent 𝒪_X-module, let p be a point of |X| with image f(p) in |Y| and let d be an element of ℕ∞ = {0, 1, 2, …, ∞}. Then G has length d at p if and only if f_*G has length d at f(p).

"Has length d at a point" is the condition of Stacks 0EE2: the length of the module at that point of the space, AlgebraicGeometry.Space.lengthAtPoint, is d. Both sides are therefore = d for one and the same number, by AlgebraicGeometry.Space.lengthAtPoint_chartDirectImage.

theorem lengthAtPoint_chartDirectImage_iff (f : X ⟶ Y)
    (hf : IsClosedImmersion B S hS f.hom) (G : Modules.{u, u} B S hS X.1 X.2)
    [G.IsQuasicoherentOnSite] (p : points B S hS X.1) (d : ℕ∞) :
    lengthAtPoint B S hS X p G = d ↔
      lengthAtPoint B S hS Y (pointsMap B S hS X.1 f.hom p)
        (chartDirectImage B S hS f hf G) = d

Stacks.ClosedImmersion.length_stalkObj_pushforward_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/StalkLength.lean, line 186. The attribute's comment: “for a closed immersion of schemes”.

Stacks 0EE3 for a closed immersion of schemes, in the form the source states: for d ∈ {0, 1, 2, …, ∞}, the module G has length d at z if and only if i_* G has length d at the image i(z).

Both sides are read off Stacks.ClosedImmersion.length_stalkObj_pushforward, which says the two lengths are equal.

theorem length_stalkObj_pushforward_eq_iff {Z X : Scheme.{u}} (i : Z ⟶ X)
    [IsClosedImmersion i] (G : Z.Modules) (z : Z) (d : ℕ∞) :
    Module.length (TopCat.Presheaf.stalk (C := RingCat.{u}) Z.ringCatSheaf.obj z)
          (SheafOfModules.stalkObj Z.ringCatSheaf z G) = d ↔
      Module.length (TopCat.Presheaf.stalk (C := RingCat.{u}) X.ringCatSheaf.obj (i.base z))
          (SheafOfModules.stalkObj X.ringCatSheaf (i.base z)
            ((Scheme.Modules.pushforward i).obj G)) = d
Tag 0EE4, a lemma

Tag 0EE4 in the Stacks Project.

AlgebraicGeometry.Space.isDecentSpace_iff_isAbsolutelyQuasiSeparated_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicityAtPoint.lean, line 126. The attribute's comment: “decent iff quasi-separated”.

The parenthetical of Stacks 0EE4. A locally Noetherian algebraic space over S is decent if and only if it is quasi-separated.

Decency of a quasi-separated algebraic space is the chain of conditions of Stacks 03JX and needs no finiteness hypothesis; quasi-separatedness of a locally Noetherian decent algebraic space is Stacks 0BB6.

theorem isDecentSpace_iff_isAbsolutelyQuasiSeparated_of_isLocallyNoetherian
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hNoeth : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} => IsLocallyNoetherian Y)) :
    IsDecentSpace B S hS X ↔ IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X

AlgebraicGeometry.Space.tfae_isGenericPoint_supp_restrictToChart_geometricLength, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicityAtPoint.lean, line 325. The attribute's comment: “conditions (1), (2) and (3)”.

Stacks 0EE4, conditions (1), (2) and (3). Let X be a locally Noetherian algebraic space over S, let F be a coherent 𝒪_X-module and let x ∈ |X|. The following are equivalent:

  1. for some étale morphism U → X with U a scheme and some u ∈ U mapping to x, the point u is a generic point of an irreducible component of Supp(F|_U);
  2. for every étale morphism U → X with U a scheme and every u ∈ U mapping to x, the point u is a generic point of an irreducible component of Supp(F|_U);
  3. the length of F at x is finite and nonzero.

The étale morphisms from schemes are the étale scheme charts W of X, and u maps to x when AlgebraicGeometry.Space.chartSchemeToPoints sends it to x. The length of F at x is the length of Stacks 0EE2: the length at a geometric point above x, which by Stacks 0EE1 (AlgebraicGeometry.Space.geometricLength_eq_of_image_eq) does not depend on the geometric point; condition (3) is stated at every geometric point above x.

Each chart point above x satisfies the chart condition exactly when the length is finite and nonzero (AlgebraicGeometry.Space.exists_isGenericPoint_supp_restrictToChart_iff_geometricLength), and a chart point above x exists.

theorem tfae_isGenericPoint_supp_restrictToChart_geometricLength
    (hLN : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) [IsCoherent B S hS X.1 X.2 F]
    (x : points B S hS X.1) :
    List.TFAE
      [∃ (W : SmallEtale B S hS X.1) (u : chartScheme W),
          chartSchemeToPoints B S hS X.1 W u = x ∧
            ∃ Z : irreducibleComponents
                (SheafOfModules.supp (restrictToChart B S hS X.2 F W) : Set (chartScheme W)),
              IsGenericPoint u (Subtype.val '' Z.1),
        ∀ (W : SmallEtale B S hS X.1) (u : chartScheme W),
          chartSchemeToPoints B S hS X.1 W u = x →
            ∃ Z : irreducibleComponents
                (SheafOfModules.supp (restrictToChart B S hS X.2 F W) : Set (chartScheme W)),
              IsGenericPoint u (Subtype.val '' Z.1),
        ∀ xbar : GeometricPoint B S hS X.1, xbar.LiesOver x →
          geometricLength B S hS X xbar F ≠ ⊤ ∧ 0 < geometricLength B S hS X xbar F]

AlgebraicGeometry.Space.tfae_isGenericPoint_supportOfSheaf_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicityAtPoint.lean, line 451. The attribute's comment: “conditions (1) to (4), for a decent space”.

Stacks 0EE4, conditions (1) to (4), for a decent space. Let X be a locally Noetherian algebraic space over S which is decent (equivalently, by AlgebraicGeometry.Space.isDecentSpace_iff_isAbsolutelyQuasiSeparated_of_isLocallyNoetherian, quasi-separated), let F be a coherent 𝒪_X-module and let x ∈ |X|. The three conditions of AlgebraicGeometry.Space.tfae_isGenericPoint_supp_restrictToChart_geometricLength are also equivalent to

  1. x is a generic point of an irreducible component of Supp(F).

The support of F is the support of Stacks 04KA of its underlying sheaf of abelian groups (AlgebraicGeometry.Space.supportOfSheaf). Condition (4) is equivalent to the chart condition at every chart point above x (AlgebraicGeometry.Space.exists_isGenericPoint_supp_restrictToChart_iff_supportOfSheaf).

theorem tfae_isGenericPoint_supportOfSheaf_of_isDecentSpace
    (hLN : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hdec : IsDecentSpace B S hS X.1) (F : Modules.{u, u} B S hS X.1 X.2)
    [IsCoherent B S hS X.1 X.2 F] (x : points B S hS X.1) :
    List.TFAE
      [∃ (W : SmallEtale B S hS X.1) (u : chartScheme W),
          chartSchemeToPoints B S hS X.1 W u = x ∧
            ∃ Z : irreducibleComponents
                (SheafOfModules.supp (restrictToChart B S hS X.2 F W) : Set (chartScheme W)),
              IsGenericPoint u (Subtype.val '' Z.1),
        ∀ (W : SmallEtale B S hS X.1) (u : chartScheme W),
          chartSchemeToPoints B S hS X.1 W u = x →
            ∃ Z : irreducibleComponents
                (SheafOfModules.supp (restrictToChart B S hS X.2 F W) : Set (chartScheme W)),
              IsGenericPoint u (Subtype.val '' Z.1),
        ∀ xbar : GeometricPoint B S hS X.1, xbar.LiesOver x →
          geometricLength B S hS X xbar F ≠ ⊤ ∧ 0 < geometricLength B S hS X xbar F,
        ∃ Z : irreducibleComponents
            (supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F)),
          IsGenericPoint x (Subtype.val '' Z.1)]
Tag 0EE6, a lemma

Tag 0EE6 in the Stacks Project.

AlgebraicGeometry.Space.isGenericPoint_of_deltaDimensionClosed_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MaximalDeltaDimension.lean, line 60.

Stacks 0EE6. A point of a closed set of points at which the induced dimension function attains the delta-dimension bound is a generic point of an irreducible component of that set.

theorem isGenericPoint_of_deltaDimensionClosed_le (f : X ⟶ D.space) (hf : D.IsGood f)
    (T : Set (points D.site D.base D.base_mem X)) (hT : IsClosed T)
    (t : points D.site D.base D.base_mem X) (ht : t ∈ T) (k : ℤ)
    (hbound : deltaDimensionClosed D f hf T hT ≤ (k : EInt))
    (hdim : inducedDimensionValue D.site D.base D.base_mem D.delta f t = k) :
    ∃ Z : irreducibleComponents T, IsGenericPoint (⟨t, ht⟩ : T) Z.1
Sources

Section82.5 Cycle associated to a closed subspace#

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

Tag 0EE8, a remark

Tag 0EE8 in the Stacks Project.

AlgebraicGeometry.Space.IsIrreducibleComponent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/CycleOfClosedSubspace.lean, line 64. The attribute's comment: “irreducible_component_of_closed_subspace”.

Stacks 0EE8. An irreducible component of an algebraic space Y over S is a closed subspace which is an integral algebraic space and whose set of points is an irreducible component of |Y|.

abbrev IsIrreducibleComponent (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (_hY : IsAlgebraicSpace B S hS Y)
    (Z : Subfunctor Y) : Prop

AlgebraicGeometry.Space.IsGenericPointOf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/CycleOfClosedSubspace.lean, line 73. The attribute's comment: “irreducible_component_of_closed_subspace”.

Stacks 0EE8. A point of an algebraic space Y over S is the generic point of a subspace Z when it is the generic point of the set of points of Z.

abbrev IsGenericPointOf (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (_hY : IsAlgebraicSpace B S hS Y)
    (Z : Subfunctor Y) (ξ : points B S hS Y) : Prop
Tag 0EE9, a definition

Tag 0EE9 in the Stacks Project.

AlgebraicGeometry.Space.closedSubspaceCycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ClosedSubspaceCycle.lean, line 183. The attribute's comment: “part (2): the k-cycle [Y]_k of a closed subspace; the multiplicity at each point is independent of the choice of geometric representative by Lemma 0EE1 (closedSubspaceMultiplicity_eq_toNat_geometricLength) and positive by Lemma 0EE4 (closedSubspaceMultiplicity_pos)”.

In Situation 0EDT let X/B be good, let Y ⊆ X be a closed subspace and assume dim_δ(Y) ≤ k. The k-cycle associated to Y is [Y]_k = ∑ m_{Z, Y} [Z], the sum over the irreducible components Z of Y of δ-dimension k, with m_{Z, Y} the multiplicity of Z in Y; as an element of Z_k(X) it is the coefficient family AlgebraicGeometry.Space.cycleCoeffOfClosedSubspace at the canonical geometric points.

def closedSubspaceCycle (sX : X ⟶ D.space) (hX : D.IsGood sX) (Y : Subfunctor X)
    (hY : IsClosedSubspace D.site D.base D.base_mem Y) (k : ℤ)
    (hdim : deltaDimensionSubspace D sX hX Y hY ≤ (k : EInt)) : CycleGroup D sX k

AlgebraicGeometry.Space.closedSubspaceMultiplicity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ClosedSubspaceCycleComponents.lean, line 151. The attribute's comment: “part (1): the multiplicity m_{Z,Y}, together with its positivity (closedSubspaceMultiplicity_pos, Lemma 0EE4)”.

Stacks 0EE9, part (1). The multiplicity m_{W, Y} of an integral closed subspace W ⊆ Y in a closed subspace Y ⊆ X: the length of 𝒪_Y at the generic point of W, read inside Y, at a geometric representative of that generic point.

This is the coefficient the sum of part (2) attaches to W, as AlgebraicGeometry.Space.closedSubspaceCycle_apply_eq_finsum records. The representative used is AlgebraicGeometry.Space.canonicalGeometricPoint, but by Stacks 0EE1 (AlgebraicGeometry.Space.closedSubspaceMultiplicity_eq_toNat_geometricLength) the value does not depend on this choice.

def closedSubspaceMultiplicity (Y : Subfunctor X)
    (hY : IsClosedSubspace D.site D.base D.base_mem Y)
    (W : IntegralClosedSubspace D.site D.base D.base_mem Y.toFunctor) : ℤ
Sources

Section82.6 Cycle associated to a coherent sheaf#

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

Tag 0EEB, a definition

Tag 0EEB in the Stacks Project.

AlgebraicGeometry.Space.moduleMultiplicity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/CoherentSheafCycle.lean, line 221. The attribute's comment: “part (1): the multiplicity of an integral closed subspace in a module, at a chosen geometric representative of its generic point and valued in ℕ∞; the reading at a point of |X| additionally needs the equivalence of Lemma 0EE1, and the finiteness asserted by Lemma 0EE4, neither of which is proved in this library”.

Stacks 0EEB, part (1). The multiplicity of an integral closed subspace Z ⊆ X in an 𝒪_X-module F: the length of F at the generic point ξ of Z, in the sense of Stacks 0EE2, read at the geometric point that γ assigns to ξ.

The source defines this when |Z| is an irreducible component of Supp(F), where by Stacks 0EE4 it is a positive integer; the length itself is defined at every integral closed subspace, and the positivity on a component is AlgebraicGeometry.Space.moduleMultiplicity_pos_of_isIrreducibleComponent_moduleSupport.

def moduleMultiplicity (hX : IsAlgebraicSpace B S hS X) (F : Modules.{u, u} B S hS X hX)
    (γ : points B S hS X → GeometricPoint B S hS X)
    (Z : IntegralClosedSubspace B S hS X) : ℕ∞

AlgebraicGeometry.Space.associatedCycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/CoherentSheafCycle.lean, line 677. The attribute's comment: “part (2): the k-cycle [F]_k of a coherent module, for a chosen geometric representative of each point; the reading at a point of |X| additionally needs the equivalence of Lemma 0EE1, which is not proved in this library”.

Stacks 0EEB, part (2). In Situation 0EDT let X/B be good, let F be a coherent 𝒪_X-module and assume dim_δ(Supp(F)) ≤ k. The k-cycle associated to F is

[F]_k = ∑ m_{Z, F} [Z],

the sum over the integral closed subspaces Z ⊆ X whose set of points is an irreducible component of Supp(F) of δ-dimension k, with m_{Z, F} the multiplicity of part (1).

As an element of Z_k(X) this is the coefficient family AlgebraicGeometry.Space.cycleCoeffOfModule, which assigns m_{Z, F} to each Z of δ-dimension k: off the support the multiplicity already vanishes, and AlgebraicGeometry.Space.exists_irreducibleComponents_of_cycleCoeffOfModule_ne_zero shows that the subspaces left with a nonzero coefficient are exactly the components of Supp(F) of δ-dimension k, so the family is the displayed sum. That it is a k-cycle at all is Stacks 0EE5, by AlgebraicGeometry.Space.cycleCoeffOfModule_mem_cyclesOfDimension.

def associatedCycle (sX : X ⟶ D.space) (hX : D.IsGood sX)
    (F : Modules.{u, u} D.site D.base D.base_mem X hX.1)
    [IsCoherent D.site D.base D.base_mem X hX.1 F] (k : ℤ)
    (γ : points D.site D.base D.base_mem X → GeometricPoint D.site D.base D.base_mem X)
    (hγ : ∀ x, (γ x).LiesOver x)
    (hdim : deltaDimensionClosed D sX hX (moduleSupport D.site D.base D.base_mem hX.1 F)
      (isClosed_moduleSupport D.site D.base D.base_mem hX.1 F) ≤ (k : EInt)) :
    CycleGroup D sX k
Tag 0EEC, a lemma

Tag 0EEC in the Stacks Project.

AlgebraicGeometry.Space.associatedCycle_apply_eq_geometricLength, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/CoherentSheafCycle.lean, line 733. The attribute's comment: “the coefficient at a chosen geometric representative of the generic point, valued in ℤ through ENat.toNat as cycle coefficients are; the reading at a point of |X| additionally needs the equivalence of Lemma 0EE1, which is not proved in this library”.

Stacks 0EEC. In Situation 0EDT let X/B be good, let F be a coherent 𝒪_X-module with dim_δ(Supp(F)) ≤ k, and let Z be an integral closed subspace of X with dim_δ(Z) = k and generic point ξ. Then the coefficient of Z in [F]_k is the length of F at ξ.

The generic point is AlgebraicGeometry.Space.IntegralClosedSubspace.ambientGenericPoint, which is a generic point of |Z| by AlgebraicGeometry.Space.IntegralClosedSubspace.isGenericPoint_ambientGenericPoint; the length is read at the geometric point γ assigns to it, and is the multiplicity of part (1) of Stacks 0EEB. No hypothesis asks |Z| to be an irreducible component of Supp(F): the source reaches that case from the dichotomy that |Z| is such a component exactly when ξ lies in Supp(F), off which the length vanishes, and both halves of it are already recorded here, as AlgebraicGeometry.Space.exists_irreducibleComponents_of_cycleCoeffOfModule_ne_zero and AlgebraicGeometry.Space.moduleMultiplicity_eq_zero_of_notMem_moduleSupport.

theorem associatedCycle_apply_eq_geometricLength (sX : X ⟶ D.space) (hX : D.IsGood sX)
    (F : Modules.{u, u} D.site D.base D.base_mem X hX.1)
    [IsCoherent D.site D.base D.base_mem X hX.1 F] (k : ℤ)
    (γ : points D.site D.base D.base_mem X → GeometricPoint D.site D.base D.base_mem X)
    (hγ : ∀ x, (γ x).LiesOver x)
    (hdim : deltaDimensionClosed D sX hX (moduleSupport D.site D.base D.base_mem hX.1 F)
      (isClosed_moduleSupport D.site D.base D.base_mem hX.1 F) ≤ (k : EInt))
    {Z : IntegralClosedSubspace D.site D.base D.base_mem X}
    (hZ : deltaDimension D sX Z = k) :
    (associatedCycle D sX hX F k γ hγ hdim).1 Z =
      ((geometricLength D.site D.base D.base_mem ⟨X, hX.1⟩
        (γ (Z.ambientGenericPoint D.site D.base D.base_mem)) F).toNat : ℤ)
Tag 0EED, a lemma

Tag 0EED in the Stacks Project.

AlgebraicGeometry.Space.cycleCoeffOfClosedSubspace_eq_cycleCoeffOfModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/StructureSheafCycle.lean, line 422. The attribute's comment: “the coefficient at an integral closed subspace contained in Y, for a choice of geometric representatives above the points they are assigned to, using Lemma 0EE1 to compare the two”.

Stacks 0EED, at an integral closed subspace contained in Y. In Situation 0EDT let X/B be good, let Y ⊂ X be a closed subspace with inclusion i : Y → X, assume dim_δ(Y) ≤ k, and let W be an integral closed subspace of Y with image Z ⊂ X. Then the coefficient of Z in [Y]_k is the coefficient of Z in [i_*𝒪_Y]_k.

The chosen geometric representatives γY and γX are each assumed to lie over the point they are assigned to, which AlgebraicGeometry.Space.exists_compatible_geometricRepresentative shows is possible; the content is then Stacks 0EE3, by way of AlgebraicGeometry.Space.geometricLength_closedSubspacePushforwardStructureSheaf, together with Stacks 0EE1 to move from γX at the image of the generic point of W to the geometric point i(γY(ξ_W)) that the comparison with 𝒪_Y is stated at.

theorem cycleCoeffOfClosedSubspace_eq_cycleCoeffOfModule (sX : X ⟶ D.space) (hX : D.IsGood sX)
    (Y : Subfunctor X) (hY : IsClosedSubspace D.site D.base D.base_mem Y) (k : ℤ)
    (_hdim : deltaDimensionSubspace D sX hX Y hY ≤ (k : EInt))
    (γY : points D.site D.base D.base_mem Y.toFunctor →
      GeometricPoint D.site D.base D.base_mem Y.toFunctor)
    (γX : points D.site D.base D.base_mem X → GeometricPoint D.site D.base D.base_mem X)
    (hγY : ∀ y, (γY y).LiesOver y) (hγX : ∀ x, (γX x).LiesOver x)
    (W : IntegralClosedSubspace D.site D.base D.base_mem Y.toFunctor) :
    cycleCoeffOfClosedSubspace D sX hX Y hY k γY
        (closedSubspaceComponentImage D sX hX Y hY W) =
      cycleCoeffOfModule D sX hX
        (closedSubspacePushforwardStructureSheaf D.site D.base D.base_mem hX.1 Y hY) k γX
        (closedSubspaceComponentImage D sX hX Y hY W)

AlgebraicGeometry.Space.cycleCoeffOfClosedSubspace_eq_cycleCoeffOfModule_of_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/StructureSheafCycle.lean, line 470. The attribute's comment: “the equality of the two k-cycles, for a choice of geometric representatives above the points they are assigned to”.

Stacks 0EED. In Situation 0EDT let X/B be good, let Y ⊂ X be a closed subspace with inclusion i : Y → X, and assume dim_δ(Y) ≤ k. Then [Y]_k = [i_*𝒪_Y]_k, as an equality of coefficient families on the integral closed subspaces of X.

For an integral closed subspace Z with image contained in |Y| this is AlgebraicGeometry.Space.cycleCoeffOfClosedSubspace_eq_cycleCoeffOfModule. Otherwise both sides vanish: the left by AlgebraicGeometry.Space.cycleCoeffOfClosedSubspace_eq_zero, and the right because i_*𝒪_Y is annihilated by the ideal cutting out Y (AlgebraicGeometry.Space.annihilatedByKerIdeal_closedSubspacePushforwardStructureSheaf), so its geometric stalk is trivial at any geometric point over a point of |X| outside the image of |Y| (AlgebraicGeometry.Space.subsingleton_geometricModuleStalk_of_annihilatedByKerIdeal_of_notMem); and the generic point of Z is such a point exactly when no integral closed subspace of Y has image Z, since Y is a decent space (AlgebraicGeometry.Space.isDecentSpace_of_relativelyRepresentable) and every integral closed subspace of X contained in the image of |Y| is itself such an image (AlgebraicGeometry.Space.IntegralClosedSubspace.exists_pushforward_eq). This is the support bound of Lemma 07U0, proved rather than taken as a hypothesis.

theorem cycleCoeffOfClosedSubspace_eq_cycleCoeffOfModule_of_eq_zero (sX : X ⟶ D.space)
    (hX : D.IsGood sX) (Y : Subfunctor X)
    (hY : IsClosedSubspace D.site D.base D.base_mem Y) (k : ℤ)
    (hdim : deltaDimensionSubspace D sX hX Y hY ≤ (k : EInt))
    (γY : points D.site D.base D.base_mem Y.toFunctor →
      GeometricPoint D.site D.base D.base_mem Y.toFunctor)
    (γX : points D.site D.base D.base_mem X → GeometricPoint D.site D.base D.base_mem X)
    (hγY : ∀ y, (γY y).LiesOver y) (hγX : ∀ x, (γX x).LiesOver x) :
    cycleCoeffOfClosedSubspace D sX hX Y hY k γY =
      cycleCoeffOfModule D sX hX
        (closedSubspacePushforwardStructureSheaf D.site D.base D.base_mem hX.1 Y hY) k γX
Tag 0EEE, a lemma

Tag 0EEE in the Stacks Project.

AlgebraicGeometry.Space.associatedCycle_add_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/CoherentSheafCycle.lean, line 807.

Stacks 0EEE. In Situation 0EDT let X/B be good and let 0 → F → G → H → 0 be a short exact sequence of coherent 𝒪_X-modules whose three supports have δ-dimension at most k. Then

[G]_k = [F]_k + [H]_k.

Coefficientwise this is additivity of the multiplicity, AlgebraicGeometry.Space.moduleMultiplicity_add_of_shortExact, hence additivity of length in a short exact sequence, Stacks 00IV, at the generic point of each integral closed subspace of δ-dimension k; at the subspaces of other δ-dimension all three coefficients vanish.

Cycle coefficients are integers, reached from the ℕ∞-valued multiplicity by ENat.toNat, which is additive only on finite values, so the proof also needs the multiplicities of the middle term to be finite at the subspaces of δ-dimension k. Off its support the multiplicity is zero. On its support, the generic point of such a subspace attains the δ-dimension bound, so it is a generic point of an irreducible component of the support by Stacks 0EE6 (AlgebraicGeometry.Space.isGenericPoint_of_deltaDimensionClosed_le), and the length there is finite by Stacks 0EE4 (AlgebraicGeometry.Space.geometricLength_ne_top_and_pos_of_isGenericPoint_supportOfSheaf).

The cycles are read at the geometric points γ chooses above the points of |X|; by Stacks 0EE1, AlgebraicGeometry.Space.geometricLength_eq_of_image_eq, the lengths, hence the cycles, do not depend on that choice.

theorem associatedCycle_add_of_shortExact (sX : X ⟶ D.space) (hX : D.IsGood sX)
    (σ : ShortComplex (Modules.{u, u} D.site D.base D.base_mem X hX.1)) (hσ : σ.ShortExact)
    [IsCoherent D.site D.base D.base_mem X hX.1 σ.X₁]
    [IsCoherent D.site D.base D.base_mem X hX.1 σ.X₂]
    [IsCoherent D.site D.base D.base_mem X hX.1 σ.X₃] (k : ℤ)
    (γ : points D.site D.base D.base_mem X → GeometricPoint D.site D.base D.base_mem X)
    (hγ : ∀ x, (γ x).LiesOver x)
    (hdim₁ : deltaDimensionClosed D sX hX
      (moduleSupport D.site D.base D.base_mem hX.1 σ.X₁)
      (isClosed_moduleSupport D.site D.base D.base_mem hX.1 σ.X₁) ≤ (k : EInt))
    (hdim₂ : deltaDimensionClosed D sX hX
      (moduleSupport D.site D.base D.base_mem hX.1 σ.X₂)
      (isClosed_moduleSupport D.site D.base D.base_mem hX.1 σ.X₂) ≤ (k : EInt))
    (hdim₃ : deltaDimensionClosed D sX hX
      (moduleSupport D.site D.base D.base_mem hX.1 σ.X₃)
      (isClosed_moduleSupport D.site D.base D.base_mem hX.1 σ.X₃) ≤ (k : EInt)) :
    associatedCycle D sX hX σ.X₂ k γ hγ hdim₂ =
      associatedCycle D sX hX σ.X₁ k γ hγ hdim₁ +
        associatedCycle D sX hX σ.X₃ k γ hγ hdim₃
Sources

Section82.7 Preparation for proper pushforward#

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

Tag 0EEG, a lemma

Tag 0EEG in the Stacks Project.

AlgebraicGeometry.Space.IntegralClosedSubspace.existsUnique_isDominant_hom_of_isGood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/IntegralClosedImage.lean, line 259.

Stacks 0EEG. In Situation 0EDT, let X and Y be good algebraic spaces over the base and let f : X ⟶ Y be a morphism over the base. For an integral closed subspace Z ⊂ X there is exactly one integral closed subspace Z' ⊂ Y admitting a morphism Z ⟶ Z' over f — that is, one making the square with Z ⟶ X, Z' ⟶ Y and f commute — which is dominant; and if f is proper, then every such morphism is proper and surjective. Every morphism making that square commute is a morphism over the base, so the whole diagram is one over the base.

The subspace is AlgebraicGeometry.Space.IntegralClosedSubspace.closureImage at f, the integral closed subspace of Y on the closure of the image of |Z|.

theorem IntegralClosedSubspace.existsUnique_isDominant_hom_of_isGood (pX : X ⟶ D.space)
    (pY : Y ⟶ D.space) (hX : D.IsGood pX) (hY : D.IsGood pY) (f : X ⟶ Y) (hf : f ≫ pY = pX)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem X) :
    (∃! Z' : IntegralClosedSubspace D.site D.base D.base_mem Y,
        ∃ g : Z.subspace.toFunctor ⟶ Z'.subspace.toFunctor,
          g ≫ Z'.subspace.ι = Z.subspace.ι ≫ f ∧
            IsDominant D.site D.base D.base_mem g) ∧
      (∀ (Z' : IntegralClosedSubspace D.site D.base D.base_mem Y)
          (g : Z.subspace.toFunctor ⟶ Z'.subspace.toFunctor),
          g ≫ Z'.subspace.ι = Z.subspace.ι ≫ f →
            g ≫ Z'.subspace.ι ≫ pY = Z.subspace.ι ≫ pX) ∧
      (IsProper D.site D.base D.base_mem f →
        ∀ (Z' : IntegralClosedSubspace D.site D.base D.base_mem Y)
          (g : Z.subspace.toFunctor ⟶ Z'.subspace.toFunctor),
          g ≫ Z'.subspace.ι = Z.subspace.ι ≫ f → IsDominant D.site D.base D.base_mem g →
            IsProper D.site D.base D.base_mem g ∧
              IsSurjective D.site D.base D.base_mem g)
Tag 0ENW, a remark

Tag 0ENW in the Stacks Project.

AlgebraicGeometry.Space.BaseSpaceDimensionSituation.residueField, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ResidueFieldAtPoint.lean, line 159.

The residue field κ(x) of a good algebraic space over the base of a BaseSpaceDimensionSituation at a point x of |X|: the field of the monomorphism from a field spectrum representing x.

noncomputable abbrev BaseSpaceDimensionSituation.residueField (f : X ⟶ D.space)
    (hf : D.IsGood f) (x : points D.site D.base D.base_mem X) : Type u

AlgebraicGeometry.Space.BaseSpaceDimensionSituation.residueFieldMorphism_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ResidueFieldAtPoint.lean, line 176. The attribute's comment: “a point is represented by a monomorphism from the spectrum of its residue field”.

A point x of a good algebraic space over the base of a BaseSpaceDimensionSituation is represented by the morphism Spec κ(x) ⟶ X out of the spectrum of its residue field, and that morphism is a monomorphism.

theorem BaseSpaceDimensionSituation.residueFieldMorphism_spec (f : X ⟶ D.space)
    (hf : D.IsGood f) (x : points D.site D.base D.base_mem X) :
    (D.residueFieldRepresentative f hf x).1.class D.site D.base D.base_mem X = x ∧
      Mono (D.residueFieldMorphism f hf x)

AlgebraicGeometry.Space.BaseSpaceDimensionSituation.residueFieldRepresentative_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ResidueFieldAtPoint.lean, line 187. The attribute's comment: “the monomorphism from a field spectrum representing a point is unique up to unique isomorphism over the space”.

The monomorphism from a field spectrum representing a point x of a good algebraic space over the base of a BaseSpaceDimensionSituation is unique: any monomorphic field-valued representative of x is uniquely isomorphic, over the space, to Spec κ(x) ⟶ X.

theorem BaseSpaceDimensionSituation.residueFieldRepresentative_unique (f : X ⟶ D.space)
    (hf : D.IsGood f) (x : points D.site D.base D.base_mem X)
    (q : FieldValuedPoint D.site D.base D.base_mem X)
    (hq : q.class D.site D.base D.base_mem X = x)
    (hmq : Mono (fieldMorphism D.site D.base D.base_mem X q)) :
    ∃! e : yoneda.obj ((D.residueFieldRepresentative f hf x).1.siteObject
        D.site D.base D.base_mem X) ≅
        yoneda.obj (q.siteObject D.site D.base D.base_mem X),
      e.hom ≫ fieldMorphism D.site D.base D.base_mem X q = D.residueFieldMorphism f hf x

AlgebraicGeometry.Space.BaseSpaceDimensionSituation.exists_denseRange_isRepresentable_isOpenSubspace_of_isGood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ResidueFieldAtPoint.lean, line 202. The attribute's comment: “a good algebraic space has a dense open subspace which is a scheme”.

A good algebraic space over the base of a BaseSpaceDimensionSituation has a dense open subspace which is a scheme.

theorem BaseSpaceDimensionSituation.exists_denseRange_isRepresentable_isOpenSubspace_of_isGood
    (f : X ⟶ D.space) (hf : D.IsGood f) :
    ∃ G : Subfunctor X, IsOpenSubspace D.site D.base D.base_mem G ∧
      G.toFunctor.IsRepresentable ∧
      DenseRange (pointsMap D.site D.base D.base_mem G.toFunctor G.ι)

AlgebraicGeometry.Space.BaseSpaceDimensionSituation.exists_ringEquiv_residueField_schemeResidueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ResidueFieldAtPoint.lean, line 217. The attribute's comment: “at a point of an open subspace which is a scheme the residue field agrees with the residue field of the corresponding point on that scheme”.

Let X/B be good over the base of a BaseSpaceDimensionSituation and let U ⊆ X be an open subspace which is a scheme, presented by an open immersion out of the presheaf represented by an object of the site. At a point x of |X| coming from a point u of that scheme, the residue field κ(x) agrees with the residue field of u on U as a scheme: they are isomorphic by an isomorphism whose spectrum is the comparison morphism over X.

theorem BaseSpaceDimensionSituation.exists_ringEquiv_residueField_schemeResidueField
    (f : X ⟶ D.space) (hf : D.IsGood f) (T : BigFppfOver D.site D.base D.base_mem)
    (j : yoneda.obj T ⟶ X) (hj : IsOpenImmersion D.site D.base D.base_mem j)
    (u : (BigFppfOver.toScheme D.site D.base D.base_mem).obj T)
    (x : points D.site D.base D.base_mem X)
    (hu : pointsMap D.site D.base D.base_mem (yoneda.obj T) j
      ((schemePointRepresentative D.site D.base D.base_mem T u).class
        D.site D.base D.base_mem (yoneda.obj T)) = x) :
    ∃ (φ : D.residueField f hf x ≃+*
        ((BigFppfOver.toScheme D.site D.base D.base_mem).obj T).residueField u)
      (g : (schemePointRepresentative D.site D.base D.base_mem T u).siteObject
          D.site D.base D.base_mem (yoneda.obj T) ⟶
        (D.residueFieldRepresentative f hf x).1.siteObject D.site D.base D.base_mem X),
      D.site.inclusion.map g.left = Spec.map (CommRingCat.ofHom φ.toRingHom) ∧
        yoneda.map g ≫ D.residueFieldMorphism f hf x =
          yoneda.map (schemePointRepresentative D.site D.base D.base_mem T u).siteHom ≫ j
Tag 0ENX, a remark

Tag 0ENX in the Stacks Project.

AlgebraicGeometry.Space.BaseSpaceDimensionSituation.isField_functionField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FunctionFieldAtPoint.lean, line 205. The attribute's comment: “the function field R(X) of a good integral algebraic space is defined: its ring of rational functions is a field”.

In the situation of Stacks 0EDT let X/B be good and let X be integral. Then the function field R(X) of X is defined: the ring of rational functions of X is a field.

theorem BaseSpaceDimensionSituation.isField_functionField (f : X ⟶ D.space)
    (hf : D.IsGood f) (hInt : IsIntegralSpace D.site D.base D.base_mem X) :
    IsField (rationalFunctions D.site D.base D.base_mem hf.1)

AlgebraicGeometry.Space.BaseSpaceDimensionSituation.functionFieldRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FunctionFieldAtPoint.lean, line 214. The attribute's comment: “the function field R(X) of a good integral algebraic space is the residue field at its generic point”.

In the situation of Stacks 0EDT let X/B be good and let X be integral. Then the function field R(X) of X is the residue field of X at its generic point.

noncomputable def BaseSpaceDimensionSituation.functionFieldRingEquiv (f : X ⟶ D.space)
    (hf : D.IsGood f) (hInt : IsIntegralSpace D.site D.base D.base_mem X) :
    rationalFunctions D.site D.base D.base_mem hf.1 ≃+*
      residueField D.site D.base D.base_mem X hInt.2.1
        (genericPoint D.site D.base D.base_mem hf.1 hInt)

AlgebraicGeometry.Space.BaseSpaceDimensionSituation.residueFieldRingEquivFunctionField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FunctionFieldAtPoint.lean, line 226. The attribute's comment: “for any point x of a good algebraic space, the residue field κ(x) is the function field of the unique integral closed subspace whose generic point is x”.

In the situation of Stacks 0EDT let X/B be good. For a point ξ of X the residue field κ(ξ) is the function field of the unique integral closed subspace Z ⊆ X whose generic point is ξ.

noncomputable def BaseSpaceDimensionSituation.residueFieldRingEquivFunctionField
    (f : X ⟶ D.space) (hf : D.IsGood f) (ξ : points D.site D.base D.base_mem X) :
    residueField D.site D.base D.base_mem X (D.isDecentSpace_of_isGood f hf) ξ ≃+*
      rationalFunctions D.site D.base D.base_mem
        (integralClosedSubspaceOfPoint D.site D.base D.base_mem hf.1
          (D.isDecentSpace_of_isGood f hf) ξ).isClosedSubspace.1
Tag 0ENY, a lemma

Tag 0ENY in the Stacks Project.

AlgebraicGeometry.Space.factorsThrough_properIntegralClosedSubspace_or_isDominant_and_finite_functionField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/EqualDeltaDimension.lean, line 627.

Stacks 0ENY. In Situation 0EDT let X and Y be good integral algebraic spaces over the fixed base with dim_δ(X) = dim_δ(Y), and let f : X ⟶ Y be a morphism over the base. Then either f factors through a proper closed subspace of Y — namely the integral closed subspace of Y on the closure of the image of |X|, whose set of points is strictly smaller than |Y| — or f is dominant, carries the generic point of X to the generic point of Y, and the extension of function fields R(X)/R(Y) it induces is finite.

The function fields are the residue fields at the generic points, by Stacks 0END, and the extension is the homomorphism f induces on them; finiteness is finiteness as a module.

If the image of |X| is not dense its closure is an irreducible closed proper subset of |Y|, and X is reduced, so f factors through the integral closed subspace on it by Stacks 03IQ and Stacks 03JJ. If the image is dense, then f is dominant and carries the generic point to the generic point; equality of the δ-dimensions makes the relative transcendence degree at the generic point vanish, and then Spaces over Fields, Lemma 0AD5 gives finiteness.

theorem factorsThrough_properIntegralClosedSubspace_or_isDominant_and_finite_functionField
    (pX : X ⟶ D.space) (pY : Y ⟶ D.space) (hX : D.IsGood pX) (hY : D.IsGood pY)
    (hXInt : IsIntegralSpace D.site D.base D.base_mem X)
    (hYInt : IsIntegralSpace D.site D.base D.base_mem Y) (f : X ⟶ Y) (hf : f ≫ pY = pX)
    (hdim : deltaDimensionClosed D pX hX Set.univ isClosed_univ =
      deltaDimensionClosed D pY hY Set.univ isClosed_univ) :
    (∃ Z : IntegralClosedSubspace D.site D.base D.base_mem Y,
        subspacePointSet D.site D.base D.base_mem Y Z.subspace ≠ Set.univ ∧
          ∃ g : X ⟶ Z.subspace.toFunctor, g ≫ Z.subspace.ι = f) ∨
      (IsDominant D.site D.base D.base_mem f ∧
        pointsMap D.site D.base D.base_mem X f
            (genericPoint D.site D.base D.base_mem hX.1 hXInt) =
          genericPoint D.site D.base D.base_mem hY.1 hYInt ∧
        letI := (residueFieldHom D.site D.base D.base_mem X Y hY.1 hXInt.2.1 hYInt.2.1 f
          (genericPoint D.site D.base D.base_mem hX.1 hXInt)).toAlgebra
        Module.Finite
          (residueField D.site D.base D.base_mem Y hYInt.2.1
            (pointsMap D.site D.base D.base_mem X f
              (genericPoint D.site D.base D.base_mem hX.1 hXInt)))
          (residueField D.site D.base D.base_mem X hXInt.2.1
            (genericPoint D.site D.base D.base_mem hX.1 hXInt)))
Tag 0ENZ, a lemma

Tag 0ENZ in the Stacks Project.

AlgebraicGeometry.Space.locallyFinite_closure_image_pointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforward.lean, line 66.

Stacks 0ENZ. Let X/B and Y/B be good algebraic spaces over the base of the theory of cycles and let f : X ⟶ Y be a quasi-compact morphism over B. The closures of the images under |f| of a locally finite collection of closed subsets of |X| form a locally finite collection of closed subsets of |Y|.

theorem locallyFinite_closure_image_pointsMap
    {X Y : (BigFppfOver D.site D.base D.base_mem)ᵒᵖ ⥤ Type u}
    (sX : X ⟶ D.space) (hX : D.IsGood sX) (sY : Y ⟶ D.space) (hY : D.IsGood sY)
    {f : X ⟶ Y} (_hfB : f ≫ sY = sX)
    (hf : IsQuasiCompact D.site D.base D.base_mem f)
    {I : Type v} (T : I → Set (points D.site D.base D.base_mem X))
    (_hT : ∀ i, IsClosed (T i)) (hTlf : LocallyFinite T) :
    LocallyFinite (fun i ↦ closure (pointsMap D.site D.base D.base_mem X f '' T i)) ∧
      ∀ i, IsClosed (closure (pointsMap D.site D.base D.base_mem X f '' T i))
Sources

Section82.8 Proper pushforward#

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

Tag 0EP1, a definition

Tag 0EP1 in the Stacks Project.

AlgebraicGeometry.Space.properCycleDegree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardCycles.lean, line 143. The attribute's comment: “part (1): the coefficient of the image in the pushforward of a prime cycle”.

The coefficient with which the closure Z' of the image of an integral closed subspace Z ⊆ X occurs in f_*[Z]: the degree [R(Z) : R(Z')] when the δ-dimension is preserved, and 0 when it drops.

noncomputable def properCycleDegree (sX : X ⟶ D.space) (hX : D.IsGood sX) (sY : Y ⟶ D.space)
    (hY : D.IsGood sY) (f : X ⟶ Y)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem X) : ℤ

AlgebraicGeometry.Space.properCyclePushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardCycles.lean, line 380. The attribute's comment: “part (2): the pushforward of a k-cycle, as a homomorphism of abelian groups”.

The proper pushforward of cycles along a quasi-compact morphism f : X ⟶ Y of good algebraic spaces over B: the additive map f_* : Z_k(X) → Z_k(Y) sending a cycle α to the cycle whose coefficient at Z' is ∑ α_Z · [R(Z) : R(Z')], the sum being over the integral closed subspaces Z ⊆ X whose image closure is Z' and the degree being taken to be 0 where the δ-dimension drops. The morphism f is assumed quasi-compact, not proper.

noncomputable def properCyclePushforward (sX : X ⟶ D.space) (hX : D.IsGood sX) (sY : Y ⟶ D.space)
    (hY : D.IsGood sY) {f : X ⟶ Y} (hfB : f ≫ sY = sX)
    (hf : IsQuasiCompact D.site D.base D.base_mem f) (k : ℤ) :
    CycleGroup D sX k →+ CycleGroup D sY k

AlgebraicGeometry.Space.properPushforwardWeightInDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardCyclesInDimension.lean, line 194. The attribute's comment: “part (1): the multiplicity of an integral closed subspace in the pushforward”.

Stacks 0EP1, part (1). The multiplicity with which proper pushforward along f records an integral closed subspace Z of X in the cycle group of δ-dimension k: the degree deg(Z/Z') of Z over its integral closed image Z' when dim_δ(Z') = k, and 0 when dim_δ(Z') < k, which for Z of δ-dimension k is the only other case.

noncomputable def properPushforwardWeightInDimension (sX : X ⟶ D.space) (sY : Y ⟶ D.space)
    (hX : D.IsGood sX) (hY : D.IsGood sY) (f : X ⟶ Y) (k : ℤ)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem X) : ℤ

AlgebraicGeometry.Space.properPushforwardInDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardCyclesInDimension.lean, line 347. The attribute's comment: “part (2): the pushforward of a k-cycle, as a map Z_k(X) → Z_k(Y)”.

Proper pushforward of cycles of δ-dimension k along a proper morphism f : X ⟶ Y of good algebraic spaces over the base: the cycle whose coefficient at Z' is the sum of n_Z deg(Z/Z') over the integral closed subspaces Z of X with integral closed image Z' of δ-dimension k.

noncomputable def properPushforwardInDimension (sX : X ⟶ D.space) (sY : Y ⟶ D.space)
    (hX : D.IsGood sX) (hY : D.IsGood sY) (f : X ⟶ Y) (hfB : f ≫ sY = sX)
    (hf : IsProper D.site D.base D.base_mem f) (k : ℤ) :
    CycleGroup D sX k → CycleGroup D sY k

AlgebraicGeometry.Space.properPushforwardInDimension_cycleOfIntegralClosedSubspace_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardCyclesInDimension.lean, line 404. The attribute's comment: “part (1): f_*[Z] = 0 when dim_δ(Z') < k”.

The pushforward of the cycle [Z] of an integral closed subspace of δ-dimension k is zero when its integral closed image has smaller δ-dimension.

theorem properPushforwardInDimension_cycleOfIntegralClosedSubspace_eq_zero (sX : X ⟶ D.space)
    (sY : Y ⟶ D.space) (hX : D.IsGood sX) (hY : D.IsGood sY) (f : X ⟶ Y) (hfB : f ≫ sY = sX)
    (hf : IsProper D.site D.base D.base_mem f) (k : ℤ)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem X) (hZ : deltaDimension D sX Z = k)
    (hlt : deltaDimension D sY (cycleImageSubspace D sY hY f Z) < k) :
    properPushforwardInDimension D sX sY hX hY f hfB hf k
        (cycleOfIntegralClosedSubspace D sX k Z hZ) = 0

AlgebraicGeometry.Space.properPushforwardInDimension_cycleOfIntegralClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardCyclesInDimension.lean, line 421. The attribute's comment: “part (1): f_*[Z] = deg(Z/Z')·[Z'] when dim_δ(Z') = k”.

The pushforward of the cycle [Z] of an integral closed subspace of δ-dimension k whose integral closed image Z' again has δ-dimension k is deg(Z/Z')·[Z'].

theorem properPushforwardInDimension_cycleOfIntegralClosedSubspace (sX : X ⟶ D.space)
    (sY : Y ⟶ D.space) (hX : D.IsGood sX) (hY : D.IsGood sY) (f : X ⟶ Y) (hfB : f ≫ sY = sX)
    (hf : IsProper D.site D.base D.base_mem f) (k : ℤ)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem X) (hZ : deltaDimension D sX Z = k)
    (hdim : deltaDimension D sY (cycleImageSubspace D sY hY f Z) = k) :
    properPushforwardInDimension D sX sY hX hY f hfB hf k
        (cycleOfIntegralClosedSubspace D sX k Z hZ) =
      (IntegralClosedSubspace.degreeOverImage D sX sY hX hY f Z : ℤ) •
        cycleOfIntegralClosedSubspace D sY k
          (cycleImageSubspace D sY hY f Z) hdim

AlgebraicGeometry.Space.properPushforward_integralCycle_integralClosedSubspaceUniv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardOfDivisor.lean, line 366. The attribute's comment: “f_*[X] = [R(X):R(Y)] [Y]: the pushforward of the fundamental cycle of an integral good X along a dominant quasi-compact morphism to an integral good Y of the same δ-dimension”.

Stacks 0EP1 at the fundamental cycle. For a dominant quasi-compact morphism f : X ⟶ Y over B of integral good algebraic spaces with dim_δ(X) = dim_δ(Y) = n,

f_*[X] = [R(X) : R(Y)] [Y] in Z_n(Y).

The whole of X is the only integral closed subspace carrying a coefficient of [X], its image closure is the whole of Y, and the degree there is [R(X) : R(Y)] because the δ-dimension does not drop. This is the identity the source uses to read its second conclusion.

theorem properPushforward_integralCycle_integralClosedSubspaceUniv
    (hYInt : IsIntegralSpace D.site D.base D.base_mem Y) {f : X ⟶ Y}
    (hfB : f ≫ sY = sX) (hf : IsQuasiCompact D.site D.base D.base_mem f)
    (hdom : IsDominant D.site D.base D.base_mem f) {n : ℤ}
    (hnX : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt))
    (hnY : deltaDimensionClosed D sY hY Set.univ isClosed_univ = (n : EInt)) :
    properCyclePushforward D sX hX sY hY hfB hf n (integralCycle D sX n
          (integralClosedSubspaceUniv D sX hX hXInt)
          (deltaDimension_integralClosedSubspaceUniv D sX hX hXInt hnX)) =
      (functionFieldDegreeAtGenericPoint D sX hX sY hY hXInt f : ℤ) •
        integralCycle D sY n (integralClosedSubspaceUniv D sY hY hYInt)
          (deltaDimension_integralClosedSubspaceUniv D sY hY hYInt hnY)
Tag 0EP2, a lemma

Tag 0EP2 in the Stacks Project.

AlgebraicGeometry.Space.properPushforwardInDimension_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardCyclesInDimension.lean, line 564.

Proper pushforward of k-cycles is functorial: pushing forward along f : X ⟶ Y and then along g : Y ⟶ W is pushing forward along the composite.

theorem properPushforwardInDimension_comp (sX : X ⟶ D.space) (sY : Y ⟶ D.space) (sW : W ⟶ D.space)
    (hX : D.IsGood sX) (hY : D.IsGood sY) (hW : D.IsGood sW) (f : X ⟶ Y) (g : Y ⟶ W)
    (hfB : f ≫ sY = sX) (hgB : g ≫ sW = sY) (hf : IsProper D.site D.base D.base_mem f)
    (hg : IsProper D.site D.base D.base_mem g) (k : ℤ) (α : CycleGroup D sX k) :
    properPushforwardInDimension D sY sW hY hW g hgB hg k
        (properPushforwardInDimension D sX sY hX hY f hfB hf k α) =
      properPushforwardInDimension D sX sW hX hW (f ≫ g) (by rw [Category.assoc, hgB, hfB])
        (isProper_comp D.site D.base D.base_mem hX.1 hY.1 hW.1 f g hf hg) k α
Tag 0EP3, a lemma

Tag 0EP3 in the Stacks Project.

AlgebraicGeometry.Space.properCyclePushforward_associatedCycle_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardModuleCycle.lean, line 147. The attribute's comment: “part (2)”.

Stacks 0EP3, part (2). In Situation 0EDT let f : X ⟶ Y be a proper morphism of good algebraic spaces over the base and let F be a coherent 𝒪_X-module with dim_δ(Supp(F)) ≤ k. Then

f_*[F]_k = [f_*F]_k

in Z_k(Y): the proper pushforward of the k-cycle [F]_k of Stacks 0EEB is the k-cycle whose coefficient at an integral closed subspace W ⊂ Y of δ-dimension k is the length of f_*F at the generic point of W. The cycles of modules are read at chosen geometric representatives γX, γY of the points (by Stacks 0EE1 the lengths do not depend on them). That the coefficient family of f_*F is a k-cycle is part of the statement (AlgebraicGeometry.Space.cycleCoeffOfModule_directImageModule_mem_cyclesOfDimension); the coherence of f_*F (Stacks 08AR) is not needed.

theorem properCyclePushforward_associatedCycle_eq {f : X ⟶ Y} (hfB : f ≫ sY = sX)
    (hproper : IsProper D.site D.base D.base_mem f)
    (F : Modules.{u, u} D.site D.base D.base_mem X hX.1)
    [IsCoherent D.site D.base D.base_mem X hX.1 F] (k : ℤ)
    (hdimF : deltaDimensionClosed D sX hX (moduleSupport D.site D.base D.base_mem hX.1 F)
      (isClosed_moduleSupport D.site D.base D.base_mem hX.1 F) ≤ (k : EInt))
    (γX : points D.site D.base D.base_mem X → GeometricPoint D.site D.base D.base_mem X)
    (hγX : ∀ x, (γX x).LiesOver x)
    (γY : points D.site D.base D.base_mem Y → GeometricPoint D.site D.base D.base_mem Y)
    (hγY : ∀ y, (γY y).LiesOver y) :
    properCyclePushforward D sX hX sY hY hfB hproper.2.1.2 k
        (associatedCycle D sX hX F k γX hγX hdimF) =
      ⟨cycleCoeffOfModule D sY hY (directImageModule D hX.1 hY.1 f F) k γY,
        cycleCoeffOfModule_directImageModule_mem_cyclesOfDimension D sX hX sY hY hfB hproper F k
          hdimF γX hγX γY hγY⟩

AlgebraicGeometry.Space.properCyclePushforward_closedSubspaceCycle_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardModuleCycle.lean, line 288. The attribute's comment: “part (1)”.

In Situation 0EDT let f : X ⟶ Y be a proper morphism of good algebraic spaces over the base and let Z ⊂ X be a closed subspace with dim_δ(Z) ≤ k. Then

f_*[Z]_k = [f_*𝒪_Z]_k

in Z_k(Y), where [Z]_k is the k-cycle of Stacks 0EE9 and f_*𝒪_Z is the direct image of the structure sheaf of Z along Z → X → Y: the proper pushforward of [Z]_k is the k-cycle whose coefficient at an integral closed subspace W ⊂ Y of δ-dimension k is the length of f_*𝒪_Z at the generic point of W (read at the chosen geometric representative γY; by Stacks 0EE1 it does not depend on it). That this coefficient family is a k-cycle is part of the statement (cycleCoeffOfModule_closedSubspaceDirectImageStructureSheaf_mem_cyclesOfDimension).

theorem properCyclePushforward_closedSubspaceCycle_eq {f : X ⟶ Y} (hfB : f ≫ sY = sX)
    (hproper : IsProper D.site D.base D.base_mem f) (Z : Subfunctor X)
    (hZ : IsClosedSubspace D.site D.base D.base_mem Z) (k : ℤ)
    (hdim : deltaDimensionSubspace D sX hX Z hZ ≤ (k : EInt))
    (γY : points D.site D.base D.base_mem Y → GeometricPoint D.site D.base D.base_mem Y)
    (hγY : ∀ y, (γY y).LiesOver y) :
    properCyclePushforward D sX hX sY hY hfB hproper.2.1.2 k
        (closedSubspaceCycle D sX hX Z hZ k hdim) =
      ⟨cycleCoeffOfModule D sY hY (closedSubspaceDirectImageStructureSheaf D sX hX sY hY f Z hZ)
          k γY,
        cycleCoeffOfModule_closedSubspaceDirectImageStructureSheaf_mem_cyclesOfDimension D sX hX
          sY hY hfB hproper Z hZ k hdim γY hγY⟩
Sources

Section82.9 Preparation for flat pullback#

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

Tag 0EP5, a lemma

Tag 0EP5 in the Stacks Project.

AlgebraicGeometry.Space.IntegralClosedSubspace.closure_image_subspacePointSet_preimageComponent_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatInverseImageDeltaDimension.lean, line 281. The attribute's comment: “a component of the inverse image of an integral closed subspace dominates it”.

Let f : X ⟶ Y be a flat morphism of good algebraic spaces over the base and let Z ⊆ Y be an integral closed subspace. An irreducible component Z' of f^{-1}(Z) dominates Z: the closure of the image of |Z'| is |Z|.

theorem IntegralClosedSubspace.closure_image_subspacePointSet_preimageComponent_of_isFlat
    (sX : X ⟶ D.space) (hX : D.IsGood sX) (sY : Y ⟶ D.space) (hY : D.IsGood sY) {f : X ⟶ Y}
    (hflat : IsFlat D.site D.base D.base_mem f)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem Y)
    (C : irreducibleComponents (Z.preimagePointSet D.site D.base D.base_mem f)) :
    closure (pointsMap D.site D.base D.base_mem X f ''
        subspacePointSet D.site D.base D.base_mem X
          (Z.preimageComponent D.site D.base D.base_mem f hX.1
            (D.isDecentSpace_of_isGood sX hX) hY.1 C).subspace) =
      subspacePointSet D.site D.base D.base_mem Y Z.subspace

AlgebraicGeometry.Space.IntegralClosedSubspace.deltaDimension_preimageComponent_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatInverseImageDeltaDimension.lean, line 385. The attribute's comment: “the δ-dimension of a component of the inverse image of an integral closed subspace”.

Let f : X ⟶ Y be a morphism of good algebraic spaces over the base which is flat of relative dimension r, and let Z ⊆ Y be an integral closed subspace. An irreducible component Z' of f^{-1}(Z) satisfies dim_δ(Z') = dim_δ(Z) + r.

theorem IntegralClosedSubspace.deltaDimension_preimageComponent_of_isFlat
    (sX : X ⟶ D.space) (hX : D.IsGood sX) (sY : Y ⟶ D.space) (hY : D.IsGood sY) {f : X ⟶ Y}
    (hbase : f ≫ sY = sX) (r : ℕ) (hflat : IsFlat D.site D.base D.base_mem f)
    (hr : HasRelativeDimension r D.site D.base D.base_mem f)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem Y)
    (C : irreducibleComponents (Z.preimagePointSet D.site D.base D.base_mem f)) :
    deltaDimension D sX (Z.preimageComponent D.site D.base D.base_mem f hX.1
        (D.isDecentSpace_of_isGood sX hX) hY.1 C) = deltaDimension D sY Z + r

AlgebraicGeometry.Space.deltaDimensionClosed_preimage_eq_iSup_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatInverseImageDeltaDimension.lean, line 526. The attribute's comment: “the δ-dimension of the inverse image of a closed set of points”.

Let f : X ⟶ Y be a morphism of good algebraic spaces over the base which is flat of relative dimension r, and let T ⊆ |Y| be a closed set of points whose inverse image is nonempty. Then dim_δ(f^{-1}(T)) is r more than the supremum of the δ-dimensions of the irreducible components of T which f meets.

When f meets every component of T, in particular when f is surjective, the supremum is dim_δ(T) and the formula reads dim_δ(f^{-1}(T)) = dim_δ(T) + r.

theorem deltaDimensionClosed_preimage_eq_iSup_add (sX : X ⟶ D.space) (hX : D.IsGood sX)
    (sY : Y ⟶ D.space) (hY : D.IsGood sY) {f : X ⟶ Y} (hbase : f ≫ sY = sX) (r : ℕ)
    (hflat : IsFlat D.site D.base D.base_mem f)
    (hr : HasRelativeDimension r D.site D.base D.base_mem f)
    (T : Set (points D.site D.base D.base_mem Y)) (hT : IsClosed T)
    (_hne : (pointsMap D.site D.base D.base_mem X f ⁻¹' T).Nonempty) :
    deltaDimensionClosed D sX hX (pointsMap D.site D.base D.base_mem X f ⁻¹' T)
        (isClosed_preimage_pointsMap D.site D.base D.base_mem hX.1 hY.1 f hT) =
      (⨆ C : irreducibleComponents T,
        ⨆ _ : (pointsMap D.site D.base D.base_mem X f ⁻¹'
            (Subtype.val '' (C : Set T))).Nonempty,
          deltaDimensionClosed D sY hY (closure (Subtype.val '' (C : Set T)))
            isClosed_closure) + ((r : ℤ) : EInt)
Tag 0EP6, a lemma

Tag 0EP6 in the Stacks Project.

AlgebraicGeometry.Space.isClosed_preimage_pointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullback.lean, line 55. The attribute's comment: “closedness”.

Stacks 0EP6, closedness. The inverse image of a closed subset of the points of Y under a morphism f : X ⟶ Y of algebraic spaces over S is closed in the points of X.

theorem isClosed_preimage_pointsMap
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (_hX : IsAlgebraicSpace B S hS X)
    (_hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    letI : TopologicalSpace (points B S hS X) := pointTopology B S hS X
    letI : TopologicalSpace (points B S hS Y) := pointTopology B S hS Y
    ∀ {T : Set (points B S hS Y)}, IsClosed T →
      IsClosed ((pointsMap B S hS X f) ⁻¹' T)

AlgebraicGeometry.Space.locallyFinite_preimage_pointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullback.lean, line 72. The attribute's comment: “local finiteness”.

Stacks 0EP6, local finiteness. The inverse images of a locally finite collection of subsets of the points of Y under a morphism f : X ⟶ Y of algebraic spaces over S form a locally finite collection of subsets of the points of X.

theorem locallyFinite_preimage_pointsMap
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (_hX : IsAlgebraicSpace B S hS X)
    (_hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    {I : Type v} (T : I → Set (points B S hS Y)) :
    letI : TopologicalSpace (points B S hS X) := pointTopology B S hS X
    letI : TopologicalSpace (points B S hS Y) := pointTopology B S hS Y
    LocallyFinite T →
      LocallyFinite (fun i ↦ (pointsMap B S hS X f) ⁻¹' T i)
Sources

Section82.10 Flat pullback#

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

Tag 0EP8, a definition

Tag 0EP8 in the Stacks Project.

AlgebraicGeometry.Space.flatPullbackIntegralCycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullbackOfCycles.lean, line 169. The attribute's comment: “part (1): f^*[W] = [f^{-1}(W)]_{k+r} for an integral closed subspace W”.

The flat pullback of the cycle of an integral closed subspace W ⊆ Y of δ-dimension k: the (k+r)-cycle [f^{-1}(W)]_{k+r} of the scheme-theoretic inverse image.

def flatPullbackIntegralCycle (W : IntegralClosedSubspace D.site D.base D.base_mem Y) :
    CycleGroup D sX (deltaDimension D sY W + (r : ℤ))

AlgebraicGeometry.Space.flatPullbackMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullbackOfCycles.lean, line 326. The attribute's comment: “parts (2) and (3): the flat pullback of a cycle and the homomorphism Z_k(Y) → Z_{k+r}(X)”.

The flat pullback of cycles along a morphism f : X ⟶ Y of good algebraic spaces over the base which is flat of relative dimension r, as a homomorphism f^* : Z_m(Y) →+ Z_n(X) for m + r = n.

def flatPullbackMap (m n : ℤ) (hmn : m + (r : ℤ) = n) :
    CycleGroup D sY m →+ CycleGroup D sX n

AlgebraicGeometry.Space.flatCyclePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullbackOfCycles.lean, line 372. The attribute's comment: “the whole definition, bundled with its defining formula”.

The flat pullback of cycles along a morphism f : X ⟶ Y of good algebraic spaces over the base which is flat of relative dimension r, as an inhabitant of the bundled AlgebraicGeometry.Space.FlatCyclePullback: the multiplicities of the inverse images, the homomorphisms Z_m(Y) →+ Z_n(X) for m + r = n, the defining formula relating them, and the containment of the support of f^*[W] in f^{-1}(W).

def flatCyclePullback (sX : X ⟶ D.space) (hX : D.IsGood sX) (sY : Y ⟶ D.space)
    (hY : D.IsGood sY) (f : X ⟶ Y) (hbase : f ≫ sY = sX) (r : ℕ)
    (hflat : IsFlat D.site D.base D.base_mem f)
    (hr : HasRelativeDimension r D.site D.base D.base_mem f) :
    FlatCyclePullback D sX hX sY hY f r
Tag 0EP9, a lemma

Tag 0EP9 in the Stacks Project.

AlgebraicGeometry.Space.cycleGroupRestrict_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/LocalizationSequence.lean, line 475. The attribute's comment: “exactness at the k-cycles of the ambient space”.

Stacks 0EP9, exactness at the k-cycles of the ambient space. In Situation 0EDT let X/B be good, let i : Y ⟶ X be a closed immersion over the base and let j : U ⟶ X be an open immersion over the base whose image is the complement of the image of i. A k-cycle on X restricts to zero on U exactly when it is the pushforward of a k-cycle on Y.

theorem cycleGroupRestrict_eq_zero_iff (sX : X ⟶ D.space) (hX : D.IsGood sX) (sY : Y ⟶ D.space)
    (hY : D.IsGood sY) (sU : U ⟶ D.space) (hU : D.IsGood sU) {i : Y ⟶ X}
    (hi : IsClosedImmersion D.site D.base D.base_mem i) (hic : i ≫ sX = sY) {j : U ⟶ X}
    (hj : IsOpenImmersion D.site D.base D.base_mem j) (hjc : j ≫ sX = sU)
    (hcomplement : Set.range (pointsMap D.site D.base D.base_mem Y i) =
      (Set.range (pointsMap D.site D.base D.base_mem U j))ᶜ) (k : ℤ) (α : CycleGroup D sX k) :
    cycleGroupRestrict D sX hX sU hU hj hjc k α = 0 ↔
      ∃ β : CycleGroup D sY k,
        cycleGroupClosedPushforward D hX.1 hY.1 (D.isDecentSpace_of_isGood sX hX) hi sX hX.2.2
          sY hic k β = α

AlgebraicGeometry.Space.cycleGroupRestrict_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/LocalizationSequence.lean, line 565. The attribute's comment: “surjectivity onto the k-cycles of the open subspace”.

Stacks 0EP9, surjectivity onto the k-cycles of the open subspace. In Situation 0EDT let X/B and U/B be good and let j : U ⟶ X be an open immersion over the base. Every k-cycle on U is the restriction of a k-cycle on X, namely of the coefficient family extending it by zero along the map which takes the closure of the image of an integral closed subspace.

That extension is a k-cycle: it has the right δ-dimension because taking the closure of the image preserves it, and its support family is locally finite because |X| is locally Noetherian, the structure morphism being locally of finite type over a locally Noetherian base.

theorem cycleGroupRestrict_surjective (sX : X ⟶ D.space) (hX : D.IsGood sX) (sU : U ⟶ D.space)
    (hU : D.IsGood sU) {j : U ⟶ X} (hj : IsOpenImmersion D.site D.base D.base_mem j)
    (hjc : j ≫ sX = sU) (k : ℤ) :
    Function.Surjective (cycleGroupRestrict D sX hX sU hU hj hjc k)
Tag 0EPY, a lemma

Tag 0EPY in the Stacks Project.

AlgebraicGeometry.Space.IntegralClosedSubspace.preimageComponentsCycle_mem_cyclesOfDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/EtalePullbackComponents.lean, line 434. The attribute's comment: “the sum of the components of the inverse image is a cycle of the same δ-dimension”.

Stacks 0EPY, the right-hand side of its formula. Let f : X ⟶ Y be an étale morphism of good algebraic spaces over the base of Situation 0EDT and let Z ⊆ Y be an integral closed subspace. The formal sum of the irreducible components of the inverse image of Z, each with coefficient one, is a cycle of the δ-dimension of Z on X.

The components are integral closed subspaces of X, they form a locally finite family, and each of them has the δ-dimension of Z; these are exactly the two conditions defining Z_{δ(Z)}(X).

theorem IntegralClosedSubspace.preimageComponentsCycle_mem_cyclesOfDimension (sX : X ⟶ D.space)
    (hX : D.IsGood sX) (sY : Y ⟶ D.space) (hY : D.IsGood sY) {f : X ⟶ Y}
    (hf : IsEtale D.site D.base D.base_mem f) (hfc : f ≫ sY = sX)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem Y) :
    Z.preimageComponentsCycle D sX hX sY hY f ∈
      cyclesOfDimension D sX (deltaDimension D sY Z)

AlgebraicGeometry.Space.IntegralClosedSubspace.flatPullbackMap_integralCycle_eq_preimageComponentsCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/EtalePullbackIdentity.lean, line 482.

Let f : X ⟶ Y be an étale morphism of good algebraic spaces over the base B of Situation 0EDT and let Z ⊆ Y be an integral closed subspace, of δ-dimension m. Then

f^*[Z] = ∑ [Z'],

the sum running over the irreducible components Z' of the inverse image f^{-1}(Z) (in the sense of Remark 0EE8), each with coefficient one: the coefficient family of the cycle f^*[Z] is the formal sum AlgebraicGeometry.Space.IntegralClosedSubspace.preimageComponentsCycle of those components.

The left-hand side is the flat pullback AlgebraicGeometry.Space.flatPullbackMap of Stacks 0EP8 at relative dimension 0, which an étale morphism has by AlgebraicGeometry.Space.hasRelativeDimension_zero_of_isEtale, applied to the cycle [Z]; the pullback lands in degree n for any n with m + 0 = n.

theorem IntegralClosedSubspace.flatPullbackMap_integralCycle_eq_preimageComponentsCycle
    (sX : X ⟶ D.space) (hX : D.IsGood sX) (sY : Y ⟶ D.space) (hY : D.IsGood sY) {f : X ⟶ Y}
    (hf : IsEtale D.site D.base D.base_mem f) (hfc : f ≫ sY = sX)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem Y) (m n : ℤ)
    (hm : deltaDimension D sY Z = m) (hmn : m + ((0 : ℕ) : ℤ) = n) :
    (flatPullbackMap D sX hX sY hY f hfc 0
          (isFlat_of_isEtale D.site D.base D.base_mem hf)
          (hasRelativeDimension_zero_of_isEtale D.site D.base D.base_mem f hY.1 hf) m n hmn
        (integralCycle D sY m Z hm)).1 =
      Z.preimageComponentsCycle D sX hX sY hY f
Tag 0EPA, a lemma

Tag 0EPA in the Stacks Project.

AlgebraicGeometry.Space.isFlat_and_hasRelativeDimension_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatCompositeRelativeDimension.lean, line 64. The attribute's comment: “the composite is flat of relative dimension r + s”.

Let X/B, Y/B and Z/B be good algebraic spaces over the base of D and let f : X ⟶ Y and g : Y ⟶ Z be morphisms over the base which are flat of relative dimensions r and s. Then the composite f ≫ g is flat of relative dimension r + s: it is locally of finite type, flat, and of relative dimension r + s.

theorem isFlat_and_hasRelativeDimension_comp (D : BaseSpaceDimensionSituation.{u})
    {X Y Z : (BigFppfOver D.site D.base D.base_mem)ᵒᵖ ⥤ Type u}
    (sX : X ⟶ D.space) (hX : D.IsGood sX) (sY : Y ⟶ D.space) (hY : D.IsGood sY)
    (sZ : Z ⟶ D.space) (hZ : D.IsGood sZ) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hfbase : f ≫ sY = sX) (hgbase : g ≫ sZ = sY) (r s : ℕ)
    (hff : IsFlat D.site D.base D.base_mem f)
    (hfr : HasRelativeDimension r D.site D.base D.base_mem f)
    (hgf : IsFlat D.site D.base D.base_mem g)
    (hgs : HasRelativeDimension s D.site D.base D.base_mem g) :
    IsLocallyOfFiniteType D.site D.base D.base_mem (f ≫ g) ∧
      IsFlat D.site D.base D.base_mem (f ≫ g) ∧
        HasRelativeDimension (r + s) D.site D.base D.base_mem (f ≫ g)

AlgebraicGeometry.Space.isFlat_and_hasRelativeDimension_comp_and_flatPullbackMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullbackComposition.lean, line 222. The attribute's comment: “both assertions: g ∘ f is flat of relative dimension r + s, and f^ ∘ g^ = (g ∘ f)^* as maps Z_k(Z) → Z_{k+r+s}(X)”.

In Situation 0EDT let X/B, Y/B and Z/B be good and let f : X ⟶ Y and g : Y ⟶ Z be morphisms over the base which are flat of relative dimensions r and s. Then

  1. g ∘ f is flat of relative dimension r + s (and locally of finite type), and
  2. f^* ∘ g^* = (g ∘ f)^* as maps Z_k(Z) → Z_{k+r+s}(X), for every k.

The degree of the target is any n with k + (r + s) = n, which is how AlgebraicGeometry.Space.flatPullbackMap is graded. The flat pullback along g ∘ f in part (2) is formed with the flatness and relative dimension that part (1) provides.

theorem isFlat_and_hasRelativeDimension_comp_and_flatPullbackMap_comp :
    (IsLocallyOfFiniteType D.site D.base D.base_mem (f ≫ g) ∧
      IsFlat D.site D.base D.base_mem (f ≫ g) ∧
        HasRelativeDimension (r + s) D.site D.base D.base_mem (f ≫ g)) ∧
      ∀ (k n : ℤ) (hn : k + ((r + s : ℕ) : ℤ) = n),
        (flatPullbackMap D sX hX sY hY f hfbase r hff hfr (k + (s : ℤ)) n
            (by push_cast at hn; omega)).comp
          (flatPullbackMap D sY hY sZ hZ g hgbase s hgf hgs k (k + (s : ℤ)) rfl) =
        flatPullbackMap D sX hX sZ hZ (f ≫ g)
          (comp_structureMorphism_eq D sX sY sZ f g hfbase hgbase) (r + s)
          (isFlat_and_hasRelativeDimension_comp D sX hX sY hY sZ hZ f g hfbase hgbase r s
            hff hfr hgf hgs).2.1
          (isFlat_and_hasRelativeDimension_comp D sX hX sY hY sZ hZ f g hfbase hgbase r s
            hff hfr hgf hgs).2.2 k n hn
Tag 0EPB, a lemma

Tag 0EPB in the Stacks Project.

AlgebraicGeometry.Space.flatPullback_closedSubspaceCycle_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullbackAssociatedCycle.lean, line 591. The attribute's comment: “part (1)”.

Stacks 0EPB, part (1). In Situation 0EDT let X/B and Y/B be good and let f : X ⟶ Y be a morphism over the base which is flat of relative dimension r. Let Z ⊆ Y be a closed subspace with dim_δ(Z) ≤ k. Then dim_δ(f^{-1}(Z)) ≤ k + r and

[f^{-1}(Z)]_{k+r} = f^*[Z]_k in Z_{k+r}(X).

The cycle of a closed subspace is AlgebraicGeometry.Space.closedSubspaceCycle (Stacks 0EE9) and the flat pullback is AlgebraicGeometry.Space.flatPullbackMap (Stacks 0EP8).

theorem flatPullback_closedSubspaceCycle_preimage (sX : X ⟶ D.space) (hX : D.IsGood sX)
    (sY : Y ⟶ D.space) (hY : D.IsGood sY) (f : X ⟶ Y) (hbase : f ≫ sY = sX) (r : ℕ)
    (hflat : IsFlat D.site D.base D.base_mem f)
    (hr : HasRelativeDimension r D.site D.base D.base_mem f) (k : ℤ) (Z : Subfunctor Y)
    (hZ : IsClosedSubspace D.site D.base D.base_mem Z)
    (hZk : deltaDimensionSubspace D sY hY Z hZ ≤ (k : EInt)) :
    ∃ hdim : deltaDimensionSubspace D sX hX (Z.preimage f)
        (isClosedSubspace_preimage D.site D.base D.base_mem f Z hY.1 hX.1 hZ) ≤
          ((k + (r : ℤ) : ℤ) : EInt),
      closedSubspaceCycle D sX hX (Z.preimage f)
          (isClosedSubspace_preimage D.site D.base D.base_mem f Z hY.1 hX.1 hZ) (k + (r : ℤ))
          hdim =
        flatPullbackMap D sX hX sY hY f hbase r hflat hr k (k + (r : ℤ)) rfl
          (closedSubspaceCycle D sY hY Z hZ k hZk)

AlgebraicGeometry.Space.flatPullback_associatedCycle_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullbackAssociatedCycle.lean, line 723. The attribute's comment: “part (2)”.

Stacks 0EPB, part (2). In Situation 0EDT let X/B and Y/B be good and let f : X ⟶ Y be a morphism over the base which is flat of relative dimension r. Let F be a coherent 𝒪_Y-module with dim_δ(Supp(F)) ≤ k. Then dim_δ(Supp(f^*F)) ≤ k + r and

f^*[F]_k = [f^*F]_{k+r} in Z_{k+r}(X).

The cycle of a coherent module is AlgebraicGeometry.Space.associatedCycle (Stacks 0EEB), read at any choice γ_X, γ_Y of geometric points over the points of X and Y; the pullback f^*F is coherent by AlgebraicGeometry.Space.isCoherent_modulePullback, X being locally Noetherian.

theorem flatPullback_associatedCycle_modulePullback (sX : X ⟶ D.space) (hX : D.IsGood sX)
    (sY : Y ⟶ D.space) (hY : D.IsGood sY) (f : X ⟶ Y) (hbase : f ≫ sY = sX) (r : ℕ)
    (hflat : IsFlat D.site D.base D.base_mem f)
    (hr : HasRelativeDimension r D.site D.base D.base_mem f)
    (F : Modules.{u, u} D.site D.base D.base_mem Y hY.1)
    [IsCoherent D.site D.base D.base_mem Y hY.1 F] (k : ℤ)
    (hFk : deltaDimensionClosed D sY hY (moduleSupport D.site D.base D.base_mem hY.1 F)
      (isClosed_moduleSupport D.site D.base D.base_mem hY.1 F) ≤ (k : EInt))
    (γY : points D.site D.base D.base_mem Y → GeometricPoint D.site D.base D.base_mem Y)
    (hγY : ∀ y, (γY y).LiesOver y)
    (γX : points D.site D.base D.base_mem X → GeometricPoint D.site D.base D.base_mem X)
    (hγX : ∀ x, (γX x).LiesOver x) :
    letI : IsCoherent D.site D.base D.base_mem X hX.1
        ((modulePullback D.site D.base D.base_mem
          (ObjectProperty.homMk f :
            (⟨X, hX.1⟩ : AlgebraicSpaces D.site D.base D.base_mem) ⟶ ⟨Y, hY.1⟩)).obj F) :=
      haveI : Fact (HasEtaleLocalProperty D.site D.base D.base_mem X
          (fun V : Scheme.{u} => IsLocallyNoetherian V)) :=
        ⟨hasEtaleLocalProperty_isLocallyNoetherian_of_isLocallyOfFiniteType D.site D.base
          D.base_mem hX.1 D.isAlgebraicSpace sX hX.2.2 D.locallyNoetherian⟩
      isCoherent_modulePullback D.site D.base D.base_mem
        (ObjectProperty.homMk f :
          (⟨X, hX.1⟩ : AlgebraicSpaces D.site D.base D.base_mem) ⟶ ⟨Y, hY.1⟩) F inferInstance
    ∃ hdim : deltaDimensionClosed D sX hX
        (moduleSupport D.site D.base D.base_mem hX.1
          ((modulePullback D.site D.base D.base_mem
            (ObjectProperty.homMk f :
              (⟨X, hX.1⟩ : AlgebraicSpaces D.site D.base D.base_mem) ⟶ ⟨Y, hY.1⟩)).obj F))
        (isClosed_moduleSupport D.site D.base D.base_mem hX.1 _) ≤
          ((k + (r : ℤ) : ℤ) : EInt),
      flatPullbackMap D sX hX sY hY f hbase r hflat hr k (k + (r : ℤ)) rfl
          (associatedCycle D sY hY F k γY hγY hFk) =
        associatedCycle D sX hX
          ((modulePullback D.site D.base D.base_mem
            (ObjectProperty.homMk f :
              (⟨X, hX.1⟩ : AlgebraicSpaces D.site D.base D.base_mem) ⟶ ⟨Y, hY.1⟩)).obj F)
          (k + (r : ℤ)) γX hγX hdim
Sources

Section82.11 Push and pull#

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

Tag 0EPD, a lemma

Tag 0EPD in the Stacks Project.

AlgebraicGeometry.Space.isProper_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperFlatBaseChange.lean, line 195. The attribute's comment: “first assertion: the base change of a proper morphism is proper”.

Stacks 0EPD, first assertion, by way of Stacks 04WP. In a cartesian square of algebraic spaces over S the base change f' of a proper morphism f is proper.

theorem isProper_of_isPullback
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (sq : IsPullback g' f' f g) (hf : IsProper B S hS f) :
    IsProper B S hS f'

AlgebraicGeometry.Space.isFlat_and_hasRelativeDimension_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperFlatBaseChange.lean, line 242. The attribute's comment: “second assertion: the base change of a morphism flat of relative dimension r is flat of relative dimension r”.

Stacks 0EPD, second assertion. In Situation 0EDT let the four corners of a cartesian square of algebraic spaces over B be good and let g : Y' ⟶ Y be a morphism over B which is flat of relative dimension r. Then the base change g' : X' ⟶ X is flat of relative dimension r: it is locally of finite type, flat, and of relative dimension r.

Local finite type of g' is goodness of X'/B and the cancellation of Stacks 0462 applied to g' ≫ sX = sX', flatness is Stacks 03MO, and the relative dimension is AlgebraicGeometry.Space.hasRelativeDimension_of_isPullback, which is part (1) of Stacks 04NS.

theorem isFlat_and_hasRelativeDimension_of_isPullback
    (sX' : X' ⟶ D.space) (hX' : D.IsGood sX') (sX : X ⟶ D.space) (hX : D.IsGood sX)
    (sY' : Y' ⟶ D.space) (hY' : D.IsGood sY') (sY : Y ⟶ D.space) (hY : D.IsGood sY)
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
    (hg'base : g' ≫ sX = sX') (hgbase : g ≫ sY = sY') (sq : IsPullback g' f' f g) (r : ℕ)
    (hgflat : IsFlat D.site D.base D.base_mem g)
    (hgr : HasRelativeDimension r D.site D.base D.base_mem g) :
    IsLocallyOfFiniteType D.site D.base D.base_mem g' ∧
      IsFlat D.site D.base D.base_mem g' ∧
        HasRelativeDimension r D.site D.base D.base_mem g'

AlgebraicGeometry.Space.flatPullback_properPushforward_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperFlatBaseChange.lean, line 644. The attribute's comment: “third assertion: the identity g^ f_ α = f'_ (g')^ α in Z_{k+r}(Y') for an arbitrary k-cycle α, at the source's hypotheses”.

Stacks 0EPD, third assertion. In Situation 0EDT let the four corners of a cartesian square of good algebraic spaces over B be good, let f : X ⟶ Y be proper and let g : Y' ⟶ Y be flat of relative dimension r. Then for every k-cycle α on X

g^*f_*α = f'_*(g')^*α

in Z_{k+r}(Y').

Nothing is carried. The pushforward along f' is legitimate because f' is proper, which is the first assertion AlgebraicGeometry.Space.isProper_of_isPullback and appears in the statement; the pullback along g' is legitimate because g' is flat of relative dimension r, which is the second assertion AlgebraicGeometry.Space.isFlat_and_hasRelativeDimension_of_isPullback and is written out as the hypotheses hg'flat and hg'r so that the degree bookkeeping stays explicit.

The two numerical inputs are proved. One is the degree count at the generic points, deg(Z/Z')·m_{T'}(g^{-1}(Z')) = ∑_T m_T((g')^{-1}(Z))·deg(T/T'), which is Space.BaseChangeDegreeCount.properCycleDegree_mul_flatPullbackMult_eq_finsum_of_isProper of StacksFrontier.AlgebraicGeometry.Spaces.Chow.ProperFlatBaseChangeDegreeCount: the source's route ([Z] = [𝒪_Z]_k, part (1) of Stacks 0EP3 on both sides, and flat base change in degree zero, part (1) of Stacks 073K) read at one pair of generic points. The other is that the left-hand side of the count is the whole coefficient of g^*f_*[Z] at T', by AlgebraicGeometry.Space.finsum_properCycleMult_mul_flatPullbackMult. The count is bundled into AlgebraicGeometry.Space.ProperFlatBaseChangeComparison and handed to AlgebraicGeometry.Space.flatPullback_properPushforward above, which is where the passage from a prime cycle to an arbitrary cycle is carried out.

theorem flatPullback_properPushforward_of_isPullback (sq : IsPullback g' f' f g)
    (hfproper : IsProper D.site D.base D.base_mem f)
    (k n : ℤ) (hkn : k + (r : ℤ) = n) (α : CycleGroup D sX k) :
    flatPullbackMap D sY' hY' sY hY g hgbase r hgflat hgr k n hkn
        (properCyclePushforward D sX hX sY hY hfbase hfproper.2.1.2 k α) =
      properCyclePushforward D sX' hX' sY' hY' hf'base
        (isProper_of_isPullback D.site D.base D.base_mem hX'.1 hX.1 hY'.1 hY.1 sq hfproper).2.1.2
        n (flatPullbackMap D sX' hX' sX hX g' hg'base r hg'flat hg'r k n hkn α)

AlgebraicGeometry.Space.flatPullback_properPushforward', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperFlatBaseChangeGenericPoints.lean, line 282. The attribute's comment: “third assertion: the identity g^ f_ α = f'_ (g')^ α in Z_{k+r}(Y') for an arbitrary k-cycle α, with no comparison datum and no numerical identity carried”.

The identity g^*f_*α = f'_*(g')^*α in Z_{k+r}(Y'), for a cartesian square of good algebraic spaces over B with f proper and g flat of relative dimension r, and for an arbitrary k-cycle α on X.

alias flatPullback_properPushforward'

AlgebraicGeometry.Space.flatPullback_properPushforward_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperFlatBaseChangeUnconditional.lean, line 246. The attribute's comment: “third assertion: the identity g^ f_ α = f'_ (g')^ α in Z_{k+r}(Y') for an arbitrary k-cycle α, at the source's hypotheses”.

Stacks 0EPD, third assertion. In Situation 0EDT let

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

be a cartesian square of good algebraic spaces over B, let f : X ⟶ Y be proper and let g : Y' ⟶ Y be flat of relative dimension r. Then for every k-cycle α on X

g^*f_*α = f'_*(g')^*α

in Z_{k+r}(Y').

Nothing is assumed: the pushforward along f' is legitimate because f' is proper, which is the first assertion AlgebraicGeometry.Space.isProper_of_isPullback; the pullback along g' is legitimate because g' is flat of relative dimension r, which is the second assertion AlgebraicGeometry.Space.isFlat_and_hasRelativeDimension_of_isPullback; and both are written out in the statement rather than carried. The identity itself is AlgebraicGeometry.Space.flatPullback_properPushforward, whose comparison at the generic points is AlgebraicGeometry.Space.properFlatBaseChangeComparison.

A CycleGroup is never transported along an equality of degrees, so the identity is stated at a pair k, n with k + r = n and the degree equality as an explicit argument, which is the convention of AlgebraicGeometry.Space.flatPullbackMap.

theorem flatPullback_properPushforward_unconditional (sq : IsPullback g' f' f g)
    (hfproper : IsProper D.site D.base D.base_mem f)
    (k n : ℤ) (hkn : k + (r : ℤ) = n) (α : CycleGroup D sX k) :
    flatPullbackMap D sY' hY' sY hY g hgbase r hgflat hgr k n hkn
        (properCyclePushforward D sX hX sY hY hfbase hfproper.2.1.2 k α) =
      properCyclePushforward D sX' hX' sY' hY' hf'base
        (isProper_of_isPullback D.site D.base D.base_mem hX'.1 hX.1 hY'.1 hY.1 sq hfproper).2.1.2
        n (flatPullbackMap D sX' hX' sX hX g' hg'base r
          (isFlat_and_hasRelativeDimension_of_isPullback D sX' hX' sX hX sY' hY' sY hY hg'base
            hgbase sq r hgflat hgr).2.1
          (isFlat_and_hasRelativeDimension_of_isPullback D sX' hX' sX hX sY' hY' sY hY hg'base
            hgbase sq r hgflat hgr).2.2 k n hkn α)
Tag 0EPE, a lemma

Tag 0EPE in the Stacks Project.

AlgebraicGeometry.Space.properPushforward_finiteLocallyFreeCyclePullback_eq_zsmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FiniteLocallyFreeConstructedPullback.lean, line 456. The attribute's comment: “f_ f^ alpha = d alpha”.

In Situation 0EDT let X/B and Y/B be good and let f : X ⟶ Y be finite locally free of degree d. Then

f_*f^*α = dα

for every α ∈ Z_k(Y), with f^* the flat pullback of Stacks 0EP8 (AlgebraicGeometry.Space.finiteLocallyFreeCyclePullback, whose flatness and relative-dimension hypotheses are the second conclusion of Stacks 0EPE) and f_* the proper pushforward of Stacks 0EP1 (whose quasi-compactness hypothesis is the first conclusion).

theorem properPushforward_finiteLocallyFreeCyclePullback_eq_zsmul
    (sX : X.obj ⟶ D.space) (hX : D.IsGood sX) (sY : Y.obj ⟶ D.space) (hY : D.IsGood sY)
    (f : X ⟶ Y) (hbase : f.hom ≫ sY = sX) (d : ℕ)
    (hf : IsFiniteLocallyFreeOfRank D.site D.base D.base_mem f d) (k : ℤ)
    (α : CycleGroup D sY k) :
    properPushforward D sX hX sY hY hbase
        (isQuasiCompact_hom_of_isFiniteLocallyFreeOfRank D f d hf) k
        ((finiteLocallyFreeCyclePullback D sX hX sY hY f hbase d hf).map k k (by simp) α) =
      (d : ℤ) • α

AlgebraicGeometry.Space.isProper_of_isFiniteLocallyFreeOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FiniteLocallyFreePushPull.lean, line 237. The attribute's comment: “f is proper”.

Stacks 0EPE, first conclusion. A finite locally free morphism of degree d of algebraic spaces over S is proper.

A finite locally free morphism is finite by Stacks 0416, and a finite morphism is proper by Stacks 04NZ. The goodness hypotheses of Situation 0EDT are not used, so the conclusion is drawn for an arbitrary morphism of algebraic spaces over S.

theorem isProper_of_isFiniteLocallyFreeOfRank
    (hcross : FiniteLocallyFreeRankChartComparison B S hS)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (d : ℕ)
    (hf : IsFiniteLocallyFreeOfRank B S hS f d) :
    IsProper B S hS f.hom

AlgebraicGeometry.Space.isFlat_and_hasRelativeDimension_zero_of_isFiniteLocallyFreeOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FiniteLocallyFreePushPull.lean, line 263. The attribute's comment: “f is flat of relative dimension 0”.

Stacks 0EPE, second conclusion. A finite locally free morphism of degree d of algebraic spaces over S is flat of relative dimension 0: it is flat and locally of finite type, and has relative dimension 0 at every point of its source.

Flatness is Stacks 0416. For the relative dimension, the morphism is finite, hence locally quasi-finite and locally of finite type, and Stacks 04NV turns local quasi-finiteness into the vanishing of the relative dimension at every point. The goodness hypotheses of Situation 0EDT are not used.

theorem isFlat_and_hasRelativeDimension_zero_of_isFiniteLocallyFreeOfRank
    (hcross : FiniteLocallyFreeRankChartComparison B S hS)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (d : ℕ)
    (hf : IsFiniteLocallyFreeOfRank B S hS f d) :
    IsFlat B S hS f.hom ∧ IsLocallyOfFiniteType B S hS f.hom ∧
      HasRelativeDimension 0 B S hS f.hom

AlgebraicGeometry.Space.properPushforward_flatCyclePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FiniteLocallyFreePushPull.lean, line 376. The attribute's comment: “f_ f^ alpha = d alpha”.

Stacks 0EPE, third conclusion. In Situation 0EDT let X/B and Y/B be good and let f : X ⟶ Y be finite locally free of degree d. Then f_*f^*α = dα for every α ∈ Z_k(Y).

Only the term of the flat pullback at W' itself survives in the coefficient of f_*f^*α at an integral closed subspace W' ⊆ Y, by AlgebraicGeometry.Space.eq_cycleImageSubspace_of_mult_ne_zero, and what is left is α_{W'} times the degree hdeg of the fibre over the generic point of W'; at a W' of δ-dimension other than k the coefficient of α there vanishes and both sides are zero.

theorem properPushforward_flatCyclePullback
    (hcross : FiniteLocallyFreeRankChartComparison D.site D.base D.base_mem)
    (sX : X.obj ⟶ D.space) (hX : D.IsGood sX) (sY : Y.obj ⟶ D.space) (hY : D.IsGood sY)
    (f : X ⟶ Y) (hbase : f.hom ≫ sY = sX) (d : ℕ)
    (hf : IsFiniteLocallyFreeOfRank D.site D.base D.base_mem f d)
    (pb : FlatCyclePullback D sX hX sY hY f.hom 0)
    (k : ℤ)
    (hdeg : ∀ W : IntegralClosedSubspace D.site D.base D.base_mem Y.obj,
      deltaDimension D sY W = k →
      ∑ᶠ T ∈ {T : IntegralClosedSubspace D.site D.base D.base_mem X.obj |
          cycleImageSubspace D sY hY f.hom T = W},
        pb.mult W T * (cycleResidueDegree D sX hX sY hY f.hom
          (T.ambientGenericPoint D.site D.base D.base_mem) : ℤ) = (d : ℤ))
    (α : CycleGroup D sY k) :
    properPushforward D sX hX sY hY hbase
        (isQuasiCompact_of_isFiniteLocallyFreeOfRank D.site D.base D.base_mem hcross f d hf) k
        (pb.map k k (by simp) α) = (d : ℤ) • α

AlgebraicGeometry.Space.isProper_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FiniteLocallyFreePushPullUnranked.lean, line 91. The attribute's comment: “f is proper”.

Stacks 0EPE, first conclusion. A finite locally free morphism of algebraic spaces over S is proper.

A finite locally free morphism is finite by Stacks 0416, and a finite morphism is proper by Stacks 04NZ. Neither the rank nor the goodness hypotheses of Situation 0EDT are used, so the conclusion is drawn for the unranked definition of Stacks 03ZV and an arbitrary morphism of algebraic spaces over S.

theorem isProper_of_isFiniteLocallyFree {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : IsFiniteLocallyFree B S hS f) :
    IsProper B S hS f.hom

AlgebraicGeometry.Space.isFlat_and_hasRelativeDimension_zero_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FiniteLocallyFreePushPullUnranked.lean, line 113. The attribute's comment: “f is flat of relative dimension 0”.

Stacks 0EPE, second conclusion. A finite locally free morphism of algebraic spaces over S is flat of relative dimension 0: it is flat and locally of finite type, and has relative dimension 0 at every point of its source.

Flatness is Stacks 0416. For the relative dimension, the morphism is finite, hence locally quasi-finite and locally of finite type, and Stacks 04NV turns local quasi-finiteness into the vanishing of the relative dimension at every point. Neither the rank nor the goodness hypotheses of Situation 0EDT are used.

theorem isFlat_and_hasRelativeDimension_zero_of_isFiniteLocallyFree
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsFiniteLocallyFree B S hS f) :
    IsFlat B S hS f.hom ∧ IsLocallyOfFiniteType B S hS f.hom ∧
      HasRelativeDimension 0 B S hS f.hom

AlgebraicGeometry.Space.properPushforward_flatCyclePullback_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FiniteLocallyFreePushPullUnranked.lean, line 147. The attribute's comment: “f_ f^ alpha = d alpha”.

Stacks 0EPE, third conclusion. In Situation 0EDT let X/B and Y/B be good and let f : X ⟶ Y be finite locally free, with hdeg recording the degree d of its fibre over the generic point of every integral closed subspace of δ-dimension k. Then f_*f^*α = dα for every α ∈ Z_k(Y).

Only the term of the flat pullback at W' itself survives in the coefficient of f_*f^*α at an integral closed subspace W' ⊆ Y, by AlgebraicGeometry.Space.eq_cycleImageSubspace_of_mult_ne_zero, and what is left is α_{W'} times the degree hdeg of the fibre over the generic point of W'; at a W' of δ-dimension other than k the coefficient of α there vanishes and both sides are zero.

Finite local freeness enters only through quasi-compactness, which is all the proper pushforward of Stacks 0EP1 asks for, so the rank of Stacks 03ZV is not imposed on f: the degree d is pinned by hdeg alone.

theorem properPushforward_flatCyclePullback_of_isFiniteLocallyFree
    (sX : X.obj ⟶ D.space) (hX : D.IsGood sX) (sY : Y.obj ⟶ D.space) (hY : D.IsGood sY)
    (f : X ⟶ Y) (hbase : f.hom ≫ sY = sX) (d : ℕ)
    (hf : IsFiniteLocallyFree D.site D.base D.base_mem f)
    (pb : FlatCyclePullback D sX hX sY hY f.hom 0)
    (k : ℤ)
    (hdeg : ∀ W : IntegralClosedSubspace D.site D.base D.base_mem Y.obj,
      deltaDimension D sY W = k →
      ∑ᶠ T ∈ {T : IntegralClosedSubspace D.site D.base D.base_mem X.obj |
          cycleImageSubspace D sY hY f.hom T = W},
        pb.mult W T * (cycleResidueDegree D sX hX sY hY f.hom
          (T.ambientGenericPoint D.site D.base D.base_mem) : ℤ) = (d : ℤ))
    (α : CycleGroup D sY k) :
    properPushforward D sX hX sY hY hbase
        (isQuasiCompact_of_isFiniteLocallyFree D.site D.base D.base_mem f hf) k
        (pb.map k k (by simp) α) = (d : ℤ) • α
Sources

Section82.12 Preparation for principal divisors#

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

Tag 0EPZ, a lemma

Tag 0EPZ in the Stacks Project.

AlgebraicGeometry.Space.deltaDimensionIrreducible_closureSingleton_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/EffectiveCartierComponentDeltaDimension.lean, line 287. The attribute's comment: “part (2)”.

Stacks 0EPZ, part (2). In Situation 0EDT let X/B be good and assume X integral with dim_δ(X) = n. If Z is an irreducible component of an effective Cartier divisor D ⊆ X, then dim_δ(Z) = n - 1.

The component is presented by a generic point ξ of an irreducible component W of the closed subset |D| ⊆ |X|, and dim_δ(Z) is the δ-dimension of Stacks 0EDX of the irreducible closed subset closure {ξ} of |X|, the summand W contributes to dim_δ(D).

By part (1) the equality is equivalent to the component having codimension one in |X|, which is AlgebraicGeometry.Space.codimension_closureSingleton_eq_one_of_isEffectiveCartierDivisor; the passage between the two is the topological equivalence codimension_closureSingleton_eq_one_iff_dimensionFunction for the dimension function δ_{X/B} of Stacks 0EDN, which is where integrality of X and dim_δ(X) = n are used.

theorem deltaDimensionIrreducible_closureSingleton_isEffectiveCartierDivisor
    (D : BaseSpaceDimensionSituation.{u})
    {X : (BigFppfOver D.site D.base D.base_mem)ᵒᵖ ⥤ Type u} (sX : X ⟶ D.space)
    (hX : D.IsGood sX) (hint : IsIntegralSpace D.site D.base D.base_mem X) {n : ℤ}
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt))
    (E : ClosedSubspaces D.site D.base D.base_mem X)
    (hE : IsEffectiveCartierDivisor D.site D.base D.base_mem ⟨X, hX.1⟩ E)
    {W : Set (subspacePointSet D.site D.base D.base_mem X E.1)}
    (hW : W ∈ irreducibleComponents (subspacePointSet D.site D.base D.base_mem X E.1))
    {ξ : subspacePointSet D.site D.base D.base_mem X E.1} (hξ : IsGenericPoint ξ W) :
    deltaDimensionIrreducible D sX hX
        (IrreducibleCloseds.closureSingleton (ξ : points D.site D.base D.base_mem X)) =
      n - 1

AlgebraicGeometry.Space.isPrimeDivisor_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrimeDivisorDeltaDimension.lean, line 249. The attribute's comment: “part (1)”.

Stacks 0EPZ, part (1). In Situation 0EDT let X/B be good and assume X integral with dim_δ(X) = n. For an integral closed subspace Z ⊆ X the following are equivalent: Z is a prime divisor of X; the set of points of Z has codimension one in |X|; and dim_δ(Z) = n - 1.

These are the hypotheses of the source and nothing else. The equivalence itself is isPrimeDivisor_tfae_of_isIntegralSpace, which also takes a dimension function on |X| with underlying function δ_{X/B}; that is not an input of Stacks 0EPZ but the conclusion of Stacks 0EDN, exists_dimensionFunction_inducedDimensionValue, applied to the standing data of Situation 0EDT: the base is a quasi-separated, locally Noetherian, universally catenary algebraic space with a dimension function, a quasi-separated algebraic space is decent, and a good X/B is decent and locally of finite type over the base.

theorem isPrimeDivisor_tfae (D : BaseSpaceDimensionSituation.{u})
    {X : (BigFppfOver D.site D.base D.base_mem)ᵒᵖ ⥤ Type u} (sX : X ⟶ D.space)
    (hX : D.IsGood sX) (hint : IsIntegralSpace D.site D.base D.base_mem X) {n : ℤ}
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt))
    (Z : IntegralClosedSubspace D.site D.base D.base_mem X) :
    List.TFAE
      [∃ W : PrimeDivisor D.site D.base D.base_mem X, W.subspace = Z.subspace,
        codimension (integralClosedSubspaceSupport D.site D.base D.base_mem hX.1 Z) = 1,
        deltaDimension D sX Z = n - 1]

AlgebraicGeometry.Space.isPrimeDivisor_tfae_of_isIntegralSpace', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrimeDivisorDeltaDimensionOfGood.lean, line 67. The attribute's comment: “part (1)”.

In Situation 0EDT let X/B be good and assume X integral with dim_δ(X) = n. For an integral closed subspace Z ⊆ X the following are equivalent: Z is a prime divisor of X; the set of points of Z has codimension one in |X|; and dim_δ(Z) = n - 1.

This is an alias of AlgebraicGeometry.Space.isPrimeDivisor_tfae, which is proved at these hypotheses in StacksFrontier.AlgebraicGeometry.Spaces.Chow.PrimeDivisorDeltaDimension. The bundled dimension function on |X| with underlying function δ_{X/B} that the engine AlgebraicGeometry.Space.isPrimeDivisor_tfae_of_isIntegralSpace takes is produced from goodness of X/B by Stacks 0EDN, AlgebraicGeometry.Space.exists_dimensionFunction_inducedDimensionValue: the base of Situation 0EDT is a quasi-separated, locally Noetherian, universally catenary algebraic space with a dimension function, a good X/B is decent and locally of finite type over it, and a quasi-separated algebraic space is decent.

alias isPrimeDivisor_tfae_of_isIntegralSpace'
Sources

Section82.13 Principal divisors#

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

Tag 0EQ1, a definition

Tag 0EQ1 in the Stacks Project.

AlgebraicGeometry.Space.principalDivisorCycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrincipalDivisor.lean, line 649. The attribute's comment: “div(f) = ∑ ord_Z(f) [Z] as an element of Z_{n-1}(X); the δ-dimension of a prime divisor is n-1 by Stacks 0EPZ, whose dimension-function hypotheses d and hd are Stacks 0EDN, carried; local finiteness is Stacks 0ENN, the argument hfin, discharged by locallyFinite_principalDivisorCoefficients_ne_zero in principalDivisorCycleOfRegularLocus”.

Stacks 0EQ1. The principal divisor associated to f ∈ R(X)^*, that is div(f) = ∑_Z ord_Z(f) [Z], as an element of Z_{n-1}(X) for X/B good and integral with dim_δ(X) = n.

This is the principal divisor of Stacks 0ENP read as a cycle: the formal sum is the same, and it is an (n-1)-cycle because a prime divisor of such an X has δ-dimension n - 1 by Stacks 0EPZ. Local finiteness is Stacks 0ENN, the argument hfin, which AlgebraicGeometry.Space.principalDivisorCycleOfRegularLocus discharges.

def principalDivisorCycle
    (hfin : LocallyFinite fun W : PrimeDivisor D.site D.base D.base_mem X =>
      if principalDivisorCoefficients D.site D.base D.base_mem hX.1 hdec emb f hf W = 0 then ∅
      else W.support D.site D.base D.base_mem X)
    (hint : IsIntegralSpace D.site D.base D.base_mem X)
    (d : DimensionFunction (points D.site D.base D.base_mem X))
    (hd : ∀ x, d x = D.deltaValue sX x) {n : ℤ}
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt)) :
    CycleGroup D sX (n - 1)

AlgebraicGeometry.Space.principalDivisorCycleOfRegularLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrincipalDivisor.lean, line 683. The attribute's comment: “div(f) in Z_{n-1}(X), with local finiteness (Stacks 0ENN) proved from a nonempty open U over which f is invertible, the datum (U, hUopen, hUne, hreg) of the first sentence of the source's own proof of that lemma; the dimension-function hypotheses d and hd are Stacks 0EDN, carried”.

Stacks 0EQ1. The principal divisor div(f) = ∑_Z ord_Z(f) [Z] of a rational function f ∈ R(X)^* as an element of Z_{n-1}(X), with the local finiteness of Stacks 0ENN proved from a nonempty open subset of |X| over which f is invertible.

def principalDivisorCycleOfRegularLocus
    (hN : HasEtaleLocalProperty D.site D.base D.base_mem X
      (fun Y : Scheme.{u} => IsLocallyNoetherian Y))
    (U : Set (points D.site D.base D.base_mem X)) (hUopen : IsOpen U) (hUne : U.Nonempty)
    (hreg : ∀ W : PrimeDivisor D.site D.base D.base_mem X,
      W.genericPoint D.site D.base D.base_mem X ∈ U →
        ∃ r : ↥(W.genericHenselianLocalRing D.site D.base D.base_mem hX.1 hdec), IsUnit r ∧
          emb W f =
            algebraMap _ (W.genericTotalFractionRing D.site D.base D.base_mem hX.1 hdec) r)
    (hint : IsIntegralSpace D.site D.base D.base_mem X)
    (d : DimensionFunction (points D.site D.base D.base_mem X))
    (hd : ∀ x, d x = D.deltaValue sX x) {n : ℤ}
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt)) :
    CycleGroup D sX (n - 1)

AlgebraicGeometry.Space.rationalFunctionPrincipalDivisorCycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrincipalDivisorCanonical.lean, line 73. The attribute's comment: “div(f) = ∑ ord_Z(f) [Z] in Z_{n-1}(X) for X/B good and integral with dim_δ(X) = n and f ∈ R(X)^*; ord_Z(f) is read through the canonical embedding of Stacks 0ENK, local finiteness is Stacks 0ENN proved, the δ-dimension n - 1 of a prime divisor is Stacks 0EPZ with the dimension function of Stacks 0EDN proved; nothing carried”.

The principal divisor associated to f ∈ R(X)^*, div(f) = div_X(f) = ∑_Z ord_Z(f) [Z], as an element of Z_{n-1}(X), for X/B good and integral with dim_δ(X) = n.

def rationalFunctionPrincipalDivisorCycle {n : ℤ}
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt))
    (f : (rationalFunctions D.site D.base D.base_mem hX.1)ˣ) :
    CycleGroup D sX (n - 1)
Tag 0EQ2, a lemma

Tag 0EQ2 in the Stacks Project.

AlgebraicGeometry.Space.etalePullback_principalDivisorCycle_eq_sum_components_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/EtalePullbackPrincipalDivisor.lean, line 359. The attribute's comment: “REDUCED, not proved: the displayed equality of cycles on X — coefficientwise at every integral closed subspace, with the sum over the irreducible components of X — HOLDS IF AND ONLY IF it holds at the integral closed subspaces of δ-dimension n-1. Proved away from them, where both sides vanish, both being (n-1)-cycles. The coefficient identity at those subspaces is NOT proved and NOT assumed: it is the source's steps three to six, namely the square of henselian local rings of Remark 0EPL, the multiplicity one of Lemma 0EPY, the length equality along a flat unramified map of Lemma 02M1 and the length decomposition of Lemma 02QG. Hypotheses: hrel, the relative dimension 0 of the étale morphism, flatness itself being supplied from Stacks 0467; and, on each irreducible component, the fields of EtaleComponentDivisorData — goodness over the base, the three hypotheses of Stacks 0ENK with the embeddings they go with, the dominance of f restricted to the component (the source's first step, which makes g ∘ f|_{X'} defined), that g ∘ f|_{X'} is in R(X')^*, local finiteness of its divisor (Stacks 0ENN) and the dimension function of Stacks 0EDN. That dim_δ(X') = n for every component, the source's second paragraph, is proved”.

In Situation 0EDT let f : X ⟶ Y be an étale morphism of good algebraic spaces over B, let Y be integral with dim_δ(Y) = n and let g ∈ R(Y)^*. Then the identity of cycles on X

f^*(div_Y(g)) = ∑_{X'} (X' → X)_* div_{X'}(g ∘ f|_{X'}),

the sum being over the irreducible components X' of X (Remark 0EE8), holds at every integral closed subspace Z ⊆ X, coefficientwise, if and only if it holds at those of δ-dimension n - 1.

theorem etalePullback_principalDivisorCycle_eq_sum_components_iff
    (data : EtaleComponentDivisorData D sX hX sY hY f hbase hetale hintY n hnY g) :
    (∀ Z : IntegralClosedSubspace D.site D.base D.base_mem X,
        (etalePullbackPrincipalDivisorCycle D sX hX sY hY hbase hetale hrel hintY embY g hg
            hfinY dY hdY hnY).1 Z =
          data.componentPushforwardCoeff Z) ↔
      ∀ Z : IntegralClosedSubspace D.site D.base D.base_mem X,
        deltaDimension D sX Z = n - 1 →
          (etalePullbackPrincipalDivisorCycle D sX hX sY hY hbase hetale hrel hintY embY g hg
              hfinY dY hdY hnY).1 Z =
            data.componentPushforwardCoeff Z

AlgebraicGeometry.Space.etalePullback_principalDivisorCycle_eq_sum_components_iff_eq_ord_closureImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/EtalePullbackPrincipalDivisorComponents.lean, line 721. The attribute's comment: “REDUCED to ONE identity of integers, with NOTHING about the components assumed. The displayed equality of cycles on X — coefficientwise, the sum over the irreducible components of X — HOLDS IF AND ONLY IF at every integral closed subspace Z of X of δ-dimension n-1 the sum over the components X' of ord_Z(g ∘ f|_{X'}), computed on X', equals ord_{Z'}(g) for Z' the image of Z in Y. This is that equivalence. Proved here, in both halves: away from δ-dimension n-1 both sides vanish, both being (n-1)-cycles, which on the right uses dim_δ(X') = n for every component (the source's second paragraph, PROVED in deltaDimensionClosed_univ_irreducibleComponentSubspace); and at δ-dimension n-1 the coefficient of the left side is ord_{Z'}(g) by Lemma 0EPY, for an ARBITRARY X, which is etalePullbackPrincipalDivisorCycle_apply_eq_apply_closureImage together with IntegralClosedSubspace.exists_eq_preimageComponent. The right side is formed through etaleComponentDivisorData, so the dominance of f restricted to a component — the source's first step, what makes g ∘ f|_{X'} defined, and formerly a field of EtaleComponentDivisorDataOfGood — is PROVED, in pointsMap_genericPoint_eq_genericPoint_irreducibleComponentSubspace: an étale morphism is flat, so generizations lift along |X| → |Y|, and a continuous generalizing map into a quasi-sober space carries the generic point of an irreducible component to the generic point of one, which for the irreducible |Y| is its generic point. The source's own route, openness of |f| plus local finiteness of the components, is not needed. The only input beyond the source's hypotheses is ComponentDivisorLocallyFinite, which is Stacks 0ENN on each component and is what makes div_{X'}(g ∘ f|_{X'}) a cycle at all; Stacks 0EQ1 takes it in the same shape on Y (TargetDivisorLocallyFinite) and this repository proves it from a nonempty open subset over which the function is invertible (locallyFinite_principalDivisorCoefficients_ne_zero). For X INTEGRAL the remaining identity of integers is PROVED and with it the whole of the source's displayed identity, which then reads f^* div_Y(g) = div_X(g ∘ f) in Z_{n-1}(X): etalePullbackPrincipalDivisorCycle_eq_principalDivisorCycle_of_isIntegralSpace, coefficientwise etalePullbackPrincipalDivisorCycle_apply_of_isIntegralSpace, through ord_rationalFunctionMap_eq_ord_of_isEtale. WHAT IS STILL MISSING, for an X with several components, is exactly the right-hand side of this equivalence, and it is the source's grouping of the branches at the generic point of Z over the components through it: ord_Z(g ∘ f|_{X'}) has to be identified with the sum of Ring.minimalPrimeOrd over the minimal primes 𝔭 of the local ring of an affine étale chart W of X at a point over the generic point of Z with componentOfBranch 𝔭 = X'. The partition itself is available (finsum_flatBranch_eq_finsum_component_finsum_flatBranch), the chart reading of g ∘ f|_{X'} is available with no flatness of f|_{X'} (rationalFunctionsToTotalFractionRing_rationalFunctionMap_componentChart, nonZeroDivisors_le_comap_chartGlobalSectionsRestrict), and the components of W ×_X X' are components of W (mem_irreducibleComponents_image_closedSubspaceBaseChangeChartProj), in the stalk-level form comap_stalkMap_closedSubspaceBaseChangeChartProj_mem_minimalPrimes; and the transport of Ring.minimalPrimeOrd along the surjection of local rings 𝒪_{W,w} → 𝒪_{W ×_X X', w'} is Ring.minimalPrimeOrd_map_of_surjective. So the grouping of the branches over the components is now proved, as finsum_minimalPrimeOrd_stalkMap_eq_finsum_branch_on_component, and so is the recognition of its left-hand side as ord_Z(g ∘ f|_{X'}): ord_rationalFunctionMap_eq_finsum_branch_on_component, through the stalk-level chart reading chartPointRationalFunctionMap_rationalFunctionMap_componentChart, which composes the two halves, rationalFunctionsToTotalFractionRing_rationalFunctionMap_componentChart on global sections and Scheme.totalFractionRingToStalkFractionRing_map_appTop from global sections to the local ring. The sum over ALL the branches of 𝒪_{W,w} is ord_{Z'}(g) on Y, with the same element of Q(𝒪_{W,w}): PrimeDivisor.ord_eq_finsum_minimalPrimeOrd_etaleChartComp. So the whole grouping of the branches, the content of the source's third to sixth paragraphs, is proved. The coefficient of the pushforward along the inclusion of a component is proved too, in componentDivisorPushforward_apply_pushforward and _apply_of_forall_ne, through properCyclePushforward_ι_eq_integralClosedSubspacePushforward: the inclusion of an irreducible component is the inclusion of an integral closed subspace, so the pushforward of Stacks 0EP1 along it is integralClosedSubspacePushforward, whose coefficients are the extension by zero of the coefficients on the component. WHAT NO DECLARATION PROVIDES is the CONVERSE presentation — that an integral closed subspace Z of X whose points lie in |X'| is the image of an integral closed subspace of X', of δ-dimension making it a prime divisor of X' — which is what cuts componentPushforwardCoeff Z, a sum over ALL the components, down to the components through the generic point of Z and matches each term with ord_{Z ∩ X'}(g ∘ f|_{X'}); nor is the partition of the minimal primes of 𝒪_{W,w} over those components (finsum_flatBranch_eq_finsum_component_finsum_flatBranch) joined to the two sums above”.

Stacks 0EQ2, reduced to one identity of orders of vanishing, and with no data on the components assumed. In Situation 0EDT let f : X ⟶ Y be an étale morphism of good algebraic spaces over B, let Y be integral with dim_δ(Y) = n and let g ∈ R(Y)^*. Then the identity of cycles on X

f^*(div_Y(g)) = ∑_{X'} (X' → X)_* div_{X'}(g ∘ f|_{X'}),

read coefficientwise over the irreducible components X' of X (Remark 0EE8), holds if and only if at every integral closed subspace Z ⊆ X of δ-dimension n - 1

∑_{X'} ord_Z(g ∘ f|_{X'}) = ord_{Z'}(g),

Z' being the image of Z in Y. That one identity of integers — the last step of the source's third to sixth paragraphs — is the whole of what is left.

Nothing about the components is assumed: the right-hand side is formed through AlgebraicGeometry.Space.etaleComponentDivisorData, whose only input is the local finiteness of Stacks 0ENN on each component, which is what makes div_{X'}(g ∘ f|_{X'}) a cycle at all and which Stacks 0EQ1 takes in the same form on Y. In particular the dominance of f|_{X'} is proved, not assumed (AlgebraicGeometry.Space.pointsMap_genericPoint_eq_genericPoint_irreducibleComponentSubspace).

Two reductions are combined. Away from δ-dimension n - 1 both sides vanish, both being (n-1)-cycles — on the right because every component has dim_δ(X') = n, the source's second paragraph, which is proved — the reduction of AlgebraicGeometry.Space.etalePullback_principalDivisorCycle_eq_sum_components_iff, taken here at the canonical embeddings and hence re-run rather than cited. At δ-dimension n - 1 the left-hand side is ord_{Z'}(g), which is Lemma 0EPY in the form AlgebraicGeometry.Space.etalePullbackPrincipalDivisorCycle_apply_eq_apply_closureImage, and that holds for an arbitrary X, not only an integral one.

theorem etalePullback_principalDivisorCycle_eq_sum_components_iff_eq_ord_closureImage
    (hfin : ComponentDivisorLocallyFinite D sX hX sY hY hetale hintY g hg) :
    (∀ Z : IntegralClosedSubspace D.site D.base D.base_mem X,
        (etalePullbackPrincipalDivisorCycleOfGood D sX hX sY hY hbase hetale hintY g hg
            hfinY hnY).1 Z =
          (etaleComponentDivisorData D sX hX sY hY f hbase hetale hintY n hnY g hg
            hfin).toEtaleComponentDivisorData.componentPushforwardCoeff Z) ↔
      ∀ Z : IntegralClosedSubspace D.site D.base D.base_mem X,
        deltaDimension D sX Z = n - 1 →
          (etaleComponentDivisorData D sX hX sY hY f hbase hetale hintY n hnY g hg
              hfin).toEtaleComponentDivisorData.componentPushforwardCoeff Z =
            (targetPrincipalDivisorCycle D sY hY hintY g hg hfinY hnY).1
              (Z.closureImage D.site D.base D.base_mem hY.1
                (D.isDecentSpace_of_isGood sY hY) f)

AlgebraicGeometry.Space.etalePullbackPrincipalDivisorCycle_apply_eq_componentPushforwardCoeff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/EtalePullbackPrincipalDivisorIdentity.lean, line 353. The attribute's comment: “the displayed equality of cycles on X, read coefficientwise at every integral closed subspace, the sum being over the irreducible components of X (Remark 0EE8); it is read coefficientwise because that family is only locally finite, so the right-hand side is not a sum in Z_{n-1}(X). Both sides are formed at the canonical Stacks 0ENK embeddings of genericFractionEmbedding, on Y and on each component, so the two orders of vanishing are taken at the same data and are tied through rationalFunctionMap. UNCONDITIONAL: nothing beyond the source's own hypotheses goes in. The left-hand side is the flat pullback of Stacks 0EP8 at relative dimension 0 (etalePullbackCycleMap), an etale morphism being flat by Stacks 0467 and of relative dimension 0; the right-hand side is the sum of the pushforwards of Stacks 0EP1 of the principal divisors of Stacks 0EQ1 on the components. The source's first step, dominance of f restricted to a component, is PROVED (pointsMap_genericPoint_eq_genericPoint_irreducibleComponentSubspace); its second paragraph, dim_delta(X') = n for every component, is PROVED (deltaDimensionClosed_univ_irreducibleComponentSubspace); the local finiteness of Stacks 0ENN on Y and on each component, which makes the principal divisors cycles at all, is PROVED (targetDivisorLocallyFinite_of_isGood, componentDivisorLocallyFinite_of_isGood, out of ordRationalFunction_mem_weilDivisor, the repository's Stacks 0ENN); and the source's third to sixth paragraphs are componentPushforwardCoeff_eq_ord_of_chart, which computes both sides on one affine etale chart of X through the generic point of Z -- also a chart of Y because f is etale -- as sums of Ring.minimalPrimeOrd over the branches at the chart point: the coefficient of the left side is ord_{Z'}(g) by Lemma 0EPY (etalePullbackPrincipalDivisorCycle_apply_eq_apply_closureImage) and is the sum over ALL the branches (PrimeDivisor.ord_eq_finsum_minimalPrimeOrd_etaleChartComp, Stacks 0ENM), each term of the right side is the subsum over the branches lying on its component (ord_rationalFunctionMap_eq_finsum_branch_on_component), and the branches are partitioned over the components through the generic point of Z (finsum_minimalPrimes_eq_finsum_componentSubspace), which is the source's last step that {1,...,t} is the disjoint union of the J(X'); that replaces the square of Remark 0EPL, Lemma 02M1 and Lemma 02QG”.

Stacks 0EQ2. In Situation 0EDT let f : X ⟶ Y be an étale morphism of good algebraic spaces over B, let Y be integral with dim_δ(Y) = n and let g ∈ R(Y)^*. Then, as cycles on X,

f^*(div_Y(g)) = ∑_{X'} (X' → X)_* div_{X'}(g ∘ f|_{X'}),

the sum being over the irreducible components X' of X (Remark 0EE8). The identity is read coefficientwise, at every integral closed subspace of X, because the family of irreducible components is only locally finite and the right-hand side is therefore not a sum in Z_{n-1}(X).

Both sides are formed at the canonical embeddings of Stacks 0ENK, on Y for g and on each component X' for g ∘ f|_{X'}, so that the two orders of vanishing are read at the same data and are tied to one another through AlgebraicGeometry.Space.rationalFunctionMap.

Nothing beyond the source's own hypotheses goes in. The dominance of f|_{X'}, the source's first step, is AlgebraicGeometry.Space.pointsMap_genericPoint_eq_genericPoint_irreducibleComponentSubspace; dim_δ(X') = n, the source's second paragraph, is AlgebraicGeometry.Space.deltaDimensionClosed_univ_irreducibleComponentSubspace; and the local finiteness of Stacks 0ENN, on Y and on each component, which is what makes each principal divisor a cycle at all, is discharged by AlgebraicGeometry.Space.targetDivisorLocallyFinite_of_isGood and AlgebraicGeometry.Space.componentDivisorLocallyFinite_of_isGood.

theorem etalePullbackPrincipalDivisorCycle_apply_eq_componentPushforwardCoeff
    (D : BaseSpaceDimensionSituation.{u})
    {X Y : (BigFppfOver D.site D.base D.base_mem)ᵒᵖ ⥤ Type u}
    (sX : X ⟶ D.space) (hX : D.IsGood sX) (sY : Y ⟶ D.space) (hY : D.IsGood sY)
    {f : X ⟶ Y} (hbase : f ≫ sY = sX) (hetale : IsEtale D.site D.base D.base_mem f)
    (hintY : IsIntegralSpace D.site D.base D.base_mem Y)
    (g : rationalFunctions D.site D.base D.base_mem hY.1) (hg : IsUnit g) {n : ℤ}
    (hnY : deltaDimensionClosed D sY hY Set.univ isClosed_univ = (n : EInt))
    (Z : IntegralClosedSubspace D.site D.base D.base_mem X) :
    (etalePullbackPrincipalDivisorCycleOfGood D sX hX sY hY hbase hetale hintY g hg
        (targetDivisorLocallyFinite_of_isGood D sY hY hintY g hg) hnY).1 Z =
      (etaleComponentDivisorData D sX hX sY hY f hbase hetale hintY n hnY g hg
        (componentDivisorLocallyFinite_of_isGood D sX hX sY hY hetale hintY g
          hg)).toEtaleComponentDivisorData.componentPushforwardCoeff Z
Sources

Section82.14 Principal divisors and pushforward#

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

Tag 0EQ4, a lemma

Tag 0EQ4 in the Stacks Project.

AlgebraicGeometry.Space.properPushforward_principalDivisorCycle_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardPrincipalDivisor.lean, line 403. The attribute's comment: “REDUCED, not proved: p_*div(f) = div(g) in Z_{n-1}(Y) IF AND ONLY IF it holds at every prime divisor of Y; proved away from them, using dim_δ(X) = dim_δ(Y). Take g to be rationalFunctionNorm, the norm Nm_{R(X)/R(Y)} constructed here, for the source's statement”.

Stacks 0EQ4, reduced to its coefficients at the prime divisors of Y. In Situation 0EDT let X/B and Y/B be good, let p : X ⟶ Y be quasi-compact over B, let X and Y be integral with dim_δ(X) = dim_δ(Y) = n, and let f ∈ R(X)^* and g ∈ R(Y)^*. Then

p_* div(f) = div(g) in Z_{n-1}(Y)

holds exactly when it holds coefficientwise at every prime divisor of Y, that is when

∑_Z ord_Z(f) · deg(Z/Z') = ord_{Z'}(g)

for every prime divisor Z' ⊆ Y, the sum being over the integral closed subspaces Z ⊆ X.

Both sides are coefficient families on the integral closed subspaces of Y, and away from the prime divisors of Y both vanish: the coefficient of div(g) at an integral closed subspace whose point set does not have codimension one is zero by Stacks 0ENP, and the pushforward has no contribution there by AlgebraicGeometry.Space.properPushforwardCoeff_principalDivisorCycleCoefficients_eq_zero, which is where the equality of the δ-dimensions is used. That is the whole content of the reduction; the coefficient identity at a prime divisor of Y — which is the mathematical content of Stacks 0EQ4 — is not proved here, and is not assumed either. Taking g = Nm_{R(X)/R(Y)}(f), that is AlgebraicGeometry.Space.rationalFunctionNorm D.site D.base D.base_mem … p hgen f, gives the source's statement.

theorem properPushforward_principalDivisorCycle_eq_iff
    (hfinX : LocallyFinite fun W : PrimeDivisor D.site D.base D.base_mem X =>
      if principalDivisorCoefficients D.site D.base D.base_mem hX.1 hdecX embX f hf W = 0 then ∅
      else W.support D.site D.base D.base_mem X)
    (hfinY : LocallyFinite fun W : PrimeDivisor D.site D.base D.base_mem Y =>
      if principalDivisorCoefficients D.site D.base D.base_mem hY.1 hdecY embY g hg W = 0 then ∅
      else W.support D.site D.base D.base_mem Y)
    {p : X ⟶ Y} (hpB : p ≫ sY = sX) (hp : IsQuasiCompact D.site D.base D.base_mem p) :
    properCyclePushforward D sX hX sY hY hpB hp (n - 1)
          (principalDivisorCycle D sX hX hdecX embX f hf hfinX hintX dX hdX hnX) =
        principalDivisorCycle D sY hY hdecY embY g hg hfinY hintY dY hdY hnY ↔
      ∀ W : PrimeDivisor D.site D.base D.base_mem Y,
        (∑ᶠ Z : IntegralClosedSubspace D.site D.base D.base_mem X,
            principalDivisorCycleCoefficients D sX hX hdecX embX f hf Z *
              properCycleMult D sX hX sY hY p Z
                (W.toIntegralClosedSubspace D.site D.base D.base_mem)) =
          principalDivisorCoefficients D.site D.base D.base_mem hY.1 hdecY embY g hg W

AlgebraicGeometry.Space.properCyclePushforward_rationalFunctionPrincipalDivisorCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardPrincipalDivisorCanonical.lean, line 642. The attribute's comment: “p_ div(f) = div(Nm_{R(X)/R(Y)}(f)) in Z_{n-1}(Y), for X/B, Y/B good and integral with dim_δ X = dim_δ Y = n, p : X → Y dominant and proper, f ∈ R(X)^; div is 0EQ1 at the canonical embeddings, p_* is 0EP2, the norm is constructed; nothing carried”.

Stacks 0EQ4. In Situation 0EDT let X/B and Y/B be good, let X and Y be integral with n = dim_δ(X) = dim_δ(Y), let p : X ⟶ Y be a dominant proper morphism, let f ∈ R(X)^* and set g = Nm_{R(X)/R(Y)}(f). Then

p_* div(f) = div(g) in Z_{n-1}(Y).

Here div is the principal divisor of Stacks 0EQ1 (AlgebraicGeometry.Space.rationalFunctionPrincipalDivisorCycle, at the canonical embeddings of Stacks 0ENK), p_* is proper pushforward of cycles (Stacks 0EP2) and g is the norm AlgebraicGeometry.Space.rationalFunctionNorm along the extension of function fields p induces, as a unit of R(Y) (AlgebraicGeometry.Space.rationalFunctionNormUnit); R(X)/R(Y) is finite (Stacks 0AD5, from dim_δ(X) = dim_δ(Y)). Both sides are (n-1)-cycles on Y, determined by their coefficients at the prime divisors of Y, where they agree by AlgebraicGeometry.Space.finsum_rationalFunctionPrincipalDivisorCycle_mul_properCycleMult_eq.

theorem properCyclePushforward_rationalFunctionPrincipalDivisorCycle {p : X ⟶ Y}
    (hpB : p ≫ sY = sX) (hproper : IsProper D.site D.base D.base_mem p)
    (hdom : IsDominant D.site D.base D.base_mem p) {n : ℤ}
    (hnX : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt))
    (hnY : deltaDimensionClosed D sY hY Set.univ isClosed_univ = (n : EInt))
    (f : (rationalFunctions D.site D.base D.base_mem hX.1)ˣ) :
    properCyclePushforward D sX hX sY hY hpB hproper.2.1.2 (n - 1)
        (rationalFunctionPrincipalDivisorCycle D sX hX hintX hnX f) =
      rationalFunctionPrincipalDivisorCycle D sY hY hintY hnY
        (rationalFunctionNormUnit D.site D.base D.base_mem hX.1 hY.1 hintX hintY p
          (pointsMap_genericPoint_of_isDominant D.site D.base D.base_mem hX.1 hY.1 hintX hintY
            p hdom) f)

Stacks.Norm.norm_baseChange_eq_prod_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Norm/BaseChangeProduct.lean, line 154. The attribute's comment: “the field-theoretic norm compatibility at the end of the proof, for which the source says 'we omit the proof': for L/K finite and M/K finite separable, M ⊗_K L = ∏ M_i and Nm_{L/K}(t) = ∏ Nm_{M_i/M}(t_i)”.

The field-theoretic step of Stacks 0EQ4, whose proof the source omits. Let K be a field, L/K a finite extension and M/K a finite separable extension. Then M ⊗_K L is a finite product of fields ∏ᵢ Mᵢ — concretely, the product of its quotients by its maximal ideals — and for t ∈ L the image in M of Nm_{L/K}(t) is the product of the norms over M of the images tᵢ of 1 ⊗ t:

Nm_{L/K}(t) = ∏ᵢ Nm_{Mᵢ/M}(tᵢ) in M.

Separability of M/K is what makes M ⊗_K L reduced, and being also finite-dimensional over M it is then the product of its residue fields. The identity itself is base change of the norm followed by multiplicativity over the factors.

theorem norm_baseChange_eq_prod_quotient {K L M : Type*} [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M] [FiniteDimensional K L] [FiniteDimensional K M]
    [Algebra.IsSeparable K M] [Fintype (MaximalSpectrum (M ⊗[K] L))] (t : L) :
    algebraMap K M (Algebra.norm K t) =
      ∏ p : MaximalSpectrum (M ⊗[K] L),
        Algebra.norm M (Ideal.Quotient.mk p.asIdeal (1 ⊗ₜ[K] t))
Sources

Section82.15 Rational equivalence#

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

Tag 0EQ6, a definition

Tag 0EQ6 in the Stacks Project.

AlgebraicGeometry.Space.cycleFamilySumCoeff_mem_cyclesOfDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ClosedSubspaceFamilySums.lean, line 185. The attribute's comment: “part (1)”.

Stacks 0EQ6, part (1). The coefficientwise sum ∑ (i_j)_* c_j of the pushforwards of a family of k-cycles along the inclusions of a locally finite collection of integral closed subspaces is a k-cycle on X.

Local finiteness of the collection gives local finiteness of the support: a neighbourhood of a point meeting only finitely many of the |W_j| is shrunk, using the pushforwards from those finitely many, to one meeting only finitely many point sets of subspaces with a nonzero coefficient. The δ-dimension of each such subspace is k because that holds for the summand it comes from.

theorem cycleFamilySumCoeff_mem_cyclesOfDimension (sX : X ⟶ D.space) (hX : D.IsGood sX)
    (W : J → IntegralClosedSubspace D.site D.base D.base_mem X)
    (hWfin : LocallyFinite fun j : J =>
      subspacePointSet D.site D.base D.base_mem X (W j).subspace)
    (k : ℤ) (c : ∀ j, CycleGroup D ((W j).subspace.ι ≫ sX) k) :
    cycleFamilySumCoeff D sX hX W k c ∈ cyclesOfDimension D sX k

AlgebraicGeometry.Space.cycleFamilySum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ClosedSubspaceFamilySums.lean, line 221. The attribute's comment: “part (1)”.

Stacks 0EQ6, part (1). The element ∑ (i_j)_* c_j of Z_k(X) determined by a locally finite collection {W_j ⊆ X} of integral closed subspaces and a family of k-cycles c_j on them; taking c_j = div(f_j) for f_j ∈ R(W_j)^* on subspaces of δ-dimension k + 1 gives the cycle of the source.

def cycleFamilySum (sX : X ⟶ D.space) (hX : D.IsGood sX)
    (W : J → IntegralClosedSubspace D.site D.base D.base_mem X)
    (hWfin : LocallyFinite fun j : J =>
      subspacePointSet D.site D.base D.base_mem X (W j).subspace)
    (k : ℤ) (c : ∀ j, CycleGroup D ((W j).subspace.ι ≫ sX) k) : CycleGroup D sX k

AlgebraicGeometry.Space.IsRationallyEquivalentToZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalence.lean, line 261. The attribute's comment: “part (2): rationally equivalent to zero. The sum is part (1), AlgebraicGeometry.Space.cycleFamilySum; the index type ranges over the universe v”.

Stacks 0EQ6, part (2). A k-cycle on a good algebraic space X/B is rationally equivalent to zero when it is the cycle ∑ (i_j)_* div(f_j) of part (1): there is a locally finite family {W_j ⊆ X} of integral closed subspaces with dim_δ(W_j) = k + 1, and on each a principal divisor div(f_j), f_j ∈ R(W_j)^*, whose pushforwards sum to the cycle.

The sum is AlgebraicGeometry.Space.cycleFamilySum, which is part (1) of the source.

def IsRationallyEquivalentToZero (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ)
    (α : CycleGroup D sX k) : Prop

AlgebraicGeometry.Space.rationalEquivalences, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalence.lean, line 336. The attribute's comment: “part (2): the cycles rationally equivalent to zero, as a subgroup of Z_k(X); the carrier is exactly the set of sums of part (1)”.

Stacks 0EQ6, part (2). The subgroup of k-cycles rationally equivalent to zero. Its carrier is exactly the set of cycles of the form ∑ (i_j)_* div(f_j) of part (1); that this set is a subgroup is the content of the three closure proofs.

def rationalEquivalences (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ) :
    AddSubgroup (CycleGroup D sX k)

AlgebraicGeometry.Space.RationallyEquivalent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalence.lean, line 354. The attribute's comment: “part (3): α ∼_rat β, defined as α - β being rationally equivalent to zero”.

Stacks 0EQ6, part (3). Two k-cycles are rationally equivalent when their difference is rationally equivalent to zero.

def RationallyEquivalent (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ)
    (α β : CycleGroup D sX k) : Prop

AlgebraicGeometry.Space.rationallyEquivalent_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalence.lean, line 364. The attribute's comment: “part (3): ∼_rat is an equivalence relation, from the subgroup property of the cycles rationally equivalent to zero”.

Stacks 0EQ6, part (3). Rational equivalence is an equivalence relation on Z_k(X): reflexivity, symmetry and transitivity are the three closure properties of the subgroup of cycles rationally equivalent to zero, applied to α - α = 0, β - α = -(α - β) and α - γ = (α - β) + (β - γ).

theorem rationallyEquivalent_equivalence (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ) :
    Equivalence (RationallyEquivalent.{v} D sX hX k)

AlgebraicGeometry.Space.chowGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalence.lean, line 394. The attribute's comment: “part (4): CH_k(X) = Z_k(X)/∼_rat, the quotient of Z_k(X) by the subgroup of cycles rationally equivalent to zero”.

Stacks 0EQ6, part (4). The Chow group of k-cycles on X, that is the Chow group of k-cycles modulo rational equivalence,

CH_k(X) = Z_k(X)/∼_rat,

the quotient of the group of k-cycles of a good algebraic space X/B by the subgroup of cycles rationally equivalent to zero.

abbrev chowGroup (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ)

AlgebraicGeometry.Space.chowClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalence.lean, line 399. The attribute's comment: “part (4): the class map Z_k(X) → CH_k(X) of the quotient by ∼_rat”.

Stacks 0EQ6, part (4). The class map Z_k(X) → CH_k(X), the quotient homomorphism.

def chowClass (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ) :
    CycleGroup D sX k →+ chowGroup.{v} D sX hX k

AlgebraicGeometry.Space.chowClass_cycleFamilySum_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalence.lean, line 426. The attribute's comment: “parts (2) and (4): the class map kills ∑ (i_j)_* div(f_j), the cycle of part (1); proved for the constructed CH_k(X), not assumed”.

Stacks 0EQ6, parts (2) and (4). The class in CH_k(X) of the cycle ∑ (i_j)_* div(f_j) of part (1) is zero: a sum of principal divisors on a locally finite family of integral closed subspaces of δ-dimension k + 1 is rationally equivalent to zero, hence dies in the quotient.

theorem chowClass_cycleFamilySum_eq_zero (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ)
    {J : Type v} (W : J → IntegralClosedSubspace D.site D.base D.base_mem X)
    (hWfin : LocallyFinite fun j : J =>
      subspacePointSet D.site D.base D.base_mem X (W j).subspace)
    (c : ∀ j, CycleGroup D ((W j).subspace.ι ≫ sX) k)
    (hWdim : ∀ j, deltaDimension D sX (W j) = k + 1)
    (hWprin : ∀ j, IsPrincipalDivisorCycle D ((W j).subspace.ι ≫ sX) k (c j)) :
    chowClass.{v} D sX hX k (cycleFamilySum D sX hX W hWfin k c) = 0

AlgebraicGeometry.Space.IsRationallyEquivalentToZeroCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalenceCanonical.lean, line 137. The attribute's comment: “part (2): rationally equivalent to zero, the summands being principal divisors at the canonical embeddings of Stacks 0ENK. The sum is part (1), AlgebraicGeometry.Space.cycleFamilySum; the index type ranges over the universe v”.

A k-cycle on a good algebraic space X/B is rationally equivalent to zero when it is the cycle ∑ (i_j)_* div(f_j) of part (1): there is a locally finite family {W_j ⊆ X} of integral closed subspaces with dim_δ(W_j) = k + 1, and on each a rational function f_j ∈ R(W_j)^* whose principal divisor div(f_j) is the j-th summand, the pushforwards summing to the cycle.

Each W_j is good over B by AlgebraicGeometry.Space.isGood_integralClosedSubspace and integral by definition, so div(f_j) is read at the canonical embeddings R(W_j) → Q(𝒪^h_{W_j,ξ}) of Stacks 0ENK and depends on nothing but f_j: the summand condition is AlgebraicGeometry.Space.IsPrincipalDivisorCycleOfGood. The sum is AlgebraicGeometry.Space.cycleFamilySum.

def IsRationallyEquivalentToZeroCanonical (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ)
    (α : CycleGroup D sX k) : Prop

AlgebraicGeometry.Space.rationalEquivalencesCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalenceCanonical.lean, line 211. The attribute's comment: “part (2): the cycles rationally equivalent to zero, as a subgroup of Z_k(X); the carrier is exactly the set of sums of part (1) with div(f) at the canonical embeddings”.

The subgroup of k-cycles rationally equivalent to zero. Its carrier is exactly the set of cycles of the form ∑ (i_j)_* div(f_j), the principal divisors being read at the canonical embeddings of Stacks 0ENK.

def rationalEquivalencesCanonical (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ) :
    AddSubgroup (CycleGroup D sX k)

AlgebraicGeometry.Space.RationallyEquivalentCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalenceCanonical.lean, line 231. The attribute's comment: “part (3): α ∼_rat β, defined as α - β being rationally equivalent to zero, for the reading of part (2) at the canonical embeddings”.

Two k-cycles are rationally equivalent when their difference is rationally equivalent to zero.

def RationallyEquivalentCanonical (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ)
    (α β : CycleGroup D sX k) : Prop

AlgebraicGeometry.Space.rationallyEquivalentCanonical_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalenceCanonical.lean, line 238. The attribute's comment: “part (3): ∼_rat is an equivalence relation, from the subgroup property of the cycles rationally equivalent to zero”.

Rational equivalence is an equivalence relation on Z_k(X).

theorem rationallyEquivalentCanonical_equivalence (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ) :
    Equivalence (RationallyEquivalentCanonical.{v} D sX hX k)

AlgebraicGeometry.Space.chowGroupCanonical, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalenceCanonical.lean, line 268. The attribute's comment: “part (4): CH_k(X) = Z_k(X)/∼_rat, the quotient of Z_k(X) by the subgroup of cycles rationally equivalent to zero”.

The Chow group of k-cycles on X, that is the group of k-cycles modulo rational equivalence,

CH_k(X) = Z_k(X)/∼_rat,

the quotient of the group of k-cycles of a good algebraic space X/B by the subgroup of cycles rationally equivalent to zero.

abbrev chowGroupCanonical (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ)

AlgebraicGeometry.Space.chowClassCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalenceCanonical.lean, line 273. The attribute's comment: “part (4): the class map Z_k(X) → CH_k(X) of the quotient by ∼_rat”.

The class map Z_k(X) → CH_k(X), the quotient homomorphism.

def chowClassCanonical (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ) :
    CycleGroup D sX k →+ chowGroupCanonical.{v} D sX hX k

AlgebraicGeometry.Space.chowClassCanonical_cycleFamilySum_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RationalEquivalenceCanonical.lean, line 297. The attribute's comment: “parts (2) and (4): the class map kills ∑ (i_j)_* div(f_j), the cycle of part (1); proved for the constructed CH_k(X), not assumed”.

The class in CH_k(X) of the cycle ∑ (i_j)_* div(f_j), a sum of principal divisors on a locally finite family of integral closed subspaces of δ-dimension k + 1, is zero.

theorem chowClassCanonical_cycleFamilySum_eq_zero (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ)
    {J : Type v} (W : J → IntegralClosedSubspace D.site D.base D.base_mem X)
    (hWfin : LocallyFinite fun j : J =>
      subspacePointSet D.site D.base D.base_mem X (W j).subspace)
    (c : ∀ j, CycleGroup D ((W j).subspace.ι ≫ sX) k)
    (hWdim : ∀ j, deltaDimension D sX (W j) = k + 1)
    (hWprin : ∀ j, IsPrincipalDivisorCycleOfGood D ((W j).subspace.ι ≫ sX)
      (isGood_integralClosedSubspace D sX hX (W j)) (W j).isIntegralSpace k (c j)) :
    chowClassCanonical.{v} D sX hX k (cycleFamilySum D sX hX W hWfin k c) = 0
Tag 0EQ7, a lemma

Tag 0EQ7 in the Stacks Project.

AlgebraicGeometry.Space.chowGroup_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ChowLocalizationSequence.lean, line 542.

In Situation 0EDT let X/B be good, let U ⊆ X be an open subspace, let Y ⊆ X be a closed subspace with |Y| = |X| \ |U| and let i : Y → X, j : U → X be the inclusions. Let k ∈ ℤ.

  1. If α, β ∈ Z_k(X) satisfy α|_U ∼_rat β|_U, then α ∼_rat β + i_*γ for some γ ∈ Z_k(Y).
  2. In other words, CH_k(Y) →[i_*] CH_k(X) →[j^*] CH_k(U) → 0 is an exact complex of abelian groups: the kernel of j^* is the image of i_*, and j^* is surjective.
theorem chowGroup_localization
    (hcomplement : Set.range (pointsMap D.site D.base D.base_mem Y.toFunctor Y.ι) =
      (Set.range (pointsMap D.site D.base D.base_mem U.toFunctor U.ι))ᶜ) (k : ℤ) :
    (∀ α β : CycleGroup D sX k,
      RationallyEquivalent.{v} D (U.ι ≫ sX) (isGood_ι_of_isOpenSubspace D sX hX U hU) k
        (cycleGroupRestrict D sX hX (U.ι ≫ sX) (isGood_ι_of_isOpenSubspace D sX hX U hU) hU.2
          rfl k α)
        (cycleGroupRestrict D sX hX (U.ι ≫ sX) (isGood_ι_of_isOpenSubspace D sX hX U hU) hU.2
          rfl k β) →
      ∃ γ : CycleGroup D (Y.ι ≫ sX) k,
        RationallyEquivalent.{v} D sX hX k α
          (β + cycleGroupClosedPushforward D hX.1 hY.1 (D.isDecentSpace_of_isGood sX hX) hY.2
            sX hX.2.2 (Y.ι ≫ sX) rfl k γ)) ∧
      Function.Exact (chowGroupClosedPushforward.{v} D sX hX Y hY k)
        (chowGroupRestrict.{v} D sX hX U hU k) ∧
      Function.Surjective (chowGroupRestrict.{v} D sX hX U hU k)
Tag 0EQ8, a remark

Tag 0EQ8 in the Stacks Project.

AlgebraicGeometry.Space.rationallyEquivalent_locallyFiniteCycleSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/InfiniteSumsRationalEquivalence.lean, line 182. The attribute's comment: “the remark in full: for alpha_i, beta_i supported on a locally finite family T_i with alpha_i ~rat beta_i on T_i, the sums are k-cycles and are rationally equivalent, the combined witnessing family being locally finite”.

Stacks 0EQ8. Let {T_i}_{i ∈ I} be a locally finite collection of subsets of |X| and let α_i, β_i ∈ Z_k(X) be supported on T_i. If α_i ∼_rat β_i on T_i for every i, then ∑ α_i ∼_rat ∑ β_i: the combined family {W_{i, j}}_{i ∈ I, j ∈ J_i} of witnessing subspaces is locally finite, so it is a single rational equivalence between the two sums.

theorem rationallyEquivalent_locallyFiniteCycleSum (sX : X ⟶ D.space) (hX : D.IsGood sX) (k : ℤ)
    (T : I → Set (points D.site D.base D.base_mem X)) (hT : LocallyFinite T)
    (α β : I → CycleGroup D sX k)
    (hαT : ∀ (i : I) (Z : IntegralClosedSubspace D.site D.base D.base_mem X),
      (α i).1 Z ≠ 0 → subspacePointSet D.site D.base D.base_mem X Z.subspace ⊆ T i)
    (hβT : ∀ (i : I) (Z : IntegralClosedSubspace D.site D.base D.base_mem X),
      (β i).1 Z ≠ 0 → subspacePointSet D.site D.base D.base_mem X Z.subspace ⊆ T i)
    (hαβ : ∀ i, RationallyEquivalentOn.{v} D sX hX k (T i) (α i) (β i)) :
    RationallyEquivalent.{v} D sX hX k (locallyFiniteCycleSum D sX k T hT α hαT)
      (locallyFiniteCycleSum D sX k T hT β hβT)

locallyFinite_sigma_of_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/LocallyFinite/Sigma.lean, line 42. The attribute's comment: “local finiteness of the combined family”.

Let T : I → Set Y be a locally finite collection of subsets of a topological space and, for each i, let W i : J i → Set Y be a locally finite collection with W i j ⊆ T i for all j. Then the combined collection fun ij : Σ i, J i ↦ W ij.1 ij.2 is locally finite.

theorem locallyFinite_sigma_of_subset {Y : Type u} [TopologicalSpace Y] {I : Type v}
    {J : I → Type w} {T : I → Set Y} (hT : LocallyFinite T) {W : ∀ i, J i → Set Y}
    (hW : ∀ i, LocallyFinite (W i)) (hWT : ∀ i j, W i j ⊆ T i) :
    LocallyFinite fun ij : Σ i, J i ↦ W ij.1 ij.2
Sources

Section82.16 Rational equivalence and push and pull#

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

Tag 0EQA, a lemma

Tag 0EQA in the Stacks Project.

AlgebraicGeometry.Space.PrimeDivisor.ord_eq_multiplicity_mul_ord, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullbackOrderOfVanishing.lean, line 375. The attribute's comment: “coefficientwise at a prime divisor Z of X with generic point ξ lying over a prime divisor Z' of Y with generic point ξ': the order of vanishing of a rational function pulls back with the multiplicity, ord_Z(g ∘ f) = m · ord_{Z'}(g), where m is the colength of the extended maximal ideal — the multiplicity with which Z occurs in the closed subspace f^{-1}(Z'), hence the coefficient the flat pullback of Stacks 0EP8 attaches to Z. PROVED, not assumed: that the order of vanishing multiplies by the multiplicity, from Stacks 02M1 (length_baseChange_eq_length_mul_length_quotient) applied to the cyclic modules O^h/a and O^h/b, which is how Stacks 02M1 computes with a multiplicity. For X integral this is the source's identity f^ div_Y(g) = ∑ m_{X',X} (X' → X)_ div_{X'}(g ∘ f|_{X'}) read at the coefficient of Z, the one component having multiplicity one; the statement is coefficientwise because neither side exists in this repository — the flat pullback of cycles is Stacks 0EP8 and the principal divisor div(g) is Stacks 0ENP — and for that same reason Stacks 0EPT and 0EPV are already carried coefficientwise here. NOT COVERED: for X with several irreducible components, the step from this identity to the cycle identity, namely the additivity over the components of the multiplicities of Stacks 0EE2 and Stacks 0EE9; the statement applies to X and to each component X' separately, with m read in each, but no additivity of those multiplicities is proved in this repository. RESTRICTED: carried as explicit named hypotheses are (i) the flat local homomorphism φ of the henselian local rings at the generic points, the map of henselian local rings induced by a morphism of decent algebraic spaces not being available here, with its locality and flatness as the hypotheses hloc and hflat; (ii) the embeddings R(Y) → Q(O^h_{Y,ξ'}) and R(X) → Q(O^h_{X,ξ}) of Stacks 0ENK as embY and embX, exactly as Stacks 0EPT carries them; (iii) the composite g ∘ f|_X as the parameter gf together with hgf, that its ratio at ξ is the image under φ of the ratio of g at ξ' — this repository has no pullback of a rational function along a morphism of algebraic spaces, only the chartwise fraction rule a/b ↦ f-sharp a / f-sharp b of Stacks 0ENC, which is what hgf states; and (iv) finiteness of the multiplicity, as hm naming the natural number m it equals. Locality, Noetherianness and the dimension bound on the henselian local rings are instance arguments, as they are for PrimeDivisor.ord and orderOfVanishingSection themselves”.

Stacks 0EQA, coefficientwise. The order of vanishing of a rational function pulls back with multiplicities. Let f : X ⟶ Y be flat, let Z' ⊆ Y and Z ⊆ X be prime divisors with Z lying over Z', let φ : 𝒪^h_{Y,ξ'} ⟶ 𝒪^h_{X,ξ} be the induced flat local homomorphism and let m be the multiplicity of Z over Z'. For a rational function g on Y whose ratio at ξ' is a / b with a and b nonzerodivisors, and for the composite g ∘ f|_X, whose ratio at ξ is therefore φ(a) / φ(b),

ord_Z(g ∘ f|_X) = m · ord_{Z'}(g).

The multiplicity m is the one with which Z occurs in f^{-1}(Z'), so for X integral this is the source's identity f^* div_Y(g) = ∑ m_{X',X} (X' ⟶ X)_* div_{X'}(g ∘ f|_{X'}) read at the coefficient of Z; for X with several components it is each of the two readings of that identity, as the implementation notes explain.

Nothing about the conclusion is assumed. The multiplicity enters as the colength hm and the whole content — that the order of vanishing multiplies by it — is Ring.ord_map_of_flatHom, which is Stacks 02M1 applied to 𝒪^h_{Y,ξ'} / a and to 𝒪^h_{Y,ξ'} / b.

theorem PrimeDivisor.ord_eq_multiplicity_mul_ord
    (hloc : IsLocalHom φ) (hflat : φ.Flat) {m : ℕ}
    (hm : primeDivisorFlatMultiplicity B S hS hX hdecX ZX hY hdecY ZY φ = (m : ℕ∞))
    (embY : rationalFunctions B S hS hY →+* ZY.genericTotalFractionRing B S hS hY hdecY)
    (embX : rationalFunctions B S hS hX →+* ZX.genericTotalFractionRing B S hS hX hdecX)
    (g : rationalFunctions B S hS hY) (gf : rationalFunctions B S hS hX)
    (a b : nonZeroDivisors ↥(ZY.genericHenselianLocalRing B S hS hY hdecY))
    (hg : embY g = IsLocalization.mk' (ZY.genericTotalFractionRing B S hS hY hdecY)
      (a : ↥(ZY.genericHenselianLocalRing B S hS hY hdecY)) b)
    (hgf : embX gf = IsLocalization.mk' (ZX.genericTotalFractionRing B S hS hX hdecX)
      (φ (a : ↥(ZY.genericHenselianLocalRing B S hS hY hdecY)))
      (⟨φ (b : ↥(ZY.genericHenselianLocalRing B S hS hY hdecY)),
        Ring.map_mem_nonZeroDivisors_of_flatHom hflat b.2⟩ :
        nonZeroDivisors ↥(ZX.genericHenselianLocalRing B S hS hX hdecX)))
    (hgu : IsUnit (embY g)) (hgfu : IsUnit (embX gf)) :
    ZX.ord B S hS hX hdecX (embX gf) hgfu =
      (m : ℤ) * ZY.ord B S hS hY hdecY (embY g) hgu

AlgebraicGeometry.Space.flatPullbackMap_rationalFunctionPrincipalDivisorCycle_eq_finsum_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullbackPrincipalDivisorComponents.lean, line 719. The attribute's comment: “the displayed identity of (k + r - 1)-cycles on X, at every integral closed subspace of X; the sum is over the irreducible components X' of X (a locally finite family), m_{X',X} is the length of O_X at the generic point of X' (0EE9 part (1) for the space X), g ∘ f|_{X'} is the image of g under the extension of function fields of the dominant f|_{X'} (0EML), and every cycle is the one of this chapter: f^ is 0EP8, div is 0EQ1 at the canonical embeddings of 0ENK, (X' → X)_ is 0EP1”.

Stacks 0EQA. Flat pullback of a principal divisor. In Situation 0EDT let X, Y/B be good, assume Y integral with dim_δ(Y) = k, and let f : X ⟶ Y be a flat morphism over B of relative dimension r. Then for g ∈ R(Y)^*

f^* div_Y(g) = ∑_{X'} m_{X', X} (X' → X)_* div_{X'}(g ∘ f|_{X'})

as (k + r - 1)-cycles on X: at every integral closed subspace Z ⊆ X the coefficient of the flat pullback (Stacks 0EP8) of div_Y(g) (Stacks 0EQ1) is the sum over the irreducible components X' of X of m_{X', X}, the multiplicity of X' in X (Stacks 0EE9), times the coefficient at Z of the pushforward along X' → X (Stacks 0EP1) of the principal divisor of g ∘ f|_{X'} ∈ R(X')^*. The sum is a locally finite one, which is why the identity of cycles is stated at each coefficient.

theorem flatPullbackMap_rationalFunctionPrincipalDivisorCycle_eq_finsum_components {k : ℤ}
    (hk : deltaDimensionClosed D sY hY Set.univ isClosed_univ = (k : EInt))
    (g : (rationalFunctions D.site D.base D.base_mem hY.1)ˣ)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem X) :
    (flatPullbackMap D sX hX sY hY f hbase r hflat hr (k - 1) (k + r - 1) (by ring)
        (rationalFunctionPrincipalDivisorCycle D sY hY hintY hk g)).1 Z =
      ∑ᶠ W : IrreducibleComponentSubspace D.site D.base D.base_mem hX.1,
        spaceMultiplicity D X hX.1 W.1 *
          (W.flatPullbackDivisorPushforward D sX hX sY hY f hbase r hr hflat hintY hk g).1 Z
Tag 0EQB, a lemma

Tag 0EQB in the Stacks Project.

AlgebraicGeometry.Space.rationallyEquivalentCanonical_flatPullbackMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullbackRationalEquivalenceCanonical.lean, line 466. The attribute's comment: “f^α ∼_rat f^β in Z_{m+r}(X) for α ∼_rat β in Z_m(Y), f flat of relative dimension r between good spaces over B; rational equivalence at the canonical embeddings of 0ENK, the presenting family on X indexed in max v (u+1) when the one on Y is indexed in v”.

In Situation 0EDT let X, Y/B be good and let f : X ⟶ Y be a morphism over B which is flat of relative dimension r. If α ∼_rat β are rationally equivalent m-cycles on Y, then f^*α ∼_rat f^*β as n-cycles on X, where m + r = n.

Rational equivalence is that of Stacks 0EQ6 with div(g) read at the canonical embeddings of Stacks 0ENK (AlgebraicGeometry.Space.RationallyEquivalentCanonical), and f^* is the flat pullback of cycles of Stacks 0EP8 (AlgebraicGeometry.Space.flatPullbackMap). The family presenting α - β is indexed in a universe v, the one presenting f^*α - f^*β in max v (u + 1).

theorem rationallyEquivalentCanonical_flatPullbackMap (m n : ℤ) (hmn : m + (r : ℤ) = n)
    {α β : CycleGroup D sY m} (h : RationallyEquivalentCanonical.{v} D sY hY m α β) :
    RationallyEquivalentCanonical.{max v (u + 1)} D sX hX n
      (flatPullbackMap D sX hX sY hY f hbase r hflat hr m n hmn α)
      (flatPullbackMap D sX hX sY hY f hbase r hflat hr m n hmn β)
Tag 0EQC, a lemma

Tag 0EQC in the Stacks Project.

AlgebraicGeometry.Space.rationallyEquivalentCanonical_properCyclePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardRationalEquivalence.lean, line 708.

Stacks 0EQC. In Situation 0EDT let X/B and Y/B be good and let p : X ⟶ Y be a proper morphism over the base. If α, β ∈ Z_k(X) are rationally equivalent, then p_*α is rationally equivalent to p_*β.

Rational equivalence is that of Stacks 0EQ6 with the summands div(f_j) read at the canonical embeddings R(W_j) → Q(𝒪^h_{W_j,ξ}) of Stacks 0ENK (AlgebraicGeometry.Space.RationallyEquivalentCanonical), and p_* is the proper pushforward of cycles of Stacks 0EP1.

theorem rationallyEquivalentCanonical_properCyclePushforward (sX : X ⟶ D.space)
    (hX : D.IsGood sX) (sY : Y ⟶ D.space) (hY : D.IsGood sY) {p : X ⟶ Y} (hpB : p ≫ sY = sX)
    (hp : IsProper D.site D.base D.base_mem p) (k : ℤ) {α β : CycleGroup D sX k}
    (h : RationallyEquivalentCanonical.{v} D sX hX k α β) :
    RationallyEquivalentCanonical.{v} D sY hY k
      (properCyclePushforward D sX hX sY hY hpB hp.2.1.2 k α)
      (properCyclePushforward D sX hX sY hY hpB hp.2.1.2 k β)
Sources

Section82.17 The divisor associated to an invertible sheaf#

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

Tag 0EQE, a definition

Tag 0EQE in the Stacks Project.

AlgebraicGeometry.Space.divisorCycleOfSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/InvertibleSheafDivisor.lean, line 339. The attribute's comment: “part (1): div_ℒ(s) = ∑ ord_{Z,ℒ}(s) [Z] as an element of Z_{n-1}(X); the δ-dimension of a prime divisor is n-1 by Stacks 0EPZ, whose dimension-function hypotheses d and hd are Stacks 0EDN, carried; local finiteness of the prime divisors with ord ≠ 0 is Stacks 0EPS, the hypothesis hfin; the ratio family at the generic points is the parameter ratio, as in Stacks 0EPR and 0EPU”.

Stacks 0EQE, part (1). The Weil divisor associated to a nonzero meromorphic section s of ℒ, that is div_ℒ(s) = ∑_Z ord_{Z,ℒ}(s) [Z] of Stacks 0EPU, as an element of Z_{n-1}(X): it is an (n-1)-cycle because a prime divisor of an integral good algebraic space of δ-dimension n has δ-dimension n - 1 by Stacks 0EPZ.

Local finiteness of the prime divisors with ord_{Z,ℒ}(s) ≠ 0 is Stacks 0EPS, here the hypothesis hfin; AlgebraicGeometry.Space.divisorCycleOfSectionOfGenerating discharges it from a nonempty open subspace over which s generates ℒ.

def divisorCycleOfSection (s : MeromorphicSection.{u, z} D.site D.base D.base_mem X hX.1 L)
    (ratio : LocalRatioFamily.{u, z} D.site D.base D.base_mem hX.1 hdec L)
    (hfin : LocallyFinite fun W : PrimeDivisor D.site D.base D.base_mem X =>
      if divisorCoefficients.{u, z} D.site D.base D.base_mem hX.1 hdec L s ratio W = 0 then ∅
      else W.support D.site D.base D.base_mem X)
    (hint : IsIntegralSpace D.site D.base D.base_mem X)
    (d : DimensionFunction (points D.site D.base D.base_mem X))
    (hd : ∀ x, d x = D.deltaValue sX x) {n : ℤ}
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt)) :
    CycleGroup D sX (n - 1)

AlgebraicGeometry.Space.divisorCycleOfSectionOfGenerating, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/InvertibleSheafDivisor.lean, line 377. The attribute's comment: “part (1): div_ℒ(s) in Z_{n-1}(X), with local finiteness supplied by Stacks 0EPS from the open subspace U over which s generates ℒ; the δ-dimension of a prime divisor is n-1 by Stacks 0EPZ, whose dimension-function hypotheses d and hd are Stacks 0EDN, carried”.

Stacks 0EQE, part (1). The Weil divisor div_ℒ(s) = ∑_Z ord_{Z,ℒ}(s) [Z] of a nonzero meromorphic section s of ℒ as an element of Z_{n-1}(X), with the local finiteness of its support supplied by Stacks 0EPS from a nonempty open subset of |X| containing the generic point of no prime divisor along which s has nonzero order — the open subspace over which s generates ℒ.

def divisorCycleOfSectionOfGenerating
    (hN : HasEtaleLocalProperty D.site D.base D.base_mem X
      (fun Y : Scheme.{u} => IsLocallyNoetherian Y))
    (s : MeromorphicSection.{u, z} D.site D.base D.base_mem X hX.1 L)
    (ratio : LocalRatioFamily.{u, z} D.site D.base D.base_mem hX.1 hdec L)
    (U : Set (points D.site D.base D.base_mem X)) (hUopen : IsOpen U) (hUne : U.Nonempty)
    (hgen : ∀ W : PrimeDivisor D.site D.base D.base_mem X,
      divisorCoefficients.{u, z} D.site D.base D.base_mem hX.1 hdec L s ratio W ≠ 0 →
        W.genericPoint D.site D.base D.base_mem X ∈ Uᶜ)
    (hint : IsIntegralSpace D.site D.base D.base_mem X)
    (d : DimensionFunction (points D.site D.base D.base_mem X))
    (hd : ∀ x, d x = D.deltaValue sX x) {n : ℤ}
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt)) :
    CycleGroup D sX (n - 1)

AlgebraicGeometry.Space.firstChernClassCapFundamental, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/InvertibleSheafDivisor.lean, line 463. The attribute's comment: “part (2): c₁(ℒ) ∩ [X] = class of div_ℒ(s) in CH_{n-1}(X); CH_{n-1}(X) together with its class map and its principal divisors is carried as the ChowTarget parameter chow, standing in for Stacks 0EQ6 parts (2)-(4); independence of the chosen section s is firstChernClassCapFundamental_eq”.

Stacks 0EQE, part (2). The Weil divisor associated to ℒ, that is c₁(ℒ) ∩ [X] = [div_ℒ(s)] ∈ CH_{n-1}(X), the class of the Weil divisor of a nonzero meromorphic section s of ℒ.

The class is independent of the chosen section: AlgebraicGeometry.Space.firstChernClassCapFundamental_eq. The Chow group CH_{n-1}(X) is the parameter chow, only part (1) of Stacks 0EQ6 being available in this library.

def firstChernClassCapFundamental
    (chow : ChowTarget.{u, w, v} D sX hX (n - 1) CH)
    (s : MeromorphicSection.{u, z} D.site D.base D.base_mem X hX.1 L)
    (ratio : LocalRatioFamily.{u, z} D.site D.base D.base_mem hX.1 hdec L)
    (hfin : LocallyFinite fun W : PrimeDivisor D.site D.base D.base_mem X =>
      if divisorCoefficients.{u, z} D.site D.base D.base_mem hX.1 hdec L s ratio W = 0 then ∅
      else W.support D.site D.base D.base_mem X)
    (hint : IsIntegralSpace D.site D.base D.base_mem X)
    (d : DimensionFunction (points D.site D.base D.base_mem X))
    (hd : ∀ x, d x = D.deltaValue sX x)
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt)) : CH

AlgebraicGeometry.Space.firstChernClassCapFundamental_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/InvertibleSheafDivisor.lean, line 490. The attribute's comment: “part (2), well-definedness: c₁(ℒ) ∩ [X] is independent of the chosen nonzero meromorphic section, by Stacks 0EPT; the principal divisor div(f) of Stacks 0ENP is not carried here, so that the cycle div(f) belongs to the principal divisors of the ChowTarget parameter — the input of Stacks 0EQ6 part (1) — is the hypothesis hprincipal, and Stacks 0EQ6 parts (2) and (4) are the parameter's field cls_cycleFamilySum_eq_zero”.

Stacks 0EQE, part (2), well-definedness. The class c₁(ℒ) ∩ [X] does not depend on the chosen nonzero meromorphic section of ℒ.

If the ratios of s and s' at the generic points of the prime divisors differ by the image of a rational function f, then div_ℒ(s) - div_ℒ(s') = div(f) by Stacks 0EPT, and div(f) is rationally equivalent to zero by Stacks 0EQ6: it is the one-member family ∑ (i_j)_* div(f_j) of part (1), taken on X itself. That div(f) is one of the principal divisors of the Chow group parameter is the hypothesis hprincipal, the principal divisor of Stacks 0ENP not being available in this library.

theorem firstChernClassCapFundamental_eq
    (chow : ChowTarget.{u, w, v} D sX hX (n - 1) CH)
    (s s' : MeromorphicSection.{u, z} D.site D.base D.base_mem X hX.1 L)
    (ratio : LocalRatioFamily.{u, z} D.site D.base D.base_mem hX.1 hdec L)
    (hfin : LocallyFinite fun W : PrimeDivisor D.site D.base D.base_mem X =>
      if divisorCoefficients.{u, z} D.site D.base D.base_mem hX.1 hdec L s ratio W = 0 then ∅
      else W.support D.site D.base D.base_mem X)
    (hfin' : LocallyFinite fun W : PrimeDivisor D.site D.base D.base_mem X =>
      if divisorCoefficients.{u, z} D.site D.base D.base_mem hX.1 hdec L s' ratio W = 0 then ∅
      else W.support D.site D.base D.base_mem X)
    (hint : IsIntegralSpace D.site D.base D.base_mem X)
    (d : DimensionFunction (points D.site D.base D.base_mem X))
    (hd : ∀ x, d x = D.deltaValue sX x)
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt))
    (emb : ∀ W : PrimeDivisor D.site D.base D.base_mem X,
      rationalFunctions D.site D.base D.base_mem hX.1 →+*
        W.genericTotalFractionRing D.site D.base D.base_mem hX.1 hdec)
    (f : rationalFunctions D.site D.base D.base_mem hX.1)
    (hf : ∀ W : PrimeDivisor D.site D.base D.base_mem X, IsUnit (emb W f))
    (hratio : ∀ W : PrimeDivisor D.site D.base D.base_mem X,
      ((ratio W s : W.genericTotalFractionRing D.site D.base D.base_mem hX.1 hdec)) =
        emb W f * (ratio W s' : W.genericTotalFractionRing D.site D.base D.base_mem hX.1 hdec))
    (hprincipal : ∃ (Y : IntegralClosedSubspace D.site D.base D.base_mem X)
      (c : CycleGroup D (Y.subspace.ι ≫ sX) (n - 1)), c ∈ chow.principalDivisors Y ∧
        ∀ Z : IntegralClosedSubspace D.site D.base D.base_mem X,
          (integralClosedSubspacePushforward D sX hX Y (n - 1) c).1 Z =
            principalDivisorCycleCoefficients D sX hX hdec emb f hf Z) :
    firstChernClassCapFundamental D sX hX hdec L chow s ratio hfin hint d hd hn =
      firstChernClassCapFundamental D sX hX hdec L chow s' ratio hfin' hint d hd hn

AlgebraicGeometry.Space.sectionWeilDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/WeilDivisorOfInvertibleSheaf.lean, line 148. The attribute's comment: “part (1): div_ℒ(s) = ∑ ord_{Z,ℒ}(s) [Z] as an element of Z_{n-1}(X), for X/B good and integral with n = dim_δ(X), ℒ invertible and s a nonzero meromorphic section; ord_{Z,ℒ}(s) at the generators of Stacks 0EPR, local finiteness by Stacks 0EPS for the section s, the δ-dimension n-1 of a prime divisor by Stacks 0EPZ with the dimension function of Stacks 0EDN, and the properties of the henselian local rings by Stacks 0ENK, all proved”.

Stacks 0EQE, part (1). In Situation 0EDT let X/B be good, let X be integral with n = dim_δ(X) and let ℒ be an invertible 𝒪_X-module. The Weil divisor associated to a nonzero meromorphic section s of ℒ, the (n-1)-cycle

div_ℒ(s) = ∑ ord_{Z,ℒ}(s) [Z] ∈ Z_{n-1}(X),

the sum over the prime divisors Z of X, ord_{Z,ℒ}(s) being the order of vanishing of Stacks 0EPR (AlgebraicGeometry.Space.sectionWeilDivisor_apply_toIntegralClosedSubspace).

def sectionWeilDivisor {n : ℤ}
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt))
    (s : MeromorphicSection.{u, u} D.site D.base D.base_mem X hX.1 L)
    (hs : s ≠ 0) :
    CycleGroup D sX (n - 1)

AlgebraicGeometry.Space.weilDivisorOfInvertibleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/WeilDivisorOfInvertibleSheaf.lean, line 234. The attribute's comment: “part (2): c₁(ℒ) ∩ [X] = the class of div_ℒ(s) in CH_{n-1}(X) = Z_{n-1}(X)/∼_rat (Stacks 0EQ6), for a nonzero meromorphic section s of ℒ, which exists by Stacks 0EPQ; it is the class of div_ℒ(s) for every nonzero s by chowClass_sectionWeilDivisor”.

Stacks 0EQE, part (2). In Situation 0EDT let X/B be good, let X be integral with n = dim_δ(X) and let ℒ be an invertible 𝒪_X-module. The Weil divisor associated to ℒ,

c₁(ℒ) ∩ [X] = class of div_ℒ(s) ∈ CH_{n-1}(X),

for the nonzero meromorphic section s of ℒ of Stacks 0EPQ (AlgebraicGeometry.Space.regularMeromorphicSection); the class does not depend on the choice of s (AlgebraicGeometry.Space.chowClass_sectionWeilDivisor).

def weilDivisorOfInvertibleSheaf {n : ℤ}
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt)) :
    chowGroup.{v} D sX hX (n - 1)

AlgebraicGeometry.Space.chowClass_sectionWeilDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/WeilDivisorOfInvertibleSheaf.lean, line 254. The attribute's comment: “part (2), well-definedness: the class of div_ℒ(s) in CH_{n-1}(X) is c₁(ℒ) ∩ [X] for every nonzero meromorphic section s, by Stacks 0EPT, the principal divisor div(f) of the ratio being rationally equivalent to zero in the sense of Stacks 0EQ6”.

Stacks 0EQE, part (2), well-definedness. c₁(ℒ) ∩ [X] is the class of div_ℒ(s) in CH_{n-1}(X) for every nonzero meromorphic section s of ℒ.

theorem chowClass_sectionWeilDivisor {n : ℤ}
    (hn : deltaDimensionClosed D sX hX Set.univ isClosed_univ = (n : EInt))
    (s : MeromorphicSection.{u, u} D.site D.base D.base_mem X hX.1 L)
    (hs : s ≠ 0) :
    chowClass.{v} D sX hX (n - 1) (sectionWeilDivisor D sX hX hint L hL hn s hs) =
      weilDivisorOfInvertibleSheaf.{v} D sX hX hint L hL hn
Tag 0EQF, a lemma

Tag 0EQF in the Stacks Project.

AlgebraicGeometry.Space.zeroSchemeCycleCoeff_mem_cyclesOfDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/DivisorOfSectionCycle.lean, line 201. The attribute's comment: “[Z(s)]_k is a k-cycle, so that at k = n - 1 the right side of both identities is an element of Z_{n-1}(X); the multiplicity of Stacks 0EE9 is read at the chosen geometric representative γ, which by Stacks 0EE1 (geometricLength_eq_of_image_eq) does not change its value, and local finiteness of the coefficient family is the argument hfin, a property of the input datum (ℒ, s, γ), as it is for div_ℒ(s) in Stacks 0EQE part (1) and for divisorOfSection in Stacks 0EPU part (1)”.

Stacks 0EQF. The right side of both identities of the source is a k-cycle: the coefficient family of [Z(s)]_k lies in Z_k(X).

The δ-dimension clause holds by construction, the coefficient of Stacks 0EE9 at an integral closed subspace of δ-dimension other than k being zero. Local finiteness is the argument hfin, a property of the input datum (ℒ, s, γ), as it is for div_ℒ(s) on the other side.

theorem zeroSchemeCycleCoeff_mem_cyclesOfDimension
    (hfin : LocallyFinite fun Z : IntegralClosedSubspace D.site D.base D.base_mem X =>
      if zeroSchemeCycleCoeff D sX hX L s k γ Z = 0 then ∅
      else subspacePointSet D.site D.base D.base_mem X Z.subspace) :
    zeroSchemeCycleCoeff D sX hX L s k γ ∈ cyclesOfDimension D sX k

AlgebraicGeometry.Space.divisorCycleOfSection_eq_zeroSchemeCycle_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/DivisorOfSectionCycle.lean, line 281. The attribute's comment: “first conclusion REDUCED to its coefficients: div_ℒ(s) = [Z(s)]_{n-1} in Z_{n-1}(X) holds IF AND ONLY IF it holds at every prime divisor, where div_ℒ(s) is Stacks 0EQE part (1) and [Z(s)]_{n-1} is Stacks 0EE9 at the chosen geometric representative γ; what is proved here is that the two coefficient families agree away from the prime divisors, by Stacks 0EQE part (1) and Stacks 0EPZ. The coefficient identity ord_{Z,ℒ}(s) = m_{Z,Z(s)} AT a prime divisor — the right-hand side of this equivalence — is proved separately, in GlobalSectionDivisorCycle.lean, for the canonical meromorphic section of s and with no chart carried”.

Stacks 0EQF, the identity in Z_{n-1}(X), reduced to its coefficients at the prime divisors. In Situation 0EDT let X/B be good, let X be integral with n = dim_δ(X), let ℒ be an invertible 𝒪_X-module, let s ∈ Γ(X, ℒ) and let σ be a nonzero meromorphic section of ℒ. Then

div_ℒ(σ) = [Z(s)]_{n-1} in Z_{n-1}(X)

holds exactly when it holds coefficientwise at every prime divisor of X, that is when ord_{Z,ℒ}(σ) is the multiplicity of Z in Z(s) for every prime divisor Z ⊆ X.

Both sides are coefficient families on the integral closed subspaces of X, and away from the prime divisors both vanish: the coefficient of div_ℒ(σ) at an integral closed subspace whose point set does not have codimension one is zero by Stacks 0EQE, part (1), and such a subspace has δ-dimension other than n - 1 by Stacks 0EPZ, so its coefficient in [Z(s)]_{n-1} is zero too. That is the whole content of the reduction. The right-hand side — the coefficient identity at a prime divisor — is proved, for the canonical meromorphic section of s, by AlgebraicGeometry.Space.invertibleDivisorCoefficients_globalSection_toIntegralClosedSubspace.

theorem divisorCycleOfSection_eq_zeroSchemeCycle_iff (_hL : IsInvertibleSheaf D sX hX L)
    (hfin : LocallyFinite fun Z : IntegralClosedSubspace D.site D.base D.base_mem X =>
      if zeroSchemeCycleCoeff D sX hX L s (n - 1) γ Z = 0 then ∅
      else subspacePointSet D.site D.base D.base_mem X Z.subspace) :
    divisorCycleOfSection D sX hX hdec L σ ratio hDv hint dimF hdimF hn =
        zeroSchemeCycle D sX hX L s (n - 1) γ hfin ↔
      ∀ W : PrimeDivisor D.site D.base D.base_mem X,
        divisorCoefficients.{u, u} D.site D.base D.base_mem hX.1 hdec L σ ratio W =
          zeroSchemeCycleCoeff D sX hX L s (n - 1) γ
            (W.toIntegralClosedSubspace D.site D.base D.base_mem)

AlgebraicGeometry.Space.firstChernClassCapFundamental_eq_cls_zeroSchemeCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/DivisorOfSectionCycle.lean, line 325. The attribute's comment: “second conclusion: c₁(ℒ) ∩ [X] = [Z(s)]_{n-1} in CH_{n-1}(X), where c₁(ℒ) ∩ [X] is Stacks 0EQE part (2) — the class of div_ℒ(s) in the ChowTarget parameter standing in for Stacks 0EQ6; this is the source's own derivation of its second conclusion FROM its first, so the argument heq is the FIRST conclusion of this tag (reduced to the prime divisors by divisorCycleOfSection_eq_zeroSchemeCycle_iff) and not this theorem's own conclusion”.

Stacks 0EQF, the identity in CH_{n-1}(X), from the identity in Z_{n-1}(X). In the situation above, if

div_ℒ(σ) = [Z(s)]_{n-1} in Z_{n-1}(X),

which is the first conclusion of the source and the hypothesis heq, then

c₁(ℒ) ∩ [X] = [Z(s)]_{n-1} in CH_{n-1}(X).

This is the source's own derivation of its second conclusion from its first: c₁(ℒ) ∩ [X] is by Stacks 0EQE, part (2), the class of div_ℒ(σ) for a nonzero meromorphic section σ of ℒ, a class independent of σ by AlgebraicGeometry.Space.firstChernClassCapFundamental_eq, so the second identity is the image of the first under the class map of the Chow group.

theorem firstChernClassCapFundamental_eq_cls_zeroSchemeCycle
    (_hL : IsInvertibleSheaf D sX hX L) {CH : Type w} [AddCommGroup CH]
    (chow : ChowTarget.{u, w, v} D sX hX (n - 1) CH)
    (hfin : LocallyFinite fun Z : IntegralClosedSubspace D.site D.base D.base_mem X =>
      if zeroSchemeCycleCoeff D sX hX L s (n - 1) γ Z = 0 then ∅
      else subspacePointSet D.site D.base D.base_mem X Z.subspace)
    (heq : divisorCycleOfSection D sX hX hdec L σ ratio hDv hint dimF hdimF hn =
      zeroSchemeCycle D sX hX L s (n - 1) γ hfin) :
    firstChernClassCapFundamental D sX hX hdec L chow σ ratio hDv hint dimF hdimF hn =
      chow.cls (zeroSchemeCycle D sX hX L s (n - 1) γ hfin)

AlgebraicGeometry.Space.sectionWeilDivisor_eq_zeroSchemeCycle_and_weilDivisorOfInvertibleSheaf_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/GlobalSectionDivisorCycle.lean, line 380. The attribute's comment: “both identities: div_ℒ(s) = [Z(s)]_{n-1} in Z_{n-1}(X) and c₁(ℒ) ∩ [X] = [Z(s)]_{n-1} in CH_{n-1}(X), for X/B good and integral with n = dim_δ(X), ℒ invertible and s a nonzero global section; div_ℒ(s) and c₁(ℒ) ∩ [X] are Stacks 0EQE parts (1) and (2) with every ingredient constructed, CH_{n-1}(X) is Stacks 0EQ6, [Z(s)]_{n-1} is Stacks 0EE9 of the zero scheme of Stacks 0845 at the canonical geometric representatives; nothing carried”.

Stacks 0EQF. In Situation 0EDT let X/B be good, let X be integral with n = dim_δ(X), let ℒ be an invertible 𝒪_X-module and let s ∈ Γ(X, ℒ) be a nonzero global section. Then

div_ℒ(s) = [Z(s)]_{n-1} in Z_{n-1}(X) and c₁(ℒ) ∩ [X] = [Z(s)]_{n-1} in CH_{n-1}(X).

div_ℒ(s) is the Weil divisor of Stacks 0EQE, part (1), of the meromorphic section of ℒ that s is; c₁(ℒ) ∩ [X] is Stacks 0EQE, part (2), in the Chow group CH_{n-1}(X) of Stacks 0EQ6; and [Z(s)]_{n-1} is the cycle of Stacks 0EE9 of the zero scheme of Stacks 0845, its multiplicities read at the canonical geometric representative of each point — by Stacks 0EE1 any representatives lying over the points give the same cycle, and sectionWeilDivisor_eq_zeroSchemeCycle_and_weilDivisorOfInvertibleSheaf_eq_of_liesOver states the identities for all of them. That [Z(s)]_{n-1} is an (n-1)-cycle is part of the conclusion: its coefficients are those of div_ℒ(s).

theorem sectionWeilDivisor_eq_zeroSchemeCycle_and_weilDivisorOfInvertibleSheaf_eq
    {s : L.sections} (hs : s ≠ 0) :
    sectionWeilDivisor D sX hX hint L hL hn
        (globalSectionMeromorphic D.site D.base D.base_mem hX.1 L s)
        (globalSectionMeromorphic_ne_zero_of_isInvertibleSheaf D sX hX L hL hs) =
      zeroSchemeCycle D sX hX L s (n - 1)
        (canonicalGeometricPoint D.site D.base D.base_mem
          (vanishingLocus D sX hX L s).1.toFunctor)
        (locallyFinite_zeroSchemeCycleCoeff_globalSection D sX hX hint L hL hn hs _
          (canonicalGeometricPoint_liesOver D _)) ∧
    weilDivisorOfInvertibleSheaf.{v} D sX hX hint L hL hn =
      chowClass.{v} D sX hX (n - 1) (zeroSchemeCycle D sX hX L s (n - 1)
        (canonicalGeometricPoint D.site D.base D.base_mem
          (vanishingLocus D sX hX L s).1.toFunctor)
        (locallyFinite_zeroSchemeCycleCoeff_globalSection D sX hX hint L hL hn hs _
          (canonicalGeometricPoint_liesOver D _)))
Tag 0EQG, a lemma

Tag 0EQG in the Stacks Project.

AlgebraicGeometry.Space.torsorOfInvertible_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorBaseChange.lean, line 211. The attribute's comment: “clause (3): in Situation 0EDT with X/B good and L an invertible O_X-module, for every morphism g : Y ⟶ X of good algebraic spaces the multiplicative torsor (q_Y : T_Y ⟶ Y, alpha_Y) of g^L, with T_Y = Spec_Y(⨁_n (g^L)^{⊗n}), is the base change of (q : T ⟶ X, alpha): there is g' : T_Y ⟶ T over g making the square cartesian and pulling alpha back to alpha_Y”.

Stacks 0EQG, clause (3): formation of (q : T ⟶ X, α) commutes with base change. For a morphism g : Y ⟶ X of good algebraic spaces, let q_Y : T_Y ⟶ Y and α_Y : q_Y^*(g^*ℒ) ≅ 𝒪_{T_Y} be the multiplicative torsor of the invertible 𝒪_Y-module g^*ℒ. There is a morphism g' : T_Y ⟶ T with g' ≫ q = q_Y ≫ g such that the square is cartesian and α pulls back along g' to α_Y: the trivialization g'^*α of (g' ≫ q)^*ℒ = (q_Y ≫ g)^*ℒ is α_Y composed with the canonical identification (q_Y ≫ g)^*ℒ ≅ q_Y^*(g^*ℒ) of Stacks 03LU.

theorem torsorOfInvertible_baseChange :
    ∃ (g' : torsorOfInvertibleSpace D pY hpY ((modulePullback D.site D.base D.base_mem g).obj L)
        (isInvertible_modulePullback_obj D.site D.base D.base_mem g L hL) ⟶
        torsorOfInvertibleSpace D p hp L hL)
      (w : g' ≫ torsorOfInvertibleProjection D p hp L hL =
        torsorOfInvertibleProjection D pY hpY ((modulePullback D.site D.base D.base_mem g).obj L)
        (isInvertible_modulePullback_obj D.site D.base D.base_mem g L hL) ≫ g),
      IsPullback g' (torsorOfInvertibleProjection D pY hpY
        ((modulePullback D.site D.base D.base_mem g).obj L)
        (isInvertible_modulePullback_obj D.site D.base D.base_mem g L hL))
          (torsorOfInvertibleProjection D p hp L hL) g ∧
        𝔱[p, hp, L, hL, g', w] =
          (modulePullbackTriangle D.site D.base D.base_mem
            (rfl : torsorOfInvertibleProjection D pY hpY
              ((modulePullback D.site D.base D.base_mem g).obj L)
        (isInvertible_modulePullback_obj D.site D.base D.base_mem g L hL) ≫ g =
              torsorOfInvertibleProjection D pY hpY
                ((modulePullback D.site D.base D.base_mem g).obj L)
        (isInvertible_modulePullback_obj D.site D.base D.base_mem g L hL) ≫ g)).hom.app L ≫
            (torsorOfInvertibleTrivialization D pY hpY
              ((modulePullback D.site D.base D.base_mem g).obj L)
        (isInvertible_modulePullback_obj D.site D.base D.base_mem g L hL)).hom

AlgebraicGeometry.Space.torsorOfInvertible_clause_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorCycles.lean, line 78. The attribute's comment: “clause (1): q is surjective, smooth, affine, of relative dimension 1”.

Stacks 0EQG, clause (1). In Situation 0EDT let X/B be good and let ℒ be an invertible 𝒪_X-module. The morphism q : T = \underline{Spec}_X(⨁_{n ∈ ℤ} ℒ^{⊗ n}) ⟶ X is surjective, smooth, affine, and of relative dimension 1.

theorem torsorOfInvertible_clause_one :
    IsSurjective D.site D.base D.base_mem (torsorOfInvertibleProjection D p hp L hL).hom ∧
      IsSmooth D.site D.base D.base_mem (torsorOfInvertibleProjection D p hp L hL).hom ∧
      IsAffineHom D.site D.base D.base_mem (torsorOfInvertibleProjection D p hp L hL).hom ∧
      HasRelativeDimension 1 D.site D.base D.base_mem
        (torsorOfInvertibleProjection D p hp L hL).hom

AlgebraicGeometry.Space.torsorOfInvertible_clause_six, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorCycles.lean, line 102. The attribute's comment: “clause (6): q^{-1}(Z) is a closed subspace of T of delta-dimension at most k + 1 and q^*[Z]_k = [q^{-1}(Z)]_{k+1}”.

Stacks 0EQG, clause (6). If Z ⊆ X is a closed subspace of δ-dimension ≤ k, then q^{-1}(Z) is a closed subspace of T of δ-dimension ≤ k + 1, and q^*[Z]_k = [q^{-1}(Z)]_{k+1}.

theorem torsorOfInvertible_clause_six (k : ℤ) (Z : Subfunctor X)
    (hZ : IsClosedSubspace D.site D.base D.base_mem Z)
    (hZk : deltaDimensionSubspace D p hp Z hZ ≤ (k : EInt)) :
    ∃ (hZ' : IsClosedSubspace D.site D.base D.base_mem
        (Z.preimage (torsorOfInvertibleProjection D p hp L hL).hom))
      (hdim : deltaDimensionSubspace D _ (isGood_torsorOfInvertible D p hp L hL)
        (Z.preimage (torsorOfInvertibleProjection D p hp L hL).hom) hZ' ≤ ((k + 1 : ℤ) : EInt)),
      torsorOfInvertibleFlatPullback D p hp L hL k (closedSubspaceCycle D p hp Z hZ k hZk) =
        closedSubspaceCycle D _ (isGood_torsorOfInvertible D p hp L hL)
          (Z.preimage (torsorOfInvertibleProjection D p hp L hL).hom) hZ' (k + 1) hdim

AlgebraicGeometry.Space.torsorOfInvertible_clause_seven, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorHenselian.lean, line 620. The attribute's comment: “clause (7): if ξ' ∈ |T| is the generic point of the fibre of |T| → |X| over ξ, then the ring map O^h_{X,ξ} → O^h_{T,ξ'} induced by q (the local homomorphism compatible with the stalk map of a commuting square of elementary etale neighbourhoods over q) is flat, the maximal ideal of O^h_{T,ξ'} is m^h_ξ O^h_{T,ξ'}, and the residue field extension is purely transcendental of transcendence degree 1 (generated by one element transcendental over the residue field of O^h_{X,ξ})”.

Stacks 0EQG, clause (7). In Situation 0EDT let X/B be good, let ℒ be an invertible 𝒪_X-module and q : T = \underline{Spec}(⨁_{n ∈ ℤ} ℒ^{⊗ n}) ⟶ X. If ξ' ∈ |T| is the generic point of the fibre of |T| → |X| over ξ = q(ξ') — every point of that fibre is a specialization of ξ' — then the ring map φ : 𝒪^h_{X, ξ} ⟶ 𝒪^h_{T, ξ'} induced by q is flat, 𝔪^h_{ξ'} = 𝔪^h_ξ 𝒪^h_{T, ξ'}, and the residue field extension is purely transcendental of transcendence degree 1: it is generated by a single element transcendental over κ(ξ).

The map φ is the one induced by q: it is the local homomorphism agreeing on the image of 𝒪_{V, v} with the stalk map of a commuting square of elementary étale neighborhoods U ⟶ V over q, which determines it by the universal property of the henselization.

theorem torsorOfInvertible_clause_seven
    (ξ' : points D.site D.base D.base_mem (torsorOfInvertibleSpace D p hp L hL).obj)
    (hξ' : ∀ t, pointsMap D.site D.base D.base_mem _
      (torsorOfInvertibleProjection D p hp L hL).hom t =
      pointsMap D.site D.base D.base_mem _ (torsorOfInvertibleProjection D p hp L hL).hom ξ' →
        ξ' ⤳ t) :
    letI := henselianLocalRing_isLocalRing D.site D.base D.base_mem X hp.1
      (pointsMap D.site D.base D.base_mem _ (torsorOfInvertibleProjection D p hp L hL).hom ξ')
      (D.isDecentSpace_of_isGood p hp)
    letI := henselianLocalRing_isLocalRing D.site D.base D.base_mem
      (torsorOfInvertibleSpace D p hp L hL).obj (torsorOfInvertibleSpace D p hp L hL).property ξ'
      (D.isDecentSpace_of_isGood _ (isGood_torsorOfInvertible D p hp L hL))
    ∃ (V : ElementaryEtaleNeighborhood D.site D.base D.base_mem X hp.1
        (pointsMap D.site D.base D.base_mem _ (torsorOfInvertibleProjection D p hp L hL).hom ξ'))
      (U : ElementaryEtaleNeighborhood D.site D.base D.base_mem
        (torsorOfInvertibleSpace D p hp L hL).obj (torsorOfInvertibleSpace D p hp L hL).property ξ')
      (j : U.scheme ⟶ V.scheme) (hj : j.left.1 U.point = V.point)
      (φ : (henselianLocalRing D.site D.base D.base_mem X hp.1
          (pointsMap D.site D.base D.base_mem _ (torsorOfInvertibleProjection D p hp L hL).hom ξ')
          (D.isDecentSpace_of_isGood p hp) : Type (u + 1)) →+*
        (henselianLocalRing D.site D.base D.base_mem (torsorOfInvertibleSpace D p hp L hL).obj
          (torsorOfInvertibleSpace D p hp L hL).property ξ'
          (D.isDecentSpace_of_isGood _ (isGood_torsorOfInvertible D p hp L hL)) : Type (u + 1))),
      yoneda.map j ≫ V.toSpace = U.toSpace ≫ (torsorOfInvertibleProjection D p hp L hL).hom ∧
        (∀ a, φ (stalkToHenselianLocalRing D.site D.base D.base_mem X hp.1 _
            (D.isDecentSpace_of_isGood p hp) V a) =
          stalkToHenselianLocalRing D.site D.base D.base_mem _ _ ξ'
            (D.isDecentSpace_of_isGood _ (isGood_torsorOfInvertible D p hp L hL)) U
            (((V.scheme.left.1.presheaf.stalkCongr (.of_eq hj.symm)).hom ≫
              j.left.1.stalkMap U.point).hom a)) ∧
        ∃ _ : IsLocalHom φ,
          φ.Flat ∧
          Ideal.map φ (maximalIdeal _) = maximalIdeal _ ∧
          letI := (ResidueField.map φ).toAlgebra
          ∃ t : ResidueField (henselianLocalRing D.site D.base D.base_mem
              (torsorOfInvertibleSpace D p hp L hL).obj
                (torsorOfInvertibleSpace D p hp L hL).property
              ξ' (D.isDecentSpace_of_isGood _ (isGood_torsorOfInvertible D p hp L hL)) :
                Type (u + 1)),
            Transcendental (ResidueField (henselianLocalRing D.site D.base D.base_mem X hp.1
              (pointsMap D.site D.base D.base_mem _
                (torsorOfInvertibleProjection D p hp L hL).hom ξ')
              (D.isDecentSpace_of_isGood p hp) : Type (u + 1))) t ∧
            IntermediateField.adjoin (ResidueField
              (henselianLocalRing D.site D.base D.base_mem X hp.1
              (pointsMap D.site D.base D.base_mem _
                (torsorOfInvertibleProjection D p hp L hL).hom ξ')
              (D.isDecentSpace_of_isGood p hp) : Type (u + 1))) {t} = ⊤

AlgebraicGeometry.Space.torsorOfInvertible_clause_four, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorInjective.lean, line 154. The attribute's comment: “clause (4): q^* : Z_k(X) → Z_{k+1}(T) is injective”.

Stacks 0EQG, clause (4). The flat pullback q^* : Z_k(X) → Z_{k+1}(T) is injective.

theorem torsorOfInvertible_clause_four (k : ℤ) :
    Function.Injective (torsorOfInvertibleFlatPullback D p hp L hL k)

AlgebraicGeometry.Space.torsorOfInvertible_clause_five, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorIntegral.lean, line 228. The attribute's comment: “clause (5): q^{-1}(Z) is an integral closed subspace of T for Z an integral closed subspace of X”.

Stacks 0EQG, clause (5). If Z ⊆ X is an integral closed subspace, then q^{-1}(Z) ⊆ T is an integral closed subspace.

theorem torsorOfInvertible_clause_five (Z : IntegralClosedSubspace D.site D.base D.base_mem X) :
    IsClosedSubspace D.site D.base D.base_mem
        (Z.subspace.preimage (torsorOfInvertibleProjection D p hp L hL).hom) ∧
      IsIntegralSpace D.site D.base D.base_mem
        (Z.subspace.preimage (torsorOfInvertibleProjection D p hp L hL).hom).toFunctor

AlgebraicGeometry.Space.isQuasicoherent_laurentAlgebraSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorOfInvertible.lean, line 123. The attribute's comment: “the quasi-coherence of ⨁_{n ∈ ℤ} L^{⊗n} that clause (1) presupposes in forming T = Spec_X(⨁_{n ∈ ℤ} L^{⊗n}): in Situation 0EDT with X/B good, the Laurent algebra of an invertible O_X-module is a quasi-coherent O_X-algebra, with no hypothesis on L beyond invertibility -- triviality of L on an etale covering is DISCHARGED here from local ringedness of the small etale site, not assumed. Nothing about the morphism q is covered by this declaration”.

The Laurent algebra sheaf ⨁_{n ∈ ℤ} ℒ^{⊗ n} of an invertible 𝒪_X-module ℒ is quasi-coherent.

theorem isQuasicoherent_laurentAlgebraSheaf :
    AlgebraSheaf.IsQuasicoherent (laurentAlgebraSheaf D p hp L hL)

AlgebraicGeometry.Space.isAffineHom_multiplicativeTorsorProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorOfInvertible.lean, line 152. The attribute's comment: “clause (1), the affineness part -- BUT VACUOUS AS STATED, and registered here only because the base file carries this line. The statement takes a parameter E : AffineAlgebraAntiEquivalence, this development's rendering of Stacks 081V with the tag's unrestricted target, and that type is EMPTY over any site one of whose algebraic spaces has an affine etale chart with a nonzero ring of functions (not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart). Over such a site this theorem asserts nothing: quasi-coherence of the Laurent algebra, which IS discharged by isQuasicoherent_laurentAlgebraSheaf, is discharged into a statement with no content. THE REGISTRATION THAT CARRIES THIS CLAUSE is isAffineHom_multiplicativeTorsorSpectrumProjection (MultiplicativeTorsorSpectrum), which takes no parameter at all; isAffineHom_boundedMultiplicativeTorsorProjection gives it inside the site of X under the size condition of the corrected 081V, which E implies. Read this line as covering nothing”.

The projection q : T = \underline{Spec}_X(⨁_{n ∈ ℤ} ℒ^{⊗ n}) ⟶ X of the multiplicative torsor of an invertible 𝒪_X-module is an affine morphism of algebraic spaces.

This statement is vacuous over any nondegenerate site, since the parameter E it takes is empty there; see the implementation notes above. The assertion under the hypotheses of Situation 0EDT alone is AlgebraicGeometry.Space.isAffineHom_multiplicativeTorsorSpectrumProjection.

theorem isAffineHom_multiplicativeTorsorProjection :
    IsAffineHom D.site D.base D.base_mem (multiplicativeTorsorProjection D p hp L hL E
      (isQuasicoherent_laurentAlgebraSheaf D p hp L hL)).hom

AlgebraicGeometry.Space.isPullback_multiplicativeTorsorBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorOfInvertible.lean, line 207. The attribute's comment: “clause (3) for q: the base change of q along an arbitrary g : Y ⟶ X is cartesian and Y ×_X T is the relative spectrum over Y of g^(⨁_n L^{⊗n}), the latter being the corner of the cartesian square as stated. VACUOUS AS STATED: it takes the parameters E : AffineAlgebraAntiEquivalence and C its base-change clause, and E is EMPTY over any site one of whose algebraic spaces has an affine etale chart with a nonzero ring of functions (not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart). Over such a site this theorem asserts nothing. In particular, although Stacks 08AI at q -- the input the construction of alpha : q^L ≅ O_T consumes -- is genuinely discharged from X/B good and L invertible by affineDirectImageEquivalence_multiplicativeTorsorProjection, that discharge is itself stated under E and so is equally vacuous; it should not be read as evidence that this clause is in better shape than it is. Two further pieces of the source's clause (3) lie outside this statement in any case: alpha itself, whose construction needs in addition the degree-shift isomorphism of the Laurent algebra over itself, ⨁_n L^{⊗(n+1)} ≅ ⨁_n L^{⊗n}, which is clause (2)'s own content and which this tree does not have (only the per-degree powSuccIso); and the identification of g^(⨁_n L^{⊗n}) with ⨁_n (g^L)^{⊗n}. No parameter-free counterpart of this base-change square has been formed: MultiplicativeTorsorSpectrum supplies T, q and the affineness of q without parameters, not the base change”.

The base change of q : T ⟶ X along g : Y ⟶ X is cartesian, with corner \underline{Spec}_Y(g^*(⨁_{n ∈ ℤ} ℒ^{⊗ n})): forming the multiplicative torsor commutes with arbitrary base change.

This statement is vacuous over any nondegenerate site, since the parameters E and C it takes are empty there; see the implementation notes above.

theorem isPullback_multiplicativeTorsorBaseChange :
    IsPullback (multiplicativeTorsorBaseChangeProjection D p hp L hL E C g)
      (multiplicativeTorsorBaseChange D p hp L hL E C g).obj.hom
      (multiplicativeTorsorProjection D p hp L hL E
        (isQuasicoherent_laurentAlgebraSheaf D p hp L hL)) g

AlgebraicGeometry.Space.isAffineHom_multiplicativeTorsorSpectrumProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorSpectrum.lean, line 183. The attribute's comment: “clause (1), the affineness part only, in Situation 0EDT with X/B good: for an invertible O_X-module L the projection q of T = Spec_X(⨁_{n ∈ ℤ} L^{⊗n}) is affine. Carries NO parameter and no size condition: quasi-coherence of the Laurent algebra is discharged by isQuasicoherent_laurentAlgebraSheaf, itself resting on triviality of L on an etale covering, discharged by isLocallyTrivial_of_isInvertibleSheaf from local ringedness of the small etale site, and T is formed by relativeSpectrum, the unconditional form of Stacks 081W. This replaces isAffineHom_multiplicativeTorsorProjection, which asserts the same thing under a parameter E : AffineAlgebraAntiEquivalence that is EMPTY over any site one of whose algebraic spaces has an affine etale chart with a nonzero ring of functions (not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart) and so asserts nothing there. q lives over relativeSpectrumSite, the Stacks 03FO enlargement of the site of X; isAffineHom_boundedMultiplicativeTorsorProjection is the same assertion inside the site of X itself, under the size condition of the corrected 081V, which E implies. NOT COVERED by this or any other declaration: the rest of clause (1) -- q surjective, smooth and of relative dimension 1 -- and clauses (2), (4), (5), (6), (7). The source derives the three remaining properties of clause (1) from T x_X U ≅ G_m x U for an etale chart U trivialising L, and that identification does not exist in this tree: isPullback_affineChartSpec identifies the relative spectrum over an affine chart with Spec of the algebra's sections there, nothing identifies the Laurent algebra's sections at a trivialising chart V with O(V)[t,t^{-1}] (the sheafification step is unaccounted for), and no scheme-level smoothness, surjectivity or relative-dimension statement about multiplicativeGroupBaseChange exists”.

The projection q : T ⟶ X of the multiplicative torsor of an invertible 𝒪_X-module is an affine morphism of algebraic spaces, under the hypotheses of Situation 0EDT and no others: X/B good and ℒ invertible.

theorem isAffineHom_multiplicativeTorsorSpectrumProjection :
    IsAffineHom
      (relativeSpectrumSite
        (laurentQuasicoherentAlgebra D p hp L hL (isQuasicoherent_laurentAlgebraSheaf D p hp L hL)))
      D.base
      (contains_relativeSpectrumSite
        (laurentQuasicoherentAlgebra D p hp L hL
          (isQuasicoherent_laurentAlgebraSheaf D p hp L hL)))
      (multiplicativeTorsorSpectrumProjection D p hp L hL).hom

AlgebraicGeometry.Space.torsorOfInvertible_clause_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/MultiplicativeTorsorTrivialization.lean, line 426. The attribute's comment: “clause (2): there is an isomorphism alpha : q^*L ≅ O_T”.

There is an isomorphism α : q^*ℒ ≅ 𝒪_T.

theorem torsorOfInvertible_clause_two :
    Nonempty ((modulePullback D.site D.base D.base_mem
      (torsorOfInvertibleProjection D p hp L hL)).obj L ≅ SheafOfModules.unit _)
Tag 0EQH, a lemma

Tag 0EQH in the Stacks Project.

AlgebraicGeometry.Space.PrimeDivisor.ord_eq_ord_of_extendedMaximalIdeal_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FlatPullbackOrderOfVanishing.lean, line 503. The attribute's comment: “coefficientwise at a prime divisor Z = q^{-1}(Z') of T: ord_Z(q^(s)) = ord_{Z',L}(s), which is the source's q^ div_L(s) = div_T(q^(s)) read at the coefficient of Z. No component bookkeeping arises: the source assumes the base integral, so the multiplicity of a component is one, and the multiplicity of Z over Z' is one as well by hmax. It is stated coefficientwise because the flat pullback of cycles is Stacks 0EP8, which this repository does not have, and because the principal divisor div(q^(s)) of Stacks 0ENP is not available either; for the same reason Stacks 0EPT and 0EPV are already carried coefficientwise here. The source's other case, a prime divisor of T dominating Y, where both coefficients vanish, is bookkeeping internal to the flat pullback and does not arise in a statement indexed by a prime divisor lying over a prime divisor. PROVED, not assumed: that the two orders of vanishing are equal, from Stacks 02M1 (length_baseChange_eq_length_mul_length_quotient) through Ring.ord_map_of_flatHom, the multiplicity being one because the extended maximal ideal is the maximal ideal and the residue field has length one. RESTRICTED: carried as explicit named hypotheses are (i) the flat local homomorphism φ : O^h_{Y,ξ'} → O^h_{T,ξ} with hloc and hflat, and (ii) the identity hmax that the maximal ideal of O^h_{Y,ξ'} extends to the maximal ideal of O^h_{T,ξ} — these are the two properties of q that Lemma 0EQG supplies and that the source uses here, the morphism q itself being available in this repository only as multiplicativeTorsorProjection, whose surjectivity, smoothness and relative dimension are not proved there; (iii) the rational function qs standing for q^(s), with the embedding embT of Stacks 0ENK, and hqs, that its ratio at ξ is the image under φ of the ratio of s at ξ' — the trivialization alpha : q^L ≅ O_T is not constructed in this repository, as the clause of Stacks 0EQG on multiplicativeTorsorBaseChange records, so the identification of q^*(s) as a function is this hypothesis, which is the source's own step of writing s/s_{ξ'} = a/b and pulling the fraction back; and (iv) the ratio of Stacks 0EPR at the generic point of Z' as the parameter ratioY”.

Stacks 0EQH, coefficientwise. The divisor of a meromorphic section pulls back to the divisor of the associated rational function on the multiplicative torsor. Let q : T ⟶ Y be the morphism of Stacks 0EQG for an invertible 𝒪_Y-module ℒ, so that q^*ℒ ≅ 𝒪_T and a nonzero meromorphic section s of ℒ becomes a nonzero meromorphic function q^*(s) on T. Let Z' ⊆ Y be a prime divisor and Z = q^{-1}(Z'), and let φ : 𝒪^h_{Y,ξ'} ⟶ 𝒪^h_{T,ξ} be the induced flat local homomorphism. Because 𝔪^h_{Y,ξ'} 𝒪^h_{T,ξ} = 𝔪^h_{T,ξ},

ord_Z(q^*(s)) = ord_{Z',ℒ}(s),

which is q^* div_ℒ(s) = div_T(q^*(s)) coefficientwise.

The hypothesis hmax is the identity of ideals that Stacks 0EQG supplies, and it is what makes the multiplicity one: the quotient is then the residue field of 𝒪^h_{T,ξ}, whose length is one, so Ring.ord_map_of_flatHom gives equality of the two orders rather than a multiple.

theorem PrimeDivisor.ord_eq_ord_of_extendedMaximalIdeal_eq
    (hloc : IsLocalHom φ) (hflat : φ.Flat)
    (hmax : Ideal.map φ
        (IsLocalRing.maximalIdeal ↥(ZY.genericHenselianLocalRing B S hS hY hdecY)) =
      IsLocalRing.maximalIdeal ↥(ZX.genericHenselianLocalRing B S hS hX hdecX))
    (L : Modules.{u, max u z} B S hS Y hY)
    (s : MeromorphicSection.{u, z} B S hS Y hY L)
    (ratioY : LocalRatio.{u, z} B S hS hY hdecY ZY L)
    (embT : rationalFunctions B S hS hX →+* ZX.genericTotalFractionRing B S hS hX hdecX)
    (qs : rationalFunctions B S hS hX)
    (a b : nonZeroDivisors ↥(ZY.genericHenselianLocalRing B S hS hY hdecY))
    (hs : (ratioY s : ZY.genericTotalFractionRing B S hS hY hdecY) =
      IsLocalization.mk' (ZY.genericTotalFractionRing B S hS hY hdecY)
        (a : ↥(ZY.genericHenselianLocalRing B S hS hY hdecY)) b)
    (hqs : embT qs = IsLocalization.mk' (ZX.genericTotalFractionRing B S hS hX hdecX)
      (φ (a : ↥(ZY.genericHenselianLocalRing B S hS hY hdecY)))
      (⟨φ (b : ↥(ZY.genericHenselianLocalRing B S hS hY hdecY)),
        Ring.map_mem_nonZeroDivisors_of_flatHom hflat b.2⟩ :
        nonZeroDivisors ↥(ZX.genericHenselianLocalRing B S hS hX hdecX)))
    (hqsu : IsUnit (embT qs)) :
    ZX.ord B S hS hX hdecX (embT qs) hqsu =
      orderOfVanishingSection.{u, z} B S hS hY hdecY ZY L s ratioY

AlgebraicGeometry.Space.flatPullbackMap_sectionWeilDivisor_torsorOfInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/TorsorPullbackDivisor.lean, line 108. The attribute's comment: “q^ div_L(s) = div_T(q^(s)) as cycles on T, for X/B good and integral, L invertible, s a nonzero meromorphic section and q : T -> X the morphism of 0EQG (torsorOfInvertibleProjection: flat of relative dimension 1, T/B good, T integral, all proved). Stated with div_{q^L}(q^s) and, for EVERY isomorphism alpha : q^L ≅ O_T, with the divisor div_{O_T}(alpha(q^s)) of the nonzero meromorphic function alpha(q^s); q^ on cycles is the flat pullback of 0EP8, div is 0EQE, q^*s is the pullback of 0ENC. Proved from 0EQQ for q (T integral, so the component sum collapses) and the invariance of div under an isomorphism of modules”.

In Situation 0EDT let X/B be good and integral with n = dim_δ(X), let ℒ be an invertible 𝒪_X-module, let s be a nonzero meromorphic section of ℒ, and let q : T ⟶ X be the morphism of Stacks 0EQG. Then

q^* div_ℒ(s) = div_T(q^*(s))

in Z_n(T): the left-hand side is the flat pullback along q (flat of relative dimension one) of the Weil divisor of s; on the right q^*(s) is the pullback of s, and the identity holds both with div_{q^*ℒ}(q^*s) and, for every isomorphism α : q^*ℒ ≅ 𝒪_T, with the divisor div_{𝒪_T}(α(q^*s)) of the meromorphic function α(q^*s) on T.

theorem flatPullbackMap_sectionWeilDivisor_torsorOfInvertible {n : ℤ}
    (hn : deltaDimensionClosed D p hp Set.univ isClosed_univ = (n : EInt))
    (s : MeromorphicSection.{u, u} D.site D.base D.base_mem X hp.1 L) (hs : s ≠ 0) :
    flatPullbackMap D ((torsorOfInvertibleProjection D p hp L hL).hom ≫ p)
        (isGood_torsorOfInvertible D p hp L hL) p hp (torsorOfInvertibleProjection D p hp L hL).hom
        rfl 1 (isFlat_torsorOfInvertibleProjection D p hp L hL)
        (hasRelativeDimension_torsorOfInvertibleProjection D p hp L hL) (n - 1) (n + (1 : ℕ) - 1)
        (by push_cast; ring) (sectionWeilDivisor D p hp hint L hL hn s hs) =
      sectionWeilDivisor D ((torsorOfInvertibleProjection D p hp L hL).hom ≫ p)
        (isGood_torsorOfInvertible D p hp L hL)
        (isIntegralSpace_torsorOfInvertibleSpace D p hp L hL hint)
        ((modulePullback D.site D.base D.base_mem (torsorOfInvertibleProjection D p hp L hL)).obj L)
        (isInvertibleSheaf_modulePullback D p hp _ (isGood_torsorOfInvertible D p hp L hL)
          (torsorOfInvertibleProjection D p hp L hL) hL)
        (deltaDimensionClosed_torsorOfInvertibleSpace D p hp hint L hL hn)
        (pullbackMeromorphicSection D.site D.base D.base_mem
          (torsorOfInvertibleProjection D p hp L hL) L
          (pullbacksMeromorphicSections_of_flat D.site D.base D.base_mem _
            (isFlat_torsorOfInvertibleProjection D p hp L hL)) s)
        (pullbackMeromorphicSection_ne_zero_of_isFlat D p hp hint _
          (isGood_torsorOfInvertible D p hp L hL)
          (isIntegralSpace_torsorOfInvertibleSpace D p hp L hL hint) _
          (isFlat_torsorOfInvertibleProjection D p hp L hL) hL s hs) ∧
    ∀ α : (modulePullback D.site D.base D.base_mem
          (torsorOfInvertibleProjection D p hp L hL)).obj L ≅
        SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite D.site
          D.base D.base_mem (torsorOfInvertibleSpace D p hp L hL).obj
          (isGood_torsorOfInvertible D p hp L hL).1).O),
      flatPullbackMap D ((torsorOfInvertibleProjection D p hp L hL).hom ≫ p)
          (isGood_torsorOfInvertible D p hp L hL) p hp
          (torsorOfInvertibleProjection D p hp L hL).hom
          rfl 1 (isFlat_torsorOfInvertibleProjection D p hp L hL)
          (hasRelativeDimension_torsorOfInvertibleProjection D p hp L hL) (n - 1) (n + (1 : ℕ) - 1)
          (by push_cast; ring) (sectionWeilDivisor D p hp hint L hL hn s hs) =
        sectionWeilDivisor D ((torsorOfInvertibleProjection D p hp L hL).hom ≫ p)
          (isGood_torsorOfInvertible D p hp L hL)
          (isIntegralSpace_torsorOfInvertibleSpace D p hp L hL hint) _
          (isInvertibleSheaf_unit D _ (isGood_torsorOfInvertible D p hp L hL))
          (deltaDimensionClosed_torsorOfInvertibleSpace D p hp hint L hL hn)
          (SheafOfModules.sectionsMap
            (meromorphicSectionSheafMap D.site D.base D.base_mem _
              (isGood_torsorOfInvertible D p hp L hL).1 α.hom)
            (pullbackMeromorphicSection D.site D.base D.base_mem
              (torsorOfInvertibleProjection D p hp L hL) L
              (pullbacksMeromorphicSections_of_flat D.site D.base D.base_mem _
                (isFlat_torsorOfInvertibleProjection D p hp L hL)) s))
          (sectionsMap_meromorphicSectionSheafMap_inv_ne_zero D _
            (isGood_torsorOfInvertible D p hp L hL)
            (isIntegralSpace_torsorOfInvertibleSpace D p hp L hL hint)
            (isInvertibleSheaf_unit D _ (isGood_torsorOfInvertible D p hp L hL))
            (isInvertibleSheaf_modulePullback D p hp _ (isGood_torsorOfInvertible D p hp L hL)
              (torsorOfInvertibleProjection D p hp L hL) hL) α.symm _
            (pullbackMeromorphicSection_ne_zero_of_isFlat D p hp hint _
              (isGood_torsorOfInvertible D p hp L hL)
              (isIntegralSpace_torsorOfInvertibleSpace D p hp L hL hint) _
              (isFlat_torsorOfInvertibleProjection D p hp L hL) hL s hs))
Sources

Section82.18 Intersecting with an invertible sheaf#

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

Tag 0EQJ, a definition

Tag 0EQJ in the Stacks Project.

AlgebraicGeometry.Space.canonicalFirstChernCap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/CanonicalFirstChernCap.lean, line 122. The attribute's comment: “the cap product c_1(N) ∩ - : Z_{k+1}(X) → CH_k(X) with the first Chern class of an invertible O_X-module N on a good algebraic space X/B, cases (1) and (2): the component cycle c_1(N|_W) ∩ [W] is the Weil divisor div_{N|_W}(t_W) of Stacks 0EQE at the canonical ratios of Stacks 0EPR for a regular meromorphic section given by Stacks 0EPQ (canonicalFirstChernRule), the target is the Chow group of Stacks 0EQ6 part (4), and the pushforward i_* and the fundamental cycle [W] are the genuine ones; nothing is a parameter. Case (1) is canonicalFirstChernCap_integralCycle and case (2) is the coefficientwise additive extension firstChernCapCycleMap. The source pushes the class of div_{N|_W}(t_W) forward, this pushes the cycle forward and takes the class afterwards”.

Intersection with the first Chern class of an invertible sheaf: the cap product c₁(𝒩) ∩ - : Z_{k+1}(X) → CH_k(X) attached to an invertible 𝒪_X-module 𝒩 on a good algebraic space X/B. It sends α = ∑ n_W [W] to the class of ∑_W n_W i_*(c₁(𝒩|_W) ∩ [W]), where i : W → X is the inclusion and the component cycle c₁(𝒩|_W) ∩ [W] is AlgebraicGeometry.Space.canonicalFirstChernRule, the Weil divisor div_{𝒩|_W}(t_W) of Stacks 0EQE, part (1), at the canonical ratios of Stacks 0EPR for the regular meromorphic section of 𝒩|_W given by Stacks 0EPQ. The target is the Chow group CH_k(X) = Z_k(X)/∼_rat of Stacks 0EQ6, part (4); the pushforward i_* is applied to the cycle and the class is taken in CH_k(X) afterwards.

def canonicalFirstChernCap (k : ℤ) : CycleGroup D sX (k + 1) →+ chowGroup.{v} D sX hX k

AlgebraicGeometry.Space.canonicalFirstChernCap_integralCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/CanonicalFirstChernCap.lean, line 135. The attribute's comment: “case (1): the value of the cap product on the fundamental cycle [W] of an integral closed subspace W of δ-dimension k+1 is the class of i_(c_1(N|_W) ∩ [W]), with the component cycle c_1(N|_W) ∩ [W] the Weil divisor div_{N|_W}(t_W) of Stacks 0EQE at the canonical ratios and the class taken in the Chow group of Stacks 0EQ6; i_ is applied to the cycle and the class taken afterwards, the source applying it to the class”.

On the fundamental cycle [W] of an integral closed subspace i : W → X of δ-dimension k + 1 the cap product AlgebraicGeometry.Space.canonicalFirstChernCap is the class of i_*(c₁(𝒩|_W) ∩ [W]), the inner cycle being the Weil divisor div_{𝒩|_W}(t_W) of Stacks 0EQE at the canonical choices.

theorem canonicalFirstChernCap_integralCycle (k : ℤ)
    {W : IntegralClosedSubspace D.site D.base D.base_mem X}
    (hW : deltaDimension D sX W = k + 1) :
    canonicalFirstChernCap.{u, v} D sX hX N hN k (integralCycle D sX (k + 1) W hW) =
      chowClass.{v} D sX hX k (integralClosedSubspacePushforward D sX hX W k
        (canonicalFirstChernRule D sX hX N hN k W hW))

AlgebraicGeometry.Space.firstChernClassCap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FirstChernClassCap.lean, line 458. The attribute's comment: “the cap product c_1(L) ∩ - : Z_{k+1}(X) → CH_k(X) with the first Chern class of an invertible sheaf L on a good algebraic space X/B, cases (1) and (2); the component cycle c_1(L|_W) ∩ [W] on an integral closed subspace W of δ-dimension k+1 and the Chow group CH_k(X) are explicit parameters, standing in for Stacks 0EQE and Stacks 0EQ6 parts (2)-(4), neither of which exists for algebraic spaces here; the pushforward i_* and the fundamental cycle [W] are not parameters”.

Stacks 0EQJ. Intersection with the first Chern class of an invertible sheaf: the cap product c₁(ℒ) ∩ - : Z_{k+1}(X) ⟶ CH_k(X) attached to an invertible sheaf ℒ on a good algebraic space X/B.

On the cycle [W] of an integral closed subspace W ⊆ X of δ-dimension k + 1 it is the class of i_*(c₁(ℒ|_W) ∩ [W]), which is case (1) of the source; see AlgebraicGeometry.Space.firstChernClassCap_integralCycle. Case (2), the extension of that rule by linearity over an arbitrary (k+1)-cycle, is AlgebraicGeometry.Space.firstChernCapCycleMap, which is proved to land in Z_k(X) and to be additive.

The component cycle c₁(ℒ|_W) ∩ [W] on W and the Chow group CH_k(X) are explicit parameters, standing in for Stacks 0EQE and Stacks 0EQ6 parts (2)–(4), neither of which is available for algebraic spaces in this repository; see the implementation notes of StacksFrontier.AlgebraicGeometry.Spaces.Chow.FirstChernClassCap. The pushforward i_* and the fundamental cycle [W] are not parameters.

def firstChernClassCap (_hL : IsInvertibleSheaf D sX hX L)
    (chern : FirstChernComponentCycleRule D sX k)
    {CH : Type w} [AddCommGroup CH] (chow : ChowTarget.{u, w, v} D sX hX k CH) :
    CycleGroup D sX (k + 1) →+ CH

AlgebraicGeometry.Space.firstChernClassCap_integralCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FirstChernClassCap.lean, line 477. The attribute's comment: “case (1): the value of the cap product on the fundamental cycle [W] of an integral closed subspace W of δ-dimension k+1 is the class of i_(c_1(L|_W) ∩ [W]), with the component cycle c_1(L|_W) ∩ [W] and the Chow group CH_k(X) as explicit parameters standing in for Stacks 0EQE and Stacks 0EQ6 parts (2)-(4); the pushforward i_ is applied to the cycle and the class taken afterwards, the source applying it to the class”.

Stacks 0EQJ, case (1). On the cycle [W] of an integral closed subspace W ⊆ X of δ-dimension k + 1 the cap product is the class of i_*(c₁(ℒ|_W) ∩ [W]), for the closed immersion i : W → X.

The source applies the proper pushforward i_* : CH_k(W) ⟶ CH_k(X) to the class of c₁(ℒ|_W) ∩ [W]; the form below applies the pushforward of cycles and takes the class afterwards, which is the same statement once proper pushforward is known to respect rational equivalence.

theorem firstChernClassCap_integralCycle (hL : IsInvertibleSheaf D sX hX L)
    (chern : FirstChernComponentCycleRule D sX k)
    {CH : Type w} [AddCommGroup CH] (chow : ChowTarget.{u, w, v} D sX hX k CH)
    {W : IntegralClosedSubspace D.site D.base D.base_mem X}
    (hW : deltaDimension D sX W = k + 1) :
    firstChernClassCap D sX hX L k hL chern chow (integralCycle D sX (k + 1) W hW) =
      chow.cls (integralClosedSubspacePushforward D sX hX W k (chern W hW))
Tag 0EQK, a lemma

Tag 0EQK in the Stacks Project.

AlgebraicGeometry.Space.canonicalFirstChernCap_picardTensorModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/CanonicalFirstChernCapAdditive.lean, line 418. The attribute's comment: “first assertion: c_1(L) ∩ α + c_1(N) ∩ α = c_1(L ⊗ N) ∩ α in CH_k(X), for the cap product of Stacks 0EQJ at the canonical choices (canonicalFirstChernCap), the tensor product picardTensorModule and the Chow group of Stacks 0EQ6. DISCHARGED: the component cycle c_1(L|_W) ∩ [W] is the constructed canonicalFirstChernRule, not a parameter, and the tensor product and the product of meromorphic sections are constructed too, so nothing is carried. Proved from Stacks 0EPV at the canonical choices, Stacks 03EL for the restriction of a tensor product to W, Stacks 0EPT, and Stacks 0EQ6 parts (1), (2) and (4). CORRECTED: the source writes α ∈ Z_{k-1}(X), which cannot give an identity in CH_k(X) for the operation Z_{k+1}(X) → CH_k(X) of Stacks 0EQJ; stated here for α ∈ Z_{k+1}(X), as the identical scheme-side lemma Stacks 02SP does”.

Additivity of the first Chern class cap product. For invertible 𝒪_X-modules ℒ and 𝒩 on a good algebraic space X/B and every α ∈ Z_{k+1}(X),

c₁(ℒ) ∩ α + c₁(𝒩) ∩ α = c₁(ℒ ⊗_{𝒪_X} 𝒩) ∩ α in CH_k(X).

The cap product is the one of Stacks 0EQJ at the canonical choices, AlgebraicGeometry.Space.canonicalFirstChernCap, the tensor product is AlgebraicGeometry.Space.picardTensorModule, and CH_k(X) is the Chow group of Stacks 0EQ6.

theorem canonicalFirstChernCap_picardTensorModule
    (L N : Modules.{u, u} D.site D.base D.base_mem X hX.1)
    (hL : IsInvertibleModule (⟨X, hX.1⟩ : AlgebraicSpaces D.site D.base D.base_mem) L)
    (hN : IsInvertibleModule (⟨X, hX.1⟩ : AlgebraicSpaces D.site D.base D.base_mem) N)
    (k : ℤ) (α : CycleGroup D sX (k + 1)) :
    canonicalFirstChernCap.{u, u + 1} D sX hX L hL k α +
        canonicalFirstChernCap.{u, u + 1} D sX hX N hN k α =
      canonicalFirstChernCap.{u, u + 1} D sX hX
        (picardTensorModule D.site D.base D.base_mem hX.1 L N)
        (isInvertibleModule_picardTensorModule D.site D.base D.base_mem hX.1 L N hL hN) k α

AlgebraicGeometry.Space.canonicalFirstChernCap_tensorUnit_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/CanonicalFirstChernCapAdditive.lean, line 486. The attribute's comment: “second assertion: c_1(O_X) ∩ α = 0 in CH_k(X), for the cap product of Stacks 0EQJ at the canonical choices (canonicalFirstChernCap) and the Chow group of Stacks 0EQ6; O_X is the tensor unit of the modules on the small étale site, which is the structure sheaf viewed as a module over itself on the nose (modulesTensorUnit_eq). DISCHARGED: the component cycle is the constructed canonicalFirstChernRule, not a parameter, and no section of O_X|_W is chosen; proved from the first assertion at L = N = O_X, the invertibility of the tensor unit, the right unitor O_X ⊗ O_X ≅ O_X and the isomorphism invariance canonicalFirstChernCap_congr_iso. CORRECTED: stated for α ∈ Z_{k+1}(X), the source's Z_{k-1}(X) being a slip”.

c₁(𝒪_X) ∩ α = 0 in CH_k(X) for every α ∈ Z_{k+1}(X), the structure sheaf being the tensor unit of AlgebraicGeometry.Space.Modules, which is 𝒪_X as a module over itself.

theorem canonicalFirstChernCap_tensorUnit_eq_zero (k : ℤ) (α : CycleGroup D sX (k + 1)) :
    canonicalFirstChernCap.{u, u + 1} D sX hX
      (𝟙_ (Modules.{u, u} D.site D.base D.base_mem X hX.1))
      (isInvertibleModule_tensorUnit hX) k α = 0

AlgebraicGeometry.Space.firstChernClassCap_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FirstChernClassCapAdditive.lean, line 543. The attribute's comment: “first assertion: c_1(L) ∩ α + c_1(N) ∩ α = c_1(L ⊗ N) ∩ α in CH_k(X), for the cap product of Stacks 0EQJ as carried in this repository — so the component cycle c_1(L|_W) ∩ [W] and the Chow group CH_k(X) remain explicit parameters, standing in for Stacks 0EQE and Stacks 0EQ6 parts (2)-(4), neither of which exists for algebraic spaces here. QUALIFIED: carried as explicit named hypotheses are (i) that each of the three component rules is the Weil divisor div_{L|_W}(s) of a meromorphic section, which is the definition of Stacks 0EQE, and (ii) that the ratio of the third section at the generic point of every prime divisor is the product of the ratios of the first two, which stands in for M = L ⊗ N and st = s·t because this repository has neither the tensor product of sheaves of modules on an algebraic space nor the product of meromorphic sections — this is the hypothesis shape of the carried Stacks 0EPV. Proved on top of those: the additivity of the component cycles, from Stacks 0EPV, and the additivity of the cap product, from it. Neither side of the equality, and no conjunct of it, is a hypothesis. CORRECTED: the source writes α ∈ Z_{k-1}(X), which cannot give an identity in CH_k(X) for the operation Z_{k+1}(X) → CH_k(X) of Stacks 0EQJ; stated here for α ∈ Z_{k+1}(X), as the identical scheme-side lemma Stacks 02SP does”.

Stacks 0EQK, first assertion. Additivity of the first Chern class cap product. For invertible sheaves ℒ and 𝒩 on a good algebraic space X/B and every α ∈ Z_{k+1}(X),

c₁(ℒ) ∩ α + c₁(𝒩) ∩ α = c₁(ℒ ⊗_{O_X} 𝒩) ∩ α in CH_k(X).

The cap product is the carried Stacks 0EQJ, AlgebraicGeometry.Space.firstChernClassCap, whose component cycle and Chow group are explicit parameters; the three component rules here are its parameters for the three sheaves, and the Chow group CH is shared.

Nothing about the conclusion is assumed. Each of the three component rules is assumed only to be presented by the Weil divisor of a meromorphic section of its own sheaf, which is the definition Stacks 0EQE would supply, and the hypothesis hst is the source's own step that s_ξ ⊗ t_ξ generates (ℒ ⊗ 𝒩)_ξ, so that st/(s_ξ t_ξ) = (s/s_ξ)(t/t_ξ). Additivity of the component cycles is then Stacks 0EPV, and additivity of the cap product follows from it by the extension of Stacks 0EQJ, case (2).

theorem firstChernClassCap_tensor
    {L N M : Modules.{u, u} D.site D.base D.base_mem X hX.1}
    (hL : IsInvertibleSheaf D sX hX L) (hN : IsInvertibleSheaf D sX hX N)
    (hM : IsInvertibleSheaf D sX hX M)
    {chernL chernN chernM : FirstChernComponentCycleRule D sX k}
    {CH : Type w} [AddCommGroup CH] (chow : ChowTarget.{u, w, v} D sX hX k CH)
    (dL : ComponentDivisorData sX k setup chernL)
    (dN : ComponentDivisorData sX k setup chernN)
    (dM : ComponentDivisorData sX k setup chernM)
    (hst : ∀ (W : IntegralClosedSubspace D.site D.base D.base_mem X)
      (P : PrimeDivisor D.site D.base D.base_mem W.subspace.toFunctor),
      (dM.ratio W P (dM.sect W) :
          P.genericTotalFractionRing D.site D.base D.base_mem (setup.isSpace W)
            (setup.isDecent W)) =
        (dL.ratio W P (dL.sect W) :
            P.genericTotalFractionRing D.site D.base D.base_mem (setup.isSpace W)
              (setup.isDecent W)) *
          (dN.ratio W P (dN.sect W) :
            P.genericTotalFractionRing D.site D.base D.base_mem (setup.isSpace W)
              (setup.isDecent W)))
    (α : CycleGroup D sX (k + 1)) :
    firstChernClassCap D sX hX L k hL chernL chow α +
        firstChernClassCap D sX hX N k hN chernN chow α =
      firstChernClassCap D sX hX M k hM chernM chow α

AlgebraicGeometry.Space.firstChernClassCap_structureSheaf_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FirstChernClassCapAdditive.lean, line 596. The attribute's comment: “second assertion: c_1(O_X) ∩ α = 0 in CH_k(X), for the cap product of Stacks 0EQJ as carried in this repository — so the component cycle and the Chow group CH_k(X) remain explicit parameters, standing in for Stacks 0EQE and Stacks 0EQ6 parts (2)-(4). QUALIFIED: carried as explicit named hypotheses are (i) that the component rule is the Weil divisor div_{O_X|_W}(s) of a meromorphic section, the definition of Stacks 0EQE, and (ii) that the ratio of that section against the chosen generator is a unit of the henselian local ring at the generic point of every prime divisor, which is the source's 1 restricting to an everywhere nonzero section of O_X|_W — the structure sheaf itself is not named because this repository has no tensor-unit sheaf of modules on an algebraic space. Proved on top of those: that every component cycle vanishes, from the order of vanishing of a unit being zero, and that the cap product vanishes, from that. The conclusion is not a hypothesis”.

Stacks 0EQK, second assertion. c₁(O_X) ∩ α = 0 for every α ∈ Z_{k+1}(X).

The source's proof: the global section 1 of O_X restricts, on an integral closed subspace W ⊆ X, to an everywhere nonzero section of O_X|_W, so c₁(O_X|_W) ∩ [W] = 0. Here the hypothesis hunit is that everywhere nonzero section: a nowhere vanishing section generates, so its ratio against the chosen generator at the generic point of a prime divisor is a unit of the henselian local ring there, and the order of vanishing of a unit is zero. That the component cycles all vanish is then proved, not assumed, and the vanishing of the cap product follows from it.

theorem firstChernClassCap_structureSheaf_eq_zero
    {L : Modules.{u, u} D.site D.base D.base_mem X hX.1} (hL : IsInvertibleSheaf D sX hX L)
    {chern : FirstChernComponentCycleRule D sX k}
    {CH : Type w} [AddCommGroup CH] (chow : ChowTarget.{u, w, v} D sX hX k CH)
    (d : ComponentDivisorData sX k setup chern)
    (hunit : ∀ (W : IntegralClosedSubspace D.site D.base D.base_mem X)
      (P : PrimeDivisor D.site D.base D.base_mem W.subspace.toFunctor),
      ∃ vP : ↥(P.genericHenselianLocalRing D.site D.base D.base_mem (setup.isSpace W)
        (setup.isDecent W)), IsUnit vP ∧
        (d.ratio W P (d.sect W) :
            P.genericTotalFractionRing D.site D.base D.base_mem (setup.isSpace W)
              (setup.isDecent W)) =
          algebraMap
            ↥(P.genericHenselianLocalRing D.site D.base D.base_mem (setup.isSpace W)
              (setup.isDecent W))
            (P.genericTotalFractionRing D.site D.base D.base_mem (setup.isSpace W)
              (setup.isDecent W)) vP)
    (α : CycleGroup D sX (k + 1)) :
    firstChernClassCap D sX hX L k hL chern chow α = 0
Tag 0EQL, a lemma

Tag 0EQL in the Stacks Project.

AlgebraicGeometry.Space.componentZeroCycleSumCoeff, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/FirstChernClassCap.lean, line 682. The attribute's comment: “RIGHT-HAND SIDE ONLY — the equality of 0EQM is NOT formalized here, see cycleCoeffOfClosedSubspace_vanishingLocus_eq_componentZeroCycleSumCoeff: the sum ∑ n_i [Z(s_i)]_k as a coefficient family on the integral closed subspaces of X, over the irreducible components X_i of X of δ-dimension k+1, of the pushforward along X_i → X of the cycle [Z(s|_{X_i})]_k of Stacks 0EE9, weighted by the coefficient n_i of X_i in [X]_{k+1} = [O_X]_{k+1}; the restriction s|_{X_i} is the inverse image of Stacks 03LU and Z(s|_{X_i}) its zero scheme of Stacks 0845, both on X_i; the geometric representatives of the generic points are the arguments γ and γW, as throughout this library, Lemma 0EE1 being absent from it”.

Stacks 0EQL, the right-hand side. The coefficient family of the k-cycle ∑ n_i [Z(s|_{X_i})]_k on X: the sum, over the irreducible components X_i ⊆ X of δ-dimension k + 1, of the pushforward along X_i → X of the cycle of the zero scheme of s|_{X_i}, weighted by the multiplicity n_i of X_i in the fundamental cycle [X]_{k+1}.

The sum is a finite sum at every integral closed subspace of X, by AlgebraicGeometry.Space.hasFiniteSupport_componentZeroCycleSumCoeff.

def componentZeroCycleSumCoeff
    (γ : Space.points D.site D.base D.base_mem X →
      GeometricPoint D.site D.base D.base_mem X)
    (γW : ComponentGeometricRepresentatives D sX hX L s k)
    (Z : IntegralClosedSubspace D.site D.base D.base_mem X) : ℤ

AlgebraicGeometry.Space.cycleCoeffOfClosedSubspace_zeroScheme_eq_componentZeroCycleSumCoeff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ZeroSchemeChartGeneralChart.lean, line 290. The attribute's comment: “equation 82.18.3.1, which is Stacks 0EQM, is the conclusion: the coefficient family of [Z(s)]_k of Stacks 0EE9 equals componentZeroCycleSumCoeff, the sum over the irreducible components X_i of X of δ-dimension k+1 of the pushforward along X_i → X of [Z(s|_{X_i})]_k weighted by the coefficient n_i of X_i in [X]_{k+1}. The geometric representatives of the generic points are the parameters γ, γW, γZ, as throughout this library, Lemma 0EE1 being absent from it; the equality holds for every choice of them. The definition of the right-hand side is componentZeroCycleSumCoeff (StacksFrontier/AlgebraicGeometry/Spaces/Chow/FirstChernClassCap.lean)”.

Stacks 0EQL. In Situation 0EDT let X/B be good, let ℒ be an invertible 𝒪_X-module, let s ∈ Γ(X, ℒ) be a regular section and assume dim_δ(X) ≤ k + 1. Write [X]_{k+1} = ∑ n_i [X_i] with X_i the irreducible components of X of δ-dimension k + 1, and s_i = s|_{X_i}. Then

[Z(s)]_k = ∑ n_i [Z(s_i)]_k

as k-cycles on X. This is equation 82.18.3.1, Stacks 0EQM.

The two sides are the coefficient families of AlgebraicGeometry.Space.cycleCoeffOfClosedSubspace at the zero scheme Z(s) of Stacks 0845 and of AlgebraicGeometry.Space.componentZeroCycleSumCoeff; the geometric representatives γ, γW, γZ of the generic points are parameters throughout this library, Lemma 0EE1 being absent from it, and the equality holds for every choice of them.

theorem cycleCoeffOfClosedSubspace_zeroScheme_eq_componentZeroCycleSumCoeff
    (k : ℤ) (hL : IsInvertibleSheaf D sX hX L)
    (hsreg : AlgebraicGeometry.IsRegularSection
      (structureCommRings D.site D.base D.base_mem ⟨X, hX.1⟩)
      (structureRingSheaf D.site D.base D.base_mem ⟨X, hX.1⟩).property s)
    (hdim : deltaDimensionClosed D sX hX Set.univ isClosed_univ ≤ ((k + 1 : ℤ) : EInt))
    (γ : points D.site D.base D.base_mem X → GeometricPoint D.site D.base D.base_mem X)
    (hγ : ∀ x, (γ x).image = x)
    (γW : ComponentGeometricRepresentatives D sX hX L s k)
    (hγW : ∀ (W : ComponentsOfDeltaDimension D sX hX (k + 1)) y, (γW W y).image = y)
    (γZ : points D.site D.base D.base_mem (vanishingLocus D sX hX L s).1.toFunctor →
      GeometricPoint D.site D.base D.base_mem (vanishingLocus D sX hX L s).1.toFunctor)
    (hγZ : ∀ y, (γZ y).image = y) :
    cycleCoeffOfClosedSubspace D sX hX (vanishingLocus D sX hX L s).1
        (vanishingLocus D sX hX L s).2 k γZ =
      componentZeroCycleSumCoeff D sX hX L s k γ γW
Tag 0EQN, a lemma

Tag 0EQN in the Stacks Project.

AlgebraicGeometry.Space.chowClassCanonical_firstChernCapCycleMap_closedSubspaceCycle_eq_vanishingLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/RegularSectionFirstChernCap.lean, line 535. The attribute's comment: “c₁(ℒ) ∩ [Y]_{k+1} = [Z(s)]_k in CH_k(X), for X/B good, ℒ invertible, Y ⊆ X a closed subspace with dim_δ(Y) ≤ k + 1 and s ∈ Γ(Y, ℒ|_Y) a regular section; c₁(ℒ) ∩ - is Stacks 0EQJ at the canonical choices, [Y]_{k+1} and [Z(s)]_k are Stacks 0EE9 (the latter on Y, read on X through Y → X), Z(s) is Stacks 0845 and CH_k(X) is Stacks 0EQ6; nothing carried”.

Stacks 0EQN. In Situation 0EDT let X/B be good and let ℒ be an invertible 𝒪_X-module. Let Y ⊆ X be a closed subspace with dim_δ(Y) ≤ k + 1 and let s ∈ Γ(Y, ℒ|_Y) be a regular section. Then

c₁(ℒ) ∩ [Y]_{k+1} = [Z(s)]_k in CH_k(X).

Here [Y]_{k+1} is the cycle of Stacks 0EE9 of Y on X, AlgebraicGeometry.Space.closedSubspaceCycle; c₁(ℒ) ∩ - is the cap product of Stacks 0EQJ, the cycle-level operation AlgebraicGeometry.Space.firstChernCapCycleMap at the canonical component rule AlgebraicGeometry.Space.canonicalFirstChernRule, its class taken afterwards; Z(s) ⊆ Y is the zero scheme of Stacks 0845, whose k-cycle (defined because dim_δ(Z(s)) ≤ k, AlgebraicGeometry.Space.deltaDimensionSubspace_vanishingLocus_closedSubspaceModuleRestrict_le) is read on X through the inclusion Y → X; and CH_k(X) is the Chow group of Stacks 0EQ6, AlgebraicGeometry.Space.chowGroupCanonical, whose rational equivalences are sums of principal divisors at the canonical embeddings of Stacks 0ENK.

The proof is the source's. Write [Y]_{k+1} = ∑ n_i [Y_i] over the irreducible components Y_i of Y of δ-dimension k + 1. The restriction s_i = s|_{Y_i} is nonzero (AlgebraicGeometry.Space.closedSubspaceComponentImageSection_ne_zero), so by Stacks 0EQF the cycle [Z(s_i)]_k is the Weil divisor of s_i (AlgebraicGeometry.Space.cycleCoeffOfClosedSubspace_vanishingLocus_eq_canonicalDivisorCycleAt), which differs from the component cycle c₁(ℒ|_{Y_i}) ∩ [Y_i] of the cap product by a principal divisor on Y_i at the canonical embeddings (Stacks 0EPT, AlgebraicGeometry.Space.isPrincipalDivisorCycleOfGood_zsmul_canonicalDivisorCycleAt_sub). So c₁(ℒ) ∩ [Y]_{k+1} = ∑ n_i [Z(s_i)]_k in CH_k(X), and the right side is [Z(s)]_k by Stacks 0EQL on Y (cycleCoeffOfClosedSubspace_vanishingLocus_eq_componentZeroCycleSumCoeff_of_isRegularSection), the zero schemes Z(s_i) being inverse images of Z(s) (Stacks 0846).

theorem chowClassCanonical_firstChernCapCycleMap_closedSubspaceCycle_eq_vanishingLocus
    (s : (closedSubspaceModuleRestrict D sX hX L Y).sections)
    (hs : AlgebraicGeometry.IsRegularSection
      (structureCommRings D.site D.base D.base_mem ⟨Y.1.toFunctor, Y.2.1⟩)
      (structureRingSheaf D.site D.base D.base_mem ⟨Y.1.toFunctor, Y.2.1⟩).property s) {k : ℤ}
    (hdim : deltaDimensionSubspace D sX hX Y.1 Y.2 ≤ ((k + 1 : ℤ) : EInt)) :
    chowClassCanonical.{max (u + 1) v} D sX hX k
        (firstChernCapCycleMap D sX hX k (canonicalFirstChernRule D sX hX L hL k)
          (closedSubspaceCycle D sX hX Y.1 Y.2 (k + 1) hdim)) =
      chowClassCanonical.{max (u + 1) v} D sX hX k (closedSubspaceCyclePushforward D sX hX Y k
        (closedSubspaceCycle D (Y.1.ι ≫ sX) (isGood_closedSubspace D sX hX Y)
          (vanishingLocus D (Y.1.ι ≫ sX) (isGood_closedSubspace D sX hX Y)
            (closedSubspaceModuleRestrict D sX hX L Y) s).1
          (vanishingLocus D (Y.1.ι ≫ sX) (isGood_closedSubspace D sX hX Y)
            (closedSubspaceModuleRestrict D sX hX L Y) s).2 k
          (deltaDimensionSubspace_vanishingLocus_closedSubspaceModuleRestrict_le D sX hX L Y hL s
            hs hdim)))
Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.