Linear Hom comodules #

For comodules M and N over a Hopf algebra, with M finite projective, Hom_R(M,N) is a comodule by transport from the diagonal tensor comodule M* ⊗ N. On algebra-valued points its action is f ↦ g_N ∘ f ∘ g_M⁻¹. In particular, taking N = M gives the conjugation representation on endomorphisms, used to construct representations with prescribed normal kernels. For a commutative Hopf algebra, the fixed vectors are exactly the comodule morphisms.

The order M* ⊗ N is part of this construction. Over a noncommutative Hopf algebra, swapping it to N ⊗ M* need not be colinear, and the identity endomorphism need not be fixed in the former. The fixed-morphism characterization below therefore retains commutative coefficients.

The construction uses Comodule.dual, Comodule.tensor, Comodule.Transport and Mathlib's dualTensorHomEquiv; the point formula uses the existing inverse-point evaluation identity.

References #

J. C. Jantzen, Representations of Algebraic Groups, I.2.
J. S. Milne, Algebraic Groups (2017), §4.a and §5.c.

source

@[implicit_reducible]

noncomputable def TauCeti.Comodule.linearHom {R : Type u} {H : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R M] [Module.Projective R M] [Semiring H] [HopfAlgebra R H] [Comodule R H M] [Comodule R H N] :

Comodule R H (M →ₗ[R] N)

The comodule of linear maps from a finite projective comodule to an arbitrary comodule, with the contragredient action on the source. This is an explicit structure, not a global instance, so different coactions on the same linear Hom space can coexist.

Equations

TauCeti.Comodule.linearHom = TauCeti.Comodule.Transport (dualTensorHomEquiv R M N)

Instances For

source

@[simp]

theorem TauCeti.Comodule.linearHom_coact {R : Type u} {H : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R M] [Module.Projective R M] [Semiring H] [HopfAlgebra R H] [Comodule R H M] [Comodule R H N] (f : M →ₗ[R] N) :

coact f = (TensorProduct.map (dualTensorHom R M N) LinearMap.id) (coact ((dualTensorHomEquiv R M N).symm f))

The Hom coaction is transported from the tensor product of the dual and the target.

source

@[simp]

theorem TauCeti.Comodule.baseChangeTensorHom_endOfPoint_linearHom {R : Type u} {H : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R M] [Module.Projective R M] [Semiring H] [HopfAlgebra R H] [Comodule R H M] [Comodule R H N] {A : Type y} [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (f : TensorProduct R A (M →ₗ[R] N)) :

(LinearMap.baseChangeTensorHom R A M N) ((endOfPoint (M →ₗ[R] N) g.ofConv) f) = endOfPoint N g.ofConv ∘ₗ (LinearMap.baseChangeTensorHom R A M N) f ∘ₗ endOfPoint M g⁻¹.ofConv

Under scalar extension of linear Hom, an algebra-valued point acts by conjugating with its actions on the target and source.

source

theorem TauCeti.Comodule.endOfPoint_linearHom_one_tmul_eq_iff {R : Type u} {H : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R M] [Module.Projective R M] [Semiring H] [HopfAlgebra R H] [Comodule R H M] [Comodule R H N] {A : Type y} [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (f : M →ₗ[R] N) :

(endOfPoint (M →ₗ[R] N) g.ofConv) (1 ⊗ₜ[R] f) = 1 ⊗ₜ[R] f ↔ LinearMap.baseChange A f ∘ₗ endOfPoint M g.ofConv = endOfPoint N g.ofConv ∘ₗ LinearMap.baseChange A f

A scalar-extended linear map is fixed by a point in the Hom comodule exactly when it intertwines the point actions on its source and target.

source

@[simp]

theorem TauCeti.Comodule.mem_fixedSubcomodule_linearHom_iff {R : Type u} {H : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Finite R M] [Module.Projective R M] [CommSemiring H] [HopfAlgebra R H] [Comodule R H M] [Comodule R H N] (f : M →ₗ[R] N) :

f ∈ fixedSubcomodule R H (M →ₗ[R] N) ↔ TensorProduct.map f LinearMap.id ∘ₗ coact = coact ∘ₗ f

The fixed vectors in the linear Hom comodule are exactly the colinear linear maps. This criterion includes nonreduced Hopf algebras and needs no hypothesis on geometric points.

source