95 Examples of Stacks

Chapter 95 of the Stacks Project, Examples of Stacks, Tag 04SL: the 10 sections of its 18 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 35 tags are carried by 134 declarations of the repository (all in StacksFrontier) and 7 registered declarations.

Section95.4 Quasi-coherent sheaves #

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

Tag 04U2, an equation

Tag 04U2 in the Stacks Project.

Stacks.QCoh.exists_categoryData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Basic.lean, line 177. The attribute's comment: “quasi-coherent category and f-map homs”.

Stacks 04U2. The category of quasi-coherent pairs over S exists together with its projection to the big fppf slice, and its morphisms are exactly the pairs of a morphism of schemes over S and an f-map of modules. The description of a hom-set as a disjoint union of pullback homs then follows by the pullback–pushforward adjunction.

public theorem exists_categoryData : Nonempty (CategoryData B S hS)

Stacks.QCoh.homEquivPullbackHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Basic.lean, line 209. The attribute's comment: “pullback hom equation”.

Stacks 04U2. A hom-set of the category of quasi-coherent pairs is the disjoint union, over the morphisms f of the base, of the morphisms from the pullback of the target module along f to the source module.

public noncomputable def homEquivPullbackHom (A C : Object B S hS) :
    (A ⟶ C) ≃
      Σ f : A.base ⟶ C.base,
        (Scheme.Modules.pullback (Object.schemeMap f)).obj C.module ⟶ A.module

Tag 04U3, a lemma

Tag 04U3 in the Stacks Project.

Stacks.QCoh.isStronglyCartesian_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/StronglyCartesian.lean, line 342.

Stacks 04U3. An arrow of quasi-coherent modules is strongly cartesian if and only if its canonical pullback comparison map is an isomorphism.

public theorem isStronglyCartesian_iff :
    (projection (B := B) (S := S) (hS := hS)).IsStronglyCartesian
      ((projection (B := B) (S := S) (hS := hS)).map m) m ↔
      IsIso ((homEquivPullbackHom A C m).2)

Tag 03YM, a lemma

Tag 03YM in the Stacks Project.

Stacks.QCoh.projection_isFibered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Fibred.lean, line 147. The attribute's comment: “condition (1): the functor is a fibred category”. References: SGA 1 VIII (1.1), “special case”.

Stacks 03YM, condition (1) of Stacks 026F: the projection from quasi-coherent modules on the schemes of the big fppf site over S to that site is a fibred category. A cartesian lift of f : V ⟶ U at a module F on U is the unit F ⟶ f_* f^* F of the pullback–pushforward adjunction, read as an f-map.

public theorem projection_isFibered (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    (projection (B := B) (S := S) (hS := hS)).IsFibered

Stacks.QCoh.projection_isStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Stack/SchemeDescent.lean, line 616. References: SGA 1 VIII (1.1), “special case”; SGA 1 VIII (1.3), “special case”.

Stacks 03YM. The projection p : 𝒬𝒞oh ⟶ (Sch/S)_fppf from quasi-coherent modules on the schemes of the big fppf site over S to that site satisfies the three conditions of Stacks 026F: it is a fibred category, the presheaves Mor(x, y) of Stacks 02ZB on each slice of the site are sheaves, and every descent datum along a covering sieve is effective.

The three conditions are the three fields of CategoryTheory.Functor.IsStack. Condition (1) is the existence of the cartesian lifts given by the units of the pullback–pushforward adjunction, and conditions (2) and (3) are Mathlib's stack condition for the pullback pseudofunctor of p (CategoryTheory.Functor.isStack_pullbackPseudofunctor_iff), hence the statement that the comparison from each fibre to the descent data of each fppf covering family is an equivalence. That comparison is identified with the canonical descent functor of Stacks 023D on schemes (canonicalComparisonNatIso), which is an equivalence by the two halves of Stacks 023T: full faithfulness AlgebraicGeometry.nonempty_fullyFaithful_canonicalDescentFunctor' and effectivity AlgebraicGeometry.QuasicoherentDescentData.isEffective_fpqcPrecoverage, both of which hold for an arbitrary fpqc covering family, fppf coverings being fpqc coverings.

public theorem projection_isStack (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    Functor.IsStack (projection (B := B) (S := S) (hS := hS))
      (AlgebraicGeometry.BigFppfOver.topology B S hS)

Sources

LeanStacks.QCoh.exists_categoryData · Stacks.QCoh.homEquivPullbackHom · Stacks.QCoh.isStronglyCartesian_iff · Stacks.QCoh.projection_isFibered · Stacks.QCoh.projection_isStack

Section95.5 The stack of finitely generated quasi-coherent sheaves #

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

Tag 04U4, a lemma

Tag 04U4 in the Stacks Project.

Stacks.QCoh.isStack_finiteTypeProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FiniteTypeStack.lean, line 168. The attribute's comment: “conditional on Stacks 03YM, that the projection from quasi-coherent modules to the big fppf site of S is a stack”.

Stacks 04U4. The quasi-coherent modules of finite type over S form a stack for the big fppf topology: finite type is preserved by the pullbacks computing the strongly cartesian arrows of Stacks 04U3, and it descends along fppf coverings by Stacks 05AZ, so Stacks 04TU applies to the full subcategory they cut out. The hypothesis is Stacks 03YM, that the projection from all quasi-coherent modules is a stack.

public theorem isStack_finiteTypeProjection
    (hp : Functor.IsStack (projection (B := B) (S := S) (hS := hS))
      (AlgebraicGeometry.BigFppfOver.topology B S hS)) :
    Functor.IsStack (finiteTypeProjection B S hS)
      (AlgebraicGeometry.BigFppfOver.topology B S hS)

Stacks.QCoh.finiteTypeProjection_isStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FiniteTypeStackUnconditional.lean, line 45.

Stacks 04U4. The projection from the quasi-coherent modules of finite type on the schemes of the big fppf site over S to that site satisfies the three conditions of Stacks 026F: it is a fibred category, the presheaves Mor(x, y) are sheaves, and descent data are effective. Finite type is preserved by the pullbacks computing the strongly cartesian arrows of Stacks 04U3 and descends along fppf coverings (Stacks 05AZ), so Stacks 04TU passes the stack of all quasi-coherent modules, Stacks 03YM, to its full subcategory of modules of finite type.

theorem finiteTypeProjection_isStack (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    Functor.IsStack (finiteTypeProjection B S hS)
      (AlgebraicGeometry.BigFppfOver.topology B S hS)

Tag 04U5, a lemma

Tag 04U5 in the Stacks Project.

Stacks.SheafOfModules.essentiallySmall_isFiniteType_and_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Algebraic/QuasiCoherentFiniteType.lean, line 49. The attribute's comment: “finite_type_quasi_coherent_modules”.

The finite type quasi-coherent sheaves of modules on a ringed space have only a set of isomorphism classes.

theorem essentiallySmall_isFiniteType_and_isQuasicoherent (X : RingedSpace.{u, u}) :
    ObjectProperty.EssentiallySmall.{u}
      (fun M : SheafOfModules.{u}
          ((sheafCompose (Opens.grothendieckTopology X)
            (forget₂ CommRingCat RingCat)).obj X.sheaf) ↦
        SheafOfModules.IsFiniteType M ∧ SheafOfModules.IsQuasicoherent M)

Declarations registered for the tag:

Stacks.SheafOfModules.essentiallySmall_isFiniteType, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/Algebraic/QuasiCoherentFiniteType.lean, line 35 (StacksFrontier): “finite_type_modules”.

Tag 04U6, a lemma

Tag 04U6 in the Stacks Project.

Stacks.QCoh.small_fiber_finiteTypeSmallProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FiniteTypeSmallStack.lean, line 299. The attribute's comment: “the selected subcategory is small: its objects over each object of the big fppf site over S form a set”.

Stacks 04U6, smallness. QCoh_fg,small is small: its objects over each object of the base site form a set. The ambient fibre is not set-sized, so this is the content of the cut; see the implementation notes for why the bound is fibrewise.

theorem small_fiber_finiteTypeSmallProjection (T : AlgebraicGeometry.BigFppfOver B S hS) :
    Small.{u} ((finiteTypeSmallProjection B S hS).Fiber T)

Stacks.QCoh.fullyFaithful_ι_finiteTypeSmall, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FiniteTypeSmallStack.lean, line 307. The attribute's comment: “clause (1), first half: the inclusion functor is fully faithful”.

Stacks 04U6 (1), first half. The inclusion QCoh_fg,small → QCoh_fg is fully faithful, the subcategory being full.

noncomputable def fullyFaithful_ι_finiteTypeSmall :
    (FiniteTypeSmall B S hS).ι.FullyFaithful

Stacks.QCoh.essSurj_ι_finiteTypeSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FiniteTypeSmallStack.lean, line 314. The attribute's comment: “clause (1), second half: the inclusion functor is essentially surjective”.

Stacks 04U6 (1), second half. The inclusion QCoh_fg,small → QCoh_fg is essentially surjective: a canonical representative of its own isomorphism class was kept in every fibre.

theorem essSurj_ι_finiteTypeSmall : (FiniteTypeSmall B S hS).ι.EssSurj

Stacks.QCoh.isStack_finiteTypeSmallProjection_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FiniteTypeSmallStackUnconditional.lean, line 46. The attribute's comment: “clause (2): the restricted projection is a stack over the big fppf site over S”.

Stacks 04U6 (2), unconditionally. The hypothesis of Stacks.QCoh.isStack_finiteTypeSmallProjection is Stacks 03YM, and that is Stacks.QCoh.projection_isStack.

theorem isStack_finiteTypeSmallProjection_unconditional :
    Functor.IsStack (finiteTypeSmallProjection B S hS)
      (AlgebraicGeometry.BigFppfOver.topology B S hS)

Sources

LeanStacks.QCoh.isStack_finiteTypeProjection · Stacks.QCoh.finiteTypeProjection_isStack · Stacks.SheafOfModules.essentiallySmall_isFiniteType_and_isQuasicoherent · Stacks.SheafOfModules.essentiallySmall_isFiniteType · Stacks.QCoh.small_fiber_finiteTypeSmallProjection · Stacks.QCoh.fullyFaithful_ι_finiteTypeSmall · Stacks.QCoh.essSurj_ι_finiteTypeSmall · Stacks.QCoh.isStack_finiteTypeSmallProjection_unconditional

Section95.6 Finite étale covers #

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

Tag 0BLY, the section

Tag 0BLY in the Stacks Project.

AlgebraicGeometry.FiniteEtaleCovers, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteEtaleCovers.lean, line 78. The attribute's comment: “the category FÉt of the section: objects are the finite étale morphisms of the big fppf category over S, morphisms are the commutative squares”.

The category FÉt of Stacks 0BLY over a big fppf site: an object is a finite étale morphism U ⟶ T of the big fppf category over S, and a morphism is a commutative square.

abbrev FiniteEtaleCovers : Type _

AlgebraicGeometry.finiteEtaleProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteEtaleCovers.lean, line 84. The attribute's comment: “the functor p of the section, sending a finite étale cover to its base”.

The functor p : FÉt ⟶ (Sch/S)_fppf of Stacks 0BLY, sending a finite étale morphism U ⟶ T to its base T.

def finiteEtaleProjection : FiniteEtaleCovers B S hS ⥤ BigFppfOver B S hS

Tag 0BLZ, a lemma

Tag 0BLZ in the Stacks Project.

AlgebraicGeometry.finiteEtaleProjection_isFibered, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteEtaleCovers.lean, line 121. The attribute's comment: “condition (1) of Stacks 026F: p is a fibred category. Condition (2), that the presheaves Mor(x, y) are fppf sheaves, is AlgebraicGeometry.finiteEtaleProjection_isMorSheaf.”.

Condition (1) of Stacks 026F for FÉt. The functor p : FÉt ⟶ (Sch/S)_fppf is a fibred category: the strongly cartesian lift of a morphism f : T ⟶ T' with target the finite étale cover U ⟶ T' is the base change U ×_{T'} T ⟶ T, again finite étale.

instance finiteEtaleProjection_isFibered :
    (finiteEtaleProjection B S hS).IsFibered

AlgebraicGeometry.finiteEtaleProjection_isStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteEtaleCoversDescent.lean, line 749.

Stacks 0BLZ. The functor p : FÉt ⟶ (Sch/S)_fppf of Stacks 0BLY defines a stack over the big fppf site of S: it satisfies the three conditions of Stacks 026F.

Condition (1) is AlgebraicGeometry.finiteEtaleProjection_isFibered, condition (2) is AlgebraicGeometry.finiteEtaleProjection_isMorSheaf and condition (3) is AlgebraicGeometry.finiteEtaleProjection_hasEffectiveDescent.

theorem finiteEtaleProjection_isStack :
    Functor.IsStack (finiteEtaleProjection B S hS) (BigFppfOver.topology B S hS)

AlgebraicGeometry.finiteEtaleProjection_isMorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteEtaleCoversStack.lean, line 316. The attribute's comment: “condition (2) of Stacks 026F: the presheaves Mor(x, y) are fppf sheaves, so locally equal morphisms of FÉt are equal and morphisms given compatibly over a covering sieve glue. Condition (1) is AlgebraicGeometry.finiteEtaleProjection_isFibered.”.

Condition (2) of Stacks 026F for FÉt. The presheaves Mor(x, y) of Stacks 02ZB attached to two finite étale covers of one and the same base are sheaves for the fppf topology: locally equal morphisms of FÉt are equal, and morphisms of FÉt given compatibly over a covering sieve of the base glue.

theorem finiteEtaleProjection_isMorSheaf (U : BigFppfOver B S hS)
    (x y : (finiteEtaleProjection B S hS).Fiber U) :
    Functor.IsMorSheaf (finiteEtaleProjection B S hS) (BigFppfOver.topology B S hS) U x y

Sources

LeanAlgebraicGeometry.FiniteEtaleCovers · AlgebraicGeometry.finiteEtaleProjection · AlgebraicGeometry.finiteEtaleProjection_isFibered · AlgebraicGeometry.finiteEtaleProjection_isStack · AlgebraicGeometry.finiteEtaleProjection_isMorSheaf

Section95.7 Algebraic spaces #

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

Tag 04U8, an equation

Tag 04U8 in the Stacks Project.

AlgebraicGeometry.spaceHomEquivPullbackHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/VaryingBaseHom.lean, line 82.

The hom-set equation for algebraic spaces over varying representable bases.

noncomputable def spaceHomEquivPullbackHom
    (A C : Comma
      (ObjectProperty.ι (fun F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u =>
        IsAlgebraicSpace B S hS F))
      (yoneda : BigFppfOver B S hS ⥤
        (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)) :
    { e : (A ⟶ C) ≃
        Σ g : A.right ⟶ C.right,
          (Over.mk (ObjectProperty.homMk A.hom : A.left ⟶
            schemeSpace A.right) ⟶ pullbackOver A C g) //
      ∀ m : A ⟶ C, (e m).1 = m.right ∧
        ((e m).2).left ≫
          (ObjectProperty.homMk
            (pullback.snd (schemeSpaceMap (e m).1).hom C.hom) :
              AlgebraicSpaces.fiberProduct B S hS
                (schemeSpaceMap (e m).1) (ObjectProperty.homMk C.hom) ⟶
                C.left) = m.left }

Tag 04U9, a lemma

Tag 04U9 in the Stacks Project.

AlgebraicGeometry.spacesProjection_isStronglyCartesian_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StronglyCartesian.lean, line 80.

Stacks 04U9. A morphism of algebraic spaces over varying schemes is strongly cartesian if and only if its canonical comparison with the base change of its target is an isomorphism.

theorem spacesProjection_isStronglyCartesian_iff
    {A C : Comma
      (ObjectProperty.ι (fun F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u =>
        IsAlgebraicSpace B S hS F))
      (yoneda : BigFppfOver B S hS ⥤ (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)} (m : A ⟶ C) :
    (spacesProjection B S hS).IsStronglyCartesian m.right m ↔
      IsIso (ObjectProperty.homMk (pullback.lift A.hom m.left.hom m.w.symm) :
        A.left ⟶ AlgebraicSpaces.fiberProduct B S hS
          (schemeSpaceMap m.right) (ObjectProperty.homMk C.hom))

Tag 04UA, a lemma

Tag 04UA in the Stacks Project.

AlgebraicGeometry.spacesProjection_isFibered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Prestack.lean, line 1084. The attribute's comment: “condition (1)”.

The projection from algebraic spaces over schemes is a fibred category.

theorem spacesProjection_isFibered :
    (spacesProjection B S hS).IsFibered

AlgebraicGeometry.spacesProjection_isMorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Prestack.lean, line 1092. The attribute's comment: “condition (2)”.

Morphisms of algebraic spaces over a fixed scheme satisfy fppf descent.

theorem spacesProjection_isMorSheaf :
    haveI : (spacesProjection B S hS).IsFibered :=
      spacesProjection_isFibered B S hS
    ∀ (U : BigFppfOver B S hS)
      (X Y : (spacesProjection B S hS).Fiber U),
      (spacesProjection B S hS).IsMorSheaf
        (BigFppfOver.topology B S hS) U X Y

Sources

LeanAlgebraicGeometry.spaceHomEquivPullbackHom · AlgebraicGeometry.spacesProjection_isStronglyCartesian_iff · AlgebraicGeometry.spacesProjection_isFibered · AlgebraicGeometry.spacesProjection_isMorSheaf

Section95.8 The stack of finite type algebraic spaces #

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

Tag 04UD, a lemma

Tag 04UD in the Stacks Project.

AlgebraicGeometry.finiteTypeSpacesProjection_isStack_of_bootstrap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/VaryingBase/FiniteTypeEffective.lean, line 154.

Stacks 04UD. The projection from finite-type algebraic spaces over varying base schemes is a stack over the big fppf site of S: it satisfies all three conditions of Stacks 026F.

Conditions (1) and (2) are AlgebraicGeometry.finiteTypeSpacesProjection_isFibered and AlgebraicGeometry.finiteTypeSpacesProjection_isMorSheaf. For condition (3), a descent datum is read in the ambient comma category, where its underlying sheaves glue (AlgebraicGeometry.SpacesDescent.nonempty_sheafGlueing, Stacks 04TR). The glued sheaf is an algebraic space by Stacks 04U0 over the base of the datum (AlgebraicGeometry.SpacesDescent.isAlgebraicSpace_of_isPullback_of_isFiniteType), which is where Stacks 04S6 condition (3) and the finite-type hypothesis are spent, so the datum is effective there (AlgebraicGeometry.SpacesDescent.SheafGlueing.isEffective). The descended object is of finite type over the base because finite type is fppf local on the base (AlgebraicGeometry.SpacesDescent.locallyClosed_isFiniteTypeSpace, Stacks 041U), which brings the effectivity back to the full subcategory (CategoryTheory.Functor.SieveDescentDatum.isEffective_of_isEffective_mapι).

theorem finiteTypeSpacesProjection_isStack_of_bootstrap :
    (finiteTypeSpacesProjection B S hS).IsStack (BigFppfOver.topology B S hS)

AlgebraicGeometry.finiteTypeSpacesProjection_isFibered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeStack.lean, line 184. The attribute's comment: “condition (1)”.

Condition (1) of Stacks 04UD. The projection from finite-type algebraic spaces over varying schemes to the big fppf site of S is a fibred category.

theorem finiteTypeSpacesProjection_isFibered :
    (finiteTypeSpacesProjection B S hS).IsFibered

AlgebraicGeometry.finiteTypeSpacesProjection_isMorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeStack.lean, line 193. The attribute's comment: “condition (2)”.

Condition (2) of Stacks 04UD. Morphisms of finite-type algebraic spaces over a fixed scheme satisfy fppf descent.

theorem finiteTypeSpacesProjection_isMorSheaf :
    haveI : (finiteTypeSpacesProjection B S hS).IsFibered :=
      finiteTypeSpacesProjection_isFibered B S hS
    ∀ (U : BigFppfOver B S hS)
      (X Y : (finiteTypeSpacesProjection B S hS).Fiber U),
      (finiteTypeSpacesProjection B S hS).IsMorSheaf
        (BigFppfOver.topology B S hS) U X Y

AlgebraicGeometry.finiteTypeSpacesProjection_hasEffectiveDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeStackDescent.lean, line 207. The attribute's comment: “condition (3)”.

Every descent datum of finite-type algebraic spaces relative to an fppf covering sieve of the big fppf site of S is effective.

theorem finiteTypeSpacesProjection_hasEffectiveDescent :
    haveI : (finiteTypeSpacesProjection B S hS).IsFibered :=
      finiteTypeSpacesProjection_isFibered B S hS
    (finiteTypeSpacesProjection B S hS).HasEffectiveDescent (BigFppfOver.topology B S hS)

Tag 04UE, a lemma

Tag 04UE in the Stacks Project.

AlgebraicGeometry.exists_small_finiteTypeSpaces_stack_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/VaryingBase/FiniteTypeEffective.lean, line 191. The attribute's comment: “the small stack of finite-type algebraic spaces”.

Stacks 04UE. There is a strictly full subcategory of the stack of finite-type algebraic spaces over varying base schemes with set-sized fibres whose inclusion is essentially surjective (and fully faithful, being the inclusion of a full subcategory) and whose restricted projection is still a stack over the big fppf site of S.

The source deduces this from Stacks 04UD, AlgebraicGeometry.finiteTypeSpacesProjection_isStack_of_bootstrap, and the replacement of Stacks 03ZZ, CategoryTheory.Functor.IsStack.exists_small_fullSubcategory, which applies because the category of finite-type algebraic spaces is essentially small; that deduction is AlgebraicGeometry.exists_small_finiteTypeSpaces_stack, whose Stacks 04UD input is discharged here.

theorem exists_small_finiteTypeSpaces_stack_unconditional :
    ∃ P : ObjectProperty (FiniteTypeSpaces B S hS),
      (∀ T : BigFppfOver B S hS,
        Small.{u} ((P.ι ⋙ finiteTypeSpacesProjection B S hS).Fiber T)) ∧
        P.ι.EssSurj ∧
        (P.ι ⋙ finiteTypeSpacesProjection B S hS).IsStack
          (BigFppfOver.topology B S hS)

AlgebraicGeometry.exists_small_finiteTypeSpaces_stack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeStackSmall.lean, line 135. The attribute's comment: “the small stack of finite-type algebraic spaces”.

Stacks 04UE. Granted that the projection from finite-type algebraic spaces over varying base schemes is a stack over the big fppf site of S — Stacks 04UD, whose condition (3) this library does not have — there is a strictly full subcategory of it with set-sized fibres whose inclusion is essentially surjective and whose restricted projection is still a stack.

theorem exists_small_finiteTypeSpaces_stack (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S)
    (hp : (finiteTypeSpacesProjection B S hS).IsStack (BigFppfOver.topology B S hS)) :
    ∃ P : ObjectProperty (FiniteTypeSpaces B S hS),
      (∀ T : BigFppfOver B S hS,
        Small.{u} ((P.ι ⋙ finiteTypeSpacesProjection B S hS).Fiber T)) ∧
        P.ι.EssSurj ∧
        (P.ι ⋙ finiteTypeSpacesProjection B S hS).IsStack
          (BigFppfOver.topology B S hS)

Sources

LeanAlgebraicGeometry.finiteTypeSpacesProjection_isStack_of_bootstrap · AlgebraicGeometry.finiteTypeSpacesProjection_isFibered · AlgebraicGeometry.finiteTypeSpacesProjection_isMorSheaf · AlgebraicGeometry.finiteTypeSpacesProjection_hasEffectiveDescent · AlgebraicGeometry.exists_small_finiteTypeSpaces_stack_unconditional · AlgebraicGeometry.exists_small_finiteTypeSpaces_stack

Section95.14 Classifying torsors #

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

Tag 04UJ, a subsection

Tag 04UJ in the Stacks Project.

SheafOfGroups.Torsors, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsors/CategoryOfTorsors.lean, line 88. The attribute's comment: “the objects of 𝒢-Torsors”. References: SGA 1 XIII (1.3), “partial”.

Stacks 04UJ. An object of the category 𝒢-Torsors of torsors under a sheaf of groups 𝒢 on a site (C, J): an object U of C together with a 𝒢|_U-torsor on the localized site C/U.

structure SheafOfGroups.Torsors (𝒢 : SheafOfGroups.{w} (C := C) J)

SheafOfGroups.Torsors.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsors/CategoryOfTorsors.lean, line 134. The attribute's comment: “the morphisms of 𝒢-Torsors”. References: SGA 1 XIII (1.3), “partial”.

Stacks 04UJ. A morphism (U, F) ⟶ (V, H) of the category 𝒢-Torsors: a morphism f : U ⟶ V of C together with an isomorphism α : f^{-1}H ⟶ F of 𝒢|_U-torsors. The isomorphism is recorded through its inverse on total spaces: a map of sheaves on C over f which restricts to a bijection from the fibre of Total F over each a : V ⟶ U to the fibre of Total H over a ≫ f.

structure Hom (T T' : Torsors.{t} 𝒢)

SheafOfGroups.Torsors.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsors/CategoryOfTorsors.lean, line 198. The attribute's comment: “the category 𝒢-Torsors”. References: SGA 1 XIII (1.3), “partial”.

Stacks 04UJ. The torsors under a sheaf of groups 𝒢 on a site (C, J) form a category 𝒢-Torsors: morphisms compose by composing f and α.

instance instCategory : Category (Torsors.{t} 𝒢)

SheafOfGroups.Torsors.projection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsors/CategoryOfTorsors.lean, line 209. The attribute's comment: “the functor p to the site”. References: SGA 1 XIII (1.3), “partial”.

Stacks 04UJ. The functor p : 𝒢-Torsors ⥤ C sending a pair (U, F) to U, which is how 𝒢-Torsors is regarded as a category over the site.

def projection : Torsors.{t} 𝒢 ⥤ C

SheafOfGroups.Torsors.isIso_of_isIso_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsors/CategoryOfTorsors.lean, line 275. The attribute's comment: “the fibre categories are groupoids”.

Stacks 04UJ. A morphism of 𝒢-Torsors whose morphism f of the site is an isomorphism is itself an isomorphism. Every morphism of a fibre category of p : 𝒢-Torsors ⥤ C lies over an identity, so this says that the fibre category over U — the category of 𝒢|_U-torsors — is a groupoid.

theorem isIso_of_isIso_base : IsIso m

Tag 04UK, a lemma

Tag 04UK in the Stacks Project.

SheafOfGroups.Torsors.projection_effectiveDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsors/StackOfTorsors/EffectiveDescent.lean, line 590. The attribute's comment: “condition (3): descent data are effective”. References: EGA IV (16.5.15), “more general”.

Stacks 04UK, condition (3) of Stacks 02ZI: every descent datum for p : 𝒢-Torsors ⥤ C relative to a J-covering family with genuine fibre-product overlaps is effective.

The object over U is glued by hand: the sections of its torsor over (W, β) are the matching families which assign, to every factorization of g ≫ β through a member f i of the covering family, a section of D.x i, compatibly with the restriction maps and with the glueing isomorphisms of the descent datum. That this is a sheaf is the sheaf condition for the D.x i; that 𝒢 acts simply transitively on it is the simple transitivity on the D.x i together with the sheaf condition for 𝒢; and that it is locally nonempty follows because each D.x i is. The morphisms D.x i ⟶ x send a section of D.x i to the matching family it spreads out to, whose compatibility over the double overlaps is exactly the cocycle condition of the descent datum, and which recovers the section it came from because of the cocycle condition at (i, i, i). Effectivity then follows from SheafOfGroups.Torsors.isEffective_of_glueing.

A matching family is indexed by the objects and the morphisms of C and by the index set of the covering family, so it lives in Type (max u v s t): the statement is for torsors whose sections lie in Type (max u v s t), which is the same bound max u v s ≤ t that the route through Stacks 04TP and 04TS imposes.

theorem projection_effectiveDescent {U : C} {I : Type s} (V : I → C) (f : ∀ i, V i ⟶ U)
    (hf : Sieve.ofArrows V f ∈ J U)
    (Vij : I → I → C) (pr₁ : ∀ i j, Vij i j ⟶ V i) (pr₂ : ∀ i j, Vij i j ⟶ V j)
    (hVij : ∀ i j, IsPullback (pr₁ i j) (pr₂ i j) (f i) (f j))
    (Vijk : I → I → I → C)
    (s₁₂ : ∀ i j k, Vijk i j k ⟶ Vij i j) (s₂₃ : ∀ i j k, Vijk i j k ⟶ Vij j k)
    (hVijk : ∀ i j k, IsPullback (s₁₂ i j k) (s₂₃ i j k) (pr₂ i j) (pr₁ j k))
    (q₁ : ∀ i j k, Vijk i j k ⟶ V i) (q₂ : ∀ i j k, Vijk i j k ⟶ V j)
    (q₃ : ∀ i j k, Vijk i j k ⟶ V k)
    (hq₁ : ∀ i j k, q₁ i j k = s₁₂ i j k ≫ pr₁ i j)
    (hq₂ : ∀ i j k, q₂ i j k = s₁₂ i j k ≫ pr₂ i j)
    (hq₃ : ∀ i j k, q₃ i j k = s₂₃ i j k ≫ pr₂ j k)
    (D : Functor.DescentDatum (projection : Torsors.{max u v s t} 𝒢 ⥤ C) V f Vij pr₁ pr₂ hVij
      Vijk s₁₂ s₂₃ hVijk q₁ q₂ q₃ hq₁ hq₂ hq₃) :
    D.IsEffective

SheafOfGroups.Torsors.projection_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsors/StackOfTorsors/EffectiveDescent.lean, line 719. References: SGA 3 IV (4.5.13), “special case”.

Stacks 04UK. The functor p : 𝒢-Torsors ⥤ C of Stacks 04UJ is a stack in groupoids over the site (C, J): it is fibred in groupoids, its Isom presheaves are sheaves, and every descent datum relative to a covering family is effective.

theorem projection_isStackInGroupoids :
    Functor.IsStackInGroupoids.{s} (projection : Torsors.{max u v s t} 𝒢 ⥤ C) J

SheafOfGroups.Torsors.projection_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsors/StackOfTorsors/FiberedInGroupoids.lean, line 188. The attribute's comment: “condition (1): p is fibred in groupoids”. References: SGA 4 XVIII (1.2.1), “partial”.

Stacks 04UK, condition (1) of Stacks 02ZI. The functor p : 𝒢-Torsors ⥤ C of Stacks 04UJ is fibred in groupoids: a morphism f : V ⟶ U of C lifts to the morphism (V, f^{-1}F) ⟶ (U, F) out of the restricted torsor, and a fill-in is unique because the recorded map of a morphism of 𝒢-Torsors is a bijection on the sections over each base morphism.

theorem projection_isFiberedInGroupoids :
    (projection : Torsors.{t} 𝒢 ⥤ C).IsFiberedInGroupoids

SheafOfGroups.Torsors.projection_isomIsSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Torsors/StackOfTorsors/IsomSheaf.lean, line 45. The attribute's comment: “condition (2): the Isom presheaves are sheaves”.

Stacks 04UK, condition (2) of Stacks 02ZI: the presheaves Isom(x, y) on C/U are sheaves. For two torsors x and y over the same object U of C and a covering family {V i → U} of U whose overlaps are genuine fibre products V i ×_U V j, a family of isomorphisms x|_{V i} ⟶ y|_{V i} of torsors which agree on the overlaps glues to a unique isomorphism x ⟶ y of 𝒢|_U-torsors restricting to the given ones.

The glued morphism is produced by the sheaf condition for the torsor y on C/U: a section of x over an object of C/U is, locally on a covering refining {V i → U}, the image of a section of a restriction x|_{V i} under the cartesian morphism x|_{V i} ⟶ x, and applying the given isomorphism there prescribes the sought section of y locally. The prescriptions agree because two local factorizations through f i and f j factor jointly through the fibre product V i ×_U V j, where the hypothesis supplies a single common restriction of the two isomorphisms. Equivariance for 𝒢 and compatibility with the restriction maps are inherited pointwise from the given isomorphisms, and the glued morphism is an isomorphism because a morphism of 𝒢-Torsors lying over an isomorphism of C is one (Stacks 04UJ).

theorem projection_isomIsSheaf {U : C} (x y : Torsors.{t} 𝒢)
    (hx : projection.obj x = U) (hy : projection.obj y = U)
    {I : Type s} (V : I → C) (f : ∀ i, V i ⟶ U) (hf : Sieve.ofArrows V f ∈ J U)
    (Vij : I → I → C) (pr₁ : ∀ i j, Vij i j ⟶ V i) (pr₂ : ∀ i j, Vij i j ⟶ V j)
    (hVij : ∀ i j, IsPullback (pr₁ i j) (pr₂ i j) (f i) (f j))
    (xr : ∀ i, Functor.Restriction projection (f i) x hx)
    (yr : ∀ i, Functor.Restriction projection (f i) y hy)
    (xrij : ∀ i j, Functor.Restriction projection (pr₁ i j ≫ f i) x hx)
    (yrij : ∀ i j, Functor.Restriction projection (pr₁ i j ≫ f i) y hy) :
    Functor.IsomIsSheafFor projection x y hx hy V f Vij pr₁ pr₂ hVij xr yr xrij yrij

Tag 04UL, a subsection

Tag 04UL in the Stacks Project.

AlgebraicGeometry.Space.SheafTorsors, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfSheafTorsors.lean, line 123. The attribute's comment: “the objects of 𝒢/ℬ-Torsors”.

Stacks 04UL. An object of the category 𝒢/ℬ-Torsors: an object U of the big fppf site of S, a section b : U ⟶ ℬ of ℬ over U, and a U ×_{b, ℬ} 𝒢-torsor F over U.

structure SheafTorsors

AlgebraicGeometry.Space.SheafTorsors.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfSheafTorsors.lean, line 272. The attribute's comment: “the morphisms of 𝒢/ℬ-Torsors”.

Stacks 04UL. A morphism (U, b, F) ⟶ (U', b', F') of 𝒢/ℬ-Torsors: a morphism f : U ⟶ U' with b = b' ∘ f together with an equivariant identification of F with f^{-1}F'.

structure Hom (T T' : SheafTorsors G)

AlgebraicGeometry.Space.SheafTorsors.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfSheafTorsors.lean, line 323. The attribute's comment: “the category 𝒢/ℬ-Torsors”.

Stacks 04UL. The torsors for a group object 𝒢 over a sheaf ℬ form a category 𝒢/ℬ-Torsors: morphisms compose by composing f and the identification of the total spaces.

instance instCategory : Category (SheafTorsors G)

AlgebraicGeometry.Space.SheafTorsors.projection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfSheafTorsors.lean, line 336. The attribute's comment: “the functor p to the site”.

Stacks 04UL. The functor p : 𝒢/ℬ-Torsors ⥤ (Sch/S)_fppf sending (U, b, F) to U, which is how 𝒢/ℬ-Torsors is regarded as a category over the big fppf site of S.

def projection : SheafTorsors G ⥤ BigFppfOver 𝒞 S hS

AlgebraicGeometry.Space.SheafTorsors.isIso_of_isIso_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfSheafTorsors.lean, line 391. The attribute's comment: “the fibre categories are groupoids”.

Stacks 04UL. A morphism of 𝒢/ℬ-Torsors whose morphism f of the big fppf site is an isomorphism is itself an isomorphism. Every morphism of a fibre category of p : 𝒢/ℬ-Torsors ⥤ (Sch/S)_fppf lies over an identity, so this says that the fibre category over U — the disjoint union over the sections b of ℬ over U of the categories of U ×_{b, ℬ} 𝒢-torsors — is a groupoid.

theorem isIso_of_isIso_base : IsIso φ

Tag 04UM, a lemma

Tag 04UM in the Stacks Project.

AlgebraicGeometry.Space.SheafTorsors.projection_effectiveDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/SheafTorsorsEffectiveDescent.lean, line 1392. The attribute's comment: “condition (3): descent data are effective”.

Stacks 04UM. Condition (3) of Stacks 02ZI for the functor p : 𝒢/ℬ-Torsors ⥤ (Sch/S)_fppf of Stacks 04UL: every descent datum of 𝒢/ℬ-Torsors relative to a covering family of the big fppf site of S is effective.

theorem projection_effectiveDescent
    (hB : Presheaf.IsSheaf (BigFppfOver.topology 𝒞 S hS) B)
    (hG : Presheaf.IsSheaf (BigFppfOver.topology 𝒞 S hS) G.X.left) :
    ∀ {U : BigFppfOver 𝒞 S hS} {I : Type w} (V : I → BigFppfOver 𝒞 S hS)
      (f : ∀ i, V i ⟶ U), Sieve.ofArrows V f ∈ BigFppfOver.topology 𝒞 S hS U →
      ∀ (Vij : I → I → BigFppfOver 𝒞 S hS)
        (pr₁ : ∀ i j, Vij i j ⟶ V i) (pr₂ : ∀ i j, Vij i j ⟶ V j)
        (hVij : ∀ i j, IsPullback (pr₁ i j) (pr₂ i j) (f i) (f j))
        (Vijk : I → I → I → BigFppfOver 𝒞 S hS)
        (s₁₂ : ∀ i j k, Vijk i j k ⟶ Vij i j) (s₂₃ : ∀ i j k, Vijk i j k ⟶ Vij j k)
        (hVijk : ∀ i j k, IsPullback (s₁₂ i j k) (s₂₃ i j k) (pr₂ i j) (pr₁ j k))
        (q₁ : ∀ i j k, Vijk i j k ⟶ V i) (q₂ : ∀ i j k, Vijk i j k ⟶ V j)
        (q₃ : ∀ i j k, Vijk i j k ⟶ V k)
        (hq₁ : ∀ i j k, q₁ i j k = s₁₂ i j k ≫ pr₁ i j)
        (hq₂ : ∀ i j k, q₂ i j k = s₁₂ i j k ≫ pr₂ i j)
        (hq₃ : ∀ i j k, q₃ i j k = s₂₃ i j k ≫ pr₂ j k)
        (D : Functor.DescentDatum (projection G) V f Vij pr₁ pr₂ hVij Vijk s₁₂ s₂₃ hVijk
          q₁ q₂ q₃ hq₁ hq₂ hq₃),
        D.IsEffective

AlgebraicGeometry.Space.SheafTorsors.projection_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/SheafTorsorsEffectiveDescent.lean, line 1789.

Stacks 04UM. The functor p : 𝒢/ℬ-Torsors ⥤ (Sch/S)_fppf of Stacks 04UL is a stack in groupoids over the big fppf site of S: the three conditions of Stacks 02ZI, namely AlgebraicGeometry.Space.SheafTorsors.projection_isFiberedInGroupoids, AlgebraicGeometry.Space.SheafTorsors.projection_isomIsSheaf and AlgebraicGeometry.Space.SheafTorsors.projection_effectiveDescent.

theorem projection_isStackInGroupoids
    (hB : Presheaf.IsSheaf (BigFppfOver.topology 𝒞 S hS) B)
    (hG : Presheaf.IsSheaf (BigFppfOver.topology 𝒞 S hS) G.X.left) :
    Functor.IsStackInGroupoids.{w} (projection G) (BigFppfOver.topology 𝒞 S hS)

AlgebraicGeometry.Space.SheafTorsors.projection_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/StackOfSheafTorsors.lean, line 612. The attribute's comment: “condition (1): p is fibred in groupoids”.

Stacks 04UM. Condition (1) of Stacks 02ZI for the functor p : 𝒢/ℬ-Torsors ⥤ (Sch/S)_fppf of Stacks 04UL: p is fibred in groupoids. Every morphism f : V ⟶ U of the big fppf site of S lifts to the restriction (V, b ∘ f, f^{-1}F) of an object (U, b, F) along f, and fill-ins exist and are unique.

theorem projection_isFiberedInGroupoids : (projection G).IsFiberedInGroupoids

AlgebraicGeometry.Space.SheafTorsors.projection_isomIsSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/StackOfSheafTorsors.lean, line 1011. The attribute's comment: “condition (2): the Isom presheaves are sheaves”.

Stacks 04UM. Condition (2) of Stacks 02ZI for the functor p : 𝒢/ℬ-Torsors ⥤ (Sch/S)_fppf of Stacks 04UL: for two objects (U, b, F) and (U, b', F') over the same object of the big fppf site of S, the presheaf Isom(F, F') is a sheaf. A family of isomorphisms of the restrictions along a covering family which agree on the overlaps glues, uniquely, to an isomorphism over U, because the total spaces are sheaves and the restrictions have as total spaces their base changes.

theorem projection_isomIsSheaf
    (hB : Presheaf.IsSheaf (BigFppfOver.topology 𝒞 S hS) B) :
    ∀ {U : BigFppfOver 𝒞 S hS} (x y : SheafTorsors G)
      (hx : (projection G).obj x = U) (hy : (projection G).obj y = U)
      {I : Type w} (V : I → BigFppfOver 𝒞 S hS) (f : ∀ i, V i ⟶ U),
      Sieve.ofArrows V f ∈ BigFppfOver.topology 𝒞 S hS U →
      ∀ (Vij : I → I → BigFppfOver 𝒞 S hS)
        (pr₁ : ∀ i j, Vij i j ⟶ V i) (pr₂ : ∀ i j, Vij i j ⟶ V j)
        (hVij : ∀ i j, IsPullback (pr₁ i j) (pr₂ i j) (f i) (f j))
        (xr : ∀ i, Functor.Restriction (projection G) (f i) x hx)
        (yr : ∀ i, Functor.Restriction (projection G) (f i) y hy)
        (xrij : ∀ i j, Functor.Restriction (projection G) (pr₁ i j ≫ f i) x hx)
        (yrij : ∀ i j, Functor.Restriction (projection G) (pr₁ i j ≫ f i) y hy),
        Functor.IsomIsSheafFor (projection G) x y hx hy V f Vij pr₁ pr₂ hVij xr yr xrij yrij

Tag 04UN, a subsection

Tag 04UN in the Stacks Project.

AlgebraicGeometry.Space.TorsorsFor.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfFppfTorsors.lean, line 280. The attribute's comment: “the morphisms of G-Principal, stated for an arbitrary trivializing covering property”.

A morphism (U, b, X) ⟶ (U', b', X') of torsors: a morphism f : U ⟶ U' over B together with an equivariant identification of X with U ×_{f, U'} X'.

structure Hom (T T' : TorsorsFor hB G P)

AlgebraicGeometry.Space.TorsorsFor.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfFppfTorsors.lean, line 331. The attribute's comment: “the category G-Principal, whose composition is stated for an arbitrary trivializing covering property”.

The torsors under a group algebraic space G over B which are trivialized by a family satisfying P form a category: morphisms compose by composing f and the identification of the total spaces.

instance instCategory : Category (TorsorsFor hB G P)

AlgebraicGeometry.Space.TorsorsFor.isIso_of_isIso_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfFppfTorsors.lean, line 402. The attribute's comment: “the fibre categories of p : G-Principal ⥤ (Sch/S)_fppf are groupoids, by the assertion for an arbitrary trivializing covering property”.

A morphism of torsors whose morphism f of the big fppf site is an isomorphism is itself an isomorphism. Every morphism of a fibre category of the functor p to the site lies over an identity, so this says that the fibre category over U — the disjoint union over the morphisms b : U ⟶ B of the categories of torsors under U ×_{b, B} G trivialized by a family satisfying P — is a groupoid.

theorem isIso_of_isIso_base : IsIso φ

AlgebraicGeometry.Space.PrincipalHomogeneousSpaces, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfPrincipalHomogeneousSpaces.lean, line 89. The attribute's comment: “the objects of G-Principal”.

Stacks 04UN. An object of the category G-Principal: an object U of the big fppf site of S, a morphism b : U ⟶ B, and a principal homogeneous space X over U under G_U = U ×_{b, B} G, that is a pseudo-torsor trivialized by an fpqc covering of U.

abbrev PrincipalHomogeneousSpaces

AlgebraicGeometry.Space.PrincipalHomogeneousSpaces.projection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfPrincipalHomogeneousSpaces.lean, line 109. The attribute's comment: “the functor p to the site”.

Stacks 04UN. The functor p : G-Principal ⥤ (Sch/S)_fppf sending (U, b, X) to U, which is how G-Principal is regarded as a category over the big fppf site of S.

abbrev PrincipalHomogeneousSpaces.projection :
    PrincipalHomogeneousSpaces hB G ⥤ BigFppfOver 𝒞 S hS

Tag 04UP, a remark

Tag 04UP in the Stacks Project.

AlgebraicGeometry.Space.PrincipalHomogeneousSpaces.isStackInGroupoids_of_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/PrincipalHomogeneousSpacesStack.lean, line 742. The attribute's comment: “p : G-Principal ⥤ (Sch/S)_fppf is a stack in groupoids once principal homogeneous spaces descend along fppf coverings as in (1)-(4)”.

Stacks 04UP. If principal homogeneous spaces satisfy effective descent along the coverings of (Sch/S)_fppf (items (1)–(4) of the remark, AlgebraicGeometry.Space.PrincipalHomogeneousSpaceDescent), then p : G-Principal ⥤ (Sch/S)_fppf is a stack in groupoids over (Sch/S)_fppf.

This is the formal content of the remark: Stacks conjectures that p is a stack in groupoids and says that this would follow from the descent statement (1)–(4), whose proof by the technique of Stacks 04U1 stops at a set theoretical question; that descent statement is the antecedent here, and the implication is proved in full.

Condition (1) of Stacks 02ZI, that p is fibred in groupoids, is AlgebraicGeometry.Space.PrincipalHomogeneousSpaces.projection_isFiberedInGroupoids.

Condition (2), that the Isom presheaves are sheaves, is AlgebraicGeometry.Space.TorsorsFor.projection_isomIsSheaf at the fpqc coverings: isomorphisms of total spaces glue because the total spaces are algebraic spaces, hence sheaves.

Condition (3): given a descent datum of G-Principal along a covering {Vᵢ ⟶ U}, the sections bᵢ : Vᵢ ⟶ B glue to b : U ⟶ B because B is a sheaf (AlgebraicGeometry.Space.PrincipalHomogeneousSpaces.exists_glued_sec); with H = U ×_{b, B} G the acting groups Vᵢ ×_{bᵢ, B} G are identified with H_{Vᵢ} (AlgebraicGeometry.Space.groupCompIso), which turns the datum into one of the shape (1)–(4) (AlgebraicGeometry.Space.PrincipalHomogeneousSpaces.descentDatumOfBase); the antecedent makes it effective, and the descended principal homogeneous H-space read back in G-Principal makes the original datum effective (PrincipalHomogeneousSpaces.isEffective_of_isEffective_descentDatumOfBase).

"Up to a replacement as in Stacks 03ZZ" is not needed: an object of G-Principal carries as total space an object of the slice over a representable presheaf of the set-sized big fppf site, so G-Principal is a genuine category and p a functor, as for Stacks 04US.

theorem isStackInGroupoids_of_descent (h : PrincipalHomogeneousSpaceDescent.{w} 𝒞 S hS) :
    Functor.IsStackInGroupoids.{w} (projection hB G) (BigFppfOver.topology 𝒞 S hS)

Tag 04UR, a subsection

Tag 04UR in the Stacks Project.

AlgebraicGeometry.Space.FppfTorsors, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfFppfTorsors.lean, line 145. The attribute's comment: “the objects of G-Torsors”.

Stacks 04UR. An object of the category G-Torsors: an object U of the big fppf site of S, a morphism b : U ⟶ B, and an fppf torsor X over U under G_U = U ×_{b, B} G.

abbrev FppfTorsors

AlgebraicGeometry.Space.TorsorsFor.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfFppfTorsors.lean, line 280. The attribute's comment: “the morphisms of G-Torsors”.

A morphism (U, b, X) ⟶ (U', b', X') of torsors: a morphism f : U ⟶ U' over B together with an equivariant identification of X with U ×_{f, U'} X'.

structure Hom (T T' : TorsorsFor hB G P)

AlgebraicGeometry.Space.TorsorsFor.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfFppfTorsors.lean, line 331. The attribute's comment: “the category G-Torsors”.

The torsors under a group algebraic space G over B which are trivialized by a family satisfying P form a category: morphisms compose by composing f and the identification of the total spaces.

instance instCategory : Category (TorsorsFor hB G P)

AlgebraicGeometry.Space.TorsorsFor.isIso_of_isIso_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfFppfTorsors.lean, line 402. The attribute's comment: “the fibre categories are groupoids”.

A morphism of torsors whose morphism f of the big fppf site is an isomorphism is itself an isomorphism. Every morphism of a fibre category of the functor p to the site lies over an identity, so this says that the fibre category over U — the disjoint union over the morphisms b : U ⟶ B of the categories of torsors under U ×_{b, B} G trivialized by a family satisfying P — is a groupoid.

theorem isIso_of_isIso_base : IsIso φ

AlgebraicGeometry.Space.FppfTorsors.projection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/CategoryOfFppfTorsors.lean, line 415. The attribute's comment: “the functor p to the site”.

Stacks 04UR. The functor p : G-Torsors ⥤ (Sch/S)_fppf sending (U, b, X) to U, which is how G-Torsors is regarded as a category over the big fppf site of S.

abbrev projection : FppfTorsors hB G ⥤ BigFppfOver 𝒞 S hS

Tag 04US, a lemma

Tag 04US in the Stacks Project.

AlgebraicGeometry.Space.FppfTorsors.projection_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/StackOfFppfTorsors.lean, line 182. The attribute's comment: “condition (1): p is fibred in groupoids”.

Condition (1) of Stacks 02ZI for the functor p : G-Torsors ⥤ (Sch/S)_fppf of Stacks 04UR: p is fibred in groupoids.

theorem projection_isFiberedInGroupoids : (projection hB G).IsFiberedInGroupoids

AlgebraicGeometry.Space.FppfTorsors.projection_isomIsSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/StackOfFppfTorsors.lean, line 270. The attribute's comment: “condition (2): the Isom presheaves are sheaves”.

Condition (2) of Stacks 02ZI for the functor p : G-Torsors ⥤ (Sch/S)_fppf of Stacks 04UR: for two objects (U, b, X) and (U, b', X') over the same object of the big fppf site of S, the presheaf Isom(X, X') is a sheaf.

theorem projection_isomIsSheaf
    {U : BigFppfOver 𝒞 S hS} (x y : FppfTorsors hB G)
    (hx : (projection hB G).obj x = U) (hy : (projection hB G).obj y = U)
    {I : Type w} (V : I → BigFppfOver 𝒞 S hS) (f : ∀ i, V i ⟶ U)
    (hf : Sieve.ofArrows V f ∈ BigFppfOver.topology 𝒞 S hS U)
    (Vij : I → I → BigFppfOver 𝒞 S hS)
    (pr₁ : ∀ i j, Vij i j ⟶ V i) (pr₂ : ∀ i j, Vij i j ⟶ V j)
    (hVij : ∀ i j, IsPullback (pr₁ i j) (pr₂ i j) (f i) (f j))
    (xr : ∀ i, Functor.Restriction (projection hB G) (f i) x hx)
    (yr : ∀ i, Functor.Restriction (projection hB G) (f i) y hy)
    (xrij : ∀ i j, Functor.Restriction (projection hB G) (pr₁ i j ≫ f i) x hx)
    (yrij : ∀ i j, Functor.Restriction (projection hB G) (pr₁ i j ≫ f i) y hy) :
    Functor.IsomIsSheafFor (projection hB G) x y hx hy V f Vij pr₁ pr₂ hVij
      xr yr xrij yrij

AlgebraicGeometry.Space.FppfTorsors.hasEffectiveDescent_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorStackUnconditional.lean, line 108. The attribute's comment: “condition (3): effectivity of descent, with nothing carried”.

Stacks 04US, condition (3) of Stacks 026F for p : G-Torsors ⥤ (Sch/S)_fppf, with nothing carried: every descent datum relative to a covering sieve of the big fppf site of S is effective.

This is AlgebraicGeometry.Space.FppfTorsors.hasEffectiveDescent_projection_of_bootstrap with both of its hypotheses discharged: Stacks 04S6 part (3) by AlgebraicGeometry.Space.isBootstrapAlgebraicSpaceAlongFlatSurjection, and condition (3) of Stacks 04UM for 𝒢/ℬ-Torsors by AlgebraicGeometry.Space.SheafTorsors.projection_hasEffectiveDescent, whose two sheaf hypotheses hold because B and G are algebraic spaces.

theorem hasEffectiveDescent_projection (hB : IsAlgebraicSpace 𝒞 S hS B)
    (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
    letI : (projection hB G).IsFibered :=
      (projection_isFiberedInGroupoids (hB := hB) (G := G)).isFibered
    Functor.HasEffectiveDescent (projection hB G) (BigFppfOver.topology 𝒞 S hS)

AlgebraicGeometry.Space.FppfTorsors.projection_isStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorStackUnconditional.lean, line 126. The attribute's comment: “the three conditions of Stacks 026F together, with nothing carried”.

Stacks 04US, with nothing carried: the projection p : G-Torsors ⥤ (Sch/S)_fppf of Stacks 04UR is a stack over the big fppf site of S, in the sense of Stacks 026F.

Condition (1) is AlgebraicGeometry.Space.FppfTorsors.projection_isFiberedInGroupoids; condition (2) is AlgebraicGeometry.Space.FppfTorsors.projection_isomIsSheaf, read through CategoryTheory.Functor.isMorSheaf_of_isomIsSheaf; condition (3) is AlgebraicGeometry.Space.FppfTorsors.hasEffectiveDescent_projection.

theorem projection_isStack (hB : IsAlgebraicSpace 𝒞 S hS B)
    (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
    Functor.IsStack (projection hB G) (BigFppfOver.topology 𝒞 S hS)

AlgebraicGeometry.Space.FppfTorsors.projection_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorStackUnconditional.lean, line 146. The attribute's comment: “the stack in groupoids in the rendering of Stacks 02ZI, with nothing carried”.

Stacks 04US, with nothing carried, in the rendering of Stacks 02ZI: the projection p : G-Torsors ⥤ (Sch/S)_fppf is a stack in groupoids over the big fppf site of S.

This is AlgebraicGeometry.Space.FppfTorsors.projection_isStack read through the forward bridge of Stacks 02ZJ, CategoryTheory.Functor.IsStack.isStackInGroupoids.

theorem projection_isStackInGroupoids (hB : IsAlgebraicSpace 𝒞 S hS B)
    (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
    Functor.IsStackInGroupoids.{w} (projection hB G) (BigFppfOver.topology 𝒞 S hS)

AlgebraicGeometry.Space.torsorProjection_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorStackUnconditional.lean, line 232. The attribute's comment: “condition (1) for the TorsorObj rendering, with nothing carried”.

Stacks 04US, condition (1) of Stacks 02ZI for the second rendering of the category of fppf G-torsors: AlgebraicGeometry.Space.torsorProjection is fibred in groupoids.

This is AlgebraicGeometry.Space.FppfTorsors.projection_isFiberedInGroupoids transported along AlgebraicGeometry.Space.torsorObjBasedEquivalence by Stacks 042G.

theorem torsorProjection_isFiberedInGroupoids :
    (torsorProjection hB G).IsFiberedInGroupoids

AlgebraicGeometry.Space.torsorProjection_isStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorStackUnconditional.lean, line 244. The attribute's comment: “the stack property for the TorsorObj rendering, with nothing carried”.

Stacks 04US in full, with nothing carried, for the second rendering of the category of fppf G-torsors: AlgebraicGeometry.Space.torsorProjection is a stack over the big fppf site of S.

This is AlgebraicGeometry.Space.FppfTorsors.projection_isStack transported along AlgebraicGeometry.Space.torsorObjBasedEquivalence by Stacks 042W.

theorem torsorProjection_isStack :
    (torsorProjection hB G).IsStack (BigFppfOver.topology 𝒞 S hS)

Tag 04UT, a lemma

Tag 04UT in the Stacks Project.

AlgebraicGeometry.Space.FppfTorsors.comparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparison.lean, line 167. The attribute's comment: “the comparison functor”.

The comparison functor G-Torsors ⥤ 𝒢/ℬ-Torsors which associates to a triple (U, b, X) the triple (U, b, 𝒳) where 𝒳 is X viewed as a sheaf.

def comparison (hB : IsAlgebraicSpace 𝒞 S hS B) (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
    FppfTorsors hB G ⥤ SheafTorsors G.obj

AlgebraicGeometry.Space.FppfTorsors.comparison_comp_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparison.lean, line 191. The attribute's comment: “the comparison functor lies over the site”.

The comparison functor is a 1-morphism of categories over the big fppf site of S: it sends a triple (U, b, X) to a triple with the same base object U and a morphism to a morphism with the same morphism f of the site.

theorem comparison_comp_projection (hB : IsAlgebraicSpace 𝒞 S hS B)
    (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
    comparison hB G ⋙ SheafTorsors.projection G.obj = projection hB G

AlgebraicGeometry.Space.FppfTorsors.instFaithfulComparison, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparison.lean, line 199. The attribute's comment: “the comparison functor is faithful”.

The comparison functor is faithful: a morphism of G-Torsors is determined by the morphism of 𝒢/ℬ-Torsors it becomes.

instance instFaithfulComparison : (comparison hB G).Faithful

AlgebraicGeometry.Space.FppfTorsors.instFullComparison, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparison.lean, line 206. The attribute's comment: “the comparison functor is full”.

The comparison functor is full: a morphism of 𝒢/ℬ-Torsors between torsors of algebraic spaces is already a morphism of G-Torsors.

instance instFullComparison : (comparison hB G).Full

AlgebraicGeometry.Space.FppfTorsors.isEquivalenceOverComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparisonEquivalence.lean, line 203. The attribute's comment: “the hypothesis-carrying form, taking hdesc — effectivity of descent for G-Torsors, condition (3) of Stacks 02ZI in Stacks 04US. That hypothesis is PROVED, as FppfTorsors.hasEffectiveDescent_projection, and the form carrying nothing is FppfTorsors.nonempty_isEquivalenceOver_comparison”.

If every descent datum of fppf torsors of algebraic spaces along a covering sieve of the big fppf site of S is effective (hdesc, condition (3) of Stacks 02ZI for p : G-Torsors ⥤ (Sch/S)_fppf), then the comparison functor G-Torsors ⥤ 𝒢/ℬ-Torsors, which sends a triple (U, b, X) to the triple (U, b, 𝒳) with 𝒳 the total space seen as a sheaf, is an equivalence of stacks in groupoids over the big fppf site of S: it has a quasi-inverse which is again a functor over the site, with vertical unit and counit.

noncomputable def isEquivalenceOverComparison (hB : IsAlgebraicSpace 𝒞 S hS B)
    (G : GroupAlgebraicSpace 𝒞 S hS B hB)
    (hdesc : letI : (projection hB G).IsFibered :=
        (projection_isFiberedInGroupoids (hB := hB) (G := G)).isFibered
      Functor.HasEffectiveDescent (projection hB G) (BigFppfOver.topology 𝒞 S hS)) :
    Functor.IsEquivalenceOver (projection hB G) (SheafTorsors.projection G.obj)
      (comparison hB G)

AlgebraicGeometry.Space.FppfTorsors.nonempty_isEquivalenceOver_comparison_of_isStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparisonEquivalence.lean, line 220. The attribute's comment: “the hypothesis-carrying form of the criterion Stacks 046N, taking the two stack conditions Stacks 04US and Stacks 04UM as hsource and htarget. BOTH are proved — FppfTorsors.projection_isStack and SheafTorsors.projection_isStackInGroupoids — and the form carrying nothing is FppfTorsors.nonempty_isEquivalenceOver_comparison”.

If both p : G-Torsors ⥤ (Sch/S)_fppf and p : 𝒢/ℬ-Torsors ⥤ (Sch/S)_fppf are stacks over the big fppf site of S (Stacks 04US and Stacks 04UM), then the comparison functor is an equivalence over that site.

theorem nonempty_isEquivalenceOver_comparison_of_isStack (hB : IsAlgebraicSpace 𝒞 S hS B)
    (G : GroupAlgebraicSpace 𝒞 S hS B hB)
    (hsource : (projection hB G).IsStack (BigFppfOver.topology 𝒞 S hS))
    (htarget : (SheafTorsors.projection G.obj).IsStack (BigFppfOver.topology 𝒞 S hS)) :
    Nonempty (Functor.IsEquivalenceOver (projection hB G) (SheafTorsors.projection G.obj)
      (comparison hB G))

AlgebraicGeometry.Space.FppfTorsors.isEquivalenceOverComparisonOfAlgebraic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparisonEquivalence.lean, line 295. The attribute's comment: “the hypothesis-carrying form, taking halg — algebraicity of the total space of every 𝒢/ℬ-torsor sheaf, which isAlgebraicSpace_total_of_isEquivalenceOver shows the tag's conclusion in turn implies, so the two are equivalent. halg is PROVED, via isBootstrapAlgebraicSpaceAlongFlatSurjection, and the form carrying nothing is FppfTorsors.nonempty_isEquivalenceOver_comparison”.

The comparison functor G-Torsors ⥤ 𝒢/ℬ-Torsors is an equivalence of stacks in groupoids over the big fppf site of S as soon as every torsor of sheaves has an algebraic space as total space.

noncomputable def isEquivalenceOverComparisonOfAlgebraic
    (hB : IsAlgebraicSpace 𝒞 S hS B) (G : GroupAlgebraicSpace 𝒞 S hS B hB)
    (halg : ∀ T : SheafTorsors G.obj, IsAlgebraicSpace 𝒞 S hS T.total.left) :
    Functor.IsEquivalenceOver (projection hB G) (SheafTorsors.projection G.obj)
      (comparison hB G)

AlgebraicGeometry.Space.FppfTorsors.nonempty_isEquivalenceOver_comparison_iff_isAlgebraicSpace_total, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparisonEquivalence.lean, line 347. The attribute's comment: “the equivalence holds exactly when every 𝒢/ℬ-torsor sheaf has an algebraic space as total space; the tag asserts the left-hand side, which this does not prove unconditionally”.

The comparison functor G-Torsors ⥤ 𝒢/ℬ-Torsors is an equivalence of stacks in groupoids over the big fppf site of S if and only if every 𝒢/ℬ-torsor sheaf has an algebraic space as total space.

theorem nonempty_isEquivalenceOver_comparison_iff_isAlgebraicSpace_total
    (hB : IsAlgebraicSpace 𝒞 S hS B) (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
    Nonempty (Functor.IsEquivalenceOver (projection hB G) (SheafTorsors.projection G.obj)
        (comparison hB G)) ↔
      ∀ T : SheafTorsors G.obj, IsAlgebraicSpace 𝒞 S hS T.total.left

AlgebraicGeometry.Space.FppfTorsors.isFibredOneMorphism_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparisonFibred.lean, line 45. The attribute's comment: “the comparison functor is a 1-morphism of fibred categories”.

The comparison functor G-Torsors ⥤ 𝒢/ℬ-Torsors is a 1-morphism of fibred categories over the big fppf site of S: it lies over the site and preserves strongly cartesian morphisms.

theorem isFibredOneMorphism_comparison (hB : IsAlgebraicSpace 𝒞 S hS B)
    (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
    Functor.IsFibredOneMorphism (projection hB G) (SheafTorsors.projection G.obj)
      (comparison hB G)

AlgebraicGeometry.Space.FppfTorsors.nonempty_isEquivalenceOver_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparisonUnconditional.lean, line 67. The attribute's comment: “the equivalence of stacks in groupoids, with nothing carried”.

Stacks 04UT, with nothing carried, and with it the 𝒢/ℬ-Torsors leg of Stacks 0CQJ: the comparison functor G-Torsors ⥤ 𝒢/ℬ-Torsors is an equivalence of stacks in groupoids over the big fppf site of S.

The hypothesis every earlier rendering carried is the object half of Stacks 04U1, equivalently Stacks 04S6 part (3), which is now the theorem AlgebraicGeometry.Space.isBootstrapAlgebraicSpaceAlongFlatSurjection.

theorem nonempty_isEquivalenceOver_comparison (hB : IsAlgebraicSpace 𝒞 S hS B)
    (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
    Nonempty (Functor.IsEquivalenceOver (projection hB G) (SheafTorsors.projection G.obj)
      (comparison hB G))

Sources

LeanSheafOfGroups.Torsors · SheafOfGroups.Torsors.Hom · SheafOfGroups.Torsors.instCategory · SheafOfGroups.Torsors.projection · SheafOfGroups.Torsors.isIso_of_isIso_base · SheafOfGroups.Torsors.projection_effectiveDescent · SheafOfGroups.Torsors.projection_isStackInGroupoids · SheafOfGroups.Torsors.projection_isFiberedInGroupoids

Section95.15 Quotients by group actions #

Section 95.15 of the Stacks Project, Tag 04UV. 5 tags here are carried by 17 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04WL, a situation

Tag 04WL in the Stacks Project.

AlgebraicGeometry.Space.GroupActionSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GroupActionSituation.lean, line 48.

Stacks Project, Tag 04WL. The data a quotient by a group action is formed from: a scheme S of a big fppf site, an algebraic space B over S, a group algebraic space G over B, an algebraic space X over B, and an action of G on X over B.

structure GroupActionSituation

Tag 0370, a lemma

Tag 0370 in the Stacks Project.

AlgebraicGeometry.Space.TorsorWithMap.projection_isStackInGroupoids_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorStackUnconditional.lean, line 260. The attribute's comment: “in Situation 04WL: the projection of [[X/G]] is a stack in groupoids for the fppf topology, with hB and G explicit”.

Stacks 0370: in Situation 04WL the projection p : [[X/G]] ⟶ (Sch/S)_fppf is a stack in groupoids for the fppf topology.

This is AlgebraicGeometry.Space.TorsorWithMap.projection_isStackInGroupoids_unconditional with hB and G explicit. The argument hX is part of Situation 04WL: [[X/G]] is formed for an arbitrary object X of Over B, and the situation asks that it be an algebraic space.

theorem projection_isStackInGroupoids_of_isAlgebraicSpace (X : Over B) [ModObj G.obj.X X]
    (hX : IsAlgebraicSpace 𝒞 S hS X.left) :
    Functor.IsStackInGroupoids.{w} (projection hB G X) (BigFppfOver.topology 𝒞 S hS)

AlgebraicGeometry.Space.TorsorWithMap.projection_isStackInGroupoids_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorsWithEquivariantMap.lean, line 997. The attribute's comment: “in Situation 04WL: the projection of [[X/G]] is a stack in groupoids for the fppf topology”.

In Situation 04WL the projection p : [[X/G]] ⟶ (Sch/S)_fppf is a stack in groupoids for the fppf topology.

theorem projection_isStackInGroupoids_unconditional
    (hX : IsAlgebraicSpace 𝒞 S hS X.left) :
    Functor.IsStackInGroupoids.{w} (projection hB G X) (BigFppfOver.topology 𝒞 S hS)

Tag 04WM, a proposition

Tag 04WM in the Stacks Project.

AlgebraicGeometry.Space.trivialTorsorWithMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TrivialTorsorWithMap.lean, line 278. The attribute's comment: “the trivial torsor with equivariant map attached to a point of X”.

Stacks 04WM, the trivial torsor with its equivariant map. The object of the category [[X/G]] of Situation 04WL attached to a point x : U ⟶ X of X: the trivial torsor G_U = U ×_{b, B} G over U, for b = x ≫ X.hom, with its left translation action, together with the G-equivariant morphism G_U ⟶ X, h ↦ h · x.

def trivialTorsorWithMap (U : BigFppfOver 𝒞 S hS) (x : yoneda.obj U ⟶ X.left) :
    TorsorWithMap hB G X

AlgebraicGeometry.Space.quotientStackTorsorEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackTorsorEquivalence.lean, line 187. The attribute's comment: “the canonical equivalence [X/G] ≌ [[X/G]] over the big fppf site, whose forward functor extends the explicit pointwise comparison F_p”.

The quotient stack [X/G] of the action of a group algebraic space G over an algebraic space B on an algebraic space X over B is canonically equivalent, over the big fppf site of S, to the stack [[X/G]] of fppf G-torsors with a G-equivariant map to X; and the forward 1-morphism of the equivalence extends the explicit pointwise comparison F_p of AlgebraicGeometry.Space.actionPointwiseComparison, the identification being a natural isomorphism all of whose components lie over identities of the site.

The source is the quotient stack of the action groupoid (X, G ×_B X, pr₁, a, m) of Stacks 0444, that is AlgebraicGeometry.Stack.quotientStackOfAction of Stacks 044Q part (2).

def quotientStackTorsorEquivalence :
    {e : StacksRepresentableCFG.EquivalenceOver
        (Stack.quotientStackOfAction ⟨B, hB⟩ G.obj.X X G.property hX).p
        (TorsorWithMap.projection hB G X) //
      ∃ α : Stack.pointwiseToQuotientStack
            (groupoidOfAction ⟨B, hB⟩ G.obj.X X G.property hX).groupoid ⋙ e.hom.functor ≅
          actionPointwiseComparison hB G X hX,
        ∀ A : (actionPointwiseCategory hB G X hX).obj,
          (TorsorWithMap.projection hB G X).IsHomLift (𝟙 A.base) (α.hom.app A)}

Tag 0CQJ, a lemma

Tag 0CQJ in the Stacks Project.

AlgebraicGeometry.Space.classifyingQuotientStackEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/ClassifyingStackEquivalences.lean, line 81. The attribute's comment: “the leg [B/G] ≌ [[B/G]] over the big fppf site, Stacks 04WM at X = B”.

Stacks 0CQJ, the leg [B/G] ≌ [[B/G]]. The quotient stack [B/G] of the trivial action of G on B (Stacks 044Q part (2), the quotient stack of the action groupoid of Stacks 0444) is equivalent over the big fppf site of S to [[B/G]], the stack of fppf G-torsors with an equivariant morphism to B. This is Stacks 04WM at X = B.

def classifyingQuotientStackEquivalence :
    StacksRepresentableCFG.EquivalenceOver
      (Stack.quotientStackOfAction ⟨B, hB⟩ G.obj.X (𝟙_ (Over B)) G.property hB).p
      (TorsorWithMap.projection hB G (𝟙_ (Over B)))

AlgebraicGeometry.Space.classifyingStackEquivalences, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/ClassifyingStackEquivalences.lean, line 152. The attribute's comment: “the whole lemma: [B/G] ≌ [[B/G]] ≌ G-Torsors ≌ 𝒢/ℬ-Torsors over the big fppf site, and G-Torsors ≌ G-Principal for G ⟶ B flat and locally of finite presentation, each with its canonical forward functor”.

Stacks 0CQJ. Let S be a scheme, B an algebraic space over S and G a group algebraic space over B. Then the stacks in groupoids over (Sch/S)_fppf [B/G], [[B/G]], G-Torsors and 𝒢/ℬ-Torsors are all canonically equivalent: this gives equivalences over the site [B/G] ≌ [[B/G]], [[B/G]] ≌ G-Torsors and G-Torsors ≌ 𝒢/ℬ-Torsors, and, if G ⟶ B is flat and locally of finite presentation, G-Torsors ≌ G-Principal.

Each is the canonical one: * the forward functor of [B/G] ≌ [[B/G]] extends the pointwise comparison F_p (AlgebraicGeometry.Space.actionPointwiseComparison) sending a point b : U ⟶ B to the trivial torsor, by a natural isomorphism lying over identities (Stacks 04WM at X = B); * the forward functor of [[B/G]] ≌ G-Torsors forgets the equivariant map to B; * the forward functor of G-Torsors ≌ 𝒢/ℬ-Torsors is the comparison functor of Stacks 04UT; * the forward functor of G-Torsors ≌ G-Principal is the canonical inclusion AlgebraicGeometry.Space.FppfTorsors.toPrincipal.

def classifyingStackEquivalences :
    { c : StacksRepresentableCFG.EquivalenceOver
          (Stack.quotientStackOfAction ⟨B, hB⟩ G.obj.X (𝟙_ (Over B)) G.property hB).p
          (TorsorWithMap.projection hB G (𝟙_ (Over B))) ×
        StacksRepresentableCFG.EquivalenceOver (TorsorWithMap.projection hB G (𝟙_ (Over B)))
          (FppfTorsors.projection hB G) ×
        StacksRepresentableCFG.EquivalenceOver (FppfTorsors.projection hB G)
          (SheafTorsors.projection G.obj) ×
        (IsFlat 𝒞 S hS G.obj.X.hom → IsLocallyOfFinitePresentation 𝒞 S hS G.obj.X.hom →
          StacksRepresentableCFG.EquivalenceOver (FppfTorsors.projection hB G)
            (PrincipalHomogeneousSpaces.projection hB G)) //
      (∃ α : Stack.pointwiseToQuotientStack
            (groupoidOfAction ⟨B, hB⟩ G.obj.X (𝟙_ (Over B)) G.property hB).groupoid ⋙
              c.1.hom.functor ≅
            actionPointwiseComparison hB G (𝟙_ (Over B)) hB,
          ∀ A : (actionPointwiseCategory hB G (𝟙_ (Over B)) hB).obj,
            (TorsorWithMap.projection hB G (𝟙_ (Over B))).IsHomLift (𝟙 A.base) (α.hom.app A)) ∧
        c.2.1.hom.functor =
          TorsorWithMap.forget hB G (𝟙_ (Over B)) ⋙ torsorObjComparisonInverse hB G ∧
        c.2.2.1.hom.functor = FppfTorsors.comparison hB G ∧
        ∀ hflat hlfp, (c.2.2.2 hflat hlfp).hom.functor = FppfTorsors.toPrincipal hB G }

AlgebraicGeometry.Space.fppfTorsorsEquivPrincipal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/FppfTorsorsPrincipalComparison.lean, line 102. The attribute's comment: “G-Torsors ≌ G-Principal, for G ⟶ B flat and locally of finite presentation”.

Stacks 0CQJ. For G ⟶ B flat and locally of finite presentation the canonical functor G-Torsors ⥤ G-Principal is an equivalence of categories, with quasi-inverse the functor reading a principal homogeneous space as an fppf torsor and with identity unit and counit.

def fppfTorsorsEquivPrincipal (hB : IsAlgebraicSpace 𝒞 S hS B)
    (G : GroupAlgebraicSpace 𝒞 S hS B hB) (hflat : IsFlat 𝒞 S hS G.obj.X.hom)
    (hlfp : IsLocallyOfFinitePresentation 𝒞 S hS G.obj.X.hom) :
    FppfTorsors hB G ≌ PrincipalHomogeneousSpaces hB G

AlgebraicGeometry.Space.FppfTorsors.nonempty_isEquivalenceOver_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparisonUnconditional.lean, line 67. The attribute's comment: “the 𝒢/ℬ-Torsors leg: G-Torsors ≌ 𝒢/ℬ-Torsors over the big fppf site”.

Stacks 04UT, with nothing carried, and with it the 𝒢/ℬ-Torsors leg of Stacks 0CQJ: the comparison functor G-Torsors ⥤ 𝒢/ℬ-Torsors is an equivalence of stacks in groupoids over the big fppf site of S.

The hypothesis every earlier rendering carried is the object half of Stacks 04U1, equivalently Stacks 04S6 part (3), which is now the theorem AlgebraicGeometry.Space.isBootstrapAlgebraicSpaceAlongFlatSurjection.

theorem nonempty_isEquivalenceOver_comparison (hB : IsAlgebraicSpace 𝒞 S hS B)
    (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
    Nonempty (Functor.IsEquivalenceOver (projection hB G) (SheafTorsors.projection G.obj)
      (comparison hB G))

AlgebraicGeometry.Space.torsorObjToTorsorWithMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorsWithEquivariantMap.lean, line 1108. The attribute's comment: “the functor G-Torsors ⥤ [[B/G]]”.

The canonical functor G-Torsors ⥤ [[B/G]], attaching to an fppf G-torsor its unique equivariant morphism to the base and to a morphism of torsors the same morphism.

def torsorObjToTorsorWithMap : TorsorObj hB G ⥤ TorsorWithMap hB G (𝟙_ (Over B))

AlgebraicGeometry.Space.torsorWithMapEquivTorsorObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorsWithEquivariantMap.lean, line 1140. The attribute's comment: “[[B/G]] ≌ G-Torsors”.

The category [[B/G]] of fppf G-torsors with an equivariant morphism to the base, that is the quotient category of the trivial action of G on B, is canonically equivalent to the category G-Torsors of fppf G-torsors; the equivalence forgets the equivariant morphism.

def torsorWithMapEquivTorsorObj : TorsorWithMap hB G (𝟙_ (Over B)) ≌ TorsorObj hB G

Declarations registered for the tag:

AlgebraicGeometry.Space.FppfTorsors.toPrincipal, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/FppfTorsorsPrincipalComparison.lean, line 70 (StacksFrontier): “the functor G-Torsors ⥤ G-Principal”.
AlgebraicGeometry.Space.FppfTorsors.comparison, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/TorsorComparisonFibred.lean, line 60 (StacksFrontier): “the canonical functor G-Torsors ⥤ 𝒢/ℬ-Torsors”.

Tag 0371, a remark

Tag 0371 in the Stacks Project.

AlgebraicGeometry.AbstractGroupQuotientStack, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStack.lean, line 104. The attribute's comment: “the objects of [[X/G]]”.

Stacks 0371. An object of the quotient [[X/G]] of a sheaf X by an abstract group G: an object U of (Sch/S)_fppf, a torsor on (Sch/U)_fppf under the constant sheaf of groups with value G, and a G-equivariant map of sheaves from it to X.

structure AbstractGroupQuotientStack

AlgebraicGeometry.AbstractGroupQuotientStack.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStack.lean, line 162. The attribute's comment: “the morphisms of [[X/G]]”.

Stacks 0371. A morphism (U, P, φ) ⟶ (U', P', φ') of the quotient [[X/G]]: a morphism f : U ⟶ U' of (Sch/S)_fppf together with a G-equivariant isomorphism g : P → f^{-1}P' of torsors under the constant sheaf of groups with value G, compatible with φ and φ'. The isomorphism is recorded on total spaces: g is a map of sheaves on (Sch/S)_fppf over f restricting to a bijection from the fibre of P over each a : V ⟶ U to the fibre of P' over a ≫ f.

structure Hom (A A' : AbstractGroupQuotientStack B S hS G X ρ)

AlgebraicGeometry.AbstractGroupQuotientStack.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStack.lean, line 226. The attribute's comment: “the category [[X/G]]”.

Stacks 0371. The quotient [[X/G]] of a sheaf X by an abstract group G is a category: morphisms compose by composing f and g.

instance instCategory : Category (AbstractGroupQuotientStack B S hS G X ρ)

AlgebraicGeometry.AbstractGroupQuotientStack.projection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStack.lean, line 237. The attribute's comment: “the functor to the big fppf site”.

Stacks 0371. The functor [[X/G]] ⥤ (Sch/S)_fppf sending a triple (U, P, φ) to U, which is how [[X/G]] is regarded as a category over the big fppf site of S.

def projection :
    AbstractGroupQuotientStack B S hS G X ρ ⥤ BigFppfOver B S hS

AlgebraicGeometry.nonempty_isEquivalenceOver_abstractGroupQuotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackEquivalence.lean, line 478. The attribute's comment: “the equivalence of [[X/G]] with [[X/G_S]]”.

Let G be an abstract group whose constant group scheme G_S lies in the big fppf site, X an algebraic space over S and ρ : G →* Aut X an action. Then the stack [[X/G]] of triples (U, P, φ), P a torsor under the constant sheaf G on (Sch/U)_fppf and φ : P → X equivariant, is equivalent over (Sch/S)_fppf to the stack [[X/G_S]], for G_S the constant group algebraic space AlgebraicGeometry.Space.constantGroupSpace acting on X through ρ (AlgebraicGeometry.Space.constGSModObj, whose constant sections act as ρ does by AlgebraicGeometry.Space.constGS_isCompatibleAction).

theorem nonempty_isEquivalenceOver_abstractGroupQuotientStack :
    letI : ModObj (constantGroupSpace 𝒞 S hS G (baseS 𝒞 S hS) (isAlgebraicSpace_baseS 𝒞 S hS)
        hG).obj.X (overBaseS X₀) := constGSModObj hG hX.isSheaf ρ₀
    ∃ F : TorsorWithMap (isAlgebraicSpace_baseS 𝒞 S hS)
        (constantGroupSpace 𝒞 S hS G (baseS 𝒞 S hS) (isAlgebraicSpace_baseS 𝒞 S hS) hG)
        (overBaseS X₀) ⥤
      AbstractGroupQuotientStack.{max t (u + 1)} 𝒞 S hS G (X₀ ⋙ uliftFunctor.{max t (u + 1)})
        (uliftAction.{max t (u + 1)} ρ₀),
      Nonempty (Functor.IsEquivalenceOver
        (TorsorWithMap.projection (isAlgebraicSpace_baseS 𝒞 S hS)
          (constantGroupSpace 𝒞 S hS G (baseS 𝒞 S hS) (isAlgebraicSpace_baseS 𝒞 S hS) hG)
          (overBaseS X₀))
        AbstractGroupQuotientStack.projection F)

AlgebraicGeometry.AbstractGroupQuotientStack.projection_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackIsStack.lean, line 772. The attribute's comment: “[[X/G]] is a stack in groupoids over (Sch/S)_fppf”.

Stacks 0371. For an algebraic space X over S with an action ρ : G →* Aut X of an abstract group G, the functor [[X/G]] ⥤ (Sch/S)_fppf of AlgebraicGeometry.AbstractGroupQuotientStack.projection turns [[X/G]] into a stack in groupoids over the big fppf site of S.

This is the assertion of the remark, under exactly its standing hypothesis that X is an algebraic space over S: nothing beyond the sheaf condition for X is used, and the three conditions of Stacks 02ZI are proved outright, with the stack property of the torsors under the constant sheaf of groups supplied by Stacks 04UK rather than assumed.

theorem projection_isStackInGroupoids
    (hX : Space.IsAlgebraicSpaceULift.{max t (u + 1)} B S hS X) :
    Functor.IsStackInGroupoids.{w}
      (projection : AbstractGroupQuotientStack.{max t (u + 1)} B S hS G X ρ ⥤
        BigFppfOver B S hS) (BigFppfOver.topology B S hS)

Declarations registered for the tag:

AlgebraicGeometry.constantGroupSheafRepresentedByConstantGroupScheme_bigFppf, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackIsStack.lean, line 88 (StacksFrontier): “the constant sheaf G is representable by G_S on (Sch/S)_fppf”.

Sources

Section95.16 The Picard stack #

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

Tag 0372, the section

Tag 0372 in the Stacks Project.

AlgebraicGeometry.Space.PicardObject, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStack.lean, line 252. The attribute's comment: “the objects of the Picard stack”.

Section 0372, the objects of Picardstack_{X/B}. A triple (U, b, L): a scheme U of the site with a morphism b : U ⟶ B to the base, and an invertible module L on the base change X_U.

structure PicardObject (s : PicardSituation B S hS)

AlgebraicGeometry.Space.PicardHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStack.lean, line 264. The attribute's comment: “the morphisms of the Picard stack”.

Section 0372, the morphisms of Picardstack_{X/B}. A pair (f, g): a morphism f : U ⟶ U' of schemes over the base, and an isomorphism g : f^*L' ⟶ L of modules on X_U.

structure PicardHom {s : PicardSituation B S hS} (A C : PicardObject s)

AlgebraicGeometry.Space.PicardHom.id, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStack.lean, line 294. The attribute's comment: “the identity, conditional on the pseudofunctoriality of the direct images of Stacks 03LU”.

Section 0372, the identity of an object. The identity of its pair (U, b), with the unit law (X_{𝟙 U})^* ≅ 𝟭 of Stacks 03LU as its comparison of modules.

def id (hc : ModulePushforwardCoherence B S hS) (A : PicardObject s) : PicardHom A A

AlgebraicGeometry.Space.PicardHom.comp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStack.lean, line 303. The attribute's comment: “the composition”.

Section 0372, the composition (f, g) with (f', g') is (f' ∘ f, g ∘ f^*(g')). The composite of the base maps, with the inverse image of the second comparison followed by the first, read through the comparison of Stacks 03LU for the composite.

def comp (m : PicardHom A C) (n : PicardHom C D) : PicardHom A D

AlgebraicGeometry.Space.PicardHom.id_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 243. The attribute's comment: “the identity law at the source for the composition of the Picard stack”.

Section 0372, the identity law at the source. Composing a morphism of Picardstack_{X/B} with the identity of its source returns it.

theorem id_comp (hc : ModulePushforwardCoherence B S hS) {A C : PicardObject s}
    (m : PicardHom A C) : PicardHom.comp (PicardHom.id hc A) m = m

AlgebraicGeometry.Space.PicardHom.comp_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 253. The attribute's comment: “the identity law at the target for the composition of the Picard stack”.

Section 0372, the identity law at the target. Composing a morphism of Picardstack_{X/B} with the identity of its target returns it.

theorem comp_id (hc : ModulePushforwardCoherence B S hS) {A C : PicardObject s}
    (m : PicardHom A C) : PicardHom.comp m (PicardHom.id hc C) = m

AlgebraicGeometry.Space.PicardHom.comp_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 262. The attribute's comment: “associativity of the composition of the Picard stack”.

Section 0372, associativity. The composition of Picardstack_{X/B} is associative.

theorem comp_assoc (hc : ModulePushforwardCoherence B S hS) {A C D E : PicardObject s}
    (m : PicardHom A C) (n : PicardHom C D) (p : PicardHom D E) :
    PicardHom.comp (PicardHom.comp m n) p = PicardHom.comp m (PicardHom.comp n p)

AlgebraicGeometry.Space.picardCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 286. The attribute's comment: “the category Picardstack_{X/B}, conditional on the pseudofunctoriality of the direct images of Stacks 03LU that its identity already needs”.

Section 0372, the category Picardstack_{X/B}. The objects are the triples (U, b, L), the morphisms are the pairs (f, g) of a morphism of test schemes over the base and an isomorphism f^*L' ≅ L, and the identities and the composition are the ones of Section 0372.

def picardCategory (hc : ModulePushforwardCoherence B S hS) (s : PicardSituation B S hS) :
    Category.{u + 1} (PicardObject s)

AlgebraicGeometry.Space.picardProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 298. The attribute's comment: “the projection of the Picard stack to the test schemes over the base”.

Section 0372, the functor p. The projection of Picardstack_{X/B} to the test schemes over the base, forgetting the invertible module.

def picardProjection (hc : ModulePushforwardCoherence B S hS) (s : PicardSituation B S hS) :
    letI : Category.{u + 1} (PicardObject s) := picardCategory hc s
    PicardObject s ⥤ s.SchemesOver

AlgebraicGeometry.Space.picardCategoryData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackCategory.lean, line 312. The attribute's comment: “a value of the specification of the category Picardstack_{X/B} with its projection, conditional on the pseudofunctoriality of the direct images of Stacks 03LU”.

Section 0372. The category Picardstack_{X/B} together with its projection satisfies the specification AlgebraicGeometry.Space.PicardCategoryData: its hom-sets, identities, composition and projection are the ones of Section 0372.

def picardCategoryData (hc : ModulePushforwardCoherence B S hS)
    (s : PicardSituation B S hS) : PicardCategoryData hc s

Tag 04WN, a lemma

Tag 04WN in the Stacks Project.

AlgebraicGeometry.Space.picardProjection_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackFibered.lean, line 385. The attribute's comment: “condition (1) of Stacks 02ZI only — the functor Picardstack_{X/B} ⟶ (Sch/S)_fppf is fibred in groupoids — and conditional on the category of Section 0372; conditions (2) and (3) need Stacks 04W8, which this development does not carry”.

Condition (1) of Stacks 02ZI for the functor of Stacks 04WN. In Situation 0D25 the projection p : Picardstack_{X/B} ⟶ (Sch/S)_fppf of Section 0372, which sends an object (U, b, L) to its test scheme U, is fibred in groupoids.

The projection of Picardstack_{X/B} to the test schemes over the base is fibred in groupoids by AlgebraicGeometry.Space.picardProjection_isFiberedInGroupoids_schemesOver, the projection of the test schemes over the base to the schemes of the site is fibred in groupoids by CategoryTheory.Functor.IsFiberedInGroupoids.costructuredArrow_proj, and Stacks 09WW composes the two.

This carrier asserts the first of the three conditions of Stacks 02ZI, and asserts it conditionally. Stacks 04WN is the conjunction of all three for this functor, and conditions (2) and (3) — the Isom presheaves being sheaves, and effectivity of descent data — are not proved here: the source proves them by citing Descent on Spaces, Proposition 74.4.1 (Stacks 04W8), fpqc descent of quasi-coherent modules on algebraic spaces, which this development does not carry. Of the hypotheses, cd is the category of Section 0372, which the source introduces by designation, and hc is the pseudofunctoriality of Stacks 03LU that its identities and composition already need. The attribute is qualified accordingly, and no unqualified 04WN claim is made here. The source's "up to a replacement as in Remark 03ZZ" clause needs nothing: see the implementation notes of the file.

theorem picardProjection_isFiberedInGroupoids (hc : ModulePushforwardCoherence B S hS)
    {s : PicardSituation B S hS} (cd : PicardCategoryData hc s) :
    letI : Category.{u + 1} (PicardObject s) := cd.category
    Functor.IsFiberedInGroupoids
      (cd.projection ⋙ CostructuredArrow.proj (schemeSpaceFunctor B S hS) s.base)

AlgebraicGeometry.Space.picardBasedCategory_isStackInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackIsStack.lean, line 71. The attribute's comment: “the functor Picardstack_{X/B} ⟶ (Sch/S)_fppf is a stack in groupoids: all three conditions of Stacks 02ZI”.

Stacks 04WN. In Situation 0D25, the functor p : Picardstack_{X/B} ⟶ (Sch/S)_fppf of Section 0372, sending (U, b, L) to U, is a stack in groupoids over the big fppf site of S: it is fibred in groupoids, its Isom presheaves are sheaves, and every descent datum relative to an fppf covering is effective.

The statement is made for p itself rather than for the cutdown of Stacks 03ZZ, the objects of Picardstack_{X/B} forming a type.

theorem picardBasedCategory_isStackInGroupoids (s : PicardSituation B S hS) :
    Functor.IsStackInGroupoids.{w} (picardBasedCategory (modulePushforwardCoherence B S hS) s).p
      (BigFppfOver.topology B S hS)

Sources

LeanAlgebraicGeometry.Space.PicardObject · AlgebraicGeometry.Space.PicardHom · AlgebraicGeometry.Space.PicardHom.id · AlgebraicGeometry.Space.PicardHom.comp · AlgebraicGeometry.Space.PicardHom.id_comp · AlgebraicGeometry.Space.PicardHom.comp_id · AlgebraicGeometry.Space.PicardHom.comp_assoc · AlgebraicGeometry.Space.picardCategory

Section95.17 Examples of inertia stacks #

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

Tag 0374, an example

Tag 0374 in the Stacks Project.

AlgebraicGeometry.fixedScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientInertia.lean, line 166. The attribute's comment: “the fixed-point scheme X^g as the displayed fibre product”.

Stacks 0374. The fixed-point scheme Y^g = {y ∈ Y | g(y) = y} of the automorphism of Y attached to a group element g, as the fibre product Y^g = Y ×_{(1, 1), Y ×_S Y, (g, 1)} Y displayed in the source.

def fixedScheme (Y : Over S) (a : G →* Aut Y) (g : G) : Over S

AlgebraicGeometry.fixedSchemeHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientInertia.lean, line 221. The attribute's comment: “X^g = {x ∈ X | g(x) = x} as a functor of points”.

Stacks 0374. The fibre product Y ×_{(1, 1), Y ×_S Y, (g, 1)} Y is the locus Y^g = {y ∈ Y | g(y) = y}: its T-points are exactly the T-points of Y fixed by the automorphism attached to g.

def fixedSchemeHomEquiv (Y : Over S) (a : G →* Aut Y) (g : G) (T : Over S) :
    (T ⟶ fixedScheme S G Y a g) ≃ {x : T ⟶ Y // x ≫ (a g).asIso.hom = x}

AlgebraicGeometry.fixedSchemeAut, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientInertia.lean, line 271. The attribute's comment: “the induced action of G on X^g”.

Stacks 0374. The action of G on the fixed-point scheme Y^g induced by the action on Y. It is here that commutativity of G enters: for h ∈ G the automorphism of Y attached to h commutes with the one attached to g, hence preserves Y^g.

def fixedSchemeAut (Y : Over S) (a : G →* Aut Y) (g : G) :
    G →* Aut (fixedScheme S G Y a g)

AlgebraicGeometry.totalToTarget_factorsThroughFixedScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientInertia.lean, line 599. The attribute's comment: “φ ∘ α = φ makes φ factor through the inclusion of X^g in X”.

Stacks 0374. The source's sentence "the condition that φ ∘ α = φ means that φ factors through the inclusion of Y^g in Y": for an object of [Y/G] whose equivariant map is fixed by g, every value of that map factors uniquely through Y^g.

theorem totalToTarget_factorsThroughFixedScheme (g : G)
    (A : schemeQuotient.{t} B S hS G Y a)
    (hA : ∀ (V : (BigFppfOver B S hS)ᵒᵖ) (p : A.Total V),
      (schemePointsAut B S hS G Y a g).asIso.hom.app V (A.totalToTarget V p) =
        A.totalToTarget V p)
    (V : (BigFppfOver B S hS)ᵒᵖ) (p : A.Total V) :
    ∃! y : (Over.post B.inclusion).obj V.unop ⟶ fixedScheme S G Y a g,
      y ≫ fixedSchemeIncl S G Y a g = A.totalToTarget V p

AlgebraicGeometry.fixedQuotientToInertia, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientInertia.lean, line 616. The attribute's comment: “the g-th summand of the morphism to the inertia stack”.

Stacks 0374. The morphism [Y^g/G] → I_{[Y/G]} of the source: a torsor P with a G-equivariant map ψ : P → Y^g goes to the triple (P, ι ∘ ψ) together with the automorphism given by multiplication by g on P.

def fixedQuotientToInertia (g : G) :
    fixedSchemeQuotient.{t} B S hS G Y a g ⥤
      AbsoluteInertia (schemeQuotientProjection.{t} B S hS G Y a)

AlgebraicGeometry.AbstractGroupQuotientStack.inertiaComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientInertia.lean, line 645. The attribute's comment: “the morphism from the disjoint union of the [X^g/G] to the inertia stack”.

Stacks 0374. The morphism ∐_{g ∈ G} [Y^g/G] → I_{[Y/G]} of the source, assembled from its summands. On T-points it is the source's recipe: a G-torsor P → T with a G-equivariant ψ : P → Y^g is sent to (P, ι ∘ ψ, α) with α multiplication by g.

def inertiaComparison :
    (Σ g : G, fixedSchemeQuotient.{t} B S hS G Y a g) ⥤
      AbsoluteInertia (schemeQuotientProjection.{t} B S hS G Y a)

AlgebraicGeometry.AbstractGroupQuotientStack.inertiaComparison_comp_struct, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientInertia.lean, line 662. The attribute's comment: “the comparison is a morphism over the big fppf site”.

Stacks 0374. The comparison morphism is a morphism over (Sch/S)_fppf: on each summand, composing it with the structure functor of the inertia gives back the projection of [Y^g/G] to the site, since neither the inclusion Y^g → Y nor remembering the automorphism α changes the object of the site attached to a triple.

lemma inertiaComparison_comp_struct (g : G) :
    Sigma.incl g ⋙ inertiaComparison.{t} B S hS G Y a ⋙
        relativeInertiaStruct (schemeQuotientProjection.{t} B S hS G Y a)
          (schemeQuotientProjection.{t} B S hS G Y a) =
      schemeQuotientProjection.{t} B S hS G (fixedScheme S G Y a g)
        (fixedSchemeAut Y a g)

AlgebraicGeometry.inertia_equivalence_stackCoproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientInertiaEquivalence.lean, line 313. The attribute's comment: “I_{[X/G]} = ∐_{g ∈ G} [X^g/G]: an equivalence over (Sch/S)_fppf from the coproduct of stacks to the inertia stack, restricting on each summand to the canonical functor”.

Stacks 0374. Let S be a scheme, G a commutative group, Y → S a scheme over S and a : G →* Aut_S(Y) an action of G on Y. Then the inertia stack of [Y/G] is the coproduct of stacks I_{[Y/G]} = ∐_{g ∈ G} [Y^g/G], where Y^g = Y ×_{(1, 1), Y ×_S Y, (g, 1)} Y is the fixed-point scheme of g (AlgebraicGeometry.fixedScheme) with the action of G induced by a: there is an equivalence of categories over (Sch/S)_fppf (a quasi-inverse over (Sch/S)_fppf with unit and counit lying over identities) from the coproduct of stacks ∐_{g ∈ G} [Y^g/G] to I_{[Y/G]}, whose restriction to the g-th summand [Y^g/G] is the canonical functor of the source, sending a torsor P with an equivariant map P → Y^g to P with the composite map to Y and the automorphism given by multiplication by g.

theorem inertia_equivalence_stackCoproduct :
    ∃ H : Functor.StackCoproduct
        (fun g : G => schemeQuotientProjection.{max (u + 1) t} B S hS G (fixedScheme S G Y a g)
          (fixedSchemeAut Y a g))
        (BigFppfOver.topology B S hS) (fun _ => projection_isFiberedInGroupoids) ⥤
        AbsoluteInertia (schemeQuotientProjection.{max (u + 1) t} B S hS G Y a),
      Nonempty (Functor.IsEquivalenceOver (Functor.stackCoproductProj _ _ _)
        (schemeInertiaProj.{max (u + 1) t} B S hS G Y a) H) ∧
      ∀ g : G, Nonempty (Functor.stackCoproductι _ _ _ g ⋙ H ≅
        fixedQuotientToInertia.{max (u + 1) t} B S hS G Y a g)

AlgebraicGeometry.isPullback_fixedPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackInertia.lean, line 181. The attribute's comment: “the fixed locus as a fibre product”.

Stacks 0374. The fixed subpresheaf X^σ is the fibre product X ×_{(1,1), X × X, (σ,1)} X displayed in the source. On presheaves over the big fppf site of S the binary product is the fibre product over S, as S is the terminal object.

theorem isPullback_fixedPresheaf (σ : X ⟶ X) :
    IsPullback (fixedPresheafIncl σ) (fixedPresheafIncl σ)
      (prod.lift (𝟙 X) (𝟙 X)) (prod.lift σ (𝟙 X))

AlgebraicGeometry.fixedPresheafAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackInertia.lean, line 263. The attribute's comment: “the induced action on the fixed locus”.

Stacks 0374. Because G is commutative, its action on X restricts to an action on the fixed locus X^g. This is what makes the quotient [X^g/G] of the source's formula meaningful.

def fixedPresheafAction (ρ : G →* Aut X) (g : G) : G →* Aut (fixedPresheaf (ρ g).asIso.hom)

AlgebraicGeometry.fixedQuotientStack, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackInertia.lean, line 353. The attribute's comment: “the quotient of the fixed locus”.

Stacks 0374. The quotient [X^g/G] of the fixed locus X^g by G, formed by the construction of Stacks 0371 applied to X^g with its induced action.

abbrev fixedQuotientStack (g : G) : Type _

AlgebraicGeometry.inertiaSummand, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackInertia.lean, line 405. The attribute's comment: “the canonical functor to the inertia stack”.

Stacks 0374. The canonical functor [X^g/G] ⥤ I_{[X/G]}: a torsor with an equivariant map to X^g is sent to the same torsor, mapping to X, together with the automorphism given by translation by g.

def inertiaSummand (g : G) :
    fixedQuotientStack B S hS G X ρ g ⥤ quotientInertia B S hS G X ρ

AlgebraicGeometry.inertiaSummandLift_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackInertia.lean, line 514. The attribute's comment: “the g-summand of the inertia stack”.

Stacks 0374. I_{[X/G]} = ∐_{g ∈ G} [X^g/G], summand by summand: for each g ∈ G the canonical functor is an equivalence from the quotient [X^g/G] of the fixed locus onto the part of the inertia stack of [[X/G]] on which the automorphism is translation by g. Objects correspond because φ ∘ α = φ says that φ factors through X^g → X, and morphisms correspond because a morphism of [[X/G]] is G-equivariant.

theorem inertiaSummandLift_isEquivalence (g : G) :
    (inertiaSummandLift (ρ := ρ) g).IsEquivalence

AlgebraicGeometry.inertiaSummandLift_comp_structure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackInertia.lean, line 520. The attribute's comment: “the g-summand is an equivalence over the base”.

The equivalence of Stacks 0374 is an equivalence over (Sch/S)_fppf: it carries the projection of [X^g/G] to the structure functor of the inertia stack.

theorem inertiaSummandLift_comp_structure (g : G) :
    inertiaSummandLift (ρ := ρ) g ⋙ ObjectProperty.ι (IsTranslationBy (ρ := ρ) g) ⋙
        relativeInertiaStruct
          (AbstractGroupQuotientStack.projection (B := B) (S := S) (hS := hS) (G := G)
            (X := X) (ρ := ρ))
          (AbstractGroupQuotientStack.projection (B := B) (S := S) (hS := hS) (G := G)
            (X := X) (ρ := ρ)) =
      AbstractGroupQuotientStack.projection (B := B) (S := S) (hS := hS) (G := G)
        (X := fixedPresheaf (ρ g).asIso.hom) (ρ := fixedPresheafAction ρ g)

AlgebraicGeometry.inertiaCoproduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackInertia.lean, line 535. The attribute's comment: “the disjoint union of the quotients of the fixed loci”.

Stacks 0374. The disjoint union ∐_{g ∈ G} [X^g/G] of the quotients of the fixed loci, mapping to the inertia stack of [[X/G]]; on the g-summand this is AlgebraicGeometry.inertiaSummand.

def inertiaCoproduct :
    (Σ g : G, fixedQuotientStack B S hS G X ρ g) ⥤ quotientInertia B S hS G X ρ

AlgebraicGeometry.incl_comp_inertiaCoproduct_comp_structure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackInertia.lean, line 546. The attribute's comment: “the coproduct over the base”.

The coproduct of Stacks 0374 maps to the inertia stack over (Sch/S)_fppf: on each summand it carries the projection of [X^g/G] to the structure functor of the inertia.

theorem incl_comp_inertiaCoproduct_comp_structure (g : G) :
    Sigma.incl g ⋙ inertiaCoproduct (ρ := ρ) ⋙
        relativeInertiaStruct
          (AbstractGroupQuotientStack.projection (B := B) (S := S) (hS := hS) (G := G)
            (X := X) (ρ := ρ))
          (AbstractGroupQuotientStack.projection (B := B) (S := S) (hS := hS) (G := G)
            (X := X) (ρ := ρ)) =
      AbstractGroupQuotientStack.projection (B := B) (S := S) (hS := hS) (G := G)
        (X := fixedPresheaf (ρ g).asIso.hom) (ρ := fixedPresheafAction ρ g)

AlgebraicGeometry.existsUnique_auto_eq_totalSmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/AbstractGroupQuotientStackInertia.lean, line 563. The attribute's comment: “the automorphism is a translation”.

Stacks 0374. Conversely to AlgebraicGeometry.inertiaSummand: the automorphism α of an object (P/T, φ, α) of I_{[X/G]} is, at every section of its torsor, translation by a unique section of the constant sheaf of groups with value G. Commutativity of G is not needed for this step; what it buys is that the section is independent of the chosen point, which is why the summands of the formula are indexed by G.

theorem existsUnique_auto_eq_totalSmul (Z : quotientInertia B S hS G X ρ)
    (V : (BigFppfOver B S hS)ᵒᵖ) (p : Z.obj.Total V) :
    ∃! γ : (constantSheafOfGroups (BigFppfOver.topology B S hS) G).presheaf.obj V,
      Z.obj.totalSmul γ p = Z.auto.asIso.hom.map V p

Tag 0375, an example

Tag 0375 in the Stacks Project.

AlgebraicGeometry.Space.verticalEquivAut, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackInertia.lean, line 194. The attribute's comment: “the points of the inertia stack of the Picard stack over a test scheme are the pairs of an invertible module on the base change and an automorphism of it”.

The data α of a point (L, α) of the inertia stack of Picardstack_{X/B} is an automorphism of the invertible module L.

A morphism of Picardstack_{X/B} from (U, b, L) to itself consists of a base map and an isomorphism (X_{base})^*L ⟶ L; when the base map is the identity the unit comparison (X_{𝟙 U})^* ≅ 𝟭 of Stacks 03LU turns that isomorphism into an automorphism of L, and every automorphism of L arises from exactly one such morphism.

def verticalEquivAut (hc : ModulePushforwardCoherence B S hS) {s : PicardSituation B S hS}
    (A : PicardObject s) : A.Vertical ≃ (A.lineBundle ≅ A.lineBundle)

AlgebraicGeometry.Space.autLineBundleMulEquivAutStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackInertia.lean, line 242. The attribute's comment: “an automorphism of an invertible module on the base change is an invertible global function on the base change, so the automorphism group is independent of the module”.

The automorphism group of the invertible module of an object of Picardstack_{X/B} is the automorphism group of the structure sheaf of the base change.

def autLineBundleMulEquivAutStructure {s : PicardSituation B S hS} (A : PicardObject s) :
    Aut A.lineBundle ≃* Aut (structureModule (s.baseChange A.T))

AlgebraicGeometry.Space.PicardObject.autMulEquivMultiplicativeGroupPoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackInertia.lean, line 692. The attribute's comment: “the 𝐆_m factor of the inertia stack: when 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every test scheme T, the automorphism group of the invertible module of an object of the Picard stack over T is 𝐆_{m,S}(T)”.

The 𝐆_m factor of the inertia stack, as an explicit isomorphism of groups. When 𝒪_T ⟶ f_{T, *}𝒪_{X_T} is an isomorphism for every test scheme T, the automorphism group of the invertible module of an object of Picardstack_{X/B} over T is 𝐆_{m, S}(T): an automorphism is multiplication by a unique invertible regular function on T (AlgebraicGeometry.Space.PicardObject.bijective_unitsToAut), and H^0(T, 𝒪_T^*) is 𝐆_{m, S}(T) by Stacks 022U.

def autMulEquivMultiplicativeGroupPoints (h : s.StructureSheafMapIso) (A : PicardObject s) :
    Aut A.lineBundle ≃* multiplicativeGroupPointsAt B S hS A.T.left

AlgebraicGeometry.Space.PicardObject.verticalEquivMultiplicativeGroupPoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackInertia.lean, line 718. The attribute's comment: “the points of the inertia stack above an object of the Picard stack over T are 𝐆_{m,S}(T), when 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every test scheme T”.

The points of the inertia stack. When 𝒪_T ⟶ f_{T, *}𝒪_{X_T} is an isomorphism for every test scheme T, the endomorphisms of an object (T, b, L) of Picardstack_{X/B} lying over the identity of T — the points (L, α) of the inertia stack above it — are the points 𝐆_{m, S}(T) of the multiplicative group: α is an automorphism of L (AlgebraicGeometry.Space.verticalEquivAut, for the comparisons of Stacks 03LU of the library, AlgebraicGeometry.Space.modulePushforwardCoherence), which is multiplication by a unique invertible function on T (AlgebraicGeometry.Space.PicardObject.autMulEquivMultiplicativeGroupPoints).

def verticalEquivMultiplicativeGroupPoints (h : s.StructureSheafMapIso) (A : PicardObject s) :
    A.Vertical ≃ multiplicativeGroupPointsAt B S hS A.T.left

AlgebraicGeometry.Space.nonempty_autLineBundle_mulEquiv_multiplicativeGroupPoints_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackInertiaCoordinates.lean, line 241. The attribute's comment: “the 𝐆_m factor of the inertia stack: under the hypothesis that 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every test scheme T, the automorphism group of the invertible module of an object of the Picard stack over T is 𝐆_{m,S}(T)”.

The 𝐆_m factor of the inertia stack. Assume that for every test scheme T over the base the structure map 𝒪_T ⟶ f_{T, *}𝒪_{X_T} of the base change is an isomorphism. Then for every object (U, b, L) of Picardstack_{X/B} the automorphism group of L is the group 𝐆_{m, S}(U).

theorem nonempty_autLineBundle_mulEquiv_multiplicativeGroupPoints_of_iso
    (h : s.StructureSheafMapIso) (A : PicardObject s) :
    Nonempty (Aut A.lineBundle ≃* multiplicativeGroupPointsAt B S hS A.T.left)

AlgebraicGeometry.Space.nonempty_vertical_equiv_multiplicativeGroupPoints_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackInertiaCoordinates.lean, line 254. The attribute's comment: “the points of the inertia stack above an object of the Picard stack over T are 𝐆_{m,S}(T), under the hypothesis that 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every test scheme T”.

The points of the inertia stack. Assume that for every test scheme T over the base the structure map 𝒪_T ⟶ f_{T, *}𝒪_{X_T} of the base change is an isomorphism. Then the endomorphisms of an object (U, b, L) of Picardstack_{X/B} lying over the identity of U — the points of the inertia stack above it — are the points 𝐆_{m, S}(U).

theorem nonempty_vertical_equiv_multiplicativeGroupPoints_of_iso
    (hc : ModulePushforwardCoherence B S hS) (h : s.StructureSheafMapIso) (A : PicardObject s) :
    Nonempty (A.Vertical ≃ multiplicativeGroupPointsAt B S hS A.T.left)

AlgebraicGeometry.Space.nonempty_equivalenceOver_picardInertia_multiplicativeGroupProduct_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardStackInertiaCoordinates.lean, line 471. The attribute's comment: “the inertia stack of the Picard stack is 𝐆_{m,S} ×_S Picardstack_{X/B}, as categories over (Sch/S)_fppf, when 𝒪_T ⟶ f_{T,*}𝒪_{X_T} is an isomorphism for every test scheme T”.

Let f : X ⟶ B be a morphism of algebraic spaces over S such that for every scheme T over B the structure map 𝒪_T ⟶ f_{T, *}𝒪_{X_T} of the base change f_T : X_T ⟶ T is an isomorphism. Then the inertia stack of the Picard stack Picardstack_{X/B} of Section 0372 is

I_{Picardstack_{X/B}} = 𝐆_{m, S} ×_S Picardstack_{X/B}

as a category over (Sch/S)_fppf: the two are equivalent over the big fppf site, by an equivalence which is the identity on the Picardstack_{X/B}-factor and sends a point (L, α) of the inertia over T to the point of 𝐆_{m, S}(T) = H^0(T, 𝒪_T^*) that the automorphism α of L is multiplication by.

In Stacks 0375 f is a morphism of schemes; here it is a morphism of algebraic spaces, which contains that case. "Equal" is read as an equivalence over the site (CategoryTheory.StacksRepresentableCFG.EquivalenceOver), and the product is the 2-fibre product CategoryTheory.inertiaPresheafProduct of the category of elements of 𝐆_{m, S} with Picardstack_{X/B} over the site.

theorem nonempty_equivalenceOver_picardInertia_multiplicativeGroupProduct_of_iso
    (s : PicardSituation B S hS) (h : s.StructureSheafMapIso) :
    letI : Category.{u + 1} (PicardObject s) :=
      (picardCategoryData (modulePushforwardCoherence B S hS) s).category
    Nonempty (StacksRepresentableCFG.EquivalenceOver
      (relativeInertiaStruct
        (picardCategoryData (modulePushforwardCoherence B S hS) s).siteProjection
        (picardCategoryData (modulePushforwardCoherence B S hS) s).siteProjection)
      (inertiaPresheafProductStruct
        (picardCategoryData (modulePushforwardCoherence B S hS) s).siteProjection
        (multiplicativeGroupPresheaf B S hS)))

Sources

LeanAlgebraicGeometry.fixedScheme · AlgebraicGeometry.fixedSchemeHomEquiv · AlgebraicGeometry.fixedSchemeAut · AlgebraicGeometry.totalToTarget_factorsThroughFixedScheme · AlgebraicGeometry.fixedQuotientToInertia · AlgebraicGeometry.AbstractGroupQuotientStack.inertiaComparison · AlgebraicGeometry.AbstractGroupQuotientStack.inertiaComparison_comp_struct · AlgebraicGeometry.inertia_equivalence_stackCoproduct

Section95.18 Finite Hilbert stacks #

Section 95.18 of the Stacks Project, Tag 05WA. 4 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05WB, a lemma

Tag 05WB in the Stacks Project.

AlgebraicGeometry.Stack.isStackInGroupoids_finiteCoverProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/FiniteCoverStack.lean, line 47. The attribute's comment: “The category ℋ_d of degree-d finite locally free covers, i.e. the case 𝒳 = 𝒴 = S of the source's ℋ_d(𝒳/𝒴), is a stack in groupoids over the big fppf site of S. All three conditions of Stacks 02ZI are discharged: condition (1) is AlgebraicGeometry.Stack.isFiberedInGroupoids_finiteCoverProjection, condition (2) is AlgebraicGeometry.Stack.isom_isSheaf_finiteCoverProjection, and condition (3), effectivity of descent data, is AlgebraicGeometry.Stack.descentDatum_isEffective_finiteCoverProjection.”. References: SGA 3 IV (4.5.13), “special case”.

The category ℋ_d of degree-d finite locally free covers is a stack in groupoids over the big fppf site of S.

theorem isStackInGroupoids_finiteCoverProjection :
    (finiteCoverProjection (B := B) (S := S) (hS := hS) (d := d)).IsStackInGroupoids.{w}
      (BigFppfOver.topology B S hS)

AlgebraicGeometry.Stack.isStackInGroupoids_finiteHilbertProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/StackDescent.lean, line 959.

The relative finite Hilbert category ℋ_d(𝒳/𝒴) of a 1-morphism F : 𝒳 ⟶ 𝒴 of stacks in groupoids over the big fppf site of a scheme S, endowed with its forgetful functor to the site, is a stack in groupoids over (Sch/S)_fppf.

theorem isStackInGroupoids_finiteHilbertProjection :
    (finiteHilbertProjection (B := B) (S := S) (hS := hS)
      (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d)).IsStackInGroupoids.{w}
      (BigFppfOver.topology B S hS)

Tag 05WC, a definition

Tag 05WC in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Stack.finiteHilbertCategory, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/StackDefinition.lean, line 63 (StacksFrontier): “the stack ℋ_d(𝒳/𝒴)”.
AlgebraicGeometry.Stack.absoluteHilbertCategory, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/StackDefinition.lean, line 65 (StacksFrontier): “ℋ_d(𝒳), the case 𝒴 = S”.
AlgebraicGeometry.Stack.finiteCoverCategory, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/StackDefinition.lean, line 67 (StacksFrontier): “ℋ_d, the case 𝒳 = 𝒴 = S”.

Tag 05WD, an equation

Tag 05WD in the Stacks Project.

AlgebraicGeometry.Stack.forgetRelativeStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Diagram.lean, line 322. The attribute's comment: “relative Hilbert stack to absolute Hilbert stack”.

Stacks 05WD. The 1-morphism ℋ_d(𝒳/𝒴) ⟶ ℋ_d(𝒳) from the relative to the absolute finite Hilbert category: forget the object of 𝒴 and the identification, keeping the cover and the object of 𝒳.

def forgetRelativeStructure :
    finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d) ⥤ᵇ
      absoluteHilbertCategory (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳)

AlgebraicGeometry.Stack.forgetTarget, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Diagram.lean, line 338. The attribute's comment: “relative Hilbert stack to the target stack”.

Stacks 05WD. The 1-morphism ℋ_d(𝒳/𝒴) ⟶ 𝒴 to the target stack: forget the cover and the object of 𝒳, keeping the object of 𝒴.

def forgetTarget :
    finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d) ⥤ᵇ
      𝒴.toBasedCategory

AlgebraicGeometry.Stack.forgetAbsoluteStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Diagram.lean, line 356. The attribute's comment: “absolute Hilbert stack to finite covers”.

Stacks 05WD. The 1-morphism ℋ_d(𝒳) ⟶ ℋ_d from the absolute finite Hilbert category to the category of finite locally free covers: forget the object of 𝒳.

def forgetAbsoluteStructure :
    absoluteHilbertCategory (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳) ⥤ᵇ
      finiteCoverCategory (B := B) (S := S) (hS := hS) (d := d)

AlgebraicGeometry.Stack.forgetRelativeToFiniteCover, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Diagram.lean, line 370. The attribute's comment: “relative Hilbert stack to finite covers”.

Stacks 05WD. The 1-morphism ℋ_d(𝒳/𝒴) ⟶ ℋ_d from the relative finite Hilbert category to the category of finite locally free covers: forget both stack objects and the identification, keeping the cover.

def forgetRelativeToFiniteCover :
    finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d) ⥤ᵇ
      finiteCoverCategory (B := B) (S := S) (hS := hS) (d := d)

AlgebraicGeometry.Stack.forgetToProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/ProductMorphism.lean, line 188. The attribute's comment: “the 1-morphism of the equation, as the pairing of the two legs”.

Stacks 05WD. The 1-morphism ℋ_d(𝒳/𝒴) ⟶ ℋ_d(𝒳) × 𝒴 of the equation: the pairing of the two legs AlgebraicGeometry.Stack.forgetRelativeStructure and AlgebraicGeometry.Stack.forgetTarget.

noncomputable def forgetToProduct :
    finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d) ⥤ᵇ
      absoluteHilbertTargetProduct
        (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳) (𝒴 := 𝒴)

Tag 05XV, a lemma

Tag 05XV in the Stacks Project.

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

For a positive degree d, the 1-morphism ℋ_d(𝒳/𝒴) ⟶ ℋ_d(𝒳) from the relative to the absolute finite Hilbert category is faithful.

theorem forgetRelativeStructure_faithful (hd : 0 < d) :
    (forgetRelativeStructure (B := B) (S := S) (hS := hS)
      (d := d) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)).toFunctor.Faithful

Sources

LeanAlgebraicGeometry.Stack.isStackInGroupoids_finiteCoverProjection · AlgebraicGeometry.Stack.isStackInGroupoids_finiteHilbertProjection · AlgebraicGeometry.Stack.finiteHilbertCategory · AlgebraicGeometry.Stack.absoluteHilbertCategory · AlgebraicGeometry.Stack.finiteCoverCategory · AlgebraicGeometry.Stack.forgetRelativeStructure · AlgebraicGeometry.Stack.forgetTarget · AlgebraicGeometry.Stack.forgetAbsoluteStructure

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

95 Examples of Stacks

Section95.4 Quasi-coherent sheaves#

Tag 04U2, an equation

Tag 04U3, a lemma

Tag 03YM, a lemma

Sources

Section95.5 The stack of finitely generated quasi-coherent sheaves#

Tag 04U4, a lemma

Tag 04U5, a lemma

Tag 04U6, a lemma

Sources

Section95.6 Finite étale covers#

Tag 0BLY, the section

Tag 0BLZ, a lemma

Sources

Section95.7 Algebraic spaces#

Tag 04U8, an equation

Tag 04U9, a lemma

Tag 04UA, a lemma

Sources

Section95.8 The stack of finite type algebraic spaces#

Tag 04UD, a lemma

Tag 04UE, a lemma

Sources

Section95.14 Classifying torsors#

Tag 04UJ, a subsection

Tag 04UK, a lemma

Tag 04UL, a subsection

Tag 04UM, a lemma

Tag 04UN, a subsection

Tag 04UP, a remark

Tag 04UR, a subsection

Tag 04US, a lemma

Tag 04UT, a lemma

Sources

Section95.15 Quotients by group actions#

Tag 04WL, a situation

Tag 0370, a lemma

Tag 04WM, a proposition

Tag 0CQJ, a lemma

Tag 0371, a remark

Sources

Section95.16 The Picard stack#

Tag 0372, the section

Tag 04WN, a lemma

Sources

Section95.17 Examples of inertia stacks#

Tag 0374, an example

Tag 0375, an example

Sources

Section95.18 Finite Hilbert stacks#

Tag 05WB, a lemma

Tag 05WC, a definition

Tag 05WD, an equation

Tag 05XV, a lemma

Sources

Section95.4 Quasi-coherent sheaves #

Section95.5 The stack of finitely generated quasi-coherent sheaves #

Section95.6 Finite étale covers #

Section95.7 Algebraic spaces #

Section95.8 The stack of finite type algebraic spaces #

Section95.14 Classifying torsors #

Section95.15 Quotients by group actions #

Section95.16 The Picard stack #

Section95.17 Examples of inertia stacks #

Section95.18 Finite Hilbert stacks #