Documentation

Mathlib.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.moduleEquiv : ULift M ≃ₗ[R] M.

instance ULift.smulLeft {R : Type u} {M : Type v} [SMul R M] :

SMul (ULift.{u_1, u} R) M

Equations

ULift.smulLeft = { smul := fun (s : ULift.{?u.4, ?u.6} R) (x : M) => s.down • x }

instance ULift.vaddLeft {R : Type u} {M : Type v} [VAdd R M] :

VAdd (ULift.{u_1, u} R) M

Equations

ULift.vaddLeft = { vadd := fun (s : ULift.{?u.4, ?u.6} R) (x : M) => s.down +ᵥ x }

@[simp]

theorem ULift.smul_def {R : Type u} {M : Type v} [SMul R M] (s : ULift.{u_1, u} R) (x : M) :

s • x = s.down • x

@[simp]

theorem ULift.vadd_def {R : Type u} {M : Type v} [VAdd R M] (s : ULift.{u_1, u} R) (x : M) :

s +ᵥ x = s.down +ᵥ x

theorem ULift.isScalarTower {R : Type u} {M : Type v} {N : Type w} [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] :

IsScalarTower (ULift.{u_1, u} R) M N

theorem ULift.isScalarTower' {R : Type u} {M : Type v} {N : Type w} [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] :

IsScalarTower R (ULift.{u_1, v} M) N

theorem ULift.isScalarTower'' {R : Type u} {M : Type v} {N : Type w} [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] :

IsScalarTower R M (ULift.{u_1, w} N)

theorem ULift.instIsCentralScalar {R : Type u} {M : Type v} [SMul R M] [SMul Rᵐᵒᵖ M] [IsCentralScalar R M] :

IsCentralScalar R (ULift.{u_1, v} M)

instance ULift.mulAction {R : Type u} {M : Type v} [Monoid R] [MulAction R M] :

MulAction (ULift.{u_1, u} R) M

Equations

ULift.mulAction = MulAction.mk ⋯ ⋯

instance ULift.addAction {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] :

AddAction (ULift.{u_1, u} R) M

Equations

ULift.addAction = AddAction.mk ⋯ ⋯

instance ULift.mulAction' {R : Type u} {M : Type v} [Monoid R] [MulAction R M] :

MulAction R (ULift.{u_1, v} M)

Equations

ULift.mulAction' = MulAction.mk ⋯ ⋯

instance ULift.addAction' {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] :

AddAction R (ULift.{u_1, v} M)

Equations

ULift.addAction' = AddAction.mk ⋯ ⋯

instance ULift.smulZeroClass {R : Type u} {M : Type v} [Zero M] [SMulZeroClass R M] :

SMulZeroClass (ULift.{u_1, u} R) M

Equations

ULift.smulZeroClass = SMulZeroClass.mk ⋯

instance ULift.smulZeroClass' {R : Type u} {M : Type v} [Zero M] [SMulZeroClass R M] :

SMulZeroClass R (ULift.{u_1, v} M)

Equations

ULift.smulZeroClass' = SMulZeroClass.mk ⋯

instance ULift.distribSMul {R : Type u} {M : Type v} [AddZeroClass M] [DistribSMul R M] :

DistribSMul (ULift.{u_1, u} R) M

Equations

ULift.distribSMul = DistribSMul.mk ⋯

instance ULift.distribSMul' {R : Type u} {M : Type v} [AddZeroClass M] [DistribSMul R M] :

DistribSMul R (ULift.{u_1, v} M)

Equations

ULift.distribSMul' = DistribSMul.mk ⋯

instance ULift.distribMulAction {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] :

DistribMulAction (ULift.{u_1, u} R) M

Equations

ULift.distribMulAction = DistribMulAction.mk ⋯ ⋯

instance ULift.distribMulAction' {R : Type u} {M : Type v} [Monoid R] [AddMonoid M] [DistribMulAction R M] :

DistribMulAction R (ULift.{u_1, v} M)

Equations

ULift.distribMulAction' = DistribMulAction.mk ⋯ ⋯

instance ULift.mulDistribMulAction {R : Type u} {M : Type v} [Monoid R] [Monoid M] [MulDistribMulAction R M] :

MulDistribMulAction (ULift.{u_1, u} R) M

Equations

ULift.mulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯

instance ULift.mulDistribMulAction' {R : Type u} {M : Type v} [Monoid R] [Monoid M] [MulDistribMulAction R M] :

MulDistribMulAction R (ULift.{u_1, v} M)

Equations

ULift.mulDistribMulAction' = MulDistribMulAction.mk ⋯ ⋯

instance ULift.smulWithZero {R : Type u} {M : Type v} [Zero R] [Zero M] [SMulWithZero R M] :

SMulWithZero (ULift.{u_1, u} R) M

Equations

ULift.smulWithZero = SMulWithZero.mk ⋯

instance ULift.smulWithZero' {R : Type u} {M : Type v} [Zero R] [Zero M] [SMulWithZero R M] :

SMulWithZero R (ULift.{u_1, v} M)

Equations

ULift.smulWithZero' = SMulWithZero.mk ⋯

instance ULift.mulActionWithZero {R : Type u} {M : Type v} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] :

MulActionWithZero (ULift.{u_1, u} R) M

Equations

ULift.mulActionWithZero = MulActionWithZero.mk ⋯ ⋯

instance ULift.mulActionWithZero' {R : Type u} {M : Type v} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] :

MulActionWithZero R (ULift.{u_1, v} M)

Equations

ULift.mulActionWithZero' = MulActionWithZero.mk ⋯ ⋯

instance ULift.module {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

Module (ULift.{u_1, u} R) M

Equations

ULift.module = Module.mk ⋯ ⋯

instance ULift.module' {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

Module R (ULift.{u_1, v} M)

Equations

ULift.module' = Module.mk ⋯ ⋯

def ULift.moduleEquiv {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

ULift.{w, v} M ≃ₗ[R] M

The R-linear equivalence between ULift M and M.

This is a linear version of AddEquiv.ulift.

Equations

ULift.moduleEquiv = { toFun := ULift.down, map_add' := ⋯, map_smul' := ⋯, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }

Instances For

@[simp]

theorem ULift.moduleEquiv_symm_apply {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (down : M) :

ULift.moduleEquiv.symm down = { down := down }

@[simp]

theorem ULift.moduleEquiv_apply {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (self : ULift.{w, v} M) :

ULift.moduleEquiv self = self.down