Finitely generated cofree comodules

This file lifts the cofree right comodule M ⊗[R] C to the finitely generated comodule category when the tensor-product carrier is finitely generated over R. It is the finite-category version of ComoduleCat.cofree.

This is Layer 1 infrastructure for the Tau Ceti reductive-groups roadmap target "Comodules over a coalgebra/Hopf algebra": the finite-dimensional representation category needs finite versions of the regular and cofree comodules before tensor products, duals, and the embedding theorem can be developed.

Main definitions

• TauCeti.FGComoduleCat.cofree: the cofree comodule as a finitely generated object.
• TauCeti.FGComoduleCat.cofreeMap: functoriality between finite cofree objects.
• TauCeti.FGComoduleCat.cofreeLift: the finite-category form of the cofree lifting map.
• TauCeti.FGComoduleCat.cofreeEquiv: the cofree universal property in FGComoduleCat.
• TauCeti.FGComoduleCat.incl_cofree: forgetting the finite cofree comodule gives the ambient cofree comodule.

References

The cofree-comodule construction follows Sweedler, Hopf Algebras, Chapter 2, as in TauCeti.Algebra.Coalgebra.Comodule.Cofree.

@[reducible, inline]

noncomputable abbrev TauCeti.FGComoduleCat.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] [Module.Finite R (TensorProduct R M C)] : FGComoduleCat R C

The cofree right C-comodule with finitely generated tensor-product carrier, bundled as an object of FGComoduleCat.

The underlying module is M ⊗[R] C, with coaction id ⊗ Δ followed by reassociation.

Equations

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

@[simp]

theorem TauCeti.FGComoduleCat.cofree_obj (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] : (cofree R C M).obj = ComoduleCat.cofree R C M

Forgetting the finitely generated cofree comodule to all comodules gives the ambient cofree comodule.

@[simp]

theorem TauCeti.FGComoduleCat.cofree_coe (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] : ↑(cofree R C M) = TensorProduct R M C

The underlying type of the finitely generated cofree comodule is M ⊗[R] C.

@[simp]

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

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

@[simp]

theorem TauCeti.FGComoduleCat.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] [Module.Finite R (TensorProduct R M C)] (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 finitely generated cofree comodule sends a simple tensor m ⊗ c to ∑ (m ⊗ c₁) ⊗ c₂.

@[simp]

theorem TauCeti.FGComoduleCat.incl_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] [Module.Finite R (TensorProduct R M C)] : incl.obj (cofree R C M) = ComoduleCat.cofree R C M

The inclusion of finitely generated comodules sends FGComoduleCat.cofree to ComoduleCat.cofree.

@[simp]

theorem TauCeti.FGComoduleCat.forget₂_semimoduleCat_cofree_obj (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] : (CategoryTheory.forget₂ (FGComoduleCat R C) (SemimoduleCat R)).obj (cofree R C M) = ↧(TensorProduct R M C)

The finite cofree comodule forgets to the tensor product module M ⊗[R] C.

@[reducible, inline]

noncomputable abbrev TauCeti.FGComoduleCat.cofreeMap (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] {N : Type w} [AddCommMonoid N] [Module R N] [Module.Finite R (TensorProduct R N C)] (f : M →ₗ[R] N) : cofree R C M ⟶ cofree R C N

Functoriality of finite cofree comodules in the coefficient module.

An R-linear map f : M → N induces the comodule morphism f ⊗ id.

Equations

• TauCeti.FGComoduleCat.cofreeMap R C f = TauCeti.FGComoduleCat.ofHom (TauCeti.Comodule.Hom.cofreeMap f)

@[simp]

theorem TauCeti.FGComoduleCat.cofreeMap_apply (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] {N : Type w} [AddCommMonoid N] [Module R N] [Module.Finite R (TensorProduct R N C)] (f : M →ₗ[R] N) (x : TensorProduct R M C) : (CategoryTheory.ConcreteCategory.hom (cofreeMap R C f)) x = (LinearMap.rTensor C f) x

cofreeMap f acts as f ⊗ id.

@[simp]

theorem TauCeti.FGComoduleCat.cofreeMap_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] [Module.Finite R (TensorProduct R M C)] {N : Type w} [AddCommMonoid N] [Module R N] [Module.Finite R (TensorProduct R N C)] (f : M →ₗ[R] N) (m : M) (c : C) : (CategoryTheory.ConcreteCategory.hom (cofreeMap R C f)) (m ⊗ₜ[R] c) = f m ⊗ₜ[R] c

On simple tensors, cofreeMap f applies f to the coefficient factor.

@[simp]

theorem TauCeti.FGComoduleCat.cofreeMap_id (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] : cofreeMap R C LinearMap.id = CategoryTheory.CategoryStruct.id (cofree R C M)

The finite cofree construction sends the identity linear map to the identity morphism.

@[simp]

theorem TauCeti.FGComoduleCat.cofreeMap_comp (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] {N : Type w} [AddCommMonoid N] [Module R N] [Module.Finite R (TensorProduct R N C)] {P : Type w} [AddCommMonoid P] [Module R P] [Module.Finite R (TensorProduct R P C)] (g : N →ₗ[R] P) (f : M →ₗ[R] N) : cofreeMap R C (g ∘ₗ f) = CategoryTheory.CategoryStruct.comp (cofreeMap R C f) (cofreeMap R C g)

The finite cofree construction preserves composition of coefficient-module maps.

@[reducible, inline]

noncomputable abbrev TauCeti.FGComoduleCat.cofreeLift (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] (P : FGComoduleCat R C) (g : ↑P →ₗ[R] M) : P ⟶ cofree R C M

The finite-category cofree lift of an R-linear map from a finite comodule to the coefficient module.

Equations

• TauCeti.FGComoduleCat.cofreeLift R C P g = CategoryTheory.ObjectProperty.homMk (TauCeti.ComoduleCat.ofHom R C (TauCeti.Comodule.Hom.cofreeLift g))

@[simp]

theorem TauCeti.FGComoduleCat.cofreeLift_apply (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] {P : FGComoduleCat R C} (g : ↑P →ₗ[R] M) (p : ↑P) : (CategoryTheory.ConcreteCategory.hom (cofreeLift R C P g)) p = (LinearMap.rTensor C g) (Comodule.coact p)

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

noncomputable def TauCeti.FGComoduleCat.cofreeEquiv (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] (P : FGComoduleCat R C) : (P ⟶ cofree R C M) ≃ (↑P →ₗ[R] M)

The finite-category cofree universal property.

Equations

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

@[simp]

theorem TauCeti.FGComoduleCat.cofreeEquiv_apply (R : Type u) (C : Type v) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R (TensorProduct R M C)] {P : FGComoduleCat R C} (φ : P ⟶ cofree R C M) : (cofreeEquiv R C P) φ = Comodule.Hom.cofreeEquiv φ.hom

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

@[simp]

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

The inverse direction of the finite cofree adjunction is cofreeLift.