Lean declarations

structure Langlands.AlgebraicGeometry.FaithfulLinearRepresentation LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.FaithfulRepresentation

structure FaithfulLinearRepresentation
    {k : Type u} [Field k] (G : Scheme.{u})
    [G.Over (Spec (.of k))]
    [IsAlgebraicGroup G (Spec (.of k))] where
  /-- The representation space. -/
  V : Type u
  [addCommGroup : AddCommGroup V]
  [module : Module k V]
  [finiteDimensional : FiniteDimensional k V]
  /-- The scheme-theoretic `GL(V)` target. -/
  generalLinear : GeneralLinearGroupSchemeModel k V
  /-- The representation morphism. -/
  rho : G ⟶ generalLinear.carrier
  /-- The morphism is over `Spec k`. -/
  rhoIsOver : rho.IsOver (Spec (.of k))
  /-- The morphism is a homomorphism of group objects in `Over (Spec k)`.

  The `IsMonObj`/`MonObj` instances come from the `GrpObj` structures on
  `G` (via `IsAlgebraicGroup`) and on `generalLinear.carrier`. -/
  rhoIsMonHom : letI := rhoIsOver; IsMonHom (rho.asOver (Spec (.of k)))
  /-- Faithfulness: the underlying morphism of schemes is a closed immersion. -/
  isClosedImmersion_rho : IsClosedImmersion rho

structure Langlands.AlgebraicGeometry.GeneralLinearGroupSchemeModel LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.FaithfulRepresentation

structure GeneralLinearGroupSchemeModel (k : Type u) [Field k] (V : Type v)
    [AddCommGroup V] [Module k V] [FiniteDimensional k V] where
  /-- The scheme modelling `GL(V)`. -/
  carrier : Scheme.{u}
  /-- The structure morphism to `Spec k`. -/
  over : carrier.Over (Spec (.of k))
  /-- The group object structure on `GL(V)`. -/
  grpObj : GrpObj (Scheme.asOver carrier (Spec (.of k)))

Modules: LanglandsLean.AlgebraicGeometry.FaithfulRepresentation

Faithful Linear Representation

Let \(k\) be a field and \(G\) an algebraic group over \(\operatorname{Spec} k\). A faithful finite-dimensional representation of \(G\) consists of:

a finite-dimensional \(k\)-vector space \(V\);
a scheme-theoretic model of the general linear group \(\operatorname{GL}(V)\), namely a scheme over \(\operatorname{Spec} k\) equipped with a group object structure realizing the functor \(R \mapsto \operatorname{GL}_R(V \otimes_k R)\);
a morphism of group schemes \(\rho : G \to \operatorname{GL}(V)\) over \(\operatorname{Spec} k\);
the requirement that the underlying morphism of schemes \(\rho\) is a closed immersion.

Equivalently, a faithful finite-dimensional representation exhibits \(G\) as a closed subgroup scheme of some scheme-theoretic \(\operatorname{GL}_n\).

In the project's Lean development the data above is packaged as the structure \(\texttt{FaithfulLinearRepresentation}\,G\), with the scheme-theoretic \(\operatorname{GL}(V)\) abstracted as \(\texttt{GeneralLinearGroupSchemeModel}\,k\,V\) (an interface to be realized concretely in Phase D4). The existence statement (embedding theorem) is recorded as a separate node; its proof is the subject of Phase B.

Faithful Linear Representation

Used by