Lean declarations

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

instance instIsAlgebraicGroup (G S : Scheme) [G.Over S]
    [IsAffineGroupScheme G S] [LocallyOfFiniteType (G ↘ S)] :
    IsAlgebraicGroup G S where

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

class IsAlgebraicGroup (G S : Scheme) [G.Over S]
    extends IsAffineGroupScheme G S, LocallyOfFiniteType (G ↘ S)

/-- Reverse synthesis: an `IsAffineGroupScheme G S` instance is built from a
`GrpObj` on `Scheme.asOver G S` together with an `IsAffineHom` on
`G ↘ S`. -/

Modules: LanglandsLean.AlgebraicGeometry.IsAlgebraicGroup

Algebraic Group over a Base

Let \(S\) be a scheme. An algebraic group over \(S\) is an affine group scheme \(G\) over \(S\) whose structure morphism \(G \to S\) is locally of finite type.

Following the modern convention (Milne, Algebraic Groups; SGA 3), we do not require \(G\) to be smooth over \(S\). Smoothness is a separate hypothesis added where the theory needs it (for example, to identify the identity component or to make a Lie-algebra argument work). Important non-smooth examples include \(\mu_n\) and \(\alpha_p\) over a field of characteristic \(p\).

In the project's Lean development this is the typeclass aggregator \(\texttt{IsAlgebraicGroup}\,G\,S\), which extends \(\texttt{IsAffineGroupScheme}\,G\,S\) and \(\texttt{LocallyOfFiniteType}\,(G \downarrow S)\). When the base \(S\) is the spectrum of a field, the term linear algebraic group is also used (Milne / Borel / Humphreys / Springer).

Algebraic Group over a Base

Used by