# mathlibdocumentation

linear_algebra.bilinear_map

# Basics on bilinear maps #

This file provides basics on bilinear maps.

## Main declarations #

• linear_map.mk₂: a constructor for bilinear maps, taking an unbundled function together with proof witnesses of bilinearity
• linear_map.flip: turns a bilinear map M × N → P into N × M → P
• linear_map.lcomp and linear_map.llcomp: composition of linear maps as a bilinear map
• linear_map.compl₂: composition of a bilinear map M × N → P with a linear map Q → M
• linear_map.compr₂: composition of a bilinear map M × N → P with a linear map Q → N
• linear_map.lsmul: scalar multiplication as a bilinear map R × M → M

## Tags #

bilinear

def linear_map.mk₂' (R : Type u_1) [semiring R] (S : Type u_2) [semiring S] {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] [ P] [ 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) :

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_1} [semiring R] {S : Type u_2} [semiring S] {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] [ P] [ 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) :
( S f H1 H2 H3 H4) m) n = f m n
theorem linear_map.ext₂ {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] [ P] [ P] {f g : M →ₗ[R] N →ₗ[S] P} (H : ∀ (m : M) (n : N), (f m) n = (g m) n) :
f = g
def linear_map.flip {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] [ P] [ P] (f : M →ₗ[R] N →ₗ[S] 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_1} [semiring R] {S : Type u_2} [semiring S] {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] [ P] [ P] (f : M →ₗ[R] N →ₗ[S] P) (m : M) (n : N) :
((f.flip) n) m = (f m) n
theorem linear_map.flip_inj {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] [ P] [ P] {f g : M →ₗ[R] N →ₗ[S] P} (H : f.flip = g.flip) :
f = g
theorem linear_map.map_zero₂ {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] [ P] [ P] (f : M →ₗ[R] N →ₗ[S] P) (y : N) :
(f 0) y = 0
theorem linear_map.map_neg₂ {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] {N : Type u_4} {M' : Type u_6} {P' : Type u_8} [add_comm_group M'] [add_comm_group P'] [ N] [ M'] [ P'] [ P'] [ P'] (f : M' →ₗ[R] N →ₗ[S] P') (x : M') (y : N) :
(f (-x)) y = -(f x) y
theorem linear_map.map_sub₂ {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] {N : Type u_4} {M' : Type u_6} {P' : Type u_8} [add_comm_group M'] [add_comm_group P'] [ N] [ M'] [ P'] [ P'] [ P'] (f : M' →ₗ[R] N →ₗ[S] P') (x y : M') (z : N) :
(f (x - y)) z = (f x) z - (f y) z
theorem linear_map.map_add₂ {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] [ P] [ P] (f : M →ₗ[R] N →ₗ[S] P) (x₁ x₂ : M) (y : N) :
(f (x₁ + x₂)) y = (f x₁) y + (f x₂) y
theorem linear_map.map_smul₂ {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] [ P] [ P] (f : M →ₗ[R] N →ₗ[S] P) (r : R) (x : M) (y : N) :
(f (r x)) y = r (f x) y
theorem linear_map.map_sum₂ {R : Type u_1} [semiring R] {S : Type u_2} [semiring S] {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] [ P] [ P] {ι : Type u_6} (f : M →ₗ[R] N →ₗ[S] P) (t : finset ι) (x : ι → M) (y : N) :
(f (∑ (i : ι) in t, x i)) y = ∑ (i : ι) in t, (f (x i)) y
def linear_map.mk₂ (R : Type u_1) {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ 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) :

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
• H1 H2 H3 H4 = f H1 H2 H3 H4
@[simp]
theorem linear_map.mk₂_apply (R : Type u_1) {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ 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) :
( f H1 H2 H3 H4) m) n = f m n
def linear_map.lflip (R : Type u_1) (M : Type u_2) (N : Type u_3) (P : Type u_4) [ M] [ N] [ 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_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
(( M N P) f) n) m = (f m) n
def linear_map.lcomp (R : Type u_1) {M : Type u_2} {N : Type u_3} (P : Type u_4) [ M] [ N] [ P] (f : M →ₗ[R] N) :

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_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (x : M) :
( P f) g) x = g (f x)
def linear_map.llcomp (R : Type u_1) (M : Type u_2) (N : Type u_3) (P : Type u_4) [ M] [ N] [ 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_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : N →ₗ[R] P) (g : M →ₗ[R] N) (x : M) :
(( N P) f) g) x = f (g x)
def linear_map.compl₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_5} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] N →ₗ[R] P) (g : Q →ₗ[R] N) :

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_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_5} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] N →ₗ[R] P) (g : Q →ₗ[R] N) (m : M) (q : Q) :
((f.compl₂ g) m) q = (f m) (g q)
def linear_map.compr₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_5} [ M] [ N] [ P] [ Q] (f : M →ₗ[R] N →ₗ[R] P) (g : P →ₗ[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_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_5} [ M] [ N] [ P] [ 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_1) (M : Type u_2) [ M] :

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

Equations
• = _ _
@[simp]
theorem linear_map.lsmul_apply {R : Type u_1} {M : Type u_2} [ M] (r : R) (m : M) :
( M) r) m = r m
theorem linear_map.lsmul_injective {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {x : R} (hx : x 0) :
theorem linear_map.ker_lsmul {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {a : R} (ha : a 0) :
( M) a).ker =