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.

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.

@[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.

@[implicit_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.

@[implicit_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.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)