68.3 Universally bounded fibres to 68.17 Relative conditions

Section68.3 Universally bounded fibres #

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

Tag 03JL, a definition

Tag 03JL in the Stacks Project.

AlgebraicGeometry.Space.HasUniversallyBoundedFibers, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/UniversallyBoundedFibres.lean, line 57.

A scheme morphism to a presheaf has universally bounded fibres if every field-valued base change is represented by a finite scheme and all their degrees have one integer bound.

abbrev HasUniversallyBoundedFibers (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (U : BigFppfOver B S hS)
    (f : yoneda.obj U ⟶ X) : Prop

Tag 03JM, a lemma

Tag 03JM in the Stacks Project.

AlgebraicGeometry.Space.hasUniversallyBoundedFibers_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/UniversallyBoundedFibresComposition.lean, line 170.

Stacks 03JM. Let X be a presheaf on the big fppf site of S, let f : V ⟶ U be a morphism of schemes over S and let g : U ⟶ X be a morphism over S. If the fibres of f and of g are universally bounded, then so are the fibres of the composite V ⟶ X.

theorem hasUniversallyBoundedFibers_comp
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {V U : BigFppfOver B S hS}
    (f : V ⟶ U) (g : yoneda.obj U ⟶ X)
    (hf : HasUniversallyBoundedFibers B S hS V (yoneda.map f))
    (hg : HasUniversallyBoundedFibers B S hS U g) :
    HasUniversallyBoundedFibers B S hS V (yoneda.map f ≫ g)

Tag 03JN, a lemma

Tag 03JN in the Stacks Project.

AlgebraicGeometry.Space.hasUniversallyBoundedFibers_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/UniversallyBoundedFibres.lean, line 72.

A representable base change of a scheme morphism with universally bounded fibres is represented by a scheme whose fibres remain universally bounded.

theorem hasUniversallyBoundedFibers_baseChange
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (g : Y ⟶ X) (hg : yoneda.relativelyRepresentable g)
    (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ X)
    (hf : HasUniversallyBoundedFibers B S hS U f) :
    ∃ (V : BigFppfOver B S hS)
      (i : yoneda.obj V ⟶ yoneda.obj U) (p : yoneda.obj V ⟶ Y),
      IsPullback i p f g ∧ HasUniversallyBoundedFibers B S hS V p

Tag 03JO, a lemma

Tag 03JO in the Stacks Project.

AlgebraicGeometry.Space.hasUniversallyBoundedFibers_of_baseChange_of_range_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/UniversallyBoundedFibresDescent.lean, line 298.

Stacks 03JO. Let g : Y ⟶ X be a morphism of algebraic spaces over S, let f : h_U ⟶ X be a morphism from a scheme over S, and let h_V ⟶ Y be a base change of f along g. If the image of |h_U| → |X| is contained in the image of |Y| → |X| and the fibres of h_V ⟶ Y are universally bounded, then the fibres of f are universally bounded, with the same bound.

theorem hasUniversallyBoundedFibers_of_baseChange_of_range_subset
    (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) (g : Y ⟶ X)
    {U : BigFppfOver B S hS} (f : yoneda.obj U ⟶ X)
    (himage : Set.range (pointsMap B S hS (yoneda.obj U) f) ⊆
      Set.range (pointsMap B S hS Y g))
    {V : BigFppfOver B S hS} {i : yoneda.obj V ⟶ yoneda.obj U} {p : yoneda.obj V ⟶ Y}
    (hcart : IsPullback i p f g) (hp : HasUniversallyBoundedFibers B S hS V p) :
    HasUniversallyBoundedFibers B S hS U f

Tag 03JP, a lemma

Tag 03JP in the Stacks Project.

AlgebraicGeometry.Space.hasUniversallyBoundedFibers_of_comp_of_surjective_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/UniversallyBoundedFibresDescent.lean, line 127.

Stacks 03JP. Let X be an algebraic space over S, let U ⟶ V be a morphism of schemes over S and let V ⟶ X be a morphism over S. If the fibres of the composite U ⟶ X are universally bounded and U ⟶ V is surjective and flat, then the fibres of V ⟶ X are universally bounded, with the same bound.

theorem hasUniversallyBoundedFibers_of_comp_of_surjective_flat
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    {U V : BigFppfOver B S hS} (φ : U ⟶ V) (h : yoneda.obj V ⟶ X)
    [AlgebraicGeometry.Surjective ((BigFppfOver.toScheme B S hS).map φ)]
    [AlgebraicGeometry.Flat ((BigFppfOver.toScheme B S hS).map φ)]
    (hU : HasUniversallyBoundedFibers B S hS U (yoneda.map φ ≫ h)) :
    HasUniversallyBoundedFibers B S hS V h

Tag 03JQ, a lemma

Tag 03JQ in the Stacks Project.

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

Stacks 03JQ. If the fibres of a morphism f : h_U ⟶ X from a represented presheaf are universally bounded, then one natural number bounds the number of points of |h_U| lying above each point of |X|.

theorem cardinalMk_pointFiber_le_of_hasUniversallyBoundedFibers
    (hf : HasUniversallyBoundedFibers B S hS U f) :
    ∃ n : ℕ, ∀ x : points B S hS X,
      Cardinal.mk (pointsMap B S hS (yoneda.obj U) f ⁻¹' {x}) ≤ (n : Cardinal)

Sources

LeanAlgebraicGeometry.Space.HasUniversallyBoundedFibers · AlgebraicGeometry.Space.hasUniversallyBoundedFibers_comp · AlgebraicGeometry.Space.hasUniversallyBoundedFibers_baseChange · AlgebraicGeometry.Space.hasUniversallyBoundedFibers_of_baseChange_of_range_subset · AlgebraicGeometry.Space.hasUniversallyBoundedFibers_of_comp_of_surjective_flat · AlgebraicGeometry.Space.cardinalMk_pointFiber_le_of_hasUniversallyBoundedFibers

Section68.4 Finiteness conditions and points #

Section 68.4 of the Stacks Project, Tag 03JR. 7 tags here are carried by 44 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03II, a remark

Tag 03II in the Stacks Project.

AlgebraicGeometry.locallyQuasiFinite_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/EtaleQuasiFinite.lean, line 54. The attribute's comment: “etale_locally_quasi_finite”.

An étale morphism of schemes is locally quasi-finite.

theorem locallyQuasiFinite_of_etale {X S : Scheme.{u}} (f : X ⟶ S) [Etale f] :
    LocallyOfFiniteType f ∧ LocallyQuasiFinite f

AlgebraicGeometry.flat_and_generalizingMap_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/EtaleQuasiFinite.lean, line 63. The attribute's comment: “etale_flat_generalizing”. References: EGA IV (2.3.4), “(i), special case”.

An étale morphism of schemes is flat, and hence generalizations lift along it.

theorem flat_and_generalizingMap_of_etale {X S : Scheme.{u}} (f : X ⟶ S) [Etale f] :
    Flat f ∧ GeneralizingMap f.base

AlgebraicGeometry.finite_preimage_singleton_of_etale_of_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/EtaleQuasiFinite.lean, line 71. The attribute's comment: “etale_quasi_compact_finite_fibres”.

A quasi-compact étale morphism of schemes has finite fibres.

It is locally quasi-finite, hence quasi-finite as it is quasi-compact.

theorem finite_preimage_singleton_of_etale_of_quasiCompact {X S : Scheme.{u}} (f : X ⟶ S)
    [Etale f] [QuasiCompact f] (s : S) : (f.base ⁻¹' {s}).Finite

AlgebraicGeometry.discreteTopology_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Different/Support/EtaleDiscreteFibres.lean, line 40. The attribute's comment: “etale_discrete_fibres”.

Every scheme-theoretic fibre of an étale morphism is a discrete space.

theorem discreteTopology_fiber {X S : Scheme.{u}} (f : X ⟶ S)
    [Etale f] (s : S) : DiscreteTopology (f.fiber s)

AlgebraicGeometry.unramified_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/EtaleUnramified.lean, line 31. The attribute's comment: “etale_unramified”.

An étale morphism of schemes is unramified.

theorem unramified_of_etale {X S : Scheme.{u}} (f : X ⟶ S) [Etale f] : Unramified f

AlgebraicGeometry.etale_iff_iso_coproduct_spectra_finite_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/OverField.lean, line 75. The attribute's comment: “etale_over_field”. References: EGA IV (17.6.2), “base = Spec k”; SGA 4½ Arcata (2.1.2), “a)”.

Stacks Project, Tag 03PC (over a field). A morphism to the spectrum of a field is étale if and only if its source is, over that spectrum, a coproduct of spectra of finite separable field extensions.

public theorem etale_iff_iso_coproduct_spectra_finite_separable
    (k : Type u) [Field k] {U : Scheme.{u}} (f : U ⟶ Spec (.of k)) :
    Etale f ↔
      ∃ (I : Type u) (K : I → Type u) (_ : ∀ i, Field (K i))
        (_ : ∀ i, Algebra k (K i)) (_ : ∀ i, Module.Finite k (K i))
        (_ : ∀ i, Algebra.IsSeparable k (K i))
        (e : U ≅ ∐ fun i ↦ Spec (.of (K i))),
        e.hom ≫ Sigma.desc (fun i ↦ Spec.map (CommRingCat.ofHom (algebraMap k (K i)))) = f

Tag 03JS, a lemma

Tag 03JS in the Stacks Project.

AlgebraicGeometry.Space.exists_etaleCover_finite_fibre_iff_forall_affine_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FinitenessConditions.lean, line 449.

For a point x of an algebraic space X over S, the following are equivalent: some jointly locally surjective family of étale charts of X has finite fibres above x, and every étale chart of X by an affine scheme has a finite fibre above x.

theorem exists_etaleCover_finite_fibre_iff_forall_affine_etale (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) (x : points B S hS X) :
    (∃ (I : Type u) (U : I → BigFppfOver B S hS) (φ : ∀ i, yoneda.obj (U i) ⟶ X),
      Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) (Sigma.desc φ) ∧
      ∀ i, (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) (φ i) ∧
        (pointsMap B S hS (yoneda.obj (U i)) (φ i) ⁻¹' {x}).Finite) ↔
    (∀ U : BigFppfOver B S hS, IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
      ∀ φ : yoneda.obj U ⟶ X, (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) φ →
        (pointsMap B S hS (yoneda.obj U) φ ⁻¹' {x}).Finite)

AlgebraicGeometry.Space.finite_chartFibre_of_etaleCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsChartFibres.lean, line 309. The attribute's comment: “part (1) implies part (2)”.

Stacks 03JS, part (1) implies part (2). If some family of étale charts of an algebraic space F over S whose coproduct is surjective has finite chart fibres above a point x of |F|, then every étale chart of F with affine source has a finite chart fibre above x.

The family is used only through joint surjectivity on points, which is what surjectivity of the coproduct gives by AlgebraicGeometry.Space.exists_pointsMap_eq_of_isSurjective_sigmaDesc, and affineness of the chart is used only through quasi-compactness of its underlying scheme; the general statement is AlgebraicGeometry.Space.finite_chartFibre_of_jointlySurjective.

theorem finite_chartFibre_of_etaleCover
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) {x : points B S hS F}
    {I : Type u} {V : I → BigFppfOver B S hS} (ψ : ∀ i, yoneda.obj (V i) ⟶ F)
    (hψ : ∀ i, IsEtale B S hS (ψ i)) (hsurj : IsSurjective B S hS (Sigma.desc ψ))
    (hfin : ∀ i, (chartFibre B S hS F (ψ i) x).Finite)
    (U : BigFppfOver B S hS) (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
    (φ : yoneda.obj U ⟶ F) (hφ : IsEtale B S hS φ) :
    (chartFibre B S hS F φ x).Finite

AlgebraicGeometry.Space.exists_etaleCover_finite_chartFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsChartFibres.lean, line 329. The attribute's comment: “part (2) implies part (1)”.

Stacks 03JS, part (2) implies part (1). An algebraic space over S has an étale covering family by affine schemes, so if every étale chart with affine source has a finite chart fibre above a point x of |F|, then the members of one covering family do.

The covering family is the one of Stacks 03FX (AlgebraicGeometry.IsAlgebraicSpace.exists_affine_coproduct_atlas), exactly as in AlgebraicGeometry.Space.HasFiniteFibresOnEveryAffineEtaleChart.hasFiniteFibresOnSomeEtaleCover, whose surjectivity argument this repeats.

theorem exists_etaleCover_finite_chartFibre
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F}
    (h : ∀ U : BigFppfOver B S hS, IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
      ∀ φ : yoneda.obj U ⟶ F, IsEtale B S hS φ → (chartFibre B S hS F φ x).Finite) :
    ∃ (I : Type u) (V : I → BigFppfOver B S hS) (ψ : ∀ i, yoneda.obj (V i) ⟶ F),
      (∀ i, IsEtale B S hS (ψ i)) ∧ IsSurjective B S hS (Sigma.desc ψ) ∧
      ∀ i, (chartFibre B S hS F (ψ i) x).Finite

Tag 03JU, a lemma

Tag 03JU in the Stacks Project.

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

For a point of an algebraic space over S, having a field-valued representative with étale quasi-compact self-intersection projections is equivalent to having a monomorphic field-valued representative.

theorem hasEtaleQuasiCompactFieldRepresentative_iff_hasMonomorphicFieldRepresentative
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (x : points B S hS F) :
    HasEtaleQuasiCompactFieldRepresentative B S hS F x ↔
      HasMonomorphicFieldRepresentative B S hS F x

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

Stacks 03JU, conditions (1) and (2). For a point of an algebraic space over S, finiteness of one relation fibre in one étale chart is equivalent to finiteness of every relation fibre in every étale chart.

theorem hasFiniteRelationFiberAt_iff_everyEtaleChart (hF : IsAlgebraicSpace B S hS F)
    (x : points B S hS F) :
    HasFiniteRelationFiberAt B S hS F x ↔
      HasFiniteRelationFiberAtEveryEtaleChart B S hS F x

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

Stacks 03JU, conditions (2) and (3). For a point of an algebraic space over S, finiteness of every relation fibre in every étale chart is equivalent to having a field-valued representative with étale quasi-compact self-intersection projections.

theorem hasFiniteRelationFiberAtEveryEtaleChart_iff_hasEtaleQuasiCompactFieldRepresentative
    (hF : IsAlgebraicSpace B S hS F) (x : points B S hS F) :
    HasFiniteRelationFiberAtEveryEtaleChart B S hS F x ↔
      HasEtaleQuasiCompactFieldRepresentative B S hS F x

AlgebraicGeometry.Space.HasMonomorphicFieldRepresentative.hasFiniteRelationFiberAtEveryEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationFibreEquivalence.lean, line 74. The attribute's comment: “part (4) implies part (2)”.

Stacks 03JU, condition (4) implies condition (2). If a point x of an algebraic space F over S has a field-valued representative presenting it by a monomorphism out of the spectrum of a field, then for every étale chart φ : h_U ⟶ F and every pair of points of |U| above x the fibre of |h_U ×_F h_U| → |U| × |U| over that pair is finite.

theorem HasMonomorphicFieldRepresentative.hasFiniteRelationFiberAtEveryEtaleChart
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F} (h : HasMonomorphicFieldRepresentative B S hS F x) :
    HasFiniteRelationFiberAtEveryEtaleChart B S hS F x

AlgebraicGeometry.Space.HasFiniteRelationFiberAtEveryEtaleChart.hasEtaleQuasiCompactFieldRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationFibreFieldRepresentative.lean, line 192. The attribute's comment: “part (2) implies part (3)”.

Stacks 03JU, part (2) implies part (3). If every pair of points above a point x of an algebraic space F over S, in every étale chart of F, has finite relation fibre, then x has a field-valued representative whose two self-intersection projections are étale and quasi-compact.

Take a surjective étale chart φ : h_U ⟶ F and a point a of |U| above x, let u be the point of the scheme U underlying a, and let ν : P ⟶ U be the canonical morphism from the spectrum P of the residue field at u. It is a monomorphism, by Stacks 01L6, and the composite f : h_P ⟶ F presents x. Writing the self-fibre-product of f as N = P ×_U (U ×_F U) ×_U P, its first projection factors as the base change of ν followed by the base change of the chart, that is as a monomorphism followed by an étale morphism to P; and N maps monomorphically to U ×_F U with both legs above a, so condition (2) makes |N| finite. The first projection is therefore étale by Tags 02GL and 03DP and quasi-compact by finiteness, and the second is the first conjugated by the symmetry of the fibre product.

theorem HasFiniteRelationFiberAtEveryEtaleChart.hasEtaleQuasiCompactFieldRepresentative
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F}
    (h : HasFiniteRelationFiberAtEveryEtaleChart B S hS F x) :
    HasEtaleQuasiCompactFieldRepresentative B S hS F x

AlgebraicGeometry.Space.HasEtaleQuasiCompactFieldRepresentative.hasMonomorphicFieldRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationFibreMonomorphism.lean, line 420. The attribute's comment: “part (3) implies part (4)”.

Stacks 03JU, part (3) implies part (4). If a point x of an algebraic space F over S has a field-valued representative whose two self-intersection projections are étale and quasi-compact, then x has a field-valued representative presenting it by a monomorphism.

Let f : h_U ⟶ F be the morphism presented by the representative of condition (3), so that U is Spec k for a field k, and let R be the kernel pair of f, which exists because the diagonal of F is representable. The two projections R ⟶ U are étale and quasi-compact, hence finite locally free with R affine, so (U, R) is a finite locally free equivalence relation on an affine scheme; Stacks 03BM represents its fppf quotient sheaf by the spectrum of the invariant ring, which is a field, and which lies in the site because the quotient does not increase size. The descent of f to that quotient sheaf is a monomorphism because R is the kernel pair of f and F is a sheaf, and the resulting field-valued point is dominated by the original one, so it represents the same point of |F|.

theorem HasEtaleQuasiCompactFieldRepresentative.hasMonomorphicFieldRepresentative
    (hF : IsAlgebraicSpace B S hS F) {x : points B S hS F}
    (h : HasEtaleQuasiCompactFieldRepresentative B S hS F x) :
    HasMonomorphicFieldRepresentative B S hS F x

AlgebraicGeometry.Space.HasMonomorphicFieldRepresentative.hasEtaleQuasiCompactFieldRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationFibreMonomorphism.lean, line 466. The attribute's comment: “part (4) implies part (3)”.

Stacks 03JU, part (4) implies part (3). A field-valued representative presenting a point by a monomorphism has invertible self-intersection projections, and an isomorphism is étale and quasi-compact after every representable base change.

theorem HasMonomorphicFieldRepresentative.hasEtaleQuasiCompactFieldRepresentative
    {x : points B S hS F} (h : HasMonomorphicFieldRepresentative B S hS F x) :
    HasEtaleQuasiCompactFieldRepresentative B S hS F x

AlgebraicGeometry.Space.HasFiniteRelationFiberAt.hasFiniteRelationFiberAtEveryEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationFibreTransfer.lean, line 346. The attribute's comment: “part (1) implies part (2)”.

Stacks 03JU, part (1) implies part (2). If some étale chart of an algebraic space F over S has two points above x with finite relation fibre, then every pair of points above x in every étale chart of F has finite relation fibre.

Let φ : h_U ⟶ F be the chart of part (1), with points a, b above x, and let ψ : h_W ⟶ F be any étale chart with points c, d above x. The fibre product T = h_W ×_F h_U is representable with both projections étale, and Tag 03H4 lifts (a, c) and (b, d) to points of |T|. The relation fibre of h_T ⟶ F above that pair of lifts is finite because the relation fibre of φ above (a, b) is, and the relation fibre of ψ above (c, d) is finite because that one is.

The hypothesis _hF that F is an algebraic space is retained from the source statement but is not used.

theorem HasFiniteRelationFiberAt.hasFiniteRelationFiberAtEveryEtaleChart
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F} (h : HasFiniteRelationFiberAt B S hS F x) :
    HasFiniteRelationFiberAtEveryEtaleChart B S hS F x

AlgebraicGeometry.Space.HasFiniteRelationFiberAtEveryEtaleChart.hasFiniteRelationFiberAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationFibreTransfer.lean, line 379. The attribute's comment: “part (2) implies part (1)”.

Stacks 03JU, part (2) implies part (1). An algebraic space over S has a surjective étale chart, which carries a point above x, so the universally quantified condition (2) is witnessed and condition (1) holds.

This is AlgebraicGeometry.Space.hasFiniteRelationFiberAt_of_everyEtaleChart with its hypothesis that some étale chart has a point above x discharged by an atlas of Tag 03FQ, which is surjective on the points of Tag 03BU by Tag 03H5. Together with AlgebraicGeometry.Space.HasFiniteRelationFiberAt.hasFiniteRelationFiberAtEveryEtaleChart it makes conditions (1) and (2) of Stacks 03JU equivalent.

theorem HasFiniteRelationFiberAtEveryEtaleChart.hasFiniteRelationFiberAt
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F} (h : HasFiniteRelationFiberAtEveryEtaleChart B S hS F x) :
    HasFiniteRelationFiberAt B S hS F x

Tag 040U, a lemma

Tag 040U in the Stacks Project.

AlgebraicGeometry.Space.finiteFibres_of_mono_isFinite_fieldFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFibresOneChart.lean, line 244. The attribute's comment: “part (2) implies part (1)”.

Let F be an algebraic space over a scheme S, let x be a point of |F| and let φ : h_U ⟶ F be étale. Suppose some field-valued point of F in the class of x presents it by a monomorphism Spec(k) ⟶ F for which Spec(k) ×_F U is nonempty and finite over Spec(k). Then x lies in the image of |U| → |F| and the fibres of |U| → |F| and of |R| → |F| above x, where R = h_U ×_F h_U, are both finite.

theorem finiteFibres_of_mono_isFinite_fieldFibre (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) {x : points B S hS F} {U : BigFppfOver B S hS}
    {φ : yoneda.obj U ⟶ F} (hφ : IsEtale B S hS φ)
    (h : ∃ p : FieldValuedPoint B S hS F, p.class B S hS F = x ∧
      Mono (fieldMorphism B S hS F p) ∧
      IsFinite B S hS (pullback.fst (fieldMorphism B S hS F p) φ) ∧
      Nonempty (points B S hS (pullback (fieldMorphism B S hS F p) φ))) :
    (∃ a : points B S hS (yoneda.obj U), pointsMap B S hS (yoneda.obj U) φ a = x) ∧
      (chartFibre B S hS F φ x).Finite ∧ (relationFibre B S hS F φ x).Finite

AlgebraicGeometry.Space.exists_mono_isFinite_fieldFibre_of_finiteFibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFibresOneChart.lean, line 267. The attribute's comment: “part (1) implies part (2)”.

A point x of |F| lying in the image of |U| → |F| whose chart and relation fibres above it are finite is presented by a monomorphism Spec(k) ⟶ F for which Spec(k) ×_F U is nonempty and finite over Spec(k), finiteness being the presheaf-relative form.

theorem exists_mono_isFinite_fieldFibre_of_finiteFibres
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F} {U : BigFppfOver B S hS} {φ : yoneda.obj U ⟶ F}
    (hφ : IsEtale B S hS φ)
    (h : (∃ a : points B S hS (yoneda.obj U), pointsMap B S hS (yoneda.obj U) φ a = x) ∧
      (chartFibre B S hS F φ x).Finite ∧ (relationFibre B S hS F φ x).Finite) :
    ∃ p : FieldValuedPoint B S hS F, p.class B S hS F = x ∧
      Mono (fieldMorphism B S hS F p) ∧
      (MorphismProperty.inverseImage
        (@_root_.AlgebraicGeometry.IsFinite.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf
        (pullback.fst (fieldMorphism B S hS F p) φ) ∧
      Nonempty (points B S hS (pullback (fieldMorphism B S hS F p) φ))

Tag 03JV, a lemma

Tag 03JV in the Stacks Project.

AlgebraicGeometry.Space.hasQuasiCompactMonomorphicFieldRepresentative_of_hasQuasiCompactFieldRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FieldBaseChange.lean, line 178. The attribute's comment: “condition (5) implies condition (4)”.

Stacks 03JV, condition (5) implies condition (4). If some field-valued point in the class of x presents it by a quasi-compact morphism, then some field-valued point in that class presents it by a morphism which is both a monomorphism and quasi-compact.

theorem hasQuasiCompactMonomorphicFieldRepresentative_of_hasQuasiCompactFieldRepresentative
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F}
    (h : HasQuasiCompactFieldRepresentative B S hS F x) :
    HasQuasiCompactMonomorphicFieldRepresentative B S hS F x

AlgebraicGeometry.Space.hasFiniteChartAndRelationFibersAt_iff_hasQuasiCompactMonomorphicFieldRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/QuasiCompactMonomorphicPoint.lean, line 209. The attribute's comment: “conditions (1) and (4)”.

For a point of an algebraic space over S, finiteness of the fibres of every affine étale chart and of its self-intersection above the point is equivalent to the point being in the class of a quasi-compact monomorphism from the spectrum of a field.

theorem hasFiniteChartAndRelationFibersAt_iff_hasQuasiCompactMonomorphicFieldRepresentative
    (hX : IsAlgebraicSpace B S hS X) (x : points B S hS X) :
    HasFiniteChartAndRelationFibersAt B S hS X x ↔
      HasQuasiCompactMonomorphicFieldRepresentative B S hS X x

AlgebraicGeometry.Space.HasQuasiCompactMonomorphicFieldRepresentative, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactMonomorphicFieldRepresentative.lean, line 62. The attribute's comment: “part (4)”.

Stacks 03JV, condition (4). A point of F has a quasi-compact monomorphic field-valued representative when some field-valued point in its class presents it by a morphism which is both a monomorphism and quasi-compact.

def HasQuasiCompactMonomorphicFieldRepresentative (x : points B S hS F) : Prop

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

Stacks 03JV, condition (1). For every affine scheme U and every étale morphism φ : h_U ⟶ F, setting R = h_U ×_F h_U, the fibres of |U| → |F| and of |R| → |F| above x are both finite.

def HasFiniteFibresOnEveryAffineEtaleChart (x : points B S hS F) : Prop

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

Stacks 03JV, condition (2). There is a family of étale morphisms φ i : h_{U i} ⟶ F whose coproduct is surjective on points and for which, setting R i = h_{U i} ×_F h_{U i}, the fibres of |U i| → |F| and of |R i| → |F| above x are all finite.

def HasFiniteFibresOnSomeEtaleCover (x : points B S hS F) : Prop

AlgebraicGeometry.Space.HasMonomorphicFieldRepresentativeWithFiniteCharts, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsConditions.lean, line 137. The attribute's comment: “part (3)”.

Stacks 03JV, condition (3). Some field-valued representative of x presents it by a monomorphism Spec(k) ⟶ F whose base change along every étale chart of F with affine source is a finite scheme over k.

def HasMonomorphicFieldRepresentativeWithFiniteCharts (x : points B S hS F) : Prop

AlgebraicGeometry.Space.HasQuasiCompactFieldRepresentative, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsConditions.lean, line 150. The attribute's comment: “part (5)”.

Stacks 03JV, condition (5). Some field-valued point in the class of x presents it by a quasi-compact morphism, the monomorphism condition of condition (4) being dropped.

def HasQuasiCompactFieldRepresentative (x : points B S hS F) : Prop

AlgebraicGeometry.Space.EveryFieldRepresentativeIsQuasiCompact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsConditions.lean, line 157. The attribute's comment: “part (6)”.

Stacks 03JV, condition (6). Every field-valued point in the class of x presents it by a quasi-compact morphism.

def EveryFieldRepresentativeIsQuasiCompact (x : points B S hS F) : Prop

AlgebraicGeometry.Space.HasQuasiCompactMonomorphicFieldRepresentative.hasQuasiCompactFieldRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsConditions.lean, line 166. The attribute's comment: “part (4) implies part (5)”.

Stacks 03JV, condition (4) implies condition (5). Forgetting that the presenting morphism is a monomorphism leaves a quasi-compact field-valued representative.

theorem HasQuasiCompactMonomorphicFieldRepresentative.hasQuasiCompactFieldRepresentative
    {x : points B S hS F}
    (h : HasQuasiCompactMonomorphicFieldRepresentative B S hS F x) :
    HasQuasiCompactFieldRepresentative B S hS F x

AlgebraicGeometry.Space.EveryFieldRepresentativeIsQuasiCompact.hasQuasiCompactFieldRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsConditions.lean, line 177. The attribute's comment: “part (6) implies part (5)”.

Stacks 03JV, condition (6) implies condition (5). A point of |F| is by construction the class of some field-valued point, so a universally quasi-compact class has a quasi-compact representative.

theorem EveryFieldRepresentativeIsQuasiCompact.hasQuasiCompactFieldRepresentative
    {x : points B S hS F}
    (h : EveryFieldRepresentativeIsQuasiCompact B S hS F x) :
    HasQuasiCompactFieldRepresentative B S hS F x

AlgebraicGeometry.Space.HasQuasiCompactMonomorphicFieldRepresentative.everyFieldRepresentativeIsQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsEveryRepresentative.lean, line 39. The attribute's comment: “part (4) implies part (6)”.

If a point x of an algebraic space F over S is the class of a field-valued point whose presenting morphism Spec(k) ⟶ F is a quasi-compact monomorphism, then the presenting morphism of every field-valued point in the class of x is quasi-compact.

theorem HasQuasiCompactMonomorphicFieldRepresentative.everyFieldRepresentativeIsQuasiCompact
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F}
    (h : HasQuasiCompactMonomorphicFieldRepresentative B S hS F x) :
    EveryFieldRepresentativeIsQuasiCompact B S hS F x

AlgebraicGeometry.Space.HasQuasiCompactMonomorphicFieldRepresentative.hasMonomorphicFieldRepresentativeWithFiniteCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsFiniteCharts.lean, line 141. The attribute's comment: “part (4) implies part (3)”.

Stacks 03JV, condition (4) implies condition (3). If a point x of a presheaf F on the big fppf site of S is the class of a field-valued point whose presenting morphism Spec(k) ⟶ F is a quasi-compact monomorphism, then that same monomorphism presents x and has finite base change to every affine étale chart of F.

The representative, the equality of classes and the monomorphism are carried over unchanged; the only content is the finiteness of the base change, which is AlgebraicGeometry.Space.isFinite_pullback_fst_fieldMorphism_of_isQuasiCompact applied to the affine — hence quasi-compact — chart.

theorem hasMonomorphicFieldRepresentativeWithFiniteCharts
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) {x : points B S hS F}
    (h : HasQuasiCompactMonomorphicFieldRepresentative B S hS F x) :
    HasMonomorphicFieldRepresentativeWithFiniteCharts B S hS F x

AlgebraicGeometry.Space.HasQuasiCompactMonomorphicFieldRepresentative.hasFiniteFibresOnEveryAffineEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsFiniteFibres.lean, line 169. The attribute's comment: “part (4) implies part (1)”.

Stacks 03JV, condition (4) implies condition (1). If a point x of an algebraic space F over S is the class of a field-valued point whose presenting morphism Spec(k) ⟶ F is a quasi-compact monomorphism, then for every affine scheme U and every étale φ : h_U ⟶ F the fibres of |U| → |F| and of |R| → |F| above x, where R = h_U ×_F h_U, are both finite.

theorem HasQuasiCompactMonomorphicFieldRepresentative.hasFiniteFibresOnEveryAffineEtaleChart
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F}
    (h : HasQuasiCompactMonomorphicFieldRepresentative B S hS F x) :
    HasFiniteFibresOnEveryAffineEtaleChart B S hS F x

AlgebraicGeometry.Space.HasFiniteFibresOnEveryAffineEtaleChart.hasFiniteFibresOnSomeEtaleCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsFiniteFibres.lean, line 237. The attribute's comment: “part (1) implies part (2)”.

Stacks 03JV, condition (1) implies condition (2). An algebraic space over S has an étale covering family by affine schemes, so the finiteness condition of condition (1), which quantifies over every affine étale chart, is in particular satisfied by the members of one covering family.

theorem HasFiniteFibresOnEveryAffineEtaleChart.hasFiniteFibresOnSomeEtaleCover
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F}
    (h : HasFiniteFibresOnEveryAffineEtaleChart B S hS F x) :
    HasFiniteFibresOnSomeEtaleCover B S hS F x

AlgebraicGeometry.Space.HasQuasiCompactMonomorphicFieldRepresentative.hasFiniteFibresOnSomeEtaleCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsFiniteFibres.lean, line 272. The attribute's comment: “part (4) implies part (2)”.

Stacks 03JV, condition (4) implies condition (2). The composite of the two implications above: condition (4) gives condition (1), which gives condition (2).

theorem HasQuasiCompactMonomorphicFieldRepresentative.hasFiniteFibresOnSomeEtaleCover
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F}
    (h : HasQuasiCompactMonomorphicFieldRepresentative B S hS F x) :
    HasFiniteFibresOnSomeEtaleCover B S hS F x

AlgebraicGeometry.Space.HasFiniteFibresOnSomeEtaleCover.hasFiniteFibresOnEveryAffineEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsFromEtaleCover.lean, line 96. The attribute's comment: “part (2) implies part (1)”.

Stacks 03JV, condition (2) implies condition (1). If some family of étale charts of an algebraic space F over S with surjective coproduct has finite chart and relation fibres above a point x of |F|, then every étale chart of F with affine source has finite chart and relation fibres above x.

The chart half is Stacks 03JS. For the relation half, condition (2) supplies condition (1) of Stacks 03JU at x, so Stacks 03JU, part (1) implies part (2), bounds the relation fibre above each pair of points of the — now finite — chart fibre, and the fibre of |R| → |F| above x is the union of those.

theorem HasFiniteFibresOnSomeEtaleCover.hasFiniteFibresOnEveryAffineEtaleChart
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F} (h : HasFiniteFibresOnSomeEtaleCover B S hS F x) :
    HasFiniteFibresOnEveryAffineEtaleChart B S hS F x

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

Stacks 03JV, conditions (1) and (2) are equivalent. For a point x of an algebraic space F over S, finiteness of the chart and relation fibres above x on every étale chart with affine source holds if and only if it holds on the members of some étale covering family.

This is the first equivalence of Stacks 03JV to be closed. The forward direction is AlgebraicGeometry.Space.HasFiniteFibresOnEveryAffineEtaleChart.hasFiniteFibresOnSomeEtaleCover, which reads the covering family off the affine atlas of Stacks 03FX; the reverse direction is AlgebraicGeometry.Space.HasFiniteFibresOnSomeEtaleCover.hasFiniteFibresOnEveryAffineEtaleChart above, which is the source's own argument through Stacks 03JS and 03JU. Algebraicity of F is used in both directions and is not removable: the atlas of Stacks 03FX and the transfer of Stacks 03JU each require it.

theorem hasFiniteFibresOnEveryAffineEtaleChart_iff_onSomeEtaleCover
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F} :
    HasFiniteFibresOnEveryAffineEtaleChart B S hS F x ↔
      HasFiniteFibresOnSomeEtaleCover B S hS F x

AlgebraicGeometry.Space.HasMonomorphicFieldRepresentativeWithFiniteCharts.hasFiniteFibresOnEveryAffineEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsFromFiniteCharts.lean, line 102. The attribute's comment: “part (3) implies part (1)”.

Stacks 03JV, condition (3) implies condition (1). If a point x of an algebraic space F over S is presented by a monomorphism Spec(k) ⟶ F whose base change along every étale chart with affine source is finite over Spec(k), then for every affine scheme U and every étale φ : h_U ⟶ F the fibres of |U| → |F| and of |R| → |F| above x, where R = h_U ×_F h_U, are both finite.

This is the source's "apply Lemma 040U to every étale morphism U → X with U affine", in the nonemptiness-free form AlgebraicGeometry.Space.finite_chartFibre_and_relationFibre_of_mono_isFinite: finiteness of the field fibre over Spec(k) makes its point set finite and Stacks 03H4 maps that set onto the chart fibre, after which the relation fibre is bounded by Stacks 0AC7 above each pair of points of the chart fibre, the monomorphism being what 0AC7 needs.

theorem HasMonomorphicFieldRepresentativeWithFiniteCharts.hasFiniteFibresOnEveryAffineEtaleChart
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F}
    (h : HasMonomorphicFieldRepresentativeWithFiniteCharts B S hS F x) :
    HasFiniteFibresOnEveryAffineEtaleChart B S hS F x

AlgebraicGeometry.Space.HasMonomorphicFieldRepresentativeWithFiniteCharts.hasFiniteFibresOnSomeEtaleCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsFromFiniteCharts.lean, line 121. The attribute's comment: “part (3) implies part (2)”.

Stacks 03JV, condition (3) implies condition (2). The composite of the implication above with AlgebraicGeometry.Space.HasFiniteFibresOnEveryAffineEtaleChart.hasFiniteFibresOnSomeEtaleCover: a monomorphic representative with finite charts gives finiteness of the chart and relation fibres on every affine étale chart, hence on the members of the affine étale covering family of Stacks 03FX.

theorem HasMonomorphicFieldRepresentativeWithFiniteCharts.hasFiniteFibresOnSomeEtaleCover
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F}
    (h : HasMonomorphicFieldRepresentativeWithFiniteCharts B S hS F x) :
    HasFiniteFibresOnSomeEtaleCover B S hS F x

AlgebraicGeometry.Space.HasQuasiCompactFieldRepresentative.everyFieldRepresentativeIsQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsFromQuasiCompactRepresentative.lean, line 121. The attribute's comment: “part (5) implies part (6)”.

Stacks 03JV, condition (5) implies condition (6). If some field-valued point in the class of a point x of an algebraic space F over S presents it by a quasi-compact morphism Spec(k) ⟶ F, then every field-valued point in the class of x does.

theorem HasQuasiCompactFieldRepresentative.everyFieldRepresentativeIsQuasiCompact
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F}
    (h : HasQuasiCompactFieldRepresentative B S hS F x) :
    EveryFieldRepresentativeIsQuasiCompact B S hS F x

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

Stacks 03JV, conditions (5) and (6) are equivalent. For a point x of an algebraic space F over S, some field-valued point in the class of x has quasi-compact presenting morphism if and only if every one does.

theorem hasQuasiCompactFieldRepresentative_iff_everyFieldRepresentativeIsQuasiCompact
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    {x : points B S hS F} :
    HasQuasiCompactFieldRepresentative B S hS F x ↔
      EveryFieldRepresentativeIsQuasiCompact B S hS F x

AlgebraicGeometry.Space.hasQuasiCompactMonomorphicFieldRepresentative_of_finiteCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointsZariskiChart.lean, line 128. The attribute's comment: “part (3) implies part (4)”.

Stacks 03JV, condition (3) implies condition (4). Let F be an algebraic space over S and let x be a point of F. If some field-valued representative of x presents it by a monomorphism whose base change along every affine étale chart of F is finite, then that monomorphism is in addition quasi-compact.

A surjective étale chart h_V ⟶ F by a single object of the site exists by Stacks 03FX, and V is covered by its affine open subschemes, each of which is an object of the site whose composite to F is an affine étale chart. The hypothesis applies to those charts, and the resulting fibre products are affine objects of the site whose projections to the members of the covering are morphisms of affine schemes, hence quasi-compact. The Zariski-local criterion AlgebraicGeometry.Space.isQuasiCompact_pullback_snd_of_openCover turns that into quasi-compactness of the base change of the representative along the chart, which is condition (4) of Stacks 03KG, and AlgebraicGeometry.Space.isQuasiCompact_of_surjectiveEtale_atlas is its condition (4) implies condition (1).

Together with the converse this closes the adjacent equivalence of conditions (3) and (4) of Stacks 03JV.

theorem hasQuasiCompactMonomorphicFieldRepresentative_of_finiteCharts
    (hF : IsAlgebraicSpace B S hS F) {x : points B S hS F}
    (h : HasMonomorphicFieldRepresentativeWithFiniteCharts B S hS F x) :
    HasQuasiCompactMonomorphicFieldRepresentative B S hS F x

Tag 03JT, a lemma

Tag 03JT in the Stacks Project.

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

Stacks 03JT. For an algebraic space X over S the following are equivalent: (1) there is a jointly surjective family of étale charts of X by schemes, each with universally bounded fibres, and (2) every étale chart of X by an affine scheme has universally bounded fibres, which is AlgebraicGeometry.Space.IsReasonableSpace.

theorem isReasonableSpace_iff_exists_boundedEtaleCover
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X) :
    IsReasonableSpace B S hS X ↔
      ∃ (I : Type u) (U : I → BigFppfOver B S hS) (φ : ∀ i, yoneda.obj (U i) ⟶ X),
        Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) (Sigma.desc φ) ∧
        ∀ i, (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) (φ i) ∧
          HasUniversallyBoundedFibers B S hS (U i) (φ i)

Tag 03IH, a lemma

Tag 03IH in the Stacks Project.

AlgebraicGeometry.Space.isVeryReasonableSpace_iff_exists_isZariskiCover_quasiCompact_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/VeryReasonableAtlas.lean, line 118.

Stacks 03IH. An algebraic space over S is very reasonable — it has a jointly surjective family of étale charts by schemes whose two self-intersection projections are quasi-compact — if and only if it has a Zariski covering by open subspaces each of which carries a quasi-compact surjective étale chart by a scheme.

theorem isVeryReasonableSpace_iff_exists_isZariskiCover_quasiCompact_chart
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X) :
    IsVeryReasonableSpace B S hS X ↔
      ∃ (I : Type u) (Xᵢ : I → Subfunctor X), IsZariskiCover B S hS I Xᵢ ∧
        ∃ (U : I → BigFppfOver B S hS) (φ : ∀ i, yoneda.obj (U i) ⟶ (Xᵢ i).toFunctor),
          ∀ i, IsEtale B S hS (φ i) ∧
            Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) (φ i) ∧
            IsQuasiCompact B S hS (φ i)

Sources

LeanAlgebraicGeometry.locallyQuasiFinite_of_etale · AlgebraicGeometry.flat_and_generalizingMap_of_etale · AlgebraicGeometry.finite_preimage_singleton_of_etale_of_quasiCompact · AlgebraicGeometry.discreteTopology_fiber · AlgebraicGeometry.unramified_of_etale · AlgebraicGeometry.etale_iff_iso_coproduct_spectra_finite_separable · AlgebraicGeometry.Space.exists_etaleCover_finite_fibre_iff_forall_affine_etale · AlgebraicGeometry.Space.finite_chartFibre_of_etaleCover

Section68.5 Conditions on algebraic spaces #

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

Tag 03JX, a lemma

Tag 03JX in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_isQuasiSeparatedScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 91. The attribute's comment: “(iota) implies (theta)”.

Condition (ι) implies condition (θ): an algebraic space which is a quasi-separated scheme is representable.

theorem isRepresentable_of_isQuasiSeparatedScheme
    (h : IsQuasiSeparatedScheme B S hS X) : X.IsRepresentable

AlgebraicGeometry.Space.isAbsolutelyZariskiLocallyQuasiSeparated_of_isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 101. The attribute's comment: “(eta) implies (zeta)”.

Condition (η) implies condition (ζ): a quasi-separated algebraic space is Zariski locally quasi-separated.

theorem isAbsolutelyZariskiLocallyQuasiSeparated_of_isAbsolutelyQuasiSeparated
    (hX : IsAlgebraicSpace B S hS X) (h : IsAbsolutelyQuasiSeparated B S hS hZ X) :
    IsAbsolutelyZariskiLocallyQuasiSeparated B S hS hZ X

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_isQuasiSeparatedScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 130. The attribute's comment: “(iota) implies (eta)”.

Condition (ι) implies condition (η): an algebraic space which is a quasi-separated scheme is a quasi-separated algebraic space.

theorem isAbsolutelyQuasiSeparated_of_isQuasiSeparatedScheme
    (h : IsQuasiSeparatedScheme B S hS X) : IsAbsolutelyQuasiSeparated B S hS hZ X

AlgebraicGeometry.Space.hasFiniteChartFibersAtEveryPoint_of_hasFiniteChartAndRelationFibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 156. The attribute's comment: “(gamma) implies (alpha)”.

Condition (γ) implies condition (α): if every affine étale chart has finite fibres together with its self-intersection, then every affine étale chart has finite fibres.

theorem hasFiniteChartFibersAtEveryPoint_of_hasFiniteChartAndRelationFibers
    (h : HasFiniteChartAndRelationFibersAtEveryPoint B S hS X) :
    HasFiniteChartFibersAtEveryPoint B S hS X

AlgebraicGeometry.Space.hasFiniteRelationFibersAtEveryPoint_of_hasFiniteChartAndRelationFibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 189. The attribute's comment: “(gamma) implies (beta)”.

Condition (γ) implies condition (β), in the form of condition (1) of Stacks 03JU: for an algebraic space satisfying (γ), every point has an étale chart and a pair of points above it whose relation fibre is finite.

theorem hasFiniteRelationFibersAtEveryPoint_of_hasFiniteChartAndRelationFibers
    (hX : IsAlgebraicSpace B S hS X)
    (h : HasFiniteChartAndRelationFibersAtEveryPoint B S hS X) :
    HasFiniteRelationFibersAtEveryPoint B S hS X

AlgebraicGeometry.Space.hasFiniteChartAndRelationFibersAtEveryPoint_of_alpha_and_beta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 208. The attribute's comment: “(alpha) and (beta) imply (gamma)”.

Conditions (α) and (β) imply condition (γ): an algebraic space all of whose affine étale charts have finite fibres and all of whose points have a finite relation fibre satisfies condition (γ).

theorem hasFiniteChartAndRelationFibersAtEveryPoint_of_alpha_and_beta
    (hX : IsAlgebraicSpace B S hS X)
    (hα : HasFiniteChartFibersAtEveryPoint B S hS X)
    (hβ : HasFiniteRelationFibersAtEveryPoint B S hS X) :
    HasFiniteChartAndRelationFibersAtEveryPoint B S hS X

AlgebraicGeometry.Space.hasFiniteChartAndRelationFibersAtEveryPoint_iff_alpha_and_beta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 241. The attribute's comment: “(gamma) iff (alpha) and (beta)”.

Condition (γ) is equivalent to conditions (α) and (β) together: for an algebraic space over S, finiteness of the fibres of every affine étale chart together with its self-intersection is equivalent to finiteness of the fibres of every affine étale chart together with finiteness of one relation fibre at every point.

theorem hasFiniteChartAndRelationFibersAtEveryPoint_iff_alpha_and_beta
    (hX : IsAlgebraicSpace B S hS X) :
    HasFiniteChartAndRelationFibersAtEveryPoint B S hS X ↔
      HasFiniteChartFibersAtEveryPoint B S hS X ∧
        HasFiniteRelationFibersAtEveryPoint B S hS X

AlgebraicGeometry.Space.isAbsolutelyZariskiLocallyQuasiSeparated_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 629. The attribute's comment: “(theta) implies (zeta)”.

Condition (θ) implies condition (ζ): a representable algebraic space over S is Zariski locally quasi-separated.

theorem isAbsolutelyZariskiLocallyQuasiSeparated_of_isRepresentable
    (hX : IsAlgebraicSpace B S hS X) (h : X.IsRepresentable) :
    IsAbsolutelyZariskiLocallyQuasiSeparated B S hS hZ X

AlgebraicGeometry.Space.hasFiniteChartAndRelationFibersAtEveryPoint_of_isReasonableSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReasonableImpliesFiniteFibres.lean, line 72. The attribute's comment: “(delta) implies (gamma)”.

Stacks 03JX, (δ) ⇒ (γ). A reasonable algebraic space satisfies condition (γ): above every point of it, every étale chart by an affine scheme has a finite fibre, and so does the self-intersection of that chart.

theorem hasFiniteChartAndRelationFibersAtEveryPoint_of_isReasonableSpace
    (hX : IsAlgebraicSpace B S hS X) (hr : IsReasonableSpace B S hS X) :
    HasFiniteChartAndRelationFibersAtEveryPoint B S hS X

AlgebraicGeometry.Space.isReasonableSpace_of_isVeryReasonableSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/VeryReasonableImpliesReasonable.lean, line 177. The attribute's comment: “(epsilon) implies (delta)”.

Stacks 03JX, (ε) ⇒ (δ). A very reasonable algebraic space over S is reasonable: every étale chart of it by an affine scheme has universally bounded fibres.

This is also the third implication of Stacks 03M5. The given family of charts is refined by the affine opens of its sources, which have universally bounded fibres over the space by AlgebraicGeometry.Space.hasUniversallyBoundedFibers_affineOpen_comp_of_isQuasiCompact, and Stacks 03JT turns one such jointly surjective family into reasonableness.

theorem isReasonableSpace_of_isVeryReasonableSpace
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (h : IsVeryReasonableSpace B S hS X) :
    IsReasonableSpace B S hS X

AlgebraicGeometry.Space.isVeryReasonableSpace_of_isAbsolutelyZariskiLocallyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ZariskiLocallyQuasiSeparatedVeryReasonable.lean, line 238. The attribute's comment: “(zeta) implies (epsilon)”.

A Zariski locally quasi-separated algebraic space over S is very reasonable: it admits a jointly surjective family of étale charts by schemes whose two self-intersection projections are quasi-compact.

theorem isVeryReasonableSpace_of_isAbsolutelyZariskiLocallyQuasiSeparated
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hζ : IsAbsolutelyZariskiLocallyQuasiSeparated B S hS hZ X) :
    IsVeryReasonableSpace B S hS X

Tag 03KE, a lemma

Tag 03KE in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_isZariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 271. The attribute's comment: “the case (theta)”.

Condition (θ) is Zariski local: an algebraic space with a Zariski open covering by representable open subspaces is representable.

theorem isRepresentable_of_isZariskiCover (hX : IsAlgebraicSpace B S hS X)
    (I : Type u) (Xᵢ : I → Subfunctor X) (hcover : IsZariskiCover B S hS I Xᵢ)
    (hθ : ∀ i : I, (Xᵢ i).toFunctor.IsRepresentable) : X.IsRepresentable

AlgebraicGeometry.Space.hasFiniteChartFibersAtEveryPoint_of_isZariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 309. The attribute's comment: “the case (alpha)”.

Condition (α) is Zariski local: an algebraic space with a Zariski open covering by open subspaces satisfying condition (α) satisfies condition (α).

theorem hasFiniteChartFibersAtEveryPoint_of_isZariskiCover (hX : IsAlgebraicSpace B S hS X)
    (I : Type u) (Xᵢ : I → Subfunctor X) (hcover : IsZariskiCover B S hS I Xᵢ)
    (hα : ∀ i : I, HasFiniteChartFibersAtEveryPoint B S hS (Xᵢ i).toFunctor) :
    HasFiniteChartFibersAtEveryPoint B S hS X

AlgebraicGeometry.Space.hasFiniteRelationFibersAtEveryPoint_of_isZariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 409. The attribute's comment: “the case (beta)”.

Condition (β) is Zariski local: an algebraic space with a Zariski open covering by open subspaces satisfying condition (β) satisfies condition (β).

theorem hasFiniteRelationFibersAtEveryPoint_of_isZariskiCover
    (hX : IsAlgebraicSpace B S hS X) (I : Type u) (Xᵢ : I → Subfunctor X)
    (hcover : IsZariskiCover B S hS I Xᵢ)
    (hβ : ∀ i : I, HasFiniteRelationFibersAtEveryPoint B S hS (Xᵢ i).toFunctor) :
    HasFiniteRelationFibersAtEveryPoint B S hS X

AlgebraicGeometry.Space.hasFiniteChartAndRelationFibersAtEveryPoint_of_isZariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 438. The attribute's comment: “the case (gamma)”.

Condition (γ) is Zariski local: an algebraic space with a Zariski open covering by open subspaces satisfying condition (γ) satisfies condition (γ).

theorem hasFiniteChartAndRelationFibersAtEveryPoint_of_isZariskiCover
    (hX : IsAlgebraicSpace B S hS X) (I : Type u) (Xᵢ : I → Subfunctor X)
    (hcover : IsZariskiCover B S hS I Xᵢ)
    (hγ : ∀ i : I, HasFiniteChartAndRelationFibersAtEveryPoint B S hS (Xᵢ i).toFunctor) :
    HasFiniteChartAndRelationFibersAtEveryPoint B S hS X

AlgebraicGeometry.Space.isAbsolutelyZariskiLocallyQuasiSeparated_of_isZariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 550. The attribute's comment: “the case (zeta)”.

Condition (ζ) is Zariski local: an algebraic space with a Zariski open covering by open subspaces which are Zariski locally quasi-separated is Zariski locally quasi-separated.

theorem isAbsolutelyZariskiLocallyQuasiSeparated_of_isZariskiCover
    (I : Type u) (Xᵢ : I → Subfunctor X) (hcover : IsZariskiCover B S hS I Xᵢ)
    (hζ : ∀ i : I, IsAbsolutelyZariskiLocallyQuasiSeparated B S hS hZ (Xᵢ i).toFunctor) :
    IsAbsolutelyZariskiLocallyQuasiSeparated B S hS hZ X

AlgebraicGeometry.Space.isReasonableSpace_of_isZariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReasonableZariskiLocal.lean, line 82. The attribute's comment: “the case (delta)”.

Stacks 03KE, the case (δ). An algebraic space with a Zariski open covering by reasonable open subspaces is reasonable.

Given an affine étale chart φ : h_U ⟶ X, the point sets of the members of the covering pull back to an open cover of the affine scheme U, which therefore has a finite refinement by affine opens each of which maps into a single member. Each of those affine opens is an affine étale chart of the member it maps into, so reasonableness there bounds its fibres, and Stacks 03JO carries the bound along the inclusion of the member; the finitely many bounds then assemble to one for φ.

theorem isReasonableSpace_of_isZariskiCover
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (I : Type u) (Xᵢ : I → Subfunctor X) (hcover : IsZariskiCover B S hS I Xᵢ)
    (hδ : ∀ i : I, IsReasonableSpace B S hS (Xᵢ i).toFunctor) :
    IsReasonableSpace B S hS X

AlgebraicGeometry.Space.isVeryReasonableSpace_of_isZariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/VeryReasonableConditions.lean, line 64. The attribute's comment: “property_epsilon”.

Stacks 03KE, the case (ε). Property (ε) of Stacks 03JX — very reasonableness — is local for Zariski coverings: a presheaf on the big fppf site of S admitting a Zariski covering by very reasonable open subspaces is itself very reasonable.

theorem isVeryReasonableSpace_of_isZariskiCover
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (I : Type u) (Xᵢ : I → Subfunctor X)
    (hcover : IsZariskiCover B S hS I Xᵢ)
    (hε : ∀ i : I, IsVeryReasonableSpace B S hS (Xᵢ i).toFunctor) :
    IsVeryReasonableSpace B S hS X

Tag 03KF, a lemma

Tag 03KF in the Stacks Project.

AlgebraicGeometry.Space.isDecentSpace_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PropertyGammaPermanence.lean, line 76. The attribute's comment: “property_gamma, as condition (4) of Stacks 03JV”.

Decency passes from the target of a representable morphism of presheaves on the big fppf site of S to its source, when the source is an algebraic space.

theorem isDecentSpace_of_relativelyRepresentable
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f) (hY : IsDecentSpace B S hS Y) :
    IsDecentSpace B S hS X

AlgebraicGeometry.Space.hasFiniteChartAndRelationFibersAtEveryPoint_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PropertyGammaPermanence.lean, line 109. The attribute's comment: “property_gamma”.

Let f : X ⟶ Y be a representable morphism of algebraic spaces over S. If every étale chart of Y by an affine scheme and the self-intersection of that chart have finite fibres above every point, then the same holds for X.

theorem hasFiniteChartAndRelationFibersAtEveryPoint_of_relativelyRepresentable
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f)
    (hYγ : HasFiniteChartAndRelationFibersAtEveryPoint B S hS Y) :
    HasFiniteChartAndRelationFibersAtEveryPoint B S hS X

AlgebraicGeometry.Space.isReasonableSpace_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReasonablePermanence.lean, line 72. The attribute's comment: “property_delta”.

Stacks 03KF, the case (δ), and the reasonable half of Stacks 0ABT. Property (δ) of Stacks 03JX — reasonableness — passes from the target of a representable morphism of algebraic spaces over S to its source.

A jointly surjective family of étale charts of Y with universally bounded fibres, which reasonableness of Y provides through Stacks 03JT, base changes along f to a family of étale charts of X; the bounds survive by Stacks 03JN and joint surjectivity survives because the squares are cartesian, so Stacks 03JT applies to X.

theorem isReasonableSpace_of_relativelyRepresentable
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f) (hYr : IsReasonableSpace B S hS Y) :
    IsReasonableSpace B S hS X

AlgebraicGeometry.Space.hasFiniteRelationFibersAtEveryPoint_of_relativelyRepresentable_of_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RepresentablePermanence.lean, line 179. The attribute's comment: “property_beta”.

Stacks 03KF, the case (β). Property (β) of Stacks 03JX passes from the target of a representable morphism of algebraic spaces over S to its source.

Property (β) is condition (1) of Stacks 03JU at every point, which is how AlgebraicGeometry.Space.HasFiniteRelationFibersAtEveryPoint spells it. The source's argument runs on condition (4) instead, a monomorphic field-valued representative, so the hypothesis on Y is carried across the equivalences of Stacks 03JU before AlgebraicGeometry.Space.hasFiniteRelationFibersAtEveryPoint_of_relativelyRepresentable transports it to X; that is what makes Y an algebraic space a hypothesis here.

theorem hasFiniteRelationFibersAtEveryPoint_of_relativelyRepresentable_of_target
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f)
    (hYβ : HasFiniteRelationFibersAtEveryPoint B S hS Y) :
    HasFiniteRelationFibersAtEveryPoint B S hS X

AlgebraicGeometry.Space.isRepresentable_of_relativelyRepresentable_of_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RepresentablePermanence.lean, line 198. The attribute's comment: “property_theta”.

Stacks 03KF, property (θ). Property (θ) of an algebraic space over S is representability of its functor of points, so this is the case 𝒫 = (θ): for a representable morphism f : X ⟶ Y, representability of Y gives representability of X.

Neither the sheaf condition nor an atlas is used, so the implication holds for presheaves on any category; that general form is Stacks 03KC.

theorem isRepresentable_of_relativelyRepresentable_of_target
    (f : X ⟶ Y) (hf : yoneda.relativelyRepresentable f) (hYθ : Y.IsRepresentable) :
    X.IsRepresentable

AlgebraicGeometry.Space.isVeryReasonableSpace_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/VeryReasonablePermanence.lean, line 114. The attribute's comment: “property_epsilon”.

Property (ε) of Stacks 03JX, very reasonableness, passes from the target of a representable morphism of presheaves on the big fppf site of S to its source.

theorem isVeryReasonableSpace_of_relativelyRepresentable
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f) (hY : IsVeryReasonableSpace B S hS Y) :
    IsVeryReasonableSpace B S hS X

Sources

LeanAlgebraicGeometry.Space.isRepresentable_of_isQuasiSeparatedScheme · AlgebraicGeometry.Space.isAbsolutelyZariskiLocallyQuasiSeparated_of_isAbsolutelyQuasiSeparated · AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_isQuasiSeparatedScheme · AlgebraicGeometry.Space.hasFiniteChartFibersAtEveryPoint_of_hasFiniteChartAndRelationFibers · AlgebraicGeometry.Space.hasFiniteRelationFibersAtEveryPoint_of_hasFiniteChartAndRelationFibers · AlgebraicGeometry.Space.hasFiniteChartAndRelationFibersAtEveryPoint_of_alpha_and_beta · AlgebraicGeometry.Space.hasFiniteChartAndRelationFibersAtEveryPoint_iff_alpha_and_beta · AlgebraicGeometry.Space.isAbsolutelyZariskiLocallyQuasiSeparated_of_isRepresentable

Section68.6 Reasonable and decent algebraic spaces #

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

Tag 03I8, a definition

Tag 03I8 in the Stacks Project.

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

Stacks 03I8, decent. An algebraic space over S is decent when every one of its points satisfies the equivalent conditions of Stacks 03JV, taken here in the form of condition (4): a quasi-compact monomorphism from the spectrum of a field.

abbrev IsDecentSpace : Prop

AlgebraicGeometry.Space.IsReasonableSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Reasonable.lean, line 117. The attribute's comment: “reasonable”.

Stacks 03I8, reasonable. An algebraic space over S is reasonable when it satisfies the equivalent conditions of Stacks 03JT, taken here in the form of condition (2): every étale chart of it by an affine scheme has universally bounded fibres.

abbrev IsReasonableSpace : Prop

AlgebraicGeometry.Space.IsVeryReasonableSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Reasonable.lean, line 131. The attribute's comment: “very_reasonable”.

Stacks 03I8, very reasonable. An algebraic space over S is very reasonable when it satisfies the equivalent conditions of Stacks 03IH, taken here in the form of condition (2), which is property (ε) of Stacks 03JX: there is a jointly surjective family of étale charts by schemes whose two self-intersection projections are quasi-compact.

abbrev IsVeryReasonableSpace : Prop

Tag 03ID, an example

Tag 03ID in the Stacks Project.

AlgebraicGeometry.AffineLineTranslation.not_isDecentSpace_translationQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineLineTranslationNotDecent.lean, line 759.

Stacks 03ID. The quotient of the affine line over a field of characteristic zero by the integer translations is not a decent algebraic space: the point of the quotient represented by the generic point of the line has no monomorphic field-valued representative.

theorem not_isDecentSpace_translationQuotient (k : Type u) [Field k] [CharZero k]
    (B : BigFppfSite.{u}) (hS : B.Contains (Spec (.of k)))
    (hG : B.Contains (Spec (.of (RatFunc k))))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)] :
    ¬ Space.IsDecentSpace B (Spec (.of k)) hS
      (translationQuotient k B hS (contains_affineLine k B hS))

Tag 03K0, a lemma

Tag 03K0 in the Stacks Project.

AlgebraicGeometry.Space.exists_directedApproximation_of_isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReasonableFilteredApproximation/DirectedApproximation.lean, line 283. The attribute's comment: “correction: clause (1) as literally stated holds only for quasi-separated X,and is proved here under that hypothesis”.

Stacks 03K0 for a quasi-separated space. A quasi-compact, quasi-separated algebraic space over S carries a directed approximation in the sense of the source, with clause (1) in its original form over all quasi-compact test schemes: the constant system indexed by the one-object category works, all of whose transition morphisms and coprojections are identities.

By AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_directedApproximation the quasi-separatedness hypothesis is also necessary when X is a scheme, so the statement of Stacks 03K0 is not available for a general quasi-compact reasonable X; the hypothesis is the correction, and an approximation of a non-quasi-separated X exists only after clause (1) is restricted to quasi-compact quasi-separated test schemes.

theorem exists_directedApproximation_of_isAbsolutelyQuasiSeparated
    (X : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (hX : IsAlgebraicSpace B S hS X.obj)
    (hqc : IsQuasiCompactSpace B S hS X.obj)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X.obj) :
    Nonempty (DirectedApproximation B S hS hZ X)

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_directedApproximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReasonableFilteredApproximation/DirectedApproximation.lean, line 334. The attribute's comment: “refutation of clause (1) as stated: it forces X quasi-separated, so thecorrect clause (1) restricts to quasi-compact quasi-separated test schemes”.

Clause (1) of Stacks 03K0, as stated, forces X to be quasi-separated. Let X be a quasi-compact algebraic space which is a scheme, and suppose it carries a directed approximation by quasi-separated algebraic spaces satisfying clause (1) in the form the source states it, over every quasi-compact test scheme. Testing clause (1) on T = X itself — legitimate, since X is a quasi-compact scheme over S — produces a section of one coprojection X i ⟶ X, exhibiting X as a retract of the quasi-separated space X i; so X is quasi-separated.

Consequently Stacks 03K0 is false as stated: a quasi-compact scheme which is not quasi-separated is a quasi-compact reasonable algebraic space carrying no such system. The repair supported by the source's own proof is to restrict clause (1) to test schemes that are quasi-compact and quasi-separated.

theorem isAbsolutelyQuasiSeparated_of_directedApproximation
    (X : Sheaf (BigFppfOver.topology B S hS) (Type u))
    [hrep : X.obj.IsRepresentable]
    (hqc : IsQuasiCompactSpace B S hS X.obj)
    (A : DirectedApproximation B S hS hZ X) :
    IsAbsolutelyQuasiSeparated B S hS hZ X.obj

AlgebraicGeometry.Space.exists_correctedDirectedApproximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReasonableFilteredApproximation/Existence.lean, line 465. The attribute's comment: “clause (1) in the corrected form: the test schemes are the quasi-compactquasi-separated ones, which is what the source's proof supports”.

Stacks 03K0. A quasi-compact reasonable algebraic space over S is the colimit, in sheaves, of a directed system of quasi-compact and quasi-separated algebraic spaces, and the system can be arranged to satisfy clauses (1), (2) and (3) of the source. No quasi-separatedness is assumed of X.

The system is the one of the source's proof, and it is not constant: by Stacks 03H6 write X = U/R with U affine, and index the system by the quasi-compact open subschemes R' ⊆ R which are still equivalence relations on U, ordered by inclusion. Reasonableness bounds the degrees of the fibres of U ⟶ X by some N (Stacks 03JL), and that bound is what makes the index set cofinal in the quasi-compact opens of R and hence directed: the chain of composites A ↦ c(A ×_{s, U, t} A) out of a quasi-compact open A containing e(U) stabilises at step N, because a chain of length exceeding N repeats a point in a fibre of U(k) ⟶ X(k) for an algebraically closed k and can be shortened. Each stage U/R' is an algebraic space by Stacks 02WW, and is quasi-separated by Stacks 07S4 because R' is quasi-compact and U affine — whereas R itself is quasi-compact only when X is quasi-separated, which is precisely when the system collapses to a single stage.

Clause (1) is the corrected one: injectivity of colim X i(T) ⟶ X(T) over every quasi-compact test scheme T, surjectivity over the quasi-compact quasi-separated ones; see AlgebraicGeometry.Space.CorrectedDirectedApproximation. Over all quasi-compact T the surjectivity fails, by AlgebraicGeometry.Space.exists_quasiCompact_reasonable_isEmpty_directedApproximation.

theorem exists_correctedDirectedApproximation
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hqc : AlgebraicGeometry.Space.IsQuasiCompactSpace B S hS X)
    (hr : IsReasonableSpace B S hS X) :
    Nonempty (CorrectedDirectedApproximation B S hS hZ ⟨X, hX.isSheaf⟩)

AlgebraicGeometry.Space.exists_quasiCompact_reasonable_isEmpty_directedApproximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReasonableFilteredApproximationCounterexample.lean, line 161. The attribute's comment: “refutation of clause (1) as stated, assuming nothing: the doubled-origin scheme of Example 01KL is a quasi-compact reasonable algebraic space with no such system”.

Stacks 03K0 is false as stated. There are a big fppf site, a scheme over its terminal object, and no hypotheses at all, for which the lemma's hypotheses hold and its conclusion fails: the represented sheaf is an algebraic space, representable, quasi-compact and reasonable, and it carries no directed system of quasi-compact quasi-separated algebraic spaces with the three clauses of 03K0, because clause (1) over every quasi-compact test scheme forces quasi-separatedness of the space itself — a hypothesis 03K0 does not make.

The witness is the doubled-origin scheme of Example 01KL, and the three facts about it that the refutation needs are proved in this library: quasi-compactness (AlgebraicGeometry.compactSpace_scheme), failure of quasi-separatedness (AlgebraicGeometry.not_quasiSeparatedSpace_scheme) and reasonableness (AlgebraicGeometry.Space.isReasonableSpace_yoneda, the composite (θ) ⇒ (δ) of Stacks 03JX).

The repair supported by the source's own proof is AlgebraicGeometry.Space.exists_correctedDirectedApproximation, whose clause (1) quantifies over test schemes that are quasi-compact and quasi-separated; it holds for every quasi-compact reasonable algebraic space, this one included.

theorem exists_quasiCompact_reasonable_isEmpty_directedApproximation (k : Type u) [Field k] :
    ∃ (B : BigFppfSite.{u}) (hZ : B.Contains (⊤_ Scheme.{u}))
      (X : Sheaf (BigFppfOver.topology B (⊤_ Scheme.{u}) hZ) (Type u))
      (_ : X.obj.IsRepresentable),
      IsAlgebraicSpace B (⊤_ Scheme.{u}) hZ X.obj ∧
      IsQuasiCompactSpace B (⊤_ Scheme.{u}) hZ X.obj ∧
      IsReasonableSpace B (⊤_ Scheme.{u}) hZ X.obj ∧
      IsEmpty (DirectedApproximation B (⊤_ Scheme.{u}) hZ hZ X)

Tag 0ABT, a lemma

Tag 0ABT in the Stacks Project.

AlgebraicGeometry.Space.isDecentSpace_relocalizeRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FieldBaseChange.lean, line 217. The attribute's comment: “decency under change of affine base”.

Decency of an algebraic space over an affine scheme S is preserved by restriction along a morphism g : S' ⟶ S of affine schemes of the site: every point of the restricted space is presented by a quasi-compact monomorphism from the spectrum of a field.

theorem isDecentSpace_relocalizeRestrict (B : BigFppfSite.{u}) (S S' : Scheme.{u})
    (hS : B.Contains S) (hS' : B.Contains S')
    [IsAffine S] [IsAffine S']
    (g : B.obj hS' ⟶ B.obj hS)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (hdecent : IsDecentSpace B S hS X) :
    IsDecentSpace B S' hS' ((CategoryTheory.OverShriek.relocalizeRestrict g).obj X)

AlgebraicGeometry.Space.hasMonomorphicFieldRepresentative_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RepresentablePermanence.lean, line 101. The attribute's comment: “decent, as condition (4) of Stacks 03JU at every point”.

Stacks 0ABT, the decent case in the form of condition (4) of Stacks 03JU. Let f : X ⟶ Y be a representable morphism of presheaves on the big fppf site over S. If every point of Y is the class of a field-valued point presenting it by a monomorphism, then so is every point of X.

theorem hasMonomorphicFieldRepresentative_of_relativelyRepresentable (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f)
    (hY : ∀ y : points B S hS Y, HasMonomorphicFieldRepresentative B S hS Y y)
    (x : points B S hS X) :
    HasMonomorphicFieldRepresentative B S hS X x

AlgebraicGeometry.Space.hasFiniteRelationFibersAtEveryPoint_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RepresentablePermanence.lean, line 149. The attribute's comment: “decent, as property (β) of Stacks 03JX”.

Stacks 0ABT, the decent case as property (β) of Stacks 03JX. The source of a representable morphism into a presheaf all of whose points have a monomorphic field-valued representative has property (β): every point of it has a finite relation fibre in some étale chart.

This is the reading of AlgebraicGeometry.Space.hasMonomorphicFieldRepresentative_of_relativelyRepresentable through the equivalences of Stacks 03JU, which need the source to be an algebraic space.

theorem hasFiniteRelationFibersAtEveryPoint_of_relativelyRepresentable
    (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f)
    (hY : ∀ y : points B S hS Y, HasMonomorphicFieldRepresentative B S hS Y y) :
    HasFiniteRelationFibersAtEveryPoint B S hS X

Declarations registered for the tag:

AlgebraicGeometry.Space.isDecentSpace_of_relativelyRepresentable, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PropertyGammaPermanence.lean, line 128 (StacksFrontier): “decent”.
AlgebraicGeometry.Space.isReasonableSpace_of_relativelyRepresentable, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReasonablePermanence.lean, line 90 (StacksFrontier): “reasonable”.

Tag 0ABU, a lemma

Tag 0ABU in the Stacks Project.

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

Stacks 0ABU, the decent case. An algebraic space over S étale over a decent algebraic space over S is decent.

theorem isDecentSpace_of_isEtale (f : X ⟶ Y) (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hf : IsEtale B S hS f)
    (hdec : IsDecentSpace B S hS Y) :
    IsDecentSpace B S hS X

AlgebraicGeometry.Space.isReasonableSpace_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/EtaleSourceReasonableness.lean, line 108. The attribute's comment: “reasonable”.

Stacks 0ABU, the reasonable case. An algebraic space over S étale over a reasonable algebraic space over S is reasonable.

theorem isReasonableSpace_of_isEtale (f : X ⟶ Y) (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hf : IsEtale B S hS f)
    (hreas : IsReasonableSpace B S hS Y) :
    IsReasonableSpace B S hS X

Sources

LeanAlgebraicGeometry.Space.IsDecentSpace · AlgebraicGeometry.Space.IsReasonableSpace · AlgebraicGeometry.Space.IsVeryReasonableSpace · AlgebraicGeometry.AffineLineTranslation.not_isDecentSpace_translationQuotient · AlgebraicGeometry.Space.exists_directedApproximation_of_isAbsolutelyQuasiSeparated · AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_directedApproximation · AlgebraicGeometry.Space.exists_correctedDirectedApproximation · AlgebraicGeometry.Space.exists_quasiCompact_reasonable_isEmpty_directedApproximation

Section68.7 Points and specializations #

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

Tag 03IM, a lemma

Tag 03IM in the Stacks Project.

AlgebraicGeometry.Space.eq_of_specializes_of_pointsMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/Specializations.lean, line 256.

Stacks 03IM. Let X be an algebraic space over S and let x be a point of X above which every étale chart of X by an affine scheme has a finite fibre, which is condition (2) of Stacks 03JS for the pair (X, x). If two points u and u' of an étale scheme chart of X both lie above x and u is a specialization of u', then u = u'.

theorem eq_of_specializes_of_pointsMap_eq {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (x : points B S hS X)
    (hfinite : ∀ V : BigFppfOver B S hS, IsAffine ((BigFppfOver.toScheme B S hS).obj V) →
      ∀ ψ : yoneda.obj V ⟶ X, (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf ψ →
      (pointsMap B S hS (yoneda.obj V) ψ ⁻¹' {x}).Finite)
    (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X)
    (hφ : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf φ)
    (u u' : points B S hS (yoneda.obj U))
    (hu : pointsMap B S hS (yoneda.obj U) φ u = x)
    (hu' : pointsMap B S hS (yoneda.obj U) φ u' = x)
    (hs : u' ⤳ u) : u = u'

Tag 0H1Q, a lemma

Tag 0H1Q in the Stacks Project.

AlgebraicGeometry.Space.eq_of_specializes_of_chartPoint_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/GenericPointsAndDimension.lean, line 125.

Let X be an algebraic space over S and let a : h_U ⟶ X be an étale scheme chart of X whose scheme is locally Noetherian. Two points u, u' of U lying above the same point x of |X| with u' ⤳ u are then equal.

theorem eq_of_specializes_of_chartPoint_of_isLocallyNoetherian
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X)
    (ha : (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf a)
    [IsLocallyNoetherian ((BigFppfOver.toScheme B S hS).obj U)]
    (u u' : (BigFppfOver.toScheme B S hS).obj U) (x : points B S hS X)
    (hu : ChartPoint B S hS U a u x) (hu' : ChartPoint B S hS U a u' x)
    (hs : u' ⤳ u) : u = u'

Tag 03K2, a lemma

Tag 03K2 in the Stacks Project.

AlgebraicGeometry.Space.exists_specializes_pointsMap_eq_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/Specializations.lean, line 517.

Stacks 03K2. Let X be an algebraic space over S, let x' ⤳ x be a specialization of points of X and assume that every étale chart of X by an affine scheme has a finite fibre above x', which is condition (2) of Stacks 03JS for the pair (X, x'). Then for every étale chart φ : h_U ⟶ X of X by a scheme and every point u of the chart above x there is a point u' of the chart above x' with u' ⤳ u.

theorem exists_specializes_pointsMap_eq_of_isEtale
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    {x x' : points B S hS X} (hs : x' ⤳ x)
    (hfinite : ∀ V : BigFppfOver B S hS, IsAffine ((BigFppfOver.toScheme B S hS).obj V) →
      ∀ ψ : yoneda.obj V ⟶ X, (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf ψ →
      (pointsMap B S hS (yoneda.obj V) ψ ⁻¹' {x'}).Finite)
    (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X)
    (hφ : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf φ)
    (u : points B S hS (yoneda.obj U)) (hu : pointsMap B S hS (yoneda.obj U) φ u = x) :
    ∃ u' : points B S hS (yoneda.obj U), u' ⤳ u ∧
      pointsMap B S hS (yoneda.obj U) φ u' = x'

Tag 0B7W, a lemma

Tag 0B7W in the Stacks Project.

AlgebraicGeometry.Space.exists_specializes_pointsMap_eq_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/Specializations.lean, line 552.

Stacks 0B7W. Let f : Y ⟶ X be a flat morphism of algebraic spaces over S, let x' ⤳ x be a specialization of points of X and assume that every étale chart of X by an affine scheme has a finite fibre above x', which is condition (2) of Stacks 03JS for the pair (X, x'). Then every point y of Y above x is the specialization of a point of Y above x'.

theorem exists_specializes_pointsMap_eq_of_isFlat
    {Y X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hY : IsAlgebraicSpace B S hS Y) (hX : IsAlgebraicSpace B S hS X)
    (f : Y ⟶ X) (hf : IsFlat B S hS f)
    {x x' : points B S hS X} (hs : x' ⤳ x)
    (hfinite : ∀ V : BigFppfOver B S hS, IsAffine ((BigFppfOver.toScheme B S hS).obj V) →
      ∀ ψ : yoneda.obj V ⟶ X, (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf ψ →
      (pointsMap B S hS (yoneda.obj V) ψ ⁻¹' {x'}).Finite)
    (y : points B S hS Y) (hy : pointsMap B S hS Y f y = x) :
    ∃ y' : points B S hS Y, y' ⤳ y ∧ pointsMap B S hS Y f y' = x'

Sources

LeanAlgebraicGeometry.Space.eq_of_specializes_of_pointsMap_eq · AlgebraicGeometry.Space.eq_of_specializes_of_chartPoint_of_isLocallyNoetherian · AlgebraicGeometry.Space.exists_specializes_pointsMap_eq_of_isEtale · AlgebraicGeometry.Space.exists_specializes_pointsMap_eq_of_isFlat

Section68.8 Stratifying algebraic spaces by schemes #

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

Tag 07S8, a lemma

Tag 07S8 in the Stacks Project.

AlgebraicGeometry.Space.exists_closedChain_isFiniteLocallyFreeOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreDegreeClosedStratification.lean, line 138.

Stacks Project, Tag 07S8. A flat, locally finitely presented, separated, locally quasi-finite morphism from a scheme to an algebraic space with universally bounded fibres induces a finite increasing chain of closed subsets of the point set, from ∅ to the whole point set, whose strata are the loci over which the base change of the morphism is finite locally free of a fixed degree.

theorem exists_closedChain_isFiniteLocallyFreeOfRank
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (W : BigFppfOver B S hS)
    (g : yoneda.obj W ⟶ X) (hX : IsAlgebraicSpace B S hS X)
    (hflat : IsFlat B S hS g) (hlfp : IsLocallyOfFinitePresentation B S hS g)
    (hsep : IsSeparated B S hS g) (hlqf : IsLocallyQuasiFinite B S hS g)
    (hbound : HasUniversallyBoundedFibers B S hS W g) :
    ∃ (n : ℕ) (Z : ℕ → Set (points B S hS X)), Z 0 = ∅ ∧ (∀ r, IsClosed (Z r)) ∧ Monotone Z ∧
      Z (n + 1) = Set.univ ∧
      ∀ r : ℕ, r ≤ n → ∀ (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hm : T ⟶ X),
        IsAlgebraicSpace B S hS T →
        ∀ (Pp : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (pr₁ : Pp ⟶ yoneda.obj W) (pr₂ : Pp ⟶ T),
          IsPullback pr₁ pr₂ g hm →
          ((MorphismProperty.inverseImage (IsFiniteLocallyFreeOfRank.property.{u} r)
              (BigFppfOver.toScheme B S hS)).presheaf pr₂ ↔
            Set.range (pointsMap B S hS T hm) ⊆ Z (r + 1) \ Z r)

Tag 086T, a lemma

Tag 086T in the Stacks Project.

AlgebraicGeometry.Space.exists_antitone_isOpenSubspace_iff_fibre_degree_ge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreDegreeStratification.lean, line 982.

Let X be an algebraic space over a scheme S and let f : yoneda.obj W ⟶ X be a morphism from a scheme which is flat, locally of finite presentation, separated and locally quasi-finite. Then there is a descending chain of open subspaces X = X₀ ⊇ X₁ ⊇ X₂ ⊇ … such that a field-valued point of X factors through Xᵈ exactly when the fibre of f above it has degree at least d; a fibre which is not finite counts as having infinite degree.

theorem exists_antitone_isOpenSubspace_iff_fibre_degree_ge
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    {W : BigFppfOver B S hS} (f : yoneda.obj W ⟶ X)
    (hflat : IsFlat B S hS f) (hfp : IsLocallyOfFinitePresentation B S hS f)
    (hsep : IsSeparated B S hS f) (hlqf : IsLocallyQuasiFinite B S hS f) :
    ∃ Y : ℕ → Subfunctor X,
      Y 0 = ⊤ ∧ Antitone Y ∧ (∀ d, IsOpenSubspace B S hS (Y d)) ∧
      ∀ (d : ℕ) (p : FieldValuedPoint B S hS X),
        (∃ g : yoneda.obj p.siteObject ⟶ (Y d).toFunctor,
            g ≫ (Y d).ι = yonedaEquiv.symm p.value) ↔
          (¬ (MorphismProperty.inverseImage (@_root_.AlgebraicGeometry.IsFinite.{u})
                (BigFppfOver.toScheme B S hS)).presheaf
                (pullback.fst (yonedaEquiv.symm p.value) f) ∨
            ∃ r : ℕ, d ≤ r ∧
              (MorphismProperty.inverseImage (IsFiniteLocallyFreeOfRank.property.{u} r)
                (BigFppfOver.toScheme B S hS)).presheaf
                (pullback.fst (yonedaEquiv.symm p.value) f))

Tag 0BBN, a lemma

Tag 0BBN in the Stacks Project.

AlgebraicGeometry.Space.exists_schemeStratification_quasiCompactPoint_mem_stratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FiniteSchemeFiltration/Strata.lean, line 298.

A quasi-compact algebraic space X over S carries a descending chain of open subspaces starting at X whose reduced strata, the differences of consecutive members, each receive an isomorphism from the part lying over them of a separated scheme surjective and étale over the corresponding member; and every point of |X| represented by a quasi-compact morphism from the spectrum of a field lies in one of those strata.

public theorem exists_schemeStratification_quasiCompactPoint_mem_stratum
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hqc : AlgebraicGeometry.Space.IsQuasiCompactSpace B S hS X) :
    ∃ strat : AlgebraicGeometry.Space.SchemeStratification B S hS X,
      ∀ (x : AlgebraicGeometry.Space.points B S hS X)
        (z : AlgebraicGeometry.Space.FieldValuedPoint B S hS X),
        z.class B S hS X = x →
        AlgebraicGeometry.Space.IsQuasiCompact B S hS
          (AlgebraicGeometry.Space.fieldMorphism B S hS X z) →
        ∃ p : ℕ, x ∈ Set.range (AlgebraicGeometry.Space.pointsMap B S hS
          (strat.stratum p).toFunctor ((strat.stratum p).ι ≫ (strat.openPart p).ι))

Tag 07S9, a lemma

Tag 07S9 in the Stacks Project.

AlgebraicGeometry.Space.exists_finiteFiltration_of_isReasonableSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FiniteSchemeFiltration/Strata.lean, line 474.

A quasi-compact reasonable algebraic space has a finite filtration by open subspaces such that every reduced stratum has a separated scheme as an étale neighborhood, isomorphic above the stratum.

public theorem exists_finiteFiltration_of_isReasonableSpace
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hqc : AlgebraicGeometry.Space.IsQuasiCompactSpace B S hS X)
    (hr : AlgebraicGeometry.Space.IsReasonableSpace B S hS X) :
    ∃ (n : ℕ) (U : ℕ → Subfunctor X),
      0 < n ∧
      U 0 = ⊤ ∧
      U n = (⊥ : Subfunctor X).sheafify
        (AlgebraicGeometry.BigFppfOver.topology B S hS) ∧
      (∀ p ≤ n, AlgebraicGeometry.Space.IsOpenSubspace B S hS (U p)) ∧
      (∀ p < n, U (p + 1) ≤ U p) ∧
      ∃ (T : (p : Fin n) → Subfunctor (U p.val).toFunctor)
        (V : Fin n → AlgebraicGeometry.BigFppfOver B S hS)
        (f : ∀ p : Fin n, yoneda.obj (V p) ⟶ (U p.val).toFunctor),
        ∀ p : Fin n,
          (AlgebraicGeometry.Space.IsClosedSubspace B S hS (T p)) ∧
          (Set.range (AlgebraicGeometry.Space.pointsMap B S hS (T p).toFunctor
            ((T p).ι ≫ (U p.val).ι)) =
              Set.range (AlgebraicGeometry.Space.pointsMap B S hS (U p.val).toFunctor
                (U p.val).ι) \
              Set.range (AlgebraicGeometry.Space.pointsMap B S hS (U (p.val + 1)).toFunctor
                (U (p.val + 1)).ι)) ∧
          (AlgebraicGeometry.Space.HasEtaleLocalProperty B S hS (T p).toFunctor
            (fun Y : Scheme.{u} => IsReduced Y)) ∧
          Scheme.IsSeparated ((AlgebraicGeometry.BigFppfOver.toScheme B S hS).obj (V p)) ∧
          (MorphismProperty.inverseImage
            (@Surjective.{u} : MorphismProperty Scheme.{u})
            (AlgebraicGeometry.BigFppfOver.toScheme B S hS)).presheaf (f p) ∧
          AlgebraicGeometry.Space.IsEtale B S hS (f p) ∧
          IsIso (pullback.fst (T p).ι (f p))

Tag 07SA, a lemma

Tag 07SA in the Stacks Project.

AlgebraicGeometry.Space.exists_finiteFiltration_isRepresentable_strata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FiniteSchemeFiltration/Strata.lean, line 519.

A quasi-compact reasonable algebraic space has a finite filtration by open subspaces whose reduced strata are schemes.

public theorem exists_finiteFiltration_isRepresentable_strata
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hqc : AlgebraicGeometry.Space.IsQuasiCompactSpace B S hS X)
    (hr : AlgebraicGeometry.Space.IsReasonableSpace B S hS X) :
    ∃ (n : ℕ) (U : ℕ → Subfunctor X),
      0 < n ∧
      U 0 = ⊤ ∧
      U n = (⊥ : Subfunctor X).sheafify
        (AlgebraicGeometry.BigFppfOver.topology B S hS) ∧
      (∀ p ≤ n, AlgebraicGeometry.Space.IsOpenSubspace B S hS (U p)) ∧
      (∀ p < n, U (p + 1) ≤ U p) ∧
      ∃ T : (p : Fin n) → Subfunctor (U p.val).toFunctor,
        ∀ p : Fin n,
          (AlgebraicGeometry.Space.IsClosedSubspace B S hS (T p)) ∧
          (Set.range (AlgebraicGeometry.Space.pointsMap B S hS (T p).toFunctor
            ((T p).ι ≫ (U p.val).ι)) =
              Set.range (AlgebraicGeometry.Space.pointsMap B S hS (U p.val).toFunctor
                (U p.val).ι) \
              Set.range (AlgebraicGeometry.Space.pointsMap B S hS (U (p.val + 1)).toFunctor
                (U (p.val + 1)).ι)) ∧
          (AlgebraicGeometry.Space.HasEtaleLocalProperty B S hS (T p).toFunctor
            (fun Y : Scheme.{u} => IsReduced Y)) ∧
          (T p).toFunctor.IsRepresentable

Tag 07ST, a lemma

Tag 07ST in the Stacks Project.

AlgebraicGeometry.Space.exists_finiteFiltration_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FiniteSchemeFiltration/Strata.lean, line 420.

A quasi-compact quasi-separated algebraic space has a finite filtration by open subspaces such that every reduced stratum has a quasi-compact separated scheme as an étale neighborhood, isomorphic above the stratum.

public theorem exists_finiteFiltration_of_isQuasiCompactSpace
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hqc : AlgebraicGeometry.Space.IsQuasiCompactSpace B S hS X)
    (hqs : AlgebraicGeometry.Space.IsAbsolutelyQuasiSeparated B S hS hZ X) :
    ∃ (n : ℕ) (U : ℕ → Subfunctor X),
      0 < n ∧
      U 0 = ⊤ ∧
      U n = (⊥ : Subfunctor X).sheafify
        (AlgebraicGeometry.BigFppfOver.topology B S hS) ∧
      (∀ p ≤ n, AlgebraicGeometry.Space.IsOpenSubspace B S hS (U p)) ∧
      (∀ p < n, U (p + 1) ≤ U p) ∧
      ∃ (T : (p : Fin n) → Subfunctor (U p.val).toFunctor)
        (V : Fin n → AlgebraicGeometry.BigFppfOver B S hS)
        (f : ∀ p : Fin n, yoneda.obj (V p) ⟶ (U p.val).toFunctor),
        ∀ p : Fin n,
          (AlgebraicGeometry.Space.IsClosedSubspace B S hS (T p)) ∧
          (Set.range (AlgebraicGeometry.Space.pointsMap B S hS (T p).toFunctor
            ((T p).ι ≫ (U p.val).ι)) =
              Set.range (AlgebraicGeometry.Space.pointsMap B S hS (U p.val).toFunctor
                (U p.val).ι) \
              Set.range (AlgebraicGeometry.Space.pointsMap B S hS (U (p.val + 1)).toFunctor
                (U (p.val + 1)).ι)) ∧
          (AlgebraicGeometry.Space.HasEtaleLocalProperty B S hS (T p).toFunctor
            (fun Y : Scheme.{u} => IsReduced Y)) ∧
          CompactSpace ((AlgebraicGeometry.BigFppfOver.toScheme B S hS).obj (V p)) ∧
          Scheme.IsSeparated ((AlgebraicGeometry.BigFppfOver.toScheme B S hS).obj (V p)) ∧
          (MorphismProperty.inverseImage
            (@Surjective.{u} : MorphismProperty Scheme.{u})
            (AlgebraicGeometry.BigFppfOver.toScheme B S hS)).presheaf (f p) ∧
          AlgebraicGeometry.Space.IsEtale B S hS (f p) ∧
          IsIso (pullback.fst (T p).ι (f p))

Tag 0ECZ, a lemma

Tag 0ECZ in the Stacks Project.

AlgebraicGeometry.Space.isEtaleLocallyConstructible_iff_isLocallyConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConstructiblePointsQuasiSeparated.lean, line 290.

Stacks 0ECZ. A subset of the point space of a quasi-separated algebraic space over S is étale locally constructible exactly when it is locally constructible.

theorem isEtaleLocallyConstructible_iff_isLocallyConstructible
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X)
    (E : Set (points B S hS X)) :
    IsEtaleLocallyConstructible B S hS X E ↔ IsLocallyConstructible E

Sources

LeanAlgebraicGeometry.Space.exists_closedChain_isFiniteLocallyFreeOfRank · AlgebraicGeometry.Space.exists_antitone_isOpenSubspace_iff_fibre_degree_ge · AlgebraicGeometry.Space.exists_schemeStratification_quasiCompactPoint_mem_stratum · AlgebraicGeometry.Space.exists_finiteFiltration_of_isReasonableSpace · AlgebraicGeometry.Space.exists_finiteFiltration_isRepresentable_strata · AlgebraicGeometry.Space.exists_finiteFiltration_of_isQuasiCompactSpace · AlgebraicGeometry.Space.isEtaleLocallyConstructible_iff_isLocallyConstructible

Section68.9 Integral cover by a scheme #

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

Tag 0G2D, a lemma

Tag 0G2D in the Stacks Project.

AlgebraicGeometry.Space.exists_isIntegralHom_isPullback_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ExtendIntegralMorphism.lean, line 111.

Stacks 0G2D. Let j : V ⟶ Y be a quasi-compact open immersion of algebraic spaces over a scheme S and let π : Z ⟶ V be an integral morphism. Then there is an integral morphism ν : Y' ⟶ Y of algebraic spaces over S such that Z is V-isomorphic to the inverse image of V in Y': the square formed by π, j, ν and the canonical morphism Z ⟶ Y' is cartesian.

Y' is the normalization of Y in Z, and the cartesian square is obtained from the chart description of that normalization by the cancellation of Tag 07VZ along a surjective étale chart of V; see the implementation notes.

theorem exists_isIntegralHom_isPullback_of_isOpenImmersion
    (hZ : IsAlgebraicSpace B S hS Z) (hV : IsAlgebraicSpace B S hS V)
    (hY : IsAlgebraicSpace B S hS Y) (j : V ⟶ Y) (hj : IsOpenImmersion B S hS j)
    (hjqc : IsQuasiCompact B S hS j) (π : Z ⟶ V) (hπ : IsIntegralHom B S hS π) :
    ∃ (Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (ν : Y' ⟶ Y) (f' : Z ⟶ Y'),
      IsAlgebraicSpace B S hS Y' ∧ IsIntegralHom B S hS ν ∧ IsPullback f' π ν j

Tag 09YB, a lemma

Tag 09YB in the Stacks Project.

AlgebraicGeometry.Space.existsIntegralSurjectiveSchemeCover_and_refining, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralSchemeCoverExistence.lean, line 185.

Stacks Project, Tag 09YB. Let X be a quasi-compact and quasi-separated algebraic space over a scheme S. Then

there is a surjective integral morphism to X from the presheaf represented by an object of the big fppf site — a scheme over S — and

given a surjective étale morphism p : U ⟶ X from an algebraic space, such a cover can be chosen so that it factors through p on a representable open subspace neighbourhood of every one of its points.

Both clauses are proved, over no hypothesis. Clause (1) is the source's induction on a bound for the degree of the geometric fibres of an étale chart, performed in StacksFrontier.AlgebraicGeometry.Spaces.IntegralSchemeCoverInduction; clause (2) is deduced here from clause (1) by the unconditional Stacks 0CP0.

theorem existsIntegralSurjectiveSchemeCover_and_refining
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (hXqc : IsQuasiCompactSpace B S hS X)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X) :
    ExistsIntegralSurjectiveSchemeCover B S hS X ∧
      ∀ (U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS U →
        ∀ p : U ⟶ X, IsSurjective B S hS p → IsEtale B S hS p →
          ∃ (Y : BigFppfOver B S hS) (f : yoneda.obj Y ⟶ X),
            IsSurjective B S hS f ∧ IsIntegralHom B S hS f ∧
              FactorsZariskiLocallyThrough B S hS p Y f

Tag 0GUL, a lemma

Tag 0GUL in the Stacks Project.

AlgebraicGeometry.Space.exists_integralSchemeCover_finiteEtaleOverDenseOpen_and_refining, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralSchemeCoverEtaleInduction.lean, line 1423.

Stacks Project, Tag 0GUL. Let X be a quasi-compact and quasi-separated algebraic space over a scheme S such that |X| has finitely many irreducible components. Then

there is a surjective integral morphism to X from the presheaf represented by an object of the big fppf site — a scheme over S — which is finite étale over a quasi-compact open subspace of X with dense point set, and

given a surjective étale morphism p : V ⟶ X from an algebraic space, such a cover can be chosen so that it factors through p on a representable open subspace neighbourhood of every one of its points.

Clause (2) for a cover p is reduced to a chart c : h_{V₀} ⟶ V (AlgebraicGeometry.Space.existsIntegralSchemeCoverRefining_of_comp_chart); for the chart c ≫ p the induction gives a cover étale over a dense open (AlgebraicGeometry.Space.existsIntegralSchemeCoverEtaleRefining_of_isEtale), which is upgraded to one finite étale over a quasi-compact dense open (AlgebraicGeometry.Space.existsIntegralSchemeCoverRefining_of_etaleRefining). Clause (1) is clause (2) at the identity of X.

theorem exists_integralSchemeCover_finiteEtaleOverDenseOpen_and_refining
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (hXqc : IsQuasiCompactSpace B S hS X)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (hcomp : (irreducibleComponents (points B S hS X)).Finite) :
    ExistsIntegralSchemeCoverFiniteEtaleOverDenseOpen B S hS X ∧
      ∀ (V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS V →
        ∀ p : V ⟶ X, IsSurjective B S hS p → IsEtale B S hS p →
          ExistsIntegralSchemeCoverRefining B S hS p

Sources

LeanAlgebraicGeometry.Space.exists_isIntegralHom_isPullback_of_isOpenImmersion · AlgebraicGeometry.Space.existsIntegralSurjectiveSchemeCover_and_refining · AlgebraicGeometry.Space.exists_integralSchemeCover_finiteEtaleOverDenseOpen_and_refining

Section68.10 Schematic locus #

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

Tag 03JI, a proposition

Tag 03JI in the Stacks Project.

AlgebraicGeometry.Space.exists_denseRange_isRepresentable_isOpenSubspace_of_isReasonableSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReasonableDenseSchematicLocus.lean, line 206.

Stacks 03JI. The schematic locus of a reasonable algebraic space is dense: a reasonable algebraic space X over a scheme S has a representable open subspace whose point set is dense in |X|.

Reasonableness is condition (2) of Stacks 03JT, so Stacks 03JT in the form AlgebraicGeometry.Space.exists_boundedEtaleCover_of_isReasonableSpace gives a jointly surjective family of étale charts φ i by affine schemes with universally bounded fibres. No member of the family is surjective, so the corollary does not apply to X directly. Replacing X by the open subspace X i swept out by φ i — Stacks 06NF — makes the induced chart ψ i : h_{U i} ⟶ X i surjective, and the bound passes from φ i to ψ i because (X i).ι is a monomorphism. The corollary then gives in each X i a representable open subspace L i with dense point set.

Stacks 03JH, in the form AlgebraicGeometry.Space.exists_denseRange_isRepresentable_isOpenSubspace_of_isAlgebraicSpace, reduces the conclusion to finding a nonempty representable open subspace inside every nonempty open subspace G of X. The point sets of the X i cover |X|, so some |X i| meets |G|; the preimage of |G| in |X i| is then a nonempty open set, which by density meets |L i|. So |G| ∩ |L i| is nonempty, and the open subspace of X it cuts out is contained in G and contained in L i, hence representable by AlgebraicGeometry.Space.isRepresentable_of_le_of_isRepresentable.

theorem exists_denseRange_isRepresentable_isOpenSubspace_of_isReasonableSpace
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hreasonable : IsReasonableSpace B S hS X) :
    ∃ G : Subfunctor X, IsOpenSubspace B S hS G ∧ G.toFunctor.IsRepresentable ∧
      DenseRange (pointsMap B S hS G.toFunctor G.ι)

Tag 086U, a theorem

Tag 086U in the Stacks Project.

AlgebraicGeometry.Space.exists_denseRange_isRepresentable_isOpenSubspace_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DenseSchematicLocusDecent.lean, line 322.

Stacks 086U (David Rydh). A decent algebraic space over a scheme has a dense open subspace which is a scheme: its schematic locus of Stacks 03JH is a representable open subspace whose set of points is dense.

The reduction to the local statement AlgebraicGeometry.Space.exists_isRepresentable_isOpenSubspace_nonempty_of_isDecentSpace is AlgebraicGeometry.Space.exists_denseRange_isRepresentable_isOpenSubspace_of_isAlgebraicSpace, which is Stacks 03JH together with the reduction of StacksFrontier/AlgebraicGeometry/Spaces/DenseSchematicLocus.lean.

theorem exists_denseRange_isRepresentable_isOpenSubspace_of_isDecentSpace
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) :
    ∃ G : Subfunctor X, IsOpenSubspace B S hS G ∧ G.toFunctor.IsRepresentable ∧
      DenseRange (pointsMap B S hS G.toFunctor G.ι)

Tag 0BA1, a lemma

Tag 0BA1 in the Stacks Project.

AlgebraicGeometry.Space.mem_range_pointsMap_schematicLocus_iff_exists_isAffine_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeSchematicLocus.lean, line 804.

Stacks 0BA1. Let X ⟶ Y be a surjective finite locally free morphism of algebraic spaces over a scheme S, and let y be a point of Y. Then the following are equivalent:

y lies in the schematic locus of Y — the point set of AlgebraicGeometry.Space.schematicLocus, the largest open subspace of Y which is a scheme (Tag 03JH); and

there is an affine open subspace of X, presented as an open immersion i : h_U ⟶ X from an affine object U of the site, whose point set contains the whole fibre of y.

Finite local freeness of f is taken in the representable sense: f is representable and every represented base change of it is a finite locally free morphism of schemes. That is condition (1) of Tag 03ZW, which the source's Definition 03ZV — condition (2) of that tag — is equivalent to. Surjectivity is likewise taken after representable base change, which is condition (1) of Tag 02YN.

The two implications are AlgebraicGeometry.Space.exists_isAffine_isOpenImmersion_of_mem_schematicLocus and AlgebraicGeometry.Space.mem_range_pointsMap_schematicLocus_of_exists_isAffine; see their docstrings for the two arguments.

theorem mem_range_pointsMap_schematicLocus_iff_exists_isAffine_isOpenImmersion
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hsurj : (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f.hom)
    (hflf : (MorphismProperty.inverseImage
      (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f.hom)
    (y : points B S hS Y.obj) :
    y ∈ Set.range (pointsMap B S hS (schematicLocus B S hS Y.obj).toFunctor
        (schematicLocus B S hS Y.obj).ι) ↔
      ∃ (U : BigFppfOver B S hS) (i : yoneda.obj U ⟶ X.obj),
        IsAffine ((BigFppfOver.toScheme B S hS).obj U) ∧ IsOpenImmersion B S hS i ∧
        ∀ x : points B S hS X.obj, pointsMap B S hS X.obj f.hom x = y →
          x ∈ Set.range (pointsMap B S hS (yoneda.obj U) i)

Tag 06NG, a lemma

Tag 06NG in the Stacks Project.

AlgebraicGeometry.Space.exists_denseRange_isRepresentable_isOpenSubspace_of_finite_etale_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FiniteEtaleAtlasSchematicLocus.lean, line 106.

Stacks 06NG. An algebraic space over S admitting a finite étale surjective morphism from a scheme over S has a representable open subspace whose point set is dense: such a space is reasonable, so Stacks 03JI applies.

theorem exists_denseRange_isRepresentable_isOpenSubspace_of_finite_etale_cover
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    {U : BigFppfOver B S hS} (f : yoneda.obj U ⟶ X)
    (hfin : IsFinite B S hS f) (_hetale : IsEtale B S hS f)
    (hsurj : IsSurjective B S hS f) :
    ∃ G : Subfunctor X, IsOpenSubspace B S hS G ∧ G.toFunctor.IsRepresentable ∧
      DenseRange (pointsMap B S hS G.toFunctor G.ι)

Sources

LeanAlgebraicGeometry.Space.exists_denseRange_isRepresentable_isOpenSubspace_of_isReasonableSpace · AlgebraicGeometry.Space.exists_denseRange_isRepresentable_isOpenSubspace_of_isDecentSpace · AlgebraicGeometry.Space.mem_range_pointsMap_schematicLocus_iff_exists_isAffine_isOpenImmersion · AlgebraicGeometry.Space.exists_denseRange_isRepresentable_isOpenSubspace_of_finite_etale_cover

Section68.11 Residue fields and henselian local rings #

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

Tag 03K4, a lemma

Tag 03K4 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.iso_of_mono_of_point_eq, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidueField.lean, line 56 (StacksFrontier): “injectivity”.
AlgebraicGeometry.Space.IsDecentSpace.hasMonomorphicFieldRepresentative, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidueField.lean, line 57 (StacksFrontier): “surjectivity”.

Tag 0EMW, a definition

Tag 0EMW in the Stacks Project.

AlgebraicGeometry.Space.residueFieldRepresentative, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidueField.lean, line 68. The attribute's comment: “field-valued monomorphism”.

The chosen field-valued representative of a point of a decent algebraic space whose morphism to the space is a monomorphism.

noncomputable def residueFieldRepresentative (hDecent : IsDecentSpace B S hS X)
    (x : points B S hS X) :
    {p : FieldValuedPoint B S hS X //
      p.class B S hS X = x ∧ Mono (fieldMorphism B S hS X p)}

AlgebraicGeometry.Space.residueField, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidueField.lean, line 78. The attribute's comment: “residue field”.

The residue field of a decent algebraic space at a point: the field of the monomorphism from a field spectrum representing that point.

noncomputable abbrev residueField (hDecent : IsDecentSpace B S hS X)
    (x : points B S hS X) : Type u

AlgebraicGeometry.Space.residueFieldRepresentative_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidueField.lean, line 92. The attribute's comment: “uniqueness”.

A monomorphic field-valued representative of a point of a decent algebraic space is uniquely isomorphic, over the space, to the chosen one: the residue field is unique up to unique isomorphism.

theorem residueFieldRepresentative_unique (hX : IsAlgebraicSpace B S hS X)
    (hDecent : IsDecentSpace B S hS X) (x : points B S hS X)
    (q : FieldValuedPoint B S hS X) (hq : q.class B S hS X = x)
    (hmq : Mono (fieldMorphism B S hS X q)) :
    ∃! e : yoneda.obj ((residueFieldRepresentative B S hS X hDecent x).1.siteObject B S hS X) ≅
        yoneda.obj (q.siteObject B S hS X),
      e.hom ≫ fieldMorphism B S hS X q = residueFieldMorphism B S hS X hDecent x

Tag 0EMX, a lemma

Tag 0EMX in the Stacks Project.

AlgebraicGeometry.Space.isIso_residueFieldHom_iff_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidueField.lean, line 194.

A morphism of decent algebraic spaces induces an isomorphism of residue fields at a point exactly when the morphism from the spectrum of the residue field at that point to the target space is a monomorphism.

theorem isIso_residueFieldHom_iff_mono (hY : IsAlgebraicSpace B S hS Y)
    (hDecentX : IsDecentSpace B S hS X) (hDecentY : IsDecentSpace B S hS Y)
    (f : X ⟶ Y) (x : points B S hS X) :
    IsIso (CommRingCat.ofHom (residueFieldHom B S hS X Y hY hDecentX hDecentY f x)) ↔
      Mono (residueFieldMorphism B S hS X hDecentX x ≫ f)

Tag 0BBP, a lemma

Tag 0BBP in the Stacks Project.

AlgebraicGeometry.Space.exists_affine_elementaryEtaleNeighborhood', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/AffineElementaryEtaleNeighborhood.lean, line 611.

Stacks 0BBP. Every point x of a decent algebraic space X over S has an elementary étale neighborhood whose scheme is affine, whose distinguished point is the only point above x, and whose residue field at that point is the residue field of X at x through the induced homomorphism.

theorem exists_affine_elementaryEtaleNeighborhood'
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hDecent : IsDecentSpace B S hS X) (x : points B S hS X) :
    ∃ E : ElementaryEtaleNeighborhood B S hS X hX x,
      IsAffine E.scheme.left.1 ∧
      (∀ y : points B S hS (yoneda.obj E.scheme),
        pointsMap B S hS (yoneda.obj E.scheme) E.toSpace y = x →
          y = presheafPoint B S hS E.scheme E.point E.residueField_contained) ∧
      ∃ φ : residueField B S hS X hDecent x →+* E.scheme.left.1.residueField E.point,
        Function.Bijective φ ∧
          ∃ g : residueFieldObject B S hS E.scheme E.point E.residueField_contained ⟶
              (residueFieldRepresentative B S hS X hDecent x).1.siteObject B S hS X,
            B.inclusion.map g.left = Spec.map (CommRingCat.ofHom φ) ∧
              yoneda.map g ≫ residueFieldMorphism B S hS X hDecent x =
                yoneda.map (residueFieldMap B S hS E.scheme E.point
                  E.residueField_contained) ≫ E.toSpace

Tag 0BGU, a definition

Tag 0BGU in the Stacks Project.

AlgebraicGeometry.Space.ElementaryEtaleNeighborhood, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhood.lean, line 131. The attribute's comment: “elementary étale neighborhoods”.

Stacks 0BGU, elementary étale neighborhoods. A scheme étale over an algebraic space, pointed above x, for which the residue-field point is a monomorphism into the space.

structure ElementaryEtaleNeighborhood (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) (x : points B S hS F)

AlgebraicGeometry.Space.ElementaryEtaleNeighborhood.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhood.lean, line 158. The attribute's comment: “morphisms of elementary étale neighborhoods”.

Stacks 0BGU, morphisms. A map of elementary étale neighborhoods is a map over the algebraic space carrying the chosen point to the chosen point.

structure Hom (V W : ElementaryEtaleNeighborhood B S hS F hF x)

Tag 0BGV, a lemma

Tag 0BGV in the Stacks Project.

AlgebraicGeometry.Space.ElementaryEtaleNeighborhood.exists_affine_cone_objs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/AffineRefinementOfNeighborhood.lean, line 57. The attribute's comment: “two neighbourhoods are refined by a common one whose scheme is affine”.

Any two elementary étale neighborhoods of a point of an algebraic space are refined by a common elementary étale neighborhood whose scheme is affine.

theorem exists_affine_cone_objs (U V : ElementaryEtaleNeighborhood B S hS X hX x) :
    ∃ (W : ElementaryEtaleNeighborhood B S hS X hX x) (_ : W ⟶ U) (_ : W ⟶ V),
      IsAffine W.scheme.left.1

AlgebraicGeometry.Space.ElementaryEtaleNeighborhood.exists_cone_objs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodCofiltered.lean, line 435. The attribute's comment: “common refinements: any two elementary étale neighbourhoods admit a third mapping to both”.

Stacks 0BGV, common refinements. Two elementary étale neighborhoods of x admit a common refinement.

theorem exists_cone_objs (V W : ElementaryEtaleNeighborhood B S hS X hX x) :
    ∃ (E : ElementaryEtaleNeighborhood B S hS X hX x) (_ : E ⟶ V) (_ : E ⟶ W), True

AlgebraicGeometry.Space.ElementaryEtaleNeighborhood.exists_cone_maps, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodCofiltered.lean, line 537. The attribute's comment: “equalizing refinements: any two parallel morphisms are equalized by a refinement”.

Stacks 0BGV, equalizing refinements. Two morphisms of elementary étale neighborhoods of x are equalized by a refinement of their source.

theorem exists_cone_maps {V W : ElementaryEtaleNeighborhood B S hS X hX x} (f g : V ⟶ W) :
    ∃ (E : ElementaryEtaleNeighborhood B S hS X hX x) (h : E ⟶ V), h ≫ f = h ≫ g

AlgebraicGeometry.Space.ElementaryEtaleNeighborhood.isCofilteredOrEmpty, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodCofiltered.lean, line 549. The attribute's comment: “the category is cofiltered or empty; unconditional”.

Stacks 0BGV. The category of elementary étale neighborhoods of a point of an algebraic space is cofiltered as soon as it is nonempty: any two neighborhoods are refined by a third, and any two parallel morphisms are equalized by a refinement.

instance isCofilteredOrEmpty : IsCofilteredOrEmpty (ElementaryEtaleNeighborhood B S hS X hX x)

AlgebraicGeometry.Space.ElementaryEtaleNeighborhood.isCofiltered_of_nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodCofiltered.lean, line 558. The attribute's comment: “cofilteredness, with nonemptiness -- which is Tag 0BBP, absent from this library -- as an explicit hypothesis”.

Stacks 0BGV. The category of elementary étale neighborhoods of a point of an algebraic space, if nonempty, is cofiltered.

theorem isCofiltered_of_nonempty
    (hne : Nonempty (ElementaryEtaleNeighborhood B S hS X hX x)) :
    IsCofiltered (ElementaryEtaleNeighborhood B S hS X hX x)

AlgebraicGeometry.Space.isCofiltered_elementaryEtaleNeighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HenselianCompletionBaseChange.lean, line 76. The attribute's comment: “cofilteredness for a decent space, with the nonemptiness hypothesis of the existing carrier discharged by Tag 0BBP”.

The category of elementary étale neighborhoods of a point of a decent algebraic space is cofiltered.

theorem isCofiltered_elementaryEtaleNeighborhood :
    IsCofiltered (ElementaryEtaleNeighborhood B S hS X hX x)

Tag 0BGW, a definition

Tag 0BGW in the Stacks Project.

AlgebraicGeometry.Space.henselianLocalRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRing.lean, line 164. The attribute's comment: “the henselian local ring at a point”.

The henselian local ring of a decent algebraic space at a point: the colimit of the rings of global sections over the elementary étale neighborhoods of the point.

abbrev henselianLocalRing (_hDecent : IsDecentSpace B S hS X) : CommRingCat.{u + 1}

AlgebraicGeometry.Space.sectionHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRing.lean, line 170. The attribute's comment: “canonical section homomorphisms”.

The canonical ring homomorphism from the global sections of an elementary étale neighborhood into the henselian local ring.

def sectionHom (hDecent : IsDecentSpace B S hS X)
    (U : (ElementaryEtaleNeighborhood B S hS X hX x)ᵒᵖ) :
    (globalSections B S hS X hX x).obj U →+* henselianLocalRing B S hS X hX x hDecent

AlgebraicGeometry.Space.sectionHom_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRing.lean, line 179. The attribute's comment: “naturality of section homomorphisms”.

Restricting a section to a finer elementary étale neighborhood does not change its canonical image in the henselian local ring.

theorem sectionHom_naturality (hDecent : IsDecentSpace B S hS X)
    {U V : (ElementaryEtaleNeighborhood B S hS X hX x)ᵒᵖ} (f : U ⟶ V)
    (s : (globalSections B S hS X hX x).obj U) :
    sectionHom B S hS X hX x hDecent V ((globalSections B S hS X hX x).map f s) =
      sectionHom B S hS X hX x hDecent U s

AlgebraicGeometry.Space.existsUnique_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRing.lean, line 191. The attribute's comment: “colimit universal property”.

A family of ring homomorphisms out of the global sections of the elementary étale neighborhoods of a point, compatible with restriction, factors uniquely through the henselian local ring.

theorem existsUnique_lift (hDecent : IsDecentSpace B S hS X) (R : Type v) [CommRing R]
    (φ : ∀ U : (ElementaryEtaleNeighborhood B S hS X hX x)ᵒᵖ,
      (globalSections B S hS X hX x).obj U →+* R)
    (hφ : ∀ {U V} (f : U ⟶ V) (s : (globalSections B S hS X hX x).obj U),
      φ V ((globalSections B S hS X hX x).map f s) = φ U s) :
    ∃! ψ : henselianLocalRing B S hS X hX x hDecent →+* R,
      ∀ U s, ψ (sectionHom B S hS X hX x hDecent U s) = φ U s

Tag 0EMY, a lemma

Tag 0EMY in the Stacks Project.

AlgebraicGeometry.Space.stalkToHenselianLocalRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRingStalk.lean, line 603. The attribute's comment: “the canonical map from the stalk of an elementary étale neighbourhood”.

Stacks 0EMY. The canonical homomorphism from the local ring of an elementary étale neighborhood at its distinguished point into the henselian local ring of the algebraic space.

def stalkToHenselianLocalRing (hDecent : IsDecentSpace B S hS X)
    (U : ElementaryEtaleNeighborhood B S hS X hX x) :
    U.scheme.left.1.presheaf.stalk U.point →+*
      (henselianLocalRing B S hS X hX x hDecent : Type (u + 1))

AlgebraicGeometry.Space.stalkToHenselianLocalRing_openGerm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRingStalk.lean, line 623. The attribute's comment: “the canonical map on germs over a pointed open”.

Stacks 0EMY. The canonical homomorphism sends the germ of a section over a pointed open subscheme to the canonical image of that section in the henselian local ring.

theorem stalkToHenselianLocalRing_openGerm (hDecent : IsDecentSpace B S hS X)
    (U : ElementaryEtaleNeighborhood B S hS X hX x)
    (W : U.scheme.left.1.Opens) (hW : U.point ∈ W)
    (s : U.scheme.left.1.presheaf.obj (op W)) :
    stalkToHenselianLocalRing B S hS X hX x hDecent U
        (U.scheme.left.1.presheaf.germ W U.point hW s) =
      openRestrictionSectionHom B S hS X hX x hDecent U W hW s

AlgebraicGeometry.Space.stalkToHenselianLocalRing_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRingStalk.lean, line 687. The attribute's comment: “naturality of the canonical map in the neighbourhood”.

Stacks 0EMY. The canonical homomorphisms out of the local rings of the elementary étale neighborhoods are compatible with every morphism of neighborhoods.

theorem stalkToHenselianLocalRing_naturality (hDecent : IsDecentSpace B S hS X)
    {V U : ElementaryEtaleNeighborhood B S hS X hX x} (f : V ⟶ U) :
    (stalkToHenselianLocalRing B S hS X hX x hDecent V).comp
        (neighborhoodStalkMap B S hS X hX x f).hom =
      stalkToHenselianLocalRing B S hS X hX x hDecent U

AlgebraicGeometry.Space.henselianLocalRing_isLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRingStalk.lean, line 740. The attribute's comment: “O^h is a local ring”.

Stacks 0EMY. The henselian local ring of a decent algebraic space at a point is a local ring.

theorem henselianLocalRing_isLocalRing (hDecent : IsDecentSpace B S hS X) :
    IsLocalRing (henselianLocalRing B S hS X hX x hDecent : Type (u + 1))

AlgebraicGeometry.Space.henselianLocalRing_isHenselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRingStalk.lean, line 1088. The attribute's comment: “O^h is a henselization of the stalk”. References: SGA 3 X (4.4), “Case 2°”.

Stacks 0EMY. The henselian local ring of a decent algebraic space at a point is a henselization of the local ring of any elementary étale neighborhood at its distinguished point.

theorem henselianLocalRing_isHenselization (hDecent : IsDecentSpace B S hS X)
    (U : ElementaryEtaleNeighborhood B S hS X hX x) :
    letI := henselianLocalRing_isLocalRing B S hS X hX x hDecent
    letI := stalkAlgebra B S hS X hX x hDecent U
    IsLocalRing.IsHenselization (U.scheme.left.1.presheaf.stalk U.point)
      (IsLocalRing.ResidueField (U.scheme.left.1.presheaf.stalk U.point))
      (henselianLocalRing B S hS X hX x hDecent : Type (u + 1))

AlgebraicGeometry.Space.map_maximalIdeal_stalkToHenselianLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRingStalk.lean, line 1147. The attribute's comment: “the maximal ideal of O^h”.

Stacks 0EMY. The maximal ideal of the henselian local ring is generated by the image of the maximal ideal of the local ring of any elementary étale neighborhood.

theorem map_maximalIdeal_stalkToHenselianLocalRing (hDecent : IsDecentSpace B S hS X)
    (U : ElementaryEtaleNeighborhood B S hS X hX x) :
    letI := henselianLocalRing_isLocalRing B S hS X hX x hDecent
    (IsLocalRing.maximalIdeal (U.scheme.left.1.presheaf.stalk U.point)).map
        (stalkToHenselianLocalRing B S hS X hX x hDecent U) =
      IsLocalRing.maximalIdeal (henselianLocalRing B S hS X hX x hDecent : Type (u + 1))

AlgebraicGeometry.Space.exists_residueFieldEquiv_henselianLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRingStalk.lean, line 1163. The attribute's comment: “the residue field of O^h”.

Stacks 0EMY. The residue field of the henselian local ring is the residue field of the local ring of any elementary étale neighborhood at its distinguished point.

theorem exists_residueFieldEquiv_henselianLocalRing (hDecent : IsDecentSpace B S hS X)
    (U : ElementaryEtaleNeighborhood B S hS X hX x) :
    letI := henselianLocalRing_isLocalRing B S hS X hX x hDecent
    ∃ e : IsLocalRing.ResidueField (U.scheme.left.1.presheaf.stalk U.point) ≃+*
        IsLocalRing.ResidueField
          (henselianLocalRing B S hS X hX x hDecent : Type (u + 1)),
      ∀ r : U.scheme.left.1.presheaf.stalk U.point,
        e (IsLocalRing.residue _ r) =
          IsLocalRing.residue _ (stalkToHenselianLocalRing B S hS X hX x hDecent U r)

AlgebraicGeometry.Space.PrimeDivisor.neighborhoodSectionsToGenericHenselianLocalRing_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PrimeDivisorFunctionFieldChartIndependence.lean, line 101. The attribute's comment: “naturality in the neighbourhood of the map from global sections into the henselian local ring”.

Stacks 0EMY. The map from the global sections of an elementary étale neighbourhood of the generic point of a prime divisor into the henselian local ring there is compatible with every morphism of neighbourhoods.

theorem PrimeDivisor.neighborhoodSectionsToGenericHenselianLocalRing_naturality
    {V U : ElementaryEtaleNeighborhood B S hS X hX (Z.genericPoint B S hS X)} (f : V ⟶ U)
    (a : Γ(U.scheme.left.1, ⊤)) :
    Z.neighborhoodSectionsToGenericHenselianLocalRing B S hS hX hdec V (f.hom.left.1.appTop a) =
      Z.neighborhoodSectionsToGenericHenselianLocalRing B S hS hX hdec U a

AlgebraicGeometry.Space.isLocalRing_henselianLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HenselianCompletionBaseChange.lean, line 83. The attribute's comment: “O^h is a local ring for a decent space”.

The henselian local ring of a decent algebraic space at a point is a local ring.

theorem isLocalRing_henselianLocalRing :
    IsLocalRing (henselianLocalRing B S hS X hX x hXdec : Type (u + 1))

Tag 0EMZ, a lemma

Tag 0EMZ in the Stacks Project.

AlgebraicGeometry.Space.exists_isHenselization_etaleLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/EtaleLocalRingStrictHenselization.lean, line 81. The attribute's comment: “the étale local ring at a geometric point is a strict henselization of the henselian local ring at the point below it, for a chosen separable closure κsep of the residue field. The algebra structures are produced, not assumed; the structure map is pinned by lying over the neighborhood stalk, of which the étale local ring is also a strict henselization”.

Stacks 0EMZ. The étale local ring of a decent algebraic space at a geometric point is a strict henselization of the henselian local ring of the space at the point it lies over.

theorem exists_isHenselization_etaleLocalRing (hDecent : IsDecentSpace B S hS X)
    (U : ElementaryEtaleNeighborhood B S hS X hX x)
    (xbar : GeometricPoint B S hS X) (hxbar : xbar.LiesOver x)
    (κsep : Type u) [Field κsep]
    [Algebra (ResidueField (U.scheme.left.1.presheaf.stalk U.point : Type u)) κsep]
    [IsSepClosure (ResidueField (U.scheme.left.1.presheaf.stalk U.point : Type u)) κsep] :
    letI := henselianLocalRing_isLocalRing B S hS X hX x hDecent
    letI := isLocalRing_etaleLocalRing B S hS X hX xbar
    ∃ (algU : Algebra (U.scheme.left.1.presheaf.stalk U.point : Type u)
        (etaleLocalRing B S hS X xbar : Type (u + 1)))
      (alg : Algebra (henselianLocalRing B S hS X hX x hDecent : Type (u + 1))
        (etaleLocalRing B S hS X xbar : Type (u + 1)))
      (algRes : Algebra (ResidueField
        (henselianLocalRing B S hS X hX x hDecent : Type (u + 1))) κsep),
      (@algebraMap (henselianLocalRing B S hS X hX x hDecent : Type (u + 1))
            (etaleLocalRing B S hS X xbar : Type (u + 1)) _ _ alg).comp
          (stalkToHenselianLocalRing B S hS X hX x hDecent U) =
        @algebraMap (U.scheme.left.1.presheaf.stalk U.point : Type u)
          (etaleLocalRing B S hS X xbar : Type (u + 1)) _ _ algU ∧
      @IsHenselization (U.scheme.left.1.presheaf.stalk U.point : Type u) _ _ κsep _ _
        (etaleLocalRing B S hS X xbar : Type (u + 1)) _ _ algU ∧
      @IsHenselization (henselianLocalRing B S hS X hX x hDecent : Type (u + 1)) _ _
        κsep _ algRes (etaleLocalRing B S hS X xbar : Type (u + 1)) _ _ alg

Tag 0EN0, a lemma

Tag 0EN0 in the Stacks Project.

AlgebraicGeometry.Space.PrimeDivisor.genericResidueFieldEquivHenselian, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/KeyFormula/GenericResidueField.lean, line 284. The attribute's comment: “the residue field of the henselian local ring at the generic point of a prime divisor is the residue field of the chosen chart, canonically through the henselization map”.

The canonical isomorphism κ(u) ≃+* κ(𝒪^h_{X, ξ}) induced by the henselization map 𝒪_{U, u} → 𝒪^h_{X, ξ}.

def PrimeDivisor.genericResidueFieldEquivHenselian :
    letI := henselianLocalRing_isLocalRing B S hS X hX (Z.genericPoint B S hS X) hdec
    Z.genericResidueField B S hS hX hdec ≃+*
      IsLocalRing.ResidueField ↥(Z.genericHenselianLocalRing B S hS hX hdec)

AlgebraicGeometry.Space.exists_residueFieldEquiv_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRingResidueField.lean, line 205. The attribute's comment: “the residue field of the henselian local ring is the residue field of the space. Both fields are determined only up to canonical isomorphism, so the identification is existential, pinned by the isomorphism eκ of the neighborhood residue field with the residue field of the space lying over the space (the morphism g) and by compatibility with the canonical homomorphism out of the neighborhood stalk. No hypothesis is carried: cofilteredness of the elementary étale neighborhoods comes from Stacks 0BGV, nonemptiness from the given neighborhood”.

The residue field of the henselian local ring of a decent algebraic space at a point is the residue field of the space at that point, through an isomorphism compatible with the canonical homomorphism out of the stalk of a given elementary étale neighborhood.

theorem exists_residueFieldEquiv_residueField (hDecent : IsDecentSpace B S hS X)
    (U : ElementaryEtaleNeighborhood B S hS X hX x) :
    letI := henselianLocalRing_isLocalRing B S hS X hX x hDecent
    ∃ (eκ : (neighborhoodFieldPoint B S hS X hX x U).carrier ≃+*
        residueField B S hS X hDecent x)
      (g : (residueFieldRepresentative B S hS X hDecent x).1.siteObject B S hS X ⟶
        (neighborhoodFieldPoint B S hS X hX x U).siteObject B S hS X)
      (e : residueField B S hS X hDecent x ≃+*
        IsLocalRing.ResidueField (henselianLocalRing B S hS X hX x hDecent : Type (u + 1))),
      fieldValuedPointHom B S hS X _ _ g = eκ.toRingHom ∧
        yoneda.map g ≫ fieldMorphism B S hS X (neighborhoodFieldPoint B S hS X hX x U) =
          residueFieldMorphism B S hS X hDecent x ∧
        ∀ r : U.scheme.left.1.presheaf.stalk U.point,
          e (eκ (IsLocalRing.residue _ r)) =
            IsLocalRing.residue _ (stalkToHenselianLocalRing B S hS X hX x hDecent U r)

AlgebraicGeometry.Space.existsUnique_residueFieldEquiv_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/HenselianLocalRingResidueField.lean, line 237. The attribute's comment: “the residue field of the henselian local ring is the residue field of the space, by the canonical isomorphism: the unique one compatible, for every elementary étale neighborhood, with the canonical homomorphism out of its stalk and the homomorphism of residue fields over the space. No neighborhood is assumed; one exists by Stacks 0BBP”.

The residue field of the henselian local ring of a decent algebraic space at a point is the residue field of the space at that point: there is exactly one isomorphism between them compatible with every elementary étale neighborhood of the point, namely the one carrying the class of the image of a germ r of the neighborhood to the value at r of the homomorphism of residue fields lying over the space.

theorem existsUnique_residueFieldEquiv_residueField (hDecent : IsDecentSpace B S hS X) :
    letI := henselianLocalRing_isLocalRing B S hS X hX x hDecent
    ∃! e : IsLocalRing.ResidueField
        (henselianLocalRing B S hS X hX x hDecent : Type (u + 1)) ≃+*
          residueField B S hS X hDecent x,
      ∀ (U : ElementaryEtaleNeighborhood B S hS X hX x)
        (g : (residueFieldRepresentative B S hS X hDecent x).1.siteObject B S hS X ⟶
          (neighborhoodFieldPoint B S hS X hX x U).siteObject B S hS X),
        yoneda.map g ≫ fieldMorphism B S hS X (neighborhoodFieldPoint B S hS X hX x U) =
            residueFieldMorphism B S hS X hDecent x →
        ∀ r : U.scheme.left.1.presheaf.stalk U.point,
          e (IsLocalRing.residue _ (stalkToHenselianLocalRing B S hS X hX x hDecent U r)) =
            fieldValuedPointHom B S hS X (residueFieldRepresentative B S hS X hDecent x).1
              (neighborhoodFieldPoint B S hS X hX x U) g (IsLocalRing.residue _ r)

Tag 0EPL, a remark

Tag 0EPL in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_point_over_elementaryEtaleNeighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodBaseChange.lean, line 50. The attribute's comment: “the unique point above the two distinguished points”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S with X decent, let x be a point of X and let V be an elementary étale neighborhood of the image of x. The fibre product V ×_Y X has exactly one point lying above the distinguished point of V and above x.

theorem existsUnique_point_over_elementaryEtaleNeighborhood
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hX : IsDecentSpace B S hS X.1)
    (x : points B S hS X.1)
    (V : ElementaryEtaleNeighborhood B S hS Y.1 Y.property
      (pointsMap B S hS X.1 f.hom x)) :
    ∃! x' : points B S hS (pullback V.toSpace f.hom),
      pointsMap B S hS (pullback V.toSpace f.hom) (pullback.fst V.toSpace f.hom) x' =
          presheafPoint B S hS V.scheme V.point V.residueField_contained ∧
        pointsMap B S hS (pullback V.toSpace f.hom) (pullback.snd V.toSpace f.hom) x' = x

AlgebraicGeometry.Space.yoneda_map_neighborhoodOver_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodDiagram.lean, line 108. The attribute's comment: “the square of charts over f”.

Stacks 0EPL. The two charts form a commutative square over f: the chart of the upper elementary étale neighborhood maps to the chart of the lower one compatibly with f.

theorem yoneda_map_neighborhoodOver_comp :
    yoneda.map (neighborhoodOver B S hS f V U) ≫ V.toSpace =
      neighborhoodToSource B S hS f V U ≫ f.hom

AlgebraicGeometry.Space.neighborhoodOver_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodDiagram.lean, line 117. The attribute's comment: “the morphism of charts is pointed”.

Stacks 0EPL. The morphism of chart schemes carries the distinguished point of the upper elementary étale neighborhood to that of the lower one.

theorem neighborhoodOver_point
    (hx' : pointsMap B S hS (pullback V.toSpace f.hom) (pullback.fst V.toSpace f.hom) x' =
      presheafPoint B S hS V.scheme V.point V.residueField_contained) :
    (BigFppfOver.toScheme B S hS).map (neighborhoodOver B S hS f V U) U.point = V.point

AlgebraicGeometry.Space.neighborhoodOverSource, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodDiagram.lean, line 178. The attribute's comment: “the upper neighborhood is one of the source”.

Stacks 0EPL. An elementary étale neighborhood of a point x' of V ×_Y X lying over the distinguished point of V and over x is an elementary étale neighborhood of x in X.

This is what makes the identifications of the remark available at (U, u): Stacks 0EMY and Properties of Spaces, Lemma 04KF both ask for an elementary étale neighborhood of the point of the space whose local rings are being computed.

def neighborhoodOverSource
    (hfst : pointsMap B S hS (pullback V.toSpace f.hom) (pullback.fst V.toSpace f.hom) x' =
      presheafPoint B S hS V.scheme V.point V.residueField_contained)
    (hsnd : pointsMap B S hS (pullback V.toSpace f.hom) (pullback.snd V.toSpace f.hom) x' = x) :
    ElementaryEtaleNeighborhood B S hS X.1 X.property x

AlgebraicGeometry.Space.exists_henselianLocalRingMap_of_neighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodDiagram.lean, line 310. The attribute's comment: “the square of henselian local rings”.

Stacks 0EPL. Let (U, u) be an elementary étale neighborhood of a point x of a decent algebraic space X, let (W, w) be one of a point y of a decent algebraic space Y and let j : U ⟶ W be a morphism of the chart schemes carrying u to w. Then there is a local homomorphism 𝒪^h_{Y, y} ⟶ 𝒪^h_{X, x} over the map 𝒪_{W, w} ⟶ 𝒪_{U, u} of neighborhood stalks.

theorem exists_henselianLocalRingMap_of_neighborhood
    (j : U.scheme ⟶ W.scheme) (hj : j.left.1 U.point = W.point) :
    letI := isLocalRing_henselianLocalRing B S hS hX hXdec x
    letI := isLocalRing_henselianLocalRing B S hS hY hYdec y
    ∃ φ : (henselianLocalRing B S hS Y hY y hYdec : Type (u + 1)) →+*
        (henselianLocalRing B S hS X hX x hXdec : Type (u + 1)),
      IsLocalHom φ ∧
      φ.comp (stalkToHenselianLocalRing B S hS Y hY y hYdec W) =
        (stalkToHenselianLocalRing B S hS X hX x hXdec U).comp
          ((W.scheme.left.1.presheaf.stalkCongr (Inseparable.of_eq hj.symm)).hom ≫
            j.left.1.stalkMap U.point).hom

AlgebraicGeometry.Space.exists_diagram_of_neighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodDiagram.lean, line 376. The attribute's comment: “the commutative diagram, as a diagram of ring homomorphisms”.

Stacks 0EPL, the commutative diagram. For a pointed morphism k : (N, n) ⟶ (M, m) of elementary étale neighborhoods over g : X ⟶ Y, the rows

𝒪_{M, m} ⟶ 𝒪^h_{Y, y} ⟶ 𝒪_{Y, w̄} and 𝒪_{N, n} ⟶ 𝒪^h_{X, z} ⟶ 𝒪_{X, z̄}

are joined by local homomorphisms making both squares commute, over the map 𝒪_{M, m} ⟶ 𝒪_{N, n} of neighborhood stalks; and the étale and henselian local rings of the two spaces are the strict henselization and the henselization of the respective neighborhood stalks.

theorem exists_diagram_of_neighborhood (hzbar : zbar.LiesOver z)
    (hwbar : wbar.LiesOver (pointsMap B S hS Xs.1 g.hom z)) :
    letI := isLocalRing_henselianLocalRing B S hS Xs.property hXd z
    letI := isLocalRing_henselianLocalRing B S hS Ys.property hYd
      (pointsMap B S hS Xs.1 g.hom z)
    letI := isLocalRing_etaleLocalRing B S hS Xs.1 Xs.property zbar
    letI := isLocalRing_etaleLocalRing B S hS Ys.1 Ys.property wbar
    ∃ (algN : Algebra (N.scheme.left.1.presheaf.stalk N.point : Type u)
          (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)))
      (algM : Algebra (M.scheme.left.1.presheaf.stalk M.point : Type u)
          (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)))
      (algHX : Algebra (henselianLocalRing B S hS Xs.1 Xs.property z hXd : Type (u + 1))
          (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)))
      (algHY : Algebra (henselianLocalRing B S hS Ys.1 Ys.property
            (pointsMap B S hS Xs.1 g.hom z) hYd : Type (u + 1))
          (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)))
      (φ : (henselianLocalRing B S hS Ys.1 Ys.property
            (pointsMap B S hS Xs.1 g.hom z) hYd : Type (u + 1)) →+*
          (henselianLocalRing B S hS Xs.1 Xs.property z hXd : Type (u + 1)))
      (ψ : (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)) →+*
          (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1))),
      IsLocalHom φ ∧ IsLocalHom ψ ∧
      φ.comp (stalkToHenselianLocalRing B S hS Ys.1 Ys.property
            (pointsMap B S hS Xs.1 g.hom z) hYd M) =
          (stalkToHenselianLocalRing B S hS Xs.1 Xs.property z hXd N).comp
            ((M.scheme.left.1.presheaf.stalkCongr (Inseparable.of_eq hk.symm)).hom ≫
              k.left.1.stalkMap N.point).hom ∧
      (@algebraMap (henselianLocalRing B S hS Xs.1 Xs.property z hXd : Type (u + 1))
            (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)) _ _ algHX).comp
          (stalkToHenselianLocalRing B S hS Xs.1 Xs.property z hXd N) =
        @algebraMap (N.scheme.left.1.presheaf.stalk N.point : Type u)
          (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)) _ _ algN ∧
      (@algebraMap (henselianLocalRing B S hS Ys.1 Ys.property
              (pointsMap B S hS Xs.1 g.hom z) hYd : Type (u + 1))
            (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)) _ _ algHY).comp
          (stalkToHenselianLocalRing B S hS Ys.1 Ys.property
            (pointsMap B S hS Xs.1 g.hom z) hYd M) =
        @algebraMap (M.scheme.left.1.presheaf.stalk M.point : Type u)
          (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)) _ _ algM ∧
      ψ.comp (@algebraMap (henselianLocalRing B S hS Ys.1 Ys.property
              (pointsMap B S hS Xs.1 g.hom z) hYd : Type (u + 1))
            (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)) _ _ algHY) =
        (@algebraMap (henselianLocalRing B S hS Xs.1 Xs.property z hXd : Type (u + 1))
            (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)) _ _ algHX).comp φ ∧
      @IsHenselization (N.scheme.left.1.presheaf.stalk N.point : Type u) _ _ κN _ _
        (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)) _ _ algN ∧
      @IsHenselization (M.scheme.left.1.presheaf.stalk M.point : Type u) _ _ κM _ _
        (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)) _ _ algM

AlgebraicGeometry.Space.exists_diagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodDiagram.lean, line 511. The attribute's comment: “the remark, with both choices made”.

Stacks 0EPL. Let g : X ⟶ Y be a morphism of decent algebraic spaces over S, let z be a point of X with image y in Y, and let z̄ and w̄ be geometric points of X and of Y lying over z and over y. Then there are an elementary étale neighborhood (M, m) of y, an elementary étale neighborhood (N, n) of z and a morphism k : N ⟶ M of chart schemes over g carrying n to m, for which the two rows

𝒪_{M, m} ⟶ 𝒪^h_{Y, y} ⟶ 𝒪_{Y, w̄} and 𝒪_{N, n} ⟶ 𝒪^h_{X, z} ⟶ 𝒪_{X, z̄}

are joined by local homomorphisms making both squares commute, the étale local rings being strict henselizations and the henselian local rings henselizations of the two neighborhood stalks.

Both choices of the remark are made here: (M, m) by Stacks 0BBP, and (N, n) together with k by base change of (M, m) along g, which runs through the fibre product M ×_Y X and chooses an elementary étale neighborhood of the point of it above m and z.

theorem exists_diagram (hzbar : zbar.LiesOver z)
    (hwbar : wbar.LiesOver (pointsMap B S hS Xs.1 g.hom z)) :
    letI := isLocalRing_henselianLocalRing B S hS Xs.property hXd z
    letI := isLocalRing_henselianLocalRing B S hS Ys.property hYd
      (pointsMap B S hS Xs.1 g.hom z)
    letI := isLocalRing_etaleLocalRing B S hS Xs.1 Xs.property zbar
    letI := isLocalRing_etaleLocalRing B S hS Ys.1 Ys.property wbar
    ∃ (M₀ : ElementaryEtaleNeighborhood B S hS Ys.1 Ys.property
          (pointsMap B S hS Xs.1 g.hom z))
      (N₀ : ElementaryEtaleNeighborhood B S hS Xs.1 Xs.property z)
      (k₀ : N₀.scheme ⟶ M₀.scheme) (hk₀ : k₀.left.1 N₀.point = M₀.point)
      (algN : Algebra (N₀.scheme.left.1.presheaf.stalk N₀.point : Type u)
          (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)))
      (algM : Algebra (M₀.scheme.left.1.presheaf.stalk M₀.point : Type u)
          (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)))
      (algHX : Algebra (henselianLocalRing B S hS Xs.1 Xs.property z hXd : Type (u + 1))
          (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)))
      (algHY : Algebra (henselianLocalRing B S hS Ys.1 Ys.property
            (pointsMap B S hS Xs.1 g.hom z) hYd : Type (u + 1))
          (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)))
      (φ : (henselianLocalRing B S hS Ys.1 Ys.property
            (pointsMap B S hS Xs.1 g.hom z) hYd : Type (u + 1)) →+*
          (henselianLocalRing B S hS Xs.1 Xs.property z hXd : Type (u + 1)))
      (ψ : (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)) →+*
          (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1))),
      yoneda.map k₀ ≫ M₀.toSpace = N₀.toSpace ≫ g.hom ∧
      IsLocalHom φ ∧ IsLocalHom ψ ∧
      φ.comp (stalkToHenselianLocalRing B S hS Ys.1 Ys.property
            (pointsMap B S hS Xs.1 g.hom z) hYd M₀) =
          (stalkToHenselianLocalRing B S hS Xs.1 Xs.property z hXd N₀).comp
            ((M₀.scheme.left.1.presheaf.stalkCongr (Inseparable.of_eq hk₀.symm)).hom ≫
              k₀.left.1.stalkMap N₀.point).hom ∧
      (@algebraMap (henselianLocalRing B S hS Xs.1 Xs.property z hXd : Type (u + 1))
            (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)) _ _ algHX).comp
          (stalkToHenselianLocalRing B S hS Xs.1 Xs.property z hXd N₀) =
        @algebraMap (N₀.scheme.left.1.presheaf.stalk N₀.point : Type u)
          (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)) _ _ algN ∧
      (@algebraMap (henselianLocalRing B S hS Ys.1 Ys.property
              (pointsMap B S hS Xs.1 g.hom z) hYd : Type (u + 1))
            (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)) _ _ algHY).comp
          (stalkToHenselianLocalRing B S hS Ys.1 Ys.property
            (pointsMap B S hS Xs.1 g.hom z) hYd M₀) =
        @algebraMap (M₀.scheme.left.1.presheaf.stalk M₀.point : Type u)
          (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)) _ _ algM ∧
      ψ.comp (@algebraMap (henselianLocalRing B S hS Ys.1 Ys.property
              (pointsMap B S hS Xs.1 g.hom z) hYd : Type (u + 1))
            (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)) _ _ algHY) =
        (@algebraMap (henselianLocalRing B S hS Xs.1 Xs.property z hXd : Type (u + 1))
            (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)) _ _ algHX).comp φ ∧
      @IsHenselization (N₀.scheme.left.1.presheaf.stalk N₀.point : Type u) _ _ (SeparableClosure
          (ResidueField (N₀.scheme.left.1.presheaf.stalk N₀.point : Type u))) _ _
        (etaleLocalRing B S hS Xs.1 zbar : Type (u + 1)) _ _ algN ∧
      @IsHenselization (M₀.scheme.left.1.presheaf.stalk M₀.point : Type u) _ _ (SeparableClosure
          (ResidueField (M₀.scheme.left.1.presheaf.stalk M₀.point : Type u))) _ _
        (etaleLocalRing B S hS Ys.1 wbar : Type (u + 1)) _ _ algM

Declarations registered for the tag:

AlgebraicGeometry.isAlgebraicSpace_pullback, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodBaseChange.lean, line 41 (StacksFrontier): “the fibre product is an algebraic space”.
AlgebraicGeometry.Space.isEtale_of_isPullback, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ElementaryEtaleNeighborhoodBaseChange.lean, line 43 (StacksFrontier): “the projection to the source is étale”.

Sources

LeanAlgebraicGeometry.Space.iso_of_mono_of_point_eq · AlgebraicGeometry.Space.IsDecentSpace.hasMonomorphicFieldRepresentative · AlgebraicGeometry.Space.residueFieldRepresentative · AlgebraicGeometry.Space.residueField · AlgebraicGeometry.Space.residueFieldRepresentative_unique · AlgebraicGeometry.Space.isIso_residueFieldHom_iff_mono · AlgebraicGeometry.Space.exists_affine_elementaryEtaleNeighborhood' · AlgebraicGeometry.Space.ElementaryEtaleNeighborhood

Section68.12 Points on decent spaces #

Section 68.12 of the Stacks Project, Tag 03IG. 8 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03K5, a lemma

Tag 03K5 in the Stacks Project.

AlgebraicGeometry.Space.eq_of_specializes_of_pointsMap_eq_of_hasFiniteChartFibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/Specializations.lean, line 406.

Stacks 03K5. Let X be an algebraic space over S every point of which satisfies condition (2) of Stacks 03JS — in particular, a decent one — and let h_U ⟶ X be an étale chart of X by a scheme. Two points of the chart with the same image in X, one a specialization of the other, are equal.

theorem eq_of_specializes_of_pointsMap_eq_of_hasFiniteChartFibers
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hdecent : HasFiniteChartFibersAtEveryPoint B S hS X)
    (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X)
    (hφ : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf φ)
    (u u' : points B S hS (yoneda.obj U))
    (huu' : pointsMap B S hS (yoneda.obj U) φ u = pointsMap B S hS (yoneda.obj U) φ u')
    (hs : u' ⤳ u) : u = u'

Tag 03IL, a lemma

Tag 03IL in the Stacks Project.

AlgebraicGeometry.Space.exists_specialization_lift_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDimensionFunction.lean, line 183.

Stacks 03IL. Let X be a decent algebraic space over a scheme S and let x, x' be points of |X| with x' ⤳ x, that is, x a specialization of x'. Then for every étale φ : h_U ⟶ X with U an object of the site and every point p of |U| above x there is a point p' ⤳ p of |U| above x'.

This is the source's "combine 03JX and 03K2": decency is condition (4) of Stacks 03JV at every point, which gives condition (1) at x' by, in this namespace, HasQuasiCompactMonomorphicFieldRepresentative.hasFiniteFibresOnEveryAffineEtaleChart, and that is the hypothesis of AlgebraicGeometry.Space.exists_specialization_lift_of_finite_etale_fibers.

theorem exists_specialization_lift_of_isDecentSpace
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hXdec : IsDecentSpace B S hS X) (x x' : points B S hS X) (hs : x' ⤳ x)
    (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X)
    (hφ : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) φ)
    (p : points B S hS (yoneda.obj U)) (hp : pointsMap B S hS (yoneda.obj U) φ p = x) :
    ∃ p' : points B S hS (yoneda.obj U),
      p' ⤳ p ∧ pointsMap B S hS (yoneda.obj U) φ p' = x'

Tag 03K3, a lemma

Tag 03K3 in the Stacks Project.

AlgebraicGeometry.Space.t0Space_points_of_hasFiniteChartFibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/Points.lean, line 59.

Stacks 03K3. The point space of an algebraic space over S all of whose points have finite fibres in every étale chart by an affine scheme — in particular, of a decent algebraic space — is Kolmogorov.

theorem t0Space_points_of_hasFiniteChartFibers
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hdecent : HasFiniteChartFibersAtEveryPoint B S hS X) :
    T0Space (points B S hS X)

AlgebraicGeometry.Space.t0Space_points_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/Sober.lean, line 107.

Stacks 03K3. The point space of a decent algebraic space over S is Kolmogorov: decency is condition (4) of Stacks 03JV at every point, which gives condition (α) of Stacks 03JX, and Stacks 03K3 concludes.

Kolmogorov is T0Space; StacksFrontier.Topology.Sober.Defs identifies Definition 004X's Kolmogorov condition with T0Space in kolmogorov_iff.

theorem t0Space_points_of_isDecentSpace (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) : T0Space (points B S hS X)

Tag 03K6, a proposition

Tag 03K6 in the Stacks Project.

AlgebraicGeometry.Space.stacksSober_points_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/Sober.lean, line 155.

Stacks 03K6. The point space of a decent algebraic space over S is sober in the sense of Stacks 004X: it is Kolmogorov, and every irreducible closed subset of it has a unique generic point.

theorem stacksSober_points_of_isDecentSpace (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) : StacksSober (points B S hS X)

Tag 0A4J, a lemma

Tag 0A4J 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: “part (1)”.

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.topologicalKrullDim_points_eq_dimension_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/Dimension.lean, line 133. The attribute's comment: “part (2)”.

Stacks 0A4J, part (2). The Krull dimension of the point space of a decent algebraic space over S agrees with the dimension of the space, as defined by étale scheme charts.

theorem topologicalKrullDim_points_eq_dimension_of_isDecentSpace
    (hX : IsAlgebraicSpace B S hS X) (hdec : IsDecentSpace B S hS X) :
    topologicalKrullDim (points B S hS X) = dimension B S hS X hX

Tag 0ABW, a lemma

Tag 0ABW in the Stacks Project.

AlgebraicGeometry.Space.localRingDimension_le_of_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/GenericPointsAndDimension.lean, line 142.

A locally quasi-finite morphism of algebraic spaces over S does not increase the dimension of the local ring: for a point x of the source, the dimension of the local ring there is at most the dimension of the local ring of the target at the image of x.

theorem localRingDimension_le_of_isLocallyQuasiFinite
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyQuasiFinite B S hS f)
    (x : points B S hS X) :
    localRingDimension B S hS x ≤
      localRingDimension B S hS (pointsMap B S hS X f x)

Tag 0ED0, a lemma

Tag 0ED0 in the Stacks Project.

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

Stacks 0ED0. The dimension of the source of a locally quasi-finite morphism of algebraic spaces over S is at most the dimension of its target.

theorem dimension_le_of_isLocallyQuasiFinite
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyQuasiFinite B S hS f) :
    dimension B S hS X hX ≤ dimension B S hS Y hY

Tag 03IK, a lemma

Tag 03IK in the Stacks Project.

AlgebraicGeometry.Space.exists_iso_yoneda_spec_of_isDecentSpace_of_etale_fieldSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FieldAtlas.lean, line 76.

Stacks Project, Tag 03IK. Let S be a scheme, let k be a field and let F be an algebraic space over S admitting a surjective étale morphism from the spectrum of k. If F is decent then F is represented by the spectrum of a field k' over S, with k a finite separable extension of k', and under that identification the given morphism is the one induced by the extension k/k'.

theorem exists_iso_yoneda_spec_of_isDecentSpace_of_etale_fieldSpec
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hdecent : IsDecentSpace B S hS F)
    (k : Type u) [Field k] (hk : B.Contains (Spec (.of k))) (b : Spec (.of k) ⟶ S)
    (f : yoneda.obj (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS)) ⟶ F)
    (hsurj : IsSurjective B S hS f)
    (hetale : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k' k) (_ : Module.Finite k' k)
      (_ : Algebra.IsSeparable k' k) (hk' : B.Contains (Spec (.of k')))
      (b' : Spec (.of k') ⟶ S),
      ∃ (hbase : Spec.map (CommRingCat.ofHom (algebraMap k' k)) ≫ b' = b)
        (e : F ≅ yoneda.obj (Over.mk (⟨b'⟩ : B.obj hk' ⟶ B.obj hS))),
        f ≫ e.hom = yoneda.map (Over.homMk
          (ObjectProperty.homMk (Spec.map (CommRingCat.ofHom (algebraMap k' k))) :
            B.obj hk ⟶ B.obj hk') (by
              apply ObjectProperty.hom_ext
              simpa using hbase))

Sources

Section68.13 Reduced singleton spaces #

Section 68.13 of the Stacks Project, Tag 06QU. 12 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06QV, a lemma

Tag 06QV in the Stacks Project.

AlgebraicGeometry.Space.isSurjective_of_fieldCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFieldCover.lean, line 241. The attribute's comment: “surjectivity”.

Stacks 06QV, surjectivity. If an algebraic space over S receives a surjective morphism from the spectrum of a field, then every morphism to it from the spectrum of a field is surjective.

Only the existence of the surjective field-valued morphism is used: it forces the point set of the target to be a singleton, and the point set of a field spectrum is nonempty.

theorem isSurjective_of_fieldCover
    (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
    (b : Spec (.of k) ⟶ S)
    (f : yoneda.obj (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS)) ⟶ Z)
    (hsurj : IsSurjective B S hS f)
    (k' : Type u) [Field k'] (hk' : B.Contains (Spec (.of k')))
    (b' : Spec (.of k') ⟶ S)
    (g : yoneda.obj (Over.mk (⟨b'⟩ : B.obj hk' ⟶ B.obj hS)) ⟶ Z) :
    IsSurjective B S hS g

AlgebraicGeometry.Space.isFlat_of_fieldCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFieldCover.lean, line 267. The attribute's comment: “flatness”.

Stacks 06QV, flatness. If an algebraic space over S receives a surjective flat morphism from the spectrum of a field, then every morphism to it from the spectrum of a field is flat.

The algebraic-space hypothesis _hZ is retained from the source but is not needed: the argument only uses that the chart b₀ of Z is relatively representable and étale, which is a hypothesis of the chart condition itself.

theorem isFlat_of_fieldCover
    (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (_hZ : IsAlgebraicSpace B S hS Z)
    (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
    (b : Spec (.of k) ⟶ S)
    (f : yoneda.obj (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS)) ⟶ Z)
    (hsurj : IsSurjective B S hS f)
    (hflat : IsFlat B S hS f)
    (k' : Type u) [Field k'] (hk' : B.Contains (Spec (.of k')))
    (b' : Spec (.of k') ⟶ S)
    (g : yoneda.obj (Over.mk (⟨b'⟩ : B.obj hk' ⟶ B.obj hS)) ⟶ Z) :
    IsFlat B S hS g

Tag 06QW, a lemma

Tag 06QW in the Stacks Project.

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

Stacks 06QW, conditions (1) and (2). A reduced algebraic space over S has exactly one point if and only if it admits a surjective flat morphism from the spectrum of a field.

theorem isReduced_and_singleton_points_iff_hasFlatFieldCover
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F) :
    (HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} => IsReduced X) ∧
      Nonempty (points B S hS F) ∧ Subsingleton (points B S hS F)) ↔
        HasFlatFieldCover B S hS F

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

Stacks 06QW, conditions (2) and (3). A surjective flat morphism to an algebraic space over S from the spectrum of a field may be replaced by one that is in addition locally of finite type.

theorem hasFlatFieldCover_iff_hasLocallyOfFiniteTypeFlatFieldCover
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F) :
    HasFlatFieldCover B S hS F ↔ HasLocallyOfFiniteTypeFlatFieldCover B S hS F

Tag 06QX, a lemma

Tag 06QX in the Stacks Project.

AlgebraicGeometry.Space.isReduced_locallyNoetherian_singleton_iff_hasFinitePresentationCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReducedSingleton.lean, line 538.

Stacks 06QX. A reduced, locally Noetherian algebraic space over S has exactly one point if and only if it admits a flat, surjective, locally finitely presented morphism from the spectrum of a field.

theorem isReduced_locallyNoetherian_singleton_iff_hasFinitePresentationCover
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F) :
    (HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} => IsReduced X) ∧
      HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} => IsLocallyNoetherian X) ∧
      Nonempty (points B S hS F) ∧ Subsingleton (points B S hS F)) ↔
    HasLocallyOfFinitePresentationFlatFieldCover B S hS F

Tag 06QY, a lemma

Tag 06QY in the Stacks Project.

AlgebraicGeometry.Space.isEmpty_points_or_isIso_of_mono_of_hasFinitePresentationCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReducedSingleton.lean, line 650.

Stacks 06QY. Let f : Z' ⟶ Z be a monomorphism of algebraic spaces over S, and suppose Z admits a surjective, flat, locally finitely presented morphism from the spectrum of a field. Then either Z' is empty or f is an isomorphism.

theorem isEmpty_points_or_isIso_of_mono_of_hasFinitePresentationCover
    {Z' Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hZ' : IsAlgebraicSpace B S hS Z') (hZ : IsAlgebraicSpace B S hS Z) (f : Z' ⟶ Z) [Mono f]
    (hcover : HasLocallyOfFinitePresentationFlatFieldCover B S hS Z) :
    IsEmpty (points B S hS Z') ∨ IsIso f

Tag 06QZ, a lemma

Tag 06QZ in the Stacks Project.

AlgebraicGeometry.Space.exists_isResidualSpaceAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidualSpaceExistence.lean, line 1177. The attribute's comment: “existence”.

Stacks 06QZ, existence. Every point of an algebraic space carries a residual space: a monomorphism from a reduced, locally Noetherian algebraic space with exactly one point, whose image on points is that point.

theorem exists_isResidualSpaceAt (hXalg : IsAlgebraicSpace B S hS X)
    (x : points B S hS X) :
    ∃ (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : Z ⟶ X),
      IsResidualSpaceAt B S hS X x f

AlgebraicGeometry.Space.existsUnique_isResidualSpaceAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidualSpaceUniqueness.lean, line 104.

Every point x of an algebraic space X over S has a unique residual space: there is a monomorphism Z ⟶ X with Z a reduced, locally Noetherian algebraic space whose point set is the singleton {x}, and any two such are isomorphic over X by exactly one isomorphism.

theorem existsUnique_isResidualSpaceAt (hX : IsAlgebraicSpace B S hS X)
    (x : points B S hS X) :
    (∃ (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : Z ⟶ X), IsResidualSpaceAt B S hS X x f) ∧
      ∀ (Z Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : Z ⟶ X) (f' : Z' ⟶ X),
        IsResidualSpaceAt B S hS X x f → IsResidualSpaceAt B S hS X x f' →
        ∃! e : Z' ≅ Z, e.hom ≫ f = f'

Tag 06R0, a definition

Tag 06R0 in the Stacks Project.

AlgebraicGeometry.Space.IsResidualSpaceAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReducedSingleton.lean, line 698.

Stacks 06R0. A monomorphism f : Z ⟶ X of algebraic spaces over S exhibits Z as a residual space of X at a point x of |X| when Z is reduced and locally Noetherian, |Z| consists of exactly one point, and that point maps to x. Reducedness and local Noetherianity are the étale-local scheme properties of Stacks 03E6.

def IsResidualSpaceAt (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (x : points B S hS X)
    {Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : Z ⟶ X) : Prop

Tag 0H1R, a lemma

Tag 0H1R in the Stacks Project.

AlgebraicGeometry.Space.exists_isIso_fieldMorphism_iff_hasMonomorphicFieldRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidualSpaceFieldSpectrum.lean, line 108. The attribute's comment: “the equivalence at a point”.

Stacks 0H1R, the equivalence at a point. Let X be an algebraic space over S, let x be a point of |X| and let f : Z ⟶ X be a residual space of X at x. Then Z is the spectrum of a field if and only if x can be represented by a monomorphism from the spectrum of a field.

For the easy implication, the presenting morphism of a field-valued point of Z which is an isomorphism, composed with the monomorphism f, is a monomorphism representing x, since the only point of |Z| maps to x.

Conversely, let g : yoneda.obj (Spec k over S) ⟶ X be a monomorphism representing x. The only point of |Z| and the point of the field spectrum both map to x, so the fibre product Z ×_X Spec k has a point by Stacks 03H4; its projection to the field spectrum is a monomorphism, hence an isomorphism by Stacks 06MG. That produces a monomorphism Spec k ⟶ Z with nonempty source, and Z, being reduced and locally Noetherian with exactly one point, has a flat, surjective, locally finitely presented cover by the spectrum of a field by Stacks 06QX, so the monomorphism is an isomorphism by Stacks 06QY.

theorem exists_isIso_fieldMorphism_iff_hasMonomorphicFieldRepresentative
    (hX : IsAlgebraicSpace B S hS X) (x : points B S hS X) (f : Z ⟶ X)
    (hf : IsResidualSpaceAt B S hS X x f) :
    (∃ q : FieldValuedPoint B S hS Z, IsIso (fieldMorphism B S hS Z q)) ↔
      HasMonomorphicFieldRepresentative B S hS X x

AlgebraicGeometry.Space.exists_isIso_fieldMorphism_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidualSpaceFieldSpectrum.lean, line 163. The attribute's comment: “the assertion for a decent algebraic space”.

Stacks 0H1R, the assertion for a decent algebraic space: every residual space of a decent algebraic space over S is the spectrum of a field.

A decent algebraic space has a monomorphic field-valued representative at every point, which is condition (4) of Stacks 03JV, so the equivalence AlgebraicGeometry.Space.exists_isIso_fieldMorphism_iff_hasMonomorphicFieldRepresentative applies at every point.

theorem exists_isIso_fieldMorphism_of_isDecentSpace (hX : IsAlgebraicSpace B S hS X)
    (hdecent : IsDecentSpace B S hS X) (x : points B S hS X) (f : Z ⟶ X)
    (hf : IsResidualSpaceAt B S hS X x f) :
    ∃ q : FieldValuedPoint B S hS Z, IsIso (fieldMorphism B S hS Z q)

Tag 06R1, a lemma

Tag 06R1 in the Stacks Project.

AlgebraicGeometry.Space.hasEtaleLocalProperty_isRegular_of_isReduced_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReducedSingleton.lean, line 567.

Stacks 06R1. A reduced, locally Noetherian algebraic space over S with exactly one point is regular.

theorem hasEtaleLocalProperty_isRegular_of_isReduced_of_isLocallyNoetherian
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hred : HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} => IsReduced X))
    (hnoeth : HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} => IsLocallyNoetherian X))
    (hnonempty : Nonempty (points B S hS F)) (hsub : Subsingleton (points B S hS F)) :
    HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} => IsRegular X)

Tag 0H1S, a lemma

Tag 0H1S in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_comp_eq_of_isResidualSpaceAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReducedToResidualSpaceFactorization.lean, line 351. The attribute's comment: “the factorization through a given residual space at the point”.

A morphism from a reduced space with image one point of a locally Noetherian space factors through every residual space at that point. Let S be a scheme, let f : Y ⟶ X be a morphism of algebraic spaces over S and let x be a point of |X|. Assume that the image of |Y| → |X| is contained in {x}, that Y is reduced and that X is locally Noetherian. Then f factors uniquely through any residual space i : Z ⟶ X of X at x.

theorem existsUnique_comp_eq_of_isResidualSpaceAt
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : Y ⟶ X) (x : points B S hS X) (i : Z ⟶ X)
    (hi : IsResidualSpaceAt B S hS X x i)
    (himage : Set.range (pointsMap B S hS Y f) ⊆ {x})
    (hred : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsReduced T))
    (hN : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T)) :
    ∃! g : Y ⟶ Z, g ≫ i = f

AlgebraicGeometry.Space.exists_isResidualSpaceAt_and_existsUnique_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReducedToResidualSpaceFactorization.lean, line 415.

A morphism from a reduced space with image one point of a locally Noetherian space factors through a residual space. Let f : Y ⟶ X be a morphism of algebraic spaces whose image in |X| is contained in {x}, with Y reduced and X locally Noetherian. Then there is a residual space of X at x through which f factors, by a unique morphism.

theorem exists_isResidualSpaceAt_and_existsUnique_comp_eq
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : Y ⟶ X) (x : points B S hS X)
    (himage : Set.range (pointsMap B S hS Y f) ⊆ {x})
    (hred : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsReduced T))
    (hN : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T)) :
    ∃ (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (i : Z ⟶ X),
      IsResidualSpaceAt B S hS X x i ∧ ∃! g : Y ⟶ Z, g ≫ i = f

Tag 0H1T, a lemma

Tag 0H1T in the Stacks Project.

AlgebraicGeometry.Space.isResidualSpaceAt_fieldMorphism_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidualSpaceFactorization.lean, line 305. The attribute's comment: “the residual space at the point is the spectrum of the field of hypothesis (3)”.

The morphism presented by a monomorphic field-valued representative of a point x of an algebraic space X over S exhibits the spectrum of its field as a residual space of X at x in the sense of Stacks 06R0.

The spectrum of a field is reduced and locally Noetherian and has exactly one point, and that point goes to x because the representative represents x.

theorem isResidualSpaceAt_fieldMorphism_of_mono
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (x : points B S hS X)
    (p : FieldValuedPoint B S hS X) (hpx : p.class B S hS X = x)
    (hmono : Mono (fieldMorphism B S hS X p)) :
    IsResidualSpaceAt B S hS X x (fieldMorphism B S hS X p)

AlgebraicGeometry.Space.exists_comp_fieldMorphism_eq_of_range_pointsMap_subset_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidualSpaceFactorization.lean, line 340.

Stacks 0H1T. Let f : Y ⟶ X be a morphism of algebraic spaces over S and let x be a point of |X|. Assume that the image of |Y| in |X| is contained in {x}, that Y is reduced, and that x is represented by a quasi-compact monomorphism from the spectrum of a field. Then f factors through that monomorphism, which by AlgebraicGeometry.Space.isResidualSpaceAt_fieldMorphism_of_mono is a residual space of X at x.

Replace X by a quasi-compact open subspace containing x and apply Stacks 0BBN: the point lies in a stratum, a reduced closed subspace of an open subspace which is a scheme. Both f and the representative factor through that open subspace by Stacks 03IE and through the stratum by Stacks 03JJ, which is where reducedness of Y enters. That leaves the case of a morphism into a representable presheaf monomorphic over X, which Stacks 0H1M and Stacks 0H2X settle on a surjective étale scheme chart of Y.

theorem exists_comp_fieldMorphism_eq_of_range_pointsMap_subset_singleton
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : Y ⟶ X) (x : points B S hS X)
    (hf : Set.range (pointsMap B S hS Y f) ⊆ {x})
    (hred : HasEtaleLocalProperty B S hS Y (fun W : Scheme.{u} => IsReduced W))
    (p : FieldValuedPoint B S hS X) (hpx : p.class B S hS X = x)
    (hmono : Mono (fieldMorphism B S hS X p))
    (hqc : IsQuasiCompact B S hS (fieldMorphism B S hS X p)) :
    ∃ g : Y ⟶ yoneda.obj (p.siteObject B S hS X),
      g ≫ fieldMorphism B S hS X p = f

AlgebraicGeometry.Space.exists_isResidualSpaceAt_comp_fieldMorphism_eq_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidualSpaceFactorization.lean, line 475. The attribute's comment: “hypothesis (3) supplied by decency of the target”.

Stacks 0H1T with hypothesis (3) supplied by its parenthetical: for a decent algebraic space X over S, a morphism f : Y ⟶ X from a reduced algebraic space whose image on points is contained in {x} factors through a residual space of X at x, and that residual space is the spectrum of a field.

Decency of Stacks 03I8 is condition (4) of Stacks 03JV at every point, which is hypothesis (3) at x.

theorem exists_isResidualSpaceAt_comp_fieldMorphism_eq_of_isDecentSpace
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : Y ⟶ X) (x : points B S hS X)
    (hf : Set.range (pointsMap B S hS Y f) ⊆ {x})
    (hred : HasEtaleLocalProperty B S hS Y (fun W : Scheme.{u} => IsReduced W))
    (hdecent : IsDecentSpace B S hS X) :
    ∃ p : FieldValuedPoint B S hS X,
      IsResidualSpaceAt B S hS X x (fieldMorphism B S hS X p) ∧
      ∃ g : Y ⟶ yoneda.obj (p.siteObject B S hS X),
        g ≫ fieldMorphism B S hS X p = f

Tag 0H2Y, an example

Tag 0H2Y in the Stacks Project.

AlgebraicGeometry.ProfiniteTranslation.not_exists_comp_orbitMap_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ProfiniteTranslationNoFieldFactorization.lean, line 935. The attribute's comment: “the orbit map of the origin has no section”.

The orbit map of the origin admits no section. For an infinite profinite group G and a field k, the orbit map of the origin from the discrete k-scheme Γ = ∐_{g ∈ G} Spec k to the zero-dimensional affine k-scheme Y = Spec (LocallyConstant G k) admits no section.

theorem not_exists_comp_orbitMap_eq_id [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Infinite G] :
    ¬ ∃ s : Spec (.of (LocallyConstant G k)) ⟶ ∐ (fun _ : G => Spec (.of k)),
        s ≫ orbitMap k G = 𝟙 _

AlgebraicGeometry.Space.not_isLocallyNoetherian_and_not_isDecentSpace_of_not_exists_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ProfiniteTranslationNoFieldFactorization.lean, line 1093. The attribute's comment: “the one-point algebraic space and the non-factorization”.

The one-point quotient of an infinite profinite group by translation. Let k be a field and let G be an infinite profinite group. Let Y = Spec (LocallyConstant G k) be G as a zero-dimensional affine k-scheme, let Γ be G as a discrete k-group scheme acting on Y by translations, and let X = Y/Γ with projection q : Y ⟶ X. Then X is an algebraic space with a single point, Y is reduced, the k-point of X at the origin is a monomorphism, and q factors through no field-valued point of X whatsoever.

theorem not_isLocallyNoetherian_and_not_isDecentSpace_of_not_exists_section :
    IsAlgebraicSpace B (Spec (.of k)) hS (profiniteTranslationQuotient k G B hS hY) ∧
      Subsingleton (points B (Spec (.of k)) hS
        (profiniteTranslationQuotient k G B hS hY)) ∧
      HasEtaleLocalProperty B (Spec (.of k)) hS
        (yoneda.obj (profiniteChart k G B hS hY)) (fun T : Scheme.{u} => IsReduced T) ∧
      Mono (fieldMorphism B (Spec (.of k)) hS _ (originQuotientPoint k G B hS hY)) ∧
      ∀ (p : FieldValuedPoint B (Spec (.of k)) hS
          (profiniteTranslationQuotient k G B hS hY))
        (g : yoneda.obj (profiniteChart k G B hS hY) ⟶
          yoneda.obj (p.siteObject B (Spec (.of k)) hS _)),
        g ≫ fieldMorphism B (Spec (.of k)) hS _ p ≠ profiniteQuotientMap k G B hS hY

AlgebraicGeometry.Space.not_isLocallyNoetherian_and_not_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ProfiniteTranslationNoFieldFactorization.lean, line 1145. The attribute's comment: “the conclusion for the quotient of a profinite group by translation”.

The quotient of an infinite profinite group by translation is neither locally Noetherian nor decent. For the quotient X = Y/Γ of the previous theorem, the conclusion of Stacks 0H1S and of Stacks 0H1T fails for the projection q : Y ⟶ X at every residual space of X at its point.

theorem not_isLocallyNoetherian_and_not_isDecentSpace :
    ¬ HasEtaleLocalProperty B (Spec (.of k)) hS (profiniteTranslationQuotient k G B hS hY)
        (fun T : Scheme.{u} => IsLocallyNoetherian T) ∧
      ¬ IsDecentSpace B (Spec (.of k)) hS (profiniteTranslationQuotient k G B hS hY) ∧
      ∀ {W : (BigFppfOver B (Spec (.of k)) hS)ᵒᵖ ⥤ Type u}
        (i : W ⟶ profiniteTranslationQuotient k G B hS hY),
        IsResidualSpaceAt B (Spec (.of k)) hS (profiniteTranslationQuotient k G B hS hY)
          ((originQuotientPoint k G B hS hY).class B (Spec (.of k)) hS _) i →
        ¬ ∃ g : yoneda.obj (profiniteChart k G B hS hY) ⟶ W,
            g ≫ i = profiniteQuotientMap k G B hS hY

Tag 0H1U, a lemma

Tag 0H1U in the Stacks Project.

AlgebraicGeometry.Space.isClosed_singleton_iff_isClosedImmersion_of_isResidualSpaceAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReducedSingleton.lean, line 762.

Stacks Project, Tag 0H1U. Let S be a scheme, let X be an algebraic space over S which is locally Noetherian, let x be a point of |X|, and let f : Z ⟶ X be a residual space of X at x. Then x is a closed point of |X| if and only if f is a closed immersion. The hypothesis huniq is the uniqueness part of Stacks 06QZ: every residual space of X at x is isomorphic to f over X.

theorem isClosed_singleton_iff_isClosedImmersion_of_isResidualSpaceAt
    (hX : IsAlgebraicSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (x : points B S hS X) (f : Z ⟶ X) (hf : IsResidualSpaceAt B S hS X x f)
    (huniq : ∀ (W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (g : W ⟶ X),
      IsResidualSpaceAt B S hS X x g → ∃ e : W ≅ Z, e.hom ≫ f = g) :
    _root_.IsClosed ({x} : Set (points B S hS X)) ↔ IsClosedImmersion B S hS f

AlgebraicGeometry.Space.isClosed_singleton_iff_exists_isResidualSpaceAt_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReducedSingleton.lean, line 790. The attribute's comment: “the equivalence through the existence of a residual space”.

Stacks Project, Tag 0H1U, phrased so as not to refer to the uniqueness of the residual space: a point x of the point set of a locally Noetherian algebraic space X over S is closed exactly when some residual space of X at x is a closed subspace of X.

theorem isClosed_singleton_iff_exists_isResidualSpaceAt_isClosedImmersion
    (hX : IsAlgebraicSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (x : points B S hS X) :
    _root_.IsClosed ({x} : Set (points B S hS X)) ↔
      ∃ (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : Y ⟶ X),
        IsResidualSpaceAt B S hS X x f ∧ IsClosedImmersion B S hS f

AlgebraicGeometry.Space.IsResidualSpaceAt.isClosed_singleton_iff_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ResidualSpaceClosedPoint.lean, line 78. The attribute's comment: “stated for any residual space of X at x”.

Stacks Project, Tag 0H1U. Let S be a scheme, let X be an algebraic space over S which is locally Noetherian, let x be a point of |X|, and let f : Z ⟶ X be a residual space of X at x. Then x is a closed point of |X| if and only if f is a closed immersion.

One implication is AlgebraicGeometry.Space.isClosed_singleton_of_isClosedImmersion_of_isResidualSpaceAt. For the other, the reduced closed subspace of X on the closed point {x} is a residual space of X at x and its inclusion is a closed immersion; the uniqueness half of Stacks 06QZ identifies f with that inclusion up to an isomorphism of its source over X, and being a closed immersion is invariant under such an isomorphism.

theorem IsResidualSpaceAt.isClosed_singleton_iff_isClosedImmersion
    (hX : IsAlgebraicSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    {x : points B S hS X} {f : Z ⟶ X} (hf : IsResidualSpaceAt B S hS X x f) :
    _root_.IsClosed ({x} : Set (points B S hS X)) ↔ IsClosedImmersion B S hS f

Sources

LeanAlgebraicGeometry.Space.isSurjective_of_fieldCover · AlgebraicGeometry.Space.isFlat_of_fieldCover · AlgebraicGeometry.Space.isReduced_and_singleton_points_iff_hasFlatFieldCover · AlgebraicGeometry.Space.hasFlatFieldCover_iff_hasLocallyOfFiniteTypeFlatFieldCover · AlgebraicGeometry.Space.isReduced_locallyNoetherian_singleton_iff_hasFinitePresentationCover · AlgebraicGeometry.Space.isEmpty_points_or_isIso_of_mono_of_hasFinitePresentationCover · AlgebraicGeometry.Space.exists_isResidualSpaceAt · AlgebraicGeometry.Space.existsUnique_isResidualSpaceAt

Section68.14 Decent spaces #

Section 68.14 of the Stacks Project, Tag 047Y. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BB6, a lemma

Tag 0BB6 in the Stacks Project.

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_isLocallyNoetherian_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/NoetherianQuasiSeparated.lean, line 574.

A locally Noetherian decent algebraic space is quasi-separated.

theorem isAbsolutelyQuasiSeparated_of_isLocallyNoetherian_of_isDecentSpace
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (hNoeth : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} => IsLocallyNoetherian Y))
    (hdec : IsDecentSpace B S hS X) :
    IsAbsolutelyQuasiSeparated B S hS hZ X

Tag 047Z, a lemma

Tag 047Z in the Stacks Project.

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

Stacks 047Z, part (1). A decent algebraic space over S whose point set is a singleton is a scheme.

theorem isRepresentable_of_subsingleton_points (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) (hne : Nonempty (points B S hS X))
    (hsub : Subsingleton (points B S hS X)) : X.IsRepresentable

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

Stacks 047Z, part (2). A reduced decent algebraic space over S whose point set is a singleton is the spectrum of a field.

theorem exists_iso_yoneda_spec_of_subsingleton_points (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) (hne : Nonempty (points B S hS X))
    (hsub : Subsingleton (points B S hS X))
    (hred : HasEtaleLocalProperty B S hS X (fun Y : Scheme.{u} ↦ IsReduced Y)) :
    ∃ (M : BigFppfOver B S hS) (k : Type u) (_ : Field k),
      Nonempty ((BigFppfOver.toScheme B S hS).obj M ≅ Spec (.of k)) ∧
        Nonempty (X ≅ yoneda.obj M)

Tag 049D, a remark

Tag 049D in the Stacks Project.

AlgebraicGeometry.IsAlgebraicSpace.isRepresentable_of_isRepresentable_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeOfSchemeReduction.lean, line 167.

An algebraic space over S whose reduction is a scheme is a scheme.

theorem isRepresentable_of_isRepresentable_reduction {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hred : (reduction B S hS X hX).toFunctor.IsRepresentable) :
    X.IsRepresentable

Declarations registered for the tag:

AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_reduction, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SchemeOfIntegralBijection.lean, line 363 (StacksFrontier): “an algebraic space whose reduction is a scheme is a scheme, granted the same three hypotheses h09YA, h07SQ and hFinitePresentation that the Stacks 07VU attribute of this declaration records.”.

Tag 07U5, a lemma

Tag 07U5 in the Stacks Project.

AlgebraicGeometry.Space.isClosed_singleton_class_of_isAlgebraic_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ClosedPoints.lean, line 278. The attribute's comment: “with decency read as condition (alpha) of Stacks 03JX”.

Let X be an algebraic space over a scheme S above every point of which every étale chart of X by an affine scheme has a finite fibre, which is condition (α) of Stacks 03JX — in particular a decent one. Let p be a field-valued point of X with field of definition k, so a commutative diagram Spec k ⟶ X ⟶ S. If the image point s of Spec k ⟶ S is a closed point of S and the residue field extension κ(s) ⟶ k is algebraic, then the image of Spec k ⟶ X is a closed point of |X|.

theorem isClosed_singleton_class_of_isAlgebraic_residueField
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hdecent : HasFiniteChartFibersAtEveryPoint B S hS X)
    (p : FieldValuedPoint B S hS X)
    (hclosed : IsClosed ({(S.SpecToEquivOfField p.carrier p.toBase).1} : Set S))
    (halg : letI := (S.SpecToEquivOfField p.carrier p.toBase).2.hom.toAlgebra
      Algebra.IsAlgebraic
        (S.residueField (S.SpecToEquivOfField p.carrier p.toBase).1) p.carrier) :
    IsClosed ({p.class B S hS X} : Set (points B S hS X))

Tag 08AL, a lemma

Tag 08AL in the Stacks Project.

AlgebraicGeometry.Space.isFinite_fieldMorphism_of_moduleFinite_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FiniteFieldValuedPoint.lean, line 313. The attribute's comment: “finite morphism”.

Stacks 08AL, the finite case. Let X be a decent algebraic space over a scheme S and let p be a field-valued point of X with field of definition k, so a commutative diagram Spec k ⟶ X ⟶ S. If the image point s of Spec k ⟶ S is a closed point of S and k is finite over the residue field κ(s), then Spec k ⟶ X is a finite morphism.

theorem isFinite_fieldMorphism_of_moduleFinite_residueField (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) (p : FieldValuedPoint B S hS X)
    (hs : IsClosed ({(S.SpecToEquivOfField p.carrier p.toBase).1} : Set S))
    (hfin : letI := (S.SpecToEquivOfField p.carrier p.toBase).2.hom.toAlgebra
      Module.Finite (S.residueField (S.SpecToEquivOfField p.carrier p.toBase).1) p.carrier) :
    IsFinite B S hS (fieldMorphism B S hS X p)

AlgebraicGeometry.Space.isClosedImmersion_fieldMorphism_of_isIso_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FiniteFieldValuedPoint.lean, line 341. The attribute's comment: “closed immersion”.

Stacks 08AL, the closed-immersion case. Let X be a decent algebraic space over a scheme S and let p be a field-valued point of X with field of definition k, so a commutative diagram Spec k ⟶ X ⟶ S. If the image point s of Spec k ⟶ S is a closed point of S and the residue field embedding κ(s) ⟶ k is an isomorphism, then Spec k ⟶ X is a closed immersion.

theorem isClosedImmersion_fieldMorphism_of_isIso_residueField (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) (p : FieldValuedPoint B S hS X)
    (hs : IsClosed ({(S.SpecToEquivOfField p.carrier p.toBase).1} : Set S))
    (hrat : IsIso (S.SpecToEquivOfField p.carrier p.toBase).2) :
    IsClosedImmersion B S hS (fieldMorphism B S hS X p)

Tag 0AHB, a lemma

Tag 0AHB in the Stacks Project.

AlgebraicGeometry.Space.exists_fieldValuedPoint_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ClosedPoints.lean, line 504.

A closed point of a decent algebraic space X over a scheme S is represented by a closed immersion from the spectrum of a field: there is a field-valued point of X whose class is the given point and whose presenting morphism Spec k ⟶ X is a closed immersion.

theorem exists_fieldValuedPoint_isClosedImmersion
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hdec : IsDecentSpace B S hS X) (x : points B S hS X)
    (hx : IsClosed ({x} : Set (points B S hS X))) :
    ∃ p : FieldValuedPoint B S hS X,
      p.class B S hS X = x ∧ IsClosedImmersion B S hS (fieldMorphism B S hS X p)

Sources

LeanAlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_isLocallyNoetherian_of_isDecentSpace · AlgebraicGeometry.Space.isRepresentable_of_subsingleton_points · AlgebraicGeometry.Space.exists_iso_yoneda_spec_of_subsingleton_points · AlgebraicGeometry.IsAlgebraicSpace.isRepresentable_of_isRepresentable_reduction · AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_reduction · AlgebraicGeometry.Space.isClosed_singleton_class_of_isAlgebraic_residueField · AlgebraicGeometry.Space.isFinite_fieldMorphism_of_moduleFinite_residueField · AlgebraicGeometry.Space.isClosedImmersion_fieldMorphism_of_isIso_residueField

Section68.15 Locally separated spaces #

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

Tag 088I, a lemma

Tag 088I in the Stacks Project.

AlgebraicGeometry.Space.Decent.closure_iUnion_range_residuePairMap_meets_diagonal, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/InfiniteResidueFields.lean, line 225.

The closure of the union of the off-diagonal products of residue-field spectra meets the diagonal in Spec(A ⊗ℤ A).

lemma closure_iUnion_range_residuePairMap_meets_diagonal (_hp : Function.Injective p) :
    (closure (⋃ n, ⋃ m, ⋃ (_ : n ≠ m),
        range (PrimeSpectrum.comap (residuePairMap A k p n m))) ∩
      range (PrimeSpectrum.comap (diagonalMap A))).Nonempty

Tag 088J, a lemma

Tag 088J in the Stacks Project.

AlgebraicGeometry.Space.isDecentSpace_of_isAbsolutelyLocallySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocallySeparated.lean, line 1018.

Stacks 088J. A locally separated algebraic space is decent.

theorem isDecentSpace_of_isAbsolutelyLocallySeparated (hZ : B.Contains (⊤_ Scheme.{u}))
    (hX : IsAlgebraicSpace B S hS X) (hsep : IsAbsolutelyLocallySeparated B S hS hZ X) :
    IsDecentSpace B S hS X

Sources

LeanAlgebraicGeometry.Space.Decent.closure_iUnion_range_residuePairMap_meets_diagonal · AlgebraicGeometry.Space.isDecentSpace_of_isAbsolutelyLocallySeparated

Section68.16 Valuative criterion #

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

Tag 03KJ, a proposition

Tag 03KJ in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_iff_valuativeCriterion_existence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/UniversallyClosedValuative.lean, line 374.

Stacks 03KJ. A quasi-compact morphism of algebraic spaces over S whose source is a decent algebraic space is universally closed exactly when it satisfies the existence part of the valuative criterion.

theorem universallyClosed_iff_valuativeCriterion_existence
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsQuasiCompact B S hS f)
    (hdecent : IsDecentSpace B S hS X) :
    UniversallyClosed B S hS f ↔ ValuativeCriterion.Existence f

Sources

LeanAlgebraicGeometry.Space.universallyClosed_iff_valuativeCriterion_existence

Section68.17 Relative conditions #

Section 68.17 of the Stacks Project, Tag 03KW. 11 tags here are carried by 37 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03KZ, a definition

Tag 03KZ in the Stacks Project.

AlgebraicGeometry.Space.HasFiniteRelationFibersAtEveryPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent.lean, line 104. The attribute's comment: “property beta for an algebraic space”.

Stacks 03KZ, property (β) for an algebraic space. This is property (β) of Stacks 03JX: every point of F satisfies the equivalent conditions of Stacks 03JU, taken here in the form of condition (1), finiteness of one relation fibre in some étale chart.

abbrev HasFiniteRelationFibersAtEveryPoint : Prop

AlgebraicGeometry.Space.HasPropertyBeta, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent.lean, line 149. The attribute's comment: “property beta for a morphism”.

Stacks 03KZ, property (β) for a morphism. A morphism of algebraic spaces over S has property (β) when every base change of it along a morphism from a representable presheaf into its target has property (β).

abbrev HasPropertyBeta (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsDecent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent.lean, line 157. The attribute's comment: “decent morphism”.

Stacks 03KZ, decent morphism. A morphism of algebraic spaces over S is decent when every base change of it along a morphism from a representable presheaf into its target is a decent algebraic space.

abbrev IsDecent (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsReasonable, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Reasonable.lean, line 180. The attribute's comment: “reasonable morphism”.

Stacks 03KZ, reasonable morphism. A morphism of algebraic spaces over S is reasonable when every base change of it along a morphism from a representable presheaf into its target is a reasonable algebraic space.

abbrev IsReasonable (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsVeryReasonable, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Reasonable.lean, line 188. The attribute's comment: “very reasonable morphism”.

Stacks 03KZ, very reasonable morphism. A morphism of algebraic spaces over S is very reasonable when every base change of it along a morphism from a representable presheaf into its target is a very reasonable algebraic space.

abbrev IsVeryReasonable (f : X ⟶ Y) : Prop

Tag 03M5, a lemma

Tag 03M5 in the Stacks Project.

AlgebraicGeometry.Space.isVeryReasonable_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/QuasiSeparatedVeryReasonable.lean, line 84. The attribute's comment: “quasi-separated implies very reasonable”.

A quasi-separated morphism of algebraic spaces over S is very reasonable.

theorem isVeryReasonable_of_isQuasiSeparated (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y} (hf : IsQuasiSeparated B S hS f) :
    IsVeryReasonable B S hS f

AlgebraicGeometry.Space.isVeryReasonable_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditionComparisons.lean, line 91. The attribute's comment: “representable implies very reasonable”.

Stacks 03M5, representable implies very reasonable. A representable morphism of algebraic spaces over S is very reasonable: each of its represented base changes is again a representable algebraic space, hence Zariski locally quasi-separated by the implication (θ) ⇒ (ζ) of Stacks 03JX and very reasonable by (ζ) ⇒ (ε).

theorem isVeryReasonable_of_relativelyRepresentable (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f) : IsVeryReasonable B S hS f

AlgebraicGeometry.Space.isDecent_of_isReasonable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditionComparisons.lean, line 108. The attribute's comment: “reasonable implies decent”.

Stacks 03M5, reasonable implies decent. A reasonable morphism of algebraic spaces over S is decent: each of its represented base changes is a reasonable algebraic space, hence satisfies property (γ) of Stacks 03JX by the implication (δ) ⇒ (γ), which is decency.

theorem isDecent_of_isReasonable (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsReasonable B S hS f) :
    IsDecent B S hS f

AlgebraicGeometry.Space.hasPropertyBeta_of_isDecent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditionComparisons.lean, line 120. The attribute's comment: “decent implies property (beta)”.

Stacks 03M5, decent implies property (β). A decent morphism of algebraic spaces over S has property (β): each of its represented base changes is a decent algebraic space, hence satisfies property (β) of Stacks 03JX by the implication (γ) ⇒ (β).

theorem hasPropertyBeta_of_isDecent (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsDecent B S hS f) :
    HasPropertyBeta B S hS f

AlgebraicGeometry.Space.isReasonable_of_isVeryReasonable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/VeryReasonableImpliesReasonable.lean, line 221. The attribute's comment: “very reasonable implies reasonable”.

Stacks 03M5, very reasonable implies reasonable. A very reasonable morphism of algebraic spaces over S is reasonable.

Both conditions of Stacks 03KZ are conditions on the represented base changes of the morphism, each of which is an algebraic space, so this is the implication AlgebraicGeometry.Space.isReasonableSpace_of_isVeryReasonableSpace applied base change by base change.

theorem isReasonable_of_isVeryReasonable {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (h : IsVeryReasonable B S hS f) : IsReasonable B S hS f

Tag 0ABX, a lemma

Tag 0ABX in the Stacks Project.

AlgebraicGeometry.Space.isDecent_of_isDecentSpace_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FieldFibreTopologicalDimension.lean, line 99. The attribute's comment: “decent: a morphism whose source is decent is decent”.

Stacks 0ABX, the decent case. A morphism of algebraic spaces over S whose source is a decent algebraic space is a decent morphism.

A morphism g : h_T ⟶ Y out of a representable presheaf into an algebraic space is representable, because the diagonal of Y is; hence so is the projection T ×_Y X ⟶ X of its base change, and decency passes from the target of a representable morphism to its source by Stacks 0ABT.

theorem isDecent_of_isDecentSpace_source (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hdec : IsDecentSpace B S hS X) :
    IsDecent B S hS f

AlgebraicGeometry.Space.hasMonomorphicFieldRepresentative_pullback_of_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditions.lean, line 330. The attribute's comment: “decent, as condition (4) of Stacks 03JU at every represented base change”.

Stacks 0ABX, the decent case in the form of condition (4) of Stacks 03JU. Let f : X ⟶ Y be a morphism of presheaves on the big fppf site over S with Y an algebraic space. If every point of X is the class of a field-valued point presenting it by a monomorphism, then so is every point of every base change of f along a morphism from a representable presheaf into Y: that base change is representable over X.

theorem hasMonomorphicFieldRepresentative_pullback_of_source
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hmono : ∀ x : points B S hS X, HasMonomorphicFieldRepresentative B S hS X x)
    (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y)
    (w : points B S hS (pullback g f)) :
    HasMonomorphicFieldRepresentative B S hS (pullback g f) w

AlgebraicGeometry.Space.hasPropertyBeta_of_hasMonomorphicFieldRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditions.lean, line 343. The attribute's comment: “property beta, from condition (4) of Stacks 03JU on the source”.

Stacks 0ABX, the case (β). Let f : X ⟶ Y be a morphism of algebraic spaces over S. If every point of X is the class of a field-valued point presenting it by a monomorphism — condition (4) of Stacks 03JU — then f has property (β) of Stacks 03JX.

theorem hasPropertyBeta_of_hasMonomorphicFieldRepresentative
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hmono : ∀ x : points B S hS X, HasMonomorphicFieldRepresentative B S hS X x) :
    HasPropertyBeta B S hS f

AlgebraicGeometry.Space.hasPropertyBeta_of_hasFiniteRelationFibersAtEveryPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditions.lean, line 370. The attribute's comment: “property beta”.

Stacks 0ABX, the case (β). A morphism of algebraic spaces over S whose source has property (β) of Stacks 03JX has property (β).

Property (β) of the source is condition (1) of Stacks 03JU at each of its points, which the equivalences of that lemma turn into condition (4).

theorem hasPropertyBeta_of_hasFiniteRelationFibersAtEveryPoint
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hXβ : HasFiniteRelationFibersAtEveryPoint B S hS X) :
    HasPropertyBeta B S hS f

AlgebraicGeometry.Space.isReasonable_of_isReasonableSpace_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditions.lean, line 384. The attribute's comment: “reasonable”.

Stacks 0ABX, the reasonable case. A morphism of algebraic spaces over S whose source is a reasonable algebraic space is a reasonable morphism.

Each base change of f along a morphism from a representable presheaf into Y projects to X by a representable morphism, because the diagonal of Y is representable, and reasonableness passes to the source of a representable morphism by Stacks 0ABT.

theorem isReasonable_of_isReasonableSpace_source (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hXr : IsReasonableSpace B S hS X) :
    IsReasonable B S hS f

Tag 03L0, a lemma

Tag 03L0 in the Stacks Project.

AlgebraicGeometry.Space.hasPropertyBeta_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditions.lean, line 277. The attribute's comment: “property beta”.

Stacks 03L0, property (β). Property (β) of a morphism of algebraic spaces over S is preserved by arbitrary base change: a base change of the base change of f : X ⟶ Y along g : Y' ⟶ Y is a base change of f.

theorem hasPropertyBeta_baseChange (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : HasPropertyBeta B S hS f) : HasPropertyBeta B S hS (pullback.fst g f)

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

Stacks 03L0, decent. Decency of a morphism of algebraic spaces over S is preserved by arbitrary base change: a base change of the base change of f : X ⟶ Y along g : Y' ⟶ Y is a base change of f.

theorem isDecent_baseChange (f : X ⟶ Y) (g : Y' ⟶ Y) (hf : IsDecent B S hS f) :
    IsDecent B S hS (pullback.fst g f)

AlgebraicGeometry.Space.isReasonable_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditions.lean, line 294. The attribute's comment: “reasonable”.

Stacks 03L0, reasonable. Reasonableness of a morphism of algebraic spaces over S is preserved by arbitrary base change: a base change of the base change of f : X ⟶ Y along g : Y' ⟶ Y is a base change of f.

theorem isReasonable_baseChange (f : X ⟶ Y) (g : Y' ⟶ Y) (hf : IsReasonable B S hS f) :
    IsReasonable B S hS (pullback.fst g f)

Tag 0ABY, a lemma

Tag 0ABY in the Stacks Project.

AlgebraicGeometry.Space.hasMonomorphicFieldRepresentative_of_target_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditions.lean, line 404. The attribute's comment: “property beta, as condition (4) of Stacks 03JU at every point”.

Stacks 0ABY, the case (β) in the form of condition (4) of Stacks 03JU. Let f : X ⟶ Y be a morphism of presheaves on the big fppf site over S. If every point of Y is the class of a field-valued point presenting it by a monomorphism, and if the same holds at every point of every base change of f along a morphism from a representable presheaf into Y, then it holds at every point of X.

This is the source's argument: a monomorphic representative Spec k ⟶ Y of the image of x is a morphism out of a representable presheaf, the point x lifts to the base change Spec k ×_Y X by Stacks 03H4, and a monomorphic representative there composes with the projection — a monomorphism, being a base change of one — to a monomorphic representative of x.

theorem hasMonomorphicFieldRepresentative_of_target_of_baseChange (f : X ⟶ Y)
    (hY : ∀ y : points B S hS Y, HasMonomorphicFieldRepresentative B S hS Y y)
    (hf : ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y)
      (w : points B S hS (pullback g f)),
      HasMonomorphicFieldRepresentative B S hS (pullback g f) w)
    (x : points B S hS X) :
    HasMonomorphicFieldRepresentative B S hS X x

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

Stacks 0ABY, decent. If a morphism of algebraic spaces over S is decent and its target is decent, then its source is decent.

A point x of the source maps to a point of the target, which decency of the target presents by a quasi-compact monomorphism g : Spec k ⟶ Y. The point x and the tautological point of Spec k have the same image in Y, so they come from a point of Spec k ×_Y X; that fibre product is decent because the morphism is, so that point is presented by a quasi-compact monomorphism, and composing it with the projection to X — a base change of g, hence again a quasi-compact monomorphism — presents x.

theorem isDecentSpace_of_isDecent (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hYdecent : IsDecentSpace B S hS Y) (hfdecent : IsDecent B S hS f) :
    IsDecentSpace B S hS X

AlgebraicGeometry.Space.isReasonableSpace_of_isReasonable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeReasonablePermanence.lean, line 250. The attribute's comment: “reasonable”.

Stacks 0ABY, reasonable. If a morphism of algebraic spaces over S is reasonable and its target is reasonable, then its source is reasonable.

A jointly surjective family of étale charts with universally bounded fibres for the target, Stacks 03JT, pulls back to a family of fibre products over the source, each of which is a reasonable algebraic space because the morphism is reasonable; a family of charts for each of those, composed with the projections to the source, is again jointly surjective and étale, and the fibres of the composites remain universally bounded.

theorem isReasonableSpace_of_isReasonable (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hYr : IsReasonableSpace B S hS Y)
    (hf : IsReasonable B S hS f) :
    IsReasonableSpace B S hS X

Tag 03L1, a lemma

Tag 03L1 in the Stacks Project.

AlgebraicGeometry.Space.hasPropertyBeta_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditions.lean, line 466. The attribute's comment: “property beta”.

Stacks 03L1, property (β). Property (β) of a morphism of algebraic spaces over S is preserved by composition.

The base change of f ≫ g along k : T ⟶ Z is the base change of f along the projection T ×_Z Y ⟶ Y, viewed over T ×_Z Y; that projection has property (β) by Stacks 03L0 and T ×_Z Y has it because g does, so Stacks 0ABY applies.

theorem hasPropertyBeta_comp (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : HasPropertyBeta B S hS f) (hg : HasPropertyBeta B S hS g) :
    HasPropertyBeta B S hS (f ≫ g)

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

Stacks 03L1, decent. Decency of a morphism of algebraic spaces over S is preserved by composition.

The base change of f ≫ g along k : T ⟶ Z is the base change of f along the projection T ×_Z Y ⟶ Y, viewed over T ×_Z Y; that projection is decent by Stacks 03L0 and T ×_Z Y is decent because g is, so Stacks 0ABY applies.

theorem isDecent_comp (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsDecent B S hS f) (hg : IsDecent B S hS g) :
    IsDecent B S hS (f ≫ g)

AlgebraicGeometry.Space.isReasonable_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeReasonablePermanence.lean, line 349. The attribute's comment: “reasonable”.

Stacks 03L1, reasonable. Reasonableness of a morphism of algebraic spaces over S is preserved by composition.

The base change of f ≫ g along k : T ⟶ Z is the base change of f along the projection T ×_Z Y ⟶ Y, viewed over T ×_Z Y; that projection is reasonable by Stacks 03L0 and T ×_Z Y is reasonable because g is, so Stacks 0ABY applies.

theorem isReasonable_comp (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsReasonable B S hS f) (hg : IsReasonable B S hS g) :
    IsReasonable B S hS (f ≫ g)

Tag 0ABZ, a lemma

Tag 0ABZ in the Stacks Project.

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

Stacks 0ABZ, decent. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of algebraic spaces over S. If X and Z are decent algebraic spaces, then so is X ×_Y Z.

Decency of X makes f a decent morphism by Stacks 0ABX, its base change Z ×_Y X ⟶ Z is decent by Stacks 03L0, and decency of Z together with that of the base change gives decency of Z ×_Y X by Stacks 0ABY.

theorem isDecentSpace_pullback (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Z ⟶ Y)
    (hXdec : IsDecentSpace B S hS X) (hZdec : IsDecentSpace B S hS Z) :
    IsDecentSpace B S hS (pullback f g)

AlgebraicGeometry.Space.isReasonableSpace_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FibreProductConditions.lean, line 116. The attribute's comment: “reasonable”.

Stacks 0ABZ, reasonable. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of algebraic spaces over S. If X and Z are reasonable algebraic spaces, then so is X ×_Y Z.

Reasonableness of X makes f a reasonable morphism by Stacks 0ABX, its base change Z ×_Y X ⟶ Z is reasonable by Stacks 03L0, and reasonableness of Z together with that of the base change gives reasonableness of Z ×_Y X by Stacks 0ABY.

theorem isReasonableSpace_pullback (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Z ⟶ Y)
    (hXr : IsReasonableSpace B S hS X) (hZr : IsReasonableSpace B S hS Z) :
    IsReasonableSpace B S hS (pullback f g)

AlgebraicGeometry.Space.hasFiniteRelationFibersAtEveryPoint_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FibreProductConditions.lean, line 133. The attribute's comment: “property beta”.

Stacks 0ABZ, property (β). Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of algebraic spaces over S. If X and Z have property (β) of Stacks 03JX, then so does X ×_Y Z.

Property (β) of X makes f a morphism with property (β) by Stacks 0ABX, its base change Z ×_Y X ⟶ Z has property (β) by Stacks 03L0, and property (β) of Z together with that of the base change gives property (β) of Z ×_Y X by Stacks 0ABY.

theorem hasFiniteRelationFibersAtEveryPoint_pullback (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Z ⟶ Y)
    (hXβ : HasFiniteRelationFibersAtEveryPoint B S hS X)
    (hZβ : HasFiniteRelationFibersAtEveryPoint B S hS Z) :
    HasFiniteRelationFibersAtEveryPoint B S hS (pullback f g)

Tag 03L2, a lemma

Tag 03L2 in the Stacks Project.

AlgebraicGeometry.Space.hasFiniteRelationFibersAtEveryPoint_of_surjective_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/PropertyBetaDescent.lean, line 70. The attribute's comment: “property (beta)”.

Stacks 03L2, property (β). Let f : X ⟶ Y be a quasi-compact étale morphism of algebraic spaces over S which is surjective on points. If X has property (β) of Stacks 03JX — every point has a field-valued representative with a finite relation fibre — then so does Y.

theorem hasFiniteRelationFibersAtEveryPoint_of_surjective_isEtale
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hq : IsQuasiCompact B S hS f)
    (he : IsEtale B S hS f) (hs : Function.Surjective (pointsMap B S hS X f))
    (hβ : HasFiniteRelationFibersAtEveryPoint B S hS X) :
    HasFiniteRelationFibersAtEveryPoint B S hS Y

AlgebraicGeometry.Space.isReasonableSpace_of_surjective_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ReasonableEtaleDescent.lean, line 96. The attribute's comment: “reasonable”.

Stacks 03L2, reasonable. Let f be a quasi-compact morphism of algebraic spaces over S which is surjective on points. If its source is reasonable, then so is its target.

An affine étale chart of the target is dominated, after base change along f, by an affine étale chart of the source, and the bound reasonableness of the source gives the latter bounds the degrees of the fibres of the former. Étaleness of f, which Stacks 03L2 also assumes, is not used.

theorem isReasonableSpace_of_surjective_isQuasiCompact
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsQuasiCompact B S hS f)
    (hsurj : Function.Surjective (pointsMap B S hS X f))
    (hXr : IsReasonableSpace B S hS X) :
    IsReasonableSpace B S hS Y

AlgebraicGeometry.Space.hasQuasiCompactFieldRepresentative_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeDecency.lean, line 151. The attribute's comment: “condition (5) of Stacks 03JV at every point of the target”.

Stacks 03L2, condition (5) of Stacks 03JV at every point of the target. Let f be a quasi-compact morphism of algebraic spaces over S which is surjective on points. If the source is decent, then every point of the target has a quasi-compact field-valued representative.

A point of the target is the image of a point of the source, which decency of the source presents by a quasi-compact morphism from the spectrum of a field; composing it with f again gives a quasi-compact morphism, and it presents the chosen point of the target.

Decency of the target asks for a representative which is in addition a monomorphism, and obtaining one from this is the equivalence of conditions (4) and (5) of Stacks 03JV. Étaleness of f, which Stacks 03L2 also assumes, is not used.

theorem hasQuasiCompactFieldRepresentative_of_isDecentSpace (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsQuasiCompact B S hS f)
    (hsurj : Function.Surjective (pointsMap B S hS X f))
    (hXdecent : IsDecentSpace B S hS X) (y : points B S hS Y) :
    HasQuasiCompactFieldRepresentative B S hS Y y

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

Stacks 03L2, decent. Let f be a quasi-compact morphism of algebraic spaces over S which is surjective on points. If its source is decent, then so is its target.

Every point of the target acquires a quasi-compact field-valued representative by pushing one forward along f, and the implication from condition (5) to condition (4) of Stacks 03JV makes that representative a monomorphism. Étaleness of f, which Stacks 03L2 also assumes, is not used.

theorem isDecentSpace_of_surjective_isQuasiCompact (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsQuasiCompact B S hS f)
    (hsurj : Function.Surjective (pointsMap B S hS X f))
    (hXdecent : IsDecentSpace B S hS X) :
    IsDecentSpace B S hS Y

Tag 03L3, a lemma

Tag 03L3 in the Stacks Project.

AlgebraicGeometry.Space.hasPropertyBeta_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeLocalCriteria.lean, line 603. The attribute's comment: “property beta”.

For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: (1) f has property (β) in the sense of Stacks 03KZ; (2) for every affine object Z of the site and every Z ⟶ Y, the base change Z ×_Y X ⟶ Z has property (β); (3) for every such Z ⟶ Y the algebraic space Z ×_Y X has property (β); (4) there is a Zariski covering of Y by open subspaces Yᵢ with every restriction Yᵢ ×_Y X ⟶ Yᵢ having property (β); (5) there is a scheme of the site with a surjective étale morphism V ⟶ Y such that V ×_Y X ⟶ V has property (β).

theorem hasPropertyBeta_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE
      [HasPropertyBeta B S hS f,
        ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
            HasPropertyBeta B S hS (pullback.fst g f),
        ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
            HasFiniteRelationFibersAtEveryPoint B S hS (pullback g f),
        ∃ (I : Type u) (Yᵢ : I → Subfunctor Y), IsZariskiCover B S hS I Yᵢ ∧
          ∀ i, HasPropertyBeta B S hS (pullback.fst (Yᵢ i).ι f),
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y), IsSurjective B S hS g ∧
          IsEtale B S hS g ∧ HasPropertyBeta B S hS (pullback.fst g f)]

AlgebraicGeometry.Space.isVeryReasonable_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeLocalCriteria.lean, line 630. The attribute's comment: “very reasonable”.

For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: (1) f is very reasonable in the sense of Stacks 03KZ; (2) for every affine object Z of the site and every Z ⟶ Y, the base change Z ×_Y X ⟶ Z is very reasonable; (3) for every such Z ⟶ Y the algebraic space Z ×_Y X is very reasonable; (4) there is a Zariski covering of Y by open subspaces Yᵢ with every restriction Yᵢ ×_Y X ⟶ Yᵢ very reasonable.

theorem isVeryReasonable_tfae (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [IsVeryReasonable B S hS f,
        ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
            IsVeryReasonable B S hS (pullback.fst g f),
        ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
            IsVeryReasonableSpace B S hS (pullback g f),
        ∃ (I : Type u) (Yᵢ : I → Subfunctor Y), IsZariskiCover B S hS I Yᵢ ∧
          ∀ i, IsVeryReasonable B S hS (pullback.fst (Yᵢ i).ι f)]

AlgebraicGeometry.Space.isDecent_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeLocalCriteria.lean, line 652. The attribute's comment: “decent, conditions (1) to (4)”.

For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: (1) f is decent in the sense of Stacks 03KZ; (2) for every affine object Z of the site and every Z ⟶ Y, the base change Z ×_Y X ⟶ Z is decent; (3) for every such Z ⟶ Y the algebraic space Z ×_Y X is decent; (4) there is a Zariski covering of Y by open subspaces Yᵢ with every restriction Yᵢ ×_Y X ⟶ Yᵢ decent.

theorem isDecent_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE
      [IsDecent B S hS f,
        ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
            IsDecent B S hS (pullback.fst g f),
        ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
            IsDecentSpace B S hS (pullback g f),
        ∃ (I : Type u) (Yᵢ : I → Subfunctor Y), IsZariskiCover B S hS I Yᵢ ∧
          ∀ i, IsDecent B S hS (pullback.fst (Yᵢ i).ι f)]

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

For a morphism f : X ⟶ Y of algebraic spaces over S the four conditions of AlgebraicGeometry.Space.isDecent_tfae are also equivalent to (5) there is a scheme of the site with a surjective étale morphism V ⟶ Y such that V ×_Y X ⟶ V is decent.

theorem isDecent_tfae_etale (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [IsDecent B S hS f,
        ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
            IsDecent B S hS (pullback.fst g f),
        ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
            IsDecentSpace B S hS (pullback g f),
        ∃ (I : Type u) (Yᵢ : I → Subfunctor Y), IsZariskiCover B S hS I Yᵢ ∧
          ∀ i, IsDecent B S hS (pullback.fst (Yᵢ i).ι f),
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y), IsSurjective B S hS g ∧
          IsEtale B S hS g ∧ IsDecent B S hS (pullback.fst g f)]

AlgebraicGeometry.Space.isReasonable_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeLocalCriteria.lean, line 700. The attribute's comment: “reasonable”.

For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: (1) f is reasonable in the sense of Stacks 03KZ; (2) for every affine object Z of the site and every Z ⟶ Y, the base change Z ×_Y X ⟶ Z is reasonable; (3) for every such Z ⟶ Y the algebraic space Z ×_Y X is reasonable; (4) there is a Zariski covering of Y by open subspaces Yᵢ with every restriction Yᵢ ×_Y X ⟶ Yᵢ reasonable; (5) there is a scheme of the site with a surjective étale morphism V ⟶ Y such that V ×_Y X ⟶ V is reasonable.

theorem isReasonable_tfae (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [IsReasonable B S hS f,
        ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
            IsReasonable B S hS (pullback.fst g f),
        ∀ (T : BigFppfOver B S hS) (g : yoneda.obj T ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
            IsReasonableSpace B S hS (pullback g f),
        ∃ (I : Type u) (Yᵢ : I → Subfunctor Y), IsZariskiCover B S hS I Yᵢ ∧
          ∀ i, IsReasonable B S hS (pullback.fst (Yᵢ i).ι f),
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y), IsSurjective B S hS g ∧
          IsEtale B S hS g ∧ IsReasonable B S hS (pullback.fst g f)]

Tag 03L4, a remark

Tag 03L4 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.isDecent_of_isReasonable, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeConditionComparisons.lean, line 139 (StacksFrontier): “Remark 68.17.10, which states no proposition of its own: its comparative sentence, that being reasonable is a bit stronger than being decent, is sharp only as the implication reasonable ⇒ decent of Stacks 03M5, which is this theorem.”.
AlgebraicGeometry.Space.hasPropertyBeta_tfae, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeLocalCriteria.lean, line 728 (StacksFrontier): “Remark 68.17.10, which states no proposition of its own: its one mathematical sentence, that a morphism has one of the conditions of Stacks 03KZ when, in the source's words '(very) loosely speaking', the fibres of the morphism do, is disclaimed there as loose and is sharp only as Stacks 03L3 — here the case of property (β).”.
AlgebraicGeometry.Space.isVeryReasonable_tfae, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeLocalCriteria.lean, line 734 (StacksFrontier): “Remark 68.17.10, which states no proposition of its own: its one mathematical sentence, that a morphism has one of the conditions of Stacks 03KZ when, in the source's words '(very) loosely speaking', the fibres of the morphism do, is disclaimed there as loose and is sharp only as Stacks 03L3 — here the case of very reasonableness.”.
AlgebraicGeometry.Space.isDecent_tfae_etale, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeLocalCriteria.lean, line 740 (StacksFrontier): “Remark 68.17.10, which states no proposition of its own: its one mathematical sentence, that a morphism has one of the conditions of Stacks 03KZ when, in the source's words '(very) loosely speaking', the fibres of the morphism do, is disclaimed there as loose and is sharp only as Stacks 03L3 — here the case of decency.”.
AlgebraicGeometry.Space.isReasonable_tfae, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RelativeLocalCriteria.lean, line 746 (StacksFrontier): “Remark 68.17.10, which states no proposition of its own: its one mathematical sentence, that a morphism has one of the conditions of Stacks 03KZ when, in the source's words '(very) loosely speaking', the fibres of the morphism do, is disclaimed there as loose and is sharp only as Stacks 03L3 — here the case of reasonableness.”.

Tag 03M6, a lemma

Tag 03M6 in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_iff_valuativeCriterion_existence_of_isDecent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/UniversallyClosedValuative.lean, line 393.

Stacks 03M6. A quasi-compact morphism of algebraic spaces over S which is decent as a morphism is universally closed exactly when it satisfies the existence part of the valuative criterion.

A valuative square for f has its bottom edge Spec R ⟶ Y, so it is a valuative square for the base change X ×_Y Spec R ⟶ Spec R, which is quasi-compact and has decent source; that base change is universally closed, hence satisfies the existence part by Stacks 03KJ, and a dominating extension solving the square there solves the original one after composing the lift with the projection to X.

theorem universallyClosed_iff_valuativeCriterion_existence_of_isDecent
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsQuasiCompact B S hS f)
    (hdecent : IsDecent B S hS f) :
    UniversallyClosed B S hS f ↔ ValuativeCriterion.Existence f

Sources

LeanAlgebraicGeometry.Space.HasFiniteRelationFibersAtEveryPoint · AlgebraicGeometry.Space.HasPropertyBeta · AlgebraicGeometry.Space.IsDecent · AlgebraicGeometry.Space.IsReasonable · AlgebraicGeometry.Space.IsVeryReasonable · AlgebraicGeometry.Space.isVeryReasonable_of_isQuasiSeparated · AlgebraicGeometry.Space.isVeryReasonable_of_relativelyRepresentable · AlgebraicGeometry.Space.isDecent_of_isReasonable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

68.3 Universally bounded fibres to 68.17 Relative conditions

Section68.3 Universally bounded fibres#

Tag 03JL, a definition

Tag 03JM, a lemma

Tag 03JN, a lemma

Tag 03JO, a lemma

Tag 03JP, a lemma

Tag 03JQ, a lemma

Sources

Section68.4 Finiteness conditions and points#

Tag 03II, a remark

Tag 03JS, a lemma

Tag 03JU, a lemma

Tag 040U, a lemma

Tag 03JV, a lemma

Tag 03JT, a lemma

Tag 03IH, a lemma

Sources

Section68.5 Conditions on algebraic spaces#

Tag 03JX, a lemma

Tag 03KE, a lemma

Tag 03KF, a lemma

Sources

Section68.6 Reasonable and decent algebraic spaces#

Tag 03I8, a definition

Tag 03ID, an example

Tag 03K0, a lemma

Tag 0ABT, a lemma

Tag 0ABU, a lemma

Sources

Section68.7 Points and specializations#

Tag 03IM, a lemma

Tag 0H1Q, a lemma

Tag 03K2, a lemma

Tag 0B7W, a lemma

Sources

Section68.8 Stratifying algebraic spaces by schemes#

Tag 07S8, a lemma

Tag 086T, a lemma

Tag 0BBN, a lemma

Tag 07S9, a lemma

Tag 07SA, a lemma

Tag 07ST, a lemma

Tag 0ECZ, a lemma

Sources

Section68.9 Integral cover by a scheme#

Tag 0G2D, a lemma

Tag 09YB, a lemma

Tag 0GUL, a lemma

Sources

Section68.10 Schematic locus#

Tag 03JI, a proposition

Tag 086U, a theorem

Tag 0BA1, a lemma

Tag 06NG, a lemma

Sources

Section68.11 Residue fields and henselian local rings#

Tag 03K4, a lemma

Tag 0EMW, a definition

Tag 0EMX, a lemma

Tag 0BBP, a lemma

Tag 0BGU, a definition

Tag 0BGV, a lemma

Tag 0BGW, a definition

Tag 0EMY, a lemma

Tag 0EMZ, a lemma

Tag 0EN0, a lemma

Tag 0EPL, a remark

Sources

Section68.12 Points on decent spaces#

Tag 03K5, a lemma

Tag 03IL, a lemma

Tag 03K3, a lemma

Tag 03K6, a proposition

Tag 0A4J, a lemma

Tag 0ABW, a lemma

Tag 0ED0, a lemma

Tag 03IK, a lemma

Sources

Section68.13 Reduced singleton spaces#

Section68.3 Universally bounded fibres #

Section68.4 Finiteness conditions and points #

Section68.5 Conditions on algebraic spaces #

Section68.6 Reasonable and decent algebraic spaces #

Section68.7 Points and specializations #

Section68.8 Stratifying algebraic spaces by schemes #

Section68.9 Integral cover by a scheme #

Section68.10 Schematic locus #

Section68.11 Residue fields and henselian local rings #

Section68.12 Points on decent spaces #

Section68.13 Reduced singleton spaces #

Section68.14 Decent spaces #

Section68.15 Locally separated spaces #

Section68.16 Valuative criterion #

Section68.17 Relative conditions #