Documentation

TauCeti.Algebra.AlgebraicGroup.Tangent.Lie.Adjoint.Ideal

Lie ideals as adjoint subrepresentations #

For a connected affine group of finite type over an algebraically closed field of characteristic zero, Lie ideals in its tangent Lie algebra are exactly the subrepresentations of its adjoint representation. The identification preserves the underlying subspace and its order. In particular, it turns the solvable radical of the tangent Lie algebra into an adjoint subrepresentation, an input to the comparison of group and Lie-algebra radicals.

Over an arbitrary commutative ring, an adjoint subcomodule is still a Lie ideal. The converse uses characteristic zero and connectedness through the equivalence between Lie-stable subspaces and subcomodules, via Submodule.coact_mem_range_of_forall_differential_mem.

References #

source
noncomputable def TauCeti.Subcomodule.toLieIdeal {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (Bialgebra.CotangentSpace R H)] [Module.Projective R (Bialgebra.CotangentSpace R H)] (N : Subcomodule R H (Module.Dual R (Bialgebra.CotangentSpace R H))) :
LieIdeal R (Module.Dual R (Bialgebra.CotangentSpace R H))

An adjoint subcomodule is a Lie ideal, without smoothness or characteristic assumptions.

Instances For
    source
    @[simp]
    theorem TauCeti.Subcomodule.toLieIdeal_toSubmodule {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (Bialgebra.CotangentSpace R H)] [Module.Projective R (Bialgebra.CotangentSpace R H)] (N : Subcomodule R H (Module.Dual R (Bialgebra.CotangentSpace R H))) :
    ↑N.toLieIdeal = N.toSubmodule

    Passage from an adjoint subcomodule to a Lie ideal preserves the underlying submodule.

    source
    @[simp]
    theorem TauCeti.Subcomodule.mem_toLieIdeal {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (Bialgebra.CotangentSpace R H)] [Module.Projective R (Bialgebra.CotangentSpace R H)] (N : Subcomodule R H (Module.Dual R (Bialgebra.CotangentSpace R H))) (x : Module.Dual R (Bialgebra.CotangentSpace R H)) :
    x ∈ N.toLieIdeal ↔ x ∈ N

    Membership in the Lie ideal is membership in the original adjoint subcomodule.

    source
    noncomputable def LieIdeal.toAdjointSubcomodule {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))) :
    TauCeti.Subcomodule k (↑H.obj) (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))

    A Lie ideal of a connected affine group in characteristic zero is a subrepresentation of its adjoint representation, over an algebraically closed field.

    Instances For
      source
      @[simp]
      theorem LieIdeal.toAdjointSubcomodule_toSubmodule {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))) :
      I.toAdjointSubcomodule.toSubmodule = ↑I

      Passage from a Lie ideal to an adjoint subcomodule preserves the underlying submodule.

      source
      @[simp]
      theorem LieIdeal.mem_toAdjointSubcomodule {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))) (x : Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj)) :
      x ∈ I.toAdjointSubcomodule ↔ x ∈ I

      Membership in the adjoint subcomodule is membership in the original Lie ideal.

      source
      @[simp]
      theorem LieIdeal.toAdjointSubcomodule_toLieIdeal {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (TauCeti.Bialgebra.CotangentSpace k ↑H.obj))) :
      I.toAdjointSubcomodule.toLieIdeal = I

      Passing from a Lie ideal to its adjoint subcomodule and back recovers the ideal.

      source
      @[simp]
      theorem TauCeti.Subcomodule.toLieIdeal_toAdjointSubcomodule {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (N : Subcomodule k (↑H.obj) (Module.Dual k (Bialgebra.CotangentSpace k ↑H.obj))) :
      N.toLieIdeal.toAdjointSubcomodule = N

      Passing from an adjoint subcomodule to its Lie ideal and back recovers the subcomodule.

      source
      noncomputable def TauCeti.adjointSubcomoduleOrderIsoLieIdeal {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) [ConnectedSpace (PrimeSpectrum ↑H.obj)] :
      Subcomodule k (↑H.obj) (Module.Dual k (Bialgebra.CotangentSpace k ↑H.obj)) ≃o LieIdeal k (Module.Dual k (Bialgebra.CotangentSpace k ↑H.obj))

      For a connected affine group over an algebraically closed field of characteristic zero, adjoint subrepresentations and Lie ideals are the same ordered collection of subspaces.

      Instances For
        source
        @[simp]
        theorem TauCeti.adjointSubcomoduleOrderIsoLieIdeal_apply {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) [ConnectedSpace (PrimeSpectrum ↑H.obj)] (N : Subcomodule k (↑H.obj) (Module.Dual k (Bialgebra.CotangentSpace k ↑H.obj))) :
        (adjointSubcomoduleOrderIsoLieIdeal H) N = N.toLieIdeal

        The order isomorphism sends a subcomodule to its Lie ideal.

        source
        @[simp]
        theorem TauCeti.adjointSubcomoduleOrderIsoLieIdeal_symm_apply {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) [ConnectedSpace (PrimeSpectrum ↑H.obj)] (I : LieIdeal k (Module.Dual k (Bialgebra.CotangentSpace k ↑H.obj))) :
        (adjointSubcomoduleOrderIsoLieIdeal H).symm I = I.toAdjointSubcomodule

        The inverse order isomorphism sends a Lie ideal to its adjoint subcomodule.