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.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 }

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 }

@[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

@[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

instance 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

Equations

• ⋯ = ⋯

instance 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

Equations

• ⋯ = ⋯

instance 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)

Equations

• ⋯ = ⋯

instance ULift.instIsCentralScalar {R : Type u} {M : Type v} [SMul R M] [SMul Rᵐᵒᵖ M] [IsCentralScalar R M] : IsCentralScalar R (ULift.{u_1, v} M)

Equations

• ⋯ = ⋯

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 (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 R (ULift.{u_1, v} 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.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 ⋯ ⋯

@[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

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 := ⋯ }