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
linear_map.mul_left_conj_of_mul_equiv
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[comm_semiring R]
[non_unital_non_assoc_semiring E]
[non_unital_non_assoc_semiring F]
[module R E]
[module R F]
[smul_comm_class R E E]
[smul_comm_class R F F]
[is_scalar_tower R E E]
[is_scalar_tower R F F]
(f : E ≃* F)
(x : E) :
theorem
linear_map.mul_right_conj_of_mul_equiv
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[comm_semiring R]
[non_unital_non_assoc_semiring E]
[non_unital_non_assoc_semiring F]
[module R E]
[module R F]
[smul_comm_class R E E]
[smul_comm_class R F F]
[is_scalar_tower R E E]
[is_scalar_tower R F F]
(f : E ≃* F)
(x : E) :
def
lmul
{R : Type u_1}
{H₁ : Type u_2}
[comm_semiring R]
[non_unital_non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁] :
theorem
lmul_apply
{R : Type u_1}
{H₁ : Type u_2}
[comm_semiring R]
[non_unital_non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
(x y : H₁) :
theorem
lmul_eq_mul
{R : Type u_1}
{H₁ : Type u_2}
[comm_semiring R]
[non_unital_non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
(x : H₁) :
⇑lmul x = linear_map.mul_left R x
theorem
lmul_eq_alg_lmul
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[semiring H₁]
[algebra R H₁]
(x : H₁) :
⇑lmul x = ⇑(algebra.lmul R H₁) x
theorem
lmul_one
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁] :
def
rmul
{R : Type u_1}
{H₂ : Type u_3}
[comm_semiring R]
[non_unital_non_assoc_semiring H₂]
[module R H₂]
[smul_comm_class R H₂ H₂]
[is_scalar_tower R H₂ H₂] :
theorem
rmul_apply
{R : Type u_1}
{H₂ : Type u_3}
[comm_semiring R]
[non_unital_non_assoc_semiring H₂]
[module R H₂]
[smul_comm_class R H₂ H₂]
[is_scalar_tower R H₂ H₂]
(x y : H₂) :
theorem
rmul_eq_mul
{R : Type u_1}
{H₂ : Type u_3}
[comm_semiring R]
[non_unital_non_assoc_semiring H₂]
[module R H₂]
[smul_comm_class R H₂ H₂]
[is_scalar_tower R H₂ H₂]
(x : H₂) :
⇑rmul x = linear_map.mul_right R x
theorem
rmul_one
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁] :
def
rmul_map_lmul
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[non_unital_non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
[non_unital_non_assoc_semiring H₂]
[module R H₂]
[smul_comm_class R H₂ H₂]
[is_scalar_tower R H₂ H₂] :
tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂ →ₗ[R] tensor_product R H₁ H₂
Equations
- rmul_map_lmul = (tensor_product.hom_tensor_hom_map R H₁ H₂ H₁ H₂).comp (tensor_product.map rmul lmul)
theorem
rmul_map_lmul_apply
{R : Type u_1}
{H₁ : Type u_2}
{H₂ : Type u_3}
[comm_semiring R]
[non_unital_non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
[non_unital_non_assoc_semiring H₂]
[module R H₂]
[smul_comm_class R H₂ H₂]
[is_scalar_tower R H₂ H₂]
(x : H₁)
(y : H₂) :
⇑rmul_map_lmul (x ⊗ₜ[R] y) = tensor_product.map (⇑rmul x) (⇑lmul y)
theorem
rmul_map_lmul_one
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
{H₂ : Type u_3}
[non_assoc_semiring H₂]
[module R H₂]
[smul_comm_class R H₂ H₂]
[is_scalar_tower R H₂ H₂] :
⇑rmul_map_lmul (1 ⊗ₜ[R] 1) = 1
theorem
linear_map.mul_left_sum
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[non_unital_non_assoc_semiring A]
[module R A]
[smul_comm_class R A A]
[is_scalar_tower R A A]
{n : Type u_3}
{s : finset n}
{x : n → A} :
s.sum (λ (i : n), linear_map.mul_left R (x i)) = linear_map.mul_left R (s.sum (λ (i : n), x i))
theorem
linear_map.mul_right_sum
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[non_unital_non_assoc_semiring A]
[module R A]
[smul_comm_class R A A]
[is_scalar_tower R A A]
{n : Type u_3}
{s : finset n}
{x : n → A} :
s.sum (λ (i : n), linear_map.mul_right R (x i)) = linear_map.mul_right R (s.sum (λ (i : n), x i))
theorem
lmul_eq_one_iff
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
(x : H₁) :
theorem
linear_map.mul_left_eq_one_iff
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
(x : H₁) :
linear_map.mul_left R x = 1 ↔ x = 1
theorem
rmul_eq_one_iff
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
(x : H₁) :
theorem
linear_map.mul_right_eq_one_iff
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
(x : H₁) :
linear_map.mul_right R x = 1 ↔ x = 1
theorem
linear_map.mul_left_eq_one_or_zero_iff_mul_right_tfae
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[semiring H₁]
[algebra R H₁]
(x : H₁)
(p : Prop)
[decidable p] :
[linear_map.mul_left R x = ite p 1 0, linear_map.mul_right R x = ite p 1 0, x = ite p 1 0].tfae
theorem
linear_map.mul_left_eq_one_or_zero_iff_mul_right
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[semiring H₁]
[algebra R H₁]
(x : H₁)
(p : Prop)
[decidable p] :
linear_map.mul_left R x = ite p 1 0 ↔ linear_map.mul_right R x = ite p 1 0
theorem
linear_map.mul_right_smul
{R : Type u_1}
{H₁ : Type u_2}
[comm_semiring R]
[non_unital_non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
(x : H₁)
(α : R) :
linear_map.mul_right R (α • x) = α • linear_map.mul_right R x
theorem
linear_map.mul_left_smul
{R : Type u_1}
{H₁ : Type u_2}
[comm_semiring R]
[non_unital_non_assoc_semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
(x : H₁)
(α : R) :
linear_map.mul_left R (α • x) = α • linear_map.mul_left R x
theorem
linear_map.mul_left_comp_inj
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
{H₂ : Type u_3}
[semiring H₁]
[module R H₁]
[add_comm_monoid H₂]
[module R H₂]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
(f g : H₁ →ₗ[R] H₂)
(x : H₁)
[invertible x] :
f.comp (linear_map.mul_left R x) = g.comp (linear_map.mul_left R x) ↔ f = g
theorem
linear_map.mul_left_inj
{R : Type u_1}
[comm_semiring R]
{H₁ : Type u_2}
[semiring H₁]
[module R H₁]
[smul_comm_class R H₁ H₁]
[is_scalar_tower R H₁ H₁]
(x : H₁)
[invertible x]
(y z : H₁) :
⇑(linear_map.mul_left R x) y = ⇑(linear_map.mul_left R x) z ↔ y = z