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.

source
instance ULift.vaddLeft {R : Type u} {M : Type v} [VAdd R M] :
VAdd (ULift.{u_1, u} R) M
Equations
source
instance ULift.smulLeft {R : Type u} {M : Type v} [SMul R M] :
SMul (ULift.{u_1, u} R) M
Equations
source
@[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
source
@[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
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
theorem ULift.addAction.proof_1 {R : Type u_2} {M : Type u_3} [AddMonoid R] [AddAction R M] :
∀ (x x_1 : ULift.{u_1, u_2} R) (b : M), x.down + x_1.down +ᵥ b = x.down +ᵥ (x_1.down +ᵥ b)
source
instance ULift.addAction {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] :
AddAction (ULift.{u_1, u} R) M
Equations
source
instance ULift.mulAction {R : Type u} {M : Type v} [Monoid R] [MulAction R M] :
MulAction (ULift.{u_1, u} R) M
Equations
source
theorem ULift.addAction'.proof_1 {R : Type u_3} {M : Type u_2} [AddMonoid R] [AddAction R M] :
∀ (x : ULift.{u_1, u_2} M), { down := 0 +ᵥ x.down } = { down := x.down }
source
theorem ULift.addAction'.proof_2 {R : Type u_3} {M : Type u_2} [AddMonoid R] [AddAction R M] :
∀ (x x_1 : R) (x_2 : ULift.{u_1, u_2} M), { down := x + x_1 +ᵥ x_2.down } = { down := x +ᵥ (x_1 +ᵥ x_2).down }
source
instance ULift.addAction' {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] :
AddAction R (ULift.{u_1, v} M)
Equations
source
instance ULift.mulAction' {R : Type u} {M : Type v} [Monoid R] [MulAction R M] :
MulAction R (ULift.{u_1, v} M)
Equations
source
instance ULift.smulZeroClass {R : Type u} {M : Type v} [Zero M] [SMulZeroClass R M] :
SMulZeroClass (ULift.{u_1, u} R) M
Equations
source
instance ULift.smulZeroClass' {R : Type u} {M : Type v} [Zero M] [SMulZeroClass R M] :
SMulZeroClass R (ULift.{u_1, v} M)
Equations
source
instance ULift.distribSMul {R : Type u} {M : Type v} [AddZeroClass M] [DistribSMul R M] :
DistribSMul (ULift.{u_1, u} R) M
Equations
source
instance ULift.distribSMul' {R : Type u} {M : Type v} [AddZeroClass M] [DistribSMul R M] :
DistribSMul R (ULift.{u_1, v} M)
Equations
source
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 = let __src := ULift.mulAction; let __src_1 := ULift.distribSMul; DistribMulAction.mk ⋯ ⋯
source
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' = let __src := ULift.mulAction'; let __src_1 := ULift.distribSMul'; DistribMulAction.mk ⋯ ⋯
source
instance ULift.mulDistribMulAction {R : Type u} {M : Type v} [Monoid R] [Monoid M] [MulDistribMulAction R M] :
MulDistribMulAction (ULift.{u_1, u} R) M
Equations
source
instance ULift.mulDistribMulAction' {R : Type u} {M : Type v} [Monoid R] [Monoid M] [MulDistribMulAction R M] :
MulDistribMulAction R (ULift.{u_1, v} M)
Equations
source
instance ULift.smulWithZero {R : Type u} {M : Type v} [Zero R] [Zero M] [SMulWithZero R M] :
SMulWithZero (ULift.{u_1, u} R) M
Equations
source
instance ULift.smulWithZero' {R : Type u} {M : Type v} [Zero R] [Zero M] [SMulWithZero R M] :
SMulWithZero R (ULift.{u_1, v} M)
Equations
source
instance ULift.mulActionWithZero {R : Type u} {M : Type v} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] :
MulActionWithZero (ULift.{u_1, u} R) M
Equations
source
instance ULift.mulActionWithZero' {R : Type u} {M : Type v} [MonoidWithZero R] [Zero M] [MulActionWithZero R M] :
MulActionWithZero R (ULift.{u_1, v} M)
Equations
source
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 = let __src := ULift.smulWithZero; Module.mk ⋯ ⋯
source
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' = let __src := ULift.smulWithZero'; Module.mk ⋯ ⋯
source
@[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
source
@[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 }
source
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 = let __spread.0 := AddEquiv.ulift; { toFun := ULift.down, map_add' := ⋯, map_smul' := ⋯, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }
Instances For