83 Quotients of Groupoids

Chapter 83 of the Stacks Project, Quotients of Groupoids, Tag 048A: the 8 sections of its 10 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 37 tags are carried by 99 declarations of the repository (all in StacksFrontier) and 4 registered declarations.

Section83.3 Invariant morphisms#

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

Tag 048E, a definition

Tag 048E in the Stacks Project.

AlgebraicGeometry.Space.IsInvariant, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvariantMorphisms.lean, line 93. The attribute's comment: “R-invariant”.

A morphism φ out of U is invariant under a pre-relation j : R ⟶ U ×_Z U when it identifies the target and the source of every arrow of j.

noncomputable abbrev IsInvariant {C : Type*} [Category C] {Z : C}
    [HasBinaryProducts (Over Z)] {R U : Over Z} {X : C}
    (j : PreRelation R U) (φ : U.left ⟶ X) : Prop

AlgebraicGeometry.Space.IsGroupInvariant, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvariantMorphisms.lean, line 101. The attribute's comment: “G-invariant”. References: SGA 3 IV (3.2.1), “special case”.

A morphism φ out of an object U carrying an action of a group algebraic space G is invariant when acting does not change its value.

noncomputable abbrev IsGroupInvariant
    (G : Over B.obj) {U X : Over B.obj} [GrpObj G] [ModObj G U]
    (φ : U ⟶ X) : Prop

Tag 048F, a lemma

Tag 048F in the Stacks Project.

AlgebraicGeometry.Space.invariant_iff_factors_through_quotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/QuotientSheafBaseChange.lean, line 75.

Stacks 048F. A morphism from U to a sheaf is invariant under a pre-relation j if and only if it factors through the canonical projection of U onto the quotient sheaf U/R.

theorem invariant_iff_factors_through_quotientSheaf (j : PreRelation R U)
    (hX : Presheaf.IsSheaf (BigFppfOver.topology site S hS) X) (φ : U.left ⟶ X) :
    IsInvariant j φ ↔
      ∃ d : quotientSheaf j ⟶ baseSheaf hX, toQuotientSheaf j ≫ d.hom = φ

Tag 048G, a lemma

Tag 048G in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.overInvariantTarget, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GroupoidBaseChange.lean, line 76. The attribute's comment: “groupoid_over_x”.

Stacks 048G. A morphism out of the object space of a groupoid in algebraic spaces which is invariant under the pre-relation of the groupoid makes the groupoid a groupoid over its target: the object and arrow spaces, the source, the target and the composition are unchanged, and the new structure morphism on objects is the invariant morphism itself.

noncomputable def overInvariantTarget (G : GroupoidInAlgebraicSpaces C S hS B)
    {X : AlgebraicSpaces C S hS} (XtoB : X ⟶ B) (φ : G.objects ⟶ X)
    (_hφB : φ ≫ XtoB = G.objectsToBase)
    (hφ : Space.IsInvariant (Space.groupoidPreRelation G) φ.hom) :
    { H : GroupoidInAlgebraicSpaces C S hS X //
      H.toGroupoidInFunctors = G.toGroupoidInFunctors ∧
      ∃ hobj : H.objects = G.objects, eqToHom hobj.symm ≫ H.objectsToBase = φ }

AlgebraicGeometry.GroupoidInAlgebraicSpaces.baseChangedPreRelation_isBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GroupoidBaseChange.lean, line 214. The attribute's comment: “base_changed_groupoid_relation”.

Stacks 048G. The base change of the pre-relation of a groupoid in algebraic spaces along a morphism to an invariant target is the pre-relation of the base change of the groupoid over that target: the object and the arrow spaces agree, canonically through the two projections of the pullbacks, and the identifications intertwine the source and the target maps.

theorem baseChangedPreRelation_isBaseChange (G : GroupoidInAlgebraicSpaces C S hS B)
    {X X' : AlgebraicSpaces C S hS} (XtoB : X ⟶ B) (φ : G.objects ⟶ X)
    (hφB : φ ≫ XtoB = G.objectsToBase)
    (hφ : Space.IsInvariant (Space.groupoidPreRelation G) φ.hom)
    (f : X' ⟶ X) :
    let H := (overInvariantTarget G XtoB φ hφB hφ).val
    let bc := Space.baseChange H f
    let j := Space.groupoidPreRelation G
    let j' := (Space.baseChangedPreRelation j φ.hom f.hom hφ).val
    ∃ (hobj : H.objects = G.objects) (harr : H.arrows = G.arrows)
      (α : (Space.baseChangedObject (U := Over.mk G.objectsToBase.hom) φ.hom f.hom).left ≅
          bc.groupoid.objects.obj)
      (β : (Space.baseChangedArrows j φ.hom f.hom).left ≅ bc.groupoid.arrows.obj),
      (α.hom ≫ bc.groupoid.objectsToBase.hom = pullback.fst f.hom φ.hom) ∧
      (β.hom ≫ bc.groupoid.arrowsToBase.hom =
        pullback.fst f.hom (j.target.left ≫ φ.hom)) ∧
      (α.hom ≫ bc.projection.mapObjects ≫ (eqToHom hobj).hom =
        pullback.snd f.hom φ.hom) ∧
      (β.hom ≫ bc.projection.mapArrows ≫ (eqToHom harr).hom =
        pullback.snd f.hom (j.target.left ≫ φ.hom)) ∧
      (j'.source.left ≫ α.hom = β.hom ≫ bc.groupoid.source.hom) ∧
      (j'.target.left ≫ α.hom = β.hom ≫ bc.groupoid.target.hom)

AlgebraicGeometry.Space.exists_inducedAction_of_baseChangedPreRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/InducedGroupAction.lean, line 75. The attribute's comment: “induced_group_action”.

An invariant base change of an action pre-relation is again an action pre-relation. The comparison of arrow spaces respects the original arrows and both endpoints, while the induced action fixes the new-base coordinate.

theorem exists_inducedAction_of_baseChangedPreRelation
    (hsource : j.source = snd G U) (htarget : j.target = γ[G,U])
    (hφ : IsInvariant j φ) :
    ∃ action : ModObj G (baseChangedObject φ f),
      letI : ModObj G (baseChangedObject φ f) := action
      let U' := baseChangedObject φ f
      let R' := baseChangedArrows j φ f
      let j' := (baseChangedPreRelation j φ f hφ).val
      let q : U' ⟶ U := Over.homMk (pullback.snd f φ) (by rfl)
      let toOriginal : G ⊗ U' ⟶ G ⊗ U :=
        lift (fst G U') (snd G U' ≫ q)
      ((γ[G, U']).left ≫ pullback.fst f φ =
        (snd G U').left ≫ pullback.fst f φ) ∧
      (γ[G, U'] ≫ q = toOriginal ≫ γ[G,U]) ∧
    ∃ e : G ⊗ U' ≅ R',
        (e.hom.left ≫ pullback.snd f (j.target.left ≫ φ) = toOriginal.left) ∧
        (e.hom ≫ j'.source = snd G U') ∧
        (e.hom ≫ j'.target = γ[G, U'])

AlgebraicGeometry.Space.baseChangedPreRelation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/InvariantBaseChange.lean, line 134. The attribute's comment: “base_changed_pre_relation”.

Stacks 048G and Stacks 048H. The canonical pre-relation on the base changes of the object and of the arrow space of an invariant pre-relation. Its target and source maps are fixed by their composites with the two projections of the pullbacks: both preserve the component in X', and on the component in U they are the target and the source of j.

noncomputable def baseChangedPreRelation (j : PreRelation R U) (φ : U.left ⟶ X) (f : X' ⟶ X)
    (hφ : IsInvariant j φ) :
    { j' : PreRelation (baseChangedArrows j φ f) (baseChangedObject φ f) //
      ((j'.target.left ≫ pullback.fst f φ =
          pullback.fst f (j.target.left ≫ φ)) ∧
        (j'.target.left ≫ pullback.snd f φ =
          pullback.snd f (j.target.left ≫ φ) ≫ j.target.left)) ∧
      ((j'.source.left ≫ pullback.fst f φ =
          pullback.fst f (j.target.left ≫ φ)) ∧
        (j'.source.left ≫ pullback.snd f φ =
          pullback.snd f (j.target.left ≫ φ) ≫ j.source.left)) }

AlgebraicGeometry.Space.isPreEquivalenceRelation_baseChangedPreRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/InvariantBaseChange.lean, line 319. The attribute's comment: “pre_equivalence_preserved”.

Stacks 048G. Base change along an invariant morphism preserves the pointwise equivalence property of a pre-relation.

theorem isPreEquivalenceRelation_baseChangedPreRelation (j : PreRelation R U)
    (φ : U.left ⟶ X) (f : X' ⟶ X) (hφ : IsInvariant j φ)
    (hj : IsPreEquivalenceRelation j) :
    IsPreEquivalenceRelation (baseChangedPreRelation j φ f hφ).val

AlgebraicGeometry.Space.mono_baseChangedPreRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/InvariantBaseChange.lean, line 332. The attribute's comment: “relation_preserved”.

Stacks 048G. Base change along an invariant morphism preserves relations, that is monomorphy of the map to the product.

theorem mono_baseChangedPreRelation (j : PreRelation R U) (φ : U.left ⟶ X) (f : X' ⟶ X)
    (hφ : IsInvariant j φ) [Mono j] :
    Mono (baseChangedPreRelation j φ f hφ).val

AlgebraicGeometry.Space.isEquivalenceRelation_baseChangedPreRelation, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/InvariantBaseChange.lean, line 344. The attribute's comment: “equivalence_preserved”.

Stacks 048G. Base change along an invariant morphism preserves equivalence relations: the base-changed pre-relation of an invariant equivalence relation is again an internal categorical equivalence relation.

instance isEquivalenceRelation_baseChangedPreRelation (j : PreRelation R U) (φ : U.left ⟶ X)
    (f : X' ⟶ X) (hφ : IsInvariant j φ)
    [IsEquivalenceRelation j.target j.source] :
    IsEquivalenceRelation
      (PreRelation.target (baseChangedPreRelation j φ f hφ).val)
      (PreRelation.source (baseChangedPreRelation j φ f hφ).val)

Tag 048H, a definition

Tag 048H in the Stacks Project.

AlgebraicGeometry.Space.baseChangedPreRelation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/InvariantBaseChange.lean, line 134. The attribute's comment: “base change of the pre-relation”.

Stacks 048G and Stacks 048H. The canonical pre-relation on the base changes of the object and of the arrow space of an invariant pre-relation. Its target and source maps are fixed by their composites with the two projections of the pullbacks: both preserve the component in X', and on the component in U they are the target and the source of j.

noncomputable def baseChangedPreRelation (j : PreRelation R U) (φ : U.left ⟶ X) (f : X' ⟶ X)
    (hφ : IsInvariant j φ) :
    { j' : PreRelation (baseChangedArrows j φ f) (baseChangedObject φ f) //
      ((j'.target.left ≫ pullback.fst f φ =
          pullback.fst f (j.target.left ≫ φ)) ∧
        (j'.target.left ≫ pullback.snd f φ =
          pullback.snd f (j.target.left ≫ φ) ≫ j.target.left)) ∧
      ((j'.source.left ≫ pullback.fst f φ =
          pullback.fst f (j.target.left ≫ φ)) ∧
        (j'.source.left ≫ pullback.snd f φ =
          pullback.snd f (j.target.left ≫ φ) ≫ j.source.left)) }

Declarations registered for the tag:

• AlgebraicGeometry.Space.IsFlat, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/InvariantBaseChange.lean, line 360 (StacksFrontier): “flat base change”.

Tag 0DTF, a lemma

Tag 0DTF in the Stacks Project.

AlgebraicGeometry.Space.quotientSheaf_isPullback_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/QuotientSheafBaseChange.lean, line 250.

Stacks 0DTF. The quotient sheaf of the base change of an invariant pre-relation along f : X' ⟶ X is the fibre product of X' and the original quotient sheaf over X. The three canonical maps are specified by their composites with the quotient projections.

theorem quotientSheaf_isPullback_baseChange (j : PreRelation R U)
    (hX : Presheaf.IsSheaf (BigFppfOver.topology site S hS) X)
    (hX' : Presheaf.IsSheaf (BigFppfOver.topology site S hS) X')
    (φ : U.left ⟶ X) (f : X' ⟶ X) (hφ : IsInvariant j φ) :
    let j' := (baseChangedPreRelation j φ f hφ).val
    ∃ (qToX : quotientSheaf j ⟶ baseSheaf hX)
      (q'ToX' : quotientSheaf j' ⟶ baseSheaf hX')
      (q'ToQ : quotientSheaf j' ⟶ quotientSheaf j),
      (toQuotientSheaf j ≫ qToX.hom = φ) ∧
      (toQuotientSheaf j' ≫ q'ToX'.hom = pullback.fst f φ) ∧
      (toQuotientSheaf j' ≫ q'ToQ.hom = pullback.snd f φ ≫ toQuotientSheaf j) ∧
      IsPullback q'ToX' q'ToQ ⟨f⟩ qToX

Tag 0DTG, a lemma

Tag 0DTG in the Stacks Project.

AlgebraicGeometry.Stack.baseChangeQuotientStackSquare_isTwoFibreProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/BaseChangeQuotientStackComparisonFibreFull.lean, line 356.

Stacks 0DTG, the 2-fibre product. For a groupoid in algebraic spaces (U, R, s, t, c) over an algebraic space B over a scheme S of a big fppf site, an R-invariant morphism φ : U ⟶ X of algebraic spaces over B and a morphism g : X' ⟶ X of algebraic spaces over B, the 2-commutative square

[U'/R'] ---> [U/R]
  |            |
  v            v
 𝒮_{X'} ---> 𝒮_X

of AlgebraicGeometry.Stack.baseChangeQuotientStackSquare is a 2-fibre product (Stacks 003Q), where (U', R', s', t', c') is the base change of Stacks 048G.

Its comparison 1-morphism is faithful by AlgebraicGeometry.Stack.faithful_comparison, locally essentially surjective on fibres by AlgebraicGeometry.Stack.locallyEssSurjOnFibers_baseChangeQuotientStackComparison and full by AlgebraicGeometry.Stack.full_baseChangeQuotientStackComparison.

noncomputable def baseChangeQuotientStackSquare_isTwoFibreProduct :
    Bicategory.IsTwoFibreProduct
      (baseChangeQuotientStackSquare.{u, w} G XtoB X'toB g hg φ hφB hφ)

AlgebraicGeometry.Stack.baseChangeQuotientStackSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/BaseChangeQuotientStackSquare.lean, line 257. The attribute's comment: “the displayed square and its 2-commutativity”.

Stacks 0DTG, the displayed square. For a groupoid in algebraic spaces (U, R, s, t, c) over an algebraic space B over a scheme S of a big fppf site, an R-invariant morphism φ : U ⟶ X of algebraic spaces over B and a morphism g : X' ⟶ X of algebraic spaces over B, the square

[U'/R'] ---> [U/R]
  |            |
  v            v
 𝒮_{X'} ---> 𝒮_X

of stacks in groupoids over the big fppf site 2-commutes, where (U', R', s', t', c') is the base change of Stacks 048G. It is a 2-commutative diagram over the cospan in the sense of Stacks 003O, with its filling 2-isomorphism an identity.

The further assertion of Stacks 0DTG, that this square is a 2-fibre product, is AlgebraicGeometry.Stack.baseChangeQuotientStackSquare_isTwoFibreProduct; hence the qualifier on the tag here.

noncomputable def baseChangeQuotientStackSquare :
    let J := BigFppfOver.topology C S hS
    let Q : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨quotientStack (invariantTargetGroupoid G XtoB φ hφB hφ),
        isStackInGroupoids_quotientStack _⟩
    let SX : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨liftedFibredCategory X, isStackInGroupoids_liftedFibredCategory X⟩
    let SX' : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨liftedFibredCategory X', isStackInGroupoids_liftedFibredCategory X'⟩
    Bicategory.TwoCommSq
      (Bicategory.InducedBicategory.mkHom
        (liftedQuotientStackToBase (invariantTargetGroupoid G XtoB φ hφB hφ)) : Q ⟶ SX)
      (Bicategory.InducedBicategory.mkHom (liftedAssociatedMap g) : SX' ⟶ SX)

Sources

• Section 83.3, Tag 048D
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsInvariant · AlgebraicGeometry.Space.IsGroupInvariant · AlgebraicGeometry.Space.invariant_iff_factors_through_quotientSheaf · AlgebraicGeometry.GroupoidInAlgebraicSpaces.overInvariantTarget · AlgebraicGeometry.GroupoidInAlgebraicSpaces.baseChangedPreRelation_isBaseChange · AlgebraicGeometry.Space.exists_inducedAction_of_baseChangedPreRelation · AlgebraicGeometry.Space.baseChangedPreRelation · AlgebraicGeometry.Space.isPreEquivalenceRelation_baseChangedPreRelation

Section83.4 Categorical quotients#

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

Tag 048J, a definition

Tag 048J in the Stacks Project.

AlgebraicGeometry.Space.IsCategoricalQuotient, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotient.lean, line 57. The attribute's comment: “part (1): algebraic spaces”.

A morphism φ : U ⟶ X of algebraic spaces over B is a categorical quotient of a pre-relation j when it is invariant under j and every invariant morphism out of U factors uniquely through it.

noncomputable abbrev IsCategoricalQuotient {R U X : Over B} (j : PreRelation R U)
    (φ : U ⟶ X) : Prop

AlgebraicGeometry.Space.IsCategoricalQuotientIn, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotient.lean, line 67. The attribute's comment: “part (2): full subcategory”.

A morphism φ : U ⟶ X is a categorical quotient in the full subcategory cut out by an object property P when R, U and X lie in it and the universal property of a categorical quotient holds against the objects of P.

noncomputable abbrev IsCategoricalQuotientIn (P : ObjectProperty (Over B)) {R U X : Over B}
    (j : PreRelation R U) (φ : U ⟶ X) : Prop

AlgebraicGeometry.Space.IsCategoricalQuotientInSchemes, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotient.lean, line 77. The attribute's comment: “part (3): schemes”.

A morphism φ : U ⟶ X of schemes over T is a categorical quotient of a pre-relation of schemes when it equalizes the target and the source of the pre-relation and every morphism out of U which does so factors uniquely through it.

noncomputable abbrev IsCategoricalQuotientInSchemes {T : Scheme.{u}} {R U X : Over T}
    (j : Stacks.Groupoids.PreRelation R U) (φ : U ⟶ X) : Prop

Tag 048K, a lemma

Tag 048K in the Stacks Project.

AlgebraicGeometry.Space.categoricalQuotient_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotient.lean, line 105. The attribute's comment: “algebraic spaces over the base”.

Two categorical quotients of a pre-relation of algebraic spaces over B are uniquely isomorphic over B, compatibly with their quotient maps.

theorem categoricalQuotient_unique {R U X Y : Over B} (j : PreRelation R U) (φ : U ⟶ X)
    (ψ : U ⟶ Y) (hφ : IsCategoricalQuotient j φ) (hψ : IsCategoricalQuotient j ψ) :
    ∃! e : X ≅ Y, φ ≫ e.hom = ψ

AlgebraicGeometry.Space.categoricalQuotientIn_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotient.lean, line 114. The attribute's comment: “full subcategories”.

Two categorical quotients of a pre-relation in the full subcategory cut out by an object property are uniquely isomorphic within that subcategory, compatibly with their quotient maps.

theorem categoricalQuotientIn_unique (P : ObjectProperty (Over B)) {R U X Y : Over B}
    (j : PreRelation R U) (φ : U ⟶ X) (ψ : U ⟶ Y)
    (hφ : IsCategoricalQuotientIn P j φ) (hψ : IsCategoricalQuotientIn P j ψ) :
    ∃! e : X ≅ Y, φ ≫ e.hom = ψ

Tag 049V, an example

Tag 049V in the Stacks Project.

AlgebraicGeometry.Space.IsCategoricalQuotient, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotient.lean, line 57. The attribute's comment: “items (2)-(5): the separated, quasi-separated, locally separated and decent”.

A morphism φ : U ⟶ X of algebraic spaces over B is a categorical quotient of a pre-relation j when it is invariant under j and every invariant morphism out of U factors uniquely through it.

noncomputable abbrev IsCategoricalQuotient {R U X : Over B} (j : PreRelation R U)
    (φ : U ⟶ X) : Prop

AlgebraicGeometry.Space.IsCategoricalQuotientIn, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotient.lean, line 67. The attribute's comment: “items (2)-(5): the separated, quasi-separated, locally separated and decent”.

A morphism φ : U ⟶ X is a categorical quotient in the full subcategory cut out by an object property P when R, U and X lie in it and the universal property of a categorical quotient holds against the objects of P.

noncomputable abbrev IsCategoricalQuotientIn (P : ObjectProperty (Over B)) {R U X : Over B}
    (j : PreRelation R U) (φ : U ⟶ X) : Prop

AlgebraicGeometry.Space.IsCategoricalQuotientInSchemes, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotient.lean, line 77. The attribute's comment: “items (2)-(5): the separated, quasi-separated, locally separated and decent”.

A morphism φ : U ⟶ X of schemes over T is a categorical quotient of a pre-relation of schemes when it equalizes the target and the source of the pre-relation and every morphism out of U which does so factors uniquely through it.

noncomputable abbrev IsCategoricalQuotientInSchemes {T : Scheme.{u}} {R U X : Over T}
    (j : Stacks.Groupoids.PreRelation R U) (φ : U ⟶ X) : Prop

Tag 048L, a definition

Tag 048L in the Stacks Project.

AlgebraicGeometry.Space.IsUniversalCategoricalQuotientIn, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/QuotientProperties.lean, line 236. The attribute's comment: “part (1): universal categorical quotient”.

Stacks 048L, part (1). An R-invariant morphism φ : U ⟶ X is a universal categorical quotient in a full subcategory P of the algebraic spaces over B, closed under fibre products, when R, U and X lie in P and for every morphism f : X' ⟶ X of P the projection X' ×_X U ⟶ X' is the categorical quotient in P of the base change of j along f.

abbrev IsUniversalCategoricalQuotientIn {B : AlgebraicSpaces site S hS}
    (P : ObjectProperty (Over B)) [P.IsClosedUnderLimitsOfShape WalkingCospan]
    {R U X : Over B} (j : PreRelation R U) (φ : U ⟶ X) (hφ : IsInvariant j φ.left) : Prop

AlgebraicGeometry.Space.IsUniformCategoricalQuotientIn, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/QuotientProperties.lean, line 249. The attribute's comment: “part (2): uniform categorical quotient”.

Stacks 048L, part (2). An R-invariant morphism φ : U ⟶ X is a uniform categorical quotient in a full subcategory P of the algebraic spaces over B, closed under fibre products, when R, U and X lie in P and for every flat morphism f : X' ⟶ X of P the projection X' ×_X U ⟶ X' is the categorical quotient in P of the base change of j along f.

abbrev IsUniformCategoricalQuotientIn {B : AlgebraicSpaces site S hS}
    (P : ObjectProperty (Over B)) [P.IsClosedUnderLimitsOfShape WalkingCospan]
    {R U X : Over B} (j : PreRelation R U) (φ : U ⟶ X) (hφ : IsInvariant j φ.left) : Prop

Tag 049W, a lemma

Tag 049W in the Stacks Project.

AlgebraicGeometry.Space.isReduced_of_isCategoricalQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotientReduced.lean, line 192. The attribute's comment: “algebraic spaces”.

Stacks 049W, for algebraic spaces over the base. A categorical quotient of a reduced algebraic space is reduced. Unconditional.

theorem isReduced_of_isCategoricalQuotient
    {R U X : Over Base} (j : PreRelation R U) (φ : U ⟶ X)
    (hφ : IsCategoricalQuotient j φ)
    (hU : HasEtaleLocalProperty B S hS U.left.obj (fun Y : Scheme.{u} => IsReduced Y)) :
    HasEtaleLocalProperty B S hS X.left.obj (fun Y : Scheme.{u} => IsReduced Y)

AlgebraicGeometry.Space.isReduced_of_isCategoricalQuotientInSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotientReduced.lean, line 206. The attribute's comment: “separated algebraic spaces”.

Stacks 049W, for separated algebraic spaces. A categorical quotient in the full subcategory of separated algebraic spaces, of a reduced algebraic space, is reduced.

The reduction of the target is separated because its inclusion is a closed immersion, hence a separated morphism by Stacks 04CH, and the target is separated — Stacks 04ZH, part (1).

theorem isReduced_of_isCategoricalQuotientInSeparated
    (hZ : B.Contains (⊤_ Scheme.{u}))
    {R U X : Over Base} (j : PreRelation R U) (φ : U ⟶ X)
    (hφ : IsCategoricalQuotientIn
      (fun Y : Over Base => IsAbsolutelySeparated B S hS hZ Y.left.obj) j φ)
    (hU : HasEtaleLocalProperty B S hS U.left.obj (fun Y : Scheme.{u} => IsReduced Y)) :
    HasEtaleLocalProperty B S hS X.left.obj (fun Y : Scheme.{u} => IsReduced Y)

AlgebraicGeometry.Space.isReduced_of_isCategoricalQuotientInQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotientReduced.lean, line 228. The attribute's comment: “quasi-separated algebraic spaces”.

Stacks 049W, for quasi-separated algebraic spaces. A categorical quotient in the full subcategory of quasi-separated algebraic spaces, of a reduced algebraic space, is reduced.

The inclusion of the reduction of the target is a closed immersion, hence separated by Stacks 04CH and so quasi-separated by Stacks 03KK; Stacks 04ZH, part (2) then transfers quasi-separatedness from the target.

theorem isReduced_of_isCategoricalQuotientInQuasiSeparated
    (hZ : B.Contains (⊤_ Scheme.{u}))
    {R U X : Over Base} (j : PreRelation R U) (φ : U ⟶ X)
    (hφ : IsCategoricalQuotientIn
      (fun Y : Over Base => IsAbsolutelyQuasiSeparated B S hS hZ Y.left.obj) j φ)
    (hU : HasEtaleLocalProperty B S hS U.left.obj (fun Y : Scheme.{u} => IsReduced Y)) :
    HasEtaleLocalProperty B S hS X.left.obj (fun Y : Scheme.{u} => IsReduced Y)

AlgebraicGeometry.Space.isReduced_of_isCategoricalQuotientInLocallySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotientReduced.lean, line 251. The attribute's comment: “locally separated algebraic spaces”.

Stacks 049W, for locally separated algebraic spaces. A categorical quotient in the full subcategory of locally separated algebraic spaces, of a reduced algebraic space, is reduced.

The inclusion of the reduction of the target is a closed immersion, hence separated by Stacks 04CH and so locally separated by Stacks 03KK; Stacks 04ZH, part (3) then transfers local separatedness from the target.

theorem isReduced_of_isCategoricalQuotientInLocallySeparated
    (hZ : B.Contains (⊤_ Scheme.{u}))
    {R U X : Over Base} (j : PreRelation R U) (φ : U ⟶ X)
    (hφ : IsCategoricalQuotientIn
      (fun Y : Over Base => IsAbsolutelyLocallySeparated B S hS hZ Y.left.obj) j φ)
    (hU : HasEtaleLocalProperty B S hS U.left.obj (fun Y : Scheme.{u} => IsReduced Y)) :
    HasEtaleLocalProperty B S hS X.left.obj (fun Y : Scheme.{u} => IsReduced Y)

AlgebraicGeometry.Space.isReduced_of_isCategoricalQuotientInDecent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotientReduced.lean, line 274. The attribute's comment: “decent algebraic spaces”.

Stacks 049W, for decent algebraic spaces. A categorical quotient in the full subcategory of decent algebraic spaces, of a reduced algebraic space, is reduced.

The reduction of the target is decent because the inclusion of a closed subspace is representable and decency passes to the source of a representable morphism — Stacks 03KF for property (γ), which is condition (4) of Stacks 03JV.

theorem isReduced_of_isCategoricalQuotientInDecent
    {R U X : Over Base} (j : PreRelation R U) (φ : U ⟶ X)
    (hφ : IsCategoricalQuotientIn
      (fun Y : Over Base => IsDecentSpace B S hS Y.left.obj) j φ)
    (hU : HasEtaleLocalProperty B S hS U.left.obj (fun Y : Scheme.{u} => IsReduced Y)) :
    HasEtaleLocalProperty B S hS X.left.obj (fun Y : Scheme.{u} => IsReduced Y)

AlgebraicGeometry.Space.isReduced_of_isCategoricalQuotientInSchemes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CategoricalQuotientReduced.lean, line 294. The attribute's comment: “schemes”. References: SGA 3 VIB (9.2), “more general”.

Stacks 049W, for schemes. A categorical quotient in the category of schemes over a base scheme, of a reduced scheme, is reduced.

Unconditional: the reduction of a scheme is its closed subscheme cut out by the nilradical, and a morphism from a reduced scheme factors uniquely through it by Stacks 0356.

theorem isReduced_of_isCategoricalQuotientInSchemes
    {T : Scheme.{u}} {R U X : Over T} (j : Stacks.Groupoids.PreRelation R U)
    (φ : U ⟶ X) (hφ : IsCategoricalQuotientInSchemes j φ)
    (hU : IsReduced U.left) : IsReduced X.left

Sources

• Section 83.4, Tag 048I
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsCategoricalQuotient · AlgebraicGeometry.Space.IsCategoricalQuotientIn · AlgebraicGeometry.Space.IsCategoricalQuotientInSchemes · AlgebraicGeometry.Space.categoricalQuotient_unique · AlgebraicGeometry.Space.categoricalQuotientIn_unique · AlgebraicGeometry.Space.IsUniversalCategoricalQuotientIn · AlgebraicGeometry.Space.IsUniformCategoricalQuotientIn · AlgebraicGeometry.Space.isReduced_of_isCategoricalQuotient

Section83.5 Quotients as orbit spaces#

Section 83.5 of the Stacks Project, Tag 048M. 21 tags here are carried by 53 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 048N, a definition

Tag 048N in the Stacks Project.

AlgebraicGeometry.Space.PreRelation.pointOrbit, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/PointOrbits.lean, line 81.

Stacks 048N. The orbit of a point of |U| under a pre-relation j : R ⟶ U ×_Z U: the set of points joined to it by a finite chain of arrows of j, traversed in either direction, with stationary steps allowed.

noncomputable abbrev PreRelation.pointOrbit (j : PreRelation R U)
    (u : points B S hS U.left) : Set (points B S hS U.left)

Tag 048O, a lemma

Tag 048O in the Stacks Project.

AlgebraicGeometry.Space.PreRelation.pointOrbit_eq_targets_of_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/PointOrbits.lean, line 90.

Stacks 048O. For a pre-equivalence relation an orbit is cut out by a single arrow: it consists of the targets of the arrows of the pre-relation whose source is the given point.

theorem PreRelation.pointOrbit_eq_targets_of_source (j : PreRelation R U)
    (hj : IsPreEquivalenceRelation j) (u : points B S hS U.left) :
    j.pointOrbit u =
      {u' | ∃ r : points B S hS R.left,
        pointsMap B S hS R.left j.source.left r = u ∧
          pointsMap B S hS R.left j.target.left r = u'}

Tag 048P, a lemma

Tag 048P in the Stacks Project.

AlgebraicGeometry.Space.pointsMap_eq_of_mem_pointOrbit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/PointOrbits.lean, line 119.

Stacks 048P. A morphism out of U which is invariant under a pre-relation takes the same value at any two points in one orbit.

theorem pointsMap_eq_of_mem_pointOrbit (j : PreRelation R U)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (φ : U.left ⟶ X)
    (hφ : IsInvariant j φ)
    {x y : points B S hS U.left} (hy : y ∈ j.pointOrbit x) :
    pointsMap B S hS U.left φ x = pointsMap B S hS U.left φ y

Tag 048Q, a definition

Tag 048Q in the Stacks Project.

AlgebraicGeometry.Space.PreRelation.WeaklyEquivalent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/GeometricOrbits.lean, line 76. The attribute's comment: “part (1): weak equivalence”.

Two points of U over a field-valued point p of Z are weakly equivalent when they are joined by a finite chain of arrows of the pre-relation over the field of p, traversed in either direction and with stationary steps allowed.

abbrev WeaklyEquivalent (j : PreRelation R U) (p : FieldValuedPoint B S hS Z)
    (x y : TestPoint (p.siteObject B S hS Z) (yonedaEquiv.symm p.value) U) : Prop

AlgebraicGeometry.Space.PreRelation.Equivalent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/GeometricOrbits.lean, line 84. The attribute's comment: “part (2): equivalence after extension”.

Two points of U over a field-valued point p of Z are equivalent when their restrictions to some extension of the field of p are weakly equivalent.

abbrev Equivalent (j : PreRelation R U) (p : FieldValuedPoint B S hS Z)
    (x y : TestPoint (p.siteObject B S hS Z) (yonedaEquiv.symm p.value) U) : Prop

AlgebraicGeometry.Space.PreRelation.weakOrbit, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/GeometricOrbits.lean, line 94. The attribute's comment: “part (3): weak orbit”.

The weak orbit of a point of U over a geometric point of Z: its class for weak equivalence over the given algebraically closed field.

abbrev weakOrbit (j : PreRelation R U) (p : GeometricPoint B S hS Z)
    (x : TestPoint (p.val.siteObject B S hS Z) (yonedaEquiv.symm p.val.value) U) :
    Set (TestPoint (p.val.siteObject B S hS Z) (yonedaEquiv.symm p.val.value) U)

AlgebraicGeometry.Space.PreRelation.orbit, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/GeometricOrbits.lean, line 102. The attribute's comment: “part (4): orbit”.

The orbit of a point of U over a geometric point of Z: its class for equivalence, that is after allowing one extension of the field.

abbrev orbit (j : PreRelation R U) (p : GeometricPoint B S hS Z)
    (x : TestPoint (p.val.siteObject B S hS Z) (yonedaEquiv.symm p.val.value) U) :
    Set (TestPoint (p.val.siteObject B S hS Z) (yonedaEquiv.symm p.val.value) U)

Tag 048R, a lemma

Tag 048R in the Stacks Project.

AlgebraicGeometry.Space.PreRelation.weakOrbit_eq_targets, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/GeometricOrbits.lean, line 115. The attribute's comment: “weak orbit”.

For a pre-equivalence relation the weak orbit of a point is cut out by a single arrow: it consists of the targets of the arrows whose source is that point.

theorem weakOrbit_eq_targets (j : PreRelation R U) (hj : IsPreEquivalenceRelation j)
    (p : GeometricPoint B S hS Z)
    (x : TestPoint (p.val.siteObject B S hS Z) (yonedaEquiv.symm p.val.value) U) :
    j.weakOrbit p x = {y | j.Rel (yonedaEquiv.symm p.val.value) y x}

AlgebraicGeometry.Space.PreRelation.orbit_eq_targets_after_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/GeometricOrbits.lean, line 125. The attribute's comment: “orbit”.

For a pre-equivalence relation the orbit of a point is cut out by a single arrow over some extension of the field of the geometric point.

theorem orbit_eq_targets_after_extension (j : PreRelation R U)
    (hj : IsPreEquivalenceRelation j) (p : GeometricPoint B S hS Z)
    (x : TestPoint (p.val.siteObject B S hS Z) (yonedaEquiv.symm p.val.value) U) :
    j.orbit p x =
      {y | ∃ (q : FieldValuedPoint B S hS Z)
          (f : q.siteObject B S hS Z ⟶ p.val.siteObject B S hS Z),
          Z.map f.op p.val.value = q.value ∧
            ∃ x' y' : TestPoint (q.siteObject B S hS Z) (yonedaEquiv.symm q.value) U,
              x'.1 = yoneda.map f ≫ x.1 ∧ y'.1 = yoneda.map f ≫ y.1 ∧
                j.Rel (yonedaEquiv.symm q.value) y' x'}

Tag 048S, an equation

Tag 048S in the Stacks Project.

AlgebraicGeometry.Space.flippedRelation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvariantMorphisms.lean, line 80. The attribute's comment: “flip map”.

The flipped arrow of a pre-relation, r ↦ (s(r), t(r)): the map to U ×_B U that reverses each arrow of j.

noncomputable def flippedRelation {R U : Over B} (j : PreRelation R U) : R ⟶ U ⨯ U

AlgebraicGeometry.Space.composedRelation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvariantMorphisms.lean, line 86. The attribute's comment: “composable-pair map”.

The endpoint map on composable pairs, (r, r') ↦ (t(r), s(r')): the map to U ×_B U recording the outer endpoints of a pair of arrows of j that compose.

noncomputable def composedRelation {R U : Over B} (j : PreRelation R U) :
    pullback j.source j.target ⟶ U ⨯ U

Declarations registered for the tag:

• CategoryTheory.Limits.diag registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/InvariantMorphisms.lean, line 71 (StacksFrontier): “diagonal map”. References: EGA I (10.15.1); EGA I (5.3.1); EGA IV (17.13.9), “binary diagonal”; SGA 4 IV (5.11.1).

Tag 048T, a lemma

Tag 048T in the Stacks Project.

AlgebraicGeometry.Space.allPathsRelation_source_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GeneratedRelationFiniteType.lean, line 127. The attribute's comment: “part (5): locally of finite type”.

Stacks 048T, part (5). The source map of the relation of all finite paths is locally of finite type when both endpoint maps of the original pre-relation are.

theorem allPathsRelation_source_locallyOfFiniteType (P : PathConstruction j)
    (hs : IsLocallyOfFiniteType site S hS j.source.left.hom)
    (ht : IsLocallyOfFiniteType site S hS j.target.left.hom) :
    IsLocallyOfFiniteType site S hS P.allPathsRelation.source.left.hom

AlgebraicGeometry.Space.allPathsRelation_target_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GeneratedRelationFiniteType.lean, line 142. The attribute's comment: “part (5): locally of finite type”.

Stacks 048T, part (5). The target map of the relation of all finite paths is locally of finite type when both endpoint maps of the original pre-relation are.

theorem allPathsRelation_target_locallyOfFiniteType (P : PathConstruction j)
    (hs : IsLocallyOfFiniteType site S hS j.source.left.hom)
    (ht : IsLocallyOfFiniteType site S hS j.target.left.hom) :
    IsLocallyOfFiniteType site S hS P.allPathsRelation.target.left.hom

AlgebraicGeometry.Space.isInvariant_allPathsRelation_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GeneratedRelationInvariance.lean, line 160. The attribute's comment: “part (1): invariance under the generated relation”.

Stacks 048T, part (1). A morphism out of U is invariant under a pre-relation exactly when it is invariant under the relation of all finite paths that the pre-relation generates.

The codomain is an arbitrary algebraic space over S; for a morphism φ of algebraic spaces over B take φ.left.

theorem isInvariant_allPathsRelation_iff (P : PathConstruction j) (φ : U.left ⟶ X) :
    IsInvariant P.allPathsRelation φ ↔ IsInvariant j φ

AlgebraicGeometry.Space.weakOrbit_allPathsRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GeneratedRelationOrbits.lean, line 184. The attribute's comment: “part (3): weak orbits are unchanged”.

Stacks 048T, part (3). The weak orbit of a point of U at a geometric point of B is unchanged when the pre-relation is replaced by the relation of all finite paths it generates.

theorem weakOrbit_allPathsRelation (p : GeometricPoint site S hS B.obj)
    (x : TestPoint p.val.siteObject (yonedaEquiv.symm p.val.value) ((overForgetSpace B).obj U)) :
    (presheafPreRelation P.allPathsRelation).weakOrbit p x =
      (presheafPreRelation j).weakOrbit p x

AlgebraicGeometry.Space.orbit_allPathsRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GeneratedRelationOrbits.lean, line 209. The attribute's comment: “part (4): orbits are unchanged”.

Stacks 048T, part (4). The orbit of a point of U at a geometric point of B is unchanged when the pre-relation is replaced by the relation of all finite paths it generates.

theorem orbit_allPathsRelation (p : GeometricPoint site S hS B.obj)
    (x : TestPoint p.val.siteObject (yonedaEquiv.symm p.val.value) ((overForgetSpace B).obj U)) :
    (presheafPreRelation P.allPathsRelation).orbit p x =
      (presheafPreRelation j).orbit p x

AlgebraicGeometry.Space.isPreEquivalenceRelation_allPathsRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GeneratedRelationPreEquivalence.lean, line 324. The attribute's comment: “the generated relation is a pre-equivalence relation”.

Stacks 048T. The relation generated by a pre-relation of algebraic spaces over B, whose arrows are the finite composable paths of original, identity and reversed arrows, is a pre-equivalence relation over B: on the points of every test scheme over B it induces an equivalence relation.

Reflexivity is witnessed by the identity arrow of a point, symmetry by the reverse of a path, and transitivity by the concatenation of two paths.

theorem isPreEquivalenceRelation_allPathsRelation (P : PathConstruction j) :
    IsPreEquivalenceRelation (presheafPreRelation P.allPathsRelation)

AlgebraicGeometry.Space.isIso_quotientSheafToAllPaths, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/GeneratedRelationQuotientSheaf.lean, line 231. The attribute's comment: “part (2): the quotient sheaf is unchanged”.

Stacks 048T, part (2). The canonical map of quotient sheaves U/R ⟶ U/R_∞, from the quotient by a pre-relation to the quotient by the relation of all the finite paths it generates, is an isomorphism.

theorem isIso_quotientSheafToAllPaths (P : PathConstruction j) :
    IsIso (quotientSheafToAllPaths P)

Tag 048U, a lemma

Tag 048U in the Stacks Project.

AlgebraicGeometry.Space.equivalent_iff_weaklyEquivalent_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/GeometricQuotient.lean, line 84. The attribute's comment: “finite_type_equivalence”.

Stacks 048U. For a pre-relation whose source and target are locally of finite type, two points of U over a geometric point of B are equivalent exactly when they are already weakly equivalent over the field of that geometric point: no extension of the field is needed.

theorem equivalent_iff_weaklyEquivalent_of_locallyOfFiniteType (j : PreRelation R U)
    (hs : IsLocallyOfFiniteType site S hS j.source.left.hom)
    (ht : IsLocallyOfFiniteType site S hS j.target.left.hom)
    (p : GeometricPoint site S hS B.obj)
    (x y : TestPoint p.val.siteObject (yonedaEquiv.symm p.val.value)
      ((overForgetSpace B).obj U)) :
    (presheafPreRelation j).Equivalent p.val x y ↔
      (presheafPreRelation j).WeaklyEquivalent p.val x y

AlgebraicGeometry.Space.orbit_eq_weakOrbit_of_large_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/LargeFields.lean, line 198. The attribute's comment: “large_field_orbits”.

Stacks 048U, part (2). Over a sufficiently large algebraically closed field the orbit of a point of U under a pre-relation is its weak orbit over the same field: no extension of the field is needed. The bound is on the relation generated by the pre-relation, and is uniform in the geometric point and in the point whose orbit is taken.

theorem orbit_eq_weakOrbit_of_large_field {j : PreRelation R U} (P : PathConstruction j)
    (p : GeometricPoint site S hS B.obj)
    (hp : IsLargeField site S hS P.allPaths.left.obj p.val.carrier)
    (x : TestPoint p.val.siteObject (yonedaEquiv.symm p.val.value)
      ((overForgetSpace B).obj U)) :
    (presheafPreRelation j).orbit p x = (presheafPreRelation j).weakOrbit p x

AlgebraicGeometry.Space.equivalent_iff_weaklyEquivalent_of_large_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/LargeFields.lean, line 213. The attribute's comment: “large_field_equivalence”.

Stacks 048U, part (2). Over a sufficiently large algebraically closed field, equivalence of two points of U under a pre-relation is their weak equivalence over the same field. The bound is on the relation generated by the pre-relation, and is uniform in the geometric point and in the pair of points.

theorem equivalent_iff_weaklyEquivalent_of_large_field {j : PreRelation R U}
    (P : PathConstruction j) (p : GeometricPoint site S hS B.obj)
    (hp : IsLargeField site S hS P.allPaths.left.obj p.val.carrier)
    (x y : TestPoint p.val.siteObject (yonedaEquiv.symm p.val.value)
      ((overForgetSpace B).obj U)) :
    (presheafPreRelation j).Equivalent p.val x y ↔
      (presheafPreRelation j).WeaklyEquivalent p.val x y

Tag 048V, a definition

Tag 048V in the Stacks Project.

AlgebraicGeometry.Space.IsSetTheoreticallyInvariant, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/OrbitSeparation.lean, line 68. The attribute's comment: “part (1): set-theoretic invariance”.

A morphism out of U is set-theoretically invariant under a pre-relation when it takes the same value at the two endpoints of every arrow of the pre-relation between points over an algebraically closed field.

abbrev IsSetTheoreticallyInvariant (j : PreRelation R U) (φ : U.left ⟶ X) : Prop

AlgebraicGeometry.Space.SeparatesOrbits, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/OrbitSeparation.lean, line 77. The attribute's comment: “part (2): separation of orbits”.

A morphism out of U separates the orbits of a pre-relation when it is set-theoretically invariant and two points over an algebraically closed field with the same image lie in one orbit.

abbrev SeparatesOrbits (j : PreRelation R U) (φ : U.left ⟶ X) : Prop

Tag 048W, a lemma

Tag 048W in the Stacks Project.

AlgebraicGeometry.Space.isSetTheoreticallyInvariant_iff_eq_of_mem_orbit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/InvarianceOnOrbits.lean, line 190.

A morphism from U to an algebraic space is set-theoretically invariant under a pre-relation if and only if, for every algebraically closed field over the base, the induced map on the points of U over that field is constant on the orbits of the pre-relation.

theorem isSetTheoreticallyInvariant_iff_eq_of_mem_orbit (hX : IsAlgebraicSpace B S hS X)
    (j : PreRelation R U) (φ : U.left ⟶ X) :
    IsSetTheoreticallyInvariant j φ ↔
      ∀ (p : GeometricPoint B S hS Z)
        (x y : TestPoint (p.val.siteObject B S hS Z) (yonedaEquiv.symm p.val.value) U),
        y ∈ j.orbit p x → x.1 ≫ φ = y.1 ≫ φ

Tag 048X, a lemma

Tag 048X in the Stacks Project.

AlgebraicGeometry.Space.isSetTheoreticallyInvariant_of_isInvariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/OrbitSeparation.lean, line 85.

A morphism which is invariant under a pre-relation is set-theoretically invariant.

theorem isSetTheoreticallyInvariant_of_isInvariant (j : PreRelation R U) (φ : U.left ⟶ X)
    (hφ : IsInvariant j φ) :
    IsSetTheoreticallyInvariant j φ

Tag 048Y, a lemma

Tag 048Y in the Stacks Project.

AlgebraicGeometry.Space.isInvariant_of_isSetTheoreticallyInvariant_of_reduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/ReducedRelation.lean, line 230.

Stacks 048Y. On a reduced relation space, set-theoretic invariance of a morphism to a locally separated target implies that the morphism is invariant under the pre-relation.

theorem isInvariant_of_isSetTheoreticallyInvariant_of_reduced {R U X : Over Z}
    (j : PreRelation R U)
    (φ : U ⟶ X) (hφ : IsSetTheoreticallyInvariant j φ.left)
    (hR : HasEtaleLocalProperty B S hS R.left (fun Y : Scheme.{u} ↦ IsReduced Y))
    (hX : IsLocallySeparated B S hS X.hom)
    (hXsheaf : Presheaf.IsSheaf (BigFppfOver.topology B S hS) X.left) :
    IsInvariant j φ.left

Tag 048Z, an example

Tag 048Z in the Stacks Project.

AlgebraicGeometry.Space.diskToInvolutionQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NonInvariantFormalDiskExample.lean, line 328. The attribute's comment: “the coordinate map to the quotient”.

Stacks 048Z. The morphism from the formal disk to the quotient of the affine line by the involution relation given by the power-series variable.

noncomputable def diskToInvolutionQuotient
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)] :
    yoneda.obj (siteFormalDisk k B hS hD) ⟶ (involutionQuotient k B hS).obj

AlgebraicGeometry.Space.diskToInvolutionQuotientNeg, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NonInvariantFormalDiskExample.lean, line 337. The attribute's comment: “the negated coordinate map to the quotient”.

Stacks 048Z. The morphism from the formal disk to the quotient of the affine line by the involution relation given by the negative of the power-series variable.

noncomputable def diskToInvolutionQuotientNeg
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)] :
    yoneda.obj (siteFormalDisk k B hS hD) ⟶ (involutionQuotient k B hS).obj

AlgebraicGeometry.Space.diskMaps_agree_on_fieldPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NonInvariantFormalDiskExample.lean, line 412. The attribute's comment: “agreement on field-valued points”.

Stacks 048Z. The two morphisms from the formal disk to the quotient agree after every field-valued point of the disk.

theorem diskMaps_agree_on_fieldPoints
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)]
    (K : Type u) [Field K] (hK : B.Contains (Spec (.of K)))
    (β : Spec (.of K) ⟶ Spec (.of k))
    (g : (Over.mk (ObjectProperty.homMk β : B.obj hK ⟶ B.obj hS) :
      BigFppfOver B (Spec (.of k)) hS) ⟶ siteFormalDisk k B hS hD) :
    yoneda.map g ≫ diskToInvolutionQuotient k B hS hD =
      yoneda.map g ≫ diskToInvolutionQuotientNeg k B hS hD

AlgebraicGeometry.Space.diskMaps_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NonInvariantFormalDiskExample.lean, line 563. The attribute's comment: “distinct morphisms”.

Stacks 048Z. Away from characteristic two, the two morphisms from the formal disk to the quotient are nevertheless distinct.

theorem diskMaps_ne (hchar : (2 : k) ≠ 0)
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)] :
    diskToInvolutionQuotient k B hS hD ≠ diskToInvolutionQuotientNeg k B hS hD

AlgebraicGeometry.Space.exists_setTheoreticallyInvariant_not_invariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NonInvariantFormalDiskExample.lean, line 618. The attribute's comment: “quasi-separatedness does not suffice”.

Stacks 048Z. Quasi-separatedness of the target cannot replace local separatedness in the criterion AlgebraicGeometry.Space.isInvariant_of_isSetTheoreticallyInvariant_of_reduced (Stacks 048Y): over a field in which two is invertible there is a pre-relation on a reduced algebraic space, with quasi-separated target, carrying a set-theoretically invariant morphism which is not invariant.

The relation is the formal disk, acting on itself by the identity and by negation of the coordinate, and the morphism is the coordinate map to the quotient of the affine line by the involution relation. Quasi-separatedness of that quotient is Stacks 02Z1, taken from AlgebraicGeometry.AffineLineInvolution.isAbsolutelyQuasiSeparated_involutionQuotient and converted to quasi-separatedness of the structure morphism by Stacks 073B part (2).

theorem exists_setTheoreticallyInvariant_not_invariant (hchar : (2 : k) ≠ 0)
    (hZ : B.Contains (⊤_ Scheme.{u}))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)] :
    ∃ (Z : (BigFppfOver B (Spec (.of k)) hS)ᵒᵖ ⥤ Type u) (R U X : Over Z)
      (j : PreRelation R U) (φ : U ⟶ X),
      HasEtaleLocalProperty B (Spec (.of k)) hS R.left (fun T : Scheme.{u} ↦ IsReduced T) ∧
        IsQuasiSeparated B (Spec (.of k)) hS X.hom ∧
        IsSetTheoreticallyInvariant j φ.left ∧ ¬ IsInvariant j φ.left

AlgebraicGeometry.Space.exists_agree_on_fieldPoints_ne_and_not_invariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NonInvariantFormalDiskExample.lean, line 755.

Stacks 048Z. Over a field in which two is invertible there are reduced quasi-separated algebraic spaces X, Y and two morphisms a, b : Y ⟶ X which agree on every field-valued point of Y yet are not equal; consequently quasi-separatedness of the target cannot replace local separatedness in the criterion AlgebraicGeometry.Space.isInvariant_of_isSetTheoreticallyInvariant_of_reduced (Stacks 048Y), because there is a pre-relation on a reduced algebraic space with quasi-separated target carrying a set-theoretically invariant morphism which is not invariant.

The spaces are Y = Spec k[[x]] and X = 𝔸¹_k/(Δ ⨿ {(x, -x) | x ≠ 0}), the algebraic space of Stacks 02Z1, and the two morphisms are the coordinate and its negative followed by the projection to the quotient. The pre-relation witnessing the second assertion is Y acting on itself by the identity and by negation of the coordinate.

theorem exists_agree_on_fieldPoints_ne_and_not_invariant (hchar : (2 : k) ≠ 0)
    (hZ : B.Contains (⊤_ Scheme.{u}))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hS) (Type u)] :
    (∃ (X Y : (BigFppfOver B (Spec (.of k)) hS)ᵒᵖ ⥤ Type u) (a b : Y ⟶ X),
        IsAlgebraicSpace B (Spec (.of k)) hS X ∧
        IsAlgebraicSpace B (Spec (.of k)) hS Y ∧
        HasEtaleLocalProperty B (Spec (.of k)) hS X (fun T : Scheme.{u} ↦ IsReduced T) ∧
        HasEtaleLocalProperty B (Spec (.of k)) hS Y (fun T : Scheme.{u} ↦ IsReduced T) ∧
        IsAbsolutelyQuasiSeparated B (Spec (.of k)) hS hZ X ∧
        IsAbsolutelyQuasiSeparated B (Spec (.of k)) hS hZ Y ∧
        (∀ (K : Type u) [Field K] (hK : B.Contains (Spec (.of K)))
            (β : Spec (.of K) ⟶ Spec (.of k))
            (g : yoneda.obj (Over.mk (ObjectProperty.homMk β : B.obj hK ⟶ B.obj hS) :
              BigFppfOver B (Spec (.of k)) hS) ⟶ Y),
          g ≫ a = g ≫ b) ∧
        a ≠ b) ∧
      ∃ (Z : (BigFppfOver B (Spec (.of k)) hS)ᵒᵖ ⥤ Type u) (R U X : Over Z)
        (j : PreRelation R U) (φ : U ⟶ X),
        HasEtaleLocalProperty B (Spec (.of k)) hS R.left
            (fun T : Scheme.{u} ↦ IsReduced T) ∧
          IsQuasiSeparated B (Spec (.of k)) hS X.hom ∧
          IsSetTheoreticallyInvariant j φ.left ∧ ¬ IsInvariant j φ.left

Tag 0490, a definition

Tag 0490 in the Stacks Project.

AlgebraicGeometry.Space.IsSetTheoreticPreEquivalenceRelation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/SetTheoreticEquivalence.lean, line 131. The attribute's comment: “part (1): set-theoretic pre-equivalence relation”.

Stacks 0490, part (1). A pre-relation is a set-theoretic pre-equivalence relation when the relation it induces on the fibres of the points over every algebraically closed field in the site is an equivalence relation, arrows being allowed to appear only after a field extension.

abbrev IsSetTheoreticPreEquivalenceRelation (j : PreRelation R U) : Prop

AlgebraicGeometry.Space.IsSetTheoreticEquivalenceRelation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/SetTheoreticEquivalence.lean, line 139. The attribute's comment: “part (2): set-theoretic equivalence relation”.

Stacks 0490, part (2). A set-theoretic equivalence relation is a universally injective set-theoretic pre-equivalence relation.

abbrev IsSetTheoreticEquivalenceRelation (j : PreRelation R U) : Prop

Tag 0491, a lemma

Tag 0491 in the Stacks Project.

AlgebraicGeometry.Space.PreRelation.ContainsRelationImages, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/PreEquivalenceGeometricCriterion.lean, line 837. The attribute's comment: “part (2): the three image containments”.

Stacks 0491, part (2). A pre-relation contains the relation images when its image on topological points contains the images of the diagonal of U, of the flip of the pre-relation and of the endpoint map on composable pairs of arrows.

noncomputable abbrev PreRelation.ContainsRelationImages (j : PreRelation R U) : Prop

AlgebraicGeometry.Space.isSetTheoreticPreEquivalenceRelation_iff_containsRelationImages, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/PreEquivalenceGeometricCriterion.lean, line 850. The attribute's comment: “parts (1) and (2)”.

Stacks 0491, parts (1) and (2). A pre-relation is a set-theoretic pre-equivalence relation exactly when its image on points contains the images of the diagonal, of the flip and of the endpoint map on composable pairs.

theorem isSetTheoreticPreEquivalenceRelation_iff_containsRelationImages
    (j : PreRelation R U) :
    IsSetTheoreticPreEquivalenceRelation (presheafPreRelation j) ↔
      j.ContainsRelationImages

AlgebraicGeometry.Space.containsRelationImages_iff_exists_geometricRel_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/PreEquivalenceGeometricCriterion.lean, line 1051. The attribute's comment: “parts (2) and (3)”.

Stacks 0491, parts (2) and (3). The three image containments hold exactly when the relation cut out by the arrows already present over k is an equivalence relation for every algebraically closed field k in the site above one cardinal strictly below the size cutoff of the site.

theorem containsRelationImages_iff_exists_geometricRel_equivalence (j : PreRelation R U) :
    j.ContainsRelationImages ↔
      ∃ κ : Cardinal.{u}, κ < site.cutoff ∧ ∀ (k : Type u) [Field k] [IsAlgClosed k]
        (hk : site.Contains (Spec (.of k))) (b : Spec (.of k) ⟶ S)
        (β : B.obj.obj (Opposite.op (fieldObject (hS := hS) k hk b))),
        κ < Cardinal.mk k → Equivalence ((presheafPreRelation j).GeometricRel k hk b β)

AlgebraicGeometry.Space.isSetTheoreticPreEquivalenceRelation_iff_geometricRel_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/PreEquivalenceGeometricCriterion.lean, line 1080. The attribute's comment: “part (4)”.

Stacks 0491, part (4). For a pre-relation whose source and target are locally of finite type no cardinal bound is needed: the set-theoretic pre-equivalence condition is equivalent to the relation of actual arrows being an equivalence relation over every algebraically closed field in the site.

theorem isSetTheoreticPreEquivalenceRelation_iff_geometricRel_equivalence
    (j : PreRelation R U) (_hs : IsLocallyOfFiniteType site S hS j.source.left.hom)
    (ht : IsLocallyOfFiniteType site S hS j.target.left.hom) :
    IsSetTheoreticPreEquivalenceRelation (presheafPreRelation j) ↔
      ∀ (k : Type u) [Field k] [IsAlgClosed k] (hk : site.Contains (Spec (.of k)))
        (b : Spec (.of k) ⟶ S)
        (β : B.obj.obj (Opposite.op (fieldObject (hS := hS) k hk b))),
        Equivalence ((presheafPreRelation j).GeometricRel k hk b β)

Tag 049X, a lemma

Tag 049X in the Stacks Project.

AlgebraicGeometry.Space.isSetTheoreticEquivalenceRelation_iff_containsRelationImages, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/SetTheoreticEquivalenceCriterion.lean, line 405. The attribute's comment: “conditions (1) and (2)”.

Stacks 049X, conditions (1) and (2). A pre-relation of algebraic spaces is a set-theoretic equivalence relation exactly when it is universally injective and its image on topological points contains the images of the diagonal of U, of its flip, and of the endpoint map on composable pairs of its arrows.

Universal injectivity is one of the two conditions on either side, and the other two are equivalent by Stacks 0491.

theorem isSetTheoreticEquivalenceRelation_iff_containsRelationImages (j : PreRelation R U) :
    IsSetTheoreticEquivalenceRelation (presheafPreRelation j) ↔
      UniversallyInjective site S hS (presheafPreRelation j).left ∧
        j.ContainsRelationImages

AlgebraicGeometry.Space.isSetTheoreticEquivalenceRelation_iff_exists_hasGeometricEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/SetTheoreticEquivalenceCriterion.lean, line 421. The attribute's comment: “conditions (1) and (3)”.

Stacks 049X, conditions (1) and (3). A pre-relation of algebraic spaces is a set-theoretic equivalence relation exactly when, over every algebraically closed field in the site above one cardinal strictly below the size cutoff of the site, its map on arrows is injective and the relation its arrows cut out is an equivalence relation.

The equivalence-relation half is Stacks 0491. Universal injectivity gives the injectivity over every sufficiently large field through the descent of a point of R along the relative diagonal of j, and conversely injectivity over all sufficiently large fields makes that diagonal surjective on points, which is universal injectivity by Stacks 040X.

theorem isSetTheoreticEquivalenceRelation_iff_exists_hasGeometricEquivalence
    (j : PreRelation R U) :
    IsSetTheoreticEquivalenceRelation (presheafPreRelation j) ↔
      ∃ κ : Cardinal.{u}, κ < site.cutoff ∧ ∀ (k : Type u) [Field k] [IsAlgClosed k]
        (hk : site.Contains (Spec (.of k))) (b : Spec (.of k) ⟶ S)
        (β : B.obj.obj (Opposite.op (fieldObject (hS := hS) k hk b))),
        κ < Cardinal.mk k → j.HasGeometricEquivalence k hk b β

AlgebraicGeometry.Space.isSetTheoreticEquivalenceRelation_iff_hasGeometricEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/SetTheoreticEquivalenceCriterion.lean, line 547. The attribute's comment: “condition (4)”.

Stacks 049X, condition (4). For a pre-relation of algebraic spaces which is decent, locally separated or quasi-separated the cardinality restriction can be dropped: it is a set-theoretic equivalence relation exactly when over every algebraically closed field in the site its map on arrows is injective and the relation its arrows cut out is an equivalence relation.

Under any of the three hypotheses a universally injective pre-relation is radicial by Stacks 0484, and over an algebraically closed field a fibre of a radicial morphism has exactly one section as soon as it has a point: this gives the injectivity on arrows, and makes the relation cut out by the arrows present over the field agree with the one of Stacks 0490, where arrows are allowed to appear after a field extension.

theorem isSetTheoreticEquivalenceRelation_iff_hasGeometricEquivalence
    (j : PreRelation R U)
    (hsep : IsDecent site S hS (presheafPreRelation j).left ∨
      IsLocallySeparated site S hS (presheafPreRelation j).left ∨
      IsQuasiSeparated site S hS (presheafPreRelation j).left) :
    IsSetTheoreticEquivalenceRelation (presheafPreRelation j) ↔
      ∀ (k : Type u) [Field k] [IsAlgClosed k] (hk : site.Contains (Spec (.of k)))
        (b : Spec (.of k) ⟶ S)
        (β : B.obj.obj (Opposite.op (fieldObject (hS := hS) k hk b))),
        j.HasGeometricEquivalence k hk b β

Tag 0492, a lemma

Tag 0492 in the Stacks Project.

AlgebraicGeometry.Space.isSetTheoreticPreEquivalenceRelation_of_isPreEquivalenceRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/SetTheoreticEquivalence.lean, line 182. The attribute's comment: “part (1): a pre-equivalence relation”.

Stacks 0492, part (1). A pre-equivalence relation is a set-theoretic pre-equivalence relation: over every algebraically closed field over the base, the relation its arrows induce on the points of U — arrows being allowed to appear after an extension of the field — is an equivalence relation.

theorem isSetTheoreticPreEquivalenceRelation_of_isPreEquivalenceRelation
    (j : PreRelation R U) (hj : IsPreEquivalenceRelation j) :
    IsSetTheoreticPreEquivalenceRelation j

AlgebraicGeometry.Space.isSetTheoreticPreEquivalenceRelation_groupoidPreRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/SetTheoreticEquivalence.lean, line 249. The attribute's comment: “part (1): a groupoid in algebraic spaces”.

Stacks 0492, part (1). The pre-relation of a groupoid in algebraic spaces is a set-theoretic pre-equivalence relation.

theorem isSetTheoreticPreEquivalenceRelation_groupoidPreRelation
    {A : AlgebraicSpaces B S hS} (G : GroupoidInAlgebraicSpaces B S hS A) :
    IsSetTheoreticPreEquivalenceRelation (groupoidPreRelation G)

AlgebraicGeometry.Space.isSetTheoreticPreEquivalenceRelation_groupoidOfAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/SetTheoreticEquivalence.lean, line 258. The attribute's comment: “part (1): an action of a group algebraic space”.

Stacks 0492, part (1). The pre-relation of the groupoid of an action of a group algebraic space on an algebraic space is a set-theoretic pre-equivalence relation.

theorem isSetTheoreticPreEquivalenceRelation_groupoidOfAction
    (A : AlgebraicSpaces B S hS) (G W : Over A.obj) [GrpObj G] [ModObj G W]
    (hG : IsAlgebraicSpace B S hS G.left) (hW : IsAlgebraicSpace B S hS W.left) :
    IsSetTheoreticPreEquivalenceRelation
      (groupoidPreRelation (groupoidOfAction A G W hG hW).groupoid)

AlgebraicGeometry.Space.isSetTheoreticEquivalenceRelation_of_isEquivalenceRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/SetTheoreticEquivalence.lean, line 269. The attribute's comment: “part (2)”.

Stacks 0492, part (2). An equivalence relation is a set-theoretic equivalence relation: it is a monomorphism, hence universally injective, and a pre-equivalence relation, hence set-theoretically one.

theorem isSetTheoreticEquivalenceRelation_of_isEquivalenceRelation (j : PreRelation R U)
    (hj : CategoryTheory.IsEquivalenceRelation j.target j.source) :
    IsSetTheoreticEquivalenceRelation j

Tag 049Y, a lemma

Tag 049Y in the Stacks Project.

AlgebraicGeometry.Space.isSetTheoreticallyInvariant_iff_isSurjective_invarianceToRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/InvarianceSquare.lean, line 714. The attribute's comment: “part (1)”.

Stacks 049Y, part (1). A morphism φ : U ⟶ X over the base, with X an algebraic space, is set-theoretically invariant under a pre-relation j : R ⟶ U ×_Z U if and only if the projection p : (U ×_X U) ×_{U ×_Z U} R ⟶ R is surjective.

theorem isSetTheoreticallyInvariant_iff_isSurjective_invarianceToRelation
    (hX : IsAlgebraicSpace B S hS X.left) (j : PreRelation R U) (φ : U ⟶ X) :
    IsSetTheoreticallyInvariant j φ.left ↔
      IsSurjective B S hS (j.invarianceToRelation φ).left

AlgebraicGeometry.Space.separatesOrbits_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/InvarianceSquare.lean, line 735. The attribute's comment: “part (3): separation of orbits”.

Stacks 049Y, part (3). If both projections of the square are surjective, then the morphism φ separates the orbits of the pre-relation.

theorem separatesOrbits_of_isSurjective (hX : IsAlgebraicSpace B S hS X.left)
    (j : PreRelation R U) (φ : U ⟶ X)
    (hp : IsSurjective B S hS (j.invarianceToRelation φ).left)
    (hq : IsSurjective B S hS (j.invarianceToSelfFibreProduct φ).left) :
    SeparatesOrbits j φ.left

AlgebraicGeometry.Space.isSetTheoreticPreEquivalenceRelation_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/InvarianceSquare.lean, line 770. The attribute's comment: “part (3): set-theoretic pre-equivalence relation”.

Stacks 049Y, part (3). If both projections of the square are surjective, then the pre-relation is a set-theoretic pre-equivalence relation.

theorem isSetTheoreticPreEquivalenceRelation_of_isSurjective
    (hX : IsAlgebraicSpace B S hS X.left) (j : PreRelation R U) (φ : U ⟶ X)
    (hp : IsSurjective B S hS (j.invarianceToRelation φ).left)
    (hq : IsSurjective B S hS (j.invarianceToSelfFibreProduct φ).left) :
    IsSetTheoreticPreEquivalenceRelation j

AlgebraicGeometry.Space.separatesOrbits_iff_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/InvarianceSquare.lean, line 791. The attribute's comment: “part (2)”.

Stacks 049Y, part (2). For a set-theoretic pre-equivalence relation, a morphism φ : U ⟶ X over the base, with X an algebraic space, separates the orbits of the pre-relation if and only if both projections p and q of the square are surjective.

theorem separatesOrbits_iff_isSurjective (hX : IsAlgebraicSpace B S hS X.left)
    (j : PreRelation R U) (φ : U ⟶ X) (hj : IsSetTheoreticPreEquivalenceRelation j) :
    SeparatesOrbits j φ.left ↔
      (IsSurjective B S hS (j.invarianceToRelation φ).left ∧
        IsSurjective B S hS (j.invarianceToSelfFibreProduct φ).left)

AlgebraicGeometry.Space.separatesOrbits_iff_isSurjective_toSelfFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/InvarianceSquare.lean, line 857. The attribute's comment: “part (4)”.

Stacks 049Y, part (4). If φ : U ⟶ X is invariant under a set-theoretic pre-equivalence relation j : R ⟶ U ×_Z U, with X an algebraic space, then φ separates the orbits of j if and only if the induced morphism (t, s) : R ⟶ U ×_X U is surjective.

theorem separatesOrbits_iff_isSurjective_toSelfFibreProduct
    (hX : IsAlgebraicSpace B S hS X.left) (j : PreRelation R U) (φ : U ⟶ X)
    (hφ : IsInvariant j φ.left) (hj : IsSetTheoreticPreEquivalenceRelation j) :
    SeparatesOrbits j φ.left ↔
      IsSurjective B S hS (j.toSelfFibreProduct φ hφ).left

Tag 0493, a definition

Tag 0493 in the Stacks Project.

AlgebraicGeometry.Space.IsOrbitSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/OrbitSeparation.lean, line 95.

A morphism out of U is an orbit space for a pre-relation when it is invariant under the pre-relation, separates its orbits, and is surjective on points.

abbrev IsOrbitSpace (j : PreRelation R U) (φ : U.left ⟶ X) : Prop

Tag 049Z, a lemma

Tag 049Z in the Stacks Project.

AlgebraicGeometry.Space.isOrbitSpace_iff_isSurjective_toSelfFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/OrbitSpaceCriterion.lean, line 84.

Stacks 049Z. Let j : R ⟶ U ×_Z U be a set-theoretic pre-equivalence relation and let φ : U ⟶ X be a morphism over the base whose target is an algebraic space. Then φ is an orbit space for j if and only if

1. φ is invariant, t ≫ φ = s ≫ φ,
2. the induced morphism (t, s) : R ⟶ U ×_X U is surjective, and
3. the morphism φ : U ⟶ X is surjective.

Condition (2) is stated for the morphism (t, s) built from the proof of condition (1), so the three conditions appear as an existential over that proof.

theorem isOrbitSpace_iff_isSurjective_toSelfFibreProduct
    (hX : IsAlgebraicSpace B S hS X.left) (j : PreRelation R U) (φ : U ⟶ X)
    (hj : IsSetTheoreticPreEquivalenceRelation j) :
    IsOrbitSpace j φ.left ↔
      ∃ hφ : IsInvariant j φ.left,
        IsSurjective B S hS (j.toSelfFibreProduct φ hφ).left ∧
          IsSurjective B S hS φ.left

Tag 04A0, a lemma

Tag 04A0 in the Stacks Project.

AlgebraicGeometry.Space.isOrbitSpace_iff_geometricPoints_quotient_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/OrbitSpaces/GeometricQuotient.lean, line 196.

Stacks 04A0. For a pre-relation whose relation space and whose source are locally of finite type over the base, an invariant morphism out of U is an orbit space for the pre-relation exactly when, over every algebraically closed field-valued point of the base, it induces a bijection from the quotient of the points of U by the relation generated by the pre-relation onto the points of the target: every point of the target over that point of the base lifts, and two points of U have the same image precisely when they are weakly equivalent.

theorem isOrbitSpace_iff_geometricPoints_quotient_bijective {X : Over B}
    (j : PreRelation R U) (φ : U ⟶ X)
    (hR : IsLocallyOfFiniteType site S hS R.hom.hom)
    (hU : IsLocallyOfFiniteType site S hS U.hom.hom)
    (hφ : IsInvariant j φ.left) :
    IsOrbitSpace (presheafPreRelation j) φ.left.hom ↔
      ∀ p : GeometricPoint site S hS B.obj,
        (∀ y : TestPoint p.val.siteObject (yonedaEquiv.symm p.val.value)
            ((overForgetSpace B).obj X),
          ∃ x : TestPoint p.val.siteObject (yonedaEquiv.symm p.val.value)
            ((overForgetSpace B).obj U), x.1 ≫ φ.left.hom = y.1) ∧
        (∀ x y : TestPoint p.val.siteObject (yonedaEquiv.symm p.val.value)
            ((overForgetSpace B).obj U),
          x.1 ≫ φ.left.hom = y.1 ≫ φ.left.hom ↔
            (presheafPreRelation j).WeaklyEquivalent p.val x y)

Sources

• Section 83.5, Tag 048M
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.PreRelation.pointOrbit · AlgebraicGeometry.Space.PreRelation.pointOrbit_eq_targets_of_source · AlgebraicGeometry.Space.pointsMap_eq_of_mem_pointOrbit · AlgebraicGeometry.Space.PreRelation.WeaklyEquivalent · AlgebraicGeometry.Space.PreRelation.Equivalent · AlgebraicGeometry.Space.PreRelation.weakOrbit · AlgebraicGeometry.Space.PreRelation.orbit · AlgebraicGeometry.Space.PreRelation.weakOrbit_eq_targets

Section83.6 Coarse quotients#

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

Tag 04A2, a definition

Tag 04A2 in the Stacks Project.

AlgebraicGeometry.Space.IsCoarseQuotient, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CoarseQuotient.lean, line 150. The attribute's comment: “algebraic spaces”.

Stacks 04A2. A morphism φ : U ⟶ X of algebraic spaces over B is a coarse quotient of a pre-relation j when it is a categorical quotient of j and an orbit space for it.

noncomputable abbrev IsCoarseQuotient {R U X : Over B} (j : PreRelation R U) (φ : U ⟶ X) :
    Prop

AlgebraicGeometry.Space.IsCoarseQuotientInSchemes, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/CoarseQuotient.lean, line 252. The attribute's comment: “schemes”.

Stacks 04A2. A morphism φ : U ⟶ X of schemes over the base scheme S, with R, U and X contained in the big fppf site, is a coarse quotient in schemes of a pre-relation j of schemes over S when it is a categorical quotient in schemes of j and an orbit space for it.

noncomputable abbrev IsCoarseQuotientInSchemes {R U X : Over S} (hR : site.Contains R.left)
    (hU : site.Contains U.left) (hX : site.Contains X.left)
    (j : Stacks.Groupoids.PreRelation R U) (φ : U ⟶ X) : Prop

Sources

• Section 83.6, Tag 04A1
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsCoarseQuotient · AlgebraicGeometry.Space.IsCoarseQuotientInSchemes

Section83.7 Topological properties#

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

Tag 04A4, a definition

Tag 04A4 in the Stacks Project.

AlgebraicGeometry.Space.IsInvariantClosedMap, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 121. The attribute's comment: “condition (2): invariant closed subsets have closed image”.

Stacks 04A4, condition (2). An invariant morphism φ : U ⟶ X has closed invariant images when for every R-invariant closed subset Z ⊆ |U| the image φ(Z) is closed in |X|.

abbrev IsInvariantClosedMap (j : PreRelation R U) (φ : U.left ⟶ X) : Prop

AlgebraicGeometry.Space.IsInvariantClosedMapInter, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 128. The attribute's comment: “condition (3): intersections of invariant closed subsets”.

Stacks 04A4, condition (3). Condition (2) holds, and moreover for every pair of R-invariant closed subsets Z₁, Z₂ ⊆ |U| one has φ(Z₁ ∩ Z₂) = φ(Z₁) ∩ φ(Z₂).

abbrev IsInvariantClosedMapInter (j : PreRelation R U) (φ : U.left ⟶ X) : Prop

AlgebraicGeometry.Space.IsStronglySubmersive, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 147. The attribute's comment: “condition (4): strongly submersive”.

Stacks 04A4, condition (4). An invariant morphism φ : U ⟶ X is strongly submersive when the morphism (t, s) : R ⟶ U ×_X U assembled from the target and the source of j is universally submersive.

Invariance of φ is exactly the commutation t ≫ φ = s ≫ φ needed to form that morphism, so it is taken as an argument.

noncomputable abbrev IsStronglySubmersive (j : PreRelation R U) (φ : U.left ⟶ X)
    (hφ : IsInvariant j φ) : Prop

AlgebraicGeometry.Space.IsUniformlySubmersive, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 203. The attribute's comment: “uniform condition (1)”.

Stacks 04A4, uniform condition (1). Condition (1) holds after every flat base change.

abbrev IsUniformlySubmersive : Prop

AlgebraicGeometry.Space.IsUniformlyInvariantClosedMap, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 209. The attribute's comment: “uniform condition (2)”.

Stacks 04A4, uniform condition (2). Condition (2) holds after every flat base change.

abbrev IsUniformlyInvariantClosedMap : Prop

AlgebraicGeometry.Space.IsUniversallyInvariantClosedMap, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 215. The attribute's comment: “universal condition (2)”.

Stacks 04A4, universal condition (2). Condition (2) holds after every base change.

abbrev IsUniversallyInvariantClosedMap : Prop

AlgebraicGeometry.Space.IsUniformlyInvariantClosedMapInter, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 221. The attribute's comment: “uniform condition (3)”.

Stacks 04A4, uniform condition (3). Condition (3) holds after every flat base change.

abbrev IsUniformlyInvariantClosedMapInter : Prop

AlgebraicGeometry.Space.IsUniversallyInvariantClosedMapInter, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 228. The attribute's comment: “universal condition (3)”.

Stacks 04A4, universal condition (3). Condition (3) holds after every base change.

abbrev IsUniversallyInvariantClosedMapInter : Prop

AlgebraicGeometry.Space.IsUniformlyStronglySubmersive, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 234. The attribute's comment: “uniform condition (4)”.

Stacks 04A4, uniform condition (4). Condition (4) holds after every flat base change.

noncomputable abbrev IsUniformlyStronglySubmersive : Prop

AlgebraicGeometry.Space.IsUniversallyStronglySubmersive, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 241. The attribute's comment: “universal condition (4)”.

Stacks 04A4, universal condition (4). Condition (4) holds after every base change.

noncomputable abbrev IsUniversallyStronglySubmersive : Prop

Declarations registered for the tag:

• AlgebraicGeometry.Space.IsSubmersive, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 114 (StacksFrontier): “condition (1): submersive”.
• AlgebraicGeometry.Space.UniversallySubmersive, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/TopologicalConditions.lean, line 115 (StacksFrontier): “universal condition (1)”.

Sources

• Section 83.7, Tag 04A3
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsInvariantClosedMap · AlgebraicGeometry.Space.IsInvariantClosedMapInter · AlgebraicGeometry.Space.IsStronglySubmersive · AlgebraicGeometry.Space.IsUniformlySubmersive · AlgebraicGeometry.Space.IsUniformlyInvariantClosedMap · AlgebraicGeometry.Space.IsUniversallyInvariantClosedMap · AlgebraicGeometry.Space.IsUniformlyInvariantClosedMapInter · AlgebraicGeometry.Space.IsUniversallyInvariantClosedMapInter

Section83.8 Invariant functions#

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

Tag 04AA, a definition

Tag 04AA in the Stacks Project.

AlgebraicGeometry.Space.invariantFunctionSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/InvariantFunctions.lean, line 196. The attribute's comment: “part (1): the sheaf of invariant functions”.

Stacks 04AA, part (1). The sheaf of R-invariant functions (φ_*O_U)^R of an R-invariant morphism φ : U ⟶ X: the equalizer, on the small étale site of X, of the two maps φ_*t^♯, φ_*s^♯ : φ_*O_U ⟶ φ'_*O_R given by pulling functions back along the target and the source of the pre-relation.

Its inclusion into φ_*O_U as an O_X-subalgebra is CategoryTheory.Limits.equalizer.ι, which is a monomorphism.

noncomputable def invariantFunctionSheaf {R U : Over B} {X : AlgebraicSpaces site S hS}
    (j : PreRelation R U) (φ : U.left ⟶ X) (hφ : IsInvariant j φ) :
    Sheaf (SmallEtale.topology site S hS X.1) CommRingCat.{u}

AlgebraicGeometry.Space.HasInvariantFunctions, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/InvariantFunctions.lean, line 213. The attribute's comment: “part (2): the functions on X are the invariant functions”.

Stacks 04AA, part (2). The functions on X are the R-invariant functions on U when the natural map O_X ⟶ (φ_*O_U)^R is an isomorphism.

noncomputable abbrev HasInvariantFunctions {R U : Over B} {X : AlgebraicSpaces site S hS}
    (j : PreRelation R U) (φ : U.left ⟶ X) (hφ : IsInvariant j φ) : Prop

Sources

• Section 83.8, Tag 04A9
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.invariantFunctionSheaf · AlgebraicGeometry.Space.HasInvariantFunctions

Section83.9 Good quotients#

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

Tag 04AC, a definition

Tag 04AC in the Stacks Project.

AlgebraicGeometry.Space.IsGoodQuotient, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/QuotientProperties.lean, line 277.

Stacks 04AC. A morphism φ : U ⟶ X of algebraic spaces over B is a good quotient of a pre-relation j when it is R-invariant, affine and surjective, condition (3) of Stacks 04A4 holds for it universally, and the functions on X are the R-invariant functions on U.

abbrev IsGoodQuotient {B : AlgebraicSpaces site S hS} {R U X : Over B} (j : PreRelation R U)
    (φ : U ⟶ X) : Prop

Sources

• Section 83.9, Tag 04AB
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsGoodQuotient

Section83.10 Geometric quotients#

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

Tag 04AE, a definition

Tag 04AE in the Stacks Project.

AlgebraicGeometry.Space.IsGeometricQuotient, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Quotients/QuotientProperties.lean, line 291.

Stacks 04AE. A morphism φ : U ⟶ X of algebraic spaces over B is a geometric quotient of a pre-relation j when it is an orbit space for j, universally submersive, and the functions on X are the R-invariant functions on U.

abbrev IsGeometricQuotient {B : AlgebraicSpaces site S hS} {R U X : Over B}
    (j : PreRelation R U) (φ : U ⟶ X) : Prop

Sources

• Section 83.10, Tag 04AD
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsGeometricQuotient

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.