Documentation

Monlib.LinearAlgebra.LmulRmul

lmul and rmul (the left and right multiplication maps) #

Basically just copies of linear_map.mul_left and linear_map.mul_right but defined as linear maps.

theorem LinearMap.mulLeft_conj_of_mulEquivClass_apply {R : Type u_4} {E : Type u_2} {F : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring E] [NonUnitalNonAssocSemiring F] [Module R E] [Module R F] [SMulCommClass R E E] [SMulCommClass R F F] {Fn : Type u_1} [EquivLike Fn E F] [MulEquivClass Fn E F] (f : Fn) (x : E) (y : F) :

f ((mulLeft R x) (EquivLike.inv f y)) = (mulLeft R (f x)) y

theorem LinearMap.mulRight_conj_of_mulEquivClass_apply {R : Type u_4} {E : Type u_2} {F : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring E] [NonUnitalNonAssocSemiring F] [Module R E] [Module R F] [IsScalarTower R E E] [IsScalarTower R F F] {Fn : Type u_1} [EquivLike Fn E F] [MulEquivClass Fn E F] (f : Fn) (x : E) (y : F) :

f ((mulRight R x) (EquivLike.inv f y)) = (mulRight R (f x)) y

theorem left_module_map_iff {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [Semiring H₁] [Algebra R H₁] {x : H₁ →ₗ[R] H₁} :

(∀ (a b : H₁), x (a * b) = a * x b) ↔ x = LinearMap.mulRight R (x 1)

theorem right_module_map_iff {R : Type u_2} [CommSemiring R] {H₂ : Type u_1} [Semiring H₂] [Algebra R H₂] {x : H₂ →ₗ[R] H₂} :

(∀ (a b : H₂), x (a * b) = x a * b) ↔ x = LinearMap.mulLeft R (x 1)

def lmul {R : Type u_1} {H₁ : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] :

H₁ →ₗ[R] H₁ →ₗ[R] H₁

Equations

lmul = { toFun := fun (x : H₁) => LinearMap.mulLeft R x, map_add' := ⋯, map_smul' := ⋯ }

Instances For

theorem lmul_apply {R : Type u_2} {H₁ : Type u_1} [CommSemiring R] [NonUnitalNonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] (x y : H₁) :

(lmul x) y = x * y

theorem lmul_eq_mul {R : Type u_2} {H₁ : Type u_1} [CommSemiring R] [NonUnitalNonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] (x : H₁) :

lmul x = LinearMap.mulLeft R x

theorem lmul_eq_alg_lmul {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [Semiring H₁] [Algebra R H₁] (x : H₁) :

lmul x = (Algebra.lmul R H₁) x

theorem lmul_one {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [NonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] :

lmul 1 = 1

def rmul {R : Type u_1} {H₂ : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring H₂] [Module R H₂] [SMulCommClass R H₂ H₂] [IsScalarTower R H₂ H₂] :

H₂ →ₗ[R] H₂ →ₗ[R] H₂

Equations

rmul = { toFun := fun (x : H₂) => LinearMap.mulRight R x, map_add' := ⋯, map_smul' := ⋯ }

Instances For

theorem rmul_apply {R : Type u_2} {H₂ : Type u_1} [CommSemiring R] [NonUnitalNonAssocSemiring H₂] [Module R H₂] [SMulCommClass R H₂ H₂] [IsScalarTower R H₂ H₂] (x y : H₂) :

(rmul x) y = y * x

theorem rmul_eq_mul {R : Type u_2} {H₂ : Type u_1} [CommSemiring R] [NonUnitalNonAssocSemiring H₂] [Module R H₂] [SMulCommClass R H₂ H₂] [IsScalarTower R H₂ H₂] (x : H₂) :

rmul x = LinearMap.mulRight R x

theorem rmul_one {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [NonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] :

rmul 1 = 1

noncomputable def rmulMapLmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] [NonUnitalNonAssocSemiring H₂] [Module R H₂] [SMulCommClass R H₂ H₂] [IsScalarTower R H₂ H₂] :

TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂ →ₗ[R] TensorProduct R H₁ H₂

Equations

rmulMapLmul = TensorProduct.homTensorHomMap R H₁ H₂ H₁ H₂ ∘ₗ TensorProduct.map rmul lmul

Instances For

theorem rmulMapLmul_apply {R : Type u_3} {H₁ : Type u_1} {H₂ : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] [NonUnitalNonAssocSemiring H₂] [Module R H₂] [SMulCommClass R H₂ H₂] [IsScalarTower R H₂ H₂] (x : H₁) (y : H₂) :

rmulMapLmul (x ⊗ₜ[R] y) = TensorProduct.map (rmul x) (lmul y)

theorem rmulMapLmul_one {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [NonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] {H₂ : Type u_3} [NonAssocSemiring H₂] [Module R H₂] [SMulCommClass R H₂ H₂] [IsScalarTower R H₂ H₂] :

rmulMapLmul (1 ⊗ₜ[R] 1) = 1

theorem LinearMap.mulLeft_sum {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {n : Type u_3} {s : Finset n} {x : n → A} :

∑ i ∈ s, mulLeft R (x i) = mulLeft R (∑ i ∈ s, x i)

theorem LinearMap.mulRight_sum {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {n : Type u_3} {s : Finset n} {x : n → A} :

∑ i ∈ s, mulRight R (x i) = mulRight R (∑ i ∈ s, x i)

theorem lmul_eq_zero_iff {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [Semiring H₁] [Algebra R H₁] (x : H₁) :

lmul x = 0 ↔ x = 0

theorem rmul_eq_zero_iff {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [Semiring H₁] [Algebra R H₁] (x : H₁) :

rmul x = 0 ↔ x = 0

theorem lmul_eq_one_iff {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [NonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] (x : H₁) :

lmul x = 1 ↔ x = 1

theorem LinearMap.mulLeft_eq_one_iff {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [NonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] (x : H₁) :

mulLeft R x = 1 ↔ x = 1

theorem rmul_eq_one_iff {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [NonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] (x : H₁) :

rmul x = 1 ↔ x = 1

theorem LinearMap.mulRight_eq_one_iff {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [NonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] (x : H₁) :

mulRight R x = 1 ↔ x = 1

theorem LinearMap.mulLeft_eq_one_or_zero_iff_mulRight_tfae {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [Semiring H₁] [Algebra R H₁] (x : H₁) (p : Prop) [Decidable p] :

[mulLeft R x = if p then 1 else 0, mulRight R x = if p then 1 else 0, x = if p then 1 else 0].TFAE

theorem LinearMap.mulLeft_eq_one_or_zero_iff_mulRight {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [Semiring H₁] [Algebra R H₁] (x : H₁) (p : Prop) [Decidable p] :

(mulLeft R x = if p then 1 else 0) ↔ mulRight R x = if p then 1 else 0

theorem LinearMap.mulRight_smul {R : Type u_2} {H₁ : Type u_1} [CommSemiring R] [NonUnitalNonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] (x : H₁) (α : R) :

mulRight R (α • x) = α • mulRight R x

theorem LinearMap.mulLeft_smul {R : Type u_2} {H₁ : Type u_1} [CommSemiring R] [NonUnitalNonAssocSemiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] (x : H₁) (α : R) :

mulLeft R (α • x) = α • mulLeft R x

theorem LinearMap.mulLeft_comp_inj {R : Type u_3} [CommSemiring R] {H₁ : Type u_1} {H₂ : Type u_2} [Semiring H₁] [Module R H₁] [AddCommMonoid H₂] [Module R H₂] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] (f g : H₁ →ₗ[R] H₂) (x : H₁) [Invertible x] :

f ∘ₗ mulLeft R x = g ∘ₗ mulLeft R x ↔ f = g

theorem LinearMap.mulLeft_inj {R : Type u_2} [CommSemiring R] {H₁ : Type u_1} [Semiring H₁] [Module R H₁] [SMulCommClass R H₁ H₁] [IsScalarTower R H₁ H₁] (x : H₁) [Invertible x] (y z : H₁) :

(mulLeft R x) y = (mulLeft R x) z ↔ y = z

theorem lmul_op {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (x : Aᵐᵒᵖ) :

lmul x = (rmul (MulOpposite.unop x)).op

theorem lmul_op' {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (x : A) :

lmul (MulOpposite.op x) = (rmul x).op

theorem rmul_op' {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (x : A) :

rmul (MulOpposite.op x) = (lmul x).op