Normal-subgroup equivariant linear maps

For the normal closed subgroup cut out by a Hopf ideal I in a reduced finite-type Hopf algebra H over an algebraically closed field, the subgroup-invariant vectors in the linear Hom comodule form an ambient subcomodule. The source is finite-dimensional and the target is arbitrary; the Hom criteria work over any commutative base ring with a finite projective source. Its elements are exactly the maps intertwining the subgroup's actions over its coordinate algebra, equivalently over every commutative coefficient algebra. No reducedness is assumed for the subgroup or for the coefficient algebra.

Applied to endomorphisms of a representation spanned by subgroup character spaces, this is the conjugation representation on subgroup-equivariant endomorphisms. Such endomorphisms preserve every character space. This representation is used to realize normal closed subgroups as kernels of representations.

The construction uses HopfIdeal.IsNormal.weightSpaceOneSubcomodule, the existing Comodule.linearHom and its scalar-extension conjugation formula; subgroup invariance is detected at the universal subgroup point rather than at rational points of the subgroup.

References

• J. E. Humphreys, Linear Algebraic Groups, §11.5.
• A. Borel, Linear Algebraic Groups, §5.5.

@[simp]

theorem TauCeti.HopfIdeal.mem_weightSpace_linearHom_one_iff {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {M : Type w} {N : Type x} [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] [Module.Finite R M] [Module.Projective R M] (I : HopfIdeal R H) (f : M →ₗ[R] N) : f ∈ I.weightSpace (M →ₗ[R] N) 1 ↔ LinearMap.baseChange (H ⧸ I.toIdeal) f ∘ₗ Comodule.endOfPoint M (Ideal.Quotient.mkₐ R I.toIdeal) = Comodule.endOfPoint N (Ideal.Quotient.mkₐ R I.toIdeal) ∘ₗ LinearMap.baseChange (H ⧸ I.toIdeal) f

A linear map is subgroup-invariant in the Hom comodule precisely when its scalar extension intertwines the actions of the universal subgroup point.

theorem TauCeti.HopfIdeal.baseChange_comp_endOfPoint_of_mem_weightSpace_linearHom_one {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {M : Type w} {N : Type x} [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] [Module.Finite R M] [Module.Projective R M] (I : HopfIdeal R H) {B : Type y} [CommSemiring B] [Algebra R B] (g : H ⧸ I.toIdeal →ₐ[R] B) {f : M →ₗ[R] N} (hf : f ∈ I.weightSpace (M →ₗ[R] N) 1) : LinearMap.baseChange B f ∘ₗ Comodule.endOfPoint M (g.comp (Ideal.Quotient.mkₐ R I.toIdeal)) = Comodule.endOfPoint N (g.comp (Ideal.Quotient.mkₐ R I.toIdeal)) ∘ₗ LinearMap.baseChange B f

A subgroup-invariant linear map intertwines subgroup actions over every commutative value algebra, including nonreduced algebras.

theorem TauCeti.HopfIdeal.mem_weightSpace_linearHom_one_iff_forall_baseChange_comp_endOfPoint {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {M : Type w} {N : Type x} [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] [Module.Finite R M] [Module.Projective R M] (I : HopfIdeal R H) (f : M →ₗ[R] N) : f ∈ I.weightSpace (M →ₗ[R] N) 1 ↔ ∀ (B : Type v) [inst : CommSemiring B] [inst_1 : Algebra R B] (g : H ⧸ I.toIdeal →ₐ[R] B), LinearMap.baseChange B f ∘ₗ Comodule.endOfPoint M (g.comp (Ideal.Quotient.mkₐ R I.toIdeal)) = Comodule.endOfPoint N (g.comp (Ideal.Quotient.mkₐ R I.toIdeal)) ∘ₗ LinearMap.baseChange B f

Subgroup invariance is equivalent to intertwining every algebra-valued subgroup point.

theorem TauCeti.HopfIdeal.comp_mem_weightSpace_linearHom_one {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {M : Type w} {N : Type x} [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] [Module.Finite R M] [Module.Projective R M] (I : HopfIdeal R H) {P : Type y} [AddCommGroup P] [Module R P] [Comodule R H P] [Module.Finite R N] [Module.Projective R N] {f : N →ₗ[R] P} {g : M →ₗ[R] N} (hf : f ∈ I.weightSpace (N →ₗ[R] P) 1) (hg : g ∈ I.weightSpace (M →ₗ[R] N) 1) : f ∘ₗ g ∈ I.weightSpace (M →ₗ[R] P) 1

Composites of subgroup-equivariant linear maps are subgroup-equivariant.

theorem TauCeti.HopfIdeal.map_mem_weightSpace_of_mem_weightSpace_linearHom_one {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {M : Type w} {N : Type x} [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] [Module.Finite R M] [Module.Projective R M] (I : HopfIdeal R H) {f : M →ₗ[R] N} (hf : f ∈ I.weightSpace (M →ₗ[R] N) 1) {χ : GroupLike R (H ⧸ I.toIdeal)} {m : M} (hm : m ∈ I.weightSpace M χ) : f m ∈ I.weightSpace N χ

Subgroup-equivariant linear maps preserve every scheme-theoretic character space.

theorem TauCeti.HopfIdeal.mem_weightSpace_linearHom_one_iff_forall_mapsTo_weightSpace {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {M : Type w} {N : Type x} [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] [Module.Finite R M] [Module.Projective R M] (I : HopfIdeal R H) (hspan : ⨆ (χ : GroupLike R (H ⧸ I.toIdeal)), I.weightSpace M χ = ⊤) (f : M →ₗ[R] N) : f ∈ I.weightSpace (M →ₗ[R] N) 1 ↔ ∀ (χ : GroupLike R (H ⧸ I.toIdeal)), Set.MapsTo ⇑f ↑(I.weightSpace M χ) ↑(I.weightSpace N χ)

When subgroup character spaces span the source, equivariance is equivalent to preserving each character space.

@[simp]

theorem TauCeti.HopfIdeal.IsNormal.mem_weightSpaceOneSubcomodule_linearHom_iff {H : Type v} [CommRing H] {k : Type u} [Field k] [IsAlgClosed k] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] {V : Type w} {W : Type x} [AddCommGroup V] [Module k V] [Comodule k H V] [AddCommGroup W] [Module k W] [Comodule k H W] [FiniteDimensional k V] {J : HopfIdeal k H} (hJ : J.IsNormal) (f : V →ₗ[k] W) : f ∈ weightSpaceOneSubcomodule (V →ₗ[k] W) hJ ↔ LinearMap.baseChange (H ⧸ J.toIdeal) f ∘ₗ Comodule.endOfPoint V (Ideal.Quotient.mkₐ k J.toIdeal) = Comodule.endOfPoint W (Ideal.Quotient.mkₐ k J.toIdeal) ∘ₗ LinearMap.baseChange (H ⧸ J.toIdeal) f

The normal-subgroup invariant linear Hom representation consists exactly of maps that intertwine the universal subgroup action.

theorem TauCeti.HopfIdeal.IsNormal.mem_weightSpaceOneSubcomodule_linearHom_iff_forall_mapsTo_weightSpace {H : Type v} [CommRing H] {k : Type u} [Field k] [IsAlgClosed k] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] {V : Type w} {W : Type x} [AddCommGroup V] [Module k V] [Comodule k H V] [AddCommGroup W] [Module k W] [Comodule k H W] [FiniteDimensional k V] {J : HopfIdeal k H} (hJ : J.IsNormal) (hspan : ⨆ (χ : GroupLike k (H ⧸ J.toIdeal)), J.weightSpace V χ = ⊤) (f : V →ₗ[k] W) : f ∈ weightSpaceOneSubcomodule (V →ₗ[k] W) hJ ↔ ∀ (χ : GroupLike k (H ⧸ J.toIdeal)), Set.MapsTo ⇑f ↑(J.weightSpace V χ) ↑(J.weightSpace W χ)

If subgroup characters span the source, the normal-subgroup invariant Hom subcomodule consists exactly of the maps preserving each character space.

theorem TauCeti.HopfIdeal.IsNormal.id_mem_weightSpaceOneSubcomodule_linearHom {H : Type v} [CommRing H] {k : Type u} [Field k] [IsAlgClosed k] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] {V : Type w} [AddCommGroup V] [Module k V] [Comodule k H V] [FiniteDimensional k V] {J : HopfIdeal k H} (hJ : J.IsNormal) : LinearMap.id ∈ weightSpaceOneSubcomodule (V →ₗ[k] V) hJ

The identity belongs to the subgroup-equivariant endomorphism representation.

theorem TauCeti.HopfIdeal.IsNormal.comp_mem_weightSpaceOneSubcomodule_linearHom {H : Type v} [CommRing H] {k : Type u} [Field k] [IsAlgClosed k] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] {V : Type w} [AddCommGroup V] [Module k V] [Comodule k H V] [FiniteDimensional k V] {J : HopfIdeal k H} (hJ : J.IsNormal) {f g : V →ₗ[k] V} (hf : f ∈ weightSpaceOneSubcomodule (V →ₗ[k] V) hJ) (hg : g ∈ weightSpaceOneSubcomodule (V →ₗ[k] V) hJ) : f ∘ₗ g ∈ weightSpaceOneSubcomodule (V →ₗ[k] V) hJ

The normal-subgroup invariant endomorphism representation is closed under composition.