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.module_equiv : ulift M ≃ₗ[R] M
.
@[protected, instance]
def
ulift.is_scalar_tower
{R : Type u}
{M : Type v}
{N : Type w}
[has_smul R M]
[has_smul M N]
[has_smul R N]
[is_scalar_tower R M N] :
is_scalar_tower (ulift R) M N
@[protected, instance]
def
ulift.is_scalar_tower'
{R : Type u}
{M : Type v}
{N : Type w}
[has_smul R M]
[has_smul M N]
[has_smul R N]
[is_scalar_tower R M N] :
is_scalar_tower R (ulift M) N
@[protected, instance]
def
ulift.is_scalar_tower''
{R : Type u}
{M : Type v}
{N : Type w}
[has_smul R M]
[has_smul M N]
[has_smul R N]
[is_scalar_tower R M N] :
is_scalar_tower R M (ulift N)
@[protected, instance]
def
ulift.is_central_scalar
{R : Type u}
{M : Type v}
[has_smul R M]
[has_smul Rᵐᵒᵖ M]
[is_central_scalar R M] :
is_central_scalar R (ulift M)
@[protected, instance]
Equations
- ulift.mul_action = {to_has_smul := {smul := has_smul.smul ulift.has_smul_left}, one_smul := _, mul_smul := _}
@[protected, instance]
def
ulift.add_action
{R : Type u}
{M : Type v}
[add_monoid R]
[add_action R M] :
add_action (ulift R) M
Equations
- ulift.add_action = {to_has_vadd := {vadd := has_vadd.vadd ulift.has_vadd_left}, zero_vadd := _, add_vadd := _}
@[protected, 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_smul := {smul := has_smul.smul ulift.has_smul}, one_smul := _, mul_smul := _}
@[protected, instance]
def
ulift.add_action'
{R : Type u}
{M : Type v}
[add_monoid R]
[add_action R M] :
add_action R (ulift M)
Equations
- ulift.add_action' = {to_has_vadd := {vadd := has_vadd.vadd ulift.has_vadd}, zero_vadd := _, add_vadd := _}
@[protected, 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
@[protected, 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_smul := mul_action.to_has_smul ulift.mul_action', one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
@[protected, instance]
def
ulift.mul_distrib_mul_action
{R : Type u}
{M : Type v}
[monoid R]
[monoid M]
[mul_distrib_mul_action R M] :
mul_distrib_mul_action (ulift R) M
Equations
@[protected, instance]
def
ulift.mul_distrib_mul_action'
{R : Type u}
{M : Type v}
[monoid R]
[monoid M]
[mul_distrib_mul_action R M] :
mul_distrib_mul_action R (ulift M)
Equations
- ulift.mul_distrib_mul_action' = {to_mul_action := {to_has_smul := mul_action.to_has_smul ulift.mul_action', one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}
@[protected, instance]
def
ulift.smul_with_zero
{R : Type u}
{M : Type v}
[has_zero R]
[has_zero M]
[smul_with_zero R M] :
smul_with_zero (ulift R) M
Equations
- ulift.smul_with_zero = {to_has_smul := {smul := has_smul.smul ulift.has_smul_left}, smul_zero := _, zero_smul := _}
@[protected, instance]
def
ulift.smul_with_zero'
{R : Type u}
{M : Type v}
[has_zero R]
[has_zero M]
[smul_with_zero R M] :
smul_with_zero R (ulift M)
Equations
@[protected, instance]
def
ulift.mul_action_with_zero
{R : Type u}
{M : Type v}
[monoid_with_zero R]
[has_zero M]
[mul_action_with_zero R M] :
mul_action_with_zero (ulift R) M
Equations
@[protected, instance]
def
ulift.mul_action_with_zero'
{R : Type u}
{M : Type v}
[monoid_with_zero R]
[has_zero M]
[mul_action_with_zero R M] :
mul_action_with_zero R (ulift M)
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
The R
-linear equivalence between ulift M
and M
.
Equations
- ulift.module_equiv = {to_fun := ulift.down M, map_add' := _, map_smul' := _, inv_fun := ulift.up M, left_inv := _, right_inv := _}