94 Algebraic Stacks

Chapter 94 of the Stacks Project, Algebraic Stacks, Tag 026K: the 14 sections of its 19 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 67 tags are carried by 182 declarations of the repository (all in StacksFrontier) and 23 registered declarations.

Section94.4 Representable categories fibred in groupoids#

Section 94.4 of the Stacks Project, Tag 02ZQ. 1 tag here is carried by 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04SR, an equation

Tag 04SR in the Stacks Project.

Declarations registered for the tag:

Sources
LeanCategoryTheory.Functor.twoIsoQuotientEquivHomOfRepresentableBy · CategoryTheory.Functor.exists_oneMorphism_inducing_hom

Section94.6 Representable morphisms of categories fibred in groupoids#

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

Tag 02ZR, a lemma

Tag 02ZR in the Stacks Project.

Stacks.RepresentableMorphism.isRepresentableMorphism_overMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Algebraic/RepresentableMorphism/Slices.lean, line 315.

Stacks 02ZR. A morphism in a category with pullbacks induces a representable 1-morphism of the categories fibred in groupoids of objects over its source and target.

public theorem isRepresentableMorphism_overMap (f : X ⟶ Y) :
    Stacks.RepresentableMorphism.IsRepresentableMorphism (Over.forget X) (Over.forget Y)
      (Over.map f)
Tag 0456, a lemma

Tag 0456 in the Stacks Project.

Stacks.RepresentableMorphism.isRepresentableMorphism_iff_of_equivalences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Algebraic/RepresentableMorphism/Invariance.lean, line 660.

Stacks 0456. Representability of a 1-morphism of categories fibred in groupoids is invariant under equivalences in a 2-commutative square.

public theorem isRepresentableMorphism_iff_of_equivalences
    (f' : 𝒳' ⟶ 𝒴') (f : 𝒳 ⟶ 𝒴)
    (a : 𝒳' ⟶ 𝒳) (b : 𝒴' ⟶ 𝒴)
    (α : a ≫ f ≅ f' ≫ b)
    [Functor.IsEquivalence (CatFiberedInGroupoids.homFunctor a)]
    [Functor.IsEquivalence (CatFiberedInGroupoids.homFunctor b)] :
    Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳.val.p 𝒴.val.p
      (CatFiberedInGroupoids.homFunctor f) ↔
    Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳'.val.p 𝒴'.val.p
      (CatFiberedInGroupoids.homFunctor f')
Tag 02ZS, a lemma

Tag 02ZS in the Stacks Project.

Stacks.RepresentableMorphism.isRepresentableMorphism_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Algebraic/RepresentableMorphism/Composition.lean, line 277.

Stacks 02ZS. A composite of representable 1-morphisms of categories fibred in groupoids over a base category is representable.

public lemma isRepresentableMorphism_comp
    (p : 𝒳 ⥤ 𝒞) (q : 𝒴 ⥤ 𝒞) (r : 𝒵 ⥤ 𝒞)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (hr : r.IsFiberedInGroupoids)
    (F : 𝒳 ⥤ 𝒴) (G : 𝒴 ⥤ 𝒵)
    (hF : F ⋙ q = p) (hG : G ⋙ r = q)
    (hrepF : Stacks.RepresentableMorphism.IsRepresentableMorphism p q F)
    (hrepG : Stacks.RepresentableMorphism.IsRepresentableMorphism q r G) :
    Stacks.RepresentableMorphism.IsRepresentableMorphism p r (F ⋙ G)
Tag 02ZT, a lemma

Tag 02ZT in the Stacks Project.

Stacks.RepresentableMorphism.isRepresentableMorphism_fst_twoFibreProductOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Algebraic/RepresentableMorphism/BaseChange.lean, line 437.

Stacks Project, Tag 02ZT. The projection to 𝒵 from the 2-fibre product 𝒵 ×_𝒴 𝒳 is representable when 𝒳 ⥤ 𝒴 is representable.

public theorem isRepresentableMorphism_fst_twoFibreProductOver
    (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (p𝒵 : 𝒵 ⥤ 𝒞)
    (F : 𝒳 ⥤ 𝒴) (G : 𝒵 ⥤ 𝒴)
    (hF : F ⋙ p𝒴 = p𝒳) (hG : G ⋙ p𝒴 = p𝒵)
    (hrep : Stacks.RepresentableMorphism.IsRepresentableMorphism p𝒳 p𝒴 F) :
    Stacks.RepresentableMorphism.IsRepresentableMorphism
      (TwoFibreProductOver.structureFunctor p𝒵 p𝒳 p𝒴 G F) p𝒵
      (TwoFibreProductOver.fst p𝒵 p𝒳 p𝒴 G F)
Tag 02ZU, a lemma

Tag 02ZU in the Stacks Project.

Stacks.RepresentableMorphism.isRepresentableMorphism_product, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Algebraic/RepresentableMorphism/Product.lean, line 362.

The product of two representable 1-morphisms of categories fibred in groupoids over a base category is representable.

public theorem isRepresentableMorphism_product
    (p₁ : 𝒳₁ ⥤ 𝒞) (p₂ : 𝒳₂ ⥤ 𝒞)
    (q₁ : 𝒴₁ ⥤ 𝒞) (q₂ : 𝒴₂ ⥤ 𝒞)
    (hp₁ : p₁.IsFiberedInGroupoids) (hp₂ : p₂.IsFiberedInGroupoids)
    (hq₁ : q₁.IsFiberedInGroupoids) (hq₂ : q₂.IsFiberedInGroupoids)
    (F₁ : 𝒳₁ ⥤ 𝒴₁) (F₂ : 𝒳₂ ⥤ 𝒴₂)
    (hF₁ : F₁ ⋙ q₁ = p₁) (hF₂ : F₂ ⋙ q₂ = p₂)
    (hrep₁ : Stacks.RepresentableMorphism.IsRepresentableMorphism p₁ q₁ F₁)
    (hrep₂ : Stacks.RepresentableMorphism.IsRepresentableMorphism p₂ q₂ F₂) :
    Stacks.RepresentableMorphism.IsRepresentableMorphism
      (TwoFibreProductOver.structureFunctor p₁ p₂ (𝟭 𝒞) p₁ p₂)
      (TwoFibreProductOver.structureFunctor q₁ q₂ (𝟭 𝒞) q₁ q₂)
      (productMorphism p₁ p₂ q₁ q₂ F₁ F₂ hF₁ hF₂)
Sources
LeanStacks.RepresentableMorphism.isRepresentableMorphism_overMap · Stacks.RepresentableMorphism.isRepresentableMorphism_iff_of_equivalences · Stacks.RepresentableMorphism.isRepresentableMorphism_comp · Stacks.RepresentableMorphism.isRepresentableMorphism_fst_twoFibreProductOver · Stacks.RepresentableMorphism.isRepresentableMorphism_product

Section94.7 Split categories fibred in groupoids#

Section 94.7 of the Stacks Project, Tag 04SU. 1 tag here is carried by 3 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04SU, the section

Tag 04SU in the Stacks Project.

CategoryTheory.PresheafOfCategories.elementsMapEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SplitCategoriesFibredInGroupoids.lean, line 95. The attribute's comment: “(e) maps of presheaves F ⟶ G are the 1-morphisms S_F ⥤ S_G over the base”.

Tag 04SU (e). The rule F ↦ 𝒮_F is fully faithful on presheaves of sets: maps of presheaves F ⟶ G are in bijection with the 1-morphisms 𝒮_F ⥤ 𝒮_G strictly over C, by m ↦ El m.

def elementsMapEquiv (F G : Cᵒᵖ ⥤ Type v) :
    (F ⟶ G) ≃ {θ : (presheafOfCategories (F ⋙ typeToCat)).obj ⥤
        (presheafOfCategories (G ⋙ typeToCat)).obj //
      θ ⋙ discreteProjection G = discreteProjection F}

CategoryTheory.TwoFibreProductOver.exists_elementsOp_equivalence_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SplitCategoriesFibredInGroupoids.lean, line 117. The attribute's comment: “(f) S_{F ×_H G} = S_F ×_{S_H} S_G for maps F → H ← G of presheaves of sets”.

Tag 04SU (f), fibre products. For maps α : F ⟶ H and β : G ⟶ H of presheaves of sets and a fibre product P = F ×_H G, the category of elements 𝒮_P is equivalent to the 2-fibre product 𝒮_F ×_{𝒮_H} 𝒮_G over C, by an equivalence which is strictly over C and whose composites with the two projections are the 1-morphisms induced by the projections of P.

theorem exists_elementsOp_equivalence_of_isPullback {α : F ⟶ H} {β : G ⟶ H} {pF : P ⟶ F}
    {pG : P ⟶ G} (h : IsPullback pF pG α β) :
    ∃ e : P.Elementsᵒᵖ ≌
        TwoFibreProductOver (CategoryOfElements.π F).leftOp (CategoryOfElements.π G).leftOp
          (CategoryOfElements.π H).leftOp (CategoryOfElements.map α).op
          (CategoryOfElements.map β).op,
      e.functor ⋙ structureFunctor _ _ _ _ _ = (CategoryOfElements.π P).leftOp ∧
      e.functor ⋙ fst _ _ _ _ _ = (CategoryOfElements.map pF).op ∧
      e.functor ⋙ snd _ _ _ _ _ = (CategoryOfElements.map pG).op

CategoryTheory.TwoFibreProductOver.exists_elementsOp_equivalence_of_isLimit_binaryFan, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SplitCategoriesFibredInGroupoids.lean, line 135. The attribute's comment: “(f) S_{F × G} = S_F ×_C S_G for presheaves of sets F, G”.

Tag 04SU (f), products. For a product P = F × G of presheaves of sets, the category of elements 𝒮_P is equivalent to the 2-fibre product 𝒮_F ×_C 𝒮_G over C (taken along the two structure functors and the identity of C), by an equivalence which is strictly over C and whose composites with the two projections are the 1-morphisms induced by the projections of P.

theorem exists_elementsOp_equivalence_of_isLimit_binaryFan {pF : P ⟶ F} {pG : P ⟶ G}
    (h : IsLimit (BinaryFan.mk pF pG)) :
    ∃ e : P.Elementsᵒᵖ ≌
        TwoFibreProductOver (CategoryOfElements.π F).leftOp (CategoryOfElements.π G).leftOp
          (𝟭 C) (CategoryOfElements.π F).leftOp (CategoryOfElements.π G).leftOp,
      e.functor ⋙ structureFunctor _ _ _ _ _ = (CategoryOfElements.π P).leftOp ∧
      e.functor ⋙ fst _ _ _ _ _ = (CategoryOfElements.map pF).op ∧
      e.functor ⋙ snd _ _ _ _ _ = (CategoryOfElements.map pG).op

Declarations registered for the tag:

Sources
LeanCategoryTheory.PresheafOfCategories.elementsMapEquiv · CategoryTheory.TwoFibreProductOver.exists_elementsOp_equivalence_of_isPullback · CategoryTheory.TwoFibreProductOver.exists_elementsOp_equivalence_of_isLimit_binaryFan · CategoryTheory.presheafOfGroupoids · CategoryTheory.isFiberedInGroupoids_presheafOfGroupoids · CategoryTheory.Functor.IsSplitFiberedInGroupoids · CategoryTheory.Functor.exists_isFibredEquivalenceOver_presheafOfGroupoids · CategoryTheory.PresheafOfCategories.isFiberedInSets_discreteProjection

Section94.8 Categories fibred in groupoids representable by algebraic spaces#

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

Tag 02ZV, the section

Tag 02ZV in the Stacks Project.

Declarations registered for the tag:

Tag 04SV, a definition

Tag 04SV in the Stacks Project.

AlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Representability.lean, line 66.

Stacks 04SV. A category fibred in groupoids over the big fppf site of S is represented by an algebraic space over S if it is equivalent, over that site, to the category of elements of the sheaf of points of an algebraic space over S.

abbrev IsRepresentableByAlgebraicSpace
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)) : Prop
Tag 02ZX, a lemma

Tag 02ZX in the Stacks Project.

AlgebraicGeometry.isRepresentableByAlgebraicSpace_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Algebraic/RepresentableBySpace/Characterization.lean, line 600.

Stacks 02ZX. A category fibred in groupoids over the big fppf site is represented by an algebraic space precisely when its fibres are setoids and its presheaf of isomorphism classes is an algebraic space.

public theorem isRepresentableByAlgebraicSpace_iff
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, v, u + 1, w} (AlgebraicGeometry.BigFppfOver B S hS)) :
    AlgebraicGeometry.IsRepresentableByAlgebraicSpace B S hS 𝒳 ↔
      (𝒳.val.p.IsFiberedInSetoids ∧ IsAlgebraicSpaceIsoClassPresheaf B S hS 𝒳)
Tag 04SW, an equation

Tag 04SW in the Stacks Project.

AlgebraicGeometry.Stack.morphismSpaceEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MorphismSpace.lean, line 72. The attribute's comment: “equivalence of morphism spaces”.

Stacks 04SW. One-morphisms of categories fibred in groupoids represented by F and G, modulo two-isomorphism, are morphisms F ⟶ G of the representing presheaves.

noncomputable def morphismSpaceEquiv
    (eX : StacksRepresentableCFG.EquivalenceOver
      𝒳.val.p (presheafOfCategories (F ⋙ typeToCat)).p)
    (eY : StacksRepresentableCFG.EquivalenceOver
      𝒴.val.p (presheafOfCategories (G ⋙ typeToCat)).p) :
    Quotient (Functor.twoIsoSetoid 𝒳.val.p 𝒴.val.p) ≃ (F ⟶ G)

AlgebraicGeometry.Stack.morphismSpaceEquiv_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MorphismSpace.lean, line 109. The attribute's comment: “induced map on fibre isomorphism classes”.

Stacks 04SW. On every fibre, the forward direction of AlgebraicGeometry.Stack.morphismSpaceEquiv is the map induced by the given one-morphism on isomorphism classes of objects.

theorem morphismSpaceEquiv_map
    (eX : StacksRepresentableCFG.EquivalenceOver
      𝒳.val.p (presheafOfCategories (F ⋙ typeToCat)).p)
    (eY : StacksRepresentableCFG.EquivalenceOver
      𝒴.val.p (presheafOfCategories (G ⋙ typeToCat)).p)
    (f : {H : 𝒳.val.obj ⥤ 𝒴.val.obj // H ⋙ 𝒴.val.p = 𝒳.val.p})
    (U : BigFppfOver B S hS) (a : F.obj (op U)) :
    letI : 𝒳.val.p.IsFibered := 𝒳.2.isFibered
    letI : 𝒴.val.p.IsFibered := 𝒴.2.isFibered
    ((Functor.isoClassMap
      (Functor.isFibredOneMorphism_of_isFiberedInGroupoids 𝒴.2 f.2)).app (op U))
      (Functor.isoClassMk 𝒳.val.p
        ((Functor.fiberFunctorOfCompEq eX.inv.w U).obj
          (⟨⟨U, Discrete.mk a⟩, rfl⟩ :
            (presheafOfCategories (F ⋙ typeToCat)).p.Fiber U))) =
    Functor.isoClassMk 𝒴.val.p
      ((Functor.fiberFunctorOfCompEq eY.inv.w U).obj
        (⟨⟨U, Discrete.mk
          ((morphismSpaceEquiv B S hS 𝒳 𝒴 F G eX eY (Quotient.mk _ f)).app
            (op U) a)⟩, rfl⟩ :
          (presheafOfCategories (G ⋙ typeToCat)).p.Fiber U))

AlgebraicGeometry.Stack.existsUnique_twoIso_of_morphismSpaceEquiv_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MorphismSpace.lean, line 177. The attribute's comment: “uniqueness up to unique two-isomorphism”.

Stacks 04SW. Two one-morphisms inducing the same morphism of representing presheaves admit a unique two-isomorphism over the site.

theorem existsUnique_twoIso_of_morphismSpaceEquiv_eq
    (eX : StacksRepresentableCFG.EquivalenceOver
      𝒳.val.p (presheafOfCategories (F ⋙ typeToCat)).p)
    (eY : StacksRepresentableCFG.EquivalenceOver
      𝒴.val.p (presheafOfCategories (G ⋙ typeToCat)).p)
    (f g : {H : 𝒳.val.obj ⥤ 𝒴.val.obj // H ⋙ 𝒴.val.p = 𝒳.val.p})
    (h : morphismSpaceEquiv B S hS 𝒳 𝒴 F G eX eY (Quotient.mk _ f) =
      morphismSpaceEquiv B S hS 𝒳 𝒴 F G eX eY (Quotient.mk _ g)) :
    ∃! α : f.1 ≅ g.1,
      ∀ x : 𝒳.val.obj, 𝒴.val.p.IsHomLift (𝟙 (𝒳.val.p.obj x)) (α.hom.app x)

AlgebraicGeometry.Space.eq_inducedSpacesHom_iff_forall_sectionOfObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MorphismSpaceInduced.lean, line 199. The attribute's comment: “the morphism of algebraic spaces determined by a 1-morphism, characterised on named sections”.

Stacks 04SW. A morphism g : X ⟶ Y of algebraic spaces is the one determined by a 1-morphism f : 𝒳 ⥤ 𝒴 over the site if and only if it carries the section of X named by every object z of 𝒳 to the section of Y named by f z.

This is the identification of Stacks 04SW stated as a property of a given morphism of algebraic spaces: it is what pins a morphism of algebraic spaces appearing as a free parameter against a 1-morphism appearing as another, which is the compatibility a statement about "the induced morphism of algebraic spaces" presupposes. The right-hand condition is the recipe of the source — an object of 𝒳 over U is a section of X over U, and f of it is a section of Y over U — and the left-hand side is AlgebraicGeometry.Space.inducedSpacesHom, the morphism of algebraic spaces that recipe defines.

The hypotheses are those of the source: X and Y are algebraic spaces, and eF, eG are the equivalences over the site exhibiting 𝒳 and 𝒴 as representable by them. Being equivalent over the site to a category of elements already makes p and q fibred in groupoids, so no such hypothesis is carried.

theorem eq_inducedSpacesHom_iff_forall_sectionOfObj
    (eF : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (X.1 ⋙ typeToCat)).p)
    (eG : StacksRepresentableCFG.EquivalenceOver q
      (presheafOfCategories (Y.1 ⋙ typeToCat)).p)
    (f : 𝒳 ⥤ 𝒴) (hf : f ⋙ q = p) (g : X ⟶ Y) :
    g = inducedSpacesHom B S hS p q eF eG f hf ↔
      ∀ (z : 𝒳) (W : BigFppfOver B S hS) (h : p.obj z = W),
        g.hom.app (op W) (PresheafOfCategories.sectionOfObj eF z h) =
          PresheafOfCategories.sectionOfObj eG (f.obj z)
            ((Functor.congr_obj hf z).trans h)

AlgebraicGeometry.Stack.morphismSpaceEquiv_eq_inducedSpaceMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MorphismSpaceInduced.lean, line 241. The attribute's comment: “the bijection is the morphism of representing presheaves induced by the 1-morphism”.

Stacks 04SW. The bijection of morphism spaces takes the 2-isomorphism class of a 1-morphism Φ : 𝒳 ⥤ 𝒴 over the site to the morphism of representing presheaves that Φ induces: the section of G attached to a section of F is the one named by the image under Φ of the object naming it.

So the abstract identification AlgebraicGeometry.Stack.morphismSpaceEquiv and the explicit construction AlgebraicGeometry.Space.inducedSpaceMap of Stacks 0GQA are the same map, and a compatibility expressed through the latter — as AlgebraicGeometry.Space.eq_inducedSpacesHom_iff_forall_sectionOfObj expresses it — is a compatibility with the former.

Both sides are computed on named sections: the left by AlgebraicGeometry.Stack.morphismSpaceEquiv_app_sectionOfObj, the right by AlgebraicGeometry.Space.inducedSpaceMap_app_sectionOfObj, and a morphism of representing presheaves is determined by those values.

theorem morphismSpaceEquiv_eq_inducedSpaceMap
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, w} (BigFppfOver B S hS))
    (F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (eX : StacksRepresentableCFG.EquivalenceOver
      𝒳.val.p (presheafOfCategories (F ⋙ typeToCat)).p)
    (eY : StacksRepresentableCFG.EquivalenceOver
      𝒴.val.p (presheafOfCategories (G ⋙ typeToCat)).p)
    (Φ : {H : 𝒳.val.obj ⥤ 𝒴.val.obj // H ⋙ 𝒴.val.p = 𝒳.val.p}) :
    morphismSpaceEquiv B S hS 𝒳 𝒴 F G eX eY (Quotient.mk _ Φ) =
      Space.inducedSpaceMap B S hS F G 𝒳.val.p 𝒴.val.p eX eY Φ.1 Φ.2

AlgebraicGeometry.Stack.morphismSpaceEquiv_app_sectionOfObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MorphismSpaceSections.lean, line 68. The attribute's comment: “value of the induced morphism on a named section”.

Stacks 04SW. The morphism F ⟶ G of representing presheaves induced by a 1-morphism Φ over the site carries the section of F named by an object z of 𝒳 to the section of G named by Φ z.

theorem morphismSpaceEquiv_app_sectionOfObj
    (Φ : {H : 𝒳.val.obj ⥤ 𝒴.val.obj // H ⋙ 𝒴.val.p = 𝒳.val.p})
    (z : 𝒳.val.obj) {W : BigFppfOver B S hS} (h : 𝒳.val.p.obj z = W) :
    (morphismSpaceEquiv B S hS 𝒳 𝒴 F G eX eY (Quotient.mk _ Φ)).app (op W)
        (PresheafOfCategories.sectionOfObj eX z h) =
      PresheafOfCategories.sectionOfObj eY (Φ.1.obj z) ((Functor.congr_obj Φ.2 z).trans h)
Sources
LeanAlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpace · AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isRepresentableCFG · AlgebraicGeometry.isRepresentableByAlgebraicSpace_iff · AlgebraicGeometry.Stack.morphismSpaceEquiv · AlgebraicGeometry.Stack.existsUnique_twoIso_of_morphismSpaceEquiv_eq · AlgebraicGeometry.Stack.morphismSpaceEquiv_map · AlgebraicGeometry.Space.eq_inducedSpacesHom_iff_forall_sectionOfObj · AlgebraicGeometry.Stack.morphismSpaceEquiv_eq_inducedSpaceMap

Section94.9 Morphisms representable by algebraic spaces#

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

Tag 02ZW, a definition

Tag 02ZW in the Stacks Project.

AlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpaces, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Representability.lean, line 80.

Stacks 02ZW. A 1-morphism of categories over the big fppf site of S is representable by algebraic spaces if, for every scheme U over S and every scheme-valued point y : (Sch/U)_{fppf} ⟶ 𝒴 of its target, the first projection of the 2-fibre product (Sch/U)_{fppf} ×_𝒴 𝒳 ⟶ (Sch/U)_{fppf} is equivalent, over the big fppf site of U, to the category of elements of the sheaf of points of an algebraic space over U.

abbrev IsRepresentableByAlgebraicSpaces
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : BasedCategory.{v₁, w₁} (BigFppfOver B S hS)}
    {𝒴 : BasedCategory.{v₂, w₂} (BigFppfOver B S hS)}
    (f : 𝒳 ⥤ᵇ 𝒴) : Prop
Tag 0402, an equation

Tag 0402 in the Stacks Project.

AlgebraicGeometry.Stack.exists_algebraicSpace_over_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/BaseChangeAlgebraicSpace.lean, line 43.

The algebraic space representing the 2-fibre product of a 1-morphism representable by algebraic spaces with a scheme-valued point y of its target, viewed over the original base, comes with its canonical morphism to U. The representing equivalence is over the big fppf category of U.

theorem exists_algebraicSpace_over_baseChange
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w}
      (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (hf : Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (U : BigFppfOver B S hS)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
    (hy : y ⋙ 𝒴.val.p = Over.map U.hom) :
    ∃ (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B U.left.1 U.left.2 F)
      (Fy : SpacesOverSmallerBase B U.left.1 S U.left.2 hS U.hom),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.p 𝒴.val.p y
          (CatFiberedInGroupoids.homFunctor f))
        (presheafOfCategories (F ⋙ typeToCat)).p) ∧
      Fy = (spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩ ∧
      ∃ (ι : Fy.1.left ≅ (OverShriek.relocalizePresheafFunctor U.hom).obj F),
        ∀ (W : BigFppfOver B S hS) (s : Fy.1.left.obj (op W)),
          (Fy.1.hom.app (op W) s).left = (ι.hom.app (op W) s).1.1

AlgebraicGeometry.Stack.baseChangeSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/BaseChangeSpace.lean, line 99. The attribute's comment: “the representing algebraic space F_y”.

Stacks 0402. The algebraic space F_y over U representing the 2-fibre product (Sch/U)_fppf ×_{y, 𝒴} 𝒳 of a 1-morphism f representable by algebraic spaces along a point y of its target over U.

This is a choice of representative; see the implementation notes.

noncomputable def baseChangeSpace : AlgebraicSpaces B U.left.1 U.left.2

AlgebraicGeometry.Stack.nonempty_equivalenceOver_baseChangeSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/BaseChangeSpace.lean, line 106. The attribute's comment: “F_y represents the 2-fibre product”.

Stacks 0402, the squiggly arrow. The category of elements of AlgebraicGeometry.Stack.baseChangeSpace is equivalent, over the big fppf site of U, to the first projection of the 2-fibre product (Sch/U)_fppf ×_{y, 𝒴} 𝒳.

theorem nonempty_equivalenceOver_baseChangeSpace :
    Nonempty (StacksRepresentableCFG.EquivalenceOver
      (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.p 𝒴.p y f.toFunctor)
      (presheafOfCategories ((baseChangeSpace B S hS f hf U y hy).1 ⋙ typeToCat)).p)

AlgebraicGeometry.Stack.baseChangeStructureMap, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/BaseChangeSpace.lean, line 124. The attribute's comment: “the structure morphism f_y”.

Stacks 0402. The structure morphism f_y : F_y ⟶ U of the display, as a morphism of algebraic spaces over S from AlgebraicGeometry.Stack.baseChangeSpace to the representable algebraic space of U.

noncomputable abbrev baseChangeStructureMap :
    (⟨(baseChangeSpaceOverBase B S hS f hf U y hy).1.left,
      (baseChangeSpaceOverBase B S hS f hf U y hy).property⟩ : AlgebraicSpaces B S hS) ⟶
      (schemeSpace (Over.mk U.hom) :
        AlgebraicSpaces B S hS)
Tag 02ZY, a lemma

Tag 02ZY in the Stacks Project.

AlgebraicGeometry.isRepresentableByAlgebraicSpaces_iff_associatedMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Algebraic/MorphismRepresentableBySpaces/Criterion.lean, line 756.

Stacks 02ZY. A morphism of categories fibred in groupoids is representable by algebraic spaces if and only if its functors on fibres are faithful and, for every object of the target over a scheme, the associated presheaf of pairs is an algebraic space over that scheme.

public theorem isRepresentableByAlgebraicSpaces_iff_associatedMap
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w}
      (AlgebraicGeometry.BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (c : 𝒴.val.p.ChoiceOfPullbacks) :
    AlgebraicGeometry.IsRepresentableByAlgebraicSpaces B S hS f.hom ↔
      ((∀ U : AlgebraicGeometry.BigFppfOver B S hS,
        (Stacks.RepresentableMorphism.inducedFiberFunctor 𝒳.val.p 𝒴.val.p
          (CatFiberedInGroupoids.homFunctor f)
          (CatFiberedInGroupoids.homFunctor_comp_p f) U).Faithful) ∧
        (∀ (U : AlgebraicGeometry.BigFppfOver B S hS) (y : 𝒴.val.p.Fiber U),
          IsAlgebraicSpacePairIsoClassPresheaf B S hS f c U y))
Tag 0457, a lemma

Tag 0457 in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_iff_of_equivalences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentabilityInvariance.lean, line 93.

Representability by algebraic spaces of a morphism of categories fibred in groupoids is invariant under horizontal equivalences in a 2-commutative square.

theorem isRepresentableByAlgebraicSpaces_iff_of_equivalences
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳' : CatFiberedInGroupoids.{u, v₁, u + 1, w₁}
      (BigFppfOver B S hS)}
    {𝒳 : CatFiberedInGroupoids.{u, v₂, u + 1, w₂}
      (BigFppfOver B S hS)}
    {𝒴' : CatFiberedInGroupoids.{u, v₃, u + 1, w₃}
      (BigFppfOver B S hS)}
    {𝒴 : CatFiberedInGroupoids.{u, v₄, u + 1, w₄}
      (BigFppfOver B S hS)}
    (f' : 𝒳'.val ⥤ᵇ 𝒴'.val) (f : 𝒳.val ⥤ᵇ 𝒴.val)
    (a : 𝒳'.val ⥤ᵇ 𝒳.val) (b : 𝒴'.val ⥤ᵇ 𝒴.val)
    (α : BasedFunctor.comp a f ≅ BasedFunctor.comp f' b)
    [Functor.IsEquivalence a.toFunctor]
    [Functor.IsEquivalence b.toFunctor] :
    IsRepresentableByAlgebraicSpaces B S hS f ↔
      IsRepresentableByAlgebraicSpaces B S hS f'
Tag 02ZZ, a lemma

Tag 02ZZ in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_of_isRepresentableByAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicSpaceStack.lean, line 213.

Stacks 02ZZ. A 1-morphism of categories fibred in groupoids over the big fppf site of S whose source and target are both representable by algebraic spaces over S is representable by algebraic spaces.

Both source and target are transported to categories of elements, where AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_fibredCategory applies: the source by AlgebraicGeometry.Stack.nonempty_equivalenceOver_fst_of_equivalence_source, the target by Stacks 0457.

theorem isRepresentableByAlgebraicSpaces_of_isRepresentableByAlgebraicSpace
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴)
    (h𝒳 : IsRepresentableByAlgebraicSpace B S hS 𝒳)
    (h𝒴 : IsRepresentableByAlgebraicSpace B S hS 𝒴) :
    IsRepresentableByAlgebraicSpaces B S hS f.hom
Tag 0458, a lemma

Tag 0458 in the Stacks Project.

AlgebraicGeometry.Stack.associatedMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresheafFibredCategory.lean, line 65. The attribute's comment: “associated morphism”.

The 1-morphism of categories fibred in groupoids induced by a map a of set-valued presheaves, together with its value on objects: it sends (U, x) to (U, a_U(x)).

def associatedMap
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) :
    {f : fibredCategory B S hS F ⟶ fibredCategory B S hS G //
      ∀ x : (fibredCategory B S hS F).val.obj,
      HEq ((CatFiberedInGroupoids.homFunctor f).obj x).fiber
          (Discrete.mk (a.app (Opposite.op x.base)
            (Discrete.as (show Discrete (F.obj (Opposite.op x.base)) from x.fiber))))}

AlgebraicGeometry.Stack.associatedMap_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresheafFibredCategory.lean, line 99. The attribute's comment: “the associated morphism on objects”.

The 1-morphism attached to a map a : F ⟶ G of set-valued presheaves sends the pair (U, x) to the pair (U, a_U(x)).

theorem associatedMap_obj
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G)
    (x : (fibredCategory B S hS F).val.obj) :
    (associatedMap B S hS a).1.hom.obj x =
      ⟨x.base, Discrete.mk (a.app (Opposite.op x.base) x.fiber.as)⟩

AlgebraicGeometry.Stack.associatedMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresheafFibredCategory.lean, line 174. The attribute's comment: “functoriality of the associated morphism”.

The 1-morphism attached to a composite of maps of presheaves is the composite of the two attached 1-morphisms.

theorem associatedMap_comp {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) (b : G ⟶ H) :
    (associatedMap B S hS (a ≫ b)).1 =
      (associatedMap B S hS a).1 ≫ (associatedMap B S hS b).1

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_iff_associatedMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresheafRepresentability.lean, line 146. The attribute's comment: “representability equivalence”.

Stacks 0458, representability equivalence. A map a : F ⟶ G of set-valued presheaves on the big fppf site of S is representable by algebraic spaces exactly when the 1-morphism of categories fibred in groupoids it induces, AlgebraicGeometry.Stack.associatedMap, is.

A scheme-valued point of the category of elements of G over a scheme U over S and a section of G over U naming the same family of elements have the same base change of a: the presheaf representing the base change of the 1-morphism along the point is the fibre of a over the section, and the relocalization of that fibre along the structure morphism of U is the base change of a along the section.

theorem isRepresentableByAlgebraicSpaces_iff_associatedMap
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) :
    Space.IsRepresentableByAlgebraicSpaces B S hS a ↔
      IsRepresentableByAlgebraicSpaces B S hS (associatedMap B S hS a).1.hom
Tag 04SY, a lemma

Tag 04SY in the Stacks Project.

AlgebraicGeometry.Stack.isoClassMap_isRepresentableByAlgebraicSpaces_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SetoidRepresentability.lean, line 256.

For categories fibred in setoids, representability by algebraic spaces of the induced map of isomorphism-class presheaves is equivalent to representability of the original morphism.

public theorem isoClassMap_isRepresentableByAlgebraicSpaces_iff
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInSetoids.{u, v, u + 1, u}
      (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (a : 𝒳.val.p.isoClassPresheaf ⟶ 𝒴.val.p.isoClassPresheaf)
    (ha : ∀ (U : BigFppfOver B S hS) (x : 𝒳.val.p.Fiber U),
      a.app (Opposite.op U) (Functor.isoClassMk 𝒳.val.p x) =
        Functor.isoClassMk 𝒴.val.p
          ((Functor.Fiber.mapOfComp 𝒳.val.p 𝒴.val.p
            (CatFiberedInGroupoids.homFunctor f)
            (CatFiberedInGroupoids.homFunctor_comp_p f) U).obj x)) :
    AlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces B S hS
        a ↔
      AlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpaces B S hS
        (CatFiberedInSetoids.inclusion.map f).hom
Tag 0302, a lemma

Tag 0302 in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_twoFibreProductFst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/BaseChangeRepresentableBySpace.lean, line 91.

If f : 𝒳 ⟶ 𝒴 is a 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces and g : 𝒵 ⟶ 𝒴 is any 1-morphism, then the base change 𝒵 ×_{g, 𝒴, f} 𝒳 ⟶ 𝒵 is representable by algebraic spaces. No relation is assumed between the universes of the three categories.

theorem isRepresentableByAlgebraicSpaces_twoFibreProductFst
    (𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS))
    (𝒵 : CatFiberedInGroupoids.{u, v₁, u + 1, w₁} (BigFppfOver B S hS))
    (𝒳 : CatFiberedInGroupoids.{u, v₂, u + 1, w₂} (BigFppfOver B S hS))
    (g : 𝒵.val ⥤ᵇ 𝒴.val) (f : 𝒳.val ⥤ᵇ 𝒴.val)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f) :
    IsRepresentableByAlgebraicSpaces B S hS (twoFibreProductFst B S hS 𝒴 𝒵 𝒳 g f)
Tag 0300, a lemma

Tag 0300 in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/BaseChangeRepresentableBySpace.lean, line 110.

Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces, let g : 𝒵 ⟶ 𝒴 be any 1-morphism, and assume 𝒵 is represented by an algebraic space over S. Then the 2-fibre product 𝒵 ×_𝒴 𝒳 is represented by an algebraic space over S.

theorem isRepresentableByAlgebraicSpace_twoFibreProduct
    (𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS))
    (𝒵 : CatFiberedInGroupoids.{u, v₁, u + 1, w₁} (BigFppfOver B S hS))
    (𝒳 : CatFiberedInGroupoids.{u, v₂, u + 1, w₂} (BigFppfOver B S hS))
    (g : 𝒵.val ⥤ᵇ 𝒴.val) (f : 𝒳.val ⥤ᵇ 𝒴.val)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f)
    (h𝒵 : IsRepresentableByAlgebraicSpace B S hS 𝒵) :
    IsRepresentableByAlgebraicSpace B S hS (twoFibreProduct B S hS 𝒴 𝒵 𝒳 g f)
Tag 0301, a lemma

Tag 0301 in the Stacks Project.

AlgebraicGeometry.isRepresentableByAlgebraicSpaces_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentabilityComp.lean, line 332.

The composition of two morphisms representable by algebraic spaces is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, v, u + 1, w}
      (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hg : IsRepresentableByAlgebraicSpaces B S hS g.hom) :
    IsRepresentableByAlgebraicSpaces B S hS (f ≫ g).hom
Tag 0303, a lemma

Tag 0303 in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_productMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ProductMorphism.lean, line 360.

Stacks 0303. The product f₁ × f₂ of two 1-morphisms of categories fibred in groupoids over the big fppf site of S, each representable by algebraic spaces, is representable by algebraic spaces.

It factors as (id_{𝒴₁} × f₂) ∘ (f₁ × id_{𝒳₂}), each factor is representable by AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_productMap_id_left resp. …_id_right, and the composite is representable by Stacks 0301.

theorem isRepresentableByAlgebraicSpaces_productMap (f₁ : 𝒳₁ ⟶ 𝒴₁) (f₂ : 𝒳₂ ⟶ 𝒴₂)
    (hf₁ : IsRepresentableByAlgebraicSpaces B S hS f₁.hom)
    (hf₂ : IsRepresentableByAlgebraicSpaces B S hS f₂.hom) :
    IsRepresentableByAlgebraicSpaces B S hS (productMap f₁ f₂).hom
Tag 0CKY, a lemma

Tag 0CKY in the Stacks Project.

AlgebraicGeometry.Stack.isStack_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableMorphismStack.lean, line 842.

Stacks 0CKY. Let 𝒳 ⟶ 𝒵 and 𝒴 ⟶ 𝒵 be 1-morphisms of categories fibred in groupoids over the big fppf site of S. If 𝒳 ⟶ 𝒵 is representable by algebraic spaces and 𝒴 is a stack in groupoids, then the 2-fibre product 𝒳 ×_𝒵 𝒴 is a stack in groupoids.

theorem isStack_of_isTwoFibreProduct
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, max u v, u + 1, max (max (u + 1) w) v}
      (AlgebraicGeometry.BigFppfOver B S hS))
    (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵)
    (P : Bicategory.TwoCommSq f g)
    (hP : Bicategory.IsTwoFibreProduct P)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (h𝒴 : 𝒴.val.p.IsStack (AlgebraicGeometry.BigFppfOver.topology B S hS)) :
    P.pt.val.p.IsStack (AlgebraicGeometry.BigFppfOver.topology B S hS)
Sources
LeanAlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpaces · AlgebraicGeometry.Stack.exists_algebraicSpace_over_baseChange · AlgebraicGeometry.Stack.baseChangeSpace · AlgebraicGeometry.Stack.nonempty_equivalenceOver_baseChangeSpace · AlgebraicGeometry.Stack.baseChangeStructureMap · AlgebraicGeometry.isRepresentableByAlgebraicSpaces_iff_associatedMap · AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_iff_of_equivalences · AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_of_isRepresentableByAlgebraicSpace

Section94.10 Properties of morphisms representable by algebraic spaces#

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

Tag 03YJ, the section

Tag 03YJ in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_schemePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemePointRelativeProperty.lean, line 82. The attribute's comment: “in the situation of Lemma 045G, every 1-morphism x : (Sch/U)_fppf -> X is representable by algebraic spaces, so that saying x has P makes sense”.

Stacks, Section 03YJ. If the diagonal of a category fibred in groupoids 𝒳 over the big fppf site of S is representable by algebraic spaces, then every 1-morphism x : (Sch/U)_fppf → 𝒳 from the category represented by a scheme U over S is representable by algebraic spaces. This is condition (3) of Stacks 045G obtained from condition (1).

theorem isRepresentableByAlgebraicSpaces_schemePoint
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : HasRepresentableDiagonal B S hS 𝒳) {U : BigFppfOver B S hS}
    (x : schemeFibredCategory B S hS U ⟶ 𝒳) :
    IsRepresentableByAlgebraicSpaces B S hS x.hom

AlgebraicGeometry.Stack.SchemePointHasRelativeProperty, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemePointRelativeProperty.lean, line 98. The attribute's comment: “for X as in Lemma 045G and P as in Definition 03YK, the property that a 1-morphism x : (Sch/U)_fppf -> X has P”.

Stacks, Section 03YJ. Let 𝒳 be a category fibred in groupoids over the big fppf site of S whose diagonal is representable by algebraic spaces, and let 𝒫 be a property of morphisms of algebraic spaces as in Definition 03YK. A 1-morphism x : (Sch/U)_fppf → 𝒳 from the category represented by a scheme U over S has 𝒫 when it has 𝒫 in the sense of Stacks 03YK; it is representable by algebraic spaces by AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_schemePoint.

abbrev SchemePointHasRelativeProperty
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : HasRepresentableDiagonal B S hS 𝒳) {U : BigFppfOver B S hS}
    (x : schemeFibredCategory B S hS U ⟶ 𝒳) : Prop

AlgebraicGeometry.Stack.surjective_smooth_etale_relativePropertyHypotheses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemePointRelativeProperty.lean, line 111. The attribute's comment: “surjective, smooth and etale are properties as in Definition 03YK”.

Stacks, Section 03YJ. Surjectivity, smoothness and étaleness of morphisms of algebraic spaces over S are each properties as in Definition 03YK: each is stable under base change and local on the base for the fppf topology (Stacks 041Q, 0429 and 042B).

theorem surjective_smooth_etale_relativePropertyHypotheses :
    ((Space.surjectiveMorphismProperty B S hS).IsStableUnderBaseChange ∧
        (Space.surjectiveMorphismProperty B S hS).IsLocalAtTarget
          (Space.Topology.fppf.precoverage.{u, v} B S hS)) ∧
      ((Space.smoothMorphismProperty B S hS).IsStableUnderBaseChange ∧
        (Space.smoothMorphismProperty B S hS).IsLocalAtTarget
          (Space.Topology.fppf.precoverage.{u, v} B S hS)) ∧
      ((Space.etaleMorphisms B S hS).IsStableUnderBaseChange ∧
        (Space.etaleMorphisms B S hS).IsLocalAtTarget
          (Space.Topology.fppf.precoverage.{u, v} B S hS))
Tag 03YK, a definition

Tag 03YK in the Stacks Project.

AlgebraicGeometry.Stack.HasRelativeProperty, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeProperty.lean, line 51.

A 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces has the property P when every algebraic space representing its base change along a scheme-valued point of the target has structural morphism with P, read as a morphism of algebraic spaces over S.

abbrev HasRelativeProperty
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴) (_hf : IsRepresentableByAlgebraicSpaces B S hS f.hom) :
    Prop
Tag 0459, a lemma

Tag 0459 in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_iff_of_equivalences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyEquivalence.lean, line 78. The attribute's comment: “a vertical 1-morphism of a 2-commutative square whose horizontals are equivalences has the relative property exactly when the other vertical one does”.

In a 2-commutative square of categories fibred in groupoids over the big fppf site of S whose two horizontal 1-morphisms are equivalences, a vertical 1-morphism representable by algebraic spaces has the relative property P of Stacks 03YK if and only if the other vertical 1-morphism does. Representability of f' is deduced from that of f.

theorem hasRelativeProperty_iff_of_equivalences
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    (f' : 𝒳' ⟶ 𝒴') (f : 𝒳 ⟶ 𝒴)
    (a : 𝒳'.val ⥤ᵇ 𝒳.val) (b : 𝒴'.val ⥤ᵇ 𝒴.val)
    (α : BasedFunctor.comp a f.hom ≅ BasedFunctor.comp f'.hom b)
    [Functor.IsEquivalence a.toFunctor] [Functor.IsEquivalence b.toFunctor]
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom) :
    HasRelativeProperty.{u, v₂, w₂} B S hS P f hf ↔
      HasRelativeProperty.{u, v₁, w₁} B S hS P f'
        ((isRepresentableByAlgebraicSpaces_iff_of_equivalences B S hS f'.hom f.hom a b α).mp
          hf)

AlgebraicGeometry.Stack.hasRelativeProperty_iff_of_equivalences', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyEquivalenceIff.lean, line 182. The attribute's comment: “the same biconditional assembled from the two one-directional statements”.

Stacks 0459. In a 2-commutative square of categories fibred in groupoids over the big fppf site of S whose two horizontal 1-morphisms are equivalences, a vertical 1-morphism representable by algebraic spaces has the relative property at P of Stacks 03YK exactly when the other one does.

The forward direction is AlgebraicGeometry.Stack.hasRelativeProperty_of_equivalences and the reverse one AlgebraicGeometry.Stack.relativeProperty_of_equivalences_symm; neither uses any hypothesis on P, which is carried only because the statement mentions the abbreviation.

The representability witness for f' is an arbitrary one, which is what distinguishes this from AlgebraicGeometry.Stack.hasRelativeProperty_iff_of_equivalences of StacksFrontier.AlgebraicGeometry.Stacks.RelativePropertyEquivalence: that form reads the witness for f' off the one for f through Stacks 0457, and is the special case of this one at that witness.

theorem hasRelativeProperty_iff_of_equivalences' (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    (f' : 𝒳' ⟶ 𝒴') (f : 𝒳 ⟶ 𝒴)
    (a : 𝒳'.val ⥤ᵇ 𝒳.val) (b : 𝒴'.val ⥤ᵇ 𝒴.val)
    (α : BasedFunctor.comp a f.hom ≅ BasedFunctor.comp f'.hom b)
    [Functor.IsEquivalence a.toFunctor] [Functor.IsEquivalence b.toFunctor]
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hf' : IsRepresentableByAlgebraicSpaces B S hS f'.hom) :
    HasRelativeProperty.{u, v₂, w₂} B S hS P f hf ↔
      HasRelativeProperty.{u, v₁, w₁} B S hS P f' hf'
Tag 045A, a lemma

Tag 045A in the Stacks Project.

AlgebraicGeometry.Stack.holdsOnEverySchemePoint_iff_hasRelativeProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresheafRepresentability.lean, line 183.

Stacks 045A. Let P be a property of morphisms of algebraic spaces over S which is stable under base change and local on the target for the fppf precoverage. A map a : F ⟶ G of presheaves on the big fppf site of S which is representable by algebraic spaces has P in the sense of Stacks 03XZ exactly when the 1-morphism of categories fibred in groupoids attached to it by Stacks 0458 has the relative property P of Stacks 03YK.

theorem holdsOnEverySchemePoint_iff_hasRelativeProperty
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G)
    (ha : Space.IsRepresentableByAlgebraicSpaces B S hS a) :
    Space.HasProperty B S hS P a ha ↔
      HasRelativeProperty B S hS P (associatedMap B S hS a).1
        ((isRepresentableByAlgebraicSpaces_iff_associatedMap B S hS a).1 ha)
Tag 04TC, a lemma

Tag 04TC in the Stacks Project.

AlgebraicGeometry.Stack.isoClassMap_holdsOnEverySchemePoint_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SetoidRelativeProperty.lean, line 55.

Stacks 04TC. For a 1-morphism f of categories fibred in setoids over the big fppf site of S whose induced map a of isomorphism-class presheaves is representable by algebraic spaces, a has a property P in the sense of Stacks 03XZ exactly when f has P in the relative sense of Stacks 03YK.

theorem isoClassMap_holdsOnEverySchemePoint_iff
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    {𝒳 𝒴 : CatFiberedInSetoids.{u, v, u + 1, u} (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (a : 𝒳.val.p.isoClassPresheaf ⟶ 𝒴.val.p.isoClassPresheaf)
    (ha : ∀ (U : BigFppfOver B S hS) (x : 𝒳.val.p.Fiber U),
      a.app (Opposite.op U) (Functor.isoClassMk 𝒳.val.p x) =
        Functor.isoClassMk 𝒴.val.p
          ((Functor.Fiber.mapOfComp 𝒳.val.p 𝒴.val.p
            (CatFiberedInGroupoids.homFunctor f)
            (CatFiberedInGroupoids.homFunctor_comp_p f) U).obj x))
    (hf : IsRepresentableByAlgebraicSpaces B S hS
      (CatFiberedInSetoids.inclusion.map f).hom) :
    Space.HasProperty B S hS P a
        ((isoClassMap_isRepresentableByAlgebraicSpaces_iff B S hS f a ha).mpr hf) ↔
      HasRelativeProperty B S hS P (CatFiberedInSetoids.inclusion.map f) hf
Tag 045B, a lemma

Tag 045B in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyComp.lean, line 301.

Stacks 045B. Let P be a property of morphisms of algebraic spaces over S which is stable under base change, local on the target for the fppf precoverage, and stable under composition. If two composable 1-morphisms of categories fibred in groupoids over the big fppf site of S are representable by algebraic spaces and have the relative property P of Stacks 03YK, then so does their composite.

theorem hasRelativeProperty_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage.{u, t} B S hS)]
    [P.IsStableUnderComposition]
    {𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hg : IsRepresentableByAlgebraicSpaces B S hS g.hom)
    (hPf : HasRelativeProperty B S hS P f hf)
    (hPg : HasRelativeProperty B S hS P g hg) :
    HasRelativeProperty B S hS P (f ≫ g)
      (isRepresentableByAlgebraicSpaces_comp B S hS f g hf hg)
Tag 045C, a lemma

Tag 045C in the Stacks Project.

AlgebraicGeometry.Stack.isImmersion_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionBaseChange.lean, line 67. The attribute's comment: “the immersion property of Stacks 04XB, for the first projection”.

Stacks 045C at the immersion property of Stacks 04XB. In a 2-fibre product square over a cospan g : 𝒵 ⟶ 𝒴, f : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf site of S, the projection to 𝒵 is an immersion as soon as f is.

theorem isImmersion_baseChange
    (𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, max u v, u + 1, max (max (u + 1) w) v}
      (BigFppfOver B S hS))
    (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (R : Bicategory.TwoCommSq g f) (hR : Bicategory.IsTwoFibreProduct R)
    (hf : Stack.IsImmersion B S hS f) :
    Stack.IsImmersion B S hS R.fst

AlgebraicGeometry.Stack.isImmersion_twoFibreProductSnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionBaseChange.lean, line 83. The attribute's comment: “the immersion property of Stacks 04XB, for the canonical second projection”.

Stacks 045C at the immersion property, for the second projection. The second projection of the canonical 2-fibre product square over a cospan (g, f) of categories fibred in groupoids is an immersion as soon as g is.

theorem isImmersion_twoFibreProductSnd
    {𝒵 𝒴 𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (g : 𝒵 ⟶ 𝒴) (f : 𝒳 ⟶ 𝒴) (hg : Stack.IsImmersion B S hS g) :
    Stack.IsImmersion B S hS
      (CatFiberedInGroupoids.twoFibreProductSquare.{u, u, u + 1, u + 1} g f).snd

AlgebraicGeometry.Stack.isImmersion_snd_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionBaseChange.lean, line 110. The attribute's comment: “the immersion property of Stacks 04XB, at a 2-fibre product of algebraic stacks”.

Stacks 045C at the immersion property, for the second projection of a 2-fibre product square of algebraic stacks. If g : 𝒵 ⟶ 𝒴 is an immersion in the sense of Stacks 04XB and P is a 2-fibre product of the cospan (g, f) in the 2-category of algebraic stacks, then so is P.snd : P.pt ⟶ 𝒳.

The statement is obtained at the canonical square — where the stronger terminality hypothesis of Stacks 045C holds unconditionally — and transported to P along the comparison 1-morphism by Stacks 0457 for the relative property.

theorem isImmersion_snd_of_isTwoFibreProduct
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hg : Stack.IsImmersion B S hS g.hom) :
    Stack.IsImmersion B S hS P.snd.hom

AlgebraicGeometry.Stack.AlgebraicStacks.isImmersion_snd_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ImmersionBaseChange.lean, line 143. The attribute's comment: “the immersion property of Stacks 04XB, conjoined with representability, at a 2-fibre product of algebraic stacks”.

Base change of an immersion of algebraic stacks. If g : 𝒵 ⟶ 𝒴 is an immersion of algebraic stacks over S and P is a 2-fibre product of the cospan (g, f) in the 2-category of algebraic stacks, then P.snd : P.pt ⟶ 𝒳 is an immersion of algebraic stacks.

Both halves are base-change statements: representability by algebraic spaces is Stacks 0302 and the immersion property of Stacks 04XB is Stacks 045C. The attribute records the latter, at the level of algebraic stacks. It deliberately does not record Stacks 04YL: that tag is a definition — its three parts define open immersions, closed immersions and immersions in terms of Section 04XB — and says nothing about stability under base change, so a theorem must not carry it. The definition itself is carried by AlgebraicStacks.IsImmersion.

theorem isImmersion_snd_of_isTwoFibreProduct
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hg : IsImmersion B S hS g) :
    IsImmersion B S hS P.snd

AlgebraicGeometry.Stack.hasRelativeProperty_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyBaseChange.lean, line 135.

Stacks 045C. Let P be a property of morphisms of algebraic spaces over S which is stable under base change and local on the target for the fppf precoverage. In a 2-fibre product square over a cospan g : 𝒵 ⟶ 𝒴, f : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf site of S, the projection to 𝒵 has the relative property P of Stacks 03YK as soon as f does.

theorem hasRelativeProperty_baseChange
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    (𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, max u v, u + 1, max (max (u + 1) w) v}
      (BigFppfOver B S hS))
    (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (R : Bicategory.TwoCommSq g f)
    (hR : Bicategory.IsTwoFibreProduct R)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hPf : HasRelativeProperty B S hS P f hf) :
    HasRelativeProperty B S hS P R.fst
      (isRepresentableByAlgebraicSpaces_baseChange.{u, v, w} B S hS 𝒳 𝒴 𝒵 f g R hR hf)
Tag 045D, a lemma

Tag 045D in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyDescent.lean, line 266.

Stacks 045D. Let P be a property of morphisms of algebraic spaces over S which is stable under base change and local on the target for the fppf precoverage, let f : 𝒳 ⟶ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf site of S representable by algebraic spaces and let g : 𝒵 ⟶ 𝒴 be any 1-morphism. Assume that every object of a fibre of 𝒴 becomes, after restriction to a covering sieve, isomorphic to the image of an object of 𝒵. Then in a 2-fibre product square over the cospan (g, f), if the projection to 𝒵 has the relative property P of Stacks 03YK, so does f.

This is AlgebraicGeometry.Stack.relativeProperty_of_baseChange with the representability of f assumed as the source assumes it, which is what names the relative property of Stacks 03YK on both sides.

theorem hasRelativeProperty_of_baseChange
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, max u v, u + 1, max (max (u + 1) w) v}
      (BigFppfOver B S hS))
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget (Space.Topology.fppf.precoverage.{u, max u t} B S hS)]
    (f : 𝒳 ⟶ 𝒴) (g : 𝒵 ⟶ 𝒴)
    (D : Bicategory.TwoCommSq g f)
    (hD : Bicategory.IsTwoFibreProduct D)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hg : ∀ (U : BigFppfOver B S hS) (y : 𝒴.val.p.Fiber U),
      ∃ R ∈ BigFppfOver.topology B S hS U,
        ∀ ⦃V : BigFppfOver B S hS⦄ ⦃k : V ⟶ U⦄, R.arrows k →
          ∃ z : 𝒵.val.obj, ∃ φ : (CatFiberedInGroupoids.homFunctor g).obj z ⟶ y.1,
            𝒴.val.p.IsHomLift k φ)
    (hP : HasRelativeProperty B S hS P D.fst
      (isRepresentableByAlgebraicSpaces_baseChange.{u, v, w} B S hS 𝒳 𝒴 𝒵 f g D hD hf)) :
    HasRelativeProperty B S hS P f hf
Tag 045E, a lemma

Tag 045E in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_productMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ProductRelativeProperty.lean, line 140.

Stacks 045E. A property of morphisms of algebraic spaces over S which is stable under base change, local on the target for the fppf precoverage and stable under composition, and which holds relatively for two 1-morphisms of categories fibred in groupoids over the big fppf site of S representable by algebraic spaces, holds relatively for their product.

The product factors as (f₁ × id_{𝒳₂}) ∘ (id_{𝒴₁} × f₂); the two factors are handled by AlgebraicGeometry.Stack.hasRelativeProperty_productMap_id_right and …_id_left, and the composite by Stacks 045B.

theorem hasRelativeProperty_productMap (f₁ : 𝒳₁ ⟶ 𝒴₁) (f₂ : 𝒳₂ ⟶ 𝒴₂)
    (hf₁ : IsRepresentableByAlgebraicSpaces B S hS f₁.hom)
    (hf₂ : IsRepresentableByAlgebraicSpaces B S hS f₂.hom)
    (hP₁ : HasRelativeProperty.{u, _, _, t} B S hS P f₁ hf₁)
    (hP₂ : HasRelativeProperty.{u, _, _, t} B S hS P f₂ hf₂) :
    HasRelativeProperty.{u, _, _, t} B S hS P (productMap f₁ f₂)
      (isRepresentableByAlgebraicSpaces_productMap B S hS f₁ f₂ hf₁ hf₂)
Tag 045F, a lemma

Tag 045F in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativePropertyMono.lean, line 58.

Stacks 045F. If a property P of morphisms of algebraic spaces over S implies a property P', then a 1-morphism of categories fibred in groupoids over (Sch/S)_fppf which is representable by algebraic spaces and has the relative property P of Stacks 03YK also has the relative property P'.

The relative property is a universally quantified statement in which the property occurs only in the conclusion, so the implication applies under the quantifiers.

theorem hasRelativeProperty_mono
    {P P' : MorphismProperty (AlgebraicSpaces B S hS)}
    [P.IsStableUnderBaseChange] [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    [P'.IsStableUnderBaseChange] [P'.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)]
    (hPP' : P ≤ P')
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} {f : 𝒳 ⟶ 𝒴}
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hP : HasRelativeProperty B S hS P f hf) :
    HasRelativeProperty B S hS P' f hf
Tag 05UK, a lemma

Tag 05UK in the Stacks Project.

AlgebraicGeometry.Stack.full_and_faithful_homFunctor_of_mono_representingMaps, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismFullyFaithful.lean, line 276.

Stacks 05UK, with Stacks 003Z: the implication (1) ⟹ (2) of Stacks 04ZZ. A 1-morphism j : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces and all of whose representing structural morphisms are monomorphisms has fully faithful underlying functor.

Faithfulness is Stacks 04Y5 and uses only representability. For fullness: a morphism of the fibre 𝒴_U out of j(a) makes a second object of the fibre of (Sch/U)_fppf ×_𝒴 𝒳 over the terminal object of (Sch/U)_fppf, next to the one given by a itself; the representing algebraic space has at most one section there because its structural morphism is injective on sections, so the two objects are isomorphic and the 𝒳-component of the isomorphism is the preimage sought.

theorem full_and_faithful_homFunctor_of_mono_representingMaps
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (j : 𝒳 ⟶ 𝒴)
    (hj : IsRepresentableByAlgebraicSpaces B S hS j.hom)
    (hmono : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
      (_hy : y ⋙ 𝒴.val.p = Over.map U.hom)
      (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.p 𝒴.val.p y
            (CatFiberedInGroupoids.homFunctor j))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Mono (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom) :
    (CatFiberedInGroupoids.homFunctor j).Full ∧
      (CatFiberedInGroupoids.homFunctor j).Faithful
Tag 045G, a lemma

Tag 045G in the Stacks Project.

AlgebraicGeometry.isRepresentableFromSchemes_iff_isRepresentableFromRepresentableCategories, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Algebraic/RepresentableDiagonal/SchemeAndRepresentableSources.lean, line 164. The attribute's comment: “parts (3) and (5)”.

Stacks 045G, conditions (3) and (5). For a category fibred in groupoids 𝒳 over the big fppf site of S, every 1-morphism to 𝒳 out of a slice of the site is representable by algebraic spaces if and only if every 1-morphism to 𝒳 out of a representable category fibred in groupoids is.

public theorem isRepresentableFromSchemes_iff_isRepresentableFromRepresentableCategories :
    IsRepresentableFromSchemes B S hS 𝒳 ↔
      IsRepresentableFromRepresentableCategories.{u, v, w, u, u + 1} B S hS 𝒳

AlgebraicGeometry.Stack.hasRepresentableDiagonal_iff_isAlgebraicSpaceIsomPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DiagonalCriteria.lean, line 42. The attribute's comment: “parts (1) and (2)”.

The diagonal of a category fibred in groupoids over the big fppf site of S is representable by algebraic spaces if and only if every isomorphism sheaf Isom(x, y) of two objects of a fibre is an algebraic space over the scheme the fibre sits over.

theorem hasRepresentableDiagonal_iff_isAlgebraicSpaceIsomPresheaf :
    HasRepresentableDiagonal B S hS 𝒳 ↔ IsAlgebraicSpaceIsomPresheaf B S hS 𝒳

AlgebraicGeometry.Stack.isRepresentableFromAlgebraicSpaces_iff_hasAlgebraicSpaceProducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DiagonalCriteriaAlgebraicSpaceProducts.lean, line 109. The attribute's comment: “parts (7) and (8)”.

Stacks 045G, the equivalence of conditions (7) and (8). Every 1-morphism to 𝒳 out of a category fibred in groupoids representable by an algebraic space over S is representable by algebraic spaces if and only if the 2-fibre product over 𝒳 of any two such 1-morphisms is representable by an algebraic space.

theorem isRepresentableFromAlgebraicSpaces_iff_hasAlgebraicSpaceProducts :
    IsRepresentableFromAlgebraicSpaces.{u, v, w, v₁, w₁} B S hS 𝒳 ↔
      HasAlgebraicSpaceProducts.{u, v, w, v₁, w₁, v₂, w₂} B S hS 𝒳

AlgebraicGeometry.Stack.hasAlgebraicSpaceRepresentableProducts_iff_isRepresentableFromAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DiagonalCriteriaAlgebraicSpaceSources.lean, line 207. The attribute's comment: “parts (6) and (7)”.

Stacks 045G, the equivalence of conditions (6) and (7). The 2-fibre product over 𝒳 of any two 1-morphisms out of representable categories fibred in groupoids is representable by an algebraic space if and only if every 1-morphism to 𝒳 out of a category fibred in groupoids representable by an algebraic space is representable by algebraic spaces.

theorem hasAlgebraicSpaceRepresentableProducts_iff_isRepresentableFromAlgebraicSpaces :
    HasAlgebraicSpaceRepresentableProducts.{u, v, w, v₁, w₁, v₂, w₂} B S hS 𝒳 ↔
      IsRepresentableFromAlgebraicSpaces.{u, v, w, v₁, w₁} B S hS 𝒳

AlgebraicGeometry.Stack.isAlgebraicSpaceIsomPresheaf_iff_isRepresentableFromSchemes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DiagonalCriteriaProductsToDiagonal.lean, line 434. The attribute's comment: “parts (2) and (3)”.

Stacks 045G, the equivalence of conditions (2) and (3). Every isomorphism sheaf Isom(x, y) of two objects of a fibre of 𝒳 is an algebraic space over the scheme the fibre sits over if and only if every 1-morphism to 𝒳 from the category represented by a scheme over S is representable by algebraic spaces.

theorem isAlgebraicSpaceIsomPresheaf_iff_isRepresentableFromSchemes :
    IsAlgebraicSpaceIsomPresheaf B S hS 𝒳 ↔ IsRepresentableFromSchemes B S hS 𝒳

AlgebraicGeometry.Stack.representableFromCategories_iff_algebraicSpaceProducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DiagonalCriteriaRepresentableProducts.lean, line 144. The attribute's comment: “parts (5) and (6)”.

Stacks 045G, the equivalence of conditions (5) and (6). Every 1-morphism to 𝒳 from a representable category fibred in groupoids is representable by algebraic spaces if and only if the 2-fibre product over 𝒳 of any two such 1-morphisms is representable by an algebraic space.

theorem representableFromCategories_iff_algebraicSpaceProducts :
    IsRepresentableFromRepresentableCategories.{u, v, w, v₁, w₁} B S hS 𝒳 ↔
      HasAlgebraicSpaceRepresentableProducts.{u, v, w, v₁, w₁, v₂, w₂} B S hS 𝒳

AlgebraicGeometry.Stack.hasAlgebraicSpaceSchemePointProducts_iff_isRepresentableFromRepresentableCategories, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DiagonalCriteriaRepresentableSources.lean, line 126. The attribute's comment: “parts (4) and (5)”.

Stacks 045G, the equivalence of conditions (4) and (5). The 2-fibre product over 𝒳 of any two scheme-valued points of 𝒳 is representable by an algebraic space if and only if every 1-morphism to 𝒳 from a representable category fibred in groupoids is representable by algebraic spaces.

theorem hasAlgebraicSpaceSchemePointProducts_iff_isRepresentableFromRepresentableCategories :
    HasAlgebraicSpaceSchemePointProducts B S hS 𝒳 ↔
      IsRepresentableFromRepresentableCategories.{u, v, w, v₁, w₁} B S hS 𝒳

AlgebraicGeometry.Stack.isRepresentableFromSchemes_iff_hasAlgebraicSpaceSchemePointProducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DiagonalCriteriaSchemePoints.lean, line 79. The attribute's comment: “parts (3) and (4)”.

Every 1-morphism to 𝒳 from the category represented by a scheme over S is representable by algebraic spaces if and only if the 2-fibre product over 𝒳 of any two such 1-morphisms is representable by an algebraic space.

theorem isRepresentableFromSchemes_iff_hasAlgebraicSpaceSchemePointProducts :
    IsRepresentableFromSchemes B S hS 𝒳 ↔ HasAlgebraicSpaceSchemePointProducts B S hS 𝒳
Sources
LeanAlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_schemePoint · AlgebraicGeometry.Stack.SchemePointHasRelativeProperty · AlgebraicGeometry.Stack.surjective_smooth_etale_relativePropertyHypotheses · AlgebraicGeometry.Stack.HasRelativeProperty · AlgebraicGeometry.Stack.hasRelativeProperty_iff_of_equivalences · AlgebraicGeometry.Stack.hasRelativeProperty_iff_of_equivalences' · AlgebraicGeometry.Stack.holdsOnEverySchemePoint_iff_hasRelativeProperty · AlgebraicGeometry.Stack.isoClassMap_holdsOnEverySchemePoint_iff

Section94.12 Algebraic stacks#

Section 94.12 of the Stacks Project, Tag 026N. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 026O, a definition

Tag 026O in the Stacks Project.

AlgebraicGeometry.Stack.IsAlgebraicStack, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicStack.lean, line 99.

Stacks 026O. A category over the big fppf site of S is an algebraic stack when it is fibred in groupoids, is a stack for the fppf topology, has a diagonal representable by algebraic spaces, and has a presentation by a scheme: a 1-morphism from the category represented by a scheme U over S, representable by algebraic spaces, which is surjective and smooth in the sense that every algebraic space representing its base change along a scheme-valued point of the stack has surjective and smooth structural morphism.

The stack clause is a conjunction of the two renderings of Stacks 02ZJ, the sieve-indexed CategoryTheory.Functor.IsStack of Stacks 026F and the family-indexed CategoryTheory.Functor.IsStackInGroupoids of Stacks 02ZI at the descent universe w. The second conjunct is a consequence of the first — see the implementation notes.

abbrev IsAlgebraicStack.{u, w, v, t}
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : BasedCategory.{v, t} (BigFppfOver B S hS)) : Prop
Tag 03YO, a definition

Tag 03YO in the Stacks Project.

AlgebraicGeometry.Stack.IsDeligneMumfordStack, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordStack.lean, line 73.

Stacks 03YO. An algebraic stack over S is a Deligne-Mumford stack when it admits a presentation by a scheme which is surjective and étale: a 1-morphism from the category represented by a scheme U over S, representable by algebraic spaces, such that every algebraic space representing its base change along a scheme-valued point of the stack has surjective and étale structural morphism.

abbrev IsDeligneMumfordStack.{u, w}
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : BasedCategory.{u, u + 1} (BigFppfOver B S hS)) : Prop
Tag 03YP, a definition

Tag 03YP in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicStack.lean, line 129.

Stacks 03YP. The 2-category of algebraic stacks over S: the full sub-2-category of the 2-category of categories fibred in groupoids over the big fppf site of S whose objects are the algebraic stacks. Its 1-morphisms and 2-morphisms are those of the ambient 2-category, with no further condition.

abbrev AlgebraicStacks.{u, w}
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
Tag 03YQ, a lemma

Tag 03YQ in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_iff_of_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicStackEquivalence.lean, line 143. The attribute's comment: “algebraic_stack_iff_of_equivalence”.

Two categories over the big fppf site of S which are equivalent as categories over that site are algebraic stacks at the same time.

theorem isAlgebraicStack_iff_of_equivalence
    {𝒳 𝒴 : BasedCategory.{v, t} (BigFppfOver B S hS)}
    (e : BasedCategory.Equivalence 𝒳 𝒴) :
    IsAlgebraicStack.{u, w} B S hS 𝒳 ↔ IsAlgebraicStack.{u, w} B S hS 𝒴

AlgebraicGeometry.Stack.isDeligneMumfordStack_iff_of_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicStackEquivalence.lean, line 191. The attribute's comment: “deligne_mumford_iff_of_equivalence”.

Two categories over the big fppf site of S which are equivalent as categories over that site are Deligne-Mumford stacks at the same time.

theorem isDeligneMumfordStack_iff_of_equivalence
    {𝒳 𝒴 : BasedCategory.{u, u + 1} (BigFppfOver B S hS)}
    (e : BasedCategory.Equivalence 𝒳 𝒴) :
    IsDeligneMumfordStack.{u, w} B S hS 𝒳 ↔ IsDeligneMumfordStack.{u, w} B S hS 𝒴

AlgebraicGeometry.Stack.isAlgebraicStack_iff_of_equivalence', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicStackEquivalenceInvariance.lean, line 89. The attribute's comment: “algebraic stacks”.

Stacks 03YQ, the algebraic-stack assertion. Two categories over the big fppf site of S which are equivalent as categories over the site are algebraic stacks at the same time.

Stated for categories in the universes CategoryTheory.BasedCategory.{u, u + 1}, with both of them explicit; AlgebraicGeometry.Stack.isAlgebraicStack_iff_of_equivalence is the same assertion for categories in arbitrary universes.

theorem isAlgebraicStack_iff_of_equivalence'
    (𝒳 𝒴 : BasedCategory.{u, u + 1} (BigFppfOver B S hS))
    (e : BasedCategory.Equivalence 𝒳 𝒴) :
    IsAlgebraicStack.{u, w} B S hS 𝒳 ↔ IsAlgebraicStack.{u, w} B S hS 𝒴

AlgebraicGeometry.Stack.isAlgebraicStack_of_equivalenceOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicStackEquivalenceUniverses.lean, line 83. The attribute's comment: “the two categories in independent universes”.

A category over the big fppf site of S which is equivalent over that site to an algebraic stack is an algebraic stack, the two categories being allowed independent object and morphism universes.

theorem isAlgebraicStack_of_equivalenceOver
    {𝒳 : BasedCategory.{v₁, t₁} (BigFppfOver B S hS)}
    {𝒴 : BasedCategory.{v₂, t₂} (BigFppfOver B S hS)}
    (e : StacksRepresentableCFG.EquivalenceOver 𝒳.p 𝒴.p)
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳) :
    IsAlgebraicStack.{u, w} B S hS 𝒴
Sources
LeanAlgebraicGeometry.Stack.IsAlgebraicStack · AlgebraicGeometry.Stack.IsDeligneMumfordStack · AlgebraicGeometry.Stack.AlgebraicStacks · AlgebraicGeometry.Stack.isAlgebraicStack_iff_of_equivalence · AlgebraicGeometry.Stack.isDeligneMumfordStack_iff_of_equivalence · AlgebraicGeometry.Stack.isAlgebraicStack_iff_of_equivalence' · AlgebraicGeometry.Stack.isAlgebraicStack_of_equivalenceOver

Section94.13 Algebraic stacks and algebraic spaces#

Section 94.13 of the Stacks Project, Tag 03YR. 4 tags here are carried by 13 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03YR, the section

Tag 03YR in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_iff_isStackInSetoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicStacksAndSpaces.lean, line 50. The attribute's comment: “the main result: an algebraic stack is an algebraic space exactly when its fibre categories are setoids”.

An algebraic stack over S is representable by an algebraic space if and only if it is a stack in setoids, that is, objects of its fibre categories have no nontrivial automorphisms.

theorem isRepresentableByAlgebraicSpace_iff_isStackInSetoids
    (halg : IsAlgebraicStack.{u, w} B S hS 𝒳.val) :
    IsRepresentableByAlgebraicSpace B S hS 𝒳 ↔
      𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS)

Declarations registered for the tag:

Tag 03YS, a lemma

Tag 03YS in the Stacks Project.

AlgebraicGeometry.Stack.isDeligneMumfordStack_fibredCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicSpaceStackPresentation.lean, line 313. The attribute's comment: “part (2)”.

Stacks 03YS, part (2). The category of elements of an algebraic space F over S, read as a category fibred in groupoids over the big fppf site of S, is a Deligne-Mumford stack.

It is an algebraic stack by AlgebraicGeometry.Stack.isAlgebraicStack_fibredCategory, and the same scheme atlas of F presents it étale-ly: the atlas of Stacks 025Y is surjective and étale, and AlgebraicGeometry.Stack.prop_presentationBasedFunctor carries both properties to the induced 1-morphism.

theorem isDeligneMumfordStack_fibredCategory (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) :
    IsDeligneMumfordStack.{u, w} B S hS (fibredCategory B S hS F).val

AlgebraicGeometry.Stack.isDeligneMumfordStack_of_isRepresentableByAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableDeligneMumford.lean, line 223. The attribute's comment: “part (1)”.

Stacks 03YS, part (1). A category fibred in groupoids over the big fppf site of S which is representable by an algebraic space over S is a Deligne-Mumford stack.

It is an algebraic stack by AlgebraicGeometry.Stack.isAlgebraicStack_of_isRepresentableByAlgebraicSpace, and the surjective étale scheme atlas of Stacks 025Y for the representing algebraic space presents it étale-ly, again by AlgebraicGeometry.Stack.prop_transportedPresentation.

theorem isDeligneMumfordStack_of_isRepresentableByAlgebraicSpace
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsRepresentableByAlgebraicSpace B S hS 𝒳) :
    IsDeligneMumfordStack.{u, w} B S hS 𝒳.val

AlgebraicGeometry.Stack.isDeligneMumfordStack_schemeFibredCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeStack.lean, line 221. The attribute's comment: “part (3)”.

Stacks 03YS, part (3). The big fppf site of a scheme X over S, read as a category fibred in groupoids over the big fppf site of S, is a Deligne-Mumford stack.

It is an algebraic stack by AlgebraicGeometry.Stack.isAlgebraicStack_schemeFibredCategory, and the same identity 1-morphism presents it étale-ly, since the identity of yoneda.obj X is surjective and étale.

theorem isDeligneMumfordStack_schemeFibredCategory (X : BigFppfOver B S hS) :
    IsDeligneMumfordStack.{u, w} B S hS (schemeFibredCategory B S hS X).val
Tag 045H, a lemma

Tag 045H in the Stacks Project.

AlgebraicGeometry.Stack.isDeligneMumfordStack_and_isStackInSetoids_of_isRepresentableByAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordStackInSetoids.lean, line 123. The attribute's comment: “the implication (3) ⟹ (1)”.

Stacks 045H, the implication (3) ⟹ (1). A category fibred in groupoids over the big fppf site of S which is representable by an algebraic space over S is a Deligne-Mumford stack and a stack in setoids for the fppf topology.

The first conjunct is Stacks 03YS part (1) and the second is the implication (3) ⟹ (1) of Stacks 04SZ; neither uses algebraicity as a hypothesis, so none is assumed.

theorem isDeligneMumfordStack_and_isStackInSetoids_of_isRepresentableByAlgebraicSpace
    (h : IsRepresentableByAlgebraicSpace B S hS 𝒳) :
    IsDeligneMumfordStack.{u, w} B S hS 𝒳.val ∧
      𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS)

AlgebraicGeometry.Stack.isDeligneMumfordStack_and_inertiaProjection_isEquivalence_of_isRepresentableByAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordStackInSetoids.lean, line 137. The attribute's comment: “the implication (3) ⟹ (2)”.

Stacks 045H, the implication (3) ⟹ (2). A category fibred in groupoids over the big fppf site of S which is representable by an algebraic space over S is a Deligne-Mumford stack whose canonical projection from the inertia category is an equivalence.

This is the implication (3) ⟹ (1) with its second conjunct passed through Stacks 04ZM, which is the implication (3) ⟹ (2) of Stacks 04SZ.

theorem isDeligneMumfordStack_and_inertiaProjection_isEquivalence_of_isRepresentableByAlgebraicSpace
    (h : IsRepresentableByAlgebraicSpace B S hS 𝒳) :
    IsDeligneMumfordStack.{u, w} B S hS 𝒳.val ∧
      (RelativeInertia.π 𝒳.val.p :
        AbsoluteInertia 𝒳.val.p ⥤ 𝒳.val.obj).IsEquivalence

AlgebraicGeometry.Stack.isStackInSetoids_iff_inertiaProjection_isEquivalence_of_isDeligneMumfordStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordStackInSetoids.lean, line 154. The attribute's comment: “the equivalence of parts (1) and (2)”.

Stacks 045H, the equivalence of parts (1) and (2). A Deligne-Mumford stack over the big fppf site of S is a stack in setoids if and only if the canonical projection from its inertia category is an equivalence.

The Deligne-Mumford condition contains the algebraic-stack condition, which supplies the stack hypothesis of Stacks 04ZM through AlgebraicGeometry.Stack.isStackInSetoids_iff_inertiaProjection_isEquivalence_of_isAlgebraicStack; the Deligne-Mumford conjunct is then common to both sides.

theorem isStackInSetoids_iff_inertiaProjection_isEquivalence_of_isDeligneMumfordStack
    (h𝒳 : IsDeligneMumfordStack.{u, w} B S hS 𝒳.val) :
    𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS) ↔
      (RelativeInertia.π 𝒳.val.p :
        AbsoluteInertia 𝒳.val.p ⥤ 𝒳.val.obj).IsEquivalence

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isDeligneMumfordStack_isStackInSetoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordStackInSetoids.lean, line 234. The attribute's comment: “the implication (1) ⟹ (3)”.

Stacks 045H, the implication (1) ⟹ (3). A Deligne-Mumford stack over the big fppf site of S which is a stack in setoids for the fppf topology is representable by an algebraic space over S.

The surjective étale presentation by a scheme that the Deligne-Mumford condition provides is the presentation the étale engine consumes, and the fibres of an algebraic stack are essentially small.

theorem isRepresentableByAlgebraicSpace_of_isDeligneMumfordStack_isStackInSetoids
    (h𝒳 : IsDeligneMumfordStack.{u, w} B S hS 𝒳.val)
    (hset : 𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS)) :
    IsRepresentableByAlgebraicSpace B S hS 𝒳

AlgebraicGeometry.Stack.isDeligneMumfordStack_isStackInSetoids_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordStackInSetoids.lean, line 255. The attribute's comment: “the equivalence of all three parts”.

Stacks 045H. For a category fibred in groupoids over the big fppf site of S the following are equivalent: it is a Deligne-Mumford stack and a stack in setoids for the fppf topology; it is a Deligne-Mumford stack whose canonical projection from the inertia is an equivalence; it is representable by an algebraic space over S.

No algebraicity hypothesis is assumed: algebraicity is part of the Deligne-Mumford condition of the first two parts, and the third implies it by Stacks 03YS part (1).

theorem isDeligneMumfordStack_isStackInSetoids_tfae :
    List.TFAE
      [IsDeligneMumfordStack.{u, w} B S hS 𝒳.val ∧
          𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS),
        IsDeligneMumfordStack.{u, w} B S hS 𝒳.val ∧
          (RelativeInertia.π 𝒳.val.p :
            AbsoluteInertia 𝒳.val.p ⥤ 𝒳.val.obj).IsEquivalence,
        IsRepresentableByAlgebraicSpace B S hS 𝒳]

Declarations registered for the tag:

Tag 04SZ, a proposition

Tag 04SZ in the Stacks Project.

AlgebraicGeometry.Stack.isStackInSetoids_iff_inertiaProjection_isEquivalence_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicStackIsStack.lean, line 55. The attribute's comment: “parts (1) and (2)”.

An algebraic stack over the big fppf site of S is a stack in setoids if and only if the canonical projection from its inertia category is an equivalence.

theorem isStackInSetoids_iff_inertiaProjection_isEquivalence_of_isAlgebraicStack
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val) :
    𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS) ↔
      (RelativeInertia.π 𝒳.val.p :
        AbsoluteInertia 𝒳.val.p ⥤ 𝒳.val.obj).IsEquivalence

AlgebraicGeometry.Stack.isStackInSetoids_of_isRepresentableByAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableStackInSetoids.lean, line 89. The attribute's comment: “the implication (3) ⟹ (1)”.

Stacks 04SZ, the implication (3) ⟹ (1). A category fibred in groupoids over the big fppf site of S which is representable by an algebraic space over S is a stack in setoids for the fppf topology.

The representing presheaf is an fppf sheaf, so the category of its elements is a stack in sets, and the equivalence over the site that representability provides carries that back to 𝒳. No part of the algebraic-stack condition is used.

theorem isStackInSetoids_of_isRepresentableByAlgebraicSpace
    (h : IsRepresentableByAlgebraicSpace B S hS 𝒳) :
    𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS)

AlgebraicGeometry.Stack.isEquivalence_inertiaProjection_of_isRepresentableByAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableStackInSetoids.lean, line 127. The attribute's comment: “the implication (3) ⟹ (2)”.

Stacks 04SZ, the implication (3) ⟹ (2). For a category fibred in groupoids over the big fppf site of S which is representable by an algebraic space over S, the canonical projection from its inertia category is an equivalence.

This is the implication (3) ⟹ (1) composed with Stacks 04ZM.

theorem isEquivalence_inertiaProjection_of_isRepresentableByAlgebraicSpace
    (h : IsRepresentableByAlgebraicSpace B S hS 𝒳) :
    (RelativeInertia.π 𝒳.val.p :
      AbsoluteInertia 𝒳.val.p ⥤ 𝒳.val.obj).IsEquivalence

AlgebraicGeometry.Stack.isStackInSetoids_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StackInSetoidsRepresentableBySpace.lean, line 229.

Stacks 04SZ. For an algebraic stack 𝒳 over the big fppf site of S the following are equivalent:

  1. 𝒳 is a stack in setoids;
  2. the canonical 1-morphism I_𝒳 ⟶ 𝒳 from the inertia is an equivalence;
  3. 𝒳 is representable by an algebraic space.

The equivalence (1) ⟺ (2) is AlgebraicGeometry.Stack.isStackInSetoids_iff_inertiaProjection_isEquivalence_of_isAlgebraicStack, the implication (3) ⟹ (1) is AlgebraicGeometry.Stack.isStackInSetoids_of_isRepresentableByAlgebraicSpace, and the implication (1) ⟹ (3) is AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isStackInSetoids.

theorem isStackInSetoids_tfae (halg : IsAlgebraicStack.{u, w} B S hS 𝒳.val) :
    List.TFAE
      [𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS),
        (RelativeInertia.π 𝒳.val.p : AbsoluteInertia 𝒳.val.p ⥤ 𝒳.val.obj).IsEquivalence,
        IsRepresentableByAlgebraicSpace B S hS 𝒳]
Sources
LeanAlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_iff_isStackInSetoids · AlgebraicGeometry.Stack.isDeligneMumfordStack_of_isRepresentableByAlgebraicSpace · AlgebraicGeometry.Stack.isDeligneMumfordStack_fibredCategory · CategoryTheory.RelativeInertia.π_isEquivalence_iff · AlgebraicGeometry.Stack.isDeligneMumfordStack_schemeFibredCategory · AlgebraicGeometry.Stack.isDeligneMumfordStack_and_isStackInSetoids_of_isRepresentableByAlgebraicSpace · AlgebraicGeometry.Stack.isDeligneMumfordStack_and_inertiaProjection_isEquivalence_of_isRepresentableByAlgebraicSpace · AlgebraicGeometry.Stack.isStackInSetoids_iff_inertiaProjection_isEquivalence_of_isDeligneMumfordStack

Section94.14 2-Fibre products of algebraic stacks#

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

Tag 04TE, a lemma

Tag 04TE in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isTwoFibreProduct_productSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicStackEquivalence.lean, line 289.

The product 𝒳 ×_{(Sch/S)_fppf} 𝒴 of two algebraic stacks over S is a product in the 2-category of algebraic stacks over S: the canonical square AlgebraicGeometry.Stack.AlgebraicStacks.productSquare over the cospan of structure 1-morphisms to the final object is a 2-fibre product in that 2-category.

noncomputable def isTwoFibreProduct_productSquare (𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS) :
    Bicategory.IsTwoFibreProduct (productSquare B S hS 𝒳 𝒴)
Tag 04TF, a lemma

Tag 04TF in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/TwoFibreProductAlgebraicStack.lean, line 1332.

Stacks 04TF. Let 𝒵 be a stack in groupoids over the big fppf site of S whose diagonal is representable by algebraic spaces, let 𝒳 and 𝒴 be algebraic stacks over S and let f : 𝒳 ⟶ 𝒵, g : 𝒴 ⟶ 𝒵 be 1-morphisms of stacks in groupoids. Then the 2-fibre product 𝒳 ×_{f, 𝒵, g} 𝒴 is an algebraic stack over S.

The hypothesis on 𝒵 is the stack clause of AlgebraicGeometry.Stack.IsAlgebraicStack, i.e. "stack in groupoids" in both renderings of Stacks 02ZJ; the sieve-indexed conjunct is what Stacks 04TF asks for, and it is what Stacks 026G (CategoryTheory.TwoFibreProductOver.isStack_structureFunctor) consumes.

theorem isAlgebraicStack_twoFibreProduct
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 𝒵 : BasedCategory.{u, u + 1} (BigFppfOver B S hS))
    (f : 𝒳 ⥤ᵇ 𝒵) (g : 𝒴 ⥤ᵇ 𝒵)
    (h𝒵 : 𝒵.p.IsStack (BigFppfOver.topology B S hS) ∧
      𝒵.p.IsStackInGroupoids.{w} (BigFppfOver.topology B S hS))
    (hdiag : HasRepresentableDiagonal B S hS
      (CatFiberedInGroupoids.mk 𝒵 h𝒵.2.isFiberedInGroupoids))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳)
    (h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴) :
    IsAlgebraicStack.{u, w} B S hS
      (BasedCategory.ofFunctor
        (TwoFibreProductOver.structureFunctor 𝒳.p 𝒴.p 𝒵.p f.toFunctor g.toFunctor))

AlgebraicGeometry.Stack.isAlgebraicStack_twoFibreProduct_of_locallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/TwoFibreProductAlgebraicStackLocallySmall.lean, line 206. The attribute's comment: “the two algebraic factors with locally small morphisms in any universe”.

Let 𝒵 be a stack in groupoids over the big fppf site of S whose diagonal is representable by algebraic spaces, let 𝒳 and 𝒴 be algebraic stacks over S whose hom-sets are u-small, in any morphism universes, and let f : 𝒳 ⟶ 𝒵, g : 𝒴 ⟶ 𝒵 be 1-morphisms. Then the 2-fibre product 𝒳 ×_{f, 𝒵, g} 𝒴 is an algebraic stack over S.

theorem isAlgebraicStack_twoFibreProduct_of_locallySmall
    (𝒳 : BasedCategory.{v₁, u + 1} (BigFppfOver B S hS))
    (𝒴 : BasedCategory.{v₂, u + 1} (BigFppfOver B S hS))
    (𝒵 : BasedCategory.{u, u + 1} (BigFppfOver B S hS))
    [LocallySmall.{u} 𝒳.obj] [LocallySmall.{u} 𝒴.obj]
    (f : 𝒳 ⥤ᵇ 𝒵) (g : 𝒴 ⥤ᵇ 𝒵)
    (h𝒵 : 𝒵.p.IsStack (BigFppfOver.topology B S hS) ∧
      𝒵.p.IsStackInGroupoids.{w} (BigFppfOver.topology B S hS))
    (hdiag : HasRepresentableDiagonal B S hS
      (CatFiberedInGroupoids.mk 𝒵 h𝒵.2.isFiberedInGroupoids))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳)
    (h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴) :
    IsAlgebraicStack.{u, w} B S hS
      (BasedCategory.ofFunctor
        (TwoFibreProductOver.structureFunctor 𝒳.p 𝒴.p 𝒵.p f.toFunctor g.toFunctor))
Tag 04T2, a lemma

Tag 04T2 in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_twoFibreProductSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/TwoFibreProductSquareAlgebraicStack.lean, line 67.

Stacks 04T2, first assertion. The apex of the canonical 2-commutative square of a cospan of algebraic stacks over S is an algebraic stack. This is AlgebraicGeometry.Stack.isAlgebraicStack_twoFibreProduct, Stacks 04TF, with base the common target, whose stack and diagonal hypotheses there are two of the clauses of its algebraicity.

theorem isAlgebraicStack_twoFibreProductSquare
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) :
    IsAlgebraicStack.{u, w} B S hS
      (CatFiberedInGroupoids.twoFibreProductSquare.{u, u, u + 1, u + 1} f.hom g.hom).pt.val

AlgebraicGeometry.Stack.isTwoFibreProduct_twoFibreProductSquareAlgebraicStacks, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/TwoFibreProductSquareAlgebraicStack.lean, line 112. The attribute's comment: “2-categorical universal property”.

Stacks 04T2, second assertion: the 2-categorical universal property. The canonical square of a cospan of algebraic stacks over S is a 2-fibre product in the 2-category of algebraic stacks, and not merely in the ambient 2-category of categories fibred in groupoids: the square underlying it is the canonical one there, which is a 2-fibre product unconditionally, and the 2-category of algebraic stacks is a full sub-2-category.

This is also the right square of Stacks 06PQ, whose left square is AlgebraicGeometry.Stack.exists_cartesianRelativeInertiaSquare: the right square of the diagram there is the defining base-change square of the cospan (π, f).

noncomputable def isTwoFibreProduct_twoFibreProductSquareAlgebraicStacks
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) :
    Bicategory.IsTwoFibreProduct (twoFibreProductSquareAlgebraicStacks B S hS f g)

AlgebraicGeometry.Stack.AlgebraicStacks.isTwoFibreProduct_twoFibreProductSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/TwoFibreProductUniversalProperty.lean, line 117. The attribute's comment: “the 2-categorical universal property”.

Stacks 04T2, the 2-categorical universal property. The canonical 2-fibre product square AlgebraicGeometry.Stack.AlgebraicStacks.twoFibreProductSquare of a cospan of algebraic stacks over S is a 2-fibre product in the 2-category of algebraic stacks over (Sch/S)_fppf, not merely in the ambient 2-category of categories fibred in groupoids.

That its apex is an algebraic stack is Stacks 04TF; see AlgebraicGeometry.Stack.isAlgebraicStack_twoFibreProduct.

noncomputable def isTwoFibreProduct_twoFibreProductSquare (g : 𝒵 ⟶ 𝒴) (f : 𝒳 ⟶ 𝒴) :
    Bicategory.IsTwoFibreProduct (twoFibreProductSquare B S hS g f)

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.Stack.AlgebraicStacks.isTwoFibreProduct_productSquare · AlgebraicGeometry.Stack.isAlgebraicStack_twoFibreProduct · AlgebraicGeometry.Stack.isAlgebraicStack_twoFibreProduct_of_locallySmall · AlgebraicGeometry.Stack.isAlgebraicStack_twoFibreProductSquare · AlgebraicGeometry.Stack.isTwoFibreProduct_twoFibreProductSquareAlgebraicStacks · AlgebraicGeometry.Stack.AlgebraicStacks.isTwoFibreProduct_twoFibreProductSquare

Section94.15 Algebraic stacks, overhauled#

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

Tag 04T1, a lemma

Tag 04T1 in the Stacks Project.

AlgebraicGeometry.Stack.exists_smoothSurjectivePresentation_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/PresentationLift.lean, line 190.

Stacks 04T1. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let y : (Sch/V)_fppf ⟶ 𝒴 be surjective and smooth. Then there are a scheme U over S, a 1-morphism x : (Sch/U)_fppf ⟶ 𝒳 which is surjective and smooth, and a 1-morphism a : (Sch/U)_fppf ⟶ (Sch/V)_fppf making the square x ≫ f ≅ a ≫ y 2-commute.

Surjectivity and smoothness are the relative properties of Stacks 03YK for AlgebraicGeometry.Space.surjectiveMorphismProperty and AlgebraicGeometry.Space.smoothMorphismProperty.

theorem exists_smoothSurjectivePresentation_lift
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (_h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴.val)
    (f : 𝒳 ⟶ 𝒴) (V : BigFppfOver B S hS) (y : schemeFibredCategory B S hS V ⟶ 𝒴)
    (hy : IsRepresentableByAlgebraicSpaces B S hS y.hom)
    (hysurj : HasRelativeProperty B S hS (Space.surjectiveMorphismProperty B S hS) y hy)
    (hysmooth : HasRelativeProperty B S hS (Space.smoothMorphismProperty B S hS) y hy) :
    ∃ (U : BigFppfOver B S hS) (x : schemeFibredCategory B S hS U ⟶ 𝒳)
      (a : schemeFibredCategory B S hS U ⟶ schemeFibredCategory B S hS V)
      (hx : IsRepresentableByAlgebraicSpaces B S hS x.hom),
      Nonempty (x ≫ f ≅ a ≫ y) ∧
        HasRelativeProperty B S hS (Space.surjectiveMorphismProperty B S hS) x hx ∧
          HasRelativeProperty B S hS (Space.smoothMorphismProperty B S hS) x hx
Tag 04Y5, a lemma

Tag 04Y5 in the Stacks Project.

AlgebraicGeometry.Stack.faithful_homFunctor_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FaithfulRepresentable.lean, line 63. The attribute's comment: “the implication (3) ⟹ (2)”.

A 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces has faithful underlying functor.

theorem faithful_homFunctor_of_isRepresentableByAlgebraicSpaces
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom) :
    (CatFiberedInGroupoids.homFunctor f).Faithful

AlgebraicGeometry.Stack.AlgebraicStacks.faithful_homFunctor_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FaithfulRepresentable.lean, line 79. The attribute's comment: “the implication (3) ⟹ (2) for algebraic stacks”.

A 1-morphism of algebraic stacks over S which is representable by algebraic spaces has faithful underlying functor.

theorem faithful_homFunctor_of_isRepresentableByAlgebraicSpaces
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    (CatFiberedInGroupoids.homFunctor f.hom).Faithful

AlgebraicGeometry.Stack.AlgebraicStacks.faithful_homFunctor_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FaithfulRepresentableUnconditional.lean, line 119.

Stacks 04Y5. For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S the following are equivalent:

  1. for every object U of the big fppf site of S the functor f_U : 𝒳_U ⥤ 𝒴_U on fibres is faithful;
  2. the functor f is faithful;
  3. f is representable by algebraic spaces.

The equivalence (1) ⟺ (2) is Stacks 003Z (1), CategoryTheory.Functor.IsFiberedInGroupoids.faithful_iff_forall_fiber; the implication (3) ⟹ (2) is AlgebraicGeometry.Stack.AlgebraicStacks.faithful_homFunctor_of_isRepresentableByAlgebraicSpaces and the implication (2) ⟹ (3) is AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_of_faithful.

theorem faithful_homFunctor_tfae {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    List.TFAE
      [∀ U : BigFppfOver B S hS, (Functor.Fiber.mapOfComp 𝒳.val.val.p 𝒴.val.val.p
          (CatFiberedInGroupoids.homFunctor f.hom)
          (CatFiberedInGroupoids.homFunctor_comp_p f.hom) U).Faithful,
        (CatFiberedInGroupoids.homFunctor f.hom).Faithful,
        IsRepresentableByAlgebraicSpaces B S hS f.hom.hom]

Declarations registered for the tag:

Tag 05UL, a lemma

Tag 05UL in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_of_smoothPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothPresentationAlgebraicStack.lean, line 82.

Stacks 05UL. A stack in groupoids over the big fppf site of S which receives a 1-morphism from a category representable by an algebraic space that is representable by algebraic spaces, surjective and smooth is an algebraic stack.

theorem isAlgebraicStack_of_smoothPresentation (v : 𝒰 ⟶ 𝒳)
    (h𝒳 : 𝒳.val.p.IsStack (BigFppfOver.topology B S hS))
    (h𝒰 : IsRepresentableByAlgebraicSpace B S hS 𝒰)
    (hv : IsRepresentableByAlgebraicSpaces B S hS v.hom)
    (hsurj : HasRelativeProperty.{u, u, u + 1, u + 1} B S hS
      (Space.surjectiveMorphismProperty B S hS) v hv)
    (hsmooth : HasRelativeProperty.{u, u, u + 1, u + 1} B S hS
      (Space.smoothMorphismProperty B S hS) v hv) :
    IsAlgebraicStack.{u, w} B S hS 𝒳.val
Tag 05UM, a lemma

Tag 05UM in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_source_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableMorphismAlgebraicStack.lean, line 145.

Stacks 05UM. If a 1-morphism j : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf site of S is representable by algebraic spaces and 𝒴 is an algebraic stack over S, then 𝒳 is an algebraic stack over S.

The scheme atlas of 𝒴 base changes along j to a 1-morphism W ⟶ 𝒳 which is again representable by algebraic spaces (Stacks 0302), surjective and smooth (Stacks 045C), with W representable by an algebraic space (Stacks 0300); the diagonal of 𝒳 is inherited from that of 𝒴, so the form of Stacks 05UL that takes the diagonal as a hypothesis applies.

The same statement is the algebraic-stack clause of Stacks 05UN, whose stack-in-groupoids clause is AlgebraicGeometry.Stack.isStack_of_isRepresentableByAlgebraicSpaces; the two clauses together are AlgebraicGeometry.Stack.isStack_and_isAlgebraicStack_of_isRepresentableByAlgebraicSpaces.

theorem isAlgebraicStack_source_of_isRepresentableByAlgebraicSpaces (j : 𝒳 ⟶ 𝒴)
    (hj : IsRepresentableByAlgebraicSpaces B S hS j.hom)
    (h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴.val) :
    IsAlgebraicStack.{u, w} B S hS 𝒳.val
Tag 05UN, a lemma

Tag 05UN in the Stacks Project.

AlgebraicGeometry.Stack.isStack_and_isAlgebraicStack_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableMorphismAlgebraicStack.lean, line 188.

Stacks 05UN. Let j : 𝒳 ⟶ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces. If 𝒴 is a stack in groupoids then so is 𝒳, and if 𝒴 is an algebraic stack then so is 𝒳.

The first clause is AlgebraicGeometry.Stack.isStack_of_isRepresentableByAlgebraicSpaces, the second AlgebraicGeometry.Stack.isAlgebraicStack_source_of_isRepresentableByAlgebraicSpaces.

theorem isStack_and_isAlgebraicStack_of_isRepresentableByAlgebraicSpaces (j : 𝒳 ⟶ 𝒴)
    (hj : IsRepresentableByAlgebraicSpaces B S hS j.hom) :
    (𝒴.val.p.IsStack (BigFppfOver.topology B S hS) →
        𝒳.val.p.IsStack (BigFppfOver.topology B S hS)) ∧
      (IsAlgebraicStack.{u, w} B S hS 𝒴.val → IsAlgebraicStack.{u, w} B S hS 𝒳.val)

AlgebraicGeometry.Stack.isStack_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableMorphismStack.lean, line 808. The attribute's comment: “the stack-in-groupoids clause”.

Stacks 05UN, the stack-in-groupoids clause. A category fibred in groupoids over the big fppf site of S admitting a 1-morphism representable by algebraic spaces into a stack in groupoids is itself a stack in groupoids.

This is the source's own proof of that clause: the criterion of Stacks 02ZY turns representability by algebraic spaces into the faithfulness and sheaf hypotheses of Stacks 0CKJ.

theorem isStack_of_isRepresentableByAlgebraicSpaces
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w}
      (AlgebraicGeometry.BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (hf : AlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (h𝒴 : 𝒴.val.p.IsStack (AlgebraicGeometry.BigFppfOver.topology B S hS)) :
    𝒳.val.p.IsStack (AlgebraicGeometry.BigFppfOver.topology B S hS)
Sources
LeanAlgebraicGeometry.Stack.exists_smoothSurjectivePresentation_lift · AlgebraicGeometry.Stack.faithful_homFunctor_of_isRepresentableByAlgebraicSpaces · AlgebraicGeometry.Stack.AlgebraicStacks.faithful_homFunctor_of_isRepresentableByAlgebraicSpaces · AlgebraicGeometry.Stack.AlgebraicStacks.faithful_homFunctor_tfae · CategoryTheory.Functor.IsFiberedInGroupoids.faithful_iff_forall_fiber · AlgebraicGeometry.Stack.isAlgebraicStack_of_smoothPresentation · AlgebraicGeometry.Stack.isAlgebraicStack_source_of_isRepresentableByAlgebraicSpaces · AlgebraicGeometry.Stack.isStack_and_isAlgebraicStack_of_isRepresentableByAlgebraicSpaces

Section94.16 From an algebraic stack to a presentation#

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

Tag 04T3, the section

Tag 04T3 in the Stacks Project.

AlgebraicGeometry.Stack.nonempty_groupoidPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothPresentationExistence.lean, line 152. The attribute's comment: “every algebraic stack has a presentation by a smooth groupoid in algebraic spaces”.

Stacks 04T3: every algebraic stack has a presentation. Let 𝒳 be an algebraic stack over S. Then there are a smooth groupoid (U, R, s, t, c) in algebraic spaces over S and an equivalence over the big fppf site of S from its quotient stack [U/R] to 𝒳.

The groupoid is the self-intersection groupoid of Stacks 04T4 (4) of the presentation of 𝒳 by a scheme, which is smooth by Stacks 04T5 (1), and the equivalence is the canonical 1-morphism of Stacks 04T4 (5), which is an equivalence by Stacks 04T5 (2).

theorem nonempty_groupoidPresentation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val) :
    Nonempty (GroupoidPresentation B S hS 𝒳.val)
Tag 04T4, a lemma

Tag 04T4 in the Stacks Project.

AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersection.lean, line 165. The attribute's comment: “part (2): three-fold product as composable arrows”.

Stacks 04T4 (2). The canonical equivalence, in the 2-category of categories over the big fppf site of S, between the three-fold 2-fibre product 𝒰 ×_𝒳 𝒰 ×_𝒳 𝒰 and the category ℛ ×_{pr₁, 𝒰, pr₀} ℛ of composable pairs of arrows of the relation. On fibres over a scheme T it sends ((a, b, α), c, β) to ((a, b, α), (b, c, β)).

noncomputable def tripleEquivComposable :
    StacksRepresentableCFG.EquivalenceOver (tripleProjection B S hS 𝒰 𝒳 f)
      (composableProjection B S hS 𝒰 𝒳 f)

AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersection.lean, line 174. The attribute's comment: “part (2): first arrow of the comparison”.

The comparison of Stacks 04T4 (2) leaves the first relation arrow unchanged.

theorem tripleEquivComposable_fst (x : triple B S hS 𝒰 𝒳 f) :
    ((tripleEquivComposable B S hS 𝒰 𝒳 f).hom.functor.obj x).x = x.x

AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable_last, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersection.lean, line 179. The attribute's comment: “part (2): last object of the comparison”.

The comparison of Stacks 04T4 (2) leaves the final object unchanged.

theorem tripleEquivComposable_last (x : triple B S hS 𝒰 𝒳 f) :
    ((tripleEquivComposable B S hS 𝒰 𝒳 f).hom.functor.obj x).y.y = x.y

AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable_middle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersection.lean, line 185. The attribute's comment: “part (2): middle object of the comparison”.

Under the comparison of Stacks 04T4 (2) the second relation arrow starts at the first arrow's endpoint.

theorem tripleEquivComposable_middle (x : triple B S hS 𝒰 𝒳 f) :
    ((tripleEquivComposable B S hS 𝒰 𝒳 f).hom.functor.obj x).y.x = x.x.y

AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable_secondIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersection.lean, line 191. The attribute's comment: “part (2): second isomorphism of the comparison”.

Under the comparison of Stacks 04T4 (2) the second relation arrow carries the original second isomorphism.

theorem tripleEquivComposable_secondIso (x : triple B S hS 𝒰 𝒳 f) :
    HEq ((tripleEquivComposable B S hS 𝒰 𝒳 f).hom.functor.obj x).y.iso x.iso

AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable_middleIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersection.lean, line 197. The attribute's comment: “part (2): identity at the middle object”.

Under the comparison of Stacks 04T4 (2) the identification of the two middle objects is the identity.

theorem tripleEquivComposable_middleIso (x : triple B S hS 𝒰 𝒳 f) :
    HEq ((tripleEquivComposable B S hS 𝒰 𝒳 f).hom.functor.obj x).iso
      (Iso.refl x.x.y)

AlgebraicGeometry.Stack.SelfIntersection.composition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersection.lean, line 206. The attribute's comment: “part (3): composition of the relation”.

Stacks 04T4 (3). The outer projection pr₀₂, induced through the comparison of part (2) by the projection of the three-fold product onto its outer two factors: a 1-morphism from the category of composable pairs to the relation, sending ((a, b, α), (b, c, β)) to (a, c, β ∘ α).

noncomputable def composition :
    BasedCategory.ofFunctor (composableProjection B S hS 𝒰 𝒳 f) ⥤ᵇ
      (relation B S hS 𝒰 𝒳 f).val

AlgebraicGeometry.Stack.SelfIntersection.composition_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersection.lean, line 219. The attribute's comment: “part (3): source of the composite”.

The composite of Stacks 04T4 (3) begins at the first arrow's source.

theorem composition_fst (x : composable B S hS 𝒰 𝒳 f) :
    ((composition B S hS 𝒰 𝒳 f).toFunctor.obj x).x = x.x.x

AlgebraicGeometry.Stack.SelfIntersection.composition_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersection.lean, line 224. The attribute's comment: “part (3): target of the composite”.

The composite of Stacks 04T4 (3) ends at the second arrow's target.

theorem composition_snd (x : composable B S hS 𝒰 𝒳 f) :
    ((composition B S hS 𝒰 𝒳 f).toFunctor.obj x).y = x.y.y

AlgebraicGeometry.Stack.SelfIntersection.composition_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersection.lean, line 230. The attribute's comment: “part (3): composition on fibre objects”.

On objects the outer arrow of Stacks 04T4 (3) carries the composite of the two isomorphisms, including the identification of their middle objects.

theorem composition_iso (x : composable B S hS 𝒰 𝒳 f) :
    HEq ((composition B S hS 𝒰 𝒳 f).toFunctor.obj x).iso
      (x.x.iso ≪≫ f.toFunctor.mapIso x.iso ≪≫ x.y.iso)

AlgebraicGeometry.Stack.SelfIntersection.isRepresentableByAlgebraicSpace_relation_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionAlgebraicSpace.lean, line 102. The attribute's comment: “part (1): the relation is an algebraic space”.

Stacks 04T4 (1). Let 𝒳 be an algebraic stack over S and let f : 𝒰 ⟶ 𝒳 be a 1-morphism whose source is a category fibred in groupoids representable by an algebraic space over S. Then the self-intersection ℛ = 𝒰 ×_{f, 𝒳, f} 𝒰 is representable by an algebraic space.

The diagonal of an algebraic stack is representable by algebraic spaces, which is condition (1) of Stacks 045G; condition (8) of Stacks 045G follows, and instantiated at 𝒯₁ = 𝒯₂ = 𝒰 and x = y = f it is the conclusion.

theorem isRepresentableByAlgebraicSpace_relation_of_isAlgebraicStack
    (h𝒴 : Stack.IsAlgebraicStack.{u, w} B S hS 𝒴.val)
    (h𝒰 : Stack.IsRepresentableByAlgebraicSpace B S hS 𝒰) :
    Stack.IsRepresentableByAlgebraicSpace B S hS (relation B S hS 𝒰 𝒴 f)

AlgebraicGeometry.Stack.SelfIntersection.nonempty_fullyFaithful_canonicalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionFullyFaithful.lean, line 394. The attribute's comment: “part (6): full faithfulness”.

The canonical morphism f_can : [U/R] ⟶ 𝒳 of the presentation datum AlgebraicGeometry.Stack.SelfIntersection.selfIntersectionPresentation is fully faithful.

theorem nonempty_fullyFaithful_canonicalMap (h𝒳 : IsAlgebraicStack B S hS 𝒳.val) :
    Nonempty ((selfIntersectionPresentation eU eR h𝒳).canonicalMap.toFunctor.FullyFaithful)

AlgebraicGeometry.Stack.SelfIntersection.relationTarget, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionGroupoid.lean, line 172. The attribute's comment: “part (4): target morphism of the groupoid”.

The target morphism t : R ⟶ U of the self-intersection groupoid, read in the category of algebraic spaces over S of Stacks 02X2: the morphism of algebraic spaces named, through Stacks 04SW, by the first projection pr₀ : ℛ ⟶ 𝒰 of the 2-fibre product.

On a test scheme T it sends the isomorphism class of a triple (a, b, α) to that of a.

noncomputable def relationTarget : R ⟶ U

AlgebraicGeometry.Stack.SelfIntersection.relationSource, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionGroupoid.lean, line 181. The attribute's comment: “part (4): source morphism of the groupoid”.

The source morphism s : R ⟶ U of the self-intersection groupoid, read in the category of algebraic spaces over S of Stacks 02X2: the morphism of algebraic spaces named, through Stacks 04SW, by the second projection pr₁ : ℛ ⟶ 𝒰 of the 2-fibre product.

On a test scheme T it sends the isomorphism class of a triple (a, b, α) to that of b.

noncomputable def relationSource : R ⟶ U

AlgebraicGeometry.Stack.SelfIntersection.SelfIntersectionPresentation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionPresentation.lean, line 308. The attribute's comment: “parts (4) and (5), the presentation datum: the groupoid and the canonical morphism from its quotient stack, as a structure”.

A presentation datum for f: a groupoid in algebraic spaces whose object space is the chosen representing space of 𝒰 and whose arrow space is the chosen representing space of the self-intersection, together with a morphism from its quotient stack to 𝒳 and a vertical comparison of that morphism with f compatible with descent.

structure SelfIntersectionPresentation

AlgebraicGeometry.Stack.SelfIntersection.selfIntersectionPresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionPresentation.lean, line 400. The attribute's comment: “parts (4) and (5), the construction: that datum built from the declarations of this file and its three predecessors”.

The presentation datum of an algebraic stack 𝒳: the groupoid AlgebraicGeometry.Stack.SelfIntersection.selfIntersectionGroupoid over the final algebraic space, the canonical morphism AlgebraicGeometry.Stack.SelfIntersection.canonicalMapToStack, the comparison extendsFQuotient with f, and eU as the chosen equivalence of the object fibration.

noncomputable def selfIntersectionPresentation (h𝒳 : IsAlgebraicStack B S hS 𝒳.val) :
    SelfIntersectionPresentation eU eR
Tag 04T5, a lemma

Tag 04T5 in the Stacks Project.

AlgebraicGeometry.Stack.SelfIntersection.isSmooth_relationSource_and_relationTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionGroupoidRelativeProperty.lean, line 251. The attribute's comment: “part (1): the structure morphisms of the groupoid are smooth”.

Stacks 04T5 (1). If the point f : 𝒰 ⟶ 𝒳 is smooth in the sense of Stacks 04XB, then the source and target morphisms s, t : R ⟶ U of the self-intersection groupoid of Stacks 04T4 (4) are smooth morphisms of algebraic spaces over S.

theorem isSmooth_relationSource_and_relationTarget (hf : IsRelativelySmooth B S hS f) :
    Space.IsSmooth B S hS (relationSource eU eR).hom ∧
      Space.IsSmooth B S hS (relationTarget eU eR).hom

AlgebraicGeometry.Stack.SelfIntersection.exists_equivalenceOver_canonicalMap_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionSmoothPresentation.lean, line 65. The attribute's comment: “part (2): canonical equivalence”.

Let 𝒳 be an algebraic stack over S, let f : 𝒰 ⟶ 𝒳 be a 1-morphism whose source is represented by an algebraic space U and whose self-intersection is represented by an algebraic space R, and suppose that every algebraic space representing a base change of f along a scheme-valued point of 𝒳 has smooth and surjective structural morphism. Then the canonical 1-morphism f_can : [U/R] ⟶ 𝒳 out of the quotient stack of the groupoid of selfIntersectionPresentation eU eR h𝒳 is the forward 1-morphism of an equivalence over the big fppf site of S.

theorem exists_equivalenceOver_canonicalMap_of_isSmooth
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (hsmooth : ∀ (T : BigFppfOver B S hS)
        (y : BigFppfOver B T.left.1 T.left.2 ⥤ 𝒳.val.obj)
        (_hy : y ⋙ 𝒳.val.p = Over.map T.hom)
        (F : (BigFppfOver B T.left.1 T.left.2)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B T.left.1 T.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map T.hom) 𝒰.val.p 𝒳.val.p y
            (CatFiberedInGroupoids.homFunctor f))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.IsSmooth B S hS (algebraicSpaceMap B S hS T
          ((spacesOverSmallerBaseFunctor B T.left.1 S T.left.2 hS T.hom).obj ⟨F, hF⟩)).hom)
    (hsurj : ∀ (T : BigFppfOver B S hS)
        (y : BigFppfOver B T.left.1 T.left.2 ⥤ 𝒳.val.obj)
        (_hy : y ⋙ 𝒳.val.p = Over.map T.hom)
        (F : (BigFppfOver B T.left.1 T.left.2)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B T.left.1 T.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map T.hom) 𝒰.val.p 𝒳.val.p y
            (CatFiberedInGroupoids.homFunctor f))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.IsSurjective B S hS (algebraicSpaceMap B S hS T
          ((spacesOverSmallerBaseFunctor B T.left.1 S T.left.2 hS T.hom).obj ⟨F, hF⟩)).hom) :
    ∃ e : StacksRepresentableCFG.EquivalenceOver
        (Stack.quotientStack (selfIntersectionPresentation eU eR h𝒳).groupoid).p 𝒳.val.p,
      e.hom.functor = (selfIntersectionPresentation eU eR h𝒳).canonicalMap.toFunctor

AlgebraicGeometry.Stack.SelfIntersection.isSmooth_selfIntersectionPresentation_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionSmoothProjections.lean, line 50. The attribute's comment: “part (1): source projection”.

The source morphism R ⟶ U of the groupoid in algebraic spaces AlgebraicGeometry.Stack.SelfIntersection.selfIntersectionPresentation is smooth when the presenting 1-morphism F is representable by algebraic spaces and smooth.

theorem isSmooth_selfIntersectionPresentation_source
    (hF : IsRepresentableByAlgebraicSpaces B S hS F.hom)
    (hsmooth : HasRelativeProperty.{u, u, u + 1, u} B S hS
      (Space.smoothMorphismProperty B S hS) F hF)
    (h𝒳 : IsAlgebraicStack B S hS 𝒳.val) :
    Space.IsSmooth B S hS (selfIntersectionPresentation eU eR h𝒳).groupoid.source.hom

AlgebraicGeometry.Stack.SelfIntersection.isSmooth_selfIntersectionPresentation_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionSmoothProjections.lean, line 68. The attribute's comment: “part (1): target projection”.

The target morphism R ⟶ U of the groupoid in algebraic spaces AlgebraicGeometry.Stack.SelfIntersection.selfIntersectionPresentation is smooth when the presenting 1-morphism F is representable by algebraic spaces and smooth.

theorem isSmooth_selfIntersectionPresentation_target
    (hF : IsRepresentableByAlgebraicSpaces B S hS F.hom)
    (hsmooth : HasRelativeProperty.{u, u, u + 1, u} B S hS
      (Space.smoothMorphismProperty B S hS) F hF)
    (h𝒳 : IsAlgebraicStack B S hS 𝒳.val) :
    Space.IsSmooth B S hS (selfIntersectionPresentation eU eR h𝒳).groupoid.target.hom
Tag 04WY, a remark

Tag 04WY in the Stacks Project.

AlgebraicGeometry.Stack.SelfIntersection.nonempty_isEquivalenceOver_canonicalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionFlatPresentation.lean, line 187. The attribute's comment: “flat_presentation_equivalence”.

Let 𝒳 be an algebraic stack over S, let f : 𝒰 ⟶ 𝒳 be a 1-morphism whose source is represented by an algebraic space U and whose self-intersection is represented by an algebraic space R, and suppose that every algebraic space representing a base change of f along a scheme-valued point of 𝒳 has surjective, flat and locally finitely presented structural morphism. Then the canonical 1-morphism f_can : [U/R] ⟶ 𝒳 of the presentation datum selfIntersectionPresentation eU eR h𝒳 is an equivalence over the big fppf site of S.

theorem nonempty_isEquivalenceOver_canonicalMap
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (hCover : ∀ (T : BigFppfOver B S hS)
        (y : BigFppfOver B T.left.1 T.left.2 ⥤ 𝒳.val.obj)
        (_hy : y ⋙ 𝒳.val.p = Over.map T.hom)
        (F : (BigFppfOver B T.left.1 T.left.2)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B T.left.1 T.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map T.hom) 𝒰.val.p 𝒳.val.p y
            (CatFiberedInGroupoids.homFunctor f))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        let a := algebraicSpaceMap B S hS T
          ((spacesOverSmallerBaseFunctor B T.left.1 S T.left.2 hS T.hom).obj ⟨F, hF⟩)
        (Space.IsSurjective B S hS a.hom ∧ Space.IsFlat B S hS a.hom ∧
          Space.IsLocallyOfFinitePresentation B S hS a.hom)) :
    Nonempty (Functor.IsEquivalenceOver
      (Stack.quotientStack (selfIntersectionPresentation eU eR h𝒳).groupoid).p
      𝒳.val.p
      (selfIntersectionPresentation eU eR h𝒳).canonicalMap.toFunctor)

AlgebraicGeometry.Stack.SelfIntersection.isFlat_selfIntersectionPresentation_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionFlatProjections.lean, line 153. The attribute's comment: “the source projection of a flat presentation is flat”.

Stacks 04WY for the source projection, flatness. The source morphism R ⟶ U of the groupoid in algebraic spaces of Stacks 04T4 (4) is flat when the presenting 1-morphism is.

The source morphism is induced by the second projection pr₁ of the self-intersection, which is the first leg of the leg exchange (Stacks 003Q) of the canonical 2-fibre product square over the cospan F, F; so this is Stacks 04XC at flatness, read at that square.

theorem isFlat_selfIntersectionPresentation_source
    (hF : IsRepresentableByAlgebraicSpaces B S hS F.hom)
    (hflat : HasRelativeProperty.{u, u, u + 1, u} B S hS
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (g : X ⟶ Y) => Space.IsFlat B S hS g.hom) F hF)
    (h𝒳 : IsAlgebraicStack B S hS 𝒳.val) :
    Space.IsFlat B S hS (selfIntersectionPresentation eU eR h𝒳).groupoid.source.hom

AlgebraicGeometry.Stack.SelfIntersection.isFlat_selfIntersectionPresentation_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionFlatProjections.lean, line 168. The attribute's comment: “the target projection of a flat presentation is flat”.

Stacks 04WY for the target projection, flatness. The target morphism R ⟶ U of the groupoid in algebraic spaces of Stacks 04T4 (4) is flat when the presenting 1-morphism is.

The target morphism is induced by the first projection pr₀ of the self-intersection, which is the first leg of the canonical 2-fibre product square over the cospan F, F; so this is Stacks 04XC at flatness, read at that square, with no leg exchange.

theorem isFlat_selfIntersectionPresentation_target
    (hF : IsRepresentableByAlgebraicSpaces B S hS F.hom)
    (hflat : HasRelativeProperty.{u, u, u + 1, u} B S hS
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (g : X ⟶ Y) => Space.IsFlat B S hS g.hom) F hF)
    (h𝒳 : IsAlgebraicStack B S hS 𝒳.val) :
    Space.IsFlat B S hS (selfIntersectionPresentation eU eR h𝒳).groupoid.target.hom

AlgebraicGeometry.Stack.SelfIntersection.isLocallyOfFinitePresentation_selfIntersectionPresentation_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionFlatProjections.lean, line 183. The attribute's comment: “the source projection is locally of finite presentation”.

Stacks 04WY for the source projection, local finite presentation. The source morphism R ⟶ U of the groupoid in algebraic spaces of Stacks 04T4 (4) is locally of finite presentation when the presenting 1-morphism is.

This is Stacks 04XC at local finite presentation, read at the leg exchange (Stacks 003Q) of the canonical 2-fibre product square over the cospan F, F.

theorem isLocallyOfFinitePresentation_selfIntersectionPresentation_source
    (hF : IsRepresentableByAlgebraicSpaces B S hS F.hom)
    (hlfp : HasRelativeProperty.{u, u, u + 1, u} B S hS
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (g : X ⟶ Y) =>
        Space.IsLocallyOfFinitePresentation B S hS g.hom) F hF)
    (h𝒳 : IsAlgebraicStack B S hS 𝒳.val) :
    Space.IsLocallyOfFinitePresentation B S hS
      (selfIntersectionPresentation eU eR h𝒳).groupoid.source.hom

AlgebraicGeometry.Stack.SelfIntersection.isLocallyOfFinitePresentation_selfIntersectionPresentation_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionFlatProjections.lean, line 200. The attribute's comment: “the target projection is locally of finite presentation”.

Stacks 04WY for the target projection, local finite presentation. The target morphism R ⟶ U of the groupoid in algebraic spaces of Stacks 04T4 (4) is locally of finite presentation when the presenting 1-morphism is.

This is Stacks 04XC at local finite presentation, read at the canonical 2-fibre product square over the cospan F, F, with no leg exchange.

theorem isLocallyOfFinitePresentation_selfIntersectionPresentation_target
    (hF : IsRepresentableByAlgebraicSpaces B S hS F.hom)
    (hlfp : HasRelativeProperty.{u, u, u + 1, u} B S hS
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (g : X ⟶ Y) =>
        Space.IsLocallyOfFinitePresentation B S hS g.hom) F hF)
    (h𝒳 : IsAlgebraicStack B S hS 𝒳.val) :
    Space.IsLocallyOfFinitePresentation B S hS
      (selfIntersectionPresentation eU eR h𝒳).groupoid.target.hom

AlgebraicGeometry.dualNumbers_projections_not_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionFlatProjections.lean, line 308. The attribute's comment: “the projections of a flat presentation need not be smooth”.

Stacks 04WY, the dual-number counterexample. The cover of a point by the spectrum of its dual numbers is surjective, flat and locally of finite presentation, and neither projection of its self-fibre product is smooth. So the two projections of a flat presentation locally of finite presentation are not smooth in general, unlike the smooth case of Stacks 04T5 (1).

theorem dualNumbers_projections_not_smooth (k : Type u) [Field k] :
    let U := Spec (.of (TrivSqZeroExt k k))
    let X := Spec (.of k)
    let f : U ⟶ X := Spec.map (CommRingCat.ofHom (TrivSqZeroExt.inlHom k k))
    Surjective f ∧ Flat f ∧ LocallyOfFinitePresentation f ∧
      ¬ Smooth (pullback.fst f f) ∧ ¬ Smooth (pullback.snd f f)

AlgebraicGeometry.Stack.SelfIntersection.isFlat_relationSource_and_relationTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionGroupoidRelativeProperty.lean, line 209. The attribute's comment: “second clause, flatness half: the structure morphisms of the groupoid are flat”.

Stacks 04WY, the flatness half of its clause on the structure morphisms of the groupoid. If the point f : 𝒰 ⟶ 𝒳 is flat in the relative sense of Stacks 03YK, then the source and target morphisms s, t : R ⟶ U of the self-intersection groupoid of Stacks 04T4 (4) are flat morphisms of algebraic spaces over S.

The source statement is the remark that the conclusion of Stacks 04T5 survives weakening smoothness of f to flatness together with local finite presentation, and that s and t are then flat and locally of finite presentation; this is its flatness half.

theorem isFlat_relationSource_and_relationTarget
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hP : HasRelativeProperty.{u, u, u + 1, u} B S hS
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (g : F ⟶ G) => Space.IsFlat B S hS g.hom) f hf) :
    Space.IsFlat B S hS (relationSource eU eR).hom ∧
      Space.IsFlat B S hS (relationTarget eU eR).hom

AlgebraicGeometry.Stack.SelfIntersection.isLocallyOfFinitePresentation_relationSource_and_relationTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionGroupoidRelativeProperty.lean, line 231. The attribute's comment: “second clause, lfp half: the structure morphisms are locally of finite presentation”.

Stacks 04WY, the local finite presentation half of its clause on the structure morphisms of the groupoid. If the point f : 𝒰 ⟶ 𝒳 is locally of finite presentation in the relative sense of Stacks 03YK, then the source and target morphisms s, t : R ⟶ U of the self-intersection groupoid of Stacks 04T4 (4) are locally of finite presentation.

The source statement is the remark that the conclusion of Stacks 04T5 survives weakening smoothness of f to flatness together with local finite presentation, and that s and t are then flat and locally of finite presentation; this is its local finite presentation half. The flatness half is AlgebraicGeometry.Stack.SelfIntersection.isFlat_relationSource_and_relationTarget.

theorem isLocallyOfFinitePresentation_relationSource_and_relationTarget
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hP : HasRelativeProperty.{u, u, u + 1, u} B S hS
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (g : F ⟶ G) =>
        Space.IsLocallyOfFinitePresentation B S hS g.hom) f hf) :
    Space.IsLocallyOfFinitePresentation B S hS
        (relationSource eU eR).hom ∧
      Space.IsLocallyOfFinitePresentation B S hS
        (relationTarget eU eR).hom
Tag 04TH, a definition

Tag 04TH in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.IsSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SmoothGroupoid.lean, line 62.

Stacks 04TH. A groupoid (U, R, s, t, c) in algebraic spaces over B is smooth when both its source and its target morphism R ⟶ U are smooth morphisms of algebraic spaces.

Despite the name this does not say that the quotient stack [U/R] is smooth over anything.

abbrev IsSmooth (G : GroupoidInAlgebraicSpaces B S hS Z) : Prop
Tag 04TI, a definition

Tag 04TI in the Stacks Project.

AlgebraicGeometry.Stack.GroupoidPresentation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GroupoidPresentation.lean, line 57.

A presentation of a category 𝒳 over (Sch/S)_fppf is a smooth groupoid (U, R, s, t, c) in algebraic spaces over S together with an equivalence of categories over the site from its quotient stack [U/R] to 𝒳.

structure GroupoidPresentation (𝒳 : BasedCategory.{v, w} (BigFppfOver B S hS))
Sources
LeanAlgebraicGeometry.Stack.nonempty_groupoidPresentation · AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable · AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable_fst · AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable_last · AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable_middle · AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable_secondIso · AlgebraicGeometry.Stack.SelfIntersection.tripleEquivComposable_middleIso · AlgebraicGeometry.Stack.SelfIntersection.composition

Section94.17 The algebraic stack associated to a smooth groupoid#

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

Tag 04TJ, the section

Tag 04TJ in the Stacks Project.

AlgebraicGeometry.Stack.smoothGroupoidAlgebraicStack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothGroupoidPresentation.lean, line 149. The attribute's comment: “the section's construction: the algebraic stack associated to a smooth groupoid in algebraic spaces, as one object bundling the quotient stack with its algebraicity. The quotient stack and its fibredness in groupoids are Stacks 044Q; algebraicity is Stacks 04TK”.

Stacks 04TJ. The algebraic stack associated to a smooth groupoid in algebraic spaces G = (U, R, s, t, c) over an algebraic space over S: the quotient stack [U/R] of Stacks 044Q, fibred in groupoids over the big fppf site of S, together with the proof that it is an algebraic stack over S.

The underlying category over the site is the quotient stack on the nose (AlgebraicGeometry.Stack.smoothGroupoidAlgebraicStack_val); the algebraicity component is Stacks 04TK.

noncomputable def smoothGroupoidAlgebraicStack
    {G : GroupoidInAlgebraicSpaces C S hS A}
    (hG : GroupoidInAlgebraicSpaces.IsSmooth C S hS G) :
    LargeAlgebraicStack.{u, w} C S hS
Tag 04WZ, a lemma

Tag 04WZ in the Stacks Project.

AlgebraicGeometry.Stack.hasRepresentableDiagonal_quotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackRepresentableDiagonal.lean, line 204.

Stacks 04WZ. The diagonal of the quotient stack of a groupoid in algebraic spaces over a scheme of a big fppf site is representable by algebraic spaces.

The diagonal criterion of Stacks 045G reduces this to algebraicity of every isomorphism sheaf of a fibre, which is Stacks 04TB; that result in turn rests on Stacks 04SK, whose last step is the bootstrap theorem.

theorem hasRepresentableDiagonal_quotientStack
    {C : BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S} {A : AlgebraicSpaces C S hS}
    (G : GroupoidInAlgebraicSpaces C S hS A) :
    HasRepresentableDiagonal C S hS
      (CatFiberedInGroupoids.mk (quotientStack G) (isFiberedInGroupoids_quotientStack G))
Tag 04X0, a lemma

Tag 04X0 in the Stacks Project.

AlgebraicGeometry.Stack.QuotientAtlas.isRelativelySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothGroupoidQuotientAtlas.lean, line 97. The attribute's comment: “smoothness”.

Stacks 04X0, smoothness of the projection. Let G = (U, R, s, t, c) be a smooth groupoid in algebraic spaces over S. Then the canonical projection π : S_U ⟶ [U/R] of Stacks 044R is smooth in the sense of Stacks 04XB: it is representable by algebraic spaces, and every algebraic space representing a base change of it along a scheme-valued point of [U/R] has smooth structural morphism.

Only smoothness of the source map s is used. The 2-cartesian square of Stacks 04M9 is AlgebraicGeometry.Stack.QuotientAtlas.presentation, built from the representability of the projection, AlgebraicGeometry.Stack.representable_quotientStackProjectionHom.

theorem isRelativelySmooth {G : GroupoidInAlgebraicSpaces C S hS B}
    (hG : GroupoidInAlgebraicSpaces.IsSmooth C S hS G) :
    IsRelativelySmooth C S hS (quotientStackProjectionHom G)

AlgebraicGeometry.Stack.QuotientAtlas.isRelativelySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothGroupoidQuotientAtlas.lean, line 112. The attribute's comment: “surjectivity”.

Stacks 04X0, surjectivity of the projection. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over S. Then the canonical projection π : S_U ⟶ [U/R] of Stacks 044R is surjective in the sense of Stacks 04XB: every algebraic space representing a base change of it along a scheme-valued point of [U/R] has surjective structural morphism.

No smoothness is needed: the source map of a groupoid is surjective because the identity arrow at a point of the object space is a preimage of that point.

theorem isRelativelySurjective {G : GroupoidInAlgebraicSpaces C S hS B} :
    HasRelativeProperty.{u, u + 1, u + 1, u} C S hS
      (Space.surjectiveMorphismProperty C S hS)
      (quotientStackProjectionHom G) (representable_quotientStackProjectionHom G)

AlgebraicGeometry.Stack.QuotientAtlas.isRelativelySmooth_isSurjective_of_bootstrap04S6, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothGroupoidQuotientAtlas.lean, line 128.

Stacks 04X0. Let G = (U, R, s, t, c) be a smooth groupoid in algebraic spaces over S. Then the canonical projection π : S_U ⟶ [U/R] of Stacks 044R is smooth and surjective in the sense of Stacks 04XB: it is representable by algebraic spaces, and every algebraic space representing a base change of it along a scheme-valued point of [U/R] has smooth and surjective structural morphism.

Representability is AlgebraicGeometry.Stack.representable_quotientStackProjectionHom (Stacks 04WZ and 045G); everything else is built, the 2-cartesian square of Stacks 04M9 by AlgebraicGeometry.Stack.QuotientAtlas.presentation.

theorem isRelativelySmooth_isSurjective_of_bootstrap04S6 {G : GroupoidInAlgebraicSpaces C S hS B}
    (hG : GroupoidInAlgebraicSpaces.IsSmooth C S hS G) :
    IsRelativelySmooth C S hS (quotientStackProjectionHom G) ∧
      HasRelativeProperty.{u, u + 1, u + 1, u} C S hS
        (Space.surjectiveMorphismProperty C S hS)
        (quotientStackProjectionHom G) (representable_quotientStackProjectionHom G)
Tag 04TK, a theorem

Tag 04TK in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/SmoothQuotientStackAlgebraic.lean, line 472.

Let S be a scheme contained in a big fppf site, and let G = (U, R, s, t, c) be a smooth groupoid in algebraic spaces over an algebraic space A over S. Then the quotient stack [U/R] is an algebraic stack over S.

theorem isAlgebraicStack_quotientStack_of_isSmooth
    {G : GroupoidInAlgebraicSpaces C S hS A}
    (hG : GroupoidInAlgebraicSpaces.IsSmooth C S hS G) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack G)

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_of_isSmooth_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/SmoothQuotientStackModel.lean, line 132.

Stacks 04TK. Let S be a scheme contained in a big fppf site and let G = (U, R, s, t, c) be a smooth groupoid in algebraic spaces over an algebraic space over S. Then the quotient stack [U/R] is an algebraic stack over S.

This is AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_of_isSmooth_of_bootstrap with part (3) of Stacks 04S6 supplied by AlgebraicGeometry.Stack.bootstrap04S6.

theorem isAlgebraicStack_quotientStack_of_isSmooth_unconditional
    {G : GroupoidInAlgebraicSpaces C S hS B} (hG : GroupoidInAlgebraicSpaces.IsSmooth C S hS G) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack G)

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStackOfAction_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothActionQuotientStackAlgebraic.lean, line 59. The attribute's comment: “the quotient stack of an action of a smooth group algebraic space”.

Stacks 04TK for a group action: if the structure morphism G ⟶ B of a group object in the slice of presheaves over B is smooth, then the quotient stack [X/G] of Stacks 044Q, part (2), is an algebraic stack over S.

theorem isAlgebraicStack_quotientStackOfAction_of_isSmooth
    (B : AlgebraicSpaces C S hS) (G X : Over B.obj) [GrpObj G] [ModObj G X]
    (hG : IsAlgebraicSpace C S hS G.left) (hX : IsAlgebraicSpace C S hS X.left)
    (hsm : Space.IsSmooth C S hS G.hom) :
    IsAlgebraicStack.{u, w} C S hS (quotientStackOfAction B G X hG hX)
Sources
LeanAlgebraicGeometry.Stack.smoothGroupoidAlgebraicStack · AlgebraicGeometry.Stack.hasRepresentableDiagonal_quotientStack · AlgebraicGeometry.Stack.QuotientAtlas.isRelativelySmooth · AlgebraicGeometry.Stack.QuotientAtlas.isRelativelySurjective · AlgebraicGeometry.Stack.QuotientAtlas.isRelativelySmooth_isSurjective_of_bootstrap04S6 · AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_of_isSmooth · AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_of_isSmooth_unconditional · AlgebraicGeometry.Stack.isAlgebraicStack_quotientStackOfAction_of_isSmooth

Section94.18 Change of big site#

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

Tag 04X2, a lemma

Tag 04X2 in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_pullbackStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBigSiteAlgebraicStack.lean, line 182. The attribute's comment: “part (3)”.

Stacks 04X2, part (3). Let B be a big fppf site contained in a larger one B', let S be a scheme of B and let f be the morphism of sites determined by the localized inclusion. The inverse image f⁻¹𝒳 of an algebraic stack 𝒳 over the localized big fppf site of S is an algebraic stack over the enlarged localized big fppf site.

theorem isAlgebraicStack_pullbackStack {B B' : BigFppfSite.{u}}
    (h : IsContained (τ := .fppf) B B') (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val) :
    letI : 𝒳.val.p.IsFibered := 𝒳.isFiberedInGroupoids.isFibered
    IsAlgebraicStack.{u, w} B' S (largerContains h hS) (pullbackStack h S hS 𝒳.val)

AlgebraicGeometry.Stack.isDeligneMumfordStack_pullbackStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBigSiteAlgebraicStack.lean, line 217. The attribute's comment: “part (4)”.

Stacks 04X2, part (4). Let B be a big fppf site contained in a larger one B', let S be a scheme of B and let f be the morphism of sites determined by the localized inclusion. The inverse image f⁻¹𝒳 of a Deligne-Mumford stack 𝒳 over the localized big fppf site of S is a Deligne-Mumford stack over the enlarged localized big fppf site. The inverse image is a stackification, whose morphisms are not small, so the conclusion is read with AlgebraicGeometry.Stack.IsDeligneMumfordStackUniv, the definition of Stacks 03YO for a total category in arbitrary universes.

The source's route: a surjective étale atlas of 𝒳 presents it as the quotient stack [U/R] of a groupoid whose source map is étale (Stacks 04T5, and Stacks 04XC at étaleness), the inverse image of that groupoid has étale source map, f⁻¹[U/R] = [f⁻¹U/f⁻¹R] (Stacks 04WX), and the quotient stack of a groupoid in algebraic spaces with étale source map is presented étale-ly by a scheme atlas of its object space followed by the canonical projection (Stacks 04X0 at étaleness).

theorem isDeligneMumfordStack_pullbackStack {B B' : BigFppfSite.{u}}
    (h : IsContained (τ := .fppf) B B') (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsDeligneMumfordStack.{u, w} B S hS 𝒳.val) :
    letI : 𝒳.val.p.IsFibered := 𝒳.isFiberedInGroupoids.isFibered
    IsDeligneMumfordStackUniv.{u, w} B' S (largerContains h hS) (pullbackStack h S hS 𝒳.val)

AlgebraicGeometry.Stack.pullbackStack_equivalenceOfSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBigSiteRepresentableStack.lean, line 256. The attribute's comment: “representability by an algebraic space: the inverse image of a stack represented by an algebraic space is represented by the inverse image of that same algebraic space”.

Stacks 04X2, representability by an algebraic space. A stack over the localized big fppf site of S represented by an algebraic space F has inverse image represented by the inverse image of F, that is by AlgebraicGeometry.changeBigSite applied to F.

theorem pullbackStack_equivalenceOfSpace (S : Scheme.{u}) (hS : B.Contains S)
    (F : AlgebraicSpaces B S hS) (𝒳 : BasedCategory.{u, u + 1} (BigFppfOver B S hS))
    (e : StacksRepresentableCFG.EquivalenceOver 𝒳.p
      (presheafOfCategories (F.obj ⋙ typeToCat)).p) :
    letI : 𝒳.p.IsFibered :=
      (StacksRepresentableCFG.isFiberedInGroupoids_of_equivalenceOver e
        (fibredCategory B S hS F.obj).property).isFibered
    Nonempty (StacksRepresentableCFG.EquivalenceOver (pullbackStack h S hS 𝒳).p
      (presheafOfCategories
        (((changeBigSite B B' h S hS).obj F).obj ⋙ typeToCat)).p)

AlgebraicGeometry.Stack.pullbackStack_representableBy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBigSiteRepresentableStack.lean, line 289. The attribute's comment: “representability by a scheme: the inverse image of a stack represented by a scheme of the smaller big fppf site is represented by that same scheme, read in the larger one”.

Stacks 04X2, representability by a scheme. A stack over the localized big fppf site of S represented by a scheme X of the smaller site has inverse image represented by the same scheme, read as an object of the larger localized site.

theorem pullbackStack_representableBy (S : Scheme.{u}) (hS : B.Contains S)
    (X : BigFppfOver B S hS) (𝒳 : BasedCategory.{u, u + 1} (BigFppfOver B S hS))
    (e : StacksRepresentableCFG.RepresentableBy 𝒳.p X) :
    letI : 𝒳.p.IsFibered :=
      (StacksRepresentableCFG.isFiberedInGroupoids_of_equivalenceOver e
        (Functor.IsFiberedInGroupoids.over_forget X)).isFibered
    Nonempty (StacksRepresentableCFG.RepresentableBy (pullbackStack h S hS 𝒳).p
      ((inclusionOver h S hS).obj X : BigFppfOver B' S (largerContains h hS)))
Tag 04X3, a lemma

Tag 04X3 in the Stacks Project.

AlgebraicGeometry.Stack.ChangeOfBigSite.pullbackPseudofunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBigSitePseudofunctor.lean, line 287. The attribute's comment: “the functor of 2-categories”.

The 2-functor 𝒳 ↦ f⁻¹𝒳 from the algebraic stacks over S for the smaller big fppf site to those for the larger one. Its value at 𝒳 is pullbackObj, equivalent over the larger site to the inverse image AlgebraicGeometry.Stack.pullbackStack of Stacks 04X2 (pullbackObjEquivalenceOver), and its value at a 1-morphism g : 𝒳 ⟶ 𝒴 is the 1-morphism f⁻¹𝒳 ⟶ f⁻¹𝒴 through which 𝒳 ⟶ 𝒴 ⥤ f⁻¹𝒴 factors by the universal property of 𝒳 ⥤ f⁻¹𝒳.

noncomputable def pullbackPseudofunctor :
    AlgebraicStacks.{u, w} B S hS ⥤ᵖ AlgebraicStacks.{u, w} B' S (largerContains h hS)

AlgebraicGeometry.Stack.ChangeOfBigSite.isEquivalence_mapFunctor_pullbackPseudofunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBigSitePseudofunctor.lean, line 299. The attribute's comment: “the equivalences of morphism categories”.

The 2-functor 𝒳 ↦ f⁻¹𝒳 induces equivalences of morphism categories Mor(𝒳, 𝒴) ≌ Mor(f⁻¹𝒳, f⁻¹𝒴).

theorem isEquivalence_mapFunctor_pullbackPseudofunctor (𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS) :
    ((pullbackPseudofunctor h S hS).mapFunctor 𝒳 𝒴).IsEquivalence

AlgebraicGeometry.Stack.hasChangeBigSitePresentation_of_isPullbackOfAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBigSiteStackEssentialImage.lean, line 205. The attribute's comment: “the characterization of the essential image, 'only if' half: a category over the enlarged localized big fppf site equivalent to the inverse image of an algebraic stack over the smaller one has a presentation by the inverse image of a smooth groupoid in algebraic spaces over the smaller site”.

Stacks 04X3, the "only if" half of the characterization of the essential image. If 𝒳' is equivalent over the enlarged localized big fppf site to the inverse image of an algebraic stack 𝒳 over the smaller site, then 𝒳' has a presentation [U'/R'] with U', R' the inverse images of U, R.

Stacks 04T5 presents 𝒳 as the quotient stack [U/R] of a smooth groupoid, Stacks 04WX identifies f⁻¹[U/R] with [f⁻¹U / f⁻¹R], the inverse image of an equivalence over the smaller site is an equivalence over the enlarged one, and the inverse image of a smooth groupoid is smooth. The presentation is the inverse-image groupoid itself, with the identity morphism.

theorem hasChangeBigSitePresentation_of_isPullbackOfAlgebraicStack
    (𝒳' : BasedCategory.{v, t} (BigFppfOver B' S (largerContains h hS)))
    (h𝒳' : IsPullbackOfAlgebraicStack.{u, w} h S hS 𝒳') :
    HasChangeBigSitePresentation h S hS 𝒳'

AlgebraicGeometry.Stack.isPullbackOfAlgebraicStack_of_hasChangeBigSitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBigSiteStackEssentialImage.lean, line 240. The attribute's comment: “the characterization of the essential image, 'if' half: a category over the enlarged localized big fppf site with a presentation by the inverse image of a smooth groupoid in algebraic spaces over the smaller site is equivalent to the inverse image of an algebraic stack over the smaller site”.

Stacks 04X3, the "if" half of the characterization of the essential image. If 𝒳' has a presentation [U'/R'] with U', R' the inverse images of U, R, then 𝒳' is equivalent over the enlarged localized big fppf site to the inverse image of an algebraic stack over the smaller site.

The isomorphism G' ≅ f⁻¹G identifies the quotient stacks (Stacks 046T) and makes f⁻¹G smooth; smoothness then descends to G (AlgebraicGeometry.isSmooth_of_changeBigSiteGroupoid_isSmooth). The quotient stack of G is an algebraic stack by Stacks 04TK; its small model AlgebraicGeometry.Stack.AlgebraicStacks.smallModel is an object of the 2-category of Stacks 03YP equivalent to it over the site; and Stacks 04WX identifies the inverse image of the quotient stack with the quotient stack of the inverse image.

theorem isPullbackOfAlgebraicStack_of_hasChangeBigSitePresentation
    (𝒳' : BasedCategory.{v, t} (BigFppfOver B' S (largerContains h hS)))
    (h𝒳' : HasChangeBigSitePresentation h S hS 𝒳') :
    IsPullbackOfAlgebraicStack.{u, w} h S hS 𝒳'

AlgebraicGeometry.Stack.isPullbackOfAlgebraicStack_iff_hasChangeBigSitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBigSiteStackEssentialImage.lean, line 264. The attribute's comment: “the characterization of the essential image”.

Stacks 04X3, the characterization of the essential image. A category 𝒳' over the enlarged localized big fppf site is equivalent to the inverse image f⁻¹𝒳 of an algebraic stack 𝒳 over the smaller site if and only if it has a presentation [U'/R'] with U', R' the inverse images of U, R for a groupoid (U, R, s, t, c) in algebraic spaces over the smaller site.

theorem isPullbackOfAlgebraicStack_iff_hasChangeBigSitePresentation
    (𝒳' : BasedCategory.{v, t} (BigFppfOver B' S (largerContains h hS))) :
    IsPullbackOfAlgebraicStack.{u, w} h S hS 𝒳' ↔ HasChangeBigSitePresentation h S hS 𝒳'
Sources
LeanAlgebraicGeometry.Stack.isAlgebraicStack_pullbackStack · AlgebraicGeometry.Stack.isDeligneMumfordStack_pullbackStack · AlgebraicGeometry.Stack.pullbackStack_equivalenceOfSpace · AlgebraicGeometry.Stack.pullbackStack_representableBy · AlgebraicGeometry.Stack.ChangeOfBigSite.pullbackPseudofunctor · AlgebraicGeometry.Stack.ChangeOfBigSite.isEquivalence_mapFunctor_pullbackPseudofunctor · AlgebraicGeometry.Stack.hasChangeBigSitePresentation_of_isPullbackOfAlgebraicStack · AlgebraicGeometry.Stack.isPullbackOfAlgebraicStack_of_hasChangeBigSitePresentation

Section94.19 Change of base scheme#

Section 94.19 of the Stacks Project, Tag 04X4. 4 tags here are carried by 40 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04X4, the section

Tag 04X4 in the Stacks Project.

AlgebraicGeometry.Stack.changeOfBaseFibreProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseSection.lean, line 92. The attribute's comment: “the 2-fibre product X'_S = (Sch/S)_fppf ×_{(Sch/S')_fppf} X', which is an algebraic stack over S' according to Lemma 04T2”.

The 2-fibre product 𝒳'_S = (Sch/S)_fppf ×_{(Sch/S')_fppf} 𝒳' of Section 04X4. For an algebraic stack 𝒳' over S', the apex of the canonical 2-fibre product square of the cospan formed by the structure 1-morphisms of the stack represented by S/S' (that is, (Sch/S)_fppf over S') and of 𝒳' to the final object (Sch/S')_fppf. It is an object of the 2-category of algebraic stacks over S', which is the source's appeal to Lemma 04T2.

def changeOfBaseFibreProduct (𝒳' : AlgebraicStacks.{u, w} B S' hS') :
    AlgebraicStacks.{u, w} B S' hS'

AlgebraicGeometry.Stack.changeOfBaseFibreProductProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseSection.lean, line 102. The attribute's comment: “the natural 1-morphism p : X'_S → (Sch/S)_fppf”.

The natural 1-morphism p : 𝒳'_S ⟶ (Sch/S)_fppf of Section 04X4: the projection of the 2-fibre product AlgebraicGeometry.Stack.changeOfBaseFibreProduct to its first factor, the stack represented by S/S'.

def changeOfBaseFibreProductProjection (𝒳' : AlgebraicStacks.{u, w} B S' hS') :
    changeOfBaseFibreProduct B S S' hS hS' g 𝒳' ⟶ schemeStack.{u, w} B S' hS' (Over.mk g)

AlgebraicGeometry.Stack.changeOfBaseFibreProductPair, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseSection.lean, line 113. The attribute's comment: “the pair (X'_S, p), an algebraic stack over S' with a 1-morphism to (Sch/S)_fppf, i.e. an object of the right-hand side of Lemma 04X5”.

The pair (𝒳'_S, p) of Section 04X4, as an object of the right-hand 2-category of Lemma 04X5: an algebraic stack over S' with a 1-morphism to the stack represented by S/S'.

def changeOfBaseFibreProductPair (𝒳' : AlgebraicStacks.{u, w} B S' hS') :
    AlgebraicStackPair.{u, w} B S S' hS hS' g

AlgebraicGeometry.Stack.changeOfBaseFibreProductOverBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseSection.lean, line 123. The attribute's comment: “by Lemma 04X5 the pair (X'_S, p) corresponds in a canonical way to an algebraic stack over S”.

The algebraic stack over S that (𝒳'_S, p) corresponds to (Section 04X4). The image of the pair AlgebraicGeometry.Stack.changeOfBaseFibreProductPair under the inverse of the bijection on objects of Lemma 04X5, that is, under Construction B.

def changeOfBaseFibreProductOverBase (𝒳' : AlgebraicStacks.{u, w} B S' hS') :
    AlgebraicStacks.{u, w} B S hS

AlgebraicGeometry.Stack.algebraicStackConstructionObjEquiv_changeOfBaseFibreProductOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseSection.lean, line 134. The attribute's comment: “the algebraic stack over S corresponds to (X'_S, p) under Lemma 04X5: Construction A returns X'_S over S' together with p”.

The correspondence of Lemma 04X5 carries the algebraic stack over S of Section 04X4 back to (𝒳'_S, p). Construction A applied to AlgebraicGeometry.Stack.changeOfBaseFibreProductOverBase returns the 2-fibre product 𝒳'_S over S' together with its natural 1-morphism p.

theorem algebraicStackConstructionObjEquiv_changeOfBaseFibreProductOverBase
    (𝒳' : AlgebraicStacks.{u, w} B S' hS') :
    algebraicStackConstructionObjEquiv.{u, w} B S S' hS hS' g
        (changeOfBaseFibreProductOverBase B S S' hS hS' g 𝒳') =
      changeOfBaseFibreProductPair B S S' hS hS' g 𝒳'

AlgebraicGeometry.Stack.changeOfBaseFibreProductOverBase_p, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseSection.lean, line 145. The attribute's comment: “the structure functor of that algebraic stack over S is p”.

The structure functor over S of the algebraic stack of Section 04X4 is the natural 1-morphism p : 𝒳'_S ⟶ (Sch/S)_fppf, read through the identification of the big fppf site of S with the localization of the big fppf site of S' at S/S'.

lemma changeOfBaseFibreProductOverBase_p (𝒳' : AlgebraicStacks.{u, w} B S' hS') :
    (changeOfBaseFibreProductOverBase B S S' hS hS' g 𝒳').val.val.p =
      (changeOfBaseFibreProductProjection B S S' hS hS' g 𝒳').hom.hom.toFunctor ⋙
        (Over.iteratedSliceEquiv (Over.mk g)).functor

Declarations registered for the tag:

Tag 04X5, a lemma

Tag 04X5 in the Stacks Project.

AlgebraicGeometry.Stack.exists_comp_p_eq_map_of_changeBase, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBase.lean, line 355. The attribute's comment: “the scheme-valued points of Construction A”.

The scheme-valued points of Construction A are those of the original category. Every scheme-valued point of changeBase 𝒳 over the big fppf site of S' is a scheme-valued point of 𝒳 over the big fppf site of S, on the same scheme, lying over a morphism to S whose composite with g is the structure morphism of the point's base.

This is the content of the source's remark that the statement of Stacks 04X5 makes sense because j : (Sch/S)_{fppf} ⟶ (Sch/S')_{fppf} is the localization functor at S/S': no information about the base is lost by Construction A. Together with AlgebraicGeometry.Stack.comp_changeBase_p_eq_map it matches up the quantifications over scheme-valued points in the two sides of the algebraicity criterion.

lemma exists_comp_p_eq_map_of_changeBase (𝒳 : BasedCategory.{v, t} (BigFppfOver B S hS))
    (V' : BigFppfOver B S' hS') (y : BigFppfOver B V'.left.1 V'.left.2 ⥤ 𝒳.obj)
    (hy : y ⋙ (changeBase B S S' hS hS' g 𝒳).p = Over.map V'.hom) :
    ∃ h : V'.left ⟶ B.obj hS, y ⋙ 𝒳.p = Over.map h ∧ h ≫ g = V'.hom

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_changeBaseFunctor_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBase.lean, line 394. The attribute's comment: “representability by algebraic spaces is unchanged by Construction A”.

Stacks 02ZW is unchanged by Construction A. A 1-morphism of categories over the big fppf site of S is representable by algebraic spaces exactly when the 1-morphism over the big fppf site of S' produced by Construction A is.

This is the second of the four clauses of Stacks 026O, in the form in which the clause is used: the clause itself is this statement for the diagonal. The proof is the two halves of the source's remark that j : (Sch/S)_{fppf} ⟶ (Sch/S')_{fppf} is the localization functor at S/S'. On points it is AlgebraicGeometry.Stack.comp_changeBase_p_eq_map and AlgebraicGeometry.Stack.exists_comp_p_eq_map_of_changeBase, which match up the quantifications over scheme-valued points of the target. On 2-fibre products it is CategoryTheory.TwoFibreProductOver.fstEquivalenceOver, which says that relocalizing the base does not change the 2-fibre product of a point with the 1-morphism, as an equivalence over the big fppf site of the point's scheme; so the representing algebraic space is literally the same on both sides, and no transport of algebraicity along a comparison is needed.

theorem isRepresentableByAlgebraicSpaces_changeBaseFunctor_iff
    {𝒳 : BasedCategory.{v, t} (BigFppfOver B S hS)}
    {𝒴 : BasedCategory.{v₂, t₂} (BigFppfOver B S hS)} (f : 𝒳 ⥤ᵇ 𝒴) :
    IsRepresentableByAlgebraicSpaces B S' hS' (changeBaseFunctor B S S' hS hS' g f) ↔
      IsRepresentableByAlgebraicSpaces B S hS f

AlgebraicGeometry.Stack.hasRelativeProperty_surjective_changeBaseHom_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBase.lean, line 504. The attribute's comment: “surjectivity of the presentation is unchanged by Construction A”.

Relative surjectivity is unchanged by Construction A. A 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces has the relative property of Stacks 03YK for surjectivity of morphisms of algebraic spaces exactly when the 1-morphism over the big fppf site of S' produced by Construction A has it.

This is the surjectivity half of the presentation clause of Stacks 026O, which is what Stacks 04X5 needs of it: that clause tests surjectivity and smoothness of the structural morphism of every algebraic space representing a base change of the presentation along a scheme-valued point of the stack, and for surjectivity that test is exactly AlgebraicGeometry.Stack.HasRelativeProperty at AlgebraicGeometry.Space.surjectiveMorphismProperty.

No statement about the lower-shriek extension of Stacks 03I5 part (2) is needed. Stacks 06D7 replaces the relative test by surjectivity on objects, Stacks 06D4, which AlgebraicGeometry.Stack.isSurjectiveOnObjects_changeBaseHom_iff transfers directly.

theorem hasRelativeProperty_surjective_changeBaseHom_iff
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom) :
    HasRelativeProperty.{u, v, w, vP} B S' hS' (Space.surjectiveMorphismProperty B S' hS')
        (changeBaseHom B S S' hS hS' g f)
        ((isRepresentableByAlgebraicSpaces_changeBaseFunctor_iff B S S' hS hS' g f.hom).2 hf) ↔
      HasRelativeProperty.{u, v, w, vP} B S hS (Space.surjectiveMorphismProperty B S hS) f hf

AlgebraicGeometry.Stack.hasRelativeProperty_smooth_changeBaseHom_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBase.lean, line 558. The attribute's comment: “smoothness of the presentation is unchanged by Construction A”.

A relative property tested on étale charts is unchanged by Construction A. Let Q be a property of morphisms of schemes. A 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces has the relative property of Stacks 03YK at the every-étale-chart condition of Stacks 03MJ for Q exactly when the 1-morphism over the big fppf site of S' produced by Construction A has it.

At Q = AlgebraicGeometry.Smooth this is the smoothness half of the presentation clause of Stacks 026O, the other half being AlgebraicGeometry.Stack.hasRelativeProperty_surjective_changeBaseHom_iff; that case is recovered by applying this statement to @AlgebraicGeometry.Smooth, since AlgebraicGeometry.Space.smoothMorphismProperty is the every-étale-chart condition at AlgebraicGeometry.Smooth. It is stated at a general Q because that is what the separation axioms of Stacks 04YW need of it: for instance AlgebraicGeometry.Space.IsLocallyQuasiFinite is the every-étale-chart condition at AlgebraicGeometry.LocallyOfFiniteType ⊓ AlgebraicGeometry.LocallyQuasiFinite, and nothing in the argument is about smoothness.

The relative property is written out as the quantifier of AlgebraicGeometry.Stack.HasRelativeProperty rather than through that abbreviation, exactly as AlgebraicGeometry.Stack.relativeProperty_baseChange and AlgebraicGeometry.Stack.relativeProperty_of_equivalences do: the abbreviation carries [P.IsStableUnderBaseChange] and [P.IsLocalAtTarget (Space.Topology.fppf.precoverage B S hS)] as instance arguments and neither is available for a general Q, while its body uses neither, so the quantifier is the same proposition carrying no hypothesis on the property.

Unlike surjectivity this really is a statement about the lower-shriek extension of Stacks 03I5 part (2), since smoothness has no objects-level criterion. The two quantifications match up by AlgebraicGeometry.Stack.comp_changeBase_p_eq_map and AlgebraicGeometry.Stack.exists_comp_p_eq_map_of_changeBase on scheme-valued points and by CategoryTheory.TwoFibreProductOver.fstEquivalenceOver on 2-fibre products, exactly as in AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_changeBaseFunctor_iff; so the representing algebraic space is the same object on both sides, living over the same scheme over S, and what is left is that its structural morphism has Q on every étale chart over S exactly when it does over S'. That is AlgebraicGeometry.Space.holdsOnEveryEtaleChart_spacesOverSmallerBaseFunctor_iff: the every-étale-chart condition of Stacks 03MJ for the structural morphism of the image of Stacks 04SG's forward functor does not depend on the base at all.

theorem hasRelativeProperty_smooth_changeBaseHom_iff (Q : MorphismProperty Scheme.{u})
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (f : 𝒳 ⟶ 𝒴)
    (_hf : IsRepresentableByAlgebraicSpaces B S hS f.hom) :
    (∀ (U : BigFppfOver B S' hS')
        (y : BigFppfOver B U.left.1 U.left.2 ⥤
          (changeBaseFiberedInGroupoids B S S' hS hS' g 𝒴).val.obj)
        (_hy : y ⋙ (changeBaseFiberedInGroupoids B S S' hS hS' g 𝒴).val.p = Over.map U.hom)
        (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom)
            (changeBaseFiberedInGroupoids B S S' hS hS' g 𝒳).val.p
            (changeBaseFiberedInGroupoids B S S' hS hS' g 𝒴).val.p y
            (CatFiberedInGroupoids.homFunctor (changeBaseHom B S S' hS hS' g f)))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.HoldsOnEveryEtaleChart B S' hS' Q
          (algebraicSpaceMap B S' hS' U
            ((spacesOverSmallerBaseFunctor B U.left.1 S' U.left.2 hS' U.hom).obj
              ⟨F, hF⟩)).hom) ↔
      (∀ (U : BigFppfOver B S hS)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
        (_hy : y ⋙ 𝒴.val.p = Over.map U.hom)
        (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.p 𝒴.val.p y
            (CatFiberedInGroupoids.homFunctor f))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.HoldsOnEveryEtaleChart B S hS Q
          (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj
              ⟨F, hF⟩)).hom)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_diagonalBasedFunctor_changeBase_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBase.lean, line 784. The attribute's comment: “representability of the diagonal is unchanged by Construction A”.

The diagonal clause of Stacks 026O is unchanged by Construction A. The diagonal of a category fibred in groupoids over the big fppf site of S is representable by algebraic spaces exactly when the diagonal of the category over the big fppf site of S' produced by Construction A is.

The two diagonals are not comparable directly: the self-product of changeBase 𝒳 over the big fppf site of S' has the strictly larger object set of pairs lying over a common S'-scheme by two different morphisms to S, so there is no equivalence to transport along. The route taken instead is Stacks 045G: by its conditions (1), (2) and (3) the clause is equivalent to AlgebraicGeometry.Stack.IsRepresentableFromSchemes, which does transfer (AlgebraicGeometry.Stack.isRepresentableFromSchemes_changeBase_iff), because a 1-morphism out of a scheme-valued point sees only one morphism to S at a time. The equalizer of the two morphisms, which a direct comparison of the self-products would have to form, is absorbed into the already-proved equivalence of conditions (2) and (3).

theorem isRepresentableByAlgebraicSpaces_diagonalBasedFunctor_changeBase_iff
    (𝒳 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)) :
    IsRepresentableByAlgebraicSpaces B S' hS'
        (diagonalBasedFunctor B S' hS' (changeBaseFiberedInGroupoids B S S' hS hS' g 𝒳)) ↔
      IsRepresentableByAlgebraicSpaces B S hS (diagonalBasedFunctor B S hS 𝒳)

AlgebraicGeometry.Stack.exists_factorization_of_isCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBase.lean, line 830. The attribute's comment: “the descent input of the stack clause of Construction A”.

A point of the big fppf site of S' covered by points coming from the site of S comes from the site of S itself. If the structure morphism of every member of a covering family of U' factors through g, and the factorizations agree on every pair of morphisms into two members agreeing over U', then the structure morphism of U' factors through g, compatibly with the given factorizations, and the factorization is unique by AlgebraicGeometry.Stack.eq_of_isCovering.

This is the descent input of the stack-in-groupoids clause of Stacks 026O for Construction A: an object of the total category of changeBase 𝒳 lying over U' lies over an object of the big fppf site of S, so gluing objects along a covering family of U' is only possible when U'.hom itself factors through g, and nothing short of the sheaf condition for the representable presheaf of S on the big fppf site produces that factorization.

theorem exists_factorization_of_isCovering {U' : BigFppfOver B S' hS'} {I : Type w}
    (Z : I → BigFppfOver B S' hS') (f : ∀ i, Z i ⟶ U')
    (hf : Sieve.ofArrows Z f ∈ BigFppfOver.topology B S' hS' U')
    (a : ∀ i, (Z i).left ⟶ B.obj hS) (ha : ∀ i, a i ≫ g = (Z i).hom)
    (hcompat : ∀ (i j : I) (Y : B.Schemes) (u : Y ⟶ (Z i).left) (v : Y ⟶ (Z j).left),
      u ≫ (f i).left = v ≫ (f j).left → u ≫ a i = v ≫ a j) :
    ∃ h : U'.left ⟶ B.obj hS, h ≫ g = U'.hom ∧ ∀ i, (f i).left ≫ h = a i

AlgebraicGeometry.Stack.isStackInGroupoids_of_changeBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBase.lean, line 862. The attribute's comment: “the stack clause transfers back along Construction A”.

The stack-in-groupoids clause of Stacks 026O transfers back along Construction A. If the category over the big fppf site of S' produced by Construction A is a stack in groupoids for the fppf topology there, then the original category over the big fppf site of S is a stack in groupoids for the fppf topology of that site.

This is one of the two implications of the third of the four clauses of Stacks 026O. Every piece of data over the site of S is read over the site of S' — covering families by CategoryTheory.Over.mem_over_map_iff, the fibre-product overlaps by CategoryTheory.Over.isPullback_map_iff, restrictions by CategoryTheory.Functor.Restriction.overMap, and descent data field by field — the hypothesis is applied there, and the conclusion is read back. The one step that is not formal is the object of the site of S that a glued object lies over: the hypothesis produces an object lying over the image of U, which determines its structure morphism only after composition with every member of the covering family, so AlgebraicGeometry.Stack.eq_of_isCovering is used to identify it with U.

The converse implication is AlgebraicGeometry.Stack.isStackInGroupoids_changeBase, and the two together are AlgebraicGeometry.Stack.isStackInGroupoids_changeBase_iff.

theorem isStackInGroupoids_of_changeBase (𝒳 : BasedCategory.{v, t} (BigFppfOver B S hS))
    (h : (changeBase B S S' hS hS' g 𝒳).p.IsStackInGroupoids.{w}
      (BigFppfOver.topology B S' hS')) :
    𝒳.p.IsStackInGroupoids.{w} (BigFppfOver.topology B S hS)

AlgebraicGeometry.Stack.isStackInGroupoids_changeBase_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBase.lean, line 903. The attribute's comment: “the stack clause of Stacks 026O is unchanged by Construction A”.

The stack-in-groupoids clause of Stacks 026O is unchanged by Construction A. A category over the big fppf site of S is a stack in groupoids for the fppf topology there exactly when the category over the big fppf site of S' produced by Construction A is a stack in groupoids for the fppf topology of that site.

This is the third of the four clauses of Stacks 026O, in full. The clause is read entirely in the two localized fppf topologies: a covering family of the site of S is one of the site of S' and conversely (CategoryTheory.Over.mem_over_map_iff and CategoryTheory.Over.mem_over_mk), and the fibre-product overlaps, the restrictions, the fibre isomorphisms and the descent data all match. The one non-formal ingredient is subcanonicity of the fppf topology, AlgebraicGeometry.BigFppfSite.subcanonical_topology, which is what pins down the morphism to S carried by an object of the site of S'.

theorem isStackInGroupoids_changeBase_iff (𝒳 : BasedCategory.{v, t} (BigFppfOver B S hS)) :
    (changeBase B S S' hS hS' g 𝒳).p.IsStackInGroupoids.{w}
        (BigFppfOver.topology B S' hS') ↔
      𝒳.p.IsStackInGroupoids.{w} (BigFppfOver.topology B S hS)

AlgebraicGeometry.Stack.isStack_changeBase_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBase.lean, line 930. The attribute's comment: “the sieve-indexed stack clause of Stacks 026O is unchanged by Construction A”.

The sieve-indexed stack clause of Stacks 026F is unchanged by Construction A. A category over the big fppf site of S is a stack in the sense of Stacks 026F for the fppf topology there exactly when the category over the big fppf site of S' produced by Construction A is one for the fppf topology of that site.

Unlike the family-indexed condition this needs no transfer of covering families and descent data at all: both sides are read through the single statement that the composite of the structure functor with the localization functor of the big fppf site of S is a stack over the whole big fppf site, by Constructions A and B of Stacks 04WV (CategoryTheory.Over.isStack_map_iff). Subcanonicity of the fppf topology (AlgebraicGeometry.BigFppfSite.subcanonical_topology) supplies the sheaf hypothesis of those two constructions for the representable presheaves of S and of S'.

The universes are those of Stacks 04X5 itself: Construction B relates two categories over the same site in the same universes, so the total category is taken in the object universe one above the scheme universe, which is what AlgebraicGeometry.Stack.IsAlgebraicStack is applied at.

theorem isStack_changeBase_iff (𝒳 : BasedCategory.{u, u + 1} (BigFppfOver B S hS)) :
    (changeBase B S S' hS hS' g 𝒳).p.IsStack (BigFppfOver.topology B S' hS') ↔
      𝒳.p.IsStack (BigFppfOver.topology B S hS)

AlgebraicGeometry.Stack.isAlgebraicStack_changeBase_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBase.lean, line 1159. The attribute's comment: “algebraicity criterion”.

The algebraicity criterion of Stacks 04X5. A category over the big fppf site of S is an algebraic stack over S exactly when the category over the big fppf site of S' produced by Construction A is an algebraic stack over S'. Together with the object, 1-morphism and 2-morphism equivalences of Stacks 04WV this is what restricts that isomorphism of 2-categories to algebraic stacks.

AlgebraicGeometry.Stack.IsAlgebraicStack is not a conjunction of the four clauses of Stacks 026O: the fibred-in-groupoids clause is existentially quantified ahead of the others, which are stated for the bundled category fibred in groupoids it produces. So the witness is transported first, by AlgebraicGeometry.Stack.isFiberedInGroupoids_changeBase_iff, and the bundled object on the S' side is then AlgebraicGeometry.Stack.changeBaseFiberedInGroupoids of the bundled object on the S side — the same underlying category over the site, paired with a proof of a proposition, so the two agree definitionally and the remaining clauses can be transported one by one:

  • the stack clause is AlgebraicGeometry.Stack.isStack_changeBase_iff in its sieve-indexed half and AlgebraicGeometry.Stack.isStackInGroupoids_changeBase_iff in its family-indexed half;
  • the diagonal clause is AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_diagonalBasedFunctor_changeBase_iff;
  • the presentation clause is the pair AlgebraicGeometry.Stack.hasRelativeProperty_surjective_changeBaseHom_iff and AlgebraicGeometry.Stack.hasRelativeProperty_smooth_changeBaseHom_iff, read through AlgebraicGeometry.Stack.forall_isSurjective_and_isSmooth_iff_hasRelativeProperty.

The presentation clause is the only one whose quantifiers move. A presentation of the stack over S' is a 1-morphism out of the category represented by an object U' of the site of S', and its mere existence forces U'.hom to factor through g, by the rigidity of relocalization (CategoryTheory.Over.exists_eq_map_of_comp_map); the slice of the site of S' over U' is then identified with the slice of the site of S over that factorization by AlgebraicGeometry.Stack.factorSliceFunctor, and in the other direction a presentation by U over S becomes one by (Over.map g).obj U over S' through AlgebraicGeometry.Stack.factorSliceInverse. Neither identification is an equality of categories, so the relative properties of Stacks 03YK have to be moved across it; that is AlgebraicGeometry.Stack.hasRelativeProperty_iff_of_equivalence_source.

The universes are those of Stacks 04X5: the total category is taken with object universe one above the scheme universe, which is where Construction B of Stacks 04WV — the one ingredient whose universes are pinned — applies.

theorem isAlgebraicStack_changeBase_iff (𝒳 : BasedCategory.{u, u + 1} (BigFppfOver B S hS)) :
    IsAlgebraicStack.{u, w} B S' hS' (changeBase B S S' hS hS' g 𝒳) ↔
      IsAlgebraicStack.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.isAlgebraicStack_of_changeBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseAlgebraicStack.lean, line 196. The attribute's comment: “algebraicity transfers back along Construction A”.

Stacks 04X5, the algebraic-stack clause in the direction Construction A reflects. Let g : S ⟶ S' be a morphism of a big fppf site and let 𝒳 be a category fibred in groupoids over the big fppf site of S. If the category over the big fppf site of S' produced by Construction A out of 𝒳 is an algebraic stack, then 𝒳 is an algebraic stack over S.

All four clauses of Stacks 026O are carried back: see the implementation notes. The descent universe of the conclusion is free, because the sieve-indexed conjunct of the stack clause does not depend on it.

theorem isAlgebraicStack_of_changeBase
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h : IsAlgebraicStack.{u, w'} B S' hS' (changeBase B S S' hS hS' g 𝒳.val)) :
    IsAlgebraicStack.{u, w} B S hS 𝒳.val

AlgebraicGeometry.Stack.isAlgebraicStack_changeBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseAlgebraicStack.lean, line 315. The attribute's comment: “algebraicity transfers along Construction A”.

Stacks 04X5, the algebraic-stack clause in the direction Construction A produces. Let g : S ⟶ S' be a morphism of a big fppf site and let 𝒳 be a category fibred in groupoids over the big fppf site of S. If 𝒳 is an algebraic stack over S, then the category over the big fppf site of S' produced by Construction A out of 𝒳 is an algebraic stack over S'.

This is the converse of AlgebraicGeometry.Stack.isAlgebraicStack_of_changeBase, and it is the statement that makes Stacks 04X6 a definition of an algebraic stack rather than merely of a category over the big fppf site of S'.

Three of the four clauses of Stacks 026O are the already-available biconditionals of StacksFrontier.AlgebraicGeometry.Stacks.ChangeOfBase, read in the forward direction: being fibred in groupoids is AlgebraicGeometry.Stack.isFiberedInGroupoids_changeBase_iff, the stack clause is AlgebraicGeometry.Stack.isStack_changeBase together with AlgebraicGeometry.Stack.isStackInGroupoids_changeBase_of_isStack, and the diagonal clause is AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_diagonalBasedFunctor_changeBase_iff. The descent universe of the conclusion is free, because the sieve-indexed conjunct of the stack clause does not depend on it and the family-indexed one is derived from it at any universe.

The presentation clause is easier in this direction than in the reflecting one, and this is the asymmetry of Construction A working in our favour. Reflection has to discover the presenting object of the site of S inside a presentation by an object of the site of S', which is what forces CategoryTheory.Over.exists_eq_map_of_comp_map there. Here the presenting object is simply pushed forward: a presentation of 𝒳 by U becomes a presentation of changeBase 𝒳 by (CategoryTheory.Over.map g).obj U, the two slices are identified by AlgebraicGeometry.Stack.factorSliceInverse — which is exactly AlgebraicGeometry.Stack.factorSliceFunctor taken in the direction that makes the comparison isomorphism of Stacks 0457 the identity — and representability and the two relative properties cross by AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_changeBaseFunctor_iff, AlgebraicGeometry.Stack.hasRelativeProperty_surjective_changeBaseHom_iff and AlgebraicGeometry.Stack.hasRelativeProperty_smooth_changeBaseHom_iff, followed by Stacks 0457 and 0459 in the source variable along that identification.

theorem isAlgebraicStack_changeBase
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h : IsAlgebraicStack.{u, w} B S hS 𝒳.val) :
    IsAlgebraicStack.{u, w'} B S' hS' (changeBase B S S' hS hS' g 𝒳.val)

AlgebraicGeometry.Stack.changeBaseStructureHom_toFunctor, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 222. The attribute's comment: “Construction A on 1-morphisms, as a functor”.

The underlying functor of AlgebraicGeometry.Stack.changeBaseStructureHom is the structure functor of 𝒳, read through the inverse of the iterated-slice equivalence. This is the object_structure clause of the correspondence of Stacks 04X5.

lemma changeBaseStructureHom_toFunctor (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    (changeBaseStructureHom B S S' hS hS' g 𝒳).hom.toFunctor =
      𝒳.val.val.p ⋙ (Over.iteratedSliceEquiv (Over.mk g)).inverse

AlgebraicGeometry.Stack.algebraicStackConstructionA_val_val, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 239. The attribute's comment: “Construction A on objects, on the underlying fibred category”.

The algebraic stack over S' underlying Construction A is Construction A of the underlying category over the big fppf site of S. This is the object_underlying clause of the correspondence of Stacks 04X5.

lemma algebraicStackConstructionA_val_val (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    (algebraicStackConstructionA B S S' hS hS' g 𝒳).1.val.val =
      changeBase B S S' hS hS' g 𝒳.val.val

AlgebraicGeometry.Stack.algebraicStackConstructionB_p, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 295. The attribute's comment: “Construction B on objects, on the projection”.

The structure functor produced by Construction B is the pair's 1-morphism to the stack represented by S/S', read through the iterated-slice equivalence.

lemma algebraicStackConstructionB_p (X : AlgebraicStackPair.{u, w} B S S' hS hS' g) :
    (algebraicStackConstructionB B S S' hS hS' g X).val.val.p =
      X.2.hom.toFunctor ⋙ (Over.iteratedSliceEquiv (Over.mk g)).functor

AlgebraicGeometry.Stack.algebraicStackConstructionObjEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 330. The attribute's comment: “the bijection on objects”.

Constructions A and B of Stacks 04X5 are mutually inverse on objects. An algebraic stack over S is the same thing as an algebraic stack over S' together with a 1-morphism to the stack represented by S/S'.

Both round trips are strict. In one direction nothing has to be done: the pair carries no information beyond its 1-morphism, and the iterated-slice equivalence composed the other way is the identity on the nose. In the other the structure functor of the pair's first component has to be recognized as the 1-morphism followed by the localization functor of S/S', which is what being a 1-morphism over S' says. The two algebraicity conditions agree by AlgebraicGeometry.Stack.isAlgebraicStack_changeBase_iff.

def algebraicStackConstructionObjEquiv :
    AlgebraicStacks.{u, w} B S hS ≃ AlgebraicStackPair.{u, w} B S S' hS hS' g

AlgebraicGeometry.Stack.algebraicStackConstructionHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 347. The attribute's comment: “the bijection on 1-morphisms”.

Constructions A and B of Stacks 04X5 are bijective on 1-morphisms, and both are the identity on the underlying functor. In one direction the commutation with the structure functors is composed with the relocalization functor and with the inverse iterated-slice equivalence; in the other it is recovered by composing the pair condition with the iterated-slice equivalence, which cancels on the nose.

def algebraicStackConstructionHomEquiv (𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS) :
    (𝒳 ⟶ 𝒴) ≃ AlgebraicStackPairHom B S S' hS hS' g
      (algebraicStackConstructionA B S S' hS hS' g 𝒳)
      (algebraicStackConstructionA B S S' hS hS' g 𝒴)

AlgebraicGeometry.Stack.algebraicStackConstructionHomEquiv_val_hom_toFunctor, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 369. The attribute's comment: “that bijection, on the underlying functor”.

The bijection on 1-morphisms is the identity on the underlying functor. This is the hom_underlying clause of the correspondence of Stacks 04X5; no heterogeneous equality is needed, the two functors having the same type.

lemma algebraicStackConstructionHomEquiv_val_hom_toFunctor
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (φ : 𝒳 ⟶ 𝒴) :
    (algebraicStackConstructionHomEquiv B S S' hS hS' g 𝒳 𝒴 φ).val.hom.toFunctor =
      φ.hom.hom.toFunctor

AlgebraicGeometry.Stack.algebraicStackConstructionHomEquiv_id, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 377. The attribute's comment: “that bijection carries the identity to the identity”.

Construction A preserves the identity 1-morphism.

lemma algebraicStackConstructionHomEquiv_id (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    algebraicStackConstructionHomEquiv B S S' hS hS' g 𝒳 𝒳 (𝟙 𝒳) =
      AlgebraicStackPairHom.id B S S' hS hS' g
        (algebraicStackConstructionA B S S' hS hS' g 𝒳)

AlgebraicGeometry.Stack.algebraicStackConstructionHomEquiv_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 385. The attribute's comment: “that bijection is compatible with composition”.

Construction A preserves composition of 1-morphisms.

lemma algebraicStackConstructionHomEquiv_comp {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS}
    (φ : 𝒳 ⟶ 𝒴) (ψ : 𝒴 ⟶ 𝒵) :
    algebraicStackConstructionHomEquiv B S S' hS hS' g 𝒳 𝒵 (φ ≫ ψ) =
      AlgebraicStackPairHom.comp B S S' hS hS' g
        (algebraicStackConstructionHomEquiv B S S' hS hS' g 𝒳 𝒴 φ)
        (algebraicStackConstructionHomEquiv B S S' hS hS' g 𝒴 𝒵 ψ)

AlgebraicGeometry.Stack.algebraicStackConstructionHom₂Equiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 398. The attribute's comment: “the bijection on 2-morphisms”.

Constructions A and B of Stacks 04X5 are bijective on 2-morphisms, and both are the identity on the underlying morphism of functors. The only thing to transfer is the condition that a component lie over an identity, and that is unchanged by the relocalization functor by CategoryTheory.Functor.isHomLift_overMap_iff.

def algebraicStackConstructionHom₂Equiv {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (φ ψ : 𝒳 ⟶ 𝒴) :
    (φ ⟶ ψ) ≃ AlgebraicStackPairHom₂ B S S' hS hS' g
      (algebraicStackConstructionHomEquiv B S S' hS hS' g 𝒳 𝒴 φ)
      (algebraicStackConstructionHomEquiv B S S' hS hS' g 𝒳 𝒴 ψ)

AlgebraicGeometry.Stack.algebraicStackConstructionHom₂Equiv_hom_toNatTrans, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 420. The attribute's comment: “the 2-morphism bijection, on the underlying natural transformation”.

The bijection on 2-morphisms is the identity on the underlying morphism of functors. This is the twoHom_underlying clause of the correspondence of Stacks 04X5.

lemma algebraicStackConstructionHom₂Equiv_hom_toNatTrans
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} {φ ψ : 𝒳 ⟶ 𝒴} (η : φ ⟶ ψ) :
    (algebraicStackConstructionHom₂Equiv B S S' hS hS' g φ ψ η).hom.toNatTrans =
      η.hom.hom.toNatTrans

AlgebraicGeometry.Stack.algebraicStackConstructionHom₂Equiv_id, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 428. The attribute's comment: “the 2-morphism bijection carries the identity to the identity”.

Construction A preserves identity 2-morphisms.

lemma algebraicStackConstructionHom₂Equiv_id {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS}
    (φ : 𝒳 ⟶ 𝒴) :
    algebraicStackConstructionHom₂Equiv B S S' hS hS' g φ φ (𝟙 φ) = 𝟙 _

AlgebraicGeometry.Stack.algebraicStackConstructionHom₂Equiv_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 435. The attribute's comment: “the 2-morphism bijection is compatible with vertical composition”.

Construction A preserves vertical composition of 2-morphisms.

lemma algebraicStackConstructionHom₂Equiv_comp {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS}
    {φ ψ χ : 𝒳 ⟶ 𝒴} (η : φ ⟶ ψ) (θ : ψ ⟶ χ) :
    algebraicStackConstructionHom₂Equiv B S S' hS hS' g φ χ (η ≫ θ) =
      algebraicStackConstructionHom₂Equiv B S S' hS hS' g φ ψ η ≫
        algebraicStackConstructionHom₂Equiv B S S' hS hS' g ψ χ θ

AlgebraicGeometry.Stack.algebraicStackConstructionHom₂Equiv_whiskerLeft, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 444. The attribute's comment: “the 2-morphism bijection is compatible with left whiskering”.

Construction A preserves left whiskering.

lemma algebraicStackConstructionHom₂Equiv_whiskerLeft
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (a : 𝒳 ⟶ 𝒴) {φ ψ : 𝒴 ⟶ 𝒵} (η : φ ⟶ ψ) :
    algebraicStackConstructionHom₂Equiv B S S' hS hS' g (a ≫ φ) (a ≫ ψ)
        (Bicategory.whiskerLeft a η) =
      Bicategory.whiskerLeft (algebraicStackConstructionHomEquiv B S S' hS hS' g 𝒳 𝒴 a).val
        (algebraicStackConstructionHom₂Equiv B S S' hS hS' g φ ψ η)

AlgebraicGeometry.Stack.algebraicStackConstructionHom₂Equiv_whiskerRight, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 454. The attribute's comment: “the 2-morphism bijection is compatible with right whiskering”.

Construction A preserves right whiskering.

lemma algebraicStackConstructionHom₂Equiv_whiskerRight
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} {φ ψ : 𝒳 ⟶ 𝒴} (η : φ ⟶ ψ) (a : 𝒴 ⟶ 𝒵) :
    algebraicStackConstructionHom₂Equiv B S S' hS hS' g (φ ≫ a) (ψ ≫ a)
        (Bicategory.whiskerRight η a) =
      Bicategory.whiskerRight (algebraicStackConstructionHom₂Equiv B S S' hS hS' g φ ψ η)
        (algebraicStackConstructionHomEquiv B S S' hS hS' g 𝒴 𝒵 a).val

AlgebraicGeometry.Stack.categoryOfAlgebraicStacksOverSmallerBaseScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean, line 534. The attribute's comment: “the resulting equivalence of 2-categories”.

Constructions A and B restrict to mutually inverse isomorphisms on objects, 1-morphisms and 2-morphisms of algebraic stacks. This is the whole of the correspondence of Stacks 04X5 as a single object, assembled from the components proved above; the algebraicity criterion AlgebraicGeometry.Stack.isAlgebraicStack_changeBase_iff is what makes its object map well defined in both directions.

noncomputable def categoryOfAlgebraicStacksOverSmallerBaseScheme :
    AlgebraicStackCorrespondence.{u, w} B S S' hS hS' g

AlgebraicGeometry.Stack.isAlgebraicStack_schemeFibredCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SchemeStack.lean, line 195. The attribute's comment: “the stack of a scheme of the big fppf site is algebraic”.

Stacks 026O for the big fppf site of a scheme over S. The big fppf site of a scheme X over S, read as a category fibred in groupoids over the big fppf site of S, is an algebraic stack.

It is representable by the algebraic space yoneda.obj X by Stacks 04SV, so it is a stack in groupoids and its diagonal is representable by algebraic spaces; the identity 1-morphism presents it, being representable by algebraic spaces by Stacks 02ZZ and surjective and smooth by AlgebraicGeometry.Stack.prop_identityPresentation.

Taken at X = S/S' for a morphism g : S ⟶ S' of the site, this is the clause of the 2-categorical correspondence of Stacks 04X5 asserting that the base of the right-hand 2-category is itself an algebraic stack over S'; the rest of that correspondence is in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseCorrespondence.lean.

theorem isAlgebraicStack_schemeFibredCategory (X : BigFppfOver B S hS) :
    IsAlgebraicStack.{u, w} B S hS (schemeFibredCategory B S hS X).val
Tag 04X6, a definition

Tag 04X6 in the Stacks Project.

AlgebraicGeometry.Stack.changeBaseAlgebraicStacks, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseAlgebraicStack.lean, line 381.

Stacks 04X6. An algebraic stack 𝒳 over S, viewed as an algebraic stack over S' along a morphism g : S ⟶ S' of the big fppf site: the algebraic stack over S' obtained by applying Construction A of Stacks 04X5 to 𝒳.

The underlying category and its structure functor are AlgebraicGeometry.Stack.changeBase, which composes the structure functor of 𝒳 with CategoryTheory.Over.map g; the content of the definition is that the result is again an algebraic stack, which is AlgebraicGeometry.Stack.isAlgebraicStack_changeBase.

def changeBaseAlgebraicStacks (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    AlgebraicStacks.{u, w'} B S' hS'
Tag 04X7, a definition

Tag 04X7 in the Stacks Project.

AlgebraicGeometry.Stack.baseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/BaseChangeAlgebraicStack.lean, line 177. The attribute's comment: “the construction”.

Stacks 04X7, the construction. The change of base of a category 𝒳' over the big fppf site of S' along g : S ⟶ S': the strict pullback of its structure functor along the relocalization functor of g, as a category over the big fppf site of S. An object is an object U of the big fppf site of S together with an object of 𝒳' lying over U/S', and the structure functor is the first projection.

def baseChange : BasedCategory.{u, u + 1} (BigFppfOver B S hS)

AlgebraicGeometry.Stack.baseChangeProductEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/BaseChangeAlgebraicStack.lean, line 361. The attribute's comment: “the change of base is the two-fibre product over the base”.

The image of the change of base under Construction A is the 2-fibre product 𝒳' ×_{S'} S. The identification is strict in one composite: an object of the strict pullback is carried to the triple consisting of its object of 𝒳', its object of the big fppf site of S read in the slice at S/S', and the defining equation of the strict pullback as the comparison 2-cell, and recovering the strict pullback from that triple returns it unchanged. In the other composite the object of the slice at S/S' is only recovered up to the unit of CategoryTheory.Over.iteratedSliceEquiv.

noncomputable def baseChangeProductEquivalence :
    BasedCategory.Equivalence (changeBase B S S' hS hS' g (baseChange B S S' hS hS' g 𝒳'))
      (baseChangeProduct B S S' hS hS' g 𝒳')

AlgebraicGeometry.Stack.isAlgebraicStack_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/BaseChangeAlgebraicStack.lean, line 396. The attribute's comment: “the change of base is an algebraic stack”.

Stacks 04X7. The change of base of an algebraic stack over S' along g : S ⟶ S' is an algebraic stack over S.

Its image under Construction A is the 2-fibre product 𝒳' ×_{S'} S, hence an algebraic stack over S' by Stacks 04TF; algebraicity is then carried back along Construction A by the direction of Stacks 04X5 proved in AlgebraicGeometry.Stack.isAlgebraicStack_of_changeBase.

theorem isAlgebraicStack_baseChange (h𝒳' : IsAlgebraicStack.{u, u + 1} B S' hS' 𝒳') :
    IsAlgebraicStack.{u, w} B S hS (baseChange B S S' hS hS' g 𝒳')

AlgebraicGeometry.Stack.changeOfBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseStack.lean, line 332.

The change of base of an algebraic stack 𝒳' over S' along a morphism S ⟶ S' of the big fppf site: the algebraic stack over S whose total category is the strict pullback of the structure functor of 𝒳' along the relocalization functor of g.

def changeOfBase (𝒳' : AlgebraicStacks.{u, w} B S' hS') :
    AlgebraicStacks.{u, w} B S hS

AlgebraicGeometry.Stack.changeOfBase_twoFibreProductWitness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChangeOfBaseStack.lean, line 425. The attribute's comment: “canonical two-fibre-product characterization”.

Under the canonical 2-categorical correspondence of Stacks 04X5 between algebraic stacks over S and algebraic stacks over S' equipped with a 1-morphism to the stack represented by S/S', the change of base of 𝒳' is the 2-fibre product of 𝒳' and the stack represented by S/S' over the stack represented by the final object S'/S'.

The two 1-morphisms to the base are the structure functor of 𝒳' and the forgetful functor of S/S' read through the iterated-slice equivalence, the apex is the correspondence's image of the change of base, the second projection is the correspondence's structural 1-morphism and the first is the projection of the strict pullback.

theorem changeOfBase_twoFibreProductWitness (𝒳' : AlgebraicStacks.{u, w} B S' hS') :
    Nonempty (ChangeOfBaseTwoFibreProductWitness B S S' hS hS' g 𝒳')
Sources
LeanAlgebraicGeometry.Stack.changeOfBaseFibreProduct · AlgebraicGeometry.Stack.changeOfBaseFibreProductProjection · AlgebraicGeometry.Stack.changeOfBaseFibreProductPair · AlgebraicGeometry.Stack.changeOfBaseFibreProductOverBase · AlgebraicGeometry.Stack.algebraicStackConstructionObjEquiv_changeOfBaseFibreProductOverBase · AlgebraicGeometry.Stack.changeOfBaseFibreProductOverBase_p · AlgebraicGeometry.Stack.changeBaseAlgebraicStack · AlgebraicGeometry.Stack.exists_comp_p_eq_map_of_changeBase

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.