Lean declarations

instance Langlands.AlgebraicGeometry.instIsAffineGroupScheme LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.IsAlgebraicGroup

instance instIsAffineGroupScheme (G S : Scheme) [G.Over S]
    [GrpObj (Scheme.asOver G S)] [IsAffineHom (G ↘ S)] :
    IsAffineGroupScheme G S where

class Langlands.AlgebraicGeometry.IsAffineGroupScheme LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.IsAlgebraicGroup

class IsAffineGroupScheme (G S : Scheme) [G.Over S]
    extends GrpObj (Scheme.asOver G S), IsAffineHom (G ↘ S)

/-- `G` is an (affine) algebraic group over `S`: an affine group scheme that
is locally of finite type. Following Milne / SGA 3, no smoothness assumed;
smoothness is added separately as `[Smooth (G ↘ S)]` where needed.

This is the Level-1 sugar aggregator over the Mathlib stack
`GrpObj (Scheme.asOver G S)` + `IsAffineHom (G ↘ S)` +
`LocallyOfFiniteType (G ↘ S)`. -/

Modules: LanglandsLean.AlgebraicGeometry.IsAlgebraicGroup

Affine Group Scheme over a Base

Let \(S\) be a scheme. An affine group scheme over \(S\) is a scheme \(G\) together with:

a structure morphism \(G \to S\), making \(G\) an object of the slice category \(\mathsf{Over}(S)\);
a group object structure on \(G\) in \(\mathsf{Over}(S)\), supplied by morphisms

\[ m : G \times_S G \to G, \qquad e : S \to G, \qquad i : G \to G, \]

subject to the standard associativity, unit, and inverse axioms for group objects in a cartesian category; 3. an affineness assumption: the structure morphism \(G \to S\) is affine (the preimage of any affine open of \(S\) is an affine scheme).

In the project's Lean development this is the typeclass aggregator \(\texttt{IsAffineGroupScheme}\,G\,S\), which extends \(\texttt{GrpObj}(\operatorname{asOver}\,G\,S)\) and \(\texttt{IsAffineHom}\,(G \downarrow S)\). No smoothness or finite-type assumption is imposed; those are added separately via additional typeclasses when the theory requires them.

Affine Group Scheme over a Base

Used by