79 More on Groupoids in Spaces

Chapter 79 of the Stacks Project, More on Groupoids in Spaces, Tag 04P4: the 14 sections of its 15 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 64 tags are carried by 200 declarations of the repository (all in StacksFrontier) and 6 registered declarations.

Section79.1 Introduction#

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

Tag 04P6, an equation

Tag 04P6 in the Stacks Project.

AlgebraicGeometry.Stack.quotientStackSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/TwoFibreProduct.lean, line 138. The attribute's comment: “the displayed square of a groupoid over its quotient stack”.

The canonical source-target square over the quotient stack.

noncomputable def quotientStackSquare
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    let J := BigFppfOver.topology C S hS
    let U : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨liftedFibredCategory G.objects,
        isStackInGroupoids_liftedFibredCategory G.objects⟩
    let Q : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨quotientStack G,
        isStackInGroupoids_quotientStack G⟩
    Bicategory.TwoCommSq
      (Bicategory.InducedBicategory.mkHom
        (liftedQuotientStackProjection G) : U ⟶ Q)
      (Bicategory.InducedBicategory.mkHom
        (liftedQuotientStackProjection G) : U ⟶ Q)

AlgebraicGeometry.Stack.quotientStack_twoCartesian_source_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackSquares/TwoFibreProduct.lean, line 1044. The attribute's comment: “the 2-cartesian square R ⇉ U → [U/R]: legs s, t, π twice, 2-arrow of 044S”.

The 2-cartesian square R ⇉ U → [U/R]. Take the square whose apex is the arrow space R, whose two legs R ⟶ U are the source s and the target t, whose two maps U ⟶ [U/R] are both the projection π, and whose filler is the canonical 2-arrow π ∘ s ⟶ π ∘ t of Stacks 044S. That 2-arrow is invertible, so the square 2-commutes through it, and the square is 2-cartesian. Here R and U stand for the stacks in groupoids attached to the two spaces.

theorem quotientStack_twoCartesian_source_target
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    let J := BigFppfOver.topology C S hS
    let R : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨liftedFibredCategory G.arrows, isStackInGroupoids_liftedFibredCategory G.arrows⟩
    let U : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨liftedFibredCategory G.objects, isStackInGroupoids_liftedFibredCategory G.objects⟩
    let Q : StackInGroupoids (BigFppfOver C S hS) J :=
      ⟨quotientStack G, isStackInGroupoids_quotientStack G⟩
    let s : R ⟶ U := Bicategory.InducedBicategory.mkHom (liftedAssociatedMap G.source)
    let t : R ⟶ U := Bicategory.InducedBicategory.mkHom (liftedAssociatedMap G.target)
    let π : U ⟶ Q := Bicategory.InducedBicategory.mkHom (liftedQuotientStackProjection G)
    ∃ γ : s ≫ π ≅ t ≫ π,
      γ.hom = Bicategory.InducedBicategory.mkHom₂ (liftedQuotientStackTwoArrow G) ∧
      Nonempty (Bicategory.IsTwoFibreProduct
        ({ pt := R, fst := s, snd := t, iso := γ } : Bicategory.TwoCommSq π π))
Sources
LeanAlgebraicGeometry.Stack.quotientStackSquare · AlgebraicGeometry.Stack.quotientStack_twoCartesian_source_target

Section79.3 Useful diagrams#

Section 79.3 of the Stacks Project, Tag 04P8. 2 tags here are carried by 10 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04P9, an equation

Tag 04P9 in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isPullback_fst_snd_source_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 190. The attribute's comment: “the lower-left square”.

Stacks 0450, the lower-left square for the projections. The two projections out of the space of composable pairs of arrows of a groupoid in algebraic spaces form a cartesian square with the source and the target morphisms: a composable pair is exactly a pair of arrows whose first arrow has as its source the target of the second.

theorem isPullback_fst_snd_source_target (G : GroupoidInAlgebraicSpaces C S hS B) :
    IsPullback
      (ObjectProperty.homMk (pullback.fst G.source.hom G.target.hom) :
        AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows)
      (ObjectProperty.homMk (pullback.snd G.source.hom G.target.hom) :
        AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows)
      G.source G.target

Declarations registered for the tag:

Tag 0451, an equation

Tag 0451 in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 108. The attribute's comment: “the displayed diagram, through its vertical comparison pr_0 × c ∘ (i,1)”.

Stacks 0450. The canonical comparison (α, β) ↦ (α, α⁻¹ ∘ β) of the space of pairs of arrows of a groupoid in algebraic spaces with a common target with the space of composable pairs of arrows.

noncomputable def commonTargetPairsIso (G : GroupoidInAlgebraicSpaces C S hS B) :
    AlgebraicSpaces.fiberProduct C S hS G.target G.target ≅
      AlgebraicSpaces.fiberProduct C S hS G.source G.target

AlgebraicGeometry.GroupoidInAlgebraicSpaces.comp_source_eq_snd_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 165. The attribute's comment: “commutativity of the upper of the two lower left squares”.

Stacks 0450, the commutativity of the lower square for composition: c ≫ s = pr₁ ≫ s. The composite of a composable pair of arrows of a groupoid in algebraic spaces has the same source as the second arrow of the pair.

theorem comp_source_eq_snd_source (G : GroupoidInAlgebraicSpaces C S hS B) :
    G.comp ≫ G.source =
      (ObjectProperty.homMk (pullback.snd G.source.hom G.target.hom) :
        AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows) ≫ G.source

AlgebraicGeometry.GroupoidInAlgebraicSpaces.fst_source_eq_snd_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 176. The attribute's comment: “commutativity of the lower of the two lower left squares”.

Stacks 0450, the commutativity of the lower square for the projections: pr₀ ≫ s = pr₁ ≫ t. The first arrow of a composable pair of arrows of a groupoid in algebraic spaces has as its source the target of the second arrow of the pair.

theorem fst_source_eq_snd_target (G : GroupoidInAlgebraicSpaces C S hS B) :
    (ObjectProperty.homMk (pullback.fst G.source.hom G.target.hom) :
        AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows) ≫ G.source =
      (ObjectProperty.homMk (pullback.snd G.source.hom G.target.hom) :
        AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows) ≫ G.target

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isPullback_fst_snd_source_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 190. The attribute's comment: “the lower of the two lower left squares is cartesian”.

Stacks 0450, the lower-left square for the projections. The two projections out of the space of composable pairs of arrows of a groupoid in algebraic spaces form a cartesian square with the source and the target morphisms: a composable pair is exactly a pair of arrows whose first arrow has as its source the target of the second.

theorem isPullback_fst_snd_source_target (G : GroupoidInAlgebraicSpaces C S hS B) :
    IsPullback
      (ObjectProperty.homMk (pullback.fst G.source.hom G.target.hom) :
        AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows)
      (ObjectProperty.homMk (pullback.snd G.source.hom G.target.hom) :
        AlgebraicSpaces.fiberProduct C S hS G.source G.target ⟶ G.arrows)
      G.source G.target

AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 243. The attribute's comment: “the vertical comparison pr_0 × c ∘ (i, 1)”.

Stacks 0451. The vertical comparison pr_0 × c ∘ (i, 1) of the diagram: it sends a pair (α, β) of arrows with a common target to the composable pair (α, α⁻¹ ∘ β).

noncomputable def commonTargetPairsComparison (G : GroupoidInAlgebraicSpaces C S hS B) :
    AlgebraicSpaces.fiberProduct C S hS G.target G.target ⟶
      AlgebraicSpaces.fiberProduct C S hS G.source G.target

AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsComparison_comp_firstArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 259. The attribute's comment: “the lower square on the left of the top two rows”.

Stacks 0451, the lower of the two squares on the left of the top two rows: the vertical comparison preserves the first arrow.

theorem commonTargetPairsComparison_comp_firstArrow
    (G : GroupoidInAlgebraicSpaces C S hS B) :
    commonTargetPairsComparison G ≫ firstArrow G = commonTargetFirstArrow G

AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsComparison_comp_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 314. The attribute's comment: “the upper square on the left of the top two rows”.

Stacks 0451, the upper of the two squares on the left of the top two rows: composing the vertical comparison with the composition of the groupoid recovers the second arrow, because α ∘ (α⁻¹ ∘ β) = β.

theorem commonTargetPairsComparison_comp_comp (G : GroupoidInAlgebraicSpaces C S hS B) :
    commonTargetPairsComparison G ≫ G.comp = commonTargetSecondArrow G

AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsIso_hom_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 347. The attribute's comment: “the two top rows are isomorphic via the vertical maps given”.

Stacks 0451. The vertical comparison drawn in the diagram, pr_0 × c ∘ (i, 1), is the canonical comparison of the two fibre products, hence an isomorphism: this is the assertion that the two top rows of the diagram are isomorphic via the vertical maps given, the other two vertical maps being the identities.

theorem commonTargetPairsIso_hom_eq (G : GroupoidInAlgebraicSpaces C S hS B) :
    (commonTargetPairsIso G).hom = commonTargetPairsComparison G

AlgebraicGeometry.GroupoidInAlgebraicSpaces.id_comp_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/CommonTargetPairs.lean, line 365. The attribute's comment: “the square on the right of the top two rows”.

Stacks 0451, the square on the right of the top two rows: both of its vertical maps are identities, of the arrow space and of the object space, and its two horizontal maps are the target.

theorem id_comp_target (G : GroupoidInAlgebraicSpaces C S hS B) :
    𝟙 G.arrows ≫ G.target = G.target ≫ 𝟙 G.objects

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.GroupoidInAlgebraicSpaces.isPullback_fst_snd_source_target · AlgebraicGeometry.AlgebraicSpaces.isPullback_fiberProduct · AlgebraicGeometry.Space.isPullback_comp_source · AlgebraicGeometry.Space.isPullback_fst_comp · AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsIso · AlgebraicGeometry.GroupoidInAlgebraicSpaces.comp_source_eq_snd_source · AlgebraicGeometry.GroupoidInAlgebraicSpaces.fst_source_eq_snd_target · AlgebraicGeometry.GroupoidInAlgebraicSpaces.commonTargetPairsComparison

Section79.4 Local structure#

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

Tag 0CK9, the section

Tag 0CK9 in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.localStructure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/LocalStructure/GeometricStalkTensorHenselization.lean, line 633. The attribute's comment: “The whole section, for the etale local rings A = O_{U,u-bar}, B = O_{R,e(u-bar)} and C = O_{R x_{s,U,t} R,(e,e)(u-bar)} of a groupoid in algebraic spaces at a geometric point u-bar: (1) A, B, C are local and the maps s, t, c, e, i, (e,e) they induce are local homomorphisms; (2) e . t = 1 = e . s; (3) B = s(A) + I = t(A) + I as direct sums, I = ker e; (4) m_B (x) B + B (x) m_B is a maximal ideal of B (x)_{s,A,t} B (the pushout of s and t in CommRingCat), the localization at it has separably closed residue field, and C is the henselization of that localization through the map induced by b1 (x) b2 -> pr1(b1) pr2(b2); (5) the ideal J of C generated by I (x) B + B (x) I is the kernel of (e,e) : C -> A; (6) c : B -> C sends I into J.”.

Stacks 0CK9 (Local structure). Let (U, R, s, t, c, e, i) be a groupoid in algebraic spaces over S, let ū be a geometric point of U, and let A = 𝒪_{U, ū}, B = 𝒪_{R, e(ū)} and C = 𝒪_{R ×_{s, U, t} R, (e, e)(ū)} be the étale local rings, with the homomorphisms s, t : A → B, c : B → C, e : B → A, i : B → B and (e, e) : C → A induced by the structure morphisms. Then:

  1. A, B, C are local rings and s, t, c, e, i, (e, e) are local homomorphisms;
  2. e ∘ t = 1 and e ∘ s = 1;
  3. B = s(A) ⊕ I = t(A) ⊕ I for I = ker (e : B → A);
  4. 𝔪_B ⊗ B + B ⊗ 𝔪_B is a maximal ideal of B ⊗_{s, A, t} B, the localization at it has separably closed residue field, and C is the henselization of that localization through the homomorphism induced by b₁ ⊗ b₂ ↦ pr₁(b₁) pr₂(b₂);
  5. the ideal J of C generated by I ⊗ B + B ⊗ I is the kernel of (e, e) : C → A;
  6. c sends I into J.
theorem localStructure :
    (IsLocalRing (Space.etaleLocalRing C S hS G.objects.obj z) ∧
      IsLocalRing (Space.etaleLocalRing C S hS G.arrows.obj (identityArrowPoint G z)) ∧
      IsLocalRing (Space.etaleLocalRing C S hS (pullback G.source.hom G.target.hom)
        (identityPairPoint G z)) ∧
      IsLocalHom (sourceStalk G z) ∧ IsLocalHom (targetStalk G z) ∧
      IsLocalHom (identityPairComp G z) ∧ IsLocalHom (identityStalk G z) ∧
      IsLocalHom (inverseStalk G z) ∧ IsLocalHom (identityPairStalk G z)) ∧
    ((identityStalk G z).comp (targetStalk G z) = RingHom.id _ ∧
      (identityStalk G z).comp (sourceStalk G z) = RingHom.id _) ∧
    (IsCompl (sourceStalk G z).range.toAddSubgroup
        (RingHom.ker (identityStalk G z)).toAddSubgroup ∧
      IsCompl (targetStalk G z).range.toAddSubgroup
        (RingHom.ker (identityStalk G z)).toAddSubgroup) ∧
    ((pushoutMaximalIdeal (sourceStalk G z) (targetStalk G z)).IsMaximal ∧
      IsSepClosed (ResidueField
        (Localization.AtPrime (pushoutMaximalIdeal (sourceStalk G z) (targetStalk G z)))) ∧
      ∃ φ : Localization.AtPrime (pushoutMaximalIdeal (sourceStalk G z) (targetStalk G z)) →+*
          Space.etaleLocalRing C S hS (pullback G.source.hom G.target.hom)
            (identityPairPoint G z),
        φ.comp (algebraMap _ _) = identityPairTensorMap G z ∧ IsLocalHom φ ∧
        @IsLocalRing.IsHenselization
          (Localization.AtPrime (pushoutMaximalIdeal (sourceStalk G z) (targetStalk G z))) _ _
          (ResidueField
            (Localization.AtPrime (pushoutMaximalIdeal (sourceStalk G z) (targetStalk G z))))
          _ _ (Space.etaleLocalRing C S hS (pullback G.source.hom G.target.hom)
            (identityPairPoint G z)) _ _ φ.toAlgebra) ∧
    RingHom.ker (identityPairStalk G z) =
      ((RingHom.ker (identityStalk G z)).map (pushout.inl (CommRingCat.ofHom (sourceStalk G z))
          (CommRingCat.ofHom (targetStalk G z))).hom ⊔
        (RingHom.ker (identityStalk G z)).map (pushout.inr
          (CommRingCat.ofHom (sourceStalk G z)) (CommRingCat.ofHom (targetStalk G z))).hom).map
        (identityPairTensorMap G z) ∧
    (RingHom.ker (identityStalk G z)).map (identityPairComp G z) ≤
      ((RingHom.ker (identityStalk G z)).map (pushout.inl (CommRingCat.ofHom (sourceStalk G z))
          (CommRingCat.ofHom (targetStalk G z))).hom ⊔
        (RingHom.ker (identityStalk G z)).map (pushout.inr
          (CommRingCat.ofHom (sourceStalk G z)) (CommRingCat.ofHom (targetStalk G z))).hom).map
        (identityPairTensorMap G z)
Tag 0CKA, a lemma

Tag 0CKA in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.GroupoidInAlgebraicSpaces.localStructure · Stacks.Groupoids.GroupoidScheme.cotangent_composition · Stacks.Groupoids.GroupoidScheme.cotangent_inverse

Section79.5 Groupoid of sections#

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

Tag 0CKC, an equation

Tag 0CKC in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.sectionCompHom_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Sections.lean, line 72. The attribute's comment: “well-definedness of composition”.

The groupoid composition formula applied to two sections is again a section of the source morphism.

theorem sectionCompHom_source (δ₁ δ₂ : Section G) :
    sectionCompHom G δ₁ δ₂ ≫ G.source = 𝟙 G.objects

AlgebraicGeometry.GroupoidInAlgebraicSpaces.sectionComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Sections.lean, line 114. The attribute's comment: “composition formula”.

Composition of sections of a groupoid in algebraic spaces: δ₁ ∘ δ₂ = c(δ₁ ∘ t ∘ δ₂, δ₂), which is again a section by sectionCompHom_source.

noncomputable def sectionComp (δ₁ δ₂ : Section G) : Section G
Tag 0CKD, a lemma

Tag 0CKD in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.conormalMap_sectionTarget_eq_conormalMap_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/SectionsConormalAction.lean, line 420. The attribute's comment: “the conormal map induced by f = t ∘ δ equals the conormal map induced by the identity; only flatness of s is assumed”.

Stacks 0CKD. Let G = (U, R, s, t, c) be a groupoid in algebraic spaces, let U₀ ⊆ U be a closed subspace whose inverse images along the source and the target agree — the invariance of AlgebraicGeometry.GroupoidInAlgebraicSpaces.IsInvariantClosed — and let δ : U ⟶ R be a section of the source agreeing with the unit on U₀, and let s be flat. Then the conormal map of 𝒞_{U₀/U} induced by f = t ∘ δ is the conormal map induced by id_U, which is the canonical identification of (id_{U₀})^*𝒞_{U₀/U} with 𝒞_{U₀/U}. In the language of the source, f acts as the identity on 𝒞_{U₀/U}.

The source assumes s and t flat and U a first-order thickening of U₀; only flatness of s is used.

theorem conormalMap_sectionTarget_eq_conormalMap_id (δ : Section G)
    (hδ : subspaceInclusion C S hS G.objects U₀ ≫ δ.1 =
      subspaceInclusion C S hS G.objects U₀ ≫ identityArrow G)
    (hinv : U₀.1.preimage G.target.hom = U₀.1.preimage G.source.hom)
    (hs : Space.IsFlat C S hS G.source.hom)
    (hsq : subspaceInclusion C S hS G.objects U₀ ≫ (δ.1 ≫ G.target) =
      𝟙 _ ≫ subspaceInclusion C S hS G.objects U₀)
    (hsqId : subspaceInclusion C S hS G.objects U₀ ≫ 𝟙 G.objects =
      𝟙 _ ≫ subspaceInclusion C S hS G.objects U₀) :
    conormalMap C S hS U₀ U₀ (δ.1 ≫ G.target) (𝟙 _) hsq =
      conormalMap C S hS U₀ U₀ (𝟙 G.objects) (𝟙 _) hsqId

AlgebraicGeometry.GroupoidInAlgebraicSpaces.conormalMap_sectionTarget_comp_inv_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/SectionsConormalAction.lean, line 523. The attribute's comment: “f = t ∘ δ acts as the identity on the conormal module, read through the conormal map of the identity; only flatness of s is assumed”.

Stacks 0CKD, read as the identity. Transported across the conormal map of the identity square — the canonical identification of (id_{U₀})^*𝒞_{U₀/U} with 𝒞_{U₀/U}, an isomorphism by AlgebraicGeometry.Space.isIso_conormalMap_id — the conormal map induced by f = t ∘ δ is the identity: followed by the inverse of that identification it is the identity of (id_{U₀})^*𝒞_{U₀/U}. As in AlgebraicGeometry.GroupoidInAlgebraicSpaces.conormalMap_sectionTarget_eq_conormalMap_id, only flatness of s is assumed.

theorem conormalMap_sectionTarget_comp_inv_eq_id (δ : Section G)
    (hδ : subspaceInclusion C S hS G.objects U₀ ≫ δ.1 =
      subspaceInclusion C S hS G.objects U₀ ≫ identityArrow G)
    (hinv : U₀.1.preimage G.target.hom = U₀.1.preimage G.source.hom)
    (hs : Space.IsFlat C S hS G.source.hom)
    (hsq : subspaceInclusion C S hS G.objects U₀ ≫ (δ.1 ≫ G.target) =
      𝟙 _ ≫ subspaceInclusion C S hS G.objects U₀)
    (hsqId : subspaceInclusion C S hS G.objects U₀ ≫ 𝟙 G.objects =
      𝟙 _ ≫ subspaceInclusion C S hS G.objects U₀) :
    conormalMap C S hS U₀ U₀ (δ.1 ≫ G.target) (𝟙 _) hsq ≫
        @inv _ _ _ _ (conormalMap C S hS U₀ U₀ (𝟙 G.objects) (𝟙 _) hsqId)
          (isIso_conormalMap_id C S hS U₀ hsqId) = 𝟙 _
Tag 0CKE, an equation

Tag 0CKE in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.bijective_vadd_unitInfinitesimalSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/SectionsInfinitesimalBijection.lean, line 234. The attribute's comment: “the displayed bijection Hom_{O_{U_0}}(e_0^*Omega_{R_0/U_0}, C_{U_0/U}) -> Gamma_0, theta |-> theta . e, for a groupoid in algebraic spaces and a first order thickening U_0 of U”.

The displayed bijection of Equation (0CKE). Translation of the unit is a bijection from the 𝒪_{U₀}-linear maps θ : e₀^*Ω_{R₀/U₀} ⟶ 𝒞_{U₀/U} onto the sections Γ₀ of the source which agree with the unit on U₀: every δ ∈ Γ₀ is θ · e for exactly one θ.

theorem bijective_vadd_unitInfinitesimalSection :
    letI := (infinitesimalSectionDifference G U₀ hU₀).addAction
    Function.Bijective
      (fun θ : InfinitesimalSectionsHom G U₀ => θ +ᵥ unitInfinitesimalSection G U₀)

AlgebraicGeometry.GroupoidInAlgebraicSpaces.unitVAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/SectionsInfinitesimalBijection.lean, line 246. The attribute's comment: “the displayed arrow Hom_{O_{U_0}}(e_0^*Omega_{R_0/U_0}, C_{U_0/U}) -> Gamma_0 bundled as a bijection, for a groupoid in algebraic spaces and a first order thickening U_0 of U”.

Equation (0CKE) as a bijection. The map θ ↦ θ · e from the 𝒪_{U₀}-linear maps e₀^*Ω_{R₀/U₀} ⟶ 𝒞_{U₀/U} to the sections Γ₀ infinitesimally close to the unit, bundled with its inverse.

noncomputable def unitVAddEquiv :
    InfinitesimalSectionsHom G U₀ ≃ InfinitesimalSections G U₀
Tag 0CKF, a lemma

Tag 0CKF in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.unitVAddEquiv_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/SectionsInfinitesimalGroup.lean, line 365. The attribute's comment: “the bijection theta |-> theta . e of (0CKE) carries the sum of two linear maps e_0^*Omega_{R_0/U_0} -> C_{U_0/U} to the composite of the two sections in Gamma_0, for an R-invariant first order thickening U_0 of U”.

Lemma 0CKF. Let (U, R, s, t, c) be a groupoid in algebraic spaces, U₀ ⊆ U an R-invariant closed subspace such that U is a first order thickening of U₀. The bijection of Equation [Stacks Project, Tag 0CKE], θ ↦ θ · e from Hom_{𝒪_{U₀}}(e₀^*Ω_{R₀/U₀}, 𝒞_{U₀/U}) onto Γ₀, sends a sum of linear maps to the composite of the corresponding sections:

(θ₁ + θ₂) · e = (θ₁ · e) ∘ (θ₂ · e).

With InfinitesimalSectionDifference.unitVAddEquiv_zero (0 · e = e) this says that the bijection is an isomorphism of groups.

theorem unitVAddEquiv_add (hinv : U₀.1.preimage G.target.hom = U₀.1.preimage G.source.hom)
    (θ₁ θ₂ : InfinitesimalSectionsHom G U₀) :
    unitVAddEquiv G U₀ hU₀ (θ₁ + θ₂) =
      infinitesimalSectionComp G U₀ (unitVAddEquiv G U₀ hU₀ θ₁) (unitVAddEquiv G U₀ hU₀ θ₂)

AlgebraicGeometry.GroupoidInAlgebraicSpaces.unitVAddMulEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/SectionsInfinitesimalGroup.lean, line 399. The attribute's comment: “the bijection Hom_{O_{U_0}}(e_0^*Omega_{R_0/U_0}, C_{U_0/U}) -> Gamma_0 of (0CKE) as an isomorphism from the additive group of linear maps onto Gamma_0 with its composition, for an R-invariant first order thickening U_0 of U”.

Lemma 0CKF, bundled: the bijection (0CKE) is an isomorphism of groups. For an R-invariant closed subspace U₀ ⊆ U of which U is a first order thickening, the bijection θ ↦ θ · e of Equation [Stacks Project, Tag 0CKE] is a multiplicative equivalence from the additive group of the 𝒪_{U₀}-linear maps e₀^*Ω_{R₀/U₀} ⟶ 𝒞_{U₀/U} (written multiplicatively) onto Γ₀ with the composition of [Stacks Project, Tag 0CKC].

noncomputable def unitVAddMulEquiv
    (hinv : U₀.1.preimage G.target.hom = U₀.1.preimage G.source.hom) :
    Multiplicative (InfinitesimalSectionsHom G U₀) ≃* InfinitesimalSections G U₀
Sources
LeanAlgebraicGeometry.GroupoidInAlgebraicSpaces.sectionCompHom_source · AlgebraicGeometry.GroupoidInAlgebraicSpaces.sectionComp · AlgebraicGeometry.GroupoidInAlgebraicSpaces.conormalMap_sectionTarget_eq_conormalMap_id · AlgebraicGeometry.GroupoidInAlgebraicSpaces.conormalMap_sectionTarget_comp_inv_eq_id · AlgebraicGeometry.GroupoidInAlgebraicSpaces.bijective_vadd_unitInfinitesimalSection · AlgebraicGeometry.GroupoidInAlgebraicSpaces.unitVAddEquiv · AlgebraicGeometry.GroupoidInAlgebraicSpaces.unitVAddEquiv_add · AlgebraicGeometry.GroupoidInAlgebraicSpaces.unitVAddMulEquiv

Section79.6 Properties of groupoids#

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

Tag 044Z, a lemma

Tag 044Z in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isInvariantOpen_largestOpenSubspace_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/InvariantSourceLocus.lean, line 108.

Stacks 044Z. Let G be a groupoid in algebraic spaces whose source and target morphisms are both coverings for a topology τ other than the fpqc topology, and let P be a property of morphisms of algebraic spaces local on the target for τ. The largest open subspace of the object space over which the restriction of the source morphism has P is invariant under G.

theorem isInvariantOpen_largestOpenSubspace_source (G : GroupoidInAlgebraicSpaces C S hS B)
    (τ : Space.Topology) (hτ : τ ≠ .fpqc) (P : MorphismProperty (AlgebraicSpaces C S hS))
    [P.IsLocalAtTarget (Space.Topology.precoverage.{u, u + 1} τ C S hS)]
    (hs : τ.IsCovering C S hS (fun _ : Unit => G.arrows.obj) (fun _ => G.source.hom))
    (ht : τ.IsCovering C S hS (fun _ : Unit => G.arrows.obj) (fun _ => G.target.hom)) :
    IsInvariantOpen G (Space.largestOpenSubspace C S hS τ hτ P G.source).1.1
Tag 06R4, a lemma

Tag 06R4 in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.stabilizerProjectionOverOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/InvariantStabilizerLocus.lean, line 691. The attribute's comment: “the stabilizer restricted over an open subspace of the object space”.

Stacks 06R4. The restriction of the stabilizer of a groupoid in algebraic spaces over an open subspace of the object space.

noncomputable def stabilizerProjectionOverOpen
    (W : {W : Subfunctor G.objects.obj // Space.IsOpenSubspace C S hS W}) :
    AlgebraicSpaces.fiberProduct C S hS (stabilizerToObjects G)
        (Space.openInclusion C S hS W) ⟶ Space.openObject C S hS W

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isInvariantOpen_of_isGreatest_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/InvariantStabilizerLocus.lean, line 721. The attribute's comment: “invariance of the maximal open stabilizer-property locus”.

Stacks 06R4. Let G be a groupoid in algebraic spaces whose source and target morphisms are both coverings for a topology τ other than the fpqc topology, and let P be a property of morphisms of algebraic spaces local on the target for τ. A greatest open subspace of the object space over which the restriction of the stabilizer has P is invariant under G.

theorem isInvariantOpen_of_isGreatest_stabilizer (τ : Space.Topology) (hτ : τ ≠ .fpqc)
    (P : MorphismProperty (AlgebraicSpaces C S hS))
    [P.IsLocalAtTarget (Space.Topology.precoverage.{u, u + 1} τ C S hS)]
    (hs : τ.IsCovering C S hS (fun _ : Unit => G.arrows.obj) (fun _ => G.source.hom))
    (ht : τ.IsCovering C S hS (fun _ : Unit => G.arrows.obj) (fun _ => G.target.hom))
    (W : {W : Subfunctor G.objects.obj // Space.IsOpenSubspace C S hS W})
    (hW : IsGreatest {V : {V : Subfunctor G.objects.obj // Space.IsOpenSubspace C S hS V} |
      P (stabilizerProjectionOverOpen G V)} W) :
    IsInvariantOpen G W.1
Sources
LeanAlgebraicGeometry.GroupoidInAlgebraicSpaces.isInvariantOpen_largestOpenSubspace_source · AlgebraicGeometry.GroupoidInAlgebraicSpaces.stabilizerProjectionOverOpen · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isInvariantOpen_of_isGreatest_stabilizer

Section79.7 Comparing fibres#

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

Tag 0452, a lemma

Tag 0452 in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.sourceFibersIsoOfTargetEq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Fibres.lean, line 50.

Stacks 0452. Two arrows of a groupoid in algebraic spaces over a test algebraic space X with the same target have isomorphic source fibres over X.

theorem sourceFibersIsoOfTargetEq (C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
    (B : AlgebraicSpaces C S hS) (G : GroupoidInAlgebraicSpaces C S hS B)
    (X : AlgebraicSpaces C S hS) (r r' : X ⟶ G.arrows)
    (h : r ≫ G.target = r' ≫ G.target) :
    Nonempty
      ((Over.mk
          (ObjectProperty.homMk (pullback.fst (r ≫ G.source).hom G.source.hom) :
            AlgebraicSpaces.fiberProduct C S hS (r ≫ G.source) G.source ⟶ X) :
          Over X) ≅
       (Over.mk
          (ObjectProperty.homMk (pullback.fst (r' ≫ G.source).hom G.source.hom) :
            AlgebraicSpaces.fiberProduct C S hS (r' ≫ G.source) G.source ⟶ X) :
          Over X))
Sources
LeanAlgebraicGeometry.GroupoidInAlgebraicSpaces.sourceFibersIsoOfTargetEq

Section79.8 Restricting groupoids#

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

Tag 04RN, an equation

Tag 04RN in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.restrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidRestriction/Restrict.lean, line 59. The attribute's comment: “the fibre-product diagram defining R' with its source and target maps”.

Restriction along an arbitrary map to the object space, with its canonical composition law and functor to the original groupoid.

public noncomputable def restrict
    {C : BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S}
    {B : AlgebraicSpaces C S hS}
    (G : GroupoidInAlgebraicSpaces C S hS B)
    {U' : AlgebraicSpaces C S hS} (g : U' ⟶ G.objects) :
    Restriction G g
Tag 04RP, a lemma

Tag 04RP in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallyOfFiniteType_restrict_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/RestrictionProperties.lean, line 155. The attribute's comment: “part (1): the restricted source is locally of finite type”.

Stacks 04RP. If the source of a groupoid in algebraic spaces over B and the morphism g along which it is restricted are locally of finite type, then so is the source of the restriction.

theorem isLocallyOfFiniteType_restrict_source
    (hs : Space.IsLocallyOfFiniteType C S hS G.source.hom)
    (hg : Space.IsLocallyOfFiniteType C S hS g.hom) :
    Space.IsLocallyOfFiniteType C S hS (restrict G g).groupoid.source.hom

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallyOfFiniteType_restrict_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/RestrictionProperties.lean, line 168. The attribute's comment: “part (1): the restricted target is locally of finite type”.

Stacks 04RP. If the target of a groupoid in algebraic spaces over B and the morphism g along which it is restricted are locally of finite type, then so is the target of the restriction.

theorem isLocallyOfFiniteType_restrict_target
    (ht : Space.IsLocallyOfFiniteType C S hS G.target.hom)
    (hg : Space.IsLocallyOfFiniteType C S hS g.hom) :
    Space.IsLocallyOfFiniteType C S hS (restrict G g).groupoid.target.hom

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallyOfFinitePresentation_restrict_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/RestrictionProperties.lean, line 181. The attribute's comment: “part (2): the restricted source is locally of finite presentation”.

Stacks 04RP. If the source of a groupoid in algebraic spaces over B and the morphism g along which it is restricted are locally of finite presentation, then so is the source of the restriction.

theorem isLocallyOfFinitePresentation_restrict_source
    (hs : Space.IsLocallyOfFinitePresentation C S hS G.source.hom)
    (hg : Space.IsLocallyOfFinitePresentation C S hS g.hom) :
    Space.IsLocallyOfFinitePresentation C S hS (restrict G g).groupoid.source.hom

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallyOfFinitePresentation_restrict_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/RestrictionProperties.lean, line 194. The attribute's comment: “part (2): the restricted target is locally of finite presentation”.

Stacks 04RP. If the target of a groupoid in algebraic spaces over B and the morphism g along which it is restricted are locally of finite presentation, then so is the target of the restriction.

theorem isLocallyOfFinitePresentation_restrict_target
    (ht : Space.IsLocallyOfFinitePresentation C S hS G.target.hom)
    (hg : Space.IsLocallyOfFinitePresentation C S hS g.hom) :
    Space.IsLocallyOfFinitePresentation C S hS (restrict G g).groupoid.target.hom

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isFlat_restrict_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/RestrictionProperties.lean, line 206. The attribute's comment: “part (3): the restricted source is flat”.

Stacks 04RP. If the source of a groupoid in algebraic spaces over B and the morphism g along which it is restricted are flat, then so is the source of the restriction.

theorem isFlat_restrict_source (hs : Space.IsFlat C S hS G.source.hom)
    (hg : Space.IsFlat C S hS g.hom) :
    Space.IsFlat C S hS (restrict G g).groupoid.source.hom

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isFlat_restrict_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/RestrictionProperties.lean, line 216. The attribute's comment: “part (3): the restricted target is flat”.

Stacks 04RP. If the target of a groupoid in algebraic spaces over B and the morphism g along which it is restricted are flat, then so is the target of the restriction.

theorem isFlat_restrict_target (ht : Space.IsFlat C S hS G.target.hom)
    (hg : Space.IsFlat C S hS g.hom) :
    Space.IsFlat C S hS (restrict G g).groupoid.target.hom
Sources
LeanAlgebraicGeometry.GroupoidInAlgebraicSpaces.restrict · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallyOfFiniteType_restrict_source · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallyOfFiniteType_restrict_target · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallyOfFinitePresentation_restrict_source · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isLocallyOfFinitePresentation_restrict_target · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isFlat_restrict_source · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isFlat_restrict_target

Section79.9 Properties of groups over fields and groupoids on fields#

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

Tag 06DX, a situation

Tag 06DX in the Stacks Project.

AlgebraicGeometry.Space.GroupAlgebraicSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupActions.lean, line 101. The attribute's comment: “the situation: this notion at the base Spec k for a field k over S”.

Stacks Project, Tag 043H. Group algebraic spaces over an algebraic space B. An object is a group object in presheaves over B whose underlying presheaf is an algebraic space; morphisms are group-object morphisms over B.

noncomputable abbrev GroupAlgebraicSpace (𝒞 : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : 𝒞.Contains S) (B : (BigFppfOver 𝒞 S hS)ᵒᵖ ⥤ Type u)
    (_hB : IsAlgebraicSpace 𝒞 S hS B)
Tag 06DY, a situation

Tag 06DY in the Stacks Project.

AlgebraicGeometry.GroupoidOverField, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupoidOverField.lean, line 53. The attribute's comment: “groupoid in algebraic spaces over a field”.

Stacks 06DY. A groupoid in algebraic spaces over an algebraic space B over a scheme S, whose space of objects is the spectrum of a field k regarded as an algebraic space over S through Yoneda.

structure GroupoidOverField (C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
    (B : AlgebraicSpaces C S hS)
Tag 06DZ, an equation

Tag 06DZ in the Stacks Project.

AlgebraicGeometry.Space.actionGroupoid, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/ActionGroupoidModules.lean, line 84. The attribute's comment: “the groupoid (Spec k, G, p, p, m) of a group over a field, at the trivial”.

The action groupoid (X, G ×_B X, pr₁, a, m) of an action A of a group algebraic space G over B on an algebraic space X over B, with the projection as its source and the action morphism as its target.

noncomputable abbrev actionGroupoid (G : GroupAlgebraicSpace 𝒞 S hS B hB) (X : Over B)
    (hX : IsAlgebraicSpace 𝒞 S hS X.left) (A : ModObj G.obj.X X) :
    GroupoidInAlgebraicSpaces 𝒞 S hS ⟨B, hB⟩
Tag 06E0, a lemma

Tag 06E0 in the Stacks Project.

AlgebraicGeometry.Space.isFlat_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/FlatMultiplication.lean, line 217. The attribute's comment: “second assertion: the group law of a group space over a field”. References: SGA 3 XVIII (2.2), “special case”.

Stacks 06E0, second assertion. For a field k over the scheme S, the multiplication of a group algebraic space over Spec k is flat and universally open.

The first assertion of the same tag, for the composition of a groupoid in algebraic spaces whose object space is the spectrum of a field, is AlgebraicGeometry.GroupoidInAlgebraicSpaces.isFlat_comp_of_objects_eq_spec_field.

theorem isFlat_mul {k : Type u} [Field k] (C : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : C.Contains S) (structureMap : Spec (.of k) ⟶ S) (hk : C.Contains (Spec (.of k)))
    (G : GroupAlgebraicSpace C S hS
      (schemeSpace (Over.mk (⟨structureMap⟩ : C.obj hk ⟶ C.obj hS))).obj
      (schemeSpace (Over.mk (⟨structureMap⟩ : C.obj hk ⟶ C.obj hS))).property) :
    IsFlat C S hS μ[G.obj.X].left ∧ UniversallyOpen C S hS μ[G.obj.X].left

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isFlat_comp_of_objects_eq_spec_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FlatComposition.lean, line 183. The attribute's comment: “first assertion: the composition of a groupoid over a field”.

Stacks 06E0, first assertion. Composition in a groupoid in algebraic spaces whose object space is the spectrum of a field is flat and universally open.

theorem isFlat_comp_of_objects_eq_spec_field {k : Type u} [Field k]
    (C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
    (structureMap : Spec (.of k) ⟶ S) (hk : C.Contains (Spec (.of k)))
    (B : AlgebraicSpaces C S hS) (G : GroupoidInAlgebraicSpaces C S hS B)
    (objects_eq : G.objects =
      schemeSpace (Over.mk (⟨structureMap⟩ : C.obj hk ⟶ C.obj hS))) :
    Space.IsFlat C S hS G.comp.hom ∧ Space.UniversallyOpen C S hS G.comp.hom
Tag 08BH, a lemma

Tag 08BH in the Stacks Project.

AlgebraicGeometry.Space.isAbsolutelySeparated_groupAlgebraicSpace_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/DecentSeparated.lean, line 348. The attribute's comment: “a decent group algebraic space over a field”.

Stacks 08BH. A decent group algebraic space over the spectrum of a field is a separated algebraic space.

By Stacks 06P6 separatedness of the structure morphism is the identity section being a closed immersion, and the identity section is a section of the structure morphism, hence a closed immersion because the space is decent. The base is separated because the spectrum of a field is affine, so Stacks 04ZH part (1) upgrades separatedness of the structure morphism to separatedness of the group space.

theorem isAbsolutelySeparated_groupAlgebraicSpace_of_isDecentSpace (k : Type u) [Field k]
    (C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
    (structureMap : Spec (.of k) ⟶ S) (hk : C.Contains (Spec (.of k)))
    (hZ : C.Contains (⊤_ Scheme.{u}))
    (G : GroupAlgebraicSpace C S hS
      (yoneda.obj (Over.mk (⟨structureMap⟩ : C.obj hk ⟶ C.obj hS)))
      (isAlgebraicSpace_yoneda C S hS
        (Over.mk (⟨structureMap⟩ : C.obj hk ⟶ C.obj hS))))
    (hG : IsDecentSpace C S hS G.obj.X.left) :
    IsAbsolutelySeparated C S hS hZ G.obj.X.left

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isAbsolutelySeparated_arrows_of_isDecentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/DecentSeparated.lean, line 514. The attribute's comment: “the arrows of a decent groupoid on a field”.

Stacks 08BH. The arrow space of a groupoid in algebraic spaces whose object space is the algebraic space of the spectrum of a field and whose arrow space is decent is a separated algebraic space.

The unit of the groupoid is a section of the source morphism, hence a closed immersion because the arrow space is decent; the target morphism is then separated, and the object space is separated because the spectrum of a field is affine, so Stacks 04ZH part (1) applies.

theorem isAbsolutelySeparated_arrows_of_isDecentSpace (k : Type u) [Field k]
    (C : BigFppfSite.{u}) (S : Scheme.{u}) (hS : C.Contains S)
    (structureMap : Spec (.of k) ⟶ S) (hk : C.Contains (Spec (.of k)))
    (hZ : C.Contains (⊤_ Scheme.{u})) (B : AlgebraicSpaces C S hS)
    (G : GroupoidInAlgebraicSpaces C S hS B)
    (hU : G.objects.obj =
      yoneda.obj (Over.mk (⟨structureMap⟩ : C.obj hk ⟶ C.obj hS)))
    (hR : Space.IsDecentSpace C S hS G.arrows.obj) :
    Space.IsAbsolutelySeparated C S hS hZ G.arrows.obj
Tag 06E1, a lemma

Tag 06E1 in the Stacks Project.

AlgebraicGeometry.Space.isSurjective_of_restrictionDiagramMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionFieldExtension.lean, line 531. The attribute's comment: “surjective”.

Stacks 06E1. Every arrow of the diagram defining the restriction of a groupoid in algebraic spaces whose object space is the spectrum of a field, over a field extension, is surjective.

theorem isSurjective_of_restrictionDiagramMap
    {X Y : AlgebraicSpaces C S hS} (f : X ⟶ Y)
    (hf : RestrictionDiagramMap C hS hk hk' structureMap i G hU f) :
    IsSurjective C S hS f.hom

AlgebraicGeometry.Space.isFlat_of_restrictionDiagramMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionFieldExtension.lean, line 545. The attribute's comment: “flat”.

Stacks 06E1. Every arrow of the diagram defining the restriction of a groupoid in algebraic spaces whose object space is the spectrum of a field, over a field extension, is flat.

theorem isFlat_of_restrictionDiagramMap
    {X Y : AlgebraicSpaces C S hS} (f : X ⟶ Y)
    (hf : RestrictionDiagramMap C hS hk hk' structureMap i G hU f) :
    IsFlat C S hS f.hom

AlgebraicGeometry.Space.universallyOpen_of_restrictionDiagramMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionFieldExtension.lean, line 561. The attribute's comment: “universally open”.

Stacks 06E1. Every arrow of the diagram defining the restriction of a groupoid in algebraic spaces whose object space is the spectrum of a field, over a field extension, is universally open.

theorem universallyOpen_of_restrictionDiagramMap
    {X Y : AlgebraicSpaces C S hS} (f : X ⟶ Y)
    (hf : RestrictionDiagramMap C hS hk hk' structureMap i G hU f) :
    UniversallyOpen C S hS f.hom

AlgebraicGeometry.Space.isAffineHom_restrictionArrowsToArrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/Quotient/RestrictionFieldExtension.lean, line 577. The attribute's comment: “affine dotted arrow”.

Stacks 06E1. The canonical map from the arrows of the restriction of a groupoid in algebraic spaces over a field extension to the arrows of the groupoid is affine.

theorem isAffineHom_restrictionArrowsToArrows :
    IsAffineHom C S hS
      (restrictionArrowsToArrows G
        (restrictionObjectMap C hS hk hk' structureMap i G hU)).hom
Tag 06E2, a lemma

Tag 06E2 in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.exists_isIso_source_target_over_isAlgClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/GeometricArrows.lean, line 337.

Stacks 06E2. Let (U, R, s, t, c) be a groupoid in algebraic spaces over B whose object space U is the algebraic space represented by the spectrum of a field k. Every point r of the arrow space R has, after an algebraically closed field extension k'/k, a representative r' in the arrow space of the restriction (U', R', s', t', c') of the groupoid along Spec k' ⟶ Spec k: it maps to r in the points of R, and both its source s' ∘ r' and its target t' ∘ r' are automorphisms of Spec k'.

theorem exists_isIso_source_target_over_isAlgClosed {k : Type u} [Field k]
    (C : BigFppfSite.{u}) {S : Scheme.{u}} (hS : C.Contains S)
    (structureMap : Spec (CommRingCat.of k) ⟶ S)
    (hk : C.Contains (Spec (CommRingCat.of k))) (B : AlgebraicSpaces C S hS)
    (G : GroupoidInAlgebraicSpaces C S hS B)
    (objects_eq : G.objects = schemeSpace
      (Over.mk (⟨structureMap⟩ : C.obj hk ⟶ C.obj hS)))
    (r : Space.points C S hS G.arrows.obj) :
    ∃ (k' : Type u) (field' : Field k') (_ : IsAlgClosed k')
      (i : k →+* k') (hk' : C.Contains (Spec (CommRingCat.of k'))),
      let T : BigFppfOver C S hS :=
        Over.mk (⟨structureMap⟩ : C.obj hk ⟶ C.obj hS)
      let T' : BigFppfOver C S hS :=
        Over.mk (⟨Scheme.Spec.map (CommRingCat.ofHom i).op ≫ structureMap⟩ :
          C.obj hk' ⟶ C.obj hS)
      let g : schemeSpace T' ⟶ G.objects :=
        schemeSpaceMap
          (Over.homMk (⟨Scheme.Spec.map (CommRingCat.ofHom i).op⟩ :
            C.obj hk' ⟶ C.obj hk) rfl : T' ⟶ T) ≫
          eqToHom objects_eq.symm
      ∃ r' : (restrictionArrows G g).obj.obj (Opposite.op T'),
        let p : Space.FieldValuedPoint C S hS G.arrows.obj :=
          { carrier := k'
            field := field'
            contained := hk'
            toBase := Scheme.Spec.map (CommRingCat.ofHom i).op ≫ structureMap
            value := (restrictionArrowsToArrows G g).hom.app (Opposite.op T') r' }
        let sourceEnd : T' ⟶ T' := (restrictionSource G g).hom.app (Opposite.op T') r'
        let targetEnd : T' ⟶ T' := (restrictionTarget G g).hom.app (Opposite.op T') r'
        p.class C S hS G.arrows.obj = r ∧ IsIso sourceEnd ∧ IsIso targetEnd
Tag 06E3, a lemma

Tag 06E3 in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.translationByArrow_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Translation.lean, line 256. The attribute's comment: “the automorphism”.

Stacks 06E3. Translation by a family of arrows whose source and target are both isomorphisms of the object space is an automorphism of the arrow space.

theorem translationByArrow_isIso (G : GroupoidInAlgebraicSpaces C S hS B)
    (r : G.objects ⟶ G.arrows) [IsIso (r ≫ G.source)] [IsIso (r ≫ G.target)] :
    IsIso (translationByArrow G r)

AlgebraicGeometry.GroupoidInAlgebraicSpaces.translationByArrow_identity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Translation.lean, line 288. The attribute's comment: “image of the identity”.

Stacks 06E3. Translation by r takes the identity arrow at the source of r to r itself.

theorem translationByArrow_identity (G : GroupoidInAlgebraicSpaces C S hS B)
    (r : G.objects ⟶ G.arrows) [IsIso (r ≫ G.source)]
    (T : (BigFppfOver C S hS)ᵒᵖ) (x : G.toGroupoidInFunctors.Evaluation T) :
    (translationByArrow G r).hom.app T
      (G.toGroupoidInFunctors.identity T ((r ≫ G.source).hom.app T x)) = r.hom.app T x

AlgebraicGeometry.GroupoidInAlgebraicSpaces.identityArrow_comp_translationByArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/UnibranchIdentityArrow.lean, line 117. The attribute's comment: “image of the identity, as an equation of morphisms”.

Stacks 06E3, as an equation of morphisms. Left translation by a family r of arrows whose source is an isomorphism, precomposed with the identity arrow at the source of r, is r itself.

theorem identityArrow_comp_translationByArrow (H : GroupoidInAlgebraicSpaces C S hS B)
    (r : H.objects ⟶ H.arrows) [IsIso (r ≫ H.source)] :
    ((r ≫ H.source) ≫ identityArrow H) ≫ translationByArrow H r = r
Tag 06E4, a lemma

Tag 06E4 in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.isGeometricallyUnibranch_arrows_of_splitAtIds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GroupoidArrowsUnibranch.lean, line 103. The attribute's comment: “groupoid case, for a groupoid whose object space is the spectrum of a field”.

Stacks 06E4, the groupoid case. The arrow space of a groupoid in algebraic spaces whose object space is the spectrum of a field is geometrically unibranch.

The last step of the source proof is [Stacks Project, Tag 06DU] for the étale local rings 𝒪_{R, e} and 𝒪_{R ×_{s, U, t} R, (e, e)} of each restriction of the groupoid along an algebraically closed extension of the field; it is AlgebraicGeometry.GroupoidInAlgebraicSpaces.minimalPrimesSplitAtIdentityArrow_restriction.

theorem isGeometricallyUnibranch_arrows_of_splitAtIds :
    Space.IsGeometricallyUnibranch C S hS G.arrows.obj

AlgebraicGeometry.GroupoidOverField.isGeometricallyUnibranch_arrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GroupoidArrowsUnibranch.lean, line 129. The attribute's comment: “groupoid case, in the situation 06DY”.

Stacks 06E4, the groupoid case. In the situation of [Stacks Project, Tag 06DY] — a groupoid in algebraic spaces (U, R, s, t, c) whose object space U is the spectrum of a field k — the arrow space R is geometrically unibranch.

theorem isGeometricallyUnibranch_arrows (G : GroupoidOverField C S hS B) :
    Space.IsGeometricallyUnibranch C S hS G.arrows.obj

AlgebraicGeometry.Space.isGeometricallyUnibranch_groupAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GroupoidArrowsUnibranch.lean, line 199. The attribute's comment: “group case, in the situation 06DX”.

Stacks 06E4, the group case. A group algebraic space over a field is geometrically unibranch.

A group G over Spec k is the arrow space of a groupoid in algebraic spaces whose object space is Spec k: the group acts trivially on the base, and the arrow space of the resulting action groupoid is G ×_{Spec k} Spec k, which the first projection identifies with G.

theorem isGeometricallyUnibranch_groupAlgebraicSpace :
    IsGeometricallyUnibranch C (Spec (.of k)) hk G.obj.X.left
Tag 06FD, a lemma

Tag 06FD in the Stacks Project.

AlgebraicGeometry.Space.dimension_eq_dimensionAtPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/ConstantDimensionOverField.lean, line 355. The attribute's comment: “constant dimension of the arrow space”.

Stacks 06FD. Let G be a groupoid in algebraic spaces over S whose space of objects is the spectrum of a field k, viewed as an algebraic space through Yoneda, and whose source and target are locally of finite type. Then the dimension of the space of arrows of G equals its dimension at every one of its points.

theorem dimension_eq_dimensionAtPoint
    {k : Type u} [Field k] (hk : B.Contains (Spec (.of k)))
    (structureMap : Spec (.of k) ⟶ S)
    {A : AlgebraicSpaces B S hS} (G : GroupoidInAlgebraicSpaces B S hS A)
    (objects_eq : G.objects = _root_.AlgebraicGeometry.schemeSpace
      (Over.mk (⟨structureMap⟩ : B.obj hk ⟶ B.obj hS)))
    (_hs : IsLocallyOfFiniteType B S hS G.source.hom)
    (ht : IsLocallyOfFiniteType B S hS G.target.hom)
    (r : points B S hS G.arrows.obj) :
    dimension B S hS G.arrows.obj G.arrows.property =
      dimensionAtPoint B S hS G.arrows.obj G.arrows.property r

AlgebraicGeometry.Space.hasTranscendenceDegreeAt_source_iff_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/ConstantDimensionOverField.lean, line 444. The attribute's comment: “part (2): the transcendence degree through the source and through the target”.

Stacks 06FD, part (2). Let G be a groupoid in algebraic spaces over S whose space of objects is the spectrum of a field k, viewed as an algebraic space through Yoneda, and whose source and target are locally of finite type. Then the transcendence degree over k of a point of the space of arrows is the same whether it is measured through the source or through the target.

Both are read on one étale chart of the arrow space whose chart of the object space is the field spectrum itself, where they become the two transcendence degrees of the residue field at a point of a scheme over two morphisms to the spectrum of a field.

theorem hasTranscendenceDegreeAt_source_iff_target
    {k : Type u} [Field k] (hk : B.Contains (Spec (.of k)))
    (structureMap : Spec (.of k) ⟶ S)
    {A : AlgebraicSpaces B S hS} (G : GroupoidInAlgebraicSpaces B S hS A)
    (objects_eq : G.objects = _root_.AlgebraicGeometry.schemeSpace
      (Over.mk (⟨structureMap⟩ : B.obj hk ⟶ B.obj hS)))
    (hs : IsLocallyOfFiniteType B S hS G.source.hom)
    (ht : IsLocallyOfFiniteType B S hS G.target.hom)
    (r : points B S hS G.arrows.obj) (n : ℕ∞) :
    HasTranscendenceDegreeAt B S hS G.source.hom r n ↔
      HasTranscendenceDegreeAt B S hS G.target.hom r n

AlgebraicGeometry.Space.dimension_eq_localRingDimension_of_hasTranscendenceDegreeAt_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/ConstantDimensionOverField.lean, line 535. The attribute's comment: “part (3): the dimension of the local ring at a point of transcendence degree 0”.

Stacks 06FD, part (3). Let G be a groupoid in algebraic spaces over S whose space of objects is the spectrum of a field k, viewed as an algebraic space through Yoneda, and whose source and target are locally of finite type. At a point of the space of arrows whose transcendence degree over k is zero, the dimension of the space of arrows is the dimension of the local ring there.

theorem dimension_eq_localRingDimension_of_hasTranscendenceDegreeAt_zero
    {k : Type u} [Field k] (hk : B.Contains (Spec (.of k)))
    (structureMap : Spec (.of k) ⟶ S)
    {A : AlgebraicSpaces B S hS} (G : GroupoidInAlgebraicSpaces B S hS A)
    (objects_eq : G.objects = _root_.AlgebraicGeometry.schemeSpace
      (Over.mk (⟨structureMap⟩ : B.obj hk ⟶ B.obj hS)))
    (hs : IsLocallyOfFiniteType B S hS G.source.hom)
    (ht : IsLocallyOfFiniteType B S hS G.target.hom)
    (r : points B S hS G.arrows.obj)
    (htr : HasTranscendenceDegreeAt B S hS G.source.hom r 0) :
    dimension B S hS G.arrows.obj G.arrows.property =
      (localRingDimension B S hS r : WithBot ℕ∞)
Tag 06FE, a lemma

Tag 06FE in the Stacks Project.

AlgebraicGeometry.Space.dimension_eq_dimensionAtPoint_of_groupAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ConstantDimension.lean, line 163. The attribute's comment: “part (1): dimension at every point”.

Stacks 06FE, part (1). A group algebraic space over a field which is locally of finite type has the same dimension at every one of its points, namely its dimension.

Constant dimension of the arrow space of a groupoid in algebraic spaces whose object space is the spectrum of a field is AlgebraicGeometry.Space.dimension_eq_dimensionAtPoint.

theorem dimension_eq_dimensionAtPoint_of_groupAlgebraicSpace {k : Type u} [Field k]
    (C : BigFppfSite.{u}) (hk : C.Contains (Spec (.of k)))
    (G : GroupAlgebraicSpace C (Spec (.of k)) hk (terminalSpace C (Spec (.of k)) hk).obj
      (terminalSpace C (Spec (.of k)) hk).property)
    (hG : IsLocallyOfFiniteType C (Spec (.of k)) hk G.obj.X.hom)
    (g : points C (Spec (.of k)) hk G.obj.X.left) :
    dimension C (Spec (.of k)) hk G.obj.X.left G.property =
      dimensionAtPoint C (Spec (.of k)) hk G.obj.X.left G.property g

AlgebraicGeometry.Space.dimension_eq_localRingDimension_of_groupAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ConstantDimension.lean, line 214. The attribute's comment: “part (2): dimension of the local ring at a point of transcendence degree zero”.

Stacks 06FE, part (2). At a point of a group algebraic space locally of finite type over a field whose transcendence degree over that field is zero, the dimension of the group is the dimension of the local ring.

theorem dimension_eq_localRingDimension_of_groupAlgebraicSpace {k : Type u} [Field k]
    (C : BigFppfSite.{u}) (hk : C.Contains (Spec (.of k)))
    (G : GroupAlgebraicSpace C (Spec (.of k)) hk (terminalSpace C (Spec (.of k)) hk).obj
      (terminalSpace C (Spec (.of k)) hk).property)
    (hG : IsLocallyOfFiniteType C (Spec (.of k)) hk G.obj.X.hom)
    (g : points C (Spec (.of k)) hk G.obj.X.left)
    (htr : HasTranscendenceDegreeAt C (Spec (.of k)) hk G.obj.X.hom g 0) :
    dimension C (Spec (.of k)) hk G.obj.X.left G.property =
      (localRingDimension C (Spec (.of k)) hk g : WithBot ℕ∞)
Tag 06FF, a lemma

Tag 06FF in the Stacks Project.

AlgebraicGeometry.Space.dimension_arrows_eq_dimension_stabilizer_of_objects_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/StabilizerDimensionObjectsIso.lean, line 57. The attribute's comment: “with the space of objects isomorphic to the spectrum of the field”.

Stacks 06FF. Let G be a groupoid in algebraic spaces over S whose space of objects is the spectrum of a field k, viewed as an algebraic space through Yoneda, and whose source and target are locally of finite type. Then the space of arrows of G and the stabilizer of G have the same dimension.

The hypothesis is an isomorphism of the object space with the spectrum of the field, not an equality of algebraic spaces; the equality case is AlgebraicGeometry.Space.dimension_arrows_eq_dimension_stabilizer.

theorem dimension_arrows_eq_dimension_stabilizer_of_objects_iso {k : Type u} [Field k]
    (hk : B.Contains (Spec (.of k))) (structureMap : Spec (.of k) ⟶ S)
    {A : AlgebraicSpaces B S hS} (G : GroupoidInAlgebraicSpaces B S hS A)
    (objects_iso : G.objects ≅ _root_.AlgebraicGeometry.schemeSpace
      (Over.mk (⟨structureMap⟩ : B.obj hk ⟶ B.obj hS)))
    (hs : IsLocallyOfFiniteType B S hS G.source.hom)
    (ht : IsLocallyOfFiniteType B S hS G.target.hom) :
    dimension B S hS G.arrows.obj G.arrows.property =
      dimension B S hS (GroupoidInAlgebraicSpaces.stabilizerOverBase G).obj
        (GroupoidInAlgebraicSpaces.stabilizerOverBase G).property

AlgebraicGeometry.Space.dimension_arrows_eq_dimension_stabilizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/StabilizerDimensionOverField.lean, line 666.

Let G be a groupoid in algebraic spaces over S whose space of objects is the spectrum of a field k, viewed as an algebraic space through Yoneda, and whose source and target are locally of finite type. Then the space of arrows of G and the stabilizer of G have the same dimension.

theorem dimension_arrows_eq_dimension_stabilizer {k : Type u} [Field k]
    (hk : B.Contains (Spec (.of k))) (structureMap : Spec (.of k) ⟶ S)
    {A : AlgebraicSpaces B S hS} (G : GroupoidInAlgebraicSpaces B S hS A)
    (objects_eq : G.objects = _root_.AlgebraicGeometry.schemeSpace
      (Over.mk (⟨structureMap⟩ : B.obj hk ⟶ B.obj hS)))
    (hs : IsLocallyOfFiniteType B S hS G.source.hom)
    (ht : IsLocallyOfFiniteType B S hS G.target.hom) :
    dimension B S hS G.arrows.obj G.arrows.property =
      dimension B S hS (GroupoidInAlgebraicSpaces.stabilizerOverBase G).obj
        (GroupoidInAlgebraicSpaces.stabilizerOverBase G).property
Sources
LeanAlgebraicGeometry.Space.GroupAlgebraicSpace · AlgebraicGeometry.GroupoidOverField · AlgebraicGeometry.Space.actionGroupoid · AlgebraicGeometry.Space.isFlat_mul · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isFlat_comp_of_objects_eq_spec_field · AlgebraicGeometry.Space.isAbsolutelySeparated_groupAlgebraicSpace_of_isDecentSpace · AlgebraicGeometry.GroupoidInAlgebraicSpaces.isAbsolutelySeparated_arrows_of_isDecentSpace · AlgebraicGeometry.Space.isSurjective_of_restrictionDiagramMap

Section79.10 Group algebraic spaces over fields#

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

Tag 0B8E, a lemma

Tag 0B8E in the Stacks Project.

AlgebraicGeometry.Space.GroupOverField.isRepresentable_relocalizeRestrict_algebraicClosure_of_isSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpacesOverFields/AlgebraicClosureScheme.lean, line 662.

Let k be a field with algebraic closure k̄ and let G be a separated group algebraic space over k. Then G_{k̄} is a scheme.

By AlgebraicGeometry.Space.GroupOverField.exists_isAlgClosed_isRepresentable_relocalizeRestrict the base change G_L is a scheme for some algebraically closed extension L/k; this is the source's argument with translations of the group and Jacobson charts. A separated algebraic space over the affine Spec k is quasi-separated, so Stacks 0B84 part (1) descends this to k̄.

theorem isRepresentable_relocalizeRestrict_algebraicClosure_of_isSeparatedOver
    (B : BigFppfSite.{u}) (hk : B.Contains (Spec (.of k)))
    (G : GroupAlgebraicSpace B (Spec (.of k)) hk (yoneda.obj (⊤_ (BigFppfOver B (Spec (.of k)) hk)))
      (isAlgebraicSpace_yoneda B (Spec (.of k)) hk _))
    (hsep : IsSeparatedOver B (Spec (.of k)) hk G.obj.X.left) :
    ((OverShriek.relocalizeRestrict (specExtensionHom k (AlgebraicClosure k) B hk
      (contains_spec_of_isAlgebraic B k (AlgebraicClosure k) hk))).obj
        G.obj.X.left).IsRepresentable
Tag 0B8F, a lemma

Tag 0B8F in the Stacks Project.

AlgebraicGeometry.Space.GroupOverField.isRepresentable_of_isSeparatedOver_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpacesOverFields/SeparatedFiniteTypeScheme.lean, line 50.

A separated group algebraic space locally of finite type over a field is a scheme. Let G be a group algebraic space over S ≅ Spec k which is separated over k and locally of finite type over k. Then G is representable.

Being separated over k, the space G is locally separated over k, hence decent, and a decent group algebraic space locally of finite type over a field is a scheme.

theorem isRepresentable_of_isSeparatedOver_of_isLocallyOfFiniteType (e : S ≅ Spec (.of k))
    (G : GroupAlgebraicSpace C S hS (yoneda.obj (⊤_ (BigFppfOver C S hS)))
      (isAlgebraicSpace_yoneda C S hS _))
    (hsep : IsSeparatedOver C S hS G.obj.X.left)
    (hlft : IsLocallyOfFiniteType C S hS
      ((isTerminal_yoneda_obj_base C S hS).from G.obj.X.left)) :
    G.obj.X.left.IsRepresentable
Tag 0B8G, a proposition

Tag 0B8G in the Stacks Project.

AlgebraicGeometry.Space.GroupOverField.isRepresentable_of_isSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpacesOverFields/SeparatedScheme.lean, line 253.

Stacks 0B8G. Let k be a field and let G be a group algebraic space over k. If G is separated, then G is a scheme.

By Stacks 0B8E the base change G_{k̄} is a scheme X₀. For a purely transcendental extension K = k(x_σ) of cardinality above the size of X₀, Stacks 0B85 reduces the statement to G_K. With Ω the algebraic closure of K, the base change G_Ω = X₀ ×_{k̄} Ω is a Jacobson scheme whose closed points are Ω-rational (Stacks 0479), and AlgebraicGeometry.Space.GroupOverField.isRepresentable_of_relocalizeRestrict_algebraicClosure concludes that G_K is a scheme.

theorem isRepresentable_of_isSeparatedOver {k : Type u} [Field k] (B : BigFppfSite.{u})
    (hk : B.Contains (Spec (.of k)))
    (G : GroupAlgebraicSpace B (Spec (.of k)) hk (yoneda.obj (⊤_ (BigFppfOver B (Spec (.of k)) hk)))
      (isAlgebraicSpace_yoneda B (Spec (.of k)) hk _))
    (hsep : IsSeparatedOver B (Spec (.of k)) hk G.obj.X.left) :
    G.obj.X.left.IsRepresentable
Sources
LeanAlgebraicGeometry.Space.GroupOverField.isRepresentable_relocalizeRestrict_algebraicClosure_of_isSeparatedOver · AlgebraicGeometry.Space.GroupOverField.isRepresentable_of_isSeparatedOver_of_isLocallyOfFiniteType · AlgebraicGeometry.Space.GroupOverField.isRepresentable_of_isSeparatedOver

Section79.11 No rational curves on groups#

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

Tag 0AEL, a lemma

Tag 0AEL in the Stacks Project.

AlgebraicGeometry.Space.exists_factorization_of_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FactorizationDenseOpen.lean, line 201.

Stacks 0AEL. Let f : X ⟶ Y and g : X ⟶ Z be morphisms of algebraic spaces over an algebraic space T with Y ⟶ T separated and g surjective, flat and locally of finite presentation. If there is a scheme-theoretically dense open subspace V ⊆ Z such that the restriction of f to g⁻¹(V) factors through V over T, then f factors through g over T.

theorem exists_factorization_of_dense_open
    {T X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hT : IsAlgebraicSpace B S hS T) (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z)
    (pX : X ⟶ T) (pY : Y ⟶ T) (pZ : Z ⟶ T) (f : X ⟶ Y) (g : X ⟶ Z)
    (hf : f ≫ pY = pX) (hg : g ≫ pZ = pX)
    (hsep : IsSeparated B S hS pY)
    (hsurj : IsSurjective B S hS g) (hflat : IsFlat B S hS g)
    (hlfp : IsLocallyOfFinitePresentation B S hS g)
    (V : Subfunctor Z) (hV : IsOpenSubspace B S hS V)
    (hdense : IsSchemeTheoreticallyDense B S hS V)
    (hfactor : ∃ v : V.toFunctor ⟶ Y,
      (v ≫ pY = V.ι ≫ pZ) ∧
      (pullback.fst g V.ι ≫ f = pullback.snd g V.ι ≫ v)) :
    ∃ h : Z ⟶ Y, (g ≫ h = f) ∧ (h ≫ pY = pZ)
Tag 0AEM, a lemma

Tag 0AEM in the Stacks Project.

AlgebraicGeometry.Space.exists_coordinateProjection_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ProjectiveLineFactorization.lean, line 176.

Stacks 0AEM. Let k be a field, let n be a positive integer, let Z be an algebraic space over Spec k separated and of finite type over Spec k and let w : (ℙ¹_k)^n ⟶ Z. Then w factors as the projection onto the coordinates in some subset I ⊆ Fin n followed by a finite morphism.

The contraction step is AlgebraicGeometry.Space.exists_coordinateProjection_finite_fibres, and a morphism out of a finite power of the projective line all of whose fibres on points are finite is finite by AlgebraicGeometry.Space.isFinite_of_finite_fibres.

theorem exists_coordinateProjection_isFinite (n : ℕ) (hn : 0 < n)
    (Z : (BigFppfOver B (Spec (CommRingCat.of k)) hk)ᵒᵖ ⥤ Type u)
    (hZ : IsAlgebraicSpace B (Spec (CommRingCat.of k)) hk Z)
    (z : Z ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hk)) : BigFppfOver B (Spec (CommRingCat.of k)) hk))
    (hsep : IsSeparated B (Spec (CommRingCat.of k)) hk z)
    (hft : IsFiniteType B (Spec (CommRingCat.of k)) hk z)
    (w : projectiveLinePower k B hk (Fin n) ⟶ Z) :
    ∃ (I : Finset (Fin n)) (g : projectiveLinePower k B hk I ⟶ Z),
      w = coordinateProjection k B hk n I ≫ g ∧
        IsFinite B (Spec (CommRingCat.of k)) hk g
Tag 0AEN, a lemma

Tag 0AEN in the Stacks Project.

AlgebraicGeometry.Space.morphism_projectiveLine_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/ProjectiveLineFactorization.lean, line 197.

Stacks 0AEN. Let k be a field and let G be a separated group algebraic space locally of finite type over k. Every morphism from the projective line over k to G over Spec k is constant: it factors through a section of the structure morphism of G.

This is AlgebraicGeometry.Space.morphism_projectiveLine_eq_constant with its hypothesis h0AEMfibres — the contraction step of [Stacks, Tag 0AEM] — supplied by AlgebraicGeometry.Space.exists_coordinateProjection_finite_fibres.

theorem morphism_projectiveLine_constant
    (G : GroupAlgebraicSpace B (Spec (CommRingCat.of k)) hk
      (yoneda.obj (Over.mk (𝟙 (B.obj hk))))
      (isAlgebraicSpace_yoneda B (Spec (CommRingCat.of k)) hk _))
    (hsep : IsSeparatedOver B (Spec (CommRingCat.of k)) hk G.obj.X.left)
    (hft : IsLocallyOfFiniteType B (Spec (CommRingCat.of k)) hk G.obj.X.hom)
    (f : projectiveLineOverBase k B hk ⟶ G.obj.X) :
    ∃ c : yoneda.obj (Over.mk (𝟙 (B.obj hk))) ⟶ G.obj.X.left,
      c ≫ G.obj.X.hom = 𝟙 _ ∧
        f.left = (projectiveLineOverBase k B hk).hom ≫ c
Sources
LeanAlgebraicGeometry.Space.exists_factorization_of_dense_open · AlgebraicGeometry.Space.exists_coordinateProjection_isFinite · AlgebraicGeometry.Space.morphism_projectiveLine_constant

Section79.12 The finite part of a morphism#

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

Tag 04PC, an equation

Tag 04PC in the Stacks Project.

AlgebraicGeometry.Space.FiniteOpenSubspace, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Basic.lean, line 55.

Stacks 04PC. For a morphism f : X ⟶ Y of algebraic spaces over S and an algebraic space T, a morphism T ⟶ Y together with an open subspace of T ×_Y X which is finite over T.

structure FiniteOpenSubspace (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (T : AlgebraicSpaces B S hS)
Tag 04PD, an equation

Tag 04PD in the Stacks Project.

AlgebraicGeometry.Space.finiteOpenSubspacePresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Presheaf.lean, line 101.

Stacks 04PD. The finite part (X/Y)_fin of a morphism f : X ⟶ Y of algebraic spaces over S: the presheaf whose sections over a scheme T are the pairs consisting of a morphism T ⟶ Y and an open subspace of T ×_Y X finite over T, with restriction given by base change.

noncomputable def finiteOpenSubspacePresheaf (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    FinitePartPresheaf B S hS f
Tag 04PE, a lemma

Tag 04PE in the Stacks Project.

AlgebraicGeometry.Space.isSheaf_finiteOpenSubspacePresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/FppfSheaf.lean, line 809. The attribute's comment: “part (1)”.

Stacks 04PE, part (1). For a morphism f : X ⟶ Y of algebraic spaces over a scheme S, the finite part (X/Y)_fin of f satisfies the sheaf condition for the fppf topology of the big fppf site of S.

public theorem isSheaf_finiteOpenSubspacePresheaf
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    Presheaf.IsSheaf (BigFppfOver.topology B S hS)
      (finiteOpenSubspacePresheaf B S hS f).toFunctor

AlgebraicGeometry.Space.finiteOpenSubspaceEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/FppfSheaf.lean, line 1023. The attribute's comment: “part (2)”.

Stacks 04PE, part (2). For an algebraic space T over S, the morphisms of sheaves from T to the finite part (X/Y)_fin of f : X ⟶ Y are in canonical bijection with the pairs (a, Z) of Stacks 04PC over T: the pair attached to a morphism restricts, along every morphism from a scheme of the site, to the pair that the morphism names there.

public noncomputable def finiteOpenSubspaceEquiv
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (T : AlgebraicSpaces B S hS) :
    { e : (T.obj ⟶ (finiteOpenSubspacePresheaf B S hS f).toFunctor) ≃
        FiniteOpenSubspace B S hS f T //
      ∀ (v : T.obj ⟶ (finiteOpenSubspacePresheaf B S hS f).toFunctor)
        (U : BigFppfOver B S hS)
        (g : yoneda.obj U ⟶ T.obj),
        let p := e v
        let q := (finiteOpenSubspacePresheaf B S hS f).sections U
          (v.app (op U) (yonedaEquiv g))
        (q.toBase.hom = g ≫ p.toBase.hom) ∧
          ∃ j : q.subspace.toFunctor ⟶ p.subspace.toFunctor,
            (IsPullback
              (q.subspace.ι ≫ pullback.fst q.toBase.hom f.hom)
              j g
              (p.subspace.ι ≫ pullback.fst p.toBase.hom f.hom)) ∧
            (j ≫ p.subspace.ι ≫ pullback.snd p.toBase.hom f.hom =
              q.subspace.ι ≫ pullback.snd q.toBase.hom f.hom) }
Tag 04PF, a lemma

Tag 04PF in the Stacks Project.

AlgebraicGeometry.Space.finiteOpenSubspaceMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/OpenImmersionMap.lean, line 409.

The canonical injective map (X'/Y)₍fin₎ ⟶ (X/Y)₍fin₎ induced by an open immersion X' ⟶ X over Y. Its specification identifies each image finite open pair over a test scheme.

public noncomputable def finiteOpenSubspaceMap
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X' X Y : AlgebraicGeometry.AlgebraicSpaces B S hS}
    (j : X' ⟶ X) (f' : X' ⟶ Y) (f : X ⟶ Y)
    (hj : j ≫ f = f') (hjOpen : AlgebraicGeometry.Space.IsOpenImmersion B S hS j.hom) :
    { m : (AlgebraicGeometry.Space.finiteOpenSubspacePresheaf B S hS f').toFunctor ⟶
        (AlgebraicGeometry.Space.finiteOpenSubspacePresheaf B S hS f).toFunctor //
      Mono m ∧
        ∀ (T : AlgebraicGeometry.BigFppfOver B S hS)
          (s : (AlgebraicGeometry.Space.finiteOpenSubspacePresheaf B S hS f').toFunctor.obj (op T)),
          let p := (AlgebraicGeometry.Space.finiteOpenSubspacePresheaf B S hS f').sections T s
          let q := (AlgebraicGeometry.Space.finiteOpenSubspacePresheaf B S hS f).sections T
            (m.app (op T) s)
          (p.toBase = q.toBase) ∧
            ∃ k : p.subspace.toFunctor ⟶ q.subspace.toFunctor,
              IsIso k ∧
                (k ≫ q.subspace.ι ≫ pullback.fst q.toBase.hom f.hom =
                  p.subspace.ι ≫ pullback.fst p.toBase.hom f'.hom) ∧
                (k ≫ q.subspace.ι ≫ pullback.snd q.toBase.hom f.hom =
                  p.subspace.ι ≫ pullback.snd p.toBase.hom f'.hom ≫ j.hom) }
Tag 04PG, a lemma

Tag 04PG in the Stacks Project.

AlgebraicGeometry.Space.isIso_finiteOpenSubspaceMap_locallyQuasiFinitePart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/LocallyQuasiFinitePart.lean, line 336.

Stacks 04PG. Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S which is locally of finite type and let X' ⊆ X be the maximal open subspace over which f is locally quasi-finite, Stacks 04NW. Then (X/Y)_fin = (X'/Y)_fin, in the sense that the canonical injection (X'/Y)_fin ⟶ (X/Y)_fin of Stacks 04PF is an isomorphism.

theorem isIso_finiteOpenSubspaceMap_locallyQuasiFinitePart {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f.hom) :
    IsIso (finiteOpenSubspaceMap B S hS (locallyQuasiFinitePartInclusion B S hS f hf)
      (locallyQuasiFinitePartInclusion B S hS f hf ≫ f) f rfl
      (isOpenImmersion_locallyQuasiFinitePartInclusion B S hS f hf)).1
Tag 04PH, a lemma

Tag 04PH in the Stacks Project.

AlgebraicGeometry.Space.FiniteOpenSubspace.isClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/SeparatedClosed.lean, line 66.

Stacks 04PH. An open subspace of T ×_Y X which is finite over T is a closed subspace of T ×_Y X, provided f : X ⟶ Y is separated.

theorem FiniteOpenSubspace.isClosedSubspace (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (T : AlgebraicSpaces B S hS) (Z : FiniteOpenSubspace B S hS f T)
    (hf : IsSeparated B S hS f.hom) :
    IsClosedSubspace B S hS Z.subspace
Tag 04PI, a remark

Tag 04PI in the Stacks Project.

AlgebraicGeometry.Space.FinitePartFibre.zeroFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 151. The attribute's comment: “zero_as_a_section_over_any_base”.

Stacks 04PI, the zero of the F₂-algebra. The section 0 = (a, ∅) cut out by no point at all, whose projection to T is finite because the empty open subspace is the coproduct of the empty family.

def zeroFibre (a : T ⟶ Y) : FinitePartFibre B S hS f a

AlgebraicGeometry.Space.FinitePartPresheaf.zeroSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 231. The attribute's comment: “zero_section_over_the_base”.

Stacks 04PI. The zero section 0 = (1_Y, ∅) of the F₂-algebra, as a section of the finite part over Y.

def zeroSection : Y.obj ⟶ P.toFunctor

AlgebraicGeometry.Space.FinitePartPresheaf.sections_zeroSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 237. The attribute's comment: “zero_section_is_the_empty_subspace”.

Stacks 04PI. On sections, the zero is the empty open subspace.

theorem sections_zeroSection (T : BigFppfOver B S hS) (y : Y.obj.obj (op T)) :
    P.sections T ((zeroSection P).app (op T) y) =
      (FinitePartFibre.zeroFibre
        (ObjectProperty.homMk (yonedaEquiv.symm y) : schemeSpace T ⟶ Y)).toPair

AlgebraicGeometry.Space.FinitePartPresheaf.zeroSection_comp_baseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 245. The attribute's comment: “zero_section_lies_over_the_base”.

Stacks 04PI. The zero is a section of the projection to Y.

theorem zeroSection_comp_baseMap : zeroSection P ≫ P.baseMap = 𝟙 Y.obj

AlgebraicGeometry.Space.FinitePartPresheaf.oneSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 251. The attribute's comment: “unit_section_over_the_base”.

Stacks 04PI, the finite case. The unit 1 = (1_Y, X) of the F₂-algebra, as a section of the finite part over Y.

def oneSection (hfin : IsFinite B S hS f.hom) : Y.obj ⟶ P.toFunctor

AlgebraicGeometry.Space.FinitePartPresheaf.sections_oneSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 257. The attribute's comment: “unit_section_is_the_whole_fibre_product”.

Stacks 04PI, the finite case. On sections, the unit is the whole fibre product.

theorem sections_oneSection (hfin : IsFinite B S hS f.hom) (T : BigFppfOver B S hS)
    (y : Y.obj.obj (op T)) :
    P.sections T ((oneSection P hfin).app (op T) y) =
      (FinitePartFibre.one (a := (ObjectProperty.homMk (yonedaEquiv.symm y) :
        schemeSpace T ⟶ Y)) hfin).toPair

AlgebraicGeometry.Space.FinitePartPresheaf.oneSection_comp_baseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 266. The attribute's comment: “unit_section_lies_over_the_base”.

Stacks 04PI, the finite case. The unit is a section of the projection to Y.

theorem oneSection_comp_baseMap (hfin : IsFinite B S hS f.hom) :
    oneSection P hfin ≫ P.baseMap = 𝟙 Y.obj

AlgebraicGeometry.Space.FinitePartFibre.nonUnitalCommRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 280. The attribute's comment: “f2_algebra_without_unit”.

Stacks 04PI. The sections of the finite part over T lying over a fixed a : T ⟶ Y form a commutative ring without unit: the multiplication is the intersection ⋆₂, the addition is the symmetric difference ⋆₁(⋆₃(s, s'), ⋆₄(s, s')) and the zero is (a, ∅).

noncomputable def nonUnitalCommRing (hf : IsSeparated B S hS f.hom) (a : T ⟶ Y) :
    NonUnitalCommRing (FinitePartFibre B S hS f a)

AlgebraicGeometry.Space.FinitePartFibre.zmodModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 323. The attribute's comment: “f2_algebra_scalars”.

Stacks 04PI. Every section is its own additive inverse, so the ring of sections over a fixed a : T ⟶ Y is an algebra over F₂.

noncomputable def zmodModule (hf : IsSeparated B S hS f.hom) (a : T ⟶ Y) :
    letI := nonUnitalCommRing hf a
    Module (ZMod 2) (FinitePartFibre B S hS f a)

AlgebraicGeometry.Space.FinitePartFibre.commRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 336. The attribute's comment: “f2_algebra_with_its_unit_in_the_finite_case”.

Stacks 04PI, the finite case. When f is finite the sections of the finite part over a fixed a : T ⟶ Y form a commutative ring, the unit being the section (a, T ×_Y X) and the remaining structure that of the F₂-algebra.

noncomputable def commRing (hf : IsSeparated B S hS f.hom) (hfin : IsFinite B S hS f.hom)
    (a : T ⟶ Y) : CommRing (FinitePartFibre B S hS f a)

AlgebraicGeometry.Space.FinitePartFibre.star₃_eq_mul_one_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 349. The attribute's comment: “star_3_is_s_times_one_plus_s_prime”.

Stacks 04PI, the finite case. ⋆₃(s, s') = s (1 + s').

theorem star₃_eq_mul_one_add (hf : IsSeparated B S hS f.hom) (hfin : IsFinite B S hS f.hom)
    {a : T ⟶ Y} (Z₁ Z₂ : FinitePartFibre B S hS f a) :
    letI := commRing hf hfin a
    star₃ hf Z₁ Z₂ = Z₁ * (1 + Z₂)

AlgebraicGeometry.Space.FinitePartFibre.star₄_eq_one_add_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/F2Algebra.lean, line 357. The attribute's comment: “star_4_is_one_plus_s_times_s_prime”.

Stacks 04PI, the finite case. ⋆₄(s, s') = (1 + s) s'.

theorem star₄_eq_one_add_mul (hf : IsSeparated B S hS f.hom) (hfin : IsFinite B S hS f.hom)
    {a : T ⟶ Y} (Z₁ Z₂ : FinitePartFibre B S hS f a) :
    letI := commRing hf hfin a
    star₄ hf Z₁ Z₂ = (1 + Z₁) * Z₂

AlgebraicGeometry.Space.FinitePartFibre.star₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 302. The attribute's comment: “star_2_on_sections”.

Stacks 04PI, the operation ⋆₂. The intersection (a, Z₁ ∩ Z₂) of two sections of the finite part lying over the same morphism to Y.

def star₂ : FinitePartFibre B S hS f a

AlgebraicGeometry.Space.FinitePartFibre.star₃, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 311. The attribute's comment: “star_3_on_sections”.

Stacks 04PI, the operation ⋆₃. The difference (a, Z₁ ∖ Z₂) of two sections of the finite part lying over the same morphism to Y.

def star₃ : FinitePartFibre B S hS f a

AlgebraicGeometry.Space.FinitePartFibre.star₄, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 320. The attribute's comment: “star_4_on_sections”.

Stacks 04PI, the operation ⋆₄. The difference (a, Z₂ ∖ Z₁) of two sections of the finite part lying over the same morphism to Y.

def star₄ : FinitePartFibre B S hS f a

AlgebraicGeometry.Space.FinitePartFibre.pointSet_star₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 329. The attribute's comment: “star_2_on_points”.

Stacks 04PI, the operation ⋆₂. On points, ⋆₂(s, s') is the intersection Z₁ ∩ Z₂.

theorem pointSet_star₂ : (star₂ hf Z₁ Z₂).pointSet = Z₁.pointSet ∩ Z₂.pointSet

AlgebraicGeometry.Space.FinitePartFibre.pointSet_star₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 335. The attribute's comment: “star_3_on_points”.

Stacks 04PI, the operation ⋆₃. On points, ⋆₃(s, s') is the difference Z₁ ∖ Z₂.

theorem pointSet_star₃ : (star₃ hf Z₁ Z₂).pointSet = Z₁.pointSet \ Z₂.pointSet

AlgebraicGeometry.Space.FinitePartFibre.pointSet_star₄, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 341. The attribute's comment: “star_4_on_points”.

Stacks 04PI, the operation ⋆₄. On points, ⋆₄(s, s') is the difference Z₂ ∖ Z₁.

theorem pointSet_star₄ : (star₄ hf Z₁ Z₂).pointSet = Z₂.pointSet \ Z₁.pointSet

AlgebraicGeometry.Space.FinitePartFibre.isOpenImmersion_star₂_le_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 354. The attribute's comment: “intersection_open_in_left”.

Stacks 04PI. Z₁ ∩ Z₂ is open inside Z₁.

theorem isOpenImmersion_star₂_le_left :
    IsOpenImmersion B S hS (Subfunctor.homOfLe (star₂_le_left hf Z₁ Z₂))

AlgebraicGeometry.Space.FinitePartFibre.isClosedImmersion_star₂_le_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 360. The attribute's comment: “intersection_closed_in_left”.

Stacks 04PI. Z₁ ∩ Z₂ is closed inside Z₁.

theorem isClosedImmersion_star₂_le_left :
    IsClosedImmersion B S hS (Subfunctor.homOfLe (star₂_le_left hf Z₁ Z₂))

AlgebraicGeometry.Space.FinitePartFibre.isOpenImmersion_star₂_le_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 366. The attribute's comment: “intersection_open_in_right”.

Stacks 04PI. Z₁ ∩ Z₂ is open inside Z₂.

theorem isOpenImmersion_star₂_le_right :
    IsOpenImmersion B S hS (Subfunctor.homOfLe (star₂_le_right hf Z₁ Z₂))

AlgebraicGeometry.Space.FinitePartFibre.isClosedImmersion_star₂_le_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 372. The attribute's comment: “intersection_closed_in_right”.

Stacks 04PI. Z₁ ∩ Z₂ is closed inside Z₂.

theorem isClosedImmersion_star₂_le_right :
    IsClosedImmersion B S hS (Subfunctor.homOfLe (star₂_le_right hf Z₁ Z₂))

AlgebraicGeometry.Space.FinitePartFibre.zero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 379. The attribute's comment: “zero_of_the_f2_algebra”.

Stacks 04PI. The zero section 0 = (a, ∅) of the F₂-algebra: the empty open subspace, which is finite over T.

def zero : FinitePartFibre B S hS f a

AlgebraicGeometry.Space.FinitePartFibre.subspace_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 393. The attribute's comment: “zero_is_the_empty_subspace”.

Stacks 04PI. The open subspace of the zero section is the empty one, so 0 = (a, ∅).

The empty open subspace of an algebraic space is the sheafification of the bottom subfunctor and not the bottom subfunctor itself, whose sections over an object of the site with no points are not those of a sheaf.

theorem subspace_zero : (zero Z₁).subspace =
    (⊥ : Subfunctor (pullback a.hom f.hom)).sheafify (BigFppfOver.topology B S hS)

AlgebraicGeometry.Space.FinitePartFibre.one, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 405. The attribute's comment: “unit_of_finite”.

Stacks 04PI, the unit of the finite case. When f is finite the section 1 = (a, T ×_Y X) cut out by all of the points of T ×_Y X, which is the restriction along a of the pair (1_Y, X).

def one (hfin : IsFinite B S hS f.hom) : FinitePartFibre B S hS f a

AlgebraicGeometry.Space.FinitePartFibre.subspace_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 418. The attribute's comment: “unit_is_the_whole_fibre_product”.

Stacks 04PI, the unit of the finite case. The open subspace of the unit is the whole of T ×_Y X, so 1 is the restriction along a of the pair (1_Y, X).

theorem subspace_one (hfin : IsFinite B S hS f.hom) :
    (one (a := a) hfin).subspace = ⊤

AlgebraicGeometry.Space.FinitePartFibre.star₂_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 424. The attribute's comment: “unit_of_finite_is_unit”.

Stacks 04PI, the unit of the finite case. 1 s = s.

theorem star₂_one (hfin : IsFinite B S hS f.hom) : star₂ hf (one hfin) Z₁ = Z₁

AlgebraicGeometry.Space.FinitePartFibre.star₂_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 433. The attribute's comment: “multiplication_is_commutative”.

Stacks 04PI. The multiplication s s' = ⋆₂(s, s') is commutative.

theorem star₂_comm : star₂ hf Z₁ Z₂ = star₂ hf Z₂ Z₁

AlgebraicGeometry.Space.FinitePartFibre.star₂_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Operations.lean, line 438. The attribute's comment: “multiplication_is_associative”.

Stacks 04PI. The multiplication s s' = ⋆₂(s, s') is associative.

theorem star₂_assoc (Z₃ : FinitePartFibre B S hS f a) :
    star₂ hf (star₂ hf Z₁ Z₂) Z₃ = star₂ hf Z₁ (star₂ hf Z₂ Z₃)

AlgebraicGeometry.Space.FinitePartPresheaf.existsUnique_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Presheaf.lean, line 86. The attribute's comment: “projection_to_base”.

Stacks 04PI. The component rule sending a finite open pair to its morphism to Y determines a unique morphism of presheaves to Y, namely the projection FinitePartPresheaf.baseMap.

theorem existsUnique_projection (P : FinitePartPresheaf B S hS f) :
    ∃! π : P.toFunctor ⟶ Y.obj,
      ∀ T (p : P.toFunctor.obj (op T)),
        yonedaEquiv.symm (π.app (op T) p) = (P.sections T p).toBase.hom

AlgebraicGeometry.Space.FinitePartPresheaf.star₁Map, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 260. The attribute's comment: “star_1_as_a_morphism_of_sheaves”.

Stacks 04PI, the operation ⋆₁. The morphism of presheaves ⋆₁ : (X/Y)_fin ×_Y (X/Y)_fin ⟶ (X/Y)_fin sending a pair of sections over a common morphism to Y to the union Z₁ ∪ Z₂.

def star₁Map : Limits.pullback P.baseMap P.baseMap ⟶ P.toFunctor

AlgebraicGeometry.Space.FinitePartPresheaf.sections_star₁Map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 266. The attribute's comment: “star_1_morphism_on_sections”.

Stacks 04PI, the operation ⋆₁. On sections, ⋆₁ is the union Z₁ ∪ Z₂.

theorem sections_star₁Map (T : BigFppfOver B S hS)
    (z : (Limits.pullback P.baseMap P.baseMap).obj (op T)) :
    P.sections T ((star₁Map P hf).app (op T) z) =
      (FinitePartFibre.star₁ hf (FinitePartFibre.ofPair rfl)
        (FinitePartFibre.ofPair (P.sections_snd_toBase_eq_fst T z))).toPair

AlgebraicGeometry.Space.FinitePartPresheaf.star₁Map_comp_baseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 275. The attribute's comment: “star_1_is_a_morphism_over_the_base”.

Stacks 04PI, the operation ⋆₁. It is a morphism over Y.

theorem star₁Map_comp_baseMap :
    star₁Map P hf ≫ P.baseMap = Limits.pullback.fst P.baseMap P.baseMap ≫ P.baseMap

AlgebraicGeometry.Space.FinitePartPresheaf.star₂Map, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 283. The attribute's comment: “star_2_as_a_morphism_of_sheaves”.

Stacks 04PI, the operation ⋆₂. The morphism of presheaves ⋆₂ : (X/Y)_fin ×_Y (X/Y)_fin ⟶ (X/Y)_fin sending a pair of sections over a common morphism to Y to the intersection Z₁ ∩ Z₂.

def star₂Map : Limits.pullback P.baseMap P.baseMap ⟶ P.toFunctor

AlgebraicGeometry.Space.FinitePartPresheaf.sections_star₂Map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 289. The attribute's comment: “star_2_morphism_on_sections”.

Stacks 04PI, the operation ⋆₂. On sections, ⋆₂ is the intersection Z₁ ∩ Z₂.

theorem sections_star₂Map (T : BigFppfOver B S hS)
    (z : (Limits.pullback P.baseMap P.baseMap).obj (op T)) :
    P.sections T ((star₂Map P hf).app (op T) z) =
      (FinitePartFibre.star₂ hf (FinitePartFibre.ofPair rfl)
        (FinitePartFibre.ofPair (P.sections_snd_toBase_eq_fst T z))).toPair

AlgebraicGeometry.Space.FinitePartPresheaf.star₂Map_comp_baseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 298. The attribute's comment: “star_2_is_a_morphism_over_the_base”.

Stacks 04PI, the operation ⋆₂. It is a morphism over Y.

theorem star₂Map_comp_baseMap :
    star₂Map P hf ≫ P.baseMap = Limits.pullback.fst P.baseMap P.baseMap ≫ P.baseMap

AlgebraicGeometry.Space.FinitePartPresheaf.star₃Map, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 306. The attribute's comment: “star_3_as_a_morphism_of_sheaves”.

Stacks 04PI, the operation ⋆₃. The morphism of presheaves ⋆₃ : (X/Y)_fin ×_Y (X/Y)_fin ⟶ (X/Y)_fin sending a pair of sections over a common morphism to Y to the difference Z₁ ∖ Z₂.

def star₃Map : Limits.pullback P.baseMap P.baseMap ⟶ P.toFunctor

AlgebraicGeometry.Space.FinitePartPresheaf.sections_star₃Map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 312. The attribute's comment: “star_3_morphism_on_sections”.

Stacks 04PI, the operation ⋆₃. On sections, ⋆₃ is the difference Z₁ ∖ Z₂.

theorem sections_star₃Map (T : BigFppfOver B S hS)
    (z : (Limits.pullback P.baseMap P.baseMap).obj (op T)) :
    P.sections T ((star₃Map P hf).app (op T) z) =
      (FinitePartFibre.star₃ hf (FinitePartFibre.ofPair rfl)
        (FinitePartFibre.ofPair (P.sections_snd_toBase_eq_fst T z))).toPair

AlgebraicGeometry.Space.FinitePartPresheaf.star₃Map_comp_baseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 321. The attribute's comment: “star_3_is_a_morphism_over_the_base”.

Stacks 04PI, the operation ⋆₃. It is a morphism over Y.

theorem star₃Map_comp_baseMap :
    star₃Map P hf ≫ P.baseMap = Limits.pullback.fst P.baseMap P.baseMap ≫ P.baseMap

AlgebraicGeometry.Space.FinitePartPresheaf.star₄Map, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 329. The attribute's comment: “star_4_as_a_morphism_of_sheaves”.

Stacks 04PI, the operation ⋆₄. The morphism of presheaves ⋆₄ : (X/Y)_fin ×_Y (X/Y)_fin ⟶ (X/Y)_fin sending a pair of sections over a common morphism to Y to the difference Z₂ ∖ Z₁.

def star₄Map : Limits.pullback P.baseMap P.baseMap ⟶ P.toFunctor

AlgebraicGeometry.Space.FinitePartPresheaf.sections_star₄Map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 335. The attribute's comment: “star_4_morphism_on_sections”.

Stacks 04PI, the operation ⋆₄. On sections, ⋆₄ is the difference Z₂ ∖ Z₁.

theorem sections_star₄Map (T : BigFppfOver B S hS)
    (z : (Limits.pullback P.baseMap P.baseMap).obj (op T)) :
    P.sections T ((star₄Map P hf).app (op T) z) =
      (FinitePartFibre.star₄ hf (FinitePartFibre.ofPair rfl)
        (FinitePartFibre.ofPair (P.sections_snd_toBase_eq_fst T z))).toPair

AlgebraicGeometry.Space.FinitePartPresheaf.star₄Map_comp_baseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 344. The attribute's comment: “star_4_is_a_morphism_over_the_base”.

Stacks 04PI, the operation ⋆₄. It is a morphism over Y.

theorem star₄Map_comp_baseMap :
    star₄Map P hf ≫ P.baseMap = Limits.pullback.fst P.baseMap P.baseMap ≫ P.baseMap

AlgebraicGeometry.Space.FinitePartPresheaf.addMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 351. The attribute's comment: “addition_as_a_morphism_of_sheaves”.

Stacks 04PI. The addition of the F₂-algebra as a morphism of presheaves (X/Y)_fin ×_Y (X/Y)_fin ⟶ (X/Y)_fin.

def addMap : Limits.pullback P.baseMap P.baseMap ⟶ P.toFunctor

AlgebraicGeometry.Space.FinitePartPresheaf.sections_addMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 357. The attribute's comment: “addition_morphism_on_sections”.

Stacks 04PI. On sections, the addition is ⋆₁(⋆₃(s, s'), ⋆₄(s, s')).

theorem sections_addMap (T : BigFppfOver B S hS)
    (z : (Limits.pullback P.baseMap P.baseMap).obj (op T)) :
    P.sections T ((addMap P hf).app (op T) z) =
      (FinitePartFibre.add hf (FinitePartFibre.ofPair rfl)
        (FinitePartFibre.ofPair (P.sections_snd_toBase_eq_fst T z))).toPair

AlgebraicGeometry.Space.FinitePartPresheaf.addMap_comp_baseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/PresheafOperations.lean, line 366. The attribute's comment: “addition_is_a_morphism_over_the_base”.

Stacks 04PI. The addition of the F₂-algebra is a morphism over Y.

theorem addMap_comp_baseMap :
    addMap P hf ≫ P.baseMap = Limits.pullback.fst P.baseMap P.baseMap ≫ P.baseMap

AlgebraicGeometry.Space.FinitePartFibre.restrict_star₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Restriction.lean, line 98. The attribute's comment: “star_1_commutes_with_restriction”.

The operation ⋆₁, the union of two sections, commutes with restriction along T' ⟶ T.

theorem restrict_star₁ : (star₁ hf Z₁ Z₂).restrict h = star₁ hf (Z₁.restrict h) (Z₂.restrict h)

AlgebraicGeometry.Space.FinitePartFibre.restrict_star₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Restriction.lean, line 104. The attribute's comment: “star_2_commutes_with_restriction”.

The operation ⋆₂, the intersection of two sections, commutes with restriction along T' ⟶ T.

theorem restrict_star₂ : (star₂ hf Z₁ Z₂).restrict h = star₂ hf (Z₁.restrict h) (Z₂.restrict h)

AlgebraicGeometry.Space.FinitePartFibre.restrict_star₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Restriction.lean, line 110. The attribute's comment: “star_3_commutes_with_restriction”.

The operation ⋆₃, the difference Z₁ ∖ Z₂, commutes with restriction along T' ⟶ T.

theorem restrict_star₃ : (star₃ hf Z₁ Z₂).restrict h = star₃ hf (Z₁.restrict h) (Z₂.restrict h)

AlgebraicGeometry.Space.FinitePartFibre.restrict_star₄, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Restriction.lean, line 116. The attribute's comment: “star_4_commutes_with_restriction”.

The operation ⋆₄, the difference Z₂ ∖ Z₁, commutes with restriction along T' ⟶ T.

theorem restrict_star₄ : (star₄ hf Z₁ Z₂).restrict h = star₄ hf (Z₁.restrict h) (Z₂.restrict h)

AlgebraicGeometry.Space.FinitePartFibre.restrict_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Restriction.lean, line 122. The attribute's comment: “addition_commutes_with_restriction”.

The addition of the F₂-algebra, the symmetric difference of two sections, commutes with restriction along T' ⟶ T.

theorem restrict_add : (add hf Z₁ Z₂).restrict h = add hf (Z₁.restrict h) (Z₂.restrict h)

AlgebraicGeometry.Space.FinitePartFibre.restrict_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Restriction.lean, line 127. The attribute's comment: “zero_commutes_with_restriction”.

The zero section restricts to the zero section.

theorem restrict_zero : (zero Z₁).restrict h = zero (Z₁.restrict h)

AlgebraicGeometry.Space.FinitePartFibre.restrict_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Restriction.lean, line 132. The attribute's comment: “unit_commutes_with_restriction”.

For f finite, the unit section restricts to the unit section.

theorem restrict_one (hfin : IsFinite B S hS f.hom) :
    (one (a := a) hfin).restrict h = one (a := h ≫ a) hfin

AlgebraicGeometry.Space.FinitePartFibre.star₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 284. The attribute's comment: “star_1_on_sections”.

Stacks 04PI, the operation ⋆₁. The union (a, Z₁ ∪ Z₂) of two sections of the finite part lying over the same morphism to Y.

Its projection to T is finite because Z₁ ∪ Z₂ is the disjoint union of the open and closed pieces Z₁ and Z₂ ∖ Z₁, hence their coproduct as a sheaf, and a morphism out of a finite coproduct whose restriction to each summand is finite is finite.

def star₁ : FinitePartFibre B S hS f a

AlgebraicGeometry.Space.FinitePartFibre.pointSet_star₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 315. The attribute's comment: “star_1_on_points”.

Stacks 04PI, the operation ⋆₁. On points, ⋆₁(s, s') is the union Z₁ ∪ Z₂.

theorem pointSet_star₁ : (star₁ hf Z₁ Z₂).pointSet = Z₁.pointSet ∪ Z₂.pointSet

AlgebraicGeometry.Space.FinitePartFibre.add, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 326. The attribute's comment: “addition_of_the_f2_algebra”.

Stacks 04PI, the addition of the F₂-algebra. s + s' = ⋆₁(⋆₃(s, s'), ⋆₄(s, s')).

def add : FinitePartFibre B S hS f a

AlgebraicGeometry.Space.FinitePartFibre.pointSet_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 331. The attribute's comment: “addition_is_the_symmetric_difference”.

Stacks 04PI. The addition s + s' = ⋆₁(⋆₃(s, s'), ⋆₄(s, s')) of the F₂-algebra is the symmetric difference.

theorem pointSet_add : (add hf Z₁ Z₂).pointSet = Z₁.pointSet ∆ Z₂.pointSet

AlgebraicGeometry.Space.FinitePartFibre.add_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 337. The attribute's comment: “addition_is_commutative”.

Stacks 04PI. The addition of the F₂-algebra is commutative.

theorem add_comm : add hf Z₁ Z₂ = add hf Z₂ Z₁

AlgebraicGeometry.Space.FinitePartFibre.add_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 342. The attribute's comment: “addition_is_associative”.

Stacks 04PI. The addition of the F₂-algebra is associative.

theorem add_assoc (Z₃ : FinitePartFibre B S hS f a) :
    add hf (add hf Z₁ Z₂) Z₃ = add hf Z₁ (add hf Z₂ Z₃)

AlgebraicGeometry.Space.FinitePartFibre.add_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 348. The attribute's comment: “zero_is_neutral_for_addition”.

Stacks 04PI. The zero section 0 = (a, ∅) is neutral for the addition.

theorem add_zero : add hf Z₁ (zero Z₁) = Z₁

AlgebraicGeometry.Space.FinitePartFibre.add_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 363. The attribute's comment: “section_plus_itself_is_zero”.

Stacks 04PI. s + s = 0 for every local section: the algebra is an F₂-algebra, every section being its own additive inverse.

theorem add_self : add hf Z₁ Z₁ = zero Z₁

AlgebraicGeometry.Space.FinitePartFibre.star₂_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 370. The attribute's comment: “multiplication_distributes_over_addition”.

Stacks 04PI. The multiplication s s' = ⋆₂(s, s') distributes over the addition.

theorem star₂_add (Z₃ : FinitePartFibre B S hS f a) :
    star₂ hf (add hf Z₁ Z₂) Z₃ = add hf (star₂ hf Z₁ Z₃) (star₂ hf Z₂ Z₃)

AlgebraicGeometry.Space.FinitePartFibre.star₃_eq_star₂_one_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 386. The attribute's comment: “star_3_through_the_unit”.

Stacks 04PI, the finite case. ⋆₃(s, s') = s (1 + s').

theorem star₃_eq_star₂_one_add (hfin : IsFinite B S hS f.hom) :
    star₃ hf Z₁ Z₂ = star₂ hf Z₁ (add hf (one hfin) Z₂)

AlgebraicGeometry.Space.FinitePartFibre.star₄_eq_star₂_one_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Union.lean, line 392. The attribute's comment: “star_4_through_the_unit”.

Stacks 04PI, the finite case. ⋆₄(s, s') = (1 + s) s'.

theorem star₄_eq_star₂_one_add (hfin : IsFinite B S hS f.hom) :
    star₄ hf Z₁ Z₂ = star₂ hf (add hf (one hfin) Z₁) Z₂
Tag 04PK, a lemma

Tag 04PK in the Stacks Project.

AlgebraicGeometry.Space.isOpenImmersion_diagonal_finiteOpenSubspacePresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Diagonal.lean, line 855. The attribute's comment: “relative diagonal”.

Stacks 04PK, the relative diagonal. For a morphism f : X ⟶ Y of algebraic spaces over S, the diagonal (X/Y)_fin ⟶ (X/Y)_fin ×_Y (X/Y)_fin is representable by schemes and an open immersion.

theorem isOpenImmersion_diagonal_finiteOpenSubspacePresheaf
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    IsOpenImmersion B S hS
      (pullback.diagonal (finiteOpenSubspacePresheaf B S hS f).baseMap)

AlgebraicGeometry.Space.relativelyRepresentable_diag_finiteOpenSubspacePresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Diagonal.lean, line 912. The attribute's comment: “absolute diagonal”.

Stacks 04PK, the absolute diagonal. For a morphism f : X ⟶ Y of algebraic spaces over S, the absolute diagonal (X/Y)_fin ⟶ (X/Y)_fin × (X/Y)_fin is representable by schemes: it is the relative diagonal followed by a base change of the diagonal of Y.

theorem relativelyRepresentable_diag_finiteOpenSubspacePresheaf
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    yoneda.relativelyRepresentable
      (diag (finiteOpenSubspacePresheaf B S hS f).toFunctor)
Tag 04QE, a lemma

Tag 04QE in the Stacks Project.

AlgebraicGeometry.Space.isEtale_of_isEtale_comp_baseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/EtaleChart.lean, line 118.

Stacks 04QE. Let f : X ⟶ Y be a morphism of algebraic spaces over S and let U be a scheme of the big fppf site. A morphism from the presheaf represented by U to the finite part (X/Y)_fin — equivalently, a morphism U ⟶ Y together with an open subspace of U ×_Y X finite over U — is representable by schemes and étale as soon as its composite with the projection (X/Y)_fin ⟶ Y is.

theorem isEtale_of_isEtale_comp_baseMap
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (U : AlgebraicGeometry.BigFppfOver B S hS)
    (p : yoneda.obj U ⟶
      (finiteOpenSubspacePresheaf B S hS f).toFunctor)
    (hp : (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (AlgebraicGeometry.BigFppfOver.toScheme B S hS)).presheaf
        (p ≫ (finiteOpenSubspacePresheaf B S hS f).baseMap)) :
    (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (AlgebraicGeometry.BigFppfOver.toScheme B S hS)).presheaf p
Tag 04QF, a lemma

Tag 04QF in the Stacks Project.

AlgebraicGeometry.Space.FinitePartPresheaf.isPullback_mapOfPullbackSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/BaseChangeSquare.lean, line 342.

Stacks 04QF. Let S be a scheme and let a square X' → X, X' → Y', X → Y, Y' → Y be a fibre product square of algebraic spaces over S. Then the square (X'/Y')_fin → (X/Y)_fin, (X'/Y')_fin → Y', (X/Y)_fin → Y, Y' → Y is a fibre product square of sheaves on the big fppf site of S.

theorem isPullback_mapOfPullbackSquare (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X' X Y' Y : AlgebraicSpaces B S hS} (f' : X' ⟶ X) (g' : X' ⟶ Y')
    (f : X ⟶ Y) (g : Y' ⟶ Y) (h : IsPullback f' g' f g) (P : FinitePartPresheaf B S hS g')
    (Q : FinitePartPresheaf B S hS f) :
    IsPullback (mapOfPullbackSquare B S hS f' g' f g h P Q) P.baseMap Q.baseMap g.hom
Tag 04QG, a lemma

Tag 04QG in the Stacks Project.

AlgebraicGeometry.Space.exists_surjective_etale_chart_finiteOpenSubspacePresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/EtaleCover/SurjectiveChart.lean, line 683.

The finite-part sheaf of a separated, locally quasi-finite morphism of algebraic spaces has a surjective étale scheme cover that is étale over the target.

theorem _root_.AlgebraicGeometry.Space.exists_surjective_etale_chart_finiteOpenSubspacePresheaf
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf_sep : Space.IsSeparated B S hS f.hom)
    (hf_lqf : Space.IsLocallyQuasiFinite B S hS f.hom) :
    ∃ (U : BigFppfOver B S hS)
      (p : yoneda.obj U ⟶
        (Space.finiteOpenSubspacePresheaf B S hS f).toFunctor),
      (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf
          (p ≫ (Space.finiteOpenSubspacePresheaf B S hS f).baseMap) ∧
      (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf p ∧
      (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf p
Tag 04QH, a proposition

Tag 04QH in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_finiteOpenSubspacePresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/AlgebraicSpace.lean, line 262. The attribute's comment: “(X/Y)_fin is an algebraic space”.

Stacks 04QH, the first conclusion. The finite part (X/Y)_fin of a separated morphism f : X ⟶ Y of algebraic spaces over S which is locally of finite type is an algebraic space over S.

theorem isAlgebraicSpace_finiteOpenSubspacePresheaf
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hsep : IsSeparated B S hS f.hom) (hf : IsLocallyOfFiniteType B S hS f.hom) :
    IsAlgebraicSpace B S hS (finiteOpenSubspacePresheaf B S hS f).toFunctor

AlgebraicGeometry.Space.isEtale_baseMap_finiteOpenSubspacePresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/AlgebraicSpace.lean, line 274. The attribute's comment: “(X/Y)_fin → Y is étale”.

Stacks 04QH, the second conclusion. The projection (X/Y)_fin ⟶ Y of the finite part of a separated morphism f : X ⟶ Y of algebraic spaces over S which is locally of finite type is étale.

theorem isEtale_baseMap_finiteOpenSubspacePresheaf
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hsep : IsSeparated B S hS f.hom) (hf : IsLocallyOfFiniteType B S hS f.hom) :
    IsEtale B S hS (finiteOpenSubspacePresheaf B S hS f).baseMap
Tag 04QI, a remark

Tag 04QI in the Stacks Project.

AlgebraicGeometry.chartInclusion_origin_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOriginNotSeparated.lean, line 54. The attribute's comment: “the example: the two chart origins are distinct points”.

The two chart origins of affine space with doubled origin are distinct points of the glued scheme.

theorem chartInclusion_origin_ne (k : Type u) [Field k] (n : ℕ) :
    chartInclusion k n 0 (affineOrigin k n) ≠ chartInclusion k n 1 (affineOrigin k n)

AlgebraicGeometry.flat_locallyOfFinitePresentation_not_isSeparated_coordinateMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Scheme/Glueing/DoubledOriginNotSeparated.lean, line 122. The attribute's comment: “the example: flat and locally of finite presentation but not separated”.

In positive dimension the coordinate morphism of affine space with doubled origin is flat and locally of finite presentation but not separated.

theorem flat_locallyOfFinitePresentation_not_isSeparated_coordinateMorphism
    (k : Type u) [Field k] (n : ℕ) (hn : 0 < n) :
    Flat (coordinateMorphism k n) ∧
      LocallyOfFinitePresentation (coordinateMorphism k n) ∧
      ¬ IsSeparated (coordinateMorphism k n)

AlgebraicGeometry.Space.doubledOrigin_finitePart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/DoubledOriginNotAlgebraic/FourPoints.lean, line 457. References: EGA I (5.5.11), “partial”.

Stacks Project, Tag 04QI. The condition that f be separated cannot be dropped from Stacks 04QH. Let X be affine n-space over a field k with its origin doubled, n > 0 (the remark takes n = 1, the affine line with zero doubled), Y affine n-space, and f : X ⟶ Y the coordinate morphism, read as a morphism of algebraic spaces over Spec k in a big fppf site containing Spec k. Then:

  1. f is locally of finite type but not separated, so it satisfies every hypothesis of Stacks 04QH except separatedness;
  2. over the origin of Y there are exactly two points 0₁ ≠ 0₂ of X, the chart origins, and (X/Y)_fin has exactly four points over the origin, its sections over Spec k lying over the origin, which correspond to the four subsets ∅, {0₁}, {0₂}, {0₁, 0₂} of that fibre (AlgebraicGeometry.Space.exists_equiv_originPoints);
  3. of these, exactly the three subsets ∅, {0₁}, {0₂} lift to an open subscheme of U ×_Y X finite over U for an étale U ⟶ Y (AlgebraicGeometry.Space.IsEtaleLiftablePoint, chart index i standing for the chart origin 0ᵢ);
  4. hence (X/Y)_fin, if it is an algebraic space, is not étale over Y;
  5. in fact (X/Y)_fin is not an algebraic space ("Details omitted" in the source).

The second clause of (1) also follows from (5) and Stacks 04QH, which is how it is proved here; (4) is proved by the argument of the remark, independently of (5).

theorem doubledOrigin_finitePart (hn : 0 < n) :
    (IsLocallyOfFiniteType B (Spec (.of k)) hk (schemeSpaceMap (doubledCoordHom B k hk n)).hom ∧
      ¬ IsSeparated B (Spec (.of k)) hk (schemeSpaceMap (doubledCoordHom B k hk n)).hom) ∧
    ((coordinateMorphism k n).base ⁻¹' {affineOrigin k n} =
        {chartInclusion k n 0 (affineOrigin k n), chartInclusion k n 1 (affineOrigin k n)} ∧
      chartInclusion k n 0 (affineOrigin k n) ≠ chartInclusion k n 1 (affineOrigin k n)) ∧
    (∃ e : originPoints (B := B) (k := k) (hk := hk) (n := n) ≃ Set (Fin 2),
      ∀ ξ, e ξ = chartIndices ((doubledOriginFinitePart B k hk n).sections _ ξ.1)) ∧
    Nat.card (originPoints (B := B) (k := k) (hk := hk) (n := n)) = 4 ∧
    {T : Set (Fin 2) | IsEtaleLiftablePoint B k hk n T} = {∅, {0}, {1}} ∧
    (IsAlgebraicSpace B (Spec (.of k)) hk (doubledOriginFinitePart B k hk n).toFunctor →
      ¬ IsEtale B (Spec (.of k)) hk (doubledOriginFinitePart B k hk n).baseMap) ∧
    ¬ IsAlgebraicSpace B (Spec (.of k)) hk (doubledOriginFinitePart B k hk n).toFunctor
Tag 04RI, a lemma

Tag 04RI in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_baseMap_finiteOpenSubspacePresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/SeparatedRepresentable.lean, line 773. The attribute's comment: “part (1): separatedness”.

Stacks 04RI, part (1). For a separated, flat morphism f : X ⟶ Y of algebraic spaces over S which is locally of finite presentation, the projection (X/Y)_fin ⟶ Y from the finite part of f is separated.

theorem isSeparated_baseMap_finiteOpenSubspacePresheaf
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hsep : IsSeparated B S hS f.hom)
    (hflat : IsFlat B S hS f.hom)
    (hfp : IsLocallyOfFinitePresentation B S hS f.hom) :
    IsSeparated B S hS (finiteOpenSubspacePresheaf B S hS f).baseMap

AlgebraicGeometry.Space.isEtale_baseMap_finiteOpenSubspacePresheaf_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/SeparatedRepresentable.lean, line 837. The attribute's comment: “part (1): étaleness”.

For a separated, flat morphism f : X ⟶ Y of algebraic spaces over S which is locally of finite presentation, the projection (X/Y)_fin ⟶ Y from the finite part of f is étale: such a morphism is in particular locally of finite type.

theorem isEtale_baseMap_finiteOpenSubspacePresheaf_of_isFlat
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hsep : IsSeparated B S hS f.hom)
    (_hflat : IsFlat B S hS f.hom)
    (hfp : IsLocallyOfFinitePresentation B S hS f.hom) :
    IsEtale B S hS (finiteOpenSubspacePresheaf B S hS f).baseMap

AlgebraicGeometry.Space.relativelyRepresentable_baseMap_finiteOpenSubspacePresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/SeparatedRepresentable.lean, line 853. The attribute's comment: “part (1): representability”.

Stacks 04RI, part (1). For a separated, flat morphism f : X ⟶ Y of algebraic spaces over S which is locally of finite presentation, the projection (X/Y)_fin ⟶ Y from the finite part of f is representable: it is étale, hence locally quasi-finite, and separated.

theorem relativelyRepresentable_baseMap_finiteOpenSubspacePresheaf
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hsep : IsSeparated B S hS f.hom)
    (hflat : IsFlat B S hS f.hom)
    (hfp : IsLocallyOfFinitePresentation B S hS f.hom) :
    yoneda.relativelyRepresentable (finiteOpenSubspacePresheaf B S hS f).baseMap

AlgebraicGeometry.Space.isRepresentable_finiteOpenSubspacePresheaf_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/SeparatedRepresentable.lean, line 871. The attribute's comment: “part (2): the finite part over a scheme is a scheme”.

Stacks 04RI, part (2). If moreover Y is a scheme, then the finite part (X/Y)_fin of a separated, flat morphism locally of finite presentation is a scheme: it is separated and locally quasi-finite over the representable Y, so Stacks 03XX applies.

theorem isRepresentable_finiteOpenSubspacePresheaf_of_isRepresentable
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hsep : IsSeparated B S hS f.hom)
    (hflat : IsFlat B S hS f.hom)
    (hfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (hY : Y.obj.IsRepresentable) :
    (finiteOpenSubspacePresheaf B S hS f).toFunctor.IsRepresentable
Tag 04RQ, an equation

Tag 04RQ in the Stacks Project.

AlgebraicGeometry.Space.FiniteOpenPairWithSection, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Basic.lean, line 71.

Stacks 04RQ. For a morphism f : X ⟶ Y of algebraic spaces over S with a section σ, and an algebraic space T, a morphism a : T ⟶ Y together with an open subspace Z of T ×_Y X which is finite over T and contains the section of T ×_Y X over T induced by σ.

structure FiniteOpenPairWithSection (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X Y T : AlgebraicSpaces B S hS) (f : X ⟶ Y) (σ : Y ⟶ X)
    (hσ : σ.hom ≫ f.hom = 𝟙 Y.obj)
Tag 04RR, a lemma

Tag 04RR in the Stacks Project.

AlgebraicGeometry.Space.finitePartWithSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/WithSection.lean, line 220. The attribute's comment: “the transformation”.

The canonical transformation from finite open pairs containing a section to all finite open pairs, with its pointwise characterization.

public noncomputable def finitePartWithSection
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicGeometry.AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (σ : Y ⟶ X) (hσ : σ.hom ≫ f.hom = 𝟙 Y.obj) :
    FinitePartWithSection B S hS f σ hσ

AlgebraicGeometry.Space.isOpenImmersion_finitePartWithSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/WithSection.lean, line 316. The attribute's comment: “part (1)”.

The transformation is representable by open immersions.

public theorem isOpenImmersion_finitePartWithSection
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicGeometry.AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (σ : Y ⟶ X) (hσ : σ.hom ≫ f.hom = 𝟙 Y.obj) :
    Space.IsOpenImmersion B S hS
      (finitePartWithSection B S hS f σ hσ).toSubfunctor.ι

AlgebraicGeometry.Space.isClosedImmersion_finitePartWithSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/WithSection.lean, line 331. The attribute's comment: “part (2)”.

For separated f, the same transformation is representable by closed immersions as well as open immersions.

public theorem isClosedImmersion_finitePartWithSection
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicGeometry.AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (σ : Y ⟶ X) (hσ : σ.hom ≫ f.hom = 𝟙 Y.obj)
    (hf : Space.IsSeparated B S hS f.hom) :
    Space.IsClosedImmersion B S hS
      (finitePartWithSection B S hS f σ hσ).toSubfunctor.ι

AlgebraicGeometry.Space.isOpenSubspace_finitePartWithSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/WithSection.lean, line 351. The attribute's comment: “part (3)”.

If the finite-part functor is an algebraic space, the section-containing subfunctor is an open algebraic subspace of it.

public theorem isOpenSubspace_finitePartWithSection
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicGeometry.AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (σ : Y ⟶ X) (hσ : σ.hom ≫ f.hom = 𝟙 Y.obj)
    (hfin : AlgebraicGeometry.IsAlgebraicSpace B S hS
      (Space.finiteOpenSubspacePresheaf B S hS f).toFunctor) :
    Space.IsOpenSubspace B S hS
      (finitePartWithSection B S hS f σ hσ).toSubfunctor

AlgebraicGeometry.Space.openSubscheme_finitePartWithSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/WithSection.lean, line 366. The attribute's comment: “part (4)”.

A scheme representing the finite-part functor contains the section-containing functor as a compatible open subscheme.

public theorem openSubscheme_finitePartWithSection
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicGeometry.AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (σ : Y ⟶ X) (hσ : σ.hom ≫ f.hom = 𝟙 Y.obj)
    (V : AlgebraicGeometry.BigFppfOver B S hS)
    (e : yoneda.obj V ≅
      (Space.finiteOpenSubspacePresheaf B S hS f).toFunctor) :
    ∃ (U : AlgebraicGeometry.BigFppfOver B S hS) (i : U ⟶ V)
      (e' : yoneda.obj U ≅
        (finitePartWithSection B S hS f σ hσ).toSubfunctor.toFunctor),
      AlgebraicGeometry.IsOpenImmersion
        ((AlgebraicGeometry.BigFppfOver.toScheme B S hS).map i) ∧
      yoneda.map i ≫ e.hom =
        e'.hom ≫ (finitePartWithSection B S hS f σ hσ).toSubfunctor.ι
Sources
LeanAlgebraicGeometry.Space.FiniteOpenSubspace · AlgebraicGeometry.Space.finiteOpenSubspacePresheaf · AlgebraicGeometry.Space.isSheaf_finiteOpenSubspacePresheaf · AlgebraicGeometry.Space.finiteOpenSubspaceEquiv · AlgebraicGeometry.Space.finiteOpenSubspaceMap · AlgebraicGeometry.Space.isIso_finiteOpenSubspaceMap_locallyQuasiFinitePart · AlgebraicGeometry.Space.FiniteOpenSubspace.isClosedSubspace · AlgebraicGeometry.Space.FinitePartFibre.zeroFibre

Section79.13 Finite collections of arrows#

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

Tag 04RS, the section

Tag 04RS in the Stacks Project.

Deformation.PointwiseGroupoid.finiteArrows, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FiniteArrows.lean, line 621. The attribute's comment: “the groupoid of finite collections of arrows”.

Stacks 04RS. The septuple of finite collections of arrows of a groupoid is a groupoid: its objects are the finite subsets Z of the arrows with s(Z) a singleton {u} and e(u) ∈ Z, its arrows are the pairs (Z, z) with z ∈ Z, the source of (Z, z) is Z, its target is {z' ∘ z⁻¹ : z' ∈ Z}, and the composite of (Z₁, z₁) with (Z₂, z₂) is (Z₂, z₁ ∘ z₂).

The verification is a reflection along the faithful pair of maps Z ↦ u and (Z, z) ↦ z, which carries the unit, the composition and the inverse of C_fin to those of the original groupoid.

def finiteArrows (P : PointwiseGroupoid source target comp) :
    PointwiseGroupoid (FiniteArrows.src P) (FiniteArrows.tgt P) (FiniteArrows.compose P)
Sources
LeanDeformation.PointwiseGroupoid.finiteArrows

Section79.14 The finite part of a groupoid#

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

Tag 04RT, the section

Tag 04RT in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.finitePart, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/GroupoidFinitePart.lean, line 299. The attribute's comment: “the object space and the arrow space of the finite part”.

Stacks 04RT. The finite part of a groupoid in algebraic spaces whose source morphism is separated and locally of finite type.

Its object space is U' = (R_s/U, e)_fin, the finite part of the source morphism containing the unit: an algebraic space by Stacks 04QH and Stacks 04RR, part (3), and an open subspace of (R_s/U)_fin. Its morphism g : U' ⟶ U is the projection of (R_s/U)_fin restricted to U', and is étale because that projection is étale by Stacks 04QH and the inclusion of an open subspace is étale. Its arrow space is the open subspace Z_univ of U' ×_{g, U, s} R belonging to the pair which the inclusion names under Stacks 04PE, part (2); it is finite over U' by construction, closed by Stacks 04PH, and contains the base change of the unit because every pair named by a section of U' does.

noncomputable def finitePart (G : GroupoidInAlgebraicSpaces C S hS B)
    (hsep : Space.IsSeparated C S hS G.source.hom)
    (hft : Space.IsLocallyOfFiniteType C S hS G.source.hom) :
    FinitePart G
Tag 04RU, a lemma

Tag 04RU in the Stacks Project.

AlgebraicGeometry.Space.FinitePartUniversalOpen, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 1845. The attribute's comment: “clauses (1) and (2) stated; not the groupoid structure”.

Stacks 04RU, clauses (1) and (2). The two structure spaces of the finite part of a groupoid in algebraic spaces over B: the object space U' with its étale projection g : U' ⟶ U, identified with (R_s/U, e)_fin ⟶ U, and the universal open and closed subspace Z_univ ⊂ R ×_{s, U, g} U' finite over U' which contains the base change of the unit.

public structure FinitePartUniversalOpen
    {C : AlgebraicGeometry.BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S}
    {B : AlgebraicGeometry.AlgebraicSpaces C S hS}
    (G : AlgebraicGeometry.GroupoidInAlgebraicSpaces C S hS B)

AlgebraicGeometry.Space.finitePartUniversalOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 1890. The attribute's comment: “clauses (1) and (2); not the groupoid structure or its morphism”.

Stacks 04RU, clauses (1) and (2). For a groupoid in algebraic spaces over B whose source and target are separated and locally of finite type, the object space (R_s/U, e)_fin with its étale projection to U and the universal open and closed subspace of R ×_{s, U, g} U' finite over U' containing the base change of the unit.

public noncomputable def finitePartUniversalOpen
    {C : AlgebraicGeometry.BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S}
    {B : AlgebraicGeometry.AlgebraicSpaces C S hS}
    (G : AlgebraicGeometry.GroupoidInAlgebraicSpaces C S hS B)
    (hs_sep : AlgebraicGeometry.Space.IsSeparated C S hS G.source.hom)
    (_ht_sep : AlgebraicGeometry.Space.IsSeparated C S hS G.target.hom)
    (hs_lft : AlgebraicGeometry.Space.IsLocallyOfFiniteType C S hS G.source.hom)
    (_ht_lft : AlgebraicGeometry.Space.IsLocallyOfFiniteType C S hS G.target.hom) :
    FinitePartUniversalOpen G

AlgebraicGeometry.Space.FinitePartGroupoid, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 1948. The attribute's comment: “clause (3), the groupoid structure on the finite part and its morphism to R”.

Stacks 04RU, clause (3). The groupoid in algebraic spaces (U', Z_univ, s', t', c') carried by the finite part of (U, R, s, t, c), together with its canonical morphism of groupoids to (U, R, s, t, c) over B.

public structure FinitePartGroupoid
    {C : AlgebraicGeometry.BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S}
    {B : AlgebraicGeometry.AlgebraicSpaces C S hS}
    (G : AlgebraicGeometry.GroupoidInAlgebraicSpaces C S hS B)

AlgebraicGeometry.Space.nonempty_finitePartGroupoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 2007. The attribute's comment: “clause (3), the groupoid structure on the finite part and its morphism to R”.

Stacks 04RU, clause (3). For a groupoid in algebraic spaces over B whose source and target are separated and locally of finite type, the finite part carries a groupoid (U', Z_univ, s', t', c') together with a morphism of groupoids to (U, R, s, t, c).

public theorem nonempty_finitePartGroupoid
    {C : AlgebraicGeometry.BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S}
    {B : AlgebraicGeometry.AlgebraicSpaces C S hS}
    (G : AlgebraicGeometry.GroupoidInAlgebraicSpaces C S hS B)
    (hs_sep : AlgebraicGeometry.Space.IsSeparated C S hS G.source.hom)
    (_ht_sep : AlgebraicGeometry.Space.IsSeparated C S hS G.target.hom)
    (hs_lft : AlgebraicGeometry.Space.IsLocallyOfFiniteType C S hS G.source.hom)
    (_ht_lft : AlgebraicGeometry.Space.IsLocallyOfFiniteType C S hS G.target.hom) :
    Nonempty (FinitePartGroupoid G)

AlgebraicGeometry.Space.finitePartGroupoid, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 2728. The attribute's comment: “the groupoid (U', Z_univ, s', t', c', e', i') on the finite part”.

Stacks 04RU. The groupoid in algebraic spaces (U', Z_univ, s', t', c', e', i') over B carried by the finite part of (U, R, s, t, c, e, i).

public noncomputable def finitePartGroupoid :
    AlgebraicGeometry.GroupoidInAlgebraicSpaces C S hS B

AlgebraicGeometry.Space.finitePartGroupoidHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 2735. The attribute's comment: “the canonical morphism of groupoids over B to (U, R, s, t, c, e, i)”.

Stacks 04RU. The canonical morphism of groupoids in algebraic spaces over B (U', Z_univ, s', t', c', e', i') ⟶ (U, R, s, t, c, e, i) whose existence the lemma asserts.

public noncomputable def finitePartGroupoidHom :
    AlgebraicGeometry.GroupoidInAlgebraicSpaces.Hom
      (finitePartGroupoid G hs_sep ht_sep hs_lft ht_lft) G

AlgebraicGeometry.Space.finitePartGroupoid_objectProjection_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 2778. The attribute's comment: “clause (1), g : U' ⟶ U is identified with (R_s/U, e)_fin ⟶ U”.

Stacks 04RU, clause (1). Under the identification of U' with (R_s/U, e)_fin the projection g : U' ⟶ U is the projection of the finite part.

public theorem finitePartGroupoid_objectProjection_spec :
    (finitePartGroupoidObjectProjection G hs_sep ht_sep hs_lft ht_lft).hom =
      (finitePartGroupoidObjectsEquiv G hs_sep ht_sep hs_lft ht_lft).hom ≫
        (finitePartWithSection C S hS G.source
          (finitePartGroupoidUnit G hs_sep ht_sep hs_lft ht_lft)
          (finitePartGroupoidUnit_source G hs_sep ht_sep hs_lft ht_lft)).toSubfunctor.ι ≫
        (AlgebraicGeometry.Space.finiteOpenSubspacePresheaf C S hS G.source).baseMap

AlgebraicGeometry.Space.finitePartGroupoidUniversalOpen_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 2809. The attribute's comment: “clause (2), Z_univ is the universal finite open subspace of R ×_{s, U, g} U'”.

Stacks 04RU, clause (2), universality. Z_univ is the finite open subspace of R ×_{s, U, g} U' classified by the inclusion of U' into the finite part of s; this is what makes it the universal such subspace.

public theorem finitePartGroupoidUniversalOpen_spec :
    (finiteOpenSubspaceEquiv C S hS G.source
        (finitePartGroupoid G hs_sep ht_sep hs_lft ht_lft).objects).1
      ((finitePartGroupoidObjectsEquiv G hs_sep ht_sep hs_lft ht_lft).hom ≫
        (finitePartWithSection C S hS G.source
          (finitePartGroupoidUnit G hs_sep ht_sep hs_lft ht_lft)
          (finitePartGroupoidUnit_source G hs_sep ht_sep hs_lft ht_lft)).toSubfunctor.ι) =
      finitePartGroupoidUniversalOpen G hs_sep ht_sep hs_lft ht_lft

AlgebraicGeometry.Space.finitePartGroupoidUniversalOpen_containsUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 2821. The attribute's comment: “clause (2), Z_univ contains the base change of the unit e”.

Stacks 04RU, clause (2), the unit. Z_univ contains the base change of the unit e.

public theorem finitePartGroupoidUniversalOpen_containsUnit :
    AlgebraicGeometry.Space.ContainsSection C S hS G.source
      (finitePartGroupoidUnit G hs_sep ht_sep hs_lft ht_lft)
      (finitePartGroupoidUnit_source G hs_sep ht_sep hs_lft ht_lft)
      (finitePartGroupoidUniversalOpen G hs_sep ht_sep hs_lft ht_lft)

AlgebraicGeometry.Space.finitePartGroupoidUniversalOpen_closed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 2831. The attribute's comment: “clause (2), Z_univ is closed in R ×_{s, U, g} U' as well as open”.

Stacks 04RU, clause (2), closedness. Z_univ is closed in R ×_{s, U, g} U' as well as open.

public theorem finitePartGroupoidUniversalOpen_closed :
    AlgebraicGeometry.Space.IsClosedSubspace C S hS
      (finitePartGroupoidUniversalOpen G hs_sep ht_sep hs_lft ht_lft).subspace

AlgebraicGeometry.Space.finitePartGroupoid_arrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 2839. The attribute's comment: “clause (2), the arrow space of the finite part is Z_univ”.

Stacks 04RU, clause (2), the arrow space. The space of arrows of the groupoid on the finite part is the universal finite open subspace Z_univ.

public theorem finitePartGroupoid_arrows :
    (finitePartGroupoid G hs_sep ht_sep hs_lft ht_lft).arrows.obj =
      (finitePartGroupoidUniversalOpen G hs_sep ht_sep hs_lft ht_lft).subspace.toFunctor

AlgebraicGeometry.Space.finitePartGroupoidHom_mapArrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/Groupoid.lean, line 2859. The attribute's comment: “the arrow map of the canonical morphism is Z_univ ⊂ R ×_{s, U, g} U' ⟶ R”.

Stacks 04RU. Under the identification of the arrow space with Z_univ, the canonical morphism of groupoids sends an arrow of the finite part to its underlying arrow of R, i.e. it is the second projection of R ×_{s, U, g} U'.

public theorem finitePartGroupoidHom_mapArrows :
    (finitePartGroupoidHom G hs_sep ht_sep hs_lft ht_lft).toGroupoidHom.mapArrows =
      eqToHom (finitePartGroupoid_arrows G hs_sep ht_sep hs_lft ht_lft) ≫
        (finitePartGroupoidUniversalOpen G hs_sep ht_sep hs_lft ht_lft).subspace.ι ≫
        pullback.snd
          (finitePartGroupoidUniversalOpen G hs_sep ht_sep hs_lft ht_lft).toBase.hom
          G.source.hom

AlgebraicGeometry.GroupoidInAlgebraicSpaces.finitePartGroupoid, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/GroupoidStructure.lean, line 639. The attribute's comment: “the groupoid structure on the finite part”.

Stacks 04RU, the groupoid structure. For a groupoid in algebraic spaces over B whose source morphism is separated and locally of finite type, the finite part (U', Z_univ, s', t', c', e', i') is a groupoid in algebraic spaces over B.

noncomputable def finitePartGroupoid (hsep : Space.IsSeparated C S hS G.source.hom)
    (hft : Space.IsLocallyOfFiniteType C S hS G.source.hom) :
    GroupoidInAlgebraicSpaces C S hS B

AlgebraicGeometry.GroupoidInAlgebraicSpaces.finitePartGroupoidHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/FinitePart/GroupoidStructure.lean, line 651. The attribute's comment: “the canonical morphism of groupoids from the finite part to the given groupoid”.

Stacks 04RU, the canonical morphism of groupoids. For a groupoid in algebraic spaces over B whose source morphism is separated and locally of finite type, the canonical morphism of groupoids in algebraic spaces over B from the finite part to the given groupoid: on objects it is the étale projection g : U' ⟶ U of Stacks 04RU, clause (1), and on arrows it is the rule (u, Z, z) ↦ z.

noncomputable def finitePartGroupoidHom (hsep : Space.IsSeparated C S hS G.source.hom)
    (hft : Space.IsLocallyOfFiniteType C S hS G.source.hom) :
    Hom (finitePartGroupoid hsep hft) G
Sources
LeanAlgebraicGeometry.GroupoidInAlgebraicSpaces.finitePart · AlgebraicGeometry.Space.FinitePartUniversalOpen · AlgebraicGeometry.Space.finitePartUniversalOpen · AlgebraicGeometry.Space.FinitePartGroupoid · AlgebraicGeometry.Space.nonempty_finitePartGroupoid · AlgebraicGeometry.Space.finitePartGroupoid · AlgebraicGeometry.Space.finitePartGroupoidHom · AlgebraicGeometry.Space.finitePartGroupoid_objectProjection_spec

Section79.15 Étale localization of groupoid schemes#

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

Tag 04RK, a definition

Tag 04RK in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.isQuasiSplitAt_of_isLocallyArtinian_arrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/OverField/IdentityArrowSubgroupoid.lean, line 427. The attribute's comment: “part (3): a groupoid scheme with a one-point object scheme and a zero-dimensional arrow scheme is quasi-split at every point of its object scheme, the quasi-splitting being the open and closed piece of the arrow scheme through the identity”.

A groupoid scheme with a one-point object scheme and a zero-dimensional arrow scheme is quasi-split at every point of its object scheme, in the sense of part (3) of Stacks 04RK.

theorem isQuasiSplitAt_of_isLocallyArtinian_arrows (u : G.objects.left) : IsQuasiSplitAt G u

AlgebraicGeometry.GroupoidInAlgebraicSpaces.OpenFiniteSubgroupoid, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Splittings.lean, line 88. The attribute's comment: “conditions (a) and (b) on the open subspace”.

An open subspace of the arrow space of a groupoid in algebraic spaces which is itself a groupoid on the ambient object space, with the restricted source and target morphisms finite and with composition the restriction of the ambient composition.

This is conditions (a) and (b) shared by the three splittings of Stacks 04RK.

structure OpenFiniteSubgroupoid (G : GroupoidInAlgebraicSpaces C S hS B)

AlgebraicGeometry.GroupoidInAlgebraicSpaces.identityPoint_hasCommonExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Splittings.lean, line 126. The attribute's comment: “part (3): the identity on points is well defined”.

Taking the identity arrow at a field-valued point of the object space respects common extension, so it descends to the points of the two spaces.

theorem identityPoint_hasCommonExtension (G : GroupoidInAlgebraicSpaces C S hS B)
    {p q : Space.FieldValuedPoint C S hS G.objects.obj}
    (h : Space.FieldValuedPoint.HasCommonExtension C S hS G.objects.obj p q) :
    Space.FieldValuedPoint.HasCommonExtension C S hS G.arrows.obj
      (identityPoint G p) (identityPoint G q)

AlgebraicGeometry.GroupoidInAlgebraicSpaces.StrongSplitting, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Splittings.lean, line 163. The attribute's comment: “part (1): a strong splitting”.

A strong splitting of a groupoid in algebraic spaces at a point u of its object space: an open finite subgroupoid containing every point of the arrow space whose source and target are both u.

structure StrongSplitting (G : GroupoidInAlgebraicSpaces C S hS B)
    (u : Space.points C S hS G.objects.obj) extends OpenFiniteSubgroupoid G

AlgebraicGeometry.GroupoidInAlgebraicSpaces.Splitting, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Splittings.lean, line 175. The attribute's comment: “part (2): a splitting”.

A splitting of a groupoid in algebraic spaces at a point u of its object space: an open finite subgroupoid containing every point of the stabilizer which lies over u.

structure Splitting (G : GroupoidInAlgebraicSpaces C S hS B)
    (u : Space.points C S hS G.objects.obj) extends OpenFiniteSubgroupoid G

AlgebraicGeometry.GroupoidInAlgebraicSpaces.QuasiSplitting, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Splittings.lean, line 187. The attribute's comment: “part (3): a quasi-splitting”.

A quasi-splitting of a groupoid in algebraic spaces at a point u of its object space: an open finite subgroupoid containing the identity arrow at u.

structure QuasiSplitting (G : GroupoidInAlgebraicSpaces C S hS B)
    (u : Space.points C S hS G.objects.obj) extends OpenFiniteSubgroupoid G

AlgebraicGeometry.GroupoidInAlgebraicSpaces.IsStronglySplitAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Splittings.lean, line 196. The attribute's comment: “part (1): strongly split over a point”.

A groupoid in algebraic spaces is strongly split at a point of its object space when a strong splitting there exists.

abbrev IsStronglySplitAt (G : GroupoidInAlgebraicSpaces C S hS B)
    (u : Space.points C S hS G.objects.obj) : Prop

AlgebraicGeometry.GroupoidInAlgebraicSpaces.IsSplitAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Splittings.lean, line 202. The attribute's comment: “part (2): split over a point”.

A groupoid in algebraic spaces is split at a point of its object space when a splitting there exists.

abbrev IsSplitAt (G : GroupoidInAlgebraicSpaces C S hS B)
    (u : Space.points C S hS G.objects.obj) : Prop

AlgebraicGeometry.GroupoidInAlgebraicSpaces.IsQuasiSplitAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/Splittings.lean, line 208. The attribute's comment: “part (3): quasi-split over a point”.

A groupoid in algebraic spaces is quasi-split at a point of its object space when a quasi-splitting there exists.

abbrev IsQuasiSplitAt (G : GroupoidInAlgebraicSpaces C S hS B)
    (u : Space.points C S hS G.objects.obj) : Prop

Stacks.Groupoids.GroupoidScheme.OpenFiniteSubgroupoid, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SchemeSplittings.lean, line 124. The attribute's comment: “conditions (a) and (b) on the open subscheme, for a groupoid scheme”.

An open subscheme of the arrow scheme of a groupoid scheme which is itself a groupoid scheme on the ambient object scheme, with the restricted source and target morphisms finite and with composition the restriction of the ambient composition.

This is conditions (a) and (b) shared by the three splittings of Stacks 04RK, read for a groupoid scheme.

structure OpenFiniteSubgroupoid (G : GroupoidScheme S)

Stacks.Groupoids.GroupoidScheme.QuasiSplitting, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SchemeSplittings.lean, line 147. The attribute's comment: “part (3), for a groupoid scheme: a quasi-splitting of R over u”.

A quasi-splitting of a groupoid scheme over a point u of its object scheme: an open finite subgroupoid whose scheme of arrows contains the identity arrow e(u).

structure QuasiSplitting (G : GroupoidScheme S) (u : G.objects.left) extends
    OpenFiniteSubgroupoid G

Stacks.Groupoids.GroupoidScheme.IsQuasiSplitAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SchemeSplittings.lean, line 157. The attribute's comment: “part (3), for a groupoid scheme: R is quasi-split over u”.

A groupoid scheme is quasi-split over a point of its object scheme when a quasi-splitting there exists.

abbrev IsQuasiSplitAt (G : GroupoidScheme S) (u : G.objects.left) : Prop

Stacks.Groupoids.GroupoidScheme.OpenFiniteSubgroupoid.toQuasiSplitting, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SchemeSplittings.lean, line 166. The attribute's comment: “the footnote to part (3): condition (c) follows from condition (a)”.

The footnote to part (3) of Stacks 04RK: condition (c) is implied by condition (a). An open finite subgroupoid of a groupoid scheme contains the identity arrow at every point of the object scheme, because the inclusion is a morphism of groupoid schemes which is the identity on objects, and so carries the identity section of the subgroupoid to that of the ambient groupoid.

def OpenFiniteSubgroupoid.toQuasiSplitting {G : GroupoidScheme S} (P : OpenFiniteSubgroupoid G)
    (u : G.objects.left) : QuasiSplitting G u

Stacks.Groupoids.GroupoidScheme.StrongSplitting, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SchemeSplittings.lean, line 187. The attribute's comment: “part (1), for a groupoid scheme: a strong splitting of R over u”.

A strong splitting of a groupoid scheme over a point u of its object scheme: an open finite subgroupoid whose scheme of arrows contains every arrow of R whose source and target are both u.

This is part (1) of Stacks 04RK, read for a groupoid scheme. It is strictly stronger than Stacks.Groupoids.GroupoidScheme.QuasiSplitting, whose condition (c) asks only for the identity arrow e(u); see Stacks.Groupoids.GroupoidScheme.StrongSplitting.toQuasiSplitting.

structure StrongSplitting (G : GroupoidScheme S) (u : G.objects.left) extends
    OpenFiniteSubgroupoid G

Stacks.Groupoids.GroupoidScheme.IsStronglySplitAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SchemeSplittings.lean, line 197. The attribute's comment: “part (1), for a groupoid scheme: R is strongly split over u”.

A groupoid scheme is strongly split over a point of its object scheme when a strong splitting there exists.

abbrev IsStronglySplitAt (G : GroupoidScheme S) (u : G.objects.left) : Prop
Tag 04RL, a situation

Tag 04RL in the Stacks Project.

AlgebraicGeometry.Space.StrongSplittingSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SplittingSituations.lean, line 91.

Stacks Project, Tag 04RL. The standing strong splitting situation for a groupoid scheme: a chosen object with finite stabilizer, at whose stabilizer points the source is quasi-finite.

structure StrongSplittingSituation
Tag 0DTB, a situation

Tag 0DTB in the Stacks Project.

AlgebraicGeometry.Space.SplittingSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SplittingSituations.lean, line 122.

Stacks Project, Tag 0DTB. The standing splitting situation for a groupoid scheme at a point of its object scheme.

structure SplittingSituation
Tag 04RV, a situation

Tag 04RV in the Stacks Project.

AlgebraicGeometry.Space.QuasiSplittingSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SplittingSituations.lean, line 63.

Stacks Project, Tag 04RV. The standing quasi-splitting situation: a point u of the object scheme of a groupoid scheme whose source and target are separated and locally of finite type, with the source quasi-finite at the identity arrow e(u).

structure QuasiSplittingSituation
Tag 03FM, a lemma

Tag 03FM in the Stacks Project.

AlgebraicGeometry.Space.exists_stronglySplit_of_strongSplittingSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/EtaleLocalizationArrowContainment/StrongSplitting.lean, line 313. The attribute's comment: “all four assertions, in Situation 04RL: the algebraic space U', the étale g : U' ⟶ U and the point u' : Spec κ(u) ⟶ U' over u are PRODUCED, and R|_{U'} is strongly split over u'. Beyond Situation 04RL the only hypotheses are that the big fppf site contains the base, object, arrow and composable-pair schemes and Spec κ(u), which is this library's standing ambient requirement”.

Stacks Project, Tag 03FM. In the strong splitting situation of Stacks 04RL there are an algebraic space U', an étale morphism g : U' ⟶ U of algebraic spaces and a point u' : Spec κ(u) ⟶ U' lying over u : Spec κ(u) ⟶ U such that the restriction R' = R|_{U'} of R to U' is strongly split over u'.

U' is the object space of the finite part (R_s/U, e)_fin of Stacks 04RU, g its étale projection, u' the pair (u, Z_u) where Z_u is the open and closed piece of the fibre F_u = R ×_{s, U} Spec κ(u) supported on the arrows from u to itself, and the strong splitting is the universal open Z_univ read inside R|_{U'}. Being strongly split is a condition on a point of |U'|, so it is asserted at the point of |U'| which the morphism u' : Spec κ(u) ⟶ U' determines.

theorem exists_stronglySplit_of_strongSplittingSituation
    (D : StrongSplittingSituation.{u})
    (C : BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left)
    (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hK : C.Contains (Spec (D.groupoid.objects.left.residueField D.u))) :
    ∃ (U' : AlgebraicSpaces C D.S hS)
      (g : U' ⟶ (D.groupoid.realization C hS hU hR hP).objects),
      IsEtale C D.S hS g.hom ∧
      ∃ v : U'.obj.obj (Opposite.op
          (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK)),
        (yonedaSchemePointEquiv C hS hU (Opposite.op
            (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK))
            (g.hom.app _ v)).left =
          D.groupoid.objects.left.fromSpecResidueField D.u ∧
        GroupoidInAlgebraicSpaces.IsStronglySplitAt
          (GroupoidInAlgebraicSpaces.restrict (D.groupoid.realization C hS hU hR hP)
            g).groupoid
          ((residueSectionValuedPoint D.groupoid C hS D.u hK U' v).class C D.S hS U'.obj)
Tag 0DTC, a lemma

Tag 0DTC in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.exists_split_of_splittingSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/EtaleLocalizationStabilizerContainment.lean, line 1016. The attribute's comment: “ALL FOUR ASSERTIONS, in Situation 0DTB: the algebraic space U', the etale morphism g : U' -> U, the point u' : Spec k(u) -> U' lying over u, and that the restriction R|_{U'} is SPLIT over u' -- all four PRODUCED, none assumed. The situation hypothesis is AlgebraicGeometry.Space.SplittingSituation, which carries the 0DTB attribute, and NOT the stronger StrongSplittingSituation of Tag 04RL. Beyond Situation 0DTB the only hypotheses are that the big fppf site contains the base, object, arrow and composable-pair schemes and Spec k(u), which is this library's standing ambient requirement. The supporting open of the fibre is the stabilizer-supported one of SplittingSituation.exists_fiberOpens_stabilizer, a proper subset in general of the target-condition open that Tag 03FM uses”.

Stacks Project, Tag 0DTC. In the splitting situation of Stacks 0DTB there are an algebraic space U', an étale morphism g : U' ⟶ U of algebraic spaces and a point u' : Spec κ(u) ⟶ U' lying over u : Spec κ(u) ⟶ U such that the restriction R' = R|_{U'} of R to U' is split over u'.

U' is the object space of the finite part (R_s/U, e)_fin of Stacks 04RU, g its étale projection, u' the pair (u, Z_u) where Z_u is the open and closed piece of the fibre F_u = R ×_{s, U} Spec κ(u) supported on the arrows underlying the points of the stabilizer group scheme over u, and the splitting is the universal open Z_univ read inside R|_{U'}. Being split is a condition on a point of |U'|, so it is asserted at the point of |U'| which the morphism u' : Spec κ(u) ⟶ U' determines.

The standing hypothesis is AlgebraicGeometry.Space.SplittingSituation, Situation 0DTB, and not the strictly stronger AlgebraicGeometry.Space.StrongSplittingSituation of Stacks 04RL: the open Z_u is supported on the stabilizer, which is in general a proper subset of the arrows with both endpoints at u. So this is not a formal consequence of Stacks 03FM, AlgebraicGeometry.Space.exists_stronglySplit_of_strongSplittingSituation.

theorem exists_split_of_splittingSituation
    (D : AlgebraicGeometry.Space.SplittingSituation.{u})
    (C : BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left)
    (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hK : C.Contains (Spec (D.groupoid.objects.left.residueField D.u))) :
    ∃ (U' : AlgebraicSpaces C D.S hS)
      (g : U' ⟶ (D.groupoid.realization C hS hU hR hP).objects),
      IsEtale C D.S hS g.hom ∧
      ∃ v : U'.obj.obj (Opposite.op
          (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK)),
        (yonedaSchemePointEquiv C hS hU (Opposite.op
            (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK))
            (g.hom.app _ v)).left =
          D.groupoid.objects.left.fromSpecResidueField D.u ∧
        GroupoidInAlgebraicSpaces.IsSplitAt
          (GroupoidInAlgebraicSpaces.restrict (D.groupoid.realization C hS hU hR hP)
            g).groupoid
          ((residueSectionValuedPoint D.groupoid C hS D.u hK U' v).class C D.S hS U'.obj)
Tag 04RW, a lemma

Tag 04RW in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.exists_etale_quasiSplitting_of_quasiSplittingSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/EtaleLocalizationQuasiSplittingPoint.lean, line 337.

Stacks Project, Tag 04RW.

In the quasi-splitting situation of Stacks 04RV there are an algebraic space U', an étale morphism g : U' ⟶ U of algebraic spaces and a point u' : Spec κ(u) ⟶ U' lying over u such that the restriction R|_{U'} is quasi-split over u'.

U' is the finite part (R_s/U, e)_fin of Stacks 04RU and g its étale projection; u' is the pair (u, Z_u) with Z_u = {e(u)}, which is an open and closed piece of the fibre F_u = R ×_{s, U} Spec κ(u) finite over κ(u) because the source is quasi-finite at e(u); and the quasi-splitting is the universal open Z_univ of Stacks 04RU read inside R|_{U'}, which is a quasi-splitting at every point of U'.

theorem exists_etale_quasiSplitting_of_quasiSplittingSituation
    (D : AlgebraicGeometry.Space.QuasiSplittingSituation.{u})
    (C : BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left)
    (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hK : C.Contains (Spec (D.groupoid.objects.left.residueField D.u))) :
    ∃ (U' : AlgebraicSpaces C D.S hS)
      (g : U' ⟶ (D.groupoid.realization C hS hU hR hP).objects),
      AlgebraicGeometry.Space.IsEtale C D.S hS g.hom ∧
      ∃ v : U'.obj.obj (Opposite.op
          (AlgebraicGeometry.Space.residueFieldSiteObject C hS
            (X := D.groupoid.objects) D.u hK)),
        (AlgebraicGeometry.Space.yonedaSchemePointEquiv C hS hU
            (Opposite.op (AlgebraicGeometry.Space.residueFieldSiteObject C hS
              (X := D.groupoid.objects) D.u hK))
            (g.hom.app _ v)).left =
              D.groupoid.objects.left.fromSpecResidueField D.u ∧
        IsQuasiSplitAt (restrict (D.groupoid.realization C hS hU hR hP) g).groupoid
          (AlgebraicGeometry.Space.pointsMap C D.S hS U'.obj
            (eqToHom (restrict (D.groupoid.realization C hS hU hR hP) g).objects_eq.symm).hom
            (AlgebraicGeometry.Space.FieldValuedPoint.class C D.S hS U'.obj
              { carrier := D.groupoid.objects.left.residueField D.u
                contained := hK
                toBase := D.groupoid.objects.left.fromSpecResidueField D.u ≫
                  D.groupoid.objects.hom
                value := v }))

Stacks.Groupoids.GroupoidScheme.exists_quasiSplit_of_quasiSplittingSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasiSplittingEtaleLocalization.lean, line 484. The attribute's comment: “ALL FOUR ASSERTIONS, in Situation 04RV: the algebraic space U', the etale morphism g : U' -> U, the point u' : Spec k(u) -> U' lying over u, and that the restriction R|_{U'} is QUASI-SPLIT over u' -- all four PRODUCED, none assumed. The situation hypothesis is AlgebraicGeometry.Space.QuasiSplittingSituation, which carries the 04RV attribute. The open Z_u of the fibre is the one supported on the identity arrow e(u), which is open and closed and finite over k(u) because s is quasi-finite at e(u), the one geometric hypothesis of Tag 04RV beyond separatedness and local finiteness of type. Beyond Situation 04RV the only hypotheses are that the big fppf site contains the base, object, arrow and composable-pair schemes and Spec k(u), which is this library's standing ambient requirement”.

Stacks Project, Tag 04RW. In the quasi-splitting situation of Stacks 04RV there are an algebraic space U', an étale morphism g : U' ⟶ U of algebraic spaces and a point u' : Spec κ(u) ⟶ U' lying over u : Spec κ(u) ⟶ U such that the restriction R' = R|_{U'} of R to U' is quasi-split over u'.

U' is the object space of the finite part (R_s/U, e)_fin, g its étale projection, u' the pair (u, Z_u) with Z_u the open and closed piece of the fibre F_u = R ×_{s, U} Spec κ(u) supported on the identity arrow e(u), and the quasi-splitting is the universal open Z_univ read inside R|_{U'}.

theorem exists_quasiSplit_of_quasiSplittingSituation
    (D : AlgebraicGeometry.Space.QuasiSplittingSituation.{u})
    (C : BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left)
    (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hK : C.Contains (Spec (D.groupoid.objects.left.residueField D.u))) :
    ∃ (U' : AlgebraicSpaces C D.S hS)
      (g : U' ⟶ (D.groupoid.realization C hS hU hR hP).objects),
      IsEtale C D.S hS g.hom ∧
      ∃ v : U'.obj.obj (Opposite.op
          (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK)),
        (yonedaSchemePointEquiv C hS hU (Opposite.op
            (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK))
            (g.hom.app _ v)).left =
          D.groupoid.objects.left.fromSpecResidueField D.u ∧
        GroupoidInAlgebraicSpaces.IsQuasiSplitAt
          (GroupoidInAlgebraicSpaces.restrict (D.groupoid.realization C hS hU hR hP)
            g).groupoid
          ((residueSectionValuedPoint D.groupoid C hS D.u hK U' v).class C D.S hS U'.obj)
Tag 04RX, a lemma

Tag 04RX in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.nonempty_etaleStrongSplitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/StrongSplittingEtaleScheme.lean, line 146. The attribute's comment: “in Situation 04RL with the source flat and locally of finite presentation: U' is a SCHEME (asserted as representability of the neighbourhood), U' ⟶ U is SEPARATED as well as étale, and R|_{U'} is strongly split over a Spec κ(u)-valued point of U' lying over u. The neighbourhood, its point and the splitting are Stacks 03FM, which this library proves as AlgebraicGeometry.Space.exists_stronglySplit_of_strongSplittingSituation; the scheme-ness and the separatedness are Stacks 04RI and Stacks 04RR applied to the finite part (R_s/U, e)_fin, through its identification with the neighbourhood recorded by AlgebraicGeometry.Space.FinitePartUniversalOpen.objectsEquiv and objectProjection_spec. Strong splitting is Stacks 04RK part (1) for the restriction of the REALIZATION of the groupoid scheme, as in this library's Stacks 03FM and Stacks 04RY; the scheme-level Stacks.Groupoids.GroupoidScheme.StrongSplitting is not used, the composition of the restricted realization not being compared with the composition of AlgebraicGeometry.GroupoidScheme.restrict. Only flatness and local finite presentation of the SOURCE are assumed, where the tag asks them of the target too, so the hypotheses are weaker than the tag's. Beyond Situation 04RL the remaining hypotheses are that the big fppf site contains the base, object, arrow and composable-pair schemes and Spec κ(u), this library's standing ambient requirement”.

Stacks Project, Tag 04RX.

In the strong splitting situation of Stacks 04RL, with the source in addition flat and locally of finite presentation, there are a scheme U', a separated étale morphism g : U' ⟶ U, and a point u' of U' over u with κ(u) = κ(u'), such that the restriction R' = R|_{U'} is strongly split over u'.

The neighbourhood is U' = (R_s/U, e)_{fin}, the finite part of Stacks 04RU containing the unit, with its étale projection; it is a scheme by Stacks 04RI part (2) and Stacks 04RR part (4), and the projection is separated by Stacks 04RI part (1) and Stacks 04RR part (1). The point and the strong splitting are those of Stacks 03FM, the point being recorded as a section over Spec κ(u) whose image under g is the canonical morphism Spec κ(u) ⟶ U.

theorem nonempty_etaleStrongSplitting
    (D : AlgebraicGeometry.Space.StrongSplittingSituation.{u})
    (C : AlgebraicGeometry.BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left)
    (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hK : C.Contains (Spec (D.groupoid.objects.left.residueField D.u)))
    (hflat : AlgebraicGeometry.Flat D.groupoid.source.left)
    (hfp : AlgebraicGeometry.LocallyOfFinitePresentation D.groupoid.source.left) :
    ∃ (U' : AlgebraicGeometry.AlgebraicSpaces C D.S hS)
      (g : U' ⟶ (D.groupoid.realization C hS hU hR hP).objects),
      U'.obj.IsRepresentable ∧
      AlgebraicGeometry.Space.IsEtale C D.S hS g.hom ∧
      AlgebraicGeometry.Space.IsSeparated C D.S hS g.hom ∧
      ∃ v : U'.obj.obj (Opposite.op
          (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK)),
        (yonedaSchemePointEquiv C hS hU (Opposite.op
            (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK))
            (g.hom.app _ v)).left =
          D.groupoid.objects.left.fromSpecResidueField D.u ∧
        IsStronglySplitAt
          (restrict (D.groupoid.realization C hS hU hR hP) g).groupoid
          ((residueSectionValuedPoint D.groupoid C hS D.u hK U' v).class C D.S hS U'.obj)
Tag 0DTD, a lemma

Tag 0DTD in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.exists_etale_separated_scheme_split, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SplittingEtaleScheme.lean, line 120. The attribute's comment: “in Situation 0DTB with the source flat and locally of finite presentation: U' is a SCHEME (asserted as representability of the neighbourhood), U' ⟶ U is SEPARATED as well as étale, and R|_{U'} is SPLIT over a Spec κ(u)-valued point of U' lying over u. The neighbourhood, its point and the splitting are Stacks 0DTC, which this library proves as Stacks.Groupoids.GroupoidScheme.exists_split_of_splittingSituation; the scheme-ness and the separatedness are Stacks 04RI and Stacks 04RR applied to the finite part (R_s/U, e)_fin, through its identification with the neighbourhood recorded by AlgebraicGeometry.Space.FinitePartUniversalOpen.objectsEquiv and objectProjection_spec. Splitting is Stacks 04RK part (2) for the restriction of the REALIZATION of the groupoid scheme, as in this library's Stacks 0DTC and Stacks 04RX; the scheme-level Stacks.Groupoids.GroupoidScheme.Splitting is not used, the composition of the restricted realization not being compared with the composition of AlgebraicGeometry.GroupoidScheme.restrict. The residue-field clause κ(u) = κ(u') is the section over Spec κ(u): a section of a representable U' is a point u' of U' over u together with a retraction of the residue field map at u', and a retraction forces that map to be an isomorphism by AlgebraicGeometry.Scheme.Hom.isIso_residueFieldMap_of_retraction. Only flatness and local finite presentation of the SOURCE are assumed, where the tag asks them of the target too, so the hypotheses are weaker than the tag's. Beyond Situation 0DTB the remaining hypotheses are that the big fppf site contains the base, object, arrow and composable-pair schemes and Spec κ(u), this library's standing ambient requirement”.

Stacks Project, Tag 0DTD.

In the splitting situation of Stacks 0DTB, with the source in addition flat and locally of finite presentation, there are a scheme U', a separated étale morphism g : U' ⟶ U, and a point u' of U' over u with κ(u) = κ(u'), such that the restriction R' = R|_{U'} is split over u'.

The neighbourhood is U' = (R_s/U, e)_{fin}, the finite part of Stacks 04RU containing the unit, with its étale projection; it is a scheme by Stacks 04RI part (2) and Stacks 04RR part (4), and the projection is separated by Stacks 04RI part (1) and Stacks 04RR part (1). The point and the splitting are those of Stacks 0DTC, the point being recorded as a section over Spec κ(u) whose image under g is the canonical morphism Spec κ(u) ⟶ U.

theorem exists_etale_separated_scheme_split
    (D : AlgebraicGeometry.Space.SplittingSituation.{u})
    (C : AlgebraicGeometry.BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left)
    (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hK : C.Contains (Spec (D.groupoid.objects.left.residueField D.u)))
    (hflat : AlgebraicGeometry.Flat D.groupoid.source.left)
    (hfp : AlgebraicGeometry.LocallyOfFinitePresentation D.groupoid.source.left) :
    ∃ (U' : AlgebraicGeometry.AlgebraicSpaces C D.S hS)
      (g : U' ⟶ (D.groupoid.realization C hS hU hR hP).objects),
      U'.obj.IsRepresentable ∧
      AlgebraicGeometry.Space.IsEtale C D.S hS g.hom ∧
      AlgebraicGeometry.Space.IsSeparated C D.S hS g.hom ∧
      ∃ v : U'.obj.obj (Opposite.op
          (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK)),
        (yonedaSchemePointEquiv C hS hU (Opposite.op
            (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK))
            (g.hom.app _ v)).left =
          D.groupoid.objects.left.fromSpecResidueField D.u ∧
        IsSplitAt
          (restrict (D.groupoid.realization C hS hU hR hP) g).groupoid
          ((residueSectionValuedPoint D.groupoid C hS D.u hK U' v).class C D.S hS U'.obj)
Tag 04RY, a lemma

Tag 04RY in the Stacks Project.

AlgebraicGeometry.GroupoidInAlgebraicSpaces.exists_etale_separated_scheme_quasiSplitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/FinitePartSchemeLocalization.lean, line 79. The attribute's comment: “U' is a scheme, U' ⟶ U is separated and étale, and R|_{U'} is quasi-split at every point of U'”.

Stacks Project, Tag 04RY, for a groupoid in algebraic spaces whose object space is a scheme.

Let G = (U, R, s, t, c) be a groupoid in algebraic spaces over B whose source and target are separated, whose source is flat and locally of finite presentation, whose target is locally of finite type and whose object space U is a scheme. Then there is an algebraic space U' which is a scheme, a separated étale morphism g : U' ⟶ U, and R|_{U'} is quasi-split at every point of U'.

theorem exists_etale_separated_scheme_quasiSplitting
    (G : GroupoidInAlgebraicSpaces C S hS B)
    (hsep : Space.IsSeparated C S hS G.source.hom)
    (htsep : Space.IsSeparated C S hS G.target.hom)
    (hflat : Space.IsFlat C S hS G.source.hom)
    (hfp : Space.IsLocallyOfFinitePresentation C S hS G.source.hom)
    (htlft : Space.IsLocallyOfFiniteType C S hS G.target.hom)
    (hU : G.objects.obj.IsRepresentable) :
    ∃ (U' : AlgebraicSpaces C S hS) (g : U' ⟶ G.objects),
      U'.obj.IsRepresentable ∧
      Space.IsEtale C S hS g.hom ∧
      Space.IsSeparated C S hS g.hom ∧
      ∀ u' : Space.points C S hS (restrict G g).groupoid.objects.obj,
        IsQuasiSplitAt (restrict G g).groupoid u'

Stacks.Groupoids.GroupoidScheme.exists_etale_separated_scheme_quasiSplitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/FinitePartSchemeLocalization.lean, line 146. The attribute's comment: “in Situation 04RV: U' is a scheme, U' ⟶ U is separated and étale, and R|_{U'} is quasi-split at every point of U'”.

Stacks Project, Tag 04RY, in the quasi-splitting situation of Stacks 04RV.

In Situation 04RV, assume in addition that the source of the groupoid scheme is flat and locally of finite presentation. Then there is a scheme U', a separated étale morphism g : U' ⟶ U, and R|_{U'} is quasi-split at every point of U'.

Only the flatness and local finite presentation of the source are used; the tag assumes them of the target as well, so the hypotheses here are weaker than the tag's. Separatedness and local finiteness of type of the source and of the target come from Situation 04RV itself.

theorem exists_etale_separated_scheme_quasiSplitting
    (D : AlgebraicGeometry.Space.QuasiSplittingSituation.{u})
    (C : AlgebraicGeometry.BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left)
    (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hflat : AlgebraicGeometry.Flat D.groupoid.source.left)
    (hfp : AlgebraicGeometry.LocallyOfFinitePresentation D.groupoid.source.left) :
    ∃ (U' : AlgebraicGeometry.AlgebraicSpaces C D.S hS)
      (g : U' ⟶ (D.groupoid.realization C hS hU hR hP).objects),
      U'.obj.IsRepresentable ∧
      AlgebraicGeometry.Space.IsEtale C D.S hS g.hom ∧
      AlgebraicGeometry.Space.IsSeparated C D.S hS g.hom ∧
      ∀ u' : AlgebraicGeometry.Space.points C D.S hS
          (restrict (D.groupoid.realization C hS hU hR hP) g).groupoid.objects.obj,
        IsQuasiSplitAt (restrict (D.groupoid.realization C hS hU hR hP) g).groupoid u'

AlgebraicGeometry.Space.exists_finitePartGroupoid_isRepresentable_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/More/SplittingSchemes.lean, line 85. The attribute's comment: “the finite part U' = (R_s/U, e)_fin is a scheme, U' ⟶ U is separated and étale, and R|_{U'} is quasi-split at every point of U'”.

Stacks 04RY, three of the four clauses of its conclusion. For a groupoid in algebraic spaces whose source and target are separated, whose source is flat and locally of finite presentation, whose target is locally of finite type and whose object space is a scheme, the finite part is a scheme, its projection to the object space is separated and étale, and the restriction along that projection is quasi-split at every point.

theorem exists_finitePartGroupoid_isRepresentable_isSeparated
    {C : BigFppfSite.{u}} {S : Scheme.{u}} {hS : C.Contains S}
    {B : AlgebraicSpaces C S hS} (G : GroupoidInAlgebraicSpaces C S hS B)
    (hs_sep : IsSeparated C S hS G.source.hom)
    (ht_sep : IsSeparated C S hS G.target.hom)
    (hs_flat : IsFlat C S hS G.source.hom)
    (hs_fp : IsLocallyOfFinitePresentation C S hS G.source.hom)
    (ht_lft : IsLocallyOfFiniteType C S hS G.target.hom)
    (hU : G.objects.obj.IsRepresentable) :
    ∃ F : FinitePartGroupoid G,
      F.groupoid.objects.obj.IsRepresentable ∧
      IsSeparated C S hS F.objectProjection.hom ∧
      IsEtale C S hS F.objectProjection.hom ∧
      ∀ u' : points C S hS
          (GroupoidInAlgebraicSpaces.restrict G F.objectProjection).groupoid.objects.obj,
        GroupoidInAlgebraicSpaces.IsQuasiSplitAt
          (GroupoidInAlgebraicSpaces.restrict G F.objectProjection).groupoid u'

Stacks.Groupoids.GroupoidScheme.exists_quasiSplit_separated_scheme_of_quasiSplittingSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasiSplittingEtaleScheme.lean, line 139. The attribute's comment: “ALL FOUR ASSERTIONS PRODUCED, in Situation 04RV with the source flat and locally of finite presentation: U' is a SCHEME (delivered as representability of the neighbourhood), U' -> U is SEPARATED as well as etale, there is a point u' of U' over u with k(u) = k(u') -- recorded both as a Spec k(u)-valued section v of U' over the canonical Spec k(u) -> U, and, on any scheme X' representing U' with any morphism of schemes X' -> U inducing g, as a point u' of X' with image u at which the residue field map is an ISOMORPHISM -- and R|_{U'} is QUASI-SPLIT over u'. Each of the four is constructed, none of them an input. The neighbourhood, the point and the quasi-splitting are Tag 04RW, proved in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasiSplittingEtaleLocalization.lean; the scheme-ness and the separatedness are Tags 04RI and 04RR applied to the finite part (R_s/U, e)_fin. Flatness and local finite presentation are required of the SOURCE alone, where the tag requires them of the target too, so these hypotheses are WEAKER than the tag's. Beyond Situation 04RV the remaining requirements are that the big fppf site contains the base, object, arrow and composable-pair schemes and Spec k(u), this library's standing ambient requirement”.

Stacks Project, Tag 04RY.

In the quasi-splitting situation of Stacks 04RV, with the source in addition flat and locally of finite presentation, there are a scheme U', a separated étale morphism g : U' ⟶ U, and a point u' of U' over u with κ(u) = κ(u'), such that R' = R|_{U'} is quasi-split over u'.

theorem exists_quasiSplit_separated_scheme_of_quasiSplittingSituation
    (D : AlgebraicGeometry.Space.QuasiSplittingSituation.{u})
    (C : AlgebraicGeometry.BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left)
    (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hK : C.Contains (Spec (D.groupoid.objects.left.residueField D.u)))
    (hflat : AlgebraicGeometry.Flat D.groupoid.source.left)
    (hfp : AlgebraicGeometry.LocallyOfFinitePresentation D.groupoid.source.left) :
    ∃ (U' : AlgebraicGeometry.AlgebraicSpaces C D.S hS)
      (g : U' ⟶ (D.groupoid.realization C hS hU hR hP).objects),
      U'.obj.IsRepresentable ∧
      AlgebraicGeometry.Space.IsEtale C D.S hS g.hom ∧
      AlgebraicGeometry.Space.IsSeparated C D.S hS g.hom ∧
      ∃ v : U'.obj.obj (Opposite.op
          (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK)),
        (yonedaSchemePointEquiv C hS hU (Opposite.op
            (schemeSiteObject C hS (X := residueOver D.groupoid D.u) hK))
            (g.hom.app _ v)).left =
          D.groupoid.objects.left.fromSpecResidueField D.u ∧
        IsQuasiSplitAt
          (restrict (D.groupoid.realization C hS hU hR hP) g).groupoid
          ((residueSectionValuedPoint D.groupoid C hS D.u hK U' v).class C D.S hS U'.obj) ∧
        ∀ (X' : AlgebraicGeometry.BigFppfOver C D.S hS) (ε : U'.obj ≅ yoneda.obj X')
          (gS : X' ⟶ schemeSiteObject C hS hU), yoneda.map gS = ε.inv ≫ g.hom →
          ∃ u' : (AlgebraicGeometry.BigFppfOver.toScheme C D.S hS).obj X',
            ((AlgebraicGeometry.BigFppfOver.toScheme C D.S hS).map gS).base u' = D.u ∧
            IsIso (((AlgebraicGeometry.BigFppfOver.toScheme C D.S hS).map
              gS).residueFieldMap u')
Tag 04RZ, a lemma

Tag 04RZ in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.exists_isAffine_isStronglySplitAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/StrongSplittingAffineLocalization.lean, line 982. The attribute's comment: “in Situation 04RL with s, t flat and locally of finite presentation and U affine: an affine scheme U'', an étale U'' ⟶ U and a point u'' over u with κ(u) = κ(u''), such that R|_{U''} is strongly split over u''. R|_{U''} is covered in its two-step reading, as the restriction to U'' of R' = R|_{U'} for the étale neighbourhood U' of Stacks 04RX, rather than as the restriction of R along the composite U'' ⟶ U' ⟶ U; the identification of the two is Stacks 04MW, which this library has as the comparison diagram doubleRestrictionDiagram and not as an identification of realizations. The conclusion is stronger than the tag in two respects: U'' ⟶ U' is an open immersion, not merely étale, and the strong splitting is produced for EVERY groupoid scheme realizing that restriction. Beyond Situation 04RL the hypotheses are that the big fppf site contains the base, object, arrow and composable-pair schemes and Spec κ(u), this library's standing ambient requirement”.

Stacks Project, Tag 04RZ.

In the strong splitting situation of Stacks 04RL, with s and t in addition flat and locally of finite presentation and with U affine, there are an affine scheme U'', an étale morphism U'' ⟶ U and a point u'' of U'' over u with κ(u) = κ(u''), such that the restriction of R to U'' is strongly split over u''.

The étale neighbourhood U' of Stacks 04RX is shrunk to an affine one: U'' is an invariant affine open of the object scheme of the strong splitting of R' = R|_{U'}, so U'' ⟶ U' is an open immersion and the restriction of that splitting to U'' is a strong splitting of R'|_{U''} over u''. The restriction is taken in two steps, as the restriction of R' to U''; its identification with the restriction of R along the composite U'' ⟶ U' ⟶ U is Stacks 04MW.

theorem exists_isAffine_isStronglySplitAt
    (D : AlgebraicGeometry.Space.StrongSplittingSituation.{u})
    (C : AlgebraicGeometry.BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left) (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hK : C.Contains (Spec (D.groupoid.objects.left.residueField D.u)))
    [IsAffine D.groupoid.objects.left]
    [Flat D.groupoid.source.left] [LocallyOfFinitePresentation D.groupoid.source.left]
    [Flat D.groupoid.target.left] [LocallyOfFinitePresentation D.groupoid.target.left] :
    ∃ (U' : Over D.S) (g : U' ⟶ D.groupoid.objects)
      (R' : AlgebraicGeometry.GroupoidScheme.Restriction D.groupoid g)
      (U'' : Over D.S) (j : U'' ⟶ R'.groupoid.objects) (u'' : U''.left),
      IsAffine U''.left ∧ IsOpenImmersion j.left ∧
      Etale (j ≫ R'.hom.mapObjects).left ∧
      (j ≫ R'.hom.mapObjects).left.base u'' = D.u ∧
      IsIso ((j ≫ R'.hom.mapObjects).left.residueFieldMap u'') ∧
      ∀ R'' : AlgebraicGeometry.GroupoidScheme.Restriction R'.groupoid j,
        IsStronglySplitAt R''.groupoid ((eqToHom R''.objects_eq.symm).left.base u'')
Tag 0DTE, a lemma

Tag 0DTE in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.exists_isAffine_isSplitAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/SplittingAffineLocalization.lean, line 789. The attribute's comment: “in Situation 0DTB with s, t flat and locally of finite presentation and U affine: an affine scheme U'', an étale U'' ⟶ U and a point u'' over u with κ(u) = κ(u''), such that R|_{U''} is SPLIT over u'' -- all of it PRODUCED: the neighbourhood, the point and the splitting are conclusions of this theorem, never inputs to it. Splitting is Stacks 04RK part (2) read for a groupoid scheme, stated in this file as Splitting: an open subscheme P of the arrow scheme which (a) is a groupoid scheme on the same object scheme, with composition the restriction of the ambient one, (b) has s|_P and t|_P finite, and (c) contains the arrow underlying every point of the stabilizer group scheme AlgebraicGeometry.stabilizer lying over the point; (a) and (b) are OpenFiniteSubgroupoid, which carries the 04RK attribute, and (c) is the field contains_stabilizer. The situation hypothesis is AlgebraicGeometry.Space.SplittingSituation, which carries the 0DTB attribute, and not the stronger StrongSplittingSituation of Tag 04RL. R|_{U''} is covered in its two-step reading, as the restriction to U'' of R' = R|_{U'} for the étale neighbourhood U' of Stacks 0DTD, rather than as the restriction of R along the composite U'' ⟶ U' ⟶ U; the identification of the two is Stacks 04MW, which this library has as the comparison diagram doubleRestrictionDiagram and not as an identification of realizations. The conclusion is stronger than the tag in two respects: U'' ⟶ U' is an open immersion, not merely étale, and the splitting is produced for EVERY groupoid scheme realizing that restriction. Beyond Situation 0DTB the hypotheses are that the big fppf site contains the base, object, arrow and composable-pair schemes and Spec κ(u), this library's standing ambient requirement”.

Stacks Project, Tag 0DTE.

In the splitting situation of Stacks 0DTB, with s and t in addition flat and locally of finite presentation and with U affine, there are an affine scheme U'', an étale morphism U'' ⟶ U and a point u'' of U'' over u with κ(u) = κ(u''), such that the restriction of R to U'' is split over u''.

The étale neighbourhood U' of Stacks 0DTD is shrunk to an affine one: U'' is an invariant affine open of the object scheme of the splitting of R' = R|_{U'}, so U'' ⟶ U' is an open immersion and the restriction of that splitting to U'' is a splitting of R'|_{U''} over u''. The restriction is taken in two steps, as the restriction of R' to U''; its identification with the restriction of R along the composite U'' ⟶ U' ⟶ U is Stacks 04MW.

theorem exists_isAffine_isSplitAt
    (D : AlgebraicGeometry.Space.SplittingSituation.{u})
    (C : AlgebraicGeometry.BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left) (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hK : C.Contains (Spec (D.groupoid.objects.left.residueField D.u)))
    [IsAffine D.groupoid.objects.left]
    [Flat D.groupoid.source.left] [LocallyOfFinitePresentation D.groupoid.source.left]
    [Flat D.groupoid.target.left] [LocallyOfFinitePresentation D.groupoid.target.left] :
    ∃ (U' : Over D.S) (g : U' ⟶ D.groupoid.objects)
      (R' : AlgebraicGeometry.GroupoidScheme.Restriction D.groupoid g)
      (U'' : Over D.S) (j : U'' ⟶ R'.groupoid.objects) (u'' : U''.left),
      IsAffine U''.left ∧ IsOpenImmersion j.left ∧
      Etale (j ≫ R'.hom.mapObjects).left ∧
      (j ≫ R'.hom.mapObjects).left.base u'' = D.u ∧
      IsIso ((j ≫ R'.hom.mapObjects).left.residueFieldMap u'') ∧
      ∀ R'' : AlgebraicGeometry.GroupoidScheme.Restriction R'.groupoid j,
        IsSplitAt R''.groupoid ((eqToHom R''.objects_eq.symm).left.base u'')
Tag 04S0, a lemma

Tag 04S0 in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.exists_isAffine_isQuasiSplitAt_of_quasiSplittingSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasiSplittingAffineLocalization.lean, line 92. The attribute's comment: “ALL ASSERTIONS, in Situation 04RV with U affine and with s and t flat and locally of finite presentation: the separated etale neighbourhood U' -> U, a groupoid scheme R' realizing R|_{U'}, an AFFINE open U'' of U' with a point u'' over u at which the residue field map is an ISOMORPHISM, and the QUASI-SPLITTING of R|_{U''} over u'' -- all PRODUCED. Stacks 04RY is invoked internally as exists_quasiSplit_separated_scheme_of_quasiSplittingSituation; its quasi-splitting is AlgebraicGeometry.GroupoidInAlgebraicSpaces.QuasiSplitting of the restriction of the REALIZATION, and it is converted to the groupoid-scheme notion Stacks.Groupoids.GroupoidScheme.QuasiSplitting by nonempty_openFiniteSubgroupoid_of_realization, which de-realizes the open finite subgroupoid. In two respects the conclusion is STRONGER than the tag: the morphism U'' -> U' is an open immersion, not merely etale, and the quasi-splitting is produced for EVERY groupoid scheme realizing the restriction. R|_{U''} is read both as the restriction of R along the composite U'' -> U' -> U, as the tag reads it, and as the restriction of R' to U''. Beyond Situation 04RV the only requirements are that the big fppf site contain the base, object, arrow and composable-pair schemes and Spec k(u), this library's standing ambient requirement”.

Stacks Project, Tag 04S0.

In the quasi-splitting situation of Stacks 04RV, with U affine and with s and t flat and locally of finite presentation, there are a separated étale neighbourhood U' ⟶ U, a groupoid scheme R' realizing the restriction R|_{U'}, an affine open U'' ⊆ U' and a point u'' of U'' over u with κ(u) = κ(u''), such that U'' ⟶ U is étale and R|_{U''} is quasi-split over u'' — both when R|_{U''} is read as the restriction of R' to U'' and when it is read, as the tag reads it, as the restriction of R along the composite U'' ⟶ U' ⟶ U.

Stacks 04RY supplies the neighbourhood and a quasi-splitting of the restriction of the realization of the groupoid scheme; the comparison with the groupoid-scheme notion is Stacks.Groupoids.GroupoidScheme.nonempty_openFiniteSubgroupoid_of_realization, and the shrinking to an affine neighbourhood is Stacks.Groupoids.GroupoidScheme.exists_isAffine_isQuasiSplitAt.

theorem exists_isAffine_isQuasiSplitAt_of_quasiSplittingSituation
    (D : AlgebraicGeometry.Space.QuasiSplittingSituation.{u})
    (C : AlgebraicGeometry.BigFppfSite.{u}) (hS : C.Contains D.S)
    (hU : C.Contains D.groupoid.objects.left)
    (hR : C.Contains D.groupoid.arrows.left)
    (hP : C.Contains (pullback D.groupoid.source D.groupoid.target).left)
    (hK : C.Contains (Spec (D.groupoid.objects.left.residueField D.u)))
    [IsAffine D.groupoid.objects.left]
    [Flat D.groupoid.source.left] [LocallyOfFinitePresentation D.groupoid.source.left]
    [Flat D.groupoid.target.left] [LocallyOfFinitePresentation D.groupoid.target.left]
    :
    ∃ (U' : Over D.S) (gp : U' ⟶ D.groupoid.objects)
      (R' : AlgebraicGeometry.GroupoidScheme.Restriction D.groupoid gp)
      (U'' : Over D.S) (j : U'' ⟶ R'.groupoid.objects) (u'' : U''.left),
      AlgebraicGeometry.IsSeparated gp.left ∧ Etale gp.left ∧
      IsAffine U''.left ∧ IsOpenImmersion j.left ∧
      Etale (j ≫ R'.hom.mapObjects).left ∧
      (j ≫ R'.hom.mapObjects).left.base u'' = D.u ∧
      IsIso ((j ≫ R'.hom.mapObjects).left.residueFieldMap u'') ∧
      (∀ R'' : AlgebraicGeometry.GroupoidScheme.Restriction R'.groupoid j,
        IsQuasiSplitAt R''.groupoid ((eqToHom R''.objects_eq.symm).left.base u'')) ∧
      ∀ R''' : AlgebraicGeometry.GroupoidScheme.Restriction D.groupoid
          (j ≫ R'.hom.mapObjects),
        IsQuasiSplitAt R'''.groupoid ((eqToHom R'''.objects_eq.symm).left.base u'')
Sources
LeanStacks.Groupoids.GroupoidScheme.isQuasiSplitAt_of_isLocallyArtinian_arrows · AlgebraicGeometry.GroupoidInAlgebraicSpaces.OpenFiniteSubgroupoid · AlgebraicGeometry.GroupoidInAlgebraicSpaces.identityPoint_hasCommonExtension · AlgebraicGeometry.GroupoidInAlgebraicSpaces.StrongSplitting · AlgebraicGeometry.GroupoidInAlgebraicSpaces.Splitting · AlgebraicGeometry.GroupoidInAlgebraicSpaces.QuasiSplitting · AlgebraicGeometry.GroupoidInAlgebraicSpaces.IsStronglySplitAt · AlgebraicGeometry.GroupoidInAlgebraicSpaces.IsSplitAt

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.