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.
@[simp]
@[simp]
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.instIsCentralScalarULiftSmulMulOpposite
{R : Type u}
{M : Type v}
[SMul R M]
[SMul Rᵐᵒᵖ M]
[IsCentralScalar R M]
:
instance
ULift.addAction
{R : Type u}
{M : Type v}
[AddMonoid R]
[AddAction R M]
:
AddAction (ULift.{u_1, u} R) M
Equations
- ULift.addAction = AddAction.mk (_ : ∀ (b : M), 0 +ᵥ b = b) (_ : ∀ (x x_1 : ULift.{u_1, u} 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]
:
MulAction (ULift.{u_1, u} R) M
Equations
- ULift.mulAction = MulAction.mk (_ : ∀ (b : M), 1 • b = b) (_ : ∀ (x x_1 : ULift.{u_1, u} R) (b : M), (x.down * x_1.down) • b = x.down • x_1.down • b)
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 }
instance
ULift.addAction'
{R : Type u}
{M : Type v}
[AddMonoid R]
[AddAction R M]
:
AddAction R (ULift.{u_1, v} M)
Equations
- One or more equations did not get rendered due to their size.
instance
ULift.mulAction'
{R : Type u}
{M : Type v}
[Monoid R]
[MulAction R M]
:
MulAction R (ULift.{u_1, v} M)
Equations
- One or more equations did not get rendered due to their size.
instance
ULift.smulZeroClass
{R : Type u}
{M : Type v}
[Zero M]
[SMulZeroClass R M]
:
SMulZeroClass (ULift.{u_1, u} R) M
Equations
- ULift.smulZeroClass = let src := ULift.smulLeft; SMulZeroClass.mk (_ : ∀ (x : ULift.{u_1, u} R), x.down • 0 = 0)
instance
ULift.smulZeroClass'
{R : Type u}
{M : Type v}
[Zero M]
[SMulZeroClass R M]
:
SMulZeroClass R (ULift.{u_1, v} M)
Equations
- ULift.smulZeroClass' = SMulZeroClass.mk (_ : ∀ (c : R), c • 0 = 0)
instance
ULift.distribSmul
{R : Type u}
{M : Type v}
[AddZeroClass M]
[DistribSMul R M]
:
DistribSMul (ULift.{u_1, u} R) M
Equations
- ULift.distribSmul = DistribSMul.mk (_ : ∀ (x : ULift.{u_1, u} R) (b₁ b₂ : M), x.down • (b₁ + b₂) = x.down • b₁ + x.down • b₂)
instance
ULift.distribSmul'
{R : Type u}
{M : Type v}
[AddZeroClass M]
[DistribSMul R M]
:
DistribSMul R (ULift.{u_1, v} M)
Equations
- ULift.distribSmul' = DistribSMul.mk (_ : ∀ (c : R) (f g : ULift.{u_1, v} M), c • (f + g) = c • f + c • g)
instance
ULift.distribMulAction
{R : Type u}
{M : Type v}
[Monoid R]
[AddMonoid M]
[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}
[Monoid R]
[AddMonoid M]
[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}
[Monoid R]
[Monoid M]
[MulDistribMulAction R M]
:
Equations
- One or more equations did not get rendered due to their size.
instance
ULift.mulDistribMulAction'
{R : Type u}
{M : Type v}
[Monoid R]
[Monoid M]
[MulDistribMulAction R M]
:
Equations
- One or more equations did not get rendered due to their size.
instance
ULift.smulWithZero
{R : Type u}
{M : Type v}
[Zero R]
[Zero M]
[SMulWithZero R M]
:
SMulWithZero (ULift.{u_1, u} R) M
Equations
- ULift.smulWithZero = let src := ULift.smulLeft; SMulWithZero.mk (_ : ∀ (m : M), 0 • m = 0)
instance
ULift.smulWithZero'
{R : Type u}
{M : Type v}
[Zero R]
[Zero M]
[SMulWithZero R M]
:
SMulWithZero R (ULift.{u_1, v} M)
Equations
- ULift.smulWithZero' = SMulWithZero.mk (_ : ∀ (x : ULift.{u_1, v} M), 0 • x = 0)
instance
ULift.mulActionWithZero
{R : Type u}
{M : Type v}
[MonoidWithZero R]
[Zero M]
[MulActionWithZero R M]
:
Equations
- ULift.mulActionWithZero = let src := ULift.smulWithZero; MulActionWithZero.mk (_ : ∀ (a : ULift.{u_1, u} R), a • 0 = 0) (_ : ∀ (m : M), 0 • m = 0)
instance
ULift.mulActionWithZero'
{R : Type u}
{M : Type v}
[MonoidWithZero R]
[Zero M]
[MulActionWithZero R M]
:
Equations
- ULift.mulActionWithZero' = let src := ULift.smulWithZero'; MulActionWithZero.mk (_ : ∀ (a : R), a • 0 = 0) (_ : ∀ (m : ULift.{u_1, v} M), 0 • m = 0)
instance
ULift.module
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Module (ULift.{u_1, u} R) M
instance
ULift.module'
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Module R (ULift.{u_1, v} M)
@[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 }
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
- One or more equations did not get rendered due to their size.