Mathlib.Algebra.Module.ULift

ULift.smulLeft instance

[SMul R M] : SMul (ULift R) M

Full source

@[to_additive]
instance smulLeft [SMul R M] : SMul (ULift R) M :=
  ⟨fun s x => s.down • x⟩

Scalar Multiplication on Lifted Types

Informal description

For any type $R$ with a scalar multiplication operation on a type $M$, the lifted type $\mathrm{ULift}\, R$ also has a scalar multiplication operation on $M$, defined by $( \mathrm{up}\, r ) \cdot m = r \cdot m$ for $r \in R$ and $m \in M$.

ULift.smul_def theorem

[SMul R M] (s : ULift R) (x : M) : s • x = s.down • x

Full source

@[to_additive (attr := simp)]
theorem smul_def [SMul R M] (s : ULift R) (x : M) : s • x = s.down • x :=
  rfl

Scalar Multiplication Definition for Lifted Types

Informal description

For any type $R$ with a scalar multiplication operation on a type $M$, and for any lifted scalar $s \in \mathrm{ULift}\, R$ and element $x \in M$, the scalar multiplication $s \cdot x$ is equal to $s.\mathrm{down} \cdot x$, where $s.\mathrm{down}$ is the unlifted version of $s$.

ULift.isScalarTower instance

[SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] : IsScalarTower (ULift R) M N

Full source

instance isScalarTower [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] :
    IsScalarTower (ULift R) M N :=
  ⟨fun x y z => show (x.down • y) • z = x.down • y • z from smul_assoc _ _ _⟩

Scalar Tower Property for Lifted Scalar Type

Informal description

For any types $R$, $M$, and $N$ with scalar multiplication operations, if $R$ acts on $M$, $M$ acts on $N$, and $R$ acts on $N$ forming a scalar tower (i.e., $(r \cdot m) \cdot n = r \cdot (m \cdot n)$ for all $r \in R$, $m \in M$, $n \in N$), then the lifted type $\mathrm{ULift}\, R$ also forms a scalar tower with $M$ and $N$ under the same scalar multiplication structure.

ULift.isScalarTower' instance

[SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] : IsScalarTower R (ULift M) N

Full source

instance isScalarTower' [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] :
    IsScalarTower R (ULift M) N :=
  ⟨fun x y z => show (x • y.down) • z = x • y.down • z from smul_assoc _ _ _⟩

Scalar Tower Property for Lifted Module Type

Informal description

For any types $R$, $M$, and $N$ with scalar multiplication operations, if $R$ acts on $M$, $M$ acts on $N$, and $R$ acts on $N$ forming a scalar tower (i.e., $(r \cdot m) \cdot n = r \cdot (m \cdot n)$ for all $r \in R$, $m \in M$, $n \in N$), then the lifted type $\mathrm{ULift}\, M$ also forms a scalar tower with $R$ and $N$ under the same scalar multiplication structure.

ULift.isScalarTower'' instance

[SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] : IsScalarTower R M (ULift N)

Full source

instance isScalarTower'' [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] :
    IsScalarTower R M (ULift N) :=
  ⟨fun x y z => show up ((x • y) • z.down) = ⟨x • y • z.down⟩ by rw [smul_assoc]⟩

Scalar Tower Property for Lifted Target Type

Informal description

For any types $R$, $M$, and $N$ with scalar multiplication operations, if $R$ acts on $M$, $M$ acts on $N$, and $R$ acts on $N$ forming a scalar tower (i.e., $(r \cdot m) \cdot n = r \cdot (m \cdot n)$ for all $r \in R$, $m \in M$, $n \in N$), then the lifted type $\mathrm{ULift}\, N$ also forms a scalar tower with $R$ and $M$ under the same scalar multiplication structure.

ULift.instIsCentralScalar instance

[SMul R M] [SMul Rᵐᵒᵖ M] [IsCentralScalar R M] : IsCentralScalar R (ULift M)

Full source

instance [SMul R M] [SMul Rᵐᵒᵖ M] [IsCentralScalar R M] : IsCentralScalar R (ULift M) :=
  ⟨fun r m => congr_arg up <| op_smul_eq_smul r m.down⟩

Central Scalar Actions on Lifted Types

Informal description

For any type $R$ with scalar multiplication operations on a type $M$ and its multiplicative opposite $R^\text{op}$, if the scalar actions are central (i.e., the left and right actions coincide), then the lifted type $\text{ULift}(M)$ also has central scalar actions by $R$.

ULift.mulAction instance

[Monoid R] [MulAction R M] : MulAction (ULift R) M

Full source

@[to_additive]
instance mulAction [Monoid R] [MulAction R M] : MulAction (ULift R) M where
  smul := (· • ·)
  mul_smul _ _ := mul_smul _ _
  one_smul := one_smul _

Multiplicative Action on Lifted Monoid

Informal description

For any monoid $R$ with a multiplicative action on a type $M$, the lifted type $\mathrm{ULift}\, R$ also has a multiplicative action on $M$, defined by $(\mathrm{up}\, r) \cdot m = r \cdot m$ for all $r \in R$ and $m \in M$.

ULift.mulAction' instance

[Monoid R] [MulAction R M] : MulAction R (ULift M)

Full source

@[to_additive]
instance mulAction' [Monoid R] [MulAction R M] : MulAction R (ULift M) where
  smul := (· • ·)
  mul_smul := fun _ _ _ => congr_arg ULift.up <| mul_smul _ _ _
  one_smul := fun _ => congr_arg ULift.up <| one_smul _ _

Multiplicative Action on Lifted Types

Informal description

For any monoid $R$ with a multiplicative action on a type $M$, there is a multiplicative action of $R$ on the lifted type $\mathrm{ULift}\, M$ defined by $r \cdot \mathrm{up}\, m = \mathrm{up}\, (r \cdot m)$ for all $r \in R$ and $m \in M$.

ULift.smulZeroClass instance

[Zero M] [SMulZeroClass R M] : SMulZeroClass (ULift R) M

Full source

instance smulZeroClass [Zero M] [SMulZeroClass R M] : SMulZeroClass (ULift R) M :=
  { ULift.smulLeft with smul_zero := fun _ => smul_zero _ }

Zero-Preserving Scalar Multiplication on Lifted Types

Informal description

For any type $M$ with a zero element and a scalar multiplication operation by elements of type $R$ that preserves zero, the lifted type $\mathrm{ULift}\, R$ also has a scalar multiplication operation on $M$ that preserves zero. Specifically, for any $r \in R$ and $m \in M$, we have $(\mathrm{up}\, r) \cdot 0 = 0$.

ULift.smulZeroClass' instance

[Zero M] [SMulZeroClass R M] : SMulZeroClass R (ULift M)

Full source

instance smulZeroClass' [Zero M] [SMulZeroClass R M] : SMulZeroClass R (ULift M) where
  smul_zero c := by { ext; simp [smul_zero] }

Zero-Preserving Scalar Multiplication on Lifted Types

Informal description

For any type $M$ with a zero element and any type $R$ with a scalar multiplication operation that preserves zero (i.e., $r \cdot 0 = 0$ for all $r \in R$), the lifted type $\text{ULift}(M)$ inherits a scalar multiplication operation from $R$ that also preserves zero.

ULift.distribSMul instance

[AddZeroClass M] [DistribSMul R M] : DistribSMul (ULift R) M

Full source

instance distribSMul [AddZeroClass M] [DistribSMul R M] : DistribSMul (ULift R) M where
  smul_add _ := smul_add _

Distributive Scalar Multiplication on Lifted Types

Informal description

For any type $M$ with an additive zero class structure and any type $R$ with a distributive scalar multiplication action on $M$, the lifted type $\mathrm{ULift}\, R$ also has a distributive scalar multiplication action on $M$. This means that for any $r \in R$ and $x, y \in M$, we have $(\mathrm{up}\, r) \cdot (x + y) = (\mathrm{up}\, r) \cdot x + (\mathrm{up}\, r) \cdot y$.

ULift.distribSMul' instance

[AddZeroClass M] [DistribSMul R M] : DistribSMul R (ULift M)

Full source

instance distribSMul' [AddZeroClass M] [DistribSMul R M] : DistribSMul R (ULift M) where
  smul_add c f g := by
    ext
    simp [smul_add]

Distributive Scalar Multiplication on Lifted Additive Zero Classes

Informal description

For any type $M$ with an additive zero class structure and any type $R$ with a distributive scalar multiplication action on $M$, the lifted type $\mathrm{ULift}\, M$ inherits a distributive scalar multiplication action from $R$. This means that for any $r \in R$ and $x, y \in \mathrm{ULift}\, M$, we have $r \cdot (x + y) = r \cdot x + r \cdot y$.

ULift.distribMulAction instance

[Monoid R] [AddMonoid M] [DistribMulAction R M] : DistribMulAction (ULift R) M

Full source

instance distribMulAction [Monoid R] [AddMonoid M] [DistribMulAction R M] :
    DistribMulAction (ULift R) M :=
  { ULift.mulAction, ULift.distribSMul with }

Distributive Multiplicative Action on Lifted Monoids

Informal description

For any monoid $R$ and additive monoid $M$ with a distributive multiplicative action of $R$ on $M$, the lifted type $\mathrm{ULift}\, R$ also has a distributive multiplicative action on $M$. This means that for any $r \in R$ and $x, y \in M$, we have $(\mathrm{up}\, r) \cdot (x + y) = (\mathrm{up}\, r) \cdot x + (\mathrm{up}\, r) \cdot y$ and $(\mathrm{up}\, r) \cdot 0 = 0$.

ULift.distribMulAction' instance

[Monoid R] [AddMonoid M] [DistribMulAction R M] : DistribMulAction R (ULift M)

Full source

instance distribMulAction' [Monoid R] [AddMonoid M] [DistribMulAction R M] :
    DistribMulAction R (ULift M) :=
  { ULift.mulAction', ULift.distribSMul' with }

Distributive Multiplicative Action on Lifted Additive Monoids

Informal description

For any monoid $R$ and additive monoid $M$ with a distributive multiplicative action of $R$ on $M$, the lifted type $\mathrm{ULift}\, M$ inherits a distributive multiplicative action from $R$. This means that for any $r \in R$ and $x, y \in \mathrm{ULift}\, M$, we have $r \cdot (x + y) = r \cdot x + r \cdot y$ and $r \cdot 0 = 0$.

ULift.mulDistribMulAction instance

[Monoid R] [Monoid M] [MulDistribMulAction R M] : MulDistribMulAction (ULift R) M

Full source

instance mulDistribMulAction [Monoid R] [Monoid M] [MulDistribMulAction R M] :
    MulDistribMulAction (ULift R) M where
  smul_one _ := smul_one _
  smul_mul _ := smul_mul' _

Multiplicative Distributive Action on Lifted Monoids

Informal description

For any monoid $R$ and monoid $M$ with a multiplicative distributive action of $R$ on $M$, the lifted type $\mathrm{ULift}\, R$ also has a multiplicative distributive action on $M$. This means that for any $r \in R$ and $m_1, m_2 \in M$, the action satisfies $(\mathrm{up}\, r) \cdot (m_1 * m_2) = ((\mathrm{up}\, r) \cdot m_1) * ((\mathrm{up}\, r) \cdot m_2)$.

ULift.mulDistribMulAction' instance

[Monoid R] [Monoid M] [MulDistribMulAction R M] : MulDistribMulAction R (ULift M)

Full source

instance mulDistribMulAction' [Monoid R] [Monoid M] [MulDistribMulAction R M] :
    MulDistribMulAction R (ULift M) :=
  { ULift.mulAction' with
    smul_one := fun _ => by
      ext
      simp [smul_one]
    smul_mul := fun _ _ _ => by
      ext
      simp [smul_mul'] }

Multiplicative Distributive Action on Lifted Types

Informal description

For any monoid $R$ and monoid $M$ with a multiplicative distributive action of $R$ on $M$, there is a multiplicative distributive action of $R$ on the lifted type $\mathrm{ULift}\, M$ defined by $r \cdot \mathrm{up}\, m = \mathrm{up}\, (r \cdot m)$ for all $r \in R$ and $m \in M$.

ULift.smulWithZero instance

[Zero R] [Zero M] [SMulWithZero R M] : SMulWithZero (ULift R) M

Full source

instance smulWithZero [Zero R] [Zero M] [SMulWithZero R M] : SMulWithZero (ULift R) M :=
  { ULift.smulLeft with
    smul_zero := fun _ => smul_zero _
    zero_smul := zero_smul _ }

Zero-Preserving Scalar Multiplication on Lifted Types

Informal description

For any types $R$ and $M$ with zero elements and a scalar multiplication operation that preserves zero (i.e., $0 \cdot m = 0$ and $r \cdot 0 = 0$ for all $r \in R$ and $m \in M$), the lifted type $\mathrm{ULift}\, R$ also has a scalar multiplication operation on $M$ that preserves zero.

ULift.smulWithZero' instance

[Zero R] [Zero M] [SMulWithZero R M] : SMulWithZero R (ULift M)

Full source

instance smulWithZero' [Zero R] [Zero M] [SMulWithZero R M] : SMulWithZero R (ULift M) where
  smul_zero _ := ULift.ext _ _ <| smul_zero _
  zero_smul _ := ULift.ext _ _ <| zero_smul _ _

Scalar Multiplication with Zero on Lifted Types

Informal description

For any types $R$ and $M$ with zero elements and a scalar multiplication operation $R \times M \to M$ that preserves zero, there is a scalar multiplication operation $R \times \text{ULift}(M) \to \text{ULift}(M)$ that also preserves zero.

ULift.mulActionWithZero instance

[MonoidWithZero R] [Zero M] [MulActionWithZero R M] : MulActionWithZero (ULift R) M

Full source

instance mulActionWithZero [MonoidWithZero R] [Zero M] [MulActionWithZero R M] :
    MulActionWithZero (ULift R) M :=
  { ULift.smulWithZero with
    one_smul := one_smul _
    mul_smul := mul_smul }

Multiplicative Action with Zero on Lifted Monoids

Informal description

For any monoid with zero $R$ and any type $M$ with a zero element, if $M$ has a multiplicative action with zero by $R$, then the lifted type $\mathrm{ULift}\, R$ also has a multiplicative action with zero on $M$.

ULift.mulActionWithZero' instance

[MonoidWithZero R] [Zero M] [MulActionWithZero R M] : MulActionWithZero R (ULift M)

Full source

instance mulActionWithZero' [MonoidWithZero R] [Zero M] [MulActionWithZero R M] :
    MulActionWithZero R (ULift M) :=
  { ULift.smulWithZero' with
    one_smul := one_smul _
    mul_smul := mul_smul }

Multiplicative Action with Zero on Lifted Types

Informal description

For any monoid with zero $R$, any type $M$ with a zero element, and a multiplicative action of $R$ on $M$ that preserves zero, there is a multiplicative action of $R$ on $\text{ULift}(M)$ that also preserves zero.

ULift.module instance

[Semiring R] [AddCommMonoid M] [Module R M] : Module (ULift R) M

Full source

instance module [Semiring R] [AddCommMonoid M] [Module R M] : Module (ULift R) M :=
  { ULift.smulWithZero with
    add_smul := fun _ _ => add_smul _ _
    smul_add := smul_add
    one_smul := one_smul _
    mul_smul := mul_smul }

Module Structure on Lifted Semiring

Informal description

For any semiring $R$, additive commutative monoid $M$, and module structure of $R$ over $M$, the lifted type $\mathrm{ULift}\, R$ also has a module structure over $M$.

ULift.module' instance

[Semiring R] [AddCommMonoid M] [Module R M] : Module R (ULift M)

Full source

instance module' [Semiring R] [AddCommMonoid M] [Module R M] : Module R (ULift M) :=
  { ULift.smulWithZero' with
    add_smul := fun _ _ _ => ULift.ext _ _ <| add_smul _ _ _
    one_smul := one_smul _
    mul_smul := mul_smul
    smul_add := smul_add }

Module Structure on Lifted Types

Informal description

For any semiring $R$ and any $R$-module $M$, the lifted type $\text{ULift}(M)$ is also an $R$-module.

ULift.moduleEquiv definition

[Semiring R] [AddCommMonoid M] [Module R M] : ULift.{w} M ≃ₗ[R] M

Full source

/-- The `R`-linear equivalence between `ULift M` and `M`.

This is a linear version of `AddEquiv.ulift`. -/
@[simps apply symm_apply]
def moduleEquiv [Semiring R] [AddCommMonoid M] [Module R M] : ULiftULift.{w} M ≃ₗ[R] M where
  toFun := ULift.down
  invFun := ULift.up
  map_smul' _ _ := rfl
  __ := AddEquiv.ulift

Linear equivalence between lifted module and original module

Informal description

For a semiring $R$ and an $R$-module $M$, the linear equivalence between $\text{ULift}(M)$ and $M$ is given by the functions $\text{ULift.down}$ (projection) and $\text{ULift.up}$ (lifting), which preserve the module structure. Specifically, this equivalence is $R$-linear and additive.