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] :
VAdd (ULift 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 (ULift R) 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 : ULift R) (x : M) :
s +ᵥ x = s.down +ᵥ x
@[simp]
theorem ULift.smul_def {R : Type u} {M : Type v} [inst : SMul R M] (s : ULift R) (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 : IsScalarTower R M N] :
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 : IsScalarTower R M N] :
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 : IsScalarTower R M N] :
Equations
instance ULift.addAction {R : Type u} {M : Type v} [inst : AddMonoid R] [inst : AddAction R M] :
Equations
def ULift.addAction.proof_1 {R : Type u_2} {M : Type u_3} [inst : AddMonoid R] [inst : AddAction R M] :
∀ (x x_1 : ULift R) (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 : Monoid R] [inst : MulAction R M] :
Equations
def ULift.addAction'.proof_1 {R : Type u_3} {M : Type u_2} [inst : AddMonoid R] [inst : AddAction R M] :
∀ (x : ULift M), { 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 : AddMonoid R] [inst : AddAction R M] :
∀ (x x_1 : R) (x_2 : ULift M), { 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 : AddMonoid R] [inst : AddAction R M] :
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.mulAction' {R : Type u} {M : Type v} [inst : Monoid R] [inst : MulAction R M] :
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 : SMulZeroClass R M] :
Equations
instance ULift.smulZeroClass' {R : Type u} {M : Type v} [inst : Zero M] [inst : SMulZeroClass R M] :
Equations
instance ULift.distribSmul {R : Type u} {M : Type v} [inst : AddZeroClass M] [inst : DistribSMul R M] :
Equations
instance ULift.distribSmul' {R : Type u} {M : Type v} [inst : AddZeroClass M] [inst : DistribSMul R M] :
Equations
instance ULift.distribMulAction {R : Type u} {M : Type v} [inst : Monoid R] [inst : AddMonoid M] [inst : DistribMulAction R M] :
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.distribMulAction' {R : Type u} {M : Type v} [inst : Monoid R] [inst : AddMonoid M] [inst : DistribMulAction R M] :
Equations
  • One or more equations did not get rendered due to their size.
instance ULift.mulDistribMulAction {R : Type u} {M : Type v} [inst : Monoid R] [inst : Monoid M] [inst : MulDistribMulAction R M] :
Equations
instance ULift.mulDistribMulAction' {R : Type u} {M : Type v} [inst : Monoid R] [inst : Monoid M] [inst : MulDistribMulAction R M] :
Equations
instance ULift.smulWithZero {R : Type u} {M : Type v} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] :
Equations
instance ULift.smulWithZero' {R : Type u} {M : Type v} [inst : Zero R] [inst : Zero M] [inst : SMulWithZero R M] :
Equations
instance ULift.mulActionWithZero {R : Type u} {M : Type v} [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] :
Equations
instance ULift.mulActionWithZero' {R : Type u} {M : Type v} [inst : MonoidWithZero R] [inst : Zero M] [inst : MulActionWithZero R M] :
Equations
instance ULift.module {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
Equations
  • ULift.module = let src := ULift.smulWithZero; Module.mk (_ : ∀ (x x_1 : ULift R) (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 : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
Equations
@[simp]
theorem ULift.moduleEquiv_apply {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (self : ULift M) :
ULift.moduleEquiv self = self.down
@[simp]
theorem ULift.moduleEquiv_symm_apply {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (down : M) :
↑(LinearEquiv.symm ULift.moduleEquiv) down = { down := down }
def ULift.moduleEquiv {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [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.