101.7 Quasi-compact morphisms to 101.22 The Deligne-Mumford locus

Section101.7 Quasi-compact morphisms #

Section 101.7 of the Stacks Project, Tag 050S. 10 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 050T, a lemma

Tag 050T in the Stacks Project.

AlgebraicGeometry.Stack.isQuasiCompact_iff_baseChange_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactMorphism.lean, line 800.

For a 1-morphism of algebraic stacks over S representable by algebraic spaces, quasi-compactness in the sense of Properties of Stacks, Section 04XB — every algebraic space representing a base change along a scheme-valued point of the target is quasi-compact over its base — is equivalent to quasi-compactness in the sense of Stacks 050U: every base change by a quasi-compact algebraic stack is a quasi-compact algebraic stack.

public theorem isQuasiCompact_iff_baseChange_quasiCompact
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    IsQuasiCompact B S hS f.hom ↔ IsQuasiCompactMorphism.{u, w} B S hS f

Tag 050U, a definition

Tag 050U in the Stacks Project.

AlgebraicGeometry.Stack.IsQuasiCompactMorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactMorphism.lean, line 58.

A 1-morphism of algebraic stacks over S is quasi-compact when every base change of it by a quasi-compact algebraic stack is again a quasi-compact algebraic stack, the fibre product being the canonical 2-fibre product of algebraic stacks and quasi-compactness being AlgebraicGeometry.Stack.IsQuasiCompactStack.

abbrev IsQuasiCompactMorphism {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

Tag 050V, a lemma

Tag 050V in the Stacks Project.

AlgebraicGeometry.Stack.isQuasiCompactMorphism_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactMorphismPermanence.lean, line 104.

Stacks 050V. A base change of a quasi-compact 1-morphism of algebraic stacks over S is quasi-compact: if P is a 2-fibre product of the cospan (g, f) and f is quasi-compact, then the projection P.fst is quasi-compact.

The base change of P.fst by a test 1-morphism k is 𝒵 ×_{𝒴'} P.pt, and Stacks 02XD at the recognised 2-fibre product P identifies it with a 2-fibre product of the cospan (f, k ≫ g); the base change of f along k ≫ g is another, and it is quasi-compact by hypothesis.

theorem isQuasiCompactMorphism_baseChange {𝒳 𝒴 𝒴' : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴) (P : Bicategory.TwoCommSq g f)
    (hP : Bicategory.IsTwoFibreProduct P) (hf : IsQuasiCompactMorphism B S hS f) :
    IsQuasiCompactMorphism B S hS P.fst

Tag 050W, a lemma

Tag 050W in the Stacks Project.

AlgebraicGeometry.Stack.isQuasiCompactMorphism_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactMorphismPermanence.lean, line 86.

Stacks 050W. The composite of two quasi-compact 1-morphisms of algebraic stacks over S is quasi-compact.

A base change of f ≫ g by a quasi-compact algebraic stack is the iterated 2-fibre product (𝒲 ×_𝒵 𝒴) ×_𝒴 𝒳; the inner apex is quasi-compact because g is, the outer one because f is, and Stacks 02XD identifies the outer apex with a 2-fibre product of the cospan of f ≫ g.

theorem isQuasiCompactMorphism_comp {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsQuasiCompactMorphism B S hS f) (hg : IsQuasiCompactMorphism B S hS g) :
    IsQuasiCompactMorphism B S hS (f ≫ g)

Tag 0CL1, a lemma

Tag 0CL1 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiCompactMorphism_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ClosedImmersionQuasiCompact.lean, line 71.

Stacks 0CL1. A closed immersion of algebraic stacks over S is quasi-compact.

A closed immersion is representable by algebraic spaces (Stacks 04YL, part (2)), which is the hypothesis of Stacks 050T; and its second conjunct AlgebraicGeometry.Stack.IsClosedImmersion differs from AlgebraicGeometry.Stack.IsQuasiCompact only in the property demanded of the structural morphism of each representing algebraic space, so Stacks 04CG transfers it pointwise.

theorem isQuasiCompactMorphism_of_isClosedImmersion
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsClosedImmersion B S hS f) :
    Stack.IsQuasiCompactMorphism.{u, w} B S hS f

Tag 050X, a lemma

Tag 050X in the Stacks Project.

AlgebraicGeometry.Stack.isQuasiCompactMorphism_of_comp_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactMorphismPermanence.lean, line 139.

Stacks 050X. Let f : 𝒳 ⟶ 𝒴, p : 𝒳 ⟶ 𝒵 and q : 𝒴 ⟶ 𝒵 be a 2-commutative triangle of 1-morphisms of algebraic stacks over S. If f is surjective and p is quasi-compact, then q is quasi-compact.

A base change 𝒯 ×_𝒵 𝒴 of q by a quasi-compact algebraic stack receives the iterated product (𝒯 ×_𝒵 𝒴) ×_𝒴 𝒳, which is a base change of the surjective f and hence surjects onto it (Stacks 04ZU); Stacks 02XD identifies that iterated apex with a 2-fibre product of the cospan (k, p), quasi-compact by the hypothesis on p, and quasi-compactness of an algebraic stack passes along a surjection.

theorem isQuasiCompactMorphism_of_comp_of_isSurjective
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (p : 𝒳 ⟶ 𝒵) (q : 𝒴 ⟶ 𝒵) (e : f ≫ q ≅ p)
    (hf : IsSurjective B S hS f) (hp : IsQuasiCompactMorphism B S hS p) :
    IsQuasiCompactMorphism B S hS q

Tag 050Y, a lemma

Tag 050Y in the Stacks Project.

AlgebraicGeometry.Stack.isQuasiCompactMorphism_of_comp_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactMorphismPermanence.lean, line 186. References: EGA IV (1.2.4).

Stacks 050Y. If a composite of 1-morphisms of algebraic stacks over S is quasi-compact and its second factor is quasi-separated, then its first factor is quasi-compact.

f is the composite of its graph section with the projection of 𝒴 ×_𝒵 𝒳 to 𝒴. The projection to 𝒳 is a base change of g, hence quasi-separated (Stacks 050F), so the graph section is quasi-compact by Stacks 050J part (5); the projection to 𝒴 is a base change of f ≫ g, hence quasi-compact by Stacks 050V; and Stacks 050W composes the two.

theorem isQuasiCompactMorphism_of_comp_of_isQuasiSeparated (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hgf : IsQuasiCompactMorphism B S hS (f ≫ g))
    (hg : AlgebraicStacks.IsQuasiSeparated B S hS g) :
    IsQuasiCompactMorphism B S hS f

Tag 075S, a lemma

Tag 075S in the Stacks Project.

AlgebraicGeometry.Stack.isQuasiCompactMorphism_of_isQuasiCompactStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactQuasiSeparatedStack.lean, line 172. The attribute's comment: “part (1)”. References: SGA 4 VI (1.14), “(i), algebraic stacks”.

Stacks 075S, part (1). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over a quasi-separated base scheme with 𝒳 quasi-compact and 𝒴 quasi-separated over the base is quasi-compact.

The structure morphism of 𝒳 is f followed by the structure morphism of 𝒴, and it is quasi-compact because 𝒳 is; the structure morphism of 𝒴 is quasi-separated because 𝒴 is quasi-separated over the base; so Stacks 050Y cancels it.

theorem isQuasiCompactMorphism_of_isQuasiCompactStack (hqs : QuasiSeparatedSpace S)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (h𝒳 : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒴 : IsQuasiSeparatedOver.{u, w} B S hS 𝒴) :
    IsQuasiCompactMorphism.{u, w} B S hS f

AlgebraicGeometry.Stack.isQuasiCompactMorphism_and_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactQuasiSeparatedStack.lean, line 190. The attribute's comment: “part (2)”. References: SGA 4 VI (1.14), “(i), stacks, X also qs”.

Stacks 075S, part (2). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over a quasi-separated base scheme with 𝒳 quasi-compact and quasi-separated over the base and 𝒴 quasi-separated over the base is quasi-compact and quasi-separated.

Quasi-compactness is part (1); quasi-separatedness is Stacks 050N part (8), whose hypothesis on the relative diagonal of the structure morphism of 𝒴 is the second conjunct of quasi-separatedness of 𝒴 over the base.

theorem isQuasiCompactMorphism_and_isQuasiSeparated (hqs : QuasiSeparatedSpace S)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (h𝒳qc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳qs : IsQuasiSeparatedOver.{u, w} B S hS 𝒳)
    (h𝒴 : IsQuasiSeparatedOver.{u, w} B S hS 𝒴) :
    IsQuasiCompactMorphism.{u, w} B S hS f ∧
      AlgebraicStacks.IsQuasiSeparated.{u, w} B S hS f

AlgebraicGeometry.Stack.isQuasiCompactStack_and_isQuasiSeparatedOver_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactQuasiSeparatedStack.lean, line 209. The attribute's comment: “part (3)”.

Stacks 075S, part (3). A 2-fibre product 𝒳 ×_𝒴 𝒵 of algebraic stacks over a quasi-separated base scheme, with 𝒳, 𝒵 quasi-compact and quasi-separated over the base and 𝒴 quasi-separated over the base, is quasi-compact and quasi-separated over the base.

The projection to 𝒵 is a base change of f, which is quasi-compact and quasi-separated by part (2), hence is itself quasi-compact (Stacks 050V) and quasi-separated (Stacks 050F). A quasi-compact 1-morphism into the quasi-compact 𝒵 has quasi-compact source, and Stacks 050L part (4) carries quasi-separatedness over the base from 𝒵 to the apex.

theorem isQuasiCompactStack_and_isQuasiSeparatedOver_twoFibreProduct
    (hqs : QuasiSeparatedSpace S) {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (h𝒳qc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳qs : IsQuasiSeparatedOver.{u, w} B S hS 𝒳)
    (h𝒵qc : IsQuasiCompactStack.{u, w} B S hS 𝒵.val 𝒵.property)
    (h𝒵qs : IsQuasiSeparatedOver.{u, w} B S hS 𝒵)
    (h𝒴 : IsQuasiSeparatedOver.{u, w} B S hS 𝒴) :
    IsQuasiCompactStack.{u, w} B S hS
        (twoFibreProductAlgebraicStack B S hS f g).val
        (twoFibreProductAlgebraicStack B S hS f g).property ∧
      IsQuasiSeparatedOver.{u, w} B S hS (twoFibreProductAlgebraicStack B S hS f g)

AlgebraicGeometry.Stack.isQuasiCompactMorphism_of_isQuasiCompactStack_absolute, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactQuasiSeparatedStackAbsolute.lean, line 155. The attribute's comment: “part (1)”. References: SGA 4 VI (1.14), “(i), algebraic stacks”.

Stacks 075S, part (1). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks with 𝒳 quasi-compact and 𝒴 quasi-separated in the absolute sense of Stacks 050D part (8) is quasi-compact. Nothing is asked of the base scheme of the big fppf site.

Quasi-compactness of a 1-morphism is Stacks 050U, so what has to be shown is quasi-compactness of each base change of f by a quasi-compact algebraic stack. Over the terminal scheme the relative statement AlgebraicGeometry.Stack.isQuasiCompactMorphism_of_isQuasiCompactStack applies with no hypothesis — the terminal scheme is affine, hence quasi-separated — to the views of f and of the test stack, whose quasi-compactness is AlgebraicGeometry.Stack.isQuasiCompactStack_changeBaseAlgebraicStack_iff; and AlgebraicGeometry.Stack .isQuasiCompactStack_twoFibreProductAlgebraicStack_of_viewOverIntegers brings the resulting quasi-compact 2-fibre product back to S.

theorem isQuasiCompactMorphism_of_isQuasiCompactStack_absolute
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (h𝒳 : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒴 : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒴) :
    IsQuasiCompactMorphism.{u, w} B S hS f

AlgebraicGeometry.Stack.isQuasiCompactMorphism_and_isQuasiSeparated_absolute, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactQuasiSeparatedStackAbsolute.lean, line 177. The attribute's comment: “part (2)”. References: SGA 4 VI (1.14), “(i), stacks, X also qs”.

Stacks 075S, part (2). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks with 𝒳 quasi-compact and quasi-separated and 𝒴 quasi-separated, both in the absolute sense of Stacks 050D part (8), is quasi-compact and quasi-separated.

Quasi-compactness is part (1). Quasi-separatedness is Stacks 050N part (8), whose two inputs are the over-the-base readings of the two absolute hypotheses, supplied by Stacks 050N part (4).

theorem isQuasiCompactMorphism_and_isQuasiSeparated_absolute
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (h𝒳qc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳qs : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒳)
    (h𝒴 : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒴) :
    IsQuasiCompactMorphism.{u, w} B S hS f ∧
      AlgebraicStacks.IsQuasiSeparated.{u, w} B S hS f

AlgebraicGeometry.Stack.isQuasiCompactStack_and_isAbsolutelyQuasiSeparated_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactQuasiSeparatedStackAbsolute.lean, line 203. The attribute's comment: “part (3)”.

Stacks 075S, part (3). A 2-fibre product 𝒳 ×_𝒴 𝒵 of algebraic stacks, with 𝒳, 𝒵 quasi-compact and quasi-separated and 𝒴 quasi-separated, all in the absolute sense of Stacks 050D part (8), is quasi-compact and quasi-separated in that same absolute sense. Nothing is asked of the base scheme of the big fppf site.

The projection to 𝒵 is a base change of f, which is quasi-compact and quasi-separated by part (2), hence is itself quasi-compact (Stacks 050V) and quasi-separated (Stacks 050F). A quasi-compact 1-morphism into the quasi-compact 𝒵 has quasi-compact source, and Stacks 050L part (8) carries absolute quasi-separatedness from 𝒵 to the apex.

The absolute conclusion is what the next application of part (1) needs of its target, which the over-the-base conclusion of AlgebraicGeometry.Stack.isQuasiCompactStack_and_isQuasiSeparatedOver_twoFibreProduct is not.

theorem isQuasiCompactStack_and_isAbsolutelyQuasiSeparated_twoFibreProduct
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (h𝒳qc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (h𝒳qs : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒳)
    (h𝒵qc : IsQuasiCompactStack.{u, w} B S hS 𝒵.val 𝒵.property)
    (h𝒵qs : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒵)
    (h𝒴 : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒴) :
    IsQuasiCompactStack.{u, w} B S hS
        (twoFibreProductAlgebraicStack B S hS f g).val
        (twoFibreProductAlgebraicStack B S hS f g).property ∧
      AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ
        (twoFibreProductAlgebraicStack B S hS f g)

Tag 0CL2, a lemma

Tag 0CL2 in the Stacks Project.

AlgebraicGeometry.Stack.exists_valuationRing_of_mem_closure_range_pointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ClosureImageValuativePoint.lean, line 473.

A point in the closure of the image of a quasi-compact 1-morphism of algebraic stacks is reached by the closed point of a valuative square. Stacks 0CL2.

theorem exists_valuationRing_of_mem_closure_range_pointsMap
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (hf : IsQuasiCompactMorphism.{u, w} B S hS f)
    (y : points B S hS 𝒴.val.val (Classical.choose 𝒴.property))
    (hy : y ∈ @closure _
      (pointTopology B S hS 𝒴.val)
      (Set.range
      (pointsMap B S hS 𝒳.val.val (Classical.choose 𝒳.property)
        (Classical.choose 𝒴.property) f.hom.hom))) :
    ∃ (q : ValuativeSquare B S hS f)
      (hz : B.Contains
        (Spec (.of ((Spec (.of q.R)).residueField (IsLocalRing.closedPoint q.R))))),
      pointClass B S hS 𝒴.val.val
        (Classical.choose 𝒴.property)
        (fieldValuedPointMap B S hS
          (schemeFibredCategory B S hS
            (siteObject B S hS q.ring_mem q.base)).val
          q.y.hom
          (closedPointFieldValuedPoint B S hS
            (siteObject B S hS q.ring_mem q.base)
            (IsLocalRing.closedPoint q.R) hz)) = y

Tag 0DTL, a lemma

Tag 0DTL in the Stacks Project.

AlgebraicGeometry.Stack.isQuasiCompactMorphism_of_isQuasiCompactMorphism_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactFppfDescent.lean, line 199.

Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : W ⟶ 𝒴 be surjective, flat and locally of finite presentation, where W is an algebraic space. If the base change W ×_𝒴 𝒳 ⟶ W of f along g is quasi-compact, then f is quasi-compact.

theorem isQuasiCompactMorphism_of_isQuasiCompactMorphism_fst
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    {W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hW : IsAlgebraicSpace B S hS W)
    (g : algebraicSpaceStack.{u, w} B S hS W hW ⟶ 𝒴)
    (hgsurj : IsSurjective B S hS g)
    (hgflat : AlgebraicStacks.IsFlat B S hS g)
    (hglfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hbase : IsQuasiCompactMorphism B S hS P.fst) :
    IsQuasiCompactMorphism B S hS f

Sources

Section101.8 Noetherian algebraic stacks #

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

Tag 0510, a definition

Tag 0510 in the Stacks Project.

AlgebraicGeometry.Stack.IsNoetherianStack, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianStack.lean, line 72.

Stacks 0510, verbatim: "Let 𝒳 be an algebraic stack. We say 𝒳 is Noetherian if 𝒳 is quasi-compact, quasi-separated and locally Noetherian."

Quasi-compactness is AlgebraicGeometry.Stack.IsQuasiCompactStack (Stacks 04YB), quasi-separatedness is the absolute axiom AlgebraicGeometry.Stack.IsQuasiSeparatedAbs (Stacks 050D, part (8)) and local Noetherianity is the smooth-scheme-atlas criterion AlgebraicGeometry.Stack.HasPropertyOnSomeSchemeAtlas of Stacks 04YG at AlgebraicGeometry.IsLocallyNoetherian.

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

Tag 0CPM, a lemma

Tag 0CPM in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyNoetherian_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianAlgebraicStack.lean, line 228. The attribute's comment: “part (1): the source is locally Noetherian”.

Stacks 0CPM, part (1), first half, verbatim: "Let j : 𝒳 → 𝒴 be an immersion of algebraic stacks. If 𝒴 is locally Noetherian, then 𝒳 is locally Noetherian [and j is quasi-compact]." Local Noetherianity of an algebraic stack over S is the smooth-scheme-atlas criterion of Stacks 04YG at AlgebraicGeometry.IsLocallyNoetherian.

The 2-fibre product 𝒫 = V ×_𝒴 𝒳 of a locally Noetherian smooth surjective scheme chart g : V ⟶ 𝒴 with j has first projection a base change of j, so 𝒫 is representable by an algebraic space F and the induced morphism F ⟶ V is locally of finite type; F is then locally Noetherian by Stacks 04ZK, and an étale scheme chart of F composed with the second projection — a base change of g, hence smooth and surjective — is a locally Noetherian scheme atlas of 𝒳.

Quasi-compactness of j, the other half of part (1), and part (2) are in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactImmersion.lean, which consumes this statement.

theorem isLocallyNoetherian_of_isImmersion
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS}
    (j : 𝒳 ⟶ 𝒴) (hj : IsImmersion B S hS j)
    (hY : HasPropertyOnSomeSchemeAtlas B S hS
      (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴) :
    HasPropertyOnSomeSchemeAtlas B S hS
      (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.hasRelativeProperty_quasiCompact_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactImmersion.lean, line 97. The attribute's comment: “part (1): the 1-morphism is quasi-compact, in the sense of Stacks 03YK”.

Let j : 𝒳 ⟶ 𝒴 be an immersion of algebraic stacks, where 𝒴 has a smooth surjective scheme atlas with locally Noetherian source. Then j is quasi-compact: it has the relative property of Stacks 03YK at quasi-compactness of morphisms of algebraic spaces.

theorem hasRelativeProperty_quasiCompact_of_isImmersion
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS}
    (j : 𝒳 ⟶ 𝒴) (hj : IsImmersion B S hS j)
    (hY : HasPropertyOnSomeSchemeAtlas B S hS
      (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴) :
    HasRelativeProperty.{u, u, u + 1, u} B S hS
      (Space.quasiCompactProperty B S hS) j.hom hj.1

AlgebraicGeometry.Stack.AlgebraicStacks.isNoetherianStack_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactImmersion.lean, line 164. The attribute's comment: “part (2): the source is Noetherian”.

Let j : 𝒳 ⟶ 𝒴 be an immersion of algebraic stacks. If 𝒴 is Noetherian, then 𝒳 is Noetherian.

theorem isNoetherianStack_of_isImmersion
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS}
    (j : 𝒳 ⟶ 𝒴) (hj : IsImmersion B S hS j)
    (hY : IsNoetherianStack.{u, w, w'} B S hS 𝒴) :
    IsNoetherianStack.{u, w, w'} B S hS 𝒳

Tag 0DQI, a lemma

Tag 0DQI in the Stacks Project.

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

Stacks 0DQI, part (1). The space of points of Stacks 04XL of a locally Noetherian algebraic stack over S is a locally Noetherian topological space.

Local Noetherianity of the stack is read as the existential atlas condition of Stacks 04YF: a smooth surjective 1-morphism from the algebraic stack of a locally Noetherian scheme U of the site. The point space of that algebraic stack is the topological space of U, which is locally Noetherian by Stacks 01OZ, and the chart is open on points by Stacks 06R7 and surjective on points by the definition of Stacks 04ZS, so Stacks 04Z8 part (2) carries local Noetherianity across.

theorem isLocallyNoetherianSpace_points_of_isLocallyNoetherian
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (hN : Stack.HasPropertyOnSomeSchemeAtlas B S hS
      (fun X : Scheme.{u} => IsLocallyNoetherian X) 𝒳) :
    letI := Stack.pointTopology B S hS 𝒳.val
    IsLocallyNoetherianSpace (Stack.points B S hS 𝒳.val.val 𝒳.val.property)

AlgebraicGeometry.Stack.AlgebraicStacks.noetherianSpace_points_of_isQuasiCompactStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianPointsAlgebraicStack.lean, line 169. The attribute's comment: “part (2)”.

Stacks 0DQI, part (2). The space of points of Stacks 04XL of a quasi-compact locally Noetherian algebraic stack over S is a Noetherian topological space.

Quasi-compactness of Stacks 04YB is compactness of the point space, so this is Stacks 04ZB applied to part (1). The name records only the quasi-compactness hypothesis; the local-Noetherianity hypothesis is the same atlas condition part (1) carries.

theorem noetherianSpace_points_of_isQuasiCompactStack
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (hqc : Stack.IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (hN : Stack.HasPropertyOnSomeSchemeAtlas B S hS
      (fun X : Scheme.{u} => IsLocallyNoetherian X) 𝒳) :
    letI := Stack.pointTopology B S hS 𝒳.val
    NoetherianSpace (Stack.points B S hS 𝒳.val.val 𝒳.val.property)

Tag 0GVX, a lemma

Tag 0GVX in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.quasiSober_points_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianPointsAlgebraicStack.lean, line 191.

Stacks 0GVX. The space of points of Stacks 04XL of a locally Noetherian algebraic stack over S is quasi-sober in the sense of Stacks 004X: every irreducible closed subset of it has a generic point.

Local Noetherianity is read as the atlas condition of Stacks 04YF, which supplies a smooth surjective 1-morphism from the algebraic stack of a locally Noetherian scheme U of the site. The point space of that algebraic stack is the topological space of U, hence is quasi-sober and locally Noetherian, and the chart is continuous, open and surjective on points, so quasi-sobriety passes to |𝒳|.

theorem quasiSober_points_of_isLocallyNoetherian
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (hN : Stack.HasPropertyOnSomeSchemeAtlas B S hS
      (fun X : Scheme.{u} => IsLocallyNoetherian X) 𝒳) :
    letI := Stack.pointTopology B S hS 𝒳.val
    QuasiSober (Stack.points B S hS 𝒳.val.val 𝒳.val.property)

Sources

LeanAlgebraicGeometry.Stack.IsNoetherianStack · AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyNoetherian_of_isImmersion · AlgebraicGeometry.Stack.AlgebraicStacks.hasRelativeProperty_quasiCompact_of_isImmersion · AlgebraicGeometry.Stack.AlgebraicStacks.isNoetherianStack_of_isImmersion · AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyNoetherianSpace_points_of_isLocallyNoetherian · AlgebraicGeometry.Stack.AlgebraicStacks.noetherianSpace_points_of_isQuasiCompactStack · AlgebraicGeometry.Stack.AlgebraicStacks.quasiSober_points_of_isLocallyNoetherian

Section101.9 Affine morphisms #

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

Tag 0CHQ, a definition

Tag 0CHQ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsAffineHom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AffineMorphism.lean, line 105.

Stacks 0CHQ. A 1-morphism of algebraic stacks over S is affine when it is representable by algebraic spaces and is affine in the sense of Stacks 04XB.

abbrev IsAffineHom (f : 𝒳 ⟶ 𝒴) : Prop

Tag 0CHR, a lemma

Tag 0CHR in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_and_isAffineHom_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AffineMorphismBaseChange.lean, line 58.

Stacks 0CHR. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒵 ⟶ 𝒴 be an affine 1-morphism of algebraic stacks, that is (Stacks 0CHQ) one which is representable by algebraic spaces and affine in the sense of Stacks 04XB. If P is a 2-fibre product of the cospan (g, f), then the base change P.snd : 𝒵 ×_𝒴 𝒳 ⟶ 𝒳 is an affine 1-morphism of algebraic stacks: it is representable by algebraic spaces, and it is affine in the sense of Stacks 04XB.

theorem isRepresentableByAlgebraicSpaces_and_isAffineHom_snd
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hg_rep : IsRepresentableByAlgebraicSpaces B S hS g.hom.hom)
    (hg_aff : Stack.IsAffineHom B S hS g.hom) :
    IsRepresentableByAlgebraicSpaces B S hS P.snd.hom.hom ∧
      Stack.IsAffineHom B S hS P.snd.hom

AlgebraicGeometry.Stack.AlgebraicStacks.isAffineHom_snd_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AffineMorphismStability.lean, line 267.

Stacks 0CHR. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S, let g : 𝒵 ⟶ 𝒴 be an affine 1-morphism of algebraic stacks, and let P be a 2-fibre product of the cospan (g, f). Then the base change P.snd : 𝒵 ×_𝒴 𝒳 ⟶ 𝒳 of g along f is affine.

Both halves are base-change statements: representability by algebraic spaces is Stacks 0302 and affineness in the sense of Stacks 04XB is Stacks 045C. The square is arbitrary, so this applies to any square a consumer has already exhibited as a 2-fibre product rather than only to the canonical one of Stacks 04T2.

theorem isAffineHom_snd_of_isTwoFibreProduct
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hg : IsAffineHom B S hS g) :
    IsAffineHom B S hS P.snd

Tag 0CHS, a lemma

Tag 0CHS in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableMorphism_comp_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AffineMorphismRepresentableComp.lean, line 119. The attribute's comment: “with 0CHQ read literally: representable by schemes and affine in the sense of 04XB”.

Stacks 0CHS, for the definition of Stacks 0CHQ read literally. Call a 1-morphism of algebraic stacks over S affine when it is representable (by schemes, Stacks 02Y7) and affine in the sense of Stacks 04XB. Then a composite of two affine 1-morphisms of algebraic stacks is affine: representability composes by Stacks 02ZS, and affineness in the sense of Stacks 04XB composes by AlgebraicGeometry.Stack.isAffineHom_comp (Stacks 045B with Stacks 03WH and the implication (4) ⇒ (2) of Stacks 03WG), which applies because a representable 1-morphism is representable by algebraic spaces.

theorem isRepresentableMorphism_comp_isAffineHom (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳.val.val.p 𝒴.val.val.p
        (CatFiberedInGroupoids.homFunctor f.hom) ∧ Stack.IsAffineHom B S hS f.hom)
    (hg : Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒴.val.val.p 𝒵.val.val.p
        (CatFiberedInGroupoids.homFunctor g.hom) ∧ Stack.IsAffineHom B S hS g.hom) :
    Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳.val.val.p 𝒵.val.val.p
        (CatFiberedInGroupoids.homFunctor (f ≫ g).hom) ∧
      Stack.IsAffineHom B S hS (f ≫ g).hom

AlgebraicGeometry.Stack.AlgebraicStacks.isAffineHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AffineMorphismStability.lean, line 285.

Stacks 0CHS. A composite of two affine 1-morphisms of algebraic stacks over S is affine: representability by algebraic spaces composes by Stacks 0301, and affineness in the sense of Stacks 04XB composes by Stacks 045B, whose two ingredients at affineness are Stacks 03WH and the implication (4) ⇒ (2) of Stacks 03WG.

theorem isAffineHom_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsAffineHom B S hS f) (hg : IsAffineHom B S hS g) :
    IsAffineHom B S hS (f ≫ g)

Tag 0GQE, a lemma

Tag 0GQE in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isAffineHom_of_comp_of_isAffineHom_relativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AffineDiagonalPermanence.lean, line 182.

Stacks 0GQE. Let
  𝒳 ----f----> 𝒴
    \         /
     a       b
      \     /
       >  𝒵 <
be a 2-commutative triangle of 1-morphisms of algebraic stacks over S, the commutativity being the 2-isomorphism comm : a ≅ f ≫ b. If a is affine and the relative diagonal Δ_b is affine in the sense of Properties of Stacks, Section 04XB, then f is affine.

Reading the statement. The unqualified IsAffineHom, in the hypothesis ha on a and in the conclusion on f, elaborates to AlgebraicGeometry.Stack.AlgebraicStacks.IsAffineHom, the notion of an affine 1-morphism of algebraic stacks of Stacks 0CHQ (registered in StacksFrontier.AlgebraicGeometry.Stacks.AffineMorphism). It is by definition the conjunction IsRepresentableByAlgebraicSpaces B S hS q.hom.hom ∧ Stack.IsAffineHom B S hS q.hom for q = a and for q = f, so it includes representability by algebraic spaces: a is assumed, and f is concluded, to be representable by algebraic spaces and affine in the sense of Stacks 04XB, exactly as in the source. The 1-morphism relativeDiagonalAlgebraicStacks B S hS b is the relative diagonal Δ_b : 𝒴 ⟶ 𝒴 ×_{b, 𝒵, b} 𝒴, y ↦ (y, y, id). The hypothesis hΔ on it is written with the qualified Stack.IsAffineHom, the condition of Stacks 04XB alone, without representability; it is weaker than the source's hypothesis that Δ_b is affine, and loses nothing, since Δ_b is representable by algebraic spaces unconditionally by Stacks 04XS part (1) (AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_relativeDiagonal_of_isAlgebraicStack).

This is the source's proof. The 1-morphism f is 2-isomorphic to Γ_f ≫ pr₂, where Γ_f : 𝒳 ⟶ 𝒳 ×_𝒵 𝒴 is the graph of f over 𝒵 (Stacks 050I) and pr₂ : 𝒳 ×_𝒵 𝒴 ⟶ 𝒴 is the second projection of the canonical 2-fibre product of the cospan (a, b). The projection is a base change of a, hence affine by Stacks 0CHR; the graph is affine by AlgebraicGeometry.Stack.isAffineHom_graph, which carries the hypothesis on Δ_b along the base-change square of Stacks 04Z1; and Stacks 0CHS composes the two.

theorem isAffineHom_of_comp_of_isAffineHom_relativeDiagonal
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (a : 𝒳 ⟶ 𝒵) (b : 𝒴 ⟶ 𝒵) (comm : a ≅ f ≫ b)
    (ha : IsAffineHom B S hS a)
    (hΔ : Stack.IsAffineHom B S hS (relativeDiagonalAlgebraicStacks B S hS b).hom) :
    IsAffineHom B S hS f

Sources

LeanAlgebraicGeometry.Stack.AlgebraicStacks.IsAffineHom · AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_and_isAffineHom_snd · AlgebraicGeometry.Stack.AlgebraicStacks.isAffineHom_snd_of_isTwoFibreProduct · AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableMorphism_comp_isAffineHom · AlgebraicGeometry.Stack.AlgebraicStacks.isAffineHom_comp · AlgebraicGeometry.Stack.AlgebraicStacks.isAffineHom_of_comp_of_isAffineHom_relativeDiagonal

Section101.10 Integral and finite morphisms #

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

Tag 0CHU, a definition

Tag 0CHU in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsIntegralHom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IntegralFiniteMorphism.lean, line 113. The attribute's comment: “part (1): integral morphisms”.

Stacks 0CHU, part (1). A 1-morphism of algebraic stacks over S is integral when it is representable by algebraic spaces and is integral in the sense of Stacks 04XB: every algebraic space representing its base change along a scheme-valued point of the target has integral structural morphism, read as a morphism of algebraic spaces over S.

abbrev IsIntegralHom (f : 𝒳 ⟶ 𝒴) : Prop

Declarations registered for the tag:

AlgebraicGeometry.Stack.AlgebraicStacks.IsFinite, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/IntegralFiniteMorphism.lean, line 128 (StacksFrontier): “part (2): finite morphisms”.

Tag 0CHV, a lemma

Tag 0CHV in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isIntegralHom_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IntegralFiniteMorphism.lean, line 163. The attribute's comment: “integral”.

Stacks 0CHV, the integral case. A base change of an integral 1-morphism of algebraic stacks over S is integral: if g : 𝒵 ⟶ 𝒴 is integral and P is a 2-fibre product of the cospan (f, g) for a 1-morphism f : 𝒳 ⟶ 𝒴, then P.fst : 𝒵 ×_𝒴 𝒳 ⟶ 𝒳 is integral.

Representability by algebraic spaces base changes by Stacks 0302 and the relative property of Stacks 04XB by Stacks 045C, which applies because integrality of morphisms of algebraic spaces is stable under base change and local at the target for the fppf precoverage.

theorem isIntegralHom_baseChange (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (P : Bicategory.TwoCommSq f g) (hP : Bicategory.IsTwoFibreProduct P)
    (hg : IsIntegralHom B S hS g) :
    IsIntegralHom B S hS P.fst

AlgebraicGeometry.Stack.AlgebraicStacks.isFinite_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IntegralFiniteMorphism.lean, line 184. The attribute's comment: “finite”.

Stacks 0CHV, the finite case. A base change of a finite 1-morphism of algebraic stacks over S is finite: if g : 𝒵 ⟶ 𝒴 is finite and P is a 2-fibre product of the cospan (f, g) for a 1-morphism f : 𝒳 ⟶ 𝒴, then P.fst : 𝒵 ×_𝒴 𝒳 ⟶ 𝒳 is finite.

Representability by algebraic spaces base changes by Stacks 0302 and the relative property of Stacks 04XB by Stacks 045C, which applies because finiteness of morphisms of algebraic spaces is stable under base change and local at the target for the fppf precoverage.

theorem isFinite_baseChange (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (P : Bicategory.TwoCommSq f g) (hP : Bicategory.IsTwoFibreProduct P)
    (hg : IsFinite B S hS g) :
    IsFinite B S hS P.fst

Tag 0CHW, a lemma

Tag 0CHW in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isIntegralHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IntegralFiniteMorphism.lean, line 211. The attribute's comment: “integral”.

Stacks 0CHW, the integral case: a composite of integral 1-morphisms of algebraic stacks over S is integral.

Representability by algebraic spaces composes by Stacks 0301 and the relative property of Stacks 04XB by Stacks 045B, which applies because integrality of morphisms of algebraic spaces is stable under base change and under composition (Stacks 03ZR) and local at the target for the fppf precoverage.

theorem isIntegralHom_comp (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsIntegralHom B S hS f) (hg : IsIntegralHom B S hS g) :
    IsIntegralHom B S hS (f ≫ g)

AlgebraicGeometry.Stack.AlgebraicStacks.isFinite_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IntegralFiniteMorphism.lean, line 228. The attribute's comment: “finite”.

Stacks 0CHW, the finite case: a composite of finite 1-morphisms of algebraic stacks over S is finite.

Representability by algebraic spaces composes by Stacks 0301 and the relative property of Stacks 04XB by Stacks 045B, which applies because finiteness of morphisms of algebraic spaces is stable under base change and under composition (Stacks 03ZR) and local at the target for the fppf precoverage.

theorem isFinite_comp (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsFinite B S hS f) (hg : IsFinite B S hS g) :
    IsFinite B S hS (f ≫ g)

Sources

LeanAlgebraicGeometry.Stack.AlgebraicStacks.IsIntegralHom · AlgebraicGeometry.Stack.AlgebraicStacks.IsFinite · AlgebraicGeometry.Stack.AlgebraicStacks.isIntegralHom_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.isFinite_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.isIntegralHom_comp · AlgebraicGeometry.Stack.AlgebraicStacks.isFinite_comp

Section101.11 Open morphisms #

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

Tag 06U1, a lemma

Tag 06U1 in the Stacks Project.

AlgebraicGeometry.Stack.representable_universallyOpen_iff_openMap_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyOpenCriterion.lean, line 511.

Stacks 06U1. For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S which is representable by algebraic spaces, the two conditions

f is universally open in the sense of Properties of Stacks, Section 04XB, that is AlgebraicGeometry.Stack.UniversallyOpen; and

for every 1-morphism g : 𝒵 ⟶ 𝒴 of algebraic stacks over S the map |𝒵 ×_𝒴 𝒳| → |𝒵| on the points of Stacks 04XG for the topology of Stacks 04XL is open, that is AlgebraicGeometry.Stack.AlgebraicStacks.UniversallyOpen

are equivalent.

theorem representable_universallyOpen_iff_openMap_baseChange
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    UniversallyOpen B S hS f.hom ↔ AlgebraicStacks.UniversallyOpen B S hS f

Tag 06U2, a definition

Tag 06U2 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsOpen, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenAlgebraicStack.lean, line 50. The attribute's comment: “part (1): open”.

A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is open when the map |𝒳| → |𝒴| it induces on the topological spaces of points is an open map.

abbrev IsOpen {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.AlgebraicStacks.UniversallyOpen, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenAlgebraicStack.lean, line 59. The attribute's comment: “part (2): universally open”.

A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is universally open when, for every 1-morphism g : 𝒵 ⟶ 𝒴 of algebraic stacks over S, the base change 𝒵 ×_{g, 𝒴, f} 𝒳 ⟶ 𝒵 of f by g is open in the sense of AlgebraicGeometry.Stack.AlgebraicStacks.IsOpen.

abbrev UniversallyOpen {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

Tag 06U3, a lemma

Tag 06U3 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.universallyOpen_baseChange_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyOpenSubmersiveBaseChange.lean, line 200.

Stacks 06U3. Universal openness is stable under base change: let f : 𝒳 ⟶ 𝒴 be a universally open 1-morphism of algebraic stacks over S and let R be a 2-fibre product square of the cospan (g, f) for some g : 𝒴' ⟶ 𝒴. Then the base change R.fst : R.pt ⟶ 𝒴' of f along g is universally open.

The square is arbitrary, so this applies to any square a consumer has already exhibited as a 2-fibre product rather than only to the canonical one of Stacks 04T2.

theorem universallyOpen_baseChange_of_isTwoFibreProduct
    {𝒳 𝒴 𝒴' : Stack.AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴} {g : 𝒴' ⟶ 𝒴}
    (R : Bicategory.TwoCommSq g f) (hR : Bicategory.IsTwoFibreProduct R)
    (hf : UniversallyOpen B S hS f) :
    UniversallyOpen B S hS R.fst

Tag 06U4, a lemma

Tag 06U4 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isOpen_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubmersiveComposition.lean, line 70. The attribute's comment: “composition_open”.

Stacks 06U4. The composite of two open 1-morphisms of algebraic stacks over S is open.

theorem isOpen_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hf : IsOpen B S hS f) (hg : IsOpen B S hS g) :
    IsOpen B S hS (f ≫ g)

AlgebraicGeometry.Stack.AlgebraicStacks.universallyOpen_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubmersiveUniversalComposition.lean, line 115. The attribute's comment: “composition_universally_open”.

Stacks 06U4. The composite of two universally open 1-morphisms of algebraic stacks over S is universally open.

theorem universallyOpen_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : UniversallyOpen B S hS f) (hg : UniversallyOpen B S hS g) :
    UniversallyOpen B S hS (f ≫ g)

Sources

LeanAlgebraicGeometry.Stack.representable_universallyOpen_iff_openMap_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.IsOpen · AlgebraicGeometry.Stack.AlgebraicStacks.UniversallyOpen · AlgebraicGeometry.Stack.AlgebraicStacks.universallyOpen_baseChange_of_isTwoFibreProduct · AlgebraicGeometry.Stack.AlgebraicStacks.isOpen_comp · AlgebraicGeometry.Stack.AlgebraicStacks.universallyOpen_comp

Section101.12 Submersive morphisms #

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

Tag 0CHX, a lemma

Tag 0CHX in the Stacks Project.

AlgebraicGeometry.Stack.representable_universallySubmersive_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallySubmersiveCriterion.lean, line 57.

Stacks 0CHX. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S representable by algebraic spaces is universally submersive in the relative sense of Tag 04XB — every algebraic space representing a base change of f along a scheme-valued point of 𝒴 has universally submersive structural morphism — exactly when, for every algebraic stack 𝒵 over 𝒴, the map |𝒵 ×_𝒴 𝒳| → |𝒵| of topological spaces is submersive.

theorem representable_universallySubmersive_iff
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    (∀ (U : BigFppfOver B S hS) (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.val.obj)
        (_hy : y ⋙ 𝒴.val.val.p = Over.map U.hom)
        (T : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hT : IsAlgebraicSpace B U.left.1 U.left.2 T),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.val.p 𝒴.val.val.p y
            (CatFiberedInGroupoids.homFunctor f.hom))
          (presheafOfCategories (T ⋙ typeToCat)).p) →
        Space.UniversallySubmersive B S hS
          (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨T, hT⟩)).hom) ↔
      AlgebraicStacks.IsUniversallySubmersive B S hS f

Tag 06U6, a definition

Tag 06U6 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsSubmersive, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubmersiveAlgebraicStack.lean, line 77. The attribute's comment: “part (1)”. References: SGA 1 IX (2.1), “submersive”.

Stacks 06U6, part (1). A 1-morphism of algebraic stacks over S is submersive when the map |𝒳| → |𝒴| it induces on the topological spaces of points of Stacks 04XG and 04XL is a quotient map, which is submersiveness in the sense of Stacks 0406.

abbrev IsSubmersive {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.AlgebraicStacks.IsUniversallySubmersive, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubmersiveAlgebraicStack.lean, line 88. The attribute's comment: “part (2)”. References: SGA 1 IX (2.1), “univ. submersive”.

Stacks 06U6, part (2). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is universally submersive when, for every 1-morphism g : 𝒴' ⟶ 𝒴 of algebraic stacks over S, the base change 𝒴' ×_{g, 𝒴, f} 𝒳 ⟶ 𝒴' of f by g is submersive in the sense of AlgebraicGeometry.Stack.AlgebraicStacks.IsSubmersive.

abbrev IsUniversallySubmersive {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

Tag 0CHY, a lemma

Tag 0CHY in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isUniversallySubmersive_baseChange_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyOpenSubmersiveBaseChange.lean, line 221.

Stacks 0CHY. Universal submersiveness is stable under base change: let f : 𝒳 ⟶ 𝒴 be a universally submersive 1-morphism of algebraic stacks over S and let R be a 2-fibre product square of the cospan (g, f) for some g : 𝒴' ⟶ 𝒴. Then the base change R.fst : R.pt ⟶ 𝒴' of f along g is universally submersive.

The square is arbitrary, so this applies to any square a consumer has already exhibited as a 2-fibre product rather than only to the canonical one of Stacks 04T2.

theorem isUniversallySubmersive_baseChange_of_isTwoFibreProduct
    {𝒳 𝒴 𝒴' : Stack.AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴} {g : 𝒴' ⟶ 𝒴}
    (R : Bicategory.TwoCommSq g f) (hR : Bicategory.IsTwoFibreProduct R)
    (hf : IsUniversallySubmersive B S hS f) :
    IsUniversallySubmersive B S hS R.fst

Tag 0CHZ, a lemma

Tag 0CHZ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isSubmersive_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubmersiveComposition.lean, line 84. The attribute's comment: “composition_submersive”.

Stacks 0CHZ. The composite of two submersive 1-morphisms of algebraic stacks over S is submersive.

theorem isSubmersive_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hf : IsSubmersive B S hS f) (hg : IsSubmersive B S hS g) :
    IsSubmersive B S hS (f ≫ g)

AlgebraicGeometry.Stack.AlgebraicStacks.isUniversallySubmersive_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubmersiveUniversalComposition.lean, line 132. The attribute's comment: “composition_universally_submersive”.

Stacks 0CHZ. The composite of two universally submersive 1-morphisms of algebraic stacks over S is universally submersive.

theorem isUniversallySubmersive_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsUniversallySubmersive B S hS f) (hg : IsUniversallySubmersive B S hS g) :
    IsUniversallySubmersive B S hS (f ≫ g)

Sources

LeanAlgebraicGeometry.Stack.representable_universallySubmersive_iff · AlgebraicGeometry.Stack.AlgebraicStacks.IsSubmersive · AlgebraicGeometry.Stack.AlgebraicStacks.IsUniversallySubmersive · AlgebraicGeometry.Stack.AlgebraicStacks.isUniversallySubmersive_baseChange_of_isTwoFibreProduct · AlgebraicGeometry.Stack.AlgebraicStacks.isSubmersive_comp · AlgebraicGeometry.Stack.AlgebraicStacks.isUniversallySubmersive_comp

Section101.13 Universally closed morphisms #

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

Tag 0512, a lemma

Tag 0512 in the Stacks Project.

AlgebraicGeometry.Stack.representable_universallyClosed_iff_closedMap_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedCriterion.lean, line 551.

Stacks 0512. A 1-morphism of algebraic stacks over S which is representable by algebraic spaces is universally closed — the relative property of Tag 04XB at universal closedness of morphisms of algebraic spaces — exactly when, for every algebraic stack 𝒵 over 𝒴, the first projection of the canonical 2-fibre product of Tag 04T2 is a closed map on the points of Tag 04XL.

theorem representable_universallyClosed_iff_closedMap_baseChange
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    UniversallyClosed B S hS f.hom ↔
      ∀ (𝒵 : AlgebraicStacks.{u, w} B S hS) (g : 𝒵 ⟶ 𝒴),
        let P := twoFibreProductSquareAlgebraicStacks B S hS g f
        @IsClosedMap
          (points B S hS P.pt.val.val (Classical.choose P.pt.property))
          (points B S hS 𝒵.val.val (Classical.choose 𝒵.property))
          (pointTopology B S hS P.pt.val)
          (pointTopology B S hS 𝒵.val)
          (pointsMap B S hS P.pt.val.val
            (Classical.choose P.pt.property) (Classical.choose 𝒵.property)
            P.fst.hom.hom)

Tag 0513, a definition

Tag 0513 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsClosed, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ProperAlgebraicStack.lean, line 89. The attribute's comment: “closed”.

Stacks 0513, part (1). A 1-morphism of algebraic stacks over S is closed when the map |𝒳| → |𝒴| it induces on the topological spaces of points of Stacks 04XG and 04XL is a closed map.

abbrev IsClosed {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.AlgebraicStacks.UniversallyClosed, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ProperAlgebraicStack.lean, line 99. The attribute's comment: “universally closed”.

Stacks 0513, part (2). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is universally closed when, for every 1-morphism g : 𝒵 ⟶ 𝒴 of algebraic stacks over S, the base change 𝒵 ×_{g, 𝒴, f} 𝒳 ⟶ 𝒵 of f by g is closed in the sense of AlgebraicGeometry.Stack.AlgebraicStacks.IsClosed.

abbrev UniversallyClosed {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

Tag 0514, a lemma

Tag 0514 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_baseChange_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedBaseChange.lean, line 95.

Stacks 0514. Universal closedness is stable under base change: let f : 𝒳 ⟶ 𝒴 be a universally closed 1-morphism of algebraic stacks over S and let R be a 2-fibre product square of the cospan (g, f) for some g : 𝒴' ⟶ 𝒴. Then the base change R.fst : R.pt ⟶ 𝒴' of f along g is universally closed.

The square is arbitrary, so this applies to any square a consumer has already exhibited as a 2-fibre product rather than only to the canonical one of Stacks 04T2.

theorem universallyClosed_baseChange_of_isTwoFibreProduct
    {𝒳 𝒴 𝒴' : AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴} {g : 𝒴' ⟶ 𝒴}
    (R : Bicategory.TwoCommSq g f) (hR : Bicategory.IsTwoFibreProduct R)
    (hf : UniversallyClosed B S hS f) :
    UniversallyClosed B S hS R.fst

Tag 0515, a lemma

Tag 0515 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedComposition.lean, line 48. The attribute's comment: “closed”.

The composite of two closed 1-morphisms of algebraic stacks over S is closed.

theorem isClosed_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hf : IsClosed B S hS f) (hg : IsClosed B S hS g) :
    IsClosed B S hS (f ≫ g)

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedComposition.lean, line 62. The attribute's comment: “universally closed”.

The composite of two universally closed 1-morphisms of algebraic stacks over S is universally closed.

theorem universallyClosed_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : UniversallyClosed B S hS f) (hg : UniversallyClosed B S hS g) :
    UniversallyClosed B S hS (f ≫ g)

Tag 0CL3, a lemma

Tag 0CL3 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyClosedSmoothLocal.lean, line 483.

Stacks 0CL3. For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S the following are equivalent: f is universally closed; every base change of f to a scheme of the site is closed on points; every base change of f to an affine scheme of the site is closed on points; and there is a smooth surjective 1-morphism from the algebraic stack of an algebraic space to 𝒴 along which the base change of f is universally closed.

theorem universallyClosed_tfae {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    List.TFAE
      [UniversallyClosed B S hS f,
        ∀ (U : BigFppfOver B S hS) (g : Stack.schemeStack.{u, w} B S hS U ⟶ 𝒴),
          IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst,
        ∀ (U : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
          ∀ (g : Stack.schemeStack.{u, w} B S hS U ⟶ 𝒴),
            IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst,
        ∃ (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
            (g : Stack.algebraicSpaceStack.{u, w} B S hS F hF ⟶ 𝒴),
          Stack.IsSurjective B S hS g ∧ IsSmooth B S hS g ∧
            UniversallyClosed B S hS
              (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst]

Sources

LeanAlgebraicGeometry.Stack.representable_universallyClosed_iff_closedMap_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.IsClosed · AlgebraicGeometry.Stack.AlgebraicStacks.UniversallyClosed · AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_baseChange_of_isTwoFibreProduct · AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_comp · AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_comp · AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_tfae

Section101.14 Universally injective morphisms #

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

Tag 0CI1, a lemma

Tag 0CI1 in the Stacks Project.

AlgebraicGeometry.Stack.representable_universallyInjective_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveCriterion.lean, line 62.

Stacks 0CI1. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S representable by algebraic spaces is universally injective in the relative sense of Tag 04XB — every algebraic space representing a base change of f along a scheme-valued point of 𝒴 has universally injective structural morphism — exactly when, for every algebraic stack 𝒵 over 𝒴 and every 2-fibre product of the cospan, the map |𝒵 ×_𝒴 𝒳| → |𝒵| is injective.

theorem representable_universallyInjective_iff
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    (∀ (U : BigFppfOver B S hS) (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.val.obj)
        (_hy : y ⋙ 𝒴.val.val.p = Over.map U.hom)
        (T : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hT : IsAlgebraicSpace B U.left.1 U.left.2 T),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.val.p 𝒴.val.val.p y
            (CatFiberedInGroupoids.homFunctor f.hom))
          (presheafOfCategories (T ⋙ typeToCat)).p) →
        Space.UniversallyInjective B S hS
          (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨T, hT⟩)).hom) ↔
      UniversallyInjective B S hS f

Tag 0CI2, a definition

Tag 0CI2 in the Stacks Project.

AlgebraicGeometry.Stack.UniversallyInjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjective.lean, line 58.

Stacks 0CI2. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is universally injective if for every 1-morphism g : 𝒵 ⟶ 𝒴 of algebraic stacks over S and every 2-fibre product of (g, f) the map |𝒵 ×_𝒴 𝒳| → |𝒵| induced by the projection to 𝒵 is injective.

abbrev UniversallyInjective {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

Tag 0CI3, a lemma

Tag 0CI3 in the Stacks Project.

AlgebraicGeometry.Stack.universallyInjective_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveBaseChange.lean, line 49. References: EGA IV (11.9.14), “base change stability”.

Stacks 0CI3. The base change of a universally injective 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S along any g : 𝒵 ⟶ 𝒴 is universally injective: in a 2-fibre-product square over (g, f), the projection to 𝒵 is universally injective.

theorem universallyInjective_baseChange {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴) (hf : UniversallyInjective B S hS f)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P) :
    UniversallyInjective B S hS P.fst

Tag 0CI4, a lemma

Tag 0CI4 in the Stacks Project.

AlgebraicGeometry.Stack.universallyInjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveComp.lean, line 106.

Stacks 0CI4. The composite of a pair of universally injective 1-morphisms of algebraic stacks over S is universally injective.

theorem universallyInjective_comp {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hf : UniversallyInjective B S hS f)
    (hg : UniversallyInjective B S hS g) :
    UniversallyInjective B S hS (f ≫ g)

Tag 0CPN, a lemma

Tag 0CPN in the Stacks Project.

AlgebraicGeometry.Stack.universallyInjective_iff_isSurjective_relativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveDiagonal.lean, line 221. The attribute's comment: “parts (1) and (2)”.

Stacks 0CPN, parts (1) and (2). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is universally injective if and only if its relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is surjective.

theorem universallyInjective_iff_isSurjective_relativeDiagonal (f : 𝒳 ⟶ 𝒴) :
    UniversallyInjective B S hS f ↔
      IsSurjective B S hS (AlgebraicStacks.relativeDiagonal B S hS f)

AlgebraicGeometry.Stack.isSurjective_relativeDiagonal_of_liftsTwoArrowsAtGeometricPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveGeometricTwoArrows.lean, line 174. The attribute's comment: “part (3) implies part (2)”.

Stacks 0CPN, the implication (3) ⟹ (2). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S which lifts 2-arrows at geometric points has surjective relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳.

A point of |𝒳 ×_𝒴 𝒳| is represented over an algebraically closed field, where it is a triple (x₁, x₂, β); condition (3) writes β as f(α), and then (𝟙, α) is an arrow from Δ_f(x₁) = (x₁, x₁, id) to that triple, so the two represent the same point.

theorem isSurjective_relativeDiagonal_of_liftsTwoArrowsAtGeometricPoints (f : 𝒳 ⟶ 𝒴)
    (h₃ : LiftsTwoArrowsAtGeometricPoints B S hS f) :
    IsSurjective B S hS (AlgebraicStacks.relativeDiagonal B S hS f)

AlgebraicGeometry.Stack.universallyInjective_of_liftsTwoArrowsAtGeometricPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveGeometricTwoArrows.lean, line 209. The attribute's comment: “part (3) implies part (1)”.

Stacks 0CPN, the implication (3) ⟹ (1). A 1-morphism of algebraic stacks over S which lifts 2-arrows at geometric points is universally injective: its relative diagonal is surjective, and parts (1) and (2) of Stacks 0CPN (AlgebraicGeometry.Stack.universallyInjective_iff_isSurjective_relativeDiagonal) conclude.

theorem universallyInjective_of_liftsTwoArrowsAtGeometricPoints (f : 𝒳 ⟶ 𝒴)
    (h₃ : LiftsTwoArrowsAtGeometricPoints B S hS f) :
    UniversallyInjective B S hS f

AlgebraicGeometry.Stack.liftsTwoArrowsAtGeometricPoints_of_isSurjective_relativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveGeometricTwoArrows.lean, line 251. The attribute's comment: “part (2) implies part (3)”.

Stacks 0CPN, the implication (2) ⟹ (3). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S whose relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is surjective lifts 2-arrows at geometric points: for every algebraically closed field k, all x₁, x₂ : Spec k ⟶ 𝒳 and every 2-arrow β : f ∘ x₁ ⟶ f ∘ x₂ there is a 2-arrow α : x₁ ⟶ x₂ with β = id_f ⋆ α.

The triple t = (x₁, x₂, β) is a point of 𝒳 ×_𝒴 𝒳 over Spec k, and the fibre T = 𝒳 ×_{Δ_f, 𝒳 ×_𝒴 𝒳, t} Spec k is an algebraic space locally of finite type over Spec k by Stacks 04XS. Surjectivity of Δ_f makes T nonempty, and since k is algebraically closed T then has a k-point (AlgebraicGeometry.Space.nonempty_obj_base_of_nonempty_points), which is exactly the 2-arrow α.

theorem liftsTwoArrowsAtGeometricPoints_of_isSurjective_relativeDiagonal (f : 𝒳 ⟶ 𝒴)
    (h₂ : IsSurjective B S hS (AlgebraicStacks.relativeDiagonal B S hS f)) :
    LiftsTwoArrowsAtGeometricPoints B S hS f

AlgebraicGeometry.Stack.universallyInjective_iff_liftsTwoArrowsAtGeometricPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveGeometricTwoArrows.lean, line 307. The attribute's comment: “parts (1) and (3)”.

Stacks 0CPN, parts (1) and (3). A 1-morphism of algebraic stacks over S is universally injective if and only if it lifts 2-arrows at geometric points.

theorem universallyInjective_iff_liftsTwoArrowsAtGeometricPoints (f : 𝒳 ⟶ 𝒴) :
    UniversallyInjective B S hS f ↔ LiftsTwoArrowsAtGeometricPoints B S hS f

Tag 0DTM, a lemma

Tag 0DTM in the Stacks Project.

AlgebraicGeometry.Stack.exists_fiber_lift_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveAlgebraicallyClosedPoint.lean, line 685.

Let f : 𝒳 ⟶ 𝒴 be a universally injective 1-morphism of algebraic stacks and y : Spec k ⟶ 𝒴 a morphism with k algebraically closed. If y is in the image of |𝒳| → |𝒴|, then there is x : Spec k ⟶ 𝒳 with y = f ∘ x: an object x of the fibre of 𝒳 over the base of y whose image under f is isomorphic to y in that fibre.

theorem exists_fiber_lift_of_universallyInjective
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : AlgebraicGeometry.Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicGeometry.Stack.UniversallyInjective B S hS f)
    (y : AlgebraicGeometry.Stack.FieldValuedPoint B S hS 𝒴.val.val)
    [IsAlgClosed y.carrier]
    (hy : AlgebraicGeometry.Stack.pointClass B S hS 𝒴.val.val
      𝒴.val.isFiberedInGroupoids y ∈
        Set.range (AlgebraicGeometry.Stack.pointsMap B S hS 𝒳.val.val
          𝒳.val.isFiberedInGroupoids 𝒴.val.isFiberedInGroupoids f.hom.hom)) :
    ∃ x : 𝒳.val.val.p.Fiber y.base,
      Nonempty
        (((Functor.fiberMap 𝒳.val.val.p 𝒴.val.val.p
          f.hom.hom.toFunctor f.hom.hom.w y.base).obj x) ≅
          (⟨y.obj, y.over⟩ : 𝒴.val.val.p.Fiber y.base))

Tag 0DTN, a lemma

Tag 0DTN in the Stacks Project.

AlgebraicGeometry.Stack.universallyInjective_iff_affineBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveAffineLocal.lean, line 112.

Stacks 0DTN. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is universally injective if and only if for every affine scheme U of the big fppf site over S and every 1-morphism from the algebraic stack it represents to 𝒴, the base change of f is universally injective.

The base change is an arbitrary 2-fibre product of the cospan, as in Stacks 0CI2 itself, so neither side depends on a chosen model.

theorem universallyInjective_iff_affineBaseChange (f : 𝒳 ⟶ 𝒴) :
    UniversallyInjective B S hS f ↔
      ∀ (U : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
        ∀ (g : schemeStack.{u, w} B S hS U ⟶ 𝒴) (P : Bicategory.TwoCommSq g f),
          Bicategory.IsTwoFibreProduct P → UniversallyInjective B S hS P.fst

Tag 0DTP, a lemma

Tag 0DTP in the Stacks Project.

AlgebraicGeometry.Stack.universallyInjective_of_fppfCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyInjectiveDescent.lean, line 143. References: EGA IV (11.9.14), “fppf descent clause”.

Stacks 0DTP. Universal injectivity of a 1-morphism of algebraic stacks over S can be checked after base change along a surjective, flat, locally finitely presented 1-morphism from the stack of an algebraic space onto its target.

Only surjectivity of the cover is used; see AlgebraicGeometry.Stack.universallyInjective_of_isSurjective_baseChange.

theorem universallyInjective_of_fppfCover
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hW : IsAlgebraicSpace B S hS W)
    (g : algebraicSpaceStack.{u, w} B S hS W hW ⟶ 𝒴)
    (hgSurj : IsSurjective B S hS g)
    (_hgFlat : AlgebraicStacks.IsFlat B S hS g)
    (_hgLfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (hgf : UniversallyInjective B S hS
      (AlgebraicStacks.twoFibreProductSquare B S hS g f).fst) :
    UniversallyInjective B S hS f

Sources

Section101.15 Universal homeomorphisms #

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

Tag 0CI6, a lemma

Tag 0CI6 in the Stacks Project.

AlgebraicGeometry.Stack.representable_universalHomeomorphism_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversalHomeomorphismCriterion.lean, line 58.

Stacks 0CI6. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S representable by algebraic spaces is a universal homeomorphism in the relative sense of Tag 04XB — every algebraic space representing a base change of f along a scheme-valued point of 𝒴 has structural morphism a universal homeomorphism — exactly when, for every algebraic stack 𝒵 over 𝒴, the map |𝒵 ×_𝒴 𝒳| → |𝒵| of topological spaces is a homeomorphism.

theorem representable_universalHomeomorphism_iff
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    (∀ (U : BigFppfOver B S hS) (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.val.obj)
        (_hy : y ⋙ 𝒴.val.val.p = Over.map U.hom)
        (T : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hT : IsAlgebraicSpace B U.left.1 U.left.2 T),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.val.p 𝒴.val.val.p y
            (CatFiberedInGroupoids.homFunctor f.hom))
          (presheafOfCategories (T ⋙ typeToCat)).p) →
        Space.UniversalHomeomorphism B S hS
          (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨T, hT⟩)).hom) ↔
      AlgebraicStacks.UniversalHomeomorphism B S hS f

Tag 0CI7, a definition

Tag 0CI7 in the Stacks Project.

AlgebraicGeometry.Stack.UniversalHomeomorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversalHomeomorphism.lean, line 68.

Stacks 0CI7. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is a universal homeomorphism if for every 1-morphism g : 𝒵 ⟶ 𝒴 of algebraic stacks over S and every 2-fibre product of (g, f) the map |𝒵 ×_𝒴 𝒳| → |𝒵| induced by the projection to 𝒵 is a homeomorphism.

abbrev UniversalHomeomorphism {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.AlgebraicStacks.UniversalHomeomorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversalHomeomorphismAlgebraicStack.lean, line 136.

Stacks 0CI7. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is a universal homeomorphism when, for every 1-morphism g : 𝒵 ⟶ 𝒴 of algebraic stacks over S, the base change 𝒵 ×_{g, 𝒴, f} 𝒳 ⟶ 𝒵 of f by g induces a homeomorphism |𝒵 ×_𝒴 𝒳| → |𝒵| on the points of Stacks 04XG for the topology of Stacks 04XL.

For a 1-morphism representable by algebraic spaces this agrees with the relative notion of Stacks 04XB, by Stacks 0CI6.

abbrev UniversalHomeomorphism {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

Tag 0CI8, a lemma

Tag 0CI8 in the Stacks Project.

AlgebraicGeometry.Stack.universalHomeomorphism_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversalHomeomorphismBaseChange.lean, line 40.

The base change of a universal homeomorphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S along any g : 𝒵 ⟶ 𝒴 is a universal homeomorphism: in a 2-fibre-product square over (g, f), the projection to 𝒵 is a universal homeomorphism.

theorem universalHomeomorphism_baseChange {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴) (hf : UniversalHomeomorphism B S hS f)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P) :
    UniversalHomeomorphism B S hS P.fst

Tag 0CI9, a lemma

Tag 0CI9 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.universalHomeomorphism_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversalHomeomorphismAlgebraicStack.lean, line 162.

Stacks 0CI9. The composite of two universal homeomorphisms of algebraic stacks over S is a universal homeomorphism.

A base change of f ≫ g along k is the outer rectangle of a base change of g along k followed by a base change of f along the resulting projection, by the pasting law for 2-fibre products; the two legs of that rectangle are homeomorphisms on points by hypothesis, so the rectangle's own first leg is one too, and that condition depends only on the cospan.

theorem universalHomeomorphism_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : UniversalHomeomorphism B S hS f) (hg : UniversalHomeomorphism B S hS g) :
    UniversalHomeomorphism B S hS (f ≫ g)

Tag 0DTQ, a lemma

Tag 0DTQ in the Stacks Project.

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

Stacks 0DTQ. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒲 ⟶ 𝒴 be a surjective, flat, locally finitely presented 1-morphism from the stack of an algebraic space. If the base change 𝒲 ×_𝒴 𝒳 ⟶ 𝒲 of f along g is a universal homeomorphism, then so is f.

theorem universalHomeomorphism_of_fppfCover {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hW : IsAlgebraicSpace B S hS W)
    (g : algebraicSpaceStack.{u, w} B S hS W hW ⟶ 𝒴)
    (hgSurj : IsSurjective B S hS g)
    (hgFlat : AlgebraicStacks.IsFlat B S hS g)
    (hgLfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (hgf : UniversalHomeomorphism B S hS
      (AlgebraicStacks.twoFibreProductSquare B S hS g f).fst) :
    UniversalHomeomorphism B S hS f

Sources

LeanAlgebraicGeometry.Stack.representable_universalHomeomorphism_iff · AlgebraicGeometry.Stack.UniversalHomeomorphism · AlgebraicGeometry.Stack.AlgebraicStacks.UniversalHomeomorphism · AlgebraicGeometry.Stack.universalHomeomorphism_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.universalHomeomorphism_comp · AlgebraicGeometry.Stack.universalHomeomorphism_of_fppfCover

Section101.16 Types of morphisms smooth local on source-and-target #

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

Tag 06FM, a lemma

Tag 06FM in the Stacks Project.

AlgebraicGeometry.Stack.hasPropertyOnEverySmoothDiagram_iff_some, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalMorphismEveryConverse.lean, line 457. The attribute's comment: “equivalence of parts (1) and (2)”.

For a property P of morphisms of algebraic spaces over S which is smooth local on the source-and-target and a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S: every diagram of algebraic spaces over f with smooth vertical 1-morphisms whose comparison to the 2-fibre product is smooth has P on its top horizontal morphism if and only if some such diagram with left vertical 1-morphism surjective on objects does.

theorem hasPropertyOnEverySmoothDiagram_iff_some
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hP : Space.IsSmoothLocalOnSourceAndTarget B S hS P)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴.val)
    (f : 𝒳 ⟶ 𝒴) :
    HasPropertyOnEverySmoothDiagram B S hS P f ↔ HasPropertyOnSomeSmoothDiagram B S hS P f

AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_iff_relative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalMorphismRelative.lean, line 667. The attribute's comment: “representable morphism”.

Stacks 06FM, the assertion for a representable morphism. Let P be a property of morphisms of algebraic spaces over S smooth local on the source-and-target which is moreover stable under base change and local at the target for the fppf precoverage, and let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S representable by algebraic spaces. Then f passes the existential smooth-diagram test of condition (2) exactly when it has the relative property P in the sense of Stacks 03YK, i.e. of Properties of Stacks, Section 04XB.

Algebraicity of the source is not used in either direction; it is kept because it is part of the statement of the tagged assertion.

theorem hasPropertyOnSomeSmoothDiagram_iff_relative
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hP : Space.IsSmoothLocalOnSourceAndTarget B S hS P)
    [(spaceProperty B S hS P).IsStableUnderBaseChange]
    [(spaceProperty B S hS P).IsLocalAtTarget
      (Space.Topology.fppf.precoverage.{u, v} B S hS)]
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (_h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴.val)
    (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom) :
    HasPropertyOnSomeSmoothDiagram B S hS P f ↔
      HasRelativeProperty.{u, u, u + 1, v} B S hS (spaceProperty B S hS P) f hf

AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_iff_represented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalMorphismRepresented.lean, line 252. The attribute's comment: “representable source and target”.

Stacks 06FM, the assertion for representable source and target. For a property P of morphisms of algebraic spaces over S smooth local on the source-and-target, and a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S whose source and target are representable by algebraic spaces F and G, the existential smooth-diagram test of condition (2) holds for f exactly when the induced morphism F ⟶ G of representing presheaves has P.

Forward: the given diagram becomes a diagram of morphisms of algebraic spaces and criterion (3) of Stacks 06FA applies. Backward: test condition (2) on the diagram given by the two representing equivalences.

theorem hasPropertyOnSomeSmoothDiagram_iff_represented
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hP : Space.IsSmoothLocalOnSourceAndTarget B S hS P)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (_h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (_h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴.val)
    (F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (eX : StacksRepresentableCFG.EquivalenceOver
      𝒳.val.p (presheafOfCategories (F ⋙ typeToCat)).p)
    (eY : StacksRepresentableCFG.EquivalenceOver
      𝒴.val.p (presheafOfCategories (G ⋙ typeToCat)).p)
    (f : 𝒳 ⟶ 𝒴) :
    HasPropertyOnSomeSmoothDiagram B S hS P f ↔
      P (representingMap B S hS 𝒳 𝒴 F G eX eY f)

Tag 06FN, a definition

Tag 06FN in the Stacks Project.

AlgebraicGeometry.Stack.HasPropertyOnSomeSmoothDiagram, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalMorphism.lean, line 177. The attribute's comment: “the definition, as condition (2) of Stacks 06FM”.

Condition (2) of Stacks 06FM, and the definition of Stacks 06FN. There is a 2-commutative square of algebraic spaces over f whose two vertical 1-morphisms are smooth, whose left vertical 1-morphism is surjective on objects, and whose top horizontal morphism of algebraic spaces has P.

By Stacks 06FN this is what it means for a 1-morphism of algebraic stacks to have the property P, for P smooth local on the source-and-target: Stacks 06FN defines that notion by the equivalent conditions of Stacks 06FM, and AlgebraicGeometry.Stack.hasPropertyOnEverySmoothDiagram_iff_some is that equivalence, so either condition may serve as the definition. The existential one is taken, because it carries the diagram data its consumers need.

abbrev HasPropertyOnSomeSmoothDiagram
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴) :
    Prop

Tag 06FP, a remark

Tag 06FP in the Stacks Project.

AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalMorphismComp.lean, line 132.

Stacks 06FP. Let P be a property of morphisms of algebraic spaces over S which is smooth local on the source-and-target and whose restriction to algebraic spaces is stable under composition. Then the induced property of 1-morphisms of algebraic stacks over S — the existential smooth-diagram criterion of Stacks 06FM, which is Definition 06FN — is stable under composition.

The proof is the source's. Choose a smooth presentation W ⟶ 𝒵, surjective on objects, by an algebraic space; then a diagram over g whose right vertical 1-morphism is that presentation, which exists by condition (1) of Stacks 06FM — its left vertical 1-morphism is a smooth presentation V ⟶ 𝒴 surjective on objects; then a diagram over f whose right vertical 1-morphism is that one. The two top horizontal morphisms U ⟶ V and V ⟶ W have P by condition (1), so their composite has P by hypothesis, and the outer square is a diagram over f ≫ g whose left vertical 1-morphism is the one of the diagram over f — smooth and surjective on objects — and whose right vertical 1-morphism is the presentation of 𝒵.

theorem hasPropertyOnSomeSmoothDiagram_comp
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hP : Space.IsSmoothLocalOnSourceAndTarget B S hS P)
    (hcomp : ∀ {U V W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u},
      IsAlgebraicSpace B S hS U → IsAlgebraicSpace B S hS V → IsAlgebraicSpace B S hS W →
      ∀ (p : U ⟶ V) (q : V ⟶ W), P p → P q → P (p ≫ q))
    {𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴.val)
    (h𝒵 : IsAlgebraicStack.{u, w} B S hS 𝒵.val)
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : HasPropertyOnSomeSmoothDiagram B S hS P f)
    (hg : HasPropertyOnSomeSmoothDiagram B S hS P g) :
    HasPropertyOnSomeSmoothDiagram B S hS P (f ≫ g)

AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_comp_of_precomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalMorphismCompGeneral.lean, line 168.

Stacks 06FP. Let P be a property of morphisms of algebraic spaces over S which is stable under precomposition with a smooth morphism, stable under composition, and whose restriction to algebraic spaces is stable under base change. The property of 1-morphisms of categories fibred in groupoids over the big fppf site of S that Stacks 06FN attaches to P is stable under composition: if f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 both pass the existential smooth-diagram test of condition (2) of Stacks 06FM, then so does f ≫ g.

Stacks 06FP assumes P smooth local on the source-and-target, which is what makes the property of Stacks 06FN well behaved; of its three clauses only precomposition-stability is used here, so the hypothesis is taken in that weaker form and AlgebraicGeometry.Space.IsSmoothLocalOnSourceAndTarget.precomp is what a caller holding the full condition supplies. No hypothesis is made on the three categories beyond their being fibred in groupoids: the diagram is built from the two given ones, so no presentation of 𝒵 is chosen. See the implementation notes of this module, which also compare this with the sibling AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_comp.

theorem hasPropertyOnSomeSmoothDiagram_comp_of_precomp
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hprecomp : ∀ {X₀ Y₀ Z₀ : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
      (_hX : IsAlgebraicSpace B S hS X₀) (_hY : IsAlgebraicSpace B S hS Y₀)
      (_hZ : IsAlgebraicSpace B S hS Z₀) (p : X₀ ⟶ Y₀) (q : Y₀ ⟶ Z₀),
      Space.IsSmooth B S hS p → P q → P (p ≫ q))
    (hcomp : ∀ {X₀ Y₀ Z₀ : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
      (_hX : IsAlgebraicSpace B S hS X₀) (_hY : IsAlgebraicSpace B S hS Y₀)
      (_hZ : IsAlgebraicSpace B S hS Z₀) (p : X₀ ⟶ Y₀) (q : Y₀ ⟶ Z₀),
      P p → P q → P (p ≫ q))
    [(spaceProperty B S hS P).IsStableUnderBaseChange]
    {𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : HasPropertyOnSomeSmoothDiagram B S hS P f)
    (hg : HasPropertyOnSomeSmoothDiagram B S hS P g) :
    HasPropertyOnSomeSmoothDiagram B S hS P (f ≫ g)

Tag 06FQ, a remark

Tag 06FQ in the Stacks Project.

AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalMorphismBaseChange.lean, line 529.

A property of morphisms of algebraic spaces over S which is smooth local on the source-and-target and whose restriction to algebraic spaces is stable under base change induces, through the existential smooth-diagram criterion of Stacks 06FM, a property of 1-morphisms of algebraic stacks over S stable under arbitrary 2-fibre-product base change.

theorem hasPropertyOnSomeSmoothDiagram_baseChange
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (_hP : Space.IsSmoothLocalOnSourceAndTarget B S hS P)
    [hbase : (spaceProperty B S hS P).IsStableUnderBaseChange]
    {𝒳 𝒴 𝒴' : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (Q : Bicategory.TwoCommSq g f)
    (hQ : Bicategory.IsTwoFibreProduct Q)
    (hf : HasPropertyOnSomeSmoothDiagram B S hS P f.hom) :
    HasPropertyOnSomeSmoothDiagram B S hS P Q.fst.hom

Tag 06PS, a remark

Tag 06PS in the Stacks Project.

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

Stacks 06PS. An implication between two properties of morphisms of algebraic spaces over S induces the same implication for 1-morphisms of algebraic stacks over S: the existential smooth-diagram criterion of Stacks 06FM is monotone in the property it tests.

The same diagram witnesses both: its top horizontal morphism is a morphism of algebraic spaces and has the first property, hence the second.

theorem hasPropertyOnSomeSmoothDiagram_mono
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P P' : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hPP' : ∀ {U V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u},
      IsAlgebraicSpace B S hS U → IsAlgebraicSpace B S hS V →
      ∀ (g : U ⟶ V), P g → P' g)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴)
    (hf : HasPropertyOnSomeSmoothDiagram B S hS P f) :
    HasPropertyOnSomeSmoothDiagram B S hS P' f

Sources

Section101.17 Morphisms of finite type #

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

Tag 06FS, a definition

Tag 06FS in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsLocallyOfFiniteType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypeAlgebraicStack.lean, line 56. The attribute's comment: “part (1): locally of finite type”.

A 1-morphism f of algebraic stacks over S is locally of finite type when every 2-commutative square of algebraic spaces over f whose two vertical 1-morphisms are smooth and whose every comparison 1-morphism to a 2-fibre product is smooth has its top horizontal morphism locally of finite type.

abbrev IsLocallyOfFiniteType {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.AlgebraicStacks.IsFiniteType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypeAlgebraicStack.lean, line 63. The attribute's comment: “part (2): finite type”.

A 1-morphism of algebraic stacks over S is of finite type when it is locally of finite type and quasi-compact.

abbrev IsFiniteType {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

Tag 06FT, a lemma

Tag 06FT in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FinitenessComposition.lean, line 110. The attribute's comment: “locally of finite type”.

Stacks 06FT, the local assertion. The composite of two 1-morphisms of algebraic stacks over S which are locally of finite type is locally of finite type.

Stacks 06FS part (1) is condition (1) of Stacks 06FM at local finite type of morphisms of algebraic spaces, so this is Stacks 06FP at that property, transported across the equivalence of conditions (1) and (2) of Stacks 06FM. Local finite type is smooth local on the source-and-target by Stacks 06FC and stable under composition by Stacks 03XG.

theorem isLocallyOfFiniteType_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g) :
    IsLocallyOfFiniteType B S hS (f ≫ g)

AlgebraicGeometry.Stack.AlgebraicStacks.isFiniteType_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FinitenessComposition.lean, line 127. The attribute's comment: “finite type”.

Stacks 06FT, the global assertion. The composite of two finite type 1-morphisms of algebraic stacks over S is of finite type.

Being of finite type is being locally of finite type together with being quasi-compact (Stacks 06FS, part (2)); the first conjunct composes by the local assertion above and the second by Stacks 050W.

theorem isFiniteType_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsFiniteType B S hS f) (hg : IsFiniteType B S hS g) :
    IsFiniteType B S hS (f ≫ g)

Tag 06FU, a lemma

Tag 06FU in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FinitenessBaseChange.lean, line 89. The attribute's comment: “locally of finite type”.

Stacks 06FU, the local assertion. A base change of a 1-morphism of algebraic stacks over S which is locally of finite type is locally of finite type: if P is a 2-fibre product of the cospan (g, f) and f is locally of finite type, then the projection P.fst is locally of finite type.

This is the base-change remark Stacks 06FQ at local finite type of morphisms of algebraic spaces, transported across the equivalence of conditions (1) and (2) of Stacks 06FM, since Stacks 06FS part (1) is the universal criterion where Stacks 06FQ concludes about the existential one. Local finite type is smooth local on the source-and-target by Stacks 06FC and stable under base change by Stacks 03XH.

theorem isLocallyOfFiniteType_baseChange {𝒳 𝒴 𝒴' : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (P : Bicategory.TwoCommSq g f)
    (hP : Bicategory.IsTwoFibreProduct P)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyOfFiniteType B S hS P.fst

AlgebraicGeometry.Stack.AlgebraicStacks.isFiniteType_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FinitenessBaseChange.lean, line 117. The attribute's comment: “finite type”.

Stacks 06FU, the global assertion. A base change of a finite type 1-morphism of algebraic stacks over S is of finite type.

Being of finite type is being locally of finite type together with being quasi-compact (Stacks 06FS, part (2)); the first conjunct base changes by the local assertion above and the second by Stacks 050V.

theorem isFiniteType_baseChange {𝒳 𝒴 𝒴' : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (P : Bicategory.TwoCommSq g f)
    (hP : Bicategory.IsTwoFibreProduct P)
    (hf : IsFiniteType B S hS f) :
    IsFiniteType B S hS P.fst

Tag 06FV, a lemma

Tag 06FV in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionFiniteness.lean, line 99.

Stacks 06FV. An immersion of algebraic stacks over S is locally of finite type.

By Stacks 04YL the 1-morphism is representable by algebraic spaces and every algebraic space representing a base change of it along a scheme-valued point of the target has immersion structural morphism, hence by Stacks 06ED has structural morphism locally of finite type. That is the relative property of Stacks 03YK at local finite type of morphisms of algebraic spaces, which Stacks 06FM equates with the universal smooth-diagram test defining local finite type of the 1-morphism.

theorem isLocallyOfFiniteType_of_isImmersion
    (f : 𝒳 ⟶ 𝒴) (hf : IsImmersion B S hS f) :
    IsLocallyOfFiniteType B S hS f

Tag 06R6, a lemma

Tag 06R6 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyNoetherian_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianAlgebraicStack.lean, line 310.

Stacks 06R6. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. If f is locally of finite type and 𝒴 is locally Noetherian, then 𝒳 is locally Noetherian. Local Noetherianity of an algebraic stack over S is the smooth-scheme-atlas criterion of Stacks 04YG at AlgebraicGeometry.IsLocallyNoetherian.

The source argues with scheme charts; here the whole argument runs on algebraic-space charts, which is what the chapter's vocabulary already supports, and the scheme criterion is reached at the two ends by Stacks 04YF. A smooth diagram over f is a pair of algebraic-space charts a : U ⟶ 𝒳 and b : V ⟶ 𝒴 whose top horizontal morphism h : U ⟶ V is locally of finite type, with a moreover surjective on objects; V is then a smooth algebraic-space chart of 𝒴, so it has the étale-local property of Stacks 03E6 at local Noetherianity, and Stacks 04ZK carries that along h to U. Since a is a smooth surjective algebraic-space atlas of 𝒳, that is the third criterion of Stacks 04YF for 𝒳.

theorem isLocallyNoetherian_of_isLocallyOfFiniteType
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (hf : IsLocallyOfFiniteType B S hS f)
    (hY : HasPropertyOnSomeSchemeAtlas B S hS
      (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴) :
    HasPropertyOnSomeSchemeAtlas B S hS
      (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒳

Tag 06U7, a lemma

Tag 06U7 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_of_baseChange_algebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypeFppfBaseChange.lean, line 123.

Stacks 06U7. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : W ⟶ 𝒴 be surjective, flat and locally of finite presentation, where W is an algebraic space over S. If the base change W ×_𝒴 𝒳 ⟶ W of f along g is locally of finite type, then so is f.

theorem isLocallyOfFiniteType_of_baseChange_algebraicSpace
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hW : IsAlgebraicSpace B S hS W)
    (g : Stack.algebraicSpaceStack.{u, w} B S hS W hW ⟶ 𝒴)
    (hgsurj : Stack.IsSurjective B S hS g)
    (hgflat : IsFlat B S hS g)
    (hglfp : IsLocallyOfFinitePresentation B S hS g)
    (hbase : IsLocallyOfFiniteType B S hS
      (Stack.twoFibreProductSquareAlgebraicStacks B S hS f g).snd) :
    IsLocallyOfFiniteType B S hS f

Tag 06U8, a lemma

Tag 06U8 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_of_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypeFppfDescent.lean, line 250.

Let f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 be 1-morphisms of algebraic stacks over S. If f ≫ g is locally of finite type and f is representable by algebraic spaces, surjective, flat and locally of finite presentation, then g is locally of finite type.

theorem isLocallyOfFiniteType_of_comp_of_fppf
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsLocallyOfFiniteType B S hS (f ≫ g))
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hfsurj : IsSurjective B S hS f)
    (hfflat : IsFlat B S hS f)
    (hflfp : IsLocallyOfFinitePresentation B S hS f) :
    IsLocallyOfFiniteType B S hS g

Tag 06U9, a lemma

Tag 06U9 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalMorphismCancellation.lean, line 292.

Let f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 be 1-morphisms of algebraic stacks over S. If f ≫ g is locally of finite type, then so is f.

theorem isLocallyOfFiniteType_of_comp
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsLocallyOfFiniteType B S hS (f ≫ g)) :
    IsLocallyOfFiniteType B S hS f

Sources

LeanAlgebraicGeometry.Stack.AlgebraicStacks.IsLocallyOfFiniteType · AlgebraicGeometry.Stack.AlgebraicStacks.IsFiniteType · AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_comp · AlgebraicGeometry.Stack.AlgebraicStacks.isFiniteType_comp · AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.isFiniteType_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_of_isImmersion · AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyNoetherian_of_isLocallyOfFiniteType

Section101.18 Points of finite type #

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

Tag 06FX, a lemma

Tag 06FX in the Stacks Project.

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

Stacks 06FX, condition (2) implies condition (1). Let x be a point of an algebraic stack 𝒳 over S. If there are a scheme U of the site, a closed point of U, and a smooth 1-morphism from the algebraic stack of U to 𝒳 carrying that point to x, then some field-valued point representing x has a 1-morphism Spec k ⟶ 𝒳 which is locally of finite type, i.e. x is a finite type point in the sense of Stacks 06FY.

The point of U is the closed point, a smooth 1-morphism is locally of finite type, and Stacks 06G0 carries finite type points along a 1-morphism locally of finite type.

theorem isFiniteTypePoint_of_exists_isClosed_smoothChart
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (x : points B S hS 𝒳.val.val 𝒳.val.property)
    (h : ∃ (U : BigFppfOver B S hS) (φ : schemeStack.{u, w} B S hS U ⟶ 𝒳)
        (z : points B S hS (schemeFibredCategory B S hS U).val
          (schemeFibredCategory B S hS U).property),
        AlgebraicStacks.IsSmooth B S hS φ ∧
          IsClosed ({pointsHomeomorphScheme B S hS U z} :
            Set ((BigFppfOver.toScheme B S hS).obj U)) ∧
          pointsMap B S hS (schemeFibredCategory B S hS U).val
            (schemeFibredCategory B S hS U).property 𝒳.val.property φ.hom.hom z = x) :
    IsFiniteTypePoint.{u, w} B S hS 𝒳 x

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

Stacks 06FX, condition (1) implies condition (2). A finite type point x of an algebraic stack 𝒳 over S (Stacks 06FY) is the image of a closed point of a scheme of the site carrying a smooth 1-morphism to 𝒳.

A smooth surjective scheme chart a : U ⟶ 𝒳 has a finite type point above x, and by Stacks 06EF such a point is the image of a closed point of a scheme V étale over U. An étale morphism of schemes is smooth, so the composite V ⟶ U ⟶ 𝒳 is smooth by Stacks 075V, and it carries that closed point to x.

theorem exists_isClosed_smoothChart_of_isFiniteTypePoint
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (x : points B S hS 𝒳.val.val 𝒳.val.property)
    (hx : IsFiniteTypePoint.{u, w} B S hS 𝒳 x) :
    ∃ (U : BigFppfOver B S hS) (φ : schemeStack.{u, w} B S hS U ⟶ 𝒳)
      (z : points B S hS (schemeFibredCategory B S hS U).val
        (schemeFibredCategory B S hS U).property),
      AlgebraicStacks.IsSmooth B S hS φ ∧
        IsClosed ({pointsHomeomorphScheme B S hS U z} :
          Set ((BigFppfOver.toScheme B S hS).obj U)) ∧
        pointsMap B S hS (schemeFibredCategory B S hS U).val
          (schemeFibredCategory B S hS U).property 𝒳.val.property φ.hom.hom z = x

AlgebraicGeometry.Stack.exists_isClosed_smoothChart_size_le_of_isFiniteTypePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointSmoothChart.lean, line 688. The attribute's comment: “condition (1) implies condition (2), with the chart's size bounded by that of a given smooth surjective chart”.

Stacks 06FX, condition (1) implies condition (2), with the chart no larger than a given smooth surjective chart. Let a : U₀ ⟶ 𝒳 be a smooth surjective 1-morphism out of a scheme of the site. Then a finite type point x of 𝒳 is the image of a closed point of a scheme U of the site carrying a smooth 1-morphism to 𝒳 whose size is at most that of U₀ and whose underlying scheme is affine.

The proof of AlgebraicGeometry.Stack.exists_isClosed_smoothChart_of_isFiniteTypePoint run at the given chart rather than at one chosen for the occasion, and with the affine form of Stacks 06EH (AlgebraicGeometry.Space.isFiniteTypePoint_iff_exists_isAffine_isClosed_etaleChart) in place of the general one: the chart it produces is then an affine scheme étale over U₀, so it is quasi-compact and locally of finite type over U₀, and Stacks 04T7 (AlgebraicGeometry.Scheme.size_le_of_locallyOfFiniteType) bounds its size by that of U₀. The affineness is recorded in the conclusion as well: the chart construction of Stacks 06N3 reads its slicing sequence in the global functions of the chart, and on an affine chart it may do so with no shrinking, by AlgebraicGeometry.exists_global_isRegular_ofList_eq_maximalIdeal_stalk_of_unramifiedAt.

This is the form the chart construction of Stacks 06MF needs: the charts it cuts out of these are indexed by the finite type points of 𝒳, a set which need not be below the cofinality of the site's size cutoff, so their coproduct lies in the site by AlgebraicGeometry.BigFppfSite.contains_sigma_of_forall_size_le and that asks for a bound on their sizes which is uniform in the point.

theorem exists_isClosed_smoothChart_size_le_of_isFiniteTypePoint
    (𝒳 : AlgebraicStacks.{u, w} B S hS) (U₀ : BigFppfOver B S hS)
    (a : schemeStack.{u, w} B S hS U₀ ⟶ 𝒳)
    (hasm : AlgebraicStacks.IsSmooth B S hS a) (hasurj : IsSurjective B S hS a)
    (x : points B S hS 𝒳.val.val 𝒳.val.property)
    (hx : IsFiniteTypePoint.{u, w} B S hS 𝒳 x) :
    ∃ (U : BigFppfOver B S hS) (φ : schemeStack.{u, w} B S hS U ⟶ 𝒳)
      (z : points B S hS (schemeFibredCategory B S hS U).val
        (schemeFibredCategory B S hS U).property),
      AlgebraicStacks.IsSmooth B S hS φ ∧
        IsClosed ({pointsHomeomorphScheme B S hS U z} :
          Set ((BigFppfOver.toScheme B S hS).obj U)) ∧
        pointsMap B S hS (schemeFibredCategory B S hS U).val
          (schemeFibredCategory B S hS U).property 𝒳.val.property φ.hom.hom z = x ∧
        ((BigFppfOver.toScheme B S hS).obj U).size ≤
          ((BigFppfOver.toScheme B S hS).obj U₀).size ∧
        IsAffine ((BigFppfOver.toScheme B S hS).obj U)

Tag 06FY, a definition

Tag 06FY in the Stacks Project.

AlgebraicGeometry.Stack.IsFiniteTypePoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointAlgebraicStack.lean, line 78. The attribute's comment: “finite_type_point”.

Stacks 06FY. A point of an algebraic stack 𝒳 over S is a finite type point when some field-valued point representing it has a locally-of-finite-type 1-morphism Spec k → 𝒳.

This is condition (1) of Stacks 06FX.

abbrev IsFiniteTypePoint (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (x : points B S hS 𝒳.val.val 𝒳.val.property) : Prop

AlgebraicGeometry.Stack.finiteTypePoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointAlgebraicStack.lean, line 88. The attribute's comment: “finite_type_points_set”.

Stacks 06FY. The set 𝒳_{ft-pts} of finite type points of an algebraic stack 𝒳 over S.

abbrev finiteTypePoints (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    Set (points B S hS 𝒳.val.val 𝒳.val.property)

Tag 06FZ, a lemma

Tag 06FZ in the Stacks Project.

AlgebraicGeometry.Stack.affineSmoothChartClosedPoints_eq_smoothChartClosedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsSmoothUnion.lean, line 191. The attribute's comment: “the union over all schemes smooth over the stack equals the union over the affine schemes smooth over it”.

Stacks 06FZ, the agreement of the two ranges. The union of the images of the closed points of the schemes of the site smooth over an algebraic stack 𝒳 over S is unchanged when the schemes are restricted to the affine ones.

A closed point of a chart U is a closed point of an affine open V ⊆ U containing it, the inclusion of V is an open immersion and hence smooth, and the composite of the induced 1-morphism with the chart is smooth by Stacks 075V.

theorem affineSmoothChartClosedPoints_eq_smoothChartClosedPoints
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    affineSmoothChartClosedPoints.{u, w} B S hS 𝒳 =
      smoothChartClosedPoints.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.smoothChartClosedPoints_subset_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsSmoothUnion.lean, line 220. The attribute's comment: “the inclusion of the union over all schemes smooth over the stack in the set of finite type points, i.e. the ⊇ direction of the set equality”.

Stacks 06FZ, the inclusion of the union in the set of finite type points. Every image of a closed point of a scheme of the site smooth over an algebraic stack 𝒳 over S is a finite type point of 𝒳 (Stacks 06FY).

This is condition (2) of Stacks 06FX implying condition (1).

theorem smoothChartClosedPoints_subset_finiteTypePoints
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    smoothChartClosedPoints.{u, w} B S hS 𝒳 ⊆ finiteTypePoints B S hS 𝒳

AlgebraicGeometry.Stack.finiteTypePoints_subset_smoothChartClosedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsSmoothUnion.lean, line 236. The attribute's comment: “the inclusion of the set of finite type points in the union over all schemes smooth over the stack, i.e. the ⊆ direction of the set equality”.

Stacks 06FZ, the inclusion of the set of finite type points in the union. Every finite type point of an algebraic stack 𝒳 over S (Stacks 06FY) is the image of a closed point of a scheme of the site smooth over 𝒳.

This is the restatement as a subset relation of condition (1) of Stacks 06FX implying condition (2).

theorem finiteTypePoints_subset_smoothChartClosedPoints
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    finiteTypePoints B S hS 𝒳 ⊆ smoothChartClosedPoints.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.finiteTypePoints_eq_smoothChartClosedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsSmoothUnion.lean, line 249. The attribute's comment: “the set equality 𝒳_{ft-pts} = ⋃_{φ : U ⟶ 𝒳 smooth} |φ|(U₀) over all schemes smooth over the stack”.

Stacks 06FZ, the set equality. The set 𝒳_{ft-pts} of finite type points of an algebraic stack 𝒳 over S is the union ⋃_{φ : U ⟶ 𝒳 smooth} |φ|(U₀) of the images of the sets of closed points of the schemes of the site smooth over 𝒳.

theorem finiteTypePoints_eq_smoothChartClosedPoints
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    finiteTypePoints B S hS 𝒳 = smoothChartClosedPoints.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.affineSmoothChartClosedPoints_subset_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsSmoothUnion.lean, line 259. The attribute's comment: “the inclusion of the union over the affine schemes smooth over the stack in the set of finite type points, i.e. the ⊇ direction of the set equality for the affine range”.

The union over the affine schemes of the site smooth over an algebraic stack 𝒳 over S is contained in the set of finite type points of 𝒳.

theorem affineSmoothChartClosedPoints_subset_finiteTypePoints
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    affineSmoothChartClosedPoints.{u, w} B S hS 𝒳 ⊆ finiteTypePoints B S hS 𝒳

AlgebraicGeometry.Stack.finiteTypePoints_eq_affineSmoothChartClosedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsSmoothUnion.lean, line 270. The attribute's comment: “the set equality 𝒳_{ft-pts} = ⋃_{φ : U ⟶ 𝒳 smooth} |φ|(U₀) over the affine schemes smooth over the stack”.

Stacks 06FZ, the set equality for the affine range. The set 𝒳_{ft-pts} of finite type points of an algebraic stack 𝒳 over S is the union ⋃_{φ : U ⟶ 𝒳 smooth} |φ|(U₀) of the images of the sets of closed points of the affine schemes of the site smooth over 𝒳.

theorem finiteTypePoints_eq_affineSmoothChartClosedPoints
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    finiteTypePoints B S hS 𝒳 = affineSmoothChartClosedPoints.{u, w} B S hS 𝒳

Tag 06G0, a lemma

Tag 06G0 in the Stacks Project.

AlgebraicGeometry.Stack.mapsTo_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsMorphism.lean, line 92.

Stacks 06G0. A 1-morphism of algebraic stacks over S which is locally of finite type maps the set of finite type points of its source into the set of finite type points of its target.

A field-valued representative of a finite type point of the source has a locally-of-finite-type 1-morphism, and its image represents the image point; the image's 1-morphism is 2-isomorphic to the composite of that one with f, which is locally of finite type by Stacks 06FT.

theorem mapsTo_finiteTypePoints {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f) :
    Set.MapsTo
      (Stack.pointsMap B S hS 𝒳.val.val 𝒳.val.property 𝒴.val.property f.hom.hom)
      (finiteTypePoints B S hS 𝒳) (finiteTypePoints B S hS 𝒴)

Tag 06G1, a lemma

Tag 06G1 in the Stacks Project.

AlgebraicGeometry.Stack.image_finiteTypePoints_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsSurjective.lean, line 123.

Stacks 06G1. A surjective 1-morphism of algebraic stacks over S which is locally of finite type maps the set of finite type points of its source onto the set of finite type points of its target.

That the image is contained in 𝒴_{ft-pts} is Stacks 06G0. Conversely a finite type point of 𝒴 is represented by a field-valued point whose 1-morphism out of the algebraic stack of the spectrum of a field is locally of finite type, and that spectrum has a single point, so AlgebraicGeometry.Stack.mem_image_finiteTypePoints_of_subsingleton applies to it.

theorem image_finiteTypePoints_of_isSurjective {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (hsurj : IsSurjective B S hS f) :
    Stack.pointsMap B S hS 𝒳.val.val 𝒳.val.property 𝒴.val.property f.hom.hom ''
        finiteTypePoints B S hS 𝒳 = finiteTypePoints B S hS 𝒴

Tag 06G2, a lemma

Tag 06G2 in the Stacks Project.

AlgebraicGeometry.Stack.closure_inter_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsDense.lean, line 153. The attribute's comment: “closed subsets, in the spelling of the scheme-level Stacks 02J4 and the algebraic-space-level Stacks 06EK: for a closed subset of the point space, the closure of its intersection with the set of finite type points is the subset itself”.

For a closed subset T of the point space of an algebraic stack 𝒳, the closure of the set of finite type points lying in T is T itself; that is, T ∩ 𝒳_{ft-pts} is dense in T.

theorem closure_inter_finiteTypePoints (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    letI := pointTopology B S hS 𝒳.val
    ∀ T : Set (points B S hS 𝒳.val.val 𝒳.val.property), IsClosed T →
      closure (T ∩ finiteTypePoints B S hS 𝒳) = T

AlgebraicGeometry.Stack.nonempty_inter_and_closure_inter_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsDense.lean, line 170. The attribute's comment: “both assertions: for a locally closed subset T of the point space of an algebraic stack, T nonempty implies that T meets the set of finite type points; and in particular, for a closed subset T, the intersection of T with the set of finite type points is dense in T”.

Let 𝒳 be an algebraic stack over S. Then

for any locally closed subset T ⊆ |𝒳| of its point space, T ≠ ∅ → T ∩ 𝒳_{ft-pts} ≠ ∅; and

in particular, for any closed subset T ⊆ |𝒳| the closure of T ∩ 𝒳_{ft-pts} is T, that is, T ∩ 𝒳_{ft-pts} is dense in T.

theorem nonempty_inter_and_closure_inter_finiteTypePoints
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    letI := pointTopology B S hS 𝒳.val
    (∀ T : Set (points B S hS 𝒳.val.val 𝒳.val.property), IsLocallyClosed T → T.Nonempty →
        (T ∩ finiteTypePoints B S hS 𝒳).Nonempty) ∧
      ∀ T : Set (points B S hS 𝒳.val.val 𝒳.val.property), IsClosed T →
        closure (T ∩ finiteTypePoints B S hS 𝒳) = T

AlgebraicGeometry.Stack.nonempty_inter_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsLocallyClosed.lean, line 188. The attribute's comment: “the first clause: a nonempty locally closed subset of the point space meets the set of finite type points. The reduced induced substack structure of Stacks 06FK on a locally closed subset is carried as the hypothesis hsub, since Stacks 06FK is absent from this library; the rest of the proof, including the existence of a finite type point on a nonempty algebraic stack, is proved”.

Stacks 06G2, first clause. A nonempty locally closed subset of the point space of an algebraic stack contains a finite type point.

The reduced induced substack 𝒵 of T is nonempty because its image on points is T, so it has a finite type point by AlgebraicGeometry.Stack.exists_isFiniteTypePoint_of_nonempty; the image of that point is a finite type point of 𝒳 by Stacks 06G0 and lies in T.

The substack is carried as AlgebraicGeometry.Stack.HasReducedInducedSubstacks, which stands for Stacks 06FK; everything else is proved.

theorem nonempty_inter_finiteTypePoints (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hsub : HasReducedInducedSubstacks.{u, w} B S hS 𝒳) :
    letI := pointTopology B S hS 𝒳.val
    ∀ T : Set (points B S hS 𝒳.val.val 𝒳.val.property), IsLocallyClosed T → T.Nonempty →
      (T ∩ finiteTypePoints B S hS 𝒳).Nonempty

AlgebraicGeometry.Stack.subset_closure_inter_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsLocallyClosed.lean, line 213. The attribute's comment: “the second clause: for a closed subset of the point space, its intersection with the set of finite type points is dense in it. Derived from the first clause by topology alone, so it carries exactly the same Stacks 06FK hypothesis hsub and nothing further”.

Stacks 06G2, second clause. For a closed subset T of the point space of an algebraic stack, the finite type points lying in T are dense in T.

This follows from the first clause by pure topology: given x ∈ T and an open V containing x, the set T ∩ V is locally closed and nonempty, so it meets the set of finite type points, which is exactly the statement that V meets T ∩ 𝒳_{ft-pts}.

theorem subset_closure_inter_finiteTypePoints (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hsub : HasReducedInducedSubstacks.{u, w} B S hS 𝒳) :
    letI := pointTopology B S hS 𝒳.val
    ∀ T : Set (points B S hS 𝒳.val.val 𝒳.val.property), IsClosed T →
      T ⊆ closure (T ∩ finiteTypePoints B S hS 𝒳)

AlgebraicGeometry.Stack.exists_mem_finiteTypePoints_of_isLocallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsLocallyClosedChart.lean, line 46. The attribute's comment: “the first clause: a nonempty locally closed subset of the point space meets the set of finite type points”.

A nonempty locally closed subset of the point space of an algebraic stack contains a finite type point.

theorem exists_mem_finiteTypePoints_of_isLocallyClosed (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    letI := pointTopology B S hS 𝒳.val
    ∀ T : Set (points B S hS 𝒳.val.val 𝒳.val.property), IsLocallyClosed T → T.Nonempty →
      (T ∩ finiteTypePoints B S hS 𝒳).Nonempty

AlgebraicGeometry.Stack.subset_closure_inter_finiteTypePoints_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointsLocallyClosedChart.lean, line 115. The attribute's comment: “the second clause: for a closed subset of the point space, its intersection with the set of finite type points is dense in it”.

For a closed subset T of the point space of an algebraic stack, the finite type points lying in T are dense in T.

theorem subset_closure_inter_finiteTypePoints_of_isClosed (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    letI := pointTopology B S hS 𝒳.val
    ∀ T : Set (points B S hS 𝒳.val.val 𝒳.val.property), IsClosed T →
      T ⊆ closure (T ∩ finiteTypePoints B S hS 𝒳)

Tag 06G3, a lemma

Tag 06G3 in the Stacks Project.

AlgebraicGeometry.Stack.isFiniteTypePoint_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointResidualGerbe.lean, line 189. The attribute's comment: “the equivalence of (1) being a finite type point, (2) admitting a locally-of-finite-type 1-morphism from a one-point algebraic stack with image the point, and (3) the residual gerbe existing with locally-of-finite-type inclusion. The implications (3) => (2) and (2) => (1) are proved; (1) => (3) is carried as the hypothesis hForward, since Stacks 06FI, 04ZZ and 06MX are absent from this library and it has no construction of a residual gerbe”.

Stacks 06G3. For a point x of the point space of an algebraic stack 𝒳 over S, the following are equivalent: x is a finite type point; there is a one-point algebraic stack with a locally-of-finite-type 1-morphism to 𝒳 whose image on points is {x}; the residual gerbe of 𝒳 at x exists and its inclusion is locally of finite type.

The implication (1) ⟹ (3) is carried as the hypothesis hForward; see AlgebraicGeometry.Stack.ExistsLocallyOfFiniteTypeResidualGerbeOfIsFiniteTypePoint for what it stands for and why. The other two implications are proved.

theorem isFiniteTypePoint_tfae (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hForward : ExistsLocallyOfFiniteTypeResidualGerbeOfIsFiniteTypePoint.{u, w} B S hS 𝒳)
    (x : points B S hS 𝒳.val.val 𝒳.val.property) :
    [IsFiniteTypePoint.{u, w} B S hS 𝒳 x,
      HasSingletonLocallyOfFiniteTypeCoverAt.{u, w} B S hS 𝒳 x,
      HasLocallyOfFiniteTypeResidualGerbeAt.{u, w} B S hS 𝒳 x].TFAE

AlgebraicGeometry.Stack.isFiniteTypePoint_tfae_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypePointResidualGerbeExistence.lean, line 175. The attribute's comment: “the equivalence of (1) being a finite type point, (2) admitting a locally-of-finite-type 1-morphism from a one-point algebraic stack with image the point, and (3) the residual gerbe existing with locally-of-finite-type inclusion. All three implications are proved and nothing is assumed: (1) => (3) cuts the one-point algebraic stack out of the target as the strictly full subcategory of the objects fppf-locally in the image of the field-valued point, whose inclusion is fully faithful and, by Stacks 05UM at the bootstrap theorem Stacks 04S6 part (3), representable by algebraic spaces”.

Stacks 06G3. For a point x of the point space of an algebraic stack 𝒳 over S, the following are equivalent: x is a finite type point; there is a one-point algebraic stack with a locally-of-finite-type 1-morphism to 𝒳 whose image on points is {x}; the residual gerbe of 𝒳 at x exists and its inclusion is locally of finite type.

All three implications are proved. (1) ⟹ (3) is AlgebraicGeometry.Stack.existsLocallyOfFiniteTypeResidualGerbe, which builds the one-point algebraic stack as the strictly full subcategory of the objects of 𝒳 fppf-locally in the image of the field-valued point of condition (1) of Stacks 06FX; (3) ⟹ (2) is AlgebraicGeometry.Stack.hasSingletonLocallyOfFiniteTypeCoverAt_of_residualGerbe and (2) ⟹ (1) is AlgebraicGeometry.Stack.isFiniteTypePoint_of_hasSingletonLocallyOfFiniteTypeCoverAt.

theorem isFiniteTypePoint_tfae_unconditional (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (x : points B S hS 𝒳.val.val 𝒳.val.property) :
    [IsFiniteTypePoint.{u, w} B S hS 𝒳 x,
      HasSingletonLocallyOfFiniteTypeCoverAt.{u, w} B S hS 𝒳 x,
      HasLocallyOfFiniteTypeResidualGerbeAt.{u, w} B S hS 𝒳 x].TFAE

Sources

LeanAlgebraicGeometry.Stack.isFiniteTypePoint_of_exists_isClosed_smoothChart · AlgebraicGeometry.Stack.exists_isClosed_smoothChart_of_isFiniteTypePoint · AlgebraicGeometry.Stack.exists_isClosed_smoothChart_size_le_of_isFiniteTypePoint · AlgebraicGeometry.Stack.IsFiniteTypePoint · AlgebraicGeometry.Stack.finiteTypePoints · AlgebraicGeometry.Stack.affineSmoothChartClosedPoints_eq_smoothChartClosedPoints · AlgebraicGeometry.Stack.smoothChartClosedPoints_subset_finiteTypePoints · AlgebraicGeometry.Stack.finiteTypePoints_subset_smoothChartClosedPoints

Section101.19 Automorphism groups #

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

Tag 0DTS, a lemma

Tag 0DTS in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentable_pointAutomorphismSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismGroupScheme.lean, line 83. The attribute's comment: “the automorphism group algebraic space of a field-valued point is a scheme under any of the six conditions”.

Stacks 0DTS. Let 𝒳 be an algebraic stack over S and let x : Spec k ⟶ 𝒳 be a field-valued point with automorphism group algebraic space G_x = Isom_𝒳(x, x) over Spec k. Then G_x is a scheme if one of the following holds: the diagonal Δ : 𝒳 ⟶ 𝒳 × 𝒳 is quasi-separated, Δ is locally separated, 𝒳 is quasi-DM, the inertia projection I_𝒳 ⟶ 𝒳 is quasi-separated, I_𝒳 ⟶ 𝒳 is locally separated, or I_𝒳 ⟶ 𝒳 is locally quasi-finite.

Products are over S (Properties of Stacks, Section 04XA), the properties of Δ and of I_𝒳 ⟶ 𝒳 are taken in the sense of Properties of Stacks, Section 04XB, quasi-DM is the absolute notion of Stacks 050D (over Spec ℤ), and "is a scheme" is representability of the presheaf G_x on the big fppf site of Spec k.

theorem isRepresentable_pointAutomorphismSpace (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (x : FieldValuedPoint B S hS 𝒳.val.val)
    (h : IsQuasiSeparated B S hS (diagonal.{u, u, u + 1} B S hS 𝒳.val) ∨
      IsLocallySeparated B S hS (diagonal.{u, u, u + 1} B S hS 𝒳.val) ∨
      AlgebraicStacks.IsAbsolutelyQuasiDM B S hS B.contains_terminal 𝒳 ∨
      IsQuasiSeparated B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳).hom ∨
      IsLocallySeparated B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳).hom ∨
      IsLocallyQuasiFinite B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳).hom) :
    (pointAutomorphismSpace B S hS 𝒳.val x).IsRepresentable

Tag 0DTT, a lemma

Tag 0DTT in the Stacks Project.

AlgebraicGeometry.Stack.exists_pointAutomorphismSpace_iff_forall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismGroupGroundFieldExtension.lean, line 531.

Stacks 0DTT. Let 𝒳 be an algebraic stack, let q ∈ |𝒳| be a point and let P be a property of algebraic spaces over fields which is invariant under ground field extensions. Then the automorphism group algebraic space G_x/k has P for some field-valued representative x : Spec k → 𝒳 of q if and only if it has P for every field-valued representative.

theorem exists_pointAutomorphismSpace_iff_forall
    (q : points B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids)
    (P : ∀ U : BigFppfOver B S hS, ((BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u) → Prop)
    (hP : IsInvariantUnderGroundFieldExtension B S hS P) :
    (∃ p : FieldValuedPoint B S hS 𝒳.val.val,
        pointClass B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids p = q ∧
        P p.base (pointAutomorphismSpace B S hS 𝒳.val p)) ↔
      ∀ p : FieldValuedPoint B S hS 𝒳.val.val,
        pointClass B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids p = q →
        P p.base (pointAutomorphismSpace B S hS 𝒳.val p)

Tag 0DTU, a remark

Tag 0DTU in the Stacks Project.

AlgebraicGeometry.Stack.AutomorphismGroupHasProperty, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismGroupProperty.lean, line 105. The attribute's comment: “the definition: the automorphism group of a stack at a point has P when the automorphism group algebraic space of every field-valued representative has P”.

Stacks 0DTU. Let P be a property of algebraic spaces over fields and let q be a point of |𝒳| for an algebraic stack 𝒳. The automorphism group of 𝒳 at q has P when the automorphism group algebraic space G_x/k = Isom_𝒳(x, x) has P for every field-valued representative x : Spec k → 𝒳 of q.

This is condition (2) of Stacks 0DTT, so it makes no choice of representative. When P is invariant under ground field extensions (AlgebraicGeometry.Stack.IsInvariantUnderGroundFieldExtension) it agrees with condition (1) of Stacks 0DTT by AlgebraicGeometry.Stack.automorphismGroupHasProperty_iff_exists, and it is decided by any single representative by AlgebraicGeometry.Stack.automorphismGroupHasProperty_iff_of_representative; that is what makes the phrase well posed, and it is the content of Remark 0DTU.

def AutomorphismGroupHasProperty
    (P : ∀ U : BigFppfOver B S hS, ((BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u) → Prop)
    (q : points B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids) : Prop

AlgebraicGeometry.Stack.automorphismGroupHasProperty_iff_of_representative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismGroupProperty.lean, line 148. The attribute's comment: “the phrase is well posed: for a property invariant under ground field extensions, an arbitrary single field-valued representative decides it”.

Stacks 0DTU: the phrase is well posed. For a property P of algebraic spaces over fields which is invariant under ground field extensions, the statement that the automorphism group of 𝒳 at q has P is decided by an arbitrary single field-valued representative p of q: it holds exactly when the automorphism group algebraic space G_p has P. In particular the answer does not depend on which representative of q one reads it at, which is what licenses the phrase "the automorphism group of 𝒳 at q has P" of Remark 0DTU.

theorem automorphismGroupHasProperty_iff_of_representative
    (P : ∀ U : BigFppfOver B S hS, ((BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u) → Prop)
    (hP : IsInvariantUnderGroundFieldExtension B S hS P)
    {q : points B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids}
    (p : FieldValuedPoint B S hS 𝒳.val.val)
    (hp : pointClass B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids p = q) :
    AutomorphismGroupHasProperty B S hS P q ↔
      P p.base (pointAutomorphismSpace B S hS 𝒳.val p)

Tag 0DTV, a lemma

Tag 0DTV in the Stacks Project.

AlgebraicGeometry.Stack.inducesIsomorphismAt_iff_forall_representatives, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismGroupAtPoint.lean, line 325. The attribute's comment: “for the lifts of one field-valued representative: some lift, hence any lift”.

A 1-morphism of algebraic stacks induces an isomorphism between automorphism groups at a point of |𝒳| exactly when it does so at every object lying above every field-valued representative of that point: one pullback of one representative above each object of the big site already decides it, because in a category fibred in groupoids any two lifts of the same morphism of the base are isomorphic over an identity.

This is Stacks 0DTV for the lifts of one field-valued representative. Passing between two representatives of the same point is a descent statement, proved for the automorphism group algebraic spaces in AlgebraicGeometry.Stack.exists_isIso_pointAutomorphismSpaceMap_iff_forall: the map of automorphism group algebraic spaces over a field extension is a base change, and being an isomorphism is fpqc local on the target (Stacks 041Y). AlgebraicGeometry.Stack.InducesIsomorphismAt quantifies over all field-valued representatives, which is condition (2) of Stacks 0DTV and so never weaker than the notion of Stacks 0DTW.

theorem inducesIsomorphismAt_iff_forall_representatives (f : 𝒳 ⟶ 𝒴)
    (q : points B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids) :
    InducesIsomorphismAt B S hS f q ↔
      ∀ p : FieldValuedPoint B S hS 𝒳.val.val,
        pointClass B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids p = q →
          InducesIsomorphismAtObject B S hS f p.obj

AlgebraicGeometry.Stack.exists_isIso_pointAutomorphismSpaceMap_iff_forall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismGroupGroundFieldExtension.lean, line 698.

Stacks 0DTV. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks and let x be a point of |𝒳|. The map G_x ⟶ G_y of automorphism group algebraic spaces, where y = f ∘ x, is an isomorphism for some field-valued representative x : Spec k → 𝒳 of the point if and only if it is an isomorphism for every such representative.

Two representatives of one point admit a common refinement. Over a field extension the map of automorphism group algebraic spaces is a base change of the map below, and being an isomorphism is fpqc local on the target (Stacks 041Y), so it passes both ways between a representative and a refinement.

theorem exists_isIso_pointAutomorphismSpaceMap_iff_forall (f : 𝒳 ⟶ 𝒴)
    (q : points B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids) :
    (∃ p : FieldValuedPoint B S hS 𝒳.val.val,
        pointClass B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids p = q ∧
          IsIso (pointAutomorphismSpaceMap B S hS f p)) ↔
      ∀ p : FieldValuedPoint B S hS 𝒳.val.val,
        pointClass B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids p = q →
          IsIso (pointAutomorphismSpaceMap B S hS f p)

Tag 0DTW, a remark

Tag 0DTW in the Stacks Project.

AlgebraicGeometry.Stack.InducesIsomorphismAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismGroupAtPoint.lean, line 279. The attribute's comment: “f induces an isomorphism between automorphism groups at a point”.

A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks induces an isomorphism between automorphism groups at a point q of |𝒳| and at f(q) — in the literature, f is stabilizer preserving, or fixed-point reflecting, at q — when for every field-valued representative p of q and every object of the big site the morphism of automorphism group algebraic spaces of p has a pullback of p at which it is bijective on sections.

By AlgebraicGeometry.Stack.inducesIsomorphismAt_iff_forall_representatives one such pullback per object of the site is enough: the condition then holds at every object lying above every representative of q, which is the content of Stacks 0DTV for the representatives of a fixed field-valued point.

def InducesIsomorphismAt (f : 𝒳 ⟶ 𝒴)
    (q : points B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids) : Prop

Sources

LeanAlgebraicGeometry.Stack.isRepresentable_pointAutomorphismSpace · AlgebraicGeometry.Stack.exists_pointAutomorphismSpace_iff_forall · AlgebraicGeometry.Stack.AutomorphismGroupHasProperty · AlgebraicGeometry.Stack.automorphismGroupHasProperty_iff_of_representative · AlgebraicGeometry.Stack.inducesIsomorphismAt_iff_forall_representatives · AlgebraicGeometry.Stack.exists_isIso_pointAutomorphismSpaceMap_iff_forall · AlgebraicGeometry.Stack.InducesIsomorphismAt

Section101.20 Presentations and properties of algebraic stacks #

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

Tag 0DTY, a lemma

Tag 0DTY in the Stacks Project.

AlgebraicGeometry.Stack.isSeparated_diagonal_of_isSeparated_sourceTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientStackSeparation.lean, line 161. The attribute's comment: “part (1): a separated relation gives a separated diagonal, the diagonal being the one over the base scheme of the site”.

Stacks 0DTY, part (1). Let (U, R, s, t, c) be a groupoid in algebraic spaces over S with s and t flat and locally of finite presentation, and let 𝒳 be an algebraic stack equivalent over the site to its quotient stack [U/R]. If (t, s) : R ⟶ U ×_S U is separated, then the diagonal of 𝒳 is separated in the sense of Properties of Stacks, Section 04XB.

theorem isSeparated_diagonal_of_isSeparated_sourceTarget
    (hequiv : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (quotientStack G).p 𝒳.val.val.p))
    (_hsFlat : Space.IsFlat B S hS G.source.hom)
    (_htFlat : Space.IsFlat B S hS G.target.hom)
    (_hsLfp : Space.IsLocallyOfFinitePresentation B S hS G.source.hom)
    (_htLfp : Space.IsLocallyOfFinitePresentation B S hS G.target.hom)
    (hj : Space.IsSeparated B S hS (GroupoidInAlgebraicSpaces.sourceTarget G).hom) :
    Stack.IsSeparated B S hS (diagonal.{u, u, u + 1} B S hS 𝒳.val)

AlgebraicGeometry.Stack.isSeparated_diagonal_of_isSeparated_spaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientStackSeparation.lean, line 182. The attribute's comment: “part (2): separated object and arrow spaces give a separated diagonal, the diagonal being the one over the base scheme of the site”.

Stacks 0DTY, part (2). Let (U, R, s, t, c) be a groupoid in algebraic spaces over S with s and t flat and locally of finite presentation, and let 𝒳 be an algebraic stack equivalent over the site to its quotient stack [U/R]. If U and R are separated, then the diagonal of 𝒳 is separated in the sense of Properties of Stacks, Section 04XB.

theorem isSeparated_diagonal_of_isSeparated_spaces
    (hequiv : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (quotientStack G).p 𝒳.val.val.p))
    (_hsFlat : Space.IsFlat B S hS G.source.hom)
    (_htFlat : Space.IsFlat B S hS G.target.hom)
    (_hsLfp : Space.IsLocallyOfFinitePresentation B S hS G.source.hom)
    (_htLfp : Space.IsLocallyOfFinitePresentation B S hS G.target.hom)
    (_hU : Space.IsSeparated B S hS G.objectsToBase.hom)
    (hR : Space.IsSeparated B S hS G.arrowsToBase.hom) :
    Stack.IsSeparated B S hS (diagonal.{u, u, u + 1} B S hS 𝒳.val)

AlgebraicGeometry.Stack.isAbsolutelyQuasiDM_of_isLocallyQuasiFinite_sourceTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientStackSeparation.lean, line 204. The attribute's comment: “part (3): a locally quasi-finite relation gives a quasi-DM quotient”.

Stacks 0DTY, part (3). Let (U, R, s, t, c) be a groupoid in algebraic spaces over S with s and t flat and locally of finite presentation, and let 𝒳 be an algebraic stack equivalent over the site to its quotient stack [U/R]. If (t, s) : R ⟶ U ×_S U is locally quasi-finite, then 𝒳 is quasi-DM.

theorem isAbsolutelyQuasiDM_of_isLocallyQuasiFinite_sourceTarget
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (hequiv : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (quotientStack G).p 𝒳.val.val.p))
    (_hsFlat : Space.IsFlat B S hS G.source.hom)
    (_htFlat : Space.IsFlat B S hS G.target.hom)
    (_hsLfp : Space.IsLocallyOfFinitePresentation B S hS G.source.hom)
    (_htLfp : Space.IsLocallyOfFinitePresentation B S hS G.target.hom)
    (hj : Space.IsLocallyQuasiFinite B S hS
      (GroupoidInAlgebraicSpaces.sourceTarget G).hom) :
    AlgebraicStacks.IsAbsolutelyQuasiDM.{u, w} B S hS hZ 𝒳

AlgebraicGeometry.Stack.isAbsolutelyQuasiDM_of_isLocallyQuasiFinite_source_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientStackSeparation.lean, line 228. The attribute's comment: “part (4): a locally quasi-finite source and target give a quasi-DM quotient”.

Stacks 0DTY, part (4). Let (U, R, s, t, c) be a groupoid in algebraic spaces over S with s and t flat and locally of finite presentation, and let 𝒳 be an algebraic stack equivalent over the site to its quotient stack [U/R]. If s and t are locally quasi-finite, then 𝒳 is quasi-DM.

theorem isAbsolutelyQuasiDM_of_isLocallyQuasiFinite_source_target
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (hequiv : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (quotientStack G).p 𝒳.val.val.p))
    (_hsFlat : Space.IsFlat B S hS G.source.hom)
    (_htFlat : Space.IsFlat B S hS G.target.hom)
    (_hsLfp : Space.IsLocallyOfFinitePresentation B S hS G.source.hom)
    (_htLfp : Space.IsLocallyOfFinitePresentation B S hS G.target.hom)
    (hs : Space.IsLocallyQuasiFinite B S hS G.source.hom)
    (_ht : Space.IsLocallyQuasiFinite B S hS G.target.hom) :
    AlgebraicStacks.IsAbsolutelyQuasiDM.{u, w} B S hS hZ 𝒳

AlgebraicGeometry.Stack.isSeparatedOver_of_isProper_sourceTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientStackSeparation.lean, line 253. The attribute's comment: “part (5): a proper relation gives a quotient separated over the base scheme S (Stacks 050D part (3)), the source's separated for an algebraic stack over S”.

Stacks 0DTY, part (5). Let (U, R, s, t, c) be a groupoid in algebraic spaces over S with s and t flat and locally of finite presentation, and let 𝒳 be an algebraic stack equivalent over the site to its quotient stack [U/R]. If (t, s) : R ⟶ U ×_S U is proper, then 𝒳 is separated over the base scheme of the site (Stacks 050D, part (3)).

theorem isSeparatedOver_of_isProper_sourceTarget
    (hequiv : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (quotientStack G).p 𝒳.val.val.p))
    (_hsFlat : Space.IsFlat B S hS G.source.hom)
    (_htFlat : Space.IsFlat B S hS G.target.hom)
    (_hsLfp : Space.IsLocallyOfFinitePresentation B S hS G.source.hom)
    (_htLfp : Space.IsLocallyOfFinitePresentation B S hS G.target.hom)
    (hj : Space.IsProper B S hS (GroupoidInAlgebraicSpaces.sourceTarget G).hom) :
    IsSeparatedOver.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.isSeparatedOver_of_isProper_source_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientStackSeparation.lean, line 278. The attribute's comment: “part (6): a proper source and target over a separated object space give a quotient separated over the base scheme S (Stacks 050D part (3)), the source's separated for an algebraic stack over S”.

Stacks 0DTY, part (6). Let (U, R, s, t, c) be a groupoid in algebraic spaces over S with s and t flat and locally of finite presentation, and let 𝒳 be an algebraic stack equivalent over the site to its quotient stack [U/R]. If s and t are proper and U is separated, then 𝒳 is separated over the base scheme of the site (Stacks 050D, part (3)).

theorem isSeparatedOver_of_isProper_source_target
    (hequiv : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (quotientStack G).p 𝒳.val.val.p))
    (_hsFlat : Space.IsFlat B S hS G.source.hom)
    (_htFlat : Space.IsFlat B S hS G.target.hom)
    (_hsLfp : Space.IsLocallyOfFinitePresentation B S hS G.source.hom)
    (_htLfp : Space.IsLocallyOfFinitePresentation B S hS G.target.hom)
    (hs : Space.IsProper B S hS G.source.hom)
    (_ht : Space.IsProper B S hS G.target.hom)
    (hU : Space.IsSeparated B S hS G.objectsToBase.hom) :
    IsSeparatedOver.{u, w} B S hS 𝒳

Tag 0DTZ, a lemma

Tag 0DTZ in the Stacks Project.

AlgebraicGeometry.Stack.equivalence_sourceTargetRel_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackPoints.lean, line 183. The attribute's comment: “the image of |R| in |U| x |U| is an equivalence relation, with no hypothesis on the source and target maps”.

Stacks 0DTZ. For a groupoid in algebraic spaces (U, R, s, t, c) the image of |R| → |U| × |U| is an equivalence relation on the points of the object space: the pair of points related by a point of the arrow space is its target and its source, and the arrows over each test scheme form a groupoid.

No hypothesis on the source and target maps is needed; the flatness and local finite presentation of Stacks 0DTZ enter only through the algebraicity of the quotient stack.

theorem equivalence_sourceTargetRel_points (G : GroupoidInAlgebraicSpaces C S hS B) :
    Equivalence (Function.SourceTargetRel
      (Space.pointsMap C S hS G.arrows.obj G.source.hom)
      (Space.pointsMap C S hS G.arrows.obj G.target.hom))

AlgebraicGeometry.Stack.pointMap_eq_iff_sourceTargetRel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackPoints.lean, line 416. The attribute's comment: “the fibres of |U| -> |[U/R]| are the classes of the image of |R|, with no hypothesis on the source and target maps”.

Stacks 0DTZ. Two points of the object space of a groupoid in algebraic spaces have the same image in the points of the quotient stack exactly when they lie in the image of |R| → |U| × |U|, that is exactly when some point of the arrow space has the first as its target and the second as its source.

No hypothesis on the source and target maps is needed; the flatness and local finite presentation of Stacks 0DTZ enter only through the algebraicity of the quotient stack.

theorem pointMap_eq_iff_sourceTargetRel
    (G : GroupoidInAlgebraicSpaces C S hS B)
    (first second : Space.points C S hS G.objects.obj) :
    quotientStackPointMap G first = quotientStackPointMap G second ↔
      Function.SourceTargetRel
        (Space.pointsMap C S hS G.arrows.obj G.source.hom)
        (Space.pointsMap C S hS G.arrows.obj G.target.hom)
        first second

AlgebraicGeometry.Stack.surjective_quotientStackPointMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackPoints.lean, line 458. The attribute's comment: “|U| surjects onto the points of the quotient stack, with no hypothesis on the source and target maps”.

Stacks 0DTZ. Every point of the quotient stack [U/R] of a groupoid in algebraic spaces is the image of a point of the object space U.

No hypothesis on the groupoid is needed: a point of |[U/R]| is represented by an object over the spectrum of a field, the projection is surjective on objects by AlgebraicGeometry.Stack.isSurjectiveOnObjects_quotientStackProjection, and the resulting object of the object space over a field extension is dominated by a field-valued point of U whose image therefore has a common refinement with the chosen representative.

theorem surjective_quotientStackPointMap (G : GroupoidInAlgebraicSpaces C S hS B) :
    Function.Surjective (quotientStackPointMap G)

AlgebraicGeometry.Stack.exists_quotientPointsEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackPoints.lean, line 491. The attribute's comment: “|[U/R]| is the quotient of |U| by that equivalence relation, with no hypothesis on the source and target maps”.

Stacks 0DTZ. The points of the quotient stack of a groupoid in algebraic spaces are the quotient of the points of the object space by the image of |R| → |U| × |U|: there is an equivalence of the quotient set with |[U/R]| carrying the class of a point of |U| to its image under the canonical map, so the identification is the canonical one and not merely a bijection of underlying sets.

No hypothesis on the source and target maps is needed; the flatness and local finite presentation of Stacks 0DTZ enter only through the algebraicity of the quotient stack.

theorem exists_quotientPointsEquiv (G : GroupoidInAlgebraicSpaces C S hS B) :
    ∃ e : Quotient (arrowSetoid G) ≃
        points C S hS (quotientStack G) (isFiberedInGroupoids_quotientStack G),
      ∀ x : Space.points C S hS G.objects.obj,
        e (Quotient.mk _ x) = quotientStackPointMap G x

Sources

Section101.21 Special presentations of algebraic stacks #

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

Tag 06MD, a lemma

Tag 06MD in the Stacks Project.

AlgebraicGeometry.Stack.exists_openSubspace_isLocallyOfFinitePresentation_zeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChartSlicingFinitePresentation.lean, line 225. The attribute's comment: “the locally-of-finite-presentation conjunct ONLY: V(f₁,…,f_r) ⟶ 𝒳 is locally of finite presentation. Flatness of it is NOT proved and no part of that conjunct is claimed. Local finite presentation of the closed immersion V(f₁,…,f_r) ⟶ U, which reduces to the surjectivity half of Stacks 03MB, is carried as a hypothesis.”.

Stacks 06MD, the locally-of-finite-presentation conjunct. Let 𝒳 be an algebraic stack over S, let U be an algebraic space with a 1-morphism f : U ⟶ 𝒳 which is flat and locally of finite presentation, let Spec k ⟶ 𝒳 be a field-valued point, and let F = U ×_𝒳 Spec k with projection p : F ⟶ U. Let f₁, …, f_r ∈ Γ(U, 𝒪_U) and let z be a geometric point of F at which the f_i map to a regular sequence in 𝒪_{F, z̄}. Then, after replacing U by an open subspace containing p(z), the 1-morphism V(f₁, …, f_r) ⟶ 𝒳 is locally of finite presentation.

Only that conjunct is proved; flatness of V(f₁, …, f_r) ⟶ 𝒳 is not claimed, and the implementation notes say why. The flatness and regular-sequence hypotheses of the source are recorded and unused — the conjunct proved here needs no shrinking of U either, so the open subspace produced is the whole of U and the stronger statement over an arbitrary open subspace is AlgebraicGeometry.Stack.isLocallyOfFinitePresentation_zeroLocusOnOpenToStack. Local finite presentation of the closed immersion V(f₁, …, f_r) ⟶ U, the hypothesis hslice of AlgebraicGeometry.Space.isLocallyOfFinitePresentation_vanishingSubfunctor_comp which reduces to the surjectivity half of Stacks 03MB, is carried.

theorem exists_openSubspace_isLocallyOfFinitePresentation_zeroLocus
    (_hflat : AlgebraicStacks.IsFlat B S hS f)
    (hfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS f)
    (z : Space.GeometricPoint B S hS Fsp)
    (_hreg : FibreIsRegularSequenceAt.{u, w} B S hS 𝒳 U hU k hk toBase f g a Fsp hFsp eF z)
    (hslice : Space.IsLocallyOfFinitePresentation B S hS (chartZeroLocus B S hS U hU a).ι) :
    ∃ (V : Subfunctor U) (hV : Space.IsOpenSubspace B S hS V),
      Space.pointsMap B S hS Fsp
          (fibreSpaceProjection B S hS 𝒳 U hU k hk toBase f g Fsp eF) z.image ∈
        Set.range (Space.pointsMap B S hS V.toFunctor V.ι) ∧
      AlgebraicStacks.IsLocallyOfFinitePresentation B S hS
        (zeroLocusOnOpenToStack.{u, w} B S hS 𝒳 U hU f a V hV)

AlgebraicGeometry.Stack.exists_openSubspace_isFlat_isLocallyOfFinitePresentation_zeroLocus_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChartSlicingFlatness.lean, line 768.

Stacks 06MD. Let 𝒳 be an algebraic stack over S, let U be an algebraic space with a 1-morphism f : U ⟶ 𝒳 which is flat and locally of finite presentation, let Spec k ⟶ 𝒳 be a field-valued point, and let F = U ×_𝒳 Spec k with projection p : F ⟶ U. Let f₁, …, f_r ∈ Γ(U, 𝒪_U) and let z be a geometric point of F at which the f_i map to a regular sequence in the étale local ring 𝒪_{F, z̄}. Then, after replacing U by an open subspace containing p(z), the 1-morphism V(f₁, …, f_r) ⟶ 𝒳 is flat and locally of finite presentation.

Nothing is carried. Local finite presentation holds over every open subspace, AlgebraicGeometry.Stack.isLocallyOfFinitePresentation_zeroLocusOnOpenToStack. For flatness the proof is the source's: base change along a smooth chart of 𝒳 by an algebraic space surjective on objects, apply the flatness half of Stacks 06LW to the morphism of algebraic spaces U ×_𝒳 𝒲 ⟶ 𝒲 at the fibre which AlgebraicGeometry.Stack.exists_chartFibre_isPullback_isRegular produces, take the open subspace of U swept out by the open subspace Stacks 06LW returns — open because the projection U ×_𝒳 𝒲 ⟶ 𝒲 is a base change of the smooth chart, hence flat and locally of finite presentation, hence open on points — and read flatness back point by point through the chart independence of Stacks 0CIC.

theorem exists_openSubspace_isFlat_isLocallyOfFinitePresentation_zeroLocus_of_isRegular
    (hflat : AlgebraicStacks.IsFlat B S hS f)
    (hfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS f)
    (z : Space.GeometricPoint B S hS Fsp)
    (hreg : FibreIsRegularSequenceAt.{u, w} B S hS 𝒳 U hU k hk toBase f g a Fsp hFsp eF z) :
    ∃ (V : Subfunctor U) (hV : Space.IsOpenSubspace B S hS V),
      Space.pointsMap B S hS Fsp
          (fibreSpaceProjection B S hS 𝒳 U hU k hk toBase f g Fsp eF) z.image ∈
        Set.range (Space.pointsMap B S hS V.toFunctor V.ι) ∧
      AlgebraicStacks.IsFlat B S hS
          (zeroLocusOnOpenToStack.{u, w} B S hS 𝒳 U hU f a V hV) ∧
        AlgebraicStacks.IsLocallyOfFinitePresentation B S hS
          (zeroLocusOnOpenToStack.{u, w} B S hS 𝒳 U hU f a V hV)

Tag 06ME, a lemma

Tag 06ME in the Stacks Project.

AlgebraicGeometry.Stack.exists_openSubstack_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChartShrinkingQuasiFiniteEtale.lean, line 246. The attribute's comment: “after replacing the algebraic space by an open subspace containing the image of the given point of the fibre, a 1-morphism locally of finite type whose fibre over a field-valued point has dimension zero at that point is locally quasi-finite. The two clauses of Stacks 06M5 are carried, as the data W with hW (the open locus on which the 1-morphism is locally quasi-finite) and the hypothesis hBaseChange (that locus commutes with the base change along the field-valued point), since Stacks 06M5 is absent from this library; the deduction of the conclusion from them is proved”.

Stacks 06ME. Let 𝒳 be an algebraic stack, let U be an algebraic space with a 1-morphism f : U ⟶ 𝒳 which is locally of finite type, let Spec k ⟶ 𝒳 be a field-valued point, and let F = U ×_𝒳 Spec k with projection p : F ⟶ U and structure 1-morphism q : F ⟶ Spec k. If z ∈ |F| has dim_z(F) = 0 then, after replacing U by an open subspace containing p(z), the 1-morphism U ⟶ 𝒳 is locally quasi-finite.

The proof is the source's. The open substack W is the locus W(f) of Stacks 06M5 on which f is locally quasi-finite, carried as the data W together with hW; the compatibility of that locus with the base change along g, which is the second clause of Stacks 06M5, is carried as hBaseChange. Given those, the conclusion is exactly that p(z) ∈ |W|, and that follows because the fibre hypothesis puts z in an open substack of F which is locally quasi-finite over Spec k, hence inside the preimage of |W|.

theorem exists_openSubstack_isLocallyQuasiFinite
    (_hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (W : OpenSubstack (algebraicSpaceStack.{u, w} B S hS U hU))
    (hW : AlgebraicStacks.IsLocallyQuasiFinite B S hS (W.inclusion ≫ f))
    (hBaseChange : ∀ V : OpenSubstack (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g),
      AlgebraicStacks.IsLocallyQuasiFinite B S hS
          (V.inclusion ≫ fibreStructureMorphism B S hS 𝒳 U hU k hk toBase f g) →
        V.pointSet B S hS ⊆
          AlgebraicStacks.pointsMap B S hS
              (fibreProjection B S hS 𝒳 U hU k hk toBase f g) ⁻¹' W.pointSet B S hS)
    (z : AlgebraicStacks.points B S hS (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g))
    (hz : FibreIsLocallyQuasiFiniteNear.{u, w} B S hS 𝒳 U hU k hk toBase f g z) :
    AlgebraicStacks.pointsMap B S hS
        (fibreProjection B S hS 𝒳 U hU k hk toBase f g) z ∈ W.pointSet B S hS ∧
      AlgebraicStacks.IsLocallyQuasiFinite B S hS (W.inclusion ≫ f)

AlgebraicGeometry.Stack.exists_openSubstack_isLocallyQuasiFinite_of_dimensionAtPoint_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreQuasiFiniteNearSubstack.lean, line 422. The attribute's comment: “the source's own hypotheses, with the conclusion read on an open substack of the stack of the algebraic space: the 1-morphism is locally of finite type and the given point z of the fibre has dim_z(F) = 0, the dimension of Stacks 04N5 of a representing algebraic space Fsp of the fibre at z. Nothing is added and nothing is weakened. The proof is exists_openSubstack_isLocallyQuasiFinite_unconditional of ChartShrinkingQuasiFiniteEtaleUnconditional -- which states the same conclusion at the intermediate condition the source's own proof extracts from dim_z(F) = 0, that some open substack of the fibre containing z is locally quasi-finite over Spec k -- composed with the step the source's proof takes from dim_z(F) = 0 to that condition by Stacks 04NV, which is fibreIsLocallyQuasiFiniteNear_of_dimensionAtPoint_eq_zero above. The source's open subspace of the algebraic space is rendered here as an open substack of the stack of that space, with the same point set, both directions of that passage being proved as exists_openSubstack_algebraicSpaceStack_of_isOpenImmersion and exists_isOpenSubspace_property_eq_essImage; the conclusion read on an open subspace, as the source reads it, is exists_isOpenSubspace_isLocallyQuasiFinite_of_dimensionAtPoint_eq_zero below. The point of the fibre is the image of z under the comparison spacePointMap of the representing equivalence, which bijective_spacePointMap_representing makes a bijection, so no point of the fibre is excluded by stating the hypothesis on Fsp”.

Stacks 06ME at the source's own hypothesis, with the conclusion read on an open substack. Let 𝒳 be an algebraic stack, let U be an algebraic space with a 1-morphism f : U ⟶ 𝒳 locally of finite type, let Spec k ⟶ 𝒳 be a field-valued point, let Fsp represent the fibre F = U ×_𝒳 Spec k through eF, and let z be a point of |Fsp| with dim_z(F) = 0 — the dimension of Stacks 04N5 of the algebraic space Fsp at z. Then there is an open substack W of the algebraic stack of U whose point set contains p(z) and for which W.inclusion ≫ f is locally quasi-finite.

This is AlgebraicGeometry.Stack.exists_openSubstack_isLocallyQuasiFinite_unconditional with its fibre hypothesis AlgebraicGeometry.Stack.FibreIsLocallyQuasiFiniteNear replaced by the source's dim_z(F) = 0, through AlgebraicGeometry.Stack.fibreIsLocallyQuasiFiniteNear_of_dimensionAtPoint_eq_zero. Nothing is added and nothing is weakened: the finite-type hypothesis is the source's, and the hypothesis on z is the source's. The point of |F| is the image of z under the comparison AlgebraicGeometry.Stack.spacePointMap of the representing equivalence, which is a bijection by AlgebraicGeometry.Stack.bijective_spacePointMap_representing, so every point of |F| is reached.

theorem exists_openSubstack_isLocallyQuasiFinite_of_dimensionAtPoint_eq_zero
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (z : Space.points B S hS Fsp)
    (hz : Space.dimensionAtPoint B S hS Fsp hFsp z = 0) :
    ∃ W : OpenSubstack (algebraicSpaceStack.{u, w} B S hS U hU),
      AlgebraicStacks.pointsMap B S hS
          (fibreProjection B S hS 𝒳 U hU k hk toBase f g)
          (spacePointMap B S hS Fsp
            (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g).val
            (representingEquivalence B S hS Fsp
              (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g).val eF).functor z) ∈
        W.pointSet B S hS ∧
        AlgebraicStacks.IsLocallyQuasiFinite B S hS (W.inclusion ≫ f)

AlgebraicGeometry.Stack.exists_isOpenSubspace_isLocallyQuasiFinite_of_dimensionAtPoint_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreQuasiFiniteNearSubstack.lean, line 464. The attribute's comment: “the statement of the source, hypotheses and conclusion: the 1-morphism out of the algebraic space is locally of finite type, the given point z of the fibre has dim_z(F) = 0 -- the dimension of Stacks 04N5 of a representing algebraic space Fsp of the fibre at z -- and after replacing the algebraic space by an open subspace of Stacks 02YU, part (2), containing the image of z, the 1-morphism is locally quasi-finite, the replacement read as the composite of the 1-morphism of Stacks 0458 induced by that open subspace. Nothing is added and nothing is weakened. The proof is exists_isOpenSubspace_isLocallyQuasiFinite of ChartShrinkingOpenSubspace -- the same conclusion at the intermediate condition the source's own proof extracts from dim_z(F) = 0 -- composed with the step the source's proof takes from dim_z(F) = 0 to that condition by Stacks 04NV, which is fibreIsLocallyQuasiFiniteNear_of_dimensionAtPoint_eq_zero above. The point of the fibre is the image of z under the comparison spacePointMap of the representing equivalence, which bijective_spacePointMap_representing makes a bijection, so no point of the fibre is excluded by stating the hypothesis on Fsp”.

Stacks 06ME at the source's own hypothesis, with the conclusion read on an open subspace. The statement of the source: with f : U ⟶ 𝒳 locally of finite type and z a point of the fibre F = U ×_𝒳 Spec k at which the dimension of F is zero, there is an open subspace V ⊆ U of Stacks 02YU, part (2), whose point set contains p(z) and for which the composite of the 1-morphism of Stacks 0458 induced by V with f is locally quasi-finite.

This is AlgebraicGeometry.Stack.exists_isOpenSubspace_isLocallyQuasiFinite with its fibre hypothesis replaced by the source's, through AlgebraicGeometry.Stack.fibreIsLocallyQuasiFiniteNear_of_dimensionAtPoint_eq_zero. Both hypotheses are now the source's and the conclusion is the source's.

theorem exists_isOpenSubspace_isLocallyQuasiFinite_of_dimensionAtPoint_eq_zero
    (hf : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (z : Space.points B S hS Fsp)
    (hz : Space.dimensionAtPoint B S hS Fsp hFsp z = 0) :
    ∃ (V : Subfunctor U) (hV : Space.IsOpenSubspace B S hS V),
      AlgebraicStacks.pointsMap B S hS
          (fibreProjection B S hS 𝒳 U hU k hk toBase f g)
          (spacePointMap B S hS Fsp
            (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g).val
            (representingEquivalence B S hS Fsp
              (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g).val eF).functor z) ∈
        spacePointMap B S hS U (algebraicSpaceStack.{u, w} B S hS U hU).val
            (BasedFunctor.id (fibredCategory B S hS U).val) ''
          Set.range (Space.pointsMap B S hS V.toFunctor V.ι) ∧
        AlgebraicStacks.IsLocallyQuasiFinite B S hS
          (algebraicSpaceStackMap.{u, w} B S hS hV.1 hU V.ι ≫ f)

Tag 06MF, a theorem

Tag 06MF in the Stacks Project.

AlgebraicGeometry.Stack.isAbsolutelyQuasiDM_iff_hasQuasiDMPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordPresentationTheorem.lean, line 197. The attribute's comment: “the equivalence of (1) quasi-DM with (2) the existence of a surjective, flat, locally finitely presented, locally quasi-finite presentation by a scheme. Both implications are carried, as the hypotheses hForward (the structure theorem: Stacks 06MD, 06ME, 06G2, 06G3 are absent) and hBackward (Stacks 06MB part (2) is present but the repackaging of the Section 04XB local quasi-finiteness of the chart into its HasRelativeProperty form is absent)”.

Stacks 06MF. An algebraic stack is quasi-DM exactly when there is a scheme of the site with a surjective, flat, locally finitely presented, locally quasi-finite 1-morphism to it.

Both implications are carried; see AlgebraicGeometry.Stack.ExistsQuasiDMPresentationOfIsAbsolutelyQuasiDM and AlgebraicGeometry.Stack.IsAbsolutelyQuasiDMOfHasQuasiDMPresentation.

theorem isAbsolutelyQuasiDM_iff_hasQuasiDMPresentation
    (hForward : ExistsQuasiDMPresentationOfIsAbsolutelyQuasiDM.{u, w} B S hS hZ)
    (hBackward : IsAbsolutelyQuasiDMOfHasQuasiDMPresentation.{u, w} B S hS hZ)
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    AlgebraicStacks.IsAbsolutelyQuasiDM B S hS hZ 𝒳 ↔
      HasQuasiDMPresentation.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.isAbsolutelyQuasiDM_of_hasQuasiDMPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordPresentationUnconditional.lean, line 374. The attribute's comment: “the implication (2) implies (1): a surjective, flat, locally finitely presented, locally quasi-finite presentation by a scheme of the site makes an algebraic stack quasi-DM”.

An algebraic stack with a surjective, flat, locally finitely presented, locally quasi-finite presentation by a scheme of the site is quasi-DM: the implication (2) ⟹ (1).

theorem isAbsolutelyQuasiDM_of_hasQuasiDMPresentation (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h : HasQuasiDMPresentation.{u, w} B S hS 𝒳) :
    AlgebraicStacks.IsAbsolutelyQuasiDM B S hS hZ 𝒳

AlgebraicGeometry.Stack.isAbsolutelyQuasiDM_iff_hasQuasiDMPresentation_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordPresentationUnconditional.lean, line 500. The attribute's comment: “the equivalence of (1) quasi-DM with (2) the existence of a surjective, flat, locally finitely presented, locally quasi-finite presentation by a scheme. BOTH implications are proved and nothing is carried. (2) implies (1) is Stacks 06MB part (2), isAbsolutelyQuasiDM_of_hasQuasiDMPresentation; (1) implies (2) is the structure theorem, hasQuasiDMPresentation_of_isAbsolutelyQuasiDM, whose local half is the chart of exists_flat_isLocallyOfFinitePresentation_isLocallyQuasiFinite_chart_at_finiteTypePoint -- the smooth chart of 06FX with a closed point over the finite type point, the charted self-intersection of 04ZP and 04SW, the identity point of 04XH, and the slice cut out by a regular sequence in the etale local ring of a fibre (06LC, 06MD, 06LW) shrunk to be locally quasi-finite by 06M3 and 06ME -- and whose assembly is hasQuasiDMPresentation_of_forall_isLocallyQuasiFinite: the 1-morphism out of the coproduct W = coprod_x Z_x, the descent of the three properties along the summand inclusions, and surjectivity from the corollary of 06G2. The coproduct lies in the site by contains_sigma_of_forall_size_le, which the uniform bound 2 ^ 2 ^ size U_0 on the charts supplies -- the finite type points need not be below the cofinality of the site's cutoff, so contains_sigma_of_lt_cof does not apply”.

An algebraic stack is quasi-DM exactly when there is a scheme of the site with a surjective, flat, locally finitely presented, locally quasi-finite 1-morphism to it.

theorem isAbsolutelyQuasiDM_iff_hasQuasiDMPresentation_unconditional
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    AlgebraicStacks.IsAbsolutelyQuasiDM B S hS hZ 𝒳 ↔
      HasQuasiDMPresentation.{u, w} B S hS 𝒳

Tag 06N0, a lemma

Tag 06N0 in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.exists_division_identityArrowOpens_of_isoSpecField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/IdentityArrowDivision.lean, line 84. The attribute's comment: “the division of the groupoid of a flat field-valued presentation by the open and closed piece of its arrow scheme through the identity, with the quotient the spectrum of a field: the step of the proof which produces the field k_0 of invariants”.

Stacks 04S4 applied to the open and closed piece through the identity. A groupoid scheme whose object scheme is the spectrum of a field, whose arrow scheme is zero-dimensional and whose pre-relation is unramified, separated, locally of finite type and locally quasi-finite can be divided by the piece of its arrow scheme through the identity, and the quotient is the spectrum of a field.

theorem exists_division_identityArrowOpens_of_isoSpecField {S : Scheme.{u}}
    (G : Stacks.Groupoids.GroupoidScheme S) (k : Type u) [Field k]
    (iso : G.objects.left ≅ Spec (.of k))
    [IsLocallyArtinian G.arrows.left]
    [LocallyOfFiniteType G.source.left] [LocallyOfFiniteType G.target.left]
    [Unramified (prod.lift G.target G.source).left]
    [IsSeparated (prod.lift G.target G.source).left]
    [LocallyOfFiniteType (prod.lift G.target G.source).left]
    [LocallyQuasiFinite (prod.lift G.target G.source).left]
    (u : G.objects.left) :
    ∃ (P : OpenFiniteSubgroupoid G)
      (D : Division G P.subgroupoid P.inclusion P.objects_eq),
      Set.range P.inclusion.mapArrows.left.base = {G.identity.left.base u} ∧
        IsField Γ(D.quotient.left, ⊤)

AlgebraicGeometry.Stack.hasSurjectiveEtaleFieldSpectrumCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordSingletonEtaleCover.lean, line 170. The attribute's comment: “a DM, locally Noetherian, reduced algebraic stack with a singleton point space admits a surjective etale 1-morphism from the spectrum of a field. The implication is carried as the hypothesis hCover: the source's first step is the direction (1) => (2) of Stacks 06MP, of which this library proves only the converse, and Stacks 06FF, 06LZ and 04S4 are absent too”.

Stacks 06N0. A DM, locally Noetherian, reduced algebraic stack whose point space is a singleton admits a field k and a surjective étale 1-morphism Spec k ⟶ 𝒵.

The implication is carried as the hypothesis hCover; see AlgebraicGeometry.Stack.ExistsSurjectiveEtaleFieldCoverOfReducedSingletonDM for exactly which cited inputs are absent and why no part of the chain can be run without them.

theorem hasSurjectiveEtaleFieldSpectrumCover
    (hCover : ExistsSurjectiveEtaleFieldCoverOfReducedSingletonDM.{u, w} B S hS hZ)
    (𝒵 : AlgebraicStacks.{u, w} B S hS)
    (h𝒵 : IsReducedLocallyNoetherianSingletonDM.{u, w} B S hS hZ 𝒵) :
    HasSurjectiveEtaleFieldSpectrumCover.{u, w} B S hS 𝒵

AlgebraicGeometry.Stack.hasSurjectiveEtaleFieldSpectrumCover_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordSingletonEtaleCoverUnconditional.lean, line 164. The attribute's comment: “a DM, locally Noetherian, reduced algebraic stack with a singleton point space admits a surjective etale 1-morphism from the spectrum of a field. The field-valued point comes in two steps: Stacks 06MP (1) => (2) supplies a surjective, flat, locally finitely presented xi : Spec k -> Z, and the groupoid (U, R, s, t, c) of that flat presentation, with U = Spec k and R = U x_Z U, is divided by the open and closed subgroupoid P through the identity, whose quotient U_bar = Spec k_0 is the spectrum of the field of invariants. The division is exists_division_identityArrowOpens_etale_pointGroupoid, on the four conclusions of Stacks 04S4 in exists_division; it is run at the de-realization of the self-intersection groupoid, whose object and arrow spaces are representable by isRepresentable_objects_pointGroupoid_fieldSpectrum and isRepresentable_arrows_pointGroupoid_fieldSpectrum, the latter being condition (2) of Stacks 06LZ read on the base site at the dimension bound dimension_relation_le_zero_fieldSpectrum, i.e. Stacks 06FF against the quasi-DM hypothesis through Stacks 050H part (5). Etaleness of U_bar -> Z follows the source's steps 6 and 8 rather than its Stacks 04XD reading: the divided groupoid is the restriction of the descended groupoid (U_bar, R_bar, s_bar, t_bar, c_bar) along the finite locally free surjection U -> U_bar, so [U/R] -> [U_bar/R_bar] is an equivalence by Stacks 046T (nonempty_isEquivalenceOver_quotientStackMap_realizationHom, whose clause (1) is full faithfulness of the evaluations of the descent morphism and whose clause (2) is that its map on objects is an fppf covering), [U/R] -> Z is an equivalence by Stacks 04WY (nonempty_isEquivalenceOver_canonicalMap), and s_bar is etale by Division.etale_descended_source, which is Stacks 047W at unramifiedness through etale_source_of_flat_of_isOpenImmersion_identity rather than the computation of Omega_{R_bar/U_bar} that Stacks 04R9 gives the source. Stacks 04M9 then makes the projection S_{U_bar} -> [U_bar/R_bar] of Stacks 044R etale (isRelativelyEtale_quotientStackProjection_realization), and two instances of Stacks 0457 carry that verdict across the equivalence with Z and down the universe lift of the source, giving quotientProjectionSchemeStackMap, which is etale in the sense of Stacks 0CIL by isEtale_of_isRelativelyEtale. The DM hypothesis enters only at the division, in the absolute form of Stacks 050D part (5), turned into DM-ness over S by Stacks 050N part (1)”.

Stacks 06N0. A DM, locally Noetherian, reduced algebraic stack whose point space is a singleton admits a field k and a surjective étale 1-morphism Spec k ⟶ 𝒵.

The field-valued point is produced in two steps. Stacks 06MP, part (1) ⟹ (2), gives a surjective, flat, locally finitely presented ξ : Spec k ⟶ 𝒵; and AlgebraicGeometry.Stack.exists_isEtale_fieldSpectrum_cover_of_flat_fieldSpectrum_cover divides the groupoid of that flat presentation by the open subgroupoid through the identity and returns an étale 1-morphism out of the spectrum of the field of invariants. Surjectivity of that 1-morphism is read off the point space: |𝒵| is a subsingleton and the algebraic stack of the spectrum of a field has a point. The DM hypothesis is used at the division, in the absolute form of Stacks 050D part (5), turned into DM-ness over S by Stacks 050N part (1).

theorem hasSurjectiveEtaleFieldSpectrumCover_unconditional
    (𝒵 : AlgebraicStacks.{u, w} B S hS)
    (h𝒵 : IsReducedLocallyNoetherianSingletonDM.{u, w} B S hS hZ 𝒵) :
    HasSurjectiveEtaleFieldSpectrumCover.{u, w} B S hS 𝒵

Tag 06N2, a lemma

Tag 06N2 in the Stacks Project.

AlgebraicGeometry.Stack.exists_isOpenSubspace_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChartShrinkingOpenSubspace.lean, line 358. The attribute's comment: “the conclusion read on an open subspace of the algebraic space, as the source reads it: the composite of the 1-morphism of Stacks 0458 induced by an open subspace containing the image of the given point of the fibre with the given 1-morphism is etale. Nothing is added to exists_openSubstack_isEtale_unconditional: its open substack is carried to an open subspace with the same point set by exists_isOpenSubspace_property_eq_essImage, and the etaleness is carried across the Stacks 0506 factorization of that subspace's 1-morphism through the substack's inclusion by isEtale_comp_of_eq_essImage”.

Stacks 06N2, with the conclusion read on an open subspace of the chart. Let 𝒳 be an algebraic stack, let U be an algebraic space with a 1-morphism f : U ⟶ 𝒳 which is flat and locally of finite presentation, let Spec k ⟶ 𝒳 be a field-valued point and let F = U ×_𝒳 Spec k with projection p : F ⟶ U. If F ⟶ Spec k is unramified at z ∈ |F| then there is an open subspace V ⊆ U, in the sense of Stacks 02YU, part (2), whose point set contains p(z) and for which the composite of the 1-morphism of Stacks 0458 induced by V with f is étale.

This is the source's own conclusion, obtained from AlgebraicGeometry.Stack.exists_openSubstack_isEtale_unconditional the way AlgebraicGeometry.Stack.exists_isOpenSubspace_isLocallyQuasiFinite is obtained from Stacks 06ME, with AlgebraicGeometry.Stack.isEtale_comp_of_eq_essImage for the transport.

theorem exists_isOpenSubspace_isEtale
    (hflat : AlgebraicStacks.IsFlat B S hS f)
    (hfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS f)
    (z : AlgebraicStacks.points B S hS (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g))
    (hz : FibreIsUnramifiedNear.{u, w} B S hS 𝒳 U hU k hk toBase f g z) :
    ∃ (V : Subfunctor U) (hV : Space.IsOpenSubspace B S hS V),
      AlgebraicStacks.pointsMap B S hS
          (fibreProjection B S hS 𝒳 U hU k hk toBase f g) z ∈
        spacePointMap B S hS U (algebraicSpaceStack.{u, w} B S hS U hU).val
            (BasedFunctor.id (fibredCategory B S hS U).val) ''
          Set.range (Space.pointsMap B S hS V.toFunctor V.ι) ∧
        IsEtale B S hS (algebraicSpaceStackMap.{u, w} B S hS hV.1 hU V.ι ≫ f)

AlgebraicGeometry.Stack.exists_openSubstack_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChartShrinkingQuasiFiniteEtale.lean, line 285. The attribute's comment: “after replacing the algebraic space by an open subspace containing the image of the given point of the fibre, a flat, locally finitely presented 1-morphism whose fibre over a field-valued point is unramified at that point is etale. Three inputs are carried: the data W with hW and the hypothesis hBaseChange, which are the two clauses of Stacks 06M5 at etaleness, absent from this library; and hFibreEtale, which is Stacks 06LU for 1-morphisms of algebraic stacks over the field-valued point, available in this library only for morphisms of algebraic spaces. The deduction of the conclusion from them is proved”.

Stacks 06N2. Let 𝒳 be an algebraic stack, let U be an algebraic space with a 1-morphism f : U ⟶ 𝒳 which is flat and locally of finite presentation, let Spec k ⟶ 𝒳 be a field-valued point, and let F = U ×_𝒳 Spec k with projection p : F ⟶ U and structure 1-morphism q : F ⟶ Spec k. If q is unramified at z ∈ |F| then, after replacing U by an open subspace containing p(z), the 1-morphism U ⟶ 𝒳 is étale.

The proof is the source's. The open substack W is the locus W(f) of Stacks 06M5 on which f is étale, carried as the data W with hW, and its compatibility with the base change along g is carried as hBaseChange. The step from the source's pointwise hypothesis to étaleness of the fibre near z is Stacks 06LU — unramified plus flat plus locally of finite presentation gives étale — which the library has for morphisms of algebraic spaces (AlgebraicGeometry.Space.isEtale_of_isFlat_of_isUnramified) but not for 1-morphisms of algebraic stacks; it is carried as hFibreEtale, stated over Spec k, which is where the source applies it. Given those, the conclusion is that p(z) ∈ |W|.

theorem exists_openSubstack_isEtale
    (_hflat : AlgebraicStacks.IsFlat B S hS f)
    (_hfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS f)
    (W : OpenSubstack (algebraicSpaceStack.{u, w} B S hS U hU))
    (hW : IsEtale B S hS (W.inclusion ≫ f))
    (hFibreEtale : ∀ V : OpenSubstack (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g),
      IsUnramified B S hS
          (V.inclusion ≫ fibreStructureMorphism B S hS 𝒳 U hU k hk toBase f g) →
        IsEtale B S hS
          (V.inclusion ≫ fibreStructureMorphism B S hS 𝒳 U hU k hk toBase f g))
    (hBaseChange : ∀ V : OpenSubstack (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g),
      IsEtale B S hS
          (V.inclusion ≫ fibreStructureMorphism B S hS 𝒳 U hU k hk toBase f g) →
        V.pointSet B S hS ⊆
          AlgebraicStacks.pointsMap B S hS
              (fibreProjection B S hS 𝒳 U hU k hk toBase f g) ⁻¹' W.pointSet B S hS)
    (z : AlgebraicStacks.points B S hS (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g))
    (hz : FibreIsUnramifiedNear.{u, w} B S hS 𝒳 U hU k hk toBase f g z) :
    AlgebraicStacks.pointsMap B S hS
        (fibreProjection B S hS 𝒳 U hU k hk toBase f g) z ∈ W.pointSet B S hS ∧
      IsEtale B S hS (W.inclusion ≫ f)

AlgebraicGeometry.Stack.exists_openSubstack_isEtale_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChartShrinkingQuasiFiniteEtaleUnconditional.lean, line 229. The attribute's comment: “after replacing the algebraic space by an open subspace containing the image of the given point of the fibre, a flat, locally finitely presented 1-morphism whose fibre over a field-valued point is unramified at that point is etale. Nothing is carried: the open substack is the locus W(P, f) of assertion (A) of Stacks 06M3 at P = unramified -- the entry of the list of Stacks 06M5 whose base-change clause holds for an arbitrary base change, which is why it and not the etale entry applies to a base change along a field-valued point -- produced by exists_isRelativePropertyLocus_of_hasRelativePropertyLocusOnSpaces from the entry-(3) instances of LocalSourceLemmaUnramified, and the conclusion that the image of the given point of the fibre lies in it is the maximality half of assertion (B) at the open substack the fibre hypothesis supplies. The comparison of the two renderings of unramifiedness, Stacks 0CIT against the relative notion of Stacks 04XB, is available in both directions for a 1-morphism representable by algebraic spaces, by hasSurjectiveEtaleSmoothDiagram_of_isRepresentableByAlgebraicSpaces, and needs nothing of Stacks 0CIA. Stacks 06LU for 1-morphisms of algebraic stacks is not carried but proved, and it is what turns the locus into the etaleness of the conclusion”.

Stacks 06N2. Let 𝒳 be an algebraic stack, let U be an algebraic space with a 1-morphism f : U ⟶ 𝒳 which is flat and locally of finite presentation, let Spec k ⟶ 𝒳 be a field-valued point, and let F = U ×_𝒳 Spec k with projection p : F ⟶ U and structure 1-morphism q : F ⟶ Spec k. If q is unramified at z ∈ |F| then, after replacing U by an open subspace containing p(z), the 1-morphism U ⟶ 𝒳 is étale.

The proof is the source's, and nothing is carried. The open substack W is the locus W(𝒫, f) of assertion (A) of Stacks 06M3 at 𝒫 = unramifiedness — the entry of the list of Stacks 06M5 whose base-change clause holds for an arbitrary base change, and so the entry that applies to the base change along a field-valued point. It exists by AlgebraicGeometry.Stack.exists_isRelativePropertyLocus_of_hasRelativePropertyLocusOnSpaces at the entry-(3) instances AlgebraicGeometry.Stack.hasRelativePropertyLocusOnSpaces_isUnramified and AlgebraicGeometry.Stack.relativePropertyLocusBaseChange_isUnramified of StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaUnramified.lean, the source's 𝒬 being local finite type, which f has because it is locally of finite presentation (Stacks 0464).

The conclusion p(z) ∈ |W| is the maximality half of assertion (B), AlgebraicGeometry.Stack.pointSet_subset_preimage_of_hasRelativeProperty, at the open substack of F that the fibre hypothesis supplies. That step consumes unramifiedness in the relative sense of Stacks 04XB while the fibre hypothesis and the étaleness criterion are stated at AlgebraicGeometry.Stack.IsUnramified (Stacks 0CIT), and both directions of that comparison are available here because every 1-morphism in sight is representable by algebraic spaces: AlgebraicGeometry.Stack.hasRelativeProperty_unramified_of_isUnramified and AlgebraicGeometry.Stack.isUnramified_of_hasRelativeProperty_unramified, whose étale-smooth diagram comes from AlgebraicGeometry.Stack.hasSurjectiveEtaleSmoothDiagram_of_isRepresentableByAlgebraicSpaces and not from Stacks 0CIA. Given that comparison, an open W with hW and the base-change containment hBaseChange are not needed as hypotheses.

Étaleness of f|_W is Stacks 06LU for 1-morphisms of algebraic stacks, AlgebraicGeometry.Stack.isEtale_fullSubcategoryInclusion_comp_of_isUnramified, applied to the restriction of f to W, which is flat and locally of finite presentation because f is.

theorem exists_openSubstack_isEtale_unconditional
    (hflat : AlgebraicStacks.IsFlat B S hS f)
    (hfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS f)
    (z : AlgebraicStacks.points B S hS (fibreOverFieldPoint B S hS 𝒳 U hU k hk toBase f g))
    (hz : FibreIsUnramifiedNear.{u, w} B S hS 𝒳 U hU k hk toBase f g z) :
    ∃ W : OpenSubstack (algebraicSpaceStack.{u, w} B S hS U hU),
      AlgebraicStacks.pointsMap B S hS
          (fibreProjection B S hS 𝒳 U hU k hk toBase f g) z ∈ W.pointSet B S hS ∧
        IsEtale B S hS (W.inclusion ≫ f)

Tag 06N3, a theorem

Tag 06N3 in the Stacks Project.

AlgebraicGeometry.Stack.isAbsolutelyDM_iff_isDeligneMumfordStack_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AbsolutelyDMEtaleChartAssembly.lean, line 737. The attribute's comment: “the equivalence of (1) DM with (2) Deligne-Mumford and (3) the existence of a surjective etale presentation by a scheme; (2) and (3) are the same condition here, since Stacks 03YO defines Deligne-Mumford that way. The implication (2) => (1) is proved, from Stacks 06MB part (1); the structure theorem (1) => (3) is PROVED, not carried, as existsEtalePresentationOfIsAbsolutelyDM of this file -- the chart at ONE finite type point with the uniform size bound (exists_isRelativelyEtale_chart_size_le_of_isFiniteTypePoint) fed to the family assembly existsEtalePresentationOfIsAbsolutelyDM_of_forall_exists_chart. The statement binds only the containment hZ of the terminal scheme, which the absolute Deligne-Mumford condition is stated at, and the algebraic stack 𝒳, and nothing stands for the structure theorem. The CHART CONSTRUCTION it runs on, the source's etale chart at each finite type point together with the site-membership of their coproduct, is isolated as ExistsEtaleChartFamilyOfIsAbsolutelyDM, and delivers the presentation by existsEtalePresentationOfIsAbsolutelyDM_of_existsEtaleChartFamily. Everything the source does after the charts is proved, in isDeligneMumfordStack_of_forall_isRelativelyEtale: the 1-morphism out of the coproduct W = ∐_x Z_x is exists_stackMap_comp_iso_sigmaOver_of_lt_cof, its surjectivity is exists_isSurjective_stackMap_of_finiteTypePoints_subset_iUnion_range (resting on 06R7 and the corollary of 06G2 rather than on any property of the assembled chart), and its relative etaleness is isRelativelyEtale_of_isColimit_of_forall_isRelativelyEtale, the descent of the relative property of 03YK along the summand inclusions. NO TAG of the construction is carried. Stacks 06N0 is hasSurjectiveEtaleFieldSpectrumCover_unconditional, at its own binders: the division of the groupoid of the flat field-valued presentation by the open and closed subgroupoid through the identity is exists_division_identityArrowOpens_of_isoSpecField, on identityOpenFiniteSubgroupoid and mono_prodLift_of_unramified; the two tags it rests on are proved -- all four conclusions of 04S4 are exists_division and condition (2) of 06LZ is isRepresentable_of_isLocallyOfFiniteType_over_field; the construction carrying the stack-level flat presentation to a GroupoidScheme is the de-realization of the self-intersection groupoid, on isRepresentable_objects_pointGroupoid_fieldSpectrum and isRepresentable_arrows_pointGroupoid_fieldSpectrum; and the etaleness of Spec k_0 -> Z is isOpenImmersion_descended_identity and etale_descended_source read off the presentation through the quotient stack of the divided groupoid, by isEtale_quotientProjectionSchemeStackMap across the 046T equivalence nonempty_isEquivalenceOver_quotientStackMap_realizationHom, rather than by 04XD. So the source's unramified field-valued point at a finite type point follows outright, by exists_relativelyUnramified_fieldSpectrum_point_of_isFiniteTypePoint, whose own binders are its statement's. The step before it is PROVED and not carried: the residual gerbe exists, by 06G3 (1) => (3) (existsLocallyOfFiniteTypeResidualGerbe, which needs neither Artin's theorem 06DC nor 04Y5 (2) => (3), cutting the gerbe out of the target instead), its inclusion is a monomorphism (AlgebraicStacks.isMonomorphism_fullSubcategoryInclusion) and the gerbe is a reduced, locally Noetherian, one-point DM algebraic stack, which is exactly the hypothesis of 06N0 (isReducedLocallyNoetherianSingletonDM_of_isResidualGerbeAt, by 06MZ at that monomorphism). So 06G3 (1) => (3) is not carried either. Stacks 06MP (1) => (2) and both halves of 06MM are available. What else is missing is the body of the source's argument at a single finite type point -- the affine V etale over F = U x_X Spec k, its closed point with residue field finite separable over k, the regular sequence, and the slicing -- of which two steps are available: from the source's phi(m_u) O_{V,v} = m_v of 02GF, the regular sequence is exists_mem_maximalIdeal_isRegular_ofList_eq_maximalIdeal_fiberStalk_of_smooth, which produces it GENERATING the maximal ideal of the fibre stalk and not merely cutting it to dimension zero (the fibre stalk of a smooth morphism is regular, so a minimal generating family selected inside phi(m_u) by exists_fn_mem_maximalIdeal_ofList_map_eq_maximalIdeal is regular by 00NQ), and the residue computation O_{T,v} = kappa(v) off it is map_maximalIdeal_comp_eq_of_ofList_eq_maximalIdeal_fiberStalk, read on the scheme-theoretic fibre by isField_fiberStalk_comp_of_ofList_eq_maximalIdeal_fiberStalk. Both clauses of 02GF that body needs are proved as well, each off the unramifiedness of F -> U that the monomorphy of Z_x -> X gives: the PRODUCTION of phi(m_u) O_{V,v} = m_v, and with it the sequence generating m_v, is exists_fn_mem_maximalIdeal_isRegular_ofList_eq_maximalIdeal_stalk_of_unramifiedAt (with exists_isAffineOpen_isRegular_ofList_eq_maximalIdeal_stalk_of_unramifiedAt reading it as regular functions on an affine open, the source's first shrinking), and its passage to the ETALE local ring where 06MD reads its hypothesis is exists_fn_isRegular_ofList_eq_maximalIdeal_etaleLocalRing_of_unramifiedAt across the faithful flatness of 05VP and the square of local rings of 05VU, with forall_isRegular_etaleLocalRingMap_germ_of_isRegular_chartLocalRing the same passage in the germ shape FibreIsRegularSequenceAt is written in, quantifier over etale neighbourhoods included (it costs nothing, by etaleLocalRingMap_etaleLocalRingGerm_eval_eq), so that the fibre hypothesis of 06MD is reduced to a regular sequence in the ordinary local ring of a scheme chart of the fibre; the SECOND clause of 02GF for the slice, the transport of the finite separability of kappa(v)/k along O_{V,v} ->> O_{T,v}, is unramifiedAt_comp_of_ofList_eq_maximalIdeal_fiberStalk, on bijective_residueFieldMap_of_isPreimmersion, with unramifiedAt_comp_of_ofList_eq_maximalIdeal_stalk the same statement at a generating sequence read in O_{V,v} -- where the sequence above is produced -- the two agreeing over a field-valued point of the base by ofList_eq_maximalIdeal_fiberStalk_of_ofList_eq_maximalIdeal. The SLICING POINT of that body is proved too, with everything both slicing lemmas read off it: exists_isClosed_isAffineOpen_isRegular_ofList_eq_maximalIdeal_finiteSeparable_of_unramified of SmoothSliceSeparablePoint takes an unramified q : V -> U of schemes with V nonempty and smooth over Spec k and returns the closed point v of 056U, the regularity of O_{V,v}, the sequence of regular functions on an affine open of U whose germs generate m_v as a regular sequence, and the residue field extension in the shape the criterion of 02GF reads it; the two come stated over DIFFERENT renderings of kappa(v) as an extension -- 056U through evaluation of global sections of Spec k, the criterion over kappa(pi v) through residueFieldMap -- and the reconciliation is finite_separable_residueFieldMap_of_finite_separable_Gammaevaluation of the same file, the two algebra structures sitting in one scalar tower by Gammaevaluation_naturality, with isRegularLocalRing_stalk_of_smooth_over_field the scheme form of the regularity (056S on stalks through 02IT) and unramifiedAt_comp_of_ofList_eq_maximalIdeal_stalk_over_field the unramifiedness of the slice with the hypothesis on the base discharged, the local ring of Spec k being the field itself. The slicing sequence in the etale local ring is likewise available off the hypotheses the assembly PRODUCES rather than off a chart square: exists_fn_isRegular_ofList_eq_maximalIdeal_etaleLocalRing_of_isUnramified of FibreSlicingSequenceFromIsUnramified asks only for Space.IsUnramified of the projection F -> U and regularity of F, discharging the chart-square hypotheses itself by unramified_chartMap_of_isUnramified (what Space.IsUnramified says, 03ZH part (1)) and isRegularLocalRing_chartLocalRing (06M1's etale-local regularity carried to a prescribed small etale neighbourhood by 03E8 and read on the stalk by 02IT). What remains of the body is its ASSEMBLY at one finite type point, and that is now exactly the identifications and the plumbing. The relative unramifiedness of exists_relativelyUnramified_fieldSpectrum_point_of_isFiniteTypePoint is NOT carried: read at a chart it is Space.IsUnramified of the projection F -> U of the fibre F = U x_X Spec k, by isUnramified_fibreSpaceProjection_of_relativeProperty of FibreProjectionUnramified, which carries the relative condition to the projection by 045C (hasRelativeProperty_baseChange_algebraicStacks) and reads it on the representing morphism by the 04XB bridge (hasRelativeProperty_iff_prop_representingMap); with the regularity of F that gives the slicing sequence in the etale local ring off the stack-level hypotheses alone, exists_fn_isRegular_ofList_eq_maximalIdeal_etaleLocalRing_fibre of the same file. Its companions are proved, the REGULARITY of F being hasEtaleLocalProperty_isRegular_fibreSpace of ChartFibreRegularity (06M1 at the structure morphism F -> Spec k, smooth by 075W because the chart is, by isSmooth_fibreStructureMorphism) in the form isRegularLocalRing_chartLocalRing consumes, and the NONEMPTINESS of F being exists_point_fibreOverFieldPoint_of_range_eq_singleton of the same file (04XH at a point of Spec k, which the singleton range of the field-valued point supplies). The GEOMETRIC POINT over the closed point of an etale chart of F is available too: every point of an etale chart is the chart point of a small etale neighbourhood of a geometric point of the space, by exists_chartGeometricPoint_chartPoint_eq of ChartSlicingGeometricPoint (03BX part (1) and exists_geometricRepresentative on the chart, pushed forward by ofChartGeometricPoint), and exists_chartGeometricPoint_isClosed_isRegularLocalRing_finiteSeparable of the same file puts the 056U closed point of a chart nonempty and smooth over Spec k, with its regular local ring and its finite separable residue field extension, at such a geometric point. The PLUMBING of the slice as a scheme of the site is proved too, in EtaleChartFamilySizeBound: a monomorphism of schemes into a chart U of the site makes its source an object of the site over U of size at most 2 ^ 2 ^ size U0 whenever size U <= size U0, which is the bound 06FX delivers (exists_siteObject_toScheme_map_eq_size_le), and with that bound uniform in the point exists_etaleChartFamily_of_forall_isFiniteTypePoint assembles the family of ExistsEtaleChartFamilyOfIsAbsolutelyDM with its site-membership conjunct, indexed by the points the substantial direction follows from the chart at ONE finite type point, by existsEtalePresentationOfIsAbsolutelyDM_of_forall_exists_chart, and nothing about the family, the index type or the coproduct is needed. Two further inputs are proved. The affine etale chart V of F through a prescribed point of |F|, with its scheme smooth over Spec k as a morphism of schemes, is exists_affine_smallEtale_smooth_chartScheme_at_point of AffineSmoothChartAtPoint, on exists_affine_etale_chart_at_point and on 03ZC part (1) read at the square against the IDENTITY chart of the representing object of Spec k (isEtaleChart_id), whose morphism of schemes is the chart's own structure morphism -- smooth_chartMap_of_isSmooth and smooth_toScheme_map_of_isSmooth_yoneda, the mirrors at smoothness of unramified_chartMap_of_isUnramified; with the 056U slicing point on it that is exists_affine_chartGeometricPoint_isClosed_isRegularLocalRing_finiteSeparable of the same file, and the space-level smoothness it consumes is isSmooth_fibreStructureMorphism read on the representing map by isSmooth_representingMap_of_isSmooth. And the shrinking of U that was to make the f_i global functions on the algebraic space U is NOT NEEDED: on a chart whose scheme is AFFINE the sequence may be chosen among the GLOBAL functions outright, the minimal generating family of exists_fn_mem_ofList_eq_maximalIdeal_of_span_eq being selectable inside any prescribed generating set and the global germs generating m_u because the stalk of an affine scheme is a localization of its global functions (span_image_preimage_germ_top_eq_maximalIdeal and exists_global_isRegular_ofList_eq_maximalIdeal_stalk_of_unramifiedAt of GlobalSlicingSequenceAffine), and a global function on the representing scheme IS a global section of the structure sheaf of the small etale site of a represented algebraic space, the identity chart being terminal there (representedUnitSection and eval_representedUnitSection of RepresentedGlobalSections, on isTerminal_idChart) -- no etale descent for O and nothing of 05B2 enters. The two together give the fibre hypothesis of 06MD and the generation the 02GF criterion reads, in exists_representedUnitSection_isRegular_etaleLocalRing_of_isAffine of FibreGlobalSlicingSequenceAffine, and that the 06FX chart is affine is recorded in the conclusion of exists_isClosed_smoothChart_size_le_of_isFiniteTypePoint. The PLUMBING of that body into existsEtalePresentationOfIsAbsolutelyDM_of_forall_exists_chart is PROVED, in exists_isRelativelyEtale_chart_size_le_of_isFiniteTypePoint of this file, from the following three inputs. The 06FX chart schemeStack U -> X is read as the 1-morphism algebraicSpaceStack (yoneda U) -> X that 06MD slices by algebraicSpaceStackChart of SchemeChartAsAlgebraicSpaceChart. The vanishing hypothesis of unramifiedAt_comp_of_ofList_eq_maximalIdeal_stalk_over_field, which asks for the chart of the slice to be identified with the zero scheme of the pulled-back functions, is supplied by definingIdealAt_vanishingSubspace_globalFunctionsMap_eq_ofList of FibreSliceChartZeroScheme, read at the chart by forall_unramifiedAt_toScheme_map_rep_snd_comp_of_eq_vanishingSubfunctor of ChartSliceUnramifiedFieldPoint and carried to the fibre hypothesis of 06N2 by exists_fibreIsUnramifiedNear_zeroLocusOnOpen_of_forall_germ_mem_maximalIdeal of SliceFibreSubspaceComparison. And the shrinking that turns the flat, locally finitely presented slice into a relatively etale chart BY A SCHEME OF THE SITE needs NEITHER an etale analogue of the relation-slice route NOR the missing direction of the open-substack correspondence: 06N2 read as exists_isOpenSubspace_isEtale_mem_range_pointsMap of EtaleChartStackPointMembership returns an open SUBSPACE of U, its point-set clause read off the singleton range of the field-valued point rather than off any bijectivity of spacePointMap, and exists_siteObject_isRelativelyEtale_chart_of_mem_range of EtaleChartOpenSubspaceSiteObject reads that subspace as a scheme of the site through a representing isomorphism. The FIBRE HYPOTHESIS of 06N2, FibreIsUnramifiedNear, is PROVED, in FibreUnramifiedNearSubstack, off the unramifiedness of the slice over Spec k at the sliced point as a morphism of schemes -- fibreIsUnramifiedNear_of_unramifiedAt. Two steps: that scheme-level statement is lifted to Space.IsUnramifiedAt of the structure morphism of the fibre read through a representing algebraic space Fsp, hence to an open subspace W of Fsp unramified over Spec k around the point (exists_isOpenSubspace_isUnramified_fibreSpace_of_unramifiedAt of FibreUnramifiedFromChart, off the chart criterion isUnramifiedAt_chartPoint_iff of UnramifiedAtChart, the mirror at unramifiedness of isFlatAt_chart_iff); and W is read as an OPEN SUBSTACK cut out by the ESSENTIAL IMAGE of S_W -> S_Fsp -> F, which is an open immersion by isOpenImmersion_algebraicSpaceStackMap_of_isOpenImmersion and isOpenImmersion_comp_of_quasiInverse, so 0506 both makes that essential image an open substack and factors the composite through it by an equivalence -- and that factorization is what carries all three of the things the clause needs. 003Z (2) upgrades it to an equivalence OVER THE SITE, so the open substack is represented by the algebraic space W (isRepresentableByAlgebraicSpace_essImage_of_isImmersion); the morphism of representing presheaves 04SW attaches to S_W -> F -> Spec k is computed outright to be W.iota followed by fibreSpaceStructureMorphism (representingMap_openSubspaceFibreMap_comp, on representingMap_associatedMap and representingMap_equivalenceOverInvMap), so the relative property of 03YK at unramifiedness holds of S_W -> Spec k by the 04XB bridge hasRelativeProperty_iff_prop_representingMap and transports to the open substack by 0457 (relativeProperty_of_equivalences_symm), the DM conjunct being 050E (3) at that representability; and the point-set membership is mem_range_pointsMap_openSubspaceFibreMap, on AlgebraicStacks.pointsMap_comp and pointsMap_eq_of_hom2. The open substack there is NOT the one exists_openSubstack_mem_pointSet_of_isOpenSubspace produces from the surjectivity half of 06FJ, which carries no representing datum. Invariance of Stack.IsUnramified under precomposition with an equivalence with NO representability hypothesis is not needed, and remains available only for a 1-morphism representable by algebraic spaces, where IsDM, IsFlat, IsSmooth and HasRelativeProperty have it outright. 056U, which gives that closed point at an affine etale chart of the algebraic space F, is formalized as dense_closedPoints_with_finite_separable_residueField_of_smooth, with its space-level form 07W4 as dense_setOf_class_finiteSeparable_of_isSmooth, which is stated over the base Spec k itself and so is not the form the assembly uses. 06MD is not missing either, in either conjunct: exists_openSubspace_isFlat_isLocallyOfFinitePresentation_zeroLocus_of_isRegular carries the tag at the hypotheses the source states, so the slice may be cut the source's way and need not go through the relation-slice descent the 06MF chart uses; the hypothesis it consumes is the regular sequence read in the ETALE local ring of F at a geometric point, which is regular by 06M1 (isRegular_of_isSmooth_over_field). The flatness conjunct of 06MD is likewise not carried as the hypothesis ZeroLocusIsFlatOverSmoothChart of ChartSlicingRegularSequence. Stacks 06N2 is not missing: exists_openSubstack_isEtale is proved outright, the comparison of Stacks 0CIT with the relative notion of 04XB being available for a representable 1-morphism by hasSurjectiveEtaleSmoothDiagram_of_isRepresentableByAlgebraicSpaces, which needs nothing of Stacks 0CIA”.

Stacks 06N3. An algebraic stack is DM exactly when it is Deligne–Mumford — equivalently, by Stacks 03YO, exactly when there is a scheme of the site carrying a representable, surjective, étale 1-morphism to it.

Both directions are proved and nothing is assumed. The implication (2) ⟹ (1) — equivalently (3) ⟹ (1), these being the same condition here — is AlgebraicGeometry.Stack.isAbsolutelyDM_of_isDeligneMumfordStack, off part (1) of Stacks 06MB. The substantial direction (1) ⟹ (3) is AlgebraicGeometry.Stack.existsEtalePresentationOfIsAbsolutelyDM of this file: the source's étale chart at one finite type point, with the size bound uniform in the point (AlgebraicGeometry.Stack.exists_isRelativelyEtale_chart_size_le_of_isFiniteTypePoint), fed to the family assembly AlgebraicGeometry.Stack.existsEtalePresentationOfIsAbsolutelyDM_of_forall_exists_chart, which builds the index type, puts the coproduct in the site, and produces the surjective relatively étale 1-morphism out of it (AlgebraicGeometry.Stack.isDeligneMumfordStack_of_forall_isRelativelyEtale).

The substantial direction, AlgebraicGeometry.Stack.ExistsEtalePresentationOfIsAbsolutelyDM, reduced to the chart construction AlgebraicGeometry.Stack.ExistsEtaleChartFamilyOfIsAbsolutelyDM, is proved and not carried as a hypothesis. The statement cannot be placed in StacksFrontier.AlgebraicGeometry.Stacks.DeligneMumfordPresentationTheorem: StacksFrontier.AlgebraicGeometry.Stacks.EtaleChartFamilySizeBound, which this file needs for the family assembly, imports that module, so naming AlgebraicGeometry.Stack.existsEtalePresentationOfIsAbsolutelyDM there would be an import cycle.

The attribute below records where each step of the source's argument is.

theorem isAbsolutelyDM_iff_isDeligneMumfordStack_unconditional
    (hZ : B.Contains (⊤_ Scheme.{u})) (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    AlgebraicStacks.IsAbsolutelyDM B S hS hZ 𝒳 ↔
      IsDeligneMumfordStack.{u, w} B S hS 𝒳.val.val

AlgebraicGeometry.Stack.isAbsolutelyDM_iff_isDeligneMumfordStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordPresentationTheorem.lean, line 177. The attribute's comment: “the equivalence of (1) DM with (2) Deligne-Mumford and (3) the existence of a surjective etale presentation by a scheme; (2) and (3) are the same condition here, since Stacks 03YO defines Deligne-Mumford that way. Both implications are carried, as the hypotheses hForward (the structure theorem: Stacks 06MD, 06N0, 06N2, 06G2, 06G3 are absent) and hBackward (Stacks 06MB part (1) is present but the bridge from the Section 04XB form of an etale chart to the smooth-diagram flatness of Stacks 06PW is absent)”.

Stacks 06N3. An algebraic stack is DM exactly when it is Deligne–Mumford — equivalently, by Stacks 03YO, exactly when there is a scheme of the site with a representable, surjective, étale 1-morphism to it.

Both implications are carried; see AlgebraicGeometry.Stack.ExistsEtalePresentationOfIsAbsolutelyDM and AlgebraicGeometry.Stack.IsAbsolutelyDMOfExistsEtalePresentation for what each one stands for and why.

theorem isAbsolutelyDM_iff_isDeligneMumfordStack
    (hForward : ExistsEtalePresentationOfIsAbsolutelyDM.{u, w} B S hS hZ)
    (hBackward : IsAbsolutelyDMOfExistsEtalePresentation.{u, w} B S hS hZ)
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    AlgebraicStacks.IsAbsolutelyDM B S hS hZ 𝒳 ↔
      IsDeligneMumfordStack.{u, w} B S hS 𝒳.val.val

AlgebraicGeometry.Stack.isAbsolutelyDM_of_isDeligneMumfordStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordPresentationUnconditional.lean, line 346. The attribute's comment: “the implication (2) => (1), equivalently (3) => (1), these being the same condition here: an algebraic stack admitting a surjective etale presentation by a scheme is DM”.

A Deligne–Mumford algebraic stack is DM: the implication (2) ⟹ (1), equivalently (3) ⟹ (1), these being the same condition here.

theorem isAbsolutelyDM_of_isDeligneMumfordStack (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsDeligneMumfordStack.{u, w} B S hS 𝒳.val.val) :
    AlgebraicStacks.IsAbsolutelyDM B S hS hZ 𝒳

Tag 0CIA, a lemma

Tag 0CIA in the Stacks Project.

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

Stacks 0CIA, part (1). Let f : 𝒳 ⟶ 𝒴 be a DM 1-morphism of algebraic stacks. For every DM algebraic stack 𝒵 and 1-morphism g : 𝒵 ⟶ 𝒴 there is a scheme with a surjective étale 1-morphism onto 𝒳 ×_{f, 𝒴, g} 𝒵.

theorem isDeligneMumfordStack_twoFibreProduct_of_isDM_of_dm
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (hf : Stack.IsDM B S hS f) (h𝒵 : IsAbsolutelyDM B S hS B.contains_terminal 𝒵) :
    Stack.IsDeligneMumfordStack.{u, w} B S hS
      (Stack.twoFibreProductSquareAlgebraicStacks B S hS f g).pt.val.val

AlgebraicGeometry.Stack.AlgebraicStacks.isDeligneMumfordStack_twoFibreProduct_of_isDM_algebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordFibreProductPresentation.lean, line 56. The attribute's comment: “part (2)”.

Stacks 0CIA, part (2). Let f : 𝒳 ⟶ 𝒴 be a DM 1-morphism of algebraic stacks. For every algebraic space Z and 1-morphism g : Z ⟶ 𝒴 there is a scheme with a surjective étale 1-morphism onto 𝒳 ×_{f, 𝒴, g} Z.

theorem isDeligneMumfordStack_twoFibreProduct_of_isDM_algebraicSpace
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (hf : Stack.IsDM B S hS f)
    (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hZ : IsAlgebraicSpace B S hS Z)
    (g : Stack.algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒴) :
    Stack.IsDeligneMumfordStack.{u, w} B S hS
      (Stack.twoFibreProductSquareAlgebraicStacks B S hS f g).pt.val.val

AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_twoFibreProduct_of_isDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordSpecialPresentation.lean, line 126. The attribute's comment: “part (1), the Deligne-Mumford condition on the 2-fibre product: the apex of the canonical square of a DM 1-morphism f and a 1-morphism out of a DM algebraic stack is itself a DM algebraic stack. This is the source's own argument for part (1) up to its closing appeal to Stacks 06N3; that appeal is made in AlgebraicGeometry.Stack.AlgebraicStacks.isDeligneMumfordStack_twoFibreProduct_of_isDM, which states part (1) in the source's existence form”.

A 2-fibre product of a Deligne–Mumford 1-morphism over a Deligne–Mumford algebraic stack is Deligne–Mumford. The projection of the canonical square of (f, g) to 𝒵 is a base change of f, so it is Deligne–Mumford by Stacks 050F, and a stack Deligne–Mumford over a Deligne–Mumford stack is Deligne–Mumford by Stacks 050L.

This is the first half of the argument for part (1) of Stacks 0CIA; the half left is the structure theorem Stacks 06N3, which turns the conclusion into a surjective étale presentation of the apex by a scheme and is applied in AlgebraicGeometry.Stack.AlgebraicStacks.isDeligneMumfordStack_twoFibreProduct_of_isDM.

theorem isAbsolutelyDM_twoFibreProduct_of_isDM
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (hf : Stack.IsDM B S hS f) (h𝒵 : IsAbsolutelyDM B S hS hT 𝒵) :
    IsAbsolutelyDM B S hS hT (Stack.twoFibreProductSquareAlgebraicStacks B S hS f g).pt

AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_twoFibreProduct_algebraicSpaceStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordSpecialPresentation.lean, line 148. The attribute's comment: “part (2), the Deligne-Mumford condition on the 2-fibre product: the apex of the canonical square of a DM 1-morphism f and a 1-morphism out of an algebraic space is a DM algebraic stack, with no hypothesis on the algebraic space. This is the source's own reduction of part (2) to part (1), up to the closing appeal to Stacks 06N3; that appeal is made in AlgebraicGeometry.Stack.AlgebraicStacks.isDeligneMumfordStack_twoFibreProduct_algebraicSpace, which states part (2) in the source's existence form”.

A 2-fibre product of a Deligne–Mumford 1-morphism over an algebraic space is Deligne–Mumford. The source's reduction of part (2) of Stacks 0CIA to part (1): an algebraic space is Deligne–Mumford when read as an algebraic stack, so no hypothesis beyond Deligne–Mumfordness of f is needed.

As for AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_twoFibreProduct_of_isDM, what is left of Stacks 0CIA after this is one application of Stacks 06N3, made in AlgebraicGeometry.Stack.AlgebraicStacks.isDeligneMumfordStack_twoFibreProduct_algebraicSpace.

theorem isAbsolutelyDM_twoFibreProduct_algebraicSpaceStack
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (hf : Stack.IsDM B S hS f)
    (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hZ : IsAlgebraicSpace B S hS Z)
    (g : Stack.algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒴) :
    IsAbsolutelyDM B S hS hT (Stack.twoFibreProductSquareAlgebraicStacks B S hS f g).pt

AlgebraicGeometry.Stack.AlgebraicStacks.isDeligneMumfordStack_twoFibreProduct_of_isDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordSpecialPresentation.lean, line 170. The attribute's comment: “part (1), in the source's existence form: a scheme with a surjective etale 1-morphism onto the 2-fibre product, with the substantial direction of Stacks 06N3 as the explicit hypothesis hForward (the structure theorem behind it, Stacks 06MD, 06N0, 06N2, 06G2, 06G3, is absent from the library). The Deligne-Mumford condition on the apex, which is the whole of the source's argument apart from that appeal, is proved unconditionally in AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_twoFibreProduct_of_isDM”.

Stacks 0CIA, part (1). Let f : 𝒳 ⟶ 𝒴 be a Deligne–Mumford 1-morphism of algebraic stacks. For every Deligne–Mumford algebraic stack 𝒵 over 𝒴 there is a scheme of the site with a surjective étale 1-morphism onto 𝒳 ×_{f, 𝒴, g} 𝒵.

The apex is a Deligne–Mumford algebraic stack by AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_twoFibreProduct_of_isDM, and the presentation comes from the structure theorem Stacks 06N3, carried here as the hypothesis hForward.

theorem isDeligneMumfordStack_twoFibreProduct_of_isDM
    (hForward : Stack.ExistsEtalePresentationOfIsAbsolutelyDM.{u, w} B S hS hT)
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (hf : Stack.IsDM B S hS f) (h𝒵 : IsAbsolutelyDM B S hS hT 𝒵) :
    Stack.IsDeligneMumfordStack.{u, w} B S hS
      (Stack.twoFibreProductSquareAlgebraicStacks B S hS f g).pt.val.val

AlgebraicGeometry.Stack.AlgebraicStacks.isDeligneMumfordStack_twoFibreProduct_algebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordSpecialPresentation.lean, line 191. The attribute's comment: “part (2), in the source's existence form: a scheme with a surjective etale 1-morphism onto the 2-fibre product with an algebraic space, with the substantial direction of Stacks 06N3 as the explicit hypothesis hForward (the structure theorem behind it, Stacks 06MD, 06N0, 06N2, 06G2, 06G3, is absent from the library). The Deligne-Mumford condition on the apex is proved unconditionally in AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_twoFibreProduct_algebraicSpaceStack”.

Stacks 0CIA, part (2). Let f : 𝒳 ⟶ 𝒴 be a Deligne–Mumford 1-morphism of algebraic stacks. For every algebraic space Z over 𝒴 there is a scheme of the site with a surjective étale 1-morphism onto 𝒳 ×_{f, 𝒴, g} Z, with no further hypothesis on Z.

This is part (1) applied to the algebraic space read as an algebraic stack, which is Deligne–Mumford by AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_algebraicSpaceStack.

theorem isDeligneMumfordStack_twoFibreProduct_algebraicSpace
    (hForward : Stack.ExistsEtalePresentationOfIsAbsolutelyDM.{u, w} B S hS hT)
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (hf : Stack.IsDM B S hS f)
    (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hZ : IsAlgebraicSpace B S hS Z)
    (g : Stack.algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒴) :
    Stack.IsDeligneMumfordStack.{u, w} B S hS
      (Stack.twoFibreProductSquareAlgebraicStacks B S hS f g).pt.val.val

Sources

LeanAlgebraicGeometry.Stack.exists_openSubspace_isLocallyOfFinitePresentation_zeroLocus · AlgebraicGeometry.Stack.exists_openSubspace_isFlat_isLocallyOfFinitePresentation_zeroLocus_of_isRegular · AlgebraicGeometry.Stack.exists_openSubstack_isLocallyQuasiFinite · AlgebraicGeometry.Stack.exists_openSubstack_isLocallyQuasiFinite_of_dimensionAtPoint_eq_zero · AlgebraicGeometry.Stack.exists_isOpenSubspace_isLocallyQuasiFinite_of_dimensionAtPoint_eq_zero · AlgebraicGeometry.Stack.isAbsolutelyQuasiDM_iff_hasQuasiDMPresentation · AlgebraicGeometry.Stack.isAbsolutelyQuasiDM_of_hasQuasiDMPresentation · AlgebraicGeometry.Stack.isAbsolutelyQuasiDM_iff_hasQuasiDMPresentation_unconditional

Section101.22 The Deligne-Mumford locus #

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

Tag 0DSM, a lemma

Tag 0DSM in the Stacks Project.

AlgebraicGeometry.Stack.dmLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordLocus.lean, line 124. The attribute's comment: “the DM locus, as the supremum of the DM open substacks”.

Stacks 0DSM, the Deligne–Mumford locus. The object property of an algebraic stack 𝒳 cut out by the supremum of the object properties of its Deligne–Mumford open substacks; this is the substack 𝒳'' of the source.

noncomputable def dmLocus (hZ : B.Contains (⊤_ Scheme.{u}))
    (𝒳 : AlgebraicStacks.{u, w} B S hS) : ObjectProperty 𝒳.val.val.obj

AlgebraicGeometry.Stack.quasiDMLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordLocus.lean, line 132. The attribute's comment: “the quasi-DM locus, as the supremum of the quasi-DM open substacks”.

Stacks 0DSM, the quasi-Deligne–Mumford locus. The object property of an algebraic stack 𝒳 cut out by the supremum of the object properties of its quasi-Deligne–Mumford open substacks; this is the substack 𝒳' of the source.

noncomputable def quasiDMLocus (hZ : B.Contains (⊤_ Scheme.{u}))
    (𝒳 : AlgebraicStacks.{u, w} B S hS) : ObjectProperty 𝒳.val.val.obj

AlgebraicGeometry.Stack.le_dmLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordLocus.lean, line 163. The attribute's comment: “maximality of the DM locus”.

Stacks 0DSM, maximality for the DM locus. Every Deligne–Mumford open substack of 𝒳 is contained in the Deligne–Mumford locus. This is the force of the word largest in the source, and it holds with no hypothesis beyond those of the ambient site.

theorem le_dmLocus (U : OpenSubstack 𝒳)
    (hU : AlgebraicStacks.IsAbsolutelyDM B S hS hZ U.toAlgebraicStack) :
    U.property ≤ dmLocus B S hS hZ 𝒳

AlgebraicGeometry.Stack.le_quasiDMLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordLocus.lean, line 171. The attribute's comment: “maximality of the quasi-DM locus”.

Stacks 0DSM, maximality for the quasi-DM locus. Every quasi-Deligne–Mumford open substack of 𝒳 is contained in the quasi-Deligne–Mumford locus.

theorem le_quasiDMLocus (U : OpenSubstack 𝒳)
    (hU : AlgebraicStacks.IsAbsolutelyQuasiDM B S hS hZ U.toAlgebraicStack) :
    U.property ≤ quasiDMLocus B S hS hZ 𝒳

AlgebraicGeometry.Stack.dmLocus_le_quasiDMLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordLocus.lean, line 198. The attribute's comment: “the DM locus is contained in the quasi-DM locus”.

Stacks 0DSM, the nesting 𝒳'' ⊆ 𝒳'. The Deligne–Mumford locus is contained in the quasi-Deligne–Mumford locus, because a Deligne–Mumford open substack is quasi-Deligne–Mumford by Stacks 050E (AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_of_isDM). This holds with no further input.

theorem dmLocus_le_quasiDMLocus :
    dmLocus B S hS hZ 𝒳 ≤ quasiDMLocus B S hS hZ 𝒳

AlgebraicGeometry.Stack.exists_largest_isAbsolutelyDM_openSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordLocus.lean, line 270. The attribute's comment: “existence of the largest DM open substack; the structure theorem Stacks 06N3 is not in the library, so its two uses are carried as the hypotheses hLocal (a union of DM open substacks is DM) and hOpen (the DM locus is cut out by an open substack)”.

Stacks 0DSM for the DM property. An algebraic stack has a largest Deligne–Mumford open substack, and it cuts out the Deligne–Mumford locus.

Two inputs are carried, both standing for Stacks 06N3, which the library does not have: hOpen, that the Deligne–Mumford locus is cut out by an open substack at all, and hLocal, the local-global step. Maximality is not among them — it is AlgebraicGeometry.Stack.le_dmLocus, which holds unconditionally.

theorem exists_largest_isAbsolutelyDM_openSubstack
    (hLocal : IsAbsolutelyDMLocalOnOpenSubstacks.{u, w} B S hS hZ)
    (hOpen : ∃ W : OpenSubstack 𝒳, W.property = dmLocus B S hS hZ 𝒳) :
    ∃ W : OpenSubstack 𝒳,
      W.property = dmLocus B S hS hZ 𝒳 ∧
      AlgebraicStacks.IsAbsolutelyDM B S hS hZ W.toAlgebraicStack ∧
      ∀ V : OpenSubstack 𝒳, AlgebraicStacks.IsAbsolutelyDM B S hS hZ V.toAlgebraicStack →
        V.property ≤ W.property

AlgebraicGeometry.Stack.exists_largest_isAbsolutelyQuasiDM_openSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordLocus.lean, line 289. The attribute's comment: “existence of the largest quasi-DM open substack; the structure theorem Stacks 06MF is not in the library, so its two uses are carried as the hypotheses hLocal (a union of quasi-DM open substacks is quasi-DM) and hOpen (the quasi-DM locus is cut out by an open substack)”.

Stacks 0DSM for the quasi-DM property. An algebraic stack has a largest quasi-Deligne–Mumford open substack, and it cuts out the quasi-Deligne–Mumford locus. The two carried inputs stand for Stacks 06MF, as in AlgebraicGeometry.Stack.exists_largest_isAbsolutelyDM_openSubstack.

theorem exists_largest_isAbsolutelyQuasiDM_openSubstack
    (hLocal : IsAbsolutelyQuasiDMLocalOnOpenSubstacks.{u, w} B S hS hZ)
    (hOpen : ∃ W : OpenSubstack 𝒳, W.property = quasiDMLocus B S hS hZ 𝒳) :
    ∃ W : OpenSubstack 𝒳,
      W.property = quasiDMLocus B S hS hZ 𝒳 ∧
      AlgebraicStacks.IsAbsolutelyQuasiDM B S hS hZ W.toAlgebraicStack ∧
      ∀ V : OpenSubstack 𝒳, AlgebraicStacks.IsAbsolutelyQuasiDM B S hS hZ V.toAlgebraicStack →
        V.property ≤ W.property

AlgebraicGeometry.Stack.exists_nested_largest_isAbsolutelyDM_isAbsolutelyQuasiDM_openSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordLocus.lean, line 314. The attribute's comment: “the lemma: nested largest DM and quasi-DM open substacks. The structure theorems Stacks 06N3 and 06MF are not in the library, so their uses are carried as the hypotheses hLocalDM, hLocalQuasiDM (a union of DM, resp. quasi-DM, open substacks has that property) and hOpenDM, hOpenQuasiDM (each locus is cut out by an open substack)”.

Stacks 0DSM. For an algebraic stack 𝒳 there are open substacks 𝒳'' ⊆ 𝒳' ⊆ 𝒳 with 𝒳'' Deligne–Mumford, 𝒳' quasi-Deligne–Mumford, and each the largest open substack of 𝒳 with its property. This is the statement of the source lemma.

The four carried hypotheses are the two uses apiece of Stacks 06N3 and Stacks 06MF described on AlgebraicGeometry.Stack.exists_largest_isAbsolutelyDM_openSubstack and AlgebraicGeometry.Stack.exists_largest_isAbsolutelyQuasiDM_openSubstack. The nesting 𝒳'' ⊆ 𝒳' is not among them: it is AlgebraicGeometry.Stack.dmLocus_le_quasiDMLocus, which holds unconditionally.

theorem exists_nested_largest_isAbsolutelyDM_isAbsolutelyQuasiDM_openSubstack
    (hLocalDM : IsAbsolutelyDMLocalOnOpenSubstacks.{u, w} B S hS hZ)
    (hLocalQuasiDM : IsAbsolutelyQuasiDMLocalOnOpenSubstacks.{u, w} B S hS hZ)
    (hOpenDM : ∃ W : OpenSubstack 𝒳, W.property = dmLocus B S hS hZ 𝒳)
    (hOpenQuasiDM : ∃ W : OpenSubstack 𝒳, W.property = quasiDMLocus B S hS hZ 𝒳) :
    ∃ W' W'' : OpenSubstack 𝒳,
      W''.property ≤ W'.property ∧
      AlgebraicStacks.IsAbsolutelyDM B S hS hZ W''.toAlgebraicStack ∧
      AlgebraicStacks.IsAbsolutelyQuasiDM B S hS hZ W'.toAlgebraicStack ∧
      (∀ V : OpenSubstack 𝒳, AlgebraicStacks.IsAbsolutelyDM B S hS hZ V.toAlgebraicStack →
        V.property ≤ W''.property) ∧
      ∀ V : OpenSubstack 𝒳, AlgebraicStacks.IsAbsolutelyQuasiDM B S hS hZ V.toAlgebraicStack →
        V.property ≤ W'.property

AlgebraicGeometry.Stack.exists_nested_largest_isAbsolutelyDM_openSubstacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordLocusExistence.lean, line 324.

Stacks 0DSM. Let 𝒳 be an algebraic stack. There exist open substacks 𝒳'' ⊆ 𝒳' ⊆ 𝒳 such that 𝒳'' is DM, 𝒳' is quasi-DM, and these are the largest open substacks with these properties.

Here W'' is 𝒳'' and W' is 𝒳'. DM and quasi-DM are the absolute notions of Stacks 050D, parts (5) and (6), read over the terminal scheme Spec ℤ, which every big fppf site contains (AlgebraicGeometry.BigFppfSite.contains_terminal); containment of open substacks is containment of their objects.

theorem exists_nested_largest_isAbsolutelyDM_openSubstacks :
    ∃ W' W'' : OpenSubstack 𝒳,
      W''.property ≤ W'.property ∧
      AlgebraicStacks.IsAbsolutelyDM B S hS B.contains_terminal W''.toAlgebraicStack ∧
      AlgebraicStacks.IsAbsolutelyQuasiDM B S hS B.contains_terminal W'.toAlgebraicStack ∧
      (∀ V : OpenSubstack 𝒳,
        AlgebraicStacks.IsAbsolutelyDM B S hS B.contains_terminal V.toAlgebraicStack →
          V.property ≤ W''.property) ∧
      ∀ V : OpenSubstack 𝒳,
        AlgebraicStacks.IsAbsolutelyQuasiDM B S hS B.contains_terminal V.toAlgebraicStack →
          V.property ≤ W'.property

Tag 0DSN, a lemma

Tag 0DSN in the Stacks Project.

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

Stacks 0DSN, part (1). A field-valued point of an algebraic stack lies in its Deligne–Mumford locus exactly when its automorphism group algebraic space is unramified over its field.

The objects of 𝒳 whose automorphism group algebraic space is unramified form an open substack, AlgebraicGeometry.Stack.automorphismLocusSubstack, open because the unramified base locus of Stacks 0DSJ is, and Deligne–Mumford by the pseudo-torsor argument of Stacks 0CL0 through Stacks 0DSK; conversely an open substack is Deligne–Mumford only if the automorphism group algebraic spaces of its objects, which are those computed in 𝒳, are unramified.

theorem dmLocus_apply_iff_isUnramifiedAutomorphismGroupSpace
    (x : FieldValuedPoint B S hS 𝒳.val.val) :
    dmLocus B S hS hZ 𝒳 x.obj ↔ IsUnramifiedAutomorphismGroupSpace B S hS 𝒳 x

AlgebraicGeometry.Stack.quasiDMLocus_apply_iff_isLocallyQuasiFiniteAutomorphismGroupSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordLocusPoints.lean, line 499. The attribute's comment: “part (2)”.

Stacks 0DSN, part (2). A field-valued point of an algebraic stack lies in its quasi-Deligne–Mumford locus exactly when its automorphism group algebraic space is locally quasi-finite over its field. The source says the proof is the same as for part (1), and it is.

theorem quasiDMLocus_apply_iff_isLocallyQuasiFiniteAutomorphismGroupSpace
    (x : FieldValuedPoint B S hS 𝒳.val.val) :
    quasiDMLocus B S hS hZ 𝒳 x.obj ↔
      IsLocallyQuasiFiniteAutomorphismGroupSpace B S hS 𝒳 x

Sources

LeanAlgebraicGeometry.Stack.dmLocus · AlgebraicGeometry.Stack.quasiDMLocus · AlgebraicGeometry.Stack.le_dmLocus · AlgebraicGeometry.Stack.le_quasiDMLocus · AlgebraicGeometry.Stack.dmLocus_le_quasiDMLocus · AlgebraicGeometry.Stack.exists_largest_isAbsolutelyDM_openSubstack · AlgebraicGeometry.Stack.exists_largest_isAbsolutelyQuasiDM_openSubstack · AlgebraicGeometry.Stack.exists_nested_largest_isAbsolutelyDM_isAbsolutelyQuasiDM_openSubstack

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

101.7 Quasi-compact morphisms to 101.22 The Deligne-Mumford locus

Section101.7 Quasi-compact morphisms#

Tag 050T, a lemma

Tag 050U, a definition

Tag 050V, a lemma

Tag 050W, a lemma

Tag 0CL1, a lemma

Tag 050X, a lemma

Tag 050Y, a lemma

Tag 075S, a lemma

Tag 0CL2, a lemma

Tag 0DTL, a lemma

Sources

Section101.8 Noetherian algebraic stacks#

Tag 0510, a definition

Tag 0CPM, a lemma

Tag 0DQI, a lemma

Tag 0GVX, a lemma

Sources

Section101.9 Affine morphisms#

Tag 0CHQ, a definition

Tag 0CHR, a lemma

Tag 0CHS, a lemma

Tag 0GQE, a lemma

Sources

Section101.10 Integral and finite morphisms#

Tag 0CHU, a definition

Tag 0CHV, a lemma

Tag 0CHW, a lemma

Sources

Section101.11 Open morphisms#

Tag 06U1, a lemma

Tag 06U2, a definition

Tag 06U3, a lemma

Tag 06U4, a lemma

Sources

Section101.12 Submersive morphisms#

Tag 0CHX, a lemma

Tag 06U6, a definition

Tag 0CHY, a lemma

Tag 0CHZ, a lemma

Sources

Section101.13 Universally closed morphisms#

Tag 0512, a lemma

Tag 0513, a definition

Tag 0514, a lemma

Tag 0515, a lemma

Tag 0CL3, a lemma

Sources

Section101.14 Universally injective morphisms#

Tag 0CI1, a lemma

Tag 0CI2, a definition

Tag 0CI3, a lemma

Tag 0CI4, a lemma

Tag 0CPN, a lemma

Tag 0DTM, a lemma

Tag 0DTN, a lemma

Tag 0DTP, a lemma

Sources

Section101.15 Universal homeomorphisms#

Tag 0CI6, a lemma

Tag 0CI7, a definition

Tag 0CI8, a lemma

Tag 0CI9, a lemma

Tag 0DTQ, a lemma

Sources

Section101.16 Types of morphisms smooth local on source-and-target#

Tag 06FM, a lemma

Tag 06FN, a definition

Tag 06FP, a remark

Tag 06FQ, a remark

Tag 06PS, a remark

Sources

Section101.17 Morphisms of finite type#

Tag 06FS, a definition

Tag 06FT, a lemma

Tag 06FU, a lemma

Tag 06FV, a lemma

Tag 06R6, a lemma

Tag 06U7, a lemma

Section101.7 Quasi-compact morphisms #

Section101.8 Noetherian algebraic stacks #

Section101.9 Affine morphisms #

Section101.10 Integral and finite morphisms #

Section101.11 Open morphisms #

Section101.12 Submersive morphisms #

Section101.13 Universally closed morphisms #

Section101.14 Universally injective morphisms #

Section101.15 Universal homeomorphisms #

Section101.16 Types of morphisms smooth local on source-and-target #

Section101.17 Morphisms of finite type #

Section101.18 Points of finite type #

Section101.19 Automorphism groups #

Section101.20 Presentations and properties of algebraic stacks #

Section101.21 Special presentations of algebraic stacks #

Section101.22 The Deligne-Mumford locus #