Documentation

TauCeti.Algebra.AlgebraicGroup.LinearlyReductive

Linearly reductive commutative Hopf algebras #

An affine group over a field is linearly reductive when its finite-dimensional rational representations are completely reducible. This file packages the existing comodule formulation as an isomorphism-invariant object property on commutative Hopf algebras. The property tests comodule carriers in the base field's universe; transport to a finite standard basis then shows that this covers carriers in every universe.

The property is deliberately separate from smoothness, connectedness, and finite type. In positive characteristic a torus is linearly reductive, while a general reductive group need not be. The comparison with reductivity defined by a trivial geometric unipotent radical belongs later in the theory: for smooth connected affine groups, reductive and linearly reductive are equivalent in characteristic zero.

Main declarations #

References #

This is the complete-reducibility side of Layer 6, "Reductive and semisimple groups", in the ReductiveGroups roadmap.

The organization follows TauCeti/Algebra/AlgebraicGroup/Unipotent/Basic.lean.

source
def TauCeti.linearlyReductiveCommHopfAlgProperty (k : Type u) [Field k] :
CategoryTheory.ObjectProperty (CommHopfAlgCat k)

The object property selecting commutative Hopf algebras for which every finite-dimensional comodule is completely reducible. It tests carriers in the base field's universe, which suffices for carriers in every universe by finite-dimensional transport.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.linearlyReductiveCommHopfAlgProperty_iff (k : Type u) [Field k] (H : CommHopfAlgCat k) :
    linearlyReductiveCommHopfAlgProperty k H ↔ Coalgebra.IsLinearlyReductive k ↑H

    Membership in the linearly reductive commutative-Hopf-algebra property means that every finite-dimensional comodule with carrier in the base field's universe is completely reducible.

    source
    instance TauCeti.instIsClosedUnderIsomorphismsCommHopfAlgCatLinearlyReductiveCommHopfAlgProperty (k : Type u) [Field k] :
    (linearlyReductiveCommHopfAlgProperty k).IsClosedUnderIsomorphisms

    Linear reductivity is invariant under isomorphism of commutative Hopf algebras.

    source
    theorem TauCeti.linearlyReductiveCommHopfAlgProperty_monoidAlgebra (k : Type u) [Field k] (G : Type v) [CommGroup G] :
    linearlyReductiveCommHopfAlgProperty k ↧(MonoidAlgebra k G)

    The monoid algebra of a commutative group is a linearly reductive commutative Hopf algebra.

    source
    theorem TauCeti.linearlyReductiveCommHopfAlgProperty.of_baseChange {k : Type u} [Field k] (K : Type w) [Field K] [Algebra k K] {H : CommHopfAlgCat k} (hH : linearlyReductiveCommHopfAlgProperty K (CommHopfAlgCat.baseChange H)) :
    linearlyReductiveCommHopfAlgProperty k H

    Linear reductivity descends along field extensions. A commutative Hopf algebra over k is linearly reductive as soon as its scalar extension to some extension field K is.

    source
    theorem TauCeti.linearlyReductiveCommHopfAlgProperty.of_injective {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (hf : Function.Injective ⇑(CommHopfAlgCat.Hom.hom f)) (hK : linearlyReductiveCommHopfAlgProperty k K) :
    linearlyReductiveCommHopfAlgProperty k H

    An injective coordinate morphism of commutative Hopf algebras preserves linear reductivity from its codomain to its domain. In particular, it applies to a quotient affine-group projection with an injective coordinate morphism.

    source
    @[reducible, inline]
    abbrev TauCeti.LinearlyReductiveCommHopfAlgCat (k : Type u) [Field k] :
    Type (max u (v + 1))

    The category of linearly reductive commutative Hopf algebras over a field.

    Equations
    Instances For