mathlib documentation

algebra.algebra.bilinear

Facts about algebras involving bilinear maps and tensor products #

We move a few basic statements about algebras out of algebra.algebra.basic, in order to avoid importing linear_algebra.bilinear_map and linear_algebra.tensor_product unnecessarily.

source
def algebra.lmul (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R A] :
A →ₐ[R] module.End R A

The multiplication in an algebra is a bilinear map.

A weaker version of this for semirings exists as add_monoid_hom.mul.

Equations
source
@[simp]
theorem algebra.lmul_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (p q : A) :
⇑(⇑(algebra.lmul R A) p) q = p * q
source
def algebra.lmul_left (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (r : A) :
A →ₗ[R] A

The multiplication on the left in an algebra is a linear map.

Equations
source
@[simp]
theorem algebra.lmul_left_to_add_monoid_hom (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (r : A) :
↑(algebra.lmul_left R r) = add_monoid_hom.mul_left r
source
def algebra.lmul_right (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (r : A) :
A →ₗ[R] A

The multiplication on the right in an algebra is a linear map.

Equations
source
@[simp]
theorem algebra.lmul_right_to_add_monoid_hom (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (r : A) :
↑(algebra.lmul_right R r) = add_monoid_hom.mul_right r
source
def algebra.lmul_left_right (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (vw : A × A) :
A →ₗ[R] A

Simultaneous multiplication on the left and right is a linear map.

Equations
source
theorem algebra.commute_lmul_left_right (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a b : A) :
commute (algebra.lmul_left R a) (algebra.lmul_right R b)
source
def algebra.lmul' (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
A ⊗ A →ₗ[R] A

The multiplication map on an algebra, as an R-linear map from A ⊗[R] A to A.

Equations
source
@[simp]
theorem algebra.lmul'_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] {x y : A} :
⇑(algebra.lmul' R) (x ⊗ₜ[R] y) = x * y
source
@[simp]
theorem algebra.lmul_left_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (p q : A) :
⇑(algebra.lmul_left R p) q = p * q
source
@[simp]
theorem algebra.lmul_right_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (p q : A) :
⇑(algebra.lmul_right R p) q = q * p
source
@[simp]
theorem algebra.lmul_left_right_apply {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (vw : A × A) (p : A) :
⇑(algebra.lmul_left_right R vw) p = ((vw.fst) * p) * vw.snd
source
@[simp]
theorem algebra.lmul_left_one {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
algebra.lmul_left R 1 = linear_map.id
source
@[simp]
theorem algebra.lmul_left_mul {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a b : A) :
algebra.lmul_left R (a * b) = (algebra.lmul_left R a).comp (algebra.lmul_left R b)
source
@[simp]
theorem algebra.lmul_right_one {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
algebra.lmul_right R 1 = linear_map.id
source
@[simp]
theorem algebra.lmul_right_mul {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a b : A) :
algebra.lmul_right R (a * b) = (algebra.lmul_right R b).comp (algebra.lmul_right R a)
source
@[simp]
theorem algebra.lmul_left_zero_eq_zero {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
algebra.lmul_left R 0 = 0
source
@[simp]
theorem algebra.lmul_right_zero_eq_zero {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
algebra.lmul_right R 0 = 0
source
@[simp]
theorem algebra.lmul_left_eq_zero_iff {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
algebra.lmul_left R a = 0 ↔ a = 0
source
@[simp]
theorem algebra.lmul_right_eq_zero_iff {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
algebra.lmul_right R a = 0 ↔ a = 0
source
@[simp]
theorem algebra.pow_lmul_left {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a : A) (n : ℕ) :
algebra.lmul_left R a ^ n = algebra.lmul_left R (a ^ n)
source
@[simp]
theorem algebra.pow_lmul_right {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (a : A) (n : ℕ) :
algebra.lmul_right R a ^ n = algebra.lmul_right R (a ^ n)
source
theorem algebra.lmul_left_injective {R : Type u_1} {A : Type u_2} [comm_semiring R] [ring A] [algebra R A] [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
function.injective ⇑(algebra.lmul_left R x)
source
theorem algebra.lmul_right_injective {R : Type u_1} {A : Type u_2} [comm_semiring R] [ring A] [algebra R A] [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
function.injective ⇑(algebra.lmul_right R x)
source
theorem algebra.lmul_injective {R : Type u_1} {A : Type u_2} [comm_semiring R] [ring A] [algebra R A] [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
function.injective ⇑(⇑(algebra.lmul R A) x)