# 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.vaddLeft {R : Type u} {M : Type v} [inst : VAdd R M] :
Equations
• ULift.vaddLeft = { vadd := fun s x => s.down +ᵥ x }
instance ULift.smulLeft {R : Type u} {M : Type v} [inst : SMul R M] :
SMul () M
Equations
• ULift.smulLeft = { smul := fun s x => s.down x }
@[simp]
theorem ULift.vadd_def {R : Type u} {M : Type v} [inst : VAdd R M] (s : ) (x : M) :
s +ᵥ x = s.down +ᵥ x
@[simp]
theorem ULift.smul_def {R : Type u} {M : Type v} [inst : SMul R M] (s : ) (x : M) :
s x = s.down x
instance ULift.isScalarTower {R : Type u} {M : Type v} {N : Type w} [inst : SMul R M] [inst : SMul M N] [inst : SMul R N] [inst : ] :
Equations
instance ULift.isScalarTower' {R : Type u} {M : Type v} {N : Type w} [inst : SMul R M] [inst : SMul M N] [inst : SMul R N] [inst : ] :
Equations
instance ULift.isScalarTower'' {R : Type u} {M : Type v} {N : Type w} [inst : SMul R M] [inst : SMul M N] [inst : SMul R N] [inst : ] :
Equations
instance ULift.instIsCentralScalarULiftSmulMulOpposite {R : Type u} {M : Type v} [inst : SMul R M] [inst : SMul Rᵐᵒᵖ M] [inst : ] :
Equations
instance ULift.addAction {R : Type u} {M : Type v} [inst : ] [inst : ] :
Equations
def ULift.addAction.proof_1 {R : Type u_2} {M : Type u_3} [inst : ] [inst : ] :
∀ (x x_1 : ) (b : M), x.down + x_1.down +ᵥ b = x.down +ᵥ (x_1.down +ᵥ b)
Equations
• (_ : ∀ (b : M), x.down + x.down +ᵥ b = x.down +ᵥ (x.down +ᵥ b)) = (_ : ∀ (p : M), x.down + x.down +ᵥ p = x.down +ᵥ (x.down +ᵥ p))
instance ULift.mulAction {R : Type u} {M : Type v} [inst : ] [inst : ] :
Equations
• ULift.mulAction = MulAction.mk (_ : ∀ (b : M), 1 b = b) (_ : ∀ (x x_1 : ) (b : M), (x.down * x_1.down) b = x.down x_1.down b)
def ULift.addAction'.proof_1 {R : Type u_3} {M : Type u_2} [inst : ] [inst : ] :
∀ (x : ), { down := (0 +ᵥ x).down } = { down := x.down }
Equations
• (_ : { down := (0 +ᵥ x).down } = { down := x.down }) = (_ : { down := (0 +ᵥ x).down } = { down := x.down })
def ULift.addAction'.proof_2 {R : Type u_3} {M : Type u_2} [inst : ] [inst : ] :
∀ (x x_1 : R) (x_2 : ), { down := (x + x_1 +ᵥ x_2).down } = { down := (x +ᵥ (x_1 +ᵥ x_2)).down }
Equations
• (_ : { down := (x + x +ᵥ x).down } = { down := (x +ᵥ (x +ᵥ x)).down }) = (_ : { down := (x + x +ᵥ x).down } = { down := (x +ᵥ (x +ᵥ x)).down })
instance ULift.addAction' {R : Type u} {M : Type v} [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance ULift.mulAction' {R : Type u} {M : Type v} [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance ULift.smulZeroClass {R : Type u} {M : Type v} [inst : Zero M] [inst : ] :
Equations
instance ULift.smulZeroClass' {R : Type u} {M : Type v} [inst : Zero M] [inst : ] :
Equations
instance ULift.distribSmul {R : Type u} {M : Type v} [inst : ] [inst : ] :
Equations
instance ULift.distribSmul' {R : Type u} {M : Type v} [inst : ] [inst : ] :
Equations
instance ULift.distribMulAction {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance ULift.distribMulAction' {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance ULift.mulDistribMulAction {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : ] :
Equations
instance ULift.mulDistribMulAction' {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : ] :
Equations
instance ULift.smulWithZero {R : Type u} {M : Type v} [inst : Zero R] [inst : Zero M] [inst : ] :
Equations
instance ULift.smulWithZero' {R : Type u} {M : Type v} [inst : Zero R] [inst : Zero M] [inst : ] :
Equations
instance ULift.mulActionWithZero {R : Type u} {M : Type v} [inst : ] [inst : Zero M] [inst : ] :
Equations
instance ULift.mulActionWithZero' {R : Type u} {M : Type v} [inst : ] [inst : Zero M] [inst : ] :
Equations
instance ULift.module {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :
Module () M
Equations
• ULift.module = let src := ULift.smulWithZero; Module.mk (_ : ∀ (x x_1 : ) (x_2 : M), (x.down + x_1.down) x_2 = x.down x_2 + x_1.down x_2) (_ : ∀ (m : M), 0 m = 0)
instance ULift.module' {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :
Module R ()
Equations
• ULift.module' = let src := ULift.smulWithZero'; Module.mk (_ : ∀ (x x_1 : R) (x_2 : ), (x + x_1) x_2 = x x_2 + x_1 x_2) (_ : ∀ (m : ), 0 m = 0)
@[simp]
theorem ULift.moduleEquiv_apply {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] (self : ) :
ULift.moduleEquiv self = self.down
@[simp]
theorem ULift.moduleEquiv_symm_apply {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] (down : M) :
↑(LinearEquiv.symm ULift.moduleEquiv) down = { down := down }
def ULift.moduleEquiv {R : Type u} {M : Type v} [inst : ] [inst : ] [inst : Module R M] :

The R-linear equivalence between ULift M and M.

Equations
• One or more equations did not get rendered due to their size.