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.)
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
@[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' := _}