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

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

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

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)

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)

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

Equations

• ULift.mulAction = { smul := fun (x1 : ULift.{?u.5, ?u.7} R) (x2 : M) => x1 • x2, one_smul := ⋯, mul_smul := ⋯ }

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

Equations

• ULift.addAction = { vadd := fun (x1 : ULift.{?u.5, ?u.7} R) (x2 : M) => x1 +ᵥ x2, zero_vadd := ⋯, add_vadd := ⋯ }

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

Equations

• ULift.mulAction' = { smul := fun (x1 : R) (x2 : ULift.{?u.5, ?u.6} M) => x1 • x2, one_smul := ⋯, mul_smul := ⋯ }

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

Equations

• ULift.addAction' = { vadd := fun (x1 : R) (x2 : ULift.{?u.5, ?u.6} M) => x1 +ᵥ x2, zero_vadd := ⋯, add_vadd := ⋯ }

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

Equations

• ULift.smulZeroClass = { toSMul := ULift.smulLeft, smul_zero := ⋯ }

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

Equations

• ULift.smulZeroClass' = { toSMul := ULift.smul, smul_zero := ⋯ }

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

Equations

• ULift.distribSMul = { toSMulZeroClass := ULift.smulZeroClass, smul_add := ⋯ }

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

Equations

• ULift.distribSMul' = { toSMulZeroClass := ULift.smulZeroClass', smul_add := ⋯ }

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 = { toMulAction := ULift.mulAction, smul_zero := ⋯, smul_add := ⋯ }

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' = { toMulAction := ULift.mulAction', smul_zero := ⋯, smul_add := ⋯ }

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 = { toMulAction := ULift.mulAction, smul_mul := ⋯, smul_one := ⋯ }

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' = { toMulAction := ULift.mulAction', smul_mul := ⋯, smul_one := ⋯ }

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 = { toSMul := ULift.smulLeft, smul_zero := ⋯, zero_smul := ⋯ }

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' = { toSMul := ULift.smul, smul_zero := ⋯, zero_smul := ⋯ }

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 = { toSMul := ULift.smulWithZero.toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, zero_smul := ⋯ }

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' = { toSMul := ULift.smulWithZero'.toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, zero_smul := ⋯ }

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 = { toSMul := ULift.smulWithZero.toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

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' = { toSMul := ULift.smulWithZero'.toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

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

@[simp]

theorem ULift.moduleEquiv_symm_apply {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (down : M) : 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) : moduleEquiv self = self.down