72.3 Generically finite… to 72.13 Geometrically irreducible…

Section72.3 Generically finite morphisms#

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

Tag 0AD1, a lemma

Tag 0AD1 in the Stacks Project.

AlgebraicGeometry.Space.isQuasiFiniteAt_of_localRingDimension_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericallyFiniteCodimensionOne.lean, line 187.

Stacks Project, Tag 0AD1. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, with Y locally Noetherian, and let y be a point of |Y| whose local ring has dimension at most one. Write X⁰ for the points of |X| whose local ring has dimension zero. If one of the following holds — the transcendence degree of x over f(x) is zero for every x of X⁰; the same for every x of X⁰ whose image specializes to y; f is quasi-finite at every point of X⁰; f is quasi-finite at a dense set of points of |X| — then f is quasi-finite at every point of |X| above y.

The proof reduces to the corresponding statement for morphisms of schemes, Stacks 0AB6, which is AlgebraicGeometry.quasiFiniteAt_of_target_stalk_dimension_le_one, applied in an étale chart of the target.

theorem isQuasiFiniteAt_of_localRingDimension_le_one
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (y : points B S hS Y) (hy : localRingDimension B S hS y ≤ 1)
    (hgeneric :
      (∀ x : points B S hS X, localRingDimension B S hS x = 0 →
        HasTranscendenceDegreeAt B S hS f x 0) ∨
      (∀ x : points B S hS X, localRingDimension B S hS x = 0 →
        pointsMap B S hS X f x ⤳ y → HasTranscendenceDegreeAt B S hS f x 0) ∨
      (∀ x : points B S hS X, localRingDimension B S hS x = 0 →
        IsQuasiFiniteAt B S hS f x) ∨
      Dense {x : points B S hS X | IsQuasiFiniteAt B S hS f x}) :
    ∀ x : points B S hS X, pointsMap B S hS X f x = y → IsQuasiFiniteAt B S hS f x

Tag 0AD2, a lemma

Tag 0AD2 in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_isFinite_pullback_snd_of_localRingDimension_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteNearCodimensionOnePoint.lean, line 67.

Stacks Project, Tag 0AD2. Let f : X ⟶ Y be a proper morphism of algebraic spaces over S with Y locally Noetherian, and let y be a point of |Y| whose local ring has dimension at most one. If one of the four generic quasi-finiteness conditions of Stacks 0AD1 holds, then y has an open neighbourhood V ⊆ Y over which the base change f^{-1}(V) ⟶ V is finite.

theorem exists_isOpenSubspace_isFinite_pullback_snd_of_localRingDimension_le_one
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hp : IsProper B S hS f)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (y : points B S hS Y) (hy : localRingDimension B S hS y ≤ 1)
    (hgeneric :
      (∀ x : points B S hS X, localRingDimension B S hS x = 0 →
        HasTranscendenceDegreeAt B S hS f x 0) ∨
      (∀ x : points B S hS X, localRingDimension B S hS x = 0 →
        pointsMap B S hS X f x ⤳ y → HasTranscendenceDegreeAt B S hS f x 0) ∨
      (∀ x : points B S hS X, localRingDimension B S hS x = 0 →
        IsQuasiFiniteAt B S hS f x) ∨
      Dense {x : points B S hS X | IsQuasiFiniteAt B S hS f x}) :
    ∃ V : Subfunctor Y, IsOpenSubspace B S hS V ∧
      y ∈ Set.range (pointsMap B S hS V.toFunctor V.ι) ∧
      IsFinite B S hS (pullback.snd f V.ι)

Tag 0BBQ, a lemma

Tag 0BBQ in the Stacks Project.

AlgebraicGeometry.Space.mem_isomorphismLocus_of_localRingDimension_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperBirationalIsomorphismLocus.lean, line 646. The attribute's comment: “part (1): every point of codimension zero”.

Stacks 0BBQ, part (1). Let X be a Noetherian algebraic space over S and let f : Y ⟶ X be a proper birational morphism with Y reduced. The maximal open subspace U of X over which f is an isomorphism contains every point of |X| of codimension 0.

By Stacks 0BBF the morphism is an isomorphism over a dense open subspace V ⊆ X, which is contained in U by maximality. A dense subset of the Noetherian point space |X| meets the nonempty open part of every irreducible component, so it meets the component of the given codimension-zero point, which is therefore in V.

theorem mem_isomorphismLocus_of_localRingDimension_eq_zero
    (x : points B S hS X) (hx : localRingDimension B S hS x = 0) :
    x ∈ Set.range (pointsMap B S hS U.toFunctor U.ι)

AlgebraicGeometry.Space.mem_isomorphismLocus_of_finite_fibre_of_normal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperBirationalIsomorphismLocus.lean, line 676. The attribute's comment: “part (3): every point with finite fibre and normal local ring”.

Stacks 0BBQ, part (3). With the hypotheses of part (1), the maximal open subspace over which f is an isomorphism contains every point of |X| whose fibre in |Y| is finite and whose local ring is normal.

Stacks 0A4W, applied through Stacks 0ACK to convert the finite set-theoretic fibre into a finite geometric fibre, makes f finite over an open neighbourhood of the point, and AlgebraicGeometry.Space.mem_isomorphismLocus_of_isFinite_over_neighbourhood concludes.

theorem mem_isomorphismLocus_of_finite_fibre_of_normal
    (x : points B S hS X) (hfibre : ((pointsMap B S hS Y f) ⁻¹' {x}).Finite)
    (hNormal : HasNormalLocalRingAtPoint B S hS X hX x) :
    x ∈ Set.range (pointsMap B S hS U.toFunctor U.ι)

AlgebraicGeometry.Space.mem_isomorphismLocus_of_localRingDimension_eq_one_of_normal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperBirationalIsomorphismLocus.lean, line 694. The attribute's comment: “part (2): every point of codimension one with normal local ring”.

Stacks 0BBQ, part (2). With the hypotheses of part (1), the maximal open subspace over which f is an isomorphism contains every point of |X| of codimension 1 whose local ring is normal.

Part (1) already puts the image of every codimension-zero point of |Y| in U, which makes f quasi-finite there, so the third generic condition of Stacks 0AD2 holds and f is finite over an open neighbourhood of the given point; part (3)'s argument then concludes.

theorem mem_isomorphismLocus_of_localRingDimension_eq_one_of_normal
    (x : points B S hS X) (hx : localRingDimension B S hS x = 1)
    (hNormal : HasNormalLocalRingAtPoint B S hS X hX x) :
    x ∈ Set.range (pointsMap B S hS U.toFunctor U.ι)

Sources

• Section 72.3, Tag 0ACY
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isQuasiFiniteAt_of_localRingDimension_le_one · AlgebraicGeometry.Space.exists_isOpenSubspace_isFinite_pullback_snd_of_localRingDimension_le_one · AlgebraicGeometry.Space.mem_isomorphismLocus_of_localRingDimension_eq_zero · AlgebraicGeometry.Space.mem_isomorphismLocus_of_finite_fibre_of_normal · AlgebraicGeometry.Space.mem_isomorphismLocus_of_localRingDimension_eq_one_of_normal

Section72.4 Integral algebraic spaces#

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

Tag 0AD4, a definition

Tag 0AD4 in the Stacks Project.

AlgebraicGeometry.Space.IsIntegralSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralSpace.lean, line 67.

Stacks 0AD4. An algebraic space over S is integral when it is reduced, decent, and its space of points is irreducible.

abbrev IsIntegralSpace : Prop

Tag 0END, a lemma

Tag 0END in the Stacks Project.

AlgebraicGeometry.Space.evalPartial_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 359. The attribute's comment: “the characterisation of evaluation at the generic point: the value on a representative is its coordinate along any factorisation of the residue-field morphism through the domain, independently of the factorisation”.

Evaluation is computed by any lift of the generic field-valued point.

theorem evalPartial_eq (p : FieldValuedPoint B S hS X)
    (hp : p.class B S hS X = genericPoint B S hS hX hInt)
    (f : PartialMap B S hS hX (affineLineFunctor B S hS))
    (j : yoneda.obj (p.siteObject B S hS X) ⟶ f.domain.toFunctor)
    (hj : j ≫ f.domain.ι = fieldMorphism B S hS X p) :
    evalPartial B S hS hX hInt p hp f =
      (Scheme.ΓSpecIso (CommRingCat.of p.carrier)).hom.hom
        (affineLineCoordinate B S hS (Opposite.op (p.siteObject B S hS X))
          (yonedaEquiv (j ≫ f.hom)))

AlgebraicGeometry.Space.evalRingHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 445. The attribute's comment: “evaluation of rational functions at the generic point, as a ring homomorphism R(X) → κ(η)”.

Evaluation at the generic point, as a ring homomorphism from the rational functions to the field of a field-valued representative of that point.

noncomputable def evalRingHom (p : FieldValuedPoint B S hS X)
    (hp : p.class B S hS X = genericPoint B S hS hX hInt) :
    rationalFunctions B S hS hX →+* p.carrier

AlgebraicGeometry.Space.isField_residueField_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 580. The attribute's comment: “the residue field at the generic point is a field”.

Stacks 0END. The residue field at the generic point of an integral algebraic space over S is a field.

theorem isField_residueField_genericPoint (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) :
    IsField (residueField B S hS X hInt.2.1 (genericPoint B S hS hX hInt))

AlgebraicGeometry.Space.evalRingHom_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 855. The attribute's comment: “injectivity of evaluation at the generic point”.

Evaluation at the generic point is injective: a rational function whose value there vanishes has a representative on a representable dense open chart through the generic point, and the coordinate of that representative, a regular function on an integral scheme, is determined by its value at the dense point of that scheme.

theorem evalRingHom_injective (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) (p : FieldValuedPoint B S hS X)
    (hp : p.class B S hS X = genericPoint B S hS hX hInt) :
    Function.Injective (evalRingHom B S hS hX hInt p hp)

AlgebraicGeometry.Space.evalRingHom_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 992. The attribute's comment: “surjectivity of evaluation at the generic point”.

Evaluation at the generic point is surjective: the field of a monomorphic representative of the generic point is the residue field of a representable dense open chart at the point below the generic point, every element of that residue field is the value of a regular function on a smaller open set, and that open set carries a representable dense open chart again.

theorem evalRingHom_surjective (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) (p : FieldValuedPoint B S hS X)
    (hp : p.class B S hS X = genericPoint B S hS hX hInt)
    (hmono : Mono (fieldMorphism B S hS X p)) :
    Function.Surjective (evalRingHom B S hS hX hInt p hp)

AlgebraicGeometry.Space.evalRingHom_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1091. The attribute's comment: “bijectivity of evaluation at the generic point, on a monomorphic field-valued representative”.

Evaluation at the generic point is a bijection onto the field of a monomorphic field-valued representative of that point.

theorem evalRingHom_bijective (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) (p : FieldValuedPoint B S hS X)
    (hp : p.class B S hS X = genericPoint B S hS hX hInt)
    (hmono : Mono (fieldMorphism B S hS X p)) :
    Function.Bijective (evalRingHom B S hS hX hInt p hp)

AlgebraicGeometry.Space.rationalFunctionsRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1104. The attribute's comment: “the identification R(X) = κ(η) of the rational functions with the residue field at the generic point”.

Stacks 0END. The ring of rational functions of an integral algebraic space over S is the residue field at its generic point: evaluation at the generic point is an isomorphism of rings from the rational functions of Tag 0EMP onto the residue field of Tag 0EMW.

noncomputable def rationalFunctionsRingEquiv (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) :
    rationalFunctions B S hS hX ≃+*
      residueField B S hS X hInt.2.1 (genericPoint B S hS hX hInt)

AlgebraicGeometry.Space.isField_rationalFunctions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1141. The attribute's comment: “the rational functions of an integral algebraic space form a field”.

Stacks 0END. The ring of rational functions of an integral algebraic space over S is a field: it is the residue field at the generic point.

theorem isField_rationalFunctions (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) : IsField (rationalFunctions B S hS hX)

AlgebraicGeometry.Space.isField_neighborhoodStalk_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1219. The attribute's comment: “the local ring of an elementary étale neighbourhood at its marked point, over the generic point, is a field; the neighbourhood is a parameter because the statement is about it, and Tag 0BBP provides one”.

The local ring of an elementary étale neighbourhood of the generic point of an integral algebraic space, at the marked point of that neighbourhood, is a field: the scheme of the neighbourhood is reduced, because reducedness is an étale-local property and the neighbourhood is étale over the space, and the local ring has Krull dimension zero, because the generic point is a point of codimension zero by Stacks 0ABV and the dimension of the local ring of an algebraic space at a point is measured on any étale chart above it by Stacks 0BAM.

theorem isField_neighborhoodStalk_genericPoint (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X)
    (E : ElementaryEtaleNeighborhood B S hS X hX (genericPoint B S hS hX hInt)) :
    IsField (E.scheme.left.1.presheaf.stalk E.point)

AlgebraicGeometry.Space.evalNeighborhoodRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1275. The attribute's comment: “the rational functions are the residue field of an elementary étale neighbourhood of the generic point at its marked point”.

The ring of rational functions of an integral algebraic space is the residue field of any elementary étale neighbourhood of the generic point at its marked point: that residue field is a monomorphic field-valued representative of the generic point, by the data of Stacks 0BGU, so evaluation at the generic point is bijective onto it.

noncomputable def evalNeighborhoodRingEquiv (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X)
    (E : ElementaryEtaleNeighborhood B S hS X hX (genericPoint B S hS hX hInt)) :
    rationalFunctions B S hS hX ≃+* E.scheme.left.1.residueField E.point

AlgebraicGeometry.Space.isField_henselianLocalRing_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1291. The attribute's comment: “the henselian local ring O^h_{X,η} at the generic point is a field”.

Stacks 0END. The henselian local ring of Stacks 0BGW at the generic point of an integral algebraic space is a field: it is a henselisation of the local ring of the elementary étale neighbourhood of Stacks 0BBP at its marked point by Stacks 0EMY, that local ring is a field, and a henselisation of a field is a field.

theorem isField_henselianLocalRing_genericPoint (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) :
    IsField (henselianLocalRing B S hS X hX (genericPoint B S hS hX hInt) hInt.2.1 :
      Type (u + 1))

AlgebraicGeometry.Space.bijective_stalkToHenselianLocalRing_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1307. The attribute's comment: “bijectivity at the generic point of the canonical map O_{U,u} → O^h_{X,η} of Tag 0EMY”.

The canonical map of Stacks 0EMY from the local ring of an elementary étale neighbourhood of the generic point into the henselian local ring is bijective: it is the structure map of a henselisation of a field.

theorem bijective_stalkToHenselianLocalRing_genericPoint (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X)
    (E : ElementaryEtaleNeighborhood B S hS X hX (genericPoint B S hS hX hInt)) :
    Function.Bijective (stalkToHenselianLocalRing B S hS X hX
      (genericPoint B S hS hX hInt) hInt.2.1 E)

AlgebraicGeometry.Space.rationalFunctionsHenselianRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1381. The attribute's comment: “the identification R(X) = O^h_{X,η} of the rational functions with the henselian local ring at the generic point”.

Stacks 0END. The ring of rational functions of an integral algebraic space over S is the henselian local ring of Stacks 0BGW at its generic point: the comparison is built from the elementary étale neighbourhood of Stacks 0BBP.

noncomputable def rationalFunctionsHenselianRingEquiv (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) :
    rationalFunctions B S hS hX ≃+*
      (henselianLocalRing B S hS X hX (genericPoint B S hS hX hInt) hInt.2.1 : Type (u + 1))

AlgebraicGeometry.Space.rationalFunctionsHenselianRingEquivOfNeighborhood_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1417. The attribute's comment: “the characterisation of that identification: a rational function goes to the canonical image of any element of the neighbourhood's local ring whose residue is its value at the generic point”.

The identification with the henselian local ring is pinned down without inverses: it carries a rational function to the canonical image of any element of the local ring of the neighbourhood whose residue is the value of that function at the generic point.

theorem rationalFunctionsHenselianRingEquivOfNeighborhood_eq (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X)
    (E : ElementaryEtaleNeighborhood B S hS X hX (genericPoint B S hS hX hInt))
    (x : rationalFunctions B S hS hX) (r : E.scheme.left.1.presheaf.stalk E.point)
    (hr : IsLocalRing.residue (E.scheme.left.1.presheaf.stalk E.point) r =
      evalRingHom B S hS hX hInt (genericNeighborhoodFieldPoint B S hS hX hInt E)
        (neighborhoodFieldPoint_class B S hS X hX (genericPoint B S hS hX hInt) E) x) :
    rationalFunctionsHenselianRingEquivOfNeighborhood B S hS hX hInt E x =
      stalkToHenselianLocalRing B S hS X hX (genericPoint B S hS hX hInt) hInt.2.1 E r

AlgebraicGeometry.Space.residueFieldHenselianRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1462. The attribute's comment: “the identification O^h_{X,η} = κ(η) of the henselian local ring at the generic point with the residue field there”.

Stacks 0END. The residue field at the generic point of an integral algebraic space over S is the henselian local ring of Stacks 0BGW there: both are the ring of rational functions.

noncomputable def residueFieldHenselianRingEquiv (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) :
    residueField B S hS X hInt.2.1 (genericPoint B S hS hX hInt) ≃+*
      (henselianLocalRing B S hS X hX (genericPoint B S hS hX hInt) hInt.2.1 : Type (u + 1))

AlgebraicGeometry.Space.rationalFunctionsHenselianRingEquiv_eq_trans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericRationalFunctions.lean, line 1474. The attribute's comment: “the chain R(X) = O^h_{X,η} = κ(η): the three identifications commute”.

Stacks 0END. The tag asserts one chain of identifications R(X) = O^h_{X,η} = κ(η), and the three identifications are indeed the three edges of one commuting triangle: going from the rational functions to the henselian local ring is going to the residue field and on from there.

theorem rationalFunctionsHenselianRingEquiv_eq_trans (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) :
    rationalFunctionsHenselianRingEquiv B S hS hX hInt =
      (rationalFunctionsRingEquiv B S hS hX hInt).trans
        (residueFieldHenselianRingEquiv B S hS hX hInt)

Tag 0ENE, a definition

Tag 0ENE in the Stacks Project.

AlgebraicGeometry.Space.functionField, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FunctionField.lean, line 65. The attribute's comment: “the function field R(X) = k(X) of an integral algebraic space”.

Stacks 0ENE. The function field, or field of rational functions, of an integral algebraic space X over S: the ring R(X) of rational functions of Tag 0EMP, which Tag 0END shows to be a field by identifying it with the residue field at the generic point.

noncomputable def functionField (hX : IsAlgebraicSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X) : Field (rationalFunctions B S hS hX)

Tag 0BH2, a lemma

Tag 0BH2 in the Stacks Project.

AlgebraicGeometry.Space.isDomain_globalSections_of_isIntegralSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralSpaceProperties.lean, line 285.

The ring of global regular functions on an integral algebraic space, the compatible families of regular functions on its étale charts, is a domain.

theorem isDomain_globalSections_of_isIntegralSpace (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) (hXint : IsIntegralSpace B S hS X) :
    IsDomain (RingCat.sectionsSubring
      (structurePresheaf B S hS X ⋙ forget₂ CommRingCat.{u} RingCat.{u}))

Tag 0AYH, a lemma

Tag 0AYH in the Stacks Project.

AlgebraicGeometry.Space.exists_isAffine_isNormal_isIntegral_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalIntegralEtaleChart.lean, line 248.

Stacks 0AYH. Let X be a normal integral algebraic space over S. Every point of |X| is in the image of an étale morphism to X from a normal integral affine scheme.

An affine étale chart through the point is shrunk to an affine open which is normal and integral by AlgebraicGeometry.Space.exists_isAffineOpen_isNormal_isIntegral_of_isAffine_etaleChart, and that open is an object of the chosen big site by AlgebraicGeometry.BigFppfOver.exists_affineOpen_restrict.

theorem exists_isAffine_isNormal_isIntegral_etaleChart (hX : IsAlgebraicSpace B S hS X)
    (hnormal : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsNormal Y))
    (hintegral : IsIntegralSpace B S hS X) (x : points B S hS X) :
    ∃ (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X),
      IsAffine ((BigFppfOver.toScheme B S hS).obj U) ∧
      IsNormal ((BigFppfOver.toScheme B S hS).obj U) ∧
      IsIntegral ((BigFppfOver.toScheme B S hS).obj U) ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) φ ∧
      x ∈ Set.range (pointsMap B S hS (yoneda.obj U) φ)

Tag 0BH3, a lemma

Tag 0BH3 in the Stacks Project.

AlgebraicGeometry.Space.isNormalDomain_globalSections_of_isIntegralSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralSpaceProperties.lean, line 409. References: EGA II (8.8.6.1).

The ring of global regular functions on a normal integral algebraic space, the compatible families of regular functions on its étale charts, is a normal domain.

theorem isNormalDomain_globalSections_of_isIntegralSpace (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) (hXint : IsIntegralSpace B S hS X)
    (hXnormal : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} => IsNormal Y)) :
    IsNormalDomain (RingCat.sectionsSubring
      (structurePresheaf B S hS X ⋙ forget₂ CommRingCat.{u} RingCat.{u}))

Tag 0ENF, a lemma

Tag 0ENF in the Stacks Project.

AlgebraicGeometry.Space.injective_closureSingleton_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IntegralClosedSubspaces.lean, line 101. The attribute's comment: “the map from (1) to (2) is injective, unconditionally”.

Two points of a decent algebraic space over S with the same closure are equal: the map from (1) to (2) is injective.

theorem injective_closureSingleton_points (hX : IsAlgebraicSpace B S hS X)
    (hdecent : IsDecentSpace B S hS X) :
    Function.Injective (IrreducibleCloseds.closureSingleton (X := points B S hS X))

AlgebraicGeometry.Space.bijective_closureSingleton_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IntegralClosedSubspaces.lean, line 114. The attribute's comment: “the bijection from (1) to (2)”.

Taking the closure of a point is a bijection from the points of a decent algebraic space X over S onto the irreducible closed subsets of |X|.

theorem bijective_closureSingleton_points (hX : IsAlgebraicSpace B S hS X)
    (hdecent : IsDecentSpace B S hS X) :
    Function.Bijective (IrreducibleCloseds.closureSingleton (X := points B S hS X))

AlgebraicGeometry.Space.IntegralClosedSubspace, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IntegralClosedSubspaces.lean, line 128. The attribute's comment: “(3): the integral closed subspaces of an algebraic space”.

An integral closed subspace of an algebraic space X over S is a closed subspace of X, in the sense of Stacks 02YU, which is an integral algebraic space over S, in the sense of Stacks 0AD4.

structure IntegralClosedSubspace (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)

AlgebraicGeometry.Space.integralClosedSubspaceSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IntegralClosedSubspaces.lean, line 157. The attribute's comment: “the map from (3) to (2): the point set of an integral closed subspace”.

The set of points of an integral closed subspace of X, as an irreducible closed subset of |X|. This is the map from (3) to (2).

def integralClosedSubspaceSupport (hX : IsAlgebraicSpace B S hS X)
    (Z : IntegralClosedSubspace B S hS X) : IrreducibleCloseds (points B S hS X)

AlgebraicGeometry.Space.injective_integralClosedSubspaceSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IntegralClosedSubspaces.lean, line 175. The attribute's comment: “the map from (3) to (2) is injective, unconditionally”.

An integral closed subspace of an algebraic space over S is determined by its set of points: the map from (3) to (2) is injective.

theorem injective_integralClosedSubspaceSupport (hX : IsAlgebraicSpace B S hS X) :
    Function.Injective (integralClosedSubspaceSupport B S hS hX)

AlgebraicGeometry.Space.surjective_integralClosedSubspaceSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IntegralClosedSubspaces.lean, line 189. The attribute's comment: “the map from (3) to (2) is surjective”.

Every irreducible closed subset of |X|, for X a decent algebraic space over S, is the set of points of an integral closed subspace: the map from (3) to (2) is surjective.

theorem surjective_integralClosedSubspaceSupport (hX : IsAlgebraicSpace B S hS X)
    (hdecent : IsDecentSpace B S hS X) :
    Function.Surjective (integralClosedSubspaceSupport B S hS hX)

AlgebraicGeometry.Space.bijective_integralClosedSubspaceSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IntegralClosedSubspaces.lean, line 216. The attribute's comment: “the bijection from (3) to (2)”.

Taking the set of points is a bijection from the integral closed subspaces of a decent algebraic space X over S onto the irreducible closed subsets of |X|.

theorem bijective_integralClosedSubspaceSupport (hX : IsAlgebraicSpace B S hS X)
    (hdecent : IsDecentSpace B S hS X) :
    Function.Bijective (integralClosedSubspaceSupport B S hS hX)

Sources

• Section 72.4, Tag 0AD3
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsIntegralSpace · AlgebraicGeometry.Space.evalPartial_eq · AlgebraicGeometry.Space.evalRingHom · AlgebraicGeometry.Space.isField_residueField_genericPoint · AlgebraicGeometry.Space.evalRingHom_injective · AlgebraicGeometry.Space.evalRingHom_surjective · AlgebraicGeometry.Space.evalRingHom_bijective · AlgebraicGeometry.Space.rationalFunctionsRingEquiv

Section72.5 Morphisms between integral algebraic spaces#

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

Tag 0AD5, a lemma

Tag 0AD5 in the Stacks Project.

AlgebraicGeometry.Space.finite_residueFieldHom_genericPoint_of_hasTranscendenceDegreeAt_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/EqualDeltaDimension.lean, line 486. The attribute's comment: “condition (1) implies condition (2): finiteness of the residue field extension at the generic point, from vanishing of the relative transcendence degree there”.

Spaces over Fields, Lemma 0AD5, (1) implies (2). Let f : X ⟶ Y be a dominant morphism of integral algebraic spaces over S which is locally of finite type. If the transcendence degree of the generic point of X over the generic point of Y is zero, then the induced extension of residue fields at the generic point is finite.

Both residue fields are read on a pair of representable open charts through the generic point, which exist by Stacks 086U and Stacks 03IE.

theorem finite_residueFieldHom_genericPoint_of_hasTranscendenceDegreeAt_zero
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXInt : IsIntegralSpace B S hS X) (hYInt : IsIntegralSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f) (hdom : IsDominant B S hS f)
    (htr : HasTranscendenceDegreeAt B S hS f (genericPoint B S hS hX hXInt) 0) :
    letI := (residueFieldHom B S hS X Y hY hXInt.2.1 hYInt.2.1 f
      (genericPoint B S hS hX hXInt)).toAlgebra
    Module.Finite
      (residueField B S hS Y hYInt.2.1
        (pointsMap B S hS X f (genericPoint B S hS hX hXInt)))
      (residueField B S hS X hXInt.2.1 (genericPoint B S hS hX hXInt))

AlgebraicGeometry.Space.isQuasiFiniteAt_iff_forall_eq_of_pointsMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralGenericallyFinite.lean, line 109. The attribute's comment: “conditions (4) and (5)”.

Stacks 0AD5, conditions (4) and (5). Let f : X ⟶ Y be a dominant morphism locally of finite type of algebraic spaces over S with Y integral, and let x and y be generic points of |X| and |Y|. Then f is quasi-finite at x exactly when x is the only point of |X| mapping to y.

theorem isQuasiFiniteAt_iff_forall_eq_of_pointsMap_eq
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hYint : IsIntegralSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (hdom : IsDominant B S hS f)
    {x : points B S hS X} (hx : IsGenericPoint x (Set.univ : Set (points B S hS X)))
    {y : points B S hS Y} (hy : IsGenericPoint y (Set.univ : Set (points B S hS Y))) :
    IsQuasiFiniteAt B S hS f x ↔
      ∀ x' : points B S hS X, pointsMap B S hS X f x' = y → x' = x

AlgebraicGeometry.Space.hasTranscendenceDegreeAt_zero_of_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralGenericallyFinite.lean, line 167. The attribute's comment: “condition (4) implies condition (1)”.

Stacks 0AD5, condition (4) implies condition (1). A morphism of algebraic spaces over S which is quasi-finite at a point of its source has transcendence degree zero there: on an open subspace containing the point the morphism is locally quasi-finite, so contributes a finite residue field extension in every étale chart, and an open immersion does not change the transcendence degree (Stacks 06RX).

theorem hasTranscendenceDegreeAt_zero_of_isQuasiFiniteAt
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    {x : points B S hS X} (h : IsQuasiFiniteAt B S hS f x) :
    HasTranscendenceDegreeAt B S hS f x 0

AlgebraicGeometry.Space.tfae_hasTranscendenceDegreeAt_eq_zero_and_isFiniteOverAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralGenericallyFiniteTfae.lean, line 956.

Stacks 0AD5. Let S be a scheme, let X and Y be integral algebraic spaces over S, let x ∈ |X| and y ∈ |Y| be the generic points, and let f : X ⟶ Y be locally of finite type and dominant. The following are equivalent:

1. the transcendence degree of x/y is 0;
2. the extension κ(x)/κ(y) is finite;
3. there exist nonempty affine opens U ⊂ X and V ⊂ Y such that f(U) ⊂ V and f|_U : U ⟶ V is finite;
4. f is quasi-finite at x;
5. x is the only point of |X| mapping to y.

If f is separated or if f is quasi-compact, then these are also equivalent to

1. there exists a nonempty affine open V ⊂ Y such that f^{-1}(V) ⟶ V is finite.

theorem tfae_hasTranscendenceDegreeAt_eq_zero_and_isFiniteOverAffineOpen
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXInt : IsIntegralSpace B S hS X) (hYInt : IsIntegralSpace B S hS Y)
    (f : X ⟶ Y) (hlft : IsLocallyOfFiniteType B S hS f) (hdom : IsDominant B S hS f)
    {x : points B S hS X} (hx : IsGenericPoint x (Set.univ : Set (points B S hS X)))
    {y : points B S hS Y} (hy : IsGenericPoint y (Set.univ : Set (points B S hS Y))) :
    List.TFAE
        [HasTranscendenceDegreeAt B S hS f x 0,
          HasFiniteResidueFieldExtensionAt B S hS hY hXInt.2.1 hYInt.2.1 f x,
          ExistsAffineOpenFiniteRestriction B S hS f,
          IsQuasiFiniteAt B S hS f x,
          ∀ x' : points B S hS X, pointsMap B S hS X f x' = y → x' = x] ∧
      ((IsSeparated B S hS f ∨ IsQuasiCompact B S hS f) →
        List.TFAE
          [HasTranscendenceDegreeAt B S hS f x 0,
            HasFiniteResidueFieldExtensionAt B S hS hY hXInt.2.1 hYInt.2.1 f x,
            ExistsAffineOpenFiniteRestriction B S hS f,
            IsQuasiFiniteAt B S hS f x,
            (∀ x' : points B S hS X, pointsMap B S hS X f x' = y → x' = x),
            IsFiniteOverAffineOpen B S hS f])

Tag 0AD6, a definition

Tag 0AD6 in the Stacks Project.

AlgebraicGeometry.Space.degree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralDegree.lean, line 214. The attribute's comment: “the degree of X over Y”.

Stacks 0AD6. The degree of X over Y for a morphism f : X ⟶ Y of integral algebraic spaces over S: the degree [κ(x) : κ(y)] of the extension of residue fields at the generic point x of |X| and its image y.

noncomputable def degree (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXint : IsIntegralSpace B S hS X) (hYint : IsIntegralSpace B S hS Y) (f : X ⟶ Y) : ℕ

AlgebraicGeometry.Space.degree_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralDegree.lean, line 244. The attribute's comment: “positivity of the degree, under condition (2) of Stacks 0AD5, which this development cannot yet deduce from the other four”.

Stacks 0AD6. The degree of X over Y is a positive integer once the extension of residue fields at the generic point is finite, which is condition (2) of Stacks 0AD5.

theorem degree_pos (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXint : IsIntegralSpace B S hS X) (hYint : IsIntegralSpace B S hS Y) (f : X ⟶ Y)
    {x : points B S hS X}
    (hx : IsGenericPoint x (Set.univ : Set (points B S hS X)))
    (hfin : HasFiniteResidueFieldExtensionAt B S hS hY hXint.isDecentSpace
      hYint.isDecentSpace f x) :
    0 < degree B S hS hX hY hXint hYint f

Tag 0ENH, a lemma

Tag 0ENH in the Stacks Project.

AlgebraicGeometry.Space.degree_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralDegree.lean, line 272. The attribute's comment: “multiplicativity of the degree; local finiteness of type of the two morphisms, finiteness of the two residue field extensions and dominance of g are not needed”.

Stacks 0ENH. For a dominant morphism f : X ⟶ Y and a morphism g : Y ⟶ Z of integral algebraic spaces over S, the degree of X over Z is the degree of X over Y times the degree of Y over Z.

The generic point of |X| maps to the generic point of |Y| because f is dominant, so all three degrees are read off the same tower of residue fields, and degrees multiply in a tower of field extensions (Stacks 09G9).

theorem degree_comp (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (hXint : IsIntegralSpace B S hS X)
    (hYint : IsIntegralSpace B S hS Y) (hZint : IsIntegralSpace B S hS Z) (f : X ⟶ Y)
    (g : Y ⟶ Z) (hf : IsDominant B S hS f) :
    degree B S hS hX hZ hXint hZint (f ≫ g) =
      degree B S hS hX hY hXint hYint f * degree B S hS hY hZ hYint hZint g

Sources

• Section 72.5, Tag 0ENG
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.finite_residueFieldHom_genericPoint_of_hasTranscendenceDegreeAt_zero · AlgebraicGeometry.Space.isQuasiFiniteAt_iff_forall_eq_of_pointsMap_eq · AlgebraicGeometry.Space.hasTranscendenceDegreeAt_zero_of_isQuasiFiniteAt · AlgebraicGeometry.Space.tfae_hasTranscendenceDegreeAt_eq_zero_and_isFiniteOverAffineOpen · AlgebraicGeometry.Space.degree · AlgebraicGeometry.Space.degree_pos · AlgebraicGeometry.Space.degree_comp

Section72.6 Weil divisors#

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

Tag 0EE5, a lemma

Tag 0EE5 in the Stacks Project.

AlgebraicGeometry.Space.locallyFinite_irreducibleComponents_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianIrreducibleComponents.lean, line 45.

The irreducible components of a closed subset of the space of points of a locally Noetherian algebraic space over S form a locally finite collection.

theorem locallyFinite_irreducibleComponents_of_isClosed (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F)
    (hN : HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} ↦ IsLocallyNoetherian X))
    (T : Set (points B S hS F)) (hT : IsClosed T) :
    LocallyFinite fun C : irreducibleComponents T ↦ Subtype.val '' (C : Set T)

Tag 0ENJ, a definition

Tag 0ENJ in the Stacks Project.

AlgebraicGeometry.Space.PrimeDivisor, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeilDivisor.lean, line 75. The attribute's comment: “part (1): prime divisors”.

Stacks 0ENJ, part (1). A prime divisor of X is an integral closed subspace of X whose generic point has codimension one in X.

structure PrimeDivisor

AlgebraicGeometry.Space.WeilDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeilDivisor.lean, line 121. The attribute's comment: “part (2): Weil divisors”.

Stacks 0ENJ, part (2). The group Div(X) of Weil divisors of X: integer coefficient families on prime divisors of X whose nonzero part has locally finite support in |X|.

def WeilDivisor : AddSubgroup (PrimeDivisor B S hS X → ℤ)

Tag 0ENK, a lemma

Tag 0ENK in the Stacks Project.

AlgebraicGeometry.Space.PrimeDivisor.neighborhoodTotalFractionRingToGeneric_pullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorFunctionFieldChartIndependence.lean, line 151. The attribute's comment: “independence of the canonical map R(X) → Q(𝒪^h_{X, ξ}) of the affine elementary étale neighbourhood used to compute it -- a verification the source omits”.

Stacks 0ENK, computed on an arbitrary affine chart. The canonical map from the function field of a decent, locally Noetherian, integral algebraic space into the total ring of fractions of the henselian local ring at the generic point of a prime divisor is computed on any affine elementary étale neighbourhood of that generic point, not only on the chart of Stacks 0BBP which defines it.

theorem PrimeDivisor.neighborhoodTotalFractionRingToGeneric_pullback_eq
    [IsLocalRing ↥(Z.genericHenselianLocalRing B S hS hX hdec)]
    (hInt : IsIntegralSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} => IsLocallyNoetherian Y))
    (U : ElementaryEtaleNeighborhood B S hS X hX (Z.genericPoint B S hS X))
    [IsAffine U.scheme.left.1] [IsReduced U.scheme.left.1]
    [IsLocallyNoetherian U.scheme.left.1]
    (hCofiltered :
      IsCofiltered (ElementaryEtaleNeighborhood B S hS X hX (Z.genericPoint B S hS X)))
    (r : rationalFunctions B S hS hX) :
    Z.neighborhoodTotalFractionRingToGeneric B S hS hX hdec U hCofiltered
        (rationalFunctionsToTotalFractionRing B S hS hX U.scheme U.toSpace U.etale_toSpace r) =
      Z.rationalFunctionsToGenericTotalFractionRing B S hS hX hdec hInt hN r

AlgebraicGeometry.Space.PrimeDivisor.rationalFunctionsToGenericTotalFractionRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorFunctionFieldEmbedding.lean, line 187. The attribute's comment: “the canonical map R(X) → Q(𝒪^h_{X, ξ}) from the function field into the total ring of fractions of the henselian local ring at the generic point of a prime divisor”.

The canonical map from the function field of a decent, locally Noetherian, integral algebraic space into the total ring of fractions of the henselian local ring at the generic point of a prime divisor: a rational function is pulled back to the spectrum of the total ring of fractions of the global sections A of the chosen affine elementary étale neighbourhood (U, u) of the generic point, and then pushed along A → 𝒪_{U, u} → 𝒪^h_{X, ξ}.

def PrimeDivisor.rationalFunctionsToGenericTotalFractionRing :
    rationalFunctions B S hS hX →+* Z.genericTotalFractionRing B S hS hX hdec

AlgebraicGeometry.Space.PrimeDivisor.injective_rationalFunctionsToGenericTotalFractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorFunctionFieldEmbedding.lean, line 204. The attribute's comment: “injectivity of the canonical map R(X) → Q(𝒪^h_{X, ξ}), the function field being a field and the total ring of fractions nontrivial”.

The canonical map from the function field of a decent, locally Noetherian, integral algebraic space into the total ring of fractions of the henselian local ring at the generic point of a prime divisor is injective.

theorem PrimeDivisor.injective_rationalFunctionsToGenericTotalFractionRing :
    Function.Injective
      (Z.rationalFunctionsToGenericTotalFractionRing B S hS hX hdec hInt hN)

AlgebraicGeometry.Space.genericFractionEmbedding, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorFunctionFieldEmbedding.lean, line 219. The attribute's comment: “the conclusions of the lemma assembled at every prime divisor, as the data the order of vanishing along a prime divisor is defined from”.

At every prime divisor of a decent, locally Noetherian, integral algebraic space: the henselian local ring at the generic point of the prime divisor is a nontrivial Noetherian local ring of dimension at most one, and the function field embeds in its total ring of fractions.

def genericFractionEmbedding : GenericFractionEmbedding B S hS hX hdec

AlgebraicGeometry.Space.PrimeDivisor.isReduced_and_ringKrullDim_eq_one_and_isNoetherianRing_genericHenselianLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorHenselianLocalRing.lean, line 55. The attribute's comment: “the henselian local ring at the generic point of a prime divisor is a reduced 1-dimensional Noetherian local ring; the canonical injection of the function field into its total ring of fractions is AlgebraicGeometry.Space.PrimeDivisor.rationalFunctionsToGenericTotalFractionRing”.

The henselian local ring at the generic point of a prime divisor of a decent, locally Noetherian, integral algebraic space is reduced, of Krull dimension one, and Noetherian.

theorem
  PrimeDivisor.isReduced_and_ringKrullDim_eq_one_and_isNoetherianRing_genericHenselianLocalRing
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X)
    (hInt : IsIntegralSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} => IsLocallyNoetherian Y))
    (Z : PrimeDivisor B S hS X) :
    _root_.IsReduced ↥(Z.genericHenselianLocalRing B S hS hX hdec) ∧
      ringKrullDim ↥(Z.genericHenselianLocalRing B S hS hX hdec) = 1 ∧
      IsNoetherianRing ↥(Z.genericHenselianLocalRing B S hS hX hdec)

Tag 0ENL, a definition

Tag 0ENL in the Stacks Project.

AlgebraicGeometry.Space.PrimeDivisor.ord_mk', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OrderOfVanishing.lean, line 219. The attribute's comment: “the difference-of-lengths formula, on a unit of the total ring of fractions of the henselian local ring at the generic point”.

The order of vanishing along a prime divisor of a fraction a / b of nonzerodivisors of the henselian local ring at its generic point is the difference of the lengths of the quotients by the ideals (a) and (b).

This is the defining formula of the order of vanishing, computed on the total ring of fractions of the henselian local ring.

theorem PrimeDivisor.ord_mk'
    (a b : nonZeroDivisors ↥(Z.genericHenselianLocalRing B S hS hX hdec))
    (hu : IsUnit (IsLocalization.mk' (Z.genericTotalFractionRing B S hS hX hdec)
      (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec)) b)) :
    Z.ord B S hS hX hdec (IsLocalization.mk' (Z.genericTotalFractionRing B S hS hX hdec)
        (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec)) b) hu =
      ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec)
          (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec))).toNat : ℤ) -
        ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec)
          (b : ↥(Z.genericHenselianLocalRing B S hS hX hdec))).toNat : ℤ)

AlgebraicGeometry.Space.ordRationalFunction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OrderOfVanishingRationalFunction.lean, line 88. The attribute's comment: “ord_Z(f) for an invertible rational function f on a locally Noetherian integral algebraic space, at the hypotheses of the source; the defining difference-of-lengths formula is AlgebraicGeometry.Space.ordRationalFunction_eq_length_sub_length”.

Stacks 0ENL. The order of vanishing of f along Z, for f an invertible rational function on a locally Noetherian integral algebraic space X and Z a prime divisor of X: the order of vanishing, along Z, of the image of f in the total ring of fractions of the henselian local ring at the generic point of Z under the canonical injection of Stacks 0ENK.

The hypotheses are those of the source and no others — the conclusions of Stacks 0ENK are discharged by AlgebraicGeometry.Space.genericFractionEmbedding, and decency comes from integrality by Stacks 0AD4 — and the defining difference of lengths is AlgebraicGeometry.Space.ordRationalFunction_eq_length_sub_length.

abbrev ordRationalFunction (f : (rationalFunctions B S hS hX)ˣ)
    (Z : PrimeDivisor B S hS X) : ℤ

AlgebraicGeometry.Space.ordRationalFunction_eq_length_sub_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OrderOfVanishingRationalFunction.lean, line 102. The attribute's comment: “the difference-of-lengths formula defining ord_Z(f), on an arbitrary presentation of the image of f in Q(𝒪^h_{X, ξ}) as a ratio of nonzerodivisors; hence also the independence of the presentation, which the source cites Algebra, Lemma 02MC for”.

Stacks 0ENL, the defining formula. If the image of f in Q(𝒪^h_{X, ξ}) is the ratio a / b of nonzerodivisors a and b of 𝒪^h_{X, ξ}, then ord_Z(f) is the difference of the lengths of 𝒪^h_{X, ξ} / a 𝒪^h_{X, ξ} and 𝒪^h_{X, ξ} / b 𝒪^h_{X, ξ}.

The hypothesis is placed on an arbitrary such presentation, so this is simultaneously the formula the source defines ord_Z(f) by and the independence of that formula from the choice of a and b, which the source takes from Algebra, Lemma 02MC.

theorem ordRationalFunction_eq_length_sub_length (f : (rationalFunctions B S hS hX)ˣ)
    (Z : PrimeDivisor B S hS X)
    (a b : nonZeroDivisors ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace))
    (hab : Z.rationalFunctionsToGenericTotalFractionRing B S hS hX hInt.isDecentSpace hInt hN
        (f : rationalFunctions B S hS hX) =
      IsLocalization.mk' (Z.genericTotalFractionRing B S hS hX hInt.isDecentSpace)
        (a : ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace)) b) :
    ordRationalFunction B S hS hX hInt hN f Z =
      ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace)
          (a : ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace))).toNat : ℤ) -
        ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace)
          (b : ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace))).toNat : ℤ)

AlgebraicGeometry.Space.exists_ordRationalFunction_eq_length_sub_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OrderOfVanishingRationalFunction.lean, line 141. The attribute's comment: “existence of the presentation a/b by nonzerodivisors of the image of f in Q(𝒪^h_{X, ξ}), which is what makes the difference of lengths an admissible description of ord_Z(f)”.

Stacks 0ENL, well-definedness. The image of an invertible rational function f in Q(𝒪^h_{X, ξ}) is a ratio a / b of nonzerodivisors of 𝒪^h_{X, ξ}, and for one — hence, by AlgebraicGeometry.Space.ordRationalFunction_eq_length_sub_length, for every — such presentation ord_Z(f) is the difference of the lengths of 𝒪^h_{X, ξ} / a 𝒪^h_{X, ξ} and 𝒪^h_{X, ξ} / b 𝒪^h_{X, ξ}.

The source defines ord_Z(f) by that difference, for a and b nonzerodivisors such that the image of f is a / b, so the existence of such a pair is what makes the difference of lengths an admissible description of ord_Z(f). Invertibility of f is what produces it: the image of f is a unit of the total ring of fractions, and the numerator of any presentation of a unit is again a nonzerodivisor.

theorem exists_ordRationalFunction_eq_length_sub_length (f : (rationalFunctions B S hS hX)ˣ)
    (Z : PrimeDivisor B S hS X) :
    ∃ a b : nonZeroDivisors ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace),
      Z.rationalFunctionsToGenericTotalFractionRing B S hS hX hInt.isDecentSpace hInt hN
            (f : rationalFunctions B S hS hX) =
          IsLocalization.mk' (Z.genericTotalFractionRing B S hS hX hInt.isDecentSpace)
            (a : ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace)) b ∧
        ordRationalFunction B S hS hX hInt hN f Z =
          ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace)
              (a : ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace))).toNat : ℤ) -
            ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace)
              (b : ↥(Z.genericHenselianLocalRing B S hS hX hInt.isDecentSpace))).toNat : ℤ)

Tag 0ENM, a lemma

Tag 0ENM in the Stacks Project.

AlgebraicGeometry.Space.PrimeDivisor.ord_eq_ordTotalFracInt_chartPointRationalFunctionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/KeyFormulaChart/RationalFunctionOrder.lean, line 410. The attribute's comment: “at an arbitrary affine étale chart, not necessarily integral, through a point over the generic point of the prime divisor: the order of vanishing is the one of the total ring of fractions of the local ring of the chart at the point”.

Stacks 0ENM at an arbitrary affine étale chart. Let Z be a prime divisor of a decent, locally Noetherian, integral algebraic space X, let V be an affine étale chart of X and v a point of its scheme over the generic point of Z. Then the order of vanishing along Z of an invertible rational function f is the order of vanishing at v of the reading of f in the total ring of fractions of 𝒪_{V, v}.

Unlike AlgebraicGeometry.Space.PrimeDivisor.ord_eq_scheme_ord_of_chart the chart need not be an elementary étale neighbourhood, nor integral: 𝒪_{V, v} is a reduced one-dimensional local ring, possibly with several minimal primes, and its order of vanishing is the one on its total ring of fractions. The proof compares the chart with the chosen elementary étale neighbourhood of the generic point at a common affine refinement (AlgebraicGeometry.Space.ordTotalFracInt_chartPointRationalFunctionMap_eq) and the neighbourhood with the henselian local ring (AlgebraicGeometry.Space.PrimeDivisor.ord_eq_ordTotalFracInt_genericEtaleChart).

The dimension hypothesis on 𝒪_{V, v}, needed to state the right-hand side, is AlgebraicGeometry.Space.PrimeDivisor.krullDimLE_chartStalk.

theorem PrimeDivisor.ord_eq_ordTotalFracInt_chartPointRationalFunctionMap
    (hInt : IsIntegralSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} => IsLocallyNoetherian Y))
    (V : SmallEtale B S hS X) [IsAffine V.obj.left.left.1] [IsReduced V.obj.left.left.1]
    [IsLocallyNoetherian V.obj.left.left.1] (v : V.obj.left.left.1)
    (hv : chartSchemeToPoints B S hS X V v = Z.genericPoint B S hS X)
    [Ring.KrullDimLE 1 (V.obj.left.left.1.presheaf.stalk v)]
    (f : (rationalFunctions B S hS hX)ˣ) :
    (genericFractionEmbedding B S hS hX hdec hInt hN).ord f Z =
      Ring.ordTotalFracInt (V.obj.left.left.1.presheaf.stalk v)
        (chartPointRationalFunctionMap B S hS hX V v (f : rationalFunctions B S hS hX))
        (f.isUnit.map _)

AlgebraicGeometry.Space.PrimeDivisor.ord_functionFieldToTotalFractionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OrderOfVanishingChartComparison.lean, line 207. The attribute's comment: “with the shrinking step of the proof carried: in place of the hypothesis that Z meets the schematic locus of X, an elementary étale neighbourhood U of the generic point of Z whose scheme is integral and locally Noetherian and whose marked point has codimension one is given, the rational function is one of U, and it is compared along the induced map on total rings of fractions; Noetherianness and the dimension bound for the henselian local ring are hypotheses”.

Stacks 0ENM. The order of vanishing along a prime divisor Z of the image of a nonzero rational function f of an elementary étale neighbourhood U of the generic point of Z is the order of vanishing of f at the marked point of U in the sense of Divisors, Definition 02RJ.

Both sides are a difference of lengths, and the canonical map from the stalk of U into the henselian local ring is the structure map of a henselization, so it leaves those lengths unchanged.

theorem PrimeDivisor.ord_functionFieldToTotalFractionRing
    (hcoh : coheight U.point = 1) (f : ↥U.scheme.left.1.functionField) (hf : f ≠ 0) :
    Z.ord B S hS hX hdec (Z.functionFieldToTotalFractionRing B S hS hX hdec U f)
        ((isUnit_iff_ne_zero.mpr hf).map
          (Z.functionFieldToTotalFractionRing B S hS hX hdec U)) =
      U.scheme.left.1.ord f U.point

AlgebraicGeometry.Space.PrimeDivisor.ord_mk'_eq_ord_mk'_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OrderOfVanishingEtaleChart.lean, line 439. The attribute's comment: “at an arbitrary étale chart, routed through the étale local ring at a geometric point rather than through the canonical map into the henselian local ring: in place of the hypothesis that Z meets the schematic locus of X, a small étale neighbourhood (U, u) of a geometric point whose scheme is integral and locally Noetherian and whose point has codimension one is given, and the two fractions are compared through their images in 𝒪_{X, x̄}. Noetherianness and the dimension bound for the henselian local ring are hypotheses”.

Stacks 0ENM at an arbitrary étale chart. Let Z be a prime divisor of a decent algebraic space X with generic point ξ, let x̄ be a geometric point of X, and let (U, u) be a small étale neighbourhood of x̄ whose scheme is integral and locally Noetherian and whose point has codimension one. Let a / b be a fraction of nonzerodivisors of 𝒪^h_{X, ξ} and c / d one of nonzerodivisors of 𝒪_{U, u} whose numerators and denominators agree in 𝒪_{X, x̄}, along a map ψ : 𝒪^h_{X, ξ} → 𝒪_{X, x̄} leaving Ring.ord unchanged and the canonical map of Stacks 05VP. Then the order of vanishing of a / b along Z is the order of vanishing of c / d at u in the sense of Divisors, Definition 02RJ.

Both sides are a difference of two Ring.ords, by AlgebraicGeometry.Space.PrimeDivisor.ord_mk' and AlgebraicGeometry.Scheme.ord_mk', and the four Ring.ords are pairwise equal: the canonical map of Stacks 05VP is the structure map of a strict henselization, so it leaves Ring.ord unchanged (AlgebraicGeometry.Space.ord_chartLocalRingToEtaleLocalRing), and hψ says the same of ψ.

The hypothesis hψ is supplied by AlgebraicGeometry.Space.exists_ringHom_ord_henselianLocalRing at any geometric point above ξ; unlike the elementary-neighbourhood comparison AlgebraicGeometry.Space.PrimeDivisor.ord_functionFieldToTotalFractionRing, nothing here asks that (U, u) be an elementary étale neighbourhood of ξ, which is what makes the statement usable on a chart chosen for a different reason — in the proof of Stacks 0EPX, one trivializing an invertible module.

theorem PrimeDivisor.ord_mk'_eq_ord_mk'_chart
    [Nontrivial ↥(Z.genericHenselianLocalRing B S hS hX hdec)]
    [IsNoetherianRing ↥(Z.genericHenselianLocalRing B S hS hX hdec)]
    [Ring.KrullDimLE 1 ↥(Z.genericHenselianLocalRing B S hS hX hdec)]
    {xbar : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood xbar)
    [AlgebraicGeometry.IsIntegral (chartScheme V.chart)]
    [IsLocallyNoetherian (chartScheme V.chart)]
    (ψ : ↥(Z.genericHenselianLocalRing B S hS hX hdec) →+*
      (etaleLocalRing B S hS X xbar : Type (u + 1)))
    (hψ : ∀ r, Ring.ord (etaleLocalRing B S hS X xbar : Type (u + 1)) (ψ r) =
      Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec) r)
    (hcoh : coheight (chartPoint B S hS X V) = 1)
    (a b : (↥(Z.genericHenselianLocalRing B S hS hX hdec))⁰)
    (c d : (↥(chartLocalRing B S hS X V))⁰)
    (hac : ψ (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec)) =
      chartLocalRingToEtaleLocalRing B S hS X hX V (c : ↥(chartLocalRing B S hS X V)))
    (hbd : ψ (b : ↥(Z.genericHenselianLocalRing B S hS hX hdec)) =
      chartLocalRingToEtaleLocalRing B S hS X hX V (d : ↥(chartLocalRing B S hS X V)))
    (hu : IsUnit (IsLocalization.mk' (Z.genericTotalFractionRing B S hS hX hdec)
      (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec)) b)) :
    Z.ord B S hS hX hdec (IsLocalization.mk' (Z.genericTotalFractionRing B S hS hX hdec)
        (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec)) b) hu =
      (chartScheme V.chart).ord
        (IsLocalization.mk' (chartScheme V.chart).functionField
          (c : ↥(chartLocalRing B S hS X V)) d) (chartPoint B S hS X V)

AlgebraicGeometry.Space.PrimeDivisor.exists_affine_schematic_neighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OrderOfVanishingSchematicLocus.lean, line 106. The attribute's comment: “the shrinking step of the proof, with the neighbourhood affine: from the hypothesis that the prime divisor meets the schematic locus, an affine elementary étale neighbourhood of its generic point whose scheme is integral, locally Noetherian and of codimension one at the marked point”.

Stacks 0ENM, the shrinking step of the proof in affine form. If a prime divisor Z of a locally Noetherian integral algebraic space X meets the schematic locus of X, then the generic point of Z has an affine elementary étale neighbourhood whose scheme is integral, locally Noetherian and of codimension one at the marked point.

The schematic locus itself is such a neighbourhood except for affineness, by AlgebraicGeometry.Space.PrimeDivisor.exists_schematic_neighborhood; restricting it to an affine open around the marked point preserves integrality and local Noetherianness, as properties of an open subscheme, and preserves the codimension of the marked point because codimension is computed in any open neighbourhood.

theorem PrimeDivisor.exists_affine_schematic_neighborhood
    (hmeet : (Z.support B S hS X ∩
      subspacePointSet B S hS X (schematicLocus B S hS X)).Nonempty) :
    ∃ U : ElementaryEtaleNeighborhood B S hS X hX (Z.genericPoint B S hS X),
      IsAffine U.scheme.left.1 ∧
      AlgebraicGeometry.IsIntegral U.scheme.left.1 ∧
      IsLocallyNoetherian U.scheme.left.1 ∧
      coheight U.point = 1

AlgebraicGeometry.Space.PrimeDivisor.ord_eq_scheme_ord, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OrderOfVanishingSchematicLocus.lean, line 242.

Stacks 0ENM. Let S be a scheme, let X be a locally Noetherian integral algebraic space over S and let f ∈ R(X)^*. If the prime divisor Z ⊂ X meets the schematic locus of X, then the order of vanishing ord_Z(f) of Definition 0ENL agrees with the order of vanishing of Divisors, Definition 02RJ.

After shrinking X to the schematic locus and then to an affine open around the generic point ξ of Z we are on an integral Noetherian affine scheme U with a point of codimension one; there 𝒪^h_{X, ξ} is a henselization of 𝒪_{U, u}, so the two orders of vanishing, each a difference of lengths, agree.

The hypotheses are exactly those of the source: decency, which the henselian local ring and hence the order of vanishing of Definition 0ENL are defined from, is part of integrality of an algebraic space — Stacks 0AD4, AlgebraicGeometry.Space.IsIntegralSpace — and is taken from hInt rather than assumed separately.

theorem PrimeDivisor.ord_eq_scheme_ord
    (hmeet : (Z.support B S hS X ∩
      subspacePointSet B S hS X (schematicLocus B S hS X)).Nonempty)
    (f : (rationalFunctions B S hS hX)ˣ) :
    ∃ (U : ElementaryEtaleNeighborhood B S hS X hX (Z.genericPoint B S hS X))
      (_ : IsAffine U.scheme.left.1) (_ : AlgebraicGeometry.IsIntegral U.scheme.left.1)
      (_ : IsLocallyNoetherian U.scheme.left.1),
      coheight U.point = 1 ∧
        (genericFractionEmbedding B S hS hX (hInt.isDecentSpace B S hS X) hInt hN).ord f Z =
          U.scheme.left.1.ord
            (rationalFunctionsToFunctionField B S hS hX U.scheme U.point U.toSpace
              U.etale_toSpace (f : rationalFunctions B S hS hX)) U.point

AlgebraicGeometry.Space.PrimeDivisor.exists_schematic_neighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchematicNeighborhoodOfPrimeDivisor.lean, line 129. The attribute's comment: “the shrinking step of the proof: from the hypothesis that the prime divisor meets the schematic locus, an elementary étale neighbourhood of its generic point which is an open immersion and whose scheme is integral, locally Noetherian and of codimension one at the marked point”.

Stacks 0ENM, the shrinking step of the proof. If a prime divisor Z of a locally Noetherian integral algebraic space X meets the schematic locus of X, then the generic point of Z has an elementary étale neighbourhood whose structure morphism is an open immersion and whose scheme is integral, locally Noetherian and of codimension one at the marked point.

The neighbourhood is the schematic locus itself: it is an open subspace represented by a scheme V by Stacks 03JH, its point set is open in |X| and meets |Z|, hence contains the generic point ξ of Z, and the point v ∈ V over ξ has codimension one because |V| → |X| is an open embedding.

theorem PrimeDivisor.exists_schematic_neighborhood
    (hmeet : (Z.support B S hS X ∩
      subspacePointSet B S hS X (schematicLocus B S hS X)).Nonempty) :
    ∃ U : ElementaryEtaleNeighborhood B S hS X hX (Z.genericPoint B S hS X),
      IsOpenImmersion B S hS U.toSpace ∧
      AlgebraicGeometry.IsIntegral U.scheme.left.1 ∧
      IsLocallyNoetherian U.scheme.left.1 ∧
      coheight U.point = 1

Tag 0ENN, a lemma

Tag 0ENN in the Stacks Project.

AlgebraicGeometry.Space.locallyFinite_principalDivisorCoefficients_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrincipalDivisor.lean, line 288. The attribute's comment: “the second set: the prime divisors with ord_Z(f) ≠ 0 are locally finite. The first set, the prime divisors at whose generic point f is not regular, is locallyFinite_primeDivisor_not_isDefinedAt”.

Stacks 0ENN, the second set. The prime divisors of X along which a rational function f has nonzero order of vanishing are locally finite in |X|, given a nonempty open subset of |X| over which f is invertible.

This is the source's argument. Such a prime divisor has its generic point outside the open set, by AlgebraicGeometry.Space.genericPoint_notMem_of_principalDivisorCoefficients_ne_zero, so its point set is an irreducible component of the closed complement — codimension one leaves no room for a larger irreducible closed subset of that complement — and the irreducible components of a closed set are locally finite by Stacks 0EE5. Both steps are AlgebraicGeometry.Space.locallyFinite_primeDivisor_of_genericPoint_notMem, already in the library in exactly this generality; it is also the Stacks 0EE5 step in the proof of Stacks 0EPS.

theorem locallyFinite_principalDivisorCoefficients_ne_zero
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} => IsLocallyNoetherian Y))
    (hirr : IrreducibleSpace (points B S hS X))
    (emb : ∀ W : PrimeDivisor B S hS X, rationalFunctions B S hS hX →+*
      W.genericTotalFractionRing B S hS hX hdec)
    (f : rationalFunctions B S hS hX)
    (hf : ∀ W : PrimeDivisor B S hS X, IsUnit (emb W f))
    (U : Set (points B S hS X)) (hUopen : IsOpen U) (hUne : U.Nonempty)
    (hreg : ∀ W : PrimeDivisor B S hS X, W.genericPoint B S hS X ∈ U →
      ∃ r : ↥(W.genericHenselianLocalRing B S hS hX hdec), IsUnit r ∧
        emb W f = algebraMap _ (W.genericTotalFractionRing B S hS hX hdec) r) :
    LocallyFinite fun W : PrimeDivisor B S hS X =>
      if principalDivisorCoefficients B S hS hX hdec emb f hf W = 0 then ∅
      else W.support B S hS X

AlgebraicGeometry.Space.locallyFinite_primeDivisor_not_isDefinedAt_and_ordRationalFunction_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvertibleRationalFunctionUnitLocus.lean, line 298. The attribute's comment: “both collections, with the source's hypotheses only: the prime divisors at whose generic point f is not defined (f ∉ 𝒪_{X,ξ}) and those with ord_Z(f) ≠ 0 are locally finite”.

Stacks 0ENN. Let X be a locally Noetherian integral algebraic space over S and let f ∈ R(X)^*. Then the prime divisors Z of X whose generic point ξ has f ∉ 𝒪_{X, ξ} — f not defined at ξ in the sense of Stacks 0EMQ — and the prime divisors Z with ord_Z(f) ≠ 0, for the order of vanishing of Stacks 0ENL, are both locally finite collections in |X|.

As in the source, both follow from Stacks 0EE5 once the generic points of the prime divisors in question avoid a nonempty open. For the first collection that open is the domain of a representative of f, which is AlgebraicGeometry.Space.locallyFinite_primeDivisor_not_isDefinedAt; for the second it is the open on which f is a unit section, which is AlgebraicGeometry.Space.ordRationalFunction_mem_weilDivisor.

theorem locallyFinite_primeDivisor_not_isDefinedAt_and_ordRationalFunction_ne_zero
    (f : (rationalFunctions B S hS hX)ˣ) :
    LocallyFinite (fun Z : {Z : PrimeDivisor B S hS X //
        ¬ RationalMap.IsDefinedAt B S hS (f : rationalFunctions B S hS hX)
          (Z.genericPoint B S hS X)} ↦ Z.1.support B S hS X) ∧
    LocallyFinite (fun Z : {Z : PrimeDivisor B S hS X //
        ordRationalFunction B S hS hX hInt hN f Z ≠ 0} ↦ Z.1.support B S hS X)

Tag 0ENP, a definition

Tag 0ENP in the Stacks Project.

AlgebraicGeometry.Space.principalDivisorCoefficients, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrincipalDivisor.lean, line 219. The attribute's comment: “the coefficients ord_Z(f) of div(f); the embeddings R(X) → Q(O^h_{X,ξ}) of Stacks 0ENK are the parameter emb, as they are for Stacks 0EPT”.

Stacks 0ENP, the coefficients. The coefficients ord_Z(f) of the principal divisor div(f) = ∑_Z ord_Z(f) [Z] of a rational function f on X, indexed by the prime divisors of X: the coefficient at Z is the order of vanishing along Z of the image of f in the total ring of fractions of 𝒪^h_{X,ξ}.

The embeddings R(X) → Q(𝒪^h_{X,ξ}) of Stacks 0ENK are the parameter emb, as in Stacks 0EPT; regularity of f is the hypothesis hf that each image is a unit.

def principalDivisorCoefficients
    (emb : ∀ W : PrimeDivisor B S hS X, rationalFunctions B S hS hX →+*
      W.genericTotalFractionRing B S hS hX hdec)
    (f : rationalFunctions B S hS hX)
    (hf : ∀ W : PrimeDivisor B S hS X, IsUnit (emb W f)) :
    PrimeDivisor B S hS X → ℤ

AlgebraicGeometry.Space.principalWeilDivisor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrincipalDivisor.lean, line 320. The attribute's comment: “div(f) = ∑ ord_Z(f) [Z] as an element of Div(X); local finiteness is Stacks 0ENN, the argument hfin, discharged by locallyFinite_principalDivisorCoefficients_ne_zero in principalWeilDivisorOfRegularLocus; the embeddings of Stacks 0ENK are the parameter emb”.

Stacks 0ENP. The principal divisor associated to f ∈ R(X)^*, that is div(f) = ∑_Z ord_Z(f) [Z], as an element of Div(X).

That the sum makes sense is Stacks 0ENN, the argument hfin, which AlgebraicGeometry.Space.locallyFinite_principalDivisorCoefficients_ne_zero proves and AlgebraicGeometry.Space.principalWeilDivisorOfRegularLocus discharges from a nonempty open subset of |X| over which f is invertible.

def principalWeilDivisor
    (emb : ∀ W : PrimeDivisor B S hS X, rationalFunctions B S hS hX →+*
      W.genericTotalFractionRing B S hS hX hdec)
    (f : rationalFunctions B S hS hX)
    (hf : ∀ W : PrimeDivisor B S hS X, IsUnit (emb W f))
    (hfin : LocallyFinite fun W : PrimeDivisor B S hS X =>
      if principalDivisorCoefficients B S hS hX hdec emb f hf W = 0 then ∅
      else W.support B S hS X) :
    WeilDivisor B S hS X

AlgebraicGeometry.Space.principalWeilDivisorOfRegularLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrincipalDivisor.lean, line 352. The attribute's comment: “div(f) in Div(X), with local finiteness (Stacks 0ENN) discharged here: it is proved from a nonempty open U over which f is invertible, the datum (U, hUopen, hUne, hreg) that is the first sentence of the source's own proof of Stacks 0ENN”.

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

def principalWeilDivisorOfRegularLocus
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} => IsLocallyNoetherian Y))
    (hirr : IrreducibleSpace (points B S hS X))
    (emb : ∀ W : PrimeDivisor B S hS X, rationalFunctions B S hS hX →+*
      W.genericTotalFractionRing B S hS hX hdec)
    (f : rationalFunctions B S hS hX)
    (hf : ∀ W : PrimeDivisor B S hS X, IsUnit (emb W f))
    (U : Set (points B S hS X)) (hUopen : IsOpen U) (hUne : U.Nonempty)
    (hreg : ∀ W : PrimeDivisor B S hS X, W.genericPoint B S hS X ∈ U →
      ∃ r : ↥(W.genericHenselianLocalRing B S hS hX hdec), IsUnit r ∧
        emb W f = algebraMap _ (W.genericTotalFractionRing B S hS hX hdec) r) :
    WeilDivisor B S hS X

AlgebraicGeometry.Space.principalWeilDivisorOfUnit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrincipalWeilDivisorOfUnit.lean, line 144. The attribute's comment: “div(f) = ∑ ord_Z(f) [Z] as an element of Div(X), for X a locally Noetherian integral algebraic space over S and f ∈ R(X)^*: the order of vanishing of Stacks 0ENL along the canonical embedding R(X) → Q(O^h_{X,ξ}) of Stacks 0ENK, whose ring-theoretic properties are proved; the local finiteness of Stacks 0ENN is proved, nothing is carried”.

The principal Weil divisor associated to f ∈ R(X)^*, div(f) = div_X(f) = ∑_Z ord_Z(f) [Z], as an element of Div(X), for X a locally Noetherian integral algebraic space over S.

The sum is over the prime divisors of X, and ord_Z(f) is the order of vanishing of Stacks 0ENL, taken along the canonical embedding R(X) → Q(𝒪^h_{X, ξ}) of Stacks 0ENK (AlgebraicGeometry.Space.genericFractionEmbedding).

def principalWeilDivisorOfUnit (f : (rationalFunctions B S hS hX)ˣ) :
    ↥(WeilDivisor B S hS X)

AlgebraicGeometry.Space.divRationalFunction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PrincipalWeilDivisorRationalFunction.lean, line 70. The attribute's comment: “div_X(f) = ∑ ord_Z(f) [Z] as a Weil divisor, at the hypotheses of the source: the order of vanishing is the canonical one of Stacks 0ENL and the local finiteness is Stacks 0ENN, both proved”.

Stacks 0ENP. The principal Weil divisor div_X(f) = ∑ ord_Z(f) [Z] of an invertible rational function f on a locally Noetherian integral algebraic space X, the sum running over the prime divisors Z of X and ord_Z(f) being the order of vanishing of Stacks 0ENL. It is a Weil divisor by Stacks 0ENN, which is AlgebraicGeometry.Space.ordRationalFunction_mem_weilDivisor.

abbrev divRationalFunction (f : (rationalFunctions B S hS hX)ˣ) : ↥(WeilDivisor B S hS X)

Tag 0ENQ, a lemma

Tag 0ENQ in the Stacks Project.

AlgebraicGeometry.Space.principalWeilDivisor_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrincipalDivisor.lean, line 422. The attribute's comment: “div(fg) = div(f) + div(g) in Div(X)”.

Stacks 0ENQ. The principal divisor of a product of rational functions is the sum of their principal divisors, div(fg) = div(f) + div(g) in Div(X).

Local finiteness for fg is not assumed: it is deduced from local finiteness for f and for g, which is what makes div(f) and div(g) elements of Div(X) in the first place.

theorem principalWeilDivisor_mul
    (emb : ∀ W : PrimeDivisor B S hS X, rationalFunctions B S hS hX →+*
      W.genericTotalFractionRing B S hS hX hdec)
    (f g : rationalFunctions B S hS hX)
    (hf : ∀ W : PrimeDivisor B S hS X, IsUnit (emb W f))
    (hg : ∀ W : PrimeDivisor B S hS X, IsUnit (emb W g))
    (hfg : ∀ W : PrimeDivisor B S hS X, IsUnit (emb W (f * g)))
    (hfinf : LocallyFinite fun W : PrimeDivisor B S hS X =>
      if principalDivisorCoefficients B S hS hX hdec emb f hf W = 0 then ∅
      else W.support B S hS X)
    (hfing : LocallyFinite fun W : PrimeDivisor B S hS X =>
      if principalDivisorCoefficients B S hS hX hdec emb g hg W = 0 then ∅
      else W.support B S hS X) :
    principalWeilDivisor B S hS hX hdec emb (f * g) hfg
        (locallyFinite_principalDivisorCoefficients_mul B S hS hX hdec emb f g hf hg hfg hfinf
          hfing) =
      principalWeilDivisor B S hS hX hdec emb f hf hfinf +
        principalWeilDivisor B S hS hX hdec emb g hg hfing

AlgebraicGeometry.Space.principalWeilDivisorOfRegularLocus_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/PrincipalDivisor.lean, line 504. The attribute's comment: “div(fg) = div(f) + div(g) in Div(X), local finiteness proved throughout”.

Stacks 0ENQ. The principal divisor of a product of rational functions is the sum of their principal divisors, div(fg) = div(f) + div(g) in Div(X), with the local finiteness of Stacks 0ENN proved for all three divisors from a nonempty open subset of |X| over which both f and g are invertible.

theorem principalWeilDivisorOfRegularLocus_mul
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} => IsLocallyNoetherian Y))
    (hirr : IrreducibleSpace (points B S hS X))
    (emb : ∀ W : PrimeDivisor B S hS X, rationalFunctions B S hS hX →+*
      W.genericTotalFractionRing B S hS hX hdec)
    (f g : rationalFunctions B S hS hX)
    (hf : ∀ W : PrimeDivisor B S hS X, IsUnit (emb W f))
    (hg : ∀ W : PrimeDivisor B S hS X, IsUnit (emb W g))
    (hfg : ∀ W : PrimeDivisor B S hS X, IsUnit (emb W (f * g)))
    (U : Set (points B S hS X)) (hUopen : IsOpen U) (hUne : U.Nonempty)
    (hregf : ∀ W : PrimeDivisor B S hS X, W.genericPoint B S hS X ∈ U →
      ∃ r : ↥(W.genericHenselianLocalRing B S hS hX hdec), IsUnit r ∧
        emb W f = algebraMap _ (W.genericTotalFractionRing B S hS hX hdec) r)
    (hregg : ∀ W : PrimeDivisor B S hS X, W.genericPoint B S hS X ∈ U →
      ∃ r : ↥(W.genericHenselianLocalRing B S hS hX hdec), IsUnit r ∧
        emb W g = algebraMap _ (W.genericTotalFractionRing B S hS hX hdec) r) :
    principalWeilDivisorOfRegularLocus B S hS hX hdec hN hirr emb (f * g) hfg U hUopen hUne
        (exists_isUnit_emb_mul_eq_algebraMap B S hS hX hdec emb f g U hregf hregg) =
      principalWeilDivisorOfRegularLocus B S hS hX hdec hN hirr emb f hf U hUopen hUne hregf +
        principalWeilDivisorOfRegularLocus B S hS hX hdec hN hirr emb g hg U hUopen hUne hregg

AlgebraicGeometry.Space.divRationalFunction_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PrincipalWeilDivisorRationalFunction.lean, line 96. The attribute's comment: “div_X(fg) = div_X(f) + div_X(g) as Weil divisors on X, at the hypotheses of the source only”.

Stacks 0ENQ. Let X be a locally Noetherian integral algebraic space over S and let f, g ∈ R(X)^*. Then div_X(fg) = div_X(f) + div_X(g) as Weil divisors on X.

As in the source this is the additivity of the order of vanishing, AlgebraicGeometry.Space.GenericFractionEmbedding.ord_mul_apply, at every prime divisor.

theorem divRationalFunction_mul (f g : (rationalFunctions B S hS hX)ˣ) :
    divRationalFunction B S hS hX hInt hN (f * g) =
      divRationalFunction B S hS hX hInt hN f + divRationalFunction B S hS hX hInt hN g

AlgebraicGeometry.Space.GenericFractionEmbedding.ord_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeilDivisorClassGroup.lean, line 146. The attribute's comment: “additivity of the principal Weil divisor, read on the coefficient families over the prime divisors; this form needs no hypothesis beyond the embedding of Stacks 0ENK”.

Stacks 0ENQ. The order of vanishing of a product of invertible rational functions is the sum of the orders of vanishing, as coefficient families on the prime divisors of X.

This is the equation div(fg) = div(f) + div(g) of the source, read on the coefficient families of which the two sides of that equation are the Weil divisors.

theorem ord_mul (f g : (rationalFunctions B S hS hX)ˣ) :
    E.ord (f * g) = E.ord f + E.ord g

Tag 0ENR, a definition

Tag 0ENR in the Stacks Project.

AlgebraicGeometry.Space.GenericFractionEmbedding.principalWeilDivisors, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeilDivisorClassGroup.lean, line 190. The attribute's comment: “the subgroup of principal Weil divisors, by which the class group is formed”.

Stacks 0ENR. The subgroup of Div(X) of principal Weil divisors: they contain zero and are closed under addition and negation by the additivity of the order of vanishing, which is Stacks 0ENQ.

def principalWeilDivisors : AddSubgroup ↥(WeilDivisor B S hS X)

AlgebraicGeometry.Space.GenericFractionEmbedding.weilDivisorClassGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeilDivisorClassGroup.lean, line 213. The attribute's comment: “the Weil divisor class group as the quotient of the Weil divisors by the principal Weil divisors”.

Stacks 0ENR. The Weil divisor class group Cl(X) of X: the group of Weil divisors on X modulo the subgroup of principal Weil divisors.

abbrev weilDivisorClassGroup : Type (u + 1)

AlgebraicGeometry.Space.weilDivisorClassGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeilDivisorClassGroupCanonical.lean, line 97. The attribute's comment: “Cl(X) = Div(X) / {div(f) : f ∈ R(X)^*}, at the source's hypotheses only: the principal divisors are the range of the homomorphism div of Stacks 0ENP and 0ENQ, built from the canonical order of vanishing”.

Stacks 0ENR. The Weil divisor class group Cl(X) of a locally Noetherian integral algebraic space X over S: the quotient of the group Div(X) of Weil divisors by the subgroup of principal Weil divisors div(f), f ∈ R(X)^*.

abbrev weilDivisorClassGroup : Type (u + 1)

Tag 0ENT, an example

Tag 0ENT in the Stacks Project.

AlgebraicGeometry.AffineLineInvolution.involutionQuotient_classGroup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineLineInvolutionClassGroup.lean, line 300.

Stacks 0ENT. Let k be a field of characteristic different from two and let X = 𝔸¹_k/\{t ∼ -t ∣ t ≠ 0\} be the algebraic space of Stacks 02Z1, the quotient of the affine line by the punctured graph of negation. Then:

1. X is an algebraic space, smooth over k;
2. the morphism X → 𝔸¹_k = Spec k[t] descended from squaring the coordinate is a universal homeomorphism which is an isomorphism over 𝔸¹_k ∖ {0};
3. X is Noetherian and integral, and |X| has dimension one;
4. the prime divisors of X are the closed points of X, a prime divisor corresponding to its generic point;
5. the prime divisor x of X over the origin is a closed point, and the unique point of X over 0 ∈ 𝔸¹_k;
6. the classes in Cl(X) of the prime divisors other than x are zero;
7. the divisor of t on X is 2 [x];
8. Cl(X) ≅ ℤ/2ℤ, by an isomorphism sending [x] to 1.

Here Cl(X) is the Weil divisor class group of Stacks 0ENR, and t is the coordinate of the affine line, pulled back to a rational function on X.

The characteristic hypothesis is that of Stacks 02Z1, where X is constructed, which Stacks 05Z6 and Stacks 0ENT continue: in characteristic two the graph of negation is the diagonal, so the relation Δ ⨿ Γ ⟶ 𝔸¹_k ×_k 𝔸¹_k is not a monomorphism and the construction does not produce an equivalence relation at all. The hypothesis hZ that the big fppf site contains the final scheme is the one under which AlgebraicGeometry.Space.IsNoetherian is formulated.

theorem involutionQuotient_classGroup (hchar : (2 : k) ≠ 0) (hZ : B.Contains (⊤_ Scheme.{u})) :
    IsAlgebraicSpace B (Spec (.of k)) hk (involutionQuotient k B hk).obj ∧
      Space.IsSmooth B (Spec (.of k)) hk (terminal.from (involutionQuotient k B hk).obj) ∧
      Space.UniversalHomeomorphism B (Spec (.of k)) hk (squaringMap k B hk) ∧
      IsIso (pullback.snd (squaringMap k B hk) (Space.puncturedLineInclusion k B hk)) ∧
      Space.IsNoetherian B (Spec (.of k)) hk hZ (involutionQuotient k B hk).obj ∧
      Space.IsIntegralSpace B (Spec (.of k)) hk (involutionQuotient k B hk).obj ∧
      topologicalKrullDim (Space.points B (Spec (.of k)) hk (involutionQuotient k B hk).obj) = 1 ∧
      (∃ e : Space.PrimeDivisor B (Spec (.of k)) hk (involutionQuotient k B hk).obj ≃
          {ξ : Space.points B (Spec (.of k)) hk (involutionQuotient k B hk).obj //
            IsClosed ({ξ} : Set _)},
        ∀ Z, (e Z : Space.points B (Spec (.of k)) hk _) = Z.genericPoint B (Spec (.of k)) hk _) ∧
      IsClosed ({(originDivisor k B hk hchar hZ).genericPoint B (Spec (.of k)) hk _} :
        Set (Space.points B (Spec (.of k)) hk (involutionQuotient k B hk).obj)) ∧
      (∀ ξ : Space.points B (Spec (.of k)) hk (involutionQuotient k B hk).obj,
        Space.pointsHomeomorphAffineLine (squaringMap k B hk)
            (universalHomeomorphism_squaringMap k B hk hchar) ξ = origin k ↔
          ξ = (originDivisor k B hk hchar hZ).genericPoint B (Spec (.of k)) hk _) ∧
      (∀ Z : Space.PrimeDivisor B (Spec (.of k)) hk (involutionQuotient k B hk).obj,
        Z ≠ originDivisor k B hk hchar hZ →
          (Space.primeDivisorClass Z : Space.weilDivisorClassGroup B (Spec (.of k)) hk
            (isAlgebraicSpace_involutionQuotient k hchar B hk)
            (isIntegralSpace_involutionQuotient k B hk hchar hZ)
            (hasEtaleLocalProperty_isLocallyNoetherian k B hk hchar)) = 0) ∧
      Space.divRationalFunction B (Spec (.of k)) hk
          (isAlgebraicSpace_involutionQuotient k hchar B hk)
          (isIntegralSpace_involutionQuotient k B hk hchar hZ)
          (hasEtaleLocalProperty_isLocallyNoetherian k B hk hchar)
          (Space.coordinatePullbackUnit (squaringMap k B hk)
            (isAlgebraicSpace_involutionQuotient k hchar B hk)
            (isIntegralSpace_involutionQuotient k B hk hchar hZ)
            (isIso_squaringMap_pullback_puncturedAffineLine k hchar B hk)) =
        2 • Space.primeDivisorClass (originDivisor k B hk hchar hZ) ∧
      ∃ e : Space.weilDivisorClassGroup B (Spec (.of k)) hk
          (isAlgebraicSpace_involutionQuotient k hchar B hk)
          (isIntegralSpace_involutionQuotient k B hk hchar hZ)
          (hasEtaleLocalProperty_isLocallyNoetherian k B hk hchar) ≃+ ZMod 2,
        e (Space.primeDivisorClass (originDivisor k B hk hchar hZ)) = 1

AlgebraicGeometry.AffineLineInvolution.isNoetherian_involutionQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineLineInvolutionNoetherian.lean, line 69. The attribute's comment: “the Noetherian property”.

Away from characteristic two, the quotient of the affine line by the punctured graph of negation is a Noetherian algebraic space over the ground field: it is quasi-compact, quasi-separated and locally Noetherian.

theorem isNoetherian_involutionQuotient (hchar : (2 : k) ≠ 0) (B : BigFppfSite.{u})
    (hS : B.Contains (Spec (.of k))) (hZ : B.Contains (⊤_ Scheme.{u}))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)] :
    Space.IsNoetherian B (Spec (.of k)) hS hZ (involutionQuotient k B hS).obj

AlgebraicGeometry.AffineLineInvolution.isSmooth_involutionQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineLineInvolutionQuotient.lean, line 583. The attribute's comment: “smoothness”.

Stacks 0ENT. Away from characteristic two, the quotient of the affine line by the punctured graph of negation is smooth over the ground field.

Smoothness is tested on the quotient chart, which is a surjective étale chart of the quotient by Stacks 0265, and on the affine line itself, which is smooth over the base.

theorem isSmooth_involutionQuotient (hchar : (2 : k) ≠ 0) (B : BigFppfSite.{u})
    (hS : B.Contains (Spec (.of k)))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)] :
    Space.IsSmooth B (Spec (.of k)) hS
      (terminal.from (involutionQuotient k B hS).obj)

Tag 0ENU, an example

Tag 0ENU in the Stacks Project.

AlgebraicGeometry.CoordinateAxesQuotient.coordinateAxesQuotient_properties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoordinateAxesQuotientClassGroup.lean, line 271.

Stacks 0ENU. Let k be a field, U = Spec (k[x, y]/(xy)) the union of the coordinate axes, σ the automorphism exchanging them, and R = Δ(U) ⨿ Δ'(U ∖ {0_U}) where Δ' is the graph u ↦ (u, σ(u)). Then: 1. R is an étale equivalence relation on U, and X = U/R is an algebraic space; 2. the morphism U → 𝔸¹_k, (x, y) ↦ x + y, is R-invariant and defines π : X → 𝔸¹_k; 3. π is a universal homeomorphism and an isomorphism over 𝔸¹_k ∖ {0}; 4. X is integral and Noetherian; 5. as in Stacks 0ENT, the prime divisors of X are its closed points, the point x of X over 0 ∈ 𝔸¹_k is closed and is the only point over 0, the divisor of t is 2 [x], the class of every other prime divisor is zero, and Cl(X) ≅ ℤ/2ℤ by an isomorphism sending [x] to 1; 6. the henselian local ring of X at x is a henselization of 𝒪_{U, 0_U}, and it is not a domain. No hypothesis is put on the field. The hypothesis hZ that the big fppf site contains the final scheme is the one under which AlgebraicGeometry.Space.IsNoetherian is formulated; the integrality, the class group and the henselian local ring, which is defined for decent spaces, use it through the decency of a Noetherian space.

theorem coordinateAxesQuotient_properties (hZ : B.Contains (⊤_ Scheme.{u})) :
    Stacks.Groupoids.IsEtaleEquivalenceRelation (relationPreRelation S) ∧
      IsAlgebraicSpace B (Spec (.of S.k)) hS (quotientSpace S B hS).obj ∧
      quotientMap S B hS ≫ sumMap S B hS =
        (Over.post (X := B.obj hS) B.inclusion).op.whiskerLeft
          (yoneda.map (coordinateSumMap S)) ∧
      Space.UniversalHomeomorphism B (Spec (.of S.k)) hS (sumMap S B hS) ∧
      IsIso (pullback.snd (sumMap S B hS) (Space.puncturedLineInclusion S.k B hS)) ∧
      Space.IsIntegralSpace B (Spec (.of S.k)) hS (quotientSpace S B hS).obj ∧
      Space.IsNoetherian B (Spec (.of S.k)) hS hZ (quotientSpace S B hS).obj ∧
      (∀ ξ : Space.points B (Spec (.of S.k)) hS (quotientSpace S B hS).obj,
        (∃ Z : Space.PrimeDivisor B (Spec (.of S.k)) hS (quotientSpace S B hS).obj,
          Z.genericPoint B (Spec (.of S.k)) hS _ = ξ) ↔ IsClosed {ξ}) ∧
      (originDivisor S B hS hZ).genericPoint B (Spec (.of S.k)) hS _ = originPoint S B hS ∧
      IsClosed {originPoint S B hS} ∧
      (∀ ξ : Space.points B (Spec (.of S.k)) hS (quotientSpace S B hS).obj,
        Space.pointsHomeomorphAffineLine (sumMap S B hS) (universalHomeomorphism_sumMap B S hS) ξ =
            AffineLineInvolution.origin S.k ↔ ξ = originPoint S B hS) ∧
      Space.divRationalFunction B (Spec (.of S.k)) hS (isAlgebraicSpace_quotientSpace S B hS)
          (isIntegralSpace_quotientSpace S B hS hZ)
          (hasEtaleLocalProperty_isLocallyNoetherian S B hS)
          (Space.coordinatePullbackUnit (sumMap S B hS) (isAlgebraicSpace_quotientSpace S B hS)
            (isIntegralSpace_quotientSpace S B hS hZ)
            (isIso_sumMap_pullback_puncturedAffineLine B S hS)) =
        2 • Space.primeDivisorClass (originDivisor S B hS hZ) ∧
      (∀ Z : Space.PrimeDivisor B (Spec (.of S.k)) hS (quotientSpace S B hS).obj,
        Z ≠ originDivisor S B hS hZ →
        (Space.primeDivisorClass Z : Space.weilDivisorClassGroup B (Spec (.of S.k)) hS
            (isAlgebraicSpace_quotientSpace S B hS)
            (isIntegralSpace_quotientSpace S B hS hZ)
            (hasEtaleLocalProperty_isLocallyNoetherian S B hS)) = 0) ∧
      (∃ e : Space.weilDivisorClassGroup B (Spec (.of S.k)) hS
            (isAlgebraicSpace_quotientSpace S B hS)
            (isIntegralSpace_quotientSpace S B hS hZ)
            (hasEtaleLocalProperty_isLocallyNoetherian S B hS) ≃+ ZMod 2,
        e (Space.primeDivisorClass (originDivisor S B hS hZ)) = 1) ∧
      (letI := Space.henselianLocalRing_isLocalRing B (Spec (.of S.k)) hS (quotientSpace S B hS).obj
          (isAlgebraicSpace_quotientSpace S B hS) (originPoint S B hS)
            (isIntegralSpace_quotientSpace S B hS hZ).isDecentSpace;
        letI := Space.stalkAlgebra B (Spec (.of S.k)) hS (quotientSpace S B hS).obj
          (isAlgebraicSpace_quotientSpace S B hS) (originPoint S B hS)
            (isIntegralSpace_quotientSpace S B hS hZ).isDecentSpace
          (originNeighborhood S B hS _ rfl);
        IsLocalRing.IsHenselization
          ((originNeighborhood S B hS _ rfl).scheme.left.1.presheaf.stalk
            (originNeighborhood S B hS _ rfl).point)
          (ResidueField ((originNeighborhood S B hS _ rfl).scheme.left.1.presheaf.stalk
            (originNeighborhood S B hS _ rfl).point))
          (Space.henselianLocalRing B (Spec (.of S.k)) hS (quotientSpace S B hS).obj
            (isAlgebraicSpace_quotientSpace S B hS) (originPoint S B hS)
              (isIntegralSpace_quotientSpace S B hS hZ).isDecentSpace : Type (u + 1))) ∧
      ¬ IsDomain (Space.henselianLocalRing B (Spec (.of S.k)) hS (quotientSpace S B hS).obj
        (isAlgebraicSpace_quotientSpace S B hS) (originPoint S B hS)
          (isIntegralSpace_quotientSpace S B hS hZ).isDecentSpace)

AlgebraicGeometry.Space.EtaleRelation.isEtaleEquivalenceRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/CoordinateAxesEtaleRelation.lean, line 497. The attribute's comment: “etale_relation”.

The specified relation is an étale equivalence relation on the coordinate axes.

theorem isEtaleEquivalenceRelation (S : CoordinateAxesQuotientSetup.{u}) :
    Stacks.Groupoids.IsEtaleEquivalenceRelation (relationPreRelation S)

AlgebraicGeometry.CoordinateAxesQuotient.coordinateSumMap_invariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FunctionFieldEmbedding.lean, line 315. The attribute's comment: “quotient_map_exists”.

The coordinate-sum map is invariant under the relation: it has the same composite with the source and the target of relationPreRelation.

theorem coordinateSumMap_invariant (S : Setup.{u}) :
    (relationPreRelation S).target ≫ coordinateSumMap S =
      (relationPreRelation S).source ≫ coordinateSumMap S

AlgebraicGeometry.CoordinateAxesQuotient.quotientSumMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FunctionFieldEmbedding.lean, line 364. The attribute's comment: “quotient_map_exists”.

The morphism from the quotient sheaf to the affine line through which the coordinate-sum map factors, together with the equation expressing that factorisation.

noncomputable def quotientSumMap
    [HasSheafify (BigFppfOver.topology B (Spec (.of S.k)) hS) (Type u)] :
    { f : (Stacks.Groupoids.quotientSheaf
          (BigFppfOver.topology B (Spec (.of S.k)) hS)
          (Over.post (X := B.obj hS) B.inclusion)
          (relationPreRelation S)).obj ⟶
        Stacks.Groupoids.points (Over.post (X := B.obj hS) B.inclusion)
          (AffineLineInvolution.affineLine S.k) //
      Stacks.Groupoids.toQuotientSheaf
          (BigFppfOver.topology B (Spec (.of S.k)) hS)
          (Over.post (X := B.obj hS) B.inclusion)
          (relationPreRelation S) ≫ f =
        (Over.post (X := B.obj hS) B.inclusion).op.whiskerLeft
          (yoneda.map (coordinateSumMap S)) }

Sources

• Section 72.6, Tag 0ENI
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.locallyFinite_irreducibleComponents_of_isClosed · AlgebraicGeometry.Space.PrimeDivisor · AlgebraicGeometry.Space.WeilDivisor · AlgebraicGeometry.Space.PrimeDivisor.neighborhoodTotalFractionRingToGeneric_pullback_eq · AlgebraicGeometry.Space.PrimeDivisor.rationalFunctionsToGenericTotalFractionRing · AlgebraicGeometry.Space.PrimeDivisor.injective_rationalFunctionsToGenericTotalFractionRing · AlgebraicGeometry.Space.genericFractionEmbedding · AlgebraicGeometry.Space.PrimeDivisor.isReduced_and_ringKrullDim_eq_one_and_isNoetherianRing_genericHenselianLocalRing

Section72.7 The Weil divisor class associated to an invertible module#

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

Tag 0EPR, a definition

Tag 0EPR in the Stacks Project.

AlgebraicGeometry.Space.PrimeDivisor.pullbacksMeromorphicSections_genericHenselianMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianSpecMorphismFlat.lean, line 152. The attribute's comment: “the clause of the construction preceding the definition: c_ξ is flat, so pullbacks of meromorphic functions and (regular) sections are defined for c_ξ”.

Pullbacks of meromorphic functions and sections are defined for c_ξ : Spec(𝒪^h_{X, ξ}) ⟶ X.

This is the clause of the construction of Section 72.7 of the source preceding Definition 72.7.1: "Since c_ξ is flat, pullbacks of meromorphic functions and (regular) sections are defined for c_ξ". It is what carries a regular meromorphic section s of ℒ to a meromorphic section of ℒ_ξ = c_ξ^*ℒ on Spec(𝒪^h_{X, ξ}), against which the ratio s / s_ξ is taken.

theorem PrimeDivisor.pullbacksMeromorphicSections_genericHenselianMorphism :
    PullbacksMeromorphicSections B S hS
      (Z.genericHenselianMorphism B S hS hX hdec R hR).hom

AlgebraicGeometry.Space.PrimeDivisor.canonicalGenericRatio, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorCanonicalRatio.lean, line 84. The attribute's comment: “the ratio s/s_ξ in Q(O^h_{X, ξ}) of a meromorphic section of an invertible module against the generator at the generic point of a prime divisor, read on the spectrum of the local ring of an affine elementary étale neighbourhood”.

The ratio s / s_ξ of a meromorphic section of an invertible 𝒪_X-module against the generator of ℒ at the generic point of a prime divisor, as an element of Q(𝒪^h_{X, ξ}): the coefficient of the section against the generator over Spec(𝒪_{U, u}), pushed along Q(𝒪_{U, u}) → Q(𝒪^h_{X, ξ}).

def PrimeDivisor.canonicalGenericRatio (t : MeromorphicSection.{u, u} B S hS X hX L) :
    Z.genericTotalFractionRing B S hS hX hdec

AlgebraicGeometry.Space.PrimeDivisor.isUnit_canonicalGenericRatio, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorCanonicalRatio.lean, line 91. The attribute's comment: “the ratio s/s_ξ of a regular meromorphic section is a unit of Q(O^h_{X, ξ})”.

The ratio s / s_ξ of a regular meromorphic section is a unit of Q(𝒪^h_{X, ξ}).

theorem PrimeDivisor.isUnit_canonicalGenericRatio
    (t : MeromorphicSection.{u, u} B S hS X hX L)
    (ht : IsRegularMeromorphicSection.{u, u} B S hS X hX L t) :
    IsUnit (Z.canonicalGenericRatio B S hS hX hdec L hL hInt hN t)

AlgebraicGeometry.Space.PrimeDivisor.canonicalLocalRatio, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorCanonicalRatio.lean, line 103. The attribute's comment: “the generator s_ξ of an invertible module at the generic point of a prime divisor, read as the ratio family it assigns to meromorphic sections”.

The choice of the generator s_ξ: the generator of ℒ at the generic point of a prime divisor, read as the ratio t ↦ t / s_ξ in the units of Q(𝒪^h_{X, ξ}) that it assigns to a meromorphic section of ℒ. On a regular meromorphic section the value is the ratio AlgebraicGeometry.Space.PrimeDivisor.canonicalGenericRatio.

def PrimeDivisor.canonicalLocalRatio : LocalRatio.{u, u} B S hS hX hdec Z L

AlgebraicGeometry.Space.PrimeDivisor.canonicalGenericRatio_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorCanonicalRatio.lean, line 152. The attribute's comment: “the ratio s/s_ξ is multiplied by c when the section is, which is the step by which Stacks 0EPT and Stacks 0EPV compare two sections through one generator”.

If the pullback of t to Spec(𝒪_{U, u}) is c times the pullback of t' there, then the ratio of t is the image of c times the ratio of t'.

theorem PrimeDivisor.canonicalGenericRatio_smul
    (t t' : MeromorphicSection.{u, u} B S hS X hX L)
    (c : (meromorphicFunctionSheaf B S hS (Z.genericStalkSpace B S hS hX hdec).1
      (Z.genericStalkSpace B S hS hX hdec).2).obj.obj
        (op (Z.genericStalkChart B S hS hX hdec)))
    (hc : (pullbackMeromorphicSection B S hS (Z.genericStalkMorphism B S hS hX hdec) L
            (Z.pullbacksMeromorphicSections_genericStalkMorphism B S hS hX hdec) t).eval
          (op (Z.genericStalkChart B S hS hX hdec)) =
      (meromorphicChartRingEquiv B S hS (Z.genericStalkSpace B S hS hX hdec).1
          (Z.genericStalkSpace B S hS hX hdec).2
          (Z.genericStalkChart B S hS hX hdec)).symm c •
        (pullbackMeromorphicSection B S hS (Z.genericStalkMorphism B S hS hX hdec) L
              (Z.pullbacksMeromorphicSections_genericStalkMorphism B S hS hX hdec) t').eval
          (op (Z.genericStalkChart B S hS hX hdec))) :
    Z.canonicalGenericRatio B S hS hX hdec L hL hInt hN t =
      Z.genericStalkMeromorphicToGeneric B S hS hX hdec hInt hN c *
        Z.canonicalGenericRatio B S hS hX hdec L hL hInt hN t'

AlgebraicGeometry.Space.PrimeDivisor.canonicalGenericRatio_smul_of_eval, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorCanonicalRatio.lean, line 217. The attribute's comment: “the ratio s/s_ξ is multiplied by c when the section is, with the scaling read over the chart of X rather than over the spectrum of the local ring -- the step by which Stacks 0EPT and Stacks 0EPV compare two sections through one generator”.

If t is c times t' over the chosen affine elementary étale neighbourhood U of the generic point, for c a meromorphic function on U, then the ratio of t is the image of the pullback of c to Spec(𝒪_{U, u}) times the ratio of t'.

theorem PrimeDivisor.canonicalGenericRatio_smul_of_eval
    (t t' : MeromorphicSection.{u, u} B S hS X hX L)
    (c : (Stacks.SheafOfModules.Tensor.ringSheaf (meromorphicRingedSite B S hS X hX).O).obj.obj
      (op (Z.genericEtaleChart B S hS hX hdec)))
    (hc : t.eval (op (Z.genericEtaleChart B S hS hX hdec)) =
      c • t'.eval (op (Z.genericEtaleChart B S hS hX hdec))) :
    Z.canonicalGenericRatio B S hS hX hdec L hL hInt hN t =
      Z.genericStalkMeromorphicToGeneric B S hS hX hdec hInt hN
          (chartMeromorphicRingedSitePullbackHom B S hS (Z.genericStalkMorphism B S hS hX hdec)
            (Z.pullbacksMeromorphicSections_genericStalkMorphism B S hS hX hdec)
            (Z.genericStalkChartDiagram B S hS hX hdec) c) *
        Z.canonicalGenericRatio B S hS hX hdec L hL hInt hN t'

AlgebraicGeometry.Space.canonicalLocalRatioFamily, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorCanonicalRatio.lean, line 242. The attribute's comment: “the generators s_ξ at every prime divisor, read as the ratio family”.

The family of canonical ratios over all prime divisors of X: the choice of a generator of ℒ at the generic point of every prime divisor.

def canonicalLocalRatioFamily : LocalRatioFamily.{u, u} B S hS hX hdec L

AlgebraicGeometry.Space.PrimeDivisor.orderOfVanishingSection_canonicalLocalRatio_eq_length_sub_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorCanonicalRatio.lean, line 251. The attribute's comment: “the length formula for ord_{Z,ℒ}(s) at the canonical ratio s/s_ξ on a locally Noetherian integral algebraic space”.

If the canonical ratio s / s_ξ of a meromorphic section is a / b with a and b nonzerodivisors of 𝒪^h_{X,ξ}, then ord_{Z,ℒ}(s) is the difference of the lengths of the quotients of 𝒪^h_{X,ξ} by a and by b.

theorem PrimeDivisor.orderOfVanishingSection_canonicalLocalRatio_eq_length_sub_length
    (t : MeromorphicSection.{u, u} B S hS X hX L)
    (a b : nonZeroDivisors ↥(Z.genericHenselianLocalRing B S hS hX hdec))
    (hab : (Z.canonicalLocalRatio B S hS hX hdec L hL hInt hN t :
        Z.genericTotalFractionRing B S hS hX hdec) =
      IsLocalization.mk' (Z.genericTotalFractionRing B S hS hX hdec)
        (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec)) b) :
    haveI : ∀ W : PrimeDivisor B S hS X,
        Nontrivial ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.nontrivial_genericHenselianLocalRing B S hS hX hdec hInt hN
    haveI : ∀ W : PrimeDivisor B S hS X,
        IsNoetherianRing ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.isNoetherianRing_genericHenselianLocalRing B S hS hX hdec hInt hN
    haveI : ∀ W : PrimeDivisor B S hS X,
        Ring.KrullDimLE 1 ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.krullDimLE_genericHenselianLocalRing B S hS hX hdec hInt hN
    orderOfVanishingSection.{u, u} B S hS hX hdec Z L t
        (Z.canonicalLocalRatio B S hS hX hdec L hL hInt hN) =
      ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec)
          (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec))).toNat : ℤ) -
        ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec)
          (b : ↥(Z.genericHenselianLocalRing B S hS hX hdec))).toNat : ℤ)

AlgebraicGeometry.Space.PrimeDivisor.exists_orderOfVanishingSection_canonicalLocalRatio_eq_length_sub_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorCanonicalRatio.lean, line 291. The attribute's comment: “existence of the presentation s/s_ξ = a/b by nonzerodivisors at the canonical ratio, with the length formula, on a locally Noetherian integral algebraic space”.

The canonical ratio s / s_ξ is a fraction a / b of nonzerodivisors of 𝒪^h_{X,ξ}, and for one — hence for every — such presentation ord_{Z,ℒ}(s) is the difference of the lengths of the quotients.

theorem PrimeDivisor.exists_orderOfVanishingSection_canonicalLocalRatio_eq_length_sub_length
    (t : MeromorphicSection.{u, u} B S hS X hX L) :
    haveI : ∀ W : PrimeDivisor B S hS X,
        Nontrivial ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.nontrivial_genericHenselianLocalRing B S hS hX hdec hInt hN
    haveI : ∀ W : PrimeDivisor B S hS X,
        IsNoetherianRing ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.isNoetherianRing_genericHenselianLocalRing B S hS hX hdec hInt hN
    haveI : ∀ W : PrimeDivisor B S hS X,
        Ring.KrullDimLE 1 ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.krullDimLE_genericHenselianLocalRing B S hS hX hdec hInt hN
    ∃ a b : nonZeroDivisors ↥(Z.genericHenselianLocalRing B S hS hX hdec),
      (Z.canonicalLocalRatio B S hS hX hdec L hL hInt hN t :
            Z.genericTotalFractionRing B S hS hX hdec) =
          IsLocalization.mk' (Z.genericTotalFractionRing B S hS hX hdec)
            (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec)) b ∧
        orderOfVanishingSection.{u, u} B S hS hX hdec Z L t
            (Z.canonicalLocalRatio B S hS hX hdec L hL hInt hN) =
          ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec)
              (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec))).toNat : ℤ) -
            ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec)
              (b : ↥(Z.genericHenselianLocalRing B S hS hX hdec))).toNat : ℤ)

AlgebraicGeometry.Space.orderOfVanishingSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 767. The attribute's comment: “ord_{Z,ℒ}(s), in the general form that takes the ratio s/s_ξ as data, so that it is available for an arbitrary module over an arbitrary space. The tag's own definition is at the CONSTRUCTED ratio: PrimeDivisor.canonicalLocalRatio and canonicalLocalRatioFamily of StacksFrontier.AlgebraicGeometry.Spaces.Decent.PrimeDivisorCanonicalRatio build s/s_ξ for an invertible module on a locally Noetherian integral algebraic space and carry no parameter”.

Stacks 0EPR. The order of vanishing of a meromorphic section s of ℒ along Z: the order of vanishing of the ratio s / s_ξ in Q(𝒪^h_{X,ξ}), that is the difference length (𝒪^h_{X,ξ} ⧸ a) - length (𝒪^h_{X,ξ} ⧸ b) for s / s_ξ = a / b with a and b nonzerodivisors.

def orderOfVanishingSection (L : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatio.{u, z} B S hS hX hdec Z L) : ℤ

AlgebraicGeometry.Space.orderOfVanishingSection_eq_length_sub_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 794. The attribute's comment: “the length formula on any presentation, hence independence of the presentation”.

Stacks 0EPR. If the ratio s / s_ξ is a / b with a and b nonzerodivisors of 𝒪^h_{X,ξ}, then ord_{Z,ℒ}(s) is the difference of the lengths of the quotients of 𝒪^h_{X,ξ} by a and by b. In particular it does not depend on the presentation.

theorem orderOfVanishingSection_eq_length_sub_length (L : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatio.{u, z} B S hS hX hdec Z L)
    (a b : nonZeroDivisors ↥(Z.genericHenselianLocalRing B S hS hX hdec))
    (hab : (ratio s : Z.genericTotalFractionRing B S hS hX hdec) =
      IsLocalization.mk' (Z.genericTotalFractionRing B S hS hX hdec)
        (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec)) b) :
    orderOfVanishingSection.{u, z} B S hS hX hdec Z L s ratio =
      ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec)
          (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec))).toNat : ℤ) -
        ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec)
          (b : ↥(Z.genericHenselianLocalRing B S hS hX hdec))).toNat : ℤ)

AlgebraicGeometry.Space.exists_orderOfVanishingSection_eq_length_sub_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 846. The attribute's comment: “existence of the presentation s/s_ξ = a/b by nonzerodivisors, with the length formula; the ratio s/s_ξ is the parameter ratio”.

Stacks 0EPR, well-definedness. The ratio s / s_ξ is a fraction a / b of nonzerodivisors of 𝒪^h_{X,ξ}, and for one — hence, by AlgebraicGeometry.Space.orderOfVanishingSection_eq_length_sub_length, for every — such presentation ord_{Z,ℒ}(s) is the difference length (𝒪^h_{X,ξ} ⧸ a) - length (𝒪^h_{X,ξ} ⧸ b).

This is the clause of the source's definition that fixes the integer: Definition 72.7.1 reads ord_{Z,ℒ}(s) off nonzerodivisors a, b of 𝒪^h_{X,ξ} such that s / s_ξ = a / b, so the existence of such a pair is what makes the difference of lengths an admissible description of ord_{Z,ℒ}(s) at all. Regularity of the meromorphic section — carried, as throughout this module, by ratio s being a unit of Q(𝒪^h_{X,ξ}) — is exactly what produces it: the numerator of an arbitrary presentation of a unit is again a nonzerodivisor.

theorem exists_orderOfVanishingSection_eq_length_sub_length
    (L : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatio.{u, z} B S hS hX hdec Z L) :
    ∃ a b : nonZeroDivisors ↥(Z.genericHenselianLocalRing B S hS hX hdec),
      (ratio s : Z.genericTotalFractionRing B S hS hX hdec) =
          IsLocalization.mk' (Z.genericTotalFractionRing B S hS hX hdec)
            (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec)) b ∧
        orderOfVanishingSection.{u, z} B S hS hX hdec Z L s ratio =
          ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec)
              (a : ↥(Z.genericHenselianLocalRing B S hS hX hdec))).toNat : ℤ) -
            ((Ring.ord ↥(Z.genericHenselianLocalRing B S hS hX hdec)
              (b : ↥(Z.genericHenselianLocalRing B S hS hX hdec))).toNat : ℤ)

AlgebraicGeometry.Space.orderOfVanishingSection_unit_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 889. The attribute's comment: “independence of the choice of the generator s_ξ”.

Stacks 0EPR, well-definedness. Replacing the generator s_ξ of ℒ at the generic point of Z by u · s_ξ for a unit u of 𝒪^h_{X,ξ} replaces the ratio s / s_ξ by u · (s / s_ξ) and does not change ord_{Z,ℒ}(s).

theorem orderOfVanishingSection_unit_smul (L : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio ratio' : LocalRatio.{u, z} B S hS hX hdec Z L)
    {v : ↥(Z.genericHenselianLocalRing B S hS hX hdec)} (hv : IsUnit v)
    (hvr : (ratio' s : Z.genericTotalFractionRing B S hS hX hdec) =
      algebraMap ↥(Z.genericHenselianLocalRing B S hS hX hdec)
        (Z.genericTotalFractionRing B S hS hX hdec) v *
      (ratio s : Z.genericTotalFractionRing B S hS hX hdec)) :
    orderOfVanishingSection.{u, z} B S hS hX hdec Z L s ratio' =
      orderOfVanishingSection.{u, z} B S hS hX hdec Z L s ratio

Tag 0EPS, a lemma

Tag 0EPS in the Stacks Project.

AlgebraicGeometry.Space.exists_localRatioFamily_locallyFinite_divisorCoefficients_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/GenericSectionRatioOrderZero.lean, line 213. The attribute's comment: “the second set: the prime divisors with ord_{Z,ℒ}(s) ≠ 0 are locally finite, at the hypotheses of the source alone -- the proviso hord of locallyFinite_divisorCoefficients_ne_zero_of_isIntegral is supplied here, by the canonical ratio of Stacks 0EPR, rather than assumed; the family of ratios is quantified existentially, over the choice of a free generator of ℒ_ξ at each prime divisor and of the isomorphism across the universe gap that step (iii) of that construction is existential in, and its value at s is pinned to the ratio of s against that generator by the first clause of the conclusion”.

Stacks 0EPS, the second set, with hord supplied rather than assumed. Let S be a scheme, let X be a locally Noetherian integral algebraic space over S, let ℒ be an invertible 𝒪_X-module and let s be a regular meromorphic section of ℒ. Then there is a family of local ratios whose value at s is, at each prime divisor, the ratio of s against a free generator t_ξ of ℒ_ξ — the canonical ratio s / s_ξ of Stacks 0EPR, which is the first clause of the conclusion — for which ord_{Z, ℒ}(s) = 0 at every prime divisor where s generates ℒ_ξ, and for which the prime divisors with ord_{Z, ℒ}(s) ≠ 0 are locally finite in |X|.

This carries no hypothesis beyond the source's. It is AlgebraicGeometry.Space.locallyFinite_divisorCoefficients_ne_zero_of_isIntegral, whose single proviso hord is here a conclusion rather than an assumption, and it is existential over the choices the source also makes. The first clause is load-bearing: without it fun _ ↦ 1 would satisfy the other two vacuously. See the implementation notes of this module for what the existential quantifier ranges over and why the family is canonical at s and not at every section.

theorem exists_localRatioFamily_locallyFinite_divisorCoefficients_ne_zero
    (L : Modules.{u, u} B S hS X hX)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible
      (structureCommRings B S hS (⟨X, hX⟩ : AlgebraicSpaces B S hS))
      (structureRingSheaf B S hS (⟨X, hX⟩ : AlgebraicSpaces B S hS)).property L)
    (s : MeromorphicSection.{u, u} B S hS X hX L)
    (hreg : IsRegularMeromorphicSection.{u, u} B S hS X hX L s) :
    ∃ ratio : LocalRatioFamily.{u, u} B S hS hX hdec L,
      (∀ Z : PrimeDivisor B S hS X,
          ∃ (t : Z.genericModuleStalk B S hS hX hdec (RR Z) (hRR Z) L)
            (ψ : meromorphicChartRing B S hS
                (Z.genericHenselianSpace B S hS hX hdec (RR Z) (hRR Z)).obj
                (Z.genericHenselianSpace B S hS hX hdec (RR Z) (hRR Z)).property
                (Z.genericHenselianChart B S hS hX hdec (RR Z) (hRR Z)) ≃+*
              Z.genericTotalFractionRing B S hS hX hdec),
            (Function.Bijective fun r : RR Z ↦ r • t) ∧
              ψ.symm (ratio Z s : Z.genericTotalFractionRing B S hS hX hdec) •
                  toMeromorphicSectionValue B S hS
                    (Z.genericHenselianSpace B S hS hX hdec (RR Z) (hRR Z)).obj
                    (Z.genericHenselianSpace B S hS hX hdec (RR Z) (hRR Z)).property
                    (Z.genericHenselianPullback B S hS hX hdec (RR Z) (hRR Z) L)
                    (Z.genericHenselianChart B S hS hX hdec (RR Z) (hRR Z)) t =
                Z.genericMeromorphicGerm B S hS hX hdec (RR Z) (hRR Z) L s) ∧
        (∀ Z : PrimeDivisor B S hS X,
            Z.GeneratesGenericModuleStalk B S hS hX hdec (RR Z) (hRR Z) L s →
              divisorCoefficients.{u, u} B S hS hX hdec L s ratio Z = 0) ∧
          LocallyFinite fun Z : PrimeDivisor B S hS X ↦
            if divisorCoefficients.{u, u} B S hS hX hdec L s ratio Z = 0 then ∅
            else Z.support B S hS X

AlgebraicGeometry.Space.locallyFinite_primeDivisor_not_memGenericModuleStalk_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocallyFiniteFirstSetOfRegularSection.lean, line 94. The attribute's comment: “the first set: the prime divisors whose generic point ξ has s ∉ ℒ_ξ are locally finite -- unconditionally, at the hypotheses of the source, the nonempty open subspace of the source's first sentence being produced rather than assumed”.

Stacks 0EPS, the first set. Let S be a scheme, let X be a locally Noetherian integral algebraic space over S, let ℒ be an invertible 𝒪_X-module and let s be a regular meromorphic section of ℒ. Then the prime divisors Z of X whose generic point ξ satisfies s ∉ ℒ_ξ are locally finite in |X|.

theorem locallyFinite_primeDivisor_not_memGenericModuleStalk_of_isIntegral
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsLocallyNoetherian Y))
    (hint : IsIntegralSpace B S hS X) (L : Modules.{u, u} B S hS X hX)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible
      (structureCommRings B S hS (⟨X, hX⟩ : AlgebraicSpaces B S hS))
      (structureRingSheaf B S hS (⟨X, hX⟩ : AlgebraicSpaces B S hS)).property L)
    (s : MeromorphicSection.{u, u} B S hS X hX L)
    (hreg : IsRegularMeromorphicSection.{u, u} B S hS X hX L s)
    [DecidablePred fun Z : PrimeDivisor B S hS X ↦
      ¬ Z.MemGenericModuleStalk B S hS hX hdec (RR Z) (hRR Z) L s] :
    LocallyFinite fun Z : PrimeDivisor B S hS X ↦
      if ¬ Z.MemGenericModuleStalk B S hS hX hdec (RR Z) (hRR Z) L s then
        Z.support B S hS X
      else ∅

AlgebraicGeometry.Space.locallyFinite_primeDivisor_not_generatesGenericModuleStalk_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocallyFiniteSecondSetOfRegularSection.lean, line 102. The attribute's comment: “the generating set: the prime divisors whose generic point ξ has s not generating ℒ_ξ are locally finite -- unconditionally, at the hypotheses of the source, the nonempty open subspace of the source's first sentence being produced rather than assumed; the second set of the source is contained in this one”.

Stacks 0EPS, the generating set. Let S be a scheme, let X be a locally Noetherian integral algebraic space over S, let ℒ be an invertible 𝒪_X-module and let s be a regular meromorphic section of ℒ. Then the prime divisors Z of X whose generic point ξ is such that s does not generate ℒ_ξ are locally finite in |X|.

theorem locallyFinite_primeDivisor_not_generatesGenericModuleStalk_of_isIntegral
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsLocallyNoetherian Y))
    (hint : IsIntegralSpace B S hS X) (L : Modules.{u, u} B S hS X hX)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible
      (structureCommRings B S hS (⟨X, hX⟩ : AlgebraicSpaces B S hS))
      (structureRingSheaf B S hS (⟨X, hX⟩ : AlgebraicSpaces B S hS)).property L)
    (s : MeromorphicSection.{u, u} B S hS X hX L)
    (hreg : IsRegularMeromorphicSection.{u, u} B S hS X hX L s)
    [DecidablePred fun Z : PrimeDivisor B S hS X ↦
      ¬ Z.GeneratesGenericModuleStalk B S hS hX hdec (RR Z) (hRR Z) L s] :
    LocallyFinite fun Z : PrimeDivisor B S hS X ↦
      if ¬ Z.GeneratesGenericModuleStalk B S hS hX hdec (RR Z) (hRR Z) L s then
        Z.support B S hS X
      else ∅

AlgebraicGeometry.Space.locallyFinite_divisorCoefficients_ne_zero_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocallyFiniteSecondSetOfRegularSection.lean, line 168. The attribute's comment: “the second set: the prime divisors with ord_{Z,ℒ}(s) ≠ 0 are locally finite, at the hypotheses of the source together with hord, the vanishing of ord_{Z,ℒ}(s) where s generates ℒ_ξ -- which the ratio parameter of orderOfVanishingSection does not supply by itself”.

Stacks 0EPS, the second set. Let S be a scheme, let X be a locally Noetherian integral algebraic space over S, let ℒ be an invertible 𝒪_X-module and let s be a regular meromorphic section of ℒ. Then the prime divisors Z with ord_{Z, ℒ}(s) ≠ 0 are locally finite in |X|, provided ord_{Z, ℒ}(s) = 0 wherever s generates ℒ_ξ.

That proviso, hord, is the only hypothesis beyond the source's.

theorem locallyFinite_divisorCoefficients_ne_zero_of_isIntegral
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsLocallyNoetherian Y))
    (hint : IsIntegralSpace B S hS X) (L : Modules.{u, u} B S hS X hX)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible
      (structureCommRings B S hS (⟨X, hX⟩ : AlgebraicSpaces B S hS))
      (structureRingSheaf B S hS (⟨X, hX⟩ : AlgebraicSpaces B S hS)).property L)
    (s : MeromorphicSection.{u, u} B S hS X hX L)
    (hreg : IsRegularMeromorphicSection.{u, u} B S hS X hX L s)
    (ratio : LocalRatioFamily.{u, u} B S hS hX hdec L)
    (hord : ∀ Z : PrimeDivisor B S hS X,
      Z.GeneratesGenericModuleStalk B S hS hX hdec (RR Z) (hRR Z) L s →
        divisorCoefficients.{u, u} B S hS hX hdec L s ratio Z = 0) :
    LocallyFinite fun Z : PrimeDivisor B S hS X ↦
      if divisorCoefficients.{u, u} B S hS hX hdec L s ratio Z = 0 then ∅
      else Z.support B S hS X

AlgebraicGeometry.Space.locallyFinite_primeDivisor_of_genericPoint_notMem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 683. The attribute's comment: “both sets: prime divisors whose generic points avoid a nonempty open”.

The Stacks 0EE5 step in the proof of Stacks 0EPS. Any collection of prime divisors of a locally Noetherian integral algebraic space whose generic points all avoid one nonempty open subset of |X| is locally finite in |X|.

Such a prime divisor is an irreducible component of |X| ∖ U, because a strictly larger irreducible closed subset of |X| ∖ U would make its codimension at least two, and the irreducible components of a closed subset are locally finite by Stacks 0EE5.

This is the second and third sentences of the proof of Stacks 0EPS, in the generality that covers both of that lemma's sets at once, and it is the same step the proofs of Stacks 0ENN and Stacks 0EQU take. It does not on its own prove Stacks 0EPS: the nonempty open subset U is a hypothesis here, while Stacks 0EPS asserts local finiteness from regularity of the meromorphic section alone — its proof's first sentence, that s generates ℒ over some nonempty open subspace, is what produces U, and the attribute note below records that this statement carries it. Discharging U is the open part of Stacks 0EPS; the implementation notes of this module say exactly what is missing for each of the lemma's two sets.

theorem locallyFinite_primeDivisor_of_genericPoint_notMem
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsLocallyNoetherian Y))
    (hirr : IrreducibleSpace (points B S hS X)) (P : PrimeDivisor B S hS X → Prop)
    [DecidablePred P]
    (U : Set (points B S hS X)) (hUopen : IsOpen U) (hUne : U.Nonempty)
    (hP : ∀ Z : PrimeDivisor B S hS X, P Z → Z.genericPoint B S hS X ∈ Uᶜ) :
    LocallyFinite fun Z : PrimeDivisor B S hS X ↦ if P Z then Z.support B S hS X else ∅

AlgebraicGeometry.Space.locallyFinite_divisorCoefficients_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 1009. The attribute's comment: “the second set: the prime divisors with ord_{Z,ℒ}(s) ≠ 0 are locally finite”.

The Stacks 0EE5 step in the proof of Stacks 0EPS, for its second set. The prime divisors at which ord_{Z,ℒ}(s) is nonzero are locally finite in |X|, given a nonempty open subset of |X| containing the generic point of no such prime divisor — which in the source is the open subspace over which the regular meromorphic section s generates ℒ.

This is AlgebraicGeometry.Space.locallyFinite_primeDivisor_of_genericPoint_notMem specialized to the predicate ord_{Z,ℒ}(s) ≠ 0. Like it, it carries the hypothesis hgen that Stacks 0EPS proves rather than assumes, which the attribute note records. For this set hgen cannot even be dropped: the order of vanishing is taken against the arbitrary parameter ratio, so the set of prime divisors with nonzero coefficient is not determined by ℒ and s, and without hgen the statement is false. See the implementation notes of this module.

theorem locallyFinite_divisorCoefficients_ne_zero
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsLocallyNoetherian Y))
    (hirr : IrreducibleSpace (points B S hS X)) (L : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatioFamily.{u, z} B S hS hX hdec L)
    (U : Set (points B S hS X)) (hUopen : IsOpen U) (hUne : U.Nonempty)
    (hgen : ∀ W : PrimeDivisor B S hS X,
      divisorCoefficients.{u, z} B S hS hX hdec L s ratio W ≠ 0 →
        W.genericPoint B S hS X ∈ Uᶜ) :
    LocallyFinite fun W : PrimeDivisor B S hS X ↦
      if divisorCoefficients.{u, z} B S hS hX hdec L s ratio W = 0 then ∅
      else W.support B S hS X

Tag 0EPT, a lemma

Tag 0EPT in the Stacks Project.

AlgebraicGeometry.Space.exists_divisorCoefficients_canonicalLocalRatioFamily_sub_eq_ord_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorMeromorphicSectionIso.lean, line 193. The attribute's comment: “the second conclusion for two ISOMORPHIC invertible modules: the Weil divisors of the chosen regular meromorphic sections of ℒ and of 𝒩 differ coefficientwise by div(f) for an invertible rational function f, at the canonical ratio s/s_ξ of Stacks 0EPR and the embedding of Stacks 0ENK, with nothing assumed beyond X decent, locally Noetherian and integral”.

Stacks 0EPT in the form the construction of Stacks 0EPW uses, at the canonical choices. On a decent, locally Noetherian, integral algebraic space the Weil divisors of the chosen regular meromorphic sections of two isomorphic invertible 𝒪_X-modules differ coefficientwise by the divisor of an invertible rational function on X, the order of vanishing being read at the canonical ratio s / s_ξ of Stacks 0EPR and the embedding R(X) → Q(𝒪^h_{X, ξ}) of Stacks 0ENK.

The chosen section of 𝒩 is carried by the isomorphism 𝒦_X(𝒩) ≅ 𝒦_X(ℒ) to a regular meromorphic section of ℒ with the same orders of vanishing (AlgebraicGeometry.Space.PrimeDivisor.orderOfVanishingSection_canonicalLocalRatio_sectionsMap), and two regular meromorphic sections of the one module ℒ differ by an invertible rational function, which is Stacks 0EPT in the form AlgebraicGeometry.Space.exists_units_orderOfVanishingSection_canonicalLocalRatio_eq_add_ord.

theorem exists_divisorCoefficients_canonicalLocalRatioFamily_sub_eq_ord_of_iso (e : L ≅ N) :
    haveI : ∀ W : PrimeDivisor B S hS X,
        Nontrivial ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.nontrivial_genericHenselianLocalRing B S hS hX hdec hInt hNoeth
    haveI : ∀ W : PrimeDivisor B S hS X,
        IsNoetherianRing ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.isNoetherianRing_genericHenselianLocalRing B S hS hX hdec hInt hNoeth
    haveI : ∀ W : PrimeDivisor B S hS X,
        Ring.KrullDimLE 1 ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.krullDimLE_genericHenselianLocalRing B S hS hX hdec hInt hNoeth
    ∃ f : (rationalFunctions B S hS hX)ˣ, ∀ W : PrimeDivisor B S hS X,
      divisorCoefficients.{u, u} B S hS hX hdec L
            (regularMeromorphicSection B S hS hX hInt hNoeth L hL)
            (canonicalLocalRatioFamily B S hS hX hdec L hL hInt hNoeth) W -
          divisorCoefficients.{u, u} B S hS hX hdec N
            (regularMeromorphicSection B S hS hX hInt hNoeth N hNinv)
            (canonicalLocalRatioFamily B S hS hX hdec N hNinv hInt hNoeth) W =
        (genericFractionEmbedding B S hS hX hdec hInt hNoeth).ord f W

AlgebraicGeometry.Space.exists_units_rationalFunctions_canonicalLocalRatio_eq_emb_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorMeromorphicSectionRatio.lean, line 63. The attribute's comment: “the first conclusion, that the ratio s/s' of two regular meromorphic sections of an invertible module is an element of R(X)^*, read on the canonical ratios s/s_ξ of Stacks 0EPR through the embedding R(X) → Q(O^h_{X, ξ}) of Stacks 0ENK”.

The ratio of two regular meromorphic sections is an invertible rational function. On a decent, locally Noetherian, integral algebraic space the ratio of two regular meromorphic sections s, s' of an invertible 𝒪_X-module is an invertible rational function f: at the generic point of every prime divisor the canonical ratio s / s_ξ of Stacks 0EPR is the image of f under the embedding R(X) → Q(𝒪^h_{X, ξ}) of Stacks 0ENK times the canonical ratio s' / s_ξ.

theorem exists_units_rationalFunctions_canonicalLocalRatio_eq_emb_mul
    (L : Modules.{u, u} B S hS X hX) (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L)
    (s s' : MeromorphicSection.{u, u} B S hS X hX L)
    (hs : IsRegularMeromorphicSection.{u, u} B S hS X hX L s)
    (hs' : IsRegularMeromorphicSection.{u, u} B S hS X hX L s') :
    ∃ f : (rationalFunctions B S hS hX)ˣ, ∀ W : PrimeDivisor B S hS X,
      (canonicalLocalRatioFamily B S hS hX hdec L hL hInt hN W s :
          W.genericTotalFractionRing B S hS hX hdec) =
        (genericFractionEmbedding B S hS hX hdec hInt hN).emb W
            (f : rationalFunctions B S hS hX) *
          (canonicalLocalRatioFamily B S hS hX hdec L hL hInt hN W s' :
            W.genericTotalFractionRing B S hS hX hdec)

AlgebraicGeometry.Space.exists_units_orderOfVanishingSection_canonicalLocalRatio_eq_add_ord, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorMeromorphicSectionRatio.lean, line 95. The attribute's comment: “the second conclusion, div_ℒ(s) = div_ℒ(s') + div(f) coefficientwise, at the canonical ratio s/s_ξ of Stacks 0EPR and the embedding of Stacks 0ENK, with f = s/s' PRODUCED rather than assumed”.

The orders of vanishing of two regular meromorphic sections differ by ord_Z of their ratio. On a decent, locally Noetherian, integral algebraic space the orders of vanishing of two regular meromorphic sections s, s' of an invertible 𝒪_X-module along a prime divisor differ by ord_Z(f) for one invertible rational function f, namely their ratio. Summed over the prime divisors this is the identity div_ℒ(s) = div_ℒ(s') + div(f) of Weil divisors.

theorem exists_units_orderOfVanishingSection_canonicalLocalRatio_eq_add_ord
    (L : Modules.{u, u} B S hS X hX) (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L)
    (s s' : MeromorphicSection.{u, u} B S hS X hX L)
    (hs : IsRegularMeromorphicSection.{u, u} B S hS X hX L s)
    (hs' : IsRegularMeromorphicSection.{u, u} B S hS X hX L s') :
    haveI : ∀ W : PrimeDivisor B S hS X,
        Nontrivial ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.nontrivial_genericHenselianLocalRing B S hS hX hdec hInt hN
    haveI : ∀ W : PrimeDivisor B S hS X,
        IsNoetherianRing ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.isNoetherianRing_genericHenselianLocalRing B S hS hX hdec hInt hN
    haveI : ∀ W : PrimeDivisor B S hS X,
        Ring.KrullDimLE 1 ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.krullDimLE_genericHenselianLocalRing B S hS hX hdec hInt hN
    ∃ f : (rationalFunctions B S hS hX)ˣ, ∀ W : PrimeDivisor B S hS X,
      orderOfVanishingSection.{u, u} B S hS hX hdec W L s
          (canonicalLocalRatioFamily B S hS hX hdec L hL hInt hN W) =
        orderOfVanishingSection.{u, u} B S hS hX hdec W L s'
            (canonicalLocalRatioFamily B S hS hX hdec L hL hInt hN W) +
          (genericFractionEmbedding B S hS hX hdec hInt hN).ord f W

AlgebraicGeometry.Space.orderOfVanishingSection_eq_add_ord, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 919. The attribute's comment: “div_ℒ(s) = div_ℒ(s') + div(f) coefficientwise; f = s/s' is the argument hs, discharged at the canonical ratio of Stacks 0EPR by exists_units_orderOfVanishingSection_canonicalLocalRatio_eq_add_ord, which produces f”.

Stacks 0EPT, coefficientwise. If s and s' are meromorphic sections of ℒ whose ratios at the generic point of Z differ by the image of a rational function f, then ord_{Z,ℒ}(s) = ord_{Z,ℒ}(s') + ord_Z(f). Summing over all prime divisors this is the identity div_ℒ(s) = div_ℒ(s') + div(f) of Weil divisors.

That such an f exists — the first assertion of Stacks 0EPT — is the argument hs here, and is proved at the canonical ratio of Stacks 0EPR by AlgebraicGeometry.Space.exists_units_orderOfVanishingSection_canonicalLocalRatio_eq_add_ord, which produces f rather than taking it.

theorem orderOfVanishingSection_eq_add_ord (L : Modules.{u, max u z} B S hS X hX)
    (s s' : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatio.{u, z} B S hS hX hdec Z L)
    (emb : rationalFunctions B S hS hX →+* Z.genericTotalFractionRing B S hS hX hdec)
    (f : rationalFunctions B S hS hX) (hf : IsUnit (emb f))
    (hs : (ratio s : Z.genericTotalFractionRing B S hS hX hdec) =
      emb f * (ratio s' : Z.genericTotalFractionRing B S hS hX hdec)) :
    orderOfVanishingSection.{u, z} B S hS hX hdec Z L s ratio =
      orderOfVanishingSection.{u, z} B S hS hX hdec Z L s' ratio +
        Z.ord B S hS hX hdec (emb f) hf

AlgebraicGeometry.Space.divisorOfSection_eq_add_principalDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSectionRatio.lean, line 152. The attribute's comment: “the identity in Div(X); the coefficientwise form is orderOfVanishingSection_eq_add_ord”.

Stacks 0EPT. If s and s' are nonzero meromorphic sections of ℒ whose ratios at the generic point of every prime divisor differ by the invertible rational function f = s/s' ∈ R(X)^*, then their Weil divisors of Stacks 0EPU differ by the principal Weil divisor of f:

∑ ord_{Z,ℒ}(s) [Z] = ∑ ord_{Z,ℒ}(s') [Z] + div(f)

as an identity in the group Div(X) of Weil divisors on X. Coefficientwise at a single prime divisor this is AlgebraicGeometry.Space.orderOfVanishingSection_eq_add_ord, of which this statement is the sum over all prime divisors; that div(f) is itself a Weil divisor is what Stacks 0EPS gives in the source, and is here the hypothesis hlf, which AlgebraicGeometry.Space.ord_mem_weilDivisor_of_ratio_eq discharges from the local finiteness of the two divisors.

theorem divisorOfSection_eq_add_principalDivisor
    (hlf : ∀ g : (rationalFunctions B S hS hX)ˣ, E.ord g ∈ WeilDivisor B S hS X)
    (L : Modules.{u, max u z} B S hS X hX)
    (s s' : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatioFamily.{u, z} B S hS hX hdec L)
    (f : (rationalFunctions B S hS hX)ˣ)
    (hfin : LocallyFinite fun W : PrimeDivisor B S hS X ↦
      if divisorCoefficients.{u, z} B S hS hX hdec L s ratio W = 0 then ∅
      else W.support B S hS X)
    (hfin' : LocallyFinite fun W : PrimeDivisor B S hS X ↦
      if divisorCoefficients.{u, z} B S hS hX hdec L s' ratio W = 0 then ∅
      else W.support B S hS X)
    (hs : ∀ W : PrimeDivisor B S hS X,
      (ratio W s : W.genericTotalFractionRing B S hS hX hdec) =
        E.emb W (f : rationalFunctions B S hS hX) *
          (ratio W s' : W.genericTotalFractionRing B S hS hX hdec)) :
    divisorOfSection.{u, z} B S hS hX hdec L s ratio hfin =
      divisorOfSection.{u, z} B S hS hX hdec L s' ratio hfin' + E.principalDivisor hlf f

AlgebraicGeometry.Space.existsUnique_ratio_weilDivisorOfSection_eq_add_divRationalFunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvertibleModuleWeilDivisorClass.lean, line 208. The attribute's comment: “both conclusions at the source's hypotheses: for nonzero meromorphic sections s, s' of an invertible module on a locally Noetherian integral X, f = s/s' is THE element of R(X)^* with s = f s' (f read in Γ(X, 𝒦_X) through the canonical comparison of Stacks 0ENA, for every presentation), and div_ℒ(s) = div_ℒ(s') + div(f) in Div(X), the sums being Weil divisors by Stacks 0EPS (proved) and div(f) the principal divisor of Stacks 0ENQ”.

Stacks 0EPT. Let X be a locally Noetherian integral algebraic space over S, let ℒ be an invertible 𝒪_X-module and let s, s' be nonzero meromorphic sections of ℒ. Then f = s / s' is an element of R(X)^* and

∑ ord_{Z,ℒ}(s) [Z] = ∑ ord_{Z,ℒ}(s') [Z] + div(f)

as Weil divisors.

The ratio is stated as the source means it: f is the unit of R(X) with s = f · s', f being read in Γ(X, 𝒦_X) through the canonical comparison R(X) → Γ(X, 𝒦_X) of Stacks 0ENA (AlgebraicGeometry.Space.rationalToMeromorphic), for every presentation the comparison is built from — it does not depend on it, AlgebraicGeometry.Space.rationalToMeromorphic_eq_of_presentation — and f is unique with this property. The two sums are AlgebraicGeometry.Space.weilDivisorOfSection (Stacks 0EPU, part (1)), which are Weil divisors by Stacks 0EPS, proved there; div(f) is the principal Weil divisor AlgebraicGeometry.Space.divRationalFunction of Stacks 0ENQ, a Weil divisor by Stacks 0ENN. Nothing is assumed beyond the hypotheses of the source.

The ratio in Γ(X, 𝒦_X)^* is AlgebraicGeometry.Space.existsUnique_units_smul_eq_of_isRegularMeromorphicSection (nonzero sections being regular, AlgebraicGeometry.Space.isRegularMeromorphicSection_of_ne_zero); it comes from a unit of R(X) because the comparison is bijective; and at the generic point of every prime divisor the canonical ratio s / s_ξ of Stacks 0EPR is the image of f times s' / s_ξ, so that the orders of vanishing add up (AlgebraicGeometry.Space.orderOfVanishingSection_eq_add_ord_of_ratio_eq).

theorem existsUnique_ratio_weilDivisorOfSection_eq_add_divRationalFunction
    (L : Modules.{u, u} B S hS X hX) (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L)
    (s s' : MeromorphicSection.{u, u} B S hS X hX L) (hs : s ≠ 0) (hs' : s' ≠ 0) :
    ∃! f : (rationalFunctions B S hS hX)ˣ,
      (∀ P : CodimensionZeroPresentation B S hS X,
        s = (id (rationalToMeromorphic (X := (⟨X, hX⟩ : AlgebraicSpaces B S hS)) P
              (fun _ hz => (weaklyAssociatedPointsOfSpace_eq_setOf_localRingDimension_eq_zero
                B S hS ⟨X, hX⟩ hInt.hasEtaleLocalProperty_isReduced).subset hz)
              (hasLocallyFiniteIrreducibleComponents_of_isLocallyNoetherian B S hS X hX hN)
              (f : rationalFunctions B S hS hX)) :
            ↥(RingCat.sectionsSubring ((Stacks.SheafOfModules.Tensor.ringSheaf
              (meromorphicRingedSite B S hS X hX).O).obj))) • s') ∧
      weilDivisorOfSection B S hS hX hInt hN L hL s hs =
        weilDivisorOfSection B S hS hX hInt hN L hL s' hs' +
          divRationalFunction B S hS hX hInt hN f

AlgebraicGeometry.Space.existsUnique_units_smul_eq_of_isRegularMeromorphicSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicSectionRatio.lean, line 146. The attribute's comment: “the first conclusion, that the ratio s/s' of two regular meromorphic sections of an invertible module is invertible, read in Γ(X, 𝒦_X) -- which is R(X) by the third conclusion of Stacks 0ENA; the ratio is also unique”.

Stacks 0EPT, the first conclusion; the algebraic-space analogue of Stacks 02SH. On a locally Noetherian integral algebraic space over a scheme S, two regular meromorphic sections s, s' of an invertible 𝒪_X-module differ by a unique invertible global meromorphic function: s = g · s' with g ∈ Γ(X, 𝒦_X)^*. Since R(X) = Γ(X, 𝒦_X) by the third conclusion of Stacks 0ENA, this says that the ratio s / s' lies in R(X)^*.

The trivialisation 𝒦_X ≅ 𝒦_X(ℒ) of Stacks 0EPQ writes both sections as multiples of one section t, the coefficients being global meromorphic functions; they are nonzero by regularity, hence invertible because Γ(X, 𝒦_X) is the function field; and uniqueness is injectivity of multiplication by the regular section s'.

theorem existsUnique_units_smul_eq_of_isRegularMeromorphicSection
    (L : Modules.{u, u} B S hS X hX) (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L)
    (s s' : MeromorphicSection.{u, u} B S hS X hX L)
    (hs : IsRegularMeromorphicSection.{u, u} B S hS X hX L s)
    (hs' : IsRegularMeromorphicSection.{u, u} B S hS X hX L s') :
    ∃! g : (↥(RingCat.sectionsSubring
        ((Stacks.SheafOfModules.Tensor.ringSheaf (meromorphicRingedSite B S hS X hX).O).obj)))ˣ,
      s = (g : ↥(RingCat.sectionsSubring
        ((Stacks.SheafOfModules.Tensor.ringSheaf (meromorphicRingedSite B S hS X hX).O).obj))) •
        s'

Tag 0EPU, a definition

Tag 0EPU in the Stacks Project.

AlgebraicGeometry.Space.divisorCoefficients, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 966. The attribute's comment: “part (1): the coefficients ord_{Z,ℒ}(s) of div_ℒ(s)”.

Stacks 0EPU, part (1). The coefficients of the Weil divisor associated to a meromorphic section s of ℒ: the coefficient at a prime divisor Z is ord_{Z,ℒ}(s).

def divisorCoefficients (L : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatioFamily.{u, z} B S hS hX hdec L) : PrimeDivisor B S hS X → ℤ

AlgebraicGeometry.Space.divisorOfSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 975. The attribute's comment: “part (1): div_ℒ(s) = ∑ ord_{Z,ℒ}(s) [Z] as an element of Div(X)”.

Stacks 0EPU, part (1). The Weil divisor associated to a meromorphic section s of ℒ, that is div_ℒ(s) = ∑ ord_{Z,ℒ}(s) [Z] in Div(X). The prime divisors with nonzero coefficient are locally finite by Stacks 0EPS, which is the hypothesis hfin.

def divisorOfSection (L : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatioFamily.{u, z} B S hS hX hdec L)
    (hfin : LocallyFinite fun W : PrimeDivisor B S hS X ↦
      if divisorCoefficients.{u, z} B S hS hX hdec L s ratio W = 0 then ∅
      else W.support B S hS X) :
    WeilDivisor B S hS X

AlgebraicGeometry.Space.divisorOfSectionOfGenerating, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 1038. The attribute's comment: “part (1): div_ℒ(s) in Div(X); the local finiteness that Stacks 0EPS supplies in the source comes from the hypothesis quadruple (U, hUopen, hUne, hgen), the open subspace over which s generates ℒ not being produced in this library”.

Stacks 0EPU, part (1). The Weil divisor div_ℒ(s) = ∑ ord_{Z,ℒ}(s) [Z] of a meromorphic section s of ℒ, with the local finiteness of its support supplied by AlgebraicGeometry.Space.locallyFinite_divisorCoefficients_ne_zero from a nonempty open subset of |X| whose complement carries the generic point of every prime divisor with nonzero coefficient — in the source, the open subspace over which s generates ℒ. That open subset is a hypothesis: the first sentence of the proof of Stacks 0EPS, which produces it there, is not established in this library, for the reasons given in the implementation notes of this module.

def divisorOfSectionOfGenerating
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsLocallyNoetherian Y))
    (hirr : IrreducibleSpace (points B S hS X)) (L : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatioFamily.{u, z} B S hS hX hdec L)
    (U : Set (points B S hS X)) (hUopen : IsOpen U) (hUne : U.Nonempty)
    (hgen : ∀ W : PrimeDivisor B S hS X,
      divisorCoefficients.{u, z} B S hS hX hdec L s ratio W ≠ 0 →
        W.genericPoint B S hS X ∈ Uᶜ) :
    WeilDivisor B S hS X

AlgebraicGeometry.Space.weilDivisorOfSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvertibleModuleWeilDivisor.lean, line 245. The attribute's comment: “part (1): div_ℒ(s) = ∑ ord_{Z,ℒ}(s)[Z] ∈ Div(X) for a nonzero meromorphic section s of an invertible module, at the canonical ratio s/s_ξ of Stacks 0EPR, with the local finiteness of Stacks 0EPS proved”.

Stacks 0EPU, part (1). The Weil divisor associated to a nonzero meromorphic section s of an invertible 𝒪_X-module ℒ on a locally Noetherian integral algebraic space:

div_ℒ(s) = ∑_Z ord_{Z,ℒ}(s) [Z] ∈ Div(X),

the sum over the prime divisors of X. The coefficient ord_{Z,ℒ}(s) is the order of vanishing of Stacks 0EPR at the canonical ratio s / s_ξ (AlgebraicGeometry.Space.canonicalLocalRatioFamily), and the sum is a Weil divisor by Stacks 0EPS, which is AlgebraicGeometry.Space.locallyFinite_ord_ne_zero_of_ne_zero. Nothing beyond X, ℒ and s enters.

def weilDivisorOfSection
    (L : Modules.{u, u} B S hS X hX) (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L)
    (s : MeromorphicSection.{u, u} B S hS X hX L) (hs : s ≠ 0) : ↥(WeilDivisor B S hS X)

AlgebraicGeometry.Space.weilDivisorClassOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvertibleModuleWeilDivisorClass.lean, line 129. The attribute's comment: “part (2): the Weil divisor class of ℒ, the image of div_ℒ(s) in the canonical Cl(X) of Stacks 0ENR for a nonzero meromorphic section s, which exists; independence of s is weilDivisorClassOfInvertible_eq”.

Stacks 0EPU, part (2). The Weil divisor class associated to an invertible 𝒪_X-module ℒ on a locally Noetherian integral algebraic space: the image of div_ℒ(s) in the Weil divisor class group Cl(X) of Stacks 0ENR, for s a nonzero meromorphic section of ℒ.

It is evaluated at the nonzero meromorphic section of AlgebraicGeometry.Space.exists_meromorphicSection_ne_zero, and it is the image of div_ℒ(s) for every nonzero s by AlgebraicGeometry.Space.weilDivisorClassOfInvertible_eq.

def weilDivisorClassOfInvertible
    (L : Modules.{u, u} B S hS X hX) (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L) :
    weilDivisorClassGroup B S hS hX hInt hN

AlgebraicGeometry.Space.weilDivisorClassOfInvertible_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvertibleModuleWeilDivisorClass.lean, line 141. The attribute's comment: “part (2): well-definedness, the class of div_ℒ(s) in Cl(X) is the same for every nonzero meromorphic section s, by Stacks 0EPT”.

Stacks 0EPU, part (2), well-definedness. The Weil divisor class of ℒ is the image of div_ℒ(s) in Cl(X) for every nonzero meromorphic section s of ℒ: two nonzero meromorphic sections have Weil divisors differing by the principal divisor div(s / s'), by Stacks 0EPT.

theorem weilDivisorClassOfInvertible_eq
    (L : Modules.{u, u} B S hS X hX) (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L)
    (s : MeromorphicSection.{u, u} B S hS X hX L) (hs : s ≠ 0) :
    weilDivisorClassOfInvertible B S hS hX hInt hN L hL =
      (QuotientAddGroup.mk (weilDivisorOfSection B S hS hX hInt hN L hL s hs) :
        weilDivisorClassGroup B S hS hX hInt hN)

AlgebraicGeometry.Space.divisorClassOfSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeilDivisorClassOfSection.lean, line 120. The attribute's comment: “part (2): the Weil divisor class of ℒ, the image of div_ℒ(s) in Cl(X); the class group is Stacks 0ENR, relative to the embedding R(X) → Q(𝒪^h_{X,ξ}) of Stacks 0ENK, which is the parameter E inhabited by genericFractionEmbedding, and the ratio s/s_ξ is the parameter ratio as in Stacks 0EPR and in part (1)”.

Stacks 0EPU, part (2). The Weil divisor class associated to ℒ: the image in Cl(X) of the Weil divisor div_ℒ(s) = ∑_Z ord_{Z,ℒ}(s) [Z] of a nonzero meromorphic section s of ℒ.

It depends only on ℒ and not on s, which is AlgebraicGeometry.Space.divisorClassOfSection_eq and is the use the source makes of Stacks 0EPT.

def divisorClassOfSection (L : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatioFamily.{u, z} B S hS hX hdec L)
    (hfin : LocallyFinite fun W : PrimeDivisor B S hS X ↦
      if divisorCoefficients.{u, z} B S hS hX hdec L s ratio W = 0 then ∅
      else W.support B S hS X) :
    E.weilDivisorClassGroup

AlgebraicGeometry.Space.divisorClassOfSection_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeilDivisorClassOfSection.lean, line 138. The attribute's comment: “part (2): well-definedness, the class of div_ℒ(s) in Cl(X) is independent of the nonzero meromorphic section s; this is the appeal to Stacks 0EPT that the source makes, whose conclusion div_ℒ(s) = div_ℒ(s') + div(f) is read through the coefficientwise membership condition of the subgroup of principal Weil divisors of Stacks 0ENR”.

Stacks 0EPU, part (2), well-definedness. The Weil divisor class of ℒ does not depend on the chosen nonzero meromorphic section: if the ratios of s and of s' at the generic point of every prime divisor differ by the image of an invertible rational function f — which is the assertion f = s/s' ∈ R(X)^* of Stacks 0EPT — then div_ℒ(s) and div_ℒ(s') differ by the principal divisor div(f), hence have the same class in Cl(X).

theorem divisorClassOfSection_eq (L : Modules.{u, max u z} B S hS X hX)
    (s s' : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatioFamily.{u, z} B S hS hX hdec L)
    (hfin : LocallyFinite fun W : PrimeDivisor B S hS X ↦
      if divisorCoefficients.{u, z} B S hS hX hdec L s ratio W = 0 then ∅
      else W.support B S hS X)
    (hfin' : LocallyFinite fun W : PrimeDivisor B S hS X ↦
      if divisorCoefficients.{u, z} B S hS hX hdec L s' ratio W = 0 then ∅
      else W.support B S hS X)
    (f : (rationalFunctions B S hS hX)ˣ)
    (hs : ∀ W : PrimeDivisor B S hS X,
      (ratio W s : W.genericTotalFractionRing B S hS hX hdec) =
        E.emb W (f : rationalFunctions B S hS hX) *
          (ratio W s' : W.genericTotalFractionRing B S hS hX hdec)) :
    divisorClassOfSection.{u, z} B S hS hX hdec E L s ratio hfin =
      divisorClassOfSection.{u, z} B S hS hX hdec E L s' ratio hfin'

AlgebraicGeometry.Space.divisorClassOfSectionOfGenerating, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeilDivisorClassOfSection.lean, line 171. The attribute's comment: “part (2): the Weil divisor class of ℒ in Cl(X), with the local finiteness of the support of div_ℒ(s) supplied by Stacks 0EPS from the open subspace U over which s generates ℒ”.

Stacks 0EPU, part (2). The Weil divisor class of ℒ, with the local finiteness that makes div_ℒ(s) a Weil divisor supplied by Stacks 0EPS from a nonempty open subset of |X| containing the generic point of no prime divisor along which s has nonzero order — the open subspace over which the nonzero meromorphic section s generates ℒ.

def divisorClassOfSectionOfGenerating
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsLocallyNoetherian Y))
    (hirr : IrreducibleSpace (points B S hS X)) (L : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (ratio : LocalRatioFamily.{u, z} B S hS hX hdec L)
    (U : Set (points B S hS X)) (hUopen : IsOpen U) (hUne : U.Nonempty)
    (hgen : ∀ W : PrimeDivisor B S hS X,
      divisorCoefficients.{u, z} B S hS hX hdec L s ratio W ≠ 0 →
        W.genericPoint B S hS X ∈ Uᶜ) :
    E.weilDivisorClassGroup

Tag 0EPV, a lemma

Tag 0EPV in the Stacks Project.

AlgebraicGeometry.Space.orderOfVanishingSection_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DivisorOfMeromorphicSection.lean, line 938. The attribute's comment: “div_{ℒ⊗𝒩}(st) = div_ℒ(s) + div_𝒩(t) coefficientwise; ℒ⊗𝒩 is the module M”.

Stacks 0EPV, coefficientwise. If the ratio of st at the generic point of Z is the product of the ratios of s and of t, then ord_{Z,ℒ⊗𝒩}(st) = ord_{Z,ℒ}(s) + ord_{Z,𝒩}(t). Summing over all prime divisors this is the identity div_{ℒ⊗𝒩}(st) = div_ℒ(s) + div_𝒩(t) of Weil divisors.

theorem orderOfVanishingSection_mul (L N M : Modules.{u, max u z} B S hS X hX)
    (s : MeromorphicSection.{u, z} B S hS X hX L)
    (t : MeromorphicSection.{u, z} B S hS X hX N)
    (st : MeromorphicSection.{u, z} B S hS X hX M)
    (ratioL : LocalRatio.{u, z} B S hS hX hdec Z L)
    (ratioN : LocalRatio.{u, z} B S hS hX hdec Z N)
    (ratioM : LocalRatio.{u, z} B S hS hX hdec Z M)
    (hst : (ratioM st : Z.genericTotalFractionRing B S hS hX hdec) =
      (ratioL s : Z.genericTotalFractionRing B S hS hX hdec) *
        (ratioN t : Z.genericTotalFractionRing B S hS hX hdec)) :
    orderOfVanishingSection.{u, z} B S hS hX hdec Z M st ratioM =
      orderOfVanishingSection.{u, z} B S hS hX hdec Z L s ratioL +
        orderOfVanishingSection.{u, z} B S hS hX hdec Z N t ratioN

AlgebraicGeometry.Space.exists_ne_zero_weilDivisorOfSection_meromorphicSectionTensor_eq_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvertibleModuleWeilDivisorClass.lean, line 335. The attribute's comment: “the whole lemma at the source's hypotheses: for nonzero meromorphic sections s of ℒ and t of 𝒩 on a locally Noetherian integral X, the product st (meromorphicSectionTensor) is a nonzero meromorphic section of ℒ ⊗ 𝒩, div_{ℒ⊗𝒩}(st) = div_ℒ(s) + div_𝒩(t) in Div(X), and the Weil divisor class of ℒ ⊗ 𝒩 in the canonical Cl(X) of Stacks 0ENR is the sum of the classes of ℒ and 𝒩 (Stacks 0EPU part (2) evaluated at s, t and st)”.

Stacks 0EPV. Let X be a locally Noetherian integral algebraic space over S, let ℒ, 𝒩 be invertible 𝒪_X-modules and let s, resp. t, be a nonzero meromorphic section of ℒ, resp. 𝒩. Then st is a nonzero meromorphic section of ℒ ⊗_{𝒪_X} 𝒩 and

div_{ℒ⊗𝒩}(st) = div_ℒ(s) + div_𝒩(t)

in Div(X). In particular the Weil divisor class of ℒ ⊗_{𝒪_X} 𝒩 is the sum of the Weil divisor classes of ℒ and of 𝒩, in the class group Cl(X) of Stacks 0ENR.

The product st is AlgebraicGeometry.Space.meromorphicSectionTensor, the global product of the two sections (the chartwise product of their representatives over every affine chart), whose hypotheses (a) and (b) of Stacks 0EN6 are X's own; the divisors are AlgebraicGeometry.Space.weilDivisorOfSection (Stacks 0EPU, part (1)). The product is regular, hence nonzero; at the generic point of every prime divisor its coefficient is a unit times the product of the coefficients of s and of t, so the orders of vanishing add up. The class statement is then the definition of the class (AlgebraicGeometry.Space.weilDivisorClassOfInvertible, Stacks 0EPU, part (2)) evaluated at s, t and st, by AlgebraicGeometry.Space.weilDivisorClassOfInvertible_eq, and additivity of the quotient map Div(X) → Cl(X).

theorem exists_ne_zero_weilDivisorOfSection_meromorphicSectionTensor_eq_add
    (L N : Modules.{u, u} B S hS X hX) (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L)
    (hNinv : IsInvertibleModule (B := B) ⟨X, hX⟩ N)
    (s : MeromorphicSection.{u, u} B S hS X hX L) (t : MeromorphicSection.{u, u} B S hS X hX N)
    (hs : s ≠ 0) (ht : t ≠ 0) :
    ∃ hst : meromorphicSectionTensor B S hS hX
        (fun _ hz => (weaklyAssociatedPointsOfSpace_eq_setOf_localRingDimension_eq_zero
          B S hS ⟨X, hX⟩ hInt.hasEtaleLocalProperty_isReduced).subset hz)
        (hasLocallyFiniteIrreducibleComponents_of_isLocallyNoetherian B S hS X hX hN) L N s t
        (isQuasicoherentOnSite_of_isInvertibleModule (⟨X, hX⟩ : AlgebraicSpaces B S hS) L hL)
        (isQuasicoherentOnSite_of_isInvertibleModule (⟨X, hX⟩ : AlgebraicSpaces B S hS) N
          hNinv) ≠ 0,
      weilDivisorOfSection B S hS hX hInt hN (picardTensorModule B S hS hX L N)
          (isInvertibleModule_picardTensorModule B S hS hX L N hL hNinv) _ hst =
        weilDivisorOfSection B S hS hX hInt hN L hL s hs +
          weilDivisorOfSection B S hS hX hInt hN N hNinv t ht ∧
      weilDivisorClassOfInvertible B S hS hX hInt hN (picardTensorModule B S hS hX L N)
          (isInvertibleModule_picardTensorModule B S hS hX L N hL hNinv) =
        weilDivisorClassOfInvertible B S hS hX hInt hN L hL +
          weilDivisorClassOfInvertible B S hS hX hInt hN N hNinv

AlgebraicGeometry.Space.PicardDivisorData.divisor_picardTensorModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PicardWeilDivisorClass.lean, line 454. The attribute's comment: “the identity div_{ℒ⊗𝒩}(st) = div_ℒ(s) + div_𝒩(t) in Div(X), at the sections and ratio families chosen by PicardDivisorData; st/(s_ξ t_ξ) = (s/s_ξ)(t/t_ξ), the source's own computation, is the argument hst, as it is in the coefficientwise orderOfVanishingSection_mul: the ratio s/s_ξ is a parameter here as in Stacks 0EPR, and the generator chosen at ξ for ℒ⊗𝒩 differs from s_ξ ⊗ t_ξ by a unit that no choice pins to 1 (HasCanonicalTensorProductSection), so hst is not derivable. What the data gives with no extra input is the weaker exists_ord_sub_eq_tensorModule, used by divisorClass_picardTensorModule”.

Stacks 0EPV, the identity in Div(X). The Weil divisor of the chosen section of ℒ ⊗ 𝒩 is the sum of the Weil divisors of the chosen sections of ℒ and of 𝒩, as soon as the ratio of the chosen section of the tensor product is the product of the ratios.

This is div_{ℒ⊗𝒩}(st) = div_ℒ(s) + div_𝒩(t) as an identity of Weil divisors, on the nose rather than up to the divisor of a rational function; AlgebraicGeometry.Space.orderOfVanishingSection_mul is the same identity coefficientwise at a single prime divisor, of which this is the sum over all of them.

The ratio identity st/(s_ξ t_ξ) = (s/s_ξ)(t/t_ξ) is the source's own computation, and it is the argument hst here rather than a field of AlgebraicGeometry.Space.PicardDivisorData, exactly as it is the argument hst of the coefficientwise AlgebraicGeometry.Space.orderOfVanishingSection_mul. It is not derivable from the data, and for two independent reasons. The generator chosen at ξ for ℒ ⊗ 𝒩 and the product of the generators chosen for ℒ and for 𝒩 are two free generators of one invertible module, so they differ by a unit of the local ring that nothing pins to 1 — see the docstring of AlgebraicGeometry.Space.HasCanonicalTensorProductSection, which is why the canonical choices produce the identity only up to such a unit. And the section chosen for ℒ ⊗ 𝒩 is a section of that module alone: it differs from the product of the chosen sections of ℒ and of 𝒩 by an element of R(X)^* whose divisor is in general nonzero. What the data does give, with no extra argument, is the weaker exists_ord_sub_eq_tensorModule — the two divisors differ by the divisor of an invertible rational function — and that is what AlgebraicGeometry.Space.PicardDivisorData.divisorClass_picardTensorModule uses, which is why only the class of the divisor of a tensor product is additive for an arbitrary AlgebraicGeometry.Space.PicardDivisorData.

theorem divisor_picardTensorModule (L N : Modules.{u, u} B S hS X hX)
    (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L)
    (hN : IsInvertibleModule (B := B) ⟨X, hX⟩ N)
    (hst : ∀ W : PrimeDivisor B S hS X,
      (D.ratio (picardTensorModule B S hS hX L N)
          (isInvertibleModule_picardTensorModule B S hS hX L N hL hN) W
          (D.sect _ (isInvertibleModule_picardTensorModule B S hS hX L N hL hN)) :
        W.genericTotalFractionRing B S hS hX hdec) =
        (D.ratio L hL W (D.sect L hL) : W.genericTotalFractionRing B S hS hX hdec) *
          (D.ratio N hN W (D.sect N hN) : W.genericTotalFractionRing B S hS hX hdec)) :
    D.divisor (picardTensorModule B S hS hX L N)
        (isInvertibleModule_picardTensorModule B S hS hX L N hL hN) =
      D.divisor L hL + D.divisor N hN

AlgebraicGeometry.Space.PicardDivisorData.divisorClass_picardTensorModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PicardWeilDivisorClass.lean, line 493. The attribute's comment: “the in-particular clause: the Weil divisor class of ℒ ⊗ 𝒩 is the sum of the Weil divisor classes of ℒ and of 𝒩, from the field exists_ord_sub_eq_tensorModule and so with nothing assumed of the chosen sections; divisor_picardTensorModule is the identity in Div(X), which needs the ratio identity. Cl(X) is Stacks 0ENR relative to the embedding R(X) → Q(𝒪^h_{X,ξ}) of Stacks 0ENK, which is the parameter E inhabited by genericFractionEmbedding”.

Stacks 0EPV, the clause in Cl(X). The Weil divisor class of a tensor product of invertible 𝒪_X-modules is the sum of their Weil divisor classes: the Weil divisor of the chosen section of ℒ ⊗ 𝒩 and the sum of the Weil divisors of the chosen sections of ℒ and of 𝒩 differ by div(f) for an invertible rational function f, which is zero in Cl(X).

This is the source's "in particular" clause. It asks nothing of the three chosen sections, so unlike AlgebraicGeometry.Space.PicardDivisorData.divisor_picardTensorModule it is not an identity in Div(X).

theorem divisorClass_picardTensorModule (L N : Modules.{u, u} B S hS X hX)
    (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L)
    (hN : IsInvertibleModule (B := B) ⟨X, hX⟩ N) :
    D.divisorClass (picardTensorModule B S hS hX L N)
        (isInvertibleModule_picardTensorModule B S hS hX L N hL hN) =
      D.divisorClass L hL + D.divisorClass N hN

AlgebraicGeometry.Space.exists_divisorOfSection_canonicalLocalRatioFamily_picardTensorModule_eq_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PicardWeilDivisorClassTensor.lean, line 615. The attribute's comment: “the identity div_{ℒ⊗𝒩}(st) = div_ℒ(s) + div_𝒩(t) in Div(X), read through the ratio families of Stacks 0EPR, for arbitrary regular meromorphic sections s of ℒ and t of 𝒩 and for their product st, whose existence is the source's first clause and is asserted here too; nothing is assumed beyond X being decent, locally Noetherian and integral. The source's computation st/(s_ξ t_ξ) = (s/s_ξ)(t/t_ξ) holds up to a unit of 𝒪_{U,u}, the discrepancy between the generator chosen at ξ for ℒ⊗𝒩 and the product of those chosen for ℒ and for 𝒩, and that unit has order of vanishing zero. The whole lemma for nonzero sections, with the in-particular clause in the canonical Cl(X), is exists_ne_zero_weilDivisorOfSection_meromorphicSectionTensor_eq_add”.

Stacks 0EPV's identity in Div(X). Let X be a decent, locally Noetherian, integral algebraic space over S, let ℒ and 𝒩 be invertible 𝒪_X-modules, let s be a regular meromorphic section of ℒ and let t be one of 𝒩. Then there is a regular meromorphic section st of ℒ ⊗ 𝒩 which is the product of s and of t — its coefficient of Stacks 0EPR at the generic point of every prime divisor is the product of the coefficients of s and of t, up to a unit of 𝒪_{U, u} — and the Weil divisors read through the ratio families of Stacks 0EPR satisfy

div_{ℒ⊗𝒩}(st) = div_ℒ(s) + div_𝒩(t)

as an identity of elements of Div(X), on the nose and not merely up to the divisor of a rational function. Nothing is assumed beyond X itself.

This is the source's statement: the existence of the product section is its first clause and is asserted here too, the identity in Div(X) its second, and s and t range over all regular meromorphic sections as they do there. The unit in the product clause is unavoidable and is harmless: the generator chosen at ξ for ℒ ⊗ 𝒩 and the product of the generators chosen for ℒ and for 𝒩 are two free generators of one invertible module, so they differ by a unit (AlgebraicGeometry.Space.PrimeDivisor.exists_isUnit_smul_genericStalkGenerator) whose order of vanishing is zero — the source's own computation st/(s_ξ t_ξ) = (s/s_ξ)(t/t_ξ) holds up to exactly that unit, and it is discarded by AlgebraicGeometry.Space.PrimeDivisor.orderOfVanishingSection_canonicalLocalRatio_eq_add_of_genericStalkCoefficient_eq_unit_mul.

The product section is the chartwise product AlgebraicGeometry.Space.meromorphicSectionTensorMul amalgamated over an affine covering, AlgebraicGeometry.Space.meromorphicSectionTensor, and the local finiteness that makes each of the three divisors an element of Div(X) is AlgebraicGeometry.Space.locallyFinite_divisorCoefficients_ne_zero_canonicalLocalRatioFamily.

AlgebraicGeometry.Space.PicardDivisorData.divisor_picardTensorModule is the same identity for the sections and ratio families that an arbitrary AlgebraicGeometry.Space.PicardDivisorData chooses, where the chosen section of ℒ ⊗ 𝒩 has no relation to the chosen sections of ℒ and of 𝒩 and the ratio identity has to be supplied; at the canonical choices and for the product section, as here, it is proved.

theorem exists_divisorOfSection_canonicalLocalRatioFamily_picardTensorModule_eq_add
    (s : MeromorphicSection.{u, u} B S hS X hX L)
    (t : MeromorphicSection.{u, u} B S hS X hX N)
    (hs : IsRegularMeromorphicSection.{u, u} B S hS X hX L s)
    (ht : IsRegularMeromorphicSection.{u, u} B S hS X hX N t) :
    haveI : ∀ W : PrimeDivisor B S hS X,
        Nontrivial ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.nontrivial_genericHenselianLocalRing B S hS hX hdec hInt hNoeth
    haveI : ∀ W : PrimeDivisor B S hS X,
        IsNoetherianRing ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.isNoetherianRing_genericHenselianLocalRing B S hS hX hdec hInt hNoeth
    haveI : ∀ W : PrimeDivisor B S hS X,
        Ring.KrullDimLE 1 ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.krullDimLE_genericHenselianLocalRing B S hS hX hdec hInt hNoeth
    ∃ (st : MeromorphicSection.{u, u} B S hS X hX (picardTensorModule B S hS hX L N))
      (_ : IsRegularMeromorphicSection.{u, u} B S hS X hX
        (picardTensorModule B S hS hX L N) st),
      (∀ W : PrimeDivisor B S hS X,
          ∃ w : (structurePresheaf B S hS (W.genericStalkSpace B S hS hX hdec).1).obj
            (op (W.genericStalkChart B S hS hX hdec)),
            IsUnit w ∧
              W.genericStalkCoefficient B S hS hX hdec (picardTensorModule B S hS hX L N)
                  (isInvertibleModule_picardTensorModule B S hS hX L N hL hNinv) st =
                algebraMap ((structurePresheaf B S hS
                      (W.genericStalkSpace B S hS hX hdec).1).obj
                    (op (W.genericStalkChart B S hS hX hdec)))
                  ((meromorphicFunctionSheaf B S hS (W.genericStalkSpace B S hS hX hdec).1
                    (W.genericStalkSpace B S hS hX hdec).2).obj.obj
                      (op (W.genericStalkChart B S hS hX hdec))) w *
                  (W.genericStalkCoefficient B S hS hX hdec L hL s *
                    W.genericStalkCoefficient B S hS hX hdec N hNinv t)) ∧
        ∃ (hfinst : LocallyFinite fun W : PrimeDivisor B S hS X =>
              if divisorCoefficients.{u, u} B S hS hX hdec
                  (picardTensorModule B S hS hX L N) st
                  (canonicalLocalRatioFamily B S hS hX hdec
                    (picardTensorModule B S hS hX L N)
                    (isInvertibleModule_picardTensorModule B S hS hX L N hL hNinv)
                    hInt hNoeth) W = 0 then ∅
              else W.support B S hS X)
          (hfins : LocallyFinite fun W : PrimeDivisor B S hS X =>
              if divisorCoefficients.{u, u} B S hS hX hdec L s
                  (canonicalLocalRatioFamily B S hS hX hdec L hL hInt hNoeth) W = 0 then ∅
              else W.support B S hS X)
          (hfint : LocallyFinite fun W : PrimeDivisor B S hS X =>
              if divisorCoefficients.{u, u} B S hS hX hdec N t
                  (canonicalLocalRatioFamily B S hS hX hdec N hNinv hInt hNoeth) W = 0 then ∅
              else W.support B S hS X),
          divisorOfSection.{u, u} B S hS hX hdec (picardTensorModule B S hS hX L N) st
                (canonicalLocalRatioFamily B S hS hX hdec (picardTensorModule B S hS hX L N)
                  (isInvertibleModule_picardTensorModule B S hS hX L N hL hNinv) hInt hNoeth)
                hfinst =
            divisorOfSection.{u, u} B S hS hX hdec L s
                (canonicalLocalRatioFamily B S hS hX hdec L hL hInt hNoeth) hfins +
              divisorOfSection.{u, u} B S hS hX hdec N t
                (canonicalLocalRatioFamily B S hS hX hdec N hNinv hInt hNoeth) hfint

Tag 0EPW, an equation

Tag 0EPW in the Stacks Project.

AlgebraicGeometry.Space.canonicalPicardToWeilDivisorClassHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PicardWeilDivisorClassHom.lean, line 107. The attribute's comment: “the homomorphism Pic(X) → Cl(X) assigning to an invertible module its Weil divisor class, on a locally Noetherian integral algebraic space X over a scheme S — the hypotheses of Lemma 72.7.5 and no others, decency coming from integrality by IsIntegralSpace.isDecentSpace”.

The homomorphism of abelian groups

Pic(X) ⟶ Cl(X)

which assigns to an invertible 𝒪_X-module its Weil divisor class, on a locally Noetherian integral algebraic space X over a scheme S.

It is AlgebraicGeometry.Space.PicardDivisorData.picardToWeilDivisorClassGroup at the canonical choices: the embedding R(X) → Q(𝒪^h_{X, ξ}) of Stacks 0ENK, the regular meromorphic sections of Stacks 0EPQ and the ratio family of Stacks 0EPR. Its value on the class of an invertible module is that module's Weil divisor class (AlgebraicGeometry.Space.canonicalPicardToWeilDivisorClassHom_picardClass), well defined on isomorphism classes by Stacks 0EPT, and additivity is Stacks 0EPV, addition in Pic(X) being tensor product.

def canonicalPicardToWeilDivisorClassHom :
    haveI hdec : IsDecentSpace B S hS X := hInt.isDecentSpace B S hS X
    picardGroup (B := B) (S := S) (hS := hS) ⟨X, hX⟩ →+
      (genericFractionEmbedding B S hS hX hdec hInt hN).weilDivisorClassGroup

AlgebraicGeometry.Space.canonicalPicardToWeilDivisorClassHom_picardClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PicardWeilDivisorClassHom.lean, line 135. The attribute's comment: “the value of the homomorphism Pic(X) → Cl(X) on the class of an invertible module, which characterizes it, on a locally Noetherian integral algebraic space X over a scheme S — the hypotheses of Lemma 72.7.5 and no others, decency coming from integrality by IsIntegralSpace.isDecentSpace”.

The homomorphism Pic(X) ⟶ Cl(X) sends the class of an invertible 𝒪_X-module to its Weil divisor class — the class of the Weil divisor of the regular meromorphic section of Stacks 0EPQ read through the ratio family of Stacks 0EPR. This characterizes the homomorphism, because every class in Pic(X) is the class of an invertible module.

theorem canonicalPicardToWeilDivisorClassHom_picardClass (L : Modules.{u, u} B S hS X hX)
    (hL : IsInvertibleModule (B := B) ⟨X, hX⟩ L) :
    haveI hdec : IsDecentSpace B S hS X := hInt.isDecentSpace B S hS X
    haveI : ∀ W : PrimeDivisor B S hS X,
        Nontrivial ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.nontrivial_genericHenselianLocalRing B S hS hX hdec hInt hN
    haveI : ∀ W : PrimeDivisor B S hS X,
        IsNoetherianRing ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.isNoetherianRing_genericHenselianLocalRing B S hS hX hdec hInt hN
    haveI : ∀ W : PrimeDivisor B S hS X,
        Ring.KrullDimLE 1 ↥(W.genericHenselianLocalRing B S hS hX hdec) := fun W =>
      W.krullDimLE_genericHenselianLocalRing B S hS hX hdec hInt hN
    canonicalPicardToWeilDivisorClassHom B S hS hX hInt hN
          (picardClass (B := B) ⟨X, hX⟩ L hL) =
        (canonicalPicardDivisorData B S hS hX hdec hInt hN
          (canonicalRatioIsUnitOnGeneratingChart B S hS hX hdec hInt hN)
          (canonicalTensorDivisorIdentity_of_exists_product B S hS hX hdec hInt hN
            (hasCanonicalTensorProductSection B S hS hX hdec hInt hN))).divisorClass L hL

Tag 0EPX, a lemma

Tag 0EPX in the Stacks Project.

AlgebraicGeometry.Space.injective_canonicalPicardToWeilDivisorClassHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PicardWeilDivisorClassInjective.lean, line 324. The attribute's comment: “injectivity of Pic(X) → Cl(X) — the homomorphism of Stacks 0EPW at the canonical choices, which takes no auxiliary data — on a normal, locally Noetherian, integral algebraic space over a scheme. No hypothesis beyond the source's: decency comes from integrality by IsIntegralSpace.isDecentSpace, the claim of the source is picardClass_eq_zero_of_forall_isUnit_canonicalGenericRatio, the rescaling t = f⁻¹ s is exists_isRegularMeromorphicSection_canonicalLocalRatio_eq_genericEmb_mul, and the three instance hypotheses on the henselian local rings at the generic points of the prime divisors are conclusions of Stacks 0ENK”.

Stacks 0EPX. On a normal, locally Noetherian, integral algebraic space X over a scheme S, the homomorphism

Pic(X) ⟶ Cl(X)

of Stacks 0EPW — AlgebraicGeometry.Space.canonicalPicardToWeilDivisorClassHom, which takes no auxiliary data — is injective.

The binders are the source's and nothing else: X an algebraic space over the scheme S (hX), integral (hInt), locally Noetherian (hN) and normal (hNormal). There is no auxiliary embedding, no divisor data, no decency hypothesis — Stacks 0AD4 puts decency inside integrality, so AlgebraicGeometry.Space.IsIntegralSpace.isDecentSpace supplies it — no instance hypotheses on the henselian local rings at the generic points of the prime divisors, and nothing left of the claim the source makes and calls the whole content of the lemma: that is AlgebraicGeometry.Space.picardClass_eq_zero_of_forall_isUnit_canonicalGenericRatio, passed below. See the module docstring for what each of those discharges is.

Triviality of ℒ is written as the vanishing of its class in Pic(X), which by AlgebraicGeometry.Space.picardClass_eq_zero_iff says that ℒ is isomorphic to 𝒪_X.

theorem injective_canonicalPicardToWeilDivisorClassHom (hNormal : IsNormal B S hS X) :
    Function.Injective (canonicalPicardToWeilDivisorClassHom B S hS hX hInt hN)

Sources

• Section 72.7, Tag 0ENV
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.PrimeDivisor.pullbacksMeromorphicSections_genericHenselianMorphism · AlgebraicGeometry.Space.PrimeDivisor.canonicalGenericRatio · AlgebraicGeometry.Space.PrimeDivisor.isUnit_canonicalGenericRatio · AlgebraicGeometry.Space.PrimeDivisor.canonicalLocalRatio · AlgebraicGeometry.Space.PrimeDivisor.canonicalGenericRatio_smul · AlgebraicGeometry.Space.PrimeDivisor.canonicalGenericRatio_smul_of_eval · AlgebraicGeometry.Space.canonicalLocalRatioFamily · AlgebraicGeometry.Space.PrimeDivisor.orderOfVanishingSection_canonicalLocalRatio_eq_length_sub_length

Section72.8 Modifications and alterations#

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

Tag 0AD8, a definition

Tag 0AD8 in the Stacks Project.

AlgebraicGeometry.Space.IsIntegralModification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralModification.lean, line 85.

Stacks 0AD8. A modification of an integral algebraic space X over S is a birational proper morphism f : X' ⟶ X of algebraic spaces over S with X' integral.

No decency hypotheses are needed: an integral algebraic space is decent, so the decency of the target is hXint.isDecentSpace and that of the source comes with its integrality.

def IsIntegralModification {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hXint : IsIntegralSpace B S hS X) (f : X' ⟶ X) : Prop

Tag 0AD9, a lemma

Tag 0AD9 in the Stacks Project.

AlgebraicGeometry.Space.IsIntegralModification.exists_isIso_fromPreimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralModification.lean, line 132.

Stacks 0AD9. A modification of an integral algebraic space over S is an isomorphism over a nonempty open subspace of its target.

theorem IsIntegralModification.exists_isIso_fromPreimage
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {hX' : IsAlgebraicSpace B S hS X'} {hX : IsAlgebraicSpace B S hS X}
    {hXint : IsIntegralSpace B S hS X} {f : X' ⟶ X}
    (hf : IsIntegralModification B S hS hX' hX hXint f) :
    ∃ U : Subfunctor X, IsOpenSubspace B S hS U ∧
      Nonempty (points B S hS U.toFunctor) ∧ IsIso (U.fromPreimage f)

Tag 0ADA, a definition

Tag 0ADA in the Stacks Project.

AlgebraicGeometry.Space.IsAlteration, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralAlteration.lean, line 84.

Stacks 0ADA. An alteration of an integral algebraic space X over S is a proper dominant morphism f : Y ⟶ X of algebraic spaces over S with Y integral such that the inverse image of some nonempty open subspace U ⊆ X is finite over U.

abbrev IsAlteration (f : Y ⟶ X) : Prop

Tag 0ADB, a lemma

Tag 0ADB in the Stacks Project.

AlgebraicGeometry.Space.isAlteration_iff_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralAlteration.lean, line 126. The attribute's comment: “against condition (4) of Stacks 0AD5”.

Stacks 0ADB. A proper dominant morphism f : Y ⟶ X of integral algebraic spaces over S is an alteration exactly when it is quasi-finite at the generic point of |Y|, which is condition (4) of Stacks 0AD5 and hence equivalent to the other conditions compared there.

theorem isAlteration_iff_isQuasiFiniteAt (hY : IsAlgebraicSpace B S hS Y)
    (hX : IsAlgebraicSpace B S hS X) (hYint : IsIntegralSpace B S hS Y)
    (hXint : IsIntegralSpace B S hS X) (f : Y ⟶ X) (hp : IsProper B S hS f)
    (hdom : IsDominant B S hS f)
    {y : points B S hS Y} (hy : IsGenericPoint y (Set.univ : Set (points B S hS Y)))
    {x : points B S hS X} (hx : IsGenericPoint x (Set.univ : Set (points B S hS X))) :
    IsAlteration B S hS f ↔ IsQuasiFiniteAt B S hS f y

Tag 0DMN, a lemma

Tag 0DMN in the Stacks Project.

AlgebraicGeometry.Space.exists_isClosedSubspace_isAlteration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlterationInProperSurjection.lean, line 164.

Let f : X ⟶ Y be a proper surjective morphism of algebraic spaces over a scheme S with Y integral. Then f restricts to an alteration on some integral closed subspace of X.

theorem exists_isClosedSubspace_isAlteration (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hYint : IsIntegralSpace B S hS Y) (f : X ⟶ Y)
    (hp : IsProper B S hS f) (hsurj : IsSurjective B S hS f) :
    ∃ Z : Subfunctor X, IsClosedSubspace B S hS Z ∧
      IsIntegralSpace B S hS Z.toFunctor ∧ IsAlteration B S hS (Z.ι ≫ f)

Sources

• Section 72.8, Tag 0AD7
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsIntegralModification · AlgebraicGeometry.Space.IsIntegralModification.exists_isIso_fromPreimage · AlgebraicGeometry.Space.IsAlteration · AlgebraicGeometry.Space.isAlteration_iff_isQuasiFiniteAt · AlgebraicGeometry.Space.exists_isClosedSubspace_isAlteration

Section72.9 Schematic locus#

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

Tag 06LZ, a lemma

Tag 06LZ in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_isAbsolutelyQuasiSeparated_of_dimension_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroSeparatedScheme.lean, line 128. The attribute's comment: “case (1): X is a scheme”.

A quasi-separated algebraic space of dimension zero over S is representable.

theorem isRepresentable_of_isAbsolutelyQuasiSeparated_of_dimension_eq_zero
    (hX : IsAlgebraicSpace B S hS X) (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (hdim : dimension B S hS X hX = 0) : X.IsRepresentable

AlgebraicGeometry.Space.isSeparatedSchemeWithAffineQuasiCompactOpens_of_isAbsolutelyQuasiSeparated_of_dimension_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroSeparatedScheme.lean, line 199. The attribute's comment: “case (1)”.

A quasi-separated algebraic space of dimension zero over S is a separated scheme, and every quasi-compact open of it is affine.

theorem
    isSeparatedSchemeWithAffineQuasiCompactOpens_of_isAbsolutelyQuasiSeparated_of_dimension_eq_zero
    (hX : IsAlgebraicSpace B S hS X) (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (hdim : dimension B S hS X hX = 0) :
    IsSeparatedSchemeWithAffineQuasiCompactOpens B S hS X

AlgebraicGeometry.Space.isSeparatedSchemeWithAffineQuasiCompactOpens_of_isNoetherian_of_dimension_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroSeparatedScheme.lean, line 217. The attribute's comment: “case (3)”.

A Noetherian algebraic space of dimension zero over S is a separated scheme, and every quasi-compact open of it is affine.

theorem isSeparatedSchemeWithAffineQuasiCompactOpens_of_isNoetherian_of_dimension_eq_zero
    (hX : IsAlgebraicSpace B S hS X) (hnoeth : IsNoetherian B S hS hZ X)
    (hdim : dimension B S hS X hX = 0) :
    IsSeparatedSchemeWithAffineQuasiCompactOpens B S hS X

AlgebraicGeometry.Space.isRepresentable_of_isNoetherian_of_dimension_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroSeparatedScheme.lean, line 226. The attribute's comment: “case (3): X is a scheme”.

A Noetherian algebraic space of dimension zero over S is representable.

theorem isRepresentable_of_isNoetherian_of_dimension_eq_zero
    (hX : IsAlgebraicSpace B S hS X) (hnoeth : IsNoetherian B S hS hZ X)
    (hdim : dimension B S hS X hX = 0) : X.IsRepresentable

AlgebraicGeometry.Space.isSeparatedSchemeWithAffineQuasiCompactOpens_of_isLocallyOfFiniteType_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroSeparatedScheme.lean, line 412. The attribute's comment: “case (2)”.

An algebraic space over S of dimension zero which is locally of finite type over a field k is a separated scheme, and every quasi-compact open of it is affine.

theorem isSeparatedSchemeWithAffineQuasiCompactOpens_of_isLocallyOfFiniteType_over_field
    (hX : IsAlgebraicSpace B S hS X) {k : Type u} [Field k]
    {K : BigFppfOver B (⊤_ Scheme.{u}) hZ}
    (eK : (BigFppfOver.toScheme B (⊤_ Scheme.{u}) hZ).obj K ≅ Spec (.of k))
    {f : viewOverIntegers B S hS hZ X ⟶ yoneda.obj K}
    (hf : IsLocallyOfFiniteType B (⊤_ Scheme.{u}) hZ f)
    (hdim : dimension B S hS X hX = 0) :
    IsSeparatedSchemeWithAffineQuasiCompactOpens B S hS X

AlgebraicGeometry.Space.isRepresentable_of_isLocallyOfFiniteType_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroSeparatedScheme.lean, line 427. The attribute's comment: “case (2): X is a scheme”.

An algebraic space over S of dimension zero which is locally of finite type over a field is representable.

theorem isRepresentable_of_isLocallyOfFiniteType_over_field (hX : IsAlgebraicSpace B S hS X)
    {k : Type u} [Field k] {K : BigFppfOver B (⊤_ Scheme.{u}) hZ}
    (eK : (BigFppfOver.toScheme B (⊤_ Scheme.{u}) hZ).obj K ≅ Spec (.of k))
    {f : viewOverIntegers B S hS hZ X ⟶ yoneda.obj K}
    (hf : IsLocallyOfFiniteType B (⊤_ Scheme.{u}) hZ f)
    (hdim : dimension B S hS X hX = 0) : X.IsRepresentable

Tag 0ADC, a lemma

Tag 0ADC in the Stacks Project.

AlgebraicGeometry.Space.tfae_localRingDimension_eq_zero_and_exists_isRepresentable_isOpenSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiSeparatedSchematicLocusCodimensionZero.lean, line 174.

Let x be a point of a quasi-separated algebraic space over S. The following are equivalent: 1. x is a point of codimension 0 on the space, that is, by Tag 04NA, the dimension of the local ring there is 0; 2. the local ring of the space at x has dimension 0, in the chart-wise form of Tag 0BAM: every étale scheme chart has a local ring of Krull dimension 0 at each point above x; 3. x is a generic point of an irreducible component of the space of points.

If these hold, then some open subspace of the space containing x is a scheme.

theorem tfae_localRingDimension_eq_zero_and_exists_isRepresentable_isOpenSubspace
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ F) (x : points B S hS F) :
    [localRingDimension B S hS x = 0, AllChartsLocalRingDimension B S hS x 0,
        x ∈ genericPoints (points B S hS F)].TFAE ∧
      (localRingDimension B S hS x = 0 →
        ∃ G : Subfunctor F, IsOpenSubspace B S hS G ∧ G.toFunctor.IsRepresentable ∧
          x ∈ Set.range (pointsMap B S hS G.toFunctor G.ι))

AlgebraicGeometry.Space.exists_isRepresentable_isOpenSubspace_mem_range_of_mem_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiLocallyQuasiSeparatedCodimensionZero.lean, line 309. The attribute's comment: “the final statement”.

Stacks 0ADC, the final statement. A generic point of an irreducible component of the space of points of a quasi-separated algebraic space over S lies in an open subspace which is a scheme, namely in the schematic locus of Tag 03JH.

The equivalence of the tag's conditions (1), (2) and (3) is AlgebraicGeometry.Space.localRingDimension_eq_zero_iff_mem_genericPoints_of_quasiSeparated; the codimension-zero clause of Tag 06NH which carries such a generic point into the schematic locus is codimensionZero_mem_schematicLocus_of_isZariskiLocallyQuasiSeparated above.

theorem exists_isRepresentable_isOpenSubspace_mem_range_of_mem_genericPoints
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ F)
    (x : points B S hS F) (hx : x ∈ genericPoints (points B S hS F)) :
    ∃ G : Subfunctor F, IsOpenSubspace B S hS G ∧ G.toFunctor.IsRepresentable ∧
      x ∈ Set.range (pointsMap B S hS G.toFunctor G.ι)

AlgebraicGeometry.Space.localRingDimension_eq_zero_iff_mem_genericPoints_of_quasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiLocallyQuasiSeparatedSchematicLocus.lean, line 137. The attribute's comment: “the equivalence of conditions (1), (2) and (3)”.

A point of a quasi-separated algebraic space over S has a local ring of dimension zero — equivalently, is a point of codimension 0 — exactly when it is a generic point of an irreducible component of the space of points.

theorem localRingDimension_eq_zero_iff_mem_genericPoints_of_quasiSeparated
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ F) (x : points B S hS F) :
    localRingDimension B S hS x = 0 ↔ x ∈ genericPoints (points B S hS F)

Tag 0ADD, a lemma

Tag 0ADD in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_isRepresentable_of_localRingDimension_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CodimensionOneSchematicLocus.lean, line 341.

Stacks 0ADD. Let X be an algebraic space over S which is separated and locally Noetherian, and let x ∈ |X| be a point whose local ring has dimension at most one (Stacks 04NA). Then there is an open subspace of X containing x which is a scheme, that is, whose functor of points is representable.

An affine étale chart V ⟶ X through x has open image Z₀, which is quasi-compact, separated and locally Noetherian; V is immersed over Z₀ in a proper representable morphism, the fibres of V ⟶ Z₀ at field-valued points have bounded degree, and AlgebraicGeometry.Space.exists_isOpenSubspace_isRepresentable_of_chart_rank_le applies.

theorem exists_isOpenSubspace_isRepresentable_of_localRingDimension_le_one
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hsep : IsAbsolutelySeparated B S hS B.contains_terminal X)
    (hnoeth : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (x : points B S hS X) (hdim : localRingDimension B S hS x ≤ 1) :
    ∃ G : Subfunctor X, IsOpenSubspace B S hS G ∧ G.toFunctor.IsRepresentable ∧
      x ∈ Set.range (pointsMap B S hS G.toFunctor G.ι)

Tag 0ADE, a remark

Tag 0ADE in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_isRepresentable_of_localRingDimension_le_one_of_fittingBlowups, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CodimensionOneSchematicLocusByFlattening.lean, line 424. The attribute's comment: “Lemma 0ADD proved along the route of the remark, avoiding Stacks 0ABI”.

Stacks 0ADE. Let X be an algebraic space over S which is separated and locally Noetherian, and let x ∈ |X| be a point whose local ring has dimension at most one (Stacks 04NA). Then there is an open subspace of X containing x which is a scheme, that is, whose functor of points is representable; the route of the remark makes it an affine scheme, which is recorded as well.

This is the statement of Stacks 0ADD, proved along the route of the remark Stacks 0ADE, which avoids More on Groupoids, Lemma 0ABI: the finite surjective cover by a scheme near x comes from the induction on the degree of an affine étale chart through x (exists_isOpenSubspace_isRepresentable_of_chart_rank_le_of_fittingBlowups), and the remark's Steps 1 to 5 — reduction, flattening by blowing up Fitting ideals (Stacks 0D0Q), the finite flat quotient of Stacks 07S6 with Stacks 09NN, the affine open with saturated principal trace via Stacks 0ADC and 09NN, and Stacks 07VP — turn it into an open subspace which is a scheme.

theorem exists_isOpenSubspace_isRepresentable_of_localRingDimension_le_one_of_fittingBlowups
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hsep : IsAbsolutelySeparated B S hS B.contains_terminal X)
    (hnoeth : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (x : points B S hS X) (hdim : localRingDimension B S hS x ≤ 1) :
    ∃ G : Subfunctor X, IsOpenSubspace B S hS G ∧ G.toFunctor.IsRepresentable ∧
      IsAffineSpace B S hS G.toFunctor ∧ x ∈ Set.range (pointsMap B S hS G.toFunctor G.ι)

Sources

• Section 72.9, Tag 06LY
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isRepresentable_of_isAbsolutelyQuasiSeparated_of_dimension_eq_zero · AlgebraicGeometry.Space.isSeparatedSchemeWithAffineQuasiCompactOpens_of_isAbsolutelyQuasiSeparated_of_dimension_eq_zero · AlgebraicGeometry.Space.isSeparatedSchemeWithAffineQuasiCompactOpens_of_isNoetherian_of_dimension_eq_zero · AlgebraicGeometry.Space.isRepresentable_of_isNoetherian_of_dimension_eq_zero · AlgebraicGeometry.Space.isSeparatedSchemeWithAffineQuasiCompactOpens_of_isLocallyOfFiniteType_over_field · AlgebraicGeometry.Space.isRepresentable_of_isLocallyOfFiniteType_over_field · AlgebraicGeometry.Space.tfae_localRingDimension_eq_zero_and_exists_isRepresentable_isOpenSubspace · AlgebraicGeometry.Space.exists_isRepresentable_isOpenSubspace_mem_range_of_mem_genericPoints

Section72.10 Schematic locus and field extension#

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

Tag 0B83, a lemma

Tag 0B83 in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_isPurelyInseparable_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PurelyInseparableSchemeDescent.lean, line 304.

Stacks 0B83. Let k be a field and let X be an algebraic space over k. If there exists a purely inseparable field extension k'/k such that the base change X_{k'} is a scheme, then X is a scheme.

The projection X_{k'} ⟶ X is integral, surjective and universally injective, hence integral and bijective on the points of Stacks 03BU, so the proof of Stacks 07VV, AlgebraicGeometry.Space.isRepresentable_of_isIntegralHom_of_bijective_of_isAffineSpace, applies once every open subspace W ⊆ X with affine preimage W_{k'} is known to be affine. That preimage is a base change of W along Spec k' ⟶ Spec k, so W is affine by AlgebraicGeometry.Space.isAffineSpace_of_isPullback_specExtensionToBase, which descends affineness along the fpqc covering Spec k' ⟶ Spec k by Stacks 041Z; this replaces the appeal to Stacks 07VT in the proof of Stacks 07VV.

The spectrum of k' lies in the chosen big fppf site as soon as the spectrum of k does, by AlgebraicGeometry.Space.contains_spec_of_isAlgebraic; membership of the site is a proposition, so the statement is unchanged if another proof of it is substituted.

theorem isRepresentable_of_isPurelyInseparable_of_isRepresentable [IsPurelyInseparable k k']
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (hXk' : (extensionBaseChange k k' B hk
      (contains_spec_of_isAlgebraic B k k' hk) X).IsRepresentable) :
    X.IsRepresentable

Tag 0B84, a lemma

Tag 0B84 in the Stacks Project.

AlgebraicGeometry.Space.exists_finite_separable_isRepresentable_relocalizeRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OverFields/AlgClosureSchemeDescent.lean, line 418. The attribute's comment: “part (2)”.

[Stacks, Tag 0B84] part (2). Let k be a field and let X be a quasi-compact and quasi-separated algebraic space over k. If there is a field extension K/k such that the base change X_K is a scheme, then there is a finite separable extension k'/k such that X_{k'} is a scheme.

The proof is the source's. K is the filtered union of its finitely generated k-subalgebras A, and [Stacks, Tag 07SR] makes one of the base changes X_A a scheme; this is AlgebraicGeometry.Space.exists_fgSubalgebra_isRepresentable_relocalizeRestrict. A residue field k₁ of A at a maximal ideal is finite over k by the Nullstellensatz, X_{k₁} is a scheme, and the separable closure k' of k in k₁ is finite separable over k with k₁/k' purely inseparable, so X_{k'} is a scheme by the finite case of [Stacks, Tag 0B83], AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_extensionBaseChange_of_finite.

theorem exists_finite_separable_isRepresentable_relocalizeRestrict (k K : Type u) [Field k]
    [Field K] [Algebra k K] (B : BigFppfSite.{u}) (hk : B.Contains (Spec (.of k)))
    (hK : B.Contains (Spec (.of K))) (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (hXqc : IsQuasiCompactSpace B (Spec (.of k)) hk X)
    (hXqs : IsAbsolutelyQuasiSeparated B (Spec (.of k)) hk B.contains_terminal X)
    (hXK : ((OverShriek.relocalizeRestrict (specExtensionHom k K B hk hK)).obj
      X).IsRepresentable) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k') (_ : Module.Finite k k')
      (_ : Algebra.IsSeparable k k') (hk' : B.Contains (Spec (.of k'))),
      ((OverShriek.relocalizeRestrict (specExtensionHom k k' B hk hk')).obj
        X).IsRepresentable

AlgebraicGeometry.Space.isRepresentable_relocalizeRestrict_algebraicClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OverFields/AlgClosureSchemeDescent.lean, line 597. The attribute's comment: “part (1)”.

[Stacks, Tag 0B84] part (1). Let k be a field with algebraic closure k̄ and let X be a quasi-separated algebraic space over k. If there is a field extension K/k such that the base change X_K is a scheme, then X_{k̄} is a scheme.

The source reduces this to part (2) by covering X with quasi-compact open subspaces and omits the details; they are supplied in AlgebraicGeometry.Space.isRepresentable_relocalizeRestrict_of_isAlgClosed. The spectrum of the algebraic closure lies in the site automatically.

theorem isRepresentable_relocalizeRestrict_algebraicClosure (k K : Type u) [Field k] [Field K]
    [Algebra k K] (B : BigFppfSite.{u}) (hk : B.Contains (Spec (.of k)))
    (hK : B.Contains (Spec (.of K))) (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (hXqs : IsAbsolutelyQuasiSeparated B (Spec (.of k)) hk B.contains_terminal X)
    (hXK : ((OverShriek.relocalizeRestrict (specExtensionHom k K B hk hK)).obj
      X).IsRepresentable) :
    ((OverShriek.relocalizeRestrict (specExtensionHom k (AlgebraicClosure k) B hk
      (contains_spec_of_isAlgebraic B k (AlgebraicClosure k) hk))).obj X).IsRepresentable

Tag 0B86, a lemma

Tag 0B86 in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_extensionBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GaloisBaseChangeQuotient.lean, line 164. The attribute's comment: “the base change is an algebraic space”.

Stacks 0B86, the algebraicity of the base change: the base change of an algebraic space over k along a field extension k'/k is, viewed over k, an algebraic space.

theorem isAlgebraicSpace_extensionBaseChange
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) :
    IsAlgebraicSpace B (Spec (.of k)) hk (extensionBaseChange k k' B hk hk' X)

AlgebraicGeometry.Space.isFreeOnNonemptyPoints_extensionBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GaloisBaseChangeQuotient.lean, line 271. The attribute's comment: “the Galois group acts freely on the base change”.

Stacks 0B86, the freeness assertion: the group of k-automorphisms of k' acts freely on X_{k'}. For a finite Galois extension this is the first half of the tag; freeness in fact needs no assumption on the extension.

theorem isFreeOnNonemptyPoints_extensionBaseChange :
    IsFreeOnNonemptyPoints B (Spec (.of k)) hk (k' ≃ₐ[k] k')
      (extensionBaseChange k k' B hk hk' X)

AlgebraicGeometry.Space.isIso_extensionBaseChangeQuotientLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GaloisBaseChangeQuotient.lean, line 635. The attribute's comment: “X = X_{k'}/G”.

Stacks 0B86, the quotient assertion: for a finite Galois extension k'/k with Galois group G, an algebraic space X over k is the quotient X_{k'}/G.

theorem isIso_extensionBaseChangeQuotientLift [FiniteDimensional k k'] [IsGalois k k']
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) :
    IsIso (extensionBaseChangeQuotientLift k k' B hk hk' X hX.isSheaf)

Tag 0B87, a lemma

Tag 0B87 in the Stacks Project.

AlgebraicGeometry.Space.mem_schematicLocus_actionQuotient_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/FiniteFreeActionSchematicLocus.lean, line 292. The attribute's comment: “for a free action of a finite group on an object of the big fppf site over S in place of an action on an arbitrary algebraic space, the quotient being the quotient sheaf of the graph relation of the action as in the library's form of Tag 071S, freeness being read on the points over the test schemes with nonempty underlying space, and the affine open of condition (2) being presented as in the library's form of Tag 0BA1, by an open immersion into the functor of points of the scheme acted on out of an affine object of the site”.

Stacks 0B87. Let a finite group G act freely on an object V of a big fppf site over a scheme S and let y be a point of the quotient V/G. Then y lies in the schematic locus of V/G if and only if there is an affine object U of the site and an open immersion i : h_U ⟶ h_V whose point set contains every point of h_V above y.

The quotient map is surjective and finite locally free after every representable base change, so this is Stacks 0BA1 for it, read on the chart h_V ⟶ V/G bundled as a morphism of algebraic spaces over S.

theorem mem_schematicLocus_actionQuotient_iff [Finite G]
    (ha : ActsFreelyOnNonemptyPoints (underlyingOver B hS V) G a)
    (y : points B S hS (actionQuotient G B hS V a)) :
    y ∈ Set.range (pointsMap B S hS
        (schematicLocus B S hS (actionQuotient G B hS V a)).toFunctor
        (schematicLocus B S hS (actionQuotient G B hS V a)).ι) ↔
      ∃ (U : BigFppfOver B S hS) (i : yoneda.obj U ⟶ yoneda.obj V),
        IsAffine ((BigFppfOver.toScheme B S hS).obj U) ∧ IsOpenImmersion B S hS i ∧
        ∀ x : points B S hS (yoneda.obj V),
          pointsMap B S hS (yoneda.obj V) (freeActionQuotientMap G B S hS V a ha) x = y →
            x ∈ Set.range (pointsMap B S hS (yoneda.obj U) i)

AlgebraicGeometry.Space.mem_schematicLocus_orbitQuotient_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/FreeActionSpaceSchematicLocus.lean, line 495.

Stacks 0B87. Let S be a scheme, let X be an algebraic space over S, let G be a finite group acting freely on X and let Y = X/G be the quotient of Tag 071S. For a point y of Y the following are equivalent:

1. y lies in the schematic locus of Y — the point set of AlgebraicGeometry.Space.schematicLocus, the largest open subspace of Y which is a scheme (Tag 03JH); and
2. there is an affine open subspace of X, presented as an open immersion i : h_V ⟶ X from an affine object V of the site, whose point set contains the whole fibre of y.

The quotient map X ⟶ X/G is surjective and finite locally free after every representable base change, so this is Stacks 0BA1 for it. Freeness is read on the points over the test objects with nonempty underlying scheme, which is how the library's form of Tag 071S — the form producing the quotient here — reads it.

theorem mem_schematicLocus_orbitQuotient_iff
    (hnat : IsNaturalAction B S hS G X) (hX : IsAlgebraicSpace B S hS X)
    (hfree : IsFreeOnNonemptyPoints B S hS G X)
    (y : points B S hS (orbitQuotientSheaf B S hS G X hnat).obj) :
    y ∈ Set.range (pointsMap B S hS
        (schematicLocus B S hS (orbitQuotientSheaf B S hS G X hnat).obj).toFunctor
        (schematicLocus B S hS (orbitQuotientSheaf B S hS G X hnat).obj).ι) ↔
      ∃ (V : BigFppfOver B S hS) (i : yoneda.obj V ⟶ X),
        IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧ IsOpenImmersion B S hS i ∧
        ∀ x : points B S hS X,
          pointsMap B S hS X (toOrbitQuotient B S hS G X hnat) x = y →
            x ∈ Set.range (pointsMap B S hS (yoneda.obj V) i)

Tag 0B85, a lemma

Tag 0B85 in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_purelyTranscendental_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OverFields/PurelyTranscendentalDescent/Descent.lean, line 239.

Stacks 0B85. Let k be a field and X a quasi-separated algebraic space over k. If there is a purely transcendental field extension K/k such that X_K is a scheme, then X is a scheme. Here X_K is the restriction of X to the big fppf site over Spec K.

theorem isRepresentable_of_isRepresentable_purelyTranscendental_baseChange
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    [PurelyTranscendental k K]
    (B : AlgebraicGeometry.BigFppfSite.{u})
    (hk : B.Contains (Spec (.of k))) (hK : B.Contains (Spec (.of K)))
    (F : (AlgebraicGeometry.BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hF : AlgebraicGeometry.IsAlgebraicSpace B (Spec (.of k)) hk F)
    (hqs : AlgebraicGeometry.Space.IsQuasiSeparatedOver B (Spec (.of k)) hk F)
    (hbase : ((OverShriek.relocalizeRestrict
      (ObjectProperty.homMk
        (Spec.map (CommRingCat.ofHom (algebraMap k K))) :
          B.obj hK ⟶ B.obj hk)).obj F).IsRepresentable) :
    F.IsRepresentable

Tag 0BA7, a remark

Tag 0BA7 in the Stacks Project.

Algebra.IsGeometricallyIrreducible.finiteField_remark, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyIrreducibleFiniteFieldDescent.lean, line 171.

Stacks 0BA7. Let k be a finite field and K/k a geometrically irreducible field extension. 1. K is the directed union of geometrically irreducible k-subalgebras of finite type. 2. For every geometrically irreducible k-algebra A of finite type there is N such that for every finite extension k'/k of degree n ≥ N there is a k-algebra map A → k'. 3. If X is a quasi-separated algebraic space over k and X_K is a scheme, then X is a scheme.

theorem finiteField_remark (k K : Type u) [Field k] [Finite k] [Field K] [Algebra k K]
    (hK : Algebra.IsGeometricallyIrreducible k K) :
    (∃ (ι : Type u) (A : ι → Subalgebra k K), Directed (· ≤ ·) A ∧ (⨆ i, A i) = ⊤ ∧
      ∀ i, Algebra.FiniteType k (A i) ∧ Algebra.IsGeometricallyIrreducible k (A i)) ∧
    (∀ (A : Type u) [CommRing A] [Algebra k A] [Algebra.FiniteType k A],
      Algebra.IsGeometricallyIrreducible k A →
      ∃ N : ℕ, ∀ (k' : Type u) [Field k'] [Algebra k k'] [FiniteDimensional k k'],
        N ≤ finrank k k' → Nonempty (A →ₐ[k] k')) ∧
    (∀ (B : BigFppfSite.{u}) (hk : B.Contains (Spec (.of k))) (hK' : B.Contains (Spec (.of K)))
      (F : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u),
      IsAlgebraicSpace B (Spec (.of k)) hk F →
      IsQuasiSeparatedOver B (Spec (.of k)) hk F →
      ((OverShriek.relocalizeRestrict
        (ObjectProperty.homMk (Spec.map (CommRingCat.ofHom (algebraMap k K))) :
          B.obj hK' ⟶ B.obj hk)).obj F).IsRepresentable →
      F.IsRepresentable)

Tag 0B88, a lemma

Tag 0B88 in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_isAlgClosure_finite_rationalPoints_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OverFields/DecentFiniteTypeScheme.lean, line 916. The attribute's comment: “all three hypotheses of the source, none dropped, weakened or added”.

Stacks 0B88. Let k be a field with algebraic closure K = k̄ and let X be an algebraic space over k. Assume

1. X is decent and locally of finite type over k,
2. X_{k̄} is a scheme, and
3. any finite set of k̄-rational points of X_{k̄} is contained in an affine.

Then X is a scheme.

All three source hypotheses are present and none is weakened: hdecent together with hfinite is hypothesis (1), hbase is hypothesis (2), and haffine is hypothesis (3).

X_{k̄} is the restriction of X to the big fppf site over Spec k̄ along the morphism g : Spec k̄ ⟶ Spec k of the site, a k̄-rational point of it is a section over the terminal object Spec k̄ of that site, and an affine open is presented by an open immersion out of an affine object, as in the library's form of Tag 0BA1. The structure morphism of X over Spec k is given explicitly as f, the base Spec k being terminal in its own big fppf site.

Being decent and locally of finite type over a field, |X| is a Jacobson space (Tag 0BA6 and Tag 0BA3), so it is enough to put every closed point of |X| in the schematic locus of Tag 03JH, and then Tag 03KE in the case (θ) finishes. A closed point is represented by a closed immersion Spec l ⟶ X (Tag 0AHB) with l/k finite (Tag 03XG and the Hilbert Nullstellensatz), so Spec l ×_X X_{k̄} is a finite scheme over an algebraically closed field and hypothesis (3) gives an affine open of X_{k̄} through which it factors. The projection π : X_{k̄} ⟶ X is a base change of the affine, flat, surjective morphism Spec k̄ ⟶ Spec k, hence universally closed and quasi-compact, and closedness converts the fibrewise containment into a quasi-compact open neighbourhood N of the point whose base change to k̄ is quasi-affine over Spec k̄. Tag 0423 descends quasi-affineness along that fpqc covering and Tag 03WM makes N a scheme, so the point is in the schematic locus.

theorem isRepresentable_of_isAlgClosure_finite_rationalPoints_isAffine
    (k K : Type u) [Field k] [Field K] [Algebra k K] [IsAlgClosure k K]
    (B : BigFppfSite.{u})
    (hk : B.Contains (Spec (.of k))) (hK : B.Contains (Spec (.of K)))
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (hdecent : IsDecentSpace B (Spec (.of k)) hk X)
    (f : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hk))))
    (hfinite : IsLocallyOfFiniteType B (Spec (.of k)) hk f)
    (hbase : ((OverShriek.relocalizeRestrict
      (ObjectProperty.homMk (Spec.map (CommRingCat.ofHom (algebraMap k K))) :
        B.obj hK ⟶ B.obj hk)).obj X).IsRepresentable)
    (haffine :
      let Xbase := (OverShriek.relocalizeRestrict
        (ObjectProperty.homMk (Spec.map (CommRingCat.ofHom (algebraMap k K))) :
          B.obj hK ⟶ B.obj hk)).obj X
      ∀ s : Finset (Xbase.obj (op (Over.mk (𝟙 (B.obj hK))))),
        ∃ (U : BigFppfOver B (Spec (.of K)) hK) (i : yoneda.obj U ⟶ Xbase),
          IsAffine ((BigFppfOver.toScheme B (Spec (.of K)) hK).obj U) ∧
          IsOpenImmersion B (Spec (.of K)) hK i ∧
          ∀ x ∈ s, x ∈ Set.range (i.app (op (Over.mk (𝟙 (B.obj hK)))))) :
    X.IsRepresentable

Tag 06S0, a lemma

Tag 06S0 in the Stacks Project.

AlgebraicGeometry.Space.tfae_isLocallyQuasiFinite_to_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocallyQuasiFiniteOverFieldTfae.lean, line 84.

Stacks 06S0. Let k be a field and X an algebraic space over k, presented as an algebraic space over S with a morphism g : X ⟶ h_K to an object K of the site whose underlying scheme is Spec k. The following are equivalent: 1. X is locally quasi-finite over k; 2. X is locally of finite type over k and has dimension 0; 3. X is a scheme and is locally quasi-finite over k; 4. X is a scheme, is locally of finite type over k and has dimension 0; 5. X is a disjoint union of spectra of Artinian local k-algebras A with dim_k A < ∞, over k.

"Dimension 0" is read as ≤ 0, since the empty space has dimension ⊥ and satisfies (1).

theorem tfae_isLocallyQuasiFinite_to_field {k : Type u} [Field k]
    {K : BigFppfOver B S hS} (e : (BigFppfOver.toScheme B S hS).obj K ≅ Spec (.of k))
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (g : X ⟶ yoneda.obj K) :
    [IsLocallyQuasiFinite B S hS g,
      IsLocallyOfFiniteType B S hS g ∧ dimension B S hS X hX ≤ 0,
      X.IsRepresentable ∧ IsLocallyQuasiFinite B S hS g,
      X.IsRepresentable ∧ IsLocallyOfFiniteType B S hS g ∧ dimension B S hS X hX ≤ 0,
      ∃ (Y : BigFppfOver B S hS) (eX : yoneda.obj Y ≅ X) (I : Type u) (A : I → Type u)
        (_ : ∀ i, CommRing (A i)) (_ : ∀ i, Algebra k (A i)) (_ : ∀ i, IsLocalRing (A i))
        (_ : ∀ i, IsArtinianRing (A i)) (_ : ∀ i, Module.Finite k (A i))
        (eY : (BigFppfOver.toScheme B S hS).obj Y ≅ ∐ fun i ↦ Spec (.of (A i))),
        eY.hom ≫ Sigma.desc (fun i ↦ Spec.map (CommRingCat.ofHom (algebraMap k (A i)))) =
          (BigFppfOver.toScheme B S hS).map (yoneda.preimage (eX.hom ≫ g)) ≫ e.hom].TFAE

Tag 06S1, a lemma

Tag 06S1 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyQuasiFinite_of_mono_of_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MonoLocallyQuasiFiniteOverField.lean, line 68.

Stacks 06S1. Let k be a field and f : X ⟶ Y a monomorphism of algebraic spaces over k. If Y is locally quasi-finite over k, so is X.

theorem isLocallyQuasiFinite_of_mono_of_isLocallyQuasiFinite {k : Type u} [Field k]
    (e : S ≅ Spec (.of k)) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) [Mono f]
    (hYk : IsLocallyQuasiFinite B S hS ((isTerminal_yoneda_obj_base B S hS).from Y)) :
    IsLocallyQuasiFinite B S hS ((isTerminal_yoneda_obj_base B S hS).from X)

Sources

• Section 72.10, Tag 0B82
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isRepresentable_of_isPurelyInseparable_of_isRepresentable · AlgebraicGeometry.Space.exists_finite_separable_isRepresentable_relocalizeRestrict · AlgebraicGeometry.Space.isRepresentable_relocalizeRestrict_algebraicClosure · AlgebraicGeometry.Space.isAlgebraicSpace_extensionBaseChange · AlgebraicGeometry.Space.isFreeOnNonemptyPoints_extensionBaseChange · AlgebraicGeometry.Space.isIso_extensionBaseChangeQuotientLift · AlgebraicGeometry.Space.mem_schematicLocus_actionQuotient_iff · AlgebraicGeometry.Space.mem_schematicLocus_orbitQuotient_iff

Section72.11 Geometrically reduced algebraic spaces#

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

Tag 0DMQ, a definition

Tag 0DMQ in the Stacks Project.

AlgebraicGeometry.Space.IsGeometricallyReducedAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyReduced.lean, line 204. The attribute's comment: “part (1): at a point”.

Stacks 0DMQ, part (1). An algebraic space X over a field k is geometrically reduced at a point x of X when the étale local ring of X at every geometric point above x is geometrically reduced as a k-algebra.

abbrev IsGeometricallyReducedAt (k : Type u) [Field k] (B : BigFppfSite.{u})
    (hk : B.Contains (Spec (.of k)))
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (x : points B (Spec (.of k)) hk X) : Prop

AlgebraicGeometry.Space.IsGeometricallyReduced, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyReduced.lean, line 217. The attribute's comment: “part (2): over the field”.

Stacks 0DMQ, part (2). An algebraic space over a field k is geometrically reduced when it is geometrically reduced at every one of its points.

abbrev IsGeometricallyReduced (k : Type u) [Field k] (B : BigFppfSite.{u})
    (hk : B.Contains (Spec (.of k)))
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) : Prop

Tag 0DMR, a lemma

Tag 0DMR in the Stacks Project.

AlgebraicGeometry.Space.isGeometricallyReducedAt_iff_exists_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyReduced.lean, line 510. The attribute's comment: “conditions (1) and (2): some étale neighbourhood”.

Stacks 0DMR, conditions (1) and (2). An algebraic space over a field k is geometrically reduced at a point x exactly when some étale neighbourhood (U, u) → (X, x) with U a scheme is geometrically reduced at u.

theorem isGeometricallyReducedAt_iff_exists_etaleChart
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) (x : points B (Spec (.of k)) hk X) :
    IsGeometricallyReducedAt k B hk X hX x ↔
      ∃ (U : BigFppfOver B (Spec (.of k)) hk) (a : yoneda.obj U ⟶ X),
        IsEtale B (Spec (.of k)) hk a ∧
          ∃ p : FieldValuedPoint B (Spec (.of k)) hk (yoneda.obj U),
            pointsMap B (Spec (.of k)) hk (yoneda.obj U) a
                (p.class B (Spec (.of k)) hk (yoneda.obj U)) = x ∧
              _root_.AlgebraicGeometry.IsGeometricallyReducedAt (B.inclusion.map U.hom)
                (schemePoint B (Spec (.of k)) hk U p)

AlgebraicGeometry.Space.isGeometricallyReducedAt_iff_forall_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyReduced.lean, line 533. The attribute's comment: “conditions (1) and (3): every étale neighbourhood”.

Stacks 0DMR, conditions (1) and (3). An algebraic space over a field k is geometrically reduced at a point x exactly when every étale neighbourhood (U, u) → (X, x) with U a scheme is geometrically reduced at u.

theorem isGeometricallyReducedAt_iff_forall_etaleChart
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) (x : points B (Spec (.of k)) hk X) :
    IsGeometricallyReducedAt k B hk X hX x ↔
      ∀ (U : BigFppfOver B (Spec (.of k)) hk) (a : yoneda.obj U ⟶ X),
        IsEtale B (Spec (.of k)) hk a →
          ∀ p : FieldValuedPoint B (Spec (.of k)) hk (yoneda.obj U),
            pointsMap B (Spec (.of k)) hk (yoneda.obj U) a
                (p.class B (Spec (.of k)) hk (yoneda.obj U)) = x →
              _root_.AlgebraicGeometry.IsGeometricallyReducedAt (B.inclusion.map U.hom)
                (schemePoint B (Spec (.of k)) hk U p)

Tag 0DMS, a lemma

Tag 0DMS in the Stacks Project.

AlgebraicGeometry.Space.isGeometricallyReduced_iff_exists_surjective_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyReduced.lean, line 579. The attribute's comment: “conditions (1) and (2): some surjective étale chart”.

Stacks 0DMS, conditions (1) and (2). An algebraic space over a field k is geometrically reduced exactly when some surjective étale morphism U → X with U a scheme has U geometrically reduced over k.

theorem isGeometricallyReduced_iff_exists_surjective_etaleChart
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) :
    IsGeometricallyReduced k B hk X hX ↔
      ∃ (U : BigFppfOver B (Spec (.of k)) hk) (a : yoneda.obj U ⟶ X),
        IsSurjective B (Spec (.of k)) hk a ∧ IsEtale B (Spec (.of k)) hk a ∧
          _root_.AlgebraicGeometry.GeometricallyReduced (B.inclusion.map U.hom)

AlgebraicGeometry.Space.isGeometricallyReduced_iff_forall_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyReduced.lean, line 600. The attribute's comment: “conditions (1) and (3): every étale chart”.

Stacks 0DMS, conditions (1) and (3). An algebraic space over a field k is geometrically reduced exactly when every étale morphism U → X with U a scheme has U geometrically reduced over k.

theorem isGeometricallyReduced_iff_forall_etaleChart
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) :
    IsGeometricallyReduced k B hk X hX ↔
      ∀ (U : BigFppfOver B (Spec (.of k)) hk) (a : yoneda.obj U ⟶ X),
        IsEtale B (Spec (.of k)) hk a →
          _root_.AlgebraicGeometry.GeometricallyReduced (B.inclusion.map U.hom)

Tag 0E02, a lemma

Tag 0E02 in the Stacks Project.

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

Stacks 0E02, part (2). Over a perfect field a reduced algebraic space is geometrically reduced: by Stacks 0DMS it suffices that every étale scheme chart is geometrically reduced, which over a perfect field is Stacks 020I.

theorem isGeometricallyReduced_of_isReduced [PerfectField k]
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (hred : HasEtaleLocalProperty B (Spec (.of k)) hk X (fun Y : Scheme.{u} => IsReduced Y)) :
    IsGeometricallyReduced k B hk X hX

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

Stacks 0E02, part (1). Let X be an algebraic space over a perfect field k, for example a field of characteristic zero. If the étale local ring 𝒪_{X, x̄} at a geometric point x̄ above x is reduced, then X is geometrically reduced at x.

theorem isGeometricallyReducedAt_of_isReduced_etaleLocalRing
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (x : points B (Spec (.of k)) hk X)
    (xbar : GeometricPoint B (Spec (.of k)) hk X) (hxbar : xbar.LiesOver x)
    (hred : _root_.IsReduced (etaleLocalRing B (Spec (.of k)) hk X xbar)) :
    IsGeometricallyReducedAt k B hk X hX x

Tag 0E03, a lemma

Tag 0E03 in the Stacks Project.

AlgebraicGeometry.Space.isGeometricallyReduced_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyReducedFieldExtension.lean, line 83.

Stacks 0E03. Let k be a field of exponential characteristic p and let X be an algebraic space over k. Then X is geometrically reduced over k if and only if X_{k'} is reduced for every field extension k'/k, if and only if X_{k'} is reduced for every finite purely inseparable extension k'/k, if and only if each of X_{k^{1/p}}, X_{k^{perf}} and X_{k̄} is reduced.

theorem isGeometricallyReduced_tfae (k : Type u) [Field k] (p : ℕ) [ExpChar k p]
    (B : BigFppfSite.{u}) (hk : B.Contains (Spec (.of k)))
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (kperf : Type u) [Field kperf] [Algebra k kperf] [ExpChar kperf p] [PerfectRing kperf p]
    [IsPerfectClosure (algebraMap k kperf) p]
    (kbar : Type u) [Field kbar] [Algebra k kbar] [IsAlgClosure k kbar] :
    let isReducedBaseChange := fun (k' : Type u) [Field k'] [Algebra k k'] ↦
      ∀ (U : BigFppfOver B (Spec (.of k)) hk) (a : yoneda.obj U ⟶ X),
        IsEtale B (Spec (.of k)) hk a →
          IsReduced (pullback (B.inclusion.map U.hom)
            (Spec.map (CommRingCat.ofHom (algebraMap k k'))))
    List.TFAE
      [ IsGeometricallyReduced k B hk X hX,
        ∀ (k' : Type u) [Field k'] [Algebra k k'], isReducedBaseChange k',
        ∀ (k' : Type u) [Field k'] [Algebra k k'] [FiniteDimensional k k']
          [IsPurelyInseparable k k'], isReducedBaseChange k',
        isReducedBaseChange (AdjoinPthRoots k),
        isReducedBaseChange kperf,
        isReducedBaseChange kbar ]

Tag 0E04, a lemma

Tag 0E04 in the Stacks Project.

AlgebraicGeometry.Space.isGeometricallyReducedAt_relocalizeRestrict_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyReducedFieldExtension.lean, line 342. The attribute's comment: “pointwise equivalence”.

Stacks 0E04, pointwise statement. An algebraic space over a field k is geometrically reduced at a point x exactly when its base change to a field extension k'/k is geometrically reduced at any point x' lying over x.

theorem isGeometricallyReducedAt_relocalizeRestrict_iff
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (x : points B (Spec (.of k)) hk X)
    (x' : points B (Spec (.of k')) hk'
      ((OverShriek.relocalizeRestrict (fieldExtensionMap B k k' hk hk')).obj X))
    (hx : pointsOfRelocalizeRestrict B (Spec (.of k')) (Spec (.of k)) hk' hk
      (fieldExtensionMap B k k' hk hk') X x' = x) :
    IsGeometricallyReducedAt k B hk X hX x ↔
      IsGeometricallyReducedAt k' B hk'
        ((OverShriek.relocalizeRestrict (fieldExtensionMap B k k' hk hk')).obj X)
        (isAlgebraicSpace_relocalizeRestrict B (Spec (.of k')) (Spec (.of k)) hk' hk
          (fieldExtensionMap B k k' hk hk') X hX) x'

AlgebraicGeometry.Space.isGeometricallyReduced_relocalizeRestrict_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyReducedFieldExtension.lean, line 388. The attribute's comment: “global equivalence”.

Stacks 0E04, global statement. An algebraic space over a field k is geometrically reduced over k exactly when its base change to a field extension k'/k is geometrically reduced over k'.

theorem isGeometricallyReduced_relocalizeRestrict_iff
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) :
    IsGeometricallyReduced k B hk X hX ↔
      IsGeometricallyReduced k' B hk'
        ((OverShriek.relocalizeRestrict (fieldExtensionMap B k k' hk hk')).obj X)
        (isAlgebraicSpace_relocalizeRestrict B (Spec (.of k')) (Spec (.of k)) hk' hk
          (fieldExtensionMap B k k' hk hk') X hX)

Tag 0E05, a lemma

Tag 0E05 in the Stacks Project.

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

Stacks 0E05, part (1). Let f : X ⟶ Y be a morphism of algebraic spaces over a field k and let x be a point of X with image y. If f is étale at x, then X is geometrically reduced at x if and only if Y is geometrically reduced at y.

theorem isGeometricallyReducedAt_iff_of_isEtaleAt
    {X Y : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (hY : IsAlgebraicSpace B (Spec (.of k)) hk Y)
    (f : X ⟶ Y) (x : points B (Spec (.of k)) hk X)
    (hf : IsEtaleAt B (Spec (.of k)) hk f x) :
    IsGeometricallyReducedAt k B hk X hX x ↔
      IsGeometricallyReducedAt k B hk Y hY (pointsMap B (Spec (.of k)) hk X f x)

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

Stacks 0E05, part (2). Let f : X ⟶ Y be a surjective étale morphism of algebraic spaces over a field k. Then X is geometrically reduced if and only if Y is.

theorem isGeometricallyReduced_iff_of_surjective_isEtale
    {X Y : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (hY : IsAlgebraicSpace B (Spec (.of k)) hk Y)
    (f : X ⟶ Y) (hf : IsEtale B (Spec (.of k)) hk f)
    (hs : IsSurjective B (Spec (.of k)) hk f) :
    IsGeometricallyReduced k B hk X hX ↔ IsGeometricallyReduced k B hk Y hY

Sources

• Section 72.11, Tag 0DMP
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsGeometricallyReducedAt · AlgebraicGeometry.Space.IsGeometricallyReduced · AlgebraicGeometry.Space.isGeometricallyReducedAt_iff_exists_etaleChart · AlgebraicGeometry.Space.isGeometricallyReducedAt_iff_forall_etaleChart · AlgebraicGeometry.Space.isGeometricallyReduced_iff_exists_surjective_etaleChart · AlgebraicGeometry.Space.isGeometricallyReduced_iff_forall_etaleChart · AlgebraicGeometry.Space.isGeometricallyReduced_of_isReduced · AlgebraicGeometry.Space.isGeometricallyReducedAt_of_isReduced_etaleLocalRing

Section72.12 Geometrically connected algebraic spaces#

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

Tag 0A0Z, a definition

Tag 0A0Z in the Stacks Project.

AlgebraicGeometry.Space.IsGeometricallyConnected, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyConnected.lean, line 492.

Stacks 0A0Z. A presheaf on the big fppf site over a field k — in particular an algebraic space over k — is geometrically connected when for every field extension K/k whose spectrum lies in the chosen big fppf site the base change X_K has a connected space of points.

def IsGeometricallyConnected (B : BigFppfSite.{u}) (k : Type u) [Field k]
    (hk : B.Contains (Spec (.of k)))
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u) : Prop

Tag 0A10, a lemma

Tag 0A10 in the Stacks Project.

AlgebraicGeometry.Space.isGeometricallyConnected_iff_relocalizeRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyConnected.lean, line 797.

Stacks 0A10. A presheaf on the big fppf site over a field k — in particular an algebraic space over k — is geometrically connected over k if and only if its base change to a field extension k' of k is geometrically connected over k'.

theorem isGeometricallyConnected_iff_relocalizeRestrict (B : BigFppfSite.{u})
    (k k' : Type u) [Field k] [Field k'] [Algebra k k']
    (hk : B.Contains (Spec (.of k))) (hk' : B.Contains (Spec (.of k')))
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) :
    IsGeometricallyConnected B k hk X ↔
      IsGeometricallyConnected B k' hk'
        ((OverShriek.relocalizeRestrict (fieldExtensionMap B k k' hk hk')).obj X)

Tag 0A11, a lemma

Tag 0A11 in the Stacks Project.

AlgebraicGeometry.Space.bijective_connectedComponents_pullback_of_isGeometricallyConnected, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyConnected.lean, line 1005.

Stacks 0A11. Let k be a field, let X and Y be algebraic spaces over k and assume X is geometrically connected over k. The projection X ×_k Y ⟶ Y induces a bijection between the sets of connected components of the two point spaces.

The projection is open on points because X ⟶ Spec k is universally open (Stacks 06DN), and its fibre over the point represented by a field-valued point Spec K ⟶ Y is the image of |X_K ×_k Spec K|; that fibre product is the base change X_K of X to K viewed again over k, whose point space is homeomorphic to |X_K| and so is connected. Stacks 0378 then gives the bijection.

theorem bijective_connectedComponents_pullback_of_isGeometricallyConnected
    {X Y : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (hY : IsAlgebraicSpace B (Spec (.of k)) hk Y)
    (hXconn : IsGeometricallyConnected B k hk X)
    (f : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hk))))
    (g : Y ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hk)))) :
    Function.Bijective
      (continuous_pointsMap B (Spec (.of k)) hk
        (pullback.snd f g)).connectedComponentsMap

Tag 0A12, a lemma

Tag 0A12 in the Stacks Project.

AlgebraicGeometry.Space.bijective_connectedComponents_relocalizeRestrict_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyConnected.lean, line 1188. The attribute's comment: “bijection on connected components”. References: EGA IV (4.4.6), “more general”.

Stacks 0A12, the bijection on connected components. Let k be a separably closed field, let K/k be a field extension whose spectrum lies in the chosen big fppf site and let X be an algebraic space over k. The map |X_K| → |X| induced by the base change is a bijection between the sets of connected components.

Viewed again over k, the base change X_K is the product Spec K ×_k X (CategoryTheory.OverShriek.isPullback_relocalizeRestrictCounit), and Spec K is geometrically connected over k, so Stacks 0A11 applies to the projection to X.

theorem bijective_connectedComponents_relocalizeRestrict_of_isSepClosed [IsSepClosed k]
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) :
    Function.Bijective
      (continuous_pointsOfRelocalizeRestrict B (Spec (.of K)) (Spec (.of k)) hK hk
        (fieldExtensionMap B k K hk hK) X
        (isAlgebraicSpace_relocalizeRestrict B (Spec (.of K)) (Spec (.of k)) hK hk
          (fieldExtensionMap B k K hk hK) X hX)).connectedComponentsMap

AlgebraicGeometry.Space.isGeometricallyConnected_iff_connectedSpace_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyConnected.lean, line 1259. The attribute's comment: “geometric connectedness”.

Stacks 0A12, geometric connectedness. Over a separably closed field an algebraic space is geometrically connected exactly when its space of points is connected.

theorem isGeometricallyConnected_iff_connectedSpace_of_isSepClosed [IsSepClosed k]
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) :
    IsGeometricallyConnected B k hk X ↔ ConnectedSpace (points B (Spec (.of k)) hk X)

Tag 0A13, a lemma

Tag 0A13 in the Stacks Project.

AlgebraicGeometry.Space.isGeometricallyConnected_iff_connectedSpace_sepClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyConnected.lean, line 1291.

Stacks 0A13. Let k be a field, let K be a separable algebraic closure of k whose spectrum lies in the chosen big fppf site and let X be an algebraic space over k. Then X is geometrically connected over k if and only if the base change X_K has a connected space of points.

Geometric connectedness over k is geometric connectedness of X_K over K by Stacks 0A10, and over the separably closed field K that is connectedness by Stacks 0A12.

theorem isGeometricallyConnected_iff_connectedSpace_sepClosure (B : BigFppfSite.{u})
    (k K : Type u) [Field k] [Field K] [Algebra k K] [IsSepClosure k K]
    (hk : B.Contains (Spec (.of k))) (hK : B.Contains (Spec (.of K)))
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) :
    IsGeometricallyConnected B k hk X ↔
      ConnectedSpace (points B (Spec (.of K)) hK
        ((OverShriek.relocalizeRestrict (fieldExtensionMap B k K hk hK)).obj X))

Tag 0A14, an equation

Tag 0A14 in the Stacks Project.

AlgebraicGeometry.Space.galoisActionOnBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyConnected.lean, line 917. The attribute's comment: “the action”.

Stacks 0A14, the action. The canonical action of the opposite group of k-algebra automorphisms of K on the base change X_K, viewed again as a presheaf over k. For a Galois extension K/k this is the Galois action on X_{\overline{k}}.

The action is over k, not over K: an automorphism changes only the K-coordinate of a section.

noncomputable def galoisActionOnBaseChange :
    Action ((BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u) (MulOpposite (K ≃ₐ[k] K))

AlgebraicGeometry.Space.galoisActionOnBaseChange_ρ_app_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyConnected.lean, line 948. The attribute's comment: “the action on the K-coordinate of a section”.

Stacks 0A14, the action on the K-coordinate. An automorphism σ acts on a section of X_K over a k-scheme by composing its morphism to Spec K with the automorphism of Spec K induced by σ.

theorem galoisActionOnBaseChange_ρ_app_fst (σ : MulOpposite (K ≃ₐ[k] K))
    (W : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ)
    (x : ((OverShriek.relocalizePresheafFunctor (fieldExtensionMap B k K hk hK)).obj
      ((OverShriek.relocalizeRestrict (fieldExtensionMap B k K hk hK)).obj X)).obj W) :
    (((galoisActionOnBaseChange B k K hk hK X).ρ σ).asHom.app W x).val.1 =
      x.val.1 ≫ siteMapAlgAut B k K hK σ.unop

AlgebraicGeometry.Space.galoisActionOnBaseChange_ρ_app_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyConnected.lean, line 960. The attribute's comment: “the action on the section”.

Stacks 0A14, the action on the section. An automorphism leaves the section of X itself untouched. The equality is heterogeneous because the type of the section is indexed by the morphism to Spec K, which the action does change.

theorem galoisActionOnBaseChange_ρ_app_snd (σ : MulOpposite (K ≃ₐ[k] K))
    (W : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ)
    (x : ((OverShriek.relocalizePresheafFunctor (fieldExtensionMap B k K hk hK)).obj
      ((OverShriek.relocalizeRestrict (fieldExtensionMap B k K hk hK)).obj X)).obj W) :
    HEq (((galoisActionOnBaseChange B k K hk hK X).ρ σ).asHom.app W x).val.2 x.val.2

Tag 0A15, a lemma

Tag 0A15 in the Stacks Project.

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

Let X be an algebraic space over a field k and let K/k be an algebraic field extension. A quasi-compact open subspace of the base change of X to K is the base change of a quasi-compact open subspace of the base change of X to a finite subextension of K/k.

theorem exists_finite_subextension_descending_isQuasiCompact_open (B : BigFppfSite.{u})
    (k K : Type u) [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K]
    (hk : B.Contains (Spec (.of k))) (hK : B.Contains (Spec (.of K)))
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (V : Subfunctor ((OverShriek.relocalizeRestrict (fieldExtensionMap B k K hk hK)).obj X))
    (hV : IsOpenSubspace B (Spec (.of K)) hK V)
    (hVqc : IsQuasiCompactSpace B (Spec (.of K)) hK V.toFunctor) :
    ∃ (E : IntermediateField k K) (_ : FiniteDimensional k E)
      (hE : B.Contains (Spec (.of E)))
      (V' : Subfunctor
        ((OverShriek.relocalizeRestrict (fieldExtensionMap B k E hk hE)).obj X)),
      IsOpenSubspace B (Spec (.of E)) hE V' ∧
        IsQuasiCompactSpace B (Spec (.of E)) hE V'.toFunctor ∧
        Subfunctor.preimage V
            (eqToHom (relocalizeRestrict_fieldExtensionMap_comp B k E K hk hE hK X)) =
          OverShriek.relocalizeRestrictSubfunctor (fieldExtensionMap B E K hE hK) V'

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

Let X be an algebraic space over a field k and let K/k be a Galois extension. A quasi-compact open subspace of the base change of X to K is fixed by an open subgroup of Gal(K/k).

theorem exists_open_subgroup_fixing_isQuasiCompact_open [IsGalois k K]
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (V : Subfunctor ((OverShriek.relocalizeRestrict (fieldExtensionMap B k K hk hK)).obj X))
    (hV : IsOpenSubspace B (Spec (.of K)) hK V)
    (hVqc : IsQuasiCompactSpace B (Spec (.of K)) hK V.toFunctor) :
    ∃ H : Subgroup Gal(K/k), IsOpen (H : Set Gal(K/k)) ∧
      ∀ σ : Gal(K/k), σ ∈ H →
        Subfunctor.preimage (galoisOpenSubfunctor B k K hk hK X V)
            ((galoisActionOnBaseChange B k K hk hK X).ρ (MulOpposite.op σ)).asHom =
          galoisOpenSubfunctor B k K hk hK X V

Tag 0A16, a lemma

Tag 0A16 in the Stacks Project.

AlgebraicGeometry.Space.exists_closed_subset_with_preimage_eq_of_galois_invariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GaloisInvariantClosedSubspace.lean, line 721.

Stacks 0A16. Let K/k be a Galois extension whose spectra lie in the chosen big fppf site, and let X be an algebraic space over k. A closed subset of the points of the base change X_K which is invariant under the action of every k-algebra automorphism of K is the inverse image of a closed subset of the points of X.

theorem exists_closed_subset_with_preimage_eq_of_galois_invariant (B : BigFppfSite.{u})
    (k K : Type u) [Field k] [Field K] [Algebra k K] [IsGalois k K]
    (hk : B.Contains (Spec (.of k))) (hK : B.Contains (Spec (.of K)))
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X)
    (Tbar : Set (points B (Spec (.of K)) hK
      ((OverShriek.relocalizeRestrict (fieldExtensionMap B k K hk hK)).obj X)))
    (hTbar : @IsClosed _ (pointTopology B (Spec (.of K)) hK _) Tbar)
    (hstable : ∀ σ : K ≃ₐ[k] K, galoisPointsAction B k K hk hK X σ ⁻¹' Tbar = Tbar) :
    ∃ T : Set (points B (Spec (.of k)) hk X),
      @IsClosed _ (pointTopology B (Spec (.of k)) hk X) T ∧
      pointsOfRelocalizeRestrict B (Spec (.of K)) (Spec (.of k)) hK hk
          (fieldExtensionMap B k K hk hK) X ⁻¹' T = Tbar

Tag 0A17, a lemma

Tag 0A17 in the Stacks Project.

AlgebraicGeometry.Space.isGeometricallyConnected_iff_connectedSpace_finite_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyConnectedFiniteSeparable.lean, line 378. References: EGA IV (8.4.5); EGA IV (4.5.18), “more general”.

Let k be a field and let X be an algebraic space over k. Then X is geometrically connected over k if and only if the base change X_{k'} has a connected space of points for every finite separable field extension k'/k whose spectrum lies in the chosen big fppf site.

theorem isGeometricallyConnected_iff_connectedSpace_finite_separable (B : BigFppfSite.{u})
    (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
    (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of k)) hk X) :
    IsGeometricallyConnected B k hk X ↔
      ∀ (K : Type u) [Field K] [Algebra k K] [FiniteDimensional k K]
        [Algebra.IsSeparable k K] (hK : B.Contains (Spec (.of K))),
        ConnectedSpace (points B (Spec (.of K)) hK
          ((OverShriek.relocalizeRestrict (fieldExtensionMap B k K hk hK)).obj X))

Sources

• Section 72.12, Tag 0A0Y
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsGeometricallyConnected · AlgebraicGeometry.Space.isGeometricallyConnected_iff_relocalizeRestrict · AlgebraicGeometry.Space.bijective_connectedComponents_pullback_of_isGeometricallyConnected · AlgebraicGeometry.Space.bijective_connectedComponents_relocalizeRestrict_of_isSepClosed · AlgebraicGeometry.Space.isGeometricallyConnected_iff_connectedSpace_of_isSepClosed · AlgebraicGeometry.Space.isGeometricallyConnected_iff_connectedSpace_sepClosure · AlgebraicGeometry.Space.galoisActionOnBaseChange · AlgebraicGeometry.Space.galoisActionOnBaseChange_ρ_app_fst

Section72.13 Geometrically irreducible algebraic spaces#

Section 72.13 of the Stacks Project, Tag 0DMT. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DMU, a definition

Tag 0DMU in the Stacks Project.

AlgebraicGeometry.Space.IsGeometricallyIrreducible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricallyIntegral.lean, line 94.

Stacks 0DMU. An algebraic space over a field k is geometrically irreducible when the space of points of its base change to every field extension of k is irreducible — in particular nonempty.

def IsGeometricallyIrreducible (X : (BigFppfOver B (Spec (.of k)) hk)ᵒᵖ ⥤ Type u) : Prop

Sources

• Section 72.13, Tag 0DMT
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsGeometricallyIrreducible

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.