mathlib3 documentation

algebra.module.ulift

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.has_smul_left {R : Type u} {M : Type v} [has_smul R M] :
Equations
@[protected, instance]
def ulift.has_vadd_left {R : Type u} {M : Type v} [has_vadd R M] :
Equations
@[simp]
theorem ulift.vadd_def {R : Type u} {M : Type v} [has_vadd R M] (s : ulift R) (x : M) :
s +ᵥ x = s.down +ᵥ x
@[simp]
theorem ulift.smul_def {R : Type u} {M : Type v} [has_smul R M] (s : ulift R) (x : M) :
s x = s.down x
@[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] :
@[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] :
@[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] :
@[protected, instance]
@[protected, instance]
def ulift.mul_action {R : Type u} {M : Type v} [monoid R] [mul_action R M] :
Equations
@[protected, instance]
def ulift.add_action {R : Type u} {M : Type v} [add_monoid R] [add_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.add_action' {R : Type u} {M : Type v} [add_monoid R] [add_action R M] :
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) :
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
@[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}