80 Bootstrap
Chapter 80 of the Stacks Project, Bootstrap, Tag 046A: the 10 sections of its 12 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 38 tags are carried by 76 declarations of the repository (all in StacksFrontier) and 2 registered declarations.
Section80.3 Morphisms representable by algebraic spaces#
Section 80.3 of the Stacks Project, Tag 02YP. 11 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 02YQ, a definition
Tag 02YQ in the Stacks Project.
AlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RepresentableByAlgebraicSpaces.lean, line 85.
Stacks Project, Tag 02YQ. A morphism of presheaves is representable by algebraic spaces if its pullback to every scheme over the base is an algebraic space.
abbrev IsRepresentableByAlgebraicSpaces (B : BigFppfSite.{u}) (S : Scheme.{u})
(hS : B.Contains S) {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) : Prop
Tag 03BN, a lemma
Tag 03BN in the Stacks Project.
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Stability.lean, line 93.
Stacks 03BN. A morphism between algebraic spaces over
Sis representable by algebraic spaces: its base change along a scheme-valued point of its target is a fibre product of three algebraic spaces.
theorem isRepresentableByAlgebraicSpaces_of_isAlgebraicSpace
{X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
IsRepresentableByAlgebraicSpaces B S hS f
Tag 03Y0, a lemma
Tag 03Y0 in the Stacks Project.
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_isPullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RepresentableByAlgebraicSpaces.lean, line 222.
Stacks Project, Tag 03Y0. A cartesian base change of a morphism representable by algebraic spaces is representable by algebraic spaces.
lemma isRepresentableByAlgebraicSpaces_of_isPullback
(B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
{F G G' H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(p : H ⟶ F) (a' : H ⟶ G') (a : F ⟶ G) (g : G' ⟶ G)
(h : IsPullback p a' a g)
(ha : IsRepresentableByAlgebraicSpaces B S hS a) :
IsRepresentableByAlgebraicSpaces B S hS a'
Tag 02YR, a lemma
Tag 02YR in the Stacks Project.
AlgebraicGeometry.Space.isSheaf_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RepresentableByAlgebraicSpaces.lean, line 157.
Stacks Project, Tag 02YR. A transformation representable by algebraic spaces has a sheaf as its source if its target is a sheaf.
theorem isSheaf_of_isRepresentableByAlgebraicSpaces
(B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
{F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(a : F ⟶ G)
(ha : IsRepresentableByAlgebraicSpaces B S hS a)
(hG : Presheaf.IsSheaf (BigFppfOver.topology B S hS) G) :
Presheaf.IsSheaf (BigFppfOver.topology B S hS) F
Tag 05LA, a lemma
Tag 05LA in the Stacks Project.
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RepresentableDiagonal.lean, line 62.
Stacks Project, Tag 05LA. The relative diagonal of a transformation representable by algebraic spaces is representable by algebraic spaces.
theorem isRepresentableByAlgebraicSpaces_diagonal
(B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
{F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(a : F ⟶ G) (ha : IsRepresentableByAlgebraicSpaces B S hS a) :
IsRepresentableByAlgebraicSpaces B S hS (pullback.diagonal a)
Tag 02YS, a lemma
Tag 02YS in the Stacks Project.
AlgebraicGeometry.Space.isAlgebraicSpaceULift_of_isRepresentable_uliftYoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedProperLocality.lean, line 104. The attribute's comment: “representable target, arbitrary value universe”.
The source of a morphism of presheaves with values in
Type (max w u)which is representable by algebraic spaces and whose target is isomorphic to the universe-lifted Yoneda presheaf of an object of the big fppf site ofSis an algebraic space overS.
theorem isAlgebraicSpaceULift_of_isRepresentable_uliftYoneda
{F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)} {U : BigFppfOver B S hS} (a : F ⟶ G)
(e : G ≅ (uliftYoneda.{w}).obj U)
(ha : IsRepresentableByAlgebraicSpacesULift.{w} B S hS a) :
IsAlgebraicSpaceULift.{w} B S hS F
AlgebraicGeometry.isAlgebraicSpace_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentableByAlgebraicSpaces.lean, line 187.
Stacks 02YS. A transformation representable by algebraic spaces to an algebraic space over
Shas an algebraic space overSas its source.The three clauses of
AlgebraicGeometry.IsAlgebraicSpaceare verified as in Stacks 02WY. The sheaf clause is Stacks 02YR. The diagonal clause is the compositeΔ_F = Δ_{F/G} ≫ (F ×_G F ⟶ F × F), representable becauseΔ_{F/G}is — this is Stacks 05LA in the strengthened form above — and because the second factor is a base change ofΔ_G. For the atlas clause, base-changing a scheme atlas ofGalongagives a surjective étale morphism toFfrom an algebraic space, and composing it with a scheme atlas of that algebraic space gives a scheme atlas ofF.
theorem isAlgebraicSpace_of_isRepresentableByAlgebraicSpaces
{F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(a : F ⟶ G) (ha : Space.IsRepresentableByAlgebraicSpaces B S hS a)
(hG : IsAlgebraicSpace B S hS G) :
IsAlgebraicSpace B S hS F
Tag 03XY, a lemma
Tag 03XY in the Stacks Project.
AlgebraicGeometry.Space.isAlgebraicSpaceULift_pullback_of_isRepresentableULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Representable.lean, line 404. The attribute's comment: “in an arbitrary value universe”.
The fibre product of an algebraic space over
Swith the source of a morphism representable by algebraic spaces, over the target of that morphism, is an algebraic space overS, for presheaves on the big fppf site ofSwith values inType (max w u).
theorem isAlgebraicSpaceULift_pullback_of_isRepresentableULift
{F G X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)} (a : F ⟶ G) (f : X ⟶ G)
(ha : IsRepresentableByAlgebraicSpacesULift.{w} B S hS a)
(hX : IsAlgebraicSpaceULift.{w} B S hS X) :
IsAlgebraicSpaceULift.{w} B S hS (pullback f a)
AlgebraicGeometry.Space.isAlgebraicSpace_pullback_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Stability.lean, line 103.
Stacks 03XY. The fibre product of an algebraic space over
Swith the source of a morphism representable by algebraic spaces, over the target of that morphism, is an algebraic space overS.
theorem isAlgebraicSpace_pullback_of_isRepresentableByAlgebraicSpaces
{F G X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) (f : X ⟶ G)
(ha : IsRepresentableByAlgebraicSpaces B S hS a)
(hX : IsAlgebraicSpace B S hS X) :
IsAlgebraicSpace B S hS (pullback f a)
Tag 03Y1, a lemma
Tag 03Y1 in the Stacks Project.
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Stability.lean, line 118.
Stacks 03Y1. A composite of morphisms of presheaves on the big fppf site of
Srepresentable by algebraic spaces is representable by algebraic spaces.The base change of
a ≫ balongξis the base change ofaalong the second projection of the base change ofbalongξ, which is an algebraic space by Stacks 03XY.
theorem isRepresentableByAlgebraicSpaces_comp
{F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) (b : G ⟶ H)
(ha : IsRepresentableByAlgebraicSpaces B S hS a)
(hb : IsRepresentableByAlgebraicSpaces B S hS b) :
IsRepresentableByAlgebraicSpaces B S hS (a ≫ b)
Tag 046D, a lemma
Tag 046D in the Stacks Project.
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_prod_map, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Stability.lean, line 132.
Stacks 046D. The product of two morphisms of presheaves on the big fppf site of
Srepresentable by algebraic spaces is representable by algebraic spaces.The product
a₁ ⨯ a₂is the composite ofa₁ ⨯ 𝟙with𝟙 ⨯ a₂, and each of these is a base change of one of the two factors along a projection.
lemma isRepresentableByAlgebraicSpaces_prod_map
{F₁ F₂ G₁ G₂ : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a₁ : F₁ ⟶ G₁) (a₂ : F₂ ⟶ G₂)
(h₁ : IsRepresentableByAlgebraicSpaces B S hS a₁)
(h₂ : IsRepresentableByAlgebraicSpaces B S hS a₂) :
IsRepresentableByAlgebraicSpaces B S hS (prod.map a₁ a₂)
Tag 0AMN, a lemma
Tag 0AMN in the Stacks Project.
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpacesULift_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Representable.lean, line 417. The attribute's comment: “representable by algebraic spaces in an arbitrary value universe”.
If the relative diagonal of
band the compositea ≫ bare representable by algebraic spaces, then so isa, for presheaves on the big fppf site ofSwith values inType (max w u).
theorem isRepresentableByAlgebraicSpacesULift_of_comp
{F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)} (a : F ⟶ G) (b : G ⟶ H)
(hdiag : IsRepresentableByAlgebraicSpacesULift.{w} B S hS (pullback.diagonal b))
(hcomp : IsRepresentableByAlgebraicSpacesULift.{w} B S hS (a ≫ b)) :
IsRepresentableByAlgebraicSpacesULift.{w} B S hS a
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Stability.lean, line 153.
Stacks 0AMN. If the relative diagonal of
band the compositea ≫ bare representable by algebraic spaces, then so isa.The base change of
aalongξis the base change of the relative diagonal ofbalong the canonical morphism from the base change ofa ≫ balongξ ≫ btopullback b b.
theorem isRepresentableByAlgebraicSpaces_of_comp
{F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) (b : G ⟶ H)
(hdiag : IsRepresentableByAlgebraicSpaces B S hS (pullback.diagonal b))
(hcomp : IsRepresentableByAlgebraicSpaces B S hS (a ≫ b)) :
IsRepresentableByAlgebraicSpaces B S hS a
Tag 07WE, a lemma
Tag 07WE in the Stacks Project.
AlgebraicGeometry.Space.isSheaf_of_locallySurjective_representable_subfunctors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/SheafFromSubsheaves.lean, line 674.
Stacks 07WE. A Zariski sheaf on the big fppf site over
Swhich is covered, locally for the fppf topology, by fppf subsheaves whose inclusions are representable by algebraic spaces is an fppf sheaf.
theorem isSheaf_of_locallySurjective_representable_subfunctors
(B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
(F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf (B.zariskiTopology.over (B.obj hS)) F)
(I : Type v) (G : I → Subfunctor F)
(hG : ∀ i, Presheaf.IsSheaf (BigFppfOver.topology B S hS) (G i).toFunctor)
(hrep : ∀ i, IsRepresentableByAlgebraicSpaces B S hS (G i).ι)
(hcover : Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) (iSup G).ι) :
Presheaf.IsSheaf (BigFppfOver.topology B S hS) F
Sources
Section80.4 Properties of maps of presheaves representable by algebraic spaces#
Section 80.4 of the Stacks Project, Tag 046E. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 03XZ, a definition
Tag 03XZ in the Stacks Project.
AlgebraicGeometry.Space.HasProperty, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentableProperty.lean, line 78.
Stacks 03XZ. A map of presheaves
a : F ⟶ Gon the big fppf site ofSwhich is representable by algebraic spaces has propertyPwhen, for every objectUof the site and everyξ : h_U ⟶ G, the morphism of algebraic spacesU ×_G F ⟶ UhasP.
abbrev HasProperty (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
(P : MorphismProperty (AlgebraicSpaces B S hS))
{F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G)
(ha : IsRepresentableByAlgebraicSpaces B S hS a) : Prop
Tag 046F, a lemma
Tag 046F in the Stacks Project.
AlgebraicGeometry.Space.HasProperty.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BootstrapRepresentableCalculus.lean, line 98.
Stacks 046F. In a Cartesian square of presheaves on the big fppf site of
Swhose right-hand columnais representable by algebraic spaces and has a propertyPof morphisms of algebraic spaces overS, the left-hand columna'is representable by algebraic spaces (Stacks 03Y0) and hasP.Only invariance of
Punder isomorphism is used, which is weaker than the two conditions Stacks imposes onPin Definition 03XZ.
theorem HasProperty.of_isPullback {P : MorphismProperty (AlgebraicSpaces B S hS)}
[P.RespectsIso] {F G F' G' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {a : F ⟶ G} {g : G' ⟶ G}
{k : F' ⟶ F} {a' : F' ⟶ G'} (sq : IsPullback k a' a g)
(ha : IsRepresentableByAlgebraicSpaces B S hS a) (h : HasProperty B S hS P a ha) :
HasProperty B S hS P a' (IsRepresentableByAlgebraicSpaces.of_isPullback sq ha)
AlgebraicGeometry.Space.hasProperty_of_isPullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Properties.lean, line 113. The attribute's comment: “property”.
Stacks 046F. A property of morphisms of algebraic spaces over
Swhich is stable under base change is inherited, as a property of a morphism of presheaves representable by algebraic spaces, by every cartesian base change of that morphism.
lemma hasProperty_of_isPullback (P : MorphismProperty (AlgebraicSpaces B S hS))
[P.IsStableUnderBaseChange]
{F G G' H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(p : H ⟶ F) (a' : H ⟶ G') (a : F ⟶ G) (g : G' ⟶ G) (h : IsPullback p a' a g)
(ha : IsRepresentableByAlgebraicSpaces B S hS a)
(hP : HasProperty B S hS P a ha) :
HasProperty B S hS P a'
(isRepresentableByAlgebraicSpaces_of_isPullback B S hS p a' a g h ha)
Declarations registered for the tag:
isRepresentableByAlgebraicSpaces_of_isPullbackregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Properties.lean, line 107 (StacksFrontier): “representability”.
Tag 046G, a lemma
Tag 046G in the Stacks Project.
AlgebraicGeometry.Space.hasProperty_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Properties.lean, line 229. The attribute's comment: “property of the composite”.
Stacks 046G. A composite of morphisms of presheaves on the big fppf site of
Srepresentable by algebraic spaces has a propertyPof morphisms of algebraic spaces overSas soon as both factors do, providedPis stable under base change, local on the base for the fppf topology, and stable under composition.
theorem hasProperty_comp (P : MorphismProperty (AlgebraicSpaces B S hS))
[P.IsStableUnderBaseChange] [P.IsLocalAtTarget (Topology.fppf.precoverage B S hS)]
[P.IsStableUnderComposition]
{F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) (b : G ⟶ H)
(ha : IsRepresentableByAlgebraicSpaces B S hS a)
(hb : IsRepresentableByAlgebraicSpaces B S hS b)
(hPa : HasProperty B S hS P a ha) (hPb : HasProperty B S hS P b hb) :
HasProperty B S hS P (a ≫ b)
(isRepresentableByAlgebraicSpaces_comp B S hS a b ha hb)
Declarations registered for the tag:
isRepresentableByAlgebraicSpaces_compregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Properties.lean, line 221 (StacksFrontier): “representability”.
Tag 046H, a lemma
Tag 046H in the Stacks Project.
AlgebraicGeometry.Space.hasProperty_prod_map, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Properties.lean, line 263.
Stacks 046H. The product of two morphisms of presheaves on the big fppf site of
Srepresentable by algebraic spaces has a propertyPof morphisms of algebraic spaces overSas soon as both factors do, providedPis stable under base change, local on the base for the fppf topology, and stable under composition.The product is the composite of two base changes of the two factors, so this follows from Stacks 046F and Stacks 046G.
lemma hasProperty_prod_map (P : MorphismProperty (AlgebraicSpaces B S hS))
[P.IsStableUnderBaseChange] [P.IsLocalAtTarget (Topology.fppf.precoverage B S hS)]
[P.IsStableUnderComposition]
{F₁ F₂ G₁ G₂ : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a₁ : F₁ ⟶ G₁) (a₂ : F₂ ⟶ G₂)
(h₁ : IsRepresentableByAlgebraicSpaces B S hS a₁)
(h₂ : IsRepresentableByAlgebraicSpaces B S hS a₂)
(ha₁ : HasProperty B S hS P a₁ h₁) (ha₂ : HasProperty B S hS P a₂ h₂) :
HasProperty B S hS P (prod.map a₁ a₂)
(isRepresentableByAlgebraicSpaces_prod_map B S hS a₁ a₂ h₁ h₂)
Tag 0AM1, a lemma
Tag 0AM1 in the Stacks Project.
AlgebraicGeometry.Space.HasProperty.mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentabilityCriteria.lean, line 102.
The property tested by
AlgebraicGeometry.Space.HasPropertymay be enlarged: ifPimpliesQfor every morphism of algebraic spaces overS, then a morphism of presheaves representable by algebraic spaces havingPalso hasQ.
theorem HasProperty.mono {P Q : MorphismProperty (AlgebraicSpaces B S hS)} (hPQ : P ≤ Q)
{F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {a : F ⟶ G}
{ha : IsRepresentableByAlgebraicSpaces B S hS a}
(h : HasProperty B S hS P a ha) : HasProperty B S hS Q a ha
Tag 04S1, a lemma
Tag 04S1 in the Stacks Project.
AlgebraicGeometry.Space.isLocallySurjective_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/LocallySurjective.lean, line 70.
Stacks 04S1. A morphism of fppf sheaves on the big fppf site of
Swhich is representable by algebraic spaces, surjective, flat and locally of finite presentation is locally surjective for the big fppf topology.
theorem isLocallySurjective_of_isRepresentableByAlgebraicSpaces
(B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
{F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(_hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
(_hG : Presheaf.IsSheaf (BigFppfOver.topology B S hS) G)
(a : F ⟶ G)
(ha : IsRepresentableByAlgebraicSpaces B S hS a)
(hflat : HasProperty B S hS (fun _ _ f => IsFlat B S hS f.hom) a ha)
(hlfp : HasProperty B S hS
(fun _ _ f => IsLocallyOfFinitePresentation B S hS f.hom) a ha)
(hsurj : HasProperty B S hS (fun _ _ f => IsSurjective B S hS f.hom) a ha) :
Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) a
Sources
Section80.5 Bootstrapping the diagonal#
Section 80.5 of the Stacks Project, Tag 046I. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 03Y2, a lemma
Tag 03Y2 in the Stacks Project.
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_diag_iff_forall_yoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Diagonal.lean, line 318. The attribute's comment: “conditions (1) and (2)”.
Stacks 03Y2, conditions (1) and (2). The absolute diagonal of a presheaf on the big fppf site of
Sis representable by algebraic spaces exactly when every morphism to that presheaf from a scheme overSis representable by algebraic spaces.
theorem isRepresentableByAlgebraicSpaces_diag_iff_forall_yoneda
(F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) :
IsRepresentableByAlgebraicSpaces B S hS (diag F) ↔
∀ (T : BigFppfOver B S hS) (f : yoneda.obj T ⟶ F),
IsRepresentableByAlgebraicSpaces B S hS f
AlgebraicGeometry.Space.forall_yoneda_isRepresentableByAlgebraicSpaces_iff_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Diagonal.lean, line 342. The attribute's comment: “conditions (2) and (3)”.
Stacks 03Y2, conditions (2) and (3). Representability by algebraic spaces of every morphism to a presheaf on the big fppf site of
Sfrom a scheme overSis equivalent to representability by algebraic spaces of every morphism to it from an algebraic space overS.
theorem forall_yoneda_isRepresentableByAlgebraicSpaces_iff_isAlgebraicSpace
(F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) :
(∀ (T : BigFppfOver B S hS) (f : yoneda.obj T ⟶ F),
IsRepresentableByAlgebraicSpaces B S hS f) ↔
∀ (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u), IsAlgebraicSpace B S hS X →
∀ (f : X ⟶ F), IsRepresentableByAlgebraicSpaces B S hS f
Tag 046J, a lemma
Tag 046J in the Stacks Project.
AlgebraicGeometry.Space.relativelyRepresentable_separated_locallyQuasiFinite_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/SeparatedQuasiFiniteDescent.lean, line 480.
Stacks 046J, conditional only on the fppf locality of separatedness.
In a cartesian square of sheaves on the big fppf site of
Swhose right-hand columngis representable by algebraic spaces, surjective, flat and locally of finite presentation and whose top rowais representable by algebraic spaces, separated and locally quasi-finite, the bottom rowbis representable by objects of the site, separated and locally quasi-finite.Representability of
bby objects of the site isAlgebraicGeometry.Space.relativelyRepresentable_of_isPullback_of_flat_surjective, the source's own argument by effective fppf descent of schemes. Separatedness and local quasi-finiteness descend by Stacks 0421 and Stacks 0427, each read at the fppf precoverage from its fpqc form.
theorem relativelyRepresentable_separated_locallyQuasiFinite_of_isPullback
{E F H G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(a : E ⟶ F) (f : E ⟶ H) (g : F ⟶ G) (b : H ⟶ G) (sq : IsPullback a f g b)
(hH : Presheaf.IsSheaf (BigFppfOver.topology B S hS) H)
(hG : Presheaf.IsSheaf (BigFppfOver.topology B S hS) G)
(hgRep : IsRepresentableByAlgebraicSpaces B S hS g)
(hgSurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) g hgRep)
(hgFlat : HasProperty B S hS (flatProperty B S hS) g hgRep)
(hgLfp : HasProperty B S hS (locallyOfFinitePresentationProperty B S hS) g hgRep)
(haRep : IsRepresentableByAlgebraicSpaces B S hS a)
(haSep : HasProperty B S hS (separatedProperty B S hS) a haRep)
(haLqf : HasProperty B S hS (locallyQuasiFiniteProperty B S hS) a haRep) :
∃ hbRep : IsRepresentableByAlgebraicSpaces B S hS b,
yoneda.relativelyRepresentable b ∧
HasProperty B S hS (separatedProperty B S hS) b hbRep ∧
HasProperty B S hS (locallyQuasiFiniteProperty B S hS) b hbRep
Tag 046K, a lemma
Tag 046K in the Stacks Project.
AlgebraicGeometry.Space.relativelyRepresentable_diag_of_flat_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Diagonal.lean, line 441.
Stacks 046K. Let
Fbe a sheaf on the big fppf site of a schemeSwhich admits a morphismf : X ⟶ Ffrom an algebraic space overSthat is representable by algebraic spaces, surjective, flat and locally of finite presentation. Then the absolute diagonalΔ_F : F ⟶ F × Fis representable by objects of the site, that is, every fibre product ofΔ_Fwith a scheme-valued point ofF × Fis again a scheme overS— not merely an algebraic space, as Stacks 03Y2 would give.Let
d = Δ_Fand letk = f × f : X ⨯ X ⟶ F × F, which is representable by algebraic spaces, surjective, flat and locally of finite presentation by Stacks 046D and Stacks 046H. The fibre productW = (X ⨯ X) ×_{F × F} Fis the kernel pairX ×_F Xoff, so its projection toX ⨯ Xis representable by algebraic spaces, separated and locally quasi-finite. Given a scheme-valued pointη : h_T ⟶ F × F, the base changeT' = h_T ×_{F × F} (X ⨯ X) ⟶ h_Tofkinherits the three properties by Stacks 046F, andT' ×_{X ⨯ X} W ⟶ T'inherits separatedness and local quasi-finiteness from the projection ofW; that fibre product is at the same time the base change ofZ = h_T ×_{F × F} F ⟶ h_TalongT' ⟶ h_T. Stacks 046J applied to the resulting cartesian square makesZ ⟶ h_Trepresentable by objects of the site, andZis the fibre product ofΔ_Fwithη.
theorem relativelyRepresentable_diag_of_flat_presentation
{F X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
(hX : IsAlgebraicSpace B S hS X) (f : X ⟶ F)
(hf : IsRepresentableByAlgebraicSpaces B S hS f)
(hfSurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) f hf)
(hfFlat : HasProperty B S hS (flatProperty B S hS) f hf)
(hfLfp : HasProperty B S hS (locallyOfFinitePresentationProperty B S hS) f hf) :
yoneda.relativelyRepresentable (diag F)
Tag 0AHV, a lemma
Tag 0AHV in the Stacks Project.
AlgebraicGeometry.Space.relativelyRepresentable_of_isLocallyQuasiFinite_of_schemeSource, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/LocallyQuasiFiniteFromScheme.lean, line 93.
Stacks 0AHV. Let
Fbe a presheaf of sets on the big fppf site ofSand letXbe a scheme overS, that is an object of the site. A morphisma : h_X ⟶ Fwhich is representable by algebraic spaces and locally quasi-finite is representable by schemes.The hypothesis of local quasi-finiteness is the one of Stacks 03XZ: every base change of
aalong a scheme-valued point ofFis a locally quasi-finite morphism of algebraic spaces overS.
theorem relativelyRepresentable_of_isLocallyQuasiFinite_of_schemeSource
(B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
(X : BigFppfOver B S hS) (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
(a : yoneda.obj X ⟶ F)
(ha : IsRepresentableByAlgebraicSpaces B S hS a)
(hlqf : HasProperty B S hS
(fun ⦃_ _⦄ φ => IsLocallyQuasiFinite B S hS φ.hom) a ha) :
yoneda.relativelyRepresentable a
Sources
Section80.6 Bootstrap#
Section 80.6 of the Stacks Project, Tag 03XV. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 03Y3, a theorem
Tag 03Y3 in the Stacks Project.
AlgebraicGeometry.Space.isAlgebraicSpace_of_isRepresentableByAlgebraicSpaces_surjective_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BootstrapEtaleSurjective.lean, line 252. The attribute's comment: “conditions (a) and (b)”.
Stacks 03Y3, conditions (a) and (b). Let
Fbe an fppf sheaf on the big fppf site of a schemeSadmitting a morphismf : X ⟶ Ffrom an algebraic space overSwhich is representable by algebraic spaces, surjective and étale. ThenFis an algebraic space overS.The chart of
Fis the composite of a chart ofXwithf, which is representable by algebraic spaces by Stacks 03Y1 and therefore by objects of the site; the diagonal is the only clause of Stacks 025Y needing effective fppf descent, which is supplied byisEffectiveDescentAlongCoveringSieve_monomorphisms_inf_lft.
theorem isAlgebraicSpace_of_isRepresentableByAlgebraicSpaces_surjective_etale
{F X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
(hX : IsAlgebraicSpace B S hS X) (f : X ⟶ F)
(hf : IsRepresentableByAlgebraicSpaces B S hS f)
(hfSurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) f hf)
(hfEtale : HasProperty B S hS (etaleMorphisms B S hS) f hf) :
IsAlgebraicSpace B S hS F
AlgebraicGeometry.Space.isAlgebraicSpace_of_isRepresentableByAlgebraicSpaces_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BootstrapEtaleSurjective.lean, line 356. The attribute's comment: “conditions (1), (2) and (3)”.
Stacks 03Y3, conditions (1), (2) and (3). Let
Fbe an fppf sheaf on the big fppf site of a schemeSwhose diagonal is representable by algebraic spaces and which admits a surjective étale morphism from an algebraic space overS. ThenFis an algebraic space overS.Condition (2) makes the morphism of condition (3) representable by algebraic spaces by Stacks 03Y2, so the hypotheses (a) and (b) hold and the previous theorem applies.
theorem isAlgebraicSpace_of_isRepresentableByAlgebraicSpaces_diag
{F X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
(hdiag : IsRepresentableByAlgebraicSpaces B S hS (diag F))
(hX : IsAlgebraicSpace B S hS X) (f : X ⟶ F)
(hfSurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) f
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS hdiag hX f))
(hfEtale : HasProperty B S hS (etaleMorphisms B S hS) f
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS hdiag hX f)) :
IsAlgebraicSpace B S hS F
Sources
Section80.7 Finding opens#
Section 80.7 of the Stacks Project, Tag 04S2. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 046M, a lemma
Tag 046M in the Stacks Project.
AlgebraicGeometry.GroupoidScheme.isOpenImmersion_restrictionQuotientMap_of_open_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/OpenSaturation.lean, line 386.
Stacks 046M. Let
Gbe a groupoid scheme overSand letg : U' ⟶ Ube a morphism to its scheme of objects whose saturation is the range of an open immersioni : W ⟶ U. If the reach map factors ask ≫ iwithkinducing a surjection of fppf sheaves, then the map of quotient sheavesU'/R' ⟶ U/Rinduced by the restriction ofGalonggis a representable open immersion.
theorem isOpenImmersion_restrictionQuotientMap_of_open_image
(B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
[HasSheafify (BigFppfOver.topology B S hS) (Type u)]
(G : GroupoidScheme S) {U' W : Over S}
(g : U' ⟶ G.objects) (i : W ⟶ G.objects)
[IsOpenImmersion i.left]
(k : pullback g G.target ⟶ W)
(hk : k ≫ i = restrictionReachMap G g)
(himage : Set.range i.left.base =
Set.range (restrictionReachMap G g).left.base)
(hsurj : Sheaf.IsLocallySurjective
((presheafToSheaf (BigFppfOver.topology B S hS) (Type u)).map
((Over.post B.inclusion).op.whiskerLeft (yoneda.map k)))) :
Space.IsOpenImmersion B S hS
(restrictionQuotientMap (BigFppfOver.topology B S hS) (Over.post B.inclusion) G g
(restrict G g)).1
Sources
Section80.8 Slicing equivalence relations#
Section 80.8 of the Stacks Project, Tag 046L. 1 tag here is carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0489, a lemma
Tag 0489 in the Stacks Project.
Stacks.Groupoids.GroupoidScheme.exists_restriction_locallyQuasiFinite_isIso_quotientMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/EquivalenceRelationQuasiFiniteRefinement.lean, line 225. The attribute's comment: “the refinement with locally quasi-finite source and target and the same quotient sheaf, given the refinement data as QuasiFiniteRefinement. The tag itself, with nothing carried, is AlgebraicGeometry.exists_locallyQuasiFinite_groupoid_quotientSheaf_iso of StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/CohenMacaulayQuotientUnchanged.lean, which builds that data from the Cohen-Macaulay restriction and the reach map”.
Stacks Project, Tag 0489, conditional on Steps 1 to 3 of its proof.
Let
Rbe a groupoid scheme overSwhose target and source are an equivalence relation. Given a refinement in the sense ofStacks.Groupoids.GroupoidScheme.QuasiFiniteRefinement— a morphismg : U' ⟶ Uwhose reach map is flat, locally of finite presentation and locally quasi-finite and is a singleton covering of the site — the restrictionR' = R|_{U'}is again an equivalence relation, its source and target are flat, locally of finite presentation, locally of finite type and locally quasi-finite, and the induced mapU'/R' ⟶ U/Rof quotient sheaves is an isomorphism.The conclusion is stated for every groupoid scheme realizing the restriction, which is stronger than producing one and avoids any appeal to the realization
AlgebraicGeometry.GroupoidScheme.restrictbuilt byClassical.choice. The morphismU' ⟶ UcarryingR'intoRis the one recorded byAlgebraicGeometry.GroupoidScheme.Restriction.hom, so the clause of the tag that the isomorphism of quotient sheaves is induced by a morphismU' ⟶ UmappingR'intoRis part of the statement rather than an afterthought.The flatness and local finite presentation hypotheses which the tag places on
sandtare not assumed; see the module docstring.
theorem exists_restriction_locallyQuasiFinite_isIso_quotientMap
(J : GrothendieckTopology C) [HasSheafify J (Type u)] (F : C ⥤ Over S) (hF : F.Full)
(G : GroupoidScheme S) [IsEquivalenceRelation G.target G.source]
(N : QuasiFiniteRefinement J F G) :
∃ (U' : Over S) (g : U' ⟶ G.objects),
∀ R' : AlgebraicGeometry.GroupoidScheme.Restriction G g,
IsEquivalenceRelation R'.groupoid.target R'.groupoid.source ∧
Flat R'.groupoid.source.left ∧
LocallyOfFinitePresentation R'.groupoid.source.left ∧
LocallyOfFiniteType R'.groupoid.source.left ∧
LocallyQuasiFinite R'.groupoid.source.left ∧
Flat R'.groupoid.target.left ∧
LocallyOfFinitePresentation R'.groupoid.target.left ∧
LocallyOfFiniteType R'.groupoid.target.left ∧
LocallyQuasiFinite R'.groupoid.target.left ∧
IsIso (restrictionQuotientMap J F G g R')
AlgebraicGeometry.GroupoidScheme.exists_locallyQuasiFinite_refinement_isIso_quotientMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/EquivalenceRelationQuasiFiniteRefinementFppf.lean, line 154. The attribute's comment: “unconditionally, with no assumed input: the hypotheses are exactly the tag's, that the source and target of the groupoid scheme are an equivalence relation and are flat and locally of finite presentation. The refined equivalence relation R' is the restriction H' along the second stage g' of the restriction H₁ along the first stage g₁ of the two-stage refinement that exists_cohenMacaulay_and_quasiFinite_refinement produces -- the Cohen-Macaulay open of Stacks 0460, then the disjoint union of the affine slices of Stacks 04N0 over the finite type points -- and the morphism U' ⟶ U of the tag is the composite g, over which the composite of the two restrictions' canonical morphisms carries R' into R. Its source and target are flat, locally of finite presentation, locally of finite type and locally quasi-finite, being base changes of the second stage's reach map by Stacks 04MV; it is an equivalence relation by restriction_isEquivalenceRelation; and U'/R' ⟶ U/R, the composite of the two stages' maps of quotient sheaves, is an isomorphism because each stage's reach map is flat, locally of finite presentation and surjective and therefore locally surjective on the functors of points of the big fppf site by isLocallySurjective_points_map_of_fppf, which Stacks 02VH turns into an isomorphism of quotient sheaves. No covering datum is assumed: on this site a flat, locally finitely presented, surjective morphism of Over S is locally surjective on points whatever the sizes of its source and target, so neither the disjoint union of Step 3 nor the source of either reach map has to be exhibited as an object of the site. The two stages are not collapsed into one morphism whose reach map is a covering, because the reach map of the composite factors through the base change of an immersion and so is not flat; the final conclusion instead gives the isomorphism of quotient sheaves for the restriction along the composite as well, by isIso_restrictionQuotientMap_of_comp_reach”.
Stacks Project, Tag 0489.
Let
(U, R, s, t, c, e, i)be a groupoid scheme overSwhose target and source maps form an equivalence relation and are flat and locally of finite presentation. Then there are a schemeU'overS, a morphismU' ⟶ U, and an equivalence relationR'onU'mapping intoRover it, whose source and target maps are flat, locally of finite presentation, locally of finite type and locally quasi-finite, and for which the induced mapU'/R' ⟶ U/Rof quotient sheaves on the big fppf site overSis an isomorphism.The refinement is produced in the two stages of the source proof:
g₁ : U₁ ⟶ Uis the inclusion of the Cohen-Macaulay open of Stacks 0460,H₁is the restriction ofRalong it,g' : U' ⟶ U₁is the disjoint union of the affine slices of Stacks 04N0 over the finite type points ofU₁, andR'is the restrictionH'ofH₁alongg'. The morphismU' ⟶ Uis the compositeg, and the morphism ofR'intoRis the composite of the two restrictions' canonical morphisms, which lies overgby the second conclusion below.The last conclusion is more than the tag asks: the map of quotient sheaves induced by the restriction of
Ralong the single morphismgis an isomorphism for every groupoid scheme realizing that restriction. Together with the isomorphism forR'it says that the two descriptions of the refined relation — the restriction of the restriction, and the restriction along the composite — have the same quotient; that they are the same relation is Stacks 04MW, which is not used here.The last two conclusions are the size estimates of the two stages, also more than the tag asks: the first stage is an open of
U, and the second is a disjoint union of affine immersions locally of finite presentation indexed by the points of the first, sosize U₁ ≤ size Uandsize U' ≤ 2 ^ size U. They are not used for the isomorphism of quotient sheaves — that needs no cardinality hypothesis at all, see the implementation notes — but they are what a later consumer needs in order to exhibitU'and the arrow scheme ofR'as objects of the site, which the engine of Stacks 02WW requires and which the existential form of this statement would otherwise destroy.
theorem exists_locallyQuasiFinite_refinement_isIso_quotientMap
(B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
(G : GroupoidScheme S) [IsEquivalenceRelation G.target G.source]
[Flat G.source.left] [Flat G.target.left]
[LocallyOfFinitePresentation G.source.left] [LocallyOfFinitePresentation G.target.left] :
letI := BigFppfOver.hasSheafify_type B S hS
∃ (U₁ : Over S) (g₁ : U₁ ⟶ G.objects) (H₁ : Restriction G g₁) (U' : Over S)
(g' : U' ⟶ H₁.groupoid.objects) (H' : Restriction H₁.groupoid g')
(g : U' ⟶ G.objects),
g = g' ≫ H₁.hom.mapObjects ∧
H'.hom.mapObjects ≫ H₁.hom.mapObjects = eqToHom H'.objects_eq ≫ g ∧
IsEquivalenceRelation H'.groupoid.target H'.groupoid.source ∧
Flat H'.groupoid.source.left ∧
LocallyOfFinitePresentation H'.groupoid.source.left ∧
LocallyOfFiniteType H'.groupoid.source.left ∧
LocallyQuasiFinite H'.groupoid.source.left ∧
Flat H'.groupoid.target.left ∧
LocallyOfFinitePresentation H'.groupoid.target.left ∧
LocallyOfFiniteType H'.groupoid.target.left ∧
LocallyQuasiFinite H'.groupoid.target.left ∧
IsIso (restrictionQuotientMap (BigFppfOver.topology B S hS) (Over.post B.inclusion)
H₁.groupoid g' H' ≫
restrictionQuotientMap (BigFppfOver.topology B S hS) (Over.post B.inclusion) G g₁ H₁) ∧
(∀ H : Restriction G g,
IsIso (restrictionQuotientMap (BigFppfOver.topology B S hS)
(Over.post B.inclusion) G g H)) ∧
U₁.left.size ≤ G.objects.left.size ∧
U'.left.size ≤ 2 ^ G.objects.left.size
AlgebraicGeometry.exists_slice_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/EquivalenceRelationQuasiFiniteSlice.lean, line 722.
An equivalence relation on schemes over
Swith flat, locally finitely presented source and target maps admits a slice: an equivalence relation whose source and target maps are flat, locally of finite presentation and locally quasi-finite, together with a morphismgof object schemes and a morphismrof arrow schemes over it, inducing an isomorphism of fppf quotient sheaves.
public theorem exists_slice_locallyQuasiFinite
(B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
[HasSheafify (AlgebraicGeometry.BigFppfOver.topology B S hS) (Type u)]
{R U : AlgebraicGeometry.BigFppfOver B S hS}
(j : Stacks.Groupoids.PreRelation (S := S) ((Over.post B.inclusion).obj R)
((Over.post B.inclusion).obj U))
[IsEquivalenceRelation j.target j.source]
[Flat j.source.left] [LocallyOfFinitePresentation j.source.left]
[Flat j.target.left] [LocallyOfFinitePresentation j.target.left] :
∃ (U' R' : AlgebraicGeometry.BigFppfOver B S hS)
(j' : Stacks.Groupoids.PreRelation (S := S) ((Over.post B.inclusion).obj R')
((Over.post B.inclusion).obj U'))
(g : U' ⟶ U) (r : R' ⟶ R)
(hs : (Over.post B.inclusion).map r ≫ j.source =
j'.source ≫ (Over.post B.inclusion).map g)
(ht : (Over.post B.inclusion).map r ≫ j.target =
j'.target ≫ (Over.post B.inclusion).map g),
IsEquivalenceRelation j'.target j'.source ∧
Flat j'.source.left ∧ LocallyOfFinitePresentation j'.source.left ∧
LocallyQuasiFinite j'.source.left ∧
Flat j'.target.left ∧ LocallyOfFinitePresentation j'.target.left ∧
LocallyQuasiFinite j'.target.left ∧
IsIso (Stacks.Groupoids.quotientSheafMap
(AlgebraicGeometry.BigFppfOver.topology B S hS) (Over.post B.inclusion) j' j
((Over.post B.inclusion).map r) ((Over.post B.inclusion).map g)
hs ht)
Sources
Section80.9 Quotient by a subgroupoid#
Section 80.9 of the Stacks Project, Tag 04S3. 1 tag here is carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04S4, a lemma
Tag 04S4 in the Stacks Project.
AlgebraicGeometry.GroupoidScheme.exists_division_isField_quotient_of_isoSpecField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteFlatQuotient/FieldObjectDivision.lean, line 180. The attribute's comment: “all four conclusions, at an object scheme which is the spectrum of a field and with only finiteness assumed of the source and target of the subgroupoid, together with the quotient being the spectrum of a field”.
Stacks Project, Tag 04S4, at an object scheme which is the spectrum of a field. A subgroupoid on the same object scheme whose pre-relation is a monomorphism and whose source and target maps are finite can be divided out, and the quotient is the spectrum of a field.
Over a field the two finite locally free hypotheses of
AlgebraicGeometry.GroupoidScheme.exists_divisionreduce to finiteness, byAlgebraicGeometry.isFiniteLocallyFree_of_isFinite_of_isoSpecField, and affineness of the object scheme is automatic. The quotient morphism being finite locally free and surjective, its global functions are a field byAlgebraicGeometry.isField_sections_of_isFiniteLocallyFree_of_surjective.
theorem exists_division_isField_quotient_of_isoSpecField {S : Scheme.{u}} (G H : GroupoidScheme S)
(i : GroupoidScheme.Hom H G) (hobj : H.objects = G.objects)
(hiobj : i.mapObjects = eqToHom hobj) (k : Type u) [Field k]
(e : G.objects.left ≅ Spec (.of k))
[Mono i.mapArrows]
[IsFinite H.source.left] [IsFinite H.target.left]
[Mono (prod.lift H.target H.source)]
[IsSeparated (prod.lift G.target G.source).left]
[LocallyOfFiniteType (prod.lift G.target G.source).left]
[LocallyQuasiFinite (prod.lift G.target G.source).left] :
∃ D : Division G H i hobj, IsField Γ(D.quotient.left, ⊤)
AlgebraicGeometry.exists_finiteFlatQuotient_isAffine_of_mono_groupoidPreRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteFlatQuotient/SubgroupoidDivision.lean, line 494. References: SGA 3 V (4.1), “special case”.
Stacks Project, Tag 04S4. Let
(U, R, s, t, c)be a groupoid schemeGoverSand let(U, P, s|_P, t|_P, c|_P)be a groupoid schemeHmapping to it by a morphismiwhich is an isomorphism on objects, such that
s|_P, t|_P : P ⟶ Uare finite locally free,j|_P = (t|_P, s|_P) : P ⟶ U ×_S Uis a monomorphism,Uis affine, andj = (t, s) : R ⟶ U ×_S Uis separated and locally quasi-finite (locally of finite type with finite fibres; the finite type half is a separate class here).Then
U/Pis representable by an affine schemeŪ, the quotient morphismU ⟶ Ūis finite locally free (and surjective), andP = U ×_Ū U; these are the fields ofStacks.Groupoids.FiniteFlatQuotienttogether with affineness of its quotient scheme. MoreoverRis the restriction of a groupoid scheme onŪalong the quotient morphism: there is a groupoid schemeKwith object schemeŪand a morphismG ⟶ Kwhich is the quotient morphism on objects and whose square of arrow schemes over the pairs of objects is cartesian,R = (U ×_S U) ×_{Ū ×_S Ū} R̄; equivalently, it is fully faithful on the generalized points of every test scheme.The source asks in addition that
P ⟶ Rbe a monomorphism; this follows from the other hypotheses (j ∘ i = (i × i) ∘ j|_Pis a monomorphism) and is not used.
theorem exists_finiteFlatQuotient_isAffine_of_mono_groupoidPreRelation (G H : GroupoidScheme S)
(i : GroupoidScheme.Hom H G) [IsIso i.mapObjects]
[IsFiniteLocallyFree H.source.left] [IsFiniteLocallyFree H.target.left]
[Mono (groupoidPreRelation H)] [IsAffine G.objects.left]
[IsSeparated (groupoidPreRelation G).left] [LocallyQuasiFinite (groupoidPreRelation G).left]
[LocallyOfFiniteType (groupoidPreRelation G).left] :
∃ Q : FiniteFlatQuotient H, IsAffine Q.space.left ∧
∃ (K : GroupoidScheme S) (he : K.objects = Q.space) (F : GroupoidScheme.Hom G K),
F.mapObjects = (inv i.mapObjects ≫ Q.quotientMap) ≫ eqToHom he.symm ∧
IsPullback F.mapArrows (groupoidPreRelation G) (groupoidPreRelation K)
(prod.map F.mapObjects F.mapObjects) ∧
∀ T : Over S, Nonempty (F.evaluation T).FullyFaithful
AlgebraicGeometry.GroupoidScheme.exists_division, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteFlatQuotient/SubgroupoidDivisionDescent.lean, line 1075. The attribute's comment: “all four conclusions: the affine quotient Ū = U/P as the fppf-sheaf coequalizer, its finite locally free surjective quotient map, the kernel-pair square P = U ×_Ū U, and the descent of the ambient groupoid R to a groupoid on Ū of which it is the restriction”.
A finite locally free subgroupoid equivalence relation on an affine scheme can be divided out, and a separated locally quasi-finite ambient groupoid descends to the quotient.
theorem exists_division {S : Scheme.{u}} (G H : GroupoidScheme S)
(i : GroupoidScheme.Hom H G) (hobj : H.objects = G.objects)
(hiobj : i.mapObjects = eqToHom hobj)
[Mono i.mapArrows]
[Stacks.Morphisms.IsFiniteLocallyFree H.source.left]
[Stacks.Morphisms.IsFiniteLocallyFree H.target.left]
[Mono (prod.lift H.target H.source)]
[IsAffine G.objects.left]
[IsSeparated (prod.lift G.target G.source).left]
[LocallyOfFiniteType (prod.lift G.target G.source).left]
[LocallyQuasiFinite (prod.lift G.target G.source).left] :
Nonempty (Division G H i hobj)
Sources
Section80.10 Final bootstrap#
Section 80.10 of the Stacks Project, Tag 04S5. 1 tag here is carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04S6, a theorem
Tag 04S6 in the Stacks Project.
AlgebraicGeometry.Space.isAlgebraicSpace_of_diag_of_flat_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FinalBootstrap.lean, line 90. The attribute's comment: “condition (5)”.
Stacks 04S6, condition (5). Let
Fbe a sheaf on the big fppf site of a schemeSwhose absolute diagonal is representable by algebraic spaces, and suppose there is an algebraic spaceXoverSand a morphismf : X ⟶ Fwhich is surjective, flat and locally of finite presentation. ThenFis an algebraic space overS.The chart
fis not assumed to be representable by algebraic spaces; it is so automatically, byAlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_diagonal, which is what turns the data of condition (5) into the data of condition (3).
theorem isAlgebraicSpace_of_diag_of_flat_chart
{F X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
(hdiag : IsRepresentableByAlgebraicSpaces B S hS (diag F))
(hX : IsAlgebraicSpace B S hS X) (f : X ⟶ F)
(hSurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) f
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS hdiag hX f))
(hFlat : HasProperty B S hS (flatProperty B S hS) f
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS hdiag hX f))
(hLfp : HasProperty B S hS (locallyOfFinitePresentationProperty B S hS) f
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS hdiag hX f)) :
IsAlgebraicSpace B S hS F
AlgebraicGeometry.Space.isAlgebraicSpace_of_relativelyRepresentable_diag_of_flat_scheme_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FinalBootstrap.lean, line 115. The attribute's comment: “condition (6)”.
Stacks 04S6, condition (6). Let
Fbe a sheaf on the big fppf site of a schemeSwhose absolute diagonal is representable, and suppose there is a schemeUoverSand a morphismf : h_U ⟶ Fwhich is surjective, flat and locally of finite presentation. ThenFis an algebraic space overS.This is condition (5) for the algebraic space
h_U: a representable diagonal is representable by algebraic spaces byAlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces.of_relativelyRepresentable, and a representable presheaf is an algebraic space by Stacks 025Z.
theorem isAlgebraicSpace_of_relativelyRepresentable_diag_of_flat_scheme_chart
{F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
(hdiag : yoneda.relativelyRepresentable (diag F))
(U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ F)
(hSurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) f
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS
(IsRepresentableByAlgebraicSpaces.of_relativelyRepresentable hdiag)
(isAlgebraicSpace_yoneda B S hS U) f))
(hFlat : HasProperty B S hS (flatProperty B S hS) f
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS
(IsRepresentableByAlgebraicSpaces.of_relativelyRepresentable hdiag)
(isAlgebraicSpace_yoneda B S hS U) f))
(hLfp : HasProperty B S hS (locallyOfFinitePresentationProperty B S hS) f
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS
(IsRepresentableByAlgebraicSpaces.of_relativelyRepresentable hdiag)
(isAlgebraicSpace_yoneda B S hS U) f)) :
IsAlgebraicSpace B S hS F
AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_quotient_groupoidInAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FinalBootstrapTheorem.lean, line 1154. The attribute's comment: “part (1)”.
Condition (1): the quotient of a flat, locally finitely presented equivalence-relation groupoid in algebraic spaces is an algebraic space.
public theorem isAlgebraicSpace_quotient_groupoidInAlgebraicSpaces
(site : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : site.Contains S)
[HasSheafify (AlgebraicGeometry.BigFppfOver.topology site S hS) (Type u)]
{base : AlgebraicGeometry.AlgebraicSpaces site S hS}
(G : AlgebraicGeometry.GroupoidInAlgebraicSpaces site S hS base)
(hrel : CategoryTheory.IsEquivalenceRelation
(AlgebraicGeometry.Space.groupoidPreRelation G).target
(AlgebraicGeometry.Space.groupoidPreRelation G).source)
(hsflat : AlgebraicGeometry.Space.IsFlat site S hS G.source.hom)
(htflat : AlgebraicGeometry.Space.IsFlat site S hS G.target.hom)
(hslfp : AlgebraicGeometry.Space.IsLocallyOfFinitePresentation site S hS G.source.hom)
(htlfp : AlgebraicGeometry.Space.IsLocallyOfFinitePresentation site S hS G.target.hom) :
AlgebraicGeometry.IsAlgebraicSpace site S hS
(AlgebraicGeometry.Space.quotientSheaf
(AlgebraicGeometry.Space.groupoidPreRelation G)).obj
AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representable_hasProperty_surjective_flat_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FinalBootstrapTheorem.lean, line 1413. The attribute's comment: “part (3), surjectivity on base changes”.
Condition (3) with surjectivity read, like flatness and local finite presentation, on every scheme-valued base change of
f.It implies
isAlgebraicSpace_of_representable_surjective_flat_locallyOfFinitePresentation, since a surjection of presheaves representable by algebraic spaces is surjective on every base change.
public theorem
isAlgebraicSpace_of_representable_hasProperty_surjective_flat_locallyOfFinitePresentation
(site : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : site.Contains S)
(F : (AlgebraicGeometry.BigFppfOver site S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology site S hS) F)
{X : (AlgebraicGeometry.BigFppfOver site S hS)ᵒᵖ ⥤ Type u}
(hX : AlgebraicGeometry.IsAlgebraicSpace site S hS X)
(f : X ⟶ F)
(hrep : AlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces site S hS f)
(hsurj : AlgebraicGeometry.Space.HasProperty site S hS
(fun ⦃_ _⦄ φ => AlgebraicGeometry.Space.IsSurjective site S hS φ.hom) f hrep)
(hflat : AlgebraicGeometry.Space.HasProperty site S hS
(fun ⦃_ _⦄ φ => AlgebraicGeometry.Space.IsFlat site S hS φ.hom) f hrep)
(hlfp : AlgebraicGeometry.Space.HasProperty site S hS
(fun ⦃_ _⦄ φ => AlgebraicGeometry.Space.IsLocallyOfFinitePresentation site S hS φ.hom)
f hrep) :
AlgebraicGeometry.IsAlgebraicSpace site S hS F
AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representable_surjective_flat_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FinalBootstrapTheorem.lean, line 1453. The attribute's comment: “part (3)”.
Condition (3): a representable, surjective, flat, locally finitely presented map from an algebraic space presents an algebraic space.
public theorem isAlgebraicSpace_of_representable_surjective_flat_locallyOfFinitePresentation
(site : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : site.Contains S)
(F : (AlgebraicGeometry.BigFppfOver site S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology site S hS) F)
{X : (AlgebraicGeometry.BigFppfOver site S hS)ᵒᵖ ⥤ Type u}
(hX : AlgebraicGeometry.IsAlgebraicSpace site S hS X)
(f : X ⟶ F)
(hrep : AlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces site S hS f)
(hsurj : AlgebraicGeometry.Space.IsSurjective site S hS f)
(hflat : AlgebraicGeometry.Space.HasProperty site S hS
(fun ⦃_ _⦄ φ => AlgebraicGeometry.Space.IsFlat site S hS φ.hom) f hrep)
(hlfp : AlgebraicGeometry.Space.HasProperty site S hS
(fun ⦃_ _⦄ φ => AlgebraicGeometry.Space.IsLocallyOfFinitePresentation site S hS φ.hom)
f hrep) :
AlgebraicGeometry.IsAlgebraicSpace site S hS F
AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representable_hasProperty_surjective_flat_locallyOfFinitePresentation_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FinalBootstrapTheorem.lean, line 1476. The attribute's comment: “part (4), surjectivity on base changes”.
Condition (4) with surjectivity read on every scheme-valued base change of
f:isAlgebraicSpace_of_representable_hasProperty_surjective_flat_locallyOfFinitePresentationwith a scheme as the source.
public theorem
isAlgebraicSpace_of_representable_hasProperty_surjective_flat_locallyOfFinitePresentation_scheme
(site : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : site.Contains S)
(F : (AlgebraicGeometry.BigFppfOver site S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology site S hS) F)
(U : AlgebraicGeometry.BigFppfOver site S hS)
(f : yoneda.obj U ⟶ F)
(hrep : AlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces site S hS f)
(hsurj : AlgebraicGeometry.Space.HasProperty site S hS
(fun ⦃_ _⦄ φ => AlgebraicGeometry.Space.IsSurjective site S hS φ.hom) f hrep)
(hflat : AlgebraicGeometry.Space.HasProperty site S hS
(fun ⦃_ _⦄ φ => AlgebraicGeometry.Space.IsFlat site S hS φ.hom) f hrep)
(hlfp : AlgebraicGeometry.Space.HasProperty site S hS
(fun ⦃_ _⦄ φ => AlgebraicGeometry.Space.IsLocallyOfFinitePresentation site S hS φ.hom)
f hrep) :
AlgebraicGeometry.IsAlgebraicSpace site S hS F
AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representable_surjective_flat_locallyOfFinitePresentation_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FinalBootstrapTheorem.lean, line 1498. The attribute's comment: “part (4)”.
Condition (4): the preceding criterion with a scheme as the source.
public theorem isAlgebraicSpace_of_representable_surjective_flat_locallyOfFinitePresentation_scheme
(site : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : site.Contains S)
(F : (AlgebraicGeometry.BigFppfOver site S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology site S hS) F)
(U : AlgebraicGeometry.BigFppfOver site S hS)
(f : yoneda.obj U ⟶ F)
(hrep : AlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces site S hS f)
(hsurj : AlgebraicGeometry.Space.IsSurjective site S hS f)
(hflat : AlgebraicGeometry.Space.HasProperty site S hS
(fun ⦃_ _⦄ φ => AlgebraicGeometry.Space.IsFlat site S hS φ.hom) f hrep)
(hlfp : AlgebraicGeometry.Space.HasProperty site S hS
(fun ⦃_ _⦄ φ => AlgebraicGeometry.Space.IsLocallyOfFinitePresentation site S hS φ.hom)
f hrep) :
AlgebraicGeometry.IsAlgebraicSpace site S hS F
AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representableDiagonal_surjective_flat_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FinalBootstrapTheorem.lean, line 1520. The attribute's comment: “part (5)”.
Condition (5): a sheaf with diagonal representable by algebraic spaces and a surjective flat locally finitely presented algebraic-space presentation is an algebraic space.
public theorem isAlgebraicSpace_of_representableDiagonal_surjective_flat_locallyOfFinitePresentation
(site : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : site.Contains S)
(F : (AlgebraicGeometry.BigFppfOver site S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology site S hS) F)
(hdiag : AlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces site S hS (diag F))
{X : (AlgebraicGeometry.BigFppfOver site S hS)ᵒᵖ ⥤ Type u}
(hX : AlgebraicGeometry.IsAlgebraicSpace site S hS X)
(f : X ⟶ F)
(hsurj : AlgebraicGeometry.Space.IsSurjective site S hS f)
(hflat : ∀ (T : AlgebraicGeometry.BigFppfOver site S hS)
(ξ : yoneda.obj T ⟶ F),
AlgebraicGeometry.Space.IsFlat site S hS (pullback.fst ξ f))
(hlfp : ∀ (T : AlgebraicGeometry.BigFppfOver site S hS)
(ξ : yoneda.obj T ⟶ F),
AlgebraicGeometry.Space.IsLocallyOfFinitePresentation site S hS
(pullback.fst ξ f)) :
AlgebraicGeometry.IsAlgebraicSpace site S hS F
AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representableDiagonal_surjective_flat_locallyOfFinitePresentation_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FinalBootstrapTheorem.lean, line 1550. The attribute's comment: “part (6)”.
Condition (6): a scheme presentation suffices when the diagonal is representable by schemes.
public theorem
isAlgebraicSpace_of_representableDiagonal_surjective_flat_locallyOfFinitePresentation_scheme
(site : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : site.Contains S)
(F : (AlgebraicGeometry.BigFppfOver site S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology site S hS) F)
(hdiag : yoneda.relativelyRepresentable (diag F))
(U : AlgebraicGeometry.BigFppfOver site S hS)
(f : yoneda.obj U ⟶ F)
(hsurj : AlgebraicGeometry.Space.IsSurjective site S hS f)
(hflat : ∀ (T : AlgebraicGeometry.BigFppfOver site S hS)
(ξ : yoneda.obj T ⟶ F),
AlgebraicGeometry.Space.IsFlat site S hS (pullback.fst ξ f))
(hlfp : ∀ (T : AlgebraicGeometry.BigFppfOver site S hS)
(ξ : yoneda.obj T ⟶ F),
AlgebraicGeometry.Space.IsLocallyOfFinitePresentation site S hS
(pullback.fst ξ f)) :
AlgebraicGeometry.IsAlgebraicSpace site S hS F
AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_quotientSheaf_groupoidScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FlatRelationQuotient.lean, line 3609. The attribute's comment: “condition (2): the quotient of a scheme by a flat, locally finitely presented equivalence relation groupoid scheme is an algebraic space”.
Stacks 04S6, condition (2). Let
(U, R, s, t, c)be a groupoid scheme overSwhose object scheme belongs to the big fppf site, such thats, tare flat and locally of finite presentation andj = (t, s) : R ⟶ U ×_S Uis an equivalence relation. Then the fppf quotient sheafU/Ris an algebraic space.
theorem isAlgebraicSpace_quotientSheaf_groupoidScheme
(site : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : site.Contains S)
[HasSheafify (AlgebraicGeometry.BigFppfOver.topology site S hS) (Type u)]
(G : Stacks.Groupoids.GroupoidScheme S) (hU : site.Contains G.objects.left)
[IsEquivalenceRelation G.target G.source]
[Flat G.source.left] [Flat G.target.left]
[LocallyOfFinitePresentation G.source.left]
[LocallyOfFinitePresentation G.target.left] :
AlgebraicGeometry.IsAlgebraicSpace site S hS
(Stacks.Groupoids.quotientSheaf (AlgebraicGeometry.BigFppfOver.topology site S hS)
(Over.post site.inclusion) (AlgebraicGeometry.groupoidPreRelation G)).obj
AlgebraicGeometry.Space.bootstrap04S6QuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FlatRelationQuotient.lean, line 3736. The attribute's comment: “condition (1): the quotient of an algebraic space by a flat, locally finitely presented equivalence relation of algebraic spaces is an algebraic space”.
Stacks 04S6, condition (1). Let
j : R ⟶ U ×_Z Ube an equivalence relation of algebraic spaces over a presheafZon the big fppf site ofS, whose target and sourcet, s : R ⟶ Uare flat and locally of finite presentation. Then the fppf quotient sheafU/Ris an algebraic space.The proof is the source's:
Uis replaced by an étale atlash_{U₀} ⟶ U(Groupoids in Spaces, Lemma 046P,AlgebraicGeometry.Space.isIso_restrictQuotientSheafMap_chartInSliceMap); the restricted relationR₀ = U₀ ×_U R ×_U U₀is then an algebraic space with a monomorphism, locally of finite type, toU₀ ×_S U₀, hence representable by Morphisms of Spaces, Proposition 03XX; and the resulting relation of schemes in the site is condition (2),AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_quotientSheaf_of_flat_preRelation.
theorem bootstrap04S6QuotientSheaf (site : BigFppfSite.{u}) (S : Scheme.{u})
(hS : site.Contains S) : Bootstrap04S6QuotientSheaf site S hS
AlgebraicGeometry.Space.isBootstrapAlgebraicSpaceAlongFlatSurjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Unconditional.lean, line 51. The attribute's comment: “condition (3): a sheaf with a surjective, flat, locally finitely presented chart from an algebraic space, representable by algebraic spaces, is an algebraic space”.
Let
Fbe a sheaf on the big fppf site ofS, and suppose there are an algebraic spaceXoverSand a morphismX ⟶ Fwhich is representable by algebraic spaces, surjective, flat and locally of finite presentation. ThenFis an algebraic space overS.
theorem isBootstrapAlgebraicSpaceAlongFlatSurjection :
IsBootstrapAlgebraicSpaceAlongFlatSurjection B S hS
AlgebraicGeometry.Space.isAlgebraicSpace_of_flat_scheme_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/Unconditional.lean, line 61. The attribute's comment: “condition (4)”.
Let
Fbe a sheaf on the big fppf site ofS, and suppose there are a schemeUof the site and a morphismh_U ⟶ Fwhich is representable by algebraic spaces (in particular, one representable by schemes), surjective, flat and locally of finite presentation. ThenFis an algebraic space overS.
theorem isAlgebraicSpace_of_flat_scheme_chart
{F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
(U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ F)
(hf : IsRepresentableByAlgebraicSpaces B S hS f)
(hSurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) f hf)
(hFlat : HasProperty B S hS (flatProperty B S hS) f hf)
(hLfp : HasProperty B S hS (locallyOfFinitePresentationProperty B S hS) f hf) :
IsAlgebraicSpace B S hS F
Sources
Section80.11 Applications#
Section 80.11 of the Stacks Project, Tag 04SJ. 8 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04SK, a lemma
Tag 04SK in the Stacks Project.
AlgebraicGeometry.isAlgebraicSpace_of_isCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringRestrictionCoproduct.lean, line 777.
Stacks 04SK.
Let
Fbe a presheaf of sets on the big fppf site ofSand let{S i → S}be a covering family of the base. Assume
Fis a sheaf (hF);- each restriction
F_i = h_{S i} × Fis an algebraic space (hFi);- the coproduct
∐ F_iis an algebraic space:G, presented by the colimit cofanhcoprodwith legsι, is a coproduct of theF_iin sheaves, and it is an algebraic space (hG).Then
Fis an algebraic space.The coproduct in (3) is given as data because the index type of the covering is of the next universe, so a coproduct of the
F_ineed not exist in sheaves ofType u; any two coproducts are isomorphic, so this is the source's hypothesis.The source's proof applies Stacks 04S6 to
∐ F_i ⟶ F, the base change of∐ S_i ⟶ S. Inside the site this chart is built from a refinement of the covering of size bounded byS, which isAlgebraicGeometry.isAlgebraicSpace_of_isCovering_of_atlas_size_le; what that lemma asks for is a bounded étale atlas of the restriction of eachF_ito an affine openWofS_i, and hypothesis (3) is exactly what supplies it. An étale atlasUof∐ F_isplits along the coproduct into étale atlasesU_iof theF_i, which are open inU(AlgebraicGeometry.Sheaf.exists_clopen_decomposition_of_isColimit_cofan). The restriction ofF_itoWis the base change ofF_ialongW ⟶ S_i, soW ×_{S_i} U_iis an étale atlas of it, of size at mostmax (size S) (size U).The last step is Stacks 04S6, condition (3), for a chart representable by objects of the site: a sheaf which receives a representable, surjective, flat, locally finitely presented morphism from an algebraic space is an algebraic space.
theorem isAlgebraicSpace_of_isCovering
{F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
(E : PreZeroHypercover.{u + 1} (Over.mk (𝟙 (B.obj hS))))
(hE : BigFppfOver.IsCovering B S hS ⟨Over.mk (𝟙 (B.obj hS)), E⟩)
(hFi : ∀ i : E.I₀, IsAlgebraicSpace B S hS (yoneda.obj (E.X i) ⨯ F))
{G : Sheaf (BigFppfOver.topology B S hS) (Type u)}
(ι : ∀ i : E.I₀, (⟨yoneda.obj (E.X i) ⨯ F, (hFi i).isSheaf⟩ :
Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ G)
(hcoprod : IsColimit (Cofan.mk G ι))
(hG : IsAlgebraicSpace B S hS G.obj) :
IsAlgebraicSpace B S hS F
Tag 04U0, a lemma
Tag 04U0 in the Stacks Project.
AlgebraicGeometry.isAlgebraicSpace_of_isCovering_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringRestrictionFiniteType.lean, line 134.
Let
Fbe a presheaf of sets on the big fppf site ofSand let{S i → S}be a covering family of the base, and assume
Fis a sheaf (hF);- each restriction
h_{S i} × Fis an algebraic space (hFi);- each restriction is of finite type over its member (
hft).Then
Fis an algebraic space.The refinement of the covering by affines over the points of
S, Stacks 02WQ and the final appeal to Stacks 04S6 areAlgebraicGeometry.isAlgebraicSpace_of_isCovering_of_atlas_size_le. What this proof adds is the bounded atlas it asks for: the restriction ofh_{S i} × Fto an affine openWofS iis of finite type overW, hence quasi-compact, hence has an affine étale atlas (Stacks 03H6), which is locally of finite type overSand so of size at mostsize (S)(Stacks 04T7).
theorem isAlgebraicSpace_of_isCovering_of_isFiniteType
{F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
(E : PreZeroHypercover.{u + 1} (Over.mk (𝟙 (B.obj hS))))
(hE : BigFppfOver.IsCovering B S hS ⟨Over.mk (𝟙 (B.obj hS)), E⟩)
(hFi : ∀ i : E.I₀, IsAlgebraicSpace B S hS (yoneda.obj (E.X i) ⨯ F))
(hft : ∀ i : E.I₀, Space.IsFiniteType B S hS
(prod.fst : yoneda.obj (E.X i) ⨯ F ⟶ yoneda.obj (E.X i))) :
IsAlgebraicSpace B S hS F
Tag 0ADV, a lemma
Tag 0ADV in the Stacks Project.
AlgebraicGeometry.Space.Descent.DescentData.isEffective_of_countable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/EffectiveCountableCovering.lean, line 207. The attribute's comment: “part (1): countable index set”.
Stacks 0ADV, part (1). Let
{f i : X i ⟶ T}be an fppf covering of algebraic spaces overSwhose index type is countable. Then every descent datum for algebraic spaces relative to it is effective.
theorem isEffective_of_countable (hcov : IsFppfCovering B S hS X f) : D.IsEffective
AlgebraicGeometry.Space.Descent.DescentData.isEffective_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/EffectiveFiniteTypeCovering.lean, line 325. The attribute's comment: “part (2): finite type, index set of any size”.
Stacks 0ADV, part (2). Let
{f i : X i ⟶ T}be an fppf covering of algebraic spaces overS, indexed by a type of any size. Then every descent datum(Y i, φ i j)relative to it with eachY i ⟶ X iof finite type is effective.The proof is the source's. The sheaf
Fof Stacks 0ADT the datum descends to hasX i ×_T F = Y i. Refine the covering by an fppf covering{R k ⟶ T}by affine objects of the site, with the index type and the sizes of the members bounded by the sizeμof an atlas ofT(AlgebraicGeometry.Space.exists_affine_refinement_of_isFppfCovering, which uses Stacks 042T). IfR k ⟶ Tfactors throughX i, thenR k ×_T F = R k ×_{X i} Y iis of finite type over the affineR k. So it has an atlas of size at mostsize (R k) ≤ μby Stacks 04T7 (AlgebraicGeometry.Space.exists_atlas_size_le_of_isFiniteType). This is the size bound the source draws from Stacks 04U0. Stacks 02WQ then makes the coproducts∐ R kand∐ (R k ×_T F)algebraic spaces, and Stacks 04S6 makesFan algebraic space.
theorem isEffective_of_isFiniteType (hcov : IsFppfCovering B S hS X f)
(hft : ∀ i, IsFiniteType B S hS (D.obj i).hom) : D.IsEffective
Tag 0AMP, a lemma
Tag 0AMP in the Stacks Project.
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_comp_of_flat_surjective_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/FinalBootstrap.lean, line 153.
Stacks 0AMP. Let
a : F ⟶ Gandb : G ⟶ Hbe morphisms of presheaves on the big fppf site ofS, withGandHsheaves. Ifais representable by algebraic spaces, surjective, flat and locally of finite presentation and the compositea ≫ bis representable by algebraic spaces, thenbis representable by algebraic spaces.At a scheme-valued point
ξofHthe fibre productU ×_H Fis an algebraic space, being a base change ofa ≫ b, andU ×_H Gis a sheaf. The morphismU ×_H F ⟶ U ×_H Gis the base change ofaalongU ×_H G ⟶ G, so Stacks 046F gives it the three properties ofa, and Stacks 04S6 condition (3) makesU ×_H Gan algebraic space; that deduction isAlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_comp_of_flat_surjective, whose bootstrap input is discharged here byAlgebraicGeometry.Space.isBootstrapAlgebraicSpaceAlongFlatSurjection.Sheafness of
Fis assumed in the source and is not needed here: representability ofa ≫ balready makes the base changes ofFthat the argument uses algebraic spaces.
theorem isRepresentableByAlgebraicSpaces_of_comp_of_flat_surjective_unconditional
{F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) (b : G ⟶ H)
(hG : Presheaf.IsSheaf (BigFppfOver.topology B S hS) G)
(hH : Presheaf.IsSheaf (BigFppfOver.topology B S hS) H)
(haRep : IsRepresentableByAlgebraicSpaces B S hS a)
(haSurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) a haRep)
(haFlat : HasProperty B S hS (flatProperty B S hS) a haRep)
(haLfp : HasProperty B S hS (locallyOfFinitePresentationProperty B S hS) a haRep)
(hcomp : IsRepresentableByAlgebraicSpaces B S hS (a ≫ b)) :
IsRepresentableByAlgebraicSpaces B S hS b
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_comp_of_flat_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Bootstrap/SeparatedQuasiFiniteDescent.lean, line 563. The attribute's comment: “granted Stacks 04S6 part (3), carried as the hypothesis hbootstrap”.
Stacks 0AMP from the bootstrap theorem Stacks 04S6 part (3).
For morphisms of presheaves
a : F ⟶ Gandb : G ⟶ Hon the big fppf site ofSwithGandHsheaves, ifais representable by algebraic spaces, surjective, flat and locally of finite presentation and the compositea ≫ bis representable by algebraic spaces, thenbis representable by algebraic spaces.At a scheme-valued point
ξofHthe fibre productU ×_H Fis an algebraic space, being a base change ofa ≫ b, andU ×_H Gis a sheaf. The morphismU ×_H F ⟶ U ×_H Gis the base change ofaalongU ×_H G ⟶ G, so Stacks 046F gives it the three properties ofa, and the bootstrap theorem makesU ×_H Gan algebraic space.Sheafness of
Fis assumed in the source and is not needed here: representability ofa ≫ balready makes the base changes ofFthat the argument uses algebraic spaces.This does not register [Stacks, Tag 0AMP] and carries no attribute. Its input
hbootstrapis Stacks 04S6 part (3), which this repository does not prove, andisBootstrapAlgebraicSpaceAlongFlatSurjection_iffbelow shows the two statements are equivalent: the universally quantified form of this theorem is 04S6 part (3). So nothing weaker than 04S6 part (3) can discharge the input, and a declaration assuming an equivalent statement does not formalize the tag. The theorem and its proof are kept, because they are the deduction the source makes; the tag will be registered here once 04S6 part (3) is proved.
theorem isRepresentableByAlgebraicSpaces_of_comp_of_flat_surjective
(hbootstrap : IsBootstrapAlgebraicSpaceAlongFlatSurjection B S hS)
{F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) (b : G ⟶ H)
(hG : Presheaf.IsSheaf (BigFppfOver.topology B S hS) G)
(hH : Presheaf.IsSheaf (BigFppfOver.topology B S hS) H)
(haRep : IsRepresentableByAlgebraicSpaces B S hS a)
(haSurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) a haRep)
(haFlat : HasProperty B S hS (flatProperty B S hS) a haRep)
(haLfp : HasProperty B S hS (locallyOfFinitePresentationProperty B S hS) a haRep)
(hcomp : IsRepresentableByAlgebraicSpaces B S hS (a ≫ b)) :
IsRepresentableByAlgebraicSpaces B S hS b
Tag 04TB, a lemma
Tag 04TB in the Stacks Project.
AlgebraicGeometry.Stack.isAlgebraicSpace_isomPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/IsomorphismSheafAlgebraic.lean, line 1196.
The sheaf
Isom(x, y)of isomorphisms between two objects of the quotient stack of a groupoid in algebraic spaces, read on the big fppf site of the scheme the test object lies over, is an algebraic space over that scheme.Algebraicity is expressed by a pointwise bijection, natural in the test object, with a presheaf of
Type uwhich is an algebraic space: the hom sets of the stackification are not small, soIsom(x, y)itself takes values one universe up.
theorem isAlgebraicSpace_isomPresheaf
(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) :
let I := (Over.iteratedSliceBackward T).op ⋙ (quotientStack G).p.isomPresheaf x y
∃ F : (BigFppfOver C T.left.1 T.left.2)ᵒᵖ ⥤ Type u,
IsAlgebraicSpace C T.left.1 T.left.2 F ∧
∃ e : ∀ U, I.obj U ≃ F.obj U,
∀ ⦃U V⦄ (f : U ⟶ V) (z : I.obj U), e V (I.map f z) = F.map f (e U z)
Tag 06PG, a lemma
Tag 06PG in the Stacks Project.
AlgebraicGeometry.Space.isSurjective_toQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CoveringMap.lean, line 169. The attribute's comment: “surjectivity”.
Stacks 06PG. The object presheaf of a pre-relation surjects onto its quotient sheaf.
A point of the quotient is represented by a section over the spectrum of a field in the site; the quotient map is a surjection of fppf sheaves, so that section lifts to
Uon a covering, and the spectrum of a residue field of a member of the covering is again an object of the site and gives a field-valued point ofUdominating the original one.This also discharges the surjectivity clause of Stacks 06PH, that
X ⟶ X/Gis surjective for a free action of a group algebraic space: the quotientX/Gof [Stacks, Tag 044J] is the quotient sheaf of the pre-relation of the action, so that clause is this lemma at that pre-relation. It is stated here for an arbitrary pre-relation, which is more general and uses neither freeness of the action nor flatness ofG ⟶ B; the remaining clauses of Stacks 06PH — algebraicity ofX/G, flatness and local finite presentation ofX ⟶ X/G, and the fppf torsor property — are not proved here and nothing in this file assumes them.
theorem isSurjective_toQuotientSheaf (j : PreRelation R U) :
IsSurjective site S hS (toQuotientSheaf j)
AlgebraicGeometry.Space.isFlat_toQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CoveringMap.lean, line 459. The attribute's comment: “flatness”.
Stacks 06PG. The object space of a groupoid in algebraic spaces is flat over its sheaf quotient, as soon as that quotient is an algebraic space, the relation cut out by the groupoid is an equivalence relation and the target map of the groupoid is flat.
theorem isFlat_toQuotientSheaf
(hrel : CategoryTheory.IsEquivalenceRelation
(groupoidPreRelation G).target (groupoidPreRelation G).source)
(hF : IsAlgebraicSpace site S hS (quotientSheaf (groupoidPreRelation G)).obj)
(ht : IsFlat site S hS G.target.hom) :
IsFlat site S hS (toQuotientSheaf (groupoidPreRelation G))
AlgebraicGeometry.Space.isLocallyOfFinitePresentation_toQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CoveringMap.lean, line 479. The attribute's comment: “local finite presentation”.
Stacks 06PG. The object space of a groupoid in algebraic spaces is locally of finite presentation over its sheaf quotient, as soon as that quotient is an algebraic space, the relation cut out by the groupoid is an equivalence relation and the target map of the groupoid is locally of finite presentation.
theorem isLocallyOfFinitePresentation_toQuotientSheaf
(hrel : CategoryTheory.IsEquivalenceRelation
(groupoidPreRelation G).target (groupoidPreRelation G).source)
(hF : IsAlgebraicSpace site S hS (quotientSheaf (groupoidPreRelation G)).obj)
(ht : IsLocallyOfFinitePresentation site S hS G.target.hom) :
IsLocallyOfFinitePresentation site S hS (toQuotientSheaf (groupoidPreRelation G))
Tag 06PH, a lemma
Tag 06PH in the Stacks Project.
AlgebraicGeometry.GroupoidInAlgebraicSpaces.isAlgebraicSpace_arrowStabilizerQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/ArrowQuotient.lean, line 367. The attribute's comment: “R/S is an algebraic space”.
Stacks 06PH. The quotient
R/Sof the arrow space by the stabilizer action is an algebraic space, as soon as the stabilizer is flat and locally of finite presentation over the object space.
theorem isAlgebraicSpace_arrowStabilizerQuotient (G : GroupoidInAlgebraicSpaces C S hS B)
(hflat : Space.IsFlat C S hS (stabilizer G).hom)
(hfp : Space.IsLocallyOfFinitePresentation C S hS (stabilizer G).hom) :
IsAlgebraicSpace C S hS (arrowStabilizerQuotient G).obj
AlgebraicGeometry.GroupoidInAlgebraicSpaces.isSurjective_toArrowStabilizerQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/ArrowQuotient.lean, line 377. The attribute's comment: “surjectivity of R ⟶ R/S”.
Stacks 06PH. The quotient map
π : R ⟶ R/Sis surjective.
theorem isSurjective_toArrowStabilizerQuotient (G : GroupoidInAlgebraicSpaces C S hS B) :
Space.IsSurjective C S hS (toArrowStabilizerQuotient G)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.isFlat_toArrowStabilizerQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/ArrowQuotient.lean, line 383. The attribute's comment: “flatness of R ⟶ R/S”.
Stacks 06PH. The quotient map
π : R ⟶ R/Sis flat.
theorem isFlat_toArrowStabilizerQuotient (G : GroupoidInAlgebraicSpaces C S hS B)
(hflat : Space.IsFlat C S hS (stabilizer G).hom)
(hfp : Space.IsLocallyOfFinitePresentation C S hS (stabilizer G).hom) :
Space.IsFlat C S hS (toArrowStabilizerQuotient G)
AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallyOfFinitePresentation_toArrowStabilizerQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Stabilizer/ArrowQuotient.lean, line 393. The attribute's comment: “local finite presentation of R ⟶ R/S”.
Stacks 06PH. The quotient map
π : R ⟶ R/Sis locally of finite presentation.
theorem isLocallyOfFinitePresentation_toArrowStabilizerQuotient
(G : GroupoidInAlgebraicSpaces C S hS B)
(hflat : Space.IsFlat C S hS (stabilizer G).hom)
(hfp : Space.IsLocallyOfFinitePresentation C S hS (stabilizer G).hom) :
Space.IsLocallyOfFinitePresentation C S hS (toArrowStabilizerQuotient G)
AlgebraicGeometry.Space.isSurjective_toQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CoveringMap.lean, line 169. The attribute's comment: “surjectivity of the quotient map, for an arbitrary pre-relation”.
Stacks 06PG. The object presheaf of a pre-relation surjects onto its quotient sheaf.
A point of the quotient is represented by a section over the spectrum of a field in the site; the quotient map is a surjection of fppf sheaves, so that section lifts to
Uon a covering, and the spectrum of a residue field of a member of the covering is again an object of the site and gives a field-valued point ofUdominating the original one.This also discharges the surjectivity clause of Stacks 06PH, that
X ⟶ X/Gis surjective for a free action of a group algebraic space: the quotientX/Gof [Stacks, Tag 044J] is the quotient sheaf of the pre-relation of the action, so that clause is this lemma at that pre-relation. It is stated here for an arbitrary pre-relation, which is more general and uses neither freeness of the action nor flatness ofG ⟶ B; the remaining clauses of Stacks 06PH — algebraicity ofX/G, flatness and local finite presentation ofX ⟶ X/G, and the fppf torsor property — are not proved here and nothing in this file assumes them.
theorem isSurjective_toQuotientSheaf (j : PreRelation R U) :
IsSurjective site S hS (toQuotientSheaf j)
AlgebraicGeometry.Space.isSurjective_toActionQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GroupActionQuotient.lean, line 351. The attribute's comment: “surjectivity of X ⟶ X/G”.
Stacks 06PH. The quotient morphism
X ⟶ X/Gis surjective.This holds for the quotient sheaf of any pre-relation, by Stacks 06PG, so neither freeness nor any property of
G ⟶ Bis needed.
theorem isSurjective_toActionQuotientSheaf (G X : Over B) [GrpObj G] [ModObj G X] :
IsSurjective site S hS (toQuotientSheaf (actionPreRelation G X))
AlgebraicGeometry.Space.isAlgebraicSpace_actionQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GroupActionQuotientAlgebraic.lean, line 81. The attribute's comment: “X/G is an algebraic space”.
Stacks 06PH. The quotient
X/Gof an algebraic space by a free action of a group algebraic space which is flat and locally of finite presentation over the base is an algebraic space.
theorem isAlgebraicSpace_actionQuotientSheaf
(hB : IsAlgebraicSpace site S hS B) (G X : Over B) [GrpObj G] [ModObj G X]
(hG : IsAlgebraicSpace site S hS G.left) (hX : IsAlgebraicSpace site S hS X.left)
(hfree : IsFreeAction site S hS B G X) (hflat : IsFlat site S hS G.hom)
(hfp : IsLocallyOfFinitePresentation site S hS G.hom) :
IsAlgebraicSpace site S hS (actionQuotientSheaf G X).obj
AlgebraicGeometry.Space.isFlat_toActionQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GroupActionQuotientAlgebraic.lean, line 93. The attribute's comment: “flatness of X ⟶ X/G”.
Stacks 06PH. The quotient morphism
X ⟶ X/Gof a free action of a group algebraic space which is flat and locally of finite presentation over the base is flat.
theorem isFlat_toActionQuotientSheaf
(hB : IsAlgebraicSpace site S hS B) (G X : Over B) [GrpObj G] [ModObj G X]
(hG : IsAlgebraicSpace site S hS G.left) (hX : IsAlgebraicSpace site S hS X.left)
(hfree : IsFreeAction site S hS B G X) (hflat : IsFlat site S hS G.hom)
(hfp : IsLocallyOfFinitePresentation site S hS G.hom) :
IsFlat site S hS (toQuotientSheaf (actionPreRelation G X))
AlgebraicGeometry.Space.isLocallyOfFinitePresentation_toActionQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GroupActionQuotientAlgebraic.lean, line 106. The attribute's comment: “local finite presentation of X ⟶ X/G”.
Stacks 06PH. The quotient morphism
X ⟶ X/Gof a free action of a group algebraic space which is flat and locally of finite presentation over the base is locally of finite presentation.
theorem isLocallyOfFinitePresentation_toActionQuotientSheaf
(hB : IsAlgebraicSpace site S hS B) (G X : Over B) [GrpObj G] [ModObj G X]
(hG : IsAlgebraicSpace site S hS G.left) (hX : IsAlgebraicSpace site S hS X.left)
(hfree : IsFreeAction site S hS B G X) (hflat : IsFlat site S hS G.hom)
(hfp : IsLocallyOfFinitePresentation site S hS G.hom) :
IsLocallyOfFinitePresentation site S hS (toQuotientSheaf (actionPreRelation G X))
AlgebraicGeometry.Space.isFppfTorsor_actionQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GroupActionQuotientAlgebraic.lean, line 119. The attribute's comment: “X is an fppf G-torsor over X/G”.
Stacks 06PH. For a free action of a group algebraic space which is flat and locally of finite presentation over the base,
Xis an fppf torsor overX/Gunder the groupGpulled back toX/G.
theorem isFppfTorsor_actionQuotientSheaf
(hB : IsAlgebraicSpace site S hS B) (G X : Over B) [GrpObj G] [ModObj G X]
(hG : IsAlgebraicSpace site S hS G.left) (hX : IsAlgebraicSpace site S hS X.left)
(hfree : IsFreeAction site S hS B G X) (hflat : IsFlat site S hS G.hom)
(hfp : IsLocallyOfFinitePresentation site S hS G.hom) :
IsFppfTorsor site S hS (actionQuotientPresheaf G X)
(isAlgebraicSpace_actionQuotientSheaf hB G X hG hX hfree hflat hfp)
(groupOverQuotient hB.isSheaf G X) (sourceOverQuotient G X)
(isAlgebraicSpace_pullback site S hS G.hom (actionQuotientToBase hB.isSheaf G X) hG
(isAlgebraicSpace_actionQuotientSheaf hB G X hG hX hfree hflat hfp) hB)
hX
Tag 04U1, a lemma
Tag 04U1 in the Stacks Project.
AlgebraicGeometry.Space.isFppfTorsor_of_isFppfCovering_of_modIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/TorsorDescent/GlueingTorsors.lean, line 181. The attribute's comment: “the glued object is an fppf torsor; not its existence from the descent datum”.
The glued object of Stacks 04U1 is an fppf torsor.
Let
{Bᵢ ⟶ B}be an fppf covering of an algebraic spaceBoverS, letGbe a group algebraic space overB, and suppose given for eachian fppf torsorXᵢoverBᵢunder the base change ofG. IfXis an algebraic space overBcarrying an action ofGtogether with, for eachi, an isomorphisme iof the base change ofXtoBᵢwithXᵢwhich is equivariant for the base change ofG, thenXis an fppfG-torsor overB.The base changes of the action on
Xare fppf torsors by transport along thee i(AlgebraicGeometry.Space.isFppfTorsor_of_modIsoapplied to the inverse isomorphisms), and the two conditions are fppf local on the base byAlgebraicGeometry.Space.isFppfTorsor_of_isFppfCovering.The existence of
Xfrom the transition isomorphisms of a descent datum, and so the whole of Stacks 04U1, isAlgebraicGeometry.Space.exists_isFppfTorsor_of_descentDatum.
theorem isFppfTorsor_of_isFppfCovering_of_modIso (hB : IsAlgebraicSpace 𝒞 S hS B)
(G : Over B) [GrpObj G] (hG : IsAlgebraicSpace 𝒞 S hS G.left)
(X : Over B) [ModObj G X] (hX : IsAlgebraicSpace 𝒞 S hS X.left)
{I : Type (u + 1)} (Bᵢ : I → (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, Bᵢ i ⟶ B)
(hBᵢ : ∀ i, IsAlgebraicSpace 𝒞 S hS (Bᵢ i)) (hcov : IsFppfCovering 𝒞 S hS Bᵢ f)
(Xᵢ : ∀ i, Over (Bᵢ i)) [∀ i, ModObj ((Over.pullback (f i)).obj G) (Xᵢ i)]
(hXᵢ : ∀ i, IsAlgebraicSpace 𝒞 S hS (Xᵢ i).left)
(e : ∀ i, (Over.pullback (f i)).obj X ≅ Xᵢ i)
(he : ∀ i, IsModHom ((Over.pullback (f i)).obj G) (e i).hom)
(htors : ∀ i, IsFppfTorsor 𝒞 S hS (Bᵢ i) (hBᵢ i) ((Over.pullback (f i)).obj G) (Xᵢ i)
(isAlgebraicSpace_pullback 𝒞 S hS G.hom (f i) hG (hBᵢ i) hB) (hXᵢ i)) :
IsFppfTorsor 𝒞 S hS B hB G X hG hX
AlgebraicGeometry.Space.exists_isFppfTorsor_of_descentDatum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/TorsorDescent/GlueingTorsorsExistence.lean, line 213.
Stacks 04U1. Let
{f i : Sᵢ ⟶ S}be a covering family of the big fppf site ofSand letGbe a group algebraic space overS. A descent datumDof fppf torsors along that family — for eachian fppf torsorD.x ioverSᵢunder the base changeGᵢofG, and for eachi, jan equivariant isomorphismD.φ i jbetween the restrictions ofD.x iand ofD.x jtoSᵢ ×_S Sⱼ, satisfying the cocycle condition over everySᵢ ×_S Sⱼ ×_S Sₖ— is effective: there is an fppfG-torsorXoverSwhose restriction to eachSᵢis isomorphic toD.x i, compatibly with theD.φ i j.The bootstrap theorem Stacks 04S6, condition (3), is used only to see that the glued torsor of sheaves is an algebraic space; the glueing is Stacks 04UM and the torsor conditions are carried along by it.
theorem exists_isFppfTorsor_of_descentDatum
(G : GroupAlgebraicSpace 𝒞 S hS (baseYoneda 𝒞 S hS)
(isAlgebraicSpace_yoneda 𝒞 S hS (Over.mk (𝟙 (𝒞.obj hS)))))
{I : Type w} (V : I → BigFppfOver 𝒞 S hS) (f : ∀ i, V i ⟶ Over.mk (𝟙 (𝒞.obj hS)))
(hf : Sieve.ofArrows V f ∈ BigFppfOver.topology 𝒞 S hS (Over.mk (𝟙 (𝒞.obj hS))))
(Vij : I → I → BigFppfOver 𝒞 S hS)
(pr₁ : ∀ i j, Vij i j ⟶ V i) (pr₂ : ∀ i j, Vij i j ⟶ V j)
(hVij : ∀ i j, IsPullback (pr₁ i j) (pr₂ i j) (f i) (f j))
(Vijk : I → I → I → BigFppfOver 𝒞 S hS)
(s₁₂ : ∀ i j k, Vijk i j k ⟶ Vij i j) (s₂₃ : ∀ i j k, Vijk i j k ⟶ Vij j k)
(hVijk : ∀ i j k, IsPullback (s₁₂ i j k) (s₂₃ i j k) (pr₂ i j) (pr₁ j k))
(q₁ : ∀ i j k, Vijk i j k ⟶ V i) (q₂ : ∀ i j k, Vijk i j k ⟶ V j)
(q₃ : ∀ i j k, Vijk i j k ⟶ V k)
(hq₁ : ∀ i j k, q₁ i j k = s₁₂ i j k ≫ pr₁ i j)
(hq₂ : ∀ i j k, q₂ i j k = s₁₂ i j k ≫ pr₂ i j)
(hq₃ : ∀ i j k, q₃ i j k = s₂₃ i j k ≫ pr₂ j k)
(D : Functor.DescentDatum
(FppfTorsors.projection (isAlgebraicSpace_yoneda 𝒞 S hS (Over.mk (𝟙 (𝒞.obj hS)))) G)
V f Vij pr₁ pr₂ hVij Vijk s₁₂ s₂₃ hVijk q₁ q₂ q₃ hq₁ hq₂ hq₃) :
D.IsEffective
Sources
Section80.12 Algebraic spaces in the étale topology#
Section 80.12 of the Stacks Project, Tag 076L. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 076M, a lemma
Tag 076M in the Stacks Project.
AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSheafAlgebraicCriterionTag076M.lean, line 80.
Stacks 076M. A presheaf of sets on the big fppf category over
Swhich is a sheaf for the chosen étale topology, whose diagonal is representable and which admits a surjective étale atlas by a scheme is an algebraic space overS.Only the fppf sheaf condition is at issue, and it comes from a comparison with the fppf quotient sheaf
U/Rof the étale equivalence relationR = U ×_F U: the atlas and the quotient map are both locally surjective for the étale topology and have the same kernel pair, soFandU/Rare the same coequalizer ofh_R ⇉ h_Uin étale sheaves, andFinherits the fppf sheaf condition fromU/R. The comparison isAlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_isLocallySurjective_quotientMap; the étale-local surjectivity of the quotient map is Stacks 02WW.
theorem isAlgebraicSpace_of_isSheaf_etale (B : BigFppfSite.{u}) (S : Scheme.{u})
(hS : B.Contains S) (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf ((etaleTopology B).over (B.obj hS)) F)
(hdiag : yoneda.relativelyRepresentable (diag F))
(hatlas : ∃ (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ F),
(MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
(BigFppfOver.toScheme B S hS)).presheaf f ∧
(MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
(BigFppfOver.toScheme B S hS)).presheaf f) :
IsAlgebraicSpace B S hS F
Tag 0BH4, a lemma
Tag 0BH4 in the Stacks Project.
AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_etale_space_atlas_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSheafAtlasCriteria.lean, line 111.
Stacks 0BH4. Let
Fbe a presheaf of sets on the big category overS, which is the common underlying category of the chosen big fppf and big étale sites. IfFis a sheaf for the étale topology and there are an algebraic spaceXoverSand a morphismX ⟶ Fwhich is representable by algebraic spaces, surjective and étale, thenFis an algebraic space overSin the sense of Algebraic Spaces, Definition 025Y.This is
AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_etale_space_atlaswith its Stacks 04S6 input discharged byAlgebraicGeometry.Space.bootstrap04S6QuotientSheaf.
theorem isAlgebraicSpace_of_isSheaf_etale_of_etale_space_atlas_unconditional
(F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf ((etaleTopology B).over (B.obj hS)) F)
{X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) (a : X ⟶ F)
(ha : IsRepresentableByAlgebraicSpaces B S hS a)
(hsurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) a ha)
(hetale : HasProperty B S hS (etaleMorphisms B S hS) a ha) :
IsAlgebraicSpace B S hS F
AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_etale_space_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSheafSpaceCoverCriterion.lean, line 734. The attribute's comment: “granted Stacks 04S6 part (1), the algebraicity of the fppf quotient sheaf of a flat locally finitely presented equivalence relation of algebraic spaces, carried as the hypothesis h04S6; the library's Stacks 04S6 is conditions (5) and (6), which need the quotient's diagonal and are themselves conditional on condition (3), so neither discharges it”.
Stacks 0BH4. Let
Fbe a presheaf of sets on the big category overS, which is the common underlying category of the chosen big fppf and big étale sites. IfFis a sheaf for the étale topology and there are an algebraic spaceXoverSand a morphismX ⟶ Fwhich is representable by algebraic spaces, surjective and étale, thenFis an algebraic space overSin the sense of Algebraic Spaces, Definition 025Y.The étale cover is smooth, so the criterion is the smooth one of
AlgebraicGeometry.Space.coreCriterion.
theorem isAlgebraicSpace_of_isSheaf_etale_of_etale_space_atlas
(F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf ((etaleTopology B).over (B.obj hS)) F)
{X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) (a : X ⟶ F)
(ha : IsRepresentableByAlgebraicSpaces B S hS a)
(hsurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) a ha)
(hetale : HasProperty B S hS (etaleMorphisms B S hS) a ha)
(h04S6 : Bootstrap04S6QuotientSheaf B S hS) :
IsAlgebraicSpace B S hS F
Tag 07WF, a lemma
Tag 07WF in the Stacks Project.
AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_smooth_scheme_atlas_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSheafAtlasCriteria.lean, line 135.
Stacks 07WF. Let
Fbe a presheaf of sets on the big category overS, which is the common underlying category of the chosen big fppf and big étale sites. IfFis a sheaf for the étale topology, its diagonalΔ : F ⟶ F × Fis representable by algebraic spaces, and there are an objectUof the category overSand a morphismh_U ⟶ Fwhich is surjective and smooth, thenFis an algebraic space overSin the sense of Algebraic Spaces, Definition 025Y.The representability by algebraic spaces of the cover is not a further hypothesis: it follows from the representable diagonal by
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_diagonal, and the surjectivity and smoothness are asked of that witness. This isAlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_smooth_scheme_atlaswith its Stacks 04S6 input discharged byAlgebraicGeometry.Space.bootstrap04S6QuotientSheaf.
theorem isAlgebraicSpace_of_isSheaf_etale_of_smooth_scheme_atlas_unconditional
(F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf ((etaleTopology B).over (B.obj hS)) F)
(hdiag : IsRepresentableByAlgebraicSpaces B S hS (diag F))
(U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ F)
(hsurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) a
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS hdiag
(isAlgebraicSpace_yoneda B S hS U) a))
(hsmooth : HasProperty B S hS (smoothMorphismProperty B S hS) a
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS hdiag
(isAlgebraicSpace_yoneda B S hS U) a)) :
IsAlgebraicSpace B S hS F
AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_smooth_scheme_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSheafSpaceCoverCriterion.lean, line 760. The attribute's comment: “granted Stacks 04S6 part (1), the algebraicity of the fppf quotient sheaf of a flat locally finitely presented equivalence relation of algebraic spaces, carried as the hypothesis h04S6; the library's Stacks 04S6 is conditions (5) and (6), which need the quotient's diagonal and are themselves conditional on condition (3), so neither discharges it”.
Stacks 07WF. Let
Fbe a presheaf of sets on the big category overS, which is the common underlying category of the chosen big fppf and big étale sites. IfFis a sheaf for the étale topology, its diagonalΔ : F ⟶ F × Fis representable by algebraic spaces, and there are an objectUof the category overSand a morphismh_U ⟶ Fwhich is surjective and smooth, thenFis an algebraic space overSin the sense of Algebraic Spaces, Definition 025Y.The representability by algebraic spaces of the cover is not a further hypothesis: it follows from the representable diagonal by
AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_diagonal, and the surjectivity and smoothness are asked of that witness.
theorem isAlgebraicSpace_of_isSheaf_etale_of_smooth_scheme_atlas
(F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
(hF : Presheaf.IsSheaf ((etaleTopology B).over (B.obj hS)) F)
(hdiag : IsRepresentableByAlgebraicSpaces B S hS (diag F))
(U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ F)
(hsurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) a
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS hdiag
(isAlgebraicSpace_yoneda B S hS U) a))
(hsmooth : HasProperty B S hS (smoothMorphismProperty B S hS) a
(isRepresentableByAlgebraicSpaces_of_diagonal B S hS hdiag
(isAlgebraicSpace_yoneda B S hS U) a))
(h04S6 : Bootstrap04S6QuotientSheaf B S hS) :
IsAlgebraicSpace B S hS F
Tag 0GE0, a lemma
Tag 0GE0 in the Stacks Project.
AlgebraicGeometry.Space.isAlgebraicSpace_of_etaleSheaf_of_smooth_surjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleTopologyBootstrap.lean, line 101.
Let
Sbe a scheme contained in a big fppf siteBand letFbe a presheaf on the common underlying categorySch_α/Sof the big fppf and the big étale site ofS. Assume
Fis a sheaf for the étale topology, and- there are an algebraic space
UoverSand a morphismf : U ⟶ Fwhich is representable by algebraic spaces, surjective and smooth.Then
Fis an algebraic space overS.
theorem isAlgebraicSpace_of_etaleSheaf_of_smooth_surjection
{F U : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
(hF : Presheaf.IsSheaf (BigEtaleOver.topology (associatedBigEtaleSite B) S hS) F)
(hU : IsAlgebraicSpace B S hS U) (f : U ⟶ F)
(hf : IsRepresentableByAlgebraicSpaces B S hS f)
(hsurj : HasProperty B S hS (surjectiveMorphismProperty B S hS) f hf)
(hsmooth : HasProperty B S hS (smoothMorphismProperty B S hS) f hf) :
IsAlgebraicSpace B S hS F
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.