40 More on Groupoid Schemes

Chapter 40 of the Stacks Project, More on Groupoid Schemes, Tag 04LA: the 13 sections of its 15 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 58 tags are carried by 140 declarations of the repository (all in StacksFrontier) and 1 registered declaration.

Section40.3 Useful diagrams #

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

Tag 04LF, an equation

Tag 04LF in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.comp_source_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FieldExtensionEvaluation.lean, line 148. The attribute's comment: “diagram (04LF): the lower-right square is cartesian”.

The square formed by composition, the second projection, and two copies of the source map is a pullback square: a composable pair of arrows is determined by its first member together with its composite.

theorem comp_source_isPullback {S : Scheme.{u}} (G : GroupoidScheme S) :
    IsPullback G.comp (pullback.snd G.source G.target) G.source G.source

Stacks.Groupoids.GroupoidScheme.target_comp_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FieldExtensionEvaluation.lean, line 197. The attribute's comment: “diagram (04LF): the lower-right square is cartesian”.

The upper triangle in the composition diagram, viewed as a square with two copies of its apex, is a pullback square: a pair of arrows with the same target is the same thing as a composable pair together with its composite.

theorem target_comp_isPullback {S : Scheme.{u}} (G : GroupoidScheme S) :
    IsPullback (pullback.fst G.source G.target) G.comp G.target G.target

Tag 04LG, an equation

Tag 04LG in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 81. The attribute's comment: “the vertical map (pr₀, c ∘ (i, 1)) of the displayed diagram”.

The vertical map in the top left of the diagram: it sends a pair (α, β) with equal targets to the composable pair (α, α⁻¹ ∘ β).

noncomputable def targetPullbackToComposable {S : Scheme.{u}}
    (G : Stacks.Groupoids.GroupoidScheme S) :
    pullback G.target G.target ⟶ pullback G.source G.target

AlgebraicGeometry.GroupoidScheme.fst_source_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 103. The attribute's comment: “cartesianness: the lower of the two lower left squares, the one taken with the first projection on top and the target along the bottom”.

The square formed by the two projections of the scheme of composable pairs together with the source and the target maps is a pullback square. This is the lower-left square of the diagram taken with the lower horizontal maps, and it is cartesian because the scheme of composable pairs is by definition the fibre product of the source and the target.

theorem fst_source_isPullback {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S) :
    IsPullback (pullback.fst G.source G.target) (pullback.snd G.source G.target)
      G.source G.target

AlgebraicGeometry.GroupoidScheme.id_target_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 114. The attribute's comment: “commutativity: the right-hand square between the two top rows, whose vertical maps are the identities”.

The upper-right square of the diagram commutes. Both of its vertical maps are identities, of the arrow scheme and of the object scheme respectively, and both of its horizontal maps are the target map.

theorem id_target_comm {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S) :
    𝟙 G.arrows ≫ G.target = G.target ≫ 𝟙 G.objects

AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 123. The attribute's comment: “commutativity: the left square between the two top rows taken with the first projections”.

The comparison map preserves the first projection. This is the lower of the two commutative triangles in the top left of the diagram.

theorem targetPullbackToComposable_fst {S : Scheme.{u}}
    (G : Stacks.Groupoids.GroupoidScheme S) :
    targetPullbackToComposable G ≫ pullback.fst G.source G.target =
      pullback.fst G.target G.target

AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 142. The attribute's comment: “commutativity: the left square between the two top rows taken with the second projection on top and the composition along the bottom”.

Composing a pair after the change of coordinates recovers its second member. This is the upper of the two commutative triangles in the top left of the diagram.

theorem targetPullbackToComposable_comp {S : Scheme.{u}}
    (G : Stacks.Groupoids.GroupoidScheme S) :
    targetPullbackToComposable G ≫ G.comp = pullback.snd G.target G.target

AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 213. The attribute's comment: “the two top rows are isomorphic via the vertical maps given”.

The vertical comparison between pairs with the same target and composable pairs is an isomorphism.

theorem targetPullbackToComposable_isIso {S : Scheme.{u}}
    (G : Stacks.Groupoids.GroupoidScheme S) :
    IsIso (targetPullbackToComposable G)

AlgebraicGeometry.GroupoidScheme.diagram_pull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 250. The attribute's comment: “the whole diagram: it is commutative, its two top rows are isomorphic via the vertical maps given, and its two lower left squares are cartesian”.

Every assertion made about the displayed diagram, in one statement.

Each square is written as left ≫ bottom = top ≫ right, so that the vertical maps which are identities are displayed rather than suppressed. The first three conjuncts are the commutativity of the three squares between the two top rows: the two on the left, one for each of the two parallel arrows, and the right-hand one whose vertical maps are the identity of the arrow scheme and the identity of the object scheme. Together with the fourth conjunct, which says that the remaining vertical map is an isomorphism, they say that the two top rows are isomorphic through the vertical maps given. The last two conjuncts say that the two lower left squares, again one for each of the two parallel arrows, are cartesian; the commutativity of those two squares is part of the same assertions.

theorem diagram_pull {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S) :
    targetPullbackToComposable G ≫ G.comp =
          pullback.snd G.target G.target ≫ 𝟙 G.arrows ∧
      targetPullbackToComposable G ≫ pullback.fst G.source G.target =
          pullback.fst G.target G.target ≫ 𝟙 G.arrows ∧
      𝟙 G.arrows ≫ G.target = G.target ≫ 𝟙 G.objects ∧
      IsIso (targetPullbackToComposable G) ∧
      IsPullback G.comp (pullback.snd G.source G.target) G.source G.source ∧
      IsPullback (pullback.fst G.source G.target) (pullback.snd G.source G.target)
        G.source G.target

Declarations registered for the tag:

Stacks.Groupoids.GroupoidScheme.comp_source_isPullback, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 92 (StacksFrontier): “cartesianness: the upper of the two lower left squares, the one taken with the composition on top and the source along the bottom”.

Sources

LeanStacks.Groupoids.GroupoidScheme.comp_source_isPullback · Stacks.Groupoids.GroupoidScheme.target_comp_isPullback · AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable · AlgebraicGeometry.GroupoidScheme.fst_source_isPullback · AlgebraicGeometry.GroupoidScheme.id_target_comm · AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable_fst · AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable_comp · AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable_isIso

Section40.4 Sheaf of differentials #

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

Tag 04R9, a lemma

Tag 04R9 in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.conormalToDifferentials, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/SheafOfDifferentials.lean, line 321. The attribute's comment: “the canonical map”.

[Stacks Project, Tag 04R9]: the canonical map t^* 𝒞_{U/R} ⟶ Ω_{R/U}, from the pullback along the target morphism of the conormal sheaf of the identity section to the sheaf of relative differentials of the source morphism.

It is the canonical map of conormal sheaves of [Stacks Project, Tag 01R4] attached to the cartesian square Stacks.Groupoids.GroupoidScheme.isPullback_diagonal_divide, whose source is t^* 𝒞_{U/R} and whose target is the conormal sheaf of the diagonal of s, followed by the inverse of the isomorphism of [Stacks Project, Tag 08S2] identifying that conormal sheaf with Ω_{R/U}. See the module docstring on which of s and t carries the differentials.

def conormalToDifferentials :
    (RingedSpaceModuleAdjunction.modulePullback G.target.left.toLRSHom.toShHom).obj
        (Stacks.Conormal.conormalSheaf G.identity.left) ⟶
      Scheme.Hom.relativeDifferentials G.source.left

Stacks.Groupoids.GroupoidScheme.epi_conormalToDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/SheafOfDifferentials.lean, line 338. The attribute's comment: “the canonical surjection”.

[Stacks Project, Tag 04R9]: the canonical map t^* 𝒞_{U/R} ⟶ Ω_{R/U} is surjective. The sheaf of differentials of R over U is a quotient of the pullback along the target morphism of the conormal sheaf of the identity section.

The map of conormal sheaves of the cartesian square is surjective by [Stacks Project, Tag 0473], and the comparison of [Stacks Project, Tag 08S2] is an isomorphism.

theorem epi_conormalToDifferentials : Epi G.conormalToDifferentials

Stacks.Groupoids.GroupoidScheme.isIso_conormalToDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/SheafOfDifferentials.lean, line 457. The attribute's comment: “an isomorphism when the source morphism is flat”.

[Stacks Project, Tag 04R9]: the canonical map t^* 𝒞_{U/R} ⟶ Ω_{R/U} is an isomorphism when the source morphism is flat. With R over U via s, the sheaf of differentials of R over U is then equal to the pullback along the target morphism of the conormal sheaf of the identity section, not merely a quotient of it.

Flatness of s makes division flat, by Stacks.Groupoids.GroupoidScheme.flat_divide: division is a base change of the target morphism, which is flat with the source morphism because the inverse is an isomorphism. The map of conormal sheaves of the cartesian square is then an isomorphism by the flat half of [Stacks Project, Tag 0473], and so is the comparison of [Stacks Project, Tag 08S2].

theorem isIso_conormalToDifferentials [Flat G.source.left] :
    IsIso G.conormalToDifferentials

Stacks.Groupoids.GroupoidScheme.targetConormalToDifferentials, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/SheafOfDifferentials.lean, line 633. The attribute's comment: “the canonical map for the differentials of the target”.

[Stacks Project, Tag 04R9]: the canonical map s^* 𝒞_{U/R} ⟶ Ω_{R/U}, with R over U via t. This is the reading of the tag in which the differentials are those of the target morphism; it is the previous map pulled back along the inverse, and is built here the same way, from the cartesian square Stacks.Groupoids.GroupoidScheme.isPullback_diagonal_divideTarget and the isomorphism of [Stacks Project, Tag 08S2].

def targetConormalToDifferentials :
    (RingedSpaceModuleAdjunction.modulePullback G.source.left.toLRSHom.toShHom).obj
        (Stacks.Conormal.conormalSheaf G.identity.left) ⟶
      Scheme.Hom.relativeDifferentials G.target.left

Stacks.Groupoids.GroupoidScheme.epi_targetConormalToDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/SheafOfDifferentials.lean, line 647. The attribute's comment: “the canonical surjection for the differentials of the target”.

[Stacks Project, Tag 04R9]: the canonical map s^* 𝒞_{U/R} ⟶ Ω_{R/U} is surjective, with R over U via t. The sheaf of differentials of R seen as a scheme over U via the target morphism is a quotient of the pullback along the source morphism of the conormal sheaf of the identity section.

theorem epi_targetConormalToDifferentials : Epi G.targetConormalToDifferentials

Stacks.Groupoids.GroupoidScheme.isIso_targetConormalToDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/SheafOfDifferentials.lean, line 751. The attribute's comment: “an isomorphism for the differentials of the target when the source map is flat”.

[Stacks Project, Tag 04R9]: the canonical map s^* 𝒞_{U/R} ⟶ Ω_{R/U} is an isomorphism when the source morphism is flat, with R over U via t. This is the second reading of the tag, in which the differentials are those of the target morphism.

Here flatness of s is used directly: division on this side is a base change of the source morphism, by Stacks.Groupoids.GroupoidScheme.isPullback_divideTarget_fst.

theorem isIso_targetConormalToDifferentials [Flat G.source.left] :
    IsIso G.targetConormalToDifferentials

Sources

LeanStacks.Groupoids.GroupoidScheme.conormalToDifferentials · Stacks.Groupoids.GroupoidScheme.epi_conormalToDifferentials · Stacks.Groupoids.GroupoidScheme.isIso_conormalToDifferentials · Stacks.Groupoids.GroupoidScheme.targetConormalToDifferentials · Stacks.Groupoids.GroupoidScheme.epi_targetConormalToDifferentials · Stacks.Groupoids.GroupoidScheme.isIso_targetConormalToDifferentials

Section40.5 Local structure #

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

Tag 0CK4, a lemma

Tag 0CK4 in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.cotangent_composition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/LocalStructure/Cotangent.lean, line 536. The attribute's comment: “composition on I/I²”.

At an identity of a groupoid scheme, the map I/I² → J/J² induced by composition is the diagonal followed by the two maps induced by the projections.

theorem cotangent_composition :
    G.compositionCotangent x =
      ((G.firstCotangent x).coprod (G.secondCotangent x)).comp
        (LinearMap.id.prod LinearMap.id)

Stacks.Groupoids.GroupoidScheme.cotangent_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/LocalStructure/Cotangent.lean, line 556. The attribute's comment: “inversion on I/I²”.

At an identity of a groupoid scheme, inversion acts by -1 on I/I².

theorem cotangent_inverse : G.inverseCotangent x = -LinearMap.id

Sources

LeanStacks.Groupoids.GroupoidScheme.cotangent_composition · Stacks.Groupoids.GroupoidScheme.cotangent_inverse

Section40.6 Properties of groupoids #

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

Tag 04LH, a lemma

Tag 04LH in the Stacks Project.

AlgebraicGeometry.exists_open_with_preimage_maximal_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/MaximalLocus.lean, line 128.

Stacks Project, Tag 04LH. Suppose P, Q, and R are properties of morphisms of schemes, R implies Q, Q is stable under composition and base change, and maximal open P-loci exist for Q-morphisms and commute with base change by R-morphisms. For a groupoid scheme whose source and target have R, the maximal P-locus of the indicated map from the pullback of its arrow scheme is the inverse image of an open of U'.

public theorem exists_open_with_preimage_maximal_locus
    (P Q R : MorphismProperty Scheme.{u})
    (hRQ : R ≤ Q) [Q.IsStableUnderComposition] [Q.IsStableUnderBaseChange]
    (hmax : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y), Q f →
      ∃ V : X.Opens, IsGreatest {W : X.Opens | P (W.ι ≫ f)} V)
    (hbase : ∀ {X Y X' Y' : Scheme.{u}} {f : X ⟶ Y} {f' : X' ⟶ Y'}
      {p : X' ⟶ X} {q : Y' ⟶ Y}, Q f → R q → IsPullback p f' f q →
      ∀ {V : X.Opens}, IsGreatest {W : X.Opens | P (W.ι ≫ f)} V →
        IsGreatest {W' : X'.Opens | P (W'.ι ≫ f')} (p ⁻¹ᵁ V))
    {S : Scheme.{u}} (G : GroupoidScheme S) {U' : Scheme.{u}}
    (g : U' ⟶ G.objects.left) (hs : R G.source.left) (ht : R G.target.left) (hg : Q g) :
    ∃ W : U'.Opens,
      IsGreatest
        {V : (pullback g G.target.left).Opens |
          P (V.ι ≫ pullback.snd g G.target.left ≫ G.source.left)}
        ((pullback.fst g G.target.left) ⁻¹ᵁ W)

Tag 04LI, a remark

Tag 04LI in the Stacks Project.

AlgebraicGeometry.exists_flat_locus_not_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/PointwiseFlatLocus.lean, line 355. The attribute's comment: “pointwise_warning”.

Stacks Project, Tag 04LI (pointwise warning). For some morphism of schemes, its maximal flat open is strictly smaller than its pointwise flat locus.

public theorem exists_flat_locus_not_open :
    ∃ (X Y : Scheme.{u}) (f : X ⟶ Y) (W : X.Opens),
      IsGreatest {V : X.Opens | Flat (V.ι ≫ f)} W ∧
        (W.1 : Set X) ⊂
          {x : X | IsFlatAt f.toLRSHom.toShHom x}

Tag 047W, a remark

Tag 047W in the Stacks Project.

AlgebraicGeometry.exists_open_with_preimage_maximal_cohenMacaulayLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CohenMacaulayLocus.lean, line 173. The attribute's comment: “cohen_macaulay”.

The maximal Cohen–Macaulay locus of h : U' ×_{g,U,t} R ⟶ U is the inverse image of an open of U'.

public theorem exists_open_with_preimage_maximal_cohenMacaulayLocus
    (D : FlatLocallyFinitelyPresentedGroupoidSituation) :
    ∃ W : D.U'.Opens,
      IsGreatest
        {V : D.fiberProduct.Opens |
          ∃ hf : ∀ y : D.groupoid.objects.left,
              IsLocallyNoetherian ((V.ι ≫ D.h).fiber y),
            Scheme.Hom.IsCohenMacaulay (V.ι ≫ D.h) hf}
        ((pullback.fst D.g D.groupoid.target.left) ⁻¹ᵁ W)

AlgebraicGeometry.exists_open_with_preimage_maximal_etaleLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/EtaleLocus.lean, line 55. The attribute's comment: “etale”.

Stacks Project, Tag 047W, case (8). In the flat, locally finitely presented groupoid situation the largest open of U' ×_{g, U, t} R on which h is étale is the inverse image along the projection of an open of U'.

public theorem exists_open_with_preimage_maximal_etaleLocus
    (D : FlatLocallyFinitelyPresentedGroupoidSituation.{u}) :
    ∃ W : D.U'.Opens,
      IsGreatest {V : D.fiberProduct.Opens | Etale (V.ι ≫ D.h)}
        ((pullback.fst D.g D.groupoid.target.left) ⁻¹ᵁ W)

AlgebraicGeometry.exists_open_with_preimage_maximal_flatLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/FlatLocus.lean, line 59. The attribute's comment: “flat”.

Stacks Project, Tag 047W, case (4). In the flat, locally finitely presented groupoid situation the largest open of U' ×_{g, U, t} R on which h is flat is the inverse image along the projection of an open of U'.

public theorem exists_open_with_preimage_maximal_flatLocus
    (D : FlatLocallyFinitelyPresentedGroupoidSituation.{u}) :
    ∃ W : D.U'.Opens,
      IsGreatest {V : D.fiberProduct.Opens | Flat (V.ι ≫ D.h)}
        ((pullback.fst D.g D.groupoid.target.left) ⁻¹ᵁ W)

AlgebraicGeometry.exists_open_with_preimage_maximal_quasiFiniteLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/QuasiFiniteLocus.lean, line 80. The attribute's comment: “locally quasi-finite”.

Stacks Project, Tag 047W, case (2). In the groupoid situation with structure maps locally of finite type, the largest open of U' ×_{g, U, t} R on which h is locally quasi-finite is the inverse image along the projection of an open of U'.

public theorem exists_open_with_preimage_maximal_quasiFiniteLocus
    (D : LocallyOfFiniteTypeGroupoidSituation.{u}) :
    ∃ W : D.U'.Opens,
      IsGreatest
        {V : D.fiberProduct.Opens |
          LocallyOfFiniteType (V.ι ≫ D.h) ∧ LocallyQuasiFinite (V.ι ≫ D.h)}
        ((pullback.fst D.g D.groupoid.target.left) ⁻¹ᵁ W)

AlgebraicGeometry.exists_open_with_preimage_maximal_relativeDimensionLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RelativeDimensionLocus.lean, line 99. The attribute's comment: “relative dimension at most d”.

In the locally finite type groupoid situation, the relative-dimension-at-most-d locus of h : U' ×_{g, U, t} R ⟶ U is the inverse image of an open of U', and it is the greatest open on which the restriction of h has that dimension bound.

This is Stacks Project, Tag 047W, case (1).

public theorem exists_open_with_preimage_maximal_relativeDimensionLE
    (D : LocallyOfFiniteTypeGroupoidSituation) (d : ℕ) :
    let _ : LocallyOfFiniteType
        (pullback.snd D.g D.groupoid.target.left ≫ D.groupoid.source.left) := inferInstance
    ∃ W : D.U'.Opens,
      IsGreatest
        {V : (pullback D.g D.groupoid.target.left).Opens |
          RelativeDimensionLE
            (V.ι ≫ pullback.snd D.g D.groupoid.target.left ≫ D.groupoid.source.left) d}
        ((pullback.fst D.g D.groupoid.target.left) ⁻¹ᵁ W)

AlgebraicGeometry.exists_open_with_preimage_maximal_smoothLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/SmoothLocus.lean, line 64. The attribute's comment: “smooth”.

Stacks Project, Tag 047W, case (7). In the flat, locally finitely presented groupoid situation the largest open of U' ×_{g, U, t} R on which h is smooth is the inverse image along the projection of an open of U'.

public theorem exists_open_with_preimage_maximal_smoothLocus
    (D : FlatLocallyFinitelyPresentedGroupoidSituation.{u}) :
    ∃ W : D.U'.Opens,
      IsGreatest {V : D.fiberProduct.Opens | Smooth (V.ι ≫ D.h)}
        ((pullback.fst D.g D.groupoid.target.left) ⁻¹ᵁ W)

AlgebraicGeometry.exists_open_with_preimage_maximal_syntomicLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/SyntomicLocus.lean, line 109. The attribute's comment: “syntomic”.

Stacks Project, Tag 047W, case (6). In the flat, locally finitely presented groupoid situation the largest open of U' ×_{g, U, t} R on which h is syntomic is the inverse image along the projection of an open of U'.

public theorem exists_open_with_preimage_maximal_syntomicLocus
    (D : FlatLocallyFinitelyPresentedGroupoidSituation.{u}) :
    ∃ W : D.U'.Opens,
      IsGreatest {V : D.fiberProduct.Opens | Syntomic (V.ι ≫ D.h)}
        ((pullback.fst D.g D.groupoid.target.left) ⁻¹ᵁ W)

AlgebraicGeometry.exists_open_with_preimage_maximal_unramifiedLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/UnramifiedLocus.lean, line 98. The attribute's comment: “unramified”.

Stacks Project, Tag 047W, case (3). In the groupoid situation with structure maps locally of finite type, the largest open of U' ×_{g, U, t} R on which h is unramified is the inverse image along the projection of an open of U'.

public theorem exists_open_with_preimage_maximal_unramifiedLocus
    (D : LocallyOfFiniteTypeGroupoidSituation.{u}) :
    ∃ W : D.U'.Opens,
      IsGreatest {V : D.fiberProduct.Opens | Unramified (V.ι ≫ D.h)}
        ((pullback.fst D.g D.groupoid.target.left) ⁻¹ᵁ W)

Tag 03JC, a lemma

Tag 03JC in the Stacks Project.

AlgebraicGeometry.isInvariantOpen_largestTargetOpen_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/InvariantLargestOpen.lean, line 77.

Stacks Project, Tag 03JC. For a groupoid scheme whose source and target maps are coverings for one of the five topologies, the largest open of the object scheme over which the source map has a target-local property is invariant.

theorem isInvariantOpen_largestTargetOpen_source {S : Scheme.{u}} (G : GroupoidScheme S)
    (P Q : MorphismProperty Scheme.{u})
    (hQ : (Q = (@IsOpenImmersion : MorphismProperty Scheme.{u})) ∨ IsDescentMorphismClass Q)
    [P.IsLocalAtTarget (Scheme.precoverage Q)]
    (hs : Presieve.ofArrows (fun _ : Unit => G.arrows.left)
      (fun _ => G.source.left) ∈ Scheme.precoverage Q G.objects.left)
    (ht : Presieve.ofArrows (fun _ : Unit => G.arrows.left)
      (fun _ => G.target.left) ∈ Scheme.precoverage Q G.objects.left) :
    IsInvariantOpen G (largestTargetOpen P G.source.left)

Tag 06QQ, a lemma

Tag 06QQ in the Stacks Project.

AlgebraicGeometry.isInvariantOpen_largestTargetOpen_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/StabilizerLargestOpen.lean, line 514.

Stacks Project, Tag 06QQ. For a groupoid scheme whose source and target maps are coverings for one of the fppf, syntomic, smooth or étale topologies, the largest open of the object scheme over which the stabilizer group scheme has a target-local property is invariant.

theorem isInvariantOpen_largestTargetOpen_stabilizer {S : Scheme.{u}} (G : GroupoidScheme S)
    (P Q : MorphismProperty Scheme.{u}) (hQ : IsDescentMorphismClass Q)
    [P.IsLocalAtTarget (Scheme.precoverage Q)]
    (hs : Presieve.ofArrows (fun _ : Unit => G.arrows.left)
      (fun _ => G.source.left) ∈ Scheme.precoverage Q G.objects.left)
    (ht : Presieve.ofArrows (fun _ : Unit => G.arrows.left)
      (fun _ => G.target.left) ∈ Scheme.precoverage Q G.objects.left) :
    IsInvariantOpen G (largestTargetOpen P (stabilizer G).hom)

Sources

Section40.7 Comparing fibres #

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

Tag 02YF, a lemma

Tag 02YF in the Stacks Project.

AlgebraicGeometry.exists_common_field_fiber_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CommonField.lean, line 134. The attribute's comment: “common_field”.

If two arrows in a groupoid scheme have the same target, then the fibres of the source map over their sources become isomorphic after extending both residue fields to a common field.

public theorem exists_common_field_fiber_iso {S : Scheme.{u}}
    (G : GroupoidScheme S) (r r' : G.arrows.left)
    (h : G.target.left r = G.target.left r') :
    ∃ (K : Type u) (_ : Field K)
      (_ : Algebra (G.objects.left.residueField (G.source.left r)) K)
      (_ : Algebra (G.objects.left.residueField (G.source.left r')) K),
      Nonempty
        (Over.mk (pullback.snd
          (G.source.left.fiberToSpecResidueField (G.source.left r))
          (Spec.map (CommRingCat.ofHom
            (algebraMap (G.objects.left.residueField (G.source.left r)) K)))) ≅
        Over.mk (pullback.snd
          (G.source.left.fiberToSpecResidueField (G.source.left r'))
          (Spec.map (CommRingCat.ofHom
            (algebraMap (G.objects.left.residueField (G.source.left r')) K)))))

AlgebraicGeometry.exists_common_field_fiber_iso_mapping_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CommonField.lean, line 162. The attribute's comment: “point_compatible”.

The common field and source-fibre isomorphism for two arrows with the same target can be chosen so that the isomorphism carries a point above the first arrow to a point above the second.

public theorem exists_common_field_fiber_iso_mapping_point {S : Scheme.{u}}
    (G : GroupoidScheme S) (r r' : G.arrows.left)
    (h : G.target.left r = G.target.left r') :
    ∃ (K : Type u) (_ : Field K)
      (_ : Algebra (G.objects.left.residueField (G.source.left r)) K)
      (_ : Algebra (G.objects.left.residueField (G.source.left r')) K),
      let g : Spec (.of K) ⟶ Spec (.of (G.objects.left.residueField (G.source.left r))) :=
        Spec.map (CommRingCat.ofHom
          (algebraMap (G.objects.left.residueField (G.source.left r)) K))
      let g' : Spec (.of K) ⟶ Spec (.of (G.objects.left.residueField (G.source.left r'))) :=
        Spec.map (CommRingCat.ofHom
          (algebraMap (G.objects.left.residueField (G.source.left r')) K))
      let P : Scheme.{u} :=
        pullback (G.source.left.fiberToSpecResidueField (G.source.left r)) g
      let _P' : Scheme.{u} :=
        pullback (G.source.left.fiberToSpecResidueField (G.source.left r')) g'
      let POver : Over (Spec (.of K)) := Over.mk
        (pullback.snd (G.source.left.fiberToSpecResidueField (G.source.left r)) g)
      let POver' : Over (Spec (.of K)) := Over.mk
        (pullback.snd (G.source.left.fiberToSpecResidueField (G.source.left r')) g')
      ∃ (x : P) (e : POver ≅ POver'),
        ((pullback.fst
            (G.source.left.fiberToSpecResidueField (G.source.left r)) g) ≫
              G.source.left.fiberι (G.source.left r)).base x = r ∧
          ((pullback.fst
            (G.source.left.fiberToSpecResidueField (G.source.left r')) g') ≫
              G.source.left.fiberι (G.source.left r')).base (e.hom.left.base x) = r'

AlgebraicGeometry.flatIsoLocallyOnBase_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/GermComparison.lean, line 170. The attribute's comment: “(3)”.

Stacks 02YF (3). If the source and target maps of a groupoid scheme are flat, then for two arrows with the same target the two germs of the source map, at the first arrow over its source and at the second arrow over its source, are flat locally on the base isomorphic.

theorem flatIsoLocallyOnBase_source {S : Scheme.{u}} (G : GroupoidScheme S)
    (hs : Flat G.source.left) (ht : Flat G.target.left)
    (r r' : G.arrows.left) (h : G.target.left r = G.target.left r') :
    FlatIsoLocallyOnBase G.source.left r G.source.left r'

AlgebraicGeometry.isoLocallyOnBase_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/GermComparison.lean, line 183. The attribute's comment: “(4)”.

Stacks 02YF (4). If the source and target maps of a groupoid scheme have a property P of morphisms of schemes, then for two arrows with the same target the two germs of the source map, at the first arrow over its source and at the second arrow over its source, are isomorphic locally on the base in the topology belonging to P.

theorem isoLocallyOnBase_source {S : Scheme.{u}} (G : GroupoidScheme S)
    (P : MorphismProperty Scheme.{u}) (hs : P G.source.left) (ht : P G.target.left)
    (r r' : G.arrows.left) (h : G.target.left r = G.target.left r') :
    IsoLocallyOnBase P G.source.left r G.source.left r'

AlgebraicGeometry.isoLocallyOnBase_source_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/GermComparison.lean, line 192. The attribute's comment: “(4) etale”.

Stacks 02YF (4), the étale case.

theorem isoLocallyOnBase_source_etale {S : Scheme.{u}} (G : GroupoidScheme S)
    (hs : Etale G.source.left) (ht : Etale G.target.left)
    (r r' : G.arrows.left) (h : G.target.left r = G.target.left r') :
    IsoLocallyOnBase @Etale G.source.left r G.source.left r'

AlgebraicGeometry.isoLocallyOnBase_source_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/GermComparison.lean, line 200. The attribute's comment: “(4) smooth”.

Stacks 02YF (4), the smooth case.

theorem isoLocallyOnBase_source_smooth {S : Scheme.{u}} (G : GroupoidScheme S)
    (hs : Smooth G.source.left) (ht : Smooth G.target.left)
    (r r' : G.arrows.left) (h : G.target.left r = G.target.left r') :
    IsoLocallyOnBase @Smooth G.source.left r G.source.left r'

AlgebraicGeometry.isoLocallyOnBase_source_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/GermComparison.lean, line 208. The attribute's comment: “(4) syntomic”.

Stacks 02YF (4), the syntomic case.

theorem isoLocallyOnBase_source_syntomic {S : Scheme.{u}} (G : GroupoidScheme S)
    (hs : Syntomic G.source.left) (ht : Syntomic G.target.left)
    (r r' : G.arrows.left) (h : G.target.left r = G.target.left r') :
    IsoLocallyOnBase @Syntomic G.source.left r G.source.left r'

AlgebraicGeometry.isoLocallyOnBase_source_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/GermComparison.lean, line 217. The attribute's comment: “(4) fppf”.

Stacks 02YF (4), the fppf case: source and target flat and locally of finite presentation.

theorem isoLocallyOnBase_source_fppf {S : Scheme.{u}} (G : GroupoidScheme S)
    (hs : Flat G.source.left) (hs' : LocallyOfFinitePresentation G.source.left)
    (ht : Flat G.target.left) (ht' : LocallyOfFinitePresentation G.target.left)
    (r r' : G.arrows.left) (h : G.target.left r = G.target.left r') :
    IsoLocallyOnBase (@Flat ⊓ @LocallyOfFinitePresentation) G.source.left r
      G.source.left r'

AlgebraicGeometry.source_fiber_comparison_of_target_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/GermComparison.lean, line 250.

Stacks 02YF. Let (U, R, s, t, c) be a groupoid over a scheme S and let r, r' be two arrows with the same target. Writing u = s r and u' = s r', and F_u = s⁻¹(u), F_{u'} = s⁻¹(u') for the scheme theoretic fibres of the source map:

there is a field k extending both κ(u) and κ(u') together with an isomorphism (F_u)_k ≅ (F_{u'})_k;

that isomorphism may be chosen so that a point lying over r maps to a point lying over r';

if s and t are flat then the morphisms of germs s : (R, r) ⟶ (U, u) and s : (R, r') ⟶ (U, u') are flat locally on the base isomorphic;

if s and t are étale (resp. smooth, syntomic, or flat and locally of finite presentation) then those two morphisms of germs are locally on the base isomorphic in the étale (resp. smooth, syntomic, fppf) topology.

The four parts are AlgebraicGeometry.exists_common_field_fiber_iso, AlgebraicGeometry.exists_common_field_fiber_iso_mapping_point, AlgebraicGeometry.flatIsoLocallyOnBase_source and the four cases AlgebraicGeometry.isoLocallyOnBase_source_etale, AlgebraicGeometry.isoLocallyOnBase_source_smooth, AlgebraicGeometry.isoLocallyOnBase_source_syntomic, AlgebraicGeometry.isoLocallyOnBase_source_fppf; the flatness, étaleness, smoothness, syntomicity and finite presentation assumptions of parts (3) and (4) appear as hypotheses of those parts, exactly as in the source, and not of the lemma.

theorem source_fiber_comparison_of_target_eq {S : Scheme.{u}} (G : GroupoidScheme S)
    (r r' : G.arrows.left) (h : G.target.left r = G.target.left r') :
    (∃ (K : Type u) (_ : Field K)
      (_ : Algebra (G.objects.left.residueField (G.source.left r)) K)
      (_ : Algebra (G.objects.left.residueField (G.source.left r')) K),
      Nonempty
        (Over.mk (pullback.snd
          (G.source.left.fiberToSpecResidueField (G.source.left r))
          (Spec.map (CommRingCat.ofHom
            (algebraMap (G.objects.left.residueField (G.source.left r)) K)))) ≅
        Over.mk (pullback.snd
          (G.source.left.fiberToSpecResidueField (G.source.left r'))
          (Spec.map (CommRingCat.ofHom
            (algebraMap (G.objects.left.residueField (G.source.left r')) K)))))) ∧
    (∃ (K : Type u) (_ : Field K)
      (_ : Algebra (G.objects.left.residueField (G.source.left r)) K)
      (_ : Algebra (G.objects.left.residueField (G.source.left r')) K),
      let g : Spec (.of K) ⟶ Spec (.of (G.objects.left.residueField (G.source.left r))) :=
        Spec.map (CommRingCat.ofHom
          (algebraMap (G.objects.left.residueField (G.source.left r)) K))
      let g' : Spec (.of K) ⟶ Spec (.of (G.objects.left.residueField (G.source.left r'))) :=
        Spec.map (CommRingCat.ofHom
          (algebraMap (G.objects.left.residueField (G.source.left r')) K))
      let P : Scheme.{u} :=
        pullback (G.source.left.fiberToSpecResidueField (G.source.left r)) g
      let _P' : Scheme.{u} :=
        pullback (G.source.left.fiberToSpecResidueField (G.source.left r')) g'
      let POver : Over (Spec (.of K)) := Over.mk
        (pullback.snd (G.source.left.fiberToSpecResidueField (G.source.left r)) g)
      let POver' : Over (Spec (.of K)) := Over.mk
        (pullback.snd (G.source.left.fiberToSpecResidueField (G.source.left r')) g')
      ∃ (x : P) (e : POver ≅ POver'),
        ((pullback.fst
            (G.source.left.fiberToSpecResidueField (G.source.left r)) g) ≫
              G.source.left.fiberι (G.source.left r)).base x = r ∧
          ((pullback.fst
            (G.source.left.fiberToSpecResidueField (G.source.left r')) g') ≫
              G.source.left.fiberι (G.source.left r')).base (e.hom.left.base x) = r') ∧
    (Flat G.source.left → Flat G.target.left →
      FlatIsoLocallyOnBase G.source.left r G.source.left r') ∧
    (Etale G.source.left → Etale G.target.left →
      IsoLocallyOnBase @Etale G.source.left r G.source.left r') ∧
    (Smooth G.source.left → Smooth G.target.left →
      IsoLocallyOnBase @Smooth G.source.left r G.source.left r') ∧
    (Syntomic G.source.left → Syntomic G.target.left →
      IsoLocallyOnBase @Syntomic G.source.left r G.source.left r') ∧
    (Flat G.source.left → LocallyOfFinitePresentation G.source.left →
      Flat G.target.left → LocallyOfFinitePresentation G.target.left →
      IsoLocallyOnBase (@Flat ⊓ @LocallyOfFinitePresentation) G.source.left r
        G.source.left r')

Sources

LeanAlgebraicGeometry.exists_common_field_fiber_iso · AlgebraicGeometry.exists_common_field_fiber_iso_mapping_point · AlgebraicGeometry.flatIsoLocallyOnBase_source · AlgebraicGeometry.isoLocallyOnBase_source · AlgebraicGeometry.isoLocallyOnBase_source_etale · AlgebraicGeometry.isoLocallyOnBase_source_smooth · AlgebraicGeometry.isoLocallyOnBase_source_syntomic · AlgebraicGeometry.isoLocallyOnBase_source_fppf

Section40.8 Cohen-Macaulay presentations #

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

Tag 0460, a lemma

Tag 0460 in the Stacks Project.

AlgebraicGeometry.exists_open_source_cohenMacaulay_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CohenMacaulayRestriction.lean, line 324. The attribute's comment: “part (1)”.

There is an open of objects whose inverse image under the target is the greatest open on which the source map is Cohen–Macaulay.

public theorem exists_open_source_cohenMacaulay_locus {S : Scheme.{u}}
    (G : GroupoidScheme S)
    [Flat G.source.left] [Flat G.target.left]
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left] :
    ∃ W : G.objects.left.Opens,
      IsGreatest
        {V : G.arrows.left.Opens |
          ∃ hf : ∀ y : G.objects.left,
            IsLocallyNoetherian ((V.ι ≫ G.source.left).fiber y),
            Scheme.Hom.IsCohenMacaulay (V.ι ≫ G.source.left) hf}
        (G.target.left ⁻¹ᵁ W)

AlgebraicGeometry.target_cohenMacaulay_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CohenMacaulayRestriction.lean, line 382. The attribute's comment: “part (2)”.

The inverse image of the object open under the source is the greatest open on which the target map is Cohen–Macaulay.

public theorem target_cohenMacaulay_locus {S : Scheme.{u}} (G : GroupoidScheme S)
    [Flat G.source.left] [Flat G.target.left]
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left] :
    IsGreatest
      {V : G.arrows.left.Opens |
        ∃ hf : ∀ y : G.objects.left,
          IsLocallyNoetherian ((V.ι ≫ G.target.left).fiber y),
          Scheme.Hom.IsCohenMacaulay (V.ι ≫ G.target.left) hf}
      (G.source.left ⁻¹ᵁ cohenMacaulayOpen G)

AlgebraicGeometry.target_from_source_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CohenMacaulayRestriction.lean, line 477. The attribute's comment: “part (3)”.

The target remains surjective on the inverse image of the open under the source.

public theorem target_from_source_surjective {S : Scheme.{u}} (G : GroupoidScheme S)
    [Flat G.source.left] [Flat G.target.left]
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left] :
    Surjective ((G.source.left ⁻¹ᵁ cohenMacaulayOpen G).ι ≫ G.target.left)

AlgebraicGeometry.source_from_target_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CohenMacaulayRestriction.lean, line 487. The attribute's comment: “part (4)”.

The source remains surjective on the inverse image of the open under the target.

public theorem source_from_target_surjective {S : Scheme.{u}} (G : GroupoidScheme S)
    [Flat G.source.left] [Flat G.target.left]
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left] :
    Surjective ((G.target.left ⁻¹ᵁ cohenMacaulayOpen G).ι ≫ G.source.left)

AlgebraicGeometry.restricted_source_cohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CohenMacaulayRestriction.lean, line 588. The attribute's comment: “part (5): source Cohen–Macaulay”.

The source map of the restricted groupoid is Cohen–Macaulay.

public theorem restricted_source_cohenMacaulay {S : Scheme.{u}} (G : GroupoidScheme S)
    [Flat G.source.left] [Flat G.target.left]
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left] :
    let U' := cohenMacaulayOpen G
    let g : Over.mk (U'.ι ≫ G.objects.hom) ⟶ G.objects := Over.homMk U'.ι
    let f := (GroupoidScheme.restrict G g).groupoid.source.left
    ∃ hf : ∀ y, IsLocallyNoetherian (f.fiber y),
      Scheme.Hom.IsCohenMacaulay f hf

AlgebraicGeometry.restricted_target_cohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CohenMacaulayRestriction.lean, line 631. The attribute's comment: “part (5): target Cohen–Macaulay”.

The target map of the restricted groupoid is Cohen–Macaulay.

public theorem restricted_target_cohenMacaulay {S : Scheme.{u}} (G : GroupoidScheme S)
    [Flat G.source.left] [Flat G.target.left]
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left] :
    let U' := cohenMacaulayOpen G
    let g : Over.mk (U'.ι ≫ G.objects.hom) ⟶ G.objects := Over.homMk U'.ι
    let f := (GroupoidScheme.restrict G g).groupoid.target.left
    ∃ hf : ∀ y, IsLocallyNoetherian (f.fiber y),
      Scheme.Hom.IsCohenMacaulay f hf

AlgebraicGeometry.restricted_source_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CohenMacaulayRestriction.lean, line 655. The attribute's comment: “part (5): source locally of finite presentation”.

The source map of the restricted groupoid is locally of finite presentation.

public theorem restricted_source_locallyOfFinitePresentation {S : Scheme.{u}}
    (G : GroupoidScheme S) [Flat G.source.left] [Flat G.target.left]
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left] :
    let U' := cohenMacaulayOpen G
    let g : Over.mk (U'.ι ≫ G.objects.hom) ⟶ G.objects := Over.homMk U'.ι
    LocallyOfFinitePresentation (GroupoidScheme.restrict G g).groupoid.source.left

AlgebraicGeometry.restricted_target_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CohenMacaulayRestriction.lean, line 666. The attribute's comment: “part (5): target locally of finite presentation”.

The target map of the restricted groupoid is locally of finite presentation.

public theorem restricted_target_locallyOfFinitePresentation {S : Scheme.{u}}
    (G : GroupoidScheme S) [Flat G.source.left] [Flat G.target.left]
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left] :
    let U' := cohenMacaulayOpen G
    let g : Over.mk (U'.ι ≫ G.objects.hom) ⟶ G.objects := Over.homMk U'.ι
    LocallyOfFinitePresentation (GroupoidScheme.restrict G g).groupoid.target.left

Sources

LeanAlgebraicGeometry.exists_open_source_cohenMacaulay_locus · AlgebraicGeometry.target_cohenMacaulay_locus · AlgebraicGeometry.target_from_source_surjective · AlgebraicGeometry.source_from_target_surjective · AlgebraicGeometry.restricted_source_cohenMacaulay · AlgebraicGeometry.restricted_target_cohenMacaulay · AlgebraicGeometry.restricted_source_locallyOfFinitePresentation · AlgebraicGeometry.restricted_target_locallyOfFinitePresentation

Section40.9 Restricting groupoids #

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

Tag 04MN, an equation

Tag 04MN in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.restrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/RestrictionGroupoid.lean, line 69. The attribute's comment: “R' is the iterated fibre product of the displayed diagram and s', t' are its”.

Restriction of a groupoid scheme along a morphism to its scheme of objects.

noncomputable def restrict {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S)
    {U' : Over S} (g : U' ⟶ G.objects) : Restriction G g

Tag 04MP, a lemma

Tag 04MP in the Stacks Project.

AlgebraicGeometry.restrictionSource_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionProperties.lean, line 173. The attribute's comment: “part (1), source map”.

The source map of a restriction is locally of finite type if the original source map and the restricting morphism are locally of finite type.

public theorem restrictionSource_locallyOfFiniteType {S : Scheme.{u}}
    (G : GroupoidScheme S) {U' : Scheme.{u}} (g : U' ⟶ G.objects.left)
    [LocallyOfFiniteType G.source.left] [LocallyOfFiniteType g] :
    let U'_S : Over S := Over.mk (g ≫ G.objects.hom)
    let g' : U'_S ⟶ G.objects := Over.homMk g
    LocallyOfFiniteType (GroupoidScheme.restrict G g').groupoid.source.left

AlgebraicGeometry.restrictionTarget_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionProperties.lean, line 185. The attribute's comment: “part (1), target map”.

The target map of a restriction is locally of finite type if the original target map and the restricting morphism are locally of finite type.

public theorem restrictionTarget_locallyOfFiniteType {S : Scheme.{u}}
    (G : GroupoidScheme S) {U' : Scheme.{u}} (g : U' ⟶ G.objects.left)
    [LocallyOfFiniteType G.target.left] [LocallyOfFiniteType g] :
    let U'_S : Over S := Over.mk (g ≫ G.objects.hom)
    let g' : U'_S ⟶ G.objects := Over.homMk g
    LocallyOfFiniteType (GroupoidScheme.restrict G g').groupoid.target.left

AlgebraicGeometry.restrictionSource_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionProperties.lean, line 197. The attribute's comment: “part (2), source map”.

The source map of a restriction is locally of finite presentation if the original source map and the restricting morphism are locally of finite presentation.

public theorem restrictionSource_locallyOfFinitePresentation {S : Scheme.{u}}
    (G : GroupoidScheme S) {U' : Scheme.{u}} (g : U' ⟶ G.objects.left)
    [LocallyOfFinitePresentation G.source.left] [LocallyOfFinitePresentation g] :
    let U'_S : Over S := Over.mk (g ≫ G.objects.hom)
    let g' : U'_S ⟶ G.objects := Over.homMk g
    LocallyOfFinitePresentation
      (GroupoidScheme.restrict G g').groupoid.source.left

AlgebraicGeometry.restrictionTarget_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionProperties.lean, line 210. The attribute's comment: “part (2), target map”.

The target map of a restriction is locally of finite presentation if the original target map and the restricting morphism are locally of finite presentation.

public theorem restrictionTarget_locallyOfFinitePresentation {S : Scheme.{u}}
    (G : GroupoidScheme S) {U' : Scheme.{u}} (g : U' ⟶ G.objects.left)
    [LocallyOfFinitePresentation G.target.left] [LocallyOfFinitePresentation g] :
    let U'_S : Over S := Over.mk (g ≫ G.objects.hom)
    let g' : U'_S ⟶ G.objects := Over.homMk g
    LocallyOfFinitePresentation
      (GroupoidScheme.restrict G g').groupoid.target.left

AlgebraicGeometry.restrictionSource_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionProperties.lean, line 223. The attribute's comment: “part (3), source map”.

The source map of a restriction is flat if the original source map and the restricting morphism are flat.

public theorem restrictionSource_flat {S : Scheme.{u}} (G : GroupoidScheme S)
    {U' : Scheme.{u}} (g : U' ⟶ G.objects.left) [Flat G.source.left] [Flat g] :
    let U'_S : Over S := Over.mk (g ≫ G.objects.hom)
    let g' : U'_S ⟶ G.objects := Over.homMk g
    Flat (GroupoidScheme.restrict G g').groupoid.source.left

AlgebraicGeometry.restrictionTarget_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionProperties.lean, line 234. The attribute's comment: “part (3), target map”.

The target map of a restriction is flat if the original target map and the restricting morphism are flat.

public theorem restrictionTarget_flat {S : Scheme.{u}} (G : GroupoidScheme S)
    {U' : Scheme.{u}} (g : U' ⟶ G.objects.left) [Flat G.target.left] [Flat g] :
    let U'_S : Over S := Over.mk (g ≫ G.objects.hom)
    let g' : U'_S ⟶ G.objects := Over.homMk g
    Flat (GroupoidScheme.restrict G g').groupoid.target.left

Tag 04MV, a lemma

Tag 04MV in the Stacks Project.

AlgebraicGeometry.restriction_source_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionProperties.lean, line 149. The attribute's comment: “source map”.

The source map of a restriction has every morphism property which is stable under base change and holds for the source map after pulling back the target.

public theorem restriction_source_mem {S : Scheme.{u}} (G : GroupoidScheme S) {U' : Over S}
    (g : U' ⟶ G.objects) (R : GroupoidScheme.Restriction G g)
    (P : MorphismProperty Scheme) [P.IsStableUnderBaseChange]
    (hP : P ((pullback.snd g G.target ≫ G.source).left)) :
    P R.groupoid.source.left

AlgebraicGeometry.restriction_target_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionProperties.lean, line 159. The attribute's comment: “target map”.

The target map of a restriction has every morphism property which is stable under base change and holds for the source map after pulling back the target.

public theorem restriction_target_mem {S : Scheme.{u}} (G : GroupoidScheme S) {U' : Over S}
    (g : U' ⟶ G.objects) (R : GroupoidScheme.Restriction G g)
    (P : MorphismProperty Scheme) [P.IsStableUnderBaseChange]
    (hP : P ((pullback.snd g G.target ≫ G.source).left)) :
    P R.groupoid.target.left

Tag 04MW, a lemma

Tag 04MW in the Stacks Project.

AlgebraicGeometry.doubleRestrictionDiagram, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/DoubleRestriction.lean, line 326.

Stacks Project, Tag 04MW. Restricting a groupoid scheme successively along g and g' gives a comparison diagram whose two squares are cartesian; the comparison arrow is given by composing the second arrow with the inverse of the first.

public noncomputable def doubleRestrictionDiagram {S : Scheme.{u}} (G : GroupoidScheme S)
    {U' U'' : Over S} (g : U' ⟶ G.objects) (g' : U'' ⟶ U') :
    DoubleRestrictionDiagram G g g'

Tag 04MX, a lemma

Tag 04MX in the Stacks Project.

AlgebraicGeometry.restrictionSource_mem_of_composite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/DoubleRestrictionDescent.lean, line 64. The attribute's comment: “pullback_to_second_restriction”.

A property of the source map over a composite restriction descends to the source map over the second restriction when the original target map covers.

public theorem restrictionSource_mem_of_composite {S : Scheme.{u}} (G : GroupoidScheme S)
    {U' U'' : Over S} (g : U' ⟶ G.objects) (g' : U'' ⟶ U')
    (K : Precoverage Scheme.{u}) [K.IsStableUnderBaseChange]
    (P : MorphismProperty Scheme.{u}) [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget K]
    (ht : Presieve.singleton G.target.left ∈ K G.objects.left)
    (hP : P ((pullback.snd (g' ≫ g) G.target ≫ G.source).left)) :
    P ((pullback.snd g' (restrictionTarget G g) ≫ restrictionSource G g).left)

AlgebraicGeometry.descent_to_open_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/DoubleRestrictionDescent.lean, line 99. The attribute's comment: “descent_to_open_image”.

A morphism property local on the target descends from the source map of a restriction to the source map after a further restriction, viewed over the open image of the first source map.

public theorem descent_to_open_image {S : Scheme.{u}} (G : GroupoidScheme S)
    {U' U'' : Over S} (g : U' ⟶ G.objects) (g' : U'' ⟶ U')
    (K : Precoverage Scheme.{u}) (P : MorphismProperty Scheme.{u})
    [P.IsStableUnderBaseChange] [P.IsLocalAtTarget K]
    (V : G.objects.left.Opens)
    (hV : (firstArrowSource G g).left ⟶ V.toScheme)
    (hV_fac : hV ≫ V.ι = (firstSourceMap G g).left)
    (_hV_range : Set.range (firstSourceMap G g).left = (V : Set G.objects.left))
    (hV_cover : Presieve.singleton hV ∈ K V.toScheme)
    (hP : P (secondSourceMap G g g').left) :
    ∃ hV' : (compositeArrowSource G g g').left ⟶ V.toScheme,
      hV' ≫ V.ι = (compositeSourceMap G g g').left ∧ P hV'

Sources

LeanAlgebraicGeometry.GroupoidScheme.restrict · AlgebraicGeometry.restrictionSource_locallyOfFiniteType · AlgebraicGeometry.restrictionTarget_locallyOfFiniteType · AlgebraicGeometry.restrictionSource_locallyOfFinitePresentation · AlgebraicGeometry.restrictionTarget_locallyOfFinitePresentation · AlgebraicGeometry.restrictionSource_flat · AlgebraicGeometry.restrictionTarget_flat · AlgebraicGeometry.restriction_source_mem

Section40.10 Properties of groupoids on fields #

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

Tag 04LM, a lemma

Tag 04LM in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.isOpenMap_comp_of_objects_isFieldSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/CompositionOpen.lean, line 42.

Composition in a groupoid scheme is an open map when the scheme of objects is the spectrum of a field.

public theorem isOpenMap_comp_of_objects_isFieldSpectrum
    {S : Scheme.{u}} (G : GroupoidScheme S)
    (k : Type u) [Field k] (e : G.objects.left ≅ Spec (.of k)) :
    IsOpenMap G.comp.left

Tag 04LN, a lemma

Tag 04LN in the Stacks Project.

AlgebraicGeometry.isSeparated_arrows_of_objects_isSpec_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Separated.lean, line 50.

Stacks Project, Tag 04LN. The arrow scheme of a groupoid scheme with object scheme the spectrum of a field is separated.

public theorem isSeparated_arrows_of_objects_isSpec_field
    {S : Scheme.{u}} (G : GroupoidScheme S) {k : Type u} [Field k]
    (_ : G.objects.left ≅ Spec (.of k)) : G.arrows.left.IsSeparated

Tag 04LP, a lemma

Tag 04LP in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.exists_fieldExtension_sourceFiber_iso_mapping_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FieldExtensionFiber.lean, line 85.

If the object scheme of a groupoid scheme is the spectrum of a field k, then any two points of its arrow scheme lift, after a field extension k'/k, to points of two base changes of the arrow scheme along the source map which are carried to one another by an isomorphism over Spec k'.

The two base changes are taken along the two k-algebra structures on k' that Tag 02YF produces, namely the ones induced by the target and by the source of a chosen arrow.

theorem exists_fieldExtension_sourceFiber_iso_mapping_points
    {S : Scheme.{u}} (G : GroupoidScheme S)
    (k : Type u) [Field k] (e : G.objects.left ≅ Spec (.of k))
    (r r' : G.arrows.left) :
    let s : G.arrows.left ⟶ Spec (.of k) := G.source.left ≫ e.hom
    ∃ (k' : Type u) (_ : Field k') (α β : Algebra k k'),
      let gt : Spec (.of k') ⟶ Spec (.of k) :=
        Spec.map (CommRingCat.ofHom (@algebraMap k k' _ _ α))
      let gs : Spec (.of k') ⟶ Spec (.of k) :=
        Spec.map (CommRingCat.ofHom (@algebraMap k k' _ _ β))
      let P : Scheme.{u} := pullback s gt
      let P' : Scheme.{u} := pullback s gs
      let POver : Over (Spec (.of k')) := Over.mk (pullback.snd s gt)
      let POver' : Over (Spec (.of k')) := Over.mk (pullback.snd s gs)
      ∃ (r₁ : P) (r₂ : P') (φ : POver ≅ POver'),
        φ.hom.left.base r₁ = r₂ ∧
          (pullback.fst s gt).base r₁ = r ∧
          (pullback.fst s gs).base r₂ = r'

Tag 04LQ, a lemma

Tag 04LQ in the Stacks Project.

AlgebraicGeometry.surjective_restrictionDiagramMorphisms, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionOverField.lean, line 102. The attribute's comment: “surjectivity”.

Every morphism in the defining restriction diagram over a field extension is surjective.

public lemma surjective_restrictionDiagramMorphisms {S : Scheme.{u}} (G : GroupoidScheme S)
    {U' : Over S} (g : U' ⟶ G.objects) (k k' : Type u) [Field k] [Field k']
    (_ : G.objects.left ≅ Spec (.of k)) (_ : U'.left ≅ Spec (.of k'))
    (i : Fin 12) :
    Surjective ((restrictionDiagramMorphisms G g i).hom)

AlgebraicGeometry.flat_restrictionDiagramMorphisms, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionOverField.lean, line 115. The attribute's comment: “flatness”.

Every morphism in the defining restriction diagram over a field extension is flat.

public lemma flat_restrictionDiagramMorphisms {S : Scheme.{u}} (G : GroupoidScheme S)
    {U' : Over S} (g : U' ⟶ G.objects) (k k' : Type u) [Field k] [Field k']
    (_ : G.objects.left ≅ Spec (.of k)) (_ : U'.left ≅ Spec (.of k'))
    (i : Fin 12) :
    Flat ((restrictionDiagramMorphisms G g i).hom)

AlgebraicGeometry.universallyOpen_restrictionDiagramMorphisms, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionOverField.lean, line 128. The attribute's comment: “universal openness”.

Every morphism in the defining restriction diagram over a field extension is universally open.

public lemma universallyOpen_restrictionDiagramMorphisms {S : Scheme.{u}}
    (G : GroupoidScheme S) {U' : Over S} (g : U' ⟶ G.objects)
    (k k' : Type u) [Field k] [Field k']
    (_ : G.objects.left ≅ Spec (.of k)) (_ : U'.left ≅ Spec (.of k'))
    (i : Fin 12) :
    UniversallyOpen ((restrictionDiagramMorphisms G g i).hom)

AlgebraicGeometry.isAffineHom_restrictionArrowsToArrows, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/RestrictionOverField.lean, line 142. The attribute's comment: “affineness of the dotted morphism”.

The dotted morphism from the arrow scheme of a restriction to the original arrow scheme is affine.

public lemma isAffineHom_restrictionArrowsToArrows {S : Scheme.{u}} (G : GroupoidScheme S)
    {U' : Over S} (g : U' ⟶ G.objects) (k k' : Type u) [Field k] [Field k']
    (_ : G.objects.left ≅ Spec (.of k)) (_ : U'.left ≅ Spec (.of k')) :
    IsAffineHom (restrictionArrowsToArrows G g).left

Tag 04LR, a lemma

Tag 04LR in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.exists_isIso_source_target_over_isAlgClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/PointsOverField.lean, line 218.

An arrow over a point of a groupoid scheme on Spec k can be lifted after an algebraically closed extension of k so that both its source and target induce isomorphisms from the extending field to the residue field of the lifted point.

public theorem exists_isIso_source_target_over_isAlgClosed {S : Scheme.{u}} {k : Type u}
    [Field k] (structureMap : Spec (.of k) ⟶ S) (G : GroupoidScheme S)
    (objects_eq : G.objects = Over.mk structureMap) (r : G.arrows.left) :
    ∃ (k' : Type u) (_ : Field k') (_ : IsAlgClosed k') (i : k →+* k'),
      let g : Over.mk (Scheme.Spec.map (CommRingCat.ofHom i).op ≫ structureMap) ⟶ G.objects :=
        extensionMap structureMap i ≫ eqToHom objects_eq.symm
      ∃ (r' : Spec (.of k') ⟶ (restrictionArrows G g).left),
      let rPoint := r' (IsLocalRing.closedPoint k')
      (restrictionArrowsToArrows G g).left rPoint = r ∧
        IsIso ((restrictionSource G g).left.residueFieldMap rPoint) ∧
        IsIso ((restrictionTarget G g).left.residueFieldMap rPoint)

Tag 04LS, a lemma

Tag 04LS in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.translationByPoint_isIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Translation.lean, line 460. The attribute's comment: “the automorphism”.

Stacks Project, Tag 04LS. Translation by a point whose source and target induce isomorphisms on residue fields is an automorphism of the arrow scheme.

public lemma translationByPoint_isIso {S : Scheme.{u}} (G : GroupoidScheme S)
    (k : Type u) [Field k] (hU : G.objects.left = Spec (.of k))
    (r : G.arrows.left) [IsIso (G.source.left.residueFieldMap r)]
    [IsIso (G.target.left.residueFieldMap r)] :
    IsIso (translationByPoint G k hU r)

AlgebraicGeometry.GroupoidScheme.identity_image_translationByPoint, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Translation.lean, line 473. The attribute's comment: “image of the identity”.

Stacks Project, Tag 04LS. Translation by r maps the identity arrow at the source of r to r.

public lemma identity_image_translationByPoint {S : Scheme.{u}} (G : GroupoidScheme S)
    (k : Type u) [Field k] (hU : G.objects.left = Spec (.of k))
    (r : G.arrows.left) [IsIso (G.source.left.residueFieldMap r)] :
    (G.identity ≫ translationByPoint G k hU r).left (G.source.left r) = r

Tag 0B7V, a lemma

Tag 0B7V in the Stacks Project.

AlgebraicGeometry.isOpen_image_comp_of_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/OpenTranslates.lean, line 254.

Stacks Project, Tag 0B7V. If the objects of a groupoid scheme form the spectrum of a field, the image of the composition of a family of arrows with an open set of arrows is open.

public theorem isOpen_image_comp_of_isOpen
    {S : Scheme.{u}} (G : GroupoidScheme S) (k : Type u) [Field k]
    (hobjects : G.objects.left ≅ Spec (.of k))
    (Z : Over S) (f : Z ⟶ G.arrows) (W : G.arrows.left.Opens) :
    let p := pullback.snd f (pullback.fst G.source G.target)
    IsOpen ((p ≫ G.comp).left.base ''
      {x | (p ≫ pullback.snd G.source G.target).left.base x ∈ W})

Tag 04LT, a lemma

Tag 04LT in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.existsUnique_minimalPrime_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/IrreducibleComponents.lean, line 575. The attribute's comment: “part (1)”.

Stacks Project, Tag 04LT. Every local ring of the arrows of a groupoid scheme over a field has a unique minimal prime ideal.

public theorem existsUnique_minimalPrime_stalk {S : Scheme.{u}} (G : GroupoidScheme S)
    (k : Type u) [Field k] (hU : G.objects.left = Spec (.of k))
    (r : G.arrows.left) :
    ∃! p : Ideal (G.arrows.left.presheaf.stalk r),
      p ∈ minimalPrimes (G.arrows.left.presheaf.stalk r)

AlgebraicGeometry.GroupoidScheme.existsUnique_irreducibleComponent_containing_identity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/IrreducibleComponents.lean, line 633. The attribute's comment: “part (2)”.

Stacks Project, Tag 04LT. There is exactly one irreducible component of the arrow scheme containing the identity section.

public theorem existsUnique_irreducibleComponent_containing_identity
    {S : Scheme.{u}} (G : GroupoidScheme S) (k : Type u) [Field k]
    (hU : G.objects.left = Spec (.of k)) :
    ∃! Z : irreducibleComponents G.arrows.left,
      Set.range G.identity.left ⊆ (Z : Set G.arrows.left)

AlgebraicGeometry.GroupoidScheme.geometricallyIrreducible_irreducibleComponent_of_identity_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/IrreducibleComponents.lean, line 838. The attribute's comment: “part (3), source”. References: EGA IV (15.6.10), “partial”; SGA 3 VIA (2.6.2), “more general”; SGA 3 VIA (2.6.5), “more general”.

Stacks Project, Tag 04LT. The component containing the identity is geometrically irreducible over the field via the source morphism.

public theorem geometricallyIrreducible_irreducibleComponent_of_identity_source
    {S : Scheme.{u}} (G : GroupoidScheme S) (k : Type u) [Field k]
    (hU : G.objects.left = Spec (.of k)) (Z : irreducibleComponents G.arrows.left)
    (he : Set.range G.identity.left ⊆ (Z : Set G.arrows.left)) :
    GeometricallyIrreducible
      ((Scheme.IdealSheafData.vanishingIdeal
        (⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.2⟩ :
          Closeds G.arrows.left)).subschemeι ≫ G.source.left ≫ eqToHom hU)

AlgebraicGeometry.GroupoidScheme.geometricallyIrreducible_irreducibleComponent_of_identity_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/IrreducibleComponents.lean, line 855. The attribute's comment: “part (3), target”. References: EGA IV (15.6.10), “partial”; SGA 3 VIA (2.6.2), “more general”; SGA 3 VIA (2.6.5), “more general”.

Stacks Project, Tag 04LT. The component containing the identity is geometrically irreducible over the field via the target morphism.

public theorem geometricallyIrreducible_irreducibleComponent_of_identity_target
    {S : Scheme.{u}} (G : GroupoidScheme S) (k : Type u) [Field k]
    (hU : G.objects.left = Spec (.of k)) (Z : irreducibleComponents G.arrows.left)
    (he : Set.range G.identity.left ⊆ (Z : Set G.arrows.left)) :
    GeometricallyIrreducible
      ((Scheme.IdealSheafData.vanishingIdeal
        (⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.2⟩ :
          Closeds G.arrows.left)).subschemeι ≫ G.target.left ≫ eqToHom hU)

Tag 04LU, a lemma

Tag 04LU in the Stacks Project.

AlgebraicGeometry.trdeg_residueField_eq_of_target_isSpec_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/Dimension.lean, line 159. The attribute's comment: “transcendence_degrees”.

Stacks Project, Tag 04LU. The transcendence degree of the residue field at a point of a scheme over the residue field of its image does not depend on which morphism locally of finite type to the spectrum of a field is used.

theorem trdeg_residueField_eq_of_target_isSpec_field {X Y : Scheme.{u}} {k : Type u} [Field k]
    (e : Y ≅ Spec (.of k)) (f g : X ⟶ Y) [LocallyOfFiniteType f] [LocallyOfFiniteType g]
    (x : X) :
    letI : Algebra (Y.residueField (f x)) (X.residueField x) :=
      (f.residueFieldMap x).hom.toAlgebra
    letI : Algebra (Y.residueField (g x)) (X.residueField x) :=
      (g.residueFieldMap x).hom.toAlgebra
    Algebra.trdeg (Y.residueField (f x)) (X.residueField x) =
      Algebra.trdeg (Y.residueField (g x)) (X.residueField x)

AlgebraicGeometry.GroupoidScheme.topologicalKrullDim_arrows_eq_topologicalKrullDimAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/Dimension.lean, line 230. The attribute's comment: “dimension_at_every_point”.

Stacks Project, Tag 04LU. The dimension of the arrow scheme of a groupoid scheme whose object scheme is the spectrum of a field is its local dimension at every point, provided both structure morphisms are locally of finite type.

theorem topologicalKrullDim_arrows_eq_topologicalKrullDimAt {S : Scheme.{u}}
    (G : GroupoidScheme S) {k : Type u} [Field k] (e : G.objects.left ≅ Spec (.of k))
    [LocallyOfFiniteType G.source.left] [LocallyOfFiniteType G.target.left]
    (r : G.arrows.left) :
    topologicalKrullDim G.arrows.left = topologicalKrullDimAt G.arrows.left r

AlgebraicGeometry.GroupoidScheme.topologicalKrullDim_arrows_eq_ringKrullDim_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/Dimension.lean, line 244. The attribute's comment: “dimension_at_closed_point”.

Stacks Project, Tag 04LU. At a closed point of the arrow scheme of a groupoid scheme whose object scheme is the spectrum of a field, the dimension of the arrow scheme is the Krull dimension of the local ring.

theorem topologicalKrullDim_arrows_eq_ringKrullDim_stalk {S : Scheme.{u}}
    (G : GroupoidScheme S) {k : Type u} [Field k] (e : G.objects.left ≅ Spec (.of k))
    [LocallyOfFiniteType G.source.left] [LocallyOfFiniteType G.target.left]
    (r : G.arrows.left) (hr : IsClosed ({r} : Set G.arrows.left)) :
    topologicalKrullDim G.arrows.left = ringKrullDim (G.arrows.left.presheaf.stalk r)

AlgebraicGeometry.GroupoidScheme.equidimensional_arrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/Dimension.lean, line 257. The attribute's comment: “equidimensional”.

Stacks Project, Tag 04LU. The arrow scheme of a groupoid scheme whose object scheme is the spectrum of a field is equidimensional, provided both structure morphisms are locally of finite type.

theorem equidimensional_arrows {S : Scheme.{u}} (G : GroupoidScheme S) {k : Type u} [Field k]
    (e : G.objects.left ≅ Spec (.of k)) [LocallyOfFiniteType G.source.left]
    [LocallyOfFiniteType G.target.left] :
    Equidimensional G.arrows.left

Tag 04MQ, a lemma

Tag 04MQ in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.topologicalKrullDim_arrows_eq_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/StabilizerDimension.lean, line 142.

Stacks Project, Tag 04MQ. The arrow scheme of a groupoid scheme whose object scheme is the spectrum of a field has the same dimension as its stabilizer group scheme, provided both structure morphisms are locally of finite type.

theorem topologicalKrullDim_arrows_eq_stabilizer
    {S : Scheme.{u}} (G : GroupoidScheme S)
    {k : Type u} [Field k] (e : G.objects.left ≅ Spec (.of k))
    [LocallyOfFiniteType G.source.left] [LocallyOfFiniteType G.target.left] :
    topologicalKrullDim G.arrows.left = topologicalKrullDim (stabilizer G).left

Tag 04MR, a remark

Tag 04MR in the Stacks Project.

AlgebraicGeometry.RationalFunctionPairGroupoid.groupoid, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/DimensionWithoutFiniteType.lean, line 702. The attribute's comment: “the groupoid scheme of the warning, as the pair groupoid of Spec Q(x) over Q”.

The groupoid scheme of the warning. The restriction of the groupoid scheme of the multiplicative action of 𝐆_{m,𝐐} on 𝐀¹_𝐐 to the generic point of 𝐀¹_𝐐, presented as the pair groupoid of Spec 𝐐(x) → Spec 𝐐: its object scheme is Spec 𝐐(x), the spectrum of a field, and its arrow scheme is Spec 𝐐(x) ×_{Spec 𝐐} Spec 𝐐(x), whose ring of functions is the arrow ring 𝐐(x)[Y][1/P(Y)] of the source.

noncomputable def groupoid : GroupoidScheme (Spec (CommRingCat.of ℚ))

AlgebraicGeometry.RationalFunctionPairGroupoid.topologicalKrullDim_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/DimensionWithoutFiniteType.lean, line 735. The attribute's comment: “dim G = 0”.

The stabilizer group scheme has dimension zero: the second projection of its defining square carries it isomorphically onto Spec 𝐐(x).

theorem topologicalKrullDim_stabilizer :
    topologicalKrullDim (stabilizer groupoid).left = 0

AlgebraicGeometry.RationalFunctionPairGroupoid.topologicalKrullDim_arrows_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/DimensionWithoutFiniteType.lean, line 762. The attribute's comment: “dim R = 1”.

The arrow scheme has dimension one.

theorem topologicalKrullDim_arrows_eq_one :
    topologicalKrullDim groupoid.arrows.left = 1

AlgebraicGeometry.RationalFunctionPairGroupoid.topologicalKrullDim_arrows_ne_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/DimensionWithoutFiniteType.lean, line 774. The attribute's comment: “dim R = 1 ≠ 0 = dim G there, so the conclusion of Tag 04MQ fails for this groupoid scheme; that its source and target are not locally of finite type, which is the hypothesis of Tag 04MQ the example drops, is proved below”.

The conclusion of Tag 04MQ fails for this groupoid scheme. Its object scheme is the spectrum of a field, yet the dimension of its arrow scheme is not the dimension of its stabilizer group scheme: the stabilizer has dimension zero and the arrows have dimension one. The source and target morphisms are not locally of finite type, which is the hypothesis of Tag 04MQ that this example drops.

theorem topologicalKrullDim_arrows_ne_stabilizer :
    topologicalKrullDim groupoid.arrows.left
      ≠ topologicalKrullDim (stabilizer groupoid).left

AlgebraicGeometry.RationalFunctionPairGroupoid.not_locallyOfFiniteType_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/DimensionWithoutFiniteType.lean, line 791. The attribute's comment: “s is not locally of finite type”.

The source of the groupoid scheme is not locally of finite type. On rings it is the inclusion of 𝐐(x) into 𝐐(x) ⊗_𝐐 𝐐(x) as the right factor, which is not of finite type.

theorem not_locallyOfFiniteType_source : ¬ LocallyOfFiniteType groupoid.source.left

AlgebraicGeometry.RationalFunctionPairGroupoid.not_locallyOfFiniteType_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/DimensionWithoutFiniteType.lean, line 804. The attribute's comment: “t is not locally of finite type”.

The target of the groupoid scheme is not locally of finite type. On rings it is the inclusion of 𝐐(x) into 𝐐(x) ⊗_𝐐 𝐐(x) as the left factor, which is not of finite type.

theorem not_locallyOfFiniteType_target : ¬ LocallyOfFiniteType groupoid.target.left

AlgebraicGeometry.RationalFunctionPairGroupoid.exists_dim_arrows_eq_one_dim_stabilizer_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/DimensionWithoutFiniteType.lean, line 833. The attribute's comment: “the example in full: U = Spec Q(x) with Q(x) a field, R = Spec (Q(x)[y][1/P(xy)]), s and t are not locally of finite type, dim R = 1 and dim G = 0”.

The example of Tag 04MR, in full. There is a groupoid scheme whose object scheme is the spectrum of a field — here 𝐐(x) — whose arrow scheme is Spec (𝐐(x)[y][1/P(xy)]), whose source and target morphisms are not locally of finite type, and for which the dimension of the arrow scheme is one while the dimension of the stabilizer group scheme is zero.

theorem exists_dim_arrows_eq_one_dim_stabilizer_eq_zero :
    ∃ (k : Type) (_ : Field k) (G : GroupoidScheme (Spec (CommRingCat.of ℚ))),
      G.objects.left = Spec (CommRingCat.of k) ∧
        Nonempty (G.arrows.left ≅ Spec (CommRingCat.of sourceArrowRing)) ∧
        ¬ LocallyOfFiniteType G.source.left ∧
        ¬ LocallyOfFiniteType G.target.left ∧
        topologicalKrullDim G.arrows.left = 1 ∧
        topologicalKrullDim (stabilizer G).left = 0

AlgebraicGeometry.RationalFunctionPairGroupoid.not_forall_dim_arrows_eq_dim_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/DimensionWithoutFiniteType.lean, line 849. The attribute's comment: “Tag 04MQ is wrong without the condition that s and t are locally of finite type”.

The warning of Tag 04MR. Tag 04MQ is wrong without the condition that s and t are locally of finite type: for a groupoid scheme whose object scheme is the spectrum of a field, the dimension of the arrow scheme need not be the dimension of the stabilizer group scheme.

theorem not_forall_dim_arrows_eq_dim_stabilizer :
    ¬ ∀ (S : Scheme.{0}) (G : GroupoidScheme S) (k : Type) (_ : Field k),
        G.objects.left = Spec (CommRingCat.of k) →
          topologicalKrullDim G.arrows.left = topologicalKrullDim (stabilizer G).left

Tag 04RA, a lemma

Tag 04RA in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.smooth_source_left_of_charZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Smooth.lean, line 195. The attribute's comment: “the source morphism”. References: SGA 3 VIB (1.6), “special case”; SGA 3 XVII (5.5), “partial”.

[Stacks Project, Tag 04RA]: the source morphism of a groupoid scheme on a field of characteristic zero is smooth. If the scheme of objects of a groupoid scheme is the spectrum of a field of characteristic zero and the source morphism is locally of finite type, then the source morphism is smooth.

The sheaf of differentials Ω_{R/U} is free by Stacks.Groupoids.GroupoidScheme.exists_free_iso_relativeDifferentials_source_left, and a scheme locally of finite type over a field of characteristic zero whose differentials are locally free is smooth by [Stacks Project, Tag 04QN].

theorem smooth_source_left_of_charZero [CharZero k] (e : G.objects.left ≅ Spec (.of k))
    [LocallyOfFiniteType G.source.left] : Smooth G.source.left

Stacks.Groupoids.GroupoidScheme.smooth_target_left_of_charZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Smooth.lean, line 206. The attribute's comment: “the target morphism”. References: SGA 3 XVII (5.5), “partial”.

[Stacks Project, Tag 04RA]: the target morphism of a groupoid scheme on a field of characteristic zero is smooth. This is the previous statement transported along the inverse, which is an automorphism of the scheme of arrows carrying the source morphism to the target morphism.

theorem smooth_target_left_of_charZero [CharZero k] (e : G.objects.left ≅ Spec (.of k))
    [LocallyOfFiniteType G.source.left] : Smooth G.target.left

Tag 04RB, a lemma

Tag 04RB in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.smooth_source_left_of_isReduced_of_perfectField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Smooth.lean, line 222. The attribute's comment: “the source morphism”.

[Stacks Project, Tag 04RB]: the source morphism of a groupoid scheme with reduced scheme of arrows on a perfect field is smooth. If the scheme of objects of a groupoid scheme is the spectrum of a perfect field, the source morphism is locally of finite type and the scheme of arrows is reduced, then the source morphism is smooth.

The sheaf of differentials Ω_{R/U} is free by Stacks.Groupoids.GroupoidScheme.exists_free_iso_relativeDifferentials_source_left, and a reduced scheme locally of finite type over a perfect field whose differentials are locally free is smooth by [Stacks Project, Tag 04QP].

theorem smooth_source_left_of_isReduced_of_perfectField [PerfectField k]
    (e : G.objects.left ≅ Spec (.of k)) [IsReduced G.arrows.left]
    [LocallyOfFiniteType G.source.left] : Smooth G.source.left

Stacks.Groupoids.GroupoidScheme.smooth_target_left_of_isReduced_of_perfectField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Smooth.lean, line 234. The attribute's comment: “the target morphism”.

[Stacks Project, Tag 04RB]: the target morphism of a groupoid scheme with reduced scheme of arrows on a perfect field is smooth. This is the previous statement transported along the inverse, which is an automorphism of the scheme of arrows carrying the source morphism to the target morphism.

theorem smooth_target_left_of_isReduced_of_perfectField [PerfectField k]
    (e : G.objects.left ≅ Spec (.of k)) [IsReduced G.arrows.left]
    [LocallyOfFiniteType G.source.left] : Smooth G.target.left

Sources

LeanAlgebraicGeometry.GroupoidScheme.isOpenMap_comp_of_objects_isFieldSpectrum · AlgebraicGeometry.isSeparated_arrows_of_objects_isSpec_field · Stacks.Groupoids.GroupoidScheme.exists_fieldExtension_sourceFiber_iso_mapping_points · AlgebraicGeometry.surjective_restrictionDiagramMorphisms · AlgebraicGeometry.flat_restrictionDiagramMorphisms · AlgebraicGeometry.universallyOpen_restrictionDiagramMorphisms · AlgebraicGeometry.isAffineHom_restrictionArrowsToArrows · AlgebraicGeometry.GroupoidScheme.exists_isIso_source_target_over_isAlgClosed

Section40.11 Morphisms of groupoids on fields #

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

Tag 04Q5, a situation

Tag 04Q5 in the Stacks Project.

AlgebraicGeometry.GroupoidMorphismOverFieldSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/Situation.lean, line 56.

The standing data of Situation 04Q5: two groupoid schemes over a base scheme sharing a scheme of objects which is the spectrum of a field, and a morphism between them whose component on objects is the identity.

structure GroupoidMorphismOverFieldSituation

Tag 04Q6, a lemma

Tag 04Q6 in the Stacks Project.

AlgebraicGeometry.isClosed_range_mapArrows_of_isOpen, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/OpenImageOverField.lean, line 228.

Stacks Project, Tag 04Q6. If a morphism of groupoid schemes whose common object scheme is the spectrum of a field has open image on arrows, then that image is closed.

public lemma isClosed_range_mapArrows_of_isOpen
    {S : Scheme.{u}} {k : Type u} [Field k]
    {G₁ G₂ : GroupoidScheme S} (F : GroupoidScheme.Hom G₁ G₂)
    (hobjects : G₁.objects = G₂.objects)
    (hfield : G₁.objects.left = Spec (.of k))
    (hmapObjects : F.mapObjects = eqToHom hobjects)
    (hopen : IsOpen (Set.range F.mapArrows.left.base)) :
    IsClosed (Set.range F.mapArrows.left.base)

Tag 04Q7, a lemma

Tag 04Q7 in the Stacks Project.

AlgebraicGeometry.comp_mapsTo_closure_range_mapArrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/ImageClosure.lean, line 66.

Stacks Project, Tag 04Q7. For a morphism of groupoid schemes over a field which is the identity on the common scheme of objects, the closure of the image on arrows is stable under composition.

theorem comp_mapsTo_closure_range_mapArrows {S : Scheme.{u}} {k : Type u} [Field k]
    {G₁ G₂ : GroupoidScheme S} (F : GroupoidScheme.Hom G₁ G₂)
    (hobjects : G₁.objects = G₂.objects) (hfield : G₁.objects.left = Spec (.of k))
    (hmapObjects : F.mapObjects = eqToHom hobjects) :
    Set.MapsTo G₂.comp.left.base
      ((pullback.fst G₂.source G₂.target).left.base ⁻¹'
          closure (Set.range F.mapArrows.left.base) ∩
        (pullback.snd G₂.source G₂.target).left.base ⁻¹'
          closure (Set.range F.mapArrows.left.base))
      (closure (Set.range F.mapArrows.left.base))

Tag 04Q8, a lemma

Tag 04Q8 in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.reducedClosureImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/ReducedClosureGroupoid.lean, line 476. The attribute's comment: “construction”. References: SGA 3 VIA (0.2), “special case”.

Stacks Project, Tag 04Q8. The reduced closure of the image on arrows of a morphism of groupoid schemes over a perfect field which is the identity on objects carries a groupoid structure for which the closed immersion into the target is a morphism of groupoid schemes.

noncomputable def reducedClosureImage {k : Type u} [Field k] [PerfectField k]
    (F : GroupoidScheme.Hom G₁ G₂) (hobjects : G₁.objects = G₂.objects)
    (hfield : G₁.objects.left = Spec (.of k))
    (hmapObjects : F.mapObjects = eqToHom hobjects) : ReducedClosureImage F

AlgebraicGeometry.GroupoidScheme.reducedClosureGroupoid_objects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/ReducedClosureGroupoid.lean, line 500. The attribute's comment: “object scheme”.

Stacks Project, Tag 04Q8. The reduced-closure groupoid has the same scheme of objects as the target groupoid.

theorem reducedClosureGroupoid_objects {k : Type u} [Field k] [PerfectField k]
    (F : GroupoidScheme.Hom G₁ G₂) (hobjects : G₁.objects = G₂.objects)
    (hfield : G₁.objects.left = Spec (.of k))
    (hmapObjects : F.mapObjects = eqToHom hobjects) :
    (reducedClosureGroupoid F hobjects hfield hmapObjects).objects = G₂.objects

AlgebraicGeometry.GroupoidScheme.reducedClosureGroupoid_arrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/ReducedClosureGroupoid.lean, line 510. The attribute's comment: “arrow scheme”.

Stacks Project, Tag 04Q8. The scheme of arrows of the reduced-closure groupoid is the reduced closure of the image on arrows.

theorem reducedClosureGroupoid_arrows {k : Type u} [Field k] [PerfectField k]
    (F : GroupoidScheme.Hom G₁ G₂) (hobjects : G₁.objects = G₂.objects)
    (hfield : G₁.objects.left = Spec (.of k))
    (hmapObjects : F.mapObjects = eqToHom hobjects) :
    (reducedClosureGroupoid F hobjects hfield hmapObjects).arrows = reducedClosureArrows F

AlgebraicGeometry.GroupoidScheme.reducedClosureInclusion_mapObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/ReducedClosureGroupoid.lean, line 520. The attribute's comment: “inclusion on objects”.

Stacks Project, Tag 04Q8. The canonical morphism from the reduced-closure groupoid is the identity on objects.

theorem reducedClosureInclusion_mapObjects {k : Type u} [Field k] [PerfectField k]
    (F : GroupoidScheme.Hom G₁ G₂) (hobjects : G₁.objects = G₂.objects)
    (hfield : G₁.objects.left = Spec (.of k))
    (hmapObjects : F.mapObjects = eqToHom hobjects) :
    (reducedClosureInclusion F hobjects hfield hmapObjects).mapObjects =
      eqToHom (reducedClosureGroupoid_objects F hobjects hfield hmapObjects)

AlgebraicGeometry.GroupoidScheme.reducedClosureInclusion_mapArrows_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/ReducedClosureGroupoid.lean, line 542. The attribute's comment: “inclusion on arrows”.

Stacks Project, Tag 04Q8. On arrows the canonical morphism from the reduced-closure groupoid is the closed immersion of the reduced closure of the image.

theorem reducedClosureInclusion_mapArrows_left {k : Type u} [Field k] [PerfectField k]
    (F : GroupoidScheme.Hom G₁ G₂) (hobjects : G₁.objects = G₂.objects)
    (hfield : G₁.objects.left = Spec (.of k))
    (hmapObjects : F.mapObjects = eqToHom hobjects) :
    (reducedClosureInclusion F hobjects hfield hmapObjects).mapArrows.left =
      eqToHom (congrArg Over.left
        (reducedClosureGroupoid_arrows F hobjects hfield hmapObjects)) ≫
        (reducedClosureArrowImage F).subschemeι

Tag 04Q9, a lemma

Tag 04Q9 in the Stacks Project.

AlgebraicGeometry.isClosed_range_mapArrows_of_isLocallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/LocallyClosedImage.lean, line 391.

Stacks Project, Tag 04Q9. The image on arrows of a morphism of groupoid schemes over a field which is the identity on their common scheme of objects is closed as soon as it is locally closed.

theorem isClosed_range_mapArrows_of_isLocallyClosed {k : Type u} [Field k]
    (F : GroupoidScheme.Hom G₁ G₂) (hobjects : G₁.objects = G₂.objects)
    (hfield : G₁.objects.left = Spec (.of k))
    (hmapObjects : F.mapObjects = eqToHom hobjects)
    (h : IsLocallyClosed (Set.range F.mapArrows.left.base)) :
    IsClosed (Set.range F.mapArrows.left.base)

Tag 04QA, a lemma

Tag 04QA in the Stacks Project.

AlgebraicGeometry.exists_groupoidScheme_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/ArrowImageOverField.lean, line 627.

Stacks Project, Tag 04QA. The scheme-theoretic image of a quasi-compact arrow map of groupoid schemes over a field has the restricted groupoid structure.

public theorem exists_groupoidScheme_image
    {S : Scheme.{u}} {k : Type u} [Field k]
    {G₁ G₂ : GroupoidScheme S} (F : GroupoidScheme.Hom G₁ G₂)
    (hobjects : G₁.objects = G₂.objects)
    (hfield : G₁.objects.left = Spec (.of k))
    (hmapObjects : F.mapObjects = eqToHom hobjects)
    [QuasiCompact F.mapArrows.left] :
    ∃ (H : GroupoidScheme S) (j : GroupoidScheme.Hom H G₂)
      (hHobjects : H.objects = G₂.objects)
      (hHarrows : H.arrows = Over.mk
        (F.mapArrows.left.imageι ≫ G₂.arrows.hom)),
        (j.mapObjects = eqToHom hHobjects) ∧
        (j.mapArrows.left =
          eqToHom (congrArg Over.left hHarrows) ≫ F.mapArrows.left.imageι)

Tag 04QB, a lemma

Tag 04QB in the Stacks Project.

AlgebraicGeometry.comp_mapsTo_closure_range_groupoidPreRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/ClosureComposition.lean, line 71.

Stacks Project, Tag 04QB. Let (U, R, s, t, c) be a groupoid scheme over S with U the spectrum of a field, and let Z be the closure of the image of j = (t, s) in U ×_S U. Then pr₀₂ maps Z ×_{pr₁, U, pr₀} Z into Z.

theorem comp_mapsTo_closure_range_groupoidPreRelation :
    Set.MapsTo
      (prod.lift
        (pullback.fst (prod.snd : G.objects ⨯ G.objects ⟶ G.objects) prod.fst ≫ prod.fst)
        (pullback.snd (prod.snd : G.objects ⨯ G.objects ⟶ G.objects) prod.fst
          ≫ prod.snd)).left.base
      ((pullback.fst (prod.snd : G.objects ⨯ G.objects ⟶ G.objects) prod.fst).left.base ⁻¹'
          closure (Set.range (groupoidPreRelation G).left.base) ∩
        (pullback.snd (prod.snd : G.objects ⨯ G.objects ⟶ G.objects) prod.fst).left.base ⁻¹'
          closure (Set.range (groupoidPreRelation G).left.base))
      (closure (Set.range (groupoidPreRelation G).left.base))

Tag 04QC, a lemma

Tag 04QC in the Stacks Project.

AlgebraicGeometry.reducedClosureGroupoidPreRelation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/ClosureComposition.lean, line 89.

Stacks Project, Tag 04QC. For a groupoid scheme (U, R, s, t, c) over S with U the spectrum of a perfect field, the reduced closed subscheme Z of U ×_S U supported on the closure of the image of j = (t, s) is the scheme of arrows of a groupoid scheme on U whose structure maps are the restrictions of pr₁, pr₀ and pr₀₂.

noncomputable def reducedClosureGroupoidPreRelation [PerfectField k] :
    GroupoidScheme.ReducedClosureImage (groupoidPreRelationHom G)

Tag 04QD, a lemma

Tag 04QD in the Stacks Project.

AlgebraicGeometry.exists_groupoidScheme_image_groupoidPreRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/Morphisms/ClosureComposition.lean, line 117.

Stacks Project, Tag 04QD. For a groupoid scheme (U, R, s, t, c) over S with U the spectrum of a field and R quasi-compact, the scheme-theoretic image of j = (t, s) in U ×_S U is the scheme of arrows of a groupoid scheme on U whose structure maps are the restrictions of pr₁, pr₀ and pr₀₂.

theorem exists_groupoidScheme_image_groupoidPreRelation [CompactSpace G.arrows.left] :
    ∃ (H : GroupoidScheme S) (ι : GroupoidScheme.Hom H (prodPairGroupoid G.objects))
      (hHobjects : H.objects = G.objects)
      (hHarrows : H.arrows = Over.mk ((groupoidPreRelation G).left.imageι ≫
        (G.objects ⨯ G.objects).hom)),
        (ι.mapObjects = eqToHom hHobjects) ∧
        (ι.mapArrows.left =
          eqToHom (congrArg Over.left hHarrows) ≫ (groupoidPreRelation G).left.imageι)

Sources

LeanAlgebraicGeometry.GroupoidMorphismOverFieldSituation · AlgebraicGeometry.isClosed_range_mapArrows_of_isOpen · AlgebraicGeometry.comp_mapsTo_closure_range_mapArrows · AlgebraicGeometry.GroupoidScheme.reducedClosureImage · AlgebraicGeometry.GroupoidScheme.reducedClosureGroupoid_objects · AlgebraicGeometry.GroupoidScheme.reducedClosureGroupoid_arrows · AlgebraicGeometry.GroupoidScheme.reducedClosureInclusion_mapObjects · AlgebraicGeometry.GroupoidScheme.reducedClosureInclusion_mapArrows_left

Section40.12 Slicing groupoids #

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

Tag 04MY, a situation

Tag 04MY in the Stacks Project.

AlgebraicGeometry.SliceSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/SliceSituation.lean, line 61. The attribute's comment: “the slice situation”.

The standing data for the slice situation: a groupoid scheme, a morphism to its object scheme, and points lying over one another.

public structure SliceSituation

AlgebraicGeometry.SliceSituation.sliceFiberComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/SliceSituation.lean, line 259. The attribute's comment: “the fibre comparison”.

Stacks Project, Tag 04MY. The source fibre in the restricted groupoid is canonically the base change of h⁻¹(u) along Spec(κ(u')) ⟶ Spec(κ(u)).

noncomputable def sliceFiberComparison (D : SliceSituation) :
    SliceFiberComparison D

AlgebraicGeometry.SliceSituation.sliceIdentityPoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/SliceSituation.lean, line 628. The attribute's comment: “the compatible identity points”.

Stacks Project, Tag 04MY. The identity arrows determine compatible points of the stabilizer and source fibres before and after restriction; the canonical maps of fibres carry each restricted identity point to the original one.

noncomputable def sliceIdentityPoints (D : SliceSituation) :
    SliceIdentityPoints D

AlgebraicGeometry.stabilizerArrow_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/SliceSituation.lean, line 637. The attribute's comment: “the stabilizer is locally closed”.

Stacks Project, Tag 04MY. The stabilizer of a groupoid scheme is a locally closed subscheme of its arrow scheme.

public theorem stabilizerArrow_isImmersion {S : Scheme.{u}} (G : GroupoidScheme S) :
    IsImmersion (stabilizerArrow G)

Tag 0461, a lemma

Tag 0461 in the Stacks Project.

AlgebraicGeometry.exists_affine_slice_dim_sub_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/SliceDimensionDrop.lean, line 543.

Stacks Project, Tag 0461. Let (U, R, s, t, c) be a groupoid scheme with s and t Cohen--Macaulay and locally of finite presentation, let u be a finite type point of U, and suppose the source fibre F_u has larger dimension at the identity arrow than the stabilizer fibre G_u. Then there are an affine scheme U' and a morphism g : U' ⟶ U which is an immersion through u and locally of finite presentation, such that h : U' ×_{g,U,t} R ⟶ U is Cohen--Macaulay at the identity arrow and the restricted source fibre has dimension one less at the restricted identity arrow.

public theorem exists_affine_slice_dim_sub_one {S : Scheme.{u}}
    (G : GroupoidScheme S) (u : G.objects.left)
    (hs : ∃ h : ∀ y : G.objects.left, IsLocallyNoetherian (G.source.left.fiber y),
      Scheme.Hom.IsCohenMacaulay G.source.left h)
    (_ht : ∃ h : ∀ y : G.objects.left, IsLocallyNoetherian (G.target.left.fiber y),
      Scheme.Hom.IsCohenMacaulay G.target.left h)
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left]
    (hu : IsFiniteTypePoint u)
    (hdim : topologicalKrullDim ((stabilizer G).hom.fiber u) <
      topologicalKrullDimAt (G.source.left.fiber u) (sourceFiberIdentity G u))
    :
    ∃ (U' : Over S) (g : U' ⟶ G.objects) (u' : U'.left) (hu' : g.left u' = u),
      let E : SliceSituation := ⟨S, G, U', g, u, u', hu'⟩
      IsAffine U'.left ∧ IsImmersion g.left ∧ LocallyOfFinitePresentation g.left ∧
        (∃ (x : E.arrowSource.left)
          (_ : (pullback.fst E.g E.groupoid.target).left x = u')
          (_ : (pullback.snd E.g E.groupoid.target).left x = E.groupoid.identity.left E.u)
          (hnoeth : ∀ y : E.groupoid.objects.left,
            IsLocallyNoetherian (E.sourceMap.left.fiber y)),
          Scheme.Hom.IsCohenMacaulayAt E.sourceMap.left hnoeth x) ∧
        topologicalKrullDimAt E.restrictedSourceFiber
            E.sliceIdentityPoints.restrictedSourceIdentity + 1 =
          topologicalKrullDimAt (G.source.left.fiber u) (sourceFiberIdentity G u)

Module.IsMaximalCohenMacaulay.exists_mem_notMem_minimalPrimes_of_ringKrullDim_quotient_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/SliceDimensionDrop.lean, line 188. The attribute's comment: “step 2 of the proof: the minimal-prime avoidance, from equidimensionality of a Cohen--Macaulay local ring (Tag 00NA) and prime avoidance (Tag 00DS). The ideal is not assumed maximal and the source ring is not assumed Noetherian or local”. References: EGA 0 (16.5.5), “special case”.

Minimal-prime avoidance in a Cohen–Macaulay local ring. Let R be a Noetherian local Cohen–Macaulay ring, u : A →+* R a ring map and I an ideal of A such that the ideal u(I)R already cuts the dimension, dim(R/u(I)R) < dim(R). Then there is f ∈ I whose image u f lies in no minimal prime of R.

theorem Module.IsMaximalCohenMacaulay.exists_mem_notMem_minimalPrimes_of_ringKrullDim_quotient_lt
    {A R : Type u} [CommRing A] [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (hR : Module.IsMaximalCohenMacaulay R R) (u : A →+* R) (I : Ideal A)
    (hlt : ringKrullDim (R ⧸ I.map u) < ringKrullDim R) :
    ∃ f ∈ I, ∀ p ∈ minimalPrimes R, u f ∉ p

Module.IsMaximalCohenMacaulay.exists_mem_isSMulRegular_map_quotient_isMaximalCohenMacaulay, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/SliceDimensionDrop.lean, line 238. The attribute's comment: “the commutative-algebra core, conclusions (a), (b) and (c), over an abstract Noetherian local Cohen--Macaulay ring and a ring map into it; no groupoid, scheme or localisation data appears, and the dimension drop is stated additively”. References: EGA 0 (16.5.5), “special case”.

Slicing a Cohen–Macaulay local ring, the commutative-algebra core of Stacks 0461. Let (R, 𝔪_R) be a Noetherian local Cohen–Macaulay ring, let u : A →+* R be a ring map and let I be an ideal of A with u(I)R ⊆ 𝔪_R and dim(R/u(I)R) < dim(R). Then there is f ∈ I such that dim(R/u(f)R) < dim(R), the element u f is a nonzerodivisor on R, and R/u(f)R is a Cohen–Macaulay local ring of dimension dim(R) - 1.

theorem Module.IsMaximalCohenMacaulay.exists_mem_isSMulRegular_map_quotient_isMaximalCohenMacaulay
    {A R : Type u} [CommRing A] [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (hR : Module.IsMaximalCohenMacaulay R R) (u : A →+* R) (I : Ideal A)
    (hu : I.map u ≤ IsLocalRing.maximalIdeal R)
    (hlt : ringKrullDim (R ⧸ I.map u) < ringKrullDim R) :
    ∃ f ∈ I, ringKrullDim (R ⧸ Ideal.span {u f}) < ringKrullDim R ∧ IsSMulRegular R (u f) ∧
      ∃ _ : IsLocalRing (R ⧸ Ideal.span {u f}),
        Module.IsMaximalCohenMacaulay (R ⧸ Ideal.span {u f}) (R ⧸ Ideal.span {u f}) ∧
          ringKrullDim (R ⧸ Ideal.span {u f}) + 1 = ringKrullDim R

IsCohenMacaulayLocalRing.exists_mem_maximalIdeal_isSMulRegular_map_of_ringKrullDim_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CohenMacaulay/SliceDimensionDrop.lean, line 262. The attribute's comment: “the commutative-algebra core along a local homomorphism, at the maximal ideal of the source, in the Tag 00N8 spelling of Cohen--Macaulayness; this is the form the geometric argument consumes”.

Slicing along a local homomorphism. Let φ : A →+* C be a local homomorphism of local rings with C Noetherian and Cohen–Macaulay, and suppose the ideal φ(𝔪_A)C already cuts the dimension, dim(C/φ(𝔪_A)C) < dim(C). Then some a ∈ 𝔪_A has φ a a nonzerodivisor on C with dim(C/φ(a)C) + 1 = dim(C).

theorem IsCohenMacaulayLocalRing.exists_mem_maximalIdeal_isSMulRegular_map_of_ringKrullDim_lt
    (A C : Type u) [CommRing A] [IsLocalRing A] [CommRing C] [IsLocalRing C]
    [IsNoetherianRing C] (hC : IsCohenMacaulayLocalRing C) (φ : A →+* C) (hφ : IsLocalHom φ)
    (hlt : ringKrullDim (C ⧸ Ideal.map φ (IsLocalRing.maximalIdeal A)) < ringKrullDim C) :
    ∃ a ∈ IsLocalRing.maximalIdeal A, IsSMulRegular C (φ a) ∧
      ringKrullDim (C ⧸ Ideal.span {φ a}) + 1 = ringKrullDim C

Tag 04MZ, a lemma

Tag 04MZ in the Stacks Project.

AlgebraicGeometry.exists_affine_slice_dim_eq_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/MaximalSlice.lean, line 1276.

Stacks Project, Tag 04MZ. Let (U, R, s, t, c, e, i) be a groupoid scheme whose source and target maps are Cohen--Macaulay and locally of finite presentation, and let u be a finite type point of U. Then there are an affine scheme U' and a morphism g : U' ⟶ U which is an immersion through u and locally of finite presentation, such that h : U' ×_{g,U,t} R ⟶ U and the source and target maps of the restricted groupoid are again Cohen--Macaulay and locally of finite presentation, and the restricted source fibre F'_u has at the identity arrow exactly the dimension of the restricted stabilizer fibre G'_u.

public theorem exists_affine_slice_dim_eq_stabilizer {S : Scheme.{u}}
    (G : GroupoidScheme S) (u : G.objects.left)
    (hu : AlgebraicGeometry.IsFiniteTypePoint u)
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left]
    (hs : ∃ hf : ∀ y : G.objects.left,
      IsLocallyNoetherian (G.source.left.fiber y),
      Scheme.Hom.IsCohenMacaulay G.source.left hf)
    (_ht : ∃ hf : ∀ y : G.objects.left,
      IsLocallyNoetherian (G.target.left.fiber y),
      Scheme.Hom.IsCohenMacaulay G.target.left hf) :
    ∃ (U' : Over S) (g : U' ⟶ G.objects) (u' : U'.left)
      (hgu : g.left u' = u),
      let D : SliceSituation :=
        { S := S, groupoid := G, U' := U', g := g,
          u := u, u' := u', mapsTo := hgu }
      IsAffine U'.left ∧
      IsImmersion g.left ∧
      LocallyOfFinitePresentation g.left ∧
      LocallyOfFinitePresentation D.sourceMap.left ∧
      (∃ hf : ∀ y : G.objects.left,
        IsLocallyNoetherian (D.sourceMap.left.fiber y),
        Scheme.Hom.IsCohenMacaulay D.sourceMap.left hf) ∧
      LocallyOfFinitePresentation D.restrictedGroupoid.source.left ∧
      (∃ hf : ∀ y : D.restrictedGroupoid.objects.left,
        IsLocallyNoetherian (D.restrictedGroupoid.source.left.fiber y),
        Scheme.Hom.IsCohenMacaulay D.restrictedGroupoid.source.left hf) ∧
      LocallyOfFinitePresentation D.restrictedGroupoid.target.left ∧
      (∃ hf : ∀ y : D.restrictedGroupoid.objects.left,
        IsLocallyNoetherian (D.restrictedGroupoid.target.left.fiber y),
        Scheme.Hom.IsCohenMacaulay D.restrictedGroupoid.target.left hf) ∧
      topologicalKrullDimAt D.restrictedSourceFiber
          D.sliceIdentityPoints.restrictedSourceIdentity =
        topologicalKrullDim D.restrictedStabilizerFiber

Tag 04N0, a lemma

Tag 04N0 in the Stacks Project.

AlgebraicGeometry.exists_affine_slice_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/MaxSliceQuasiFinite.lean, line 121. The attribute's comment: “conclusions (1)-(5) with the fibre products of schemes: g an affine immersion locally of finite presentation, h, s', t' flat, locally finitely presented, quasi-finite”.

Stacks Project, Tag 04N0. A finite type point of a groupoid scheme whose source and target maps are Cohen--Macaulay and locally of finite presentation and whose stabilizer group scheme is locally quasi-finite has an affine slice g : U' ⟶ U, an immersion locally of finite presentation, for which h : U' ×_{g, U, t} R ⟶ U and the source and target maps of the restricted groupoid are flat, locally of finite presentation and locally quasi-finite.

public theorem exists_affine_slice_locallyQuasiFinite {S : Scheme.{u}}
    (G : GroupoidScheme S) (u : G.objects.left)
    (hu : AlgebraicGeometry.IsFiniteTypePoint u)
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left]
    (hs : ∃ hf : ∀ y : G.objects.left, IsLocallyNoetherian (G.source.left.fiber y),
      Scheme.Hom.IsCohenMacaulay G.source.left hf)
    (ht : ∃ hf : ∀ y : G.objects.left, IsLocallyNoetherian (G.target.left.fiber y),
      Scheme.Hom.IsCohenMacaulay G.target.left hf)
    [LocallyQuasiFinite (stabilizer G).hom] :
    ∃ (U' : Scheme.{u}) (g : U' ⟶ G.objects.left) (u' : U'),
      g u' = u ∧ IsAffine U' ∧ IsImmersion g ∧ LocallyOfFinitePresentation g ∧
      Flat (pullback.snd g G.target.left ≫ G.source.left) ∧
      LocallyOfFinitePresentation (pullback.snd g G.target.left ≫ G.source.left) ∧
      LocallyQuasiFinite (pullback.snd g G.target.left ≫ G.source.left) ∧
      Flat (GroupoidScheme.restrict G
        (Over.homMk g : Over.mk (g ≫ G.objects.hom) ⟶ G.objects)).groupoid.source.left ∧
      LocallyOfFinitePresentation (GroupoidScheme.restrict G
        (Over.homMk g : Over.mk (g ≫ G.objects.hom) ⟶ G.objects)).groupoid.source.left ∧
      LocallyQuasiFinite (GroupoidScheme.restrict G
        (Over.homMk g : Over.mk (g ≫ G.objects.hom) ⟶ G.objects)).groupoid.source.left ∧
      Flat (GroupoidScheme.restrict G
        (Over.homMk g : Over.mk (g ≫ G.objects.hom) ⟶ G.objects)).groupoid.target.left ∧
      LocallyOfFinitePresentation (GroupoidScheme.restrict G
        (Over.homMk g : Over.mk (g ≫ G.objects.hom) ⟶ G.objects)).groupoid.target.left ∧
      LocallyQuasiFinite (GroupoidScheme.restrict G
        (Over.homMk g : Over.mk (g ≫ G.objects.hom) ⟶ G.objects)).groupoid.target.left

AlgebraicGeometry.exists_affine_slice_locallyQuasiFinite_of_isFiniteTypePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/QuasiFiniteSlice.lean, line 308. The attribute's comment: “conclusions (1)-(5): an affine immersion locally of finite presentation whose h, s' and t' are flat, locally of finite presentation and locally quasi-finite”.

Stacks Project, Tag 04N0. Let (U, R, s, t, c, e, i) be a groupoid scheme with s and t Cohen-Macaulay and locally of finite presentation, let u be a finite type point of U, and assume the stabilizer group scheme is locally quasi-finite. Then there are an affine scheme U' and a morphism g : U' ⟶ U such that g is an immersion, u lies in U', g is locally of finite presentation, the morphism h : U' ×_{g, U, t} R ⟶ U is flat, locally of finite presentation and locally quasi-finite, and the structure maps s', t' : R' ⟶ U' of the restricted groupoid are flat, locally of finite presentation and locally quasi-finite.

public theorem exists_affine_slice_locallyQuasiFinite_of_isFiniteTypePoint {S : Scheme.{u}}
    (G : GroupoidScheme S) (u : G.objects.left)
    (hu : AlgebraicGeometry.IsFiniteTypePoint u)
    [LocallyOfFinitePresentation G.source.left]
    [LocallyOfFinitePresentation G.target.left]
    (hs : ∃ hf : ∀ y : G.objects.left, IsLocallyNoetherian (G.source.left.fiber y),
      Scheme.Hom.IsCohenMacaulay G.source.left hf)
    (ht : ∃ hf : ∀ y : G.objects.left, IsLocallyNoetherian (G.target.left.fiber y),
      Scheme.Hom.IsCohenMacaulay G.target.left hf)
    [LocallyQuasiFinite (stabilizer G).hom] :
    ∃ (U' : Over S) (g : U' ⟶ G.objects) (u' : U'.left) (hgu : g.left u' = u),
      let D : SliceSituation :=
        { S := S, groupoid := G, U' := U', g := g, u := u, u' := u', mapsTo := hgu }
      IsAffine U'.left ∧ IsImmersion g.left ∧ LocallyOfFinitePresentation g.left ∧
        (Flat D.sourceMap.left ∧ LocallyOfFinitePresentation D.sourceMap.left ∧
          LocallyQuasiFinite D.sourceMap.left) ∧
        (Flat D.restrictedGroupoid.source.left ∧
          LocallyOfFinitePresentation D.restrictedGroupoid.source.left ∧
          LocallyQuasiFinite D.restrictedGroupoid.source.left) ∧
        (Flat D.restrictedGroupoid.target.left ∧
          LocallyOfFinitePresentation D.restrictedGroupoid.target.left ∧
          LocallyQuasiFinite D.restrictedGroupoid.target.left)

Sources

LeanAlgebraicGeometry.SliceSituation · AlgebraicGeometry.SliceSituation.sliceFiberComparison · AlgebraicGeometry.SliceSituation.sliceIdentityPoints · AlgebraicGeometry.stabilizerArrow_isImmersion · AlgebraicGeometry.exists_affine_slice_dim_sub_one · Module.IsMaximalCohenMacaulay.exists_mem_notMem_minimalPrimes_of_ringKrullDim_quotient_lt · Module.IsMaximalCohenMacaulay.exists_mem_isSMulRegular_map_quotient_isMaximalCohenMacaulay · IsCohenMacaulayLocalRing.exists_mem_maximalIdeal_isSMulRegular_map_of_ringKrullDim_lt

Section40.13 Étale localization of groupoids #

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

Tag 03FL, a lemma

Tag 03FL in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.exists_finite_openClosed_subgroupoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/EtaleLocalizationFiniteSubgroupoid/FiniteSubgroupoid.lean, line 308.

Around a point at which the object map is quasi-finite and whose source fibre is finite, a flat finitely presented groupoid has, after an elementary étale base change, a finite open-and-closed subgroupoid containing precisely the orbit of the point in the distinguished fibre.

public theorem exists_finite_openClosed_subgroupoid
    {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S) (p : S)
    (u : G.objects.left) (hu : G.objects.hom u = p)
    [LocallyOfFiniteType G.objects.hom]
    (hqu : AlgebraicGeometry.quasiFiniteAt G.objects.hom u)
    [IsSeparated G.objects.hom] [IsSeparated G.arrows.hom]
    [Flat G.source.left] [LocallyOfFinitePresentation G.source.left]
    [Flat G.target.left] [LocallyOfFinitePresentation G.target.left]
    (hfinite : Set.Finite (G.source.left ⁻¹' {u})) :
    ∃ (N : AlgebraicGeometry.EtaleNeighborhood S p), N.IsElementary ∧
      ∃ (H : Stacks.Groupoids.GroupoidScheme N.scheme) (W W' : Scheme.{u})
        (jU : H.objects.left ⟶ pullback G.objects.hom N.toBase)
        (jW : W ⟶ pullback G.objects.hom N.toBase)
        (jR : H.arrows.left ⟶ pullback G.arrows.hom N.toBase)
        (jW' : W' ⟶ pullback G.arrows.hom N.toBase),
        IsOpenImmersion jU ∧ IsClosedImmersion jU ∧
        IsOpenImmersion jW ∧ IsClosedImmersion jW ∧
        IsIso (coprod.desc jU jW) ∧
        IsOpenImmersion jR ∧ IsClosedImmersion jR ∧
        IsOpenImmersion jW' ∧ IsClosedImmersion jW' ∧
        IsIso (coprod.desc jR jW') ∧
        H.objects.hom = jU ≫ pullback.snd G.objects.hom N.toBase ∧
        H.arrows.hom = jR ≫ pullback.snd G.arrows.hom N.toBase ∧
        (∃ u' : H.objects.left,
          (jU ≫ pullback.fst G.objects.hom N.toBase) u' = u ∧
          jU '' {x : H.objects.left | H.objects.hom x = N.point} =
            (pullback.map G.arrows.hom N.toBase G.objects.hom N.toBase
              G.target.left (𝟙 _) (𝟙 _) (by simp) (by simp)) ''
              ((pullback.map G.arrows.hom N.toBase G.objects.hom N.toBase
                G.source.left (𝟙 _) (𝟙 _) (by simp) (by simp)) ⁻¹' {jU u'}) ∧
          jR '' {r : H.arrows.left | H.arrows.hom r = N.point} =
            (pullback.map G.arrows.hom N.toBase G.objects.hom N.toBase
              G.source.left (𝟙 _) (𝟙 _) (by simp) (by simp)) ⁻¹'
                (jU '' {x : H.objects.left | H.objects.hom x = N.point})) ∧
        IsFinite H.objects.hom ∧ IsFinite H.arrows.hom ∧
        H.source.left ≫ jU ≫ pullback.fst G.objects.hom N.toBase =
          jR ≫ pullback.fst G.arrows.hom N.toBase ≫ G.source.left ∧
        H.target.left ≫ jU ≫ pullback.fst G.objects.hom N.toBase =
          jR ≫ pullback.fst G.arrows.hom N.toBase ≫ G.target.left ∧
        ∃ k : (pullback H.source H.target).left ⟶
            (pullback G.source G.target).left,
          k ≫ (pullback.fst G.source G.target).left =
              (pullback.fst H.source H.target).left ≫ jR ≫
                pullback.fst G.arrows.hom N.toBase ∧
          k ≫ (pullback.snd G.source G.target).left =
              (pullback.snd H.source H.target).left ≫ jR ≫
                pullback.fst G.arrows.hom N.toBase ∧
          H.comp.left ≫ jR ≫ pullback.fst G.arrows.hom N.toBase =
            k ≫ G.comp.left

Tag 03X5, a lemma

Tag 03X5 in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.exists_finite_openClosed_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/EtaleLocalizationFiniteSubgroupoid/FiniteRestriction.lean, line 416.

The finite open-and-closed subgroupoid around a quasi-finite point can be chosen as the full restriction when the relation morphism is universally closed.

public theorem exists_finite_openClosed_restriction
    {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S) (p : S)
    (u : G.objects.left) (hu : G.objects.hom u = p)
    [LocallyOfFiniteType G.objects.hom]
    (hqu : AlgebraicGeometry.quasiFiniteAt G.objects.hom u)
    [IsSeparated G.objects.hom] [IsSeparated G.arrows.hom]
    [Flat G.source.left] [LocallyOfFinitePresentation G.source.left]
    [Flat G.target.left] [LocallyOfFinitePresentation G.target.left]
    (hfinite : Set.Finite (G.source.left ⁻¹' {u}))
    [UniversallyClosed (prod.lift G.target G.source).left] :
    ∃ (N : AlgebraicGeometry.EtaleNeighborhood S p), N.IsElementary ∧
      ∃ (H : Stacks.Groupoids.GroupoidScheme N.scheme) (W W' : Scheme.{u})
        (jU : H.objects.left ⟶ pullback G.objects.hom N.toBase)
        (jW : W ⟶ pullback G.objects.hom N.toBase)
        (jR : H.arrows.left ⟶ pullback G.arrows.hom N.toBase)
        (jW' : W' ⟶ pullback G.arrows.hom N.toBase),
        IsOpenImmersion jU ∧ IsClosedImmersion jU ∧
        IsOpenImmersion jW ∧ IsClosedImmersion jW ∧
        IsIso (coprod.desc jU jW) ∧
        IsOpenImmersion jR ∧ IsClosedImmersion jR ∧
        IsOpenImmersion jW' ∧ IsClosedImmersion jW' ∧
        IsIso (coprod.desc jR jW') ∧
        H.objects.hom = jU ≫ pullback.snd G.objects.hom N.toBase ∧
        H.arrows.hom = jR ≫ pullback.snd G.arrows.hom N.toBase ∧
        (∃ u' : H.objects.left,
          (jU ≫ pullback.fst G.objects.hom N.toBase) u' = u ∧
          jU '' {x : H.objects.left | H.objects.hom x = N.point} =
            (pullback.map G.arrows.hom N.toBase G.objects.hom N.toBase
              G.target.left (𝟙 _) (𝟙 _) (by simp) (by simp)) ''
              ((pullback.map G.arrows.hom N.toBase G.objects.hom N.toBase
                G.source.left (𝟙 _) (𝟙 _) (by simp) (by simp)) ⁻¹' {jU u'}) ∧
          jR '' {r : H.arrows.left | H.arrows.hom r = N.point} =
            (pullback.map G.arrows.hom N.toBase G.objects.hom N.toBase
              G.source.left (𝟙 _) (𝟙 _) (by simp) (by simp)) ⁻¹'
                (jU '' {x : H.objects.left | H.objects.hom x = N.point})) ∧
        IsFinite H.objects.hom ∧ IsFinite H.arrows.hom ∧
        H.source.left ≫ jU ≫ pullback.fst G.objects.hom N.toBase =
          jR ≫ pullback.fst G.arrows.hom N.toBase ≫ G.source.left ∧
        H.target.left ≫ jU ≫ pullback.fst G.objects.hom N.toBase =
          jR ≫ pullback.fst G.arrows.hom N.toBase ≫ G.target.left ∧
        (∃ k : (pullback H.source H.target).left ⟶
            (pullback G.source G.target).left,
          k ≫ (pullback.fst G.source G.target).left =
              (pullback.fst H.source H.target).left ≫ jR ≫
                pullback.fst G.arrows.hom N.toBase ∧
          k ≫ (pullback.snd G.source G.target).left =
              (pullback.snd H.source H.target).left ≫ jR ≫
                pullback.fst G.arrows.hom N.toBase ∧
          H.comp.left ≫ jR ≫ pullback.fst G.arrows.hom N.toBase =
            k ≫ G.comp.left) ∧
        (∀ (T : Scheme.{u})
          (f : T ⟶ pullback G.arrows.hom N.toBase)
          (x y : T ⟶ H.objects.left),
          (f ≫ pullback.map G.arrows.hom N.toBase G.objects.hom N.toBase
              G.source.left (𝟙 _) (𝟙 _) (by simp) (by simp) = x ≫ jU) →
          (f ≫ pullback.map G.arrows.hom N.toBase G.objects.hom N.toBase
              G.target.left (𝟙 _) (𝟙 _) (by simp) (by simp) = y ≫ jU) →
          (∃! g : T ⟶ H.arrows.left,
            g ≫ jR = f ∧ g ≫ H.source.left = x ∧ g ≫ H.target.left = y))

Sources

LeanAlgebraicGeometry.GroupoidScheme.exists_finite_openClosed_subgroupoid · AlgebraicGeometry.GroupoidScheme.exists_finite_openClosed_restriction

Section40.14 Finite groupoids #

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

Tag 0AB9, a lemma

Tag 0AB9 in the Stacks Project.

Stacks.Groupoids.finiteStratification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteStratification.lean, line 51. The attribute's comment: “the Fitting stratification”.

The canonical Fitting stratification associated to source of a groupoid scheme.

noncomputable def finiteStratification {S : Scheme.{u}} (G : GroupoidScheme S) (n : ℕ) :
    G.objects.left.IdealSheafData

Stacks.Groupoids.finiteStratification_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteStratification.lean, line 57. The attribute's comment: “the first closed subscheme”.

The identity arrows force the zeroth Fitting closed subscheme to be all objects.

theorem finiteStratification_zero {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsFinite G.source.left] [IsFinite G.target.left] :
    finiteStratification G 0 = ⊥

Stacks.Groupoids.finiteStratification_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteStratification.lean, line 65. The attribute's comment: “decreasing closed subschemes”.

The Fitting closed subschemes form a decreasing sequence.

theorem finiteStratification_mono {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsFinite G.source.left] [IsFinite G.target.left] (n : ℕ) :
    finiteStratification G n ≤ finiteStratification G (n + 1)

Stacks.Groupoids.finiteStratification_exhaustive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteStratification.lean, line 72. The attribute's comment: “empty intersection”.

No point lies in all Fitting closed subschemes.

theorem finiteStratification_exhaustive {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsFinite G.source.left] [IsFinite G.target.left] (x : G.objects.left) :
    ∃ n, x ∉ (finiteStratification G n).support

Stacks.Groupoids.finiteStratification_invariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteStratificationInvariant.lean, line 195. The attribute's comment: “invariance”.

Every member of the Fitting stratification is invariant under the groupoid.

The second projection of the scheme of composable pairs is simultaneously the base change of source along target and the base change of source along source, by the two cartesian lower squares of the diagram of Stacks Tag 04LF. So both inverse images of a member of the stratification are the Fitting ideal sheaf of the pushforward of the structure sheaf along that single projection.

theorem finiteStratification_invariant {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsFinite G.source.left] [IsFinite G.target.left] (n : ℕ) :
    IsInvariantClosedSubscheme G (finiteStratification G n)

Stacks.Groupoids.finiteStratification_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteStratificationRankSheaf.lean, line 81. The attribute's comment: “rank of each stratum”.

Stacks Project, Tag 0AB9: the rank of each stratum. For a groupoid scheme with finite source and target there is an open subscheme W of the closed subscheme cut out by the (r-1)st Fitting ideal sheaf of s_* 𝒪_R whose image in the object scheme is the difference of the supports of the (r-1)st and rth Fitting ideal sheaves, and the base change of source to W is finite locally free of rank r.

The open subscheme is Stacks.Groupoids.exists_opens_finiteStratification_stratum. Finite local freeness is checked affine-locally by Stacks.Groupoids.module_isFiniteLocallyFreeOfRank_finiteStratification_stratum and assembled into the sheaf-level statement by Stacks.Modules.isFiniteLocallyFreeOfRank_of_module_affineOpens and Stacks.Modules.isFiniteLocallyFreeOfRank_iff_localGenerators.

theorem finiteStratification_rank {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsFinite G.source.left] [IsFinite G.target.left] (r : ℕ) (hr : 0 < r) :
    ∃ W : (finiteStratification G (r - 1)).subscheme.Opens,
      Set.range (W.ι ≫ (finiteStratification G (r - 1)).subschemeι) =
          ((finiteStratification G (r - 1)).support : Set G.objects.left) \
            ((finiteStratification G r).support : Set G.objects.left) ∧
        IsFiniteLocallyFreeOfRank
          (pullback.snd G.source.left
            (W.ι ≫ (finiteStratification G (r - 1)).subschemeι)) r

Tag 0ABA, a lemma

Tag 0ABA in the Stacks Project.

AlgebraicGeometry.exists_invariant_thickening_finiteLocallyFree_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/FiniteGroupoidThickening.lean, line 1081.

Stacks Project, Tag 0ABA. A groupoid scheme with finite source and target has an invariant open subscheme W carrying an invariant closed thickening W' such that the source and target maps of the restriction of the groupoid to W' are finite locally free, and such that the saturation of the closure of W is the whole object scheme.

public theorem exists_invariant_thickening_finiteLocallyFree_restriction {S : Scheme.{u}}
    (G : GroupoidScheme S) [IsFinite G.source.left] [IsFinite G.target.left] :
    ∃ (W : G.objects.left.Opens) (W' : Scheme.{u}) (i : W' ⟶ W.toScheme)
      (hmono : Mono (i ≫ W.ι)),
      letI : Mono (i ≫ W.ι) := hmono
      IsInvariantOpen G W ∧
      IsInvariantMonomorphism G (i ≫ W.ι) ∧
      (G.target.left.base ''
        (G.source.left.base ⁻¹' closure (W : Set G.objects.left)) = Set.univ) ∧
      IsThickening i ∧
      (let g : Over.mk (i ≫ W.ι ≫ G.objects.hom) ⟶ G.objects := Over.homMk (i ≫ W.ι)
       IsFiniteLocallyFree (restrictionSource G g).left ∧
       IsFiniteLocallyFree (restrictionTarget G g).left)

Tag 0ABB, a lemma

Tag 0ABB in the Stacks Project.

AlgebraicGeometry.finitePresentation_layerThickeningInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/FinitePresentationThickening.lean, line 58. The attribute's comment: “finite_presentation”.

Stacks Project, Tag 0ABB (1). For a groupoid scheme with finite source and target whose source map is of finite presentation, the inclusion of the invariant closed thickening into the invariant open is of finite presentation: on each stage it is the base change of one member of the Fitting stratification along the inclusion of the open chosen there.

theorem finitePresentation_layerThickeningInclusion {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsFinite G.source.left] [IsFinite G.target.left]
    (hs : FinitePresentation G.source.left) :
    FinitePresentation (layerThickeningInclusion G)

AlgebraicGeometry.mem_layerUnionOpen_of_orbit_subset_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/FinitePresentationThickening.lean, line 119. The attribute's comment: “generic_orbit_mem”.

Stacks Project, Tag 0ABB (2). For a groupoid scheme with finite source and target whose source map is of finite presentation, a point whose orbit consists of generic points of irreducible components of the object scheme lies in the invariant open constructed for the groupoid.

theorem mem_layerUnionOpen_of_orbit_subset_genericPoints {S : Scheme.{u}}
    (G : GroupoidScheme S) [IsFinite G.source.left] [IsFinite G.target.left]
    (hs : FinitePresentation G.source.left) (x : G.objects.left)
    (hx : ∀ y : G.objects.left,
      (∃ r : G.arrows.left, G.source.left r = x ∧ G.target.left r = y) →
        y ∈ genericPoints G.objects.left) :
    x ∈ layerUnionOpen G

Tag 0ABC, a lemma

Tag 0ABC in the Stacks Project.

AlgebraicGeometry.exists_invariant_affine_open_with_finiteLocallyFree_thickening', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/GenericOrbitInvariantAffine.lean, line 1302.

[Stacks, Tag 0ABC]. Let G be a groupoid scheme whose source and target are finite and of finite presentation, with quasi-separated object scheme, and let x : ι → U be finitely many points whose orbits consist of generic points of irreducible components of the object scheme. Then there is an invariant affine open V of the object scheme and an ideal sheaf Z on it such that the closed subscheme V(Z) is an affine invariant thickening of finite presentation inside V containing the images of the x i, over which the source and target of the restricted groupoid are finite locally free.

Nothing is assumed beyond the hypotheses of the tag. This is AlgebraicGeometry.exists_invariant_affine_open_with_finiteLocallyFree_thickening, which carries [Stacks, Tag 06AD] as the hypothesis H06AD, with that hypothesis discharged by Stacks.Thickenings.forall_isAffine_of_isThickening, the library's 06AD.

theorem exists_invariant_affine_open_with_finiteLocallyFree_thickening'
    {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S)
    [IsFinite G.source.left] [IsFinite G.target.left]
    (hs : FinitePresentation G.source.left)
    (ht : FinitePresentation G.target.left)
    [QuasiSeparatedSpace G.objects.left]
    {ι : Type v} [Finite ι] (x : ι → G.objects.left)
    (hx : ∀ i y, (∃ r : G.arrows.left,
      G.source.left r = x i ∧ G.target.left r = y) →
        ∃ Z ∈ irreducibleComponents G.objects.left, IsGenericPoint y Z) :
    ∃ (V : G.objects.left.Opens) (Z : V.toScheme.IdealSheafData),
      (∀ i, x i ∈ Set.range (Z.subschemeι ≫ V.ι)) ∧
      Stacks.Groupoids.IsInvariantOpen G V ∧
      IsAffineOpen V ∧
      Stacks.Groupoids.IsInvariantMonomorphism G (Z.subschemeι ≫ V.ι) ∧
      IsAffine Z.subscheme ∧
      IsThickening Z.subschemeι ∧
      FinitePresentation Z.subschemeι ∧
      (let U' : Over S := Over.mk (Z.subschemeι ≫ V.ι ≫ G.objects.hom)
       let g : U' ⟶ G.objects := Over.homMk (Z.subschemeι ≫ V.ι) (by rfl)
       Stacks.Morphisms.IsFiniteLocallyFree
          (AlgebraicGeometry.GroupoidScheme.restrict G g).groupoid.source.left ∧
       Stacks.Morphisms.IsFiniteLocallyFree
          (AlgebraicGeometry.GroupoidScheme.restrict G g).groupoid.target.left)

Tag 0ABD, a lemma

Tag 0ABD in the Stacks Project.

AlgebraicGeometry.exists_invariant_affine_finiteLocallyFree_thickening_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/GenericOrbitInvariantAffine.lean, line 1392.

[Stacks, Tag 0ABD]. Let G be a groupoid scheme whose source and target are finite, with locally Noetherian object scheme, and let x : ι → U be finitely many points whose orbits consist of generic points of irreducible components of the object scheme. Then there is an invariant affine open V of the object scheme and an ideal sheaf Z on it such that the closed subscheme V(Z) is an affine invariant thickening inside V containing the images of the x i, over which the source and target of the restricted groupoid are finite locally free.

Nothing is assumed beyond the hypotheses: the affineness of V comes from [Stacks, Tag 01YQ] through AlgebraicGeometry.exists_isAffineOpen_preimage_eq_of_isThickening_of_isLocallyNoetherian.

theorem exists_invariant_affine_finiteLocallyFree_thickening_of_isLocallyNoetherian
    {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S)
    [IsFinite G.source.left] [IsFinite G.target.left]
    [IsLocallyNoetherian G.objects.left]
    {ι : Type v} [Finite ι] (x : ι → G.objects.left)
    (hx : ∀ i y, (∃ r : G.arrows.left,
      G.source.left r = x i ∧ G.target.left r = y) →
        ∃ Z ∈ irreducibleComponents G.objects.left, IsGenericPoint y Z) :
    ∃ (V : G.objects.left.Opens) (Z : V.toScheme.IdealSheafData),
      (∀ i, x i ∈ Set.range (Z.subschemeι ≫ V.ι)) ∧
      Stacks.Groupoids.IsInvariantOpen G V ∧
      IsAffineOpen V ∧
      Stacks.Groupoids.IsInvariantMonomorphism G (Z.subschemeι ≫ V.ι) ∧
      IsAffine Z.subscheme ∧
      IsThickening Z.subschemeι ∧
      (let U' : Over S := Over.mk (Z.subschemeι ≫ V.ι ≫ G.objects.hom)
       let g : U' ⟶ G.objects := Over.homMk (Z.subschemeι ≫ V.ι) (by rfl)
       Stacks.Morphisms.IsFiniteLocallyFree
          (AlgebraicGeometry.GroupoidScheme.restrict G g).groupoid.source.left ∧
       Stacks.Morphisms.IsFiniteLocallyFree
          (AlgebraicGeometry.GroupoidScheme.restrict G g).groupoid.target.left)

Tag 0ABE, a lemma

Tag 0ABE in the Stacks Project.

AlgebraicGeometry.exists_invariant_affine_open_of_restriction_integral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/InvariantAffineOpenDescent.lean, line 186.

[Stacks, Tag 0ABE]. Let G be a groupoid scheme over S whose source and target maps are integral, let g : U' ⟶ G.objects be integral with image meeting every orbit of G, and let R be the restriction of G along g. A point of the object scheme of R contained in an invariant affine open has its image in G.objects contained in an invariant affine open.

theorem exists_invariant_affine_open_of_restriction_integral
    (G : Stacks.Groupoids.GroupoidScheme S) [IsIntegralHom G.source.left]
    [IsIntegralHom G.target.left] {U' : Over S} {g : U' ⟶ G.objects} [IsIntegralHom g.left]
    (R : GroupoidScheme.Restriction G g)
    (horbit : ∀ u : G.objects.left, ∃ u' : U'.left, ∃ r : G.arrows.left,
      G.source.left r = u ∧ G.target.left r = g.left u')
    (u' : R.groupoid.objects.left) (W' : R.groupoid.objects.left.Opens)
    (hW'inv : Stacks.Groupoids.IsInvariantOpen R.groupoid W') (hW'aff : IsAffineOpen W')
    (hu' : u' ∈ W') :
    ∃ W : G.objects.left.Opens, Stacks.Groupoids.IsInvariantOpen G W ∧ IsAffineOpen W ∧
      R.hom.mapObjects.left u' ∈ W

Tag 0ABF, a lemma

Tag 0ABF in the Stacks Project.

AlgebraicGeometry.exists_mem_ideal_invariant_affine_preimage_basicOpen', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/InvariantPrincipalOpenGenericOrbits.lean, line 850.

[Stacks, Tag 0ABF]. Let G be a groupoid scheme whose source and target are finite and of finite presentation, let x : ι → U be finitely many points whose orbits consist of generic points of irreducible components of the object scheme, let j : U ⟶ Spec A be an immersion, and let I be an ideal of A whose vanishing locus misses the image of j and whose union with that image is closed. Then some h ∈ I has j ⁻¹ D(h) an invariant affine open of the object scheme containing all the x i.

Nothing is assumed beyond the hypotheses of the tag. This is AlgebraicGeometry.exists_mem_ideal_invariant_affine_preimage_basicOpen, which carries [Stacks, Tag 06AD] as the hypothesis H06AD, with that hypothesis discharged by Stacks.Thickenings.forall_isAffine_of_isThickening, which is Tag 06AD.

theorem exists_mem_ideal_invariant_affine_preimage_basicOpen'
    {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S)
    [IsFinite G.source.left] [IsFinite G.target.left]
    (hs : FinitePresentation G.source.left)
    (ht : FinitePresentation G.target.left)
    {ι : Type v} [Finite ι] (x : ι → G.objects.left)
    (hx : ∀ i y, (∃ r : G.arrows.left,
      G.source.left r = x i ∧ G.target.left r = y) →
        ∃ Z ∈ irreducibleComponents G.objects.left, IsGenericPoint y Z)
    {A : Type u} [CommRing A]
    (j : G.objects.left ⟶ Spec (CommRingCat.of A)) [IsImmersion j]
    (I : Ideal A)
    (hdisj : Disjoint (Set.range (j : G.objects.left → Spec (CommRingCat.of A)))
      (PrimeSpectrum.zeroLocus (I : Set A)))
    (hclosed : IsClosed (PrimeSpectrum.zeroLocus (I : Set A) ∪
      Set.range (j : G.objects.left → Spec (CommRingCat.of A)))) :
    ∃ h : A, h ∈ I ∧
      (let W := j ⁻¹ᵁ PrimeSpectrum.basicOpen h
       Stacks.Groupoids.IsInvariantOpen G W ∧ IsAffineOpen W ∧ ∀ i, x i ∈ W)

Tag 0ABG, a lemma

Tag 0ABG in the Stacks Project.

AlgebraicGeometry.not_specialization_of_exists_arrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/FiniteGroupoid.lean, line 63.

Distinct points joined by an arrow of a groupoid scheme with finite source and target cannot be related by specialization.

theorem not_specialization_of_exists_arrow {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsFinite G.source.left] [IsFinite G.target.left]
    {u u' : G.objects.left} (hne : u ≠ u')
    (horbit : ∃ r : G.arrows.left, G.source.left r = u ∧ G.target.left r = u') :
    ¬ (u ⤳ u')

Tag 0ABH, a lemma

Tag 0ABH in the Stacks Project.

AlgebraicGeometry.isAffine_of_isImmersion_of_isAffineOpen_preimage_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/AffineQuasiCompactImmersion.lean, line 46.

Stacks Project, Tag 0ABH. A quasi-compact immersion into an affine scheme whose restriction over a standard open is affine and the remainder of whose image is closed has an affine source.

theorem isAffine_of_isImmersion_of_isAffineOpen_preimage_basicOpen {A : Type u} [CommRing A]
    {V : Scheme.{u}} (j : V ⟶ Spec (CommRingCat.of A)) [IsImmersion j] [QuasiCompact j]
    (f : A) (hD : IsAffineOpen (j ⁻¹ᵁ PrimeSpectrum.basicOpen f))
    (hclosed : IsClosed (Set.range (j : V → Spec (CommRingCat.of A)) ∩
      ((Spec (CommRingCat.of A)).basicOpen
        ((Scheme.ΓSpecIso (CommRingCat.of A)).inv f) :
          Set (Spec (CommRingCat.of A)))ᶜ)) : IsAffine V

Tag 0ABI, a lemma

Tag 0ABI in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.exists_isInvariantOpen_isAffineOpen_mem_of_krullDimLE_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/InvariantAffineOpenDimensionOne.lean, line 125.

Let G be a groupoid scheme whose source and target maps are finite and whose object scheme is separated and locally Noetherian, and let u be a point of the object scheme such that every point of the orbit of u has a stalk of Krull dimension at most one. Then u lies in an invariant affine open of the object scheme.

theorem exists_isInvariantOpen_isAffineOpen_mem_of_krullDimLE_one
    (G : GroupoidScheme S) [IsFinite G.source.left] [IsFinite G.target.left]
    [G.objects.left.IsSeparated] [IsLocallyNoetherian G.objects.left]
    (u : G.objects.left)
    (hdim : ∀ u' : G.objects.left,
      (∃ r : G.arrows.left, G.source.left.base r = u ∧ G.target.left.base r = u') →
        Ring.KrullDimLE 1 (G.objects.left.presheaf.stalk u')) :
    ∃ W : G.objects.left.Opens, IsInvariantOpen G W ∧ IsAffineOpen W ∧ u ∈ W

Sources

LeanStacks.Groupoids.finiteStratification · Stacks.Groupoids.finiteStratification_zero · Stacks.Groupoids.finiteStratification_mono · Stacks.Groupoids.finiteStratification_exhaustive · Stacks.Groupoids.finiteStratification_invariant · Stacks.Groupoids.finiteStratification_rank · AlgebraicGeometry.exists_invariant_thickening_finiteLocallyFree_restriction · AlgebraicGeometry.finitePresentation_layerThickeningInclusion

Section40.15 Descending ind-quasi-affine morphisms #

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

Tag 0APH, an equation

Tag 0APH in the Stacks Project.

AlgebraicGeometry.colimit_sections_equiv_sections_iInter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/SectionsOnIntersection.lean, line 756.

Sections on the intersection of a nonempty directed family of quasi-compact opens of a quasi-separated scheme are the filtered colimit of the sections on those opens. The equivalence commutes with every canonical map from a stage.

theorem colimit_sections_equiv_sections_iInter
    {X : AlgebraicGeometry.Scheme.{u}} {I : Type u}
    [QuasiSeparatedSpace X] [Nonempty I]
    (F : X.toTopCat.Sheaf (Type u)) (U : I → Opens X)
    (hqc : ∀ i, IsCompact (U i : Set X))
    (hdir : ∀ i j, ∃ k, (U k : Set X) ⊆ U i ∩ U j) (E : Set X)
    (hE : E = ⋂ i, (U i : Set X)) :
    ∃ e : colimit (sectionsDiagram F U) ≃ sectionsOnSubset E F,
      ∀ (i : intersectionIndex U) (s : (sectionsDiagram F U).obj i),
        e (colimit.ι (sectionsDiagram F U) i s) =
          stageToSubset F U E
            (fun j ↦ by rw [hE]; exact Set.iInter_subset _ j) i s

Tag 0API, a lemma

Tag 0API in the Stacks Project.

AlgebraicGeometry.exists_iInter_iso_iInter_in_specΓ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/IntersectionEmbedding.lean, line 1166. The attribute's comment: “intersection_embedding”.

Stacks Project, Tag 0API. The canonical map from a nonempty intersection of quasi-compact opens in an ind-quasi-affine scheme to the spectrum of its ring of sections identifies it, as a locally ringed space, with an intersection of quasi-compact opens in that spectrum. Each comparison map to the spectrum of a stage is the spectrum of the restriction map of functions from that stage.

theorem exists_iInter_iso_iInter_in_specΓ
    {X : Scheme.{u}} [AlgebraicGeometry.IsIndQuasiAffine X]
    {I : Type v} [Nonempty I] (U : I → X.Opens)
    (hU : ∀ i, IsCompact (U i : Set X)) :
    let E : Set X := ⋂ i, (U i : Set X)
    let Z := subsetLocallyRingedSpace X.toLocallyRingedSpace E
    let Y := Spec.toLocallyRingedSpace.obj (op (LocallyRingedSpace.Γ.obj (op Z)))
    ∃ (p : ∀ i, Y ⟶ Spec.toLocallyRingedSpace.obj (op Γ(X, U i)))
      (V : I → Opens Y),
      (∀ i, IsCompact (V i : Set Y)) ∧
      (∀ i, (V i : Set Y) = (p i).base ⁻¹' Set.range (U i).toSpecΓ.base) ∧
      (∀ i (x : E), (p i).base (Z.toΓSpec.base x) =
        (U i).toSpecΓ.base ⟨x.1, Set.mem_iInter.mp x.2 i⟩) ∧
      (∀ i (W : Set X), IsOpen W → W ⊆ E →
        (p i).base ⁻¹' ((U i).toSpecΓ.base ''
          {x : U i | (x : X) ∈ W}) =
        Z.toΓSpec.base '' {x : E | (x : X) ∈ W}) ∧
      (∀ i, p i = (Scheme.Spec.map (X.openToSubset (U i) E
        (Set.iInter_subset (fun k ↦ (U k : Set X)) i)).op).toLRSHom) ∧
      ∃ e : Z ≅ subsetLocallyRingedSpace Y (⋂ i, (V i : Set Y)),
          e.hom.toHom ≫ ofSubset Y (⋂ i, (V i : Set Y)) =
            (identityToΓSpec.app Z).toHom

AlgebraicGeometry.isOpen_image_toΓSpec_of_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/IntersectionEmbedding.lean, line 1249. The attribute's comment: “open_image”.

Stacks Project, Tag 0API (open image). The canonical map from an intersection of a nonempty family of quasi-compact opens in an ind-quasi-affine scheme to the spectrum of its global sections sends subsets which are open in the ambient scheme to open subsets.

theorem isOpen_image_toΓSpec_of_isOpen
    (X : Scheme.{u}) [AlgebraicGeometry.IsIndQuasiAffine X]
    {I : Type v} [Nonempty I] (U : I → X.Opens)
    (hU : ∀ i, IsCompact (U i : Set X))
    (E W : Set X) (hE : E = ⋂ i, (U i : Set X))
    (hWE : W ⊆ E) (hW : IsOpen W) :
    IsOpen
      ((subsetLocallyRingedSpace
          X.toLocallyRingedSpace E).toΓSpec.base ''
        { x : E | (x : X) ∈ W })

Tag 0APJ, a lemma

Tag 0APJ in the Stacks Project.

AlgebraicGeometry.sectionsRingOnSubset_preimage_iInter_iso_pushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/More/Properties/IndQuasiAffineDescent.lean, line 177.

Stacks Project, Tag 0APJ. In a cartesian square of schemes over the affine schemes Spec B ⟶ Spec A, where A ⟶ B is flat, formation of sections over a nonempty intersection of quasi-compact opens commutes with base change.

theorem sectionsRingOnSubset_preimage_iInter_iso_pushout
    {A B : CommRingCat.{u}} (φ : A ⟶ B) {X Y : Scheme.{u}}
    (g : X ⟶ Scheme.Spec.obj (op B)) (f : X ⟶ Y)
    (h : Y ⟶ Scheme.Spec.obj (op A))
    (H : IsPullback g f (Scheme.Spec.map φ.op) h)
    {ι : Type v} [Nonempty ι] (V : ι → Y.Opens)
    (hV : ∀ i, IsCompact (V i : Set Y)) [QuasiSeparatedSpace Y]
    (hφ : φ.hom.Flat) :
    ∃ e : pushout (toSectionsOnSubset h (⋂ i, (V i : Set Y))) φ ≅
        X.sectionsRingOnSubset (f ⁻¹' (⋂ i, (V i : Set Y))),
      (pushout.inr _ _ ≫ e.hom =
        toSectionsOnSubset g (f ⁻¹' (⋂ i, (V i : Set Y)))) ∧
      (∀ (U : Y.Opens) (hU : (⋂ i, (V i : Set Y)) ⊆ U),
        Y.restrictOpenToSubset (⋂ i, (V i : Set Y)) U hU ≫
            pushout.inl _ _ ≫ e.hom =
          f.appLE U (f ⁻¹ᵁ U) le_rfl ≫
            X.restrictOpenToSubset (f ⁻¹' (⋂ i, (V i : Set Y))) (f ⁻¹ᵁ U) (by
              intro x hx
              exact Set.mem_preimage.mpr (hU (Set.mem_preimage.mp hx))))

AlgebraicGeometry.isPushout_sectionsRingOnSubset_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Slicing/FlatBaseChangeOnIntersection.lean, line 315.

Let
  X ---k---→ Spec R
  |            |
  p            g
  ↓            ↓
  Y ---πY--→ Spec A
be a Cartesian diagram of schemes, let E ⊆ Y be an intersection of a nonempty family of quasi-compact opens of Y, and suppose that Y is quasi-separated and that g is flat. Then
Γ(p⁻¹E, 𝒪_X|_{p⁻¹E}) = Γ(E, 𝒪_Y|_E) ⊗_{Γ(Spec A, ⊤)} Γ(Spec R, ⊤) :
the square formed by the restrictions of the global functions of Spec A and of Spec R to E and to p⁻¹E is a pushout of rings.

The comparison morphism Γ(E, 𝒪_Y|_E) ⟶ Γ(p⁻¹E, 𝒪_X|_{p⁻¹E}) is produced by the statement and characterized by the second conjunct: it agrees with the restriction along p on each member of the given family.

theorem isPushout_sectionsRingOnSubset_of_flat {A R : CommRingCat.{u}} {Y X : Scheme.{u}}
    {πY : Y ⟶ Spec A} {g : Spec R ⟶ Spec A} {p : X ⟶ Y} {k : X ⟶ Spec R}
    (H : IsPullback p k πY g) [Flat g] [QuasiSeparatedSpace Y] {I : Type u} [Nonempty I]
    (V : I → Y.Opens) (hV : ∀ i, IsCompact (V i : Set Y))
    (E : Set Y) (hE : E = ⋂ i, (V i : Set Y)) :
    ∃ w : Y.sectionsRingOnSubset E ⟶ X.sectionsRingOnSubset (p.base ⁻¹' E),
      IsPushout (πY.appTop ≫ Y.topToSubset E) g.appTop w
          (k.appTop ≫ X.topToSubset (p.base ⁻¹' E)) ∧
        ∀ i : I,
          Y.stageToSubset V E (fun j ↦ hE ▸ Set.iInter_subset _ j) ⟨i⟩ ≫ w =
            p.appLE (V i) (p ⁻¹ᵁ V i) le_rfl ≫
              X.stageToSubset (fun j ↦ p ⁻¹ᵁ V j) (p.base ⁻¹' E)
                (fun j ↦ hE ▸ Set.preimage_mono (Set.iInter_subset _ j)) ⟨i⟩

Tag 0APK, a lemma

Tag 0APK in the Stacks Project.

AlgebraicGeometry.DescentData.isFamilyEffective_of_forall_isIndQuasiAffineHom_of_anyIndex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/IndQuasiAffineFpqcEffective.lean, line 119. References: SGA 1 VIII (7.9), “partial”; SGA 3 IX (2.3), “partial”; SGA 3 VIII (1.7.2), “more general”; SGA 3 X (5.4), “more general”; SGA 3 XI (4.2), “partial”; SGA 3 XXIV (3.11.2), “partial”.

Stacks, Tag 0APK, Gabber's theorem. Let S be a scheme, let {X i ⟶ S} be an fpqc covering family, indexed by a type in an arbitrary universe, and let D be a descent datum relative to it each of whose component morphisms V i ⟶ X i is ind-quasi-affine. Then D is effective: it is isomorphic to the canonical descent datum of a scheme over S.

Ind-quasi-affineness is stable under base change, Stacks 0AP7, and closed under finite disjoint unions, so the general-base fpqc reduction of Stacks 02W3, AlgebraicGeometry.DescentData.isFamilyEffective_fpqc_of_affineSingleton_of_anyIndex, reduces the statement to the case of a surjective flat morphism of affine schemes, which is AlgebraicGeometry.DescentDatum.isEffective_of_isIndQuasiAffineHom.

theorem isFamilyEffective_of_forall_isIndQuasiAffineHom_of_anyIndex {ι : Type v} {S : Scheme.{u}}
    {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ S)
    (hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage S)
    (D : DescentData f) (hP : ∀ i, IsIndQuasiAffineHom (D.obj i).hom) :
    D.IsFamilyEffective

AlgebraicGeometry.DescentData.isFamilyEffective_of_forall_isIndQuasiAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/IndQuasiAffineFpqcEffective.lean, line 144. The attribute's comment: “the case of an affine base”. References: SGA 1 VIII (7.9), “special case”; SGA 3 IX (2.3), “partial”; SGA 3 VIII (1.7.2), “(ii), special case”; SGA 3 X (5.4), “special case”; SGA 3 XXIV (3.11.2), “partial”.

Stacks, Tag 0APK over an affine base. Let S be an affine scheme, let {X i ⟶ S} be an fpqc covering family and let D be a descent datum relative to it each of whose component morphisms is ind-quasi-affine. Then D is effective: it is isomorphic to the canonical descent datum of a scheme over S.

This is the special case of AlgebraicGeometry.DescentData.isFamilyEffective_of_forall_isIndQuasiAffineHom_of_anyIndex kept for the consumers taking this shape.

theorem isFamilyEffective_of_forall_isIndQuasiAffineHom {ι : Type u} {S : Scheme.{u}} [IsAffine S]
    {X : ι → Scheme.{u}} (f : ∀ i, X i ⟶ S)
    (hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage S)
    (D : DescentData f) (hP : ∀ i, IsIndQuasiAffineHom (D.obj i).hom) :
    D.IsFamilyEffective

AlgebraicGeometry.DescentDatum.isEffective_of_isIndQuasiAffineHom_of_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SeparatedQuasiFiniteSchemeDescent.lean, line 170. The attribute's comment: “the case of a one-member covering by a surjective flat quasi-compact morphism, over an arbitrary base”. References: SGA 1 VIII (7.8), “partial”; SGA 1 VIII (7.9), “partial”; SGA 3 X (5.4), “special case”; SGA 3 XI (4.2), “more general”.

Gabber's effectivity for ind-quasi-affine descent data along a single quasi-compact fpqc covering. A descent datum relative to a surjective, flat, quasi-compact morphism f : X ⟶ S whose structure morphism V ⟶ X is ind-quasi-affine is effective.

This is Stacks, Tag 0APK for a one-member covering, over an arbitrary base.

theorem isEffective_of_isIndQuasiAffineHom_of_quasiCompact {S X : Scheme.{u}} {f : X ⟶ S}
    [Surjective f] [Flat f] [QuasiCompact f] (D : DescentDatum f)
    (hiqa : IsIndQuasiAffineHom D.over.hom) : DescentData.IsEffective D

Sources

LeanAlgebraicGeometry.colimit_sections_equiv_sections_iInter · AlgebraicGeometry.exists_iInter_iso_iInter_in_specΓ · AlgebraicGeometry.isOpen_image_toΓSpec_of_isOpen · AlgebraicGeometry.sectionsRingOnSubset_preimage_iInter_iso_pushout · AlgebraicGeometry.isPushout_sectionsRingOnSubset_of_flat · AlgebraicGeometry.DescentData.isFamilyEffective_of_forall_isIndQuasiAffineHom_of_anyIndex · AlgebraicGeometry.DescentData.isFamilyEffective_of_forall_isIndQuasiAffineHom · AlgebraicGeometry.DescentDatum.isEffective_of_isIndQuasiAffineHom_of_quasiCompact

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

40 More on Groupoid Schemes

Section40.3 Useful diagrams#

Tag 04LF, an equation

Tag 04LG, an equation

Sources

Section40.4 Sheaf of differentials#

Tag 04R9, a lemma

Sources

Section40.5 Local structure#

Tag 0CK4, a lemma

Sources

Section40.6 Properties of groupoids#

Tag 04LH, a lemma

Tag 04LI, a remark

Tag 047W, a remark

Tag 03JC, a lemma

Tag 06QQ, a lemma

Sources

Section40.7 Comparing fibres#

Tag 02YF, a lemma

Sources

Section40.8 Cohen-Macaulay presentations#

Tag 0460, a lemma

Sources

Section40.9 Restricting groupoids#

Tag 04MN, an equation

Tag 04MP, a lemma

Tag 04MV, a lemma

Tag 04MW, a lemma

Tag 04MX, a lemma

Sources

Section40.10 Properties of groupoids on fields#

Tag 04LM, a lemma

Tag 04LN, a lemma

Tag 04LP, a lemma

Tag 04LQ, a lemma

Tag 04LR, a lemma

Tag 04LS, a lemma

Tag 0B7V, a lemma

Tag 04LT, a lemma

Tag 04LU, a lemma

Tag 04MQ, a lemma

Tag 04MR, a remark

Tag 04RA, a lemma

Tag 04RB, a lemma

Sources

Section40.11 Morphisms of groupoids on fields#

Tag 04Q5, a situation

Tag 04Q6, a lemma

Tag 04Q7, a lemma

Tag 04Q8, a lemma

Tag 04Q9, a lemma

Tag 04QA, a lemma

Tag 04QB, a lemma

Tag 04QC, a lemma

Tag 04QD, a lemma

Sources

Section40.12 Slicing groupoids#

Tag 04MY, a situation

Tag 0461, a lemma

Tag 04MZ, a lemma

Tag 04N0, a lemma

Sources

Section40.13 Étale localization of groupoids#

Tag 03FL, a lemma

Tag 03X5, a lemma

Sources

Section40.14 Finite groupoids#

Tag 0AB9, a lemma

Tag 0ABA, a lemma

Tag 0ABB, a lemma

Tag 0ABC, a lemma

Tag 0ABD, a lemma

Tag 0ABE, a lemma

Tag 0ABF, a lemma

Tag 0ABG, a lemma

Tag 0ABH, a lemma

Tag 0ABI, a lemma

Sources

Section40.15 Descending ind-quasi-affine morphisms#

Section40.3 Useful diagrams #

Section40.4 Sheaf of differentials #

Section40.5 Local structure #

Section40.6 Properties of groupoids #

Section40.7 Comparing fibres #

Section40.8 Cohen-Macaulay presentations #

Section40.9 Restricting groupoids #

Section40.10 Properties of groupoids on fields #

Section40.11 Morphisms of groupoids on fields #

Section40.12 Slicing groupoids #

Section40.13 Étale localization of groupoids #

Section40.14 Finite groupoids #

Section40.15 Descending ind-quasi-affine morphisms #