100.3 Properties of morphisms… to 100.10 Reduced algebraic stacks

Section100.3 Properties of morphisms representable by algebraic spaces#

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

Tag 04XB, the section

Tag 04XB in the Stacks Project.

AlgebraicGeometry.Stack.UniversallyOpen, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniversallyOpenCriterion.lean, line 143. The attribute's comment: “RESTRICTED: the section's relative property at universal openness”.

A 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces is universally open when every algebraic space representing its base change along a scheme-valued point of the target has universally open structural morphism, read as a morphism of algebraic spaces over S. This is the notion of Stacks 04XB for AlgebraicGeometry.Space.UniversallyOpen, and it is the condition Stacks 06U1 part (1) names.

It is not AlgebraicGeometry.Stack.AlgebraicStacks.UniversallyOpen, which is Stacks 06U2 part (2) and tests openness of base changes on the topological spaces of points; the equivalence of the two is Stacks 06U1.

abbrev UniversallyOpen {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴) : Prop
Tag 04ZP, a lemma

Tag 04ZP in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_iff_isRepresentableByAlgebraicSpace_pt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableBySpacesOfFppfCover.lean, line 271.

Stacks 04ZP. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S, let 𝒲 be represented by an algebraic space W and let g : 𝒲 ⟶ 𝒴 be surjective, flat and locally of finite presentation. Then f is representable by algebraic spaces if and only if the apex W ×_𝒴 𝒳 of a 2-fibre product square over the cospan (g, f) is represented by an algebraic space.

The implication (1) ⟹ (2) is Stacks 0300, AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isTwoFibreProduct, which needs none of the hypotheses on g; the converse is AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_of_isTwoFibreProduct_of_bootstrap.

theorem isRepresentableByAlgebraicSpaces_iff_isRepresentableByAlgebraicSpace_pt
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS}
    (𝒲 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒲 : IsRepresentableByAlgebraicSpace B S hS 𝒲)
    (f : 𝒳 ⟶ 𝒴) (g : 𝒲 ⟶ 𝒴.val)
    (hg : ∀ (V : BigFppfOver B S hS)
      (yv : BigFppfOver B V.left.1 V.left.2 ⥤ 𝒴.val.val.obj)
      (_hyv : yv ⋙ 𝒴.val.val.p = Over.map V.hom)
      (F : (BigFppfOver B V.left.1 V.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B V.left.1 V.left.2 F),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map V.hom) 𝒲.val.p 𝒴.val.val.p yv
          (CatFiberedInGroupoids.homFunctor g))
        (presheafOfCategories (F ⋙ typeToCat)).p) →
      (let h := (algebraicSpaceMap B S hS V
        ((spacesOverSmallerBaseFunctor B V.left.1 S V.left.2 hS V.hom).obj ⟨F, hF⟩)).hom
       Space.IsSurjective B S hS h ∧ Space.IsFlat B S hS h ∧
         Space.IsLocallyOfFinitePresentation B S hS h))
    (Q : Bicategory.TwoCommSq g f.hom) (hQ : Bicategory.IsTwoFibreProduct Q) :
    IsRepresentableByAlgebraicSpaces B S hS f.hom.hom ↔
      IsRepresentableByAlgebraicSpace B S hS Q.pt

AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_of_isRepresentableByAlgebraicSpace_pt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableOfFlatCoverBaseChange.lean, line 101. The attribute's comment: “the implication (2) ⟹ (1)”.

Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S, let g : 𝒲 ⟶ 𝒴 be surjective, flat and locally of finite presentation with 𝒲 an algebraic space, and suppose a 2-fibre product 𝒲 ×_𝒴 𝒳 of the cospan (g, f) is an algebraic space. Then f is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_of_isRepresentableByAlgebraicSpace_pt
    {𝒳 𝒴 𝒲 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒲 ⟶ 𝒴)
    (h𝒲 : IsRepresentableByAlgebraicSpace B S hS 𝒲.val)
    (hSurj : IsSurjective B S hS g) (hFlat : AlgebraicStacks.IsFlat B S hS g)
    (hLfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (Q : Bicategory.TwoCommSq g f) (hQ : Bicategory.IsTwoFibreProduct Q)
    (hQpt : IsRepresentableByAlgebraicSpace B S hS Q.pt.val) :
    IsRepresentableByAlgebraicSpaces B S hS f.hom.hom

Declarations registered for the tag:

Tag 04XC, a lemma

Tag 04XC in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_iff_forall_space_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertySpaceBaseChange.lean, line 265.

Stacks 04XC. A 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces has the relative property P exactly when, for every 2-fibre product square over a 1-morphism out of a stack representable by an algebraic space, the morphism of representing presheaves induced by the first projection of that square has P as a morphism of algebraic spaces over S.

The chosen representing equivalences are universally quantified, so the condition does not depend on them; and algebraicity of 𝒳 and 𝒴 is not needed, only representability of f by algebraic spaces.

theorem hasRelativeProperty_iff_forall_space_baseChange :
    HasRelativeProperty B S hS P f hf ↔
      ∀ (𝒵 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
        (_h𝒵 : IsRepresentableByAlgebraicSpace B S hS 𝒵)
        (g : 𝒵 ⟶ 𝒴) (Q : Bicategory.TwoCommSq g f)
        (_hQ : Bicategory.IsTwoFibreProduct Q)
        (F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
        (eF : StacksRepresentableCFG.EquivalenceOver
          Q.pt.val.p (presheafOfCategories (F ⋙ typeToCat)).p)
        (eG : StacksRepresentableCFG.EquivalenceOver
          𝒵.val.p (presheafOfCategories (G ⋙ typeToCat)).p),
        P (ObjectProperty.homMk (representingMap B S hS Q.pt 𝒵 F G eF eG Q.fst) :
          (⟨F, hF⟩ : AlgebraicSpaces B S hS) ⟶ (⟨G, hG⟩ : AlgebraicSpaces B S hS))
Tag 04XD, a lemma

Tag 04XD in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_iff_prop_representingMap_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalEssentialSurjectivity.lean, line 493.

Properties of Stacks, Lemma 04XD. In the situation above, f has the relative property P of Stacks 03YK exactly when the morphism V ⟶ W of representing presheaves induced by the first projection of the square has P as a morphism of algebraic spaces over S.

The forward implication is Stacks 04XC and uses no hypothesis on g; the backward one is AlgebraicGeometry.Stack.hasRelativeProperty_of_prop_representingMap_of_fppf.

theorem hasRelativeProperty_iff_prop_representingMap_of_fppf
    (P : MorphismProperty (AlgebraicSpaces B S hS)) [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage.{u, max u t} B S hS)]
    (𝒳 𝒴 𝒲 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (f : 𝒳 ⟶ 𝒴) (g : 𝒲 ⟶ 𝒴) (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hgr : IsRepresentableByAlgebraicSpaces B S hS g.hom)
    (hg : ∀ (V : BigFppfOver B S hS)
      (yv : BigFppfOver B V.left.1 V.left.2 ⥤ 𝒴.val.obj)
      (_hyv : yv ⋙ 𝒴.val.p = Over.map V.hom)
      (F : (BigFppfOver B V.left.1 V.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B V.left.1 V.left.2 F),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map V.hom) 𝒲.val.p 𝒴.val.p yv
          (CatFiberedInGroupoids.homFunctor g))
        (presheafOfCategories (F ⋙ typeToCat)).p) →
      (let h := (algebraicSpaceMap B S hS V
        ((spacesOverSmallerBaseFunctor B V.left.1 S V.left.2 hS V.hom).obj ⟨F, hF⟩)).hom
       Space.IsSurjective B S hS h ∧ Space.IsFlat B S hS h ∧
         Space.IsLocallyOfFinitePresentation B S hS h))
    (Q : Bicategory.TwoCommSq g f) (hQ : Bicategory.IsTwoFibreProduct Q)
    (V W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hV : IsAlgebraicSpace B S hS V) (hW : IsAlgebraicSpace B S hS W)
    (eV : StacksRepresentableCFG.EquivalenceOver
      Q.pt.val.p (presheafOfCategories (V ⋙ typeToCat)).p)
    (eW : StacksRepresentableCFG.EquivalenceOver
      𝒲.val.p (presheafOfCategories (W ⋙ typeToCat)).p) :
    HasRelativeProperty.{u, u, u + 1, max u t} B S hS P f hf ↔
      P (ObjectProperty.homMk (representingMap B S hS Q.pt 𝒲 V W eV eW Q.fst) :
        (⟨V, hV⟩ : AlgebraicSpaces B S hS) ⟶ (⟨W, hW⟩ : AlgebraicSpaces B S hS))
Tag 06TY, a lemma

Tag 06TY in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_iff_of_fppfCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyFppfCover.lean, line 102.

Let P be a property of morphisms of algebraic spaces over S which is stable under base change and local on the target for the fppf precoverage, let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S representable by algebraic spaces, and let g : 𝒵 ⟶ 𝒴 be representable by algebraic spaces, surjective, flat and locally of finite presentation. Then f has the relative property P of Stacks 03YK if and only if the projection to 𝒵 of a 2-fibre product of the cospan (g, f) has it.

theorem hasRelativeProperty_iff_of_fppfCover
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage.{u, u} B S hS)]
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hg : IsRepresentableByAlgebraicSpaces B S hS g.hom.hom)
    (hSurj : IsSurjective B S hS g)
    (hFlat : AlgebraicStacks.IsFlat B S hS g)
    (hLfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (Q : Bicategory.TwoCommSq g f)
    (hQ : Bicategory.IsTwoFibreProduct Q) :
    HasRelativeProperty B S hS P f.hom hf ↔
      ∃ hfst : IsRepresentableByAlgebraicSpaces B S hS Q.fst.hom.hom,
        HasRelativeProperty B S hS P Q.fst.hom hfst
Tag 06M2, a lemma

Tag 06M2 in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_of_comp_of_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyCancelSourceLocal.lean, line 879.

A relative property local on the source descends along a representable covering of the intermediate fibred category.

public theorem hasRelativeProperty_of_comp_of_cover
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty (AlgebraicGeometry.AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (AlgebraicGeometry.Space.Topology.fppf.precoverage B S hS)]
    (τ : AlgebraicGeometry.Space.Topology)
    (hτ : τ = .etale ∨ τ = .smooth ∨ τ = .syntomic ∨ τ = .fppf)
    [P.IsLocalAtSource (τ.precoverage B S hS)]
    {𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, v, u + 1, w}
      (AlgebraicGeometry.BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : AlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hg : AlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpaces B S hS g.hom)
    (hcover :
      ∀ (U : AlgebraicGeometry.BigFppfOver B S hS)
        (y : AlgebraicGeometry.BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.based.obj)
        (_hy : y ⋙ 𝒴.based.p = Over.map U.hom)
        (F : (AlgebraicGeometry.BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hF : AlgebraicGeometry.IsAlgebraicSpace B U.left.1 U.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.based.p 𝒴.based.p y
            (CatFiberedInGroupoids.homFunctor f))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        let a := AlgebraicGeometry.algebraicSpaceMap B S hS U
          ((AlgebraicGeometry.spacesOverSmallerBaseFunctor B U.left.1 S U.left.2
            hS U.hom).obj ⟨F, hF⟩)
        (AlgebraicGeometry.Space.IsSurjective B S hS a.hom ∧
          (match τ with
          | .etale => AlgebraicGeometry.Space.IsEtale B S hS a.hom
          | .smooth => AlgebraicGeometry.Space.IsSmooth B S hS a.hom
          | .syntomic => AlgebraicGeometry.Space.IsSyntomic B S hS a.hom
          | .fppf =>
              AlgebraicGeometry.Space.IsFlat B S hS a.hom ∧
                AlgebraicGeometry.Space.IsLocallyOfFinitePresentation B S hS a.hom
          | .fpqc => False)))
    (hcomp : AlgebraicGeometry.Stack.HasRelativeProperty B S hS P (f ≫ g)
      (AlgebraicGeometry.isRepresentableByAlgebraicSpaces_comp B S hS f g hf hg)) :
    AlgebraicGeometry.Stack.HasRelativeProperty B S hS P g hg
Tag 04Y6, a lemma

Tag 04Y6 in the Stacks Project.

AlgebraicGeometry.Stack.GroupoidPresentation.pr, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresentationBaseChangeProjection.lean, line 454. The attribute's comment: “assertion (3): the morphism of groupoids pr : (U', R', s', t', c') ⟶ (U, R, s, t, c)”.

Stacks 04Y6, assertion (3). The morphism of groupoids in algebraic spaces pr : (U', R', s', t', c') ⟶ (U, R, s, t, c): on objects the projection U' = U ×_𝒳 𝒳' ⟶ U, on arrows the map carrying (u₁, x₁, ψ₁), (u₂, x₂, ψ₂), φ to (u₁, u₂, ψ₁ ≫ g(φ) ≫ ψ₂⁻¹). The identity clause is not a hypothesis of AlgebraicGeometry.GroupoidInAlgebraicSpaces.Hom.mk', and the two clauses over the base are free, the base being final.

noncomputable def pr : GroupoidInAlgebraicSpaces.Hom
    (baseChangedPresentation P g h𝒳 h𝒳' eU' eR').groupoid P.groupoid

AlgebraicGeometry.Stack.GroupoidPresentation.quotientStackPr, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresentationBaseChangeProjection.lean, line 475. The attribute's comment: “assertion (3): the induced morphism [pr] of quotient stacks”.

Stacks 04Y6, assertion (3). The 1-morphism [pr] : [U'/R'] ⟶ [U/R] of quotient stacks induced by pr through Stacks 046Q.

noncomputable def quotientStackPr :
    BasedFunctor (quotientStack (baseChangedPresentation P g h𝒳 h𝒳' eU' eR').groupoid)
      (quotientStack P.groupoid)

AlgebraicGeometry.Stack.GroupoidPresentation.exists_baseChangedPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresentationBaseChangeRelation.lean, line 164. The attribute's comment: “assertions (1) and (2): a groupoid of the form (U', R', s', t', c') and a presentation [U'/R'] -> X'; the 2-commutative square of assertions (3) and (4) is not claimed”.

Let g : 𝒳' ⟶ 𝒳 be a 1-morphism of algebraic stacks over S representable by algebraic spaces and let [U/R] ⟶ 𝒳 be a presentation. Then there is a presentation [U'/R'] ⟶ 𝒳' whose presenting groupoid is of the form (U', R', s', t', c'): its object space represents U' = U ×_𝒳 𝒳' and its arrow space represents R' = R ×_𝒳 𝒳', where R is the self-intersection U ×_𝒳 U of the atlas.

theorem exists_baseChangedPresentation
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (h𝒳' : IsAlgebraicStack.{u, w} B S hS 𝒳'.val)
    (hg : IsRepresentableByAlgebraicSpaces B S hS g.hom) :
    ∃ (P' : GroupoidPresentation B S hS 𝒳'.val),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (baseChangedAtlasSquare P g).pt.val.p
        (presheafOfCategories (P'.groupoid.objects.obj ⋙ typeToCat)).p) ∧
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (atlasRelationBaseChangeSquare P g).pt.val.p
        (presheafOfCategories (P'.groupoid.arrows.obj ⋙ typeToCat)).p)

AlgebraicGeometry.Stack.GroupoidPresentation.nonempty_bcSquareIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresentationBaseChangeSquare.lean, line 1060. The attribute's comment: “assertion (4): the square [U'/R'] -> X' -> X and [U'/R'] -> [U/R] -> X 2-commutes”.

Stacks 04Y6, assertion (4). The square

[U'/R'] ---ε'---> 𝒳'
   |               |
  [pr]             g
   v               v
 [U/R] ----ε----> 𝒳

2-commutes: the presenting 1-morphism of the base-changed presentation followed by g is 2-isomorphic, over the big fppf site, to the morphism [pr] of quotient stacks induced by pr followed by the presenting 1-morphism of P.

theorem nonempty_bcSquareIso :
    Nonempty (BasedFunctor.comp
        (baseChangedPresentation P g h𝒳 h𝒳' eU' eR').basedFunctor g.hom ≅
      BasedFunctor.comp (quotientStackPr P g eU' eR' h𝒳 h𝒳') P.basedFunctor)

AlgebraicGeometry.Stack.GroupoidPresentation.exists_baseChangedPresentationSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresentationBaseChangeSquare.lean, line 1095. The attribute's comment: “the whole statement: assertions (1), (2), (3) and (4) conjoined”.

Stacks 04Y6, the whole statement. Let g : 𝒳' ⟶ 𝒳 be a 1-morphism of algebraic stacks over S representable by algebraic spaces and let [U/R] ⟶ 𝒳 be a presentation. Then there are a presentation [U'/R'] ⟶ 𝒳' of the form (U', R', s', t', c') — its object space representing U' = U ×_𝒳 𝒳' and its arrow space representing R' = R ×_𝒳 𝒳' — and a morphism of groupoids pr : (U', R', s', t', c') ⟶ (U, R, s, t, c) for which the square

[U'/R'] ---ε'---> 𝒳'
   |               |
  [pr]             g
   v               v
 [U/R] ----ε----> 𝒳

2-commutes.

The four assertions are AlgebraicGeometry.Stack.GroupoidPresentation.exists_baseChangedPresentation, ...pr, ...quotientStackPr and AlgebraicGeometry.Stack.GroupoidPresentation.nonempty_bcSquareIso; this is their conjunction. The 2-commutativity is a Nonempty of an isomorphism of 1-morphisms over the site, an isomorphism being data while a conjunct must be a proposition — and asserting that a square 2-commutes is asserting that such an isomorphism exists.

theorem exists_baseChangedPresentationSquare
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (h𝒳' : IsAlgebraicStack.{u, w} B S hS 𝒳'.val)
    (hg : IsRepresentableByAlgebraicSpaces B S hS g.hom) :
    ∃ P' : GroupoidPresentation B S hS 𝒳'.val,
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (baseChangedAtlasSquare P g).pt.val.p
        (presheafOfCategories (P'.groupoid.objects.obj ⋙ typeToCat)).p) ∧
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (atlasRelationBaseChangeSquare P g).pt.val.p
        (presheafOfCategories (P'.groupoid.arrows.obj ⋙ typeToCat)).p) ∧
      ∃ pr' : GroupoidInAlgebraicSpaces.Hom P'.groupoid P.groupoid,
        Nonempty (BasedFunctor.comp P'.basedFunctor g.hom ≅
          BasedFunctor.comp (quotientStackMap pr') P.basedFunctor)

CategoryTheory.CatFiberedInGroupoids.RepresentablePresentation.isTwoFibreProduct_relationBaseChangeSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentablePresentationBaseChange.lean, line 168. The attribute's comment: “R' = R ×_𝒳 𝒳' for the canonical squares; no hypothesis carried”.

Stacks 04Y6. The canonical R ×_{s, 𝒰} U' is a base change of the relation R along g: pasted onto the square of U' = 𝒰 ×_𝒳 𝒳', it is a 2-fibre product of the cospan (s ≫ f, g). This is the R' = R ×_𝒳 𝒳' of the statement of the lemma.

noncomputable def isTwoFibreProduct_relationBaseChangeSquare :
    Bicategory.IsTwoFibreProduct
      ((atlasBaseChangeSquare f g).pasteFst (relationBaseChangeSquare f g))

CategoryTheory.CatFiberedInGroupoids.RepresentablePresentation.nonempty_iso_baseChangedRelationSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentablePresentationBaseChange.lean, line 180. The attribute's comment: “R ×_𝒳 𝒳' = U' ×_{𝒳'} U' for the canonical squares; nothing carried”.

Stacks 04Y6. The displayed chain of the proof, for the canonical 2-fibre products: R ×_𝒳 𝒳' = 𝒰 ×_𝒳 𝒰 ×_𝒳 𝒳' = (𝒰 ×_𝒳 𝒳') ×_{𝒳'} (𝒰 ×_𝒳 𝒳'). The base change of the relation and the self-intersection of the base-changed atlas are isomorphic as 2-commutative squares over the triple product, hence compatibly with the projections pr_R and s'.

theorem nonempty_iso_baseChangedRelationSquare :
    Nonempty ((atlasBaseChangeSquare f g).baseChangedSelfIntersection
        (baseChangedRelationSquare f g) ≅
      (relationSquare f).paste (relationBaseChangeSquare f g))
Tag 04ZQ, a remark

Tag 04ZQ in the Stacks Project.

AlgebraicGeometry.Stack.SpacesOverStack, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpacesOverAlgebraicStack.lean, line 59. The attribute's comment: “the objects”.

An object of the 2-category Spaces/𝒴: an algebraic stack over S together with a 1-morphism to 𝒴 which is representable by algebraic spaces.

structure SpacesOverStack
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒴 : AlgebraicStacks.{u, w} B S hS)

AlgebraicGeometry.Stack.SpacesOverStack.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpacesOverAlgebraicStack.lean, line 77. The attribute's comment: “the 1-morphisms”.

A 1-morphism of Spaces/𝒴: a 1-morphism of the source stacks together with a 2-morphism from the structure morphism of the source to its composite with that of the target.

structure Hom (F G : SpacesOverStack B S hS 𝒴)

AlgebraicGeometry.Stack.SpacesOverStack.Hom₂, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpacesOverAlgebraicStack.lean, line 86. The attribute's comment: “the 2-morphisms”.

A 2-morphism of Spaces/𝒴: a 2-morphism of the underlying 1-morphisms of source stacks, compatible with the two comparison 2-morphisms.

structure Hom₂ {F G : SpacesOverStack B S hS 𝒴} (f g : Hom F G)

AlgebraicGeometry.Stack.SpacesOverStack.instCategoryStruct, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpacesOverAlgebraicStack.lean, line 148. The attribute's comment: “composition of 1-morphisms”.

The 1-morphisms of Spaces/𝒴, with their identities and composition.

instance instCategoryStruct : CategoryStruct.{u + 1} (SpacesOverStack B S hS 𝒴)

AlgebraicGeometry.Stack.SpacesOverStack.instHomCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpacesOverAlgebraicStack.lean, line 156. The attribute's comment: “the hom-categories”.

The category of 1-morphisms and 2-morphisms of Spaces/𝒴 between two fixed objects: the hom-category of its 2-category structure.

instance instHomCategory (F G : SpacesOverStack B S hS 𝒴) : Category.{u + 1} (F ⟶ G)

AlgebraicGeometry.Stack.SpacesOverStack.instBicategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpacesOverAlgebraicStack.lean, line 229. The attribute's comment: “the 2-category structure”.

The 2-category Spaces/𝒴 of algebraic spaces over the algebraic stack 𝒴, with the objects SpacesOverStack, the 1-morphisms Hom and the 2-morphisms Hom₂.

instance instBicategory : Bicategory.{u + 1, u + 1} (SpacesOverStack B S hS 𝒴)

AlgebraicGeometry.Stack.SpacesOverStack.isSetoidCategory_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpacesOverAlgebraicStackSetoid.lean, line 136. The attribute's comment: “the hom-categories are setoids”.

Stacks 04ZQ. Every hom-category of Spaces/𝒴 is a setoid in the sense of Stacks 02XZ: it is a groupoid and it is thin, so a 1-morphism of Spaces/𝒴 has no automorphism but the identity. This is the source's claim that the morphism categories Mor_{Spaces/𝒴}((f₁ : 𝒳₁ ⟶ 𝒴), (f₂ : 𝒳₂ ⟶ 𝒴)) are all setoids.

theorem isSetoidCategory_hom (F G : SpacesOverStack B S hS 𝒴) :
    IsSetoidCategory (F ⟶ G)

AlgebraicGeometry.Stack.SpacesOverStack.isoClassCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpacesOverAlgebraicStackSetoid.lean, line 155. The attribute's comment: “the category of isomorphism classes of 1-morphisms”.

Stacks 04ZQ. Replacing the 1-morphisms of Spaces/𝒴 by their isomorphism classes gives a category: the objects are those of Spaces/𝒴, a morphism F ⟶ G is an isomorphism class of 1-morphisms F ⟶ G of the 2-category, and the identities and the composition are induced by those of the 2-category.

Composition descends because whiskering turns a pair of isomorphic 1-morphisms into isomorphic composites, and the three category laws hold because the unitors and the associator of Spaces/𝒴 become equalities of isomorphism classes.

def isoClassCategory : Category.{u + 1} (SpacesOverStack B S hS 𝒴)
Sources
LeanAlgebraicGeometry.Stack.UniversallyOpen · AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_iff_isRepresentableByAlgebraicSpace_pt · AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_of_isRepresentableByAlgebraicSpace_pt · AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isTwoFibreProduct · AlgebraicGeometry.Stack.hasRelativeProperty_iff_forall_space_baseChange · AlgebraicGeometry.Stack.hasRelativeProperty_iff_prop_representingMap_of_fppf · AlgebraicGeometry.Stack.hasRelativeProperty_iff_of_fppfCover · AlgebraicGeometry.Stack.hasRelativeProperty_of_comp_of_cover

Section100.4 Points of algebraic stacks#

Section 100.4 of the Stacks Project, Tag 04XE. 10 tags here are carried by 16 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04XE, the section

Tag 04XE in the Stacks Project.

Declarations registered for the tag:

Tag 04XF, a lemma

Tag 04XF in the Stacks Project.

AlgebraicGeometry.Stack.FieldValuedPoint.hasCommonExtension_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Points.lean, line 250.

Stacks 04XF. Common field-valued refinement is an equivalence relation on the field-valued points of a category fibred in groupoids.

theorem hasCommonExtension_equivalence
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    {𝒳 : BasedCategory.{v, t} (BigFppfOver B S hS)}
    (h𝒳 : 𝒳.p.IsFiberedInGroupoids) :
    Equivalence (HasCommonExtension (𝒳 := 𝒳))
Tag 04XG, a definition

Tag 04XG in the Stacks Project.

AlgebraicGeometry.Stack.points, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Points.lean, line 273.

Stacks 04XG. The points of a category fibred in groupoids, in particular of an algebraic stack, are the equivalence classes of its field-valued points.

abbrev points (h𝒳 : 𝒳.p.IsFiberedInGroupoids) : Type (max (u + 1) t)
Tag 04XH, a lemma

Tag 04XH in the Stacks Project.

AlgebraicGeometry.Stack.exists_point_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsFibreProduct.lean, line 249. The attribute's comment: “for a 2-fibre product of categories fibred in groupoids”.

Points of a 2-fibre product of categories fibred in groupoids: a point of 𝒵 and a point of 𝒳 with the same image in |𝒴| lift to a point of any 2-fibre product of g : 𝒵 ⟶ 𝒴 and f : 𝒳 ⟶ 𝒴.

theorem exists_point_of_isTwoFibreProduct
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒵 𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    {g : 𝒵 ⟶ 𝒴} {f : 𝒳 ⟶ 𝒴}
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (z : points B S hS 𝒵.val 𝒵.property) (x : points B S hS 𝒳.val 𝒳.property)
    (h : pointsMap B S hS 𝒵.val 𝒵.property 𝒴.property g.hom z =
      pointsMap B S hS 𝒳.val 𝒳.property 𝒴.property f.hom x) :
    ∃ p : points B S hS P.pt.val P.pt.property,
      pointsMap B S hS P.pt.val P.pt.property 𝒵.property P.fst.hom p = z ∧
        pointsMap B S hS P.pt.val P.pt.property 𝒳.property P.snd.hom p = x

AlgebraicGeometry.Stack.exists_point_of_isTwoFibreProduct_algebraicStacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsFibreProductAlgebraicStack.lean, line 102.

Stacks 04XH. Let g : 𝒵 ⟶ 𝒴 and f : 𝒳 ⟶ 𝒴 be 1-morphisms of algebraic stacks over S and let P be a 2-fibre product of that cospan in the 2-category of algebraic stacks. A point of 𝒵 and a point of 𝒳 with the same image in |𝒴| lift to a point of P; that is, the canonical map |P| ⟶ |𝒵| ×_{|𝒴|} |𝒳| is surjective.

theorem exists_point_of_isTwoFibreProduct_algebraicStacks
    {𝒵 𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} {g : 𝒵 ⟶ 𝒴} {f : 𝒳 ⟶ 𝒴}
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (z : points B S hS 𝒵.val.val (Classical.choose 𝒵.property))
    (x : points B S hS 𝒳.val.val (Classical.choose 𝒳.property))
    (h : pointsMap B S hS 𝒵.val.val (Classical.choose 𝒵.property)
          (Classical.choose 𝒴.property) g.hom.hom z =
        pointsMap B S hS 𝒳.val.val (Classical.choose 𝒳.property)
          (Classical.choose 𝒴.property) f.hom.hom x) :
    ∃ p : points B S hS P.pt.val.val (Classical.choose P.pt.property),
      pointsMap B S hS P.pt.val.val (Classical.choose P.pt.property)
          (Classical.choose 𝒵.property) P.fst.hom.hom p = z ∧
        pointsMap B S hS P.pt.val.val (Classical.choose P.pt.property)
          (Classical.choose 𝒳.property) P.snd.hom.hom p = x

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

Stacks 04XH for a 2-fibre product in the 2-category of algebraic stacks: a point of 𝒵 and a point of 𝒳 with the same image in |𝒴| lift to a point of any 2-fibre product of g : 𝒵 ⟶ 𝒴 and f : 𝒳 ⟶ 𝒴.

This is the same proposition as AlgebraicGeometry.Stack.exists_point_of_isTwoFibreProduct_algebraicStacks, which writes the points and the maps on points in longhand instead of through the abbreviations AlgebraicGeometry.Stack.AlgebraicStacks.points and AlgebraicGeometry.Stack.AlgebraicStacks.pointsMap.

theorem exists_point_of_isTwoFibreProduct {g : 𝒵 ⟶ 𝒴} {f : 𝒳 ⟶ 𝒴}
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (z : points B S hS 𝒵) (x : points B S hS 𝒳)
    (h : pointsMap B S hS g z = pointsMap B S hS f x) :
    ∃ p : points B S hS P.pt,
      pointsMap B S hS P.fst p = z ∧ pointsMap B S hS P.snd p = x
Tag 04XI, a lemma

Tag 04XI in the Stacks Project.

AlgebraicGeometry.Stack.pointsMap_surjective_iff_isRelativelySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsSurjective.lean, line 143.

Stacks 04XI. A 1-morphism of algebraic stacks over S which is representable by algebraic spaces is surjective — the relative property of Stacks 03YK at surjectivity of morphisms of algebraic spaces — exactly when the map it induces on points is surjective.

theorem pointsMap_surjective_iff_isRelativelySurjective
    (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) :
    Function.Surjective
        (pointsMap B S hS 𝒳.val.val (Classical.choose 𝒳.property)
          (Classical.choose 𝒴.property) f.hom.hom) ↔
      HasRelativeProperty B S hS (Space.surjectiveMorphismProperty B S hS) f.hom hf
Tag 04XJ, a lemma

Tag 04XJ in the Stacks Project.

AlgebraicGeometry.Stack.GroupoidPresentation.range_pointsMap_source_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsGroupoidPresentation.lean, line 435. The attribute's comment: “part 1: the image of |R| → |U| × |U| is an equivalence relation”.

Stacks 04XJ, the equivalence relation. Let 𝒳 = [U/R] be a presentation of a category 𝒳 over the big fppf site of S which is fibred in groupoids. Then the image of |R| ⟶ |U| × |U| is an equivalence relation on |U|, namely the kernel of the map |p| : |U| ⟶ |𝒳| induced by the presenting 1-morphism.

theorem range_pointsMap_source_target (P : GroupoidPresentation B S hS 𝒳)
    (h𝒳 : 𝒳.p.IsFiberedInGroupoids) :
    Set.range (fun r : arrowSpacePoints P.groupoid ↦
        (sourcePointsMap P.groupoid r, targetPointsMap P.groupoid r)) =
      {q : objectSpacePoints P.groupoid × objectSpacePoints P.groupoid |
        (Setoid.ker (P.presentingPointsMap h𝒳)).r q.1 q.2}

AlgebraicGeometry.Stack.GroupoidPresentation.pointsQuotientEquivOfPresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsGroupoidPresentation.lean, line 454. The attribute's comment: “part 2: |X| is the quotient of |U| by that relation”.

Stacks 04XJ, the quotient. Let 𝒳 = [U/R] be a presentation of a category 𝒳 over the big fppf site of S which is fibred in groupoids. Then |𝒳| is the quotient of |U| by the equivalence relation of AlgebraicGeometry.Stack.GroupoidPresentation.range_pointsMap_source_target, the image of |R| ⟶ |U| × |U|.

noncomputable def pointsQuotientEquivOfPresentation (P : GroupoidPresentation B S hS 𝒳)
    (h𝒳 : 𝒳.p.IsFiberedInGroupoids) :
    Quotient (Setoid.ker (P.presentingPointsMap h𝒳)) ≃ points B S hS 𝒳 h𝒳
Tag 04XK, a remark

Tag 04XK in the Stacks Project.

AlgebraicGeometry.Stack.range_prod_pointsMapToSpace_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsQuotientOfSpaceAtlas.lean, line 84. The attribute's comment: “image of the relation on points”.

The image of the relation on points. For a 2-fibre product R of a chart f : U ⟶ 𝒳 by an algebraic space with itself, the image of |R| ⟶ |U| × |U| is exactly the set of pairs of points of U with the same image in |𝒳|.

theorem range_prod_pointsMapToSpace_eq
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    {𝒳 : AlgebraicStacks.{u, w} B S hS}
    {p : algebraicSpaceStack.{u, w} B S hS F hF ⟶ 𝒳}
    (P : Bicategory.TwoCommSq p p) (hP : Bicategory.IsTwoFibreProduct P) :
    Set.range (fun r : AlgebraicStacks.points B S hS P.pt =>
        (pointsMapToSpace B S hS hF P.fst r, pointsMapToSpace B S hS hF P.snd r)) =
      {q : Space.points B S hS F × Space.points B S hS F |
        spacePointMap B S hS F 𝒳.val p.hom.hom q.1 =
          spacePointMap B S hS F 𝒳.val p.hom.hom q.2}

AlgebraicGeometry.Stack.equivalence_mem_range_prod_pointsMapToSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsQuotientOfSpaceAtlas.lean, line 113. The attribute's comment: “equivalence relation on points”.

The relation on points is an equivalence relation. The image of |R| ⟶ |U| × |U| is the kernel of |f|.

theorem equivalence_mem_range_prod_pointsMapToSpace
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    {𝒳 : AlgebraicStacks.{u, w} B S hS}
    {p : algebraicSpaceStack.{u, w} B S hS F hF ⟶ 𝒳}
    (P : Bicategory.TwoCommSq p p) (hP : Bicategory.IsTwoFibreProduct P) :
    Equivalence (fun x y : Space.points B S hS F =>
      (x, y) ∈ Set.range (fun r : AlgebraicStacks.points B S hS P.pt =>
        (pointsMapToSpace B S hS hF P.fst r, pointsMapToSpace B S hS hF P.snd r)))

AlgebraicGeometry.Stack.spacePointsQuotientEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsQuotientOfSpaceAtlas.lean, line 129. The attribute's comment: “the points of the stack as a quotient”.

The points of the stack as a quotient. For a surjective chart f : U ⟶ 𝒳 by an algebraic space, |𝒳| is the quotient of |U| by the kernel of |f|, which is the image of |R| ⟶ |U| × |U| by AlgebraicGeometry.Stack.range_prod_pointsMapToSpace_eq.

noncomputable def spacePointsQuotientEquiv
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (p : algebraicSpaceStack.{u, w} B S hS F hF ⟶ 𝒳) (hsurj : IsSurjective B S hS p) :
    Quotient (Setoid.ker (spacePointMap B S hS F 𝒳.val p.hom.hom)) ≃
      AlgebraicStacks.points B S hS 𝒳
Tag 04XL, a lemma

Tag 04XL in the Stacks Project.

AlgebraicGeometry.Stack.spacePointMap_class, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsTopology.lean, line 138. The attribute's comment: “canonical map on points”.

The chosen quotient representative in AlgebraicGeometry.Stack.spacePointMap has the same image as any field-valued representative of the point.

theorem spacePointMap_class (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (f : (fibredCategory B S hS F).val ⥤ᵇ 𝒳.val)
    (p : Space.FieldValuedPoint B S hS F) :
    spacePointMap B S hS F 𝒳 f (p.class B S hS F) =
      pointClass B S hS 𝒳.val 𝒳.property
        (fieldValuedPointMap B S hS (fibredCategory B S hS F).val f
          (spaceFieldValuedPoint B S hS F p))

AlgebraicGeometry.Stack.existsUnique_pointTopologyFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsTopology.lean, line 623. The attribute's comment: “existence and uniqueness of topology”.

There is a unique family of topologies on the points of the algebraic stacks over S which makes every 1-morphism continuous on points and makes a 1-morphism from an algebraic space whose represented base changes are all flat and locally of finite presentation continuous and open on points.

theorem existsUnique_pointTopologyFamily :
    ∃! _t : PointTopologyFamily.{u, w} B S hS, True
Tag 04Y8, a definition

Tag 04Y8 in the Stacks Project.

AlgebraicGeometry.Stack.pointTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsTopology.lean, line 345. The attribute's comment: “the underlying topological space of an algebraic stack”.

The topology on the points of a category fibred in groupoids over the big fppf site of S: the supremum, over all charts by algebraic spaces, of the topologies coinduced from the point topologies of the algebraic spaces along the canonical maps.

noncomputable def pointTopology
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)) :
    TopologicalSpace (points B S hS 𝒳.val 𝒳.property)
Tag 04Y9, a lemma

Tag 04Y9 in the Stacks Project.

AlgebraicGeometry.Stack.hasBasis_nhds_isOpen_isCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsLocallyQuasiCompact.lean, line 97. The attribute's comment: “fundamental system of quasi-compact open neighbourhoods”.

The quasi-compact open neighbourhoods of a point of the space of points of an algebraic stack over S are a fundamental system of neighbourhoods of that point.

theorem hasBasis_nhds_isOpen_isCompact (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (x : points B S hS 𝒳.val 𝒳.property) :
    (nhds x).HasBasis
      (fun W : Set (points B S hS 𝒳.val 𝒳.property) ↦ IsOpen W ∧ IsCompact W ∧ x ∈ W) id

AlgebraicGeometry.Stack.locallyCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsLocallyQuasiCompact.lean, line 109. The attribute's comment: “local quasi-compactness”.

The space of points of an algebraic stack over S is locally quasi-compact, that is, a LocallyCompactSpace.

theorem locallyCompactSpace (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val) :
    LocallyCompactSpace (points B S hS 𝒳.val 𝒳.property)
Sources
LeanAlgebraicGeometry.Stack.FieldValuedPoint.HasCommonExtension · AlgebraicGeometry.Stack.pointsMap · AlgebraicGeometry.Stack.pointsMap_eq_of_basedNatTrans · AlgebraicGeometry.Stack.pointsMap_comp · AlgebraicGeometry.Stack.pointsEquivOfBasedEquivalence · AlgebraicGeometry.Stack.spacePointMap_id_bijective · AlgebraicGeometry.Stack.FieldValuedPoint.hasCommonExtension_equivalence · AlgebraicGeometry.Stack.points

Section100.5 Surjective morphisms#

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

Tag 04ZS, a definition

Tag 04ZS in the Stacks Project.

AlgebraicGeometry.Stack.IsSurjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Surjective.lean, line 99.

Stacks 04ZS. A morphism of algebraic stacks is surjective if its map on points is surjective.

abbrev IsSurjective {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop
Tag 04ZT, a lemma

Tag 04ZT in the Stacks Project.

AlgebraicGeometry.Stack.isSurjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SurjectiveProperties.lean, line 46.

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

theorem isSurjective_comp (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsSurjective B S hS f) (hg : IsSurjective B S hS g) :
    IsSurjective B S hS (f ≫ g)
Tag 04ZU, a lemma

Tag 04ZU in the Stacks Project.

AlgebraicGeometry.Stack.isSurjective_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SurjectiveBaseChange.lean, line 146.

Stacks 04ZU. The base change of a surjective 1-morphism of algebraic stacks over S is surjective: in a 2-fibre-product square over the cospan (g, f), if g is surjective then so is the projection to the source of f.

theorem isSurjective_of_isTwoFibreProduct
    {𝒵 𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} {g : 𝒵 ⟶ 𝒴} {f : 𝒳 ⟶ 𝒴}
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hg : IsSurjective B S hS g) : IsSurjective B S hS P.snd
Tag 06PM, a lemma

Tag 06PM in the Stacks Project.

AlgebraicGeometry.Stack.isSurjective_of_isSurjective_twoCommSq_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SurjectiveProperties.lean, line 64. References: SGA 1 VIII (3.1), “f' surj => f surj”.

Surjectivity of a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S descends along a surjective 1-morphism g : 𝒵 ⟶ 𝒴: if some 2-commutative square over the cospan (g, f) has surjective first projection, then f is surjective.

theorem isSurjective_of_isSurjective_twoCommSq_fst {g : 𝒵 ⟶ 𝒴} {f : 𝒳 ⟶ 𝒴}
    (P : Bicategory.TwoCommSq g f) (hg : IsSurjective B S hS g)
    (hfst : IsSurjective B S hS P.fst) : IsSurjective B S hS f
Tag 06PN, a lemma

Tag 06PN in the Stacks Project.

AlgebraicGeometry.Stack.isSurjective_of_isSurjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SurjectiveProperties.lean, line 55.

If a composite of 1-morphisms of algebraic stacks over S is surjective, then so is its second factor.

theorem isSurjective_of_isSurjective_comp (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsSurjective B S hS (f ≫ g)) : IsSurjective B S hS g
Sources
LeanAlgebraicGeometry.Stack.IsSurjective · AlgebraicGeometry.Stack.isSurjective_comp · AlgebraicGeometry.Stack.isSurjective_of_isTwoFibreProduct · AlgebraicGeometry.Stack.isSurjective_of_isSurjective_twoCommSq_fst · AlgebraicGeometry.Stack.isSurjective_of_isSurjective_comp

Section100.6 Quasi-compact algebraic stacks#

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

Tag 04YB, a definition

Tag 04YB in the Stacks Project.

AlgebraicGeometry.Stack.IsQuasiCompactStack, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactStack.lean, line 50.

An algebraic stack over S is quasi-compact when its space of points, with the topology pointTopology, is a compact space.

abbrev IsQuasiCompactStack
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (_h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val) : Prop
Tag 04YC, a lemma

Tag 04YC in the Stacks Project.

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

An algebraic stack is quasi-compact if and only if it has a surjective smooth presentation by an affine scheme.

theorem isQuasiCompactStack_iff_hasAffineSmoothPresentation :
    IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property ↔
      HasAffineSmoothPresentation.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.hasAffineSmoothPresentation_iff_hasQuasiCompactSchemeSmoothPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothPresentationQuasiCompact.lean, line 450. The attribute's comment: “parts (2) and (3)”.

An algebraic stack has a surjective smooth presentation by an affine scheme if and only if it has one by a quasi-compact scheme.

theorem hasAffineSmoothPresentation_iff_hasQuasiCompactSchemeSmoothPresentation :
    HasAffineSmoothPresentation.{u, w} B S hS 𝒳 ↔
      HasQuasiCompactSchemeSmoothPresentation.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.hasQuasiCompactSchemeSmoothPresentation_iff_hasQuasiCompactSpaceSmoothPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothPresentationQuasiCompact.lean, line 462. The attribute's comment: “parts (3) and (4)”.

An algebraic stack has a surjective smooth presentation by a quasi-compact scheme if and only if it has one by a quasi-compact algebraic space.

theorem hasQuasiCompactSchemeSmoothPresentation_iff_hasQuasiCompactSpaceSmoothPresentation :
    HasQuasiCompactSchemeSmoothPresentation.{u, w} B S hS 𝒳 ↔
      HasQuasiCompactSpaceSmoothPresentation.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.hasQuasiCompactSpaceSmoothPresentation_iff_hasQuasiCompactStackSurjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothPresentationQuasiCompact.lean, line 476. The attribute's comment: “parts (4) and (5)”.

An algebraic stack has a surjective smooth presentation by a quasi-compact algebraic space if and only if there is a surjection onto it from a quasi-compact algebraic stack.

theorem hasQuasiCompactSpaceSmoothPresentation_iff_hasQuasiCompactStackSurjection :
    HasQuasiCompactSpaceSmoothPresentation.{u, w} B S hS 𝒳 ↔
      HasQuasiCompactStackSurjection.{u, w} B S hS 𝒳
Tag 04YD, a lemma

Tag 04YD in the Stacks Project.

AlgebraicGeometry.Stack.isQuasiCompactStack_of_isOpenSubstackCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactStackCover.lean, line 119. The attribute's comment: “the union is quasi-compact”.

Stacks 04YD, quasi-compactness. An algebraic stack covered by finitely many quasi-compact open substacks is quasi-compact; in particular a finite disjoint union of quasi-compact algebraic stacks is quasi-compact, disjointness of the members playing no role. The points of the substacks cover the points of 𝒳, so this is the topological fact that a finite union of quasi-compact subsets is quasi-compact.

theorem isQuasiCompactStack_of_isOpenSubstackCover
    {ι : Type*} [Finite ι] (𝒳 : AlgebraicStacks.{u, w} B S hS) (𝒰 : ι → OpenSubstack 𝒳)
    (hcover : IsOpenSubstackCover 𝒳 𝒰)
    (h𝒰 : ∀ i, IsQuasiCompactStack.{u, w} B S hS
      (fullSubcategoryAlgebraicStack 𝒳 (𝒰 i).property (𝒰 i).isAlgebraic).val
      (fullSubcategoryAlgebraicStack 𝒳 (𝒰 i).property (𝒰 i).isAlgebraic).property) :
    IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property
Sources
LeanAlgebraicGeometry.Stack.IsQuasiCompactStack · AlgebraicGeometry.Stack.isQuasiCompactStack_iff_hasAffineSmoothPresentation · AlgebraicGeometry.Stack.hasAffineSmoothPresentation_iff_hasQuasiCompactSchemeSmoothPresentation · AlgebraicGeometry.Stack.hasQuasiCompactSchemeSmoothPresentation_iff_hasQuasiCompactSpaceSmoothPresentation · AlgebraicGeometry.Stack.hasQuasiCompactSpaceSmoothPresentation_iff_hasQuasiCompactStackSurjection · AlgebraicGeometry.Stack.isQuasiCompactStack_of_isOpenSubstackCover

Section100.7 Properties of algebraic stacks defined by properties of schemes#

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

Tag 04YF, a lemma

Tag 04YF in the Stacks Project.

AlgebraicGeometry.Stack.exists_scheme_atlas_iff_forall_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalPropertyAtlasScheme.lean, line 163. The attribute's comment: “scheme criteria”.

Stacks 04YF, the two scheme criteria. For a property P of schemes local in the smooth topology, an algebraic stack over S admits some smooth surjective 1-morphism from the algebraic stack of a scheme over S with P exactly when every smooth 1-morphism from the algebraic stack of a scheme over S has source with P.

theorem exists_scheme_atlas_iff_forall_scheme
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    HasPropertyOnSomeSchemeAtlas B S hS P 𝒳 ↔
      HasPropertyOnEverySchemeChart B S hS P 𝒳

AlgebraicGeometry.Stack.exists_scheme_atlas_iff_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalPropertyAtlasScheme.lean, line 205. The attribute's comment: “scheme case”.

Stacks 04YF, the scheme case. On the algebraic stack of a scheme U over S, the existential scheme criterion for a smooth-local property P is P of the scheme underlying U.

One direction is smooth surjective descent along the presentation; the other tests the universal criterion, which the identity presentation satisfies, at an arbitrary chart.

theorem exists_scheme_atlas_iff_scheme
    (U : BigFppfOver B S hS) :
    HasPropertyOnSomeSchemeAtlas B S hS P (schemeStack.{u, w} B S hS U) ↔
      P ((BigFppfOver.toScheme B S hS).obj U)

AlgebraicGeometry.Stack.exists_scheme_atlas_iff_exists_space_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalPropertyAtlasSpace.lean, line 373. The attribute's comment: “scheme and space atlases”.

An algebraic stack over S admits a smooth surjective 1-morphism from the algebraic stack of a scheme over S with P exactly when it admits one from the algebraic stack of an algebraic space over S with the étale-local property P of Stacks 03E6.

theorem exists_scheme_atlas_iff_exists_space_atlas
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    HasPropertyOnSomeSchemeAtlas B S hS P 𝒳 ↔
      HasPropertyOnSomeSpaceAtlas B S hS P 𝒳

AlgebraicGeometry.Stack.exists_space_atlas_iff_forall_space, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalPropertyAtlasSpace.lean, line 396. The attribute's comment: “space criteria”.

An algebraic stack over S admits a smooth surjective 1-morphism from the algebraic stack of an algebraic space over S with the étale-local property P exactly when every smooth 1-morphism from the algebraic stack of an algebraic space over S has source with that property.

theorem exists_space_atlas_iff_forall_space
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    HasPropertyOnSomeSpaceAtlas B S hS P 𝒳 ↔
      HasPropertyOnEverySpaceChart B S hS P 𝒳

AlgebraicGeometry.Stack.exists_space_atlas_iff_space, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalPropertyAtlasSpace.lean, line 421. The attribute's comment: “algebraic-space case”.

On the algebraic stack of an algebraic space over S, the existential algebraic-space criterion for a smooth-local property P is the étale-local property P of Stacks 03E6 of that algebraic space.

theorem exists_space_atlas_iff_space
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F) :
    HasPropertyOnSomeSpaceAtlas B S hS P (algebraicSpaceStack.{u, w} B S hS F hF) ↔
      Space.HasEtaleLocalProperty B S hS F P
Tag 04YG, a definition

Tag 04YG in the Stacks Project.

AlgebraicGeometry.Stack.HasPropertyOnSomeSchemeAtlas, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalPropertyAtlas.lean, line 96.

The existential scheme criterion of Stacks 04YF, and Stacks 04YG: the algebraic stack 𝒳 has property P when it admits a smooth surjective 1-morphism from the algebraic stack of a scheme over S whose underlying scheme has P.

Stacks 04YG defines "𝒳 has P" by any of the four equivalent conditions of Stacks 04YF; this is the first of them, and the comparisons of Stacks 04YF identify it with the other three.

abbrev HasPropertyOnSomeSchemeAtlas (𝒳 : AlgebraicStacks.{u, w} B S hS) : Prop
Tag 04YI, a lemma

Tag 04YI in the Stacks Project.

AlgebraicGeometry.Stack.tfae_germProperty_at_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalGermAtPoint.lean, line 476.

Stacks 04YI. Let 𝒳 be an algebraic stack over S, let x be a point of 𝒳, and let P be a smooth-local property of germs of schemes (Stacks 04N1). Then the four conditions comparing P against the smooth charts of 𝒳 through x — every scheme chart, some scheme chart, every algebraic space chart, some algebraic space chart — are equivalent.

theorem tfae_germProperty_at_point (hP : GermOfScheme.IsSmoothLocal P) :
    [GermPropertyAtEverySchemeChart B S hS 𝒳 x P,
      GermPropertyAtSomeSchemeChart B S hS 𝒳 x P,
      GermPropertyAtEverySpaceChart B S hS 𝒳 x P,
      GermPropertyAtSomeSpaceChart B S hS 𝒳 x P].TFAE

AlgebraicGeometry.Stack.germPropertyAtSomeSpaceChart_algebraicSpaceStack_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalGermAtPoint.lean, line 527. The attribute's comment: “algebraic space case”.

Stacks 04YI, the algebraic space addendum. On the algebraic stack of an algebraic space F over S the four conditions say that F has property P at the corresponding point of F, in the sense of Stacks 04RC. The chart realizing the existential condition is the identity.

theorem germPropertyAtSomeSpaceChart_algebraicSpaceStack_iff
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (z : Space.points B S hS F) (P : GermOfScheme.{u} → Prop)
    (hP : GermOfScheme.IsSmoothLocal P) :
    GermPropertyAtSomeSpaceChart B S hS (algebraicSpaceStack.{u, w} B S hS F hF)
        (spacePointMap B S hS F (fibredCategory B S hS F)
          (BasedFunctor.id (fibredCategory B S hS F).val) z) P ↔
      Space.HasPropertyAtPoint B S hS F z P

AlgebraicGeometry.Stack.germPropertyAtSomeSpaceChart_yoneda_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalGermAtPoint.lean, line 548. The attribute's comment: “representable case”.

Stacks 04YI, the representable addendum. On the algebraic stack of a scheme U over S the four conditions say that the germ of U at the corresponding scheme point has P.

theorem germPropertyAtSomeSpaceChart_yoneda_iff (U : BigFppfOver B S hS)
    (p : Space.FieldValuedPoint B S hS (yoneda.obj U)) (P : GermOfScheme.{u} → Prop)
    (hP : GermOfScheme.IsSmoothLocal P) :
    GermPropertyAtSomeSpaceChart B S hS
        (algebraicSpaceStack.{u, w} B S hS (yoneda.obj U)
          (isAlgebraicSpace_yoneda B S hS U))
        (spacePointMap B S hS (yoneda.obj U) (fibredCategory B S hS (yoneda.obj U))
          (BasedFunctor.id (fibredCategory B S hS (yoneda.obj U)).val)
          (p.class B S hS (yoneda.obj U))) P ↔
      P ⟨(BigFppfOver.toScheme B S hS).obj U, Space.schemePoint B S hS U p⟩
Tag 04YJ, a definition

Tag 04YJ in the Stacks Project.

AlgebraicGeometry.Stack.HasPropertyAtPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocalGermAtPoint.lean, line 578.

Stacks 04YJ. Let P be a property of germs of schemes which is smooth local (Stacks 04N1), let 𝒳 be an algebraic stack over S and let x be a point of 𝒳 (Stacks 04XG). Then 𝒳 has property P at x when some smooth chart of 𝒳 by an algebraic space has property P at some point of it lying over x, in the sense of Stacks 04RC.

The source defines this by any of the four equivalent conditions of Stacks 04YI; this is the fourth of them, and AlgebraicGeometry.Stack.tfae_germProperty_at_point identifies it with the other three for a smooth-local P, which is what makes the choice immaterial. As for Stacks 04RC, stating this one condition needs neither that hypothesis nor surjectivity of the chart. Its specializations are the two addenda above: AlgebraicGeometry.Stack.germPropertyAtSomeSpaceChart_algebraicSpaceStack_iff on the algebraic stack of an algebraic space and AlgebraicGeometry.Stack.germPropertyAtSomeSpaceChart_yoneda_iff on that of a scheme.

abbrev HasPropertyAtPoint : Prop
Sources
LeanAlgebraicGeometry.Stack.exists_scheme_atlas_iff_forall_scheme · AlgebraicGeometry.Stack.exists_scheme_atlas_iff_scheme · AlgebraicGeometry.Stack.exists_scheme_atlas_iff_exists_space_atlas · AlgebraicGeometry.Stack.exists_space_atlas_iff_forall_space · AlgebraicGeometry.Stack.exists_space_atlas_iff_space · AlgebraicGeometry.Stack.HasPropertyOnSomeSchemeAtlas · AlgebraicGeometry.Stack.tfae_germProperty_at_point · AlgebraicGeometry.Stack.germPropertyAtSomeSpaceChart_algebraicSpaceStack_iff

Section100.8 Monomorphisms of algebraic stacks#

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

Tag 04ZW, a definition

Tag 04ZW in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsMonomorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ResidualGerbe.lean, line 109.

Stacks 04ZW. A 1-morphism of algebraic stacks over S is a monomorphism when it is representable by algebraic spaces and every algebraic space representing one of its base changes along a scheme-valued point of the target has structural morphism a monomorphism of algebraic spaces over S.

This is AlgebraicGeometry.Stack.HasRelativeProperty (Stacks 03YK, the Section 04XB notion the source refers to) at the monomorphisms, written out rather than invoked; see the implementation notes.

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

Tag 04ZX in the Stacks Project.

Declarations registered for the tag:

Tag 04ZY, a lemma

Tag 04ZY in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismPermanence.lean, line 65.

Stacks 04ZY. A composite of monomorphisms of algebraic stacks over S (Stacks 04ZW) is a monomorphism.

theorem isMonomorphism_comp (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsMonomorphism B S hS f) (hg : IsMonomorphism B S hS g) :
    IsMonomorphism B S hS (f ≫ g)
Tag 04ZZ, a lemma

Tag 04ZZ in the Stacks Project.

AlgebraicGeometry.Stack.mono_hom_representingMaps_of_full_and_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FullyFaithfulMonomorphism.lean, line 198. The attribute's comment: “(2) implies (1), the monomorphism clause for categories fibred in groupoids”.

The implication (2) ⟹ (1) of Stacks 04ZZ. A fully faithful 1-morphism j : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf site of S is a monomorphism in the sense of Stacks 04XB: every algebraic space representing a base change of j along a scheme-valued point of 𝒴 has monomorphic structural morphism.

This is the converse of AlgebraicGeometry.Stack.full_and_faithful_homFunctor_of_mono_representingMaps, and it carries no representability hypothesis.

theorem mono_hom_representingMaps_of_full_and_faithful
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (j : 𝒳 ⟶ 𝒴)
    (hfull : (CatFiberedInGroupoids.homFunctor j).Full)
    (hfaithful : (CatFiberedInGroupoids.homFunctor j).Faithful)
    (U : BigFppfOver B S hS)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
    (_hy : y ⋙ 𝒴.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)
    (he : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.p 𝒴.val.p y
        (CatFiberedInGroupoids.homFunctor j))
      (presheafOfCategories (F ⋙ typeToCat)).p)) :
    Mono (algebraicSpaceMap B S hS U
      ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

AlgebraicGeometry.Stack.mono_representingMaps_of_full_and_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FullyFaithfulMonomorphism.lean, line 222. The attribute's comment: “(2) implies (1), the monomorphism clause read in the category of algebraic spaces over S”.

The implication (2) ⟹ (1) of Stacks 04ZZ, in the category of algebraic spaces. This is AlgebraicGeometry.Stack.mono_hom_representingMaps_of_full_and_faithful read in the category of algebraic spaces over S, which is the form the relative properties of Stacks 03YK — and hence AlgebraicGeometry.Stack.AlgebraicStacks.IsMonomorphism — are stated in.

theorem mono_representingMaps_of_full_and_faithful
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (j : 𝒳 ⟶ 𝒴)
    (hfull : (CatFiberedInGroupoids.homFunctor j).Full)
    (hfaithful : (CatFiberedInGroupoids.homFunctor j).Faithful)
    (U : BigFppfOver B S hS)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
    (_hy : y ⋙ 𝒴.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)
    (he : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.p 𝒴.val.p y
        (CatFiberedInGroupoids.homFunctor j))
      (presheafOfCategories (F ⋙ typeToCat)).p)) :
    Mono (algebraicSpaceMap B S hS U
      ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩))

AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_of_full_and_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FullyFaithfulMonomorphism.lean, line 251. The attribute's comment: “(2) implies (1) for 1-morphisms of algebraic stacks”.

The implication (2) ⟹ (1) of Stacks 04ZZ, for a 1-morphism of algebraic stacks. A fully faithful 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is a monomorphism in the sense of Stacks 04ZW.

The representability conjunct of AlgebraicGeometry.Stack.AlgebraicStacks.IsMonomorphism is the implication (2) ⟹ (3) of Stacks 04Y5, AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_of_faithful; the monomorphy conjunct is AlgebraicGeometry.Stack.mono_representingMaps_of_full_and_faithful.

theorem isMonomorphism_of_full_and_faithful
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hfull : (CatFiberedInGroupoids.homFunctor f.hom).Full)
    (hfaithful : (CatFiberedInGroupoids.homFunctor f.hom).Faithful) :
    AlgebraicStacks.IsMonomorphism B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_tfae_of_bootstrap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismEquivalentConditions.lean, line 217.

Stacks 04ZZ. For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S the following are equivalent:

  1. f is a monomorphism (Stacks 04ZW);
  2. f is fully faithful;
  3. the diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is an equivalence;
  4. there are an algebraic space W and a surjective, flat, locally finitely presented W ⟶ 𝒴 such that V = 𝒳 ×_𝒴 W is an algebraic space and V ⟶ W is a monomorphism.

(1) ⟹ (2) is Stacks 05UK, (2) ⟺ (3) is Stacks 04Z7, (2) ⟹ (1) is AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_of_full_and_faithful (through Stacks 04Y5), (1) ⟹ (4) is AlgebraicGeometry.Stack.AlgebraicStacks.hasMonomorphicFppfSpaceBaseChange_of_isMonomorphism and (4) ⟹ (2) is full_and_faithful_homFunctor_of_hasMonomorphicFppfSpaceBaseChange.

theorem isMonomorphism_tfae_of_bootstrap (f : 𝒳 ⟶ 𝒴) :
    List.TFAE
      [IsMonomorphism B S hS f,
        (CatFiberedInGroupoids.homFunctor f.hom).Full ∧
          (CatFiberedInGroupoids.homFunctor f.hom).Faithful,
        (CatFiberedInGroupoids.homFunctor
          (relativeDiagonalAlgebraicStacks B S hS f).hom).IsEquivalence,
        HasMonomorphicFppfSpaceBaseChange B S hS f]

AlgebraicGeometry.Stack.AlgebraicStacks.full_and_faithful_homFunctor_of_isMonomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismFullyFaithful.lean, line 333. The attribute's comment: “the implication (1) ⟹ (2): a monomorphism of algebraic stacks is fully faithful”.

The implication (1) ⟹ (2) of Stacks 04ZZ: a monomorphism of algebraic stacks is fully faithful. A 1-morphism of algebraic stacks over S which is a monomorphism in the sense of Stacks 04ZW has fully faithful underlying functor.

This is AlgebraicGeometry.Stack.full_and_faithful_homFunctor_of_mono_representingMaps (Stacks 05UK with Stacks 003Z) read in the 2-category of algebraic stacks of Stacks 03YP. The representability witness is the first conjunct of Stacks 04ZW, and its second conjunct gives the monomorphy of each representing structural morphism in the category of algebraic spaces over S, which Stacks 042M turns into monomorphy of the underlying morphism of presheaves.

theorem full_and_faithful_homFunctor_of_isMonomorphism (f : 𝒳 ⟶ 𝒴)
    (hf : IsMonomorphism B S hS f) :
    (CatFiberedInGroupoids.homFunctor f.hom).Full ∧
      (CatFiberedInGroupoids.homFunctor f.hom).Faithful
Tag 0500, a lemma

Tag 0500 in the Stacks Project.

AlgebraicGeometry.Stack.pointsMap_injective_of_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PointsInjective.lean, line 37.

A monomorphism of algebraic stacks induces an injective map on points.

public theorem pointsMap_injective_of_fullyFaithful
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴)
    [Functor.Full (CatFiberedInGroupoids.homFunctor f.hom)]
    [Functor.Faithful (CatFiberedInGroupoids.homFunctor f.hom)] :
    Function.Injective
      (pointsMap B S hS 𝒳.val.val
        (Classical.choose 𝒳.property) (Classical.choose 𝒴.property) f.hom.hom)
Tag 0CBB, a lemma

Tag 0CBB in the Stacks Project.

AlgebraicGeometry.Stack.isTwoFibreProduct_monomorphismDiagonalSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismDiagonalSquare.lean, line 171.

Stacks 0CBB. Let f : 𝒳 ⟶ 𝒳' and g : 𝒳' ⟶ 𝒴 be 1-morphisms of algebraic stacks over S. If f is a monomorphism (Stacks 04ZW), then the canonical square

  𝒳  --Δ_{𝒳/𝒴}-->  𝒳 ×_𝒴 𝒳
  |                     |
 f|                     | f × f
  v                     v
  𝒳' --Δ_{𝒳'/𝒴}--> 𝒳' ×_𝒴 𝒳'

AlgebraicGeometry.Stack.monomorphismDiagonalSquare is a 2-fibre product in the 2-category of algebraic stacks over (Sch/S)_fppf.

This is the source's proof: 𝒳 = 𝒳 ×_{𝒳'} 𝒳 by Stacks 04ZZ, the relative diagonal of the monomorphism f being an equivalence, and the square is then the 2-cartesian square of Stacks 04Z1 precomposed with that equivalence.

def isTwoFibreProduct_monomorphismDiagonalSquare (f : 𝒳 ⟶ 𝒳') (g : 𝒳' ⟶ 𝒴)
    (hf : AlgebraicStacks.IsMonomorphism B S hS f) :
    IsTwoFibreProduct (monomorphismDiagonalSquare B S hS f g)

CategoryTheory.Limits.CategoricalPullback.isEquivalence_monomorphism_diagonalComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/TwoFibreProduct/MonomorphismDiagonal.lean, line 94.

Stacks 0CBB. The square from the relative diagonal of a fully faithful functor f to the relative diagonal of f ⋙ g is a 2-fibre product square: the induced functor into the explicit 2-fibre product is an equivalence.

It is the composite of the relative diagonal of f, an equivalence because f is fully faithful, with the Stacks 04Z1 comparison functor.

theorem isEquivalence_monomorphism_diagonalComparison
    {X X' Y : Type*} [Category X] [Category X'] [Category Y]
    (f : X ⥤ X') (g : X' ⥤ Y) (hf : f.Full ∧ f.Faithful) :
    (relativeDiagonal f ⋙ toRelativeDiagonalPullback f f g).IsEquivalence
Sources
LeanAlgebraicGeometry.Stack.AlgebraicStacks.IsMonomorphism · AlgebraicStacks.isMonomorphism_fst_twoFibreProductSquareAlgebraicStacks · AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_comp · AlgebraicGeometry.Stack.mono_hom_representingMaps_of_full_and_faithful · AlgebraicGeometry.Stack.mono_representingMaps_of_full_and_faithful · AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_of_full_and_faithful · AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_tfae_of_bootstrap · AlgebraicGeometry.Stack.AlgebraicStacks.full_and_faithful_homFunctor_of_isMonomorphism

Section100.9 Immersions of algebraic stacks#

Section 100.9 of the Stacks Project, Tag 04YK. 20 tags here are carried by 83 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04YL, a definition

Tag 04YL in the Stacks Project.

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

Stacks 04YL, part (1). A 1-morphism of algebraic stacks over S is an open immersion when it is representable by algebraic spaces and is an open immersion in the sense of Stacks 04XB.

abbrev IsOpenImmersion (f : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.AlgebraicStacks.IsClosedImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionAlgebraicStack.lean, line 216. The attribute's comment: “part (2): closed immersions”.

Stacks 04YL, part (2). A 1-morphism of algebraic stacks over S is a closed immersion when it is representable by algebraic spaces and is a closed immersion in the sense of Stacks 04XB.

abbrev IsClosedImmersion (f : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.AlgebraicStacks.IsImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionAlgebraicStack.lean, line 222. The attribute's comment: “part (3): immersions”.

Stacks 04YL, part (3). A 1-morphism of algebraic stacks over S is an immersion when it is representable by algebraic spaces and is an immersion in the sense of Stacks 04XB.

abbrev IsImmersion (f : 𝒳 ⟶ 𝒴) : Prop
Tag 0501, a lemma

Tag 0501 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isImmersion_snd_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionBaseChange.lean, line 143. The attribute's comment: “immersions”.

Base change of an immersion of algebraic stacks. If g : 𝒵 ⟶ 𝒴 is an immersion of algebraic stacks over S and P is a 2-fibre product of the cospan (g, f) in the 2-category of algebraic stacks, then P.snd : P.pt ⟶ 𝒳 is an immersion of algebraic stacks.

Both halves are base-change statements: representability by algebraic spaces is Stacks 0302 and the immersion property of Stacks 04XB is Stacks 045C. The attribute records the latter, at the level of algebraic stacks. It deliberately does not record Stacks 04YL: that tag is a definition — its three parts define open immersions, closed immersions and immersions in terms of Section 04XB — and says nothing about stability under base change, so a theorem must not carry it. The definition itself is carried by AlgebraicStacks.IsImmersion.

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

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

Stacks 0501 for closed immersions. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒵 ⟶ 𝒴 be a closed immersion of algebraic stacks. Then the projection 𝒵 ×_𝒴 𝒳 ⟶ 𝒳 is a closed immersion of algebraic stacks.

Stated at an arbitrary 2-fibre product square P of the cospan (g, f) in the 2-category of algebraic stacks; the source's 𝒵 ×_𝒴 𝒳 is the canonical such square.

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

AlgebraicGeometry.Stack.AlgebraicStacks.isOpenImmersion_baseChange_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionsStableUnderBaseChange.lean, line 180. The attribute's comment: “open immersions”.

Stacks 0501 for open immersions. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒵 ⟶ 𝒴 be an open immersion of algebraic stacks. Then the projection 𝒵 ×_𝒴 𝒳 ⟶ 𝒳 is an open immersion of algebraic stacks.

Stated at an arbitrary 2-fibre product square P of the cospan (g, f) in the 2-category of algebraic stacks; the source's 𝒵 ×_𝒴 𝒳 is the canonical such square.

theorem isOpenImmersion_baseChange_snd
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hg : IsOpenImmersion B S hS g) :
    IsOpenImmersion B S hS P.snd
Tag 0502, a lemma

Tag 0502 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isOpenImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionAlgebraicStack.lean, line 285. The attribute's comment: “open immersions”. References: EGA I (4.2.5), “open immersions”.

Stacks 0502 for open immersions: a composite of open immersions of algebraic stacks over S is an open immersion.

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

AlgebraicGeometry.Stack.AlgebraicStacks.isClosedImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionAlgebraicStack.lean, line 297. The attribute's comment: “closed immersions”. References: EGA I (4.2.5), “closed immersions”.

Stacks 0502 for closed immersions: a composite of closed immersions of algebraic stacks over S is a closed immersion.

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

AlgebraicGeometry.Stack.AlgebraicStacks.isImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionAlgebraicStack.lean, line 312. The attribute's comment: “immersions”. References: EGA I (4.2.5), “immersions”.

Stacks 0502: a composite of immersions of algebraic stacks over S is an immersion.

theorem isImmersion_comp
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsImmersion B S hS f) (hg : IsImmersion B S hS g) :
    IsImmersion B S hS (f ≫ g)
Tag 0503, a lemma

Tag 0503 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isImmersion_iff_exists_isImmersion_representingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionFppfCoverCriterion.lean, line 296. The attribute's comment: “immersions”.

Stacks 0503 for immersions. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S, let W be an algebraic space over S and let g : W ⟶ 𝒴 be surjective, flat and locally of finite presentation. Then f is an immersion of algebraic stacks (Stacks 04YL, part (3)) exactly when V = W ×_𝒴 𝒳 is an algebraic space and V ⟶ W is an immersion of algebraic spaces.

The forward implication reads representability by algebraic spaces off clause (1); the backward one obtains it from Stacks 04ZP. The content of both is Stacks 04XD at the immersion property.

theorem isImmersion_iff_exists_isImmersion_representingMap :
    IsImmersion B S hS f ↔
      ∃ (V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_hV : IsAlgebraicSpace B S hS V)
        (eV : StacksRepresentableCFG.EquivalenceOver
          Q.pt.val.p (presheafOfCategories (V ⋙ typeToCat)).p),
        Space.IsImmersion B S hS (representingMap B S hS Q.pt 𝒲 V W eV eW Q.fst)

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

Stacks 0503 for closed immersions. In the situation of AlgebraicGeometry.Stack.AlgebraicStacks.isImmersion_iff_exists_isImmersion_representingMap, f is a closed immersion of algebraic stacks (Stacks 04YL, part (2)) exactly when V = W ×_𝒴 𝒳 is an algebraic space and V ⟶ W is a closed immersion of algebraic spaces.

theorem isClosedImmersion_iff_exists_isClosedImmersion_representingMap :
    IsClosedImmersion B S hS f ↔
      ∃ (V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_hV : IsAlgebraicSpace B S hS V)
        (eV : StacksRepresentableCFG.EquivalenceOver
          Q.pt.val.p (presheafOfCategories (V ⋙ typeToCat)).p),
        Space.IsClosedImmersion B S hS (representingMap B S hS Q.pt 𝒲 V W eV eW Q.fst)

AlgebraicGeometry.Stack.AlgebraicStacks.isOpenImmersion_iff_exists_isOpenImmersion_representingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionFppfCoverCriterion.lean, line 326. The attribute's comment: “open immersions”.

Stacks 0503 for open immersions. In the situation of AlgebraicGeometry.Stack.AlgebraicStacks.isImmersion_iff_exists_isImmersion_representingMap, f is an open immersion of algebraic stacks (Stacks 04YL, part (1)) exactly when V = W ×_𝒴 𝒳 is an algebraic space and V ⟶ W is an open immersion of algebraic spaces.

theorem isOpenImmersion_iff_exists_isOpenImmersion_representingMap :
    IsOpenImmersion B S hS f ↔
      ∃ (V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_hV : IsAlgebraicSpace B S hS V)
        (eV : StacksRepresentableCFG.EquivalenceOver
          Q.pt.val.p (presheafOfCategories (V ⋙ typeToCat)).p),
        Space.IsOpenImmersion B S hS (representingMap B S hS Q.pt 𝒲 V W eV eW Q.fst)
Tag 0504, a lemma

Tag 0504 in the Stacks Project.

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

An immersion of algebraic stacks over S is a monomorphism.

theorem isMonomorphism_of_isImmersion (f : 𝒳 ⟶ 𝒴) (hf : IsImmersion B S hS f) :
    IsMonomorphism B S hS f
Tag 0H20, a lemma

Tag 0H20 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isEmbedding_pointsMap_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionPointsAlgebraicStack.lean, line 281. The attribute's comment: “homeomorphism onto the image”.

Stacks 0H20, the homeomorphism onto the image. An immersion of algebraic stacks over S is a topological embedding on the spaces of points of Stacks 04XG and 04XL.

theorem isEmbedding_pointsMap_of_isImmersion (f : 𝒳 ⟶ 𝒴) (hf : IsImmersion B S hS f) :
    @Topology.IsEmbedding _ _ (Stack.pointTopology B S hS 𝒳.val)
      (Stack.pointTopology B S hS 𝒴.val)
      (Stack.pointsMap B S hS 𝒳.val.val 𝒳.val.property 𝒴.val.property f.hom.hom)

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyClosed_range_pointsMap_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionPointsAlgebraicStack.lean, line 298. The attribute's comment: “locally closed image”.

Stacks 0H20, the locally closed image. The image on points of an immersion of algebraic stacks over S is a locally closed subset of the space of points of the target.

theorem isLocallyClosed_range_pointsMap_of_isImmersion (f : 𝒳 ⟶ 𝒴)
    (hf : IsImmersion B S hS f) :
    @IsLocallyClosed _ (Stack.pointTopology B S hS 𝒴.val)
      (Set.range (Stack.pointsMap B S hS 𝒳.val.val 𝒳.val.property 𝒴.val.property f.hom.hom))

AlgebraicGeometry.Stack.AlgebraicStacks.isClosedMap_pointsMap_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionPointsAlgebraicStack.lean, line 314. The attribute's comment: “closed immersions are closed on points”.

Stacks 0H20, closed immersions. A closed immersion of algebraic stacks over S is a closed map on the spaces of points of Stacks 04XG and 04XL.

theorem isClosedMap_pointsMap_of_isClosedImmersion (f : 𝒳 ⟶ 𝒴)
    (hf : IsClosedImmersion B S hS f) :
    @IsClosedMap _ _ (Stack.pointTopology B S hS 𝒳.val) (Stack.pointTopology B S hS 𝒴.val)
      (Stack.pointsMap B S hS 𝒳.val.val 𝒳.val.property 𝒴.val.property f.hom.hom)

AlgebraicGeometry.Stack.AlgebraicStacks.isOpenMap_pointsMap_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionPointsAlgebraicStack.lean, line 335. The attribute's comment: “open immersions are open on points”.

Stacks 0H20, open immersions. An open immersion of algebraic stacks over S is an open map on the spaces of points of Stacks 04XG and 04XL.

theorem isOpenMap_pointsMap_of_isOpenImmersion (f : 𝒳 ⟶ 𝒴)
    (hf : IsOpenImmersion B S hS f) :
    @IsOpenMap _ _ (Stack.pointTopology B S hS 𝒳.val) (Stack.pointTopology B S hS 𝒴.val)
      (Stack.pointsMap B S hS 𝒳.val.val 𝒳.val.property 𝒴.val.property f.hom.hom)
Tag 0505, a lemma

Tag 0505 in the Stacks Project.

AlgebraicGeometry.Stack.isInvariantLocallyClosed_range_of_isImmersion_essImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionIntoQuotientStackSubspace.lean, line 351. The attribute's comment: “the R-invariant locally closed subspace Z = U' of U cut out by an immersion into [U/R]; the 2-fibre product U' = 𝒵 ×_{[U/R]} U of Stacks 04Y6 is carried as the morphism m together with hmem, and the immersion property of m (Stacks 04XD applied to i) as hm; the presentation [Z/R_Z] ⟶ 𝒵 and the 2-commutative triangle are not proved”.

Stacks 0505, the invariant locally closed subspace. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces, let i : 𝒵 ⟶ [U/R] be a 1-morphism over the big fppf site, and let m : U' ⟶ U be an immersion of algebraic spaces whose range is, pointwise, the inverse image along U ⟶ [U/R] of the essential image of i — which is what it is for U' to be the 2-fibre product 𝒵 ×_{[U/R]} U of Stacks 04Y6. Then the range of m is an R-invariant locally closed subspace Z ⊆ U in the sense of Stacks 044F, part (2), and U' ≅ Z.

Smoothness of G is not used.

theorem isInvariantLocallyClosed_range_of_isImmersion_essImage
    (hm : Space.IsImmersion C S hS m.hom)
    (hmem : ∀ (W : (BigFppfOver C S hS)ᵒᵖ) (u : G.objects.obj.obj W),
      u ∈ (Subfunctor.range m.hom).obj W ↔
        i.toFunctor.essImage ((quotientStackProjection G).obj ⟨W.unop, Discrete.mk u⟩)) :
    IsInvariantLocallyClosed G (Subfunctor.range m.hom)

AlgebraicGeometry.Stack.isInvariantClosed_range_of_isClosedImmersion_essImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionIntoQuotientStackSubspace.lean, line 367. The attribute's comment: “the R-invariant closed subspace, for a closed immersion into [U/R]; the 2-fibre product of Stacks 04Y6 is carried as m together with hmem, and the closed immersion property of m (Stacks 04XD applied to i) as hm”.

Stacks 0505, the invariant closed subspace. In the situation of AlgebraicGeometry.Stack.isInvariantLocallyClosed_range_of_isImmersion_essImage, if m is a closed immersion — which is what the source gets from i being a closed immersion — then the range of m is an invariant closed subspace of U.

theorem isInvariantClosed_range_of_isClosedImmersion_essImage
    (hm : Space.IsClosedImmersion C S hS m.hom)
    (hmem : ∀ (W : (BigFppfOver C S hS)ᵒᵖ) (u : G.objects.obj.obj W),
      u ∈ (Subfunctor.range m.hom).obj W ↔
        i.toFunctor.essImage ((quotientStackProjection G).obj ⟨W.unop, Discrete.mk u⟩)) :
    IsInvariantClosed G (Subfunctor.range m.hom)

AlgebraicGeometry.Stack.isInvariantOpen_range_of_isOpenImmersion_essImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionIntoQuotientStackSubspace.lean, line 386. The attribute's comment: “the R-invariant open subspace, for an open immersion into [U/R]; the 2-fibre product of Stacks 04Y6 is carried as m together with hmem, and the open immersion property of m (Stacks 04XD applied to i) as hm”.

Stacks 0505, the invariant open subspace. In the situation of AlgebraicGeometry.Stack.isInvariantLocallyClosed_range_of_isImmersion_essImage, if m is an open immersion — which is what the source gets from i being an open immersion — then the range of m is an invariant open subspace of U in the sense of Stacks 044F, part (1).

theorem isInvariantOpen_range_of_isOpenImmersion_essImage
    (hm : Space.IsOpenImmersion C S hS m.hom)
    (hmem : ∀ (W : (BigFppfOver C S hS)ᵒᵖ) (u : G.objects.obj.obj W),
      u ∈ (Subfunctor.range m.hom).obj W ↔
        i.toFunctor.essImage ((quotientStackProjection G).obj ⟨W.unop, Discrete.mk u⟩)) :
    IsInvariantOpen G (Subfunctor.range m.hom)

AlgebraicGeometry.Stack.essImage_quotientStackProjection_iff_exists_twoFibreProductOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionIntoQuotientStackSubspace.lean, line 408. The attribute's comment: “the points of U covered by the 2-fibre product U' = 𝒵 ×_{[U/R]} U of Stacks 04Y6 are exactly those whose image in [U/R] is in the essential image of i; nothing carried”.

Stacks 0505: the locus the 2-fibre product of Stacks 04Y6 covers is the essential-image locus. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces and let i : 𝒵 ⟶ [U/R] be a 1-morphism over the big fppf site whose source is fibred in groupoids. A point x of U over an object W of the site is carried by an object of the 2-fibre product U ×_{[U/R]} 𝒵 — the U' Stacks 04Y6 forms, for the canonical atlas U ⟶ [U/R] of Stacks 044R — exactly when the image of x in [U/R] lies in the essential image of i.

Nothing is carried: this is the hypothesis hmem of AlgebraicGeometry.Stack.isInvariantLocallyClosed_range_of_isImmersion_essImage, in the shape Stacks 04Y6 states it, proved rather than assumed.

theorem essImage_quotientStackProjection_iff_exists_twoFibreProductOver
    (h𝒵 : 𝒵.p.IsFiberedInGroupoids) (W : (BigFppfOver C S hS)ᵒᵖ)
    (x : G.objects.obj.obj W) :
    i.toFunctor.essImage ((quotientStackProjection G).obj ⟨W.unop, Discrete.mk x⟩) ↔
      ∃ P : TwoFibreProductOver (fibredCategory C S hS G.objects.obj).val.p 𝒵.p
          (quotientStack G).p (quotientStackProjection G).toFunctor i.toFunctor,
        P.x = ⟨W.unop, Discrete.mk x⟩

AlgebraicGeometry.Stack.essImage_quotientStackProjection_iff_exists_twoFibreProductSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionIntoQuotientStackSubspace.lean, line 435. The attribute's comment: “the points of U covered by the apex of the canonical 2-fibre product square of Stacks 04Y6 at the atlas U ⟶ [U/R] are exactly those whose image in [U/R] is in the essential image of the other leg; nothing carried”.

Stacks 0505 for the canonical 2-fibre product square of Stacks 04Y6. The same statement as AlgebraicGeometry.Stack.essImage_quotientStackProjection_iff_exists_twoFibreProductOver, read on the apex of CategoryTheory.CatFiberedInGroupoids.twoFibreProductSquare at the canonical atlas AlgebraicGeometry.Stack.quotientStackProjectionHom of Stacks 044R and at a 1-morphism j : 𝒴 ⟶ [U/R] of categories fibred in groupoids. That square is the U' = 𝒰 ×_𝒳 𝒳' of Stacks 04Y6, formed at the universes a quotient stack lives at.

Nothing is carried.

theorem essImage_quotientStackProjection_iff_exists_twoFibreProductSquare
    (𝒴 : CatFiberedInGroupoids.{u, u + 1, u + 1, u + 1} (BigFppfOver C S hS))
    (j : 𝒴 ⟶ CatFiberedInGroupoids.mk (quotientStack G)
      (isFiberedInGroupoids_quotientStack G))
    (W : (BigFppfOver C S hS)ᵒᵖ) (x : G.objects.obj.obj W) :
    j.hom.toFunctor.essImage
        ((quotientStackProjection G).obj ⟨W.unop, Discrete.mk x⟩) ↔
      ∃ P : (CatFiberedInGroupoids.twoFibreProductSquare.{u, u + 1, u + 1, u + 1}
          (quotientStackProjectionHom G) j).pt.val.obj,
        P.x = ULiftHom.objUp ⟨W.unop, Discrete.mk x⟩

AlgebraicGeometry.Stack.exists_isInvariantLocallyClosed_groupoidPresentation_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionQuotientStackPresentation.lean, line 490.

Stacks 0505. Let G = (U, R, s, t, c) be a smooth groupoid in algebraic spaces over a scheme S of a big fppf site, and let i : 𝒵 ⟶ [U/R] be an immersion — a 1-morphism representable by algebraic spaces with the relative immersion property of Stacks 04XB, that is part (3) of Stacks 04YL — whose source satisfies descent. Then there are an R-invariant locally closed subspace Z ⊆ U in the sense of Stacks 044F, part (2), a presentation [Z/R_Z] ⟶ 𝒵 of 𝒵 in the sense of Stacks 04TI by the restriction R_Z of G to Z (Stacks 044B), and a 2-isomorphism making the triangle

[Z/R_Z] ⟶ 𝒵 ⟶ [U/R]        [Z/R_Z] ⟶ [U/R]

2-commutative, the second leg being the 1-morphism of Stacks 046Q induced by the canonical morphism of groupoids from the restriction. If i is a closed, respectively open, immersion then Z is a closed, respectively open, subspace of U.

Z is pinned down by the conclusion: it is, pointwise, the locus of U whose image in [U/R] lies in the essential image of i, which is the 𝒵 ×_{[U/R]} U of Stacks 04Y6 read as a subspace of U.

The subspace and its invariance are AlgebraicGeometry.Stack.exists_isInvariantLocallyClosed_range_of_isImmersion_quotientStack; smoothness of the restricted groupoid, the one place smoothness of G is used, is AlgebraicGeometry.GroupoidInAlgebraicSpaces.isSmoothGroupoid_restrict_invariant; and the equivalence together with the 2-commutative triangle is AlgebraicGeometry.Stack.exists_equivalenceOver_quotientStack_restrict, whose two inputs are full faithfulness of i (Stacks 05UK at the monomorphism Stacks 042R supplies, which is Stacks 0504) and the pointwise description of Z.

theorem exists_isInvariantLocallyClosed_groupoidPresentation_of_isImmersion
    (G : GroupoidInAlgebraicSpaces C S hS (baseSpace C S hS))
    (hG : GroupoidInAlgebraicSpaces.IsSmooth C S hS G)
    (h𝒵 : 𝒵.val.p.IsStack (BigFppfOver.topology C S hS))
    (i : 𝒵 ⟶ CatFiberedInGroupoids.mk (quotientStack G) (isFiberedInGroupoids_quotientStack G))
    (hi : IsRepresentableByAlgebraicSpaces C S hS i.hom)
    (himm : IsImmersion C S hS i) :
    ∃ (Z : Subfunctor G.objects.obj) (hZ : IsInvariantLocallyClosed G Z)
      (hsm : GroupoidInAlgebraicSpaces.IsSmooth C S hS
        (G.restrict (subspaceInclusion G Z hZ.1.1)).groupoid)
      (e : StacksRepresentableCFG.EquivalenceOver
        (quotientStack (G.restrict (subspaceInclusion G Z hZ.1.1)).groupoid).p 𝒵.val.p),
      Nonempty ((GroupoidPresentation.basedFunctor
            (⟨(G.restrict (subspaceInclusion G Z hZ.1.1)).groupoid, hsm, e⟩ :
              GroupoidPresentation C S hS 𝒵.val)).comp i.hom ≅
          quotientStackMap (G.restrict (subspaceInclusion G Z hZ.1.1)).hom) ∧
        (∀ (W : (BigFppfOver C S hS)ᵒᵖ) (u : G.objects.obj.obj W),
          u ∈ Z.obj W ↔ (CatFiberedInGroupoids.homFunctor i).essImage
            ((quotientStackProjection G).obj ⟨W.unop, Discrete.mk u⟩)) ∧
        (IsClosedImmersion C S hS i → Space.IsClosedSubspace C S hS Z) ∧
        (IsOpenImmersion C S hS i → Space.IsOpenSubspace C S hS Z)

AlgebraicGeometry.Stack.exists_isInvariantLocallyClosed_range_of_isImmersion_quotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackImmersionBaseChangeSpace.lean, line 315. The attribute's comment: “the R-invariant locally closed subspace Z of U cut out by an immersion into [U/R], together with its pointwise description as the locus of U whose image in [U/R] lies in the essential image of i; nothing carried -- the projection m of the 2-fibre product of Stacks 04Y6 and its immersion property are produced here rather than assumed”.

Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over an algebraic space A over a scheme S of a big fppf site, and let i : 𝒵 ⟶ [U/R] be an immersion which is representable by algebraic spaces. Then the locus of U whose image in [U/R] lies in the essential image of i is an R-invariant locally closed subspace Z ⊆ U; it is the range of an immersion of algebraic spaces m : U' ⟶ U.

theorem exists_isInvariantLocallyClosed_range_of_isImmersion_quotientStack
    (G : GroupoidInAlgebraicSpaces C S hS A)
    {𝒵 : CatFiberedInGroupoids.{u, u + 1, u + 1, u + 1} (BigFppfOver C S hS)}
    (i : 𝒵 ⟶ CatFiberedInGroupoids.mk (quotientStack G) (isFiberedInGroupoids_quotientStack G))
    (hi : IsRepresentableByAlgebraicSpaces C S hS i.hom)
    (himm : IsImmersion C S hS i) :
    ∃ (U' : AlgebraicSpaces C S hS) (m : U' ⟶ G.objects),
      Space.IsImmersion C S hS m.hom ∧
        IsInvariantLocallyClosed G (Subfunctor.range m.hom) ∧
        ∀ (W : (BigFppfOver C S hS)ᵒᵖ) (u : G.objects.obj.obj W),
          u ∈ (Subfunctor.range m.hom).obj W ↔
            i.hom.toFunctor.essImage
              ((quotientStackProjection G).obj ⟨W.unop, Discrete.mk u⟩)

AlgebraicGeometry.Stack.exists_isInvariantOpen_range_of_isOpenImmersion_quotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackImmersionBaseChangeSpace.lean, line 338. The attribute's comment: “the R-invariant open subspace of U, for an open immersion into [U/R]; nothing carried”.

The open-immersion case of AlgebraicGeometry.Stack.exists_isInvariantLocallyClosed_range_of_isImmersion_quotientStack: the locus is an R-invariant open subspace of U.

theorem exists_isInvariantOpen_range_of_isOpenImmersion_quotientStack
    (G : GroupoidInAlgebraicSpaces C S hS A)
    {𝒵 : CatFiberedInGroupoids.{u, u + 1, u + 1, u + 1} (BigFppfOver C S hS)}
    (i : 𝒵 ⟶ CatFiberedInGroupoids.mk (quotientStack G) (isFiberedInGroupoids_quotientStack G))
    (hi : IsRepresentableByAlgebraicSpaces C S hS i.hom)
    (hopen : IsOpenImmersion C S hS i) :
    ∃ (U' : AlgebraicSpaces C S hS) (m : U' ⟶ G.objects),
      Space.IsOpenImmersion C S hS m.hom ∧
        IsInvariantOpen G (Subfunctor.range m.hom) ∧
        ∀ (W : (BigFppfOver C S hS)ᵒᵖ) (u : G.objects.obj.obj W),
          u ∈ (Subfunctor.range m.hom).obj W ↔
            i.hom.toFunctor.essImage
              ((quotientStackProjection G).obj ⟨W.unop, Discrete.mk u⟩)

AlgebraicGeometry.Stack.exists_isInvariantClosed_range_of_isClosedImmersion_quotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackImmersionBaseChangeSpace.lean, line 361. The attribute's comment: “the R-invariant closed subspace of U, for a closed immersion into [U/R]; nothing carried”.

The closed-immersion case of AlgebraicGeometry.Stack.exists_isInvariantLocallyClosed_range_of_isImmersion_quotientStack: the locus is an R-invariant closed subspace of U.

theorem exists_isInvariantClosed_range_of_isClosedImmersion_quotientStack
    (G : GroupoidInAlgebraicSpaces C S hS A)
    {𝒵 : CatFiberedInGroupoids.{u, u + 1, u + 1, u + 1} (BigFppfOver C S hS)}
    (i : 𝒵 ⟶ CatFiberedInGroupoids.mk (quotientStack G) (isFiberedInGroupoids_quotientStack G))
    (hi : IsRepresentableByAlgebraicSpaces C S hS i.hom)
    (hclosed : IsClosedImmersion C S hS i) :
    ∃ (U' : AlgebraicSpaces C S hS) (m : U' ⟶ G.objects),
      Space.IsClosedImmersion C S hS m.hom ∧
        IsInvariantClosed G (Subfunctor.range m.hom) ∧
        ∀ (W : (BigFppfOver C S hS)ᵒᵖ) (u : G.objects.obj.obj W),
          u ∈ (Subfunctor.range m.hom).obj W ↔
            i.hom.toFunctor.essImage
              ((quotientStackProjection G).obj ⟨W.unop, Discrete.mk u⟩)
Tag 04YN, a lemma

Tag 04YN in the Stacks Project.

AlgebraicGeometry.Stack.isImmersion_quotientStackMap_of_invariantRestrictionBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InvariantSubspaceQuotientImmersion.lean, line 238. The attribute's comment: “the immersion [Z/R_Z] ⟶ [U/R] for an invariant locally closed subspace”.

Stacks 04YN, the immersion. For a smooth groupoid G in algebraic spaces and an invariant locally closed subspace Z of its object space, the 1-morphism [Z/R_Z] ⟶ [U/R] of Stacks 044B is an immersion of algebraic stacks: it is representable by algebraic spaces and an immersion in the sense of Stacks 04XB.

theorem isImmersion_quotientStackMap_of_invariantRestrictionBaseChange
    {G : GroupoidInAlgebraicSpaces C S hS B} (hG : IsSmooth C S hS G)
    {Z : Subfunctor G.objects.obj} (hZ : IsInvariantLocallyClosed G Z) :
    IsRepresentableByAlgebraicSpaces C S hS
        (quotientStackMapHom (G.restrict (subspaceInclusion G Z hZ.1.1)).hom).hom ∧
      Stack.IsImmersion C S hS
        (quotientStackMapHom (G.restrict (subspaceInclusion G Z hZ.1.1)).hom)

AlgebraicGeometry.Stack.isOpenImmersion_quotientStackMap_of_invariantRestrictionBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InvariantSubspaceQuotientImmersion.lean, line 255. The attribute's comment: “the open immersion [Z/R_Z] ⟶ [U/R] for an invariant open subspace”.

Stacks 04YN, the open immersion. For a smooth groupoid G in algebraic spaces and an invariant open subspace Z of its object space, the 1-morphism [Z/R_Z] ⟶ [U/R] of Stacks 044B is an open immersion of algebraic stacks: it is representable by algebraic spaces and an open immersion in the sense of Stacks 04XB.

theorem isOpenImmersion_quotientStackMap_of_invariantRestrictionBaseChange
    {G : GroupoidInAlgebraicSpaces C S hS B} (hG : IsSmooth C S hS G)
    {Z : Subfunctor G.objects.obj} (hZ : IsInvariantOpen G Z) :
    IsRepresentableByAlgebraicSpaces C S hS
        (quotientStackMapHom (G.restrict (subspaceInclusion G Z hZ.1.1)).hom).hom ∧
      Stack.IsOpenImmersion C S hS
        (quotientStackMapHom (G.restrict (subspaceInclusion G Z hZ.1.1)).hom)

AlgebraicGeometry.Stack.isClosedImmersion_quotientStackMap_of_invariantRestrictionBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InvariantSubspaceQuotientImmersion.lean, line 273. The attribute's comment: “the closed immersion [Z/R_Z] ⟶ [U/R] for an invariant closed subspace”.

Stacks 04YN, the closed immersion. For a smooth groupoid G in algebraic spaces and an invariant closed subspace Z of its object space, the 1-morphism [Z/R_Z] ⟶ [U/R] of Stacks 044B is a closed immersion of algebraic stacks: it is representable by algebraic spaces and a closed immersion in the sense of Stacks 04XB.

theorem isClosedImmersion_quotientStackMap_of_invariantRestrictionBaseChange
    {G : GroupoidInAlgebraicSpaces C S hS B} (hG : IsSmooth C S hS G)
    {Z : Subfunctor G.objects.obj} (hZ : IsInvariantClosed G Z) :
    IsRepresentableByAlgebraicSpaces C S hS
        (quotientStackMapHom (G.restrict (subspaceInclusion G Z hZ.1.1)).hom).hom ∧
      Stack.IsClosedImmersion C S hS
        (quotientStackMapHom (G.restrict (subspaceInclusion G Z hZ.1.1)).hom)
Tag 04YM, a definition

Tag 04YM in the Stacks Project.

AlgebraicGeometry.Stack.OpenSubstack, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Substack.lean, line 107. The attribute's comment: “open_substack”.

Stacks 04YM, part (1). An open substack of an algebraic stack 𝒳 over S is a strictly full subcategory of 𝒳 which is an algebraic stack and whose canonical inclusion into 𝒳 is an open immersion.

structure OpenSubstack (𝒳 : AlgebraicStacks.{u, w} B S hS)

AlgebraicGeometry.Stack.OpenSubstack.ext, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Substack.lean, line 120. The attribute's comment: “open_substack”.

Two open substacks with the same objects are equal.

theorem OpenSubstack.ext {𝒳 : AlgebraicStacks.{u, w} B S hS} {U V : OpenSubstack 𝒳}
    (h : U.property = V.property) : U = V

AlgebraicGeometry.Stack.fullSubcategoryInclusion_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Substack.lean, line 144. The attribute's comment: “open_substack”.

On objects, the canonical inclusion forgets the membership proof.

theorem fullSubcategoryInclusion_obj (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (P : ObjectProperty 𝒳.val.val.obj)
    (hP : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 P))
    (X : P.FullSubcategory) :
    (fullSubcategoryInclusion 𝒳 P hP).hom.hom.toFunctor.obj X = X.obj

AlgebraicGeometry.Stack.fullSubcategoryInclusion_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Substack.lean, line 153. The attribute's comment: “open_substack”.

On morphisms, the canonical inclusion forgets the membership proof.

theorem fullSubcategoryInclusion_map (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (P : ObjectProperty 𝒳.val.val.obj)
    (hP : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 P))
    {X Y : P.FullSubcategory} (f : X ⟶ Y) :
    (fullSubcategoryInclusion 𝒳 P hP).hom.hom.toFunctor.map f = f.hom

AlgebraicGeometry.Stack.IsClosedSubstack, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Substack.lean, line 165. The attribute's comment: “closed_substack”.

Stacks 04YM, part (2). A property of the objects of an algebraic stack 𝒳 over S selects a closed substack when it is closed under isomorphism, its full subcategory is an algebraic stack, and the canonical inclusion of that full subcategory into 𝒳 is a closed immersion.

abbrev IsClosedSubstack (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (P : ObjectProperty 𝒳.val.val.obj) : Prop

AlgebraicGeometry.Stack.IsLocallyClosedSubstack, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Substack.lean, line 176. The attribute's comment: “locally_closed_substack”.

Stacks 04YM, part (3). A property of the objects of an algebraic stack 𝒳 over S selects a locally closed substack when it is closed under isomorphism, its full subcategory is an algebraic stack, and the canonical inclusion of that full subcategory into 𝒳 is an immersion.

abbrev IsLocallyClosedSubstack (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (P : ObjectProperty 𝒳.val.val.obj) : Prop
Tag 0506, a lemma

Tag 0506 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyClosedSubstack_essImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionSubstack.lean, line 363. The attribute's comment: “the image is a locally closed substack”.

Stacks 0506, the image is a locally closed substack. The essential image of an immersion of algebraic stacks over S cuts out a locally closed substack of its target.

It is closed under isomorphism because an essential image always is; its full subcategory is an algebraic stack by Stacks 03YQ; and the inclusion of that full subcategory is an immersion because the immersion i factors through it by an equivalence, so Stacks 0457 transports both representability by algebraic spaces and the Stacks 04XB immersion condition.

theorem isLocallyClosedSubstack_essImage (i : 𝒵 ⟶ 𝒳) (hi : IsImmersion B S hS i) :
    IsLocallyClosedSubstack 𝒳 (CatFiberedInGroupoids.homFunctor i.hom).essImage

AlgebraicGeometry.Stack.AlgebraicStacks.exists_isEquivalence_to_essImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionSubstack.lean, line 372. The attribute's comment: “the factorization through the image”.

Stacks 0506, the factorization. An immersion of algebraic stacks over S factors as a 1-morphism onto the full subcategory cut out by its essential image whose underlying functor is an equivalence of categories, followed by the inclusion of that full subcategory.

theorem exists_isEquivalence_to_essImage (i : 𝒵 ⟶ 𝒳) (hi : IsImmersion B S hS i)
    (hP : IsAlgebraicStack.{u, w} B S hS
      (fullSubcategoryBased 𝒳 (CatFiberedInGroupoids.homFunctor i.hom).essImage)) :
    ∃ f : 𝒵 ⟶ fullSubcategoryAlgebraicStack 𝒳
        (CatFiberedInGroupoids.homFunctor i.hom).essImage hP,
      Functor.IsEquivalence (CatFiberedInGroupoids.homFunctor f.hom) ∧
        Nonempty (f ≫ fullSubcategoryInclusion 𝒳
          (CatFiberedInGroupoids.homFunctor i.hom).essImage hP ≅ i)

AlgebraicGeometry.Stack.AlgebraicStacks.eq_essImage_of_isEquivalence_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionSubstack.lean, line 394. The attribute's comment: “uniqueness of the substack”.

Stacks 0506, uniqueness. A strictly full subcategory of an algebraic stack which is an algebraic stack and through which an immersion factors by a 1-morphism whose underlying functor is an equivalence of categories is cut out by the essential image of the immersion.

The essential image of the inclusion of a strictly full subcategory is the property cutting it out, and precomposing with an essentially surjective functor does not change an essential image, so the essential image of the immersion is that property.

theorem eq_essImage_of_isEquivalence_factorization (i : 𝒵 ⟶ 𝒳)
    (P : ObjectProperty 𝒳.val.val.obj) (hstrict : P.IsClosedUnderIsomorphisms)
    (hP : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 P))
    (f : 𝒵 ⟶ fullSubcategoryAlgebraicStack 𝒳 P hP)
    (hf : Functor.IsEquivalence (CatFiberedInGroupoids.homFunctor f.hom))
    (α : f ≫ fullSubcategoryInclusion 𝒳 P hP ≅ i) :
    P = (CatFiberedInGroupoids.homFunctor i.hom).essImage

AlgebraicGeometry.Stack.AlgebraicStacks.existsUnique_locallyClosedSubstack_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionSubstack.lean, line 427.

Stacks 0506. For an immersion i : 𝒵 ⟶ 𝒳 of algebraic stacks over S there is a unique locally closed substack of 𝒳 through which i factors as a 1-morphism whose underlying functor is an equivalence of categories followed by the inclusion of the substack.

That substack is cut out by the essential image of the functor underlying i.

theorem existsUnique_locallyClosedSubstack_of_isImmersion (i : 𝒵 ⟶ 𝒳)
    (hi : IsImmersion B S hS i) :
    ∃! P : ObjectProperty 𝒳.val.val.obj,
      IsLocallyClosedSubstack 𝒳 P ∧
        ∃ (hP : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 P))
          (f : 𝒵 ⟶ fullSubcategoryAlgebraicStack 𝒳 P hP),
          Functor.IsEquivalence (CatFiberedInGroupoids.homFunctor f.hom) ∧
            Nonempty (f ≫ fullSubcategoryInclusion 𝒳 P hP ≅ i)

AlgebraicGeometry.Stack.AlgebraicStacks.isClosedSubstack_essImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionSubstack.lean, line 449. The attribute's comment: “the image of a closed immersion is a closed substack”.

Stacks 0506, the closed case. The essential image of a closed immersion of algebraic stacks over S cuts out a closed substack of its target.

A closed immersion is an immersion, so the essential image cuts out a locally closed substack; the closed-immersion condition on the inclusion is the condition on i transported across the equivalence by Stacks 0457.

theorem isClosedSubstack_essImage (i : 𝒵 ⟶ 𝒳) (hi : IsClosedImmersion B S hS i) :
    IsClosedSubstack 𝒳 (CatFiberedInGroupoids.homFunctor i.hom).essImage

AlgebraicGeometry.Stack.AlgebraicStacks.exists_openSubstack_essImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionSubstack.lean, line 464. The attribute's comment: “the image of an open immersion is an open substack”.

Stacks 0506, the open case. The essential image of an open immersion of algebraic stacks over S is the object property of an open substack of its target.

An open immersion is an immersion, so the essential image cuts out a locally closed substack; the open-immersion condition on the inclusion is the condition on i transported across the equivalence by Stacks 0457.

theorem exists_openSubstack_essImage (i : 𝒵 ⟶ 𝒳) (hi : IsOpenImmersion B S hS i) :
    ∃ U : OpenSubstack 𝒳,
      U.property = (CatFiberedInGroupoids.homFunctor i.hom).essImage
Tag 0507, a lemma

Tag 0507 in the Stacks Project.

AlgebraicGeometry.Stack.factorsThroughSubstack_iff_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubstackFactorizationPresentation.lean, line 386. The attribute's comment: “factorization_criterion”.

Stacks 0507, the factorization criterion. Let 𝒳 be an algebraic stack over S presented by a smooth groupoid in algebraic spaces G through an equivalence E over the big fppf site, let P cut out an open, closed or locally closed substack of 𝒳, and let f : 𝒴 ⟶ 𝒳 be a 1-morphism of algebraic stacks. Then f factors through the substack, over the big fppf site and up to a 2-isomorphism, if and only if the base change of f along the presentation S_U ⟶ 𝒳 factors through the base change of the substack.

The proof is pointwise on both sides, and the content is that membership of the substack is local on the site; see the module documentation.

theorem factorsThroughSubstack_iff_presentation
    (𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS)
    (G : GroupoidInAlgebraicSpaces B S hS (baseSpace B S hS))
    (_hG : GroupoidInAlgebraicSpaces.IsSmooth B S hS G)
    (E : (quotientStack G).obj ⥤ 𝒳.val.val.obj)
    [E.IsEquivalence]
    (hE : E ⋙ 𝒳.val.val.p = (quotientStack G).p)
    (P : ObjectProperty 𝒳.val.val.obj)
    (hP : (IsLocallyClosedSubstack 𝒳 P ∨ IsClosedSubstack 𝒳 P) ∨
      ∃ V : OpenSubstack 𝒳, V.property = P)
    (f : 𝒴 ⟶ 𝒳) :
    let U := (fibredCategory B S hS G.objects.obj).val
    let p := (quotientStackProjection G).comp
      (⟨E, hE⟩ : (quotientStack G) ⥤ᵇ 𝒳.val.val)
    let F := TwoFibreProductOver.structureFunctor U.p 𝒴.val.val.p 𝒳.val.val.p
      p.toFunctor f.hom.hom.toFunctor
    let D := BasedCategory.ofFunctor F
    let q : D ⥤ᵇ U :=
      { toFunctor := TwoFibreProductOver.fst U.p 𝒴.val.val.p 𝒳.val.val.p
          p.toFunctor f.hom.hom.toFunctor
        w := TwoFibreProductOver.fst_comp_eq }
    let i := fullSubcategoryBasedInclusion 𝒳 P
    let Z := BasedCategory.ofFunctor
      (TwoFibreProductOver.structureFunctor U.p
        (fullSubcategoryBased 𝒳 P).p
        𝒳.val.val.p p.toFunctor i.toFunctor)
    let z : Z ⥤ᵇ U :=
      { toFunctor := TwoFibreProductOver.fst U.p
          (fullSubcategoryBased 𝒳 P).p
          𝒳.val.val.p p.toFunctor i.toFunctor
        w := TwoFibreProductOver.fst_comp_eq }
    (∃ g : 𝒴.val.val ⥤ᵇ fullSubcategoryBased 𝒳 P,
      Nonempty (g.comp i ≅ f.hom.hom)) ↔
      (∃ g : D ⥤ᵇ Z, Nonempty (g.comp z ≅ q))

AlgebraicGeometry.Stack.exists_equiv_isInvariantLocallyClosed_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubstackPresentationCorrespondence.lean, line 505. The attribute's comment: “locally closed”.

Stacks 0507, locally closed substacks. Let [U/R] ⟶ 𝒳 be a presentation of an algebraic stack. There is a canonical bijection from the locally closed substacks 𝒵 of 𝒳 to the R-invariant locally closed subspaces of U, sending 𝒵 to U ×_𝒳 𝒵. Moreover, a 1-morphism f : 𝒴 ⟶ 𝒳 of algebraic stacks factors through 𝒵 if and only if 𝒴 ×_𝒳 U ⟶ U factors through U ×_𝒳 𝒵.

Here [U/R] ⟶ 𝒳 is a presentation of the algebraic stack 𝒳 (Stacks 04TI), and π : U ⟶ 𝒳 is the canonical projection followed by the equivalence. The bijection e sends 𝒵 to the subspace of U that is the image of the projection U ×_𝒳 𝒵 ⟶ U from the 2-fibre product (first conjunct). For every 1-morphism f : 𝒴 ⟶ 𝒳 of algebraic stacks, f factors through 𝒵 over the site and up to a 2-isomorphism exactly when the projection 𝒴 ×_𝒳 U ⟶ U factors through U ×_𝒳 𝒵 (second conjunct), and exactly when the U-component of every object of 𝒴 ×_𝒳 U lies in e 𝒵 (third conjunct), which is to say that 𝒴 ×_𝒳 U ⟶ U factors through the subspace e 𝒵.

theorem exists_equiv_isInvariantLocallyClosed_presentation :
    ∃ e : {P : ObjectProperty 𝒳.val.val.obj // IsLocallyClosedSubstack 𝒳 P} ≃
        {Z : Subfunctor Pr.groupoid.objects.obj // IsInvariantLocallyClosed Pr.groupoid Z},
      ∀ P : {P : ObjectProperty 𝒳.val.val.obj // IsLocallyClosedSubstack 𝒳 P},
        (∀ (T : BigFppfOver B S hS) (u : Pr.groupoid.objects.obj.obj (op T)),
          u ∈ (e P).1.obj (op T) ↔
            ∃ d : TwoFibreProductOver (fibredCategory B S hS Pr.groupoid.objects.obj).val.p
                (fullSubcategoryBased 𝒳 P.1).p 𝒳.val.val.p
                (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                  Pr.basedFunctor.w).toFunctor
                (fullSubcategoryBasedInclusion 𝒳 P.1).toFunctor,
              d.x = ⟨T, Discrete.mk u⟩) ∧
        ∀ (𝒴 : AlgebraicStacks.{u, w} B S hS) (f : 𝒴 ⟶ 𝒳),
          ((∃ g : 𝒴.val.val ⥤ᵇ fullSubcategoryBased 𝒳 P.1,
              Nonempty (g.comp (fullSubcategoryBasedInclusion 𝒳 P.1) ≅ f.hom.hom)) ↔
            ∃ g : BasedCategory.ofFunctor (TwoFibreProductOver.structureFunctor
                  (fibredCategory B S hS Pr.groupoid.objects.obj).val.p 𝒴.val.val.p 𝒳.val.val.p
                  (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor f.hom.hom.toFunctor) ⥤ᵇ
                BasedCategory.ofFunctor (TwoFibreProductOver.structureFunctor
                  (fibredCategory B S hS Pr.groupoid.objects.obj).val.p
                  (fullSubcategoryBased 𝒳 P.1).p 𝒳.val.val.p
                  (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor
                  (fullSubcategoryBasedInclusion 𝒳 P.1).toFunctor),
              Nonempty (g.comp (TwoFibreProductOver.fstBased (fullSubcategoryBased 𝒳 P.1).p
                  𝒳.val.val.p (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor
                  (fullSubcategoryBasedInclusion 𝒳 P.1).toFunctor) ≅
                TwoFibreProductOver.fstBased 𝒴.val.val.p 𝒳.val.val.p
                  (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor f.hom.hom.toFunctor)) ∧
          ((∃ g : 𝒴.val.val ⥤ᵇ fullSubcategoryBased 𝒳 P.1,
              Nonempty (g.comp (fullSubcategoryBasedInclusion 𝒳 P.1) ≅ f.hom.hom)) ↔
            ∀ d : TwoFibreProductOver (fibredCategory B S hS Pr.groupoid.objects.obj).val.p
                𝒴.val.val.p 𝒳.val.val.p
                (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                  Pr.basedFunctor.w).toFunctor f.hom.hom.toFunctor,
              d.x.fiber.as ∈ (e P).1.obj (op d.x.base))

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

Stacks 0507, closed substacks. Let [U/R] ⟶ 𝒳 be a presentation of an algebraic stack. There is a canonical bijection from the closed substacks 𝒵 of 𝒳 to the R-invariant closed subspaces of U, sending 𝒵 to U ×_𝒳 𝒵. Moreover, a 1-morphism f : 𝒴 ⟶ 𝒳 of algebraic stacks factors through 𝒵 if and only if 𝒴 ×_𝒳 U ⟶ U factors through U ×_𝒳 𝒵.

Here [U/R] ⟶ 𝒳 is a presentation of the algebraic stack 𝒳 (Stacks 04TI), and π : U ⟶ 𝒳 is the canonical projection followed by the equivalence. The bijection e sends 𝒵 to the subspace of U that is the image of the projection U ×_𝒳 𝒵 ⟶ U from the 2-fibre product (first conjunct). For every 1-morphism f : 𝒴 ⟶ 𝒳 of algebraic stacks, f factors through 𝒵 over the site and up to a 2-isomorphism exactly when the projection 𝒴 ×_𝒳 U ⟶ U factors through U ×_𝒳 𝒵 (second conjunct), and exactly when the U-component of every object of 𝒴 ×_𝒳 U lies in e 𝒵 (third conjunct), which is to say that 𝒴 ×_𝒳 U ⟶ U factors through the subspace e 𝒵.

theorem exists_equiv_isInvariantClosed_presentation :
    ∃ e : {P : ObjectProperty 𝒳.val.val.obj // IsClosedSubstack 𝒳 P} ≃
        {Z : Subfunctor Pr.groupoid.objects.obj // IsInvariantClosed Pr.groupoid Z},
      ∀ P : {P : ObjectProperty 𝒳.val.val.obj // IsClosedSubstack 𝒳 P},
        (∀ (T : BigFppfOver B S hS) (u : Pr.groupoid.objects.obj.obj (op T)),
          u ∈ (e P).1.obj (op T) ↔
            ∃ d : TwoFibreProductOver (fibredCategory B S hS Pr.groupoid.objects.obj).val.p
                (fullSubcategoryBased 𝒳 P.1).p 𝒳.val.val.p
                (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                  Pr.basedFunctor.w).toFunctor
                (fullSubcategoryBasedInclusion 𝒳 P.1).toFunctor,
              d.x = ⟨T, Discrete.mk u⟩) ∧
        ∀ (𝒴 : AlgebraicStacks.{u, w} B S hS) (f : 𝒴 ⟶ 𝒳),
          ((∃ g : 𝒴.val.val ⥤ᵇ fullSubcategoryBased 𝒳 P.1,
              Nonempty (g.comp (fullSubcategoryBasedInclusion 𝒳 P.1) ≅ f.hom.hom)) ↔
            ∃ g : BasedCategory.ofFunctor (TwoFibreProductOver.structureFunctor
                  (fibredCategory B S hS Pr.groupoid.objects.obj).val.p 𝒴.val.val.p 𝒳.val.val.p
                  (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor f.hom.hom.toFunctor) ⥤ᵇ
                BasedCategory.ofFunctor (TwoFibreProductOver.structureFunctor
                  (fibredCategory B S hS Pr.groupoid.objects.obj).val.p
                  (fullSubcategoryBased 𝒳 P.1).p 𝒳.val.val.p
                  (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor
                  (fullSubcategoryBasedInclusion 𝒳 P.1).toFunctor),
              Nonempty (g.comp (TwoFibreProductOver.fstBased (fullSubcategoryBased 𝒳 P.1).p
                  𝒳.val.val.p (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor
                  (fullSubcategoryBasedInclusion 𝒳 P.1).toFunctor) ≅
                TwoFibreProductOver.fstBased 𝒴.val.val.p 𝒳.val.val.p
                  (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor f.hom.hom.toFunctor)) ∧
          ((∃ g : 𝒴.val.val ⥤ᵇ fullSubcategoryBased 𝒳 P.1,
              Nonempty (g.comp (fullSubcategoryBasedInclusion 𝒳 P.1) ≅ f.hom.hom)) ↔
            ∀ d : TwoFibreProductOver (fibredCategory B S hS Pr.groupoid.objects.obj).val.p
                𝒴.val.val.p 𝒳.val.val.p
                (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                  Pr.basedFunctor.w).toFunctor f.hom.hom.toFunctor,
              d.x.fiber.as ∈ (e P).1.obj (op d.x.base))

AlgebraicGeometry.Stack.exists_equiv_isInvariantOpen_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SubstackPresentationCorrespondence.lean, line 630. The attribute's comment: “open”.

Stacks 0507, open substacks. Let [U/R] ⟶ 𝒳 be a presentation of an algebraic stack. There is a canonical bijection from the open substacks 𝒵 of 𝒳 to the R-invariant open subspaces of U, sending 𝒵 to U ×_𝒳 𝒵. Moreover, a 1-morphism f : 𝒴 ⟶ 𝒳 of algebraic stacks factors through 𝒵 if and only if 𝒴 ×_𝒳 U ⟶ U factors through U ×_𝒳 𝒵.

Here [U/R] ⟶ 𝒳 is a presentation of the algebraic stack 𝒳 (Stacks 04TI), and π : U ⟶ 𝒳 is the canonical projection followed by the equivalence. The bijection e sends 𝒵 to the subspace of U that is the image of the projection U ×_𝒳 𝒵 ⟶ U from the 2-fibre product (first conjunct). For every 1-morphism f : 𝒴 ⟶ 𝒳 of algebraic stacks, f factors through 𝒵 over the site and up to a 2-isomorphism exactly when the projection 𝒴 ×_𝒳 U ⟶ U factors through U ×_𝒳 𝒵 (second conjunct), and exactly when the U-component of every object of 𝒴 ×_𝒳 U lies in e 𝒵 (third conjunct), which is to say that 𝒴 ×_𝒳 U ⟶ U factors through the subspace e 𝒵. An R-invariant open subspace is one whose inverse image under the source map is contained in its inverse image under the target map (Stacks 044F, part (1)).

theorem exists_equiv_isInvariantOpen_presentation :
    ∃ e : OpenSubstack 𝒳 ≃
        {Z : Subfunctor Pr.groupoid.objects.obj // IsInvariantOpen Pr.groupoid Z},
      ∀ P : OpenSubstack 𝒳,
        (∀ (T : BigFppfOver B S hS) (u : Pr.groupoid.objects.obj.obj (op T)),
          u ∈ (e P).1.obj (op T) ↔
            ∃ d : TwoFibreProductOver (fibredCategory B S hS Pr.groupoid.objects.obj).val.p
                (fullSubcategoryBased 𝒳 P.property).p 𝒳.val.val.p
                (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                  Pr.basedFunctor.w).toFunctor
                (fullSubcategoryBasedInclusion 𝒳 P.property).toFunctor,
              d.x = ⟨T, Discrete.mk u⟩) ∧
        ∀ (𝒴 : AlgebraicStacks.{u, w} B S hS) (f : 𝒴 ⟶ 𝒳),
          ((∃ g : 𝒴.val.val ⥤ᵇ fullSubcategoryBased 𝒳 P.property,
              Nonempty (g.comp (fullSubcategoryBasedInclusion 𝒳 P.property) ≅ f.hom.hom)) ↔
            ∃ g : BasedCategory.ofFunctor (TwoFibreProductOver.structureFunctor
                  (fibredCategory B S hS Pr.groupoid.objects.obj).val.p 𝒴.val.val.p 𝒳.val.val.p
                  (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor f.hom.hom.toFunctor) ⥤ᵇ
                BasedCategory.ofFunctor (TwoFibreProductOver.structureFunctor
                  (fibredCategory B S hS Pr.groupoid.objects.obj).val.p
                  (fullSubcategoryBased 𝒳 P.property).p 𝒳.val.val.p
                  (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor
                  (fullSubcategoryBasedInclusion 𝒳 P.property).toFunctor),
              Nonempty (g.comp (TwoFibreProductOver.fstBased (fullSubcategoryBased 𝒳 P.property).p
                  𝒳.val.val.p (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor
                  (fullSubcategoryBasedInclusion 𝒳 P.property).toFunctor) ≅
                TwoFibreProductOver.fstBased 𝒴.val.val.p 𝒳.val.val.p
                  (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                    Pr.basedFunctor.w).toFunctor f.hom.hom.toFunctor)) ∧
          ((∃ g : 𝒴.val.val ⥤ᵇ fullSubcategoryBased 𝒳 P.property,
              Nonempty (g.comp (fullSubcategoryBasedInclusion 𝒳 P.property) ≅ f.hom.hom)) ↔
            ∀ d : TwoFibreProductOver (fibredCategory B S hS Pr.groupoid.objects.obj).val.p
                𝒴.val.val.p 𝒳.val.val.p
                (presentationProjection Pr.groupoid Pr.basedFunctor.toFunctor
                  Pr.basedFunctor.w).toFunctor f.hom.hom.toFunctor,
              d.x.fiber.as ∈ (e P).1.obj (op d.x.base))
Tag 06FJ, a lemma

Tag 06FJ in the Stacks Project.

AlgebraicGeometry.Stack.OpenSubstack.isOpen_pointSet, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackPoints.lean, line 131. The attribute's comment: “the point set of an open substack is open, so the rule is defined”.

The rule of Stacks 06FJ is defined. The set of points of an algebraic stack lying in an open substack is open: it is the range of the map on points of the inclusion, which is an open map because the inclusion is an open immersion.

theorem isOpen_pointSet (W : OpenSubstack 𝒳) :
    @IsOpen _ (pointTopology B S hS 𝒳.val) (W.pointSet B S hS)

AlgebraicGeometry.Stack.OpenSubstack.opens, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackPoints.lean, line 142. The attribute's comment: “the rule”.

The rule 𝒰 ↦ |𝒰| of Stacks 06FJ: the point set of an open substack of 𝒳, as an open subset of the topological space of points of 𝒳.

noncomputable def opens (W : OpenSubstack 𝒳) :
    letI := pointTopology B S hS 𝒳.val
    TopologicalSpace.Opens (AlgebraicStacks.points B S hS 𝒳)

AlgebraicGeometry.Stack.OpenSubstack.pointSet_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackPoints.lean, line 151. The attribute's comment: “inclusion-preservation for the point set of an open substack”.

The rule of Stacks 06FJ preserves inclusions. An open substack contained in another has a smaller point set.

theorem pointSet_mono {U V : OpenSubstack 𝒳} (h : U.property ≤ V.property) :
    U.pointSet B S hS ⊆ V.pointSet B S hS

AlgebraicGeometry.Stack.OpenSubstack.opens_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackPoints.lean, line 161. The attribute's comment: “inclusion-preservation for the rule U goes to |U| as an open subset of the point space”.

The rule of Stacks 06FJ preserves inclusions, for the rule 𝒰 ↦ |𝒰| of AlgebraicGeometry.Stack.OpenSubstack.opens.

theorem opens_mono {U V : OpenSubstack 𝒳} (h : U.property ≤ V.property) :
    letI := pointTopology B S hS 𝒳.val
    opens B S hS U ≤ opens B S hS V

AlgebraicGeometry.Stack.OpenSubstack.bijective_opens_and_opens_le_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackPoints.lean, line 530.

Stacks 06FJ. Let 𝒳 be an algebraic stack. The rule 𝒰 ↦ |𝒰| defines an inclusion preserving bijection between open substacks of 𝒳 and open subsets of |𝒳|: the rule AlgebraicGeometry.Stack.OpenSubstack.opens is bijective, and |𝒰| ⊆ |𝒱| holds exactly when 𝒰 ⊆ 𝒱.

Injectivity, and the reflection of inclusions, is AlgebraicGeometry.Stack.OpenSubstack.property_le_of_pointSet_subset; surjectivity is AlgebraicGeometry.Stack.OpenSubstack.ofIsOpen with AlgebraicGeometry.Stack.OpenSubstack.pointSet_ofIsOpen; preservation of inclusions is AlgebraicGeometry.Stack.OpenSubstack.pointSet_mono.

theorem bijective_opens_and_opens_le_iff :
    letI := pointTopology B S hS 𝒳.val
    Function.Bijective (opens B S hS (𝒳 := 𝒳)) ∧
      ∀ U V : OpenSubstack 𝒳, opens B S hS U ≤ opens B S hS V ↔ U ≤ V
Tag 05UP, a lemma

Tag 05UP in the Stacks Project.

AlgebraicGeometry.Stack.exists_openSubstack_isOpenImmersion_smooth_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenImageSubstack.lean, line 389. The attribute's comment: “the algebraic stack, the open immersion into the given stack and the smooth surjection from the open subspace, all three together with the 2-commutativity of the resulting square. The stack is constructed as the open substack of Stacks 04YM whose point set is the image of the points of the open subspace, by Stacks 06FJ”.

Stacks 05UP. Let 𝒳 be an algebraic stack over S, let U be an algebraic space over S with a surjective smooth 1-morphism f : U ⟶ 𝒳, and let i : V ⟶ U be an open immersion of presheaves on the big fppf site of S. Then V is an algebraic space over S and there are an algebraic stack 𝒴 over S, an open immersion j : 𝒴 ⟶ 𝒳 and a surjective smooth 1-morphism q : V ⟶ 𝒴 making the square (i, f, q, j) 2-commute.

The algebraic stack 𝒴 is the open substack of 𝒳 whose points are the image of |V|, and q is the factorization of V ⟶ 𝒳 through it, so the three pieces are produced from one construction rather than chosen from an existential; the 2-commutativity is an identity.

theorem exists_openSubstack_isOpenImmersion_smooth_surjective
    {U V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hU : IsAlgebraicSpace B S hS U) {i : V ⟶ U}
    (hi : Space.IsOpenImmersion B S hS i)
    {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (f : algebraicSpaceStack.{u, w} B S hS U hU ⟶ 𝒳)
    (hfsm : AlgebraicStacks.IsSmooth B S hS f)
    (_hfsurj : IsSurjective B S hS f) :
    ∃ (hV : IsAlgebraicSpace B S hS V) (𝒴 : AlgebraicStacks.{u, w} B S hS)
      (j : 𝒴 ⟶ 𝒳) (q : algebraicSpaceStack.{u, w} B S hS V hV ⟶ 𝒴),
      AlgebraicStacks.IsOpenImmersion B S hS j ∧
        AlgebraicStacks.IsSmooth B S hS q ∧
          IsSurjective B S hS q ∧
            Nonempty (algebraicSpaceStackMap.{u, w} B S hS hV hU i ≫ f ≅ q ≫ j)
Tag 05UQ, a lemma

Tag 05UQ in the Stacks Project.

AlgebraicGeometry.Stack.OpenSubstack.eq_of_isUnion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackUnion.lean, line 130. The attribute's comment: “uniqueness of the union”.

The union of a family of open substacks is unique: an open substack of 𝒳 which contains every member of the family and is covered by the family is determined by the family. This is what makes the notation ⋃_{i ∈ I} 𝒳ᵢ of the source legitimate.

theorem eq_of_isUnion {𝒳 : AlgebraicStacks.{u, w} B S hS} {I : Type*} {𝒰 : I → OpenSubstack 𝒳}
    {W W' : OpenSubstack 𝒳} (h : IsUnion 𝒳 𝒰 W.property) (h' : IsUnion 𝒳 𝒰 W'.property) :
    W = W'

AlgebraicGeometry.Stack.OpenSubstack.exists_openSubstack_of_isUnion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackUnion.lean, line 177. The attribute's comment: “the members of the family are open substacks of the union”.

The members of a family of open substacks are open substacks of its union. If an open substack W of 𝒳 is the union of a family 𝒰 : I → OpenSubstack 𝒳, then each 𝒰 i is an open substack of W: there are open substacks V i of W whose objects are, under the inclusion of W into 𝒳, exactly the objects of 𝒰 i.

theorem exists_openSubstack_of_isUnion {𝒳 : AlgebraicStacks.{u, w} B S hS} {I : Type*}
    {𝒰 : I → OpenSubstack 𝒳} {W : OpenSubstack 𝒳} (h : IsUnion 𝒳 𝒰 W.property) :
    ∃ V : I → OpenSubstack (fullSubcategoryAlgebraicStack 𝒳 W.property W.isAlgebraic),
      ∀ (i : I) (x : 𝒳.val.val.obj),
        (𝒰 i).property x ↔ ∃ hx : W.property x, (V i).property ⟨x, hx⟩

AlgebraicGeometry.Stack.OpenSubstack.exists_isUnion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackUnion.lean, line 293.

Stacks 05UQ. Let 𝒳 be an algebraic stack and 𝒳ᵢ ⊆ 𝒳, i ∈ I, a collection of open substacks. Then there is an open substack ⋃_{i ∈ I} 𝒳ᵢ ⊆ 𝒳 such that the 𝒳ᵢ are open substacks covering it.

The open substack is AlgebraicGeometry.Stack.OpenSubstack.iUnion 𝒰. It is the union of the family in the sense of AlgebraicGeometry.Stack.OpenSubstack.IsUnion: it contains every 𝒳ᵢ, and every object of it lies, over the members of a covering sieve of the fppf topology, in some 𝒳ᵢ. Its points are ⋃_{i ∈ I} |𝒳ᵢ|, so ∐_{i ∈ I} 𝒳ᵢ ⟶ ⋃_{i ∈ I} 𝒳ᵢ is surjective. Each 𝒳ᵢ is an open substack V i of it. And it is the only open substack of 𝒳 that is the union of the family, which is what makes the notation ⋃_{i ∈ I} 𝒳ᵢ legitimate.

theorem exists_isUnion {𝒳 : AlgebraicStacks.{u, w} B S hS} {I : Type*}
    (𝒰 : I → OpenSubstack 𝒳) :
    ∃ W : OpenSubstack 𝒳,
      (IsUnion 𝒳 𝒰 W.property ∧ W.pointSet B S hS = ⋃ i, (𝒰 i).pointSet B S hS ∧
        ∃ V : I → OpenSubstack (fullSubcategoryAlgebraicStack 𝒳 W.property W.isAlgebraic),
          ∀ (i : I) (x : 𝒳.val.val.obj),
            (𝒰 i).property x ↔ ∃ hx : W.property x, (V i).property ⟨x, hx⟩) ∧
      ∀ W' : OpenSubstack 𝒳, IsUnion 𝒳 𝒰 W'.property → W' = W

AlgebraicGeometry.Stack.OpenSubstack.isUnion_pointsWithin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackUnionPointsWithin.lean, line 379. The attribute's comment: “the union of the family is the locus of the set of points lying in a member”.

Let Ω be a set of points of |𝒳| consisting exactly of the classes of the field-valued points of 𝒳 whose object lies in a member of the family. Then the locus AlgebraicGeometry.Stack.pointsWithin of Ω is the union of the family: it contains every member, and every object of it lies, over a covering sieve, in a member.

theorem OpenSubstack.isUnion_pointsWithin {𝒳 : AlgebraicStacks.{u, w} B S hS} {I : Type*}
    (𝒰 : I → OpenSubstack 𝒳) {Ω : Set (points B S hS 𝒳.val.val 𝒳.val.property)}
    (hΩ : ∀ c, c ∈ Ω ↔ ∃ (i : I) (q : FieldValuedPoint B S hS 𝒳.val.val),
      (𝒰 i).property q.obj ∧ pointClass B S hS 𝒳.val.val 𝒳.val.property q = c) :
    OpenSubstack.IsUnion 𝒳 𝒰 (pointsWithin 𝒳 Ω)
Tag 05UR, a lemma

Tag 05UR in the Stacks Project.

AlgebraicGeometry.Stack.exists_finset_pointSet_subset_of_isQuasiCompactStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackFiniteSubcover.lean, line 142. The attribute's comment: “the conclusion read on points: finitely many members of the family contain the point set of the quasi-compact open substack”.

If a quasi-compact open substack 𝒳' of an algebraic stack 𝒳 is covered by a family of open substacks 𝒳ᵢ, then finitely many of the 𝒳ᵢ already cover the point set of 𝒳'.

theorem exists_finset_pointSet_subset_of_isQuasiCompactStack
    {𝒳 : AlgebraicStacks.{u, w} B S hS} (𝒳' : OpenSubstack 𝒳)
    (hqc : IsQuasiCompactStack.{u, w} B S hS
      (fullSubcategoryAlgebraicStack 𝒳 𝒳'.property 𝒳'.isAlgebraic).val
      (fullSubcategoryAlgebraicStack 𝒳 𝒳'.property 𝒳'.isAlgebraic).property)
    {I : Type*} (𝒰 : I → OpenSubstack 𝒳)
    (hcover : IsOpenSubstackCoverOn B S hS 𝒳 𝒳' 𝒰) :
    ∃ J : Finset I, 𝒳'.pointSet B S hS ⊆ ⋃ i ∈ J, (𝒰 i).pointSet B S hS

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

Let 𝒳 be an algebraic stack and 𝒳' ⊆ 𝒳 a quasi-compact open substack. Let 𝒳ᵢ ⊆ 𝒳, i ∈ I, be open substacks such that 𝒳' ⊆ ⋃_{i ∈ I} 𝒳ᵢ, the union being AlgebraicGeometry.Stack.OpenSubstack.iUnion. Then there is a finite subset I' ⊆ I such that 𝒳' ⊆ ⋃_{i ∈ I'} 𝒳ᵢ.

theorem exists_finset_le_of_isQuasiCompactStack {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (𝒳' : OpenSubstack 𝒳)
    (hqc : IsQuasiCompactStack.{u, w} B S hS
      (fullSubcategoryAlgebraicStack 𝒳 𝒳'.property 𝒳'.isAlgebraic).val
      (fullSubcategoryAlgebraicStack 𝒳 𝒳'.property 𝒳'.isAlgebraic).property)
    {I : Type*} (𝒰 : I → OpenSubstack 𝒳) (hle : 𝒳' ≤ OpenSubstack.iUnion 𝒰) :
    ∃ J : Finset I, 𝒳' ≤ OpenSubstack.iUnion (fun i : J => 𝒰 i)

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

Let 𝒳' be a quasi-compact open substack of an algebraic stack 𝒳 and let 𝒳ᵢ, i ∈ I, be open substacks of 𝒳 covering 𝒳'. Then there is a finite I' ⊆ I such that 𝒳' is contained in every open substack containing 𝒳ᵢ for all i ∈ I', that is, 𝒳' ⊆ ⋃_{i ∈ I'} 𝒳ᵢ.

theorem exists_finset_le_of_isQuasiCompactStack_unconditional {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (𝒳' : OpenSubstack 𝒳)
    (hqc : IsQuasiCompactStack.{u, w} B S hS
      (fullSubcategoryAlgebraicStack 𝒳 𝒳'.property 𝒳'.isAlgebraic).val
      (fullSubcategoryAlgebraicStack 𝒳 𝒳'.property 𝒳'.isAlgebraic).property)
    {I : Type*} (𝒰 : I → OpenSubstack 𝒳)
    (hcover : IsOpenSubstackCoverOn B S hS 𝒳 𝒳' 𝒰) :
    ∃ J : Finset I, ∀ W : OpenSubstack 𝒳,
      (∀ i ∈ J, (𝒰 i).property ≤ W.property) → 𝒳'.property ≤ W.property
Tag 05WE, a lemma

Tag 05WE in the Stacks Project.

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

Stacks 05WE. Let 𝒳 be an algebraic stack over S and let 𝒰 i, i ∈ I, be open substacks of 𝒳 which cover 𝒳 and are each representable by an algebraic space over S. Then 𝒳 is representable by an algebraic space.

The covering hypothesis makes 𝒳 a stack in setoids, AlgebraicGeometry.Stack.isStackInSetoids_of_isOpenSubstackCover, which is the first step of the source's proof; the second step is the implication (1) ⟹ (3) of Stacks 04SZ, AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isStackInSetoids.

theorem isRepresentableByAlgebraicSpace_of_isOpenSubstackCover
    (𝒳 : AlgebraicStacks.{u, w} B S hS) {I : Type*} (𝒰 : I → OpenSubstack 𝒳)
    (hcover : IsOpenSubstackCover 𝒳 𝒰)
    (hspace : ∀ i, IsRepresentableByAlgebraicSpace B S hS
      (fullSubcategoryAlgebraicStack 𝒳 (𝒰 i).property (𝒰 i).isAlgebraic).val) :
    IsRepresentableByAlgebraicSpace B S hS 𝒳.val
Tag 05WF, a lemma

Tag 05WF in the Stacks Project.

AlgebraicGeometry.Stack.exists_equivalenceOver_yoneda_of_isOpenSubstackCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/OpenSubstackCoverScheme.lean, line 237.

Stacks 05WF. Let 𝒳 be an algebraic stack over S and let 𝒰 i, i ∈ I, be open substacks of 𝒳 which cover 𝒳 and are each a scheme, that is, equivalent over the site to the category of elements of the representable presheaf of an object of the site. Then 𝒳 is a scheme.

The first step of the source's proof is Stacks 05WE, AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isOpenSubstackCover: it makes 𝒳 an algebraic space F. The second step is the schematic locus of Stacks 03JH: each substack gives an open immersion h_{T_i} ⟶ F whose image is therefore contained in the locus, the covering hypothesis puts every section of F locally in one of those images, and the locus is a sheaf, so it is all of F and F is a scheme. See the implementation notes of this module.

theorem exists_equivalenceOver_yoneda_of_isOpenSubstackCover
    (𝒳 : AlgebraicStacks.{u, w} B S hS) {I : Type*} (𝒰 : I → OpenSubstack 𝒳)
    (hcover : IsOpenSubstackCover 𝒳 𝒰)
    (hscheme : ∀ i, ∃ T : BigFppfOver B S hS, Nonempty
      (StacksRepresentableCFG.EquivalenceOver
        (fullSubcategoryAlgebraicStack 𝒳 (𝒰 i).property (𝒰 i).isAlgebraic).val.val.p
        (presheafOfCategories (yoneda.obj T ⋙ typeToCat)).p)) :
    ∃ T : BigFppfOver B S hS, Nonempty
      (StacksRepresentableCFG.EquivalenceOver 𝒳.val.val.p
        (presheafOfCategories (yoneda.obj T ⋙ typeToCat)).p)
Tag 06M3, a lemma

Tag 06M3 in the Stacks Project.

AlgebraicGeometry.Stack.eq_of_isRelativePropertyLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyLocus.lean, line 166. The attribute's comment: “assertion (A), uniqueness of the maximal open substack on which f has P; unconditional”.

Stacks 06M3, assertion (A), uniqueness of the maximal open substack. Two open substacks of 𝒳 on which f has P and which are maximal with that property coincide: each is contained in the other, and an open substack is determined by its object property.

This is what makes the definite article in the maximal open substack of the source legitimate, and it needs no input beyond those of the ambient site.

theorem eq_of_isRelativePropertyLocus (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴}
    {hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom} {W W' : OpenSubstack 𝒳}
    (h : IsRelativePropertyLocus B S hS P f hf W)
    (h' : IsRelativePropertyLocus B S hS P f hf W') :
    W = W'

AlgebraicGeometry.Stack.exists_isRelativePropertyLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyLocus.lean, line 212. The attribute's comment: “assertion (A), existence of the maximal open substack on which f has P, with the locality of P along a union of open substacks carried as hLocal; the property Q of the source is not needed”.

Stacks 06M3, assertion (A), the existence of the maximal open substack. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S representable by algebraic spaces has an open substack of 𝒳 on which it restricts to a 1-morphism with the relative property P of Stacks 03YK and which contains every open substack with that property.

It is the union AlgebraicGeometry.Stack.OpenSubstack.iUnion (Stacks 05UQ) of the set of all open substacks on which f has P: that f has P on it is the carried hLocal, and maximality is the first clause of AlgebraicGeometry.Stack.OpenSubstack.IsUnion and does not need it.

theorem exists_isRelativePropertyLocus (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    (hLocal : IsRelativePropertyLocalOnOpenSubstackUnions.{u, w} B S hS P)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    ∃ W : OpenSubstack 𝒳, IsRelativePropertyLocus B S hS P f hf W

AlgebraicGeometry.Stack.isRelativePropertyLocus_baseChange_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyLocus.lean, line 337. The attribute's comment: “assertion (B), the containment 𝒵 ×_𝒴 𝒳' ⊆ W(P, f') of the base change of the maximal open substack in the maximal open substack of the base change, for an arbitrary base change and with neither the property R nor the property Q used; the reverse containment, which is where R enters, is not proved”.

Stacks 06M3, assertion (B), the containment g'^{-1}𝒳' ⊆ 𝒳''. Let Q be a 2-fibre product square over the cospan (g, f), so that Q.fst is the base change of f : 𝒳 ⟶ 𝒴 along g : 𝒵 ⟶ 𝒴 and Q.snd is the projection to 𝒳. Let W be the P-locus of f and W' the P-locus of Q.fst. Then every object of the apex carried by Q.snd into W lies in W'.

This is one of the two containments assertion (B) asserts, and it holds for an arbitrary base change: the property R of the source is not used, nor is Q. The inverse image of W along Q.snd is the 2-fibre product (𝒵 ×_𝒴 𝒳) ×_𝒳 W, which by pasting (Stacks 003Q) is also W ×_𝒴 𝒵, so its projection to 𝒵 is a base change of f|_W and has P by Stacks 045C; maximality of W' finishes.

The reverse containment, which is where the hypotheses on R enter, is not proved; see the module documentation.

theorem isRelativePropertyLocus_baseChange_apply
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴} {g : 𝒵 ⟶ 𝒴}
    {hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom}
    (Q : Bicategory.TwoCommSq g f) (hQ : Bicategory.IsTwoFibreProduct Q)
    {hfst : IsRepresentableByAlgebraicSpaces B S hS Q.fst.hom.hom}
    {W : OpenSubstack 𝒳} {W' : OpenSubstack Q.pt}
    (hW : IsRelativePropertyLocus B S hS P f hf W)
    (hW' : IsRelativePropertyLocus B S hS P Q.fst hfst W')
    {x : Q.pt.val.val.obj} (hx : W.property (Q.snd.hom.hom.toFunctor.obj x)) :
    W'.property x

AlgebraicGeometry.Stack.exists_isRelativePropertyLocus_of_hasRelativePropertyLocusOnSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyLocusOnSpaces.lean, line 643. The attribute's comment: “assertion (A), the existence of the largest open substack of the source on which a 1-morphism representable by algebraic spaces and having Q has P, from the four hypotheses of the source on P, Q and R, by the chart construction of the source”.

The existence of the maximal open substack on which a relative property holds. Let P, Q, R be properties of morphisms of algebraic spaces over S which are fppf local on the target and stable under arbitrary base change, with smoothness implying R, with every morphism of algebraic spaces having Q carrying a greatest open subspace of its source on which it has P, and with that greatest open subspace compatible with base change along a morphism with R. Then a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S representable by algebraic spaces and having Q has an open substack of 𝒳 on which it restricts to a 1-morphism with the relative property P of Stacks 03YK and which contains every open substack with that property.

theorem exists_isRelativePropertyLocus_of_hasRelativePropertyLocusOnSpaces
    (P Q R : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage.{u, u} B S hS)]
    [Q.IsStableUnderBaseChange]
    [Q.IsLocalAtTarget (Space.Topology.fppf.precoverage.{u, u} B S hS)]
    [R.IsStableUnderBaseChange]
    [R.IsLocalAtTarget (Space.Topology.fppf.precoverage.{u, u} B S hS)]
    (hsmR : SmoothImplies B S hS R)
    (h3 : HasRelativePropertyLocusOnSpaces B S hS P Q)
    (h4 : RelativePropertyLocusBaseChange B S hS P Q R)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hQf : HasRelativeProperty.{u, u, u + 1, u} B S hS Q f.hom hf) :
    ∃ W : OpenSubstack 𝒳, IsRelativePropertyLocus B S hS P f hf W

AlgebraicGeometry.Stack.isRelativePropertyLocus_baseChange_apply_symm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyLocusOnSpaces.lean, line 1080. The attribute's comment: “assertion (B), the maximality half: the locus of the base change is carried into the locus of the 1-morphism, so that together with the containment proved above the base change of the locus is the locus of the base change. From the four hypotheses of the source on P, Q and R, with Q for the 1-morphism and R for the base change as the source has them, by the source's chart construction run at one more base change”.

The locus of a base change is carried into the locus. Let P, Q, R be properties of morphisms of algebraic spaces over S satisfying the hypotheses of Stacks 06M3, let f : 𝒳 ⟶ 𝒴 be a 1-morphism representable by algebraic spaces having Q, let g : 𝒵 ⟶ 𝒴 be representable by algebraic spaces having R and let D be a 2-fibre product square over the cospan (g, f). If W is the P-locus of f and W' the P-locus of the base change D.fst, then every object of the apex lying in W' is carried by D.snd into W: that is, W(P, f') ⊆ 𝒵 ×_𝒴 W(P, f).

theorem isRelativePropertyLocus_baseChange_apply_symm
    (hsmR : SmoothImplies B S hS R)
    (h3 : HasRelativePropertyLocusOnSpaces B S hS P Q)
    (h4 : RelativePropertyLocusBaseChange B S hS P Q R)
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴} {g : 𝒵 ⟶ 𝒴}
    {hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom}
    {hg : IsRepresentableByAlgebraicSpaces B S hS g.hom.hom}
    (hQf : HasRelativeProperty.{u, u, u + 1, u} B S hS Q f.hom hf)
    (hRg : HasRelativeProperty.{u, u, u + 1, u} B S hS R g.hom hg)
    (D : Bicategory.TwoCommSq g f) (hD : Bicategory.IsTwoFibreProduct D)
    {hfst : IsRepresentableByAlgebraicSpaces B S hS D.fst.hom.hom}
    {W : OpenSubstack 𝒳} {W' : OpenSubstack D.pt}
    (hW : IsRelativePropertyLocus B S hS P f hf W)
    (hW' : IsRelativePropertyLocus B S hS P D.fst hfst W')
    {x : D.pt.val.val.obj} (hx : W'.property x) :
    W.property (D.snd.hom.hom.toFunctor.obj x)
Tag 06M4, a remark

Tag 06M4 in the Stacks Project.

AlgebraicGeometry.Space.le_maximalFlatOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatLocusWarning.lean, line 286. The attribute's comment: “hypothesis (3) of Stacks 06M3 at P = flat, Q = empty: maximality”.

Stacks 06M4, the instantiation: maximality in hypothesis (3) of Stacks 06M3 at P = flat and Q = empty. Every open subspace of the source on which the morphism is flat is contained in the largest flat open: it is a member of the family that open is the supremum of. No hypothesis on the morphism is needed, which is what Q = empty means.

theorem le_maximalFlatOpen (f : X ⟶ Y) {U : Subfunctor X}
    (hU : IsOpenSubspace B S hS U) (hUf : IsFlat B S hS (U.ι ≫ f)) :
    U ≤ maximalFlatOpen B S hS f

AlgebraicGeometry.Space.isOpenSubspace_maximalFlatOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatLocusWarning.lean, line 331. The attribute's comment: “hypothesis (3) of Stacks 06M3 at P = flat, Q = empty: openness”.

Stacks 06M4, the instantiation: openness in hypothesis (3) of Stacks 06M3 at P = flat and Q = empty. The largest flat open of a morphism of algebraic spaces over S is an open subspace of the source. No hypothesis on the morphism is needed.

theorem isOpenSubspace_maximalFlatOpen (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsOpenSubspace B S hS (maximalFlatOpen B S hS f)

AlgebraicGeometry.Space.isFlat_maximalFlatOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatLocusWarning.lean, line 340. The attribute's comment: “hypothesis (3) of Stacks 06M3 at P = flat, Q = empty: flatness on the open”.

Stacks 06M4, the instantiation: flatness in hypothesis (3) of Stacks 06M3 at P = flat and Q = empty. A morphism of algebraic spaces over S is flat on its largest flat open. No hypothesis on the morphism is needed.

theorem isFlat_maximalFlatOpen (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsFlat B S hS ((maximalFlatOpen B S hS f).ι ≫ f)

AlgebraicGeometry.Space.range_pointsMap_maximalFlatOpen_eq_interior, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatLocusWarning.lean, line 390. The attribute's comment: “the warning: the largest flat open is the interior of the flat locus”.

Stacks 06M4, the warning. The point set of the largest open subspace of the source on which a morphism of algebraic spaces over S is flat is the interior, in the point space of Stacks 03BU, of the set of points at which the morphism is flat.

This is the structural statement behind the warning of Stacks 06M4: the open subspace that the construction of Stacks 06M3 produces at P = flat is characterised by a universal property — largest open on whose restriction the morphism is flat — and that universal property computes the interior of the pointwise flat locus, not the locus. Flatness at a point is the germ condition of Stacks 03ML part (2), which does not quantify over neighbourhoods, so no hypothesis on the morphism makes the interior superfluous for free.

theorem range_pointsMap_maximalFlatOpen_eq_interior (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    Set.range (pointsMap B S hS (maximalFlatOpen B S hS f).toFunctor
        (maximalFlatOpen B S hS f).ι) =
      interior {x : points B S hS X | IsFlatAt B S hS f x}

AlgebraicGeometry.Space.range_pointsMap_maximalFlatOpen_eq_setOf_isFlatAt_iff_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatLocusWarning.lean, line 409. The attribute's comment: “the warning: equality with the flat locus holds exactly when it is open”.

Stacks 06M4, the warning. The largest open subspace of the source on which a morphism of algebraic spaces over S is flat has the pointwise flat locus as its point set if and only if that locus is open.

This is the warning of Stacks 06M4 in sharp form. The literal reading of the remark — that the two are not equal — is the statement that the right-hand side fails for some morphism, i.e. that the flat locus of some morphism of algebraic spaces is not open; such a morphism exists, and AlgebraicGeometry.Space.exists_range_pointsMap_maximalFlatOpen_ne_setOf_isFlatAt derives the literal reading from this equivalence by Iff.not.

theorem range_pointsMap_maximalFlatOpen_eq_setOf_isFlatAt_iff_isOpen
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    Set.range (pointsMap B S hS (maximalFlatOpen B S hS f).toFunctor
        (maximalFlatOpen B S hS f).ι) =
        {x : points B S hS X | IsFlatAt B S hS f x} ↔
      IsOpen {x : points B S hS X | IsFlatAt B S hS f x}

AlgebraicGeometry.Space.exists_range_pointsMap_maximalFlatOpen_ne_setOf_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatLocusWarning.lean, line 474. The attribute's comment: “the warning: for some morphism the largest flat open is not the flat locus”.

Stacks 06M4, the warning, in its literal form. There is a morphism of algebraic spaces whose largest flat open subspace does not have as its point set the set of points at which the morphism is flat.

The witness is the morphism of schemes of AlgebraicGeometry.exists_flat_locus_not_open — the inclusion of ℤ into the trivial square-zero extension of ℤ by ⨁_p ℤ/p — read as a morphism of representable algebraic spaces over a big fppf site large enough to contain its source and target. By AlgebraicGeometry.Space.range_pointsMap_maximalFlatOpen_eq_setOf_isFlatAt_iff_isOpen it is enough that its pointwise flat locus is not open, and for a morphism of representable presheaves the flat locus of the morphism of algebraic spaces is cut out by the flat locus of the morphism of schemes, through AlgebraicGeometry.Space.isFlatAt_yoneda_iff and the correspondence AlgebraicGeometry.Space.isOpen_yoneda_iff_isSchemeOpen of Stacks 03BX.

theorem exists_range_pointsMap_maximalFlatOpen_ne_setOf_isFlatAt :
    ∃ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
      (X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS X)
      (_ : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y),
      Set.range (pointsMap B S hS (maximalFlatOpen B S hS f).toFunctor
          (maximalFlatOpen B S hS f).ι) ≠
        {x : points B S hS X | IsFlatAt B S hS f x}
Tag 06M5, a remark

Tag 06M5 in the Stacks Project.

AlgebraicGeometry.Space.exists_isGreatest_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaFurtherInstances.lean, line 205. The attribute's comment: “entry (2), locally quasi-finite: hypothesis (3) of 06M3”.

Stacks 06M5, entry (2), hypothesis (3) of Stacks 06M3. For 𝒬 = locally of finite type and 𝒫 = locally quasi-finite: every morphism f : X ⟶ Y of algebraic spaces over S which is locally of finite type has a largest open subspace of X on which it is locally quasi-finite.

It is AlgebraicGeometry.Space.locallyQuasiFinitePart, the open subspace of Stacks 04NW, which is the case d = 0 of the first entry by Stacks 04NV.

theorem exists_isGreatest_isLocallyQuasiFinite
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f) :
    ∃ W : {W : Subfunctor X // IsOpenSubspace B S hS W},
      IsGreatest {V : {V : Subfunctor X // IsOpenSubspace B S hS V} |
        IsLocallyQuasiFinite B S hS (V.1.ι ≫ f)} W

AlgebraicGeometry.Space.eq_preimage_of_isGreatest_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaFurtherInstances.lean, line 225. The attribute's comment: “entry (2), locally quasi-finite: hypothesis (4) of 06M3”.

Stacks 06M5, entry (2), hypothesis (4) of Stacks 06M3. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite type, any largest open subspace of the source of the base change f' on which f' is locally quasi-finite is the inverse image of any largest open subspace of X on which f is locally quasi-finite.

The source writes ℛ = ∅ for this entry, and no condition is imposed on the base change. Both greatest elements are the canonical open subspaces of Stacks 04NW, whose formation commutes with arbitrary base change, AlgebraicGeometry.Space.locallyQuasiFinitePart_preimage_of_isPullback.

theorem eq_preimage_of_isGreatest_isLocallyQuasiFinite
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (W : {W : Subfunctor X // IsOpenSubspace B S hS W})
    (hW : IsGreatest {V : {V : Subfunctor X // IsOpenSubspace B S hS V} |
      IsLocallyQuasiFinite B S hS (V.1.ι ≫ f)} W)
    (W' : {W' : Subfunctor X' // IsOpenSubspace B S hS W'})
    (hW' : IsGreatest {V : {V : Subfunctor X' // IsOpenSubspace B S hS V} |
      IsLocallyQuasiFinite B S hS (V.1.ι ≫ f')} W') :
    W'.1 = W.1.preimage g'

AlgebraicGeometry.Space.exists_isGreatest_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaFurtherInstances.lean, line 298. The attribute's comment: “entry (3), unramified: hypothesis (3) of 06M3”.

Stacks 06M5, entry (3), hypothesis (3) of Stacks 06M3. For 𝒫 = unramified: every morphism f : X ⟶ Y of algebraic spaces over S has a largest open subspace of X on which it is unramified, and its point set is the set of points at which f is unramified.

This is Stacks 05W2, part (1): the set of points at which f is unramified is open, the corresponding open subspace (Stacks 03BZ) is AlgebraicGeometry.Space.unramifiedLocus, and an open subspace on which f is unramified is one at all of whose points f is unramified. The entry's 𝒬, locally of finite type, is not needed for this hypothesis; it is needed for (4).

theorem exists_isGreatest_isUnramified
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    ∃ W : {W : Subfunctor X // IsOpenSubspace B S hS W},
      IsGreatest {V : {V : Subfunctor X // IsOpenSubspace B S hS V} |
        IsUnramified B S hS (V.1.ι ≫ f)} W ∧
      Set.range (pointsMap B S hS W.1.toFunctor W.1.ι) =
        {x : points B S hS X | IsUnramifiedAt B S hS f x}

AlgebraicGeometry.Space.eq_preimage_of_isGreatest_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaFurtherInstances.lean, line 319. The attribute's comment: “entry (3), unramified: hypothesis (4) of 06M3”.

Stacks 06M5, entry (3), hypothesis (4) of Stacks 06M3. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite type, any largest open subspace of the source of the base change f' on which f' is unramified is the inverse image of any largest open subspace of X on which f is unramified.

The source writes ℛ = ∅ for this entry, and no condition is imposed on the base change. By hypothesis (3) both open subspaces are the loci of points at which the morphisms are unramified, and those correspond under base change by Stacks 05W2, part (2), AlgebraicGeometry.Space.isUnramifiedAt_iff_of_isPullback.

theorem eq_preimage_of_isGreatest_isUnramified
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (W : {W : Subfunctor X // IsOpenSubspace B S hS W})
    (hW : IsGreatest {V : {V : Subfunctor X // IsOpenSubspace B S hS V} |
      IsUnramified B S hS (V.1.ι ≫ f)} W)
    (W' : {W' : Subfunctor X' // IsOpenSubspace B S hS W'})
    (hW' : IsGreatest {V : {V : Subfunctor X' // IsOpenSubspace B S hS V} |
      IsUnramified B S hS (V.1.ι ≫ f')} W') :
    W'.1 = W.1.preimage g'

AlgebraicGeometry.Space.exists_isGreatest_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaFurtherInstances.lean, line 371. The attribute's comment: “entry (4), flat: hypothesis (3) of 06M3”.

Stacks 06M5, entry (4), hypothesis (3) of Stacks 06M3. For 𝒬 = locally of finite presentation and 𝒫 = flat: every morphism f : X ⟶ Y of algebraic spaces over S which is locally of finite presentation has a largest open subspace of X on which it is flat, and its point set is exactly the set of points at which f is flat.

The set of points at which f is flat is open by Stacks 05WV for the structure sheaf, AlgebraicGeometry.Space.isOpen_setOf_isFlatAt, and an open subspace on which f is flat is one at all of whose points f is flat. The second clause is the source's remark that, because f has 𝒬, W(𝒫, f) is the set of points at which f is flat; without 𝒬 it is only the interior of that set, which is the warning of Stacks 06M4.

theorem exists_isGreatest_isFlat
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFinitePresentation B S hS f) :
    ∃ W : {W : Subfunctor X // IsOpenSubspace B S hS W},
      IsGreatest {V : {V : Subfunctor X // IsOpenSubspace B S hS V} |
        IsFlat B S hS (V.1.ι ≫ f)} W ∧
      Set.range (pointsMap B S hS W.1.toFunctor W.1.ι) =
        {x : points B S hS X | IsFlatAt B S hS f x}

AlgebraicGeometry.Space.eq_preimage_of_isGreatest_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaFurtherInstances.lean, line 395. The attribute's comment: “entry (4), flat: hypothesis (4) of 06M3”.

Stacks 06M5, entry (4), hypothesis (4) of Stacks 06M3. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite presentation and whose bottom arrow g is flat, any largest open subspace of the source of the base change f' on which f' is flat is the inverse image of any largest open subspace of X on which f is flat.

The entry's ℛ is flat and locally of finite presentation; only flatness of g is used. By hypothesis (3) both open subspaces are the loci of points at which the morphisms are flat, the base change being locally of finite presentation as well, and those correspond under a flat base change, which is Stacks 05WW for the structure sheaf, AlgebraicGeometry.Space.isFlatAt_iff_of_isPullback_of_isFlat.

theorem eq_preimage_of_isGreatest_isFlat
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFinitePresentation B S hS f) (hg : IsFlat B S hS g)
    (W : {W : Subfunctor X // IsOpenSubspace B S hS W})
    (hW : IsGreatest {V : {V : Subfunctor X // IsOpenSubspace B S hS V} |
      IsFlat B S hS (V.1.ι ≫ f)} W)
    (W' : {W' : Subfunctor X' // IsOpenSubspace B S hS W'})
    (hW' : IsGreatest {V : {V : Subfunctor X' // IsOpenSubspace B S hS V} |
      IsFlat B S hS (V.1.ι ≫ f')} W') :
    W'.1 = W.1.preimage g'

AlgebraicGeometry.Space.exists_isGreatest_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaFurtherInstances.lean, line 459. The attribute's comment: “entry (5), étale: hypothesis (3) of 06M3”.

Stacks 06M5, entry (5), hypothesis (3) of Stacks 06M3. For 𝒬 = locally of finite presentation and 𝒫 = étale: every morphism f : X ⟶ Y of algebraic spaces over S which is locally of finite presentation has a largest open subspace of X on which it is étale, and its point set is the set of points at which f is both unramified and flat.

This combines entries (3) and (4): the two sets of points are open, and on an open subspace f is étale exactly when it is unramified and flat there, because an unramified morphism which is flat and locally of finite presentation is étale (Stacks 06LU).

theorem exists_isGreatest_isEtale
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFinitePresentation B S hS f) :
    ∃ W : {W : Subfunctor X // IsOpenSubspace B S hS W},
      IsGreatest {V : {V : Subfunctor X // IsOpenSubspace B S hS V} |
        IsEtale B S hS (V.1.ι ≫ f)} W ∧
      Set.range (pointsMap B S hS W.1.toFunctor W.1.ι) =
        {x : points B S hS X | IsUnramifiedAt B S hS f x ∧ IsFlatAt B S hS f x}

AlgebraicGeometry.Space.eq_preimage_of_isGreatest_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaFurtherInstances.lean, line 483. The attribute's comment: “entry (5), étale: hypothesis (4) of 06M3”.

Stacks 06M5, entry (5), hypothesis (4) of Stacks 06M3. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite presentation and whose bottom arrow g is flat, any largest open subspace of the source of the base change f' on which f' is étale is the inverse image of any largest open subspace of X on which f is étale.

The entry's ℛ is flat and locally of finite presentation; only flatness of g is used. By hypothesis (3) both open subspaces are the loci of points at which the morphisms are unramified and flat, and both conditions correspond under the base change: unramifiedness under any base change (Stacks 05W2, part (2)) and flatness under a flat one (Stacks 05WW for the structure sheaf).

theorem eq_preimage_of_isGreatest_isEtale
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFinitePresentation B S hS f) (hg : IsFlat B S hS g)
    (W : {W : Subfunctor X // IsOpenSubspace B S hS W})
    (hW : IsGreatest {V : {V : Subfunctor X // IsOpenSubspace B S hS V} |
      IsEtale B S hS (V.1.ι ≫ f)} W)
    (W' : {W' : Subfunctor X' // IsOpenSubspace B S hS W'})
    (hW' : IsGreatest {V : {V : Subfunctor X' // IsOpenSubspace B S hS V} |
      IsEtale B S hS (V.1.ι ≫ f')} W') :
    W'.1 = W.1.preimage g'

AlgebraicGeometry.Space.exists_isGreatest_hasRelativeDimensionLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaInstances.lean, line 266. The attribute's comment: “entry (1), hypothesis (3) of Stacks 06M3 at 𝒬 = locally of finite type and 𝒫 = relative dimension ≤ d: the existence of a largest open subspace of the source on which the morphism has relative dimension ≤ d, from Stacks 06LR and Stacks 04NT”.

Stacks 06M5, first entry, hypothesis (3) of Stacks 06M3. For 𝒬 = locally of finite type and 𝒫 = relative dimension ≤ d (Stacks 06LR): every morphism f : X ⟶ Y of algebraic spaces over S which is locally of finite type has a largest open subspace of X on which it has relative dimension ≤ d.

The open subspace is AlgebraicGeometry.Space.boundedRelativeDimensionPart, built from the openness statement Stacks 04NT through the correspondence of Stacks 03BZ; the two clauses of being greatest are AlgebraicGeometry.Space.hasRelativeDimensionLE_boundedRelativeDimensionPart and AlgebraicGeometry.Space.le_boundedRelativeDimensionPart.

theorem exists_isGreatest_hasRelativeDimensionLE (d : ℕ)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f) :
    ∃ W : {W : Subfunctor X // IsOpenSubspace B S hS W},
      IsGreatest {V : {V : Subfunctor X // IsOpenSubspace B S hS V} |
        HasRelativeDimensionLE d B S hS (V.1.ι ≫ f)} W

AlgebraicGeometry.Space.boundedRelativeDimensionPart_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaInstances.lean, line 289. The attribute's comment: “entry (1), hypothesis (4) of Stacks 06M3 at 𝒬 = locally of finite type and 𝒫 = relative dimension ≤ d, for the canonical open subspace: the formation of the largest open subspace commutes with base change, for an arbitrary base change since the entry's ℛ is ∅, from Stacks 04NS”.

Stacks 06M5, first entry, hypothesis (4) of Stacks 06M3, for the canonical open subspace. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite type, the base change f' is locally of finite type and its open subspace of relative dimension ≤ d is the inverse image of that of f.

No condition is imposed on the base change: the source writes ℛ = ∅ for this entry, and Stacks 04NS gives the invariance of the relative dimension at a point under an arbitrary base change. On points both sides are the locus of relative dimension at most d, by AlgebraicGeometry.Space.range_pointsMap_boundedRelativeDimensionPart and the identification of the point set of an inverse image; the two open subspaces then agree because Stacks 03BZ is injective.

theorem boundedRelativeDimensionPart_preimage_of_isPullback (d : ℕ)
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) :
    ∃ hf' : IsLocallyOfFiniteType B S hS f',
      (boundedRelativeDimensionPart B S hS d hX' hY' f' hf').1 =
        (boundedRelativeDimensionPart B S hS d hX hY f hf).1.preimage g'

AlgebraicGeometry.Space.eq_preimage_of_isGreatest_hasRelativeDimensionLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaInstances.lean, line 336. The attribute's comment: “entry (1), hypothesis (4) of Stacks 06M3 at 𝒬 = locally of finite type and 𝒫 = relative dimension ≤ d, quantified over largest open subspaces as the lemma takes it, for an arbitrary base change since the entry's ℛ is ∅”.

Stacks 06M5, first entry, hypothesis (4) of Stacks 06M3, in the form the lemma consumes. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite type, any largest open subspace of the source of the base change on which the base change has relative dimension ≤ d is the inverse image of any largest open subspace of X on which f has relative dimension ≤ d.

Stacks 06M3 takes hypothesis (4) in this shape, quantified over largest open subspaces rather than over a chosen one. A greatest element of an ordered type is unique, so both are the canonical AlgebraicGeometry.Space.boundedRelativeDimensionPart and the statement reduces to AlgebraicGeometry.Space.boundedRelativeDimensionPart_preimage_of_isPullback.

theorem eq_preimage_of_isGreatest_hasRelativeDimensionLE (d : ℕ)
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (W : {W : Subfunctor X // IsOpenSubspace B S hS W})
    (hW : IsGreatest {V : {V : Subfunctor X // IsOpenSubspace B S hS V} |
      HasRelativeDimensionLE d B S hS (V.1.ι ≫ f)} W)
    (W' : {W' : Subfunctor X' // IsOpenSubspace B S hS W'})
    (hW' : IsGreatest {V : {V : Subfunctor X' // IsOpenSubspace B S hS V} |
      HasRelativeDimensionLE d B S hS (V.1.ι ≫ f')} W') :
    W'.1 = W.1.preimage g'

AlgebraicGeometry.Space.unramifiedLocus_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSourceLemmaUnramified.lean, line 180. The attribute's comment: “entry (3), hypothesis (4) of Stacks 06M3 at 𝒬 = locally of finite type and 𝒫 = unramified, for the canonical open subspace: the formation of the largest open subspace commutes with base change, for an arbitrary base change since the entry's ℛ is ∅, from Stacks 05W2”. References: EGA IV (17.7.2), “more general”.

Stacks 06M5, third entry, hypothesis (4) of Stacks 06M3, for the canonical open subspace. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite type, the open unramified locus of the base change f' is the inverse image of the open unramified locus of f.

No condition is imposed on the base change: the source writes ℛ = ∅ for this entry, and part (2) of Stacks 05W2, AlgebraicGeometry.Space.setOf_isUnramifiedAt_eq_preimage_of_isPullback, gives the invariance of the set of points of unramifiedness under an arbitrary base change. On points both sides are that set, by AlgebraicGeometry.Space.range_pointsMap_unramifiedLocus and the identification AlgebraicGeometry.Space.pointsRange_preimage of the point set of an inverse image; the two open subspaces then agree because part (1) of Stacks 03BZ is injective.

theorem unramifiedLocus_preimage_of_isPullback
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) :
    (unramifiedLocus B S hS hX' f').1 = (unramifiedLocus B S hS hX f).1.preimage g'
Sources
LeanAlgebraicGeometry.Stack.AlgebraicStacks.IsOpenImmersion · AlgebraicGeometry.Stack.AlgebraicStacks.IsClosedImmersion · AlgebraicGeometry.Stack.AlgebraicStacks.IsImmersion · AlgebraicGeometry.Stack.AlgebraicStacks.isImmersion_snd_of_isTwoFibreProduct · AlgebraicGeometry.Stack.AlgebraicStacks.isClosedImmersion_baseChange_snd · AlgebraicGeometry.Stack.AlgebraicStacks.isOpenImmersion_baseChange_snd · AlgebraicGeometry.Stack.AlgebraicStacks.isOpenImmersion_comp · AlgebraicGeometry.Stack.AlgebraicStacks.isClosedImmersion_comp

Section100.10 Reduced algebraic stacks#

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

Tag 0509, a lemma

Tag 0509 in the Stacks Project.

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

The uniqueness assertion of Stacks 0509. Two reduced closed substacks of an algebraic stack 𝒳 over S with the same set of points are equal: each is contained in the other by AlgebraicGeometry.Stack.le_of_isReducedStack_of_range_pointsMap_subset.

theorem eq_of_isReducedStack_of_range_pointsMap_eq {𝒳 : AlgebraicStacks.{u, w} B S hS}
    {P Q : ObjectProperty 𝒳.val.val.obj}
    (hP : IsClosedSubstack 𝒳 P) (hQ : IsClosedSubstack 𝒳 Q)
    (hAP : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 P))
    (hAQ : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 Q))
    (hPred : IsReducedStack B S hS (fullSubcategoryAlgebraicStack 𝒳 P hAP))
    (hQred : IsReducedStack B S hS (fullSubcategoryAlgebraicStack 𝒳 Q hAQ))
    (hpoints :
      Set.range (AlgebraicStacks.pointsMap B S hS (fullSubcategoryInclusion 𝒳 P hAP)) =
        Set.range (AlgebraicStacks.pointsMap B S hS (fullSubcategoryInclusion 𝒳 Q hAQ))) :
    P = Q

AlgebraicGeometry.Stack.existsUnique_reducedClosedSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ReducedClosedSubstackExistence.lean, line 520.

Let 𝒳 be an algebraic stack over S and let T be a closed subset of its space of points |𝒳|. There exists a unique closed substack 𝒵 ⊆ 𝒳 such that (a) |𝒵| = T and (b) 𝒵 is reduced.

A closed substack is a property of the objects of 𝒳 cutting out a strictly full subcategory which is an algebraic stack with closed immersion inclusion (AlgebraicGeometry.Stack.IsClosedSubstack); its set of points is the image of the map on points of its inclusion. Both clauses are stated for every proof that the full subcategory is an algebraic stack.

theorem existsUnique_reducedClosedSubstack :
    ∃! P : ObjectProperty 𝒳.val.val.obj, IsClosedSubstack 𝒳 P ∧
      (∀ hP : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 P),
        Set.range (AlgebraicStacks.pointsMap B S hS (fullSubcategoryInclusion 𝒳 P hP)) = T) ∧
      ∀ hP : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 P),
        IsReducedStack B S hS (fullSubcategoryAlgebraicStack 𝒳 P hP)
Tag 050A, a lemma

Tag 050A in the Stacks Project.

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

Stacks 050A. Let 𝒳 be an algebraic stack over S and let P cut out a closed substack of 𝒳. If 𝒳 is reduced and the inclusion of the substack is surjective on points, then the substack is the whole of 𝒳.

Every scheme chart of a reduced algebraic stack is reduced, and the chart supplied by the algebraic-stack condition is locally essentially surjective; so AlgebraicGeometry.Stack.prop_of_isReduced_fiber puts the image of the tautological object of that chart in the substack, AlgebraicGeometry.Stack.prop_of_isHomLift puts the image of every object of the chart there, and membership of a substack being local on the big fppf site puts every object of 𝒳 there.

theorem eq_top_of_isClosedSubstack_of_isReducedStack {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (P : ObjectProperty 𝒳.val.val.obj) (hclosed : IsClosedSubstack 𝒳 P)
    (hpoints : IsSurjective B S hS (fullSubcategoryInclusion 𝒳 P hclosed.2.choose))
    (hred : IsReducedStack B S hS 𝒳) :
    P = ⊤
Tag 050B, a lemma

Tag 050B in the Stacks Project.

AlgebraicGeometry.Stack.factorsThroughSubstack_iff_range_pointsMap_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ReducedStackFactorization.lean, line 73.

Let 𝒳 and 𝒴 be algebraic stacks over S, let P cut out a closed substack of 𝒳 and let 𝒴 be reduced. A 1-morphism f : 𝒴 ⟶ 𝒳 factors through the substack if and only if the image of the induced map on points is contained in the points of the substack.

theorem factorsThroughSubstack_iff_range_pointsMap_subset
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒴 ⟶ 𝒳)
    {P : ObjectProperty 𝒳.val.val.obj} (hP : IsClosedSubstack 𝒳 P)
    (hA : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 P))
    (hred : IsReducedStack B S hS 𝒴) :
    FactorsThroughSubstack f P ↔
      Set.range (AlgebraicStacks.pointsMap B S hS f) ⊆
        Set.range (AlgebraicStacks.pointsMap B S hS (fullSubcategoryInclusion 𝒳 P hA))
Tag 050C, a definition

Tag 050C in the Stacks Project.

AlgebraicGeometry.Stack.IsAlgebraicStackStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Reduction.lean, line 94. The attribute's comment: “algebraic stack structure on a closed set of points”.

Stacks 050C, an algebraic stack structure on a closed set of points. Let 𝒳 be an algebraic stack over S and let Z be a set of points of 𝒳. An algebraic stack structure on Z is a closed substack of 𝒳 whose set of points is Z, that is, a property P of the objects of 𝒳 cutting out a closed substack the canonical inclusion of which has range Z on points.

def IsAlgebraicStackStructure {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (Z : Set (AlgebraicStacks.points B S hS 𝒳)) (P : ObjectProperty 𝒳.val.val.obj) : Prop

AlgebraicGeometry.Stack.IsReducedInducedStackStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Reduction.lean, line 131. The attribute's comment: “the reduced induced algebraic stack structure”.

Stacks 050C, the reduced induced algebraic stack structure. The reduced induced algebraic stack structure on a set Z of points of 𝒳 is the algebraic stack structure on Z which is reduced. There is at most one, AlgebraicGeometry.Stack.IsReducedInducedStackStructure.unique, which is the content of the uniqueness half of Stacks 0509.

def IsReducedInducedStackStructure {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (Z : Set (AlgebraicStacks.points B S hS 𝒳)) (P : ObjectProperty 𝒳.val.val.obj) : Prop

AlgebraicGeometry.Stack.IsReducedInducedStackStructure.unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Reduction.lean, line 159. The attribute's comment: “uniqueness of the reduced induced structure”.

Stacks 050C, uniqueness of the reduced induced structure. Two reduced induced algebraic stack structures on the same set of points are equal. This is the uniqueness half of Stacks 0509, and it is what makes the definite article of the source legitimate.

theorem IsReducedInducedStackStructure.unique {𝒳 : AlgebraicStacks.{u, w} B S hS}
    {Z : Set (AlgebraicStacks.points B S hS 𝒳)} {P Q : ObjectProperty 𝒳.val.val.obj}
    (hP : IsReducedInducedStackStructure B S hS Z P)
    (hQ : IsReducedInducedStackStructure B S hS Z Q) :
    P = Q

AlgebraicGeometry.Stack.IsReduction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Reduction.lean, line 171. The attribute's comment: “the reduction”.

Stacks 050C, the reduction. The reduction 𝒳_red of an algebraic stack 𝒳 over S is the reduced induced algebraic stack structure on the whole of its space of points. It is unique, AlgebraicGeometry.Stack.IsReduction.unique.

def IsReduction {𝒳 : AlgebraicStacks.{u, w} B S hS} (P : ObjectProperty 𝒳.val.val.obj) : Prop
Tag 06FK, a remark

Tag 06FK in the Stacks Project.

AlgebraicGeometry.Stack.exists_reducedInducedSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ReducedInducedSubstackLocallyClosed.lean, line 123. The attribute's comment: “a locally closed T in |X|: the open substack U with |U| = |X| minus the boundary of T, the reduced induced closed substack Z of U on the points of T (Stacks 050C), the immersion Z -> U -> X, Z reduced, and |Z| = T in |X|”.

The reduced induced substack structure on a locally closed set of points. Let 𝒳 be an algebraic stack over S and let T be a locally closed subset of its space of points, with boundary ∂T = T̄ \ T. Then there are

  • an open substack 𝒰 of 𝒳 with |𝒰| = |𝒳| \ ∂T (Mathlib's coborder T), and
  • a reduced induced algebraic stack structure 𝒵 (Stacks 050C) on the part of T inside |𝒰|, that is, a reduced closed substack of 𝒰 with that set of points,

such that the composite 𝒵 ⟶ 𝒰 ⟶ 𝒳 of the two inclusions is an immersion, 𝒵 is reduced, and the image of |𝒵| in |𝒳| is exactly T.

theorem exists_reducedInducedSubstack
    (T : Set (AlgebraicStacks.points B S hS 𝒳))
    (hT : @IsLocallyClosed _ (pointTopology B S hS 𝒳.val) T) :
    ∃ (𝒰 : OpenSubstack 𝒳)
      (P : ObjectProperty
        (fullSubcategoryAlgebraicStack 𝒳 𝒰.property 𝒰.isAlgebraic).val.val.obj)
      (hP : IsAlgebraicStack.{u, w} B S hS
        (fullSubcategoryBased (fullSubcategoryAlgebraicStack 𝒳 𝒰.property 𝒰.isAlgebraic) P)),
      𝒰.pointSet B S hS = @coborder _ (pointTopology B S hS 𝒳.val) T ∧
      IsReducedInducedStackStructure B S hS
        (AlgebraicStacks.pointsMap B S hS 𝒰.inclusion ⁻¹' T) P ∧
      AlgebraicStacks.IsImmersion B S hS
        (fullSubcategoryInclusion (fullSubcategoryAlgebraicStack 𝒳 𝒰.property 𝒰.isAlgebraic)
          P hP ≫ 𝒰.inclusion) ∧
      IsReducedStack B S hS
        (fullSubcategoryAlgebraicStack (fullSubcategoryAlgebraicStack 𝒳 𝒰.property 𝒰.isAlgebraic)
          P hP) ∧
      Set.range (AlgebraicStacks.pointsMap B S hS
        (fullSubcategoryInclusion (fullSubcategoryAlgebraicStack 𝒳 𝒰.property 𝒰.isAlgebraic)
          P hP ≫ 𝒰.inclusion)) = T
Sources
LeanAlgebraicGeometry.Stack.eq_of_isReducedStack_of_range_pointsMap_eq · AlgebraicGeometry.Stack.existsUnique_reducedClosedSubstack · AlgebraicGeometry.Stack.eq_top_of_isClosedSubstack_of_isReducedStack · AlgebraicGeometry.Stack.factorsThroughSubstack_iff_range_pointsMap_subset · AlgebraicGeometry.Stack.IsAlgebraicStackStructure · AlgebraicGeometry.Stack.IsReducedInducedStackStructure · AlgebraicGeometry.Stack.IsReducedInducedStackStructure.unique · AlgebraicGeometry.Stack.IsReduction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.