mathlib documentation


Additional typeclass for modules over an algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, and remove the original Module, 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.

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] :