ulift instances for module and multiplicative actions
This file defines instances for module, mul_action and related structures on ulift types.
(Recall ulift α is just a "copy" of a type α in a higher universe.)
We also provide ulift.semimodule_equiv : ulift M ≃ₗ[R] M.
@[instance]
@[simp]
@[instance]
@[simp]
@[instance]
def
ulift.is_scalar_tower
{R : Type u}
{M : Type v}
{N : Type w}
[has_scalar R M]
[has_scalar M N]
[has_scalar R N]
[is_scalar_tower R M N] :
is_scalar_tower (ulift R) M N
Equations
@[instance]
def
ulift.is_scalar_tower'
{R : Type u}
{M : Type v}
{N : Type w}
[has_scalar R M]
[has_scalar M N]
[has_scalar R N]
[is_scalar_tower R M N] :
is_scalar_tower R (ulift M) N
Equations
@[instance]
def
ulift.is_scalar_tower''
{R : Type u}
{M : Type v}
{N : Type w}
[has_scalar R M]
[has_scalar M N]
[has_scalar R N]
[is_scalar_tower R M N] :
is_scalar_tower R M (ulift N)
Equations
@[instance]
def
ulift.mul_action
{R : Type u}
{M : Type v}
[monoid R]
[mul_action R M] :
mul_action (ulift R) M
Equations
- ulift.mul_action = {to_has_scalar := {smul := has_scalar.smul ulift.has_scalar}, one_smul := _, mul_smul := _}
@[instance]
def
ulift.mul_action'
{R : Type u}
{M : Type v}
[monoid R]
[mul_action R M] :
mul_action R (ulift M)
Equations
- ulift.mul_action' = {to_has_scalar := {smul := has_scalar.smul ulift.has_scalar'}, one_smul := _, mul_smul := _}
@[instance]
def
ulift.distrib_mul_action
{R : Type u}
{M : Type v}
[monoid R]
[add_monoid M]
[distrib_mul_action R M] :
distrib_mul_action (ulift R) M
Equations
- ulift.distrib_mul_action = {to_mul_action := {to_has_scalar := mul_action.to_has_scalar ulift.mul_action, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
@[instance]
def
ulift.distrib_mul_action'
{R : Type u}
{M : Type v}
[monoid R]
[add_monoid M]
[distrib_mul_action R M] :
distrib_mul_action R (ulift M)
Equations
- ulift.distrib_mul_action' = {to_mul_action := {to_has_scalar := mul_action.to_has_scalar ulift.mul_action', one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
@[instance]
def
ulift.semimodule
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
semimodule (ulift R) M
Equations
- ulift.semimodule = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action ulift.distrib_mul_action, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[instance]
def
ulift.semimodule'
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
semimodule R (ulift M)
Equations
def
ulift.semimodule_equiv
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
The R-linear equivalence between ulift M and M.
Equations
- ulift.semimodule_equiv = {to_fun := ulift.down M, map_add' := _, map_smul' := _, inv_fun := ulift.up M, left_inv := _, right_inv := _}