Comodules over a coalgebra

This file defines right comodules over an R-coalgebra C and their morphisms. A right comodule is an R-module M equipped with a coaction ρ : M →ₗ[R] M ⊗[R] C satisfying the usual coassociativity and counit identities.

This is a first Layer 1 prerequisite for the reductive-groups roadmap: representations of an affine group scheme represented by a Hopf algebra are comodules over its coordinate Hopf algebra, and the roadmap explicitly calls for comodules, comodule morphisms, tensor products, duals, and the regular representation. The file starts with the core definition, the regular right comodule of a coalgebra over itself, and the basic morphism API.

Main definitions

• TauCeti.Comodule: a right comodule over a coalgebra.
• TauCeti.Comodule.Hom: morphisms of comodules.
• TauCeti.Comodule.instSelf: the regular right comodule of a coalgebra over itself.
• TauCeti.Comodule.coactComponent: the component of a coaction selected by a linear functional on the coalgebra.

References

This follows the standard definition of a right comodule over a coalgebra; see for example Sweedler, Hopf Algebras, Chapter 2. It is added for the "Comodules over a coalgebra/Hopf algebra" target in Layer 1 of the Tau Ceti reductive-groups roadmap.

class TauCeti.Comodule (R : Type u) (C : Type v) (M : Type w) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] : Type (max v w)

A right comodule over an R-coalgebra C.

The coaction is written as a linear map coact : M →ₗ[R] M ⊗[R] C. The coassociativity law says that coacting twice on the M component agrees with coacting once and then comultiplying the C component. The counit law says that applying the coalgebra counit to the C component recovers the original vector, under the canonical M ⊗ R presentation.

• coact : M →ₗ[R] TensorProduct R M C

  The coaction of a right comodule.

• coassoc : ↑(TensorProduct.assoc R M C C) ∘ₗ LinearMap.rTensor C coact ∘ₗ coact = LinearMap.lTensor M CoalgebraStruct.comul ∘ₗ coact

  Coassociativity of the right coaction.

• lTensor_counit_comp_coact : LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ coact = (TensorProduct.mk R M R).flip 1

  The right counit law for the coaction.

theorem TauCeti.Comodule.ext {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] {rho sigma : Comodule R C M} (h : coact = coact) : rho = sigma

Two right-comodule structures are equal when their coactions are equal.

theorem TauCeti.Comodule.ext_iff {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] {rho sigma : Comodule R C M} : rho = sigma ↔ coact = coact

@[simp]

theorem TauCeti.Comodule.coact_coassoc {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] : ↑(TensorProduct.assoc R M C C) ∘ₗ LinearMap.rTensor C coact ∘ₗ coact = LinearMap.lTensor M CoalgebraStruct.comul ∘ₗ coact

Coassociativity of the coaction, as an equality of linear maps.

@[simp]

theorem TauCeti.Comodule.coassoc_apply {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (m : M) : (TensorProduct.assoc R M C C) ((LinearMap.rTensor C coact) (coact m)) = (LinearMap.lTensor M CoalgebraStruct.comul) (coact m)

Coassociativity of the coaction, evaluated at a vector.

@[simp]

theorem TauCeti.Comodule.lTensor_counit_coact {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (m : M) : (LinearMap.lTensor M CoalgebraStruct.counit) (coact m) = m ⊗ₜ[R] 1

The counit law of the coaction, evaluated at a vector.

Components selected by linear functionals

noncomputable def TauCeti.Comodule.pairCoeff {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] (phi psi : C →ₗ[R] R) : TensorProduct R C C →ₗ[R] R

Pair two linear functionals on the factors of a tensor square.

Equations

• TauCeti.Comodule.pairCoeff phi psi = ↑(TensorProduct.rid R R) ∘ₗ TensorProduct.map phi psi

@[simp]

theorem TauCeti.Comodule.pairCoeff_tmul {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] (phi psi : C →ₗ[R] R) (c d : C) : (pairCoeff phi psi) (c ⊗ₜ[R] d) = phi c * psi d

noncomputable def TauCeti.Comodule.tensorPairComponent {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [AddCommMonoid M] [Module R M] (phi psi : C →ₗ[R] R) : TensorProduct R M (TensorProduct R C C) →ₗ[R] M

Apply a pair of linear functionals to the two coalgebra factors of a threefold tensor.

Equations

• TauCeti.Comodule.tensorPairComponent phi psi = ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M (TauCeti.Comodule.pairCoeff phi psi)

@[simp]

theorem TauCeti.Comodule.tensorPairComponent_tmul {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [AddCommMonoid M] [Module R M] (phi psi : C →ₗ[R] R) (m : M) (t : TensorProduct R C C) : (tensorPairComponent phi psi) (m ⊗ₜ[R] t) = (pairCoeff phi psi) t • m

theorem TauCeti.Comodule.tensorComponent_comp_tensorComponent {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [AddCommMonoid M] [Module R M] (phi psi : C →ₗ[R] R) : phi.tensorComponent ∘ₗ psi.tensorComponent = tensorPairComponent phi psi ∘ₗ ↑(TensorProduct.assoc R M C C)

Applying two tensor components successively is applying their pair after reassociation.

theorem TauCeti.Comodule.coact_comp_tensorComponent {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (phi : C →ₗ[R] R) : coact ∘ₗ phi.tensorComponent = phi.tensorComponent ∘ₗ LinearMap.rTensor C coact

Taking a tensor component commutes with a coaction on the other factor.

noncomputable def TauCeti.Comodule.coactComponent {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (phi : C →ₗ[R] R) : M →ₗ[R] M

The component of a coaction selected by a linear functional on the coalgebra.

Equations

• TauCeti.Comodule.coactComponent phi = phi.tensorComponent ∘ₗ TauCeti.Comodule.coact

theorem TauCeti.Comodule.coactComponent_apply {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (phi : C →ₗ[R] R) (m : M) : (coactComponent phi) m = phi.tensorComponent (coact m)

theorem TauCeti.Comodule.coactComponent_coactComponent {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (phi psi : C →ₗ[R] R) (m : M) : (coactComponent phi) ((coactComponent psi) m) = (tensorPairComponent phi psi) ((LinearMap.lTensor M CoalgebraStruct.comul) (coact m))

Coassociativity read off by two linear functionals on the coalgebra.

theorem TauCeti.Comodule.tensorPairComponent_comp_lTensor_comul {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] {phi psi theta : C →ₗ[R] R} (h : pairCoeff phi psi ∘ₗ CoalgebraStruct.comul = theta) : tensorPairComponent phi psi ∘ₗ LinearMap.lTensor M CoalgebraStruct.comul = theta.tensorComponent

Contracting a pair component after comultiplication uses the corresponding contraction of the two coefficient functionals.

@[instance_reducible]

instance TauCeti.Comodule.instSelf (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : Comodule R C C

The regular right comodule of a coalgebra over itself, with coaction given by the coalgebra comultiplication.

Equations

• TauCeti.Comodule.instSelf R C = { coact := CoalgebraStruct.comul, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.instSelf_coact {R : Type u} {C : Type v} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] : coact = CoalgebraStruct.comul

The coaction of the regular right comodule is the coalgebra comultiplication.

structure TauCeti.Comodule.Hom (R : Type u) (C : Type v) (M : Type w) (N : Type x) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] extends M →ₗ[R] N : Type (max w x)

A morphism of right comodules over a fixed coalgebra.

• toFun : M → N
• map_add' (x y : M) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : R) (x : M) : self.toFun (m • x) = (RingHom.id R) m • self.toFun x
• map_coact : TensorProduct.map self.toLinearMap LinearMap.id ∘ₗ coact = coact ∘ₗ self.toLinearMap

  A comodule morphism commutes with the two coactions.

@[instance_reducible]

instance TauCeti.Comodule.Hom.funLike {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : FunLike (Hom R C M N) M N

Equations

• TauCeti.Comodule.Hom.funLike = { coe := fun (f : TauCeti.Comodule.Hom R C M N) => ⇑f.toLinearMap, coe_injective := ⋯ }

def TauCeti.Comodule.Hom.Simps.apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) : M → N

See Note [custom simps projection].

Equations

• TauCeti.Comodule.Hom.Simps.apply f = ⇑f

@[simp]

theorem TauCeti.Comodule.Hom.coe_mk {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {f : M →ₗ[R] N} (h : TensorProduct.map f LinearMap.id ∘ₗ coact = coact ∘ₗ f) : ⇑{ toLinearMap := f, map_coact := h } = ⇑f

@[simp]

theorem TauCeti.Comodule.Hom.coe_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) : ⇑f.toLinearMap = ⇑f

theorem TauCeti.Comodule.Hom.toLinearMap_injective {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : Function.Injective toLinearMap

A comodule morphism is determined by its underlying linear map.

theorem TauCeti.Comodule.Hom.ext {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {f g : Hom R C M N} (h : ∀ (m : M), f m = g m) : f = g

Two comodule morphisms are equal when their underlying functions are equal.

theorem TauCeti.Comodule.Hom.ext_iff {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {f g : Hom R C M N} : f = g ↔ ∀ (m : M), f m = g m

@[simp]

theorem TauCeti.Comodule.Hom.map_coact_eq {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) : TensorProduct.map f.toLinearMap LinearMap.id ∘ₗ coact = coact ∘ₗ f.toLinearMap

A comodule morphism commutes with coactions, as an equality of linear maps.

@[simp]

theorem TauCeti.Comodule.Hom.map_coact_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (m : M) : (TensorProduct.map f.toLinearMap LinearMap.id) (coact m) = coact (f m)

A comodule morphism commutes with coactions, evaluated at a vector.

def TauCeti.Comodule.Hom.id (R : Type u) (C : Type v) (M : Type w) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] : Hom R C M M

The identity morphism of a right comodule.

Equations

• TauCeti.Comodule.Hom.id R C M = { toLinearMap := LinearMap.id, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.id_apply (R : Type u) (C : Type v) (M : Type w) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (x : M) : (id R C M) x = x

def TauCeti.Comodule.Hom.comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (g : Hom R C N P) (f : Hom R C M N) : Hom R C M P

Composition of right-comodule morphisms.

Equations

• g.comp f = { toLinearMap := g.toLinearMap ∘ₗ f.toLinearMap, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.comp_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (g : Hom R C N P) (f : Hom R C M N) (x : M) : (g.comp f) x = g (f x)

@[simp]

theorem TauCeti.Comodule.Hom.id_toLinearMap {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] : (id R C M).toLinearMap = LinearMap.id

The underlying linear map of the identity morphism is the identity linear map.

@[simp]

theorem TauCeti.Comodule.Hom.comp_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (g : Hom R C N P) (f : Hom R C M N) : (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

The underlying linear map of a composition is the composition of the underlying linear maps.

@[simp]

theorem TauCeti.Comodule.Hom.id_comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) : (id R C N).comp f = f

@[simp]

theorem TauCeti.Comodule.Hom.comp_id {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) : f.comp (id R C M) = f

@[simp]

theorem TauCeti.Comodule.Hom.comp_assoc {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} {Q : Type u_2} [AddCommMonoid P] [Module R P] [Comodule R C P] [AddCommMonoid Q] [Module R Q] [Comodule R C Q] (h : Hom R C P Q) (g : Hom R C N P) (f : Hom R C M N) : (h.comp g).comp f = h.comp (g.comp f)