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.

Equations

• M.moduleOfAlgebraModule = RestrictScalars.module k A ↑M

theorem ModuleCat.isScalarTower_of_algebra_moduleCat {k : Type u} [Field k] {A : Type w} [Ring A] [Algebra k A] (M : ModuleCat A) : IsScalarTower k A ↑M

instance ModuleCat.linearOverField {k : Type u} [Field k] {A : Type w} [Ring A] [Algebra k A] : CategoryTheory.Linear k (ModuleCat A)

Equations

• ModuleCat.linearOverField = { homModule := fun (x x_1 : ModuleCat A) => inferInstance, smul_comp := ⋯, comp_smul := ⋯ }