Additional typeclass for modules over an algebra #

For an object in M : ModuleCat A, where A is a k-algebra, we provide additional typeclasses on the underlying type M, namely Module k M and IsScalarTower k A M. These are not made into instances by default.

We provide the Linear k (ModuleCat A) instance.

Note #

If you begin with a [Module k M] [Module A M] [IsScalarTower k A M], and build a bundled module via ModuleCat.of A M, these instances will not necessarily agree with the original ones.

It seems without making a parallel version ModuleCat' k A, for modules over a k-algebra A, that carries these typeclasses, this seems hard to achieve. (An alternative would be to always require these typeclasses, and remove the original ModuleCat, requiring users to write ModuleCat' ℤ A when A is merely a ring.)

def ModuleCat.moduleOfAlgebraModule {k : Type u} [Field k] {A : Type w} [Ring A] [Algebra k A] (M : ModuleCat A) :
Module k M

Type synonym for considering a module over a k-algebra as a k-module.

Instances For
    instance ModuleCat.linearOverField {k : Type u} [Field k] {A : Type w} [Ring A] [Algebra k A] :
    • ModuleCat.linearOverField = { homModule := fun (M N : ModuleCat A) => LinearMap.module, smul_comp := , comp_smul := }