78.24 Explicit description of… to 78.29 Separation conditions

Section78.24 Explicit description of quotient stacks#

Section 78.24 of the Stacks Project, Tag 04MB. 1 tag here is carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 044X, a lemma

Tag 044X in the Stacks Project.

AlgebraicGeometry.Stack.essImage_toQuotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStack.lean, line 217. The attribute's comment: “part (1): local representatives”.

Every object of the quotient locally comes from the pointwise groupoid presentation: clause (2) of Stacks 02ZN for this witness, and part (1) of Stacks 044X.

theorem essImage_toQuotientStack
    (G : GroupoidInAlgebraicSpaces C S hS B)
    (U : BigFppfOver C S hS) (x : (quotientStack G).p.Fiber U) :
    ∃ R ∈ BigFppfOver.topology C S hS U,
      ∀ ⦃V : BigFppfOver C S hS⦄ ⦃f : V ⟶ U⦄, R.arrows f →
        (Functor.fiberFunctorOfCompEq (isFibredOneMorphism_toQuotientStack G).comp_eq V).essImage
          (Functor.pullbackFiber (quotientStack G).p x f)

AlgebraicGeometry.Stack.fullyFaithful_fiberFunctor_toQuotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/FibreFullFaithfulness.lean, line 57. The attribute's comment: “part (2): transition arrows”.

Stacks 044X, part (2). A transition isomorphism between two objects of a fibre of the quotient stack that come from points of the object space is the image under π of a unique arrow of the arrow space: the functor induced by π on the fibre over any test object is fully faithful. This is Stacks 044V read through the identity map of the test object.

theorem fullyFaithful_fiberFunctor_toQuotientStack
    (G : GroupoidInAlgebraicSpaces C S hS B)
    (T : BigFppfOver C S hS) :
    Nonempty (Functor.fiberFunctorOfCompEq
      (isFibredOneMorphism_toQuotientStack G).comp_eq T).FullyFaithful

AlgebraicGeometry.Stack.presentingDescentFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/PresentingDescentData.lean, line 307. The attribute's comment: “parts (2) and (3): projection of presenting data”.

Stacks 044X, parts (2) and (3). The functor on descent data relative to a fixed covering of a test object induced by the canonical 1-morphism π : 𝒮_U ⟶ [U/R]: a system (u i, r i j) of points of the object space and arrows of the arrow space is carried to the descent datum of [U/R] whose local objects are the π (u i) and whose transition isomorphisms are the images π (r i j), conjugated by the canonical comparison between the chosen pullback of an image and the image of a chosen pullback. Part (3), that (u i, r i j) is a descent datum, is the hypothesis on the source; the content here is that its image is one for the quotient.

noncomputable def presentingDescentFunctor
    (G : GroupoidInAlgebraicSpaces C S hS B)
    {T : BigFppfOver C S hS} (𝒰 : PreZeroHypercover.{w} T) :
    Functor.FamilyDescentDatum (quotientPrestack G).p 𝒰 ⥤
      Functor.FamilyDescentDatum (quotientStack G).p 𝒰

AlgebraicGeometry.Stack.presentingDescentFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/PresentingDescentData.lean, line 401. The attribute's comment: “part (2): local components”.

Stacks 044X, part (2). The local objects of the projected descent datum are the images under π of the local points of the object space.

theorem presentingDescentFunctor_obj
    (G : GroupoidInAlgebraicSpaces C S hS B)
    {T : BigFppfOver C S hS} (𝒰 : PreZeroHypercover.{w} T)
    (D : Functor.FamilyDescentDatum (quotientPrestack G).p 𝒰)
    (i : 𝒰.I₀) :
    ((presentingDescentFunctor G 𝒰).obj D).obj i =
      (Functor.fiberFunctorOfCompEq
        (isFibredOneMorphism_toQuotientStack G).comp_eq
        (𝒰.X i)).obj (D.obj i)

AlgebraicGeometry.Stack.presentingDescentFunctor_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/PresentingDescentData.lean, line 416. The attribute's comment: “part (2): transition specification”.

Stacks 044X, part (2). The transition isomorphism of the projected descent datum on an overlap is the image under π of the arrow of the arrow space, conjugated by the canonical comparisons between the chosen pullbacks of the images and the images of the chosen pullbacks.

theorem presentingDescentFunctor_hom
    (G : GroupoidInAlgebraicSpaces C S hS B)
    {T : BigFppfOver C S hS} (𝒰 : PreZeroHypercover.{w} T)
    (D : Functor.FamilyDescentDatum (quotientPrestack G).p 𝒰)
    {W : BigFppfOver C S hS} (q : W ⟶ T)
    {i j : 𝒰.I₀} (a : W ⟶ 𝒰.X i) (b : W ⟶ 𝒰.X j)
    (ha : a ≫ 𝒰.f i = q) (hb : b ≫ 𝒰.f j = q) :
    HEq (((presentingDescentFunctor G 𝒰).obj D).hom q a b ha hb)
      (((isFibredOneMorphism_toQuotientStack G).mapPullbackFiberIso
        (D.obj i) a).hom ≫
      (Functor.fiberFunctorOfCompEq
        (isFibredOneMorphism_toQuotientStack G).comp_eq W).map
          (D.hom q a b ha hb) ≫
      ((isFibredOneMorphism_toQuotientStack G).mapPullbackFiberIso
        (D.obj j) b).inv)

AlgebraicGeometry.Stack.presentingDescentFunctor_map_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/PresentingDescentData.lean, line 436. The attribute's comment: “part (5): local arrows of the projected morphism”.

Stacks 044X, part (5). On morphisms the projection applies π to each local arrow of the arrow space.

theorem presentingDescentFunctor_map_hom
    (G : GroupoidInAlgebraicSpaces C S hS B)
    {T : BigFppfOver C S hS} (𝒰 : PreZeroHypercover.{w} T)
    {D E : Functor.FamilyDescentDatum (quotientPrestack G).p 𝒰}
    (f : D ⟶ E) (i : 𝒰.I₀) :
    HEq (((presentingDescentFunctor G 𝒰).map f).hom i)
      ((Functor.fiberFunctorOfCompEq
        (isFibredOneMorphism_toQuotientStack G).comp_eq
        (𝒰.X i)).map (f.hom i))

AlgebraicGeometry.Stack.exists_presentingDescentDatum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/PresentingDescentData.lean, line 712. The attribute's comment: “parts (1)–(3): local presenting descent datum”.

Stacks 044X, parts (1)–(3). Every object x of a fibre of the quotient stack is, after an fppf covering of the test object, the projection of a descent datum for the pointwise groupoid presentation: there is a covering 𝒰 indexed in the universe of the site, a system (u i, r i j) of points of the object space and arrows of the arrow space forming a descent datum for the presentation relative to 𝒰, and an isomorphism between the canonical descent datum of x and the projection of that system. The local isomorphisms f i ^* x ≅ π (u i) and their transition arrows are the components of that isomorphism.

theorem exists_presentingDescentDatum
    (G : GroupoidInAlgebraicSpaces C S hS B)
    (T : BigFppfOver C S hS)
    (x : (quotientStack G).p.Fiber T) :
    ∃ (𝒰 : PreZeroHypercover.{u} T)
      (_ : 𝒰.sieve₀ ∈ BigFppfOver.topology C S hS T)
      (D : Functor.FamilyDescentDatum (quotientPrestack G).p 𝒰),
      Nonempty (((Functor.toFamilyDescentDatum
        (quotientStack G).p 𝒰).obj x) ≅
          (presentingDescentFunctor G 𝒰).obj D)

AlgebraicGeometry.Stack.effective_presentingDescentDatum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/PresentingDescentData.lean, line 736. The attribute's comment: “part (4): effectivity”.

Stacks 044X, part (4). Every descent datum for the pointwise groupoid presentation relative to an fppf covering arises as in parts (1)–(3): its projection is the canonical descent datum of an object of the fibre of the quotient stack over the test object. This is the effectivity of descent data in the stack [U/R].

theorem effective_presentingDescentDatum
    (G : GroupoidInAlgebraicSpaces C S hS B)
    {T : BigFppfOver C S hS} (𝒰 : PreZeroHypercover.{w} T)
    (h𝒰 : 𝒰.sieve₀ ∈ BigFppfOver.topology C S hS T)
    (D : Functor.FamilyDescentDatum (quotientPrestack G).p 𝒰) :
    ∃ x : (quotientStack G).p.Fiber T,
      Nonempty (((Functor.toFamilyDescentDatum
        (quotientStack G).p 𝒰).obj x) ≅
          (presentingDescentFunctor G 𝒰).obj D)

AlgebraicGeometry.Stack.fullyFaithful_presentingDescentFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/PresentingDescentData.lean, line 754. The attribute's comment: “part (5): morphisms of presenting data”.

Stacks 044X, part (5). For a fixed covering the projection is fully faithful on descent data for the presentation: a morphism of the projected data is the image of a unique compatible family of arrows of the arrow space.

theorem fullyFaithful_presentingDescentFunctor
    (G : GroupoidInAlgebraicSpaces C S hS B)
    {T : BigFppfOver C S hS} (𝒰 : PreZeroHypercover.{w} T) :
    Nonempty (presentingDescentFunctor G 𝒰).FullyFaithful

AlgebraicGeometry.Stack.homEquiv_presentingDescentDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/PresentingDescentData.lean, line 796. The attribute's comment: “part (5): canonical bijection”.

Stacks 044X, part (5). The canonical bijection between the morphisms x ⟶ y of a fibre of the quotient stack and the morphisms of the descent data for the presentation that represent x and y, together with the equation that characterises it: the projection of the morphism of descent data is the canonical descent datum morphism of f, conjugated by the two representing isomorphisms.

noncomputable def homEquiv_presentingDescentDatum
    (G : GroupoidInAlgebraicSpaces C S hS B)
    {T : BigFppfOver C S hS} (𝒰 : PreZeroHypercover.{w} T)
    (h𝒰 : 𝒰.sieve₀ ∈ BigFppfOver.topology C S hS T)
    (x y : (quotientStack G).p.Fiber T)
    (D E : Functor.FamilyDescentDatum (quotientPrestack G).p 𝒰)
    (δ : (Functor.toFamilyDescentDatum (quotientStack G).p 𝒰).obj x ≅
      (presentingDescentFunctor G 𝒰).obj D)
    (ε : (Functor.toFamilyDescentDatum (quotientStack G).p 𝒰).obj y ≅
      (presentingDescentFunctor G 𝒰).obj E) :
    {e : (x ⟶ y) ≃ (D ⟶ E) //
      ∀ f, (presentingDescentFunctor G 𝒰).map (e f) = δ.inv ≫
        (Functor.toFamilyDescentDatum (quotientStack G).p 𝒰).map f ≫ ε.hom}

AlgebraicGeometry.Stack.presentingDescentFunctor_refinementIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/PresentingDescentData.lean, line 845. The attribute's comment: “part (6): refinement compatibility”.

Stacks 044X, part (6). The correspondence of parts (1)–(5) is compatible with refinement of the fppf covering: projecting a descent datum for the presentation and then pulling it back along a refinement is naturally isomorphic to pulling it back first and then projecting, and the isomorphism is natural in the descent datum, hence compatible with the bijection of part (5).

noncomputable def presentingDescentFunctor_refinementIso
    (G : GroupoidInAlgebraicSpaces C S hS B)
    {T : BigFppfOver C S hS}
    {𝒰 : PreZeroHypercover.{w} T} {𝒱 : PreZeroHypercover.{w} T}
    (Φ : 𝒱.HomOver 𝒰 (𝟙 T)) :
    presentingDescentFunctor G 𝒰 ⋙
        Functor.FamilyDescentDatum.pullFunctor (quotientStack G).p Φ ≅
      Functor.FamilyDescentDatum.pullFunctor (quotientPrestack G).p Φ ⋙
        presentingDescentFunctor G 𝒱
Sources
LeanAlgebraicGeometry.Stack.essImage_toQuotientStack · AlgebraicGeometry.Stack.fullyFaithful_fiberFunctor_toQuotientStack · AlgebraicGeometry.Stack.presentingDescentFunctor · AlgebraicGeometry.Stack.presentingDescentFunctor_obj · AlgebraicGeometry.Stack.presentingDescentFunctor_hom · AlgebraicGeometry.Stack.presentingDescentFunctor_map_hom · AlgebraicGeometry.Stack.exists_presentingDescentDatum · AlgebraicGeometry.Stack.effective_presentingDescentDatum

Section78.25 Restriction and quotient stacks#

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

Tag 046S, a lemma

Tag 046S in the Stacks Project.

AlgebraicGeometry.Stack.fullyFaithful_quotientStackMap_iff_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/FullFaithfulness.lean, line 370.

Stacks 046S. The induced morphism of quotient stacks [f] : [U/R] ⟶ [U'/R'] is fully faithful if and only if R is the restriction of R' along f : U ⟶ U', i.e. if and only if the square formed by the arrow map of f and the two source–target maps is cartesian.

public theorem fullyFaithful_quotientStackMap_iff_isPullback
    {G H : GroupoidInAlgebraicSpaces C S hS B}
    (f : GroupoidInAlgebraicSpaces.Hom G H) :
    Nonempty (quotientStackMap f).toFunctor.FullyFaithful ↔
      IsPullback f.toGroupoidHom.mapArrows
        (prod.lift G.toGroupoidInFunctors.source G.toGroupoidInFunctors.target)
        (prod.lift H.toGroupoidInFunctors.source H.toGroupoidInFunctors.target)
        (prod.map f.toGroupoidHom.mapObjects f.toGroupoidHom.mapObjects)
Tag 046T, a lemma

Tag 046T in the Stacks Project.

AlgebraicGeometry.Space.isLocallySurjective_source_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/RestrictionCoverings.lean, line 132. The attribute's comment: “surjective_object_map”.

Stacks 046T. A map on objects which is surjective as a map of fppf sheaves stays surjective after passing to the arrows of the target groupoid whose target lifts through it and taking their sources.

theorem isLocallySurjective_source_pullback_snd
    {C : BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S}
    {B : AlgebraicSpaces C S hS} {G H : GroupoidInAlgebraicSpaces C S hS B}
    (f : GroupoidInAlgebraicSpaces.Hom G H)
    (hf : Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS)
      f.toGroupoidHom.mapObjects) :
    Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS)
      (pullback.snd f.toGroupoidHom.mapObjects H.target.hom ≫ H.source.hom)

AlgebraicGeometry.Space.isLocallySurjective_source_pullback_of_isFppfCovering_mapObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/RestrictionCoverings.lean, line 162. The attribute's comment: “fppf_object_map”.

Stacks 046T. If the map on objects of a morphism of groupoids in algebraic spaces is an fppf covering, then every object of the target groupoid is fppf-locally the source of an arrow whose target lifts to the source groupoid.

theorem isLocallySurjective_source_pullback_of_isFppfCovering_mapObjects
    (C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
    (B : AlgebraicSpaces C S hS)
    (G H : GroupoidInAlgebraicSpaces C S hS B)
    (f : GroupoidInAlgebraicSpaces.Hom G H)
    (hf : IsFppfCovering C S hS (fun _ : PUnit => G.objects.obj)
      (fun _ => f.toGroupoidHom.mapObjects)) :
    Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS)
      (pullback.snd f.toGroupoidHom.mapObjects H.target.hom ≫ H.source.hom)

AlgebraicGeometry.Space.isLocallySurjective_source_pullback_of_isFppfCovering_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/RestrictionCoverings.lean, line 178. The attribute's comment: “fppf_saturation”.

Stacks 046T. If the arrows of the target groupoid whose target lifts to the source groupoid form an fppf covering of the object space of the target through their sources, then that saturation map is surjective as a map of fppf sheaves.

theorem isLocallySurjective_source_pullback_of_isFppfCovering_self
    {C : BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S}
    {B : AlgebraicSpaces C S hS} {G H : GroupoidInAlgebraicSpaces C S hS B}
    (f : GroupoidInAlgebraicSpaces.Hom G H)
    (hf : IsFppfCovering C S hS
      (fun _ : PUnit => pullback f.toGroupoidHom.mapObjects H.target.hom)
      (fun _ => pullback.snd f.toGroupoidHom.mapObjects H.target.hom ≫ H.source.hom)) :
    Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS)
      (pullback.snd f.toGroupoidHom.mapObjects H.target.hom ≫ H.source.hom)

AlgebraicGeometry.Stack.quotientStackMap_isEquivalenceOver_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/RestrictionCoverings.lean, line 496. The attribute's comment: “equivalence_criterion”.

Stacks 046T. The induced morphism of quotient stacks [f] : [U/R] ⟶ [U'/R'] is an equivalence over the big fppf site if and only if (1) (U, R, s, t, c) is the restriction of (U', R', s', t', c') along f : U ⟶ U', i.e. the square formed by the arrow map of f and the two source–target maps is cartesian, and (2) the saturation map U ×_{f, U', t'} R' ⟶ R' ⟶ U' is a surjection of fppf sheaves.

public theorem quotientStackMap_isEquivalenceOver_iff
    {G H : GroupoidInAlgebraicSpaces C S hS B}
    (f : GroupoidInAlgebraicSpaces.Hom G H) :
    Nonempty (Functor.IsEquivalenceOver (quotientStack G).p (quotientStack H).p
      (quotientStackMap f).toFunctor) ↔
      (IsPullback f.toGroupoidHom.mapArrows
          (prod.lift G.toGroupoidInFunctors.source G.toGroupoidInFunctors.target)
          (prod.lift H.toGroupoidInFunctors.source H.toGroupoidInFunctors.target)
          (prod.map f.toGroupoidHom.mapObjects f.toGroupoidHom.mapObjects) ∧
        Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS)
          ((GroupoidInAlgebraicSpaces.fiberProductSnd
              (ObjectProperty.homMk f.toGroupoidHom.mapObjects : G.objects ⟶ H.objects)
              H.target ≫ H.source).hom))
Tag 04ZN, a lemma

Tag 04ZN in the Stacks Project.

AlgebraicGeometry.Stack.isTwoFibreProduct_functorialitySquare_of_isPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/FunctorialityComparisonSurjectivity.lean, line 523.

Stacks 04ZN. Let φ : (U, R, s, t, c) ⟶ (U', R', s', t', c') be a morphism of groupoids in algebraic spaces over an algebraic space B over a scheme S of a big fppf site, and suppose the square formed by the two source maps,

R ---f---> R'
|          |
s          s'
v          v
U ---f---> U'

is cartesian. Then the square

𝒮_U ----π----> [U/R]
 |              |
𝒮_f            [φ]
 v              v
𝒮_{U'} --π'--> [U'/R']

of the projections of Stacks 044R, the induced 1-morphism of Stacks 046Q and the 1-morphism of Stacks 0458 is a 2-fibre product in the 2-category of stacks in groupoids over the big fppf site.

Both halves of the proof consume the cartesian source square and nothing else: AlgebraicGeometry.Stack.functorialityComparison_full for fullness of the comparison 1-morphism — and faithfulness is free — and AlgebraicGeometry.Stack.locallyEssSurjOnFibers_functorialityComparison for local essential surjectivity on fibres. The reduction of the 2-fibre product property to those two is AlgebraicGeometry.Stack.isTwoFibreProduct_functorialitySquare.

noncomputable def isTwoFibreProduct_functorialitySquare_of_isPullback (φ : Hom G G')
    (hφ : IsPullback φ.toGroupoidHom.mapArrows G.source.hom G'.source.hom
      φ.toGroupoidHom.mapObjects) :
    Bicategory.IsTwoFibreProduct (functorialitySquare φ)

AlgebraicGeometry.Stack.isTwoFibreProduct_presentationQuotientMapSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresentationQuotientMapSquare.lean, line 287. The attribute's comment: “in the 2-category of algebraic stacks, for a morphism into a presenting groupoid”.

The square of a morphism into a presenting groupoid is a 2-fibre product. Let 𝒳 be an algebraic stack over S presented by a smooth groupoid (U, R, s, t, c) (Stacks 04TI), and let φ : (U', R', s', t', c') ⟶ (U, R, s, t, c) be a morphism from a smooth groupoid in algebraic spaces whose square of source maps

R' --φ--> R
|s'       |s
v         v
U' --φ--> U

is cartesian. Then the square AlgebraicGeometry.Stack.presentationQuotientMapSquare

𝒮_{U'} ------> [U'/R']
  |               |
  v               v
𝒮_U   ------>     𝒳

is a 2-fibre product in the 2-category of algebraic stacks over S (Stacks 03YP).

noncomputable def isTwoFibreProduct_presentationQuotientMapSquare
    (hφ : IsPullback φ.toGroupoidHom.mapArrows G'.source.hom P.groupoid.source.hom
      φ.toGroupoidHom.mapObjects) :
    Bicategory.IsTwoFibreProduct (presentationQuotientMapSquare B S hS P hG' φ)
Sources
LeanAlgebraicGeometry.Stack.fullyFaithful_quotientStackMap_iff_isPullback · AlgebraicGeometry.Space.isLocallySurjective_source_pullback_snd · AlgebraicGeometry.Space.isLocallySurjective_source_pullback_of_isFppfCovering_mapObjects · AlgebraicGeometry.Space.isLocallySurjective_source_pullback_of_isFppfCovering_self · AlgebraicGeometry.Stack.quotientStackMap_isEquivalenceOver_iff · AlgebraicGeometry.Stack.isTwoFibreProduct_functorialitySquare_of_isPullback · AlgebraicGeometry.Stack.isTwoFibreProduct_presentationQuotientMapSquare

Section78.26 Inertia and quotient stacks#

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

Tag 06PB, a lemma

Tag 06PB in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.inertiaGroupoid, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/InertiaGroupoid.lean, line 890. The attribute's comment: “the groupoid (G, R', s', t', c')”.

The groupoid (G, R', s', t', c') in algebraic spaces over B built from a groupoid (U, R, s, t, c) in algebraic spaces over B: its object space is the stabilizer G/U, its arrow space is R' = R ×_{s, U} G, and its source, target and composition are the morphisms s', t' and c'.

noncomputable def inertiaGroupoid
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    GroupoidInAlgebraicSpaces C S hS B

AlgebraicGeometry.Stack.inertiaComparison_comp_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaQuotientStackComparison.lean, line 1373. The attribute's comment: “second assertion: the comparison [G/R'] ⟶ I_{[U/R]} is over the site”.

The comparison [G/R'] ⟶ ℐ_{[U/R]} composed with the structure functor of the inertia of [U/R] is the structure functor of [G/R']: it is a 1-morphism of categories over the big fppf site.

theorem inertiaComparison_comp_toBase (G : GroupoidInAlgebraicSpaces C S hS B) :
    (inertiaComparison G).toFunctor ⋙ RelativeInertia.toBase (quotientStack G).p =
      (quotientStack (inertiaGroupoid G)).p

AlgebraicGeometry.Stack.inertiaComparisonForgetfulIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaQuotientStackComparison.lean, line 1382. The attribute's comment: “second assertion: the comparison is a 1-morphism over [U/R]”.

Composing the comparison [G/R'] ⟶ ℐ_{[U/R]} with the forgetful 1-morphism ℐ_{[U/R]} ⟶ [U/R] gives the 1-morphism [G/R'] ⟶ [U/R] of Stacks 046Q induced by the forgetful morphism of groupoids (G, R', s', t', c') ⟶ (U, R, s, t, c), by an isomorphism of functors.

noncomputable def inertiaComparisonForgetfulIso
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    ((inertiaComparison G).toFunctor ⋙ RelativeInertia.π (quotientStack G).p) ≅
      (quotientStackMap (inertiaForgetful G)).toFunctor

AlgebraicGeometry.Stack.isEquivalence_inertiaComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaQuotientStackComparison.lean, line 1401. The attribute's comment: “second assertion: I_{[U/R]} = [G/R'], the comparison is an equivalence”.

The underlying functor of the comparison [G/R'] ⟶ ℐ_{[U/R]} is an equivalence of categories: the quotient stack of the inertia groupoid (G, R', s', t', c') is the inertia stack of [U/R].

theorem isEquivalence_inertiaComparison (G : GroupoidInAlgebraicSpaces C S hS B) :
    (inertiaComparison G).toFunctor.IsEquivalence
Tag 06PC, a lemma

Tag 06PC in the Stacks Project.

AlgebraicGeometry.Stack.inertiaQuotientStackSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/InertiaQuotientStackSquare.lean, line 116. The attribute's comment: “the canonical square, lower-left corner as the quotient stack [G/R'] of 06PB”.

For a groupoid (U, R, s, t, c) in algebraic spaces over B with stabilizer group algebraic space G/U (Stacks 0448), the 2-commutative square

𝒮_G  ------>  𝒮_U
 |             |
 v             v
[G/R'] ----> [U/R]

of stacks in groupoids over the big fppf site: the apex is the stack 𝒮_G of the stabilizer, the horizontal arrows are the 1-morphism of Stacks 0458 induced by G → U and the projection of Stacks 044R for the inertia groupoid (G, R', s', t', c') of Stacks 06PB, and the vertical arrows are that projection for (U, R, s, t, c) and the 1-morphism of Stacks 046Q induced by AlgebraicGeometry.GroupoidInAlgebraicSpaces.inertiaForgetful. The filler is the 2-isomorphism of Stacks 046Q.

noncomputable def inertiaQuotientStackSquare (G : GroupoidInAlgebraicSpaces C S hS B) :
    let J := BigFppfOver.topology C S hS
    let Q : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨quotientStack G, isStackInGroupoids_quotientStack G⟩
    let I : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨quotientStack (inertiaGroupoid G), isStackInGroupoids_quotientStack (inertiaGroupoid G)⟩
    let W : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨liftedFibredCategory G.objects, isStackInGroupoids_liftedFibredCategory G.objects⟩
    Bicategory.TwoCommSq
      (Bicategory.InducedBicategory.mkHom (liftedQuotientStackProjection G) : W ⟶ Q)
      (Bicategory.InducedBicategory.mkHom (quotientStackMap (inertiaForgetful G)) : I ⟶ Q)

AlgebraicGeometry.Stack.isTwoFibreProduct_inertiaQuotientStackSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/InertiaQuotientStackSquare.lean, line 159. The attribute's comment: “that square is 2-cartesian, lower-left corner as the quotient stack [G/R'] of 06PB”.

The square

𝒮_G  ------>  𝒮_U
 |             |
 v             v
[G/R'] ----> [U/R]

of AlgebraicGeometry.Stack.inertiaQuotientStackSquare is a 2-fibre product (Stacks 003Q) in the bicategory of stacks in groupoids over the big fppf site, i.e. the diagram is 2-cartesian.

noncomputable def isTwoFibreProduct_inertiaQuotientStackSquare
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    Bicategory.IsTwoFibreProduct (inertiaQuotientStackSquare G)

AlgebraicGeometry.Stack.isTwoFibreProduct_quotientStackInertiaSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaQuotientStackSquareFibred.lean, line 249. The attribute's comment: “the canonical square with corners S_G, S_U, I_[U/R], [U/R] is 2-cartesian”.

Assume B → S and (U, R, s, t, c) as in Stacks 044Q (1). Let G/U be the stabilizer group algebraic space of the groupoid (U, R, s, t, c, e, i) (Stacks 0448). Then the canonical diagram

𝒮_G  ------>  𝒮_U
 |             |
 v             v
ℐ_{[U/R]} --> [U/R]

of AlgebraicGeometry.Stack.quotientStackInertiaSquare is 2-cartesian, i.e. a 2-fibre product in the sense of Stacks 003Q, in the 2-category of categories fibred in groupoids over the big fppf site (Stacks 02XS).

noncomputable def isTwoFibreProduct_quotientStackInertiaSquare
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    Bicategory.IsTwoFibreProduct (quotientStackInertiaSquare G)

AlgebraicGeometry.Stack.isTwoFibreProduct_quotientStackInertiaSquareInGroupoids, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaQuotientStackSquareFibred.lean, line 310. The attribute's comment: “that square, in the 2-category of stacks in groupoids, is 2-cartesian”.

Assume B → S and (U, R, s, t, c) as in Stacks 044Q (1) and let G/U be the stabilizer group algebraic space of (U, R, s, t, c, e, i) (Stacks 0448). Then the canonical diagram

𝒮_G  ------>  𝒮_U
 |             |
 v             v
ℐ_{[U/R]} --> [U/R]

is 2-cartesian in the 2-category of stacks in groupoids over the big fppf site (Stacks 02ZK).

noncomputable def isTwoFibreProduct_quotientStackInertiaSquareInGroupoids
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    Bicategory.IsTwoFibreProduct (quotientStackInertiaSquareInGroupoids G)
Sources
LeanAlgebraicGeometry.GroupoidInAlgebraicSpaces.inertiaGroupoid · AlgebraicGeometry.Stack.inertiaComparison_comp_toBase · AlgebraicGeometry.Stack.inertiaComparisonForgetfulIso · AlgebraicGeometry.Stack.isEquivalence_inertiaComparison · AlgebraicGeometry.Stack.inertiaQuotientStackSquare · AlgebraicGeometry.Stack.isTwoFibreProduct_inertiaQuotientStackSquare · AlgebraicGeometry.Stack.isTwoFibreProduct_quotientStackInertiaSquare · AlgebraicGeometry.Stack.isTwoFibreProduct_quotientStackInertiaSquareInGroupoids

Section78.27 Gerbes and quotient stacks#

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

Tag 06PE, a lemma

Tag 06PE in the Stacks Project.

AlgebraicGeometry.Stack.isGerbeOver_quotientStackMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/GerbeCriterion.lean, line 491.

The induced morphism of quotient stacks [f] : [U/R] ⟶ [U'/R'] makes [U/R] a gerbe over [U'/R'] as soon as f : U ⟶ U' and R ⟶ R'|_U are surjective maps of fppf sheaves: the first hypothesis is local surjectivity of the map of object spaces, the second asks that an arrow of R' between the images of two local points of U lift, after an fppf covering, to an arrow of R between those points.

public theorem isGerbeOver_quotientStackMap
    (C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
    (B : AlgebraicSpaces C S hS)
    {G H : GroupoidInAlgebraicSpaces C S hS B}
    (f : GroupoidInAlgebraicSpaces.Hom G H)
    (hobj : Presheaf.IsLocallySurjective
      (BigFppfOver.topology C S hS) f.toGroupoidHom.mapObjects)
    (harr : ∀ (T : BigFppfOver C S hS)
      (a b : G.objects.obj.obj (Opposite.op T))
      (r' : H.arrows.obj.obj (Opposite.op T)),
      H.source.hom.app (Opposite.op T) r' =
        f.toGroupoidHom.mapObjects.app (Opposite.op T) a →
      H.target.hom.app (Opposite.op T) r' =
        f.toGroupoidHom.mapObjects.app (Opposite.op T) b →
      ∃ R ∈ BigFppfOver.topology C S hS T,
        ∀ ⦃V : BigFppfOver C S hS⦄ (i : V ⟶ T), R i →
          ∃ r : G.arrows.obj.obj (Opposite.op V),
            G.source.hom.app (Opposite.op V) r =
              G.objects.obj.map i.op a ∧
            G.target.hom.app (Opposite.op V) r =
              G.objects.obj.map i.op b ∧
            f.toGroupoidHom.mapArrows.app (Opposite.op V) r =
              H.arrows.obj.map i.op r') :
    CategoryTheory.IsGerbeOver
      (BigFppfOver.topology C S hS)
      (quotientStack H).p
      (quotientStackMap f).toFunctor
Tag 06PF, a lemma

Tag 06PF in the Stacks Project.

AlgebraicGeometry.Stack.isGerbeOver_quotientStackToBase_trivialAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/TrivialActionGerbe.lean, line 76.

Stacks 06PF. Let G be a group algebraic space over B and endow B with the trivial action of G. The structure arrow [B/G] ⟶ B turns [B/G] into a gerbe over B.

theorem isGerbeOver_quotientStackToBase_trivialAction
    (B : AlgebraicSpaces C S hS) (G : Over B.obj) [GrpObj G]
    (hG : IsAlgebraicSpace C S hS G.left)
    (A : Space.ActionGroupoidConstruction B G (𝟙_ (Over B.obj)) hG B.property) :
    CategoryTheory.IsGerbeOver (BigFppfOver.topology C S hS)
      (fibredCategory C S hS B.obj).val.p (quotientStackToBase A.groupoid).toFunctor
Sources
LeanAlgebraicGeometry.Stack.isGerbeOver_quotientStackMap · AlgebraicGeometry.Stack.isGerbeOver_quotientStackToBase_trivialAction

Section78.28 Quotient stacks and change of big site#

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

Tag 04WX, a lemma

Tag 04WX in the Stacks Project.

AlgebraicGeometry.Stack.isEquivalenceOver_changeBigSiteQuotientEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/ChangeBigSiteQuotientUnconditional.lean, line 70.

The canonical 1-morphism [f⁻¹U/f⁻¹R] ⟶ f⁻¹[U/R] is an equivalence in the 2-category of fibred categories over the enlarged localized big fppf site: it has a quasi-inverse strictly over the site, with vertical unit and counit.

theorem isEquivalenceOver_changeBigSiteQuotientEquivalence :
    Nonempty (Functor.IsEquivalenceOver
      (quotientStack (changeBigSiteGroupoid B B' h S hS G)).p
      (pullbackQuotientStack h S hS G).p
      (changeBigSiteQuotientEquivalence B B' h S hS G))
Sources
LeanAlgebraicGeometry.Stack.isEquivalenceOver_changeBigSiteQuotientEquivalence

Section78.29 Separation conditions#

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

Tag 0454, a lemma

Tag 0454 in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isIso_arrowToArrowsOverObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/Diagonal.lean, line 183. The attribute's comment: “the upper horizontal morphism is an isomorphism”.

Stacks 0454. The upper horizontal morphism f ↦ (f, s f) of the diagram is an isomorphism, its inverse being the first projection of R ×_{s, U} U.

theorem isIso_arrowToArrowsOverObjects (G : GroupoidInAlgebraicSpaces C S hS B) :
    IsIso (arrowToArrowsOverObjects G)

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isIso_arrowPairsToArrowsOverStabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/Diagonal.lean, line 440. The attribute's comment: “the lower horizontal morphism is an isomorphism”.

Stacks 0454. The lower horizontal morphism (f, g) ↦ (f, f⁻¹ g) of the diagram is an isomorphism, its inverse being (f, h) ↦ (f, f h).

theorem isIso_arrowPairsToArrowsOverStabilizer
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    IsIso (arrowPairsToArrowsOverStabilizer G)

AlgebraicGeometry.GroupoidInAlgebraicSpaces.diagonal_comp_arrowPairsToArrowsOverStabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/Diagonal.lean, line 515. The attribute's comment: “commutativity of the left hand square”.

Stacks 0454. The left hand square of the diagram commutes: the relative diagonal of j = (t, s), followed by (f, g) ↦ (f, f⁻¹ g), is f ↦ (f, s f) followed by the unit section of the stabilizer.

theorem diagonal_comp_arrowPairsToArrowsOverStabilizer
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    pullback.diagonal (sourceTarget G).hom ≫ arrowPairsToArrowsOverStabilizer G =
      arrowToArrowsOverObjects G ≫ arrowsOverObjectsUnit G

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isPullback_stabilizerUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/Diagonal.lean, line 541. The attribute's comment: “the right hand square is cartesian”.

Stacks 0454. The right hand square of the diagram is cartesian: R ×_{s, U} S is the base change of the unit section e : U ⟶ S of the stabilizer along the projection R ×_{s, U} S ⟶ S, the base change being R ×_{s, U} U.

theorem isPullback_stabilizerUnit (G : GroupoidInAlgebraicSpaces C S hS B) :
    IsPullback (arrowsOverObjectsToObjects G) (arrowsOverObjectsUnit G)
      (η[stabilizer G]).left (arrowsOverStabilizerToStabilizer G)
Tag 0455, a lemma

Tag 0455 in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isSeparated_stabilizer_iff_unit_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/SeparationConditions.lean, line 125. The attribute's comment: “separated_equivalences”.

Stacks 0455. The structure morphism of the stabilizer of a groupoid in algebraic spaces is separated exactly when the unit section of the stabilizer is a closed immersion.

theorem isSeparated_stabilizer_iff_unit_closedImmersion
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    Space.IsSeparated C S hS (stabilizer G).hom ↔
      Space.IsClosedImmersion C S hS (η[stabilizer G]).left

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isSeparated_sourceTarget_iff_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/SeparationConditions.lean, line 135. The attribute's comment: “separated_equivalences”.

Stacks 0455. The source-target morphism of a groupoid in algebraic spaces is separated exactly when the structure morphism of its stabilizer is separated.

theorem isSeparated_sourceTarget_iff_stabilizer (G : GroupoidInAlgebraicSpaces C S hS B) :
    Space.IsSeparated C S hS (sourceTarget G).hom ↔
      Space.IsSeparated C S hS (stabilizer G).hom

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallySeparated_stabilizer_iff_unit_immersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/SeparationConditions.lean, line 147. The attribute's comment: “locally_separated_equivalences”.

Stacks 0455. The structure morphism of the stabilizer of a groupoid in algebraic spaces is locally separated exactly when the unit section of the stabilizer is an immersion.

theorem isLocallySeparated_stabilizer_iff_unit_immersion
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    Space.IsLocallySeparated C S hS (stabilizer G).hom ↔
      Space.IsImmersion C S hS (η[stabilizer G]).left

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallySeparated_sourceTarget_iff_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/SeparationConditions.lean, line 157. The attribute's comment: “locally_separated_equivalences”.

Stacks 0455. The source-target morphism of a groupoid in algebraic spaces is locally separated exactly when the structure morphism of its stabilizer is locally separated.

theorem isLocallySeparated_sourceTarget_iff_stabilizer
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    Space.IsLocallySeparated C S hS (sourceTarget G).hom ↔
      Space.IsLocallySeparated C S hS (stabilizer G).hom

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isQuasiSeparated_stabilizer_iff_unit_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/SeparationConditions.lean, line 171. The attribute's comment: “quasi_separated_equivalences”.

Stacks 0455. The structure morphism of the stabilizer of a groupoid in algebraic spaces is quasi-separated exactly when the unit section of the stabilizer is quasi-compact.

theorem isQuasiSeparated_stabilizer_iff_unit_quasiCompact
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    Space.IsQuasiSeparated C S hS (stabilizer G).hom ↔
      Space.IsQuasiCompact C S hS (η[stabilizer G]).left

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isQuasiSeparated_sourceTarget_iff_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/SeparationConditions.lean, line 181. The attribute's comment: “quasi_separated_equivalences”.

Stacks 0455. The source-target morphism of a groupoid in algebraic spaces is quasi-separated exactly when the structure morphism of its stabilizer is quasi-separated.

theorem isQuasiSeparated_sourceTarget_iff_stabilizer
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    Space.IsQuasiSeparated C S hS (sourceTarget G).hom ↔
      Space.IsQuasiSeparated C S hS (stabilizer G).hom
Sources
LeanAlgebraicGeometry.GroupoidInAlgebraicSpaces.isIso_arrowToArrowsOverObjects · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isIso_arrowPairsToArrowsOverStabilizer · AlgebraicGeometry.GroupoidInAlgebraicSpaces.diagonal_comp_arrowPairsToArrowsOverStabilizer · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isPullback_stabilizerUnit · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isSeparated_stabilizer_iff_unit_closedImmersion · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isSeparated_sourceTarget_iff_stabilizer · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallySeparated_stabilizer_iff_unit_immersion · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallySeparated_sourceTarget_iff_stabilizer

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.