78.4 Equivalence relations to 78.23 The 2-coequalizer…
Section78.4 Equivalence relations#
Section 78.4 of the Stacks Project, Tag 043B. 4 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 043C, a definition
Tag 043C in the Stacks Project.
AlgebraicGeometry.AlgebraicSpaces.hasPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Category.lean, line 432. The attribute's comment: “fibre products of algebraic spaces”.
The category of algebraic spaces over a scheme has fibre products: they are the presheaf fibre products, which are again algebraic spaces.
instance hasPullbacks : HasPullbacks (AlgebraicSpaces B S hS)
AlgebraicGeometry.Space.hasBinaryProducts_over_algebraicSpace, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits.lean, line 99. The attribute's comment: “products over a base algebraic space”.
The category of algebraic spaces over
Sequipped with a morphism to a fixed algebraic spaceZhas binary products, namely the fibre products overZ.
noncomputable instance hasBinaryProducts_over_algebraicSpace
(Z : AlgebraicSpaces B S hS) : HasBinaryProducts (Over Z)
AlgebraicGeometry.Space.PreRelation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationsOverSpace.lean, line 130. The attribute's comment: “part (1): pre-relation”.
Stacks 043C, part (1). A pre-relation from
RtoUis a morphism fromRto the productU ⨯ U.This is stated for an arbitrary category with binary products because the two bases it is taken over are different categories. Over a base algebraic space
Zit is instantiated at the sliceCategoryTheory.Over Zof presheaves on the big fppf site, whose categorical product is the fibre productU ×_Z U, which is the notion of the source; over an algebraic spaceBit is instantiated at the sliceCategoryTheory.Over Bof the categoryAlgebraicGeometry.AlgebraicSpaces, which is the shape the invariance notions of Stacks 048E inStacksFrontier/AlgebraicGeometry/Spaces/InvariantMorphisms.leanare stated at.
abbrev PreRelation (R U : C)
AlgebraicGeometry.Space.PreRelation.target, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationsOverSpace.lean, line 139. The attribute's comment: “part (1): target”.
Stacks 043C, part (1). The target map of a pre-relation, its composite with the first projection of the product.
noncomputable abbrev target : R ⟶ U
AlgebraicGeometry.Space.PreRelation.source, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationsOverSpace.lean, line 144. The attribute's comment: “part (1): source”.
Stacks 043C, part (1). The source map of a pre-relation, its composite with the second projection of the product.
noncomputable abbrev source : R ⟶ U
AlgebraicGeometry.Space.IsPreEquivalenceRelation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationsOverSpace.lean, line 188. The attribute's comment: “part (3): pre-equivalence relation”.
Stacks 043C, part (3). A pre-relation is a pre-equivalence relation when the relation it induces on the
U-valued points is an equivalence relation for every test scheme over the base.
abbrev IsPreEquivalenceRelation {R U : Over Z} (j : PreRelation R U) : Prop
AlgebraicGeometry.Space.isEquivalenceRelation_iff_mono_and_isPreEquivalenceRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelationsOverSpace.lean, line 279. The attribute's comment: “parts (2)-(4): pointwise characterization”.
Stacks 043C, parts (2)-(4). A pre-relation of algebraic spaces over
Zis an internal categorical equivalence relation exactly when it is a monomorphism and the relation it induces on the points of every test scheme overZis an equivalence relation.
theorem isEquivalenceRelation_iff_mono_and_isPreEquivalenceRelation
{R U : Over Z} (j : PreRelation R U) :
CategoryTheory.IsEquivalenceRelation j.target j.source ↔
(CategoryTheory.Mono j ∧ IsPreEquivalenceRelation j)
Declarations registered for the tag:
CategoryTheory.Monoregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/RelationsOverSpace.lean, line 191 (StacksFrontier): “part (2): relation”. References: EGA IV (8.11.5.1); SGA 1 V (3.6); SGA 3 VIIB (2.4.1); SGA 3 VIII (3.4); SGA 4 I (10.4); SGA 4 II (3.2).CategoryTheory.IsEquivalenceRelationregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/RelationsOverSpace.lean, line 192 (StacksFrontier): “part (4): equivalence relation”. References: SGA 3 IV (3.1.1); SGA 4 I (10.9); SGA 4 IV (9.8.2).
Tag 043D, a lemma
Tag 043D in the Stacks Project.
AlgebraicGeometry.Space.PreRelation.restrict, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Restriction.lean, line 89. The attribute's comment: “the restricted pre-relation”.
Stacks 043D. The restriction of a pre-relation along a morphism
g : U' ⟶ UoverZ, that is the first projection of the pullback definingrestriction.
noncomputable abbrev restrict (g : U' ⟶ U) : PreRelation (restriction j g) U'
AlgebraicGeometry.Space.PreRelation.isPreEquivalenceRelation_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Restriction.lean, line 110. The attribute's comment: “preservation of pre-equivalence relations”.
Stacks 043D. Restriction preserves pre-equivalence relations.
theorem isPreEquivalenceRelation_restrict (g : U' ⟶ U) (hj : IsPreEquivalenceRelation j) :
IsPreEquivalenceRelation (restrict j g)
AlgebraicGeometry.Space.PreRelation.isEquivalenceRelation_restrict, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Restriction.lean, line 157. The attribute's comment: “preservation of equivalence relations”.
Stacks 043D. Restriction preserves equivalence relations.
instance isEquivalenceRelation_restrict (g : U' ⟶ U)
[hj : IsEquivalenceRelation j.target j.source] :
IsEquivalenceRelation (restrict j g).target (restrict j g).source
Declarations registered for the tag:
CategoryTheory.Limits.pullback.fst_of_monoregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Restriction.lean, line 92 (StacksFrontier): “preservation of relations”. References: EGA I (3.3.12), “more general”.
Tag 043E, a definition
Tag 043E in the Stacks Project.
AlgebraicGeometry.Space.PreRelation.restrict, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Restriction.lean, line 89. The attribute's comment: “the restriction R|_{U'} of a pre-relation along g : U' ⟶ U”.
Stacks 043D. The restriction of a pre-relation along a morphism
g : U' ⟶ UoverZ, that is the first projection of the pullback definingrestriction.
noncomputable abbrev restrict (g : U' ⟶ U) : PreRelation (restriction j g) U'
Tag 043F, a lemma
Tag 043F in the Stacks Project.
AlgebraicGeometry.Space.PreRelation.isPreEquivalenceRelation_sourceTargetRel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RelationOnPoints.lean, line 236.
A pre-equivalence relation
j : R ⟶ U ×_Z Uinduces an equivalence relation on|U|:xis related toywhen some pointrof|R|hast(r) = xands(r) = y.
theorem isPreEquivalenceRelation_sourceTargetRel (hj : IsPreEquivalenceRelation j) :
Equivalence
(Function.SourceTargetRel
(pointsMap B S hS R.left j.source.left)
(pointsMap B S hS R.left j.target.left))
Sources
Section78.5 Group algebraic spaces#
Section 78.5 of the Stacks Project, Tag 043G. 2 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 043H, a definition
Tag 043H in the Stacks Project.
AlgebraicGeometry.Space.GroupAlgebraicSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupActions.lean, line 101.
Stacks Project, Tag 043H. Group algebraic spaces over an algebraic space
B. An object is a group object in presheaves overBwhose underlying presheaf is an algebraic space; morphisms are group-object morphisms overB.
noncomputable abbrev GroupAlgebraicSpace (𝒞 : BigFppfSite.{u}) (S : Scheme.{u})
(hS : 𝒞.Contains S) (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(_hB : IsAlgebraicSpace 𝒞 S hS B)
Tag 043I, a lemma
Tag 043I in the Stacks Project.
AlgebraicGeometry.Space.groupOverStarGrpObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ActionInSite.lean, line 98. The attribute's comment: “the group object over B attached to a presheaf of groups on the site”.
Stacks Project, Tag 043I.
B ×_S Gis a group object of presheaves overB, with the pointwise group law of the given presheaf of groups.
noncomputable instance groupOverStarGrpObj (F : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ GrpCat.{u}) :
GrpObj (groupOverStar 𝒞 S hS B F)
AlgebraicGeometry.Space.GroupAlgebraicSpace.baseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseChange.lean, line 215.
Stacks Project, Tag 043I. The pullback of a group algebraic space over
Balong a morphismB' ⟶ Bof algebraic spaces is a group algebraic space overB'.
noncomputable def GroupAlgebraicSpace.baseChange
{B B' : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u} {hB : IsAlgebraicSpace 𝒞 S hS B}
(hB' : IsAlgebraicSpace 𝒞 S hS B') (f : B' ⟶ B)
(G : GroupAlgebraicSpace 𝒞 S hS B hB) :
GroupAlgebraicSpace 𝒞 S hS B' hB'
AlgebraicGeometry.Space.GroupAlgebraicSpace.baseChange_obj_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseChange.lean, line 226. The attribute's comment: “the underlying pullback”.
Stacks Project, Tag 043I. The algebraic space underlying the pullback of a group algebraic space is the fibre product of the original one with the new base.
theorem GroupAlgebraicSpace.baseChange_obj_X
{B B' : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u} {hB : IsAlgebraicSpace 𝒞 S hS B}
(hB' : IsAlgebraicSpace 𝒞 S hS B') (f : B' ⟶ B)
(G : GroupAlgebraicSpace 𝒞 S hS B hB) :
(GroupAlgebraicSpace.baseChange 𝒞 S hS hB' f G).obj.X =
(Over.mk (pullback.snd G.obj.X.hom f) : Over B')
AlgebraicGeometry.Space.GroupAlgebraicSpace.ofGroupSchemeInSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseChange.lean, line 355. The attribute's comment: “the group algebraic space attached to a group scheme over the base”.
Stacks Project, Tag 043I. The group algebraic space
G_B = B ×_S Gover an algebraic spaceBoverSattached to a group schemeGoverSbelonging to the big fppf site: it is the base change ofG, regarded as a group algebraic space over the terminal algebraic space, along the structure morphism ofB. Its points over a schemeToverBare the morphismsT ⟶ Gof schemes overS.
noncomputable def GroupAlgebraicSpace.ofGroupSchemeInSite
(B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u) (hB : IsAlgebraicSpace 𝒞 S hS B)
(G : BigFppfOver 𝒞 S hS) (hG : GrpObj ((toSchemeOver 𝒞 S hS).obj G)) :
GroupAlgebraicSpace 𝒞 S hS B hB
AlgebraicGeometry.Space.isSmooth_prod_fst_multiplicativeGroupULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/MultiplicativeSmooth.lean, line 98. The attribute's comment: “the structure morphism of the multiplicative group algebraic space is smooth”. References: SGA 3 VIII (2.1), “(e), special case”.
The structure morphism of the group algebraic space
Gₘ,B = B ×_{Spec ℤ} Gₘover an arbitrary algebraic spaceBoverSpec ℤis a smooth morphism of algebraic spaces.
theorem isSmooth_prod_fst_multiplicativeGroupULift
(B : (BigFppfOver 𝒞 (Spec (.of (ULift.{u} ℤ))) (contains_specULiftZ 𝒞))ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 (Spec (.of (ULift.{u} ℤ))) (contains_specULiftZ 𝒞) B) :
IsSmooth 𝒞 (Spec (.of (ULift.{u} ℤ))) (contains_specULiftZ 𝒞)
(prod.fst : B ⨯ (pointsOnSite 𝒞 (Spec (.of (ULift.{u} ℤ))) (contains_specULiftZ 𝒞)
(multiplicativeGroupULiftSiteObject 𝒞)
(multiplicativeGroupULiftSiteObjectGrpObj 𝒞) ⋙ forget GrpCat) ⟶ B)
Sources
Section78.6 Properties of group algebraic spaces#
Section 78.6 of the Stacks Project, Tag 06P5. 3 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 06P6, a lemma
Tag 06P6 in the Stacks Project.
AlgebraicGeometry.Space.isSeparated_iff_identity_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Separation.lean, line 153. The attribute's comment: “separatedness”. References: SGA 3 VIB (5.1).
Stacks 06P6. A group algebraic space is separated over its base exactly when its identity section is a closed immersion.
theorem isSeparated_iff_identity_isClosedImmersion (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
IsSeparated 𝒞 S hS G.obj.X.hom ↔
IsClosedImmersion 𝒞 S hS (η[G.obj.X]).left
AlgebraicGeometry.Space.isLocallySeparated_iff_identity_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Separation.lean, line 161. The attribute's comment: “local separatedness”.
Stacks 06P6. A group algebraic space is locally separated over its base exactly when its identity section is an immersion.
theorem isLocallySeparated_iff_identity_isImmersion (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
IsLocallySeparated 𝒞 S hS G.obj.X.hom ↔
IsImmersion 𝒞 S hS (η[G.obj.X]).left
AlgebraicGeometry.Space.isQuasiSeparated_iff_identity_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Separation.lean, line 169. The attribute's comment: “quasi-separatedness”.
Stacks 06P6. A group algebraic space is quasi-separated over its base exactly when its identity section is quasi-compact.
theorem isQuasiSeparated_iff_identity_isQuasiCompact (G : GroupAlgebraicSpace 𝒞 S hS B hB) :
IsQuasiSeparated 𝒞 S hS G.obj.X.hom ↔
IsQuasiCompact 𝒞 S hS (η[G.obj.X]).left
Tag 0DSI, a lemma
Tag 0DSI in the Stacks Project.
AlgebraicGeometry.Space.isLocallyQuasiFinite_iff_at_identity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/AtIdentity.lean, line 211. The attribute's comment: “the locally quasi-finite characterization”.
Stacks 0DSI. A group algebraic space locally of finite type over its base is locally quasi-finite exactly when it is quasi-finite at the identity point over every point of the base.
theorem isLocallyQuasiFinite_iff_at_identity (G : GroupAlgebraicSpace B S hS Bs hBs)
(hG : IsLocallyOfFiniteType B S hS G.obj.X.hom) :
IsLocallyQuasiFinite B S hS G.obj.X.hom ↔
∀ b : points B S hS Bs,
IsQuasiFiniteAt B S hS G.obj.X.hom
(pointsMap B S hS Bs (MonObj.one (X := G.obj.X)).left b)
AlgebraicGeometry.Space.isUnramified_iff_at_identity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/AtIdentity.lean, line 332. The attribute's comment: “the unramified characterization”.
Stacks 0DSI. A group algebraic space locally of finite type over its base is unramified exactly when it is unramified at the identity point over every point of the base.
theorem isUnramified_iff_at_identity (G : GroupAlgebraicSpace B S hS Bs hBs)
(hG : IsLocallyOfFiniteType B S hS G.obj.X.hom) :
IsUnramified B S hS G.obj.X.hom ↔
∀ b : points B S hS Bs,
IsUnramifiedAt B S hS G.obj.X.hom
(pointsMap B S hS Bs (MonObj.one (X := G.obj.X)).left b)
Tag 0DSJ, a lemma
Tag 0DSJ in the Stacks Project.
AlgebraicGeometry.Space.locallyQuasiFiniteBaseLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseLocus.lean, line 390. The attribute's comment: “the locally quasi-finite base locus”.
Stacks 0DSJ, the locally quasi-finite case. The locally quasi-finite base locus of a group algebraic space: the union of all open subspaces of the base over which it is locally quasi-finite.
def locallyQuasiFiniteBaseLocus (G : GroupAlgebraicSpace B S hS Bs hBs) : Subfunctor Bs
AlgebraicGeometry.Space.le_locallyQuasiFiniteBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseLocus.lean, line 398. The attribute's comment: “maximality of the locally quasi-finite base locus”.
Stacks 0DSJ, maximality in the locally quasi-finite case. Every open subspace of the base over which a group algebraic space is locally quasi-finite is contained in its locally quasi-finite base locus: it is a member of the family that locus is the supremum of.
theorem le_locallyQuasiFiniteBaseLocus (G : GroupAlgebraicSpace B S hS Bs hBs)
{U : Subfunctor Bs} (hU : IsOpenSubspace B S hS U)
(hGU : IsLocallyQuasiFinite B S hS (pullback.snd G.obj.X.hom U.ι)) :
U ≤ locallyQuasiFiniteBaseLocus B S hS G
AlgebraicGeometry.Space.isOpenSubspace_locallyQuasiFiniteBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseLocus.lean, line 434. The attribute's comment: “openness of the locally quasi-finite base locus”.
Stacks 0DSJ, openness in the locally quasi-finite case. The locally quasi-finite base locus of a group algebraic space locally of finite type over its base is an open subspace.
theorem isOpenSubspace_locallyQuasiFiniteBaseLocus (G : GroupAlgebraicSpace B S hS Bs hBs)
(hG : IsLocallyOfFiniteType B S hS G.obj.X.hom) :
IsOpenSubspace B S hS (locallyQuasiFiniteBaseLocus B S hS G)
AlgebraicGeometry.Space.isLocallyQuasiFinite_locallyQuasiFiniteBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseLocus.lean, line 443. The attribute's comment: “local quasi-finiteness over the locally quasi-finite base locus”.
Stacks 0DSJ, the locally quasi-finite case. A group algebraic space locally of finite type over its base is locally quasi-finite over its locally quasi-finite base locus.
theorem isLocallyQuasiFinite_locallyQuasiFiniteBaseLocus
(G : GroupAlgebraicSpace B S hS Bs hBs)
(hG : IsLocallyOfFiniteType B S hS G.obj.X.hom) :
IsLocallyQuasiFinite B S hS
(pullback.snd G.obj.X.hom (locallyQuasiFiniteBaseLocus B S hS G).ι)
AlgebraicGeometry.Space.locallyQuasiFiniteBaseLocus_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseLocus.lean, line 462. The attribute's comment: “base change of the locally quasi-finite base locus”.
Stacks 0DSJ, base change in the locally quasi-finite case. Forming the locally quasi-finite base locus of a group algebraic space locally of finite type commutes with arbitrary base change of algebraic spaces over
S.
theorem locallyQuasiFiniteBaseLocus_preimage (G : GroupAlgebraicSpace B S hS Bs hBs)
(hG : IsLocallyOfFiniteType B S hS G.obj.X.hom)
{Bt : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hBt : IsAlgebraicSpace B S hS Bt) (f : Bt ⟶ Bs) :
locallyQuasiFiniteBaseLocus B S hS (GroupAlgebraicSpace.baseChange B S hS hBt f G) =
(locallyQuasiFiniteBaseLocus B S hS G).preimage f
AlgebraicGeometry.Space.unramifiedBaseLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseLocus.lean, line 494. The attribute's comment: “the unramified base locus”.
Stacks 0DSJ, the unramified case. The unramified base locus of a group algebraic space: the union of all open subspaces of the base over which it is unramified.
def unramifiedBaseLocus (G : GroupAlgebraicSpace B S hS Bs hBs) : Subfunctor Bs
AlgebraicGeometry.Space.le_unramifiedBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseLocus.lean, line 502. The attribute's comment: “maximality of the unramified base locus”.
Stacks 0DSJ, maximality in the unramified case. Every open subspace of the base over which a group algebraic space is unramified is contained in its unramified base locus: it is a member of the family that locus is the supremum of.
theorem le_unramifiedBaseLocus (G : GroupAlgebraicSpace B S hS Bs hBs)
{U : Subfunctor Bs} (hU : IsOpenSubspace B S hS U)
(hGU : IsUnramified B S hS (pullback.snd G.obj.X.hom U.ι)) :
U ≤ unramifiedBaseLocus B S hS G
AlgebraicGeometry.Space.isOpenSubspace_unramifiedBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseLocus.lean, line 511. The attribute's comment: “openness of the unramified base locus”.
Stacks 0DSJ, openness in the unramified case. The unramified base locus of a group algebraic space is an open subspace.
theorem isOpenSubspace_unramifiedBaseLocus (G : GroupAlgebraicSpace B S hS Bs hBs) :
IsOpenSubspace B S hS (unramifiedBaseLocus B S hS G)
AlgebraicGeometry.Space.isUnramified_unramifiedBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseLocus.lean, line 520. The attribute's comment: “unramifiedness over the unramified base locus”.
Stacks 0DSJ, the unramified case. A group algebraic space is unramified over its unramified base locus.
theorem isUnramified_unramifiedBaseLocus (G : GroupAlgebraicSpace B S hS Bs hBs) :
IsUnramified B S hS (pullback.snd G.obj.X.hom (unramifiedBaseLocus B S hS G).ι)
AlgebraicGeometry.Space.unramifiedBaseLocus_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/BaseLocus.lean, line 618. The attribute's comment: “base change of the unramified base locus”.
Stacks 0DSJ, base change in the unramified case. Forming the unramified base locus of a group algebraic space locally of finite type commutes with arbitrary base change of algebraic spaces over
S.
theorem unramifiedBaseLocus_preimage (G : GroupAlgebraicSpace B S hS Bs hBs)
(hG : IsLocallyOfFiniteType B S hS G.obj.X.hom)
{Bt : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hBt : IsAlgebraicSpace B S hS Bt) (f : Bt ⟶ Bs) :
unramifiedBaseLocus B S hS (GroupAlgebraicSpace.baseChange B S hS hBt f G) =
(unramifiedBaseLocus B S hS G).preimage f
Sources
Section78.7 Examples of group algebraic spaces#
Section 78.7 of the Stacks Project, Tag 06P7. 6 tags here are carried by 33 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 043J, an example
Tag 043J in the Stacks Project.
AlgebraicGeometry.Space.multiplicativeGroupSiteObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Multiplicative.lean, line 74. The attribute's comment: “the multiplicative group scheme as an object of the site”.
Stacks Project, Tag 043J. The multiplicative group scheme over
S, read as an object of the big fppf site overS.
noncomputable def multiplicativeGroupSiteObject : BigFppfOver 𝒞 S hS
AlgebraicGeometry.Space.multiplicativeGroupSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Multiplicative.lean, line 93.
Stacks Project, Tag 043J. The multiplicative group algebraic space
Gₘ,B = B ×_S Gₘ,Sover an algebraic spaceBoverS.
noncomputable def multiplicativeGroupSpace (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B) : GroupAlgebraicSpace 𝒞 S hS B hB
AlgebraicGeometry.Space.multiplicativeGroupSpace_obj_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Multiplicative.lean, line 101. The attribute's comment: “the underlying base change”.
Stacks Project, Tag 043J. The algebraic space underlying the multiplicative group algebraic space is the fibre product
B ×_S Gₘ,S.
theorem multiplicativeGroupSpace_obj_X (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B) :
(multiplicativeGroupSpace 𝒞 S hS B hB).obj.X =
(Over.mk (prod.fst :
B ⨯ (multiplicativeGroupPointsOnSite 𝒞 S hS ⋙ forget GrpCat) ⟶ B) : Over B)
AlgebraicGeometry.Space.multiplicativeGroupSpacePoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Multiplicative.lean, line 111. The attribute's comment: “the functor of global units”.
Stacks Project, Tag 043J. The group of points of the multiplicative group algebraic space over a scheme
ToverBis the group of units in the global sections ofT.
noncomputable def multiplicativeGroupSpacePoints (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(T : BigFppfOver 𝒞 S hS) (b : yoneda.obj T ⟶ B) :
((Over.mk b : Over B) ⟶
Over.mk (prod.fst :
B ⨯ (multiplicativeGroupPointsOnSite 𝒞 S hS ⋙ forget GrpCat) ⟶ B)) ≃*
(globalUnits S).obj (Opposite.op ((toSchemeOver 𝒞 S hS).obj T))
AlgebraicGeometry.Space.multiplicativeGroupSpacePoints_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Multiplicative.lean, line 124. The attribute's comment: “the functor of global units”.
AlgebraicGeometry.Space.multiplicativeGroupSpacePointsreads a point through the second projection of the fibre product and the canonical identification of Stacks 022U.
theorem multiplicativeGroupSpacePoints_apply (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(T : BigFppfOver 𝒞 S hS) (b : yoneda.obj T ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst : B ⨯ (multiplicativeGroupPointsOnSite 𝒞 S hS ⋙ forget GrpCat) ⟶ B)) :
multiplicativeGroupSpacePoints 𝒞 S hS B T b x =
(baseChangePointsIsoGlobalUnits S).hom.app
(Opposite.op ((toSchemeOver 𝒞 S hS).obj T))
(yonedaEquiv (x.left ≫ (prod.snd :
B ⨯ (multiplicativeGroupPointsOnSite 𝒞 S hS ⋙ forget GrpCat) ⟶ _)))
AlgebraicGeometry.Space.multiplicativeGroupSpacePoints_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Multiplicative.lean, line 139. The attribute's comment: “the functor of global units”.
AlgebraicGeometry.Space.multiplicativeGroupSpacePointsis natural in the scheme overB, so what is asserted is representability of the functor of global units and not a family of unrelated group isomorphisms.
theorem multiplicativeGroupSpacePoints_naturality (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(T U : BigFppfOver 𝒞 S hS) (f : T ⟶ U) (b : yoneda.obj U ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst : B ⨯ (multiplicativeGroupPointsOnSite 𝒞 S hS ⋙ forget GrpCat) ⟶ B)) :
multiplicativeGroupSpacePoints 𝒞 S hS B T (yoneda.map f ≫ b)
((Over.homMk (yoneda.map f) :
(Over.mk (yoneda.map f ≫ b) : Over B) ⟶ Over.mk b) ≫ x) =
(globalUnits S ⋙ forget GrpCat).map ((toSchemeOver 𝒞 S hS).map f).op
(multiplicativeGroupSpacePoints 𝒞 S hS B U b x)
Tag 043K, an example
Tag 043K in the Stacks Project.
AlgebraicGeometry.Space.rootsOfUnitySiteObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/RootsOfUnity.lean, line 156. The attribute's comment: “the roots-of-unity group scheme as an object of the site”. References: SGA 1 XI (6.1).
Stacks Project, Tag 043K. The group scheme
μₙ,Sofn-th roots of unity overS, read as an object of the big fppf site overS.
noncomputable def rootsOfUnitySiteObject : BigFppfOver 𝒞 S hS
AlgebraicGeometry.Space.rootsOfUnitySpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/RootsOfUnity.lean, line 175.
Stacks Project, Tag 043K. The group algebraic space
μₙ,B = B ×_S μₙ,Sofn-th roots of unity over an algebraic spaceBoverS.
noncomputable def rootsOfUnitySpace [Fact (0 < n)] (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B) : GroupAlgebraicSpace 𝒞 S hS B hB
AlgebraicGeometry.Space.rootsOfUnitySpace_obj_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/RootsOfUnity.lean, line 183. The attribute's comment: “the underlying base change”.
Stacks Project, Tag 043K. The algebraic space underlying the group algebraic space of
n-th roots of unity is the fibre productB ×_S μₙ,S.
theorem rootsOfUnitySpace_obj_X [Fact (0 < n)] (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B) :
(rootsOfUnitySpace 𝒞 S hS n B hB).obj.X =
(Over.mk (prod.fst :
B ⨯ (rootsOfUnityPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ B) : Over B)
AlgebraicGeometry.Space.rootsOfUnitySpacePoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/RootsOfUnity.lean, line 194. The attribute's comment: “the functor of roots of unity”.
Stacks Project, Tag 043K. The group of points of the group algebraic space of
n-th roots of unity over a schemeToverBis the group ofn-th roots of unity in the global sections ofT.
noncomputable def rootsOfUnitySpacePoints [Fact (0 < n)]
(B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u) (T : BigFppfOver 𝒞 S hS) (b : yoneda.obj T ⟶ B) :
((Over.mk b : Over B) ⟶
Over.mk (prod.fst :
B ⨯ (rootsOfUnityPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ B)) ≃*
(rootsOfUnityGroupOverFunctor n S).obj
(Opposite.op ((toSchemeOver 𝒞 S hS).obj T))
AlgebraicGeometry.Space.rootsOfUnitySpacePoints_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/RootsOfUnity.lean, line 208. The attribute's comment: “the functor of roots of unity”.
AlgebraicGeometry.Space.rootsOfUnitySpacePointsreads a point through the second projection of the fibre product and the canonical identification of Stacks 040M.
theorem rootsOfUnitySpacePoints_apply [Fact (0 < n)]
(B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u) (T : BigFppfOver 𝒞 S hS) (b : yoneda.obj T ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst : B ⨯ (rootsOfUnityPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ B)) :
rootsOfUnitySpacePoints 𝒞 S hS n B T b x =
(rootsOfUnityBaseChangeGroupPointsIso n S).hom.app
(Opposite.op ((toSchemeOver 𝒞 S hS).obj T))
(yonedaEquiv (x.left ≫ (prod.snd :
B ⨯ (rootsOfUnityPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ _)))
AlgebraicGeometry.Space.rootsOfUnitySpacePoints_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/RootsOfUnity.lean, line 223. The attribute's comment: “the functor of roots of unity”.
AlgebraicGeometry.Space.rootsOfUnitySpacePointsis natural in the scheme overB, so what is asserted is representability of the functor of roots of unity and not a family of unrelated group isomorphisms.
theorem rootsOfUnitySpacePoints_naturality [Fact (0 < n)]
(B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u) (T U : BigFppfOver 𝒞 S hS) (f : T ⟶ U)
(b : yoneda.obj U ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst : B ⨯ (rootsOfUnityPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ B)) :
rootsOfUnitySpacePoints 𝒞 S hS n B T (yoneda.map f ≫ b)
((Over.homMk (yoneda.map f) :
(Over.mk (yoneda.map f ≫ b) : Over B) ⟶ Over.mk b) ≫ x) =
(rootsOfUnityGroupOverFunctor n S ⋙ forget GrpCat).map
((toSchemeOver 𝒞 S hS).map f).op
(rootsOfUnitySpacePoints 𝒞 S hS n B U b x)
Tag 043L, an example
Tag 043L in the Stacks Project.
AlgebraicGeometry.Space.additiveGroupSiteObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Additive.lean, line 64. The attribute's comment: “the additive group scheme as an object of the site”.
The additive group scheme over
S, read as an object of the big fppf site overS.
noncomputable def additiveGroupSiteObject : BigFppfOver 𝒞 S hS
AlgebraicGeometry.Space.additiveGroupSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Additive.lean, line 82.
The additive group algebraic space
Gₐ,B = B ×_S Gₐ,Sover an algebraic spaceBoverS.
noncomputable def additiveGroupSpace (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B) : GroupAlgebraicSpace 𝒞 S hS B hB
AlgebraicGeometry.Space.additiveGroupSpace_obj_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Additive.lean, line 90. The attribute's comment: “the underlying base change”.
The algebraic space underlying the additive group algebraic space is the fibre product
B ×_S Gₐ,S.
theorem additiveGroupSpace_obj_X (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B) :
(additiveGroupSpace 𝒞 S hS B hB).obj.X =
(Over.mk (prod.fst :
B ⨯ (additiveGroupPointsOnSite 𝒞 S hS ⋙ forget GrpCat) ⟶ B) : Over B)
AlgebraicGeometry.Space.additiveGroupSpacePoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Additive.lean, line 100. The attribute's comment: “the functor of global sections”.
The group of points of the additive group algebraic space over a scheme
ToverBis the additive group of global sections ofT.
noncomputable def additiveGroupSpacePoints (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(T : BigFppfOver 𝒞 S hS) (b : yoneda.obj T ⟶ B) :
((Over.mk b : Over B) ⟶
Over.mk (prod.fst :
B ⨯ (additiveGroupPointsOnSite 𝒞 S hS ⋙ forget GrpCat) ⟶ B)) ≃*
(globalSectionsAdditive S).obj (Opposite.op ((toSchemeOver 𝒞 S hS).obj T))
AlgebraicGeometry.Space.additiveGroupSpacePoints_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Additive.lean, line 113. The attribute's comment: “the functor of global sections”.
AlgebraicGeometry.Space.additiveGroupSpacePointsreads a point through the second projection of the fibre product and the canonical identification of Stacks 022V.
theorem additiveGroupSpacePoints_apply (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(T : BigFppfOver 𝒞 S hS) (b : yoneda.obj T ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst : B ⨯ (additiveGroupPointsOnSite 𝒞 S hS ⋙ forget GrpCat) ⟶ B)) :
additiveGroupSpacePoints 𝒞 S hS B T b x =
(additiveGroupBaseChangePointsIsoGlobalSections S).hom.app
(Opposite.op ((toSchemeOver 𝒞 S hS).obj T))
(yonedaEquiv (x.left ≫ (prod.snd :
B ⨯ (additiveGroupPointsOnSite 𝒞 S hS ⋙ forget GrpCat) ⟶ _)))
AlgebraicGeometry.Space.additiveGroupSpacePoints_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/Additive.lean, line 126. The attribute's comment: “the functor of global sections”.
AlgebraicGeometry.Space.additiveGroupSpacePointsis natural in the scheme overB.
theorem additiveGroupSpacePoints_naturality (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(T U : BigFppfOver 𝒞 S hS) (f : T ⟶ U) (b : yoneda.obj U ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst : B ⨯ (additiveGroupPointsOnSite 𝒞 S hS ⋙ forget GrpCat) ⟶ B)) :
additiveGroupSpacePoints 𝒞 S hS B T (yoneda.map f ≫ b)
((Over.homMk (yoneda.map f) :
(Over.mk (yoneda.map f ≫ b) : Over B) ⟶ Over.mk b) ≫ x) =
(globalSectionsAdditive S ⋙ forget GrpCat).map ((toSchemeOver 𝒞 S hS).map f).op
(additiveGroupSpacePoints 𝒞 S hS B U b x)
Tag 043M, an example
Tag 043M in the Stacks Project.
AlgebraicGeometry.Space.generalLinearSiteObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/GeneralLinear.lean, line 78. The attribute's comment: “the general linear group scheme as an object of the site”.
The general linear group scheme over
S, read as an object of the big fppf site overS.
noncomputable def generalLinearSiteObject : BigFppfOver 𝒞 S hS
AlgebraicGeometry.Space.generalLinearSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/GeneralLinear.lean, line 97.
The general linear group algebraic space
GLₙ,B = B ×_S GLₙ,Sover an algebraic spaceBoverS.
noncomputable def generalLinearSpace (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B) : GroupAlgebraicSpace 𝒞 S hS B hB
AlgebraicGeometry.Space.generalLinearSpace_obj_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/GeneralLinear.lean, line 105. The attribute's comment: “the underlying base change”.
The algebraic space underlying the general linear group algebraic space is the fibre product
B ×_S GLₙ,S.
theorem generalLinearSpace_obj_X (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B) :
(generalLinearSpace 𝒞 S hS n B hB).obj.X =
(Over.mk (prod.fst :
B ⨯ (generalLinearPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ B) : Over B)
AlgebraicGeometry.Space.generalLinearSpacePoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/GeneralLinear.lean, line 115. The attribute's comment: “the functor of invertible matrices”.
The group of points of the general linear group algebraic space over a scheme
ToverBis the group of invertiblen × nmatrices over the global sections ofT.
noncomputable def generalLinearSpacePoints (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(T : BigFppfOver 𝒞 S hS) (b : yoneda.obj T ⟶ B) :
((Over.mk b : Over B) ⟶
Over.mk (prod.fst :
B ⨯ (generalLinearPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ B)) ≃*
(generalLinearGroupOverFunctor n S).obj
(Opposite.op ((toSchemeOver 𝒞 S hS).obj T))
AlgebraicGeometry.Space.generalLinearSpacePoints_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/GeneralLinear.lean, line 129. The attribute's comment: “the functor of invertible matrices”.
AlgebraicGeometry.Space.generalLinearSpacePointssends a point to the image of its second projection toGLₙ,Sunder the canonical identification of Stacks 022W.
theorem generalLinearSpacePoints_apply (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(T : BigFppfOver 𝒞 S hS) (b : yoneda.obj T ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst : B ⨯ (generalLinearPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ B)) :
generalLinearSpacePoints 𝒞 S hS n B T b x =
(baseChangeGroupPointsIso n S).hom.app
(Opposite.op ((toSchemeOver 𝒞 S hS).obj T))
(yonedaEquiv (x.left ≫ (prod.snd :
B ⨯ (generalLinearPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ _)))
AlgebraicGeometry.Space.generalLinearSpacePoints_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/GeneralLinear.lean, line 142. The attribute's comment: “the functor of invertible matrices”.
AlgebraicGeometry.Space.generalLinearSpacePointsis natural in the scheme overB.
theorem generalLinearSpacePoints_naturality (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(T U : BigFppfOver 𝒞 S hS) (f : T ⟶ U) (b : yoneda.obj U ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst : B ⨯ (generalLinearPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ B)) :
generalLinearSpacePoints 𝒞 S hS n B T (yoneda.map f ≫ b)
((Over.homMk (yoneda.map f) :
(Over.mk (yoneda.map f ≫ b) : Over B) ⟶ Over.mk b) ≫ x) =
(generalLinearGroupOverFunctor n S ⋙ forget GrpCat).map
((toSchemeOver 𝒞 S hS).map f).op
(generalLinearSpacePoints 𝒞 S hS n B U b x)
Tag 043N, an example
Tag 043N in the Stacks Project.
AlgebraicGeometry.Space.determinantGroupSpaceMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Determinant.lean, line 200.
Stacks Project, Tag 043N. The determinant, as a morphism of group algebraic spaces
GLₙ,B ⟶ Gₘ,Bover an algebraic spaceBoverS. It is the base change toBof the determinant morphism of group schemes overS.
noncomputable def determinantGroupSpaceMorphism (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B) :
generalLinearSpace 𝒞 S hS n B hB ⟶ multiplicativeGroupSpace 𝒞 S hS B hB
AlgebraicGeometry.Space.determinantGroupSpaceMorphism_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Determinant.lean, line 214. The attribute's comment: “base change of the determinant morphism over the base scheme”.
Stacks Project, Tag 043N. The morphism over
Bunderlying the determinant morphism of group algebraic spaces is the product of the identity ofBwith the determinant morphism of group schemes overS; that is,detonGLₙ,Bis the base change ofdetonGLₙ,S.
theorem determinantGroupSpaceMorphism_hom (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B) :
(determinantGroupSpaceMorphism 𝒞 S hS n B hB).hom.hom.hom =
determinantSpaceHom 𝒞 S hS n B
AlgebraicGeometry.Space.determinantSpaceHom_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Determinant.lean, line 246. The attribute's comment: “the determinant on points”.
Stacks Project, Tag 043N. On every scheme
ToverBthe determinant morphism of group algebraic spaces sends a point ofGLₙ,B, that is an invertiblen × nmatrix over the global sections ofT, to its determinant, viewed as a global unit. Its underlying morphism overBisAlgebraicGeometry.Space.determinantSpaceHom, byAlgebraicGeometry.Space.determinantGroupSpaceMorphism_hom.
theorem determinantSpaceHom_apply (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(T : BigFppfOver 𝒞 S hS) (b : yoneda.obj T ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst : B ⨯ (generalLinearPointsOnSite 𝒞 S hS n ⋙ forget GrpCat) ⟶ B)) :
multiplicativeGroupSpacePoints 𝒞 S hS B T b (x ≫ determinantSpaceHom 𝒞 S hS n B) =
Matrix.GeneralLinearGroup.det (generalLinearSpacePoints 𝒞 S hS n B T b x)
Tag 043O, an example
Tag 043O in the Stacks Project.
AlgebraicGeometry.Space.constantGroupSiteObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ConstantGroup.lean, line 80. The attribute's comment: “the constant group scheme as an object of the site”.
Stacks Project, Tag 043O. The constant group scheme
G_Sof Stacks 03YW, read as an object of the big fppf site overS. That it belongs to the site is a size hypothesis on the site:Gis an arbitrary abstract group, so no single big site can containG_Sfor allG.
noncomputable def constantGroupSiteObject
(hG : 𝒞.Contains (constantGroupScheme G S).X.left) : BigFppfOver 𝒞 S hS
AlgebraicGeometry.Space.constantGroupSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ConstantGroup.lean, line 102.
Stacks Project, Tag 043O. The constant group algebraic space
G_B = B ×_S G_Sover an algebraic spaceBoverS, for an abstract groupG.
noncomputable def constantGroupSpace (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B)
(hG : 𝒞.Contains (constantGroupScheme G S).X.left) :
GroupAlgebraicSpace 𝒞 S hS B hB
AlgebraicGeometry.Space.constantGroupSpace_obj_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ConstantGroup.lean, line 112. The attribute's comment: “the underlying base change”.
Stacks Project, Tag 043O. The algebraic space underlying the constant group algebraic space is the fibre product
B ×_S G_S.
theorem constantGroupSpace_obj_X (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hB : IsAlgebraicSpace 𝒞 S hS B)
(hG : 𝒞.Contains (constantGroupScheme G S).X.left) :
(constantGroupSpace 𝒞 S hS G B hB hG).obj.X =
(Over.mk (prod.fst :
B ⨯ (constantGroupPointsOnSite 𝒞 S hS G hG ⋙ forget GrpCat) ⟶ B) : Over B)
AlgebraicGeometry.Space.constantGroupSpacePoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ConstantGroup.lean, line 123. The attribute's comment: “the functor of locally constant maps”. References: SGA 3 I (4.1), “Hom = loc const maps”.
Stacks Project, Tag 043O. The group of points of the constant group algebraic space over a scheme
ToverBis the group of locally constantG-valued maps onT.
noncomputable def constantGroupSpacePoints (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hG : 𝒞.Contains (constantGroupScheme G S).X.left) (T : BigFppfOver 𝒞 S hS)
(b : yoneda.obj T ⟶ B) :
((Over.mk b : Over B) ⟶
Over.mk (prod.fst :
B ⨯ (constantGroupPointsOnSite 𝒞 S hS G hG ⋙ forget GrpCat) ⟶ B)) ≃*
(locallyConstantMapsOver G S).obj (Opposite.op ((toSchemeOver 𝒞 S hS).obj T))
AlgebraicGeometry.Space.constantGroupSpacePoints_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ConstantGroup.lean, line 139. The attribute's comment: “the functor of locally constant maps”.
AlgebraicGeometry.Space.constantGroupSpacePointsreads a point through the second projection of the fibre product and the canonical identification of Stacks 03YW.
theorem constantGroupSpacePoints_apply (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hG : 𝒞.Contains (constantGroupScheme G S).X.left) (T : BigFppfOver 𝒞 S hS)
(b : yoneda.obj T ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst :
B ⨯ (constantGroupPointsOnSite 𝒞 S hS G hG ⋙ forget GrpCat) ⟶ B)) :
constantGroupSpacePoints 𝒞 S hS G B hG T b x =
(constantGroupSchemePointsIsoLocallyConstantMaps G S).hom.app
(Opposite.op ((toSchemeOver 𝒞 S hS).obj T))
(ULift.up (yonedaEquiv (x.left ≫ (prod.snd :
B ⨯ (constantGroupPointsOnSite 𝒞 S hS G hG ⋙ forget GrpCat) ⟶ _))))
AlgebraicGeometry.Space.constantGroupSpacePoints_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ConstantGroup.lean, line 156. The attribute's comment: “the functor of locally constant maps”.
AlgebraicGeometry.Space.constantGroupSpacePointsis natural in the scheme overB, so what is asserted is representability of the functor of locally constant maps and not a family of unrelated group isomorphisms.
theorem constantGroupSpacePoints_naturality (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(hG : 𝒞.Contains (constantGroupScheme G S).X.left) (T U : BigFppfOver 𝒞 S hS) (f : T ⟶ U)
(b : yoneda.obj U ⟶ B)
(x : (Over.mk b : Over B) ⟶
Over.mk (prod.fst :
B ⨯ (constantGroupPointsOnSite 𝒞 S hS G hG ⋙ forget GrpCat) ⟶ B)) :
constantGroupSpacePoints 𝒞 S hS G B hG T (yoneda.map f ≫ b)
((Over.homMk (yoneda.map f) :
(Over.mk (yoneda.map f ≫ b) : Over B) ⟶ Over.mk b) ≫ x) =
(locallyConstantMapsOver G S ⋙ forget GrpCat).map ((toSchemeOver 𝒞 S hS).map f).op
(constantGroupSpacePoints 𝒞 S hS G B hG U b x)
Sources
Section78.8 Actions of group algebraic spaces#
Section 78.8 of the Stacks Project, Tag 043P. 4 tags here are carried by 3 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 043Q, a definition
Tag 043Q in the Stacks Project.
AlgebraicGeometry.Space.objectOverStarModObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ActionInSite.lean, line 109. The attribute's comment: “part (1): the action over B attached to an action on points”.
Stacks Project, Tag 043Q, part (1). An action of a presheaf of groups on a presheaf over the big fppf site over
Sis an action ofB ×_S GonB ×_S Xin presheaves overB.
noncomputable instance objectOverStarModObj (F : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ GrpCat.{u})
(P : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u) [ModObj (F ⋙ forget GrpCat) P] :
ModObj (groupOverStar 𝒞 S hS B F) (objectOverStar 𝒞 S hS B P)
Declarations registered for the tag:
CategoryTheory.ModObjregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupActions.lean, line 107 (StacksFrontier): “part (1): action of a group algebraic space”.CategoryTheory.IsModHomregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupActions.lean, line 108 (StacksFrontier): “part (2): equivariant morphism”.
Tag 043R, an equation
Tag 043R in the Stacks Project.
Declarations registered for the tag:
CategoryTheory.ModObjregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupActions.lean, line 109 (StacksFrontier): “the unit and associativity diagrams of a group action”.
Tag 06P8, a definition
Tag 06P8 in the Stacks Project.
AlgebraicGeometry.Space.IsFreeAction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupActions.lean, line 114.
Stacks Project, Tag 06P8. A group object over
Bacts freely onXwhen its action is free on the points of every scheme overB.
abbrev IsFreeAction (𝒞 : BigFppfSite.{u}) (S : Scheme.{u}) (hS : 𝒞.Contains S)
(B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u) (G X : Over B) [GrpObj G] [ModObj G X] : Prop
Tag 06P9, a lemma
Tag 06P9 in the Stacks Project.
AlgebraicGeometry.Space.isFreeAction_iff_mono_leftSMul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/FreeAction.lean, line 80. References: SGA 3 IV (3.2.1), “(i), special case”.
Stacks 06P9. An action of a group algebraic space is free exactly when the action–projection morphism
G ×_B X ⟶ X ×_B X,(g, x) ↦ (g · x, x), is a monomorphism.
theorem isFreeAction_iff_mono_leftSMul (G X : Over B) [GrpObj G] [ModObj G X] :
IsFreeAction 𝒞 S hS B G X ↔ Mono (ModObj.leftSMul G X)
Sources
Section78.9 Principal homogeneous spaces#
Section 78.9 of the Stacks Project, Tag 04TV. 5 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04TW, a definition
Tag 04TW in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.IsPseudoTorsor, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 75 (StacksFrontier): “part (1): pseudo-torsor”.AlgebraicGeometry.IsTrivialPseudoTorsor, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 76 (StacksFrontier): “part (2): trivial pseudo-torsor”.
Tag 04TX, a lemma
Tag 04TX in the Stacks Project.
AlgebraicGeometry.Space.isPseudoTorsor_iff_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 136. The attribute's comment: “pointwise_characterization”. References: SGA 3 IV (6.7), “(i) <=> (ii)”; SGA 3 IV (5.1.0), “pointwise criterion”; SGA 3 III (0.1), “fppf site presheaves”.
A pseudo-torsor is characterized by simple transitivity on the points of every test scheme over its base presheaf.
theorem isPseudoTorsor_iff_points
(𝒞 : BigFppfSite.{u}) (S : Scheme.{u}) (hS : 𝒞.Contains S)
(B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(G X : Over B) [GrpObj G] [ModObj G X] :
IsPseudoTorsor G X ↔
∀ (T : BigFppfOver 𝒞 S hS) (b : yoneda.obj T ⟶ B)
(x y : (Over.mk b : Over B) ⟶ X),
∃! g : (Over.mk b : Over B) ⟶ G, g • x = y
AlgebraicGeometry.Space.isTrivialPseudoTorsor_iff_exists_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 180. The attribute's comment: “part (2): trivial iff the structure morphism has a section”.
A pseudo-torsor is trivial if and only if its structure morphism to the base presheaf has a section.
theorem isTrivialPseudoTorsor_iff_exists_section
(𝒞 : BigFppfSite.{u}) (S : Scheme.{u}) (hS : 𝒞.Contains S)
(B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
(G X : Over B) [GrpObj G] [ModObj G X] (hX : IsPseudoTorsor G X) :
IsTrivialPseudoTorsor G X ↔ ∃ s : B ⟶ X.left, s ≫ X.hom = 𝟙 B
Declarations registered for the tag:
AlgebraicGeometry.isTrivial_iff_exists_globalSection, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 78 (StacksFrontier): “trivial_iff_section”.
Tag 04TY, a definition
Tag 04TY in the Stacks Project.
AlgebraicGeometry.Space.IsPrincipalHomogeneousSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 224. The attribute's comment: “part (1): principal homogeneous space”. References: SGA 3 IV (5.1.5), “alg. spaces, fpqc”; SGA 3 IV (6.5), “fpqc row”; SGA 3 IV (5.1), “princ. homog. bundle”; SGA 3 VIB (10.15), “G-torsor, fpqc T”; SGA 1 XI (4.1).
A principal homogeneous space under a group algebraic space
GoverBis a pseudo-torsor which has sections after an fpqc covering ofB.
abbrev IsPrincipalHomogeneousSpace : Prop
AlgebraicGeometry.Space.IsFppfTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 231. The attribute's comment: “part (2): fppf torsor”. References: SGA 3 IV (5.1.5), “alg. spaces, fppf”; SGA 3 VIB (10.15), “G-torsor, fppf T”.
A pseudo-torsor which has sections after an fppf covering of the base.
abbrev IsFppfTorsor : Prop
AlgebraicGeometry.Space.IsSyntomicTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 236. The attribute's comment: “part (2): syntomic torsor”.
A pseudo-torsor which has sections after a syntomic covering of the base.
abbrev IsSyntomicTorsor : Prop
AlgebraicGeometry.Space.IsSmoothTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 241. The attribute's comment: “part (2): smooth torsor”.
A pseudo-torsor which has sections after a smooth covering of the base.
abbrev IsSmoothTorsor : Prop
AlgebraicGeometry.Space.IsEtaleTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 250. The attribute's comment: “parts (2), (3): étale torsor and quasi-isotriviality”. References: SGA 3 IV (5.1.5), “alg. spaces, étale”; SGA 3 IV (6.5), “étale row”; SGA 3 VIB (10.15), “G-torsor, étale T”.
A pseudo-torsor which has sections after an étale covering of the base; for a principal homogeneous space this is quasi-isotriviality.
abbrev IsEtaleTorsor : Prop
AlgebraicGeometry.Space.IsZariskiTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/PseudoTorsors.lean, line 258. The attribute's comment: “parts (2), (4): Zariski torsor and local triviality”. References: SGA 1 XI (4.7), “more general”; SGA 3 IV (6.5), “(Zar) row”.
A pseudo-torsor which has sections after a Zariski covering of the base; for a principal homogeneous space this is local triviality.
abbrev IsZariskiTorsor : Prop
Tag 04TZ, a lemma
Tag 04TZ in the Stacks Project.
AlgebraicGeometry.Space.isFppfTorsor_iff_siteTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/FppfTorsor.lean, line 398. The attribute's comment: “the whole statement: the biconditional over the base S itself, with the site-side condition read in the sense of Tag 03AH”.
Stacks 04TZ. An action of a group algebraic space over
Son an algebraic space overSis an fppf torsor exactly when it is a torsor on the big fppf site ofS.
theorem isFppfTorsor_iff_siteTorsor
(hB : IsAlgebraicSpace B S hS (⊤_ ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u)))
(G X : Over (⊤_ ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))) [GrpObj G] [ModObj G X]
(hG : IsAlgebraicSpace B S hS G.left) (hX : IsAlgebraicSpace B S hS X.left) :
IsFppfTorsor B S hS (⊤_ ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u)) hB G X hG hX ↔
IsSiteTorsor B S hS G X
Tag 0DSK, a lemma
Tag 0DSK in the Stacks Project.
AlgebraicGeometry.Space.isUnramified_of_isPseudoTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/PseudoTorsorProperties.lean, line 126. The attribute's comment: “the unramified case”.
Stacks 0DSK. A pseudo-torsor under an unramified group algebraic space is unramified over the base, provided it is locally of finite type over the base.
theorem isUnramified_of_isPseudoTorsor (𝒞 : BigFppfSite.{u}) (S : Scheme.{u})
(hS : 𝒞.Contains S) {B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u}
(hB : IsAlgebraicSpace 𝒞 S hS B) (G : GroupAlgebraicSpace 𝒞 S hS B hB) (X : Over B)
[ModObj G.obj.X X] (hX : IsAlgebraicSpace 𝒞 S hS X.left)
(hXFiniteType : IsLocallyOfFiniteType 𝒞 S hS X.hom)
(hG : IsUnramified 𝒞 S hS G.obj.X.hom) (hPseudo : IsPseudoTorsor G.obj.X X) :
IsUnramified 𝒞 S hS X.hom
AlgebraicGeometry.Space.isLocallyQuasiFinite_of_isPseudoTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/PseudoTorsorProperties.lean, line 255. The attribute's comment: “the locally quasi-finite case”.
Stacks 0DSK. A pseudo-torsor under a locally quasi-finite group algebraic space is locally quasi-finite over the base, provided it is locally of finite type over the base.
The shear map identifies the second projection of
X ×_B Xwith that ofG ×_B X, which is a base change ofG ⟶ B, so the projection is locally quasi-finite; that is the only use of the torsor structure, andAlgebraicGeometry.Space.isLocallyQuasiFinite_of_isLocallyQuasiFinite_pullbackSndis the rest of the argument.
theorem isLocallyQuasiFinite_of_isPseudoTorsor (𝒞 : BigFppfSite.{u}) (S : Scheme.{u})
(hS : 𝒞.Contains S) {B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u}
(hB : IsAlgebraicSpace 𝒞 S hS B) (G : GroupAlgebraicSpace 𝒞 S hS B hB) (X : Over B)
[ModObj G.obj.X X] (hX : IsAlgebraicSpace 𝒞 S hS X.left)
(hXFiniteType : IsLocallyOfFiniteType 𝒞 S hS X.hom)
(hG : IsLocallyQuasiFinite 𝒞 S hS G.obj.X.hom) (hPseudo : IsPseudoTorsor G.obj.X X) :
IsLocallyQuasiFinite 𝒞 S hS X.hom
Sources
Section78.10 Equivariant quasi-coherent sheaves#
Section 78.10 of the Stacks Project, Tag 043S. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 043T, a definition
Tag 043T in the Stacks Project.
AlgebraicGeometry.Space.EquivariantQuasicoherentModule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/EquivariantQuasicoherentModules.lean, line 133.
A
G-equivariant quasi-coherent𝒪_X-module for an actionAof a group algebraic spaceGoverBon an algebraic spaceXoverB: a quasi-coherent𝒪_X-moduleℱtogether with a morphismα : a^*ℱ ⟶ pr₁^*ℱof𝒪_{G ×_B X}-modules which satisfies the action cocycle condition and is normalized along the unit section.
structure EquivariantQuasicoherentModule (G : GroupAlgebraicSpace 𝒞 S hS B hB) (X : Over B)
(hX : IsAlgebraicSpace 𝒞 S hS X.left) (A : ModObj G.obj.X X)
Tag 043U, a lemma
Tag 043U in the Stacks Project.
AlgebraicGeometry.Space.equivariantQuasicoherentPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/EquivariantQuasicoherentPullback/Functor.lean, line 600. References: SGA 3 I (6.3.1), “special case”.
Stacks 043U. The inverse image along a
G-equivariant morphismf : X ⟶ Yof algebraic spaces overBis a functor from theG-equivariant quasi-coherent𝒪_Y-modules to theG-equivariant quasi-coherent𝒪_X-modules: it sends(ℱ, α)tof^*ℱwith the reindexing ofαalong1_G × f.
def equivariantQuasicoherentPullback :
EquivariantQuasicoherentModule (hB := hB) G Y hY AY ⥤
EquivariantQuasicoherentModule (hB := hB) G X hX AX
Sources
Section78.11 Groupoids in algebraic spaces#
Section 78.11 of the Stacks Project, Tag 043V. 6 tags here are carried by 16 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 043W, a definition
Tag 043W in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidInSpaces/Basic.lean, line 55. The attribute's comment: “part (1): groupoid in algebraic spaces”.
Stacks 043W, part (1). A groupoid in algebraic spaces over an algebraic space
BoverS: algebraic spaces of objects and of arrows, both overB, with source, target and composition overB, whose evaluation at every test scheme is a groupoid.
structure GroupoidInAlgebraicSpaces
(C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
(B : AlgebraicSpaces C S hS)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.points_isGroupoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidInSpaces/Basic.lean, line 108. The attribute's comment: “part (1): the T-points of the quintuple are a groupoid category”.
Stacks 043W, part (1), as a statement about the quintuple. The defining property of the quintuple
(U, R, s, t, c)of a groupoid in algebraic spaces overB: the source and the target are morphisms overB, and at every test schemeTthe quintuple ofT-points is a groupoid category. The latter is spelled out as: theT-points of the object spaceUare the objects of a groupoid, an arrowx ⟶ yof that groupoid is the same thing as aT-pointaof the arrow spaceRwiths(a) = xandt(a) = y, and the composite of two such arrows is theT-point ofRproduced by the composition morphismc.
theorem points_isGroupoid {C : BigFppfSite.{u}} {S : Scheme.{u}}
{hS : C.Contains S} {B : AlgebraicSpaces C S hS}
(G : GroupoidInAlgebraicSpaces C S hS B) (T : (BigFppfOver C S hS)ᵒᵖ) :
G.source ≫ G.objectsToBase = G.arrowsToBase ∧
G.target ≫ G.objectsToBase = G.arrowsToBase ∧
∀ (x y z : G.toGroupoidInFunctors.Evaluation T) (g : x ⟶ y) (f : y ⟶ z),
(G.toGroupoidInFunctors.evaluationArrowEquiv T x z (g ≫ f)).1 =
(composableToPullback G.source.hom G.target.hom ≫ G.comp.hom).app T
⟨((G.toGroupoidInFunctors.evaluationArrowEquiv T y z f).1,
(G.toGroupoidInFunctors.evaluationArrowEquiv T x y g).1),
(G.toGroupoidInFunctors.evaluationArrowEquiv T y z f).2.1.trans
(G.toGroupoidInFunctors.evaluationArrowEquiv T x y g).2.2.symm⟩
AlgebraicGeometry.GroupoidInAlgebraicSpaces.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidInSpaces/Basic.lean, line 127. The attribute's comment: “part (2): morphism of groupoids in algebraic spaces”.
Stacks 043W, part (2). A morphism of groupoids in algebraic spaces over the same base: a morphism of the underlying groupoids in presheaves whose maps on objects and on arrows are morphisms over the base.
structure Hom {C : BigFppfSite.{u}} {S : Scheme.{u}}
{hS : C.Contains S} {B : AlgebraicSpaces C S hS}
(G H : GroupoidInAlgebraicSpaces C S hS B)
Tag 043X, a lemma
Tag 043X in the Stacks Project.
AlgebraicGeometry.Space.groupoidPreRelation_isPreEquivalenceRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidInSpaces/Basic.lean, line 208.
Stacks 043X. The pre-relation cut out by the target and source morphisms of a groupoid in algebraic spaces is a pre-equivalence relation: on the points of every test scheme over the base it is reflexive, symmetric and transitive, because those points and the arrows between them form a groupoid.
theorem groupoidPreRelation_isPreEquivalenceRelation
(G : GroupoidInAlgebraicSpaces C S hS B) :
IsPreEquivalenceRelation (groupoidPreRelation G)
Tag 043Y, a lemma
Tag 043Y in the Stacks Project.
AlgebraicGeometry.Space.existsUnique_groupoid_of_isEquivalenceRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/EquivalenceRelationGroupoid.lean, line 548.
Stacks 043Y. An equivalence relation
j : R ⟶ U ×_B Uof algebraic spaces over an algebraic spaceBextends to a groupoid in algebraic spaces overB, and in exactly one way: the source and the target of the groupoid are the two components ofj, and its composition law is then forced, an arrow being determined by its source and its target.
theorem existsUnique_groupoid_of_isEquivalenceRelation
(j : PreRelation (Over.mk qR.hom) (Over.mk qU.hom))
[IsEquivalenceRelation j.target j.source] :
∃! G : GroupoidInAlgebraicSpaces C S hS B, ExtendsRelation j G
Tag 043Z, a lemma
Tag 043Z in the Stacks Project.
AlgebraicGeometry.Space.isPullback_comp_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidInSpacesOfComposable.lean, line 476. The attribute's comment: “lower_right”.
For a groupoid in algebraic spaces, composition and the second projection out of the space of composable pairs of arrows form a cartesian square with two copies of the source map: a composable pair is determined by its second arrow together with its composite, and every arrow and composite with matching sources arise from one, the first arrow of the pair being the composite preceded by the inverse of the second.
theorem isPullback_comp_source {B : AlgebraicSpaces C S hS}
(G : GroupoidInAlgebraicSpaces C S hS B) :
IsPullback G.comp
(ObjectProperty.homMk (pullback.snd G.source.hom G.target.hom) :
AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows)
G.source G.source
AlgebraicGeometry.Space.isPullback_fst_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidInSpacesOfComposable.lean, line 503. The attribute's comment: “top_square”.
For a groupoid in algebraic spaces, the first projection out of the space of composable pairs of arrows and composition form a cartesian square with two copies of the target map: a composable pair is determined by its first arrow together with its composite, and every arrow and composite with matching targets arise from one, the second arrow of the pair being the composite preceded by the inverse of the first.
theorem isPullback_fst_comp {B : AlgebraicSpaces C S hS}
(G : GroupoidInAlgebraicSpaces C S hS B) :
IsPullback
(ObjectProperty.homMk (pullback.fst G.source.hom G.target.hom) :
AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows)
G.comp G.target G.target
Declarations registered for the tag:
AlgebraicGeometry.AlgebraicSpaces.isPullback_fiberProduct, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidInSpacesOfComposable.lean, line 468 (StacksFrontier): “lower_left”.
Tag 0450, a lemma
Tag 0450 in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 108. The attribute's comment: “the comparison of the two upper rows”.
Stacks 0450. The canonical comparison
(α, β) ↦ (α, α⁻¹ ∘ β)of the space of pairs of arrows of a groupoid in algebraic spaces with a common target with the space of composable pairs of arrows.
noncomputable def commonTargetPairsIso (G : GroupoidInAlgebraicSpaces C S hS B) :
AlgebraicSpaces.fiberProduct C S hS G.target G.target ≅
AlgebraicSpaces.fiberProduct C S hS G.source G.target
AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsIso_hom_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 117. The attribute's comment: “commutativity for the first projection”.
Stacks 0450. The comparison of pairs with a common target with composable pairs preserves the first arrow.
theorem commonTargetPairsIso_hom_fst (G : GroupoidInAlgebraicSpaces C S hS B) :
(commonTargetPairsIso G).hom ≫
(ObjectProperty.homMk (pullback.fst G.source.hom G.target.hom) :
AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows) =
ObjectProperty.homMk (pullback.fst G.target.hom G.target.hom)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsIso_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 129. The attribute's comment: “commutativity for composition”.
Stacks 0450. Composing the comparison of pairs with a common target with composable pairs and the composition of the groupoid recovers the second arrow.
theorem commonTargetPairsIso_hom_comp (G : GroupoidInAlgebraicSpaces C S hS B) :
(commonTargetPairsIso G).hom ≫ G.comp =
ObjectProperty.homMk (pullback.snd G.target.hom G.target.hom)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsIso_inv_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 139. The attribute's comment: “the inverse comparison on the first projection”.
Stacks 0450. The inverse comparison, from composable pairs to pairs with a common target, preserves the first arrow.
theorem commonTargetPairsIso_inv_fst (G : GroupoidInAlgebraicSpaces C S hS B) :
(commonTargetPairsIso G).inv ≫
(ObjectProperty.homMk (pullback.fst G.target.hom G.target.hom) :
AlgebraicSpaces.fiberProduct C S hS G.target G.target ⟶ G.arrows) =
ObjectProperty.homMk (pullback.fst G.source.hom G.target.hom)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsIso_inv_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 151. The attribute's comment: “the inverse comparison on the second projection”.
Stacks 0450. The inverse comparison, from composable pairs to pairs with a common target, sends the second arrow to the composite.
theorem commonTargetPairsIso_inv_snd (G : GroupoidInAlgebraicSpaces C S hS B) :
(commonTargetPairsIso G).inv ≫
(ObjectProperty.homMk (pullback.snd G.target.hom G.target.hom) :
AlgebraicSpaces.fiberProduct C S hS G.target G.target ⟶ G.arrows) =
G.comp
AlgebraicGeometry.GroupoidInAlgebraicSpaces.comp_source_eq_snd_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 165. The attribute's comment: “commutativity of the lower square for composition, c ≫ s = pr₁ ≫ s”.
Stacks 0450, the commutativity of the lower square for composition:
c ≫ s = pr₁ ≫ s. The composite of a composable pair of arrows of a groupoid in algebraic spaces has the same source as the second arrow of the pair.
theorem comp_source_eq_snd_source (G : GroupoidInAlgebraicSpaces C S hS B) :
G.comp ≫ G.source =
(ObjectProperty.homMk (pullback.snd G.source.hom G.target.hom) :
AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows) ≫ G.source
AlgebraicGeometry.GroupoidInAlgebraicSpaces.fst_source_eq_snd_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 176. The attribute's comment: “commutativity of the lower square for the projections, pr₀ ≫ s = pr₁ ≫ t”.
Stacks 0450, the commutativity of the lower square for the projections:
pr₀ ≫ s = pr₁ ≫ t. The first arrow of a composable pair of arrows of a groupoid in algebraic spaces has as its source the target of the second arrow of the pair.
theorem fst_source_eq_snd_target (G : GroupoidInAlgebraicSpaces C S hS B) :
(ObjectProperty.homMk (pullback.fst G.source.hom G.target.hom) :
AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows) ≫ G.source =
(ObjectProperty.homMk (pullback.snd G.source.hom G.target.hom) :
AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows) ≫ G.target
AlgebraicGeometry.GroupoidInAlgebraicSpaces.isPullback_fst_snd_source_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 190. The attribute's comment: “the lower-left square for the projections is cartesian”.
Stacks 0450, the lower-left square for the projections. The two projections out of the space of composable pairs of arrows of a groupoid in algebraic spaces form a cartesian square with the source and the target morphisms: a composable pair is exactly a pair of arrows whose first arrow has as its source the target of the second.
theorem isPullback_fst_snd_source_target (G : GroupoidInAlgebraicSpaces C S hS B) :
IsPullback
(ObjectProperty.homMk (pullback.fst G.source.hom G.target.hom) :
AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows)
(ObjectProperty.homMk (pullback.snd G.source.hom G.target.hom) :
AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows)
G.source G.target
Declarations registered for the tag:
AlgebraicGeometry.AlgebraicSpaces.isPullback_fiberProduct, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 371 (StacksFrontier): “the lower-left square for the projections”.AlgebraicGeometry.Space.isPullback_comp_source, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 374 (StacksFrontier): “the lower-left square for composition”.
Tag 0DTA, a lemma
Tag 0DTA in the Stacks Project.
AlgebraicGeometry.Space.baseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidInSpaces/BaseChange.lean, line 71.
Pull back a groupoid in algebraic spaces along a morphism of bases.
noncomputable def baseChange {C : BigFppfSite.{u}} {S : Scheme.{u}}
{hS : C.Contains S} {B B' : AlgebraicSpaces C S hS}
(G : GroupoidInAlgebraicSpaces C S hS B) (f : B' ⟶ B) :
BaseChange G f
Sources
Section78.12 Quasi-coherent sheaves on groupoids#
Section 78.12 of the Stacks Project, Tag 0440. 6 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0441, a definition
Tag 0441 in the Stacks Project.
AlgebraicGeometry.Space.QuasicoherentModule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentModules.lean, line 392.
Stacks 0441. A quasi-coherent module on a groupoid in algebraic spaces
(U, R, s, t, c)overA: a quasi-coherent𝒪_U-moduleℱtogether with a morphismα : t^*ℱ ⟶ s^*ℱof𝒪_R-modules which satisfies the cocycle condition on the space of composable pairs of arrows and restricts to the identity along the unit.
structure QuasicoherentModule (G : GroupoidInAlgebraicSpaces B S hS A)
Tag 077W, a lemma
Tag 077W in the Stacks Project.
AlgebraicGeometry.Space.QuasicoherentModule.isIso_alpha, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentTransition.lean, line 347.
The transition morphism
α : t^*ℱ ⟶ s^*ℱof a quasi-coherent module on a groupoid in algebraic spaces is an isomorphism.
theorem isIso_alpha (M : QuasicoherentModule 𝒞 S hS G) : IsIso M.alpha
Tag 0442, a lemma
Tag 0442 in the Stacks Project.
AlgebraicGeometry.Space.groupoidQuasicoherentPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidQuasicoherentPullbackFunctor.lean, line 216. The attribute's comment: “the inverse image functor on quasi-coherent modules”.
Stacks 0442. The inverse image along a morphism
fof groupoids in algebraic spaces is a functorQCoh(U', R', s', t', c') ⥤ QCoh(U, R, s, t, c): it sends a quasi-coherent module(ℱ, α)on the target groupoid to the inverse image(f^*ℱ, f^*α)ofAlgebraicGeometry.Space.groupoidQuasicoherentPullbackObj, and a morphism to the inverse image of the underlying morphism of modules on the spaces of objects.
def groupoidQuasicoherentPullback :
QuasicoherentModule B S hS G' ⥤ QuasicoherentModule B S hS G
AlgebraicGeometry.Space.groupoidModulePullbackTransition_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentPullback.lean, line 514. The attribute's comment: “the unit law for the transition morphism of the inverse image”.
The unit law for the transition morphism of the inverse image. If the transition morphism
αof a module on the target groupoid restricts along the unit arrow to the canonical identification of the two inverse images, then so does the transition morphism of the inverse image along the unit arrow of the source groupoid.This is the unit law of Stacks 0441 for the pair
(f^*ℱ, f^*α).
theorem groupoidModulePullbackTransition_unit (φ : Hom G G')
(F : Modules.{u, u} B S hS G'.objects.1 G'.objects.2)
(α : (modulePullback B S hS G'.target).obj F ⟶ (modulePullback B S hS G'.source).obj F)
(hunit : groupoidPullbackTransition B S hS G' F α (identityArrow G') =
pullbackTransport F ((identityArrow_comp_target G').trans
(identityArrow_comp_source G').symm)) :
groupoidPullbackTransition B S hS G ((modulePullback B S hS φ.objectsMap).obj F)
(groupoidModulePullbackTransition B S hS φ F α) (identityArrow G) =
pullbackTransport ((modulePullback B S hS φ.objectsMap).obj F)
((identityArrow_comp_target G).trans (identityArrow_comp_source G).symm)
AlgebraicGeometry.Space.groupoidModulePullbackTransition_cocycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentPullback.lean, line 564. The attribute's comment: “the cocycle law for the transition morphism of the inverse image”.
The cocycle law for the transition morphism of the inverse image. If the transition morphism
αof a module on the target groupoid satisfies the cocycle law on the space of composable pairs of arrows of the target groupoid, then the transition morphism of the inverse image satisfies it on the space of composable pairs of arrows of the source groupoid.This is the cocycle law of Stacks 0441 for the pair
(f^*ℱ, f^*α). Flattened along the map on objects, both sides become the corresponding sides of the law forαat the three morphisms the map on composable pairs carries the composition and the two projections to.
theorem groupoidModulePullbackTransition_cocycle (φ : Hom G G')
(F : Modules.{u, u} B S hS G'.objects.1 G'.objects.2)
(α : (modulePullback B S hS G'.target).obj F ⟶ (modulePullback B S hS G'.source).obj F)
(hcocycle : groupoidPullbackTransition B S hS G' F α G'.comp =
groupoidTransitionComposite B S hS G' F α) :
groupoidPullbackTransition B S hS G ((modulePullback B S hS φ.objectsMap).obj F)
(groupoidModulePullbackTransition B S hS φ F α) G.comp =
groupoidTransitionComposite B S hS G ((modulePullback B S hS φ.objectsMap).obj F)
(groupoidModulePullbackTransition B S hS φ F α)
Tag 0GPM, a lemma
Tag 0GPM in the Stacks Project.
AlgebraicGeometry.Space.groupoidQuasicoherentPullbackPushforwardAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentPushforwardAdjunction.lean, line 391.
Stacks 0GPM. Let
f : (U, R, s, t, c) ⟶ (U', R', s', t', c')be a morphism of groupoids in algebraic spaces overAsuch thatf : U ⟶ U'is quasi-compact and quasi-separated, the square formed byf : R ⟶ R', the target morphismst, t'andf : U ⟶ U'is cartesian, ands'is flat. Then pushforward(ℱ, α) ↦ (f_*ℱ, f_*α)(AlgebraicGeometry.Space.groupoidQuasicoherentPushforward) is a functor from the quasi-coherent modules on(U, R, s, t, c)to those on(U', R', s', t', c'), and it is right adjoint to the inverse image functor of Stacks 0442 (AlgebraicGeometry.Space.groupoidQuasicoherentPullback).
def groupoidQuasicoherentPullbackPushforwardAdjunction :
groupoidQuasicoherentPullback B S hS φ ⊣
groupoidQuasicoherentPushforward B S hS φ hqc hqs hpb hsflat
Tag 077X, a lemma
Tag 077X in the Stacks Project.
AlgebraicGeometry.Space.quasicoherentModule_hasColimits_of_closure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentColimits.lean, line 408.
Stacks 077X. The category of quasi-coherent modules on a groupoid in algebraic spaces has colimits, indexed by the categories of the universe of the schemes.
A colimit is computed on the underlying
𝒪_U-modules, where it exists because the sheaves of modules on the small étale ringed site of an algebraic space are cocomplete, and it is quasi-coherent by the arbitrary-colimit clause of Stacks 03M1,AlgebraicGeometry.Space.isClosedUnderColimitsOfShape_quasicoherentSheaves_schemeUniverse.
theorem quasicoherentModule_hasColimits_of_closure (B : BigFppfSite.{u}) (S : Scheme.{u})
(hS : B.Contains S) {A : AlgebraicSpaces B S hS}
(G : GroupoidInAlgebraicSpaces B S hS A) :
HasColimitsOfSize.{u, u} (QuasicoherentModule B S hS G)
Tag 06VZ, a lemma
Tag 06VZ in the Stacks Project.
AlgebraicGeometry.Space.QuasicoherentModule.abelian_of_closure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentAbelian.lean, line 631.
Stacks 06VZ. If the source and the target of a groupoid in algebraic spaces
(U, R, s, t, c)overAare flat, the quasi-coherent modules on it form an abelian category.Kernels and cokernels are computed on the underlying
𝒪_U-modules, which are quasi-coherent by the kernel and cokernel clauses of Stacks 03M1(3). A transition morphism is carried along a cokernel because an inverse image of𝒪-modules is a left adjoint, and along a kernel because the inverse images alongs, alongc ≫ sand alonge ≫ sare left exact:sis flat,cis a base change ofsby Stacks 043Z, ande ≫ sis the identity. The flatness oftis not used, being equivalent to that ofsin a groupoid.
noncomputable def abelian_of_closure (hs : IsFlat B S hS G.source.hom)
(_ht : IsFlat B S hS G.target.hom) :
Abelian (QuasicoherentModule B S hS G)
Sources
Section78.13 Colimits of quasi-coherent modules#
Section 78.13 of the Stacks Project, Tag 0GPN. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GPP, a lemma
Tag 0GPP in the Stacks Project.
AlgebraicGeometry.Space.QuasicoherentModule.forgetAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentCofree.lean, line 507.
Stacks 0GPP. Let
(U, R, s, t, c)be a groupoid in algebraic spaces withs(and hencet = s ∘ i) flat, quasi-compact and quasi-separated. For a quasi-coherent𝒪_U-module𝒢the modules_*t^*𝒢carries a canonical isomorphismα : t^*s_*t^*𝒢 ⟶ s^*s_*t^*𝒢making(s_*t^*𝒢, α)a quasi-coherent module on(U, R, s, t, c); this defines the functorAlgebraicGeometry.Space.QuasicoherentModule.cofree, and it is right adjoint to the forgetful functor(ℱ, β) ↦ ℱ.
def forgetAdjunction : forgetQuasicoherent G ⊣ cofree G hsflat hsqc hsqs
Tag 0GPQ, a remark
Tag 0GPQ in the Stacks Project.
AlgebraicGeometry.Space.QuasicoherentModule.forgetAdjunction_unit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentCofreeUnit.lean, line 58.
Stacks 0GPQ. Let
(U, R, s, t, c)be a groupoid in algebraic spaces withsflat, quasi-compact and quasi-separated (then so ist = s ∘ i), and letforgetQuasicoherent G ⊣ cofree Gbe the adjunction of Stacks 0GPP between the forgetful functor(ℱ, β) ↦ ℱand𝒢 ↦ (s_*t^*𝒢, α). The unit of this adjunction at a quasi-coherent module(ℱ, β)on the groupoid is
ℱ ⟶ s_*s^*ℱ ⟶ s_*t^*ℱ,the unit of the adjunction
s^* ⊣ s_*atℱfollowed by the direct image alongsof the inverse ofβ : t^*ℱ ⟶ s^*ℱ.
theorem forgetAdjunction_unit_app (M : QuasicoherentModule B S hS G) :
((forgetAdjunction G hsflat hsqc hsqs).unit.app M).hom =
(modulePullbackAdjunction B S hS G.source).unit.app M.F.obj ≫
(modulePushforward B S hS G.source).map (inv M.alpha)
Tag 0GPR, a lemma
Tag 0GPR in the Stacks Project.
AlgebraicGeometry.Space.isCoherent_intersectionPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentIntersectionPushforwardCoherence.lean, line 149.
Stacks 0GPR. Let
f : Y ⟶ Xbe a morphism of algebraic spaces over a schemeS, letFbe a quasi-coherent𝒪_X-module, letGbe an𝒪_Y-module and letφ : G ⟶ f^*Fbe a map of𝒪_Y-modules. Assume thatφis injective, thatfis quasi-compact, quasi-separated, flat and surjective, thatXandYare locally Noetherian, and thatGis coherent. ThenF ∩ f_*G, the fibre product ofF ⟶ f_*f^*F ⟵ f_*G, is a coherent𝒪_X-module.The two direct images
f_*Gandf_*f^*Fare quasi-coherent by Stacks 03M9, soF ∩ f_*Gis quasi-coherent. Its inverse imagef^*(F ∩ f_*G)is a quasi-coherent submodule ofG, byAlgebraicGeometry.Space.mono_intersectionPushforwardAdj, hence coherent by Stacks 07UD, and coherence descends alongfbyAlgebraicGeometry.Space.isCoherent_of_isCoherent_modulePullback.
theorem isCoherent_intersectionPushforward (f : Y ⟶ X)
(F : Modules.{u, u} B S hS X.1 X.2) (G : Modules.{u, u} B S hS Y.1 Y.2)
(φ : G ⟶ (modulePullback B S hS f).obj F) (mono : Mono φ)
(quasiCompact : IsQuasiCompact B S hS f.hom)
(quasiSeparated : IsQuasiSeparated B S hS f.hom)
(flat : IsFlat B S hS f.hom) (surjective : IsSurjective B S hS f.hom)
(X_noetherian : HasEtaleLocalProperty B S hS X.1
(fun V : Scheme.{u} => IsLocallyNoetherian V))
(Y_noetherian : HasEtaleLocalProperty B S hS Y.1
(fun V : Scheme.{u} => IsLocallyNoetherian V))
(F_qcoh : F.IsQuasicoherentOnSite) (G_coherent : IsCoherent B S hS Y.1 Y.2 G) :
IsCoherent B S hS X.1 X.2 (intersectionPushforward B S hS f φ)
Tag 0GPS, a lemma
Tag 0GPS in the Stacks Project.
AlgebraicGeometry.Space.QuasicoherentModule.exists_filtered_diagram_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/CoherentColimit.lean, line 625.
Stacks 0GPS. Let
(U, R, s, t, c)be a groupoid in algebraic spaces overBsuch thatUandRare Noetherian andsandtare flat, quasi-compact and quasi-separated. Then every quasi-coherent module(ℱ, β)on(U, R, s, t, c)is a filtered colimit of coherent modules: it is the colimit of a diagram, indexed by a filtered category, of quasi-coherent modules on(U, R, s, t, c)whose underlying𝒪_U-modules are coherent.The diagram is indexed by the coherent submodules
ℋofℱ, and its term atℋis the fibre product of the unit(ℱ, β) ⟶ (s_*t^*ℱ, α)of Stacks 0GPP with(s_*t^*ℋ, α) ⟶ (s_*t^*ℱ, α). By the description of the unit in Stacks 0GPQ its underlying module isℱ ∩ s_*t^*ℋ, which is coherent by Stacks 0GPR.
theorem exists_filtered_diagram_isCoherent (terminal_mem : B.Contains (⊤_ Scheme.{u}))
(objects_noetherian : IsNoetherian B S hS terminal_mem G.objects.1)
(arrows_noetherian : IsNoetherian B S hS terminal_mem G.arrows.1)
(source_flat : IsFlat B S hS G.source.hom)
(source_quasiCompact : IsQuasiCompact B S hS G.source.hom)
(source_quasiSeparated : IsQuasiSeparated B S hS G.source.hom)
(target_flat : IsFlat B S hS G.target.hom)
(_target_quasiCompact : IsQuasiCompact B S hS G.target.hom)
(_target_quasiSeparated : IsQuasiSeparated B S hS G.target.hom)
(M : QuasicoherentModule B S hS G) :
∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
(D : I ⥤ QuasicoherentModule B S hS G) (φ : D ⟶ (Functor.const I).obj M),
(∀ i, IsCoherent B S hS G.objects.1 G.objects.2 (D.obj i).F.obj) ∧
Nonempty (IsColimit (Cocone.mk M φ))
Sources
Section78.14 Crystals in quasi-coherent sheaves#
Section 78.14 of the Stacks Project, Tag 077Y. 2 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 077Z, a lemma
Tag 077Z in the Stacks Project.
Stacks.AlgebraicGeometry.Crystals.isColimit_cardinalGeneratedSubcrystalCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/CrystalFamilyTransport.lean, line 286. The attribute's comment: “the colimit”.
Stacks 077Z, the colimit assertion. For the cardinal
cardinalBound D, which depends only on the system of schemes and not on the crystal, every crystal in quasi-coherent modules on a flat system of schemes is the colimit of itscardinalBound D-generated submodules.Together with
Stacks.AlgebraicGeometry.Crystals.isFiltered_cardinalGeneratedSubcrystal, which says that those submodules form a directed system, this is the whole of the tag: there is a cardinalκsuch that every object ofCQC(X)is the directed colimit of itsκ-generated submodules.
def isColimit_cardinalGeneratedSubcrystalCocone (D : SchemeSystem.{u}) [D.IsFlat]
(M : Crystal D) : IsColimit (cardinalGeneratedSubcrystalCocone M (cardinalBound D))
Stacks.AlgebraicGeometry.Crystals.isFiltered_cardinalGeneratedSubcrystal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/CrystalsInQuasicoherentModules.lean, line 514. The attribute's comment: “the directed system”.
Stacks 077Z, the directedness half. For the cardinal
cardinalBound D, which depends only on the system of schemes and not on the crystal, thecardinalBound D-generated submodules of every crystal on a flat system form a directed system.This is one of the two declarations carrying the tag; the other,
Stacks.AlgebraicGeometry.Crystals.isColimit_cardinalGeneratedSubcrystalCocone, says that the crystal is the colimit of that system. Together they are the whole statement: for thisκevery object ofCQC(X)is the directed colimit of itsκ-generated submodules.
instance isFiltered_cardinalGeneratedSubcrystal (D : SchemeSystem.{u}) [D.IsFlat]
(M : Crystal D) : IsFiltered (CardinalGeneratedSubcrystal M (cardinalBound D))
Tag 0780, a lemma
Tag 0780 in the Stacks Project.
AlgebraicGeometry.Space.QuasicoherentModule.exists_generating_family, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentGenerators.lean, line 90.
Stacks 0780. For a groupoid in algebraic spaces with flat source and target there is a family of quasi-coherent modules on the groupoid, independent of the module, such that every quasi-coherent module on the groupoid is the directed colimit of those of its submodules that are isomorphic to a member of the family.
theorem exists_generating_family (G : GroupoidInAlgebraicSpaces B S hS A)
(_hs : IsFlat B S hS G.source.hom) (_ht : IsFlat B S hS G.target.hom) :
∃ (T : Type (u + 1)) (F : T → QuasicoherentModule B S hS G),
∀ M : QuasicoherentModule B S hS G,
IsFiltered (IsomorphicGeneratorSubobject T F M) ∧
Nonempty (IsColimit (isomorphicGeneratorSubobjectCocone T F M))
Sources
Section78.15 Groupoids and group spaces#
Section 78.15 of the Stacks Project, Tag 0443. 2 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0444, a lemma
Tag 0444 in the Stacks Project.
AlgebraicGeometry.Space.actionGroupoid, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/ActionGroupoidModules.lean, line 84. The attribute's comment: “the action groupoid itself”.
The action groupoid
(X, G ×_B X, pr₁, a, m)of an actionAof a group algebraic spaceGoverBon an algebraic spaceXoverB, with the projection as its source and the action morphism as its target.
noncomputable abbrev actionGroupoid (G : GroupAlgebraicSpace 𝒞 S hS B hB) (X : Over B)
(hX : IsAlgebraicSpace 𝒞 S hS X.left) (A : ModObj G.obj.X X) :
GroupoidInAlgebraicSpaces 𝒞 S hS ⟨B, hB⟩
AlgebraicGeometry.Space.groupoidOfAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/ActionGroupoid.lean, line 1351.
A group action gives the action groupoid, with the stated object and arrow spaces and all five structure maps.
noncomputable def groupoidOfAction :
ActionGroupoidConstruction B G X hG hX
Tag 0445, a lemma
Tag 0445 in the Stacks Project.
AlgebraicGeometry.Space.actionGroupoidModulesComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/ActionGroupoidModules.lean, line 351.
The rule
(ℱ, α) ↦ (ℱ, α)is a fully faithful and essentially surjective functor from theG-equivariant quasi-coherent𝒪_X-modules of Stacks 043T to the quasi-coherent modules of Stacks 0441 on the action groupoid of Stacks 0444, leaving the underlying quasi-coherent module, the transition morphism and the morphisms unchanged.
noncomputable def actionGroupoidModulesComparison (G : GroupAlgebraicSpace 𝒞 S hS B hB)
(X : Over B) (hX : IsAlgebraicSpace 𝒞 S hS X.left) (A : ModObj G.obj.X X) :
ActionGroupoidModulesComparison (hB := hB) G X hX A (actionGroupoid G X hX A)
AlgebraicGeometry.Space.actionGroupoidModulesEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/ActionGroupoidModules.lean, line 362. The attribute's comment: “the equivalence of categories”.
The rule
(ℱ, α) ↦ (ℱ, α)is an equivalence between the category ofG-equivariant quasi-coherent𝒪_X-modules of Stacks 043T and the category of quasi-coherent modules of Stacks 0441 on the action groupoid of Stacks 0444.
noncomputable def actionGroupoidModulesEquivalence (G : GroupAlgebraicSpace 𝒞 S hS B hB)
(X : Over B) (hX : IsAlgebraicSpace 𝒞 S hS X.left) (A : ModObj G.obj.X X) :
EquivariantQuasicoherentModule (hB := hB) G X hX A ≌
QuasicoherentModule 𝒞 S hS (actionGroupoid G X hX A)
Sources
Section78.16 The stabilizer group algebraic space#
Section 78.16 of the Stacks Project, Tag 0446. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0447, a lemma
Tag 0447 in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces.stabilizerGroupStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/GroupStructure.lean, line 224.
Stacks 0447. The stabilizer of a groupoid in algebraic spaces is a group object in the slice over the object space, with groupoid composition as multiplication.
noncomputable def stabilizerGroupStructure (G : GroupoidInAlgebraicSpaces C S hS B) :
{ h : GrpObj (stabilizer G) // IsStabilizerGroupStructure G h }
Tag 0448, a definition
Tag 0448 in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces.stabilizerGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/GroupStructure.lean, line 367. The attribute's comment: “the stabilizer as a group algebraic space over the object space”.
The stabilizer group algebraic space over the object space of a groupoid in algebraic spaces.
noncomputable def stabilizerGroup (G : GroupoidInAlgebraicSpaces C S hS B) :
Space.GroupAlgebraicSpace C S hS G.objects.obj G.objects.property
Tag 0449, a lemma
Tag 0449 in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces.stabilizerAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/Action.lean, line 172.
The stabilizer of a groupoid in algebraic spaces acts on its arrow space over the object space, and the action is groupoid composition on generalized points.
noncomputable def stabilizerAction (G : GroupoidInAlgebraicSpaces C S hS B) :
{ h : ModObj (stabilizer G) (arrowsOverTarget G) // IsStabilizerAction G h }
Sources
Section78.17 Restricting groupoids#
Section 78.17 of the Stacks Project, Tag 044A. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 044B, a lemma
Tag 044B in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces.restrict_isRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidRestriction/Restrict.lean, line 588.
Stacks 044B. Let
G = (U, R, s, t, c)be a groupoid in algebraic spaces overBand letg : U' ⟶ Ube a morphism of algebraic spaces. Form the fibre product squaresP₁ = U' ×_{g, U, t} R(projectionspU,pR),P₂ = R ×_{s, U, g} U'(projectionsqR,qU), andR' = P₁ ×_{pR, R, qR} P₂(projectionsa,b), and putt' = a ≫ pU,s' = b ≫ qU. Then the restriction(restrict G g).groupoidis a groupoid in algebraic spaces overBwhose space of objects isU'(overBthroughg), whose space of arrows isR'(overBthroughR), whose source and target ares'andt', and whose composition lawc' : R' ×_{s', U', t'} R' ⟶ R'keeps the target of the first arrow and the source of the second and composes the two underlying arrows byc. The mapsg : U' ⟶ Uanda ≫ pR : R' ⟶ Rare the two components of the morphism(restrict G g).homof groupoids in algebraic spaces overB.Moreover, for every scheme
Tof the site, the functor of groupoids(U'(T), R'(T), s', t', c') ⟶ (U(T), R(T), s, t, c)is the restriction of(U(T), R(T), s, t, c)viaU'(T) ⟶ U(T): an element ofR'(T)is exactly a triple(x, r, y)withx, y ∈ U'(T),r ∈ R(T),t(r) = g(x)ands(r) = g(y), witht'ands'the outer projections and the composite of(x, r, y)and(y, r'', z)equal to(x, c(r, r''), z); the functor isgon objects and is fully faithful.The same holds for the
T-points overB, in the source's sense of a schemeToverB: for a schemeTof the site and a pointb ∈ B(T), the groupoid(U'(T), R'(T), s', t', c')ofT-points of the restriction lying overbmaps to the groupoid(U(T), R(T), s, t, c)ofT-points ofGlying overb, and this functor is the restriction alongU'(T) ⟶ U(T): an arrow overbis exactly a triple(x, r, y)overbas above, the composite of two arrows overblies overband is computed as above, and the functor, which isgon objects and the functor on allT-points on arrows, is fully faithful.
public theorem restrict_isRestriction
{C : BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S}
{B : AlgebraicSpaces C S hS}
(G : GroupoidInAlgebraicSpaces C S hS B)
{U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects) :
let H := (restrict G g).groupoid
let φ := (restrict G g).hom
∃ (P₁ : AlgebraicSpaces C S hS) (pU : P₁ ⟶ U') (pR : P₁ ⟶ G.arrows)
(P₂ : AlgebraicSpaces C S hS) (qR : P₂ ⟶ G.arrows) (qU : P₂ ⟶ U')
(a : H.arrows ⟶ P₁) (b : H.arrows ⟶ P₂),
IsPullback pU pR g G.target ∧ IsPullback qR qU G.source g ∧ IsPullback a b pR qR ∧
H.objects = U' ∧ H.target = a ≫ pU ∧ H.source = b ≫ qU ∧
H.objectsToBase = g ≫ G.objectsToBase ∧
H.arrowsToBase = (a ≫ pR) ≫ G.arrowsToBase ∧
H.comp ≫ H.target = fiberProductFst H.source H.target ≫ H.target ∧
H.comp ≫ H.source = fiberProductSnd H.source H.target ≫ H.source ∧
(∃ m : AlgebraicSpaces.fiberProduct C S hS H.source H.target ⟶
AlgebraicSpaces.fiberProduct C S hS G.source G.target,
m ≫ fiberProductFst G.source G.target = fiberProductFst H.source H.target ≫ a ≫ pR ∧
m ≫ fiberProductSnd G.source G.target = fiberProductSnd H.source H.target ≫ a ≫ pR ∧
H.comp ≫ a ≫ pR = m ≫ G.comp) ∧
φ.toGroupoidHom.mapObjects = g.hom ∧
φ.toGroupoidHom.mapArrows = (a ≫ pR).hom ∧
(∀ T : (BigFppfOver C S hS)ᵒᵖ,
(∀ (x y : U'.obj.obj T) (r : G.arrows.obj.obj T),
G.target.hom.app T r = g.hom.app T x → G.source.hom.app T r = g.hom.app T y →
∃! z : H.arrows.obj.obj T, H.target.hom.app T z = x ∧
(a ≫ pR).hom.app T z = r ∧ H.source.hom.app T z = y) ∧
(∀ (z w : H.arrows.obj.obj T) (h : H.source.hom.app T z = H.target.hom.app T w)
(h' : G.source.hom.app T ((a ≫ pR).hom.app T z) =
G.target.hom.app T ((a ≫ pR).hom.app T w)),
H.target.hom.app T (H.toGroupoidInFunctors.compose T z w h) =
H.target.hom.app T z ∧
(a ≫ pR).hom.app T (H.toGroupoidInFunctors.compose T z w h) =
G.toGroupoidInFunctors.compose T ((a ≫ pR).hom.app T z)
((a ≫ pR).hom.app T w) h' ∧
H.source.hom.app T (H.toGroupoidInFunctors.compose T z w h) =
H.source.hom.app T w) ∧
(∀ x : U'.obj.obj T, (φ.toGroupoidHom.evaluation T).obj x = g.hom.app T x) ∧
Nonempty (φ.toGroupoidHom.evaluation T).FullyFaithful) ∧
∀ (T : (BigFppfOver C S hS)ᵒᵖ) (b : B.obj.obj T),
(∀ (x y : U'.obj.obj T) (r : G.arrows.obj.obj T),
H.objectsToBase.hom.app T x = b → H.objectsToBase.hom.app T y = b →
G.arrowsToBase.hom.app T r = b →
G.target.hom.app T r = g.hom.app T x → G.source.hom.app T r = g.hom.app T y →
∃! z : H.arrows.obj.obj T, H.arrowsToBase.hom.app T z = b ∧
H.target.hom.app T z = x ∧ (a ≫ pR).hom.app T z = r ∧
H.source.hom.app T z = y) ∧
(∀ (z w : H.arrows.obj.obj T) (h : H.source.hom.app T z = H.target.hom.app T w)
(h' : G.source.hom.app T ((a ≫ pR).hom.app T z) =
G.target.hom.app T ((a ≫ pR).hom.app T w)),
H.arrowsToBase.hom.app T z = b → H.arrowsToBase.hom.app T w = b →
H.arrowsToBase.hom.app T (H.toGroupoidInFunctors.compose T z w h) = b ∧
H.target.hom.app T (H.toGroupoidInFunctors.compose T z w h) =
H.target.hom.app T z ∧
(a ≫ pR).hom.app T (H.toGroupoidInFunctors.compose T z w h) =
G.toGroupoidInFunctors.compose T ((a ≫ pR).hom.app T z)
((a ≫ pR).hom.app T w) h' ∧
H.source.hom.app T (H.toGroupoidInFunctors.compose T z w h) =
H.source.hom.app T w) ∧
∃ F : ObjectProperty.FullSubcategory
(fun x : H.toGroupoidInFunctors.Evaluation T => H.objectsToBase.hom.app T x = b) ⥤
ObjectProperty.FullSubcategory
(fun x : G.toGroupoidInFunctors.Evaluation T => G.objectsToBase.hom.app T x = b),
(∀ x, (F.obj x).obj = g.hom.app T x.obj) ∧
F ⋙ ObjectProperty.ι _ = ObjectProperty.ι _ ⋙ φ.toGroupoidHom.evaluation T ∧
Nonempty F.FullyFaithful
Tag 044C, a definition
Tag 044C in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces.restrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidRestriction/Restrict.lean, line 59. The attribute's comment: “the restriction of the groupoid to U'”.
Restriction along an arbitrary map to the object space, with its canonical composition law and functor to the original groupoid.
public noncomputable def restrict
{C : BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S}
{B : AlgebraicSpaces C S hS}
(G : GroupoidInAlgebraicSpaces C S hS B)
{U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects) :
Restriction G g
Tag 044D, a lemma
Tag 044D in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces.existsUnique_iso_restriction_groupoidPreRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionComparison.lean, line 368. The attribute's comment: “restricting a groupoid, then taking its pre-relation”.
Stacks 044D, restricting a groupoid and then taking its pre-relation. Let
Gbe a groupoid in algebraic spaces overBandg : U' ⟶ Ua morphism to its space of objects. The pre-relationj' = (t', s') : R' ⟶ U' ×_B U'of the restrictionG|_{U'}of Stacks 044C, whose arrow space isR' = U' ×_{g, U, t} R ×_{s, U, g} U', is the restriction alongg, in the sense of Stacks 043D, of the pre-relationj = (t, s) : R ⟶ U ×_B UofG(Stacks 043X):R' = (U' ×_B U') ×_{U ×_B U} R. Precisely, there is exactly one isomorphism from the arrow space ofG|_{U'}to the restricted pre-relation's arrow space taking the restricted pre-relation toj'and its projection toRto the map on arrows of the morphismG|_{U'} ⟶ G.
theorem existsUnique_iso_restriction_groupoidPreRelation (G : GroupoidInAlgebraicSpaces C S hS B)
{U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects) :
∃! e : (Over.mk (G.restrict g).groupoid.arrowsToBase.hom : Over B.obj) ≅
Space.PreRelation.restriction (Space.groupoidPreRelation G) (restrictionObjectsHom G g),
e.hom ≫ Space.PreRelation.restrict (Space.groupoidPreRelation G)
(restrictionObjectsHom G g) = Space.groupoidPreRelation (G.restrict g).groupoid ∧
e.hom ≫ pullback.snd (prod.map (restrictionObjectsHom G g) (restrictionObjectsHom G g))
(Space.groupoidPreRelation G) =
Over.homMk (G.restrict g).hom.toGroupoidHom.mapArrows (G.restrict g).hom.mapArrows_over
AlgebraicGeometry.Space.existsUnique_isomorphism_restrict_groupoidOfIsEquivalenceRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionComparison.lean, line 581. The attribute's comment: “restricting an equivalence relation, then taking its groupoid”.
Stacks 044D, restricting an equivalence relation and then taking its groupoid. Let
j : R ⟶ U ×_B Ube an equivalence relation of algebraic spaces overB, let(U, R, s, t, c)be the groupoid in algebraic spaces it extends to (Stacks 043Y), and letg : U' ⟶ Ube a morphism of algebraic spaces. The groupoid in algebraic spaces of the restricted equivalence relationj' : R' = (U' ×_B U') ×_{U ×_B U} R ⟶ U' ×_B U'(Stacks 043D) is the restriction(U, R, s, t, c)|_{U'}of Stacks 044C: there is exactly one isomorphism of groupoids in algebraic spaces between them which is the identity ofU'on objects, and it takes the projectionR' ⟶ Rto the map on arrows of the morphism(U, R, s, t, c)|_{U'} ⟶ (U, R, s, t, c)of Stacks 044B.
theorem existsUnique_isomorphism_restrict_groupoidOfIsEquivalenceRelation
(j : PreRelation (Over.mk qR.hom) (Over.mk qU.hom)) [IsEquivalenceRelation j.target j.source]
(g : U' ⟶ U) :
∃! e : Isomorphism (groupoidOfIsEquivalenceRelation (restrictSpace j g))
((groupoidOfIsEquivalenceRelation j).restrict g).groupoid,
e.hom.toGroupoidHom.mapObjects = 𝟙 U'.obj ∧
e.hom.toGroupoidHom.mapArrows ≫
((groupoidOfIsEquivalenceRelation j).restrict g).hom.toGroupoidHom.mapArrows =
(pullback.snd (prod.map (overHomOfComp qU g) (overHomOfComp qU g)) j).left
Sources
Section78.18 Invariant subspaces#
Section 78.18 of the Stacks Project, Tag 044E. 2 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 044F, a definition
Tag 044F in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces.IsInvariantOpen, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/InvariantSubspaces.lean, line 71. The attribute's comment: “part (1): invariant open subspaces”.
Stacks 044F, part (1). An open subspace of the object space of a groupoid in algebraic spaces is invariant when every arrow whose source lies in it has its target in it.
abbrev IsInvariantOpen (G : GroupoidInAlgebraicSpaces site S hS B)
(W : Subfunctor G.objects.obj) : Prop
AlgebraicGeometry.GroupoidInAlgebraicSpaces.IsInvariantLocallyClosed, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/InvariantSubspaces.lean, line 80. The attribute's comment: “part (2): invariant locally closed subspaces”.
Stacks 044F, part (2). A locally closed subspace of the object space of a groupoid in algebraic spaces is invariant when its inverse images under the source and the target map agree as subspaces of the space of arrows.
abbrev IsInvariantLocallyClosed (G : GroupoidInAlgebraicSpaces site S hS B)
(Z : Subfunctor G.objects.obj) : Prop
AlgebraicGeometry.GroupoidInAlgebraicSpaces.IsInvariantMonomorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/InvariantSubspaces.lean, line 89. The attribute's comment: “part (3): invariant monomorphisms”.
Stacks 044F, part (3). A monomorphism into the object space of a groupoid in algebraic spaces is invariant when its base change along the target map and its base change along the source map are isomorphic as algebraic spaces over the space of arrows.
noncomputable abbrev IsInvariantMonomorphism (G : GroupoidInAlgebraicSpaces site S hS B)
{T : AlgebraicSpaces site S hS} (i : T ⟶ G.objects) [Mono i] : Prop
Tag 044G, a lemma
Tag 044G in the Stacks Project.
AlgebraicGeometry.Space.sourceSaturation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/InvariantOpenSaturation.lean, line 139. The attribute's comment: “the saturation s(t⁻¹(W)) of a subspace of the object space”.
Stacks 044G. The saturation of a subspace
Wof the object space of a groupoid in algebraic spaces: the subspace whose point set iss(t⁻¹(W)), the union of the orbits meetingW.
noncomputable def sourceSaturation (G : GroupoidInAlgebraicSpaces B S hS A)
(W : Subfunctor G.objects.obj) : Subfunctor G.objects.obj
AlgebraicGeometry.Space.isInvariantOpen_sourceSaturation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/InvariantOpenSaturation.lean, line 289. The attribute's comment: “part (1): the saturation is an invariant open subspace”.
Stacks 044G, part (1). For an open source morphism the saturation of an open subspace of the object space is an invariant open subspace.
theorem isInvariantOpen_sourceSaturation (G : GroupoidInAlgebraicSpaces B S hS A)
(hs : IsOpenMorphism B S hS G.source.hom) (W : Subfunctor G.objects.obj)
(hW : IsOpenSubspace B S hS W) :
GroupoidInAlgebraicSpaces.IsInvariantOpen G (sourceSaturation B S hS G W)
AlgebraicGeometry.Space.exists_isZariskiCover_isInvariantOpen_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/InvariantOpenSaturation.lean, line 338. The attribute's comment: “part (2): covering by invariant quasi-compact open subspaces”.
Stacks 044G, part (2). For an open source morphism and a quasi-compact target morphism, the object space of a groupoid in algebraic spaces has a Zariski covering by invariant quasi-compact open subspaces: the saturations of the members of an affine Zariski covering supplied by Stacks 03FY.
theorem exists_isZariskiCover_isInvariantOpen_isQuasiCompactSpace
(G : GroupoidInAlgebraicSpaces B S hS A)
(hs : IsOpenMorphism B S hS G.source.hom)
(ht : IsQuasiCompact B S hS G.target.hom) :
∃ (I : Type u) (V : I → Subfunctor G.objects.obj),
IsZariskiCover B S hS I V ∧
∀ i, GroupoidInAlgebraicSpaces.IsInvariantOpen G (V i) ∧
IsQuasiCompactSpace B S hS (V i).toFunctor
Sources
Section78.19 Quotient sheaves#
Section 78.19 of the Stacks Project, Tag 044H. 7 tags here are carried by 26 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 044I, an equation
Tag 044I in the Stacks Project.
AlgebraicGeometry.Space.quotientPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Presheaf.lean, line 65. The attribute's comment: “the presheaf”.
Stacks 044I. The presheaf quotient of
Uby the equivalence relation generated by the image of the pre-relationj, as the coequalizer of its target and source maps.
noncomputable def quotientPresheaf (j : PreRelation R U) :
(BigFppfOver site S hS)ᵒᵖ ⥤ Type u
AlgebraicGeometry.Space.quotientPresheaf_obj_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Presheaf.lean, line 73. The attribute's comment: “pointwise quotient”.
Stacks 044I. At a test object
T, the quotient presheaf is the quotient ofU(T)by the relation generated by the image ofR(T); the identification sends the canonical class ofxto the class ofx.
theorem quotientPresheaf_obj_equiv (j : PreRelation R U) (T : BigFppfOver site S hS) :
∃ e : (quotientPresheaf j).obj (Opposite.op T) ≃
Quot (fun x y : U.left.obj (Opposite.op T) =>
∃ r : R.left.obj (Opposite.op T),
j.target.left.app (Opposite.op T) r = x ∧
j.source.left.app (Opposite.op T) r = y),
∀ x, e ((coequalizer.π j.target.left j.source.left).app (Opposite.op T) x) =
Quot.mk _ x
Tag 044J, a definition
Tag 044J in the Stacks Project.
AlgebraicGeometry.Space.epi_toQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionQuotientSheaf.lean, line 103. The attribute's comment: “the quotient projection is an epimorphism”.
Stacks 044J. The projection of
Uonto the quotient sheaf of a pre-relation is an epimorphism of fppf sheaves: a map out of the quotient sheaf is determined by its restriction toU.
theorem epi_toQuotientSheaf (j : PreRelation R U)
{hU : Presheaf.IsSheaf (BigFppfOver.topology site S hS) U.left}
(p : (⟨U.left, hU⟩ : Sheaf (BigFppfOver.topology site S hS) (Type u)) ⟶ quotientSheaf j)
(hp : p.hom = toQuotientSheaf j) : Epi p
AlgebraicGeometry.Space.quotientSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Sheaf.lean, line 60. The attribute's comment: “quotient by a pre-relation”.
The quotient sheaf
U/Rof a pre-relation: the fppf sheafification of its quotient presheaf.
noncomputable abbrev quotientSheaf (j : PreRelation R U) :
Sheaf (BigFppfOver.topology site S hS) (Type u)
AlgebraicGeometry.Space.target_toQuotientSheaf_eq_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Sheaf.lean, line 73. The attribute's comment: “relation equalized by the quotient projection”.
The quotient projection identifies the target and the source of every arrow of the relation.
theorem target_toQuotientSheaf_eq_source (j : PreRelation R U) :
j.target.left ≫ toQuotientSheaf j = j.source.left ≫ toQuotientSheaf j
AlgebraicGeometry.Space.toQuotientSheaf_quotientSheafDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Sheaf.lean, line 87. The attribute's comment: “descent of maps from the quotient”.
The descended map restricts to the original map on
U.
theorem toQuotientSheaf_quotientSheafDesc (j : PreRelation R U)
(A : Sheaf (BigFppfOver.topology site S hS) (Type u)) (k : U.left ⟶ A.obj)
(h : j.target.left ≫ k = j.source.left ≫ k) :
toQuotientSheaf j ≫ (quotientSheafDesc j A k h).hom = k
AlgebraicGeometry.Space.quotientSheafDesc_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Sheaf.lean, line 99. The attribute's comment: “uniqueness of descent”.
A map out of the quotient sheaf is determined by its restriction to
U.
theorem quotientSheafDesc_unique (j : PreRelation R U)
(A : Sheaf (BigFppfOver.topology site S hS) (Type u)) (k : U.left ⟶ A.obj)
(h : j.target.left ≫ k = j.source.left ≫ k) (d : quotientSheaf j ⟶ A)
(hd : toQuotientSheaf j ≫ d.hom = k) : d = quotientSheafDesc j A k h
AlgebraicGeometry.Space.quotientSheafToBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Sheaf.lean, line 117. The attribute's comment: “canonical morphism to the base”.
The canonical map from the quotient sheaf to the base.
noncomputable def quotientSheafToBase
(hZ : Presheaf.IsSheaf (BigFppfOver.topology site S hS) Z) (j : PreRelation R U) :
quotientSheaf j ⟶ baseSheaf hZ
AlgebraicGeometry.Space.toQuotientSheaf_quotientSheafToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Sheaf.lean, line 124. The attribute's comment: “compatibility of the base morphism”.
The map from the quotient to the base extends the structure map of
U.
theorem toQuotientSheaf_quotientSheafToBase
(hZ : Presheaf.IsSheaf (BigFppfOver.topology site S hS) Z) (j : PreRelation R U) :
toQuotientSheaf j ≫ (quotientSheafToBase hZ j).hom = U.hom
AlgebraicGeometry.Space.actionQuotientSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GroupActionQuotient.lean, line 293. The attribute's comment: “quotient by a group action”.
Stacks 044J for a group action: the quotient
X/Gof an algebraic space by the action of a group algebraic space, the quotient sheaf of the orbit pre-relation.
noncomputable abbrev actionQuotientSheaf (G X : Over B) [GrpObj G] [ModObj G X] :
Sheaf (BigFppfOver.topology site S hS) (Type u)
Tag 044L, a definition
Tag 044L in the Stacks Project.
AlgebraicGeometry.Space.PreRelation.QuotientIsAlgebraicSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Representability.lean, line 105. The attribute's comment: “pre-relation: quotient representable by an algebraic space”.
Stacks 044L. A pre-relation has quotient representable by an algebraic space when its quotient sheaf is an algebraic space.
noncomputable abbrev PreRelation.QuotientIsAlgebraicSpace (j : PreRelation R U) : Prop
AlgebraicGeometry.Space.PreRelation.HasRepresentableQuotient, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Representability.lean, line 111. The attribute's comment: “pre-relation: representable quotient”. References: SGA 3 IV (3.3.2), “(ii)”.
Stacks 044L. A pre-relation has a representable quotient when its quotient sheaf is represented by a scheme of the site.
noncomputable abbrev PreRelation.HasRepresentableQuotient (j : PreRelation R U) : Prop
AlgebraicGeometry.GroupoidInAlgebraicSpaces.QuotientIsAlgebraicSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Representability.lean, line 209. The attribute's comment: “groupoid: quotient representable by an algebraic space”. References: SGA 3 IV (3.3.2), “(ii)”.
Stacks 044L. A groupoid in algebraic spaces has quotient representable by an algebraic space when the quotient sheaf of its pre-relation
(t, s)is an algebraic space.
noncomputable abbrev QuotientIsAlgebraicSpace (G : GroupoidInAlgebraicSpaces site S hS B) :
Prop
AlgebraicGeometry.GroupoidInAlgebraicSpaces.HasRepresentableQuotient, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Representability.lean, line 216. The attribute's comment: “groupoid: representable quotient”. References: SGA 3 IV (3.3.2), “(ii)”.
Stacks 044L. A groupoid in algebraic spaces has a representable quotient when the quotient sheaf of its pre-relation
(t, s)is represented by a scheme of the site.
noncomputable abbrev HasRepresentableQuotient (G : GroupoidInAlgebraicSpaces site S hS B) :
Prop
Tag 044M, a lemma
Tag 044M in the Stacks Project.
AlgebraicGeometry.Space.isIso_quotientSheafDesc_of_isLocallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Representability.lean, line 166.
Stacks 044M. If
U ⟶ Ais a surjection of sheaves equalizing the relation, andRsurjects onto the kernel pair ofU ⟶ A, then the canonical map from the quotient sheaf toAis an isomorphism, soArepresents the quotientU/R.
theorem isIso_quotientSheafDesc_of_isLocallySurjective (j : PreRelation R U)
(A : Sheaf (BigFppfOver.topology site S hS) (Type u)) (k : U.left ⟶ A.obj)
(heq : j.target.left ≫ k = j.source.left ≫ k)
(hU : Presheaf.IsLocallySurjective (BigFppfOver.topology site S hS) k)
(hR : Presheaf.IsLocallySurjective (BigFppfOver.topology site S hS)
(pullback.lift j.target.left j.source.left heq)) :
IsIso (quotientSheafDesc j A k heq)
Tag 046O, a lemma
Tag 046O in the Stacks Project.
AlgebraicGeometry.Space.toQuotientSheaf_eq_iff_locally_related, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/PreEquivalenceRelation.lean, line 219. The attribute's comment: “local characterization”.
Stacks 046O. Two sections of
Uhave the same image in the quotient sheaf if and only if, on an fppf covering, they are the source and the target of a common section ofR.
theorem toQuotientSheaf_eq_iff_locally_related (T : BigFppfOver site S hS)
(a b : U.left.obj (op T)) :
((toQuotientSheaf j).app (op T) a = (toQuotientSheaf j).app (op T) b) ↔
∃ E : PreZeroHypercover.{u + 1} T,
BigFppfOver.IsCovering site S hS ⟨T, E⟩ ∧
∀ i : E.I₀, ∃ r : R.left.obj (op (E.X i)),
(U.left.map (E.f i).op a = j.source.left.app (op (E.X i)) r) ∧
(U.left.map (E.f i).op b = j.target.left.app (op (E.X i)) r)
AlgebraicGeometry.Space.isLocallySurjective_relationToQuotientPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/PreEquivalenceRelation.lean, line 265. The attribute's comment: “surjectivity of the relation map”.
Stacks 046O. The relation covers the fibre square of the quotient projection, as a map of fppf sheaves.
theorem isLocallySurjective_relationToQuotientPullback :
Presheaf.IsLocallySurjective (BigFppfOver.topology site S hS)
(pullback.lift j.source.left j.target.left
(target_toQuotientSheaf_eq_source j).symm)
Tag 046P, a lemma
Tag 046P in the Stacks Project.
AlgebraicGeometry.Space.restrictQuotientSheafMap_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Restriction.lean, line 291. The attribute's comment: “injectivity”.
Stacks 046P. Restricting a pre-equivalence relation gives an injective map of quotient sheaves.
theorem restrictQuotientSheafMap_mono (j : PreRelation R U) (g : U' ⟶ U)
(hj : IsPreEquivalenceRelation j)
(hU' : Presheaf.IsSheaf (BigFppfOver.topology site S hS) U'.left) :
Mono (restrictQuotientSheafMap j g)
AlgebraicGeometry.Space.restrictQuotientSheafMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Restriction.lean, line 351. The attribute's comment: “isomorphism under surjectivity”.
Stacks 046P. If
gis surjective as a map of fppf sheaves, then the induced map of quotient sheaves is an isomorphism.
theorem restrictQuotientSheafMap_isIso (j : PreRelation R U) (g : U' ⟶ U)
(hj : IsPreEquivalenceRelation j)
(hg : Presheaf.IsLocallySurjective (BigFppfOver.topology site S hS) g.left)
(hU : Presheaf.IsSheaf (BigFppfOver.topology site S hS) U.left)
(hU' : Presheaf.IsSheaf (BigFppfOver.topology site S hS) U'.left) :
IsIso (restrictQuotientSheafMap j g)
AlgebraicGeometry.Space.restrictQuotientSheafMap_isIso_of_isFppfCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Restriction.lean, line 378. The attribute's comment: “fppf-covering case”.
Stacks 046P. If
{g}is a one-element fppf covering, then the induced map of quotient sheaves is an isomorphism.
theorem restrictQuotientSheafMap_isIso_of_isFppfCovering (j : PreRelation R U) (g : U' ⟶ U)
(hj : IsPreEquivalenceRelation j)
(hg : IsFppfCovering site S hS (fun _ : PUnit ↦ U'.left) (fun _ ↦ g.left)) :
IsIso (restrictQuotientSheafMap j g)
Tag 044N, a lemma
Tag 044N in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces.restrictionQuotientSheafMap, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionQuotientSheaf.lean, line 137. The attribute's comment: “the map of quotient sheaves”.
Stacks 044N. The map
U'/R' ⟶ U/Rof fppf quotient sheaves induced by restricting a groupoid in algebraic spaces alongg, the arrow spaceR'of the restriction being the restricted pre-relation by Stacks 044D.
noncomputable abbrev restrictionQuotientSheafMap (G : GroupoidInAlgebraicSpaces C S hS B)
{U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects) :
Space.quotientSheaf (Space.PreRelation.restrict (Space.groupoidPreRelation G)
(restrictionObjectsHom G g)) ⟶
Space.quotientSheaf (Space.groupoidPreRelation G)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.mono_restrictionQuotientSheafMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionQuotientSheaf.lean, line 159. The attribute's comment: “injectivity”.
Stacks 044N. Restricting a groupoid in algebraic spaces gives an injective map of fppf quotient sheaves: the pre-relation of a groupoid is a pre-equivalence relation by Stacks 043X, and restricting a pre-equivalence relation is injective on quotient sheaves by Stacks 046P.
theorem mono_restrictionQuotientSheafMap (G : GroupoidInAlgebraicSpaces C S hS B)
{U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects) :
Mono (restrictionQuotientSheafMap G g)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.isIso_restrictionQuotientSheafMap_of_saturation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionQuotientSheaf.lean, line 169. The attribute's comment: “bijectivity when the saturation map is surjective”.
Stacks 044N. If every object of
Uis fppf-locally the source of an arrow ofGwhose target lifts alongg, then the map of quotient sheaves induced by the restriction is bijective.
theorem isIso_restrictionQuotientSheafMap_of_saturation
(G : GroupoidInAlgebraicSpaces C S hS B)
{U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects)
(hsat : Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS)
(restrictionSaturationMap G g).hom) :
IsIso (restrictionQuotientSheafMap G g)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.isIso_restrictionQuotientSheafMap_of_saturation_isFppfCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionQuotientSheaf.lean, line 215. The attribute's comment: “the saturation map is an fppf covering”.
Stacks 044N. If the saturation map is a one-member fppf covering, then the map of quotient sheaves induced by the restriction is bijective.
theorem isIso_restrictionQuotientSheafMap_of_saturation_isFppfCovering
(G : GroupoidInAlgebraicSpaces C S hS B)
{U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects)
(hsat : Space.IsFppfCovering C S hS
(fun _ : PUnit ↦ (AlgebraicSpaces.fiberProduct C S hS g G.target).obj)
(fun _ ↦ (restrictionSaturationMap G g).hom)) :
IsIso (restrictionQuotientSheafMap G g)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.isIso_restrictionQuotientSheafMap_of_isLocallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionQuotientSheaf.lean, line 228. The attribute's comment: “bijectivity when the restricting morphism is surjective”.
Stacks 044N. If
gis surjective as a map of fppf sheaves, then the map of quotient sheaves induced by the restriction is bijective.
theorem isIso_restrictionQuotientSheafMap_of_isLocallySurjective
(G : GroupoidInAlgebraicSpaces C S hS B)
{U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects)
(hg : Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS) g.hom) :
IsIso (restrictionQuotientSheafMap G g)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.isIso_restrictionQuotientSheafMap_of_isFppfCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionQuotientSheaf.lean, line 240. The attribute's comment: “the restricting morphism is an fppf covering”.
Stacks 044N. If
gis a one-member fppf covering, then the map of quotient sheaves induced by the restriction is bijective.
theorem isIso_restrictionQuotientSheafMap_of_isFppfCovering
(G : GroupoidInAlgebraicSpaces C S hS B)
{U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects)
(hg : Space.IsFppfCovering C S hS (fun _ : PUnit ↦ U'.obj) (fun _ ↦ g.hom)) :
IsIso (restrictionQuotientSheafMap G g)
Sources
Section78.20 Quotient stacks#
Section 78.20 of the Stacks Project, Tag 044O. 5 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 044P, an equation
Tag 044P in the Stacks Project.
Declarations registered for the tag:
AlgebraicGeometry.GroupoidInAlgebraicSpaces.toGroupoidInFunctors, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/PointwiseGroupoid.lean, line 40 (StacksFrontier): “the groupoid data on the fppf site”.Deformation.evaluationFunctor, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/PointwiseGroupoid.lean, line 42 (StacksFrontier): “the functor of pointwise groupoids”.Deformation.evaluationFunctor_groupoid, declared in the repository, registered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/PointwiseGroupoid.lean, line 43 (StacksFrontier): “each pointwise value is a groupoid”.
Tag 044Q, a definition
Tag 044Q in the Stacks Project.
AlgebraicGeometry.Space.quotientStackOfPointsAction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ActionInSite.lean, line 137. The attribute's comment: “part (2) for an action given on points”.
Stacks Project, Tag 044Q, part (2) for an action given on points: the quotient stack
[X/G]of a presheaf of groups acting on a presheaf, both represented by objects of the big fppf site overS, read over an algebraic spaceBoverS.
noncomputable abbrev quotientStackOfPointsAction (B : AlgebraicSpaces 𝒞 S hS)
(F : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ GrpCat.{u}) (P : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
[ModObj (F ⋙ forget GrpCat) P] {a b : BigFppfOver 𝒞 S hS}
(r : (F ⋙ forget GrpCat).RepresentableBy a) (s : P.RepresentableBy b) :
BasedCategory (BigFppfOver 𝒞 S hS)
AlgebraicGeometry.Space.isStackInGroupoids_quotientStackOfPointsAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ActionInSite.lean, line 150. The attribute's comment: “part (2) for an action given on points”.
The quotient stack of an action given on points is a stack in groupoids over the big fppf site.
theorem isStackInGroupoids_quotientStackOfPointsAction (B : AlgebraicSpaces 𝒞 S hS)
(F : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ GrpCat.{u}) (P : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
[ModObj (F ⋙ forget GrpCat) P] {a b : BigFppfOver 𝒞 S hS}
(r : (F ⋙ forget GrpCat).RepresentableBy a) (s : P.RepresentableBy b) :
Functor.IsStackInGroupoids (quotientStackOfPointsAction 𝒞 S hS B F P r s).p
(BigFppfOver.topology 𝒞 S hS)
AlgebraicGeometry.Stack.quotientStack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStack.lean, line 173. The attribute's comment: “part (1): quotient stack of a groupoid”.
Stacks 044Q, part (1). The quotient stack
[U/R]of a groupoid in algebraic spaces, as a category over the original big fppf site: the stackification of the pointwise groupoid fibration.
noncomputable def quotientStack
(G : GroupoidInAlgebraicSpaces C S hS B) :
BasedCategory (BigFppfOver C S hS)
AlgebraicGeometry.Stack.quotientStackOfAction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackOfAction.lean, line 84. The attribute's comment: “part (2): quotient stack of an action”.
Stacks 044Q, part (2). The quotient stack
[X/G]of an action of a group algebraic spaceGoverBon an algebraic spaceXoverB, as a category over the big fppf site: the quotient stack of part (1) of the action groupoid(X, G ×_B X, pr₁, a, m)of Stacks 0444, that is, the stackification of the pointwise groupoid fibration of that groupoid.
noncomputable abbrev quotientStackOfAction
(B : AlgebraicSpaces C S hS) (G X : Over B.obj) [GrpObj G] [ModObj G X]
(hG : IsAlgebraicSpace C S hS G.left) (hX : IsAlgebraicSpace C S hS X.left) :
BasedCategory (BigFppfOver C S hS)
Tag 044R, a lemma
Tag 044R in the Stacks Project.
AlgebraicGeometry.Stack.quotientStackProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackProjection.lean, line 148. The attribute's comment: “the canonical projection”.
The canonical arrow from the object space of a groupoid in algebraic spaces to its quotient stack, viewed as a functor over the big fppf site.
noncomputable def quotientStackProjection
(G : GroupoidInAlgebraicSpaces C S hS B) :
BasedFunctor
(fibredCategory C S hS G.objects.obj).val
(quotientStack G)
AlgebraicGeometry.Stack.quotientStackProjection_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackProjection.lean, line 163. The attribute's comment: “pointwise description of the projection”.
The projection sends a point of the object space to its image under the canonical map from the pointwise groupoid to its stackification.
theorem quotientStackProjection_obj
(G : GroupoidInAlgebraicSpaces C S hS B)
(x : (fibredCategory C S hS G.objects.obj).val.obj) :
(quotientStackProjection G).obj x =
(pointwiseToQuotientStack G).obj
⟨x.base, Discrete.as x.fiber⟩
AlgebraicGeometry.Stack.quotientStackProjection_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackProjection.lean, line 174. The attribute's comment: “pointwise description on morphisms”.
The projection sends every arrow of the object-space fibration to the corresponding identity-in-the-fibre arrow of the pointwise groupoid, followed by stackification.
theorem quotientStackProjection_map
(G : GroupoidInAlgebraicSpaces C S hS B)
{x y : (fibredCategory C S hS G.objects.obj).val.obj}
(f : x ⟶ y) :
∃ g : (⟨x.base, Discrete.as x.fiber⟩ :
(presheafOfGroupoids
(evaluationGroupoidFunctor G.toGroupoidInFunctors)).obj) ⟶
⟨y.base, Discrete.as y.fiber⟩,
g.base = f.base ∧
(G.toGroupoidInFunctors.evaluationArrowEquiv
(Opposite.op x.base) _ _ g.fiber).1 =
G.toGroupoidInFunctors.identity
(Opposite.op x.base) (Discrete.as x.fiber) ∧
(quotientStackProjection G).map f =
eqToHom (quotientStackProjection_obj G x) ≫
(pointwiseToQuotientStack G).map g ≫
eqToHom (quotientStackProjection_obj G y).symm
AlgebraicGeometry.Stack.quotientStackToBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackProjection.lean, line 416. The attribute's comment: “the canonical map to the base”.
The second canonical 1-morphism, the structure arrow
[U/R] ⟶ Bfrom the quotient stack to the base: the descent of the structure morphismU ⟶ Bof the object space, which is invariant because the source and the target of the groupoid are morphisms overB.
noncomputable def quotientStackToBase (G : GroupoidInAlgebraicSpaces C S hS B) :
quotientStack G ⥤ᵇ (fibredCategory C S hS B.obj).val
AlgebraicGeometry.Stack.quotientStackProjection_comp_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackProjection.lean, line 423. The attribute's comment: “composition with the base map”.
The composition
U ⟶ [U/R] ⟶ Bis the 1-morphism associated to the structure morphismU ⟶ B.
theorem quotientStackProjection_comp_toBase (G : GroupoidInAlgebraicSpaces C S hS B) :
BasedFunctor.comp (quotientStackProjection G) (quotientStackToBase G) =
(associatedMap C S hS G.objectsToBase.hom).1.hom
Tag 044S, a lemma
Tag 044S in the Stacks Project.
AlgebraicGeometry.Stack.quotientStackTwoArrow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/ProjectionTwoArrow.lean, line 665.
Stacks 044S. The canonical 2-morphism between the source and target maps to a quotient stack, making the square of Stacks 044R 2-commutative. Its components are the images of the groupoid arrows.
noncomputable def quotientStackTwoArrow
(G : GroupoidInAlgebraicSpaces C S hS B) :
BasedFunctor.comp (associatedMap C S hS G.source.hom).1.hom
(quotientStackProjection G) ⟶
BasedFunctor.comp (associatedMap C S hS G.target.hom).1.hom
(quotientStackProjection G)
AlgebraicGeometry.Stack.quotientStackTwoArrow_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/ProjectionTwoArrow.lean, line 676. The attribute's comment: “pointwise description”.
Stacks 044S. At a point of the arrow space, the canonical 2-morphism is the image of that groupoid arrow under the pointwise-groupoid map to the quotient stack.
theorem quotientStackTwoArrow_app
(G : GroupoidInAlgebraicSpaces C S hS B)
(x : (fibredCategory C S hS G.arrows.obj).val.obj) :
∃ g : (⟨x.base, G.source.hom.app (Opposite.op x.base) (Discrete.as x.fiber)⟩ :
(presheafOfGroupoids
(evaluationGroupoidFunctor G.toGroupoidInFunctors)).obj) ⟶
⟨x.base, G.target.hom.app (Opposite.op x.base) (Discrete.as x.fiber)⟩,
g.base = 𝟙 x.base ∧
(G.toGroupoidInFunctors.evaluationArrowEquiv
(Opposite.op x.base) _ _ g.fiber).1 = Discrete.as x.fiber ∧
HEq ((quotientStackTwoArrow G).app x) ((pointwiseToQuotientStack G).map g)
Tag 04M7, a remark
Tag 04M7 in the Stacks Project.
AlgebraicGeometry.Stack.quotientStackTwoArrow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/ProjectionTwoArrow.lean, line 665. The attribute's comment: “remark restating the 2-commutative square in the X-for-S_X notation”.
Stacks 044S. The canonical 2-morphism between the source and target maps to a quotient stack, making the square of Stacks 044R 2-commutative. Its components are the images of the groupoid arrows.
noncomputable def quotientStackTwoArrow
(G : GroupoidInAlgebraicSpaces C S hS B) :
BasedFunctor.comp (associatedMap C S hS G.source.hom).1.hom
(quotientStackProjection G) ⟶
BasedFunctor.comp (associatedMap C S hS G.target.hom).1.hom
(quotientStackProjection G)
Declarations registered for the tag:
quotientStackTwoArrowregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/ProjectionTwoArrow.lean, line 741 (StacksFrontier): “the two-commutative square of Stacks 044S, in the abbreviated notation that writes U for the stack in sets associated to U”.
Sources
Section78.21 Functoriality of quotient stacks#
Section 78.21 of the Stacks Project, Tag 04Y3. 2 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 046Q, a lemma
Tag 046Q in the Stacks Project.
AlgebraicGeometry.Stack.quotientPointwiseMapData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Functoriality.lean, line 132. The attribute's comment: “the strict map on the presenting groupoids”.
The strict natural map between the presenting pseudofunctors of the two pointwise groupoid fibrations: its component at a test object is the evaluated functor of the given groupoid morphism, and its naturality isomorphisms are transports.
noncomputable def quotientPointwiseMapData {G H : GroupoidInAlgebraicSpaces C S hS B}
(f : GroupoidInAlgebraicSpaces.Hom G H) :
{ α : (evaluationGroupoidFunctor G.toGroupoidInFunctors ⋙
Grpd.forgetToCat).toPseudofunctor' ⟶
(evaluationGroupoidFunctor H.toGroupoidInFunctors ⋙
Grpd.forgetToCat).toPseudofunctor' //
(∀ T : BigFppfOver C S hS,
(α.app ⟨op T⟩).toFunctor = f.toGroupoidHom.evaluation (op T)) ∧
(∀ {a b} (g : a ⟶ b),
∃ h : ((evaluationGroupoidFunctor G.toGroupoidInFunctors ⋙
Grpd.forgetToCat).toPseudofunctor').map g ≫ α.app b =
α.app a ≫ ((evaluationGroupoidFunctor H.toGroupoidInFunctors ⋙
Grpd.forgetToCat).toPseudofunctor').map g,
α.naturality g = eqToIso h) }
AlgebraicGeometry.Stack.quotientStackMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Functoriality.lean, line 265. The attribute's comment: “the induced morphism”.
The canonical 1-morphism
[f] : [U/R] ⟶ [U'/R']of quotient stacks induced by a morphism of groupoids in algebraic spaces over the same base.
noncomputable def quotientStackMap {G H : GroupoidInAlgebraicSpaces C S hS B}
(f : GroupoidInAlgebraicSpaces.Hom G H) :
BasedFunctor (quotientStack G) (quotientStack H)
AlgebraicGeometry.Stack.quotientStackMap_commutes, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/Functoriality.lean, line 279. The attribute's comment: “compatibility with the presentations”.
The induced 1-morphism intertwines the pointwise groupoid map with the two stackification maps, naturally and over the site.
noncomputable def quotientStackMap_commutes {G H : GroupoidInAlgebraicSpaces C S hS B}
(f : GroupoidInAlgebraicSpaces.Hom G H) :
BasedFunctor.comp (quotientPointwiseMap f) (pointwiseToQuotientStackBased H) ≅
BasedFunctor.comp (pointwiseToQuotientStackBased G) (quotientStackMap f)
Tag 04Y4, a lemma
Tag 04Y4 in the Stacks Project.
AlgebraicGeometry.Stack.isTwoFibreProduct_auxQuotientSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/FunctorialityQuotientStackTwoFibreProduct.lean, line 139. The attribute's comment: “the 2-commutative square of Section 78.21 and the identification of the quotient stack of the auxiliary groupoid with the 2-fibre product of the cospan”.
Stacks 04Y4. Let
φ : (U, R, s, t, c) ⟶ (U', R', s', t', c')be a morphism of groupoids in algebraic spaces over an algebraic spaceBover a schemeSof a big fppf site, writtenf : U ⟶ U'on object spaces, and let(U'', R'', s'', t'', c'')be the groupoid in algebraic spaces overBof Section 78.21, withU'' = U ×_{f, U', t'} R',R'' = R ×_{f ∘ s, U', t'} R',s''(r, r') = (s(r), r'),t''(r, r') = (t(r), c'(f(r), r'))andc''((r₁, r'₁), (r₂, r'₂)) = (c(r₁, r₂), r'₂). Then the square[U''/R''] ---[g]---> [U/R] | | | [φ] v v 𝒮_{U'} ----π'----> [U'/R']— whose horizontal arrow is the 1-morphism
[g]of Stacks 046Q induced by the projectiong : (U'', R'', s'', t'', c'') ⟶ (U, R, s, t, c), whose vertical arrow on the left is the descent to[U''/R'']of theR''-invariant morphismU'' ⟶ U',(u, r') ↦ s'(r'), whose vertical arrow on the right is the 1-morphism[φ]of Stacks 046Q, whose lower horizontal arrow is the canonical projectionπ'of Stacks 044R, and whose fillerAlgebraicGeometry.Stack.auxSquareCellis the arrowr'of the evaluated groupoid ofG'at a point(u, r')ofU''— is a 2-fibre product in the 2-category of stacks in groupoids over the big fppf site, so it identifies[U''/R'']with[U/R] ×_{[φ], [U'/R'], π'} 𝒮_{U'}.
noncomputable def isTwoFibreProduct_auxQuotientSquare (φ : Hom G G') :
Bicategory.IsTwoFibreProduct (auxQuotientSquare φ)
Sources
Section78.22 The 2-cartesian square of a quotient stack#
Section 78.22 of the Stacks Project, Tag 04M8. 3 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 044V, a lemma
Tag 044V in the Stacks Project.
AlgebraicGeometry.Stack.isomPresheaf_equiv_arrowFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/IsomorphismSheaf.lean, line 547.
The canonical map from pointwise groupoid arrows to isomorphisms between their images in the quotient stack is an isomorphism of presheaves on the fppf slice site. The pointwise-groupoid morphism presheaf is the fibre of the arrow space over the chosen pair of object-space points.
theorem isomPresheaf_equiv_arrowFiber
(C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
{B : AlgebraicSpaces C S hS}
(G : GroupoidInAlgebraicSpaces C S hS B)
(T : BigFppfOver C S hS)
(x y : (quotientPrestack G).p.Fiber T) :
IsIso ((isFibredOneMorphism_toQuotientStack G).morPresheafMap x y)
AlgebraicGeometry.Stack.isomPresheaf_iso_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/IsomorphismSheaf.lean, line 885. The attribute's comment: “pullback description of the isomorphism sheaf”.
The isomorphism sheaf of two presented objects is canonically the slice pullback of the arrow space along their two points. The identification sends pointwise prestack arrows to their images under
pointwiseToQuotientStack.
theorem isomPresheaf_iso_pullback
(C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
{B : AlgebraicSpaces C S hS}
(G : GroupoidInAlgebraicSpaces C S hS B)
(T : BigFppfOver C S hS)
(x' y' : G.objects.obj.obj (Opposite.op T))
(x y : (quotientStack G).p.Fiber T)
(hx : x.1 = (pointwiseToQuotientStack G).obj ⟨T, x'⟩)
(hy : y.1 = (pointwiseToQuotientStack G).obj ⟨T, y'⟩) :
∃ e : (arrowFiberOver G T x' y' ⋙ uliftFunctor.{u + 1, u}) ≅
(quotientStack G).p.isomPresheaf x y,
IsCanonicalArrowFiberIso G T x' y' x y hx hy e
AlgebraicGeometry.Stack.isomPresheafPullbackIso_inv_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/IsomorphismSheaf.lean, line 931. The attribute's comment: “canonical inverse comparison on prestack arrows”.
The inverse comparison recovers the arrow-space section of each pointwise prestack arrow from its canonical image in the quotient stack.
theorem isomPresheafPullbackIso_inv_app (V : Over T)
(r : (show G.toGroupoidInFunctors.Evaluation (op V.left) from
G.objects.obj.map V.hom.op x') ⟶ G.objects.obj.map V.hom.op y') :
arrowFiberOverSectionArrow G T x' y' V
((isomPresheafPullbackIso G T x' y' x y hx hy).inv.app (op V)
(pointwiseArrowSection G T x' y' x y hx hy V r)).down =
(G.toGroupoidInFunctors.evaluationArrowEquiv (op V.left) _ _ r).1
AlgebraicGeometry.Stack.isomPresheafPullbackIso_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/IsomorphismSheaf.lean, line 944. The attribute's comment: “canonical forward comparison on prestack arrows”.
The forward comparison sends an arrow-space section to the isomorphism induced by that very prestack arrow. This rules out translating the identification by a nonidentity automorphism.
theorem isomPresheafPullbackIso_hom_app (V : Over T)
(r : (show G.toGroupoidInFunctors.Evaluation (op V.left) from
G.objects.obj.map V.hom.op x') ⟶ G.objects.obj.map V.hom.op y')
(s : (arrowFiberOver G T x' y').obj (op V))
(hs : arrowFiberOverSectionArrow G T x' y' V s =
(G.toGroupoidInFunctors.evaluationArrowEquiv (op V.left) _ _ r).1) :
(isomPresheafPullbackIso G T x' y' x y hx hy).hom.app (op V) (ULift.up s) =
pointwiseArrowSection G T x' y' x y hx hy V r
Tag 04M9, a lemma
Tag 04M9 in the Stacks Project.
AlgebraicGeometry.Stack.quotientStack_twoFibreProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/TwoFibreProduct.lean, line 1033.
The canonical square of the quotient stack is a two-fibre product of stacks in groupoids over the big fppf site.
noncomputable def quotientStack_twoFibreProduct
(G : GroupoidInAlgebraicSpaces C S hS B) :
Bicategory.IsTwoFibreProduct (quotientStackSquare G)
Tag 044W, a lemma
Tag 044W in the Stacks Project.
AlgebraicGeometry.Stack.isomPresheaf_locallyAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/IsomorphismSheafAlgebraic.lean, line 439.
The isomorphism sheaf of two quotient-stack objects is locally representable by an algebraic space in the fppf topology.
theorem isomPresheaf_locallyAlgebraicSpace
(C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
{B : AlgebraicSpaces C S hS}
(G : GroupoidInAlgebraicSpaces C S hS B)
(T : BigFppfOver C S hS)
(x y : (quotientStack G).p.Fiber T) :
∃ R ∈ BigFppfOver.topology C S hS T,
∀ ⦃V : BigFppfOver C S hS⦄ ⦃f : V ⟶ T⦄,
R.arrows f →
∃ F : (BigFppfOver C V.left.1 V.left.2)ᵒᵖ ⥤ Type u,
IsAlgebraicSpace C V.left.1 V.left.2 F ∧
Nonempty (F ⋙ uliftFunctor.{u + 1, u} ≅
(Over.iteratedSliceBackward V).op ⋙ (Over.map f).op ⋙
(quotientStack G).p.isomPresheaf x y)
Sources
Section78.23 The 2-coequalizer property of a quotient stack#
Section 78.23 of the Stacks Project, Tag 04MA. 2 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 044T, a lemma
Tag 044T in the Stacks Project.
AlgebraicGeometry.Stack.quotientStackTwoArrow_source_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/TwoArrowCocycle.lean, line 428. The attribute's comment: “source endpoint equality”.
Stacks 044T. The composite arrow and the second arrow of a composable pair have the same source in the quotient stack.
theorem quotientStackTwoArrow_source_comp_eq
(G : GroupoidInAlgebraicSpaces C S hS B) :
let a₁ := (associatedMap C S hS
(pullback.snd G.source.hom G.target.hom)).1.hom
let ac := (associatedMap C S hS G.comp.hom).1.hom
let Fs := BasedFunctor.comp
(associatedMap C S hS G.source.hom).1.hom
(quotientStackProjection G)
BasedFunctor.comp ac Fs = BasedFunctor.comp a₁ Fs
AlgebraicGeometry.Stack.quotientStackTwoArrow_middle_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/TwoArrowCocycle.lean, line 442. The attribute's comment: “middle endpoint equality”.
Stacks 044T. The target of the second arrow is the source of the first arrow of a composable pair, as 1-morphisms to the quotient stack.
theorem quotientStackTwoArrow_middle_comp_eq
(G : GroupoidInAlgebraicSpaces C S hS B) :
let a₀ := (associatedMap C S hS
(pullback.fst G.source.hom G.target.hom)).1.hom
let a₁ := (associatedMap C S hS
(pullback.snd G.source.hom G.target.hom)).1.hom
let Fs := BasedFunctor.comp
(associatedMap C S hS G.source.hom).1.hom
(quotientStackProjection G)
let Ft := BasedFunctor.comp
(associatedMap C S hS G.target.hom).1.hom
(quotientStackProjection G)
BasedFunctor.comp a₁ Ft = BasedFunctor.comp a₀ Fs
AlgebraicGeometry.Stack.quotientStackTwoArrow_target_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/TwoArrowCocycle.lean, line 460. The attribute's comment: “target endpoint equality”.
Stacks 044T. The first arrow of a composable pair and the composite arrow have the same target in the quotient stack.
theorem quotientStackTwoArrow_target_comp_eq
(G : GroupoidInAlgebraicSpaces C S hS B) :
let a₀ := (associatedMap C S hS
(pullback.fst G.source.hom G.target.hom)).1.hom
let ac := (associatedMap C S hS G.comp.hom).1.hom
let Ft := BasedFunctor.comp
(associatedMap C S hS G.target.hom).1.hom
(quotientStackProjection G)
BasedFunctor.comp a₀ Ft = BasedFunctor.comp ac Ft
AlgebraicGeometry.Stack.quotientStackTwoArrow_cocycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/TwoArrowCocycle.lean, line 706. The attribute's comment: “vertical-composition identity”.
Stacks 044T. The canonical 2-morphism of a quotient stack sends composition of groupoid arrows to vertical composition of 2-morphisms.
theorem quotientStackTwoArrow_cocycle
(G : GroupoidInAlgebraicSpaces C S hS B) :
let a₀ := (associatedMap C S hS
(pullback.fst G.source.hom G.target.hom)).1.hom
let a₁ := (associatedMap C S hS
(pullback.snd G.source.hom G.target.hom)).1.hom
let ac := (associatedMap C S hS G.comp.hom).1.hom
let α := quotientStackTwoArrow G
BasedCategory.whiskerLeft ac α =
eqToHom (quotientStackTwoArrow_source_comp_eq G) ≫
BasedCategory.whiskerLeft a₁ α ≫
eqToHom (quotientStackTwoArrow_middle_comp_eq G) ≫
BasedCategory.whiskerLeft a₀ α ≫
eqToHom (quotientStackTwoArrow_target_comp_eq G)
Tag 044U, a lemma
Tag 044U in the Stacks Project.
AlgebraicGeometry.Stack.quotientStack_desc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/Descent.lean, line 917.
Stacks 044U. The quotient stack is a 2-coequalizer of the 2-commutative square of Stacks 044S in the 2-category of stacks in groupoids over the big fppf site: given a stack in groupoids
X, a 1-morphismf : 𝒮_U ⟶ Xout of the object space of a groupoid in algebraic spaces and a 2-morphismβ : s ∘ f ⟶ t ∘ fsatisfying the composition cocycle on the arrows, there are a 1-morphismg : [U/R] ⟶ Xout of the quotient stack and a 2-isomorphismα : π ∘ g ≅ fon the object space which carry the canonical 2-morphism of Stacks 044S toβ.The comparison 2-isomorphism is kept as data rather than replaced by the bare existence of some 1-morphism, since the compatibility with the 2-morphism of Stacks 044S is a statement about it.
public theorem quotientStack_desc
(G : GroupoidInAlgebraicSpaces C S hS B)
(X : BasedCategory (BigFppfOver C S hS))
(hX : X.p.IsStackInGroupoids.{u + 1} (BigFppfOver.topology C S hS))
(f : BasedFunctor (fibredCategory C S hS G.objects.obj).val X)
(β : BasedFunctor.comp
(associatedMap C S hS G.source.hom).1.hom f ⟶
BasedFunctor.comp (associatedMap C S hS G.target.hom).1.hom f)
(hβ : IsCocycle G X f β) :
∃ (g : BasedFunctor (quotientStack G) X)
(α : BasedFunctor.comp (quotientStackProjection G) g ≅ f),
BasedCategory.whiskerLeft
(associatedMap C S hS G.source.hom).1.hom α.hom ≫ β =
BasedCategory.whiskerRight (quotientStackTwoArrow G) g ≫
BasedCategory.whiskerLeft
(associatedMap C S hS G.target.hom).1.hom α.hom
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.