Embedding a finite-type affine group in a general linear group

Let H be a commutative Hopf algebra of finite type over a field k. The fundamental theorem of coalgebras places a finite set of algebra generators of H in a finite-dimensional subcomodule M of the regular comodule. The matrix coefficients of M then generate H as a k-algebra. After choosing a finite basis of M, every matrix coefficient is a linear combination of the entries of its coefficient matrix. Hence the associated coordinate morphism

O(GLₙ) ⟶ H

is surjective. Contravariantly, its spectrum is a closed immersion of the affine group scheme represented by H into GLₙ.

The coordinate-algebra statement permits independent universes for k and H. The final group-scheme statement uses the same universe for them, as required by Mathlib's current hopfSpec construction.

Main declarations

• TauCeti.Comodule.matrixCoefficientSubalgebra_le_coordinateBialgHom_range: the matrix coefficient subalgebra is contained in the range of the coordinate morphism.
• TauCeti.Comodule.exists_coordinateBialgHom_surjective: a finite-type commutative Hopf algebra over a field admits a finite-dimensional regular subcomodule whose coordinate morphism from O(GLₙ) is surjective.
• TauCeti.Comodule.exists_isClosedImmersion_coordinateGroupSchemeHom: the group scheme represented by a finite-type commutative Hopf algebra embeds as a closed subgroup of some GLₙ.
• TauCeti.AffineGroupSchemeCat.exists_isClosedImmersion_generalLinear: every finite-type affine group scheme over a field embeds as a closed subgroup of some GLₙ.

References

This is the coordinate-algebra form of the affine-group embedding theorem; see J. S. Milne, Algebraic Groups (2017), Proposition 4.7 and Theorem 4.9. It advances Layer 1, "Embedding theorem (hard)", of the ReductiveGroups roadmap.

theorem TauCeti.Comodule.matrixCoefficientSubalgebra_le_coordinateBialgHom_range {k : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) : matrixCoefficientSubalgebra ≤ (↑(coordinateBialgHom b)).range

The matrix coefficient subalgebra of a finite free comodule is contained in the range of its coordinate bialgebra morphism.

theorem TauCeti.Comodule.exists_coordinateBialgHom_surjective {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] : ∃ (M : Subcomodule k H H) (n : ℕ) (b : Module.Basis (Fin n) k ↥M), Function.Surjective ⇑(coordinateBialgHom b)

A finite-type commutative Hopf algebra over a field is a quotient of the coordinate ring of some general linear group. More precisely, it has a finite-dimensional subcomodule of its regular comodule and a basis for which the associated coordinate bialgebra morphism O(GLₙ) → H is surjective.

Contravariantly, the affine group scheme represented by H embeds as a closed subgroup of GLₙ.

noncomputable def TauCeti.Comodule.coordinateGroupSchemeHom {k H M : Type u} {n : ℕ} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) : (AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op ↧H) ⟶ GeneralLinear.groupScheme k n

The morphism from the affine group scheme represented by H to GLₙ associated to a comodule with a basis indexed by Fin n.

This is relative spectrum applied contravariantly to the comodule's coordinate Hopf-algebra morphism O(GLₙ) ⟶ H.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Comodule.coordinateGroupSchemeHom_def {k H M : Type u} {n : ℕ} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) : coordinateGroupSchemeHom b = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧k).map (CommHopfAlgCat.ofHom (coordinateBialgHom b)).op) (CategoryTheory.eqToHom ⋯)

The group-scheme morphism associated to a comodule is the relative spectrum of its coordinate Hopf-algebra morphism, followed by the defining identification of GLₙ.

@[simp]

theorem TauCeti.Comodule.isClosedImmersion_coordinateGroupSchemeHom_iff {k H M : Type u} {n : ℕ} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid M] [Module k M] [Comodule k H M] (b : Module.Basis (Fin n) k M) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (coordinateGroupSchemeHom b).hom.hom) ↔ Function.Surjective ⇑(coordinateBialgHom b)

The group-scheme morphism associated to a finite free comodule is a closed immersion if and only if its coordinate Hopf-algebra morphism is surjective.

theorem TauCeti.Comodule.exists_isClosedImmersion_coordinateGroupSchemeHom {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] : ∃ (M : Subcomodule k H H) (n : ℕ) (b : Module.Basis (Fin n) k ↥M), AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (coordinateGroupSchemeHom b).hom.hom)

The affine group scheme represented by a finite-type commutative Hopf algebra over a field embeds as a closed subgroup of some general linear group. More precisely, a finite-dimensional subcomodule of the regular comodule and a basis determine a closed immersion into GLₙ.

theorem TauCeti.AffineGroupSchemeCat.exists_isClosedImmersion_generalLinear {k : Type u} [Field k] (G : AffineGroupSchemeCat ↧k) [AlgebraicGeometry.LocallyOfFiniteType G.obj.X.hom] : ∃ (n : ℕ) (f : G.obj ⟶ GeneralLinear.groupScheme k n), AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left f.hom.hom)

Every finite-type affine group scheme over a field embeds as a closed subgroup of some general linear group.