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_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]
def ulift.is_central_scalar {R : Type u} {M : Type v} [has_smul R M] [has_smul Rᵐᵒᵖ M] [is_central_scalar R M] :
@[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
@[protected, instance]
def ulift.smul_zero_class {R : Type u} {M : Type v} [has_zero M] [smul_zero_class R M] :
Equations
@[protected, instance]
def ulift.smul_zero_class' {R : Type u} {M : Type v} [has_zero M] [smul_zero_class R M] :
Equations
@[protected, instance]
def ulift.smul_with_zero {R : Type u} {M : Type v} [has_zero R] [has_zero M] [smul_with_zero 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