101.38 Scheme theoretic image to 101.51 Residual gerbes

Section101.38 Scheme theoretic image#

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

Tag 0CMI, a definition

Tag 0CMI in the Stacks Project.

AlgebraicGeometry.Stack.IsSchemeTheoreticImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImage.lean, line 155. References: EGA I (9.5.3).

Stacks 0CMI. A property of the objects of 𝒴 is the scheme theoretic image of a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S when it cuts out a closed substack of 𝒴 through which f factors, and is contained in every closed substack of 𝒴 through which f factors.

def IsSchemeTheoreticImage {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (P : ObjectProperty 𝒴.val.val.obj) : Prop
Tag 0CMJ, a lemma

Tag 0CMJ in the Stacks Project.

AlgebraicGeometry.Stack.hasSchemeTheoreticImage_comp_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImage.lean, line 250. The attribute's comment: “existence_iff”.

Stacks 0CMJ, the existence assertion. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒲 ⟶ 𝒳 be a surjective, flat 1-morphism locally of finite presentation. Then the scheme theoretic image of f exists if and only if the scheme theoretic image of g ≫ f exists.

theorem hasSchemeTheoreticImage_comp_iff {𝒲 𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒲 ⟶ 𝒳)
    (hsurj : IsSurjective B S hS g)
    (hflat : AlgebraicStacks.IsFlat B S hS g)
    (hlfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g) :
    HasSchemeTheoreticImage f ↔ HasSchemeTheoreticImage (g ≫ f)

AlgebraicGeometry.Stack.eq_of_isSchemeTheoreticImage_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImage.lean, line 264. The attribute's comment: “images_equal”.

Stacks 0CMJ, the agreement of the two images. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒲 ⟶ 𝒳 be a surjective, flat 1-morphism locally of finite presentation. If P is the scheme theoretic image of f and Q is the scheme theoretic image of g ≫ f, then P = Q.

theorem eq_of_isSchemeTheoreticImage_comp {𝒲 𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒲 ⟶ 𝒳)
    (hsurj : IsSurjective B S hS g)
    (hflat : AlgebraicStacks.IsFlat B S hS g)
    (hlfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    {P Q : ObjectProperty 𝒴.val.val.obj} (hP : IsSchemeTheoreticImage f P)
    (hQ : IsSchemeTheoreticImage (g ≫ f) Q) : P = Q
Tag 0CPU, a lemma

Tag 0CPU in the Stacks Project.

AlgebraicGeometry.Stack.schemeTheoreticImageCandidate_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImageExistence.lean, line 94. The attribute's comment: “minimality of the candidate image”.

Minimality of the candidate image: the intersection of the closed substacks through which f factors is contained in each of them.

theorem schemeTheoreticImageCandidate_le {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    {Q : ObjectProperty 𝒴.val.val.obj} (hQ : IsClosedSubstack 𝒴 Q)
    (hfac : FactorsThroughSubstack f Q) : schemeTheoreticImageCandidate f ≤ Q

AlgebraicGeometry.Stack.factorsThroughSubstack_schemeTheoreticImageCandidate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImageExistence.lean, line 144. The attribute's comment: “the candidate image factors f”.

The factorization through the candidate image: f factors through the intersection of the closed substacks of 𝒴 through which it factors, because factoring through a strictly full subcategory is a condition on the objects in the image of f.

theorem factorsThroughSubstack_schemeTheoreticImageCandidate
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    FactorsThroughSubstack f (schemeTheoreticImageCandidate f)

AlgebraicGeometry.Stack.hasSchemeTheoreticImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImageExistence.lean, line 201.

Stacks 0CPU. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. Then the scheme theoretic image of f exists: there is a smallest closed substack of 𝒴 through which f factors, namely AlgebraicGeometry.Stack.schemeTheoreticImageCandidate f.

theorem hasSchemeTheoreticImage {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    HasSchemeTheoreticImage f
Tag 0CPV, a lemma

Tag 0CPV in the Stacks Project.

AlgebraicGeometry.Stack.le_inverseImage_of_isSchemeTheoreticImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImage.lean, line 570. The attribute's comment: “containment”.

Stacks 0CPV, the containment that induces the morphism. Let a commutative square of algebraic stacks over S be given, with horizontal 1-morphisms f₁ : 𝒳₁ ⟶ 𝒴₁, f₂ : 𝒳₂ ⟶ 𝒴₂ and vertical ones a : 𝒳₁ ⟶ 𝒳₂, b : 𝒴₁ ⟶ 𝒴₂, and let Pᵢ be the scheme theoretic image of fᵢ. Then P₁ is contained in the preimage of P₂ under b.

The preimage of P₂ cuts out a closed substack of 𝒴₁ (AlgebraicGeometry.Stack.isClosedSubstack_inverseImage) through which f₁ factors (AlgebraicGeometry.Stack.factorsThroughSubstack_inverseImage), so the minimality of the scheme theoretic image applies to it.

theorem le_inverseImage_of_isSchemeTheoreticImage {f₁ : 𝒳₁ ⟶ 𝒴₁} {f₂ : 𝒳₂ ⟶ 𝒴₂} {a : 𝒳₁ ⟶ 𝒳₂}
    {b : 𝒴₁ ⟶ 𝒴₂} (sq : f₁ ≫ b ≅ a ≫ f₂) {P₁ : ObjectProperty 𝒴₁.val.val.obj}
    {P₂ : ObjectProperty 𝒴₂.val.val.obj} (h₁ : IsSchemeTheoreticImage f₁ P₁)
    (h₂ : IsSchemeTheoreticImage f₂ P₂) :
    P₁ ≤ P₂.inverseImage b.hom.hom.toFunctor

AlgebraicGeometry.Stack.schemeTheoreticImageMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImage.lean, line 583. The attribute's comment: “induced_morphism”.

Stacks 0CPV, the induced 1-morphism. The 1-morphism b : 𝒴₁ ⟶ 𝒴₂ of a commutative square of algebraic stacks carries the scheme theoretic image of f₁ into the scheme theoretic image of f₂, and therefore induces a 1-morphism 𝒵₁ ⟶ 𝒵₂ between them.

def schemeTheoreticImageMap {f₁ : 𝒳₁ ⟶ 𝒴₁} {f₂ : 𝒳₂ ⟶ 𝒴₂} {a : 𝒳₁ ⟶ 𝒳₂} {b : 𝒴₁ ⟶ 𝒴₂}
    (sq : f₁ ≫ b ≅ a ≫ f₂) {P₁ : ObjectProperty 𝒴₁.val.val.obj}
    {P₂ : ObjectProperty 𝒴₂.val.val.obj} (h₁ : IsSchemeTheoreticImage f₁ P₁)
    (h₂ : IsSchemeTheoreticImage f₂ P₂) :
    fullSubcategoryAlgebraicStack 𝒴₁ P₁ h₁.isAlgebraicStack ⟶
      fullSubcategoryAlgebraicStack 𝒴₂ P₂ h₂.isAlgebraicStack

AlgebraicGeometry.Stack.schemeTheoreticImageMap_comp_inclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImage.lean, line 595. The attribute's comment: “inclusion_square”.

Stacks 0CPV, the right-hand square of the induced diagram: the induced 1-morphism 𝒵₁ ⟶ 𝒵₂ composed with the inclusion 𝒵₂ ⟶ 𝒴₂ is the inclusion 𝒵₁ ⟶ 𝒴₁ followed by b.

theorem schemeTheoreticImageMap_comp_inclusion {f₁ : 𝒳₁ ⟶ 𝒴₁} {f₂ : 𝒳₂ ⟶ 𝒴₂} {a : 𝒳₁ ⟶ 𝒳₂}
    {b : 𝒴₁ ⟶ 𝒴₂} (sq : f₁ ≫ b ≅ a ≫ f₂) {P₁ : ObjectProperty 𝒴₁.val.val.obj}
    {P₂ : ObjectProperty 𝒴₂.val.val.obj} (h₁ : IsSchemeTheoreticImage f₁ P₁)
    (h₂ : IsSchemeTheoreticImage f₂ P₂) :
    schemeTheoreticImageMap sq h₁ h₂ ≫ fullSubcategoryInclusion 𝒴₂ P₂ h₂.isAlgebraicStack =
      fullSubcategoryInclusion 𝒴₁ P₁ h₁.isAlgebraicStack ≫ b

AlgebraicGeometry.Stack.schemeTheoreticImageMapFactorizationSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImage.lean, line 611. The attribute's comment: “factorization_square”.

Stacks 0CPV, the left-hand square of the induced diagram. Let kᵢ : 𝒳ᵢ ⟶ 𝒵ᵢ be factorizations of fᵢ through the scheme theoretic images. Then the induced 1-morphism 𝒵₁ ⟶ 𝒵₂ makes the square with a : 𝒳₁ ⟶ 𝒳₂ 2-commute.

Both composites 𝒳₁ ⟶ 𝒵₂ ⟶ 𝒴₂ are 2-isomorphic, by the given square and the two factorizations, and the inclusion of 𝒵₂ is fully faithful, so the 2-isomorphism descends to 𝒵₂.

noncomputable def schemeTheoreticImageMapFactorizationSquare {f₁ : 𝒳₁ ⟶ 𝒴₁} {f₂ : 𝒳₂ ⟶ 𝒴₂}
    {a : 𝒳₁ ⟶ 𝒳₂} {b : 𝒴₁ ⟶ 𝒴₂} (sq : f₁ ≫ b ≅ a ≫ f₂)
    {P₁ : ObjectProperty 𝒴₁.val.val.obj} {P₂ : ObjectProperty 𝒴₂.val.val.obj}
    (h₁ : IsSchemeTheoreticImage f₁ P₁) (h₂ : IsSchemeTheoreticImage f₂ P₂)
    (k₁ : 𝒳₁ ⟶ fullSubcategoryAlgebraicStack 𝒴₁ P₁ h₁.isAlgebraicStack)
    (k₂ : 𝒳₂ ⟶ fullSubcategoryAlgebraicStack 𝒴₂ P₂ h₂.isAlgebraicStack)
    (e₁ : k₁ ≫ fullSubcategoryInclusion 𝒴₁ P₁ h₁.isAlgebraicStack ≅ f₁)
    (e₂ : k₂ ≫ fullSubcategoryInclusion 𝒴₂ P₂ h₂.isAlgebraicStack ≅ f₂) :
    k₁ ≫ schemeTheoreticImageMap sq h₁ h₂ ≅ a ≫ k₂
Tag 0CMK, a lemma

Tag 0CMK in the Stacks Project.

AlgebraicGeometry.Stack.schemeTheoreticImageCandidate_le_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImageFlatBaseChange.lean, line 150. The attribute's comment: “containment”.

The easy containment of Stacks 0CMK, for any 2-commutative square. Let f : 𝒳 ⟶ 𝒴 and b : 𝒴' ⟶ 𝒴 be 1-morphisms of algebraic stacks over S and let sq be a 2-commutative square over them, with apex sq.pt and legs sq.fst : sq.pt ⟶ 𝒴' and sq.snd : sq.pt ⟶ 𝒳. Then the intersection of the closed substacks of 𝒴' through which sq.fst factors is contained in the preimage under b of the intersection of the closed substacks of 𝒴 through which f factors.

Let Q be a closed substack of 𝒴 through which f factors. Its preimage under b is a closed substack of 𝒴' (AlgebraicGeometry.Stack.isClosedSubstack_inverseImage) through which sq.fst factors (AlgebraicGeometry.Stack.factorsThroughSubstack_inverseImage, which is where the 2-commutativity of the square is used), so the candidate image of sq.fst is contained in it by its own minimality. As Q ranges over the closed substacks of 𝒴 through which f factors this says exactly that an object of the candidate image of sq.fst has its image under b in the candidate image of f.

public theorem schemeTheoreticImageCandidate_le_inverseImage (f : 𝒳 ⟶ 𝒴) (b : 𝒴' ⟶ 𝒴)
    (sq : Bicategory.TwoCommSq b f) :
    schemeTheoreticImageCandidate sq.fst ≤
      (schemeTheoreticImageCandidate f).inverseImage b.hom.hom.toFunctor

AlgebraicGeometry.Stack.schemeTheoreticImageCandidate_inverseImage_fullSubcategoryInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImageFlatBaseChange.lean, line 174. The attribute's comment: “closed_substack_case”.

Stacks 0CMK for the inclusion of a closed substack. Let P cut out a closed substack of 𝒴₂ and let b : 𝒴₁ ⟶ 𝒴₂ be any 1-morphism of algebraic stacks over S. The base change of the inclusion of that substack along b is the inclusion of the preimage of P, by AlgebraicGeometry.Stack.inverseImageSquare_fst, and the square realising it is a 2-fibre product by AlgebraicGeometry.Stack.isTwoFibreProduct_inverseImageSquare. Then the scheme theoretic image of that base change is the preimage under b of the scheme theoretic image of the inclusion.

Both sides are computed by AlgebraicGeometry.Stack.schemeTheoreticImageCandidate_fullSubcategoryInclusion: a closed substack is the scheme theoretic image of its own inclusion, and the preimage of a closed substack is a closed substack. Neither flatness of b nor quasi-compactness of the inclusion is used.

public theorem schemeTheoreticImageCandidate_inverseImage_fullSubcategoryInclusion
    {𝒴₁ 𝒴₂ : AlgebraicStacks.{u, w} B S hS} (b : 𝒴₁ ⟶ 𝒴₂)
    {P : ObjectProperty 𝒴₂.val.val.obj} [P.IsClosedUnderIsomorphisms]
    (hP : IsClosedSubstack 𝒴₂ P)
    (hPalg : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒴₂ P)) :
    schemeTheoreticImageCandidate (inverseImageSquare b P hPalg).fst =
      (schemeTheoreticImageCandidate (fullSubcategoryInclusion 𝒴₂ P hPalg)).inverseImage
        b.hom.hom.toFunctor

AlgebraicGeometry.Stack.isSchemeTheoreticImage_inverseImage_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImageFlatBaseChange.lean, line 777. References: EGA IV (2.3.2), “more general”.

Stacks 0CMK. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact 1-morphism of algebraic stacks over S and let b : 𝒴' ⟶ 𝒴 be a flat 1-morphism. Then formation of the scheme theoretic image commutes with the base change along b: if P is the scheme theoretic image of f, then its inverse image under b is the scheme theoretic image of the base change f' : 𝒳 ×_𝒴 𝒴' ⟶ 𝒴' (the first projection of the canonical 2-fibre product square).

The containment of the image of f' in the inverse image of P holds for any square (AlgebraicGeometry.Stack.schemeTheoreticImageCandidate_le_inverseImage). For the converse, the flat-local image of f — the closed substack of 𝒴 cut out by the scheme theoretic images of the base changes of f to the smooth affine charts of 𝒴, which descend by the invariance of the proof of Stacks 0CMK (AlgebraicGeometry.Stack.chartImageSubfunctor_le_chartSubfunctor_flatLocalImage) — is a closed substack through which f factors, so it contains P, and its inverse image under b lies in the image of f' (AlgebraicGeometry.Stack.inverseImage_flatLocalImage_le).

theorem isSchemeTheoreticImage_inverseImage_of_isFlat (f : 𝒳 ⟶ 𝒴) (b : 𝒴' ⟶ 𝒴)
    (hf : IsQuasiCompactMorphism B S hS f) (hb : AlgebraicStacks.IsFlat B S hS b)
    {P : ObjectProperty 𝒴.val.val.obj} (hP : IsSchemeTheoreticImage f P) :
    IsSchemeTheoreticImage (twoFibreProductSquareAlgebraicStacks B S hS b f).fst
      (P.inverseImage b.hom.hom.toFunctor)
Tag 0CML, a lemma

Tag 0CML in the Stacks Project.

AlgebraicGeometry.Stack.range_pointsMap_eq_closure_of_isSchemeTheoreticImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImagePointsClosure.lean, line 129.

Stacks 0CML. Let f : 𝒳 ⟶ 𝒴 be a quasi-compact 1-morphism of algebraic stacks over S and let P cut out its scheme theoretic image 𝒵 ⊆ 𝒴 (Stacks 0CMI). Then the points of 𝒵 are the closure in |𝒴| of the image of |f|.

The closure lies in |𝒵| for any f: f factors through 𝒵, whose points are closed by Stacks 0H20. Conversely, let z be a point of 𝒵, and choose a smooth chart v : (Sch/V)_fppf ⟶ 𝒴 with V affine through its image, and a point η of V over it. The point (z, η) lifts to 𝒵 ×_𝒴 V (Stacks 04XH), so η comes from a field-valued point t : Spec K ⟶ V at which P holds. As f is quasi-compact, 𝒳 ×_𝒴 V is quasi-compact and has a smooth surjective presentation by an affine A, with composite g : A ⟶ V. The scheme theoretic image of f lies in the closed substack cut out by the scheme theoretic images of the base changes of f to the smooth affine charts (the descent of the proof of Stacks 0CMK), and that image along v lies in the scheme theoretic image of g (Stacks 0CMJ, in the form of Stacks 06QA). So t factors through the scheme theoretic image of the quasi-compact g, and η lies in the closure of the image of g (Stacks 082Z, read on schemes). The map |V| ⟶ |𝒴| is continuous and carries the image of g into the image of |f|, the square A ⟶ 𝒳 ×_𝒴 V commuting, so it carries η into the closure of the image of |f|.

theorem range_pointsMap_eq_closure_of_isSchemeTheoreticImage
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (hf : IsQuasiCompactMorphism B S hS f)
    {P : ObjectProperty 𝒴.val.val.obj} (hP : IsSchemeTheoreticImage f P) :
    Set.range (AlgebraicStacks.pointsMap B S hS
        (fullSubcategoryInclusion 𝒴 P hP.isAlgebraicStack)) =
      @closure _ (pointTopology B S hS 𝒴.val)
        (Set.range (AlgebraicStacks.pointsMap B S hS f))
Tag 0CPW, a lemma

Tag 0CPW in the Stacks Project.

AlgebraicGeometry.Stack.isEquivalence_fst_of_isSchemeTheoreticImage_partialSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeTheoreticImagePartialSection.lean, line 369.

Stacks 0CPW. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S which is representable by algebraic spaces and separated, let 𝒱 ⊆ 𝒴 be an open substack such that 𝒱 ⟶ 𝒴 is quasi-compact, and let s : 𝒱 ⟶ 𝒳 be a 1-morphism with f ∘ s ≅ id_𝒱, i.e. with a 2-isomorphism s ≫ f ≅ (𝒱 ⟶ 𝒴). Let P cut out the scheme theoretic image 𝒴' of s (Stacks 0CMI). Then 𝒴' ⟶ 𝒴 is an isomorphism over 𝒱: the projection 𝒴' ×_𝒴 𝒱 ⟶ 𝒱 is an equivalence of categories.

s is quasi-compact by Stacks 050Y, as s ≫ f is 2-isomorphic to the quasi-compact 𝒱 ⟶ 𝒴 and f is quasi-separated. The projection has a section, so it is essentially surjective (AlgebraicGeometry.Stack.essSurj_fst_partialSectionImageSquare). It is faithful because f is, being representable by algebraic spaces. It is full because every object of 𝒴' ×_𝒴 𝒱, read in 𝒱 ×_𝒴 𝒳, is isomorphic to the image of an object of 𝒱 under the graph of s (AlgebraicGeometry.Stack.exists_iso_partialSectionGraph_obj, which is where Stacks 0CMK and the separatedness of f enter), and the graph is a section of the projection to 𝒱.

theorem isEquivalence_fst_of_isSchemeTheoreticImage_partialSection
    (hrep : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hf : AlgebraicStacks.IsSeparated B S hS f)
    (hVqc : IsQuasiCompactMorphism B S hS ι[V]) (hsec : s ≫ f ≅ ι[V])
    {P : ObjectProperty 𝒳.val.val.obj} (hP : IsSchemeTheoreticImage s P) :
    Functor.IsEquivalence (twoFibreProductSquareAlgebraicStacks B S hS ι[V]
      (fullSubcategoryInclusion 𝒳 P hP.isAlgebraicStack ≫ f)).fst.hom.hom.toFunctor
Sources
LeanAlgebraicGeometry.Stack.IsSchemeTheoreticImage · AlgebraicGeometry.Stack.hasSchemeTheoreticImage_comp_iff · AlgebraicGeometry.Stack.eq_of_isSchemeTheoreticImage_comp · AlgebraicGeometry.Stack.schemeTheoreticImageCandidate_le · AlgebraicGeometry.Stack.factorsThroughSubstack_schemeTheoreticImageCandidate · AlgebraicGeometry.Stack.hasSchemeTheoreticImage · AlgebraicGeometry.Stack.le_inverseImage_of_isSchemeTheoreticImage · AlgebraicGeometry.Stack.schemeTheoreticImageMap

Section101.39 Valuative criteria#

Section 101.39 of the Stacks Project, Tag 0CL9. 14 tags here are carried by 17 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CLA, a definition

Tag 0CLA in the Stacks Project.

Declarations registered for the tag:

Tag 0CLC, a lemma

Tag 0CLC in the Stacks Project.

AlgebraicGeometry.Stack.isSetoidCategory_dottedArrow_of_isSeparated_relativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionDottedGroupoid.lean, line 318. The attribute's comment: “setoid”.

Stacks 0CLC, the setoid assertion. If the relative diagonal Δ_f of a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is separated in the sense of Stacks 04XB, then the category of dotted arrows of every valuative diagram for f is a setoid.

The category is a groupoid because the 2-category of categories fibred in groupoids is locally groupoidal, so only the triviality of automorphisms is at issue. The two compatibility conditions on an automorphism θ of a dotted arrow say that θ lies in the relative inertia of f and is trivial at the generic point; separatedness of Δ_f makes the neutral section of the relative inertia a closed immersion, and AlgebraicGeometry.Stack.eq_id_of_isClosedImmersion_relativeInertiaNeutralSection concludes, the spectrum of a valuation ring being reduced and its generic point dominant.

theorem isSetoidCategory_dottedArrow_of_isSeparated_relativeDiagonal (f : 𝒳 ⟶ 𝒴)
    (hf : IsSeparated B S hS (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom))
    (D : ValuativeDiagram B S hS 𝒳 𝒴 f) :
    IsSetoidCategory (CategoryTheory.DottedArrow D.x D.j f.hom D.y D.γ)

Declarations registered for the tag:

Tag 0CLD, a lemma

Tag 0CLD in the Stacks Project.

AlgebraicGeometry.Stack.nonempty_dottedArrow_equivalence_of_forall_exists_whiskerLeft, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionUniqueness.lean, line 175. The attribute's comment: “1 of 2: independence of the witness”.

When the inertia I_𝒴 ⟶ 𝒴 is proper, the category of dotted arrows of a valuative diagram is independent, up to a noncanonical equivalence, of the 2-morphism witnessing the 2-commutativity.

theorem nonempty_dottedArrow_equivalence_of_forall_exists_whiskerLeft
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hI : IsProper B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒴).hom)
    (D : ValuativeDiagram B S hS 𝒳 𝒴 f)
    (γ γ' : (D.j ≫ D.y) ⟶ (D.x ≫ f.hom)) :
    Nonempty (CategoryTheory.DottedArrow D.x D.j f.hom D.y γ ≌
      CategoryTheory.DottedArrow D.x D.j f.hom D.y γ')

AlgebraicGeometry.Stack.nonempty_dottedArrow_iff_exists_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionUniqueness.lean, line 191. The attribute's comment: “2 of 2: existence for some and hence every witness”.

When the inertia I_𝒴 ⟶ 𝒴 is proper, a dotted arrow of a valuative diagram exists — for one and hence for every witnessing 2-morphism — exactly when there is a diagonal 1-morphism a : Spec R ⟶ 𝒳 with 2-morphisms a ∘ j ⟶ x and y ⟶ f ∘ a, with no condition relating them to the witness.

theorem nonempty_dottedArrow_iff_exists_diagonal
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hI : IsProper B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒴).hom)
    (D : ValuativeDiagram B S hS 𝒳 𝒴 f)
    (γ : (D.j ≫ D.y) ⟶ (D.x ≫ f.hom)) :
    Nonempty (CategoryTheory.DottedArrow D.x D.j f.hom D.y γ) ↔
      ∃ a : schemeFibredCategory B S hS D.whole ⟶ 𝒳.1,
        Nonempty ((D.j ≫ a) ⟶ D.x) ∧ Nonempty (D.y ⟶ (a ≫ f.hom))
Tag 0CLE, a lemma

Tag 0CLE in the Stacks Project.

CategoryTheory.DottedArrowBaseChange.dottedArrows_baseChange_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Exercises/NonExercises/DottedArrowsBaseChange.lean, line 306.

Stacks 0CLE. The category of dotted arrows is invariant under base change along a \(2\)-cartesian square.

Split a \(2\)-commutative rectangle into a left square, filled by γ', and a right square, filled by φ and assumed \(2\)-cartesian. Then the category of dotted arrows of the left square is equivalent to the category of dotted arrows of the outer rectangle, whose filler is the pasting of γ' and φ.

theorem dottedArrows_baseChange_equivalence
    {S T X X' Y Y' : B}
    (j : S ⟶ T) (x' : S ⟶ X') (q : X' ⟶ X) (p : X' ⟶ Y')
    (f : X ⟶ Y) (y' : T ⟶ Y') (g : Y' ⟶ Y)
    (φ : (p ≫ g) ≅ (q ≫ f)) (γ' : (j ≫ y') ≅ (x' ≫ p))
    (hcart : IsTwoCartesian q p f g φ) :
    Nonempty (CategoryTheory.DottedArrow x' j p y' γ'.hom ≌
      CategoryTheory.DottedArrow (x' ≫ q) j f (y' ≫ g)
          ((α_ j y' g).symm ≪≫ whiskerRightIso γ' g ≪≫ (α_ x' p g) ≪≫
            whiskerLeftIso x' φ ≪≫ (α_ x' q f).symm).hom)
Tag 0CLF, a lemma

Tag 0CLF in the Stacks Project.

CategoryTheory.DottedArrow.toWithFactorization_isEquivalence, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DottedArrows/Composition.lean, line 400.

toWithFactorization is an equivalence of categories 𝒟 ≌ 𝒟''.

instance toWithFactorization_isEquivalence {S T X Y Z : B} (x : S ⟶ X) (j : S ⟶ T) (f : X ⟶ Y)
    (g : Y ⟶ Z) (z : T ⟶ Z) (γ : (j ≫ z) ⟶ (x ≫ f ≫ g)) :
    (toWithFactorization x j f g z γ).IsEquivalence

CategoryTheory.DottedArrow.fiber_categoryIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DottedArrows/Composition.lean, line 624.

The fibre of compose over an object d' of 𝒟' is isomorphic, as a category (a CategoryIso, not merely an equivalence), to the category of dotted arrows of the upper solid square, whose bottom arrow is d'.a and whose witness is d'.α.

theorem fiber_categoryIso {S T X Y Z : B}
    (x : S ⟶ X) (j : S ⟶ T) (f : X ⟶ Y) (g : Y ⟶ Z) (z : T ⟶ Z)
    (γ : (j ≫ z) ⟶ (x ≫ f ≫ g))
    (d' : DottedArrow (x ≫ f) j g z (γ ≫ (α_ x f g).inv)) :
    Nonempty (CategoryIso ((compose x j f g z γ).Fiber d')
      (DottedArrow x j f d'.a d'.α))

CategoryTheory.DottedArrow.compose_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DottedArrows/Composition.lean, line 778.

compose : 𝒟'' ⥤ 𝒟' is fibred in groupoids.

theorem compose_isFiberedInGroupoids {S T X Y Z : B} (x : S ⟶ X) (j : S ⟶ T) (f : X ⟶ Y)
    (g : Y ⟶ Z) (z : T ⟶ Z) (γ : (j ≫ z) ⟶ (x ≫ f ≫ g)) :
    (compose x j f g z γ).IsFiberedInGroupoids

Declarations registered for the tag:

Tag 0CLG, a definition

Tag 0CLG in the Stacks Project.

AlgebraicGeometry.Stack.ValuativeCriterion.Uniqueness, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionUniqueness.lean, line 97.

A 1-morphism of algebraic stacks satisfies the uniqueness part of the valuative criterion when, for every valuative diagram for it, the category of dotted arrows is either empty or a setoid with exactly one isomorphism class.

abbrev Uniqueness
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop
Tag 0CLH, a lemma

Tag 0CLH in the Stacks Project.

AlgebraicGeometry.Stack.valuativeCriterionUniqueness_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionBaseChange.lean, line 198.

Stacks 0CLH. A base change of a 1-morphism of algebraic stacks satisfying the uniqueness part of the valuative criterion satisfies it as well.

The base change of f : 𝒳 ⟶ 𝒴 along g : 𝒴' ⟶ 𝒴 is the first projection of a 2-fibre product P of the cospan (g, f).

theorem valuativeCriterionUniqueness_baseChange
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hf : ValuativeCriterion.Uniqueness B S hS f) :
    ValuativeCriterion.Uniqueness B S hS P.fst
Tag 0CLI, a lemma

Tag 0CLI in the Stacks Project.

AlgebraicGeometry.Stack.valuativeCriterionUniqueness_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionUniqueness.lean, line 111.

The composition of two 1-morphisms of algebraic stacks satisfying the uniqueness part of the valuative criterion satisfies it as well.

theorem valuativeCriterionUniqueness_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : ValuativeCriterion.Uniqueness B S hS f)
    (hg : ValuativeCriterion.Uniqueness B S hS g) :
    ValuativeCriterion.Uniqueness B S hS (f ≫ g)
Tag 0CLJ, a lemma

Tag 0CLJ in the Stacks Project.

AlgebraicGeometry.Stack.valuativeCriterionUniqueness_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionUniquenessPoints.lean, line 522.

Stacks 0CLJ. For a 1-morphism of algebraic stacks representable by algebraic spaces, the uniqueness part of the valuative criterion holds exactly when it holds for every base change to an algebraic space along a scheme-valued point of the target.

The base change is described exactly as in Stacks 02ZW: for an object U of the site and a scheme-valued point y of 𝒴 over U, it is the first projection of the 2-fibre product U ×_𝒴 𝒳, and the condition is imposed on the structure morphism of any algebraic space F over U equivalent to it over the site of U. Quantifying over all such F rather than over a chosen one spares a consumer the transport along a comparison equivalence.

theorem valuativeCriterionUniqueness_iff_baseChange
    (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) :
    ValuativeCriterion.Uniqueness B S hS f ↔
      ∀ U : BigFppfOver B S hS,
        let 𝒰 := BigFppfOver B U.left.1 U.left.2
        let p𝒰 : 𝒰 ⥤ BigFppfOver B S hS := Over.map U.hom
        ∀ (y : 𝒰 ⥤ 𝒴.val.val.obj) (_hy : y ⋙ 𝒴.val.val.p = p𝒰) (F : 𝒰ᵒᵖ ⥤ Type u)
          (_hF : IsAlgebraicSpace B U.left.1 U.left.2 F)
          (_e : StacksRepresentableCFG.EquivalenceOver
            (TwoFibreProductOver.fst p𝒰 𝒳.val.val.p 𝒴.val.val.p y f.hom.hom.toFunctor)
            (presheafOfCategories (F ⋙ typeToCat)).p)
          (p : F ⟶ yoneda.obj (Over.mk (𝟙 (B.obj U.left.2)))),
          Space.ValuativeCriterion.Uniqueness p
Tag 0CLK, a definition

Tag 0CLK in the Stacks Project.

AlgebraicGeometry.Stack.ValuativeCriterion.Existence, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterion.lean, line 420.

A 1-morphism of algebraic stacks satisfies the existence part of the valuative criterion when every valuative square for it admits a dotted arrow after an extension of the fraction field and passage to a dominating valuation ring.

abbrev Existence (f : 𝒳 ⟶ 𝒴) : Prop
Tag 0CLL, a lemma

Tag 0CLL in the Stacks Project.

AlgebraicGeometry.Stack.valuativeCriterionExistence_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionBaseChange.lean, line 244.

Stacks 0CLL. A base change of a 1-morphism of algebraic stacks satisfying the existence part of the valuative criterion satisfies it as well.

The base change of f : 𝒳 ⟶ 𝒴 along g : 𝒴' ⟶ 𝒴 is the first projection of a 2-fibre product P of the cospan (g, f).

theorem valuativeCriterionExistence_baseChange
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hf : ValuativeCriterion.Existence B S hS f) :
    ValuativeCriterion.Existence B S hS P.fst
Tag 0CLM, a lemma

Tag 0CLM in the Stacks Project.

AlgebraicGeometry.Stack.valuativeCriterionExistence_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterion.lean, line 497.

The composition of two 1-morphisms of algebraic stacks satisfying the existence part of the valuative criterion satisfies it as well.

theorem valuativeCriterionExistence_comp
    {𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : ValuativeCriterion.Existence B S hS f)
    (hg : ValuativeCriterion.Existence B S hS g) :
    ValuativeCriterion.Existence B S hS (f ≫ g)
Tag 0CLN, a lemma

Tag 0CLN in the Stacks Project.

AlgebraicGeometry.Stack.valuativeCriterionExistence_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionExistencePoints.lean, line 730.

Stacks 0CLN. For a 1-morphism of algebraic stacks representable by algebraic spaces, the existence part of the valuative criterion holds exactly when it holds for every base change to an algebraic space along a scheme-valued point of the target.

The base change is described exactly as in Stacks 02ZW: for an object U of the site and a scheme-valued point y of 𝒴 over U, it is the first projection of the 2-fibre product U ×_𝒴 𝒳, and the condition is imposed on the structure morphism of any algebraic space F over U equivalent to it over the site of U. Quantifying over all such F rather than over a chosen one spares a consumer the transport along a comparison equivalence.

theorem valuativeCriterionExistence_iff_baseChange (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) :
    ValuativeCriterion.Existence B S hS f ↔
      ∀ U : BigFppfOver B S hS,
        let 𝒰 := BigFppfOver B U.left.1 U.left.2
        let p𝒰 : 𝒰 ⥤ BigFppfOver B S hS := Over.map U.hom
        ∀ (y : 𝒰 ⥤ 𝒴.val.val.obj) (_hy : y ⋙ 𝒴.val.val.p = p𝒰) (F : 𝒰ᵒᵖ ⥤ Type u)
          (_hF : IsAlgebraicSpace B U.left.1 U.left.2 F)
          (_e : StacksRepresentableCFG.EquivalenceOver
            (TwoFibreProductOver.fst p𝒰 𝒳.val.val.p 𝒴.val.val.p y f.hom.hom.toFunctor)
            (presheafOfCategories (F ⋙ typeToCat)).p)
          (p : F ⟶ yoneda.obj (Over.mk (𝟙 (B.obj U.left.2)))),
          Space.ValuativeCriterion.Existence p
Tag 0CLP, a lemma

Tag 0CLP in the Stacks Project.

AlgebraicGeometry.Stack.valuativeCriterionUniqueness_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionClosedImmersion.lean, line 135. The attribute's comment: “uniqueness”.

Stacks 0CLP, the uniqueness part. A closed immersion of algebraic stacks over S satisfies the uniqueness part of the valuative criterion (Stacks 0CLG).

By Stacks 0CLJ it is enough that every presheaf representing a base change of f along a scheme-valued point of 𝒴 have structural morphism satisfying the uniqueness criterion for presheaves; those presheaves have at most one section over every object by AlgebraicGeometry.Stack.subsingleton_baseChange_of_isClosedImmersion, so every morphism out of them is a monomorphism.

theorem valuativeCriterionUniqueness_of_isClosedImmersion (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsClosedImmersion B S hS f) :
    ValuativeCriterion.Uniqueness B S hS f

AlgebraicGeometry.Stack.valuativeCriterionExistence_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionClosedImmersion.lean, line 160. The attribute's comment: “existence”.

Stacks 0CLP, the existence part. A closed immersion of algebraic stacks over S satisfies the existence part of the valuative criterion (Stacks 0CLK).

By Stacks 0CLN it is enough that every presheaf representing a base change of f along a scheme-valued point of 𝒴 have structural morphism satisfying the existence criterion for presheaves. The closed immersion condition of Stacks 04YL is a condition on the structural morphism of the lower-shriek extension of that presheaf, and AlgebraicGeometry.Space.valuativeCriterionExistence_of_isClosedImmersion_relocalizeToYoneda turns it into the existence criterion for every morphism from the presheaf to the terminal presheaf on the site of the point — which is the shape Stacks 0CLN asks for.

theorem valuativeCriterionExistence_of_isClosedImmersion (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsClosedImmersion B S hS f) :
    ValuativeCriterion.Existence B S hS f
Sources
LeanCategoryTheory.DottedArrow · CategoryTheory.DottedArrow.Hom · AlgebraicGeometry.Stack.isSetoidCategory_dottedArrow_of_isSeparated_relativeDiagonal · CategoryTheory.instGroupoidDottedArrow · AlgebraicGeometry.Stack.nonempty_dottedArrow_equivalence_of_forall_exists_whiskerLeft · AlgebraicGeometry.Stack.nonempty_dottedArrow_iff_exists_diagonal · CategoryTheory.DottedArrowBaseChange.dottedArrows_baseChange_equivalence · CategoryTheory.DottedArrow.toWithFactorization_isEquivalence

Section101.40 Valuative criterion for second diagonal#

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

Tag 0CLR, a lemma

Tag 0CLR in the Stacks Project.

AlgebraicGeometry.Stack.isSeparated_relativeDiagonal_of_isSetoidCategory_dottedArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionSecondDiagonal.lean, line 230.

Stacks 0CLR. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. If the relative diagonal Δ_f is quasi-separated, and if for every diagram (0CLB) and every choice of γ as in Definition 0CLA the category of dotted arrows is a setoid, then Δ_f is separated.

Both conditions on Δ_f are read in the relative sense of Stacks 04XB. The setoid hypothesis gives the uniqueness part of the valuative criterion for Δ_f through Stacks 0E8L, and quasi-separatedness turns that into separatedness through Stacks 03KV. This is the converse of the setoid assertion of Stacks 0CLC.

theorem isSeparated_relativeDiagonal_of_isSetoidCategory_dottedArrow (f : 𝒳 ⟶ 𝒴)
    (hqs : IsQuasiSeparated B S hS
      (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom))
    (hsetoid : ∀ D : ValuativeDiagram B S hS 𝒳 𝒴 f,
      IsSetoidCategory (CategoryTheory.DottedArrow D.x D.j f.hom D.y D.γ)) :
    IsSeparated B S hS (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom)
Sources
LeanAlgebraicGeometry.Stack.isSeparated_relativeDiagonal_of_isSetoidCategory_dottedArrow

Section101.41 Valuative criterion for the diagonal#

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

Tag 0E8L, a lemma

Tag 0E8L in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.diagonalDottedArrowFst, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionDiagonal.lean, line 189. The attribute's comment: “part (1): the dotted arrow coming from the first projection”.

Stacks 0E8L, part (1), first arrow. The triple (a₁, α₁, id) is a dotted arrow for the square of f with top row x, bottom row f ∘ a₁ and right edge f.

def diagonalDottedArrowFst :
    CategoryTheory.DottedArrow D.x D.j f.hom
      ((D.y ≫ (twoFibreProductSquare B S hS f f).fst.hom) ≫ f.hom)
      (diagonalWitness B S hS D)

AlgebraicGeometry.Stack.AlgebraicStacks.diagonalDottedArrowSnd, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionDiagonal.lean, line 203. The attribute's comment: “part (1): the dotted arrow coming from the second projection”.

Stacks 0E8L, part (1), second arrow. The triple (a₂, α₂, φ) is a dotted arrow for the same square of f: the compatibility triangle is the statement that γ is a 2-morphism into the 2-fibre product, by the exchange law and AlgebraicGeometry.Stack.AlgebraicStacks.relativeDiagonal_whiskerLeft_twoFibreProductCell.

def diagonalDottedArrowSnd :
    CategoryTheory.DottedArrow D.x D.j f.hom
      ((D.y ≫ (twoFibreProductSquare B S hS f f).fst.hom) ≫ f.hom)
      (diagonalWitness B S hS D)

AlgebraicGeometry.Stack.AlgebraicStacks.isSetoidCategory_dottedArrow_relativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionDiagonal.lean, line 256. The attribute's comment: “part (2): the category of diagonal fillers is a setoid”.

Stacks 0E8L, part (2), first assertion. The category of dotted arrows of a valuative diagram for the relative diagonal of a 1-morphism of algebraic stacks is a setoid.

The relative diagonal is representable by algebraic spaces (Stacks 04XS), hence its underlying functor is faithful (Stacks 04Y5), and the category of dotted arrows along a faithful 1-morphism is a thin groupoid.

theorem isSetoidCategory_dottedArrow_relativeDiagonal :
    IsSetoidCategory
      (CategoryTheory.DottedArrow D.x D.j (relativeDiagonal B S hS f).hom D.y D.γ)

AlgebraicGeometry.Stack.AlgebraicStacks.diagonalDottedArrowClassesEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionDiagonal.lean, line 502. The attribute's comment: “part (2): isomorphism classes are the morphisms between the two dotted arrows”.

Stacks 0E8L, part (2), second assertion. The isomorphism classes of dotted arrows of a valuative diagram for the relative diagonal of f correspond bijectively to the morphisms (a₁, α₁, id) ⟶ (a₂, α₂, φ) of dotted arrows for f, by d ↦ (β ⋆ pr₁) ∘ (β ⋆ pr₂)⁻¹.

noncomputable def diagonalDottedArrowClassesEquiv :
    Quotient (isIsomorphicSetoid
        (CategoryTheory.DottedArrow D.x D.j (relativeDiagonal B S hS f).hom D.y D.γ)) ≃
      (diagonalDottedArrowFst B S hS D ⟶ diagonalDottedArrowSnd B S hS D)
Tag 0CLT, a lemma

Tag 0CLT in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_valuativeCriterionUniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeUniquenessSeparated.lean, line 272.

Stacks 0CLT. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. Assume f is quasi-separated. If f satisfies the uniqueness part of the valuative criterion, then f is separated.

Separatedness of f is properness of Δ_f in the relative sense of Stacks 04XB. Its three conjuncts are: separatedness of Δ_f, which is Stacks 0CLR fed with the setoid half of the uniqueness criterion; finiteness of type, whose quasi-compactness half is the first conjunct of quasi-separatedness and whose local half is part (2) of Stacks 04XS; and universal closedness, which comes from the existence part of the valuative criterion for Δ_f through Stacks 0CLN and Stacks 03KA.

theorem isSeparated_of_valuativeCriterionUniqueness (f : 𝒳 ⟶ 𝒴)
    (hqs : IsQuasiSeparated B S hS f)
    (hu : ValuativeCriterion.Uniqueness B S hS f) :
    IsSeparated B S hS f
Tag 0CLU, a lemma

Tag 0CLU in the Stacks Project.

AlgebraicGeometry.Stack.valuativeCriterionUniqueness_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedImpliesValuativeUniqueness.lean, line 406.

Stacks 0CLU. A separated 1-morphism of algebraic stacks satisfies the uniqueness part of the valuative criterion.

Separatedness is properness of the relative diagonal Δ_f in the sense of Stacks 04XB, so Δ_f is in particular separated there and the category of dotted arrows of every valuative diagram is a setoid by Stacks 0CLC. For the second half, two dotted arrows a, b of one valuative diagram assemble into a scheme-valued point (a, b, β_b ∘ β_a⁻¹) of 𝒳 ×_𝒴 𝒳 whose valuative diagram for Δ_f is filled by (α_a, α_b); Δ_f is proper and representable by algebraic spaces (Stacks 04XS), so that diagram has a dotted arrow by the valuative criterion of properness for algebraic spaces (Stacks 0A40), and Stacks 0E8L turns that dotted arrow into a morphism a ⟶ b, which the setoid property makes an isomorphism.

theorem valuativeCriterionUniqueness_of_isSeparated (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsSeparated B S hS f) :
    ValuativeCriterion.Uniqueness B S hS f
Sources
LeanAlgebraicGeometry.Stack.AlgebraicStacks.diagonalDottedArrowFst · AlgebraicGeometry.Stack.AlgebraicStacks.diagonalDottedArrowSnd · AlgebraicGeometry.Stack.AlgebraicStacks.isSetoidCategory_dottedArrow_relativeDiagonal · AlgebraicGeometry.Stack.AlgebraicStacks.diagonalDottedArrowClassesEquiv · AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_valuativeCriterionUniqueness · AlgebraicGeometry.Stack.valuativeCriterionUniqueness_of_isSeparated

Section101.42 Valuative criterion for universal closedness#

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

Tag 0CLW, a lemma

Tag 0CLW in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_of_isQuasiCompactMorphism_of_valuativeCriterionExistence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionUniversallyClosed.lean, line 381.

Stacks 0CLW. A 1-morphism of algebraic stacks over S which is quasi-compact (Stacks 050U) and satisfies the existence part of the valuative criterion (Stacks 0CLK) is universally closed (Stacks 0513, part (2)).

theorem universallyClosed_of_isQuasiCompactMorphism_of_valuativeCriterionExistence
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hqc : Stack.IsQuasiCompactMorphism B S hS f)
    (hex : Stack.ValuativeCriterion.Existence B S hS f) :
    UniversallyClosed B S hS f
Tag 0CLX, a lemma

Tag 0CLX in the Stacks Project.

AlgebraicGeometry.Stack.valuativeCriterionExistence_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeExistenceUniversallyClosed.lean, line 387.

Stacks 0CLX. A quasi-separated, universally closed 1-morphism of algebraic stacks satisfies the existence part of the valuative criterion.

Given a valuative square q, the specialisation step AlgebraicGeometry.Stack.ValuativeSquare.exists_valuativeSquare_genericSection produces a valuative square q₂ for the generic section of q whose closed point lies over the closed point of Spec q.R. Its valuation ring and fraction field are the dominating extension; the two ring maps come from 2-Yoneda and the full faithfulness of Spec; locality of the ring map is the closed-point condition; and the dotted arrow is the special point of q₂ followed by the projection to 𝒳.

theorem valuativeCriterionExistence_of_universallyClosed
    (hqs : AlgebraicStacks.IsQuasiSeparated B S hS f)
    (hclosed : AlgebraicStacks.UniversallyClosed B S hS f) :
    ValuativeCriterion.Existence B S hS f
Sources
LeanAlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_of_isQuasiCompactMorphism_of_valuativeCriterionExistence · AlgebraicGeometry.Stack.valuativeCriterionExistence_of_universallyClosed

Section101.43 Valuative criterion for properness#

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

Tag 0CLZ, a lemma

Tag 0CLZ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isProper_iff_valuativeCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ValuativeCriterionProperness.lean, line 159.

Stacks 0CLZ. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S which is of finite type (Stacks 06FS, part (2)) and quasi-separated (Stacks 04YW). Then f is proper (Stacks 0CL5) if and only if it satisfies both the uniqueness part (Stacks 0CLG) and the existence part (Stacks 0CLK) of the valuative criterion.

Properness is separatedness, finite type and universal closedness, and under the standing hypotheses the equivalence is the conjunction of two equivalences: separatedness is the uniqueness part, by Stacks 0CLU forwards and Stacks 0CLT backwards, and universal closedness is the existence part, by Stacks 0CLX forwards and Stacks 0CLW backwards.

theorem isProper_iff_valuativeCriterion (f : 𝒳 ⟶ 𝒴)
    (hft : IsFiniteType B S hS f)
    (hqs : IsQuasiSeparated B S hS f) :
    IsProper B S hS f ↔
      ValuativeCriterion.Uniqueness B S hS f ∧ ValuativeCriterion.Existence B S hS f
Sources
LeanAlgebraicGeometry.Stack.AlgebraicStacks.isProper_iff_valuativeCriterion

Section101.44 Local complete intersection morphisms#

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

Tag 0CJ3, a definition

Tag 0CJ3 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsLocalCompleteIntersection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalCompleteIntersectionMorphism.lean, line 71.

Stacks 0CJ3. A 1-morphism of algebraic stacks over S is a local complete intersection morphism, or Koszul, when it passes the universal smooth-diagram test of Stacks 06FM at the local complete intersection property of morphisms of algebraic spaces: 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 a local complete intersection morphism.

abbrev IsLocalCompleteIntersection {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    Prop
Tag 0CJ4, a lemma

Tag 0CJ4 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsLocalCompleteIntersection.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalCompleteIntersectionComp.lean, line 57.

Stacks 0CJ4. The composition of local complete intersection 1-morphisms of algebraic stacks over S is a local complete intersection 1-morphism: if f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 are Koszul, so is f ≫ g.

This is the general composition remark Stacks 06FP at the Koszul property of morphisms of algebraic spaces, which is stable under composition by Stacks 06C8, as in AlgebraicGeometry.Stack.AlgebraicStacks.isLocalCompleteIntersection_comp; the smooth locality on the source-and-target that argument consumes is AlgebraicGeometry.Space.isLocalCompleteIntersection_isSmoothLocalOnSourceAndTarget.

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

AlgebraicGeometry.Stack.AlgebraicStacks.isLocalCompleteIntersection_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalCompleteIntersectionComposition.lean, line 111. The attribute's comment: “the composition argument in full, carrying one hypothesis this library does not prove: hlocal, Stacks 06FC at the Koszul property of morphisms of algebraic spaces”.

Stacks 0CJ4. A composition of local complete intersection 1-morphisms of algebraic stacks over S is a local complete intersection 1-morphism: if f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 are Koszul, so is f ≫ g.

This is the general composition remark Stacks 06FP, AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_comp, at the Koszul property of morphisms of algebraic spaces, which is stable under composition by Stacks 06C8. Stacks 0CJ3 is the universal smooth-diagram criterion of Stacks 06FM where that remark speaks about the existential one, so the hypotheses and the conclusion are moved across the equivalence of conditions (1) and (2) of Stacks 06FM.

One hypothesis beyond the source's is carried: hlocal, that the Koszul property of morphisms of algebraic spaces is smooth local on the source-and-target (Stacks 06FC at that property), which is what crosses that equivalence. It is not available in this library; see the carried-hypothesis note in the module docstring.

theorem isLocalCompleteIntersection_comp
    (hlocal : Space.IsSmoothLocalOnSourceAndTarget B S hS
      (fun _ _ k => Space.IsLocalCompleteIntersection B S hS k))
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsLocalCompleteIntersection B S hS f)
    (hg : IsLocalCompleteIntersection B S hS g) :
    IsLocalCompleteIntersection B S hS (f ≫ g)
Tag 0CJ5, a lemma

Tag 0CJ5 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocalCompleteIntersection_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalCompleteIntersectionFlatBaseChange.lean, line 529. The attribute's comment: “the base-change argument in full, carrying one hypothesis this library does not prove: hlocal, Stacks 06FC at the Koszul property of morphisms of algebraic spaces”.

Stacks 0CJ5. A flat base change of a local complete intersection 1-morphism of algebraic stacks over S is a local complete intersection 1-morphism: if Q is a 2-fibre product of the cospan (g, f), g is flat and f is Koszul, then the projection Q.fst is Koszul.

This is the flat base-change remark hasPropertyOnSomeSmoothDiagram_baseChange_of_isFlat — the form of Stacks 06FQ the source's hint names — at the Koszul property of morphisms of algebraic spaces, which is invariant under isomorphism by Stacks 03MJ and stable under flat base change by Stacks 06C7. Stacks 0CJ3 is the universal smooth-diagram criterion of Stacks 06FM where that remark concludes about the existential one, so both hypothesis and conclusion are moved across the equivalence of conditions (1) and (2) of Stacks 06FM.

One hypothesis beyond the source's is carried: hlocal, that the Koszul property of morphisms of algebraic spaces is smooth local on the source-and-target (Stacks 06FC at that property), which is what crosses that equivalence. It is not available in this library; see the carried-hypothesis note in the module docstring.

theorem isLocalCompleteIntersection_baseChange
    (hlocal : Space.IsSmoothLocalOnSourceAndTarget B S hS
      (fun _ _ k => Space.IsLocalCompleteIntersection B S hS k))
    {𝒳 𝒴 𝒴' : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴) (hg : IsFlat B S hS g)
    (Q : Bicategory.TwoCommSq g f)
    (hQ : Bicategory.IsTwoFibreProduct Q)
    (hf : IsLocalCompleteIntersection B S hS f) :
    IsLocalCompleteIntersection B S hS Q.fst

AlgebraicGeometry.Stack.AlgebraicStacks.isLocalCompleteIntersection_baseChange_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalCompleteIntersectionIsFlatBaseChange.lean, line 64.

Stacks 0CJ5. A flat base change of a local complete intersection 1-morphism of algebraic stacks over S is a local complete intersection 1-morphism: if Q is a 2-fibre product of the cospan (g, f) of algebraic stacks, g is flat and f is Koszul, then the projection Q.fst to the source of g is Koszul.

This is the flat base-change argument AlgebraicGeometry.Stack.AlgebraicStacks.isLocalCompleteIntersection_baseChange, with the smooth source-and-target locality of the Koszul property of morphisms of algebraic spaces (Stacks 06FC at that property) supplied by AlgebraicGeometry.Space.isLocalCompleteIntersection_isSmoothLocalOnSourceAndTarget.

theorem isLocalCompleteIntersection_baseChange_of_isFlat
    {𝒳 𝒴 𝒴' : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴) (hg : IsFlat B S hS g)
    (Q : Bicategory.TwoCommSq g f)
    (hQ : Bicategory.IsTwoFibreProduct Q)
    (hf : IsLocalCompleteIntersection B S hS f) :
    IsLocalCompleteIntersection B S hS Q.fst
Tag 0CJ6, a lemma

Tag 0CJ6 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocalCompleteIntersection_of_isLocalCompleteIntersection_comp_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalCompleteIntersectionSmoothCancellation.lean, line 167.

Stacks 0CJ6. Let f : 𝒳 ⟶ 𝒴, g : 𝒴 ⟶ 𝒵 and h : 𝒳 ⟶ 𝒵 be 1-morphisms of algebraic stacks over S forming a 2-commutative triangle, f ≫ g ≅ h. If g is smooth and h is a local complete intersection morphism, then f is a local complete intersection morphism.

Both the hypothesis on h and the conclusion are the universal smooth-diagram criterion of Stacks 06FM (Definition Stacks 0CJ3), and they are moved to the existential one by smooth locality on the source-and-target of the Koszul property of morphisms of algebraic spaces, AlgebraicGeometry.Space.isLocalCompleteIntersection_isSmoothLocalOnSourceAndTarget. The cancellation is AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_of_comp_of_flatBaseChange at the pair (Koszul, smooth), whose space-level input is Stacks 0CHL, AlgebraicGeometry.Space.isLocalCompleteIntersection_of_comp_of_isSmooth, and which uses flat base change of the Koszul property (Stacks 06C7) and base change of smoothness (Stacks 03ZE).

theorem isLocalCompleteIntersection_of_isLocalCompleteIntersection_comp_of_isSmooth
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (h : 𝒳 ⟶ 𝒵) (e : f ≫ g ≅ h)
    (hg : IsSmooth B S hS g) (hh : IsLocalCompleteIntersection B S hS h) :
    IsLocalCompleteIntersection B S hS f
Sources
LeanAlgebraicGeometry.Stack.AlgebraicStacks.IsLocalCompleteIntersection · AlgebraicGeometry.Stack.AlgebraicStacks.IsLocalCompleteIntersection.comp · AlgebraicGeometry.Stack.AlgebraicStacks.isLocalCompleteIntersection_comp · AlgebraicGeometry.Stack.AlgebraicStacks.isLocalCompleteIntersection_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.isLocalCompleteIntersection_baseChange_of_isFlat · AlgebraicGeometry.Stack.AlgebraicStacks.isLocalCompleteIntersection_of_isLocalCompleteIntersection_comp_of_isSmooth

Section101.45 Stabilizer preserving morphisms#

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

Tag 0DU7, a lemma

Tag 0DU7 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_of_inertiaPullbackComparison_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StabilizerPreservingRepresentable.lean, line 192.

Stacks 0DU7. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. If the canonical comparison ℐ_𝒳 ⟶ 𝒳 ×_𝒴 ℐ_𝒴 of Stacks 06R5 is an isomorphism, then f is representable by algebraic spaces.

The comparison makes f faithful (AlgebraicGeometry.Stack.faithful_homFunctor_of_inertiaPullbackComparison_full, condition (4) of Stacks 04YY), and a faithful 1-morphism of algebraic stacks is representable by algebraic spaces (Stacks 04Y5, the implication (2) ⟹ (3)).

theorem isRepresentableByAlgebraicSpaces_of_inertiaPullbackComparison_isEquivalence
    (f : 𝒳 ⟶ 𝒴)
    (hf : (CategoryTheory.inertiaPullbackComparison 𝒳.val.val.p 𝒴.val.val.p
      (CatFiberedInGroupoids.homFunctor f.hom)
      (CatFiberedInGroupoids.homFunctor_comp_p f.hom)).IsEquivalence) :
    IsRepresentableByAlgebraicSpaces B S hS f.hom.hom
Tag 0DU8, a remark

Tag 0DU8 in the Stacks Project.

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

Stacks 0DU8. Let x : T ⟶ 𝒳 have an algebraic space as source, and let G ⟶ H be the pullback to T of the stabilizer comparison ℐ_𝒳 ⟶ 𝒳 ×_𝒴 ℐ_𝒴, that is, the map G = Isom_𝒳(x, x) ⟶ Isom_𝒴(f ∘ x, f ∘ x) = H on automorphism spaces. Then G ⟶ H satisfies a condition of Stacks 04XB as soon as the relative diagonal Δ_f does, for an arbitrary property P of morphisms of algebraic spaces over S: if Δ_f is unramified, étale, proper, … then so is G ⟶ H.

The square T ×_𝒳 T ⟶ 𝒳, T ×_𝒴 T ⟶ 𝒳 ×_𝒴 𝒳 over Δ_f is 2-cartesian, so T ×_𝒳 T ⟶ T ×_𝒴 T is a base change of Δ_f (Stacks 050H), and G ⟶ H is a base change of that along the diagonal of T (Stacks 0CPL, part (2)).

theorem prop_isomMap_of_prop_relativeDiagonal
    (x : algebraicSpaceStack.{u, w} B S hS T hT ⟶ 𝒳)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤
        (AlgebraicStacks.twoFibreProduct B S hS f f).val.val.obj)
      (_hy : y ⋙ (AlgebraicStacks.twoFibreProduct B S hS f f).val.val.p = Over.map U.hom)
      (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.val.p
            (AlgebraicStacks.twoFibreProduct B S hS f f).val.val.p y
            (CatFiberedInGroupoids.homFunctor
              (Stack.relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom)))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        P (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩))) :
    ∀ (U : BigFppfOver B S hS)
      (z : BigFppfOver B U.left.1 U.left.2 ⥤
        (isomStack B S hS T hT (x ≫ f) (x ≫ f)).val.obj)
      (_hz : z ⋙ (isomStack B S hS T hT (x ≫ f) (x ≫ f)).val.p = Over.map U.hom)
      (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom)
            (isomStack B S hS T hT x x).val.p
            (isomStack B S hS T hT (x ≫ f) (x ≫ f)).val.p z
            (CatFiberedInGroupoids.homFunctor (isomMap B S hS f T hT x x)))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        P (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩))
Tag 0DU9, a lemma

Tag 0DU9 in the Stacks Project.

AlgebraicGeometry.Stack.inertiaPullbackComparison_isEquivalenceOver_iff_inducesIsomorphismAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StabilizerPreservingUnramified.lean, line 187.

Stacks 0DU9. Let f : 𝒳 ⟶ 𝒴 be an unramified 1-morphism of algebraic stacks over S. Then the canonical comparison ℐ_𝒳 ⟶ 𝒳 ×_𝒴 ℐ_𝒴 of Stacks 06R5 is an isomorphism (an equivalence over the big fppf site) if and only if f induces an isomorphism between the automorphism groups at x and at f(x) (Stacks 0DTW) for every x ∈ |𝒳|.

theorem inertiaPullbackComparison_isEquivalenceOver_iff_inducesIsomorphismAt
    (f : 𝒳 ⟶ 𝒴) (hu : IsUnramified B S hS f) :
    Nonempty (IsEquivalenceOver
      (RelativeInertia.toBase 𝒳.val.val.p)
      (TwoFibreProductOver.structureFunctor (RelativeInertia.toBase 𝒴.val.val.p)
        𝒳.val.val.p 𝒴.val.val.p (RelativeInertia.π 𝒴.val.val.p)
        (CatFiberedInGroupoids.homFunctor f.hom))
      (inertiaPullbackComparison 𝒳.val.val.p 𝒴.val.val.p
        (CatFiberedInGroupoids.homFunctor f.hom)
        (CatFiberedInGroupoids.homFunctor_comp_p f.hom))) ↔
      ∀ q : points B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids,
        InducesIsomorphismAt B S hS f q
Tag 0DUA, a lemma

Tag 0DUA in the Stacks Project.

AlgebraicGeometry.Stack.exists_openSubstack_isStabilizerPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StabilizerPreservingLocus.lean, line 694.

Stacks 0DUA. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S which is representable by algebraic spaces and unramified, and assume the inertia ℐ_𝒴 ⟶ 𝒴 is proper. Then the set of x ∈ |𝒳| at which f induces an isomorphism between the automorphism groups at x and at f(x) (Stacks 0DTW) is open; there is an open substack 𝒰 ⊆ 𝒳 with that set of points (Stacks 06FJ); and for every open substack 𝒰 ⊆ 𝒳 with that set of points, the canonical comparison ℐ_𝒰 ⟶ 𝒰 ×_𝒴 ℐ_𝒴 of Stacks 06R5 is an isomorphism.

theorem exists_openSubstack_isStabilizerPreserving
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) (hu : IsUnramified B S hS f)
    (hI : AlgebraicStacks.IsProper B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒴)) :
    @IsOpen _ (pointTopology B S hS 𝒳.val) (stabilizerPreservingLocus B S hS f) ∧
      (∃ U : OpenSubstack 𝒳, U.pointSet B S hS = stabilizerPreservingLocus B S hS f) ∧
        ∀ U : OpenSubstack 𝒳, U.pointSet B S hS = stabilizerPreservingLocus B S hS f →
          IsStabilizerPreserving B S hS (U.inclusion ≫ f)
Tag 0DUB, a lemma

Tag 0DUB in the Stacks Project.

AlgebraicGeometry.Stack.inducesIsomorphismAt_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismGroupBaseChange.lean, line 309. The attribute's comment: “the automorphism groups at a point of a base change”.

Stacks 0DUB, part (1). In a 2-cartesian square of algebraic stacks with apex 𝒳', first projection f' : 𝒳' ⟶ 𝒴' and second projection 𝒳' ⟶ 𝒳, if f induces an isomorphism between automorphism groups at the image x of a point x' of |𝒳'|, then f' induces an isomorphism between automorphism groups at x'.

The hypothesis is the isomorphism at the single point x and nothing else; in particular f is not assumed stabilizer preserving, which is the hypothesis of part (2).

theorem inducesIsomorphismAt_baseChange (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (x' : points B S hS P.pt.val.val P.pt.val.isFiberedInGroupoids)
    (hx : InducesIsomorphismAt B S hS f
      (pointsMap B S hS P.pt.val.val P.pt.val.isFiberedInGroupoids
        𝒳.val.isFiberedInGroupoids P.snd.hom.hom x')) :
    InducesIsomorphismAt B S hS P.fst x'

AlgebraicGeometry.Stack.nonempty_inertiaPullbackComparison_isEquivalenceOver_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StabilizerPreserving.lean, line 79. The attribute's comment: “the inertia map of a base change”.

Stacks 0DUB, part (2). In a cartesian square of algebraic stacks, if the canonical comparison from the inertia of 𝒳 to 𝒳 ×_𝒴 ℐ_𝒴 is an equivalence, then so is the corresponding comparison for the base change of f along g.

The base change of f : 𝒳 ⟶ 𝒴 along g : 𝒴' ⟶ 𝒴 is the first projection of a 2-fibre product P of the cospan (g, f).

theorem nonempty_inertiaPullbackComparison_isEquivalenceOver_baseChange
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hf : (CategoryTheory.inertiaPullbackComparison 𝒳.val.val.p 𝒴.val.val.p
      (CatFiberedInGroupoids.homFunctor f.hom)
      (CatFiberedInGroupoids.homFunctor_comp_p f.hom)).IsEquivalence) :
    Nonempty (CategoryTheory.IsEquivalenceOver
      (RelativeInertia.toBase P.pt.val.val.p)
      (TwoFibreProductOver.structureFunctor (RelativeInertia.toBase 𝒴'.val.val.p)
        P.pt.val.val.p 𝒴'.val.val.p (RelativeInertia.π 𝒴'.val.val.p)
        (CatFiberedInGroupoids.homFunctor P.fst.hom))
      (CategoryTheory.inertiaPullbackComparison P.pt.val.val.p 𝒴'.val.val.p
        (CatFiberedInGroupoids.homFunctor P.fst.hom)
        (CatFiberedInGroupoids.homFunctor_comp_p P.fst.hom)))
Tag 0DUC, a lemma

Tag 0DUC in the Stacks Project.

AlgebraicGeometry.Stack.isoClassMk_eq_of_isoClassMk_eq_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FieldValuedPointsBaseChange.lean, line 208. The attribute's comment: “field-valued points of a base change, injective on isomorphism classes”.

Stacks 0DUC. Let 𝒳' be the apex of a 2-cartesian square of algebraic stacks with f' : 𝒳' ⟶ 𝒴' its first projection, over f : 𝒳 ⟶ 𝒴 and g : 𝒴' ⟶ 𝒴, and suppose f induces an isomorphism between automorphism groups at every point of |𝒳| (Stacks 0DTW). Then for every field k the map Mor(Spec k, 𝒳') → Mor(Spec k, 𝒴') × Mor(Spec k, 𝒳) is injective on isomorphism classes.

A 1-morphism Spec k ⟶ 𝒳' is, by 2-Yoneda, an object of the fibre of 𝒳' over an object U of the big site with underlying scheme Spec k, and its isomorphism class is CategoryTheory.Functor.isoClassMk; so this says that two such 1-morphisms with the same pair of classes in 𝒴' and in 𝒳 have the same class in 𝒳'.

theorem isoClassMk_eq_of_isoClassMk_eq_components (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hf : ∀ q : points B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids,
      InducesIsomorphismAt B S hS f q)
    (k : Type u) [Field k] (U : BigFppfOver B S hS)
    (hU : (BigFppfOver.toScheme B S hS).obj U ≅ Spec (.of k))
    (a b : P.pt.val.val.p.Fiber U)
    (hfst : Functor.isoClassMk 𝒴'.val.val.p
        ((Functor.fiberMap P.pt.val.val.p 𝒴'.val.val.p
          (CatFiberedInGroupoids.homFunctor P.fst.hom)
          (CatFiberedInGroupoids.homFunctor_comp_p P.fst.hom) U).obj a)
      = Functor.isoClassMk 𝒴'.val.val.p
        ((Functor.fiberMap P.pt.val.val.p 𝒴'.val.val.p
          (CatFiberedInGroupoids.homFunctor P.fst.hom)
          (CatFiberedInGroupoids.homFunctor_comp_p P.fst.hom) U).obj b))
    (hsnd : Functor.isoClassMk 𝒳.val.val.p
        ((Functor.fiberMap P.pt.val.val.p 𝒳.val.val.p
          (CatFiberedInGroupoids.homFunctor P.snd.hom)
          (CatFiberedInGroupoids.homFunctor_comp_p P.snd.hom) U).obj a)
      = Functor.isoClassMk 𝒳.val.val.p
        ((Functor.fiberMap P.pt.val.val.p 𝒳.val.val.p
          (CatFiberedInGroupoids.homFunctor P.snd.hom)
          (CatFiberedInGroupoids.homFunctor_comp_p P.snd.hom) U).obj b)) :
    Functor.isoClassMk P.pt.val.val.p a = Functor.isoClassMk P.pt.val.val.p b
Tag 0DUD, a lemma

Tag 0DUD in the Stacks Project.

AlgebraicGeometry.Stack.isEquivalence_of_isEtale_of_inducesIsomorphismAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleStabilizerPreservingIsomorphism.lean, line 295.

Stacks 0DUD. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. Assume f is étale, that f induces an isomorphism between the automorphism groups at x and at f(x) for every x ∈ |𝒳| (Stacks 0DTW), and that for every algebraically closed field k the functor Mor(Spec k, 𝒳) ⟶ Mor(Spec k, 𝒴) is an equivalence. Then f is an isomorphism.

The proof is the source's. Fullness of the functors on geometric points is condition (3) of Stacks 0CPN, so f is universally injective. Étale implies unramified (Stacks 0CIW), so Stacks 0DU9 makes f stabilizer preserving and Stacks 0DU7 makes it representable by algebraic spaces. Essential surjectivity on geometric points makes f surjective, and Stacks 05W5, in the form AlgebraicGeometry.Stack.isEquivalence_of_isEtale_of_universallyInjective_of_isSurjective, concludes.

theorem isEquivalence_of_isEtale_of_inducesIsomorphismAt (f : 𝒳 ⟶ 𝒴)
    (he : IsEtale B S hS f)
    (hauto : ∀ x : AlgebraicStacks.points B S hS 𝒳, InducesIsomorphismAt B S hS f x)
    (hfibre : ∀ (k : Type u) [Field k] [IsAlgClosed k] (V : BigFppfOver B S hS),
      ((BigFppfOver.toScheme B S hS).obj V ≅ Spec (.of k)) →
        (geometricFibreFunctor B S hS f V).IsEquivalence) :
    (CatFiberedInGroupoids.homFunctor f.hom).IsEquivalence
Sources
LeanAlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_of_inertiaPullbackComparison_isEquivalence · AlgebraicGeometry.Stack.HigherDiagonal.prop_isomMap_of_prop_relativeDiagonal · AlgebraicGeometry.Stack.inertiaPullbackComparison_isEquivalenceOver_iff_inducesIsomorphismAt · AlgebraicGeometry.Stack.exists_openSubstack_isStabilizerPreserving · AlgebraicGeometry.Stack.inducesIsomorphismAt_baseChange · AlgebraicGeometry.Stack.nonempty_inertiaPullbackComparison_isEquivalenceOver_baseChange · AlgebraicGeometry.Stack.isoClassMk_eq_of_isoClassMk_eq_components · AlgebraicGeometry.Stack.isEquivalence_of_isEtale_of_inducesIsomorphismAt

Section101.46 Normalization#

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

Tag 0GMI, a lemma

Tag 0GMI in the Stacks Project.

AlgebraicGeometry.Stack.exists_smooth_atlas_iff_forall_smooth_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Normalization.lean, line 120. The attribute's comment: “conditions (1) and (2)”.

Stacks 0GMI, conditions (1) and (2). One smooth surjective scheme chart whose quasi-compact opens have finitely many irreducible components suffices: then every smooth scheme chart of the algebraic stack has that property.

theorem exists_smooth_atlas_iff_forall_smooth_chart (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    HasPropertyOnSomeSchemeAtlas B S hS
        (fun X : Scheme.{u} =>
          ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite) 𝒳 ↔
      HasPropertyOnEverySchemeChart B S hS
        (fun X : Scheme.{u} =>
          ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite) 𝒳

AlgebraicGeometry.Stack.forall_smooth_chart_iff_forall_space, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Normalization.lean, line 133. The attribute's comment: “conditions (2) and (3)”.

Stacks 0GMI, conditions (2) and (3). Every smooth scheme chart of the algebraic stack has finitely many irreducible components over each of its quasi-compact opens exactly when every algebraic space smooth over it satisfies the equivalent conditions of Tag 0BB1.

theorem forall_smooth_chart_iff_forall_space (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    HasPropertyOnEverySchemeChart B S hS
        (fun X : Scheme.{u} =>
          ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite) 𝒳 ↔
      ∀ (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
        (f : algebraicSpaceStack.{u, w} B S hS F hF ⟶ 𝒳),
        AlgebraicStacks.IsSmooth B S hS f →
          Space.HasLocallyFiniteIrreducibleComponents B S hS F

AlgebraicGeometry.Stack.forall_smooth_chart_iff_finite_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Normalization.lean, line 153. The attribute's comment: “conditions (2) and (4)”.

Stacks 0GMI, conditions (2) and (4). Every smooth scheme chart of the algebraic stack has finitely many irreducible components over each of its quasi-compact opens exactly when the space of points of Tag 04XL of every quasi-compact algebraic stack smooth over it has finitely many irreducible components.

theorem forall_smooth_chart_iff_finite_irreducibleComponents
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    HasPropertyOnEverySchemeChart B S hS
        (fun X : Scheme.{u} =>
          ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite) 𝒳 ↔
      ∀ (𝒴 : AlgebraicStacks.{u, w} B S hS) (f : 𝒴 ⟶ 𝒳),
        IsQuasiCompactStack.{u, w} B S hS 𝒴.val 𝒴.property →
          AlgebraicStacks.IsSmooth B S hS f →
            (@irreducibleComponents (AlgebraicStacks.points B S hS 𝒴)
              (pointTopology B S hS 𝒴.val)).Finite
Tag 0GMJ, a lemma

Tag 0GMJ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isIntegralHom_normalization_and_isTwoFibreProduct_normSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NormalizationBaseChange.lean, line 344.

Stacks 0GMJ. Let 𝒳 be an algebraic stack over S satisfying the equivalent conditions of Stacks 0GMI, and let ν : 𝒳^ν ⟶ 𝒳 be its normalization (Stacks 0GMK). Then ν is integral (Stacks 0CHU), and for every scheme U over S and every smooth 1-morphism f : U ⟶ 𝒳, every 2-fibre product U ×_𝒳 𝒳^ν is the normalization of U: it is represented by an algebraic space isomorphic, over U, to the normalization U^ν ⟶ U of the scheme U (AlgebraicGeometry.Space.normSpace, AlgebraicGeometry.Space.normSpaceProj; Stacks 035N).

The finiteness of irreducible components of the quasi-compact opens of U that the normalization of U needs is condition (2) of Stacks 0GMI for the smooth chart f.

theorem isIntegralHom_normalization_and_isTwoFibreProduct_normSpace :
    AlgebraicStacks.IsIntegralHom B S hS (normalization 𝒳 h𝒳) ∧
      ∀ (U : BigFppfOver B S hS) (f : schemeStack.{u, w} B S hS U ⟶ 𝒳)
        (hf : AlgebraicStacks.IsSmooth B S hS f)
        (P : Bicategory.TwoCommSq f (normalization 𝒳 h𝒳)) (_ : Bicategory.IsTwoFibreProduct P),
        ∃ (V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS V)
          (eV : StacksRepresentableCFG.EquivalenceOver P.pt.val.val.p
            (presheafOfCategories (V ⋙ typeToCat)).p)
          (e : V ≅ yoneda.obj (Space.normSpace B S hS U
            ((exists_smooth_atlas_iff_forall_smooth_chart B S hS 𝒳).1 h𝒳 U f hf))),
          e.hom ≫ yoneda.map (Space.normSpaceProj B S hS U
              ((exists_smooth_atlas_iff_forall_smooth_chart B S hS 𝒳).1 h𝒳 U f hf)) =
            representingMap B S hS P.pt.val (schemeStack.{u, w} B S hS U).val V (yoneda.obj U) eV
              (PresheafOfCategories.sliceElementsEquivalenceOver U) P.fst.hom

AlgebraicGeometry.Stack.AlgebraicStacks.exists_isIntegralHom_and_isTwoFibreProduct_normSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NormalizationBaseChange.lean, line 387. The attribute's comment: “the existential form”.

Stacks 0GMJ, in the existential form the source states. An algebraic stack 𝒳 over S satisfying the equivalent conditions of Stacks 0GMI admits an integral 1-morphism of algebraic stacks 𝒳^ν ⟶ 𝒳 such that for every scheme U and smooth U ⟶ 𝒳 every 2-fibre product U ×_𝒳 𝒳^ν is the normalization of U. The witness is the normalization of Stacks 0GMK.

theorem exists_isIntegralHom_and_isTwoFibreProduct_normSpace :
    ∃ (𝒳ν : AlgebraicStacks.{u, w} B S hS) (ν : 𝒳ν ⟶ 𝒳),
      AlgebraicStacks.IsIntegralHom B S hS ν ∧
      ∀ (U : BigFppfOver B S hS) (f : schemeStack.{u, w} B S hS U ⟶ 𝒳)
        (hf : AlgebraicStacks.IsSmooth B S hS f)
        (P : Bicategory.TwoCommSq f ν) (_ : Bicategory.IsTwoFibreProduct P),
        ∃ (V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS V)
          (eV : StacksRepresentableCFG.EquivalenceOver P.pt.val.val.p
            (presheafOfCategories (V ⋙ typeToCat)).p)
          (e : V ≅ yoneda.obj (Space.normSpace B S hS U
            ((exists_smooth_atlas_iff_forall_smooth_chart B S hS 𝒳).1 h𝒳 U f hf))),
          e.hom ≫ yoneda.map (Space.normSpaceProj B S hS U
              ((exists_smooth_atlas_iff_forall_smooth_chart B S hS 𝒳).1 h𝒳 U f hf)) =
            representingMap B S hS P.pt.val (schemeStack.{u, w} B S hS U).val V (yoneda.obj U) eV
              (PresheafOfCategories.sliceElementsEquivalenceOver U) P.fst.hom

AlgebraicGeometry.Stack.isTwoFibreProduct_normalizationChartSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NormalizationChartFibreProduct.lean, line 97. The attribute's comment: “the fibre product with a presenting chart is the normalization of the chart”.

Stacks 0GMJ, the fibre-product assertion at the presenting chart. For a groupoid in algebraic spaces (U, R, s, t, c) presenting 𝒳 = [U/R] and a normalized groupoid N for it, the square formed by the normalization 1-morphism ν : [U^ν/R^ν] ⟶ [U/R] of Stacks 046Q and the canonical projection 𝒮_U ⟶ [U/R] of Stacks 044R is a 2-fibre product with apex 𝒮_{U^ν}; that is, 𝒳^ν ×_𝒳 U = U^ν.

This is the assertion of Stacks 0GMJ that the source obtains from R^ν = R ×_{s, U} U^ν by citing Stacks 04ZN, and the proof here is that citation: the cartesian source square is the field AlgebraicGeometry.Stack.NormalizationGroupoid.isPullback_source of the normalized groupoid, and Stacks 04ZN is AlgebraicGeometry.Stack.isTwoFibreProduct_functorialitySquare_of_isPullback.

noncomputable def isTwoFibreProduct_normalizationChartSquare
    (N : NormalizationGroupoid C S hS G) :
    Bicategory.IsTwoFibreProduct (functorialitySquare N.hom)

AlgebraicGeometry.Stack.isIntegralHom_quotientStackMapHom_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NormalizationMorphism.lean, line 231. The attribute's comment: “integrality of ν; the normalized groupoid, Stacks 04ZP and the 04ZN form of the base change are hypotheses”.

Stacks 0GMJ, the 1-morphism 𝒳^ν ⟶ 𝒳 and its integrality. Let (U, R, s, t, c) be a groupoid in algebraic spaces whose quotient stack is 𝒳 = [U/R], and let N be a normalized groupoid for it. Then the 1-morphism ν : [U^ν/R^ν] ⟶ [U/R] of Stacks 046Q induced by the morphism of groupoids (U^ν, R^ν) ⟶ (U, R) is integral in the sense of Stacks 04XB.

The source's argument is exactly this one: U^ν ⟶ U is integral, it is the base change of ν along the presenting chart, and integrality descends. The base-change identification is Stacks 04ZN and is carried; integrality of U^ν ⟶ U is Stacks 0BB4, part (2), and is proved in this library. See the partial-coverage section of the module documentation for every hypothesis and the result it stands for.

theorem isIntegralHom_quotientStackMapHom_normalization
    {G : GroupoidInAlgebraicSpaces C S hS B} (N : NormalizationGroupoid C S hS G)
    (hf : IsRepresentableByAlgebraicSpaces C S hS (quotientStackMapHom N.hom).hom)
    (Q : Bicategory.TwoCommSq (quotientStackProjectionHom G) (quotientStackMapHom N.hom))
    (hQ : Bicategory.IsTwoFibreProduct Q)
    (hQfst : IsRepresentableByAlgebraicSpaces C S hS Q.fst.hom)
    {𝒜 𝒞 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver C S hS)}
    (a : 𝒜 ⟶ 𝒞) (ha : IsRepresentableByAlgebraicSpaces C S hS a.hom)
    (p : Q.pt.val ⥤ᵇ 𝒜.val) (q : (liftedObjectSpace G).val ⥤ᵇ 𝒞.val)
    [Functor.IsEquivalence p.toFunctor] [Functor.IsEquivalence q.toFunctor]
    (α : BasedFunctor.comp p a.hom ≅ BasedFunctor.comp Q.fst.hom q)
    (eF : StacksRepresentableCFG.EquivalenceOver
      𝒜.val.p (presheafOfCategories (N.data.space ⋙ typeToCat)).p)
    (eG₀ : StacksRepresentableCFG.EquivalenceOver
      𝒞.val.p (presheafOfCategories (G.objects.obj ⋙ typeToCat)).p)
    (hrep : representingMap C S hS 𝒜 𝒞 N.data.space G.objects.obj eF eG₀ a = N.data.hom) :
    IsIntegralHom C S hS (quotientStackMapHom N.hom) hf

AlgebraicGeometry.Stack.exists_isIntegralHom_quotientStackMapHom_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NormalizationMorphism.lean, line 263. The attribute's comment: “the existence assertion, witnessed by [U^ν/R^ν] and the 1-morphism of Stacks 046Q”.

Stacks 0GMJ in the existential form the source states it. For a groupoid in algebraic spaces with a normalized groupoid, there is a category fibred in groupoids 𝒳^ν over the big fppf site together with an integral 1-morphism 𝒳^ν ⟶ [U/R].

The witnesses are the quotient stack [U^ν/R^ν] of Stacks 044Q and the 1-morphism of Stacks 046Q, so the existential is inhabited by the source's own construction.

theorem exists_isIntegralHom_quotientStackMapHom_normalization
    {G : GroupoidInAlgebraicSpaces C S hS B} (N : NormalizationGroupoid C S hS G)
    (hf : IsRepresentableByAlgebraicSpaces C S hS (quotientStackMapHom N.hom).hom)
    (Q : Bicategory.TwoCommSq (quotientStackProjectionHom G) (quotientStackMapHom N.hom))
    (hQ : Bicategory.IsTwoFibreProduct Q)
    (hQfst : IsRepresentableByAlgebraicSpaces C S hS Q.fst.hom)
    {𝒜 𝒞 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver C S hS)}
    (a : 𝒜 ⟶ 𝒞) (ha : IsRepresentableByAlgebraicSpaces C S hS a.hom)
    (p : Q.pt.val ⥤ᵇ 𝒜.val) (q : (liftedObjectSpace G).val ⥤ᵇ 𝒞.val)
    [Functor.IsEquivalence p.toFunctor] [Functor.IsEquivalence q.toFunctor]
    (α : BasedFunctor.comp p a.hom ≅ BasedFunctor.comp Q.fst.hom q)
    (eF : StacksRepresentableCFG.EquivalenceOver
      𝒜.val.p (presheafOfCategories (N.data.space ⋙ typeToCat)).p)
    (eG₀ : StacksRepresentableCFG.EquivalenceOver
      𝒞.val.p (presheafOfCategories (G.objects.obj ⋙ typeToCat)).p)
    (hrep : representingMap C S hS 𝒜 𝒞 N.data.space G.objects.obj eF eG₀ a = N.data.hom) :
    ∃ (𝒳ν : CatFiberedInGroupoids (BigFppfOver C S hS))
      (ν : 𝒳ν ⟶ quotientStackCFG C S hS G)
      (hν : IsRepresentableByAlgebraicSpaces C S hS ν.hom),
      IsIntegralHom.{u, u + 1, u + 1, u + 1} C S hS ν hν
Tag 0GMK, a definition

Tag 0GMK in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.normalization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NormalizationAlgebraicStack.lean, line 130.

Stacks 0GMK, the normalization of an algebraic stack. Let 𝒳 be an algebraic stack satisfying the equivalent conditions of Stacks 0GMI. Its normalization is the morphism ν : 𝒳^ν ⟶ 𝒳 constructed in the proof of Stacks 0GMJ: for a presentation 𝒳 ≃ [U/R] (Stacks 04T3), 𝒳^ν = [U^ν/R^ν] is the quotient stack of the normalized groupoid, and ν is the 1-morphism [U^ν/R^ν] ⟶ [U/R] of Stacks 046Q induced by the morphism of groupoids (U^ν, R^ν) ⟶ (U, R), followed by the presentation.

Every ingredient is constructed from 𝒳 and the hypothesis of Stacks 0GMI: the normalization U^ν (Stacks 07U4), the cartesian square R^ν = U^ν ×_{U, s} R, the groupoid structure and its smoothness are those of AlgebraicGeometry.Stack.normalizationGroupoid.

noncomputable def normalization (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : HasPropertyOnSomeSchemeAtlas B S hS
      (fun X : Scheme.{u} =>
        ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite) 𝒳) :
    normalizationStack 𝒳 h𝒳 ⟶ 𝒳

AlgebraicGeometry.Stack.normalization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NormalizationMorphism.lean, line 325. The attribute's comment: “the normalization ν : 𝒳^ν ⟶ 𝒳 at a presenting smooth groupoid, with the normalized groupoid as data”.

Stacks 0GMK, the normalization of an algebraic stack. For a groupoid in algebraic spaces (U, R, s, t, c) presenting 𝒳 = [U/R], and a normalized groupoid N for it, the normalization of 𝒳 is the 1-morphism ν : 𝒳^ν ⟶ 𝒳 of Stacks 046Q induced by the morphism of groupoids (U^ν, R^ν) ⟶ (U, R), with 𝒳^ν = [U^ν/R^ν] the quotient stack AlgebraicGeometry.Stack.normalizationStack of the normalized groupoid.

This is the morphism constructed in Stacks 0GMJ, named: the body is the construction AlgebraicGeometry.Stack.quotientStackMapHom of the source's proof, so nothing is chosen out of the existential of AlgebraicGeometry.Stack.exists_isIntegralHom_quotientStackMapHom_normalization. Its integrality is AlgebraicGeometry.Stack.isIntegralHom_quotientStackMapHom_normalization, which applies to it unchanged.

The hypothesis of Stacks 0GMI on 𝒳 is not a separate assumption, for the reason given in the coverage notes of this module's documentation: it is carried inside N, whose normalization data of the object space contains condition (1) of Stacks 0GMI for the presenting chart through AlgebraicGeometry.Space.NormalizationData.finite_irreducibleComponents_of_chart. The equivalences of Stacks 0GMI are stated for AlgebraicGeometry.Stack.AlgebraicStacks, and exhibiting a quotient stack there is Stacks 04TK, which this library does not have, so no 0GMI condition can be stated at this presentation.

noncomputable abbrev normalization {G : GroupoidInAlgebraicSpaces C S hS B}
    (N : NormalizationGroupoid C S hS G) :
    normalizationStack C S hS N ⟶ quotientStackCFG C S hS G
Sources
LeanAlgebraicGeometry.Stack.exists_smooth_atlas_iff_forall_smooth_chart · AlgebraicGeometry.Stack.forall_smooth_chart_iff_forall_space · AlgebraicGeometry.Stack.forall_smooth_chart_iff_finite_irreducibleComponents · AlgebraicGeometry.Stack.AlgebraicStacks.isIntegralHom_normalization_and_isTwoFibreProduct_normSpace · AlgebraicGeometry.Stack.AlgebraicStacks.exists_isIntegralHom_and_isTwoFibreProduct_normSpace · AlgebraicGeometry.Stack.isTwoFibreProduct_normalizationChartSquare · AlgebraicGeometry.Stack.isIntegralHom_quotientStackMapHom_normalization · AlgebraicGeometry.Stack.exists_isIntegralHom_quotientStackMapHom_normalization

Section101.47 Points and specializations#

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

Tag 0GVZ, a lemma

Tag 0GVZ in the Stacks Project.

AlgebraicGeometry.Stack.exists_specializes_spacePointMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpecializationSmoothChart.lean, line 542.

Stacks 0GVZ. Let 𝒳 be an algebraic stack over S, let f : U ⟶ 𝒳 be a smooth 1-morphism from an algebraic space U over S, let x' ⤳ x be a specialization of points of |𝒳| and let u be a point of |U| with f(u) = x. If the point x' admits a quasi-compact field-valued representative — one of the equivalent conditions of Stacks 0DTK for the pair (𝒳, x') — then there is a specialization u' ⤳ u in |U| with f(u') = x'.

Smoothness of f enters twice. It makes |U| ⟶ |𝒳| an open map (Stacks 06R7), which is what puts u in the closure of the fibre of |U| ⟶ |𝒳| over x': an open neighbourhood of u missing that fibre would have open image containing x but not x'. And it is what makes the base change of the 1-morphism Spec k ⟶ 𝒳 of the representative an algebraic space over the affine chart, so that the fibre is the image, on points, of an affine scheme quasi-compact over the chart; Stacks 02JQ then produces the specialization inside that fibre.

theorem exists_specializes_spacePointMap_eq
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hU : IsAlgebraicSpace B S hS U)
    (f : fibredCategory B S hS U ⟶ 𝒳)
    (hf : HasPropertyOnSomeSmoothDiagram B S hS
      (fun _ _ h => Space.IsSmooth B S hS h) f)
    {x x' : points B S hS 𝒳.val 𝒳.property} (hxx' : x' ⤳ x)
    (hx' : ∃ p : FieldValuedPoint B S hS 𝒳.val,
      pointClass B S hS 𝒳.val 𝒳.property p = x' ∧
        IsQuasiCompactFieldValuedPoint B S hS 𝒳 p)
    (u : Space.points B S hS U) (hu : spacePointMap B S hS U 𝒳 f.hom u = x) :
    ∃ u' : Space.points B S hS U, u' ⤳ u ∧
      spacePointMap B S hS U 𝒳 f.hom u' = x'
Sources
LeanAlgebraicGeometry.Stack.exists_specializes_spacePointMap_eq

Section101.48 Decent algebraic stacks#

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

Tag 0GW1, a definition

Tag 0GW1 in the Stacks Project.

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

A category fibred in groupoids over the big fppf site of S — in particular an algebraic stack — is decent when every one of its points admits a quasi-compact field-valued representative.

abbrev IsDecent : Prop
Tag 0GW2, a lemma

Tag 0GW2 in the Stacks Project.

AlgebraicGeometry.Stack.isDecent_of_isQuasiCompact_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactDiagonalDecent.lean, line 88. The attribute's comment: “quasi-compact diagonal”.

An algebraic stack whose absolute diagonal is quasi-compact is decent.

theorem isDecent_of_isQuasiCompact_diagonal
    (hZ : B.Contains (⊤_ Scheme.{u})) (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hΔ : IsQuasiCompactMorphism.{u, w} B (⊤_ Scheme.{u}) hZ
      (relativeDiagonalAlgebraicStacks B (⊤_ Scheme.{u}) hZ
        (structureMorphism B (⊤_ Scheme.{u}) hZ
          (AlgebraicStacks.viewOverIntegers B S hS hZ 𝒳)))) :
    IsDecent B S hS 𝒳.val

AlgebraicGeometry.Stack.isDecent_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiSeparatedDecent.lean, line 44. The attribute's comment: “quasi-separated case”.

A quasi-separated algebraic stack is decent. If 𝒳 is quasi-separated in the absolute sense, then every point of 𝒳 has a field-valued representative which is quasi-compact.

theorem isDecent_of_isQuasiSeparated (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒳) :
    IsDecent B S hS 𝒳.val
Tag 0GW3, a lemma

Tag 0GW3 in the Stacks Project.

AlgebraicGeometry.Stack.isDecent_of_representable_or_quasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableDecent.lean, line 445.

Stacks 0GW3. The source of a 1-morphism of algebraic stacks over S with decent target is decent as soon as the 1-morphism is representable by schemes, or is representable by algebraic spaces and quasi-separated.

The argument is the source's. Fix a point x of 𝒳; decency of 𝒴 supplies a quasi-compact field-valued representative q of the image of x, and the 1-morphism g : Spec k ⟶ 𝒴 it determines is quasi-compact (Stacks 050T). Form the 2-fibre product P of g and f (Stacks 04T2); its second projection is quasi-compact as a base change of g (Stacks 050V), and by Stacks 04XH the pair consisting of the point of Spec k named by q and of x lifts to a point w of P. Any field-valued representative p of w then has quasi-compact 1-morphism — in the representable case because P is the stack of a scheme, in the quasi-separated case because the composite of that 1-morphism with the first projection is quasi-compact and the first projection is quasi-separated, so Stacks 050Y cancels it — and the field-valued point of 𝒳 it induces represents x with quasi-compact 1-morphism by Stacks 050W.

Unlike the source, no appeal to Stacks 0DTK is needed: the representative is chosen downstream rather than tested, so only the existential form of decency is ever used.

theorem isDecent_of_representable_or_quasiSeparated
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (h𝒴 : IsDecent B S hS 𝒴.val)
    (hf : Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳.val.val.p 𝒴.val.val.p
        (CatFiberedInGroupoids.homFunctor f.hom) ∨
      (IsRepresentableByAlgebraicSpaces B S hS f.hom.hom ∧
        AlgebraicStacks.IsQuasiSeparated B S hS f)) :
    IsDecent B S hS 𝒳.val
Tag 0GW4, a lemma

Tag 0GW4 in the Stacks Project.

AlgebraicGeometry.Stack.isDecent_of_isQuasiCompactMorphism_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactSurjectiveDecent.lean, line 127.

Stacks 0GW4. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. If f is quasi-compact and surjective and 𝒳 is decent, then 𝒴 is decent.

Let y be a point of 𝒴. Surjectivity of f is surjectivity of the map on points (Stacks 04ZS), so y is the image of a point x of 𝒳, and decency of 𝒳 supplies a field-valued representative p of x whose 1-morphism Spec k ⟶ 𝒳 is quasi-compact (Stacks 050T). The image field-valued point f ∘ p has the same base, represents y, and its 1-morphism is the composite of that of p with f, hence quasi-compact by Stacks 050W.

theorem isDecent_of_isQuasiCompactMorphism_of_isSurjective
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsQuasiCompactMorphism.{u, w} B S hS f)
    (hsurj : IsSurjective.{u, w} B S hS f)
    (h𝒳 : IsDecent B S hS 𝒳.val) :
    IsDecent B S hS 𝒴.val
Tag 0GW5, a lemma

Tag 0GW5 in the Stacks Project.

AlgebraicGeometry.Stack.isDecent_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeDecent.lean, line 109.

Stacks 0GW5. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. If f exhibits 𝒳 as a gerbe over 𝒴 (Stacks 06QC) and 𝒳 is decent (Stacks 0GW1), then 𝒴 is decent.

By Stacks 06R9 f is a universal homeomorphism (Stacks 0CI7), hence quasi-compact, through AlgebraicGeometry.Stack.isQuasiCompactMorphism_of_universalHomeomorphism; surjectivity of f comes from the gerbe condition directly, by the surjectivity clause of Stacks 06QI. With both in hand the conclusion is Stacks 0GW4.

theorem isDecent_of_isGerbeOver
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsGerbeOver.{u, w} B S hS f)
    (h𝒳 : IsDecent B S hS 𝒳.val) :
    IsDecent B S hS 𝒴.val
Sources
LeanAlgebraicGeometry.Stack.IsDecent · AlgebraicGeometry.Stack.isDecent_of_isQuasiCompact_diagonal · AlgebraicGeometry.Stack.isDecent_of_isQuasiSeparated · AlgebraicGeometry.Stack.isDecent_of_representable_or_quasiSeparated · AlgebraicGeometry.Stack.isDecent_of_isQuasiCompactMorphism_of_isSurjective · AlgebraicGeometry.Stack.isDecent_of_isGerbeOver

Section101.49 Points on decent stacks#

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

Tag 0GW7, a lemma

Tag 0GW7 in the Stacks Project.

AlgebraicGeometry.Stack.t0Space_points_of_isDecent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DecentStackKolmogorov.lean, line 130.

Stacks 0GW7. The space of points of a decent algebraic stack over S is Kolmogorov: two points of |𝒳| with the same open neighbourhoods are equal.

Two such points x₁, x₂ have the same closure C, and x₁, x₂ ∈ C. Choose a smooth chart φ : |U| → |𝒳| by a scheme, surjective on points, and inside the nonempty closed set φ ⁻¹' C choose a point u maximal for specialization, which the sobriety of |U| provides. Decency feeds Stacks 0GVZ the quasi-compact field-valued representative it asks for, so every specialization x' ⤳ φ u with x' ∈ C lifts to a specialization u' ⤳ u with u' ∈ φ ⁻¹' C; maximality of u forces u' = u and hence x' = φ u. Applied to x₁ and to x₂, both of which specialize to φ u because φ u ∈ C, this gives x₁ = φ u = x₂.

theorem t0Space_points_of_isDecent
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (hdecent : IsDecent B S hS 𝒳) :
    T0Space (points B S hS 𝒳.val 𝒳.property)
Tag 0GW8, a lemma

Tag 0GW8 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.stacksSober_and_isLocallyNoetherianSpace_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DecentStackSober.lean, line 76.

Stacks 0GW8. The space of points of Stacks 04XL of a decent, locally Noetherian algebraic stack over S is a sober, locally Noetherian topological space.

Soberness is Kolmogorov together with quasi-soberness. The Kolmogorov half is Stacks 0GW7, which decency supplies; the quasi-sober half is Stacks 0GVX and local Noetherianity of the space is Stacks 0DQI, part (1), both from the locally Noetherian smooth chart of Stacks 04YF.

theorem stacksSober_and_isLocallyNoetherianSpace_points
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (hdecent : Stack.IsDecent B S hS 𝒳.val)
    (hN : Stack.HasPropertyOnSomeSchemeAtlas B S hS
      (fun X : Scheme.{u} => IsLocallyNoetherian X) 𝒳) :
    StacksSober (Stack.points B S hS 𝒳.val.val 𝒳.val.property) ∧
      IsLocallyNoetherianSpace (Stack.points B S hS 𝒳.val.val 𝒳.val.property)
Tag 0GW9, a proposition

Tag 0GW9 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.stacksSober_points_of_isDecent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DecentStackSoberInertia.lean, line 140.

Stacks 0GW9. Let 𝒳 be a decent algebraic stack over S such that the inertia projection I_𝒳 ⟶ 𝒳 is quasi-compact. Then the space of points |𝒳| is sober.

theorem stacksSober_points_of_isDecent (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hd : IsDecent B S hS 𝒳.val)
    (hqc : IsQuasiCompactMorphism.{u, w} B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳)) :
    @StacksSober (AlgebraicStacks.points B S hS 𝒳) (pointTopology B S hS 𝒳.val)
Sources
LeanAlgebraicGeometry.Stack.t0Space_points_of_isDecent · AlgebraicGeometry.Stack.AlgebraicStacks.stacksSober_and_isLocallyNoetherianSpace_points · AlgebraicGeometry.Stack.AlgebraicStacks.stacksSober_points_of_isDecent

Section101.50 Integral algebraic stacks#

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

Tag 0GWB, a definition

Tag 0GWB in the Stacks Project.

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

An algebraic stack 𝒳 over S is integral when it is reduced, it is decent, its inertia projection I_𝒳 ⟶ 𝒳 is quasi-compact, and its space of points |𝒳| is irreducible.

abbrev IsIntegral (𝒳 : AlgebraicStacks.{u, w} B S hS) : Prop
Tag 0GWC, a lemma

Tag 0GWC in the Stacks Project.

AlgebraicGeometry.Stack.stacksSober_and_exists_openSubstack_isGerbeOver_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IntegralAlgebraicStackStructure.lean, line 266.

Stacks 0GWC. Let 𝒳 be an integral algebraic stack over S (Stacks 0GWB). Then 1. |𝒳| is sober (Stacks 004X), irreducible, and has a unique generic point; 2. there is an open substack 𝒰 ⊆ 𝒳 which is a gerbe over an integral scheme U: a 1-morphism from 𝒰 to the algebraic stack of U making 𝒰 a gerbe over it (Stacks 06QC).

The two parts are AlgebraicGeometry.Stack.stacksSober_irreducibleSpace_existsUnique_isGenericPoint_of_isIntegral and AlgebraicGeometry.Stack.exists_openSubstack_isGerbeOver_isIntegral.

theorem stacksSober_and_exists_openSubstack_isGerbeOver_of_isIntegral
    (𝒳 : AlgebraicStacks.{u, w} B S hS) (h𝒳 : IsIntegral B S hS 𝒳) :
    (letI := pointTopology B S hS 𝒳.val;
      StacksSober (AlgebraicStacks.points B S hS 𝒳) ∧
        IrreducibleSpace (AlgebraicStacks.points B S hS 𝒳) ∧
          ∃! x : AlgebraicStacks.points B S hS 𝒳, IsGenericPoint x Set.univ) ∧
      ∃ (𝒰 : OpenSubstack 𝒳) (U : BigFppfOver B S hS),
        AlgebraicGeometry.IsIntegral ((BigFppfOver.toScheme B S hS).obj U) ∧
          ∃ f : 𝒰.toAlgebraicStack ⟶ schemeStack.{u, w} B S hS U,
            AlgebraicStacks.IsGerbeOver B S hS f
Tag 0GWD, a lemma

Tag 0GWD in the Stacks Project.

AlgebraicGeometry.Stack.isIntegral_of_isReducedStack_of_isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IntegralQuasiSeparatedStack.lean, line 198.

Stacks 0GWD. An algebraic stack 𝒳 over S which is reduced and quasi-separated and whose space of points |𝒳| is irreducible is integral in the sense of Stacks 0GWB.

Two of the four conditions of Stacks 0GWB are hypotheses. Decency is Stacks 0GW2 for a quasi-separated algebraic stack. Quasi-compactness of the inertia projection I_𝒳 ⟶ 𝒳 holds because that 1-morphism is the base change of the absolute diagonal Δ : 𝒳 ⟶ 𝒳 × 𝒳 along itself, and Δ is quasi-compact since 𝒳 is quasi-separated.

theorem isIntegral_of_isReducedStack_of_isAbsolutelyQuasiSeparated
    (hZ : B.Contains (⊤_ Scheme.{u})) (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hred : IsReducedStack.{u, w} B S hS 𝒳)
    (hqs : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒳)
    (hirr : @IrreducibleSpace (points B S hS 𝒳.val.val 𝒳.val.property)
      (pointTopology B S hS 𝒳.val)) :
    IsIntegral.{u, w} B S hS 𝒳
Tag 0GWE, a lemma

Tag 0GWE in the Stacks Project.

AlgebraicGeometry.Stack.bijective_pointClosure_and_bijective_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IntegralClosedSubstack.lean, line 114.

Stacks 0GWE. Let 𝒳 be a decent algebraic stack over S whose inertia projection I_𝒳 ⟶ 𝒳 is quasi-compact. Then the map x ↦ closure {x} from the points of 𝒳 to the irreducible closed subsets of |𝒳| is bijective, and so is the map 𝒵 ↦ |𝒵| from the integral closed substacks of 𝒳 to the irreducible closed subsets of |𝒳|.

theorem bijective_pointClosure_and_bijective_support
    (hd : IsDecent B S hS 𝒳.val)
    (hqc : IsQuasiCompactMorphism.{u, w} B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳)) :
    Function.Bijective (pointClosure B S hS 𝒳) ∧
      Function.Bijective (IntegralClosedSubstack.support (𝒳 := 𝒳))
Sources
LeanAlgebraicGeometry.Stack.IsIntegral · AlgebraicGeometry.Stack.stacksSober_and_exists_openSubstack_isGerbeOver_of_isIntegral · AlgebraicGeometry.Stack.isIntegral_of_isReducedStack_of_isAbsolutelyQuasiSeparated · AlgebraicGeometry.Stack.bijective_pointClosure_and_bijective_support

Section101.51 Residual gerbes#

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

Tag 0H24, a lemma

Tag 0H24 in the Stacks Project.

AlgebraicGeometry.Stack.hasSingletonPointMonomorphism_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeResidualGerbe.lean, line 122. The attribute's comment: “existence clause: condition (1) of Stacks 06MT transports along a gerbe”.

The existence clause of Stacks 0H24. Let f : 𝒳 ⟶ 𝒴 make 𝒳 a gerbe over 𝒴 and let x be a point of 𝒳. If condition (1) of Stacks 06MT holds for 𝒴 at the image of x, then it holds for 𝒳 at x; that is, the residual gerbe of 𝒳 at x exists as soon as the residual gerbe of 𝒴 at f(x) does.

Writing i : 𝒵 ⟶ 𝒴 for the one-point monomorphism over f(x), the witness is the 2-fibre product 𝒳 ×_𝒴 𝒵 with its projection to 𝒳, which is a monomorphism by AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_fst_twoFibreProductSquareAlgebraicStacks. Its projection to 𝒵 is again a gerbe (Stacks 06QE), hence injective on points, and 𝒵 has a single point; so the apex has at most one point, and Stacks 04XH produces one lying over x. The identification of the residual gerbe with that 2-fibre product is not proved.

theorem hasSingletonPointMonomorphism_of_isGerbeOver
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsGerbeOver B S hS f)
    (x : points B S hS 𝒳.val.val (Classical.choose 𝒳.property))
    (hy : HasSingletonPointMonomorphism B S hS 𝒴
      (pointsMap B S hS 𝒳.val.val (Classical.choose 𝒳.property)
        (Classical.choose 𝒴.property) f.hom.hom x)) :
    HasSingletonPointMonomorphism B S hS 𝒳 x

AlgebraicGeometry.Stack.isResidualGerbeAt_inverseImage_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeResidualGerbeFibreProduct.lean, line 110.

Stacks 0H24. Let π : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S making 𝒳 a gerbe over 𝒴, let x be a point of 𝒳 and let y be its image in |𝒴|. Assume the residual gerbe 𝒵_y ⊂ 𝒴 of 𝒴 at y exists, cut out by the object property P of 𝒴 (the specification AlgebraicGeometry.Stack.IsResidualGerbeAt of Stacks 06MT). Then 𝒵_x = 𝒵_y ×_𝒴 𝒳 is the residual gerbe of 𝒳 at x:

  • the inverse image P ∘ π of P meets the residual-gerbe specification of 𝒳 at x, so the residual gerbe 𝒵_x of 𝒳 at x exists and is the strictly full subcategory of 𝒳 on the objects sent into 𝒵_y; and
  • the square formed by the 1-morphism 𝒵_x ⟶ 𝒵_y induced by π, the inclusion 𝒵_x ⟶ 𝒳, and the inclusion 𝒵_y ⟶ 𝒴, which commutes on the nose, is a 2-fibre product: 𝒵_x with its inclusion into 𝒳 is the 2-fibre product 𝒵_y ×_𝒴 𝒳.

Following the source: the inverse image is algebraic and is the 2-fibre product (AlgebraicGeometry.Stack.isAlgebraicStack_inverseImage, AlgebraicGeometry.Stack.isTwoFibreProduct_inverseImageSquare); its projection to 𝒵_y is a base change of π, hence smooth (Stacks 0DN8, Stacks 075W) and a gerbe (Stacks 06QE), so the apex is reduced and locally Noetherian as 𝒵_y is (Stacks 04YF, Stacks 06R6) and has exactly one point, which lies over x (Stacks 04XH and injectivity of a gerbe on points).

theorem isResidualGerbeAt_inverseImage_of_isGerbeOver
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsGerbeOver B S hS f)
    (x : points B S hS 𝒳.val.val (Classical.choose 𝒳.property))
    (P : ObjectProperty 𝒴.val.val.obj)
    (hP : IsResidualGerbeAt B S hS 𝒴
      (pointsMap B S hS 𝒳.val.val (Classical.choose 𝒳.property)
        (Classical.choose 𝒴.property) f.hom.hom x) P) :
    ∃ hQ : IsResidualGerbeAt B S hS 𝒳 x (P.inverseImage f.hom.hom.toFunctor),
      Nonempty (Bicategory.IsTwoFibreProduct
        ({ pt := residualGerbe B S hS 𝒳 x _ hQ
           fst := residualGerbeMap B S hS f hQ.2.choose hP.2.choose (fun _ h => h)
           snd := residualGerbeInclusion B S hS 𝒳 x _ hQ
           iso := Iso.refl _ } :
          Bicategory.TwoCommSq (residualGerbeInclusion B S hS 𝒴 _ P hP) f))
Tag 0H25, a lemma

Tag 0H25 in the Stacks Project.

AlgebraicGeometry.Stack.residualGerbe_factorization_of_isReducedStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ReducedResidualGerbeFactorization.lean, line 269.

A reduced stack over a point factors through the residual gerbe. Let f : 𝒴 ⟶ 𝒳 be a 1-morphism of algebraic stacks over S and let x ∈ |𝒳|. Assume that 1. 𝒳 is decent or locally Noetherian (or both), 2. the inertia projection I_𝒳 ⟶ 𝒳 is quasi-compact, 3. |f|(|𝒴|) is contained in {x}, and 4. 𝒴 is reduced.

Then the residual gerbe 𝒵_x of 𝒳 at x exists and f factors through it. Precisely: * the residual gerbe of 𝒳 at x exists: some reduced algebraic stack admits a monomorphism to 𝒳 whose space of points is a single point lying over x; * f factors, up to a 2-isomorphism, through every monomorphism 𝒵 ⟶ 𝒳 from an algebraic stack with a single point lying over x, in particular through every residual gerbe so presented; * f factors strictly through the inclusion of every residual gerbe of 𝒳 at x, the strictly full subcategory residualGerbe.

theorem residualGerbe_factorization_of_isReducedStack
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒴 ⟶ 𝒳) (x : AlgebraicStacks.points B S hS 𝒳)
    (h1 : IsDecent B S hS 𝒳.val ∨ IsLocallyNoetherianStack B S hS 𝒳)
    (h2 : IsQuasiCompactMorphism.{u, w} B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳))
    (h3 : Set.range (AlgebraicStacks.pointsMap B S hS f) ⊆ {x})
    (h4 : IsReducedStack B S hS 𝒴) :
    HasReducedSingletonPointMonomorphism B S hS 𝒳 x ∧
      (∀ (𝒵 : AlgebraicStacks.{u, w} B S hS) (m : 𝒵 ⟶ 𝒳),
        AlgebraicStacks.IsMonomorphism B S hS m → HasUniquePointOver B S hS m x →
          ∃ g : 𝒴 ⟶ 𝒵, Nonempty (g ≫ m ≅ f)) ∧
      ∀ (P : ObjectProperty 𝒳.val.val.obj) (hP : IsResidualGerbeAt B S hS 𝒳 x P),
        ∃ g : 𝒴 ⟶ residualGerbe B S hS 𝒳 x P hP,
          g ≫ residualGerbeInclusion B S hS 𝒳 x P hP = f
Tag 0H26, a lemma

Tag 0H26 in the Stacks Project.

AlgebraicGeometry.Stack.factorsThroughSubstack_residualGerbe_of_isClosed_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ResidualGerbeClosedPointFactorization.lean, line 123. The attribute's comment: “the closed-point case the remark asserts: for X locally Noetherian and x a closed point, f : Y -> X with Y reduced and |f|(|Y|) in {x} factors through the residual gerbe at x, which exists (via 0H27). The remark's open question, whether Lemma 0H25 holds for every point of a locally Noetherian X without the quasi-compact inertia hypothesis, is NOT asserted”.

Stacks 0H26, the closed-point case. Let 𝒳 be a locally Noetherian algebraic stack over S, let x ∈ |𝒳| be a closed point, and let f : 𝒴 ⟶ 𝒳 be a 1-morphism of algebraic stacks with 𝒴 reduced and |f|(|𝒴|) ⊆ {x}. Then the residual gerbe 𝒵_x of 𝒳 at x exists and f factors through it: every object property of 𝒳 cutting out a residual gerbe at x is one f factors through.

This is the conclusion of Stacks 0H25 with its quasi-compact-inertia hypothesis dropped, which the remark says is true at a closed point because of Stacks 0H27. The remark's open question, whether the conclusion holds at every point of a locally Noetherian 𝒳, is not asserted.

The residual gerbe is the reduced closed substack on {x} (Stacks 0509), which is a residual gerbe at x as in the proof of Stacks 0H27; every residual gerbe at x has closed immersion inclusion by Stacks 0H27, so f factors through it by Stacks 050B.

theorem factorsThroughSubstack_residualGerbe_of_isClosed_singleton
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (h𝒳 : IsLocallyNoetherianStack B S hS 𝒳)
    (x : AlgebraicStacks.points B S hS 𝒳)
    (hx : @IsClosed _ (pointTopology B S hS 𝒳.val) {x})
    (f : 𝒴 ⟶ 𝒳) (hf : Set.range (AlgebraicStacks.pointsMap B S hS f) ⊆ {x})
    (hred : IsReducedStack B S hS 𝒴) :
    (∃ P : ObjectProperty 𝒳.val.val.obj, IsResidualGerbeAt B S hS 𝒳 x P) ∧
      ∀ P : ObjectProperty 𝒳.val.val.obj, IsResidualGerbeAt B S hS 𝒳 x P →
        FactorsThroughSubstack f P
Tag 0H27, a lemma

Tag 0H27 in the Stacks Project.

AlgebraicGeometry.Stack.exists_isResidualGerbeAt_and_isClosed_singleton_iff_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ResidualGerbeClosedPoint.lean, line 127.

Stacks 0H27. Let 𝒳 be a locally Noetherian algebraic stack over S and x ∈ |𝒳|. The residual gerbe 𝒵_x ⊂ 𝒳 of 𝒳 at x exists (Stacks 0H22), and for it, x is a closed point of |𝒳| if and only if the inclusion 𝒵_x ⟶ 𝒳 is a closed immersion.

The residual gerbe is the strictly full subcategory cut out by an object property meeting the specification AlgebraicGeometry.Stack.IsResidualGerbeAt (Stacks 06MU), which is unique by AlgebraicGeometry.Stack.eq_of_isResidualGerbeAt_of_bootstrap; the equivalence is AlgebraicGeometry.Stack.isClosed_singleton_iff_isClosedImmersion_residualGerbeInclusion.

theorem exists_isResidualGerbeAt_and_isClosed_singleton_iff_isClosedImmersion
    (𝒳 : AlgebraicStacks.{u, w} B S hS) (h𝒳 : IsLocallyNoetherianStack B S hS 𝒳)
    (x : AlgebraicStacks.points B S hS 𝒳) :
    ∃ (P : ObjectProperty 𝒳.val.val.obj) (hP : IsResidualGerbeAt B S hS 𝒳 x P),
      (@IsClosed _ (pointTopology B S hS 𝒳.val) {x} ↔
        AlgebraicStacks.IsClosedImmersion B S hS (residualGerbeInclusion B S hS 𝒳 x P hP))
Sources
LeanAlgebraicGeometry.Stack.hasSingletonPointMonomorphism_of_isGerbeOver · AlgebraicGeometry.Stack.isResidualGerbeAt_inverseImage_of_isGerbeOver · AlgebraicGeometry.Stack.residualGerbe_factorization_of_isReducedStack · AlgebraicGeometry.Stack.factorsThroughSubstack_residualGerbe_of_isClosed_singleton · AlgebraicGeometry.Stack.exists_isResidualGerbeAt_and_isClosed_singleton_iff_isClosedImmersion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.