106.3 Thickenings to 106.15 Stacks and fpqc coverings

Section106.3 Thickenings#

Section 106.3 of the Stacks Project, Tag 0BPN. 9 tags here are carried by 55 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BPP, a definition

Tag 0BPP in the Stacks Project.

AlgebraicGeometry.Stack.IsThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Thickening.lean, line 82. The attribute's comment: “part (1): thickening”.

Stacks 0BPP, part (1). A 1-morphism of algebraic stacks over S is a thickening when it is a closed immersion, in the sense of Stacks 04YL part (2), and is surjective on the underlying sets of points.

The source's part (1) also asserts that the induced map of underlying topological spaces is a homeomorphism; that clause needs the point topology of Stacks 04XL, which has no library site, so it is not stated here.

abbrev IsThickening {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (i : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.ThickeningMorphism, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Thickening.lean, line 92. The attribute's comment: “part (2): morphisms of thickenings”.

Stacks 0BPP, part (2). A morphism of thickenings from the thickening i to the thickening j of algebraic stacks over S: a 1-morphism of the ambient stacks, a 1-morphism of the closed substacks, and a 2-isomorphism saying that the former restricts to the latter.

structure ThickeningMorphism {𝒳 𝒳' 𝒴 𝒴' : AlgebraicStacks.{u, w} B S hS}
    (i : 𝒳 ⟶ 𝒳') (j : 𝒴 ⟶ 𝒴') (_hi : IsThickening i) (_hj : IsThickening j)

AlgebraicGeometry.Stack.ThickeningOver, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Thickening.lean, line 105. The attribute's comment: “part (3): thickenings over a stack”.

Stacks 0BPP, part (3). A thickening of algebraic stacks over S together with a 1-morphism from its ambient stack to a fixed algebraic stack 𝒵.

structure ThickeningOver (𝒵 : AlgebraicStacks.{u, w} B S hS)

AlgebraicGeometry.Stack.ThickeningMorphismOver, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Thickening.lean, line 121. The attribute's comment: “part (3): morphisms over a stack”.

Stacks 0BPP, part (3). A morphism of thickenings of algebraic stacks over a fixed algebraic stack 𝒵: a morphism of the underlying thickenings whose ambient component lies over the base up to 2-isomorphism.

structure ThickeningMorphismOver {𝒵 : AlgebraicStacks.{u, w} B S hS}
    (𝒳 𝒴 : ThickeningOver.{u, w} 𝒵)

Tag 0CJ7, a lemma

Tag 0CJ7 in the Stacks Project.

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

A 1-morphism of algebraic stacks over S is a thickening in the sense of Stacks 0BPP part (1) if and only if it is representable by algebraic spaces and is a thickening in the relative sense of §04XB, that is a closed immersion all of whose algebraic-space base changes are surjective.

The closed-immersion clause is the same on both sides; the surjectivity clause is surjectivity on the points of Stacks 04XG on the left and the relative property of Stacks 03YK on the right, and the two agree by Stacks 04XI.

theorem isThickening_iff_isRelativeThickening (i : 𝒳 ⟶ 𝒳') :
    IsThickening i ↔ IsRelativeThickening B S hS i.hom

AlgebraicGeometry.Stack.isClosedImmersion_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningUniversalHomeomorphism.lean, line 110. The attribute's comment: “closed immersion”.

A thickening of algebraic stacks over S is a closed immersion in the sense of Stacks 04YL part (2).

In this library that is a clause of the definition of a thickening: Stacks 0BPP part (1) realises the source as a closed substack of the target, and AlgebraicGeometry.Stack.IsThickening records that closed immersion rather than recovering it from a looser condition.

theorem isClosedImmersion_of_isThickening (hi : IsThickening i) :
    AlgebraicStacks.IsClosedImmersion B S hS i

AlgebraicGeometry.Stack.universalHomeomorphism_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningUniversalHomeomorphism.lean, line 146. The attribute's comment: “universal homeomorphism”.

A thickening of algebraic stacks over S is a universal homeomorphism in the sense of Stacks 0CI7: every base change of it induces a homeomorphism on the topological spaces of points of Stacks 04XG and 04XL.

A base change of a thickening is a thickening (Stacks 0BPR, AlgebraicGeometry.Stack.isThickening_fst_of_isTwoFibreProduct), and a thickening is a homeomorphism on points by AlgebraicGeometry.Stack.isHomeomorphOnPoints_of_isThickening. The statement is at the model-independent AlgebraicGeometry.Stack.UniversalHomeomorphism, so it tests every 2-fibre product square of the cospan and not only the canonical one.

theorem universalHomeomorphism_of_isThickening (hi : IsThickening i) :
    UniversalHomeomorphism B S hS i

Tag 0BPQ, a definition

Tag 0BPQ in the Stacks Project.

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

Stacks 0BPQ. A closed immersion i : 𝒳 ⟶ 𝒳' of algebraic stacks over S exhibits 𝒳' as a first-order thickening of 𝒳 when, for every scheme-valued point U ⟶ 𝒳' and every algebraic space F representing the base change of i along it, the image of the structural morphism of F is a first-order thickening of the representable algebraic space of U in the sense of Stacks 05ZK, part (2) — that is, the ideal cutting it out is square-zero on every object of the small étale site.

abbrev IsFirstOrderThickening (i : 𝒳 ⟶ 𝒳') : Prop

Tag 0BPR, a lemma

Tag 0BPR in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isFirstOrderThickening_fst_of_isTwoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FirstOrderThickeningBaseChange.lean, line 55. The attribute's comment: “first order thickening base-changes to a first order thickening”.

If 𝒴 ⊂ 𝒴' is a first-order thickening of algebraic stacks over S and 𝒳 = 𝒴 ×_{𝒴'} 𝒳' for a 1-morphism g : 𝒳' ⟶ 𝒴', then 𝒳 ⊂ 𝒳' — the projection P.fst — is a first-order thickening.

theorem isFirstOrderThickening_fst_of_isTwoFibreProduct
    {𝒴 𝒴' 𝒳' : Stack.AlgebraicStacks.{u, w} B S hS} {j : 𝒴 ⟶ 𝒴'} {g : 𝒳' ⟶ 𝒴'}
    (hj : IsFirstOrderThickening B S hS j)
    (P : Bicategory.TwoCommSq g j) (hP : Bicategory.IsTwoFibreProduct P) :
    IsFirstOrderThickening B S hS P.fst

AlgebraicGeometry.Stack.isThickening_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningBaseChange.lean, line 275. The attribute's comment: “base-changed thickening”.

Stacks 0BPR. Let i : 𝒴 ⟶ 𝒴' be a thickening of algebraic stacks over S, let f : 𝒳' ⟶ 𝒴' be a 1-morphism of algebraic stacks, and let P be a 2-fibre product of that cospan in the 2-category of algebraic stacks. Then the second projection P.snd : 𝒴 ×_{𝒴'} 𝒳' ⟶ 𝒳' is a thickening.

A thickening is a closed immersion which is surjective on points, and each of its three constituents base-changes: representability by algebraic spaces by Stacks 0302, the closed-immersion property of Stacks 04XB by Stacks 045C, and surjectivity on points by Stacks 04ZU.

theorem isThickening_baseChange (i : 𝒴 ⟶ 𝒴') (f : 𝒳' ⟶ 𝒴')
    (P : Bicategory.TwoCommSq i f) (hP : Bicategory.IsTwoFibreProduct P)
    (hi : IsThickening i) :
    IsThickening P.snd

AlgebraicGeometry.Stack.baseChangeThickeningMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningBaseChange.lean, line 289. The attribute's comment: “morphism of thickenings”.

Stacks 0BPR. A 2-fibre product square of a thickening i : 𝒴 ⟶ 𝒴' of algebraic stacks along a 1-morphism f : 𝒳' ⟶ 𝒴' is a morphism of thickenings from the base-changed thickening P.snd to i: its ambient 1-morphism is f, its restricted 1-morphism is the first projection P.fst, and the 2-isomorphism filling the square is exactly the assertion that f restricts to P.fst.

def baseChangeThickeningMorphism (i : 𝒴 ⟶ 𝒴') (f : 𝒳' ⟶ 𝒴')
    (P : Bicategory.TwoCommSq i f) (hP : Bicategory.IsTwoFibreProduct P)
    (hi : IsThickening i) :
    ThickeningMorphism P.snd i (isThickening_baseChange B S hS i f P hP hi) hi

Tag 0BPS, a lemma

Tag 0BPS in the Stacks Project.

AlgebraicGeometry.Stack.isThickening_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningComposition.lean, line 75. The attribute's comment: “the composite of two thickenings is a thickening”.

Stacks 0BPS. A composite of thickenings of algebraic stacks over S is a thickening: the composite is a closed immersion by Stacks 0502, and it is surjective on points because each factor is.

theorem isThickening_comp
    {𝒳 𝒴 𝒵 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hf : IsThickening f) (hg : IsThickening g) :
    IsThickening (f ≫ g)

Tag 0BPT, an example

Tag 0BPT in the Stacks Project.

AlgebraicGeometry.Stack.isThickening_stackReductionInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningReduction.lean, line 148. The attribute's comment: “assertion (1): an algebraic stack is a thickening of its reduction”.

Stacks 0BPT, assertion (1). An algebraic stack over S is a thickening of its reduction: the inclusion of the reduction is a closed immersion and is surjective on points, which are the two clauses of AlgebraicGeometry.Stack.IsThickening (Stacks 0BPP, part (1)).

Surjectivity on points is the clause of Definition 050C that the set of points of the reduction is all of |𝒳|.

theorem isThickening_stackReductionInclusion (R : StackReduction B S hS 𝒳) :
    IsThickening R.inclusion

AlgebraicGeometry.Stack.isClosedSubstack_stackReductionEssImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningReduction.lean, line 180. The attribute's comment: “assertion (1), substack form: the reduction is a closed substack with every point”.

Stacks 0BPT, assertion (1), substack form. The reduction of an algebraic stack 𝒳 over S is realised as a closed substack of 𝒳 carrying every point of 𝒳, which is what it means for 𝒳 to be a thickening of it in the substack language of Stacks 04YM, part (2).

The substack is the essential image of the inclusion of the reduction, a closed substack by Stacks 0506.

theorem isClosedSubstack_stackReductionEssImage (R : StackReduction B S hS 𝒳) :
    ∃ hP : IsAlgebraicStack.{u, w} B S hS
        (fullSubcategoryBased 𝒳
          (CatFiberedInGroupoids.homFunctor R.inclusion.hom).essImage),
      AlgebraicStacks.IsClosedImmersion B S hS
          (fullSubcategoryInclusion 𝒳
            (CatFiberedInGroupoids.homFunctor R.inclusion.hom).essImage hP) ∧
        IsSurjective B S hS
          (fullSubcategoryInclusion 𝒳
            (CatFiberedInGroupoids.homFunctor R.inclusion.hom).essImage hP)

AlgebraicGeometry.Stack.stackReductionOfThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningReduction.lean, line 203. The attribute's comment: “assertion (2): a thickening has the same reduction as its ambient stack”.

Stacks 0BPT, assertion (2). Let 𝒳 ⊆ 𝒳' be a thickening of algebraic stacks over S. Then the reduction of 𝒳 is a reduction of 𝒳', included through 𝒳: this is the source's 𝒳'_red = 𝒳_red ⊆ 𝒳.

The inclusion is the composite of the inclusion of the reduction of 𝒳 with the given thickening, which is again a thickening by Stacks 0BPS, and the source stack is untouched, so it is still reduced.

def stackReductionOfThickening
    [(Space.closedImmersionProperty B S hS).IsLocalAtTarget
      (Space.Topology.fppf.precoverage.{u, u} B S hS)]
    (R : StackReduction B S hS 𝒳) (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    StackReduction B S hS 𝒳'

AlgebraicGeometry.Stack.isReducedStack_iff_essImage_stackReduction_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningReduction.lean, line 279. The attribute's comment: “assertion (3): the reduction is the whole stack exactly when the stack is reduced”.

Stacks 0BPT, assertion (3). Let R present the reduction of an algebraic stack 𝒳 over S. Then the closed substack of 𝒳 cut out by that reduction is all of 𝒳 exactly when 𝒳 is a reduced algebraic stack.

Read through assertion (2) this is the source's assertion (3): for a thickening 𝒳 ⊆ 𝒳' the reduction of 𝒳' is the reduction of 𝒳, so 𝒳 = 𝒳'_red says precisely that the reduction of 𝒳 is all of 𝒳.

One direction is Stacks 050A at the closed substack cut out by the essential image of the inclusion of the reduction, which carries every point of 𝒳. For the other, a reduction whose substack is all of 𝒳 has fully faithful and essentially surjective inclusion, so reducedness transports from the reduction to 𝒳.

theorem isReducedStack_iff_essImage_stackReduction_eq_top (R : StackReduction B S hS 𝒳) :
    (CatFiberedInGroupoids.homFunctor R.inclusion.hom).essImage = ⊤ ↔
      IsReducedStack B S hS 𝒳

AlgebraicGeometry.Stack.isThickening_stackReduction_inclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningReductionCanonical.lean, line 77. The attribute's comment: “assertion (1): an algebraic stack is a thickening of its reduction”.

Stacks 0BPT, assertion (1). An algebraic stack 𝒳' over S is a thickening of its reduction 𝒳'_red (Stacks 050C): the inclusion of the reduction is a closed immersion which is surjective on points, the two clauses of AlgebraicGeometry.Stack.IsThickening (Stacks 0BPP).

theorem isThickening_stackReduction_inclusion (𝒳' : AlgebraicStacks.{u, w} B S hS) :
    IsThickening (stackReduction 𝒳').inclusion

AlgebraicGeometry.Stack.essImage_stackReduction_eq_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningReductionCanonical.lean, line 114. The attribute's comment: “assertion (2): a thickening has the same reduction as its ambient stack”.

Stacks 0BPT, assertion (2). Let i : 𝒳 ⟶ 𝒳' be a thickening of algebraic stacks over S. Then 𝒳'_red = 𝒳_red ⊆ 𝒳: the reduction of 𝒳' is the substack of 𝒳' cut out by the reduction of 𝒳 included through i, and it lies in the substack cut out by 𝒳.

The composite of the inclusion of 𝒳_red with i is again a thickening by Stacks 0BPS and has reduced source, so its essential image is a reduction of 𝒳' in the sense of AlgebraicGeometry.Stack.IsReduction; so is that of the inclusion of 𝒳'_red, and the two agree by uniqueness of the reduction (Stacks 0509).

theorem essImage_stackReduction_eq_of_isThickening {𝒳 𝒳' : AlgebraicStacks.{u, w} B S hS}
    (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    (CatFiberedInGroupoids.homFunctor (stackReduction 𝒳').inclusion.hom).essImage =
        (CatFiberedInGroupoids.homFunctor ((stackReduction 𝒳).inclusion ≫ i).hom).essImage ∧
      (CatFiberedInGroupoids.homFunctor (stackReduction 𝒳').inclusion.hom).essImage ≤
        (CatFiberedInGroupoids.homFunctor i.hom).essImage

AlgebraicGeometry.Stack.essImage_stackReduction_eq_essImage_iff_isReducedStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningReductionCanonical.lean, line 138. The attribute's comment: “assertion (3): a thickening is the reduction of its ambient stack exactly when it is reduced”.

Stacks 0BPT, assertion (3). Let i : 𝒳 ⟶ 𝒳' be a thickening of algebraic stacks over S. Then 𝒳 = 𝒳'_red — the reduction of 𝒳' and 𝒳 cut out the same substack of 𝒳' — exactly when 𝒳 is a reduced algebraic stack.

By assertion (2) the reduction of 𝒳' is the substack cut out by the reduction of 𝒳 through i; since i is fully faithful (Stacks 0506), that is the substack cut out by i exactly when the reduction of 𝒳 is all of 𝒳, which is reducedness of 𝒳 by AlgebraicGeometry.Stack.isReducedStack_iff_essImage_stackReduction_eq_top.

theorem essImage_stackReduction_eq_essImage_iff_isReducedStack
    {𝒳 𝒳' : AlgebraicStacks.{u, w} B S hS} (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    (CatFiberedInGroupoids.homFunctor (stackReduction 𝒳').inclusion.hom).essImage =
        (CatFiberedInGroupoids.homFunctor i.hom).essImage ↔
      IsReducedStack B S hS 𝒳

Tag 0BPU, a lemma

Tag 0BPU in the Stacks Project.

AlgebraicGeometry.Stack.isThickening_diagonalComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonal.lean, line 466. The attribute's comment: “first assertion”.

Stacks 0BPU, the first assertion. In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the comparison 1-morphism 𝒳 ×_𝒴 𝒳 ⟶ 𝒳' ×_{𝒴'} 𝒳' is a thickening.

Since 𝒳 → 𝒴' factors through the closed substack 𝒴, the enlargement of the target identifies 𝒳 ×_𝒴 𝒳 with 𝒳 ×_{𝒴'} 𝒳 (Stacks 04ZZ (1) ⟹ (2) makes j fully faithful); the latter maps to 𝒳' ×_{𝒴'} 𝒳' by two base changes of the thickening i, one factor at a time, each a thickening by Stacks 0BPR, so their composite is one by Stacks 0BPS.

This carries the part key first assertion of Stacks 0BPU for this comparison 1-morphism. The other assertion of that tag, that the diagonal square is cartesian, is not proved for it — see the implementation notes, which name the obstruction. Both assertions are proved for the rebuilt comparison with an explicit body: the first by isThickening_selfProductDiagonalMap below, which carries the same part key, and the cartesian one by isTwoFibreProduct_selfProductDiagonalSquare. The 2-isomorphism between the two comparisons is still open, which is why the first assertion is registered twice rather than once.

The fppf-target-locality instance is Stacks 0420. The library proves it at the fpqc precoverage, isClosedImmersion_isLocalAtTarget_fpqc, and restricts it to the fppf precoverage asked for here in AlgebraicGeometry.Space.isClosedImmersion_isLocalAtTarget_fppf, which is an instance; the hypothesis below is therefore discharged automatically.

theorem isThickening_diagonalComparison
    [(Space.closedImmersionProperty B S hS).IsLocalAtTarget
      (Space.Topology.fppf.precoverage.{u, u} B S hS)] :
    IsThickening (diagonalComparison B S hS m)

AlgebraicGeometry.Stack.isThickening_selfProductDiagonalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonal.lean, line 807. The attribute's comment: “first assertion”.

Stacks 0BPU, the first assertion, for the comparison with an explicit body. For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the canonical comparison 1-morphism AlgebraicGeometry.Stack.selfProductDiagonalMap : 𝒳 ×_𝒴 𝒳 ⟶ 𝒳' ×_{𝒴'} 𝒳' is a thickening.

The source's factorisation of the comparison into two base changes of i, one factor at a time, is carried here strictly: the comparison is AlgebraicGeometry.Stack.selfProductFstLift followed by the base change of i along the first projection of 𝒳' ×_{𝒴'} 𝒳', on the nose (AlgebraicGeometry.Stack.selfProductFstLift_comp_snd, which holds by rfl). The second factor is a thickening by Stacks 0BPR (AlgebraicGeometry.Stack.isThickening_ambientFstRestriction_snd); the first is one because AlgebraicGeometry.Stack.isTwoFibreProduct_selfProductSndSquare exhibits it too as a base change of i, so Stacks 0BPR applies again; and their composite is a thickening by Stacks 0BPS, AlgebraicGeometry.Stack.isThickening_comp.

This carries the part key first assertion of Stacks 0BPU, and together with AlgebraicGeometry.Stack.isTwoFibreProduct_selfProductDiagonalSquare — which carries the part key cartesian diagonal square — it puts both assertions of the tag on this one comparison 1-morphism. The part key first assertion is also carried by AlgebraicGeometry.Stack.isThickening_diagonalComparison, the same assertion for the other canonical comparison AlgebraicGeometry.Stack.diagonalComparison; that registration is kept, the two comparisons being 2-isomorphic but not yet identified in the library.

The fppf-target-locality instance is Stacks 0420 and is discharged automatically, exactly as in AlgebraicGeometry.Stack.isThickening_diagonalComparison.

theorem isThickening_selfProductDiagonalMap
    [(Space.closedImmersionProperty B S hS).IsLocalAtTarget
      (Space.Topology.fppf.precoverage.{u, u} B S hS)] :
    IsThickening (selfProductDiagonalMap B S hS m)

AlgebraicGeometry.Stack.isTwoFibreProduct_selfProductDiagonalSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonal.lean, line 954. The attribute's comment: “cartesian diagonal square”.

Stacks 0BPU, the second assertion: the diagonal square of a morphism of thickenings of algebraic stacks is cartesian. For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the square

  𝒳  --Δ-->  𝒳 ×_𝒴 𝒳
  |              |
  v              v
  𝒳' --Δ'--> 𝒳' ×_{𝒴'} 𝒳'

is a 2-fibre product in the 2-category of algebraic stacks over (Sch/S)_fppf, the right-hand leg being the canonical comparison AlgebraicGeometry.Stack.selfProductDiagonalMap — canonical strictly, by AlgebraicGeometry.Stack.selfProductDiagonalMap_comp_fst and …_comp_snd.

The source proves this by applying Stacks 0CBB to 𝒳 ⟶ 𝒳' ⟶ 𝒴', using that the thickening i : 𝒳 ⟶ 𝒳' is a monomorphism. Here it is the over-the-base form of 0CBB with a growing target, CategoryTheory.TwoFibreProductOver.isEquivalence_selfProductDiagonalComparison, whose three hypotheses are met because a closed immersion of algebraic stacks is fully faithful (Stacks 04ZZ (1) ⟹ (2), AlgebraicGeometry.Stack.AlgebraicStacks.full_and_faithful_homFunctor_of_isClosedImmersion), applied to i for fullness and faithfulness and to j for the faithfulness the growing target costs. The passage from an equivalence of underlying categories to the universal property is CategoryTheory.Bicategory.isTwoFibreProduct_of_isEquivalence_to against the canonical 2-fibre product square of the cospan, and the passage from the 2-category of categories fibred in groupoids down to the full sub-2-category of algebraic stacks is AlgebraicGeometry.Stack.AlgebraicStacks.isTwoFibreProduct_of_toCatFiberedInGroupoids.

This carries the part key cartesian diagonal square of Stacks 0BPU; the other assertion, that the comparison is a thickening, is AlgebraicGeometry.Stack.isThickening_selfProductDiagonalMap, for this same comparison 1-morphism, so the two assertions of the tag are both statements about AlgebraicGeometry.Stack.selfProductDiagonalMap. The first assertion is registered a second time on AlgebraicGeometry.Stack.isThickening_diagonalComparison, which asserts it of the other canonical comparison AlgebraicGeometry.Stack.diagonalComparison; the implementation note above says why the cartesian assertion cannot be carried by that one.

What identifying the two comparisons still lacks. The two 1-morphisms are 2-isomorphic, being two canonical comparisons into a 2-fibre product, and AlgebraicGeometry.Stack.isThickening_congr_twoIso would then make either of the two first-assertion registrations redundant. The 2-isomorphism is not available from CategoryTheory.Bicategory.twoFibreProduct_twoIso_of_legs, however: that result needs the two comparison 2-cells to be compatible with the filler of 𝒳' ×_{𝒴'} 𝒳', and that compatibility mentions the filler whiskered by AlgebraicGeometry.Stack.diagonalComparison, which is the very thing the Quotient.out in AlgebraicGeometry.Stack.selfProductComparison makes uncomputable. It would instead have to come from CategoryTheory.Bicategory.twoFibreProduct_twoIso_of_preHom, i.e. by exhibiting AlgebraicGeometry.Stack.diagonalComparison as the 1-morphism of a pre-morphism of 2-commutative squares assembled by CategoryTheory.Bicategory.TwoCommSq.PreHom.comp from its four stages — the enlargement of the target, the comparison of the two models of the cospan (f ≫ j, f ≫ j), and the two base changes of i — which is a chase through two cospan reindexings that the library does not currently assemble.

def isTwoFibreProduct_selfProductDiagonalSquare :
    Bicategory.IsTwoFibreProduct (selfProductDiagonalSquare B S hS m)

Tag 0BPV, a lemma

Tag 0BPV in the Stacks Project.

AlgebraicGeometry.Stack.isSurjective_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonal.lean, line 1010. The attribute's comment: “surjective (granted: the diagonal comparison is a thickening)”.

Stacks 0BPV at the surjectivity property. For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is surjective (Stacks 04ZS) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

The two diagonals are a morphism of thickenings (AlgebraicGeometry.Stack.diagonalThickeningMorphism), and surjectivity passes between the two 1-morphisms of a morphism of thickenings by Stacks 0CJ9 part (2).

Parameter: hk, that the comparison 𝒳 ×_𝒴 𝒳 ⟶ 𝒳' ×_{𝒴'} 𝒳' of AlgebraicGeometry.Stack.selfProductDiagonalMap is a thickening. That is the first assertion of Stacks 0BPU, proved in AlgebraicGeometry.Stack.isThickening_selfProductDiagonalMap; see AlgebraicGeometry.Stack.diagonalThickeningMorphism.

theorem isSurjective_relativeDiagonal_iff
    (hk : IsThickening (selfProductDiagonalMap B S hS m)) :
    IsSurjective B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner) ↔
      IsSurjective B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer)

AlgebraicGeometry.Stack.isAffineHom_relativeDiagonal_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalAffine.lean, line 117. The attribute's comment: “property (b) of seventeen: affine”.

Stacks 0BPV, property (b). For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is affine in the sense of Stacks 04XB (Stacks 03WF) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isAffineHom_relativeDiagonal_inner_iff_outer :
    Stack.IsAffineHom B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom ↔
      Stack.IsAffineHom B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom

AlgebraicGeometry.Stack.isIntegralHom_relativeDiagonal_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalAffine.lean, line 139. The attribute's comment: “property (f) of seventeen: integral”.

Stacks 0BPV, property (f). For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is integral in the sense of Stacks 04XB (Stacks 03ZP) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isIntegralHom_relativeDiagonal_inner_iff_outer :
    HasRelativeProperty.{u, u, u + 1, u} B S hS (Space.integralMorphismProperty B S hS)
        (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom
        (isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks B S hS m.inner) ↔
      HasRelativeProperty.{u, u, u + 1, u} B S hS (Space.integralMorphismProperty B S hS)
        (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom
        (isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks B S hS m.outer)

AlgebraicGeometry.Stack.isSurjective_relativeDiagonal_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalClauses.lean, line 95. The attribute's comment: “property (c) of seventeen: surjective”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is surjective (Stacks 04ZS) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isSurjective_relativeDiagonal_inner_iff_outer :
    IsSurjective B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner) ↔
      IsSurjective B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer)

AlgebraicGeometry.Stack.universallyInjective_relativeDiagonal_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalClauses.lean, line 105. The attribute's comment: “property (i) of seventeen: universally injective”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is universally injective (Stacks 0CI2) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem universallyInjective_relativeDiagonal_inner_iff_outer :
    UniversallyInjective B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner) ↔
      UniversallyInjective B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer)

AlgebraicGeometry.Stack.isLocallyQuasiFinite_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalPointTest.lean, line 132. The attribute's comment: “property (k) of seventeen: locally quasi-finite”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is locally quasi-finite in the sense of Stacks 04XB (Stacks 03XJ, part (1)) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isLocallyQuasiFinite_relativeDiagonal_iff :
    Stack.IsLocallyQuasiFinite B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom ↔
      Stack.IsLocallyQuasiFinite B S hS
        (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom

AlgebraicGeometry.Stack.isFinite_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalPointTest.lean, line 142. The attribute's comment: “property (l) of seventeen: finite”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is finite in the sense of Stacks 04XB (Stacks 03ZP) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isFinite_relativeDiagonal_iff :
    HasRelativeProperty.{u, u, u + 1, u} B S hS (Space.finiteMorphismProperty B S hS)
        (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom
        (isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks B S hS m.inner) ↔
      HasRelativeProperty.{u, u, u + 1, u} B S hS (Space.finiteMorphismProperty B S hS)
        (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom
        (isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks B S hS m.outer)

AlgebraicGeometry.Stack.unramified_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalPointTest.lean, line 159. The attribute's comment: “property (m) of seventeen: unramified”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is unramified in the sense of Stacks 04XB (Stacks 03ZH, part (1)) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem unramified_relativeDiagonal_iff :
    haveI : (Space.unramifiedMorphismProperty B S hS).IsStableUnderBaseChange :=
      Space.isUnramified_isStableUnderBaseChange B S hS
    haveI : (Space.unramifiedMorphismProperty B S hS).IsLocalAtTarget
        (Space.Topology.fppf.precoverage.{u, u} B S hS) :=
      (Space.isUnramified_isLocalAtTarget_fpqc.{u, u} B S hS).of_le
        (Space.fppfPrecoverage_le_fpqcPrecoverage.{u, u} B S hS)
    HasRelativeProperty.{u, u, u + 1, u} B S hS (Space.unramifiedMorphismProperty B S hS)
        (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom
        (isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks B S hS m.inner) ↔
      HasRelativeProperty.{u, u, u + 1, u} B S hS (Space.unramifiedMorphismProperty B S hS)
        (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom
        (isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks B S hS m.outer)

AlgebraicGeometry.Stack.mono_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalPointTest.lean, line 188. The attribute's comment: “property (n) of seventeen: monomorphism”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is a monomorphism in the sense of Stacks 04XB if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem mono_relativeDiagonal_iff :
    HasRelativeProperty.{u, u, u + 1, u} B S hS
        (MorphismProperty.monomorphisms (AlgebraicSpaces B S hS))
        (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom
        (isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks B S hS m.inner) ↔
      HasRelativeProperty.{u, u, u + 1, u} B S hS
        (MorphismProperty.monomorphisms (AlgebraicSpaces B S hS))
        (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom
        (isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks B S hS m.outer)

AlgebraicGeometry.Stack.isImmersion_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalPointTest.lean, line 206. The attribute's comment: “property (o) of seventeen: immersion”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is an immersion in the sense of Stacks 04XB if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isImmersion_relativeDiagonal_iff :
    Stack.IsImmersion B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom ↔
      Stack.IsImmersion B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom

AlgebraicGeometry.Stack.isClosedImmersion_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalPointTest.lean, line 222. The attribute's comment: “property (p) of seventeen: closed immersion”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is a closed immersion in the sense of Stacks 04XB if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isClosedImmersion_relativeDiagonal_iff :
    Stack.IsClosedImmersion B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom ↔
      Stack.IsClosedImmersion B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom

AlgebraicGeometry.Stack.isRepresentableMorphism_relativeDiagonal_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDiagonalRepresentable.lean, line 159. The attribute's comment: “property (a) of seventeen: representable by schemes”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is representable by schemes (Stacks 02Y7) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isRepresentableMorphism_relativeDiagonal_inner_iff_outer :
    Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳.val.val.p
        (AlgebraicStacks.twoFibreProduct B S hS m.inner m.inner).val.val.p
        (CatFiberedInGroupoids.homFunctor
          (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom) ↔
      Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳'.val.val.p
        (AlgebraicStacks.twoFibreProduct B S hS m.outer m.outer).val.val.p
        (CatFiberedInGroupoids.homFunctor
          (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom)

AlgebraicGeometry.Stack.isQuasiCompact_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationConverse.lean, line 321. The attribute's comment: “property (d) of seventeen: quasi-compact”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is quasi-compact in the sense of Stacks 04XB (Stacks 03HE) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isQuasiCompact_relativeDiagonal_iff :
    Stack.IsQuasiCompact B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom ↔
      Stack.IsQuasiCompact B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom

AlgebraicGeometry.Stack.isQuasiSeparated_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationConverse.lean, line 333. The attribute's comment: “property (g) of seventeen: quasi-separated”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is quasi-separated in the sense of Stacks 04XB (Stacks 03HL part (3)) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isQuasiSeparated_relativeDiagonal_iff :
    Stack.IsQuasiSeparated B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom ↔
      Stack.IsQuasiSeparated B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom

AlgebraicGeometry.Stack.isSeparated_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationConverse.lean, line 347. The attribute's comment: “property (h) of seventeen: separated”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is separated in the sense of Stacks 04XB (Stacks 03HL part (1)) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isSeparated_relativeDiagonal_iff :
    Stack.IsSeparated B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom ↔
      Stack.IsSeparated B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom

AlgebraicGeometry.Stack.universallyClosed_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationConverse.lean, line 361. The attribute's comment: “property (e) of seventeen: universally closed”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is universally closed in the sense of Stacks 04XB (Stacks 03HI part (2)) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem universallyClosed_relativeDiagonal_iff :
    Stack.UniversallyClosed B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom ↔
      Stack.UniversallyClosed B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom

AlgebraicGeometry.Stack.universallyOpen_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationConverse.lean, line 374. The attribute's comment: “property (j) of seventeen: universally open”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is universally open in the sense of Stacks 04XB (Stacks 03Z2 part (2)) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem universallyOpen_relativeDiagonal_iff :
    HasRelativeProperty.{u, u, u + 1, u} B S hS (Space.universallyOpenMorphismProperty B S hS)
        (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom
        (isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks B S hS m.inner) ↔
      HasRelativeProperty.{u, u, u + 1, u} B S hS (Space.universallyOpenMorphismProperty B S hS)
        (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom
        (isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks B S hS m.outer)

AlgebraicGeometry.Stack.isProper_relativeDiagonal_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationConverse.lean, line 414. The attribute's comment: “property (q) of seventeen: proper”.

For a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the relative diagonal Δ : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 is proper in the sense of Stacks 04XB (Stacks 03ZM) if and only if Δ' : 𝒳' ⟶ 𝒳' ×_{𝒴'} 𝒳' is.

theorem isProper_relativeDiagonal_iff :
    Stack.IsProper B S hS (AlgebraicStacks.relativeDiagonal B S hS m.inner).hom ↔
      Stack.IsProper B S hS (AlgebraicStacks.relativeDiagonal B S hS m.outer).hom

Tag 0BPW, a lemma

Tag 0BPW in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableCFG_iff_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningIsScheme.lean, line 48. The attribute's comment: “clause (2): scheme”.

If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S, then 𝒳 is a scheme if and only if 𝒳' is a scheme.

theorem isRepresentableCFG_iff_of_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    Stacks.RepresentableMorphism.IsRepresentableCFG 𝒳.val.val.p ↔
      Stacks.RepresentableMorphism.IsRepresentableCFG 𝒳'.val.val.p

AlgebraicGeometry.Stack.isDMOver_iff_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningQuasiDMDeligneMumford.lean, line 429. The attribute's comment: “clause (3): DM over the base”.

If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S, then 𝒳 is DM over S if and only if 𝒳' is DM over S.

theorem isDMOver_iff_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    IsDMOver B S hS 𝒳 ↔ IsDMOver B S hS 𝒳'

AlgebraicGeometry.Stack.isQuasiDMOver_iff_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningQuasiDMDeligneMumford.lean, line 436. The attribute's comment: “clause (4): quasi-DM over the base”.

If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S, then 𝒳 is quasi-DM over S if and only if 𝒳' is quasi-DM over S.

theorem isQuasiDMOver_iff_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    IsQuasiDMOver B S hS 𝒳 ↔ IsQuasiDMOver B S hS 𝒳'

AlgebraicGeometry.Stack.isDMAbs_iff_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningQuasiDMDeligneMumford.lean, line 445. The attribute's comment: “clause (3): DM, the absolute axiom of Stacks 050D part (5)”.

If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S, then 𝒳 is Deligne–Mumford if and only if 𝒳' is Deligne–Mumford, in the absolute sense of AlgebraicGeometry.Stack.IsDMAbs.

theorem isDMAbs_iff_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    IsDMAbs.{u, w, w'} B S hS 𝒳 ↔ IsDMAbs.{u, w, w'} B S hS 𝒳'

AlgebraicGeometry.Stack.isQuasiDMAbs_iff_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningQuasiDMDeligneMumford.lean, line 454. The attribute's comment: “clause (4): quasi-DM, the absolute axiom of Stacks 050D part (6)”.

If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S, then 𝒳 is quasi-DM if and only if 𝒳' is quasi-DM, in the absolute sense of AlgebraicGeometry.Stack.IsQuasiDMAbs.

theorem isQuasiDMAbs_iff_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    IsQuasiDMAbs.{u, w, w'} B S hS 𝒳 ↔ IsQuasiDMAbs.{u, w, w'} B S hS 𝒳'

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_iff_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningQuasiDMDeligneMumford.lean, line 463. The attribute's comment: “clause (1): algebraic space, the whole equivalence”.

If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S, then 𝒳 is an algebraic space if and only if 𝒳' is an algebraic space.

theorem isRepresentableByAlgebraicSpace_iff_isThickening (i : 𝒳 ⟶ 𝒳')
    (hi : IsThickening i) :
    IsRepresentableByAlgebraicSpace B S hS 𝒳.val ↔
      IsRepresentableByAlgebraicSpace B S hS 𝒳'.val

AlgebraicGeometry.Stack.isSeparatedAbs_iff_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationAbsolute.lean, line 122. The attribute's comment: “clause (5): separated, the absolute axiom of Stacks 050D part (7)”.

Stacks 0BPW, clause (5). If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S then 𝒳 is separated if and only if 𝒳' is — the absolute axiom, part (7) of Stacks 050D.

Both sides are separatedness over Spec(ℤ) of the stacks viewed by Stacks 04X6, and the thickening viewed over Spec(ℤ) is a thickening (AlgebraicGeometry.Stack.isThickening_changeBaseHomAlgebraicStacks), so this is AlgebraicGeometry.Stack.isSeparatedOver_iff_isThickening at the base Spec(ℤ).

theorem isSeparatedAbs_iff_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    IsSeparatedAbs.{u, w, w'} B S hS 𝒳 ↔ IsSeparatedAbs.{u, w, w'} B S hS 𝒳'

AlgebraicGeometry.Stack.isQuasiSeparatedAbs_iff_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationAbsolute.lean, line 136. The attribute's comment: “clause (6): quasi-separated, the absolute axiom of Stacks 050D part (8)”.

Stacks 0BPW, clause (6). If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S then 𝒳 is quasi-separated if and only if 𝒳' is — the absolute axiom, part (8) of Stacks 050D.

The companion of AlgebraicGeometry.Stack.isSeparatedAbs_iff_isThickening at AlgebraicGeometry.Stack.isQuasiSeparatedOver_iff_isThickening.

theorem isQuasiSeparatedAbs_iff_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    IsQuasiSeparatedAbs.{u, w, w'} B S hS 𝒳 ↔ IsQuasiSeparatedAbs.{u, w, w'} B S hS 𝒳'

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationAxioms.lean, line 470. The attribute's comment: “clause (1): algebraic space -- only part of the clause, namely the implication from the ambient stack to the closed substack; the whole equivalence is AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_iff_isThickening”.

Stacks 0BPW, clause (1), from the ambient stack to the closed substack. If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S and 𝒳' is an algebraic space, then so is 𝒳.

The thickening i is a closed immersion, hence representable by algebraic spaces, and 𝒳 is the apex of the degenerate 2-fibre product 𝒳' ×_{𝒳'} 𝒳 of CategoryTheory.Bicategory.TwoCommSq.idCospan; so Stacks 04ZP, the implication (1) ⟹ (2) (AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_of_isTwoFibreProduct), applies. Only the closed-immersion half of AlgebraicGeometry.Stack.IsThickening is used.

theorem isRepresentableByAlgebraicSpace_of_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i)
    (h : IsRepresentableByAlgebraicSpace B S hS 𝒳'.val) :
    IsRepresentableByAlgebraicSpace B S hS 𝒳.val

AlgebraicGeometry.Stack.isDMOver_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationAxioms.lean, line 494. The attribute's comment: “clause (3): DM over the base -- only part of the clause, namely the implication from the ambient stack to the closed substack; the whole equivalence is AlgebraicGeometry.Stack.isDMOver_iff_isThickening”.

One half of Stacks 0BPW, clause (3). If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S and 𝒳' is DM over S, then so is 𝒳.

The thickening is read as a morphism of thickenings over the base (AlgebraicGeometry.Stack.structureThickeningMorphism) and AlgebraicGeometry.Stack.isDM_inner_of_outer applies to it. The separation axiom is part (1) of Stacks 050D, DM over the base scheme of the site; see the implementation notes of this file for why the statement is not at the absolute form, part (5).

Untagged: the clause itself is the equivalence AlgebraicGeometry.Stack.isDMOver_iff_isThickening in StacksFrontier.AlgebraicGeometry.Stacks.ThickeningQuasiDMDeligneMumford, which is item (9) of Stacks 0CJ9 at the same viewing and carries the part key.

theorem isDMOver_of_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i)
    (h : IsDMOver B S hS 𝒳') : IsDMOver B S hS 𝒳

AlgebraicGeometry.Stack.isQuasiDMOver_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationAxioms.lean, line 509. The attribute's comment: “clause (4): quasi-DM over the base -- only part of the clause, namely the implication from the ambient stack to the closed substack; the whole equivalence is AlgebraicGeometry.Stack.isQuasiDMOver_iff_isThickening”.

One half of Stacks 0BPW, clause (4). If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S and 𝒳' is quasi-DM over S, then so is 𝒳. The companion of AlgebraicGeometry.Stack.isDMOver_of_isThickening at part (2) of Stacks 050D.

Untagged: the clause itself is the equivalence AlgebraicGeometry.Stack.isQuasiDMOver_iff_isThickening in StacksFrontier.AlgebraicGeometry.Stacks.ThickeningQuasiDMDeligneMumford, which is item (8) of Stacks 0CJ9 at the same viewing and carries the part key.

theorem isQuasiDMOver_of_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i)
    (h : IsQuasiDMOver B S hS 𝒳') : IsQuasiDMOver B S hS 𝒳

AlgebraicGeometry.Stack.isSeparatedOver_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationAxioms.lean, line 524. The attribute's comment: “clause (5): separated over the base -- only part of the clause, namely the implication from the ambient stack to the closed substack; the whole equivalence is AlgebraicGeometry.Stack.isSeparatedOver_iff_isThickening”.

One half of Stacks 0BPW, clause (5). If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S and 𝒳' is separated over S, then so is 𝒳. The companion of AlgebraicGeometry.Stack.isDMOver_of_isThickening at part (3) of Stacks 050D.

Untagged: the clause itself is the equivalence AlgebraicGeometry.Stack.isSeparatedOver_iff_isThickening in StacksFrontier.AlgebraicGeometry.Stacks.ThickeningSeparationConverse, which is built from this implication and its converse and carries the part key.

theorem isSeparatedOver_of_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i)
    (h : IsSeparatedOver B S hS 𝒳') : IsSeparatedOver B S hS 𝒳

AlgebraicGeometry.Stack.isQuasiSeparatedOver_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationAxioms.lean, line 539. The attribute's comment: “clause (6): quasi-separated over the base -- only part of the clause, namely the implication from the ambient stack to the closed substack; the whole equivalence is AlgebraicGeometry.Stack.isQuasiSeparatedOver_iff_isThickening”.

One half of Stacks 0BPW, clause (6). If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S and 𝒳' is quasi-separated over S, then so is 𝒳. The companion of AlgebraicGeometry.Stack.isDMOver_of_isThickening at part (4) of Stacks 050D.

Untagged: the clause itself is the equivalence AlgebraicGeometry.Stack.isQuasiSeparatedOver_iff_isThickening in StacksFrontier.AlgebraicGeometry.Stacks.ThickeningSeparationConverse, which is built from this implication and its converse and carries the part key.

theorem isQuasiSeparatedOver_of_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i)
    (h : IsQuasiSeparatedOver B S hS 𝒳') : IsQuasiSeparatedOver B S hS 𝒳

AlgebraicGeometry.Stack.isQuasiSeparatedOver_iff_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationConverse.lean, line 430. The attribute's comment: “clause (6): quasi-separated over the base”.

If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S then 𝒳 is quasi-separated over S if and only if 𝒳' is. Here quasi-separatedness over S is part (4) of Stacks 050D.

theorem isQuasiSeparatedOver_iff_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    IsQuasiSeparatedOver B S hS 𝒳 ↔ IsQuasiSeparatedOver B S hS 𝒳'

AlgebraicGeometry.Stack.isSeparatedOver_iff_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningSeparationConverse.lean, line 438. The attribute's comment: “clause (5): separated over the base”.

If 𝒳 ⊂ 𝒳' is a thickening of algebraic stacks over S then 𝒳 is separated over S if and only if 𝒳' is. Here separatedness over S is part (3) of Stacks 050D.

theorem isSeparatedOver_iff_isThickening (i : 𝒳 ⟶ 𝒳') (hi : IsThickening i) :
    IsSeparatedOver B S hS 𝒳 ↔ IsSeparatedOver B S hS 𝒳'

Sources

• Section 106.3, Tag 0BPN
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.IsThickening · AlgebraicGeometry.Stack.ThickeningMorphism · AlgebraicGeometry.Stack.ThickeningOver · AlgebraicGeometry.Stack.ThickeningMorphismOver · AlgebraicGeometry.Stack.isThickening_iff_isRelativeThickening · AlgebraicGeometry.Stack.isClosedImmersion_of_isThickening · AlgebraicGeometry.Stack.universalHomeomorphism_of_isThickening · AlgebraicGeometry.Stack.AlgebraicStacks.IsFirstOrderThickening

Section106.4 Morphisms of thickenings#

Section 106.4 of the Stacks Project, Tag 0CJ8. 1 tag here is carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CJ9, a lemma

Tag 0CJ9 in the Stacks Project.

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

Stacks 0CJ9, part (1). In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the restricted 1-morphism f is affine (Stacks 0CHQ) if and only if the ambient 1-morphism f' is.

Representability by algebraic spaces is part (12) of the tag; affineness in the sense of Stacks 04XB is AlgebraicGeometry.Stack.hasRelativeProperty_outer_of_inner and AlgebraicGeometry.Stack.hasRelativeProperty_inner_of_outer at AlgebraicGeometry.Space.affineMorphismProperty, with the cancellation AlgebraicGeometry.Space.isAffineHom_of_comp_of_isClosedImmersion_of_isSurjective.

theorem isAffineHom_inner_iff_outer (m : ThickeningMorphism i j hi hj) :
    AlgebraicStacks.IsAffineHom B S hS m.inner ↔ AlgebraicStacks.IsAffineHom B S hS m.outer

AlgebraicGeometry.Stack.isIntegralHom_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningMorphismAffineIntegral.lean, line 242. The attribute's comment: “part (5): integral”.

Stacks 0CJ9, part (5). In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the restricted 1-morphism f is integral (Stacks 0CHU) if and only if the ambient 1-morphism f' is.

The argument is that of part (1) at AlgebraicGeometry.Space.integralMorphismProperty, with the cancellation AlgebraicGeometry.Space.isIntegralHom_of_comp_of_isClosedImmersion_of_isSurjective (Stacks 0415 splits integrality into affineness and universal closedness, which both cancel).

theorem isIntegralHom_inner_iff_outer (m : ThickeningMorphism i j hi hj) :
    AlgebraicStacks.IsIntegralHom B S hS m.inner ↔
      AlgebraicStacks.IsIntegralHom B S hS m.outer

AlgebraicGeometry.Stack.isQuasiSeparated_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningMorphismProperties.lean, line 95. The attribute's comment: “part (10): quasi-separated”.

Stacks 0CJ9, part (10), the quasi-separated half. In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the restricted 1-morphism f is quasi-separated (Stacks 04YW) if and only if the ambient 1-morphism f' is.

As in the source, this is a condition on the relative diagonals, which form a morphism of thickenings (Stacks 0BPU), and it is clauses (d) and (g) of Stacks 0BPV: AlgebraicGeometry.Stack.isQuasiSeparated_outer_of_inner and AlgebraicGeometry.Stack.isQuasiSeparated_inner_of_outer.

theorem isQuasiSeparated_inner_iff_outer (m : ThickeningMorphism i j hi hj) :
    AlgebraicStacks.IsQuasiSeparated B S hS m.inner ↔
      AlgebraicStacks.IsQuasiSeparated B S hS m.outer

AlgebraicGeometry.Stack.isSeparated_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningMorphismProperties.lean, line 108. The attribute's comment: “part (10): separated”.

Stacks 0CJ9, part (10), the separated half. In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the restricted 1-morphism f is separated (Stacks 04YW) if and only if the ambient 1-morphism f' is.

Separatedness is properness of the relative diagonal, and this is clause (q) of Stacks 0BPV: AlgebraicGeometry.Stack.isSeparated_outer_of_inner and AlgebraicGeometry.Stack.isSeparated_inner_of_outer.

theorem isSeparated_inner_iff_outer (m : ThickeningMorphism i j hi hj) :
    AlgebraicStacks.IsSeparated B S hS m.inner ↔ AlgebraicStacks.IsSeparated B S hS m.outer

AlgebraicGeometry.Stack.thickeningMorphism_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningMorphismProperties.lean, line 132.

Stacks 0CJ9. Let (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') be a morphism of thickenings of algebraic stacks over S, f = m.inner and f' = m.outer. Then (1) f is affine if and only if f' is affine, (2) f is surjective if and only if f' is surjective, (3) f is quasi-compact if and only if f' is quasi-compact, (4) f is universally closed if and only if f' is universally closed, (5) f is integral if and only if f' is integral, (6) f is universally injective if and only if f' is universally injective, (7) f is universally open if and only if f' is universally open, (8) f is quasi-DM if and only if f' is quasi-DM, (9) f is DM if and only if f' is DM, (10) f is quasi-separated if and only if f' is quasi-separated, and f is separated if and only if f' is separated, (11) f is representable if and only if f' is representable, (12) f is representable by algebraic spaces if and only if f' is representable by algebraic spaces.

The conjuncts are, in order, the twelve items of the source; item (13) ("add more here") states nothing.

theorem thickeningMorphism_inner_iff_outer (m : ThickeningMorphism i j hi hj) :
    (AlgebraicStacks.IsAffineHom B S hS m.inner ↔ AlgebraicStacks.IsAffineHom B S hS m.outer) ∧
    (IsSurjective B S hS m.inner ↔ IsSurjective B S hS m.outer) ∧
    (IsQuasiCompactMorphism B S hS m.inner ↔ IsQuasiCompactMorphism B S hS m.outer) ∧
    (AlgebraicStacks.UniversallyClosed B S hS m.inner ↔
      AlgebraicStacks.UniversallyClosed B S hS m.outer) ∧
    (AlgebraicStacks.IsIntegralHom B S hS m.inner ↔
      AlgebraicStacks.IsIntegralHom B S hS m.outer) ∧
    (UniversallyInjective B S hS m.inner ↔ UniversallyInjective B S hS m.outer) ∧
    (AlgebraicStacks.UniversallyOpen B S hS m.inner ↔
      AlgebraicStacks.UniversallyOpen B S hS m.outer) ∧
    (AlgebraicStacks.IsQuasiDM B S hS m.inner ↔ AlgebraicStacks.IsQuasiDM B S hS m.outer) ∧
    (IsDM B S hS m.inner ↔ IsDM B S hS m.outer) ∧
    ((AlgebraicStacks.IsQuasiSeparated B S hS m.inner ↔
        AlgebraicStacks.IsQuasiSeparated B S hS m.outer) ∧
      (AlgebraicStacks.IsSeparated B S hS m.inner ↔
        AlgebraicStacks.IsSeparated B S hS m.outer)) ∧
    (Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳.val.val.p 𝒴.val.val.p
        (CatFiberedInGroupoids.homFunctor m.inner.hom) ↔
      Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳'.val.val.p 𝒴'.val.val.p
        (CatFiberedInGroupoids.homFunctor m.outer.hom)) ∧
    (IsRepresentableByAlgebraicSpaces B S hS m.inner.hom.hom ↔
      IsRepresentableByAlgebraicSpaces B S hS m.outer.hom.hom)

AlgebraicGeometry.Stack.isRepresentableMorphism_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningMorphismRepresentable.lean, line 131. The attribute's comment: “part (11): representable”.

Stacks 0CJ9, part (11). In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the restricted 1-morphism f is representable (by schemes, Stacks 02Y7) if and only if the ambient 1-morphism f' is.

theorem isRepresentableMorphism_inner_iff_outer (m : ThickeningMorphism i j hi hj) :
    Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳.val.val.p 𝒴.val.val.p
        (CatFiberedInGroupoids.homFunctor m.inner.hom) ↔
      Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳'.val.val.p 𝒴'.val.val.p
        (CatFiberedInGroupoids.homFunctor m.outer.hom)

AlgebraicGeometry.Stack.universallyClosed_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningMorphismTopologicalProperties.lean, line 295. The attribute's comment: “part (4): universally closed”.

Stacks 0CJ9, part (4). In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the restricted 1-morphism f is universally closed (Stacks 0513) if and only if the ambient 1-morphism f' is.

The base changes of f and of f' are compared by the thickenings of AlgebraicGeometry.Stack.exists_isThickening_baseChange_comp and AlgebraicGeometry.Stack.exists_isThickening_baseChange_outer, which are homeomorphisms on points (Stacks 0CJ7).

theorem universallyClosed_inner_iff_outer (m : ThickeningMorphism i j hi hj) :
    AlgebraicStacks.UniversallyClosed B S hS m.inner ↔
      AlgebraicStacks.UniversallyClosed B S hS m.outer

AlgebraicGeometry.Stack.universallyOpen_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningMorphismTopologicalProperties.lean, line 338. The attribute's comment: “part (7): universally open”.

Stacks 0CJ9, part (7). In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the restricted 1-morphism f is universally open (Stacks 06U2) if and only if the ambient 1-morphism f' is. The argument is that of part (4).

theorem universallyOpen_inner_iff_outer (m : ThickeningMorphism i j hi hj) :
    AlgebraicStacks.UniversallyOpen B S hS m.inner ↔
      AlgebraicStacks.UniversallyOpen B S hS m.outer

AlgebraicGeometry.Stack.isQuasiCompactMorphism_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningMorphismTopologicalProperties.lean, line 383. The attribute's comment: “part (3): quasi-compact”.

Stacks 0CJ9, part (3). In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the restricted 1-morphism f is quasi-compact (Stacks 050U) if and only if the ambient 1-morphism f' is.

Quasi-compactness of an algebraic stack is compactness of its space of points (Stacks 04YB), and the base changes of f and of f' are compared by the thickenings of AlgebraicGeometry.Stack.exists_isThickening_baseChange_comp and AlgebraicGeometry.Stack.exists_isThickening_baseChange_outer.

theorem isQuasiCompactMorphism_inner_iff_outer (m : ThickeningMorphism i j hi hj) :
    IsQuasiCompactMorphism B S hS m.inner ↔ IsQuasiCompactMorphism B S hS m.outer

AlgebraicGeometry.Stack.isQuasiDM_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningQuasiDMDeligneMumford.lean, line 355. The attribute's comment: “item (8): quasi-DM”.

In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the 1-morphism f is quasi-DM if and only if f' is quasi-DM.

theorem isQuasiDM_inner_iff_outer :
    AlgebraicStacks.IsQuasiDM B S hS m.inner ↔ AlgebraicStacks.IsQuasiDM B S hS m.outer

AlgebraicGeometry.Stack.isDM_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningQuasiDMDeligneMumford.lean, line 369. The attribute's comment: “item (9): DM”.

In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the 1-morphism f is Deligne–Mumford if and only if f' is Deligne–Mumford.

theorem isDM_inner_iff_outer : IsDM B S hS m.inner ↔ IsDM B S hS m.outer

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningQuasiDMDeligneMumford.lean, line 409. The attribute's comment: “item (12): representable by algebraic spaces”.

In a morphism of thickenings (f, f') : (𝒳 ⊂ 𝒳') → (𝒴 ⊂ 𝒴') of algebraic stacks over S, the 1-morphism f is representable by algebraic spaces if and only if f' is.

theorem isRepresentableByAlgebraicSpaces_inner_iff_outer :
    IsRepresentableByAlgebraicSpaces B S hS m.inner.hom.hom ↔
      IsRepresentableByAlgebraicSpaces B S hS m.outer.hom.hom

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

Stacks 0CJ9, part (2). In a morphism of thickenings of algebraic stacks over S, the restricted 1-morphism is surjective if and only if the ambient 1-morphism is surjective.

Surjectivity is a condition on the map of sets of points of Stacks 04ZS, the restriction square induces a commutative square of those maps, and the two vertical maps of that square — the thickenings — are bijective.

theorem isSurjective_inner_iff_outer {𝒳 𝒳' 𝒴 𝒴' : AlgebraicStacks.{u, w} B S hS}
    {i : 𝒳 ⟶ 𝒳'} {j : 𝒴 ⟶ 𝒴'} {hi : IsThickening i} {hj : IsThickening j}
    (m : ThickeningMorphism i j hi hj) :
    IsSurjective B S hS m.inner ↔ IsSurjective B S hS m.outer

AlgebraicGeometry.Stack.universallyInjective_inner_iff_outer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningUniversallyInjective.lean, line 285. The attribute's comment: “part (6): universally injective”.

Stacks 0CJ9, part (6). In a morphism of thickenings of algebraic stacks over S, the restricted 1-morphism is universally injective if and only if the ambient 1-morphism is universally injective.

theorem universallyInjective_inner_iff_outer (m : ThickeningMorphism i j hi hj) :
    UniversallyInjective B S hS m.inner ↔ UniversallyInjective B S hS m.outer

Sources

• Section 106.4, Tag 0CJ8
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isAffineHom_inner_iff_outer · AlgebraicGeometry.Stack.isIntegralHom_inner_iff_outer · AlgebraicGeometry.Stack.isQuasiSeparated_inner_iff_outer · AlgebraicGeometry.Stack.isSeparated_inner_iff_outer · AlgebraicGeometry.Stack.thickeningMorphism_inner_iff_outer · AlgebraicGeometry.Stack.isRepresentableMorphism_inner_iff_outer · AlgebraicGeometry.Stack.universallyClosed_inner_iff_outer · AlgebraicGeometry.Stack.universallyOpen_inner_iff_outer

Section106.5 Infinitesimal deformations of algebraic stacks#

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

Tag 0CJB, a lemma

Tag 0CJB in the Stacks Project.

AlgebraicGeometry.Stack.isFlat_ambient_of_flatDeformation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningFlatDeformation.lean, line 972. The attribute's comment: “flatness of the ambient morphism”.

For a commutative diagram of algebraic stacks over S over a thickening iB : ℬ ⟶ ℬ' of bases, whose cube commutes (hcoh), with 𝒴' ⟶ ℬ' locally of finite type, 𝒳' ⟶ ℬ' flat and locally of finite presentation, the restricted 1-morphism f flat, and the two restricted stacks the base changes of the ambient ones along iB, the ambient 1-morphism f' is flat.

theorem isFlat_ambient_of_flatDeformation
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : AlgebraicStacks.IsLocallyOfFiniteType B S hS pY')
    (hXflat : AlgebraicStacks.IsFlat B S hS pX')
    (hXfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS pX')
    (hfflat : AlgebraicStacks.IsFlat B S hS f) :
    AlgebraicStacks.IsFlat B S hS f'

AlgebraicGeometry.Stack.isFlatAt_target_of_flatDeformation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningFlatDeformation.lean, line 1004. The attribute's comment: “flatness of the target over the base at image points”.

Under the hypotheses of AlgebraicGeometry.Stack.isFlat_ambient_of_flatDeformation, the structure 1-morphism 𝒴' ⟶ ℬ' is flat, in the sense of Stacks 0CID, at every point of |𝒴'| in the image of |f'|.

theorem isFlatAt_target_of_flatDeformation
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : AlgebraicStacks.IsLocallyOfFiniteType B S hS pY')
    (hXflat : AlgebraicStacks.IsFlat B S hS pX')
    (hXfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS pX')
    (hfflat : AlgebraicStacks.IsFlat B S hS f)
    (x' : AlgebraicStacks.points B S hS 𝒳') :
    AlgebraicStacks.IsFlatAt B S hS pY' (AlgebraicStacks.pointsMap B S hS f' x')

AlgebraicGeometry.Stack.isFlat_of_flatDeformation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningFlatDeformationCoherence.lean, line 224.

Stacks 0CJB. Let iB : ℬ ⟶ ℬ' be a thickening of algebraic stacks over S, let pX' : 𝒳' ⟶ ℬ' and pY' : 𝒴' ⟶ ℬ' be structure 1-morphisms, and let f' : 𝒳' ⟶ 𝒴' be a 1-morphism over ℬ', by houter. Let PX and PY present the restricted source and target as the base changes of 𝒳' and 𝒴' along iB, and let f : 𝒳 ⟶ 𝒴 be the restricted 1-morphism the universal property of the restricted target induces, AlgebraicGeometry.Stack.restrictedHom. Assume

1. pY' is locally of finite type,
2. pX' is flat and locally of finite presentation,
3. f is flat,
4. 𝒳 = ℬ ×_{ℬ'} 𝒳' and 𝒴 = ℬ ×_{ℬ'} 𝒴', i.e. PX and PY are 2-fibre products.

Then f' is flat, and pY' is flat — in the sense of Stacks 0CID — at every point of |𝒴'| in the image of |f'|.

This is AlgebraicGeometry.Stack.isFlat_ambient_of_flatDeformation and AlgebraicGeometry.Stack.isFlatAt_target_of_flatDeformation with the two 2-cells of the commutative diagram and its cube-coherence equation supplied by AlgebraicGeometry.Stack.restrictedIsoFst, AlgebraicGeometry.Stack.restrictedIsoSnd and AlgebraicGeometry.Stack.restrictedHom_coherence rather than assumed.

The two thickenings 𝒳 ⟶ 𝒳' and 𝒴 ⟶ 𝒴' of the source's diagram are not hypotheses: they are base changes of iB and so are thickenings by Stacks 0BPR.

theorem isFlat_of_flatDeformation
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hYft : AlgebraicStacks.IsLocallyOfFiniteType B S hS pY')
    (hXflat : AlgebraicStacks.IsFlat B S hS pX')
    (hXfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS pX')
    (hfflat : AlgebraicStacks.IsFlat B S hS (restrictedHom B S hS PX PY houter hcartY)) :
    AlgebraicStacks.IsFlat B S hS f' ∧
      ∀ x' : AlgebraicStacks.points B S hS 𝒳',
        AlgebraicStacks.IsFlatAt B S hS pY' (AlgebraicStacks.pointsMap B S hS f' x')

Tag 0CJC, a lemma

Tag 0CJC in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_iff_isFlat_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDeformationProperties.lean, line 286. The attribute's comment: “flat”.

For a commutative diagram of thickenings of algebraic stacks over S over a thickening iB : ℬ ⟶ ℬ' of bases, with 𝒴' ⟶ ℬ' locally of finite type, 𝒳' ⟶ ℬ' flat and locally of finite presentation and the two restricted stacks the base changes of the ambient ones along iB, the restricted 1-morphism f is flat if and only if the ambient 1-morphism f' is flat.

theorem isFlat_iff_isFlat_ambient
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : IsLocallyOfFiniteType B S hS pY')
    (hXflat : IsFlat B S hS pX')
    (hXfp : IsLocallyOfFinitePresentation B S hS pX') :
    IsFlat B S hS f ↔ IsFlat B S hS f'

AlgebraicGeometry.Stack.AlgebraicStacks.isSmooth_iff_isSmooth_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDeformationProperties.lean, line 309. The attribute's comment: “smooth”.

Under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_iff_isFlat_ambient, the restricted 1-morphism f is smooth if and only if the ambient 1-morphism f' is smooth.

theorem isSmooth_iff_isSmooth_ambient
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : IsLocallyOfFiniteType B S hS pY')
    (hXflat : IsFlat B S hS pX')
    (hXfp : IsLocallyOfFinitePresentation B S hS pX') :
    IsSmooth B S hS f ↔ IsSmooth B S hS f'

AlgebraicGeometry.Stack.AlgebraicStacks.isSyntomic_iff_isSyntomic_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDeformationProperties.lean, line 342. The attribute's comment: “syntomic”.

Under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_iff_isFlat_ambient, and assuming that syntomicity of morphisms of algebraic spaces is local on the source for the syntomic precoverage and local on the target for the fpqc precoverage, the restricted 1-morphism f passes the existential smooth-diagram test at syntomicity of morphisms of algebraic spaces if and only if the ambient 1-morphism f' does.

theorem isSyntomic_iff_isSyntomic_ambient
    [MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (k : F ⟶ G) => Space.IsSyntomic B S hS k.hom)
      (Space.Topology.precoverage.{u, u + 1} .syntomic B S hS)]
    [MorphismProperty.IsLocalAtTarget
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (k : F ⟶ G) => Space.IsSyntomic B S hS k.hom)
      (Space.Topology.precoverage.{u, u + 1} .fpqc B S hS)]
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : IsLocallyOfFiniteType B S hS pY')
    (hXflat : IsFlat B S hS pX')
    (hXfp : IsLocallyOfFinitePresentation B S hS pX') :
    Stack.HasPropertyOnSomeSmoothDiagram B S hS
        (fun _ _ k => Space.IsSyntomic B S hS k) f.hom ↔
      Stack.HasPropertyOnSomeSmoothDiagram B S hS
        (fun _ _ k => Space.IsSyntomic B S hS k) f'.hom

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyQuasiFinite_iff_isLocallyQuasiFinite_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDeformationPropertiesPointTest.lean, line 234. The attribute's comment: “locally quasi-finite”.

Stacks 0CJC, locally quasi-finite. Under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_iff_isFlat_ambient, the restricted 1-morphism f is locally quasi-finite if and only if the ambient 1-morphism f' is locally quasi-finite.

Local quasi-finiteness is by Stacks 06PU three conditions, and each is carried separately; none of them goes through the smooth-diagram reduction of AlgebraicGeometry.Stack.hasPropertyOnSomeSmoothDiagram_iff_of_flatDeformation, local quasi-finiteness not being smooth local on the source.

The quasi-DM condition is item (8) of Stacks 0CJ9, AlgebraicGeometry.Stack.isQuasiDM_inner_iff_outer, read on the morphism of thickenings whose ambient 1-morphism is f' and whose restricted one is f — the two thickenings being the base changes of iB, which are thickenings by Stacks 0BPR — and converted to the longhand reading of Stacks 04YW by .isQuasiDMWithRepresentableDiagonal_iff_isQuasiDM, the representability of a relative diagonal being free (Stacks 04XS, part (1)).

Local finite type holds for both 1-morphisms outright, with no appeal to the thickening: pX' is locally of finite presentation, hence locally of finite type (Stacks 0464), and houter identifies it with f' ≫ pY', so f' is locally of finite type by the cancellation Stacks 06U9 (.isLocallyOfFiniteType_of_comp), which needs nothing of pY'. For f it is the base change of that (Stacks 06FU), and it is not even needed: it is read off the hypothesis in the forward direction and supplied by base change in the converse.

The condition on the fibres is where the thickening enters. Spec of a field is reduced, so a field-valued point of the ambient target lifts along the thickening 𝒴 ⟶ 𝒴' by AlgebraicGeometry.Stack.exists_hom_comp_iso_of_isThickening_of_isReducedStack, and the fibre of f' over it is the fibre of f over the lift by AlgebraicGeometry.Stack.discreteTopology_points_twoFibreProduct_of_isThickening_lift; the reducedness of the field's stack is the scheme case of Stacks 04YF.

The converse is base change in one step: Stacks 06UB, .isLocallyQuasiFinite_baseChange, at the cartesian square AlgebraicGeometry.Stack.restrictedSourceSq.

theorem isLocallyQuasiFinite_iff_isLocallyQuasiFinite_ambient
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : IsLocallyOfFiniteType B S hS pY')
    (hXflat : IsFlat B S hS pX')
    (hXfp : IsLocallyOfFinitePresentation B S hS pX') :
    IsLocallyQuasiFinite B S hS f ↔ IsLocallyQuasiFinite B S hS f'

AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_iff_isMonomorphism_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDeformationPropertiesPointTest.lean, line 410. The attribute's comment: “monomorphism”.

Item (4) of Stacks 0CJC, monomorphism. Under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_iff_isFlat_ambient, the restricted 1-morphism f is a monomorphism in the sense of Stacks 04ZW if and only if the ambient 1-morphism f' is.

Being a monomorphism is representability by algebraic spaces together with a condition of Stacks 04XB at the monomorphisms of algebraic spaces. The first conjunct transfers by item (12) of Stacks 0CJ9, AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_inner_iff_outer, read on the morphism of thickenings whose ambient 1-morphism is f' and whose restricted one is f. The second is AlgebraicGeometry.Stack.AlgebraicStacks.hasRelativeProperty_iff_of_pointTest at CategoryTheory.MorphismProperty.monomorphisms, whose point test is part (6) of Stacks 0BPJ, AlgebraicGeometry.Space.mono_iff_of_cartesianSquareOfThickeningHoms, which asks no flatness; fppf-target-locality of the monomorphisms is Stacks 042D and stability under base change an instance.

Item (12) of Stacks 0CJ9 is unconditional, so nothing beyond the source's own hypotheses is carried in either direction.

theorem isMonomorphism_iff_isMonomorphism_ambient
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : Stack.IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (_hYft : IsLocallyOfFiniteType B S hS pY')
    (_hXflat : IsFlat B S hS pX')
    (hXfp : IsLocallyOfFinitePresentation B S hS pX') :
    IsMonomorphism B S hS f ↔ IsMonomorphism B S hS f'

AlgebraicGeometry.Stack.AlgebraicStacks.isFinite_iff_isFinite_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningDeformationPropertiesPointTest.lean, line 453. The attribute's comment: “finite”.

Item (10) of Stacks 0CJC, finite. Under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_iff_isFlat_ambient, the restricted 1-morphism f is finite in the sense of Stacks 03ZP read through Stacks 03YK if and only if the ambient 1-morphism f' is.

The companion of AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_iff_isMonomorphism_ambient at AlgebraicGeometry.Space.finiteMorphismProperty, whose point test is part (2) of Stacks 0BPJ, AlgebraicGeometry.Space.finiteMorphismProperty_iff_of_cartesianSquareOfThickeningHoms: a morphism of algebraic spaces is finite exactly when it is proper and locally quasi-finite (Stacks 0A4X), and both of those transfer across a cartesian square of thickenings with locally-of-finite-type horizontals, with no flatness. Stability under base change and fppf-target-locality (Stacks 0426) are both instances.

Representability of the two 1-morphisms comes from item (12) of Stacks 0CJ9 as in that theorem, and is unconditional for the same reason.

theorem isFinite_iff_isFinite_ambient
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : Stack.IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (_hYft : IsLocallyOfFiniteType B S hS pY')
    (_hXflat : IsFlat B S hS pX')
    (hXfp : IsLocallyOfFinitePresentation B S hS pX') :
    IsFinite B S hS f ↔ IsFinite B S hS f'

AlgebraicGeometry.Stack.AlgebraicStacks.isEquivalence_iff_isEquivalence_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningOpenImmersionIsomorphism.lean, line 170. The attribute's comment: “isomorphism”.

Stacks 0CJC, isomorphism. For a commutative diagram of thickenings of algebraic stacks over S over a thickening iB : ℬ ⟶ ℬ' of bases, with 𝒴' ⟶ ℬ' locally of finite type, 𝒳' ⟶ ℬ' flat and locally of finite presentation and the two restricted stacks the base changes of the ambient ones along iB, the restricted 1-morphism f is an isomorphism if and only if the ambient 1-morphism f' is.

theorem isEquivalence_iff_isEquivalence_ambient
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : IsLocallyOfFiniteType B S hS pY')
    (hXflat : IsFlat B S hS pX')
    (hXfp : IsLocallyOfFinitePresentation B S hS pX') :
    (CatFiberedInGroupoids.homFunctor f.hom).IsEquivalence ↔
      (CatFiberedInGroupoids.homFunctor f'.hom).IsEquivalence

AlgebraicGeometry.Stack.AlgebraicStacks.isOpenImmersion_iff_isOpenImmersion_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningOpenImmersionIsomorphism.lean, line 207. The attribute's comment: “open immersion”.

Stacks 0CJC, open immersion. Under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.isEquivalence_iff_isEquivalence_ambient, the restricted 1-morphism f is an open immersion if and only if the ambient 1-morphism f' is.

theorem isOpenImmersion_iff_isOpenImmersion_ambient
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : IsLocallyOfFiniteType B S hS pY')
    (hXflat : IsFlat B S hS pX')
    (hXfp : IsLocallyOfFinitePresentation B S hS pX') :
    IsOpenImmersion B S hS f ↔ IsOpenImmersion B S hS f'

AlgebraicGeometry.Stack.AlgebraicStacks.hasPropertyOnSomeSmoothDiagram_isSyntomic_iff_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningOpenImmersionIsomorphism.lean, line 236. The attribute's comment: “syntomic”.

Stacks 0CJC, syntomic. Under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.isEquivalence_iff_isEquivalence_ambient, the restricted 1-morphism f is syntomic — passes the existential smooth-diagram test of Stacks 06FN at syntomicity of morphisms of algebraic spaces, which is how the source defines a syntomic 1-morphism of algebraic stacks — if and only if the ambient 1-morphism f' is.

theorem hasPropertyOnSomeSmoothDiagram_isSyntomic_iff_ambient
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : IsLocallyOfFiniteType B S hS pY')
    (hXflat : IsFlat B S hS pX')
    (hXfp : IsLocallyOfFinitePresentation B S hS pX') :
    Stack.HasPropertyOnSomeSmoothDiagram B S hS
        (fun _ _ k => Space.IsSyntomic B S hS k) f.hom ↔
      Stack.HasPropertyOnSomeSmoothDiagram B S hS
        (fun _ _ k => Space.IsSyntomic B S hS k) f'.hom

AlgebraicGeometry.Stack.isUnramified_iff_isUnramified_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningUnramifiedEtaleIff.lean, line 41. The attribute's comment: “unramified”.

Stacks 0CJC, unramified. Under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_iff_isFlat_ambient, the restricted 1-morphism f is unramified if and only if the ambient 1-morphism f' is unramified.

theorem isUnramified_iff_isUnramified_ambient
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : AlgebraicStacks.IsLocallyOfFiniteType B S hS pY')
    (hXflat : AlgebraicStacks.IsFlat B S hS pX')
    (hXfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS pX') :
    IsUnramified B S hS f ↔ IsUnramified B S hS f'

AlgebraicGeometry.Stack.isEtale_iff_isEtale_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningUnramifiedEtaleIff.lean, line 66. The attribute's comment: “etale”.

Stacks 0CJC, étale. Under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_iff_isFlat_ambient, the restricted 1-morphism f is étale if and only if the ambient 1-morphism f' is étale.

theorem isEtale_iff_isEtale_ambient
    {iB : ℬ ⟶ ℬ'} {pX' : 𝒳' ⟶ ℬ'} {pY' : 𝒴' ⟶ ℬ'}
    {PX : Bicategory.TwoCommSq pX' iB} {PY : Bicategory.TwoCommSq pY' iB}
    {f : PX.pt ⟶ PY.pt} {f' : 𝒳' ⟶ 𝒴'}
    (hiB : IsThickening iB)
    (hcartX : Bicategory.IsTwoFibreProduct PX) (hcartY : Bicategory.IsTwoFibreProduct PY)
    (houter : f' ≫ pY' ≅ pX')
    (hrestrict : f ≫ PY.fst ≅ PX.fst ≫ f')
    (hinner : f ≫ PY.snd ≅ PX.snd)
    (hcoh : Bicategory.whiskerLeft f PY.iso.hom ≫ Bicategory.whiskerRight hinner.hom iB =
      Bicategory.whiskerRight hrestrict.hom pY' ≫
        Bicategory.whiskerLeft PX.fst houter.hom ≫ PX.iso.hom)
    (hYft : AlgebraicStacks.IsLocallyOfFiniteType B S hS pY')
    (hXflat : AlgebraicStacks.IsFlat B S hS pX')
    (hXfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS pX') :
    IsEtale B S hS f ↔ IsEtale B S hS f'

Sources

• Section 106.5, Tag 0CJA
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isFlat_ambient_of_flatDeformation · AlgebraicGeometry.Stack.isFlatAt_target_of_flatDeformation · AlgebraicGeometry.Stack.isFlat_of_flatDeformation · AlgebraicGeometry.Stack.AlgebraicStacks.isFlat_iff_isFlat_ambient · AlgebraicGeometry.Stack.AlgebraicStacks.isSmooth_iff_isSmooth_ambient · AlgebraicGeometry.Stack.AlgebraicStacks.isSyntomic_iff_isSyntomic_ambient · AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyQuasiFinite_iff_isLocallyQuasiFinite_ambient · AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_iff_isMonomorphism_ambient

Section106.6 Lifting affines#

Section 106.6 of the Stacks Project, Tag 0CJN. 9 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CJP, a remark

Tag 0CJP in the Stacks Project.

AlgebraicGeometry.Stack.EtaleSmoothLift, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesCategory.lean, line 191. The attribute's comment: “objects”.

Stacks 0CJP, the objects. For a thickening ι : 𝒳 ⟶ 𝒳' of algebraic stacks over S and a smooth 1-morphism x from an algebraic space W to 𝒳, a smooth lift of an étale open of W consists of an algebraic space U étale over W through a : U ⟶ W, an algebraic space U' containing it through i : U ⟶ U', a smooth 1-morphism x' : U' ⟶ 𝒳', and a 2-morphism filling the square with sides a, x, ι, i, x' which exhibits it as the 2-fibre product U = 𝒳 ×_{𝒳'} U'.

The last condition forces i to be a thickening, so no thickening hypothesis is imposed on it.

structure EtaleSmoothLift (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒳' : AlgebraicStacks.{u, w} B S hS} (ι : 𝒳 ⟶ 𝒳') (_hι : IsThickening ι)
    (W : AlgebraicSpaces B S hS)
    (x : (algebraicSpaceStackFunctor B S hS).obj W ⟶ 𝒳)
    (_hx : AlgebraicStacks.IsSmooth B S hS x)

AlgebraicGeometry.Stack.EtaleSmoothLift.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesCategory.lean, line 336. The attribute's comment: “morphisms”.

Stacks 0CJP, the morphisms. A morphism of smooth lifts of étale opens of W from (U, U', a, i, x', α) to (V, V', b, j, y', β) is a morphism f : U ⟶ V over W, a morphism f' : U' ⟶ V' restricting to f on U, and a 2-morphism γ : x' ⟶ y' ∘ f' filling the right-hand triangle, compatible with the two fillers in the sense that i^*γ ∘ α = f^*β.

structure Hom (ξ η : EtaleSmoothLift B S hS ι hι W x hx)

AlgebraicGeometry.Stack.EtaleSmoothLift.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesCategory.lean, line 450. The attribute's comment: “category”.

Stacks 0CJP, the category. The smooth lifts of the étale opens of W along the thickening ι, with the morphisms above, their identities and their composition.

instance instCategory : Category (EtaleSmoothLift B S hS ι hι W x hx)

AlgebraicGeometry.Stack.EtaleSmoothLift.proj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesCategory.lean, line 461. The attribute's comment: “projection”.

Stacks 0CJP, the projection. The functor sending a smooth lift to the étale open a : U ⟶ W it lies over and a morphism of smooth lifts to its component f : U ⟶ V.

def proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ Space.SpacesEtale B S hS W

AlgebraicGeometry.Stack.EtaleSmoothLift.isThickening_inclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesStack.lean, line 228. The attribute's comment: “the inclusion of an object is a thickening”.

Stacks 0CJP, the inclusion of an object is a thickening. For a smooth lift (U, U', a, i, x', α) the 2-fibre product condition U = 𝒳 ×_{𝒳'} U' exhibits i : U ⟶ U' as the base change of the thickening ι : 𝒳 ⟶ 𝒳' along x' : U' ⟶ 𝒳', so i is a thickening by Stacks 0BPR, AlgebraicGeometry.Stack.isThickening_baseChange.

This is the source's "In particular U ⊂ U' is a thickening", which Remark 0CJP asserts and StacksFrontier.AlgebraicGeometry.Stacks.LiftingAffinesCategory records only in prose; Stacks 0CJU re-uses it as "above we have already shown that there is a thickening i : U ⟶ U'". The conclusion is read in the 2-category of algebraic stacks, that is for the 1-morphism which AlgebraicGeometry.Stack.algebraicSpaceStackFunctor attaches to i; see the implementation notes for why it cannot yet be read as AlgebraicGeometry.Space.IsThickeningHom on i itself.

theorem isThickening_inclusion (ξ : EtaleSmoothLift B S hS ι hι W x hx) :
    IsThickening ((algebraicSpaceStackFunctor B S hS).map ξ.inclusion)

Tag 0CJS, a lemma

Tag 0CJS in the Stacks Project.

AlgebraicGeometry.Stack.EtaleSmoothLift.Hom.isEtale_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesEtaleAmbient.lean, line 226.

Stacks 0CJS. For a morphism (f, f', γ) of smooth lifts of étale opens of W along the thickening ι : 𝒳 ⟶ 𝒳' (Stacks 0CJP), from (U, U', a, i, x', α) to (V, V', b, j, y', β), the component f' : U' ⟶ V' between the ambient algebraic spaces is étale.

As in the source: f is étale as a morphism of the spaces-étale site of W (AlgebraicGeometry.Stack.EtaleSmoothLift.isEtale_base, Stacks 03FV), and the étale clause of Stacks 0CJC applies (AlgebraicGeometry.Stack.isEtale_of_isTwoFibreProduct_of_isThickening), because x' and y' are smooth — hence flat and locally of finite presentation, resp. locally of finite type — and U = 𝒳 ×_{𝒳'} U', V = 𝒳 ×_{𝒳'} V' are the isTwoFibreProduct fields of the two smooth lifts.

theorem isEtale_ambient (ξ η : EtaleSmoothLift B S hS ι hι W x hx) (m : ξ ⟶ η) :
    Space.IsEtale B S hS (Hom.ambient m).hom

AlgebraicGeometry.Stack.EtaleSmoothLift.isEtale_ambient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesEtaleMorphism.lean, line 126.

Stacks 0CJS. For a morphism (f, f', γ) of smooth lifts of étale opens of W along the thickening ι, the component f' : U' ⟶ V' between the ambient algebraic spaces is étale.

The hypothesis hCJC is the étale clause, item (9), of Stacks 0CJC for the thickening ι, written out for a morphism of two cartesian squares over ι whose right-hand legs come from algebraic spaces: given that the target's leg y' is locally of finite type, that the source's leg x' is flat and locally of finite presentation, that the two squares are 2-fibre products, and that (f, f', γ) is a morphism of them over 𝒳', étaleness of f gives étaleness of f'. See the implementation notes for why that clause is not available from the three formalized clauses of 0CJC.

Everything 0CJC asks for is supplied here from the two smooth lifts and the morphism between them: the squares are their isTwoFibreProduct fields, the restriction equation, the comparison 2-morphism and its coherence are the fields of the morphism, and the three conditions on x' and y' follow from smoothness of the ambient maps — local finite presentation by Stacks 0DNP, local finite type by Stacks 06Q5 on top of it, and flatness by monotonicity of the smooth-diagram criterion. Étaleness of f is isEtale_base.

theorem isEtale_ambient
    (hCJC : ∀ (U U' V V' : AlgebraicSpaces B S hS) (i : U ⟶ U') (j : V ⟶ V')
      (u : (algebraicSpaceStackFunctor B S hS).obj U ⟶ 𝒳)
      (v : (algebraicSpaceStackFunctor B S hS).obj V ⟶ 𝒳)
      (x' : (algebraicSpaceStackFunctor B S hS).obj U' ⟶ 𝒳')
      (y' : (algebraicSpaceStackFunctor B S hS).obj V' ⟶ 𝒳')
      (α : u ≫ ι ≅ (algebraicSpaceStackFunctor B S hS).map i ≫ x')
      (β : v ≫ ι ≅ (algebraicSpaceStackFunctor B S hS).map j ≫ y'),
      IsTwoFibreProduct
          (⟨(algebraicSpaceStackFunctor B S hS).obj U, u,
            (algebraicSpaceStackFunctor B S hS).map i, α⟩ : TwoCommSq ι x') →
        IsTwoFibreProduct
            (⟨(algebraicSpaceStackFunctor B S hS).obj V, v,
              (algebraicSpaceStackFunctor B S hS).map j, β⟩ : TwoCommSq ι y') →
          AlgebraicStacks.IsFlat B S hS x' →
            AlgebraicStacks.IsLocallyOfFinitePresentation B S hS x' →
              AlgebraicStacks.IsLocallyOfFiniteType B S hS y' →
                ∀ (f : U ⟶ V) (f' : U' ⟶ V')
                  (hL : u ≫ ι = (algebraicSpaceStackFunctor B S hS).map f ≫ (v ≫ ι)),
                  i ≫ f' = f ≫ j →
                    ∀ (γ : x' ⟶ (algebraicSpaceStackFunctor B S hS).map f' ≫ y')
                      (hR : (algebraicSpaceStackFunctor B S hS).map f ≫
                          ((algebraicSpaceStackFunctor B S hS).map j ≫ y') =
                        (algebraicSpaceStackFunctor B S hS).map i ≫
                          ((algebraicSpaceStackFunctor B S hS).map f' ≫ y')),
                      α.hom ≫ ((algebraicSpaceStackFunctor B S hS).map i ◁ γ) =
                          eqToHom hL ≫
                            ((algebraicSpaceStackFunctor B S hS).map f ◁ β.hom) ≫ eqToHom hR →
                        Space.IsEtale B S hS f.hom → Space.IsEtale B S hS f'.hom)
    (ξ η : EtaleSmoothLift B S hS ι hι W x hx) (m : ξ ⟶ η) :
    Space.IsEtale B S hS (Hom.ambient m).hom

Tag 0CJT, a lemma

Tag 0CJT in the Stacks Project.

AlgebraicGeometry.Stack.EtaleSmoothLift.isFiberedInGroupoids_proj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesCartesianLifts.lean, line 582.

Stacks 0CJT. The category of smooth lifts of étale opens of W along the thickening ι : 𝒳 ⟶ 𝒳' (Stacks 0CJP), projected to the spaces-étale site of W, is fibred in groupoids (Stacks 003S).

Both conditions of Stacks 003S are proved outright, with no hypothesis beyond those of Stacks 0CJP. Existence of lifts is AlgebraicGeometry.Stack.EtaleSmoothLift.exists_hom_isHomLift, the source's construction of f^*ξ from the topological invariance of the étale site along the thickening U ⊂ U'. Unique fill-ins hold for every pair of morphisms with a common target, which is what Stacks 003S asks and is stronger than the source's strongly cartesian verification for its chosen pullbacks together with its groupoid-fibre argument: for φ : η ⟶ ξ, ψ : ζ ⟶ ξ and h with φ ∘ h = ψ on the base, the fill-in is AlgebraicGeometry.Stack.EtaleSmoothLift.fillIn — its ambient component comes from fullness of the étale base change along U ⊂ U' (Stacks 05ZH, the source's Stacks 07VW), applied to the cartesian squares of φ and ψ and to their ambient components, étale by Stacks 0CJS — and it is unique by faithfulness of that base change and invertibility of the comparison 2-morphism of φ.

theorem isFiberedInGroupoids_proj :
    (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).IsFiberedInGroupoids

AlgebraicGeometry.Stack.EtaleSmoothLift.fiber_isGroupoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesFibredInGroupoids.lean, line 419. The attribute's comment: “the fibre categories are groupoids”.

Stacks 0CJT, the fibre categories are groupoids. A morphism of the fibre over an étale open U of W lies over the identity of U, so its base component is invertible; its ambient component is then invertible by hiso, and AlgebraicGeometry.Stack.EtaleSmoothLift.isIso_of_isIso_components makes the morphism itself invertible.

The hypothesis hiso is the isomorphism clause of Stacks 0CJC for the thickening ι, written out for this category: if the base component of a morphism of smooth lifts is an isomorphism then so is its ambient component. It is carried because that clause of 0CJC is not available here — see the implementation notes — and Stacks 0CJC is the tag that would discharge it.

theorem fiber_isGroupoid
    (hiso : ∀ (ζ ζ' : EtaleSmoothLift B S hS ι hι W x hx) (n : ζ ⟶ ζ'),
      IsIso (Hom.base n) → IsIso (Hom.ambient n))
    (U : Space.SpacesEtale B S hS W) :
    IsGroupoid ((proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).Fiber U)

AlgebraicGeometry.Stack.EtaleSmoothLift.isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesFibredInGroupoids.lean, line 458. The attribute's comment: “fibred in groupoids, granted the fibred-category half”.

Stacks 0CJT. The category of smooth lifts of the étale opens of W along the thickening ι, projected to the spaces-étale site of W, is fibred in groupoids. The fibre categories are groupoids by AlgebraicGeometry.Stack.EtaleSmoothLift.fiber_isGroupoid, and that together with the fibred-category half gives the conclusion by Stacks 003V.

Two hypotheses are carried. The first, hiso, is the isomorphism clause of Stacks 0CJC for ι; see AlgebraicGeometry.Stack.EtaleSmoothLift.fiber_isGroupoid. The second, hfib, is that the projection is a fibred category, which is Stacks 02XM in the source's own words, stated here as CategoryTheory.Functor.IsFibredCategory and converted to Mathlib's class by CategoryTheory.Functor.isFibredCategory_iff_isFibered: every morphism of the spaces-étale site of W has a strongly cartesian lift. It is carried because its substantive input is the topological invariance of the small étale site along an arbitrary thickening, Stacks 07VW, which is not available here — every available form of it asks the thickening to be first order — and because the source omits the strongly cartesian verification itself. Stacks 07VW is the tag that would discharge it; see the implementation notes for the full evidence. What hfib supplies is existence of strongly cartesian lifts; the uniqueness of fill-ins demanded by Stacks 003S is supplied by the groupoid-fibre half proved here.

theorem isFiberedInGroupoids
    (hiso : ∀ (ζ ζ' : EtaleSmoothLift B S hS ι hι W x hx) (n : ζ ⟶ ζ'),
      IsIso (Hom.base n) → IsIso (Hom.ambient n))
    (hfib : (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).IsFibredCategory) :
    (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).IsFiberedInGroupoids

Tag 0CJU, a lemma

Tag 0CJU in the Stacks Project.

AlgebraicGeometry.Stack.EtaleSmoothLift.isStackInGroupoids_proj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesIsStack.lean, line 148.

Stacks 0CJU. The category p : 𝒞 ⟶ W_{spaces, étale} of smooth lifts constructed in Stacks 0CJP is a stack in groupoids: the three conditions of Stacks 02ZI, for covering families indexed by an arbitrary universe t.

There is no hypothesis beyond those of Stacks 0CJP. Condition (1) is AlgebraicGeometry.Stack.EtaleSmoothLift.isFiberedInGroupoids_proj (Stacks 0CJT); conditions (2) and (3) come from AlgebraicGeometry.Stack.EtaleSmoothLift.isStack_proj through CategoryTheory.Functor.IsStack.isStackInGroupoids. See the module docstring for the proof of effectivity.

theorem isStackInGroupoids_proj :
    Functor.IsStackInGroupoids.{t} (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _)
      (Space.SpacesEtale.topology B S hS W)

AlgebraicGeometry.Stack.EtaleSmoothLift.isEtale_relation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesStack.lean, line 272. The attribute's comment: “the two legs of the relation are étale”.

Stacks 0CJU, the two legs of the relation are étale. Both s_{kk'} and t_{kk'} are ambient components of morphisms of the category of smooth lifts, so Stacks 0CJS applies to each of them.

The hypothesis hCJC is the one carried by AlgebraicGeometry.Stack.EtaleSmoothLift.isEtale_ambient: the étale clause, item (9), of Stacks 0CJC for the thickening ι, which is not available in this library.

theorem isEtale_relation
    (hCJC : ∀ (U U' V' V'' : AlgebraicSpaces B S hS) (i : U ⟶ U') (j : V' ⟶ V'')
      (u : (algebraicSpaceStackFunctor B S hS).obj U ⟶ 𝒳)
      (v : (algebraicSpaceStackFunctor B S hS).obj V' ⟶ 𝒳)
      (y : (algebraicSpaceStackFunctor B S hS).obj U' ⟶ 𝒳')
      (y' : (algebraicSpaceStackFunctor B S hS).obj V'' ⟶ 𝒳')
      (α : u ≫ ι ≅ (algebraicSpaceStackFunctor B S hS).map i ≫ y)
      (β : v ≫ ι ≅ (algebraicSpaceStackFunctor B S hS).map j ≫ y'),
      IsTwoFibreProduct
          (⟨(algebraicSpaceStackFunctor B S hS).obj U, u,
            (algebraicSpaceStackFunctor B S hS).map i, α⟩ : TwoCommSq ι y) →
        IsTwoFibreProduct
            (⟨(algebraicSpaceStackFunctor B S hS).obj V', v,
              (algebraicSpaceStackFunctor B S hS).map j, β⟩ : TwoCommSq ι y') →
          AlgebraicStacks.IsFlat B S hS y →
            AlgebraicStacks.IsLocallyOfFinitePresentation B S hS y →
              AlgebraicStacks.IsLocallyOfFiniteType B S hS y' →
                ∀ (g : U ⟶ V') (g' : U' ⟶ V'')
                  (hL : u ≫ ι = (algebraicSpaceStackFunctor B S hS).map g ≫ (v ≫ ι)),
                  i ≫ g' = g ≫ j →
                    ∀ (γ : y ⟶ (algebraicSpaceStackFunctor B S hS).map g' ≫ y')
                      (hR : (algebraicSpaceStackFunctor B S hS).map g ≫
                          ((algebraicSpaceStackFunctor B S hS).map j ≫ y') =
                        (algebraicSpaceStackFunctor B S hS).map i ≫
                          ((algebraicSpaceStackFunctor B S hS).map g' ≫ y')),
                      α.hom ≫ ((algebraicSpaceStackFunctor B S hS).map i ◁ γ) =
                          eqToHom hL ≫
                            ((algebraicSpaceStackFunctor B S hS).map g ◁ β.hom) ≫ eqToHom hR →
                        Space.IsEtale B S hS g.hom → Space.IsEtale B S hS g'.hom)
    (k k' : K) :
    Space.IsEtale B S hS (relationFst D k k').hom ∧
      Space.IsEtale B S hS (relationSnd D k k').hom

AlgebraicGeometry.Stack.EtaleSmoothLift.relation_refl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesStack.lean, line 316. The attribute's comment: “reflexivity of the relation”.

Stacks 0CJU, reflexivity of the relation. A fibre automorphism e of ξ_k which is the pullback along the diagonal Δ : U_k ⟶ U_k ×_U U_k ×_U U_k of each of the three gluing isomorphisms of the triple (k, k, k) has identity ambient component. This is the first identity of Stacks 026C read on the ambient spaces.

The hypotheses hiso and hfib are the two carried by AlgebraicGeometry.Stack.EtaleSmoothLift.isFiberedInGroupoids (Stacks 0CJT), which is where the fibred-in-groupoids hypothesis of Stacks 026C comes from.

theorem relation_refl
    (hiso : ∀ (ζ ζ' : EtaleSmoothLift B S hS ι hι W x hx) (n : ζ ⟶ ζ'),
      IsIso (Hom.base n) → IsIso (Hom.ambient n))
    (hfib : (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).IsFibredCategory)
    (k : K) {d : V k ⟶ Vijk k k k}
    {hd₁ : 𝟙 (V k) = d ≫ q₁ k k k} {hd₂ : 𝟙 (V k) = d ≫ q₂ k k k}
    {hd₃ : 𝟙 (V k) = d ≫ q₃ k k k}
    {e : D.x k ⟶ D.x k}
    (he : Functor.FibreHom (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _)
      (D.x k) (D.x k) (D.hx k) (D.hx k) e)
    (heij : Functor.IsRestrictionOf (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _) d hd₁ hd₂
      (D.wi k k k) (D.wj k k k)
      (Functor.Restriction.id _ (D.x k) (D.hx k)) (Functor.Restriction.id _ (D.x k) (D.hx k))
      (D.αij k k k) e)
    (hejk : Functor.IsRestrictionOf (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _) d hd₂ hd₃
      (D.wj k k k) (D.wk k k k)
      (Functor.Restriction.id _ (D.x k) (D.hx k)) (Functor.Restriction.id _ (D.x k) (D.hx k))
      (D.αjk k k k) e)
    (heik : Functor.IsRestrictionOf (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _) d hd₁ hd₃
      (D.wi k k k) (D.wk k k k)
      (Functor.Restriction.id _ (D.x k) (D.hx k)) (Functor.Restriction.id _ (D.x k) (D.hx k))
      (D.αik k k k) e) :
    ambientSpaceFunctor.map e = 𝟙 (D.x k).ambient

AlgebraicGeometry.Stack.EtaleSmoothLift.relation_symm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesStack.lean, line 348. The attribute's comment: “symmetry of the relation”.

Stacks 0CJU, symmetry of the relation. Over the overlap U_k ×_U U_{k'} the gluing isomorphism φ_{kk'} and the pullback σ^*φ_{k'k} of φ_{k'k} along the switching morphism have mutually inverse ambient components: this is the second identity of Stacks 026C read on the ambient spaces, and it is the source's observation that φ_{kk'}⁻¹ is the flip of φ_{k'k}.

theorem relation_symm (k k' : K) {d₁₃ : Vij k k' ⟶ Vijk k k' k}
    {hd₁ : pr₁ k k' = d₁₃ ≫ q₁ k k' k} {hd₂ : pr₂ k k' = d₁₃ ≫ q₂ k k' k}
    {hd₃ : pr₁ k k' = d₁₃ ≫ q₃ k k' k}
    {σφ : (D.xrji k k').pt ⟶ (D.xrij k k').pt}
    (hσφ : Functor.FibreHom (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _)
      (D.xrji k k').pt (D.xrij k k').pt (D.xrji k k').hpt (D.xrij k k').hpt σφ)
    (hij : Functor.IsRestrictionOf (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _) d₁₃ hd₁ hd₂
      (D.wi k k' k) (D.wj k k' k) (D.xrij k k') (D.xrji k k') (D.αij k k' k) (D.φ k k'))
    (hji : Functor.IsRestrictionOf (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _) d₁₃ hd₂ hd₃
      (D.wj k k' k) (D.wk k k' k) (D.xrji k k') (D.xrij k k') (D.αjk k k' k) σφ)
    (hik : Functor.IsRestrictionOf (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _) d₁₃ hd₁ hd₃
      (D.wi k k' k) (D.wk k k' k) (D.xrij k k') (D.xrij k k') (D.αik k k' k)
      (𝟙 (D.xrij k k').pt)) :
    ambientSpaceFunctor.map (D.φ k k') ≫ ambientSpaceFunctor.map σφ =
      𝟙 (D.xrij k k').pt.ambient

AlgebraicGeometry.Stack.EtaleSmoothLift.relation_trans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesStack.lean, line 372. The attribute's comment: “transitivity of the relation”.

Stacks 0CJU, transitivity of the relation. Over the triple overlap the cocycle condition of the descent datum says that the gluing isomorphism from ξ_k to ξ_{k''} is the composite of the ones from ξ_k to ξ_{k'} and from ξ_{k'} to ξ_{k''}; the same therefore holds of their ambient components. This is the source's transitivity of the relation.

theorem relation_trans (k k' k'' : K) :
    ambientSpaceFunctor.map (D.αik k k' k'') =
      ambientSpaceFunctor.map (D.αij k k' k'') ≫ ambientSpaceFunctor.map (D.αjk k k' k'')

Tag 0CJV, a lemma

Tag 0CJV in the Stacks Project.

AlgebraicGeometry.Stack.exists_etaleCovering_etaleSmoothLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesEtaleCovering.lean, line 125. The attribute's comment: “the covering, from the lifts over the affine members”.

Stacks 0CJV, the covering. Let ι : 𝒳 ⟶ 𝒳' be a thickening of algebraic stacks over S, let W be an algebraic space over S and let x : W ⟶ 𝒳 be a smooth 1-morphism. Let p : V₀ ⟶ W be a smooth morphism of algebraic spaces which is surjective on points, and suppose that every affine scheme of the site which is étale over W through a morphism factoring through p carries a smooth lift of that étale open along ι. Then there is a family of smooth lifts of étale opens of W along ι whose bases form an étale covering of W.

The hypothesis hlift stands in for Steps 2–4 of the source's proof, which construct the lift over one affine member of the covering: the immersion of the affine member into an affine space over the chart is a Koszul-regular immersion, its equations lift to the ambient chart of 𝒳', and the closed subspace they cut out there is smooth over 𝒳' by Stacks 0CER. The covering itself is not assumed: it is produced from p by Stacks 0CFV, and the members are shrunk to affine opens.

theorem exists_etaleCovering_etaleSmoothLift
    {𝒳 𝒳' : AlgebraicStacks.{u, w} B S hS} (ι : 𝒳 ⟶ 𝒳') (hι : IsThickening ι)
    (W : AlgebraicSpaces B S hS)
    (x : (algebraicSpaceStackFunctor B S hS).obj W ⟶ 𝒳)
    (hx : AlgebraicStacks.IsSmooth B S hS x)
    (V₀ : AlgebraicSpaces B S hS) (p : V₀ ⟶ W)
    (hp : Space.IsSmooth B S hS p.hom)
    (hpsurj : Function.Surjective (Space.pointsMap B S hS V₀.obj p.hom))
    (hlift : ∀ (T : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
      ∀ (t : yoneda.obj T ⟶ W.obj) (ht : Space.IsEtale B S hS t),
        (∃ s : yoneda.obj T ⟶ V₀.obj, s ≫ p.hom = t) →
          ∃ ξ : EtaleSmoothLift B S hS ι hι W x hx,
            ξ.base = Space.SpacesEtale.ofRepresentable B S hS W T t ht) :
    ∃ (J : Type (u + 1)) (ξ : J → EtaleSmoothLift B S hS ι hι W x hx),
      Space.IsEtaleCovering B S hS (fun j => ((ξ j).base.obj.left).obj)
        (fun j => ((ξ j).base.obj.hom).hom)

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

Stacks 0CJV. Let ι : 𝒳 ⟶ 𝒳' be a thickening of algebraic stacks over S, let W be an algebraic space over S and let x : W ⟶ 𝒳 be a smooth 1-morphism. Then there is a family of smooth lifts of étale opens of W along ι whose bases form an étale covering of W: an étale covering {W_j ⟶ W} with cartesian squares W_j = 𝒳 ×_{𝒳'} W'_j and W'_j ⟶ 𝒳' smooth.

theorem exists_isEtaleCovering_etaleSmoothLift
    {𝒳 𝒳' : AlgebraicStacks.{u, w} B S hS} (ι : 𝒳 ⟶ 𝒳') (hι : IsThickening ι)
    (W : AlgebraicSpaces B S hS)
    (x : (algebraicSpaceStackFunctor.{u, w} B S hS).obj W ⟶ 𝒳)
    (hx : AlgebraicStacks.IsSmooth B S hS x) :
    ∃ (J : Type (u + 1)) (ξ : J → EtaleSmoothLift B S hS ι hι W x hx),
      Space.IsEtaleCovering B S hS (fun j => ((ξ j).base.obj.left).obj)
        (fun j => ((ξ j).base.obj.hom).hom)

Tag 0CJW, a lemma

Tag 0CJW in the Stacks Project.

AlgebraicGeometry.Stack.exists_isEtaleCovering_ambientComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesAmbientComparison.lean, line 503.

Stacks 0CJW. Let ι : 𝒳 ⟶ 𝒳' be a thickening of algebraic stacks over S and let W = 𝒳 ×_{𝒳'} W' and W = 𝒳 ×_{𝒳'} W'' be two 2-fibre products, along x' : W' ⟶ 𝒳' and x'' : W'' ⟶ 𝒳', with W, W', W'' algebraic spaces, inclusions i : W ⟶ W', i'' : W ⟶ W'', fillers α', α'' and the vertical 1-morphisms x, x', x'' smooth. Then there are an étale covering {f'_k : W'_k ⟶ W'}, étale morphisms f''_k : W'_k ⟶ W'' and 2-isomorphisms γ_k : x'' ∘ f''_k ≅ x' ∘ f'_k such that, for each k, a single algebraic space U with e : U ⟶ W'_k and g : U ⟶ W is a pullback both of i along f'_k and of i'' along f''_k — that is, (f'_k)⁻¹(W) = (f''_k)⁻¹(W) and the two restrictions to it agree — and γ_k restricted to U is the filler α''⁻¹ ≫ α' of the given diagram over W, restricted along g.

This is exists_isEtaleCovering_ambientComparison_of_lifting at Stacks 0CHJ, AlgebraicGeometry.Space.exists_isEtaleCovering_lift_of_isSmooth_of_isThickeningHom. The smoothness of x is part of the source's hypotheses and is not used.

theorem exists_isEtaleCovering_ambientComparison
    (hι : IsThickening ι) {W W' W'' : AlgebraicSpaces B S hS}
    {x : (algebraicSpaceStackFunctor B S hS).obj W ⟶ 𝒳}
    {x' : (algebraicSpaceStackFunctor B S hS).obj W' ⟶ 𝒳'}
    {x'' : (algebraicSpaceStackFunctor B S hS).obj W'' ⟶ 𝒳'}
    (hx : AlgebraicStacks.IsSmooth B S hS x) (hx' : AlgebraicStacks.IsSmooth B S hS x')
    (hx'' : AlgebraicStacks.IsSmooth B S hS x'')
    {i : W ⟶ W'} {i'' : W ⟶ W''}
    {α' : x ≫ ι ≅ (algebraicSpaceStackFunctor B S hS).map i ≫ x'}
    {α'' : x ≫ ι ≅ (algebraicSpaceStackFunctor B S hS).map i'' ≫ x''}
    (h' : IsTwoFibreProduct (⟨(algebraicSpaceStackFunctor B S hS).obj W, x,
        (algebraicSpaceStackFunctor B S hS).map i, α'⟩ : TwoCommSq ι x'))
    (h'' : IsTwoFibreProduct (⟨(algebraicSpaceStackFunctor B S hS).obj W, x,
        (algebraicSpaceStackFunctor B S hS).map i'', α''⟩ : TwoCommSq ι x'')) :
    ∃ (K : Type (u + 1)) (V : K → AlgebraicSpaces B S hS) (f' : ∀ k, V k ⟶ W')
      (f'' : ∀ k, V k ⟶ W'')
      (γ : ∀ k, (algebraicSpaceStackFunctor B S hS).map (f'' k) ≫ x'' ≅
        (algebraicSpaceStackFunctor B S hS).map (f' k) ≫ x'),
      Space.IsEtaleCovering B S hS (fun k => (V k).obj) (fun k => (f' k).hom) ∧
      (∀ k, Space.IsEtale B S hS (f'' k).hom) ∧
      ∀ k, ∃ (U : AlgebraicSpaces B S hS) (e : U ⟶ V k) (g : U ⟶ W)
        (h₁ : IsPullback g e i (f' k)) (h₂ : IsPullback g e i'' (f'' k)),
        (algebraicSpaceStackFunctor B S hS).map e ◁ (γ k).hom =
          eqToHom (algebraicSpaceStackFunctor_map_comp_whisker_eq h₂.w.symm x'') ≫
            ((algebraicSpaceStackFunctor B S hS).map g ◁ (α''.inv ≫ α'.hom)) ≫
            eqToHom (algebraicSpaceStackFunctor_map_comp_whisker_eq h₁.w x')

Tag 0CJX, a lemma

Tag 0CJX in the Stacks Project.

AlgebraicGeometry.Stack.EtaleSmoothLift.isGerbe_proj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesGerbe.lean, line 370.

The category p : 𝒞 ⟶ W_{spaces, étale} of smooth lifts of étale opens of W along the thickening ι : 𝒳 ⟶ 𝒳' constructed in Stacks 0CJP is a gerbe (Stacks 06NZ), for covering families indexed by an arbitrary universe t in the stack condition.

theorem isGerbe_proj :
    Functor.IsGerbe.{t} (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _)
      (Space.SpacesEtale.topology B S hS W)

Tag 0CKG, a lemma

Tag 0CKG in the Stacks Project.

AlgebraicGeometry.Stack.EtaleSmoothLift.fiber_endomorphisms_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesAutomorphismAbelian.lean, line 482. The attribute's comment: “part (1): the automorphism sheaves of objects of the category of smooth lifts are abelian”.

Stacks 0CKG, part (1). Let 𝒳 ⊂ 𝒳' be a first-order thickening of algebraic stacks, W an algebraic space and x : W ⟶ 𝒳 smooth, and consider the category 𝒞 of smooth lifts of the étale opens of W along the thickening with its projection p : 𝒞 ⟶ W_{spaces, étale} (Stacks 0CJP). Then the automorphism sheaves of the objects of 𝒞 are abelian: for every étale open U of W and every object ζ of the fibre over U, the endomorphisms of ζ in that fibre commute.

theorem fiber_endomorphisms_comm (hι₁ : AlgebraicStacks.IsFirstOrderThickening B S hS ι)
    (U : Space.SpacesEtale B S hS W)
    (ζ : (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).Fiber U) (α β : ζ ⟶ ζ) :
    α ≫ β = β ≫ α

AlgebraicGeometry.Stack.EtaleSmoothLift.exists_band_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesBandQuasicoherent.lean, line 265. The attribute's comment: “part (2): the sheaf of groups 𝒢 of Stacks 0CJY is a quasi-coherent 𝒪_W-module”.

Stacks 0CKG (2). In Situation 0CJP, let 𝒳 ⊂ 𝒳' be a first order thickening. Then the sheaf of groups 𝒢 of Stacks 0CJY — the band of the gerbe p : 𝒞 ⟶ W_{spaces,étale} of smooth lifts, with its banding θ and the three clauses of 0CJY — is a quasi-coherent 𝒪_W-module: its restriction to W_étale (Stacks 03G1) underlies a quasi-coherent 𝒪_W-module M.

The gerbe inputs are proved (Stacks 0CJU, 0CJX) and so is the commutativity of the automorphism groups (part (1)); nothing is assumed beyond Situation 0CJP and the first order thickening.

theorem exists_band_isQuasicoherent (hι₁ : AlgebraicStacks.IsFirstOrderThickening B S hS ι) :
               haveI : (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).IsFibered :=
        isFiberedInGroupoids_proj.isFibered
      haveI : ∀ U, IsGroupoid ((proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).Fiber U) :=
        isFiberedInGroupoids_proj.fiber_isGroupoid
      ∃ (𝒢 : Sheaf (Space.SpacesEtale.topology B S hS W) CommGrpCat.{u + 1})
        (θ : ∀ (U : Space.SpacesEtale B S hS W)
          (y : (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).Fiber U),
          (Over.forget U).op ⋙ 𝒢.obj ⋙ forget CommGrpCat.{u + 1} ≅
            (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).morPresheaf y y ⋙
              uliftFunctor.{u + 1, u + 1}),
        (∀ (U : Space.SpacesEtale B S hS W)
            (y : (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).Fiber U) (g : Over U)
            (a b : 𝒢.obj.obj (op g.left)),
            ((θ U y).hom.app (op g) (a * b)).down =
              ((θ U y).hom.app (op g) a).down ≫ ((θ U y).hom.app (op g) b).down) ∧
          (∀ (U : Space.SpacesEtale B S hS W)
              (y z : (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).Fiber U) (φ : y ⟶ z)
              (g : Over U) (a : 𝒢.obj.obj (op g.left)),
            ((θ U z).hom.app (op g) a).down =
              Functor.pullbackFiberHom (CategoryTheory.inv φ) g.hom ≫
                ((θ U y).hom.app (op g) a).down ≫ Functor.pullbackFiberHom φ g.hom) ∧
          (∀ (U : Space.SpacesEtale B S hS W)
            (y : (proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).Fiber U) (g : Over U)
            (a : 𝒢.obj.obj (op g.left)),
            ((θ U y).hom.app (op g) a).down =
              (Functor.pullbackFiberIdIso
                  ((proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).pullbackFiber y g.hom)).inv ≫
                ((θ g.left ((proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).pullbackFiber y
                    g.hom)).hom.app (op (Over.mk (𝟙 g.left))) a).down ≫
                  (Functor.pullbackFiberIdIso
                    ((proj : EtaleSmoothLift B S hS ι hι W x hx ⥤ _).pullbackFiber y
                      g.hom)).hom) ∧
          ∃ M : SheafOfModules.{u + 1} (Space.structureRingSheaf B S hS W),
            M.IsQuasicoherentOnSite ∧
              Nonempty ((Space.spacesEtaleAbelianRestriction B S hS W).obj
                ((sheafCompose _ commGroupAddCommGroupEquivalence.{u + 1}.functor).obj 𝒢) ≅
                (SheafOfModules.toSheaf _).obj M)

Tag 0CKI, a proposition

Tag 0CKI in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_smooth_affine_lift_of_isFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LiftingAffinesEmertonLift.lean, line 56.

Stacks 0CKI (Emerton). Let ι : 𝒳 ⟶ 𝒳' be a first order thickening of algebraic stacks, let W be affine and let x : W ⟶ 𝒳 be smooth. Then there are an affine W', a morphism i : W ⟶ W' and a smooth x' : W' ⟶ 𝒳' such that the square x ≫ ι ≅ i ≫ x' is 2-cartesian, i.e. W = 𝒳 ×_{𝒳'} W'.

Here W and W' are algebraic spaces that are affine, that is, representable by affine schemes, viewed as algebraic stacks through algebraicSpaceStackFunctor.

theorem exists_smooth_affine_lift_of_isFirstOrderThickening {𝒳 𝒳' : AlgebraicStacks.{u, w} B S hS}
    {ι : 𝒳 ⟶ 𝒳'} (hι₁ : IsFirstOrderThickening B S hS ι) (W : AlgebraicSpaces B S hS)
    (hW : Space.IsAffineSpace B S hS W.obj) (x : (algebraicSpaceStackFunctor B S hS).obj W ⟶ 𝒳)
    (hx : IsSmooth B S hS x) :
    ∃ (W' : AlgebraicSpaces B S hS) (i : W ⟶ W')
      (x' : (algebraicSpaceStackFunctor B S hS).obj W' ⟶ 𝒳')
      (α : x ≫ ι ≅ (algebraicSpaceStackFunctor B S hS).map i ≫ x'),
      IsSmooth B S hS x' ∧
        Nonempty (IsTwoFibreProduct
          (⟨(algebraicSpaceStackFunctor B S hS).obj W, x,
            (algebraicSpaceStackFunctor B S hS).map i, α⟩ : TwoCommSq ι x')) ∧
        Space.IsAffineSpace B S hS W'.obj

Sources

• Section 106.6, Tag 0CJN
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.EtaleSmoothLift · AlgebraicGeometry.Stack.EtaleSmoothLift.Hom · AlgebraicGeometry.Stack.EtaleSmoothLift.instCategory · AlgebraicGeometry.Stack.EtaleSmoothLift.proj · AlgebraicGeometry.Stack.EtaleSmoothLift.isThickening_inclusion · AlgebraicGeometry.Stack.EtaleSmoothLift.Hom.isEtale_ambient · AlgebraicGeometry.Stack.EtaleSmoothLift.isEtale_ambient · AlgebraicGeometry.Stack.EtaleSmoothLift.isFiberedInGroupoids_proj

Section106.7 Infinitesimal deformations#

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

Tag 0DNR, a lemma

Tag 0DNR in the Stacks Project.

Deformation.Artin.existsUnique_infFlatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/FlatBaseChange.lean, line 205.

Stacks 0DNR. Let 𝒳 be a category fibred in groupoids over the big fppf site of S, let A → C be a flat homomorphism of S-algebras, let x be an object of 𝒳 over Spec A and let y = x|_{Spec C}. Then the infinitesimal automorphisms of the trivial deformations of x and of y satisfy Inf_x(M) ⊗_A C = Inf_y(C ⊗_A M): there is a unique C-linear isomorphism C ⊗_A Inf_x(M) ≅ Inf_y(N), for N a site module identified with C ⊗_A M, which sends c ⊗ θ to the base change of θ scaled by c.

The identification of Inf_x with Hom_A(Q, -), of Inf_y with Hom_C(QC, -), and of QC with C ⊗_A Q, together with the finite presentation of Q, are hypotheses: they are the inputs the source takes from Stacks 0617, 05ZF and 05ZC, which this development does not have in that combined form. See Deformation.Artin.InfHomRepresentation. What is proved here is the flat base change itself, by Stacks 087R.

public theorem existsUnique_infFlatBaseChange
    (D : InfHomRepresentation A C B S hS toS hA toSC hC p x y hx hy hp Dx Dy Q QC)
    (M : SiteModule A B) (N : SiteModule C B)
    (hMN : (C ⊗[A] (M.obj : Type u)) ≃ₗ[C] (N.obj : Type u)) :
    ∃ e : (C ⊗[A] (Dx.functor.obj M : Type w)) ≃ₗ[C] (Dy.functor.obj N : Type w),
      (∀ (c a : C) (θ : (Dx.functor.obj M : Type w)) (q : Q),
        D.homRepY N (e (c ⊗ₜ[A] θ)) (D.baseChangeQ (a ⊗ₜ[A] q)) =
          hMN ((a * c) ⊗ₜ[A] D.homRepX M θ q)) ∧
      ∀ e' : (C ⊗[A] (Dx.functor.obj M : Type w)) ≃ₗ[C] (Dy.functor.obj N : Type w),
        (∀ (c a : C) (θ : (Dx.functor.obj M : Type w)) (q : Q),
          D.homRepY N (e' (c ⊗ₜ[A] θ)) (D.baseChangeQ (a ⊗ₜ[A] q)) =
            hMN ((a * c) ⊗ₜ[A] D.homRepX M θ q)) → e' = e

Deformation.Artin.exists_infFlatBaseChange_of_inertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/InfFlatBaseChangeStack.lean, line 322.

Stacks 0DNR: infinitesimal automorphisms commute with flat base change. Let 𝒳 be an algebraic stack over S whose inertia ℐ_𝒳 ⟶ 𝒳 is locally of finite presentation, let A → C be a flat homomorphism of S-algebras, let x be an object of 𝒳 over Spec A and let y = x|_{Spec C}, exhibited by an arrow φ : y ⟶ x over Spec C ⟶ Spec A. Then for every A-module M there is a C-linear isomorphism C ⊗_A Inf_x(M) ≅ Inf_y(C ⊗_A M), sending 1 ⊗ θ to the image of θ under the map Inf_x(M) ⟶ Inf_y(C ⊗_A M) of Stacks 07YA (restriction of infinitesimal automorphisms along the arrow of trivial deformations over Spec C[C ⊗_A M] ⟶ Spec A[M]). The modules Inf_x, Inf_y are arbitrary realizations of the functors of Stacks 07Y9.

theorem exists_infFlatBaseChange_of_inertia (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hI : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS
      (inertiaProjectionAlgebraicStacks B S hS 𝒳))
    (A C : Type u) [CommRing A] [CommRing C] [Algebra A C] [Module.Flat A C]
    (toS : Spec (.of A) ⟶ S) (hA : B.Contains (Spec (.of A)))
    (toSC : Spec (.of C) ⟶ S) (hC : B.Contains (Spec (.of C)))
    (hf : Spec.map (CommRingCat.ofHom (algebraMap A C)) ≫ toS = toSC)
    (x y : 𝒳.val.val.obj) (hx : 𝒳.val.val.p.obj x = algebraOver A B S hS toS hA)
    (hy : 𝒳.val.val.p.obj y = algebraOver C B S hS toSC hC) (φ : y ⟶ x)
    (hφ : 𝒳.val.val.p.IsHomLift
      (algebraOverMapOfRingHom (algebraMap A C) B S hS toS toSC hA hC hf) φ)
    (Dx : InfinitesimalAutomorphismFunctorData A B S hS toS hA 𝒳.val.val.p x hx
      𝒳.val.isFiberedInGroupoids)
    (Dy : InfinitesimalAutomorphismFunctorData C B S hS toSC hC 𝒳.val.val.p y hy
      𝒳.val.isFiberedInGroupoids)
    (M : SiteModule A B) :
    ∃ e : (C ⊗[A] (Dx.functor.obj M : Type u)) ≃ₗ[C]
        (Dy.functor.obj ⟨ModuleCat.of C (C ⊗[A] M.obj), isSiteModule_tensor hC M⟩ : Type u),
      ∀ t : (Dx.functor.obj M : Type u), e ((1 : C) ⊗ₜ t) =
        infBaseChangeMap (algebraMap A C) B S hS toS hA toSC hC hf 𝒳.val.val.p x y hx hy φ hφ
          𝒳.val.isFiberedInGroupoids Dx Dy (tensorCoeff (A₁ := C) M.obj) t

Tag 0DNS, a lemma

Tag 0DNS in the Stacks Project.

Deformation.Artin.LiftClassSheaf.isSheaf_liftClassPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/LiftClassSheafCondition.lean, line 149.

Stacks 0DNS. For an algebraic stack over a base scheme whose inertia is locally of finite presentation, and a deformation situation (A' → A, x), the functor sending an affine A'-algebra B' to the isomorphism classes of lifts of x|_{B' ⊗_{A'} A} to B' is a sheaf on the big affine fppf site of Spec A'.

theorem isSheaf_liftClassPresheaf
    (hI : Stack.AlgebraicStacks.IsLocallyOfFinitePresentation B S hS
      (Stack.relativeInertiaProjection B S hS (Stack.structureMorphism B S hS 𝒳)))
    (hi : IsDeformationSituation (ringMap B S hS i).hom) (P : LiftClassPresheaf B S hS 𝒳 i x hx) :
    Presheaf.IsSheaf ((BigAffineFppf.topology B S hS).over U') P.presheaf

Tag 0DNT, a lemma

Tag 0DNT in the Stacks Project.

Deformation.Artin.exists_tangentFlatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/TangentFlatBaseChangeStack.lean, line 587.

Stacks 0DNT: tangent modules of an algebraic stack commute with flat base change. Let 𝒳 be an algebraic stack over S with 𝒳 → S locally of finite presentation, A → C a flat homomorphism of S-algebras, x an object of 𝒳 over Spec A and y = x|_{Spec C}, exhibited by a strongly cartesian arrow β : y ⟶ x over Spec C ⟶ Spec A. Then for every A-module M there is a C-linear isomorphism C ⊗_A T_x(M) ≅ T_y(C ⊗_A M), the one induced by pulling lifts back along Spec C[C ⊗_A M] ⟶ Spec A[M]: the ring map r : A[M] → C[C ⊗_A M] is A → C on A and m ↦ 1 ⊗ m on M, and 1 ⊗ t is sent to the class of the cartesian pullback along Spec r of a lift representing t. The tangent modules are arbitrary realizations of the tangent functors of Stacks 07Y9.

theorem exists_tangentFlatBaseChange
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (f : 𝒳 ⟶ Stack.schemeFibredCategory B S hS (Over.mk (𝟙 (B.obj hS))))
    (hf : HasPropertyOnEverySmoothDiagram B S hS
      (fun _ _ g => Space.IsLocallyOfFinitePresentation B S hS g) f)
    (A C : Type u) [CommRing A] [CommRing C] [Algebra A C] [Module.Flat A C]
    (toS : Spec (.of A) ⟶ S) (hA : B.Contains (Spec (.of A)))
    (toS' : Spec (.of C) ⟶ S) (hC : B.Contains (Spec (.of C)))
    (x y : 𝒳.val.obj) (hx : 𝒳.val.p.obj x = algebraOver A B S hS toS hA)
    (hy : 𝒳.val.p.obj y = algebraOver C B S hS toS' hC)
    (b : algebraOver C B S hS toS' hC ⟶ algebraOver A B S hS toS hA)
    (hb : (BigFppfOver.toScheme B S hS).map b = Spec.map (CommRingCat.ofHom (algebraMap A C)))
    (β : y ⟶ x) (hβ : 𝒳.val.p.IsStronglyCartesian b β)
    (M : SiteModule A B) (hMC : IsSiteModule C B (ModuleCat.of C (C ⊗[A] M.obj)))
    (Tx : TangentFunctorData A B S hS toS hA 𝒳.val.p x hx)
    (Ty : TangentFunctorData C B S hS toS' hC 𝒳.val.p y hy) :
    let N : SiteModule C B := ⟨ModuleCat.of C (C ⊗[A] M.obj), hMC⟩
    ∃ (r : squareZeroRing A M.obj ⟶ squareZeroRing C N.obj)
      (g : squareZeroOver C B S hS toS' N ⟶ squareZeroOver A B S hS toS M)
      (e : (C ⊗[A] (Tx.functor.obj M : Type _)) ≃ₗ[C] (Ty.functor.obj N : Type _)),
      ((BigFppfOver.toScheme B S hS).map g = Spec.map r) ∧
      (∀ z : TrivSqZeroExt A M.obj,
        (r.hom z).fst = algebraMap A C z.fst ∧ (r.hom z).snd = (1 : C) ⊗ₜ[A] z.snd) ∧
      (∀ t : (Tx.functor.obj M : Type _),
        ∃ (a : (Under.post 𝒳.val.p).Fiber
            (Under.mk (eqToHom hx ≫ squareZeroArrow A B S hS toS hA M)))
          (c : (Under.post 𝒳.val.p).Fiber
            (Under.mk (eqToHom hy ≫ squareZeroArrow C B S hS toS' hC N))),
          Quotient.mk _ a = Tx.liftEquiv M t ∧
          Quotient.mk _ c = Ty.liftEquiv N (e ((1 : C) ⊗ₜ[A] t)) ∧
          ∃ φ : c.1.right ⟶ a.1.right,
            𝒳.val.p.IsStronglyCartesian g φ ∧ c.1.hom ≫ φ = β ≫ a.1.hom)

Tag 0DNU, a lemma

Tag 0DNU in the Stacks Project.

AlgebraicGeometry.Stack.exists_lift_of_fppf_lift_of_isDeformationSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GroupoidLift/StackFppfLift.lean, line 333.

Stacks 0DNU. Let 𝒳 be an algebraic stack over S whose structure morphism is locally of finite presentation, and let (A' → A, x) be a deformation situation, A' → A being Γ(U') → Γ(U) for the closed immersion i : U ⟶ U' of affines and x an object over U. If there are a faithfully flat finitely presented A'-algebra B' = Γ(V') and an object y' of 𝒳 over B' lifting the restriction y of x to B' ⊗_{A'} A = Γ(V), then there is an object x' over A' lifting x.

theorem exists_lift_of_fppf_lift_of_isDeformationSituation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (f : 𝒳 ⟶ schemeFibredCategory B S hS (Over.mk (𝟙 (B.obj hS))))
    (hf : HasPropertyOnEverySmoothDiagram B S hS
      (fun _ _ g => Space.IsLocallyOfFinitePresentation B S hS g) f)
    (U U' V V' : BigAffineFppf B S hS)
    (i : U ⟶ U') (j : V ⟶ U) (l : V ⟶ V') (k : V' ⟶ U')
    (hsq : j ≫ i = l ≫ k)
    (hpb : IsPushout
      ((BigAffineFppf.toScheme B S hS).map i).appTop
      ((BigAffineFppf.toScheme B S hS).map k).appTop
      ((BigAffineFppf.toScheme B S hS).map j).appTop
      ((BigAffineFppf.toScheme B S hS).map l).appTop)
    (hi : Deformation.Artin.IsDeformationSituation
      ((BigAffineFppf.toScheme B S hS).map i).appTop.hom)
    (hff : ((BigAffineFppf.toScheme B S hS).map k).appTop.hom.FaithfullyFlat)
    (hfp : ((BigAffineFppf.toScheme B S hS).map k).appTop.hom.FinitePresentation)
    (x : 𝒳.val.obj)
    (hx : 𝒳.val.p.obj x = (BigAffineFppf.inclusion B S hS).obj U)
    (y : 𝒳.val.obj)
    (_hy : 𝒳.val.p.obj y = (BigAffineFppf.inclusion B S hS).obj V)
    (α : y ⟶ x)
    (hα : 𝒳.val.p.IsStronglyCartesian ((BigAffineFppf.inclusion B S hS).map j) α)
    (hlift : ∃ (y' : 𝒳.val.obj)
      (_hy' : 𝒳.val.p.obj y' = (BigAffineFppf.inclusion B S hS).obj V')
      (β : y ⟶ y'), 𝒳.val.p.IsStronglyCartesian ((BigAffineFppf.inclusion B S hS).map l) β) :
    ∃ (x' : 𝒳.val.obj)
      (_hx' : 𝒳.val.p.obj x' = (BigAffineFppf.inclusion B S hS).obj U')
      (β : x ⟶ x'), 𝒳.val.p.IsStronglyCartesian ((BigAffineFppf.inclusion B S hS).map i) β

Sources

• Section 106.7, Tag 0DNQ
• AxiomMath/Stacks at 5ed82d14

LeanDeformation.Artin.existsUnique_infFlatBaseChange · Deformation.Artin.exists_infFlatBaseChange_of_inertia · Deformation.Artin.LiftClassSheaf.isSheaf_liftClassPresheaf · Deformation.Artin.exists_tangentFlatBaseChange · AlgebraicGeometry.Stack.exists_lift_of_fppf_lift_of_isDeformationSituation

Section106.8 Formally smooth morphisms#

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

Tag 0DNW, a definition

Tag 0DNW 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 attribute's comment: “formal smoothness of a morphism of algebraic stacks is formal smoothness on”.

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 0DNX, an equation

Tag 0DNX in the Stacks Project.

AlgebraicGeometry.Stack.InfinitesimalLiftingDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InfinitesimalLifting.lean, line 52.

The solid part of a 2-commutative infinitesimal lifting diagram for a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S: a first-order thickening of affine objects of the big fppf site of S, a point of 𝒳 over the smaller one, a point of 𝒴 over the larger one, and a 2-morphism witnessing that the square 2-commutes.

structure InfinitesimalLiftingDiagram
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS)
    (f : 𝒳 ⟶ 𝒴)

Tag 0DNY, a lemma

Tag 0DNY in the Stacks Project.

AlgebraicGeometry.Stack.isFormallySmoothOnObjects_iff_nonempty_dottedArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FormallySmoothDottedArrows.lean, line 638.

Stacks 0DNY. A 1-morphism of algebraic stacks over S is formally smooth exactly when every infinitesimal lifting diagram for it — the solid diagram 0DNX, i.e. a first-order thickening of affine objects of the site together with a point of the source over the smaller one, a point of the target over the larger one and a 2-morphism witnessing 2-commutativity — admits a dotted arrow, i.e. the category of dotted arrows of Stacks 0H18 for that square is nonempty.

theorem isFormallySmoothOnObjects_iff_nonempty_dottedArrow
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    IsFormallySmoothOnObjects B S hS 𝒳.1 𝒴.1 f.hom ↔
      ∀ d : InfinitesimalLiftingDiagram B S hS 𝒳 𝒴 f,
        Nonempty (DottedArrow d.x d.j f.hom d.y d.γ)

Tag 0H1I, a lemma

Tag 0H1I 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. The attribute's comment: “base change of a formally smooth morphism of algebraic stacks is formally smooth”.

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 0H1J, a lemma

Tag 0H1J 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. The attribute's comment: “the case of algebraic stacks, formally smooth being formally smooth on objects”.

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 0H1K, a lemma

Tag 0H1K in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_iff_formallySmooth_terminalFrom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Criteria/FormallySmoothBaseChange.lean, line 224.

Stacks 0H1K. A 1-morphism of categories fibred in groupoids over the big fppf category of S which is representable by algebraic spaces is formally smooth on objects exactly when, for every scheme-valued point U of the target, every algebraic space representing the base change of it along that point is formally smooth over U.

This is Stacks 06D3, AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_iff_isRelativelyFormallySmooth, with the structural morphism of the representing space read over U rather than over S, which is AlgebraicGeometry.BigFppfOver.isRelativelyFormallySmooth_iff_formallySmooth_terminalFrom.

theorem isFormallySmoothOnObjects_iff_formallySmooth_terminalFrom (p : 𝒳 ⟶ 𝒴)
    (hp : Stack.IsRepresentableByAlgebraicSpaces B S hS p.hom) :
    Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒴 p ↔
      ∀ (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 p))
            (presheafOfCategories (F ⋙ typeToCat)).p) →
          Space.FormallySmooth (terminal.from F)

Tag 0DNZ, a lemma

Tag 0DNZ in the Stacks Project.

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

Stacks 0DNZ. Let T ⟶ T' be a first-order thickening of affine schemes, 𝒳 an algebraic stack whose structure morphism f : 𝒳 ⟶ T' is smooth, and x : T ⟶ 𝒳 a morphism over T' (the 2-morphism γ : j ⟶ x ≫ f, with j : T ⟶ T' the morphism of represented categories induced by the thickening). Then there is a morphism x' : T' ⟶ 𝒳 over T' with x'|_T ≅ x: a dotted arrow for the square (x, j, f, 𝟙).

theorem exists_dottedArrow_of_isSmooth_of_isFirstOrderThickening
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (T T' : BigFppfOver B S hS)
    (hT : IsAffine ((BigFppfOver.toScheme B S hS).obj T))
    (hT' : IsAffine ((BigFppfOver.toScheme B S hS).obj T'))
    (i : T ⟶ T')
    (hi : Stacks.Thickenings.IsFirstOrderThickening (B.inclusion.map i.left))
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (f : 𝒳 ⟶ schemeFibredCategory B S hS T')
    (hf : HasPropertyOnSomeSmoothDiagram B S hS
      (fun {X Y} (g : X ⟶ Y) => Space.IsSmooth B S hS g) f)
    (j : schemeFibredCategory B S hS T ⟶ schemeFibredCategory B S hS T')
    (hj : j.hom.toFunctor = Over.map i)
    (x : schemeFibredCategory B S hS T ⟶ 𝒳)
    (γ : (j ≫ 𝟙 _) ⟶ (x ≫ f)) :
    Nonempty (DottedArrow x j f (𝟙 _) γ)

Tag 0DP0, a lemma

Tag 0DP0 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isSmooth_iff_isLocallyOfFinitePresentation_and_isFormallySmoothOnObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SmoothFormallySmooth.lean, line 343. References: EGA 0 (19.0.1), “more general”.

Stacks 0DP0 (infinitesimal lifting criterion). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is smooth if and only if it is locally of finite presentation and formally smooth, formal smoothness of a 1-morphism of algebraic stacks being formal smoothness on objects (Stacks 0DNW).

theorem AlgebraicStacks.isSmooth_iff_isLocallyOfFinitePresentation_and_isFormallySmoothOnObjects
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    AlgebraicStacks.IsSmooth B S hS f ↔
      AlgebraicStacks.IsLocallyOfFinitePresentation B S hS f ∧
        IsFormallySmoothOnObjects B S hS 𝒳.1 𝒴.1 f.hom

Sources

• Section 106.8, Tag 0DNV
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.IsFormallySmoothOnObjects · AlgebraicGeometry.Stack.InfinitesimalLiftingDiagram · AlgebraicGeometry.Stack.isFormallySmoothOnObjects_iff_nonempty_dottedArrow · AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_baseChange · AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_comp · AlgebraicGeometry.BigFppfOver.isFormallySmoothOnObjects_iff_formallySmooth_terminalFrom · AlgebraicGeometry.Stack.exists_dottedArrow_of_isSmooth_of_isFirstOrderThickening · AlgebraicGeometry.Stack.AlgebraicStacks.isSmooth_iff_isLocallyOfFinitePresentation_and_isFormallySmoothOnObjects

Section106.9 Blowing up and flatness#

Section 106.9 of the Stacks Project, Tag 0CQ3. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CQ4, a lemma

Tag 0CQ4 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.exists_admissibleBlowup_flat_finitePresentation_closedSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FlatteningByBlowupStack.lean, line 42.

Flattening by blowing up. Let f : 𝒳 ⟶ Y be a 1-morphism from an algebraic stack to an algebraic space and V ⊆ Y an open subspace, with (1) Y quasi-compact and quasi-separated, (2) f of finite type and quasi-separated, (3) V quasi-compact and (4) 𝒳_V ⟶ V flat and locally of finite presentation. Then there are a V-admissible blowup b : Y' ⟶ Y and a closed substack 𝒳' ⊆ 𝒳_{Y'} containing every object of 𝒳_{Y'} over b⁻¹V (so 𝒳'_V = 𝒳_V, b being an isomorphism over V) such that 𝒳' ⟶ Y' is flat and of finite presentation.

theorem exists_admissibleBlowup_flat_finitePresentation_closedSubstack
    {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hY : IsAlgebraicSpace B S hS Y)
    (hYqc : Space.IsQuasiCompactSpace B S hS Y)
    (hYqs : Space.IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    {𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS Y hY)
    (hft : IsFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f)
    (V : Subfunctor Y) (hV : Space.IsOpenSubspace B S hS V)
    (hVqc : Space.IsQuasiCompactSpace B S hS V.toFunctor)
    (hflat : IsFlat B S hS
      (twoFibreProductSquare B S hS (algebraicSpaceStackMap.{u, w} B S hS hV.1 hY V.ι) f).fst)
    (hlfp : IsLocallyOfFinitePresentation B S hS
      (twoFibreProductSquare B S hS (algebraicSpaceStackMap.{u, w} B S hS hV.1 hY V.ι) f).fst) :
    ∃ (Y' : AlgebraicSpaces B S hS) (b : Y' ⟶ ⟨Y, hY⟩),
      Space.IsAdmissibleBlowup B S hS ⟨V, hV⟩ b ∧
        ∃ P : ObjectProperty (twoFibreProductSquare B S hS
            (algebraicSpaceStackMap.{u, w} B S hS Y'.2 hY b.hom) f).pt.val.val.obj,
          IsClosedSubstack _ P ∧
          (∀ x, ((twoFibreProductSquare B S hS
              (algebraicSpaceStackMap.{u, w} B S hS Y'.2 hY b.hom) f).fst.hom.hom.obj
                x).fiber.as ∈ (V.preimage b.hom).obj (Opposite.op ((twoFibreProductSquare B S hS
                  (algebraicSpaceStackMap.{u, w} B S hS Y'.2 hY b.hom) f).fst.hom.hom.obj
                    x).base) →
            P x) ∧
          ∀ hP : IsAlgebraicStack.{u, w} B S hS (fullSubcategoryBased _ P),
            IsFlat B S hS (fullSubcategoryInclusion _ P hP ≫ (twoFibreProductSquare B S hS
              (algebraicSpaceStackMap.{u, w} B S hS Y'.2 hY b.hom) f).fst) ∧
            IsFinitePresentation B S hS (fullSubcategoryInclusion _ P hP ≫
              (twoFibreProductSquare B S hS
                (algebraicSpaceStackMap.{u, w} B S hS Y'.2 hY b.hom) f).fst)

Sources

• Section 106.9, Tag 0CQ3
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.AlgebraicStacks.exists_admissibleBlowup_flat_finitePresentation_closedSubstack

Section106.10 Chow's lemma for algebraic stacks#

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

Tag 0CQ6, a lemma

Tag 0CQ6 in the Stacks Project.

AlgebraicGeometry.Stack.exists_finite_surjective_zariskiLocal_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChowFiniteCoverFactorizationUnconditional.lean, line 61. The attribute's comment: “Chow's lemma for algebraic stacks: a flat surjection locally of finite presentation onto a quasi-compact open of a qcqs algebraic space splits Zariski locally after a finite surjective base change.”.

[Stacks, Tag 0CQ6]. Let Y be a quasi-compact and quasi-separated algebraic space over S, let V ⊆ Y be a quasi-compact open subspace and let f : 𝒳 ⟶ V be a surjective and flat 1-morphism of algebraic stacks which is locally of finite presentation. Then there is a finite surjective morphism g : Y' ⟶ Y of algebraic spaces such that V' = g⁻¹(V) ⟶ V factors Zariski locally through f: there are open immersions ι j : W j ⟶ Y' contained in g⁻¹(V) (they factor through V over g, by q j) whose images cover g⁻¹(V), and 1-morphisms x j : W j ⟶ 𝒳 with x j ≫ f 2-isomorphic to q j.

The proof is the source's second paragraph: [Stacks, Proposition 09YC] (in the form AlgebraicGeometry.Space.existsFiniteSurjectiveSchemeCover_of_isQuasiCompactSpace) gives a finite surjective π : h_{Y₁} ⟶ Y from a scheme of the site; Y₁ is quasi-compact and quasi-separated, π⁻¹(V) is a quasi-compact open of h_{Y₁}, and the base change of f to it is again surjective, flat and locally of finite presentation. The scheme case, AlgebraicGeometry.Stack.exists_finite_surjective_zariskiLocal_factorization_of_yoneda ([Stacks, Tag 0CP0] and [Stacks, Tag 0CNY]), then gives a finite surjective Y' ⟶ h_{Y₁}, and its composite with π is the required g.

theorem exists_finite_surjective_zariskiLocal_factorization
    {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hY : IsAlgebraicSpace B S hS Y)
    (hYqc : Space.IsQuasiCompactSpace B S hS Y)
    (hYqs : Space.IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    (V : Subfunctor Y) (hV : Space.IsOpenSubspace B S hS V)
    (hVqc : Space.IsQuasiCompactSpace B S hS V.toFunctor)
    {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS V.toFunctor hV.1)
    (hfs : IsSurjective B S hS f) (hff : AlgebraicStacks.IsFlat B S hS f)
    (hfl : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS f) :
    ∃ (Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Y') (g : Y' ⟶ Y),
      Space.IsFinite B S hS g ∧ Space.IsSurjective B S hS g ∧
      ∃ (J : Type u) (W : J → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
        (hW : ∀ j, IsAlgebraicSpace B S hS (W j)) (ι : ∀ j, W j ⟶ Y')
        (q : ∀ j, W j ⟶ V.toFunctor)
        (x : ∀ j, algebraicSpaceStack.{u, w} B S hS (W j) (hW j) ⟶ 𝒳),
        (∀ j, Space.IsOpenImmersion B S hS (ι j)) ∧ (∀ j, ι j ≫ g = q j ≫ V.ι) ∧
        (∀ y : Space.points B S hS Y',
          Space.pointsMap B S hS Y' g y ∈ Set.range (Space.pointsMap B S hS V.toFunctor V.ι) →
            ∃ j, y ∈ Set.range (Space.pointsMap B S hS (W j) (ι j))) ∧
        ∀ j, Nonempty (x j ≫ f ≅ algebraicSpaceStackMap.{u, w} B S hS (hW j) hV.1 (q j))

Tag 0CQ7, a lemma

Tag 0CQ7 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.hasProperCompactifiableCover_of_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/C1575Private/ChowGerbeProperCover.lean, line 202.

[Stacks, Tag 0CQ7]. Let f : 𝒳 ⟶ Y be a 1-morphism from an algebraic stack to an algebraic space and V ⊆ Y an open subspace. Assume that f is separated and of finite type, that Y is quasi-compact and quasi-separated, that V is quasi-compact, and that 𝒳_V is a gerbe over V. Then there are algebraic spaces Z, Z̄, an open immersion j : Z ⟶ Z̄, a proper ḡ : Z̄ ⟶ Y and a proper h : Z ⟶ 𝒳 with h ≫ f 2-isomorphic to g = j ≫ ḡ, such that |V| is contained in the image of |g|.

theorem hasProperCompactifiableCover_of_isGerbeOver {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hY : IsAlgebraicSpace B S hS Y) {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS Y hY)
    (hfs : IsSeparated B S hS f) (hft : IsFiniteType B S hS f)
    (hYqc : Space.IsQuasiCompactSpace B S hS Y)
    (hYqs : Space.IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    (V : Subfunctor Y) (hV : Space.IsOpenSubspace B S hS V)
    (hVqc : Space.IsQuasiCompactSpace B S hS V.toFunctor)
    (hG : IsGerbeOver B S hS (twoFibreProductSquareAlgebraicStacks B S hS
      (algebraicSpaceStackMap.{u, w} B S hS hV.1 hY V.ι) f).fst) :
    HasProperCompactifiableCover.{u, w} B S hS hY f V

Tag 0CQ8, a theorem

Tag 0CQ8 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.hasChowCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChowLemmaAlgebraicStacks.lean, line 66. The attribute's comment: “Chow's lemma for algebraic stacks: the commutative diagram is a 2-isomorphism a ≫ f ≅ i ≫ p in the 2-category of algebraic stacks over S, with X and X̄ algebraic spaces”.

Chow's lemma for algebraic stacks (Stacks 0CQ8). Let f : 𝒳 ⟶ Y be a 1-morphism from an algebraic stack to an algebraic space over S, with Y quasi-compact and quasi-separated and f separated of finite type. Then there are an algebraic space X with a proper surjective 1-morphism a : X ⟶ 𝒳, an open immersion i : X ⟶ X̄ and a proper morphism p : X̄ ⟶ Y of algebraic spaces such that a ≫ f is 2-isomorphic to the 1-morphism induced by i ≫ p.

theorem hasChowCover (B : BigFppfSite.{u}) {S : Scheme.{u}} {hS : B.Contains S}
    {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hY : IsAlgebraicSpace B S hS Y)
    (hYqc : Space.IsQuasiCompactSpace B S hS Y)
    (hYqs : Space.IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    {𝒳 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS Y hY)
    (hsep : IsSeparated B S hS f) (hft : IsFiniteType B S hS f) :
    HasChowCover.{u, w} B S hS hY f

Sources

• Section 106.10, Tag 0CQ5
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.exists_finite_surjective_zariskiLocal_factorization · AlgebraicGeometry.Stack.AlgebraicStacks.hasProperCompactifiableCover_of_isGerbeOver · AlgebraicGeometry.Stack.AlgebraicStacks.hasChowCover

Section106.11 Noetherian valuative criterion#

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

Tag 0H2B, a lemma

Tag 0H2B in the Stacks Project.

AlgebraicGeometry.Stack.exists_discreteValuationRing_of_mem_closure_range_pointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ClosureImageDiscreteValuationPoint.lean, line 227.

Stacks 0H2B. A point in the closure of the image of a finite-type 1-morphism of algebraic stacks whose target is locally Noetherian is reached by the closed point of a valuative square whose valuation ring is a discrete valuation ring.

theorem exists_discreteValuationRing_of_mem_closure_range_pointsMap
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (hf : AlgebraicStacks.IsFiniteType B S hS f)
    (h𝒴 : HasPropertyOnSomeSchemeAtlas B S hS
      (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴)
    (y : points B S hS 𝒴.val.val (Classical.choose 𝒴.property))
    (hy : y ∈ @closure _
      (pointTopology B S hS 𝒴.val)
      (Set.range
        (pointsMap B S hS 𝒳.val.val (Classical.choose 𝒳.property)
          (Classical.choose 𝒴.property) f.hom.hom))) :
    ∃ (q : ValuativeSquare B S hS f) (_ : IsDiscreteValuationRing q.R)
      (hz : B.Contains
        (Spec (.of ((Spec (.of q.R)).residueField (IsLocalRing.closedPoint q.R))))),
      pointClass B S hS 𝒴.val.val
        (Classical.choose 𝒴.property)
        (fieldValuedPointMap B S hS
          (schemeFibredCategory B S hS
            (siteObject B S hS q.ring_mem q.base)).val
          q.y.hom
          (closedPointFieldValuedPoint B S hS
            (siteObject B S hS q.ring_mem q.base)
            (IsLocalRing.closedPoint q.R) hz)) = y

Tag 0E80, a lemma

Tag 0E80 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_discreteUniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianValuativeCriterionSeparated.lean, line 324. The attribute's comment: “a quasi-separated 1-morphism of algebraic stacks, locally of finite type over a locally Noetherian target, is separated as soon as the uniqueness part of the valuative criterion holds at every discrete valuation ring”.

Stacks 0E80, the Noetherian valuative criterion for separatedness. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S with 𝒴 locally Noetherian and f locally of finite type and quasi-separated. If, for every valuative diagram for f whose valuation ring is a discrete valuation ring, the category of dotted arrows is either empty or a setoid with exactly one isomorphism class, then f is separated.

Separatedness is properness of Δ_f in the relative sense of Stacks 04XB, and AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_discreteLift reduces it, along a locally Noetherian scheme chart of 𝒳 ×_𝒴 𝒳, to the full valuative criterion at discrete valuation rings for the algebraic spaces representing the base changes of Δ_f. Both halves of that criterion come from the hypothesis through the two transfers of Stacks 0CLN and Stacks 0CLJ, each of which carries a restriction on the valuation ring through unchanged:

• a lift exists by AlgebraicGeometry.Stack.nonempty_lift_baseChange_point, whose input is a dotted arrow for a valuative square for Δ_f over the same valuation ring; reading that square as a valuative diagram, Stacks 0E8L builds it from the hypothesis through AlgebraicGeometry.Stack.nonempty_dottedArrow_relativeDiagonal_of_pred;
• it is unique by AlgebraicGeometry.Stack.subsingleton_lift_baseChange_point, whose input is the isomorphism of any two dotted arrows of a valuative diagram for Δ_f, which is AlgebraicGeometry.Stack.nonempty_iso_dottedArrow_relativeDiagonal_of_pred.

The valuation ring never changes along the way — no extension of the fraction field and no passage to a dominating valuation ring — so "discrete" survives every step, which is the whole point of the Noetherian form of the criterion.

theorem isSeparated_of_discreteUniqueness (f : 𝒳 ⟶ 𝒴)
    (hY : HasPropertyOnSomeSchemeAtlas B S hS (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hqs : IsQuasiSeparated B S hS f)
    (H : ValuativeCriterion.DiscreteUniqueness B S hS f) :
    IsSeparated B S hS f

Tag 0CQM, a lemma

Tag 0CQM in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isProper_of_discreteExistenceAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RefinedValuativeCriterionProper.lean, line 405.

Stacks 0CQM. Let f : 𝒳 ⟶ 𝒴 and h : 𝒰 ⟶ 𝒳 be 1-morphisms of algebraic stacks over S. Assume that 𝒴 is locally Noetherian, that f and h are of finite type, that f is separated, and that the image of |h| : |𝒰| → |𝒳| is dense in |𝒳|. If for every 2-commutative diagram Spec K ⟶ 𝒰 ⟶ 𝒳 ⟶ 𝒴, Spec A ⟶ 𝒴, with A a discrete valuation ring with field of fractions K and a 2-arrow γ : y ∘ j → f ∘ h ∘ u, there are an extension K'/K of fields and a valuation ring A' ⊂ K' dominating A such that the category of dotted arrows of the induced diagram for f is nonempty, then f is proper.

𝒴 locally Noetherian is the existence of a smooth surjective atlas by a locally Noetherian scheme (HasPropertyOnSomeSchemeAtlas). The valuative hypothesis is ValuativeCriterion.DiscreteExistenceAlong B S hS h f: a diagram of the statement is a valuative square for f (Stacks 0CLK) over a discrete valuation ring whose generic point x is u ≫ h, its 2-arrow being the square's γ; the induced diagram over A' with its 2-arrow γ' is the square's restriction along the dominating extension (e.inducedGamma), and its category of dotted arrows is that of Stacks 0CLA (CategoryTheory.DottedArrow).

The proof is the source's: the reduction to an affine locally Noetherian base and an affine source (isProper_of_discreteExistenceAlong_of_affineCore), and the affine case (universallyClosed_of_discreteExistenceAlong_affineCore), which uses Chow's lemma for algebraic stacks over a Noetherian base.

theorem isProper_of_discreteExistenceAlong
    {𝒰 𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (h : 𝒰 ⟶ 𝒳) (f : 𝒳 ⟶ 𝒴)
    (h𝒴 : HasPropertyOnSomeSchemeAtlas B S hS (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴)
    (hf : IsFiniteType B S hS f) (hh : IsFiniteType B S hS h) (hsep : IsSeparated B S hS f)
    (hdense : @Dense _ (pointTopology B S hS 𝒳.val) (Set.range (pointsMap B S hS h)))
    (hlift : ValuativeCriterion.DiscreteExistenceAlong B S hS h f) :
    IsProper B S hS f

Tag 0E95, a lemma

Tag 0E95 in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_denseTestUniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DenseTestValuativeSeparated.lean, line 288.

Stacks 0E95. Let f : 𝒳 ⟶ 𝒴 and h : 𝒰 ⟶ 𝒳 be 1-morphisms of algebraic stacks over S, with 𝒴 locally Noetherian, f locally of finite type and quasi-separated, h of finite type and the image of |h| dense in |𝒳|. If every discrete valuative square for f through h has a category of dotted arrows which is either empty or a setoid with exactly one isomorphism class, then f is separated.

Δ_f is separated by the first case applied to Δ_f and h: the relative diagonal of Δ_f is separated because Δ_f is representable by algebraic spaces (Stacks 04YQ part (4), read in the sense of Stacks 04YW by Stacks 04YS), Δ_{Δ_f} is quasi-compact because Δ_f is quasi-separated (Stacks 04YZ part (2) and Stacks 050T), and the hypothesis passes from f to Δ_f by Stacks 0E8L. Then the first case applies to f and h.

theorem isSeparated_of_denseTestUniqueness
    (f : 𝒳 ⟶ 𝒴) (h : 𝒰 ⟶ 𝒳)
    (hY : HasPropertyOnSomeSchemeAtlas B S hS (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hqs : IsQuasiSeparated B S hS f)
    (hh : IsFiniteType B S hS h)
    (hdense : letI := Stack.pointTopology B S hS 𝒳.val;
      Dense (Set.range (Stack.pointsMap B S hS 𝒰.val.val 𝒰.val.property 𝒳.val.property
        h.hom.hom)))
    (hu : ValuativeCriterion.DenseTestUniqueness B S hS h f) :
    IsSeparated B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_discreteUniquenessAlong_of_dense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RefinedValuativeCriterionSeparationUnconditional.lean, line 540.

Stacks 0E95. Let f : 𝒳 ⟶ 𝒴 and h : 𝒰 ⟶ 𝒳 be 1-morphisms of algebraic stacks over S. Assume that 𝒴 is locally Noetherian, that f is locally of finite type and quasi-separated, that h is of finite type, and that the image of |h| : |𝒰| ⟶ |𝒳| is dense in |𝒳|. If for every 2-commutative diagram for f over a discrete valuation ring A with fraction field K whose generic point is h ∘ u for some u : Spec K ⟶ 𝒰, the category of dotted arrows is either empty or a setoid with exactly one isomorphism class, then f is separated.

The hypothesis on dotted arrows is AlgebraicGeometry.Stack.ValuativeCriterion.DiscreteUniquenessAlong. The proof is the source's: the first case (isSeparated_of_isSeparated_relativeDiagonal_of_discreteUniquenessAlong) applied to Δ_f in place of f shows that Δ_f is separated, and the first case applied to f concludes. For the first application, Δ_f is representable by algebraic spaces, so every category of dotted arrows of a diagram for Δ_f is a setoid (Stacks 0E8L, Stacks 0CLC), whence Δ_{Δ_f} is separated; uniqueness along h passes from f to Δ_f by Stacks 0E8L; Δ_f is quasi-separated because f is; and 𝒳 ×_𝒴 𝒳 is locally Noetherian (Stacks 06R6).

theorem isSeparated_of_discreteUniquenessAlong_of_dense
    {𝒰 𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (h : 𝒰 ⟶ 𝒳) (f : 𝒳 ⟶ 𝒴)
    (h𝒴 : HasPropertyOnSomeSchemeAtlas B S hS (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴)
    (hf : IsLocallyOfFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f)
    (hh : IsFiniteType B S hS h)
    (hdense : @Dense _ (pointTopology B S hS 𝒳.val) (Set.range (pointsMap B S hS h)))
    (huniq : ValuativeCriterion.DiscreteUniquenessAlong B S hS h f) :
    IsSeparated B S hS f

Tag 0H2C, a lemma

Tag 0H2C in the Stacks Project.

AlgebraicGeometry.Stack.ValuativeCriterion.DiscreteExistence, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianValuativeCriterionUniversallyClosed.lean, line 107. The attribute's comment: “the hypothesis of the lemma: the existence part of the valuative criterion, restricted to discrete valuation rings”.

The hypothesis of Stacks 0H2C. A 1-morphism of algebraic stacks over S satisfies the discrete existence part of the valuative criterion when every valuative square for it whose valuation ring is a discrete valuation ring admits a dotted arrow after an extension of the fraction field and passage to a dominating valuation ring.

This is AlgebraicGeometry.Stack.ValuativeCriterion.Existence of Stacks 0CLK with the extra clause IsDiscreteValuationRing q.R; the dominating valuation ring is not asked to be discrete.

abbrev DiscreteExistence (f : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.discreteExistence_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianValuativeCriterionUniversallyClosed.lean, line 122. The attribute's comment: “step 1 of the proof: the hypothesis is stable under base change, via Tag 0CLE”.

The hypothesis of Stacks 0H2C is stable under base change. A base change of a 1-morphism of algebraic stacks satisfying the discrete existence part of the valuative criterion satisfies it as well.

The valuative square for f obtained by pasting the given square with the base-change square has the same valuation ring, so discreteness transports, and the dotted arrow comes back along the equivalence of Stacks 0CLE.

theorem discreteExistence_baseChange
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (P : Bicategory.TwoCommSq g f) (hP : Bicategory.IsTwoFibreProduct P)
    (hf : ValuativeCriterion.DiscreteExistence B S hS f) :
    ValuativeCriterion.DiscreteExistence B S hS P.fst

AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_of_discreteExistence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianValuativeCriterionUniversallyClosed.lean, line 180. The attribute's comment: “steps 3 and 4 of the proof: closedness on points”.

Closedness on points from the hypothesis of Stacks 0H2C. Let f : 𝒳 ⟶ 𝒴 be a finite-type 1-morphism of algebraic stacks over S with 𝒴 locally Noetherian which satisfies the discrete existence part of the valuative criterion. Then f is closed on points.

A closed subset of |𝒳| is the set of points of a closed substack i : 𝒵 ⟶ 𝒳 by the existence half of Stacks 0509, so its image is the image of |𝒵| → |𝒴|. A point in the closure of that image is reached by a discrete valuative square for i ≫ f (Stacks 0H2B); read as a square for f it yields a lift to 𝒳 over a dominating valuation ring, and the full existence criterion, available for the closed immersion i by Stacks 0CLP, lifts that further to 𝒵.

theorem isClosed_of_discreteExistence (f : 𝒳 ⟶ 𝒴)
    (hf : IsFiniteType B S hS f)
    (h𝒴 : HasPropertyOnSomeSchemeAtlas B S hS
      (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴)
    (hlift : ValuativeCriterion.DiscreteExistence B S hS f) :
    IsClosed B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_baseChange_affine_isLocallyOfFinitePresentation_of_discreteExistence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianValuativeCriterionUniversallyClosed.lean, line 257. The attribute's comment: “clause (2) of Tag 0H2A for f”.

Stacks 0H2A, item (2), from the hypothesis of Stacks 0H2C. Let f : 𝒳 ⟶ 𝒴 be a finite-type 1-morphism of algebraic stacks over S with 𝒴 locally Noetherian which satisfies the discrete existence part of the valuative criterion. Then for every object Z of the site whose scheme is affine and every 1-morphism Stack.schemeStack Z ⟶ 𝒴 locally of finite presentation, the map |𝒳 ×_𝒴 Z| → |Z| is closed.

The base change is again of finite type (Stacks 06Q7), its target is again locally Noetherian (Stacks 06R6), and it again satisfies the hypothesis by AlgebraicGeometry.Stack.discreteExistence_baseChange. Affineness of Z is not used.

theorem isClosed_baseChange_affine_isLocallyOfFinitePresentation_of_discreteExistence
    (f : 𝒳 ⟶ 𝒴) (hf : IsFiniteType B S hS f)
    (h𝒴 : HasPropertyOnSomeSchemeAtlas B S hS
      (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴)
    (hlift : ValuativeCriterion.DiscreteExistence B S hS f) :
    ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
      ∀ (g : Stack.schemeStack.{u, w} B S hS Z ⟶ 𝒴),
        IsLocallyOfFinitePresentation B S hS g →
          IsClosed B S hS (Stack.twoFibreProductSquareAlgebraicStacks B S hS g f).fst

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_of_discreteExistence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianValuativeCriterionUniversallyClosed.lean, line 285. The attribute's comment: “the lemma”.

Stacks 0H2C. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S with 𝒴 locally Noetherian and f of finite type. If every valuative square for f whose valuation ring is a discrete valuation ring admits a dotted arrow after an extension of the fraction field and passage to a dominating valuation ring, then f is universally closed.

Clause (2) of Stacks 0H2A holds for f by AlgebraicGeometry.Stack.AlgebraicStacks .isClosed_baseChange_affine_isLocallyOfFinitePresentation_of_discreteExistence, and f is of finite type, hence quasi-compact, so (2) implies (1) of Stacks 0H2A.

theorem universallyClosed_of_discreteExistence
    (f : 𝒳 ⟶ 𝒴) (hf : IsFiniteType B S hS f)
    (h𝒴 : HasPropertyOnSomeSchemeAtlas B S hS
      (fun T : Scheme.{u} => IsLocallyNoetherian T) 𝒴)
    (hlift : ValuativeCriterion.DiscreteExistence B S hS f) :
    UniversallyClosed B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_of_discreteExistence', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianValuativeCriterionUniversallyClosedUnconditional.lean, line 50. The attribute's comment: “steps 3 and 4 of the proof: closedness on points”.

Stacks 0H2C, steps 3 and 4: closedness on points, with nothing assumed. Let f : 𝒳 ⟶ 𝒴 be a finite-type 1-morphism of algebraic stacks over S with 𝒴 locally Noetherian which satisfies the discrete existence part of the valuative criterion. Then f is closed on points.

This is AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_of_discreteExistence.

alias isClosed_of_discreteExistence'

AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_baseChange_affine_isLocallyOfFinitePresentation_of_discreteExistence', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianValuativeCriterionUniversallyClosedUnconditional.lean, line 60. The attribute's comment: “clause (2) of Tag 0H2A for f”.

Stacks 0H2A, item (2), from the hypothesis of Stacks 0H2C, with nothing assumed. For every object Z of the site whose scheme is affine and every 1-morphism Stack.schemeStack Z ⟶ 𝒴 locally of finite presentation, the map |𝒳 ×_𝒴 Z| → |Z| is closed.

This is AlgebraicGeometry.Stack.AlgebraicStacks .isClosed_baseChange_affine_isLocallyOfFinitePresentation_of_discreteExistence.

alias isClosed_baseChange_affine_isLocallyOfFinitePresentation_of_discreteExistence'

AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_of_discreteExistence', an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/NoetherianValuativeCriterionUniversallyClosedUnconditional.lean, line 70. The attribute's comment: “the lemma”.

Stacks 0H2C. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S with 𝒴 locally Noetherian and f of finite type. If every valuative square for f whose valuation ring is a discrete valuation ring admits a dotted arrow after an extension of the fraction field and passage to a dominating valuation ring, then f is universally closed.

This is AlgebraicGeometry.Stack.AlgebraicStacks.universallyClosed_of_discreteExistence.

alias universallyClosed_of_discreteExistence'

Sources

• Section 106.11, Tag 0CQL
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.exists_discreteValuationRing_of_mem_closure_range_pointsMap · AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_discreteUniqueness · AlgebraicGeometry.Stack.AlgebraicStacks.isProper_of_discreteExistenceAlong · AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_denseTestUniqueness · AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_discreteUniquenessAlong_of_dense · AlgebraicGeometry.Stack.ValuativeCriterion.DiscreteExistence · AlgebraicGeometry.Stack.discreteExistence_baseChange · AlgebraicGeometry.Stack.AlgebraicStacks.isClosed_of_discreteExistence

Section106.12 Moduli spaces#

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

Tag 0DUG, a definition

Tag 0DUG in the Stacks Project.

AlgebraicGeometry.Stack.IsCategoricalModuliSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/CategoricalModuliSpace.lean, line 60. The attribute's comment: “part (1)”.

A 1-morphism from a category fibred in groupoids to the category attached to an algebraic space Y is a categorical moduli space when every 1-morphism to the category attached to an algebraic space W factors through it by a unique morphism Y ⟶ W of algebraic spaces, the factorization holding up to an invertible 2-morphism.

abbrev IsCategoricalModuliSpace
    {𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (Y : AlgebraicSpaces B S hS)
    (f : 𝒳 ⟶ fibredCategory B S hS Y.obj) : Prop

AlgebraicGeometry.Stack.IsUniformCategoricalModuliSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/CategoricalModuliSpace.lean, line 73. The attribute's comment: “part (2)”.

A categorical moduli space is uniform when every base change of it along a flat morphism of algebraic spaces, given by any 2-fibre product of the cospan, is again a categorical moduli space.

abbrev IsUniformCategoricalModuliSpace
    {𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (Y : AlgebraicSpaces B S hS)
    (f : 𝒳 ⟶ fibredCategory B S hS Y.obj) : Prop

AlgebraicGeometry.Stack.IsCategoricalModuliSpaceIn, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/CategoricalModuliSpace.lean, line 86. The attribute's comment: “part (3)”.

The universal factorization property with the target algebraic spaces restricted to the full subcategory selected by the object predicate C, which Y is required to meet.

abbrev IsCategoricalModuliSpaceIn
    (C : AlgebraicSpaces B S hS → Prop)
    {𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (Y : AlgebraicSpaces B S hS)
    (f : 𝒳 ⟶ fibredCategory B S hS Y.obj) : Prop

AlgebraicGeometry.Stack.IsUniformCategoricalModuliSpaceIn, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/CategoricalModuliSpace.lean, line 101. The attribute's comment: “part (4)”.

A categorical moduli space in the full subcategory selected by C is uniform in C when its base change along every flat morphism of that subcategory is again a categorical moduli space in C.

abbrev IsUniformCategoricalModuliSpaceIn
    (C : AlgebraicSpaces B S hS → Prop)
    {𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (Y : AlgebraicSpaces B S hS)
    (f : 𝒳 ⟶ fibredCategory B S hS Y.obj) : Prop

Tag 0DUH, a lemma

Tag 0DUH in the Stacks Project.

AlgebraicGeometry.Stack.quotientStackHomEquivInvariant, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/MorphismsToAlgebraicSpaces.lean, line 294.

For a groupoid in algebraic spaces (U, R, s, t, c) over an algebraic space B over a scheme S of a big fppf site, and an algebraic space Y over S, the 1-morphisms [U/R] ⟶ Y of stacks over the big fppf site are in 1-to-1 correspondence with the R-invariant morphisms U ⟶ Y, by restriction along the projection π : U ⟶ [U/R] of Stacks 044R.

noncomputable def quotientStackHomEquivInvariant :
    (quotientStack G ⥤ᵇ (fibredCategory C S hS Y.obj).val) ≃
      {φ : G.objects ⟶ Y // Space.IsInvariant (Space.groupoidPreRelation G) φ.hom}

AlgebraicGeometry.Stack.quotientStackHomEquivInvariant_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/MorphismsToAlgebraicSpaces.lean, line 323. The attribute's comment: “the correspondence is restriction along the projection”.

The correspondence is restriction along the projection: the 1-morphism [U/R] ⟶ Y corresponding to an R-invariant morphism φ : U ⟶ Y restricts along the projection π : U ⟶ [U/R] to the 1-morphism attached to φ by Stacks 0458.

theorem quotientStackHomEquivInvariant_spec
    (f : quotientStack G ⥤ᵇ (fibredCategory C S hS Y.obj).val) :
    BasedFunctor.comp (quotientStackProjection G) f =
      (associatedMap C S hS (quotientStackHomEquivInvariant G Y f).val.hom).1.hom

Tag 0DUI, a lemma

Tag 0DUI in the Stacks Project.

AlgebraicGeometry.Stack.quotientStack_isCategoricalModuliSpace_iff_isCategoricalQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackModuliSpace.lean, line 265. The attribute's comment: “the non-uniform case, for a groupoid over the terminal base as in the source”.

Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over a terminal base, let j = (t, s) be its pre-relation and let f : [U/R] ⟶ Y be a 1-morphism to the category attached to an algebraic space Y. Then f is a categorical moduli space exactly when its restriction φ : U ⟶ Y along the projection is a categorical quotient of j.

theorem quotientStack_isCategoricalModuliSpace_iff_isCategoricalQuotient (hB : IsTerminal B)
    (hjt : (Space.PreRelation.target j).left = G.target)
    (hjs : (Space.PreRelation.source j).left = G.source)
    (Y : AlgebraicSpaces C S hS)
    (f : quotientStack G ⥤ᵇ (fibredCategory C S hS Y.obj).val) :
    IsBasedCategoricalModuliSpace Y f ↔
      Space.IsCategoricalQuotient j
        (Over.homMk (restrictedMorphism G f) (hB.hom_ext _ _) :
          (Over.mk G.objectsToBase : Over B) ⟶ Over.mk (hB.from Y))

AlgebraicGeometry.Stack.quotientStack_isCategoricalModuliSpace_iff_isCategoricalQuotient_prodLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackModuliSpace.lean, line 284. The attribute's comment: “the non-uniform case at the pre-relation (t, s) the groupoid cuts out”.

Let G be a groupoid in algebraic spaces over a terminal base and let f : [U/R] ⟶ Y be a 1-morphism to the category attached to an algebraic space Y. Then f is a categorical moduli space exactly when its restriction φ : U ⟶ Y along the projection is a categorical quotient of the pre-relation prod.lift t s of G.

theorem quotientStack_isCategoricalModuliSpace_iff_isCategoricalQuotient_prodLift
    (hB : IsTerminal B) (G : GroupoidInAlgebraicSpaces C S hS B)
    (Y : AlgebraicSpaces C S hS)
    (f : quotientStack G ⥤ᵇ (fibredCategory C S hS Y.obj).val) :
    IsBasedCategoricalModuliSpace Y f ↔
      Space.IsCategoricalQuotient
        (prod.lift (Over.homMk G.target G.target_over) (Over.homMk G.source G.source_over) :
          Space.PreRelation (Over.mk G.arrowsToBase) (Over.mk G.objectsToBase))
        (Over.homMk (restrictedMorphism G f) (hB.hom_ext _ _) :
          (Over.mk G.objectsToBase : Over B) ⟶ Over.mk (hB.from Y))

AlgebraicGeometry.Stack.quotientStack_isCategoricalModuliSpaceIn_iff_isCategoricalQuotientIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackModuliSpace.lean, line 303. The attribute's comment: “the non-uniform case in a full subcategory, for a groupoid over the terminal base”.

With the same data as AlgebraicGeometry.Stack.quotientStack_isCategoricalModuliSpace_iff_isCategoricalQuotient and a full subcategory of the algebraic spaces, selected by a predicate P on objects and containing the object and arrow spaces of the groupoid, f is a categorical moduli space in that subcategory exactly when φ is a categorical quotient in it.

theorem quotientStack_isCategoricalModuliSpaceIn_iff_isCategoricalQuotientIn (hB : IsTerminal B)
    (hjt : (Space.PreRelation.target j).left = G.target)
    (hjs : (Space.PreRelation.source j).left = G.source)
    (P : AlgebraicSpaces C S hS → Prop) (hR : P G.arrows) (hU : P G.objects)
    (Y : AlgebraicSpaces C S hS)
    (f : quotientStack G ⥤ᵇ (fibredCategory C S hS Y.obj).val) :
    IsBasedCategoricalModuliSpaceIn P Y f ↔
      Space.IsCategoricalQuotientIn (fun Z : Over B => P Z.left) j
        (Over.homMk (restrictedMorphism G f) (hB.hom_ext _ _) :
          (Over.mk G.objectsToBase : Over B) ⟶ Over.mk (hB.from Y))

AlgebraicGeometry.Stack.quotientStack_isUniformCategoricalModuliSpace_iff_isUniformCategoricalQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackUniformModuliSpace.lean, line 558. The attribute's comment: “the uniform case, for a groupoid over the terminal base as in the source”.

Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over a terminal base, let f : [U/R] ⟶ Y be a 1-morphism to the category attached to an algebraic space Y and let φ : U ⟶ Y be its restriction along the projection of Stacks 044R. Then f is a uniform categorical moduli space exactly when φ is a uniform categorical quotient: for every flat a : Y' ⟶ Y, the base change Y' ×_Y [U/R] ⟶ Y' of f is a categorical moduli space exactly when the base-changed quotient map U' ⟶ Y' is a categorical quotient of the base-changed pre-relation (t', s'), for U' = Y' ×_Y U and R' = Y' ×_Y R.

The base change is an arbitrary 2-fibre product of the cospan in the 2-category of stacks in groupoids of Stacks 02ZK.

theorem quotientStack_isUniformCategoricalModuliSpace_iff_isUniformCategoricalQuotient :
    (∀ (Y' : AlgebraicSpaces C S hS) (a : Y' ⟶ Y), Space.IsFlat C S hS a.hom →
        ∀ P : Bicategory.TwoCommSq
            (Bicategory.InducedBicategory.mkHom (BasedFunctor.comp f (liftedFibredCategoryUp Y)) :
              quotientStackAsStack G ⟶ spaceAsStack Y)
            (Bicategory.InducedBicategory.mkHom (liftedAssociatedMap a) :
              spaceAsStack Y' ⟶ spaceAsStack Y),
          Bicategory.IsTwoFibreProduct P →
            IsBasedCategoricalModuliSpace Y'
              (BasedFunctor.comp P.snd.hom (liftedFibredCategoryDown Y'))) ↔
      ∀ (Y' : AlgebraicSpaces C S hS) (a : Y' ⟶ Y), Space.IsFlat C S hS a.hom →
        Space.IsCategoricalQuotient
          (baseChangeSituationPreRelation hB G (restrictedMorphism G f)
            (restrictedMorphism_isInvariant G f) a)
          (baseChangeSituationQuotientMap hB G (restrictedMorphism G f)
            (restrictedMorphism_isInvariant G f) a)

AlgebraicGeometry.Stack.quotientStack_isUniformCategoricalModuliSpaceIn_iff_isUniformCategoricalQuotientIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackUniformModuliSpace.lean, line 588. The attribute's comment: “variant: the uniform case in a full subcategory, over every flat Y' ⟶ Y and with the subcategory containing every base change of R and U; the tag is quotientStack_isUniformModuliSpaceIn_iff_isUniformQuotientIn_of_isClosedUnderLimitsOfShape”.

The uniform case in a full subcategory. With the same data as quotientStack_isUniformCategoricalModuliSpace_iff_isUniformCategoricalQuotient and a full subcategory of the algebraic spaces, selected by a predicate Pr on objects which contains the object and arrow spaces of every base change of the groupoid: for every flat a : Y' ⟶ Y, the base change Y' ×_Y [U/R] ⟶ Y' of f is a categorical moduli space in Pr exactly when the base-changed quotient map U' ⟶ Y' is a categorical quotient in Pr of the base-changed pre-relation (t', s').

theorem quotientStack_isUniformCategoricalModuliSpaceIn_iff_isUniformCategoricalQuotientIn
    (Pr : AlgebraicSpaces C S hS → Prop)
    (hR : ∀ (Y' : AlgebraicSpaces C S hS) (a : Y' ⟶ Y),
      Pr (baseChangeSituationGroupoid hB G (restrictedMorphism G f)
        (restrictedMorphism_isInvariant G f) a).arrows)
    (hU : ∀ (Y' : AlgebraicSpaces C S hS) (a : Y' ⟶ Y),
      Pr (baseChangeSituationGroupoid hB G (restrictedMorphism G f)
        (restrictedMorphism_isInvariant G f) a).objects) :
    (∀ (Y' : AlgebraicSpaces C S hS) (a : Y' ⟶ Y), Space.IsFlat C S hS a.hom →
        ∀ P : Bicategory.TwoCommSq
            (Bicategory.InducedBicategory.mkHom (BasedFunctor.comp f (liftedFibredCategoryUp Y)) :
              quotientStackAsStack G ⟶ spaceAsStack Y)
            (Bicategory.InducedBicategory.mkHom (liftedAssociatedMap a) :
              spaceAsStack Y' ⟶ spaceAsStack Y),
          Bicategory.IsTwoFibreProduct P →
            IsBasedCategoricalModuliSpaceIn Pr Y'
              (BasedFunctor.comp P.snd.hom (liftedFibredCategoryDown Y'))) ↔
      ∀ (Y' : AlgebraicSpaces C S hS) (a : Y' ⟶ Y), Space.IsFlat C S hS a.hom →
        Space.IsCategoricalQuotientIn (fun Z : Over B => Pr Z.left)
          (baseChangeSituationPreRelation hB G (restrictedMorphism G f)
            (restrictedMorphism_isInvariant G f) a)
          (baseChangeSituationQuotientMap hB G (restrictedMorphism G f)
            (restrictedMorphism_isInvariant G f) a)

AlgebraicGeometry.Stack.quotientStack_isUniformModuliSpaceIn_iff_isUniformQuotientIn_of_isClosedUnderLimitsOfShape, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackUniformModuliSpace.lean, line 626. The attribute's comment: “uniform, in a full subcategory”.

Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over a terminal base, f : [U/R] ⟶ Y a 1-morphism to the category attached to an algebraic space Y, and φ : U ⟶ Y its restriction along the projection of Stacks 044R. Let Pr be a full subcategory of the algebraic spaces which is closed under fibre products and contains R and U. Then f is a uniform categorical moduli space in Pr (Stacks 0DUG, part (4)) — Y lies in Pr and for every flat a : Y' ⟶ Y with Y' in Pr the base change Y' ×_Y [U/R] ⟶ Y' is a categorical moduli space in Pr — exactly when φ is a uniform categorical quotient in Pr (Stacks 048L, part (2)) — R, U and Y lie in Pr and for every flat a : Y' ⟶ Y with Y' in Pr the base-changed quotient map U' ⟶ Y' is the categorical quotient in Pr of the base-changed pre-relation (t', s'), for U' = Y' ×_Y U and R' = Y' ×_Y R.

theorem quotientStack_isUniformModuliSpaceIn_iff_isUniformQuotientIn_of_isClosedUnderLimitsOfShape
    (Pr : ObjectProperty (AlgebraicSpaces C S hS)) [Pr.IsClosedUnderLimitsOfShape WalkingCospan]
    (hR : Pr G.arrows) (hU : Pr G.objects) :
    (Pr Y ∧ ∀ (Y' : AlgebraicSpaces C S hS), Pr Y' → ∀ (a : Y' ⟶ Y), Space.IsFlat C S hS a.hom →
        ∀ P : Bicategory.TwoCommSq
            (Bicategory.InducedBicategory.mkHom (BasedFunctor.comp f (liftedFibredCategoryUp Y)) :
              quotientStackAsStack G ⟶ spaceAsStack Y)
            (Bicategory.InducedBicategory.mkHom (liftedAssociatedMap a) :
              spaceAsStack Y' ⟶ spaceAsStack Y),
          Bicategory.IsTwoFibreProduct P →
            IsBasedCategoricalModuliSpaceIn Pr Y'
              (BasedFunctor.comp P.snd.hom (liftedFibredCategoryDown Y'))) ↔
      Pr G.arrows ∧ Pr G.objects ∧ Pr Y ∧
        ∀ (Y' : AlgebraicSpaces C S hS), Pr Y' → ∀ (a : Y' ⟶ Y), Space.IsFlat C S hS a.hom →
          Space.IsCategoricalQuotientIn (fun Z : Over B => Pr Z.left)
            (baseChangeSituationPreRelation hB G (restrictedMorphism G f)
              (restrictedMorphism_isInvariant G f) a)
            (baseChangeSituationQuotientMap hB G (restrictedMorphism G f)
              (restrictedMorphism_isInvariant G f) a)

Tag 0DUJ, a lemma

Tag 0DUJ in the Stacks Project.

AlgebraicGeometry.Stack.isUniformCategoricalModuliSpace_of_affineFlatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UniformCategoricalModuliSpaceAffine.lean, line 330.

Stacks 0DUJ. A 1-morphism from a category fibred in groupoids over the big fppf site of S to the category attached to an algebraic space Y is a uniform categorical moduli space as soon as every base change of it along a flat morphism to Y from an affine scheme is a categorical moduli space.

The source states this for a 1-morphism from an algebraic stack; nothing of 𝒳 beyond being fibred in groupoids is used, so it is stated here at that generality.

theorem isUniformCategoricalModuliSpace_of_affineFlatBaseChange
    {𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS)}
    (Y : AlgebraicSpaces B S hS) (f : 𝒳 ⟶ fibredCategory B S hS Y.obj)
    (h : ∀ T : BigFppfOver B S hS, IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
      ∀ a : (schemeSpace T : AlgebraicSpaces B S hS) ⟶ Y,
        Space.IsFlat B S hS a.hom →
          ∀ P : Bicategory.TwoCommSq (associatedMap B S hS a.hom).1 f,
            Bicategory.IsTwoFibreProduct P →
              IsCategoricalModuliSpace B S hS
                (schemeSpace T : AlgebraicSpaces B S hS)
                P.fst) :
    IsUniformCategoricalModuliSpace B S hS Y f

Sources

• Section 106.12, Tag 0DUF
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.IsCategoricalModuliSpace · AlgebraicGeometry.Stack.IsUniformCategoricalModuliSpace · AlgebraicGeometry.Stack.IsCategoricalModuliSpaceIn · AlgebraicGeometry.Stack.IsUniformCategoricalModuliSpaceIn · AlgebraicGeometry.Stack.quotientStackHomEquivInvariant · AlgebraicGeometry.Stack.quotientStackHomEquivInvariant_spec · AlgebraicGeometry.Stack.quotientStack_isCategoricalModuliSpace_iff_isCategoricalQuotient · AlgebraicGeometry.Stack.quotientStack_isCategoricalModuliSpace_iff_isCategoricalQuotient_prodLift

Section106.13 The Keel-Mori theorem#

Section 106.13 of the Stacks Project, Tag 0DUK. 10 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DUL, a definition

Tag 0DUL in the Stacks Project.

AlgebraicGeometry.Stack.IsWellNighAffine, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffine.lean, line 135.

Stacks 0DUL. An algebraic stack over S is well-nigh affine when there is an object U of the big fppf site of S with affine underlying scheme and a 1-morphism from the algebraic stack it represents to 𝒳 which is surjective, flat, finite and of finite presentation.

abbrev IsWellNighAffine (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) : Prop

Tag 0DUM, a lemma

Tag 0DUM in the Stacks Project.

AlgebraicGeometry.Stack.isQuasiCompactStack_of_isWellNighAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineGroupoid.lean, line 161. The attribute's comment: “a well-nigh affine algebraic stack is quasi-compact”.

Stacks 0DUM, the quasi-compactness assertion. A well-nigh affine algebraic stack is quasi-compact: the algebraic stack of the affine scheme that Stacks 0DUL provides is quasi-compact, and it surjects onto 𝒳.

theorem isQuasiCompactStack_of_isWellNighAffine
    (𝒳 : AlgebraicStacks.{u, w} B S hS) (h𝒳 : IsWellNighAffine.{u, w} B S hS 𝒳) :
    IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property

AlgebraicGeometry.Stack.HasAffineFiniteLocallyFreeGroupoidPresentation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineGroupoid.lean, line 191. The attribute's comment: “condition (2): a presentation by an affine groupoid scheme with finite locally free source and target”.

Stacks 0DUM, condition (2). An algebraic stack over S has an affine finite locally free groupoid presentation when it is equivalent over the site to the quotient stack of a groupoid scheme whose object and arrow schemes are affine objects of the site and whose source and target are finite locally free.

abbrev HasAffineFiniteLocallyFreeGroupoidPresentation
    (𝒳 : AlgebraicStacks.{u, w} B S hS) : Prop

AlgebraicGeometry.Stack.isAbsolutelyQuasiDM_of_representedGroupoid_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineGroupoid.lean, line 292. The attribute's comment: “a well-nigh affine algebraic stack is quasi-DM, read off condition (2)”.

Stacks 0DUM, the quasi-DM assertion. An algebraic stack equivalent over the site to the quotient stack of a groupoid scheme of the site with finite locally free source and target is quasi-DM.

This is Stacks 0DTY, part (4): finite local freeness makes the source and target flat, locally of finite presentation and locally quasi-finite, and the cancellation of the source projection of the square of the object space makes (t, s) locally quasi-finite. Affineness of the object and arrow schemes is not used.

theorem isAbsolutelyQuasiDM_of_representedGroupoid_isFiniteLocallyFree
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (hs : Stacks.Morphisms.IsFiniteLocallyFree ((BigFppfOver.toScheme B S hS).map s))
    (ht : Stacks.Morphisms.IsFiniteLocallyFree ((BigFppfOver.toScheme B S hS).map t))
    (hequiv : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (quotientStack (representedGroupoid B S hS s t c hG)).p 𝒳.val.val.p)) :
    AlgebraicStacks.IsAbsolutelyQuasiDM.{u, w} B S hS hZ 𝒳

AlgebraicGeometry.Stack.isSeparatedOver_of_representedGroupoid_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineGroupoid.lean, line 318. The attribute's comment: “a well-nigh affine algebraic stack is separated over the base scheme of the site, read off condition (2)”.

Stacks 0DUM, the separatedness assertion over the base scheme of the site. An algebraic stack equivalent over the site to the quotient stack of a groupoid scheme of the site with affine object scheme and finite locally free source and target is separated over S.

This is Stacks 0DTY, part (6): finite local freeness makes the source and target flat, locally of finite presentation and proper, the object scheme being affine makes the object space separated over S, and the cancellation of the separated source projection of the square of the object space makes (t, s) proper.

theorem isSeparatedOver_of_representedGroupoid_isFiniteLocallyFree
    (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
    (hs : Stacks.Morphisms.IsFiniteLocallyFree ((BigFppfOver.toScheme B S hS).map s))
    (ht : Stacks.Morphisms.IsFiniteLocallyFree ((BigFppfOver.toScheme B S hS).map t))
    (hequiv : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (quotientStack (representedGroupoid B S hS s t c hG)).p 𝒳.val.val.p)) :
    IsSeparatedOver.{u, w} B S hS 𝒳

AlgebraicGeometry.Stack.isAbsolutelySeparated_of_representedGroupoid_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineGroupoid.lean, line 344. The attribute's comment: “a well-nigh affine algebraic stack is separated in the source's unqualified (absolute) sense, read off condition (2)”.

Stacks 0DUM, the separatedness assertion. An algebraic stack equivalent over the site to the quotient stack of a groupoid scheme of the site with affine object scheme and finite locally free source and target is separated in the source's unqualified, absolute sense of Stacks 050D, part (7), provided the algebraic stack of the base scheme of the site is separated.

Separatedness over the base scheme is the previous clause; the absolute notion is strictly stronger, and hBase is the one further input Stacks 0DTY needs to reach it.

theorem isAbsolutelySeparated_of_representedGroupoid_isFiniteLocallyFree
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (hBase : AlgebraicStacks.IsAbsolutelySeparated.{u, w} B S hS hZ
      (schemeStack.{u, w} B S hS (Over.mk (𝟙 (B.obj hS)))))
    (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
    (hs : Stacks.Morphisms.IsFiniteLocallyFree ((BigFppfOver.toScheme B S hS).map s))
    (ht : Stacks.Morphisms.IsFiniteLocallyFree ((BigFppfOver.toScheme B S hS).map t))
    (hequiv : Nonempty (StacksRepresentableCFG.EquivalenceOver
      (quotientStack (representedGroupoid B S hS s t c hG)).p 𝒳.val.val.p)) :
    AlgebraicStacks.IsAbsolutelySeparated.{u, w} B S hS hZ 𝒳

AlgebraicGeometry.Stack.isWellNighAffine_iff_and_isQuasiCompact_isQuasiDM_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineGroupoidPresentation.lean, line 441.

Stacks 0DUM. Let 𝒳 be an algebraic stack over S. The following are equivalent:

1. 𝒳 is well-nigh affine (Stacks 0DUL);
2. there is a groupoid scheme (U, R, s, t, c) with U and R affine and s, t : R ⟶ U finite locally free such that 𝒳 = [U/R].

If they hold, then 𝒳 is quasi-compact, quasi-DM and separated, the last two in the absolute sense of Stacks 050D, parts (6) and (7), that is over Spec ℤ.

The equivalence is hasAffineFiniteLocallyFreeGroupoidPresentation_of_isWellNighAffine and isWellNighAffine_of_hasAffineFiniteLocallyFreeGroupoidPresentation; quasi-compactness is isQuasiCompactStack_of_isWellNighAffine, quasi-DM is Stacks 0DTY (4) applied to the presentation of (2), and separatedness is isAbsolutelySeparated_of_isWellNighAffine.

theorem isWellNighAffine_iff_and_isQuasiCompact_isQuasiDM_isSeparated
    (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    (IsWellNighAffine.{u, w} B S hS 𝒳 ↔
        HasAffineFiniteLocallyFreeGroupoidPresentation.{u, w} B S hS 𝒳) ∧
      (IsWellNighAffine.{u, w} B S hS 𝒳 →
        IsQuasiCompactStack.{u, w} B S hS 𝒳.val 𝒳.property ∧
          AlgebraicStacks.IsAbsolutelyQuasiDM.{u, w} B S hS (contains_terminalScheme B) 𝒳 ∧
            AlgebraicStacks.IsAbsolutelySeparated.{u, w} B S hS (contains_terminalScheme B) 𝒳)

Tag 0DUN, a lemma

Tag 0DUN in the Stacks Project.

AlgebraicGeometry.Stack.isWellNighAffine_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineGroupoid.lean, line 379. The attribute's comment: “clause (2): the source of an affine 1-morphism of algebraic stacks whose target is well-nigh affine is well-nigh affine”.

Stacks 0DUN, clause (2). If 𝒳 is a well-nigh affine algebraic stack over S and f : 𝒳' ⟶ 𝒳 is an affine 1-morphism of algebraic stacks over S, then 𝒳' is well-nigh affine.

The affine scheme U presenting 𝒳 is read as a scheme-valued point of 𝒳; the base change of f along it is represented by an algebraic space over U whose structural morphism is affine, so tested at U itself it is the projection of an affine scheme W of the site. The apex of the base-change square is then the algebraic stack of W, and its projection to 𝒳' is surjective, flat, finite and of finite presentation because the presentation of 𝒳 is.

theorem isWellNighAffine_of_isAffineHom {𝒳 𝒳' : AlgebraicStacks.{u, w} B S hS} (f : 𝒳' ⟶ 𝒳)
    (hf : AlgebraicStacks.IsAffineHom B S hS f)
    (h𝒳 : IsWellNighAffine.{u, w} B S hS 𝒳) :
    IsWellNighAffine.{u, w} B S hS 𝒳'

AlgebraicGeometry.Stack.isAffineSpace_of_isWellNighAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineGroupoid.lean, line 619. The attribute's comment: “clause (1): a well-nigh affine algebraic stack which is an algebraic space is affine”.

Stacks 0DUN, clause (1). A well-nigh affine algebraic stack over S which is an algebraic space is affine: every algebraic space F representing it over the site is affine.

The affine scheme U presenting 𝒳 represents an algebraic stack as well, so Stacks 04SW turns the presentation into a morphism h_U ⟶ F of algebraic spaces over S. It is surjective because the presentation is surjective on points, finite because the presentation is finite in the relative sense of Stacks 03YK, flat because the presentation is flat, and locally of finite presentation because the presentation is of finite presentation; so it is a surjective finite locally free chart of F by Stacks 0416, and the ring of invariant functions of its kernel pair makes F affine by Stacks 03BM.

theorem isAffineSpace_of_isWellNighAffine (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsWellNighAffine.{u, w} B S hS 𝒳)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (eF : StacksRepresentableCFG.EquivalenceOver 𝒳.val.val.p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    Space.IsAffineSpace B S hS F

Tag 0DUP, a lemma

Tag 0DUP in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.existsUnique_comp_objectsToInvariantSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteFlatAffine/InvariantModuliSpace.lean, line 129. The attribute's comment: “the construction of the moduli space and its universal property, at the groupoid presentation and for the quotient map of the object scheme: the invariant-ring quotient U -> M = Spec C is a categorical quotient in the category of affine schemes. The 1-morphism f : X -> M out of the quotient stack is NOT constructed, and none of the four assertions about f is proved: the passage from U -> M to f along Stacks 0DUH and Stacks 0DUI, and the implication (1) => (2) of Stacks 0DUM, are not available in the library”. References: SGA 1 V (1.1), “(iv), special case”.

Let G = (U, R, s, t, c) be a groupoid scheme and let C be the ring of R-invariant global functions on U. Every morphism ψ : U ⟶ Spec C' to an affine scheme which coequalizes the target and the source maps factors uniquely through φ : U ⟶ Spec C. Together with AlgebraicGeometry.GroupoidScheme.target_comp_objectsToInvariantSpectrum this says that φ is a categorical quotient of (t, s) in the category of affine schemes.

theorem existsUnique_comp_objectsToInvariantSpectrum (C' : Type u) [CommRing C']
    (ψ : G.objects.left ⟶ Spec (.of C'))
    (hψ : G.target.left ≫ ψ = G.source.left ≫ ψ) :
    ∃! χ : Spec (.of (invariantRing G)) ⟶ Spec (.of C'),
      objectsToInvariantSpectrum G ≫ χ = ψ

AlgebraicGeometry.GroupoidScheme.existsUnique_comp_objects_hom_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteFlatAffine/InvariantModuliSpace.lean, line 186. The attribute's comment: “the word uniform, at the groupoid presentation and for the quotient map of the object scheme: after a flat base change C -> C' the structure morphism U' -> Spec C' of the base-changed groupoid is again a categorical quotient in the category of affine schemes, so the flat base change of M is again the moduli space. Stated for U' -> Spec C' and NOT for the base change of a 1-morphism f : X -> M, which is not constructed here”. References: SGA 1 V (1.9), “affine case with Z = Y”.

Let C ⟶ C' be a flat ring map and let G' be the base change of the groupoid along it. Then the structure morphism U' ⟶ Spec C' of the object scheme of G' has the universal property of AlgebraicGeometry.GroupoidScheme.existsUnique_comp_objectsToInvariantSpectrum: every morphism from U' to an affine scheme which coequalizes the target and the source maps of G' factors uniquely through it.

theorem existsUnique_comp_objects_hom_of_flat [Module.Flat (invariantRing G) C']
    (C'' : Type u) [CommRing C''] (ψ : G'.groupoid.objects.left ⟶ Spec (.of C''))
    (hψ : G'.groupoid.target.left ≫ ψ = G'.groupoid.source.left ≫ ψ) :
    ∃! χ : Spec (.of C') ⟶ Spec (.of C''), G'.groupoid.objects.hom ≫ χ = ψ

AlgebraicGeometry.GroupoidScheme.universallyClosed_objectsToInvariantSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteFlatAffine/InvariantModuliSpace.lean, line 229. The attribute's comment: “part of assertion (d), at the groupoid presentation and for the quotient map of the object scheme: U -> M = Spec C is integral (Stacks 03BJ) and therefore universally closed (Stacks 01WM). That f : X -> M is a universal homeomorphism is NOT proved: neither the transport of universal closedness along the surjection U -> X (Stacks 0CQK), nor universal injectivity of f (Stacks 0DTN), nor surjectivity of |f| is covered here”. References: SGA 3 V (6.1), “special case”.

The invariant quotient map U ⟶ M = Spec C is universally closed.

theorem universallyClosed_objectsToInvariantSpectrum :
    UniversallyClosed (objectsToInvariantSpectrum G)

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

Stacks 0DUP. Let the algebraic stack 𝒳 be well-nigh affine. There exists a uniform categorical moduli space f : 𝒳 ⟶ M in the category of affine schemes. Moreover f is separated, quasi-compact, and a universal homeomorphism.

theorem exists_isUniformCategoricalModuliSpaceIn_of_isWellNighAffine
    (𝒳 : AlgebraicStacks.{u, w} B S hS) (h𝒳 : IsWellNighAffine.{u, w} B S hS 𝒳) :
    ∃ (M : AlgebraicSpaces B S hS)
      (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS M.obj M.property),
      IsUniformCategoricalModuliSpaceIn B S hS (fun W => Space.IsAffineSpace B S hS W.obj) M
          f.hom ∧
        AlgebraicStacks.IsSeparated B S hS f ∧ IsQuasiCompactMorphism.{u, w} B S hS f ∧
          UniversalHomeomorphism B S hS f

Tag 0DUQ, a lemma

Tag 0DUQ in the Stacks Project.

AlgebraicGeometry.Stack.exists_isTwoFibreProduct_moduliSpace_of_isEtale_of_inducesIsomorphismAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineEtaleModuliSquare.lean, line 244.

Stacks 0DUQ. Let h : 𝒳' ⟶ 𝒳 be a morphism of algebraic stacks. Assume 𝒳' and 𝒳 are well-nigh affine, h is étale, and h induces isomorphisms on automorphism groups (Stacks 0DTW). Then there exists a cartesian diagram

𝒳' ⟶ 𝒳
↓     ↓
M' ⟶ M

where M' ⟶ M is étale and the vertical arrows are moduli spaces as constructed in Stacks 0DUP: uniform categorical moduli spaces in affine schemes, separated, quasi-compact and universal homeomorphisms.

theorem exists_isTwoFibreProduct_moduliSpace_of_isEtale_of_inducesIsomorphismAt
    {𝒳 𝒳' : AlgebraicStacks.{u, w} B S hS} (h : 𝒳' ⟶ 𝒳)
    (h𝒳 : IsWellNighAffine.{u, w} B S hS 𝒳) (h𝒳' : IsWellNighAffine.{u, w} B S hS 𝒳')
    (he : IsEtale B S hS h)
    (hauto : ∀ q : points B S hS 𝒳'.val.val 𝒳'.val.isFiberedInGroupoids,
      InducesIsomorphismAt B S hS h q) :
    ∃ (M M' : BigFppfOver B S hS)
      (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS (yoneda.obj M) (isAlgebraicSpace_yoneda B S hS M))
      (f' : 𝒳' ⟶
        algebraicSpaceStack.{u, w} B S hS (yoneda.obj M') (isAlgebraicSpace_yoneda B S hS M'))
      (g : M' ⟶ M) (hcomm : f'.hom ≫ (associatedMap B S hS (yoneda.map g)).1 = h.hom ≫ f.hom),
      Etale ((BigFppfOver.toScheme B S hS).map g) ∧
      Nonempty (Bicategory.IsTwoFibreProduct
        (ChartBaseChange.moduliSquare h g f.hom f'.hom hcomm)) ∧
      (IsUniformCategoricalModuliSpaceIn B S hS (fun W => Space.IsAffineSpace B S hS W.obj)
          (schemeSpace M) f.hom ∧
        AlgebraicStacks.IsSeparated B S hS f ∧ IsQuasiCompactMorphism.{u, w} B S hS f ∧
          UniversalHomeomorphism B S hS f) ∧
      (IsUniformCategoricalModuliSpaceIn B S hS (fun W => Space.IsAffineSpace B S hS W.obj)
          (schemeSpace M') f'.hom ∧
        AlgebraicStacks.IsSeparated B S hS f' ∧ IsQuasiCompactMorphism.{u, w} B S hS f' ∧
          UniversalHomeomorphism B S hS f')

Tag 0DUR, a lemma

Tag 0DUR in the Stacks Project.

AlgebraicGeometry.Stack.isUniformCategoricalModuliSpace_of_isWellNighAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineUniformModuliSpace.lean, line 104.

Stacks 0DUR. Let 𝒳 be a well-nigh affine algebraic stack. The morphism f : 𝒳 ⟶ M of Stacks 0DUP is a uniform categorical moduli space.

The first clause is the morphism of Stacks 0DUP with all the properties that lemma gives it, and the conclusion of Stacks 0DUR. The second clause says the same of every 1-morphism to an algebraic space which is a uniform categorical moduli space in the category of affine algebraic spaces, the property by which Stacks 0DUP characterizes its morphism up to unique isomorphism.

theorem isUniformCategoricalModuliSpace_of_isWellNighAffine (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsWellNighAffine.{u, w} B S hS 𝒳) :
    (∃ (M : AlgebraicSpaces B S hS) (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS M.obj M.property),
        IsUniformCategoricalModuliSpaceIn B S hS (fun W => Space.IsAffineSpace B S hS W.obj) M
            f.hom ∧
          AlgebraicStacks.IsSeparated B S hS f ∧ IsQuasiCompactMorphism.{u, w} B S hS f ∧
          UniversalHomeomorphism B S hS f ∧ IsUniformCategoricalModuliSpace B S hS M f.hom) ∧
      ∀ (M : AlgebraicSpaces B S hS) (f : 𝒳.val ⟶ fibredCategory B S hS M.obj),
        IsUniformCategoricalModuliSpaceIn B S hS (fun W => Space.IsAffineSpace B S hS W.obj)
          M f →
        IsUniformCategoricalModuliSpace B S hS M f

Tag 0DUS, a lemma

Tag 0DUS in the Stacks Project.

AlgebraicGeometry.Stack.exists_isTwoFibreProduct_moduliSpace_of_isEtale_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/EtaleSeparatedModuliSquare.lean, line 176.

Stacks 0DUS. Let h : 𝒳' ⟶ 𝒳 be a morphism of algebraic stacks. Assume 𝒳 is well-nigh affine, h is étale, h is separated, and h induces isomorphisms on automorphism groups (Stacks 0DTW). Then there exists a cartesian diagram

𝒳' ⟶ 𝒳
↓     ↓
M' ⟶ M

where M' ⟶ M is a separated étale morphism of schemes and 𝒳 ⟶ M is the moduli space constructed in Stacks 0DUP: a uniform categorical moduli space in affine schemes, separated, quasi-compact and a universal homeomorphism.

theorem exists_isTwoFibreProduct_moduliSpace_of_isEtale_of_isSeparated
    {𝒳 𝒳' : AlgebraicStacks.{u, w} B S hS} (h : 𝒳' ⟶ 𝒳)
    (h𝒳 : IsWellNighAffine.{u, w} B S hS 𝒳)
    (he : IsEtale B S hS h) (hsep : AlgebraicStacks.IsSeparated B S hS h)
    (hauto : ∀ q : points B S hS 𝒳'.val.val 𝒳'.val.isFiberedInGroupoids,
      InducesIsomorphismAt B S hS h q) :
    ∃ (M M' : BigFppfOver B S hS)
      (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS (yoneda.obj M) (isAlgebraicSpace_yoneda B S hS M))
      (f' : 𝒳' ⟶
        algebraicSpaceStack.{u, w} B S hS (yoneda.obj M') (isAlgebraicSpace_yoneda B S hS M'))
      (g : M' ⟶ M) (hcomm : f'.hom ≫ (associatedMap B S hS (yoneda.map g)).1 = h.hom ≫ f.hom),
      Etale ((BigFppfOver.toScheme B S hS).map g) ∧
      _root_.AlgebraicGeometry.IsSeparated ((BigFppfOver.toScheme B S hS).map g) ∧
      Nonempty (Bicategory.IsTwoFibreProduct
        (ChartBaseChange.moduliSquare h g f.hom f'.hom hcomm)) ∧
      (IsUniformCategoricalModuliSpaceIn B S hS (fun W => Space.IsAffineSpace B S hS W.obj)
          ⟨yoneda.obj M, isAlgebraicSpace_yoneda B S hS M⟩ f.hom ∧
        AlgebraicStacks.IsSeparated B S hS f ∧ IsQuasiCompactMorphism.{u, w} B S hS f ∧
          UniversalHomeomorphism B S hS f)

Tag 0DUE, a lemma

Tag 0DUE in the Stacks Project.

AlgebraicGeometry.Stack.exists_isWellNighAffine_etale_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WellNighAffineEtaleCover.lean, line 96.

Stacks 0DUE. Let 𝒳 be an algebraic stack over S whose inertia projection I_𝒳 ⟶ 𝒳 is finite. Then there are a set I and, for i ∈ I, 1-morphisms of algebraic stacks g_i : 𝒳_i ⟶ 𝒳 such that

1. |𝒳| = ⋃ |g_i|(|𝒳_i|),
2. 𝒳_i is well-nigh affine (Stacks 0DUL),
3. I_{𝒳_i} ⟶ 𝒳_i ×_𝒳 I_𝒳 is an isomorphism (equivalently, by Stacks 0DU9, g_i induces an isomorphism between automorphism groups at every point of 𝒳_i),
4. g_i is representable by algebraic spaces, separated (Stacks 04YW) and étale.

theorem exists_isWellNighAffine_etale_cover (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hI : AlgebraicStacks.IsFinite B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳)) :
    ∃ (ι : Type (u + 1)) (𝒳ᵢ : ι → AlgebraicStacks.{u, w} B S hS) (g : ∀ i, 𝒳ᵢ i ⟶ 𝒳),
      (∀ x : AlgebraicStacks.points B S hS 𝒳,
        ∃ (i : ι) (y : AlgebraicStacks.points B S hS (𝒳ᵢ i)),
          AlgebraicStacks.pointsMap B S hS (g i) y = x) ∧
      (∀ i, IsWellNighAffine.{u, w} B S hS (𝒳ᵢ i)) ∧
      (∀ i, IsStabilizerPreserving B S hS (g i) ∧
        ∀ q : AlgebraicStacks.points B S hS (𝒳ᵢ i), InducesIsomorphismAt B S hS (g i) q) ∧
      (∀ i, IsRepresentableByAlgebraicSpaces B S hS (g i).hom.hom ∧
        AlgebraicStacks.IsSeparated B S hS (g i) ∧ IsEtale B S hS (g i))

Tag 0DUT, a theorem

Tag 0DUT in the Stacks Project.

AlgebraicGeometry.Stack.exists_isUniformCategoricalModuliSpace_of_isFinite_inertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/KeelMori/KeelMoriTheorem.lean, line 66.

Stacks 0DUT (Keel–Mori). Let 𝒳 be an algebraic stack whose inertia I_𝒳 ⟶ 𝒳 is finite. Then there exists a uniform categorical moduli space f : 𝒳 ⟶ M, and f is separated, quasi-compact, and a universal homeomorphism.

theorem exists_isUniformCategoricalModuliSpace_of_isFinite_inertia
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hI : AlgebraicStacks.IsFinite B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳)) :
    ∃ (M : AlgebraicSpaces B S hS) (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS M.obj M.property),
      IsUniformCategoricalModuliSpace B S hS M f.hom ∧ AlgebraicStacks.IsSeparated B S hS f ∧
        IsQuasiCompactMorphism.{u, w} B S hS f ∧ UniversalHomeomorphism B S hS f

Tag 0DUV, a lemma

Tag 0DUV in the Stacks Project.

AlgebraicGeometry.Stack.exists_isTwoFibreProduct_keelMoriModuliSpace_of_isEtale_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/KeelMoriEtaleLocal/EtaleMorphismModuliSquare.lean, line 62.

Stacks 0DUV. Let h : 𝒳' ⟶ 𝒳 be a 1-morphism of algebraic stacks. Assume that the inertia I_𝒳 ⟶ 𝒳 is finite, and that h is étale, separated, and induces isomorphisms between automorphism groups at every point (Stacks 0DTW). Then there are moduli spaces f : 𝒳 ⟶ M and f' : 𝒳' ⟶ M' as in Theorem 0DUT (uniform categorical moduli spaces which are separated, quasi-compact and universal homeomorphisms) and a separated étale morphism g : M' ⟶ M of algebraic spaces with f' ≫ g = h ≫ f, such that the square 𝒳' ⟶ 𝒳 over g is a 2-fibre product.

theorem exists_isTwoFibreProduct_keelMoriModuliSpace_of_isEtale_of_isSeparated
    {𝒳 𝒳' : AlgebraicStacks.{u, w} B S hS} (h : 𝒳' ⟶ 𝒳)
    (hI : AlgebraicStacks.IsFinite B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳))
    (he : IsEtale B S hS h) (hsep : AlgebraicStacks.IsSeparated B S hS h)
    (hauto : ∀ q : points B S hS 𝒳'.val.val 𝒳'.val.isFiberedInGroupoids,
      InducesIsomorphismAt B S hS h q) :
    ∃ (M M' : AlgebraicSpaces B S hS)
      (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS M.obj M.property)
      (f' : 𝒳' ⟶ algebraicSpaceStack.{u, w} B S hS M'.obj M'.property) (g : M' ⟶ M)
      (hcomm : f'.hom ≫ (associatedMap B S hS g.hom).1 = h.hom ≫ f.hom),
      Space.IsEtale B S hS g.hom ∧ Space.IsSeparated B S hS g.hom ∧
      Nonempty (Bicategory.IsTwoFibreProduct
        (⟨𝒳'.val, f'.hom, h.hom, eqToIso hcomm⟩ :
          Bicategory.TwoCommSq (associatedMap B S hS g.hom).1 f.hom)) ∧
      (IsUniformCategoricalModuliSpace B S hS M f.hom ∧ AlgebraicStacks.IsSeparated B S hS f ∧
        IsQuasiCompactMorphism.{u, w} B S hS f ∧ UniversalHomeomorphism B S hS f) ∧
      (IsUniformCategoricalModuliSpace B S hS M' f'.hom ∧ AlgebraicStacks.IsSeparated B S hS f' ∧
        IsQuasiCompactMorphism.{u, w} B S hS f' ∧ UniversalHomeomorphism B S hS f')

Sources

• Section 106.13, Tag 0DUK
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.IsWellNighAffine · AlgebraicGeometry.Stack.isQuasiCompactStack_of_isWellNighAffine · AlgebraicGeometry.Stack.HasAffineFiniteLocallyFreeGroupoidPresentation · AlgebraicGeometry.Stack.isAbsolutelyQuasiDM_of_representedGroupoid_isFiniteLocallyFree · AlgebraicGeometry.Stack.isSeparatedOver_of_representedGroupoid_isFiniteLocallyFree · AlgebraicGeometry.Stack.isAbsolutelySeparated_of_representedGroupoid_isFiniteLocallyFree · AlgebraicGeometry.Stack.isWellNighAffine_iff_and_isQuasiCompact_isQuasiDM_isSeparated · AlgebraicGeometry.Stack.isWellNighAffine_of_isAffineHom

Section106.14 Properties of moduli spaces#

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

Tag 0DUX, a lemma

Tag 0DUX in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyOfFiniteType_of_isCategoricalModuliSpace_of_isFinite_inertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/KeelMori/ModuliFiniteType.lean, line 54.

Stacks 0DUX. Let p : 𝒳 ⟶ Y be a 1-morphism from an algebraic stack to an algebraic space such that the inertia I_𝒳 ⟶ 𝒳 is finite, Y is locally Noetherian and p is locally of finite type, and let f : 𝒳 ⟶ M be a categorical moduli space (for instance the moduli space of Stacks 0DUT). Then p factors as f followed by a unique morphism M ⟶ Y, up to a 2-isomorphism, and that morphism M ⟶ Y is locally of finite type.

theorem isLocallyOfFiniteType_of_isCategoricalModuliSpace_of_isFinite_inertia
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hI : AlgebraicStacks.IsFinite B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳))
    (Y : AlgebraicSpaces B S hS)
    (hY : Space.HasEtaleLocalProperty B S hS Y.obj (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (p : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS Y.obj Y.property)
    (hp : AlgebraicStacks.IsLocallyOfFiniteType B S hS p)
    (M : AlgebraicSpaces B S hS) (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS M.obj M.property)
    (hf : IsCategoricalModuliSpace B S hS M f.hom) :
    (∃! q : M ⟶ Y, Nonempty (f.hom ≫ (associatedMap B S hS q.hom).1 ≅ p.hom)) ∧
      ∀ q : M ⟶ Y, Nonempty (f.hom ≫ (associatedMap B S hS q.hom).1 ≅ p.hom) →
        Space.IsLocallyOfFiniteType B S hS q.hom

Tag 0DUY, a lemma

Tag 0DUY in the Stacks Project.

AlgebraicGeometry.Stack.isAbsolutelyQuasiSeparated_and_isAbsolutelySeparated_of_isFinite_inertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliSeparation/KeelMoriModuliSpaceSeparation.lean, line 77.

Stacks 0DUY. Let 𝒳 be an algebraic stack whose inertia I_𝒳 ⟶ 𝒳 is finite, and let f : 𝒳 ⟶ M be a categorical moduli space — for instance the moduli space constructed in Stacks 0DUT, which every categorical moduli space of 𝒳 is up to unique isomorphism. Then 1. if 𝒳 is quasi-separated, then M is quasi-separated; 2. if 𝒳 is separated, then M is separated.

Both properties are absolute, over the terminal scheme Spec ℤ (Stacks 050D parts (8), (7) and Stacks 03BS parts (3), (1)). Part (3) of the source ("Add more here") asserts nothing.

theorem isAbsolutelyQuasiSeparated_and_isAbsolutelySeparated_of_isFinite_inertia
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hI : AlgebraicStacks.IsFinite B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳))
    (M : AlgebraicSpaces B S hS) (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS M.obj M.property)
    (hf : IsCategoricalModuliSpace B S hS M f.hom) :
    (AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒳 →
        Space.IsAbsolutelyQuasiSeparated B S hS hZ M.obj) ∧
      (AlgebraicStacks.IsAbsolutelySeparated.{u, w} B S hS hZ 𝒳 →
        Space.IsAbsolutelySeparated B S hS hZ M.obj)

AlgebraicGeometry.Stack.isAbsolutelyQuasiSeparated_and_isAbsolutelySeparated_of_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliSeparation/ModuliSpaceSeparation.lean, line 148.

Stacks 0DUY. Let f : 𝒳 ⟶ M be a universal homeomorphism (Stacks 0CI7) from an algebraic stack over S to an algebraic space over S — for instance the moduli space of the Keel–Mori theorem (Stacks 0DUT) of an algebraic stack with finite inertia, which is a universal homeomorphism. Then 1. if 𝒳 is quasi-separated, then M is quasi-separated; 2. if 𝒳 is separated, then M is separated.

Both properties are absolute (Stacks 050D parts (7), (8) and Stacks 03BS parts (1), (3)). Part (3) of the source ("Add more here") asserts nothing.

theorem isAbsolutelyQuasiSeparated_and_isAbsolutelySeparated_of_universalHomeomorphism
    {𝒳 : AlgebraicStacks.{u, w} B S hS} {M : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hM : IsAlgebraicSpace B S hS M) (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS M hM)
    (hf : AlgebraicStacks.UniversalHomeomorphism B S hS f) :
    (AlgebraicStacks.IsAbsolutelyQuasiSeparated.{u, w} B S hS hZ 𝒳 →
        Space.IsAbsolutelyQuasiSeparated B S hS hZ M) ∧
      (AlgebraicStacks.IsAbsolutelySeparated.{u, w} B S hS hZ 𝒳 →
        Space.IsAbsolutelySeparated B S hS hZ M)

Tag 0DUZ, a lemma

Tag 0DUZ in the Stacks Project.

AlgebraicGeometry.Stack.isProper_of_isCategoricalModuliSpace_of_isFinite_inertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliProperness/ModuliSpaceProper.lean, line 74.

Stacks 0DUZ. Let p : 𝒳 ⟶ Y be a 1-morphism from an algebraic stack to an algebraic space. Assume 1. I_𝒳 ⟶ 𝒳 is finite, 2. p is proper, and 3. Y is locally Noetherian.

Let f : 𝒳 ⟶ M be a categorical moduli space — for instance the moduli space constructed in Stacks 0DUT, which every categorical moduli space of 𝒳 is up to unique isomorphism. Then p factors as f followed by a unique morphism M ⟶ Y of algebraic spaces, up to a 2-isomorphism, and M ⟶ Y is proper.

theorem isProper_of_isCategoricalModuliSpace_of_isFinite_inertia
    (𝒳 : AlgebraicStacks.{u, w} B S hS)
    (hI : AlgebraicStacks.IsFinite B S hS (inertiaProjectionAlgebraicStacks B S hS 𝒳))
    (Y : AlgebraicSpaces B S hS)
    (hY : Space.HasEtaleLocalProperty B S hS Y.obj (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (p : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS Y.obj Y.property)
    (hp : AlgebraicStacks.IsProper B S hS p)
    (M : AlgebraicSpaces B S hS) (f : 𝒳 ⟶ algebraicSpaceStack.{u, w} B S hS M.obj M.property)
    (hf : IsCategoricalModuliSpace B S hS M f.hom) :
    (∃! g : M ⟶ Y, Nonempty (f.hom ≫ (associatedMap B S hS g.hom).1 ≅ p.hom)) ∧
      ∀ g : M ⟶ Y, Nonempty (f.hom ≫ (associatedMap B S hS g.hom).1 ≅ p.hom) →
        Space.IsProper B S hS g.hom

Sources

• Section 106.14, Tag 0DUW
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isLocallyOfFiniteType_of_isCategoricalModuliSpace_of_isFinite_inertia · AlgebraicGeometry.Stack.isAbsolutelyQuasiSeparated_and_isAbsolutelySeparated_of_isFinite_inertia · AlgebraicGeometry.Stack.isAbsolutelyQuasiSeparated_and_isAbsolutelySeparated_of_universalHomeomorphism · AlgebraicGeometry.Stack.isProper_of_isCategoricalModuliSpace_of_isFinite_inertia

Section106.15 Stacks and fpqc coverings#

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

Tag 0GRH, a proposition

Tag 0GRH in the Stacks Project.

AlgebraicGeometry.Stack.isStack_fpqc_of_isQuasiAffineHom_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FpqcDescent/Stack.lean, line 159.

Stacks 0GRH. An algebraic stack 𝒳 over S with quasi-affine diagonal satisfies descent for fpqc coverings: it is a stack for the fpqc topology of the big fppf site over S.

theorem isStack_fpqc_of_isQuasiAffineHom_diagonal
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (hΔ : IsQuasiAffineHom B S hS (diagonal.{u, u, u} B S hS 𝒳)) :
    𝒳.val.p.IsStack
      ((Scheme.fpqcPrecoverage.comap (BigFppfOver.toScheme B S hS)).toGrothendieck)

AlgebraicGeometry.Stack.isMorSheaf_fpqc_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomSpaceFpqcSheaf.lean, line 131. The attribute's comment: “the full-faithfulness half of the proof: condition (2) of the fpqc stack condition, that the presheaves Mor(x, y) = Isom(x, y) of an algebraic stack are sheaves for the fpqc topology. No hypothesis on the diagonal is carried: representability of the diagonal by algebraic spaces, which every algebraic stack has, already suffices for this half, so the quasi-affine diagonal of the source and the ind-quasi-affine diagonal of its footnote are both dropped. The essential-surjectivity half, effectivity of fpqc descent data, is not formalized.”.

The full-faithfulness half of Stacks 0GRH: condition (2) of the fpqc stack condition for an algebraic stack. For every scheme U over S and all objects x, y of the fibre of an algebraic stack 𝒳 over U, the presheaf Mor(x, y) of Stacks 02ZB is a sheaf for the fpqc topology on the localization at U.

theorem isMorSheaf_fpqc_of_isAlgebraicStack
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (U : BigFppfOver B S hS) (x y : 𝒳.val.p.Fiber U) :
    haveI : 𝒳.val.p.IsFibered := 𝒳.isFiberedInGroupoids.isFibered
    𝒳.val.p.IsMorSheaf
      ((Scheme.fpqcPrecoverage.comap (BigFppfOver.toScheme B S hS)).toGrothendieck) U x y

Sources

• Section 106.15, Tag 0GRG
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isStack_fpqc_of_isQuasiAffineHom_diagonal · AlgebraicGeometry.Stack.isMorSheaf_fpqc_of_isAlgebraicStack

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.