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.)

source

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

module k ↥M

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

Equations

M.module_of_algebra_Module = restrict_scalars.module k A ↥M

source

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

is_scalar_tower k A ↥M

source

@[protected, instance]

def Module.linear_over_field {k : Type u} [field k] {A : Type w} [ring A] [algebra k A] :

category_theory.linear k (Module A)

Equations

Module.linear_over_field = {hom_module := λ (M N : Module A), linear_map.module, smul_comp' := _, comp_smul' := _}