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 S is 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 of S is an algebraic space over S.

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 S has an algebraic space over S as its source.

The three clauses of AlgebraicGeometry.IsAlgebraicSpace are 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 of G along a gives a surjective étale morphism to F from an algebraic space, and composing it with a scheme atlas of that algebraic space gives a scheme atlas of F.

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 S with the source of a morphism representable by algebraic spaces, over the target of that morphism, is an algebraic space over S, for presheaves on the big fppf site of S with values in Type (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 S with the source of a morphism representable by algebraic spaces, over the target of that morphism, is an algebraic space over S.

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 S representable by algebraic spaces is representable by algebraic spaces.

The base change of a ≫ b along ξ is the base change of a along the second projection of the base change of b along ξ, 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 S representable by algebraic spaces is representable by algebraic spaces.

The product a₁ ⨯ a₂ is the composite of a₁ ⨯ 𝟙 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 b and the composite a ≫ b are representable by algebraic spaces, then so is a, for presheaves on the big fppf site of S with values in Type (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 b and the composite a ≫ b are representable by algebraic spaces, then so is a.

The base change of a along ξ is the base change of the relative diagonal of b along the canonical morphism from the base change of a ≫ b along ξ ≫ b to pullback 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 S which 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

LeanAlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces · AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_isAlgebraicSpace · AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_isPullback · AlgebraicGeometry.Space.isSheaf_of_isRepresentableByAlgebraicSpaces · AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_diagonal · AlgebraicGeometry.Space.isAlgebraicSpaceULift_of_isRepresentable_uliftYoneda · AlgebraicGeometry.isAlgebraicSpace_of_isRepresentableByAlgebraicSpaces · AlgebraicGeometry.Space.isAlgebraicSpaceULift_pullback_of_isRepresentableULift

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 ⟶ G on the big fppf site of S which is representable by algebraic spaces has property P when, for every object U of the site and every ξ : h_U ⟶ G, the morphism of algebraic spaces U ×_G F ⟶ U has P.

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 S whose right-hand column a is representable by algebraic spaces and has a property P of morphisms of algebraic spaces over S, the left-hand column a' is representable by algebraic spaces (Stacks 03Y0) and has P.

Only invariance of P under isomorphism is used, which is weaker than the two conditions Stacks imposes on P in 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 S which 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_isPullback registered with add_to_stacks in 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 S representable by algebraic spaces has a property P of morphisms of algebraic spaces over S as soon as both factors do, provided P is 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_comp registered with add_to_stacks in 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 S representable by algebraic spaces has a property P of morphisms of algebraic spaces over S as soon as both factors do, provided P is 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.HasProperty may be enlarged: if P implies Q for every morphism of algebraic spaces over S, then a morphism of presheaves representable by algebraic spaces having P also has Q.

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 S which 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

LeanAlgebraicGeometry.Space.HasProperty · AlgebraicGeometry.Space.HasProperty.of_isPullback · AlgebraicGeometry.Space.hasProperty_of_isPullback · isRepresentableByAlgebraicSpaces_of_isPullback · AlgebraicGeometry.Space.hasProperty_comp · isRepresentableByAlgebraicSpaces_comp · AlgebraicGeometry.Space.hasProperty_prod_map · AlgebraicGeometry.Space.HasProperty.mono

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 S is representable by algebraic spaces exactly when every morphism to that presheaf from a scheme over S is 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 S from a scheme over S is equivalent to representability by algebraic spaces of every morphism to it from an algebraic space over S.

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 S whose right-hand column g is representable by algebraic spaces, surjective, flat and locally of finite presentation and whose top row a is representable by algebraic spaces, separated and locally quasi-finite, the bottom row b is representable by objects of the site, separated and locally quasi-finite.

Representability of b by objects of the site is AlgebraicGeometry.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 F be a sheaf on the big fppf site of a scheme S which admits a morphism f : X ⟶ F from an algebraic space over S that is representable by algebraic spaces, surjective, flat and locally of finite presentation. Then the absolute diagonal Δ_F : F ⟶ F × F is representable by objects of the site, that is, every fibre product of Δ_F with a scheme-valued point of F × F is again a scheme over S — not merely an algebraic space, as Stacks 03Y2 would give.

Let d = Δ_F and let k = 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 product W = (X ⨯ X) ×_{F × F} F is the kernel pair X ×_F X of f, so its projection to X ⨯ X is representable by algebraic spaces, separated and locally quasi-finite. Given a scheme-valued point η : h_T ⟶ F × F, the base change T' = h_T ×_{F × F} (X ⨯ X) ⟶ h_T of k inherits the three properties by Stacks 046F, and T' ×_{X ⨯ X} W ⟶ T' inherits separatedness and local quasi-finiteness from the projection of W; that fibre product is at the same time the base change of Z = h_T ×_{F × F} F ⟶ h_T along T' ⟶ h_T. Stacks 046J applied to the resulting cartesian square makes Z ⟶ h_T representable by objects of the site, and Z is the fibre product of Δ_F with η.

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 F be a presheaf of sets on the big fppf site of S and let X be a scheme over S, that is an object of the site. A morphism a : h_X ⟶ F which 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 a along a scheme-valued point of F is a locally quasi-finite morphism of algebraic spaces over S.

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

LeanAlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_diag_iff_forall_yoneda · AlgebraicGeometry.Space.forall_yoneda_isRepresentableByAlgebraicSpaces_iff_isAlgebraicSpace · AlgebraicGeometry.Space.relativelyRepresentable_separated_locallyQuasiFinite_of_isPullback · AlgebraicGeometry.Space.relativelyRepresentable_diag_of_flat_presentation · AlgebraicGeometry.Space.relativelyRepresentable_of_isLocallyQuasiFinite_of_schemeSource

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 F be an fppf sheaf on the big fppf site of a scheme S admitting a morphism f : X ⟶ F from an algebraic space over S which is representable by algebraic spaces, surjective and étale. Then F is an algebraic space over S.

The chart of F is the composite of a chart of X with f, 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 by isEffectiveDescentAlongCoveringSieve_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 F be an fppf sheaf on the big fppf site of a scheme S whose diagonal is representable by algebraic spaces and which admits a surjective étale morphism from an algebraic space over S. Then F is an algebraic space over S.

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

LeanAlgebraicGeometry.Space.isAlgebraicSpace_of_isRepresentableByAlgebraicSpaces_surjective_etale · AlgebraicGeometry.Space.isAlgebraicSpace_of_isRepresentableByAlgebraicSpaces_diag

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 G be a groupoid scheme over S and let g : U' ⟶ U be a morphism to its scheme of objects whose saturation is the range of an open immersion i : W ⟶ U. If the reach map factors as k ≫ i with k inducing a surjection of fppf sheaves, then the map of quotient sheaves U'/R' ⟶ U/R induced by the restriction of G along g is 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

LeanAlgebraicGeometry.GroupoidScheme.isOpenImmersion_restrictionQuotientMap_of_open_image

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 R be a groupoid scheme over S whose target and source are an equivalence relation. Given a refinement in the sense of Stacks.Groupoids.GroupoidScheme.QuasiFiniteRefinement — a morphism g : U' ⟶ U whose reach map is flat, locally of finite presentation and locally quasi-finite and is a singleton covering of the site — the restriction R' = 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 map U'/R' ⟶ U/R of 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.restrict built by Classical.choice. The morphism U' ⟶ U carrying R' into R is the one recorded by AlgebraicGeometry.GroupoidScheme.Restriction.hom, so the clause of the tag that the isomorphism of quotient sheaves is induced by a morphism U' ⟶ U mapping R' into R is part of the statement rather than an afterthought.

The flatness and local finite presentation hypotheses which the tag places on s and t are 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 over S whose target and source maps form an equivalence relation and are flat and locally of finite presentation. Then there are a scheme U' over S, a morphism U' ⟶ U, and an equivalence relation R' on U' mapping into R over 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 map U'/R' ⟶ U/R of quotient sheaves on the big fppf site over S is an isomorphism.

The refinement is produced in the two stages of the source proof: g₁ : U₁ ⟶ U is the inclusion of the Cohen-Macaulay open of Stacks 0460, H₁ is the restriction of R along it, g' : U' ⟶ U₁ is the disjoint union of the affine slices of Stacks 04N0 over the finite type points of U₁, and R' is the restriction H' of H₁ along g'. The morphism U' ⟶ U is the composite g, and the morphism of R' into R is the composite of the two restrictions' canonical morphisms, which lies over g by the second conclusion below.

The last conclusion is more than the tag asks: the map of quotient sheaves induced by the restriction of R along the single morphism g is an isomorphism for every groupoid scheme realizing that restriction. Together with the isomorphism for R' 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, so size U₁ ≤ size U and size 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 exhibit U' and the arrow scheme of R' 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 S with 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 morphism g of object schemes and a morphism r of 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

LeanStacks.Groupoids.GroupoidScheme.exists_restriction_locallyQuasiFinite_isIso_quotientMap · AlgebraicGeometry.GroupoidScheme.exists_locallyQuasiFinite_refinement_isIso_quotientMap · AlgebraicGeometry.exists_slice_locallyQuasiFinite

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_division reduce to finiteness, by AlgebraicGeometry.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 by AlgebraicGeometry.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 scheme G over S and let (U, P, s|_P, t|_P, c|_P) be a groupoid scheme H mapping to it by a morphism i which is an isomorphism on objects, such that

s|_P, t|_P : P ⟶ U are finite locally free,

j|_P = (t|_P, s|_P) : P ⟶ U ×_S U is a monomorphism,

U is affine, and

j = (t, s) : R ⟶ U ×_S U is separated and locally quasi-finite (locally of finite type with finite fibres; the finite type half is a separate class here).

Then U/P is representable by an affine scheme Ū, the quotient morphism U ⟶ Ū is finite locally free (and surjective), and P = U ×_Ū U; these are the fields of Stacks.Groupoids.FiniteFlatQuotient together with affineness of its quotient scheme. Moreover R is the restriction of a groupoid scheme on Ū along the quotient morphism: there is a groupoid scheme K with object scheme Ū and a morphism G ⟶ K which 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 ⟶ R be a monomorphism; this follows from the other hypotheses (j ∘ i = (i × i) ∘ j|_P is 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

LeanAlgebraicGeometry.GroupoidScheme.exists_division_isField_quotient_of_isoSpecField · AlgebraicGeometry.exists_finiteFlatQuotient_isAffine_of_mono_groupoidPreRelation · AlgebraicGeometry.GroupoidScheme.exists_division

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 F be a sheaf on the big fppf site of a scheme S whose absolute diagonal is representable by algebraic spaces, and suppose there is an algebraic space X over S and a morphism f : X ⟶ F which is surjective, flat and locally of finite presentation. Then F is an algebraic space over S.

The chart f is not assumed to be representable by algebraic spaces; it is so automatically, by AlgebraicGeometry.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 F be a sheaf on the big fppf site of a scheme S whose absolute diagonal is representable, and suppose there is a scheme U over S and a morphism f : h_U ⟶ F which is surjective, flat and locally of finite presentation. Then F is an algebraic space over S.

This is condition (5) for the algebraic space h_U: a representable diagonal is representable by algebraic spaces by AlgebraicGeometry.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_locallyOfFinitePresentation with 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 over S whose object scheme belongs to the big fppf site, such that s, t are flat and locally of finite presentation and j = (t, s) : R ⟶ U ×_S U is an equivalence relation. Then the fppf quotient sheaf U/R is 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 U be an equivalence relation of algebraic spaces over a presheaf Z on the big fppf site of S, whose target and source t, s : R ⟶ U are flat and locally of finite presentation. Then the fppf quotient sheaf U/R is an algebraic space.

The proof is the source's: U is replaced by an étale atlas h_{U₀} ⟶ U (Groupoids in Spaces, Lemma 046P, AlgebraicGeometry.Space.isIso_restrictQuotientSheafMap_chartInSliceMap); the restricted relation R₀ = U₀ ×_U R ×_U U₀ is then an algebraic space with a monomorphism, locally of finite type, to U₀ ×_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 F be a sheaf on the big fppf site of S, and suppose there are an algebraic space X over S and a morphism X ⟶ F which is representable by algebraic spaces, surjective, flat and locally of finite presentation. Then F is an algebraic space over S.

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 F be a sheaf on the big fppf site of S, and suppose there are a scheme U of the site and a morphism h_U ⟶ F which is representable by algebraic spaces (in particular, one representable by schemes), surjective, flat and locally of finite presentation. Then F is an algebraic space over S.

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

LeanAlgebraicGeometry.Space.isAlgebraicSpace_of_diag_of_flat_chart · AlgebraicGeometry.Space.isAlgebraicSpace_of_relativelyRepresentable_diag_of_flat_scheme_chart · AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_quotient_groupoidInAlgebraicSpaces ·

AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representable_hasProperty_surjective_flat_locallyOfFinitePresentation

· AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representable_surjective_flat_locallyOfFinitePresentation ·

AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representable_hasProperty_surjective_flat_locallyOfFinitePresentation_scheme

· AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representable_surjective_flat_locallyOfFinitePresentation_scheme · AlgebraicGeometry.Bootstrap04S6.isAlgebraicSpace_of_representableDiagonal_surjective_flat_locallyOfFinitePresentation

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 F be a presheaf of sets on the big fppf site of S and let {S i → S} be a covering family of the base. Assume

F is a sheaf (hF);

each restriction F_i = h_{S i} × F is an algebraic space (hFi);

the coproduct ∐ F_i is an algebraic space: G, presented by the colimit cofan hcoprod with legs ι, is a coproduct of the F_i in sheaves, and it is an algebraic space (hG).

Then F is 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_i need not exist in sheaves of Type 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 by S, which is AlgebraicGeometry.isAlgebraicSpace_of_isCovering_of_atlas_size_le; what that lemma asks for is a bounded étale atlas of the restriction of each F_i to an affine open W of S_i, and hypothesis (3) is exactly what supplies it. An étale atlas U of ∐ F_i splits along the coproduct into étale atlases U_i of the F_i, which are open in U (AlgebraicGeometry.Sheaf.exists_clopen_decomposition_of_isColimit_cofan). The restriction of F_i to W is the base change of F_i along W ⟶ S_i, so W ×_{S_i} U_i is an étale atlas of it, of size at most max (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 F be a presheaf of sets on the big fppf site of S and let {S i → S} be a covering family of the base, and assume

F is a sheaf (hF);

each restriction h_{S i} × F is an algebraic space (hFi);

each restriction is of finite type over its member (hft).

Then F is an algebraic space.

The refinement of the covering by affines over the points of S, Stacks 02WQ and the final appeal to Stacks 04S6 are AlgebraicGeometry.isAlgebraicSpace_of_isCovering_of_atlas_size_le. What this proof adds is the bounded atlas it asks for: the restriction of h_{S i} × F to an affine open W of S i is of finite type over W, hence quasi-compact, hence has an affine étale atlas (Stacks 03H6), which is locally of finite type over S and so of size at most size (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 over S whose 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 over S, indexed by a type of any size. Then every descent datum (Y i, φ i j) relative to it with each Y i ⟶ X i of finite type is effective.

The proof is the source's. The sheaf F of Stacks 0ADT the datum descends to has X 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 of T (AlgebraicGeometry.Space.exists_affine_refinement_of_isFppfCovering, which uses Stacks 042T). If R k ⟶ T factors through X i, then R k ×_T F = R k ×_{X i} Y i is of finite type over the affine R k. So it has an atlas of size at most size (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 k and ∐ (R k ×_T F) algebraic spaces, and Stacks 04S6 makes F an 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 ⟶ G and b : G ⟶ H be morphisms of presheaves on the big fppf site of S, with G and H sheaves. If a is representable by algebraic spaces, surjective, flat and locally of finite presentation and the composite a ≫ b is representable by algebraic spaces, then b is representable by algebraic spaces.

At a scheme-valued point ξ of H the fibre product U ×_H F is an algebraic space, being a base change of a ≫ b, and U ×_H G is a sheaf. The morphism U ×_H F ⟶ U ×_H G is the base change of a along U ×_H G ⟶ G, so Stacks 046F gives it the three properties of a, and Stacks 04S6 condition (3) makes U ×_H G an algebraic space; that deduction is AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_comp_of_flat_surjective, whose bootstrap input is discharged here by AlgebraicGeometry.Space.isBootstrapAlgebraicSpaceAlongFlatSurjection.

Sheafness of F is assumed in the source and is not needed here: representability of a ≫ b already makes the base changes of F that 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 ⟶ G and b : G ⟶ H on the big fppf site of S with G and H sheaves, if a is representable by algebraic spaces, surjective, flat and locally of finite presentation and the composite a ≫ b is representable by algebraic spaces, then b is representable by algebraic spaces.

At a scheme-valued point ξ of H the fibre product U ×_H F is an algebraic space, being a base change of a ≫ b, and U ×_H G is a sheaf. The morphism U ×_H F ⟶ U ×_H G is the base change of a along U ×_H G ⟶ G, so Stacks 046F gives it the three properties of a, and the bootstrap theorem makes U ×_H G an algebraic space.

Sheafness of F is assumed in the source and is not needed here: representability of a ≫ b already makes the base changes of F that the argument uses algebraic spaces.

This does not register [Stacks, Tag 0AMP] and carries no attribute. Its input hbootstrap is Stacks 04S6 part (3), which this repository does not prove, and isBootstrapAlgebraicSpaceAlongFlatSurjection_iff below 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 u which is an algebraic space: the hom sets of the stackification are not small, so Isom(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 U on 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 of U dominating the original one.

This also discharges the surjectivity clause of Stacks 06PH, that X ⟶ X/G is surjective for a free action of a group algebraic space: the quotient X/G of [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 of G ⟶ B; the remaining clauses of Stacks 06PH — algebraicity of X/G, flatness and local finite presentation of X ⟶ 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/S of 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/S is 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/S is 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/S is 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 U on 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 of U dominating the original one.

This also discharges the surjectivity clause of Stacks 06PH, that X ⟶ X/G is surjective for a free action of a group algebraic space: the quotient X/G of [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 of G ⟶ B; the remaining clauses of Stacks 06PH — algebraicity of X/G, flatness and local finite presentation of X ⟶ 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/G is surjective.

This holds for the quotient sheaf of any pre-relation, by Stacks 06PG, so neither freeness nor any property of G ⟶ B is 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/G of 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/G of 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/G of 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, X is an fppf torsor over X/G under the group G pulled back to X/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 space B over S, let G be a group algebraic space over B, and suppose given for each i an fppf torsor Xᵢ over Bᵢ under the base change of G. If X is an algebraic space over B carrying an action of G together with, for each i, an isomorphism e i of the base change of X to Bᵢ with Xᵢ which is equivariant for the base change of G, then X is an fppf G-torsor over B.

The base changes of the action on X are fppf torsors by transport along the e i (AlgebraicGeometry.Space.isFppfTorsor_of_modIso applied to the inverse isomorphisms), and the two conditions are fppf local on the base by AlgebraicGeometry.Space.isFppfTorsor_of_isFppfCovering.

The existence of X from the transition isomorphisms of a descent datum, and so the whole of Stacks 04U1, is AlgebraicGeometry.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 of S and let G be a group algebraic space over S. A descent datum D of fppf torsors along that family — for each i an fppf torsor D.x i over Sᵢ under the base change Gᵢ of G, and for each i, j an equivariant isomorphism D.φ i j between the restrictions of D.x i and of D.x j to Sᵢ ×_S Sⱼ, satisfying the cocycle condition over every Sᵢ ×_S Sⱼ ×_S Sₖ — is effective: there is an fppf G-torsor X over S whose restriction to each Sᵢ is isomorphic to D.x i, compatibly with the D.φ 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

LeanAlgebraicGeometry.isAlgebraicSpace_of_isCovering · AlgebraicGeometry.isAlgebraicSpace_of_isCovering_of_isFiniteType · AlgebraicGeometry.Space.Descent.DescentData.isEffective_of_countable · AlgebraicGeometry.Space.Descent.DescentData.isEffective_of_isFiniteType · AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_comp_of_flat_surjective_unconditional · AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_of_comp_of_flat_surjective · AlgebraicGeometry.Stack.isAlgebraicSpace_isomPresheaf · AlgebraicGeometry.Space.isSurjective_toQuotientSheaf

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 S which 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 over S.

Only the fppf sheaf condition is at issue, and it comes from a comparison with the fppf quotient sheaf U/R of the étale equivalence relation R = U ×_F U: the atlas and the quotient map are both locally surjective for the étale topology and have the same kernel pair, so F and U/R are the same coequalizer of h_R ⇉ h_U in étale sheaves, and F inherits the fppf sheaf condition from U/R. The comparison is AlgebraicGeometry.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 F be a presheaf of sets on the big category over S, which is the common underlying category of the chosen big fppf and big étale sites. If F is a sheaf for the étale topology and there are an algebraic space X over S and a morphism X ⟶ F which is representable by algebraic spaces, surjective and étale, then F is an algebraic space over S in the sense of Algebraic Spaces, Definition 025Y.

This is AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_etale_space_atlas with its Stacks 04S6 input discharged by AlgebraicGeometry.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 F be a presheaf of sets on the big category over S, which is the common underlying category of the chosen big fppf and big étale sites. If F is a sheaf for the étale topology and there are an algebraic space X over S and a morphism X ⟶ F which is representable by algebraic spaces, surjective and étale, then F is an algebraic space over S in 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 F be a presheaf of sets on the big category over S, which is the common underlying category of the chosen big fppf and big étale sites. If F is a sheaf for the étale topology, its diagonal Δ : F ⟶ F × F is representable by algebraic spaces, and there are an object U of the category over S and a morphism h_U ⟶ F which is surjective and smooth, then F is an algebraic space over S in 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 is AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_smooth_scheme_atlas with its Stacks 04S6 input discharged by AlgebraicGeometry.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 F be a presheaf of sets on the big category over S, which is the common underlying category of the chosen big fppf and big étale sites. If F is a sheaf for the étale topology, its diagonal Δ : F ⟶ F × F is representable by algebraic spaces, and there are an object U of the category over S and a morphism h_U ⟶ F which is surjective and smooth, then F is an algebraic space over S in 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 S be a scheme contained in a big fppf site B and let F be a presheaf on the common underlying category Sch_α/S of the big fppf and the big étale site of S. Assume

F is a sheaf for the étale topology, and

there are an algebraic space U over S and a morphism f : U ⟶ F which is representable by algebraic spaces, surjective and smooth.

Then F is an algebraic space over S.

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

LeanAlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale · AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_etale_space_atlas_unconditional · AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_etale_space_atlas · AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_smooth_scheme_atlas_unconditional · AlgebraicGeometry.Space.isAlgebraicSpace_of_isSheaf_etale_of_smooth_scheme_atlas · AlgebraicGeometry.Space.isAlgebraicSpace_of_etaleSheaf_of_smooth_surjection

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

80 Bootstrap

Section80.3 Morphisms representable by algebraic spaces#

Tag 02YQ, a definition

Tag 03BN, a lemma

Tag 03Y0, a lemma

Tag 02YR, a lemma

Tag 05LA, a lemma

Tag 02YS, a lemma

Tag 03XY, a lemma

Tag 03Y1, a lemma

Tag 046D, a lemma

Tag 0AMN, a lemma

Tag 07WE, a lemma

Sources

Section80.4 Properties of maps of presheaves representable by algebraic spaces#

Tag 03XZ, a definition

Tag 046F, a lemma

Tag 046G, a lemma

Tag 046H, a lemma

Tag 0AM1, a lemma

Tag 04S1, a lemma

Sources

Section80.5 Bootstrapping the diagonal#

Tag 03Y2, a lemma

Tag 046J, a lemma

Tag 046K, a lemma

Tag 0AHV, a lemma

Sources

Section80.6 Bootstrap#

Tag 03Y3, a theorem

Sources

Section80.7 Finding opens#

Tag 046M, a lemma

Sources

Section80.8 Slicing equivalence relations#

Tag 0489, a lemma

Sources

Section80.9 Quotient by a subgroupoid#

Tag 04S4, a lemma

Sources

Section80.10 Final bootstrap#

Tag 04S6, a theorem

Sources

Section80.11 Applications#

Tag 04SK, a lemma

Tag 04U0, a lemma

Tag 0ADV, a lemma

Tag 0AMP, a lemma

Tag 04TB, a lemma

Tag 06PG, a lemma

Tag 06PH, a lemma

Tag 04U1, a lemma

Sources

Section80.12 Algebraic spaces in the étale topology#

Tag 076M, a lemma

Tag 0BH4, a lemma

Tag 07WF, a lemma

Tag 0GE0, a lemma

Sources

Section80.3 Morphisms representable by algebraic spaces #

Section80.4 Properties of maps of presheaves representable by algebraic spaces #

Section80.5 Bootstrapping the diagonal #

Section80.6 Bootstrap #

Section80.7 Finding opens #

Section80.8 Slicing equivalence relations #

Section80.9 Quotient by a subgroupoid #

Section80.10 Final bootstrap #

Section80.11 Applications #

Section80.12 Algebraic spaces in the étale topology #