Lean declarations

def Langlands.AlgebraicGeometry.Examples.GLV LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.GLV
```
noncomputable def GLV : Over (Scheme.Spec.obj (op R)) :=
  GLn.over R (Module.finrank R V)
```
noncomputable abbrev Langlands.AlgebraicGeometry.Examples.GLVSch LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.GLV
The underlying scheme of `GLV R V`.
```
noncomputable abbrev GLVSch : Scheme.{u}
```

Modules: LanglandsLean.AlgebraicGeometry.Examples.GLV

General Linear Group Scheme GL(V)

For a finite free \(R\)-module \(V\), the general linear group scheme \(\mathrm{GL}(V)\) is the affine group scheme representing the functor \[ S \;\mapsto\; \mathrm{GL}_{R}(V \otimes_R \mathcal{O}_S). \]

When \(V = R^n\), this recovers \(\mathrm{GL}_n\) as a special case. The coordinate ring perspective: \(\mathcal{O}(\mathrm{GL}(V)) = \mathrm{Sym}(V \otimes_R V^*)[\det^{-1}]\).

Lean Formalization

The Lean 4 formalization provides:

GLV: the group scheme object
GLVSch: the scheme underlying GL(V)

as elements of Langlands.AlgebraicGeometry.Examples.

References

SGA 3, Exposé I–III.
Demazure–Gabriel, Groupes algébriques (1970).