97 Criteria for Representability

Chapter 97 of the Stacks Project, Criteria for Representability, Tag 05XE: the 16 sections of its 19 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 63 tags are carried by 142 declarations of the repository (all in StacksFrontier).

Section97.4 Morphisms of stacks in groupoids#

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

Tag 05XK, a lemma

Tag 05XK in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/EtalePermanence.lean, line 94. The attribute's comment: “representability”.

Stacks 05XK. Let f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 be 1-morphisms of categories fibred in groupoids over the big fppf site of S. If f ≫ g and g are representable by algebraic spaces, then so is f.

This is cancellation of a representable postcomposition, AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_of_postcomp, applied to the triangle formed by f, g and f ≫ g, whose comparison 2-cell is the identity.

theorem isRepresentableByAlgebraicSpaces_of_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsRepresentableByAlgebraicSpaces B S hS (f ≫ g).hom)
    (hg : IsRepresentableByAlgebraicSpaces B S hS g.hom) :
    IsRepresentableByAlgebraicSpaces B S hS f.hom

AlgebraicGeometry.Stack.isEtale_algebraicSpaceMap_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/EtalePermanence.lean, line 115. The attribute's comment: “étaleness”.

Stacks 05XK. Let f : 𝒳 ⟶ 𝒴 and g : 𝒴 ⟶ 𝒵 be 1-morphisms of categories fibred in groupoids over the big fppf site of S, with f ≫ g and g representable by algebraic spaces. If every algebraic space representing a base change of f ≫ g, respectively of g, along a scheme-valued point of 𝒵 has étale structural morphism, then so does every algebraic space representing a base change of f along a scheme-valued point of 𝒴.

Together with AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_of_comp this is the statement that an intervening 1-morphism of a factorization through an étale representable 1-morphism is itself representable and étale, in the sense of Stacks 04XB at AlgebraicGeometry.Space.IsEtale.

theorem isEtale_algebraicSpaceMap_of_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsRepresentableByAlgebraicSpaces B S hS (f ≫ g).hom)
    (hg : IsRepresentableByAlgebraicSpaces B S hS g.hom)
    (hEfg : ∀ (U : BigFppfOver B S hS)
      (z : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒵.val.obj)
      (_hz : z ⋙ 𝒵.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 z
          (CatFiberedInGroupoids.homFunctor (f ≫ g)))
        (presheafOfCategories (F ⋙ typeToCat)).p) →
      Space.IsEtale B S hS (algebraicSpaceMap B S hS U
        ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom)
    (hEg : ∀ (U : BigFppfOver B S hS)
      (z : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒵.val.obj)
      (_hz : z ⋙ 𝒵.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 z
          (CatFiberedInGroupoids.homFunctor g))
        (presheafOfCategories (F ⋙ typeToCat)).p) →
      Space.IsEtale B S hS (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.IsEtale B S hS (algebraicSpaceMap B S hS U
        ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

Tag 05XL, a lemma

Tag 05XL in the Stacks Project.

AlgebraicGeometry.Stack.isStackInSetoids_of_fppf_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/StackInSetoidsDescent.lean, line 202.

Stacks 05XL. Let 𝒳 ⟶ 𝒵 and 𝒴 ⟶ 𝒵 be 1-morphisms of categories fibred in groupoids over the big fppf site of S, with 𝒳 a stack. If 𝒴 and 𝒵 are represented by algebraic spaces Y and Z over S through chosen equivalences over the site, the morphism a : Y ⟶ Z these equivalences associate to 𝒴 ⟶ 𝒵 is surjective, flat and locally of finite presentation, and the 2-fibre product 𝒴 ×_𝒵 𝒳 is a stack in setoids, then 𝒳 is a stack in setoids.

theorem isStackInSetoids_of_fppf_baseChange
    {𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, u, u + 1, w} (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵)
    (h𝒳 : 𝒳.val.p.IsStack (BigFppfOver.topology B S hS))
    (Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z)
    (eY : StacksRepresentableCFG.EquivalenceOver 𝒴.val.p
      (presheafOfCategories (Y ⋙ typeToCat)).p)
    (eZ : StacksRepresentableCFG.EquivalenceOver 𝒵.val.p
      (presheafOfCategories (Z ⋙ typeToCat)).p)
    (a : Y ⟶ Z)
    (ha : ∀ y : 𝒴.val.obj,
      a.app (op (𝒴.val.p.obj y)) (PresheafOfCategories.sectionOfObj eY y rfl) =
        PresheafOfCategories.sectionOfObj eZ ((CatFiberedInGroupoids.homFunctor g).obj y)
          (Functor.congr_obj (CatFiberedInGroupoids.homFunctor_comp_p g) y))
    (hsurj : Space.IsSurjective B S hS a) (hflat : Space.IsFlat B S hS a)
    (hlfp : Space.IsLocallyOfFinitePresentation B S hS a)
    (hP : (TwoFibreProductOver.structureFunctor 𝒴.val.p 𝒳.val.p 𝒵.val.p
        (CatFiberedInGroupoids.homFunctor g) (CatFiberedInGroupoids.homFunctor f)).IsStackInSetoids
      (BigFppfOver.topology B S hS)) :
    𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS)

Tag 05XW, a lemma

Tag 05XW in the Stacks Project.

AlgebraicGeometry.Stack.hasRepresentableDiagonal_of_flatPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatPresentationRepresentableDiagonal.lean, line 174.

Let u : 𝒰 ⟶ 𝒳 be a 1-morphism of categories fibred in groupoids over the big fppf site of S with 𝒳 a stack, 𝒰 representable by an algebraic space and u representable by algebraic spaces, surjective, flat and locally of finite presentation. Then the diagonal of 𝒳 is representable by algebraic spaces.

theorem hasRepresentableDiagonal_of_flatPresentation (u : 𝒰 ⟶ 𝒳)
    (h𝒳 : 𝒳.val.p.IsStack (BigFppfOver.topology B S hS))
    (h𝒰 : IsRepresentableByAlgebraicSpace B S hS 𝒰)
    (hu : IsRepresentableByAlgebraicSpaces B S hS u.hom)
    (hsurj : HasRelativeProperty B S hS (Space.surjectiveMorphismProperty B S hS) u hu)
    (hflat : @HasRelativeProperty.{u, u, u + 1, u + 1} B S hS
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (k : X ⟶ Y) => Space.IsFlat B S hS k.hom)
      (Space.isFlat_isStableUnderBaseChange B S hS)
      ((Space.isFlat_isLocalAtTarget_fpqc B S hS).of_le
        (Space.fppfPrecoverage_le_fpqcPrecoverage B S hS))
      𝒰 𝒳 u hu)
    (hlfp : HasRelativeProperty B S hS
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (k : X ⟶ Y) =>
        Space.IsLocallyOfFinitePresentation B S hS k.hom) u hu) :
    HasRepresentableDiagonal B S hS 𝒳

Tag 07WG, a lemma

Tag 07WG in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_secondDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SecondDiagonalCriterion.lean, line 724.

Stacks 07WG. The second diagonal of a category fibred in groupoids 𝒳 over the big fppf site of S — the relative diagonal of its diagonal — is representable by algebraic spaces if and only if, for every representable category fibred in groupoids 𝒱 over the site and every 1-morphism g : 𝒱 ⟶ 𝒳 × 𝒳, the diagonal of the base change 𝒴 = 𝒳 ×_{Δ, 𝒳 × 𝒳, g} 𝒱 is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_secondDiagonal_iff :
    IsRepresentableByAlgebraicSpaces B S hS
      (relativeDiagonalBasedFunctor B S hS 𝒳 (CatFiberedInGroupoids.product 𝒳 𝒳)
        (diagonalBasedFunctor B S hS 𝒳)) ↔
    ∀ (𝒱 : CatFiberedInGroupoids.{u, max u v', u + 1, max (u + 1) w'}
        (BigFppfOver B S hS))
      (_h𝒱 : Stacks.RepresentableMorphism.IsRepresentableCFG 𝒱.val.p)
      (g : 𝒱.val ⥤ᵇ (CatFiberedInGroupoids.product 𝒳 𝒳).val),
      let 𝒴 := twoFibreProduct B S hS (CatFiberedInGroupoids.product 𝒳 𝒳) 𝒳 𝒱
        (diagonalBasedFunctor B S hS 𝒳) g
      IsRepresentableByAlgebraicSpaces B S hS (diagonalBasedFunctor B S hS 𝒴)

Sources

• Section 97.4, Tag 05XJ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_of_comp · AlgebraicGeometry.Stack.isEtale_algebraicSpaceMap_of_comp · AlgebraicGeometry.Stack.isStackInSetoids_of_fppf_baseChange · AlgebraicGeometry.Stack.hasRepresentableDiagonal_of_flatPresentation · AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_secondDiagonal_iff

Section97.5 Limit preserving on objects#

Section 97.5 of the Stacks Project, Tag 06CT. 7 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06CU, an equation

Tag 06CU in the Stacks Project.

AlgebraicGeometry.BigFppfOver.IsLimitPreservingOnObjects, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/LimitPreservingOnObjects.lean, line 67.

Stacks 06CU. A morphism of categories fibred in groupoids is limit preserving on objects: every comparison over an affine inverse limit descends, with the comparison square commuting.

def IsLimitPreservingOnObjects
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 : CatFiberedInGroupoids (BigFppfOver B S hS)) (p : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.isLimitPreservingOnObjects_fibredCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/LimitPreservingPresheafStack.lean, line 71. The attribute's comment: “the criterion for the category fibred in sets attached to a set-valued presheaf: limit preservation on objects of its structure morphism follows from descent of the presheaf's sections along inverse limits of affine objects”.

If every section of F over an inverse limit of affine objects of the site descends to a stage below a prescribed index, then the structure morphism of the category 𝒮_F fibred in sets attached to F is limit preserving on objects.

public theorem isLimitPreservingOnObjects_fibredCategory (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : DescendsOnAffineLimits.{u, v, w} B S hS F) :
    BigFppfOver.IsLimitPreservingOnObjects.{u, v, w} B S hS
      (fibredCategory B S hS F)
      (Deformation.Artin.Approximation.baseFiberedCategory B S hS)
      (Deformation.Artin.Approximation.structureMorphism B S hS
        (fibredCategory B S hS F))

Tag 06CV, a lemma

Tag 06CV in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isLimitPreservingOnObjects_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/LimitPreservingOnObjects.lean, line 127.

Stacks 06CV. Limit preservation on objects is stable under base change.

theorem isLimitPreservingOnObjects_baseChange
    (hp : IsLimitPreservingOnObjects.{u, v, w} B S hS 𝒳 𝒴 p) :
    IsLimitPreservingOnObjects.{u, v, w} B S hS
      (twoFibreProduct B S hS 𝒳 𝒴 𝒵 p q) 𝒵
      (twoFibreProductSnd B S hS 𝒳 𝒴 𝒵 p q)

Tag 06CW, a lemma

Tag 06CW in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isLimitPreservingOnObjects_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/LimitPreservingOnObjects.lean, line 286.

Stacks 06CW. The composite of two morphisms of categories fibred in groupoids that are limit preserving on objects is limit preserving on objects.

theorem isLimitPreservingOnObjects_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 𝒵 : CatFiberedInGroupoids (BigFppfOver B S hS))
    (p : 𝒳 ⟶ 𝒴) (q : 𝒴 ⟶ 𝒵)
    (hp : IsLimitPreservingOnObjects.{u, v, w} B S hS 𝒳 𝒴 p)
    (hq : IsLimitPreservingOnObjects.{u, v, w} B S hS 𝒴 𝒵 q) :
    IsLimitPreservingOnObjects.{u, v, w} B S hS 𝒳 𝒵 (p ≫ q)

Tag 06CX, a lemma

Tag 06CX in the Stacks Project.

AlgebraicGeometry.Stack.isLimitPreservingOnObjects_iff_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/LimitPreservingFinitePresentation.lean, line 883. The attribute's comment: “index categories in the universe of the schemes”.

Stacks 06CX. A 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces is limit preserving on objects exactly when it is locally of finite presentation in the sense of Stacks 03YK: every algebraic space representing a base change of it along a scheme-valued point of the target has locally finitely presented structural morphism.

theorem isLimitPreservingOnObjects_iff_isLocallyOfFinitePresentation
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 : CatFiberedInGroupoids (AlgebraicGeometry.BigFppfOver B S hS))
    (p : 𝒳 ⟶ 𝒴)
    (hp : AlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpaces B S hS p.hom) :
    AlgebraicGeometry.BigFppfOver.IsLimitPreservingOnObjects.{u, u, u} B S hS 𝒳 𝒴 p ↔
      ∀ (U : AlgebraicGeometry.BigFppfOver B S hS)
        (y : AlgebraicGeometry.BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
        (_hy : y ⋙ 𝒴.val.p = Over.map U.hom)
        (F : (AlgebraicGeometry.BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hF : AlgebraicGeometry.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 p))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        AlgebraicGeometry.Space.IsLocallyOfFinitePresentation B S hS
          (AlgebraicGeometry.algebraicSpaceMap B S hS U
            ((AlgebraicGeometry.spacesOverSmallerBaseFunctor
              B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

Tag 06CY, a lemma

Tag 06CY in the Stacks Project.

AlgebraicGeometry.Stack.isLimitPreservingOnObjects_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/LimitPreservingOpenImmersion.lean, line 116. The attribute's comment: “index categories in the universe of the schemes, which is the scope of the formalized form of Tag 06CX that the proof uses. Limit preservation on objects for a larger index universe is a strictly stronger condition, so it does not follow from the pinned form; it is isLimitPreservingOnObjects_of_isOpenImmersion_of_criterion, which takes Tag 06CX at those universes as a hypothesis”.

Stacks 06CY. A 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces and an open immersion in the sense of Stacks 04XB is limit preserving on objects.

An open immersion of algebraic spaces is locally of finite presentation, so the relative open-immersion property of Stacks 03YK implies the relative property of being locally of finite presentation; Stacks 06CX turns the latter into limit preservation on objects.

theorem isLimitPreservingOnObjects_of_isOpenImmersion
    (p : 𝒳 ⟶ 𝒴) (hp : IsRepresentableByAlgebraicSpaces B S hS p.hom)
    (hopen : IsOpenImmersion B S hS p) :
    BigFppfOver.IsLimitPreservingOnObjects.{u, u, u} B S hS 𝒳 𝒴 p

Tag 07WH, a lemma

Tag 07WH in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_of_limitPreservingOnObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/LimitPreservingOnObjectsCriteria/Representability.lean, line 572.

Stacks 07WH. Let S be a scheme of a big fppf site, let T be an object of the big fppf site of S and put κ = size T. A 1-morphism f : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf site of S is representable by algebraic spaces as soon as

• the structure morphism 𝒴 ⟶ (Sch/S)_{fppf} is limit preserving on objects,
• for every affine V locally of finite presentation over S and every point y of 𝒴 over V, the 2-fibre product (Sch/V)_{fppf} ×_{y, 𝒴} 𝒳 is representable by an algebraic space carrying a surjective étale atlas by a scheme of size at most κ, and
• 𝒳 and 𝒴 are stacks in groupoids for the big Zariski topology over S.

The bound by the size of a single object of the site is the source's set-theoretic hypothesis; it is what makes the coproduct of the charts of an open cover again an object of the site.

public theorem isRepresentableByAlgebraicSpaces_of_limitPreservingOnObjects
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (T : AlgebraicGeometry.BigFppfOver B S hS)
    (𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1}
      (AlgebraicGeometry.BigFppfOver B S hS))
    (f : 𝒳 ⟶ 𝒴)
    (hlimit : AlgebraicGeometry.BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1} B S hS 𝒴
      (AlgebraicGeometry.Stack.terminalCFG B S hS)
      (Bicategory.InducedBicategory.mkHom (AlgebraicGeometry.Stack.toTerminalCFG B S hS 𝒴)))
    (hlocal : ∀ (U : AlgebraicGeometry.BigFppfOver B S hS),
      IsAffine U.left.1 →
      LocallyOfFinitePresentation (B.inclusion.map U.hom) →
      let 𝒰 := AlgebraicGeometry.BigFppfOver B U.left.1 U.left.2
      let p𝒰 : 𝒰 ⥤ AlgebraicGeometry.BigFppfOver B S hS := Over.map U.hom
      ∀ (y : 𝒰 ⥤ 𝒴.val.obj) (_hy : y ⋙ 𝒴.val.p = p𝒰),
        ∃ F : 𝒰ᵒᵖ ⥤ Type u,
          AlgebraicGeometry.IsAlgebraicSpace B U.left.1 U.left.2 F ∧
          Nonempty (StacksRepresentableCFG.EquivalenceOver
            (TwoFibreProductOver.fst p𝒰 𝒳.val.p 𝒴.val.p y
              (CatFiberedInGroupoids.homFunctor f))
            (presheafOfCategories (F ⋙ typeToCat)).p) ∧
          ∃ (A : 𝒰) (a : yoneda.obj A ⟶ F),
            A.left.1.size ≤ T.left.1.size ∧
            (MorphismProperty.presheaf
              (MorphismProperty.inverseImage
                (@Surjective.{u} : MorphismProperty Scheme.{u})
                (AlgebraicGeometry.BigFppfOver.toScheme B U.left.1 U.left.2))) a ∧
            (MorphismProperty.presheaf
              (MorphismProperty.inverseImage
                (@Etale.{u} : MorphismProperty Scheme.{u})
                (AlgebraicGeometry.BigFppfOver.toScheme B U.left.1 U.left.2))) a)
    (h𝒳 : 𝒳.val.p.IsStackInGroupoids.{u + 1}
      ((AlgebraicGeometry.BigFppfSite.zariskiTopology B).over (B.obj hS)))
    (h𝒴 : 𝒴.val.p.IsStackInGroupoids.{u + 1}
      ((AlgebraicGeometry.BigFppfSite.zariskiTopology B).over (B.obj hS))) :
    AlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom

Tag 07WI, a lemma

Tag 07WI in the Stacks Project.

AlgebraicGeometry.Stack.hasRelativeProperty_of_affine_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingRepresentable.lean, line 2177.

A base-change-stable, fppf-local property of a representable morphism can be checked on affine bases locally of finite presentation when the target is limit preserving on objects.

public theorem hasRelativeProperty_of_affine_locallyOfFinitePresentation
    (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, u} B S hS)]
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1}
      (BigFppfOver B S hS)}
    (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hlimit : BigFppfOver.IsLimitPreservingOnObjects.{u, max u vI, max u wI, u, u + 1}
      B S hS 𝒴 (terminalCFG B S hS)
      (Bicategory.InducedBicategory.mkHom
        (toTerminalCFG B S hS 𝒴)))
    (hlocal : ∀ (U : BigFppfOver B S hS),
      IsAffine U.left.1 →
      LocallyOfFinitePresentation (B.inclusion.map U.hom) →
      ∀ (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) →
        P (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor
            B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩))) :
    HasRelativeProperty B S hS P f hf

Sources

• Section 97.5, Tag 06CT
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.BigFppfOver.IsLimitPreservingOnObjects · AlgebraicGeometry.Stack.isLimitPreservingOnObjects_fibredCategory · AlgebraicGeometry.BigFppfOver.isLimitPreservingOnObjects_baseChange · AlgebraicGeometry.BigFppfOver.isLimitPreservingOnObjects_comp · AlgebraicGeometry.Stack.isLimitPreservingOnObjects_iff_isLocallyOfFinitePresentation · AlgebraicGeometry.Stack.isLimitPreservingOnObjects_of_isOpenImmersion · AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_of_limitPreservingOnObjects · AlgebraicGeometry.Stack.hasRelativeProperty_of_affine_locallyOfFinitePresentation

Section97.6 Formally smooth on objects#

Section 97.6 of the Stacks Project, Tag 06CZ. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06D0, an equation

Tag 06D0 in the Stacks Project.

AlgebraicGeometry.Stack.IsFormallySmoothOnObjects, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FormallySmoothOnObjects.lean, line 53.

The first-order lifting condition for a 1-morphism of categories fibred in groupoids, with the comparison square required to commute: the restriction along a first-order thickening of affine objects is the chosen pullback CategoryTheory.Functor.pullbackFiber.

def IsFormallySmoothOnObjects
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w}
      (BigFppfOver B S hS)) (p : 𝒳 ⟶ 𝒴) : Prop

Tag 06D1, a lemma

Tag 06D1 in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/FormallySmoothOnObjects.lean, line 199.

Stacks 06D1. Formal smoothness on objects is stable under base change.

theorem isFormallySmoothOnObjects_baseChange
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, max u v, u + 1, max (u + 1) v w}
      (BigFppfOver B S hS))
    (p : 𝒳 ⟶ 𝒴) (q : 𝒵 ⟶ 𝒴)
    (hp : Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒴 p) :
    Stack.IsFormallySmoothOnObjects B S hS
      (twoFibreProduct B S hS 𝒳 𝒴 𝒵 p q) 𝒵
      (twoFibreProductSnd B S hS 𝒳 𝒴 𝒵 p q)

Tag 06D2, a lemma

Tag 06D2 in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/FormallySmoothOnObjects.lean, line 413.

Stacks 06D2. A composite of morphisms formally smooth on objects is formally smooth on objects.

theorem isFormallySmoothOnObjects_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS))
    (p : 𝒳 ⟶ 𝒴) (q : 𝒴 ⟶ 𝒵)
    (hp : Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒴 p)
    (hq : Stack.IsFormallySmoothOnObjects B S hS 𝒴 𝒵 q) :
    Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒵 (p ≫ q)

Tag 06D3, a lemma

Tag 06D3 in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isRelativelyFormallySmooth_of_isFormallySmoothOnObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/FormallySmoothOnObjects.lean, line 727. The attribute's comment: “formally smooth on objects implies formally smooth”.

Stacks 06D3, that (1) implies (2): a 1-morphism of categories fibred in groupoids over the big fppf site of S which is formally smooth on objects is formally smooth, that is, every algebraic space representing a base change of it along a scheme-valued point of the target has formally smooth structural morphism.

Representability by algebraic spaces, which the source assumes throughout, is not needed for this implication: the lifting problem of formal smoothness is transported to a lifting problem for objects of the 2-fibre product through whatever equivalence with the category of elements of the representing space is supplied.

theorem isRelativelyFormallySmooth_of_isFormallySmoothOnObjects
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (p : 𝒳 ⟶ 𝒴)
    (hobj : Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒴 p) :
    IsRelativelyFormallySmooth B S hS p

AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_of_isRelativelyFormallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/FormallySmoothOnObjects.lean, line 1367. The attribute's comment: “formally smooth implies formally smooth on objects”.

Stacks 06D3, that (2) implies (1): a 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces and formally smooth is formally smooth on objects.

Representability is used here, and twice: to produce an algebraic space representing the base change of p along the scheme-valued point of 𝒴 classifying the given object, which is where the hypothesis is applied, and through the 2-Yoneda classifying functor of Stacks 02Y4 that turns that object into such a point.

theorem isFormallySmoothOnObjects_of_isRelativelyFormallySmooth
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (p : 𝒳 ⟶ 𝒴)
    (hp : Stack.IsRepresentableByAlgebraicSpaces B S hS p.hom)
    (hform : IsRelativelyFormallySmooth B S hS p) :
    Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒴 p

AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_iff_isRelativelyFormallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/FormallySmoothOnObjects.lean, line 1383. The attribute's comment: “the equivalence”.

Stacks 06D3. For a 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces, being formally smooth on objects and being formally smooth — the relative property of Stacks 03YK at formal smoothness, by AlgebraicGeometry.BigFppfOver.isRelativelyFormallySmooth_iff_hasRelativeProperty — are equivalent.

theorem isFormallySmoothOnObjects_iff_isRelativelyFormallySmooth
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (p : 𝒳 ⟶ 𝒴)
    (hp : Stack.IsRepresentableByAlgebraicSpaces B S hS p.hom) :
    Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒴 p ↔ IsRelativelyFormallySmooth B S hS p

Sources

• Section 97.6, Tag 06CZ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.IsFormallySmoothOnObjects · AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_baseChange · AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_comp · AlgebraicGeometry.BigFppfOver.isRelativelyFormallySmooth_of_isFormallySmoothOnObjects · AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_of_isRelativelyFormallySmooth · AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_iff_isRelativelyFormallySmooth

Section97.7 Surjective on objects#

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

Tag 06D5, a lemma

Tag 06D5 in the Stacks Project.

AlgebraicGeometry.Stack.isSurjectiveOnObjects_twoFibreProductSnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SurjectiveOnObjects.lean, line 94.

Stacks 06D5. Surjectivity on objects is preserved by base change: if p : 𝒳 ⟶ 𝒴 is surjective on objects then so is the second projection 𝒳 ×_𝒴 𝒵 ⟶ 𝒵 of its base change along any q : 𝒵 ⟶ 𝒴.

theorem isSurjectiveOnObjects_twoFibreProductSnd
    (𝒳 𝒴 𝒵 : CatFiberedInGroupoids.{u, max u v, u + 1, max (u + 1) v w}
      (BigFppfOver B S hS))
    (p : 𝒳 ⟶ 𝒴) (q : 𝒵 ⟶ 𝒴)
    (h : IsSurjectiveOnObjects B S hS 𝒳.val.p 𝒴.val.p
      (CatFiberedInGroupoids.homFunctor p)) :
    IsSurjectiveOnObjects B S hS
      (CatFiberedInGroupoids.twoFibreProductSquare p q).pt.val.p 𝒵.val.p
      (CatFiberedInGroupoids.homFunctor
        (CatFiberedInGroupoids.twoFibreProductSquare p q).snd)

Tag 06D6, a lemma

Tag 06D6 in the Stacks Project.

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

Stacks 06D6. A composite of two 1-morphisms surjective on objects is surjective on objects: compose the two field extensions.

theorem isSurjectiveOnObjects_comp
    {X : Type uX} [Category.{vX} X] {Y : Type uY} [Category.{vY} Y]
    {Z : Type uZ} [Category.{vZ} Z]
    (pX : X ⥤ BigFppfOver B S hS) (pY : Y ⥤ BigFppfOver B S hS)
    (pZ : Z ⥤ BigFppfOver B S hS) (F : X ⥤ Y) (G : Y ⥤ Z) (hG : G ⋙ pZ = pY)
    (hFsurj : IsSurjectiveOnObjects B S hS pX pY F)
    (hGsurj : IsSurjectiveOnObjects B S hS pY pZ G) :
    IsSurjectiveOnObjects B S hS pX pZ (F ⋙ G)

Tag 06D7, a lemma

Tag 06D7 in the Stacks Project.

AlgebraicGeometry.Stack.isSurjectiveOnObjects_iff_isRelativelySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SurjectiveOnObjectsRelative.lean, line 388.

Stacks 06D7. A 1-morphism of categories fibred in groupoids over the big fppf site of S which is representable by algebraic spaces is surjective on objects in the sense of Stacks 06D4 exactly when it has the relative property of Stacks 03YK for surjectivity of morphisms of algebraic spaces.

theorem isSurjectiveOnObjects_iff_isRelativelySurjective
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)}
    (p : 𝒳 ⟶ 𝒴) (hp : IsRepresentableByAlgebraicSpaces B S hS p.hom) :
    IsSurjectiveOnObjects B S hS 𝒳.val.p 𝒴.val.p (CatFiberedInGroupoids.homFunctor p) ↔
      HasRelativeProperty B S hS (Space.surjectiveMorphismProperty B S hS) p hp

Sources

• Section 97.7, Tag 06D4
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isSurjectiveOnObjects_twoFibreProductSnd · AlgebraicGeometry.Stack.isSurjectiveOnObjects_comp · AlgebraicGeometry.Stack.isSurjectiveOnObjects_iff_isRelativelySurjective

Section97.8 Algebraic morphisms#

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

Tag 06CF, a definition

Tag 06CF in the Stacks Project.

AlgebraicGeometry.Stack.IsAlgebraicMorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicMorphism.lean, line 44.

A morphism of stacks is algebraic if every base change along a scheme-valued point of its target is an algebraic stack.

abbrev IsAlgebraicMorphism.{u, wX, wY, w, vX, uX, vY, uY}
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : StackInGroupoids.{wX, u, vX, u + 1, uX}
      (BigFppfOver B S hS)
      (BigFppfOver.topology B S hS)}
    {𝒴 : StackInGroupoids.{wY, u, vY, u + 1, uY}
      (BigFppfOver B S hS)
      (BigFppfOver.topology B S hS)}
    (f : 𝒳.toBasedCategory ⥤ᵇ 𝒴.toBasedCategory) : Prop

Tag 05XY, a lemma

Tag 05XY in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_of_isAlgebraicMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicMorphismSourceAlgebraic.lean, line 88.

Let F : 𝒳 ⟶ 𝒴 be a 1-morphism of stacks in groupoids over the big fppf site of S. If 𝒴 is an algebraic stack and F is algebraic in the sense of Stacks 06CF, then 𝒳 is an algebraic stack.

theorem isAlgebraicStack_of_isAlgebraicMorphism
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : StackInGroupoids.{w, u, u, u + 1, u + 1}
      (BigFppfOver B S hS) (BigFppfOver.topology B S hS)}
    (f : 𝒳 ⟶ 𝒴)
    (h𝒳 : 𝒳.toBasedCategory.p.IsStack (BigFppfOver.topology B S hS))
    (h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴.toBasedCategory)
    (hf : IsAlgebraicMorphism.{u, w, w, w} B S hS (𝒳 := 𝒳) (𝒴 := 𝒴) f.hom) :
    IsAlgebraicStack.{u, w} B S hS 𝒳.toBasedCategory

Tag 06CG, a lemma

Tag 06CG in the Stacks Project.

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

Stacks 06CG. Let F : 𝒳 ⟶ 𝒴 be a 1-morphism of stacks in groupoids over the big fppf site of S. If 𝒳 is an algebraic stack and the diagonal of 𝒴 is representable by algebraic spaces, then F is algebraic in the sense of Stacks 06CF.

theorem isAlgebraicMorphism_of_isAlgebraicStack
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : StackInGroupoids.{w, u, u, u + 1, u + 1}
      (BigFppfOver B S hS) (BigFppfOver.topology B S hS)}
    (f : 𝒳 ⟶ 𝒴)
    (h𝒴 : 𝒴.toBasedCategory.p.IsStack (BigFppfOver.topology B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.toBasedCategory)
    (hΔ : HasRepresentableDiagonal B S hS
      (CatFiberedInGroupoids.mk 𝒴.toBasedCategory
        𝒴.isStackInGroupoids.isFiberedInGroupoids)) :
    IsAlgebraicMorphism.{u, w, w, w} B S hS (𝒳 := 𝒳) (𝒴 := 𝒴) f.hom

Tag 0D3R, a lemma

Tag 0D3R in the Stacks Project.

AlgebraicGeometry.Stack.hasRepresentableDiagonal_of_isAlgebraicMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AlgebraicMorphismRepresentableDiagonal.lean, line 111.

Stacks 0D3R. An algebraic 1-morphism of stacks in groupoids over the big fppf site of S inherits a diagonal representable by algebraic spaces from its target.

theorem hasRepresentableDiagonal_of_isAlgebraicMorphism
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : StackInGroupoids.{w, u, u, u + 1, u + 1}
      (BigFppfOver B S hS) (BigFppfOver.topology B S hS)}
    (f : 𝒳 ⟶ 𝒴)
    (hf : IsAlgebraicMorphism.{u, w, w, w'} B S hS (𝒳 := 𝒳) (𝒴 := 𝒴) f.hom)
    (h𝒴 : HasRepresentableDiagonal B S hS
      (CatFiberedInGroupoids.mk 𝒴.toBasedCategory
        𝒴.isStackInGroupoids.isFiberedInGroupoids)) :
    HasRepresentableDiagonal B S hS
      (CatFiberedInGroupoids.mk 𝒳.toBasedCategory
        𝒳.isStackInGroupoids.isFiberedInGroupoids)

Sources

• Section 97.8, Tag 05XX
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.IsAlgebraicMorphism · AlgebraicGeometry.Stack.isAlgebraicStack_of_isAlgebraicMorphism · AlgebraicGeometry.Stack.isAlgebraicMorphism_of_isAlgebraicStack · AlgebraicGeometry.Stack.hasRepresentableDiagonal_of_isAlgebraicMorphism

Section97.9 Spaces of sections#

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

Tag 05XQ, a lemma

Tag 05XQ in the Stacks Project.

AlgebraicGeometry.Space.isSurjective_restrictionOfScalars_projection_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartComparisonAssembly.lean, line 317. The attribute's comment: “surjectivity of Res_{Z_U/U}(W) ⟶ U for Z_U a base change of a finite locally free morphism of algebraic spaces”.

Stacks 05XQ for the fibre data of Stacks 05YD. Let z : Z ⟶ Q be a finite locally free morphism of algebraic spaces over S, let U be an object of the big fppf category over S, let Z_U be an algebraic space exhibited as a base change U ×_{a, Q} Z of z, and let w : W ⟶ Z_U be surjective and étale. Then the restriction of scalars Res_{Z_U/U}(W) ⟶ U is surjective.

Stacks 05XQ is formalized at a morphism of the site whose underlying morphism of schemes is finite, as AlgebraicGeometry.Space.isSurjective_restrictionOfScalars_projection. Here Z_U is only isomorphic to a representable presheaf: z is affine, hence representable, so the chosen represented base change ψ : Z' ⟶ U of z along a identifies Z_U with yoneda.obj Z', and ψ is finite as a morphism of schemes by AlgebraicGeometry.Space.isFinite_of_isPullback_of_isFiniteLocallyFree. Transporting the section produced over Z' back along that identification gives a pair of Stacks 05Y9 over a surjective base change of U, which is what surjectivity of the projection asks for.

theorem isSurjective_restrictionOfScalars_projection_of_isPullback
    {Z Q : AlgebraicSpaces B S hS} (z : Z ⟶ Q) (hz : IsFiniteLocallyFree B S hS z)
    (U : BigFppfOver B S hS) (ZU W : AlgebraicSpaces B S hS)
    (ζ : ZU ⟶ (⟨yoneda.obj U, isAlgebraicSpace_yoneda B S hS U⟩ : AlgebraicSpaces B S hS))
    (w : W ⟶ ZU) (a : yoneda.obj U ⟶ Q.obj) (ι : ZU.obj ⟶ Z.obj)
    (sq : IsPullback ζ.hom ι a z.hom)
    (hw_surjective : IsSurjective B S hS w.hom) (hw_etale : IsEtale B S hS w.hom) :
    IsSurjective B S hS (restrictionOfScalars B S hS w ζ).projection

AlgebraicGeometry.Space.exists_surjective_etale_sectionsOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionSpaces.lean, line 331.

Stacks 05XQ. Let Z → U be a finite morphism of schemes, let W be an algebraic space over U and let w : W → Z be surjective and étale. Then there is a surjective étale morphism T → U together with a section of W_T → Z_T.

theorem Space.exists_surjective_etale_sectionsOver (B : BigFppfSite.{u}) (U : Scheme.{u})
    (hU : B.Contains U) (Z : BigFppfOver B U hU) [IsFinite (B.inclusion.map Z.hom)]
    (W : (BigFppfOver B U hU)ᵒᵖ ⥤ Type u) (w : W ⟶ yoneda.obj Z)
    (hW : IsAlgebraicSpace B U hU W) (hw_surjective : Space.IsSurjective B U hU w)
    (hw_etale : Space.IsEtale B U hU w) :
    ∃ T : BigFppfOver B U hU, Surjective (B.inclusion.map T.hom) ∧
      Etale (B.inclusion.map T.hom) ∧ Nonempty (Space.SectionsOver B U hU Z T W w)

AlgebraicGeometry.Space.isSurjective_restrictionOfScalars_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionSpaces.lean, line 468. The attribute's comment: “surjectivity of Res_{Z/U}(W) ⟶ U for Z ⟶ U finite”.

Stacks 05XQ. Let ζ : Z ⟶ U be a morphism of the big fppf site of S whose underlying morphism of schemes is finite, let W be an algebraic space over S and let w : W ⟶ Z be surjective and étale. Then the restriction of scalars Res_{Z/U}(W) ⟶ U of Stacks 05YA — the functor assigning to T a morphism T ⟶ U together with a section of W_T ⟶ Z_T — is surjective.

A point of U is hit by a point of Res_{Z/U}(W) because the base change τ : T ⟶ U of AlgebraicGeometry.Space.exists_surjective_etale_section_of_isFinite carries a section, so h_T ⟶ U factors through Res_{Z/U}(W), and τ is surjective on points.

theorem Space.isSurjective_restrictionOfScalars_projection (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) {U Z : BigFppfOver B S hS} (ζ : Z ⟶ U)
    [IsFinite ((BigFppfOver.toScheme B S hS).map ζ)] (W : AlgebraicSpaces B S hS)
    (w : W ⟶ (schemeSpace Z : AlgebraicSpaces B S hS))
    (hw_surjective : Space.IsSurjective B S hS w.hom)
    (hw_etale : Space.IsEtale B S hS w.hom) :
    Space.IsSurjective B S hS
      (Space.restrictionOfScalars B S hS w
        (ObjectProperty.homMk (yoneda.map ζ) :
          (schemeSpace Z : AlgebraicSpaces B S hS) ⟶
            schemeSpace U)).projection

AlgebraicGeometry.Space.exists_surjective_etale_sectionOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionSpacesOverBase.lean, line 90.

Stacks 05XQ over a base object of the site. Let ζ : Z ⟶ U be a morphism of the big fppf site of S whose underlying morphism of schemes is finite, let W be an algebraic space over S and let w : W ⟶ h_Z be surjective and étale. Then there is an object T of the big fppf site of S and a morphism r : T ⟶ U, surjective and étale on underlying schemes, together with a section of W ⟶ h_Z over T ×_U Z, that is a morphism h_{T ×_U Z} ⟶ W whose composite with w is the projection to h_Z.

theorem Space.exists_surjective_etale_sectionOverBase (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (U Z : BigFppfOver B S hS) (ζ : Z ⟶ U)
    (hζ : IsFinite ((BigFppfOver.toScheme B S hS).map ζ))
    (W : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (w : W ⟶ yoneda.obj Z)
    (hW : IsAlgebraicSpace B S hS W) (hw_surjective : Space.IsSurjective B S hS w)
    (hw_etale : Space.IsEtale B S hS w) :
    ∃ (T : BigFppfOver B S hS) (r : T ⟶ U),
      Surjective ((BigFppfOver.toScheme B S hS).map r) ∧
      Etale ((BigFppfOver.toScheme B S hS).map r) ∧
      ∃ σ : pullback (yoneda.map r) (yoneda.map ζ) ⟶ W,
        σ ≫ w = pullback.snd (yoneda.map r) (yoneda.map ζ)

Tag 05XR, a lemma

Tag 05XR in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_isEtale_restrictionOfScalars_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreSectionsAlgebraicEtale.lean, line 310. The attribute's comment: “the restriction of scalars of a base change of a finite locally free morphism along an étale morphism is an algebraic space étale over the base”.

Stacks 05XR for the fibre data of Stacks 05YD and Stacks 05Y5. Let z : Z ⟶ Q be a finite locally free morphism of algebraic spaces over S, let U be an object of the big fppf category over S, let Z_U be an algebraic space exhibited as a base change U ×_{a, Q} Z of z and let w : W ⟶ Z_U be an étale morphism of algebraic spaces over S. Then the restriction of scalars Res_{Z_U/U}(W) is an algebraic space over S and its projection to U is étale.

theorem isAlgebraicSpace_isEtale_restrictionOfScalars_of_isPullback
    {Z Q : AlgebraicSpaces B S hS} (z : Z ⟶ Q) (hz : IsFiniteLocallyFree B S hS z)
    (U : BigFppfOver B S hS) (ZU W : AlgebraicSpaces B S hS)
    (ζ : ZU ⟶ (schemeSpace U : AlgebraicSpaces B S hS))
    (w : W ⟶ ZU) (a : yoneda.obj U ⟶ Q.obj) (ι : ZU.obj ⟶ Z.obj)
    (sq : IsPullback ζ.hom ι a z.hom) (hw : IsEtale B S hS w.hom) :
    IsAlgebraicSpace B S hS (restrictionOfScalars B S hS w ζ).presheaf ∧
      IsEtale B S hS (restrictionOfScalars B S hS w ζ).projection

AlgebraicGeometry.Space.isAlgebraicSpace_restrictionOfScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IsFibreSectionsGeneral.lean, line 180. The attribute's comment: “algebraic space”.

Stacks 05XR, the algebraic space. The restriction of scalars Res_{Z/Q}(X) of an étale x : X ⟶ Z along a finite z : Z ⟶ Q is an algebraic space over S.

The source states this for z finite locally free and for Q an object of the site; finiteness of z is all that is used, and Q is an arbitrary algebraic space over S.

theorem isAlgebraicSpace_restrictionOfScalars (hx : IsEtale B S hS x.hom)
    (hz : IsFinite B S hS z.hom) :
    IsAlgebraicSpace B S hS (restrictionOfScalars B S hS x z).presheaf

AlgebraicGeometry.Space.isEtale_projection_restrictionOfScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IsFibreSectionsGeneral.lean, line 200. The attribute's comment: “étale morphism”.

Stacks 05XR, the étale morphism. The projection Res_{Z/Q}(X) ⟶ Q of the restriction of scalars of an étale x : X ⟶ Z along a finite z : Z ⟶ Q is étale.

The source states this for z finite locally free and for Q an object of the site; finiteness of z is all that is used, and Q is an arbitrary algebraic space over S.

theorem isEtale_projection_restrictionOfScalars (hx : IsEtale B S hS x.hom)
    (hz : IsFinite B S hS z.hom) :
    IsEtale B S hS (restrictionOfScalars B S hS x z).projection

AlgebraicGeometry.Space.exists_sectionSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionSpace.lean, line 177. The attribute's comment: “the functor”.

The natural, small-valued functor of sections of W → Z of Stacks 05XR exists: there is a presheaf on the big fppf site of U whose value at T is the set of sections of W_T → Z_T, naturally in T, the restriction maps being base change. Stacks 05XR itself is AlgebraicGeometry.Space.isAlgebraicSpace_sectionSpace_and_isEtale.

theorem exists_sectionSpace (Z : BigFppfOver B U hU)
    (W : (BigFppfOver B U hU)ᵒᵖ ⥤ Type u) (w : W ⟶ yoneda.obj Z) :
    ∃ F : (BigFppfOver B U hU)ᵒᵖ ⥤ Type u,
      ∃ e : ∀ T : BigFppfOver B U hU, F.obj (Opposite.op T) ≃
          SectionsOver B U hU Z T W w,
        ∀ (T T' : BigFppfOver B U hU) (f : T' ⟶ T)
          (s : F.obj (Opposite.op T)),
          ((e T') (F.map f.op s)).1 =
            prod.map (yoneda.map f) (𝟙 (yoneda.obj Z)) ≫ ((e T) s).1

AlgebraicGeometry.Space.isAlgebraicSpace_sectionSpace_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionSpaceChartSurjectiveEtale.lean, line 450. The attribute's comment: “the space of sections is an algebraic space, with no separatedness”.

Stacks 05XR, the algebraicity of the space of sections, in general. Let Z ⟶ U be a morphism of the big fppf site of U whose underlying morphism of schemes is finite, and let w : W ⟶ h_Z be an étale morphism of presheaves with W an algebraic space over U. Then the space of sections of W_T ⟶ Z_T is an algebraic space over U.

No separatedness is assumed: a surjective étale chart of W whose scheme is separated exists by Stacks 03FX, and along such a chart the comparison of the spaces of sections is surjective and étale by AlgebraicGeometry.Space.isEtale_and_isSurjective_of_isPullback_sectionSpaceMap.

theorem isAlgebraicSpace_sectionSpace_of_isEtale (hW : IsAlgebraicSpace B U hU W)
    (hw : IsEtale B U hU w)
    (hZfin : _root_.AlgebraicGeometry.IsFinite (B.inclusion.map Z.hom)) :
    IsAlgebraicSpace B U hU (sectionSpace B U hU Z W w)

AlgebraicGeometry.Space.isEtale_sectionSpace_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionSpaceChartSurjectiveEtale.lean, line 461. The attribute's comment: “the space of sections is étale over the base, with no separatedness”.

Stacks 05XR, the étaleness of the space of sections over the base, in general. Under the hypotheses of AlgebraicGeometry.Space.isAlgebraicSpace_sectionSpace_of_isEtale the structure morphism of the space of sections to U is étale.

theorem isEtale_sectionSpace_of_isEtale (hW : IsAlgebraicSpace B U hU W)
    (hw : IsEtale B U hU w)
    (hZfin : _root_.AlgebraicGeometry.IsFinite (B.inclusion.map Z.hom)) :
    IsEtale B U hU (terminal.from (sectionSpace B U hU Z W w))

AlgebraicGeometry.Space.isAlgebraicSpace_sectionSpace_and_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SectionSpaceEtale.lean, line 618.

Stacks 05XR. Let Z ⟶ U be a finite morphism of schemes, let W be an algebraic space over U and let w : W ⟶ Z be étale. Then the functor of sections of W_T ⟶ Z_T over T/U is an algebraic space, and its structure morphism to U is étale.

The source asks Z ⟶ U to be finite locally free; only finiteness is used.

theorem isAlgebraicSpace_sectionSpace_and_isEtale (hW : IsAlgebraicSpace B U hU W)
    (hw : IsEtale B U hU w) (hZfin : _root_.AlgebraicGeometry.IsFinite (B.inclusion.map Z.hom)) :
    IsAlgebraicSpace B U hU (sectionSpace B U hU Z W w) ∧
      IsEtale B U hU (terminal.from (sectionSpace B U hU Z W w))

Sources

• Section 97.9, Tag 05XZ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isSurjective_restrictionOfScalars_projection_of_isPullback · AlgebraicGeometry.Space.exists_surjective_etale_sectionsOver · AlgebraicGeometry.Space.isSurjective_restrictionOfScalars_projection · AlgebraicGeometry.Space.exists_surjective_etale_sectionOverBase · AlgebraicGeometry.Space.isAlgebraicSpace_isEtale_restrictionOfScalars_of_isPullback · AlgebraicGeometry.Space.isAlgebraicSpace_restrictionOfScalars · AlgebraicGeometry.Space.isEtale_projection_restrictionOfScalars · AlgebraicGeometry.Space.exists_sectionSpace

Section97.10 Relative morphisms#

Section 97.10 of the Stacks Project, Tag 05Y0. 6 tags here are carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05Y1, an equation

Tag 05Y1 in the Stacks Project.

AlgebraicGeometry.Space.RelativeMorphism, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeMorphism.lean, line 231. The attribute's comment: “the pair (a, b) of the diagram”.

Stacks 05Y1. A pair (a, b) for the relative morphism functor of z : Z ⟶ Q and x : X ⟶ Q at a test presheaf T: a morphism a : T ⟶ Q together with a morphism b : T ×_{a, Q} Z ⟶ X lying over Q. The source's other description of b, as a morphism T ×_{a, Q} Z ⟶ T ×_{a, Q} X over T, is equivalent to this one.

structure RelativeMorphism (Z X Q : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (z : Z ⟶ Q) (x : X ⟶ Q)
    (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)

AlgebraicGeometry.Space.RelativeMorphismDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeMorphism.lean, line 347. The attribute's comment: “the displayed diagram: b : T ×_{a, B} Z ⟶ T ×_{a, B} X over T”.

Stacks 05Y1. The diagram of a pair at a test presheaf T, in the shape the source displays it: a morphism a : T ⟶ Q together with a morphism b : T ×_{a, Q} Z ⟶ T ×_{a, Q} X over T, that is, commuting with the two projections to T.

This is the first of the source's two descriptions of a pair; the second, AlgebraicGeometry.Space.RelativeMorphism, reads b instead as a morphism T ×_{a, Q} Z ⟶ X lying over Q. The two are the same data — AlgebraicGeometry.Space.relativeMorphismEquivDiagram.

structure RelativeMorphismDiagram (Z X Q : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (z : Z ⟶ Q)
    (x : X ⟶ Q) (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)

Tag 05Y2, an equation

Tag 05Y2 in the Stacks Project.

AlgebraicGeometry.Space.relativeHomData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeMorphism.lean, line 513.

Stacks 05Y2. The relative morphism functor Mor_Q(Z, X) of two morphisms z : Z ⟶ Q and x : X ⟶ Q of algebraic spaces over S: a small-valued presheaf on the big fppf site of S whose sections over a scheme T are the pairs (a, b) of Stacks 05Y1, with its projection to Q and with restriction given by base change.

The three algebraicity hypotheses are kept because the source states the functor for algebraic spaces, but they are not used: smallness of the values comes from essential smallness of the site (AlgebraicGeometry.locallySmall_presheaf_bigFppfOver), not from the existence of an étale atlas.

noncomputable def relativeHomData (Z X Q : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (z : Z ⟶ Q)
    (x : X ⟶ Q) (_hZ : IsAlgebraicSpace B S hS Z) (_hX : IsAlgebraicSpace B S hS X)
    (_hQ : IsAlgebraicSpace B S hS Q) : RelativeHomConstruction B S hS Z X Q z x

Tag 05Y3, a lemma

Tag 05Y3 in the Stacks Project.

AlgebraicGeometry.Space.relativeHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeMorphismHom.lean, line 669. The attribute's comment: “part (2): the canonical bijection between the morphisms from an algebraic space T into Mor_B(Z, X) and the pairs (a, b) of Stacks 05Y1 at T”.

Stacks 05Y3, part (2). For a test object T — in the source an algebraic space over S — the morphisms T ⟶ Mor_Q(Z, X) are canonically the pairs (a, b) of Stacks 05Y1 at T: a morphism a : T ⟶ Q together with a morphism b : T ×_{a, Q} Z ⟶ X over Q.

The bijection extends the identification of the sections over a scheme with pairs (AlgebraicGeometry.Space.relativeHomEquiv_yoneda) and is natural in T (AlgebraicGeometry.Space.relativeHomEquiv_naturality); the algebraicity of T is recorded because the source states the bijection for algebraic spaces, but it is not used.

noncomputable def relativeHomEquiv (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (_hT : IsAlgebraicSpace B S hS T) :
    (T ⟶ relativeHom B S hS Z X Q z x hZ hX hQ) ≃ RelativeMorphism B S hS Z X Q z x T

AlgebraicGeometry.Space.isSheaf_relativeHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeMorphismSheaf.lean, line 269. The attribute's comment: “part (1): the relative morphism functor Mor_B(Z, X) is a sheaf on the big fppf site of S”.

Stacks 05Y3, part (1). For morphisms z : Z ⟶ Q and x : X ⟶ Q of algebraic spaces over S, the relative morphism functor Mor_Q(Z, X) of Stacks 05Y2 is a sheaf on the big fppf site of S.

theorem isSheaf_relativeHom (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (Z X Q : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (z : Z ⟶ Q) (x : X ⟶ Q)
    (hZ : IsAlgebraicSpace B S hS Z) (hX : IsAlgebraicSpace B S hS X)
    (hQ : IsAlgebraicSpace B S hS Q) :
    Presheaf.IsSheaf (BigFppfOver.topology B S hS)
      (relativeHom B S hS Z X Q z x hZ hX hQ)

Tag 05Y4, a lemma

Tag 05Y4 in the Stacks Project.

AlgebraicGeometry.Space.isPullback_sheaf_relativeHomOfBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RelativeMorphismBaseChange.lean, line 581. The attribute's comment: “the identification in Sh((Sch/S)_fppf), with the sheaf property of the two relative morphism functors — part (1) of the cited Stacks 05Y3 — carried as a hypothesis”.

Stacks 05Y4. The identification

Mor_{Q'}(Z', X') = Q' ×_Q Mor_Q(Z, X)

in Sh((Sch/S)_fppf): the square of fppf sheaves formed by the two projections reading off the first component of a pair of Stacks 05Y1, the morphism q and the morphism forgetting the base change is cartesian.

This is the source's statement. Its proof is the source's: the square of presheaves is cartesian, which is AlgebraicGeometry.Space.isPullback_relativeHomOfBaseChange, and the inclusion of fppf sheaves into presheaves creates limits, so a square of sheaves is cartesian as soon as the underlying square of presheaves is. The sheaf property of the two relative morphism functors is part (1) of Stacks 05Y3, which this library does not carry; it is taken as the hypotheses hH and hH', and nothing else about the two functors is assumed. The sheaf property of Q and of Q' is automatic for algebraic spaces.

theorem isPullback_sheaf_relativeHomOfBaseChange (q : Q' ⟶ Q)
    (H : RelativeHomConstruction B S hS Z X Q z x)
    (H' : RelativeHomConstruction B S hS (pullback q z) (pullback q x) Q'
      (pullback.fst q z) (pullback.fst q x))
    (hQ : Presheaf.IsSheaf (BigFppfOver.topology B S hS) Q)
    (hQ' : Presheaf.IsSheaf (BigFppfOver.topology B S hS) Q')
    (hH : Presheaf.IsSheaf (BigFppfOver.topology B S hS) H.functor)
    (hH' : Presheaf.IsSheaf (BigFppfOver.topology B S hS) H'.functor) :
    IsPullback
      (ObjectProperty.homMk H'.projection :
        (⟨H'.functor, hH'⟩ : Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ ⟨Q', hQ'⟩)
      (ObjectProperty.homMk (relativeHomOfBaseChange q H H') :
        (⟨H'.functor, hH'⟩ : Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ ⟨H.functor, hH⟩)
      (ObjectProperty.homMk q :
        (⟨Q', hQ'⟩ : Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ ⟨Q, hQ⟩)
      (ObjectProperty.homMk H.projection :
        (⟨H.functor, hH⟩ : Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ ⟨Q, hQ⟩)

AlgebraicGeometry.Space.isPullback_sheaf_relativeHomOfBaseChange_relativeHomData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RelativeMorphismBaseChange.lean, line 667. The attribute's comment: “the identification in Sh((Sch/S)_fppf) for the functor of Stacks 05Y2 and the fibre products of Stacks 02X2, with the sheaf property of the two relative morphism functors — part (1) of the cited Stacks 05Y3 — carried as a hypothesis”.

Stacks 05Y4 for the relative morphism functor of Stacks 05Y2 and the fibre products of algebraic spaces of Stacks 02X2: for morphisms z : Z ⟶ Q, x : X ⟶ Q and q : Q' ⟶ Q of algebraic spaces over S,

Mor_{Q'}(Q' ×_Q Z, Q' ×_Q X) = Q' ×_Q Mor_Q(Z, X)

in Sh((Sch/S)_fppf). The sheaf property of the two relative morphism functors is part (1) of Stacks 05Y3, which this library does not carry; it is taken as the hypotheses hH and hH'. That Q and Q' are sheaves is part of being an algebraic space, so nothing else is assumed.

theorem isPullback_sheaf_relativeHomOfBaseChange_relativeHomData
    {Z X Q Q' : AlgebraicSpaces B S hS} (z : Z ⟶ Q) (x : X ⟶ Q) (q : Q' ⟶ Q)
    (hH : Presheaf.IsSheaf (BigFppfOver.topology B S hS)
      (relativeHomData B S hS Z.obj X.obj Q.obj z.hom x.hom Z.property X.property
        Q.property).functor)
    (hH' : Presheaf.IsSheaf (BigFppfOver.topology B S hS)
      (relativeHomData B S hS (AlgebraicSpaces.fiberProduct B S hS q z).obj
        (AlgebraicSpaces.fiberProduct B S hS q x).obj Q'.obj
        (pullback.fst q.hom z.hom) (pullback.fst q.hom x.hom)
        (AlgebraicSpaces.fiberProduct B S hS q z).property
        (AlgebraicSpaces.fiberProduct B S hS q x).property Q'.property).functor) :
    IsPullback
      (ObjectProperty.homMk
        (relativeHomData B S hS (AlgebraicSpaces.fiberProduct B S hS q z).obj
          (AlgebraicSpaces.fiberProduct B S hS q x).obj Q'.obj
          (pullback.fst q.hom z.hom) (pullback.fst q.hom x.hom)
          (AlgebraicSpaces.fiberProduct B S hS q z).property
          (AlgebraicSpaces.fiberProduct B S hS q x).property Q'.property).projection :
        (⟨_, hH'⟩ : Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶
          ⟨Q'.obj, Q'.property.isSheaf⟩)
      (ObjectProperty.homMk
        (relativeHomOfBaseChange q.hom
          (relativeHomData B S hS Z.obj X.obj Q.obj z.hom x.hom Z.property X.property Q.property)
          (relativeHomData B S hS (AlgebraicSpaces.fiberProduct B S hS q z).obj
            (AlgebraicSpaces.fiberProduct B S hS q x).obj Q'.obj
            (pullback.fst q.hom z.hom) (pullback.fst q.hom x.hom)
            (AlgebraicSpaces.fiberProduct B S hS q z).property
            (AlgebraicSpaces.fiberProduct B S hS q x).property Q'.property)) :
        (⟨_, hH'⟩ : Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ ⟨_, hH⟩)
      (ObjectProperty.homMk q.hom :
        (⟨Q'.obj, Q'.property.isSheaf⟩ : Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶
          ⟨Q.obj, Q.property.isSheaf⟩)
      (ObjectProperty.homMk
        (relativeHomData B S hS Z.obj X.obj Q.obj z.hom x.hom Z.property X.property
          Q.property).projection :
        (⟨_, hH⟩ : Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶
          ⟨Q.obj, Q.property.isSheaf⟩)

AlgebraicGeometry.Space.isPullback_sheaf_relativeHomOfBaseChange_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RelativeMorphismBaseChange.lean, line 764. The attribute's comment: “the identification in Sh((Sch/S)_fppf)”.

Stacks 05Y4, unconditionally. The identification

Mor_{Q'}(Z', X') = Q' ×_Q Mor_Q(Z, X)

in Sh((Sch/S)_fppf), for arbitrary realizations of the two relative morphism functors. This is AlgebraicGeometry.Space.isPullback_sheaf_relativeHomOfBaseChange with its two sheaf hypotheses discharged by part (1) of Stacks 05Y3, in the form AlgebraicGeometry.Space.RelativeHomConstruction.isSheaf_functor; the algebraicity of the sources and of the two bases is all that remains.

theorem isPullback_sheaf_relativeHomOfBaseChange_of_isAlgebraicSpace (q : Q' ⟶ Q)
    (H : RelativeHomConstruction B S hS Z X Q z x)
    (H' : RelativeHomConstruction B S hS (pullback q z) (pullback q x) Q'
      (pullback.fst q z) (pullback.fst q x))
    (hZ : IsAlgebraicSpace B S hS Z) (hX : IsAlgebraicSpace B S hS X)
    (hQ : IsAlgebraicSpace B S hS Q) (hQ' : IsAlgebraicSpace B S hS Q')
    (hZ' : IsAlgebraicSpace B S hS (pullback q z))
    (hX' : IsAlgebraicSpace B S hS (pullback q x)) :
    IsPullback
      (ObjectProperty.homMk H'.projection :
        (⟨H'.functor, H'.isSheaf_functor hZ' hX' hQ'⟩ :
          Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ ⟨Q', hQ'.isSheaf⟩)
      (ObjectProperty.homMk (relativeHomOfBaseChange q H H') :
        (⟨H'.functor, H'.isSheaf_functor hZ' hX' hQ'⟩ :
            Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶
          ⟨H.functor, H.isSheaf_functor hZ hX hQ⟩)
      (ObjectProperty.homMk q :
        (⟨Q', hQ'.isSheaf⟩ : Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ ⟨Q, hQ.isSheaf⟩)
      (ObjectProperty.homMk H.projection :
        (⟨H.functor, H.isSheaf_functor hZ hX hQ⟩ :
          Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ ⟨Q, hQ.isSheaf⟩)

AlgebraicGeometry.Space.isPullback_relativeHomSheafOfBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RelativeMorphismBaseChange.lean, line 804. The attribute's comment: “the identification in Sh((Sch/S)_fppf) for the functor of Stacks 05Y2 and the fibre products of Stacks 02X2”.

Stacks 05Y4, unconditionally, for the relative morphism functor of Stacks 05Y2 and the fibre products of algebraic spaces of Stacks 02X2: for morphisms z : Z ⟶ Q, x : X ⟶ Q and q : Q' ⟶ Q of algebraic spaces over S,

Mor_{Q'}(Q' ×_Q Z, Q' ×_Q X) = Q' ×_Q Mor_Q(Z, X)

in Sh((Sch/S)_fppf). This is the source's statement with nothing assumed: the sheaf property of the two relative morphism functors is part (1) of Stacks 05Y3, AlgebraicGeometry.Space.isSheaf_relativeHom.

theorem isPullback_relativeHomSheafOfBaseChange {Z X Q Q' : AlgebraicSpaces B S hS}
    (z : Z ⟶ Q) (x : X ⟶ Q) (q : Q' ⟶ Q) :
    IsPullback
      (ObjectProperty.homMk
        (relativeHomProjection B S hS (AlgebraicSpaces.fiberProduct B S hS q z).obj
          (AlgebraicSpaces.fiberProduct B S hS q x).obj Q'.obj
          (pullback.fst q.hom z.hom) (pullback.fst q.hom x.hom)
          (AlgebraicSpaces.fiberProduct B S hS q z).property
          (AlgebraicSpaces.fiberProduct B S hS q x).property Q'.property) :
        relativeHomSheaf B S hS (AlgebraicSpaces.fiberProduct B S hS q z).obj
            (AlgebraicSpaces.fiberProduct B S hS q x).obj Q'.obj
            (pullback.fst q.hom z.hom) (pullback.fst q.hom x.hom)
            (AlgebraicSpaces.fiberProduct B S hS q z).property
            (AlgebraicSpaces.fiberProduct B S hS q x).property Q'.property ⟶
          ⟨Q'.obj, Q'.property.isSheaf⟩)
      (ObjectProperty.homMk
        (relativeHomOfBaseChange q.hom
          (relativeHomData B S hS Z.obj X.obj Q.obj z.hom x.hom Z.property X.property Q.property)
          (relativeHomData B S hS (AlgebraicSpaces.fiberProduct B S hS q z).obj
            (AlgebraicSpaces.fiberProduct B S hS q x).obj Q'.obj
            (pullback.fst q.hom z.hom) (pullback.fst q.hom x.hom)
            (AlgebraicSpaces.fiberProduct B S hS q z).property
            (AlgebraicSpaces.fiberProduct B S hS q x).property Q'.property)) :
        relativeHomSheaf B S hS (AlgebraicSpaces.fiberProduct B S hS q z).obj
            (AlgebraicSpaces.fiberProduct B S hS q x).obj Q'.obj
            (pullback.fst q.hom z.hom) (pullback.fst q.hom x.hom)
            (AlgebraicSpaces.fiberProduct B S hS q z).property
            (AlgebraicSpaces.fiberProduct B S hS q x).property Q'.property ⟶
          relativeHomSheaf B S hS Z.obj X.obj Q.obj z.hom x.hom Z.property X.property Q.property)
      (ObjectProperty.homMk q.hom :
        (⟨Q'.obj, Q'.property.isSheaf⟩ : Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶
          ⟨Q.obj, Q.property.isSheaf⟩)
      (ObjectProperty.homMk
        (relativeHomProjection B S hS Z.obj X.obj Q.obj z.hom x.hom Z.property X.property
          Q.property) :
        relativeHomSheaf B S hS Z.obj X.obj Q.obj z.hom x.hom Z.property X.property Q.property ⟶
          ⟨Q.obj, Q.property.isSheaf⟩)

Tag 05Y5, a lemma

Tag 05Y5 in the Stacks Project.

AlgebraicGeometry.Space.isSurjective_relativeHomPostcompose_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartComparisonAssembly.lean, line 445. The attribute's comment: “surjective, given X' ⟶ X surjective: at the hypotheses of the source, with nothing carried”.

Stacks 05Y5, third conclusion, at the hypotheses of the source. Let z : Z ⟶ Q and x' : X' ⟶ X ⟶ Q be morphisms of algebraic spaces over S with X' ⟶ X étale and surjective and z finite locally free. Then Mor_Q(Z, X') ⟶ Mor_Q(Z, X) is surjective.

This is AlgebraicGeometry.Space.isSurjective_relativeHomPostcompose with its hypothesis h05XQ discharged by AlgebraicGeometry.Space.isFibreSectionsSurjective; it is stated here for the reason recorded on AlgebraicGeometry.Space.isSurjective_restrictionOfScalarsMap_of_isFiniteLocallyFree.

theorem isSurjective_relativeHomPostcompose_of_isFiniteLocallyFree
    {X' X Z Q : AlgebraicSpaces B S hS} {x' : X' ⟶ Q} {x : X ⟶ Q} {z : Z ⟶ Q}
    (HX' : RelativeHomConstruction B S hS Z.obj X'.obj Q.obj z.hom x'.hom)
    (HX : RelativeHomConstruction B S hS Z.obj X.obj Q.obj z.hom x.hom)
    (g : X' ⟶ X) (hg : g.hom ≫ x.hom = x'.hom)
    (hg_etale : IsEtale B S hS g.hom) (hg_surjective : IsSurjective B S hS g.hom)
    (hz : IsFiniteLocallyFree B S hS z) :
    IsSurjective B S hS (relativeHomPostcompose HX' HX g.hom hg)

AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_relativeHomPostcompose_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreSectionsAlgebraicEtale.lean, line 385. The attribute's comment: “representable by algebraic spaces: at the hypotheses of the source, with nothing carried”.

Stacks 05Y5, first conclusion, at the hypotheses of the source. Let Z → Q and X' → X → Q be morphisms of algebraic spaces over S with X' → X étale and Z → Q finite locally free. Then Mor_Q(Z, X') → Mor_Q(Z, X) is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_relativeHomPostcompose_of_isFiniteLocallyFree
    {X' X Z Q : AlgebraicSpaces B S hS} {x' : X' ⟶ Q} {x : X ⟶ Q} {z : Z ⟶ Q}
    (HX' : RelativeHomConstruction B S hS Z.obj X'.obj Q.obj z.hom x'.hom)
    (HX : RelativeHomConstruction B S hS Z.obj X.obj Q.obj z.hom x.hom)
    (g : X' ⟶ X) (hg : g.hom ≫ x.hom = x'.hom) (hg_etale : IsEtale B S hS g.hom)
    (hz : IsFiniteLocallyFree B S hS z) :
    IsRepresentableByAlgebraicSpaces B S hS (relativeHomPostcompose HX' HX g.hom hg)

AlgebraicGeometry.Space.hasProperty_isEtale_relativeHomPostcompose_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreSectionsAlgebraicEtale.lean, line 399. The attribute's comment: “étale: at the hypotheses of the source, with nothing carried”.

Stacks 05Y5, second conclusion, at the hypotheses of the source. In the situation of isRepresentableByAlgebraicSpaces_relativeHomPostcompose_of_isFiniteLocallyFree, the morphism Mor_Q(Z, X') → Mor_Q(Z, X) is étale.

theorem hasProperty_isEtale_relativeHomPostcompose_of_isFiniteLocallyFree
    {X' X Z Q : AlgebraicSpaces B S hS} {x' : X' ⟶ Q} {x : X ⟶ Q} {z : Z ⟶ Q}
    (HX' : RelativeHomConstruction B S hS Z.obj X'.obj Q.obj z.hom x'.hom)
    (HX : RelativeHomConstruction B S hS Z.obj X.obj Q.obj z.hom x.hom)
    (g : X' ⟶ X) (hg : g.hom ≫ x.hom = x'.hom) (hg_etale : IsEtale B S hS g.hom)
    (hz : IsFiniteLocallyFree B S hS z) :
    HasProperty B S hS (fun _ _ f => IsEtale B S hS f.hom)
      (relativeHomPostcompose HX' HX g.hom hg)
      (isRepresentableByAlgebraicSpaces_relativeHomPostcompose_of_isFiniteLocallyFree B S hS HX'
        HX g hg hg_etale hz)

Tag 05Y7, a proposition

Tag 05Y7 in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_relativeHom_of_isFiniteLocallyFree_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreSectionsAlgebraicEtale.lean, line 472. The attribute's comment: “at the hypotheses of the source, with nothing carried”.

Stacks 05Y7, at the hypotheses of the source. Let S be a scheme contained in a big fppf site, and let z : Z ⟶ Q and x : X ⟶ Q be morphisms of algebraic spaces over S. If z is finite locally free then the relative morphism functor Mor_Q(Z, X) of Stacks 05Y2 is an algebraic space over S.

theorem isAlgebraicSpace_relativeHom_of_isFiniteLocallyFree_source
    (Z X Q : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (z : Z ⟶ Q) (x : X ⟶ Q)
    (hZ : IsAlgebraicSpace B S hS Z) (hX : IsAlgebraicSpace B S hS X)
    (hQ : IsAlgebraicSpace B S hS Q)
    (hz : IsFiniteLocallyFree B S hS
      (ObjectProperty.homMk z :
        (⟨Z, hZ⟩ : AlgebraicSpaces B S hS) ⟶ (⟨Q, hQ⟩ : AlgebraicSpaces B S hS))) :
    IsAlgebraicSpace B S hS (relativeHom B S hS Z X Q z x hZ hX hQ)

Sources

• Section 97.10, Tag 05Y0
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.RelativeMorphism · AlgebraicGeometry.Space.RelativeMorphismDiagram · AlgebraicGeometry.Space.relativeHomData · AlgebraicGeometry.Space.relativeHomEquiv · AlgebraicGeometry.Space.isSheaf_relativeHom · AlgebraicGeometry.Space.isPullback_sheaf_relativeHomOfBaseChange · AlgebraicGeometry.Space.isPullback_sheaf_relativeHomOfBaseChange_relativeHomData · AlgebraicGeometry.Space.isPullback_sheaf_relativeHomOfBaseChange_of_isAlgebraicSpace

Section97.11 Restriction of scalars#

Section 97.11 of the Stacks Project, Tag 05Y8. 7 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05Y9, an equation

Tag 05Y9 in the Stacks Project.

AlgebraicGeometry.Space.RestrictionPair, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RestrictionOfScalars.lean, line 77. The attribute's comment: “the pair (a, b) displayed by the diagram”.

A pair (a, b) for the restriction of scalars of x : X ⟶ Z along z : Z ⟶ Q at a test presheaf T: a morphism a : T ⟶ Q together with a morphism b : T ×_{a, Q} Z ⟶ X lying over Z.

This is a pair of AlgebraicGeometry.Space.RelativeMorphism for z and x ≫ z subject to the stronger requirement that b lie over Z and not merely over Q; see AlgebraicGeometry.Space.restrictionPairEquivSubtype.

structure RestrictionPair {X Z Q : AlgebraicSpaces B S hS} (x : X ⟶ Z) (z : Z ⟶ Q)
    (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)

Tag 05YA, an equation

Tag 05YA in the Stacks Project.

AlgebraicGeometry.Space.restrictionOfScalars, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RestrictionOfScalars.lean, line 304.

The restriction of scalars Res_{Z/Q}(X) of x : X ⟶ Z along z : Z ⟶ Q: the functor of points on the big fppf site of S whose sections over a scheme T are the pairs (a, b) of Stacks 05Y9, with its projection to Q and with restriction given by base change.

noncomputable def restrictionOfScalars {X Z Q : AlgebraicSpaces B S hS} (x : X ⟶ Z)
    (z : Z ⟶ Q) : RestrictionOfScalarsConstruction B S hS x z

Tag 05YB, a lemma

Tag 05YB in the Stacks Project.

AlgebraicGeometry.Space.restrictionOfScalarsHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RestrictionOfScalarsHom.lean, line 340. The attribute's comment: “the functor of points”.

Stacks 05YB. Morphisms from an algebraic space T into the restriction of scalars Res_{Z/Q}(X) of x : X ⟶ Z along z : Z ⟶ Q are the pairs (a, b) of Stacks 05Y9 at T: a morphism a : T ⟶ Q together with a morphism b : T ×_{a, Q} Z ⟶ X over Z.

The bijection is characterized by the two properties recorded with it: its value at v base changes, along every scheme-valued point i of T, to the pair that Stacks 05YA attaches to i ≫ v; and it is natural in T.

noncomputable def restrictionOfScalarsHomEquiv (x : X ⟶ Z) (z : Z ⟶ Q) :
    {e : ∀ T : AlgebraicSpaces B S hS,
        (T.obj ⟶ (restrictionOfScalars B S hS x z).presheaf) ≃
          RestrictionPair B S hS x z T.obj //
      (∀ (T : AlgebraicSpaces B S hS) (U : BigFppfOver B S hS) (i : yoneda.obj U ⟶ T.obj)
          (v : T.obj ⟶ (restrictionOfScalars B S hS x z).presheaf),
        RestrictionPair.IsPullbackAlong i (e T v)
          ((restrictionOfScalars B S hS x z).pairEquiv U (yonedaEquiv (i ≫ v)))) ∧
      (∀ (T T' : AlgebraicSpaces B S hS) (f : T' ⟶ T)
          (v : T.obj ⟶ (restrictionOfScalars B S hS x z).presheaf),
        RestrictionPair.IsPullbackAlong f.hom (e T v) (e T' (f.hom ≫ v)))}

AlgebraicGeometry.Space.isSheaf_restrictionOfScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RestrictionOfScalarsSheaf.lean, line 64. The attribute's comment: “part (1): Res_{Z/B}(X) is a sheaf on the big fppf site of S”.

Stacks 05YB, part (1). For morphisms x : X ⟶ Z and z : Z ⟶ Q of algebraic spaces over S, the restriction of scalars Res_{Z/Q}(X) of Stacks 05YA is a sheaf on the big fppf site of S.

A pair (a, b) of Stacks 05Y9 is a pair of Stacks 05Y1 whose second component lies over Z, and the cartesian square of Stacks 05YE presents Res_{Z/Q}(X) as the fibre product of Mor_Q(Z, X) and Q over Mor_Q(Z, Z). The descent of pairs the source carries out is therefore already done: it is part (1) of Stacks 05Y3 for the two relative morphism functors, and the fibre product of sheaves of types is a sheaf.

theorem isSheaf_restrictionOfScalars {X Z Q : AlgebraicSpaces B S hS} (x : X ⟶ Z) (z : Z ⟶ Q) :
    Presheaf.IsSheaf (BigFppfOver.topology B S hS)
      (restrictionOfScalars B S hS x z).presheaf

Tag 05YC, a lemma

Tag 05YC in the Stacks Project.

AlgebraicGeometry.Space.baseChangeFiberProductMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RestrictionOfScalarsBaseChange.lean, line 126. The attribute's comment: “the base-changed morphism”.

Stacks 05YC. The base change Q' ×_Q X ⟶ Q' ×_Q Z of a morphism x : X ⟶ Z of algebraic spaces over z : Z ⟶ Q along a morphism b : Q' ⟶ Q, for the chosen fibre products of Stacks 02X2. It is the identity on the first factor and x on the second.

noncomputable def baseChangeFiberProductMap {X Z Q Q' : AlgebraicSpaces B S hS} (x : X ⟶ Z)
    (z : Z ⟶ Q) (b : Q' ⟶ Q) :
    AlgebraicSpaces.fiberProduct B S hS b (x ≫ z) ⟶ AlgebraicSpaces.fiberProduct B S hS b z

AlgebraicGeometry.Space.isPullback_baseChangeFiberProductMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RestrictionOfScalarsBaseChange.lean, line 168. The attribute's comment: “the base-changed morphism as a fibre product”.

Stacks 05YC. The base-changed morphism exhibits Q' ×_Q X as (Q' ×_Q Z) ×_Z X. This is the form in which AlgebraicGeometry.Space.restrictionOfScalars_baseChange asks for the base change of x.

theorem isPullback_baseChangeFiberProductMap :
    IsPullback (baseChangeFiberProductMap B S hS x z b).hom
      (pullback.snd b.hom (x ≫ z).hom) (pullback.snd b.hom z.hom) x.hom

AlgebraicGeometry.Space.restrictionOfScalars_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RestrictionOfScalarsBaseChange.lean, line 472. The attribute's comment: “the base-change identification”.

Stacks 05YC. Let x : X ⟶ Z and z : Z ⟶ Q be morphisms of algebraic spaces over S and let b : Q' ⟶ Q be a morphism of algebraic spaces over S. Let z' : Z' ⟶ Q', c : Z' ⟶ Z exhibit Z' as the base change Q' ×_Q Z, and let x' : X' ⟶ Z', e : X' ⟶ X exhibit X' as the base change Z' ×_Z X, so that X' = Q' ×_Q X. Then

Res_{Z'/Q'}(X')  =  Q' ×_Q Res_{Z/Q}(X)

as presheaves on the big fppf site of S: there is an isomorphism compatible with the projections to Q', which on sections carries the pair of Stacks 05Y9 of a section of Res_{Z'/Q'}(X') to its base change AlgebraicGeometry.Space.RestrictionPair.baseChange.

For the chosen fibre products of Stacks 02X2 the two hypotheses are AlgebraicGeometry.Space.isPullback_hom_fiberProduct and AlgebraicGeometry.Space.isPullback_baseChangeFiberProductMap; that instance is AlgebraicGeometry.Space.restrictionOfScalars_baseChange_fiberProduct.

theorem restrictionOfScalars_baseChange :
    ∃ i : r'.presheaf ≅ pullback b.hom r.projection,
      i.hom ≫ pullback.fst b.hom r.projection = r'.projection ∧
        ∀ (T : BigFppfOver B S hS) (v : r'.presheaf.obj (op T)),
          r.pairEquiv T ((i.hom ≫ pullback.snd b.hom r.projection).app (op T) v) =
            (r'.pairEquiv T v).baseChange hZ hX

AlgebraicGeometry.Space.restrictionOfScalars_baseChange_fiberProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RestrictionOfScalarsBaseChange.lean, line 506. The attribute's comment: “the base-change identification for the chosen fibre products”.

Stacks 05YC. The form of AlgebraicGeometry.Space.restrictionOfScalars_baseChange for the chosen fibre products of Stacks 02X2: with Z' = Q' ×_Q Z and X' = Q' ×_Q X those fibre products and x' : X' ⟶ Z' the base-changed morphism AlgebraicGeometry.Space.baseChangeFiberProductMap,

Res_{Z'/Q'}(X')  =  Q' ×_Q Res_{Z/Q}(X)

as presheaves on the big fppf site of S, compatibly with the projections to Q'.

theorem restrictionOfScalars_baseChange_fiberProduct {X Z Q Q' : AlgebraicSpaces B S hS}
    (x : X ⟶ Z) (z : Z ⟶ Q) (b : Q' ⟶ Q)
    (r : RestrictionOfScalarsConstruction B S hS x z)
    (r' : RestrictionOfScalarsConstruction B S hS (baseChangeFiberProductMap B S hS x z b)
      (ObjectProperty.homMk (pullback.fst b.hom z.hom) :
        AlgebraicSpaces.fiberProduct B S hS b z ⟶ Q')) :
    ∃ i : r'.presheaf ≅ pullback b.hom r.projection,
      i.hom ≫ pullback.fst b.hom r.projection = r'.projection ∧
        ∀ (T : BigFppfOver B S hS) (v : r'.presheaf.obj (op T)),
          r.pairEquiv T ((i.hom ≫ pullback.snd b.hom r.projection).app (op T) v) =
            (r'.pairEquiv T v).baseChange (isPullback_hom_fiberProduct B S hS b z)
              (isPullback_baseChangeFiberProductMap B S hS x z b)

Tag 05YD, a lemma

Tag 05YD in the Stacks Project.

AlgebraicGeometry.Space.isSurjective_restrictionOfScalarsMap_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartComparisonAssembly.lean, line 426. The attribute's comment: “surjective, given X' ⟶ X surjective: at the hypotheses of the source, with nothing carried”.

Stacks 05YD, third conclusion, at the hypotheses of the source. Let X' → X → Z → Q be morphisms of algebraic spaces over S with X' → X étale and surjective and Z → Q finite locally free. Then Res_{Z/Q}(X') → Res_{Z/Q}(X) is surjective.

This is AlgebraicGeometry.Space.isSurjective_restrictionOfScalarsMap with its hypothesis h05XQ discharged by AlgebraicGeometry.Space.isFibreSectionsSurjective. It is stated here rather than beside that theorem because StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartLocalizationBaseChange.lean, which the chart comparison of Stacks 03ZU is built on, already imports the file where it lives.

theorem isSurjective_restrictionOfScalarsMap_of_isFiniteLocallyFree
    {X' X Z Q : AlgebraicSpaces B S hS} {x' : X' ⟶ Z} {x : X ⟶ Z} (g : X' ⟶ X)
    (hg : g ≫ x = x') (z : Z ⟶ Q)
    (hg_etale : IsEtale B S hS g.hom) (hg_surjective : IsSurjective B S hS g.hom)
    (hz : IsFiniteLocallyFree B S hS z) :
    IsSurjective B S hS (restrictionOfScalarsMap g hg z).1

AlgebraicGeometry.Space.isRepresentableByAlgebraicSpaces_restrictionOfScalarsMap_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreSectionsAlgebraicEtale.lean, line 358. The attribute's comment: “representable by algebraic spaces: at the hypotheses of the source, with nothing carried”.

Stacks 05YD, first conclusion, at the hypotheses of the source. Let X' → X → Z → Q be morphisms of algebraic spaces over S with X' → X étale and Z → Q finite locally free. Then Res_{Z/Q}(X') → Res_{Z/Q}(X) is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_restrictionOfScalarsMap_of_isFiniteLocallyFree
    {X' X Z Q : AlgebraicSpaces B S hS} {x' : X' ⟶ Z} {x : X ⟶ Z} (g : X' ⟶ X)
    (hg : g ≫ x = x') (z : Z ⟶ Q) (hg_etale : IsEtale B S hS g.hom)
    (hz : IsFiniteLocallyFree B S hS z) :
    IsRepresentableByAlgebraicSpaces B S hS (restrictionOfScalarsMap g hg z).1

AlgebraicGeometry.Space.hasProperty_isEtale_restrictionOfScalarsMap_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreSectionsAlgebraicEtale.lean, line 370. The attribute's comment: “étale: at the hypotheses of the source, with nothing carried”.

Stacks 05YD, second conclusion, at the hypotheses of the source. In the situation of isRepresentableByAlgebraicSpaces_restrictionOfScalarsMap_of_isFiniteLocallyFree, the morphism Res_{Z/Q}(X') → Res_{Z/Q}(X) is étale.

theorem hasProperty_isEtale_restrictionOfScalarsMap_of_isFiniteLocallyFree
    {X' X Z Q : AlgebraicSpaces B S hS} {x' : X' ⟶ Z} {x : X ⟶ Z} (g : X' ⟶ X)
    (hg : g ≫ x = x') (z : Z ⟶ Q) (hg_etale : IsEtale B S hS g.hom)
    (hz : IsFiniteLocallyFree B S hS z) :
    HasProperty B S hS (fun _ _ f => IsEtale B S hS f.hom) (restrictionOfScalarsMap g hg z).1
      (isRepresentableByAlgebraicSpaces_restrictionOfScalarsMap_of_isFiniteLocallyFree B S hS g hg
        z hg_etale hz)

Tag 05YE, a lemma

Tag 05YE in the Stacks Project.

AlgebraicGeometry.Space.isPullback_restrictionOfScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RestrictionOfScalarsCartesian.lean, line 407. The attribute's comment: “the cartesian square of presheaves on the big fppf site”.

The square

Mor_Q(Z, X) ⟶ Mor_Q(Z, Z)
     ↑              ↑ id_Z
Res_{Z/Q}(X) ⟶     Q

of presheaves on the big fppf site of S is cartesian: the restriction of scalars of x : X ⟶ Z along z : Z ⟶ Q is the fibre product of Mor_Q(Z, X) and Q over Mor_Q(Z, Z), where the morphism from Q picks out the identity endomorphism of Z.

theorem isPullback_restrictionOfScalars {X Z Q : AlgebraicSpaces B S hS} {x : X ⟶ Z} {z : Z ⟶ Q}
    (R : RestrictionOfScalarsConstruction B S hS x z)
    (HX : RelativeHomConstruction B S hS Z.obj X.obj Q.obj z.hom (x.hom ≫ z.hom))
    (HZ : RelativeHomConstruction B S hS Z.obj Z.obj Q.obj z.hom z.hom) :
    IsPullback (restrictionOfScalarsToRelativeHom R HX) R.projection
      (relativeHomPostcompose HX HZ x.hom rfl) (relativeHomIdentity HZ)

AlgebraicGeometry.Space.isPullback_restrictionOfScalars_relativeHomData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RestrictionOfScalarsCartesian.lean, line 489. The attribute's comment: “the cartesian square, for the functors of Stacks 05Y2 and 05YA”.

The square of AlgebraicGeometry.Space.isPullback_restrictionOfScalars is cartesian for the relative morphism functor of Stacks 05Y2 and the restriction of scalars of Stacks 05YA.

theorem isPullback_restrictionOfScalars_relativeHomData {X Z Q : AlgebraicSpaces B S hS}
    (x : X ⟶ Z) (z : Z ⟶ Q) :
    IsPullback
      (restrictionOfScalarsToRelativeHom (restrictionOfScalars B S hS x z)
        (relativeHomData B S hS Z.obj X.obj Q.obj z.hom (x.hom ≫ z.hom) Z.property X.property
          Q.property))
      (restrictionOfScalars B S hS x z).projection
      (relativeHomPostcompose
        (relativeHomData B S hS Z.obj X.obj Q.obj z.hom (x.hom ≫ z.hom) Z.property X.property
          Q.property)
        (relativeHomData B S hS Z.obj Z.obj Q.obj z.hom z.hom Z.property Z.property Q.property)
        x.hom rfl)
      (relativeHomIdentity
        (relativeHomData B S hS Z.obj Z.obj Q.obj z.hom z.hom Z.property Z.property Q.property))

Tag 05YF, a proposition

Tag 05YF in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_restrictionOfScalars_of_isFiniteLocallyFree_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreSectionsAlgebraicEtale.lean, line 487. The attribute's comment: “at the hypotheses of the source, with nothing carried”.

Stacks 05YF, at the hypotheses of the source. Let x : X ⟶ Z and z : Z ⟶ Q be morphisms of algebraic spaces over S with z finite locally free. Then the restriction of scalars Res_{Z/Q}(X) of Stacks 05YA is an algebraic space over S.

theorem isAlgebraicSpace_restrictionOfScalars_of_isFiniteLocallyFree_source
    {X Z Q : AlgebraicSpaces B S hS} (x : X ⟶ Z) (z : Z ⟶ Q)
    (hz : IsFiniteLocallyFree B S hS z) :
    IsAlgebraicSpace B S hS (restrictionOfScalars B S hS x z).presheaf

Sources

• Section 97.11, Tag 05Y8
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.RestrictionPair · AlgebraicGeometry.Space.restrictionOfScalars · AlgebraicGeometry.Space.restrictionOfScalarsHomEquiv · AlgebraicGeometry.Space.isSheaf_restrictionOfScalars · AlgebraicGeometry.Space.baseChangeFiberProductMap · AlgebraicGeometry.Space.isPullback_baseChangeFiberProductMap · AlgebraicGeometry.Space.restrictionOfScalars_baseChange · AlgebraicGeometry.Space.restrictionOfScalars_baseChange_fiberProduct

Section97.12 Finite Hilbert stacks#

Section 97.12 of the Stacks Project, Tag 05XM. 7 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05XN, a lemma

Tag 05XN in the Stacks Project.

AlgebraicGeometry.Stack.mapAbsolute, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Functoriality.lean, line 137. The attribute's comment: “the induced 1-morphism of absolute finite Hilbert stacks”.

The 1-morphism ℋ_d(𝒳') ⟶ ℋ_d(𝒳) of absolute degree-d finite Hilbert stacks induced by a 1-morphism G : 𝒳' ⟶ 𝒳 of stacks in groupoids: the canonical 1-morphism of finite Hilbert stacks for the 2-commutative square whose two columns are the structure morphisms of 𝒳' and 𝒳.

def mapAbsolute :
    absoluteHilbertCategory (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳') ⥤ᵇ
      absoluteHilbertCategory (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳)

AlgebraicGeometry.Stack.mapAbsolute_comp_forgetAbsoluteStructure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Functoriality.lean, line 146. The attribute's comment: “compatibility with the forgetful 1-morphism ℋ_d(𝒳) ⟶ ℋ_d”.

The induced 1-morphism of absolute finite Hilbert stacks leaves the underlying degree-d finite locally free cover unchanged.

theorem mapAbsolute_comp_forgetAbsoluteStructure :
    BasedFunctor.comp (mapAbsolute B S hS d 𝒳' 𝒳 G)
        (forgetAbsoluteStructure (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳)) =
      forgetAbsoluteStructure (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳')

AlgebraicGeometry.Stack.mapRelative, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Functoriality.lean, line 198. The attribute's comment: “the canonical 1-morphism”.

The canonical 1-morphism ℋ_d(𝒳'/𝒴') ⟶ ℋ_d(𝒳/𝒴) of degree-d finite Hilbert stacks attached to a 2-commutative square of stacks in groupoids with horizontal arrows G and H, vertical arrows F' and F, and 2-isomorphism γ : H ∘ F' ⟶ F ∘ G.

def mapRelative :
    finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳') (𝒴 := 𝒴') (F := F') (d := d) ⥤ᵇ
      finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d)

AlgebraicGeometry.Stack.mapRelative_obj_α, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Functoriality.lean, line 207. The attribute's comment: “action on the identification”.

The canonical 1-morphism sends an object with identification α to one whose identification is α transported across the given 2-isomorphism.

theorem mapRelative_obj_α (P : FiniteHilbert.Object B S hS 𝒳' 𝒴' F' d) :
    ((mapRelative B S hS d 𝒳' 𝒴' 𝒳 𝒴 F' F G H γ).obj P).α =
      squareComparison γ P.x ≫ H.map P.α

AlgebraicGeometry.Stack.mapRelative_comp_forgetRelativeStructure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Functoriality.lean, line 215. The attribute's comment: “compatibility with the forgetful 1-morphism ℋ_d(𝒳/𝒴) ⟶ ℋ_d(𝒳)”.

The canonical 1-morphism is compatible with the forgetful 1-morphisms to the absolute finite Hilbert stacks: on them it induces the 1-morphism attached to G.

theorem mapRelative_comp_forgetRelativeStructure :
    BasedFunctor.comp (mapRelative B S hS d 𝒳' 𝒴' 𝒳 𝒴 F' F G H γ)
        (forgetRelativeStructure (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳) (𝒴 := 𝒴)
          (F := F)) =
      BasedFunctor.comp
        (forgetRelativeStructure (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳') (𝒴 := 𝒴')
          (F := F'))
        (mapAbsolute B S hS d 𝒳' 𝒳 G)

AlgebraicGeometry.Stack.mapRelative_comp_forgetTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Functoriality.lean, line 228. The attribute's comment: “compatibility with the forgetful 1-morphism ℋ_d(𝒳/𝒴) ⟶ 𝒴”.

The canonical 1-morphism is compatible with the forgetful 1-morphisms to the target stacks: on them it induces H.

theorem mapRelative_comp_forgetTarget :
    BasedFunctor.comp (mapRelative B S hS d 𝒳' 𝒴' 𝒳 𝒴 F' F G H γ)
        (forgetTarget (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)) =
      BasedFunctor.comp
        (forgetTarget (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳') (𝒴 := 𝒴') (F := F')) H

AlgebraicGeometry.Stack.mapRelative_comp_forgetRelativeToFiniteCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Functoriality.lean, line 238. The attribute's comment: “compatibility with the forgetful 1-morphism ℋ_d(𝒳/𝒴) ⟶ ℋ_d”.

The canonical 1-morphism leaves the underlying degree-d finite locally free cover unchanged.

theorem mapRelative_comp_forgetRelativeToFiniteCover :
    BasedFunctor.comp (mapRelative B S hS d 𝒳' 𝒴' 𝒳 𝒴 F' F G H γ)
        (forgetRelativeToFiniteCover (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳) (𝒴 := 𝒴)
          (F := F)) =
      forgetRelativeToFiniteCover (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳') (𝒴 := 𝒴')
        (F := F')

Tag 05XP, a lemma

Tag 05XP in the Stacks Project.

AlgebraicGeometry.Stack.isEquivalence_hilbertComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Functoriality.lean, line 588. The attribute's comment: “the comparison functor is an equivalence”.

If the comparison functor of the given square is an equivalence, then so is the comparison functor ℋ_d(𝒳'/𝒴') ⥤ ℋ_d(𝒳/𝒴) ×_𝒴 𝒴' of the induced square.

theorem isEquivalence_hilbertComparison
    (h : (sourceComparison B S hS 𝒳' 𝒴' 𝒳 𝒴 F' F G H γ).IsEquivalence) :
    (hilbertComparison B S hS d 𝒳' 𝒴' 𝒳 𝒴 F' F G H γ).IsEquivalence

AlgebraicGeometry.Stack.isTwoFibreProduct_hilbertSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/Functoriality.lean, line 601.

If the given 2-commutative square of stacks in groupoids is 2-cartesian, then so is the induced square of degree-d finite Hilbert stacks: the canonical 1-morphism ℋ_d(𝒳'/𝒴') ⟶ ℋ_d(𝒳/𝒴) and the forgetful 1-morphism ℋ_d(𝒳'/𝒴') ⟶ 𝒴' exhibit ℋ_d(𝒳'/𝒴') as the 2-fibre product 𝒴' ×_𝒴 ℋ_d(𝒳/𝒴).

noncomputable def isTwoFibreProduct_hilbertSquare
    (hcart : Bicategory.IsTwoFibreProduct (sourceSquare B S hS 𝒳' 𝒴' 𝒳 𝒴 F' F G H γ)) :
    Bicategory.IsTwoFibreProduct (hilbertSquare B S hS d 𝒳' 𝒴' 𝒳 𝒴 F' F G H γ)

Tag 05YG, a lemma

Tag 05YG in the Stacks Project.

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

Let G : 𝒳' ⟶ 𝒳 be a 1-morphism of stacks in groupoids over the big fppf site of S which is representable by algebraic spaces and étale, and let γ present 𝒳' ⟶ 𝒴 as the composite of G with F : 𝒳 ⟶ 𝒴. Then the canonical 1-morphism ℋ_d(𝒳'/𝒴) ⟶ ℋ_d(𝒳/𝒴) of Stacks 05XN is representable by algebraic spaces and étale.

The conclusion is the shape of AlgebraicGeometry.Stack.IsRelativelyEtale at the free universes of the stacks involved: representability by algebraic spaces, and étaleness over S of every algebraic space representing a fibre over a scheme-valued point. The two halves are AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_mapRelative and AlgebraicGeometry.Stack.isEtale_mapRelative.

theorem isRepresentableByAlgebraicSpaces_and_isEtale_mapRelative
    (γ : BasedFunctor.comp F' (𝟙 𝒴.toBasedCategory) ≅ BasedFunctor.comp G F)
    (hGrep : IsRepresentableByAlgebraicSpaces B S hS G)
    (hGet : ∀ (U : BigFppfOver B S hS)
      (z : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒳.toBasedCategory.obj)
      (_hz : z ⋙ 𝒳.toBasedCategory.p = Over.map U.hom)
      (W : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
      (hW : IsAlgebraicSpace B U.left.1 U.left.2 W),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map U.hom) 𝒳'.toBasedCategory.p 𝒳.toBasedCategory.p z
          G.toFunctor)
        (presheafOfCategories (W ⋙ typeToCat)).p) →
      Space.IsEtale B S hS (algebraicSpaceMap B S hS U
        ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨W, hW⟩)).hom) :
    ∃ _ : IsRepresentableByAlgebraicSpaces B S hS
        (mapRelative B S hS d 𝒳' 𝒴 𝒳 𝒴 F' F G (𝟙 𝒴.toBasedCategory) γ),
      ∀ (U : BigFppfOver B S hS)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤
          (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
            (d := d)).obj)
        (_hy : y ⋙ (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴)
          (F := F) (d := d)).p = Over.map U.hom)
        (A : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hA : IsAlgebraicSpace B U.left.1 U.left.2 A),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom)
            (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳') (𝒴 := 𝒴) (F := F')
              (d := d)).p
            (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).p y
            (mapRelative B S hS d 𝒳' 𝒴 𝒳 𝒴 F' F G (𝟙 𝒴.toBasedCategory) γ).toFunctor)
          (presheafOfCategories (A ⋙ typeToCat)).p) →
        Space.IsEtale B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨A, hA⟩)).hom

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

If G : 𝒳' ⟶ 𝒳 is representable by algebraic spaces, étale and surjective, then the canonical 1-morphism ℋ_d(𝒳'/𝒴) ⟶ ℋ_d(𝒳/𝒴) is surjective.

By Stacks 06D7 surjectivity of a 1-morphism representable by algebraic spaces is surjectivity of every algebraic space representing one of its fibres over a scheme-valued point; that algebraic space is a space of sections of a surjective étale morphism to a finite cover of the point, which is surjective over the point by Stacks 05XQ.

theorem isSurjectiveOnObjects_mapRelative
    (γ : BasedFunctor.comp F' (𝟙 𝒴.toBasedCategory) ≅ BasedFunctor.comp G F)
    (hGrep : IsRepresentableByAlgebraicSpaces B S hS G)
    (hGet : ∀ (U : BigFppfOver B S hS)
      (z : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒳.toBasedCategory.obj)
      (_hz : z ⋙ 𝒳.toBasedCategory.p = Over.map U.hom)
      (W : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
      (hW : IsAlgebraicSpace B U.left.1 U.left.2 W),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map U.hom) 𝒳'.toBasedCategory.p 𝒳.toBasedCategory.p z
          G.toFunctor)
        (presheafOfCategories (W ⋙ typeToCat)).p) →
      Space.IsEtale B S hS (algebraicSpaceMap B S hS U
        ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨W, hW⟩)).hom)
    (hGsurj : IsSurjectiveOnObjects B S hS 𝒳'.toBasedCategory.p 𝒳.toBasedCategory.p
      G.toFunctor) :
    IsSurjectiveOnObjects B S hS
      (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳') (𝒴 := 𝒴) (F := F')
        (d := d)).p
      (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d)).p
      (mapRelative B S hS d 𝒳' 𝒴 𝒳 𝒴 F' F G (𝟙 𝒴.toBasedCategory) γ).toFunctor

Tag 05XS, a lemma

Tag 05XS in the Stacks Project.

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

Stacks 05XS, part (1). Let G : 𝒳' ⟶ 𝒳 and H : 𝒴' ⟶ 𝒴 be 1-morphisms of stacks in groupoids over the big fppf site of S which are representable by algebraic spaces and étale, and let γ : H ∘ F' ⟶ F ∘ G make the square with vertical arrows F', F 2-commute. Then the canonical 1-morphism ℋ_d(𝒳'/𝒴') ⟶ ℋ_d(𝒳/𝒴) of Stacks 05XN is representable by algebraic spaces and étale.

The proof is the source's. The 1-morphism is 2-isomorphic to the composite of ℋ_d(𝒳'/𝒴') ⟶ ℋ_d((𝒳 ×_𝒴 𝒴')/𝒴'), which is representable by algebraic spaces and étale by Stacks 05YG because 𝒳' ⟶ 𝒳 ×_𝒴 𝒴' is by Stacks 05XK, with ℋ_d((𝒳 ×_𝒴 𝒴')/𝒴') ⟶ ℋ_d(𝒳/𝒴), which is a base change of H by Stacks 05XP and therefore representable by algebraic spaces and étale by Stacks 045C.

theorem isRelativelyEtale_mapRelativeFibered
    (γ : BasedFunctor.comp F' H ≅ BasedFunctor.comp G F)
    (hG : IsRelativelyEtale B S hS (stackMapFibered B S hS G))
    (hH : IsRelativelyEtale B S hS (stackMapFibered B S hS H)) :
    IsRelativelyEtale B S hS (mapRelativeFibered B S hS d 𝒳 𝒴 F 𝒳' 𝒴' F' G H γ)

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

Stacks 05XS, part (2). Let G : 𝒳' ⟶ 𝒳 and H : 𝒴' ⟶ 𝒴 be 1-morphisms of stacks in groupoids over the big fppf site of S which are representable by algebraic spaces and étale, and let γ : H ∘ F' ⟶ F ∘ G make the square with vertical arrows F', F 2-commute. If moreover H is surjective and the induced 1-morphism 𝒳' ⟶ 𝒳 ×_𝒴 𝒴' to the 2-fibre product is surjective, then the canonical 1-morphism ℋ_d(𝒳'/𝒴') ⟶ ℋ_d(𝒳/𝒴) of Stacks 05XN is surjective.

The induced 1-morphism is AlgebraicGeometry.Stack.targetFibreProductComparison, into the 2-fibre product over the site of Stacks 0040, which the source writes 𝒴' ×_𝒴 𝒳. The proof is the source's: ℋ_d(𝒳'/𝒴') ⟶ ℋ_d((𝒳 ×_𝒴 𝒴')/𝒴') is surjective by Stacks 05YG, the base change ℋ_d((𝒳 ×_𝒴 𝒴')/𝒴') ⟶ ℋ_d(𝒳/𝒴) of H is surjective as H is, and composites of surjective 1-morphisms are surjective.

theorem isSurjectiveOnObjects_mapRelativeFibered
    (γ : BasedFunctor.comp F' H ≅ BasedFunctor.comp G F)
    (hG : IsRelativelyEtale B S hS (stackMapFibered B S hS G))
    (hH : IsRelativelyEtale B S hS (stackMapFibered B S hS H))
    (hHSurj : IsSurjectiveOnObjects B S hS (stackFibered B S hS 𝒴').val.p
      (stackFibered B S hS 𝒴).val.p
      (CatFiberedInGroupoids.homFunctor (stackMapFibered B S hS H)))
    (hcomparison : IsSurjectiveOnObjects B S hS (stackFibered B S hS 𝒳').val.p
      (stackFibered B S hS (targetFibreProduct B S hS 𝒳 𝒴 F 𝒴' H)).val.p
      (CatFiberedInGroupoids.homFunctor (stackMapFibered B S hS
        (targetFibreProductComparison B S hS 𝒳 𝒴 F 𝒳' 𝒴' F' G H γ)))) :
    IsSurjectiveOnObjects B S hS (finiteHilbertFibered B S hS d 𝒳' 𝒴' F').val.p
      (finiteHilbertFibered B S hS d 𝒳 𝒴 F).val.p
      (CatFiberedInGroupoids.homFunctor
        (mapRelativeFibered B S hS d 𝒳 𝒴 F 𝒳' 𝒴' F' G H γ))

Tag 05YH, a lemma

Tag 05YH in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpacesForgetToProduct_of_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/ProductFibreEquivalence.lean, line 1030.

Let F : 𝒳 ⟶ 𝒴 be a 1-morphism of stacks in groupoids over the big fppf site of a scheme S and let d be a natural number. If the diagonal 𝒴 ⟶ 𝒴 × 𝒴 is representable by algebraic spaces then the 1-morphism

ℋ_d(𝒳/𝒴) ⟶ ℋ_d(𝒳) × 𝒴

of Equation 05WD is representable by algebraic spaces, in the sense of Stacks 02ZW.

theorem isRepresentableByAlgebraicSpacesForgetToProduct_of_diagonal
    (hΔ : HasRepresentableDiagonal B S hS (targetCFG (𝒴 := 𝒴))) :
    IsRepresentableByAlgebraicSpacesForgetToProduct
      (B := B) (S := S) (hS := hS) (d := d) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)

Tag 05YJ, a lemma

Tag 05YJ in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_mapRelative_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbertRelativeRepresentable.lean, line 307.

Stacks 05YJ. Let G : 𝒳' ⟶ 𝒳 be a 1-morphism of stacks in groupoids over the big fppf site of S which is representable by algebraic spaces, and let γ present 𝒳' ⟶ 𝒴 as the composite of G with F : 𝒳 ⟶ 𝒴. Then the canonical 1-morphism ℋ_d(𝒳'/𝒴) ⟶ ℋ_d(𝒳/𝒴) of degree-d relative finite Hilbert stacks is representable by algebraic spaces.

The fibre over the universal family of an object ξ = (U, Z, y, x, α) is the restriction of scalars along Z ⟶ U of an algebraic space representing the fibre of G over x, which is an algebraic space by Stacks 05YF; that is AlgebraicGeometry.Stack.FiniteHilbert.Object.exists_isAlgebraicSpace_sectionSpace. An arbitrary scheme-valued point reduces to those by the 2-Yoneda normalisation AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_of_universalFamilies.

theorem isRepresentableByAlgebraicSpaces_mapRelative_of_representable
    (γ : BasedFunctor.comp F' (𝟙 𝒴.toBasedCategory) ≅ BasedFunctor.comp G F)
    (hG : IsRepresentableByAlgebraicSpaces B S hS G) :
    IsRepresentableByAlgebraicSpaces B S hS
      (mapRelative B S hS d 𝒳' 𝒴 𝒳 𝒴 F' F G (𝟙 𝒴.toBasedCategory) γ)

Tag 06CH, a lemma

Tag 06CH in the Stacks Project.

AlgebraicGeometry.Stack.isLimitPreservingOnObjects_finiteHilbertToTargetCFG, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LimitPreserving.lean, line 554. The attribute's comment: “p : ℋ_d(𝒳/𝒴) ⟶ 𝒴 is limit preserving on objects”.

Stacks 06CH. Let F : 𝒳 ⟶ 𝒴 be a 1-morphism of stacks in groupoids over the big fppf site of S which is representable by algebraic spaces (Stacks 02ZW) and locally of finite presentation (every algebraic space representing a base change of F along a scheme-valued point of 𝒴 has locally finitely presented structural morphism, Stacks 03YK). Then p : ℋ_d(𝒳/𝒴) ⟶ 𝒴 is limit preserving on objects (Stacks 06CU).

The affine limits U = lim U_i of Stacks 06CU are indexed, as in the source, by a set: the index category lies in the universe of the schemes.

Given an object Ξ = (U, Z, y, x, α) of ℋ_d(𝒳/𝒴) over the limit and a comparison of y with an object y_i of 𝒴 at the stage i, the cover Z, the object x and the identification α composed with that comparison spread out to a cover Z_{i'}, an object x_{i'} and an identification η at a later stage i' (Stacks 01ZM and the degree-d form of Stacks 06AC for the cover, Stacks 06CX for the object and the identification). Lift y_i along U_{i'} ⟶ U_i to y_{i'}; the lift is strongly cartesian, so η factors uniquely through it, giving the identification α_{i'} of Ξ_{i'}, and the comparison factors uniquely through it, giving the morphism of objects of 𝒴 of the morphism Ξ ⟶ Ξ_{i'}. The remaining fields of that morphism are the spread-out data, and its compatibility condition holds because both of its sides factor the same morphism through the lift.

theorem isLimitPreservingOnObjects_finiteHilbertToTargetCFG
    (hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom) :
    BigFppfOver.IsLimitPreservingOnObjects.{u, u, u} B S hS
      (finiteHilbertCFG.{u, v, w, ws} B S hS 𝒳 𝒴 F d)
      (CatFiberedInGroupoids.mk 𝒴.toBasedCategory
        𝒴.isStackInGroupoids.isFiberedInGroupoids)
      (finiteHilbertToTargetCFG.{u, v, w, ws} B S hS 𝒳 𝒴 F d)

Sources

• Section 97.12, Tag 05XM
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.mapAbsolute · AlgebraicGeometry.Stack.mapAbsolute_comp_forgetAbsoluteStructure · AlgebraicGeometry.Stack.mapRelative · AlgebraicGeometry.Stack.mapRelative_obj_α · AlgebraicGeometry.Stack.mapRelative_comp_forgetRelativeStructure · AlgebraicGeometry.Stack.mapRelative_comp_forgetTarget · AlgebraicGeometry.Stack.mapRelative_comp_forgetRelativeToFiniteCover · AlgebraicGeometry.Stack.isEquivalence_hilbertComparison

Section97.13 The finite Hilbert stack of a point#

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

Tag 05YM, an equation

Tag 05YM in the Stacks Project.

AlgebraicGeometry.FiniteFreeAlgebra.representation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/Scheme.lean, line 127.

Points of the scheme of structure constants over T are naturally free d-dimensional algebras over Γ(T, 𝒪_T).

noncomputable def representation : Representation.{u} d

AlgebraicGeometry.FiniteFreeAlgebra.structureConstantsOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/StructureConstantsSpace.lean, line 58. The attribute's comment: “the scheme of structure constants over the integers”.

The scheme of structure constants, as a scheme over the integers.

noncomputable abbrev structureConstantsOver : Over (Spec (CommRingCat.of (ULift.{u} ℤ)))

AlgebraicGeometry.FiniteFreeAlgebra.structureConstantsBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/StructureConstantsSpace.lean, line 64. The attribute's comment: “the scheme of structure constants over a general base”.

The scheme X_S of structure constants over a scheme S, obtained by base change from the integers.

noncomputable abbrev structureConstantsBaseChange (S : Scheme.{u}) : Over S

AlgebraicGeometry.FiniteFreeAlgebra.structureConstantsBaseChangePoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/StructureConstantsSpace.lean, line 82. The attribute's comment: “the points of the scheme of structure constants over a general base”.

The points of X_S over a scheme T over S are the free d-dimensional algebras over Γ(T, 𝒪_T).

noncomputable def structureConstantsBaseChangePoints (S : Scheme.{u}) (T : Over S) :
    (T ⟶ structureConstantsBaseChange.{u} d S) ≃ FiniteFreeAlgebra Γ(T.left, ⊤) d

AlgebraicGeometry.FiniteFreeAlgebra.structureConstantsBaseChangePoints_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/StructureConstantsSpace.lean, line 90. The attribute's comment: “the points of the scheme of structure constants over a general base”.

AlgebraicGeometry.FiniteFreeAlgebra.structureConstantsBaseChangePoints is natural in the scheme over S: restricting a point along f extends the scalars of its structure constants along the induced map of global sections.

theorem structureConstantsBaseChangePoints_naturality (S : Scheme.{u}) {T U : Over S}
    (f : T ⟶ U) (x : U ⟶ structureConstantsBaseChange.{u} d S) :
    FiniteFreeAlgebra.map f.left.appTop.hom
        (structureConstantsBaseChangePoints d S U x) =
      structureConstantsBaseChangePoints d S T (f ≫ x)

AlgebraicGeometry.Space.structureConstantsSiteObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/StructureConstantsSpace.lean, line 127. The attribute's comment: “the scheme of structure constants as an object of the site”.

The scheme X_S of structure constants over S, read as an object of the big fppf site over S.

noncomputable def structureConstantsSiteObject : BigFppfOver 𝒞 S hS

AlgebraicGeometry.Space.structureConstantsSpaceOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/StructureConstantsSpace.lean, line 134. The attribute's comment: “the scheme of structure constants as an object over an algebraic space”.

The algebraic space B ×_S X_S over an algebraic space B over S, as an object of the slice of presheaves on the big fppf site over B.

noncomputable def structureConstantsSpaceOver (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u) :
    Over B

AlgebraicGeometry.Space.isAlgebraicSpace_structureConstantsSpaceOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/StructureConstantsSpace.lean, line 140. The attribute's comment: “the scheme of structure constants as an object over an algebraic space”.

The presheaf underlying B ×_S X_S is an algebraic space over S.

theorem isAlgebraicSpace_structureConstantsSpaceOver (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
    (hB : IsAlgebraicSpace 𝒞 S hS B) :
    IsAlgebraicSpace 𝒞 S hS
      (B ⨯ yoneda.obj (structureConstantsSiteObject 𝒞 S hS d))

Tag 05YN, an equation

Tag 05YN in the Stacks Project.

AlgebraicGeometry.FiniteFreeAlgebra.presheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/Presheaf.lean, line 290.

The presheaf in groupoids FA_d of free rank-d commutative algebra structures and their isomorphisms.

noncomputable def presheaf (B : BigFppfSite.{u}) (d : ℕ) [NeZero d] : Presheaf B d

Tag 05YP, a lemma

Tag 05YP in the Stacks Project.

AlgebraicGeometry.FiniteFreeAlgebra.presheaf_actionGroupoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/ActionGroupoid.lean, line 1093.

Conjugation defines an action on the scheme of structure constants, and FA_d is naturally isomorphic to its action-groupoid functor, by the representing equivalence on objects and the inverse matrices on arrows.

public theorem presheaf_actionGroupoid
    (B : BigFppfSite.{u}) (d : ℕ) [NeZero d]
    (F : Presheaf B d) :
    ∃ (laws : ConjugationPreservesAlgebraLaws.{u} d)
      (P : ActionGroupoidPresheaf B d laws)
      (η : F.functor ≅ P.toFunctor),
      (∀ (T : B.Schemesᵒᵖ) (x : F.functor.obj T),
        (η.hom.app T).obj x =
          ((representation.{u} d).equiv T.unop.1).symm
            (F.objectEquiv T x)) ∧
      (∀ (T : B.Schemesᵒᵖ) (x y : F.functor.obj T) (e : x ⟶ y),
        (P.arrowEquiv T _ _ ((η.hom.app T).map e)).1.1 =
          (F.arrowEquiv T x y e).matrix⁻¹)

Tag 05YQ, a proposition

Tag 05YQ in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_finiteCoverFibered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/FiniteCoverAlgebraicStack.lean, line 68. The attribute's comment: “the second assertion: ℋ_d is an algebraic stack over S, transported along the equivalence of the first assertion from the quotient stack [X/G] of the conjugation action, which is an algebraic stack by Stacks 04TK”.

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

theorem isAlgebraicStack_finiteCoverFibered :
    IsAlgebraicStack.{u, w} 𝒞 S hS (finiteCoverFibered 𝒞 S hS d).val

AlgebraicGeometry.FiniteFreeAlgebra.nonempty_isEquivalenceOver_finiteCover_conjugationQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/FiniteCoverStructureConstants.lean, line 84. The attribute's comment: “the category of degree-d finite locally free covers is equivalent, over the big fppf site over S, to the quotient stack [X/G] of the conjugation action of the unit-fixing subgroup G of GL_d on the scheme X of structure constants”.

The category ℋ_d of degree-d finite locally free covers is equivalent, over the big fppf site over S, to the quotient stack [X/G] of the conjugation action of the unit-fixing subgroup G ⊆ GL_d on the scheme X of structure constants of free d-dimensional algebras, by the extension of AlgebraicGeometry.FiniteFreeAlgebra.specQuotientPrestack across the stackification AlgebraicGeometry.Stack.toQuotientStack.

theorem nonempty_isEquivalenceOver_finiteCover_conjugationQuotient :
    Nonempty (Functor.IsEquivalenceOver
      (Space.structureConstantsQuotientStack 𝒞 S hS d (Space.terminalSpace 𝒞 S hS)).p
      (Functor.uliftHomProj (AlgebraicGeometry.Stack.finiteCoverProjection
        (B := 𝒞) (S := S) (hS := hS) (d := d)))
      (Functor.Stackification.extend
        (AlgebraicGeometry.Stack.isFibredOneMorphism_toQuotientStack
          (conjugationGroupoidInSpaces 𝒞 S hS d (isAlgebraicSpace_conjugationGroup 𝒞 S hS d)
          (isAlgebraicSpace_conjugationObject 𝒞 S hS d)))
        (isFibredOneMorphism_specQuotientPrestack
          (conjugationGroupoidInSpaces 𝒞 S hS d (isAlgebraicSpace_conjugationGroup 𝒞 S hS d)
          (isAlgebraicSpace_conjugationObject 𝒞 S hS d))
          (conjugationGroupoidIso 𝒞 S hS d))
        (AlgebraicGeometry.Stack.isLocallyBijective_toQuotientStack
          (conjugationGroupoidInSpaces 𝒞 S hS d (isAlgebraicSpace_conjugationGroup 𝒞 S hS d)
          (isAlgebraicSpace_conjugationObject 𝒞 S hS d)))
        (isStack_uliftHomProj_finiteCoverProjection 𝒞 S hS d).isMorSheaf
        (AlgebraicGeometry.Stack.essImage_toQuotientStack
          (conjugationGroupoidInSpaces 𝒞 S hS d (isAlgebraicSpace_conjugationGroup 𝒞 S hS d)
          (isAlgebraicSpace_conjugationObject 𝒞 S hS d)))
        (isStack_uliftHomProj_finiteCoverProjection 𝒞 S hS d).hasEffectiveDescent))

AlgebraicGeometry.FiniteFreeAlgebra.algEquivCarrierOfIsUnit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/LocalUnitBasis.lean, line 179. The attribute's comment: “clause (b) of the proof over an affine base: inverting one coordinate of the unit presents the algebra as the algebra of a free d-dimensional structure”.

If one coordinate of the unit becomes invertible in S, the base changed algebra S ⊗[R] A is the algebra of a free d-dimensional structure over S.

noncomputable def algEquivCarrierOfIsUnit (b : Module.Basis (Fin d) R A) (i : Fin d)
    (hi : IsUnit (algebraMap R S (b.repr 1 i))) :
    (S ⊗[R] A) ≃ₐ[S] Carrier (structureOfIsUnit S b i hi)

AlgebraicGeometry.FiniteFreeAlgebra.exists_structure_algEquiv_localizationAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/LocalUnitBasis.lean, line 202. The attribute's comment: “clause (b) of the proof over an affine base, on the standard open cover cut out by the coordinates of the unit”.

Over each member of the standard open cover of Spec R cut out by the coordinates of the unit, the algebra is the algebra of a free d-dimensional structure.

theorem exists_structure_algEquiv_localizationAway (b : Module.Basis (Fin d) R A) (i : Fin d) :
    ∃ m : FiniteFreeAlgebra (Localization.Away (b.repr 1 i)) d,
      Nonempty ((Localization.Away (b.repr 1 i) ⊗[R] A) ≃ₐ[Localization.Away (b.repr 1 i)]
        Carrier m)

AlgebraicGeometry.FiniteFreeAlgebra.algEquivCarrierOfBasis, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/OfBasis.lean, line 105. The attribute's comment: “transport of the multiplication along a basis whose first vector is the unit, over an affine base”.

An algebra that is free of rank d on a basis whose first vector is the unit is isomorphic, as an R-algebra, to the algebra of the structure constants of that basis.

noncomputable def algEquivCarrierOfBasis (b : Module.Basis (Fin d) R A) (hb : b 0 = 1) :
    A ≃ₐ[R] Carrier (ofBasis b hb)

AlgebraicGeometry.FiniteFreeAlgebra.isFiniteLocallyFreeOfRank_specCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/Spectrum.lean, line 66. The attribute's comment: “the degree-d clause for the spectrum of a free d-dimensional structure over a ring, in the affine case”.

The spectrum of the algebra of a free d-dimensional structure is finite locally free of degree d over the base.

theorem isFiniteLocallyFreeOfRank_specCover (m : FiniteFreeAlgebra R d) :
    Stacks.Morphisms.IsFiniteLocallyFreeOfRank (specCover m).hom d

AlgebraicGeometry.FiniteFreeAlgebra.structureIsoEquivSpecIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/Spectrum.lean, line 112. The attribute's comment: “clause (a) of the proof over an affine base: Isom (m, n) is Isom (Spec m, Spec n) as schemes over the base”.

The isomorphisms of two free d-dimensional structures over R are exactly the isomorphisms of their spectra as schemes over Spec R.

noncomputable def structureIsoEquivSpecIso (m n : FiniteFreeAlgebra R d) :
    StructureIso m n ≃ (specCover m ≅ specCover n)

AlgebraicGeometry.FiniteFreeAlgebra.Carrier.basis, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/StructureAlgebra.lean, line 319. The attribute's comment: “the module underlying the algebra of a free d-dimensional structure is free of rank d, the affine core of the degree-d clause for the relative spectrum of m”.

The module underlying the algebra of a free d-dimensional structure is free with basis the d standard basis vectors.

noncomputable def basis (m : FiniteFreeAlgebra R d) : Module.Basis (Fin d) R (Carrier m)

AlgebraicGeometry.FiniteFreeAlgebra.structureIsoEquivAlgEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/FiniteFreeAlgebra/StructureAlgebra.lean, line 524. The attribute's comment: “clause (a) of the proof, in algebraic form: the isomorphisms of two free d-dimensional structures are exactly the algebra isomorphisms of the associated algebras”.

The isomorphisms of two free d-dimensional structures over a ring are exactly the R-algebra isomorphisms of the two associated algebras.

noncomputable def structureIsoEquivAlgEquiv (m n : FiniteFreeAlgebra R d) :
    StructureIso m n ≃ (Carrier m ≃ₐ[R] Carrier n)

Sources

• Section 97.13, Tag 05YL
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FiniteFreeAlgebra.representation · AlgebraicGeometry.FiniteFreeAlgebra.structureConstantsOver · AlgebraicGeometry.FiniteFreeAlgebra.structureConstantsBaseChange · AlgebraicGeometry.FiniteFreeAlgebra.structureConstantsBaseChangePoints · AlgebraicGeometry.FiniteFreeAlgebra.structureConstantsBaseChangePoints_naturality · AlgebraicGeometry.Space.structureConstantsSiteObject · AlgebraicGeometry.Space.structureConstantsSpaceOver · AlgebraicGeometry.Space.isAlgebraicSpace_structureConstantsSpaceOver

Section97.14 Finite Hilbert stacks of spaces#

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

Tag 05YS, a lemma

Tag 05YS in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_absoluteHilbertFibered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/HilbertCoverAlgebraic.lean, line 96. The attribute's comment: “NeZero d restricts nothing: Examples of Stacks, Section 95.18 (Stacks 05WA) introduces ℋ_d(X) only For each integer d ≥ 1, and the source's proof of this lemma cites Stacks 05YQ, which stands under the Let d ≥ 1 be an integer of Section 97.13 (Stacks 05YL)”.

The finite Hilbert stack ℋ_d(𝒳) of an algebraic space 𝒳 over S is an algebraic stack.

theorem isAlgebraicStack_absoluteHilbertFibered [NeZero d]
    (𝒳 : StackInGroupoids.{w, u, u, u + 1, u + 1} (BigFppfOver B S hS)
      (BigFppfOver.topology B S hS))
    (h𝒳 : IsRepresentableByAlgebraicSpace B S hS
      (CatFiberedInGroupoids.mk 𝒳.toBasedCategory
        𝒳.isStackInGroupoids.isFiberedInGroupoids)) :
    IsAlgebraicStack.{u, w} B S hS (absoluteHilbertFibered 𝒳 d).val

Tag 06CI, a lemma

Tag 06CI in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_finiteHilbertFibered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/RelativeAlgebraicity.lean, line 554. The attribute's comment: “for positive degree d, the domain on which the source defines the finite Hilbert stack”.

Stacks 06CI. For positive degree d, the relative finite Hilbert stack ℋ_d(𝒳/𝒴) of a 1-morphism F : 𝒳 ⟶ 𝒴 of stacks in groupoids over the big fppf site of S with 𝒳 representable by an algebraic space and F representable by algebraic spaces, surjective, flat and locally of finite presentation is an algebraic stack.

The hypothesis hd : 0 < d is the domain of the statement, not a restriction of it: the source defines ℋ_d(𝒳/𝒴) only for d ≥ 1 (Examples of Stacks, Section 05WA).

Writing 𝒰 for a scheme atlas of ℋ_d(𝒳) and 𝒲 = ℋ_d(𝒳/𝒴) ×_{ℋ_d(𝒳)} 𝒰, the 1-morphism 𝒲 ⟶ ℋ_d(𝒳/𝒴) is a base change of 𝒰 ⟶ ℋ_d(𝒳), hence representable by algebraic spaces, surjective and smooth (Stacks 0302 and Stacks 045C), and 𝒲 is representable by an algebraic space, so Stacks 05UL applies to it.

theorem isAlgebraicStack_finiteHilbertFibered (hd : 0 < d)
    (h𝒴 : Functor.IsStack 𝒴.toBasedCategory.p (BigFppfOver.topology B S hS))
    (h𝒳 : IsRepresentableByAlgebraicSpace B S hS (targetCFG (𝒴 := 𝒳)))
    (hF : IsRepresentableByAlgebraicSpaces B S hS F)
    (hFprops : RelativeFlatPresentation (F := F)) :
    IsAlgebraicStack.{u, w} B S hS (finiteHilbertFibered B S hS d 𝒳 𝒴 F).val

Sources

• Section 97.14, Tag 05YR
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isAlgebraicStack_absoluteHilbertFibered · AlgebraicGeometry.Stack.isAlgebraicStack_finiteHilbertFibered

Section97.15 LCI locus in the Hilbert stack#

Section 97.15 of the Stacks Project, Tag 06CJ. 6 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06CJ, the section

Tag 06CJ in the Stacks Project.

AlgebraicGeometry.Stack.FiniteHilbert.lciLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocus.lean, line 158. The attribute's comment: “the objects of ℋ_d(𝒳/𝒴) with unramified Koszul relative map”.

The objects of the relative finite Hilbert category ℋ_d(𝒳/𝒴) whose relative map x_α : Z ⟶ X_y of Stacks 06CK is unramified and a local complete intersection morphism, for every algebraic space representing the relevant 2-fibre product and every equivalence exhibiting it.

def lciLocus : ObjectProperty (Object B S hS 𝒳 𝒴 F d)

AlgebraicGeometry.Stack.lciFiniteHilbertCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocus.lean, line 178. The attribute's comment: “the full subcategory ℋ_{d,lci}(𝒳/𝒴) of ℋ_d(𝒳/𝒴)”.

The local complete intersection locus ℋ_{d,lci}(𝒳/𝒴): the full subcategory of the relative finite Hilbert category on the objects whose relative map is unramified and a local complete intersection morphism, regarded as a category over the big fppf site through the restriction of the canonical projection.

noncomputable def lciFiniteHilbertCategory : BasedCategory (BigFppfOver B S hS)

AlgebraicGeometry.Stack.lciFiniteHilbertInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocus.lean, line 187. The attribute's comment: “the inclusion ℋ_{d,lci}(𝒳/𝒴) ⊂ ℋ_d(𝒳/𝒴)”.

The inclusion ℋ_{d,lci}(𝒳/𝒴) ⊂ ℋ_d(𝒳/𝒴) of the local complete intersection locus into the relative finite Hilbert category, as a 1-morphism of categories over the big fppf site.

def lciFiniteHilbertInclusion :
    lciFiniteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d) ⥤ᵇ
      finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d)

AlgebraicGeometry.Stack.FiniteHilbert.RelativeMapData.map_hom_ofHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusBaseChange.lean, line 456. The attribute's comment: “the remark preceding the definition of the locus: the relative map of the source of a morphism of quintuples is the base change of the relative map of the target along the base component”.

The relative map of the transported data is the restriction of the original relative map along the base component of the morphism, read through the comparison of the representable presheaf of the cover of the source quintuple with the restriction of the representable presheaf of the cover of the target — an isomorphism by AlgebraicGeometry.Stack.FiniteHilbert.RelativeMapData.isIso_restrictYonedaHom_coverComparison, so that the relative map of the source is the base change of the relative map of the target.

theorem map_hom_ofHom :
    (ofHom φ D).map.hom =
      OverShriek.restrictYonedaHom φ.f.left (coverComparison φ) ≫
        (OverShriek.relocalizeRestrict φ.f.left).map D.map.hom

AlgebraicGeometry.Stack.FiniteHilbert.lciLocus_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusChoice.lean, line 179. The attribute's comment: “membership of the locus is testable on a single choice of the data exhibiting the relative map”.

A quintuple lies in the local complete intersection locus exactly when the relative map attached to one set of data exhibiting it is unramified and a local complete intersection morphism.

theorem lciLocus_iff {P : Object B S hS 𝒳 𝒴 F d} (D : RelativeMapData P) :
    lciLocus (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d) P ↔
      (Space.IsUnramified B P.U.left.1 P.U.left.2 D.map.hom ∧
        Space.IsLocalCompleteIntersection B P.U.left.1 P.U.left.2 D.map.hom)

Tag 06CK, an equation

Tag 06CK in the Stacks Project.

AlgebraicGeometry.Stack.relativeObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RelativeMapToRepresentingSpace.lean, line 72. The attribute's comment: “the object (Z, Z → U, x, α) of the 2-fibre product”.

The object ξ = (Z, Z → U, x, α) of the 2-fibre product (Sch/U)_{fppf} ×_{y, 𝒴, F} 𝒳 attached to a scheme Z over U, an object x of 𝒳 over Z and an isomorphism α : y|_Z ⟶ F(x) vertical over Z. It lies over Z for the first projection.

def relativeObj (Z : BigFppfOver B U.left.1 U.left.2) (x : 𝒳.obj)
    (hx : 𝒳.p.obj x = (Over.map U.hom).obj Z) (α : y.obj Z ≅ F.toFunctor.obj x)
    (hα : 𝒴.p.IsHomLift (𝟙 ((Over.map U.hom).obj Z)) α.hom) :
    TwoFibreProductOver (Over.map U.hom) 𝒳.p 𝒴.p y F.toFunctor

AlgebraicGeometry.Stack.relativeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/RelativeMapToRepresentingSpace.lean, line 214. The attribute's comment: “the morphism x_α of the left-hand diagram”.

The morphism x_α : Z ⟶ X_y of algebraic spaces over U attached to a scheme Z over U, an object x of 𝒳 over Z and an isomorphism α : y|_Z ⟶ F(x) vertical over Z: the morphism of presheaves on the big fppf site of U named, under the Yoneda lemma, by the section of X_y over Z that ξ = (Z, Z → U, x, α) names.

def relativeMap (F : 𝒳 ⥤ᵇ 𝒴) (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.obj)
    (e : StacksRepresentableCFG.EquivalenceOver
      (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.p 𝒴.p y F.toFunctor)
      (presheafOfCategories (Xy ⋙ typeToCat)).p)
    (hXy : IsAlgebraicSpace B U.left.1 U.left.2 Xy)
    (Z : BigFppfOver B U.left.1 U.left.2) (x : 𝒳.obj)
    (hx : 𝒳.p.obj x = (Over.map U.hom).obj Z) (α : y.obj Z ≅ F.toFunctor.obj x)
    (hα : 𝒴.p.IsHomLift (𝟙 ((Over.map U.hom).obj Z)) α.hom) :
    (⟨yoneda.obj Z, isAlgebraicSpace_yoneda B U.left.1 U.left.2 Z⟩ :
        AlgebraicSpaces B U.left.1 U.left.2) ⟶ ⟨Xy, hXy⟩

AlgebraicGeometry.Stack.FiniteHilbert.RelativeMapData.exists_iso_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusChoice.lean, line 153. The attribute's comment: “the remark following the tag: the relative map does not depend on the data exhibiting it”.

Two sets of data exhibiting the relative map of one object of ℋ_d(𝒳/𝒴) give the same morphism up to an isomorphism of its target.

theorem RelativeMapData.exists_iso_map {P : Object B S hS 𝒳 𝒴 F d}
    (D₁ D₂ : RelativeMapData P) :
    ∃ i : D₁.Xy ≅ D₂.Xy, D₁.map.hom ≫ i.hom = D₂.map.hom

Tag 06CL, a lemma

Tag 06CL in the Stacks Project.

AlgebraicGeometry.Stack.exists_isOpenImmersion_representing_lciFiniteHilbertInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusOpen.lean, line 403. The attribute's comment: “the inclusion ℋ_{d,lci}(𝒳/𝒴) ⊂ ℋ_d(𝒳/𝒴) is representable by an open subscheme of the base, with the open locus of Stacks 05X8 and 06CE and isomorphism-invariance of the locus as explicit hypotheses”.

Stacks 06CL. The inclusion ℋ_{d,lci}(𝒳/𝒴) ⟶ ℋ_d(𝒳/𝒴) of the local complete intersection locus is representable: every 2-fibre product of it with a scheme-valued point of ℋ_d(𝒳/𝒴) is represented by an object of the big fppf site of the base which is an open subscheme of it, namely the open subscheme cut out by the locus.

theorem exists_isOpenImmersion_representing_lciFiniteHilbertInclusion
    (_hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (_hFflat : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsFlat B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (_hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hiso : ObjectProperty.IsClosedUnderIsomorphisms
      (FiniteHilbert.lciLocus (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d)))
    (hopen : FiniteHilbert.HasOpenLciLocus B S hS 𝒳 𝒴 F d) :
    ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤
        (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
          (d := d)).obj),
      y ⋙ (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
        (d := d)).p = Over.map U.hom →
      ∃ V : BigFppfOver B U.left.1 U.left.2, IsOpenImmersion V.hom.hom ∧
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom)
            (lciFiniteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).p
            (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).p y
            (lciFiniteHilbertInclusion (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).toFunctor)
          (presheafOfCategories (yoneda.obj V ⋙ typeToCat)).p)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_lciFiniteHilbertInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusOpen.lean, line 452. The attribute's comment: “the inclusion ℋ_{d,lci}(𝒳/𝒴) ⊂ ℋ_d(𝒳/𝒴) is representable by algebraic spaces, with the open locus of Stacks 05X8 and 06CE and isomorphism-invariance of the locus as explicit hypotheses”.

Stacks 06CL. The inclusion ℋ_{d,lci}(𝒳/𝒴) ⟶ ℋ_d(𝒳/𝒴) of the local complete intersection locus is representable by algebraic spaces, the representing algebraic space of a base change being the open subscheme of the base cut out by the locus.

theorem isRepresentableByAlgebraicSpaces_lciFiniteHilbertInclusion
    (_hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (_hFflat : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsFlat B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (_hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hiso : ObjectProperty.IsClosedUnderIsomorphisms
      (FiniteHilbert.lciLocus (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d)))
    (hopen : FiniteHilbert.HasOpenLciLocus B S hS 𝒳 𝒴 F d) :
    IsRepresentableByAlgebraicSpaces B S hS
      (lciFiniteHilbertInclusion (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
        (d := d))

AlgebraicGeometry.Stack.isOpenImmersion_lciFiniteHilbertInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusOpen.lean, line 528. The attribute's comment: “the inclusion ℋ_{d,lci}(𝒳/𝒴) ⊂ ℋ_d(𝒳/𝒴) is an open immersion, with the open locus of Stacks 05X8 and 06CE and isomorphism-invariance of the locus as explicit hypotheses”.

Stacks 06CL. The inclusion ℋ_{d,lci}(𝒳/𝒴) ⟶ ℋ_d(𝒳/𝒴) of the local complete intersection locus is an open immersion: every algebraic space representing a base change of it along a scheme-valued point of ℋ_d(𝒳/𝒴) has open immersion structural morphism, read as a morphism of algebraic spaces over S.

This is the condition of Stacks 04XB at AlgebraicGeometry.Space.IsOpenImmersion, written out, and the representing algebraic space is the open subscheme of the base cut out by the locus.

theorem isOpenImmersion_lciFiniteHilbertInclusion
    (_hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (_hFflat : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsFlat B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (_hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hiso : ObjectProperty.IsClosedUnderIsomorphisms
      (FiniteHilbert.lciLocus (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d)))
    (hopen : FiniteHilbert.HasOpenLciLocus B S hS 𝒳 𝒴 F d) :
    ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤
        (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
          (d := d)).obj),
      y ⋙ (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
        (d := d)).p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom)
            (lciFiniteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).p
            (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).p y
            (lciFiniteHilbertInclusion (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).toFunctor)
          (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsOpenImmersion B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom

AlgebraicGeometry.Stack.isStackInGroupoids_lciFiniteHilbertCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusOpen.lean, line 585. The attribute's comment: “ℋ_{d,lci}(𝒳/𝒴) is a stack in groupoids, with Stacks 05UN for the full subcategories of ℋ_d(𝒳/𝒴), that ℋ_d(𝒳/𝒴) is a stack in groupoids, the open locus of Stacks 05X8 and 06CE and isomorphism-invariance of the locus as explicit hypotheses”.

Stacks 06CL. The local complete intersection locus ℋ_{d,lci}(𝒳/𝒴) is a stack in groupoids over the big fppf site of S.

By Stacks 05UN this follows from the representability by algebraic spaces of the inclusion into ℋ_d(𝒳/𝒴) together with ℋ_d(𝒳/𝒴) being a stack in groupoids.

theorem isStackInGroupoids_lciFiniteHilbertCategory
    (hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (hFflat : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsFlat B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hiso : ObjectProperty.IsClosedUnderIsomorphisms
      (FiniteHilbert.lciLocus (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d)))
    (hopen : FiniteHilbert.HasOpenLciLocus B S hS 𝒳 𝒴 F d)
    (hHd : Functor.IsStackInGroupoids.{w}
      (finiteHilbertProjection (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d))
      (BigFppfOver.topology B S hS))
    (h05UN : ∀ (Q : ObjectProperty (FiniteHilbert.Object B S hS 𝒳 𝒴 F d))
      (j : BasedCategory.ofFunctor (Q.ι ⋙ finiteHilbertProjection (B := B) (S := S) (hS := hS)
            (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F) (d := d)) ⥤ᵇ
          finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
            (d := d)),
      IsRepresentableByAlgebraicSpaces B S hS j →
      Functor.IsStackInGroupoids.{w}
        (finiteHilbertProjection (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
          (d := d)) (BigFppfOver.topology B S hS) →
      Functor.IsStackInGroupoids.{w}
        (Q.ι ⋙ finiteHilbertProjection (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
          (d := d)) (BigFppfOver.topology B S hS)) :
    Functor.IsStackInGroupoids.{w}
      (lciFiniteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
        (d := d)).p (BigFppfOver.topology B S hS)

AlgebraicGeometry.Stack.exists_isOpenImmersion_representing_lciFiniteHilbertInclusion_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusRepresentable.lean, line 220. The attribute's comment: “the inclusion ℋ_{d,lci}(𝒳/𝒴) ⊂ ℋ_d(𝒳/𝒴) is representable, by an open subscheme of the base”.

The inclusion ℋ_{d,lci}(𝒳/𝒴) ⟶ ℋ_d(𝒳/𝒴) of the local complete intersection locus is representable: every 2-fibre product of it with a scheme-valued point of ℋ_d(𝒳/𝒴) is represented by an object of the big fppf site of the base which is an open subscheme of it, namely the open subscheme cut out by the locus. This is "representable" in the sense of Stacks 04ST, by a scheme.

theorem exists_isOpenImmersion_representing_lciFiniteHilbertInclusion_of_flat
    (hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (hFflat : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsFlat B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom) :
    ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤
        (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
          (d := d)).obj),
      y ⋙ (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
        (d := d)).p = Over.map U.hom →
      ∃ V : BigFppfOver B U.left.1 U.left.2, IsOpenImmersion V.hom.hom ∧
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom)
            (lciFiniteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).p
            (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).p y
            (lciFiniteHilbertInclusion (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).toFunctor)
          (presheafOfCategories (yoneda.obj V ⋙ typeToCat)).p)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_lciFiniteHilbertInclusion_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusRepresentable.lean, line 266. The attribute's comment: “the inclusion ℋ_{d,lci}(𝒳/𝒴) ⊂ ℋ_d(𝒳/𝒴) is representable by algebraic spaces”.

The inclusion ℋ_{d,lci}(𝒳/𝒴) ⟶ ℋ_d(𝒳/𝒴) of the local complete intersection locus is representable by algebraic spaces, the representing algebraic space of a base change being the open subscheme of the base cut out by the locus.

theorem isRepresentableByAlgebraicSpaces_lciFiniteHilbertInclusion_of_flat
    (hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (hFflat : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsFlat B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom) :
    IsRepresentableByAlgebraicSpaces B S hS
      (lciFiniteHilbertInclusion (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
        (d := d))

AlgebraicGeometry.Stack.isOpenImmersion_lciFiniteHilbertInclusion_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusRepresentable.lean, line 301. The attribute's comment: “the inclusion ℋ_{d,lci}(𝒳/𝒴) ⊂ ℋ_d(𝒳/𝒴) is an open immersion”.

The inclusion ℋ_{d,lci}(𝒳/𝒴) ⟶ ℋ_d(𝒳/𝒴) of the local complete intersection locus is an open immersion: every algebraic space representing a base change of it along a scheme-valued point of ℋ_d(𝒳/𝒴) has open immersion structural morphism, read as a morphism of algebraic spaces over S. This is the condition of Stacks 04XB at AlgebraicGeometry.Space.IsOpenImmersion, written out.

theorem isOpenImmersion_lciFiniteHilbertInclusion_of_flat
    (hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (hFflat : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsFlat B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom) :
    ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤
        (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
          (d := d)).obj),
      y ⋙ (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
        (d := d)).p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom)
            (lciFiniteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).p
            (finiteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).p y
            (lciFiniteHilbertInclusion (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
              (d := d)).toFunctor)
          (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsOpenImmersion B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom

AlgebraicGeometry.Stack.isStackInGroupoids_lciFiniteHilbertCategory_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusStack.lean, line 70. The attribute's comment: “ℋ_{d,lci}(𝒳/𝒴) is a stack in groupoids”.

Stacks 06CL. For a 1-morphism F : 𝒳 ⟶ 𝒴 of stacks in groupoids over the big fppf site of S which is representable by algebraic spaces, flat and locally of finite presentation, the local complete intersection locus ℋ_{d,lci}(𝒳/𝒴) is a stack in groupoids over the big fppf site of S.

The ambient ℋ_d(𝒳/𝒴) is a stack in groupoids by Stacks 05WB, and the locus is a full subcategory inherited along morphisms and local on the base by the open locus of Stacks 05X8 and 06CE, AlgebraicGeometry.Stack.FiniteHilbert.hasOpenLciLocus.

theorem isStackInGroupoids_lciFiniteHilbertCategory_of_flat
    (hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (hFflat : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsFlat B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom) :
    (lciFiniteHilbertCategory (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴) (F := F)
      (d := d)).p.IsStackInGroupoids.{w}
      (BigFppfOver.topology B S hS)

Tag 06D8, a lemma

Tag 06D8 in the Stacks Project.

AlgebraicGeometry.Stack.FiniteHilbert.exists_coverDeformation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/CoverDeformationExists.lean, line 80.

Stacks 06D8. Let i : U ⟶ U' be a first-order thickening of objects of the big fppf site of S with U affine, let X' be an algebraic space over U' flat over U', let q : Z ⟶ U be finite locally free of degree d, and let f : Z ⟶ X be an unramified local complete intersection morphism into the special fibre X = U ×_{U'} X' (the restriction of X' along U ⟶ U'). Then there are q' : Z' ⟶ U' finite locally free of degree d, a cartesian square hg exhibiting Z = U ×_{U'} Z', and f' : Z' ⟶ X' restricting to f.

The source also assumes U' affine; that follows from U affine (Stacks 06AD) and is not used.

theorem exists_coverDeformation (d : ℕ) {U U' : BigFppfOver B S hS} (i : U ⟶ U')
    (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
    (hi : Stacks.Thickenings.IsFirstOrderThickening ((BigFppfOver.toScheme B S hS).map i))
    (X' : (BigFppfOver B U'.left.1 U'.left.2)ᵒᵖ ⥤ Type u)
    (hX' : IsAlgebraicSpace B U'.left.1 U'.left.2 X')
    (hflat : Space.IsFlat B U'.left.1 U'.left.2 (Space.toYonedaId B U'.left.1 U'.left.2 X'))
    {Z : BigFppfOver B S hS} (q : Z ⟶ U)
    (hq : Stacks.Morphisms.IsFiniteLocallyFreeOfRank ((BigFppfOver.toScheme B S hS).map q) d)
    (f : yoneda.obj (Over.mk q.left : BigFppfOver B U.left.1 U.left.2) ⟶
      (OverShriek.relocalizeRestrict i.left).obj X')
    (hunr : Space.IsUnramified B U.left.1 U.left.2 f)
    (hlci : Space.IsLocalCompleteIntersection B U.left.1 U.left.2 f) :
    ∃ (Z' : BigFppfOver B S hS) (q' : Z' ⟶ U') (g : Z ⟶ Z') (hg : IsPullback g q q' i),
      Stacks.Morphisms.IsFiniteLocallyFreeOfRank ((BigFppfOver.toScheme B S hS).map q') d ∧
        ∃ f' : yoneda.obj (Over.mk q'.left : BigFppfOver B U'.left.1 U'.left.2) ⟶ X',
          OverShriek.restrictYonedaHom i.left (coverComparisonOfSquare hg.w) ≫
              (OverShriek.relocalizeRestrict i.left).map f' = f

Tag 06D9, a lemma

Tag 06D9 in the Stacks Project.

AlgebraicGeometry.Stack.isFormallySmoothOnObjects_lciFiniteHilbertToTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciHilbertTargetFormallySmooth.lean, line 60.

Stacks 06D9. Let F : 𝒳 ⟶ 𝒴 be a 1-morphism of stacks in groupoids over (Sch/S)_fppf which is representable by algebraic spaces, flat and locally of finite presentation. Then p : ℋ_{d,lci}(𝒳/𝒴) ⟶ 𝒴 is formally smooth on objects (Stacks 06D0).

This is AlgebraicGeometry.Stack.isFormallySmoothOnObjects_lciFiniteHilbertToTarget_of_coverDeformations with its deformation problem solved by AlgebraicGeometry.Stack.FiniteHilbert.hasCoverDeformations, the space-level Stacks 06D8.

theorem isFormallySmoothOnObjects_lciFiniteHilbertToTarget
    (hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (hFflat : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsFlat B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom) :
    IsFormallySmoothOnObjects B S hS
      (lciFiniteHilbertFibered (isFiberedInGroupoids_lciFiniteHilbertCategory
        (FiniteHilbert.hasOpenLciLocus (d := d) hFrep hFflat hFlfp)))
      (stackFibered B S hS 𝒴)
      (lciFiniteHilbertToTargetFibered (isFiberedInGroupoids_lciFiniteHilbertCategory
        (FiniteHilbert.hasOpenLciLocus (d := d) hFrep hFflat hFlfp)))

Tag 06DA, a lemma

Tag 06DA in the Stacks Project.

AlgebraicGeometry.Stack.isSurjectiveOnObjects_lciFiniteHilbertCoproductToTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FiniteHilbert/LciLocusSurjective.lean, line 264. The attribute's comment: “∐_{d ≥ 1} ℋ_{d,lci}(𝒳/𝒴) ⟶ 𝒴 is surjective on objects, for F representable by algebraic spaces, flat, surjective and locally of finite presentation”.

Let F : 𝒳 ⟶ 𝒴 be a 1-morphism of stacks in groupoids over the big fppf site of S which is representable by algebraic spaces, flat, surjective and locally of finite presentation. Then the 1-morphism ∐_{d ≥ 1} ℋ_{d,lci}(𝒳/𝒴) ⟶ 𝒴 is surjective on objects.

theorem isSurjectiveOnObjects_lciFiniteHilbertCoproductToTarget
    (hFrep : IsRepresentableByAlgebraicSpaces B S hS F)
    (hFflat : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsFlat B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hFsurj : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsSurjective B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom)
    (hFlfp : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.toBasedCategory.obj),
      y ⋙ 𝒴.toBasedCategory.p = Over.map U.hom →
      ∀ (P : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
        (hP : IsAlgebraicSpace B U.left.1 U.left.2 P),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.toBasedCategory.p 𝒴.toBasedCategory.p y
            F.toFunctor) (presheafOfCategories (P ⋙ typeToCat)).p) →
        Space.IsLocallyOfFinitePresentation B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨P, hP⟩)).hom) :
    IsSurjectiveOnObjects B S hS
      (lciFiniteHilbertCoproductProjection (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴)
        (F := F))
      𝒴.toBasedCategory.p
      (lciFiniteHilbertCoproductToTarget (B := B) (S := S) (hS := hS) (𝒳 := 𝒳) (𝒴 := 𝒴)
        (F := F))

Sources

• Section 97.15, Tag 06CJ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.FiniteHilbert.lciLocus · AlgebraicGeometry.Stack.lciFiniteHilbertCategory · AlgebraicGeometry.Stack.lciFiniteHilbertInclusion · AlgebraicGeometry.Stack.FiniteHilbert.RelativeMapData.map_hom_ofHom · AlgebraicGeometry.Stack.FiniteHilbert.lciLocus_iff · AlgebraicGeometry.Stack.relativeObj · AlgebraicGeometry.Stack.relativeMap · AlgebraicGeometry.Stack.FiniteHilbert.RelativeMapData.exists_iso_map

Section97.16 Bootstrapping algebraic stacks#

Section 97.16 of the Stacks Project, Tag 06DB. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06DC, a theorem

Tag 06DC in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_of_flatCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatCoverAlgebraic.lean, line 84. The attribute's comment: “stated for categories fibred in groupoids with the target a stack: the source's requirement that 𝒳 and 𝒴 be stacks in groupoids is implied, for 𝒳 by clause (1) and for 𝒴 by Stacks 02ZJ”.

Artin's theorem on representability of flat groupoids. Let F : 𝒳 ⟶ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf site of S, with 𝒴 a stack. If 𝒳 is representable by an algebraic space and F is representable by algebraic spaces, surjective, flat and locally of finite presentation, then 𝒴 is an algebraic stack.

The source asks 𝒳 and 𝒴 to be stacks in groupoids. 𝒳 is one because it is representable by an algebraic space (AlgebraicGeometry.Stack.isStack_of_isRepresentableByAlgebraicSpace), and 𝒴 is a stack in groupoids at every descent universe because it is a stack (Stacks 02ZJ).

theorem isAlgebraicStack_of_flatCover
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (F : 𝒳 ⟶ 𝒴)
    (hstack : 𝒴.val.p.IsStack (BigFppfOver.topology B S hS))
    (h𝒳 : IsRepresentableByAlgebraicSpace B S hS 𝒳)
    (hF : IsRepresentableByAlgebraicSpaces B S hS F.hom)
    (hFprops : ∀ (V : BigFppfOver B S hS)
      (y : BigFppfOver B V.left.1 V.left.2 ⥤ 𝒴.val.obj)
      (_hy : y ⋙ 𝒴.val.p = Over.map V.hom)
      (G : (BigFppfOver B V.left.1 V.left.2)ᵒᵖ ⥤ Type u)
      (hG : IsAlgebraicSpace B V.left.1 V.left.2 G),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map V.hom) 𝒳.val.p 𝒴.val.p y
          (CatFiberedInGroupoids.homFunctor F))
        (presheafOfCategories (G ⋙ typeToCat)).p) →
      (let g := (algebraicSpaceMap B S hS V
        ((spacesOverSmallerBaseFunctor B V.left.1 S V.left.2 hS V.hom).obj ⟨G, hG⟩)).hom
       Space.IsSurjective B S hS g ∧ Space.IsFlat B S hS g ∧
         Space.IsLocallyOfFinitePresentation B S hS g)) :
    IsAlgebraicStack.{u, w} B S hS 𝒴.val

AlgebraicGeometry.Stack.isAlgebraicStack_of_flatPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GroupoidPresentationBootstrap.lean, line 129. The attribute's comment: “the bootstrap assembly. Stacks 05XW (representability of the diagonal of the target) and the Hilbert-stack cover of Stacks 06CI, 06CL, 06D9 and 06DA (an algebraic stack with a representable surjective smooth 1-morphism to the target) are carried as the hypotheses hdiagonal and hcover; neither is in the library. Clause (1) and the flatness and local finite presentation of clause (2) are stated but not used, the carried inputs being exactly what the source draws from them”.

Stacks 06DC, Artin's theorem on representability of flat groupoids. Let F : 𝒳 ⟶ 𝒴 be a 1-morphism of stacks in groupoids over the big fppf site of S. If 𝒳 is representable by an algebraic space and F is representable by algebraic spaces, surjective, flat and locally of finite presentation, then 𝒴 is an algebraic stack.

Two inputs of the source's proof are not in the library and are carried as hypotheses: representability of the diagonal of 𝒴, which the source gets from Stacks 05XW, and the existence of a smooth surjective cover of 𝒴 by an algebraic stack, which the source gets from the locally-complete-intersection locus of the relative Hilbert stack of F.

theorem isAlgebraicStack_of_flatPresentation
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (F : 𝒳 ⟶ 𝒴)
    (hstack : 𝒴.val.p.IsStack (BigFppfOver.topology B S hS))
    (_h𝒳 : IsRepresentableByAlgebraicSpace B S hS 𝒳)
    (_hF : IsRepresentableByAlgebraicSpaces B S hS F.hom)
    (_hFprops : ∀ (V : BigFppfOver B S hS)
      (y : BigFppfOver B V.left.1 V.left.2 ⥤ 𝒴.val.obj)
      (_hy : y ⋙ 𝒴.val.p = Over.map V.hom)
      (G : (BigFppfOver B V.left.1 V.left.2)ᵒᵖ ⥤ Type u)
      (hG : IsAlgebraicSpace B V.left.1 V.left.2 G),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map V.hom) 𝒳.val.p 𝒴.val.p y
          (CatFiberedInGroupoids.homFunctor F))
        (presheafOfCategories (G ⋙ typeToCat)).p) →
      (let g := (algebraicSpaceMap B S hS V
        ((spacesOverSmallerBaseFunctor B V.left.1 S V.left.2 hS V.hom).obj ⟨G, hG⟩)).hom
       Space.IsSurjective B S hS g ∧ Space.IsFlat B S hS g ∧
         Space.IsLocallyOfFinitePresentation B S hS g))
    (hdiagonal : IsRepresentableByAlgebraicSpaces B S hS (diagonalBasedFunctor B S hS 𝒴))
    (hcover : ∃ (𝒲 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
      (q : 𝒲 ⟶ 𝒴) (hq : IsRepresentableByAlgebraicSpaces B S hS q.hom),
      IsAlgebraicStack.{u, w} B S hS 𝒲.val ∧
        HasRelativeProperty.{u, u, u + 1, u} B S hS
          (Space.surjectiveMorphismProperty B S hS ⊓ Space.smoothMorphismProperty B S hS)
          q hq) :
    IsAlgebraicStack.{u, w} B S hS 𝒴.val

Sources

• Section 97.16, Tag 06DB
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isAlgebraicStack_of_flatCover · AlgebraicGeometry.Stack.isAlgebraicStack_of_flatPresentation

Section97.17 Applications#

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

Tag 06FH, a lemma

Tag 06FH in the Stacks Project.

AlgebraicGeometry.Stack.QuotientAtlas.isFlat_relativeProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientAtlasArrowSquare.lean, line 225. The attribute's comment: “flatness”.

The quotient-stack projection is flat. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over a scheme S of a big fppf site and assume its source and target maps s, t are flat and locally of finite presentation. Then the canonical projection π : S_U ⟶ [U/R] of Stacks 044R is flat in the sense of Stacks 03YK: every algebraic space representing a base change of π along a scheme-valued point of [U/R] has flat structural morphism.

theorem isFlat_relativeProperty (G : GroupoidInAlgebraicSpaces C S hS B)
    (hsflat : Space.IsFlat C S hS G.source.hom)
    (_htflat : Space.IsFlat C S hS G.target.hom)
    (_hslfp : Space.IsLocallyOfFinitePresentation C S hS G.source.hom)
    (_htlfp : Space.IsLocallyOfFinitePresentation C S hS G.target.hom) :
    RelativeProperty.{u, u + 1, u + 1} C S hS
      (fun ⦃X Y : AlgebraicSpaces C S hS⦄ (f : X ⟶ Y) => Space.IsFlat C S hS f.hom)
      (quotientStackProjectionHom G)

AlgebraicGeometry.Stack.QuotientAtlas.isLocallyOfFinitePresentation_relativeProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientAtlasArrowSquare.lean, line 242. The attribute's comment: “locally of finite presentation”.

The quotient-stack projection is locally of finite presentation. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over a scheme S of a big fppf site and assume its source and target maps s, t are flat and locally of finite presentation. Then the canonical projection π : S_U ⟶ [U/R] of Stacks 044R is locally of finite presentation in the sense of Stacks 03YK: every algebraic space representing a base change of π along a scheme-valued point of [U/R] has structural morphism locally of finite presentation.

theorem isLocallyOfFinitePresentation_relativeProperty (G : GroupoidInAlgebraicSpaces C S hS B)
    (_hsflat : Space.IsFlat C S hS G.source.hom)
    (_htflat : Space.IsFlat C S hS G.target.hom)
    (hslfp : Space.IsLocallyOfFinitePresentation C S hS G.source.hom)
    (_htlfp : Space.IsLocallyOfFinitePresentation C S hS G.target.hom) :
    RelativeProperty.{u, u + 1, u + 1} C S hS
      (fun ⦃X Y : AlgebraicSpaces C S hS⦄ (f : X ⟶ Y) =>
        Space.IsLocallyOfFinitePresentation C S hS f.hom)
      (quotientStackProjectionHom G)

AlgebraicGeometry.Stack.QuotientAtlas.isSurjective_relativeProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientAtlasArrowSquare.lean, line 259. The attribute's comment: “surjectivity”.

The quotient-stack projection is surjective. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over a scheme S of a big fppf site and assume its source and target maps s, t are flat and locally of finite presentation. Then the canonical projection π : S_U ⟶ [U/R] of Stacks 044R is surjective in the sense of Stacks 03YK: every algebraic space representing a base change of π along a scheme-valued point of [U/R] has surjective structural morphism.

theorem isSurjective_relativeProperty (G : GroupoidInAlgebraicSpaces C S hS B)
    (_hsflat : Space.IsFlat C S hS G.source.hom)
    (_htflat : Space.IsFlat C S hS G.target.hom)
    (_hslfp : Space.IsLocallyOfFinitePresentation C S hS G.source.hom)
    (_htlfp : Space.IsLocallyOfFinitePresentation C S hS G.target.hom) :
    RelativeProperty.{u, u + 1, u + 1} C S hS
      (Space.surjectiveMorphismProperty C S hS)
      (quotientStackProjectionHom G)

AlgebraicGeometry.Stack.QuotientAtlas.isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientAtlasFlat.lean, line 263. The attribute's comment: “flatness; Stacks 04M9 and the representability of the projection carried as the hypothesis Presentation, and only the source map constrained”.

Stacks 06FH, flatness. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over S presented as in Stacks 04M9. If the source map s is flat, then the canonical projection π : S_U ⟶ [U/R] of Stacks 044R is flat in the relative sense of Stacks 03YK.

theorem isFlat {G : GroupoidInAlgebraicSpaces C S hS B} (A : Presentation G)
    (hs : Space.IsFlat C S hS G.source.hom) :
    HasRelativeProperty.{u, u + 1, u + 1, max u t} C S hS
      (fun ⦃X Y : AlgebraicSpaces C S hS⦄ (f : X ⟶ Y) => Space.IsFlat C S hS f.hom)
      (quotientStackProjectionHom G) A.representable

AlgebraicGeometry.Stack.QuotientAtlas.isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientAtlasFlat.lean, line 276. The attribute's comment: “locally of finite presentation; Stacks 04M9 and the representability of the projection carried as the hypothesis Presentation, and only the source map constrained”.

Stacks 06FH, local finite presentation. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over S presented as in Stacks 04M9. If the source map s is locally of finite presentation, then the canonical projection π : S_U ⟶ [U/R] of Stacks 044R is locally of finite presentation in the relative sense of Stacks 03YK.

theorem isLocallyOfFinitePresentation {G : GroupoidInAlgebraicSpaces C S hS B}
    (A : Presentation G) (hs : Space.IsLocallyOfFinitePresentation C S hS G.source.hom) :
    HasRelativeProperty.{u, u + 1, u + 1, max u t} C S hS
      (fun ⦃X Y : AlgebraicSpaces C S hS⦄ (f : X ⟶ Y) =>
        Space.IsLocallyOfFinitePresentation C S hS f.hom)
      (quotientStackProjectionHom G) A.representable

AlgebraicGeometry.Stack.QuotientAtlas.isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientAtlasFlat.lean, line 291. The attribute's comment: “surjectivity; Stacks 04M9 and the representability of the projection carried as the hypothesis Presentation, and no hypothesis on the groupoid”.

Stacks 06FH, surjectivity. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over S presented as in Stacks 04M9. The canonical projection π : S_U ⟶ [U/R] of Stacks 044R is surjective in the relative sense of Stacks 03YK, with no hypothesis on the groupoid: the source map is surjective because the identity arrow at a point of the object space is a preimage of it.

theorem isSurjective {G : GroupoidInAlgebraicSpaces C S hS B} (A : Presentation G) :
    HasRelativeProperty.{u, u + 1, u + 1, max u t} C S hS
      (Space.surjectiveMorphismProperty C S hS)
      (quotientStackProjectionHom G) A.representable

Tag 06FI, a theorem

Tag 06FI in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientStackAlgebraic.lean, line 254. The attribute's comment: “Artin's theorem Stacks 06DC, Stacks 06FH and Stacks 04TB are carried as the hypotheses h06DC, h06FH and h04TB; what is discharged is the representability of the source and of the projection (Stacks 04SV and Stacks 04WZ) and the four stack clauses”.

Stacks 06FI. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over an algebraic space A over a scheme S of a big fppf site. If the source and the target of G are flat and locally of finite presentation, then the quotient stack [U/R] is an algebraic stack over S.

Artin's theorem Stacks 06DC is carried as h06DC, Stacks 06FH as h06FH, and Stacks 04TB as h04TB.

theorem isAlgebraicStack_quotientStack {A : AlgebraicSpaces C S hS}
    (G : GroupoidInAlgebraicSpaces C S hS A)
    (h06DC : Theorem06DC.{u, w} C S hS) (h06FH : Lemma06FH C S hS)
    (h04TB : QuotientStackIsomSheavesAlgebraic C S hS G)
    (hsflat : Space.IsFlat C S hS G.source.hom)
    (htflat : Space.IsFlat C S hS G.target.hom)
    (hslfp : Space.IsLocallyOfFinitePresentation C S hS G.source.hom)
    (htlfp : Space.IsLocallyOfFinitePresentation C S hS G.target.hom) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack G)

AlgebraicGeometry.Stack.forall_isAlgebraicStack_quotientStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientStackAlgebraic.lean, line 282. The attribute's comment: “quantified over the groupoids on a fixed base; Artin's theorem Stacks 06DC, Stacks 06FH and Stacks 04TB are carried as the hypotheses h06DC, h06FH and h04TB”.

Stacks 06FI, quantified over the groupoids on a fixed base. Every groupoid in algebraic spaces over A whose source and target are flat and locally of finite presentation has an algebraic quotient stack.

This is AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack with the three carried hypotheses pulled in front of the quantifier, which is the shape a consumer of Stacks 06FI — for instance Stacks 06PL for the trivial action — takes it in.

theorem forall_isAlgebraicStack_quotientStack (A : AlgebraicSpaces C S hS)
    (h06DC : Theorem06DC.{u, w} C S hS) (h06FH : Lemma06FH C S hS)
    (h04TB : Lemma04TB C S hS) :
    ∀ H : GroupoidInAlgebraicSpaces C S hS A,
      Space.IsFlat C S hS H.source.hom → Space.IsFlat C S hS H.target.hom →
        Space.IsLocallyOfFinitePresentation C S hS H.source.hom →
          Space.IsLocallyOfFinitePresentation C S hS H.target.hom →
            IsAlgebraicStack.{u, w} C S hS (quotientStack H)

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatQuotientStackAlgebraic.lean, line 43. The attribute's comment: “stated for a groupoid in algebraic spaces over an algebraic space over S, which contains the source's groupoid over S”.

Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over an algebraic space A over a scheme S of a big fppf site. If the source and the target of G are flat and locally of finite presentation, then the quotient stack [U/R] is an algebraic stack over S.

The source states it for a groupoid over S; a groupoid over A is the more general statement, S itself being an algebraic space over S.

theorem isAlgebraicStack_quotientStack_of_flat {A : AlgebraicSpaces C S hS}
    (G : GroupoidInAlgebraicSpaces C S hS A)
    (hsflat : Space.IsFlat C S hS G.source.hom)
    (htflat : Space.IsFlat C S hS G.target.hom)
    (hslfp : Space.IsLocallyOfFinitePresentation C S hS G.source.hom)
    (htlfp : Space.IsLocallyOfFinitePresentation C S hS G.target.hom) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack G)

Sources

• Section 97.17, Tag 06FG
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.QuotientAtlas.isFlat_relativeProperty · AlgebraicGeometry.Stack.QuotientAtlas.isLocallyOfFinitePresentation_relativeProperty · AlgebraicGeometry.Stack.QuotientAtlas.isSurjective_relativeProperty · AlgebraicGeometry.Stack.QuotientAtlas.isFlat · AlgebraicGeometry.Stack.QuotientAtlas.isLocallyOfFinitePresentation · AlgebraicGeometry.Stack.QuotientAtlas.isSurjective · AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack · AlgebraicGeometry.Stack.forall_isAlgebraicStack_quotientStack

Section97.18 When is a quotient stack algebraic?#

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

Tag 06PJ, a lemma

Tag 06PJ in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_of_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/GroupoidPresentationQuotientAlgebraic.lean, line 268. The attribute's comment: “the implication from the existence of the restriction to algebraicity, for a groupoid exhibited by hrestriction as the restriction along g, with Stacks 06FI carried as a hypothesis; the converse, which needs Stacks 044X, 044V, 04T4, 046N and 04WY, is not proved”.

Stacks 06PJ, the implication from the existence of a suitable restriction to algebraicity. Let (U, R, s, t, c) be a groupoid in algebraic spaces over B and let f : (U', R', s', t', c') ⟶ (U, R, s, t, c) exhibit its source as the restriction of its target along g = f_U : U' ⟶ U. If the saturation map U' ×_{g, U, t} R ⟶ R ⟶ U is a surjection of fppf sheaves and s', t' are flat and locally of finite presentation, then the quotient stack [U/R] is an algebraic stack.

Stacks 06FI, which is not in the library, is carried as the hypothesis h06FI.

theorem isAlgebraicStack_quotientStack_of_restriction
    (G G' : GroupoidInAlgebraicSpaces C S hS B)
    (f : GroupoidInAlgebraicSpaces.Hom G' G)
    (h06FI : ∀ H : GroupoidInAlgebraicSpaces C S hS B,
      Space.IsFlat C S hS H.source.hom → Space.IsFlat C S hS H.target.hom →
        Space.IsLocallyOfFinitePresentation C S hS H.source.hom →
          Space.IsLocallyOfFinitePresentation C S hS H.target.hom →
            IsAlgebraicStack.{u, w} C S hS (quotientStack H))
    (hrestriction : IsPullback f.toGroupoidHom.mapArrows
      (prod.lift G'.toGroupoidInFunctors.source G'.toGroupoidInFunctors.target)
      (prod.lift G.toGroupoidInFunctors.source G.toGroupoidInFunctors.target)
      (prod.map f.toGroupoidHom.mapObjects f.toGroupoidHom.mapObjects))
    (hsaturation : Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS)
      ((GroupoidInAlgebraicSpaces.fiberProductSnd
        (ObjectProperty.homMk f.toGroupoidHom.mapObjects : G'.objects ⟶ G.objects)
        G.target ≫ G.source).hom))
    (hsource : Space.IsFlat C S hS G'.source.hom)
    (htarget : Space.IsFlat C S hS G'.target.hom)
    (hsourceFP : Space.IsLocallyOfFinitePresentation C S hS G'.source.hom)
    (htargetFP : Space.IsLocallyOfFinitePresentation C S hS G'.target.hom) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack G)

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_of_restrictionAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/GroupoidPresentationQuotientAlgebraic.lean, line 307. The attribute's comment: “the implication from the existence of the restriction to algebraicity, for the canonical restriction of Stacks 044B along g, with Stacks 06FI carried as a hypothesis; the converse, which needs Stacks 044X, 044V, 04T4, 046N and 04WY, is not proved”.

Stacks 06PJ, the implication from the existence of the restriction to algebraicity, in the form the source states it. Let (U, R, s, t, c) be a groupoid in algebraic spaces over B and let g : U' ⟶ U be a morphism of algebraic spaces such that the saturation map U' ×_{g, U, t} R ⟶ R ⟶ U is a surjection of fppf sheaves and the source and target of the restriction (U', R', s', t', c') of (U, R, s, t, c) along g are flat and locally of finite presentation. Then the quotient stack [U/R] is an algebraic stack.

Stacks 06FI, which is not in the library, is carried as the hypothesis h06FI.

theorem isAlgebraicStack_quotientStack_of_restrictionAlong
    (G : GroupoidInAlgebraicSpaces C S hS B)
    {U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects)
    (h06FI : ∀ H : GroupoidInAlgebraicSpaces C S hS B,
      Space.IsFlat C S hS H.source.hom → Space.IsFlat C S hS H.target.hom →
        Space.IsLocallyOfFinitePresentation C S hS H.source.hom →
          Space.IsLocallyOfFinitePresentation C S hS H.target.hom →
            IsAlgebraicStack.{u, w} C S hS (quotientStack H))
    (hsaturation : Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS)
      ((GroupoidInAlgebraicSpaces.fiberProductSnd g G.target ≫ G.source).hom))
    (hsource : Space.IsFlat C S hS
      (GroupoidInAlgebraicSpaces.restrictionSource G g).hom)
    (htarget : Space.IsFlat C S hS
      (GroupoidInAlgebraicSpaces.restrictionTarget G g).hom)
    (hsourceFP : Space.IsLocallyOfFinitePresentation C S hS
      (GroupoidInAlgebraicSpaces.restrictionSource G g).hom)
    (htargetFP : Space.IsLocallyOfFinitePresentation C S hS
      (GroupoidInAlgebraicSpaces.restrictionTarget G g).hom) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack G)

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_iff_restrictionAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/QuotientStackAlgebraicIffRestriction.lean, line 289.

Let (U, R, s, t, c) be a groupoid in algebraic spaces over B. The quotient stack [U/R] is an algebraic stack if and only if there is a morphism g : U' ⟶ U of algebraic spaces over S such that

1. the saturation map U' ×_{g, U, t} R ⟶ R ⟶ U is a surjection of fppf sheaves, and
2. the source and target of the restriction of (U, R, s, t, c) along g are flat and locally of finite presentation.

theorem isAlgebraicStack_quotientStack_iff_restrictionAlong
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack G) ↔
      ∃ (U' : AlgebraicSpaces C S hS) (g : U' ⟶ G.objects),
        Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS)
          ((GroupoidInAlgebraicSpaces.fiberProductSnd g G.target ≫ G.source).hom) ∧
        Space.IsFlat C S hS (GroupoidInAlgebraicSpaces.restrictionSource G g).hom ∧
        Space.IsFlat C S hS (GroupoidInAlgebraicSpaces.restrictionTarget G g).hom ∧
        Space.IsLocallyOfFinitePresentation C S hS
          (GroupoidInAlgebraicSpaces.restrictionSource G g).hom ∧
        Space.IsLocallyOfFinitePresentation C S hS
          (GroupoidInAlgebraicSpaces.restrictionTarget G g).hom

Tag 06PK, a lemma

Tag 06PK in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_action_iff_exists_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/ActionQuotientStackAlgebraicIff.lean, line 67. The attribute's comment: “for any action groupoid construction of Stacks 0444”.

Stacks 06PK. Let a group algebraic space G over an algebraic space B act on an algebraic space X over B. The quotient stack [X/G] of the action groupoid of Stacks 0444 is an algebraic stack exactly when there is a morphism φ : X' ⟶ X of algebraic spaces over B for which

1. G ×_B X' ⟶ X, (g, x') ↦ g • φ x', is a surjection of fppf sheaves, and
2. both projections to X' of the space of triples {(x₁, g, x₂) : φ x₁ = g • φ x₂}, the fibre product X' ×_{φ, X, a} (G ×_B X'), are flat and locally of finite presentation.

This is AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_action_iff with the biconditional of Stacks 06PJ it takes supplied by AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_iff_restrictionAlong.

theorem isAlgebraicStack_quotientStack_action_iff_exists_cover
    (C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
    (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)
    (A : Space.ActionGroupoidConstruction B G X hG hX) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack A.groupoid) ↔
      ∃ (X' : Over B.obj) (_ : IsAlgebraicSpace C S hS X'.left) (φ : X' ⟶ X),
        let a : G ⊗ X' ⟶ X := (𝟙 G ⊗ₘ φ) ≫ γ[G, X]
        Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS) a.left ∧
        Space.IsFlat C S hS (pullback.fst φ.left a.left) ∧
        Space.IsLocallyOfFinitePresentation C S hS (pullback.fst φ.left a.left) ∧
        Space.IsFlat C S hS (pullback.snd φ.left a.left ≫ (snd G X').left) ∧
        Space.IsLocallyOfFinitePresentation C S hS
          (pullback.snd φ.left a.left ≫ (snd G X').left)

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_groupoidOfAction_iff_exists_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/ActionQuotientStackAlgebraicIff.lean, line 95. The attribute's comment: “for the action groupoid of Stacks 0444 that the library builds”.

Stacks 06PK for the action groupoid of Stacks 0444 that the library builds. The quotient stack [X/G] is an algebraic stack exactly when there is a morphism φ : X' ⟶ X of algebraic spaces over B for which G ×_B X' ⟶ X, (g, x') ↦ g • φ x', is a surjection of fppf sheaves and both projections to X' of the space of triples {(x₁, g, x₂) : φ x₁ = g • φ x₂} are flat and locally of finite presentation.

This is AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_groupoidOfAction_iff with the biconditional of Stacks 06PJ it takes supplied as in AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_action_iff_exists_cover.

theorem isAlgebraicStack_quotientStack_groupoidOfAction_iff_exists_cover
    (C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
    (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) :
    IsAlgebraicStack.{u, w} C S hS
        (quotientStack (Space.groupoidOfAction B G X hG hX).groupoid) ↔
      ∃ (X' : Over B.obj) (_ : IsAlgebraicSpace C S hS X'.left) (φ : X' ⟶ X),
        let a : G ⊗ X' ⟶ X := (𝟙 G ⊗ₘ φ) ≫ γ[G, X]
        Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS) a.left ∧
        Space.IsFlat C S hS (pullback.fst φ.left a.left) ∧
        Space.IsLocallyOfFinitePresentation C S hS (pullback.fst φ.left a.left) ∧
        Space.IsFlat C S hS (pullback.snd φ.left a.left ≫ (snd G X').left) ∧
        Space.IsLocallyOfFinitePresentation C S hS
          (pullback.snd φ.left a.left ≫ (snd G X').left)

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_action_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/GerbeGroupDescent.lean, line 874. The attribute's comment: “with Stacks 06PJ, the same criterion for an arbitrary groupoid in algebraic spaces, carried as the explicit hypothesis h06PJ”.

Stacks 06PK. Let a group algebraic space G over an algebraic space B act on an algebraic space X over B. The quotient stack [X/G] of the action groupoid is an algebraic stack exactly when there is a morphism φ : X' ⟶ X of algebraic spaces over B for which G ×_B X' ⟶ X, (g, x') ↦ g • φ x', is a surjection of fppf sheaves and both projections to X' of the space of triples {(x₁, g, x₂) : φ x₁ = g • φ x₂} are flat and locally of finite presentation.

Stacks 06PJ, the same criterion for an arbitrary groupoid in algebraic spaces, is not in the library and is carried as the hypothesis h06PJ.

theorem isAlgebraicStack_quotientStack_action_iff
    (C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
    (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)
    (A : Space.ActionGroupoidConstruction B G X hG hX)
    (h06PJ : ∀ H : GroupoidInAlgebraicSpaces C S hS B,
      IsAlgebraicStack.{u, w} C S hS (quotientStack H) ↔
        ∃ (U' : AlgebraicSpaces C S hS) (g : U' ⟶ H.objects),
          Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS)
            ((GroupoidInAlgebraicSpaces.fiberProductSnd g H.target ≫ H.source).hom) ∧
          Space.IsFlat C S hS
            (GroupoidInAlgebraicSpaces.restrictionSource H g).hom ∧
          Space.IsFlat C S hS
            (GroupoidInAlgebraicSpaces.restrictionTarget H g).hom ∧
          Space.IsLocallyOfFinitePresentation C S hS
            (GroupoidInAlgebraicSpaces.restrictionSource H g).hom ∧
          Space.IsLocallyOfFinitePresentation C S hS
            (GroupoidInAlgebraicSpaces.restrictionTarget H g).hom) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack A.groupoid) ↔
      ∃ (X' : Over B.obj) (_ : IsAlgebraicSpace C S hS X'.left) (φ : X' ⟶ X),
        let a : G ⊗ X' ⟶ X := (𝟙 G ⊗ₘ φ) ≫ γ[G, X]
        Presheaf.IsLocallySurjective (BigFppfOver.topology C S hS) a.left ∧
        Space.IsFlat C S hS (pullback.fst φ.left a.left) ∧
        Space.IsLocallyOfFinitePresentation C S hS (pullback.fst φ.left a.left) ∧
        Space.IsFlat C S hS (pullback.snd φ.left a.left ≫ (snd G X').left) ∧
        Space.IsLocallyOfFinitePresentation C S hS
          (pullback.snd φ.left a.left ≫ (snd G X').left)

Tag 06PL, a lemma

Tag 06PL in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_trivialAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/TrivialActionAlgebraic.lean, line 128. The attribute's comment: “the implication from flat and locally of finite presentation to algebraic, with Stacks 06FI carried as a hypothesis; the converse, which rests on Stacks 06PK, is not proved”.

Stacks 06PL, the implication from flatness and local finite presentation to algebraicity. Let G be a group algebraic space over an algebraic space B over S and endow B with the trivial action of G. If G is flat and locally of finite presentation over B, then the quotient stack [B/G] is an algebraic stack.

Stacks 06FI, which is not in the library, is carried as the hypothesis h06FI.

theorem isAlgebraicStack_quotientStack_trivialAction
    (B : AlgebraicSpaces C S hS) (G : Over B.obj) [GrpObj G]
    (hG : IsAlgebraicSpace C S hS G.left)
    (A : Space.ActionGroupoidConstruction B G (𝟙_ (Over B.obj)) hG B.property)
    (h06FI : ∀ H : GroupoidInAlgebraicSpaces C S hS B,
      Space.IsFlat C S hS H.source.hom → Space.IsFlat C S hS H.target.hom →
        Space.IsLocallyOfFinitePresentation C S hS H.source.hom →
          Space.IsLocallyOfFinitePresentation C S hS H.target.hom →
            IsAlgebraicStack.{u, w} C S hS (quotientStack H))
    (hflat : Space.IsFlat C S hS G.hom)
    (hlfp : Space.IsLocallyOfFinitePresentation C S hS G.hom) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack A.groupoid)

AlgebraicGeometry.Stack.isFlat_and_isLocallyOfFinitePresentation_of_isAlgebraicStack_trivialAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/TrivialActionAlgebraicIff.lean, line 153. The attribute's comment: “the converse implication, from algebraicity to flat and locally of finite presentation, with nothing carried”.

Stacks 06PL, the converse implication. Let G be a group algebraic space over an algebraic space B over S, endow B with the trivial action of G, and suppose the quotient stack [B/G] is an algebraic stack. Then G ⟶ B is flat and locally of finite presentation.

The converse of Stacks 06PJ, AlgebraicGeometry.Stack.exists_restrictionAlong_of_isAlgebraicStack, supplies the citation of Stacks 06PK that the source's proof makes, and AlgebraicGeometry.Stack.isFlat_and_isLocallyOfFinitePresentation_of_trivialActionCriterion is the rest of the argument; see the module docstring.

theorem isFlat_and_isLocallyOfFinitePresentation_of_isAlgebraicStack_trivialAction
    (B : AlgebraicSpaces C S hS) (G : Over B.obj) [GrpObj G]
    (hG : IsAlgebraicSpace C S hS G.left)
    (A : Space.ActionGroupoidConstruction B G (𝟙_ (Over B.obj)) hG B.property)
    (h : IsAlgebraicStack.{u, w} C S hS (quotientStack A.groupoid)) :
    Space.IsFlat C S hS G.hom ∧ Space.IsLocallyOfFinitePresentation C S hS G.hom

AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_trivialAction_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/TrivialActionAlgebraicIff.lean, line 217.

Stacks 06PL. Let G be a group algebraic space over an algebraic space B over S and endow B with the trivial action of G. The quotient stack [B/G] is an algebraic stack if and only if G ⟶ B is flat and locally of finite presentation.

theorem isAlgebraicStack_quotientStack_trivialAction_iff
    (B : AlgebraicSpaces C S hS) (G : Over B.obj) [GrpObj G]
    (hG : IsAlgebraicSpace C S hS G.left)
    (A : Space.ActionGroupoidConstruction B G (𝟙_ (Over B.obj)) hG B.property) :
    IsAlgebraicStack.{u, w} C S hS (quotientStack A.groupoid) ↔
      (Space.IsFlat C S hS G.hom ∧
        Space.IsLocallyOfFinitePresentation C S hS G.hom)

Sources

• Section 97.18, Tag 06PI
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_of_restriction · AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_of_restrictionAlong · AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_iff_restrictionAlong · AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_action_iff_exists_cover · AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_groupoidOfAction_iff_exists_cover · AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_action_iff · AlgebraicGeometry.Stack.isAlgebraicStack_quotientStack_trivialAction · AlgebraicGeometry.Stack.isFlat_and_isLocallyOfFinitePresentation_of_isAlgebraicStack_trivialAction

Section97.19 Algebraic stacks in the étale topology#

Section 97.19 of the Stacks Project, Tag 076U. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 076V, a lemma

Tag 076V in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_of_isStackInGroupoids_etale_of_smoothAtlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleStackCriterion.lean, line 456. The attribute's comment: “the criterion, with hypotheses (2) and (3) in the topology-independent form of the corresponding clauses of Stacks 026O”.

Stacks 076V. Let S be a scheme of a big fppf site and let 𝒳 be a category over the common underlying category of the big fppf and big étale sites of S such that

1. 𝒳 is a stack in groupoids for the étale topology,
2. the diagonal Δ : 𝒳 ⟶ 𝒳 × 𝒳 is representable by algebraic spaces, and
3. there are a scheme U over S and a 1-morphism (Sch/U) ⟶ 𝒳 which is representable by algebraic spaces, surjective and smooth.

Then 𝒳 is an algebraic stack over S in the sense of Stacks 026O.

Conditions (2) and (3) are stated exactly as the corresponding clauses of AlgebraicGeometry.Stack.IsAlgebraicStack, which, as the source's proof notes, are independent of the topology; condition (1) is Stacks 02ZI for the étale topology localised at S, at the index universe of the families of the site. The fppf stack clause is AlgebraicGeometry.Stack.isStack_of_isStack_etale_of_smoothAtlas.

theorem isAlgebraicStack_of_isStackInGroupoids_etale_of_smoothAtlas
    (𝒳 : BasedCategory.{u, u + 1} (BigFppfOver B S hS))
    (hstack : 𝒳.p.IsStackInGroupoids.{u + 1} ((etaleTopology B).over (B.obj hS)))
    (hdiag : IsRepresentableByAlgebraicSpaces B S hS
      (diagonalBasedFunctor B S hS (CatFiberedInGroupoids.mk 𝒳 hstack.isFiberedInGroupoids)))
    (U : BigFppfOver B S hS)
    (f : (schemeFibredCategory B S hS U).val ⥤ᵇ 𝒳)
    (hfrep : IsRepresentableByAlgebraicSpaces B S hS f)
    (hfprop : ∀ (V : BigFppfOver B S hS)
        (y : BigFppfOver B V.left.1 V.left.2 ⥤ 𝒳.obj)
        (_hy : y ⋙ 𝒳.p = Over.map V.hom)
        (F : (BigFppfOver B V.left.1 V.left.2)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B V.left.1 V.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map V.hom)
            (schemeFibredCategory B S hS U).val.p 𝒳.p y f.toFunctor)
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        (let g := (algebraicSpaceMap B S hS V
          ((spacesOverSmallerBaseFunctor B V.left.1 S V.left.2 hS V.hom).obj ⟨F, hF⟩)).hom
         Space.IsSurjective B S hS g ∧ Space.IsSmooth B S hS g)) :
    IsAlgebraicStack.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.isAlgebraicStack_of_isStackInGroupoids_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothGroupoidPresentation.lean, line 211. The attribute's comment: “the criterion, with hypotheses (2) and (3) in the topology-independent form of the corresponding clauses of Stacks 026O. Carried as explicit hypotheses are part (1) of Stacks 04T4 (_eR: the self-intersection of the atlas is representable by the arrow space of the carried groupoid), part (4) of Stacks 04T4 (_hobjects: its object space is the space the atlas represents) and part (6) of Stacks 04T4 together with part (2) of Stacks 04T5 read at the étale index (e: the quotient stack of the carried groupoid is equivalent over the site to 𝒳); the carried groupoid is not assumed smooth, so none of the three contains algebraicity of 𝒳. What is discharged is the fppf stack clause, by Stacks 044Q for the quotient stack of a groupoid in algebraic spaces, Stacks 042W to transport it along the equivalence and Stacks 02ZJ for the family-indexed conjunct, together with clause (1) of Stacks 026O out of the étale hypothesis”.

Stacks 076V. Let 𝒳 be a category over the common underlying category of the big fppf and big étale sites of S such that

1. 𝒳 is a stack in groupoids for the étale topology,
2. the diagonal Δ : 𝒳 ⟶ 𝒳 × 𝒳 is representable by algebraic spaces, and
3. there are a scheme U over S and a 1-morphism (Sch/U) ⟶ 𝒳 which is representable by algebraic spaces, surjective and smooth.

Then 𝒳 is an algebraic stack over S in the sense of Stacks 026O.

Conditions (2) and (3) are stated exactly as the corresponding clauses of AlgebraicGeometry.Stack.IsAlgebraicStack, which is legitimate because, as the source's proof notes, both are independent of the topology. Three hypotheses carry the chain Stacks 04T4 (1), (4), (6) and Stacks 04T5 (2) that the source's proof goes through; see the implementation notes for why none of them is the conclusion restated.

theorem isAlgebraicStack_of_isStackInGroupoids_etale
    (𝒳 : BasedCategory.{u, u + 1} (BigFppfOver B S hS))
    (hstack : 𝒳.p.IsStackInGroupoids.{w} ((etaleTopology B).over (B.obj hS)))
    (hdiag : IsRepresentableByAlgebraicSpaces B S hS
      (diagonalBasedFunctor B S hS (CatFiberedInGroupoids.mk 𝒳 hstack.isFiberedInGroupoids)))
    (U : BigFppfOver B S hS)
    (f : (schemeFibredCategory B S hS U).val ⥤ᵇ 𝒳)
    (hfrep : IsRepresentableByAlgebraicSpaces B S hS f)
    (hfprop : ∀ (V : BigFppfOver B S hS)
        (y : BigFppfOver B V.left.1 V.left.2 ⥤ 𝒳.obj)
        (_hy : y ⋙ 𝒳.p = Over.map V.hom)
        (F : (BigFppfOver B V.left.1 V.left.2)ᵒᵖ ⥤ Type u)
        (hF : IsAlgebraicSpace B V.left.1 V.left.2 F),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map V.hom)
            (schemeFibredCategory B S hS U).val.p 𝒳.p y f.toFunctor)
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        (let g := (algebraicSpaceMap B S hS V
          ((spacesOverSmallerBaseFunctor B V.left.1 S V.left.2 hS V.hom).obj ⟨F, hF⟩)).hom
         Space.IsSurjective B S hS g ∧ Space.IsSmooth B S hS g))
    {A : AlgebraicSpaces B S hS} (G : GroupoidInAlgebraicSpaces B S hS A)
    (_eR : StacksRepresentableCFG.EquivalenceOver
      (SelfIntersection.relation B S hS (schemeFibredCategory B S hS U)
        (CatFiberedInGroupoids.mk 𝒳 hstack.isFiberedInGroupoids) f).val.p
      (presheafOfCategories (G.arrows.obj ⋙ typeToCat)).p)
    (_hobjects : G.objects = Space.representedAlgebraicSpace B S hS U)
    (e : BasedCategory.Equivalence (quotientStack G) 𝒳) :
    IsAlgebraicStack.{u, w} B S hS 𝒳

Sources

• Section 97.19, Tag 076U
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isAlgebraicStack_of_isStackInGroupoids_etale_of_smoothAtlas · AlgebraicGeometry.Stack.isAlgebraicStack_of_isStackInGroupoids_etale

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.