Lean declarations

instance Langlands.AlgebraicGeometry.points.instGroup LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Points

The `R`-points of `G` form a group, via Mathlib's `Hom.group`.

noncomputable instance points.instGroup (k : Type u) [Field k]
    (G : Scheme.{u}) [G.Over (Spec (CommRingCat.of k))]
    [GrpObj (Scheme.asOver G (Spec (CommRingCat.of k)))]
    (R : Type u) [CommRing R] [Algebra k R] :
    Group (points k G R) :=
  inferInstance

theorem Langlands.AlgebraicGeometry.points.map_is_group_hom LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Points

theorem points.map_is_group_hom (k : Type u) [Field k]
    (G : Scheme.{u}) [G.Over (Spec (CommRingCat.of k))]
    [GrpObj (Scheme.asOver G (Spec (CommRingCat.of k)))]
    {R R' : Type u} [CommRing R] [Algebra k R] [CommRing R'] [Algebra k R']
    (f : R →ₐ[k] R') (p q : points k G R) :
    points.map k G f (p * q) = points.map k G f p * points.map k G f q

Modules: LanglandsLean.AlgebraicGeometry.Points

R-Points of a Group Scheme Form a Group

Let $k$ be a field, $G$ an affine group scheme over $\operatorname{Spec} k$, and $R$ a commutative $k$-algebra. Then the set of $R$-points $G(R)$ carries a canonical group structure, with multiplication, identity, and inverse defined pointwise from the group object structure of $G$ in $\mathsf{Over}(\operatorname{Spec} k)$.

Furthermore, for any $k$-algebra homomorphism $f : R \to R'$, the induced map $G(R) \to G(R')$ (sending a $\operatorname{Spec} k$-morphism $\operatorname{Spec} R \to G$ to its precomposition with $\operatorname{Spec}(f) : \operatorname{Spec} R' \to \operatorname{Spec} R$) is a group homomorphism.

Proof

The category $\mathsf{Over}(\operatorname{Spec} k)$ is Cartesian monoidal (it has all binary products and a terminal object), so for any group object $G$ in it and any object $X$, the hom set $\operatorname{Hom}(X, G)$ inherits a group structure: multiplication is the composition $\operatorname{Hom}(X, G) \times \operatorname{Hom}(X, G) \to \operatorname{Hom}(X, G \times G) \to \operatorname{Hom}(X, G)$ where the second arrow is induced by the multiplication $G \times G \to G$. The identity element is the constant map at $e : 1 \to G$, and the inverse is post-composition with $i : G \to G$. The group axioms on $\operatorname{Hom}(X, G)$ follow from the group object axioms on $G$. Taking $X = \operatorname{Spec} R$ (canonically over $\operatorname{Spec} k$ via the algebra map) gives the group structure on $G(R)$. Functoriality in $R$ reduces to compatibility of composition with the group operations, which is automatic.
$\square$