107 The Geometry of Stacks

Chapter 107 of the Stacks Project, The Geometry of Stacks, Tag 0DQR: the 5 sections of its 6 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 47 tags are carried by 104 declarations of the repository (all in StacksFrontier) and 1 registered declaration.

Section107.2 Versal rings#

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

Tag 0DQU, a situation

Tag 0DQU in the Stacks Project.

AlgebraicGeometry.Stack.VersalSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalSituation.lean, line 58.

Stacks 0DQU. The versal situation: an algebraic stack locally of finite type over a locally Noetherian scheme.

structure VersalSituation

Tag 0DQV, a definition

Tag 0DQV in the Stacks Project.

AlgebraicGeometry.Stack.IsVersalRingAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRing/Basic.lean, line 69.

A complete Noetherian local algebra is a versal ring at a field-valued point if it is the base of a versal formal object in the point's predeformation category.

public abbrev IsVersalRingAt
    (D : AlgebraicGeometry.Stack.VersalSituation.{u, w})
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S)
    (_hiΛ : IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (_hfinite : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (A : Deformation.CompleteLocalAlgCat.{u, u, u} Λ k) : Prop

AlgebraicGeometry.Stack.isVersalRingAt_iff_of_affineOpenPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRing/ChartIndependence.lean, line 794. The attribute's comment: “independence of affine-open presentation”.

The notion of a versal ring is independent of which affine open neighborhood presents its structure morphism to S.

public theorem isVersalRingAt_iff_of_affineOpenPresentation
    (D : AlgebraicGeometry.Stack.VersalSituation.{u, w})
    {Λ Λ' k : Type u} [CommRing Λ] [CommRing Λ'] [Field k]
    [Algebra Λ k] [Algebra Λ' k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : IsOpenImmersion iΛ)
    (iΛ' : Spec (.of Λ') ⟶ D.S) (hiΛ' : IsOpenImmersion iΛ')
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hx₀' : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ'))
    (hfinite : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite' : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ') ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ'))
    (A : Deformation.CompleteLocalAlgCat.{u, u, u} Λ k)
    (A' : Deformation.CompleteLocalAlgCat.{u, u, u} Λ' k)
    (e : A ≃+* A')
    (heS : Spec.map (CommRingCat.ofHom e.toRingHom) ≫
        Spec.map (CommRingCat.ofHom (algebraMap Λ A)) ≫ iΛ =
      Spec.map (CommRingCat.ofHom (algebraMap Λ' A')) ≫ iΛ')
    (hek : ∀ a : A,
      A'.residueEquiv (residue A' (e a)) = A.residueEquiv (residue A a)) :
    IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite A ↔
      IsVersalRingAt D iΛ' hiΛ' x₀ hx₀' hfinite' A'

Tag 0DQW, a lemma

Tag 0DQW in the Stacks Project.

AlgebraicGeometry.Stack.isFiniteDimensionalDeformationCategory_of_versalSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalSituationFiniteDimensional.lean, line 44.

In Situation 0DQU, let x₀ be an object of 𝒳 over Spec k, for a field k of finite type over S, and let Spec Λ ⊆ S be an affine open through which Spec k ⟶ S factors with Λ → k finite. Then 𝓕_{𝒳,k,x₀} is a deformation category whose tangent space and space of infinitesimal automorphisms are finite-dimensional over k.

theorem isFiniteDimensionalDeformationCategory_of_versalSituation
    (D : VersalSituation.{u, w}) {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    [Module.Finite Λ k] (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    letI := (Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).category
    Deformation.IsFiniteDimensionalDeformationCategory
      (Deformation.Artin.predeformationCategory iΛ
        (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).projection

Tag 0DQX, a lemma

Tag 0DQX in the Stacks Project.

AlgebraicGeometry.Stack.versalRing_powerSeries_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRing/ComparisonAndExistence.lean, line 419. The attribute's comment: “the comparison of any two versal rings at x₀: A ≅ A'[[t₁,…,t_r]] or A' ≅ A[[t₁,…,t_r]]”.

Two versal rings at a field-valued point of an algebraic stack are isomorphic over the base after adjoining finitely many formal variables to one of them.

theorem versalRing_powerSeries_comparison
    (D : AlgebraicGeometry.Stack.VersalSituation.{u, w})
    {Λ Λ' k : Type u} [CommRing Λ] [CommRing Λ'] [Field k]
    [Algebra Λ k] [Algebra Λ' k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : IsOpenImmersion iΛ)
    (iΛ' : Spec (.of Λ') ⟶ D.S) (hiΛ' : IsOpenImmersion iΛ')
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hx₀' : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ'))
    (hfinite : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite' : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ') ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ'))
    (A : Deformation.CompleteLocalAlgCat.{u, u, u} Λ k)
    (A' : Deformation.CompleteLocalAlgCat.{u, u, u} Λ' k)
    (hA : AlgebraicGeometry.Stack.IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite A)
    (hA' : AlgebraicGeometry.Stack.IsVersalRingAt D iΛ' hiΛ' x₀ hx₀' hfinite' A') :
    (∃ r : ℕ, ∃ e : A ≃+* MvPowerSeries (Fin r) A',
      Spec.map (CommRingCat.ofHom e.toRingHom) ≫
        Spec.map (CommRingCat.ofHom (algebraMap Λ A)) ≫ iΛ =
      Spec.map (CommRingCat.ofHom
        (algebraMap Λ' (MvPowerSeries (Fin r) A'))) ≫ iΛ') ∨
    (∃ r : ℕ, ∃ e : A' ≃+* MvPowerSeries (Fin r) A,
      Spec.map (CommRingCat.ofHom e.toRingHom) ≫
        Spec.map (CommRingCat.ofHom (algebraMap Λ' A')) ≫ iΛ' =
      Spec.map (CommRingCat.ofHom
        (algebraMap Λ (MvPowerSeries (Fin r) A))) ≫ iΛ)

AlgebraicGeometry.Stack.exists_isVersalRingAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingExistence.lean, line 38. The attribute's comment: “existence of a versal ring to 𝒳 at x₀”.

Stacks 0DQX, first assertion. In Situation 0DQU, let x₀ be an object of 𝒳 over Spec k for a field k of finite type over S, and let Spec Λ ⊆ S be an affine open through which Spec k ⟶ S factors. Then a versal ring to 𝒳 at x₀ exists, presented over Λ.

theorem exists_isVersalRingAt
    (D : VersalSituation.{u, w}) {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    ∃ A : Deformation.CompleteLocalAlgCat.{u, u, u} Λ k,
      IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite A

Tag 0DQY, a lemma

Tag 0DQY in the Stacks Project.

AlgebraicGeometry.Stack.exists_isVersalRingAt_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingFieldExtension.lean, line 189.

Stacks 0DQY. In Situation 0DQU, let x₀ be an object of 𝒳 over Spec k for a field k of finite type over S, presented over an affine open Spec Λ ⊆ S, let l/k be a finite extension of fields, and let x_{l,0} be the induced point: an object xₗ over Spec l ⟶ Spec Λ ⟶ S with a morphism η : xₗ ⟶ x₀ over Spec l ⟶ Spec k. Given a versal ring A to 𝒳 at x₀ there are a versal ring A' to 𝒳 at x_{l,0} and an S-algebra map f : A → A' which is local, induces the given extension l/k on residue fields, and is formally smooth for the 𝔪_{A'}-adic topology.

theorem exists_isVersalRingAt_fieldExtension
    (D : VersalSituation.{u, w})
    {Λ k l : Type u} [CommRing Λ] [Field k] [Field l] [Algebra Λ k] [Algebra k l]
    [Algebra Λ l] [IsScalarTower Λ k l] [Module.Finite k l]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (xₗ : D.𝒳.val.val.obj)
    (hxₗ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj xₗ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ l)) ≫ iΛ))
    (η : xₗ ⟶ x₀)
    (hηbase : eqToHom (congrArg Over.left hxₗ).symm ≫
      ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).map η).left ≫
      eqToHom (congrArg Over.left hx₀) = Spec.map (CommRingCat.ofHom (algebraMap k l)))
    (A : Deformation.CompleteLocalAlgCat.{u, u, u} Λ k)
    (hA : IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite A) :
    ∃ (A' : Deformation.CompleteLocalAlgCat.{u, u, u} Λ l) (f : A →ₐ[Λ] A'),
      IsVersalRingAt D iΛ hiΛ xₗ hxₗ
          (locallyOfFiniteType_and_quasiCompact_fieldExtension iΛ hfinite) A' ∧
        IsLocalHom f.toRingHom ∧
        (∀ a : A, A'.residueEquiv (residue A' (f a)) =
          algebraMap k l (A.residueEquiv (residue A a))) ∧
        RingHom.FormallySmoothNAdic.{u} f.toRingHom (maximalIdeal A')

Tag 0DQZ, a lemma

Tag 0DQZ in the Stacks Project.

AlgebraicGeometry.Stack.isVersalAt_iff_exists_isRelativelySmooth_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalChartSmoothBaseChange.lean, line 885. The attribute's comment: “the equivalence of (1) and (4): x is versal at u₀ exactly when there is an open neighbourhood U' ⊆ U of u₀ such that x|_{U'} : U' → 𝒳 is smooth”.

Stacks 0DQZ, the equivalence of (1) and (4). In the versal situation, let x be an object of 𝒳 over a scheme U locally of finite type over S, and let u₀ ∈ U be a finite type point. Then x is versal at u₀ exactly when there is an open neighbourhood U' ⊆ U of u₀ such that x|_{U'} : U' → 𝒳 is smooth.

The open subscheme U' is read as an object of the site by AlgebraicGeometry.BigFppfOver.openSubObj, and x|_{U'} is the composite of its inclusion U' → U with the 1-morphism x : U → 𝒳 of the 2-Yoneda lemma; it is representable by algebraic spaces, and smooth is meant in the sense of Stacks 04XB.

The implication (4) ⟹ (1) is AlgebraicGeometry.Stack.isVersalAt_of_exists_isRelativelySmooth_restrict (Stacks 07WK, case (3), at the residue point of u₀ in U', and versality is unchanged by restriction to an open subscheme); (1) ⟹ (4) is AlgebraicGeometry.Stack.exists_isRelativelySmooth_restrict_of_isVersalAt (Stacks 0CXM along a smooth surjective presentation of 𝒳, Stacks 06EJ, and descent of smoothness along a smooth surjection).

theorem isVersalAt_iff_exists_isRelativelySmooth_restrict (D : VersalSituation.{u, w})
    (x : D.𝒳.val.val.obj)
    [LocallyOfFiniteType ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).hom]
    (u₀ : ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).left)
    (hu₀ : AlgebraicGeometry.IsFiniteTypePoint u₀) :
    Deformation.Artin.IsVersalAt ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x)
        (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) u₀ x rfl ↔
      ∃ V : (D.𝒳.val.val.p.obj x).left.obj.Opens, u₀ ∈ V ∧
        IsRelativelySmooth D.B D.S D.hS
          (schemeFibredCategoryMap D.B D.S D.hS
              (BigFppfOver.openSubHom D.B D.S D.hS (D.𝒳.val.val.p.obj x) V) ≫
            objectMorphism D.B D.S D.hS D.𝒳.val (Functor.Fiber.mk (a := x) rfl))

AlgebraicGeometry.Stack.isVersalAt_iff_isVersal_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingChartPoint.lean, line 171. The attribute's comment: “the equivalence of (1) and (3): x is versal at u₀ exactly when the formal object associated to the restriction of x to Spec 𝒪^∧_{U,u₀} is versal”.

Stacks 0DQZ, the equivalence of (1) and (3). In the versal situation, let x be an object of 𝒳 over a scheme U locally of finite type over S, let u₀ be a point of U whose image in S lies in the affine open Spec Λ, and let ξ be the formal object the approximation functor attaches to a Cartesian restriction of x over a presentation of 𝒪^∧_{U, u₀}. Then x is versal at u₀ exactly when ξ is versal.

This is Artin's Axioms, Stacks 0CXK, read in the versal situation of Stacks 0DQU, with the deformation base on the ring of an affine open of S rather than on a local ring of S.

theorem isVersalAt_iff_isVersal_completion
    (t : Spec (.of Λ)) (ht : iΛ t = Deformation.Artin.basePoint U u₀)
    [Algebra Λ (U.left.residueField u₀)]
    (hcompat : Spec.map (CommRingCat.ofHom (algebraMap Λ (U.left.residueField u₀))) ≫ iΛ =
      U.left.fromSpecResidueField u₀ ≫ U.hom) :
    Deformation.Artin.IsVersalAt U (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) u₀ x hx ↔
      Deformation.Artin.FormalObject.IsVersal D.B D.S D.hS D.𝒳.val.val.p D.𝒳.val.property
        ξ Λ iΛ hΛ

AlgebraicGeometry.Stack.isVersalRingAt_completeLocalBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingChartPoint.lean, line 237. The attribute's comment: “the final statement: the completion 𝒪^∧_{U,u₀} is a versal ring to 𝒳 at the point x₀ induced by u₀”.

Stacks 0DQZ, the final statement. In the versal situation, if x is versal at the finite type point u₀, then the completion 𝒪^∧_{U, u₀} — presented by the complete local base of the formal object ξ attached to the restriction of x over it — is a versal ring to 𝒳 at the closed fibre x₀ of ξ.

The first conjunct identifies the point: the closed fibre ξ.level 0, over which the versal ring is exhibited, is the restriction of x along the residue point of u₀, hence the point x₀ of the lemma's preamble. The second is the conclusion, and its proof is the one of the source: the equivalence of (1) and (3) turns versality of x at u₀ into versality of ξ, and versality of a formal object is by definition versality of the formal object of the predeformation category of its closed fibre that it determines, which is exactly what Stacks 0DQV asks of a versal ring.

theorem isVersalRingAt_completeLocalBase
    (t : Spec (.of Λ)) (ht : iΛ t = Deformation.Artin.basePoint U u₀)
    [Algebra Λ (U.left.residueField u₀)]
    (hcompat : Spec.map (CommRingCat.ofHom (algebraMap Λ (U.left.residueField u₀))) ≫ iΛ =
      U.left.fromSpecResidueField u₀ ≫ U.hom)
    (hversal : Deformation.Artin.IsVersalAt U
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) u₀ x hx) :
    Deformation.Artin.schemeMap (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion)
          (ξ.basePoint Λ iΛ hΛ) hx
          (Deformation.Artin.approximationLevelToOriginal D.B D.S D.hS D.𝒳.val.val.p
            D.𝒳.val.property xR ξ hξ r 0) =
        Spec.map (CommRingCat.ofHom (residue ξ.base.R)) ≫ g ∧
      IsVersalRingAt D iΛ hiΛ (ξ.level 0) (ξ.basePoint Λ iΛ hΛ)
        (locallyOfFiniteType_and_quasiCompact_residueField_formalBase D ξ Λ iΛ hΛ)
        (ξ.completeLocalBase Λ)

AlgebraicGeometry.Stack.isVersalAt_iff_isSmooth_hatX, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingChartPoint.lean, line 303. The attribute's comment: “the equivalence of (1) and (2): x is versal at u₀ exactly when x̂ : 𝓕_{U,k,u₀} ⟶ 𝓕_{𝒳,k,x₀} is smooth”.

Stacks 0DQZ, the equivalence of (1) and (2). In the versal situation, let x be an object of 𝒳 over a scheme U, let u₀ ∈ U with residue field k = κ(u₀), and let Spec Λ ⊆ S be an affine open through which Spec k ⟶ S factors. Then x is versal at u₀ exactly when the map of predeformation categories over 𝒞_Λ x̂ : 𝓕_{U, k, u₀} ⟶ 𝓕_{𝒳, k, x₀} induced by the 2-Yoneda morphism x : (Sch/U)_{fppf} ⟶ 𝒳 (for any choice c of pullbacks) at the residue point of u₀ is smooth.

The source records this as "the definition of x being versal at u₀"; in this library Deformation.Artin.IsVersalAt is the lifting property spelled out over the local ring of S, so the equivalence is Deformation.Artin.isVersalAt_iff_isSmooth_mapPredeformationCategory. Neither local finite type of U nor the finite type of u₀ is needed.

theorem isVersalAt_iff_isSmooth_hatX (t : Spec (.of Λ))
    (ht : iΛ t = Deformation.Artin.basePoint
      ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x) u₀) :
    Deformation.Artin.IsVersalAt ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x)
        (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) u₀ x rfl ↔
      Deformation.IsSmooth
        (Deformation.Artin.mapPredeformationCategory iΛ
          (Over.forget (D.𝒳.val.val.p.obj x) ⋙ Over.post D.B.inclusion)
          (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion)
          (c.sliceFunctor (⟨x, rfl⟩ : D.𝒳.val.val.p.Fiber (D.𝒳.val.val.p.obj x)))
          (Deformation.Artin.sliceFunctor_comp_post D.B D.S D.hS D.𝒳.val.val.p c x)
          (chartResiduePoint D x u₀) (chartResiduePoint_base D x u₀ iΛ hcompat)).toBasedFunctor

Tag 0DZS, a lemma

Tag 0DZS in the Stacks Project.

AlgebraicGeometry.Stack.IsSmoothLocus.property_iff_isFormallySmoothAtClosedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingSmoothLocus.lean, line 352. The attribute's comment: “the equivalence of (1) and (2): x₀ is in the smooth locus of 𝒳 → S iff 𝒪_{S,s} → A is formally smooth in the 𝔪_A-adic topology”.

Stacks 0DZS, the equivalence of (1) and (2). In Situation 0DQU — 𝒳 an algebraic stack locally of finite type over a locally Noetherian scheme S — let x₀ : Spec k ⟶ 𝒳 be a point with Spec k ⟶ S of finite type, presented over an affine open Spec Λ ⊆ S, with image s, and let A be a versal ring to 𝒳 at x₀. Then x₀ lies in the smooth locus W of 𝒳 ⟶ S (Stacks 0DZR) if and only if 𝒪_{S, s} ⟶ A is formally smooth for the 𝔪_A-adic topology.

The proof is the source's: condition (2) does not depend on the versal ring (Stacks 0DQX) and is unchanged by finite extensions of the residue field (Stacks 0DQY), so it may be tested at a point of a smooth chart U ⟶ 𝒳, where the versal ring is 𝒪^∧_{U, u₀} (Stacks 0DQZ); there membership in the smooth locus of 𝒳 ⟶ S is membership of u₀ in the smooth locus of U ⟶ S (Stacks 0DZR), which is formal smoothness of 𝒪_{S, s} ⟶ 𝒪^∧_{U, u₀} (Stacks 07VH).

theorem IsSmoothLocus.property_iff_isFormallySmoothAtClosedPoint
    {W : OpenSubstack D.𝒳}
    (hW : IsSmoothLocus D.B D.S D.hS (structureMorphism D.B D.S D.hS D.𝒳) W)
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (A : Deformation.CompleteLocalAlgCat.{u, u, u} Λ k)
    (hA : IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite A) :
    W.property x₀ ↔
      IsFormallySmoothAtClosedPoint (Spec.map (CommRingCat.ofHom (algebraMap Λ A)) ≫ iΛ)

AlgebraicGeometry.Stack.isFormallySmoothAtClosedPoint_iff_isSmooth_baseProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingSmoothLocus.lean, line 423. The attribute's comment: “the equivalence of (2) and (3): 𝒪_{S,s} → A is formally smooth in the 𝔪_A-adic topology iff the predeformation category of x₀ is unobstructed”. References: SGA 7 VI (1.14), “special case”.

Stacks 0DZS, the equivalence of (2) and (3). In Situation 0DQU let x₀ : Spec k ⟶ 𝒳 be a point with Spec k ⟶ S of finite type, presented over an affine open Spec Λ ⊆ S with Λ → k finite (the presentation of Artin's Axioms, Section 07T2, on which the predeformation category 𝓕_{𝒳, k, x₀} is built), and let A be a versal ring to 𝒳 at x₀. Then 𝒪_{S, s} ⟶ A is formally smooth for the 𝔪_A-adic topology if and only if 𝓕_{𝒳, k, x₀} is unobstructed, that is its structure functor to 𝒞_Λ is smooth. This is Formal Deformation Theory, Lemma 0DZK, together with the observation that 𝒪_{S, s} is a localization of Λ.

theorem isFormallySmoothAtClosedPoint_iff_isSmooth_baseProjection
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (A : Deformation.CompleteLocalAlgCat.{u, u, u} Λ k)
    (hA : IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite A) :
    IsFormallySmoothAtClosedPoint (Spec.map (CommRingCat.ofHom (algebraMap Λ A)) ≫ iΛ) ↔
      let C := Deformation.Artin.predeformationCategory iΛ
        (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀
      letI : Category C.carrier := C.category
      Deformation.IsSmooth (Deformation.baseProjection C.projection)

AlgebraicGeometry.Stack.tfae_smoothLocus_formallySmooth_unobstructed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingSmoothLocus.lean, line 471.

Stacks 0DZS. In Situation 0DQU let x₀ : Spec k ⟶ 𝒳 be a point with Spec k ⟶ S of finite type, presented over an affine open Spec Λ ⊆ S with Λ → k finite, with image s ∈ S, and let A be a versal ring to 𝒳 at x₀. The following are equivalent:

1. x₀ is in the smooth locus of 𝒳 ⟶ S (Stacks 0DZR);
2. 𝒪_{S, s} ⟶ A is formally smooth in the 𝔪_A-adic topology;
3. 𝓕_{𝒳, k, x₀} is unobstructed.

theorem tfae_smoothLocus_formallySmooth_unobstructed
    {W : OpenSubstack D.𝒳}
    (hW : IsSmoothLocus D.B D.S D.hS (structureMorphism D.B D.S D.hS D.𝒳) W)
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (A : Deformation.CompleteLocalAlgCat.{u, u, u} Λ k)
    (hA : IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite A) :
    List.TFAE [W.property x₀,
      IsFormallySmoothAtClosedPoint (Spec.map (CommRingCat.ofHom (algebraMap Λ A)) ≫ iΛ),
      let C := Deformation.Artin.predeformationCategory iΛ
        (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀
      letI : Category C.carrier := C.category
      Deformation.IsSmooth (Deformation.baseProjection C.projection)]

Tag 0DR0, a lemma

Tag 0DR0 in the Stacks Project.

AlgebraicGeometry.Stack.exists_smoothObject_completedLocalRing_equiv_versalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingArtinApproximation.lean, line 814.

Stacks 0DR0. In the versal situation, let x₀ be a point of 𝒳 over Spec k ⟶ Spec Λ ⟶ S, for an affine open Spec Λ ⊆ S and a field k with Spec k ⟶ S of finite type and image s, and let A be a versal ring to 𝒳 at x₀ (Stacks 0DQV). If 𝒪_{S,s} is a G-ring, there are a smooth object x of 𝒳 (a smooth morphism U ⟶ 𝒳 from a scheme U, here moreover locally of finite type over S) and a point u₀ ∈ U with residue field k, through e : k ≅ κ(u₀), such that 1. Spec k ⟶ U ⟶ 𝒳 is x₀: there is an arrow x₀ ⟶ x of 𝒳 lying over Spec k ≅ Spec κ(u₀) ⟶ U (a 2-isomorphism of 1-morphisms out of Spec k); 2. there is an isomorphism 𝒪^∧_{U, u₀} ≅ A.

The proof is the source's: the versal formal object is effective (Stacks 07X8), so AlgebraicGeometry.Stack.exists_smoothObject_completedLocalRing_realization (Artin approximation, Stacks 07XH, with Stacks 0DQJ, Stacks 0CMY and Stacks 0DQZ) applies to a realization of it.

theorem exists_smoothObject_completedLocalRing_equiv_versalRing (D : VersalSituation.{u, w})
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (A : Deformation.CompleteLocalAlgCat.{u, u, u} Λ k)
    (hA : IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite A)
    (s : D.S) (hs : (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) (closedPoint k) = s)
    (hG : IsGRing (D.S.presheaf.stalk s)) :
    ∃ (x : D.𝒳.val.val.obj) (u₀ : ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).left)
      (e : k ≃+* ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).left.residueField u₀)
      (a : x₀ ⟶ x)
      (_ : ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).left.completedLocalRing u₀ ≃+* A),
      LocallyOfFiniteType ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).hom ∧
      smoothObject.{u, w} D.B D.S D.hS D.𝒳 x ∧
      Deformation.Artin.schemeMap (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) hx₀ rfl a =
        Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫
          ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).left.fromSpecResidueField u₀

Tag 0DR1, a remark

Tag 0DR1 in the Stacks Project.

AlgebraicGeometry.Stack.exists_smoothObject_completedLocalRing_realization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingArtinApproximation.lean, line 717. The attribute's comment: “part (4): in Lemma 0DR0 the isomorphism 𝒪^∧_{U,u₀} ≅ A may be chosen so that Spec(A) → 𝒳 corresponds to the canonical map Spec(𝒪^∧_{U,u₀}) → U → 𝒳 of part (3)”.

Stacks 0DR1, part (4): Artin approximation compatible with the morphism Spec A ⟶ 𝒳. In the versal situation, let x₀ be a point of 𝒳 over Spec k ⟶ Spec Λ ⟶ S, for an affine open Spec Λ ⊆ S and a field k of finite type over S, with image s ∈ S such that 𝒪_{S,s} is a G-ring; let ξ be a versal formal object of the predeformation category of x₀, with base the versal ring A, and let y be an object of 𝒳 over Spec A ⟶ S realizing ξ (the morphism Spec A ⟶ 𝒳 of the remark). Then the data of Stacks 0DR0 may be chosen compatibly with y: there are a smooth object x of 𝒳 over a scheme U locally of finite type over S, a point u₀ ∈ U with an identification e : k ≅ κ(u₀), an arrow x₀ ⟶ x of 𝒳 over Spec k ≅ Spec κ(u₀) ⟶ U (so Spec k ⟶ U ⟶ 𝒳 is x₀), an isomorphism eA : 𝒪^∧_{U, u₀} ≅ A, and an arrow y ⟶ x of 𝒳 over Spec A ≅ Spec 𝒪^∧_{U, u₀} ⟶ U: the morphism Spec A ⟶ 𝒳 is, through eA, the canonical Spec 𝒪^∧_{U, u₀} ⟶ U ⟶ 𝒳 of part (3). As the remark says, the triangles commute up to a 2-arrow, which is what an arrow of 𝒳 over a morphism of schemes is.

This is Artin approximation, Stacks 07XH, at the formal object over the site of ξ, which is effective because it is realized and versal over 𝒪_{S,s} by Deformation.Artin.isVersal_stalk_ofPredeformation_of_realization; the structure morphism of 𝒳 is limit preserving by Stacks 0DQJ and Stacks 0CMY. The chart Artin approximation produces is versal at u₀, hence smooth after shrinking by Stacks 0DQZ, (1) ⟹ (4). The arrow y ⟶ x is the preimage, under the fully faithful approximation functor (Stacks 07X8), of the isomorphism of formal objects that Artin approximation produces, followed by the restriction arrow of the chart to the completion.

theorem exists_smoothObject_completedLocalRing_realization (D : VersalSituation.{u, w})
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (ξ : Deformation.FormalObject (Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).projection)
    (hξ : Deformation.IsVersal (Deformation.Artin.predeformationCategory_isPredeformationCategory
      D.B D.hS iΛ D.𝒳.val.val.p x₀ hx₀ D.𝒳.val.property).cofibered ξ)
    (s : D.S) (hs : (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) (closedPoint k) = s)
    (hG : IsGRing (D.S.presheaf.stalk s))
    {hA : D.B.Contains (Spec (.of ξ.base))} {y : D.𝒳.val.val.obj}
    {hy : D.𝒳.val.val.p.obj y = Deformation.Artin.baseOver D.B D.S D.hS
      (Deformation.Artin.completeLocalAlgFormalBase iΛ hfinite ξ.base) hA}
    (Ry : (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p x₀ hx₀
      hfinite ξ).Realization hA y hy) :
    ∃ (x : D.𝒳.val.val.obj) (u₀ : ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).left)
      (e : k ≃+* ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).left.residueField u₀)
      (a : x₀ ⟶ x)
      (eA : ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).left.completedLocalRing u₀ ≃+*
        ξ.base),
      LocallyOfFiniteType ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).hom ∧
      smoothObject.{u, w} D.B D.S D.hS D.𝒳 x ∧
      Deformation.Artin.schemeMap (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) hx₀ rfl a =
        Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫
          ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).left.fromSpecResidueField u₀ ∧
      ∃ m : y ⟶ x, Deformation.Artin.schemeMap (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion)
          (congrArg (Over.post D.B.inclusion).obj hy) rfl m =
        Spec.map (CommRingCat.ofHom eA.toRingHom) ≫
          ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x).left.fromSpecCompletedLocalRing u₀

AlgebraicGeometry.Stack.exists_realization_of_predeformationFormalObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingArtinApproximation.lean, line 777. The attribute's comment: “preamble: the versal formal object over A comes from a morphism Spec(A) → 𝒳 over S (Artin's Axioms, Lemma 07X8)”.

Stacks 0DR1, the preamble: the versal formal object comes from a morphism Spec A ⟶ 𝒳. In the versal situation, let x₀ be a point of 𝒳 over Spec k ⟶ Spec Λ ⟶ S, for an affine open Spec Λ ⊆ S and a field k of finite type over S, and let ξ be a formal object of the predeformation category of x₀ with base A — in the remark, the versal formal object over a versal ring A, though versality is not needed. Then ξ comes from a morphism Spec A ⟶ 𝒳 over S: there is an object y of 𝒳 over Spec A ⟶ Spec Λ ⟶ S whose restrictions to the infinitesimal thickenings of the closed point are the levels of ξ, compatibly with the transitions (a Deformation.Artin.FormalObject.Realization); y names the 1-morphism Spec A ⟶ 𝒳 under the 2-Yoneda lemma.

This is effectivity of formal objects of an algebraic stack, the essential surjectivity half of Stacks 07X8 (Deformation.Artin.FormalObject.isEffective_of_isAlgebraicStack), read over the base of ξ itself by Deformation.Artin.FormalObject.exists_realization_of_isEffective.

theorem exists_realization_of_predeformationFormalObject (D : VersalSituation.{u, w})
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (ξ : Deformation.FormalObject (Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).projection) :
    ∃ (y : D.𝒳.val.val.obj)
      (hy : D.𝒳.val.val.p.obj y = Deformation.Artin.baseOver D.B D.S D.hS
        (Deformation.Artin.completeLocalAlgFormalBase iΛ hfinite ξ.base)
        (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p x₀ hx₀
          hfinite ξ).contains_spec_base),
      Nonempty ((Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p
        x₀ hx₀ hfinite ξ).Realization
          (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p x₀ hx₀
            hfinite ξ).contains_spec_base y hy)

AlgebraicGeometry.Stack.exists_isVersalRingAt_fieldExtension_realization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingFieldExtensionRealization.lean, line 573. The attribute's comment: “part (2): in Lemma 0DQY the homomorphism A → A' may be chosen compatible with the morphisms Spec A → 𝒳, Spec A' → 𝒳”.

Stacks 0DR1, part (2). In the versal situation of Stacks 0DQU, let x₀ be a point of 𝒳 over Spec k for a field k of finite type over S, presented over an affine open Spec Λ ⊆ S, let l/k be a finite extension of fields and x_{l,0} the induced point (an object xₗ over Spec l with a morphism η : xₗ ⟶ x₀ over Spec l ⟶ Spec k). Let A be a versal ring to 𝒳 at x₀, with versal formal object ξ, coming from a morphism Spec A ⟶ 𝒳 over S: an object y of 𝒳 over Spec A realizing ξ. Then the homomorphism of Stacks 0DQY may be chosen compatible with the morphisms Spec A ⟶ 𝒳 and Spec A' ⟶ 𝒳: there are a versal ring A' to 𝒳 at x_{l,0}, with versal formal object ξₗ, and an S-algebra map f : A → A' which is local, induces l/k on residue fields and is formally smooth for the 𝔪_{A'}-adic topology, such that

• when Spec A' belongs to the site, ξₗ comes from a morphism Spec A' ⟶ 𝒳 (an object over Spec A' realizing ξₗ), and
• every object y' over Spec A' realizing ξₗ has a morphism y' ⟶ y of 𝒳 lying over Spec f : Spec A' ⟶ Spec A.

The morphism y' ⟶ y is the 2-arrow making the square Spec A' ⟶ Spec A ⟶ 𝒳 2-commute, which is how the source's "compatible" is to be read (the remark notes that the diagrams commute only up to a noncanonical 2-arrow). As in the source, the proof is that the maps of Stacks 0DQF and 07WX are compatible with the versal formal objects: the formal object of 𝓕_{l/k} produced by Stacks 0DQF is the pushforward of ξ along f (Deformation.exists_versal_formalObject_changeOfFields_pushforward), and its image under the restriction functor of Stacks 07WX maps to ξ over the site over Spec f; fullness of the approximation functor (Stacks 07X8, Deformation.Artin.full_approximationFunctor_algebraicStacks) turns that morphism of formal objects into a morphism of the realizing objects.

theorem exists_isVersalRingAt_fieldExtension_realization
    {Λ k l : Type u} [CommRing Λ] [Field k] [Field l] [Algebra Λ k] [Algebra k l]
    [Algebra Λ l] [IsScalarTower Λ k l] [Module.Finite k l]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (xₗ : D.𝒳.val.val.obj)
    (hxₗ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj xₗ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ l)) ≫ iΛ))
    (η : xₗ ⟶ x₀)
    (hηbase : eqToHom (congrArg Over.left hxₗ).symm ≫
      ((D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).map η).left ≫
      eqToHom (congrArg Over.left hx₀) = Spec.map (CommRingCat.ofHom (algebraMap k l)))
    (ξ : Deformation.FormalObject (Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).projection)
    (hξ : Deformation.IsVersal (Deformation.Artin.predeformationCategory_isPredeformationCategory
      D.B D.hS iΛ D.𝒳.val.val.p x₀ hx₀ D.𝒳.val.property).cofibered ξ)
    {hA : D.B.Contains (Spec (.of ξ.base))} {y : D.𝒳.val.val.obj}
    {hy : D.𝒳.val.val.p.obj y = Deformation.Artin.baseOver D.B D.S D.hS
      (Deformation.Artin.completeLocalAlgFormalBase iΛ hfinite ξ.base) hA}
    (Ry : (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p x₀ hx₀
      hfinite ξ).Realization hA y hy) :
    ∃ (ξₗ : Deformation.FormalObject (Deformation.Artin.predeformationCategory iΛ
        (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) xₗ hxₗ).projection)
      (f : ξ.base →ₐ[Λ] ξₗ.base),
      Deformation.IsVersal (Deformation.Artin.predeformationCategory_isPredeformationCategory
        D.B D.hS iΛ D.𝒳.val.val.p xₗ hxₗ D.𝒳.val.property).cofibered ξₗ ∧
      IsLocalHom f.toRingHom ∧
      (∀ a : ξ.base, ξₗ.base.residueEquiv (residue ξₗ.base (f a)) =
        algebraMap k l (ξ.base.residueEquiv (residue ξ.base a))) ∧
      RingHom.FormallySmoothNAdic.{u} f.toRingHom (maximalIdeal ξₗ.base) ∧
      (∀ hA' : D.B.Contains (Spec (.of ξₗ.base)), ∃ (y' : D.𝒳.val.val.obj)
        (hy' : D.𝒳.val.val.p.obj y' = Deformation.Artin.baseOver D.B D.S D.hS
          (Deformation.Artin.completeLocalAlgFormalBase iΛ
            (locallyOfFiniteType_and_quasiCompact_fieldExtension iΛ hfinite) ξₗ.base) hA'),
        Nonempty ((Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ
          D.𝒳.val.val.p xₗ hxₗ (locallyOfFiniteType_and_quasiCompact_fieldExtension iΛ hfinite)
            ξₗ).Realization hA' y' hy')) ∧
      ∀ {hA' : D.B.Contains (Spec (.of ξₗ.base))} {y' : D.𝒳.val.val.obj}
        {hy' : D.𝒳.val.val.p.obj y' = Deformation.Artin.baseOver D.B D.S D.hS
          (Deformation.Artin.completeLocalAlgFormalBase iΛ
            (locallyOfFiniteType_and_quasiCompact_fieldExtension iΛ hfinite) ξₗ.base) hA'},
        (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p xₗ hxₗ
          (locallyOfFiniteType_and_quasiCompact_fieldExtension iΛ hfinite) ξₗ).Realization
            hA' y' hy' →
        ∃ m : y' ⟶ y, (BigFppfOver.toScheme D.B D.S D.hS).map
            (eqToHom hy'.symm ≫ D.𝒳.val.val.p.map m ≫ eqToHom hy) =
          Spec.map (CommRingCat.ofHom f.toRingHom)

AlgebraicGeometry.Stack.isEffective_and_objectMorphism_completion_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingFlatMorphism.lean, line 197. The attribute's comment: “the morphism Spec(A) ⟶ 𝒳 of the remark at the versal ring A = 𝒪^∧_{U,u₀} of Stacks 0DQZ, and clause (3): that morphism is the composition of the canonical map Spec(𝒪^∧_{U,u₀}) ⟶ U with the given map U ⟶ 𝒳”.

Stacks 0DR1 at the versal ring of Stacks 0DQZ, and its clause (3). In the versal situation, let x be an object of 𝒳 over a scheme U locally of finite type over S, let u₀ be a point of U, and let xR be a complete local object restricting x over the canonical morphism Spec(𝒪^∧_{U, u₀}) ⟶ U. Then the formal object ξ the approximation functor of Stacks 07X6 attaches to xR is effective, so the versal formal object of Stacks 0DQZ comes from a morphism Spec(𝒪^∧_{U, u₀}) ⟶ 𝒳 — the 1-morphism xR names under the 2-Yoneda lemma — and that morphism is the composition of the canonical map Spec(𝒪^∧_{U, u₀}) ⟶ U with the given map U ⟶ 𝒳.

The three conclusions are the three halves of the statement: effectivity, which is the preamble of the remark; the identification of the morphism of the site that r lies over with the canonical morphism AlgebraicGeometry.Scheme.fromSpecCompletedLocalRing of the completion, read through the presentation e; and the 2-isomorphism of 1-morphisms, which is the 2-Yoneda functoriality AlgebraicGeometry.Stack.objectMorphismFactorIso of Stacks 004B at r. As the remark notes, the diagram only 2-commutes, after a choice of 2-arrow, which is why the third conclusion is a Nonempty of isomorphisms rather than an equality.

theorem isEffective_and_objectMorphism_completion_factors
    (ξ : Deformation.Artin.FormalObject D.B D.S D.hS D.𝒳.val.val.p)
    (hξ : ξ = (Deformation.Artin.approximationFunctor D.B D.S D.hS D.𝒳.val.val.p
      D.𝒳.val.property).obj xR) :
    Deformation.Artin.FormalObject.IsEffective D.B D.S D.hS D.𝒳.val.val.p
        D.𝒳.val.property ξ ∧
      ((eqToHom (Deformation.Artin.chosenBase_eq D.B D.S D.hS
            D.𝒳.val.val.p xR.obj).symm ≫ D.𝒳.val.val.p.map r).left.hom ≫
          eqToHom (congrArg Over.left hx)) =
        Spec.map (CommRingCat.ofHom e.toRingHom) ≫
          U.left.fromSpecCompletedLocalRing u₀ ∧
      Nonempty (objectMorphism D.B D.S D.hS D.𝒳.val
          (Functor.Fiber.mk (a := xR.obj.1) rfl) ≅
        schemeFibredCategoryMap D.B D.S D.hS (D.𝒳.val.val.p.map r) ≫
          objectMorphism D.B D.S D.hS D.𝒳.val (Functor.Fiber.mk (a := x) rfl))

AlgebraicGeometry.Stack.exists_powerSeries_comparison_realization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingMorphism.lean, line 419. The attribute's comment: “part (1): in Lemma 0DQX the isomorphism A ≅ A'[[t₁,…,t_r]] or A' ≅ A[[t₁,…,t_r]] may be chosen compatible with the morphisms Spec A → 𝒳, Spec A' → 𝒳”.

Stacks 0DR1, part (1). In the versal situation, let x₀ be a point of 𝒳 over Spec k for a field k of finite type over S, and let A, A' be versal rings to 𝒳 at x₀ (presented over affine opens Spec Λ, Spec Λ' of S), with versal formal objects ξ, ξ' coming from morphisms Spec A ⟶ 𝒳 and Spec A' ⟶ 𝒳 over S: objects y, y' of 𝒳 over Spec A, Spec A' realizing ξ, ξ'. Then the isomorphism of Stacks 0DQX may be chosen compatible with these morphisms: either there are r and an isomorphism e : A ≅ A'[[t₁, …, t_r]] over S together with a morphism y ⟶ y' of 𝒳 lying over Spec A ≅ Spec A'[[t₁, …, t_r]] ⟶ Spec A', or the same with A and A' exchanged. The morphism y ⟶ y' is the 2-arrow making the triangle Spec A ⟶ Spec A' ⟶ 𝒳 2-commute, which is how the source's "compatible" is to be read (the remark notes that the diagrams commute only up to a noncanonical 2-arrow).

Fullness of the approximation functor, the input from Stacks 07X8, is Deformation.Artin.full_approximationFunctor_algebraicStacks.

theorem exists_powerSeries_comparison_realization
    {Λ Λ' k : Type u} [CommRing Λ] [CommRing Λ'] [Field k]
    [Algebra Λ k] [Algebra Λ' k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : IsOpenImmersion iΛ)
    (iΛ' : Spec (.of Λ') ⟶ D.S) (hiΛ' : IsOpenImmersion iΛ')
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hx₀' : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ'))
    (hfinite : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite' : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ') ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ'))
    (ξ : Deformation.FormalObject (Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).projection)
    (hξ : Deformation.IsVersal (Deformation.Artin.predeformationCategory_isPredeformationCategory
      D.B D.hS iΛ D.𝒳.val.val.p x₀ hx₀ D.𝒳.val.property).cofibered ξ)
    (ξ' : Deformation.FormalObject (Deformation.Artin.predeformationCategory iΛ'
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀').projection)
    (hξ' : Deformation.IsVersal (Deformation.Artin.predeformationCategory_isPredeformationCategory
      D.B D.hS iΛ' D.𝒳.val.val.p x₀ hx₀' D.𝒳.val.property).cofibered ξ')
    {hA : D.B.Contains (Spec (.of ξ.base))} {hA' : D.B.Contains (Spec (.of ξ'.base))}
    {y y' : D.𝒳.val.val.obj}
    {hy : D.𝒳.val.val.p.obj y = Deformation.Artin.baseOver D.B D.S D.hS
      (Deformation.Artin.completeLocalAlgFormalBase iΛ hfinite ξ.base) hA}
    {hy' : D.𝒳.val.val.p.obj y' = Deformation.Artin.baseOver D.B D.S D.hS
      (Deformation.Artin.completeLocalAlgFormalBase iΛ' hfinite' ξ'.base) hA'}
    (Ry : (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p x₀ hx₀
      hfinite ξ).Realization hA y hy)
    (Ry' : (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ' D.𝒳.val.val.p x₀
      hx₀' hfinite' ξ').Realization hA' y' hy') :
    (∃ r : ℕ, ∃ e : (ξ.base : Type u) ≃+* MvPowerSeries (Fin r) ξ'.base,
      Spec.map (CommRingCat.ofHom e.toRingHom) ≫
          Spec.map (CommRingCat.ofHom (algebraMap Λ ξ.base)) ≫ iΛ =
        Spec.map (CommRingCat.ofHom (algebraMap Λ' (MvPowerSeries (Fin r) ξ'.base))) ≫ iΛ' ∧
      ∃ m : y ⟶ y', (BigFppfOver.toScheme D.B D.S D.hS).map
          (eqToHom hy.symm ≫ D.𝒳.val.val.p.map m ≫ eqToHom hy') =
        Spec.map (CommRingCat.ofHom (e.symm.toRingHom.comp MvPowerSeries.C))) ∨
    (∃ r : ℕ, ∃ e : (ξ'.base : Type u) ≃+* MvPowerSeries (Fin r) ξ.base,
      Spec.map (CommRingCat.ofHom e.toRingHom) ≫
          Spec.map (CommRingCat.ofHom (algebraMap Λ' ξ'.base)) ≫ iΛ' =
        Spec.map (CommRingCat.ofHom (algebraMap Λ (MvPowerSeries (Fin r) ξ.base))) ≫ iΛ ∧
      ∃ m : y' ⟶ y, (BigFppfOver.toScheme D.B D.S D.hS).map
          (eqToHom hy'.symm ≫ D.𝒳.val.val.p.map m ≫ eqToHom hy) =
        Spec.map (CommRingCat.ofHom (e.symm.toRingHom.comp MvPowerSeries.C)))

AlgebraicGeometry.Stack.formallyHomotopic_of_realization_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingMorphismHomotopy.lean, line 541. The attribute's comment: “closing claim: the map in (1) is well defined up to formal homotopy (0DQD)”.

Stacks 0DR1, closing claim: the map of part (1) is well defined up to formal homotopy. In the versal situation of Stacks 0DQU, let x₀ be a point of 𝒳 over Spec k for a field k of finite type over S, presented over an affine open Spec Λ ⊆ S with Λ → k finite, so that 𝓕_{𝒳,k,x₀} lives over 𝒞_Λ (Stacks 07T2). Let A' be a versal ring to 𝒳 at x₀ with versal formal object ξ', let A be the base of a formal object ξ of 𝓕_{𝒳,k,x₀} (for instance a second versal ring), and let y', y be objects of 𝒳 over Spec A', Spec A realizing ξ', ξ, i.e. morphisms Spec A' ⟶ 𝒳, Spec A ⟶ 𝒳 from which the formal objects come (Stacks 07X8). Then any two maps f, g : A' ⟶ A of \widehat{𝒞}_Λ compatible with these morphisms — each admitting a 2-arrow y ⟶ y' lying over its spectrum and restricting to the identity of x₀ — are formally homotopic (Stacks 0DQA). Applied with A, A' in either order this covers both the maps A' → A and A → A' of part (1) (see AlgebraicGeometry.Stack.exists_powerSeries_comparison_realization_pointed), and it is Stacks 0DQD, which applies since 𝓕_{𝒳,k,x₀} is a deformation category with finite-dimensional tangent space and infinitesimal automorphisms (Stacks 0DQW).

theorem formallyHomotopic_of_realization_compatible
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (ξ ξ' : Deformation.FormalObject (Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).projection)
    (hξ' : Deformation.IsVersal (Deformation.Artin.predeformationCategory_isPredeformationCategory
      D.B D.hS iΛ D.𝒳.val.val.p x₀ hx₀ D.𝒳.val.property).cofibered ξ')
    {hA : D.B.Contains (Spec (.of ξ.base))} {hA' : D.B.Contains (Spec (.of ξ'.base))}
    {y y' : D.𝒳.val.val.obj}
    {hy : D.𝒳.val.val.p.obj y = Deformation.Artin.baseOver D.B D.S D.hS
      (Deformation.Artin.completeLocalAlgFormalBase iΛ hfinite ξ.base) hA}
    {hy' : D.𝒳.val.val.p.obj y' = Deformation.Artin.baseOver D.B D.S D.hS
      (Deformation.Artin.completeLocalAlgFormalBase iΛ hfinite ξ'.base) hA'}
    (Ry : (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p x₀ hx₀
      hfinite ξ).Realization hA y hy)
    (Ry' : (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p x₀ hx₀
      hfinite ξ').Realization hA' y' hy')
    (f g : ξ'.base ⟶ ξ.base)
    (hf : ∃ m : y ⟶ y', (BigFppfOver.toScheme D.B D.S D.hS).map
        (eqToHom hy.symm ≫ D.𝒳.val.val.p.map m ≫ eqToHom hy') =
          Spec.map (CommRingCat.ofHom f.hom.toRingHom) ∧
        Deformation.Artin.realizationPointArrow Ry ≫ m =
          Deformation.Artin.realizationPointArrow Ry')
    (hg : ∃ m : y ⟶ y', (BigFppfOver.toScheme D.B D.S D.hS).map
        (eqToHom hy.symm ≫ D.𝒳.val.val.p.map m ≫ eqToHom hy') =
          Spec.map (CommRingCat.ofHom g.hom.toRingHom) ∧
        Deformation.Artin.realizationPointArrow Ry ≫ m =
          Deformation.Artin.realizationPointArrow Ry') :
    Deformation.CompleteLocalAlgCat.FormallyHomotopic f g

Tag 0DR2, a lemma

Tag 0DR2 in the Stacks Project.

AlgebraicGeometry.Stack.flatObject_of_realization_of_isVersal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingFlatAssembly.lean, line 258.

Stacks 0DR2. In Situation 0DQU — 𝒳 an algebraic stack locally of finite type over a locally Noetherian scheme S — let x₀ : Spec k ⟶ 𝒳 be a point with k a field of finite type over S, presented over an affine open Spec Λ ⊆ S, and let A be a versal ring to 𝒳 at x₀, with versal formal object ξ over A. Then the morphism Spec A ⟶ 𝒳 of Stacks 0DR1 — any object y of 𝒳 over Spec A realizing ξ, i.e. whose restrictions to the infinitesimal thickenings of the closed point are the levels of ξ — is flat.

The proof is the source's: Step III reaches a point of a smooth chart, where the morphism is Spec(𝒪^∧_{U, u₀}) ⟶ U ⟶ 𝒳, through two field extensions, and Steps I and II carry flatness back along the faithfully flat comparisons of parts (1) and (2) of Stacks 0DR1.

theorem flatObject_of_realization_of_isVersal
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (ξ : Deformation.FormalObject (Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).projection)
    (hξ : Deformation.IsVersal (Deformation.Artin.predeformationCategory_isPredeformationCategory
      D.B D.hS iΛ D.𝒳.val.val.p x₀ hx₀ D.𝒳.val.property).cofibered ξ)
    {hA : D.B.Contains (Spec (.of ξ.base))} {y : D.𝒳.val.val.obj}
    {hy : D.𝒳.val.val.p.obj y = Deformation.Artin.baseOver D.B D.S D.hS
      (Deformation.Artin.completeLocalAlgFormalBase iΛ hfinite ξ.base) hA}
    (Ry : (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p x₀ hx₀
      hfinite ξ).Realization hA y hy) :
    flatObject D.B D.S D.hS D.𝒳.val y

Tag 0DR3, a remark

Tag 0DR3 in the Stacks Project.

Deformation.RepresentablePresentation.comultiplication, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingCogroupoid.lean, line 142. The attribute's comment: “the comultiplication c : B ⟶ B ⊗̂_{s,A,t} B of the cogroupoid (A,B,s,t,c)”.

Stacks 0DR3. The comultiplication c : B ⟶ B ⊗̂_{s, A, t} B of a representable presentation (A, B, s, t): the composite of the two pushout inclusions under the presentation's composition law.

def comultiplication (P : RepresentablePresentation.{u, v, w} C) :
    P.arrows ⟶ pushout P.source P.target

Deformation.RepresentablePresentation.isCogroupoid_comultiplication, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingCogroupoid.lean, line 179. The attribute's comment: “(A,B,s,t,c) is a cogroupoid of complete local algebras”.

Stacks 0DR3. A representable presentation (A, B, s, t) and its comultiplication c form a cogroupoid.

theorem isCogroupoid_comultiplication (P : RepresentablePresentation.{u, v, w} C) :
    IsCogroupoid.{u, v, w} P.source P.target P.comultiplication

Deformation.exists_cogroupoid_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingCogroupoid.lean, line 298. The attribute's comment: “the equivalence [A/B] → 𝓕 of groupoids cofibred over 𝒞_Λ”.

Stacks 0DR3. Unwinding a presentation of a category cofibered in groupoids over 𝒞_Λ by a prorepresentable groupoid in functors: there are a cogroupoid (A, B, s, t, c) of Noetherian complete local Λ-algebras with residue field k and an equivalence [A|_{𝒞_Λ} / B|_{𝒞_Λ}] ⟶ 𝓕 of groupoids cofibered over 𝒞_Λ.

theorem exists_cogroupoid_presentation
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat.{uΛ, v, uk} Λ k)
    {G : GroupoidInFunctors.{_, v, max v uz} (ArtinianLocalAlgCat.{uΛ, v, uk} Λ k)}
    (hG : GroupoidInFunctors.IsProrepresentable G) (E : Presentation G p) :
    ∃ P : RepresentablePresentation.{_, v, uz} (CompleteLocalAlgCat.{uΛ, v, uk} Λ k),
      IsCogroupoid.{_, v, uz} P.source P.target P.comultiplication ∧
        Nonempty (Presentation
          (GroupoidInFunctors.restrict P.groupoidInFunctors artinianToComplete) p)

AlgebraicGeometry.Stack.isVersalRingAt_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingCogroupoid.lean, line 326. The attribute's comment: “A is a versal ring to 𝒳 at x₀”.

Stacks 0DR3, last clause. The base of a versal formal object of the deformation category of a field-valued point of 𝒳 is a versal ring to 𝒳 at that point.

theorem isVersalRingAt_base
    (D : AlgebraicGeometry.Stack.VersalSituation.{u, w})
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : _root_.AlgebraicGeometry.LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      _root_.AlgebraicGeometry.QuasiCompact
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    let C := Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀
    letI : Category C.carrier := C.category
    ∀ ξ : Deformation.FormalObject C.projection,
      Deformation.IsVersal
          (Deformation.Artin.predeformationCategory_isPredeformationCategory
            D.B D.hS iΛ D.𝒳.val.val.p x₀ hx₀ D.𝒳.val.property).cofibered ξ →
        IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite ξ.base

AlgebraicGeometry.Stack.hasSmoothPresentation_predeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingPresentation.lean, line 227. The attribute's comment: “F_{X,k,x₀} has a presentation by a smooth prorepresentable groupoid in functors”.

Stacks 0DR3, first sentence. In Situation 0DQU, let x₀ be an object of 𝒳 over Spec k for a field k of finite type over S, and let Spec Λ ⊆ S be an affine open through which Spec k ⟶ S factors with Λ → k finite. Then 𝓕_{𝒳,k,x₀} has a presentation by a smooth prorepresentable groupoid in functors on 𝒞_Λ: this is Stacks 0DQW and Stacks 06L8.

theorem hasSmoothPresentation_predeformationCategory
    (D : VersalSituation.{u, w}) {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    [Module.Finite Λ k] (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    letI := (Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).category
    Deformation.HasSmoothPresentation
      (Deformation.Artin.predeformationCategory iΛ
        (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).projection

AlgebraicGeometry.Stack.exists_versalCogroupoid_predeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/VersalRingPresentation.lean, line 264. The attribute's comment: “the unwinding: A with a versal formal object ξ, B with B|_{𝒞_Λ} ≅ A|_{𝒞_Λ} ×_{ξ,F,ξ} A|_{𝒞_Λ}, the projections formally smooth maps s, t : A → B, (A,B,s,t,c) a cogroupoid, the equivalence [A|_{𝒞_Λ}/B|_{𝒞_Λ}] → F induced by ξ, the equivalence [A/B] → F^ over the completed category, and A a versal ring to 𝒳 at x₀”.

Stacks 0DR3, the unwinding for 𝓕_{𝒳,k,x₀}. In Situation 0DQU, let x₀ be an object of 𝒳 over Spec k for a field k of finite type over S, and let Spec Λ ⊆ S be an affine open through which Spec k ⟶ S factors with Λ → k finite. Then there are 1. a versal formal object ξ of 𝓕 = 𝓕_{𝒳,k,x₀} over a Noetherian complete local Λ-algebra A with residue field k, and 2. a Noetherian complete local Λ-algebra B with residue field k and an isomorphism B|_{𝒞_Λ} ≅ A|_{𝒞_Λ} ×_{ξ, 𝓕, ξ} A|_{𝒞_Λ},

namely a representable presentation P on 𝒞^_Λ with objects A and arrows B whose restriction to 𝒞_Λ is isomorphic to the groupoid in functors of ξ (Stacks 06KY), such that the projections are induced by formally smooth maps s, t : A ⟶ B (power series maps, formally smooth for the 𝔪_B-adic topology), the comultiplication c : B ⟶ B ⊗̂_{s, A, t} B makes (A, B, s, t, c) a cogroupoid, ξ induces an equivalence [A|_{𝒞_Λ} / B|_{𝒞_Λ}] → 𝓕 of groupoids cofibred over 𝒞_Λ, there is an equivalence [A/B] → 𝓕^ of groupoids cofibred over 𝒞^_Λ, and A is a versal ring to 𝒳 at x₀.

theorem exists_versalCogroupoid_predeformationCategory
    (D : VersalSituation.{u, w}) {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    [Module.Finite Λ k] (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    let C := Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀
    letI := C.category
    let hp := Deformation.Artin.predeformationCategory_isPredeformationCategory
      D.B D.hS iΛ D.𝒳.val.val.p x₀ hx₀ D.𝒳.val.property
    ∃ (ξ : Deformation.FormalObject C.projection) (_ : Deformation.IsVersal hp.cofibered ξ)
      (P : Deformation.RepresentablePresentation.{_, u, u}
        (Deformation.CompleteLocalAlgCat.{u, u, u} Λ k)),
      P.objects = ξ.base ∧
      Nonempty (Deformation.versalGroupoid C.projection hp ξ ≅
        Deformation.GroupoidInFunctors.restrict P.groupoidInFunctors
          Deformation.artinianToComplete) ∧
      (Deformation.IsPowerSeriesOver P.source ∧
        RingHom.FormallySmoothNAdic.{u} P.source.hom.toRingHom
          (IsLocalRing.maximalIdeal P.arrows)) ∧
      (Deformation.IsPowerSeriesOver P.target ∧
        RingHom.FormallySmoothNAdic.{u} P.target.hom.toRingHom
          (IsLocalRing.maximalIdeal P.arrows)) ∧
      Deformation.IsCogroupoid.{_, u, u} P.source P.target P.comultiplication ∧
      Nonempty (Deformation.Presentation (Deformation.GroupoidInFunctors.restrict
        P.groupoidInFunctors Deformation.artinianToComplete) C.projection) ∧
      Nonempty (Deformation.Presentation P.groupoidInFunctors
        (Deformation.FormalObject.projection (p := C.projection))) ∧
      IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite P.objects

Sources

• Section 107.2, Tag 0DQT
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.VersalSituation · AlgebraicGeometry.Stack.IsVersalRingAt · AlgebraicGeometry.Stack.isVersalRingAt_iff_of_affineOpenPresentation · AlgebraicGeometry.Stack.isFiniteDimensionalDeformationCategory_of_versalSituation · AlgebraicGeometry.Stack.versalRing_powerSeries_comparison · AlgebraicGeometry.Stack.exists_isVersalRingAt · AlgebraicGeometry.Stack.exists_isVersalRingAt_fieldExtension · AlgebraicGeometry.Stack.isVersalAt_iff_exists_isRelativelySmooth_restrict

Section107.3 Multiplicities of components of algebraic stacks#

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

Tag 0DR5, a lemma

Tag 0DR5 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.closure_image_chartPointMap_mem_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ComponentMultiplicity.lean, line 229. The attribute's comment: “closure of the image of an irreducible component”.

For a smooth 1-morphism to a locally Noetherian algebraic stack over S from the algebraic stack of a scheme U of the site, the closure of the image of any irreducible component of U is an irreducible component of the space of points of Stacks 04XL.

theorem closure_image_chartPointMap_mem_irreducibleComponents (U : BigFppfOver B S hS)
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (hN : Stack.HasPropertyOnSomeSchemeAtlas B S hS
      (fun X : Scheme.{u} => IsLocallyNoetherian X) 𝒳)
    (f : Stack.schemeStack.{u, w} B S hS U ⟶ 𝒳) (hf : IsSmooth B S hS f)
    (T : Set ((BigFppfOver.toScheme B S hS).obj U))
    (hT : T ∈ irreducibleComponents ((BigFppfOver.toScheme B S hS).obj U)) :
    letI := Stack.pointTopology B S hS 𝒳.val
    closure (chartPointMap B S hS U 𝒳 f '' T) ∈ irreducibleComponents (points B S hS 𝒳)

AlgebraicGeometry.Stack.AlgebraicStacks.exists_mem_irreducibleComponents_closure_image_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ComponentMultiplicity.lean, line 249. The attribute's comment: “surjective charts give every irreducible component”.

For a smooth surjective 1-morphism to a locally Noetherian algebraic stack over S from the algebraic stack of a scheme U of the site, every irreducible component of the space of points of Stacks 04XL is the closure of the image of an irreducible component of U.

theorem exists_mem_irreducibleComponents_closure_image_eq (U : BigFppfOver B S hS)
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (hN : Stack.HasPropertyOnSomeSchemeAtlas B S hS
      (fun X : Scheme.{u} => IsLocallyNoetherian X) 𝒳)
    (f : Stack.schemeStack.{u, w} B S hS U ⟶ 𝒳) (hf : IsSmooth B S hS f)
    (hfs : Stack.IsSurjective B S hS f) :
    letI := Stack.pointTopology B S hS 𝒳.val
    ∀ Z ∈ irreducibleComponents (points B S hS 𝒳),
      ∃ T ∈ irreducibleComponents ((BigFppfOver.toScheme B S hS).obj U),
        closure (chartPointMap B S hS U 𝒳 f '' T) = Z

Tag 0DR6, a lemma

Tag 0DR6 in the Stacks Project.

Stacks.Chow.componentMultiplicity_id_eq_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/SmoothComponentMultiplicity.lean, line 119.

Stacks 0DR6. Let f : U ⟶ X be a smooth morphism of locally Noetherian schemes, let T' be an irreducible component of U and let T be the irreducible component of X obtained as the closure of the image of T'. Then T' and T have the same multiplicity.

public theorem componentMultiplicity_id_eq_of_smooth
    {X U : Scheme.{u}} (f : U ⟶ X) [Smooth f] [IsLocallyNoetherian X]
    (T' : irreducibleComponents U) (T : irreducibleComponents X)
    (hT : closure (f.base '' (T' : Set U)) = (T : Set X)) :
    Stacks.Chow.componentMultiplicity (𝟙 U) (genericPoints.ofComponent T') =
      Stacks.Chow.componentMultiplicity (𝟙 X) (genericPoints.ofComponent T)

Tag 0DR7, a lemma

Tag 0DR7 in the Stacks Project.

AlgebraicGeometry.Stack.componentMultiplicity_eq_of_closure_image_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ComponentMultiplicityIndependence.lean, line 227.

Stacks 0DR7. Let f₁ : U₁ → 𝒳 and f₂ : U₂ → 𝒳 be smooth 1-morphisms to a locally Noetherian algebraic stack over S from the algebraic stacks of two schemes U₁, U₂ of the site, and let T₁, T₂ be irreducible components of U₁, U₂. If the closures of the images of T₁ and T₂ in the space of points of Stacks 04XL of 𝒳 are the same irreducible component T, then T₁ and T₂ have the same multiplicity.

Together with Stacks 0DR5 this makes the multiplicity of an irreducible component of |𝒳| well defined: it may be computed on any smooth scheme chart, by any component lying over it.

theorem componentMultiplicity_eq_of_closure_image_eq
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hN : HasPropertyOnSomeSchemeAtlas B S hS
      (fun X : Scheme.{u} => IsLocallyNoetherian X) 𝒳)
    (U₁ U₂ : BigFppfOver B S hS)
    (f₁ : schemeStack.{u, w} B S hS U₁ ⟶ 𝒳) (f₂ : schemeStack.{u, w} B S hS U₂ ⟶ 𝒳)
    (hf₁ : AlgebraicStacks.IsSmooth B S hS f₁) (hf₂ : AlgebraicStacks.IsSmooth B S hS f₂)
    (T₁ : irreducibleComponents ((BigFppfOver.toScheme B S hS).obj U₁))
    (T₂ : irreducibleComponents ((BigFppfOver.toScheme B S hS).obj U₂)) :
    letI := pointTopology B S hS (schemeStack.{u, w} B S hS U₁).val
    letI := pointTopology B S hS (schemeStack.{u, w} B S hS U₂).val
    ∀ T ∈ irreducibleComponents (AlgebraicStacks.points B S hS 𝒳),
      closure (AlgebraicStacks.pointsMap B S hS f₁ ''
          ((pointsHomeomorphScheme B S hS U₁).symm '' (T₁ : Set _))) = T →
        closure (AlgebraicStacks.pointsMap B S hS f₂ ''
            ((pointsHomeomorphScheme B S hS U₂).symm '' (T₂ : Set _))) = T →
          _root_.Stacks.Chow.componentMultiplicity
                (𝟙 ((BigFppfOver.toScheme B S hS).obj U₁)) (genericPoints.ofComponent T₁) =
            _root_.Stacks.Chow.componentMultiplicity
                (𝟙 ((BigFppfOver.toScheme B S hS).obj U₂)) (genericPoints.ofComponent T₂)

Tag 0DR8, a definition

Tag 0DR8 in the Stacks Project.

AlgebraicGeometry.Stack.componentMultiplicity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StackComponentMultiplicity.lean, line 147.

Stacks 0DR8. The multiplicity m_{T, 𝒳} of an irreducible component T of the space of points of Stacks 04XL of a locally Noetherian algebraic stack 𝒳 over S: the multiplicity of Stacks 02QU of an irreducible component of a smooth scheme chart of 𝒳 whose image on points has closure T.

noncomputable def componentMultiplicity (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hN : HasPropertyOnSomeSchemeAtlas B S hS
      (fun X : Scheme.{u} => IsLocallyNoetherian X) 𝒳)
    (T : Set (AlgebraicStacks.points B S hS 𝒳))
    (hT : T ∈ irreducibleComponents (AlgebraicStacks.points B S hS 𝒳)) : ℤ

AlgebraicGeometry.Stack.componentMultiplicity_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StackComponentMultiplicity.lean, line 170. The attribute's comment: “the multiplicity is computed by any smooth chart”.

Stacks 0DR8. The multiplicity of an irreducible component T of the space of points of a locally Noetherian algebraic stack over S is computed by any smooth 1-morphism f : U → 𝒳 from the algebraic stack of a scheme of the site and any irreducible component T' of U whose image on points has closure T: it is the length of the local ring of U at the generic point of T'.

theorem componentMultiplicity_eq (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hN : HasPropertyOnSomeSchemeAtlas B S hS
      (fun X : Scheme.{u} => IsLocallyNoetherian X) 𝒳)
    (T : Set (AlgebraicStacks.points B S hS 𝒳))
    (hT : T ∈ irreducibleComponents (AlgebraicStacks.points B S hS 𝒳))
    (U : BigFppfOver B S hS) (f : schemeStack.{u, w} B S hS U ⟶ 𝒳)
    (hf : AlgebraicStacks.IsSmooth B S hS f)
    (T' : irreducibleComponents ((BigFppfOver.toScheme B S hS).obj U))
    (hT' : closure (AlgebraicStacks.chartPointMap B S hS U 𝒳 f '' (T' : Set _)) = T) :
    componentMultiplicity.{u, w} B S hS 𝒳 hN T hT =
      _root_.Stacks.Chow.componentMultiplicity
        (𝟙 ((BigFppfOver.toScheme B S hS).obj U)) (genericPoints.ofComponent T')

Sources

• Section 107.3, Tag 0DR4
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.AlgebraicStacks.closure_image_chartPointMap_mem_irreducibleComponents · AlgebraicGeometry.Stack.AlgebraicStacks.exists_mem_irreducibleComponents_closure_image_eq · Stacks.Chow.componentMultiplicity_id_eq_of_smooth · AlgebraicGeometry.Stack.componentMultiplicity_eq_of_closure_image_eq · AlgebraicGeometry.Stack.componentMultiplicity · AlgebraicGeometry.Stack.componentMultiplicity_eq

Section107.4 Formal branches and multiplicities#

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

Tag 0DRA, a definition

Tag 0DRA in the Stacks Project.

AlgebraicGeometry.Stack.formalBranches, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FormalBranches.lean, line 94. The attribute's comment: “relative to a chosen versal ring”.

Stacks 0DRA. The formal branches of 𝒳 through x₀, read off a versal ring A to 𝒳 at x₀: the irreducible components of Spec A, each recorded by its generic point, that is, the set of minimal primes of A.

def formalBranches
    (_hA : IsVersalRingAt D iΛ hiΛ x₀ hx₀ hfinite A) : Set (Ideal A)

Tag 0DRB, a lemma

Tag 0DRB in the Stacks Project.

AlgebraicGeometry.Stack.formalBranchComponent_surjective_and_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FormalBranchComponents.lean, line 1074.

Stacks 0DRB. In the situation of Definition 0DRA — an algebraic stack 𝒳 locally of finite type over a locally Noetherian scheme S, a point x₀ : Spec k ⟶ 𝒳 with k of finite type over S, and a versal ring A to 𝒳 at x₀, the base of a versal formal object ξ with its morphism y : Spec A ⟶ 𝒳 of Stacks 0DR1 — there is a canonical surjection from the formal branches of 𝒳 through x₀ to the irreducible components of |𝒳| containing x₀.

The map is AlgebraicGeometry.Stack.formalBranchComponent: a branch, recorded by its generic point P, goes to the closure of the image of P under Spec A ⟶ 𝒳 (AlgebraicGeometry.Stack.coe_formalBranchComponent). The first conjunct is surjectivity. The second is canonicity: for any other versal formal object at x₀, for any presentation of x₀, with versal ring A' and realization y', the two maps agree along the identification of the branches of A and A' by the faithfully flat comparison of part (1) of Stacks 0DR1, in whichever direction it goes.

theorem formalBranchComponent_surjective_and_canonical :
    Function.Surjective (formalBranchComponent D iΛ hiΛ x₀ hx₀ hfinite ξ hξ Ry) ∧
    ∀ (Λ' : Type u) [CommRing Λ'] [Algebra Λ' k]
      (iΛ' : Spec (.of Λ') ⟶ D.S) (hiΛ' : _root_.AlgebraicGeometry.IsOpenImmersion iΛ')
      (hx₀' : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
        Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ'))
      (hfinite' : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ') ∧
        QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ' k)) ≫ iΛ'))
      (ξ' : Deformation.FormalObject (Deformation.Artin.predeformationCategory iΛ'
        (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀').projection)
      (hξ' : Deformation.IsVersal
        (Deformation.Artin.predeformationCategory_isPredeformationCategory
          D.B D.hS iΛ' D.𝒳.val.val.p x₀ hx₀' D.𝒳.val.property).cofibered ξ')
      (hA' : D.B.Contains (Spec (.of ξ'.base))) (y' : D.𝒳.val.val.obj)
      (hy' : D.𝒳.val.val.p.obj y' = Deformation.Artin.baseOver D.B D.S D.hS
        (Deformation.Artin.completeLocalAlgFormalBase iΛ' hfinite' ξ'.base) hA')
      (Ry' : (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ' D.𝒳.val.val.p
        x₀ hx₀' hfinite' ξ').Realization hA' y' hy'),
      (∃ φ : (ξ'.base : Type u) →+* ξ.base, Flat (Spec.map (CommRingCat.ofHom φ)) ∧
        Surjective (Spec.map (CommRingCat.ofHom φ)) ∧
        ∀ P, ∃ hP : P.1.comap φ ∈ formalBranches D iΛ' hiΛ' x₀ hx₀' hfinite' ξ'.base
            ⟨ξ', rfl, hξ'⟩,
          (formalBranchComponent D iΛ hiΛ x₀ hx₀ hfinite ξ hξ Ry P).1 =
            (formalBranchComponent D iΛ' hiΛ' x₀ hx₀' hfinite' ξ' hξ' Ry' ⟨_, hP⟩).1) ∨
      (∃ φ : (ξ.base : Type u) →+* ξ'.base, Flat (Spec.map (CommRingCat.ofHom φ)) ∧
        Surjective (Spec.map (CommRingCat.ofHom φ)) ∧
        ∀ P', ∃ hP : P'.1.comap φ ∈ formalBranches D iΛ hiΛ x₀ hx₀ hfinite ξ.base ⟨ξ, rfl, hξ⟩,
          (formalBranchComponent D iΛ' hiΛ' x₀ hx₀' hfinite' ξ' hξ' Ry' P').1 =
            (formalBranchComponent D iΛ hiΛ x₀ hx₀ hfinite ξ hξ Ry ⟨_, hP⟩).1)

Tag 0DRC, a definition

Tag 0DRC in the Stacks Project.

AlgebraicGeometry.Stack.formalBranchMultiplicity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FormalBranches.lean, line 140. The attribute's comment: “relative to a chosen versal ring”.

Stacks 0DRC. The multiplicity of a formal branch of 𝒳 through x₀: the multiplicity of the corresponding irreducible component of Spec A, that is, the length over itself of the local ring of Spec A at the generic point of that component.

def formalBranchMultiplicity {p : Ideal A}
    (hp : p ∈ formalBranches D iΛ hiΛ x₀ hx₀ hfinite A hA) : ℕ∞

Tag 0DRD, a lemma

Tag 0DRD in the Stacks Project.

AlgebraicGeometry.Stack.componentMultiplicity_formalBranchComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FormalBranchMultiplicity.lean, line 299.

Stacks 0DRD. Let 𝒳 be an algebraic stack locally of finite type over a locally Noetherian scheme S (the versal situation, Stacks 0DQU) and let x₀ : Spec k ⟶ 𝒳 be a point with k a field of finite type over S and image s ∈ S. If 𝒪_{S,s} is a G-ring, then the map of Stacks 0DRB, from the formal branches of 𝒳 through x₀ (read off the versal ring A of a versal formal object ξ realized by y over Spec A) to the irreducible components of |𝒳| through x₀, preserves multiplicities: the multiplicity (Stacks 0DR8) of the component attached to a branch is the multiplicity of the branch (Stacks 0DRC).

theorem componentMultiplicity_formalBranchComponent (D : VersalSituation.{u, w})
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (ξ : Deformation.FormalObject (Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀).projection)
    (hξ : Deformation.IsVersal (Deformation.Artin.predeformationCategory_isPredeformationCategory
      D.B D.hS iΛ D.𝒳.val.val.p x₀ hx₀ D.𝒳.val.property).cofibered ξ)
    {hA : D.B.Contains (Spec (.of ξ.base))} {y : D.𝒳.val.val.obj}
    {hy : D.𝒳.val.val.p.obj y = Deformation.Artin.baseOver D.B D.S D.hS
      (Deformation.Artin.completeLocalAlgFormalBase iΛ hfinite ξ.base) hA}
    (Ry : (Deformation.Artin.FormalObject.ofPredeformation D.B D.S D.hS iΛ D.𝒳.val.val.p x₀ hx₀
      hfinite ξ).Realization hA y hy)
    (s : D.S) (hs : (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) (closedPoint k) = s)
    (hG : IsGRing (D.S.presheaf.stalk s))
    (P : formalBranches D iΛ hiΛ x₀ hx₀ hfinite ξ.base ⟨ξ, rfl, hξ⟩) :
    componentMultiplicity.{u, w} D.B D.S D.hS D.𝒳 D.hasLocallyNoetherianAtlas
        (formalBranchComponent D iΛ hiΛ x₀ hx₀ hfinite ξ hξ Ry P).1
        (formalBranchComponent D iΛ hiΛ x₀ hx₀ hfinite ξ hξ Ry P).2.1 =
      ((formalBranchMultiplicity D iΛ hiΛ x₀ hx₀ hfinite ξ.base ⟨ξ, rfl, hξ⟩ P.2).toNat : ℤ)

Sources

• Section 107.4, Tag 0DR9
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.formalBranches · AlgebraicGeometry.Stack.formalBranchComponent_surjective_and_canonical · AlgebraicGeometry.Stack.formalBranchMultiplicity · AlgebraicGeometry.Stack.componentMultiplicity_formalBranchComponent

Section107.5 Dimension theory of algebraic stacks#

Section 107.5 of the Stacks Project, Tag 0DRE. 24 tags here are carried by 56 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DRF, a remark

Tag 0DRF in the Stacks Project.

Stacks.Examples.DimensionVersusPointSet.dimensionAtPoint_translationQuotient_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 371. The attribute's comment: “the first counterexample: 𝔸¹_k/ℤ has dimension 1 at every point”.

Stacks 0DRF. The dimension of 𝔸¹_k/ℤ at each of its points is 1: the affine line is a surjective étale chart and has local dimension 1 at every point.

theorem dimensionAtPoint_translationQuotient_eq_one
    (x : Space.points B (Spec (.of k)) hS
      (translationQuotient k B hS (contains_affineLine k B hS))) :
    Space.dimensionAtPoint B (Spec (.of k)) hS
        (translationQuotient k B hS (contains_affineLine k B hS))
        (isAlgebraicSpace_translationQuotient k B hS) x = 1

Stacks.Examples.DimensionVersusPointSet.topologicalKrullDim_points_translationQuotient_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 487. The attribute's comment: “the first counterexample: the point space of 𝔸¹_k/ℤ is of Krull dimension 0”.

Stacks 0DRF. The point space of 𝔸¹_k/ℤ is of Krull dimension 0, being indiscrete.

theorem topologicalKrullDim_points_translationQuotient_eq_zero :
    topologicalKrullDim (Space.points B (Spec (.of k)) hS
      (translationQuotient k B hS (contains_affineLine k B hS))) = (0 : WithBot ℕ∞)

Stacks.Examples.DimensionVersusPointSet.dimensionAtPoint_ne_topologicalKrullDimAt_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 511. The attribute's comment: “the dimension at a point differs from the local dimension of the point space”.

Stacks 0DRF. The dimension of an algebraic space at a point need not coincide with the dimension of its point space at that point: for 𝔸¹_k/ℤ over a field of characteristic zero the former is 1 while the latter is 0.

theorem dimensionAtPoint_ne_topologicalKrullDimAt_points
    (x : Space.points B (Spec (.of k)) hS
      (translationQuotient k B hS (contains_affineLine k B hS))) :
    Space.dimensionAtPoint B (Spec (.of k)) hS
        (translationQuotient k B hS (contains_affineLine k B hS))
        (isAlgebraicSpace_translationQuotient k B hS) x ≠
      topologicalKrullDimAt (Space.points B (Spec (.of k)) hS
        (translationQuotient k B hS (contains_affineLine k B hS))) x

Stacks.Examples.DimensionVersusPointSet.dimensionAtPoint_infiniteProductQuotient_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 594. The attribute's comment: “the second counterexample: the space X = U/R of Stacks 02Z8 has dimension 0 at every point”.

Stacks 0DRF. The algebraic space X = U/R of Stacks 02Z8 has dimension 0 at each of its points: U = Spec (∏ n : ℕ, K) is an étale chart surjective on points, and its point space is T₁ and sober, hence of local Krull dimension 0 at every one of its points.

theorem dimensionAtPoint_infiniteProductQuotient_eq_zero
    (x : Space.points B (base K) hS (quotient K B hS hU hR)) :
    Space.dimensionAtPoint B (base K) hS (quotient K B hS hU hR)
        (isAlgebraicSpace_quotient K B hS hU hR) x = 0

Stacks.Examples.DimensionVersusPointSet.isGenericPoint_quotientCoordinatePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 634. The attribute's comment: “the second counterexample: |X| admits x₀ as a generic point”.

Stacks 0DRF. The point x₀ is a generic point of the point space of X = U/R: the coordinate points are dense in |U| and all of them map to x₀, which is Stacks 02Z8.

theorem isGenericPoint_quotientCoordinatePoint :
    IsGenericPoint (quotientCoordinatePoint K B hS hU hR)
      (Set.univ : Set (Space.points B (base K) hS (quotient K B hS hU hR)))

Stacks.Examples.DimensionVersusPointSet.irreducibleSpace_points_infiniteProductQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 651. The attribute's comment: “the second counterexample: |X| is irreducible”.

Stacks 0DRF. The point space of X = U/R is irreducible: the closure of x₀ is all of it.

theorem irreducibleSpace_points_infiniteProductQuotient :
    IrreducibleSpace (Space.points B (base K) hS (quotient K B hS hU hR))

Stacks.Examples.DimensionVersusPointSet.topologicalKrullDim_points_infiniteProductQuotient_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 842. The attribute's comment: “the second counterexample: |X| is of Krull dimension 1”.

Stacks 0DRF. The point space of X = U/R is of Krull dimension 1: it is irreducible with generic point x₀, and every irreducible closed subset of it is either all of it or a single point.

theorem topologicalKrullDim_points_infiniteProductQuotient_eq_one :
    topologicalKrullDim (Space.points B (base K) hS (quotient K B hS hU hR)) = 1

Stacks.Examples.DimensionVersusPointSet.topologicalKrullDimAt_points_infiniteProductQuotient_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 859. The attribute's comment: “the second counterexample: the local dimension of |X| is 1 at each of its points other than x₀”.

Stacks 0DRF. The local Krull dimension of the point space of X = U/R is 1 at every point other than x₀: every open neighbourhood of such a point contains x₀ as well, whose closure is everything, so the point and the neighbourhood form a chain of length one.

theorem topologicalKrullDimAt_points_infiniteProductQuotient_eq_one
    (z : Space.points B (base K) hS (quotient K B hS hU hR))
    (hz : z ≠ quotientCoordinatePoint K B hS hU hR) :
    topologicalKrullDimAt (Space.points B (base K) hS (quotient K B hS hU hR)) z = 1

Stacks.Examples.DimensionVersusPointSet.dimensionAtPoint_ne_topologicalKrullDimAt_points_infiniteProductQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 887. The attribute's comment: “the second counterexample: the dimension at a point is smaller than the local dimension of the point space”.

Stacks 0DRF. The dimension of an algebraic space at a point can also be smaller than the dimension of its point space at that point: the space X = U/R of Stacks 02Z8 is of dimension 0 at each of its points, while the local Krull dimension of |X| is 1 at every point other than x₀.

theorem dimensionAtPoint_ne_topologicalKrullDimAt_points_infiniteProductQuotient
    (z : Space.points B (base K) hS (quotient K B hS hU hR))
    (hz : z ≠ quotientCoordinatePoint K B hS hU hR) :
    Space.dimensionAtPoint B (base K) hS (quotient K B hS hU hR)
        (isAlgebraicSpace_quotient K B hS hU hR) z ≠
      topologicalKrullDimAt (Space.points B (base K) hS (quotient K B hS hU hR)) z

Stacks.Examples.DimensionVersusPointSet.topologicalKrullDimAt_quotientCoordinatePoint_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 904. The attribute's comment: “the second counterexample, corrected: at x₀ the local dimension of |X| is 0, not 1”.

Stacks 0DRF is inaccurate at the generic point. The remark says of the example of Stacks 02Z8 that |X| admitting a generic point makes "the dimension of |X| at any of its points" equal to 1. That fails at the generic point x₀ itself: the coordinate points form an open subset of |U|, saturated for the relation, and |U| → |X| is open, so {x₀} is an open neighbourhood of x₀ of Krull dimension 0. At x₀ the two dimensions compared by the remark therefore agree, both being 0; the example separates them at every other point.

theorem topologicalKrullDimAt_quotientCoordinatePoint_eq_zero :
    topologicalKrullDimAt (Space.points B (base K) hS (quotient K B hS hU hR))
      (quotientCoordinatePoint K B hS hU hR) = 0

Stacks.Examples.DimensionVersusPointSet.exists_dimensionAtPoint_eq_zero_topologicalKrullDim_points_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DimensionVersusPointSet.lean, line 950. The attribute's comment: “the second counterexample exists: an algebraic space of dimension 0 at each of its points whose point space is irreducible of Krull dimension 1 with a generic point”.

Stacks 0DRF. There is an algebraic space over a field which is of dimension 0 at each of its points while its point space is irreducible of Krull dimension 1 and admits a generic point: the example of Stacks 02Z8 over the field with two elements, on a big fppf site containing the three schemes it is built from.

theorem exists_dimensionAtPoint_eq_zero_topologicalKrullDim_points_eq_one :
    ∃ (B : BigFppfSite.{u}) (hS : B.Contains (base (ULift.{u} (ZMod 2))))
      (F : (BigFppfOver B (base (ULift.{u} (ZMod 2))) hS)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B (base (ULift.{u} (ZMod 2))) hS F),
      (∀ x, Space.dimensionAtPoint B (base (ULift.{u} (ZMod 2))) hS F hF x = 0) ∧
        IrreducibleSpace (Space.points B (base (ULift.{u} (ZMod 2))) hS F) ∧
        topologicalKrullDim (Space.points B (base (ULift.{u} (ZMod 2))) hS F) = 1 ∧
        ∃ x₀, IsGenericPoint x₀
          (Set.univ : Set (Space.points B (base (ULift.{u} (ZMod 2))) hS F))

Declarations registered for the tag:

• AlgebraicGeometry.Space.topologicalKrullDimAt_points_eq_dimensionAtPoint_of_isDecentSpace, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/DimensionCoincidence.lean, line 27 (StacksFrontier): “the remark's last assertion: for a decent space the two dimensions do coincide at every point”.

Tag 0DRG, a definition

Tag 0DRG in the Stacks Project.

AlgebraicGeometry.Stack.relativeDimensionAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionAtPoint.lean, line 335. References: EGA IV (17.10.1).

The relative dimension dim_t(T_x) at t ∈ |T| of a 1-morphism f, locally of finite type, from an algebraic space T to an algebraic stack 𝒳: the dimension of the algebraic space T ×_𝒳 Spec k at a point above t, for a field-valued point Spec k ⟶ 𝒳 representing the image x of t. The representative and the point above t are the choices the source makes; the point above t exists by Stacks 04XH.

noncomputable def relativeDimensionAt
    (_hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f) (t : Space.points B S hS T) :
    WithBot ℕ∞

Tag 0DRH, a remark

Tag 0DRH in the Stacks Project.

AlgebraicGeometry.Stack.relativeDimensionAt_eq_fieldFibreDimensionAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionAtPoint.lean, line 1189. The attribute's comment: “relative_dimension_well_defined”.

The relative dimension relativeDimensionAt is well defined. The value of the formula of Stacks 0DRG at every field-valued point p representing the image of t and every point q of the fibre T ×_𝒳 Spec κ(p) above t is relativeDimensionAt, the value at the two choices the definition makes. So any two admissible pairs of choices give the same value, which is what makes relativeDimensionAt an invariant of (f, t).

theorem relativeDimensionAt_eq_fieldFibreDimensionAt
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f) (t : Space.points B S hS T)
    (p : FieldValuedPoint B S hS 𝒳.val.val)
    (q : points B S hS (fieldFibreSquare B S hS f.hom p).pt.val
      (fieldFibreSquare B S hS f.hom p).pt.property)
    (_hp : pointClass B S hS 𝒳.val.val 𝒳.val.property p =
      pointsMap B S hS (fibredCategory B S hS T).val
        (fibredCategory B S hS T).property 𝒳.val.property f.hom.hom
        (stackPointOfSpacePoint B S hS T t))
    (hq : pointsMap B S hS (fieldFibreSquare B S hS f.hom p).pt.val
        (fieldFibreSquare B S hS f.hom p).pt.property
        (fibredCategory B S hS T).property
        (fieldFibreSquare B S hS f.hom p).fst.hom q =
      stackPointOfSpacePoint B S hS T t) :
    relativeDimensionAt B S hS T hT 𝒳 f hf t =
      fieldFibreDimensionAt.{u, w} B S hS f.hom 𝒳.property
        (isRepresentableByAlgebraicSpace_fibredCategory B S hS T hT) p q

AlgebraicGeometry.Stack.relativeDimensionAt_eq_iff_hasRelativeDimensionAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionAtPoint.lean, line 1312. The attribute's comment: “relative_dimension_agrees_with_spaces”.

The relative dimension of Stacks 0DRG agrees with the relative dimension of a morphism of algebraic spaces. For a morphism g : T ⟶ G of algebraic spaces over S, the relative dimension of Stacks 0DRG of the induced 1-morphism of algebraic stacks is, at every point t ∈ |T|, the relative dimension d of g at t in the sense of Stacks 04NM.

theorem relativeDimensionAt_eq_iff_hasRelativeDimensionAt
    {T G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hT : IsAlgebraicSpace B S hS T) (hG : IsAlgebraicSpace B S hS G) (g : T ⟶ G)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS
      (algebraicSpaceStackMap.{u, w} B S hS hT hG g))
    (t : Space.points B S hS T) (d : ℕ∞) :
    relativeDimensionAt.{u, w} B S hS T hT (algebraicSpaceStack.{u, w} B S hS G hG)
        (algebraicSpaceStackMap.{u, w} B S hS hT hG g) hf t = (d : WithBot ℕ∞) ↔
      Space.HasRelativeDimensionAt d B S hS g t

Tag 0DRI, a lemma

Tag 0DRI in the Stacks Project.

AlgebraicGeometry.Stack.dimensionAtPoint_eq_add_relativeDimensionAt_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionSmoothSpaces.lean, line 80.

Stacks 0DRI. Let g : U ⟶ X be a smooth morphism of locally Noetherian algebraic spaces over S and let u ∈ |U| have image x ∈ |X|. Then dim_u(U) = dim_x(X) + dim_u(U_x), where dim_u(U_x) is the relative dimension of Stacks 0DRG of the induced 1-morphism of algebraic stacks at u.

theorem dimensionAtPoint_eq_add_relativeDimensionAt_of_isSmooth
    {U X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hU : IsAlgebraicSpace B S hS U) (hX : IsAlgebraicSpace B S hS X)
    (hNU : Space.HasEtaleLocalProperty B S hS U
      (fun Z : Scheme.{u} => IsLocallyNoetherian Z))
    (hNX : Space.HasEtaleLocalProperty B S hS X
      (fun Z : Scheme.{u} => IsLocallyNoetherian Z))
    (g : U ⟶ X) (hg : Space.IsSmooth B S hS g) (u : Space.points B S hS U) :
    Space.dimensionAtPoint B S hS U hU u =
      Space.dimensionAtPoint B S hS X hX (Space.pointsMap B S hS U g u) +
        relativeDimensionAt.{u, w} B S hS U hU (algebraicSpaceStack.{u, w} B S hS X hX)
          (algebraicSpaceStackMap.{u, w} B S hS hU hX g)
          (isLocallyOfFiniteType_algebraicSpaceStackMap_of_isSmooth.{u, w} B S hS hU hX g hg)
          u

Tag 0DRJ, a lemma

Tag 0DRJ in the Stacks Project.

AlgebraicGeometry.Stack.dimensionAtPoint_eq_dimensionSubNat_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionChartIndependence.lean, line 497. The attribute's comment: “dimension via a smooth algebraic space”.

Let 𝒳 be a locally Noetherian algebraic stack over S, let f : T ⟶ 𝒳 be a smooth, locally-of-finite-type 1-morphism from an algebraic space, and let t ∈ |T| lie above x ∈ |𝒳|. If the relative dimension of Stacks 0DRG of f at t is the natural number d, then dim_x(𝒳) = dim_t(T) - d.

theorem dimensionAtPoint_eq_dimensionSubNat_of_isSmooth
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (x : points B S hS 𝒳.val.val 𝒳.val.property)
    {T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hT : IsAlgebraicSpace B S hS T)
    (f : algebraicSpaceStack.{u, w} B S hS T hT ⟶ 𝒳)
    (hsm : AlgebraicStacks.IsSmooth B S hS f)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (t : Space.points B S hS T)
    (ht : pointsMap B S hS (fibredCategory B S hS T).val
      (fibredCategory B S hS T).property 𝒳.val.property f.hom.hom
      (stackPointOfSpacePoint B S hS T t) = x)
    (d : ℕ) (hd : relativeDimensionAt.{u, w} B S hS T hT 𝒳 f hf t = (d : WithBot ℕ∞)) :
    dimensionAtPoint B S hS 𝒳 h𝒳 x =
      dimensionSubNat (Space.dimensionAtPoint B S hS T hT t) d

AlgebraicGeometry.Stack.exists_dimensionAtPoint_eq_dimensionSubNat_of_isSmooth_schemeChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionSchemeChart.lean, line 164. The attribute's comment: “dimension via a smooth scheme chart”.

Stacks 0DRJ at a smooth chart by a scheme of the site. Let 𝒳 be a locally Noetherian algebraic stack over S, let f : U ⟶ 𝒳 be a smooth 1-morphism from the algebraic stack of a scheme U of the site, and let u ∈ U. Then the relative dimension of Stacks 0DRG at u is a natural number d and

dim_{f(u)}(𝒳) = dim_u(U) - d,

the first term being the dimension of Stacks 0AFN and the second the local Krull dimension of the scheme U at u.

The two models of U as an algebraic stack are compared by AlgebraicGeometry.Stack.exists_smooth_algebraicSpaceStack_hom_pointsMap_eq, which turns f into a smooth chart by the algebraic space yoneda.obj U through the same point of |𝒳|; the formula is then AlgebraicGeometry.Stack.exists_dimensionAtPoint_eq_dimensionSubNat_of_isSmooth there, with the dimension of Stacks 04N5 of yoneda.obj U identified with the local Krull dimension of U by AlgebraicGeometry.Stack.dimensionAtPoint_yoneda_eq_topologicalKrullDimAt. Local finite type of the chart, which Stacks 0DRG needs to speak of its relative dimension, is a consequence of smoothness by Stacks 06MH.

theorem exists_dimensionAtPoint_eq_dimensionSubNat_of_isSmooth_schemeChart
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (U : BigFppfOver B S hS) (f : schemeStack.{u, w} B S hS U ⟶ 𝒳)
    (hf : AlgebraicStacks.IsSmooth B S hS f)
    (u : (BigFppfOver.toScheme B S hS).obj U) :
    ∃ d : ℕ,
      dimensionAtPoint B S hS 𝒳 h𝒳 (AlgebraicStacks.chartPointMap B S hS U 𝒳 f u) =
        dimensionSubNat (topologicalKrullDimAt ((BigFppfOver.toScheme B S hS).obj U) u) d

AlgebraicGeometry.Stack.dimensionAtPoint_eq_dimensionSubNat_relativeDimensionAt_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionSmoothChart.lean, line 67. The attribute's comment: “dimension via a smooth algebraic space, from smoothness alone”.

Stacks 0DRJ. Let 𝒳 be a locally Noetherian algebraic stack over S, let f : T ⟶ 𝒳 be a smooth 1-morphism from an algebraic space, and let t ∈ |T| lie above x ∈ |𝒳|. Then

dim_x(𝒳) = dim_t(T) - dim_t(T_x),

the left-hand side being the dimension of Stacks 0AFN and dim_t(T_x) the relative dimension of Stacks 0DRG of f at t.

The relative dimension is taken at the local finite type of f that smoothness gives (Stacks 06MH, AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_of_isSmooth). It is a natural number (AlgebraicGeometry.Stack.exists_relativeDimensionAt_eq_natCast), and it enters the subtraction as that natural number, ENat.toNat (r.unbotD 0).

theorem dimensionAtPoint_eq_dimensionSubNat_relativeDimensionAt_of_isSmooth
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (x : points B S hS 𝒳.val.val 𝒳.val.property)
    {T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hT : IsAlgebraicSpace B S hS T)
    (f : algebraicSpaceStack.{u, w} B S hS T hT ⟶ 𝒳)
    (hsm : AlgebraicStacks.IsSmooth B S hS f)
    (t : Space.points B S hS T)
    (ht : pointsMap B S hS (fibredCategory B S hS T).val
      (fibredCategory B S hS T).property 𝒳.val.property f.hom.hom
      (stackPointOfSpacePoint B S hS T t) = x) :
    dimensionAtPoint B S hS 𝒳 h𝒳 x =
      dimensionSubNat (Space.dimensionAtPoint B S hS T hT t)
        (ENat.toNat ((relativeDimensionAt.{u, w} B S hS T hT 𝒳 f
          (AlgebraicStacks.isLocallyOfFiniteType_of_isSmooth B S hS f hsm) t).unbotD 0))

AlgebraicGeometry.Stack.exists_relativeDimensionAt_eq_natCast, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionFiniteness.lean, line 89. The attribute's comment: “finiteness of the relative dimension”.

The relative dimension of Stacks 0DRG is a natural number. For a 1-morphism f : T ⟶ 𝒳 locally of finite type from an algebraic space to an algebraic stack and a point t ∈ |T|, the value dim_t(T_x) is finite.

theorem exists_relativeDimensionAt_eq_natCast
    (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hT : IsAlgebraicSpace B S hS T)
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (f : algebraicSpaceStack.{u, w} B S hS T hT ⟶ 𝒳)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (t : Space.points B S hS T) :
    ∃ d : ℕ, relativeDimensionAt.{u, w} B S hS T hT 𝒳 f hf t = (d : WithBot ℕ∞)

Tag 0DRK, a remark

Tag 0DRK in the Stacks Project.

AlgebraicGeometry.Stack.dimensionAtPoint_eq_topologicalKrullDimAt_of_isDeligneMumfordStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionDeligneMumford.lean, line 350. The attribute's comment: “Deligne-Mumford stacks which are decent: dim_x(𝒳) = dim_x |𝒳|”.

Stacks 0DRK, the Deligne-Mumford case. Let 𝒳 be a locally Noetherian Deligne-Mumford algebraic stack over S which is decent. Then at every point x ∈ |𝒳| the dimension of 𝒳 (Stacks 0AFN) agrees with the local Krull dimension dim_x |𝒳| of its point space.

An étale chart c : W ⟶ 𝒳 by a scheme has relative dimension 0 everywhere, so by Stacks 0DRJ the dimension of 𝒳 at x = c(t) is the dimension of W at t, which is dim_t |W|. The map |W| ⟶ |𝒳| is continuous and open (Stacks 06R7), generizations lift along it (Stacks 0GVZ, decency supplying the quasi-compact representatives), and it collapses no specialization (AlgebraicGeometry.Stack.eq_of_specializes_of_spacePointMap_eq_of_isRelativelyEtale); |W| is sober and |𝒳| is sober by Stacks 0GW8, so the two local dimensions agree.

theorem dimensionAtPoint_eq_topologicalKrullDimAt_of_isDeligneMumfordStack
    (𝒳 : AlgebraicStacks.{u, w} B S hS) (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (hDM : IsDeligneMumfordStack.{u, w} B S hS 𝒳.val.val) (hdec : IsDecent B S hS 𝒳.val)
    (x : points B S hS 𝒳.val.val 𝒳.val.property) :
    dimensionAtPoint B S hS 𝒳 h𝒳 x =
      dimensionSubNat (topologicalKrullDimAt (points B S hS 𝒳.val.val 𝒳.val.property) x) 0

AlgebraicGeometry.Stack.dimensionAtPoint_eq_topologicalKrullDimAt_of_isDeligneMumfordStack_of_quasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionDeligneMumford.lean, line 397. The attribute's comment: “quasi-separated Deligne-Mumford stacks: dim_x(𝒳) = dim_x |𝒳|”.

Stacks 0DRK, the quasi-separated Deligne-Mumford case. At every point of a locally Noetherian, quasi-separated Deligne-Mumford algebraic stack 𝒳 the dimension of 𝒳 agrees with the local Krull dimension of |𝒳|. A quasi-separated algebraic stack is decent (Stacks 0GW2).

theorem dimensionAtPoint_eq_topologicalKrullDimAt_of_isDeligneMumfordStack_of_quasiSeparated
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (𝒳 : AlgebraicStacks.{u, w} B S hS) (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (hDM : IsDeligneMumfordStack.{u, w} B S hS 𝒳.val.val)
    (hqs : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒳)
    (x : points B S hS 𝒳.val.val 𝒳.val.property) :
    dimensionAtPoint B S hS 𝒳 h𝒳 x =
      dimensionSubNat (topologicalKrullDimAt (points B S hS 𝒳.val.val 𝒳.val.property) x) 0

Stacks.Examples.AffineLineQuotient.affineLineQuotientStack_points_dimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/AffineLineQuotientDimension.lean, line 845. The attribute's comment: “the example [A¹/Gₘ] over a field: |𝒳| has two points, one a specialisation of the other, |𝒳| has Krull dimension 1, and dim_x(𝒳) = 0 at both points”.

Stacks 0DRK, the example [𝔸¹/𝔾ₘ]. Over a field k, let [𝔸¹/𝔾ₘ] be the quotient stack of the multiplicative group acting on the affine line by multiplication. It is an algebraic stack, equivalent over the site to an object 𝒳 of the 2-category of algebraic stacks, and for every such 𝒳: * |𝒳| has exactly two points x₀ ≠ x₁, and x₀ is a specialisation of x₁ (they are the images of the two orbits {0} and 𝔸¹ ∖ {0}); * |𝒳| has Krull dimension 1 as a topological space; * 𝒳 is locally Noetherian, and dim_x(𝒳) = 0 (Stacks 0AFN) at both points x.

theorem affineLineQuotientStack_points_dimension {k : Type u} [Field k]
    (hk : C.Contains (Spec (.of k))) :
    (∃ 𝒳 : Stack.AlgebraicStacks.{u, w} C (Spec (.of k)) hk,
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (affineLineQuotientStack C (Spec (.of k)) hk).p 𝒳.val.val.p)) ∧
    ∀ (𝒳 : Stack.AlgebraicStacks.{u, w} C (Spec (.of k)) hk)
      (_e : StacksRepresentableCFG.EquivalenceOver
        (affineLineQuotientStack C (Spec (.of k)) hk).p 𝒳.val.val.p),
      letI := Stack.pointTopology C (Spec (.of k)) hk 𝒳.val
      (∃ x₀ x₁ : Stack.points C (Spec (.of k)) hk 𝒳.val.val 𝒳.val.property,
        x₀ ≠ x₁ ∧ (∀ x, x = x₀ ∨ x = x₁) ∧ x₁ ⤳ x₀) ∧
      topologicalKrullDim (Stack.points C (Spec (.of k)) hk 𝒳.val.val 𝒳.val.property) = 1 ∧
      Stack.IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk 𝒳 ∧
      ∀ (h𝒳 : Stack.IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk 𝒳) x,
        Stack.dimensionAtPoint C (Spec (.of k)) hk 𝒳 h𝒳 x = 0

Stacks.Examples.AffineLineQuotient.classifyingStack_multiplicativeGroup_dimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/AffineLineQuotientDimension.lean, line 972. The attribute's comment: “the example [Spec k/Gₘ]: the classifying stack has a unique point, at which its dimension is -1”.

Stacks 0DRK, the example [Spec k/𝔾ₘ]. Over a field k the classifying stack [Spec k/𝔾ₘ] of the multiplicative group is an algebraic stack, equivalent over the site to an object 𝒳 of the 2-category of algebraic stacks, and for every such 𝒳, which is locally Noetherian, |𝒳| has a unique point, at which dim_x(𝒳) = -1 (Stacks 0AFN).

theorem classifyingStack_multiplicativeGroup_dimension {k : Type u} [Field k]
    (hk : C.Contains (Spec (.of k))) :
    (∃ 𝒳 : Stack.AlgebraicStacks.{u, w} C (Spec (.of k)) hk,
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (Stack.classifyingStack C hk (multiplicativeGroupOverField C hk)).val.p 𝒳.val.val.p)) ∧
    ∀ (𝒳 : Stack.AlgebraicStacks.{u, w} C (Spec (.of k)) hk)
      (_e : StacksRepresentableCFG.EquivalenceOver
        (Stack.classifyingStack C hk (multiplicativeGroupOverField C hk)).val.p 𝒳.val.val.p),
      Stack.IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk 𝒳 ∧
      ∃ x : Stack.points C (Spec (.of k)) hk 𝒳.val.val 𝒳.val.property,
        (∀ y, y = x) ∧
        ∀ h𝒳 : Stack.IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk 𝒳,
          Stack.dimensionAtPoint C (Spec (.of k)) hk 𝒳 h𝒳 x = ((-1 : ℤ) : EInt)

Stacks.Examples.remark_0DRK, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Stacks/DimensionAtPointRemark.lean, line 69. The attribute's comment: “the whole remark: dim_x(𝒳) = dim_x |𝒳| for decent (in particular quasi-separated) locally Noetherian Deligne-Mumford stacks; for [A¹/Gₘ] over a field |𝒳| has two points, one a specialisation of the other, |𝒳| has dimension 1 and dim_x(𝒳) = 0 at both points, so the equality fails; [Spec k/Gₘ] has dimension -1 at its unique point”.

Stacks 0DRK. The comparison of the dimension of an algebraic stack at a point (Stacks 0AFN) with the local Krull dimension of its space of points. 1. For a locally Noetherian Deligne-Mumford stack 𝒳 which is decent, dim_x(𝒳) = dim_x |𝒳| at every point x. 2. The same holds when 𝒳 is quasi-separated. 3. Over a field k, the quotient stack [𝔸¹/𝔾ₘ] of the multiplication action is an algebraic stack, and for every object 𝒳 of the 2-category of algebraic stacks equivalent to it, |𝒳| has exactly two points, one a specialisation of the other, |𝒳| has Krull dimension 1, and 𝒳 is locally Noetherian with dim_x(𝒳) = 0 at both points x. 4. Consequently the equality of 1 fails for such an 𝒳: at some point dim_x(𝒳) ≠ dim_x |𝒳|. 5. Over a field k, the classifying stack [Spec k/𝔾ₘ] is an algebraic stack, and every object 𝒳 equivalent to it is locally Noetherian, with a unique point x, at which dim_x(𝒳) = -1.

theorem remark_0DRK :
    (∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
      (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
      (h𝒳 : Stack.IsLocallyNoetherianStack.{u, w} B S hS 𝒳),
      Stack.IsDeligneMumfordStack.{u, w} B S hS 𝒳.val.val → Stack.IsDecent B S hS 𝒳.val →
      ∀ x : Stack.points B S hS 𝒳.val.val 𝒳.val.property,
        Stack.dimensionAtPoint B S hS 𝒳 h𝒳 x =
          Stack.dimensionSubNat
            (topologicalKrullDimAt (Stack.points B S hS 𝒳.val.val 𝒳.val.property) x) 0) ∧
    (∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
      (hZ : B.Contains (⊤_ Scheme.{u}))
      (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
      (h𝒳 : Stack.IsLocallyNoetherianStack.{u, w} B S hS 𝒳),
      Stack.IsDeligneMumfordStack.{u, w} B S hS 𝒳.val.val →
      Stack.AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒳 →
      ∀ x : Stack.points B S hS 𝒳.val.val 𝒳.val.property,
        Stack.dimensionAtPoint B S hS 𝒳 h𝒳 x =
          Stack.dimensionSubNat
            (topologicalKrullDimAt (Stack.points B S hS 𝒳.val.val 𝒳.val.property) x) 0) ∧
    (∀ (C : BigFppfSite.{u}) (k : Type u) [Field k] (hk : C.Contains (Spec (.of k))),
      (∃ 𝒳 : Stack.AlgebraicStacks.{u, w} C (Spec (.of k)) hk,
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (affineLineQuotientStack C (Spec (.of k)) hk).p 𝒳.val.val.p)) ∧
      ∀ (𝒳 : Stack.AlgebraicStacks.{u, w} C (Spec (.of k)) hk)
        (_e : StacksRepresentableCFG.EquivalenceOver
          (affineLineQuotientStack C (Spec (.of k)) hk).p 𝒳.val.val.p),
        (∃ x₀ x₁ : Stack.points C (Spec (.of k)) hk 𝒳.val.val 𝒳.val.property,
          x₀ ≠ x₁ ∧ (∀ x, x = x₀ ∨ x = x₁) ∧ x₁ ⤳ x₀) ∧
        topologicalKrullDim (Stack.points C (Spec (.of k)) hk 𝒳.val.val 𝒳.val.property) = 1 ∧
        Stack.IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk 𝒳 ∧
        ∀ (h𝒳 : Stack.IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk 𝒳) x,
          Stack.dimensionAtPoint C (Spec (.of k)) hk 𝒳 h𝒳 x = 0) ∧
    (∀ (C : BigFppfSite.{u}) (k : Type u) [Field k] (hk : C.Contains (Spec (.of k)))
      (𝒳 : Stack.AlgebraicStacks.{u, w} C (Spec (.of k)) hk)
      (_e : StacksRepresentableCFG.EquivalenceOver
        (affineLineQuotientStack C (Spec (.of k)) hk).p 𝒳.val.val.p)
      (h𝒳 : Stack.IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk 𝒳),
      ∃ x : Stack.points C (Spec (.of k)) hk 𝒳.val.val 𝒳.val.property,
        Stack.dimensionAtPoint C (Spec (.of k)) hk 𝒳 h𝒳 x ≠
          Stack.dimensionSubNat
            (topologicalKrullDimAt (Stack.points C (Spec (.of k)) hk 𝒳.val.val 𝒳.val.property)
              x) 0) ∧
    (∀ (C : BigFppfSite.{u}) (k : Type u) [Field k] (hk : C.Contains (Spec (.of k))),
      (∃ 𝒳 : Stack.AlgebraicStacks.{u, w} C (Spec (.of k)) hk,
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (Stack.classifyingStack C hk (multiplicativeGroupOverField C hk)).val.p 𝒳.val.val.p)) ∧
      ∀ (𝒳 : Stack.AlgebraicStacks.{u, w} C (Spec (.of k)) hk)
        (_e : StacksRepresentableCFG.EquivalenceOver
          (Stack.classifyingStack C hk (multiplicativeGroupOverField C hk)).val.p 𝒳.val.val.p),
        Stack.IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk 𝒳 ∧
        ∃ x : Stack.points C (Spec (.of k)) hk 𝒳.val.val 𝒳.val.property,
          (∀ y, y = x) ∧
          ∀ h𝒳 : Stack.IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk 𝒳,
            Stack.dimensionAtPoint C (Spec (.of k)) hk 𝒳 h𝒳 x = ((-1 : ℤ) : EInt))

Tag 0DRL, a definition

Tag 0DRL in the Stacks Project.

AlgebraicGeometry.Stack.relativeStackDimensionAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionStackMorphism.lean, line 235.

Stacks 0DRL. The relative dimension dim_t(𝒯_x) at t ∈ |𝒯| of a 1-morphism f, locally of finite type, of locally Noetherian algebraic stacks: the infimum of the dimensions of the locally Noetherian algebraic stack 𝒯 ×_𝒳 Spec k at a point above t, over the field-valued points Spec k ⟶ 𝒳 representing the image x of t and the points above t. Those are the two choices the source makes; a point above t exists by Stacks 04XH.

noncomputable def relativeStackDimensionAt (f : 𝒯 ⟶ 𝒳)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (_h𝒯 : IsLocallyNoetherianStack.{u, w} B S hS 𝒯)
    (_h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (t : points B S hS 𝒯.val.val 𝒯.val.property) : EInt

Tag 0DRM, a remark

Tag 0DRM in the Stacks Project.

AlgebraicGeometry.Stack.relativeStackDimensionAt_eq_fieldFibreStackDimensionAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionStackBaseChange.lean, line 543.

Stacks 0DRM. The relative dimension dim_t(𝒯_x) of Stacks 0DRL is well defined: for a locally-of-finite-type 1-morphism f : 𝒯 ⟶ 𝒳 of locally Noetherian algebraic stacks and a point t ∈ |𝒯|, it is the value of the formula of Stacks 0DRL at every admissible pair of choices — a field-valued point p of 𝒳 representing the image of t and a point of 𝒯 ×_𝒳 Spec κ(p) above t. So the value depends on neither choice.

Both sides are computed on one smooth chart of 𝒯 above t by AlgebraicGeometry.Stack.relativeStackDimensionAt_eq_dimensionSubNat_of_isSmooth and AlgebraicGeometry.Stack.dimensionAtPoint_eq_dimensionSubNat_of_isTwoFibreProduct_fieldFibre, and the chart exists by AlgebraicGeometry.Stack.exists_isSmooth_algebraicSpaceStack_hom_pointsMap_eq.

theorem relativeStackDimensionAt_eq_fieldFibreStackDimensionAt
    (f : 𝒯 ⟶ 𝒳) (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (h𝒯 : IsLocallyNoetherianStack.{u, w} B S hS 𝒯)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (t : points B S hS 𝒯.val.val 𝒯.val.property)
    (p : FieldValuedPoint B S hS 𝒳.val.val)
    (q : points B S hS (fieldFibreStackSquare B S hS f p).pt.val.val
      (fieldFibreStackSquare B S hS f p).pt.val.property)
    (hp : pointClass B S hS 𝒳.val.val 𝒳.val.property p =
      pointsMap B S hS 𝒯.val.val 𝒯.val.property 𝒳.val.property f.hom.hom t)
    (hq : pointsMap B S hS (fieldFibreStackSquare B S hS f p).pt.val.val
      (fieldFibreStackSquare B S hS f p).pt.val.property 𝒯.val.property
      (fieldFibreStackSquare B S hS f p).snd.hom.hom q = t) :
    relativeStackDimensionAt.{u, w} B S hS f hf h𝒯 h𝒳 t =
      fieldFibreStackDimensionAt.{u, w} B S hS f hf p q

AlgebraicGeometry.Stack.relativeStackDimensionAt_eq_fieldFibreStackDimensionAt_of_algebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionStackRepresentable.lean, line 121. The attribute's comment: “the case of a source representable by an algebraic space”.

Let f : T ⟶ 𝒳 be a 1-morphism, locally of finite type, from the algebraic stack of an algebraic space to a locally Noetherian algebraic stack, and let t ∈ |T|. Then the relative dimension of Stacks 0DRL at t is the value of the formula of Stacks 0DRL at every admissible pair of choices — a field-valued point p of 𝒳 representing the image of t and a point q of T ×_𝒳 Spec κ(p) above t. So that value depends on neither choice.

theorem relativeStackDimensionAt_eq_fieldFibreStackDimensionAt_of_algebraicSpace
    (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hT : IsAlgebraicSpace B S hS T)
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (f : algebraicSpaceStack.{u, w} B S hS T hT ⟶ 𝒳)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (h𝒯 : IsLocallyNoetherianStack.{u, w} B S hS (algebraicSpaceStack.{u, w} B S hS T hT))
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (t : points B S hS (fibredCategory B S hS T).val (fibredCategory B S hS T).property)
    (p : FieldValuedPoint B S hS 𝒳.val.val)
    (q : points B S hS (fieldFibreStackSquare B S hS f p).pt.val.val
      (fieldFibreStackSquare B S hS f p).pt.val.property)
    (hp : pointClass B S hS 𝒳.val.val 𝒳.val.property p =
      pointsMap B S hS (fibredCategory B S hS T).val (fibredCategory B S hS T).property
        𝒳.val.property f.hom.hom t)
    (hq : pointsMap B S hS (fieldFibreStackSquare B S hS f p).pt.val.val
      (fieldFibreStackSquare B S hS f p).pt.val.property
      (fibredCategory B S hS T).property
      (fieldFibreStackSquare B S hS f p).snd.hom.hom q = t) :
    relativeStackDimensionAt.{u, w} B S hS f hf h𝒯 h𝒳 t =
      fieldFibreStackDimensionAt.{u, w} B S hS f hf p q

Tag 0DRN, a lemma

Tag 0DRN in the Stacks Project.

AlgebraicGeometry.Stack.relativeStackDimensionAt_fst_eq_relativeStackDimensionAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionStackBaseChange.lean, line 696.

Stacks 0DRN. Let

  𝒯' ⟶ 𝒯
  |      |
  v      v
  𝒳' ⟶ 𝒳

be a Cartesian square of 1-morphisms of locally Noetherian algebraic stacks over S in which the vertical 1-morphisms are locally of finite type. If t' ∈ |𝒯'| has images t, x' and x in |𝒯|, |𝒳'| and |𝒳|, then dim_{t'}(𝒯'_{x'}) = dim_t(𝒯_x).

Both sides are infima of sets of values of the formula of Stacks 0DRL, and the chart formula AlgebraicGeometry.Stack.dimensionAtPoint_eq_dimensionSubNat_of_isTwoFibreProduct_fieldFibre evaluates every member of either set at one and the same smooth chart U ⟶ 𝒯 of 𝒯 above t: the fibre 𝒯' ×_{𝒳'} Spec κ(p') over a field-valued point p' of 𝒳' is, pasted with the Cartesian square and reindexed along AlgebraicGeometry.Stack.fieldValuedPointMorphism_comp_iso, a 2-fibre product of the vertical 1-morphism 𝒯 ⟶ 𝒳 with the 1-morphism of the image field-valued point of 𝒳. So no field-valued point of 𝒳 has to be lifted to 𝒳', which is what the source's one-line proof elides.

theorem relativeStackDimensionAt_fst_eq_relativeStackDimensionAt
    {𝒳' 𝒯 𝒳 : AlgebraicStacks.{u, w} B S hS} (g : 𝒳' ⟶ 𝒳) (f : 𝒯 ⟶ 𝒳)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (hfst : AlgebraicStacks.IsLocallyOfFiniteType B S hS P.fst)
    (h𝒯' : IsLocallyNoetherianStack.{u, w} B S hS P.pt)
    (h𝒯 : IsLocallyNoetherianStack.{u, w} B S hS 𝒯)
    (h𝒳' : IsLocallyNoetherianStack.{u, w} B S hS 𝒳')
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (t' : points B S hS P.pt.val.val P.pt.val.property) :
    relativeStackDimensionAt.{u, w} B S hS P.fst hfst h𝒯' h𝒳' t' =
      relativeStackDimensionAt.{u, w} B S hS f hf h𝒯 h𝒳
        (pointsMap B S hS P.pt.val.val P.pt.val.property 𝒯.val.property P.snd.hom.hom t')

Tag 0DRP, a lemma

Tag 0DRP in the Stacks Project.

AlgebraicGeometry.Stack.dimensionAtPoint_eq_add_relativeStackDimensionAt_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionSmoothStacks.lean, line 84.

If f : 𝒰 ⟶ 𝒳 is a smooth 1-morphism, locally of finite type, of locally Noetherian algebraic stacks over S and u ∈ |𝒰| has image x ∈ |𝒳|, then dim_u(𝒰) = dim_x(𝒳) + dim_u(𝒰_x), the relative dimension being that of Stacks 0DRL and the two dimensions those of Stacks 0AFN.

theorem dimensionAtPoint_eq_add_relativeStackDimensionAt_of_isSmooth
    {𝒰 𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒰 ⟶ 𝒳)
    (hsm : AlgebraicStacks.IsSmooth B S hS f)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (h𝒰 : IsLocallyNoetherianStack.{u, w} B S hS 𝒰)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (u : points B S hS 𝒰.val.val 𝒰.val.property) :
    dimensionAtPoint B S hS 𝒰 h𝒰 u =
      dimensionAtPoint B S hS 𝒳 h𝒳
          (pointsMap B S hS 𝒰.val.val 𝒰.val.property 𝒳.val.property f.hom.hom u) +
        relativeStackDimensionAt.{u, w} B S hS f hf h𝒰 h𝒳 u

AlgebraicGeometry.Stack.dimensionAtPoint_eq_dimensionAtPoint_add_relativeStackDimensionAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionSmoothStacks.lean, line 126.

If f : 𝒰 ⟶ 𝒳 is a smooth 1-morphism of locally Noetherian algebraic stacks over S and u ∈ |𝒰| has image x ∈ |𝒳|, then dim_u(𝒰) = dim_x(𝒳) + dim_u(𝒰_x), the relative dimension being that of Stacks 0DRL and the two dimensions those of Stacks 0AFN. Local finite type of f, which the relative dimension takes as an argument, is derived from smoothness by AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_of_isSmooth.

theorem dimensionAtPoint_eq_dimensionAtPoint_add_relativeStackDimensionAt
    {𝒰 𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒰 ⟶ 𝒳)
    (hsm : AlgebraicStacks.IsSmooth B S hS f)
    (h𝒰 : IsLocallyNoetherianStack.{u, w} B S hS 𝒰)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (u : points B S hS 𝒰.val.val 𝒰.val.property) :
    dimensionAtPoint B S hS 𝒰 h𝒰 u =
      dimensionAtPoint B S hS 𝒳 h𝒳
          (pointsMap B S hS 𝒰.val.val 𝒰.val.property 𝒳.val.property f.hom.hom u) +
        relativeStackDimensionAt.{u, w} B S hS f
          (AlgebraicStacks.isLocallyOfFiniteType_of_isSmooth B S hS f hsm) h𝒰 h𝒳 u

Tag 0DRQ, a lemma

Tag 0DRQ in the Stacks Project.

AlgebraicGeometry.Stack.isOpen_setOf_relativeDimensionAt_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionLocalConstancy.lean, line 146. The attribute's comment: “part (1) for a morphism of algebraic spaces”.

For a morphism g : T ⟶ G of algebraic spaces over S which is locally of finite type, the locus of points of |T| at which the fibre dimension dim_t(T_{g(t)}) of Stacks 0DRG is at most n is open.

theorem isOpen_setOf_relativeDimensionAt_le
    {T G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hT : IsAlgebraicSpace B S hS T) (hG : IsAlgebraicSpace B S hS G) (g : T ⟶ G)
    (hg : Space.IsLocallyOfFiniteType B S hS g)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS
      (algebraicSpaceStackMap.{u, w} B S hS hT hG g))
    (n : ℕ) :
    IsOpen {t : Space.points B S hS T |
      relativeDimensionAt.{u, w} B S hS T hT (algebraicSpaceStack.{u, w} B S hS G hG)
        (algebraicSpaceStackMap.{u, w} B S hS hT hG g) hf t ≤ (n : WithBot ℕ∞)}

AlgebraicGeometry.Stack.isLocallyConstant_relativeDimensionAt_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionLocalConstancy.lean, line 176. The attribute's comment: “part (2) for a morphism of algebraic spaces”. References: EGA IV (17.10.2), “more general”.

For a smooth morphism g : T ⟶ G of algebraic spaces over S, the fibre dimension t ↦ dim_t(T_{g(t)}) of Stacks 0DRG is locally constant on |T|.

theorem isLocallyConstant_relativeDimensionAt_of_isSmooth
    {T G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hT : IsAlgebraicSpace B S hS T) (hG : IsAlgebraicSpace B S hS G) (g : T ⟶ G)
    (hg : Space.IsSmooth B S hS g) :
    IsLocallyConstant
      (relativeDimensionAt.{u, w} B S hS T hT (algebraicSpaceStack.{u, w} B S hS G hG)
        (algebraicSpaceStackMap.{u, w} B S hS hT hG g)
        (isLocallyOfFiniteType_algebraicSpaceStackMap_of_isSmooth.{u, w} B S hS hT hG g hg))

AlgebraicGeometry.Stack.upperSemicontinuous_relativeStackDimensionAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionStackLocalConstancy.lean, line 447. The attribute's comment: “part (1)”.

For a locally-of-finite-type 1-morphism f : 𝒯 ⟶ 𝒳 of locally Noetherian algebraic stacks, the function t ↦ dim_t(𝒯_{f(t)}) of Stacks 0DRL is upper semi-continuous on |𝒯|.

theorem upperSemicontinuous_relativeStackDimensionAt :
    UpperSemicontinuous (relativeStackDimensionAt.{u, w} B S hS f hf h𝒯 h𝒳)

AlgebraicGeometry.Stack.isLocallyConstant_relativeStackDimensionAt_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionStackLocalConstancy.lean, line 463. The attribute's comment: “part (2)”. References: EGA IV (17.10.2), “special case”.

For a smooth 1-morphism f : 𝒯 ⟶ 𝒳 of locally Noetherian algebraic stacks, the function t ↦ dim_t(𝒯_{f(t)}) of Stacks 0DRL is locally constant on |𝒯|.

theorem isLocallyConstant_relativeStackDimensionAt_of_isSmooth
    (hfsm : AlgebraicStacks.IsSmooth B S hS f) :
    IsLocallyConstant (relativeStackDimensionAt.{u, w} B S hS f hf h𝒯 h𝒳)

AlgebraicGeometry.Stack.isOpen_setOf_relativeStackDimension_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionStackUpperSemicontinuous.lean, line 261. The attribute's comment: “part (1), as openness of the sublevel sets”.

Let f : 𝒯 ⟶ 𝒳 be a locally-of-finite-type 1-morphism of algebraic stacks over S. Then every sublevel set of the function t ↦ dim_t(𝒯_{f(t)}) of Stacks 0DRL is open in |𝒯|.

theorem isOpen_setOf_relativeStackDimension_le (c : EInt) :
    IsOpen {t : points B S hS 𝒯.val.val 𝒯.val.property |
      relativeStackDimension.{u, w} B S hS f hf t ≤ c}

AlgebraicGeometry.Stack.upperSemicontinuous_relativeStackDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionStackUpperSemicontinuous.lean, line 325. The attribute's comment: “part (1)”.

For a locally-of-finite-type 1-morphism f : 𝒯 ⟶ 𝒳 of algebraic stacks, the function t ↦ dim_t(𝒯_{f(t)}) of Stacks 0DRL is upper semi-continuous on |𝒯|.

theorem upperSemicontinuous_relativeStackDimension :
    UpperSemicontinuous (relativeStackDimension.{u, w} B S hS f hf)

AlgebraicGeometry.Stack.isLocallyConstant_relativeStackDimension_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDimensionStackUpperSemicontinuous.lean, line 335. The attribute's comment: “part (2)”. References: EGA IV (17.10.2), “more general”.

For a smooth, locally-of-finite-type 1-morphism f : 𝒯 ⟶ 𝒳 of algebraic stacks, the function t ↦ dim_t(𝒯_{f(t)}) of Stacks 0DRL is locally constant on |𝒯|.

theorem isLocallyConstant_relativeStackDimension_of_isSmooth
    (hfsm : AlgebraicStacks.IsSmooth B S hS f) :
    IsLocallyConstant (relativeStackDimension.{u, w} B S hS f hf)

Tag 0DRR, a lemma

Tag 0DRR in the Stacks Project.

AlgebraicGeometry.exists_isClosed_isFiniteTypePoint_dim_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Exercises/NonExercises/DimensionFiniteTypePoint.lean, line 81.

A finite-dimensional scheme has a closed finite type point at which its local dimension equals its dimension.

theorem exists_isClosed_isFiniteTypePoint_dim_eq
    (X : Scheme.{u}) (d : ℕ) (hX : topologicalKrullDim X = d) :
    ∃ x : X, IsClosed ({x} : Set X) ∧
      IsFiniteTypePoint x ∧
      topologicalKrullDimAt X x = topologicalKrullDim X

Tag 0DRT, a lemma

Tag 0DRT in the Stacks Project.

AlgebraicGeometry.topologicalKrullDim_eq_of_isOpen_of_catenary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/ConstancyOfDimension.lean, line 227. The attribute's comment: “dimension of nonempty opens”. References: SGA 3 VIB (1.5), “more general”.

A nonempty open subset of an irreducible, Jacobson, catenary, locally Noetherian scheme of finite dimension has the same dimension as the scheme.

theorem topologicalKrullDim_eq_of_isOpen_of_catenary
    (X : Scheme.{u}) [IrreducibleSpace X] [JacobsonSpace X]
    (hcat : IrreducibleClosedsCodim.IsCatenarySpace X) [IsLocallyNoetherian X]
    (d : ℕ) (hX : topologicalKrullDim X = d)
    (U : Set X) (hU : IsOpen U) (hne : U.Nonempty) :
    topologicalKrullDim X = topologicalKrullDim U

AlgebraicGeometry.isConstant_topologicalKrullDimAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/ConstancyOfDimension.lean, line 241. The attribute's comment: “constancy of local dimension”.

On an irreducible, Jacobson, catenary, locally Noetherian scheme of finite dimension, the local Krull dimension is constant.

theorem isConstant_topologicalKrullDimAt
    (X : Scheme.{u}) [IrreducibleSpace X] [JacobsonSpace X]
    (hcat : IrreducibleClosedsCodim.IsCatenarySpace X) [IsLocallyNoetherian X]
    (d : ℕ) (hX : topologicalKrullDim X = d) :
    ∀ x y : X, topologicalKrullDimAt X x = topologicalKrullDimAt X y

Tag 0DRU, a definition

Tag 0DRU in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsPseudoCatenary, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PseudoCatenaryAlgebraicStack.lean, line 57.

Stacks 0DRU. An algebraic stack over S is pseudo-catenary when it admits a smooth surjective 1-morphism from a scheme of the big fppf site over S whose underlying scheme is locally Noetherian and universally catenary.

abbrev IsPseudoCatenary (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) : Prop

Tag 0DRV, an example

Tag 0DRV in the Stacks Project.

AlgebraicGeometry.Stack.isPseudoCatenary_of_isLocallyOfFiniteType_over_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PseudoCatenary.lean, line 226.

Stacks 0DRV. An algebraic stack locally of finite type over a locally Noetherian universally catenary scheme S is pseudo-catenary.

Any smooth surjective scheme atlas serves as the witness, its source being universally catenary by AlgebraicGeometry.Stack.isUniversallyCatenary_of_isSmooth_schemeStack.

theorem isPseudoCatenary_of_isLocallyOfFiniteType_over_scheme [IsLocallyNoetherian S]
    (hcat : Scheme.IsUniversallyCatenary S) (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : AlgebraicStacks.IsLocallyOfFiniteType B S hS (structureMorphism B S hS 𝒳)) :
    AlgebraicStacks.IsPseudoCatenary B S hS 𝒳

Tag 0DRW, a lemma

Tag 0DRW in the Stacks Project.

AlgebraicGeometry.Stack.isPseudoCatenary_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PseudoCatenary.lean, line 242.

Stacks 0DRW. The source of a 1-morphism of algebraic stacks over S which is locally of finite type and whose target is pseudo-catenary is pseudo-catenary.

For a universally catenary smooth surjective scheme atlas U ⟶ 𝒳 and a smooth surjective scheme atlas V ⟶ 𝒴 ×_𝒳 U, the composite V ⟶ 𝒴 ×_𝒳 U ⟶ 𝒴 is smooth and surjective while V ⟶ 𝒴 ×_𝒳 U ⟶ U is locally of finite type, so V is universally catenary by Stacks 02J9.

theorem isPseudoCatenary_of_isLocallyOfFiniteType {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒴 ⟶ 𝒳) (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (h𝒳 : AlgebraicStacks.IsPseudoCatenary B S hS 𝒳) :
    AlgebraicStacks.IsPseudoCatenary B S hS 𝒴

Tag 0DRX, a lemma

Tag 0DRX in the Stacks Project.

AlgebraicGeometry.Stack.isConstant_dimensionAtPoint_of_irreducibleSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ConstancyOfStackDimension.lean, line 457.

Stacks 0DRX. On a Jacobson, pseudo-catenary, locally Noetherian algebraic stack 𝒳 over S whose space of points |𝒳| is irreducible, the dimension dim_x(𝒳) of Stacks 0AFN is the same at every point of |𝒳|.

Pseudo-catenarity (Stacks 0DRU) provides a smooth surjective 1-morphism from the algebraic stack of a scheme U of the site which is locally Noetherian and universally catenary; U is then catenary, and Jacobson by the universal scheme criterion of Stacks 04YF. The dimension formula of Stacks 0DRJ holds along that chart, read as a chart by the algebraic space U represents, and the relative dimension occurring in it is locally constant by Stacks 0DRQ (2). Around each point of U the local dimension of U is then the dimension of a nonempty open irreducible subset, by Stacks 0DRT at the irreducible components, so dim_x(𝒳) takes on the image of that subset the single value it has at the given point; two such images meet in |𝒳|, which is irreducible, and that common point identifies any two values.

theorem isConstant_dimensionAtPoint_of_irreducibleSpace (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (h𝒳Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒳)
    (h𝒳Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒳)
    (h𝒳Irreducible : @IrreducibleSpace _ (pointTopology B S hS 𝒳.val)) :
    ∀ x y : points B S hS 𝒳.val.val 𝒳.val.property,
      dimensionAtPoint B S hS 𝒳 h𝒳 x = dimensionAtPoint B S hS 𝒳 h𝒳 y

Tag 0DRY, a lemma

Tag 0DRY in the Stacks Project.

AlgebraicGeometry.Stack.dimensionAtPoint_le_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionClosedImmersion.lean, line 138.

If i : 𝒵 ⟶ 𝒳 is a closed immersion of locally Noetherian algebraic stacks over S and z ∈ |𝒵| has image x ∈ |𝒳|, then dim_z(𝒵) ≤ dim_x(𝒳), the dimensions being those of Stacks 0AFN.

theorem dimensionAtPoint_le_of_isClosedImmersion
    {𝒵 𝒳 : AlgebraicStacks.{u, w} B S hS} (i : 𝒵 ⟶ 𝒳)
    (hi : AlgebraicStacks.IsClosedImmersion B S hS i)
    (h𝒵 : IsLocallyNoetherianStack.{u, w} B S hS 𝒵)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (z : points B S hS 𝒵.val.val 𝒵.val.property) :
    dimensionAtPoint B S hS 𝒵 h𝒵 z ≤
      dimensionAtPoint B S hS 𝒳 h𝒳
        (pointsMap B S hS 𝒵.val.val 𝒵.val.property 𝒳.val.property i.hom.hom z)

Tag 0DRZ, a lemma

Tag 0DRZ in the Stacks Project.

AlgebraicGeometry.Stack.dimensionAtPoint_eq_sSup_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionIrreducibleComponentsSupremum.lean, line 399.

Stacks 0DRZ. For a locally Noetherian algebraic stack 𝒳 over S and a point x ∈ |𝒳|, the dimension of Stacks 0AFN at x is the supremum of the dimensions at x of the irreducible components of |𝒳| through x, each endowed with its induced reduced structure:

dim_x(𝒳) = sup_𝒯 dim_x(𝒯).

The inequality sup_𝒯 dim_x(𝒯) ≤ dim_x(𝒳) is Stacks 0DRY (AlgebraicGeometry.Stack.sSup_componentDimensionsAt_le). For the reverse inequality, the source's equation Stacks 0DS0, choose a smooth surjective chart f : U ⟶ 𝒳 by a scheme and a point u over x; some irreducible component T' of U through u has dim_u(T') = dim_u(U) (AlgebraicGeometry.Stack.exists_mem_irreducibleComponents_topologicalKrullDimAt_eq_of_isSmooth). The closure T of its image is an irreducible component of |𝒳| through x (Stacks 0DR5), and it carries a reduced closed substack 𝒯 with |𝒯| = T (the existence half of Stacks 0509, AlgebraicGeometry.Stack.exists_isClosedSubstack_isReducedStack_range_pointsMap_eq). Then AlgebraicGeometry.Stack.exists_dimensionAtPoint_le_of_isClosedImmersion_of_image_subset, applied to A = T', produces a point of 𝒯 over x at which dim_x(𝒳) ≤ dim(𝒯).

theorem dimensionAtPoint_eq_sSup_irreducibleComponents (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (x : points B S hS 𝒳.val.val 𝒳.val.property) :
    dimensionAtPoint B S hS 𝒳 h𝒳 x = sSup (componentDimensionsAt B S hS 𝒳 x)

Tag 0DS1, a lemma

Tag 0DS1 in the Stacks Project.

AlgebraicGeometry.Stack.exists_isFiniteTypePoint_mem_pointSet_dimensionAtPoint_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionAtFiniteTypePoint.lean, line 469.

Stacks 0DS1. Let 𝒳 be a locally Noetherian algebraic stack over S, let 𝒱 be an open substack of 𝒳 and let x ∈ |𝒱|. Then there is a finite type point x₀ ∈ |𝒱| — a finite type point both of 𝒱 and of 𝒳 — with dim_{x₀}(𝒳) = dim_x(𝒱).

The point x of |𝒳| lying in |𝒱| is given as a point of |𝒱|, which is what membership in AlgebraicGeometry.Stack.OpenSubstack.pointSet says, and dim_x(𝒱) is the dimension of Stacks 0AFN of the open substack read as an algebraic stack; that it is locally Noetherian is Stacks 0CPM, AlgebraicGeometry.Stack.isLocallyNoetherianStack_toAlgebraicStack.

The source reduces to a smooth chart of 𝒱 and performs two shrinkings there, which is AlgebraicGeometry.Stack.exists_isFiniteTypePoint_dimensionAtPoint_eq applied to 𝒱. What remains is to pass from 𝒱 back to 𝒳: the inclusion of an open substack is locally of finite type, so it carries finite type points to finite type points (Stacks 06G0), and it leaves the dimension of Stacks 0AFN unchanged, which is AlgebraicGeometry.Stack.dimensionAtPoint_pointsMap_eq_of_isOpenImmersion.

theorem exists_isFiniteTypePoint_mem_pointSet_dimensionAtPoint_eq
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (𝒱 : OpenSubstack 𝒳)
    (x : points B S hS
      (fullSubcategoryAlgebraicStack 𝒳 𝒱.property 𝒱.isAlgebraic).val.val
      (fullSubcategoryAlgebraicStack 𝒳 𝒱.property 𝒱.isAlgebraic).val.property) :
    ∃ x₀ : points B S hS
        (fullSubcategoryAlgebraicStack 𝒳 𝒱.property 𝒱.isAlgebraic).val.val
        (fullSubcategoryAlgebraicStack 𝒳 𝒱.property 𝒱.isAlgebraic).val.property,
      IsFiniteTypePoint.{u, w} B S hS
          (fullSubcategoryAlgebraicStack 𝒳 𝒱.property 𝒱.isAlgebraic) x₀ ∧
        IsFiniteTypePoint.{u, w} B S hS 𝒳
            (AlgebraicStacks.pointsMap B S hS 𝒱.inclusion x₀) ∧
          AlgebraicStacks.pointsMap B S hS 𝒱.inclusion x₀ ∈ 𝒱.pointSet B S hS ∧
            dimensionAtPoint B S hS 𝒳 h𝒳
                (AlgebraicStacks.pointsMap B S hS 𝒱.inclusion x₀) =
              dimensionAtPoint B S hS
                (fullSubcategoryAlgebraicStack 𝒳 𝒱.property 𝒱.isAlgebraic)
                (isLocallyNoetherianStack_toAlgebraicStack B S hS 𝒱 h𝒳) x

Tag 0DS2, a lemma

Tag 0DS2 in the Stacks Project.

AlgebraicGeometry.Stack.exists_openSubstack_isOpenImmersion_subset_irreducibleComponent', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismGenericOpenImmersion.lean, line 289.

Stacks 0DS2 (Morphisms of Algebraic Stacks, Lemma 107.5.21), with every input discharged. Let m : 𝒯 ⟶ 𝒳 be a monomorphism of algebraic stacks over S which is locally of finite type, with 𝒳 Jacobson, pseudo-catenary and locally Noetherian, with |𝒯| irreducible and 𝒯 of dimension d in the sense of Stacks 0AFP, and with 𝒳 reduced of dimension at most d. Then there is a non-empty open substack 𝒱 of 𝒯, in the sense of Stacks 04YM, such that 𝒱 ⟶ 𝒳 is an open immersion identifying 𝒱 with an open subset of an irreducible component of |𝒳|: its range on points lies in an irreducible component Z and is open in |𝒳|, hence open in the subspace Z, and the open immersion makes |𝒱| → |𝒳| a homeomorphism onto that range.

The source derives the Jacobson, pseudo-catenary and locally Noetherian properties of 𝒯 from those of 𝒳; of these only local Noetherianity is needed, and only so that the dimension of 𝒯 is defined, and it is supplied in the statement of h𝒯dim by Stacks 06R6 rather than assumed.

The dimension hypotheses enter the proof only through the chart-level conclusion AlgebraicGeometry.Stack.exists_chart_openSubspace_isSmooth: the source's argument on a smooth surjective chart U ⟶ 𝒳 by a reduced algebraic space, its base change U' = 𝒯 ×_𝒳 U, and the étale-local structure of the unramified monomorphism U' ⟶ U, concludes that some non-empty open W ⊆ U' has W ⟶ U étale and hence W ⟶ 𝒳 smooth. The module's "The chart" says where that is proved.

The rest, and the content of this module, is the source's last step. Stacks 05UP turns the smooth 1-morphism W ⟶ 𝒯 into the open substack 𝒱 of 𝒯 covered by |W| with a smooth surjective factorization q : W ⟶ 𝒱 satisfying q ≫ 𝒱.inclusion = W ⟶ 𝒯; since q ≫ (𝒱.inclusion ≫ m) is the smooth 1-morphism W ⟶ 𝒳, source-side cancellation of smoothness along q gives 𝒱.inclusion ≫ m smooth, and Stacks 04ZY makes it a monomorphism. A smooth monomorphism of algebraic stacks is an open immersion. Finally |𝒱| is a non-empty open subset of the irreducible |𝒯|, hence irreducible, so its continuous image in |𝒳| is irreducible and lies in an irreducible component, and that image is open because 𝒱 ⟶ 𝒳 is smooth.

theorem exists_openSubstack_isOpenImmersion_subset_irreducibleComponent'
    {𝒯 𝒳 : AlgebraicStacks.{u, w} B S hS} (m : 𝒯 ⟶ 𝒳)
    (hmono : AlgebraicStacks.IsMonomorphism B S hS m)
    (hft : AlgebraicStacks.IsLocallyOfFiniteType B S hS m)
    (h𝒳Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒳)
    (h𝒳Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒳)
    (h𝒳N : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (h𝒯Irreducible : @IrreducibleSpace _ (pointTopology B S hS 𝒯.val))
    (d : ℕ) (h𝒯dim : dimension B S hS 𝒯
      (AlgebraicStacks.isLocallyNoetherian_of_isLocallyOfFiniteType.{u, w} B S hS m hft h𝒳N) =
      ((d : ℤ) : EInt))
    (h𝒳red : IsReducedStack B S hS 𝒳)
    (h𝒳dim : dimension B S hS 𝒳 h𝒳N ≤ ((d : ℤ) : EInt)) :
    ∃ 𝒱 : OpenSubstack 𝒯, (𝒱.pointSet B S hS).Nonempty ∧
      AlgebraicStacks.IsOpenImmersion B S hS (𝒱.inclusion ≫ m) ∧
        ∃ Z ∈ @irreducibleComponents _ (pointTopology B S hS 𝒳.val),
          Set.range (AlgebraicStacks.pointsMap B S hS (𝒱.inclusion ≫ m)) ⊆ Z ∧
            @IsOpen _ (pointTopology B S hS 𝒳.val)
              (Set.range (AlgebraicStacks.pointsMap B S hS (𝒱.inclusion ≫ m)))

Tag 0DS4, a lemma

Tag 0DS4 in the Stacks Project.

AlgebraicGeometry.Stack.dimension_le_closedSubstackDimension_add_relativeStackDimensionAt_of_isQuasiCompactMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionSchemeTheoreticImage.lean, line 980. The attribute's comment: “the inequality at every point of 𝒯, for f quasi-compact as in the statement”.

The inequality of Stacks 0DS4 for a quasi-compact 1-morphism. Under the hypotheses of exists_isOpen_dimension_eq_add_relativeStackDimensionAt_of_isQuasiCompactMorphism, dim(𝒯) ≤ dim(𝒵) + dim_t(𝒯_{f(t)}) at every t ∈ |𝒯|.

The generic equality implies it, by AlgebraicGeometry.Stack.dimension_le_add_relativeStackDimensionAt_of_exists_isOpen — the upper semi-continuity of Stacks 0DRQ (1) together with the constancy of Stacks 0DRX.

theorem dimension_le_closedSubstackDimension_add_relativeStackDimensionAt_of_isQuasiCompactMorphism
    {𝒯 𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒯 ⟶ 𝒳)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (hfQC : IsQuasiCompactMorphism B S hS f)
    (h𝒯 : IsLocallyNoetherianStack.{u, w} B S hS 𝒯)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (h𝒯Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒯)
    (h𝒳Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒳)
    (h𝒯Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒯)
    (h𝒳Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒳)
    (h𝒯Irreducible : @IrreducibleSpace _ (pointTopology B S hS 𝒯.val))
    (_h𝒳QuasiSeparated : IsQuasiSeparatedAbs.{u, w, w} B S hS 𝒳)
    {P : ObjectProperty 𝒳.val.val.obj} (hP : IsSchemeTheoreticImage f P)
    (t : points B S hS 𝒯.val.val 𝒯.val.property) :
    dimension B S hS 𝒯 h𝒯 ≤
      closedSubstackDimension B S hS 𝒳 P hP.1 hP.isAlgebraicStack h𝒳 +
        relativeStackDimensionAt.{u, w} B S hS f hf h𝒯 h𝒳 t

AlgebraicGeometry.Stack.dimension_le_add_and_exists_isOpen_dense_eq_add_relativeStackDimensionAt_of_isQuasiCompactMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionSchemeTheoreticImage.lean, line 1010. The attribute's comment: “both clauses: the inequality at every point and the equality on a dense open subset, for f quasi-compact as in the statement”.

The content of Stacks 0DS4 for a quasi-compact 1-morphism. Let f : 𝒯 ⟶ 𝒳 be a quasi-compact 1-morphism locally of finite type of Jacobson, pseudo-catenary, locally Noetherian algebraic stacks over S with |𝒯| irreducible and 𝒳 quasi-separated, and let P cut out the scheme theoretic image 𝒵 of Stacks 0CMI. Then dim(𝒯) ≤ dim(𝒵) + dim_t(𝒯_{f(t)}) at every t ∈ |𝒯|, and equality holds on an open subset of |𝒯| that is nonempty, equivalently dense, |𝒯| being irreducible.

theorem
  dimension_le_add_and_exists_isOpen_dense_eq_add_relativeStackDimensionAt_of_isQuasiCompactMorphism
    {𝒯 𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒯 ⟶ 𝒳)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (hfQC : IsQuasiCompactMorphism B S hS f)
    (h𝒯 : IsLocallyNoetherianStack.{u, w} B S hS 𝒯)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (h𝒯Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒯)
    (h𝒳Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒳)
    (h𝒯Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒯)
    (h𝒳Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒳)
    (h𝒯Irreducible : @IrreducibleSpace _ (pointTopology B S hS 𝒯.val))
    (h𝒳QuasiSeparated : IsQuasiSeparatedAbs.{u, w, w} B S hS 𝒳)
    {P : ObjectProperty 𝒳.val.val.obj} (hP : IsSchemeTheoreticImage f P) :
    (∀ t : points B S hS 𝒯.val.val 𝒯.val.property,
        dimension B S hS 𝒯 h𝒯 ≤
          closedSubstackDimension B S hS 𝒳 P hP.1 hP.isAlgebraicStack h𝒳 +
            relativeStackDimensionAt.{u, w} B S hS f hf h𝒯 h𝒳 t) ∧
      ∃ W : Set (points B S hS 𝒯.val.val 𝒯.val.property),
        @IsOpen _ (pointTopology B S hS 𝒯.val) W ∧ W.Nonempty ∧
          @Dense _ (pointTopology B S hS 𝒯.val) W ∧
          ∀ t ∈ W, dimension B S hS 𝒯 h𝒯 =
            closedSubstackDimension B S hS 𝒳 P hP.1 hP.isAlgebraicStack h𝒳 +
              relativeStackDimensionAt.{u, w} B S hS f hf h𝒯 h𝒳 t

AlgebraicGeometry.Stack.forall_dimension_le_closedSubstackDimension_add_relativeStackDimensionAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionSchemeTheoreticImageInequality.lean, line 122. The attribute's comment: “the inequality clause, for every f (no quasi-compactness), under the hypotheses of the statement in the Stacks Project other than quasi-compactness of f. The equality clause needs f quasi-compact and is registered on AlgebraicGeometry.Stack.dimension_le_add_and_exists_isOpen_dense_eq_add_relativeStackDimensionAt_of_isQuasiCompactMorphism; without quasi-compactness it is refuted by AlgebraicGeometry.Stack.not_forall_dimension_le_add_and_exists_isOpen_dense_eq”.

The inequality clause of Stacks 0DS4, for every 1-morphism. Let f : 𝒯 ⟶ 𝒳 be a 1-morphism locally of finite type of Jacobson, pseudo-catenary, locally Noetherian algebraic stacks over S, with |𝒯| irreducible and 𝒳 quasi-separated, and let P cut out the scheme theoretic image 𝒵 of f (Stacks 0CMI). Then dim(𝒯) ≤ dim(𝒵) + dim_t(𝒯_{f(t)}) for every t ∈ |𝒯|, i.e. dim_t(𝒯_{f(t)}) ≥ dim(𝒯) - dim(𝒵).

No quasi-compactness of f is asked. A nonempty quasi-compact open substack 𝒰 of 𝒯 exists by AlgebraicGeometry.Stack.exists_isOpenImmersion_isQuasiCompactStack_nonempty (through Stacks 05UP); the restriction of f to it is quasi-compact by Stacks 075S, part (1), the target being quasi-separated; and dimension_le_closedSubstackDimension_add_relativeStackDimensionAt_of_quasiCompactRestriction concludes.

theorem forall_dimension_le_closedSubstackDimension_add_relativeStackDimensionAt
    {𝒯 𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒯 ⟶ 𝒳)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (h𝒯 : IsLocallyNoetherianStack.{u, w} B S hS 𝒯)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (h𝒯Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒯)
    (h𝒳Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒳)
    (h𝒯Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒯)
    (h𝒳Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒳)
    (h𝒯Irreducible : @IrreducibleSpace _ (pointTopology B S hS 𝒯.val))
    (h𝒳QuasiSeparated : IsQuasiSeparatedAbs.{u, w, w} B S hS 𝒳)
    {P : ObjectProperty 𝒳.val.val.obj} (hP : IsSchemeTheoreticImage f P) :
    ∀ t : points B S hS 𝒯.val.val 𝒯.val.property,
      dimension B S hS 𝒯 h𝒯 ≤
        closedSubstackDimension B S hS 𝒳 P hP.1 hP.isAlgebraicStack h𝒳 +
          relativeStackDimensionAt.{u, w} B S hS f hf h𝒯 h𝒳 t

Tag 0DS5, a remark

Tag 0DS5 in the Stacks Project.

AlgebraicGeometry.Stack.classifyingStack_multiplicativeGroup_dimension_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ClassifyingStackMultiplicativeGroupExample.lean, line 307. The attribute's comment: “the example [Spec k/G_m] → Spec k: it need not be that dim T ≥ dim Z, the fibres having negative dimension”.

Stacks 0DS5, the example [Spec k/𝐆_m] ⟶ Spec k. Let k be a field. The classifying stack [Spec k/𝐆_m] is an algebraic stack, of which a model 𝒬 in the 2-category of algebraic stacks over Spec k exists; and for every such model, the structure morphism f : 𝒬 ⟶ Spec k satisfies the hypotheses of Stacks 0DS4 — it is quasi-compact and locally of finite type, 𝒬 and Spec k are Jacobson, pseudo-catenary and locally Noetherian, |𝒬| is irreducible and Spec k is quasi-separated — its scheme theoretic image is all of Spec k, of dimension 0, while dim 𝒬 = -1, so that dim 𝒬 < dim 𝒵; and the fibre dimension dim_t(𝒬_{f(t)}) of Stacks 0DRL is -1 < 0 at every point t of 𝒬.

theorem classifyingStack_multiplicativeGroup_dimension_lt :
    IsAlgebraicStack.{u, w} C (Spec (.of k)) hk
        (classifyingStack C hk (multiplicativeGroupOverField C hk)).val ∧
      (∃ 𝒬 : AlgebraicStacks.{u, w} C (Spec (.of k)) hk, Nonempty
        (StacksRepresentableCFG.EquivalenceOver
          (classifyingStack C hk (multiplicativeGroupOverField C hk)).val.p 𝒬.val.val.p)) ∧
      ∀ (𝒬 : AlgebraicStacks.{u, w} C (Spec (.of k)) hk)
        (_e : StacksRepresentableCFG.EquivalenceOver
          (classifyingStack C hk (multiplicativeGroupOverField C hk)).val.p 𝒬.val.val.p),
        ∃ (h𝒯 : IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk 𝒬)
          (h𝒳 : IsLocallyNoetherianStack.{u, w} C (Spec (.of k)) hk (specFieldStack.{u, w} C hk))
          (hf : AlgebraicStacks.IsLocallyOfFiniteType C (Spec (.of k)) hk (toSpecFieldStack C hk 𝒬))
          (hP : IsSchemeTheoreticImage (toSpecFieldStack C hk 𝒬) ⊤),
          IsQuasiCompactMorphism C (Spec (.of k)) hk (toSpecFieldStack C hk 𝒬) ∧
          AlgebraicStacks.IsJacobson C (Spec (.of k)) hk 𝒬 ∧
          AlgebraicStacks.IsJacobson C (Spec (.of k)) hk (specFieldStack.{u, w} C hk) ∧
          AlgebraicStacks.IsPseudoCatenary C (Spec (.of k)) hk 𝒬 ∧
          AlgebraicStacks.IsPseudoCatenary C (Spec (.of k)) hk (specFieldStack.{u, w} C hk) ∧
          @IrreducibleSpace _ (pointTopology C (Spec (.of k)) hk 𝒬.val) ∧
          IsQuasiSeparatedAbs.{u, w, w} C (Spec (.of k)) hk (specFieldStack.{u, w} C hk) ∧
          closedSubstackDimension C (Spec (.of k)) hk (specFieldStack.{u, w} C hk) ⊤ hP.1
            hP.isAlgebraicStack h𝒳 = 0 ∧
          dimension C (Spec (.of k)) hk 𝒬 h𝒯 = ((-1 : ℤ) : EInt) ∧
          dimension C (Spec (.of k)) hk 𝒬 h𝒯 <
            closedSubstackDimension C (Spec (.of k)) hk (specFieldStack.{u, w} C hk) ⊤ hP.1
              hP.isAlgebraicStack h𝒳 ∧
          ∀ t : points C (Spec (.of k)) hk 𝒬.val.val 𝒬.val.property,
            relativeStackDimensionAt.{u, w} C (Spec (.of k)) hk (toSpecFieldStack C hk 𝒬) hf h𝒯
                h𝒳 t =
              ((-1 : ℤ) : EInt)

AlgebraicGeometry.Stack.isQuasiDMAbs_and_zero_le_dimensionAtPoint_fieldFibreStackSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiDMFibreDimension.lean, line 70. The attribute's comment: “the fibres of a quasi-DM 1-morphism are quasi-DM algebraic stacks, hence of non-negative dimension”.

Let f : 𝒯 ⟶ 𝒳 be a quasi-DM 1-morphism of algebraic stacks over S, locally of finite type, and let p be a field-valued point of 𝒳 with field spectrum Spec k. Then the fibre 𝒯 ×_𝒳 Spec k of f over p is a quasi-DM algebraic stack (Stacks 050D, part (6)), and hence has non-negative dimension at every one of its points; so, when it is nonempty, its dimension of Stacks 0AFP is non-negative.

theorem isQuasiDMAbs_and_zero_le_dimensionAtPoint_fieldFibreStackSquare
    {𝒯 𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒯 ⟶ 𝒳)
    (hqdm : AlgebraicStacks.IsQuasiDM B S hS f)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (p : FieldValuedPoint B S hS 𝒳.val.val) :
    IsQuasiDMAbs.{u, w, w} B S hS (fieldFibreStackSquare B S hS f p).pt ∧
      (∀ x : points B S hS (fieldFibreStackSquare B S hS f p).pt.val.val
          (fieldFibreStackSquare B S hS f p).pt.val.property,
        0 ≤ dimensionAtPoint B S hS (fieldFibreStackSquare B S hS f p).pt
          (isLocallyNoetherianStack_fieldFibreStackSquare.{u, w} B S hS f hf p) x) ∧
      (Nonempty (points B S hS (fieldFibreStackSquare B S hS f p).pt.val.val
          (fieldFibreStackSquare B S hS f p).pt.val.property) →
        0 ≤ dimension B S hS (fieldFibreStackSquare B S hS f p).pt
          (isLocallyNoetherianStack_fieldFibreStackSquare.{u, w} B S hS f hf p))

AlgebraicGeometry.Stack.zero_le_relativeStackDimensionAt_and_closedSubstackDimension_le_dimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiDMFibreDimension.lean, line 96. The attribute's comment: “in the quasi-DM case the lemma implies dim T ≥ dim Z”.

Let f : 𝒯 ⟶ 𝒳 be a quasi-compact, locally of finite type 1-morphism of Jacobson, pseudo-catenary, locally Noetherian algebraic stacks over S, whose source is irreducible and whose target is quasi-separated, and let 𝒵 ↪ 𝒳, cut out by P, be the scheme theoretic image of f — the situation of Stacks 0DS4. If f is moreover quasi-DM, then its fibres have non-negative dimension, dim_t(𝒯_{f(t)}) ≥ 0 at every t ∈ |𝒯|, and Stacks 0DS4 then gives dim 𝒵 ≤ dim 𝒯.

theorem zero_le_relativeStackDimensionAt_and_closedSubstackDimension_le_dimension
    {𝒯 𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒯 ⟶ 𝒳)
    (hfQC : IsQuasiCompactMorphism B S hS f)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (hDM : AlgebraicStacks.IsQuasiDM B S hS f)
    (h𝒯 : IsLocallyNoetherianStack.{u, w} B S hS 𝒯)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (h𝒯Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒯)
    (h𝒳Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒳)
    (h𝒯Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒯)
    (h𝒳Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒳)
    (h𝒯Irreducible : @IrreducibleSpace _ (pointTopology B S hS 𝒯.val))
    (h𝒳QuasiSeparated : IsQuasiSeparatedAbs.{u, w, w} B S hS 𝒳)
    {P : ObjectProperty 𝒳.val.val.obj} (hP : IsSchemeTheoreticImage f P) :
    (∀ t : points B S hS 𝒯.val.val 𝒯.val.property,
        0 ≤ relativeStackDimensionAt B S hS f hf h𝒯 h𝒳 t) ∧
      closedSubstackDimension B S hS 𝒳 P hP.1 hP.isAlgebraicStack h𝒳 ≤
        dimension B S hS 𝒯 h𝒯

Tag 0DS6, a lemma

Tag 0DS6 in the Stacks Project.

AlgebraicGeometry.Stack.closedSubstackDimension_le_dimension_of_isQuasiCompactMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionSchemeTheoreticImage.lean, line 1206. The attribute's comment: “the first clause, dim Z ≤ dim T, under exactly the hypotheses of the source”. References: EGA IV (4.1.2), “(i)”.

The inequality of Stacks 0DS6. For a quasi-compact, locally of finite type, quasi-DM 1-morphism f : 𝒯 ⟶ 𝒳 of Jacobson, pseudo-catenary, locally Noetherian algebraic stacks over S, with |𝒯| irreducible and 𝒳 quasi-separated, and P cutting out the scheme theoretic image 𝒵 of f, one has dim(𝒵) ≤ dim(𝒯).

At a point of the nonempty open subset of |𝒯| on which dim(𝒯) = dim(𝒵) + dim_t(𝒯_{f(t)}) (Stacks 0DS4 for a quasi-compact f), the fibre dimension is non-negative because f is quasi-DM.

theorem closedSubstackDimension_le_dimension_of_isQuasiCompactMorphism
    {𝒯 𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒯 ⟶ 𝒳)
    (hfQC : IsQuasiCompactMorphism B S hS f)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (hDM : AlgebraicStacks.IsQuasiDM B S hS f)
    (h𝒯 : IsLocallyNoetherianStack.{u, w} B S hS 𝒯)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (h𝒯Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒯)
    (h𝒳Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒳)
    (h𝒯Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒯)
    (h𝒳Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒳)
    (h𝒯Irreducible : @IrreducibleSpace _ (pointTopology B S hS 𝒯.val))
    (h𝒳QuasiSeparated : IsQuasiSeparatedAbs.{u, w, w} B S hS 𝒳)
    {P : ObjectProperty 𝒳.val.val.obj} (hP : IsSchemeTheoreticImage f P) :
    closedSubstackDimension B S hS 𝒳 P hP.1 hP.isAlgebraicStack h𝒳 ≤ dimension B S hS 𝒯 h𝒯

AlgebraicGeometry.Stack.closedSubstackDimension_le_dimension_and_xor_relativeDimension_pos_of_ne_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DimensionSchemeTheoreticImage.lean, line 1330. The attribute's comment: “the exactly-one form under the added hypothesis that dim T is finite; erratum: false as written when dim T = dim Z = infinity, machine-checked as AlgebraicGeometry.Stack.not_forall_xor_relativeDimension_pos (the affine line over N<X>, N Nagata's ring; Fujita 1975, Brewer-Heinzer 1980), see the docstring”.

Stacks 0DS6, for 𝒯 of finite dimension. Let f : 𝒯 ⟶ 𝒳 be a quasi-compact, locally of finite type 1-morphism of Jacobson, pseudo-catenary, locally Noetherian algebraic stacks over S which is quasi-DM, whose source is irreducible and whose target is quasi-separated, and let 𝒵 ↪ 𝒳, cut out by P, be the scheme theoretic image of f. Suppose dim(𝒯) ≠ ∞. Then dim(𝒵) ≤ dim(𝒯), and exactly one of the following holds: (1) dim_t(𝒯_{f(t)}) > 0 at every finite type point t ∈ |𝒯|, in which case dim(𝒵) < dim(𝒯); or (2) dim(𝒯) = dim(𝒵).

Erratum. The source states the lemma without the hypothesis dim(𝒯) ≠ ∞, and as written it is false when dim(𝒯) = dim(𝒵) = ∞. Let N be Nagata's Noetherian ring of infinite dimension (Stacks, Examples, Tag 02JC), let D = N⟨X⟩ be the localization of N[X] at the monic polynomials, and let f : 𝔸¹_D ⟶ Spec D be the projection. * Every hypothesis holds. N is regular, its local rings being localizations of polynomial rings, so D is a Noetherian regular domain, hence Cohen–Macaulay and universally catenary (Stacks 00NM), and D[s] is as well. D is Jacobson by J. W. Brewer and W. J. Heinzer, R Noetherian implies R⟨X⟩ is a Hilbert ring, J. Algebra 67 (1980) 204–209, doi:10.1016/0021-8693(80)90317-8; so is D[s], being of finite type over D. 𝔸¹_D is irreducible, f is affine, hence quasi-compact and representable, hence quasi-DM, and of finite type, and Spec D is affine, hence quasi-separated. * Both alternatives hold. f is faithfully flat, so its scheme theoretic image is Spec D. Every fibre is an affine line over a field, so dim_t(𝒯_{f(t)}) = 1 > 0 everywhere. The primes p_i N[X] contain no monic polynomial and have unbounded height, so dim(𝒯) = dim(𝒵) = ∞. Thus (1) and (2) hold together, and (1) does not force dim(𝒵) < dim(𝒯).

This counterexample is machine-checked: AlgebraicGeometry.Stack.not_forall_xor_relativeDimension_pos, in StacksFrontier/AlgebraicGeometry/Stacks/DimensionSchemeTheoreticImageCounterexample0DS6.lean, proves that the statement below without h𝒯Finite is false, every hypothesis of the source (quasi-compactness of f included) being proved for this f.

Infinite-dimensional Noetherian Hilbert domains were first constructed by K. Fujita, Infinite dimensional Noetherian Hilbert domains, Hiroshima Math. J. 5 (1975) 181–185, doi:10.32917/hmj/1206136627. The source's arithmetic presupposes finiteness: Stacks 0DS4, from which it derives this lemma, is stated as dim_t(𝒯_{f(t)}) ≥ dim 𝒯 - dim 𝒵, and the proof as dim_t(𝒯_{f(t)}) = dim_t 𝒯 - dim_{f(t)} 𝒵, differences that are undefined when both dimensions are infinite; Stacks 0DRT, on which Stacks 0DRX rests, assumes finite dimension explicitly. With no finiteness hypothesis, what holds is AlgebraicGeometry.Stack.closedSubstackDimension_le_dimension_and_xor_relativeDimension_pos: dim(𝒵) ≤ dim(𝒯) and Xor ((1) ∧ dim(𝒵) < dim(𝒯)) (2).

The proof: Stacks 0DS4 for a quasi-compact f gives dim(𝒯) ≤ dim(𝒵) + dim_t(𝒯_{f(t)}) at every point, with equality on a nonempty open subset W of |𝒯|; the fibre dimensions are non-negative integers because f is quasi-DM. The open W contains a finite type point t, 𝒯 being Jacobson (AlgebraicGeometry.Stack.exists_isFiniteTypePoint_mem_of_isOpen). Under (1) the fibre dimension at t is a positive integer, so dim(𝒵) < dim(𝒯) because dim(𝒯) is finite — it is neither ∞, by hypothesis, nor -∞, by AlgebraicGeometry.Stack.dimensionAtPoint_ne_bot; hence (1) excludes (2). If (2) fails, then (1) holds by AlgebraicGeometry.Stack.closedSubstackDimension_le_dimension_and_xor_relativeDimension_pos.

theorem closedSubstackDimension_le_dimension_and_xor_relativeDimension_pos_of_ne_top
    {𝒯 𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒯 ⟶ 𝒳)
    (hfQC : IsQuasiCompactMorphism B S hS f)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (hDM : AlgebraicStacks.IsQuasiDM B S hS f)
    (h𝒯 : IsLocallyNoetherianStack.{u, w} B S hS 𝒯)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (h𝒯Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒯)
    (h𝒳Jacobson : AlgebraicStacks.IsJacobson B S hS 𝒳)
    (h𝒯Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒯)
    (h𝒳Catenary : AlgebraicStacks.IsPseudoCatenary B S hS 𝒳)
    (h𝒯Irreducible : @IrreducibleSpace _ (pointTopology B S hS 𝒯.val))
    (h𝒳QuasiSeparated : IsQuasiSeparatedAbs.{u, w, w} B S hS 𝒳)
    {P : ObjectProperty 𝒳.val.val.obj} (hP : IsSchemeTheoreticImage f P)
    (h𝒯Finite : dimension B S hS 𝒯 h𝒯 ≠ ⊤) :
    closedSubstackDimension B S hS 𝒳 P hP.1 hP.isAlgebraicStack h𝒳 ≤ dimension B S hS 𝒯 h𝒯 ∧
      Xor (∀ t, IsFiniteTypePoint.{u, w} B S hS 𝒯 t →
            0 < relativeStackDimensionAt B S hS f hf h𝒯 h𝒳 t)
        (dimension B S hS 𝒯 h𝒯 =
          closedSubstackDimension B S hS 𝒳 P hP.1 hP.isAlgebraicStack h𝒳) ∧
      ((∀ t, IsFiniteTypePoint.{u, w} B S hS 𝒯 t →
            0 < relativeStackDimensionAt B S hS f hf h𝒯 h𝒳 t) →
        closedSubstackDimension B S hS 𝒳 P hP.1 hP.isAlgebraicStack h𝒳 <
          dimension B S hS 𝒯 h𝒯)

Sources

• Section 107.5, Tag 0DRE
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Examples.DimensionVersusPointSet.dimensionAtPoint_translationQuotient_eq_one · Stacks.Examples.DimensionVersusPointSet.topologicalKrullDim_points_translationQuotient_eq_zero · Stacks.Examples.DimensionVersusPointSet.dimensionAtPoint_ne_topologicalKrullDimAt_points · Stacks.Examples.DimensionVersusPointSet.dimensionAtPoint_infiniteProductQuotient_eq_zero · Stacks.Examples.DimensionVersusPointSet.isGenericPoint_quotientCoordinatePoint · Stacks.Examples.DimensionVersusPointSet.irreducibleSpace_points_infiniteProductQuotient · Stacks.Examples.DimensionVersusPointSet.topologicalKrullDim_points_infiniteProductQuotient_eq_one · Stacks.Examples.DimensionVersusPointSet.topologicalKrullDimAt_points_infiniteProductQuotient_eq_one

Section107.6 The dimension of the local ring#

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

Tag 0DS8, a lemma

Tag 0DS8 in the Stacks Project.

AlgebraicGeometry.Stack.ringKrullDim_relation_eq_add_ringKrullDim_sourceFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothPresentationLocalRingDimension.lean, line 286. The attribute's comment: “the dimension formula for the source projection”.

Stacks 0DS8, the dimension formula. For a smooth 1-morphism f : U ⟶ 𝒳 from a scheme to a locally Noetherian algebraic stack and a presented self-intersection R = U ×_𝒳 U with source morphism s, the dimension of 𝒪_{R, r} at a geometric point r is the sum of the dimension of 𝒪_{U, s(r)} and the dimension of the fibre 𝒪_{R_{s(r)}, r}.

The morphism s is smooth, hence flat, so 𝒪_{U, s(r)} ⟶ 𝒪_{R, r} is a flat local homomorphism of Noetherian local rings and Stacks 00ON applies.

theorem ringKrullDim_relation_eq_add_ringKrullDim_sourceFibre
    (hf : AlgebraicStacks.IsSmooth B S hS f) (hsq : Bicategory.IsTwoFibreProduct sq)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳) (hR : IsAlgebraicSpace B S hS R)
    (r : Space.GeometricPoint B S hS R) :
    ringKrullDim (Space.etaleLocalRing B S hS R r) =
      ringKrullDim (chartEtaleLocalRing B S hS U f sq R eU eR r) +
        ringKrullDim (sourceFibreEtaleLocalRing B S hS U f sq R eU eR hR r)

AlgebraicGeometry.Stack.ringKrullDim_chart_add_relation_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothPresentationLocalRingDimension.lean, line 329. The attribute's comment: “the dimension-difference identity”.

Stacks 0DS8. The identity dim(𝒪_{U,s(r)}) - dim(𝒪_{R_u,r}) = 2 dim(𝒪_{U,s(r)}) - dim(𝒪_{R,r}), recorded in the subtraction-free form obtained by adding dim(𝒪_{R_u,r}) + dim(𝒪_{R,r}) to both sides, which is equivalent to it wherever the three dimensions are finite — in particular here, all three rings being Noetherian local.

The invariant 2 dim(𝒪_{U,s(r)}) - dim(𝒪_{R,r}) of Stacks 0DSA is thus computed by the source fibre.

theorem ringKrullDim_chart_add_relation_eq
    (hf : AlgebraicStacks.IsSmooth B S hS f) (hsq : Bicategory.IsTwoFibreProduct sq)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳) (hR : IsAlgebraicSpace B S hS R)
    (r : Space.GeometricPoint B S hS R) :
    ringKrullDim (chartEtaleLocalRing B S hS U f sq R eU eR r) +
        ringKrullDim (Space.etaleLocalRing B S hS R r) =
      ringKrullDim (chartEtaleLocalRing B S hS U f sq R eU eR r) +
          ringKrullDim (chartEtaleLocalRing B S hS U f sq R eU eR r) +
        ringKrullDim (sourceFibreEtaleLocalRing B S hS U f sq R eU eR hR r)

Tag 0DS9, a lemma

Tag 0DS9 in the Stacks Project.

AlgebraicGeometry.Stack.hasLocalRingDimensionAtEveryChart_of_hasLocalRingDimensionAtSomeChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalRingDimensionChartComparison.lean, line 358. The attribute's comment: “condition (1) implies condition (2)”.

Stacks 0DS9, condition (1) implies condition (2). If some scheme of the site carries a smooth 1-morphism to a locally Noetherian algebraic stack 𝒳 and a finite type point above the finite type point x ∈ |𝒳| at which the invariant of Stacks 0DSA is d, then every such configuration measures it to be d.

This is the chart independence of the invariant, AlgebraicGeometry.Stack.hasChartInvariant_congr_of_isFiniteTypePoint, read through the restatement of the two conditions in terms of AlgebraicGeometry.Stack.HasChartInvariant.

theorem hasLocalRingDimensionAtEveryChart_of_hasLocalRingDimensionAtSomeChart
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (x : points B S hS 𝒳.val.val 𝒳.val.property)
    (hx : IsFiniteTypePoint.{u, w} B S hS 𝒳 x) (d : ℤ)
    (hd : HasLocalRingDimensionAtSomeChart.{u, w} B S hS 𝒳 h𝒳 x hx d) :
    HasLocalRingDimensionAtEveryChart.{u, w} B S hS 𝒳 h𝒳 x hx d

AlgebraicGeometry.Stack.hasLocalRingDimensionAtSomeChart_iff_hasLocalRingDimensionAtEveryChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalRingDimensionChartComparison.lean, line 387. The attribute's comment: “the equivalence of the two conditions”.

Stacks 0DS9. For a locally Noetherian algebraic stack 𝒳, a finite type point x ∈ |𝒳| and an integer d, the two conditions

1. there exists a scheme U of the site, a smooth 1-morphism U ⟶ 𝒳 and a finite type point u ∈ U above x with 2 dim(𝒪_{U,ū}) - dim(𝒪_{R, e(ū)}) = d, where R = U ×_𝒳 U, and
2. every such U, smooth 1-morphism and finite type point above x satisfies that identity

are equivalent. Condition (1) is AlgebraicGeometry.Stack.HasLocalRingDimensionAtSomeChart, which is also the definition of Stacks 0DSA, and condition (2) is AlgebraicGeometry.Stack.HasLocalRingDimensionAtEveryChart.

Condition (2) implies condition (1) because the range of the two quantifiers is nonempty, by Stacks 06FX. The converse is the chart independence of the invariant, which is the content of the source's proof.

theorem hasLocalRingDimensionAtSomeChart_iff_hasLocalRingDimensionAtEveryChart
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (x : points B S hS 𝒳.val.val 𝒳.val.property)
    (hx : IsFiniteTypePoint.{u, w} B S hS 𝒳 x) (d : ℤ) :
    HasLocalRingDimensionAtSomeChart.{u, w} B S hS 𝒳 h𝒳 x hx d ↔
      HasLocalRingDimensionAtEveryChart.{u, w} B S hS 𝒳 h𝒳 x hx d

AlgebraicGeometry.Stack.hasLocalRingDimensionAtSomeChart_of_hasLocalRingDimensionAtEveryChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalRingDimensionChartIndependence.lean, line 493. The attribute's comment: “condition (2) implies condition (1)”.

Stacks 0DS9, condition (2) implies condition (1). If every smooth chart of a locally Noetherian algebraic stack 𝒳 carrying a finite type point above x measures the invariant of Stacks 0DSA to be d, then some one does — because, by Stacks 06FX, there is one.

This direction of the equivalence is exactly the non-emptiness of the range of the two quantifiers, supplied by AlgebraicGeometry.Stack.exists_smoothChart_presentation_of_isFiniteTypePoint.

theorem hasLocalRingDimensionAtSomeChart_of_hasLocalRingDimensionAtEveryChart
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (x : points B S hS 𝒳.val.val 𝒳.val.property)
    (hx : IsFiniteTypePoint.{u, w} B S hS 𝒳 x) (d : ℤ)
    (h : HasLocalRingDimensionAtEveryChart.{u, w} B S hS 𝒳 h𝒳 x hx d) :
    HasLocalRingDimensionAtSomeChart.{u, w} B S hS 𝒳 h𝒳 x hx d

AlgebraicGeometry.Stack.hasRelationLocalRingDimension_transport_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalRingDimensionSquareIndependence.lean, line 248. The attribute's comment: “the invariant of the two conditions does not depend on the presented self-intersection”.

The invariant of Stacks 0DSA does not depend on the presented self-intersection. Let a smooth chart g : V ⟶ 𝒳 be given, and let its self-intersection be presented twice over — by a 2-fibre product square T for the cospan (g, g), an algebraic space Q presenting its apex through eQ and a mediating morphism δ, and by T', Q', eQ', δ'. Then at one and the same point ν of the chart the two presentations measure the invariant to be the same integer.

The point of the chart does not move: the comparison of the two presentations is an isomorphism Q ≅ Q' of the two representing presheaves of the relation, which carries the diagonal image of ν for the first presentation to the diagonal image of ν for the second and leaves ν alone. The chart dimension entering the invariant is read at ν itself (AlgebraicGeometry.Stack.hasRelationLocalRingDimension_diagonal_iff), so it is untouched, and the dimension of the relation is unchanged under an isomorphism of presheaves (AlgebraicGeometry.Space.localRingDimension_pointsMap_of_isIso).

This is one half of the presentation quantifier of condition (2) of Stacks 0DS9; the other half, the comparison equivalence of the chart, is AlgebraicGeometry.Stack.hasRelationLocalRingDimension_transport_equivalence, and the two are combined in AlgebraicGeometry.Stack.forall_hasRelationLocalRingDimension_transport_presentation.

theorem hasRelationLocalRingDimension_transport_twoFibreProduct
    (δ : Bicategory.TwoCommSq.PreHom (selfIntersectionDiagonalSquare B S hS V g) T)
    (δ' : Bicategory.TwoCommSq.PreHom (selfIntersectionDiagonalSquare B S hS V g) T')
    (ν : Space.points B S hS (yoneda.obj V)) (d : ℤ) :
    HasRelationLocalRingDimension B S hS V g T Q eV eQ
        (Space.pointsMap B S hS (yoneda.obj V)
          (selfIntersectionDiagonalMap B S hS V g T Q eV eQ δ) ν) d ↔
      HasRelationLocalRingDimension B S hS V g T' Q' eV eQ'
        (Space.pointsMap B S hS (yoneda.obj V)
          (selfIntersectionDiagonalMap B S hS V g T' Q' eV eQ' δ') ν) d

AlgebraicGeometry.Stack.exists_iff_forall_geometricPoint_hasChartLocalRingDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothPresentationLocalRingDimension.lean, line 394. The attribute's comment: “the two conditions, over the geometric point above a point of the relation”.

Stacks 0DS9, for the choice of geometric point. The existential and the universal condition over the geometric points above a point ρ of the relation are equivalent: some geometric point above ρ measures the invariant to be d exactly when every one does.

Forward this is AlgebraicGeometry.Stack.hasChartLocalRingDimension_iff_hasRelationLocalRingDimension; backward it is the existence of a geometric point above ρ.

theorem exists_iff_forall_geometricPoint_hasChartLocalRingDimension
    (hR : IsAlgebraicSpace B S hS R) (ρ : Space.points B S hS R) (d : ℤ) :
    (∃ r : Space.GeometricPoint B S hS R, r.LiesOver ρ ∧
        HasChartLocalRingDimension B S hS U f sq R eU eR r d) ↔
      ∀ r : Space.GeometricPoint B S hS R, r.LiesOver ρ →
        HasChartLocalRingDimension B S hS U f sq R eU eR r d

AlgebraicGeometry.Stack.exists_hasChartLocalRingDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothPresentationLocalRingDimension.lean, line 419. The attribute's comment: “the invariant of the two conditions is a well-defined integer at a smooth chart”.

Stacks 0DS9, well-definedness of the invariant. At a geometric point of a presented self-intersection of a smooth chart of a locally Noetherian algebraic stack the invariant 2 dim(𝒪_{U,s(r)}) - dim(𝒪_{R,r}) of Stacks 0DSA is realized by an integer: both local rings are Noetherian local rings, so Krull's height theorem makes both dimensions finite.

This is what lets the conditions of Stacks 0DS9 be read at a d ∈ ℤ; the integer is unique by AlgebraicGeometry.Stack.hasChartLocalRingDimension_unique.

theorem exists_hasChartLocalRingDimension
    (hf : AlgebraicStacks.IsSmooth B S hS f) (hsq : Bicategory.IsTwoFibreProduct sq)
    (h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳) (hR : IsAlgebraicSpace B S hS R)
    (r : Space.GeometricPoint B S hS R) :
    ∃ d : ℤ, HasChartLocalRingDimension B S hS U f sq R eU eR r d

Tag 0DSA, a definition

Tag 0DSA in the Stacks Project.

AlgebraicGeometry.Stack.HasLocalRingDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothPresentationLocalRingDimension.lean, line 478.

Stacks 0DSA. The dimension of the local ring of a locally Noetherian algebraic stack 𝒳 at a finite type point x ∈ |𝒳| is the integer d when condition (1) of Stacks 0DS9 holds: some scheme U of the site carries a smooth 1-morphism f : U ⟶ 𝒳 and a finite type point u of U above x at which a presented self-intersection R = U ×_𝒳 U, with diagonal e, has 2 dim(𝒪_{U,ū}) - dim(𝒪_{R, e(ū)}) = d.

The source phrases the dimension as a relation between x and d ∈ ℤ, not as a function of x, and so does this: the value is pinned down by Stacks 0DS9, whose independence of the chart is not available here. Negative values occur (Stacks 0DS5), whence ℤ.

def HasLocalRingDimension (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (_h𝒳 : IsLocallyNoetherianStack.{u, w} B S hS 𝒳)
    (x : points B S hS 𝒳.val.val 𝒳.val.property)
    (_hx : IsFiniteTypePoint.{u, w} B S hS 𝒳 x) (d : ℤ) : Prop

Tag 0DSB, a lemma

Tag 0DSB in the Stacks Project.

AlgebraicGeometry.Stack.hasLocalRingDimension_of_versalCogroupoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalRingDimensionVersal.lean, line 747.

Stacks 0DSB. Let 𝒳 be an algebraic stack, locally of finite type over a locally Noetherian scheme S (Situation 0DQU), and let x₀ : Spec k ⟶ 𝒳 be a morphism, k a field of finite type over S, with Spec Λ ⊆ S an affine open through which Spec k ⟶ S factors with Λ → k finite (Section 07T2). Represent 𝓕_{𝒳,k,x₀} as in Remark 0DR3 by a cogroupoid (A, B, s, t, c) of Noetherian complete local Λ-algebras with residue field k: a versal formal object ξ over A and a representable presentation P on 𝒞^_Λ with objects P.objects = A, arrows P.arrows = B, source and target s = P.source, t = P.target and comultiplication c = P.comultiplication, whose restriction to 𝒞_Λ is the groupoid in functors (A|_{𝒞_Λ}, A|_{𝒞_Λ} ×_{ξ, 𝓕, ξ} A|_{𝒞_Λ}) of ξ (this is the representation produced by AlgebraicGeometry.Stack.exists_versalCogroupoid_predeformationCategory). Then the dimension of the local ring of 𝒳 at the point of x₀ (Stacks 0DSA) is 2 dim A - dim B.

Every such representation is allowed, so the statement holds for all of them; the two dimensions are finite and are recorded as natural numbers before the difference is taken, as in Stacks 0DSA.

theorem hasLocalRingDimension_of_versalCogroupoid (D : VersalSituation.{u, w})
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k]
    (iΛ : Spec (.of Λ) ⟶ D.S) (hiΛ : _root_.AlgebraicGeometry.IsOpenImmersion iΛ)
    (x₀ : D.𝒳.val.val.obj)
    (hx₀ : (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    let C := Deformation.Artin.predeformationCategory iΛ
      (D.𝒳.val.val.p ⋙ Over.post D.B.inclusion) x₀ hx₀
    letI := C.category
    let hp := Deformation.Artin.predeformationCategory_isPredeformationCategory
      D.B D.hS iΛ D.𝒳.val.val.p x₀ hx₀ D.𝒳.val.property
    ∀ (ξ : Deformation.FormalObject C.projection) (_ : Deformation.IsVersal hp.cofibered ξ)
      (P : Deformation.RepresentablePresentation.{_, u, u}
        (Deformation.CompleteLocalAlgCat.{u, u, u} Λ k)),
      P.objects = ξ.base →
      Nonempty (Deformation.versalGroupoid C.projection hp ξ ≅
        Deformation.GroupoidInFunctors.restrict P.groupoidInFunctors
          Deformation.artinianToComplete) →
      ∃ m n : ℕ, ringKrullDim P.objects = m ∧ ringKrullDim P.arrows = n ∧
        HasLocalRingDimension D.B D.S D.hS D.𝒳 (isLocallyNoetherianStack_of_versalSituation D)
          (objectPoint D.B D.S D.hS iΛ x₀ hx₀)
          (isFiniteTypePoint_objectPoint D iΛ hiΛ x₀ hx₀ hfinite) (2 * (m : ℤ) - (n : ℤ))

Sources

• Section 107.6, Tag 0DS7
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.ringKrullDim_relation_eq_add_ringKrullDim_sourceFibre · AlgebraicGeometry.Stack.ringKrullDim_chart_add_relation_eq · AlgebraicGeometry.Stack.hasLocalRingDimensionAtEveryChart_of_hasLocalRingDimensionAtSomeChart · AlgebraicGeometry.Stack.hasLocalRingDimensionAtSomeChart_iff_hasLocalRingDimensionAtEveryChart · AlgebraicGeometry.Stack.hasLocalRingDimensionAtSomeChart_of_hasLocalRingDimensionAtEveryChart · AlgebraicGeometry.Stack.hasRelationLocalRingDimension_transport_twoFibreProduct · AlgebraicGeometry.Stack.exists_iff_forall_geometricPoint_hasChartLocalRingDimension · AlgebraicGeometry.Stack.exists_hasChartLocalRingDimension

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.