101.23 Locally quasi-finite… to 101.37 Proper morphisms

Section101.23 Locally quasi-finite morphisms #

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

Tag 06UA, a lemma

Tag 06UA in the Stacks Project.

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

Stacks 06UA, the implication (1) ⟹ (2). A 1-morphism of algebraic stacks over S which is representable by algebraic spaces and locally quasi-finite in the sense of Stacks 04XB is locally of finite type, and the fibre of it over every field-valued point of the target has discrete space of points.

theorem isLocallyOfFiniteType_and_discreteTopology_of_isLocallyQuasiFinite
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (h : IsLocallyQuasiFinite B S hS f.hom) :
    AlgebraicStacks.IsLocallyOfFiniteType B S hS f ∧
      ∀ (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
        (toBase : Spec (.of k) ⟶ S)
        (g : schemeStack.{u, w} B S hS (Over.mk (⟨toBase⟩ : B.obj hk ⟶ B.obj hS)) ⟶ 𝒴),
        DiscreteTopology
          (points B S hS (twoFibreProductSquareAlgebraicStacks B S hS f g).pt.val.val
            (twoFibreProductSquareAlgebraicStacks B S hS f g).pt.val.property)

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

Stacks 06UA, the implication (2) ⟹ (1). A 1-morphism of algebraic stacks over S which is representable by algebraic spaces, locally of finite type, and whose fibre over every field-valued point of the target has discrete space of points, is locally quasi-finite in the sense of Stacks 04XB.

One scheme atlas of 𝒴 suffices by Stacks 04XD, and for the base change of f along it the criterion of Stacks 06RW applies: it is locally of finite type by Stacks 04XC and its field-valued fibres are fibres of f.

theorem isLocallyQuasiFinite_of_isLocallyOfFiniteType_of_discreteTopology
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (hft : AlgebraicStacks.IsLocallyOfFiniteType B S hS f)
    (hfib : ∀ (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
      (toBase : Spec (.of k) ⟶ S)
      (g : schemeStack.{u, w} B S hS (Over.mk (⟨toBase⟩ : B.obj hk ⟶ B.obj hS)) ⟶ 𝒴),
      DiscreteTopology
        (points B S hS (twoFibreProductSquareAlgebraicStacks B S hS f g).pt.val.val
          (twoFibreProductSquareAlgebraicStacks B S hS f g).pt.val.property)) :
    IsLocallyQuasiFinite B S hS f.hom

AlgebraicGeometry.Stack.isLocallyQuasiFinite_iff_isLocallyOfFiniteType_and_discreteTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteRepresentable.lean, line 362.

Stacks 06UA. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S which is representable by algebraic spaces is locally quasi-finite in the sense of Stacks 04XB exactly when it is locally of finite type and for every field-valued point of 𝒴 the fibre of f over it has discrete space of points.

The right-hand side is the conjunction of the second and third clauses of Stacks 06PU.

theorem isLocallyQuasiFinite_iff_isLocallyOfFiniteType_and_discreteTopology
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    IsLocallyQuasiFinite B S hS f.hom ↔
      (AlgebraicStacks.IsLocallyOfFiniteType B S hS f ∧
        ∀ (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
          (toBase : Spec (.of k) ⟶ S)
          (g : schemeStack.{u, w} B S hS (Over.mk (⟨toBase⟩ : B.obj hk ⟶ B.obj hS)) ⟶ 𝒴),
          DiscreteTopology
            (points B S hS (twoFibreProductSquareAlgebraicStacks B S hS f g).pt.val.val
              (twoFibreProductSquareAlgebraicStacks B S hS f g).pt.val.property))

Tag 06PU, a definition

Tag 06PU in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsLocallyQuasiFinite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteAlgebraicStack.lean, line 87.

Stacks 06PU. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is locally quasi-finite when it is quasi-DM (Stacks 04YW), locally of finite type (Stacks 06FS, part (1)), and for every field-valued point of 𝒴 the fibre of f over it has discrete space of points.

A field-valued point is a field k contained in the site together with a structure morphism Spec(k) ⟶ S and a 1-morphism from the algebraic stack Spec(k) represents to 𝒴; the fibre is the apex of the canonical 2-fibre-product square of that 1-morphism with f, and its points carry the topology of Stacks 04XL.

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

Tag 06UB, a lemma

Tag 06UB in the Stacks Project.

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

Stacks 06UB. A base change of a locally quasi-finite 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is locally quasi-finite: the first projection of any 2-fibre product of the cospan (g, f) is locally quasi-finite as soon as f is.

The quasi-DM conjunct is Stacks 050F at the exchanged square and local finite type is Stacks 06FU. For the fibre conjunct, a field-valued point g' of 𝒴' gives the outer point g' ≫ g of 𝒴, and the fibre of the base change over g' is by Stacks 02XD a 2-fibre product of the cospan (f, g' ≫ g), whose fibre the hypothesis says has discrete space of points.

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

Tag 06UC, a lemma

Tag 06UC in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.locallyQuasiFinite_of_isLocallyQuasiFinite_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteOverField.lean, line 314.

Let 𝒳 ⟶ Spec(k) be a locally quasi-finite 1-morphism, where 𝒳 is an algebraic stack over the field k, and let f : V ⟶ 𝒳 be a locally quasi-finite 1-morphism out of the algebraic stack represented by a scheme V of the site with structure morphism g : V ⟶ Spec(k). Then g is locally quasi-finite: it is locally of finite type and locally quasi-finite as a morphism of schemes.

theorem locallyQuasiFinite_of_isLocallyQuasiFinite_over_field
    (B : BigFppfSite.{u}) (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
    {𝒳 : Stack.AlgebraicStacks.{u, w} B (Spec (.of k)) hk}
    (p : 𝒳 ⟶ Stack.schemeStack.{u, w} B (Spec (.of k)) hk (Over.mk (𝟙 (B.obj hk))))
    (hp : IsLocallyQuasiFinite B (Spec (.of k)) hk p)
    (V : Scheme.{u}) (hV : B.Contains V) (g : V ⟶ Spec (.of k))
    (f : Stack.schemeStack.{u, w} B (Spec (.of k)) hk
      (Over.mk (⟨g⟩ : B.obj hV ⟶ B.obj hk)) ⟶ 𝒳)
    (hf : IsLocallyQuasiFinite B (Spec (.of k)) hk f) :
    LocallyOfFiniteType g ∧ LocallyQuasiFinite g

AlgebraicGeometry.Stack.AlgebraicStacks.locallyQuasiFinite_of_isLocallyQuasiFinite_over_fieldPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteOverFieldPoint.lean, line 351. The attribute's comment: “at a field-valued point of a general base scheme”.

Stacks 06UC at a field-valued point of a general base scheme, for the Stacks 06PU notion of local quasi-finiteness of the chart. This is locallyQuasiFinite_siteMap_of_isLocallyQuasiFinite_fieldPoint with local quasi-finiteness of c read in the sense of Stacks 06PU, which is what the source's statement uses; it implies the Stacks 04XB notion by Stacks 06UA, since c is representable by algebraic spaces.

theorem locallyQuasiFinite_of_isLocallyQuasiFinite_over_fieldPoint
    (k : Type u) [Field k] (hk : B.Contains (Spec (.of k))) (toBase : Spec (.of k) ⟶ S)
    {𝒴₀ : Stack.AlgebraicStacks.{u, w} B S hS} (W : BigFppfOver B S hS)
    (q : 𝒴₀ ⟶ Stack.schemeStack.{u, w} B S hS (Over.mk (⟨toBase⟩ : B.obj hk ⟶ B.obj hS)))
    (c : Stack.schemeStack.{u, w} B S hS W ⟶ 𝒴₀)
    (hq : IsLocallyQuasiFinite B S hS q) (hc : IsLocallyQuasiFinite B S hS c) :
    LocallyOfFiniteType ((BigFppfOver.toScheme B S hS).map (siteMap B S hS (c ≫ q))) ∧
      LocallyQuasiFinite ((BigFppfOver.toScheme B S hS).map (siteMap B S hS (c ≫ q)))

Tag 06UD, a lemma

Tag 06UD in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyQuasiFinite_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteComposition.lean, line 500.

Stacks 06UD. A composite of locally quasi-finite 1-morphisms of algebraic stacks over S is locally quasi-finite.

The quasi-DM condition composes by Stacks 050K and local finite type by Stacks 06FT. For the third condition, the fibre of f ≫ g over a field-valued point p of 𝒵 is by Stacks 02XD a 2-fibre product of the cospan (f, 𝒴_k ⟶ 𝒴), where 𝒴_k is the fibre of g over p; both 𝒳 ×_𝒴 𝒴_k ⟶ 𝒴_k and 𝒴_k ⟶ Spec(k) are locally quasi-finite by Stacks 06UB, so the discreteness is the case of a target locally quasi-finite over a field.

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

Tag 06UE, a lemma

Tag 06UE in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_tfae_hasQuasiFiniteFlatSpaceCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiDMRelativePresentation.lean, line 203. The attribute's comment: “granted the substantial direction of Tag 06MF, the quasi-DM presentation theorem, as the hypothesis hPresentation, and granted the containment of the terminal scheme in the site as the hypothesis hZ, which the absolute quasi-DM condition of Tag 050D part (6) needs. Only (1) implies (2) uses hPresentation”.

Stacks 06UE. For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S the following are equivalent: f is quasi-DM; every base change of f along an algebraic space over 𝒴 has a surjective, flat, locally finitely presented, locally quasi-finite cover by an algebraic space; and some algebraic space surjective, flat and locally of finite presentation over 𝒴 carries a base change of f with such a cover.

The hypothesis hPresentation is the substantial direction of Stacks 06MF, carried in this library; it is used only for (1) ⟹ (2).

theorem isQuasiDM_tfae_hasQuasiFiniteFlatSpaceCover
    (hPresentation : Stack.ExistsQuasiDMPresentationOfIsAbsolutelyQuasiDM.{u, w} B S hS hZ)
    (f : 𝒳 ⟶ 𝒴) :
    [IsQuasiDM B S hS f,
      HasQuasiFiniteFlatSpaceCoverOnEveryBaseChange B S hS f,
      HasQuasiFiniteFlatSpaceCoverOnSomeFlatBaseChange B S hS f].TFAE

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_tfae_hasQuasiFiniteFlatSpaceCover_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiDMRelativePresentationUnconditional.lean, line 83. The attribute's comment: “unconditional. The implication (1) implies (2) uses the substantial direction of Tag 06MF, the quasi-DM presentation theorem hasQuasiDMPresentation_of_isAbsolutelyQuasiDM, which is proved; the containment of the terminal scheme in the site that the absolute quasi-DM condition of Tag 050D part (6) needs is discharged by AlgebraicGeometry.BigFppfSite.contains_terminal”.

For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S the following are equivalent: f is quasi-DM; every base change of f along an algebraic space over 𝒴 has a surjective, flat, locally finitely presented, locally quasi-finite cover by an algebraic space; and some algebraic space surjective, flat and locally of finite presentation over 𝒴 carries a base change of f with such a cover.

theorem isQuasiDM_tfae_hasQuasiFiniteFlatSpaceCover_unconditional (f : 𝒳 ⟶ 𝒴) :
    [IsQuasiDM B S hS f,
      HasQuasiFiniteFlatSpaceCoverOnEveryBaseChange B S hS f,
      HasQuasiFiniteFlatSpaceCoverOnSomeFlatBaseChange B S hS f].TFAE

Tag 06UF, a lemma

Tag 06UF in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_and_transfersLocalQuasiFiniteness_of_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteRelativePresentation.lean, line 186. The attribute's comment: “the implication (1) => (2)”.

Stacks 06UF, (1) ⟹ (2). A locally quasi-finite 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is quasi-DM, and for every algebraic space 𝒱 over 𝒴 a locally quasi-finite 1-morphism 𝒰 ⟶ 𝒳 ×_𝒴 𝒱 out of an algebraic space has locally quasi-finite composite 𝒰 ⟶ 𝒱.

The quasi-DM conjunct is the first conjunct of Stacks 06PU. For the second, the projection 𝒳 ×_𝒴 𝒱 ⟶ 𝒱 is a base change of f and so locally quasi-finite by Stacks 06UB, and Stacks 06UD composes it with the given 1-morphism.

theorem isQuasiDM_and_transfersLocalQuasiFiniteness_of_isLocallyQuasiFinite
    (f : 𝒳 ⟶ 𝒴) (hf : IsLocallyQuasiFinite B S hS f) :
    IsQuasiDM B S hS f ∧ TransfersLocalQuasiFinitenessOnSpaceBaseChanges B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.locallyQuasiFiniteCoverOnEverySpaceBaseChange_of_isQuasiDM_of_transfers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteRelativePresentation.lean, line 212. The attribute's comment: “the implication (2) => (3), granted the substantial direction of Tag 06MF as hPresentation, which is how Tag 06UE is carried in this library”.

Stacks 06UF, (2) ⟹ (3). If f is quasi-DM and transfers local quasi-finiteness to the projections of its algebraic-space base changes, then each of those base changes has a surjective, flat, locally finitely presented and locally quasi-finite cover by an algebraic space which is locally quasi-finite over the base.

The cover is the one Stacks 06UE produces from the quasi-DM condition; it is locally quasi-finite in the sense of Properties of Stacks, Section 04XB, hence in the sense of Stacks 06PU by Stacks 06UA, and the second conjunct of clause (2) then makes its composite to the base locally quasi-finite.

theorem locallyQuasiFiniteCoverOnEverySpaceBaseChange_of_isQuasiDM_of_transfers
    (hPresentation : Stack.ExistsQuasiDMPresentationOfIsAbsolutelyQuasiDM.{u, w} B S hS
      (BigFppfSite.contains_terminal B))
    (f : 𝒳 ⟶ 𝒴) (hf : IsQuasiDM B S hS f)
    (htr : TransfersLocalQuasiFinitenessOnSpaceBaseChanges B S hS f) :
    LocallyQuasiFiniteCoverOnEverySpaceBaseChange B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.locallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange_of_onEverySpaceBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteRelativePresentation.lean, line 231. The attribute's comment: “the implication (3) => (4), unconditionally”.

Stacks 06UF, (3) ⟹ (4). Every algebraic stack has a smooth surjective chart by a scheme of the site, and a smooth 1-morphism is flat and locally of finite presentation, so the universal clause (3) applied to that chart is clause (4).

theorem locallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange_of_onEverySpaceBaseChange (f : 𝒳 ⟶ 𝒴)
    (hf : LocallyQuasiFiniteCoverOnEverySpaceBaseChange B S hS f) :
    LocallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_of_locallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteRelativePresentation.lean, line 250. The attribute's comment: “the quasi-DM conjunct of the conclusion of (4) => (1), unconditionally. The local finite type and field-valued-fibre conjuncts of (4) => (1) are NOT carried”.

Stacks 06UF, the quasi-DM conjunct of (4) ⟹ (1). A locally quasi-finite flat cover of 𝒳 ×_𝒴 𝒱 by an algebraic space over one algebraic space 𝒱 surjective, flat and locally of finite presentation over 𝒴 makes f quasi-DM.

The cover is locally quasi-finite in the sense of Stacks 06PU, hence in the sense of Properties of Stacks, Section 04XB by Stacks 06UA, which is clause (3) of Stacks 06UE; that lemma's implication (3) ⟹ (1) is the conclusion.

theorem isQuasiDM_of_locallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange (f : 𝒳 ⟶ 𝒴)
    (hf : LocallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange B S hS f) :
    IsQuasiDM B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.locallyQuasiFiniteCoverOnEverySpaceBaseChange_of_isQuasiDM_of_transfers_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteRelativePresentationUnconditional.lean, line 160. The attribute's comment: “the implication (2) => (3)”.

Stacks 06UF, (2) ⟹ (3). If f is quasi-DM and transfers local quasi-finiteness to the projections of its algebraic-space base changes, then each of those base changes has a surjective, flat, locally finitely presented and locally quasi-finite cover by an algebraic space which is locally quasi-finite over the base.

This is ...AlgebraicStacks.locallyQuasiFiniteCoverOnEverySpaceBaseChange_of_isQuasiDM_of_transfers with its hypothesis, the substantial direction of Stacks 06MF, discharged by AlgebraicGeometry.Stack.hasQuasiDMPresentation_of_isAbsolutelyQuasiDM.

theorem locallyQuasiFiniteCoverOnEverySpaceBaseChange_of_isQuasiDM_of_transfers_unconditional
    (f : 𝒳 ⟶ 𝒴) (hf : IsQuasiDM B S hS f)
    (htr : TransfersLocalQuasiFinitenessOnSpaceBaseChanges B S hS f) :
    LocallyQuasiFiniteCoverOnEverySpaceBaseChange B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_of_locallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteRelativePresentationUnconditional.lean, line 240. The attribute's comment: “the local finite type conjunct of the conclusion of (4) => (1)”.

Stacks 06UF, the local finite type conjunct of (4) ⟹ (1). A locally quasi-finite flat cover of 𝒳 ×_𝒴 𝒱 by an algebraic space over one algebraic space 𝒱 surjective, flat and locally of finite presentation over 𝒴 makes f locally of finite type.

The composite 𝒰 ⟶ 𝒱 is locally quasi-finite, hence locally of finite type, and 𝒰 covers 𝒳 ×_𝒴 𝒱 by a surjective flat 1-morphism locally of finite presentation, so the projection 𝒳 ×_𝒴 𝒱 ⟶ 𝒱 is locally of finite type by Stacks 06U8; that projection is the base change of f along 𝒱 ⟶ 𝒴, so Stacks 06U7 descends local finite type to f.

theorem isLocallyOfFiniteType_of_locallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange (f : 𝒳 ⟶ 𝒴)
    (hf : LocallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange B S hS f) :
    IsLocallyOfFiniteType B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.discreteTopology_points_of_locallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteRelativePresentationUnconditional.lean, line 351. The attribute's comment: “the field-valued-fibre conjunct of the conclusion of (4) => (1)”.

Stacks 06UF, the field-valued-fibre conjunct of (4) ⟹ (1). A locally quasi-finite flat cover of 𝒳 ×_𝒴 𝒱 by an algebraic space over one algebraic space 𝒱 surjective, flat and locally of finite presentation over 𝒴 makes the fibre of f over every field-valued point of 𝒴 have discrete space of points.

This is the source's reduction of the third condition of Stacks 06PU to a field-valued point which lifts to the chart. The chart being surjective, the fibre 𝒱 ×_𝒴 Spec(k) has a point, and a point of an algebraic stack is an equivalence class of field-valued points, so some field extension k'/k carries v : Spec(k') ⟶ 𝒱 and e : Spec(k') ⟶ Spec(k) with v ≫ g 2-isomorphic to e ≫ y. Over v the fibre is discrete, which is discreteTopology_points_twoFibreProduct_of_hasLocallyQuasiFiniteFlatSpaceCoverOver; changing the cospan leg by that 2-isomorphism (CategoryTheory.Bicategory.isTwoFibreProduct_reindexSnd) and pasting (Stacks 02XD) identify the fibre over v ≫ g with (𝒳 ×\_𝒴 Spec(k)) ×\_\{Spec(k)} Spec(k'), and that maps onto 𝒳 ×\_𝒴 Spec(k) by a base change of e.

e is surjective by AlgebraicGeometry.Stack.isSurjective_of_fieldSpectrum, the spectrum of a field having exactly one point, and it is universally open because its target is the algebraic stack of the spectrum of a field (Stacks 06DN through universallyOpen_to_fieldSpectrumStack), so its base change is open on points by Stacks 06U1. No finiteness of k'/k is needed: the source gets openness from flatness and local finite presentation of a finite extension, and universal openness over a field spectrum gives it for an arbitrary one.

theorem discreteTopology_points_of_locallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange (f : 𝒳 ⟶ 𝒴)
    (hf : LocallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange B S hS f)
    (k : Type u) [Field k] (hk : B.Contains (Spec (.of k))) (toBase : Spec (.of k) ⟶ S)
    (y : Stack.schemeStack.{u, w} B S hS (Over.mk (⟨toBase⟩ : B.obj hk ⟶ B.obj hS)) ⟶ 𝒴) :
    @DiscreteTopology
      (Stack.points B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS f y).pt.val.val
        (Stack.twoFibreProductSquareAlgebraicStacks B S hS f y).pt.val.property)
      (Stack.pointTopology B S hS
        (Stack.twoFibreProductSquareAlgebraicStacks B S hS f y).pt.val)

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyQuasiFinite_of_locallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteRelativePresentationUnconditional.lean, line 419. The attribute's comment: “the implication (4) => (1)”.

Stacks 06UF, (4) ⟹ (1). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S admitting one algebraic space 𝒱 surjective, flat and locally of finite presentation over 𝒴 whose base change 𝒳 ×_𝒴 𝒱 has a surjective, flat, locally finitely presented and locally quasi-finite cover by an algebraic space locally quasi-finite over 𝒱 is locally quasi-finite.

The three conjuncts of Stacks 06PU are the three preceding theorems.

theorem isLocallyQuasiFinite_of_locallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange (f : 𝒳 ⟶ 𝒴)
    (hf : LocallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange B S hS f) :
    IsLocallyQuasiFinite B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyQuasiFinite_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteRelativePresentationUnconditional.lean, line 443.

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

f is locally quasi-finite (Stacks 06PU);

f is quasi-DM (Stacks 04YW) and for every algebraic space 𝒱 over 𝒴 every locally quasi-finite 1-morphism 𝒰 ⟶ 𝒳 ×_𝒴 𝒱 out of an algebraic space has locally quasi-finite composite 𝒰 ⟶ 𝒱;

for every algebraic space 𝒱 over 𝒴 there is a surjective, flat, locally finitely presented and locally quasi-finite 1-morphism 𝒰 ⟶ 𝒳 ×_𝒴 𝒱 out of an algebraic space whose composite 𝒰 ⟶ 𝒱 is locally quasi-finite;

there are algebraic spaces 𝒰 and 𝒱, a surjective, flat and locally finitely presented 1-morphism 𝒱 ⟶ 𝒴, and a surjective, flat, locally finitely presented and locally quasi-finite 1-morphism 𝒰 ⟶ 𝒳 ×_𝒴 𝒱 whose composite 𝒰 ⟶ 𝒱 is locally quasi-finite.

theorem isLocallyQuasiFinite_tfae (f : 𝒳 ⟶ 𝒴) :
    List.TFAE
      [IsLocallyQuasiFinite B S hS f,
        IsQuasiDM B S hS f ∧ TransfersLocalQuasiFinitenessOnSpaceBaseChanges B S hS f,
        LocallyQuasiFiniteCoverOnEverySpaceBaseChange B S hS f,
        LocallyQuasiFiniteCoverOnSomeFlatSpaceBaseChange B S hS f]

Tag 06UG, a lemma

Tag 06UG in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyQuasiFinite_of_comp_of_isQuasiDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallyQuasiFiniteCancellation.lean, line 105.

Stacks 06UG. If a composite of 1-morphisms of algebraic stacks over S is locally quasi-finite and its second factor is quasi-DM, then its first factor is locally quasi-finite.

f is 2-isomorphic to its graph over 𝒵 followed by the second projection of the canonical 2-fibre product of the cospan (f ≫ g, g). The graph is locally quasi-finite because g is quasi-DM (Stacks 050I part (3) and Stacks 06UA), the projection is a base change of f ≫ g and so is locally quasi-finite by Stacks 06UB, and Stacks 06UD composes the two.

theorem isLocallyQuasiFinite_of_comp_of_isQuasiDM
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsLocallyQuasiFinite B S hS (f ≫ g)) (hg : IsQuasiDM B S hS g) :
    IsLocallyQuasiFinite B S hS f

Sources

LeanAlgebraicGeometry.Stack.isLocallyOfFiniteType_and_discreteTopology_of_isLocallyQuasiFinite · AlgebraicGeometry.Stack.isLocallyQuasiFinite_of_isLocallyOfFiniteType_of_discreteTopology · AlgebraicGeometry.Stack.isLocallyQuasiFinite_iff_isLocallyOfFiniteType_and_discreteTopology · AlgebraicGeometry.Stack.AlgebraicStacks.IsLocallyQuasiFinite · AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyQuasiFinite_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.locallyQuasiFinite_of_isLocallyQuasiFinite_over_field · AlgebraicGeometry.Stack.AlgebraicStacks.locallyQuasiFinite_of_isLocallyQuasiFinite_over_fieldPoint · AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyQuasiFinite_comp

Section101.24 Quasi-finite morphisms #

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

Tag 0G2M, a definition

Tag 0G2M in the Stacks Project.

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

A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is quasi-finite when it is locally quasi-finite (Stacks 06PU) and quasi-compact (Stacks 050U).

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

Tag 0G2N, a lemma

Tag 0G2N in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiFinite_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiFiniteComposition.lean, line 53.

Stacks 0G2N. A composite of quasi-finite 1-morphisms of algebraic stacks over S is quasi-finite: local quasi-finiteness composes by Stacks 06UD and quasi-compactness by Stacks 050W.

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

Tag 0G2P, a lemma

Tag 0G2P in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiFinite_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiFiniteBaseChange.lean, line 60.

Stacks 0G2P. A base change of a quasi-finite 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is quasi-finite: the first projection of any 2-fibre product of the cospan (g, f) is quasi-finite as soon as f is.

Quasi-finiteness is local quasi-finiteness together with quasi-compactness, and the two conjuncts are inherited by Stacks 06UB and Stacks 050V respectively.

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

Tag 0G2Q, a lemma

Tag 0G2Q in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiFinite_of_comp_of_isQuasiSeparated_of_isQuasiDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiFiniteCancellation.lean, line 79.

Stacks 0G2Q. If a composite of 1-morphisms of algebraic stacks over S is quasi-finite and its second factor is quasi-separated and quasi-DM, then its first factor is quasi-finite.

Quasi-finiteness is local quasi-finiteness together with quasi-compactness, and the source's proof combines the cancellation of each conjunct: local quasi-finiteness cancels against the quasi-DM second factor by Stacks 06UG and quasi-compactness cancels against the quasi-separated second factor by Stacks 050Y.

theorem isQuasiFinite_of_comp_of_isQuasiSeparated_of_isQuasiDM
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsQuasiFinite B S hS (f ≫ g)) (hgQuasiSeparated : IsQuasiSeparated B S hS g)
    (hgQuasiDM : IsQuasiDM B S hS g) :
    IsQuasiFinite B S hS f

Sources

LeanAlgebraicGeometry.Stack.AlgebraicStacks.IsQuasiFinite · AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiFinite_comp · AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiFinite_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiFinite_of_comp_of_isQuasiSeparated_of_isQuasiDM

Section101.25 Flat morphisms #

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

Tag 06PW, a definition

Tag 06PW in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatAlgebraicStack.lean, line 84.

Stacks 06PW. A 1-morphism of algebraic stacks over S is flat when it passes the existential smooth-diagram test of Stacks 06FM at flatness of morphisms of algebraic spaces: there are algebraic spaces U, V over S, a smooth 1-morphism a from the category fibred in groupoids of U to the source which is surjective on objects, a smooth 1-morphism b from the one of V to the target, and a morphism h : U ⟶ V making the square 2-commute, with h a flat morphism of algebraic spaces.

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

Tag 06PX, a lemma

Tag 06PX in the Stacks Project.

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

Stacks 06PX. The composite of two flat 1-morphisms of algebraic stacks over S is flat.

Stacks 06PW is condition (2) of Stacks 06FM at flatness of morphisms of algebraic spaces, on the nose (AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_iff_hasPropertyOnSomeSmoothDiagram), so this is Stacks 06FP at that property: flatness is smooth local on the source-and-target by Stacks 06FC and stable under composition by Stacks 03MN, which is the source's own proof.

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

Tag 06PY, a lemma

Tag 06PY in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatBaseChange.lean, line 77.

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

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

Tag 06PZ, a lemma

Tag 06PZ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_twoFibreProduct_fst_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatDescentAlgebraicStack.lean, line 346.

Stacks 06PZ. Let f : 𝒳 ⟶ 𝒴 and g : 𝒵 ⟶ 𝒴 be 1-morphisms of algebraic stacks over S with g surjective and flat, and let P exhibit 𝒵 ×_𝒴 𝒳. If the base change 𝒵 ×_𝒴 𝒳 ⟶ 𝒵 is flat, then f is flat.

This is AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_of_isFlat_twoFibreProduct_fst with its hypothesis discharged by [Stacks Project, Tag 05VY].

theorem isFlat_twoFibreProduct_fst_descent
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hgsurj : Stack.IsSurjective B S hS g)
    (hgflat : IsFlat B S hS g)
    (hfst : IsFlat B S hS P.fst) :
    IsFlat B S hS f

Tag 06Q0, a lemma

Tag 06Q0 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_of_isSurjective_of_isFlat_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatDescentAlgebraicStack.lean, line 328.

Stacks 06Q0. Let 𝒳 ⟶ 𝒴 ⟶ 𝒵 be 1-morphisms of algebraic stacks over S. If 𝒳 ⟶ 𝒵 is flat and 𝒳 ⟶ 𝒴 is surjective and flat, then 𝒴 ⟶ 𝒵 is flat.

This is AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_of_comp_of_isSurjective_of_isFlat with its hypothesis discharged by [Stacks Project, Tag 05VY].

theorem isFlat_of_isSurjective_of_isFlat_comp
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsFlat B S hS (f ≫ g))
    (hfsurj : Stack.IsSurjective B S hS f)
    (hfflat : IsFlat B S hS f) :
    IsFlat B S hS g

Tag 0DN5, a lemma

Tag 0DN5 in the Stacks Project.

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

Stacks 0DN5. Let f : 𝒳 ⟶ 𝒴 be a flat 1-morphism of algebraic stacks over S and let g : Spec A ⟶ 𝒴 be a 1-morphism out of the spectrum of a valuation ring A, presented as an object V of the big fppf site of S with an isomorphism e of its underlying scheme with Spec A. If the closed point of Spec A — presented by a field-valued point p of the algebraic space V represents — is carried by g to a point of |𝒴| in the image of |𝒳| ⟶ |𝒴|, then there are an extension of valuation rings ι : A ⟶ A', an object V' of the site with an isomorphism e' of its underlying scheme with Spec A' over Spec ι, and a 1-morphism Spec A' ⟶ 𝒳 whose composite with f is 2-isomorphic to Spec A' ⟶ Spec A ⟶ 𝒴.

theorem exists_valuationRing_extension_lift_of_isFlat
    (A : Type u) [CommRing A] [IsDomain A] [ValuationRing A]
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (hf : IsFlat B S hS f)
    (V : BigFppfOver B S hS)
    (e : (BigFppfOver.toScheme B S hS).obj V ≅ Spec (.of A))
    (g : schemeStack.{u, w} B S hS V ⟶ 𝒴)
    (p : Space.FieldValuedPoint B S hS (yoneda.obj V))
    (hp : e.hom ((BigFppfOver.toScheme B S hS).map p.value
      (IsLocalRing.closedPoint p.carrier)) = IsLocalRing.closedPoint A)
    (himage : ∃ x : points B S hS 𝒳, pointsMap B S hS f x =
      pointsMap B S hS g (spacePointMap B S hS (yoneda.obj V)
        (schemeFibredCategory B S hS V) (schemeRepChart B S hS V)
        (p.class B S hS (yoneda.obj V)))) :
    ∃ (A' : Type u) (_ : CommRing A') (_ : IsDomain A') (_ : ValuationRing A') (ι : A →+* A'),
      ValuationRing.IsExtension ι ∧
      ∃ (V' : BigFppfOver B S hS)
        (e' : (BigFppfOver.toScheme B S hS).obj V' ≅ Spec (.of A'))
        (j : V' ⟶ V) (lift : schemeStack.{u, w} B S hS V' ⟶ 𝒳),
        (BigFppfOver.toScheme B S hS).map j ≫ e.hom =
            e'.hom ≫ Spec.map (CommRingCat.ofHom ι) ∧
          Nonempty (lift ≫ f ≅ schemeStackMap.{u, w} B S hS j ≫ g)

Sources

LeanAlgebraicGeometry.Stack.AlgebraicStacks.IsFlat · AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_comp · AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_twoFibreProduct_fst_descent · AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_of_isSurjective_of_isFlat_comp · AlgebraicGeometry.Stack.AlgebraicStacks.exists_valuationRing_extension_lift_of_isFlat

Section101.26 Flat at a point #

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

Tag 0CIC, a lemma

Tag 0CIC in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_isFlatAt_iff_forall_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatAtAPoint/IndependenceOfDiagram.lean, line 802.

Stacks 0CIC. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let x be a point of |𝒳|. The top horizontal morphism of some diagram of AlgebraicGeometry.Stack.AlgebraicStacks.PointedFlatDiagram is flat at its marked point if and only if the top horizontal morphism of every such diagram is.

The forward implication is the iterated-2-fibre-product chase of the source; the backward one holds because such a diagram exists through every point of |𝒳|.

theorem exists_isFlatAt_iff_forall_isFlatAt {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (x : points B S hS 𝒳) :
    (∃ d : PointedFlatDiagram B S hS f x, Space.IsFlatAt B S hS d.h d.u) ↔
      ∀ d : PointedFlatDiagram B S hS f x, Space.IsFlatAt B S hS d.h d.u

Tag 0CID, a definition

Tag 0CID in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsFlatAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatAtAPoint/PointedFlatDiagram.lean, line 475.

Stacks 0CID. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is flat at a point x of |𝒳| when the top horizontal morphism of some diagram of AlgebraicGeometry.Stack.AlgebraicStacks.PointedFlatDiagram is flat at its marked point.

Stacks 0CIC identifies this with the corresponding condition on every such diagram, so the choice of the existential formulation is immaterial.

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

Sources

LeanAlgebraicGeometry.Stack.AlgebraicStacks.exists_isFlatAt_iff_forall_isFlatAt · AlgebraicGeometry.Stack.AlgebraicStacks.IsFlatAt

Section101.27 Morphisms of finite presentation #

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

Tag 06Q2, a definition

Tag 06Q2 in the Stacks Project.

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

Stacks 06Q2, part (1). A 1-morphism of algebraic stacks over S is locally of finite presentation when it passes the universal smooth-diagram test of Stacks 06FM at local finite presentation of morphisms of algebraic spaces: every 2-commutative square of algebraic spaces over f whose two vertical 1-morphisms are smooth and whose every comparison 1-morphism to a 2-fibre product is smooth has its top horizontal morphism locally of finite presentation.

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

AlgebraicGeometry.Stack.AlgebraicStacks.IsFinitePresentation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FinitePresentationAlgebraicStack.lean, line 104. The attribute's comment: “part (2): finite presentation”.

Stacks 06Q2, part (2). A 1-morphism of algebraic stacks over S is of finite presentation when it is locally of finite presentation, quasi-compact and quasi-separated.

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

Tag 06Q3, a lemma

Tag 06Q3 in the Stacks Project.

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

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

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

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

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

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

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

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

Tag 06Q4, a lemma

Tag 06Q4 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFinitePresentation_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FinitePresentationBaseChangeAlgebraicStack.lean, line 101. The attribute's comment: “locally of finite presentation”.

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

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

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

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

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

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

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

Tag 06Q5, a lemma

Tag 06Q5 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isFiniteType_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FinitenessPresentationToType.lean, line 38. The attribute's comment: “finite presentation implies finite type”.

A 1-morphism of algebraic stacks over S of finite presentation is of finite type.

theorem isFiniteType_of_isFinitePresentation
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsFinitePresentation B S hS f) :
    IsFiniteType B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteTypeAlgebraicStack.lean, line 69. The attribute's comment: “first assertion”.

A 1-morphism of algebraic stacks over S which is locally of finite presentation is locally of finite type.

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

Tag 0DQJ, a lemma

Tag 0DQJ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFinitePresentation_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FinitePresentationNoetherian.lean, line 120. The attribute's comment: “part (1)”. References: SGA 3 VIA (2.5.4), “more general”.

Stacks 0DQJ, part (1). A 1-morphism of algebraic stacks over S which is locally of finite type and whose target is locally Noetherian is locally of finite presentation. Local Noetherianity of an algebraic stack over S is the smooth-scheme-atlas criterion of Stacks 04YG at AlgebraicGeometry.IsLocallyNoetherian.

Local finite type is the universal smooth-diagram test of Stacks 06FM, so the equivalence of its conditions (1) and (2) gives a diagram of algebraic spaces over f with smooth vertical 1-morphisms, left vertical 1-morphism surjective on objects, and top horizontal morphism h locally of finite type. The right vertical 1-morphism is a smooth algebraic-space chart of the target, so its source is locally Noetherian by Stacks 04YF, and Stacks 06G4 part (1) makes h locally of finite presentation; the same diagram read backwards across Stacks 06FM at local finite presentation is the conclusion.

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

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

Stacks 0DQJ, part (2). A 1-morphism of algebraic stacks over S which is of finite type and quasi-separated and whose target is locally Noetherian is of finite presentation.

Being of finite presentation is being locally of finite presentation, quasi-compact and quasi-separated (Stacks 06Q2 part (2)) and being of finite type is being locally of finite type together with quasi-compactness (Stacks 06FS part (2)), so only the first conjunct has content and that is part (1).

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

Tag 06Q6, a lemma

Tag 06Q6 in the Stacks Project.

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

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

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

Tag 0CMG, a lemma

Tag 0CMG in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFinitePresentation_relativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DiagonalFinitePresentation.lean, line 138. The attribute's comment: “locally of finite presentation”.

Stacks 0CMG, first assertion. The relative diagonal of a 1-morphism of algebraic stacks over S which is locally of finite type is locally of finite presentation.

The first projection of the 2-fibre product undoes the diagonal, is a base change of f and is therefore locally of finite type by Stacks 06FU, so Stacks 06Q6 cancels it against the identity of 𝒳.

theorem isLocallyOfFinitePresentation_relativeDiagonal
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyOfFinitePresentation B S hS (relativeDiagonal B S hS f)

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

Stacks 0CMG, second assertion. The relative diagonal of a quasi-separated 1-morphism of algebraic stacks over S which is locally of finite type is of finite presentation.

Local finite presentation is the first assertion; quasi-compactness of the diagonal is part (2) of Stacks 04Z0 read off quasi-separatedness of f; and quasi-separatedness of the diagonal is Section 04XB quasi-compactness of the second diagonal, which is part (2) of Stacks 04YZ at the same hypothesis, together with Section 04XB quasi-separatedness of the second diagonal, which is unconditional by part (4) of Stacks 04YQ and Stacks 03KK.

theorem isFinitePresentation_relativeDiagonal
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsLocallyOfFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f) :
    IsFinitePresentation B S hS (relativeDiagonal B S hS f)

Tag 06Q7, a lemma

Tag 06Q7 in the Stacks Project.

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

Stacks 06Q7. An open immersion of algebraic stacks over S is locally of finite presentation.

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

theorem isLocallyOfFinitePresentation_of_isOpenImmersion
    (f : 𝒳 ⟶ 𝒴) (hf : IsOpenImmersion B S hS f) :
    IsLocallyOfFinitePresentation B S hS f

Tag 0CPP, a lemma

Tag 0CPP in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_iff_of_fppfCoverStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyFppfCoverGeneral.lean, line 134.

Stacks 0CPP. 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 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.

Unlike Stacks 06TY the cover g is not assumed representable by algebraic spaces.

theorem hasRelativeProperty_iff_of_fppfCoverStack
    (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)
    (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 0DN6, a lemma

Tag 0DN6 in the Stacks Project.

AlgebraicGeometry.Stack.hasProperty_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FppfDescentProperty.lean, line 248.

Let P be smooth local on the source-and-target, with fppf local restriction to algebraic spaces, and let g : 𝒵 ⟶ 𝒴 be surjective, flat and locally of finite presentation. If the base change 𝒵 ×_𝒴 𝒳 ⟶ 𝒵 of f : 𝒳 ⟶ 𝒴 along g has P, then f has P.

theorem hasProperty_of_baseChange
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hP : Space.IsSmoothLocalOnSourceAndTarget B S hS P)
    [hlocal : (spaceProperty B S hS P).IsLocalAtTarget
      (Space.Topology.fppf.precoverage.{u, v} B S hS)]
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (hgsurj : IsSurjective B S hS g)
    (hgflat : AlgebraicStacks.IsFlat B S hS g)
    (hglfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (hbase : HasPropertyOnSomeSmoothDiagram B S hS P
      (twoFibreProductSquareAlgebraicStacks B S hS g f).fst.hom) :
    HasPropertyOnSomeSmoothDiagram B S hS P f.hom

Tag 06Q8, a lemma

Tag 06Q8 in the Stacks Project.

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

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

theorem isLocallyOfFinitePresentation_of_baseChange
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (hgs : Stack.IsSurjective B S hS g)
    (hgflat : IsFlat B S hS g)
    (hglfp : IsLocallyOfFinitePresentation B S hS g)
    (hbase : IsLocallyOfFinitePresentation B S hS
      (Stack.twoFibreProductSquareAlgebraicStacks B S hS f g).snd) :
    IsLocallyOfFinitePresentation B S hS f

Tag 06Q9, a lemma

Tag 06Q9 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFinitePresentation_of_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FinitePresentationDescentComposition.lean, line 294.

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

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

Tag 06QA, a lemma

Tag 06QA in the Stacks Project.

AlgebraicGeometry.Stack.exists_fppfCovering_fibre_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SurjectiveFlatFppfLocalSections.lean, line 332.

Stacks 06QA. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S which is surjective, flat and locally of finite presentation. Then for every object U of the big fppf site of S and every object y of the fibre of 𝒴 over U there is an fppf covering of U such that over every member of it y is isomorphic to the image of an object of 𝒳.

The covering is a covering sieve of the big fppf topology of S, and the isomorphism over a member k : V ⟶ U is a morphism f(x) ⟶ y lying over k, which in a category fibred in groupoids is exactly an isomorphism f(x) ≅ y|_V of the fibre over V. The covering produced is a one-member one; see AlgebraicGeometry.Stack.exists_scheme_lift_of_isSurjective_isFlat_isLfp.

theorem exists_fppfCovering_fibre_lift
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hsurj : IsSurjective B S hS f)
    (hflat : AlgebraicStacks.IsFlat B S hS f)
    (hlfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS f) :
    ∀ (U : BigFppfOver B S hS) (y : 𝒴.val.val.p.Fiber U),
      ∃ R ∈ BigFppfOver.topology B S hS U,
        ∀ ⦃V : BigFppfOver B S hS⦄ ⦃k : V ⟶ U⦄, R.arrows k →
          ∃ (x : 𝒳.val.val.obj) (α : (CatFiberedInGroupoids.homFunctor f.hom).obj x ⟶ y.1),
            𝒴.val.val.p.IsHomLift k α

Tag 07AN, a lemma

Tag 07AN in the Stacks Project.

AlgebraicGeometry.Stack.exists_fppfCovering_family_fibre_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/JointlySurjectiveFlatFppfLocalSections.lean, line 275. The attribute's comment: “the covering family and the index map”.

Stacks 07AN. Let f j : 𝒳 j ⟶ 𝒴, j ∈ J, be a family of 1-morphisms of algebraic stacks over S which are each flat and locally of finite presentation and which are jointly surjective, that is |𝒴| = ⋃ j, |f j|(|𝒳 j|). Then for every object U of the big fppf site of S and every object y of the fibre of 𝒴 over U there are an fppf covering {U i → U}_{i ∈ I} of U, a map a : I → J and, for every i, an object of 𝒳 (a i) over U i whose image is isomorphic to the restriction of y to U i.

The covering is given as a family of morphisms m i : W i ⟶ U.left of the underlying category of the site which are flat, locally of finite presentation and jointly surjective on the underlying schemes — which is what an fppf covering of U is. The isomorphism over a member is rendered as a morphism from the image of the object to y lying over that member, which in a category fibred in groupoids is exactly an isomorphism in the fibre.

theorem exists_fppfCovering_family_fibre_lift {J : Type v}
    {𝒳 : J → AlgebraicStacks.{u, w} B S hS} {𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒳 j ⟶ 𝒴)
    (hflat : ∀ j, AlgebraicStacks.IsFlat B S hS (f j))
    (hlfp : ∀ j, AlgebraicStacks.IsLocallyOfFinitePresentation B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒴)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (U : BigFppfOver B S hS) (y : 𝒴.val.val.p.Fiber U) :
    ∃ (I : Type (u + 1)) (W : I → B.Schemes) (m : ∀ i, W i ⟶ U.left) (a : I → J),
      (∀ i, Flat (B.inclusion.map (m i))) ∧
        (∀ i, LocallyOfFinitePresentation (B.inclusion.map (m i))) ∧
          (∀ x : (B.inclusion.obj U.left), ∃ i, x ∈ Set.range (B.inclusion.map (m i))) ∧
            ∀ i, ∃ (x : (𝒳 (a i)).val.val.obj)
              (α : (CatFiberedInGroupoids.homFunctor (f (a i)).hom).obj x ⟶ y.1),
              𝒴.val.val.p.IsHomLift
                (Over.homMk (m i) rfl :
                  (Over.mk (m i ≫ U.hom) : BigFppfOver B S hS) ⟶ U) α

AlgebraicGeometry.Stack.exists_fppfCovering_fibre_lift_of_family, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/JointlySurjectiveFlatFppfLocalSections.lean, line 327. The attribute's comment: “the covering sieve form”.

Stacks 07AN, with the covering as a covering sieve. Under the hypotheses of AlgebraicGeometry.Stack.exists_fppfCovering_family_fibre_lift there is a covering sieve of U for the big fppf topology of S such that over every arrow of it the object y is isomorphic to the image of an object of 𝒳 j for some j.

The index j is produced per arrow of the sieve rather than by a map out of the index set of a covering family, since a sieve carries no family; see AlgebraicGeometry.Stack.exists_fppfCovering_family_fibre_lift for the family form.

theorem exists_fppfCovering_fibre_lift_of_family {J : Type v}
    {𝒳 : J → AlgebraicStacks.{u, w} B S hS} {𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : ∀ j, 𝒳 j ⟶ 𝒴)
    (hflat : ∀ j, AlgebraicStacks.IsFlat B S hS (f j))
    (hlfp : ∀ j, AlgebraicStacks.IsLocallyOfFinitePresentation B S hS (f j))
    (hjs : (Set.univ : Set (AlgebraicStacks.points B S hS 𝒴)) =
      ⋃ j, Set.range (AlgebraicStacks.pointsMap B S hS (f j)))
    (U : BigFppfOver B S hS) (y : 𝒴.val.val.p.Fiber U) :
    ∃ R ∈ BigFppfOver.topology B S hS U,
      ∀ ⦃V : BigFppfOver B S hS⦄ ⦃k : V ⟶ U⦄, R.arrows k →
        ∃ (j : J) (x : (𝒳 j).val.val.obj)
          (α : (CatFiberedInGroupoids.homFunctor (f j).hom).obj x ⟶ y.1),
          𝒴.val.val.p.IsHomLift k α

Tag 06R7, a lemma

Tag 06R7 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isOpenMap_pointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatOpenPointsAlgebraicStack.lean, line 100.

Stacks 06R7. A flat 1-morphism of algebraic stacks over S which is locally of finite presentation induces an open map on the topological spaces of points of Stacks 04XG and Stacks 04XL.

theorem isOpenMap_pointsMap {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hflat : IsFlat B S hS f) (hlfp : IsLocallyOfFinitePresentation 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 0DQK, a lemma

Tag 0DQK in the Stacks Project.

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

Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒵 ⟶ 𝒴 be a surjective, flat, locally finitely presented 1-morphism of algebraic stacks. If the base change 𝒵 ×_𝒴 𝒳 ⟶ 𝒵 of f along g is quasi-compact, then f is quasi-compact.

theorem isQuasiCompactMorphism_of_isQuasiCompactMorphism_fst_of_stack
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (hgsurj : IsSurjective B S hS g)
    (hgflat : AlgebraicStacks.IsFlat B S hS g)
    (hglfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hbase : IsQuasiCompactMorphism B S hS P.fst) :
    IsQuasiCompactMorphism B S hS f

Tag 0CPQ, a lemma

Tag 0CPQ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_isSeparated_comp_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationUniversallyInjectiveCover.lean, line 377. The attribute's comment: “universal closedness of Δ_f is added: the published statement is false without it, a section of a 1-morphism of stacks being a monomorphism only when the 1-morphism is faithful; 04XS (2) and the permanence of the three properties under forming f × f are assumed”.

Stacks 0CPQ, with universal closedness of Δ_f assumed. Let f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 be 1-morphisms of algebraic stacks over S. If f is surjective, flat, locally of finite presentation and universally injective, if the relative diagonal of f is universally closed, and if f ≫ g is separated, then g is separated.

The relative diagonal of f is surjective by Stacks 0CPN, so properness of Δ_{f ≫ g} = Δ_f ≫ i gives properness of the comparison 1-morphism i : 𝒳 ×_𝒴 𝒳 ⟶ 𝒳 ×_𝒵 𝒳; and i is a base change of Δ_g along f × f, so properness of Δ_g descends by Stacks 0CPP.

Given the other hypotheses, universal closedness of Δ_f is also a consequence of the conclusion, so the implication below is in fact an equivalence; and local finite type of a relative diagonal (part (2) of Stacks 04XS) and the three properties of f × f are assumed. See the implementation notes.

theorem isSeparated_of_isSeparated_comp_of_universallyInjective
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfSurj : Stack.IsSurjective B S hS f)
    (hfFlat : IsFlat B S hS f)
    (hfLfp : IsLocallyOfFinitePresentation B S hS f)
    (hfUI : Stack.UniversallyInjective B S hS f)
    (hh : IsSeparated B S hS (f ≫ g))
    (hdiagUC : Stack.UniversallyClosed B S hS (relativeDiagonal B S hS f).hom)
    (hdiagLFT : ∀ {𝒰 𝒱 : Stack.AlgebraicStacks.{u, w} B S hS} (k : 𝒰 ⟶ 𝒱)
      (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ (twoFibreProduct B S hS k k).val.val.obj)
      (_hy : y ⋙ (twoFibreProduct B S hS k k).val.val.p = Over.map U.hom)
      (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒰.val.val.p
            (twoFibreProduct B S hS k k).val.val.p y
            (CatFiberedInGroupoids.homFunctor (relativeDiagonal B S hS k).hom))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.IsLocallyOfFiniteType B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom)
    (hCospan : ∀ {𝒰 𝒱 𝒲 : Stack.AlgebraicStacks.{u, w} B S hS} (k : 𝒰 ⟶ 𝒱) (l : 𝒱 ⟶ 𝒲),
      Stack.IsSurjective B S hS k → IsFlat B S hS k →
      IsLocallyOfFinitePresentation B S hS k →
      Stack.IsSurjective B S hS (mapCospan B S hS k k l) ∧
        IsFlat B S hS (mapCospan B S hS k k l) ∧
        IsLocallyOfFinitePresentation B S hS (mapCospan B S hS k k l)) :
    IsSeparated B S hS g

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_isSeparated_comp_of_universallyInjective_of_isSeparated_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationUniversallyInjectiveCoverCorrected.lean, line 195. The attribute's comment: “corrected form: the relative diagonal of g is assumed separated, which holds when g is representable by algebraic spaces and is strictly weaker than the conclusion; the published statement fails, see Stacks.Examples.not_forall_isSeparated_of_isSeparated_comp_of_universallyInjective”.

Stacks 0CPQ, corrected: g with separated diagonal. Let f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 be 1-morphisms of algebraic stacks over S. If f is surjective, flat, locally of finite presentation and universally injective, if f ≫ g is separated, and if the relative diagonal Δ_g : 𝒴 ⟶ 𝒴 ×_𝒵 𝒴 is separated in the sense of Properties of Stacks, Section 04XB, then g is separated.

The added hypothesis is on g, not on f, and it is strictly weaker than the conclusion, which asks Δ_g to be proper. It is exactly what the published statement is missing: the comparison 1-morphism i : 𝒳 ×_𝒴 𝒳 ⟶ 𝒳 ×_𝒵 𝒳 is a base change of Δ_g (Stacks 050H), so it is separated, and then part (3) of Stacks 050M cancels it out of the proper Δ_{f ≫ g} = Δ_f ≫ i, making Δ_f proper, in particular universally closed; the published route through Stacks 0CPN, Stacks 08AJ and Stacks 0CPP then goes through (AlgebraicGeometry.Stack.AlgebraicStacks .isSeparated_of_isSeparated_comp_of_universallyInjective_of_universallyClosed_relativeDiagonal). Without it the statement fails, the obstruction being separatedness of i: Stacks.Examples.not_forall_isSeparated_of_isSeparated_comp_of_universallyInjective. It holds whenever g is representable by algebraic spaces, AlgebraicGeometry.Stack.AlgebraicStacks .isSeparated_of_isSeparated_comp_of_universallyInjective_of_isRepresentableByAlgebraicSpaces.

theorem isSeparated_of_isSeparated_comp_of_universallyInjective_of_isSeparated_diagonal
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfSurj : Stack.IsSurjective B S hS f)
    (hfFlat : IsFlat B S hS f)
    (hfLfp : IsLocallyOfFinitePresentation B S hS f)
    (hfUI : Stack.UniversallyInjective B S hS f)
    (hh : IsSeparated B S hS (f ≫ g))
    (hΔg : Stack.IsSeparated.{u, u, u + 1} B S hS
      (Stack.relativeDiagonal.{u, u, u + 1} B S hS 𝒴.val 𝒵.val g.hom)) :
    IsSeparated B S hS g

Sources

Section101.28 Gerbes #

Section 101.28 of the Stacks Project, Tag 06QB. 15 tags here are carried by 35 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06QC, a definition

Tag 06QC in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsGerbeOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Gerbe.lean, line 64. The attribute's comment: “gerbe over an algebraic stack”.

Stacks 06QC. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S makes 𝒳 a gerbe over 𝒴 when its underlying functor makes 𝒳 a gerbe over 𝒴 in the sense of Stacks 06P2, for the fppf topology on the big fppf site of S.

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

AlgebraicGeometry.Stack.AlgebraicStacks.IsGerbe, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Gerbe.lean, line 72. The attribute's comment: “gerbe”.

Stacks 06QC. An algebraic stack 𝒳 over S is a gerbe when there is an algebraic stack 𝒴 representable by an algebraic space over S and a 1-morphism 𝒳 ⟶ 𝒴 making 𝒳 a gerbe over 𝒴.

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

Tag 06QD, a lemma

Tag 06QD in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_algebraicSpace_isGerbeOver_isoClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeIsoClasses.lean, line 107.

Stacks 06QD. If an algebraic stack 𝒳 over S is a gerbe, then the fppf sheafification of the presheaf U ↦ Ob(𝒳_U)/≅ is (the universe lift of) an algebraic space F, and 𝒳 is a gerbe over the algebraic stack 𝒴 representable by F by a 1-morphism inducing the unit of the sheafification on isomorphism classes.

theorem exists_algebraicSpace_isGerbeOver_isoClasses (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsGerbe B S hS 𝒳) :
    letI : 𝒳.val.val.p.IsFibered := (CatFiberedInGroupoids.isFiberedInGroupoids 𝒳.val).isFibered
    ∃ F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u, IsAlgebraicSpace B S hS F ∧
      ∃ (e : F ⋙ uliftFunctor.{u + 1} ≅ sheafifiedIsoClasses B S hS 𝒳)
        (𝒴 : Stack.AlgebraicStacks.{u, w} B S hS) (g : 𝒳 ⟶ 𝒴), IsGerbeOver B S hS g ∧
          letI : 𝒴.val.val.p.IsFibered :=
            (CatFiberedInGroupoids.isFiberedInGroupoids 𝒴.val).isFibered
          ∃ eY : 𝒴.val.val.p.isoClassPresheaf ≅ F ⋙ uliftFunctor.{u + 1},
            Functor.isoClassMap (Functor.isFibredOneMorphism_of_isFiberedInGroupoids
              (CatFiberedInGroupoids.isFiberedInGroupoids 𝒴.val)
              (CatFiberedInGroupoids.homFunctor_comp_p g.hom)) ≫ eY.hom ≫ e.hom =
              (BigFppfOver.topology B S hS).toSheafify (isoClassPresheaf B S hS 𝒳)

AlgebraicGeometry.Stack.AlgebraicStacks.exists_isGerbeOver_isoClassSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeOverIsoClassSpace.lean, line 70.

Stacks 06QD. If an algebraic stack 𝒳 over S is a gerbe, then the fppf sheafification of the presheaf U ↦ Ob(𝒳_U)/≅ is (the universe lift of) an algebraic space F, and 𝒳 is a gerbe over F: there are an algebraic stack 𝒴 represented by F through an equivalence E over the site (Stacks 04SV) and a 1-morphism g : 𝒳 ⟶ 𝒴 making 𝒳 a gerbe over 𝒴, such that the sheafification unit sends the class of x to the section of F named by the class of g(x).

theorem exists_isGerbeOver_isoClassSpace
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) (h𝒳 : IsGerbe B S hS 𝒳) :
    letI : 𝒳.val.val.p.IsFibered := (CatFiberedInGroupoids.isFiberedInGroupoids 𝒳.val).isFibered
    ∃ F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u, IsAlgebraicSpace B S hS F ∧
      ∃ (e : F ⋙ uliftFunctor.{u + 1} ≅ sheafifiedIsoClasses B S hS 𝒳)
        (𝒴 : Stack.AlgebraicStacks.{u, w} B S hS)
        (E : StacksRepresentableCFG.EquivalenceOver
          𝒴.val.val.p (presheafOfCategories (F ⋙ typeToCat)).p)
        (g : 𝒳 ⟶ 𝒴), IsGerbeOver B S hS g ∧
          letI : 𝒴.val.val.p.IsFibered :=
            (CatFiberedInGroupoids.isFiberedInGroupoids 𝒴.val).isFibered
          ∀ (U : (BigFppfOver B S hS)ᵒᵖ) (c : (isoClassPresheaf B S hS 𝒳).obj U),
            e.inv.app U (((BigFppfOver.topology B S hS).toSheafify
              (isoClassPresheaf B S hS 𝒳)).app U c) =
              ULift.up (PresheafOfCategories.elementsIsoClassEquiv F E U.unop
                ((Functor.isoClassMap (Functor.isFibredOneMorphism_of_isFiberedInGroupoids
                  (CatFiberedInGroupoids.isFiberedInGroupoids 𝒴.val)
                  (CatFiberedInGroupoids.homFunctor_comp_p g.hom))).app U c))

Tag 06QE, a lemma

Tag 06QE in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isGerbeOver_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeBaseChange.lean, line 119.

Stacks 06QE. In a 2-fibre-product square of algebraic stacks over S with cospan (f : 𝒳 ⟶ 𝒴, g : 𝒴' ⟶ 𝒴), if f makes 𝒳 a gerbe over 𝒴 then the projection to 𝒴' makes the apex a gerbe over 𝒴'.

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

Tag 06R8, a lemma

Tag 06R8 in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.IsGerbeOver.comp, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Gerbe/Basic.lean, line 229 (StacksFrontier).

Tag 06QF, a lemma

Tag 06QF in the Stacks Project.

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

Stacks 06QF. Let
𝒳' ⟶ 𝒳
↓     ↓
𝒴' ⟶ 𝒴
be a 2-fibre-product square of algebraic stacks over S, given as a 2-commutative square P over the cospan (f : 𝒳 ⟶ 𝒴, g : 𝒴' ⟶ 𝒴) with the 2-categorical universal property, so that P.pt is 𝒳' and P.snd is the base change of f. If g is surjective, flat and locally of finite presentation and P.snd makes 𝒳' a gerbe over 𝒴', then f makes 𝒳 a gerbe over 𝒴.

This is the descent direction; the base-change direction is AlgebraicGeometry.Stack.AlgebraicStacks.isGerbeOver_of_isTwoFibreProduct, Stacks 06QE.

theorem isGerbeOver_of_snd_of_isSurjective_isFlat_isLfp {f : 𝒳 ⟶ 𝒴} {g : 𝒴' ⟶ 𝒴}
    (P : Bicategory.TwoCommSq f g) (hP : Bicategory.IsTwoFibreProduct P)
    (hgsurj : Stack.IsSurjective B S hS g) (hgflat : IsFlat B S hS g)
    (hglfp : IsLocallyOfFinitePresentation B S hS g)
    (hgerbe : IsGerbeOver B S hS P.snd) :
    IsGerbeOver B S hS f

Tag 06QG, a lemma

Tag 06QG in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_and_isLocallyOfFinitePresentation_section_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeFlatLocalSection.lean, line 191. The attribute's comment: “part (3): flatness and local finite presentation of the section”.

A section of a gerbe over an algebraic space is flat and locally of finite presentation. Let π : 𝒳 ⟶ 𝒰 make 𝒳 a gerbe over an algebraic stack 𝒰 which is representable by an algebraic space, and let x : 𝒰 ⟶ 𝒳 be a section of π. Then x is flat and locally of finite presentation.

Together with AlgebraicGeometry.Stack.isSurjective_of_section_of_isGerbeOver this is Stacks 06QG part (3), at the source's generality; the three parts of the tag are assembled in StacksFrontier.AlgebraicGeometry.Stacks.GerbeSectionClassifyingStack.

AlgebraicGeometry.Stack.exists_single_cover_section_factorisation_of_isGerbeOver produces a surjective, flat, locally finitely presented q : 𝒱 ⟶ 𝒳 out of the algebraic stack of an object of the site together with a γ : 𝒱 ⟶ 𝒰 with γ ≫ x = q on the nose, and AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_and_isLocallyOfFinitePresentation_of_factorisation turns such a factorisation into the conclusion by the Stacks 06NR step and the descent along q. The three representability data that step needs are the two instances of isRepresentableByAlgebraicSpace_pt at the cospans (q, q) and (q, x) and Stacks 04SV for the slice of the site over V; the leg q is representable by algebraic spaces by condition (3) of Stacks 045G, its source being the algebraic stack of an object of the site, and the leg x by Stacks 045G condition (2) through AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_of_isAlgebraicStack, its source being representable by an algebraic space.

theorem isFlat_and_isLocallyOfFinitePresentation_section_of_isGerbeOver
    {𝒰 𝒳 : Stack.AlgebraicStacks.{u, w} B S hS}
    (π : 𝒳 ⟶ 𝒰) (x : 𝒰 ⟶ 𝒳) (hx : x ≫ π ≅ 𝟙 𝒰)
    (hπ : IsGerbeOver B S hS π)
    (h𝒰 : Stack.IsRepresentableByAlgebraicSpace B S hS 𝒰.val) :
    IsFlat B S hS x ∧ IsLocallyOfFinitePresentation B S hS x

AlgebraicGeometry.Stack.isSurjective_of_section_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeIsomGroupSection.lean, line 67. The attribute's comment: “part (3): surjectivity only; (1), (2), flatness and finite presentation unproved”.

Let π : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S making 𝒳 a gerbe over 𝒴, and let x : 𝒴 ⟶ 𝒳 be a section of π, i.e. a 1-morphism with a 2-isomorphism x ≫ π ≅ 𝟙 𝒴. Then x is surjective.

theorem isSurjective_of_section_of_isGerbeOver
    (π : 𝒳 ⟶ 𝒴) (x : 𝒴 ⟶ 𝒳) (hx : x ≫ π ≅ 𝟙 𝒴)
    (hπ : AlgebraicStacks.IsGerbeOver B S hS π) :
    IsSurjective B S hS x

AlgebraicGeometry.Stack.AlgebraicStacks.exists_grpObj_nonempty_equivalenceOver_quotientStackOfAction_of_section_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeSectionClassifyingStack.lean, line 351.

Stacks 06QG. Let π : 𝒳 ⟶ 𝒰 be a 1-morphism from an algebraic stack 𝒳 over S to the algebraic stack 𝒰 of an algebraic space Z over S, let x : 𝒰 ⟶ 𝒳 be a section of π — a 1-morphism together with a 2-isomorphism x ≫ π ≅ 𝟙 𝒰 — and let π make 𝒳 a gerbe over 𝒰. Write G = Isom_𝒳(x, x) for the automorphism sheaf of the section, an algebraic space over Z through AlgebraicGeometry.Stack.isomSpaceOverSpaceProj. Then

G carries the structure of a group algebraic space over Z, and the quotient stack of its trivial action on Z is equivalent, over the big fppf site of S, to 𝒳;

G ⟶ Z is flat and locally of finite presentation;

x is surjective, flat and locally of finite presentation.

Part (1) is stated as the existence of a group algebraic space G' over Z together with an isomorphism of G' with G over Z; that G' is the stabilizer of the self-intersection groupoid of Stacks 04T4 (4), whose group law is groupoid composition — composition of automorphisms of x — by Stacks 0447 (AlgebraicGeometry.GroupoidInAlgebraicSpaces.stabilizer_mul_comp_arrow), and which is all of the arrow space of that groupoid because for a section its source and target agree. The equivalence is the canonical 1-morphism of Stacks 04T4 (5), carried across the identification of the self-intersection groupoid with the trivial-action groupoid of its stabilizer.

theorem exists_grpObj_nonempty_equivalenceOver_quotientStackOfAction_of_section_of_isGerbeOver
    (π : 𝒳 ⟶ Stack.algebraicSpaceStack.{u, w} B S hS Z hZ)
    (hx : x ≫ π ≅ 𝟙 (Stack.algebraicSpaceStack.{u, w} B S hS Z hZ))
    (hπ : IsGerbeOver B S hS π) :
    (∃ (G : Over (⟨Z, hZ⟩ : AlgebraicSpaces B S hS).obj) (hGrp : GrpObj G)
        (hG : IsAlgebraicSpace B S hS G.left)
        (_ι : G ≅ Over.mk (Stack.isomSpaceOverSpaceProj B S hS Z hZ x x)),
        letI : GrpObj G := hGrp
        letI : ModObj G (𝟙_ (Over (⟨Z, hZ⟩ : AlgebraicSpaces B S hS).obj)) :=
          ModObj.trivialAction G _
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (Stack.quotientStackOfAction (⟨Z, hZ⟩ : AlgebraicSpaces B S hS) G (𝟙_ _) hG hZ).p
          𝒳.val.val.p)) ∧
      Space.IsFlat B S hS (Stack.isomSpaceOverSpaceProj B S hS Z hZ x x) ∧
      Space.IsLocallyOfFinitePresentation B S hS
        (Stack.isomSpaceOverSpaceProj B S hS Z hZ x x) ∧
      Stack.IsSurjective B S hS x ∧ IsFlat B S hS x ∧
        IsLocallyOfFinitePresentation B S hS x

AlgebraicGeometry.Stack.SelfIntersection.source_eq_target_selfIntersectionPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeSectionQuotientPresentation.lean, line 284. The attribute's comment: “part (1): the self-intersection groupoid of a section of a gerbe has equal source and target, so the group algebraic space of part (1) acts trivially”.

Stacks 06QG, part (1): the action is trivial, read on the presentation datum of Stacks 04T4 (4) and (5): the groupoid in algebraic spaces it builds from a section of a gerbe has one and the same source and target, so it is the groupoid of a group algebraic space acting trivially on the object space.

theorem source_eq_target_selfIntersectionPresentation
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val) (π : 𝒳 ⟶ 𝒴) (hx : x ≫ π ≅ 𝟙 𝒴) :
    (selfIntersectionPresentation eU eR h𝒳).groupoid.source =
      (selfIntersectionPresentation eU eR h𝒳).groupoid.target

AlgebraicGeometry.Stack.SelfIntersection.nonempty_isEquivalenceOver_canonicalMap_of_section_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeSectionQuotientPresentation.lean, line 316. The attribute's comment: “part (1): the canonical 1-morphism out of the quotient stack of the self-intersection groupoid is an equivalence”.

Stacks 06QG, part (1): the canonical equivalence. Let 𝒳 be an algebraic stack over S, let π : 𝒳 ⟶ 𝒴 make 𝒳 a gerbe over 𝒴, let x : 𝒴 ⟶ 𝒳 be a section of π, let 𝒴 be represented by an algebraic space U and let the self-intersection 𝒴 ×_{x, 𝒳, x} 𝒴 be represented by an algebraic space R — which it is, by Stacks 04T4 (1). Then the canonical 1-morphism x_can : [U/R] ⟶ 𝒳 of the presentation datum of Stacks 04T4 (4) and (5) is an equivalence over the big fppf site of S.

Full faithfulness is Stacks 04T4 (6) and needs no hypothesis beyond the presentation data; essential surjectivity on each fibre is the local essential surjectivity of the section, glued by effective descent in the quotient stack against the Mor-sheaf condition on 𝒳, and a 1-morphism of fibred categories which is fully faithful and essentially surjective on every fibre is an equivalence over the site.

The source states the equivalence at the quotient stack of the trivial action of G = Isom_𝒳(x, x). That is this equivalence: the self-intersection groupoid has equal source and target (source_eq_target_selfIntersectionPresentation), hence is the groupoid of the trivial action of its stabilizer group of Stacks 0447 on the object space, and that stabilizer is Isom_𝒳(x, x) over the object space. The passage is exists_grpObj_nonempty_equivalenceOver_quotientStackOfAction_of_section_of_isGerbeOver, in the namespace AlgebraicGeometry.Stack.AlgebraicStacks of StacksFrontier.AlgebraicGeometry.Stacks.GerbeSectionClassifyingStack, where the whole of Stacks 06QG is assembled.

theorem nonempty_isEquivalenceOver_canonicalMap_of_section_of_isGerbeOver
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val) (π : 𝒳 ⟶ 𝒴) (hx : x ≫ π ≅ 𝟙 𝒴)
    (hπ : CategoryTheory.IsGerbeOver (BigFppfOver.topology B S hS) 𝒴.val.p
      (CatFiberedInGroupoids.homFunctor π)) :
    Nonempty (Functor.IsEquivalenceOver
      (Stack.quotientStack (selfIntersectionPresentation eU eR h𝒳).groupoid).p
      𝒳.val.p
      (selfIntersectionPresentation eU eR h𝒳).canonicalMap.toFunctor)

Tag 06QH, a lemma

Tag 06QH in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isGerbeOver_of_equivalenceOver_quotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeCharacterization.lean, line 85. The attribute's comment: “(2) implies (1); the converse needs Stacks 06QG”.

Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S, let U be an algebraic space over S, let G be a group algebraic space flat and locally of finite presentation over U, and let g : U ⟶ 𝒴 be surjective, flat and locally of finite presentation. If the base change of f along g is isomorphic, as an object over U, to the quotient stack [U/G] of the trivial action of G on U, then f makes 𝒳 a gerbe over 𝒴.

theorem isGerbeOver_of_equivalenceOver_quotientStack
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (U : AlgebraicSpaces B S hS) (g : ofAlgebraicSpace.{u, w} B S hS U ⟶ 𝒴)
    (hgsurj : Stack.IsSurjective B S hS g) (hgflat : IsFlat B S hS g)
    (hglfp : IsLocallyOfFinitePresentation B S hS g)
    (G : Over U.obj) [GrpObj G] (hG : IsAlgebraicSpace B S hS G.left)
    (_hGflat : Space.IsFlat B S hS G.hom)
    (_hGlfp : Space.IsLocallyOfFinitePresentation B S hS G.hom)
    (A : Space.ActionGroupoidConstruction U G (𝟙_ (Over U.obj)) hG U.property)
    (P : Bicategory.TwoCommSq f g) (hP : Bicategory.IsTwoFibreProduct P)
    (e : StacksRepresentableCFG.EquivalenceOver
      (CatFiberedInGroupoids.homFunctor P.snd.hom)
      (quotientStackToBase A.groupoid).toFunctor) :
    IsGerbeOver B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isGerbeOver_of_hasClassifyingFppfCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeClassifyingCoverReduction.lean, line 157. The attribute's comment: “(2) implies (1), with clause (2) bundled”.

Stacks 06QH, the implication (2) ⟹ (1), packaged. A 1-morphism of algebraic stacks over S which fppf-locally on its target is the classifying stack of a flat, locally finitely presented group algebraic space makes its source a gerbe over its target.

This is AlgebraicGeometry.Stack.AlgebraicStacks.isGerbeOver_of_equivalenceOver_quotientStack with the data of clause (2) bundled into HasClassifyingFppfCover, which is the form a consumer that has clause (2) as a hypothesis — or has just produced it — can use.

theorem isGerbeOver_of_hasClassifyingFppfCover
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (h : HasClassifyingFppfCover.{u, w} B S hS f) :
    IsGerbeOver B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.hasClassifyingFppfCover_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeClassifyingCoverReduction.lean, line 180. The attribute's comment: “(1) implies (2): the reduction along a surjective, flat, locally finitely presented base change”.

The reduction step of Stacks 06QH, (1) ⟹ (2): clause (2) descends along a surjective, flat, locally finitely presented base change. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let h : 𝒴' ⟶ 𝒴 be surjective, flat and locally of finite presentation. If the base change of f along h satisfies clause (2) of Stacks 06QH, then so does f.

This is the step by which the source's proof of (1) ⟹ (2) replaces 𝒴 first by a scheme smoothly covering it and then by the member of an fppf covering of that scheme: the covering 1-morphism g : U ⟶ 𝒴' produced for the base change is composed with h, which keeps it surjective (Stacks 04ZT), flat (Stacks 06PX) and locally of finite presentation (Stacks 06Q3), and the two 2-fibre-product squares are pasted (Stacks 003Q), the pasted rectangle having the same apex and second leg as the inner square — so the identification of that apex with [U/G] over U is carried over unchanged.

theorem hasClassifyingFppfCover_of_baseChange
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 𝒴' : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (h : 𝒴' ⟶ 𝒴)
    (hhsurj : Stack.IsSurjective B S hS h) (hhflat : IsFlat B S hS h)
    (hhlfp : IsLocallyOfFinitePresentation B S hS h)
    (Q : Bicategory.TwoCommSq f h) (hQ : Bicategory.IsTwoFibreProduct Q)
    (hbc : HasClassifyingFppfCover.{u, w} B S hS Q.snd) :
    HasClassifyingFppfCover.{u, w} B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isGerbeOver_iff_hasClassifyingFppfCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeClassifyingFppfCover.lean, line 314.

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

f makes 𝒳 a gerbe over 𝒴;

there are an algebraic space U over S, a group algebraic space G over U which is flat and locally of finite presentation over U, and a surjective, flat, locally finitely presented 1-morphism U ⟶ 𝒴 such that the base change 𝒳 ×_𝒴 U is isomorphic over U to the quotient stack [U/G] of the trivial action of G on U.

Clause (2) is AlgebraicGeometry.Stack.AlgebraicStacks.HasClassifyingFppfCover.

theorem isGerbeOver_iff_hasClassifyingFppfCover
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    IsGerbeOver B S hS f ↔ HasClassifyingFppfCover.{u, w} B S hS f

Tag 06QI, a lemma

Tag 06QI in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_and_isLocallyOfFinitePresentation_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeFlatness.lean, line 381. The attribute's comment: “flat and locally of finite presentation”.

Stacks 06QI, flatness and local finite presentation. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S which makes 𝒳 a gerbe over 𝒴 is flat and locally of finite presentation.

Choose a surjective, flat, locally finitely presented p : 𝒲 ⟶ 𝒳 from an algebraic space. The comparison 𝒲 ×_𝒳 𝒲 ⟶ 𝒲 ×_𝒴 𝒲 is a base change of the relative diagonal Δ_f by Stacks 04Z1, hence locally essentially surjective by Stacks 06P1 (2)(b); its composite with the first projection of 𝒲 ×_𝒴 𝒲 is the first projection of 𝒲 ×_𝒳 𝒲, a base change of p. So Stacks 06NR for 1-morphisms of algebraic stacks makes the first projection 𝒲 ×_𝒴 𝒲 ⟶ 𝒲 flat and locally of finite presentation. That projection is the base change of p ≫ f along itself, and p ≫ f is locally essentially surjective by Stacks 06QA for p and Stacks 06P1 (2)(a); so Stacks 045D makes p ≫ f flat and locally of finite presentation, and Stacks 06Q0 and Stacks 06Q9 cancel p.

theorem isFlat_and_isLocallyOfFinitePresentation_of_isGerbeOver
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (hf : IsGerbeOver B S hS f) :
    IsFlat B S hS f ∧ IsLocallyOfFinitePresentation B S hS f

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

Stacks 06QI, surjectivity. A 1-morphism of algebraic stacks over S whose underlying functor exhibits its source as a gerbe over its target for the localized big fppf topology is surjective.

Stacks 06P1 (2)(a) lifts an object of a fibre of the target along a covering sieve; the sieve contains an arrow from a field spectrum, so an object over a field lifts after a field extension, which is surjectivity on objects in the sense of Stacks 06D4; and Stacks 04XI identifies that with surjectivity of the map on points.

theorem isSurjective_of_isGerbeOver
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴)
    (hf : CategoryTheory.IsGerbeOver
      (BigFppfOver.topology B S hS)
      𝒴.val.val.p (CatFiberedInGroupoids.homFunctor f.hom)) :
    IsSurjective B S hS f

Tag 06QJ, a proposition

Tag 06QJ in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isGerbeOver_quotientStackToBase_overArrowStabilizerQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/ArrowQuotientGerbe.lean, line 280. The attribute's comment: “the implication (2) implies (1): the quotient stack is a gerbe over U/(R/S)”.

Stacks 06QJ, the geometric half of the implication (2) ⟹ (1). The structure arrow [U/R] ⟶ X of Stacks 044R of the groupoid read over X = U/R' makes the quotient stack a gerbe over X.

The criterion is AlgebraicGeometry.Stack.isGerbeOver_quotientStackToBase_of_locallyFull (Stacks 06PE for the 1-morphism of Stacks 0DUH); its surjectivity clause is Stacks 06PG and its local-fullness clause is Stacks 046O, both in the sieve form the criterion asks for.

theorem isGerbeOver_quotientStackToBase_overArrowStabilizerQuotient
    (G : GroupoidInAlgebraicSpaces C S hS B)
    (hX : IsAlgebraicSpace C S hS
      (Space.quotientSheaf (arrowStabilizerQuotientPreRelation G)).obj) :
    CategoryTheory.IsGerbeOver (BigFppfOver.topology C S hS)
      (fibredCategory C S hS (arrowStabilizerQuotientSpace G hX).obj).val.p
      (quotientStackToBase (overArrowStabilizerQuotient G hX)).toFunctor

AlgebraicGeometry.GroupoidInAlgebraicSpaces.mono_arrowStabilizerQuotientPreRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/ArrowQuotientRelation.lean, line 396. The attribute's comment: “the implication (2) implies (1): j' = (t', s') is a monomorphism”. References: SGA 3 V (10.4), “partial”.

Stacks 043C part (2) for R/S: j' = (t', s') is a monomorphism. This is the step of the proof of Stacks 06QJ, the implication (2) ⟹ (1), which makes the quotient R' = R/S of the arrow space by the stabilizer action a relation on the object space; with the pre-equivalence-relation clause of Stacks 043X it is an equivalence relation.

Two sections of R' over a test object with the same source and the same target lift, after an fppf covering, to arrows of R with the same source and the same target, and two such arrows lie in a single orbit of the stabilizer: the loop c(a, i(b)) at their common target carries one to the other. So they already agree in R', and R' is an fppf sheaf.

theorem mono_arrowStabilizerQuotientPreRelation
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    Mono (arrowStabilizerQuotientPreRelation G)

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isEquivalenceRelation_arrowStabilizerQuotientPreRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/ArrowQuotientRelation.lean, line 565. The attribute's comment: “the implication (2) implies (1): j' = (t', s') is an equivalence relation”.

The quotient R' = R/S of the arrow space by the stabilizer action is an equivalence relation on the object space — Stacks 043C part (4). This is the step of the proof of Stacks 06QJ, the implication (2) ⟹ (1), after which the quotient X = U/R' is an algebraic space by Stacks 04S6.

By AlgebraicGeometry.Space.isEquivalenceRelation_iff_mono_and_isPreEquivalenceRelation an equivalence relation is exactly a monomorphic pre-equivalence relation, and the two halves are mono_arrowStabilizerQuotientPreRelation and isPreEquivalenceRelation_arrowStabilizerQuotientPreRelation. Nothing is assumed.

theorem isEquivalenceRelation_arrowStabilizerQuotientPreRelation
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    CategoryTheory.IsEquivalenceRelation
      (arrowStabilizerQuotientPreRelation G).target
      (arrowStabilizerQuotientPreRelation G).source

AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_and_isLocallyOfFinitePresentation_inertiaProjection_of_isGerbe, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeInertiaCharacterization.lean, line 172. The attribute's comment: “(1) implies (2)”.

Stacks 06QJ, the implication (1) ⟹ (2). If an algebraic stack 𝒳 over S is a gerbe, then the forgetful 1-morphism I_𝒳 ⟶ 𝒳 of its inertia is flat and locally of finite presentation.

Let 𝒳 ⟶ Y make 𝒳 a gerbe over an algebraic space Y and choose a smooth groupoid presentation 𝒳 ≃ [U/R] (Stacks 04T3). The composite [U/R] ⟶ Y is a gerbe, so for its restriction ψ : U ⟶ Y the arrows cover the related pairs U ×_Y U (AlgebraicGeometry.Stack.isLocallySurjective_of_isGerbeOver_restrictedMorphism), and the stabilizer of the groupoid is flat and locally of finite presentation (AlgebraicGeometry.GroupoidInAlgebraicSpaces.isFlat_stabilizer_of_isLocallySurjective, the argument of Stacks 06PL and Stacks 06PJ). The automorphism sheaves of 𝒳 are, fppf-locally, these stabilizers (Stacks 044V), and flatness and local finite presentation descend (Stacks 041W, Stacks 041T); that is clause (2), by AlgebraicGeometry.Stack.isFlat_inertiaProjection_iff_isomSpace.

theorem isFlat_and_isLocallyOfFinitePresentation_inertiaProjection_of_isGerbe
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) (h𝒳 : IsGerbe B S hS 𝒳) :
    IsFlat B S hS (Stack.inertiaProjectionAlgebraicStacks B S hS 𝒳) ∧
      IsLocallyOfFinitePresentation B S hS
        (Stack.inertiaProjectionAlgebraicStacks B S hS 𝒳)

AlgebraicGeometry.Stack.AlgebraicStacks.isGerbe_iff_isFlat_and_isLocallyOfFinitePresentation_inertiaProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeInertiaCharacterization.lean, line 224.

Stacks 06QJ. An algebraic stack 𝒳 over S is a gerbe if and only if the forgetful 1-morphism I_𝒳 ⟶ 𝒳 of its inertia is flat and locally of finite presentation.

The implication (1) ⟹ (2) is isFlat_and_isLocallyOfFinitePresentation_inertiaProjection_of_isGerbe, and the implication (2) ⟹ (1) is isGerbe_of_isFlat_and_isLocallyOfFinitePresentation_inertiaProjection.

theorem isGerbe_iff_isFlat_and_isLocallyOfFinitePresentation_inertiaProjection
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) :
    IsGerbe B S hS 𝒳 ↔
      IsFlat B S hS (Stack.inertiaProjectionAlgebraicStacks B S hS 𝒳) ∧
        IsLocallyOfFinitePresentation B S hS
          (Stack.inertiaProjectionAlgebraicStacks B S hS 𝒳)

AlgebraicGeometry.Stack.AlgebraicStacks.isGerbe_of_isFlat_and_isLocallyOfFinitePresentation_inertiaProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeOfFlatInertia.lean, line 175. The attribute's comment: “(2) implies (1): an algebraic stack whose inertia projection is flat and locally of finite presentation is a gerbe”.

An algebraic stack 𝒳 over S whose inertia projection I_𝒳 ⟶ 𝒳 is flat and locally of finite presentation is a gerbe: there are an algebraic space X and a 1-morphism 𝒳 ⟶ X making 𝒳 a gerbe over X.

theorem isGerbe_of_isFlat_and_isLocallyOfFinitePresentation_inertiaProjection
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (hflat : IsFlat B S hS (Stack.inertiaProjectionAlgebraicStacks B S hS 𝒳))
    (hlfp : IsLocallyOfFinitePresentation B S hS
      (Stack.inertiaProjectionAlgebraicStacks B S hS 𝒳)) :
    IsGerbe B S hS 𝒳

AlgebraicGeometry.Stack.isFlat_presentationStabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresentationStabilizerFlat.lean, line 91. The attribute's comment: “the implication (2) implies (1): flatness of the stabilizer of a presentation”.

If the inertia projection ℐ_𝒳 ⟶ 𝒳 of an algebraic stack 𝒳 over S is flat, then for every presentation [U/R] ⟶ 𝒳 the structure morphism G ⟶ U of the stabilizer group algebraic space of the presenting groupoid is a flat morphism of algebraic spaces.

theorem isFlat_presentationStabilizer
    (hflat : AlgebraicStacks.IsFlat B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳)) :
    Space.IsFlat B S hS (GroupoidInAlgebraicSpaces.stabilizer P.groupoid).hom

AlgebraicGeometry.Stack.isLocallyOfFinitePresentation_presentationStabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresentationStabilizerFlat.lean, line 106. The attribute's comment: “the implication (2) implies (1): local finite presentation of the stabilizer of a presentation”.

If the inertia projection ℐ_𝒳 ⟶ 𝒳 of an algebraic stack 𝒳 over S is locally of finite presentation, then for every presentation [U/R] ⟶ 𝒳 the structure morphism G ⟶ U of the stabilizer group algebraic space of the presenting groupoid is locally of finite presentation.

theorem isLocallyOfFinitePresentation_presentationStabilizer
    (hlfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS
      (inertiaProjectionAlgebraicStacks B S hS 𝒳)) :
    Space.IsLocallyOfFinitePresentation B S hS
      (GroupoidInAlgebraicSpaces.stabilizer P.groupoid).hom

Tag 0CPR, a lemma

Tag 0CPR in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isSurjective_and_isFlat_and_isLocallyOfFinitePresentation_relativeDiagonal_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeRelativeDiagonal.lean, line 120. The attribute's comment: “part (2): the relative diagonal is surjective, flat and locally of finite presentation”.

Stacks 0CPR, part (2). If a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S makes 𝒳 a gerbe over 𝒴, then its relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is surjective, flat and locally of finite presentation.

Surjectivity is Stacks 06P1 (2)(b) read at a field-valued point (AlgebraicGeometry.Stack.AlgebraicStacks.isSurjective_relativeDiagonal_of_isGerbeOver); flatness and local finite presentation hold because Δ_f is a section of the gerbe 𝒳 ×_𝒴 𝒳 ⟶ 𝒳 (isFlat_and_isLocallyOfFinitePresentation_relativeDiagonal).

theorem isSurjective_and_isFlat_and_isLocallyOfFinitePresentation_relativeDiagonal_of_isGerbeOver
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (hf : IsGerbeOver B S hS f) :
    Stack.IsSurjective B S hS (Stack.relativeDiagonalAlgebraicStacks B S hS f) ∧
      IsFlat B S hS (Stack.relativeDiagonalAlgebraicStacks B S hS f) ∧
      IsLocallyOfFinitePresentation B S hS (Stack.relativeDiagonalAlgebraicStacks B S hS f)

AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_and_isLocallyOfFinitePresentation_relativeInertiaProjection_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeRelativeDiagonal.lean, line 139. The attribute's comment: “part (1): the relative inertia is flat and locally of finite presentation over the source”.

Stacks 0CPR, part (1). If a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S makes 𝒳 a gerbe over 𝒴, then the forgetful 1-morphism I_{𝒳/𝒴} ⟶ 𝒳 of the relative inertia is flat and locally of finite presentation.

The relative inertia is equivalent over the site to 𝒳 ×_{Δ_f, 𝒳 ×_𝒴 𝒳, Δ_f} 𝒳 in such a way that the forgetful 1-morphism becomes the first projection (AlgebraicGeometry.Stack.AlgebraicStacks.relativeInertiaProjection_eq_comp_fst), which is a base change of Δ_f; so part (2) together with Stacks 06PY and Stacks 06Q4 gives the two properties for the projection, and they are unchanged by the comparison.

theorem isFlat_and_isLocallyOfFinitePresentation_relativeInertiaProjection_of_isGerbeOver
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (hf : IsGerbeOver B S hS f) :
    IsFlat B S hS (Stack.relativeInertiaProjection B S hS f) ∧
      IsLocallyOfFinitePresentation B S hS (Stack.relativeInertiaProjection B S hS f)

AlgebraicGeometry.Stack.AlgebraicStacks.isSurjective_and_isFlat_and_isLocallyOfFinitePresentation_comparison_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeRelativeDiagonal.lean, line 176. The attribute's comment: “part (3): the comparison of the two fibre products of a pair of algebraic spaces over the stacks is surjective, flat and locally of finite presentation”.

Stacks 0CPR, part (3). Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S making 𝒳 a gerbe over 𝒴, let T₁ and T₂ be algebraic spaces over S and let x_i : T_i ⟶ 𝒳 be 1-morphisms, with y_i = x_i ≫ f. Then the comparison 1-morphism
T₁ ×_{x₁, 𝒳, x₂} T₂ ⟶ T₁ ×_{y₁, 𝒴, y₂} T₂
is surjective, flat and locally of finite presentation.

By Stacks 04Z1 that comparison is a base change of the relative diagonal Δ_f, which has the three properties by part (2), and they base change by Stacks 04ZU, Stacks 06PY and Stacks 06Q4.

theorem isSurjective_and_isFlat_and_isLocallyOfFinitePresentation_comparison_of_isGerbeOver
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsGerbeOver B S hS f) (T₁ T₂ : AlgebraicSpaces B S hS)
    (x₁ : ofAlgebraicSpace.{u, w} B S hS T₁ ⟶ 𝒳)
    (x₂ : ofAlgebraicSpace.{u, w} B S hS T₂ ⟶ 𝒳) :
    Stack.IsSurjective B S hS (Stack.comparison B S hS x₁ x₂ f) ∧
      IsFlat B S hS (Stack.comparison B S hS x₁ x₂ f) ∧
      IsLocallyOfFinitePresentation B S hS (Stack.comparison B S hS x₁ x₂ f)

AlgebraicGeometry.Stack.AlgebraicStacks.isomMap_isSurjective_and_isFlat_and_isLocallyOfFinitePresentation_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeRelativeDiagonal.lean, line 222. The attribute's comment: “part (4): the morphism of isomorphism spaces is surjective, flat and locally of finite presentation”.

Stacks 0CPR, part (4). Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S making 𝒳 a gerbe over 𝒴, let T be an algebraic space over S and let x₁, x₂ : T ⟶ 𝒳 be 1-morphisms, with y_i = x_i ≫ f. Then the morphism
Isom_𝒳(x₁, x₂) ⟶ Isom_𝒴(y₁, y₂)
which applies f to an isomorphism x₁(t) ≅ x₂(t) is representable by algebraic spaces, and it is surjective, flat and locally of finite presentation: for every scheme U over S and every object of Isom_𝒴(y₁, y₂) over U, the morphism to U from the algebraic space representing the base change is surjective, flat and locally of finite presentation (Stacks 04XB).

As in the source, Isom_𝒳(x₁, x₂) ⟶ Isom_𝒴(y₁, y₂) is a base change of the comparison T ×_{x₁, 𝒳, x₂} T ⟶ T ×_{y₁, 𝒴, y₂} T of part (3) (AlgebraicGeometry.Stack.HigherDiagonal.isTwoFibreProduct_isomSquare), which is a base change of Δ_f (Stacks 050H). The relative diagonal is representable by algebraic spaces, so its three properties of part (2) are its relative properties in the sense of Stacks 04XB, by Stacks 04XI for surjectivity and by Stacks 06FM, the assertion for representable morphisms, for flatness and local finite presentation; and these pass along the two base changes.

theorem isomMap_isSurjective_and_isFlat_and_isLocallyOfFinitePresentation_of_isGerbeOver
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (hf : IsGerbeOver B S hS f)
    (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hT : IsAlgebraicSpace B S hS T)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS T hT ⟶ 𝒳) :
    IsRepresentableByAlgebraicSpaces B S hS (HigherDiagonal.isomMap B S hS f T hT x₁ x₂).hom ∧
    ∀ (U : BigFppfOver B S hS)
      (z : BigFppfOver B U.left.1 U.left.2 ⥤
        (HigherDiagonal.isomStack B S hS T hT (x₁ ≫ f) (x₂ ≫ f)).val.obj)
      (_hz : z ⋙ (HigherDiagonal.isomStack B S hS T hT (x₁ ≫ f) (x₂ ≫ f)).val.p =
        Over.map U.hom)
      (G : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
      (hG : IsAlgebraicSpace B U.left.1 U.left.2 G),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom)
            (HigherDiagonal.isomStack B S hS T hT x₁ x₂).val.p
            (HigherDiagonal.isomStack B S hS T hT (x₁ ≫ f) (x₂ ≫ f)).val.p z
            (CatFiberedInGroupoids.homFunctor (HigherDiagonal.isomMap B S hS f T hT x₁ x₂)))
          (presheafOfCategories (G ⋙ typeToCat)).p) →
        Space.IsSurjective B S hS (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨G, hG⟩)).hom ∧
          Space.IsFlat B S hS (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨G, hG⟩)).hom ∧
          Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨G, hG⟩)).hom

Tag 0CPS, a proposition

Tag 0CPS in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isGerbeOver_iff_isSurjective_isFlat_isLfp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeFlatDiagonalCharacterization.lean, line 195.

Stacks 0CPS. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. Then 𝒳 is a gerbe over 𝒴 if and only if f and its relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 are both surjective, flat and locally of finite presentation.

The implication from the gerbe condition is Stacks 06QI and Stacks 0CPR, part (2) (isSurjective_isFlat_isLfp_of_isGerbeOver); the converse reads both clauses of the gerbe condition off Stacks 06QA applied to f and to Δ_f (isGerbeOver_of_isSurjective_isFlat_isLfp).

theorem isGerbeOver_iff_isSurjective_isFlat_isLfp
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    IsGerbeOver B S hS f ↔
      (Stack.IsSurjective B S hS f ∧ IsFlat B S hS f ∧
          IsLocallyOfFinitePresentation B S hS f) ∧
        (Stack.IsSurjective B S hS (Stack.relativeDiagonalAlgebraicStacks B S hS f) ∧
          IsFlat B S hS (Stack.relativeDiagonalAlgebraicStacks B S hS f) ∧
          IsLocallyOfFinitePresentation B S hS
            (Stack.relativeDiagonalAlgebraicStacks B S hS f))

Tag 06QK, a lemma

Tag 06QK in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_gerbeOver_reducedLocallyNoetherianWithUniquePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ReducedSingletonStackGerbe.lean, line 109. The attribute's comment: “The field cover of Stacks 06MP (1) implies (2), the flatness and local finite presentation of the inertia and their fppf descent, Stacks 06QJ (2) implies (1), the gerbe 1-morphism being surjective, flat and locally of finite presentation by Stacks 06QI, and the conclusion about the base by Stacks 06MP (2) implies (1) applied to the composite from the field spectrum”.

Stacks 06QK. Let 𝒵 be a reduced, locally Noetherian algebraic stack over S whose space of points is a singleton. Then there is an algebraic stack Z over S which is representable by an algebraic space, a 1-morphism π : 𝒵 ⟶ Z making 𝒵 a gerbe over Z, and Z is again reduced, locally Noetherian with a single point.

theorem exists_gerbeOver_reducedLocallyNoetherianWithUniquePoint
    (𝒵 : Stack.AlgebraicStacks.{u, w} B S hS)
    (h𝒵 : Stack.IsReducedLocallyNoetherianWithUniquePoint B S hS 𝒵) :
    ∃ Z : Stack.AlgebraicStacks.{u, w} B S hS,
      IsRepresentableByAlgebraicSpace B S hS Z.val ∧
        (∃ π : 𝒵 ⟶ Z, IsGerbeOver B S hS π) ∧
          Stack.IsReducedLocallyNoetherianWithUniquePoint B S hS Z

AlgebraicGeometry.Stack.AlgebraicStacks.exists_gerbeOver_reducedLocallyNoetherianWithUniquePoint_unconditional, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ReducedSingletonStackGerbeUnconditional.lean, line 52. The attribute's comment: “unconditional. The field cover of Stacks 06MP (1) implies (2), the flatness and local finite presentation of the inertia and their fppf descent, Stacks 06QJ (2) implies (1) cited from GerbeOfFlatInertia, the gerbe 1-morphism being surjective, flat and locally of finite presentation by Stacks 06QI, and the conclusion about the base by Stacks 06MP (2) implies (1) applied to the composite from the field spectrum”.

Let 𝒵 be a reduced, locally Noetherian algebraic stack over S whose space of points is a singleton. Then there is an algebraic stack Z over S which is representable by an algebraic space, a 1-morphism π : 𝒵 ⟶ Z making 𝒵 a gerbe over Z, and Z is again reduced, locally Noetherian with a single point.

alias exists_gerbeOver_reducedLocallyNoetherianWithUniquePoint_unconditional

Tag 06R9, a lemma

Tag 06R9 in the Stacks Project.

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

Stacks 06R9. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S which exhibits 𝒳 as a gerbe over 𝒴 is a universal homeomorphism in the sense of Stacks 0CI7.

The gerbe condition base changes (Stacks 06QE), so each projection |𝒵 ×_𝒴 𝒳| → |𝒵| is a homeomorphism by AlgebraicGeometry.Stack.isHomeomorph_pointsMap_of_isGerbeOver.

theorem universalHomeomorphism_of_isGerbeOver {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsGerbeOver B S hS f) :
    UniversalHomeomorphism B S hS f

Tag 0DQL, a lemma

Tag 0DQL in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiCompactMorphism_diagonal_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiCompactDiagonalGerbe.lean, line 485.

Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S which makes 𝒳 a gerbe over 𝒴. If the diagonal of 𝒳 is quasi-compact, then so is the diagonal of 𝒴.

theorem isQuasiCompactMorphism_diagonal_of_isGerbeOver (f : 𝒳 ⟶ 𝒴)
    (hf : IsGerbeOver B S hS f)
    (hΔ : Stack.IsQuasiCompactMorphism B S hS (diagonal B S hS 𝒳)) :
    Stack.IsQuasiCompactMorphism B S hS (diagonal B S hS 𝒴)

Tag 06RA, a lemma

Tag 06RA in the Stacks Project.

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

Stacks 06RA. An algebraic stack over S which is a gerbe (Stacks 06QC) satisfies condition (1) of Stacks 06MT at every point of its space of points; that is, its residual gerbe exists at every point.

A gerbe comes with a 1-morphism f : 𝒳 ⟶ 𝒴 to an algebraic stack representable by an algebraic space which makes 𝒳 a gerbe over 𝒴. Condition (1) holds for 𝒴 at the image of the point by AlgebraicGeometry.Stack.hasSingletonPointMonomorphism_of_isRepresentableByAlgebraicSpace, and transports back along f by the existence clause of Stacks 0H24.

theorem hasSingletonPointMonomorphism_of_isGerbe
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : AlgebraicStacks.IsGerbe B S hS 𝒳)
    (x : points B S hS 𝒳.val.val (Classical.choose 𝒳.property)) :
    HasSingletonPointMonomorphism B S hS 𝒳 x

Sources

LeanAlgebraicGeometry.Stack.AlgebraicStacks.IsGerbeOver · AlgebraicGeometry.Stack.AlgebraicStacks.IsGerbe · AlgebraicGeometry.Stack.AlgebraicStacks.exists_algebraicSpace_isGerbeOver_isoClasses · AlgebraicGeometry.Stack.AlgebraicStacks.exists_isGerbeOver_isoClassSpace · AlgebraicGeometry.Stack.AlgebraicStacks.isGerbeOver_of_isTwoFibreProduct · CategoryTheory.IsGerbeOver.comp · AlgebraicGeometry.Stack.AlgebraicStacks.isGerbeOver_of_snd_of_isSurjective_isFlat_isLfp · AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_and_isLocallyOfFinitePresentation_section_of_isGerbeOver

Section101.29 Stratification by gerbes #

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

Tag 06RC, a proposition

Tag 06RC in the Stacks Project.

AlgebraicGeometry.Stack.exists_openSubstack_dense_isGerbe, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DenseOpenGerbe.lean, line 610.

Stacks 06RC. Let 𝒳 be a reduced algebraic stack over S whose inertia projection I_𝒳 ⟶ 𝒳 is quasi-compact. Then there is a dense open substack 𝒰 ⊆ 𝒳 which is a gerbe.

The proof is the source's. Choose a presentation [U/R] ⟶ 𝒳 whose chart U ⟶ 𝒳 is smooth and surjective (Stacks 04T3); U is reduced (Stacks 04YF) and the stabilizer G ⟶ U is the base change of I_𝒳 ⟶ 𝒳 (Stacks 06PR), hence of finite type (Stacks 050Q). Generic flatness (Stacks 06QS) gives a dense open W ⊆ U over which G is flat and locally of finite presentation. The image Ω of |W| in |𝒳| is open, W ⟶ 𝒳 being smooth, and dense; 𝒰 is the open substack with |𝒰| = Ω (Stacks 06FJ), through which W ⟶ 𝒳 factors by a smooth surjective 1-morphism. By Stacks 06R5 and Stacks 06PR the base change of I_𝒰 ⟶ 𝒰 along W ⟶ 𝒰 is G ×_U W ⟶ W, so I_𝒰 ⟶ 𝒰 is flat and locally of finite presentation, and 𝒰 is a gerbe by Stacks 06QJ.

theorem exists_openSubstack_dense_isGerbe (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hred : IsReducedStack B S hS 𝒳)
    (hqc : IsQuasiCompactMorphism.{u, w} B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳)) :
    ∃ W : OpenSubstack 𝒳, @Dense _ (pointTopology B S hS 𝒳.val) (W.pointSet B S hS) ∧
      AlgebraicStacks.IsGerbe B S hS
        (fullSubcategoryAlgebraicStack 𝒳 W.property W.isAlgebraic)

Tag 06RE, an example

Tag 06RE in the Stacks Project.

AlgebraicGeometry.PPowerWeighted.action, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExample.lean, line 89. The attribute's comment: “the weighted multiplicative-group action on Spec k[x_0, x_1, x_2, ...]”.

Stacks 06RE. The action of the multiplicative group scheme on U = Spec(k[x_0, x_1, x_2, …]) attached to the grading giving x_i the degree p^i, namely t · (x_0, x_1, x_2, …) = (t x_0, t^p x_1, t^{p^2} x_2, …).

noncomputable def action (k : Type u) [CommRing k] (p : ℕ) : GradedGmAction (grading k p)

AlgebraicGeometry.PPowerWeighted.action_μ_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExample.lean, line 95. The attribute's comment: “the coaction on the variables: x_i goes to x_i tensor T^{p^i}”.

Stacks 06RE. The coaction of the action sends the variable x_i to x_i ⊗ T^{p^i}: the group element t scales the coordinate x_i by t^{p^i}.

theorem action_μ_X (k : Type u) [CommRing k] (p i : ℕ) :
    (action k p).μ (MvPolynomial.X i) =
      (MvPolynomial.X i : MvPolynomial ℕ k) ⊗ₜ[ℤ] LaurentPolynomial.T ((p : ℤ) ^ i)

AlgebraicGeometry.PPowerWeighted.pointEval_action_μ_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 231. The attribute's comment: “the action on points is the one the coaction defines”.

Stacks 06RE. The action on points is the action the registered coaction defines: evaluating the coaction of x_i at a point φ of U and a unit t gives the i-th coordinate t^{p^i} φ(x_i) of t · φ. So smulPoint is the action of AlgebraicGeometry.PPowerWeighted.action and not a second one.

theorem pointEval_action_μ_X (k : Type u) [CommRing k] (p i : ℕ)
    (φ : MvPolynomial ℕ k →+* R) (t : Rˣ) :
    pointEval φ t ((action k p).μ (MvPolynomial.X i)) =
      smulPoint p t (fun j => φ (MvPolynomial.X j)) i

AlgebraicGeometry.PPowerWeighted.pointStabilizer_eq_rootsUnitsSubgroup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 287. The attribute's comment: “the stabilizer along the stratum X_i is mu_{p^i}”.

Stacks 06RE. On the i-th stratum the stabilizer of the weighted action is μ_{p^i}: a unit t fixes a point whose first nonvanishing coordinate is the i-th exactly when t^{p^i} = 1. The subgroup AlgebraicGeometry.rootsUnitsSubgroup n of the units is the value at R of the functor of points of the group scheme μ_n (AlgebraicGeometry.rootsOfUnitySections_representableBy_rootsOfUnity).

theorem pointStabilizer_eq_rootsUnitsSubgroup (p i : ℕ) (a : ℕ → R)
    (ha : IsPointInStratum i a) :
    pointStabilizer p a = rootsUnitsSubgroup (p ^ i)

AlgebraicGeometry.PPowerWeighted.pointStabilizer_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 314. The attribute's comment: “the stabilizer along the stratum X_infinity is G_m”.

Stacks 06RE. On the last stratum, where all the coordinates vanish, the stabilizer of the weighted action is all of G_m: the unit group of R is the value at R of the functor of points of the multiplicative group scheme (AlgebraicGeometry.unitsOfGlobalSections_representableBy_multiplicativeGroup).

theorem pointStabilizer_eq_top (p : ℕ) (a : ℕ → R) (ha : IsPointInStratumInf a) :
    pointStabilizer p a = ⊤

AlgebraicGeometry.PPowerWeighted.isPointInStratum_smulPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 321. The attribute's comment: “the stratum X_i is invariant under the action”.

Stacks 06RE. The i-th stratum is invariant under the action.

theorem isPointInStratum_smulPoint (p i : ℕ) (t : Rˣ) (a : ℕ → R) :
    IsPointInStratum i (smulPoint p t a) ↔ IsPointInStratum i a

AlgebraicGeometry.PPowerWeighted.isPointInStratumInf_smulPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 330. The attribute's comment: “the stratum X_infinity is invariant under the action”.

Stacks 06RE. The last stratum is invariant under the action.

theorem isPointInStratumInf_smulPoint (p : ℕ) (t : Rˣ) (a : ℕ → R) :
    IsPointInStratumInf (smulPoint p t a) ↔ IsPointInStratumInf a

AlgebraicGeometry.PPowerWeighted.isPointInStratumInf_or_exists_isPointInStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 350. The attribute's comment: “the strata cover: every point lies in exactly one stratum”.

Stacks 06RE. The strata cover U: a point with values in a field either has all its coordinates zero, or lies in the stratum indexed by the first index where it does not vanish.

theorem isPointInStratumInf_or_exists_isPointInStratum {K : Type*} [Field K] (a : ℕ → K) :
    IsPointInStratumInf a ∨ ∃ i, IsPointInStratum i a

AlgebraicGeometry.PPowerWeighted.isLocallyClosed_stratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 394. The attribute's comment: “the stratum X_i is locally closed”.

Stacks 06RE. The i-th stratum is locally closed: it is the intersection of the open where x_i is invertible with the closed subscheme where x_0, …, x_{i-1} vanish.

theorem isLocallyClosed_stratum (i : ℕ) : IsLocallyClosed (stratum k i)

AlgebraicGeometry.PPowerWeighted.isClosed_stratumInf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 401. The attribute's comment: “the stratum X_infinity is closed, hence locally closed”.

Stacks 06RE. The last stratum is closed, being the vanishing locus of all the coordinates.

theorem isClosed_stratumInf : IsClosed (stratumInf k)

AlgebraicGeometry.PPowerWeighted.iUnion_stratum_union_stratumInf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 419. The attribute's comment: “the strata cover the space”.

Stacks 06RE. The strata cover U: a point of the spectrum either kills all the coordinates, or lies in the stratum indexed by the first coordinate it does not kill.

theorem iUnion_stratum_union_stratumInf :
    (⋃ i, stratum k i) ∪ stratumInf k = Set.univ

AlgebraicGeometry.PPowerWeighted.mem_stratum_ker_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 431. The attribute's comment: “the strata on points and on the spectrum are the same”.

Stacks 06RE. The two readings of the i-th stratum agree: a point of U with values in a field lies in the i-th stratum in the sense of IsPointInStratum exactly when the prime it defines lies in stratum.

theorem mem_stratum_ker_iff {K : Type*} [Field K] (φ : MvPolynomial ℕ k →+* K) (i : ℕ) :
    (⟨RingHom.ker φ, RingHom.ker_isPrime φ⟩ : PrimeSpectrum (MvPolynomial ℕ k)) ∈
        stratum k i ↔
      IsPointInStratum i (fun j => φ (MvPolynomial.X j))

AlgebraicGeometry.PPowerWeighted.mem_stratumInf_ker_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 440. The attribute's comment: “the last stratum on points and on the spectrum is the same”.

Stacks 06RE. The two readings of the last stratum agree.

theorem mem_stratumInf_ker_iff {K : Type*} [Field K] (φ : MvPolynomial ℕ k →+* K) :
    (⟨RingHom.ker φ, RingHom.ker_isPrime φ⟩ : PrimeSpectrum (MvPolynomial ℕ k)) ∈
        stratumInf k ↔
      IsPointInStratumInf (fun j => φ (MvPolynomial.X j))

AlgebraicGeometry.PPowerWeighted.isDomain_stratumRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 516. The attribute's comment: “the stratum X_i is reduced, being integral”.

Stacks 06RE. The i-th stratum is integral, in particular reduced.

theorem isDomain_stratumRing [IsDomain k] (i : ℕ) : IsDomain (stratumRing k i)

AlgebraicGeometry.PPowerWeighted.isReduced_stratumRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 525. The attribute's comment: “the stratum X_i is reduced”.

Stacks 06RE. The i-th stratum is reduced.

theorem isReduced_stratumRing [IsDomain k] (i : ℕ) : IsReduced (stratumRing k i)

AlgebraicGeometry.PPowerWeighted.isDomain_quotient_coordinateIdeal_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 532. The attribute's comment: “the stratum X_infinity is reduced”.

Stacks 06RE. The last stratum is reduced: it is the origin, cut out by the prime ideal generated by all the coordinates.

theorem isDomain_quotient_coordinateIdeal_univ [IsDomain k] :
    IsDomain (MvPolynomial ℕ k ⧸ coordinateIdeal k Set.univ)

AlgebraicGeometry.PPowerWeighted.rootsUnitsSubgroup_pow_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 578. The attribute's comment: “distinct strata have distinct groups mu_{p^i}: no coarser stratification”.

Stacks 06RE. Distinct strata have distinct groups: for 1 < p and i < j the group μ_{p^i} of the stratum X_i is not the group μ_{p^j} of the stratum X_j. So no two strata can be merged into a single locus along which the stabilizer is one group, which is why there is no coarser stratification with the same properties.

theorem rootsUnitsSubgroup_pow_ne (p i j : ℕ) (hp : 1 < p) (hij : i < j) :
    rootsUnitsSubgroup (A := rootsOfUnityCoordinateRing.{u} (p ^ j)) (p ^ i) ≠
      rootsUnitsSubgroup (p ^ j)

AlgebraicGeometry.PPowerWeighted.rootsUnitsSubgroup_ne_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 587. The attribute's comment: “the group mu_{p^i} of X_i differs from the group G_m of X_infinity”.

Stacks 06RE. The group of a stratum X_i is never the group G_m of the last stratum X_∞: already in the units of the rationals the n-th roots of unity are not everything, since 2 is a unit with 2^n ≠ 1. So the last stratum cannot be merged with any other one either.

theorem rootsUnitsSubgroup_ne_top {n : ℕ} (hn : 0 < n) :
    rootsUnitsSubgroup (A := ℚ) n ≠ ⊤

AlgebraicGeometry.PPowerWeighted.pointStabilizer_ne_pointStabilizer_basisPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 621. The attribute's comment: “the strata X_i and X_j cannot be merged: their stabilizers differ”.

Stacks 06RE. The strata X_i and X_j with i < j cannot be merged: already over the coordinate ring of μ_{p^j} the stabilizer of a point of X_i differs from the stabilizer of a point of X_j, being μ_{p^i} against μ_{p^j}. Together with AlgebraicGeometry.PPowerWeighted.pointStabilizer_ne_pointStabilizer_basisPoint_zero this is the source's last assertion, that there is no coarser stratification with the same properties: a stratum of a coarser stratification would contain points of two of the strata below and so could not be a gerbe with a single group.

theorem pointStabilizer_ne_pointStabilizer_basisPoint (p i j : ℕ) (hp : 1 < p) (hij : i < j) :
    pointStabilizer p (basisPoint (rootsOfUnityCoordinateRing.{u} (p ^ j)) i) ≠
      pointStabilizer p (basisPoint (rootsOfUnityCoordinateRing.{u} (p ^ j)) j)

AlgebraicGeometry.PPowerWeighted.pointStabilizer_ne_pointStabilizer_basisPoint_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationExamplePoints.lean, line 632. The attribute's comment: “the stratum X_i cannot be merged with X_infinity: their stabilizers differ”.

Stacks 06RE. The stratum X_i cannot be merged with the last stratum X_∞: already over the rationals the stabilizer of the point of X_i with i-th coordinate one is μ_{p^i}, while the stabilizer of the origin is all of G_m.

theorem pointStabilizer_ne_pointStabilizer_basisPoint_zero (p i : ℕ) (hp : 0 < p) :
    pointStabilizer p (basisPoint ℚ i) ≠ pointStabilizer p (0 : ℕ → ℚ)

AlgebraicGeometry.PPowerWeighted.quotientStack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationQuotientStack.lean, line 83. The attribute's comment: “the quotient stack [U/G_m]”.

Stacks 06RE. The quotient stack [U/𝐆_m] of the multiplicative-group action on U = Spec(k[x_0, x_1, x_2, …]) in which x_i has weight p^i. It is the quotient stack of Stacks 044Q, part (2), for that action, read at the terminal algebraic space of the big fppf site over Spec ℤ. The hypothesis is that the site contain U.

noncomputable def quotientStack (hU : 𝒞.Contains (Spec (.of (MvPolynomial ℕ k)))) :
    BasedCategory
      (BigFppfOver 𝒞 (Spec (.of (ULift.{u} ℤ))) (Space.contains_specULiftZ 𝒞))

AlgebraicGeometry.PPowerWeighted.isAlgebraicStack_quotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationQuotientStack.lean, line 99. The attribute's comment: “the quotient stack [U/G_m] is an algebraic stack”.

Stacks 06RE. The quotient stack [U/𝐆_m] is an algebraic stack over Spec ℤ. This is Stacks 04TK for the action: the structure morphism of the group algebraic space B ×_{Spec ℤ} 𝐆_m ⟶ B is smooth because the Laurent polynomial ring is a smooth algebra, and 04TK carries nothing beyond that smoothness.

theorem isAlgebraicStack_quotientStack
    (hU : 𝒞.Contains (Spec (.of (MvPolynomial ℕ k)))) :
    Stack.IsAlgebraicStack.{u, w} 𝒞 (Spec (.of (ULift.{u} ℤ)))
      (Space.contains_specULiftZ 𝒞) (quotientStack 𝒞 k p hU)

AlgebraicGeometry.PPowerWeighted.weightedQuotientStack_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationStatement.lean, line 78. The attribute's comment: “X = [U/G_m] is an algebraic stack: the object of the 2-category of algebraic stacks presented by the action groupoid”.

Stacks 06RE, assertion (1): 𝒳 = [U/𝐆_m] is an algebraic stack. The algebraic stack weightedQuotientStack is presented, in the sense of Stacks 04TI, by the action groupoid of 𝐆_m on U, whose quotient stack is the [U/𝐆_m] of quotientStack.

theorem weightedQuotientStack_presentation :
    ∃ P : Stack.GroupoidPresentation 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
        (weightedQuotientStack.{u, w} 𝒞 k p hU).val.val,
      Stack.quotientStack P.groupoid = quotientStack 𝒞 k p hU

AlgebraicGeometry.PPowerWeighted.stratumProperty_chart_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationStatement.lean, line 92. The attribute's comment: “the strata X_i (x_0 = ... = x_{i-1} = 0, x_i invertible) and X_infinity (all x_j = 0)”.

Stacks 06RE, assertion (2), the strata: the stratum of index i is the locus where x_0, …, x_{i-1} vanish and x_i does not, and the stratum of index ∞ the locus where all x_j vanish. Precisely, a point h : W ⟶ U with values in any scheme W of the site lands in 𝒳_i if and only if x_0, …, x_{i-1} pull back to 0 and x_i to a unit of Γ(W, 𝒪_W), and in 𝒳_∞ if and only if every x_j pulls back to 0.

theorem stratumProperty_chart_iff {W : BigFppfOver 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)}
    (h : W ⟶ totalSiteObject 𝒞 k hU) :
    (∀ i : ℕ, stratumProperty.{u, w} 𝒞 k p hU i (chartObj.{u, w} p h) ↔
      (∀ j < i, coord h j = 0) ∧ IsUnit (coord h i)) ∧
    (stratumProperty.{u, w} 𝒞 k p hU ⊤ (chartObj.{u, w} p h) ↔ ∀ j, coord h j = 0)

AlgebraicGeometry.PPowerWeighted.isAlgebraicStack_stratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationStatement.lean, line 108. The attribute's comment: “each stratum is an algebraic stack (locally closed substack)”.

Stacks 06RE: each stratum is an algebraic stack. The full subcategory of 𝒳 on the objects of the stratum 𝒳_a is an algebraic stack, being a locally closed substack of 𝒳: this is the algebraicity component of isLocallyClosedSubstack_stratumProperty. It is the algebraic stack structure on 𝒳_a that assertions (2), (3) and (4) below are stated for.

theorem isAlgebraicStack_stratum (a : WithTop ℕ) :
    Stack.IsAlgebraicStack.{u, w} 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
      (Stack.fullSubcategoryBased (weightedQuotientStack.{u, w} 𝒞 k p hU)
        (stratumProperty.{u, w} 𝒞 k p hU a))

AlgebraicGeometry.PPowerWeighted.exists_stratification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationStatement.lean, line 122. The attribute's comment: “the strata form a stratification of |X|”.

Stacks 06RE, assertion (2), the stratification: the point sets |𝒳_a| of the strata form a stratification of |𝒳| (Stacks 09Y1) indexed by ℕ ∪ {∞} with the reverse order: they are pairwise disjoint, cover |𝒳|, and the closure of |𝒳_i| lies in |𝒳_i| ∪ |𝒳_{i+1}| ∪ ⋯ ∪ |𝒳_∞|.

theorem exists_stratification :
    letI := Stack.pointTopology 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
      (weightedQuotientStack.{u, w} 𝒞 k p hU).val
    ∃ σ : Stratification (Stack.AlgebraicStacks.points 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
        (weightedQuotientStack.{u, w} 𝒞 k p hU)) (WithTop ℕ)ᵒᵈ,
      ∀ a : WithTop ℕ,
        σ.strata (OrderDual.toDual a) =
          Set.range (Stack.AlgebraicStacks.pointsMap 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
            (Stack.fullSubcategoryInclusion (weightedQuotientStack.{u, w} 𝒞 k p hU)
              (stratumProperty.{u, w} 𝒞 k p hU a)
              (isAlgebraicStack_stratum.{u, w} 𝒞 k p hU a)))

AlgebraicGeometry.PPowerWeighted.isReduced_isLocallyClosedSubstack_stratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationStatement.lean, line 141. The attribute's comment: “the strata are reduced locally closed substacks”.

Stacks 06RE, assertion (4): every stratum is a reduced locally closed substack of 𝒳.

theorem isReduced_isLocallyClosedSubstack_stratum (a : WithTop ℕ) :
    Stack.IsLocallyClosedSubstack (weightedQuotientStack.{u, w} 𝒞 k p hU)
        (stratumProperty.{u, w} 𝒞 k p hU a) ∧
      Stack.IsReducedStack 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
        (Stack.fullSubcategoryAlgebraicStack (weightedQuotientStack.{u, w} 𝒞 k p hU)
          (stratumProperty.{u, w} 𝒞 k p hU a) (isAlgebraicStack_stratum.{u, w} 𝒞 k p hU a))

AlgebraicGeometry.PPowerWeighted.isGerbeOverSchemeWithGroup_algebraicStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationStatement.lean, line 155. The attribute's comment: “each stratum is a gerbe over a scheme with group mu_{p^i} for X_i and G_m for X_infinity”.

Stacks 06RE, assertion (3): each stratum is a gerbe over a scheme, with group μ_{p^i} for 𝒳_i and 𝐆_m for 𝒳_∞.

theorem isGerbeOverSchemeWithGroup_algebraicStratum (a : WithTop ℕ) :
    haveI : NeZero p := ⟨hp.out.ne_zero⟩
    Stack.AlgebraicStacks.IsGerbeOverSchemeWithGroup 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
      (Stack.fullSubcategoryAlgebraicStack (weightedQuotientStack.{u, w} 𝒞 k p hU)
        (stratumProperty.{u, w} 𝒞 k p hU a) (isAlgebraicStack_stratum.{u, w} 𝒞 k p hU a))
      (stratumGroup.{u} p a)

AlgebraicGeometry.PPowerWeighted.stratification_minimal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratificationStatement.lean, line 169. The attribute's comment: “there is no coarser stratification by reduced locally closed gerbes over schemes”.

Stacks 06RE, assertion (5): there is no coarser stratification with the same properties. If a topological partition of |𝒳| (Stacks 09XZ) consists of the point sets of reduced locally closed substacks of 𝒳 each of which is a gerbe over a scheme, and the strata |𝒳_a| refine it, then it is the partition by the strata.

theorem stratification_minimal :
    letI := Stack.pointTopology 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
      (weightedQuotientStack.{u, w} 𝒞 k p hU).val
    ∀ Qs : Set (Set (Stack.AlgebraicStacks.points 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
        (weightedQuotientStack.{u, w} 𝒞 k p hU))),
      IsTopologicalPartition Qs →
      (∀ s ∈ Qs, ∃ (W : ObjectProperty (weightedQuotientStack.{u, w} 𝒞 k p hU).val.val.obj)
          (_ : Stack.IsLocallyClosedSubstack (weightedQuotientStack.{u, w} 𝒞 k p hU) W),
        (∀ hA, Stack.IsReducedStack 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
            (Stack.fullSubcategoryAlgebraicStack (weightedQuotientStack.{u, w} 𝒞 k p hU) W hA) ∧
          Stack.AlgebraicStacks.IsGerbeOverScheme 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
            (Stack.fullSubcategoryAlgebraicStack (weightedQuotientStack.{u, w} 𝒞 k p hU) W hA)) ∧
        ∀ hA, Set.range (Stack.AlgebraicStacks.pointsMap 𝒞 𝒵 (Space.contains_specULiftZ 𝒞)
          (Stack.fullSubcategoryInclusion (weightedQuotientStack.{u, w} 𝒞 k p hU) W hA)) = s) →
      local_Refines (Set.range (stratumPoints.{u, w} 𝒞 k p hU)) Qs →
      Qs = Set.range (stratumPoints.{u, w} 𝒞 k p hU)

Tag 06RF, a lemma

Tag 06RF in the Stacks Project.

AlgebraicGeometry.Stack.exists_gerbe_stratification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratification.lean, line 565. The attribute's comment: “existence of the stratification, arranged as in (a), with strata as large as possible, and as in (b)”.

Stacks 06RF, the stratifications (a) and (b). Let 𝒳 be an algebraic stack over S whose inertia projection I_𝒳 ⟶ 𝒳 is quasi-compact. Then there are a well-ordered index set I and for every i ∈ I a reduced locally closed substack 𝒰ᵢ ⊆ 𝒳 such that

each 𝒰ᵢ is a gerbe,

|𝒳| = ⋃ᵢ |𝒰ᵢ|,

Tᵢ = |𝒳| \ ⋃_{i' < i} |𝒰ᵢ'| is closed in |𝒳|, and

|𝒰ᵢ| is open in Tᵢ,

and this can be arranged so that (a) |𝒰ᵢ| is dense in Tᵢ for every i, with 𝒰ᵢ chosen as large as possible: |𝒰ᵢ| is the set of points of Tᵢ lying in an open substack, which is a gerbe, of the reduced closed substack with points Tᵢ (maximalGerbePointSet); and also so that (b) every 𝒰ᵢ is quasi-compact. Here |𝒰ᵢ| is the image of the points of 𝒰ᵢ in |𝒳|. The stratification of case (a) is canonical: exists_gerbe_stratification_unique.

theorem exists_gerbe_stratification
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hqc : IsQuasiCompactMorphism.{u, w} B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳)) :
    (∃ (I : Type (u + 2)) (_ : LinearOrder I) (_ : WellFoundedLT I)
      (Q : I → ObjectProperty 𝒳.val.val.obj)
      (hQ : ∀ i, IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 (Q i))),
      (∀ i, IsLocallyClosedSubstack 𝒳 (Q i) ∧
        IsReducedStack B S hS (fullSubcategoryAlgebraicStack 𝒳 (Q i) (hQ i)) ∧
        AlgebraicStacks.IsGerbe B S hS (fullSubcategoryAlgebraicStack 𝒳 (Q i) (hQ i))) ∧
      (⋃ i, Set.range (AlgebraicStacks.pointsMap B S hS
        (fullSubcategoryInclusion 𝒳 (Q i) (hQ i)))) = Set.univ ∧
      (∀ i, @IsClosed _ (pointTopology B S hS 𝒳.val) (Set.univ \ ⋃ (j : I) (_ : j < i),
        Set.range (AlgebraicStacks.pointsMap B S hS (fullSubcategoryInclusion 𝒳 (Q j) (hQ j))))) ∧
      (∀ i, ∃ O, @IsOpen _ (pointTopology B S hS 𝒳.val) O ∧
        Set.range (AlgebraicStacks.pointsMap B S hS (fullSubcategoryInclusion 𝒳 (Q i) (hQ i))) =
          (Set.univ \ ⋃ (j : I) (_ : j < i), Set.range (AlgebraicStacks.pointsMap B S hS
            (fullSubcategoryInclusion 𝒳 (Q j) (hQ j)))) ∩ O) ∧
      (∀ i, (Set.univ \ ⋃ (j : I) (_ : j < i), Set.range (AlgebraicStacks.pointsMap B S hS
          (fullSubcategoryInclusion 𝒳 (Q j) (hQ j)))) ⊆
        @closure _ (pointTopology B S hS 𝒳.val) (Set.range (AlgebraicStacks.pointsMap B S hS
          (fullSubcategoryInclusion 𝒳 (Q i) (hQ i)))) ∧
        Set.range (AlgebraicStacks.pointsMap B S hS (fullSubcategoryInclusion 𝒳 (Q i) (hQ i))) =
          maximalGerbePointSet B S hS 𝒳 (Set.univ \ ⋃ (j : I) (_ : j < i),
            Set.range (AlgebraicStacks.pointsMap B S hS
              (fullSubcategoryInclusion 𝒳 (Q j) (hQ j)))))) ∧
    (∃ (I : Type (u + 2)) (_ : LinearOrder I) (_ : WellFoundedLT I)
      (Q : I → ObjectProperty 𝒳.val.val.obj)
      (hQ : ∀ i, IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased 𝒳 (Q i))),
      (∀ i, IsLocallyClosedSubstack 𝒳 (Q i) ∧
        IsReducedStack B S hS (fullSubcategoryAlgebraicStack 𝒳 (Q i) (hQ i)) ∧
        AlgebraicStacks.IsGerbe B S hS (fullSubcategoryAlgebraicStack 𝒳 (Q i) (hQ i))) ∧
      (⋃ i, Set.range (AlgebraicStacks.pointsMap B S hS
        (fullSubcategoryInclusion 𝒳 (Q i) (hQ i)))) = Set.univ ∧
      (∀ i, @IsClosed _ (pointTopology B S hS 𝒳.val) (Set.univ \ ⋃ (j : I) (_ : j < i),
        Set.range (AlgebraicStacks.pointsMap B S hS (fullSubcategoryInclusion 𝒳 (Q j) (hQ j))))) ∧
      (∀ i, ∃ O, @IsOpen _ (pointTopology B S hS 𝒳.val) O ∧
        Set.range (AlgebraicStacks.pointsMap B S hS (fullSubcategoryInclusion 𝒳 (Q i) (hQ i))) =
          (Set.univ \ ⋃ (j : I) (_ : j < i), Set.range (AlgebraicStacks.pointsMap B S hS
            (fullSubcategoryInclusion 𝒳 (Q j) (hQ j)))) ∩ O) ∧
      (∀ i, IsQuasiCompactStack.{u, w} B S hS (fullSubcategoryAlgebraicStack 𝒳 (Q i) (hQ i)).val
        (fullSubcategoryAlgebraicStack 𝒳 (Q i) (hQ i)).property))

AlgebraicGeometry.Stack.exists_gerbe_stratification_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeStratification.lean, line 630. The attribute's comment: “canonicity of the stratification (a) with strata as large as possible”.

Stacks 06RF, the canonical stratification (a). A stratification of |𝒳| as in Stacks 06RF whose strata are chosen as large as possible is unique: if two well-ordered families of nonempty sets of points Wᵢ cover |𝒳| and each Wᵢ is the largest gerbe (maximalGerbePointSet) in Tᵢ = |𝒳| \ ⋃_{j < i} Wⱼ, then the index sets are order-isomorphic with the same sets.

theorem exists_gerbe_stratification_unique (𝒳 : AlgebraicStacks.{u, w} B S hS)
    {I : Type*} [LinearOrder I] [WellFoundedLT I] (W : I → Set (AlgebraicStacks.points B S hS 𝒳))
    (hW : ∀ i, W i = maximalGerbePointSet B S hS 𝒳 (Set.univ \ ⋃ (j : I) (_ : j < i), W j))
    (hWne : ∀ i, (W i).Nonempty) (hWcov : (⋃ i, W i) = Set.univ)
    {I' : Type*} [LinearOrder I'] [WellFoundedLT I']
    (W' : I' → Set (AlgebraicStacks.points B S hS 𝒳))
    (hW' : ∀ i, W' i = maximalGerbePointSet B S hS 𝒳 (Set.univ \ ⋃ (j : I') (_ : j < i), W' j))
    (hW'ne : ∀ i, (W' i).Nonempty) (hW'cov : (⋃ i, W' i) = Set.univ) :
    ∃ e : I ≃o I', ∀ i, W' (e i) = W i

Tag 06RG, a remark

Tag 06RG in the Stacks Project.

AlgebraicGeometry.Stack.CanonicalGerbeStratificationIndexCountable, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/CanonicalGerbeStratification.lean, line 178. The attribute's comment: “the open question of the remark, stated as a proposition; neither it nor its negation is proved”.

The question of Stacks 06RG. For every algebraic stack 𝒳 over a scheme S whose inertia projection I_𝒳 ⟶ 𝒳 is quasi-compact (the setting of Stacks 06RF), the well-ordered index set I of the canonical stratification of type (a) (canonicalGerbeStratificationIndex) has cardinality at most ℵ₀.

This is the "natural guess" of the remark Stacks 06RG about the order type of the canonical stratifications. The Stacks project does not know whether it is true or false; it is stated here as a proposition, and neither it nor its negation is proved. By canonicalGerbeStratificationIndexCountable_iff it says equally that every stratification of type (a) with strata as large as possible has a countable index set.

def CanonicalGerbeStratificationIndexCountable : Prop

Sources

LeanAlgebraicGeometry.Stack.exists_openSubstack_dense_isGerbe · AlgebraicGeometry.PPowerWeighted.action · AlgebraicGeometry.PPowerWeighted.action_μ_X · AlgebraicGeometry.PPowerWeighted.pointEval_action_μ_X · AlgebraicGeometry.PPowerWeighted.pointStabilizer_eq_rootsUnitsSubgroup · AlgebraicGeometry.PPowerWeighted.pointStabilizer_eq_top · AlgebraicGeometry.PPowerWeighted.isPointInStratum_smulPoint · AlgebraicGeometry.PPowerWeighted.isPointInStratumInf_smulPoint

Section101.30 The topological space of an algebraic stack #

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

Tag 0DQN, a lemma

Tag 0DQN in the Stacks Project.

AlgebraicGeometry.Stack.spectralSpace_points_of_isQuasiCompact_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpectralPointsAlgebraicStack.lean, line 248.

Stacks 0DQN. Let 𝒳 be a quasi-compact algebraic stack over S whose absolute diagonal Δ : 𝒳 ⟶ 𝒳 ×_{Spec ℤ} 𝒳 is quasi-compact. Then the topological space of points |𝒳| is spectral.

The absolute diagonal is read as in Stacks 050D: the relative diagonal of the structure morphism of 𝒳 viewed over the terminal scheme Spec ℤ, quasi-compact in the sense of Stacks 050U.

theorem spectralSpace_points_of_isQuasiCompact_diagonal (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (hΔ : IsQuasiCompactMorphism.{u, w} B (⊤_ Scheme.{u}) B.contains_terminal
      (relativeDiagonalAlgebraicStacks B (⊤_ Scheme.{u}) B.contains_terminal
        (structureMorphism B (⊤_ Scheme.{u}) B.contains_terminal
          (AlgebraicStacks.viewOverIntegers B S hS B.contains_terminal 𝒳)))) :
    SpectralSpace (points B S hS 𝒳.val.val 𝒳.val.property)

Tag 0DQP, a lemma

Tag 0DQP in the Stacks Project.

AlgebraicGeometry.Stack.spectralSpace_points_of_isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpectralPointsAlgebraicStack.lean, line 277.

Stacks 0DQP. The topological space of points |𝒳| of a quasi-compact and quasi-separated algebraic stack 𝒳 over S is spectral.

Quasi-separatedness is absolute quasi-separatedness, part (8) of Stacks 050D; its first half is quasi-compactness of the absolute diagonal (Stacks 04Z0, part (2)), so this is the special case of Stacks 0DQN.

theorem spectralSpace_points_of_isAbsolutelyQuasiSeparated (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hqc : IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property)
    (hqs : AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS B.contains_terminal 𝒳) :
    SpectralSpace (points B S hS 𝒳.val.val 𝒳.val.property)

Tag 0DQQ, a lemma

Tag 0DQQ in the Stacks Project.

AlgebraicGeometry.Stack.exists_spectralSpace_cover_and_stacksSober, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SpectralPointsAlgebraicStack.lean, line 351.

Stacks 0DQQ. Let 𝒳 be an algebraic stack over S whose absolute diagonal Δ : 𝒳 ⟶ 𝒳 ×_{Spec ℤ} 𝒳 is quasi-compact. Then |𝒳| has an open covering by spectral subspaces, and in particular |𝒳| is sober.

The covering is by the images of the affine opens of a smooth surjective chart by a scheme. The absolute diagonal is read as in Stacks 050D, as in AlgebraicGeometry.Stack.spectralSpace_points_of_isQuasiCompact_diagonal.

theorem exists_spectralSpace_cover_and_stacksSober (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hΔ : IsQuasiCompactMorphism.{u, w} B (⊤_ Scheme.{u}) B.contains_terminal
      (relativeDiagonalAlgebraicStacks B (⊤_ Scheme.{u}) B.contains_terminal
        (structureMorphism B (⊤_ Scheme.{u}) B.contains_terminal
          (AlgebraicStacks.viewOverIntegers B S hS B.contains_terminal 𝒳)))) :
    (∃ 𝒰 : Set (Set (points B S hS 𝒳.val.val 𝒳.val.property)),
      (∀ W ∈ 𝒰, IsOpen W ∧ SpectralSpace W) ∧ ⋃₀ 𝒰 = Set.univ) ∧
      StacksSober (points B S hS 𝒳.val.val 𝒳.val.property)

Sources

LeanAlgebraicGeometry.Stack.spectralSpace_points_of_isQuasiCompact_diagonal · AlgebraicGeometry.Stack.spectralSpace_points_of_isAbsolutelyQuasiSeparated · AlgebraicGeometry.Stack.exists_spectralSpace_cover_and_stacksSober

Section101.31 Existence of residual gerbes #

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

Tag 06RD, a lemma

Tag 06RD in the Stacks Project.

AlgebraicGeometry.Stack.hasReducedSingletonPointMonomorphism_of_isQuasiCompact_inertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ResidualGerbeQuasiCompactInertia.lean, line 78.

Let 𝒳 be an algebraic stack over S whose inertia projection I_𝒳 ⟶ 𝒳 is quasi-compact. Then the residual gerbe of 𝒳 exists at every point x of |𝒳|, in the sense of Stacks 06MU (1), condition (2) of Stacks 06MT: there is a reduced algebraic stack 𝒵 with a monomorphism 𝒵 ⟶ 𝒳 whose space of points is a single point lying over x.

theorem hasReducedSingletonPointMonomorphism_of_isQuasiCompact_inertia
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hqc : IsQuasiCompactMorphism.{u, w} B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳))
    (x : points B S hS 𝒳.val.val (Classical.choose 𝒳.property)) :
    HasReducedSingletonPointMonomorphism B S hS 𝒳 x

Tag 06UI, a lemma

Tag 06UI in the Stacks Project.

AlgebraicGeometry.Stack.exists_isResidualGerbeAt_of_isAbsolutelyQuasiDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ResidualGerbeQuasiDMExistence.lean, line 68. The attribute's comment: “the residual gerbe of a quasi-DM algebraic stack exists at every point of its space, in the sense of 06MU: some strictly full subcategory meets the 06MT specification IsResidualGerbeAt, i.e. is a reduced locally Noetherian algebraic substack with one point lying over x. Nothing is left open: the source's chart comes from 06MF proved outright (hasQuasiDMPresentation_of_isAbsolutelyQuasiDM) and its 06S1 step from isLocallyQuasiFinite_comp_of_mono_to_field”.

Stacks 06UI. Let 𝒳 be a quasi-DM algebraic stack over S. Then the residual gerbe of 𝒳 at x exists for every x ∈ |𝒳|: some strictly full subcategory P of 𝒳 meets the specification AlgebraicGeometry.Stack.IsResidualGerbeAt of Stacks 06MT, which by Stacks 06MU is what it means for the residual gerbe at x to exist.

This is AlgebraicGeometry.Stack.exists_isResidualGerbeAt_of_isAbsolutelyQuasiDM_of_hasQuasiDMPresentation — the source's proof, with Stacks 06S1 already supplied — applied to the substantial direction of Stacks 06MF, AlgebraicGeometry.Stack.hasQuasiDMPresentation_of_isAbsolutelyQuasiDM.

theorem exists_isResidualGerbeAt_of_isAbsolutelyQuasiDM
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : AlgebraicStacks.IsAbsolutelyQuasiDM B S hS hZ 𝒳)
    (x : AlgebraicStacks.points B S hS 𝒳) :
    ∃ P : ObjectProperty 𝒳.val.val.obj, IsResidualGerbeAt B S hS 𝒳 x P

Tag 0H22, a lemma

Tag 0H22 in the Stacks Project.

AlgebraicGeometry.Stack.exists_isResidualGerbeAt_of_isLocallyNoetherianStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ResidualGerbeLocallyNoetherian.lean, line 175.

Stacks 0H22. Let 𝒳 be a locally Noetherian algebraic stack. Then the residual gerbe of 𝒳 at x exists for every x ∈ |𝒳|: some strictly full subcategory of 𝒳 meets the specification AlgebraicGeometry.Stack.IsResidualGerbeAt of Stacks 06MT at x.

See the module documentation for the argument.

theorem exists_isResidualGerbeAt_of_isLocallyNoetherianStack (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsLocallyNoetherianStack B S hS 𝒳) (x : AlgebraicStacks.points B S hS 𝒳) :
    ∃ P : ObjectProperty 𝒳.val.val.obj, IsResidualGerbeAt B S hS 𝒳 x P

Sources

LeanAlgebraicGeometry.Stack.hasReducedSingletonPointMonomorphism_of_isQuasiCompact_inertia · AlgebraicGeometry.Stack.exists_isResidualGerbeAt_of_isAbsolutelyQuasiDM · AlgebraicGeometry.Stack.exists_isResidualGerbeAt_of_isLocallyNoetherianStack

Section101.32 Étale local structure #

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

Tag 0DU1, a lemma

Tag 0DU1 in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_quotientSheaf_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/OpenRelationEtaleQuotient.lean, line 429. The attribute's comment: “algebraicity of the quotient U/R”.

Stacks 0DU1, algebraicity of the quotient. Let (U, R, s, t, c) be a groupoid in algebraic spaces over an algebraic space Y whose object space is flat and locally of finite presentation over Y and whose pre-relation (t, s) : R ⟶ U ×_Y U is an open immersion. Then the quotient sheaf U/R of Stacks 044J is an algebraic space over S.

The pre-relation is an equivalence relation and s and t are flat and locally of finite presentation, so Stacks 04S6, condition (1), applies.

theorem isAlgebraicSpace_quotientSheaf_of_isOpenImmersion
    (hflat : IsFlat C S hS G.objectsToBase.hom)
    (hlfp : IsLocallyOfFinitePresentation C S hS G.objectsToBase.hom)
    (hopen : IsOpenImmersion C S hS (groupoidPreRelation G).left) :
    IsAlgebraicSpace C S hS (quotientSheaf (groupoidPreRelation G)).obj

AlgebraicGeometry.Space.isEtale_quotientSheafToBase_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/OpenRelationEtaleQuotient.lean, line 574. The attribute's comment: “étaleness of the structural morphism U/R → Y”.

Stacks 0DU1, étaleness of the quotient over the base. Let (U, R, s, t, c) be a groupoid in algebraic spaces over an algebraic space Y whose object space is flat and locally of finite presentation over Y and whose pre-relation (t, s) : R ⟶ U ×_Y U is an open immersion. Then the canonical morphism U/R ⟶ Y of Stacks 044J is étale.

Algebraicity of the quotient, AlgebraicGeometry.Space.isAlgebraicSpace_quotientSheaf_of_isOpenImmersion, is what Stacks 06PG needs in order to give the three properties of the covering map U ⟶ U/R.

theorem isEtale_quotientSheafToBase_of_isOpenImmersion
    (hflat : IsFlat C S hS G.objectsToBase.hom)
    (hlfp : IsLocallyOfFinitePresentation C S hS G.objectsToBase.hom)
    (hopen : IsOpenImmersion C S hS (groupoidPreRelation G).left) :
    IsEtale C S hS (quotientSheafToBase Y.property.isSheaf (groupoidPreRelation G)).hom

AlgebraicGeometry.Stack.quotientStackToQuotientSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/OpenRelationEtaleQuotient.lean, line 638. The attribute's comment: “the canonical comparison [U/R] → U/R”.

Stacks 0DU1, the canonical comparison [U/R] ⟶ U/R. Under the hypotheses of Stacks 0DU1 the quotient sheaf is an algebraic space (AlgebraicGeometry.Space.isAlgebraicSpace_quotientSheaf_of_isOpenImmersion), so the quotient projection U ⟶ U/R is an invariant morphism to an algebraic space, and it descends to a 1-morphism from the quotient stack to the category fibred in sets of U/R.

This is the comparison asserted by the equality X = [U/R] = U/R of the source. It is a real construction — the descent of Stacks 044R applied to the quotient projection — and not a choice out of an existence statement; AlgebraicGeometry.Stack.quotientStackToQuotientSheaf_unique shows it is the only 1-morphism restricting along the projection to the quotient map.

noncomputable def quotientStackToQuotientSheaf :
    quotientStack G ⥤ᵇ
      (fibredCategory C S hS (quotientSheafSpace G hflat hlfp hopen).obj).val

AlgebraicGeometry.Stack.quotientStackProjection_comp_quotientStackToQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/OpenRelationEtaleQuotient.lean, line 648. The attribute's comment: “the comparison composed with the quotient projection is the map attached to U → U/R”.

Stacks 0DU1. The canonical comparison composed with the projection U ⟶ [U/R] of Stacks 044R is the 1-morphism that Stacks 0458 attaches to the quotient map U ⟶ U/R.

theorem quotientStackProjection_comp_quotientStackToQuotientSheaf :
    BasedFunctor.comp (quotientStackProjection G)
        (quotientStackToQuotientSheaf G hflat hlfp hopen) =
      (associatedMap C S hS (Space.toQuotientSheaf (Space.groupoidPreRelation G))).1.hom

AlgebraicGeometry.Stack.quotientStackToQuotientSheaf_comp_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/OpenRelationEtaleQuotient.lean, line 678. The attribute's comment: “the comparison is compatible with the structural morphisms to the base”.

Stacks 0DU1. The canonical comparison is a morphism over the base: composed with the 1-morphism attached to the structural morphism U/R ⟶ Y it is the structure arrow [U/R] ⟶ Y of Stacks 044R.

Both sides restrict along the projection to the structure morphism U ⟶ Y of the object space, and by Stacks 0DUH a 1-morphism from the quotient stack to an algebraic space is determined by that restriction.

theorem quotientStackToQuotientSheaf_comp_toBase :
    BasedFunctor.comp (quotientStackToQuotientSheaf G hflat hlfp hopen)
        (associatedMap C S hS (quotientSheafToBaseSpace G hflat hlfp hopen).hom).1.hom =
      quotientStackToBase G

AlgebraicGeometry.Stack.isAlgebraicSpace_and_equivalenceOver_and_isEtale_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/OpenRelationEtaleQuotientEquivalence.lean, line 413.

Stacks 0DU1. Let (U, R, s, t, c) be a groupoid in algebraic spaces over an algebraic space Y whose object space U is flat and locally of finite presentation over Y and whose pre-relation (t, s) : R ⟶ U ×_Y U is an open immersion. Then X = [U/R] = U/R is an algebraic space and X ⟶ Y is étale: the quotient sheaf U/R of Stacks 044J is an algebraic space, the canonical comparison AlgebraicGeometry.Stack.quotientStackToQuotientSheaf from the quotient stack [U/R] to it is an equivalence over the big fppf site, and the structural morphism U/R ⟶ Y is étale.

The three clauses are AlgebraicGeometry.Space.isAlgebraicSpace_quotientSheaf_of_isOpenImmersion, AlgebraicGeometry.Stack.nonempty_equivalenceOver_quotientStackToQuotientSheaf and AlgebraicGeometry.Space.isEtale_quotientSheafToBase_of_isOpenImmersion.

theorem isAlgebraicSpace_and_equivalenceOver_and_isEtale_of_isOpenImmersion :
    IsAlgebraicSpace C S hS (Space.quotientSheaf (Space.groupoidPreRelation G)).obj ∧
      Nonempty { e : StacksRepresentableCFG.EquivalenceOver (quotientStack G).p
          (fibredCategory C S hS (quotientSheafSpace G hflat hlfp hopen).obj).val.p //
        e.hom.functor = (quotientStackToQuotientSheaf G hflat hlfp hopen).toFunctor } ∧
      Space.IsEtale C S hS
        (Space.quotientSheafToBase Y.property.isSheaf (Space.groupoidPreRelation G)).hom

Tag 0DU2, a lemma

Tag 0DU2 in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_representable_surjective_etale_quotientStackMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/OpenSubgroupoidQuotientStackFull.lean, line 84.

Stacks 0DU2. Let (U, R, s, t, c) be a groupoid in algebraic spaces (here over an algebraic space A over S, which contains the case of a groupoid over S) with s, t flat and locally of finite presentation, and let P ⊆ R be an open subspace such that (U, P, s|_P, t|_P, c|_P) is a groupoid in algebraic spaces; that is, let φ : G ⟶ H be a morphism of groupoids in algebraic spaces whose map on objects is an isomorphism and whose map on arrows is an open immersion. Then [U/P] and [U/R] are algebraic stacks, and [φ] : [U/P] ⟶ [U/R] is representable by algebraic spaces, surjective and étale, the last two in the sense of Stacks 03YK.

theorem isAlgebraicStack_representable_surjective_etale_quotientStackMap
    {G H : GroupoidInAlgebraicSpaces C S hS A} (φ : GroupoidInAlgebraicSpaces.Hom G H)
    (hopen : Space.IsOpenImmersion C S hS φ.toGroupoidHom.mapArrows)
    (hobj : IsIso φ.toGroupoidHom.mapObjects)
    (hsflat : Space.IsFlat C S hS H.source.hom) (htflat : Space.IsFlat C S hS H.target.hom)
    (hslfp : Space.IsLocallyOfFinitePresentation C S hS H.source.hom)
    (htlfp : Space.IsLocallyOfFinitePresentation C S hS H.target.hom) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack G) ∧
      IsAlgebraicStack.{u, w} C S hS (quotientStack H) ∧
      ∃ hrep : IsRepresentableByAlgebraicSpaces C S hS (quotientStackMap φ),
        HasRelativeProperty.{u, u + 1, u + 1, u} C S hS
          (Space.surjectiveMorphismProperty C S hS) (quotientStackMapCFGHom φ) hrep ∧
        HasRelativeProperty.{u, u + 1, u + 1, u} C S hS
          (Space.etaleMorphisms C S hS) (quotientStackMapCFGHom φ) hrep

Tag 0DU3, a lemma

Tag 0DU3 in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.exists_quasiSplitting_isAffine_isFinite_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleLocalStructureQuasiSplitting.lean, line 165. The attribute's comment: “the groupoid scheme of clause (3), with U and its arrow scheme affine and source and target finite, flat and locally of finite presentation, built from a quasi-splitting of Stacks 04RK. Clause (1), clause (2) and the identification of the stack with [U/R] in clause (3) are NOT covered: see the implementation notes for the three named obstructions”.

Stacks 0DU3, the groupoid of clause (3).

Let (U, R, s, t, c) be a groupoid scheme over S with U affine and with s and t flat and locally of finite presentation, and let u be a point of U over which the groupoid is quasi-split in the sense of Stacks 04RK, part (3). Then there is a groupoid scheme (U, P, s|_P, t|_P, c|_P) together with a morphism into (U, R, s, t, c) which is an open immersion on arrow schemes and the identity on object schemes, carrying the identity arrow at u, whose both structure schemes are affine and whose source and target are finite, flat and locally of finite presentation.

This is the groupoid scheme of clause (3) of Stacks 0DU3, with every property that clause asserts of it: the source's proof takes 𝒰 = [U/P] for exactly this P. The properties are asserted of one single groupoid scheme, as the tag asserts them.

The three conjuncts that are not re-derivations are the equality of object schemes, the open immersion and the identity arrow: these are the three pieces of data a quasi-splitting is (conditions (a) and (c) of Stacks 04RK), and they are listed so that the groupoid produced is pinned to be the quasi-splitting at u rather than an unrelated groupoid. Everything else is derived: affineness of the object scheme from the equality, flatness and local finite presentation of s|_P and t|_P from the open immersion composed with s and t, and affineness of the arrow scheme from finiteness of s|_P over the affine object scheme — the last being the step where an open subscheme of R is shown affine without R being used at all.

theorem exists_quasiSplitting_isAffine_isFinite_flat [IsAffine G.objects.left]
    [Flat G.source.left] [LocallyOfFinitePresentation G.source.left]
    [Flat G.target.left] [LocallyOfFinitePresentation G.target.left]
    {u : G.objects.left} (h : IsQuasiSplitAt G u) :
    ∃ (G' : GroupoidScheme S) (φ : Hom G' G),
      G'.objects = G.objects ∧
      IsOpenImmersion φ.mapArrows.left ∧
      (∃ p : G'.arrows.left, φ.mapArrows.left.base p = G.identity.left.base u) ∧
      IsAffine G'.objects.left ∧ IsAffine G'.arrows.left ∧
      IsFinite G'.source.left ∧
      Flat G'.source.left ∧ LocallyOfFinitePresentation G'.source.left ∧
      IsFinite G'.target.left ∧
      Flat G'.target.left ∧ LocallyOfFinitePresentation G'.target.left

AlgebraicGeometry.Stack.exists_etale_quotientStack_of_isQuasiDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleLocalStructureStack.lean, line 341.

Stacks 0DU3. Let 𝒳 be an algebraic stack over S which is quasi-DM (Stacks 050D) with separated diagonal Δ_{𝒳/S} (Stacks 04XB), and let x ∈ |𝒳|. Then there is a 1-morphism of algebraic stacks g : 𝒰 ⟶ 𝒳 such that

some point of |𝒰| maps to x,

g is representable by algebraic spaces and étale,

𝒰 is the quotient stack [U/R] of (the realization of) a groupoid scheme (U, R, s, t, c) with U and R affine and s, t finite, flat and locally of finite presentation: there is an equivalence over the site between that quotient stack and 𝒰.

The parenthetical equivalent hypothesis of the source (I_𝒳 ⟶ 𝒳 locally quasi-finite and separated) is Stacks 0CL0, parts (1) and (5).

theorem exists_etale_quotientStack_of_isQuasiDM (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hQ : AlgebraicStacks.IsAbsolutelyQuasiDM B S hS B.contains_terminal 𝒳)
    (hΔ : Stack.IsSeparated.{u, u, u + 1} B S hS
      (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val
        (schemeStack.{u, w} B S hS (Over.mk (𝟙 (B.obj hS)))).val
        (structureMorphism B S hS 𝒳).hom))
    (x : AlgebraicStacks.points B S hS 𝒳) :
    ∃ (𝒰 : AlgebraicStacks.{u, w} B S hS) (g : 𝒰 ⟶ 𝒳),
      (∃ v, AlgebraicStacks.pointsMap B S hS g v = x) ∧
      (IsRepresentableByAlgebraicSpaces B S hS g.hom.hom ∧ IsEtale B S hS g) ∧
      ∃ (G : GroupoidScheme S) (hU : B.Contains G.objects.left) (hR : B.Contains G.arrows.left)
        (hP : B.Contains (pullback G.source G.target).left),
        IsAffine G.objects.left ∧ IsAffine G.arrows.left ∧
        IsFinite G.source.left ∧ Flat G.source.left ∧ LocallyOfFinitePresentation G.source.left ∧
        IsFinite G.target.left ∧ Flat G.target.left ∧ LocallyOfFinitePresentation G.target.left ∧
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (quotientStack (G.realization B hS hU hR hP)).p 𝒰.val.val.p)

Tag 0DU4, a lemma

Tag 0DU4 in the Stacks Project.

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

Stacks 0DU4. Let 𝒳 be an algebraic stack over S which is quasi-DM (Stacks 050D) with separated diagonal Δ_{𝒳/S} (Stacks 04XB), and let x ∈ |𝒳| be a point at which the automorphism group of 𝒳 is finite (Remark 0DTU). Then there is a 1-morphism of algebraic stacks g : 𝒰 ⟶ 𝒳 such that

some point v ∈ |𝒰| maps to x and g induces an isomorphism between the automorphism groups at v and x (Stacks 0DTW),

g is representable by algebraic spaces and étale,

𝒰 is the quotient stack [U/R] of (the realization of) a groupoid scheme (U, R, s, t, c) with U and R affine and s, t finite, flat and locally of finite presentation: there is an equivalence over the site between that quotient stack and 𝒰.

The parenthetical equivalent hypothesis of the source (I_𝒳 ⟶ 𝒳 locally quasi-finite and separated) is Stacks 0CL0, parts (1) and (5).

theorem exists_etale_quotientStack_inducesIsomorphismAt (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hQ : AlgebraicStacks.IsAbsolutelyQuasiDM B S hS B.contains_terminal 𝒳)
    (hΔ : Stack.IsSeparated.{u, u, u + 1} B S hS
      (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val
        (schemeStack.{u, w} B S hS (Over.mk (𝟙 (B.obj hS)))).val
        (structureMorphism B S hS 𝒳).hom))
    (x : AlgebraicStacks.points B S hS 𝒳)
    (hAut : AutomorphismGroupHasProperty B S hS (IsFiniteOverBase B S hS) x) :
    ∃ (𝒰 : AlgebraicStacks.{u, w} B S hS) (g : 𝒰 ⟶ 𝒳),
      (∃ v, AlgebraicStacks.pointsMap B S hS g v = x ∧ InducesIsomorphismAt B S hS g v) ∧
      (IsRepresentableByAlgebraicSpaces B S hS g.hom.hom ∧ IsEtale B S hS g) ∧
      ∃ (G : GroupoidScheme S) (hU : B.Contains G.objects.left) (hR : B.Contains G.arrows.left)
        (hP : B.Contains (pullback G.source G.target).left),
        IsAffine G.objects.left ∧ IsAffine G.arrows.left ∧
        IsFinite G.source.left ∧ Flat G.source.left ∧ LocallyOfFinitePresentation G.source.left ∧
        IsFinite G.target.left ∧ Flat G.target.left ∧ LocallyOfFinitePresentation G.target.left ∧
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (quotientStack (G.realization B hS hU hR hP)).p 𝒰.val.val.p)

Tag 0DU5, a lemma

Tag 0DU5 in the Stacks Project.

AlgebraicGeometry.Stack.exists_etale_quotientStack_residualGerbeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleLocalStructureResidualGerbeExistence.lean, line 98.

Stacks 0DU5. Let 𝒳 be an algebraic stack over S which is quasi-DM (Stacks 050D) with separated diagonal Δ_{𝒳/S} (Stacks 04XB), and let x ∈ |𝒳| be a point which can be represented by a quasi-compact morphism from the spectrum of a field. Then there is a 1-morphism of algebraic stacks g : 𝒰 ⟶ 𝒳 such that

some point v ∈ |𝒰| maps to x, the residual gerbes of 𝒰 at v and of 𝒳 at x exist, and the 1-morphism between them induced by g (Stacks 0DTH) is an isomorphism for every choice of them;

g is representable by algebraic spaces and étale;

𝒰 is the quotient stack [U/R] of (the realization of) a groupoid scheme (U, R, s, t, c) with U and R affine and s, t finite, flat and locally of finite presentation: there is an equivalence over the site between that quotient stack and 𝒰.

The parenthetical equivalent hypothesis of the source (I_𝒳 ⟶ 𝒳 locally quasi-finite and separated) is Stacks 0CL0, parts (1) and (5). See the module documentation for the proof.

theorem exists_etale_quotientStack_residualGerbeMap (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hQ : AlgebraicStacks.IsAbsolutelyQuasiDM B S hS B.contains_terminal 𝒳)
    (hΔ : Stack.IsSeparated.{u, u, u + 1} B S hS
      (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val
        (schemeStack.{u, w} B S hS (Over.mk (𝟙 (B.obj hS)))).val
        (structureMorphism B S hS 𝒳).hom))
    (x : AlgebraicStacks.points B S hS 𝒳)
    (hqc : ∃ p : FieldValuedPoint B S hS 𝒳.val.val,
      pointClass B S hS 𝒳.val.val 𝒳.val.isFiberedInGroupoids p = x ∧
        IsQuasiCompactFieldValuedPoint B S hS 𝒳.val p) :
    ∃ (𝒰 : AlgebraicStacks.{u, w} B S hS) (g : 𝒰 ⟶ 𝒳)
      (v : AlgebraicStacks.points B S hS 𝒰),
      (AlgebraicStacks.pointsMap B S hS g v = x ∧
        (∃ P : ObjectProperty 𝒰.val.val.obj, IsResidualGerbeAt B S hS 𝒰 v P) ∧
        (∃ Q : ObjectProperty 𝒳.val.val.obj, IsResidualGerbeAt B S hS 𝒳 x Q) ∧
        ∀ (P : ObjectProperty 𝒰.val.val.obj) (Q : ObjectProperty 𝒳.val.val.obj)
          (hv : IsResidualGerbeAt B S hS 𝒰 v P)
          (hx : IsResidualGerbeAt B S hS 𝒳 (AlgebraicStacks.pointsMap B S hS g v) Q),
          Nonempty (Functor.IsEquivalenceOver
            (fullSubcategoryAlgebraicStack 𝒰 P hv.2.choose).val.val.p
            (fullSubcategoryAlgebraicStack 𝒳 Q hx.2.choose).val.val.p
            (CatFiberedInGroupoids.homFunctor
              (residualGerbeMap B S hS g hv.2.choose hx.2.choose
                (map_mem_of_isResidualGerbeAt B S hS g v _ rfl hv hx)).hom))) ∧
      (IsRepresentableByAlgebraicSpaces B S hS g.hom.hom ∧ IsEtale B S hS g) ∧
      ∃ (G : GroupoidScheme S) (hU : B.Contains G.objects.left) (hR : B.Contains G.arrows.left)
        (hP : B.Contains (pullback G.source G.target).left),
        IsAffine G.objects.left ∧ IsAffine G.arrows.left ∧
        IsFinite G.source.left ∧ Flat G.source.left ∧ LocallyOfFinitePresentation G.source.left ∧
        IsFinite G.target.left ∧ Flat G.target.left ∧ LocallyOfFinitePresentation G.target.left ∧
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (quotientStack (G.realization B hS hU hR hP)).p 𝒰.val.val.p)

Sources

LeanAlgebraicGeometry.Space.isAlgebraicSpace_quotientSheaf_of_isOpenImmersion · AlgebraicGeometry.Space.isEtale_quotientSheafToBase_of_isOpenImmersion · AlgebraicGeometry.Stack.quotientStackToQuotientSheaf · AlgebraicGeometry.Stack.quotientStackProjection_comp_quotientStackToQuotientSheaf · AlgebraicGeometry.Stack.quotientStackToQuotientSheaf_comp_toBase · AlgebraicGeometry.Stack.isAlgebraicSpace_and_equivalenceOver_and_isEtale_of_isOpenImmersion · AlgebraicGeometry.Stack.isAlgebraicStack_representable_surjective_etale_quotientStackMap · Stacks.Groupoids.GroupoidScheme.exists_quasiSplitting_isAffine_isFinite_flat

Section101.33 Smooth morphisms #

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

Tag 075U, a definition

Tag 075U in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothAlgebraicStack.lean, line 93.

Stacks 075U. A 1-morphism of algebraic stacks over S is smooth when it passes the existential smooth-diagram test of Stacks 06FM at smoothness of morphisms of algebraic spaces: there are algebraic spaces U, V over S, a smooth 1-morphism a from the category fibred in groupoids of U to the source which is surjective on objects, a smooth 1-morphism b from the one of V to the target, and a morphism h : U ⟶ V making the square 2-commute, with h a smooth morphism of algebraic spaces.

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

Tag 075V, a lemma

Tag 075V in the Stacks Project.

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

Stacks 075V. The composite of two smooth 1-morphisms of algebraic stacks over S is smooth: the composition remark Stacks 06FP at smoothness of morphisms of algebraic spaces, which is smooth local on the source-and-target by the smooth case of Stacks 06FC and stable under composition by Stacks 03ZD.

theorem isSmooth_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsSmooth B S hS f) (hg : IsSmooth B S hS g) :
    IsSmooth B S hS (f ≫ g)

Tag 075W, a lemma

Tag 075W in the Stacks Project.

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

Stacks 075W. A base change of a smooth 1-morphism of algebraic stacks over S is smooth: for f : 𝒳 ⟶ 𝒴 smooth and g : 𝒴' ⟶ 𝒴 arbitrary, the projection to 𝒴' of any 2-fibre product square over the cospan (g, f) is smooth.

theorem isSmooth_baseChange {𝒳 𝒴 𝒴' : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (Q : Bicategory.TwoCommSq g f) (hQ : Bicategory.IsTwoFibreProduct Q)
    (hf : IsSmooth B S hS f) :
    IsSmooth B S hS Q.fst

Tag 0DN7, a lemma

Tag 0DN7 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isSmooth_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothFppfDescent.lean, line 63.

Stacks 0DN7. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒵 ⟶ 𝒴 be surjective, flat and locally of finite presentation. If the base change 𝒵 ×_𝒴 𝒳 ⟶ 𝒵 of f along g is smooth, then so is f.

theorem isSmooth_of_baseChange
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (hgs : Stack.IsSurjective B S hS g)
    (hgflat : IsFlat B S hS g)
    (hglfp : IsLocallyOfFinitePresentation B S hS g)
    (hbase : IsSmooth B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst) :
    IsSmooth B S hS f

Tag 0DNP, a lemma

Tag 0DNP in the Stacks Project.

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

Stacks 0DNP. A smooth 1-morphism of algebraic stacks over S is locally of finite presentation.

Stacks 075U is the existential smooth-diagram criterion at smoothness of morphisms of algebraic spaces, which is locally of finite presentation by Stacks 04AJ; monotonicity (Stacks 06PS) gives the existential criterion at local finite presentation, and the round trip of Stacks 06FM — whose smooth-locality hypothesis is the local-finite-presentation case of Stacks 06FC — gives the universal criterion, which is Stacks 06Q2 part (1).

theorem isLocallyOfFinitePresentation_of_isSmooth
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsSmooth B S hS f) :
    IsLocallyOfFinitePresentation B S hS f

Tag 0DZR, a lemma

Tag 0DZR in the Stacks Project.

AlgebraicGeometry.Stack.smoothLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothLocus.lean, line 1221. The attribute's comment: “the maximal open substack on which f is smooth exists and is unique, and its formation commutes with precomposition by smooth morphisms, with base change by flat morphisms locally of finite presentation, and with flat base change when f is locally of finite presentation”.

Stacks 0DZR. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. There is a maximal open substack 𝒰 ⊆ 𝒳 such that f|_𝒰 : 𝒰 ⟶ 𝒴 is smooth — an open substack on which f is smooth containing every other one, unique by maximality. Moreover, formation of this open substack commutes with

precomposing by smooth morphisms: for g : 𝒳' ⟶ 𝒳 smooth, the open substack of g ≫ f is the inverse image along g of that of f;

base change by morphisms which are flat and locally of finite presentation: for any 2-fibre product P of f along such a g : 𝒴' ⟶ 𝒴, the open substack of the base change P.fst is the inverse image along the projection P.snd of that of f;

base change by flat morphisms, provided f is locally of finite presentation.

The open substack is constructed from a smooth chart of f: the image of the smooth locus of the chart's morphism of algebraic spaces (Stacks 0DZI), read as an open substack by Stacks 06FJ (AlgebraicGeometry.Stack.openSubstackOfPoints). Clause (1) is descent along the smooth 𝒰' ⟶ 𝒳, and clauses (2) and (3) reduce to Stacks 0DZI on a cartesian square of charts.

theorem smoothLocus {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    (∃! W : OpenSubstack 𝒳, IsSmoothLocus B S hS f W) ∧
    (∀ (𝒳' : AlgebraicStacks.{u, w} B S hS) (g : 𝒳' ⟶ 𝒳),
      AlgebraicStacks.IsSmooth B S hS g →
      ∀ (W : OpenSubstack 𝒳) (W' : OpenSubstack 𝒳'),
        IsSmoothLocus B S hS f W → IsSmoothLocus B S hS (g ≫ f) W' →
          W'.property = fun x => W.property (g.hom.hom.toFunctor.obj x)) ∧
    (∀ (𝒴' : AlgebraicStacks.{u, w} B S hS) (g : 𝒴' ⟶ 𝒴) (P : Bicategory.TwoCommSq g f),
      Bicategory.IsTwoFibreProduct P →
      AlgebraicStacks.IsFlat B S hS g → AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g →
      ∀ (W : OpenSubstack 𝒳) (W' : OpenSubstack P.pt),
        IsSmoothLocus B S hS f W → IsSmoothLocus B S hS P.fst W' →
          W'.property = fun x => W.property (P.snd.hom.hom.toFunctor.obj x)) ∧
    (AlgebraicStacks.IsLocallyOfFinitePresentation B S hS f →
      ∀ (𝒴' : AlgebraicStacks.{u, w} B S hS) (g : 𝒴' ⟶ 𝒴) (P : Bicategory.TwoCommSq g f),
        Bicategory.IsTwoFibreProduct P → AlgebraicStacks.IsFlat B S hS g →
        ∀ (W : OpenSubstack 𝒳) (W' : OpenSubstack P.pt),
          IsSmoothLocus B S hS f W → IsSmoothLocus B S hS P.fst W' →
            W'.property = fun x => W.property (P.snd.hom.hom.toFunctor.obj x))

Tag 0DLS, a lemma

Tag 0DLS in the Stacks Project.

AlgebraicGeometry.Stack.isSmooth_quotientStackModelToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothQuotientStackOfAction.lean, line 156.

Stacks 0DLS. Let X ⟶ Y be a smooth morphism of algebraic spaces over S, let G be a group algebraic space over Y which is flat and locally of finite presentation over Y, and let G act on X over Y. Then the quotient stack [X/G] is smooth over Y: for every algebraic stack 𝒳 equivalent over the big fppf site to [X/G], the canonical morphism [X/G] ⟶ Y of Stacks 044R, read on 𝒳, is a smooth 1-morphism of algebraic stacks in the sense of Stacks 075U.

theorem isSmooth_quotientStackModelToBase
    (Y : AlgebraicSpaces B S hS) (G X : Over Y.obj) [GrpObj G] [ModObj G X]
    (hG : IsAlgebraicSpace B S hS G.left) (hX : IsAlgebraicSpace B S hS X.left)
    (hXsmooth : Space.IsSmooth B S hS X.hom)
    (hGflat : Space.IsFlat B S hS G.hom)
    (hGlfp : Space.IsLocallyOfFinitePresentation B S hS G.hom)
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (e : StacksRepresentableCFG.EquivalenceOver
      (quotientStack (actionGroupoid B S hS Y G X hG hX)).p 𝒳.val.val.p) :
    AlgebraicStacks.IsSmooth B S hS
      (quotientStackModelToBase.{u, w} B S hS Y G X hG hX 𝒳 e)

Tag 0DN8, a lemma

Tag 0DN8 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isSurjective_and_isSmooth_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GerbeSmooth.lean, line 105.

Stacks 0DN8. Let π : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S. If 𝒳 is a gerbe over 𝒴, then π is surjective and smooth.

theorem isSurjective_and_isSmooth_of_isGerbeOver {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (hf : IsGerbeOver B S hS f) :
    Stack.IsSurjective B S hS f ∧ IsSmooth B S hS f

Sources

Section101.34 Types of morphisms étale-smooth local on source-and-target #

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

Tag 0CIF, a lemma

Tag 0CIF in the Stacks Project.

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

Stacks 0CIF, the equivalence of conditions (1) and (2). Let P be a property of morphisms of algebraic spaces over S which is étale-smooth local on the source-and-target, and let f : 𝒳 ⟶ 𝒴 be a Deligne–Mumford 1-morphism of algebraic stacks over S. Then the following are equivalent:

for every 2-commutative square of algebraic spaces h : U → V over f with V → 𝒴 smooth and U → 𝒳 ×_𝒴 V étale, the morphism h has P;

for some such square with U → 𝒳 surjective, the morphism h has P.

theorem hasPropertyOnEveryEtaleSmoothDiagram_iff_some
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : Space.IsEtaleSmoothLocalOnSourceAndTarget B S hS P)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (hf : IsDM B S hS f) :
    HasPropertyOnEveryEtaleSmoothDiagram B S hS P f ↔
      HasPropertyOnSomeEtaleSmoothDiagram B S hS P f

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

The third assertion of Stacks 0CIF. For an étale-smooth local property P of morphisms of algebraic spaces over S which is stable under base change and local at the target for the fppf precoverage, and a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S representable by algebraic spaces, the existential étale-smooth diagram test for P is equivalent to the relative property P of Stacks 03YK.

This is the covering set of the key "representable morphism" of Stacks 0CIF: the key names a single asserted equivalence, and neither half of it alone asserts that equivalence.

theorem hasPropertyOnSomeEtaleSmoothDiagram_iff_relative
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : Space.IsEtaleSmoothLocalOnSourceAndTarget B S hS P)
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage.{u, v} B S hS)]
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    HasPropertyOnSomeEtaleSmoothDiagram B S hS P f ↔
      HasRelativeProperty.{u, u, u + 1, v} B S hS P f.hom hf

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

Stacks 0CIF, the assertion for representable source and target. For a property P of morphisms of algebraic spaces over S which is étale-smooth local on the source-and-target, and a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S whose source and target are representable by algebraic spaces F and G, the existential étale-smooth diagram test holds for f exactly when the induced morphism F ⟶ G of representing presheaves has P.

Forward: the given diagram becomes a square of morphisms of algebraic spaces whose comparison to the fibre product is étale, and Stacks 0CG1 applies. Backward: test the condition on the diagram given by the two representing equivalences.

theorem hasPropertyOnSomeEtaleSmoothDiagram_iff_represented :
    HasPropertyOnSomeEtaleSmoothDiagram B S hS P f ↔
      P (ObjectProperty.homMk (representingMap B S hS 𝒳.val 𝒴.val F G eX eY f.hom) :
        (⟨F, hF⟩ : AlgebraicSpaces B S hS) ⟶ ⟨G, hG⟩)

Tag 0CIG, a definition

Tag 0CIG in the Stacks Project.

AlgebraicGeometry.Stack.HasEtaleSmoothLocalProperty, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleSmoothLocalMorphism.lean, line 189. The attribute's comment: “the property of a DM morphism of algebraic stacks induced by an etale-smooth local property P of morphisms of algebraic spaces: IsDM f together with the universal etale-smooth diagram test at P, which is condition (1) of Stacks 0CIF”.

Stacks 0CIG. The property of Deligne–Mumford morphisms of algebraic stacks induced by an étale-smooth local property P of morphisms of algebraic spaces over S: the morphism is Deligne–Mumford and passes the universal étale-smooth diagram test at P.

For an étale-smooth local P — AlgebraicGeometry.Space.IsEtaleSmoothLocalOnSourceAndTarget, Stacks 0CFZ — Stacks 0CIF identifies that test with the existential one.

abbrev HasEtaleSmoothLocalProperty
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : Prop

Tag 0CIH, a remark

Tag 0CIH in the Stacks Project.

AlgebraicGeometry.Stack.hasEtaleSmoothLocalProperty_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleSmoothLocalMorphismComp.lean, line 208. The attribute's comment: “with the substantial direction of Stacks 06N3 as the explicit hypothesis hForward (the structure theorem behind it, Stacks 06MD, 06N0, 06N2, 06G2, 06G3, is absent from the library); it enters only through Stacks 0CIA, which supplies the surjective etale presentations of the two 2-fibre products the source's argument chooses”.

Stacks 0CIH. Let P be a property of morphisms of algebraic spaces over S which is étale-smooth local on the source-and-target and stable under composition. Then the property of Deligne–Mumford 1-morphisms of algebraic stacks over S which Stacks 0CIG induces from P is stable under composition.

The composite is Deligne–Mumford by Stacks 050K. For the diagram test, take a smooth chart W ⟶ 𝒵 surjective on objects, an étale chart V ⟶ 𝒴 ×_𝒵 W and an étale chart U ⟶ 𝒳 ×_𝒴 V, the last two by Stacks 0CIA; the morphisms V ⟶ W and U ⟶ V have P, hence so does U ⟶ W, and pasting the two 2-fibre products exhibits U as an étale chart of 𝒳 ×_𝒵 W.

theorem hasEtaleSmoothLocalProperty_comp
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : Space.IsEtaleSmoothLocalOnSourceAndTarget B S hS P)
    (hcomp : ∀ {X Y Z : AlgebraicSpaces B S hS} (p : X ⟶ Y) (q : Y ⟶ Z), P p → P q → P (p ≫ q))
    (hT : B.Contains (⊤_ Scheme.{u}))
    (hForward : ExistsEtalePresentationOfIsAbsolutelyDM.{u, w} B S hS hT)
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : HasEtaleSmoothLocalProperty B S hS P f)
    (hg : HasEtaleSmoothLocalProperty B S hS P g) :
    HasEtaleSmoothLocalProperty B S hS P (f ≫ g)

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

Stacks 0CIH. Let P be a property of morphisms of algebraic spaces over S which is étale-smooth local on the source-and-target and stable under composition. Then the property of Deligne–Mumford 1-morphisms of algebraic stacks over S which Stacks 0CIG induces from P is stable under composition: if f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 are DM and have it, so does f ≫ g.

This is AlgebraicGeometry.Stack.hasEtaleSmoothLocalProperty_comp with its argument hForward discharged by the unconditional forward direction of Stacks 06N3, AlgebraicGeometry.Stack.existsEtalePresentationOfIsAbsolutelyDM, at AlgebraicGeometry.BigFppfSite.contains_terminal.

theorem hasEtaleSmoothLocalProperty_comp_of_isEtaleSmoothLocal
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : Space.IsEtaleSmoothLocalOnSourceAndTarget B S hS P)
    (hcomp : ∀ {X Y Z : AlgebraicSpaces B S hS} (p : X ⟶ Y) (q : Y ⟶ Z), P p → P q → P (p ≫ q))
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : HasEtaleSmoothLocalProperty B S hS P f)
    (hg : HasEtaleSmoothLocalProperty B S hS P g) :
    HasEtaleSmoothLocalProperty B S hS P (f ≫ g)

Tag 0CII, a remark

Tag 0CII in the Stacks Project.

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

Stacks 0CII. Let P be a property of morphisms of algebraic spaces over S which is étale-smooth local on the source-and-target and stable under base change. If a Deligne–Mumford 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S has the property of Stacks 0CIG induced by P, then so does its base change 𝒳 ×_𝒴 𝒵 ⟶ 𝒵 along any 1-morphism g : 𝒵 ⟶ 𝒴, the second projection of any 2-fibre product square of (f, g).

theorem hasEtaleSmoothLocalProperty_snd_of_isTwoFibreProduct_of_isStableUnderBaseChange
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : Space.IsEtaleSmoothLocalOnSourceAndTarget B S hS P)
    [P.IsStableUnderBaseChange]
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (R : Bicategory.TwoCommSq f g) (hR : Bicategory.IsTwoFibreProduct R)
    (hf : HasEtaleSmoothLocalProperty B S hS P f) :
    HasEtaleSmoothLocalProperty B S hS P R.snd

AlgebraicGeometry.Stack.hasEtaleSmoothLocalProperty_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleSmoothLocalMorphismBaseChangeStable.lean, line 146. The attribute's comment: “for the canonical 2-fibre product square of Stacks 003Q, which is the shape the library version of Stacks 050F is stated at, and with the substantial direction of Stacks 06N3 as the explicit hypothesis hForward (the structure theorem behind it, Stacks 06MD, 06N0, 06N2, 06G2, 06G3, is absent from the library); it enters only through Stacks 0CIA, which supplies the surjective etale presentation the source's argument chooses”.

Stacks 0CII. Let P be a property of morphisms of algebraic spaces over S which is étale-smooth local on the source-and-target and stable under base change. Then the property of Deligne–Mumford 1-morphisms of algebraic stacks over S that Stacks 0CIG induces from P is inherited by the base change of a 1-morphism along the canonical 2-fibre product square.

The Deligne–Mumford condition on the base change is Stacks 050F, and the diagram of condition (2) of Stacks 0CIF is the source's: its top-left corner is V' ×_V U for a smooth presentation V ⟶ 𝒴, a surjective étale presentation U ⟶ 𝒳 ×_𝒴 V and a smooth presentation V' ⟶ 𝒵 ×_𝒴 V, and its top horizontal morphism is the base change of U ⟶ V along V' ⟶ V.

theorem hasEtaleSmoothLocalProperty_baseChange
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : Space.IsEtaleSmoothLocalOnSourceAndTarget B S hS P)
    [P.IsStableUnderBaseChange]
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (hForward : ExistsEtalePresentationOfIsAbsolutelyDM.{u, w} B S hS hZ)
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (hf : HasEtaleSmoothLocalProperty B S hS P f) :
    HasEtaleSmoothLocalProperty B S hS P
      (AlgebraicStacks.twoFibreProductSquare B S hS f g).snd

Tag 0CIJ, a remark

Tag 0CIJ in the Stacks Project.

AlgebraicGeometry.Stack.hasEtaleSmoothLocalProperty_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleSmoothLocalMorphism.lean, line 206.

Stacks 0CIJ. An implication between properties of morphisms of algebraic spaces over S also holds for the properties of 1-morphisms of algebraic stacks that Stacks 0CIG induces from them. No étale-smooth locality hypothesis on either property is needed.

theorem hasEtaleSmoothLocalProperty_mono
    {P P' : MorphismProperty (AlgebraicSpaces B S hS)} (hPP' : P ≤ P')
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴}
    (hf : HasEtaleSmoothLocalProperty B S hS P f) :
    HasEtaleSmoothLocalProperty B S hS P' f

Sources

LeanAlgebraicGeometry.Stack.hasPropertyOnEveryEtaleSmoothDiagram_iff_some · AlgebraicGeometry.Stack.hasPropertyOnSomeEtaleSmoothDiagram_iff_relative · AlgebraicGeometry.Stack.hasPropertyOnSomeEtaleSmoothDiagram_iff_represented · AlgebraicGeometry.Stack.HasEtaleSmoothLocalProperty · AlgebraicGeometry.Stack.hasEtaleSmoothLocalProperty_comp · AlgebraicGeometry.Stack.hasEtaleSmoothLocalProperty_comp_of_isEtaleSmoothLocal · AlgebraicGeometry.Stack.hasEtaleSmoothLocalProperty_snd_of_isTwoFibreProduct_of_isStableUnderBaseChange · AlgebraicGeometry.Stack.hasEtaleSmoothLocalProperty_baseChange

Section101.35 Étale morphisms #

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

Tag 0CIL, a definition

Tag 0CIL in the Stacks Project.

AlgebraicGeometry.Stack.IsEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleSmoothLocalMorphism.lean, line 228.

Stacks 0CIL. A 1-morphism of algebraic stacks over S is étale when it is Deligne–Mumford and its universal étale-smooth diagram tests are étale morphisms of algebraic spaces, in the sense of AlgebraicGeometry.Space.IsEtale (Stacks 03FR).

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

Tag 0CIM, a lemma

Tag 0CIM in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isEtale_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleMorphismComp.lean, line 66.

Stacks 0CIM. The composite of two étale 1-morphisms of algebraic stacks over S is étale, in the sense of Stacks 0CIL: it is Deligne–Mumford and passes the universal étale-smooth diagram test at étaleness of morphisms of algebraic spaces.

This is Stacks 0CIH for the property AlgebraicGeometry.Space.IsEtale, which is étale-smooth local on the source-and-target (Stacks 0CG3) and stable under composition (Stacks 0465).

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

AlgebraicGeometry.Stack.AlgebraicStacks.isDM_comp_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleMorphismPermanence.lean, line 94. The attribute's comment: “the Deligne–Mumford conjunct of the conclusion”.

The Deligne–Mumford conjunct of Stacks 0CIM. A composite of two étale 1-morphisms of algebraic stacks over S is Deligne–Mumford.

Étaleness of Stacks 0CIL contains the Deligne–Mumford condition of Stacks 04YW, and that condition is stable under composition by Stacks 050K.

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

Tag 0CIN, a lemma

Tag 0CIN in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isEtale_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleMorphismBaseChange.lean, line 116.

Stacks 0CIN. A base change of an étale 1-morphism of algebraic stacks over S is étale: if f : 𝒳 ⟶ 𝒴 is étale and Q is any 2-fibre product of a cospan (g : 𝒴' ⟶ 𝒴, f), then the projection Q.fst : Q.pt ⟶ 𝒴' is étale, both conjuncts of Stacks 0CIL included.

The diagram of condition (2) of Stacks 0CIF for the Deligne–Mumford f is cut out by the surjective étale presentation of Stacks 0CIA, part (2), whose input, the substantial direction of Stacks 06N3, is AlgebraicGeometry.Stack.existsEtalePresentationOfIsAbsolutelyDM.

theorem isEtale_baseChange {𝒳 𝒴 𝒴' : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (Q : Bicategory.TwoCommSq g f) (hQ : Bicategory.IsTwoFibreProduct Q)
    (hf : IsEtale B S hS f) :
    IsEtale B S hS Q.fst

AlgebraicGeometry.Stack.AlgebraicStacks.isDM_baseChange_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleMorphismPermanence.lean, line 109. The attribute's comment: “the Deligne–Mumford conjunct of the conclusion”.

The Deligne–Mumford conjunct of Stacks 0CIN. The projection to 𝒴' of any 2-fibre product of a cospan (g : 𝒴' ⟶ 𝒴, f : 𝒳 ⟶ 𝒴) of 1-morphisms of algebraic stacks over S is Deligne–Mumford as soon as f is étale.

Étaleness of Stacks 0CIL contains the Deligne–Mumford condition of Stacks 04YW, and that condition is inherited by base changes by Stacks 050F; a 2-fibre product of (g, f) is one of (f, g) with its two legs exchanged (Stacks 003Q), which turns the projection Q.fst into the second projection that Stacks 050F speaks about.

theorem isDM_baseChange_of_isEtale {𝒳 𝒴 𝒴' : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (Q : Bicategory.TwoCommSq g f) (hQ : Bicategory.IsTwoFibreProduct Q)
    (hf : Stack.IsEtale B S hS f) :
    Stack.IsDM B S hS Q.fst

Tag 0CIP, a lemma

Tag 0CIP in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isEtale_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleOpenImmersion.lean, line 155.

An open immersion of algebraic stacks over S is étale in the sense of Stacks 0CIL.

theorem isEtale_of_isOpenImmersion (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicStacks.IsOpenImmersion B S hS f) :
    Stack.IsEtale B S hS f

Tag 0CIQ, a lemma

Tag 0CIQ in the Stacks Project.

AlgebraicGeometry.Stack.isEtale_of_etaleOnEveryAlgebraicSpaceDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleAlgebraicSpaceCriterion.lean, line 110. The attribute's comment: “the implication (2) => (1)”.

A Deligne–Mumford 1-morphism of algebraic stacks whose every algebraic-space diagram with étale comparisons has étale top horizontal morphism is étale.

theorem isEtale_of_etaleOnEveryAlgebraicSpaceDiagram
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴}
    (hf : EtaleOnEveryAlgebraicSpaceDiagram B S hS f) : IsEtale B S hS f

AlgebraicGeometry.Stack.isDM_of_hasEtaleAlgebraicSpaceCoverAfterFppfBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleAlgebraicSpaceCriterion.lean, line 144. The attribute's comment: “the Deligne-Mumford half of the implication (3) => (1), for a site containing the terminal scheme”.

If the big fppf site contains the terminal scheme, a 1-morphism f of algebraic stacks satisfying AlgebraicGeometry.Stack.HasEtaleAlgebraicSpaceCoverAfterFppfBaseChange is Deligne–Mumford.

theorem isDM_of_hasEtaleAlgebraicSpaceCoverAfterFppfBaseChange
    (hZ : B.Contains (⊤_ Scheme.{u}))
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴}
    (hf : HasEtaleAlgebraicSpaceCoverAfterFppfBaseChange B S hS f) : IsDM B S hS f

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

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

f is étale, AlgebraicGeometry.Stack.IsEtale (Stacks 0CIL);

f is Deligne–Mumford and for every V ⟶ 𝒴 with V an algebraic space and every étale U ⟶ V ×_𝒴 𝒳 with U an algebraic space, U ⟶ V is étale, AlgebraicGeometry.Stack.EtaleOnEveryAlgebraicSpaceDiagram;

there are a surjective, flat, locally finitely presented W ⟶ 𝒴 with W an algebraic space and a surjective étale T ⟶ W ×_𝒴 𝒳 with T an algebraic space such that T ⟶ W is étale, AlgebraicGeometry.Stack.HasEtaleAlgebraicSpaceCoverAfterFppfBaseChange.

theorem isEtale_tfae_algebraicSpaceCharts
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    List.TFAE [IsEtale B S hS f, EtaleOnEveryAlgebraicSpaceDiagram B S hS f,
      HasEtaleAlgebraicSpaceCoverAfterFppfBaseChange B S hS f]

Tag 0CIR, a lemma

Tag 0CIR in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isEtale_of_isEtale_over_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleMorphismBetweenEtaleStacks.lean, line 52.

Stacks 0CIR. Let 𝒳 and 𝒴 be algebraic stacks étale over an algebraic stack 𝒵, with structure 1-morphisms p : 𝒳 ⟶ 𝒵 and q : 𝒴 ⟶ 𝒵. Any 1-morphism f : 𝒳 ⟶ 𝒴 over 𝒵, i.e. with a 2-isomorphism η : p ≅ f ≫ q, is étale in the sense of Stacks 0CIL: Deligne–Mumford, and étale on every diagram of its universal étale-smooth test.

This is AlgebraicGeometry.Stack.isEtale_of_isEtale_over_base_of_isDeligneMumfordStack_twoFibreProduct with its étale charts supplied by Stacks 0CIA, part (2), Stack.AlgebraicStacks.isDeligneMumfordStack_twoFibreProduct_of_isDM_algebraicSpace.

theorem isEtale_of_isEtale_over_base {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (p : 𝒳 ⟶ 𝒵) (q : 𝒴 ⟶ 𝒵) (η : p ≅ f ≫ q)
    (hp : Stack.IsEtale B S hS p) (hq : Stack.IsEtale B S hS q) : Stack.IsEtale B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isDM_of_isEtale_over_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationCancellation.lean, line 191. The attribute's comment: “the Deligne-Mumford conjunct of the conclusion: a morphism between two stacks etale over a base is DM. The remaining conjunct of Tag 0CIL, the universal etale-smooth diagram condition, is not proved here”.

The Deligne–Mumford conjunct of Stacks 0CIR. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over 𝒵 whose structural 1-morphism p : 𝒳 ⟶ 𝒵 is étale is Deligne–Mumford.

Being over 𝒵 means p ≅ f ≫ q, so f ≫ q is Deligne–Mumford because p is étale, and Stacks 050M, part (1), cancels the second factor.

theorem isDM_of_isEtale_over_base {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (p : 𝒳 ⟶ 𝒵) (q : 𝒴 ⟶ 𝒵) (η : p ≅ f ≫ q)
    (hp : Stack.IsEtale B S hS p) : Stack.IsDM B S hS f

Sources

Section101.36 Unramified morphisms #

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

Tag 0CIT, a definition

Tag 0CIT in the Stacks Project.

AlgebraicGeometry.Stack.IsUnramified, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleSmoothLocalMorphism.lean, line 218.

Stacks 0CIT. A 1-morphism of algebraic stacks over S is unramified when it is Deligne–Mumford and its universal étale-smooth diagram tests are unramified morphisms of algebraic spaces, in the sense of AlgebraicGeometry.Space.IsUnramified (Stacks 03ZH, part (1)).

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

Tag 0CIU, a lemma

Tag 0CIU in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isUnramified_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedMorphismComp.lean, line 56.

Stacks 0CIU. The composition of unramified 1-morphisms of algebraic stacks over S is unramified: for f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 unramified, so is f ≫ g.

This is Stacks 0CIH at unramifiedness of morphisms of algebraic spaces, which is étale-smooth local on the source-and-target by Stacks 0CG3 and stable under composition by Stacks 03ZI.

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

AlgebraicGeometry.Stack.isUnramified_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedMorphismPermanence.lean, line 100. The attribute's comment: “with the substantial direction of Stacks 06N3 as the explicit hypothesis hForward (the structure theorem behind it, Stacks 06MD, 06N0, 06N2, 06G2, 06G3, is absent from the library); it is inherited from Stacks 0CIH, where it enters only through Stacks 0CIA”.

Stacks 0CIU. A composite of unramified 1-morphisms of algebraic stacks over S is unramified.

This is Stacks 0CIH at unramifiedness of morphisms of algebraic spaces: that property is étale-smooth local on the source-and-target by the unramified entry of Stacks 0CG3 and stable under composition by Stacks 03ZI, and unramifiedness of a 1-morphism of algebraic stacks is exactly the property of Deligne–Mumford 1-morphisms that Stacks 0CIG induces from it.

theorem isUnramified_comp
    (hT : B.Contains (⊤_ Scheme.{u}))
    (hForward : ExistsEtalePresentationOfIsAbsolutelyDM.{u, w} B S hS hT)
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsUnramified B S hS f) (hg : IsUnramified B S hS g) :
    IsUnramified B S hS (f ≫ g)

Tag 0CIV, a lemma

Tag 0CIV in the Stacks Project.

AlgebraicGeometry.Stack.isUnramified_baseChange_of_isUnramifiedOnEveryEtaleDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedBaseChange.lean, line 98. The attribute's comment: “unconditional: f is unramified in the sense of Stacks 0CIT and R is an arbitrary 2-fibre product of (g, f); the route through condition (2) of Stacks 0CIY is internal to the proof”.

A base change of an unramified 1-morphism of algebraic stacks over S is unramified: if f : 𝒳 ⟶ 𝒴 is unramified, g : 𝒴' ⟶ 𝒴 is any 1-morphism and R is any 2-fibre product of (g, f), then the projection R.fst : R.pt ⟶ 𝒴' is unramified in the sense of Stacks 0CIT.

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

AlgebraicGeometry.Stack.isUnramified_snd_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedBaseChange.lean, line 110. The attribute's comment: “unconditional, for a 2-fibre product of (f, g), the base change being its second projection R.snd”.

If f : 𝒳 ⟶ 𝒴 is unramified, g : 𝒴' ⟶ 𝒴 is any 1-morphism and R is any 2-fibre product of (f, g), then the projection R.snd : R.pt ⟶ 𝒴' is unramified in the sense of Stacks 0CIT.

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

AlgebraicGeometry.Stack.isUnramified_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedMorphismPermanence.lean, line 125. The attribute's comment: “for the canonical 2-fibre product square of Stacks 003Q, which is the shape the Stacks 0CII is stated at, and with the substantial direction of Stacks 06N3 as the explicit hypothesis hForward (the structure theorem behind it, Stacks 06MD, 06N0, 06N2, 06G2, 06G3, is absent from the library); both are inherited from Stacks 0CII, where hForward enters only through Stacks 0CIA”.

Stacks 0CIV. The base change of an unramified 1-morphism of algebraic stacks over S along an arbitrary 1-morphism is unramified: for f : 𝒳 ⟶ 𝒴 unramified and g : 𝒵 ⟶ 𝒴 arbitrary, the second projection of the canonical 2-fibre product square of (f, g) — the base change of f over 𝒵 — is unramified.

This is Stacks 0CII at unramifiedness of morphisms of algebraic spaces: that property is étale-smooth local on the source-and-target by the unramified entry of Stacks 0CG3 and stable under base change by Stacks 03ZJ, and unramifiedness of a 1-morphism of algebraic stacks is exactly the property of Deligne–Mumford 1-morphisms that Stacks 0CIG induces from it.

theorem isUnramified_baseChange
    (hT : B.Contains (⊤_ Scheme.{u}))
    (hForward : ExistsEtalePresentationOfIsAbsolutelyDM.{u, w} B S hS hT)
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (hf : IsUnramified B S hS f) :
    IsUnramified B S hS (AlgebraicStacks.twoFibreProductSquare B S hS f g).snd

Tag 0CIW, a lemma

Tag 0CIW in the Stacks Project.

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

An étale 1-morphism of algebraic stacks over S is unramified.

theorem isUnramified_of_isEtale {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴}
    (hf : IsEtale B S hS f) : IsUnramified B S hS f

Tag 0CIX, a lemma

Tag 0CIX in the Stacks Project.

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

Stacks 0CIX. An immersion of algebraic stacks over S, in the sense of Stacks 04YL, part (3), is unramified in the sense of Stacks 0CIT.

theorem isUnramified_of_isImmersion (j : 𝒵 ⟶ 𝒳) (hj : IsImmersion B S hS j) :
    Stack.IsUnramified B S hS j

Tag 0CIY, a lemma

Tag 0CIY in the Stacks Project.

AlgebraicGeometry.Stack.isUnramified_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedCharacterizationTFAE.lean, line 52.

Stacks 0CIY. For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S the following are equivalent: 1. f is unramified (Stacks 0CIT); 2. f is DM, and for every algebraic space V with a 1-morphism V ⟶ 𝒴 and every algebraic space U with an étale 1-morphism U ⟶ V ×_𝒴 𝒳, the morphism U ⟶ V is unramified; 3. there are an algebraic space W with a surjective, flat, locally finitely presented 1-morphism W ⟶ 𝒴 and an algebraic space T with a surjective étale 1-morphism T ⟶ 𝒳 ×_𝒴 W such that T ⟶ W is unramified.

theorem isUnramified_tfae {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    [IsUnramified B S hS f, IsUnramifiedOnEveryEtaleDiagram.{u, w} B S hS f,
      HasUnramifiedEtalePresentationOverFlatCover.{u, w} B S hS f].TFAE

AlgebraicGeometry.Stack.isUnramified_of_isUnramifiedOnEveryEtaleDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedEtaleDiagram.lean, line 113. The attribute's comment: “the implication (2) => (1)”.

Stacks 0CIY, the implication (2) ⇒ (1). A Deligne–Mumford 1-morphism of algebraic stacks over S whose every étale diagram of algebraic spaces has unramified top horizontal morphism is unramified in the sense of Stacks 0CIT.

theorem isUnramified_of_isUnramifiedOnEveryEtaleDiagram
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴}
    (hf : IsUnramifiedOnEveryEtaleDiagram.{u, w} B S hS f) :
    IsUnramified B S hS f

AlgebraicGeometry.Stack.isUnramifiedOnEveryEtaleDiagram_of_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedEtaleDiagramForward.lean, line 86. The attribute's comment: “the implication (1) => (2)”.

Stacks 0CIY, the implication (1) ⇒ (2). An unramified 1-morphism of algebraic stacks is DM and every étale diagram of algebraic spaces over it has unramified top horizontal morphism.

theorem isUnramifiedOnEveryEtaleDiagram_of_isUnramified
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴} (hf : IsUnramified B S hS f) :
    IsUnramifiedOnEveryEtaleDiagram.{u, w} B S hS f

AlgebraicGeometry.Stack.isDM_of_surjectiveEtalePresentation_flatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedFlatPresentation.lean, line 111. The attribute's comment: “the Deligne-Mumford condition on f, which is the first conjunct of each of parts (1) and (2), from part (3); the unramifiedness of T -> W asserted by part (3) is not needed for it, and the easy direction of Stacks 06N3 that the source cites is taken in the form Stacks 06MB part (1), whose absolute Deligne-Mumford conclusion asks the big site to contain the terminal scheme”.

Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S, let W be an algebraic space with a surjective, flat, locally-of-finite-presentation 1-morphism c : W ⟶ 𝒴, and let the 2-fibre product 𝒳 ×_𝒴 W admit a surjective étale 1-morphism from an algebraic space T. Then f is Deligne–Mumford.

theorem isDM_of_surjectiveEtalePresentation_flatBaseChange
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hW : IsAlgebraicSpace B S hS W)
    (c : algebraicSpaceStack.{u, w} B S hS W hW ⟶ 𝒴)
    (hcSurj : IsSurjective B S hS c)
    (hcFlat : AlgebraicStacks.IsFlat B S hS c)
    (hcLfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS c)
    (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hT : IsAlgebraicSpace B S hS T)
    (t : algebraicSpaceStack.{u, w} B S hS T hT ⟶
      (twoFibreProductSquareAlgebraicStacks B S hS f c).pt)
    (htSurj : IsSurjective B S hS t)
    (htEt : IsRelativelyEtale B S hS t.hom) :
    IsDM B S hS f

Tag 0H2Z, a lemma

Tag 0H2Z in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyQuasiFinite_of_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedIsLocallyQuasiFinite.lean, line 253.

Stacks 0H2Z. An unramified 1-morphism of algebraic stacks over S (Stacks 0CIT) is locally quasi-finite (Stacks 06PU): it is quasi-DM, locally of finite type, and its fibre over every field-valued point of the target has discrete space of points.

The three conjuncts are AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_of_isUnramified, the existential smooth-diagram test AlgebraicGeometry.Stack.AlgebraicStacks.hasPropertyOnSomeSmoothDiagram_of_isUnramified at the diagram AlgebraicGeometry.Stack.hasSurjectiveEtaleSmoothDiagram_of_isDM, and AlgebraicGeometry.Stack.discreteTopology_points_fibre_of_isUnramified.

theorem isLocallyQuasiFinite_of_isUnramified
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : Stack.IsUnramified B S hS f) :
    IsLocallyQuasiFinite B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_of_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedLocallyQuasiFinite.lean, line 121. The attribute's comment: “the quasi-DM conjunct of local quasi-finiteness, unconditionally. The local finite type conjunct is isLocallyOfFiniteType_of_isUnramified; the field-valued-fibre conjunct is NOT carried”.

The quasi-DM conjunct of Stacks 0H2Z. An unramified 1-morphism of algebraic stacks over S is quasi-DM, with a representable relative diagonal.

Unramifiedness in the sense of Stacks 0CIT contains the Deligne–Mumford condition, and a Deligne–Mumford 1-morphism is quasi-DM by Stacks 050E, part (2); the relative diagonal of a 1-morphism of algebraic stacks is always representable by algebraic spaces.

theorem isQuasiDM_of_isUnramified {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} {f : 𝒳 ⟶ 𝒴}
    (hf : Stack.IsUnramified B S hS f) :
    IsQuasiDMWithRepresentableDiagonal B S hS f

Tag 0CIZ, a lemma

Tag 0CIZ in the Stacks Project.

AlgebraicGeometry.Stack.isUnramified_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedPermanence.lean, line 145. The attribute's comment: “carrying as a hypothesis the two nested surjective etale presentations that the source obtains from Stacks 0CIA, which this library does not have because Stacks 06N3 is not proved; once they are given, the Deligne-Mumford hypothesis on the second factor is not used”.

Stacks 0CIZ. Let f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 be 1-morphisms of algebraic stacks over S. If f ≫ g is unramified, then f is unramified.

f is Deligne–Mumford by Stacks 050M part (1). For the étale-smooth diagram test, the nested presentations supply a diagram over f extending to one over f ≫ g; the extended diagram's top horizontal morphism is unramified, hence so is the one over f by Stacks 06G6.

theorem isUnramified_of_comp {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsUnramified B S hS (f ≫ g))
    (hdata : HasSurjectiveEtaleSmoothDiagramOver.{u, w} B S hS f g) :
    IsUnramified B S hS f

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

Stacks 0CIZ. Let f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 be 1-morphisms of algebraic stacks over S. If f ≫ g is unramified and g is Deligne–Mumford, then f is unramified.

f is Deligne–Mumford by Stacks 050M. Choose a surjective smooth W ⟶ 𝒵, a surjective étale V ⟶ 𝒴 ×_𝒵 W and a surjective étale U ⟶ 𝒳 ×_𝒴 V, the last two by Stacks 0CIA (the second because g is Deligne–Mumford, the third because f is); then U ⟶ W is unramified, and U ⟶ V is unramified by Stacks 06G6.

theorem isUnramified_of_comp_of_isDM {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hfg : IsUnramified B S hS (f ≫ g)) (hg : IsDM B S hS g) :
    IsUnramified B S hS f

Tag 0CJ0, a lemma

Tag 0CJ0 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isUnramified_iff_isLocallyOfFiniteType_and_isEtale_relativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedDiagonalCriterion.lean, line 234. The attribute's comment: “both implications: unramified iff locally of finite type with etale diagonal”.

Stacks 0CJ0. A 1-morphism of algebraic stacks over S admitting a diagram of algebraic spaces as in AlgebraicGeometry.Stack.HasDiagonalDescentChart is unramified exactly when it is locally of finite type and its relative diagonal is étale.

Unramifiedness and local finite type are tested on the diagram's top morphism h of algebraic spaces, and étaleness of the relative diagonal is tested on the relative diagonal of h; the equivalence is then Stacks 05W1. Deligne–Mumfordness in the converse direction comes from étaleness of the relative diagonal, étale morphisms of algebraic spaces being unramified by Stacks 06CR.

theorem isUnramified_iff_isLocallyOfFiniteType_and_isEtale_relativeDiagonal
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hchart : Stack.HasDiagonalDescentChart.{u, w} B S hS f) :
    Stack.IsUnramified B S hS f ↔
      (IsLocallyOfFiniteType B S hS f ∧
        Stack.IsEtale B S hS (relativeDiagonal B S hS f))

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

Stacks 0CJ0. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is unramified if and only if it is locally of finite type and its relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is étale.

The implication (2) ⇒ (1) is isUnramified_of_isLocallyOfFiniteType_of_isEtale_relativeDiagonal; (1) ⇒ (2) is isLocallyOfFiniteType_and_isEtale_relativeDiagonal_of_isUnramified_of_etalePresentation at the structure theorem of Stacks 06N3, AlgebraicGeometry.Stack.existsEtalePresentationOfIsAbsolutelyDM, through which Stacks 0CIA is available.

theorem isUnramified_iff_isLocallyOfFiniteType_isEtale_relativeDiagonal
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    Stack.IsUnramified B S hS f ↔
      (IsLocallyOfFiniteType B S hS f ∧ Stack.IsEtale B S hS (relativeDiagonal B S hS f))

Tag 0CJ1, a lemma

Tag 0CJ1 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isEtale_of_isLocallyOfFinitePresentation_of_isFlat_of_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleFlatUnramifiedCriterion.lean, line 241. The attribute's comment: “part (2) implies part (1)”.

Stacks 0CJ1, (2) ⇒ (1). A 1-morphism of algebraic stacks over S which is locally of finite presentation, flat and unramified is étale. No diagram has to be supplied.

Deligne–Mumfordness is part of unramifiedness. For the universal étale-smooth test, take a diagram it offers: its right leg is smooth, its left leg is smooth by AlgebraicGeometry.Stack.isRelativelySmooth_of_etaleSmoothDiagram and its comparisons are smooth because they are étale, so the universal smooth test of Stacks 06FM applies to it as well. That gives local finite presentation of its top morphism directly, and flatness after Stacks 06FM turns the existential test of Stacks 06PW into the universal one; unramifiedness is the hypothesis at that diagram. Stacks 06LU concludes.

theorem isEtale_of_isLocallyOfFinitePresentation_of_isFlat_of_isUnramified
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hlfp : IsLocallyOfFinitePresentation B S hS f) (hflat : IsFlat B S hS f)
    (hunr : Stack.IsUnramified B S hS f) :
    Stack.IsEtale B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isEtale_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleFlatUnramifiedTFAE.lean, line 66.

Stacks 0CJ1. For a 1-morphism f of algebraic stacks over S the following are equivalent: f is étale; f is locally of finite presentation, flat and unramified; f is locally of finite presentation, flat and has étale relative diagonal.

(2) ⇔ (3) is Stacks 0CJ0 together with Stacks 06Q5; (2) ⇒ (1) is Stacks 06LU on the top morphism of an étale-smooth diagram; (1) ⇒ (2) uses the diagram Stacks 0CIA provides for the Deligne–Mumford 1-morphism f.

theorem isEtale_tfae {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    List.TFAE
      [Stack.IsEtale B S hS f,
        IsLocallyOfFinitePresentation B S hS f ∧ IsFlat B S hS f ∧ Stack.IsUnramified B S hS f,
        IsLocallyOfFinitePresentation B S hS f ∧ IsFlat B S hS f ∧
          Stack.IsEtale B S hS (relativeDiagonal B S hS f)]

Sources

LeanAlgebraicGeometry.Stack.IsUnramified · AlgebraicGeometry.Stack.AlgebraicStacks.isUnramified_comp · AlgebraicGeometry.Stack.isUnramified_comp · AlgebraicGeometry.Stack.isUnramified_baseChange_of_isUnramifiedOnEveryEtaleDiagram · AlgebraicGeometry.Stack.isUnramified_snd_of_isTwoFibreProduct · AlgebraicGeometry.Stack.isUnramified_baseChange · AlgebraicGeometry.Stack.isUnramified_of_isEtale · AlgebraicGeometry.Stack.AlgebraicStacks.isUnramified_of_isImmersion

Section101.37 Proper morphisms #

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

Tag 0CL5, a definition

Tag 0CL5 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsProper, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ProperAlgebraicStack.lean, line 111.

Stacks 0CL5. A 1-morphism of algebraic stacks over S is proper when it is separated (Stacks 04YW), of finite type (Stacks 06FS, part (2)) and universally closed (Stacks 0513, part (2)).

This is properness for an arbitrary 1-morphism of algebraic stacks; the Stacks 04XB relative notion for a 1-morphism representable by algebraic spaces is AlgebraicGeometry.Stack.IsProper.

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

Tag 0CL6, a lemma

Tag 0CL6 in the Stacks Project.

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

Stacks 0CL6. A base change of a proper 1-morphism of algebraic stacks over S is proper: if f : 𝒳 ⟶ 𝒴 is proper and P is any 2-fibre product square of the cospan (g, f) for some g : 𝒴' ⟶ 𝒴, then the projection P.fst — the base change of f along g — is proper.

Properness is separatedness, finite type and universal closedness (Stacks 0CL5), and the three conjuncts base change by Stacks 050F, Stacks 06FU and Stacks 0514 respectively, which is the source's own proof.

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

Tag 0CL7, a lemma

Tag 0CL7 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isProper_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ProperCompositionAlgebraicStack.lean, line 78.

Stacks 0CL7. A composition of proper 1-morphisms of algebraic stacks over S is proper: if f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 are proper, then so is f ≫ g.

Properness is separatedness, finite type and universal closedness (Stacks 0CL5), and the three conjuncts compose by Stacks 050K, Stacks 06FT and Stacks 0515 respectively, which is the source's own proof.

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

Tag 0CL8, a lemma

Tag 0CL8 in the Stacks Project.

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

Stacks 0CL8. A closed immersion of algebraic stacks over S is a proper 1-morphism of algebraic stacks.

Properness is the conjunction of Stacks 0CL5, and its three conjuncts are discharged in turn: separatedness through monomorphy (Stacks 0504 and 06MY), local finite type by Stacks 06FV for immersions, quasi-compactness by Stacks 0CL1, and universal closedness from stability of closed immersions under base change (Stacks 045C) together with their closedness on points (Stacks 0H20).

theorem isProper_of_isClosedImmersion (f : 𝒳 ⟶ 𝒴) (hf : IsClosedImmersion B S hS f) :
    IsProper B S hS f

Tag 0CPT, a lemma

Tag 0CPT in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_of_comp_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ProperCancellation.lean, line 146. The attribute's comment: “part (1): universal closedness”. References: EGA II (5.4.9), “5.4.3 univ. closed”.

Stacks 0CPT, part (1). If a composite of 1-morphisms of algebraic stacks over S is universally closed and its second factor is separated, then its first factor is universally closed.

f is 2-isomorphic to its graph over 𝒵 followed by the second projection of the canonical 2-fibre product of the cospan (f ≫ g, g). The graph is universally closed because g is separated, the projection is the base change of f ≫ g along g and so is universally closed by Stacks 0514, and Stacks 0515 composes them.

theorem universallyClosed_of_comp_of_isSeparated (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : UniversallyClosed B S hS (f ≫ g)) (hg : IsSeparated B S hS g) :
    UniversallyClosed B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_range_of_comp_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ProperCancellation.lean, line 163. The attribute's comment: “part (1): closed image”.

Stacks 0CPT, part (1). Under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_of_comp_of_isSeparated the image of |𝒳| in |𝒴| is closed for the topology of Stacks 04XL.

theorem isClosed_range_of_comp_of_isSeparated (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : UniversallyClosed B S hS (f ≫ g)) (hg : IsSeparated B S hS g) :
    @_root_.IsClosed _ (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.isProper_of_comp_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ProperCancellation.lean, line 182. The attribute's comment: “part (2): properness”.

Stacks 0CPT, part (2). If a composite of 1-morphisms of algebraic stacks over S is proper and its second factor is separated, then its first factor is proper.

Properness of Stacks 0CL5 is separatedness, finite type and universal closedness. The first is Stacks 050M part (3), whose hypothesis on Δ_g is separatedness in the sense of Stacks 04XB and follows from the properness of Δ_g that separatedness of g asserts. Finite type is local finite type, which cancels outright by Stacks 06U9, together with quasi-compactness, which cancels against the quasi-separatedness of g by Stacks 050Y. Universal closedness is part (1).

theorem isProper_of_comp_of_isSeparated (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsProper B S hS (f ≫ g)) (hg : IsSeparated B S hS g) :
    IsProper B S hS f

Tag 0CQK, a lemma

Tag 0CQK in the Stacks Project.

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

Stacks 0CQK, universal closedness of the image. If the composite f ≫ q of 1-morphisms of algebraic stacks over S is universally closed and f is surjective, then q is universally closed.

theorem universallyClosed_of_surjective_comp
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (q : 𝒴 ⟶ 𝒵)
    (hp : UniversallyClosed B S hS (f ≫ q)) (hf : Stack.IsSurjective B S hS f) :
    UniversallyClosed B S hS q

AlgebraicGeometry.Stack.AlgebraicStacks.isProper_of_surjective_universallyClosed_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ProperImageAlgebraicStack.lean, line 139. The attribute's comment: “properness of the image”. References: EGA II (5.4.3), “(ii)”.

Stacks 0CQK, properness of the image. If the composite f ≫ q of 1-morphisms of algebraic stacks over S is universally closed, f is surjective and q is separated and of finite type, then q is proper.

theorem isProper_of_surjective_universallyClosed_comp
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (q : 𝒴 ⟶ 𝒵)
    (hp : UniversallyClosed B S hS (f ≫ q)) (hf : Stack.IsSurjective B S hS f)
    (hsep : IsSeparated B S hS q) (hft : IsFiniteType B S hS q) :
    IsProper B S hS q

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

101.23 Locally quasi-finite… to 101.37 Proper morphisms

Section101.23 Locally quasi-finite morphisms#

Tag 06UA, a lemma

Tag 06PU, a definition

Tag 06UB, a lemma

Tag 06UC, a lemma

Tag 06UD, a lemma

Tag 06UE, a lemma

Tag 06UF, a lemma

Tag 06UG, a lemma

Sources

Section101.24 Quasi-finite morphisms#

Tag 0G2M, a definition

Tag 0G2N, a lemma

Tag 0G2P, a lemma

Tag 0G2Q, a lemma

Sources

Section101.25 Flat morphisms#

Tag 06PW, a definition

Tag 06PX, a lemma

Tag 06PY, a lemma

Tag 06PZ, a lemma

Tag 06Q0, a lemma

Tag 0DN5, a lemma

Sources

Section101.26 Flat at a point#

Tag 0CIC, a lemma

Tag 0CID, a definition

Sources

Section101.27 Morphisms of finite presentation#

Tag 06Q2, a definition

Tag 06Q3, a lemma

Tag 06Q4, a lemma

Tag 06Q5, a lemma

Tag 0DQJ, a lemma

Tag 06Q6, a lemma

Tag 0CMG, a lemma

Tag 06Q7, a lemma

Tag 0CPP, a lemma

Tag 0DN6, a lemma

Tag 06Q8, a lemma

Tag 06Q9, a lemma

Tag 06QA, a lemma

Tag 07AN, a lemma

Tag 06R7, a lemma

Tag 0DQK, a lemma

Tag 0CPQ, a lemma

Sources

Section101.28 Gerbes#

Tag 06QC, a definition

Tag 06QD, a lemma

Tag 06QE, a lemma

Tag 06R8, a lemma

Tag 06QF, a lemma

Tag 06QG, a lemma

Tag 06QH, a lemma

Tag 06QI, a lemma

Tag 06QJ, a proposition

Tag 0CPR, a lemma

Tag 0CPS, a proposition

Tag 06QK, a lemma

Tag 06R9, a lemma

Tag 0DQL, a lemma

Tag 06RA, a lemma

Sources

Section101.29 Stratification by gerbes#

Tag 06RC, a proposition

Tag 06RE, an example

Tag 06RF, a lemma

Tag 06RG, a remark

Sources

Section101.30 The topological space of an algebraic stack#

Tag 0DQN, a lemma

Tag 0DQP, a lemma

Tag 0DQQ, a lemma

Sources

Section101.31 Existence of residual gerbes#

Tag 06RD, a lemma

Tag 06UI, a lemma

Tag 0H22, a lemma

Section101.23 Locally quasi-finite morphisms #

Section101.24 Quasi-finite morphisms #

Section101.25 Flat morphisms #

Section101.26 Flat at a point #

Section101.27 Morphisms of finite presentation #

Section101.28 Gerbes #

Section101.29 Stratification by gerbes #

Section101.30 The topological space of an algebraic stack #

Section101.31 Existence of residual gerbes #

Section101.32 Étale local structure #

Section101.33 Smooth morphisms #

Section101.34 Types of morphisms étale-smooth local on source-and-target #

Section101.35 Étale morphisms #

Section101.36 Unramified morphisms #

Section101.37 Proper morphisms #