Scalar extension of comodules

Let C be a coalgebra over a commutative semiring R, and let A be an R-algebra. This file constructs scalar extension of the underlying-module functor on all comodules:

ComoduleCat R C ⥤ SemimoduleCat A,      M ↦ A ⊗[R] M.

No finiteness or bialgebra structure is needed for the construction.

Main declarations

• TauCeti.ComoduleCat.scalarExtensionFunctor: scalar extension on all comodules.

noncomputable def TauCeti.ComoduleCat.scalarExtensionFunctor (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] : CategoryTheory.Functor (ComoduleCat R C) (SemimoduleCat A)

Scalar extension of the underlying-module functor on comodules.

Equations

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

@[simp]

theorem TauCeti.ComoduleCat.scalarExtensionFunctor_obj (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] (M : ComoduleCat R C) : (scalarExtensionFunctor R C A).obj M = ↧(TensorProduct R A ↑M.toSemimoduleCat)

Scalar extension sends M to the semimodule A ⊗[R] M.

@[simp]

theorem TauCeti.ComoduleCat.scalarExtensionFunctor_map (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (A : Type x) [Semiring A] [Algebra R A] {M N : ComoduleCat R C} (f : M ⟶ N) : (scalarExtensionFunctor R C A).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (SemimoduleCat.ofHom (LinearMap.baseChange A f.toLinearMap)) (CategoryTheory.eqToHom ⋯))

Scalar extension maps a comodule morphism to base change of its underlying linear map.