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
instance
ULift.mulAction
{R : Type u}
{M : Type v}
[Monoid R]
[MulAction R M]
:
MulAction (ULift.{u_1, u} R) M
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)
instance
ULift.mulAction'
{R : Type u}
{M : Type v}
[Monoid R]
[MulAction R M]
:
MulAction R (ULift.{u_1, v} M)
instance
ULift.smulZeroClass
{R : Type u}
{M : Type v}
[Zero M]
[SMulZeroClass R M]
:
SMulZeroClass (ULift.{u_1, u} R) M
instance
ULift.smulZeroClass'
{R : Type u}
{M : Type v}
[Zero M]
[SMulZeroClass R M]
:
SMulZeroClass R (ULift.{u_1, v} M)
instance
ULift.distribSmul
{R : Type u}
{M : Type v}
[AddZeroClass M]
[DistribSMul R M]
:
DistribSMul (ULift.{u_1, u} R) M
instance
ULift.distribSmul'
{R : Type u}
{M : Type v}
[AddZeroClass M]
[DistribSMul R M]
:
DistribSMul R (ULift.{u_1, v} M)
instance
ULift.distribMulAction
{R : Type u}
{M : Type v}
[Monoid R]
[AddMonoid M]
[DistribMulAction R M]
:
instance
ULift.distribMulAction'
{R : Type u}
{M : Type v}
[Monoid R]
[AddMonoid M]
[DistribMulAction R M]
:
instance
ULift.mulDistribMulAction
{R : Type u}
{M : Type v}
[Monoid R]
[Monoid M]
[MulDistribMulAction R M]
:
instance
ULift.mulDistribMulAction'
{R : Type u}
{M : Type v}
[Monoid R]
[Monoid M]
[MulDistribMulAction R M]
:
instance
ULift.smulWithZero
{R : Type u}
{M : Type v}
[Zero R]
[Zero M]
[SMulWithZero R M]
:
SMulWithZero (ULift.{u_1, u} R) M
instance
ULift.smulWithZero'
{R : Type u}
{M : Type v}
[Zero R]
[Zero M]
[SMulWithZero R M]
:
SMulWithZero R (ULift.{u_1, v} M)
instance
ULift.mulActionWithZero
{R : Type u}
{M : Type v}
[MonoidWithZero R]
[Zero M]
[MulActionWithZero R M]
:
instance
ULift.mulActionWithZero'
{R : Type u}
{M : Type v}
[MonoidWithZero R]
[Zero M]
[MulActionWithZero R M]
:
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.