Cofree comodules

For an R-coalgebra C and an R-module M, the tensor product M ⊗[R] C carries a right C-comodule structure whose coaction is id ⊗ Δ followed by reassociation, m ⊗ c ↦ ∑ (m ⊗ c₁) ⊗ c₂. This is the cofree (or coinduced) right comodule on M: it is the value at M of the right adjoint to the forgetful functor from comodules to modules. The universal property is Comodule.Hom.cofreeEquiv: comodule morphisms from a comodule P into M ⊗[R] C are exactly R-linear maps P → M.

Taking M = R recovers (up to the unitor) the regular comodule already provided in TauCeti.Algebra.Coalgebra.Comodule.Regular; the cofree construction generalizes it to an arbitrary module of "coefficients".

The cofree comodule structure is provided as an explicit named definition Comodule.cofree, not as a global instance: an R-module can carry many coactions, and the cofree one (which on M ⊗[R] C would otherwise clash with a future tensor product of comodules) should be selected explicitly. This follows the convention already used for Comodule.trivial and Comodule.groupLike.

Main definitions

• TauCeti.Comodule.cofree: the cofree right C-comodule structure on M ⊗[R] C.
• TauCeti.Comodule.Hom.cofreeMap: the functoriality of the cofree comodule in M, sending an R-linear map f : M → N to the comodule morphism f ⊗ id.
• TauCeti.Comodule.Hom.cofreeUnit: the coaction P → P ⊗[R] C of a comodule P, viewed as a comodule morphism into its cofree comodule (the unit of the adjunction).
• TauCeti.Comodule.Hom.cofreeLift: the comodule morphism P → M ⊗[R] C lifting an R-linear map P → M.
• TauCeti.Comodule.Hom.cofreeEquiv: the cofree adjunction, Hom R C P (M ⊗[R] C) ≃ (P →ₗ[R] M).
• TauCeti.ComoduleCat.cofree: the cofree comodule, bundled as an object of ComoduleCat.

References

This is the cofree (coinduced) comodule of a coalgebra; see for example Sweedler, Hopf Algebras, Chapter 2. It is added for the Layer 1 target "Comodules over a coalgebra/Hopf algebra" of the Tau Ceti reductive-groups roadmap, ReductiveGroups/README.md in TauCetiRoadmap, specifically the regular/cofree representations and the adjunction underlying the embedding theorem.

noncomputable def TauCeti.Comodule.cofreeCoact (R : Type u) (C : Type v) (M : Type w) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] : TensorProduct R M C →ₗ[R] TensorProduct R (TensorProduct R M C) C

The coaction of the cofree right C-comodule on M ⊗[R] C, namely id ⊗ Δ followed by reassociation: m ⊗ c ↦ ∑ (m ⊗ c₁) ⊗ c₂. This is an implementation detail of Comodule.cofree; the public characterizations of the coaction are Comodule.cofree_coact and Comodule.cofree_coact_tmul.

Equations

• TauCeti.Comodule.cofreeCoact R C M = ↑(TensorProduct.assoc R M C C).symm ∘ₗ LinearMap.lTensor M CoalgebraStruct.comul

@[implicit_reducible]

noncomputable def TauCeti.Comodule.cofree (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 (TensorProduct R M C)

The cofree (coinduced) right C-comodule structure on M ⊗[R] C, with coaction m ⊗ c ↦ ∑ (m ⊗ c₁) ⊗ c₂.

This is not registered as a global instance: an R-module can carry many coactions, and the cofree one should be selected explicitly with Comodule.cofree.

Equations

• TauCeti.Comodule.cofree R C M = { coact := TauCeti.Comodule.cofreeCoact R C M, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.cofree_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] : coact = ↑(TensorProduct.assoc R M C C).symm ∘ₗ LinearMap.lTensor M CoalgebraStruct.comul

The coaction of the cofree comodule is id ⊗ Δ followed by reassociation.

@[simp]

theorem TauCeti.Comodule.cofree_coact_tmul {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] (m : M) (c : C) : coact (m ⊗ₜ[R] c) = (TensorProduct.assoc R M C C).symm (m ⊗ₜ[R] CoalgebraStruct.comul c)

The coaction of the cofree comodule on a simple tensor: m ⊗ c ↦ ∑ (m ⊗ c₁) ⊗ c₂.

noncomputable def TauCeti.Comodule.Hom.cofreeMap {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] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : Hom R C (TensorProduct R M C) (TensorProduct R N C)

Functoriality of the cofree comodule in the coefficient module: an R-linear map f : M → N induces the comodule morphism f ⊗ id : M ⊗[R] C → N ⊗[R] C.

Equations

• TauCeti.Comodule.Hom.cofreeMap f = { toLinearMap := LinearMap.rTensor C f, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.cofreeMap_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] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : (cofreeMap f).toLinearMap = LinearMap.rTensor C f

The underlying linear map of cofreeMap f is f ⊗ id.

@[simp]

theorem TauCeti.Comodule.Hom.cofreeMap_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] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (x : TensorProduct R M C) : (cofreeMap f) x = (LinearMap.rTensor C f) x

cofreeMap f acts as f ⊗ id.

@[simp]

theorem TauCeti.Comodule.Hom.cofreeMap_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] : cofreeMap LinearMap.id = id R C (TensorProduct R M C)

The cofree functor preserves identities.

@[simp]

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

The cofree functor preserves composition.

noncomputable def TauCeti.Comodule.Hom.cofreeUnit {R : Type u} {C : Type v} (P : Type y) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid P] [Module R P] [Comodule R C P] : Hom R C P (TensorProduct R P C)

The coaction of a comodule P, viewed as a comodule morphism P → P ⊗[R] C into its cofree comodule. This is the unit of the cofree adjunction.

Equations

• TauCeti.Comodule.Hom.cofreeUnit P = { toLinearMap := TauCeti.Comodule.coact, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.cofreeUnit_toLinearMap {R : Type u} {C : Type v} {P : Type y} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid P] [Module R P] [Comodule R C P] : (cofreeUnit P).toLinearMap = coact

The underlying linear map of cofreeUnit P is the coaction of P.

@[simp]

theorem TauCeti.Comodule.Hom.cofreeUnit_apply {R : Type u} {C : Type v} {P : Type y} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid P] [Module R P] [Comodule R C P] (p : P) : (cofreeUnit P) p = coact p

cofreeUnit P acts as the coaction of P.

noncomputable def TauCeti.Comodule.Hom.cofreeLift {R : Type u} {C : Type v} {M : Type w} {P : Type y} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [Comodule R C P] (g : P →ₗ[R] M) : Hom R C P (TensorProduct R M C)

The comodule morphism P → M ⊗[R] C lifting an R-linear map g : P → M, namely (g ⊗ id) ∘ ρ_P.

Equations

• TauCeti.Comodule.Hom.cofreeLift g = (TauCeti.Comodule.Hom.cofreeMap g).comp (TauCeti.Comodule.Hom.cofreeUnit P)

@[simp]

theorem TauCeti.Comodule.Hom.cofreeLift_toLinearMap {R : Type u} {C : Type v} {M : Type w} {P : Type y} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [Comodule R C P] (g : P →ₗ[R] M) : (cofreeLift g).toLinearMap = LinearMap.rTensor C g ∘ₗ coact

The underlying linear map of cofreeLift g is (g ⊗ id) ∘ ρ_P.

@[simp]

theorem TauCeti.Comodule.Hom.cofreeLift_apply {R : Type u} {C : Type v} {M : Type w} {P : Type y} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [Comodule R C P] (g : P →ₗ[R] M) (p : P) : (cofreeLift g) p = (LinearMap.rTensor C g) (coact p)

cofreeLift g acts as (g ⊗ id) ∘ ρ_P.

noncomputable def TauCeti.Comodule.Hom.cofreeEquiv {R : Type u} {C : Type v} {M : Type w} {P : Type y} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [Comodule R C P] : Hom R C P (TensorProduct R M C) ≃ (P →ₗ[R] M)

Comodule morphisms P → M ⊗[R] C into the cofree comodule on M are exactly R-linear maps P → M: this is the universal property of the cofree comodule (the cofree functor is right adjoint to the forgetful functor).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Comodule.Hom.cofreeEquiv_apply {R : Type u} {C : Type v} {M : Type w} {P : Type y} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [Comodule R C P] (φ : Hom R C P (TensorProduct R M C)) : cofreeEquiv φ = ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ φ.toLinearMap

The forward direction of the cofree adjunction sends a comodule morphism to the R-linear map obtained by applying the counit to the C factor.

@[simp]

theorem TauCeti.Comodule.Hom.cofreeEquiv_symm_apply {R : Type u} {C : Type v} {M : Type w} {P : Type y} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [Comodule R C P] (g : P →ₗ[R] M) : cofreeEquiv.symm g = cofreeLift g

The inverse direction of the cofree adjunction is cofreeLift.

@[simp]

theorem TauCeti.Comodule.Hom.eq_zero_iff_counit {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Hom R C P (TensorProduct R M C)) : f = 0 ↔ ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ f.toLinearMap = 0

A morphism into a cofree comodule vanishes exactly when its counit component vanishes.

@[reducible, inline]

noncomputable abbrev TauCeti.ComoduleCat.cofree (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (M : Type w) [AddCommMonoid M] [Module R M] : ComoduleCat R C

The cofree right C-comodule on a module M, bundled as an object of ComoduleCat. Its underlying module is M ⊗[R] C and its coaction is m ⊗ c ↦ ∑ (m ⊗ c₁) ⊗ c₂.

Equations

• TauCeti.ComoduleCat.cofree R C M = TauCeti.ComoduleCat.of R C (TensorProduct R M C)

@[simp]

theorem TauCeti.ComoduleCat.cofree_toSemimoduleCat (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] : (cofree R C M).toSemimoduleCat = ↧(TensorProduct R M C)

The underlying semimodule of the bundled cofree comodule is M ⊗[R] C.

@[simp]

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

The coaction on the bundled cofree comodule is id ⊗ Δ followed by reassociation.

@[simp]

theorem TauCeti.ComoduleCat.cofree_coact_tmul (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] (m : M) (c : C) : Comodule.coact (m ⊗ₜ[R] c) = (TensorProduct.assoc R M C C).symm (m ⊗ₜ[R] CoalgebraStruct.comul c)

The coaction on the bundled cofree comodule on a simple tensor is m ⊗ c ↦ ∑ (m ⊗ c₁) ⊗ c₂.