mathlib documentation

linear_algebra.bilinear_map

Basics on bilinear maps #

This file provides basics on bilinear maps. The most general form considered are maps that are semilinear in both arguments. They are of type M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P, where M and N are modules over R and S respectively, P is a module over both R₂ and S₂ with commuting actions, and ρ₁₂ : R →+* R₂ and σ₁₂ : S →+* S₂.

Main declarations #

Tags #

bilinear

def linear_map.mk₂'ₛₗ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] (ρ₁₂ : R →+* R₂) (σ₁₂ : S →+* S₂) (f : M N P) (H1 : (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n) (H2 : (c : R) (m : M) (n : N), f (c m) n = ρ₁₂ c f m n) (H3 : (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂) (H4 : (c : S) (m : M) (n : N), f m (c n) = σ₁₂ c f m n) :
M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P

Create a bilinear map from a function that is semilinear in each component. See mk₂' and mk₂ for the linear case.

Equations
@[simp]
theorem linear_map.mk₂'ₛₗ_apply {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M N P) {H1 : (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n} {H2 : (c : R) (m : M) (n : N), f (c m) n = ρ₁₂ c f m n} {H3 : (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂} {H4 : (c : S) (m : M) (n : N), f m (c n) = σ₁₂ c f m n} (m : M) (n : N) :
((linear_map.mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4) m) n = f m n
def linear_map.mk₂' (R : Type u_3) [semiring R] (S : Type u_4) [semiring S] {M : Type u_7} {N : Type u_8} {Pₗ : Type u_14} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid Pₗ] [module R M] [module S N] [module R Pₗ] [module S Pₗ] [smul_comm_class S R Pₗ] (f : M N Pₗ) (H1 : (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n) (H2 : (c : R) (m : M) (n : N), f (c m) n = c f m n) (H3 : (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂) (H4 : (c : S) (m : M) (n : N), f m (c n) = c f m n) :
M →ₗ[R] N →ₗ[S] Pₗ

Create a bilinear map from a function that is linear in each component. See mk₂ for the special case where both arguments come from modules over the same ring.

Equations
@[simp]
theorem linear_map.mk₂'_apply {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {M : Type u_7} {N : Type u_8} {Pₗ : Type u_14} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid Pₗ] [module R M] [module S N] [module R Pₗ] [module S Pₗ] [smul_comm_class S R Pₗ] (f : M N Pₗ) {H1 : (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n} {H2 : (c : R) (m : M) (n : N), f (c m) n = c f m n} {H3 : (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂} {H4 : (c : S) (m : M) (n : N), f m (c n) = c f m n} (m : M) (n : N) :
((linear_map.mk₂' R S f H1 H2 H3 H4) m) n = f m n
theorem linear_map.ext₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : (m : M) (n : N), (f m) n = (g m) n) :
f = g
theorem linear_map.congr_fun₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : f = g) (x : M) (y : N) :
(f x) y = (g x) y
def linear_map.flip {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) :
N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P

Given a linear map from M to linear maps from N to P, i.e., a bilinear map from M × N to P, change the order of variables and get a linear map from N to linear maps from M to P.

Equations
@[simp]
theorem linear_map.flip_apply {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (m : M) (n : N) :
((f.flip) n) m = (f m) n
@[simp]
theorem linear_map.flip_flip {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} [smul_comm_class R₂ S₂ P] (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) :
f.flip.flip = f
theorem linear_map.flip_inj {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : f.flip = g.flip) :
f = g
theorem linear_map.map_zero₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (y : N) :
(f 0) y = 0
theorem linear_map.map_neg₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {N : Type u_8} {M' : Type u_15} {P' : Type u_17} [add_comm_monoid N] [add_comm_group M'] [add_comm_group P'] [module S N] [module R M'] [module R₂ P'] [module S₂ P'] [smul_comm_class S₂ R₂ P'] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x : M') (y : N) :
(f (-x)) y = -(f x) y
theorem linear_map.map_sub₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {N : Type u_8} {M' : Type u_15} {P' : Type u_17} [add_comm_monoid N] [add_comm_group M'] [add_comm_group P'] [module S N] [module R M'] [module R₂ P'] [module S₂ P'] [smul_comm_class S₂ R₂ P'] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y : M') (z : N) :
(f (x - y)) z = (f x) z - (f y) z
theorem linear_map.map_add₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (x₁ x₂ : M) (y : N) :
(f (x₁ + x₂)) y = (f x₁) y + (f x₂) y
theorem linear_map.map_smul₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {S₂ : Type u_6} [semiring S₂] {M₂ : Type u_10} {N₂ : Type u_11} {P₂ : Type u_12} [add_comm_monoid M₂] [add_comm_monoid N₂] [add_comm_monoid P₂] [module R M₂] [module S N₂] [module R P₂] [module S₂ P₂] [smul_comm_class S₂ R P₂] {σ₁₂ : S →+* S₂} (f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂) (r : R) (x : M₂) (y : N₂) :
(f (r x)) y = r (f x) y
theorem linear_map.map_smulₛₗ₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (r : R) (x : M) (y : N) :
(f (r x)) y = ρ₁₂ r (f x) y
theorem linear_map.map_sum₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {ι : Type u_1} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (t : finset ι) (x : ι M) (y : N) :
(f (t.sum (λ (i : ι), x i))) y = t.sum (λ (i : ι), (f (x i)) y)
def linear_map.dom_restrict₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : submodule S N) :
M →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P

Restricting a bilinear map in the second entry

Equations
theorem linear_map.dom_restrict₂_apply {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : submodule S N) (x : M) (y : q) :
((f.dom_restrict₂ q) x) y = (f x) y
def linear_map.dom_restrict₁₂ {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : submodule R M) (q : submodule S N) :
p →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P

Restricting a bilinear map in both components

Equations
theorem linear_map.dom_restrict₁₂_apply {R : Type u_3} [semiring R] {S : Type u_4} [semiring S] {R₂ : Type u_5} [semiring R₂] {S₂ : Type u_6} [semiring S₂] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : submodule R M) (q : submodule S N) (x : p) (y : q) :
def linear_map.mk₂ (R : Type u_3) [comm_semiring R] {M : Type u_7} {Nₗ : Type u_12} {Pₗ : Type u_13} [add_comm_monoid M] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [module R M] [module R Nₗ] [module R Pₗ] (f : M Nₗ Pₗ) (H1 : (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n) (H2 : (c : R) (m : M) (n : Nₗ), f (c m) n = c f m n) (H3 : (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂) (H4 : (c : R) (m : M) (n : Nₗ), f m (c n) = c f m n) :
M →ₗ[R] Nₗ →ₗ[R] Pₗ

Create a bilinear map from a function that is linear in each component.

This is a shorthand for mk₂' for the common case when R = S.

Equations
@[simp]
theorem linear_map.mk₂_apply (R : Type u_3) [comm_semiring R] {M : Type u_7} {Nₗ : Type u_12} {Pₗ : Type u_13} [add_comm_monoid M] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [module R M] [module R Nₗ] [module R Pₗ] (f : M Nₗ Pₗ) {H1 : (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n} {H2 : (c : R) (m : M) (n : Nₗ), f (c m) n = c f m n} {H3 : (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂} {H4 : (c : R) (m : M) (n : Nₗ), f m (c n) = c f m n} (m : M) (n : Nₗ) :
((linear_map.mk₂ R f H1 H2 H3 H4) m) n = f m n
def linear_map.lflip (R : Type u_3) [comm_semiring R] {R₂ : Type u_4} [comm_semiring R₂] {R₃ : Type u_5} [comm_semiring R₃] (M : Type u_7) (N : Type u_8) (P : Type u_9) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R₂ N] [module R₃ P] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} :
(M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) →ₗ[R₃] N →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P

Given a linear map from M to linear maps from N to P, i.e., a bilinear map M → N → P, change the order of variables and get a linear map from N to linear maps from M to P.

Equations
@[simp]
theorem linear_map.lflip_apply {R : Type u_3} [comm_semiring R] {R₂ : Type u_4} [comm_semiring R₂] {R₃ : Type u_5} [comm_semiring R₃] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R₂ N] [module R₃ P] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (m : M) (n : N) :
(((linear_map.lflip R M N P) f) n) m = (f m) n
def linear_map.lcomp (R : Type u_3) [comm_semiring R] {M : Type u_7} {Nₗ : Type u_12} (Pₗ : Type u_13) [add_comm_monoid M] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [module R M] [module R Nₗ] [module R Pₗ] (f : M →ₗ[R] Nₗ) :
(Nₗ →ₗ[R] Pₗ) →ₗ[R] M →ₗ[R] Pₗ

Composing a linear map M → N and a linear map N → P to form a linear map M → P.

Equations
@[simp]
theorem linear_map.lcomp_apply {R : Type u_3} [comm_semiring R] {M : Type u_7} {Nₗ : Type u_12} {Pₗ : Type u_13} [add_comm_monoid M] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [module R M] [module R Nₗ] [module R Pₗ] (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) (x : M) :
((linear_map.lcomp R Pₗ f) g) x = g (f x)
theorem linear_map.lcomp_apply' {R : Type u_3} [comm_semiring R] {M : Type u_7} {Nₗ : Type u_12} {Pₗ : Type u_13} [add_comm_monoid M] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [module R M] [module R Nₗ] [module R Pₗ] (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) :
(linear_map.lcomp R Pₗ f) g = g.comp f
def linear_map.lcompₛₗ {R : Type u_3} [comm_semiring R] {R₂ : Type u_4} [comm_semiring R₂] {R₃ : Type u_5} [comm_semiring R₃] {M : Type u_7} {N : Type u_8} (P : Type u_9) [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R₂ N] [module R₃ P] {σ₁₂ : R →+* R₂} (σ₂₃ : R₂ →+* R₃) {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N) :
(N →ₛₗ[σ₂₃] P) →ₗ[R₃] M →ₛₗ[σ₁₃] P

Composing a semilinear map M → N and a semilinear map N → P to form a semilinear map M → P is itself a linear map.

Equations
@[simp]
theorem linear_map.lcompₛₗ_apply {R : Type u_3} [comm_semiring R] {R₂ : Type u_4} [comm_semiring R₂] {R₃ : Type u_5} [comm_semiring R₃] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R₂ N] [module R₃ P] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N) (g : N →ₛₗ[σ₂₃] P) (x : M) :
((linear_map.lcompₛₗ P σ₂₃ f) g) x = g (f x)
def linear_map.llcomp (R : Type u_3) [comm_semiring R] (M : Type u_7) (Nₗ : Type u_12) (Pₗ : Type u_13) [add_comm_monoid M] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [module R M] [module R Nₗ] [module R Pₗ] :
(Nₗ →ₗ[R] Pₗ) →ₗ[R] (M →ₗ[R] Nₗ) →ₗ[R] M →ₗ[R] Pₗ

Composing a linear map M → N and a linear map N → P to form a linear map M → P.

Equations
@[simp]
theorem linear_map.llcomp_apply {R : Type u_3} [comm_semiring R] {M : Type u_7} {Nₗ : Type u_12} {Pₗ : Type u_13} [add_comm_monoid M] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [module R M] [module R Nₗ] [module R Pₗ] (f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) (x : M) :
(((linear_map.llcomp R M Nₗ Pₗ) f) g) x = f (g x)
theorem linear_map.llcomp_apply' {R : Type u_3} [comm_semiring R] {M : Type u_7} {Nₗ : Type u_12} {Pₗ : Type u_13} [add_comm_monoid M] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [module R M] [module R Nₗ] [module R Pₗ] (f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) :
((linear_map.llcomp R M Nₗ Pₗ) f) g = f.comp g
def linear_map.compl₂ {R : Type u_3} [comm_semiring R] {R₂ : Type u_4} [comm_semiring R₂] {R₃ : Type u_5} [comm_semiring R₃] {R₄ : Type u_6} [comm_semiring R₄] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R₂ N] [module R₃ P] [module R₄ Q] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃} [ring_hom_comp_triple σ₄₂ σ₂₃ σ₄₃] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) :
M →ₛₗ[σ₁₃] Q →ₛₗ[σ₄₃] P

Composing a linear map Q → N and a bilinear map M → N → P to form a bilinear map M → Q → P.

Equations
@[simp]
theorem linear_map.compl₂_apply {R : Type u_3} [comm_semiring R] {R₂ : Type u_4} [comm_semiring R₂] {R₃ : Type u_5} [comm_semiring R₃] {R₄ : Type u_6} [comm_semiring R₄] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R₂ N] [module R₃ P] [module R₄ Q] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃} [ring_hom_comp_triple σ₄₂ σ₂₃ σ₄₃] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) (m : M) (q : Q) :
((f.compl₂ g) m) q = (f m) (g q)
@[simp]
theorem linear_map.compl₂_id {R : Type u_3} [comm_semiring R] {R₂ : Type u_4} [comm_semiring R₂] {R₃ : Type u_5} [comm_semiring R₃] {M : Type u_7} {N : Type u_8} {P : Type u_9} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R₂ N] [module R₃ P] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) :
def linear_map.compl₁₂ {R : Type u_3} [comm_semiring R] {Mₗ : Type u_11} {Nₗ : Type u_12} {Pₗ : Type u_13} {Qₗ : Type u_14} {Qₗ' : Type u_15} [add_comm_monoid Mₗ] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [add_comm_monoid Qₗ] [add_comm_monoid Qₗ'] [module R Mₗ] [module R Nₗ] [module R Pₗ] [module R Qₗ] [module R Qₗ'] (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ) :
Qₗ →ₗ[R] Qₗ' →ₗ[R] Pₗ

Composing linear maps Q → M and Q' → N with a bilinear map M → N → P to form a bilinear map Q → Q' → P.

Equations
@[simp]
theorem linear_map.compl₁₂_apply {R : Type u_3} [comm_semiring R] {Mₗ : Type u_11} {Nₗ : Type u_12} {Pₗ : Type u_13} {Qₗ : Type u_14} {Qₗ' : Type u_15} [add_comm_monoid Mₗ] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [add_comm_monoid Qₗ] [add_comm_monoid Qₗ'] [module R Mₗ] [module R Nₗ] [module R Pₗ] [module R Qₗ] [module R Qₗ'] (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ) (x : Qₗ) (y : Qₗ') :
((f.compl₁₂ g g') x) y = (f (g x)) (g' y)
@[simp]
theorem linear_map.compl₁₂_id_id {R : Type u_3} [comm_semiring R] {Mₗ : Type u_11} {Nₗ : Type u_12} {Pₗ : Type u_13} [add_comm_monoid Mₗ] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [module R Mₗ] [module R Nₗ] [module R Pₗ] (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) :
theorem linear_map.compl₁₂_inj {R : Type u_3} [comm_semiring R] {Mₗ : Type u_11} {Nₗ : Type u_12} {Pₗ : Type u_13} {Qₗ : Type u_14} {Qₗ' : Type u_15} [add_comm_monoid Mₗ] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [add_comm_monoid Qₗ] [add_comm_monoid Qₗ'] [module R Mₗ] [module R Nₗ] [module R Pₗ] [module R Qₗ] [module R Qₗ'] {f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} {g : Qₗ →ₗ[R] Mₗ} {g' : Qₗ' →ₗ[R] Nₗ} (hₗ : function.surjective g) (hᵣ : function.surjective g') :
f₁.compl₁₂ g g' = f₂.compl₁₂ g g' f₁ = f₂
def linear_map.compr₂ {R : Type u_3} [comm_semiring R] {M : Type u_7} {Nₗ : Type u_12} {Pₗ : Type u_13} {Qₗ : Type u_14} [add_comm_monoid M] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [add_comm_monoid Qₗ] [module R M] [module R Nₗ] [module R Pₗ] [module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) :
M →ₗ[R] Nₗ →ₗ[R] Qₗ

Composing a linear map P → Q and a bilinear map M → N → P to form a bilinear map M → N → Q.

Equations
@[simp]
theorem linear_map.compr₂_apply {R : Type u_3} [comm_semiring R] {M : Type u_7} {Nₗ : Type u_12} {Pₗ : Type u_13} {Qₗ : Type u_14} [add_comm_monoid M] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [add_comm_monoid Qₗ] [module R M] [module R Nₗ] [module R Pₗ] [module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (m : M) (n : Nₗ) :
((f.compr₂ g) m) n = g ((f m) n)
def linear_map.lsmul (R : Type u_3) [comm_semiring R] (M : Type u_7) [add_comm_monoid M] [module R M] :

Scalar multiplication as a bilinear map R → M → M.

Equations
@[simp]
theorem linear_map.lsmul_apply {R : Type u_3} [comm_semiring R] {M : Type u_7} [add_comm_monoid M] [module R M] (r : R) (m : M) :
((linear_map.lsmul R M) r) m = r m
theorem linear_map.ext_basis {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {R₂ : Type u_4} {S : Type u_5} {S₂ : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [comm_ring R] [comm_ring S] [comm_ring R₂] [comm_ring S₂] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : basis ι₁ R M) (b₂ : basis ι₂ S N) {B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : (i : ι₁) (j : ι₂), (B (b₁ i)) (b₂ j) = (B' (b₁ i)) (b₂ j)) :
B = B'

Two bilinear maps are equal when they are equal on all basis vectors.

theorem linear_map.sum_repr_mul_repr_mulₛₗ {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {R₂ : Type u_4} {S : Type u_5} {S₂ : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [comm_ring R] [comm_ring S] [comm_ring R₂] [comm_ring S₂] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module S N] [module R₂ P] [module S₂ P] [smul_comm_class S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : basis ι₁ R M) (b₂ : basis ι₂ S N) {B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (x : M) (y : N) :
((b₁.repr) x).sum (λ (i : ι₁) (xi : R), ((b₂.repr) y).sum (λ (j : ι₂) (yj : S), ρ₁₂ xi σ₁₂ yj (B (b₁ i)) (b₂ j))) = (B x) y

Write out B x y as a sum over B (b i) (b j) if b is a basis.

Version for semi-bilinear maps, see sum_repr_mul_repr_mul for the bilinear version.

theorem linear_map.sum_repr_mul_repr_mul {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {Mₗ : Type u_10} {Nₗ : Type u_11} {Pₗ : Type u_12} [comm_ring R] [add_comm_monoid Mₗ] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [module R Mₗ] [module R Nₗ] [module R Pₗ] (b₁' : basis ι₁ R Mₗ) (b₂' : basis ι₂ R Nₗ) {B : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} (x : Mₗ) (y : Nₗ) :
((b₁'.repr) x).sum (λ (i : ι₁) (xi : R), ((b₂'.repr) y).sum (λ (j : ι₂) (yj : R), xi yj (B (b₁' i)) (b₂' j))) = (B x) y

Write out B x y as a sum over B (b i) (b j) if b is a basis.

Version for bilinear maps, see sum_repr_mul_repr_mulₛₗ for the semi-bilinear version.

theorem linear_map.lsmul_injective {R : Type u_3} {M : Type u_7} [comm_ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {x : R} (hx : x 0) :
theorem linear_map.ker_lsmul {R : Type u_3} {M : Type u_7} [comm_ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {a : R} (ha : a 0) :