mathlib documentation

algebra.category.Module.algebra

Additional typeclass for modules over an algebra #

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

We provide the linear k (Module A) instance.

Note #

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

It seems without making a parallel version Module' 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, requiring users to write Module' ℤ A when A is merely a ring.)

def Module.module_of_algebra_Module {k : Type u} [field k] {A : Type w} [ring A] [algebra k A] (M : Module A) :

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

Equations
theorem Module.is_scalar_tower_of_algebra_Module {k : Type u} [field k] {A : Type w} [ring A] [algebra k A] (M : Module A) :
@[protected, instance]
def Module.linear_over_field {k : Type u} [field k] {A : Type w} [ring A] [algebra k A] :
Equations