ulift instances for module and multiplicative actions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.smul_zero_class
{R : Type u}
{M : Type v}
[has_zero M]
[smul_zero_class R M] :
smul_zero_class (ulift R) M
Equations
- ulift.smul_zero_class = {to_has_smul := {smul := has_smul.smul ulift.has_smul_left}, smul_zero := _}
@[protected, instance]
def
ulift.smul_zero_class'
{R : Type u}
{M : Type v}
[has_zero M]
[smul_zero_class R M] :
smul_zero_class R (ulift M)
Equations
@[protected, instance]
def
ulift.distrib_smul
{R : Type u}
{M : Type v}
[add_zero_class M]
[distrib_smul R M] :
distrib_smul (ulift R) M
Equations
@[protected, instance]
def
ulift.distrib_smul'
{R : Type u}
{M : Type v}
[add_zero_class M]
[distrib_smul R M] :
distrib_smul R (ulift 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 (ulift R) 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_zero := _, smul_add := _}
@[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_zero := _, smul_add := _}
@[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_smul_zero_class := {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
@[simp]
theorem
ulift.module_equiv_apply
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
(self : ulift M) :
⇑ulift.module_equiv self = self.down
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 := _}
@[simp]
theorem
ulift.module_equiv_symm_apply
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
(down : M) :
⇑(ulift.module_equiv.symm) down = {down := down}