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:
AlgebraicGeometry.Space.inducedDimensionValue, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Chow/Setup.lean, line 68 (StacksFrontier): “induced_delta”.AlgebraicGeometry.Space.inducedDimensionValue_eq, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Chow/Setup.lean, line 69 (StacksFrontier): “induced_delta”.
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 ofZis 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
Zof a good algebraic space is the δ-dimension ofZ, the value ofδ_{X/B}at the generic point ofZ; 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
Zof a good algebraic space is the δ-dimension ofZ, 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
Zof a good algebraic space at a closed point of|Z|is the δ-dimension ofZ, 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
Zof a good algebraic space at a geometric point above a closed point of|Z|is the δ-dimension ofZ, 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
Zof a good algebraic spaceX/Bis 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 spaceX/Bwhich are cycles — the point sets of the subspaces with nonzero coefficient form a locally finite collection of subsets of|X|— and are of δ-dimensionk— every subspace with nonzero coefficient has δ-dimensionk.
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)ofk-cycles on a good algebraic spaceX/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
Fat a geometric pointx̄isdexactly when the length of the Zariski stalk ofφ^* Fisdat the point of the chart under the chosen lift, for every small étale neighbourhood ofx̄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
Fat a geometric pointx̄isdexactly when the length of the Zariski stalk ofφ^* Fisdat the point of the chart under the chosen lift, for some small étale neighbourhood ofx̄whose chart is a scheme.Together with
AlgebraicGeometry.Space.geometricLength_eq_iff_forall_etaleChartthis 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
Fbe a quasi-coherent𝒪_X-module and letx̄andȳbe geometric points ofXlying over the same pointxof|X|. ThenFhas the same length atx̄as atȳ. So the length of Stacks 0EE2 is a function ofx, 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}ofAlgebraicGeometry.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
xof|X|: conditions (1), (2) and (3) are equivalent. For a quasi-coherent𝒪_X-moduleF, a pointx ∈ |X|andd ∈ ℕ∞, the following are equivalent:
length_{𝒪_{X, x̄}} F_{x̄} = dfor a geometric pointx̄abovex;- for some étale morphism
U → XwithUa scheme andu ∈ Umapping tox,length_{𝒪_{U, u}} (F|_U)_u = d;- for every étale morphism
U → XwithUa scheme andu ∈ Umapping tox,length_{𝒪_{U, u}} (F|_U)_u = d.Condition (1) is
AlgebraicGeometry.Space.HasLengthAtby definition, so this is the statement thatAlgebraicGeometry.Space.HasLengthAtis "the equivalent conditions of Lemma 0EE1", as Stacks 0EE2 has it. Together withAlgebraicGeometry.Space.geometricLength_eq_of_image_eq(condition (1) does not depend on the geometric point chosen abovex) 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 spaceXover a schemeS, a geometric pointx̄ofXand an𝒪_X-moduleF, this is the length of the stalkF_{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 "
Fhas lengthdat a pointxof|X|" to mean that this value isdfor a geometric point abovex, which by Stacks 0EE1 does not depend on the choice — proved, for a quasi-coherentF, asAlgebraicGeometry.Space.geometricLength_eq_of_image_eqinGeometricLengthPointIndependence.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:
Fhas lengthdatx. For a quasi-coherent𝒪_X-moduleF, a pointxof|X|andd ∈ ℕ∞, this says that the stalkF_{x̄}has lengthdover the étale local ring𝒪_{X, x̄}for a geometric pointx̄ofXlying overx.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 somex̄abovexiff for every one:AlgebraicGeometry.Space.hasLengthAt_iff_forall_geometricPoint) and is equivalent to conditions (2) and (3), the length of(F|_U)_uover𝒪_{U, u}for some, respectively every, étaleU → Xfrom a scheme andu ∈ Uoverx(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 ⟶ Ybe a closed immersion of algebraic spaces over a schemeS, letGbe an𝒪_X-module and letx̄be a geometric point ofX. Thenf_*Ghas the same length atf(x̄)asGhas atx̄.The germ map
𝒪_{Y, f(x̄)} → 𝒪_{X, x̄}of a closed immersion is surjective (AlgebraicGeometry.Space.surjective_etaleLocalRingMap_of_isClosedImmersion) and the stalk off_*Gatf(x̄)is the stalk ofGatx̄semilinearly over it (AlgebraicGeometry.Space.geometricStalkPushforwardAddEquiv), soAlgebraicGeometry.Space.geometricLength_eq_of_surjective_of_addEquivapplies: restriction of scalars along a surjection does not change the lattice of submodules, hence not its length.No quasi-coherence of
Gis 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
dinℕ∞ = {0, 1, 2, …, ∞}, the moduleGhas lengthdat the geometric pointx̄ofXexactly whenf_*Ghas lengthdatf(x̄).This is
AlgebraicGeometry.Space.geometricLength_chartDirectImageread 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 ⟶ Ybe a closed immersion of algebraic spaces over a schemeS, letGbe a quasi-coherent𝒪_X-module, letpbe a point of|X|with imagef(p)in|Y|and letdbe an element ofℕ∞ = {0, 1, 2, …, ∞}. ThenGhas lengthdatpif and only iff_*Ghas lengthdatf(p)."Has length
dat a point" is the condition of Stacks 0EE2: the length of the module at that point of the space,AlgebraicGeometry.Space.lengthAtPoint, isd. Both sides are therefore= dfor one and the same number, byAlgebraicGeometry.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 moduleGhas lengthdatzif and only ifi_* Ghas lengthdat the imagei(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
Sis 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
Xbe a locally Noetherian algebraic space overS, letFbe a coherent𝒪_X-module and letx ∈ |X|. The following are equivalent:
- for some étale morphism
U → XwithUa scheme and someu ∈ Umapping tox, the pointuis a generic point of an irreducible component ofSupp(F|_U);- for every étale morphism
U → XwithUa scheme and everyu ∈ Umapping tox, the pointuis a generic point of an irreducible component ofSupp(F|_U);- the length of
Fatxis finite and nonzero.The étale morphisms from schemes are the étale scheme charts
WofX, andumaps toxwhenAlgebraicGeometry.Space.chartSchemeToPointssends it tox. The length ofFatxis the length of Stacks 0EE2: the length at a geometric point abovex, 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 abovex.Each chart point above
xsatisfies the chart condition exactly when the length is finite and nonzero (AlgebraicGeometry.Space.exists_isGenericPoint_supp_restrictToChart_iff_geometricLength), and a chart point abovexexists.
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
Xbe a locally Noetherian algebraic space overSwhich is decent (equivalently, byAlgebraicGeometry.Space.isDecentSpace_iff_isAbsolutelyQuasiSeparated_of_isLocallyNoetherian, quasi-separated), letFbe a coherent𝒪_X-module and letx ∈ |X|. The three conditions ofAlgebraicGeometry.Space.tfae_isGenericPoint_supp_restrictToChart_geometricLengthare also equivalent to
xis a generic point of an irreducible component ofSupp(F).The support of
Fis 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 abovex(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
YoverSis 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
YoverSis the generic point of a subspaceZwhen it is the generic point of the set of points ofZ.
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/Bbe good, letY ⊆ Xbe a closed subspace and assumedim_δ(Y) ≤ k. Thek-cycle associated toYis[Y]_k = ∑ m_{Z, Y} [Z], the sum over the irreducible componentsZofYof δ-dimensionk, withm_{Z, Y}the multiplicity ofZinY; as an element ofZ_k(X)it is the coefficient familyAlgebraicGeometry.Space.cycleCoeffOfClosedSubspaceat 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 subspaceW ⊆ Yin a closed subspaceY ⊆ X: the length of𝒪_Yat the generic point ofW, read insideY, at a geometric representative of that generic point.This is the coefficient the sum of part (2) attaches to
W, asAlgebraicGeometry.Space.closedSubspaceCycle_apply_eq_finsumrecords. The representative used isAlgebraicGeometry.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 ⊆ Xin an𝒪_X-moduleF: the length ofFat the generic pointξofZ, in the sense of Stacks 0EE2, read at the geometric point thatγassigns toξ.The source defines this when
|Z|is an irreducible component ofSupp(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 isAlgebraicGeometry.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/Bbe good, letFbe a coherent𝒪_X-module and assumedim_δ(Supp(F)) ≤ k. Thek-cycle associated toFis
[F]_k = ∑ m_{Z, F} [Z],the sum over the integral closed subspaces
Z ⊆ Xwhose set of points is an irreducible component ofSupp(F)of δ-dimensionk, withm_{Z, F}the multiplicity of part (1).As an element of
Z_k(X)this is the coefficient familyAlgebraicGeometry.Space.cycleCoeffOfModule, which assignsm_{Z, F}to eachZof δ-dimensionk: off the support the multiplicity already vanishes, andAlgebraicGeometry.Space.exists_irreducibleComponents_of_cycleCoeffOfModule_ne_zeroshows that the subspaces left with a nonzero coefficient are exactly the components ofSupp(F)of δ-dimensionk, so the family is the displayed sum. That it is ak-cycle at all is Stacks 0EE5, byAlgebraicGeometry.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/Bbe good, letFbe a coherent𝒪_X-module withdim_δ(Supp(F)) ≤ k, and letZbe an integral closed subspace ofXwithdim_δ(Z) = kand generic pointξ. Then the coefficient ofZin[F]_kis the length ofFatξ.The generic point is
AlgebraicGeometry.Space.IntegralClosedSubspace.ambientGenericPoint, which is a generic point of|Z|byAlgebraicGeometry.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 ofSupp(F): the source reaches that case from the dichotomy that|Z|is such a component exactly whenξlies inSupp(F), off which the length vanishes, and both halves of it are already recorded here, asAlgebraicGeometry.Space.exists_irreducibleComponents_of_cycleCoeffOfModule_ne_zeroandAlgebraicGeometry.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 letX/Bbe good, letY ⊂ Xbe a closed subspace with inclusioni : Y → X, assumedim_δ(Y) ≤ k, and letWbe an integral closed subspace ofYwith imageZ ⊂ X. Then the coefficient ofZin[Y]_kis the coefficient ofZin[i_*𝒪_Y]_k.The chosen geometric representatives
γYandγXare each assumed to lie over the point they are assigned to, whichAlgebraicGeometry.Space.exists_compatible_geometricRepresentativeshows is possible; the content is then Stacks 0EE3, by way ofAlgebraicGeometry.Space.geometricLength_closedSubspacePushforwardStructureSheaf, together with Stacks 0EE1 to move fromγXat the image of the generic point ofWto the geometric pointi(γY(ξ_W))that the comparison with𝒪_Yis 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/Bbe good, letY ⊂ Xbe a closed subspace with inclusioni : Y → X, and assumedim_δ(Y) ≤ k. Then[Y]_k = [i_*𝒪_Y]_k, as an equality of coefficient families on the integral closed subspaces ofX.For an integral closed subspace
Zwith image contained in|Y|this isAlgebraicGeometry.Space.cycleCoeffOfClosedSubspace_eq_cycleCoeffOfModule. Otherwise both sides vanish: the left byAlgebraicGeometry.Space.cycleCoeffOfClosedSubspace_eq_zero, and the right becausei_*𝒪_Yis annihilated by the ideal cutting outY(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 ofZis such a point exactly when no integral closed subspace ofYhas imageZ, sinceYis a decent space (AlgebraicGeometry.Space.isDecentSpace_of_relativelyRepresentable) and every integral closed subspace ofXcontained 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/Bbe good and let0 → F → G → H → 0be a short exact sequence of coherent𝒪_X-modules whose three supports have δ-dimension at mostk. 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 δ-dimensionk; at the subspaces of other δ-dimension all three coefficients vanish.Cycle coefficients are integers, reached from the
ℕ∞-valued multiplicity byENat.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 δ-dimensionk. 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
XandYbe good algebraic spaces over the base and letf : X ⟶ Ybe a morphism over the base. For an integral closed subspaceZ ⊂ Xthere is exactly one integral closed subspaceZ' ⊂ Yadmitting a morphismZ ⟶ Z'overf— that is, one making the square withZ ⟶ X,Z' ⟶ Yandfcommute — which is dominant; and iffis 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.closureImageatf, the integral closed subspace ofYon 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 aBaseSpaceDimensionSituationat a pointxof|X|: the field of the monomorphism from a field spectrum representingx.
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
xof a good algebraic space over the base of aBaseSpaceDimensionSituationis represented by the morphismSpec κ(x) ⟶ Xout 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
xof a good algebraic space over the base of aBaseSpaceDimensionSituationis unique: any monomorphic field-valued representative ofxis uniquely isomorphic, over the space, toSpec κ(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
BaseSpaceDimensionSituationhas 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/Bbe good over the base of aBaseSpaceDimensionSituationand letU ⊆ Xbe 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 pointxof|X|coming from a pointuof that scheme, the residue fieldκ(x)agrees with the residue field ofuonUas a scheme: they are isomorphic by an isomorphism whose spectrum is the comparison morphism overX.
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/Bbe good and letXbe integral. Then the function fieldR(X)ofXis defined: the ring of rational functions ofXis 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/Bbe good and letXbe integral. Then the function fieldR(X)ofXis the residue field ofXat 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/Bbe good. For a pointξofXthe residue fieldκ(ξ)is the function field of the unique integral closed subspaceZ ⊆ Xwhose 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
XandYbe good integral algebraic spaces over the fixed base withdim_δ(X) = dim_δ(Y), and letf : X ⟶ Ybe a morphism over the base. Then eitherffactors through a proper closed subspace ofY— namely the integral closed subspace ofYon the closure of the image of|X|, whose set of points is strictly smaller than|Y|— orfis dominant, carries the generic point ofXto the generic point ofY, and the extension of function fieldsR(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
finduces 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|, andXis reduced, soffactors through the integral closed subspace on it by Stacks 03IQ and Stacks 03JJ. If the image is dense, thenfis 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/BandY/Bbe good algebraic spaces over the base of the theory of cycles and letf : X ⟶ Ybe a quasi-compact morphism overB. 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 subspaceZ ⊆ Xoccurs inf_*[Z]: the degree[R(Z) : R(Z')]when the δ-dimension is preserved, and0when 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 ⟶ Yof good algebraic spaces overB: the additive mapf_* : Z_k(X) → Z_k(Y)sending a cycleαto the cycle whose coefficient atZ'is∑ α_Z · [R(Z) : R(Z')], the sum being over the integral closed subspacesZ ⊆ Xwhose image closure isZ'and the degree being taken to be0where the δ-dimension drops. The morphismfis 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
frecords an integral closed subspaceZofXin the cycle group of δ-dimensionk: the degreedeg(Z/Z')ofZover its integral closed imageZ'whendim_δ(Z') = k, and0whendim_δ(Z') < k, which forZof δ-dimensionkis 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
kalong a proper morphismf : X ⟶ Yof good algebraic spaces over the base: the cycle whose coefficient atZ'is the sum ofn_Z deg(Z/Z')over the integral closed subspacesZofXwith integral closed imageZ'of δ-dimensionk.
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 δ-dimensionkis 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 δ-dimensionkwhose integral closed imageZ'again has δ-dimensionkisdeg(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 ⟶ YoverBof integral good algebraic spaces withdim_δ(X) = dim_δ(Y) = n,
f_*[X] = [R(X) : R(Y)] [Y]inZ_n(Y).The whole of
Xis the only integral closed subspace carrying a coefficient of[X], its image closure is the whole ofY, 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 alongf : X ⟶ Yand then alongg : Y ⟶ Wis 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 ⟶ Ybe a proper morphism of good algebraic spaces over the base and letFbe a coherent𝒪_X-module withdim_δ(Supp(F)) ≤ k. Then
f_*[F]_k = [f_*F]_kin
Z_k(Y): the proper pushforward of thek-cycle[F]_kof Stacks 0EEB is thek-cycle whose coefficient at an integral closed subspaceW ⊂ Yof δ-dimensionkis the length off_*Fat the generic point ofW. The cycles of modules are read at chosen geometric representativesγX,γYof the points (by Stacks 0EE1 the lengths do not depend on them). That the coefficient family off_*Fis ak-cycle is part of the statement (AlgebraicGeometry.Space.cycleCoeffOfModule_directImageModule_mem_cyclesOfDimension); the coherence off_*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 ⟶ Ybe a proper morphism of good algebraic spaces over the base and letZ ⊂ Xbe a closed subspace withdim_δ(Z) ≤ k. Then
f_*[Z]_k = [f_*𝒪_Z]_kin
Z_k(Y), where[Z]_kis thek-cycle of Stacks 0EE9 andf_*𝒪_Zis the direct image of the structure sheaf ofZalongZ → X → Y: the proper pushforward of[Z]_kis thek-cycle whose coefficient at an integral closed subspaceW ⊂ Yof δ-dimensionkis the length off_*𝒪_Zat the generic point ofW(read at the chosen geometric representativeγY; by Stacks 0EE1 it does not depend on it). That this coefficient family is ak-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 ⟶ Ybe a flat morphism of good algebraic spaces over the base and letZ ⊆ Ybe an integral closed subspace. An irreducible componentZ'off^{-1}(Z)dominatesZ: 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 ⟶ Ybe a morphism of good algebraic spaces over the base which is flat of relative dimensionr, and letZ ⊆ Ybe an integral closed subspace. An irreducible componentZ'off^{-1}(Z)satisfiesdim_δ(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 ⟶ Ybe a morphism of good algebraic spaces over the base which is flat of relative dimensionr, and letT ⊆ |Y|be a closed set of points whose inverse image is nonempty. Thendim_δ(f^{-1}(T))isrmore than the supremum of the δ-dimensions of the irreducible components ofTwhichfmeets.When
fmeets every component ofT, in particular whenfis surjective, the supremum isdim_δ(T)and the formula readsdim_δ(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
Yunder a morphismf : X ⟶ Yof algebraic spaces overSis closed in the points ofX.
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
Yunder a morphismf : X ⟶ Yof algebraic spaces overSform a locally finite collection of subsets of the points ofX.
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 ⊆ Yof δ-dimensionk: 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 ⟶ Yof good algebraic spaces over the base which is flat of relative dimensionr, as a homomorphismf^* : Z_m(Y) →+ Z_n(X)form + 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 ⟶ Yof good algebraic spaces over the base which is flat of relative dimensionr, as an inhabitant of the bundledAlgebraicGeometry.Space.FlatCyclePullback: the multiplicities of the inverse images, the homomorphismsZ_m(Y) →+ Z_n(X)form + r = n, the defining formula relating them, and the containment of the support off^*[W]inf^{-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 letX/Bbe good, leti : Y ⟶ Xbe a closed immersion over the base and letj : U ⟶ Xbe an open immersion over the base whose image is the complement of the image ofi. Ak-cycle onXrestricts to zero onUexactly when it is the pushforward of ak-cycle onY.
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 letX/BandU/Bbe good and letj : U ⟶ Xbe an open immersion over the base. Everyk-cycle onUis the restriction of ak-cycle onX, 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 ⟶ Ybe an étale morphism of good algebraic spaces over the base of Situation 0EDT and letZ ⊆ Ybe an integral closed subspace. The formal sum of the irreducible components of the inverse image ofZ, each with coefficient one, is a cycle of the δ-dimension ofZonX.The components are integral closed subspaces of
X, they form a locally finite family, and each of them has the δ-dimension ofZ; these are exactly the two conditions definingZ_{δ(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 ⟶ Ybe an étale morphism of good algebraic spaces over the baseBof Situation 0EDT and letZ ⊆ Ybe an integral closed subspace, of δ-dimensionm. Then
f^*[Z] = ∑ [Z'],the sum running over the irreducible components
Z'of the inverse imagef^{-1}(Z)(in the sense of Remark 0EE8), each with coefficient one: the coefficient family of the cyclef^*[Z]is the formal sumAlgebraicGeometry.Space.IntegralClosedSubspace.preimageComponentsCycleof those components.The left-hand side is the flat pullback
AlgebraicGeometry.Space.flatPullbackMapof Stacks 0EP8 at relative dimension0, which an étale morphism has byAlgebraicGeometry.Space.hasRelativeDimension_zero_of_isEtale, applied to the cycle[Z]; the pullback lands in degreenfor anynwithm + 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/BandZ/Bbe good algebraic spaces over the base ofDand letf : X ⟶ Yandg : Y ⟶ Zbe morphisms over the base which are flat of relative dimensionsrands. Then the compositef ≫ gis flat of relative dimensionr + s: it is locally of finite type, flat, and of relative dimensionr + 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/BandZ/Bbe good and letf : X ⟶ Yandg : Y ⟶ Zbe morphisms over the base which are flat of relative dimensionsrands. Then
g ∘ fis flat of relative dimensionr + s(and locally of finite type), andf^* ∘ g^* = (g ∘ f)^*as mapsZ_k(Z) → Z_{k+r+s}(X), for everyk.The degree of the target is any
nwithk + (r + s) = n, which is howAlgebraicGeometry.Space.flatPullbackMapis graded. The flat pullback alongg ∘ fin 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/BandY/Bbe good and letf : X ⟶ Ybe a morphism over the base which is flat of relative dimensionr. LetZ ⊆ Ybe a closed subspace withdim_δ(Z) ≤ k. Thendim_δ(f^{-1}(Z)) ≤ k + rand
[f^{-1}(Z)]_{k+r} = f^*[Z]_kinZ_{k+r}(X).The cycle of a closed subspace is
AlgebraicGeometry.Space.closedSubspaceCycle(Stacks 0EE9) and the flat pullback isAlgebraicGeometry.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/BandY/Bbe good and letf : X ⟶ Ybe a morphism over the base which is flat of relative dimensionr. LetFbe a coherent𝒪_Y-module withdim_δ(Supp(F)) ≤ k. Thendim_δ(Supp(f^*F)) ≤ k + rand
f^*[F]_k = [f^*F]_{k+r}inZ_{k+r}(X).The cycle of a coherent module is
AlgebraicGeometry.Space.associatedCycle(Stacks 0EEB), read at any choiceγ_X,γ_Yof geometric points over the points ofXandY; the pullbackf^*Fis coherent byAlgebraicGeometry.Space.isCoherent_modulePullback,Xbeing 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
Sthe base changef'of a proper morphismfis 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
Bbe good and letg : Y' ⟶ Ybe a morphism overBwhich is flat of relative dimensionr. Then the base changeg' : X' ⟶ Xis flat of relative dimensionr: it is locally of finite type, flat, and of relative dimensionr.Local finite type of
g'is goodness ofX'/Band the cancellation of Stacks 0462 applied tog' ≫ sX = sX', flatness is Stacks 03MO, and the relative dimension isAlgebraicGeometry.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
Bbe good, letf : X ⟶ Ybe proper and letg : Y' ⟶ Ybe flat of relative dimensionr. Then for everyk-cycleαonX
g^*f_*α = f'_*(g')^*αin
Z_{k+r}(Y').Nothing is carried. The pushforward along
f'is legitimate becausef'is proper, which is the first assertionAlgebraicGeometry.Space.isProper_of_isPullbackand appears in the statement; the pullback alongg'is legitimate becauseg'is flat of relative dimensionr, which is the second assertionAlgebraicGeometry.Space.isFlat_and_hasRelativeDimension_of_isPullbackand is written out as the hypotheseshg'flatandhg'rso 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 isSpace.BaseChangeDegreeCount.properCycleDegree_mul_flatPullbackMult_eq_finsum_of_isProperofStacksFrontier.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 ofg^*f_*[Z]atT', byAlgebraicGeometry.Space.finsum_properCycleMult_mul_flatPullbackMult. The count is bundled intoAlgebraicGeometry.Space.ProperFlatBaseChangeComparisonand handed toAlgebraicGeometry.Space.flatPullback_properPushforwardabove, 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')^*αinZ_{k+r}(Y'), for a cartesian square of good algebraic spaces overBwithfproper andgflat of relative dimensionr, and for an arbitraryk-cycleαonX.
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---> Ybe a cartesian square of good algebraic spaces over
B, letf : X ⟶ Ybe proper and letg : Y' ⟶ Ybe flat of relative dimensionr. Then for everyk-cycleαonX
g^*f_*α = f'_*(g')^*αin
Z_{k+r}(Y').Nothing is assumed: the pushforward along
f'is legitimate becausef'is proper, which is the first assertionAlgebraicGeometry.Space.isProper_of_isPullback; the pullback alongg'is legitimate becauseg'is flat of relative dimensionr, which is the second assertionAlgebraicGeometry.Space.isFlat_and_hasRelativeDimension_of_isPullback; and both are written out in the statement rather than carried. The identity itself isAlgebraicGeometry.Space.flatPullback_properPushforward, whose comparison at the generic points isAlgebraicGeometry.Space.properFlatBaseChangeComparison.A
CycleGroupis never transported along an equality of degrees, so the identity is stated at a pairk,nwithk + r = nand the degree equality as an explicit argument, which is the convention ofAlgebraicGeometry.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/BandY/Bbe good and letf : X ⟶ Ybe finite locally free of degreed. Then
f_*f^*α = dαfor every
α ∈ Z_k(Y), withf^*the flat pullback of Stacks 0EP8 (AlgebraicGeometry.Space.finiteLocallyFreeCyclePullback, whose flatness and relative-dimension hypotheses are the second conclusion of Stacks 0EPE) andf_*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
dof algebraic spaces overSis 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
dof algebraic spaces overSis flat of relative dimension0: it is flat and locally of finite type, and has relative dimension0at 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/BandY/Bbe good and letf : X ⟶ Ybe finite locally free of degreed. Thenf_*f^*α = dαfor everyα ∈ Z_k(Y).Only the term of the flat pullback at
W'itself survives in the coefficient off_*f^*αat an integral closed subspaceW' ⊆ Y, byAlgebraicGeometry.Space.eq_cycleImageSubspace_of_mult_ne_zero, and what is left isα_{W'}times the degreehdegof the fibre over the generic point ofW'; at aW'of δ-dimension other thankthe 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
Sis 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
Sis flat of relative dimension0: it is flat and locally of finite type, and has relative dimension0at 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/BandY/Bbe good and letf : X ⟶ Ybe finite locally free, withhdegrecording the degreedof its fibre over the generic point of every integral closed subspace of δ-dimensionk. Thenf_*f^*α = dαfor everyα ∈ Z_k(Y).Only the term of the flat pullback at
W'itself survives in the coefficient off_*f^*αat an integral closed subspaceW' ⊆ Y, byAlgebraicGeometry.Space.eq_cycleImageSubspace_of_mult_ne_zero, and what is left isα_{W'}times the degreehdegof the fibre over the generic point ofW'; at aW'of δ-dimension other thankthe 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 degreedis pinned byhdegalone.
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/Bbe good and assumeXintegral withdim_δ(X) = n. IfZis an irreducible component of an effective Cartier divisorD ⊆ X, thendim_δ(Z) = n - 1.The component is presented by a generic point
ξof an irreducible componentWof the closed subset|D| ⊆ |X|, anddim_δ(Z)is theδ-dimension of Stacks 0EDX of the irreducible closed subsetclosure {ξ}of|X|, the summandWcontributes todim_δ(D).By part (1) the equality is equivalent to the component having codimension one in
|X|, which isAlgebraicGeometry.Space.codimension_closureSingleton_eq_one_of_isEffectiveCartierDivisor; the passage between the two is the topological equivalencecodimension_closureSingleton_eq_one_iff_dimensionFunctionfor the dimension functionδ_{X/B}of Stacks 0EDN, which is where integrality ofXanddim_δ(X) = nare 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/Bbe good and assumeXintegral withdim_δ(X) = n. For an integral closed subspaceZ ⊆ Xthe following are equivalent:Zis a prime divisor ofX; the set of points ofZhas codimension one in|X|; anddim_δ(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 goodX/Bis 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/Bbe good and assumeXintegral withdim_δ(X) = n. For an integral closed subspaceZ ⊆ Xthe following are equivalent:Zis a prime divisor ofX; the set of points ofZhas codimension one in|X|; anddim_δ(Z) = n - 1.This is an alias of
AlgebraicGeometry.Space.isPrimeDivisor_tfae, which is proved at these hypotheses inStacksFrontier.AlgebraicGeometry.Spaces.Chow.PrimeDivisorDeltaDimension. The bundled dimension function on|X|with underlying functionδ_{X/B}that the engineAlgebraicGeometry.Space.isPrimeDivisor_tfae_of_isIntegralSpacetakes is produced from goodness ofX/Bby 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 goodX/Bis 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 isdiv(f) = ∑_Z ord_Z(f) [Z], as an element ofZ_{n-1}(X)forX/Bgood and integral withdim_δ(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 anXhas δ-dimensionn - 1by Stacks 0EPZ. Local finiteness is Stacks 0ENN, the argumenthfin, whichAlgebraicGeometry.Space.principalDivisorCycleOfRegularLocusdischarges.
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 functionf ∈ R(X)^*as an element ofZ_{n-1}(X), with the local finiteness of Stacks 0ENN proved from a nonempty open subset of|X|over whichfis 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 ofZ_{n-1}(X), forX/Bgood and integral withdim_δ(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 ⟶ Ybe an étale morphism of good algebraic spaces overB, letYbe integral withdim_δ(Y) = nand letg ∈ R(Y)^*. Then the identity of cycles onX
f^*(div_Y(g)) = ∑_{X'} (X' → X)_* div_{X'}(g ∘ f|_{X'}),the sum being over the irreducible components
X'ofX(Remark 0EE8), holds at every integral closed subspaceZ ⊆ X, coefficientwise, if and only if it holds at those of δ-dimensionn - 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 ⟶ Ybe an étale morphism of good algebraic spaces overB, letYbe integral withdim_δ(Y) = nand letg ∈ R(Y)^*. Then the identity of cycles onX
f^*(div_Y(g)) = ∑_{X'} (X' → X)_* div_{X'}(g ∘ f|_{X'}),read coefficientwise over the irreducible components
X'ofX(Remark 0EE8), holds if and only if at every integral closed subspaceZ ⊆ Xof δ-dimensionn - 1
∑_{X'} ord_Z(g ∘ f|_{X'}) = ord_{Z'}(g),
Z'being the image ofZinY. 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 makesdiv_{X'}(g ∘ f|_{X'})a cycle at all and which Stacks 0EQ1 takes in the same form onY. In particular the dominance off|_{X'}is proved, not assumed (AlgebraicGeometry.Space.pointsMap_genericPoint_eq_genericPoint_irreducibleComponentSubspace).Two reductions are combined. Away from δ-dimension
n - 1both sides vanish, both being(n-1)-cycles — on the right because every component hasdim_δ(X') = n, the source's second paragraph, which is proved — the reduction ofAlgebraicGeometry.Space.etalePullback_principalDivisorCycle_eq_sum_components_iff, taken here at the canonical embeddings and hence re-run rather than cited. At δ-dimensionn - 1the left-hand side isord_{Z'}(g), which is Lemma 0EPY in the formAlgebraicGeometry.Space.etalePullbackPrincipalDivisorCycle_apply_eq_apply_closureImage, and that holds for an arbitraryX, 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 ⟶ Ybe an étale morphism of good algebraic spaces overB, letYbe integral withdim_δ(Y) = nand letg ∈ R(Y)^*. Then, as cycles onX,
f^*(div_Y(g)) = ∑_{X'} (X' → X)_* div_{X'}(g ∘ f|_{X'}),the sum being over the irreducible components
X'ofX(Remark 0EE8). The identity is read coefficientwise, at every integral closed subspace ofX, because the family of irreducible components is only locally finite and the right-hand side is therefore not a sum inZ_{n-1}(X).Both sides are formed at the canonical embeddings of Stacks 0ENK, on
Yforgand on each componentX'forg ∘ f|_{X'}, so that the two orders of vanishing are read at the same data and are tied to one another throughAlgebraicGeometry.Space.rationalFunctionMap.Nothing beyond the source's own hypotheses goes in. The dominance of
f|_{X'}, the source's first step, isAlgebraicGeometry.Space.pointsMap_genericPoint_eq_genericPoint_irreducibleComponentSubspace;dim_δ(X') = n, the source's second paragraph, isAlgebraicGeometry.Space.deltaDimensionClosed_univ_irreducibleComponentSubspace; and the local finiteness of Stacks 0ENN, onYand on each component, which is what makes each principal divisor a cycle at all, is discharged byAlgebraicGeometry.Space.targetDivisorLocallyFinite_of_isGoodandAlgebraicGeometry.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 letX/BandY/Bbe good, letp : X ⟶ Ybe quasi-compact overB, letXandYbe integral withdim_δ(X) = dim_δ(Y) = n, and letf ∈ R(X)^*andg ∈ R(Y)^*. Then
p_* div(f) = div(g)inZ_{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 subspacesZ ⊆ X.Both sides are coefficient families on the integral closed subspaces of
Y, and away from the prime divisors ofYboth vanish: the coefficient ofdiv(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 byAlgebraicGeometry.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 ofY— which is the mathematical content of Stacks 0EQ4 — is not proved here, and is not assumed either. Takingg = Nm_{R(X)/R(Y)}(f), that isAlgebraicGeometry.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/BandY/Bbe good, letXandYbe integral withn = dim_δ(X) = dim_δ(Y), letp : X ⟶ Ybe a dominant proper morphism, letf ∈ R(X)^*and setg = Nm_{R(X)/R(Y)}(f). Then
p_* div(f) = div(g)inZ_{n-1}(Y).Here
divis the principal divisor of Stacks 0EQ1 (AlgebraicGeometry.Space.rationalFunctionPrincipalDivisorCycle, at the canonical embeddings of Stacks 0ENK),p_*is proper pushforward of cycles (Stacks 0EP2) andgis the normAlgebraicGeometry.Space.rationalFunctionNormalong the extension of function fieldspinduces, as a unit ofR(Y)(AlgebraicGeometry.Space.rationalFunctionNormUnit);R(X)/R(Y)is finite (Stacks 0AD5, fromdim_δ(X) = dim_δ(Y)). Both sides are(n-1)-cycles onY, determined by their coefficients at the prime divisors ofY, where they agree byAlgebraicGeometry.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
Kbe a field,L/Ka finite extension andM/Ka finite separable extension. ThenM ⊗_K Lis a finite product of fields∏ᵢ Mᵢ— concretely, the product of its quotients by its maximal ideals — and fort ∈ Lthe image inMofNm_{L/K}(t)is the product of the norms overMof the imagestᵢof1 ⊗ t:
Nm_{L/K}(t) = ∏ᵢ Nm_{Mᵢ/M}(tᵢ)inM.Separability of
M/Kis what makesM ⊗_K Lreduced, and being also finite-dimensional overMit 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_jof the pushforwards of a family ofk-cycles along the inclusions of a locally finite collection of integral closed subspaces is ak-cycle onX.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 iskbecause 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_jofZ_k(X)determined by a locally finite collection{W_j ⊆ X}of integral closed subspaces and a family ofk-cyclesc_jon them; takingc_j = div(f_j)forf_j ∈ R(W_j)^*on subspaces of δ-dimensionk + 1gives 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 spaceX/Bis 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 withdim_δ(W_j) = k + 1, and on each a principal divisordiv(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 onX, that is the Chow group ofk-cycles modulo rational equivalence,
CH_k(X) = Z_k(X)/∼_rat,the quotient of the group of
k-cycles of a good algebraic spaceX/Bby 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 δ-dimensionk + 1is 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 spaceX/Bis 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 withdim_δ(W_j) = k + 1, and on each a rational functionf_j ∈ R(W_j)^*whose principal divisordiv(f_j)is thej-th summand, the pushforwards summing to the cycle.Each
W_jis good overBbyAlgebraicGeometry.Space.isGood_integralClosedSubspaceand integral by definition, sodiv(f_j)is read at the canonical embeddingsR(W_j) → Q(𝒪^h_{W_j,ξ})of Stacks 0ENK and depends on nothing butf_j: the summand condition isAlgebraicGeometry.Space.IsPrincipalDivisorCycleOfGood. The sum isAlgebraicGeometry.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 onX, that is the group ofk-cycles modulo rational equivalence,
CH_k(X) = Z_k(X)/∼_rat,the quotient of the group of
k-cycles of a good algebraic spaceX/Bby 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 δ-dimensionk + 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/Bbe good, letU ⊆ Xbe an open subspace, letY ⊆ Xbe a closed subspace with|Y| = |X| \ |U|and leti : Y → X,j : U → Xbe the inclusions. Letk ∈ ℤ.
- If
α, β ∈ Z_k(X)satisfyα|_U ∼_rat β|_U, thenα ∼_rat β + i_*γfor someγ ∈ Z_k(Y).- In other words,
CH_k(Y) →[i_*] CH_k(X) →[j^*] CH_k(U) → 0is an exact complex of abelian groups: the kernel ofj^*is the image ofi_*, andj^*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 onT_i. Ifα_i ∼_rat β_ionT_ifor everyi, 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 Ybe a locally finite collection of subsets of a topological space and, for eachi, letW i : J i → Set Ybe a locally finite collection withW i j ⊆ T ifor allj. Then the combined collectionfun ij : Σ i, J i ↦ W ij.1 ij.2is 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 ⟶ Ybe flat, letZ' ⊆ YandZ ⊆ Xbe prime divisors withZlying overZ', letφ : 𝒪^h_{Y,ξ'} ⟶ 𝒪^h_{X,ξ}be the induced flat local homomorphism and letmbe the multiplicity ofZoverZ'. For a rational functiongonYwhose ratio atξ'isa / bwithaandbnonzerodivisors, and for the compositeg ∘ f|_X, whose ratio atξis thereforeφ(a) / φ(b),
ord_Z(g ∘ f|_X) = m · ord_{Z'}(g).The multiplicity
mis the one with whichZoccurs inf^{-1}(Z'), so forXintegral this is the source's identityf^* div_Y(g) = ∑ m_{X',X} (X' ⟶ X)_* div_{X'}(g ∘ f|_{X'})read at the coefficient ofZ; forXwith 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
hmand the whole content — that the order of vanishing multiplies by it — isRing.ord_map_of_flatHom, which is Stacks 02M1 applied to𝒪^h_{Y,ξ'} / aand 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/Bbe good, assumeYintegral withdim_δ(Y) = k, and letf : X ⟶ Ybe a flat morphism overBof relative dimensionr. Then forg ∈ R(Y)^*
f^* div_Y(g) = ∑_{X'} m_{X', X} (X' → X)_* div_{X'}(g ∘ f|_{X'})as
(k + r - 1)-cycles onX: at every integral closed subspaceZ ⊆ Xthe coefficient of the flat pullback (Stacks 0EP8) ofdiv_Y(g)(Stacks 0EQ1) is the sum over the irreducible componentsX'ofXofm_{X', X}, the multiplicity ofX'inX(Stacks 0EE9), times the coefficient atZof the pushforward alongX' → X(Stacks 0EP1) of the principal divisor ofg ∘ 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/Bbe good and letf : X ⟶ Ybe a morphism overBwhich is flat of relative dimensionr. Ifα ∼_rat βare rationally equivalentm-cycles onY, thenf^*α ∼_rat f^*βasn-cycles onX, wherem + r = n.Rational equivalence is that of Stacks 0EQ6 with
div(g)read at the canonical embeddings of Stacks 0ENK (AlgebraicGeometry.Space.RationallyEquivalentCanonical), andf^*is the flat pullback of cycles of Stacks 0EP8 (AlgebraicGeometry.Space.flatPullbackMap). The family presentingα - βis indexed in a universev, the one presentingf^*α - f^*βinmax 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/BandY/Bbe good and letp : X ⟶ Ybe a proper morphism over the base. Ifα, β ∈ Z_k(X)are rationally equivalent, thenp_*αis rationally equivalent top_*β.Rational equivalence is that of Stacks 0EQ6 with the summands
div(f_j)read at the canonical embeddingsR(W_j) → Q(𝒪^h_{W_j,ξ})of Stacks 0ENK (AlgebraicGeometry.Space.RationallyEquivalentCanonical), andp_*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
sofℒ, that isdiv_ℒ(s) = ∑_Z ord_{Z,ℒ}(s) [Z]of Stacks 0EPU, as an element ofZ_{n-1}(X): it is an(n-1)-cycle because a prime divisor of an integral good algebraic space of δ-dimensionnhas δ-dimensionn - 1by Stacks 0EPZ.Local finiteness of the prime divisors with
ord_{Z,ℒ}(s) ≠ 0is Stacks 0EPS, here the hypothesishfin;AlgebraicGeometry.Space.divisorCycleOfSectionOfGeneratingdischarges it from a nonempty open subspace over whichsgeneratesℒ.
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 sectionsofℒas an element ofZ_{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 whichshas nonzero order — the open subspace over whichsgeneratesℒ.
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 isc₁(ℒ) ∩ [X] = [div_ℒ(s)] ∈ CH_{n-1}(X), the class of the Weil divisor of a nonzero meromorphic sectionsofℒ.The class is independent of the chosen section:
AlgebraicGeometry.Space.firstChernClassCapFundamental_eq. The Chow groupCH_{n-1}(X)is the parameterchow, 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
sands'at the generic points of the prime divisors differ by the image of a rational functionf, thendiv_ℒ(s) - div_ℒ(s') = div(f)by Stacks 0EPT, anddiv(f)is rationally equivalent to zero by Stacks 0EQ6: it is the one-member family∑ (i_j)_* div(f_j)of part (1), taken onXitself. Thatdiv(f)is one of the principal divisors of the Chow group parameter is the hypothesishprincipal, 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/Bbe good, letXbe integral withn = dim_δ(X)and letℒbe an invertible𝒪_X-module. The Weil divisor associated to a nonzero meromorphic sectionsofℒ, the(n-1)-cycle
div_ℒ(s) = ∑ ord_{Z,ℒ}(s) [Z] ∈ Z_{n-1}(X),the sum over the prime divisors
ZofX,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/Bbe good, letXbe integral withn = 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
sofℒof Stacks 0EPQ (AlgebraicGeometry.Space.regularMeromorphicSection); the class does not depend on the choice ofs(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 ofdiv_ℒ(s)inCH_{n-1}(X)for every nonzero meromorphic sectionsofℒ.
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)]_klies inZ_k(X).The δ-dimension clause holds by construction, the coefficient of Stacks 0EE9 at an integral closed subspace of δ-dimension other than
kbeing zero. Local finiteness is the argumenthfin, a property of the input datum(ℒ, s, γ), as it is fordiv_ℒ(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 letX/Bbe good, letXbe integral withn = dim_δ(X), letℒbe an invertible𝒪_X-module, lets ∈ Γ(X, ℒ)and letσbe a nonzero meromorphic section ofℒ. Then
div_ℒ(σ) = [Z(s)]_{n-1}inZ_{n-1}(X)holds exactly when it holds coefficientwise at every prime divisor of
X, that is whenord_{Z,ℒ}(σ)is the multiplicity ofZinZ(s)for every prime divisorZ ⊆ X.Both sides are coefficient families on the integral closed subspaces of
X, and away from the prime divisors both vanish: the coefficient ofdiv_ℒ(σ)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 thann - 1by 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 ofs, byAlgebraicGeometry.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 inZ_{n-1}(X). In the situation above, if
div_ℒ(σ) = [Z(s)]_{n-1}inZ_{n-1}(X),which is the first conclusion of the source and the hypothesis
heq, then
c₁(ℒ) ∩ [X] = [Z(s)]_{n-1}inCH_{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 ofdiv_ℒ(σ)for a nonzero meromorphic sectionσofℒ, a class independent ofσbyAlgebraicGeometry.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/Bbe good, letXbe integral withn = dim_δ(X), letℒbe an invertible𝒪_X-module and lets ∈ Γ(X, ℒ)be a nonzero global section. Then
div_ℒ(s) = [Z(s)]_{n-1}inZ_{n-1}(X)andc₁(ℒ) ∩ [X] = [Z(s)]_{n-1}inCH_{n-1}(X).
div_ℒ(s)is the Weil divisor of Stacks 0EQE, part (1), of the meromorphic section ofℒthatsis;c₁(ℒ) ∩ [X]is Stacks 0EQE, part (2), in the Chow groupCH_{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, andsectionWeilDivisor_eq_zeroSchemeCycle_and_weilDivisorOfInvertibleSheaf_eq_of_liesOverstates 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 ofdiv_ℒ(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 morphismg : Y ⟶ Xof good algebraic spaces, letq_Y : T_Y ⟶ Yandα_Y : q_Y^*(g^*ℒ) ≅ 𝒪_{T_Y}be the multiplicative torsor of the invertible𝒪_Y-moduleg^*ℒ. There is a morphismg' : T_Y ⟶ Twithg' ≫ q = q_Y ≫ gsuch that the square is cartesian andαpulls back alongg'toα_Y: the trivializationg'^*αof(g' ≫ q)^*ℒ = (q_Y ≫ g)^*ℒisα_Ycomposed 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/Bbe good and letℒbe an invertible𝒪_X-module. The morphismq : T = \underline{Spec}_X(⨁_{n ∈ ℤ} ℒ^{⊗ n}) ⟶ Xis surjective, smooth, affine, and of relative dimension1.
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 ⊆ Xis a closed subspace ofδ-dimension≤ k, thenq^{-1}(Z)is a closed subspace ofTofδ-dimension≤ k + 1, andq^*[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/Bbe good, letℒbe an invertible𝒪_X-module andq : 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 byqis flat,𝔪^h_{ξ'} = 𝔪^h_ξ 𝒪^h_{T, ξ'}, and the residue field extension is purely transcendental of transcendence degree1: it is generated by a single element transcendental overκ(ξ).The map
φis the one induced byq: it is the local homomorphism agreeing on the image of𝒪_{V, v}with the stalk map of a commuting square of elementary étale neighborhoodsU ⟶ Voverq, 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 ⊆ Xis an integral closed subspace, thenq^{-1}(Z) ⊆ Tis 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}) ⟶ Xof 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
Eit takes is empty there; see the implementation notes above. The assertion under the hypotheses of Situation 0EDT alone isAlgebraicGeometry.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 ⟶ Xalongg : Y ⟶ Xis 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
EandCit 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 ⟶ Xof 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/Bgood 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 ⟶ Ybe the morphism of Stacks 0EQG for an invertible𝒪_Y-moduleℒ, so thatq^*ℒ ≅ 𝒪_Tand a nonzero meromorphic sectionsofℒbecomes a nonzero meromorphic functionq^*(s)onT. LetZ' ⊆ Ybe a prime divisor andZ = 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
hmaxis 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, soRing.ord_map_of_flatHomgives 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/Bbe good and integral withn = dim_δ(X), letℒbe an invertible𝒪_X-module, letsbe a nonzero meromorphic section ofℒ, and letq : T ⟶ Xbe 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 alongq(flat of relative dimension one) of the Weil divisor ofs; on the rightq^*(s)is the pullback ofs, and the identity holds both withdiv_{q^*ℒ}(q^*s)and, for every isomorphismα : q^*ℒ ≅ 𝒪_T, with the divisordiv_{𝒪_T}(α(q^*s))of the meromorphic functionα(q^*s)onT.
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 spaceX/B. It sendsα = ∑ n_W [W]to the class of∑_W n_W i_*(c₁(𝒩|_W) ∩ [W]), wherei : W → Xis the inclusion and the component cyclec₁(𝒩|_W) ∩ [W]isAlgebraicGeometry.Space.canonicalFirstChernRule, the Weil divisordiv_{𝒩|_W}(t_W)of Stacks 0EQE, part (1), at the canonical ratios of Stacks 0EPR for the regular meromorphic section of𝒩|_Wgiven by Stacks 0EPQ. The target is the Chow groupCH_k(X) = Z_k(X)/∼_ratof Stacks 0EQ6, part (4); the pushforwardi_*is applied to the cycle and the class is taken inCH_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 subspacei : W → Xof δ-dimensionk + 1the cap productAlgebraicGeometry.Space.canonicalFirstChernCapis the class ofi_*(c₁(𝒩|_W) ∩ [W]), the inner cycle being the Weil divisordiv_{𝒩|_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 spaceX/B.On the cycle
[W]of an integral closed subspaceW ⊆ Xof δ-dimensionk + 1it is the class ofi_*(c₁(ℒ|_W) ∩ [W]), which is case (1) of the source; seeAlgebraicGeometry.Space.firstChernClassCap_integralCycle. Case (2), the extension of that rule by linearity over an arbitrary(k+1)-cycle, isAlgebraicGeometry.Space.firstChernCapCycleMap, which is proved to land inZ_k(X)and to be additive.The component cycle
c₁(ℒ|_W) ∩ [W]onWand the Chow groupCH_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 ofStacksFrontier.AlgebraicGeometry.Spaces.Chow.FirstChernClassCap. The pushforwardi_*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 subspaceW ⊆ Xof δ-dimensionk + 1the cap product is the class ofi_*(c₁(ℒ|_W) ∩ [W]), for the closed immersioni : W → X.The source applies the proper pushforward
i_* : CH_k(W) ⟶ CH_k(X)to the class ofc₁(ℒ|_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 spaceX/Band everyα ∈ Z_{k+1}(X),
c₁(ℒ) ∩ α + c₁(𝒩) ∩ α = c₁(ℒ ⊗_{𝒪_X} 𝒩) ∩ αinCH_k(X).The cap product is the one of Stacks 0EQJ at the canonical choices,
AlgebraicGeometry.Space.canonicalFirstChernCap, the tensor product isAlgebraicGeometry.Space.picardTensorModule, andCH_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) ∩ α = 0inCH_k(X)for everyα ∈ Z_{k+1}(X), the structure sheaf being the tensor unit ofAlgebraicGeometry.Space.Modules, which is𝒪_Xas 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 spaceX/Band everyα ∈ Z_{k+1}(X),
c₁(ℒ) ∩ α + c₁(𝒩) ∩ α = c₁(ℒ ⊗_{O_X} 𝒩) ∩ αinCH_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 groupCHis 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
hstis the source's own step thats_ξ ⊗ t_ξgenerates(ℒ ⊗ 𝒩)_ξ, so thatst/(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) ∩ α = 0for everyα ∈ Z_{k+1}(X).The source's proof: the global section
1ofO_Xrestricts, on an integral closed subspaceW ⊆ X, to an everywhere nonzero section ofO_X|_W, soc₁(O_X|_W) ∩ [W] = 0. Here the hypothesishunitis 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})]_konX: the sum, over the irreducible componentsX_i ⊆ Xof δ-dimensionk + 1, of the pushforward alongX_i → Xof the cycle of the zero scheme ofs|_{X_i}, weighted by the multiplicityn_iofX_iin the fundamental cycle[X]_{k+1}.The sum is a finite sum at every integral closed subspace of
X, byAlgebraicGeometry.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/Bbe good, letℒbe an invertible𝒪_X-module, lets ∈ Γ(X, ℒ)be a regular section and assumedim_δ(X) ≤ k + 1. Write[X]_{k+1} = ∑ n_i [X_i]withX_ithe irreducible components ofXof δ-dimensionk + 1, ands_i = s|_{X_i}. Then
[Z(s)]_k = ∑ n_i [Z(s_i)]_kas
k-cycles onX. This is equation 82.18.3.1, Stacks 0EQM.The two sides are the coefficient families of
AlgebraicGeometry.Space.cycleCoeffOfClosedSubspaceat the zero schemeZ(s)of Stacks 0845 and ofAlgebraicGeometry.Space.componentZeroCycleSumCoeff; the geometric representativesγ,γW,γZof 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/Bbe good and letℒbe an invertible𝒪_X-module. LetY ⊆ Xbe a closed subspace withdim_δ(Y) ≤ k + 1and lets ∈ Γ(Y, ℒ|_Y)be a regular section. Then
c₁(ℒ) ∩ [Y]_{k+1} = [Z(s)]_kinCH_k(X).Here
[Y]_{k+1}is the cycle of Stacks 0EE9 ofYonX,AlgebraicGeometry.Space.closedSubspaceCycle;c₁(ℒ) ∩ -is the cap product of Stacks 0EQJ, the cycle-level operationAlgebraicGeometry.Space.firstChernCapCycleMapat the canonical component ruleAlgebraicGeometry.Space.canonicalFirstChernRule, its class taken afterwards;Z(s) ⊆ Yis the zero scheme of Stacks 0845, whosek-cycle (defined becausedim_δ(Z(s)) ≤ k,AlgebraicGeometry.Space.deltaDimensionSubspace_vanishingLocus_closedSubspaceModuleRestrict_le) is read onXthrough the inclusionY → X; andCH_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 componentsY_iofYof δ-dimensionk + 1. The restrictions_i = s|_{Y_i}is nonzero (AlgebraicGeometry.Space.closedSubspaceComponentImageSection_ne_zero), so by Stacks 0EQF the cycle[Z(s_i)]_kis the Weil divisor ofs_i(AlgebraicGeometry.Space.cycleCoeffOfClosedSubspace_vanishingLocus_eq_canonicalDivisorCycleAt), which differs from the component cyclec₁(ℒ|_{Y_i}) ∩ [Y_i]of the cap product by a principal divisor onY_iat the canonical embeddings (Stacks 0EPT,AlgebraicGeometry.Space.isPrincipalDivisorCycleOfGood_zsmul_canonicalDivisorCycleAt_sub). Soc₁(ℒ) ∩ [Y]_{k+1} = ∑ n_i [Z(s_i)]_kinCH_k(X), and the right side is[Z(s)]_kby Stacks 0EQL onY(cycleCoeffOfClosedSubspace_vanishingLocus_eq_componentZeroCycleSumCoeff_of_isRegularSection), the zero schemesZ(s_i)being inverse images ofZ(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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.