68.18 Points of fibres to 68.25 Catenary algebraic spaces

Section68.18 Points of fibres#

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

Tag 0AC1, an equation

Tag 0AC1 in the Stacks Project.

AlgebraicGeometry.Space.PointsFibresDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibres.lean, line 38.

A cartesian diagram of algebraic spaces W → Z, W → X, X → Y and Z → Y over S.

structure PointsFibresDiagram (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)

Tag 0AC2, an equation

Tag 0AC2 in the Stacks Project.

AlgebraicGeometry.Space.fibrePoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibres.lean, line 69.

The points of W mapping to the specified points x of X and z of Z, which have the same image in Y, in a cartesian diagram.

def fibrePoints {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    (D : PointsFibresDiagram B S hS) (x : points B S hS D.X) (z : points B S hS D.Z)
    (_h : pointsMap B S hS D.X D.f x = pointsMap B S hS D.Z D.g z) :
    Set (points B S hS D.W)

Tag 0AC3, an example

Tag 0AC3 in the Stacks Project.

AlgebraicGeometry.Space.fibreSpectrumEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresSchemes.lean, line 353. The attribute's comment: “spectrum of the fibre”.

In a cartesian square of Tag 0AC1 whose three non-pullback corners are schemes, the set of Tag 0AC2 attached to two points x and z with a common image y is in bijection with the spectrum of κ(x) ⊗_{κ(y)} κ(z).

noncomputable def fibreSpectrumEquiv
    (h : pointsMap B S hS D.X D.f x = pointsMap B S hS D.Z D.g z) :
    (fibrePoints D x z h) ≃
      Spec (Scheme.Pullback.Triplet.mk' ((D.schemePointsPresentation R).eX x)
        ((D.schemePointsPresentation R).eZ z)
        (schemeF_eq_schemeG_of_pointsMap_eq R x z h)).tensor

AlgebraicGeometry.Space.fibreSpectrumEquiv_symm_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresSchemes.lean, line 377. The attribute's comment: “canonical correspondence”.

The inverse of AlgebraicGeometry.Space.fibreSpectrumEquiv is the canonical map AlgebraicGeometry.Scheme.Pullback.Triplet.SpecTensorTo, read through the point presentation.

theorem fibreSpectrumEquiv_symm_apply
    (h : pointsMap B S hS D.X D.f x = pointsMap B S hS D.Z D.g z)
    (p : Spec (Scheme.Pullback.Triplet.mk' ((D.schemePointsPresentation R).eX x)
      ((D.schemePointsPresentation R).eZ z)
      (schemeF_eq_schemeG_of_pointsMap_eq R x z h)).tensor) :
    (D.schemePointsPresentation R).eW ((fibreSpectrumEquiv R x z h).symm p).1 =
      (Scheme.Pullback.Triplet.mk' ((D.schemePointsPresentation R).eX x)
        ((D.schemePointsPresentation R).eZ z)
        (schemeF_eq_schemeG_of_pointsMap_eq R x z h)).SpecTensorTo p

AlgebraicGeometry.Space.finite_fibrePoints_of_finite_residueField_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresSchemes.lean, line 423. The attribute's comment: “finite left residue extension”.

The set of Tag 0AC2 is finite when the residue field extension κ(y) ⊂ κ(x) is finite.

theorem finite_fibrePoints_of_finite_residueField_left
    (h : pointsMap B S hS D.X D.f x = pointsMap B S hS D.Z D.g z)
    (hfin : letI := (R.schemeF.residueFieldMap ((D.schemePointsPresentation R).eX x)).hom.toAlgebra
      Module.Finite
        (R.schemeY.residueField (R.schemeF ((D.schemePointsPresentation R).eX x)))
        (R.schemeX.residueField ((D.schemePointsPresentation R).eX x))) :
    (fibrePoints D x z h).Finite

AlgebraicGeometry.Space.finite_fibrePoints_of_finite_residueField_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresSchemes.lean, line 440. The attribute's comment: “finite right residue extension”.

The set of Tag 0AC2 is finite when the residue field extension κ(y) ⊂ κ(z) is finite.

theorem finite_fibrePoints_of_finite_residueField_right
    (h : pointsMap B S hS D.X D.f x = pointsMap B S hS D.Z D.g z)
    (hfin : letI := (R.schemeG.residueFieldMap ((D.schemePointsPresentation R).eZ z)).hom.toAlgebra
      Module.Finite
        (R.schemeY.residueField (R.schemeG ((D.schemePointsPresentation R).eZ z)))
        (R.schemeZ.residueField ((D.schemePointsPresentation R).eZ z))) :
    (fibrePoints D x z h).Finite

AlgebraicGeometry.Space.finite_fibrePoints_of_quasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresSchemes.lean, line 457. The attribute's comment: “quasi-finite case”.

The set of Tag 0AC2 is finite whenever the lower horizontal morphism is quasi-finite at z.

theorem finite_fibrePoints_of_quasiFiniteAt
    (h : pointsMap B S hS D.X D.f x = pointsMap B S hS D.Z D.g z)
    (hg : quasiFiniteAt R.schemeG ((D.schemePointsPresentation R).eZ z)) :
    (fibrePoints D x z h).Finite

Tag 0AC4, an example

Tag 0AC4 in the Stacks Project.

AlgebraicGeometry.Space.exists_isPullback_twistedLineQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/TwistedLineFibrePoints.lean, line 228. The attribute's comment: “the square is cartesian, with W the affine line”.

Stacks 0AC4, the square. The projections of the affine line and of Spec K onto their quotients by the twisted actions and the inclusion of the constants form a cartesian square, so the fibre product W = X ×_Y Z of the example is the affine line Spec K[t] itself.

This is AlgebraicGeometry.Space.exists_isPullback_toQuotientSheaf_twistedLine transported along AlgebraicGeometry.Space.pointsYonedaIso, which identifies the restricted functor of points of an object of the site with the presheaf it represents; it is stated at the represented presheaves because those are the corners whose point sets AlgebraicGeometry.Space.twistedFibreSet is a subset of.

theorem exists_isPullback_twistedLineQuotient [CharZero K] (hσ : orderOf σ = 0) :
    ∃ f : actionQuotient (Multiplicative ℤ) B hS (twistedLineSite hS hL s)
        (twistedLineSiteAction hS hL s σ hs) ⟶
      actionQuotient (Multiplicative ℤ) B hS (twistedBaseSite hS hK s)
        (twistedBaseSiteAction hS hK s σ hs),
      IsPullback (twistedLineProjection hS hL s σ hs)
        (yoneda.map (twistedLineToBaseSite hS hK hL s)) f
        (twistedBaseProjection hS hK s σ hs)

AlgebraicGeometry.Space.twistedFibreEquivInt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/TwistedLineFibrePoints.lean, line 455. The attribute's comment: “the fibre of points is the integers”.

Stacks 0AC4, the fibre. The set F_{x,z} of Stacks 0AC2 for the square of Stacks 0AC4 is in bijection with ℤ: the points t = n of the affine line all have the same image in the quotient by the twisted translations and the same image in Spec K, they are pairwise distinct because the coordinate of t = n is n and K has characteristic zero, and every point of the fibre is one of them.

def twistedFibreEquivInt [CharZero K] : twistedFibreSet hS hK hL s σ hs ≃ ℤ

Tag 0AC5, a lemma

Tag 0AC5 in the Stacks Project.

AlgebraicGeometry.Space.surjOn_fibrePoints_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresBaseChange.lean, line 78.

Let D be a cartesian square of algebraic spaces, let t : Z' ⟶ D.Z be a morphism of algebraic spaces and let z' be a point of |Z'|. Then the map F_{x, z'} → F_{x, z} induced by r : W' ⟶ D.W is surjective, where z is the image of z' and W' is the fibre product D.W ×_{D.Z} Z'.

theorem surjOn_fibrePoints_baseChange (D : PointsFibresDiagram B S hS)
    {W' Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hW' : IsAlgebraicSpace B S hS W') (hZ' : IsAlgebraicSpace B S hS Z')
    {t : Z' ⟶ D.Z} {r : W' ⟶ D.W} {q' : W' ⟶ Z'} (sq : IsPullback r q' D.q t)
    (x : points B S hS D.X) (z' : points B S hS Z')
    (h : pointsMap B S hS D.X D.f x = pointsMap B S hS Z' (t ≫ D.g) z') :
    Set.SurjOn (pointsMap B S hS W' r)
      (fibrePoints (D.baseChange hW' hZ' sq) x z' h)
      (fibrePoints D x (pointsMap B S hS Z' t z')
        (by rw [h, pointsMap_comp_apply]))

Tag 0AC6, a lemma

Tag 0AC6 in the Stacks Project.

AlgebraicGeometry.Space.finite_fibrePoints_of_isFiniteType_of_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresQuasiFinite.lean, line 54.

Stacks 0AC6. In a cartesian square of algebraic spaces as in Stacks 0AC1, the set of points of the upper-left corner lying over prescribed points x and z of the upper-right and lower-left corners is finite as soon as the right vertical morphism is of finite type and quasi-finite at x.

theorem finite_fibrePoints_of_isFiniteType_of_isQuasiFiniteAt
    (D : PointsFibresDiagram B S hS) (x : points B S hS D.X) (z : points B S hS D.Z)
    (h : pointsMap B S hS D.X D.f x = pointsMap B S hS D.Z D.g z)
    (hf : IsFiniteType B S hS D.f) (hx : IsQuasiFiniteAt B S hS D.f x) :
    (fibrePoints D x z h).Finite

Tag 0AC7, a lemma

Tag 0AC7 in the Stacks Project.

AlgebraicGeometry.Space.finite_fibrePoints_of_mono_of_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresFiniteDecent.lean, line 359. The attribute's comment: “finite fibre over a monomorphic point”.

In a cartesian square of Tag 0AC1, the set of Tag 0AC2 attached to two points x of |X| and z of |Z| with common image y in |Y| is finite whenever y can be represented by a monomorphism from the spectrum of a field and the lower horizontal morphism g is quasi-finite at z.

theorem finite_fibrePoints_of_mono_of_isQuasiFiniteAt (D : PointsFibresDiagram B S hS)
    (x : points B S hS D.X) (z : points B S hS D.Z)
    (h : pointsMap B S hS D.X D.f x = pointsMap B S hS D.Z D.g z)
    (hy : HasMonomorphicFieldRepresentative B S hS D.Y (pointsMap B S hS D.X D.f x))
    (hqf : IsQuasiFiniteAt B S hS D.g z) :
    (fibrePoints D x z h).Finite

AlgebraicGeometry.Space.finite_fibrePoints_of_isDecentSpace_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresFiniteDecent.lean, line 410. The attribute's comment: “special case: decent lower-right corner and étale lower horizontal morphism”.

In a cartesian square of Tag 0AC1 whose lower-right corner is a decent algebraic space and whose lower horizontal morphism is étale, the set of Tag 0AC2 is finite.

theorem finite_fibrePoints_of_isDecentSpace_of_isEtale (D : PointsFibresDiagram B S hS)
    (x : points B S hS D.X) (z : points B S hS D.Z)
    (h : pointsMap B S hS D.X D.f x = pointsMap B S hS D.Z D.g z)
    (hY : IsDecentSpace B S hS D.Y) (hg : IsEtale B S hS D.g) :
    (fibrePoints D x z h).Finite

Tag 0AC8, a lemma

Tag 0AC8 in the Stacks Project.

AlgebraicGeometry.Space.isInducing_pointsMap_fibre_fieldMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FibreOverFieldPoint.lean, line 304. The attribute's comment: “the topology of the fibre”.

Stacks 0AC8, the topology of the fibre. Let f : X ⟶ Y be a morphism of algebraic spaces over S and let p be a field-valued point of Y whose presenting morphism Spec k ⟶ Y is a quasi-compact monomorphism. Then the map on points induced by the projection X ×_Y Spec k ⟶ X is topologically inducing.

theorem isInducing_pointsMap_fibre_fieldMorphism (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y)
    (hmono : Mono (fieldMorphism B S hS Y p))
    (hqc : IsQuasiCompact B S hS (fieldMorphism B S hS Y p)) :
    Topology.IsInducing (pointsMap B S hS (pullback f (fieldMorphism B S hS Y p))
      (pullback.fst f (fieldMorphism B S hS Y p)))

AlgebraicGeometry.Space.isEmbedding_pointsMap_fibre_fieldMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FibreOverFieldPoint.lean, line 360. The attribute's comment: “the fibre is embedded”.

Stacks 0AC8, the topology of the fibre. The map on points induced by the projection X ×_Y Spec k ⟶ X is a topological embedding when the morphism Spec k ⟶ Y presenting the field-valued point p is a quasi-compact monomorphism.

theorem isEmbedding_pointsMap_fibre_fieldMorphism (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y)
    (hmono : Mono (fieldMorphism B S hS Y p))
    (hqc : IsQuasiCompact B S hS (fieldMorphism B S hS Y p)) :
    Topology.IsEmbedding (pointsMap B S hS (pullback f (fieldMorphism B S hS Y p))
      (pullback.fst f (fieldMorphism B S hS Y p)))

AlgebraicGeometry.Space.fibreHomeomorph, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FibreOverFieldPoint.lean, line 374. The attribute's comment: “homeomorphism onto the fibre”.

Stacks 0AC8. For a morphism f : X ⟶ Y of algebraic spaces over S and a field-valued point p of Y whose presenting morphism Spec k ⟶ Y is a quasi-compact monomorphism, the point space of the fibre X ×_Y Spec k is homeomorphic to the set-theoretic fibre of |f| above the point presented by p, with its subspace topology.

noncomputable def fibreHomeomorph (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y)
    (hmono : Mono (fieldMorphism B S hS Y p))
    (hqc : IsQuasiCompact B S hS (fieldMorphism B S hS Y p)) :
    points B S hS (pullback f (fieldMorphism B S hS Y p)) ≃ₜ
      (pointsMap B S hS X f ⁻¹' {p.class B S hS Y})

AlgebraicGeometry.Space.range_pointsMap_fibre_fieldMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresCardinality.lean, line 106. The attribute's comment: “the image of the fibre”.

Stacks 0AC8, the image of the fibre. For a morphism f : X ⟶ Y of presheaves on the big fppf site of S and a field-valued point p of Y, the map on points induced by the projection X ×_Y Spec k ⟶ X has image exactly the fibre of |f| above the point presented by p.

theorem range_pointsMap_fibre_fieldMorphism (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y) :
    Set.range (pointsMap B S hS (pullback f (fieldMorphism B S hS Y p))
        (pullback.fst f (fieldMorphism B S hS Y p))) =
      {x : points B S hS X | pointsMap B S hS X f x = p.class B S hS Y}

AlgebraicGeometry.Space.injective_pointsMap_fibre_fieldMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PointsOfFibresCardinality.lean, line 123. The attribute's comment: “injectivity of the fibre”.

Stacks 0AC8, injectivity of the fibre. When the morphism presenting a field-valued point p of Y is a monomorphism, the map on points induced by the projection X ×_Y Spec k ⟶ X is injective.

theorem injective_pointsMap_fibre_fieldMorphism (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y)
    (hp : Mono (fieldMorphism B S hS Y p)) :
    Function.Injective (pointsMap B S hS (pullback f (fieldMorphism B S hS Y p))
      (pullback.fst f (fieldMorphism B S hS Y p)))

AlgebraicGeometry.Space.injective_pointsMap_fst_fieldFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreEmbedding.lean, line 101. The attribute's comment: “injectivity on points”.

Stacks 0AC8, injectivity. If the morphism Spec(k) ⟶ Y presented by a field-valued point p of Y is a monomorphism, then the comparison map |X_k| → |X| from the points of the field fibre is injective.

The projection X_k = X ×_Y Spec(k) ⟶ X is a pullback of that monomorphism, hence itself a monomorphism, and a monomorphism is injective on points by Tag 06RV.

theorem injective_pointsMap_fst_fieldFibre (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y)
    (hp : Mono (fieldMorphism B S hS Y p)) :
    Function.Injective (pointsMap B S hS (fieldFibre B S hS f p)
      (pullback.fst f (yonedaEquiv.symm p.value)))

AlgebraicGeometry.Space.bijOn_pointsMap_fst_fieldFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreEmbedding.lean, line 117. The attribute's comment: “bijection onto the set-theoretic fibre”.

Stacks 0AC8, the bijection. Under the monomorphism hypothesis the comparison map |X_k| → |X| is a bijection from the points of the field fibre onto the set-theoretic fibre f^{-1}({y}) ⊂ |X|.

Injectivity is AlgebraicGeometry.Space.injective_pointsMap_fst_fieldFibre and the image is AlgebraicGeometry.Space.range_pointsMap_fst_fieldFibre, which is Tag 03H4.

theorem bijOn_pointsMap_fst_fieldFibre (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y)
    (hp : Mono (fieldMorphism B S hS Y p)) :
    Set.BijOn (pointsMap B S hS (fieldFibre B S hS f p)
        (pullback.fst f (yonedaEquiv.symm p.value)))
      Set.univ (setFibre B S hS f p)

AlgebraicGeometry.Space.isInducing_pointsMap_fst_fieldFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreInducing.lean, line 390. The attribute's comment: “the induced topology”.

Stacks 0AC8, the induced topology. For a morphism f : X ⟶ Y of algebraic spaces over S and a field-valued point p of Y presented by a quasi-compact monomorphism, the comparison map |X_k| → |X| from the point space of the field fibre is topologically inducing.

An étale atlas U ⟶ X is surjective and open on points, and the base change of the comparison map along it is the comparison map for the composite h_U ⟶ X ⟶ Y, which is the subject of AlgebraicGeometry.Space.isInducing_pointsMap_yoneda_of_isPullback_fieldMorphism; the property transfers by AlgebraicGeometry.Space.isInducing_pointsMap_of_isPullback.

theorem isInducing_pointsMap_fst_fieldFibre {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (p : FieldValuedPoint B S hS Y) (hmono : Mono (fieldMorphism B S hS Y p))
    (hqc : IsQuasiCompact B S hS (fieldMorphism B S hS Y p)) :
    Topology.IsInducing (pointsMap B S hS (fieldFibre B S hS f p)
      (pullback.fst f (fieldMorphism B S hS Y p)))

AlgebraicGeometry.Space.homeomorphSetFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreInducing.lean, line 437. The attribute's comment: “homeomorphism onto the set-theoretic fibre”.

Stacks 0AC8. The point space of the field fibre X_k is homeomorphic to the set-theoretic fibre f^{-1}({y}) ⊂ |X| with its induced topology, by the comparison map.

This is the tag: the map is an embedding by AlgebraicGeometry.Space.isEmbedding_pointsMap_fst_fieldFibre and its image is the fibre by AlgebraicGeometry.Space.range_pointsMap_fst_fieldFibre, which is Tag 03H4.

noncomputable def homeomorphSetFibre {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (p : FieldValuedPoint B S hS Y) (hmono : Mono (fieldMorphism B S hS Y p))
    (hqc : IsQuasiCompact B S hS (fieldMorphism B S hS Y p)) :
    points B S hS (fieldFibre B S hS f p) ≃ₜ setFibre B S hS f p

Tag 0AC9, a lemma

Tag 0AC9 in the Stacks Project.

AlgebraicGeometry.Space.topologicalKrullDimAt_points_eq_dimensionAtPoint_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/Dimension.lean, line 96. The attribute's comment: “conditions (1) and (4) for decent spaces”.

Stacks 0A4J, part (1), and the fourth clause of Stacks 0AC9. At every point of a decent algebraic space over S the local Krull dimension of the point space agrees with the dimension of the space at that point, as defined by étale scheme charts.

This equality is what makes conditions (1) and (4) of Stacks 0AC9 — vanishing of the two dimensions at the point — equivalent for a decent space.

theorem topologicalKrullDimAt_points_eq_dimensionAtPoint_of_isDecentSpace
    (hX : IsAlgebraicSpace B S hS X) (hdec : IsDecentSpace B S hS X) (x : points B S hS X) :
    topologicalKrullDimAt (points B S hS X) x = dimensionAtPoint B S hS X hX x

AlgebraicGeometry.Space.isClosedNoGeneralization_iff_isIsolatedPoint_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ZeroDimensionalPoint.lean, line 416. The attribute's comment: “conditions (2) and (3)”.

Stacks 0AC9, conditions (2) and (3). A point of an algebraic space locally of finite type over a field is closed with no nontrivial generalization exactly when it is isolated.

theorem isClosedNoGeneralization_iff_isIsolatedPoint_over_field
    {Z : (BigFppfOver B (Spec (.of k)) hK)ᵒᵖ ⥤ Type u}
    (hZ : IsAlgebraicSpace B (Spec (.of k)) hK Z)
    (f : Z ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hK))))
    (hf : IsLocallyOfFiniteType B (Spec (.of k)) hK f) (x : points B (Spec (.of k)) hK Z) :
    (IsClosed ({x} : Set (points B (Spec (.of k)) hK Z)) ∧
        ∀ x' : points B (Spec (.of k)) hK Z, x' ⤳ x → x' = x) ↔ IsIsolatedPoint x

AlgebraicGeometry.Space.isIsolatedPoint_iff_dimensionAtPoint_eq_zero_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ZeroDimensionalPoint.lean, line 430. The attribute's comment: “conditions (3) and (4)”.

Stacks 0AC9, conditions (3) and (4). A point of an algebraic space locally of finite type over a field is isolated exactly when the space has dimension zero there.

theorem isIsolatedPoint_iff_dimensionAtPoint_eq_zero_over_field
    {Z : (BigFppfOver B (Spec (.of k)) hK)ᵒᵖ ⥤ Type u}
    (hZ : IsAlgebraicSpace B (Spec (.of k)) hK Z)
    (f : Z ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hK))))
    (hf : IsLocallyOfFiniteType B (Spec (.of k)) hK f) (x : points B (Spec (.of k)) hK Z) :
    IsIsolatedPoint x ↔ dimensionAtPoint B (Spec (.of k)) hK Z hZ x = 0

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

Stacks 0AC9, conditions (4) and (5). An algebraic space locally of finite type over a field has dimension zero at a point exactly when its structure morphism is quasi-finite there.

theorem dimensionAtPoint_eq_zero_iff_isQuasiFiniteAt_over_field
    {Z : (BigFppfOver B (Spec (.of k)) hK)ᵒᵖ ⥤ Type u}
    (hZ : IsAlgebraicSpace B (Spec (.of k)) hK Z)
    (f : Z ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hK))))
    (hf : IsLocallyOfFiniteType B (Spec (.of k)) hK f) (x : points B (Spec (.of k)) hK Z) :
    dimensionAtPoint B (Spec (.of k)) hK Z hZ x = 0 ↔
      IsQuasiFiniteAt B (Spec (.of k)) hK f x

Tag 0ACA, a lemma

Tag 0ACA in the Stacks Project.

AlgebraicGeometry.Space.FiniteTypeOverField.discretePoints_of_finitePoints_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FinitePointSpaces.lean, line 185. The attribute's comment: “decent clause of the corrected statement: (1) implies the others”.

Stacks 0ACA, condition (1) implies the others for a decent space. A decent algebraic space locally of finite type over a field whose point space is finite has discrete point space; the remaining conditions follow by tfae_of_isDecentSpace.

Decency gives condition (α) of Stacks 03JX, finiteness of the fibre of every affine étale chart above every point, which is what the argument consumes.

theorem discretePoints_of_finitePoints_of_isDecentSpace (D : FiniteTypeOverField.{u})
    (hdec : IsDecentSpace D.B (Spec (.of D.k)) D.base_mem D.X.left)
    (hfinite : D.FinitePoints) : D.DiscretePoints

AlgebraicGeometry.Space.FiniteTypeOverField.discretePoints_of_zeroTopologicalDimension_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FinitePointSpaces.lean, line 197. The attribute's comment: “corrected part (3) => (2): decency gives the Kolmogorov hypothesis, by 03K3”.

Stacks 0ACA, condition (3) implies condition (2) for a decent space. The point space of a decent algebraic space is Kolmogorov, by Stacks 03K3, which is exactly the hypothesis that discretePoints_of_zeroTopologicalDimension needs and that no algebraic space satisfies automatically.

theorem discretePoints_of_zeroTopologicalDimension_of_isDecentSpace
    (D : FiniteTypeOverField.{u})
    (hdec : IsDecentSpace D.B (Spec (.of D.k)) D.base_mem D.X.left)
    (hD : D.ZeroTopologicalDimension) : D.DiscretePoints

AlgebraicGeometry.Space.FiniteTypeOverField.tfae_discretePoints_zeroDimension_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FinitePointSpaces.lean, line 217. The attribute's comment: “(2) <=> (4) <=> (5), the dim = 0 form for a nonempty space; (3) not among them”.

Stacks 0ACA, conditions (2), (4) and (5) are equivalent. For a nonempty algebraic space locally of finite type over a field, with no separation hypothesis and no decency: the point space is discrete exactly when the space has dimension zero, exactly when the structure morphism is locally quasi-finite.

Condition (3) is not among them: the arrow out of it needs |X| to be Kolmogorov, and is discretePoints_of_zeroTopologicalDimension. Nonemptiness is carried by FiniteTypeOverField and is what the = 0 reading of conditions (3) and (4) needs — the dimensions of Tags 04N6 and 0055 are suprema in WithBot ℕ∞, so the empty space has dimension ⊥ while being discrete and locally quasi-finite. Dropping nonemptiness as well means reading condition (4) as dim(X) ≤ 0, which is AlgebraicGeometry.Space.tfae_discreteTopology_dimension_le_zero_isLocallyQuasiFinite.

theorem tfae_discretePoints_zeroDimension_locallyQuasiFinite (D : FiniteTypeOverField.{u}) :
    [D.DiscretePoints, D.ZeroDimension, D.LocallyQuasiFiniteOverField].TFAE

AlgebraicGeometry.Space.FiniteTypeOverField.tfae_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FinitePointSpaces.lean, line 233. The attribute's comment: “decent case: (2) <=> (3) <=> (4) <=> (5), the arrow out of (3) by 03K3”.

Stacks 0ACA, conditions (2), (3), (4) and (5) are equivalent for a decent space. For a nonempty decent algebraic space locally of finite type over a field, the point space is discrete exactly when it has Krull dimension zero, exactly when the space has dimension zero, exactly when the structure morphism is locally quasi-finite.

Only the arrow out of condition (3) uses decency, and it uses it only through Stacks 03K3: the other three conditions are equivalent for every algebraic space locally of finite type over a field, by tfae_discretePoints_zeroDimension_locallyQuasiFinite. Condition (3) genuinely needs a separation hypothesis on |X|; see the implementation notes.

theorem tfae_of_isDecentSpace (D : FiniteTypeOverField.{u})
    (hdec : IsDecentSpace D.B (Spec (.of D.k)) D.base_mem D.X.left) :
    [D.DiscretePoints, D.ZeroTopologicalDimension, D.ZeroDimension,
      D.LocallyQuasiFiniteOverField].TFAE

AlgebraicGeometry.Space.FiniteTypeOverField.discretePoints_iff_zeroDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ZeroDimensionalFibres.lean, line 629. The attribute's comment: “(2) <=> (4) <=> (5), the dim = 0 form: (2) <=> (4) for a nonempty space”.

The point space of a nonempty algebraic space locally of finite type over a field is discrete exactly when the algebraic space has dimension zero.

theorem discretePoints_iff_zeroDimension (D : FiniteTypeOverField.{u}) :
    D.DiscretePoints ↔ D.ZeroDimension

AlgebraicGeometry.Space.FiniteTypeOverField.zeroTopologicalDimension_of_discretePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ZeroDimensionalFibres.lean, line 639. The attribute's comment: “the arrow into (3): (2) => (3), in the dim = 0 form”.

If the point space is discrete then it has Krull dimension zero.

theorem zeroTopologicalDimension_of_discretePoints (D : FiniteTypeOverField.{u})
    (hD : D.DiscretePoints) : D.ZeroTopologicalDimension

AlgebraicGeometry.Space.FiniteTypeOverField.discretePoints_of_zeroTopologicalDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ZeroDimensionalFibres.lean, line 648. The attribute's comment: “corrected part (3) => (2), the sharp form: |X| Kolmogorov”.

If the point space is T0 and has Krull dimension zero, then it is discrete. The hypothesis that the point space is T0 cannot be dropped.

theorem discretePoints_of_zeroTopologicalDimension (D : FiniteTypeOverField.{u})
    (hT0 : T0Space (points D.B (Spec (.of D.k)) D.base_mem D.X.left))
    (hD : D.ZeroTopologicalDimension) : D.DiscretePoints

AlgebraicGeometry.Space.FiniteTypeOverField.zeroDimension_iff_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ZeroDimensionalFibres.lean, line 659. The attribute's comment: “(2) <=> (4) <=> (5), the dim = 0 form: (4) <=> (5) for a nonempty space”.

A nonempty algebraic space locally of finite type over a field has dimension zero exactly when its structure morphism is locally quasi-finite.

theorem zeroDimension_iff_locallyQuasiFinite (D : FiniteTypeOverField.{u}) :
    D.ZeroDimension ↔ D.LocallyQuasiFiniteOverField

AlgebraicGeometry.Space.isLocallyQuasiFinite_iff_dimension_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroOverField.lean, line 247. The attribute's comment: “unconditional part (2) <=> (4) <=> (5): the arrow (4) <=> (5), dim <= 0 form”. References: EGA IV (4.1.2), “(ii), case Y = Spec(k)”.

Stacks 0ACA, condition (4) is equivalent to condition (5). An algebraic space over S locally of finite type over a representable base whose scheme has at most one point has dimension at most zero exactly when the structure morphism is locally quasi-finite.

The source states condition (4) as dim(X) = 0; the dimension of Tag 04N6 is a supremum in WithBot ℕ∞, so the empty space has dimension ⊥ while being locally quasi-finite over any base, and the faithful unconditional form of the equivalence is therefore the inequality. See AlgebraicGeometry.Space.dimension_eq_zero_of_isLocallyQuasiFinite for the = 0 form.

theorem isLocallyQuasiFinite_iff_dimension_le_zero (hX : IsAlgebraicSpace B S hS X)
    (hk : Subsingleton ((BigFppfOver.toScheme B S hS).obj k)) (g : X ⟶ yoneda.obj k)
    (hg : IsLocallyOfFiniteType B S hS g) :
    IsLocallyQuasiFinite B S hS g ↔ dimension B S hS X hX ≤ 0

AlgebraicGeometry.Space.dimension_eq_zero_of_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroOverField.lean, line 260. The attribute's comment: “(2) <=> (4) <=> (5), the dim = 0 form: (5) => (4) for a nonempty space”.

Stacks 0ACA, condition (5) implies condition (4). The = 0 form of the dimension statement, which needs the space to have a point: the dimension of Tag 04N6 is a supremum, so the empty space has dimension ⊥.

theorem dimension_eq_zero_of_isLocallyQuasiFinite (hX : IsAlgebraicSpace B S hS X)
    (hk : Subsingleton ((BigFppfOver.toScheme B S hS).obj k)) (g : X ⟶ yoneda.obj k)
    (hg : IsLocallyOfFiniteType B S hS g) (hqf : IsLocallyQuasiFinite B S hS g)
    (hne : Nonempty (points B S hS X)) :
    dimension B S hS X hX = 0

AlgebraicGeometry.Space.discreteTopology_points_of_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroOverField.lean, line 287. The attribute's comment: “unconditional part (2) <=> (4) <=> (5): the arrow (5) => (2)”.

Stacks 0ACA, condition (5) implies condition (2). If the structure morphism of an algebraic space over S to a representable base whose scheme has at most one point is locally quasi-finite, then the point space of Tag 03BU is discrete.

An étale atlas U ⟶ X by a scheme gives a chart square over the identity of the base, so U ⟶ Spec(k) is locally quasi-finite, hence U is discrete; and |U| → |X| is open and surjective on points, so each singleton of |X| is the image of a singleton of |U|.

theorem discreteTopology_points_of_isLocallyQuasiFinite (hX : IsAlgebraicSpace B S hS X)
    (hk : Subsingleton ((BigFppfOver.toScheme B S hS).obj k)) (g : X ⟶ yoneda.obj k)
    (hqf : IsLocallyQuasiFinite B S hS g) :
    DiscreteTopology (points B S hS X)

AlgebraicGeometry.Space.topologicalKrullDim_points_le_zero_of_discreteTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroOverField.lean, line 312. The attribute's comment: “the arrow into (3): (2) => (3), unconditional, dim <= 0 form”.

Stacks 0ACA, condition (2) implies condition (3). A discrete point space has dimension at most zero. The source writes condition (3) as dim(|X|) = 0; the empty space is discrete and has dimension ⊥, so the unconditional form is the inequality.

theorem topologicalKrullDim_points_le_zero_of_discreteTopology
    (h : DiscreteTopology (points B S hS X)) :
    topologicalKrullDim (points B S hS X) ≤ 0

AlgebraicGeometry.Space.discreteTopology_points_of_finite_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroOverFieldDecent.lean, line 111. The attribute's comment: “decent clause of the corrected statement: (1) => (2)”.

Stacks 0ACA, condition (1) implies condition (2) for a decent space. Let X be a decent algebraic space over S, locally of finite type over a representable base whose underlying scheme has at most one point. If the point set of X is finite, then it is discrete.

An affine étale chart through a given point of |X| has finite fibre above every point of |X|, by Tag 03JV applied to the quasi-compact monomorphic field-valued representative that decency supplies there; so the chart has finitely many points, and being locally of finite type over a one-point base it is discrete. The chart is open on points, so the given point is isolated.

theorem discreteTopology_points_of_finite_of_isDecentSpace
    (hX : IsAlgebraicSpace B S hS X)
    (hk : Subsingleton ((BigFppfOver.toScheme B S hS).obj k)) (g : X ⟶ yoneda.obj k)
    (hg : IsLocallyOfFiniteType B S hS g) (hdec : IsDecentSpace B S hS X)
    (hfin : Finite (points B S hS X)) :
    DiscreteTopology (points B S hS X)

AlgebraicGeometry.Space.dimension_le_zero_of_discreteTopology_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroOverFieldSpecialization.lean, line 267. The attribute's comment: “unconditional part (2) <=> (4) <=> (5): the arrow (2) => (4), dim <= 0 form”.

Stacks 0ACA, condition (2) implies condition (4). An algebraic space locally of finite type over a field whose point space of Tag 03BU is discrete has dimension at most zero.

A discrete space is T₁, so its specialization relation is trivial, which is the hypothesis of AlgebraicGeometry.Space.dimension_le_zero_of_specializes_imp_eq. The source states condition (4) as dim(X) = 0; the empty space is discrete and has dimension ⊥, so the unconditional form is the inequality.

theorem dimension_le_zero_of_discreteTopology_points (hX : IsAlgebraicSpace B S hS X)
    (hκ : B.Contains (Spec (CommRingCat.of κ))) (σ : Spec (CommRingCat.of κ) ⟶ S)
    (hk : k = BigFppfOver.mk B S hS hκ σ) (g : X ⟶ yoneda.obj k)
    (hg : IsLocallyOfFiniteType B S hS g)
    (hdisc : DiscreteTopology (points B S hS X)) :
    dimension B S hS X hX ≤ 0

AlgebraicGeometry.Space.isLocallyQuasiFinite_of_discreteTopology_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroOverFieldSpecialization.lean, line 281. The attribute's comment: “unconditional part (2) <=> (4) <=> (5): the arrow (2) => (5)”.

Stacks 0ACA, condition (2) implies condition (5). An algebraic space locally of finite type over a field whose point space of Tag 03BU is discrete is locally quasi-finite over the field.

theorem isLocallyQuasiFinite_of_discreteTopology_points (hX : IsAlgebraicSpace B S hS X)
    (hκ : B.Contains (Spec (CommRingCat.of κ))) (σ : Spec (CommRingCat.of κ) ⟶ S)
    (hk : k = BigFppfOver.mk B S hS hκ σ) (g : X ⟶ yoneda.obj k)
    (hg : IsLocallyOfFiniteType B S hS g)
    (hdisc : DiscreteTopology (points B S hS X)) :
    IsLocallyQuasiFinite B S hS g

AlgebraicGeometry.Space.tfae_discreteTopology_dimension_le_zero_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroOverFieldSpecialization.lean, line 313. The attribute's comment: “unconditional part: (2) <=> (4) <=> (5), no T0Space, no decency, no nonemptiness”. References: EGA IV (4.1.2), “(ii), case Y = Spec(κ)”.

Stacks 0ACA, conditions (2), (4) and (5) are equivalent. For an algebraic space locally of finite type over a field, with no further hypothesis: the point space of Tag 03BU is discrete exactly when the space has dimension at most zero, exactly when the structure morphism is locally quasi-finite.

This is the part of the tag that holds in general. It carries no separation hypothesis on |X|, no decency and no nonemptiness: the three arrows it is assembled from — (2) ⟹ (4) here, (4) ⟹ (5) by AlgebraicGeometry.Space.isLocallyQuasiFinite_iff_dimension_le_zero and (5) ⟹ (2) by AlgebraicGeometry.Space.discreteTopology_points_of_isLocallyQuasiFinite — carry none either. Condition (3) is deliberately absent: the arrow out of it is false in this generality, and is AlgebraicGeometry.Space.discreteTopology_points_of_topologicalKrullDim_eq_zero below.

The source writes conditions (3) and (4) with = 0. The dimension of Tag 04N6 is a supremum in WithBot ℕ∞, so the empty space has dimension ⊥ while being discrete and locally quasi-finite over any base; the faithful unconditional form of condition (4) is therefore the inequality. The = 0 form, which needs |X| to have a point, is FiniteTypeOverField.tfae_discretePoints_zeroDimension_locallyQuasiFinite.

theorem tfae_discreteTopology_dimension_le_zero_isLocallyQuasiFinite
    (hX : IsAlgebraicSpace B S hS X)
    (hκ : B.Contains (Spec (CommRingCat.of κ))) (σ : Spec (CommRingCat.of κ) ⟶ S)
    (hk : k = BigFppfOver.mk B S hS hκ σ) (g : X ⟶ yoneda.obj k)
    (hg : IsLocallyOfFiniteType B S hS g) :
    [DiscreteTopology (points B S hS X), dimension B S hS X hX ≤ 0,
      IsLocallyQuasiFinite B S hS g].TFAE

AlgebraicGeometry.Space.discreteTopology_points_of_topologicalKrullDim_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroOverFieldSpecialization.lean, line 349. The attribute's comment: “corrected part (3) => (2), the sharp form: |X| Kolmogorov”.

Condition (3) of Stacks 0ACA implies condition (2), for a T₀ point space. An algebraic space locally of finite type over a field whose point space of Tag 03BU is T₀ and has Krull dimension zero has discrete point space.

In a T₀ space a nontrivial specialization x ⤳ x' gives the chain closure {x'} ⊊ closure {x} of irreducible closed subsets, so dimension zero makes the specialization relation trivial; then AlgebraicGeometry.Space.isLocallyQuasiFinite_of_specializes_imp_eq and Stacks 0ACA, condition (5) implies condition (2), close the loop.

The T₀ hypothesis is not in the source and cannot be dropped, so the source's unrestricted claim is false: the point space of 𝔸¹_k/ℤ is the indiscrete topology on an infinite set, so it has Krull dimension zero without being discrete. See the implementation notes of this file. This is the strongest true form of the implication; with T₀ discharged for a decent space it is discreteTopology_points_of_topologicalKrullDim_eq_zero_of_isDecentSpace.

theorem discreteTopology_points_of_topologicalKrullDim_eq_zero (hX : IsAlgebraicSpace B S hS X)
    (hκ : B.Contains (Spec (CommRingCat.of κ))) (σ : Spec (CommRingCat.of κ) ⟶ S)
    (hk : k = BigFppfOver.mk B S hS hκ σ) (g : X ⟶ yoneda.obj k)
    (hg : IsLocallyOfFiniteType B S hS g) (ht0 : T0Space (points B S hS X))
    (hdim : topologicalKrullDim (points B S hS X) = (0 : WithBot ℕ∞)) :
    DiscreteTopology (points B S hS X)

AlgebraicGeometry.Space.discreteTopology_points_of_topologicalKrullDim_eq_zero_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionZeroOverFieldSpecialization.lean, line 372. The attribute's comment: “corrected part (3) => (2): decency gives the Kolmogorov hypothesis, by 03K3”.

Stacks 0ACA, condition (3) implies condition (2) for a decent space. A decent algebraic space locally of finite type over a field whose point space of Tag 03BU has Krull dimension zero has discrete point space.

The point space of a decent algebraic space is Kolmogorov by Stacks 03K3, which discharges the T₀ hypothesis of AlgebraicGeometry.Space.discreteTopology_points_of_topologicalKrullDim_eq_zero.

theorem discreteTopology_points_of_topologicalKrullDim_eq_zero_of_isDecentSpace
    (hX : IsAlgebraicSpace B S hS X) (hdec : IsDecentSpace B S hS X)
    (hκ : B.Contains (Spec (CommRingCat.of κ))) (σ : Spec (CommRingCat.of κ) ⟶ S)
    (hk : k = BigFppfOver.mk B S hS hκ σ) (g : X ⟶ yoneda.obj k)
    (hg : IsLocallyOfFiniteType B S hS g)
    (hdim : topologicalKrullDim (points B S hS X) = (0 : WithBot ℕ∞)) :
    DiscreteTopology (points B S hS X)

Stacks.Examples.DimensionVersusPointSet.exists_zeroTopologicalDimension_not_discretePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/ZeroDimensionalPointsNotDiscrete.lean, line 129. The attribute's comment: “the erratum's counterexample: the unrestricted (3) => (2) is false”.

Stacks 0ACA. Conditions (2), (3), (4) and (5) are not equivalent for a general nonempty algebraic space locally of finite type over a field: the quotient of the affine line by the integer translations has a point space of Krull dimension zero which is not discrete, and is neither of dimension zero nor locally quasi-finite over the field.

theorem exists_zeroTopologicalDimension_not_discretePoints :
    ∃ D : Space.FiniteTypeOverField.{u}, D.ZeroTopologicalDimension ∧ ¬ D.DiscretePoints ∧
      ¬ D.ZeroDimension ∧ ¬ D.LocallyQuasiFiniteOverField

Stacks.Examples.DimensionVersusPointSet.not_forall_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/ZeroDimensionalPointsNotDiscrete.lean, line 148. The attribute's comment: “the erratum's counterexample: the tag's four-way equivalence, negated”.

Stacks 0ACA is false as stated. The source asserts that conditions (2), (3), (4) and (5) are equivalent for every algebraic space locally of finite type over a field; they are not.

This is the negation of that assertion, in the source's own vocabulary. The equivalence of (2), (4) and (5) does hold with no further hypothesis, and the arrow out of (3) holds once |X| is Kolmogorov — in particular for a decent space, by Stacks 03K3.

theorem not_forall_tfae :
    ¬ ∀ D : Space.FiniteTypeOverField.{u},
        [D.DiscretePoints, D.ZeroTopologicalDimension, D.ZeroDimension,
          D.LocallyQuasiFiniteOverField].TFAE

Tag 0ACB, a lemma

Tag 0ACB in the Stacks Project.

AlgebraicGeometry.Space.isIsolatedPoint_fieldFibre_of_topologicalKrullDimAt_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FieldFibreTopologicalDimension.lean, line 134. The attribute's comment: “condition (4) implies (5) for decent morphisms”.

Stacks 0ACB, condition (4) implies condition (5) for a decent morphism. If the point space of the field fibre of a decent morphism of algebraic spaces locally of finite type has local Krull dimension zero at a point, then that point is isolated in it.

For a decent morphism the field fibre is a decent algebraic space, so Stacks 0A4J identifies the local Krull dimension of its point space with its dimension as an algebraic space, which is condition (7); conditions (7), (6) and (5) are equivalent.

theorem isIsolatedPoint_fieldFibre_of_topologicalKrullDimAt_eq_zero
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (hd : IsDecent B S hS f)
    (p : FieldValuedPoint B S hS Y) (z : points B S hS (fieldFibre B S hS f p))
    (h : topologicalKrullDimAt (points B S hS (fieldFibre B S hS f p)) z = 0) :
    IsIsolatedPoint z

AlgebraicGeometry.Space.topologicalKrullDimAt_points_fieldFibre_eq_zero_iff_isIsolatedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FieldFibreTopologicalDimension.lean, line 154. The attribute's comment: “conditions (4) and (5) for decent spaces”.

Stacks 0ACB, conditions (4) and (5) for decent spaces. A point of the point space of the field fibre of a morphism of algebraic spaces locally of finite type with decent source is isolated exactly when that point space has local Krull dimension zero there.

A morphism out of a decent algebraic space is a decent morphism, Stacks 0ABX, which gives the implication from dimension zero to isolation. The converse holds for any topological space: an isolated point has a one-point open neighbourhood.

theorem topologicalKrullDimAt_points_fieldFibre_eq_zero_iff_isIsolatedPoint
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (hdec : IsDecentSpace B S hS X)
    (p : FieldValuedPoint B S hS Y) (z : points B S hS (fieldFibre B S hS f p)) :
    topologicalKrullDimAt (points B S hS (fieldFibre B S hS f p)) z = 0 ↔
      IsIsolatedPoint z

AlgebraicGeometry.Space.isIsolatedPoint_fieldFibre_iff_isClosedNoGeneralization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IsolatedFibrePoint.lean, line 130. The attribute's comment: “conditions (5) and (6)”.

Stacks 0ACB, conditions (5) and (6). A point of the field fibre of a morphism of algebraic spaces locally of finite type is isolated exactly when it is closed in the field fibre and admits no nontrivial generalization there.

The field fibre is locally of finite type over the spectrum of a field, so this is the comparison of conditions (2) and (3) of Stacks 0AC9.

theorem isIsolatedPoint_fieldFibre_iff_isClosedNoGeneralization
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (z : points B S hS (fieldFibre B S hS f p)) :
    IsIsolatedPoint z ↔
      (IsClosed ({z} : Set (points B S hS (fieldFibre B S hS f p))) ∧
        ∀ z' : points B S hS (fieldFibre B S hS f p), z' ⤳ z → z' = z)

AlgebraicGeometry.Space.isClosedNoGeneralization_fieldFibre_iff_dimensionAtPoint_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IsolatedFibrePoint.lean, line 146. The attribute's comment: “conditions (6) and (7)”.

Stacks 0ACB, conditions (6) and (7). A point of the field fibre of a morphism of algebraic spaces locally of finite type is closed there with no nontrivial generalization exactly when the field fibre has dimension zero at that point.

The field fibre is locally of finite type over the spectrum of a field, so this is the comparison of conditions (2), (3) and (4) of Stacks 0AC9.

theorem isClosedNoGeneralization_fieldFibre_iff_dimensionAtPoint_eq_zero
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (z : points B S hS (fieldFibre B S hS f p)) :
    (IsClosed ({z} : Set (points B S hS (fieldFibre B S hS f p))) ∧
        ∀ z' : points B S hS (fieldFibre B S hS f p), z' ⤳ z → z' = z) ↔
      dimensionAtPoint B S hS (fieldFibre B S hS f p)
        (isAlgebraicSpace_fieldFibre hX hY f p) z = 0

AlgebraicGeometry.Space.dimensionAtPoint_fieldFibre_eq_zero_iff_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IsolatedFibrePoint.lean, line 170. The attribute's comment: “conditions (7) and (8)”.

Stacks 0ACB, conditions (7) and (8). The field fibre of a morphism of algebraic spaces locally of finite type has dimension zero at a point exactly when the morphism is quasi-finite at the image of that point.

The implication to quasi-finiteness is Stacks 06LS. Conversely, the locus of quasi-finiteness of the structure morphism of the field fibre is the inverse image of the locus of quasi-finiteness of the morphism (Stacks 0ABM, part (2)), so the structure morphism of the field fibre is quasi-finite at the point; the spectrum of a field has one point, so the field fibre has dimension zero there.

theorem dimensionAtPoint_fieldFibre_eq_zero_iff_isQuasiFiniteAt
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (z : points B S hS (fieldFibre B S hS f p)) :
    dimensionAtPoint B S hS (fieldFibre B S hS f p)
        (isAlgebraicSpace_fieldFibre hX hY f p) z = 0 ↔
      IsQuasiFiniteAt B S hS f
        (pointsMap B S hS (fieldFibre B S hS f p)
          (pullback.fst f (yonedaEquiv.symm p.value)) z)

AlgebraicGeometry.Space.isIsolatedPoint_fibre_iff_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IsolatedSetFibrePoint.lean, line 258. The attribute's comment: “conditions (2) and (8), for a decent target”.

Stacks 0ACB, conditions (2) and (8). Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type with decent target, let y be a point of |Y| and let F = f^{-1}({y}) carry the topology induced from |X|. A point of F is isolated in F exactly when f is quasi-finite at it.

A decent target carries a quasi-compact monomorphism Spec k' ⟶ Y in the equivalence class of y, and for such a representative the comparison map |X_{k'}| → |X| is a homeomorphism onto F, by Stacks 0AC8. Being isolated is a homeomorphism invariant, so the condition becomes condition (5) on |X_{k'}|, which is condition (8).

theorem isIsolatedPoint_fibre_iff_isQuasiFiniteAt
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (hYdec : IsDecentSpace B S hS Y)
    (y : points B S hS Y) (x : ↥(pointsMap B S hS X f ⁻¹' {y})) :
    IsIsolatedPoint x ↔ IsQuasiFiniteAt B S hS f (x : points B S hS X)

AlgebraicGeometry.Space.isClosedNoGeneralization_fibre_iff_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IsolatedSetFibrePoint.lean, line 275. The attribute's comment: “conditions (3) and (8), for a decent target”.

Stacks 0ACB, conditions (3) and (8). In the situation above, a point of F = f^{-1}({y}) is closed in F and admits no nontrivial generalization there exactly when f is quasi-finite at it.

Both halves of the condition are homeomorphism invariants, so the comparison homeomorphism |X_{k'}| ≃ F of Stacks 0AC8 turns the condition into condition (6) on |X_{k'}|, which is condition (8).

theorem isClosedNoGeneralization_fibre_iff_isQuasiFiniteAt
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (hYdec : IsDecentSpace B S hS Y)
    (y : points B S hS Y) (x : ↥(pointsMap B S hS X f ⁻¹' {y})) :
    (IsClosed ({x} : Set ↥(pointsMap B S hS X f ⁻¹' {y})) ∧
        ∀ x' : ↥(pointsMap B S hS X f ⁻¹' {y}), x' ⤳ x → x' = x) ↔
      IsQuasiFiniteAt B S hS f (x : points B S hS X)

AlgebraicGeometry.Space.topologicalKrullDimAt_fibre_eq_zero_iff_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/IsolatedSetFibrePoint.lean, line 296. The attribute's comment: “conditions (1) and (8), for a decent morphism with decent target”.

Stacks 0ACB, conditions (1) and (8). For a decent morphism of algebraic spaces over S which is locally of finite type and has decent target, the set-theoretic fibre F = f^{-1}({y}) has local Krull dimension zero at a point exactly when f is quasi-finite there.

The comparison homeomorphism |X_{k'}| ≃ F of Stacks 0AC8 turns the condition into condition (4) on |X_{k'}|, the local Krull dimension being a homeomorphism invariant, and condition (4) implies condition (5) for a decent morphism. The source states this for a decent source X, which gives a decent morphism by Stacks 0ABX.

theorem topologicalKrullDimAt_fibre_eq_zero_iff_isQuasiFiniteAt
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (hd : IsDecent B S hS f)
    (hYdec : IsDecentSpace B S hS Y) (y : points B S hS Y)
    (x : ↥(pointsMap B S hS X f ⁻¹' {y})) :
    topologicalKrullDimAt (↥(pointsMap B S hS X f ⁻¹' {y})) x = 0 ↔
      IsQuasiFiniteAt B S hS f (x : points B S hS X)

Tag 0ACK, a lemma

Tag 0ACK in the Stacks Project.

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

If the point set of the field fibre X_k of a morphism f : X ⟶ Y of algebraic spaces is finite, then the set-theoretic fibre f^{-1}({y}) ⊂ |X| is finite.

theorem finite_setFibre_of_finite_fieldFibre
    (_hX : IsAlgebraicSpace B S hS X) (_hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y)
    (hfinite : (Set.univ : Set (points B S hS (fieldFibre B S hS f p))).Finite) :
    (setFibre B S hS f p).Finite

AlgebraicGeometry.Space.IsDiscreteSetFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreConditions.lean, line 79. The attribute's comment: “condition (2)”.

The set-theoretic fibre F = f^{-1}({y}), with the topology induced from |X|, is a discrete topological space.

def IsDiscreteSetFibre (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y) : Prop

AlgebraicGeometry.Space.IsZeroDimensionalSetFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreConditions.lean, line 85. The attribute's comment: “condition (3)”.

The set-theoretic fibre F = f^{-1}({y}), with the topology induced from |X|, has dimension zero.

def IsZeroDimensionalSetFibre (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y) : Prop

AlgebraicGeometry.Space.IsDiscreteFieldFibrePoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreConditions.lean, line 90. The attribute's comment: “condition (5)”.

The point set of the field fibre X_k is a discrete topological space.

def IsDiscreteFieldFibrePoints (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y) : Prop

AlgebraicGeometry.Space.IsZeroDimensionalFieldFibrePoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreConditions.lean, line 95. The attribute's comment: “condition (6)”.

The point set of the field fibre X_k has dimension zero.

def IsZeroDimensionalFieldFibrePoints (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y) : Prop

AlgebraicGeometry.Space.IsZeroDimensionalFieldFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreConditions.lean, line 103. The attribute's comment: “condition (7)”.

The field fibre X_k, as an algebraic space over S, has dimension zero in the sense of Tag 04N6.

def IsZeroDimensionalFieldFibre (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y)
    (hXk : IsAlgebraicSpace B S hS (fieldFibre B S hS f p)) : Prop

AlgebraicGeometry.Space.IsQuasiFiniteAboveFieldValuedPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreConditions.lean, line 112. The attribute's comment: “condition (8)”.

The morphism f is quasi-finite, in the sense of part (2) of Tag 03XJ, at every point of |X| lying above the point of |Y| represented by p.

def IsQuasiFiniteAboveFieldValuedPoint (f : X ⟶ Y) (p : FieldValuedPoint B S hS Y) : Prop

AlgebraicGeometry.Space.isZeroDimensionalSetFibre_of_isDiscreteSetFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreConditions.lean, line 143. The attribute's comment: “condition (2) implies condition (3), nonempty fibre”.

A nonempty discrete set-theoretic fibre has dimension zero.

theorem isZeroDimensionalSetFibre_of_isDiscreteSetFibre (f : X ⟶ Y)
    (p : FieldValuedPoint B S hS Y) (h : IsDiscreteSetFibre B S hS f p)
    (hne : (setFibre B S hS f p).Nonempty) :
    IsZeroDimensionalSetFibre B S hS f p

AlgebraicGeometry.Space.isZeroDimensionalFieldFibrePoints_of_isDiscreteFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreConditions.lean, line 160. The attribute's comment: “condition (5) implies condition (6), nonempty fibre”.

A nonempty discrete point set of the field fibre has dimension zero.

theorem isZeroDimensionalFieldFibrePoints_of_isDiscreteFieldFibrePoints (f : X ⟶ Y)
    (p : FieldValuedPoint B S hS Y) (h : IsDiscreteFieldFibrePoints B S hS f p)
    (hne : Nonempty (points B S hS (fieldFibre B S hS f p))) :
    IsZeroDimensionalFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.isZeroDimensionalFieldFibre_of_isDiscreteFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreDiscreteDecent.lean, line 190. The attribute's comment: “condition (5) implies condition (7), nonempty fibre”.

Stacks 0ACK, condition (5) implies condition (7) for a nonempty fibre. If the point space of the field fibre X_k is discrete and nonempty, then X_k has dimension zero as an algebraic space.

The inequality dim(X_k) ≤ 0 is AlgebraicGeometry.Space.dimension_fieldFibre_le_zero_of_isDiscreteFieldFibrePoints; it makes the structure morphism X_k ⟶ Spec(k) locally quasi-finite, and nonemptiness then upgrades the inequality to the equation, since the dimension of Tag 04N6 is a supremum in WithBot ℕ∞ and the empty space has dimension ⊥.

theorem isZeroDimensionalFieldFibre_of_isDiscreteFieldFibrePoints
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (hXk : IsAlgebraicSpace B S hS (fieldFibre B S hS f p))
    (h : IsDiscreteFieldFibrePoints B S hS f p)
    (hne : Nonempty (points B S hS (fieldFibre B S hS f p))) :
    IsZeroDimensionalFieldFibre B S hS f p hXk

AlgebraicGeometry.Space.isDiscreteFieldFibrePoints_iff_isQuasiFiniteAboveFieldValuedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreDiscreteDecent.lean, line 220. The attribute's comment: “conditions (5) and (8)”.

Stacks 0ACK, conditions (5) and (8). For a morphism locally of finite type and a field-valued point of its target, the point space of the field fibre X_k is discrete exactly when f is quasi-finite at every point of |X| above the point represented.

Both directions run through local quasi-finiteness of the structure morphism X_k ⟶ Spec(k), which isLocallyQuasiFinite_snd_fieldFibre_of_isQuasiFiniteAboveFieldValuedPoint and its converse identify with condition (8). Forward, AlgebraicGeometry.Space.dimension_fieldFibre_le_zero_of_isDiscreteFieldFibrePoints gives dim(X_k) ≤ 0, which is that local quasi-finiteness. No nonemptiness hypothesis is needed, exactly as the source makes none: the two conditions compared are a topological property and a pointwise property of the fibre, both of which hold vacuously for an empty fibre, and the route taken passes only through the ≤ 0 form of the dimension of Tag 04N6 and never through its = 0 form, whose value on the empty space is ⊥.

theorem isDiscreteFieldFibrePoints_iff_isQuasiFiniteAboveFieldValuedPoint
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y) :
    IsDiscreteFieldFibrePoints B S hS f p ↔
      IsQuasiFiniteAboveFieldValuedPoint B S hS f p

AlgebraicGeometry.Space.discreteTopology_setFibre_iff_discreteTopology_points_fieldFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreDiscreteDecent.lean, line 251. The attribute's comment: “conditions (2) and (5) for a decent target”.

Stacks 0ACK, conditions (2) and (5) for a decent target. Let f : X ⟶ Y be a morphism of algebraic spaces locally of finite type, let p be a field-valued point of Y with set-theoretic fibre F, and let Y be decent. Then F is discrete exactly when the point space of the field fibre X_k is discrete.

Decency of Y supplies a field-valued point q representing the same point of |Y| whose presenting morphism is a quasi-compact monomorphism, which is condition (4) of Stacks 03JV. For that representative Lemma 0AC8 identifies |X_q| with F as topological spaces (AlgebraicGeometry.Space.homeomorphSetFibre), and F is the same set for q as for p by AlgebraicGeometry.Space.setFibre_eq_of_class_eq. So condition (2) is equivalent to condition (5) for q. Condition (5) is equivalent to condition (8) for either representative by AlgebraicGeometry.Space.isDiscreteFieldFibrePoints_iff_isQuasiFiniteAboveFieldValuedPoint, and condition (8) is representative-free, which closes the chain back to condition (5) for p.

theorem discreteTopology_setFibre_iff_discreteTopology_points_fieldFibre
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (p : FieldValuedPoint B S hS Y) (hft : IsLocallyOfFiniteType B S hS f)
    (hdecent : IsDecentSpace B S hS Y) :
    DiscreteTopology (setFibre B S hS f p) ↔
      DiscreteTopology (points B S hS (fieldFibre B S hS f p))

AlgebraicGeometry.Space.finite_univ_points_fieldFibre_of_finite_setFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreEmbedding.lean, line 144. The attribute's comment: “condition (1) implies condition (4), monomorphic representative”.

Stacks 0ACK, condition (1) implies condition (4) for a point represented by a monomorphism. This is the converse of AlgebraicGeometry.Space.finite_setFibre_of_finite_fieldFibre, and it is available because the comparison map is then a bijection and not merely a surjection onto the fibre.

theorem finite_univ_points_fieldFibre_of_finite_setFibre (f : X ⟶ Y)
    (p : FieldValuedPoint B S hS Y) (hp : Mono (fieldMorphism B S hS Y p))
    (hfin : (setFibre B S hS f p).Finite) :
    (Set.univ : Set (points B S hS (fieldFibre B S hS f p))).Finite

AlgebraicGeometry.Space.discreteTopology_points_fieldFibre_of_finite_of_isDecent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreEquivalences.lean, line 155. The attribute's comment: “condition (4) implies condition (5) for a decent morphism”.

Stacks 0ACK, condition (4) implies condition (5) for a decent morphism. If f is a decent morphism locally of finite type and the point set of the field fibre X_k is finite, then that point set is discrete.

The field fibre is an algebraic space locally of finite type over the one-point scheme Spec(k) and, f being decent, a decent one; so Lemma 0ACA, condition (1) implies condition (2), applies to it. Decency is available for the flipped pullback Spec(k) ×_Y X, which is the shape Stacks 03KZ quantifies over, and the hypothesis and conclusion are carried across the symmetry isomorphism.

theorem discreteTopology_points_fieldFibre_of_finite_of_isDecent
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (p : FieldValuedPoint B S hS Y) (hft : IsLocallyOfFiniteType B S hS f)
    (hdecent : IsDecent B S hS f)
    (hfinite : (Set.univ : Set (points B S hS (fieldFibre B S hS f p))).Finite) :
    DiscreteTopology (points B S hS (fieldFibre B S hS f p))

AlgebraicGeometry.Space.dimension_fieldFibre_eq_zero_iff_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreEquivalences.lean, line 192. The attribute's comment: “conditions (7) and (8)”.

Stacks 0ACK, conditions (7) and (8). For a morphism f locally of finite type and a field-valued point p of its target with nonempty set-theoretic fibre, the field fibre X_k has dimension zero as an algebraic space exactly when f is quasi-finite at every point of |X| above the point represented by p.

Both implications are proved in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreQuasiFinite.lean; the nonemptiness hypothesis is needed only to turn dim(X_k) ≤ 0 into dim(X_k) = 0, and it reaches the field fibre through Tag 03H4.

theorem dimension_fieldFibre_eq_zero_iff_isQuasiFiniteAt
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (p : FieldValuedPoint B S hS Y) (hft : IsLocallyOfFiniteType B S hS f)
    (hne : (setFibre B S hS f p).Nonempty) :
    dimension B S hS (fieldFibre B S hS f p)
        (isAlgebraicSpace_pullback B S hS f (fieldMorphism B S hS Y p) hX
          (isAlgebraicSpace_yoneda B S hS p.siteObject) hY) = 0 ↔
      ∀ x : points B S hS X, x ∈ setFibre B S hS f p → IsQuasiFiniteAt B S hS f x

AlgebraicGeometry.Space.finite_univ_points_fieldFibre_of_finite_setFibre_of_isDecent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreFiniteDecent.lean, line 204. The attribute's comment: “condition (1) implies condition (4) for decent spaces”.

Stacks 0ACK, condition (1) implies condition (4) for decent spaces. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, let p be a field-valued point of Y with set-theoretic fibre F, and let both X and Y be decent. If F is finite, then the point set of the field fibre X_k is finite.

The comparison map |X_k| → |X| has image F by Tag 03H4, so |X_k| is the union of its fibres over the finitely many points of F, and each of those is finite by AlgebraicGeometry.Space.finite_fibre_pointsMap_fst_fieldFibre once f is known to be quasi-finite at every point of F. That is condition (8) of the tag, and it follows from a finite F: decency of Y supplies a quasi-compact monomorphic representative q of the same point of |Y|, Lemma 0AC8 identifies |X_q| with F and so makes it finite, decency of X makes f a decent morphism and hence |X_q| discrete, and condition (5) for q is condition (8) for q, which is condition (8) for p because condition (8) is representative-free.

theorem finite_univ_points_fieldFibre_of_finite_setFibre_of_isDecent
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (p : FieldValuedPoint B S hS Y) (hft : IsLocallyOfFiniteType B S hS f)
    (hXdec : IsDecentSpace B S hS X)
    (hYdec : IsDecentSpace B S hS Y) (hfinite : (setFibre B S hS f p).Finite) :
    (Set.univ : Set (points B S hS (fieldFibre B S hS f p))).Finite

AlgebraicGeometry.Space.isDiscreteFieldFibrePoints_of_isZeroDimensionalFieldFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreQuasiFinite.lean, line 147. The attribute's comment: “condition (7) implies condition (5)”.

Stacks 0ACK, condition (7) implies condition (5). If the field fibre X_k has dimension zero as an algebraic space, then its point space |X_k| is discrete.

By Lemma 0ACA the structure morphism X_k ⟶ Spec(k) is then locally quasi-finite, and a space locally quasi-finite over a one-point base has discrete point space.

theorem isDiscreteFieldFibrePoints_of_isZeroDimensionalFieldFibre
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hf : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (hXk : IsAlgebraicSpace B S hS (fieldFibre B S hS f p))
    (h : IsZeroDimensionalFieldFibre B S hS f p hXk) :
    IsDiscreteFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.isZeroDimensionalFieldFibrePoints_of_isZeroDimensionalFieldFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreQuasiFinite.lean, line 164. The attribute's comment: “condition (7) implies condition (6)”.

Stacks 0ACK, condition (7) implies condition (6). If the field fibre X_k has dimension zero as an algebraic space, then its point space |X_k| has dimension zero.

No nonemptiness hypothesis is needed: the dimension of Tag 04N6 is a supremum over the points, so condition (7) already forces |X_k| to have a point.

theorem isZeroDimensionalFieldFibrePoints_of_isZeroDimensionalFieldFibre
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hf : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (hXk : IsAlgebraicSpace B S hS (fieldFibre B S hS f p))
    (h : IsZeroDimensionalFieldFibre B S hS f p hXk) :
    IsZeroDimensionalFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.isQuasiFiniteAboveFieldValuedPoint_of_isZeroDimensionalFieldFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreQuasiFinite.lean, line 235. The attribute's comment: “condition (7) implies condition (8)”.

Stacks 0ACK, condition (7) implies condition (8). If the field fibre X_k has dimension zero as an algebraic space, then f is quasi-finite at every point of |X| above the point represented by p.

By Lemma 0ACA the structure morphism X_k ⟶ Spec(k) is locally quasi-finite, hence quasi-finite at every point of |X_k|; part (2) of Tag 0ABM transports that along the projection |X_k| → |X|, whose image is exactly the fibre.

theorem isQuasiFiniteAboveFieldValuedPoint_of_isZeroDimensionalFieldFibre
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hf : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (hXk : IsAlgebraicSpace B S hS (fieldFibre B S hS f p))
    (h : IsZeroDimensionalFieldFibre B S hS f p hXk) :
    IsQuasiFiniteAboveFieldValuedPoint B S hS f p

AlgebraicGeometry.Space.isZeroDimensionalFieldFibre_of_isQuasiFiniteAboveFieldValuedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreQuasiFinite.lean, line 254. The attribute's comment: “condition (8) implies condition (7), nonempty fibre”.

Stacks 0ACK, condition (8) implies condition (7). If f is quasi-finite at every point of |X| above the point represented by p, and the field fibre X_k has a point, then X_k has dimension zero as an algebraic space.

Condition (8) makes the structure morphism X_k ⟶ Spec(k) locally quasi-finite, and Lemma 0ACA converts that into the dimension statement. The nonemptiness hypothesis is what upgrades dim(X_k) ≤ 0 to dim(X_k) = 0: the dimension of Tag 04N6 is a supremum, so the empty space has dimension ⊥.

theorem isZeroDimensionalFieldFibre_of_isQuasiFiniteAboveFieldValuedPoint
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hf : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (hXk : IsAlgebraicSpace B S hS (fieldFibre B S hS f p))
    (h : IsQuasiFiniteAboveFieldValuedPoint B S hS f p)
    (hne : Nonempty (points B S hS (fieldFibre B S hS f p))) :
    IsZeroDimensionalFieldFibre B S hS f p hXk

AlgebraicGeometry.Space.isDiscreteFieldFibrePoints_of_isQuasiFiniteAboveFieldValuedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreQuasiFinite.lean, line 278. The attribute's comment: “condition (8) implies condition (5)”.

Stacks 0ACK, condition (8) implies condition (5). If f is quasi-finite at every point of |X| above the point represented by p, then the point space |X_k| of the field fibre is discrete.

Condition (8) makes the structure morphism X_k ⟶ Spec(k) locally quasi-finite, and a space locally quasi-finite over a one-point base has discrete point space. No nonemptiness hypothesis intervenes: the empty space is discrete, and the route taken avoids the dimension of Tag 04N6, whose value on the empty space is ⊥ rather than 0.

theorem isDiscreteFieldFibrePoints_of_isQuasiFiniteAboveFieldValuedPoint
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hf : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (hXk : IsAlgebraicSpace B S hS (fieldFibre B S hS f p))
    (h : IsQuasiFiniteAboveFieldValuedPoint B S hS f p) :
    IsDiscreteFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.isDiscreteFieldFibrePoints_of_isZeroDimensionalFieldFibrePoints_of_t0Space, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 227. The attribute's comment: “(6) implies (5), corrected: the source omits that |X_k| must be Kolmogorov”.

Stacks 0ACK, condition (6) implies condition (5), for a Kolmogorov |X_k|. If the point space of the field fibre X_k is T₀ and has Krull dimension zero, then it is discrete.

This is the corrected arrow of Lemma 0ACA from condition (3) to condition (2), AlgebraicGeometry.Space.discreteTopology_points_of_topologicalKrullDim_eq_zero, applied to X_k over Spec(k): the field fibre is an algebraic space whose structure morphism is a base change of f, hence locally of finite type by Tag 03XH, and whose base is presented by the field k on the nose, so that lemma's presentation hypothesis holds by rfl.

The T₀ hypothesis is not in the source and cannot be dropped, so the source's unrestricted claim that conditions (5) and (6) are equivalent is false; see the implementation notes of this file for the counterexample. With T₀ discharged for a decent morphism this is AlgebraicGeometry.Space.isDiscreteFieldFibrePoints_of_isZeroDimensionalFieldFibrePoints.

theorem isDiscreteFieldFibrePoints_of_isZeroDimensionalFieldFibrePoints_of_t0Space
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (ht0 : T0Space (points B S hS (fieldFibre B S hS f p)))
    (h : IsZeroDimensionalFieldFibrePoints B S hS f p) :
    IsDiscreteFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.isDiscreteFieldFibrePoints_of_isZeroDimensionalFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 248. The attribute's comment: “decent morphism: condition (6) implies condition (5)”.

Stacks 0ACK, condition (6) implies condition (5), for a decent morphism. If f is a decent morphism locally of finite type and the point space of the field fibre X_k has Krull dimension zero, then |X_k| is discrete.

The field fibre of a decent morphism is a decent algebraic space, and the point space of a decent algebraic space is Kolmogorov by Stacks 03K3; that discharges the hypothesis of isDiscreteFieldFibrePoints_of_isZeroDimensionalFieldFibrePoints_of_t0Space. Decency of f is available in particular when X is a decent algebraic space, by the decent case of Stacks 0ABX.

theorem isDiscreteFieldFibrePoints_of_isZeroDimensionalFieldFibrePoints
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (hd : IsDecent B S hS f)
    (p : FieldValuedPoint B S hS Y)
    (h : IsZeroDimensionalFieldFibrePoints B S hS f p) :
    IsDiscreteFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.isZeroDimensionalFieldFibre_of_isZeroDimensionalFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 271. The attribute's comment: “(6) implies (7), corrected: the source omits that |X_k| must be Kolmogorov”.

Stacks 0ACK, condition (6) implies condition (7), for a Kolmogorov |X_k|. If the point space of the field fibre X_k is T₀ and has Krull dimension zero, then X_k has dimension zero as an algebraic space.

Condition (6) gives condition (5), and it also gives a point of |X_k|, since a space of Krull dimension zero is nonempty; those are the two inputs of AlgebraicGeometry.Space.isZeroDimensionalFieldFibre_of_isDiscreteFieldFibrePoints.

The T₀ hypothesis is not in the source and cannot be dropped; see the implementation notes of this file. It holds in particular when f is a decent morphism, by AlgebraicGeometry.Space.t0Space_points_fieldFibre_of_isDecent.

theorem isZeroDimensionalFieldFibre_of_isZeroDimensionalFieldFibrePoints
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (ht0 : T0Space (points B S hS (fieldFibre B S hS f p)))
    (hXk : IsAlgebraicSpace B S hS (fieldFibre B S hS f p))
    (h : IsZeroDimensionalFieldFibrePoints B S hS f p) :
    IsZeroDimensionalFieldFibre B S hS f p hXk

AlgebraicGeometry.Space.isQuasiFiniteAboveFieldValuedPoint_of_isZeroDimensionalFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 294. The attribute's comment: “(6) implies (8), corrected: the source omits that |X_k| must be Kolmogorov”.

Stacks 0ACK, condition (6) implies condition (8), for a Kolmogorov |X_k|. If the point space of the field fibre X_k is T₀ and has Krull dimension zero, then f is quasi-finite at every point of |X| above the point represented by p.

Condition (6) gives condition (5), which is condition (8) by AlgebraicGeometry.Space.isDiscreteFieldFibrePoints_iff_isQuasiFiniteAboveFieldValuedPoint.

The T₀ hypothesis is not in the source and cannot be dropped; see the implementation notes of this file. It holds in particular when f is a decent morphism, by AlgebraicGeometry.Space.t0Space_points_fieldFibre_of_isDecent.

theorem isQuasiFiniteAboveFieldValuedPoint_of_isZeroDimensionalFieldFibrePoints
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (ht0 : T0Space (points B S hS (fieldFibre B S hS f p)))
    (h : IsZeroDimensionalFieldFibrePoints B S hS f p) :
    IsQuasiFiniteAboveFieldValuedPoint B S hS f p

AlgebraicGeometry.Space.isDiscreteFieldFibrePoints_iff_isZeroDimensionalFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 316. The attribute's comment: “conditions (5) and (6), corrected: |X_k| must be Kolmogorov”.

Stacks 0ACK, conditions (5) and (6). For a morphism locally of finite type and a field-valued point of its target with nonempty field fibre whose point space is T₀, the point space |X_k| is discrete exactly when it has Krull dimension zero.

The nonemptiness hypothesis is carried by the direction from condition (5) alone, and it cannot be dropped there: topologicalKrullDim lands in WithBot ℕ∞, so the empty fibre is discrete while having dimension ⊥ rather than 0. The T₀ hypothesis is carried by the other direction, is not in the source, and cannot be dropped either; it holds in particular when f is a decent morphism, by AlgebraicGeometry.Space.t0Space_points_fieldFibre_of_isDecent.

theorem isDiscreteFieldFibrePoints_iff_isZeroDimensionalFieldFibrePoints
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (ht0 : T0Space (points B S hS (fieldFibre B S hS f p)))
    (hne : Nonempty (points B S hS (fieldFibre B S hS f p))) :
    IsDiscreteFieldFibrePoints B S hS f p ↔ IsZeroDimensionalFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.isZeroDimensionalFieldFibre_iff_isZeroDimensionalFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 338. The attribute's comment: “conditions (6) and (7), corrected: |X_k| must be Kolmogorov”.

Stacks 0ACK, conditions (6) and (7) for a decent morphism. For a decent morphism locally of finite type and a field-valued point of its target, the point space |X_k| of the field fibre has Krull dimension zero exactly when X_k has dimension zero as an algebraic space.

Neither direction needs a nonemptiness hypothesis: each of the two conditions is an equation … = 0 in WithBot ℕ∞ for a dimension whose value on the empty fibre is ⊥, so each already forces the fibre to have a point. The T₀ hypothesis is carried by the direction out of condition (6) alone, is not in the source, and cannot be dropped; it holds in particular when f is a decent morphism, by AlgebraicGeometry.Space.t0Space_points_fieldFibre_of_isDecent.

theorem isZeroDimensionalFieldFibre_iff_isZeroDimensionalFieldFibrePoints
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (ht0 : T0Space (points B S hS (fieldFibre B S hS f p)))
    (hXk : IsAlgebraicSpace B S hS (fieldFibre B S hS f p)) :
    IsZeroDimensionalFieldFibre B S hS f p hXk ↔ IsZeroDimensionalFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.isDiscreteSetFibre_of_isZeroDimensionalSetFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 369. The attribute's comment: “decent target: (3) implies (2), corrected: F must be Kolmogorov”.

Stacks 0ACK, condition (3) implies condition (2), for a decent target and a Kolmogorov F. Let f : X ⟶ Y be a morphism of algebraic spaces locally of finite type, let p be a field-valued point of a decent Y, and suppose the set-theoretic fibre F = f^{-1}({y}) is T₀ and has Krull dimension zero. Then F is discrete.

Decency of Y supplies a field-valued point q representing the same point of |Y| whose presenting morphism is a quasi-compact monomorphism, which is condition (4) of Stacks 03JV. For that representative Lemma 0AC8 identifies |X_q| with F as topological spaces (AlgebraicGeometry.Space.homeomorphSetFibre), and F is the same set for q as for p by AlgebraicGeometry.Space.setFibre_eq_of_class_eq. The Krull dimension of a topological space is a homeomorphism invariant, so condition (3) for p is condition (6) for q, and both the T₀ hypothesis and the resulting discreteness travel across that same homeomorphism.

The T₀ hypothesis on F is not in the source and cannot be dropped, so the source's claim that conditions (2) and (3) are equivalent for a decent target is false; see the implementation notes of this file. It is weaker than decency of f, which gives it through the homeomorphism above, and it holds in particular when X is a decent algebraic space — a hypothesis the source itself makes, in its last clause — by AlgebraicGeometry.Space.t0Space_setFibre_of_isDecentSpace_source.

theorem isDiscreteSetFibre_of_isZeroDimensionalSetFibre
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (ht0 : T0Space (setFibre B S hS f p)) (hYdec : IsDecentSpace B S hS Y)
    (h : IsZeroDimensionalSetFibre B S hS f p) :
    IsDiscreteSetFibre B S hS f p

AlgebraicGeometry.Space.isDiscreteFieldFibrePoints_of_isZeroDimensionalSetFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 394. The attribute's comment: “decent target: (3) implies (5), corrected: F must be Kolmogorov”.

Stacks 0ACK, condition (3) implies condition (5), for a decent target and a Kolmogorov F. If the set-theoretic fibre F is T₀ and has Krull dimension zero, Y is decent and f is locally of finite type, then the point space |X_k| of the field fibre is discrete.

Condition (3) gives condition (2), and conditions (2) and (5) are equivalent for a decent target by AlgebraicGeometry.Space.discreteTopology_setFibre_iff_discreteTopology_points_fieldFibre.

theorem isDiscreteFieldFibrePoints_of_isZeroDimensionalSetFibre
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (ht0 : T0Space (setFibre B S hS f p)) (hYdec : IsDecentSpace B S hS Y)
    (h : IsZeroDimensionalSetFibre B S hS f p) :
    IsDiscreteFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.isDiscreteSetFibre_iff_isZeroDimensionalSetFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 413. The attribute's comment: “decent target: conditions (2) and (3), corrected: F must be Kolmogorov”.

Stacks 0ACK, conditions (2) and (3) for a decent target and a Kolmogorov F. For a morphism locally of finite type into a decent algebraic space, and a field-valued point of the target whose set-theoretic fibre F is nonempty and T₀, the fibre F is discrete exactly when it has Krull dimension zero.

The nonemptiness hypothesis is carried by the direction from condition (2) alone, where it cannot be dropped: the empty fibre is discrete while having Krull dimension ⊥. The T₀ hypothesis is carried by the other direction, is not in the source, and cannot be dropped either.

theorem isDiscreteSetFibre_iff_isZeroDimensionalSetFibre
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (ht0 : T0Space (setFibre B S hS f p)) (hYdec : IsDecentSpace B S hS Y)
    (hne : (setFibre B S hS f p).Nonempty) :
    IsDiscreteSetFibre B S hS f p ↔ IsZeroDimensionalSetFibre B S hS f p

AlgebraicGeometry.Space.tfae_fibre_conditions_of_isDecentSpace_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 435. The attribute's comment: “decent target: conditions (2), (5), (7) and (8)”.

Stacks 0ACK, conditions (2), (5), (7) and (8) for a decent target. Let f : X ⟶ Y be a morphism of algebraic spaces locally of finite type, let Y be a decent algebraic space and let p be a field-valued point of Y with nonempty set-theoretic fibre F. Then the following are equivalent: F is discrete; |X_k| is discrete; dim(X_k) = 0; and f is quasi-finite at every point of |X| above the point p represents.

These are the four conditions of the source's decent-target clause whose equivalence holds at the hypotheses the source states, with no decency hypothesis on f. The two it omits are the Krull-dimension conditions (3) and (6), whose arrows to the others are false in that generality.

theorem tfae_fibre_conditions_of_isDecentSpace_target
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (hYdec : IsDecentSpace B S hS Y) (hne : (setFibre B S hS f p).Nonempty) :
    [IsDiscreteSetFibre B S hS f p, IsDiscreteFieldFibrePoints B S hS f p,
      IsZeroDimensionalFieldFibre B S hS f p (isAlgebraicSpace_fieldFibre hX hY f p),
      IsQuasiFiniteAboveFieldValuedPoint B S hS f p].TFAE

AlgebraicGeometry.Space.tfae_fibre_conditions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 473. The attribute's comment: “decent target: conditions (2), (3), (5), (6), (7) and (8), Kolmogorov fibres”.

Stacks 0ACK, conditions (2), (3), (5), (6), (7) and (8) for a decent target and Kolmogorov fibres. Let f : X ⟶ Y be a morphism of algebraic spaces locally of finite type, let Y be a decent algebraic space and let p be a field-valued point of Y whose set-theoretic fibre F is nonempty, with F and |X_k| both T₀. Then the following are equivalent: F is discrete; dim(F) = 0; |X_k| is discrete; dim(|X_k|) = 0; dim(X_k) = 0; and f is quasi-finite at every point of |X| above the point p represents.

This is the source's clause "if Y is decent, then conditions (2) and (3) are equivalent to each other and to conditions (5), (6), (7) and (8)", with the two Kolmogorov hypotheses that the clause needs and does not state, and with the nonemptiness that the = 0 form of the two dimension conditions needs; see the implementation notes of this file. The T₀ hypothesis on F is used only by the arrow out of condition (3) and the one on |X_k| only by the arrow out of condition (6), which are exactly the two arrows the counterexample kills. Both are weaker than decency of f, which gives them by AlgebraicGeometry.Space.t0Space_points_fieldFibre_of_isDecent and the homeomorphism of Lemma 0AC8.

theorem tfae_fibre_conditions
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (ht0F : T0Space (setFibre B S hS f p))
    (ht0k : T0Space (points B S hS (fieldFibre B S hS f p)))
    (hYdec : IsDecentSpace B S hS Y) (hne : (setFibre B S hS f p).Nonempty) :
    [IsDiscreteSetFibre B S hS f p, IsZeroDimensionalSetFibre B S hS f p,
      IsDiscreteFieldFibrePoints B S hS f p, IsZeroDimensionalFieldFibrePoints B S hS f p,
      IsZeroDimensionalFieldFibre B S hS f p (isAlgebraicSpace_fieldFibre hX hY f p),
      IsQuasiFiniteAboveFieldValuedPoint B S hS f p].TFAE

AlgebraicGeometry.Space.fibre_conditions_of_finite_setFibre_of_isDecent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FieldFibreZeroDimensionalDecent.lean, line 522. The attribute's comment: “decent spaces: condition (1) implies the other seven conditions”.

Stacks 0ACK, condition (1) implies all the other conditions, for decent spaces. Let f : X ⟶ Y be a morphism of algebraic spaces locally of finite type with X and Y both decent, and let p be a field-valued point of Y whose set-theoretic fibre F is finite and nonempty. Then |X_k| is finite, F is discrete, dim(F) = 0, |X_k| is discrete, dim(|X_k|) = 0, dim(X_k) = 0, and f is quasi-finite at every point of |X| above the point p represents — conditions (4), (2), (3), (5), (6), (7) and (8) of the tag.

Condition (4) is AlgebraicGeometry.Space.finite_univ_points_fieldFibre_of_finite_setFibre_of_isDecent. A morphism out of a decent algebraic space is a decent morphism by the decent case of Stacks 0ABX, so condition (4) gives condition (5) by AlgebraicGeometry.Space.discreteTopology_points_fieldFibre_of_finite_of_isDecent, and the remaining five conditions are condition (5) read through AlgebraicGeometry.Space.tfae_fibre_conditions.

The nonemptiness hypothesis is the one the two Krull-dimension conditions and condition (7) need: the empty fibre is finite and discrete while every … = 0 among the conditions reads ⊥ = 0 on it. It cannot be dropped, by AlgebraicGeometry.Space.not_forall_isZeroDimensionalSetFibre_of_finite_setFibre, which refutes this clause in the form the source states it, with both X and Y decent and no hypothesis on the fibre.

theorem fibre_conditions_of_finite_setFibre_of_isDecent
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hft : IsLocallyOfFiniteType B S hS f) (p : FieldValuedPoint B S hS Y)
    (hXdec : IsDecentSpace B S hS X) (hYdec : IsDecentSpace B S hS Y)
    (hne : (setFibre B S hS f p).Nonempty) (hfinite : (setFibre B S hS f p).Finite) :
    (Set.univ : Set (points B S hS (fieldFibre B S hS f p))).Finite ∧
      IsDiscreteSetFibre B S hS f p ∧ IsZeroDimensionalSetFibre B S hS f p ∧
      IsDiscreteFieldFibrePoints B S hS f p ∧
      IsZeroDimensionalFieldFibrePoints B S hS f p ∧
      IsZeroDimensionalFieldFibre B S hS f p (isAlgebraicSpace_fieldFibre hX hY f p) ∧
      IsQuasiFiniteAboveFieldValuedPoint B S hS f p

AlgebraicGeometry.Space.not_forall_isZeroDimensionalSetFibre_of_isDiscreteSetFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/EmptyFibreNotZeroDimensional.lean, line 223. The attribute's comment: “(2) => (3) is false: an empty fibre is discrete of dimension -infinity”.

The source's implication from condition (2) to condition (3) is false. There is a decent algebraic space locally of finite type over a decent algebraic space, and a field-valued point of the target, whose set-theoretic fibre is empty: that fibre is discrete and has Krull dimension -∞.

theorem not_forall_isZeroDimensionalSetFibre_of_isDiscreteSetFibre :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
        IsAlgebraicSpace B S hS Y → IsDecentSpace B S hS X → IsDecentSpace B S hS Y →
        ∀ f : X ⟶ Y, IsLocallyOfFiniteType B S hS f → ∀ p : FieldValuedPoint B S hS Y,
        IsDiscreteSetFibre B S hS f p → IsZeroDimensionalSetFibre B S hS f p

AlgebraicGeometry.Space.not_forall_isZeroDimensionalFieldFibrePoints_of_isDiscreteFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/EmptyFibreNotZeroDimensional.lean, line 238. The attribute's comment: “(5) => (6) is false: an empty field fibre is discrete of dimension -infinity”.

The source's implication from condition (5) to condition (6) is false. The field fibre over a field-valued point outside the image has no points, so its point set is discrete and has Krull dimension -∞.

theorem not_forall_isZeroDimensionalFieldFibrePoints_of_isDiscreteFieldFibrePoints :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
        IsAlgebraicSpace B S hS Y → IsDecentSpace B S hS X → IsDecentSpace B S hS Y →
        ∀ f : X ⟶ Y, IsLocallyOfFiniteType B S hS f → ∀ p : FieldValuedPoint B S hS Y,
        IsDiscreteFieldFibrePoints B S hS f p →
          IsZeroDimensionalFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.not_forall_isZeroDimensionalFieldFibre_of_isQuasiFiniteAboveFieldValuedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/EmptyFibreNotZeroDimensional.lean, line 254. The attribute's comment: “(8) => (7) is false: an empty field fibre has dimension -infinity”.

The source's implication from condition (8) to condition (7) is false. A morphism is quasi-finite above every point outside its image, while the field fibre there has no points and so has dimension -∞ in the sense of Stacks 04N6.

theorem not_forall_isZeroDimensionalFieldFibre_of_isQuasiFiniteAboveFieldValuedPoint :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
        (hY : IsAlgebraicSpace B S hS Y), IsDecentSpace B S hS X → IsDecentSpace B S hS Y →
        ∀ f : X ⟶ Y, IsLocallyOfFiniteType B S hS f → ∀ p : FieldValuedPoint B S hS Y,
        IsQuasiFiniteAboveFieldValuedPoint B S hS f p →
          IsZeroDimensionalFieldFibre B S hS f p (isAlgebraicSpace_fieldFibre hX hY f p)

AlgebraicGeometry.Space.not_forall_isZeroDimensionalSetFibre_of_finite_setFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/EmptyFibreNotZeroDimensional.lean, line 273. The attribute's comment: “decent spaces: (1) => (3) is false: an empty fibre is finite of dimension -infinity”.

The source's last clause is false. Stacks 0ACK asserts that when X and Y are decent, condition (1) implies all the other conditions; the empty fibre is finite while failing condition (3), so it does not.

This is the clause AlgebraicGeometry.Space.fibre_conditions_of_finite_setFibre_of_isDecent formalizes, and it is why that statement carries a nonemptiness hypothesis.

theorem not_forall_isZeroDimensionalSetFibre_of_finite_setFibre :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
        IsAlgebraicSpace B S hS Y → IsDecentSpace B S hS X → IsDecentSpace B S hS Y →
        ∀ f : X ⟶ Y, IsLocallyOfFiniteType B S hS f → ∀ p : FieldValuedPoint B S hS Y,
        (setFibre B S hS f p).Finite → IsZeroDimensionalSetFibre B S hS f p

AlgebraicGeometry.Space.not_forall_isDiscreteFieldFibrePoints_of_isZeroDimensionalFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/FieldFibreZeroDimensionalNotDiscrete.lean, line 197. The attribute's comment: “the unrestricted (6) => (5) is false, even for a decent target”.

The source's unrestricted implication from condition (6) to condition (5) is false. There is a morphism of algebraic spaces locally of finite type into a decent algebraic space, and a field-valued point of the target, whose field fibre has point space of Krull dimension zero and not discrete.

theorem not_forall_isDiscreteFieldFibrePoints_of_isZeroDimensionalFieldFibrePoints :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
        IsAlgebraicSpace B S hS Y → IsDecentSpace B S hS Y → ∀ f : X ⟶ Y,
        IsLocallyOfFiniteType B S hS f → ∀ p : FieldValuedPoint B S hS Y,
        (setFibre B S hS f p).Nonempty →
        IsZeroDimensionalFieldFibrePoints B S hS f p →
          IsDiscreteFieldFibrePoints B S hS f p

AlgebraicGeometry.Space.not_forall_isZeroDimensionalFieldFibre_of_isZeroDimensionalFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/FieldFibreZeroDimensionalNotDiscrete.lean, line 217. The attribute's comment: “the source's unrestricted (6) => (7) is false, even for a decent target”.

The source's unrestricted implication from condition (6) to condition (7) is false. Condition (7) implies condition (5) with no further hypothesis, which condition (6) does not.

theorem not_forall_isZeroDimensionalFieldFibre_of_isZeroDimensionalFieldFibrePoints :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
        (hY : IsAlgebraicSpace B S hS Y), IsDecentSpace B S hS Y → ∀ f : X ⟶ Y,
        IsLocallyOfFiniteType B S hS f → ∀ p : FieldValuedPoint B S hS Y,
        (setFibre B S hS f p).Nonempty →
        IsZeroDimensionalFieldFibrePoints B S hS f p →
          IsZeroDimensionalFieldFibre B S hS f p (isAlgebraicSpace_fieldFibre hX hY f p)

AlgebraicGeometry.Space.not_forall_isQuasiFiniteAboveFieldValuedPoint_of_isZeroDimensionalFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/FieldFibreZeroDimensionalNotDiscrete.lean, line 235. The attribute's comment: “the source's unrestricted (6) => (8) is false, even for a decent target”.

The source's unrestricted implication from condition (6) to condition (8) is false. Conditions (5) and (8) are equivalent with no further hypothesis, and condition (6) implies neither.

theorem not_forall_isQuasiFiniteAboveFieldValuedPoint_of_isZeroDimensionalFieldFibrePoints :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
        IsAlgebraicSpace B S hS Y → IsDecentSpace B S hS Y → ∀ f : X ⟶ Y,
        IsLocallyOfFiniteType B S hS f → ∀ p : FieldValuedPoint B S hS Y,
        (setFibre B S hS f p).Nonempty →
        IsZeroDimensionalFieldFibrePoints B S hS f p →
          IsQuasiFiniteAboveFieldValuedPoint B S hS f p

AlgebraicGeometry.Space.not_forall_isDiscreteFieldFibrePoints_iff_isZeroDimensionalFieldFibrePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/FieldFibreZeroDimensionalNotDiscrete.lean, line 252. The attribute's comment: “the row (5) <=> (6) <=> (7) <=> (8) is false as stated”.

The source's equivalence of conditions (5) and (6) is false. This is the negation of that equivalence, in the source's own vocabulary.

theorem not_forall_isDiscreteFieldFibrePoints_iff_isZeroDimensionalFieldFibrePoints :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
        IsAlgebraicSpace B S hS Y → IsDecentSpace B S hS Y → ∀ f : X ⟶ Y,
        IsLocallyOfFiniteType B S hS f → ∀ p : FieldValuedPoint B S hS Y,
        (setFibre B S hS f p).Nonempty →
        (IsDiscreteFieldFibrePoints B S hS f p ↔
          IsZeroDimensionalFieldFibrePoints B S hS f p)

AlgebraicGeometry.Space.not_forall_isDiscreteSetFibre_of_isZeroDimensionalSetFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/FieldFibreZeroDimensionalNotDiscrete.lean, line 293. The attribute's comment: “the decent-target clause's (3) => (2) is false”.

The source's implication from condition (3) to condition (2) for a decent target is false. There is a morphism of algebraic spaces locally of finite type into a decent algebraic space, and a field-valued point of the target, whose set-theoretic fibre has Krull dimension zero and is not discrete.

theorem not_forall_isDiscreteSetFibre_of_isZeroDimensionalSetFibre :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
        IsAlgebraicSpace B S hS Y → IsDecentSpace B S hS Y → ∀ f : X ⟶ Y,
        IsLocallyOfFiniteType B S hS f → ∀ p : FieldValuedPoint B S hS Y,
        (setFibre B S hS f p).Nonempty →
        IsZeroDimensionalSetFibre B S hS f p → IsDiscreteSetFibre B S hS f p

AlgebraicGeometry.Space.not_forall_isDiscreteSetFibre_iff_isZeroDimensionalSetFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/FieldFibreZeroDimensionalNotDiscrete.lean, line 312. The attribute's comment: “the decent-target clause's (2) <=> (3) is false as stated”.

The source's equivalence of conditions (2) and (3) for a decent target is false. This is the negation of that equivalence, in the source's own vocabulary.

theorem not_forall_isDiscreteSetFibre_iff_isZeroDimensionalSetFibre :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
        IsAlgebraicSpace B S hS Y → IsDecentSpace B S hS Y → ∀ f : X ⟶ Y,
        IsLocallyOfFiniteType B S hS f → ∀ p : FieldValuedPoint B S hS Y,
        (setFibre B S hS f p).Nonempty →
        (IsDiscreteSetFibre B S hS f p ↔ IsZeroDimensionalSetFibre B S hS f p)

Sources

• Section 68.18, Tag 0AC0
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.PointsFibresDiagram · AlgebraicGeometry.Space.fibrePoints · AlgebraicGeometry.Space.fibreSpectrumEquiv · AlgebraicGeometry.Space.fibreSpectrumEquiv_symm_apply · AlgebraicGeometry.Space.finite_fibrePoints_of_finite_residueField_left · AlgebraicGeometry.Space.finite_fibrePoints_of_finite_residueField_right · AlgebraicGeometry.Space.finite_fibrePoints_of_quasiFiniteAt · AlgebraicGeometry.Space.exists_isPullback_twistedLineQuotient

Section68.19 Monomorphisms#

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

Tag 06RZ, a lemma

Tag 06RZ in the Stacks Project.

AlgebraicGeometry.Space.relativelyRepresentable_of_mono_to_coproduct_spec_zeroDimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MonoToZeroDimensionalLocalSpectra.lean, line 208.

Stacks 06RZ. A monomorphism of algebraic spaces over S whose target is a disjoint union of spectra of zero-dimensional local rings is representable; equivalently its source is a scheme.

theorem relativelyRepresentable_of_mono_to_coproduct_spec_zeroDimensional
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F) (f : F ⟶ G)
    [Mono f] (Y : BigFppfOver B S hS) (eG : G ≅ yoneda.obj Y) (I : Type u)
    (A : I → CommRingCat.{u}) (hlocal : ∀ i, IsLocalRing (A i))
    (hdim : ∀ i, ringKrullDim (A i) = 0)
    (eY : (BigFppfOver.toScheme B S hS).obj Y ≅ ∐ fun i : I ↦ Spec (A i)) :
    yoneda.relativelyRepresentable f

Sources

• Section 68.19, Tag 06RY
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.relativelyRepresentable_of_mono_to_coproduct_spec_zeroDimensional

Section68.20 Generic points#

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

Tag 0ABV, a lemma

Tag 0ABV in the Stacks Project.

AlgebraicGeometry.Space.mem_genericPoints_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/CodimensionZeroCriterion.lean, line 165.

Stacks 0ABV. For a point x of a decent algebraic space X over S the following are equivalent: x is a generic point of an irreducible component of |X|; for every étale morphism of algebraic spaces onto X, every point above x is a generic point of an irreducible component of the source; for some étale morphism onto X some point above x is; and the local ring of X at x has dimension zero, which is to say that x is a point of codimension 0 on X.

theorem mem_genericPoints_tfae (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) (x : points B S hS X) :
    List.TFAE
      [ x ∈ genericPoints (points B S hS X),
        ∀ (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS Y → ∀ f : Y ⟶ X,
          IsEtale B S hS f → ∀ y : points B S hS Y, pointsMap B S hS Y f y = x →
            y ∈ genericPoints (points B S hS Y),
        ∃ (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Y) (f : Y ⟶ X)
          (y : points B S hS Y), IsEtale B S hS f ∧ pointsMap B S hS Y f y = x ∧
            y ∈ genericPoints (points B S hS Y),
        localRingDimension B S hS x = 0 ]

Tag 0ED1, a lemma

Tag 0ED1 in the Stacks Project.

AlgebraicGeometry.Space.codimension_eq_localRingDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/CodimensionLocalRing.lean, line 85.

For an irreducible closed subset T of the point space of a decent algebraic space over S, with generic point ξ, the codimension of T is the dimension of the local ring of the space at ξ.

theorem codimension_eq_localRingDimension (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) (T : IrreducibleCloseds (points B S hS X))
    (ξ : points B S hS X) (hξ : IsGenericPoint ξ (T : Set (points B S hS X))) :
    codimension T = localRingDimension B S hS ξ

Tag 0BB8, a lemma

Tag 0BB8 in the Stacks Project.

AlgebraicGeometry.Space.isReasonableSpace_of_finite_irreducibleComponents_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReasonableFromGenericPoints.lean, line 358.

Stacks 0BB8. An algebraic space over a scheme S is reasonable as soon as every quasi-compact scheme étale over it has finitely many irreducible components and every one of its points of codimension zero is represented by a monomorphism from the spectrum of a field.

theorem isReasonableSpace_of_finite_irreducibleComponents_of_mono
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hfinite : ∀ U : BigFppfOver B S hS,
      CompactSpace ((BigFppfOver.toScheme B S hS).obj U) →
      ∀ f : yoneda.obj U ⟶ X,
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@_root_.AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) f →
        (irreducibleComponents ((BigFppfOver.toScheme B S hS).obj U)).Finite)
    (hgeneric : ∀ x : points B S hS X, localRingDimension B S hS x = 0 →
      ∃ p : FieldValuedPoint B S hS X,
        p.class B S hS X = x ∧ Mono (yonedaEquiv.symm p.value)) :
    IsReasonableSpace B S hS X

Tag 0BB9, a lemma

Tag 0BB9 in the Stacks Project.

AlgebraicGeometry.Space.IsDecentWithFinitelyManyComponents.hasMonomorphicCodimensionZeroPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 388. The attribute's comment: “condition (1) implies the third clause of condition (2)”.

Stacks 0BB9, condition (1) implies the third clause of condition (2). A decent algebraic space has a monomorphic field-valued representative at every point, in particular at every point of codimension 0.

theorem IsDecentWithFinitelyManyComponents.hasMonomorphicCodimensionZeroPoints
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (h : IsDecentWithFinitelyManyComponents B S hS X) :
    HasMonomorphicCodimensionZeroPoints B S hS X

AlgebraicGeometry.Space.HasQuasiCompactGenericDenseOpenScheme.hasFiniteEtaleIrreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 510. The attribute's comment: “condition (3) implies the first clause of condition (2)”.

Stacks 0BB9, condition (3) implies the first clause of condition (2). If an algebraic space over S has a dense open subspace which is a scheme with finitely many irreducible components whose generic points are represented by quasi-compact morphisms, then every quasi-compact scheme étale over it has finitely many irreducible components.

Let a : U ⟶ X be étale with U compact, and let V ⊂ U be the preimage of the point set of the open subspace: it is open, and dense because an étale morphism is open on points. A generic point of an irreducible component of U lying in V has codimension 0 on X by condition (2) of Stacks 0BAQ, so its image is the image of a generic point of the open subspace; there are finitely many of those, and the fibre of |U| → |X| above each is finite because the morphism representing it is quasi-compact. So V meets only finitely many generic points, which bounds the irreducible components of U.

theorem HasQuasiCompactGenericDenseOpenScheme.hasFiniteEtaleIrreducibleComponents
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (h : HasQuasiCompactGenericDenseOpenScheme B S hS X) :
    HasFiniteEtaleIrreducibleComponents B S hS X

AlgebraicGeometry.Space.HasQuasiCompactGenericDenseOpenScheme.hasFiniteCodimensionZeroPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 612. The attribute's comment: “condition (3) implies the second clause of condition (2)”.

Stacks 0BB9, condition (3) implies the second clause of condition (2). Only finitely many points have codimension 0: each of them lies over the dense open subspace, and is the image of a generic point of one of its finitely many irreducible components.

theorem HasQuasiCompactGenericDenseOpenScheme.hasFiniteCodimensionZeroPoints
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (h : HasQuasiCompactGenericDenseOpenScheme B S hS X) :
    HasFiniteCodimensionZeroPoints B S hS X

AlgebraicGeometry.Space.HasQuasiCompactGenericDenseOpenScheme.hasMonomorphicCodimensionZeroPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 632. The attribute's comment: “condition (3) implies the third clause of condition (2)”.

Stacks 0BB9, condition (3) implies the third clause of condition (2). A point of codimension 0 lies over the dense open subspace, which is a scheme, so the residue field at the corresponding point of that scheme presents it by a monomorphism.

theorem HasQuasiCompactGenericDenseOpenScheme.hasMonomorphicCodimensionZeroPoints
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (h : HasQuasiCompactGenericDenseOpenScheme B S hS X) :
    HasMonomorphicCodimensionZeroPoints B S hS X

AlgebraicGeometry.Space.HasQuasiCompactGenericDenseOpenScheme.hasFiniteEtaleComponentsAndCodimensionZeroPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 645. The attribute's comment: “condition (3) implies condition (2)”.

Stacks 0BB9, condition (3) implies condition (2). The three clauses together.

theorem HasQuasiCompactGenericDenseOpenScheme.hasFiniteEtaleComponentsAndCodimensionZeroPoints
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (h : HasQuasiCompactGenericDenseOpenScheme B S hS X) :
    HasFiniteEtaleComponentsAndCodimensionZeroPoints B S hS X

AlgebraicGeometry.Space.IsDecentWithFinitelyManyComponents.hasQuasiCompactGenericDenseOpenScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 720. The attribute's comment: “condition (1) implies condition (3)”.

Stacks 0BB9, condition (1) implies condition (3). A decent algebraic space over S whose space of points has finitely many irreducible components has a dense open subspace which is a scheme, with finitely many irreducible components, each of whose generic points is represented by a quasi-compact morphism from the spectrum of a field.

The dense open subscheme is Stacks 086U, in the form AlgebraicGeometry.Space.exists_denseRange_isRepresentable_isOpenSubspace_of_isDecentSpace. Its components are finite in number because the inclusion is an open embedding on points and an open embedding pulls components back onto components (AlgebraicGeometry.finite_irreducibleComponents_of_isOpenEmbedding), which is the source's "taking closures sends irreducible components of |X'| to irreducible components of |X|". The quasi-compactness of the generic-point morphisms is decency itself, with the monomorphism condition of Stacks 03JV (4) dropped to Stacks 03JV (5).

theorem IsDecentWithFinitelyManyComponents.hasQuasiCompactGenericDenseOpenScheme
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (h : IsDecentWithFinitelyManyComponents B S hS X) :
    HasQuasiCompactGenericDenseOpenScheme B S hS X

AlgebraicGeometry.Space.HasFiniteEtaleComponentsAndCodimensionZeroPoints.isReasonableSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 740. The attribute's comment: “condition (2) implies the conclusion that the space is reasonable”.

Condition (2) of Stacks 0BB9 makes the algebraic space reasonable. This is Stacks 0BB8, AlgebraicGeometry.Space.isReasonableSpace_of_finite_irreducibleComponents_of_mono, whose two hypotheses are the first and third clauses of condition (2).

theorem HasFiniteEtaleComponentsAndCodimensionZeroPoints.isReasonableSpace
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (h : HasFiniteEtaleComponentsAndCodimensionZeroPoints B S hS X) :
    IsReasonableSpace B S hS X

AlgebraicGeometry.Space.HasFiniteEtaleComponentsAndCodimensionZeroPoints.isDecentWithFinitelyManyComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 755. The attribute's comment: “condition (2) implies condition (1)”.

Stacks 0BB9, condition (2) implies condition (1). Decency comes from Stacks 0BB8: the first and third clauses of condition (2) make the space reasonable, and a reasonable algebraic space is decent. Finiteness of the irreducible components of |X| comes from the second clause together with Stacks 0BAR: the points of codimension 0 are dense, there are finitely many of them, and so the finitely many irreducible closed sets they generate cover a dense subset of |X|, which bounds the components.

theorem HasFiniteEtaleComponentsAndCodimensionZeroPoints.isDecentWithFinitelyManyComponents
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (h : HasFiniteEtaleComponentsAndCodimensionZeroPoints B S hS X) :
    IsDecentWithFinitelyManyComponents B S hS X

AlgebraicGeometry.Space.isDecentWithFinitelyManyComponents_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 777.

Stacks 0BB9. For an algebraic space X over a scheme S the three conditions are equivalent: X is decent with finitely many irreducible components; every quasi-compact scheme étale over X has finitely many irreducible components, there are finitely many points of codimension 0 and each is represented by a monomorphism from the spectrum of a field; and there is a dense open subspace which is a scheme with finitely many irreducible components whose generic points are represented by quasi-compact morphisms.

theorem isDecentWithFinitelyManyComponents_tfae
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) :
    [IsDecentWithFinitelyManyComponents B S hS X,
      HasFiniteEtaleComponentsAndCodimensionZeroPoints B S hS X,
      HasQuasiCompactGenericDenseOpenScheme B S hS X].TFAE

AlgebraicGeometry.Space.IsDecentWithFinitelyManyComponents.isReasonableSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 791. The attribute's comment: “the conclusion that the space is reasonable”.

Stacks 0BB9, the concluding assertion that the space is reasonable. An algebraic space over S which is decent and has finitely many irreducible components is reasonable.

theorem IsDecentWithFinitelyManyComponents.isReasonableSpace
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (h : IsDecentWithFinitelyManyComponents B S hS X) :
    IsReasonableSpace B S hS X

AlgebraicGeometry.Space.image_genericPoints_eq_genericPoints_of_denseRange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericPointsFiniteComponents.lean, line 808. The attribute's comment: “the conclusion identifying the generic points of the dense open subscheme”.

Stacks 0BB9, the concluding assertion about generic points. If the space of points of an algebraic space over S has finitely many irreducible components and X' ⊂ X is an open subspace whose point set is dense, then the generic points of the irreducible components of |X'| map exactly onto the generic points of the irreducible components of |X|.

The inclusion is an open embedding on points, and an open embedding matches up the generic points of its source with those of its target lying in its range; the range is all of them because a dense open subset of a space with finitely many irreducible components contains every generic point.

theorem image_genericPoints_eq_genericPoints_of_denseRange
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {G : Subfunctor X} (hG : IsOpenSubspace B S hS G)
    (hdense : DenseRange (pointsMap B S hS G.toFunctor G.ι))
    (hfin : (irreducibleComponents (points B S hS X)).Finite) :
    pointsMap B S hS G.toFunctor G.ι '' genericPoints (points B S hS G.toFunctor) =
      genericPoints (points B S hS X)

Sources

• Section 68.20, Tag 0BB7
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.mem_genericPoints_tfae · AlgebraicGeometry.Space.codimension_eq_localRingDimension · AlgebraicGeometry.Space.isReasonableSpace_of_finite_irreducibleComponents_of_mono · AlgebraicGeometry.Space.IsDecentWithFinitelyManyComponents.hasMonomorphicCodimensionZeroPoints · AlgebraicGeometry.Space.HasQuasiCompactGenericDenseOpenScheme.hasFiniteEtaleIrreducibleComponents · AlgebraicGeometry.Space.HasQuasiCompactGenericDenseOpenScheme.hasFiniteCodimensionZeroPoints · AlgebraicGeometry.Space.HasQuasiCompactGenericDenseOpenScheme.hasMonomorphicCodimensionZeroPoints · AlgebraicGeometry.Space.HasQuasiCompactGenericDenseOpenScheme.hasFiniteEtaleComponentsAndCodimensionZeroPoints

Section68.21 Generically finite morphisms#

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

Tag 0ACZ, a lemma

Tag 0ACZ in the Stacks Project.

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

Stacks 0ACZ, conditions (1) and (2). Let f : X ⟶ Y be a quasi-separated morphism of algebraic spaces over S of finite type and let p be a field-valued representative of a point y of |Y|. The field fibre X_k has finitely many points exactly when f is quasi-finite at every point of |X| above y.

theorem finite_fieldFiber_iff_quasiFiniteAt_fiber (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hqs : IsQuasiSeparated B S hS f)
    (hft : IsFiniteType B S hS f) (y : points B S hS Y)
    (p : FieldValuedPoint B S hS Y) (hp : p.class B S hS Y = y) :
    Set.Finite (Set.univ : Set (points B S hS
        (pullback f (yonedaEquiv.symm p.value)))) ↔
      ∀ x : points B S hS X, pointsMap B S hS X f x = y →
        IsQuasiFiniteAt B S hS f x

AlgebraicGeometry.Space.finite_fieldFiber_iff_finite_setFiber_of_decent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericallyFinite.lean, line 515. The attribute's comment: “condition (4) for a decent target”.

Stacks 0ACZ, condition (4) for a decent target. Let f : X ⟶ Y be a quasi-separated morphism of algebraic spaces over S of finite type with Y a decent algebraic space, and let p be a field-valued representative of a point y of |Y|. The field fibre X_k has finitely many points exactly when the set-theoretic fibre f^{-1}({y}) ⊂ |X| is finite.

theorem finite_fieldFiber_iff_finite_setFiber_of_decent (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hqs : IsQuasiSeparated B S hS f)
    (hft : IsFiniteType B S hS f) (hdecent : IsDecentSpace B S hS Y)
    (y : points B S hS Y) (p : FieldValuedPoint B S hS Y)
    (hp : p.class B S hS Y = y) :
    Set.Finite (Set.univ : Set (points B S hS
        (pullback f (yonedaEquiv.symm p.value)))) ↔
      Set.Finite {x : points B S hS X | pointsMap B S hS X f x = y}

AlgebraicGeometry.Space.exists_isOpenSubspace_isFinite_pullback_snd_of_finite_fieldFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericallyFinite.lean, line 1360. The attribute's comment: “conditions (1) and (2) imply condition (3)”.

Stacks 0ACZ, conditions (1) and (2) imply condition (3). Let f : X ⟶ Y be a quasi-separated morphism of algebraic spaces over S of finite type, let y be a point of |Y| whose local ring has dimension zero and let p be a field-valued representative of y with field of definition k. If the field fibre X_k = X ×_Y Spec(k) has finitely many points then there is an open subspace V ⊂ Y with y ∈ |V| whose base change V ×_Y X ⟶ V is finite.

An affine étale chart V ⟶ Y at y may be chosen so that y comes from a generic point v of V (Stacks 0BAQ). Over an affine étale atlas U of V ×_Y X the two morphisms U ⟶ V and U ×_{V ×_Y X} U ⟶ V are quasi-finite above v (Stacks 0BBB), so both become finite after shrinking V to an affine open neighbourhood of v (Stacks 02NW). The relation being finite over the atlas makes the atlas finite over the shrunk chart, and the chart being affine with a finite surjective atlas makes V ×_Y X an affine scheme (Stacks 01ZT), over which finiteness is properness together with affineness. Descending along the étale chart produces the open subspace of Y.

theorem exists_isOpenSubspace_isFinite_pullback_snd_of_finite_fieldFiber
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hqs : IsQuasiSeparated B S hS f)
    (hft : IsFiniteType B S hS f)
    (y : points B S hS Y)
    (p : FieldValuedPoint B S hS Y)
    (hp : p.class B S hS Y = y)
    (hy : localRingDimension B S hS y = 0) :
    Set.Finite (Set.univ : Set (points B S hS
      (pullback f (yonedaEquiv.symm p.value)))) →
    ∃ 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.ι)

AlgebraicGeometry.Space.isQuasiFiniteAt_of_isFinite_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericallyFinite.lean, line 1401. The attribute's comment: “condition (3) implies condition (2)”.

Stacks 0ACZ, condition (3) implies condition (2). Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type and let V ⊂ Y be an open subspace containing a point y of |Y| in its point set. If the base change V ×_Y X ⟶ V is finite then f is quasi-finite at every point of |X| above y.

A finite morphism is quasi-finite (Stacks 04NY), so V ×_Y X ⟶ V is quasi-finite at every point of its source; a point of |X| above y lifts to |V ×_Y X| (Stacks 03H4), and quasi-finiteness at a point passes to and from a base change (Stacks 0ABM).

theorem isQuasiFiniteAt_of_isFinite_pullback_snd
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hlft : IsLocallyOfFiniteType B S hS f)
    (y : points B S hS Y)
    (V : Subfunctor Y)
    (hV : IsOpenSubspace B S hS V)
    (hyV : y ∈ Set.range (pointsMap B S hS V.toFunctor V.ι))
    (hfin : IsFinite B S hS (pullback.snd f V.ι))
    (x : points B S hS X)
    (hxy : pointsMap B S hS X f x = y) :
    IsQuasiFiniteAt B S hS f x

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

Stacks 0ACZ, conditions (1) and (3). Let f : X ⟶ Y be a quasi-separated morphism of algebraic spaces over S of finite type, let y be a point of |Y| whose local ring has dimension zero and let p be a field-valued representative of y. The field fibre X_k has finitely many points exactly when there is an open subspace V ⊂ Y with y ∈ |V| whose base change V ×_Y X ⟶ V is finite.

Together with AlgebraicGeometry.Space.finite_fieldFiber_iff_quasiFiniteAt_fiber this closes the equivalence of the source's conditions (1), (2) and (3).

theorem finite_fieldFiber_iff_exists_isOpenSubspace_isFinite_pullback_snd
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hqs : IsQuasiSeparated B S hS f)
    (hft : IsFiniteType B S hS f)
    (y : points B S hS Y)
    (p : FieldValuedPoint B S hS Y)
    (hp : p.class B S hS Y = y)
    (hy : localRingDimension B S hS y = 0) :
    Set.Finite (Set.univ : Set (points B S hS
        (pullback f (yonedaEquiv.symm p.value)))) ↔
      ∃ 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 0AD0, a lemma

Tag 0AD0 in the Stacks Project.

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

Stacks 0AD0, the equivalence of conditions (1) and (2). Let f : X ⟶ Y be a quasi-separated morphism of algebraic spaces over S which is locally of finite type, let Y be a quasi-separated algebraic space, let y be a point of |Y| of codimension zero and let p be a field-valued representative of y, with field of definition k. Then the set-theoretic fibre f^{-1}({y}) ⊂ |X| is finite exactly when the point set of the field fibre X_k = X ×_Y Spec(k) is finite.

Quasi-separatedness of Y makes Y decent (Stacks 03JX) and quasi-separatedness of f then makes X decent (Stacks 03M5 and Stacks 0ABY), so both implications are instances of the comparison of conditions (1) and (4) of Stacks 0ACK for decent source and target: condition (4) implies condition (1) because the comparison map |X_k| → |X| has image the set-theoretic fibre, and the converse is AlgebraicGeometry.Space.finite_univ_points_fieldFibre_of_finite_setFibre_of_isDecent once the fibre is nonempty, an empty fibre leaving |X_k| without points by the same surjectivity.

The codimension-zero hypothesis on y is the source's; this implication does not use it.

theorem finite_setFibre_iff_finite_fieldFibre_of_isAbsolutelyQuasiSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hqs : IsQuasiSeparated B S hS f) (hft : IsLocallyOfFiniteType B S hS f)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    (y : points B S hS Y) (_hy : localRingDimension B S hS y = 0)
    (p : FieldValuedPoint B S hS Y) (hp : p.class B S hS Y = y) :
    {x : points B S hS X | pointsMap B S hS X f x = y}.Finite ↔
      (Set.univ : Set (points B S hS (fieldFibre B S hS f p))).Finite

AlgebraicGeometry.Space.finite_setFibre_of_isFinite_openRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericallyFiniteQuasiSeparated.lean, line 193. The attribute's comment: “condition (3) implies condition (1)”.

Stacks 0AD0, condition (3) implies condition (1). Let f : X ⟶ Y be a morphism of presheaves on the big fppf site of S, let y be a point of |Y|, let U ⊂ X and V ⊂ Y be open subspaces and let g : U ⟶ V be a morphism whose square with the two inclusions and f commutes, so that f carries U into V and g restricts f. If y lies in |V|, if the set-theoretic fibre f^{-1}({y}) ⊂ |X| is contained in |U| and if g is finite, then f^{-1}({y}) is finite.

A finite morphism of algebraic spaces is universally closed with discrete fibres (Stacks 0A4X), so each of its set-theoretic fibres is finite. The inclusion |V| → |Y| is injective because the inclusion of an open subspace is a monomorphism, so the point v of |V| above y is the only one, and a point of |U| lands on y under f exactly when it lands on v under g. The fibre f^{-1}({y}) is therefore the image under |U| → |X| of a fibre of g.

No hypothesis on f, on Y or on y is needed: the quasi-separatedness, finite type and codimension-zero hypotheses of the tag are used only for the other implications.

theorem finite_setFibre_of_isFinite_openRestriction (f : X ⟶ Y) (y : points B S hS Y)
    (U : Subfunctor X) (V : Subfunctor Y) (g : U.toFunctor ⟶ V.toFunctor)
    (hU : IsOpenSubspace B S hS U) (hV : IsOpenSubspace B S hS V)
    (hcomm : g ≫ V.ι = U.ι ≫ f)
    (hy : y ∈ Set.range (pointsMap B S hS V.toFunctor V.ι))
    (hfib : {x : points B S hS X | pointsMap B S hS X f x = y} ⊆
      Set.range (pointsMap B S hS U.toFunctor U.ι))
    (hg : IsFinite B S hS g) :
    {x : points B S hS X | pointsMap B S hS X f x = y}.Finite

AlgebraicGeometry.Space.finite_fieldFibre_of_isFinite_openRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericallyFiniteQuasiSeparated.lean, line 231. The attribute's comment: “condition (3) implies condition (2)”.

Stacks 0AD0, condition (3) implies condition (2). In the situation of condition (3) of the tag, with f in addition quasi-separated and locally of finite type and Y a quasi-separated algebraic space, the point set of the field fibre X_k over a field-valued representative p of y is finite.

The source omits the proof of this implication. It is obtained here by composing AlgebraicGeometry.Space.finite_setFibre_of_isFinite_openRestriction with the equivalence of conditions (1) and (2).

theorem finite_fieldFibre_of_isFinite_openRestriction (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hqs : IsQuasiSeparated B S hS f) (hft : IsLocallyOfFiniteType B S hS f)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    (y : points B S hS Y) (hy0 : localRingDimension B S hS y = 0)
    (p : FieldValuedPoint B S hS Y) (hp : p.class B S hS Y = y)
    (U : Subfunctor X) (V : Subfunctor Y) (g : U.toFunctor ⟶ V.toFunctor)
    (hU : IsOpenSubspace B S hS U) (hV : IsOpenSubspace B S hS V)
    (hcomm : g ≫ V.ι = U.ι ≫ f)
    (hy : y ∈ Set.range (pointsMap B S hS V.toFunctor V.ι))
    (hfib : {x : points B S hS X | pointsMap B S hS X f x = y} ⊆
      Set.range (pointsMap B S hS U.toFunctor U.ι))
    (hg : IsFinite B S hS g) :
    (Set.univ : Set (points B S hS (fieldFibre B S hS f p))).Finite

AlgebraicGeometry.Space.exists_isOpenSubspace_isFinite_openRestriction_of_finite_setFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericallyFiniteQuasiSeparated.lean, line 447. The attribute's comment: “conditions (1) and (2) imply condition (3)”.

Stacks 0AD0, conditions (1) and (2) imply condition (3). Let f : X ⟶ Y be a quasi-separated morphism of algebraic spaces over S which is locally of finite type, let Y be a quasi-separated algebraic space and let y be a point of |Y| whose local ring has dimension zero. If the set-theoretic fibre f^{-1}({y}) ⊂ |X| is finite then there are open subspaces U ⊂ X and V ⊂ Y and a morphism g : U ⟶ V restricting f, with y ∈ |V|, with f^{-1}({y}) ⊂ |U|, and with g finite.

A finite set of points of an algebraic space is covered by a quasi-compact open subspace, so X may be shrunk to a quasi-compact open U₀ containing the fibre. Quasi-separatedness of Y makes the restriction U₀ ⟶ Y quasi-compact (Stacks 073B) and hence of finite type, and its fibre over y is still finite, so the field fibre is finite as well. Condition (3) of Stacks 0ACZ then supplies an open V ⊂ Y containing y over which U₀ becomes finite, and the base change U₀ ×_Y V is an open subspace of X because U₀ is.

theorem exists_isOpenSubspace_isFinite_openRestriction_of_finite_setFibre
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hqs : IsQuasiSeparated B S hS f)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    (y : points B S hS Y)
    (hy : localRingDimension B S hS y = 0) :
    Set.Finite {x : points B S hS X |
      pointsMap B S hS X f x = y} →
      ∃ (U : Subfunctor X) (V : Subfunctor Y)
        (g : U.toFunctor ⟶ V.toFunctor),
        IsOpenSubspace B S hS U ∧
        IsOpenSubspace B S hS V ∧
        g ≫ V.ι = U.ι ≫ f ∧
        y ∈ Set.range (pointsMap B S hS V.toFunctor V.ι) ∧
        {x : points B S hS X |
          pointsMap B S hS X f x = y} ⊆
          Set.range (pointsMap B S hS U.toFunctor U.ι) ∧
        IsFinite B S hS g

Tag 0BBB, a lemma

Tag 0BBB in the Stacks Project.

AlgebraicGeometry.Space.quasiFiniteAt_over_codimensionZeroPoint_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GenericallyFinite.lean, line 293.

Stacks 0BBB. Let f : X ⟶ Y be a morphism of algebraic spaces over S locally of finite type and let y be a point of Y whose local ring has dimension zero. The following are equivalent: every point of X above y has local ring of dimension zero; f is quasi-finite at every point above y; and f is quasi-finite at every point above y whose local ring has dimension zero.

theorem quasiFiniteAt_over_codimensionZeroPoint_tfae
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    (y : points B S hS Y) (hy : localRingDimension B S hS y = 0) :
    List.TFAE [
      ∀ x : points B S hS X, pointsMap B S hS X f x = y →
        localRingDimension B S hS x = 0,
      ∀ x : points B S hS X, pointsMap B S hS X f x = y → IsQuasiFiniteAt B S hS f x,
      ∀ x : points B S hS X, localRingDimension B S hS x = 0 →
        pointsMap B S hS X f x = y → IsQuasiFiniteAt B S hS f x]

Tag 0BBC, a lemma

Tag 0BBC in the Stacks Project.

AlgebraicGeometry.Space.exists_isDenseOpenSubspace_isFinite_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteOverDenseOpenSubspace.lean, line 233.

Stacks 0BBC. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, and write X⁰ and Y⁰ for the sets of points of |X| and |Y| whose local rings have dimension zero. Assume that Y is decent, that X⁰ and Y⁰ are finite with f^{-1}(Y⁰) = X⁰, and that f is either quasi-compact or separated. Then there is an open subspace V ⊂ Y whose set of points is dense in |Y| and over which f becomes finite.

The hypothesis f^{-1}(Y⁰) = X⁰ makes the fibre of f over a point of codimension zero of Y finite, so over a suitable neighbourhood of such a point f is finite: if f is quasi-compact this is condition (3) of Stacks 0ACZ, and if f is separated it is condition (3) of Stacks 0AD0 together with the vanishing of the complementary open, which carries no point of codimension zero and is therefore empty by Stacks 0BAR. Since Y⁰ is finite, finitely many such neighbourhoods are glued, and the result is dense because it contains Y⁰.

theorem exists_isDenseOpenSubspace_isFinite_pullback_snd
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hlft : IsLocallyOfFiniteType B S hS f)
    (hYdecent : IsDecentSpace B S hS Y)
    (hXzero : Set.Finite {x : points B S hS X |
      localRingDimension B S hS x = 0})
    (hYzero : Set.Finite {y : points B S hS Y |
      localRingDimension B S hS y = 0})
    (hpreimage :
      (pointsMap B S hS X f) ⁻¹'
        {y : points B S hS Y |
          localRingDimension B S hS y = 0} =
        {x : points B S hS X |
          localRingDimension B S hS x = 0})
    (hqc_or_sep : IsQuasiCompact B S hS f ∨
      IsSeparated B S hS f) :
    letI : TopologicalSpace (points B S hS Y) :=
      pointTopology B S hS Y
    ∃ V : Subfunctor Y,
      IsOpenSubspace B S hS V ∧
        Dense (Set.range (pointsMap B S hS V.toFunctor V.ι)) ∧
          IsFinite B S hS (pullback.snd f V.ι)

Sources

• Section 68.21, Tag 0BBA
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.finite_fieldFiber_iff_quasiFiniteAt_fiber · AlgebraicGeometry.Space.finite_fieldFiber_iff_finite_setFiber_of_decent · AlgebraicGeometry.Space.exists_isOpenSubspace_isFinite_pullback_snd_of_finite_fieldFiber · AlgebraicGeometry.Space.isQuasiFiniteAt_of_isFinite_pullback_snd · AlgebraicGeometry.Space.finite_fieldFiber_iff_exists_isOpenSubspace_isFinite_pullback_snd · AlgebraicGeometry.Space.finite_setFibre_iff_finite_fieldFibre_of_isAbsolutelyQuasiSeparated · AlgebraicGeometry.Space.finite_setFibre_of_isFinite_openRestriction · AlgebraicGeometry.Space.finite_fieldFibre_of_isFinite_openRestriction

Section68.22 Birational morphisms#

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

Tag 0ACV, a definition

Tag 0ACV in the Stacks Project.

AlgebraicGeometry.Space.IsBirational, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalMorphism/IsBirational.lean, line 605. References: EGA I (2.2.9), “more general”.

Stacks 0ACV. A morphism of decent algebraic spaces with finitely many irreducible components is birational when it bijects the generic points of the irreducible components and induces isomorphisms on their schematic-locus local rings.

def IsBirational
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (hdecX : IsDecentSpace B S hS X)
    (hdecY : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    (f : X ⟶ Y) : Prop

Tag 0ACW, a lemma

Tag 0ACW in the Stacks Project.

AlgebraicGeometry.Space.isDominant_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/BirationalDominant.lean, line 57. References: EGA I (2.2.9), “more general”.

Stacks 0ACW. A birational morphism of decent algebraic spaces over S with finitely many irreducible components is dominant: it maps the generic points of the irreducible components of the source onto those of the target, and those are dense in a quasi-sober space.

theorem isDominant_of_isBirational (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (hdecX : IsDecentSpace B S hS X)
    (hdecY : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    {f : X ⟶ Y}
    (hf : IsBirational B S hS hX hY hdecX hdecY hfiniteX hfiniteY f) :
    IsDominant B S hS f

Tag 0BBD, a lemma

Tag 0BBD in the Stacks Project.

AlgebraicGeometry.Space.isIso_pullback_snd_fromGenericStalk_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalGenericStalk.lean, line 817.

Stacks 0BBD. A birational morphism of decent algebraic spaces with finitely many irreducible components becomes an isomorphism after base change to the spectrum of the local ring of the target at a generic point.

theorem isIso_pullback_snd_fromGenericStalk_of_isBirational
    (hdecentY : IsDecentSpace B S hS Y)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hdecentX : IsDecentSpace B S hS X)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (f : X ⟶ Y)
    (hf : IsBirational B S hS hX hY hdecentX hdecentY hfiniteX hfiniteY f) :
    IsIso (pullback.snd f (fromGenericStalk B S hS hY
      (hasDenseRepresentableOpenSubspace_of_isDecentSpace B S hS hY hdecentY)
      hfiniteY y hy))

Tag 0BBE, a lemma

Tag 0BBE in the Stacks Project.

AlgebraicGeometry.Space.exists_dense_isOpenSubspace_isIso_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalDenseOpenIso.lean, line 405.

Stacks 0BBE. A birational morphism of decent algebraic spaces over S with finitely many irreducible components restricts to an isomorphism between dense open subspaces, provided it is locally of finite type with reduced target or locally of finite presentation.

The source reduces the statement to schemes and quotes Stacks 0BAC there; the reduction is carried out on representable open charts with dense point sets, see the module docstring.

theorem exists_dense_isOpenSubspace_isIso_of_isBirational
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hdecentX : IsDecentSpace B S hS X) (hdecentY : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    (f : X ⟶ Y)
    (hbir : IsBirational B S hS hX hY hdecentX hdecentY hfiniteX hfiniteY f)
    (hfin : (IsLocallyOfFiniteType B S hS f ∧
        HasEtaleLocalProperty B S hS Y
          (fun Z : Scheme.{u} => _root_.AlgebraicGeometry.IsReduced Z)) ∨
      IsLocallyOfFinitePresentation B S hS f) :
    ∃ (U : Subfunctor X) (V : Subfunctor Y) (ψ : U.toFunctor ⟶ V.toFunctor),
      IsOpenSubspace B S hS U ∧ IsOpenSubspace B S hS V ∧
        DenseRange (pointsMap B S hS U.toFunctor U.ι) ∧
        DenseRange (pointsMap B S hS V.toFunctor V.ι) ∧
        ψ ≫ V.ι = U.ι ≫ f ∧ IsIso ψ

Tag 0BBF, a lemma

Tag 0BBF in the Stacks Project.

AlgebraicGeometry.Space.exists_isDenseOpenSubspace_isIso_pullback_snd_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalIsoOverDenseOpen.lean, line 262.

Stacks 0BBF. Let f : X ⟶ Y be a birational morphism of algebraic spaces over a scheme S which are decent and have finitely many irreducible components. Assume that f is quasi-compact or separated, and that f is locally of finite type with Y reduced or locally of finite presentation. Then there is a dense open subspace V ⊂ Y such that f^{-1}(V) ⟶ V is an isomorphism.

The source shrinks Y to a dense open over which f is finite, by Stacks 0BBC, and separately to a dense open over which f restricts to an isomorphism of dense opens, by Stacks 0BBE; the intersection of the two is the open subspace produced here. See the module docstring.

theorem exists_isDenseOpenSubspace_isIso_pullback_snd_of_isBirational
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hdecentX : IsDecentSpace B S hS X) (hdecentY : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    (f : X ⟶ Y)
    (hbir : IsBirational B S hS hX hY hdecentX hdecentY hfiniteX hfiniteY f)
    (hqc_or_sep : IsQuasiCompact B S hS f ∨ IsSeparated B S hS f)
    (hfin : (IsLocallyOfFiniteType B S hS f ∧
        HasEtaleLocalProperty B S hS Y
          (fun Z : Scheme.{u} => _root_.AlgebraicGeometry.IsReduced Z)) ∨
      IsLocallyOfFinitePresentation B S hS f) :
    ∃ V : Subfunctor Y,
      IsOpenSubspace B S hS V ∧
        Dense (Set.range (pointsMap B S hS V.toFunctor V.ι)) ∧
          IsIso (pullback.snd f V.ι)

Tag 0B4D, a lemma

Tag 0B4D in the Stacks Project.

AlgebraicGeometry.Space.isDecentSpace_pullback_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalEtaleLocalization.lean, line 562. The attribute's comment: “decent”.

Stacks 0B4D, decency. The base change of a decent algebraic space along an étale morphism from a representable presheaf is decent.

theorem isDecentSpace_pullback_of_isEtale
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hdecentX : IsDecentSpace B S hS X)
    (V : BigFppfOver B S hS)
    (f : X ⟶ Y) (g : yoneda.obj V ⟶ Y) (hg : IsEtale B S hS g) :
    IsDecentSpace B S hS (pullback f g)

AlgebraicGeometry.Space.finite_irreducibleComponents_pullback_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalEtaleLocalization.lean, line 730. The attribute's comment: “finitely many irreducible components”.

Stacks 0B4D, finitely many irreducible components. An affine étale localization of a birational morphism of decent algebraic spaces with finitely many irreducible components has a source with finitely many irreducible components.

theorem finite_irreducibleComponents_pullback_of_isEtale
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hdecentX : IsDecentSpace B S hS X) (hdecentY : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    (f : X ⟶ Y)
    (hf : IsBirational B S hS hX hY hdecentX hdecentY hfiniteX hfiniteY f)
    (V : BigFppfOver B S hS) [IsAffine ((BigFppfOver.toScheme B S hS).obj V)]
    (g : yoneda.obj V ⟶ Y) (hg : IsEtale B S hS g) :
    letI := pointTopology B S hS (pullback f g)
    (irreducibleComponents (points B S hS (pullback f g))).Finite

AlgebraicGeometry.Space.isBirational_pullback_snd_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalEtaleLocalization.lean, line 949. The attribute's comment: “birational”. References: EGA IV (6.15.4.1), “étale affine case”.

Stacks 0B4D, birationality. An affine étale localization of a birational morphism of decent algebraic spaces with finitely many irreducible components is birational.

theorem isBirational_pullback_snd_of_isEtale
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hdecentX : IsDecentSpace B S hS X) (hdecentY : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    (f : X ⟶ Y)
    (hf : IsBirational B S hS hX hY hdecentX hdecentY hfiniteX hfiniteY f)
    (V : BigFppfOver B S hS) [IsAffine ((BigFppfOver.toScheme B S hS).obj V)]
    (g : yoneda.obj V ⟶ Y) (hg : IsEtale B S hS g) :
    IsBirational B S hS
      (isAlgebraicSpace_pullback B S hS f g hX (isAlgebraicSpace_yoneda B S hS V) hY)
      (isAlgebraicSpace_yoneda B S hS V)
      (isDecentSpace_pullback_of_isEtale B S hS hX hY hdecentX V f g hg)
      (isDecentSpace_of_isEtale B S hS g (isAlgebraicSpace_yoneda B S hS V) hY hg hdecentY)
      (finite_irreducibleComponents_pullback_of_isEtale B S hS hX hY hdecentX hdecentY
        hfiniteX hfiniteY f hf V g hg)
      (finite_irreducibleComponents_of_isEtale_of_isAffine B S hS hY hdecentY hfiniteY V g hg)
      (pullback.snd f g)

Tag 0BBG, a lemma

Tag 0BBG in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_lift_normalization_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalNormalization.lean, line 173. The attribute's comment: “the commutative square, as a unique factorization through the target normalization”.

The commutative square of Stacks 0BBG, for given normalizations. Let f : X ⟶ Y be a birational morphism of decent algebraic spaces over S with finitely many irreducible components, and let X^ν ⟶ X and Y^ν ⟶ Y be normalizations. Then X^ν ⟶ X ⟶ Y factors through Y^ν ⟶ Y by a unique morphism X^ν ⟶ Y^ν, so that the square it closes commutes.

The factorization is the universal property of the normalization of Y, part (4) of Stacks 0BB4. Its two hypotheses on the composite X^ν ⟶ X ⟶ Y are normality of X^ν, part (1) of Stacks 0BB4, and preservation of codimension-zero points, which holds for X^ν ⟶ X by part (3) of Stacks 0BB4 and for f by AlgebraicGeometry.Space.localRingDimension_eq_zero_of_isBirational.

The normalizations are hypotheses here, whereas the source asserts their existence; that existence is AlgebraicGeometry.Space.nonempty_normalizationData_of_isDecentSpace, and the whole lemma, which quantifies over no normalization data at all, is AlgebraicGeometry.Space.exists_normalizationData_isBirational_lift_of_isBirational. The statement here is the stronger one for the square — it holds for every choice of the two normalizations, not just the ones the existence theorem produces — and it is what the rest of the development consumes.

theorem existsUnique_lift_normalization_of_isBirational (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    (hXdec : IsDecentSpace B S hS X) (hYdec : IsDecentSpace B S hS Y)
    (DX : NormalizationData B S hS X) (DY : NormalizationData B S hS Y) {f : X ⟶ Y}
    (hf : IsBirational B S hS hX hY hXdec hYdec hfiniteX hfiniteY f) :
    ∃! g : DX.space ⟶ DY.space, g ≫ DY.hom = DX.hom ≫ f

AlgebraicGeometry.Space.isBirational_lift_normalization_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalNormalization.lean, line 467. The attribute's comment: “birationality of the induced morphism of normalizations”.

Birationality of the induced morphism, for given normalizations. Let f : X ⟶ Y be a birational morphism of decent algebraic spaces over S with finitely many irreducible components, and let X^ν ⟶ X and Y^ν ⟶ Y be normalizations. Then any morphism X^ν ⟶ Y^ν closing the square over f is birational.

The two normalizations are again decent with finitely many irreducible components, and their normalization morphisms biject generic points, so the induced morphism does too. At a generic point z of X^ν the local-ring map is computed on charts: the chart map of X^ν ⟶ X is surjective on local rings at z by AlgebraicGeometry.Space.NormalizationData.surjective_stalkMap_of_genericChart, and the chart map of f is an isomorphism there by birationality, so the chart map of X^ν ⟶ Y^ν followed by that of Y^ν ⟶ Y is surjective, whence the chart map of X^ν ⟶ Y^ν is surjective. It is injective because its source — the local ring of the normal space Y^ν at a point of codimension zero — is a field.

The normalizations are hypotheses here, as at AlgebraicGeometry.Space.existsUnique_lift_normalization_of_isBirational.

theorem isBirational_lift_normalization_of_isBirational (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hXdec : IsDecentSpace B S hS X)
    (hYdec : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    (DX : NormalizationData B S hS X) (DY : NormalizationData B S hS Y) {f : X ⟶ Y}
    (hf : IsBirational B S hS hX hY hXdec hYdec hfiniteX hfiniteY f)
    (g : DX.space ⟶ DY.space) (hg : g ≫ DY.hom = DX.hom ≫ f) :
    IsBirational B S hS DX.isAlgebraicSpace DY.isAlgebraicSpace
      (DX.isDecentSpace hX hXdec) (DY.isDecentSpace hY hYdec)
      (DX.finite_irreducibleComponents hX hXdec hfiniteX)
      (DY.finite_irreducibleComponents hY hYdec hfiniteY) g

AlgebraicGeometry.Space.exists_isBirational_lift_normalization_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalNormalization.lean, line 499. The attribute's comment: “the commutative square together with the birationality of the induced morphism of normalizations”.

The square and the birationality together, for given normalizations. Let f : X ⟶ Y be a birational morphism of decent algebraic spaces over S with finitely many irreducible components, and let X^ν ⟶ X and Y^ν ⟶ Y be normalizations. Then X^ν ⟶ X ⟶ Y factors through Y^ν ⟶ Y, and the factoring morphism X^ν ⟶ Y^ν is birational.

The factorization is AlgebraicGeometry.Space.existsUnique_lift_normalization_of_isBirational and its birationality is AlgebraicGeometry.Space.isBirational_lift_normalization_of_isBirational.

The normalizations are hypotheses here; the whole lemma, with their existence, is AlgebraicGeometry.Space.exists_normalizationData_isBirational_lift_of_isBirational.

theorem exists_isBirational_lift_normalization_of_isBirational
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXdec : IsDecentSpace B S hS X) (hYdec : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    (DX : NormalizationData B S hS X) (DY : NormalizationData B S hS Y) {f : X ⟶ Y}
    (hf : IsBirational B S hS hX hY hXdec hYdec hfiniteX hfiniteY f) :
    ∃ g : DX.space ⟶ DY.space, g ≫ DY.hom = DX.hom ≫ f ∧
      IsBirational B S hS DX.isAlgebraicSpace DY.isAlgebraicSpace
        (DX.isDecentSpace hX hXdec) (DY.isDecentSpace hY hYdec)
        (DX.finite_irreducibleComponents hX hXdec hfiniteX)
        (DY.finite_irreducibleComponents hY hYdec hfiniteY) g

AlgebraicGeometry.Space.nonempty_normalizationData_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalNormalizationExistence.lean, line 82. The attribute's comment: “the existence of the normalizations”.

Stacks 0BBG, the existence of the normalizations. A decent algebraic space over S whose space of points has finitely many irreducible components has normalization data: an algebraic space F^ν over S with a morphism F^ν ⟶ F whose base change along every surjective étale scheme chart of F is the normalization of that chart.

This is the first clause of Stacks 0BBG, and the source proves it the same way: the hypotheses give the equivalent conditions of Stacks 0BB1 by Stacks 0BB9 (AlgebraicGeometry.Space.hasLocallyFiniteIrreducibleComponents_of_isDecentSpace), and under those conditions the normalization exists by the existence half of Stacks 07U4, AlgebraicGeometry.Space.nonempty_normalizationData. Applied to the source and the target of a birational morphism it is the assertion that X^ν ⟶ X and Y^ν ⟶ Y exist.

theorem nonempty_normalizationData_of_isDecentSpace
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (hFdec : IsDecentSpace B S hS F)
    (hfinite : (letI := pointTopology B S hS F
      (irreducibleComponents (points B S hS F)).Finite)) :
    Nonempty (NormalizationData B S hS F)

AlgebraicGeometry.Space.exists_normalizationData_isBirational_lift_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalNormalizationExistence.lean, line 112.

Stacks 0BBG. Let f : X ⟶ Y be a birational morphism between algebraic spaces over S which are decent and have finitely many irreducible components. Then the normalizations X^ν ⟶ X and Y^ν ⟶ Y exist and there is a commutative diagram with rows X^ν ⟶ Y^ν and X ⟶ Y and columns the two normalization morphisms, and the morphism X^ν ⟶ Y^ν is birational.

Nothing is assumed about the normalizations: they are produced by AlgebraicGeometry.Space.nonempty_normalizationData_of_isDecentSpace from decency and the finiteness of the irreducible components, which is the source's own route through Stacks 0BB9 and Stacks 0BB1. The square is then AlgebraicGeometry.Space.existsUnique_lift_normalization_of_isBirational and the birationality of the morphism closing it is AlgebraicGeometry.Space.isBirational_lift_normalization_of_isBirational, both of which hold for an arbitrary choice of the two normalizations.

The decency of X^ν and Y^ν and the finiteness of their irreducible components, which the conclusion's AlgebraicGeometry.Space.IsBirational is parameterised by, are AlgebraicGeometry.Space.NormalizationData.isDecentSpace and AlgebraicGeometry.Space.NormalizationData.finite_irreducibleComponents; the source records them in its second paragraph, citing Stacks 0ABT.

theorem exists_normalizationData_isBirational_lift_of_isBirational
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXdec : IsDecentSpace B S hS X) (hYdec : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    {f : X ⟶ Y}
    (hf : IsBirational B S hS hX hY hXdec hYdec hfiniteX hfiniteY f) :
    ∃ (DX : NormalizationData B S hS X) (DY : NormalizationData B S hS Y)
      (g : DX.space ⟶ DY.space), g ≫ DY.hom = DX.hom ≫ f ∧
        IsBirational B S hS DX.isAlgebraicSpace DY.isAlgebraicSpace
          (DX.isDecentSpace hX hXdec) (DY.isDecentSpace hY hYdec)
          (DX.finite_irreducibleComponents hX hXdec hfiniteX)
          (DY.finite_irreducibleComponents hY hYdec hfiniteY) g

Tag 0B4E, a lemma

Tag 0B4E in the Stacks Project.

AlgebraicGeometry.Space.isIso_of_isIntegralHom_of_isBirational_of_isNormal_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralBirationalOverNormal.lean, line 467. References: EGA IV (8.12.10.1).

Stacks 0B4E. An integral birational morphism from a reduced algebraic space to a normal algebraic space is an isomorphism, provided both are decent with finitely many irreducible components.

Being an isomorphism is checked on the jointly locally surjective family of affine étale charts V i → Y supplied by AlgebraicGeometry.exists_affine_etale_family_isLocallySurjective. Integrality of f represents the base change X ×_Y V i by an affine object W of the site, so the chart base change is a morphism of schemes W → V i; it is birational by Stacks 0B4D together with AlgebraicGeometry.isBirational_toScheme_map_of_yonedaIso, its source is reduced and its target normal with finitely many irreducible components, whence it is an isomorphism by AlgebraicGeometry.isIso_of_isReduced_of_isBirational_of_isNormal.

theorem isIso_of_isIntegralHom_of_isBirational_of_isNormal_of_isReduced
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hdecentX : IsDecentSpace B S hS X) (hdecentY : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    (f : X ⟶ Y)
    (hintegral : IsIntegralHom B S hS f)
    (hbirational : IsBirational B S hS hX hY hdecentX hdecentY hfiniteX hfiniteY f)
    (hnormalY : IsNormal B S hS Y)
    (hreducedX : HasEtaleLocalProperty B S hS X
      (fun Z : Scheme.{u} => _root_.AlgebraicGeometry.IsReduced Z)) :
    IsIso f

Tag 0BBH, a lemma

Tag 0BBH in the Stacks Project.

AlgebraicGeometry.Space.exists_factorization_normalization_of_isIntegralHom_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BirationalNormalization.lean, line 533.

Stacks 0BBH. Let f : X ⟶ Y be an integral birational morphism of decent algebraic spaces over S with finitely many irreducible components, and let X^ν ⟶ X and Y^ν ⟶ Y be normalizations. Then the normalization morphism of Y factors as Y^ν ⟶ X ⟶ Y, and the first leg Y^ν ⟶ X is the normalization of X: it is the normalization morphism X^ν ⟶ X precomposed with an isomorphism Y^ν ≅ X^ν over X.

The induced morphism X^ν ⟶ Y^ν of Stacks 0BBG is integral by Stacks 081Z, part (2): its composite with the normalization morphism of Y is the composite of the normalization morphism of X with f, both integral, and the normalization morphism of Y is integral hence separated. It is birational by Stacks 0BBG, its source is reduced — being normal — and its target is normal, both normalizations are decent with finitely many irreducible components, so Stacks 0B4E makes it an isomorphism. Its inverse is the asserted factorization.

theorem exists_factorization_normalization_of_isIntegralHom_of_isBirational
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXdec : IsDecentSpace B S hS X) (hYdec : IsDecentSpace B S hS Y)
    (hfiniteX : (letI := pointTopology B S hS X
      (irreducibleComponents (points B S hS X)).Finite))
    (hfiniteY : (letI := pointTopology B S hS Y
      (irreducibleComponents (points B S hS Y)).Finite))
    (DX : NormalizationData B S hS X) (DY : NormalizationData B S hS Y) {f : X ⟶ Y}
    (hfint : IsIntegralHom B S hS f)
    (hf : IsBirational B S hS hX hY hXdec hYdec hfiniteX hfiniteY f) :
    ∃ (h : DY.space ⟶ X) (e : DY.space ≅ DX.space),
      h ≫ f = DY.hom ∧ h = e.hom ≫ DX.hom

Sources

• Section 68.22, Tag 0ACU
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsBirational · AlgebraicGeometry.Space.isDominant_of_isBirational · AlgebraicGeometry.Space.isIso_pullback_snd_fromGenericStalk_of_isBirational · AlgebraicGeometry.Space.exists_dense_isOpenSubspace_isIso_of_isBirational · AlgebraicGeometry.Space.exists_isDenseOpenSubspace_isIso_pullback_snd_of_isBirational · AlgebraicGeometry.Space.isDecentSpace_pullback_of_isEtale · AlgebraicGeometry.Space.finite_irreducibleComponents_pullback_of_isEtale · AlgebraicGeometry.Space.isBirational_pullback_snd_of_isEtale

Section68.23 Jacobson spaces#

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

Tag 0BA3, a lemma

Tag 0BA3 in the Stacks Project.

AlgebraicGeometry.Space.exists_jacobson_atlas_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Jacobson.lean, line 54. References: EGA IV (10.4.7), “Y Jacobson”.

Stacks 0BA3. An algebraic space locally of finite type over a Jacobson algebraic space is Jacobson: if the algebraic space X over S has a surjective étale atlas by a Jacobson scheme and f : Y ⟶ X is locally of finite type, then so does Y.

theorem exists_jacobson_atlas_of_isLocallyOfFiniteType (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : Y ⟶ X)
    (hf : IsLocallyOfFiniteType B S hS f)
    (hJac : ∃ (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) a ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) a ∧
      JacobsonSpace ((BigFppfOver.toScheme B S hS).obj U)) :
    ∃ (V : BigFppfOver B S hS) (b : yoneda.obj V ⟶ Y),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) b ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) b ∧
      JacobsonSpace ((BigFppfOver.toScheme B S hS).obj V)

Tag 0BA4, a lemma

Tag 0BA4 in the Stacks Project.

AlgebraicGeometry.Space.exists_isClosed_pointsToScheme_of_isFiniteTypePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/JacobsonClosedPoints.lean, line 74.

Stacks 0BA4. Let X be a Jacobson algebraic space over S, written as having a surjective étale atlas by a Jacobson scheme, and let g : h_W ⟶ X be locally of finite type with W an object of the big fppf site of S. A finite type point of X in the image of g is the image of a point of h_W whose underlying point of the scheme W is closed.

theorem exists_isClosed_pointsToScheme_of_isFiniteTypePoint
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hJac : ∃ (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) a ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) a ∧
      JacobsonSpace ((BigFppfOver.toScheme B S hS).obj U))
    (W : BigFppfOver B S hS) (g : yoneda.obj W ⟶ X)
    (hg : IsLocallyOfFiniteType B S hS g)
    (x : points B S hS X) (hx : IsFiniteTypePoint B S hS X x)
    (himage : x ∈ Set.range (pointsMap B S hS (yoneda.obj W) g)) :
    ∃ y : points B S hS (yoneda.obj W),
      IsClosed ({pointsToScheme B S hS W y} :
        Set ((BigFppfOver.toScheme B S hS).obj W)) ∧
      pointsMap B S hS (yoneda.obj W) g y = x

Tag 0BA5, a lemma

Tag 0BA5 in the Stacks Project.

AlgebraicGeometry.Space.isFiniteTypePoint_iff_isClosed_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/JacobsonFiniteTypePoints.lean, line 149. The attribute's comment: “pointwise form”.

Stacks 0BA5, pointwise. Let X be a decent Jacobson algebraic space over S, the Jacobson condition being written as the existence of a surjective étale atlas by a Jacobson scheme. A point of X is a finite type point exactly when it is a closed point of |X|.

theorem isFiniteTypePoint_iff_isClosed_singleton
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X)
    (hJac : ∃ (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) a ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) a ∧
      JacobsonSpace ((BigFppfOver.toScheme B S hS).obj U))
    (x : points B S hS X) :
    IsFiniteTypePoint B S hS X x ↔ IsClosed ({x} : Set (points B S hS X))

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

Stacks 0BA5. Let X be a decent Jacobson algebraic space over S, the Jacobson condition being written as the existence of a surjective étale atlas by a Jacobson scheme. Then X_{ft-pts} ⊂ |X| is the set of closed points.

theorem finiteTypePoints_eq_setOf_isClosed_singleton
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X)
    (hJac : ∃ (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) a ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) a ∧
      JacobsonSpace ((BigFppfOver.toScheme B S hS).obj U)) :
    finiteTypePoints B S hS X = {x | IsClosed ({x} : Set (points B S hS X))}

Tag 0BA6, a lemma

Tag 0BA6 in the Stacks Project.

AlgebraicGeometry.Space.exists_jacobson_atlas_iff_jacobsonSpace_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/JacobsonPointSpace.lean, line 295.

Stacks 0BA6. A decent algebraic space X over S is Jacobson — the Jacobson condition being written as the existence of a surjective étale atlas by a Jacobson scheme — if and only if its topological space |X| of points is a Jacobson topological space.

theorem exists_jacobson_atlas_iff_jacobsonSpace_points
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) :
    (∃ (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) a ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) a ∧
      JacobsonSpace ((BigFppfOver.toScheme B S hS).obj U)) ↔
    JacobsonSpace (points B S hS X)

Tag 0ED2, a lemma

Tag 0ED2 in the Stacks Project.

AlgebraicGeometry.Space.stacksSober_properGeneralizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ProperGeneralizations.lean, line 224. The attribute's comment: “sobriety”.

Stacks 0ED2, sobriety. The proper generalizations of a point x of a decent algebraic space over S form a sober topological space, sobriety being that of Stacks 004X: every irreducible closed subset has a unique generic point.

theorem stacksSober_properGeneralizations (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) (x : points B S hS X) :
    StacksSober {x' : points B S hS X // x' ⤳ x ∧ x' ≠ x}

AlgebraicGeometry.Space.spectralSpace_properGeneralizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ProperGeneralizations.lean, line 235. The attribute's comment: “spectrality”.

Stacks 0ED2, spectrality. The proper generalizations of a point x of a decent locally Noetherian algebraic space over S form a spectral topological space.

theorem spectralSpace_properGeneralizations (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsLocallyNoetherian Y))
    (x : points B S hS X) :
    SpectralSpace {x' : points B S hS X // x' ⤳ x ∧ x' ≠ x}

AlgebraicGeometry.Space.jacobsonSpace_properGeneralizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ProperGeneralizations.lean, line 252. The attribute's comment: “the Jacobson property”.

Stacks 0ED2, the Jacobson property. The proper generalizations of a point x of a decent locally Noetherian algebraic space over S form a Jacobson topological space.

theorem jacobsonSpace_properGeneralizations (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsLocallyNoetherian Y))
    (x : points B S hS X) :
    JacobsonSpace {x' : points B S hS X // x' ⤳ x ∧ x' ≠ x}

AlgebraicGeometry.Space.noetherianSpace_properGeneralizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperGeneralizations.lean, line 50. The attribute's comment: “the Noetherian property”.

Stacks 0ED2, the Noetherian property. The proper generalizations of a point x of a locally Noetherian algebraic space over S form a Noetherian topological space.

theorem noetherianSpace_properGeneralizations (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsLocallyNoetherian Y))
    (x : points B S hS X) :
    NoetherianSpace {x' : points B S hS X // x' ⤳ x ∧ x' ≠ x}

Sources

• Section 68.23, Tag 0BA2
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.exists_jacobson_atlas_of_isLocallyOfFiniteType · AlgebraicGeometry.Space.exists_isClosed_pointsToScheme_of_isFiniteTypePoint · AlgebraicGeometry.Space.isFiniteTypePoint_iff_isClosed_singleton · AlgebraicGeometry.Space.finiteTypePoints_eq_setOf_isClosed_singleton · AlgebraicGeometry.Space.exists_jacobson_atlas_iff_jacobsonSpace_points · AlgebraicGeometry.Space.stacksSober_properGeneralizations · AlgebraicGeometry.Space.spectralSpace_properGeneralizations · AlgebraicGeometry.Space.jacobsonSpace_properGeneralizations

Section68.24 Local irreducibility#

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

Tag 0DQ6, a lemma

Tag 0DQ6 in the Stacks Project.

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

Stacks 0DQ6, conditions (1) and (2). The local ring of every elementary étale neighbourhood of x at its distinguished point has a unique minimal prime exactly when exactly one irreducible component of every such neighbourhood passes through its distinguished point.

theorem forall_existsUnique_minimalPrimes_iff_forall_existsUnique_component :
    (∀ U : ElementaryEtaleNeighborhood B S hS X hX x,
        ∃! q : Ideal (U.scheme.left.1.presheaf.stalk U.point),
          q ∈ minimalPrimes (U.scheme.left.1.presheaf.stalk U.point)) ↔
      ∀ U : ElementaryEtaleNeighborhood B S hS X hX x,
        ∃! Z : irreducibleComponents U.scheme.left.1,
          U.point ∈ (Z : Set U.scheme.left.1)

AlgebraicGeometry.Space.forall_existsUnique_component_iff_forall_isUnibranchAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocalIrreducibility.lean, line 238. The attribute's comment: “conditions (2) and (3)”.

Stacks 0DQ6, conditions (2) and (3). Exactly one irreducible component of every elementary étale neighbourhood of x passes through its distinguished point exactly when the local ring of every such neighbourhood at its distinguished point is unibranch.

theorem forall_existsUnique_component_iff_forall_isUnibranchAt :
    (∀ U : ElementaryEtaleNeighborhood B S hS X hX x,
        ∃! Z : irreducibleComponents U.scheme.left.1,
          U.point ∈ (Z : Set U.scheme.left.1)) ↔
      ∀ U : ElementaryEtaleNeighborhood B S hS X hX x,
        _root_.AlgebraicGeometry.IsUnibranchAt U.scheme.left.1 U.point

AlgebraicGeometry.Space.tfae_localIrreducibility, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocalIrreducibility.lean, line 414. The attribute's comment: “(1)-(4) equivalent”.

Stacks 0DQ6. For a point of a decent algebraic space the four conditions of the source are equivalent: every elementary étale neighbourhood has a local ring with a unique minimal prime, has a unique irreducible component through its distinguished point, and has a unibranch local ring; and the henselian local ring at the point has a unique minimal prime.

theorem tfae_localIrreducibility (hDecent : IsDecentSpace B S hS X) :
    List.TFAE
      [∀ U : ElementaryEtaleNeighborhood B S hS X hX x,
          ∃! q : Ideal (U.scheme.left.1.presheaf.stalk U.point),
            q ∈ minimalPrimes (U.scheme.left.1.presheaf.stalk U.point),
        ∀ U : ElementaryEtaleNeighborhood B S hS X hX x,
          ∃! Z : irreducibleComponents U.scheme.left.1,
            U.point ∈ (Z : Set U.scheme.left.1),
        ∀ U : ElementaryEtaleNeighborhood B S hS X hX x,
          _root_.AlgebraicGeometry.IsUnibranchAt U.scheme.left.1 U.point,
        ∃! p : Ideal (henselianLocalRing B S hS X hX x hDecent : Type (u + 1)),
          p ∈ minimalPrimes (henselianLocalRing B S hS X hX x hDecent : Type (u + 1))]

Tag 0DQ7, a definition

Tag 0DQ7 in the Stacks Project.

AlgebraicGeometry.Space.IsUnibranchAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocalIrreducibility.lean, line 476. The attribute's comment: “unibranch at a point”.

Stacks 0DQ7, unibranch at a point. A decent algebraic space is unibranch at x when the local ring of every elementary étale neighbourhood of x at its distinguished point is unibranch, which is condition (3) of Tag 0DQ6.

abbrev IsUnibranchAt (_hDecent : IsDecentSpace B S hS X) : Prop

AlgebraicGeometry.Space.IsUnibranch, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocalIrreducibility.lean, line 483. The attribute's comment: “unibranch”.

Stacks 0DQ7, unibranch. A decent algebraic space is unibranch when it is unibranch at every one of its points.

abbrev IsUnibranch (hDecent : IsDecentSpace B S hS X) : Prop

Tag 0DQ8, a lemma

Tag 0DQ8 in the Stacks Project.

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

Stacks 0DQ8, conditions (1) and (2). A point of a presheaf on the big fppf site has minimal-prime count n on its elementary étale neighbourhoods exactly when it has irreducible-component count n on them: the two counts agree neighbourhood by neighbourhood.

theorem hasMinimalPrimeCount_iff_hasComponentCount (n : ℕ) :
    HasMinimalPrimeCountOnElementaryNeighborhoods B S hS X hX x n ↔
      HasComponentCountOnElementaryNeighborhoods B S hS X hX x n

AlgebraicGeometry.Space.hasComponentCount_iff_hasBranchCount, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocalIrreducibility.lean, line 348. The attribute's comment: “conditions (2) and (3)”.

Stacks 0DQ8, conditions (2) and (3). A point of a presheaf on the big fppf site has irreducible-component count n on its elementary étale neighbourhoods exactly when it has branch count n on them.

theorem hasComponentCount_iff_hasBranchCount (n : ℕ) :
    HasComponentCountOnElementaryNeighborhoods B S hS X hX x n ↔
      HasBranchCountOnElementaryNeighborhoods B S hS X hX x n

AlgebraicGeometry.Space.tfae_hasBranchCount, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocalIrreducibility.lean, line 457. The attribute's comment: “(1)-(4) equivalent”.

Stacks 0DQ8. For a point of a decent algebraic space and a natural number n the four conditions of the source are equivalent: the minimal primes of the local ring, the irreducible components through the distinguished point, and the branches each number at most n over all elementary étale neighbourhoods with n attained at one of them; and the henselian local ring at the point has exactly n minimal primes.

theorem tfae_hasBranchCount (hDecent : IsDecentSpace B S hS X) (n : ℕ) :
    List.TFAE
      [HasMinimalPrimeCountOnElementaryNeighborhoods B S hS X hX x n,
        HasComponentCountOnElementaryNeighborhoods B S hS X hX x n,
        HasBranchCountOnElementaryNeighborhoods B S hS X hX x n,
        Set.encard (minimalPrimes (henselianLocalRing B S hS X hX x hDecent : Type (u + 1))) =
          (n : ℕ∞)]

Tag 0DQ9, a definition

Tag 0DQ9 in the Stacks Project.

AlgebraicGeometry.Space.numberOfBranches, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocalIrreducibility.lean, line 511.

Stacks 0DQ9. The number of branches of a decent algebraic space at a point: the natural number satisfying the equivalent conditions of Tag 0DQ8 if there is one, and ⊤ otherwise.

def numberOfBranches (_hDecent : IsDecentSpace B S hS X) : ℕ∞

AlgebraicGeometry.Space.numberOfBranches_eq_top_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocalIrreducibility.lean, line 518. The attribute's comment: “infinite value”.

The number of branches of a decent algebraic space at a point is infinite exactly when no natural number satisfies the equivalent conditions of Tag 0DQ8.

theorem numberOfBranches_eq_top_iff (hDecent : IsDecentSpace B S hS X) :
    numberOfBranches B S hS X hX x hDecent = ⊤ ↔
      ∀ n : ℕ, ¬ HasBranchCountOnElementaryNeighborhoods B S hS X hX x n

AlgebraicGeometry.Space.numberOfBranches_eq_nat_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocalIrreducibility.lean, line 528. The attribute's comment: “finite value”.

A finite value of the number of branches of a decent algebraic space at a point is exactly the value appearing in the equivalent conditions of Tag 0DQ8.

theorem numberOfBranches_eq_nat_iff (hDecent : IsDecentSpace B S hS X) (n : ℕ) :
    numberOfBranches B S hS X hX x hDecent = (n : ℕ∞) ↔
      HasBranchCountOnElementaryNeighborhoods B S hS X hX x n

Sources

• Section 68.24, Tag 0DQ5
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.forall_existsUnique_minimalPrimes_iff_forall_existsUnique_component · AlgebraicGeometry.Space.forall_existsUnique_component_iff_forall_isUnibranchAt · AlgebraicGeometry.Space.tfae_localIrreducibility · AlgebraicGeometry.Space.IsUnibranchAt · AlgebraicGeometry.Space.IsUnibranch · AlgebraicGeometry.Space.hasMinimalPrimeCount_iff_hasComponentCount · AlgebraicGeometry.Space.hasComponentCount_iff_hasBranchCount · AlgebraicGeometry.Space.tfae_hasBranchCount

Section68.25 Catenary algebraic spaces#

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

Tag 0ED4, a definition

Tag 0ED4 in the Stacks Project.

AlgebraicGeometry.Space.IsCatenary, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Catenary.lean, line 112.

Stacks 0ED4. An algebraic space is catenary when its space of points, with the topology of Tag 03BX, is a catenary topological space.

abbrev IsCatenary (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (_hX : IsAlgebraicSpace B S hS X) : Prop

Tag 0ED5, a lemma

Tag 0ED5 in the Stacks Project.

AlgebraicGeometry.Space.inducedDimensionValue_isDimensionFunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Catenary.lean, line 192. The attribute's comment: “with decency read as condition (alpha) of Stacks 03JX”. References: SGA 6 X (1.5), “(1.5.2) is a dim. fn”.

Stacks 0ED5. Let T be an object of the big fppf site over S whose underlying scheme is locally Noetherian and universally catenary, and let δ be a dimension function on that scheme. Let X be an algebraic space over S, locally of finite type over T, above every point of which every étale chart by an affine scheme has a finite fibre. Then the function sending a point x of X to the value of δ at the image of x plus the relative transcendence degree of x over that image is a dimension function on the points of X.

The finiteness hypothesis is condition (α) of Stacks 03JX, which is weaker than the condition (1) of Stacks 03JV through which Stacks 03I8 defines a decent algebraic space, and which is all that the argument uses. Taking for T the terminal object Over.mk (𝟙 (B.obj hS)), whose underlying scheme is S, gives the statement for the structure morphism of X.

theorem inducedDimensionValue_isDimensionFunction
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {T : BigFppfOver B S hS}
    [IsLocallyNoetherian ((BigFppfOver.toScheme B S hS).obj T)]
    (hcat : Scheme.IsUniversallyCatenary ((BigFppfOver.toScheme B S hS).obj T))
    (δ : TopologicalSpace.DimensionFunction ((BigFppfOver.toScheme B S hS).obj T))
    (hX : IsAlgebraicSpace B S hS X)
    (hfib : HasFiniteChartFibersAtEveryPoint B S hS X)
    (f : X ⟶ yoneda.obj T) (hf : IsLocallyOfFiniteType B S hS f) :
    ∃ d : TopologicalSpace.DimensionFunction (points B S hS X), ∀ x : points B S hS X,
      d x = inducedDimensionValue B S hS
        (fun y ↦ δ (pointsToScheme B S hS T y)) f x

Tag 0ED6, a lemma

Tag 0ED6 in the Stacks Project.

AlgebraicGeometry.Space.isCatenary_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/Catenary.lean, line 182.

Stacks 0ED6. A decent algebraic space over S which is locally of finite type over an object of the site whose scheme is locally Noetherian and universally catenary is catenary.

theorem isCatenary_of_isDecentSpace {T : BigFppfOver B S hS}
    [IsLocallyNoetherian ((BigFppfOver.toScheme B S hS).obj T)]
    (hcat : Scheme.IsUniversallyCatenary ((BigFppfOver.toScheme B S hS).obj T))
    (hX : IsAlgebraicSpace B S hS X) (hdec : IsDecentSpace B S hS X)
    (f : X ⟶ yoneda.obj T) (hf : IsLocallyOfFiniteType B S hS f) :
    IsCatenary B S hS X hX

Tag 0ED7, a definition

Tag 0ED7 in the Stacks Project.

AlgebraicGeometry.Space.IsUniversallyCatenary, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Catenary.lean, line 119.

Stacks 0ED7. An algebraic space is universally catenary when every decent algebraic space locally of finite type over it is catenary.

abbrev IsUniversallyCatenary (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

Tag 0ED8, a lemma

Tag 0ED8 in the Stacks Project.

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

Stacks 0ED8. An algebraic space locally of finite type over a universally catenary algebraic space is universally catenary.

Universal catenarity of the target already quantifies over all decent algebraic spaces locally of finite type over it, so the source needs no decency or local Noetherianity hypothesis: a decent space locally of finite type over the source is locally of finite type over the target by Stacks 03XG.

theorem isUniversallyCatenary_of_isLocallyOfFiniteType
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hXcat : IsUniversallyCatenary B S hS X) (f : Y ⟶ X)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsUniversallyCatenary B S hS Y

Tag 0ED9, a lemma

Tag 0ED9 in the Stacks Project.

AlgebraicGeometry.Space.exists_dimensionFunction_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionFunction.lean, line 133. The attribute's comment: “decency and local Noetherianity not needed”.

Let q : Z ⟶ X be a surjective finite morphism of algebraic spaces and let δ be a function on the points of X. If the pullback of δ along the map on points of q is a dimension function, then δ is a dimension function.

theorem exists_dimensionFunction_of_isFinite
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hZ : IsAlgebraicSpace B S hS Z) (q : Z ⟶ X) (hqfin : IsFinite B S hS q)
    (hqsurj : IsSurjective B S hS q) (δ : points B S hS X → ℤ)
    (hd : ∃ d : DimensionFunction (points B S hS Z), ∀ z : points B S hS Z,
      d z = δ (pointsMap B S hS Z q z)) :
    ∃ d : DimensionFunction (points B S hS X), ∀ x : points B S hS X, d x = δ x

Sources

• Section 68.25, Tag 0ED3
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsCatenary · AlgebraicGeometry.Space.inducedDimensionValue_isDimensionFunction · AlgebraicGeometry.Space.isCatenary_of_isDecentSpace · AlgebraicGeometry.Space.IsUniversallyCatenary · AlgebraicGeometry.Space.isUniversallyCatenary_of_isLocallyOfFiniteType · AlgebraicGeometry.Space.exists_dimensionFunction_of_isFinite

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.