39.3 Equivalence relations to 39.22 Separation conditions

Section39.3 Equivalence relations#

Section 39.3 of the Stacks Project, Tag 022O. 5 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 022P, a definition

Tag 022P in the Stacks Project.

Stacks.Groupoids.PreRelation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EquivalenceRelations.lean, line 64. The attribute's comment: “part (1): pre-relation”.

Stacks 022P, part (1). A pre-relation from R to U over S is a morphism of S-schemes from R to the product U ×_S U.

abbrev PreRelation (R U : Over S)

Stacks.Groupoids.PreRelation.target, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EquivalenceRelations.lean, line 73. The attribute's comment: “part (1): target”.

Stacks 022P, part (1). The target map of a pre-relation, its composite with the first projection of the product.

noncomputable abbrev target : R ⟶ U

Stacks.Groupoids.PreRelation.source, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EquivalenceRelations.lean, line 78. The attribute's comment: “part (1): source”.

Stacks 022P, part (1). The source map of a pre-relation, its composite with the second projection of the product.

noncomputable abbrev source : R ⟶ U

Stacks.Groupoids.IsPreEquivalenceRelation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EquivalenceRelations.lean, line 91. The attribute's comment: “part (3): pre-equivalence relation”. References: SGA 3 IV (3.1), “pre-equiv. relation def”.

Stacks 022P, part (3). A pre-relation is a pre-equivalence relation when the relation it induces on the T-valued points of U is an equivalence relation for every scheme T over S.

abbrev IsPreEquivalenceRelation {R U : Over S} (j : PreRelation R U) : Prop

Declarations registered for the tag:

• CategoryTheory.Mono registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/EquivalenceRelations.lean, line 94 (StacksFrontier): “part (2): relation”. References: EGA IV (8.11.5.1); SGA 1 V (3.6); SGA 3 VIIB (2.4.1); SGA 3 VIII (3.4); SGA 4 I (10.4); SGA 4 II (3.2).
• CategoryTheory.IsEquivalenceRelation registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/EquivalenceRelations.lean, line 95 (StacksFrontier): “part (4): equivalence relation”. References: SGA 3 IV (3.1.1); SGA 4 I (10.9); SGA 4 IV (9.8.2).

Tag 02V8, a lemma

Tag 02V8 in the Stacks Project.

AlgebraicGeometry.PreRelation.restrict, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Relations/PreRelations.lean, line 292. The attribute's comment: “the restricted pre-relation”.

The restriction of a pre-relation along g.

noncomputable abbrev restrict (g : U' ⟶ U) :
    Stacks.Groupoids.PreRelation (restriction j g) U'

AlgebraicGeometry.PreRelation.isPreEquivalenceRelation_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Relations/PreRelations.lean, line 301. The attribute's comment: “preservation of pre-equivalence relations”.

Restriction preserves pre-equivalence relations.

theorem isPreEquivalenceRelation_restrict (g : U' ⟶ U)
    (hj : Stacks.Groupoids.IsPreEquivalenceRelation j) :
    Stacks.Groupoids.IsPreEquivalenceRelation (restrict j g)

AlgebraicGeometry.PreRelation.isEquivalenceRelation_restrict, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Relations/PreRelations.lean, line 325. The attribute's comment: “preservation of equivalence relations”.

Restriction preserves equivalence relations.

instance isEquivalenceRelation_restrict (g : U' ⟶ U)
    [hj : CategoryTheory.IsEquivalenceRelation j.target j.source] :
    CategoryTheory.IsEquivalenceRelation (restrict j g).target (restrict j g).source

Declarations registered for the tag:

• CategoryTheory.Limits.pullback.fst_of_mono registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/Relations/PreRelations.lean, line 296 (StacksFrontier): “preservation of relations”. References: EGA I (3.3.12), “more general”.

Tag 02V9, a definition

Tag 02V9 in the Stacks Project.

AlgebraicGeometry.PreRelation.restrict, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Relations/PreRelations.lean, line 292. The attribute's comment: “the restriction R|_{U'} of a pre-relation along U' -> U”.

The restriction of a pre-relation along g.

noncomputable abbrev restrict (g : U' ⟶ U) :
    Stacks.Groupoids.PreRelation (restriction j g) U'

Tag 022Q, a lemma

Tag 022Q in the Stacks Project.

AlgebraicGeometry.PreRelation.equivalence_sourceTargetRel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Relations/PreRelations.lean, line 225.

Stacks Project, Tag 022Q. A pre-equivalence relation induces an equivalence relation on the underlying points of the scheme.

theorem equivalence_sourceTargetRel {R U : Over S} (j : Stacks.Groupoids.PreRelation R U)
    (hj : Stacks.Groupoids.IsPreEquivalenceRelation j) :
    Equivalence (Function.SourceTargetRel j.source.left.base j.target.left.base)

Declarations registered for the tag:

• Function.SourceTargetRel, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/Relations/PreRelations.lean, line 131 (StacksFrontier): “the relation on points”.

Tag 0DT7, a lemma

Tag 0DT7 in the Stacks Project.

AlgebraicGeometry.isEquivalenceRelation_of_unramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/EquivalenceRelation/Unramified.lean, line 89.

Stacks Project, Tag 0DT7. An unramified pre-relation which is an equivalence relation on points over every algebraically closed field, and whose reflexivity, symmetry, and composition operations are represented by morphisms, is an equivalence relation.

theorem isEquivalenceRelation_of_unramified
    {S : Scheme.{u}} {R U : Over S} (j : PreRelation R U)
    [Unramified j.source.left] [Unramified j.target.left]
    (hpoints : ∀ (k : Type u) [Field k] [IsAlgClosed k]
      (p : Spec (.of k) ⟶ S),
      (Function.Injective (fun r : Over.mk p ⟶ R ↦ r ≫ j) ∧
        Equivalence (j.Rel (T := Over.mk p))))
    (e : U ⟶ R)
    (he_target : e ≫ j.target = 𝟙 U)
    (he_source : e ≫ j.source = 𝟙 U)
    (i : R ⟶ R)
    (hi_target : i ≫ j.target = j.source)
    (hi_source : i ≫ j.source = j.target)
    (c : pullback j.source j.target ⟶ R)
    (hc_target : c ≫ j.target = pullback.fst j.source j.target ≫ j.target)
    (hc_source : c ≫ j.source = pullback.snd j.source j.target ≫ j.source) :
    IsEquivalenceRelation j.target j.source

Sources

• Section 39.3, Tag 022O
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Groupoids.PreRelation · Stacks.Groupoids.PreRelation.target · Stacks.Groupoids.PreRelation.source · Stacks.Groupoids.IsPreEquivalenceRelation · CategoryTheory.Mono · CategoryTheory.IsEquivalenceRelation · AlgebraicGeometry.PreRelation.restrict · AlgebraicGeometry.PreRelation.isPreEquivalenceRelation_restrict

Section39.4 Group schemes#

Section 39.4 of the Stacks Project, Tag 022R. 5 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 022S, a definition

Tag 022S in the Stacks Project.

AlgebraicGeometry.GroupSchemeOverPoints, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Defs.lean, line 63. The attribute's comment: “a group scheme over S”.

Stacks Project, Tag 022S (1). A group scheme over S: a scheme G over S together with a multiplication morphism m : G ×_S G ⟶ G of schemes over S, such that for every scheme T over S the induced multiplication makes the set of T-valued points G(T) = Hom_{Over S}(T, G) into a group.

structure GroupSchemeOverPoints (S : Scheme.{u})

AlgebraicGeometry.GroupSchemeOverPoints.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Defs.lean, line 85. The attribute's comment: “morphisms of group schemes over S”. References: SGA 3 XI (2.1), “The value of M_H”; SGA 7 VII (2.9.6), “partial”.

Stacks Project, Tag 022S (2). A morphism ψ : (G, m) ⟶ (G', m') of group schemes over S: a morphism ψ : G ⟶ G' of schemes over S such that for every scheme T over S, the induced map ψ : G(T) ⟶ G'(T) is a homomorphism of groups.

structure Hom (G H : GroupSchemeOverPoints S)

Tag 022T, a lemma

Tag 022T in the Stacks Project.

AlgebraicGeometry.GroupScheme.grpObjPullbackObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/BaseChange.lean, line 92. References: SGA 3 VIA (0.4), “partial”.

Let (G, m) be a group scheme over S and f : S' ⟶ S a morphism of schemes. The pullback (G_{S'}, m_{S'}) is a group scheme over S'.

noncomputable instance grpObjPullbackObj : GrpObj ((Over.pullback f).obj G)

AlgebraicGeometry.GroupScheme.pointsMulEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/BaseChange.lean, line 123.

For every scheme T over S', the pair (G_{S'}(T), m_{S'}) is a group, and composition with the projection G ×_S S' ⟶ G identifies it with the group (G(T), m) of morphisms T ⟶ G over S.

noncomputable def pointsMulEquiv (T : Over S') :
    (T ⟶ (Over.pullback f).obj G) ≃* ((Over.map f).obj T ⟶ G)

Tag 047D, a definition

Tag 047D in the Stacks Project.

AlgebraicGeometry.ClosedSubgroupScheme, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Subgroups/Defs.lean, line 56. The attribute's comment: “part (1)”.

A closed subgroup scheme of G over S.

structure ClosedSubgroupScheme {S : Scheme.{u}} (G : Grp (Over S))

AlgebraicGeometry.OpenSubgroupScheme, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Subgroups/Defs.lean, line 66. The attribute's comment: “part (2)”.

An open subgroup scheme of G over S.

structure OpenSubgroupScheme {S : Scheme.{u}} (G : Grp (Over S))

Tag 0G8L, a lemma

Tag 0G8L in the Stacks Project.

AlgebraicGeometry.isClosedSubgroupScheme_iff_factor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Subgroups/Defs.lean, line 171. The attribute's comment: “part (1)”.

The factorization criterion for a closed subscheme to be a subgroup scheme.

theorem isClosedSubgroupScheme_iff_factor {S : Scheme.{u}}
    (G : Grp (Over S)) {H : Over S} (j : H ⟶ G.X)
    [AlgebraicGeometry.IsClosedImmersion j.left] :
    (∃ K : ClosedSubgroupScheme G,
      ∃ e : H ≅ K.carrier.X, j = e.hom ≫ K.ι.hom.hom) ↔
      ((∃ e : 𝟙_ (Over S) ⟶ H, e ≫ j = η[G.X]) ∧
       (∃ m : H ⊗ H ⟶ H, m ≫ j = (j ⊗ₘ j) ≫ μ[G.X]) ∧
       (∃ i : H ⟶ H, i ≫ j = j ≫ ι[G.X]))

AlgebraicGeometry.isOpenSubgroupScheme_iff_factor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Subgroups/Defs.lean, line 186. The attribute's comment: “part (2)”.

The factorization criterion for an open subscheme to be a subgroup scheme.

theorem isOpenSubgroupScheme_iff_factor {S : Scheme.{u}}
    (G : Grp (Over S)) {H : Over S} (j : H ⟶ G.X)
    [AlgebraicGeometry.IsOpenImmersion j.left] :
    (∃ K : OpenSubgroupScheme G,
      ∃ e : H ≅ K.carrier.X, j = e.hom ≫ K.ι.hom.hom) ↔
      ((∃ e : 𝟙_ (Over S) ⟶ H, e ≫ j = η[G.X]) ∧
       (∃ m : H ⊗ H ⟶ H, m ≫ j = (j ⊗ₘ j) ≫ μ[G.X]) ∧
       (∃ i : H ⟶ H, i ≫ j = j ≫ ι[G.X]))

Tag 047E, a definition

Tag 047E in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Smooth registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch39.lean, line 19 (StacksFrontier): “(1) smooth: Smooth G.hom for G a group object over S”. References: EGA IV (17.3.1); SGA 1 II (1.1); SGA 3 XI (1.1); SGA 3 XI (1.6); SGA 7 XIV (2.1), “partial”.
• AlgebraicGeometry.Flat registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch39.lean, line 21 (StacksFrontier): “(2) flat: Flat G.hom”. References: EGA 0 (6.7.1); EGA IV (2.1.1); SGA 3 III (2.0), “partial”; SGA 7 VII (1.3.8), “flatness of p”.
• AlgebraicGeometry.IsSeparated registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch39.lean, line 22 (StacksFrontier): “(3) separated: IsSeparated G.hom”. References: EGA I (5.4.1); EGA I (10.15.1), “Separated morphism X → S”.

Sources

• Section 39.4, Tag 022R
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.GroupSchemeOverPoints · AlgebraicGeometry.GroupSchemeOverPoints.Hom · AlgebraicGeometry.GroupScheme.grpObjPullbackObj · AlgebraicGeometry.GroupScheme.pointsMulEquiv · AlgebraicGeometry.ClosedSubgroupScheme · AlgebraicGeometry.OpenSubgroupScheme · AlgebraicGeometry.isClosedSubgroupScheme_iff_factor · AlgebraicGeometry.isOpenSubgroupScheme_iff_factor

Section39.5 Examples of group schemes#

Section 39.5 of the Stacks Project, Tag 047F. 6 tags here are carried by 56 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 022U, an example

Tag 022U in the Stacks Project.

AlgebraicGeometry.multiplicativeGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 86. The attribute's comment: “multiplicative_group_scheme_underlying_scheme”. References: SGA 3 I (4.3.2).

Stacks Project, Tag 022U. The underlying scheme of the multiplicative group over the integers is the spectrum of the Laurent polynomial ring ℤ[T, T⁻¹].

noncomputable abbrev multiplicativeGroup

AlgebraicGeometry.multiplicativeGroupCanonicallyOver, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 90. The attribute's comment: “multiplicative_group_scheme_underlying_scheme”.

The canonical structure morphism from the multiplicative group scheme to Spec ℤ.

noncomputable instance multiplicativeGroupCanonicallyOver :
    multiplicativeGroup.CanonicallyOver (Spec (.of ℤ))

AlgebraicGeometry.multiplicativeGroupMultiplication, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 124. The attribute's comment: “multiplication”.

Stacks Project, Tag 022U. Multiplication on the multiplicative group is the scheme morphism induced by T ↦ T ⊗ T on coordinate rings, after the canonical identification of the fibre product with the spectrum of the tensor product.

noncomputable def multiplicativeGroupMultiplication :
    pullback (multiplicativeGroup ↘ Spec (.of ℤ))
      (multiplicativeGroup ↘ Spec (.of ℤ)) ⟶ multiplicativeGroup

AlgebraicGeometry.unitsOfGlobalSections_representableBy_multiplicativeGroup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 219. The attribute's comment: “represents_units”. References: EGA IV (20.2.8), “Morphisms V → Spec Z[T”; SGA 3 I (4.3.2).

Stacks Project, Tag 022U. The functor assigning to a scheme the units in its ring of global sections is represented by the multiplicative group scheme Spec (ℤ[T, T⁻¹]).

theorem unitsOfGlobalSections_representableBy_multiplicativeGroup :
    Nonempty
      ((Scheme.Γ ⋙ forget₂ CommRingCat CommMonCat ⋙ CommMonCat.units ⋙
          forget CommGrpCat).RepresentableBy (multiplicativeGroupULift : Scheme.{u}))

AlgebraicGeometry.multiplicativeGroupGrpObj_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 263. The attribute's comment: “group_scheme”.

Stacks Project, Tag 022U. Multiplication in the multiplicative group scheme is the morphism induced by T ↦ T ⊗ T on Laurent polynomial coordinate rings.

theorem multiplicativeGroupGrpObj_mul :
    μ[multiplicativeGroup.asOver (Spec (.of ℤ))].left =
      multiplicativeGroupMultiplication

AlgebraicGeometry.multiplicativeGroupBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 274. The attribute's comment: “base_change”.

Stacks Project, Tag 022U. The multiplicative group over S is the base change of Spec (ℤ[T, T⁻¹]) along the unique morphism from S to Spec ℤ.

noncomputable abbrev multiplicativeGroupBaseChange (S : Scheme.{u}) : Scheme.{u}

AlgebraicGeometry.multiplicativeGroupBaseChangeGrpObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 446. The attribute's comment: “base_change”. References: SGA 3 I (4.3.2).

Stacks Project, Tag 022U. The base change of the multiplicative group to any scheme S is a group scheme over S. Its structure is induced by the specified representation of the group-valued global-units functor, and hence is not an arbitrary transported group law.

noncomputable instance multiplicativeGroupBaseChangeGrpObj (S : Scheme.{u}) :
    GrpObj (Scheme.asOver (multiplicativeGroupBaseChange S) S)

AlgebraicGeometry.baseChangePointsIsoMultiplicativeGroupPoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 456. The attribute's comment: “base_change”.

Stacks Project, Tag 022U. For every S-scheme T, the universal property of base change canonically identifies S-morphisms from T to the multiplicative group over S with scheme morphisms from T to the integral multiplicative group. The natural isomorphism records compatibility with every morphism of S-schemes.

noncomputable def baseChangePointsIsoMultiplicativeGroupPoints (S : Scheme.{u}) :
    yoneda.obj (Scheme.asOver (multiplicativeGroupBaseChange S) S) ≅
      (Over.forget S).op ⋙ yoneda.obj multiplicativeGroupULift

AlgebraicGeometry.baseChangePointsIsoMultiplicativeGroupPoints_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 490. The attribute's comment: “base_change”.

The forward map in AlgebraicGeometry.baseChangePointsIsoMultiplicativeGroupPoints is composition with the first pullback projection. This characterizes the isomorphism and its canonical orientation.

theorem baseChangePointsIsoMultiplicativeGroupPoints_hom_app
    (S : Scheme.{u}) (T : (Over S)ᵒᵖ)
    (f : T.unop ⟶ Scheme.asOver (multiplicativeGroupBaseChange S) S) :
    (baseChangePointsIsoMultiplicativeGroupPoints S).hom.app T f =
      f.left ≫ pullback.fst
        (multiplicativeGroupULift ↘ Spec (.of (ULift.{u} ℤ)))
        (specULiftZIsTerminal.from S)

AlgebraicGeometry.baseChangePointsIsoGlobalUnits, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 502. The attribute's comment: “base_change”. References: SGA 3 I (4.3.2), “G_{m,S}(T)=Γ(T,O_T)^*”.

Stacks Project, Tag 022U. The group of T-points of the multiplicative group over S is canonically the unit group Γ(T, 𝒪_T)ˣ, naturally in the S-scheme T.

noncomputable def baseChangePointsIsoGlobalUnits (S : Scheme.{u}) :
    yonedaGrpObj (Scheme.asOver (multiplicativeGroupBaseChange S) S) ≅ globalUnits S

AlgebraicGeometry.baseChangePointsIsoGlobalUnits_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 512. The attribute's comment: “base_change”.

The forward map in AlgebraicGeometry.baseChangePointsIsoGlobalUnits sends a point to the pullback of the Laurent coordinate along its composite with the first pullback projection. Besides characterizing the natural isomorphism, this pins down the multiplication on the group scheme as multiplication of global units.

theorem baseChangePointsIsoGlobalUnits_hom_app
    (S : Scheme.{u}) (T : (Over S)ᵒᵖ)
    (f : T.unop ⟶ Scheme.asOver (multiplicativeGroupBaseChange S) S) :
    (baseChangePointsIsoGlobalUnits S).hom.app T f =
    multiplicativeGroupPointUnit
        (f.left ≫ pullback.fst
          (multiplicativeGroupULift ↘ Spec (.of (ULift.{u} ℤ)))
          (specULiftZIsTerminal.from S))

Declarations registered for the tag:

• LaurentPolynomial.instHopfAlgebra registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 225 (StacksFrontier): “group_scheme”. References: EGA II (8.3.9), “partial, special case”; SGA 3 I (4.3.2), “special case”; SGA 3 VIIA (3.3), “special case”.
• AlgebraicGeometry.instGrpObjSpecAsOverSpec registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Multiplicative.lean, line 229 (StacksFrontier): “group_scheme”. References: SGA 3 I (4.2), “partial”; SGA 3 VIIA (3.3), “partial”; SGA 3 VIIA (3.3.0), “partial”; SGA 3 VIIB (2.1), “(i), special case”; SGA 3 VIIB (2.2.1), “partial”.
• AlgebraicGeometry.smooth_multiplicativeGroupULift, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/MultiplicativeSmooth.lean, line 51 (StacksFrontier): “the structure morphism is smooth”.

Tag 040M, an example

Tag 040M in the Stacks Project.

AlgebraicGeometry.rootsOfUnity, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/RootsOfUnity.lean, line 96. The attribute's comment: “roots_of_unity_scheme”. References: SGA 3 I (4.4.4), “μ_n = Spec Z[x]/(x^n-1)”; SGA 1 XI (6.1), “special case”.

Stacks Project, Tag 040M. The scheme of n-th roots of unity over the integers is Spec (ℤ[X] / (Xⁿ - 1)).

noncomputable abbrev rootsOfUnity (n : ℕ) : Scheme.{u}

AlgebraicGeometry.rootsOfUnityCanonicallyOver, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/RootsOfUnity.lean, line 101. The attribute's comment: “roots_of_unity_scheme”.

The canonical structure morphism from the scheme of roots of unity to the integer base.

noncomputable instance rootsOfUnityCanonicallyOver (n : ℕ) :
    (rootsOfUnity n).CanonicallyOver (Spec (.of (ULift.{u} ℤ)))

AlgebraicGeometry.rootsOfUnityBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/RootsOfUnity.lean, line 112. The attribute's comment: “roots_of_unity_scheme”. References: SGA 3 I (4.4.4), “μ_{n,S}”; SGA 1 XI (6.1); SGA 3 VIIB (2.5.2.A), “partial”.

Stacks Project, Tag 040M. The scheme of n-th roots of unity over S is the base change of the scheme of roots of unity over the integers along the unique map from S to the integer base.

noncomputable abbrev rootsOfUnityBaseChange (n : ℕ) (S : Scheme.{u}) : Scheme.{u}

AlgebraicGeometry.rootsOfUnitySections_representableBy_rootsOfUnity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/RootsOfUnity.lean, line 230. The attribute's comment: “representability”. References: SGA 1 XI (6.1), “special case”.

Stacks Project, Tag 040M. The functor of units in global sections whose n-th power is one is represented by Spec (ℤ[X] / (Xⁿ - 1)).

theorem rootsOfUnitySections_representableBy_rootsOfUnity (n : ℕ) (hn : 0 < n) :
    Nonempty ((rootsOfUnitySections n).RepresentableBy (rootsOfUnity n : Scheme.{u}))

AlgebraicGeometry.rootsOfUnityGrpObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/RootsOfUnity.lean, line 473. The attribute's comment: “group_scheme”. References: SGA 3 I (4.4.4).

The group-object structure on the scheme of positive-order roots of unity over the integers.

noncomputable instance rootsOfUnityGrpObj (n : ℕ) [Fact (0 < n)] :
    GrpObj (Over.mk (rootsOfUnity n ↘ Spec (.of (ULift.{u} ℤ))))

AlgebraicGeometry.rootsOfUnityGrpObj_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/RootsOfUnity.lean, line 481. The attribute's comment: “group_scheme”.

Stacks Project, Tag 040M. The scheme of n-th roots of unity is a group scheme over the integers, with multiplication induced by X ↦ X ⊗ X on coordinate rings.

theorem rootsOfUnityGrpObj_mul (n : ℕ) (hn : 0 < n) :
    (letI : Fact (0 < n) := ⟨hn⟩
    μ[Over.mk (rootsOfUnity n ↘ Spec (.of (ULift.{u} ℤ)))].left =
      rootsOfUnityMultiplication n)

AlgebraicGeometry.rootsOfUnitySectionsOver_representableBy_rootsOfUnityBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/RootsOfUnity.lean, line 651. The attribute's comment: “base_change_points”. References: SGA 1 XI (6.1); SGA 3 I (4.4.4); SGA 3 VIIA (4.1.4), “partial”.

Stacks Project, Tag 040M. For every scheme S, the base change to S of the scheme of n-th roots of unity represents, naturally in an S-scheme T, the units in Γ(T, 𝒪_T) whose n-th power is one. The representing universal element is the pullback of the polynomial coordinate X along the base-change projection.

theorem rootsOfUnitySectionsOver_representableBy_rootsOfUnityBaseChange
    (n : ℕ) (hn : 0 < n) (S : Scheme.{u}) :
    ((Over.forget S).op ⋙ rootsOfUnitySections n).IsRepresentedBy
      (rootsOfUnityBaseChangeUniversalRoot n hn S)

AlgebraicGeometry.rootsOfUnityGroupOverFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/RootsOfUnity.lean, line 73. The attribute's comment: “relative_functor_of_points”. References: SGA 1 XI (6.1); SGA 3 I (4.4.4); SGA 3 VIIA (4.1.4).

The group-valued functor on schemes over S whose value on T is the group of n-th roots of unity in Γ(T, 𝒪_T).

noncomputable abbrev rootsOfUnityGroupOverFunctor (n : ℕ) (S : Scheme.{u}) :
    (Over S)ᵒᵖ ⥤ GrpCat.{u}

AlgebraicGeometry.rootsOfUnityBaseChangeOverGrpObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/RootsOfUnity.lean, line 90. The attribute's comment: “base_change_group_scheme”. References: SGA 1 XI (6.1); SGA 3 I (4.4.4); SGA 3 VIIB (2.5.2.A), “more general”.

Stacks Project, Tag 040M. The base change of the group scheme of n-th roots of unity to a scheme S is a group scheme over S.

noncomputable instance rootsOfUnityBaseChangeOverGrpObj (n : ℕ) [Fact (0 < n)]
    (S : Scheme.{u}) : GrpObj (rootsOfUnityBaseChangeOver n S)

AlgebraicGeometry.rootsOfUnityBaseChangeGroupPointsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/Examples/RootsOfUnity.lean, line 127. The attribute's comment: “relative_functor_of_points”. References: SGA 3 I (4.4.4), “μ_n(T)={f : f^n=1}”; SGA 1 XI (6.1); SGA 3 VIIA (4.1.4), “partial”; SGA 3 VIIB (2.5.2.A), “more general”.

Stacks Project, Tag 040M. For every scheme S, the group-valued functor of points of the group scheme μₙ,S of n-th roots of unity is naturally isomorphic to the group of n-th roots of unity in the global sections of the varying S-scheme.

noncomputable def rootsOfUnityBaseChangeGroupPointsIso (n : ℕ) [Fact (0 < n)] (S : Scheme.{u}) :
    yonedaGrpObj (rootsOfUnityBaseChangeOver n S) ≅ rootsOfUnityGroupOverFunctor n S

Declarations registered for the tag:

• AlgebraicGeometry.Scheme.GrpObjAsOverPullback registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/RootsOfUnity.lean, line 548 (StacksFrontier): “base_change_group_scheme”.
• CategoryTheory.Functor.obj.μ_def registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/RootsOfUnity.lean, line 549 (StacksFrontier): “base_change_group_scheme”.

Tag 022V, an example

Tag 022V in the Stacks Project.

AlgebraicGeometry.additiveGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Additive.lean, line 83. The attribute's comment: “additive_group_underlying_scheme”. References: SGA 3 I (4.3.1), “the scheme G_a”.

Stacks Project, Tag 022V. The underlying scheme of the additive group over the integers is the spectrum of the polynomial ring ℤ[X].

noncomputable abbrev additiveGroup : Scheme.{u}

AlgebraicGeometry.additiveGroupCanonicallyOver, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Additive.lean, line 88. The attribute's comment: “additive_group_underlying_scheme”.

The canonical structure morphism from the additive group scheme to the spectrum of the universe-polymorphic copy of ℤ, induced by the inclusion of constant polynomials.

noncomputable instance additiveGroupCanonicallyOver :
    additiveGroup.CanonicallyOver (Spec (.of (ULift.{u} ℤ)))

AlgebraicGeometry.additionMorphism_pullbackSpecIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Additive.lean, line 117. The attribute's comment: “addition_morphism”. References: SGA 3 I (4.3.1), “Δ(T)=T⊗1+1⊗T”.

Stacks Project, Tag 022V. Under the canonical identification of the fibre product with Spec (R[X] ⊗[R] R[X]), addition is induced by the ring map sending X to X ⊗ 1 + 1 ⊗ X.

lemma additionMorphism_pullbackSpecIso :
    (pullbackSpecIso (ULift.{u} ℤ) (Polynomial (ULift.{u} ℤ))
      (Polynomial (ULift.{u} ℤ))).inv ≫ additionMorphism =
      Spec.map (CommRingCat.ofHom additionRingHom)

AlgebraicGeometry.additiveGroupGrpObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Additive.lean, line 125. The attribute's comment: “additive_group_scheme”.

The group-object structure on the affine line over the integers.

noncomputable instance additiveGroupGrpObj :
    GrpObj (Over.mk (additiveGroup ↘ Spec (.of (ULift.{u} ℤ))))

AlgebraicGeometry.additiveGroupGrpObj_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Additive.lean, line 156. The attribute's comment: “additive_group_scheme”.

Stacks Project, Tag 022V. Multiplication in the additive group scheme is the usual addition morphism.

theorem additiveGroupGrpObj_mul :
    μ[Over.mk (additiveGroup ↘ Spec (.of (ULift.{u} ℤ)))].left = additionMorphism

AlgebraicGeometry.additiveGroupBaseChangeGrpObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Additive.lean, line 167. The attribute's comment: “base_change_group_scheme”. References: SGA 3 I (4.3.1), “G_{a,S} group over S”.

Stacks Project, Tag 022V. The base change of the additive group scheme to every scheme S is a group scheme over S, with the canonical pullbacks of the integral group operations.

noncomputable instance additiveGroupBaseChangeGrpObj (S : Scheme.{u}) :
    GrpObj (Scheme.asOver (additiveGroupBaseChange S) S)

AlgebraicGeometry.globalSections_representableBy_additiveGroup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Additive.lean, line 380. The attribute's comment: “representability”. References: SGA 3 I (4.3.1), “partial”.

Stacks Project, Tag 022V. The set-valued global-sections functor on schemes is represented by the additive group scheme Spec (ℤ[X]).

theorem globalSections_representableBy_additiveGroup :
    Nonempty ((Scheme.Γ ⋙ forget CommRingCat).RepresentableBy (additiveGroup : Scheme.{u}))

AlgebraicGeometry.additiveGroupBaseChangePointsIsoGlobalSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Additive.lean, line 535. The attribute's comment: “relative_functor_of_points”. References: SGA 3 I (4.3.1), “more general”.

Stacks Project, Tag 022V. For every scheme S, the group-valued functor of points of the additive group scheme over S is naturally isomorphic to the additive group of global sections of the varying S-scheme.

noncomputable def additiveGroupBaseChangePointsIsoGlobalSections (S : Scheme.{u}) :
    yonedaGrpObj (Scheme.asOver (additiveGroupBaseChange S) S) ≅ globalSectionsAdditive S

AlgebraicGeometry.additiveGroupBaseChangePointsIsoGlobalSections_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Additive.lean, line 551. The attribute's comment: “relative_functor_of_points”.

Under the canonical identification of additive-group points with global sections, a point is sent to the pullback of the universal polynomial coordinate along its projection to the integral additive group. This characterizes the natural isomorphism.

theorem additiveGroupBaseChangePointsIsoGlobalSections_hom_app
    (S : Scheme.{u}) (T : (Over S)ᵒᵖ)
    (f : T.unop ⟶ Scheme.asOver (additiveGroupBaseChange S) S) :
    (additiveGroupBaseChangePointsIsoGlobalSections S).hom.app T f =
      additiveGroupPointSection
        (f.left ≫ pullback.fst
          (additiveGroup ↘ Spec (.of (ULift.{u} ℤ)))
          (specULiftZIsTerminal.from S))

Tag 022W, an example

Tag 022W in the Stacks Project.

AlgebraicGeometry.generalLinearScheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/GeneralLinear.lean, line 97. The attribute's comment: “general_linear_scheme”.

The general linear scheme GL_n over the integers.

noncomputable abbrev generalLinearScheme (n : ℕ) : Scheme.{u}

AlgebraicGeometry.generalLinearGroup_representableBy_generalLinearScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/GeneralLinear.lean, line 287. The attribute's comment: “representability”. References: SGA 3 XX (5.1), “special case”.

Stacks Project, Tag 022W. The functor of invertible n by n matrices over global sections is represented by the general linear scheme GL_n.

theorem generalLinearGroup_representableBy_generalLinearScheme (n : ℕ) :
    Nonempty ((generalLinearGroupFunctor.{u} n ⋙ forget GrpCat).RepresentableBy
      (generalLinearScheme.{u} n))

AlgebraicGeometry.generalLinearSchemeGrpObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/GeneralLinear.lean, line 331. The attribute's comment: “multiplication”.

Stacks Project, Tag 022W. The general linear scheme over the integers is a group scheme.

noncomputable instance generalLinearSchemeGrpObj (n : ℕ) :
    GrpObj (Over.mk (generalLinearStructureMorphism.{u} n))

AlgebraicGeometry.exists_multiplicationRingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/GeneralLinear.lean, line 420. The attribute's comment: “multiplication”.

Stacks Project, Tag 022W. Multiplication on the general linear scheme is induced by the coordinate-ring homomorphism sending xᵢⱼ to ∑ k, xᵢₖ ⊗ xₖⱼ.

theorem exists_multiplicationRingHom (n : ℕ) :
    ∃ f : generalLinearCoordinateRing.{u} n →+* generalLinearTensorSquare.{u} n,
      ((pullbackSpecIso (ULift.{u} ℤ) (generalLinearCoordinateRing.{u} n)
          (generalLinearCoordinateRing.{u} n)).inv ≫
          μ[Over.mk (generalLinearStructureMorphism.{u} n)].left =
            Spec.map (CommRingCat.ofHom f)) ∧
        ∀ i j : Fin n,
          f (algebraMap (MvPolynomial (Fin n × Fin n) (ULift.{u} ℤ))
              (generalLinearCoordinateRing.{u} n) (MvPolynomial.X (i, j))) =
            ∑ k : Fin n,
          @TensorProduct.tmul (ULift.{u} ℤ) CommRing.toCommSemiring
                (generalLinearCoordinateRing.{u} n) (generalLinearCoordinateRing.{u} n)
                CommRing.toCommSemiring.toAddCommMonoid
                CommRing.toCommSemiring.toAddCommMonoid
                Algebra.toModule Algebra.toModule
                (algebraMap (MvPolynomial (Fin n × Fin n) (ULift.{u} ℤ))
                  (generalLinearCoordinateRing.{u} n) (MvPolynomial.X (i, k)))
                (algebraMap (MvPolynomial (Fin n × Fin n) (ULift.{u} ℤ))
                  (generalLinearCoordinateRing.{u} n) (MvPolynomial.X (k, j)))

AlgebraicGeometry.generalLinearBaseChange, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/GeneralLinear.lean, line 488. The attribute's comment: “base_change”.

The general linear group scheme over S, obtained by base change from Spec ℤ.

noncomputable abbrev generalLinearBaseChange (n : ℕ) (S : Scheme.{u}) : Over S

AlgebraicGeometry.baseChangePointsIsoGeneralLinearPoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/GeneralLinear.lean, line 524. The attribute's comment: “base_change”.

Points of the base change are naturally points of the integral general linear scheme.

noncomputable def baseChangePointsIsoGeneralLinearPoints (n : ℕ) (S : Scheme.{u}) :
    yoneda.obj (generalLinearBaseChange n S) ≅
      (Over.forget S).op ⋙ yoneda.obj (generalLinearScheme n)

AlgebraicGeometry.baseChangePointsIsoGeneralLinearPoints_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/GeneralLinear.lean, line 545. The attribute's comment: “base_change”.

The pointwise map of the base-change comparison is composition with the first projection.

theorem baseChangePointsIsoGeneralLinearPoints_hom_app (n : ℕ) (S : Scheme.{u})
    (T : (Over S)ᵒᵖ) (f : T.unop ⟶ generalLinearBaseChange n S) :
    (baseChangePointsIsoGeneralLinearPoints n S).hom.app T f =
      f.left ≫ pullback.fst (generalLinearStructureMorphism.{u} n)
        (specULiftZIsTerminal.from S)

AlgebraicGeometry.generalLinearBaseChangeGrpObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/GeneralLinear.lean, line 554. The attribute's comment: “base_change”.

Base change preserves the group-scheme structure of the general linear group.

noncomputable instance generalLinearBaseChangeGrpObj (n : ℕ) (S : Scheme.{u}) :
    GrpObj (generalLinearBaseChange n S)

AlgebraicGeometry.baseChangeGroupPointsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/GeneralLinear.lean, line 658. The attribute's comment: “base_change”. References: SGA 3 I (4.5), “GL_n representability”.

The group-valued points of the base-changed scheme are invertible matrices over global sections, naturally in the scheme over S.

noncomputable def baseChangeGroupPointsIso (n : ℕ) (S : Scheme.{u}) :
    yonedaGrpObj (generalLinearBaseChange n S) ≅ generalLinearGroupOverFunctor n S

AlgebraicGeometry.baseChangeGroupPointsIso_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/GeneralLinear.lean, line 672. The attribute's comment: “base_change”.

The canonical comparison sends an S-point to the invertible matrix obtained by pulling back the generic coordinates from the integral general linear scheme.

theorem baseChangeGroupPointsIso_hom_app (n : ℕ) (S : Scheme.{u})
    (T : (Over S)ᵒᵖ) (f : T.unop ⟶ generalLinearBaseChange n S) (i j : Fin n) :
    ((baseChangeGroupPointsIso n S).hom.app T f).val i j =
      (Scheme.Γ.map
        (f.left ≫ pullback.fst (generalLinearStructureMorphism.{u} n)
          (specULiftZIsTerminal.from S)).op).hom (generalLinearCoordinateSection n i j)

Tag 022X, an example

Tag 022X in the Stacks Project.

AlgebraicGeometry.generalLinearSchemeGrpObjOverIntegers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Determinant.lean, line 92. The attribute's comment: “det_over_integers”.

The group scheme structure of GLₙ over the integers.

noncomputable instance generalLinearSchemeGrpObjOverIntegers (n : ℕ) :
    GrpObj (Over.mk (generalLinearStructureMorphismOverIntegers n))

AlgebraicGeometry.generalLinearSchemeGrpObjOverIntegers_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Determinant.lean, line 280. The attribute's comment: “det_over_integers”.

Multiplication on GLₙ is matrix multiplication, on generic matrix entries.

theorem generalLinearSchemeGrpObjOverIntegers_mul (n : ℕ) :
    ∃ m : generalLinearCoordinateRing.{0} n →+* generalLinearTensorSquareOverIntegers n,
      (pullbackSpecIso ℤ (generalLinearCoordinateRing.{0} n)
        (generalLinearCoordinateRing.{0} n)).inv ≫
          μ[Over.mk (generalLinearStructureMorphismOverIntegers n)].left =
            Spec.map (CommRingCat.ofHom m) ∧
      (∀ i j : Fin n,
        m (algebraMap (MvPolynomial (Fin n × Fin n) (ULift.{0} ℤ))
          (generalLinearCoordinateRing.{0} n) (MvPolynomial.X (i, j))) =
          ∑ k : Fin n,
          @TensorProduct.tmul ℤ CommRing.toCommSemiring
              (generalLinearCoordinateRing.{0} n) (generalLinearCoordinateRing.{0} n)
              CommRing.toCommSemiring.toAddCommMonoid CommRing.toCommSemiring.toAddCommMonoid
              Algebra.toModule Algebra.toModule
              (algebraMap (MvPolynomial (Fin n × Fin n) (ULift.{0} ℤ))
                (generalLinearCoordinateRing.{0} n) (MvPolynomial.X (i, k)))
                (algebraMap (MvPolynomial (Fin n × Fin n) (ULift.{0} ℤ))
                  (generalLinearCoordinateRing.{0} n) (MvPolynomial.X (k, j))))

AlgebraicGeometry.determinantGroupSchemeMorphismOverIntegers, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Determinant.lean, line 554. The attribute's comment: “det_over_integers”.

The determinant as a morphism of group schemes over Spec ℤ.

noncomputable def determinantGroupSchemeMorphismOverIntegers (n : ℕ) :
    Grp.mk (Over.mk (generalLinearStructureMorphismOverIntegers n)) ⟶
      Grp.mk (multiplicativeGroup.asOver (Spec (.of ℤ)))

AlgebraicGeometry.determinantGroupSchemeMorphismOverIntegers_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Determinant.lean, line 563. The attribute's comment: “det_over_integers”.

On coordinate rings, determinant sends the Laurent variable to the generic determinant.

theorem determinantGroupSchemeMorphismOverIntegers_spec (n : ℕ) :
    ∃ g : LaurentPolynomial ℤ →+* generalLinearCoordinateRing.{0} n,
      (determinantGroupSchemeMorphismOverIntegers n).hom.hom.left =
        Spec.map (CommRingCat.ofHom g) ∧
        g (LaurentPolynomial.T 1) =
          algebraMap (MvPolynomial (Fin n × Fin n) (ULift.{0} ℤ))
            (generalLinearCoordinateRing.{0} n) (generalLinearDeterminant.{0} n)

AlgebraicGeometry.determinantGroupSchemeMorphismOverULiftIntegers, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/DeterminantBaseChange.lean, line 207. The attribute's comment: “det_after_base_change”.

The determinant morphism of group schemes over the universe-lifted integers.

noncomputable def determinantGroupSchemeMorphismOverULiftIntegers (n : ℕ) :
    Grp.mk (Over.mk (generalLinearStructureMorphism.{u} n)) ⟶
      Grp.mk (multiplicativeGroupULift.asOver (Spec (.of (ULift.{u} ℤ))))

AlgebraicGeometry.determinantGroupSchemeMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/DeterminantBaseChange.lean, line 245. The attribute's comment: “det_after_base_change”.

The determinant morphism from the base-changed general linear group scheme to the base-changed multiplicative group scheme.

noncomputable def determinantGroupSchemeMorphism (n : ℕ) (S : Scheme.{u}) :
    Grp.mk (generalLinearBaseChange n S) ⟶
      Grp.mk (Scheme.asOver (multiplicativeGroupBaseChange S) S)

AlgebraicGeometry.determinantGroupSchemeMorphism_isBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/DeterminantBaseChange.lean, line 283. The attribute's comment: “det_after_base_change”.

The underlying scheme morphism is the pullback of the universal determinant over the universe-lifted integers, for every base scheme in that universe.

theorem determinantGroupSchemeMorphism_isBaseChange (n : ℕ) (S : Scheme.{u}) :
    (determinantGroupSchemeMorphism n S).hom.hom =
      (Over.pullback (specULiftZIsTerminal.from S)).map
        (determinantGroupSchemeMorphismOverULiftIntegers n).hom.hom

AlgebraicGeometry.determinantGroupSchemeMorphism_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/DeterminantBaseChange.lean, line 319. The attribute's comment: “det_after_base_change”.

The base-changed determinant sends an invertible matrix over the global sections of an S-scheme to its determinant, viewed as a global unit.

theorem determinantGroupSchemeMorphism_apply (n : ℕ) (S : Scheme.{u})
    (T : (Over S)ᵒᵖ) (f : T.unop ⟶ generalLinearBaseChange n S) :
    (baseChangePointsIsoGlobalUnits S).hom.app T
        (((yonedaGrp.map (determinantGroupSchemeMorphism n S)).app T) f) =
      Matrix.GeneralLinearGroup.det ((baseChangeGroupPointsIso n S).hom.app T f)

AlgebraicGeometry.determinantGroupSchemeMorphism_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/DeterminantBaseChange.lean, line 373. The attribute's comment: “det_after_base_change”.

After projecting the base-changed morphism to the integral models, it is the integral determinant morphism. The coefficient map compares ℤ with ULift ℤ.

theorem determinantGroupSchemeMorphism_baseChange (n : ℕ) (S : Scheme.{0}) :
    (determinantGroupSchemeMorphism n S).hom.hom.left ≫
        pullback.fst (multiplicativeGroupULift ↘ Spec (.of (ULift.{0} ℤ)))
          (specULiftZIsTerminal.from S) ≫
        Spec.map (CommRingCat.ofHom
          (AddMonoidAlgebra.mapRingHom ℤ
            (ULift.ringEquiv.{0, 0}.symm.toRingHom : ℤ →+* ULift.{0} ℤ))) =
      pullback.fst (generalLinearStructureMorphism.{0} n) (specULiftZIsTerminal.from S) ≫
        (determinantGroupSchemeMorphismOverIntegers n).hom.hom.left

Tag 03YW, an example

Tag 03YW in the Stacks Project.

AlgebraicGeometry.constantSchemeOverIntegers, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Constant.lean, line 84. The attribute's comment: “constant_group_scheme_construction”.

The scheme G_{Spec ℤ}, before equipping it with its group structure.

abbrev constantSchemeOverIntegers (G : Type v) [Small.{u} G] : Scheme.{u}

AlgebraicGeometry.constantGroupSchemeStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Constant.lean, line 342. The attribute's comment: “constant_group_scheme_construction”.

The group-object structure on the coproduct of copies of Spec ℤ indexed by G, whose multiplication sends the component (g, h) to the component g * h.

def constantGroupSchemeStructure (G : Type v) [Small.{u} G] [Group G] :
    { s : GrpObj (constantSchemeOverIntegersObj G) // IsConstantGroupSchemeStructure G s }

AlgebraicGeometry.constantGroupScheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Constant.lean, line 353. The attribute's comment: “constant_group_scheme_construction”. References: SGA 3 VIII (1.0.3).

The constant group scheme G_S, obtained by base-changing G_{Spec ℤ} to S.

abbrev constantGroupScheme (G : Type v) [Small.{u} G] [Group G] (S : Scheme.{u}) :
    Grp (Over S)

AlgebraicGeometry.constantSchemeOverIntegersPointsIsoLocallyConstantMaps, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Constant.lean, line 665. The attribute's comment: “representability_over_integers”. References: SGA 3 I (1.8), “special case”; SGA 3 VIII (1.3), “special case”; SGA 3 VIII (1.4), “special case”.

The canonical group-valued functor-of-points isomorphism for the constant group scheme over Spec ℤ.

def constantSchemeOverIntegersPointsIsoLocallyConstantMaps (G : Type v) [Small.{u} G] [Group G] :
    (yonedaGrp.obj (⟨constantSchemeOverIntegersObj G⟩ : Grp (Over (⊤_ Scheme.{u}))) ⋙
      GrpCat.uliftFunctor.{v}) ≅ locallyConstantMapsOverIntegers G

AlgebraicGeometry.constantSchemeOverIntegersPointsIsoLocallyConstantMaps_component, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Constant.lean, line 673. The attribute's comment: “representability_over_integers”.

The canonical isomorphism sends the inclusion of the component indexed by g to the constant function with value g.

theorem constantSchemeOverIntegersPointsIsoLocallyConstantMaps_component
    (G : Type v) [Small.{u} G] [Group G] (g : G) :
    ((constantSchemeOverIntegersPointsIsoLocallyConstantMaps G).hom.app
      (Opposite.op (Over.mk (𝟙 (⊤_ Scheme.{u})))))
        (ULift.up (constantComponent G g)) = LocallyConstant.const (⊤_ Scheme.{u}) g

AlgebraicGeometry.locallyConstantMaps_representableBy_constantSchemeOverIntegers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Constant.lean, line 685. The attribute's comment: “representability_over_integers”. References: SGA 3 VIII (1.3), “partial”.

The functor assigning to a scheme the group of locally constant maps to G is represented by the underlying scheme of the constant group scheme over Spec ℤ.

theorem locallyConstantMaps_representableBy_constantSchemeOverIntegers
    (G : Type v) [Small.{u} G] [Group G] :
    Nonempty ((locallyConstantMaps G ⋙ forget GrpCat).RepresentableBy
      (constantSchemeOverIntegers G))

AlgebraicGeometry.constantGroupSchemePointsIsoLocallyConstantMaps, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/Constant.lean, line 819. The attribute's comment: “relative_functor_of_points”. References: SGA 3 I (1.8), “special case”; SGA 3 VIII (1.3), “partial”; SGA 3 VIII (1.4), “partial”.

The group-valued functor of points of the constant group scheme G_S is naturally isomorphic to the functor of locally constant G-valued maps. Under this isomorphism multiplication is pointwise multiplication of functions.

def constantGroupSchemePointsIsoLocallyConstantMaps (G : Type v) [Small.{u} G] [Group G]
    (S : Scheme.{u}) :
    (yonedaGrp.obj (constantGroupScheme G S) ⋙ GrpCat.uliftFunctor.{v}) ≅
      locallyConstantMapsOver G S

Sources

• Section 39.5, Tag 047F
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.multiplicativeGroup · AlgebraicGeometry.multiplicativeGroupCanonicallyOver · AlgebraicGeometry.multiplicativeGroupMultiplication · AlgebraicGeometry.unitsOfGlobalSections_representableBy_multiplicativeGroup · AlgebraicGeometry.multiplicativeGroupGrpObj_mul · AlgebraicGeometry.multiplicativeGroupBaseChange · AlgebraicGeometry.multiplicativeGroupBaseChangeGrpObj · AlgebraicGeometry.baseChangePointsIsoMultiplicativeGroupPoints

Section39.6 Properties of group schemes#

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

Tag 047G, a lemma

Tag 047G in the Stacks Project.

AlgebraicGeometry.isSeparated_iff_isClosedImmersion_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Subgroups/Separation.lean, line 88. The attribute's comment: “separated_iff_identity_closed”. References: SGA 3 VIB (5.1).

A group scheme is separated over its base if and only if its identity section is a closed immersion.

theorem isSeparated_iff_isClosedImmersion_one {S G : Scheme.{u}} (f : G ⟶ S)
    [GrpObj (Over.mk f)] :
    IsSeparated f ↔ IsClosedImmersion (η[Over.mk f]).left

AlgebraicGeometry.quasiSeparated_iff_quasiCompact_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Subgroups/Separation.lean, line 101. The attribute's comment: “quasi_separated_iff_identity_quasi_compact”.

A group scheme is quasi-separated over its base if and only if its identity section is quasi-compact.

theorem quasiSeparated_iff_quasiCompact_one {S G : Scheme.{u}} (f : G ⟶ S)
    [GrpObj (Over.mk f)] :
    QuasiSeparated f ↔ QuasiCompact η[Over.mk f].left

Tag 047H, a lemma

Tag 047H in the Stacks Project.

AlgebraicGeometry.flat_mul_after_map, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Subgroups/Flatness.lean, line 51. The attribute's comment: “translation”.

Stacks Project, Tag 047H. Left translation parametrized by a flat scheme is flat.

lemma flat_mul_after_map {S : Scheme.{u}} (G T : Over S) [GrpObj G]
    (ψ : T ⟶ G) [Flat T.hom] :
    Flat (lift (fst T G ≫ ψ) (snd T G) ≫ μ[G]).left

AlgebraicGeometry.flat_mul, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Subgroups/Flatness.lean, line 77. The attribute's comment: “multiplication”. References: SGA 3 XVIII (2.2).

Stacks Project, Tag 047H. Multiplication on a flat group scheme is flat.

lemma flat_mul {S : Scheme.{u}} (G : Over S) [GrpObj G] [Flat G.hom] :
    Flat μ[G].left

Tag 047I, a lemma

Tag 047I in the Stacks Project.

AlgebraicGeometry.GroupSchemeDifferentials.relativeDifferentialsIsoPullbackIdentity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Differentials.lean, line 149. The attribute's comment: “the composite Ω_{G/S} ≅ f^e^Ω_{G/S} of the chain of isomorphisms”. References: SGA 3 II (4.11.4), “(a)”.

The canonical isomorphism Ω_{G/S} ≅ f^*e^*Ω_{G/S}. The sheaf of relative differentials of a group scheme is the inverse image of its restriction along the identity section.

noncomputable def relativeDifferentialsIsoPullbackIdentity :
    relativeDifferentials f ≅
      (Scheme.Modules.pullback f).obj
        ((Scheme.Modules.pullback (identity f)).obj (relativeDifferentials f))

AlgebraicGeometry.GroupSchemeDifferentials.pullbackConormalIsoPullbackIdentity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Differentials.lean, line 191. The attribute's comment: “the second isomorphism of the chain, f^𝒞_{S/G} ≅ f^e^Ω_{G/S}, where 𝒞_{S/G} is the conormal sheaf of the identity section e: f^ of the first arrow of the conormal sequence of e, an isomorphism by Tag 0474”.

The second isomorphism of the chain, f^*𝒞_{S/G} ≅ f^*e^*Ω_{G/S}, where 𝒞_{S/G} is the conormal sheaf of the identity section e: the inverse image along f of conormalIsoPullbackIdentity, that is, of the first arrow 𝒞_{S/G} ⟶ e^*Ω_{G/S} of the conormal sequence of e.

noncomputable def pullbackConormalIsoPullbackIdentity :
    (Scheme.Modules.pullback f).obj
        (Stacks.AlgebraicGeometry.RegularIdealSheaf.conormalSheaf (identity f) : S.Modules) ≅
      (Scheme.Modules.pullback f).obj
        ((Scheme.Modules.pullback (identity f)).obj (relativeDifferentials f))

AlgebraicGeometry.GroupSchemeDifferentials.relativeDifferentialsIsoPullbackConormal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Differentials.lean, line 203. The attribute's comment: “the first isomorphism of the chain, Ω_{G/S} ≅ f^*𝒞_{S/G}, where 𝒞_{S/G} is the conormal sheaf of the identity section e”.

The first isomorphism of the chain, Ω_{G/S} ≅ f^*𝒞_{S/G}, where 𝒞_{S/G} is the conormal sheaf of the identity section e: the shearing isomorphism Ω_{G/S} ≅ f^*e^*Ω_{G/S} followed by the inverse of pullbackConormalIsoPullbackIdentity.

noncomputable def relativeDifferentialsIsoPullbackConormal :
    relativeDifferentials f ≅
      (Scheme.Modules.pullback f).obj
        (Stacks.AlgebraicGeometry.RegularIdealSheaf.conormalSheaf (identity f) : S.Modules)

AlgebraicGeometry.GroupSchemeDifferentials.exists_free_iso_relativeDifferentials_of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Differentials.lean, line 233. The attribute's comment: “freeness over a field”. References: SGA 3 II (4.11.4), “(a) over a field”.

Freeness over a field. If the base is the spectrum of a field, the sheaf of relative differentials of a group scheme is a free 𝒪_G-module.

theorem exists_free_iso_relativeDifferentials_of_field (k : Type u) [Field k] (G : Scheme.{u})
    (f : G ⟶ Spec (CommRingCat.of k)) [GrpObj (Over.mk f)] :
    ∃ I : Type u,
      Nonempty (relativeDifferentials f ≅
        SheafOfModules.free (R := G.ringCatSheaf) I)

Tag 0BF5, a lemma

Tag 0BF5 in the Stacks Project.

AlgebraicGeometry.tangentMap_mul_at_identity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/TangentIdentity.lean, line 513.

Stacks Project, Tag 0BF5. The differential of group-scheme multiplication at the identity is addition of relative tangent vectors.

theorem tangentMap_mul_at_identity {S : Scheme.{u}} (G : Over S) [GrpObj G]
    (s : S) :
    let e : G.left := (η[G]).left s
    let m : pullback G.hom G.hom ⟶ G.left :=
      (Over.tensorObj_left G G) ▸ (μ[G]).left
    let z : ↑(pullback G.hom G.hom) :=
      (Over.tensorObj_left G G) ▸ ((lift (η[G]) (η[G])).left s)
    ∃ (h₁ : (pullback.fst G.hom G.hom) z = e)
      (h₂ : (pullback.snd G.hom G.hom) z = e)
      (hm : m z = e)
      (hbase : m ≫ G.hom = pullback.fst G.hom G.hom ≫ G.hom)
      (_ : IsIso (G.hom.residueFieldMap ((pullback.fst G.hom G.hom) z)))
      (_ : IsIso (G.hom.residueFieldMap ((pullback.snd G.hom G.hom) z)))
      (_ : IsIso (m.residueFieldMap z)),
      have : IsIso (G.hom.residueFieldMap ((pullback.fst G.hom G.hom) z)) :=
        ‹IsIso (G.hom.residueFieldMap ((pullback.fst G.hom G.hom) z))›
      have : IsIso (G.hom.residueFieldMap ((pullback.snd G.hom G.hom) z)) :=
        ‹IsIso (G.hom.residueFieldMap ((pullback.snd G.hom G.hom) z))›
      have : IsIso (m.residueFieldMap z) :=
        ‹IsIso (m.residueFieldMap z)›
      ∀ v w : DottedTangentArrow G.hom e,
        hm ▸ tangentMap m
          (pullback.fst G.hom G.hom ≫ G.hom) G.hom hbase z
          ((tangentSpaceProductEquiv G.hom G.hom z).toLinearEquiv.symm
            (h₁.symm ▸ v, h₂.symm ▸ w)) = v + w

Sources

• Section 39.6, Tag 045W
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isSeparated_iff_isClosedImmersion_one · AlgebraicGeometry.quasiSeparated_iff_quasiCompact_one · AlgebraicGeometry.flat_mul_after_map · AlgebraicGeometry.flat_mul · AlgebraicGeometry.GroupSchemeDifferentials.relativeDifferentialsIsoPullbackIdentity · AlgebraicGeometry.GroupSchemeDifferentials.pullbackConormalIsoPullbackIdentity · AlgebraicGeometry.GroupSchemeDifferentials.relativeDifferentialsIsoPullbackConormal · AlgebraicGeometry.GroupSchemeDifferentials.exists_free_iso_relativeDifferentials_of_field

Section39.7 Properties of group schemes over a field#

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

Tag 047K, a lemma

Tag 047K in the Stacks Project.

AlgebraicGeometry.isOpenMap_mul, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Multiplication.lean, line 54.

Stacks Project, Tag 047K. The multiplication morphism of a group scheme over a field is open.

lemma isOpenMap_mul {K : Type u} [Field K] (G : Over (Spec (.of K))) [GrpObj G] :
    IsOpenMap μ[G].left

Tag 0B7N, a lemma

Tag 0B7N in the Stacks Project.

AlgebraicGeometry.isOpen_image_mul_of_open, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Multiplication.lean, line 84.

Stacks Project, Tag 0B7N. The image of T × U under parametrized multiplication is open.

lemma isOpen_image_mul_of_open {k : Type u} [Field k]
    (G T : Over (Spec (.of k))) [GrpObj G] (ψ : T ⟶ G)
    (U : G.left.Opens) :
    IsOpen (Set.image (lift (fst T G ≫ ψ) (snd T G) ≫ μ[G]).left.base
      ((snd T G).left.base ⁻¹' (U : Set G.left)))

Tag 047L, a lemma

Tag 047L in the Stacks Project.

AlgebraicGeometry.isSeparated_of_groupScheme_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Separated.lean, line 45. References: SGA 3 VIB (1.1), “(2), special case”; SGA 3 VIB (6.2.4); SGA 3 VIII (6.5), “partial”.

Stacks Project, Tag 047L. The underlying scheme of a group scheme over a field is separated.

theorem isSeparated_of_groupScheme_over_field {k : Type u} [Field k]
    (G : Grp (Over (Spec (.of k)))) : G.X.left.IsSeparated

Tag 047M, a lemma

Tag 047M in the Stacks Project.

AlgebraicGeometry.existsUnique_irreducibleComponent_containing_identity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/IdentityComponent.lean, line 283. The attribute's comment: “identity_component_unique”. References: SGA 3 VIA (2.4), “(i) irred., base field”; SGA 3 VIA (2.6.5), “(a)”.

Stacks Project, Tag 047M. A group scheme over a field has a unique irreducible component containing its identity point.

theorem existsUnique_irreducibleComponent_containing_identity
    {k : Type u} [Field k] {G : Scheme.{u}} (f : G ⟶ Spec (.of k))
    [GrpObj (Over.mk f)] :
    ∃! Z : irreducibleComponents G,
      (η[Over.mk f]).left (IsLocalRing.closedPoint k) ∈ (Z : Set G)

AlgebraicGeometry.geometricallyIrreducible_irreducibleComponent_of_identity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/IdentityComponentGeometric.lean, line 125. The attribute's comment: “identity_component_geometrically_irreducible”. References: SGA 3 VIA (2.4), “(i) geom. irred., field”; SGA 3 VIA (2.6.5), “(ii) geom. irreducible”; SGA 3 VIA (2.6.2).

Stacks Project, Tag 047M. An irreducible component of a group scheme over a field which contains the identity is geometrically irreducible over that field.

theorem geometricallyIrreducible_irreducibleComponent_of_identity
    (k : Type u) [Field k] (G : Scheme.{u}) (f : G ⟶ Spec (.of k))
    [GrpObj (Over.mk f)] (Z : irreducibleComponents G)
    (he : Set.range (η[Over.mk f]).left ⊆ Z.1) :
    GeometricallyIrreducible
      ((Scheme.IdealSheafData.vanishingIdeal
        (⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.2⟩ :
          TopologicalSpace.Closeds G)).subschemeι ≫ f)

AlgebraicGeometry.existsUnique_minimalPrime_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/LocalMinimalPrime.lean, line 183. The attribute's comment: “local_unique_minimal_prime”.

Stacks Project, Tag 047M. Every local ring of a group scheme over a field has a unique minimal prime ideal.

theorem existsUnique_minimalPrime_stalk (k : Type u) [Field k]
    (G : Grp (Over (Spec (CommRingCat.of k)))) (g : G.X.left) :
    ∃! p : Ideal (G.X.left.presheaf.stalk g),
      p ∈ minimalPrimes (G.X.left.presheaf.stalk g)

Tag 047R, a lemma

Tag 047R in the Stacks Project.

AlgebraicGeometry.exists_closedSubgroupScheme_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverFieldProperties/Reduction.lean, line 49. References: SGA 3 VIA (0.2), “perfect k: G_red ≤ G”; SGA 3 VIA (5.6), “more general”; SGA 3 VIB (12.1), “Over the base field”; SGA 3 XII (1.0), “partial”.

The reduction of a group scheme over a perfect field is a closed subgroup scheme.

theorem exists_closedSubgroupScheme_reduction
    {k : Type u} [Field k] [PerfectField k]
    (G : Grp (Over (Spec (.of k)))) :
    let I := Scheme.IdealSheafData.vanishingIdeal (⊤ : Closeds G.X.left)
    ∃ H : ClosedSubgroupScheme G,
      ∃ e : Over.mk (I.subschemeι ≫ G.X.hom) ≅ H.carrier.X,
        Over.homMk I.subschemeι = e.hom ≫ H.ι.hom.hom

Tag 047S, a lemma

Tag 047S in the Stacks Project.

AlgebraicGeometry.isClosed_range_of_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverFieldProperties/OpenImage.lean, line 141.

Stacks Project, Tag 047S. An open image of a homomorphism of group schemes over a field is closed.

theorem isClosed_range_of_isOpen {k : Type u} [Field k]
    {G' G : Grp (Over (Spec (.of k)))} (ψ : G' ⟶ G)
    (hopen : IsOpen (Set.range ψ.hom.hom.left.base)) :
    IsClosed (Set.range ψ.hom.hom.left.base)

Tag 047T, a lemma

Tag 047T in the Stacks Project.

AlgebraicGeometry.isClosedImmersion_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/Immersion.lean, line 140.

Stacks Project, Tag 047T. Every immersion of group schemes over a field is a closed immersion.

theorem isClosedImmersion_of_isImmersion {k : Type u} [Field k]
    {G' G : Grp (Over (Spec (.of k)))} (i : G' ⟶ G)
    [IsImmersion i.hom.hom.left] : IsClosedImmersion i.hom.hom.left

Tag 0B7P, a lemma

Tag 0B7P in the Stacks Project.

AlgebraicGeometry.compactSpace_of_irreducibleSpace_grpObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/QuasiCompact.lean, line 278. References: SGA 3 VIA (0.5.1); SGA 3 VIA (2.6.5), “more general”.

Stacks Project, Tag 0B7P. An irreducible group scheme over a field is quasi-compact.

instance compactSpace_of_irreducibleSpace_grpObj
    (k : Type u) [Field k] (G : Over (Spec (.of k))) [GrpObj G]
    [IrreducibleSpace G.left] : CompactSpace G.left

Tag 0B7Q, a lemma

Tag 0B7Q in the Stacks Project.

AlgebraicGeometry.irreducibleSpace_of_connectedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Irreducible.lean, line 764. References: SGA 3 VIB (5.8.1), “X = G acting on itself”; SGA 3 VIA (2.4), “(i), special case”; SGA 3 VIA (2.6.5), “(iii)”.

A connected group scheme over a field is irreducible.

theorem irreducibleSpace_of_connectedSpace
    {k : Type u} [Field k] (G : Over (Spec (.of k))) [GrpObj G]
    [ConnectedSpace G.left] : IrreducibleSpace G.left

Tag 0B7R, a proposition

Tag 0B7R in the Stacks Project.

AlgebraicGeometry.identityComponent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/IdentitySubgroup.lean, line 359. The attribute's comment: “construction”. References: EGA IV (15.6.10); SGA 3 VIA (2.6.5), “(i) existence of G^0”; SGA 6 XIII (4.1), “G^0 over a field”; SGA 3 VIA (2.3).

The canonical closed subgroup scheme whose support is the connected component of the identity of G.

noncomputable def identityComponent (k : Type u) [Field k]
    (G : Grp (Over (Spec (.of k)))) : ClosedSubgroupScheme G

AlgebraicGeometry.identityComponent_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/IdentitySubgroup.lean, line 397. The attribute's comment: “part (1): flatness”. References: SGA 3 VIA (2.6.5), “(i)(b) flatness”.

The inclusion of the identity component is flat.

theorem identityComponent_flat (k : Type u) [Field k]
    (G : Grp (Over (Spec (.of k)))) :
    Flat (identityComponent k G).ι.hom.hom.left

AlgebraicGeometry.identityComponent_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/IdentitySubgroup.lean, line 404. The attribute's comment: “part (2): support”.

The underlying set of the identity subgroup is the connected component of the identity.

theorem identityComponent_range (k : Type u) [Field k]
    (G : Grp (Over (Spec (.of k)))) :
    Set.range (identityComponent k G).ι.hom.hom.left =
      connectedComponent (identityPoint k G)

AlgebraicGeometry.identityComponent_geometricallyIrreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/IdentitySubgroup.lean, line 416. The attribute's comment: “part (3): geometric irreducibility”. References: EGA IV (15.6.10), “partial”; SGA 3 VIA (2.4), “(i), special case”; SGA 3 VIA (2.6.2); SGA 3 VIA (2.6.5).

The identity component is geometrically irreducible over the field.

theorem identityComponent_geometricallyIrreducible (k : Type u) [Field k]
    (G : Grp (Over (Spec (.of k)))) :
    GeometricallyIrreducible (identityComponent k G).carrier.X.hom

AlgebraicGeometry.identityComponent_compactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/IdentitySubgroup.lean, line 443. The attribute's comment: “part (4): quasi-compactness”. References: SGA 3 VIA (2.6.2), “quasi-compactness”; SGA 3 VIA (2.6.5), “(ii) quasi-compact”; SGA 3 VIA (2.4), “(ii), base field”; SGA 3 VIB (3.9), “special case”.

The identity component is quasi-compact.

theorem identityComponent_compactSpace (k : Type u) [Field k]
    (G : Grp (Over (Spec (.of k)))) :
    CompactSpace (identityComponent k G).carrier.X.left

AlgebraicGeometry.identityComponent_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/IdentitySubgroup.lean, line 453. The attribute's comment: “canonicality”.

Any flat closed subgroup scheme supported on the identity component is uniquely isomorphic to the identity component over G.

theorem identityComponent_unique (k : Type u) [Field k]
    (G : Grp (Over (Spec (.of k))))
    (H : ClosedSubgroupScheme G)
    [Flat H.ι.hom.hom.left]
    (hH : Set.range H.ι.hom.hom.left =
      connectedComponent (identityPoint k G)) :
    ∃! φ : H.carrier ≅ (identityComponent k G).carrier,
      φ.hom ≫ (identityComponent k G).ι = H.ι

Tag 0B7T, a lemma

Tag 0B7T in the Stacks Project.

AlgebraicGeometry.isHomeomorph_pullback_to_product, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/AffineLimits.lean, line 442.

Let k be a field and let A be a filtered colimit of k-algebras that are finite products of copies of k. For any scheme X over k, the canonical map from the underlying space of Spec A ×_k X to |Spec A| × |X| is a homeomorphism.

theorem isHomeomorph_pullback_to_product
    (k A : Type u) [Field k] [CommRing A] [Algebra k A]
    (hA : IsFilteredColimitOfFiniteProducts k A)
    (X : Scheme.{u}) (f : X ⟶ Spec (of k)) :
    IsHomeomorph (fun x :
      (pullback (Spec.map (ofHom (algebraMap k A))) f : Scheme.{u}) ↦
        ((pullback.fst (Spec.map (ofHom (algebraMap k A))) f).base x,
          (pullback.snd (Spec.map (ofHom (algebraMap k A))) f).base x))

Tag 0B7U, a lemma

Tag 0B7U in the Stacks Project.

AlgebraicGeometry.exists_affineOpen_range_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/CompactImageAffineOpen.lean, line 1151.

Stacks Project, Tag 0B7U. The image in a Jacobson group scheme of the spectrum of a filtered colimit of finite products of the algebraically closed ground field is contained in an affine open, provided every closed point of the group scheme is rational over the ground field.

theorem exists_affineOpen_range_subset
    (k A : Type u) [Field k] [IsAlgClosed k] [CommRing A] [Algebra k A]
    (G : Grp (Over (Spec (CommRingCat.of k))))
    [JacobsonSpace G.X.left]
    (hclosed : ∀ x : G.X.left, IsClosed ({x} : Set G.X.left) →
      ∃ p : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ G.X,
        p.left.base (⊥ : PrimeSpectrum k) = x)
    (hA : IsFilteredColimitOfFiniteProducts k A)
    (f : Over.mk (Spec.map (CommRingCat.ofHom (algebraMap k A))) ⟶ G.X) :
    ∃ U : G.X.left.Opens, IsAffineOpen U ∧ Set.range f.left.base ⊆ U

Tag 047U, a lemma

Tag 047U in the Stacks Project.

AlgebraicGeometry.exists_openSubgroupScheme_isClosed_iUnion_affineOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverFieldProperties/CountableUnionOfAffines.lean, line 337.

Stacks Project, Tag 047U. A group scheme over a field has an open and closed subscheme which is a countable union of affine opens; it can be taken to be an open subgroup scheme.

theorem exists_openSubgroupScheme_isClosed_iUnion_affineOpens
    (G : Grp (Over (Spec (.of k)))) :
    ∃ (H : OpenSubgroupScheme G) (V : ℕ → G.X.left.Opens),
      IsOpen (Set.range H.ι.hom.hom.left.base) ∧
      IsClosed (Set.range H.ι.hom.hom.left.base) ∧
      Set.range η[G.X].left.base ⊆ Set.range H.ι.hom.hom.left.base ∧
      (∀ n, IsAffineOpen (V n)) ∧
      Set.range H.ι.hom.hom.left.base = ⋃ n, (V n : Set G.X.left)

Sources

• Section 39.7, Tag 047J
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isOpenMap_mul · AlgebraicGeometry.isOpen_image_mul_of_open · AlgebraicGeometry.isSeparated_of_groupScheme_over_field · AlgebraicGeometry.existsUnique_irreducibleComponent_containing_identity · AlgebraicGeometry.geometricallyIrreducible_irreducibleComponent_of_identity · AlgebraicGeometry.existsUnique_minimalPrime_stalk · AlgebraicGeometry.exists_closedSubgroupScheme_reduction · AlgebraicGeometry.isClosed_range_of_isOpen

Section39.8 Properties of algebraic group schemes#

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

Tag 045X, a lemma

Tag 045X in the Stacks Project.

AlgebraicGeometry.equidimensional_of_groupScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/Dimension.lean, line 78. The attribute's comment: “equidimensionality”. References: SGA 3 VIA (2.4.1), “special case”; SGA 3 VIB (1.5).

Stacks Project, Tag 045X. A group scheme locally of finite type over a field is equidimensional.

theorem equidimensional_of_groupScheme (k : Type u) [Field k] (G : Scheme.{u})
    [G.Over (Spec (.of k))] [GrpObj (G.asOver (Spec (.of k)))]
    [LocallyOfFiniteType (G ↘ Spec (.of k))] :
    Equidimensional G

AlgebraicGeometry.topologicalKrullDim_eq_topologicalKrullDimAt_of_groupScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/Dimension.lean, line 92. The attribute's comment: “dimension at every point”. References: EGA IV (15.6.10), “dim(G_y^0) = dim(G_y)”; SGA 3 VIB (1.2), “partial”; SGA 3 VIB (1.5).

Stacks Project, Tag 045X. The dimension of a group scheme locally of finite type over a field is its dimension at every point.

theorem topologicalKrullDim_eq_topologicalKrullDimAt_of_groupScheme (k : Type u) [Field k]
    (G : Scheme.{u}) [G.Over (Spec (.of k))] [GrpObj (G.asOver (Spec (.of k)))]
    [LocallyOfFiniteType (G ↘ Spec (.of k))] (g : G) :
    topologicalKrullDim G = topologicalKrullDimAt G g

AlgebraicGeometry.topologicalKrullDim_eq_ringKrullDim_stalk_of_groupScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/Dimension.lean, line 105. The attribute's comment: “dimension at a closed point”.

Stacks Project, Tag 045X. At a closed point of a group scheme locally of finite type over a field, the dimension of the scheme is the Krull dimension of the local ring.

theorem topologicalKrullDim_eq_ringKrullDim_stalk_of_groupScheme (k : Type u) [Field k]
    (G : Scheme.{u}) [G.Over (Spec (.of k))] [GrpObj (G.asOver (Spec (.of k)))]
    [LocallyOfFiniteType (G ↘ Spec (.of k))] (g : G) (hg : IsClosed ({g} : Set G)) :
    topologicalKrullDim G = ringKrullDim (G.presheaf.stalk g)

Tag 047N, a lemma

Tag 047N in the Stacks Project.

AlgebraicGeometry.smooth_of_groupScheme_of_charZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/SmoothCharacteristicZero.lean, line 118. References: SGA 3 VIA (1.1); SGA 3 VIA (6.9), “special case”; SGA 3 VIB (1.6), “Case S = Spec k”; SGA 3 VIB (1.6.1); SGA 3 VIIA (8.4), “more general”; SGA 3 VIIA (8.5.1), “more general”; SGA 3 XV (6.5), “partial”; SGA 3 XVII (5.5), “partial”.

Stacks Project, Tag 047N. Let k be a field of characteristic 0 and let G be a locally algebraic group scheme over k, i.e. a scheme whose structure morphism f : G ⟶ Spec k is locally of finite type and which is a group object over Spec k. Then f is smooth, i.e. G is a smooth group scheme.

By [Stacks, Tag 047I] the sheaf of relative differentials of f is free, hence locally free, and [Stacks, Tag 04QN] turns that into smoothness over a field of characteristic 0.

theorem smooth_of_groupScheme_of_charZero (k : Type u) [Field k] [CharZero k] (G : Scheme.{u})
    (f : G ⟶ Spec (CommRingCat.of k)) [GrpObj (Over.mk f)] [LocallyOfFiniteType f] :
    Smooth f

AlgebraicGeometry.Space.GroupAlgebraicSpace.isSmooth_of_charZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/GroupSpaces/OverField/SmoothCharacteristicZero.lean, line 227. The attribute's comment: “group algebraic spaces over Spec k which are schemes locally of finite type over k”. References: SGA 3 VIA (1.1), “special case”; SGA 3 VIA (6.9), “special case”; SGA 3 VIB (1.6.1), “special case”; SGA 3 VIIA (8.4), “more general”; SGA 3 XV (6.5), “special case”; SGA 3 XVII (5.5), “more general”.

Stacks 047N. Let k be a field of characteristic 0 and let G be a group algebraic space over Spec k which is a scheme locally of finite type over k. Then the structure morphism G ⟶ Spec k is smooth.

The group scheme structure on the representing scheme is obtained from the group structure of G by AlgebraicGeometry.Space.grpObjOfIsoYoneda, and the smoothness of the scheme is AlgebraicGeometry.smooth_of_groupScheme_of_charZero.

theorem GroupAlgebraicSpace.isSmooth_of_charZero
    (G : GroupAlgebraicSpace C (Spec (.of k)) hk (terminalSpace C (Spec (.of k)) hk).obj
      (terminalSpace C (Spec (.of k)) hk).property)
    [G.obj.X.left.IsRepresentable]
    (hlft : IsLocallyOfFiniteType C (Spec (.of k)) hk G.obj.X.hom) :
    IsSmooth C (Spec (.of k)) hk G.obj.X.hom

Tag 047O, a remark

Tag 047O in the Stacks Project.

AlgebraicGeometry.isReduced_of_grpObj_of_charZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/ReducedCharacteristicZeroGeneral.lean, line 46. References: SGA 3 VIA (6.9), “partial”; SGA 3 VIIA (8.5.1), “more general”; SGA 3 VIII (7.1), “more general”.

Stacks Project, Tag 047O. Any group scheme over a field of characteristic 0 is reduced (Perrin, thèse I 1.1, I 3.9, II 2.4; Bull. SMF 104, Prop. 4.2.8): a scheme G with a group object structure on f : G ⟶ Spec k over Spec k, for k a field of characteristic 0, is reduced. No finiteness assumption on f is made; the locally finite type case is AlgebraicGeometry.isReduced_of_groupScheme_of_charZero ([Stacks, Tag 047N]).

theorem isReduced_of_grpObj_of_charZero (k : Type u) [Field k] [CharZero k] (G : Scheme.{u})
    (f : G ⟶ Spec (CommRingCat.of k)) [GrpObj (Over.mk f)] : IsReduced G

AlgebraicGeometry.isReduced_of_groupScheme_of_charZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/SmoothCharacteristicZero.lean, line 138. The attribute's comment: “locally of finite type case; the general case is cited to Perrin”. References: SGA 3 VIA (6.9), “partial”; SGA 3 VIIA (8.5.1), “more general”; SGA 3 VIII (7.1), “more general”.

Stacks Project, Tag 047O, the case the source proves. A locally algebraic group scheme over a field k of characteristic 0 is reduced: it is smooth over k by [Stacks, Tag 047N], Spec k is a reduced affine scheme, and a scheme smooth over a reduced affine scheme is reduced.

The source states reducedness for an arbitrary group scheme over a field of characteristic 0, citing Perrin for that generality, and records that the locally finite type case is the consequence of [Stacks, Tag 047N] proved here.

theorem isReduced_of_groupScheme_of_charZero (k : Type u) [Field k] [CharZero k] (G : Scheme.{u})
    (f : G ⟶ Spec (CommRingCat.of k)) [GrpObj (Over.mk f)] [LocallyOfFiniteType f] :
    IsReduced G

AlgebraicGeometry.isReduced_of_groupScheme_of_charZero_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/HopfAlgebra/ReducedCharacteristicZero.lean, line 90. The attribute's comment: “for affine group schemes”. References: SGA 3 VIA (6.9), “partial”; SGA 3 VIIA (8.5.1), “more general”; SGA 3 VIII (7.1), “affine group schemes”.

Stacks Project, Tag 047O, for affine group schemes. An affine group scheme over a field of characteristic 0 is reduced, with no finiteness hypothesis: its ring of global sections is a commutative Hopf algebra, reduced by HopfAlgebra.isReduced_of_charZero.

theorem isReduced_of_groupScheme_of_charZero_of_isAffine (k : Type u) [Field k] [CharZero k]
    (G : Scheme.{u}) (f : G ⟶ Spec (CommRingCat.of k)) [GrpObj (Over.mk f)] [IsAffine G] :
    IsReduced G

Tag 047P, a lemma

Tag 047P in the Stacks Project.

AlgebraicGeometry.smooth_of_isReduced_groupScheme_of_perfectField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/SmoothPerfectField.lean, line 48. References: EGA IV (15.6.10), “special case”; SGA 3 VIIA (8.3), “Smoothness clause”; SGA 3 XII (1.0), “partial”; SGA 3 XV (4.6), “(2), special case”.

Let k be a perfect field and let G be a reduced locally algebraic group scheme over k, that is, a reduced scheme whose structure morphism f : G ⟶ Spec k is locally of finite type and which is a group object over Spec k. Then f is smooth.

theorem smooth_of_isReduced_groupScheme_of_perfectField (k : Type u) [Field k] [PerfectField k]
    (G : Scheme.{u}) (f : G ⟶ Spec (CommRingCat.of k)) [GrpObj (Over.mk f)]
    [LocallyOfFiniteType f] [IsReduced G] :
    Smooth f

Tag 0B7S, a lemma

Tag 0B7S in the Stacks Project.

AlgebraicGeometry.exists_affineOpen_containing_rational_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/RationalPointsAffineOpen.lean, line 287. References: SGA 3 XII (6.1).

A finite family of rational points of a group scheme locally of finite type over an algebraically closed field lies in an affine open.

theorem exists_affineOpen_containing_rational_points (k : Type u) [Field k] [IsAlgClosed k]
    (G : Grp (Over (Spec (.of k)))) [LocallyOfFiniteType G.X.hom] {σ : Type v} [Finite σ]
    (g : σ → (Over.mk (𝟙 (Spec (.of k))) ⟶ G.X)) :
    ∃ U : G.X.left.Opens, IsAffineOpen U ∧
      ∀ i, (g i).left.base (⊥ : PrimeSpectrum k) ∈ U

Tag 0BF7, a lemma

Tag 0BF7 in the Stacks Project.

AlgebraicGeometry.isQuasiProjective_of_groupScheme_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/QuasiProjective.lean, line 168. References: SGA 3 VIB (5.5), “special case”.

Let k be a field and G an algebraic group scheme over k. Then G is quasi-projective over k.

theorem isQuasiProjective_of_groupScheme_over_field
    (G : Grp (Over (Spec (CommRingCat.of k)))) [LocallyOfFiniteType G.X.hom]
    [QuasiCompact G.X.hom] :
    IsQuasiProjective G.X.hom

Tag 0BF8, a lemma

Tag 0BF8 in the Stacks Project.

Stacks.Groupoids.IsCentralPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Center.lean, line 91. The attribute's comment: “the functorial centre”. References: SGA 3 I (2.3.6), “center”; SGA 3 VIII (6.5).

A relative point of a group scheme lies in its functorial centre if it commutes with every point after every base change of its domain.

def IsCentralPoint {S : Scheme.{u}} (G : Grp (Over S)) {T : Over S} (h : T ⟶ G.X) : Prop

Stacks.Groupoids.exists_closedSubgroupScheme_center, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Center.lean, line 391. The attribute's comment: “representability of the centre by a closed subgroup scheme”. References: SGA 3 VIB (6.2.4), “special case”; SGA 3 VIB (6.2.5), “(i), special case”; SGA 3 VIB (6.2.6), “more general”; SGA 3 VIB (6.5.5), “Clause a), special case”; SGA 3 VIB (7.3.0), “special case”; SGA 3 VIII (6.5), “special case”; SGA 3 VIII (6.7), “first item, special case”.

Stacks Project, Tag 0BF8. The centre of a locally algebraic group scheme over a field is a closed subgroup scheme: the functorial centre Stacks.Groupoids.IsCentralPoint is represented by a closed subgroup scheme of G.

The group scheme is separated over the field by Tag 047L, so for each chart A of the affine open cover of G the locus where a point of A and a point of G commute is a closed subscheme of A ⊗ G; its Weil restriction W along the projection to G, which exists by Stacks.Groupoids.hasWeilRestrictionAffineOverField, universally cuts out "commutes with every point of A". The intersection of the W over all charts represents the centre by isCentralPoint_iff_affineCover.

theorem exists_closedSubgroupScheme_center {k : Type u} [Field k]
    (G : Grp (Over (Spec (.of k))))
    [LocallyOfFiniteType G.X.hom] :
    ∃ Z : ClosedSubgroupScheme G,
      ∀ (T : Over (Spec (.of k))) (h : T ⟶ G.X),
        (∃ z : T ⟶ Z.carrier.X, z ≫ Z.ι.hom.hom = h) ↔ IsCentralPoint G h

Sources

• Section 39.8, Tag 0BF6
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.equidimensional_of_groupScheme · AlgebraicGeometry.topologicalKrullDim_eq_topologicalKrullDimAt_of_groupScheme · AlgebraicGeometry.topologicalKrullDim_eq_ringKrullDim_stalk_of_groupScheme · AlgebraicGeometry.smooth_of_groupScheme_of_charZero · AlgebraicGeometry.Space.GroupAlgebraicSpace.isSmooth_of_charZero · AlgebraicGeometry.isReduced_of_grpObj_of_charZero · AlgebraicGeometry.isReduced_of_groupScheme_of_charZero · AlgebraicGeometry.isReduced_of_groupScheme_of_charZero_of_isAffine

Section39.9 Abelian varieties#

Section 39.9 of the Stacks Project, Tag 0BF9. 11 tags here are carried by 18 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03RO, a definition

Tag 03RO in the Stacks Project.

Stacks.Groupoids.IsAbelianVariety, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety.lean, line 52.

A group scheme over a field is an abelian variety if its structure morphism makes its underlying scheme a proper, geometrically integral variety.

class IsAbelianVariety (k : Type u) [Field k] (A : Over (Spec (.of k))) [GrpObj A] : Prop
    extends IsProperVariety k A.hom, GeometricallyIntegral A.hom

AlgebraicGeometry.IsAbelianVariety, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/AbelianVariety.lean, line 68.

Stacks Project, Tag 03RO. A group scheme over a field is an abelian variety if its structure morphism makes its underlying scheme a proper, geometrically integral variety.

class IsAbelianVariety (k : Type u) [Field k] (A : Over (Spec (.of k)))
    [GrpObj A] : Prop extends IsProperVariety k A.hom, GeometricallyIntegral A.hom

Tag 0BFA, a lemma

Tag 0BFA in the Stacks Project.

AlgebraicGeometry.isProjective_of_isAbelianVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/AbelianVarietyProjective.lean, line 69.

Stacks Project, Tag 0BFA. Let k be a field and let A be an abelian variety over k. Then A is projective over k.

An abelian variety is an algebraic group scheme over k, hence quasi-projective over k by Tag 0BF7, and it is proper over k, so Tag 0B45 makes it projective over the affine base Spec k.

theorem isProjective_of_isAbelianVariety (k : Type u) [Field k] (A : Over (Spec (.of k)))
    [GrpObj A] [IsAbelianVariety k A] : IsProjective A.hom

Tag 0BFB, a lemma

Tag 0BFB in the Stacks Project.

AlgebraicGeometry.isAbelianVariety_pullbackObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/AbelianVariety.lean, line 82.

Stacks Project, Tag 0BFB. For a field extension K/k, the base change A_K of an abelian variety A over k is an abelian variety over K.

instance isAbelianVariety_pullbackObj (A : Over (Spec (.of k))) [GrpObj A]
    [IsAbelianVariety k A] :
    IsAbelianVariety K
      ((Over.pullback (Spec.map (CommRingCat.ofHom (algebraMap k K)))).obj A)

Tag 0BFC, a lemma

Tag 0BFC in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.smooth_of_isAbelianVariety, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/AbelianVarietyEquivalentDefinitions.lean, line 293 (StacksFrontier).

Tag 0BFE, a lemma

Tag 0BFE in the Stacks Project.

Stacks.Groupoids.nonempty_cubeRelation_of_isAbelianVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cube/TheoremOfTheCube.lean, line 602.

Stacks Project, Tag 0BFE. Let k be a field, let A be an abelian variety over k and let L be an invertible 𝒪_A-module. Then

m₁₂₃^*L ⊗ m₁^*L ⊗ m₂^*L ⊗ m₃^*L ≅ m₁₂^*L ⊗ m₁₃^*L ⊗ m₂₃^*L

as invertible modules on A × A × A, where m_I is the sum of the coordinates indexed by I, written as the product of the corresponding coordinates in the group A × A × A ⟶ A. The theorem of the cube is Stacks.Groupoids.hasTheoremOfTheCube.

theorem nonempty_cubeRelation_of_isAbelianVariety [IsAbelianVariety k A]
    (L : SheafOfModules.{u} (structureSheafRing A.left.toRingedSpace))
    (hL : Stacks.SheafOfModules.IsInvertible A.left.presheaf A.left.ringCatIsSheaf L) :
    Nonempty
      (Stacks.SheafOfModules.schemeTensor (cubeObj A).left
          (Stacks.SheafOfModules.schemeTensor (cubeObj A).left
            (Stacks.SheafOfModules.schemeTensor (cubeObj A).left
              (pullbackOver (cubeProj₁ A * cubeProj₂ A * cubeProj₃ A) L)
              (pullbackOver (cubeProj₁ A) L))
            (pullbackOver (cubeProj₂ A) L))
          (pullbackOver (cubeProj₃ A) L) ≅
        Stacks.SheafOfModules.schemeTensor (cubeObj A).left
          (Stacks.SheafOfModules.schemeTensor (cubeObj A).left
            (pullbackOver (cubeProj₁ A * cubeProj₂ A) L)
            (pullbackOver (cubeProj₁ A * cubeProj₃ A) L))
          (pullbackOver (cubeProj₂ A * cubeProj₃ A) L))

Stacks.Groupoids.nonempty_cubeRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/CubeRelation.lean, line 468. The attribute's comment: “assuming the theorem of the cube (Tag 0BF4) for the triple self-product of A”.

Let A be an abelian variety over a field k satisfying the theorem of the cube HasTheoremOfTheCube A, and let L be an invertible 𝒪_A-module. Then

m₁₂₃^*L ⊗ m₁^*L ⊗ m₂^*L ⊗ m₃^*L ≅ m₁₂^*L ⊗ m₁₃^*L ⊗ m₂₃^*L

as invertible modules on A × A × A, where m_I is the product of the coordinates indexed by I in the group A × A × A ⟶ A.

theorem nonempty_cubeRelation [AlgebraicGeometry.IsAbelianVariety k A]
    (hcube : HasTheoremOfTheCube A)
    (L : SheafOfModules.{u} (structureSheafRing A.left.toRingedSpace))
    (hL : Stacks.SheafOfModules.IsInvertible A.left.presheaf A.left.ringCatIsSheaf L) :
    Nonempty
      (schemeTensor (cubeObj A).left
          (schemeTensor (cubeObj A).left
            (schemeTensor (cubeObj A).left
              (pullbackOver (cubeProj₁ A * cubeProj₂ A * cubeProj₃ A) L)
              (pullbackOver (cubeProj₁ A) L))
            (pullbackOver (cubeProj₂ A) L))
          (pullbackOver (cubeProj₃ A) L) ≅
        schemeTensor (cubeObj A).left
          (schemeTensor (cubeObj A).left
            (pullbackOver (cubeProj₁ A * cubeProj₂ A) L)
            (pullbackOver (cubeProj₁ A * cubeProj₃ A) L))
          (pullbackOver (cubeProj₂ A * cubeProj₃ A) L))

Tag 0BFF, a lemma

Tag 0BFF in the Stacks Project.

Stacks.Groupoids.nonempty_zpowId_pullback_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/ZPowPullback.lean, line 369. The attribute's comment: “for every integer n, assuming the theorem of the cube (Tag 0BF4) for A”.

Let k be a field, let A be an abelian variety over k satisfying the theorem of the cube for its triple self-product, and let L be an invertible 𝒪_A-module. Then

[n]^*L ≅ L^{⊗ n(n+1)/2} ⊗ ([-1]^*L)^{⊗ n(n-1)/2}

for every integer n, where [n] : A → A is multiplication by n, the nth power of the identity in the group A ⟶ A of morphisms into the group object, and [-1] = ι is inversion.

theorem nonempty_zpowId_pullback_iso [AlgebraicGeometry.IsAbelianVariety k A]
    (hcube : HasTheoremOfTheCube A) (n : ℤ) :
    Nonempty (pullbackOver ((𝟙 A : A ⟶ A) ^ n) L ≅
      schemeTensor A.left (schemeTensorPower A.left L hL (n * (n + 1) / 2))
        (schemeTensorPower A.left (pullbackOver (ι : A ⟶ A) L)
          (isInvertible_pullbackOver (ι : A ⟶ A) L hL) (n * (n - 1) / 2)))

Stacks.Groupoids.nonempty_zpowId_pullback_iso_of_isAbelianVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/ZPowPullbackFormula.lean, line 308.

Let k be a field, let A be an abelian variety over k and let L be an invertible 𝒪_A-module. Then for every integer n

[n]^*L ≅ L^{⊗ n(n+1)/2} ⊗ ([-1]^*L)^{⊗ n(n-1)/2}

where [n] : A → A is multiplication by n, the nth power of the identity in the group A ⟶ A of morphisms into the group object, and [-1] = ι is inversion. Both divisions are exact (Stacks.Groupoids.two_dvd_mul_succ).

theorem nonempty_zpowId_pullback_iso_of_isAbelianVariety (n : ℤ) :
    Nonempty (pullbackOver ((𝟙 A : A ⟶ A) ^ n) L ≅
      schemeTensor A.left (schemeTensorPower A.left L hL (n * (n + 1) / 2))
        (schemeTensorPower A.left (pullbackOver (ι : A ⟶ A) L)
          (isInvertible_pullbackOver (ι : A ⟶ A) L hL) (n * (n - 1) / 2)))

Tag 0BFG, a lemma

Tag 0BFG in the Stacks Project.

Stacks.Groupoids.isFiniteLocallyFreeOfRank_zpow_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/TorsionDegree.lean, line 61. The attribute's comment: “for n nonzero, the degree n^(2 dim A) read as |n|^(2 dim A): the source's statement fails for n = 0 when dim A >= 1, since [0] factors through the unit point and its fibre over the unit is all of A”.

Let k be a field, let A be an abelian variety over k and let [n] = (𝟙 A) ^ n : A ⟶ A be multiplication by a nonzero integer n in the group A ⟶ A. Then [n] is finite locally free of degree |n| ^ (2 * dim A).

theorem isFiniteLocallyFreeOfRank_zpow_id (n : ℤ) (hn : n ≠ 0) :
    Stacks.Morphisms.IsFiniteLocallyFreeOfRank ((𝟙 A : A ⟶ A) ^ n).left
      (n.natAbs ^ (2 * abelianVarietyDimension A))

Tag 0BFH, a lemma

Tag 0BFH in the Stacks Project.

Stacks.Groupoids.etale_zpow_id_iff_isUnit_intCast, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/ZPowEtaleCriterion.lean, line 232.

Stacks Project, Tag 0BFH. Let k be a field and let A be a nonzero abelian variety over k. Then [d] : A → A is étale if and only if d is invertible in k.

Nonzeroness is the positivity of the topological Krull dimension, and it is used: it is what makes the relative tangent space at the identity nonzero, so that multiplication by d on that space is injective only for d invertible. If k has characteristic p and p divides d then the derivative of [d] at the identity vanishes, and [d] is not étale.

theorem etale_zpow_id_iff_isUnit_intCast (k : Type u) [Field k] (A : Over (Spec (.of k)))
    [GrpObj A] [AlgebraicGeometry.IsAbelianVariety k A] (hA : 0 < topologicalKrullDim A.left)
    (d : ℤ) :
    Etale (((𝟙 A : A ⟶ A) ^ d).left) ↔ IsUnit ((d : ℤ) : k)

Tag 0C0Y, a lemma

Tag 0C0Y in the Stacks Project.

Stacks.Groupoids.cardinalMk_fiber_multiplication_by_char_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/ZPowCharFibre.lean, line 1574.

Let k be a field of characteristic p > 0 and A an abelian variety of dimension g over k. The fibre of [p] : A → A over the identity has at most p ^ g distinct points. The fibre is the pullback of [p] along the identity section, and its points are counted by the cardinality of its underlying space.

theorem cardinalMk_fiber_multiplication_by_char_le {k : Type u} [Field k]
    (A : Over (Spec (.of k))) [GrpObj A] [AlgebraicGeometry.IsAbelianVariety k A] (p : ℕ)
    [CharP k p] (hp : 0 < p) :
    Cardinal.mk
      (pullback (η[A]).left (((𝟙 A : A ⟶ A) ^ (p : ℤ)).left) : Scheme.{u}) ≤
      p ^ abelianVarietyDimension A

Tag 03RP, a proposition

Tag 03RP in the Stacks Project.

Stacks.Groupoids.etale_torsion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/Torsion.lean, line 88. The attribute's comment: “part (6), with the zero-dimensional case added”. References: SGA 3 XII (4.4.2), “partial”.

Stacks Project, Tag 03RP, part (6). Let A be an abelian variety over a field k and n an integer. The n-torsion group scheme A[n] = Ker([n] : A → A) is étale over k if and only if n is invertible in k, or A is zero-dimensional.

The second alternative is a correction of the source, which omits it: for the zero abelian variety A = Spec k, every A[n] is Spec k, hence étale, also when n = 0 in k. For a nonzero abelian variety the statement is the source's.

theorem etale_torsion_iff (k : Type u) [Field k] (A : Over (Spec (.of k))) [GrpObj A]
    [AlgebraicGeometry.IsAbelianVariety k A] (n : ℤ) :
    Etale (GrpObj.torsion A n).X.hom ↔ topologicalKrullDim A.left = 0 ∨ IsUnit (n : k)

Stacks.Groupoids.surjective_zpow_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/TorsionDegree.lean, line 68. The attribute's comment: “part (3), for every nonzero n”. References: SGA 7 IX (2.2.1), “more general”.

Multiplication by a nonzero integer n on an abelian variety is surjective.

theorem surjective_zpow_id (n : ℤ) (hn : n ≠ 0) : Surjective ((𝟙 A : A ⟶ A) ^ n).left

Stacks.Groupoids.exists_pow_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/TorsionDegree.lean, line 76. The attribute's comment: “part (4)”. References: SGA 3 VIII (7.11), “special case”.

If k is algebraically closed, the group A(k) of rational points of an abelian variety is divisible: for every n ≥ 1, every rational point is an n-th power.

theorem exists_pow_eq [IsAlgClosed k] (n : ℕ) (hn : n ≠ 0)
    (x : 𝟙_ (Over (Spec (.of k))) ⟶ A) : ∃ y : 𝟙_ (Over (Spec (.of k))) ⟶ A, y ^ n = x

Stacks.Groupoids.isFiniteLocallyFreeOfRank_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/TorsionDegree.lean, line 85. The attribute's comment: “part (5), for every nonzero n”.

For a nonzero integer n, the n-torsion group scheme A[n] = Ker([n] : A → A) of an abelian variety A of dimension g is finite locally free of degree |n| ^ 2g over k.

theorem isFiniteLocallyFreeOfRank_torsion (n : ℤ) (hn : n ≠ 0) :
    Stacks.Morphisms.IsFiniteLocallyFreeOfRank (GrpObj.torsion A n).X.hom
      (n.natAbs ^ (2 * abelianVarietyDimension A))

Stacks.Groupoids.nonempty_torsionBy_addEquiv_of_isUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/TorsionDegree.lean, line 95. The attribute's comment: “part (7)”.

Let A be an abelian variety of dimension g over an algebraically closed field k, and n a natural number invertible in k. Then the n-torsion A(k)[n] of the group of rational points is isomorphic to (ℤ/nℤ) ^ 2g.

theorem nonempty_torsionBy_addEquiv_of_isUnit [IsAlgClosed k] (n : ℕ) (hn : IsUnit (n : k)) :
    Nonempty (AddSubgroup.torsionBy (Additive (𝟙_ (Over (Spec (.of k))) ⟶ A)) n ≃+
      (Fin (2 * abelianVarietyDimension A) → ZMod n))

Stacks.Groupoids.exists_torsionBy_char_pow_addEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/AbelianVariety/TorsionDegree.lean, line 111. The attribute's comment: “part (8)”.

Let A be an abelian variety of dimension g over an algebraically closed field k of characteristic p > 0. There is an integer 0 ≤ f ≤ g such that A(k)[p ^ m] ≅ (ℤ/p^mℤ) ^ f for every m (for m = 0 both sides are trivial).

theorem exists_torsionBy_char_pow_addEquiv [IsAlgClosed k] (p : ℕ) [CharP k p] (hp : 0 < p) :
    ∃ f ≤ abelianVarietyDimension A, ∀ m : ℕ, Nonempty
      (AddSubgroup.torsionBy (Additive (𝟙_ (Over (Spec (.of k))) ⟶ A)) ((p ^ m : ℕ) : ℤ) ≃+
        (Fin f → ZMod (p ^ m)))

Declarations registered for the tag:

• AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/AbelianVariety.lean, line 98 (StacksFrontier): “commutative”. References: SGA 3 VIB (12.3), “special case”.
• AlgebraicGeometry.isProjective_of_isAbelianVariety, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/AbelianVarietyProjective.lean, line 78 (StacksFrontier): “projective”.

Tag 0H2U, a remark

Tag 0H2U in the Stacks Project.

AlgebraicGeometry.isAbelianVariety_iff_of_choices, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/AbelianVarietyEquivalentDefinitions.lean, line 265. References: EGA IV (15.6.10), “special case”; SGA 3 VIB (12.3), “more general”; SGA 3 VIB (7.8), “special case”; SGA 3 XV (4.6), “special case”; SGA 7 VIII (4.1), “Proper group schemes”.

Stacks Project, Tag 0H2U. Let k be a field and A a group scheme over k. Pick one property from each of the three sets

• projective, proper;
• geometrically irreducible, irreducible, geometrically connected, connected;
• smooth, geometrically reduced.

Then A is an abelian variety if and only if it has the three chosen properties over k; so the sixteen choices are sixteen equivalent definitions of an abelian variety. The choice "proper, geometrically irreducible, geometrically reduced" recovers Definition 03RO.

Every choice implies the weakest one, "proper, connected, geometrically reduced", which makes A an abelian variety (AlgebraicGeometry.isAbelianVariety_of_choices); conversely an abelian variety is projective by Tag 0BFA, smooth by Tag 0BFC and geometrically irreducible, which is the strongest choice and implies every other.

theorem isAbelianVariety_iff_of_choices
    (k : Type u) [Field k] (A : Over (Spec (.of k))) [GrpObj A] :
    ∀ P₁ ∈ [IsProjective A.hom, IsProper A.hom],
    ∀ P₂ ∈ [GeometricallyIrreducible A.hom, IrreducibleSpace A.left,
      GeometricallyConnected A.hom, ConnectedSpace A.left],
    ∀ P₃ ∈ [Smooth A.hom, GeometricallyReduced A.hom],
      (IsAbelianVariety k A ↔ P₁ ∧ P₂ ∧ P₃)

Sources

• Section 39.9, Tag 0BF9
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Groupoids.IsAbelianVariety · AlgebraicGeometry.IsAbelianVariety · AlgebraicGeometry.isProjective_of_isAbelianVariety · AlgebraicGeometry.isAbelianVariety_pullbackObj · AlgebraicGeometry.smooth_of_isAbelianVariety · Stacks.Groupoids.nonempty_cubeRelation_of_isAbelianVariety · Stacks.Groupoids.nonempty_cubeRelation · Stacks.Groupoids.nonempty_zpowId_pullback_iso

Section39.10 Actions of group schemes#

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

Tag 022Z, a definition

Tag 022Z in the Stacks Project.

AlgebraicGeometry.GroupSchemeOverPoints.Action, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Action.lean, line 82. The attribute's comment: “part (1): an action of a group scheme on a scheme over the base”.

Stacks Project, Tag 022Z (1). An action of the group scheme G over S on the scheme X over S: a morphism a : G ×_S X ⟶ X of schemes over S such that for every scheme T over S the map G(T) × X(T) ⟶ X(T), (g, x) ↦ a ∘ (g, x), defines the structure of a G(T)-set on X(T), namely the identity of G(T) acts trivially and (g h) x = g (h x).

structure Action (X : Over S)

AlgebraicGeometry.GroupSchemeOverPoints.Action.IsEquivariant, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Action.lean, line 127. The attribute's comment: “part (2): equivariant morphisms”.

Stacks Project, Tag 022Z (2). A morphism ψ : X ⟶ Y of schemes over S, where X and Y carry actions A and B of G, is G-equivariant if for every scheme T over S the map ψ : X(T) ⟶ Y(T) is a morphism of G(T)-sets.

def IsEquivariant (A : G.Action X) (B : G.Action Y) (ψ : X ⟶ Y) : Prop

AlgebraicGeometry.GroupSchemeOverPoints.Action.equivModObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Action.lean, line 246. The attribute's comment: “part (1): actions are the module objects over the internal group object”.

Stacks Project, Tag 022Z (1), compared with Mathlib. Actions of the group scheme G on X in the functor-of-points sense are the same as module objects ModObj over the internal group object G.grpObj of Over S.

noncomputable def equivModObj (X : Over S) :
    G.Action X ≃ (letI := G.grpObj; ModObj G.obj X)

AlgebraicGeometry.GroupSchemeOverPoints.Action.isEquivariant_iff_isModHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Action.lean, line 257. The attribute's comment: “part (2): equivariant morphisms are the morphisms of module objects”.

Stacks Project, Tag 022Z (2), compared with Mathlib. A morphism ψ : X ⟶ Y over S is G-equivariant for actions A and B exactly when it is a morphism IsModHom of the associated module objects over the internal group object G.grpObj.

theorem isEquivariant_iff_isModHom (A : G.Action X) (B : G.Action Y) (ψ : X ⟶ Y) :
    IsEquivariant A B ψ ↔
      letI := G.grpObj
      letI := A.modObj
      letI := B.modObj
      IsModHom G.obj ψ

Tag 03LD, an equation

Tag 03LD in the Stacks Project.

Declarations registered for the tag:

• CategoryTheory.ModObj.mul_smul_self registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Action.lean, line 48 (StacksFrontier): “associativity”.
• CategoryTheory.ModObj.one_smul_self registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Action.lean, line 49 (StacksFrontier): “identity”.

Tag 07S1, a definition

Tag 07S1 in the Stacks Project.

AlgebraicGeometry.IsFreeAction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Action.lean, line 57.

A group object acts freely on X if its action on T-points is free for every object T.

abbrev IsFreeAction {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C]
    (G X : C) [GrpObj G] [ModObj G X] : Prop

Tag 07S2, a lemma

Tag 07S2 in the Stacks Project.

AlgebraicGeometry.isFreeAction_iff_mono_leftSMul, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Action.lean, line 66. References: SGA 3 IV (3.2.1), “(i), special case”; SGA 3 V (10.2.1), “more general”; SGA 4 IV (9.8.2), “Remark after d)”.

A group action is free if and only if (g, x) ↦ (g • x, x) is a monomorphism.

lemma isFreeAction_iff_mono_leftSMul {C : Type u} [Category.{v} C]
    [CartesianMonoidalCategory C] (G X : C) [GrpObj G] [ModObj G X] :
    IsFreeAction G X ↔ Mono (ModObj.leftSMul G X)

Sources

• Section 39.10, Tag 022Y
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.GroupSchemeOverPoints.Action · AlgebraicGeometry.GroupSchemeOverPoints.Action.IsEquivariant · AlgebraicGeometry.GroupSchemeOverPoints.Action.equivModObj · AlgebraicGeometry.GroupSchemeOverPoints.Action.isEquivariant_iff_isModHom · CategoryTheory.ModObj.mul_smul_self · CategoryTheory.ModObj.one_smul_self · AlgebraicGeometry.IsFreeAction · AlgebraicGeometry.isFreeAction_iff_mono_leftSMul

Section39.11 Principal homogeneous spaces#

Section 39.11 of the Stacks Project, Tag 0497. 4 tags here are carried by 15 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0498, a definition

Tag 0498 in the Stacks Project.

AlgebraicGeometry.IsPseudoTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 61. The attribute's comment: “part (1)”. References: SGA 3 VIB (10.15), “formally principal hom.”; SGA 3 IV (6.7), “(iii)”; SGA 3 IV (5.1.0); SGA 3 III (0.1), “(ii)”; SGA 1 V (5.11), “formally princ. homog.”.

An action is a pseudo-torsor if its shear map (g, x) ↦ (g • x, x) is an isomorphism.

abbrev IsPseudoTorsor {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C]
    (G X : C) [GrpObj G] [ModObj G X] : Prop

AlgebraicGeometry.IsTrivialPseudoTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 68. The attribute's comment: “part (2)”. References: SGA 3 IV (5.1.1).

An action is trivial if it is equivariantly isomorphic to the group object with its left regular action.

abbrev IsTrivialPseudoTorsor {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C]
    (G X : C) [GrpObj G] [ModObj G X] : Prop

Tag 0499, a lemma

Tag 0499 in the Stacks Project.

AlgebraicGeometry.isPseudoTorsor_iff_forall_existsUnique_smul, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 79. The attribute's comment: “part (1), the pointwise characterization”. References: SGA 3 IV (5.1.0), “more general”; SGA 3 IV (6.7), “(i) ⇔ (iii)”.

An action is a pseudo-torsor exactly when it is pointwise simply transitive: for every test object T, any two T-points of X differ by a unique T-point of G.

lemma isPseudoTorsor_iff_forall_existsUnique_smul
    {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C]
    (G X : C) [GrpObj G] [ModObj G X] :
    IsPseudoTorsor G X ↔ ∀ (T : C) (x y : T ⟶ X), ∃! g : T ⟶ G, g • x = y

AlgebraicGeometry.isTrivial_iff_exists_globalSection, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 87. The attribute's comment: “trivial_iff_section”. References: SGA 3 IV (5.1.4); SGA 3 IV (5.1.5), “(ii) trivial ⟺ section”.

A pseudo-torsor is trivial if and only if it admits a global section.

lemma isTrivial_iff_exists_globalSection
    {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C]
    (G X : C) [GrpObj G] [ModObj G X] (hX : IsPseudoTorsor G X) :
    IsTrivialPseudoTorsor G X ↔ Nonempty (𝟙_ C ⟶ X)

Declarations registered for the tag:

• CategoryTheory.ModObj.isIso_leftSMul_iff registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 72 (StacksFrontier): “pointwise_characterization”.

Tag 049A, a definition

Tag 049A in the Stacks Project.

AlgebraicGeometry.IsFpqcTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 131. The attribute's comment: “part (1)”. References: SGA 3 IV (5.1.5), “schemes, fpqc”; SGA 3 IV (6.5), “fpqc row”; SGA 3 VIB (10.15), “G-torsor, fpqc T”; SGA 1 XI (4.1).

A pseudo-torsor trivialized by an fpqc covering.

abbrev IsFpqcTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G] [ModObj G X] : Prop

AlgebraicGeometry.IsZariskiTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 140. The attribute's comment: “parts (2), (4): Zariski and locally trivial”. References: SGA 1 XI (4.7); SGA 3 IV (6.5), “(Zar) row, special case”; SGA 4 IV (5.9), “special case”.

A pseudo-torsor trivialized by a Zariski covering; equivalently, a locally trivial torsor.

abbrev IsZariskiTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G] [ModObj G X] : Prop

AlgebraicGeometry.IsEtaleTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 148. The attribute's comment: “parts (2), (3): étale and quasi-isotrivial”. References: SGA 3 IV (5.1.5), “schemes, étale”; SGA 3 IV (6.5), “étale row”; SGA 3 VIB (10.15), “G-torsor, étale T”.

A pseudo-torsor trivialized by an étale covering; equivalently, a quasi-isotrivial torsor.

abbrev IsEtaleTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G] [ModObj G X] : Prop

AlgebraicGeometry.IsSmoothTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 153. The attribute's comment: “part (2): smooth”.

A pseudo-torsor trivialized by a smooth covering.

abbrev IsSmoothTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G] [ModObj G X] : Prop

AlgebraicGeometry.IsSyntomicTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 158. The attribute's comment: “part (2): syntomic”.

A pseudo-torsor trivialized by a syntomic covering.

abbrev IsSyntomicTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G] [ModObj G X] : Prop

AlgebraicGeometry.IsFppfTorsor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/Torsor.lean, line 167. The attribute's comment: “part (2): fppf”. References: SGA 3 IV (5.1.5), “schemes, fppf”; SGA 3 VIB (10.15), “G-torsor, fppf T”.

A pseudo-torsor trivialized by an fppf covering.

abbrev IsFppfTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G] [ModObj G X] : Prop

Tag 049B, a lemma

Tag 049B in the Stacks Project.

AlgebraicGeometry.isZariskiTorsor_iff_isSiteTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/Torsor.lean, line 341. The attribute's comment: “Zariski”.

Stacks Project, Tag 049B. Zariski torsors under group schemes are exactly the torsors of their functors of points on the big Zariski site.

theorem isZariskiTorsor_iff_isSiteTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G]
    [ModObj G X] :
    IsZariskiTorsor S G X ↔ IsSiteTorsor S (Scheme.zariskiTopology.over S) G X

AlgebraicGeometry.isEtaleTorsor_iff_isSiteTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/Torsor.lean, line 349. The attribute's comment: “étale”.

Stacks Project, Tag 049B. Étale torsors under group schemes are exactly the torsors of their functors of points on the big étale site.

theorem isEtaleTorsor_iff_isSiteTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G]
    [ModObj G X] :
    IsEtaleTorsor S G X ↔ IsSiteTorsor S (Scheme.etaleTopology.over S) G X

AlgebraicGeometry.isSmoothTorsor_iff_isSiteTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/Torsor.lean, line 357. The attribute's comment: “smooth”.

Stacks Project, Tag 049B. Smooth torsors under group schemes are exactly the torsors of their functors of points on the big smooth site.

theorem isSmoothTorsor_iff_isSiteTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G]
    [ModObj G X] :
    IsSmoothTorsor S G X ↔
      IsSiteTorsor S ((Scheme.precoverage @Smooth).toGrothendieck.over S) G X

AlgebraicGeometry.isSyntomicTorsor_iff_isSiteTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/Torsor.lean, line 366. The attribute's comment: “syntomic”.

Stacks Project, Tag 049B. Syntomic torsors under group schemes are exactly the torsors of their functors of points on the big syntomic site.

theorem isSyntomicTorsor_iff_isSiteTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G]
    [ModObj G X] :
    IsSyntomicTorsor S G X ↔
      IsSiteTorsor S ((Scheme.precoverage @Syntomic).toGrothendieck.over S) G X

AlgebraicGeometry.isFppfTorsor_iff_isSiteTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/Torsor.lean, line 375. The attribute's comment: “fppf”.

Stacks Project, Tag 049B. Fppf torsors under group schemes are exactly the torsors of their functors of points on the big fppf site.

theorem isFppfTorsor_iff_isSiteTorsor (S : Scheme.{u}) (G X : Over S) [GrpObj G]
    [ModObj G X] :
    IsFppfTorsor S G X ↔ IsSiteTorsor S (Scheme.fppfTopology.over S) G X

Sources

• Section 39.11, Tag 0497
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.IsPseudoTorsor · AlgebraicGeometry.IsTrivialPseudoTorsor · AlgebraicGeometry.isPseudoTorsor_iff_forall_existsUnique_smul · AlgebraicGeometry.isTrivial_iff_exists_globalSection · CategoryTheory.ModObj.isIso_leftSMul_iff · AlgebraicGeometry.IsFpqcTorsor · AlgebraicGeometry.IsZariskiTorsor · AlgebraicGeometry.IsEtaleTorsor

Section39.12 Equivariant quasi-coherent sheaves#

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

Tag 03LF, a definition

Tag 03LF in the Stacks Project.

AlgebraicGeometry.EquivariantModule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/EquivariantModule.lean, line 183. References: SGA 3 I (6.5.1), “equivariant module”; SGA 3 I (6.5).

A quasi-coherent module on X equivariant for a given action of G, written directly in terms of the action map and the projection.

structure EquivariantModule

Tag 03LG, a lemma

Tag 03LG in the Stacks Project.

AlgebraicGeometry.equivariantGroupoidMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/ActionGroupoidPullback.lean, line 217. The attribute's comment: “action-groupoid morphism”.

Stacks Project, Tag 03LG. An equivariant morphism induces the specified morphism of action groupoids.

noncomputable def equivariantGroupoidMorphism (f : Y ⟶ X) [IsModHom G f] :
    EquivariantGroupoidMorphism B G X Y f

AlgebraicGeometry.equivariantPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/ActionGroupoidPullback.lean, line 306. The attribute's comment: “the functor”. References: SGA 3 I (6.5.2); SGA 3 I (6.3.1).

Stacks Project, Tag 03LG. Pullback of equivariant quasi-coherent modules along an equivariant morphism f. Its action on modules, on equivariant structures and on morphisms is that of the pullback functor along the induced morphism of action groupoids.

noncomputable def equivariantPullback (f : Y ⟶ X) [IsModHom G f] :
    Stacks.Groupoids.GroupoidScheme.QuasicoherentModule (actionGroupoid B G X) ⥤
      Stacks.Groupoids.GroupoidScheme.QuasicoherentModule (actionGroupoid B G Y)

Tag 0EKJ, an example

Tag 0EKJ in the Stacks Project.

AlgebraicGeometry.gradedGmAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedAction.lean, line 189. The attribute's comment: “graded_ring_gm_action”. References: EGA II (8.3.9), “partial”.

Stacks Project, Tag 0EKJ. An integer grading defines the multiplicative-group action on the spectrum whose coordinate map sends a homogeneous element of degree n to a ⊗ Tⁿ.

noncomputable def gradedGmAction {A : Type u} [CommRing A] {σ : Type v}
    [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℤ → σ) [GradedRing 𝒜] :
    GradedGmAction 𝒜

AlgebraicGeometry.GmEquivariant.gradedDescentMorphism_homogeneous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedModuleEquivariantSheaf.lean, line 562. The attribute's comment: “the descent morphism on homogeneous sections”.

On the canonical pullback of a homogeneous section of degree n along the action, the descent morphism is multiplication by the character xⁿ.

theorem gradedDescentMorphism_homogeneous {n : ℤ} (m : ℳ n) :
    (gradedDescentMorphism 𝒜 ℳ).app ⊤
        (pullbackSection (gradedGmAction 𝒜).action.smul.left (tilde (moduleOf A M))
          (tilde.toOpen (moduleOf A M) ⊤ (m : M))) =
      laurentCoordinate A n • pullbackSection (snd gm.{u} (specAOver A)).left
        (tilde (moduleOf A M)) (tilde.toOpen (moduleOf A M) ⊤ (m : M))

AlgebraicGeometry.GmEquivariant.gradedModuleEquivariantSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedModuleEquivariantSheaf.lean, line 619. The attribute's comment: “graded_module_equivariant_sheaf”.

Let A be a ℤ-graded ring and let X = Spec A carry the 𝐆ₘ-action attached to the grading. A graded A-module M makes the associated quasi-coherent module M~ a 𝐆ₘ-equivariant quasi-coherent 𝒪_X-module, whose descent morphism carries the canonical pullback of a homogeneous section of degree n to xⁿ times that section.

noncomputable def gradedModuleEquivariantSheaf : GradedEquivariantModule.{u} 𝒜

AlgebraicGeometry.GmEquivariant.gradedModuleEquivariantSheaf_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedModuleEquivariantSheaf.lean, line 629. The attribute's comment: “underlying module”.

The underlying quasi-coherent module of the equivariant module attached to a graded module is M~.

theorem gradedModuleEquivariantSheaf_module :
    underlyingModule 𝒜 (gradedModuleEquivariantSheaf 𝒜 ℳ) = tilde (moduleOf A M)

AlgebraicGeometry.GmEquivariant.gradedModuleEquivariantSheaf_alpha, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedModuleEquivariantSheaf.lean, line 636. The attribute's comment: “descent morphism”.

The descent morphism of the equivariant module attached to a graded module is gradedDescentMorphism.

theorem gradedModuleEquivariantSheaf_alpha :
    descentMorphism 𝒜 (gradedModuleEquivariantSheaf 𝒜 ℳ) = gradedDescentMorphism 𝒜 ℳ

Tag 0EKK, a lemma

Tag 0EKK in the Stacks Project.

AlgebraicGeometry.gradingOfGmAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedActionOfGmAction.lean, line 389. References: EGA II (8.3.9), “special case”.

Stacks Project, Tag 0EKK. An action of the multiplicative group scheme on an affine scheme determines an integer grading of its coordinate ring, and is the action associated to that grading.

noncomputable def gradingOfGmAction (X : Scheme.{u}) [IsAffine X]
    [X.Over (Spec (.of (ULift.{u} ℤ)))]
    (action : ModObj
      (multiplicativeGroupULift.asOver (Spec (.of (ULift.{u} ℤ))))
      (X.asOver (Spec (.of (ULift.{u} ℤ))))) :
    Σ (𝒜 : ℤ → AddSubgroup Γ(X, ⊤)),
      {graded : GradedRing 𝒜 //
        (letI := action
         letI : X.isoSpec.hom.IsOver (Spec (.of (ULift.{u} ℤ))) :=
           ⟨specULiftZIsTerminal.hom_ext _ _⟩
         letI : IsMonHom
             (Iso.refl (multiplicativeGroupULift.asOver (Spec (.of (ULift.{u} ℤ))))).hom :=
           ⟨by exact Category.comp_id _, by simp⟩
         ModObj.ofIso (Iso.refl (multiplicativeGroupULift.asOver (Spec (.of (ULift.{u} ℤ)))))
           (X.isoSpec.asOver (Spec (.of (ULift.{u} ℤ))))) =
          (letI := graded; (gradedGmAction 𝒜).action)}

Tag 0EKL, a lemma

Tag 0EKL in the Stacks Project.

AlgebraicGeometry.GmEquivariant.homogeneousPartDecomposition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedModuleEquivariantComparison.lean, line 800. The attribute's comment: “the canonical grading of the global sections”.

Stacks Project, Tag 0EKL. The canonical grading of the global sections of a 𝐆ₘ-equivariant quasi-coherent module on Spec A: the canonical homogeneous pieces decompose the global sections as an internal direct sum.

noncomputable def homogeneousPartDecomposition (F : GradedEquivariantModule.{u} 𝒜) :
    DirectSum.Decomposition (homogeneousPart 𝒜 F)

AlgebraicGeometry.GmEquivariant.tildeHomogeneousIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedModuleEquivariantIsomorphism.lean, line 199. The attribute's comment: “the comparison is an isomorphism of equivariant modules”.

Stacks Project, Tag 0EKL. For a 𝐆ₘ-equivariant quasi-coherent module F on X = Spec A and M = Γ(X, F) with its canonical grading, the canonical comparison M~ ⟶ F is an isomorphism of 𝐆ₘ-equivariant modules, the equivariant structure on M~ being the one attached to the grading of M.

noncomputable def tildeHomogeneousIso :
    gradedModuleEquivariantSheaf 𝒜 (homogeneousPart 𝒜 F) ≅ F

AlgebraicGeometry.GmEquivariant.tildeHomogeneousIso_hom_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedModuleEquivariantIsomorphism.lean, line 212. The attribute's comment: “the equivariant isomorphism is the canonical comparison”.

Stacks Project, Tag 0EKL. The isomorphism of 𝐆ₘ-equivariant modules above is the canonical comparison of a quasi-coherent module on an affine scheme with the module associated to its global sections.

theorem tildeHomogeneousIso_hom_hom :
    @EquivariantModule.Hom.hom _ base.{u} gm.{u} (specAOver A)
        AlgebraicGeometry.instGrpObjSpecAsOverSpec (gradedGmAction 𝒜).action
        (gradedModuleEquivariantSheaf 𝒜 (homogeneousPart 𝒜 F)) F
        (@CategoryTheory.Iso.hom _ _ _ _ (tildeHomogeneousIso 𝒜 F)) =
      Scheme.Modules.fromTildeΓNatTrans.app (underlyingModule 𝒜 F)

AlgebraicGeometry.GmEquivariant.homogeneousPart, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedModuleOfEquivariantModule.lean, line 270. The attribute's comment: “the canonical homogeneous pieces of the global sections”.

The canonical degree-n piece of the global sections of a 𝐆ₘ-equivariant quasi-coherent module on Spec A: the sections on which the descent morphism of the equivariant structure multiplies the canonical pullback section by the character x ↦ xⁿ of 𝐆ₘ.

noncomputable def homogeneousPart (F : GradedEquivariantModule.{u} 𝒜) (n : ℤ) :
    AddSubgroup ((moduleSpecΓFunctor (R := .of A)).obj (underlyingModule 𝒜 F))

AlgebraicGeometry.GmEquivariant.gradedSMul_homogeneousPart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GradedModuleOfEquivariantModule.lean, line 382. The attribute's comment: “compatibility of the canonical homogeneous pieces with the grading of A”.

The canonical homogeneous pieces of the global sections of a 𝐆ₘ-equivariant quasi-coherent module on Spec A are compatible with the grading of A: a homogeneous function of degree i carries the degree-n piece into the degree-i + n piece.

theorem gradedSMul_homogeneousPart (F : GradedEquivariantModule.{u} 𝒜) :
    SetLike.GradedSMul 𝒜 (homogeneousPart 𝒜 F)

Sources

• Section 39.12, Tag 03LE
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.EquivariantModule · AlgebraicGeometry.equivariantGroupoidMorphism · AlgebraicGeometry.equivariantPullback · AlgebraicGeometry.gradedGmAction · AlgebraicGeometry.GmEquivariant.gradedDescentMorphism_homogeneous · AlgebraicGeometry.GmEquivariant.gradedModuleEquivariantSheaf · AlgebraicGeometry.GmEquivariant.gradedModuleEquivariantSheaf_module · AlgebraicGeometry.GmEquivariant.gradedModuleEquivariantSheaf_alpha

Section39.13 Groupoids#

Section 39.13 of the Stacks Project, Tag 0230. 7 tags here are carried by 18 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0230, the section

Tag 0230 in the Stacks Project.

CategoryTheory.Groupoid.eq_id_of_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 52. The attribute's comment: “the identity map e is uniquely determined”.

In a groupoid, a family of endomorphisms which is a right unit for composition is the family of identities.

theorem eq_id_of_comp_eq (e : ∀ X : C, X ⟶ X) (he : ∀ {X Y : C} (f : X ⟶ Y), f ≫ e Y = f)
    (X : C) : e X = 𝟙 X

CategoryTheory.Groupoid.eq_inv_of_comp_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 58. The attribute's comment: “the inverse map i is uniquely determined”.

In a groupoid, a right inverse of a morphism is its inverse.

theorem eq_inv_of_comp_eq_id (i : ∀ {X Y : C}, (X ⟶ Y) → (Y ⟶ X))
    (hi : ∀ {X Y : C} (f : X ⟶ Y), f ≫ i f = 𝟙 X) {X Y : C} (f : X ⟶ Y) :
    i f = Groupoid.inv f

Prefunctor.map_id_of_map_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 72. The attribute's comment: “a map of groupoids compatible with composition preserves identities”.

A map of groupoids compatible with composition preserves identities.

theorem map_id_of_map_comp (F : C ⥤q D)
    (hF : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), F.map (f ≫ g) = F.map f ≫ F.map g) (X : C) :
    F.map (𝟙 X) = 𝟙 (F.obj X)

Prefunctor.map_inv_of_map_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 90. The attribute's comment: “a map of groupoids compatible with composition preserves inverses”.

A map of groupoids compatible with composition preserves inverses.

theorem map_inv_of_map_comp (F : C ⥤q D)
    (hF : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), F.map (f ≫ g) = F.map f ≫ F.map g)
    {X Y : C} (f : X ⟶ Y) : F.map (Groupoid.inv f) = Groupoid.inv (F.map f)

Declarations registered for the tag:

• CategoryTheory.Groupoid registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 98 (StacksFrontier): “groupoid categories”. References: SGA 3 V (1.2), “partial”; SGA 4 I (6.5.1); SGA 4 I (6.5.2); SGA 4 XVIII (1.2.1), “partial”.
• CategoryTheory.Groupoid.invEquiv registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 103 (StacksFrontier): “the inverse map i is a bijection”.
• Stacks.Groupoids.GroupoidScheme.evaluationGroupoid, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 104 (StacksFrontier): “the points of a groupoid scheme over a test scheme form a groupoid”.
• AlgebraicGeometry.groupoidInverse_left_isIso, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 106 (StacksFrontier): “the inverse morphism of a groupoid scheme is an isomorphism”.
• Stacks.Groupoids.identity_left_comp_source_left, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 108 (StacksFrontier): “the identity morphism is a section of the source”.
• Stacks.Groupoids.identity_left_comp_target_left, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 110 (StacksFrontier): “the identity morphism is a section of the target”.
• AlgebraicGeometry.groupoidHom_map_inverse, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Groupoids/GroupoidCategories.lean, line 112 (StacksFrontier): “a morphism of groupoid schemes is compatible with the inverses”.

Tag 0231, a definition

Tag 0231 in the Stacks Project.

Stacks.Groupoids.GroupoidScheme, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Basic.lean, line 70. The attribute's comment: “part (1): groupoid schemes”.

A groupoid object in schemes over S.

The fields identity and inverse are included as data, although they are uniquely determined by source, target and comp.

structure GroupoidScheme (S : Scheme.{u})

Stacks.Groupoids.GroupoidScheme.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Pullback.lean, line 72. The attribute's comment: “part (2): morphisms of groupoid schemes”.

A morphism of groupoid schemes.

structure Hom {S : Scheme.{u}} (G H : GroupoidScheme S)

Tag 0232, a lemma

Tag 0232 in the Stacks Project.

AlgebraicGeometry.groupoidPreRelation_isPreEquivalenceRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidOfEquivalenceRelation.lean, line 69.

The pre-relation underlying a groupoid scheme is a pre-equivalence relation.

theorem groupoidPreRelation_isPreEquivalenceRelation {S : Scheme.{u}} (G : GroupoidScheme S) :
    IsPreEquivalenceRelation (groupoidPreRelation G)

Tag 0233, a lemma

Tag 0233 in the Stacks Project.

AlgebraicGeometry.existsUnique_groupoidScheme_of_isEquivalenceRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidOfEquivalenceRelation.lean, line 143.

An equivalence relation on a scheme over S extends in a unique way to a groupoid scheme over S.

theorem existsUnique_groupoidScheme_of_isEquivalenceRelation (j : PreRelation R U)
    [IsEquivalenceRelation j.target j.source] :
    ∃! G : GroupoidScheme S, ExtendsRelation j G

Tag 02YE, a lemma

Tag 02YE in the Stacks Project.

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

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

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

Stacks.Groupoids.GroupoidScheme.target_comp_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FieldExtensionEvaluation.lean, line 197. The attribute's comment: “the upper square”.

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

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

Tag 03C6, a lemma

Tag 03C6 in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.comp_source_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FieldExtensionEvaluation.lean, line 148. The attribute's comment: “the lower composition square of the diagram: top map the composition, verticals the second projection and the source, bottom map the source”.

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

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

AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 81. The attribute's comment: “the vertical comparison”.

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

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

AlgebraicGeometry.GroupoidScheme.fst_source_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 103. The attribute's comment: “the lower projection square”.

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

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

AlgebraicGeometry.GroupoidScheme.id_target_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 114. The attribute's comment: “commutativity of the upper right square”.

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

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

AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 123. The attribute's comment: “commutativity with the first projection”.

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

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

AlgebraicGeometry.GroupoidScheme.targetPullbackToComposable_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 142. The attribute's comment: “commutativity with composition”.

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

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

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

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

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

Declarations registered for the tag:

• Stacks.Groupoids.GroupoidScheme.comp_source_isPullback, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidPullbackDiagram.lean, line 89 (StacksFrontier): “the lower composition square”.

Tag 0DT8, a lemma

Tag 0DT8 in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.exists_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidBaseChange.lean, line 82.

Base-changing the object and arrow schemes of a groupoid scheme, and all its structure maps, produces a groupoid scheme over the new base whose projections form a morphism of groupoid schemes.

theorem exists_baseChange {S S' : Scheme.{u}} (f : S' ⟶ S)
    (G : Stacks.Groupoids.GroupoidScheme S) : Nonempty (BaseChange f G)

Sources

• Section 39.13, Tag 0230
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.Groupoid.eq_id_of_comp_eq · CategoryTheory.Groupoid.eq_inv_of_comp_eq_id · Prefunctor.map_id_of_map_comp · Prefunctor.map_inv_of_map_comp · CategoryTheory.Groupoid · CategoryTheory.Groupoid.invEquiv · Stacks.Groupoids.GroupoidScheme.evaluationGroupoid · AlgebraicGeometry.groupoidInverse_left_isIso

Section39.14 Quasi-coherent sheaves on groupoids#

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

Tag 03LI, a definition

Tag 03LI in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.QuasicoherentModule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Pullback.lean, line 200.

A quasi-coherent module on a groupoid scheme, with its descent morphism, cocycle law, and normalization along the identity section.

structure QuasicoherentModule {S : Scheme.{u}} (G : GroupoidScheme S)

Tag 077Q, a lemma

Tag 077Q in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.QuasicoherentModule.alpha_isIso, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/DescentIso.lean, line 424.

The descent morphism of a quasi-coherent module on a groupoid scheme is an isomorphism.

instance alpha_isIso (M : QuasicoherentModule G) : IsIso M.alpha

Tag 03LJ, a lemma

Tag 03LJ in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.pullbackFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/PullbackFunctor.lean, line 197. The attribute's comment: “the functor”.

Stacks Project, Tag 03LJ. Pullback along a morphism of groupoid schemes, as a functor on quasi-coherent modules equipped with groupoid descent data. On objects it sends (F, α) to (f⁺F, f⁺α), using the canonical comparison isomorphisms for pullback along composites; on morphisms it is the usual pullback of morphisms of modules.

noncomputable def pullbackFunctor (f : Hom G H) :
    QuasicoherentModule H ⥤ QuasicoherentModule G

Stacks.Groupoids.GroupoidScheme.pullbackFunctor_obj_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/PullbackFunctor.lean, line 220. The attribute's comment: “underlying modules”.

Stacks Project, Tag 03LJ. Pullback along a morphism of groupoid schemes pulls back the underlying module along the map on objects.

theorem pullbackFunctor_obj_module (f : Hom G H) (M : QuasicoherentModule H) :
    ((pullbackFunctor f).obj M).module =
      (Scheme.Modules.pullback f.mapObjects.left).obj M.module

Stacks.Groupoids.GroupoidScheme.pullbackFunctor_obj_alpha, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/PullbackFunctor.lean, line 228. The attribute's comment: “descent morphisms”.

Stacks Project, Tag 03LJ. The descent morphism of a pulled-back module is the canonical pullback of the original descent morphism.

theorem pullbackFunctor_obj_alpha (f : Hom G H) (M : QuasicoherentModule H) :
    Eq.ndrec (motive := fun X =>
      (Scheme.Modules.pullback G.target.left).obj X ⟶
        (Scheme.Modules.pullback G.source.left).obj X)
      ((pullbackFunctor f).obj M).alpha (pullbackFunctor_obj_module f M) =
      pullbackDescent f M

Stacks.Groupoids.GroupoidScheme.pullbackFunctor_map_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/PullbackFunctor.lean, line 239. The attribute's comment: “morphisms”.

Stacks Project, Tag 03LJ. Pullback of a morphism of quasi-coherent modules on a groupoid scheme is the usual pullback of morphisms of modules.

theorem pullbackFunctor_map_hom (f : Hom G H) {M N : QuasicoherentModule H} (g : M ⟶ N) :
    (pullbackFunctor_obj_module f M) ▸
      (pullbackFunctor_obj_module f N) ▸
        (QuasicoherentModule.Hom.hom ((pullbackFunctor f).map g)) =
      (Scheme.Modules.pullback f.mapObjects.left).map g.hom

Tag 09VH, a lemma

Tag 09VH in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.pushforwardFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/PushforwardDescent.lean, line 507. The attribute's comment: “the functor”. References: SGA 3 I (6.6.2), “more general”.

Stacks Project, Tag 09VH. Pushforward along a morphism of groupoid schemes, as a functor on quasi-coherent modules equipped with groupoid descent data: on objects it sends (𝓕, α) to (f_*𝓕, f_*α), and on morphisms it is the direct image of morphisms of modules.

noncomputable def pushforwardFunctor :
    QuasicoherentModule G ⥤ QuasicoherentModule H

Stacks.Groupoids.GroupoidScheme.pushforwardFunctor_obj_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/PushforwardDescent.lean, line 530. The attribute's comment: “underlying modules”.

Stacks Project, Tag 09VH. Pushforward along a morphism of groupoid schemes pushes the underlying module forward along the map on objects.

theorem pushforwardFunctor_obj_module (M : QuasicoherentModule G) :
    ((pushforwardFunctor f h).obj M).module =
      (Scheme.Modules.pushforward f.mapObjects.left).obj M.module

Stacks.Groupoids.GroupoidScheme.pushforwardFunctor_obj_alpha, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/PushforwardDescent.lean, line 538. The attribute's comment: “descent morphisms”.

Stacks Project, Tag 09VH. The descent morphism of a pushed-forward module is the pushed-forward descent morphism.

theorem pushforwardFunctor_obj_alpha (M : QuasicoherentModule G) :
    Eq.ndrec (motive := fun X =>
      (Scheme.Modules.pullback H.target.left).obj X ⟶
        (Scheme.Modules.pullback H.source.left).obj X)
      ((pushforwardFunctor f h).obj M).alpha (pushforwardFunctor_obj_module f h M) =
      pushforwardDescent f h M

Stacks.Groupoids.GroupoidScheme.pushforwardFunctor_map_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/PushforwardDescent.lean, line 549. The attribute's comment: “morphisms”.

Stacks Project, Tag 09VH. Pushforward of a morphism of quasi-coherent modules on a groupoid scheme is the direct image of morphisms of modules.

theorem pushforwardFunctor_map_hom {M N : QuasicoherentModule G} (g : M ⟶ N) :
    (pushforwardFunctor_obj_module f h M) ▸
      (pushforwardFunctor_obj_module f h N) ▸
        (QuasicoherentModule.Hom.hom ((pushforwardFunctor f h).map g)) =
      (Scheme.Modules.pushforward f.mapObjects.left).map
        (QuasicoherentModule.Hom.hom g)

Stacks.Groupoids.GroupoidScheme.pullbackPushforwardAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Equivariant/PushforwardDescent.lean, line 656. The attribute's comment: “right adjointness to the pullback functor of Tag 03LJ”.

Stacks Project, Tag 09VH. Pushforward along a morphism of groupoid schemes is right adjoint to the pullback functor of Tag 03LJ: on underlying modules the adjunction is the inverse-image--direct-image adjunction along the map on objects, under which the two compatibility conditions with the descent morphisms correspond.

noncomputable def pullbackPushforwardAdjunction :
    pullbackFunctor f ⊣ pushforwardFunctor f h

Tag 077R, a lemma

Tag 077R in the Stacks Project.

AlgebraicGeometry.instHasColimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidColimits.lean, line 252.

The category of quasi-coherent modules on a groupoid scheme admits all colimits.

instance instHasColimits {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S) :
    HasColimits (Stacks.Groupoids.GroupoidScheme.QuasicoherentModule G)

Tag 077S, a lemma

Tag 077S in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.QuasicoherentModule.abelian, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuasicoherentAbelian.lean, line 480. References: SGA 3 I (4.7.2.1), “Mod.q.c. case”.

Let S be a scheme and let G be a groupoid scheme over S whose source and target are flat. Then the category of quasi-coherent modules on G is abelian.

noncomputable instance abelian : Abelian (QuasicoherentModule G)

Sources

• Section 39.14, Tag 03LH
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Groupoids.GroupoidScheme.QuasicoherentModule · Stacks.Groupoids.GroupoidScheme.QuasicoherentModule.alpha_isIso · Stacks.Groupoids.GroupoidScheme.pullbackFunctor · Stacks.Groupoids.GroupoidScheme.pullbackFunctor_obj_module · Stacks.Groupoids.GroupoidScheme.pullbackFunctor_obj_alpha · Stacks.Groupoids.GroupoidScheme.pullbackFunctor_map_hom · Stacks.Groupoids.GroupoidScheme.pushforwardFunctor · Stacks.Groupoids.GroupoidScheme.pushforwardFunctor_obj_module

Section39.15 Colimits of quasi-coherent modules#

Section 39.15 of the Stacks Project, Tag 07TS. 7 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07TR, a lemma

Tag 07TR in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.isQuasicoherent_pushforwardSource_pullbackTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Coinduction.lean, line 178. The attribute's comment: “the quasi-coherence of s_* t^* 𝒢”.

The first assertion of Tag 07TR. For a groupoid scheme whose source map is quasi-compact and quasi-separated, the module s_* t^* 𝒢 is quasi-coherent.

theorem isQuasicoherent_pushforwardSource_pullbackTarget
    [QuasiCompact G.source.left] [QuasiSeparated G.source.left]
    (𝒢 : G.objects.left.Modules) [𝒢.IsQuasicoherent] :
    ((Scheme.Modules.pushforward G.source.left).obj
      ((Scheme.Modules.pullback G.target.left).obj 𝒢)).IsQuasicoherent

Stacks.Groupoids.GroupoidScheme.coinductionAlpha, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Coinduction.lean, line 217. The attribute's comment: “the construction of the canonical isomorphism α; not the cocycle and identity conditions making (s_* t^* 𝒢, α) a module on the groupoid, and not the functor to QCoh(U, R, s, t, c) nor its right adjointness to the forgetful functor”.

The canonical isomorphism α of Tag 07TR. For a groupoid scheme (U, R, s, t, c) with s and t flat, quasi-compact and quasi-separated and a quasi-coherent module 𝒢 on U, this is the canonical isomorphism t^* s_* t^* 𝒢 ≅ s^* s_* t^* 𝒢. It is the composite of the two flat base-change isomorphisms of the squares of the composition diagram with the identification of pr_0^* t^* 𝒢 and c^* t^* 𝒢.

This does not include the cocycle condition and the normalization along the identity section, which are what make (s_* t^* 𝒢, α) a quasi-coherent module on the groupoid scheme.

noncomputable def coinductionAlpha [Flat G.source.left] [Flat G.target.left]
    [QuasiCompact G.source.left] [QuasiSeparated G.source.left]
    (𝒢 : G.objects.left.Modules) [𝒢.IsQuasicoherent] :
    (Scheme.Modules.pullback G.target.left).obj
        ((Scheme.Modules.pushforward G.source.left).obj
          ((Scheme.Modules.pullback G.target.left).obj 𝒢)) ≅
      (Scheme.Modules.pullback G.source.left).obj
        ((Scheme.Modules.pushforward G.source.left).obj
          ((Scheme.Modules.pullback G.target.left).obj 𝒢))

Stacks.Groupoids.GroupoidScheme.coinductionAlpha_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Coinduction.lean, line 235. The attribute's comment: “the naturality of α in 𝒢”.

The canonical isomorphism α is natural in 𝒢, which is the sense in which the construction 𝒢 ↦ (s_* t^* 𝒢, α) is canonical.

theorem coinductionAlpha_naturality [Flat G.source.left] [Flat G.target.left]
    [QuasiCompact G.source.left] [QuasiSeparated G.source.left]
    {𝒢 𝒢' : G.objects.left.Modules} [𝒢.IsQuasicoherent] [𝒢'.IsQuasicoherent]
    (φ : 𝒢 ⟶ 𝒢') :
    (coinductionAlpha G 𝒢).hom ≫
        (Scheme.Modules.pullback G.source.left).map
          ((Scheme.Modules.pushforward G.source.left).map
            ((Scheme.Modules.pullback G.target.left).map φ)) =
      (Scheme.Modules.pullback G.target.left).map
          ((Scheme.Modules.pushforward G.source.left).map
            ((Scheme.Modules.pullback G.target.left).map φ)) ≫
        (coinductionAlpha G 𝒢').hom

Stacks.Groupoids.GroupoidScheme.coinductionAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/CoinductionAdjunction/Adjunction.lean, line 784. The attribute's comment: “the right adjointness of the coinduction functor to the forgetful functor”.

Coinduction is right adjoint to forgetting a groupoid descent datum. This is the adjunction of Tag 07TR.

noncomputable def coinductionAdjunction : quasicoherentForget G ⊣ coinduction G

Stacks.Groupoids.GroupoidScheme.cocycle_coinductionAlpha, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/CoinductionAdjunction/CocycleCondition.lean, line 327. The attribute's comment: “the cocycle condition for α, the first of the two conditions making (s_* t^* 𝒢, α) a quasi-coherent module on the groupoid scheme”.

The cocycle condition for the coinduction descent isomorphism. On the scheme of composable arrows, applying α to the two arrows in succession agrees with applying it to their composite.

theorem cocycle_coinductionAlpha
    [Flat G.source.left] [Flat G.target.left]
    [QuasiCompact G.source.left] [QuasiSeparated G.source.left]
    (𝒢 : G.objects.left.Modules) [𝒢.IsQuasicoherent] :
    successiveDescent G (coinductionAlpha G 𝒢).hom =
      reindexHom G.comp.left (coinductionAlpha G 𝒢).hom

Stacks.Groupoids.GroupoidScheme.identity_coinductionAlpha, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/CoinductionAdjunction/CocycleCondition.lean, line 412. The attribute's comment: “the normalization of α along the identity section, the second of the two conditions making (s_* t^* 𝒢, α) a quasi-coherent module on the groupoid scheme”.

The normalization of the coinduction descent isomorphism along the identity section. Pulling α back along the identity section gives the identity of s_* t^* 𝒢. With cocycle_coinductionAlpha this exhibits (s_* t^* 𝒢, α) as a quasi-coherent module on the groupoid scheme.

theorem identity_coinductionAlpha
    [Flat G.source.left] [Flat G.target.left]
    [QuasiCompact G.source.left] [QuasiSeparated G.source.left]
    (𝒢 : G.objects.left.Modules) [𝒢.IsQuasicoherent] :
    identityDescent G (coinductionAlpha G 𝒢).hom =
      𝟙 ((Scheme.Modules.pushforward G.source.left).obj
        ((Scheme.Modules.pullback G.target.left).obj 𝒢))

Tag 0GNF, a remark

Tag 0GNF in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.coinductionAdjunction_unit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/CoinductionAdjunction/Adjunction.lean, line 803.

Stacks 0GNF. The unit of the forgetful--coinduction adjunction at a quasi-coherent module (𝓕, α) on a groupoid scheme is, on underlying modules, the unit of the pullback--pushforward adjunction along the source followed by the direct image of the inverse of the descent morphism: 𝓕 ⟶ s_* s^* 𝓕 ⟶ s_* t^* 𝓕.

theorem coinductionAdjunction_unit_app (M : QuasicoherentModule G) :
    ((coinductionAdjunction G).unit.app M).hom =
      (Scheme.Modules.pullbackPushforwardAdjunction G.source.left).unit.app M.module ≫
        (Scheme.Modules.pushforward G.source.left).map (inv M.alpha)

Tag 07TT, a lemma

Tag 07TT in the Stacks Project.

AlgebraicGeometry.isCoherent_pullback_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/CoherentPullbackPushforward.lean, line 69.

Stacks Project, Tag 07TT. For a flat, surjective, quasi-compact and quasi-separated morphism f : Y ⟶ X of locally Noetherian schemes, a quasi-coherent module F on X and a coherent submodule G of f^*F, the fibre product of the unit F ⟶ f_* f^* F with the pushforward of the inclusion is coherent.

theorem isCoherent_pullback_pushforward {X Y : Scheme.{u}} (f : Y ⟶ X)
    [QuasiCompact f] [QuasiSeparated f] [Flat f] [Surjective f]
    [IsLocallyNoetherian X] [IsLocallyNoetherian Y]
    (F : X.Modules) [F.IsQuasicoherent]
    (G : Y.Modules) [G.IsQuasicoherent] [G.IsCoherent]
    (φ : G ⟶ (Scheme.Modules.pullback f).obj F) [Mono φ] :
    (pullback ((Scheme.Modules.pullbackPushforwardAdjunction f).unit.app F)
      ((Scheme.Modules.pushforward f).map φ)).IsCoherent

Tag 07TU, a lemma

Tag 07TU in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.exists_filtered_diagram_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/CoherentColimit.lean, line 826. The attribute's comment: “every quasi-coherent module on the groupoid scheme is the colimit of a filtered diagram of quasi-coherent modules on the groupoid scheme with coherent underlying modules”.

Stacks Project, Tag 07TU. Let (U, R, s, t, c) be a groupoid scheme over S with U and R Noetherian and with s and t flat, quasi-compact and quasi-separated. Then every quasi-coherent module (ℱ, β) on the groupoid scheme is the colimit of a filtered diagram of quasi-coherent modules on the groupoid scheme whose underlying modules on U are coherent.

theorem exists_filtered_diagram_of_isCoherent
    [IsNoetherian G.objects.left] [IsNoetherian G.arrows.left]
    [Flat G.source.left] [Flat G.target.left]
    [QuasiCompact G.source.left] [QuasiCompact G.target.left]
    [QuasiSeparated G.source.left] [QuasiSeparated G.target.left]
    (M : QuasicoherentModule G) :
    ∃ (I : Type (u + 1)) (inst : SmallCategory I),
      let _ := inst
      ∃ (_ : IsFiltered I) (D : I ⥤ QuasicoherentModule G)
        (φ : D ⟶ (Functor.const I).obj M),
        (∀ i, (D.obj i).module.IsCoherent) ∧
          Nonempty (IsColimit (Cocone.mk M φ))

Tag 07TV, a lemma

Tag 07TV in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.exists_filtered_diagram_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FiniteTypeStructure/GroupoidColimit.lean, line 1312.

Stacks Project, Tag 07TV. A quasi-coherent module on an affine groupoid scheme whose arrow ring is free over its object ring via the source map is a filtered colimit of finite-type groupoid modules.

theorem exists_filtered_diagram_of_isFiniteType
    {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsAffine G.objects.left] [IsAffine G.arrows.left]
    (hfree : letI : Algebra Γ(G.objects.left, ⊤) Γ(G.arrows.left, ⊤) :=
      G.source.left.appTop.hom.toAlgebra
      Module.Free Γ(G.objects.left, ⊤) Γ(G.arrows.left, ⊤))
    (M : QuasicoherentModule G) :
    ∃ (I : Type u) (inst : SmallCategory I),
      let _ := inst
      ∃ (_ : IsFiltered I)
        (D : I ⥤ QuasicoherentModule G)
        (φ : D ⟶ (Functor.const I).obj M),
        (∀ i, (D.obj i).module.IsFiniteType) ∧
          Nonempty (IsColimit (Cocone.mk M φ))

Tag 077T, a lemma

Tag 077T in the Stacks Project.

AlgebraicGeometry.essentiallySmall_isCardinalGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidCardinalGenerated.lean, line 87.

The κ-generated quasi-coherent modules on a groupoid scheme have only a set of isomorphism classes.

theorem essentiallySmall_isCardinalGenerated {S : Scheme.{u}}
    (G : Stacks.Groupoids.GroupoidScheme S) (κ : Cardinal.{u}) :
    ObjectProperty.EssentiallySmall.{u}
      (fun M : QuasicoherentModule G ↦
        Stacks.AlgebraicGeometry.CardinalGeneration.IsCardinalGenerated M.module κ)

Tag 077U, a lemma

Tag 077U in the Stacks Project.

Stacks.AlgebraicGeometry.GroupoidCardinalGeneration.cardinalBound, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidQuasicoherentColimit.lean, line 101. The attribute's comment: “cardinal”.

The cardinal of Stacks 077U. For a groupoid scheme it is the maximum of the cardinals Gabber's theorem attaches to the object scheme and to the arrow scheme; the closure construction producing the bounded submodules uses exactly that it is infinite and dominates the numbers of affine opens of the two schemes.

def cardinalBound {S : Scheme.{u}} (G : GroupoidScheme S) : Cardinal.{u}

Stacks.AlgebraicGeometry.GroupoidCardinalGeneration.cardinalGeneratedSubobject_isFiltered, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidQuasicoherentColimit.lean, line 294. The attribute's comment: “directedness”.

Stacks 077U, the directedness assertion, at the cardinal the tag attaches to the groupoid scheme.

instance cardinalGeneratedSubobject_isFiltered (M : QuasicoherentModule G) :
    IsFiltered (CardinalGeneratedSubobject M (cardinalBound G))

Stacks.AlgebraicGeometry.GroupoidCardinalGeneration.isColimit_cardinalGeneratedSubobjectCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/GroupoidQuasicoherentColimit.lean, line 384. The attribute's comment: “colimit”.

Stacks 077U, the colimit assertion. Every quasi-coherent module on a groupoid scheme with flat source and target is the colimit of the canonical diagram of its quasi-coherent submodules whose underlying module is generated by at most cardinalBound G local sections.

def isColimit_cardinalGeneratedSubobjectCocone (M : QuasicoherentModule G) :
    IsColimit (cardinalGeneratedSubobjectCocone M (cardinalBound G))

Sources

• Section 39.15, Tag 07TS
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Groupoids.GroupoidScheme.isQuasicoherent_pushforwardSource_pullbackTarget · Stacks.Groupoids.GroupoidScheme.coinductionAlpha · Stacks.Groupoids.GroupoidScheme.coinductionAlpha_naturality · Stacks.Groupoids.GroupoidScheme.coinductionAdjunction · Stacks.Groupoids.GroupoidScheme.cocycle_coinductionAlpha · Stacks.Groupoids.GroupoidScheme.identity_coinductionAlpha · Stacks.Groupoids.GroupoidScheme.coinductionAdjunction_unit_app · AlgebraicGeometry.isCoherent_pullback_pushforward

Section39.16 Groupoids and group schemes#

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

Tag 0234, a lemma

Tag 0234 in the Stacks Project.

AlgebraicGeometry.groupoidSchemeOfAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/OverField/ActionGroupoid.lean, line 210. References: SGA 3 V (10.2).

The action groupoid scheme of a group scheme action, with objects X, arrows G ×_Y X, and the source, target, composition, identity, and inverse maps given by the standard formulas.

noncomputable def groupoidSchemeOfAction : ActionGroupoidConstruction Y G X

Tag 03LL, a lemma

Tag 03LL in the Stacks Project.

AlgebraicGeometry.equivariantModuleEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/EquivariantModule.lean, line 336. The attribute's comment: “the canonical equivalence”.

Stacks Project, Tag 03LL. Equivariant quasi-coherent modules for an action of a group scheme are the same as quasi-coherent modules on the associated action groupoid scheme.

noncomputable def equivariantModuleEquivalence :
    EquivariantModule Y G X ≌
      GroupoidScheme.QuasicoherentModule (groupoidSchemeOfAction Y G X).groupoid

AlgebraicGeometry.equivariantModuleEquivalence_functor_obj_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/EquivariantModule.lean, line 355. The attribute's comment: “underlying module”.

Stacks Project, Tag 03LL. The canonical comparison leaves the underlying quasi-coherent module unchanged.

theorem equivariantModuleEquivalence_functor_obj_module (M : EquivariantModule Y G X) :
    ((toActionGroupoidModule Y G X).obj M).module = M.module

AlgebraicGeometry.equivariantModuleEquivalence_functor_obj_alpha, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/EquivariantModule.lean, line 362. The attribute's comment: “descent morphism”.

Stacks Project, Tag 03LL. The canonical comparison leaves the descent morphism unchanged.

theorem equivariantModuleEquivalence_functor_obj_alpha (M : EquivariantModule Y G X) :
    ((toActionGroupoidModule Y G X).obj M).alpha = M.alpha

AlgebraicGeometry.equivariantModuleEquivalence_functor_map_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/GroupSchemeProperties/EquivariantModule.lean, line 369. The attribute's comment: “morphisms”.

Stacks Project, Tag 03LL. On morphisms the canonical comparison is the identity on the underlying morphism of modules.

theorem equivariantModuleEquivalence_functor_map_hom {M N : EquivariantModule Y G X}
    (f : M ⟶ N) :
    ((toActionGroupoidModule Y G X).map f).hom = f.hom

Sources

• Section 39.16, Tag 03LK
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.groupoidSchemeOfAction · AlgebraicGeometry.equivariantModuleEquivalence · AlgebraicGeometry.equivariantModuleEquivalence_functor_obj_module · AlgebraicGeometry.equivariantModuleEquivalence_functor_obj_alpha · AlgebraicGeometry.equivariantModuleEquivalence_functor_map_hom

Section39.17 The stabilizer group scheme#

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

Tag 0235, a lemma

Tag 0235 in the Stacks Project.

AlgebraicGeometry.stabilizerGroupStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Basic.lean, line 412. References: SGA 3 V (10.2.1), “X-group scheme”.

Stacks Project, Tag 0235. The stabilizer of a groupoid scheme is canonically a group scheme over its object scheme, with multiplication induced by groupoid composition.

noncomputable def stabilizerGroupStructure {S : Scheme.{u}} (G : GroupoidScheme S) :
    { h : GrpObj (stabilizer G) // IsStabilizerGroupStructure G h }

Tag 0236, a definition

Tag 0236 in the Stacks Project.

AlgebraicGeometry.stabilizerGroupStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Basic.lean, line 412. The attribute's comment: “the stabilizer group scheme of a groupoid scheme”. References: SGA 3 V (10.2.1), “X-group scheme”.

Stacks Project, Tag 0235. The stabilizer of a groupoid scheme is canonically a group scheme over its object scheme, with multiplication induced by groupoid composition.

noncomputable def stabilizerGroupStructure {S : Scheme.{u}} (G : GroupoidScheme S) :
    { h : GrpObj (stabilizer G) // IsStabilizerGroupStructure G h }

Tag 0237, a lemma

Tag 0237 in the Stacks Project.

AlgebraicGeometry.stabilizerAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Action.lean, line 223.

The stabilizer group scheme acts canonically on the arrow scheme over the object scheme via the target map; the action is induced by composition in the groupoid.

noncomputable def stabilizerAction {S : Scheme.{u}} (G : GroupoidScheme S) :
    { h : ModObj (stabilizer G) (arrowsOverTarget G) // IsStabilizerAction G h }

Tag 04Q2, a lemma

Tag 04Q2 in the Stacks Project.

AlgebraicGeometry.stabilizerActionOverPairs, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/PairPseudotorsor.lean, line 691. The attribute's comment: “induced action”.

The stabilizer action on arrows induces the canonical action of the base-changed stabilizer on arrows over the pair scheme.

def stabilizerActionOverPairs {S : Scheme.{u}} (G : GroupoidScheme S) :
    { h : ModObj (stabilizerOverPairs G) (arrowsOverPairs G) // IsInducedAction G h }

AlgebraicGeometry.stabilizerActionOverPairs_pseudoTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/PairPseudotorsor.lean, line 718. The attribute's comment: “pseudo-torsor”.

The arrow scheme is a pseudo-torsor under the stabilizer over the pair scheme.

theorem stabilizerActionOverPairs_pseudoTorsor {S : Scheme.{u}}
    (G : GroupoidScheme S) :
    IsPseudoTorsor (stabilizerOverPairs G) (arrowsOverPairs G)

Tag 04Q3, a lemma

Tag 04Q3 in the Stacks Project.

AlgebraicGeometry.stabilizerActionOnFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Fiber.lean, line 78. The attribute's comment: “action on the fibre”.

The canonical action on the fibre, induced from the action over pairs.

def stabilizerActionOnFiber {S : Scheme.{u}} (G : GroupoidScheme S)
    (p : (G.objects ⊗ G.objects).left) :
    { h : ModObj (fiberGroup G p) (fiberArrows G p) // IsFiberAction G p h }

AlgebraicGeometry.fiber_isFpqcTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Fiber.lean, line 103. The attribute's comment: “torsor property”.

A nonempty fibre of the arrows over a pair is a torsor under the corresponding stabilizer group over the residue field.

theorem fiber_isFpqcTorsor {S : Scheme.{u}} (G : GroupoidScheme S)
    (p : (G.objects ⊗ G.objects).left) (h : Nonempty (fiberArrows G p).left) :
    IsFpqcTorsor
      (Scheme.Spec.obj (.op ((G.objects ⊗ G.objects).left.residueField p)))
      (fiberGroup G p) (fiberArrows G p)

Sources

• Section 39.17, Tag 03LM
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.stabilizerGroupStructure · AlgebraicGeometry.stabilizerAction · AlgebraicGeometry.stabilizerActionOverPairs · AlgebraicGeometry.stabilizerActionOverPairs_pseudoTorsor · AlgebraicGeometry.stabilizerActionOnFiber · AlgebraicGeometry.fiber_isFpqcTorsor

Section39.18 Restricting groupoids#

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

Tag 02VB, a lemma

Tag 02VB in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.restrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/RestrictionGroupoid.lean, line 69.

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

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

AlgebraicGeometry.GroupoidScheme.restrictGroupoid_isRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/RestrictionGroupoidDisplayed.lean, line 401.

Stacks Lemma 02VB. Let (U, R, s, t, c) be a groupoid scheme over S and g : U' ⟶ U a morphism. With R' = (U' ×_{g, U, t} R) ×_R (R ×_{s, U, g} U') the iterated fibre product of the displayed diagram, s' : R' ⟶ R ×_{s, U, g} U' ⟶ U' and t' : R' ⟶ U' ×_{g, U, t} R ⟶ U', the groupoid scheme restrictGroupoid G g is (U', R', s', t', c') for the canonical composition law c' = Stacks.Groupoids.GroupoidScheme.restrictionComposition, which is characterized as the morphism on composable pairs whose source, target and underlying arrow of R are those of the second factor, of the first factor, and the composite in R. The morphism of groupoid schemes restrictGroupoidHom G g is g on objects and the projection R' ⟶ R on arrows. Finally, on every scheme T over S, the functor of groupoids (U'(T), R'(T), s', t', c') ⟶ (U(T), R(T), s, t, c) is the restriction of (U(T), R(T), s, t, c) via U'(T) ⟶ U(T): there is an isomorphism of categories to the induced groupoid InducedCategory (U(T), R(T), s, t, c) (· ≫ g), the identity on objects, carrying the functor to the canonical functor inducedFunctor of the restriction.

theorem restrictGroupoid_isRestriction :
    (restrictGroupoid G g).objects = U' ∧
    (restrictGroupoid G g).arrows =
      pullback (pullback.snd g G.target) (pullback.fst G.source g) ∧
    (restrictGroupoid G g).source =
      pullback.snd (pullback.snd g G.target) (pullback.fst G.source g) ≫
        pullback.snd G.source g ∧
    (restrictGroupoid G g).target =
      pullback.fst (pullback.snd g G.target) (pullback.fst G.source g) ≫
        pullback.fst g G.target ∧
    (restrictGroupoid G g).comp = G.restrictionComposition g ∧
    (∀ {T : Over S} (a b : T ⟶ (restrictGroupoid G g).arrows)
        (w : a ≫ (restrictGroupoid G g).source = b ≫ (restrictGroupoid G g).target),
      (pullback.lift a b w ≫ (restrictGroupoid G g).comp) ≫ (restrictGroupoid G g).source =
          b ≫ (restrictGroupoid G g).source ∧
        (pullback.lift a b w ≫ (restrictGroupoid G g).comp) ≫ (restrictGroupoid G g).target =
          a ≫ (restrictGroupoid G g).target ∧
        (pullback.lift a b w ≫ (restrictGroupoid G g).comp) ≫
            (restrictGroupoidHom G g).mapArrows =
          G.compose (a ≫ (restrictGroupoidHom G g).mapArrows)
            (b ≫ (restrictGroupoidHom G g).mapArrows)
            (G.restriction_compose_condition g a b w)) ∧
    (restrictGroupoidHom G g).mapObjects = g ∧
    (restrictGroupoidHom G g).mapArrows =
      pullback.fst (pullback.snd g G.target) (pullback.fst G.source g) ≫
        pullback.snd g G.target ∧
    ∀ T : Over S,
      (∀ x, (restrictGroupoidEvaluationFunctor G g T).obj x = x) ∧
      restrictGroupoidEvaluationFunctor G g T ⋙ restrictGroupoidEvaluationInverse G g T =
        𝟭 _ ∧
      restrictGroupoidEvaluationInverse G g T ⋙ restrictGroupoidEvaluationFunctor G g T =
        𝟭 _ ∧
      restrictGroupoidEvaluationFunctor G g T ⋙
          inducedFunctor (restrictGroupoidEvaluationObj G g T) =
        (restrictGroupoidHom G g).evaluation T

Tag 02VC, a definition

Tag 02VC in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.restrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/RestrictionGroupoid.lean, line 69. The attribute's comment: “the restriction R|_{U'} of a groupoid scheme to U', with its morphism to the”.

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

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

Tag 02VD, a lemma

Tag 02VD in the Stacks Project.

AlgebraicGeometry.restriction_groupoidScheme_agrees_restriction_preRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/RestrictionRelation.lean, line 417.

Restricting groupoid schemes and restricting (pre-)equivalence relations agree via the constructions of Tags 0232 and 0233.

1. For a groupoid scheme G and g : U' ⟶ G.objects, the pre-relation of the restriction G|_{U'} (Tag 02VC) agrees with the restriction (Tag 02V9) of the pre-relation of G (Tag 0232): there is a unique isomorphism of their schemes of arrows compatible with the maps to U' ×_S U' and to the arrows of G.
2. For an equivalence relation j : R ⟶ U ×_S U and g : U' ⟶ U, the groupoid scheme of the restricted relation j|_{U'} (Tag 0233) agrees with the restriction to U' of the groupoid scheme of j: there is a unique isomorphism of groupoid schemes between them which is the identity of U' on objects and commutes with the maps of arrows to R. Being a pair of mutually inverse morphisms of groupoid schemes, it identifies the compositions, identities and inverses of the two groupoid structures.

theorem restriction_groupoidScheme_agrees_restriction_preRelation {S : Scheme.{u}} :
    (∀ (G : GroupoidScheme S) {U' : Over S} (g : U' ⟶ G.objects),
      ∃! e : (GroupoidScheme.restrict G g).groupoid.arrows ≅
          PreRelation.restriction (groupoidPreRelation G) g,
        e.hom ≫ PreRelation.restrict (groupoidPreRelation G) g =
            groupoidPreRelation (GroupoidScheme.restrict G g).groupoid ≫
              prod.map (eqToHom (GroupoidScheme.restrict G g).objects_eq)
                (eqToHom (GroupoidScheme.restrict G g).objects_eq) ∧
          e.hom ≫ pullback.snd (prod.map g g) (groupoidPreRelation G) =
            (GroupoidScheme.restrict G g).hom.mapArrows) ∧
    (∀ {R U U' : Over S} (j : PreRelation R U) [IsEquivalenceRelation j.target j.source]
        (g : U' ⟶ U),
      ∃! e : GroupoidScheme.Isomorphism
          (groupoidSchemeOfIsEquivalenceRelation (PreRelation.restrict j g))
          (GroupoidScheme.restrict (groupoidSchemeOfIsEquivalenceRelation j)
            (g ≫ eqToHom
              (groupoidSchemeOfIsEquivalenceRelation_extendsRelation j).objects_eq.symm)).groupoid,
        e.hom.mapObjects = eqToHom
            ((groupoidSchemeOfIsEquivalenceRelation_extendsRelation
                (PreRelation.restrict j g)).objects_eq.trans
              (GroupoidScheme.restrict _ _).objects_eq.symm) ∧
          e.hom.mapArrows ≫ (GroupoidScheme.restrict _ _).hom.mapArrows ≫
              eqToHom (groupoidSchemeOfIsEquivalenceRelation_extendsRelation j).arrows_eq =
            eqToHom (groupoidSchemeOfIsEquivalenceRelation_extendsRelation
                (PreRelation.restrict j g)).arrows_eq ≫ pullback.snd (prod.map g g) j)

Tag 04ML, a lemma

Tag 04ML in the Stacks Project.

AlgebraicGeometry.restrictStabilizerIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/RestrictionStabilizer.lean, line 238.

Stacks Project, Tag 04ML. The stabilizer of a restricted groupoid scheme is canonically the base change of the original stabilizer.

noncomputable def restrictStabilizerIso {S : Scheme.{u}} (G : GroupoidScheme S)
    {U' : Scheme.{u}} (g : U' ⟶ G.objects.left) :
    let U'_S : Over S := Over.mk (g ≫ G.objects.hom)
    let g' : U'_S ⟶ G.objects := Over.homMk g
    Over.mk ((stabilizer (GroupoidScheme.restrict G g').groupoid).hom ≫
      eqToHom (congrArg Over.left (GroupoidScheme.restrict G g').objects_eq)) ≅
      Over.mk (pullback.fst g (stabilizer G).hom)

Sources

• Section 39.18, Tag 02VA
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.GroupoidScheme.restrict · AlgebraicGeometry.GroupoidScheme.restrictGroupoid_isRestriction · AlgebraicGeometry.restriction_groupoidScheme_agrees_restriction_preRelation · AlgebraicGeometry.restrictStabilizerIso

Section39.19 Invariant subschemes#

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

Tag 03BC, a definition

Tag 03BC in the Stacks Project.

Stacks.Groupoids.IsInvariantClosedSubscheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Basic.lean, line 113. The attribute's comment: “part (3): invariant closed subschemes”.

A closed subscheme of the objects of a groupoid scheme is invariant when its scheme-theoretic inverse images along source and target agree.

abbrev IsInvariantClosedSubscheme {S : Scheme.{u}} (G : GroupoidScheme S)
    (Z : G.objects.left.IdealSheafData) : Prop

Stacks.Groupoids.IsInvariantMonomorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Basic.lean, line 120. The attribute's comment: “part (4): invariant monomorphisms”.

A monomorphism of schemes into the objects of a groupoid scheme is invariant when its source and target pullbacks define the same subobject of the arrow scheme.

abbrev IsInvariantMonomorphism {S : Scheme.{u}} (G : GroupoidScheme S) {T : Scheme.{u}}
    (i : T ⟶ G.objects.left) [Mono i] : Prop

Stacks.Groupoids.IsInvariantSet, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/InvariantSubscheme/Basic.lean, line 61. The attribute's comment: “part (1): set-theoretic invariance”.

Stacks Project, Tag 03BC, part (1). A subset of the objects of a groupoid scheme is invariant if every arrow starting in it also ends in it.

abbrev IsInvariantSet {S : AlgebraicGeometry.Scheme.{u}} (G : GroupoidScheme S)
    (W : Set G.objects.left) : Prop

Stacks.Groupoids.IsInvariantOpen, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/InvariantSubscheme/Basic.lean, line 68. The attribute's comment: “part (2): invariant opens”.

Stacks Project, Tag 03BC, part (2). An open subscheme of the objects of a groupoid scheme is invariant if its underlying set is.

abbrev IsInvariantOpen {S : AlgebraicGeometry.Scheme.{u}} (G : GroupoidScheme S)
    (W : G.objects.left.Opens) : Prop

Tag 03LO, a lemma

Tag 03LO in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.isInvariantSet_target_image_source_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/InvariantSubscheme/Basic.lean, line 88. The attribute's comment: “part (1): set-theoretic invariance”.

Stacks Project, Tag 03LO (1). The saturation of any subset by the arrows of a groupoid scheme is invariant.

theorem isInvariantSet_target_image_source_preimage {S : Scheme.{u}}
    (G : Stacks.Groupoids.GroupoidScheme S) (W : Set G.objects.left) :
    IsInvariantSet G (G.target.left.base '' (G.source.left.base ⁻¹' W))

AlgebraicGeometry.GroupoidScheme.isOpen_target_image_source_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/InvariantSubscheme/Basic.lean, line 106. The attribute's comment: “part (2): invariant open saturation”.

Stacks Project, Tag 03LO (2). The saturation of an open set is open when the target map is an open map.

theorem isOpen_target_image_source_preimage {S : Scheme.{u}}
    (G : Stacks.Groupoids.GroupoidScheme S)
    (ht : IsOpenMap G.target.left.base)
    (W : G.objects.left.Opens) :
    IsOpen (G.target.left.base '' (G.source.left.base ⁻¹' (W : Set G.objects.left)))

AlgebraicGeometry.GroupoidScheme.exists_invariant_compact_open_neighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/InvariantSubscheme/Basic.lean, line 117. The attribute's comment: “part (3): invariant quasi-compact open covering”.

Stacks Project, Tag 03LO (3). If the target map is open and the source map is quasi-compact, every point of the object scheme has an invariant quasi-compact open neighbourhood.

theorem exists_invariant_compact_open_neighborhood {S : Scheme.{u}}
    (G : Stacks.Groupoids.GroupoidScheme S)
    (ht : IsOpenMap G.target.left.base)
    [QuasiCompact G.source.left]
    (x : G.objects.left) :
    ∃ V : G.objects.left.Opens,
      x ∈ (V : Set G.objects.left) ∧
        IsInvariantOpen G V ∧ IsCompact (V : Set G.objects.left)

AlgebraicGeometry.GroupoidScheme.exists_isInvariantOpen_eq_target_image_source_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/ConstructingInvariantOpens.lean, line 145. The attribute's comment: “(2) t(s⁻¹(W)) is an invariant open subscheme”.

Stacks Project, Tag 03LO, part (2). If the target map of a groupoid scheme is open then the saturation t(s⁻¹(W)) of an open subscheme W of the object scheme is an invariant open subscheme.

theorem exists_isInvariantOpen_eq_target_image_source_preimage
    (ht : IsOpenMap G.target.left.base) (W : G.objects.left.Opens) :
    ∃ V : G.objects.left.Opens,
      (V : Set G.objects.left) =
        G.target.left.base '' (G.source.left.base ⁻¹' (W : Set G.objects.left)) ∧
      (W : Set G.objects.left) ⊆ (V : Set G.objects.left) ∧ IsInvariantOpen G V

AlgebraicGeometry.GroupoidScheme.exists_isInvariantOpen_isCompact_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/ConstructingInvariantOpens.lean, line 174. The attribute's comment: “(3) covering by invariant quasi-compact opens”.

Stacks Project, Tag 03LO, part (3). If the target map of a groupoid scheme is open and its source map is quasi-compact, then the object scheme has an open covering consisting of invariant quasi-compact open subschemes.

theorem exists_isInvariantOpen_isCompact_cover [QuasiCompact G.source.left]
    (ht : IsOpenMap G.target.left.base) :
    ∃ (ι : Type u) (V : ι → G.objects.left.Opens),
      (∀ i, IsInvariantOpen G (V i)) ∧
      (∀ i, IsCompact (V i : Set G.objects.left)) ∧
      ⨆ i, V i = ⊤

Tag 0APA, a lemma

Tag 0APA in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.target_image_source_preimage_eq_iInter_compact_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/InvariantOpen.lean, line 60.

The target-image of the source-preimage of a quasi-compact open in the object scheme of a flat quasi-compact groupoid is an intersection of a nonempty family of quasi-compact opens.

theorem target_image_source_preimage_eq_iInter_compact_open
    {S : Scheme.{u}} (G : Stacks.Groupoids.GroupoidScheme S)
    [QuasiCompact G.source.left] [Flat G.source.left]
    [QuasiCompact G.target.left] [Flat G.target.left]
    [QuasiSeparatedSpace G.objects.left]
    (W : G.objects.left.Opens) (hW : IsCompact (W : Set G.objects.left)) :
    ∃ (I : Type u) (_ : Nonempty I) (V : I → Set G.objects.left),
      (∀ i, IsOpen (V i) ∧ IsCompact (V i)) ∧
        G.target.left.base '' (G.source.left.base ⁻¹' (W : Set G.objects.left)) = ⋂ i, V i

Tag 0APB, a lemma

Tag 0APB in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.exists_invariant_open_between_compact_opens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/InvariantSubscheme/FlatGroupoid.lean, line 118.

Stacks Project, Tag 0APB. A quasi-compact open in the object scheme of a quasi-compact flat groupoid scheme has an invariant open neighbourhood contained in a quasi-compact open.

theorem exists_invariant_open_between_compact_opens
    (G : GroupoidScheme S)
    [QuasiCompact G.source.left] [Flat G.source.left]
    [QuasiCompact G.target.left] [Flat G.target.left]
    [QuasiSeparatedSpace G.objects.left]
    (W : G.objects.left.Opens) (hW : IsCompact (W : Set G.objects.left)) :
    ∃ (V W' : G.objects.left.Opens),
      IsInvariantOpen G V ∧ IsCompact (W' : Set G.objects.left) ∧
        W ≤ V ∧ V ≤ W'

AlgebraicGeometry.GroupoidScheme.exists_isInvariantOpen_isCompact_between, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/InvariantOpenBetween.lean, line 103.

Let (U, R, s, t, c) be a groupoid scheme with s and t quasi-compact and flat and with U quasi-separated, and let W ⊆ U be a quasi-compact open. Then there is an invariant open V and a quasi-compact open W' with W ⊆ V ⊆ W' ⊆ U.

theorem exists_isInvariantOpen_isCompact_between
    [QuasiCompact G.source.left] [Flat G.source.left]
    [QuasiCompact G.target.left] [Flat G.target.left]
    [QuasiSeparatedSpace G.objects.left]
    (W : G.objects.left.Opens) (hW : IsCompact (W : Set G.objects.left)) :
    ∃ V W' : G.objects.left.Opens,
      IsInvariantOpen G V ∧ IsCompact (W' : Set G.objects.left) ∧
        (W : Set G.objects.left) ⊆ (V : Set G.objects.left) ∧
        (V : Set G.objects.left) ⊆ (W' : Set G.objects.left)

Sources

• Section 39.19, Tag 03LN
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Groupoids.IsInvariantClosedSubscheme · Stacks.Groupoids.IsInvariantMonomorphism · Stacks.Groupoids.IsInvariantSet · Stacks.Groupoids.IsInvariantOpen · AlgebraicGeometry.GroupoidScheme.isInvariantSet_target_image_source_preimage · AlgebraicGeometry.GroupoidScheme.isOpen_target_image_source_preimage · AlgebraicGeometry.GroupoidScheme.exists_invariant_compact_open_neighborhood · AlgebraicGeometry.GroupoidScheme.exists_isInvariantOpen_eq_target_image_source_preimage

Section39.20 Quotient sheaves#

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

Tag 02VF, an equation

Tag 02VF in the Stacks Project.

Stacks.Groupoids.quotientPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuotientSheaf.lean, line 110. References: SGA 3 IV (3.1.2), “special case”.

Stacks 02VF. The quotient presheaf of a pre-relation, the coequalizer of its two maps on the restricted functors of points: it sends a test object T to the quotient of U(T) by the equivalence relation generated by the image of R(T).

noncomputable def quotientPresheaf (F : C ⥤ Over S) {R U : Over S}
    (j : PreRelation R U) : Cᵒᵖ ⥤ Type u

Tag 02VG, a definition

Tag 02VG in the Stacks Project.

Stacks.Groupoids.quotientSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuotientSheaf.lean, line 122.

Stacks 02VG. The quotient sheaf of a pre-relation, the sheafification of its quotient presheaf.

noncomputable abbrev quotientSheaf (J : GrothendieckTopology C)
    [HasSheafify J (Type u)] (F : C ⥤ Over S) {R U : Over S}
    (j : PreRelation R U) : Sheaf J (Type u)

Tag 03BD, a definition

Tag 03BD in the Stacks Project.

Stacks.Groupoids.PreRelation.HasRepresentableQuotient, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/RepresentableQuotient.lean, line 46. The attribute's comment: “pre-relation: representable quotient”. References: SGA 3 IV (3.3.2), “(ii)”.

A pre-relation has a representable quotient when its quotient sheaf U/R is represented by an object of the site.

noncomputable abbrev PreRelation.HasRepresentableQuotient (J : GrothendieckTopology C)
    [HasSheafify J (Type u)] (F : C ⥤ Over S) {R U : Over S}
    (j : PreRelation R U) : Prop

Stacks.Groupoids.GroupoidScheme.HasRepresentableQuotient, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/RepresentableQuotient.lean, line 54. The attribute's comment: “groupoid scheme: representable quotient”. References: SGA 3 IV (3.3.2), “(ii)”.

A groupoid scheme has a representable quotient when the quotient sheaf U/R of its pre-relation (t, s) is represented by an object of the site.

noncomputable abbrev GroupoidScheme.HasRepresentableQuotient (J : GrothendieckTopology C)
    [HasSheafify J (Type u)] (F : C ⥤ Over S) (G : GroupoidScheme S) : Prop

Tag 03C5, a lemma

Tag 03C5 in the Stacks Project.

Stacks.Groupoids.isIso_quotientSheafToPoints_baseOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/RepresentabilityBigSites.lean, line 114.

Stacks 03C5. Let τ be one of the Zariski, étale, smooth, syntomic and fppf topologies, let j : R ⟶ U ×_S U be a pre-relation of S-schemes, and let f : U ⟶ M be a morphism of S-schemes equalizing its source and its target. If f induces a surjection of τ-sheaves on the functors of points, and if (t, s) : R ⟶ U ×_M U induces one too, then M represents the quotient sheaf U/R: the canonical map U/R ⟶ h_M is an isomorphism.

The source's three hypotheses are hf, hU and hR, in that order. Nothing is assumed about the functor of points of M: it is a τ-sheaf by Stacks.Groupoids.isSheaf_points_baseOver, and neither M nor R is assumed to be an object of the site.

theorem isIso_quotientSheafToPoints_baseOver {R U M : Over S} (j : PreRelation R U) (f : U ⟶ M)
    (hf : j.target ≫ f = j.source ≫ f)
    (hU : Presheaf.IsLocallySurjective (BigFppfOver.baseOverTopology B S hS τ)
      ((Over.post (X := B.obj hS) B.inclusion).op.whiskerLeft (yoneda.map f)))
    (hR : Presheaf.IsLocallySurjective (BigFppfOver.baseOverTopology B S hS τ)
      ((Over.post (X := B.obj hS) B.inclusion).op.whiskerLeft
        (yoneda.map (pullback.lift j.target j.source hf)))) :
    IsIso (quotientSheafToPoints (BigFppfOver.baseOverTopology B S hS τ)
      (Over.post (X := B.obj hS) B.inclusion) j f hf
      (isSheaf_points_baseOver B S hS τ M))

Tag 045Y, a lemma

Tag 045Y in the Stacks Project.

Stacks.Groupoids.toQuotientSheaf_apply_eq_iff_locally_related, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuotientSheafEquality.lean, line 134.

Stacks 045Y. Two T-valued points of U have the same image in the quotient sheaf of a pre-equivalence relation if and only if, on some covering sieve of T, their restrictions are the source and the target of a point of the relation scheme.

theorem toQuotientSheaf_apply_eq_iff_locally_related
    {S : Scheme.{u}} {C : Type v} [Category.{w} C]
    (J : GrothendieckTopology C) [HasSheafify J (Type u)]
    [J.WEqualsLocallyBijective (Type u)]
    (F : C ⥤ Over S) {R U : Over S} (j : PreRelation R U)
    (hj : IsPreEquivalenceRelation j)
    (T : C) (a b : F.obj T ⟶ U) :
    (toQuotientSheaf J F j).app (op T) a = (toQuotientSheaf J F j).app (op T) b ↔
      ∃ W : Sieve T, W ∈ J T ∧
        ∀ (X : C) (f : X ⟶ T), W.arrows f →
          ∃ r : F.obj X ⟶ R,
            (r ≫ j.source = F.map f ≫ a) ∧ (r ≫ j.target = F.map f ≫ b)

Tag 045Z, a lemma

Tag 045Z in the Stacks Project.

Stacks.Groupoids.restrictQuotientSheafMap_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuotientSheafRestriction.lean, line 115. The attribute's comment: “injectivity”. References: SGA 3 IV (4.4.10), “Monomorphism clause”.

Stacks 045Z, injectivity. Restricting a pre-equivalence relation induces an injective map U'/R' ⟶ U/R of quotient sheaves.

theorem restrictQuotientSheafMap_mono (hj : IsPreEquivalenceRelation j) :
    Mono (restrictQuotientSheafMap J F j g)

Stacks.Groupoids.restrictQuotientSheafMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuotientSheafRestriction.lean, line 149. The attribute's comment: “isomorphism under surjectivity”.

Stacks 045Z, bijectivity. If g induces a local surjection on restricted functors of points, then the induced map U'/R' ⟶ U/R of quotient sheaves is an isomorphism.

theorem restrictQuotientSheafMap_isIso (hj : IsPreEquivalenceRelation j)
    (hg : Presheaf.IsLocallySurjective J (F.op.whiskerLeft (yoneda.map g))) :
    IsIso (restrictQuotientSheafMap J F j g)

Tag 02VH, a lemma

Tag 02VH in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.mono_restrictionQuotientMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/GroupoidRestriction.lean, line 387. The attribute's comment: “injectivity of the quotient map”.

Stacks 02VH. The map from the quotient sheaf of a restricted groupoid scheme to the quotient sheaf of the original one is injective.

theorem mono_restrictionQuotientMap (J : GrothendieckTopology C)
    [HasSheafify J (Type u)] (F : C ⥤ Over S) (G : GroupoidScheme S)
    {U' : Over S} (g : U' ⟶ G.objects) (H : Restriction G g) :
    Mono (restrictionQuotientMap J F G g H)

AlgebraicGeometry.GroupoidScheme.isIso_restrictionQuotientMap_of_reach, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/GroupoidRestriction.lean, line 399. The attribute's comment: “bijectivity when the reach map is surjective”.

Stacks 02VH. If every object is locally the source of an arrow whose target lifts along g, then the map of quotient sheaves induced by the restriction is bijective.

theorem isIso_restrictionQuotientMap_of_reach (J : GrothendieckTopology C)
    [HasSheafify J (Type u)] (F : C ⥤ Over S) (G : GroupoidScheme S)
    {U' : Over S} (g : U' ⟶ G.objects) (H : Restriction G g)
    (hreach : Sheaf.IsLocallySurjective ((presheafToSheaf J (Type u)).map
      (F.op.whiskerLeft (yoneda.map (restrictionReachMap G g))))) :
    IsIso (restrictionQuotientMap J F G g H)

AlgebraicGeometry.GroupoidScheme.isIso_restrictionQuotientMap_of_objects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/GroupoidRestriction.lean, line 439. The attribute's comment: “bijectivity when the restricting map is surjective”.

Stacks 02VH. If the restricting map is locally surjective on functors of points, then the map of quotient sheaves induced by the restriction is bijective.

theorem isIso_restrictionQuotientMap_of_objects (J : GrothendieckTopology C)
    [HasSheafify J (Type u)] (F : C ⥤ Over S) (G : GroupoidScheme S)
    {U' : Over S} (g : U' ⟶ G.objects) (H : Restriction G g)
    (hg : Sheaf.IsLocallySurjective
      ((presheafToSheaf J (Type u)).map (F.op.whiskerLeft (yoneda.map g)))) :
    IsIso (restrictionQuotientMap J F G g H)

AlgebraicGeometry.GroupoidScheme.isIso_restrictionQuotientMap_of_reach_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/GroupoidRestriction.lean, line 452. The attribute's comment: “bijectivity when the reach map is a covering”.

Stacks 02VH. If the reach map is, up to isomorphisms identifying its source and its target with objects of the site, a singleton covering, then the map of quotient sheaves induced by the restriction is bijective.

theorem isIso_restrictionQuotientMap_of_reach_cover (J : GrothendieckTopology C)
    [HasSheafify J (Type u)] (F : C ⥤ Over S) (hF : F.Full) (G : GroupoidScheme S)
    {U' : Over S} (g : U' ⟶ G.objects) (H : Restriction G g)
    (X Y : C) (eX : F.obj X ≅ pullback g G.target) (eY : F.obj Y ≅ G.objects)
    (a : X ⟶ Y) (ha : F.map a ≫ eY.hom = eX.hom ≫ restrictionReachMap G g)
    (hcover : Sieve.generate (Presieve.singleton a) ∈ J Y) :
    IsIso (restrictionQuotientMap J F G g H)

AlgebraicGeometry.GroupoidScheme.isIso_restrictionQuotientMap_of_objects_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/GroupoidRestriction.lean, line 467. The attribute's comment: “bijectivity when the restricting map is a covering”.

Stacks 02VH. If the restricting map is, up to isomorphisms identifying its source and its target with objects of the site, a singleton covering, then the map of quotient sheaves induced by the restriction is bijective.

theorem isIso_restrictionQuotientMap_of_objects_cover (J : GrothendieckTopology C)
    [HasSheafify J (Type u)] (F : C ⥤ Over S) (hF : F.Full) (G : GroupoidScheme S)
    {U' : Over S} (g : U' ⟶ G.objects) (H : Restriction G g)
    (X Y : C) (eX : F.obj X ≅ U') (eY : F.obj Y ≅ G.objects)
    (a : X ⟶ Y) (ha : F.map a ≫ eY.hom = eX.hom ≫ g)
    (hcover : Sieve.generate (Presieve.singleton a) ∈ J Y) :
    IsIso (restrictionQuotientMap J F G g H)

Tag 07S3, a lemma

Tag 07S3 in the Stacks Project.

AlgebraicGeometry.isPullback_toQuotientSheaf_overTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/BigSitePullbackSquare.lean, line 117.

Stacks 07S3. Let S be a scheme and let (r, f) be a morphism of equivalence relations j : R ⟶ U ×_S U and j' : R' ⟶ U' ×_S U' over S whose square on source maps is cartesian. Then for each of the Zariski, étale, smooth, syntomic and fppf topologies the square formed by the two quotient maps and by f is a fibre product square of τ-sheaves: U is the fibre product of U' and U/R over U'/R'.

The topology is quantified over AlgebraicGeometry.CoveringTopology, so the single statement is the five of the source. The two schemes of objects U and U' are the schemes presented by objects of the site; the two schemes of relations are arbitrary schemes over S.

theorem isPullback_toQuotientSheaf_overTopology (τ : CoveringTopology) (B : BigSite.{u} τ)
    (S : Scheme.{u}) (hS : S.size < cutoff τ B)
    {R R' : CategoryTheory.Over S} {U U' : CategoryTheory.Over (base B S hS)}
    (j : PreRelation R ((overToSlice τ B S hS).obj U))
    (j' : PreRelation R' ((overToSlice τ B S hS).obj U'))
    [IsEquivalenceRelation j.target j.source] [IsEquivalenceRelation j'.target j'.source]
    (r : R ⟶ R')
    (f : (overToSlice τ B S hS).obj U ⟶ (overToSlice τ B S hS).obj U')
    (hs : r ≫ j'.source = j.source ≫ f) (ht : r ≫ j'.target = j.target ≫ f)
    (hcart : IsPullback r j.source j'.source f) :
    IsPullback (toQuotientSheaf (overTopology τ B S hS) (overToSlice τ B S hS) j)
      ((overToSlice τ B S hS).op.whiskerLeft (yoneda.map f))
      (quotientSheafMap (overTopology τ B S hS) (overToSlice τ B S hS) j j' r f hs ht).hom
      (toQuotientSheaf (overTopology τ B S hS) (overToSlice τ B S hS) j')

Sources

• Section 39.20, Tag 02VE
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Groupoids.quotientPresheaf · Stacks.Groupoids.quotientSheaf · Stacks.Groupoids.PreRelation.HasRepresentableQuotient · Stacks.Groupoids.GroupoidScheme.HasRepresentableQuotient · Stacks.Groupoids.isIso_quotientSheafToPoints_baseOver · Stacks.Groupoids.toQuotientSheaf_apply_eq_iff_locally_related · Stacks.Groupoids.restrictQuotientSheafMap_mono · Stacks.Groupoids.restrictQuotientSheafMap_isIso

Section39.21 Descent in terms of groupoids#

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

Tag 0APD, a definition

Tag 0APD in the Stacks Project.

AlgebraicGeometry.IsCartesian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Cartesian.lean, line 45. The attribute's comment: “the cartesian condition”.

A morphism of groupoid schemes is cartesian if its square of source maps is a pullback.

abbrev IsCartesian {S : Scheme.{u}} {G H : GroupoidScheme S}
    (F : GroupoidScheme.Hom G H) : Prop

AlgebraicGeometry.CartesianOver, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Cartesian.lean, line 51. The attribute's comment: “groupoid schemes cartesian over a fixed groupoid scheme”.

A groupoid scheme cartesian over a fixed groupoid scheme H.

structure CartesianOver {S : Scheme.{u}} (H : GroupoidScheme S)

AlgebraicGeometry.CartesianOver.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Cartesian.lean, line 62. The attribute's comment: “morphisms cartesian over a fixed groupoid scheme”.

A morphism of groupoid schemes cartesian over H is a morphism compatible with both components of the structure morphisms to H.

structure CartesianOver.Hom {S : Scheme.{u}} {H : GroupoidScheme S}
    (X Y : CartesianOver H)

Tag 0APE, a lemma

Tag 0APE in the Stacks Project.

AlgebraicGeometry.nonempty_cartesianOverEquivariantEquivalenceData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Equivariant/Equivalence.lean, line 719. The attribute's comment: “the equivalence with the forward construction in the proof”.

There is an equivalence between groupoid schemes cartesian over G and equivariant schemes for G satisfying the equations of CartesianOverEquivariantEquivalenceData on objects, descent isomorphisms, and morphisms.

theorem nonempty_cartesianOverEquivariantEquivalenceData
    {S : Scheme.{u}} (G : GroupoidScheme S) :
    Nonempty (CartesianOverEquivariantEquivalenceData G)

AlgebraicGeometry.cartesianOverEquivalenceEquivariantScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Equivariant/Equivalence.lean, line 757.

Cartesian groupoid schemes over G are equivalent to schemes over the object scheme of G endowed with a normalized cocyclic pullback isomorphism.

noncomputable def cartesianOverEquivalenceEquivariantScheme
    {S : Scheme.{u}} (G : GroupoidScheme S) :
    CartesianOver G ≌ EquivariantScheme G

Tag 0APF, a lemma

Tag 0APF in the Stacks Project.

AlgebraicGeometry.cartesianOverEquivDescentDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/PairGroupoidDescent.lean, line 769. The attribute's comment: “the equivalence for the base scheme equal to the target of f”.

Groupoid schemes cartesian over the pair groupoid (X, X ×_S X, s, t, c), as a groupoid scheme over S, are the same thing as descent data relative to X/S.

def cartesianOverEquivDescentDatum (f : X ⟶ S) :
    CartesianOver (pairGroupoid f) ≌ DescentDatum f

AlgebraicGeometry.cartesianOverPairGroupoidEquivDescentDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/PairGroupoidDescentGeneral.lean, line 62. The attribute's comment: “the equivalence for a morphism of schemes over a base S, the general case”.

Tag 0APF. Let S be a scheme and let f : X ⟶ Y be a morphism of schemes over S, the structure morphism of Y being g : Y ⟶ S. Groupoid schemes over S cartesian over the pair groupoid (X, X ×_Y X, \mathrm{pr}_1, \mathrm{pr}_0, \mathrm{pr}_{02}) are the same thing as descent data relative to X/Y.

def cartesianOverPairGroupoidEquivDescentDatum {S Y X : Scheme.{u}} (g : Y ⟶ S) (f : X ⟶ Y) :
    CartesianOver ((pairGroupoid f).pushforward g) ≌ DescentDatum f

Sources

• Section 39.21, Tag 0APC
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.IsCartesian · AlgebraicGeometry.CartesianOver · AlgebraicGeometry.CartesianOver.Hom · AlgebraicGeometry.nonempty_cartesianOverEquivariantEquivalenceData · AlgebraicGeometry.cartesianOverEquivalenceEquivariantScheme · AlgebraicGeometry.cartesianOverEquivDescentDatum · AlgebraicGeometry.cartesianOverPairGroupoidEquivDescentDatum

Section39.22 Separation conditions#

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

Tag 02YH, a lemma

Tag 02YH in the Stacks Project.

AlgebraicGeometry.diagonalDiagram_commutes, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/DiagonalDiagram.lean, line 446. The attribute's comment: “commutativity of the diagram”.

The left-hand part of the displayed diagonal diagram commutes.

lemma diagonalDiagram_commutes {S : Scheme.{u}} (G : GroupoidScheme S) :
    arrowDiagonal G ≫ bottomComparison G = topComparison G ≫ rightVertical G

AlgebraicGeometry.topComparison_isIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/DiagonalDiagram.lean, line 480. The attribute's comment: “the upper horizontal arrow”.

The upper comparison morphism in the diagonal diagram is an isomorphism.

lemma topComparison_isIso {S : Scheme.{u}} (G : GroupoidScheme S) :
    IsIso (topComparison G)

AlgebraicGeometry.bottomComparison_isIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/DiagonalDiagram.lean, line 614. The attribute's comment: “the lower horizontal arrow”.

The lower comparison morphism in the diagonal diagram is an isomorphism, with inverse (f, h) ↦ (f, f ∘ h).

lemma bottomComparison_isIso {S : Scheme.{u}} (G : GroupoidScheme S) :
    IsIso (bottomComparison G)

AlgebraicGeometry.rightSquare_isPullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/DiagonalDiagram.lean, line 621. The attribute's comment: “the right square”.

The right-hand square in the diagonal diagram is a pullback square.

lemma rightSquare_isPullback {S : Scheme.{u}} (G : GroupoidScheme S) :
    IsPullback (pullback.snd G.source (𝟙 G.objects)) (rightVertical G)
      (identityStabilizer G) (pullback.snd G.source
        (pullback.snd (sourceTarget G) (diagonal G)))

Tag 02YI, a lemma

Tag 02YI in the Stacks Project.

AlgebraicGeometry.sourceTarget_quasiSeparated_iff_stabilizer_quasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Separation.lean, line 132. The attribute's comment: “quasi_separated_equivalences”.

The source-target morphism is quasi-separated exactly when the stabilizer is quasi-separated over the object scheme.

theorem sourceTarget_quasiSeparated_iff_stabilizer_quasiSeparated
    {S : Scheme.{u}} (G : GroupoidScheme S) :
    QuasiSeparated (sourceTarget G).left ↔ QuasiSeparated (stabilizer G).hom

AlgebraicGeometry.stabilizer_quasiSeparated_iff_identity_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Separation.lean, line 142. The attribute's comment: “quasi_separated_equivalences”.

The stabilizer is quasi-separated exactly when its identity section is quasi-compact.

theorem stabilizer_quasiSeparated_iff_identity_quasiCompact
    {S : Scheme.{u}} (G : GroupoidScheme S) :
    QuasiSeparated (stabilizer G).hom ↔ QuasiCompact (identityStabilizer G).left

AlgebraicGeometry.sourceTarget_isSeparated_iff_stabilizer_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Separation.lean, line 203. The attribute's comment: “separated_equivalences”.

The source-target morphism is separated exactly when the stabilizer is separated over the object scheme.

theorem sourceTarget_isSeparated_iff_stabilizer_isSeparated
    {S : Scheme.{u}} (G : GroupoidScheme S) :
    IsSeparated (sourceTarget G).left ↔ IsSeparated (stabilizer G).hom

AlgebraicGeometry.stabilizer_isSeparated_iff_identity_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/Stabilizer/Separation.lean, line 212. The attribute's comment: “separated_equivalences”. References: SGA 3 II (4.11.4), “more general”.

The stabilizer is separated exactly when its identity section is a closed immersion.

theorem stabilizer_isSeparated_iff_identity_isClosedImmersion
    {S : Scheme.{u}} (G : GroupoidScheme S) :
    IsSeparated (stabilizer G).hom ↔ IsClosedImmersion (identityStabilizer G).left

Sources

• Section 39.22, Tag 02YG
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.diagonalDiagram_commutes · AlgebraicGeometry.topComparison_isIso · AlgebraicGeometry.bottomComparison_isIso · AlgebraicGeometry.rightSquare_isPullback · AlgebraicGeometry.sourceTarget_quasiSeparated_iff_stabilizer_quasiSeparated · AlgebraicGeometry.stabilizer_quasiSeparated_iff_identity_quasiCompact · AlgebraicGeometry.sourceTarget_isSeparated_iff_stabilizer_isSeparated · AlgebraicGeometry.stabilizer_isSeparated_iff_identity_isClosedImmersion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.