mathlib documentation

algebra.module.ulift

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.has_scalar_left {R : Type u} {M : Type v} [has_scalar R M] :
Equations
@[simp]
theorem ulift.smul_down {R : Type u} {M : Type v} [has_scalar R M] (s : ulift R) (x : M) :
s x = s.down x
@[simp]
theorem ulift.smul_down' {R : Type u} {M : Type v} [has_scalar R M] (s : R) (x : ulift M) :
(s x).down = s x.down
@[protected, 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] :
@[protected, 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] :
@[protected, 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] :
@[protected, instance]
def ulift.mul_action {R : Type u} {M : Type v} [monoid R] [mul_action R M] :
Equations
@[protected, instance]
def ulift.mul_action' {R : Type u} {M : Type v} [monoid R] [mul_action R M] :
Equations
@[protected, instance]
def ulift.module {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[protected, instance]
def ulift.module' {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :
Equations
def ulift.module_equiv {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] :

The R-linear equivalence between ulift M and M.

Equations