101.3 Properties of diagonals to 101.6 Higher diagonals

Section101.3 Properties of diagonals#

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

Tag 04XR, a lemma

Tag 04XR in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyOfFiniteType_isomPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomPresheafFiniteType.lean, line 318.

Let 𝒳 be an algebraic stack over S, let T be an object of the big fppf site of S and let x, y be two objects of the fibre of 𝒳 over T. Then the structural morphism of the isomorphism sheaf Isom(x, y), read over T, is locally of finite type.

theorem isLocallyOfFiniteType_isomPresheaf
    (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)
    (T : BigFppfOver B S hS) :
    letI : 𝒳.val.p.IsFibered := 𝒳.isFiberedInGroupoids.isFibered
    ∀ x y : 𝒳.val.p.Fiber T,
      Space.IsLocallyOfFiniteType B T.left.1 T.left.2
        (terminal.from ((Over.iteratedSliceBackward T).op ⋙ 𝒳.val.p.isomPresheaf x y))

Tag 04YP, a lemma

Tag 04YP in the Stacks Project.

AlgebraicGeometry.Stack.isomSpaceOver_isGroupAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomGroupAlgebraicSpace.lean, line 49. The attribute's comment: “part (1): Isom(y, y) is a group algebraic space over T”.

Stacks 04YP, part (1). For an object y of the fibre category of an algebraic stack 𝒳 over a scheme T of the big fppf site of S, Isom_𝒳(y, y) is a group algebraic space over T: the group object Isom_𝒳(y, y) over the base AlgebraicGeometry.Stack.siteTerminalSpace, with the group structure AlgebraicGeometry.Stack.isomSpaceOverGrpObj, is (on the nose) an object of the category AlgebraicGeometry.Space.GroupAlgebraicSpace of group algebraic spaces over T, and its multiplication is composition of local automorphisms (AlgebraicGeometry.Stack.isomSpaceComp).

theorem isomSpaceOver_isGroupAlgebraicSpace (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)
    (U : BigFppfOver B S hS) (y : 𝒳.val.p.Fiber U) :
    letI : GrpObj (isomSpaceOver B S hS 𝒳 U y y) := isomSpaceOverGrpObj B S hS 𝒳 U y
    (∃ G : Space.GroupAlgebraicSpace B U.left.1 U.left.2 (siteTerminalSpace B S hS U)
        (isAlgebraicSpace_yoneda B U.left.1 U.left.2
          (⊤_ (BigFppfOver B U.left.1 U.left.2))),
        G.obj = Grp.mk (isomSpaceOver B S hS 𝒳 U y y)) ∧
      ∀ (Q : Over (siteTerminalSpace B S hS U)) (a b : Q ⟶ isomSpaceOver B S hS 𝒳 U y y)
        (V : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ) (t : Q.left.obj V),
        ((CartesianMonoidalCategory.lift a b ≫
          MonObj.mul (X := isomSpaceOver B S hS 𝒳 U y y)).left.app V) t =
          isomSpaceComp B S hS 𝒳 U y V ((a.left.app V) t) ((b.left.app V) t)

AlgebraicGeometry.Stack.isomSpaceOverGrpObj_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomGroupSpace.lean, line 692. The attribute's comment: “part (1): the group law is composition of automorphisms”.

The group law of Isom_𝒳(y, y) is composition of local automorphisms. On a pair of sections of Isom_𝒳(y, y) over a test object Q, the multiplication of AlgebraicGeometry.Stack.isomSpaceOverGrpObj is AlgebraicGeometry.Stack.isomSpaceComp, i.e. reverse categorical composition.

theorem isomSpaceOverGrpObj_mul (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1}
      (BigFppfOver B S hS))
    (U : BigFppfOver B S hS)
    (y : 𝒳.val.p.Fiber U)
    (Q : Over (siteTerminalSpace B S hS U))
    (a b : Q ⟶ isomSpaceOver B S hS 𝒳 U y y)
    (V : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ) (t : Q.left.obj V) :
    (letI : GrpObj (isomSpaceOver B S hS 𝒳 U y y) :=
      isomSpaceOverGrpObj B S hS 𝒳 U y;
      ((CartesianMonoidalCategory.lift a b ≫
        MonObj.mul (X := isomSpaceOver B S hS 𝒳 U y y)).left.app V) t =
      isomSpaceComp B S hS 𝒳 U y V
        ((a.left.app V) t)
        ((b.left.app V) t))

AlgebraicGeometry.Stack.isomSpaceOverModObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomGroupSpace.lean, line 719. The attribute's comment: “part (2): the action by postcomposition”.

Stacks 04YP, part (2): the action. Isom_𝒳(y, y) acts on Isom_𝒳(x, y) over AlgebraicGeometry.Stack.siteTerminalSpace, by postcomposition.

noncomputable def isomSpaceOverModObj
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1}
      (BigFppfOver B S hS))
    (U : BigFppfOver B S hS)
    (x y : 𝒳.val.p.Fiber U) :
    let G := isomSpaceOver B S hS 𝒳 U y y
    let P := isomSpaceOver B S hS 𝒳 U x y
    letI : GrpObj G := isomSpaceOverGrpObj B S hS 𝒳 U y
    ModObj G P

AlgebraicGeometry.Stack.isomSpaceOverModObj_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomGroupSpace.lean, line 752. The attribute's comment: “part (2): the action is postcomposition”.

The action of Isom_𝒳(y, y) on Isom_𝒳(x, y) is postcomposition. On a section of Isom_𝒳(y, y) and a section of Isom_𝒳(x, y) over a test object Q, the action of AlgebraicGeometry.Stack.isomSpaceOverModObj is AlgebraicGeometry.Stack.isomSpaceSmul.

theorem isomSpaceOverModObj_smul
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1}
      (BigFppfOver B S hS))
    (U : BigFppfOver B S hS)
    (x y : 𝒳.val.p.Fiber U)
    (Q : Over (siteTerminalSpace B S hS U))
    (g : Q ⟶ isomSpaceOver B S hS 𝒳 U y y)
    (p : Q ⟶ isomSpaceOver B S hS 𝒳 U x y)
    (V : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ) (t : Q.left.obj V) :
    (letI : GrpObj (isomSpaceOver B S hS 𝒳 U y y) :=
      isomSpaceOverGrpObj B S hS 𝒳 U y;
      letI : ModObj (isomSpaceOver B S hS 𝒳 U y y)
        (isomSpaceOver B S hS 𝒳 U x y) :=
        isomSpaceOverModObj B S hS 𝒳 U x y;
      ((CartesianMonoidalCategory.lift g p ≫
        ModObj.smul (M := isomSpaceOver B S hS 𝒳 U y y)
          (X := isomSpaceOver B S hS 𝒳 U x y)).left.app V) t) =
      isomSpaceSmul B S hS 𝒳 U x y V ((p.left.app V) t) ((g.left.app V) t)

AlgebraicGeometry.Stack.isomSpaceOver_isPseudoTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomGroupSpace.lean, line 810. The attribute's comment: “part (2): isomorphism pseudo-torsor”.

Stacks 04YP, part (2). Isom_𝒳(x, y) is a pseudo-torsor under Isom_𝒳(y, y) over U: the shear map (g, p) ↦ (p ≫ g, p) is an isomorphism, because for two local isomorphisms p, q : x ⟶ y the unique local automorphism g of y with p ≫ g = q is p⁻¹ ≫ q.

theorem isomSpaceOver_isPseudoTorsor
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1}
      (BigFppfOver B S hS))
    (U : BigFppfOver B S hS) (x y : 𝒳.val.p.Fiber U) :
    let G := isomSpaceOver B S hS 𝒳 U y y
    let P := isomSpaceOver B S hS 𝒳 U x y
    letI : GrpObj G := isomSpaceOverGrpObj B S hS 𝒳 U y
    letI : ModObj G P := isomSpaceOverModObj B S hS 𝒳 U x y
    IsPseudoTorsor G P

AlgebraicGeometry.Stack.automorphismGroupSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomGroupSpace.lean, line 868. The attribute's comment: “part (1): automorphism group algebraic space”.

Stacks 04YP, part (1). For an object y of the fibre category of an algebraic stack 𝒳 over a scheme T of the big fppf site of S, the automorphisms of y form a group algebraic space over T: the presheaf Isom_𝒳(y, y) is an algebraic space (AlgebraicGeometry.Stack.isAlgebraicSpace_isomSpace) and it carries the group object structure AlgebraicGeometry.Stack.isomSpaceOverGrpObj, whose law is composition of local automorphisms by AlgebraicGeometry.Stack.isomSpaceOverGrpObj_mul.

def automorphismGroupSpace (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)
    (U : BigFppfOver B S hS) (y : 𝒳.val.p.Fiber U) :
    Space.GroupAlgebraicSpace B U.left.1 U.left.2 (siteTerminalSpace B S hS U)
      (isAlgebraicSpace_yoneda B U.left.1 U.left.2
        (⊤_ (BigFppfOver B U.left.1 U.left.2)))

Tag 04XS, a lemma

Tag 04XS in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyOfFiniteType_relativeDiagonal_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDiagonalFiniteType.lean, line 266. The attribute's comment: “diagonal_locally_finite_type”.

Stacks 04XS, part (2). The relative diagonal of a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over the big fppf site of S is locally of finite type: it is representable by algebraic spaces, and every algebraic space representing one of its base changes along a scheme-valued point of 𝒳 ×_{f, 𝒴, f} 𝒳 has locally-of-finite-type structural morphism — the every-étale-chart form of part (1) of Stacks 03XF.

No hypothesis is placed on f; part (2) of Stacks 04YQ is the same statement for a 1-morphism representable by algebraic spaces.

theorem isLocallyOfFiniteType_relativeDiagonal_of_isAlgebraicStack
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴) :
    ∃ _hΔ : IsRepresentableByAlgebraicSpaces B S hS
        (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom),
      ∀ (U : BigFppfOver B S hS)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤
          (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.obj)
        (_hy : y ⋙ (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).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.val.p
            (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.p y
            (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom).toFunctor)
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.IsLocallyOfFiniteType B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_relativeDiagonal_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDiagonalRepresentable.lean, line 103. The attribute's comment: “diagonal_representable”.

Stacks 04XS, part (1). The relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 of a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over the big fppf site of S is representable by algebraic spaces.

Only the representability of the absolute diagonals of 𝒳 and of 𝒴 — the second clause of AlgebraicGeometry.Stack.IsAlgebraicStack — is used, by AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_relativeDiagonal.

theorem isRepresentableByAlgebraicSpaces_relativeDiagonal_of_isAlgebraicStack
    (𝒳 𝒴 : CatFiberedInGroupoids.{u, max u v, u + 1, max (max (u + 1) w) v}
      (BigFppfOver B S hS))
    (f : 𝒳 ⟶ 𝒴)
    (h𝒳 : IsAlgebraicStack.{u, t} B S hS 𝒳.val)
    (h𝒴 : IsAlgebraicStack.{u, t} B S hS 𝒴.val) :
    IsRepresentableByAlgebraicSpaces B S hS
      (relativeDiagonalBasedFunctor B S hS 𝒳 𝒴 f.hom)

Tag 04YQ, a lemma

Tag 04YQ in the Stacks Project.

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

Stacks 04YQ, part (3). The relative diagonal of a 1-morphism of algebraic stacks over the big fppf site of S which is representable by algebraic spaces is a monomorphism: it is representable by algebraic spaces, and every algebraic space representing one of its base changes along a scheme-valued point of 𝒳 ×_{f, 𝒴, f} 𝒳 has monomorphic structural morphism.

theorem mono_relativeDiagonal_of_isRepresentableByAlgebraicSpaces
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    ∃ _hΔ : IsRepresentableByAlgebraicSpaces B S hS
        (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom),
      ∀ (U : BigFppfOver B S hS)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤
          (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.obj)
        (_hy : y ⋙ (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).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.val.p
            (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.p y
            (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom).toFunctor)
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Mono (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩))

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

Stacks 04YQ, part (4). The relative diagonal of a 1-morphism of algebraic stacks over the big fppf site of S which is representable by algebraic spaces is separated: it is representable by algebraic spaces, and every algebraic space representing one of its base changes along a scheme-valued point of 𝒳 ×_{f, 𝒴, f} 𝒳 has separated structural morphism.

By part (3) that structural morphism is a monomorphism, and a monomorphism of algebraic spaces is separated (Stacks 042N).

theorem isSeparated_relativeDiagonal_of_isRepresentableByAlgebraicSpaces
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    ∃ _hΔ : IsRepresentableByAlgebraicSpaces B S hS
        (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom),
      ∀ (U : BigFppfOver B S hS)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤
          (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.obj)
        (_hy : y ⋙ (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).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.val.p
            (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.p y
            (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom).toFunctor)
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.IsSeparated B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

AlgebraicGeometry.Stack.isLocallyQuasiFinite_relativeDiagonal_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDiagonalQuasiFinite.lean, line 195. The attribute's comment: “part (5): locally quasi-finite”.

Stacks 04YQ, part (5). The relative diagonal of a 1-morphism of algebraic stacks over the big fppf site of S which is representable by algebraic spaces is locally quasi-finite: it is representable by algebraic spaces, and every algebraic space representing one of its base changes along a scheme-valued point of 𝒳 ×_{f, 𝒴, f} 𝒳 has locally quasi-finite structural morphism.

That structural morphism is a monomorphism by part (3) and its represented base changes are locally of finite type by part (2) for a representable 1-morphism (AlgebraicGeometry.Stack.presheaf_locallyOfFiniteType_relativeDiagonal), so Stacks 0463 applies.

theorem isLocallyQuasiFinite_relativeDiagonal_of_isRepresentableByAlgebraicSpaces :
    ∃ _hΔ : IsRepresentableByAlgebraicSpaces B S hS
        (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom),
      ∀ (U : BigFppfOver B S hS)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤
          (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.obj)
        (_hy : y ⋙ (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).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.val.p
            (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.p y
            (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom).toFunctor)
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.IsLocallyQuasiFinite B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

AlgebraicGeometry.Stack.isLocallyOfFiniteType_relativeDiagonal_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDiagonalQuasiFinite.lean, line 236. The attribute's comment: “part (2): locally of finite type”.

Stacks 04YQ, part (2). The relative diagonal of a 1-morphism of algebraic stacks over the big fppf site of S which is representable by algebraic spaces is locally of finite type: it is representable by algebraic spaces, and every algebraic space representing one of its base changes along a scheme-valued point of 𝒳 ×_{f, 𝒴, f} 𝒳 has locally-of-finite-type structural morphism — the every-étale-chart form of part (1) of Stacks 03XF.

This is read off part (5), the every-chart condition being monotone in the tested property of scheme morphisms, local finite type being the first conjunct of the meet part (5) is proved at.

The hypothesis is the source's own: Stacks 04YQ asserts all five parts for a 1-morphism representable by algebraic spaces. The statement asserted for an arbitrary 1-morphism of algebraic stacks is part (2) of Stacks 04XS, which rests on Stacks 04XR and is proved in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDiagonalFiniteType.lean; see the implementation notes.

theorem isLocallyOfFiniteType_relativeDiagonal_of_isRepresentableByAlgebraicSpaces :
    ∃ _hΔ : IsRepresentableByAlgebraicSpaces B S hS
        (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom),
      ∀ (U : BigFppfOver B S hS)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤
          (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.obj)
        (_hy : y ⋙ (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).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.val.p
            (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.p y
            (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom).toFunctor)
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.IsLocallyOfFiniteType B S hS (algebraicSpaceMap B S hS U
          ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

AlgebraicGeometry.Stack.isRepresentableMorphism_relativeDiagonal_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDiagonalRepresentableBySchemes.lean, line 316. The attribute's comment: “part (1): representable by schemes”.

The relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 of a 1-morphism f of algebraic stacks over the big fppf site of S which is representable by algebraic spaces is a representable 1-morphism in the sense of Stacks 02Y7 — representable by objects of the site, that is by schemes.

theorem isRepresentableMorphism_relativeDiagonal_of_isRepresentableByAlgebraicSpaces
    {𝒳 𝒴 : AlgebraicStacks.{u, t} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒳.val.val.p
      (twoFibreProduct B S hS 𝒴.val 𝒳.val 𝒳.val f.hom.hom f.hom.hom).val.p
      (relativeDiagonalBasedFunctor B S hS 𝒳.val 𝒴.val f.hom.hom).toFunctor

Tag 04YS, a lemma

Tag 04YS in the Stacks Project.

AlgebraicGeometry.Stack.isSeparated_relativeDiagonal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedDiagonalTFAE.lean, line 690.

Stacks 04YS. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S which is representable by algebraic spaces and write Δ_f : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 for its relative diagonal. The following are equivalent:

1. f is separated, in the relative sense of Stacks 04XB;
2. Δ_f is a closed immersion of algebraic stacks, part (2) of Stacks 04YL;
3. Δ_f is proper, in the relative sense of Stacks 04XB;
4. Δ_f is universally closed, in that sense.

theorem isSeparated_relativeDiagonal_tfae :
    List.TFAE
      [IsSeparated B S hS f.hom,
       AlgebraicStacks.IsClosedImmersion B S hS
         (Bicategory.InducedBicategory.mkHom
           (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom) :
             𝒳 ⟶ relativeDiagonalTargetStack B S hS 𝒳 𝒴 f),
       IsProper B S hS (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom),
       UniversallyClosed B S hS
         (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom)]

Tag 04YT, a lemma

Tag 04YT in the Stacks Project.

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

A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S which is representable by algebraic spaces is quasi-separated if and only if its relative diagonal Δ_f is quasi-compact.

theorem isQuasiSeparated_iff_isQuasiCompact_relativeDiagonal (f : 𝒵 ⟶ 𝒯)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    IsQuasiSeparated B S hS f ↔
      Stack.IsQuasiCompact.{u, u, u + 1} B S hS
        (Stack.relativeDiagonal.{u, u, u + 1} B S hS 𝒵.val 𝒯.val f.hom)

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiCompact_relativeDiagonal_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiSeparatedDiagonal.lean, line 120. The attribute's comment: “the implication (3) => (2)”.

If the relative diagonal Δ_f of a 1-morphism of algebraic stacks over S is of finite type, then it is quasi-compact.

theorem isQuasiCompact_relativeDiagonal_of_isFiniteType (f : 𝒵 ⟶ 𝒯)
    (h : Stack.IsFiniteType.{u, u, u + 1} B S hS
      (Stack.relativeDiagonal.{u, u, u + 1} B S hS 𝒵.val 𝒯.val f.hom)) :
    Stack.IsQuasiCompact.{u, u, u + 1} B S hS
      (Stack.relativeDiagonal.{u, u, u + 1} B S hS 𝒵.val 𝒯.val f.hom)

AlgebraicGeometry.Stack.AlgebraicStacks.isFiniteType_relativeDiagonal_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiSeparatedDiagonal.lean, line 130. The attribute's comment: “the implication (2) => (3)”.

If the relative diagonal Δ_f of a 1-morphism of algebraic stacks over S which is representable by algebraic spaces is quasi-compact, then it is of finite type.

theorem isFiniteType_relativeDiagonal_of_isQuasiCompact (f : 𝒵 ⟶ 𝒯)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom)
    (h : Stack.IsQuasiCompact.{u, u, u + 1} B S hS
      (Stack.relativeDiagonal.{u, u, u + 1} B S hS 𝒵.val 𝒯.val f.hom)) :
    Stack.IsFiniteType.{u, u, u + 1} B S hS
      (Stack.relativeDiagonal.{u, u, u + 1} B S hS 𝒵.val 𝒯.val f.hom)

Tag 04YU, a lemma

Tag 04YU in the Stacks Project.

AlgebraicGeometry.Stack.isLocallySeparated_iff_isImmersion_relativeDiagonalAlgebraicStacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocallySeparatedDiagonal.lean, line 233.

Stacks 04YU. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S which is representable by algebraic spaces. Then f is locally separated, in the relative sense of Stacks 04XB, if and only if its relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 is an immersion of algebraic stacks, part (3) of Stacks 04YL.

The content is AlgebraicGeometry.Stack.isLocallySeparated_iff_isImmersion_relativeDiagonal; the representability clause that part (3) of Stacks 04YL carries on top of the quantifier of Stacks 04XB is automatic, by part (1) of Stacks 04XS in the form AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_relativeDiagonal_algebraicStacks.

theorem isLocallySeparated_iff_isImmersion_relativeDiagonalAlgebraicStacks :
    IsLocallySeparated B S hS f.hom ↔
      AlgebraicStacks.IsImmersion B S hS (relativeDiagonalAlgebraicStacks B S hS f)

Sources

• Section 101.3, Tag 04XQ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isLocallyOfFiniteType_isomPresheaf · AlgebraicGeometry.Stack.isomSpaceOver_isGroupAlgebraicSpace · AlgebraicGeometry.Stack.isomSpaceOverGrpObj_mul · AlgebraicGeometry.Stack.isomSpaceOverModObj · AlgebraicGeometry.Stack.isomSpaceOverModObj_smul · AlgebraicGeometry.Stack.isomSpaceOver_isPseudoTorsor · AlgebraicGeometry.Stack.automorphismGroupSpace · AlgebraicGeometry.Stack.isLocallyOfFiniteType_relativeDiagonal_of_isAlgebraicStack

Section101.4 Separation axioms#

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

Tag 04YW, a definition

Tag 04YW in the Stacks Project.

AlgebraicGeometry.Stack.IsDM, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordMorphism.lean, line 68. The attribute's comment: “dm”.

Stacks 04YW, the DM condition. A 1-morphism of algebraic stacks over S is Deligne–Mumford when its relative diagonal is representable by algebraic spaces and unramified, the latter in the relative sense of Stacks 03YK: every algebraic space representing a base change of the diagonal along a scheme-valued point of 𝒳 ×_{f, 𝒴, f} 𝒳 has unramified structural morphism.

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

AlgebraicGeometry.Stack.AlgebraicStacks.IsQuasiDM, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAxioms.lean, line 119. The attribute's comment: “quasi_dm”.

Stacks 04YW, quasi-DM. A 1-morphism of algebraic stacks over S is quasi-DM when its relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 is locally quasi-finite in the sense of Stacks 04XB.

abbrev IsQuasiDM (f : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.AlgebraicStacks.IsSeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAxioms.lean, line 126. The attribute's comment: “separated”.

Stacks 04YW, separated. A 1-morphism of algebraic stacks over S is separated when its relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 is proper in the sense of Stacks 04XB.

abbrev IsSeparated (f : 𝒳 ⟶ 𝒴) : Prop

AlgebraicGeometry.Stack.AlgebraicStacks.IsQuasiSeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAxioms.lean, line 133. The attribute's comment: “quasi_separated”.

Stacks 04YW, quasi-separated. A 1-morphism of algebraic stacks over S is quasi-separated when its relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 is quasi-compact and quasi-separated, both in the sense of Stacks 04XB.

abbrev IsQuasiSeparated (f : 𝒳 ⟶ 𝒴) : Prop

Tag 050D, a definition

Tag 050D in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.IsAbsolutelyDM, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsolute.lean, line 88. The attribute's comment: “part (5): absolute DM”.

Stacks 050D, part (5). An algebraic stack is DM when it is DM over the terminal scheme Spec ℤ.

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

AlgebraicGeometry.Stack.AlgebraicStacks.IsAbsolutelyQuasiDM, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsolute.lean, line 94. The attribute's comment: “part (6): absolute quasi-DM”.

Stacks 050D, part (6). An algebraic stack is quasi-DM when it is quasi-DM over the terminal scheme Spec ℤ.

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

AlgebraicGeometry.Stack.AlgebraicStacks.IsAbsolutelySeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsolute.lean, line 100. The attribute's comment: “part (7): absolute separatedness”.

Stacks 050D, part (7). An algebraic stack is separated when it is separated over the terminal scheme Spec ℤ.

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

AlgebraicGeometry.Stack.AlgebraicStacks.IsAbsolutelyQuasiSeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsolute.lean, line 106. The attribute's comment: “part (8): absolute quasi-separatedness”.

Stacks 050D, part (8). An algebraic stack is quasi-separated when it is quasi-separated over the terminal scheme Spec ℤ.

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

AlgebraicGeometry.Stack.IsDMAbs, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsolute.lean, line 141. The attribute's comment: “part (5): DM”.

Stacks 050D, part (5). An algebraic stack is DM when it is DM over Spec(ℤ), viewed as an algebraic stack over Spec(ℤ) by Stacks 04X6.

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

AlgebraicGeometry.Stack.IsQuasiDMAbs, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsolute.lean, line 147. The attribute's comment: “part (6): quasi-DM”.

Stacks 050D, part (6). An algebraic stack is quasi-DM when it is quasi-DM over Spec(ℤ), viewed as an algebraic stack over Spec(ℤ) by Stacks 04X6.

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

AlgebraicGeometry.Stack.IsSeparatedAbs, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsolute.lean, line 153. The attribute's comment: “part (7): separated”.

Stacks 050D, part (7). An algebraic stack is separated when it is separated over Spec(ℤ), viewed as an algebraic stack over Spec(ℤ) by Stacks 04X6.

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

AlgebraicGeometry.Stack.IsQuasiSeparatedAbs, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsolute.lean, line 159. The attribute's comment: “part (8): quasi-separated”.

Stacks 050D, part (8). An algebraic stack is quasi-separated when it is quasi-separated over Spec(ℤ), viewed as an algebraic stack over Spec(ℤ) by Stacks 04X6.

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

AlgebraicGeometry.Stack.IsDMOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAxioms.lean, line 177. The attribute's comment: “part (1): DM over the base”.

Stacks 050D, part (1). An algebraic stack over S is DM over S when its structure morphism to the algebraic stack represented by S is DM in the sense of Stacks 04YW.

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

AlgebraicGeometry.Stack.IsQuasiDMOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAxioms.lean, line 184. The attribute's comment: “part (2): quasi-DM over the base”.

Stacks 050D, part (2). An algebraic stack over S is quasi-DM over S when its structure morphism to the algebraic stack represented by S is quasi-DM in the sense of Stacks 04YW.

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

AlgebraicGeometry.Stack.IsSeparatedOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAxioms.lean, line 191. The attribute's comment: “part (3): separated over the base”.

Stacks 050D, part (3). An algebraic stack over S is separated over S when its structure morphism to the algebraic stack represented by S is separated in the sense of Stacks 04YW.

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

AlgebraicGeometry.Stack.IsQuasiSeparatedOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAxioms.lean, line 198. The attribute's comment: “part (4): quasi-separated over the base”.

Stacks 050D, part (4). An algebraic stack over S is quasi-separated over S when its structure morphism to the algebraic stack represented by S is quasi-separated in the sense of Stacks 04YW.

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

Tag 050E, a lemma

Tag 050E in the Stacks Project.

AlgebraicGeometry.Stack.isUnramified_relativeDiagonal_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDiagonalUnramified.lean, line 169. The attribute's comment: “representable_implies_dm”.

Stacks 050E, part (3). A 1-morphism of algebraic stacks which is representable by algebraic spaces is Deligne–Mumford: its relative diagonal is representable by algebraic spaces (Stacks 04XS, part (1)), a monomorphism by part (3) of Stacks 04YQ and locally of finite type by part (2) of that tag, so Stacks 05W6 makes it unramified — which is the Deligne–Mumford condition of Stacks 04YW.

No part key of Stacks 04YQ is claimed: that tag's five parts are representability, local finite type, monomorphy, separatedness and local quasi-finiteness, and unramifiedness is none of them.

theorem isUnramified_relativeDiagonal_of_isRepresentableByAlgebraicSpaces : IsDM B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDMWithRepresentableDiagonal_of_isDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationOverBase.lean, line 131. The attribute's comment: “dm_implies_quasi_dm”.

Stacks 050E. A DM 1-morphism of algebraic stacks over S is quasi-DM.

Both conditions quantify over the same represented base changes of the relative diagonal and differ only in the property tested of the resulting morphism of algebraic spaces, so the implication is Stacks 05W0 — an unramified morphism of algebraic spaces is locally quasi-finite — applied at each of them.

theorem isQuasiDMWithRepresentableDiagonal_of_isDM
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (hf : Stack.IsDM B S hS f) : IsQuasiDMWithRepresentableDiagonal B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparated_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationTrivialImplications.lean, line 102. The attribute's comment: “part (1): separated implies quasi-separated”.

Stacks 050E, part (1). A separated 1-morphism of algebraic stacks over S is quasi-separated: its relative diagonal is proper, hence separated and of finite type, hence quasi-separated and quasi-compact.

theorem isQuasiSeparated_of_isSeparated {f : 𝒳 ⟶ 𝒴} (hf : IsSeparated B S hS f) :
    IsQuasiSeparated B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_of_isDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationTrivialImplications.lean, line 111. The attribute's comment: “part (2): DM implies quasi-DM”.

Stacks 050E, part (2). A Deligne–Mumford 1-morphism of algebraic stacks over S is quasi-DM: its relative diagonal is unramified, hence locally quasi-finite.

theorem isQuasiDM_of_isDM {f : 𝒳 ⟶ 𝒴} (hf : Stack.IsDM B S hS f) :
    IsQuasiDM B S hS f

Tag 050F, a lemma

Tag 050F in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isDM_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationBaseChange.lean, line 214. The attribute's comment: “dm”.

Stacks 050F, DM. The base change q : 𝒳 ×_𝒴 𝒵 ⟶ 𝒵 of a Deligne–Mumford 1-morphism of algebraic stacks over S is Deligne–Mumford: its relative diagonal is representable by algebraic spaces (Stacks 04XS, part (1)) and unramified in the sense of Stacks 04XB, the latter because Δ_q is a base change of Δ_f.

theorem isDM_baseChange (hf : Stack.IsDM B S hS f) :
    Stack.IsDM B S hS (twoFibreProductSquare B S hS f g).snd

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationBaseChange.lean, line 225. The attribute's comment: “quasi_dm”.

Stacks 050F, quasi-DM. The base change q : 𝒳 ×_𝒴 𝒵 ⟶ 𝒵 of a quasi-DM 1-morphism of algebraic stacks over S is quasi-DM: Δ_q is a base change of Δ_f, which is locally quasi-finite in the sense of Stacks 04XB.

theorem isQuasiDM_baseChange (hf : IsQuasiDM B S hS f) :
    IsQuasiDM B S hS (twoFibreProductSquare B S hS f g).snd

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationBaseChange.lean, line 234. The attribute's comment: “separated”.

Stacks 050F, separated. The base change q : 𝒳 ×_𝒴 𝒵 ⟶ 𝒵 of a separated 1-morphism of algebraic stacks over S is separated: Δ_q is a base change of Δ_f, which is proper in the sense of Stacks 04XB.

theorem isSeparated_baseChange (hf : IsSeparated B S hS f) :
    IsSeparated B S hS (twoFibreProductSquare B S hS f g).snd

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparated_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationBaseChange.lean, line 243. The attribute's comment: “quasi_separated”.

Stacks 050F, quasi-separated. The base change q : 𝒳 ×_𝒴 𝒵 ⟶ 𝒵 of a quasi-separated 1-morphism of algebraic stacks over S is quasi-separated: Δ_q is a base change of Δ_f, which is quasi-compact and quasi-separated in the sense of Stacks 04XB.

theorem isQuasiSeparated_baseChange (hf : IsQuasiSeparated B S hS f) :
    IsQuasiSeparated B S hS (twoFibreProductSquare B S hS f g).snd

Tag 06TZ, a lemma

Tag 06TZ in the Stacks Project.

AlgebraicGeometry.Stack.isDM_of_isDM_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationFppfDescent.lean, line 303. The attribute's comment: “dm_descent”.

Stacks 06TZ, the Deligne–Mumford case. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒴' ⟶ 𝒴 be surjective, flat and locally of finite presentation with 𝒴' representable by an algebraic space. If the base change f' : 𝒳 ×_{f, 𝒴, g} 𝒴' ⟶ 𝒴' of f by g is Deligne–Mumford, so is f.

By Stacks 04YR the relative diagonal Δ_{f'} is a base change of Δ_f along r × r, and unramifiedness in the relative sense of Stacks 03YK descends along r × r by Stacks 045D, whose local essential surjectivity hypothesis is AlgebraicGeometry.Stack.localEssSurj_diagonalMapDiag. The representability witness is Stacks 04XS part (1), which holds for every 1-morphism of algebraic stacks and so is not descended.

theorem isDM_of_isDM_baseChange (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (h𝒴' : IsRepresentableByAlgebraicSpace B S hS 𝒴'.val)
    (hgSurj : IsSurjective B S hS g)
    (hgFlat : AlgebraicStacks.IsFlat B S hS g)
    (hgLfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (hf' : IsDM B S hS (twoFibreProductSquareAlgebraicStacks B S hS f g).snd) :
    IsDM B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_of_isQuasiDM_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationFppfDescent.lean, line 332. The attribute's comment: “quasi_dm_descent”.

Stacks 06TZ, the quasi-DM case. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒴' ⟶ 𝒴 be surjective, flat and locally of finite presentation with 𝒴' representable by an algebraic space. If the base change f' : 𝒳 ×_{f, 𝒴, g} 𝒴' ⟶ 𝒴' of f by g is quasi-DM, so is f.

The relative diagonal of the base change is a base change of Δ_f by Stacks 04YR, and local quasi-finiteness of the represented base changes descends by Stacks 045D.

theorem isQuasiDM_of_isQuasiDM_baseChange (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (h𝒴' : IsRepresentableByAlgebraicSpace B S hS 𝒴'.val)
    (hgSurj : IsSurjective B S hS g)
    (hgFlat : AlgebraicStacks.IsFlat B S hS g)
    (hgLfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (hf' : IsQuasiDM B S hS (twoFibreProductSquareAlgebraicStacks B S hS f g).snd) :
    IsQuasiDM B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_isSeparated_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationFppfDescent.lean, line 354. The attribute's comment: “separated_descent”.

Stacks 06TZ, the separated case. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒴' ⟶ 𝒴 be surjective, flat and locally of finite presentation with 𝒴' representable by an algebraic space. If the base change f' : 𝒳 ×_{f, 𝒴, g} 𝒴' ⟶ 𝒴' of f by g is separated, so is f.

The relative diagonal of the base change is a base change of Δ_f by Stacks 04YR, and properness of the represented base changes descends by Stacks 045D, whose target-locality hypothesis is the fppf form of Stacks 0422.

theorem isSeparated_of_isSeparated_baseChange (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (h𝒴' : IsRepresentableByAlgebraicSpace B S hS 𝒴'.val)
    (hgSurj : IsSurjective B S hS g)
    (hgFlat : AlgebraicStacks.IsFlat B S hS g)
    (hgLfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (hf' : IsSeparated B S hS (twoFibreProductSquareAlgebraicStacks B S hS f g).snd) :
    IsSeparated B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparated_of_isQuasiSeparated_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationFppfDescent.lean, line 382. The attribute's comment: “quasi_separated_descent”.

Stacks 06TZ, the quasi-separated case. Let f : 𝒳 ⟶ 𝒴 be a 1-morphism of algebraic stacks over S and let g : 𝒴' ⟶ 𝒴 be surjective, flat and locally of finite presentation with 𝒴' representable by an algebraic space. If the base change f' : 𝒳 ×_{f, 𝒴, g} 𝒴' ⟶ 𝒴' of f by g is quasi-separated, so is f.

The relative diagonal of the base change is a base change of Δ_f by Stacks 04YR, and the conjunction of quasi-compactness and quasi-separatedness of the represented base changes descends by Stacks 045D — applied at the conjunction, read as a property of morphisms of algebraic spaces, exactly as the definition of quasi-separatedness is, with both of that conjunction's hypotheses formed as meets.

theorem isQuasiSeparated_of_isQuasiSeparated_baseChange (f : 𝒳 ⟶ 𝒴) (g : 𝒴' ⟶ 𝒴)
    (h𝒴' : IsRepresentableByAlgebraicSpace B S hS 𝒴'.val)
    (hgSurj : IsSurjective B S hS g)
    (hgFlat : AlgebraicStacks.IsFlat B S hS g)
    (hgLfp : AlgebraicStacks.IsLocallyOfFinitePresentation B S hS g)
    (hf' : IsQuasiSeparated B S hS (twoFibreProductSquareAlgebraicStacks B S hS f g).snd) :
    IsQuasiSeparated B S hS f

Tag 050G, a lemma

Tag 050G in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDMOver_changeOfBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationChangeOfBase.lean, line 141. The attribute's comment: “quasi-DM over the base”.

Stacks 050G, the quasi-DM key. Being quasi-DM over the base is stable under change of base scheme.

theorem isQuasiDMOver_changeOfBase (𝒳' : AlgebraicStacks.{u, w} B S' hS')
    (h𝒳' : Stack.IsQuasiDMOver B S' hS' 𝒳') :
    Stack.IsQuasiDMOver B S hS (Stack.changeOfBase B S S' hS hS' g 𝒳')

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparatedOver_changeOfBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationChangeOfBase.lean, line 164. The attribute's comment: “quasi-separated over the base”.

Stacks 050G, the quasi-separated key. Being quasi-separated over the base is stable under change of base scheme.

theorem isQuasiSeparatedOver_changeOfBase (𝒳' : AlgebraicStacks.{u, w} B S' hS')
    (h𝒳' : Stack.IsQuasiSeparatedOver B S' hS' 𝒳') :
    Stack.IsQuasiSeparatedOver B S hS (Stack.changeOfBase B S S' hS hS' g 𝒳')

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparatedOver_changeOfBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationChangeOfBase.lean, line 191. The attribute's comment: “separated over the base”.

Stacks 050G, the separated key. Being separated over the base is stable under change of base scheme.

theorem isSeparatedOver_changeOfBase (𝒳' : AlgebraicStacks.{u, w} B S' hS')
    (h𝒳' : Stack.IsSeparatedOver B S' hS' 𝒳') :
    Stack.IsSeparatedOver B S hS (Stack.changeOfBase B S S' hS hS' g 𝒳')

Tag 050H, a lemma

Tag 050H in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreProductComparison.lean, line 215. The attribute's comment: “part (1): representable by algebraic spaces”.

The comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_comparison
    (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) (h : 𝒵 ⟶ 𝒯) :
    IsRepresentableByAlgebraicSpaces B S hS (comparison B S hS f g h).hom.hom

AlgebraicGeometry.Stack.isUnramified_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreProductComparison.lean, line 231. The attribute's comment: “dm_unramified”.

If h : 𝒵 ⟶ 𝒯 is Deligne–Mumford then the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is unramified, in the sense of HasRelativeProperty. The statement supplies, as local instances, the stability of unramifiedness of morphisms of algebraic spaces under base change and its locality on the target for the fppf precoverage.

theorem isUnramified_comparison (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) (h : 𝒵 ⟶ 𝒯)
    (hh : IsDM B S hS h) :
    letI : MorphismProperty.IsStableUnderBaseChange
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (k : X ⟶ Y) =>
        Space.IsUnramified B S hS k.hom) :=
      Space.isUnramified_isStableUnderBaseChange B S hS
    letI : MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (k : X ⟶ Y) =>
        Space.IsUnramified B S hS k.hom)
      (Space.Topology.fppf.precoverage.{u, u} B S hS) :=
      (Space.isUnramified_isLocalAtTarget_fpqc B S hS).of_le
        (Space.fppfPrecoverage_le_fpqcPrecoverage.{u, u} B S hS)
    HasRelativeProperty B S hS
      (fun _ _ k => Space.IsUnramified B S hS k.hom)
      (comparison B S hS f g h).hom
      (isRepresentableByAlgebraicSpaces_comparison B S hS f g h)

AlgebraicGeometry.Stack.isLocallyOfFiniteType_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreProductComparisonFiniteType.lean, line 93. The attribute's comment: “part (1): locally of finite type”.

Stacks 050H, part (1), locally-of-finite-type half. The comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is locally of finite type, in the sense of Properties of Stacks, Section 04XB.

By Stacks 04Z1 the comparison is the base change of the relative diagonal Δ_{𝒵/𝒯} along the right-hand leg of AlgebraicGeometry.Stack.comparisonSquare; that diagonal is locally of finite type by part (2) of Stacks 04XS, with no hypothesis on h, and Stacks 045C carries the property across. Together with AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_comparison this is the whole of part (1).

theorem isLocallyOfFiniteType_comparison (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) (h : 𝒵 ⟶ 𝒯) :
    IsLocallyOfFiniteType B S hS (comparison B S hS f g h).hom

AlgebraicGeometry.Stack.isQuasiSeparated_comparison_of_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreProductComparisonSeparation.lean, line 100. The attribute's comment: “quasi_separated_diagonal”.

If the relative diagonal Δ_{𝒵/𝒯} is quasi-separated, then so is the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴, both in the sense of Properties of Stacks, Section 04XB.

theorem isQuasiSeparated_comparison_of_diagonal (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) (h : 𝒵 ⟶ 𝒯)
    (hΔ : IsQuasiSeparated B S hS (relativeDiagonalAlgebraicStacks B S hS h).hom) :
    IsQuasiSeparated B S hS (comparison B S hS f g h).hom

AlgebraicGeometry.Stack.isSeparated_comparison_of_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreProductComparisonSeparation.lean, line 108. The attribute's comment: “separated_diagonal”.

If the relative diagonal Δ_{𝒵/𝒯} is separated, then so is the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴, both in the sense of Properties of Stacks, Section 04XB.

theorem isSeparated_comparison_of_diagonal (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) (h : 𝒵 ⟶ 𝒯)
    (hΔ : IsSeparated B S hS (relativeDiagonalAlgebraicStacks B S hS h).hom) :
    IsSeparated B S hS (comparison B S hS f g h).hom

AlgebraicGeometry.Stack.isLocallyQuasiFinite_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreProductComparisonSeparation.lean, line 116. The attribute's comment: “quasi_dm_lqf”.

If h : 𝒵 ⟶ 𝒯 is quasi-DM then the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is locally quasi-finite, in the sense of Properties of Stacks, Section 04XB.

theorem isLocallyQuasiFinite_comparison (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) (h : 𝒵 ⟶ 𝒯)
    (hh : AlgebraicStacks.IsQuasiDM B S hS h) :
    IsLocallyQuasiFinite B S hS (comparison B S hS f g h).hom

AlgebraicGeometry.Stack.isProper_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreProductComparisonSeparation.lean, line 125. The attribute's comment: “separated_proper”.

If h : 𝒵 ⟶ 𝒯 is separated then the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is proper, in the sense of Properties of Stacks, Section 04XB.

theorem isProper_comparison (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) (h : 𝒵 ⟶ 𝒯)
    (hh : AlgebraicStacks.IsSeparated B S hS h) :
    IsProper B S hS (comparison B S hS f g h).hom

AlgebraicGeometry.Stack.isQuasiCompact_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreProductComparisonSeparation.lean, line 134. The attribute's comment: “part (7), the quasi-compactness half”.

If h : 𝒵 ⟶ 𝒯 is quasi-separated as a 1-morphism of algebraic stacks, then the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is quasi-compact, in the sense of Properties of Stacks, Section 04XB.

theorem isQuasiCompact_comparison (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) (h : 𝒵 ⟶ 𝒯)
    (hh : AlgebraicStacks.IsQuasiSeparated B S hS h) :
    IsQuasiCompact B S hS (comparison B S hS f g h).hom

AlgebraicGeometry.Stack.isQuasiSeparated_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FibreProductComparisonSeparation.lean, line 146. The attribute's comment: “part (7), the quasi-separatedness half”.

If h : 𝒵 ⟶ 𝒯 is quasi-separated as a 1-morphism of algebraic stacks, then the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is quasi-separated, in the sense of Properties of Stacks, Section 04XB.

theorem isQuasiSeparated_comparison (f : 𝒳 ⟶ 𝒵) (g : 𝒴 ⟶ 𝒵) (h : 𝒵 ⟶ 𝒯)
    (hh : AlgebraicStacks.IsQuasiSeparated B S hS h) :
    IsQuasiSeparated B S hS (comparison B S hS f g h).hom

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparated_mapBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationFibreProductProperties.lean, line 178. The attribute's comment: “part (2): quasi-separated”.

Stacks 050H, part (2). If the relative diagonal Δ_{𝒵/𝒯} is quasi-separated in the sense of Stacks 04XB, then so is the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴.

theorem isQuasiSeparated_mapBase
    (hΔ : Stack.IsQuasiSeparated.{u, u, u + 1} B S hS
      (relativeDiagonal.{u, u, u + 1} B S hS 𝒵.val 𝒯.val h.hom)) :
    Stack.IsQuasiSeparated.{u, u, u + 1} B S hS (mapBase B S hS f g h).hom

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_mapBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationFibreProductProperties.lean, line 188. The attribute's comment: “part (3): separated”.

Stacks 050H, part (3). If the relative diagonal Δ_{𝒵/𝒯} is separated in the sense of Stacks 04XB, then so is the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴.

theorem isSeparated_mapBase
    (hΔ : Stack.IsSeparated.{u, u, u + 1} B S hS
      (relativeDiagonal.{u, u, u + 1} B S hS 𝒵.val 𝒯.val h.hom)) :
    Stack.IsSeparated.{u, u, u + 1} B S hS (mapBase B S hS f g h).hom

AlgebraicGeometry.Stack.AlgebraicStacks.isUnramified_mapBase_of_isDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationFibreProductProperties.lean, line 199. The attribute's comment: “part (4): unramified”.

Stacks 050H, part (4). If h : 𝒵 ⟶ 𝒯 is Deligne–Mumford, then the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is unramified in the sense of Stacks 04XB: i is a base change of Δ_{𝒵/𝒯}, which is unramified by the definition of Stacks 04YW.

theorem isUnramified_mapBase_of_isDM (hh : Stack.IsDM B S hS h) :
    ∀ (U : BigFppfOver B S hS)
      (z : BigFppfOver B U.left.1 U.left.2 ⥤
        (twoFibreProduct B S hS (f ≫ h) (g ≫ h)).val.val.obj)
      (_hz : z ⋙ (twoFibreProduct B S hS (f ≫ h) (g ≫ h)).val.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)
            (twoFibreProduct B S hS f g).val.val.p
            (twoFibreProduct B S hS (f ≫ h) (g ≫ h)).val.val.p z
            (CatFiberedInGroupoids.homFunctor (mapBase B S hS f g h).hom))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.IsUnramified B S hS
          (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

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

Stacks 050H, part (5). If h : 𝒵 ⟶ 𝒯 is quasi-DM, then the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is locally quasi-finite in the sense of Stacks 04XB.

theorem isLocallyQuasiFinite_mapBase_of_isQuasiDM (hh : IsQuasiDM B S hS h) :
    Stack.IsLocallyQuasiFinite.{u, u, u + 1} B S hS (mapBase B S hS f g h).hom

AlgebraicGeometry.Stack.AlgebraicStacks.isProper_mapBase_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationFibreProductProperties.lean, line 229. The attribute's comment: “part (6): proper”.

Stacks 050H, part (6). If h : 𝒵 ⟶ 𝒯 is separated, then the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is proper in the sense of Stacks 04XB.

theorem isProper_mapBase_of_isSeparated (hh : IsSeparated B S hS h) :
    Stack.IsProper.{u, u, u + 1} B S hS (mapBase B S hS f g h).hom

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiCompactAndQuasiSeparated_mapBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationFibreProductProperties.lean, line 237. The attribute's comment: “part (7): quasi-compact and quasi-separated”.

Stacks 050H, part (7). If h : 𝒵 ⟶ 𝒯 is quasi-separated, then the comparison 1-morphism i : 𝒳 ×_𝒵 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is quasi-compact and quasi-separated in the sense of Stacks 04XB.

theorem isQuasiCompactAndQuasiSeparated_mapBase
    (hh : IsQuasiSeparated B S hS h) :
    Stack.IsQuasiCompact.{u, u, u + 1} B S hS (mapBase B S hS f g h).hom ∧
      Stack.IsQuasiSeparated.{u, u, u + 1} B S hS (mapBase B S hS f g h).hom

Tag 050I, a lemma

Tag 050I in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_graph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GraphMorphism.lean, line 563. The attribute's comment: “part (1): representable by algebraic spaces”.

Stacks 050I, part (1), representability half. The graph of a 1-morphism of algebraic stacks over a base algebraic stack is representable by algebraic spaces.

The graph is 2-isomorphic to the comparison 1-morphism of Stacks 050H precomposed and postcomposed with equivalences, and representability by algebraic spaces is invariant under such a square by Stacks 0457.

theorem isRepresentableByAlgebraicSpaces_graph (g : 𝒳 ⟶ 𝒴) (p : 𝒳 ⟶ 𝒯) (q : 𝒴 ⟶ 𝒯)
    (η : p ≅ g ≫ q) :
    IsRepresentableByAlgebraicSpaces B S hS (graph B S hS g p q η).hom.hom

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

Stacks 050I, part (2). If q : 𝒴 ⟶ 𝒯 is Deligne–Mumford then the graph of g : 𝒳 ⟶ 𝒴 over 𝒯 is unramified, in the relative sense of Stacks 03YK.

By Stacks 050H part (4) the comparison 1-morphism 𝒳 ×_𝒴 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is unramified, and AlgebraicGeometry.Stack.hasRelativeProperty_graph_of_comparison carries that to the graph. The two instance arguments of Stacks 03YK are Stacks 03ZJ and Stacks 042A composed with the comparison of the fppf and fpqc precoverages.

theorem isUnramified_graph (g : 𝒳 ⟶ 𝒴) (p : 𝒳 ⟶ 𝒯) (q : 𝒴 ⟶ 𝒯) (η : p ≅ g ≫ q)
    (hq : IsDM B S hS q) :
    letI : MorphismProperty.IsStableUnderBaseChange
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (k : X ⟶ Y) =>
        Space.IsUnramified B S hS k.hom) :=
      Space.isUnramified_isStableUnderBaseChange B S hS
    letI : MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (k : X ⟶ Y) =>
        Space.IsUnramified B S hS k.hom)
      (Space.Topology.fppf.precoverage.{u, u} B S hS) :=
      (Space.isUnramified_isLocalAtTarget_fpqc B S hS).of_le
        (Space.fppfPrecoverage_le_fpqcPrecoverage.{u, u} B S hS)
    HasRelativeProperty B S hS
      (fun _ _ k => Space.IsUnramified B S hS k.hom)
      (graph B S hS g p q η).hom
      (isRepresentableByAlgebraicSpaces_graph B S hS g p q η)

AlgebraicGeometry.Stack.isLocallyOfFiniteType_graph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GraphMorphism.lean, line 712. The attribute's comment: “part (1): locally of finite type”.

Stacks 050I, part (1), locally-of-finite-type half. The graph of a 1-morphism of algebraic stacks over a base algebraic stack is locally of finite type, in the sense of Properties of Stacks, Section 04XB.

By the locally-of-finite-type half of Stacks 050H part (1) the comparison 1-morphism 𝒳 ×_𝒴 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is locally of finite type, and AlgebraicGeometry.Stack.relativeProperty_graph_of_comparison carries that to the graph. No hypothesis on q is needed, exactly as in Stacks 050H. Together with AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_graph this is the whole of part (1).

theorem isLocallyOfFiniteType_graph (g : 𝒳 ⟶ 𝒴) (p : 𝒳 ⟶ 𝒯) (q : 𝒴 ⟶ 𝒯) (η : p ≅ g ≫ q) :
    IsLocallyOfFiniteType B S hS (graph B S hS g p q η).hom

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

Stacks 050I, part (3). If q : 𝒴 ⟶ 𝒯 is quasi-DM then the graph of g : 𝒳 ⟶ 𝒴 over 𝒯 is locally quasi-finite, in the sense of Properties of Stacks, Section 04XB.

By Stacks 050H part (5) the comparison 1-morphism 𝒳 ×_𝒴 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is locally quasi-finite, and AlgebraicGeometry.Stack.relativeProperty_graph_of_comparison carries that to the graph. One statement suffices: Stacks 050H takes the quasi-DM condition of Stacks 04YW apart, so the input is local quasi-finiteness alone.

theorem isLocallyQuasiFinite_graph (g : 𝒳 ⟶ 𝒴) (p : 𝒳 ⟶ 𝒯) (q : 𝒴 ⟶ 𝒯) (η : p ≅ g ≫ q)
    (hq : AlgebraicStacks.IsQuasiDM B S hS q) :
    IsLocallyQuasiFinite B S hS (graph B S hS g p q η).hom

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

Stacks 050I, part (4). If q : 𝒴 ⟶ 𝒯 is separated then the graph of g : 𝒳 ⟶ 𝒴 over 𝒯 is proper, in the sense of Properties of Stacks, Section 04XB.

By Stacks 050H part (6) the comparison 1-morphism 𝒳 ×_𝒴 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is proper, and AlgebraicGeometry.Stack.relativeProperty_graph_of_comparison carries that to the graph. The separatedness condition of Stacks 04YW is a single property of the relative diagonal, so there is no conjunction to project here.

theorem isProper_graph (g : 𝒳 ⟶ 𝒴) (p : 𝒳 ⟶ 𝒯) (q : 𝒴 ⟶ 𝒯) (η : p ≅ g ≫ q)
    (hq : AlgebraicStacks.IsSeparated B S hS q) :
    IsProper B S hS (graph B S hS g p q η).hom

AlgebraicGeometry.Stack.isQuasiCompact_graph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GraphMorphism.lean, line 759. The attribute's comment: “part (5): quasi-compact”.

Stacks 050I, part (5), the quasi-compactness half. If q : 𝒴 ⟶ 𝒯 is quasi-separated then the graph of g : 𝒳 ⟶ 𝒴 over 𝒯 is quasi-compact, in the sense of Properties of Stacks, Section 04XB.

By Stacks 050H part (7) the comparison 1-morphism 𝒳 ×_𝒴 𝒴 ⟶ 𝒳 ×_𝒯 𝒴 is quasi-compact, and AlgebraicGeometry.Stack.relativeProperty_graph_of_comparison carries that to the graph. A single statement suffices here, because Stacks 050H already projects the conjunction of Stacks 04YW quasi-separatedness: the input is quasi-compactness alone. The property is the longhand lambda rather than AlgebraicGeometry.Space.quasiCompactProperty, so neither Stacks 03HF nor Stacks 041L is needed even though both are available.

theorem isQuasiCompact_graph (g : 𝒳 ⟶ 𝒴) (p : 𝒳 ⟶ 𝒯) (q : 𝒴 ⟶ 𝒯) (η : p ≅ g ≫ q)
    (hq : AlgebraicStacks.IsQuasiSeparated B S hS q) :
    IsQuasiCompact B S hS (graph B S hS g p q η).hom

AlgebraicGeometry.Stack.isQuasiSeparated_graph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/GraphMorphism.lean, line 774. The attribute's comment: “part (5): quasi-separated”.

Stacks 050I, part (5), the quasi-separatedness half. If q : 𝒴 ⟶ 𝒯 is quasi-separated then the graph of g : 𝒳 ⟶ 𝒴 over 𝒯 is quasi-separated, in the sense of Properties of Stacks, Section 04XB.

As for the quasi-compactness half, over the second conjunct: Stacks 050H part (7) is stated twice, once for each conjunct of the quasi-separatedness condition of Stacks 04YW, so the input here is quasi-separatedness of the comparison 1-morphism alone.

theorem isQuasiSeparated_graph (g : 𝒳 ⟶ 𝒴) (p : 𝒳 ⟶ 𝒯) (q : 𝒴 ⟶ 𝒯) (η : p ≅ g ≫ q)
    (hq : AlgebraicStacks.IsQuasiSeparated B S hS q) :
    IsQuasiSeparated B S hS (graph B S hS g p q η).hom

Tag 050J, a lemma

Tag 050J in the Stacks Project.

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SectionMorphism.lean, line 230. The attribute's comment: “part (1): representable by algebraic spaces”.

Stacks 050J, part (1), representability half. A section of a 1-morphism of algebraic stacks is representable by algebraic spaces.

The graph of s over 𝒯, taken for the cospan (𝟙 𝒯, f), is representable by algebraic spaces by Stacks 050I, and s is 2-isomorphic to its composite with the second projection, which is an equivalence by AlgebraicGeometry.Stack.sectionSecondProjection_isEquivalence. Stacks 0457 carries representability across that square.

theorem isRepresentableByAlgebraicSpaces_section (f : 𝒳 ⟶ 𝒯) (s : 𝒯 ⟶ 𝒳)
    (hs : Nonempty (s ≫ f ≅ 𝟙 𝒯)) :
    IsRepresentableByAlgebraicSpaces B S hS s.hom.hom

AlgebraicGeometry.Stack.isLocallyOfFiniteType_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SectionMorphism.lean, line 359. The attribute's comment: “part (1): locally of finite type”.

Stacks 050J, part (1), locally-of-finite-type half. A section of a 1-morphism of algebraic stacks is locally of finite type, in the sense of Properties of Stacks, Section 04XB.

By the locally-of-finite-type half of Stacks 050I part (1) the graph Γ_s : 𝒯 ⟶ 𝒯 ×_{𝟙 𝒯, 𝒯, f} 𝒳 is locally of finite type, and AlgebraicGeometry.Stack.relativeProperty_section_of_graph carries that to s. No hypothesis on f is needed, exactly as in Stacks 050I and Stacks 050H. Together with AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_section this is the whole of part (1).

theorem isLocallyOfFiniteType_section (f : 𝒳 ⟶ 𝒯) (s : 𝒯 ⟶ 𝒳)
    (hs : Nonempty (s ≫ f ≅ 𝟙 𝒯)) :
    IsLocallyOfFiniteType B S hS s.hom

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

Stacks 050J, part (2). If f : 𝒳 ⟶ 𝒯 is Deligne–Mumford then a section of f is unramified, in the relative sense of Stacks 03YK.

By Stacks 050I part (2) the graph Γ_s : 𝒯 ⟶ 𝒯 ×_{𝟙 𝒯, 𝒯, f} 𝒳 is unramified, and AlgebraicGeometry.Stack.hasRelativeProperty_section_of_graph carries that to s. The two instance arguments of Stacks 03YK are Stacks 03ZJ and Stacks 042A composed with the comparison of the fppf and fpqc precoverages.

theorem isUnramified_section (f : 𝒳 ⟶ 𝒯) (s : 𝒯 ⟶ 𝒳) (hs : Nonempty (s ≫ f ≅ 𝟙 𝒯))
    (hf : IsDM B S hS f) :
    letI : MorphismProperty.IsStableUnderBaseChange
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (k : X ⟶ Y) =>
        Space.IsUnramified B S hS k.hom) :=
      Space.isUnramified_isStableUnderBaseChange B S hS
    letI : MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (k : X ⟶ Y) =>
        Space.IsUnramified B S hS k.hom)
      (Space.Topology.fppf.precoverage.{u, u} B S hS) :=
      (Space.isUnramified_isLocalAtTarget_fpqc B S hS).of_le
        (Space.fppfPrecoverage_le_fpqcPrecoverage.{u, u} B S hS)
    HasRelativeProperty B S hS
      (fun _ _ k => Space.IsUnramified B S hS k.hom)
      s.hom (isRepresentableByAlgebraicSpaces_section B S hS f s hs)

AlgebraicGeometry.Stack.isLocallyQuasiFinite_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SectionMorphism.lean, line 406. The attribute's comment: “part (3): locally quasi-finite”.

Stacks 050J, part (3). If f : 𝒳 ⟶ 𝒯 is quasi-DM then a section of f is locally quasi-finite, in the sense of Properties of Stacks, Section 04XB.

By Stacks 050I part (3) the graph Γ_s : 𝒯 ⟶ 𝒯 ×_{𝟙 𝒯, 𝒯, f} 𝒳 is locally quasi-finite, and AlgebraicGeometry.Stack.relativeProperty_section_of_graph carries that to s. One statement suffices: Stacks 050I already takes the quasi-DM condition of Stacks 04YW apart, so the input is local quasi-finiteness alone. The property is the longhand lambda rather than the packaged local quasi-finiteness of Stacks 06MF, so no instance of Stacks 03YK is needed.

theorem isLocallyQuasiFinite_section (f : 𝒳 ⟶ 𝒯) (s : 𝒯 ⟶ 𝒳) (hs : Nonempty (s ≫ f ≅ 𝟙 𝒯))
    (hf : AlgebraicStacks.IsQuasiDM B S hS f) :
    IsLocallyQuasiFinite B S hS s.hom

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

Stacks 050J, part (4). If f : 𝒳 ⟶ 𝒯 is separated then a section of f is proper in the sense of Properties of Stacks, Section 04XB.

By Stacks 050I part (4) the graph Γ_s : 𝒯 ⟶ 𝒯 ×_{𝟙 𝒯, 𝒯, f} 𝒳 is proper, and AlgebraicGeometry.Stack.relativeProperty_section_of_graph carries that to s. The separatedness condition of Stacks 04YW is a single property of the relative diagonal, so there is no conjunction to project here. The property is the longhand lambda rather than AlgebraicGeometry.Space.properProperty, so the fppf CategoryTheory.MorphismProperty.IsLocalAtTarget instance of Stacks 0422 is not needed — which matters here, because this library does not have it.

Properness is read in the sense of Section 04XB, as it is in Stacks 050I part (4) (AlgebraicGeometry.Stack.isProper_graph) and in Stacks 050H part (6) (AlgebraicGeometry.Stack.isProper_comparison). That is the reading the source's own proof forces: Stacks 050J is a special case of Stacks 050I, so its conclusions are the conclusions of Stacks 050I, and s carries the Section 04XB notions because part (1) makes it representable by algebraic spaces. Reading part (4) at Stacks 0CL5 instead would assert properness of s as a 1-morphism of algebraic stacks, which is a different statement from the one Stacks 050I supplies.

theorem isRelativelyProper_section (f : 𝒳 ⟶ 𝒯) (s : 𝒯 ⟶ 𝒳) (hs : Nonempty (s ≫ f ≅ 𝟙 𝒯))
    (hf : AlgebraicStacks.IsSeparated B S hS f) :
    IsProper B S hS s.hom

AlgebraicGeometry.Stack.isQuasiCompact_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SectionMorphism.lean, line 472. The attribute's comment: “part (5): quasi-compact”.

Stacks 050J, part (5), quasi-compactness half. If f : 𝒳 ⟶ 𝒯 is quasi-separated then a section of f is quasi-compact in the sense of Stacks 050U: every base change of it by a quasi-compact algebraic stack is again a quasi-compact algebraic stack.

The section is representable by algebraic spaces by part (1), and quasi-compact in the relative sense of Properties of Stacks, Section 04XB by AlgebraicGeometry.Stack.isRelativelyQuasiCompact_section. Stacks 050T identifies the two notions for a 1-morphism representable by algebraic spaces, and that is the whole step.

theorem isQuasiCompact_section (f : 𝒳 ⟶ 𝒯) (s : 𝒯 ⟶ 𝒳) (hs : Nonempty (s ≫ f ≅ 𝟙 𝒯))
    (hf : AlgebraicStacks.IsQuasiSeparated B S hS f) :
    IsQuasiCompactMorphism B S hS s

AlgebraicGeometry.Stack.isQuasiSeparated_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SectionMorphism.lean, line 490. The attribute's comment: “part (5): quasi-separated”.

Stacks 050J, part (5), quasi-separatedness half. If f : 𝒳 ⟶ 𝒯 is quasi-separated then a section of f is quasi-separated, in the sense of Properties of Stacks, Section 04XB.

By Stacks 050I part (5) the graph Γ_s : 𝒯 ⟶ 𝒯 ×_{𝟙 𝒯, 𝒯, f} 𝒳 is quasi-separated, and AlgebraicGeometry.Stack.relativeProperty_section_of_graph carries that to s. A single statement suffices, because Stacks 050I already projects the conjunction of Stacks 04YW quasi-separatedness: the input is quasi-separatedness alone. The quasi-compactness half of part (5) is AlgebraicGeometry.Stack.isQuasiCompact_section, which reads the Section 04XB assertion AlgebraicGeometry.Stack.isRelativelyQuasiCompact_section across Stacks 050T into the notion of Stacks 050U.

theorem isQuasiSeparated_section (f : 𝒳 ⟶ 𝒯) (s : 𝒯 ⟶ 𝒳) (hs : Nonempty (s ≫ f ≅ 𝟙 𝒯))
    (hf : AlgebraicStacks.IsQuasiSeparated B S hS f) :
    IsQuasiSeparated B S hS s.hom

Tag 050K, a lemma

Tag 050K in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isDM_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationComposition.lean, line 149. The attribute's comment: “dm”.

Stacks 050K, DM. The composite of two Deligne–Mumford 1-morphisms of algebraic stacks over S is Deligne–Mumford: its relative diagonal is Δ_f followed by the comparison 1-morphism i, Δ_f is unramified in the sense of Stacks 04XB because f is DM, i is unramified because g is DM (Stacks 050H, part (4)), and a condition of Stacks 04XB at a property stable under composition which descends along a surjective étale scheme chart of the target is stable under composition (Stacks 045B).

theorem isDM_comp (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hf : Stack.IsDM B S hS f)
    (hg : Stack.IsDM B S hS g) : Stack.IsDM B S hS (f ≫ g)

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationComposition.lean, line 247. The attribute's comment: “quasi-DM”.

Stacks 050K, quasi-DM. The composite of two quasi-DM 1-morphisms of algebraic stacks over S is quasi-DM: Δ_{f ≫ g} is Δ_f followed by the comparison 1-morphism i, Δ_f is locally quasi-finite in the sense of Stacks 04XB because f is quasi-DM, i is locally quasi-finite because g is quasi-DM (Stacks 050H, part (5)), and local quasi-finiteness of morphisms of algebraic spaces over S composes (Stacks 03XK) and is fpqc local on the base (Stacks 0427).

theorem isQuasiDM_comp (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hf : IsQuasiDM B S hS f)
    (hg : IsQuasiDM B S hS g) : IsQuasiDM B S hS (f ≫ g)

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationComposition.lean, line 264. The attribute's comment: “separated”.

Stacks 050K, separated. The composite of two separated 1-morphisms of algebraic stacks over S is separated: Δ_{f ≫ g} is Δ_f followed by the comparison 1-morphism i, Δ_f is proper in the sense of Stacks 04XB because f is separated, i is proper because g is separated (Stacks 050H, part (6)), and properness of morphisms of algebraic spaces over S composes (Stacks 04XY) and descends along a surjective étale scheme chart of the target (AlgebraicGeometry.Space.properMorphismProperty_of_pullbackSnd_atlas).

theorem isSeparated_comp (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hf : IsSeparated B S hS f)
    (hg : IsSeparated B S hS g) : IsSeparated B S hS (f ≫ g)

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparated_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationComposition.lean, line 280. The attribute's comment: “quasi-separated”.

Stacks 050K, quasi-separated. The composite of two quasi-separated 1-morphisms of algebraic stacks over S is quasi-separated. Quasi-separatedness of Stacks 04YW is the conjunction of two conditions of Stacks 04XB on Δ_f — quasi-compactness and quasi-separatedness — and each half is the same composition argument at its own property: Δ_{f ≫ g} = Δ_f ≫ i, the half for Δ_f is the axiom for f, the half for i comes from the axiom for g by Stacks 050H, part (7), and quasi-compactness and quasi-separatedness of morphisms of algebraic spaces over S compose (Stacks 03HG, Stacks 03KQ) and are fpqc local on the base (Stacks 041L, Stacks 041N).

theorem isQuasiSeparated_comp (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hf : IsQuasiSeparated B S hS f)
    (hg : IsQuasiSeparated B S hS g) : IsQuasiSeparated B S hS (f ≫ g)

Tag 050L, a lemma

Tag 050L in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyQuasiSeparated_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsoluteQuasiSeparated.lean, line 73. The attribute's comment: “quasi_separated_absolute”.

Stacks 050L, part (8). If f : 𝒳 ⟶ 𝒴 is quasi-separated and 𝒴 is quasi-separated, then 𝒳 is quasi-separated.

Both absolute properties are quasi-separatedness over the terminal scheme of the views AlgebraicGeometry.Stack.AlgebraicStacks.viewOverIntegers of 𝒳 and 𝒴 there, and that view is AlgebraicGeometry.Stack.changeBaseAlgebraicStack along terminal.from S on the nose. So this is part (4) at the terminal scheme, applied to the 1-morphism of views that the hom-bijection of Stacks 04X5 assigns to f, which is quasi-separated by AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparated_changeBase.

theorem isAbsolutelyQuasiSeparated_of_isQuasiSeparated (f : 𝒳 ⟶ 𝒴)
    (hY : IsAbsolutelyQuasiSeparated B S hS hZ 𝒴) (hf : IsQuasiSeparated B S hS f) :
    IsAbsolutelyQuasiSeparated B S hS hZ 𝒳

AlgebraicGeometry.Stack.isSeparatedOver_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsoluteSource.lean, line 341. The attribute's comment: “part (3): separated over the base”.

Stacks 050L, part (3). If 𝒴 is separated over S and the 1-morphism f : 𝒳 ⟶ 𝒴 is separated, then 𝒳 is separated over S.

Being separated over S is being separated as a structure morphism (Stacks 050D, part (3)), the structure morphism of 𝒳 is f followed by that of 𝒴 (AlgebraicGeometry.Stack.comp_structureMorphism), and separated 1-morphisms compose (Stacks 050K).

theorem isSeparatedOver_of_isSeparated (f : 𝒳 ⟶ 𝒴) (h𝒴 : IsSeparatedOver B S hS 𝒴)
    (hf : AlgebraicStacks.IsSeparated B S hS f) : IsSeparatedOver B S hS 𝒳

AlgebraicGeometry.Stack.isDMAbs_of_isDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsoluteSource.lean, line 372. The attribute's comment: “part (5): DM”.

Stacks 050L, part (5). If 𝒴 is DM and the 1-morphism f : 𝒳 ⟶ 𝒴 is DM, then 𝒳 is DM — the two conditions on objects in the absolute sense of Stacks 050D, part (5).

Being DM is being DM over Spec(ℤ) after viewing (Stacks 050D, part (5)); the structure morphism over Spec(ℤ) of 𝒳 viewed is f viewed followed by that of 𝒴 viewed (AlgebraicGeometry.Stack.comp_structureMorphism at the terminal base); the DM axiom for f survives the viewing (AlgebraicGeometry.Stack.isDM_changeBaseHomAlgebraicStacks); and DM 1-morphisms compose (Stacks 050K). So this is part (1) of Stacks 050L read at the base Spec(ℤ).

theorem isDMAbs_of_isDM (f : 𝒳 ⟶ 𝒴) (h𝒴 : IsDMAbs.{u, w, w'} B S hS 𝒴)
    (hf : IsDM B S hS f) : IsDMAbs.{u, w, w'} B S hS 𝒳

AlgebraicGeometry.Stack.isQuasiDMAbs_of_isQuasiDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsoluteSource.lean, line 389. The attribute's comment: “part (6): quasi-DM”.

Stacks 050L, part (6). If 𝒴 is quasi-DM and the 1-morphism f : 𝒳 ⟶ 𝒴 is quasi-DM, then 𝒳 is quasi-DM — the two conditions on objects in the absolute sense of Stacks 050D, part (6).

This is part (2) of Stacks 050L read at the base Spec(ℤ), with AlgebraicGeometry.Stack.isQuasiDM_changeBaseHomAlgebraicStacks supplying the axiom for the viewed 1-morphism.

theorem isQuasiDMAbs_of_isQuasiDM (f : 𝒳 ⟶ 𝒴) (h𝒴 : IsQuasiDMAbs.{u, w, w'} B S hS 𝒴)
    (hf : AlgebraicStacks.IsQuasiDM B S hS f) : IsQuasiDMAbs.{u, w, w'} B S hS 𝒳

AlgebraicGeometry.Stack.isSeparatedAbs_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsoluteSource.lean, line 409. The attribute's comment: “part (7): separated, f's axiom read over Spec(Z) not over S”.

Stacks 050L, part (7). If 𝒴 is separated and the 1-morphism f : 𝒳 ⟶ 𝒴 is separated, then 𝒳 is separated — the two conditions on objects in the absolute sense of Stacks 050D, part (7).

This is part (3) of Stacks 050L read at the base Spec(ℤ). The hypothesis on f is the Stacks 04YW separatedness axiom for f viewed over Spec(ℤ), which is the base the absolute statement lives at; it is not the axiom over S. Unlike the DM axiom of part (5), the separatedness axiom is not known in this library to survive the viewing: it is the Stacks 04XB condition at properness, which is not an every-étale-chart condition. See the implementation notes of this file.

theorem isSeparatedAbs_of_isSeparated (f : 𝒳 ⟶ 𝒴) (h𝒴 : IsSeparatedAbs.{u, w, w'} B S hS 𝒴)
    (hf : AlgebraicStacks.IsSeparated B _ (contains_specULiftZ B)
      (viewOverIntHom.{u, w, w'} B S hS f)) :
    IsSeparatedAbs.{u, w, w'} B S hS 𝒳

AlgebraicGeometry.Stack.isQuasiSeparatedAbs_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsoluteSource.lean, line 427. The attribute's comment: “part (8): quasi-separated, f's axiom read over Spec(Z) not over S”.

Stacks 050L, part (8). If 𝒴 is quasi-separated and the 1-morphism f : 𝒳 ⟶ 𝒴 is quasi-separated, then 𝒳 is quasi-separated — the two conditions on objects in the absolute sense of Stacks 050D, part (8), and so each the conjunction of quasi-compactness and quasi-separatedness of a relative diagonal. Both conjuncts of the conclusion are proved, through AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparated_comp.

This is part (4) of Stacks 050L read at the base Spec(ℤ). As in part (7) the hypothesis on f is the Stacks 04YW axiom for f viewed over Spec(ℤ): quasi-separatedness is the Stacks 04XB condition at quasi-compactness together with quasi-separatedness of morphisms of algebraic spaces, neither of which is an every-étale-chart condition.

theorem isQuasiSeparatedAbs_of_isQuasiSeparated (f : 𝒳 ⟶ 𝒴)
    (h𝒴 : IsQuasiSeparatedAbs.{u, w, w'} B S hS 𝒴)
    (hf : AlgebraicStacks.IsQuasiSeparated B _ (contains_specULiftZ B)
      (viewOverIntHom.{u, w, w'} B S hS f)) :
    IsQuasiSeparatedAbs.{u, w, w'} B S hS 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.isDMOver_of_isDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationOverBaseSource.lean, line 94. The attribute's comment: “dm_over_s”.

Stacks 050L, part (1). If f : 𝒳 ⟶ 𝒴 is Deligne–Mumford and 𝒴 is Deligne–Mumford over the base scheme S, then 𝒳 is Deligne–Mumford over S.

The structure morphism of 𝒳 is f followed by the structure morphism of 𝒴 (AlgebraicGeometry.Stack.comp_structureMorphism), so this is the Deligne–Mumford case of Stacks 050K.

theorem isDMOver_of_isDM (f : 𝒳 ⟶ 𝒴) (hY : Stack.IsDMOver B S hS 𝒴) (hf : Stack.IsDM B S hS f) :
    Stack.IsDMOver B S hS 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDMOver_of_isQuasiDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationOverBaseSource.lean, line 107. The attribute's comment: “quasi_dm_over_s”.

Stacks 050L, part (2). If f : 𝒳 ⟶ 𝒴 is quasi-DM and 𝒴 is quasi-DM over the base scheme S, then 𝒳 is quasi-DM over S.

The structure morphism of 𝒳 is f followed by the structure morphism of 𝒴 (AlgebraicGeometry.Stack.comp_structureMorphism), so this is the quasi-DM case of Stacks 050K.

theorem isQuasiDMOver_of_isQuasiDM (f : 𝒳 ⟶ 𝒴) (hY : Stack.IsQuasiDMOver B S hS 𝒴)
    (hf : IsQuasiDM B S hS f) :
    Stack.IsQuasiDMOver B S hS 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparatedOver_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationOverBaseSource.lean, line 121. The attribute's comment: “quasi_separated_over_s”.

Stacks 050L, part (4). If f : 𝒳 ⟶ 𝒴 is quasi-separated and 𝒴 is quasi-separated over the base scheme S, then 𝒳 is quasi-separated over S.

The structure morphism of 𝒳 is f followed by the structure morphism of 𝒴 (AlgebraicGeometry.Stack.comp_structureMorphism), so this is the quasi-separated case of Stacks 050K.

theorem isQuasiSeparatedOver_of_isQuasiSeparated (f : 𝒳 ⟶ 𝒴)
    (hY : Stack.IsQuasiSeparatedOver B S hS 𝒴) (hf : IsQuasiSeparated B S hS f) :
    Stack.IsQuasiSeparatedOver B S hS 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_of_isDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationOverBaseSource.lean, line 150. The attribute's comment: “dm_absolute”.

Stacks 050L, part (5). If f : 𝒳 ⟶ 𝒴 is Deligne–Mumford and 𝒴 is Deligne–Mumford, then 𝒳 is Deligne–Mumford.

Both absolute properties are the corresponding properties over the terminal scheme of the views AlgebraicGeometry.Stack.AlgebraicStacks.viewOverIntegers of 𝒳 and 𝒴 there, and that view is AlgebraicGeometry.Stack.changeBaseAlgebraicStack along terminal.from S on the nose. So this is part (1) at the terminal scheme, applied to the 1-morphism of views that the hom-bijection of Stacks 04X5 assigns to f, which is Deligne–Mumford by AlgebraicGeometry.Stack.isDM_changeBase_iff.

theorem isAbsolutelyDM_of_isDM (f : 𝒳 ⟶ 𝒴) (hY : IsAbsolutelyDM B S hS hZ 𝒴)
    (hf : Stack.IsDM B S hS f) :
    IsAbsolutelyDM B S hS hZ 𝒳

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

Stacks 050L, part (6). If f : 𝒳 ⟶ 𝒴 is quasi-DM and 𝒴 is quasi-DM, then 𝒳 is quasi-DM.

Part (2) at the terminal scheme, applied to the 1-morphism of views that the hom-bijection of Stacks 04X5 assigns to f, which is quasi-DM by AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_changeBase_iff. That comparison is stated at AlgebraicGeometry.Stack.AlgebraicStacks.IsQuasiDMWithRepresentableDiagonal, the reading which carries the representability witness of the relative diagonal, so the hypothesis and the conclusion are passed across AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDMWithRepresentableDiagonal_iff_isQuasiDM.

theorem isAbsolutelyQuasiDM_of_isQuasiDM (f : 𝒳 ⟶ 𝒴) (hY : IsAbsolutelyQuasiDM B S hS hZ 𝒴)
    (hf : IsQuasiDM B S hS f) :
    IsAbsolutelyQuasiDM B S hS hZ 𝒳

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

Stacks 050L, part (7). If f : 𝒳 ⟶ 𝒴 is separated and 𝒴 is separated, then 𝒳 is separated.

Both absolute properties are separatedness over the terminal scheme of the views AlgebraicGeometry.Stack.AlgebraicStacks.viewOverIntegers of 𝒳 and 𝒴 there, and that view is AlgebraicGeometry.Stack.changeBaseAlgebraicStack along terminal.from S on the nose. So this is part (3) at the terminal scheme, applied to the 1-morphism of views that the hom-bijection of Stacks 04X5 assigns to f, which is separated by AlgebraicGeometry.Stack.isProper_relativeDiagonal_changeBase.

theorem isAbsolutelySeparated_of_isSeparated (f : 𝒳 ⟶ 𝒴)
    (hY : IsAbsolutelySeparated B S hS hZ 𝒴) (hf : IsSeparated B S hS f) :
    IsAbsolutelySeparated B S hS hZ 𝒳

Tag 050M, a lemma

Tag 050M in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparated_of_isQuasiSeparated_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiSeparatedCancellation.lean, line 129. The attribute's comment: “quasi_separated_first”.

Stacks 050M, part (4). If a composite f ≫ g of 1-morphisms of algebraic stacks over S is quasi-separated and the relative diagonal of g is quasi-separated, then f is quasi-separated.

The comparison 1-morphism i : 𝒴 ×_𝒴 𝒳 ⟶ 𝒴 ×_𝒵 𝒳 of Stacks 050H, taken at the identity of 𝒴, composes with the second projection of 𝒴 ×_𝒵 𝒳 to give the second projection of 𝒴 ×_𝒴 𝒳 on the nose. The projection out of 𝒴 ×_𝒵 𝒳 is the base change of f ≫ g along 𝟙 𝒴 ≫ g and is quasi-separated by Stacks 050F; i is quasi-separated by Stacks 050H part (2) from the hypothesis on Δ_g, upgraded from the Section 04XB predicate to the Definition 04YW condition by the two forms of Stacks 04YT condition (1); and Stacks 050K composes them. The projection out of 𝒴 ×_𝒴 𝒳 is the base change of f along an identity, which is f itself by CategoryTheory.Bicategory.isTwoFibreProduct_trivialBaseChangeSquare.

theorem isQuasiSeparated_of_isQuasiSeparated_comp
    {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsQuasiSeparated B S hS (f ≫ g))
    (hΔg : Stack.IsQuasiSeparated B S hS
      (Stack.relativeDiagonalAlgebraicStacks B S hS g).hom) :
    IsQuasiSeparated B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationCancellation.lean, line 137. The attribute's comment: “quasi_dm_first”.

Stacks 050M, part (2). If a composite f ≫ g of 1-morphisms of algebraic stacks over S is quasi-DM, then f is quasi-DM.

f is 2-isomorphic to the graph of f over 𝒵 followed by the second projection of the canonical 2-fibre product of the cospan (f ≫ g, g) (AlgebraicGeometry.Stack.graph_snd_iso). That projection is the base change of f ≫ g along g, so it is quasi-DM by Stacks 050F; the graph is representable by algebraic spaces by Stacks 050I part (1), and the relative diagonal of such a 1-morphism is locally quasi-finite by Stacks 04YQ part (5), which is the quasi-DM condition on the nose. Stacks 050K composes them.

theorem isQuasiDM_of_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hfg : IsQuasiDM B S hS (f ≫ g)) :
    IsQuasiDM B S hS f

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

Stacks 050M, part (1). If a composite f ≫ g of 1-morphisms of algebraic stacks over S is Deligne–Mumford, then f is Deligne–Mumford.

f is 2-isomorphic to the graph of f over 𝒵 followed by the second projection of the canonical 2-fibre product of the cospan (f ≫ g, g) (AlgebraicGeometry.Stack.graph_snd_iso). That projection is the base change of f ≫ g along g, so it is Deligne–Mumford by Stacks 050F; the graph is representable by algebraic spaces by Stacks 050I part (1), and a 1-morphism representable by algebraic spaces is Deligne–Mumford because its relative diagonal is a monomorphism which is locally of finite type, hence unramified by Stacks 05W6. Stacks 050K composes them.

theorem isDM_of_comp {𝒳 𝒴 𝒵 : Stack.AlgebraicStacks.{u, w} B S hS}
    (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵) (hfg : Stack.IsDM B S hS (f ≫ g)) :
    Stack.IsDM B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_comp_of_isSeparated_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationCancellation.lean, line 290. The attribute's comment: “part (3): a separated composite whose second factor has separated relative diagonal has separated first factor”.

Stacks 050M, part (3). If a composite of 1-morphisms of algebraic stacks over S is separated and the relative diagonal Δ_g of its second factor is separated in the sense of Stacks 04XB, then its first factor is separated.

The relative diagonal Δ_{f ≫ g} is Δ_f followed by the comparison 1-morphism i, it is proper in the sense of Stacks 04XB because f ≫ g is separated, i is separated because Δ_g is (Stacks 050H, part (3)), and properness of morphisms of algebraic spaces over S is inherited by the first factor of a composite that has it whose second factor is separated (Stacks 04NX, part (2)).

theorem isSeparated_of_comp_of_isSeparated_diagonal (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsSeparated B S hS (f ≫ g))
    (hΔ : Stack.IsSeparated.{u, u, u + 1} B S hS
      (_root_.AlgebraicGeometry.Stack.relativeDiagonal.{u, u, u + 1} B S hS 𝒴.val 𝒵.val g.hom)) :
    IsSeparated B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparated_of_comp_of_isQuasiSeparated_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationCancellation.lean, line 317. The attribute's comment: “part (4): a quasi-separated composite whose second factor has quasi-separated relative diagonal has quasi-separated first factor”.

Stacks 050M, part (4). If a composite of 1-morphisms of algebraic stacks over S is quasi-separated and the relative diagonal Δ_g of its second factor is quasi-separated in the sense of Stacks 04XB, then its first factor is quasi-separated.

Quasi-separatedness of Stacks 04YW is the conjunction of two conditions of Stacks 04XB on the relative diagonal — quasi-compactness and quasi-separatedness — and each half cancels the comparison 1-morphism i at its own property. The hypothesis on i comes from the one on Δ_g by Stacks 050H, part (2), and it is needed only by the quasi-compact half: quasi-compactness of morphisms of algebraic spaces over S cancels against a quasi-separated second factor (Stacks 03KS), while quasi-separatedness cancels outright (Stacks 03KR).

theorem isQuasiSeparated_of_comp_of_isQuasiSeparated_diagonal (f : 𝒳 ⟶ 𝒴) (g : 𝒴 ⟶ 𝒵)
    (hfg : IsQuasiSeparated B S hS (f ≫ g))
    (hΔ : Stack.IsQuasiSeparated.{u, u, u + 1} B S hS
      (_root_.AlgebraicGeometry.Stack.relativeDiagonal.{u, u, u + 1} B S hS 𝒴.val 𝒵.val g.hom)) :
    IsQuasiSeparated B S hS f

Tag 050N, a lemma

Tag 050N in the Stacks Project.

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

Stacks 050N, part (8). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S whose source is quasi-separated over S and whose target has quasi-separated relative diagonal over S is quasi-separated.

The structure morphism of 𝒳 is f followed by the structure morphism of 𝒴 (AlgebraicGeometry.Stack.comp_structureMorphism, an equality of 1-morphisms on the nose), so the hypothesis on 𝒳 says that that composite is quasi-separated, and Stacks 050M part (4) cancels the second factor. That is the source's own proof: "Parts (5), (6), (7), and (8) follow immediately from Lemma 050M".

theorem isQuasiSeparated_of_isQuasiSeparatedOver
    {𝒳 𝒴 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴)
    (h𝒳 : Stack.IsQuasiSeparatedOver B S hS 𝒳)
    (hΔ : Stack.IsQuasiSeparated B S hS
      (Stack.relativeDiagonalAlgebraicStacks B S hS
        (Stack.structureMorphism B S hS 𝒴)).hom) :
    IsQuasiSeparated B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_iff_isDMOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsoluteDMEquivalence.lean, line 165. The attribute's comment: “dm_equiv”.

Stacks 050N, part (1). An algebraic stack over S is Deligne–Mumford exactly when it is Deligne–Mumford over S.

theorem isAbsolutelyDM_iff_isDMOver (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) :
    IsAbsolutelyDM.{u, w} B S hS hZ 𝒳 ↔ Stack.IsDMOver B S hS 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyQuasiDM_iff_isQuasiDMOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationAbsoluteDMEquivalence.lean, line 173. The attribute's comment: “quasi_dm_equiv”.

Stacks 050N, part (2). An algebraic stack over S is quasi-DM exactly when it is quasi-DM over S.

theorem isAbsolutelyQuasiDM_iff_isQuasiDMOver (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) :
    IsAbsolutelyQuasiDM.{u, w} B S hS hZ 𝒳 ↔ Stack.IsQuasiDMOver B S hS 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparatedOver_of_isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationSmallerBase.lean, line 390. The attribute's comment: “quasi_separated_base”.

Stacks 050N, part (4): a quasi-separated algebraic stack is quasi-separated over its base. This is part (8) of Stacks 050D implying part (4): absolute quasi-separatedness is quasi-separatedness over the terminal scheme Spec ℤ after 𝒳 has been viewed over it by Construction A, so this is AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparatedOver_of_isQuasiSeparatedOver_changeBase at S' = Spec ℤ.

theorem isQuasiSeparatedOver_of_isAbsolutelyQuasiSeparated
    (hZ : B.Contains (⊤_ Scheme.{u})) (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsAbsolutelyQuasiSeparated B S hS hZ 𝒳) :
    Stack.IsQuasiSeparatedOver B S hS 𝒳

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparatedOver_of_isAbsolutelySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationSmallerBaseDMAndSeparated.lean, line 211. The attribute's comment: “separated_base”.

Stacks 050N, the separated assertion: a separated algebraic stack is separated over its base. This is part (7) of Stacks 050D implying part (3): absolute separatedness is separatedness over the terminal scheme Spec ℤ after 𝒳 has been viewed over it by Construction A, so this is AlgebraicGeometry.Stack.AlgebraicStacks.isSeparatedOver_of_isSeparatedOver_changeBase at S' = Spec ℤ.

theorem isSeparatedOver_of_isAbsolutelySeparated
    (hZ : B.Contains (⊤_ Scheme.{u})) (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (h𝒳 : IsAbsolutelySeparated B S hS hZ 𝒳) :
    Stack.IsSeparatedOver B S hS 𝒳

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

Stacks 050N, part (1). An algebraic stack 𝒳 over S is DM if and only if it is DM over S.

The implication from the absolute axiom is AlgebraicGeometry.Stack.isDMOver_of_isDMAbs above, which cancels the second factor of the factorisation 𝒳 ⟶ S ⟶ Spec(ℤ) by part (1) of Stacks 050M and carries the resulting condition on the relative diagonal back from the base Spec(ℤ) to the base S. The converse is AlgebraicGeometry.Stack.isDMAbs_of_isDMOver, which composes along the same factorisation by part (5) of Stacks 050L, using that the second factor is DM (AlgebraicGeometry.Stack.isDMOver_viewOverInt_schemeStack, i.e. that Δ_{S/ℤ} is unramified). Neither direction carries a hypothesis the source does not have.

theorem isDMAbs_iff_isDMOver (𝒵 : AlgebraicStacks.{u, w} B S hS) :
    IsDMAbs.{u, w, w'} B S hS 𝒵 ↔ IsDMOver B S hS 𝒵

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

Stacks 050N, part (2). An algebraic stack 𝒳 over S is quasi-DM if and only if it is quasi-DM over S.

The same two halves as part (1), with local quasi-finiteness in place of unramifiedness: AlgebraicGeometry.Stack.isQuasiDMOver_of_isQuasiDMAbs above runs part (2) of Stacks 050M, and AlgebraicGeometry.Stack.isQuasiDMAbs_of_isQuasiDMOver runs part (6) of Stacks 050L against AlgebraicGeometry.Stack.isQuasiDMOver_viewOverInt_schemeStack. Neither direction carries a hypothesis the source does not have.

theorem isQuasiDMAbs_iff_isQuasiDMOver (𝒵 : AlgebraicStacks.{u, w} B S hS) :
    IsQuasiDMAbs.{u, w, w'} B S hS 𝒵 ↔ IsQuasiDMOver B S hS 𝒵

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

Stacks 050N, part (5). If 𝒳 is DM over S, then every 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is DM.

Being DM over S is DM-ness of the structure morphism of 𝒳 (Stacks 050D, part (1)), and that structure morphism is f followed by the structure morphism of 𝒴 (AlgebraicGeometry.Stack.comp_structureMorphism), so part (1) of Stacks 050M (AlgebraicGeometry.Stack.AlgebraicStacks.isDM_of_comp), which cancels the second factor of a DM composite with no hypothesis on it, gives the conclusion.

theorem isDM_of_isDMOver (f : 𝒳 ⟶ 𝒴) (h𝒳 : IsDMOver B S hS 𝒳) : IsDM B S hS f

AlgebraicGeometry.Stack.isQuasiDM_of_isQuasiDMOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationSourceOverBase.lean, line 277. The attribute's comment: “part (6)”.

Stacks 050N, part (6). If 𝒳 is quasi-DM over S, then every 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is quasi-DM.

The same argument as part (5), with part (2) of Stacks 050M (AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiDM_of_comp) in place of part (1); it too needs no hypothesis on the second factor.

theorem isQuasiDM_of_isQuasiDMOver (f : 𝒳 ⟶ 𝒴) (h𝒳 : IsQuasiDMOver B S hS 𝒳) :
    AlgebraicStacks.IsQuasiDM B S hS f

AlgebraicGeometry.Stack.isSeparated_of_isSeparatedOver_of_isSeparated_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationSourceOverBase.lean, line 292. The attribute's comment: “part (7)”.

Stacks 050N, part (7). If 𝒳 is separated over S and the relative diagonal Δ_{𝒴/S} is separated in the sense of Stacks 04XB, then every 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is separated.

The same argument as part (5), with part (3) of Stacks 050M (AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_comp_of_isSeparated_diagonal) in place of part (1). That part cancels the second factor of a separated composite provided the second factor has separated relative diagonal, and here the second factor is the structure morphism of 𝒴, so the proviso is exactly the hypothesis hΔ that the source's part (7) carries too.

theorem isSeparated_of_isSeparatedOver_of_isSeparated_diagonal (f : 𝒳 ⟶ 𝒴)
    (h𝒳 : IsSeparatedOver B S hS 𝒳)
    (hΔ : IsSeparated.{u, u, u + 1} B S hS
      (relativeDiagonal.{u, u, u + 1} B S hS 𝒴.val
        (schemeStack.{u, w} B S hS (Over.mk (𝟙 (B.obj hS)))).val
        (structureMorphism B S hS 𝒴).hom)) :
    AlgebraicStacks.IsSeparated B S hS f

AlgebraicGeometry.Stack.isQuasiSeparated_of_isQuasiSeparatedOver_of_isQuasiSeparated_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationSourceOverBase.lean, line 311. The attribute's comment: “part (8)”.

Stacks 050N, part (8). If 𝒳 is quasi-separated over S and the relative diagonal Δ_{𝒴/S} is quasi-separated in the sense of Stacks 04XB, then every 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is quasi-separated.

The same argument as part (7), with part (4) of Stacks 050M (AlgebraicGeometry.Stack.AlgebraicStacks.isQuasiSeparated_of_comp_of_isQuasiSeparated_diagonal) in place of part (3); the hypothesis hΔ is again what that part needs of the second factor, which here is the structure morphism of 𝒴.

theorem isQuasiSeparated_of_isQuasiSeparatedOver_of_isQuasiSeparated_diagonal (f : 𝒳 ⟶ 𝒴)
    (h𝒳 : IsQuasiSeparatedOver B S hS 𝒳)
    (hΔ : IsQuasiSeparated.{u, u, u + 1} B S hS
      (relativeDiagonal.{u, u, u + 1} B S hS 𝒴.val
        (schemeStack.{u, w} B S hS (Over.mk (𝟙 (B.obj hS)))).val
        (structureMorphism B S hS 𝒴).hom)) :
    AlgebraicStacks.IsQuasiSeparated B S hS f

Tag 06MB, a lemma

Tag 06MB in the Stacks Project.

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

Stacks 06MB, part (1). Let 𝒳 be an algebraic stack over S and let f : 𝒲 ⟶ 𝒳 be surjective, flat and locally of finite presentation with 𝒲 representable by an algebraic space. If f is unramified in the relative sense of Stacks 03YK, then 𝒳 is Deligne–Mumford.

Unramifiedness passes from f to the absolute diagonal of 𝒳 by AlgebraicGeometry.Stack.hasRelativeProperty_diagonal_of_flatCover, the cancellation of first factors being Stacks 06G6; the absolute diagonal and the relative diagonal of the structure 1-morphism have the same relative properties, and Stacks 050N part (1) turns DM over S into DM.

theorem isAbsolutelyDM_of_isUnramified_flatCover
    {𝒳 𝒲 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒲 ⟶ 𝒳)
    (h𝒲 : IsRepresentableByAlgebraicSpace B S hS 𝒲.val)
    (hSurj : IsSurjective B S hS f)
    (hFlat : IsFlat B S hS f)
    (hLfp : IsLocallyOfFinitePresentation B S hS f)
    (hUnr : 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)
        f.hom
        (isRepresentableByAlgebraicSpaces_of_isAlgebraicStack B S hS 𝒳.property h𝒲 f.hom)) :
    IsAbsolutelyDM.{u, w} B S hS hZ 𝒳

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

Stacks 06MB, part (2). Let 𝒳 be an algebraic stack over S and let f : 𝒲 ⟶ 𝒳 be surjective, flat and locally of finite presentation with 𝒲 representable by an algebraic space. If f is locally quasi-finite in the relative sense of Stacks 03YK, then 𝒳 is quasi-DM.

This is the argument of part (1) with the cancellation of first factors supplied by Stacks 03XN.

theorem isAbsolutelyQuasiDM_of_isLocallyQuasiFinite_flatCover
    {𝒳 𝒲 : Stack.AlgebraicStacks.{u, w} B S hS} (f : 𝒲 ⟶ 𝒳)
    (h𝒲 : IsRepresentableByAlgebraicSpace B S hS 𝒲.val)
    (hSurj : IsSurjective B S hS f)
    (hFlat : IsFlat B S hS f)
    (hLfp : IsLocallyOfFinitePresentation B S hS f)
    (hQf : haveI : (Space.locallyQuasiFiniteProperty B S hS).IsStableUnderBaseChange :=
        Space.isLocallyQuasiFinite_isStableUnderBaseChange B S hS
      HasRelativeProperty.{u, u, u + 1, u} B S hS
        (Space.locallyQuasiFiniteProperty B S hS) f.hom
        (isRepresentableByAlgebraicSpaces_of_isAlgebraicStack B S hS 𝒳.property h𝒲 f.hom)) :
    IsAbsolutelyQuasiDM.{u, w} B S hS hZ 𝒳

Tag 06MY, a lemma

Tag 06MY in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isDM_of_isMonomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismDeligneMumford.lean, line 109. The attribute's comment: “monomorphisms are DM”.

Stacks 06MY, the Deligne–Mumford assertion for monomorphisms. A monomorphism of algebraic stacks over S is Deligne–Mumford.

A monomorphism is representable by algebraic spaces — the first conjunct of AlgebraicGeometry.Stack.AlgebraicStacks.IsMonomorphism, Stacks 04ZW — and a 1-morphism representable by algebraic spaces is Deligne–Mumford, so the monomorphism condition on the represented base changes is not needed. The source argues instead that the relative diagonal of a monomorphism is an isomorphism and that an isomorphism of algebraic spaces is unramified; the route taken here reaches the same conclusion from less.

theorem isDM_of_isMonomorphism (f : 𝒵 ⟶ 𝒳) (hf : IsMonomorphism B S hS f) :
    Stack.IsDM B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_isMonomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismDeligneMumford.lean, line 131. The attribute's comment: “monomorphisms are separated”.

Stacks 06MY, the separatedness assertion for monomorphisms. A monomorphism of algebraic stacks over S is separated.

Every algebraic space representing a base change of a monomorphism has monomorphic structural morphism, so that morphism is a monomorphism of presheaves (Stacks 042M) and hence separated (Stacks 042N); so the monomorphism is separated in the relative sense of Stacks 04XB, and its relative diagonal is therefore proper by Stacks 04YS.

The source argues instead that the relative diagonal of a monomorphism is an isomorphism and that an isomorphism of algebraic spaces is proper; the route taken here reaches the same conclusion without that comparison.

theorem isSeparated_of_isMonomorphism (f : 𝒵 ⟶ 𝒳) (hf : IsMonomorphism B S hS f) :
    IsSeparated B S hS f

AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismDeligneMumford.lean, line 151. The attribute's comment: “immersions are separated”.

Stacks 06MY, the separatedness assertion for immersions. An immersion of algebraic stacks over S is separated.

An immersion is a monomorphism by Stacks 0504, so this is AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_isMonomorphism. This is the reduction the source makes when it says that the same is true for immersions.

theorem isSeparated_of_isImmersion (j : 𝒵 ⟶ 𝒳) (hj : IsImmersion B S hS j) :
    IsSeparated B S hS j

AlgebraicGeometry.Stack.AlgebraicStacks.isDM_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/UnramifiedImmersionAlgebraicStack.lean, line 92. The attribute's comment: “immersions are DM”.

Stacks 06MY, the Deligne–Mumford assertion for immersions. An immersion of algebraic stacks over S is Deligne–Mumford.

An immersion is representable by algebraic spaces — the first conjunct of Stacks 04YL, part (3) — and a 1-morphism representable by algebraic spaces is Deligne–Mumford, so the immersion condition on the represented base changes is not needed. The source reduces the assertion to the monomorphism case, an immersion being a monomorphism by Stacks 0504; the route taken here reaches the same conclusion from less. The separatedness assertion of Stacks 06MY for immersions, which does use the immersion condition, is AlgebraicGeometry.Stack.AlgebraicStacks.isSeparated_of_isImmersion.

theorem isDM_of_isImmersion (j : 𝒵 ⟶ 𝒳) (hj : IsImmersion B S hS j) : Stack.IsDM B S hS j

Tag 06MZ, a lemma

Tag 06MZ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_of_isMonomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismDeligneMumford.lean, line 165. The attribute's comment: “DM case”.

Stacks 06MZ, the Deligne–Mumford clause. The source of a monomorphism into a Deligne–Mumford algebraic stack is Deligne–Mumford.

The monomorphism is a Deligne–Mumford 1-morphism by Stacks 06MY, so part (5) of Stacks 050L applies to it. The statement is made at an arbitrary monomorphism, which is the form in which Stacks 06MZ's own proof uses it; see the implementation notes.

theorem isAbsolutelyDM_of_isMonomorphism (f : 𝒵 ⟶ 𝒳) (hf : IsMonomorphism B S hS f)
    (h𝒳 : IsAbsolutelyDM B S hS hZ 𝒳) :
    IsAbsolutelyDM B S hS hZ 𝒵

AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyQuasiDM_of_isMonomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismDeligneMumford.lean, line 177. The attribute's comment: “quasi-DM case”.

Stacks 06MZ, the quasi-Deligne–Mumford clause. The source of a monomorphism into a quasi-Deligne–Mumford algebraic stack is quasi-Deligne–Mumford.

The quasi-Deligne–Mumford counterpart of AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyDM_of_isMonomorphism, through part (6) of Stacks 050L.

theorem isAbsolutelyQuasiDM_of_isMonomorphism (f : 𝒵 ⟶ 𝒳) (hf : IsMonomorphism B S hS f)
    (h𝒳 : IsAbsolutelyQuasiDM B S hS hZ 𝒳) :
    IsAbsolutelyQuasiDM B S hS hZ 𝒵

AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelySeparated_of_isMonomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismDeligneMumford.lean, line 189. The attribute's comment: “separated case”.

Stacks 06MZ, the separatedness clause. The source of a monomorphism into a separated algebraic stack is separated.

The monomorphism is a separated 1-morphism by Stacks 06MY, so part (7) of Stacks 050L applies to it.

theorem isAbsolutelySeparated_of_isMonomorphism (f : 𝒵 ⟶ 𝒳) (hf : IsMonomorphism B S hS f)
    (h𝒳 : IsAbsolutelySeparated B S hS hZ 𝒳) :
    IsAbsolutelySeparated B S hS hZ 𝒵

AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelyQuasiSeparated_of_isMonomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/MonomorphismDeligneMumford.lean, line 202. The attribute's comment: “quasi-separated case”.

Stacks 06MZ, the quasi-separatedness clause. The source of a monomorphism into a quasi-separated algebraic stack is quasi-separated.

The quasi-separated counterpart of AlgebraicGeometry.Stack.AlgebraicStacks.isAbsolutelySeparated_of_isMonomorphism, through part (8) of Stacks 050L.

theorem isAbsolutelyQuasiSeparated_of_isMonomorphism (f : 𝒵 ⟶ 𝒳)
    (hf : IsMonomorphism B S hS f) (h𝒳 : IsAbsolutelyQuasiSeparated B S hS hZ 𝒳) :
    IsAbsolutelyQuasiSeparated B S hS hZ 𝒵

Sources

• Section 101.4, Tag 04YV
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.IsDM · AlgebraicGeometry.Stack.AlgebraicStacks.IsQuasiDM · AlgebraicGeometry.Stack.AlgebraicStacks.IsSeparated · AlgebraicGeometry.Stack.AlgebraicStacks.IsQuasiSeparated · AlgebraicGeometry.Stack.AlgebraicStacks.IsAbsolutelyDM · AlgebraicGeometry.Stack.AlgebraicStacks.IsAbsolutelyQuasiDM · AlgebraicGeometry.Stack.AlgebraicStacks.IsAbsolutelySeparated · AlgebraicGeometry.Stack.AlgebraicStacks.IsAbsolutelyQuasiSeparated

Section101.5 Inertia stacks#

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

Tag 050Q, a lemma

Tag 050Q in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_inertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaAlgebraic.lean, line 55. The attribute's comment: “absolute inertia is algebraic”.

The inertia I_𝒳 of an algebraic stack 𝒳 over S is an algebraic stack over S.

theorem isAlgebraicStack_inertia
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val) :
    IsAlgebraicStack.{u, w} B S hS (inertia B S hS 𝒳).val

AlgebraicGeometry.Stack.isAlgebraicStack_relativeInertia, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaAlgebraic.lean, line 120. The attribute's comment: “relative inertia is algebraic”.

The relative inertia I_{𝒳/𝒴} of a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is an algebraic stack over S.

theorem isAlgebraicStack_relativeInertia
    (𝒳 𝒴 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (f : 𝒳 ⟶ 𝒴)
    (h𝒳 : IsAlgebraicStack.{u, w} B S hS 𝒳.val)
    (h𝒴 : IsAlgebraicStack.{u, w} B S hS 𝒴.val) :
    IsAlgebraicStack.{u, w} B S hS (RelativeInertia.basedCategory f.hom)

AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_inertiaProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaFieldSpectrumCover.lean, line 92. The attribute's comment: “local finite type of the inertia projection in the sense of Stacks 06FS part (1)”.

Stacks 050Q, local finite type of the inertia projection, in the sense of Stacks 06FS part (1). The forgetful 1-morphism I_𝒳 ⟶ 𝒳 of the inertia of an algebraic stack 𝒳 over S is locally of finite type as a 1-morphism of algebraic stacks.

AlgebraicGeometry.Stack.isLocallyOfFiniteType_inertiaProjection is the same statement in the relative sense of Properties of Stacks, Section 04XB; the inertia projection is representable by algebraic spaces by Stacks 050Q, so Stacks 06FM for a representable 1-morphism converts the relative property into the existential smooth-diagram test, and the universal one follows because local finite type is smooth local on the source-and-target.

theorem isLocallyOfFiniteType_inertiaProjection (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) :
    IsLocallyOfFiniteType B S hS (Stack.inertiaProjectionAlgebraicStacks B S hS 𝒳)

AlgebraicGeometry.Stack.isLocallyOfFiniteType_inertiaProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaProjectionFiniteType.lean, line 197. The attribute's comment: “local finite type of the absolute inertia projection”.

Stacks 050Q, local finite type of the inertia projection. The forgetful 1-morphism π : I_𝒳 ⟶ 𝒳 of the inertia of an algebraic stack 𝒳 over S is locally of finite type, in the sense of Properties of Stacks, Section 04XB.

By Stacks 034H (1) the inertia is the 2-fibre product 𝒳 ×_{Δ, 𝒳 × 𝒳, Δ} 𝒳, and under that identification π is the first projection of the canonical 2-fibre product square over the cospan (Δ, Δ), hence a base change of Δ. So this is Stacks 045C applied to AlgebraicGeometry.Stack.isLocallyOfFiniteType_diagonal_of_isAlgebraicStack and transported along that equivalence of sources by Stacks 0457.

theorem isLocallyOfFiniteType_inertiaProjection (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    IsLocallyOfFiniteType B S hS (inertiaProjectionAlgebraicStacks.{u, w} B S hS 𝒳).hom

AlgebraicGeometry.Stack.isLocallyOfFiniteType_relativeInertiaProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaProjectionFiniteType.lean, line 216. The attribute's comment: “local finite type of the relative inertia projection”.

Stacks 050Q, local finite type of the relative inertia projection. The forgetful 1-morphism π : I_{𝒳/𝒴} ⟶ 𝒳 of the relative inertia of a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is locally of finite type, in the sense of Properties of Stacks, Section 04XB.

By Stacks 034H (1) the relative inertia is the 2-fibre product 𝒳 ×_{Δ_f, 𝒳 ×_𝒴 𝒳, Δ_f} 𝒳, and under that identification π is the first projection of the canonical 2-fibre product square over the cospan (Δ_f, Δ_f), hence a base change of the relative diagonal. So this is Stacks 045C applied to part (2) of Stacks 04XS, transported along that equivalence of sources by Stacks 0457.

theorem isLocallyOfFiniteType_relativeInertiaProjection
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) :
    IsLocallyOfFiniteType B S hS (relativeInertiaProjection B S hS f).hom

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_inertiaProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaProjectionRepresentable.lean, line 55. The attribute's comment: “representability by algebraic spaces of the absolute inertia projection”.

If the diagonal of a category fibred in groupoids 𝒳 over the big fppf site of S is representable by algebraic spaces, then so is the forgetful 1-morphism π : I_𝒳 ⟶ 𝒳 of its inertia.

theorem isRepresentableByAlgebraicSpaces_inertiaProjection
    (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))
    (hΔ : IsRepresentableByAlgebraicSpaces B S hS (diagonalBasedFunctor B S hS 𝒳)) :
    IsRepresentableByAlgebraicSpaces B S hS
      (RelativeInertia.basedProjection
        (𝒴 := BasedCategory.ofFunctor (𝟭 (BigFppfOver B S hS)))
        ⟨𝒳.val.p, rfl⟩)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_inertiaProjection_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaProjectionRepresentable.lean, line 100. The attribute's comment: “the inertia projection of an algebraic stack is representable by spaces”.

The forgetful 1-morphism π : I_𝒳 ⟶ 𝒳 of the inertia of an algebraic stack 𝒳 is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_inertiaProjection_of_isAlgebraicStack
    (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))
    (h𝒳 : IsAlgebraicStack.{u, t} B S hS 𝒳.val) :
    IsRepresentableByAlgebraicSpaces B S hS
      (RelativeInertia.basedProjection
        (𝒴 := BasedCategory.ofFunctor (𝟭 (BigFppfOver B S hS)))
        ⟨𝒳.val.p, rfl⟩)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_relativeInertiaProjection_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaProjectionRepresentable.lean, line 185. The attribute's comment: “representability by algebraic spaces of the relative inertia projection”.

Stacks 050Q for the relative inertia of a morphism of algebraic stacks. The forgetful 1-morphism π : I_{𝒳/𝒴} ⟶ 𝒳 of the relative inertia of a 1-morphism of algebraic stacks is representable by algebraic spaces. Only the representability of the two diagonals — the second clause of AlgebraicGeometry.Stack.IsAlgebraicStack — is used.

The source's statement also asserts that I_{𝒳/𝒴} is an algebraic stack and that π is locally of finite type; neither is proved here.

theorem isRepresentableByAlgebraicSpaces_relativeInertiaProjection_of_isAlgebraicStack
    (𝒳 𝒴 : CatFiberedInGroupoids.{u, max u v, u + 1, max (max (u + 1) w) v}
      (BigFppfOver B S hS))
    (f : 𝒳 ⟶ 𝒴)
    (h𝒳 : IsAlgebraicStack.{u, t} B S hS 𝒳.val)
    (h𝒴 : IsAlgebraicStack.{u, t} B S hS 𝒴.val) :
    IsRepresentableByAlgebraicSpaces B S hS (RelativeInertia.basedProjection f.hom)

Tag 050R, a remark

Tag 050R in the Stacks Project.

CategoryTheory.RelativeInertia.inverse, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 96. The attribute's comment: “the inverse”.

The inverse of the group law: the 1-morphism i : I_{S/S'} ⟶ I_{S/S'}, (x, α) ↦ (x, α⁻¹), acting on morphisms by the identity.

def inverse (F : S ⥤ S') : RelativeInertia F ⥤ RelativeInertia F

CategoryTheory.RelativeInertia.inverse_comp_π, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 120. The attribute's comment: “the inverse is a morphism over the source”.

The inverse is a morphism over the source: followed by the projection to S it is that projection again.

theorem inverse_comp_π (F : S ⥤ S') :
    inverse F ⋙ RelativeInertia.π F = RelativeInertia.π F

CategoryTheory.RelativeInertia.composition_pairIdNeutral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 247. The attribute's comment: “the right unit axiom”.

The right unit axiom: c ∘ ⟨id, e ∘ π⟩ = id.

theorem composition_pairIdNeutral :
    pairIdNeutral F p ⋙ composition F p = 𝟭 (RelativeInertia F)

CategoryTheory.RelativeInertia.composition_pairNeutralId, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 261. The attribute's comment: “the left unit axiom”.

The left unit axiom: c ∘ ⟨e ∘ π, id⟩ = id.

theorem composition_pairNeutralId :
    pairNeutralId F p ⋙ composition F p = 𝟭 (RelativeInertia F)

CategoryTheory.RelativeInertia.composition_pairIdInverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 276. The attribute's comment: “the right inverse axiom”.

The right inverse axiom: c ∘ ⟨id, i⟩ = e ∘ π.

theorem composition_pairIdInverse :
    pairIdInverse F p ⋙ composition F p =
      RelativeInertia.π F ⋙ RelativeInertia.neutralSection F

CategoryTheory.RelativeInertia.composition_pairInverseId, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 292. The attribute's comment: “the left inverse axiom”.

The left inverse axiom: c ∘ ⟨i, id⟩ = e ∘ π.

theorem composition_pairInverseId :
    pairInverseId F p ⋙ composition F p =
      RelativeInertia.π F ⋙ RelativeInertia.neutralSection F

CategoryTheory.RelativeInertia.composition_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 448. The attribute's comment: “the associativity axiom”.

The associativity axiom: c ∘ (c × id) = c ∘ (id × c) ∘ assoc as 1-morphisms (I_{S/S'} ×_S I_{S/S'}) ×_S I_{S/S'} ⟶ I_{S/S'} over S: both send (((x, α), (x', α'), β), (x'', α''), δ) to (x, α ∘ β⁻¹ ∘ α' ∘ β ∘ δ⁻¹ ∘ α'' ∘ δ).

theorem composition_assoc :
    compFstPair F p ⋙ composition F p = idCompPair F p ⋙ composition F p

AlgebraicGeometry.Stack.relativeInertiaPairOverStack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 473. The attribute's comment: “the twofold product of the relative inertia in the 2-category of morphisms to the source representable by algebraic spaces”.

I_{𝒳/𝒴} ×_𝒳 I_{𝒳/𝒴} as an object of Spaces/𝒳: the 2-fibre product of the projection with itself, with structure 1-morphism to 𝒳 the first projection followed by π.

noncomputable def relativeInertiaPairOverStack (f : 𝒳 ⟶ 𝒴) : SpacesOverStack B S hS 𝒳

AlgebraicGeometry.Stack.relativeInertiaCompositionHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 497. The attribute's comment: “the composition law as a 1-morphism of the 2-category of morphisms to the source representable by algebraic spaces”.

The composition law as a 1-morphism of Spaces/𝒳: the functor c : I_{𝒳/𝒴} ×_𝒳 I_{𝒳/𝒴} ⟶ I_{𝒳/𝒴}, ((x, α), (x', α'), β) ↦ (x, α ∘ β⁻¹ ∘ α' ∘ β), with the identity as comparison 2-morphism.

noncomputable def relativeInertiaCompositionHom (f : 𝒳 ⟶ 𝒴) :
    relativeInertiaPairOverStack B S hS f ⟶ relativeInertiaOverStack B S hS f

AlgebraicGeometry.Stack.relativeInertiaInverseHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 508. The attribute's comment: “the inverse as a 1-morphism of the 2-category of morphisms to the source representable by algebraic spaces”.

The inverse as a 1-morphism of Spaces/𝒳: the functor i : I_{𝒳/𝒴} ⟶ I_{𝒳/𝒴}, (x, α) ↦ (x, α⁻¹), with the identity as comparison 2-morphism.

noncomputable def relativeInertiaInverseHom (f : 𝒳 ⟶ 𝒴) :
    relativeInertiaOverStack B S hS f ⟶ relativeInertiaOverStack B S hS f

AlgebraicGeometry.Stack.relativeInertiaNeutralHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 517. The attribute's comment: “the neutral element as a 1-morphism of algebraic stacks”.

The neutral element as a 1-morphism of algebraic stacks: e : 𝒳 ⟶ I_{𝒳/𝒴}, x ↦ (x, id_x).

noncomputable def relativeInertiaNeutralHom (f : 𝒳 ⟶ 𝒴) :
    𝒳 ⟶ (relativeInertiaOverStack B S hS f).source

AlgebraicGeometry.Stack.relativeInertiaNeutralHom_comp_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupAxioms.lean, line 525. The attribute's comment: “the neutral element is a section of the projection”.

The neutral element is a section of the projection: e ≫ π = 𝟙 𝒳, an equality of 1-morphisms of algebraic stacks.

theorem relativeInertiaNeutralHom_comp_map (f : 𝒳 ⟶ 𝒴) :
    relativeInertiaNeutralHom B S hS f ≫ (relativeInertiaOverStack B S hS f).map = 𝟙 𝒳

CategoryTheory.RelativeInertia.composition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupLaw.lean, line 108. The attribute's comment: “the composition law”.

Stacks 050R, the composition law of the relative inertia. On the 2-fibre product I_{S/S'} ×_S I_{S/S'}, whose objects are the triples ((x, α), (x', α'), β) with β : x ≅ x' a vertical isomorphism, it is the functor ((x, α), (x', α'), β) ↦ (x, α ∘ β⁻¹ ∘ α' ∘ β), acting on morphisms by their first component.

def composition (F : S ⥤ S') (p : S ⥤ C) :
    TwoFibreProductOver (RelativeInertia.π F ⋙ p) (RelativeInertia.π F ⋙ p) p
        (RelativeInertia.π F) (RelativeInertia.π F) ⥤ RelativeInertia F

CategoryTheory.RelativeInertia.composition_comp_π, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupLaw.lean, line 147. The attribute's comment: “the composition law is a morphism over the source”.

The composition law is a morphism over the source: followed by the projection to S it is the first projection of the 2-fibre product followed by that projection.

theorem composition_comp_π (F : S ⥤ S') (p : S ⥤ C) :
    composition F p ⋙ RelativeInertia.π F =
      TwoFibreProductOver.fst (RelativeInertia.π F ⋙ p) (RelativeInertia.π F ⋙ p) p
        (RelativeInertia.π F) (RelativeInertia.π F) ⋙ RelativeInertia.π F

AlgebraicGeometry.Stack.relativeInertiaOverStack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupLaw.lean, line 169. The attribute's comment: “the relative inertia as an object of the 2-category of morphisms to the source representable by algebraic spaces”.

The relative inertia as an object of Spaces/𝒳. For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, the relative inertia I_{𝒳/𝒴} is an algebraic stack and its projection to 𝒳 is representable by algebraic spaces, so the pair is an object of the 2-category of Stacks 04ZQ. This is the ambient object of which Stacks 050R asserts that it is a group object.

noncomputable def relativeInertiaOverStack
    {𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS} (f : 𝒳 ⟶ 𝒴) : SpacesOverStack B S hS 𝒳

AlgebraicGeometry.Stack.relativeInertiaGrpObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupObject.lean, line 806.

Stacks 050R. For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, the relative inertia I_{𝒳/𝒴} is a group object of the category of 1-morphisms to 𝒳 representable by algebraic spaces (Stacks 04ZQ): its multiplication is the composition law c : I_{𝒳/𝒴} ×_𝒳 I_{𝒳/𝒴} ⟶ I_{𝒳/𝒴}, ((x, α), (x', α'), β) ↦ (x, α ∘ β⁻¹ ∘ α' ∘ β), its unit is the neutral element e : 𝒳 ⟶ I_{𝒳/𝒴}, x ↦ (x, id_x), and its inverse is i : (x, α) ↦ (x, α⁻¹).

noncomputable def relativeInertiaGrpObj (f : 𝒳 ⟶ 𝒴) : GrpObj (IsoClassCategory.mk
  (relativeInertiaOverStack B S hS f))

AlgebraicGeometry.Stack.relativeInertiaGrpObj_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupObject.lean, line 853. The attribute's comment: “the multiplication of the group object is the composition law”.

Stacks 050R. The multiplication of the group object is the composition law c.

theorem relativeInertiaGrpObj_mul (f : 𝒳 ⟶ 𝒴) :
    letI := relativeInertiaGrpObj B S hS f
    MonObj.mul (X := IsoClassCategory.mk (relativeInertiaOverStack B S hS f)) =
      IsoClassCategory.homMk (C := SpacesOverStack B S hS 𝒳) (relativeInertiaMulHom B S hS f)

AlgebraicGeometry.Stack.relativeInertiaGrpObj_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupObject.lean, line 860. The attribute's comment: “the unit of the group object is the neutral element”.

Stacks 050R. The unit of the group object is the neutral element e.

theorem relativeInertiaGrpObj_one (f : 𝒳 ⟶ 𝒴) :
    letI := relativeInertiaGrpObj B S hS f
    MonObj.one (X := IsoClassCategory.mk (relativeInertiaOverStack B S hS f)) =
      IsoClassCategory.homMk (C := SpacesOverStack B S hS 𝒳) (relativeInertiaOneHom B S hS f)

AlgebraicGeometry.Stack.relativeInertiaGrpObj_inv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupObject.lean, line 867. The attribute's comment: “the inverse of the group object”.

Stacks 050R. The inverse of the group object is i.

theorem relativeInertiaGrpObj_inv (f : 𝒳 ⟶ 𝒴) :
    GrpObj.inv (X := IsoClassCategory.mk (relativeInertiaOverStack B S hS f)) (self :=
      relativeInertiaGrpObj B S hS f) =
      IsoClassCategory.homMk (C := SpacesOverStack B S hS 𝒳) (relativeInertiaInvHom B S hS f)

Declarations registered for the tag:

• CategoryTheory.RelativeInertia.neutralSection, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaGroupLaw.lean, line 154 (StacksFrontier): “the neutral element”.

Tag 0CPJ, an equation

Tag 0CPJ in the Stacks Project.

AlgebraicGeometry.Stack.isomSpaceMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSequence.lean, line 177. The attribute's comment: “the map Isom_𝒳(x, x) → Isom_𝒴(y, y)”.

The map Isom_𝒳(x, y) ⟶ Isom_𝒴(f(x), f(y)) of sheaves on the big fppf site of U induced by a 1-morphism f : 𝒳 ⟶ 𝒴: it applies f to a local isomorphism and compares the chosen pullbacks of x and y with those of their images.

def isomSpaceMap (x y : 𝒳.val.p.Fiber U) :
    isomSpace B S hS 𝒳 U x y ⟶
      isomSpace B S hS 𝒴 U (imageFiberObj B S hS 𝒳 𝒴 F U x)
        (imageFiberObj B S hS 𝒳 𝒴 F U y)

AlgebraicGeometry.Stack.relativeIsomSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSequence.lean, line 201. The attribute's comment: “the sheaf Isom_{𝒳/𝒴}(x, x)”.

The relative automorphism sheaf Isom_{𝒳/𝒴}(x, x), as a subsheaf of Isom_𝒳(x, x): its sections over V are the local automorphisms α of x with f(α) = id.

def relativeIsomSubfunctor (x : 𝒳.val.p.Fiber U) :
    Subfunctor (isomSpace B S hS 𝒳 U x x)

AlgebraicGeometry.Stack.relativeIsomSpaceGrpObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSequence.lean, line 222. The attribute's comment: “the group structure on Isom_{𝒳/𝒴}(x, x)”.

The group structure on Isom_{𝒳/𝒴}(x, x), restricted from that of Isom_𝒳(x, x).

def relativeIsomSpaceGrpObj (x : 𝒳.val.p.Fiber U) :
    GrpObj (relativeIsomSpace B S hS 𝒳 𝒴 F U x)

AlgebraicGeometry.Stack.isMonHom_relativeIsomSpaceι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSequence.lean, line 284. The attribute's comment: “the first map is a homomorphism of sheaves of groups”.

The inclusion Isom_{𝒳/𝒴}(x, x) ⟶ Isom_𝒳(x, x) is a homomorphism of sheaves of groups.

theorem isMonHom_relativeIsomSpaceι (x : 𝒳.val.p.Fiber U) :
    letI : 𝒳.val.p.IsPreFibered := 𝒳.isFiberedInGroupoids.isFibered.toIsPreFibered
    letI : GrpObj (isomSpace B S hS 𝒳 U x x) := isomSpaceGrpObj B S hS 𝒳 U x
    letI : GrpObj (relativeIsomSpace B S hS 𝒳 𝒴 F U x) :=
      relativeIsomSpaceGrpObj B S hS 𝒳 𝒴 F U x
    IsMonHom (relativeIsomSubfunctor B S hS 𝒳 𝒴 F U x).ι

AlgebraicGeometry.Stack.isMonHom_isomSpaceMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSequence.lean, line 298. The attribute's comment: “the second map is a homomorphism of sheaves of groups”.

The map Isom_𝒳(x, x) ⟶ Isom_𝒴(f(x), f(x)) is a homomorphism of sheaves of groups.

theorem isMonHom_isomSpaceMap (x : 𝒳.val.p.Fiber U) :
    letI : 𝒳.val.p.IsPreFibered := 𝒳.isFiberedInGroupoids.isFibered.toIsPreFibered
    letI : 𝒴.val.p.IsPreFibered := 𝒴.isFiberedInGroupoids.isFibered.toIsPreFibered
    letI : GrpObj (isomSpace B S hS 𝒳 U x x) := isomSpaceGrpObj B S hS 𝒳 U x
    letI : GrpObj (isomSpace B S hS 𝒴 U (imageFiberObj B S hS 𝒳 𝒴 F U x)
        (imageFiberObj B S hS 𝒳 𝒴 F U x)) :=
      isomSpaceGrpObj B S hS 𝒴 U (imageFiberObj B S hS 𝒳 𝒴 F U x)
    IsMonHom (isomSpaceMap B S hS 𝒳 𝒴 F U x x)

AlgebraicGeometry.Stack.relativeIsomSpaceι_app_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSequence.lean, line 323. The attribute's comment: “injectivity of the first map”.

The inclusion Isom_{𝒳/𝒴}(x, x) ⟶ Isom_𝒳(x, x) is injective on sections.

theorem relativeIsomSpaceι_app_injective (x : 𝒳.val.p.Fiber U)
    (V : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ)
    (a b : (relativeIsomSpace B S hS 𝒳 𝒴 F U x).obj V)
    (h : (relativeIsomSubfunctor B S hS 𝒳 𝒴 F U x).ι.app V a =
      (relativeIsomSubfunctor B S hS 𝒳 𝒴 F U x).ι.app V b) : a = b

AlgebraicGeometry.Stack.relativeIsom_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSequence.lean, line 334. The attribute's comment: “exactness at Isom_𝒳(x, x)”.

The sequence 0 → Isom_{𝒳/𝒴}(x, x) → Isom_𝒳(x, x) → Isom_𝒴(y, y) is exact at the middle term: a local automorphism of x has identity image in Isom_𝒴(y, y) exactly when it comes from a relative automorphism of x.

theorem relativeIsom_exact (x : 𝒳.val.p.Fiber U)
    (V : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ)
    (m : (isomSpace B S hS 𝒳 U x x).obj V) :
    ((isomSpaceMap B S hS 𝒳 𝒴 F U x x).app V m).1 = 𝟙 _ ↔
      ∃ n : (relativeIsomSpace B S hS 𝒳 𝒴 F U x).obj V,
        (relativeIsomSubfunctor B S hS 𝒳 𝒴 F U x).ι.app V n = m

Tag 06PP, a definition

Tag 06PP in the Stacks Project.

AlgebraicGeometry.Stack.relativeAutomorphismSpaceOverSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 181. The attribute's comment: “part (1): the relative sheaf of automorphisms, Z ×_{x, X} I_{X/Y}”.

Stacks 06PP, part (1): the relative sheaf of automorphisms of x. For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks and an algebraic-space-valued point x : Z ⟶ 𝒳, the 2-fibre product

Isom_{𝒳/𝒴}(x, x) = Z ×_{x, 𝒳} ℐ_{𝒳/𝒴}

of x with the forgetful 1-morphism of the relative inertia, read in the 2-category of categories fibred in groupoids over the big fppf site of S. Its objects over a scheme W are the triples of a point z of Z over W, an object (a, α) of the relative inertia over W — that is, an object a of 𝒳 over W together with an automorphism α of a killed by f — and a vertical isomorphism x(z) ≅ a; so a section over W is an automorphism of x(z) killed by f, which is what the source calls an automorphism of x over W relative to 𝒴.

noncomputable def relativeAutomorphismSpaceOverSpace (f : 𝒳 ⟶ 𝒴)
    (x : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    CatFiberedInGroupoids (BigFppfOver B S hS)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_relativeAutomorphismSpaceOverSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 208. The attribute's comment: “part (1): Isom_{X/Y}(x, x) is an algebraic space”.

Stacks 06PP, part (1): Isom_{𝒳/𝒴}(x, x) is an algebraic space. The relative sheaf of automorphisms of an algebraic-space-valued point x : Z ⟶ 𝒳 of an algebraic stack is represented by an algebraic space over S.

Stacks 050Q makes the forgetful 1-morphism ℐ_{𝒳/𝒴} ⟶ 𝒳 of the relative inertia representable by algebraic spaces — only the representability of the two diagonals, the second clause of AlgebraicGeometry.Stack.IsAlgebraicStack, is used for that — and Z represents the stack of Z, so Stacks 0300 applies to the cospan (x, ℐ_{𝒳/𝒴} ⟶ 𝒳).

theorem isRepresentableByAlgebraicSpace_relativeAutomorphismSpaceOverSpace (f : 𝒳 ⟶ 𝒴)
    (x : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    IsRepresentableByAlgebraicSpace B S hS
      (relativeAutomorphismSpaceOverSpace B S hS Z hZ f x)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_relativeAutomorphismSpaceOverSpaceProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 228. The attribute's comment: “part (1): Isom_{X/Y}(x, x) is an algebraic space over Z”.

Stacks 06PP, part (1): Isom_{𝒳/𝒴}(x, x) is an algebraic space over Z. The projection of the relative sheaf of automorphisms of x to the stack of Z is representable by algebraic spaces, so — together with AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_relativeAutomorphismSpaceOverSpace, which makes its source an algebraic space — it is a morphism of algebraic spaces with target Z.

This is Stacks 0302 for the base change of the representable 1-morphism ℐ_{𝒳/𝒴} ⟶ 𝒳 of Stacks 050Q along x.

theorem isRepresentableByAlgebraicSpaces_relativeAutomorphismSpaceOverSpaceProj (f : 𝒳 ⟶ 𝒴)
    (x : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    IsRepresentableByAlgebraicSpaces B S hS
      (relativeAutomorphismSpaceOverSpaceProj B S hS Z hZ f x)

AlgebraicGeometry.Stack.automorphismSpaceOverSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 251. The attribute's comment: “the sheaf of automorphisms of x, Z ×_{x, X} I_X”.

Stacks 06PP: the sheaf of automorphisms of x. For an algebraic-space-valued point x : Z ⟶ 𝒳 of an algebraic stack, the 2-fibre product

Isom_𝒳(x, x) = Z ×_{x, 𝒳} ℐ_𝒳

of x with the forgetful 1-morphism of the inertia. This is the object the last paragraph of Stacks 06PP writes Isom_𝒳(x, x): part (1) of that definition when 𝒴 is an algebraic space, in which case the relative inertia of 𝒳 over 𝒴 is the absolute inertia of 𝒳.

noncomputable def automorphismSpaceOverSpace
    (x : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    CatFiberedInGroupoids (BigFppfOver B S hS)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_automorphismSpaceOverSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 276. The attribute's comment: “Isom_X(x, x) is an algebraic space”.

Stacks 06PP: Isom_𝒳(x, x) is an algebraic space. The sheaf of automorphisms of an algebraic-space-valued point of an algebraic stack is represented by an algebraic space over S: Stacks 050Q for the absolute inertia projection, together with Stacks 0300.

theorem isRepresentableByAlgebraicSpace_automorphismSpaceOverSpace
    (x : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    IsRepresentableByAlgebraicSpace B S hS (automorphismSpaceOverSpace B S hS Z hZ x)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_automorphismSpaceOverSpaceProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 289. The attribute's comment: “Isom_X(x, x) is an algebraic space over Z”.

Stacks 06PP: Isom_𝒳(x, x) is an algebraic space over Z. The projection of the sheaf of automorphisms of x to the stack of Z is representable by algebraic spaces — Stacks 0302 for the base change of the representable 1-morphism ℐ_𝒳 ⟶ 𝒳 of Stacks 050Q along x.

theorem isRepresentableByAlgebraicSpaces_automorphismSpaceOverSpaceProj
    (x : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    IsRepresentableByAlgebraicSpaces B S hS
      (automorphismSpaceOverSpaceProj B S hS Z hZ x)

AlgebraicGeometry.Stack.isomorphismSpaceOverSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 331. The attribute's comment: “the sheaf of isomorphisms from x₁ to x₂, as the fibre of the diagonal”.

Stacks 06PP: the sheaf of isomorphisms from x₁ to x₂. For two algebraic-space-valued points x₁, x₂ : Z ⟶ 𝒳 of an algebraic stack, the 2-fibre product

Isom_𝒳(x₁, x₂) = Z ×_{(x₁, x₂), 𝒳 × 𝒳, Δ} 𝒳

of the pair (x₁, x₂) with the diagonal of 𝒳. Its objects over a scheme W are the quadruples of a point z of Z over W, an object a of 𝒳 over W and two vertical isomorphisms x₁(z) ≅ a, x₂(z) ≅ a, so a section over W is an isomorphism x₁(z) ≅ x₂(z) of the fibre of 𝒳 over W — which is what the last paragraph of Stacks 06PP calls the sheaf of isomorphisms from x₁ to x₂.

This is the presentation of Isom that the diagonal conditions (1) and (2) of Stacks 045G are stated with, and it is the one CategoryTheory.TwoFibreProductOver.DiagonalFibre.equivalenceOver identifies with the presheaf of vertical morphisms from x₁ to x₂. The equivalent iterated form the source writes, (Z ×_{x₁, 𝒳, x₂} Z) ×_{Z × Z, Δ_Z} Z, is AlgebraicGeometry.Stack.absoluteIsomorphismCategory cut down by AlgebraicGeometry.Stack.absoluteIsomorphismDiagonalSubcategory; this file does not prove the comparison of the two forms.

noncomputable def isomorphismSpaceOverSpace
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    CatFiberedInGroupoids (BigFppfOver B S hS)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_isomorphismSpaceOverSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 356. The attribute's comment: “Isom_X(x₁, x₂) is an algebraic space”.

Stacks 06PP: Isom_𝒳(x₁, x₂) is an algebraic space. The sheaf of isomorphisms from one algebraic-space-valued point of an algebraic stack to another is represented by an algebraic space over S.

It is the base change of the diagonal of 𝒳 along the pair (x₁, x₂), the diagonal is representable by algebraic spaces because 𝒳 is an algebraic stack, and Z represents the stack of Z; so this is Stacks 0300.

theorem isRepresentableByAlgebraicSpace_isomorphismSpaceOverSpace
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    IsRepresentableByAlgebraicSpace B S hS (isomorphismSpaceOverSpace B S hS Z hZ x₁ x₂)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_isomorphismSpaceOverSpaceProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 367. The attribute's comment: “Isom_X(x₁, x₂) is an algebraic space over Z”.

Stacks 06PP: Isom_𝒳(x₁, x₂) is an algebraic space over Z. Its projection to the stack of Z is representable by algebraic spaces — Stacks 0302 for the base change of the diagonal of 𝒳 along the pair (x₁, x₂).

theorem isRepresentableByAlgebraicSpaces_isomorphismSpaceOverSpaceProj
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    IsRepresentableByAlgebraicSpaces B S hS
      (isomorphismSpaceOverSpaceProj B S hS Z hZ x₁ x₂)

AlgebraicGeometry.Stack.relativeIsomorphismSpaceOverSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 419. The attribute's comment: “part (2): the relative sheaf of isomorphisms, as the fibre of the relative diagonal”.

Stacks 06PP, part (2): the relative sheaf of isomorphisms from x₁ to x₂. For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, two algebraic-space-valued points x₁, x₂ : Z ⟶ 𝒳 and a 2-morphism α : x₁ ≫ f ⟶ x₂ ≫ f, the 2-fibre product

Isom^α_{𝒳/𝒴}(x₁, x₂) = Z ×_{(x₁, x₂, α), 𝒳 ×_𝒴 𝒳, Δ_f} 𝒳

of the twisted point of AlgebraicGeometry.Stack.relativeIsomorphismTwistedPoint with the relative diagonal of f. Its sections over a scheme W are the isomorphisms x₁(z) ≅ x₂(z) of the fibre of 𝒳 over W whose image under f is the component of α at z, which is what the source calls the relative sheaf of isomorphisms from x₁ to x₂.

The source writes the same object as the iterated fibre product (Z ×_{x₁, 𝒳, x₂} Z) ×_{Z ×_{y₁, 𝒴, y₂} Z, Δ^α} Z; that is the fibre of Δ^α and this is the fibre of Δ_f along the twisted point, which is the form the representability of the relative diagonal is stated for. This file does not prove the comparison of the two forms, nor the comparison with the explicit sub-presheaf AlgebraicGeometry.Stack.relativeIsomSpaceOverSpace.

noncomputable def relativeIsomorphismSpaceOverSpace (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    CatFiberedInGroupoids (BigFppfOver B S hS)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_relativeIsomorphismSpaceOverSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 459. The attribute's comment: “part (2): Isom^α_{X/Y}(x₁, x₂) is an algebraic space”.

Stacks 06PP, part (2): Isom^α_{𝒳/𝒴}(x₁, x₂) is an algebraic space. The relative sheaf of isomorphisms from x₁ to x₂ lifting α is represented by an algebraic space over S.

It is the base change of the relative diagonal Δ_f : 𝒳 ⟶ 𝒳 ×_𝒴 𝒳 along the twisted point; the relative diagonal is representable by algebraic spaces as soon as the diagonals of 𝒳 and 𝒴 are (AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_relativeDiagonal), which they are because 𝒳 and 𝒴 are algebraic stacks, and Z represents the stack of Z; so this is Stacks 0300.

theorem isRepresentableByAlgebraicSpace_relativeIsomorphismSpaceOverSpace (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    IsRepresentableByAlgebraicSpace B S hS
      (relativeIsomorphismSpaceOverSpace B S hS Z hZ f x₁ x₂ α)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_relativeIsomorphismSpaceOverSpaceProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AutomorphismSpaceOverAlgebraicSpace.lean, line 471. The attribute's comment: “part (2): Isom^α_{X/Y}(x₁, x₂) is an algebraic space over Z”.

Stacks 06PP, part (2): Isom^α_{𝒳/𝒴}(x₁, x₂) is an algebraic space over Z. Its projection to the stack of Z is representable by algebraic spaces — Stacks 0302 for the base change of the relative diagonal of f along the twisted point.

theorem isRepresentableByAlgebraicSpaces_relativeIsomorphismSpaceOverSpaceProj (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    IsRepresentableByAlgebraicSpaces B S hS
      (relativeIsomorphismSpaceOverSpaceProj B S hS Z hZ f x₁ x₂ α)

AlgebraicGeometry.Stack.isomSpaceOverSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomSpaceOverAlgebraicSpace.lean, line 322. The attribute's comment: “the sheaf of isomorphisms from one algebraic-space-valued point to another”.

Stacks 06PP. The presheaf Isom_𝒳(x₁, x₂) of isomorphisms of two algebraic-space-valued points of an algebraic stack: its sections over W are the pairs consisting of a point z of Z over W and an isomorphism x₁(z) ≅ x₂(z) in the fibre category of 𝒳 over W, and its restriction maps are AlgebraicGeometry.Stack.pointRestrict.

This is the object the last paragraph of Stacks 06PP calls Isom_𝒳(x₁, x₂), the sheaf of isomorphisms from x₁ to x₂. That it is represented by an algebraic space over Z is the other half of that definition and is not asserted here; neither is its part (1), the group law on the relative sheaf of automorphisms.

noncomputable def isomSpaceOverSpace (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    (BigFppfOver B S hS)ᵒᵖ ⥤ Type u

AlgebraicGeometry.Stack.relativeIsomSpaceOverSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomSpaceOverAlgebraicSpace.lean, line 530. The attribute's comment: “part (2): the sheaf of isomorphisms lifting a 2-morphism”.

Stacks 06PP, part (2). The presheaf Isom^α_{𝒳/𝒴}(x₁, x₂) of isomorphisms of two algebraic-space-valued points of 𝒳 lifting a given 2-morphism α : x₁ ≫ f ⟶ x₂ ≫ f of the target: it is the sub-presheaf of AlgebraicGeometry.Stack.isomSpaceOverSpace cut out by the condition that the image of the isomorphism under f be the prescribed component of α.

That it is represented by an algebraic space over Z is the remaining half of Stacks 06PP part (2) and is not asserted here.

noncomputable def relativeIsomSpaceOverSpace (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    (BigFppfOver B S hS)ᵒᵖ ⥤ Type u

AlgebraicGeometry.Stack.isAlgebraicSpace_isomSpaceOverSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomSpaceOverAlgebraicSpaceRepresentability.lean, line 542. The attribute's comment: “the sheaf of isomorphisms is an algebraic space over Z”.

Stacks 06PP: the sheaf of isomorphisms of two algebraic-space-valued points of an algebraic stack is an algebraic space over Z. The structure morphism AlgebraicGeometry.Stack.isomSpaceOverSpaceProj to Z is representable by algebraic spaces, because its fibre over every scheme-valued point of Z is the sheaf of vertical morphisms between two scheme-valued points of 𝒳, an algebraic space by condition (2) of Stacks 045G; Z is an algebraic space, so Stacks 02YS applies.

This is the representability half of Stacks 06PP, which AlgebraicGeometry.Stack.isomSpaceOverSpace constructs the sheaf of.

theorem isAlgebraicSpace_isomSpaceOverSpace
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    IsAlgebraicSpace B S hS (isomSpaceOverSpace B S hS Z hZ x₁ x₂)

AlgebraicGeometry.Stack.isAlgebraicSpace_relativeIsomSpaceOverSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomSpaceOverAlgebraicSpaceRepresentability.lean, line 557. The attribute's comment: “part (2): the sheaf of isomorphisms lifting a 2-morphism is an algebraic space”.

Stacks 06PP part (2): the sheaf of isomorphisms lifting a 2-morphism is an algebraic space over Z. It is the fibre product of Isom_𝒳(x₁, x₂) and Z over Isom_𝒴(f x₁, f x₂) by AlgebraicGeometry.Stack.isPullback_relativeIsomSpaceOverSpace, and all three of those are algebraic spaces over S, so Stacks 04T9 applies.

theorem isAlgebraicSpace_relativeIsomSpaceOverSpace (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    IsAlgebraicSpace B S hS (relativeIsomSpaceOverSpace B S hS Z hZ f x₁ x₂ α)

AlgebraicGeometry.Stack.nonempty_equivalenceOver_isomorphismSpaceOverSpaceProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomSpaceRenderingComparison.lean, line 126. The attribute's comment: “the sheaf of isomorphisms from x₁ to x₂: the 2-fibre product is that sheaf”.

Stacks 06PP: Isom_𝒳(x₁, x₂) is the sheaf of isomorphisms from x₁ to x₂. The 2-fibre product Z ×_{(x₁, x₂), 𝒳 × 𝒳, Δ} 𝒳 of AlgebraicGeometry.Stack.isomorphismSpaceOverSpace is equivalent, as a category over Z, to the category of elements of the presheaf on the category of elements of Z whose sections over a point a are the vertical morphisms x₁(a) ⟶ x₂(a) of 𝒳. Those are exactly the isomorphisms x₁(a) ≅ x₂(a) of the fibre of 𝒳, the fibres of an algebraic stack being groupoids (Stacks 003V), so this is the statement that the 2-fibre product the last paragraph of Stacks 06PP writes Isom_𝒳(x₁, x₂) is the sheaf of isomorphisms from x₁ to x₂.

This is CategoryTheory.TwoFibreProductOver.DiagonalFibre.equivalenceOver read at the pair (x₁, x₂) = AlgebraicGeometry.Stack.isomorphismPairPoint.

theorem nonempty_equivalenceOver_isomorphismSpaceOverSpaceProj
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    Nonempty (StacksRepresentableCFG.EquivalenceOver
      (isomorphismSpaceOverSpaceProj B S hS Z hZ x₁ x₂).toFunctor
      (PresheafOfCategories.discreteProjection
        (TwoFibreProductOver.DiagonalFibre.vertHomPresheaf 𝒳.val.isFiberedInGroupoids
          (isomorphismPairPoint B S hS Z hZ x₁ x₂).hom.w)))

AlgebraicGeometry.Stack.nonempty_equivalenceOver_relativeIsomorphismSpaceOverSpaceProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomSpaceRenderingComparison.lean, line 148. The attribute's comment: “part (2): the 2-fibre product is the sheaf of isomorphisms lifting α”.

Stacks 06PP, part (2): Isom^α_{𝒳/𝒴}(x₁, x₂) is the sheaf of isomorphisms lifting α. The 2-fibre product Z ×_{(x₁, x₂, α), 𝒳 ×_𝒴 𝒳, Δ_f} 𝒳 of AlgebraicGeometry.Stack.relativeIsomorphismSpaceOverSpace is equivalent, as a category over Z, to the category of elements of the presheaf on the category of elements of Z whose sections over a point a are the vertical morphisms x₁(a) ⟶ x₂(a) of 𝒳 whose image under f is the comparison isomorphism carried by the twisted point at a, that is the component α_a. So the object part (2) defines is the relative sheaf of isomorphisms from x₁ to x₂ that the source says it is.

This is CategoryTheory.TwoFibreProductOver.RelativeDiagonalFibre.equivalenceOver — Stacks 04XT — read at the twisted point AlgebraicGeometry.Stack.relativeIsomorphismTwistedPoint.

theorem nonempty_equivalenceOver_relativeIsomorphismSpaceOverSpaceProj (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    Nonempty (StacksRepresentableCFG.EquivalenceOver
      (relativeIsomorphismSpaceOverSpaceProj B S hS Z hZ f x₁ x₂ α).toFunctor
      (PresheafOfCategories.discreteProjection
        (TwoFibreProductOver.RelativeDiagonalFibre.relVertHomPresheaf
          𝒴.val.isFiberedInGroupoids 𝒳.val.isFiberedInGroupoids
          (relativeIsomorphismTwistedPoint B S hS Z hZ f x₁ x₂ α).w f.hom.hom.w)))

AlgebraicGeometry.Stack.isAlgebraicSpace_isomorphismTotalPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomTotalPresheafAlgebraic.lean, line 101. The attribute's comment: “Isom_X(x₁, x₂) as a presheaf over Z on the big fppf site is an algebraic space”.

Stacks 06PP: the sheaf Isom_𝒳(x₁, x₂) on the big fppf site is an algebraic space over Z. The presheaf whose sections over W are the pairs of a point z of Z over W and an isomorphism x₁(z) ≅ x₂(z) is an algebraic space over S, so together with its structure morphism to Z it is the algebraic space over Z that the last paragraph of Stacks 06PP asserts.

theorem isAlgebraicSpace_isomorphismTotalPresheaf
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    IsAlgebraicSpace B S hS (isomorphismTotalPresheaf B S hS Z hZ x₁ x₂)

AlgebraicGeometry.Stack.isAlgebraicSpace_relativeIsomorphismTotalPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomTotalPresheafAlgebraic.lean, line 137. The attribute's comment: “part (2): Isom^α_{X/Y}(x₁, x₂) as a presheaf over Z on the big fppf site is an algebraic space”.

Stacks 06PP, part (2): the sheaf Isom^α_{𝒳/𝒴}(x₁, x₂) on the big fppf site is an algebraic space over Z. The presheaf whose sections over W are the pairs of a point z of Z over W and an isomorphism x₁(z) ≅ x₂(z) lifting the component α_z is an algebraic space over S, so together with its structure morphism to Z it is the algebraic space over Z that part (2) asserts.

theorem isAlgebraicSpace_relativeIsomorphismTotalPresheaf (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    IsAlgebraicSpace B S hS (relativeIsomorphismTotalPresheaf B S hS Z hZ f x₁ x₂ α)

AlgebraicGeometry.Stack.relativeAutomorphismGroupAlgebraicSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismGroupAlgebraicSpace.lean, line 85. The attribute's comment: “part (1): Isom_{X/Y}(x, x) is a group algebraic space over Z, group law and algebraicity”.

Isom_{𝒳/𝒴}(x, x) as a group algebraic space over Z: the presheaf on the big fppf site whose sections over W are the pairs of a point z of Z over W and an automorphism of x(z) killed by f, together with its structure morphism to Z, the group law given by composition of automorphisms, and the algebraicity of that presheaf.

noncomputable def relativeAutomorphismGroupAlgebraicSpace (f : 𝒳 ⟶ 𝒴)
    (x : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    Space.GroupAlgebraicSpace B S hS Z hZ

AlgebraicGeometry.Stack.relativeAutomorphismGroupPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismGroupOverSpace.lean, line 247. The attribute's comment: “part (1): the group law on Isom_{X/Y}(x, x), as a presheaf of groups over Z”.

The presheaf of groups on the category of elements of Z whose sections at a point a of Z are the vertical automorphisms of x(a) killed by f, with composition as the group law and restriction along a morphism of Z as the restriction map.

noncomputable def relativeAutomorphismGroupPresheaf :
    ((algebraicSpaceStack.{u, w} B S hS Z hZ).val.val.obj)ᵒᵖ ⥤ GrpCat.{u}

AlgebraicGeometry.Stack.relativeAutomorphismPresheafGrpObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismGroupOverSpace.lean, line 294. The attribute's comment: “part (1): the group-object structure on Isom_{X/Y}(x, x) over Z”.

The presheaf of relative automorphisms of x, read over the category of elements of Z, is a group object of the cartesian monoidal category of presheaves of sets on that category: its unit, multiplication and inverse are the identity automorphism, composition and the inverse automorphism, taken pointwise over the points of Z.

noncomputable def relativeAutomorphismPresheafGrpObj :
    GrpObj (relativeAutomorphismPresheaf B S hS Z hZ f x)

AlgebraicGeometry.Stack.relativeAutomorphismPresheafGrpObj_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismGroupOverSpace.lean, line 320. The attribute's comment: “part (1): the multiplication of the group object is composition”.

The multiplication of AlgebraicGeometry.Stack.relativeAutomorphismPresheafGrpObj is composition of relative automorphisms.

theorem relativeAutomorphismPresheafGrpObj_mul
    (a : ((algebraicSpaceStack.{u, w} B S hS Z hZ).val.val.obj)ᵒᵖ)
    (φ : (CategoryTheory.MonoidalCategoryStruct.tensorObj
      (relativeAutomorphismPresheaf B S hS Z hZ f x)
      (relativeAutomorphismPresheaf B S hS Z hZ f x)).obj a) :
    letI := relativeAutomorphismPresheafGrpObj B S hS Z hZ f x
    (MonObj.mul (X := relativeAutomorphismPresheaf B S hS Z hZ f x)).app a φ =
      (φ.1 * φ.2 : RelativeAutomorphism B S hS Z hZ f x a.unop)

AlgebraicGeometry.Stack.relativeAutomorphismPresheafGrpObj_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismGroupOverSpace.lean, line 332. The attribute's comment: “part (1): the unit of the group object is the identity automorphism”.

The unit of AlgebraicGeometry.Stack.relativeAutomorphismPresheafGrpObj is the identity automorphism.

theorem relativeAutomorphismPresheafGrpObj_one
    (a : ((algebraicSpaceStack.{u, w} B S hS Z hZ).val.val.obj)ᵒᵖ)
    (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit
      (((algebraicSpaceStack.{u, w} B S hS Z hZ).val.val.obj)ᵒᵖ ⥤ Type u)).obj a) :
    letI := relativeAutomorphismPresheafGrpObj B S hS Z hZ f x
    (MonObj.one (X := relativeAutomorphismPresheaf B S hS Z hZ f x)).app a t =
      (1 : RelativeAutomorphism B S hS Z hZ f x a.unop)

AlgebraicGeometry.Stack.relativeAutomorphismPresheafGrpObj_inv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismGroupOverSpace.lean, line 343. The attribute's comment: “part (1): the inverse of the group object is the inverse automorphism”.

The inverse of AlgebraicGeometry.Stack.relativeAutomorphismPresheafGrpObj is the inverse automorphism.

theorem relativeAutomorphismPresheafGrpObj_inv
    (a : ((algebraicSpaceStack.{u, w} B S hS Z hZ).val.val.obj)ᵒᵖ)
    (φ : RelativeAutomorphism B S hS Z hZ f x a.unop) :
    (GrpObj.inv (X := relativeAutomorphismPresheaf B S hS Z hZ f x)
      (self := relativeAutomorphismPresheafGrpObj B S hS Z hZ f x)).app a φ = φ⁻¹

AlgebraicGeometry.Stack.RelativeAutomorphismSpace.nonempty_isEquivalenceOver_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSpaceGroupLaw.lean, line 380. The attribute's comment: “part (1): the group structure on Isom_{X/Y}(x, x) over Z”.

The group structure on Isom_{𝒳/𝒴}(x, x) over Z. The comparison 1-morphism is an equivalence over Z from the category of elements of the presheaf of groups of relative automorphisms of x (AlgebraicGeometry.Stack.relativeAutomorphismGroupPresheaf) to Isom_{𝒳/𝒴}(x, x) = Z ×_{x, 𝒳} ℐ_{𝒳/𝒴}.

theorem nonempty_isEquivalenceOver_comparison :
    Nonempty (CategoryTheory.IsEquivalenceOver
      (PresheafOfCategories.discreteProjection (relativeAutomorphismPresheaf B S hS Z hZ f x))
      (relativeAutomorphismSpaceOverSpaceProj B S hS Z hZ f x).toFunctor
      (comparison B S hS Z hZ f x))

AlgebraicGeometry.Stack.RelativeAutomorphismSpace.nonempty_equivalenceOver_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSpaceGroupLaw.lean, line 395. The attribute's comment: “part (1): Isom_{X/Y}(x, x) is the presheaf of groups of relative automorphisms”.

Isom_{𝒳/𝒴}(x, x) is the presheaf of relative automorphisms, as a category over Z: there is a StacksRepresentableCFG.EquivalenceOver from the projection of the category of elements of the presheaf of relative automorphisms of x to the projection Isom_{𝒳/𝒴}(x, x) ⟶ Z.

theorem nonempty_equivalenceOver_comparison :
    Nonempty (StacksRepresentableCFG.EquivalenceOver
      (PresheafOfCategories.discreteProjection (relativeAutomorphismPresheaf B S hS Z hZ f x))
      (relativeAutomorphismSpaceOverSpaceProj B S hS Z hZ f x).toFunctor)

AlgebraicGeometry.Stack.RelativeAutomorphismSpace.inertiaObj_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSpaceGroupLaw.lean, line 429. The attribute's comment: “part (1): the group law is the composition law of 050R pulled back along x”.

The multiplication of relative automorphisms is the composition law of the relative inertia. The object of the relative inertia attached to the product φ * ψ of two relative automorphisms of x at a point of Z is the value at the corresponding object of ℐ_{𝒳/𝒴} ×_𝒳 ℐ_{𝒳/𝒴} of CategoryTheory.RelativeInertia.composition, the composition law ((x, α), (x', α'), β) ↦ (x, α ∘ β⁻¹ ∘ α' ∘ β).

theorem inertiaObj_mul {a : (algebraicSpaceStack.{u, w} B S hS Z hZ).val.val.obj}
    (φ ψ : RelativeAutomorphism B S hS Z hZ f x a) :
    inertiaObj B S hS Z hZ f x (φ * ψ) =
      (CategoryTheory.RelativeInertia.composition f.hom.hom.toFunctor 𝒳.val.val.p).obj
        (inertiaPair B S hS Z hZ f x φ ψ)

AlgebraicGeometry.Stack.RelativeAutomorphismSpace.inertiaObj_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSpaceGroupLaw.lean, line 444. The attribute's comment: “part (1): the unit is the neutral element of 050R pulled back along x”.

The unit of the group of relative automorphisms is the neutral section of the relative inertia. The object of the relative inertia attached to the identity relative automorphism of x at a point a of Z is the value of CategoryTheory.RelativeInertia.neutralSection, x ↦ (x, id_x), at x(a).

theorem inertiaObj_one {a : (algebraicSpaceStack.{u, w} B S hS Z hZ).val.val.obj} :
    inertiaObj B S hS Z hZ f x (1 : RelativeAutomorphism B S hS Z hZ f x a) =
      (CategoryTheory.RelativeInertia.neutralSection f.hom.hom.toFunctor).obj
        (x.hom.hom.toFunctor.obj a)

AlgebraicGeometry.Stack.RelativeAutomorphismSpace.inertiaObj_inv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismSpaceGroupLaw.lean, line 457. The attribute's comment: “part (1): the inverse is the inverse of 050R pulled back along x”.

The inverse of the group of relative automorphisms is the inverse of the relative inertia. The object of the relative inertia attached to φ⁻¹ is the value at the object attached to φ of CategoryTheory.RelativeInertia.inverse, (x, α) ↦ (x, α⁻¹).

theorem inertiaObj_inv {a : (algebraicSpaceStack.{u, w} B S hS Z hZ).val.val.obj}
    (φ : RelativeAutomorphism B S hS Z hZ f x a) :
    inertiaObj B S hS Z hZ f x φ⁻¹ =
      (CategoryTheory.RelativeInertia.inverse f.hom.hom.toFunctor).obj
        (inertiaObj B S hS Z hZ f x φ)

AlgebraicGeometry.Stack.isAlgebraicSpace_relativeAutomorphismTotalPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeAutomorphismTotalPresheaf.lean, line 112. The attribute's comment: “part (1): Isom_{X/Y}(x, x) as a presheaf over Z on the big fppf site is an algebraic space”.

The presheaf AlgebraicGeometry.Stack.relativeAutomorphismTotalPresheaf, whose sections over W are the pairs of a point z of Z over W and an automorphism of x(z) killed by f, is an algebraic space over S.

theorem isAlgebraicSpace_relativeAutomorphismTotalPresheaf (f : 𝒳 ⟶ 𝒴)
    (x : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    IsAlgebraicSpace B S hS (relativeAutomorphismTotalPresheaf B S hS Z hZ f x)

AlgebraicGeometry.Stack.exists_relativeIsomorphismDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomorphismDiagram.lean, line 255. The attribute's comment: “part (2): functorial map and twisted diagonal”.

For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, two algebraic-space-valued points x₁, x₂ : Z ⟶ 𝒳 and a 2-morphism α : x₁ ≫ f ⟶ x₂ ≫ f of the target, there are a 1-morphism H from the isomorphism category of x₁, x₂ to that of x₁ ≫ f, x₂ ≫ f which keeps the two points of Z and applies f to the isomorphism between them, and a 1-morphism Δ from Z to the latter whose value at z is the pair (z, z) with comparison isomorphism α_z.

The 2-fibre product of H along Δ is the category of isomorphisms x₁ ≅ x₂ lifting α; that it is represented by an algebraic space over Z is the remaining half of part (2) and is not asserted here. The witnesses are AlgebraicGeometry.Stack.absoluteIsomorphismImageBasedFunctor and AlgebraicGeometry.Stack.relativeIsomorphismTwistedDiagonalBasedFunctor.

theorem exists_relativeIsomorphismDiagram
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    let PX := absoluteIsomorphismCategory B S hS Z hZ 𝒳 x₁ x₂
    let PY := absoluteIsomorphismCategory B S hS Z hZ 𝒴 (x₁ ≫ f) (x₂ ≫ f)
    ∃ (H : PX.val ⥤ᵇ PY.val)
      (Δ : (algebraicSpaceStack.{u, w} B S hS Z hZ).val.val ⥤ᵇ PY.val),
      (∀ A : PX.val.obj,
        HEq (H.toFunctor.obj A).x A.x ∧
        HEq (H.toFunctor.obj A).y A.y ∧
        HEq (H.toFunctor.obj A).iso.hom
          (f.hom.hom.toFunctor.map A.iso.hom)) ∧
      (∀ A : (algebraicSpaceStack.{u, w} B S hS Z hZ).val.val.obj,
        HEq (Δ.toFunctor.obj A).x A ∧
        HEq (Δ.toFunctor.obj A).y A ∧
        HEq (Δ.toFunctor.obj A).iso.hom
          (α.hom.hom.toNatTrans.app A))

AlgebraicGeometry.Stack.relativeIsomorphismIteratedSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomSpaceIteratedForm.lean, line 162. The attribute's comment: “part (2): Isom^α_{X/Y}(x₁, x₂) as the iterated fibre product of the source”.

Stacks 06PP, part (2): the relative sheaf of isomorphisms from x₁ to x₂ lifting α, in the iterated form the source writes it in. The 2-fibre product

Isom^α_{𝒳/𝒴}(x₁, x₂) = (Z ×_{x₁, 𝒳, x₂} Z) ×_{Z ×_{y₁, 𝒴, y₂} Z, Δ^α} Z

of the map H on absolute isomorphism categories induced by f along the twisted diagonal Δ^α determined by α. Its objects over a scheme W are the isomorphisms x₁(z) ≅ x₂(z) of the fibre of 𝒳 over W whose image under f is the component of α at z.

noncomputable def relativeIsomorphismIteratedSpace (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    CatFiberedInGroupoids (BigFppfOver B S hS)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_relativeIsomorphismIteratedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomSpaceIteratedForm.lean, line 195. The attribute's comment: “part (2): the iterated form of Isom^α_{X/Y}(x₁, x₂) is an algebraic space”.

Stacks 06PP, part (2): the iterated form of Isom^α_{𝒳/𝒴}(x₁, x₂) is an algebraic space. It is the base change of the twisted diagonal Δ^α along H; Δ^α is representable by algebraic spaces and Z ×_{x₁, 𝒳, x₂} Z is represented by an algebraic space, so this is Stacks 0300.

theorem isRepresentableByAlgebraicSpace_relativeIsomorphismIteratedSpace (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    IsRepresentableByAlgebraicSpace B S hS
      (relativeIsomorphismIteratedSpace B S hS Z hZ f x₁ x₂ α)

AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_relativeIsomorphismIteratedSpaceProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomSpaceIteratedForm.lean, line 215. The attribute's comment: “part (2): the iterated form of Isom^α_{X/Y}(x₁, x₂) is an algebraic space over Z”.

Stacks 06PP, part (2): the iterated form of Isom^α_{𝒳/𝒴}(x₁, x₂) is an algebraic space over Z. Its structure 1-morphism to the stack of Z has an algebraic space as source and the stack of Z as target, so it is representable by algebraic spaces by Stacks 02ZZ; together with AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpace_relativeIsomorphismIteratedSpace it is therefore a morphism of algebraic spaces with target Z.

theorem isRepresentableByAlgebraicSpaces_relativeIsomorphismIteratedSpaceProj (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    IsRepresentableByAlgebraicSpaces B S hS
      (relativeIsomorphismIteratedSpaceProj B S hS Z hZ f x₁ x₂ α)

Tag 0CPK, a lemma

Tag 0CPK in the Stacks Project.

AlgebraicGeometry.Stack.isomSpaceOverSpaceMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomSpaceOverAlgebraicSpace.lean, line 394. The attribute's comment: “part (3): the map on isomorphism sheaves”.

Stacks 0CPK, part (3): the map on isomorphism sheaves. A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks carries Isom_𝒳(x₁, x₂) into Isom_𝒴(x₁ ≫ f, x₂ ≫ f): it keeps the point of Z and applies f to the isomorphism of the fibre.

The source calls this a map of algebraic spaces; that the source and target are algebraic spaces over Z is asserted by Stacks 06PP and is not proved here, so this is the map of the underlying sheaves.

noncomputable def isomSpaceOverSpaceMap (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    isomSpaceOverSpace B S hS Z hZ x₁ x₂ ⟶
      isomSpaceOverSpace B S hS Z hZ (x₁ ≫ f) (x₂ ≫ f)

AlgebraicGeometry.Stack.isPullback_relativeIsomSpaceOverSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/IsomSpaceOverAlgebraicSpace.lean, line 592. The attribute's comment: “part (3): the cartesian square”.

Stacks 0CPK, part (3): the cartesian square. The isomorphisms of x₁ and x₂ lifting the 2-morphism α : x₁ ≫ f ⟶ x₂ ≫ f are the fibre product of Isom_𝒳(x₁, x₂) and Z over Isom_𝒴(x₁ ≫ f, x₂ ≫ f), along the map induced by f and the section determined by α.

The square is cartesian pointwise and for an elementary reason: a section of Isom_𝒳(x₁, x₂) over W together with a point of Z over W having the same image in Isom_𝒴(x₁ ≫ f, x₂ ≫ f) is the same thing as a section of Isom_𝒳(x₁, x₂) whose image under f is the component of α, because the two images have the same point of Z as their first component.

The square is the one Stacks 0CPK part (3) draws, as a square of sheaves on the big fppf site of S; that its four corners are algebraic spaces is asserted by Stacks 06PP and is not proved here. Together with AlgebraicGeometry.Stack.relativeIsomSpaceOverSpace it also identifies the explicit sub-presheaf with the fibre product of Stacks 06PP part (2).

theorem isPullback_relativeIsomSpaceOverSpace (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) (α : x₁ ≫ f ⟶ x₂ ≫ f) :
    IsPullback (relativeIsomSpaceOverSpaceι B S hS Z hZ f x₁ x₂ α)
      (relativeIsomSpaceOverSpaceProj B S hS Z hZ f x₁ x₂ α)
      (isomSpaceOverSpaceMap B S hS Z hZ f x₁ x₂)
      (twistedSection B S hS Z hZ f x₁ x₂ α)

AlgebraicGeometry.Stack.relativeAutSpaceSliceGrpObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 492. The attribute's comment: “part (1): the relative automorphism sheaf is a group over Z”.

The group structure over Z on the sheaf Isom_{𝒳/𝒴}(x, x) of automorphisms of an algebraic-space-valued point x of 𝒳 whose image under f is the identity: the law is composition of automorphisms, the unit is the identity and the inverse is the inverse automorphism.

noncomputable def relativeAutSpaceSliceGrpObj :
    GrpObj (relativeAutSpaceSlice B S hS Z hZ f x)

AlgebraicGeometry.Stack.relativeAutGroupAlgebraicSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 521. The attribute's comment: “part (1): the relative automorphisms are a group algebraic space over Z”.

The relative automorphism sheaf Isom_{𝒳/𝒴}(x, x) as a group algebraic space over Z, with the group structure AlgebraicGeometry.Stack.relativeAutSpaceSliceGrpObj.

noncomputable def relativeAutGroupAlgebraicSpace :
    Space.GroupAlgebraicSpace B S hS Z hZ

AlgebraicGeometry.Stack.relativeIsomSpaceSliceModObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 608. The attribute's comment: “part (4): the action by postcomposition”.

The action of Isom_{𝒳/𝒴}(x₂, x₂) on Isom^α_{𝒳/𝒴}(x₁, x₂) over Z, by postcomposition.

noncomputable def relativeIsomSpaceSliceModObj :
    letI : GrpObj (relativeAutSpaceSlice B S hS Z hZ f x₂) :=
      relativeAutSpaceSliceGrpObj B S hS Z hZ f x₂
    ModObj (relativeAutSpaceSlice B S hS Z hZ f x₂)
      (relativeIsomSpaceSlice B S hS Z hZ f x₁ x₂ α)

AlgebraicGeometry.Stack.isPseudoTorsor_relativeIsomSpaceSlice, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 679. The attribute's comment: “part (4): the relative isomorphisms are a pseudo-torsor”.

The isomorphisms lifting α are a pseudo-torsor under the relative automorphisms of the target point, over Z: Isom^α_{𝒳/𝒴}(x₁, x₂) is a pseudo-torsor under Isom_{𝒳/𝒴}(x₂, x₂).

theorem isPseudoTorsor_relativeIsomSpaceSlice :
    letI : GrpObj (relativeAutSpaceSlice B S hS Z hZ f x₂) :=
      relativeAutSpaceSliceGrpObj B S hS Z hZ f x₂
    letI : ModObj (relativeAutSpaceSlice B S hS Z hZ f x₂)
        (relativeIsomSpaceSlice B S hS Z hZ f x₁ x₂ α) :=
      relativeIsomSpaceSliceModObj B S hS Z hZ f x₁ x₂ α
    IsPseudoTorsor (relativeAutSpaceSlice B S hS Z hZ f x₂)
      (relativeIsomSpaceSlice B S hS Z hZ f x₁ x₂ α)

AlgebraicGeometry.Stack.isAlgebraicSpace_isPseudoTorsor_relativeIsomSpaceSlice, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 707. The attribute's comment: “part (4): the relative isomorphisms are an algebraic space and a pseudo-torsor”.

For every 2-morphism α : x₁ ≫ f ⟶ x₂ ≫ f the sheaf Isom^α_{𝒳/𝒴}(x₁, x₂) and the relative automorphism sheaf Isom_{𝒳/𝒴}(x₂, x₂) are algebraic spaces over Z, and the first is a pseudo-torsor under the second over Z.

theorem isAlgebraicSpace_isPseudoTorsor_relativeIsomSpaceSlice :
    letI : GrpObj (relativeAutSpaceSlice B S hS Z hZ f x₂) :=
      relativeAutSpaceSliceGrpObj B S hS Z hZ f x₂
    letI : ModObj (relativeAutSpaceSlice B S hS Z hZ f x₂)
        (relativeIsomSpaceSlice B S hS Z hZ f x₁ x₂ α) :=
      relativeIsomSpaceSliceModObj B S hS Z hZ f x₁ x₂ α
    IsAlgebraicSpace B S hS (relativeIsomSpaceOverSpace B S hS Z hZ f x₁ x₂ α) ∧
      IsAlgebraicSpace B S hS (relativeIsomSpaceOverSpace B S hS Z hZ f x₂ x₂ (𝟙 (x₂ ≫ f))) ∧
      IsPseudoTorsor (relativeAutSpaceSlice B S hS Z hZ f x₂)
        (relativeIsomSpaceSlice B S hS Z hZ f x₁ x₂ α)

AlgebraicGeometry.Stack.isAlgebraicSpace_isPullback_relativeIsomSpaceOverSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 725. The attribute's comment: “part (3): the cartesian square of algebraic spaces over Z”.

The sheaves Isom_𝒳(x₁, x₂), Isom_𝒴(f x₁, f x₂) and Isom^α_{𝒳/𝒴}(x₁, x₂) are algebraic spaces over Z, and the square cutting out Isom^α_{𝒳/𝒴}(x₁, x₂) along AlgebraicGeometry.Stack.isomSpaceOverSpaceMap is cartesian.

theorem isAlgebraicSpace_isPullback_relativeIsomSpaceOverSpace :
    IsAlgebraicSpace B S hS (isomSpaceOverSpace B S hS Z hZ x₁ x₂) ∧
      IsAlgebraicSpace B S hS (isomSpaceOverSpace B S hS Z hZ (x₁ ≫ f) (x₂ ≫ f)) ∧
      IsAlgebraicSpace B S hS (relativeIsomSpaceOverSpace B S hS Z hZ f x₁ x₂ α) ∧
      IsPullback (relativeIsomSpaceOverSpaceι B S hS Z hZ f x₁ x₂ α)
        (relativeIsomSpaceOverSpaceProj B S hS Z hZ f x₁ x₂ α)
        (isomSpaceOverSpaceMap B S hS Z hZ f x₁ x₂)
        (twistedSection B S hS Z hZ f x₁ x₂ α)

AlgebraicGeometry.Stack.isMonHom_relativeAutSpaceSliceι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 909. The attribute's comment: “part (2): the first map is a homomorphism of groups over Z”.

The inclusion Isom_{𝒳/𝒴}(x, x) ⟶ Isom_𝒳(x, x) is a homomorphism of groups over Z.

theorem isMonHom_relativeAutSpaceSliceι :
    letI : GrpObj (relativeAutSpaceSlice B S hS Z hZ f x) :=
      relativeAutSpaceSliceGrpObj B S hS Z hZ f x
    letI : GrpObj (isomSpaceSlice B S hS Z hZ x x) := isomSpaceSliceGrpObj B S hS Z hZ x
    IsMonHom (relativeAutSpaceSliceι B S hS Z hZ x f)

AlgebraicGeometry.Stack.isMonHom_isomSpaceSliceMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 935. The attribute's comment: “part (2): the second map is a homomorphism of groups over Z”.

The map Isom_𝒳(x, x) ⟶ Isom_𝒴(f x, f x) induced by f is a homomorphism of groups over Z.

theorem isMonHom_isomSpaceSliceMap :
    letI : GrpObj (isomSpaceSlice B S hS Z hZ x x) := isomSpaceSliceGrpObj B S hS Z hZ x
    letI : GrpObj (isomSpaceSlice B S hS Z hZ (x ≫ f) (x ≫ f)) :=
      isomSpaceSliceGrpObj B S hS Z hZ (x ≫ f)
    IsMonHom (isomSpaceSliceMap B S hS Z hZ x f)

AlgebraicGeometry.Stack.relativeAutSpaceSliceι_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 961. The attribute's comment: “part (2): injectivity of the first map”.

The inclusion Isom_{𝒳/𝒴}(x, x) ⟶ Isom_𝒳(x, x) is a monomorphism.

theorem relativeAutSpaceSliceι_injective (Q : Over Z)
    (g h : Q ⟶ relativeAutSpaceSlice B S hS Z hZ f x)
    (hgh : g ≫ relativeAutSpaceSliceι B S hS Z hZ x f =
      h ≫ relativeAutSpaceSliceι B S hS Z hZ x f) : g = h

AlgebraicGeometry.Stack.relativeAutSpaceSlice_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 973. The attribute's comment: “part (2): exactness at Isom_𝒳(x, x)”.

The sequence 0 ⟶ Isom_{𝒳/𝒴}(x, x) ⟶ Isom_𝒳(x, x) ⟶ Isom_𝒴(f x, f x) of groups over Z is exact at the middle term: a point of Isom_𝒳(x, x) is killed by the second map exactly when it comes from a relative automorphism.

theorem relativeAutSpaceSlice_exact (Q : Over Z) (p : Q ⟶ isomSpaceSlice B S hS Z hZ x x) :
    letI : GrpObj (isomSpaceSlice B S hS Z hZ (x ≫ f) (x ≫ f)) :=
      isomSpaceSliceGrpObj B S hS Z hZ (x ≫ f)
    p ≫ isomSpaceSliceMap B S hS Z hZ x f = 1 ↔
      ∃ g : Q ⟶ relativeAutSpaceSlice B S hS Z hZ f x,
        g ≫ relativeAutSpaceSliceι B S hS Z hZ x f = p

AlgebraicGeometry.Stack.relativeIsomSpaceSlice_properties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeIsomGroupOverAlgebraicSpace.lean, line 1019. The attribute's comment: “the whole statement: parts (1), (2), (3) and (4)”.

For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks, an algebraic space Z and two points x₁, x₂ : Z ⟶ 𝒳, the isomorphism sheaves attached to these data, read in the slice over Z, satisfy:

• the relative automorphism sheaf Isom_{𝒳/𝒴}(x₂, x₂) is an algebraic space over Z and carries a group structure over Z, i.e. is a group algebraic space over Z;
• the sequence 0 ⟶ Isom_{𝒳/𝒴}(x₂, x₂) ⟶ Isom_𝒳(x₂, x₂) ⟶ Isom_𝒴(f x₂, f x₂) is a sequence of homomorphisms of groups over Z, injective at the first map and exact at the middle term;
• the two isomorphism sheaves are algebraic spaces over Z and there is a map Isom_𝒳(x₁, x₂) ⟶ Isom_𝒴(f x₁, f x₂) for which the square cutting out Isom^α_{𝒳/𝒴}(x₁, x₂) is cartesian for every 2-morphism α : x₁ ≫ f ⟶ x₂ ≫ f;
• that sheaf is an algebraic space over Z and a pseudo-torsor under Isom_{𝒳/𝒴}(x₂, x₂) over Z for every such α.

theorem relativeIsomSpaceSlice_properties (f : 𝒳 ⟶ 𝒴)
    (x₁ x₂ : algebraicSpaceStack.{u, w} B S hS Z hZ ⟶ 𝒳) :
    letI : GrpObj (relativeAutSpaceSlice B S hS Z hZ f x₂) :=
      relativeAutSpaceSliceGrpObj B S hS Z hZ f x₂
    letI : GrpObj (isomSpaceSlice B S hS Z hZ x₂ x₂) := isomSpaceSliceGrpObj B S hS Z hZ x₂
    letI : GrpObj (isomSpaceSlice B S hS Z hZ (x₂ ≫ f) (x₂ ≫ f)) :=
      isomSpaceSliceGrpObj B S hS Z hZ (x₂ ≫ f)
    IsAlgebraicSpace B S hS (relativeIsomSpaceOverSpace B S hS Z hZ f x₂ x₂ (𝟙 (x₂ ≫ f))) ∧
      Nonempty (GrpObj (relativeAutSpaceSlice B S hS Z hZ f x₂)) ∧
      IsMonHom (relativeAutSpaceSliceι B S hS Z hZ x₂ f) ∧
      IsMonHom (isomSpaceSliceMap B S hS Z hZ x₂ f) ∧
      (∀ (Q : Over Z) (g h : Q ⟶ relativeAutSpaceSlice B S hS Z hZ f x₂),
        g ≫ relativeAutSpaceSliceι B S hS Z hZ x₂ f =
          h ≫ relativeAutSpaceSliceι B S hS Z hZ x₂ f → g = h) ∧
      (∀ (Q : Over Z) (p : Q ⟶ isomSpaceSlice B S hS Z hZ x₂ x₂),
        p ≫ isomSpaceSliceMap B S hS Z hZ x₂ f = 1 ↔
          ∃ g : Q ⟶ relativeAutSpaceSlice B S hS Z hZ f x₂,
            g ≫ relativeAutSpaceSliceι B S hS Z hZ x₂ f = p) ∧
      IsAlgebraicSpace B S hS (isomSpaceOverSpace B S hS Z hZ x₁ x₂) ∧
      IsAlgebraicSpace B S hS (isomSpaceOverSpace B S hS Z hZ (x₁ ≫ f) (x₂ ≫ f)) ∧
      (∀ α : x₁ ≫ f ⟶ x₂ ≫ f,
        IsPullback (relativeIsomSpaceOverSpaceι B S hS Z hZ f x₁ x₂ α)
          (relativeIsomSpaceOverSpaceProj B S hS Z hZ f x₁ x₂ α)
          (isomSpaceOverSpaceMap B S hS Z hZ f x₁ x₂)
          (twistedSection B S hS Z hZ f x₁ x₂ α)) ∧
      (∀ α : x₁ ≫ f ⟶ x₂ ≫ f,
        IsAlgebraicSpace B S hS (relativeIsomSpaceOverSpace B S hS Z hZ f x₁ x₂ α)) ∧
      (∀ α : x₁ ≫ f ⟶ x₂ ≫ f,
        letI : ModObj (relativeAutSpaceSlice B S hS Z hZ f x₂)
            (relativeIsomSpaceSlice B S hS Z hZ f x₁ x₂ α) :=
          relativeIsomSpaceSliceModObj B S hS Z hZ f x₁ x₂ α
        IsPseudoTorsor (relativeAutSpaceSlice B S hS Z hZ f x₂)
          (relativeIsomSpaceSlice B S hS Z hZ f x₁ x₂ α))

Tag 06PQ, a lemma

Tag 06PQ in the Stacks Project.

AlgebraicGeometry.Stack.exists_cartesianRelativeInertiaSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeInertiaBaseChange.lean, line 214. The attribute's comment: “left square of algebraic stacks”.

Stacks 06PQ, the left square. Both squares of the diagram of Stacks 06PQ are 2-fibre products of algebraic stacks: the right one is the defining base-change square of Stacks 04T2, and this provides the left one, a comparison 1-morphism from the relative inertia of the base change to the relative inertia of π, with the prescribed action on objects and automorphisms, exhibiting the left square as a 2-fibre product in the 2-category of algebraic stacks.

theorem exists_cartesianRelativeInertiaSquare :
    Nonempty (CartesianRelativeInertiaSquare B S hS π f)

AlgebraicGeometry.Stack.isTwoFibreProduct_twoFibreProductSquareAlgebraicStacks, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/TwoFibreProductSquareAlgebraicStack.lean, line 112. The attribute's comment: “right square of algebraic stacks”.

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

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

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

Tag 06R5, a lemma

Tag 06R5 in the Stacks Project.

CategoryTheory.inertiaPullbackComparison_isEquivalenceOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/InertiaMonomorphism.lean, line 417.

For a fully faithful morphism, the inertia square is a 2-fibre product over the base, with its canonical comparison functor and vertical coherence.

public theorem inertiaPullbackComparison_isEquivalenceOver
    (hFF : F.FullyFaithful) :
    Nonempty (IsEquivalenceOver (RelativeInertia.toBase pX)
      (TwoFibreProductOver.structureFunctor (RelativeInertia.toBase pY) pX pY
        (RelativeInertia.π pY) F)
      (inertiaPullbackComparison pX pY F hF))

Tag 06PR, a lemma

Tag 06PR in the Stacks Project.

AlgebraicGeometry.Stack.isTwoFibreProduct_inertiaPresentationSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaPresentationSquare.lean, line 456. The attribute's comment: “the diagram is 2-cartesian, given Stacks 06PC and Stacks 06PB part 2”.

Let [U/R] ⟶ 𝒳 be a presentation and let G/U be the stabilizer group algebraic space of the presenting groupoid (U, R, s, t, c). Then

𝒮_G  ------>  𝒮_U
 |             |
 v             v
ℐ_𝒳  ------>  𝒳

is a fibre product diagram, i.e. a 2-fibre product in the sense of Stacks 003Q, given Groupoids in Spaces, Lemma 06PC and the second assertion of Stacks 06PB as the hypothesis Z.

noncomputable def isTwoFibreProduct_inertiaPresentationSquare
    (Z : InertiaQuotientStackInput B S hS P) :
    Bicategory.IsTwoFibreProduct (inertiaPresentationSquare B S hS P Z)

AlgebraicGeometry.Stack.nonempty_isTwoFibreProduct_inertiaPresentationSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaPresentationSquare.lean, line 468. The attribute's comment: “the diagram is a fibre product diagram”.

The diagram of the stabilizer, the object space, the inertia of 𝒳 and 𝒳 attached to a presentation [U/R] ⟶ 𝒳 is a fibre product diagram, given Groupoids in Spaces, Lemma 06PC with the inertia stack of [U/R] in its lower-left corner.

theorem nonempty_isTwoFibreProduct_inertiaPresentationSquare
    (Z : InertiaQuotientStackInput B S hS P) :
    Nonempty (Bicategory.IsTwoFibreProduct (inertiaPresentationSquare B S hS P Z))

AlgebraicGeometry.Stack.isTwoFibreProduct_inertiaPresentationSquareAlgebraicStacks, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaPresentationSquareAlgebraicStacks.lean, line 334. The attribute's comment: “the diagram is 2-cartesian in the 2-category of algebraic stacks”.

Let 𝒳 be an algebraic stack over S and let [U/R] ⟶ 𝒳 be a presentation. Let G/U be the stabilizer group algebraic space associated to the presenting groupoid (U, R, s, t, c). Then

𝒮_G  ------>  𝒮_U
 |             |
 v             v
ℐ_𝒳  ------>  𝒳

is a 2-fibre product diagram in the 2-category of algebraic stacks over S.

noncomputable def isTwoFibreProduct_inertiaPresentationSquareAlgebraicStacks :
    Bicategory.IsTwoFibreProduct (inertiaPresentationSquareAlgebraicStacks B S hS P)

AlgebraicGeometry.Stack.nonempty_isTwoFibreProduct_inertiaPresentationSquareAlgebraicStacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaPresentationSquareAlgebraicStacks.lean, line 348. The attribute's comment: “the diagram is a fibre product diagram of algebraic stacks”.

For an algebraic stack 𝒳 over S with a presentation [U/R] ⟶ 𝒳, the diagram of the algebraic stack of the stabilizer, the algebraic stack of the object space, the inertia of 𝒳 and 𝒳 is a fibre product diagram in the 2-category of algebraic stacks over S.

theorem nonempty_isTwoFibreProduct_inertiaPresentationSquareAlgebraicStacks :
    Nonempty (Bicategory.IsTwoFibreProduct
      (inertiaPresentationSquareAlgebraicStacks B S hS P))

AlgebraicGeometry.Stack.isTwoFibreProduct_presentationInertiaSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaPresentationSquareCanonical.lean, line 137. The attribute's comment: “the diagram is 2-cartesian”.

Stacks 06PR. Let 𝒳 be a category fibred in groupoids over the big fppf site of S — in particular an algebraic stack — and let [U/R] ⟶ 𝒳 be a presentation (Stacks 04TI). Let G/U be the stabilizer group algebraic space associated to the groupoid (U, R, s, t, c) (Stacks 0448). Then

𝒮_G  ------>  𝒮_U
 |             |
 v             v
ℐ_𝒳  ------>  𝒳

is a fibre product diagram, i.e. a 2-fibre product in the sense of Stacks 003Q.

This is AlgebraicGeometry.Stack.isTwoFibreProduct_inertiaPresentationSquare at the canonical input of AlgebraicGeometry.Stack.inertiaQuotientStackInput, so the proof is the proof of the source — immediate from Groupoids in Spaces, Lemma 06PC (AlgebraicGeometry.Stack.isTwoFibreProduct_inertiaQuotientStackSquareFibred together with the second assertion of Stacks 06PB) pasted onto the inertia square of Stacks 06R5 for the presentation — and the only datum it consumes is the presentation.

noncomputable def isTwoFibreProduct_presentationInertiaSquare :
    Bicategory.IsTwoFibreProduct (presentationInertiaSquare P)

AlgebraicGeometry.Stack.nonempty_isTwoFibreProduct_presentationInertiaSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/InertiaPresentationSquareCanonical.lean, line 145. The attribute's comment: “the diagram is a fibre product diagram”.

Stacks 06PR, in propositional form: for a presentation [U/R] ⟶ 𝒳 the diagram of the stack of the stabilizer, the stack of the object space, the inertia of 𝒳 and 𝒳 is a fibre product diagram.

theorem nonempty_isTwoFibreProduct_presentationInertiaSquare :
    Nonempty (Bicategory.IsTwoFibreProduct (presentationInertiaSquare P))

Sources

• Section 101.5, Tag 050P
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isAlgebraicStack_inertia · AlgebraicGeometry.Stack.isAlgebraicStack_relativeInertia · AlgebraicGeometry.Stack.AlgebraicStacks.isLocallyOfFiniteType_inertiaProjection · AlgebraicGeometry.Stack.isLocallyOfFiniteType_inertiaProjection · AlgebraicGeometry.Stack.isLocallyOfFiniteType_relativeInertiaProjection · AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_inertiaProjection · AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_inertiaProjection_of_isAlgebraicStack · AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_relativeInertiaProjection_of_isAlgebraicStack

Section101.6 Higher diagonals#

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

Tag 0CL0, a lemma

Tag 0CL0 in the Stacks Project.

AlgebraicGeometry.Stack.isRelativelyUnramified_relativeInertiaProjection_iff_isDM_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordRelativeInertiaConverse.lean, line 356. The attribute's comment: “part (4): the relative inertia projection is unramified iff f is DM, both directions and with no hypothesis. The direction (b) implies (a) is Stacks 0457 and 045C at the packaged unramified property; the converse needs no pseudo-torsor, being an instance of isUnramified_of_isUnramified_pullbackSnd, because the shear identifies the self-fibre-product of a fibre of the relative diagonal with the base change of the relative automorphism presheaf the inertia projection is tested on”.

Stacks 0CL0, part (4). For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S, the relative inertia projection π : I_{𝒳/𝒴} ⟶ 𝒳 is unramified, in the relative sense of Properties of Stacks, Section 04XB, exactly when f is DM.

The direction (b) ⇒ (a) is AlgebraicGeometry.Stack.isRelativelyUnramified_relativeInertiaProjection_of_isDM and (a) ⇒ (b) is AlgebraicGeometry.Stack.isDM_of_isRelativelyUnramified_relativeInertiaProjection; neither places any hypothesis on f.

theorem isRelativelyUnramified_relativeInertiaProjection_iff_isDM_unconditional
    (f : 𝒳 ⟶ 𝒴) :
    IsRelativelyUnramified B S hS (relativeInertiaProjection B S hS f).hom ↔ IsDM B S hS f

AlgebraicGeometry.Stack.isLocallyQuasiFinite_relativeInertiaProjection_iff_isQuasiDM_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DeligneMumfordRelativeInertiaConverse.lean, line 376. The attribute's comment: “part (5): the relative inertia projection is locally quasi-finite iff f is quasi-DM, both directions and with no hypothesis. The direction (b) implies (a) is Stacks 0457 and 045C at the packaged locally-quasi-finite property; the converse is an instance of isLocallyQuasiFinite_of_isLocallyQuasiFinite_pullbackSnd, the generic half of Stacks 0DSK, fed by the shear identification rather than by a pseudo-torsor”.

Stacks 0CL0, part (5). For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S, the relative inertia projection π : I_{𝒳/𝒴} ⟶ 𝒳 is locally quasi-finite, in the relative sense of Properties of Stacks, Section 04XB, exactly when f is quasi-DM.

The direction (b) ⇒ (a) is AlgebraicGeometry.Stack.isLocallyQuasiFinite_relativeInertiaProjection_of_isQuasiDM and (a) ⇒ (b) is AlgebraicGeometry.Stack.isQuasiDM_of_isLocallyQuasiFinite_relativeInertiaProjection; neither places any hypothesis on f. This is the part the proof of Stacks 0DSN cites.

theorem isLocallyQuasiFinite_relativeInertiaProjection_iff_isQuasiDM_unconditional
    (f : 𝒳 ⟶ 𝒴) :
    IsLocallyQuasiFinite B S hS (relativeInertiaProjection B S hS f).hom ↔
      AlgebraicStacks.IsQuasiDM B S hS f

AlgebraicGeometry.Stack.isLocallySeparated_relativeInertiaProjection_iff_relativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalSeparatednessRelativeInertia.lean, line 172. The attribute's comment: “part (3), conditions (a) and (b): the relative diagonal is locally separated exactly when the first projection of the relative inertia is”.

For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S, the relative inertia projection π : I_{𝒳/𝒴} ⟶ 𝒳 is locally separated, in the relative sense of Properties of Stacks, Section 04XB, exactly when the first relative diagonal Δ_{f, 1} = Δ_f : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 is.

theorem isLocallySeparated_relativeInertiaProjection_iff_relativeDiagonal (f : 𝒳 ⟶ 𝒴) :
    IsLocallySeparated B S hS (relativeInertiaProjection B S hS f).hom ↔
      IsLocallySeparated B S hS
        (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom)

AlgebraicGeometry.Stack.isLocallySeparated_relativeDiagonal_iff_isImmersion_neutralSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SecondRelativeDiagonalInertia.lean, line 406. The attribute's comment: “part (3), conditions (b) and (c): the relative diagonal is locally separated exactly when the neutral section of the relative inertia is an immersion”.

For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S, the relative diagonal Δ_{f, 1} = Δ_f is locally separated in the sense of Stacks 04XB exactly when Δ_{f, 2} = e : 𝒳 ⟶ I_{𝒳/𝒴}, the neutral section of the relative inertia, is an immersion of algebraic stacks in the sense of part (3) of Stacks 04YL.

This is Stacks 04YU read at Δ_f instead of at f — whose representability hypothesis is automatic there by part (1) of Stacks 04XS — composed with the identification of Δ_{f, 2} with the neutral section, which is what the source means by "since Δ_{f, 2} is the diagonal of Δ_f we have (b) ⇔ (c) by definition". The transports of the two conjuncts of part (3) of Stacks 04YL are isRepresentableByAlgebraicSpaces_secondRelativeDiagonal_iff_neutralSection and isImmersion_secondRelativeDiagonal_iff_neutralSection.

theorem isLocallySeparated_relativeDiagonal_iff_isImmersion_neutralSection (f : 𝒳 ⟶ 𝒴) :
    IsLocallySeparated B S hS
        (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom) ↔
      AlgebraicStacks.IsImmersion B S hS (relativeInertiaStackNeutralSection B S hS f)

AlgebraicGeometry.Stack.isSeparated_relativeInertiaProjection_iff_relativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationRelativeInertia.lean, line 370. The attribute's comment: “part (1), conditions (a) and (b): the relative inertia projection is separated exactly when the first relative diagonal is”.

Stacks 0CL0, part (1), conditions (a) and (b). For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S, the relative inertia projection π : I_{𝒳/𝒴} ⟶ 𝒳 is separated, in the relative sense of Properties of Stacks, Section 04XB, exactly when the first relative diagonal Δ_{f, 1} = Δ_f : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 is.

Both conditions are first read at the first projection pr₁ of the 2-fibre product of Δ_f with itself, by AlgebraicGeometry.Stack.isSeparated_relativeInertiaProjection_iff_twoFibreProductFst. Then:

• (b) ⇒ (a) is Stacks 045C: pr₁ is a base change of Δ_f, so it inherits separatedness, and no hypothesis on the property is needed.
• (a) ⇒ (b) is the section argument. Δ_{f, 2} ≫ pr₁ = 𝟙 𝒳, so Δ_{f, 2} is a section of pr₁, and AlgebraicGeometry.Stack.isClosedImmersion_section_of_isSeparated — Stacks 04YS at pr₁, which is representable by AlgebraicGeometry.Stack.isRepresentableByAlgebraicSpaces_twoFibreProductFst_relativeDiagonal, followed by the three hypothesis-free transfers — makes Δ_{f, 2} a closed immersion. Stacks 04YS read at Δ_f instead of at pr₁ turns that back into separatedness of Δ_f.

Neither direction uses the group law of the relative inertia, so Groupoids in Spaces, Lemma 06P6 — the source's route, and Chapter 78 — is not needed; see the module docstring.

This theorem and AlgebraicGeometry.Stack.isSeparated_relativeDiagonal_iff_isClosedImmersion_neutralSection, which is (b) ⇔ (c), are together the covering set of part (1) of Stacks 0CL0, and both carry it.

theorem isSeparated_relativeInertiaProjection_iff_relativeDiagonal (f : 𝒳 ⟶ 𝒴) :
    IsSeparated B S hS (relativeInertiaProjection B S hS f).hom ↔
      IsSeparated B S hS
        (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom)

AlgebraicGeometry.Stack.isQuasiSeparated_relativeInertiaProjection_iff_relativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationRelativeInertia.lean, line 406. The attribute's comment: “part (2), conditions (a) and (b): the relative inertia projection is quasi-separated exactly when the first relative diagonal is”.

Stacks 0CL0, part (2), conditions (a) and (b). For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S, the relative inertia projection π : I_{𝒳/𝒴} ⟶ 𝒳 is quasi-separated, in the relative sense of Properties of Stacks, Section 04XB, exactly when the first relative diagonal Δ_{f, 1} = Δ_f is.

The argument is that of AlgebraicGeometry.Stack.isSeparated_relativeInertiaProjection_iff_relativeDiagonal one step down the scale: (b) ⇒ (a) is Stacks 045C at quasi-separatedness, and (a) ⇒ (b) is Stacks 04YT at pr₁ — making the section Δ_{f, 2} quasi-compact through AlgebraicGeometry.Stack.isRelativelyQuasiCompact_section_of_isQuasiSeparated — followed by Stacks 04YT read at Δ_f.

This theorem and AlgebraicGeometry.Stack.isQuasiSeparated_relativeDiagonal_iff_isQuasiCompact_neutralSection, which is (b) ⇔ (c), are together the covering set of part (2) of Stacks 0CL0, and both carry it.

theorem isQuasiSeparated_relativeInertiaProjection_iff_relativeDiagonal (f : 𝒳 ⟶ 𝒴) :
    IsQuasiSeparated B S hS (relativeInertiaProjection B S hS f).hom ↔
      IsQuasiSeparated B S hS
        (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom)

AlgebraicGeometry.Stack.isSeparated_relativeDiagonal_iff_isClosedImmersion_neutralSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationRelativeInertia.lean, line 437. The attribute's comment: “part (1), conditions (b) and (c): the relative diagonal is separated exactly when the neutral section of the relative inertia is a closed immersion”.

Stacks 0CL0, part (1), conditions (b) and (c). For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S, the relative diagonal Δ_{f, 1} = Δ_f is separated in the sense of Stacks 04XB exactly when Δ_{f, 2} = e : 𝒳 ⟶ I_{𝒳/𝒴}, the neutral section of the relative inertia, is a closed immersion of algebraic stacks in the sense of part (2) of Stacks 04YL.

This is part (1) of Stacks 04YZ — Stacks 04YS read at Δ_f, whose representability hypothesis is automatic by part (1) of Stacks 04XS — composed with the identification of Δ_{f, 2} with the neutral section, which is what the source means by "since Δ_{f, 2} is the diagonal of Δ_f we have (b) ⇔ (c) by definition". The transports of the two conjuncts of part (2) of Stacks 04YL are Stack.isRepresentableByAlgebraicSpaces_secondRelativeDiagonal_iff_neutralSection and Stack.isClosedImmersion_secondRelativeDiagonal_iff_neutralSection.

theorem isSeparated_relativeDiagonal_iff_isClosedImmersion_neutralSection (f : 𝒳 ⟶ 𝒴) :
    IsSeparated B S hS
        (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom) ↔
      AlgebraicStacks.IsClosedImmersion B S hS (relativeInertiaStackNeutralSection B S hS f)

AlgebraicGeometry.Stack.isQuasiSeparated_relativeDiagonal_iff_isQuasiCompact_neutralSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparationRelativeInertia.lean, line 458. The attribute's comment: “part (2), conditions (b) and (c): the relative diagonal is quasi-separated exactly when the neutral section of the relative inertia is quasi-compact”.

Stacks 0CL0, part (2), conditions (b) and (c). For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S, the relative diagonal Δ_{f, 1} = Δ_f is quasi-separated in the sense of Stacks 04XB exactly when Δ_{f, 2} = e : 𝒳 ⟶ I_{𝒳/𝒴}, the neutral section of the relative inertia, is quasi-compact in that sense.

This is part (2) of Stacks 04YZ — Stacks 04YT read at Δ_f — composed with AlgebraicGeometry.Stack.isQuasiCompact_secondRelativeDiagonal_iff_neutralSection. Being quasi-compact is not one of the three parts of Stacks 04YL, so unlike condition (1)(c) there is no representability conjunct to transport alongside.

theorem isQuasiSeparated_relativeDiagonal_iff_isQuasiCompact_neutralSection (f : 𝒳 ⟶ 𝒴) :
    IsQuasiSeparated B S hS
        (relativeDiagonal.{u, u, u + 1} B S hS 𝒳.val 𝒴.val f.hom) ↔
      IsQuasiCompact B S hS (relativeInertiaStackNeutralSection B S hS f).hom

Tag 04YY, a lemma

Tag 04YY in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_of_isEquivalence_secondRelativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/FaithfulRepresentableUnconditional.lean, line 98. The attribute's comment: “the implication (2) ⟹ (1)”.

Stacks 04YY, the implication (2) ⟹ (1). A 1-morphism of algebraic stacks over S whose second diagonal Δ_{f, 2} is an isomorphism is representable by algebraic spaces: the second diagonal is an isomorphism exactly when f is faithful (Stacks 04Z7), and a faithful 1-morphism of algebraic stacks is representable by algebraic spaces (Stacks 04Y5).

theorem isRepresentableByAlgebraicSpaces_of_isEquivalence_secondRelativeDiagonal (f : 𝒳 ⟶ 𝒴)
    (hf : Functor.IsEquivalence (secondRelativeDiagonal B S hS f.hom).hom.toFunctor) :
    IsRepresentableByAlgebraicSpaces B S hS f.hom.hom

AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RepresentableSecondDiagonalTFAE.lean, line 54.

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

1. f is representable by algebraic spaces;
2. the second diagonal Δ_{f, 2} is an isomorphism;
3. the relative inertia I_{𝒳/𝒴} is trivial over 𝒳, that is, its neutral section e : 𝒳 ⟶ I_{𝒳/𝒴} is an isomorphism;
4. for every scheme T and every x : T ⟶ 𝒳 the kernel of Isom_𝒳(x, x) ⟶ Isom_𝒴(f ∘ x, f ∘ x) is trivial — stated as: every endomorphism of an object of 𝒳 which f sends to an identity is an identity.

theorem isRepresentableByAlgebraicSpaces_tfae (f : 𝒳 ⟶ 𝒴) :
    List.TFAE
      [IsRepresentableByAlgebraicSpaces B S hS f.hom.hom,
        Functor.IsEquivalence (secondRelativeDiagonal B S hS f.hom).hom.toFunctor,
        Functor.IsEquivalence
          (relativeInertiaStackNeutralSection B S hS f).hom.hom.toFunctor,
        ∀ (x : 𝒳.val.val.obj) (a : x ⟶ x),
          (CatFiberedInGroupoids.homFunctor f.hom).map a = 𝟙 _ → a = 𝟙 x]

AlgebraicGeometry.Stack.AlgebraicStacks.isEquivalence_secondRelativeDiagonal_iff_relativeInertiaTrivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SecondDiagonalRepresentable.lean, line 239. The attribute's comment: “the equivalence of parts (2) and (3)”.

Stacks 04YY, the equivalence of parts (2) and (3). For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S, the second diagonal Δ_{f, 2} is an isomorphism exactly when the relative inertia group stack I_{𝒳/𝒴} is trivial over 𝒳, that is, exactly when its neutral section e : 𝒳 ⟶ I_{𝒳/𝒴} is an isomorphism.

theorem isEquivalence_secondRelativeDiagonal_iff_relativeInertiaTrivial (f : 𝒳 ⟶ 𝒴) :
    Functor.IsEquivalence (secondRelativeDiagonal B S hS f.hom).hom.toFunctor ↔
      Functor.IsEquivalence
        (relativeInertiaStackNeutralSection B S hS f).hom.hom.toFunctor

AlgebraicGeometry.Stack.AlgebraicStacks.relativeInertiaTrivial_iff_isomKernel_trivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SecondDiagonalRepresentable.lean, line 250. The attribute's comment: “the equivalence of parts (3) and (4)”.

Stacks 04YY, the equivalence of parts (3) and (4). The relative inertia I_{𝒳/𝒴} of a 1-morphism of algebraic stacks is trivial over 𝒳 exactly when, for every scheme T and every x : T ⟶ 𝒳, the kernel of Isom_𝒳(x, x) ⟶ Isom_𝒴(f ∘ x, f ∘ x) is trivial — stated as: every endomorphism of an object of 𝒳 which f sends to an identity is an identity.

theorem relativeInertiaTrivial_iff_isomKernel_trivial (f : 𝒳 ⟶ 𝒴) :
    Functor.IsEquivalence
        (relativeInertiaStackNeutralSection B S hS f).hom.hom.toFunctor ↔
      ∀ (x : 𝒳.val.val.obj) (a : x ⟶ x),
        (CatFiberedInGroupoids.homFunctor f.hom).map a = 𝟙 _ → a = 𝟙 x

AlgebraicGeometry.Stack.AlgebraicStacks.secondRelativeDiagonal_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SecondDiagonalRepresentable.lean, line 262. The attribute's comment: “the equivalence of parts (2), (3) and (4)”.

Stacks 04YY, the equivalence of parts (2), (3) and (4). For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S the following are equivalent: the second diagonal Δ_{f, 2} is an isomorphism; the relative inertia I_{𝒳/𝒴} is trivial over 𝒳; the kernel of the map on Isom sheaves attached to any object of 𝒳 over a scheme is trivial.

theorem secondRelativeDiagonal_tfae (f : 𝒳 ⟶ 𝒴) :
    List.TFAE
      [Functor.IsEquivalence (secondRelativeDiagonal B S hS f.hom).hom.toFunctor,
        Functor.IsEquivalence
          (relativeInertiaStackNeutralSection B S hS f).hom.hom.toFunctor,
        ∀ (x : 𝒳.val.val.obj) (a : x ⟶ x),
          (CatFiberedInGroupoids.homFunctor f.hom).map a = 𝟙 _ → a = 𝟙 x]

AlgebraicGeometry.Stack.AlgebraicStacks.isEquivalence_secondRelativeDiagonal_of_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SecondDiagonalRepresentable.lean, line 280. The attribute's comment: “the implication (1) ⟹ (2)”.

Stacks 04YY, the implication (1) ⟹ (2). If a 1-morphism of algebraic stacks over S is representable by algebraic spaces then its second diagonal Δ_{f, 2} is an isomorphism.

By Stacks 04Y5 representability by algebraic spaces makes the underlying functor faithful, and by Stacks 04Z7 that is exactly the second diagonal being an isomorphism.

theorem isEquivalence_secondRelativeDiagonal_of_isRepresentableByAlgebraicSpaces (f : 𝒳 ⟶ 𝒴)
    (hf : IsRepresentableByAlgebraicSpaces B S hS f.hom.hom) :
    Functor.IsEquivalence (secondRelativeDiagonal B S hS f.hom).hom.toFunctor

Tag 0AHJ, a lemma

Tag 0AHJ in the Stacks Project.

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

Stacks 0AHJ, part (1). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is a monomorphism (Stacks 04ZW) if and only if its first relative diagonal Δ_{f,1} is an isomorphism, i.e. has underlying functor an equivalence of categories.

Both directions pass through full faithfulness of f: Stacks 04Z7 says Δ_{f,1} is an equivalence exactly when f is fully faithful, Stacks 05UK turns the monomorphy clause into full faithfulness, and Stacks 04ZZ turns full faithfulness back into the monomorphy clause.

The representability conjunct of AlgebraicGeometry.Stack.AlgebraicStacks.IsMonomorphism in the "if" direction is the implication (2) ⟹ (3) of Stacks 04Y5 at f.

theorem isMonomorphism_iff_isEquivalence_relativeDiagonal (f : 𝒳 ⟶ 𝒴) :
    IsMonomorphism B S hS f ↔
      Functor.IsEquivalence
        (CatFiberedInGroupoids.homFunctor (relativeDiagonalAlgebraicStacks B S hS f).hom)

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

Stacks 0AHJ, part (2). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is representable by algebraic spaces if and only if its first relative diagonal Δ_{f,1} is a monomorphism (Stacks 04ZW).

The "only if" direction is part (3) of Stacks 04YQ. For the converse, Stacks 05UK makes Δ_{f,1} full, which by Stacks 04Z7 — the content clause (2) of Stacks 04YY reads as Δ_{f,2} being an isomorphism — makes f faithful, and faithfulness is representability by Stacks 04Y5.

That last step, the implication (2) ⟹ (3) of Stacks 04Y5 at f, is AlgebraicGeometry.Stack.AlgebraicStacks.isRepresentableByAlgebraicSpaces_of_faithful.

theorem isRepresentableByAlgebraicSpaces_iff_isMonomorphism_relativeDiagonal (f : 𝒳 ⟶ 𝒴) :
    IsRepresentableByAlgebraicSpaces B S hS f.hom.hom ↔
      IsMonomorphism B S hS (relativeDiagonalAlgebraicStacks B S hS f)

AlgebraicGeometry.Stack.AlgebraicStacks.isMonomorphism_secondRelativeDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/HigherDiagonalMonomorphism.lean, line 178. The attribute's comment: “the second diagonal is always a monomorphism”.

Stacks 0AHJ, the final assertion. The second relative diagonal Δ_{f,2} of any 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is a monomorphism (Stacks 04ZW). No hypothesis on f is needed.

This is the "only if" direction of part (2) applied to Δ_{f,1}, which is representable by algebraic spaces unconditionally by part (1) of Stacks 04XS.

theorem isMonomorphism_secondRelativeDiagonal (f : 𝒳 ⟶ 𝒴) :
    IsMonomorphism B S hS
      (relativeDiagonalAlgebraicStacks B S hS (relativeDiagonalAlgebraicStacks B S hS f))

Tag 04YZ, a lemma

Tag 04YZ in the Stacks Project.

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

For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S the following are equivalent: the first relative diagonal Δ_{f,1} is separated; the second relative diagonal Δ_{f,2} is a closed immersion, part (2) of Stacks 04YL; Δ_{f,2} is proper; Δ_{f,2} is universally closed — the last two, and the first, in the relative sense of Stacks 04XB.

theorem isSeparated_firstRelativeDiagonal_tfae (f : 𝒳 ⟶ 𝒴) :
    List.TFAE
      [IsSeparated B S hS (relativeDiagonalAlgebraicStacks B S hS f).hom,
       AlgebraicStacks.IsClosedImmersion B S hS
         (relativeDiagonalAlgebraicStacks B S hS (relativeDiagonalAlgebraicStacks B S hS f)),
       IsProper B S hS
         (relativeDiagonalAlgebraicStacks B S hS
           (relativeDiagonalAlgebraicStacks B S hS f)).hom,
       UniversallyClosed B S hS
         (relativeDiagonalAlgebraicStacks B S hS
           (relativeDiagonalAlgebraicStacks B S hS f)).hom]

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

For a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S the following are equivalent: the first relative diagonal Δ_{f,1} is quasi-separated; the second relative diagonal Δ_{f,2} is of finite type; Δ_{f,2} is quasi-compact — all three in the relative sense of Stacks 04XB.

theorem isQuasiSeparated_firstRelativeDiagonal_tfae (f : 𝒳 ⟶ 𝒴) :
    List.TFAE
      [IsQuasiSeparated B S hS (relativeDiagonalAlgebraicStacks B S hS f).hom,
       IsFiniteType B S hS
         (relativeDiagonalAlgebraicStacks B S hS
           (relativeDiagonalAlgebraicStacks B S hS f)).hom,
       IsQuasiCompact B S hS
         (relativeDiagonalAlgebraicStacks B S hS
           (relativeDiagonalAlgebraicStacks B S hS f)).hom]

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

The first relative diagonal Δ_{f,1} of a 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S is locally separated, in the relative sense of Stacks 04XB, if and only if the second relative diagonal Δ_{f,2} is an immersion, part (3) of Stacks 04YL.

theorem isLocallySeparated_firstRelativeDiagonal_iff_isImmersion_second (f : 𝒳 ⟶ 𝒴) :
    IsLocallySeparated B S hS (relativeDiagonalAlgebraicStacks B S hS f).hom ↔
      AlgebraicStacks.IsImmersion B S hS
        (relativeDiagonalAlgebraicStacks B S hS (relativeDiagonalAlgebraicStacks B S hS f))

Tag 04Z0, a lemma

Tag 04Z0 in the Stacks Project.

AlgebraicGeometry.Stack.isDM_iff_isUnramifiedRelative_diagonals, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DMSecondDiagonal.lean, line 149. The attribute's comment: “dm”.

Stacks 04Z0, part (4). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S — with no representability hypothesis — is DM, in the sense of Definition 04YW, if and only if its first relative diagonal Δ_{f,1} : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 and its second relative diagonal Δ_{f,2}, the relative diagonal of Δ_{f,1}, are both unramified in the relative sense of Properties of Stacks, Section 04XB.

Definition 04YW is representability of Δ_{f,1} by algebraic spaces together with Section 04XB unramifiedness of it; the representability clause is a theorem for a 1-morphism of algebraic stacks — part (1) of Stacks 04XS — so the condition carried here is the Section 04XB clause alone and the left-hand side is the first conjunct on the right. The second conjunct is unconditionally true, which is the source's own proof: Δ_{f,2} is the relative diagonal of Δ_{f,1}, which is representable by algebraic spaces, so part (3) of Stacks 050E — Stacks 05W6 applied at a diagonal which is locally of finite type and a monomorphism by parts (2) and (3) of Stacks 04YQ — makes it unramified with no hypothesis on f.

theorem isDM_iff_isUnramifiedRelative_diagonals (f : 𝒳 ⟶ 𝒴) :
    IsDM B S hS f ↔
      (IsUnramifiedRelative B S hS (relativeDiagonalAlgebraicStacks B S hS f).hom ∧
        IsUnramifiedRelative B S hS (relativeDiagonalAlgebraicStacks B S hS
          (relativeDiagonalAlgebraicStacks B S hS f)).hom)

AlgebraicGeometry.Stack.isQuasiDM_iff_isLocallyQuasiFinite_diagonals, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiDMSecondDiagonal.lean, line 54. The attribute's comment: “quasi_dm”.

A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S — with no representability hypothesis — is quasi-DM, in the sense of Definition 04YW, if and only if its first relative diagonal Δ_{f,1} : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 and its second relative diagonal Δ_{f,2}, the relative diagonal of Δ_{f,1}, are both locally quasi-finite in the relative sense of Properties of Stacks, Section 04XB.

theorem isQuasiDM_iff_isLocallyQuasiFinite_diagonals (f : 𝒳 ⟶ 𝒴) :
    AlgebraicStacks.IsQuasiDM B S hS f ↔
      (IsLocallyQuasiFinite B S hS (relativeDiagonalAlgebraicStacks B S hS f).hom ∧
        IsLocallyQuasiFinite B S hS (relativeDiagonalAlgebraicStacks B S hS
          (relativeDiagonalAlgebraicStacks B S hS f)).hom)

AlgebraicGeometry.Stack.isQuasiSeparated_iff_isQuasiCompactMorphism_diagonals, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasiSeparatedSecondDiagonal.lean, line 323. The attribute's comment: “quasi_separated”.

Stacks 04Z0, part (2). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S — with no representability hypothesis — is quasi-separated, in the sense of Definition 04YW, if and only if its first relative diagonal Δ_{f,1} : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 and its second relative diagonal Δ_{f,2}, the relative diagonal of Δ_{f,1}, are both quasi-compact in the sense of Definition 050U.

Definition 04YW is the conjunction, at every algebraic space representing a base change of Δ_{f,1} along a scheme-valued point, of quasi-compactness and quasi-separatedness of the structural morphism, so the left-hand side splits as Section 04XB quasi-compactness of Δ_{f,1} together with Section 04XB quasi-separatedness of Δ_{f,1}. Part (2) of Stacks 04YZ, which is AlgebraicGeometry.Stack.isQuasiCompact_relativeDiagonal_iff_isQuasiSeparated applied to Δ_{f,1}, replaces the second of those by Section 04XB quasi-compactness of Δ_{f,2}; and Stacks 050T, AlgebraicGeometry.Stack.isQuasiCompact_iff_baseChange_quasiCompact, replaces Section 04XB quasi-compactness of each diagonal by Definition 050U quasi-compactness, which is the form the statement asks for. Both diagonals are representable by algebraic spaces by part (1) of Stacks 04XS, so neither application needs a hypothesis.

theorem isQuasiSeparated_iff_isQuasiCompactMorphism_diagonals (f : 𝒳 ⟶ 𝒴) :
    AlgebraicStacks.IsQuasiSeparated B S hS f ↔
      (IsQuasiCompactMorphism B S hS (relativeDiagonalAlgebraicStacks B S hS f) ∧
        IsQuasiCompactMorphism B S hS (relativeDiagonalAlgebraicStacks B S hS
          (relativeDiagonalAlgebraicStacks B S hS f)))

AlgebraicGeometry.Stack.isSeparated_iff_universallyClosed_diagonals, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedSecondDiagonal.lean, line 117. The attribute's comment: “separated”.

Stacks 04Z0, part (1). A 1-morphism f : 𝒳 ⟶ 𝒴 of algebraic stacks over S — with no representability hypothesis — is separated, in the sense of Definition 04YW, if and only if its first relative diagonal Δ_{f,1} : 𝒳 ⟶ 𝒳 ×_{f, 𝒴, f} 𝒳 and its second relative diagonal Δ_{f,2}, the relative diagonal of Δ_{f,1}, are both universally closed in the relative sense of Properties of Stacks, Section 04XB.

Definition 04YW is properness of Δ_{f,1}, and properness of a morphism of algebraic spaces is separatedness, finite type and universal closedness. Universal closedness of Δ_{f,1} is the first conjunct on the right; its separatedness is universal closedness of Δ_{f,2} by part (1) of Stacks 04YZ; it is unconditionally locally of finite type by part (2) of Stacks 04XS; and it is quasi-compact because it is universally closed, by Stacks 04XW.

theorem isSeparated_iff_universallyClosed_diagonals (f : 𝒳 ⟶ 𝒴) :
    AlgebraicStacks.IsSeparated B S hS f ↔
      (UniversallyClosed B S hS (relativeDiagonalAlgebraicStacks B S hS f).hom ∧
        UniversallyClosed B S hS (relativeDiagonalAlgebraicStacks B S hS
          (relativeDiagonalAlgebraicStacks B S hS f)).hom)

Tag 0CPL, a lemma

Tag 0CPL in the Stacks Project.

AlgebraicGeometry.Stack.HigherDiagonal.isProper_mapBase_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedIsomPullback.lean, line 235. The attribute's comment: “part (1): proper”.

Stacks 0CPL, part (1), the separated case. If f : 𝒳 ⟶ 𝒴 is separated then the comparison T₁ ×_{x₁, 𝒳, x₂} T₂ ⟶ T₁ ×_{y₁, 𝒴, y₂} T₂ of algebraic-space-valued points of 𝒳 is proper, in the sense of Stacks 04XB.

This is Stacks 050H part (6) at a cospan whose two sources are algebraic spaces.

theorem isProper_mapBase_of_isSeparated (hf : AlgebraicStacks.IsSeparated B S hS f) :
    Stack.IsProper.{u, u, u + 1} B S hS (AlgebraicStacks.mapBase B S hS x₁ x₂ f).hom

AlgebraicGeometry.Stack.HigherDiagonal.isQuasiCompactAndQuasiSeparated_mapBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedIsomPullback.lean, line 245. The attribute's comment: “part (1): quasi-compact and quasi-separated”.

Stacks 0CPL, part (1), the quasi-separated case. If f : 𝒳 ⟶ 𝒴 is quasi-separated then the comparison T₁ ×_{x₁, 𝒳, x₂} T₂ ⟶ T₁ ×_{y₁, 𝒴, y₂} T₂ of algebraic-space-valued points of 𝒳 is quasi-compact and quasi-separated, in the sense of Stacks 04XB.

This is Stacks 050H part (7) at a cospan whose two sources are algebraic spaces.

theorem isQuasiCompactAndQuasiSeparated_mapBase
    (hf : AlgebraicStacks.IsQuasiSeparated B S hS f) :
    Stack.IsQuasiCompact.{u, u, u + 1} B S hS
        (AlgebraicStacks.mapBase B S hS x₁ x₂ f).hom ∧
      Stack.IsQuasiSeparated.{u, u, u + 1} B S hS
        (AlgebraicStacks.mapBase B S hS x₁ x₂ f).hom

AlgebraicGeometry.Stack.HigherDiagonal.isLocallyQuasiFinite_mapBase_of_isQuasiDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedIsomPullback.lean, line 259. The attribute's comment: “part (1): locally quasi-finite”.

Stacks 0CPL, part (1), the quasi-DM case. If f : 𝒳 ⟶ 𝒴 is quasi-DM then the comparison T₁ ×_{x₁, 𝒳, x₂} T₂ ⟶ T₁ ×_{y₁, 𝒴, y₂} T₂ of algebraic-space-valued points of 𝒳 is locally quasi-finite, in the sense of Stacks 04XB.

This is Stacks 050H part (5) at a cospan whose two sources are algebraic spaces.

theorem isLocallyQuasiFinite_mapBase_of_isQuasiDM
    (hf : AlgebraicStacks.IsQuasiDM B S hS f) :
    Stack.IsLocallyQuasiFinite.{u, u, u + 1} B S hS
      (AlgebraicStacks.mapBase B S hS x₁ x₂ f).hom

AlgebraicGeometry.Stack.HigherDiagonal.isUnramified_mapBase_of_isDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedIsomPullback.lean, line 271. The attribute's comment: “part (1): unramified”.

Stacks 0CPL, part (1), the Deligne–Mumford case. If f : 𝒳 ⟶ 𝒴 is Deligne–Mumford then the comparison T₁ ×_{x₁, 𝒳, x₂} T₂ ⟶ T₁ ×_{y₁, 𝒴, y₂} T₂ of algebraic-space-valued points of 𝒳 is unramified, in the sense of Stacks 04XB.

This is Stacks 050H part (4) at a cospan whose two sources are algebraic spaces.

theorem isUnramified_mapBase_of_isDM (hf : Stack.IsDM B S hS f) :
    ∀ (U : BigFppfOver B S hS)
      (z : BigFppfOver B U.left.1 U.left.2 ⥤
        (AlgebraicStacks.twoFibreProduct B S hS (x₁ ≫ f) (x₂ ≫ f)).val.val.obj)
      (_hz : z ⋙ (AlgebraicStacks.twoFibreProduct B S hS (x₁ ≫ f) (x₂ ≫ f)).val.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)
            (AlgebraicStacks.twoFibreProduct B S hS x₁ x₂).val.val.p
            (AlgebraicStacks.twoFibreProduct B S hS (x₁ ≫ f) (x₂ ≫ f)).val.val.p z
            (CatFiberedInGroupoids.homFunctor (AlgebraicStacks.mapBase B S hS x₁ x₂ f).hom))
          (presheafOfCategories (F ⋙ typeToCat)).p) →
        Space.IsUnramified B S hS
          (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨F, hF⟩)).hom

AlgebraicGeometry.Stack.HigherDiagonal.isProper_isomMap_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedIsomPullback.lean, line 445. The attribute's comment: “part (2): proper”.

Stacks 0CPL, part (2), the separated case. If f : 𝒳 ⟶ 𝒴 is separated then the induced map Isom_𝒳(x₁, x₂) ⟶ Isom_𝒴(y₁, y₂) is proper, in the sense of Stacks 04XB.

theorem isProper_isomMap_of_isSeparated (hf : AlgebraicStacks.IsSeparated B S hS f) :
    Stack.IsProper.{u, u, u + 1} B S hS (isomMap B S hS f T hT x₁ x₂)

AlgebraicGeometry.Stack.HigherDiagonal.isQuasiCompactAndQuasiSeparated_isomMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedIsomPullback.lean, line 455. The attribute's comment: “part (2): quasi-compact and quasi-separated”.

Stacks 0CPL, part (2), the quasi-separated case. If f : 𝒳 ⟶ 𝒴 is quasi-separated then the induced map Isom_𝒳(x₁, x₂) ⟶ Isom_𝒴(y₁, y₂) is quasi-compact and quasi-separated, in the sense of Stacks 04XB.

theorem isQuasiCompactAndQuasiSeparated_isomMap
    (hf : AlgebraicStacks.IsQuasiSeparated B S hS f) :
    Stack.IsQuasiCompact.{u, u, u + 1} B S hS (isomMap B S hS f T hT x₁ x₂) ∧
      Stack.IsQuasiSeparated.{u, u, u + 1} B S hS (isomMap B S hS f T hT x₁ x₂)

AlgebraicGeometry.Stack.HigherDiagonal.isLocallyQuasiFinite_isomMap_of_isQuasiDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedIsomPullback.lean, line 469. The attribute's comment: “part (2): locally quasi-finite”.

Stacks 0CPL, part (2), the quasi-DM case. If f : 𝒳 ⟶ 𝒴 is quasi-DM then the induced map Isom_𝒳(x₁, x₂) ⟶ Isom_𝒴(y₁, y₂) is locally quasi-finite, in the sense of Stacks 04XB.

theorem isLocallyQuasiFinite_isomMap_of_isQuasiDM
    (hf : AlgebraicStacks.IsQuasiDM B S hS f) :
    Stack.IsLocallyQuasiFinite.{u, u, u + 1} B S hS (isomMap B S hS f T hT x₁ x₂)

AlgebraicGeometry.Stack.HigherDiagonal.isUnramified_isomMap_of_isDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SeparatedIsomPullback.lean, line 480. The attribute's comment: “part (2): unramified”.

Stacks 0CPL, part (2), the Deligne–Mumford case. If f : 𝒳 ⟶ 𝒴 is Deligne–Mumford then the induced map Isom_𝒳(x₁, x₂) ⟶ Isom_𝒴(y₁, y₂) is unramified, in the sense of Stacks 04XB.

theorem isUnramified_isomMap_of_isDM (hf : Stack.IsDM B S hS f) :
    ∀ (U : BigFppfOver B S hS)
      (z : BigFppfOver B U.left.1 U.left.2 ⥤
        (isomStack B S hS T hT (x₁ ≫ f) (x₂ ≫ f)).val.obj)
      (_hz : z ⋙ (isomStack B S hS T hT (x₁ ≫ f) (x₂ ≫ f)).val.p = Over.map U.hom)
      (G : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
      (hG : IsAlgebraicSpace B U.left.1 U.left.2 G),
        Nonempty (StacksRepresentableCFG.EquivalenceOver
          (TwoFibreProductOver.fst (Over.map U.hom)
            (isomStack B S hS T hT x₁ x₂).val.p
            (isomStack B S hS T hT (x₁ ≫ f) (x₂ ≫ f)).val.p z
            (CatFiberedInGroupoids.homFunctor (isomMap B S hS f T hT x₁ x₂)))
          (presheafOfCategories (G ⋙ typeToCat)).p) →
        Space.IsUnramified B S hS
          (algebraicSpaceMap B S hS U
            ((spacesOverSmallerBaseFunctor B U.left.1 S U.left.2 hS U.hom).obj ⟨G, hG⟩)).hom

Sources

• Section 101.6, Tag 04YX
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Stack.isRelativelyUnramified_relativeInertiaProjection_iff_isDM_unconditional · AlgebraicGeometry.Stack.isLocallyQuasiFinite_relativeInertiaProjection_iff_isQuasiDM_unconditional · AlgebraicGeometry.Stack.isLocallySeparated_relativeInertiaProjection_iff_relativeDiagonal · AlgebraicGeometry.Stack.isLocallySeparated_relativeDiagonal_iff_isImmersion_neutralSection · AlgebraicGeometry.Stack.isSeparated_relativeInertiaProjection_iff_relativeDiagonal · AlgebraicGeometry.Stack.isQuasiSeparated_relativeInertiaProjection_iff_relativeDiagonal · AlgebraicGeometry.Stack.isSeparated_relativeDiagonal_iff_isClosedImmersion_neutralSection · AlgebraicGeometry.Stack.isQuasiSeparated_relativeDiagonal_iff_isQuasiCompact_neutralSection

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.