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} [VAdd R M] :
Equations
instance ULift.smulLeft {R : Type u} {M : Type v} [SMul R M] :
Equations
@[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
@[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
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] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
instance ULift.addAction {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] :
Equations
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)
instance ULift.mulAction {R : Type u} {M : Type v} [Monoid R] [MulAction R M] :
Equations
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 }
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 }
instance ULift.addAction' {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] :
Equations
instance ULift.mulAction' {R : Type u} {M : Type v} [Monoid R] [MulAction R M] :
Equations
instance ULift.smulZeroClass {R : Type u} {M : Type v} [Zero M] [SMulZeroClass R M] :
Equations
instance ULift.smulZeroClass' {R : Type u} {M : Type v} [Zero M] [SMulZeroClass R M] :
Equations
Equations
Equations
Equations
  • ULift.distribMulAction = let __src := ULift.mulAction; let __src_1 := ULift.distribSMul; DistribMulAction.mk
Equations
  • ULift.distribMulAction' = let __src := ULift.mulAction'; let __src_1 := ULift.distribSMul'; DistribMulAction.mk
Equations
Equations
instance ULift.smulWithZero {R : Type u} {M : Type v} [Zero R] [Zero M] [SMulWithZero R M] :
Equations
instance ULift.smulWithZero' {R : Type u} {M : Type v} [Zero R] [Zero M] [SMulWithZero R M] :
Equations
Equations
Equations
instance ULift.module {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
Equations
  • ULift.module = let __src := ULift.smulWithZero; Module.mk
instance ULift.module' {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :
Equations
  • ULift.module' = let __src := ULift.smulWithZero'; Module.mk
@[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
@[simp]
theorem ULift.moduleEquiv_symm_apply {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (down : M) :
(LinearEquiv.symm ULift.moduleEquiv) down = { down := down }

The R-linear equivalence between ULift M and M.

This is a linear version of AddEquiv.ulift.

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