ULift instances for module and multiplicative actions

This file defines instances for Module, MulAction 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.

@[implicit_reducible]

instance ULift.smulLeft {R : Type u} {M : Type v} [SMul R M] : SMul (ULift.{u_1, u} R) M

@[implicit_reducible]

instance ULift.vaddLeft {R : Type u} {M : Type v} [VAdd R M] : VAdd (ULift.{u_1, u} R) M

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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.

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

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