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

• LinearMap.mk₂: a constructor for bilinear maps, taking an unbundled function together with proof witnesses of bilinearity
• LinearMap.flip: turns a bilinear map M × N → P into N × M → P
• LinearMap.lflip: given a linear map from M to N →ₗ[R] P, i.e., a bilinear map M → N → P, change the order of variables and get a linear map from N to M →ₗ[R] P.
• LinearMap.lcomp: composition of a given linear map M → N with a linear map N → P as a linear map from Nₗ →ₗ[R] Pₗ to M →ₗ[R] Pₗ
• LinearMap.llcomp: composition of linear maps as a bilinear map from (M →ₗ[R] N) × (N →ₗ[R] P) to M →ₗ[R] P
• LinearMap.compl₂: composition of a linear map Q → N and a bilinear map M → N → P to form a bilinear map M → Q → P.
• LinearMap.compr₂: composition of a linear map P → Q and a bilinear map M → N → P to form a bilinear map M → N → Q.
• LinearMap.lsmul: scalar multiplication as a bilinear map R × M → M

Tags

bilinear

def LinearMap.mk₂'ₛₗ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass 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

• LinearMap.mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4 = { toFun := fun (m : M) => { toFun := f m, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.mk₂'ₛₗ_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass 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) : ((mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4) m) n = f m n

def LinearMap.mk₂' (R : Type u_1) [Semiring R] (S : Type u_2) [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass 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

• LinearMap.mk₂' R S f H1 H2 H3 H4 = LinearMap.mk₂'ₛₗ (RingHom.id R) (RingHom.id S) f H1 H2 H3 H4

@[simp]

theorem LinearMap.mk₂'_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass 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) : ((mk₂' R S f H1 H2 H3 H4) m) n = f m n

theorem LinearMap.ext₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass 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 LinearMap.congr_fun₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass 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

theorem LinearMap.ext_iff₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} : f = g ↔ ∀ (m : M) (n : N), (f m) n = (g m) n

def LinearMap.flip {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass 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

• f.flip = LinearMap.mk₂'ₛₗ σ₁₂ ρ₁₂ (fun (n : N) (m : M) => (f m) n) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem LinearMap.flip_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (m : M) (n : N) : (f.flip n) m = (f m) n

def LinearMap.lcompₛₗ {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} (R₅ : Type u_18) {M : Type u_19} {N : Type u_20} (P : Type u_21) [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring R₅] {σ₁₂ : R →+* R₂} (σ₂₃ : R₂ →+* R₃) {σ₁₃ : R →+* R₃} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₅ P] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [SMulCommClass R₃ R₅ P] (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

• LinearMap.lcompₛₗ R₅ P σ₂₃ f = (LinearMap.id.flip ∘ₛₗ f).flip

@[simp]

theorem LinearMap.lcompₛₗ_apply {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} {R₅ : Type u_18} {M : Type u_19} {N : Type u_20} {P : Type u_21} [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring R₅] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₅ P] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [SMulCommClass R₃ R₅ P] (f : M →ₛₗ[σ₁₂] N) (g : N →ₛₗ[σ₂₃] P) (x : M) : ((lcompₛₗ R₅ P σ₂₃ f) g) x = g (f x)

def LinearMap.compl₂ {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {R₅ : Type u_18} {M : Type u_19} {N : Type u_20} {P : Type u_21} {Q : Type u_22} [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring R₄] [Semiring R₅] {σ₂₃ : R₂ →+* R₃} {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q] [Module R₅ P] [RingHomCompTriple σ₄₂ σ₂₃ σ₄₃] [SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅} (h : 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

• h.compl₂ g = { toFun := fun (a : M) => (LinearMap.lcompₛₗ R₅ P σ₂₃ g) (h a), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.compl₂_apply {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {R₅ : Type u_18} {M : Type u_19} {N : Type u_20} {P : Type u_21} {Q : Type u_22} [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring R₄] [Semiring R₅] {σ₂₃ : R₂ →+* R₃} {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q] [Module R₅ P] [RingHomCompTriple σ₄₂ σ₂₃ σ₄₃] [SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅} (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) (m : M) (q : Q) : ((h.compl₂ g) m) q = (h m) (g q)

@[simp]

theorem LinearMap.compl₂_id {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} {R₅ : Type u_18} {M : Type u_19} {N : Type u_20} {P : Type u_21} [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring R₅] {σ₂₃ : R₂ →+* R₃} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₅ P] [SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅} (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) : h.compl₂ id = h

def LinearMap.lcomp {R : Type u_1} [Semiring R] (S : Type u_2) [Semiring S] {M : Type u_5} (N : Type u_6) {M₂ : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [Module R M] [Module S N] [Module R M₂] [Module R N] [SMulCommClass R S N] (f : M →ₗ[R] M₂) : (M₂ →ₗ[R] N) →ₗ[S] M →ₗ[R] N

Composing a given linear map M → N with a linear map N → P as a linear map from Nₗ →ₗ[R] Pₗ to M →ₗ[R] Pₗ.

Equations

• LinearMap.lcomp S N f = LinearMap.lcompₛₗ S N (RingHom.id R) f

@[simp]

theorem LinearMap.lcomp_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {M₂ : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [Module R M] [Module S N] [Module R M₂] [Module R N] [SMulCommClass R S N] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] N) (x : M) : ((lcomp S N f) g) x = g (f x)

theorem LinearMap.lcomp_apply' {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {M₂ : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [Module R M] [Module S N] [Module R M₂] [Module R N] [SMulCommClass R S N] (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] N) : (lcomp S N f) g = g ∘ₗ f

@[simp]

theorem LinearMap.flip_flip {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : f.flip.flip = f

theorem LinearMap.flip_inj {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : f.flip = g.flip) : f = g

theorem LinearMap.map_zero₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (y : N) : (f 0) y = 0

theorem LinearMap.map_neg₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {N : Type u_6} {M' : Type u_12} {P' : Type u_13} [AddCommMonoid N] [AddCommGroup M'] [AddCommGroup P'] [Module S N] [Module R M'] [Module R₂ P'] [Module S₂ P'] [SMulCommClass S₂ R₂ P'] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x : M') (y : N) : (f (-x)) y = -(f x) y

theorem LinearMap.map_sub₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {N : Type u_6} {M' : Type u_12} {P' : Type u_13} [AddCommMonoid N] [AddCommGroup M'] [AddCommGroup P'] [Module S N] [Module R M'] [Module R₂ P'] [Module S₂ P'] [SMulCommClass 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 LinearMap.map_add₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass 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 LinearMap.map_smul₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {S₂ : Type u_4} [Semiring S₂] {M₂ : Type u_8} {N₂ : Type u_9} {P₂ : Type u_10} [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid P₂] [Module R M₂] [Module S N₂] [Module R P₂] [Module S₂ P₂] [SMulCommClass 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 LinearMap.map_smulₛₗ₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass 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 LinearMap.map_sum₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {ι : Type u_14} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (t : Finset ι) (x : ι → M) (y : N) : (f (∑ i ∈ t, x i)) y = ∑ i ∈ t, (f (x i)) y

def LinearMap.domRestrict₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass 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

• f.domRestrict₂ q = { toFun := fun (m : M) => (f m).domRestrict q, map_add' := ⋯, map_smul' := ⋯ }

theorem LinearMap.domRestrict₂_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : Submodule S N) (x : M) (y : ↥q) : ((f.domRestrict₂ q) x) y = (f x) ↑y

def LinearMap.domRestrict₁₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass 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

• f.domRestrict₁₂ p q = (f.domRestrict p).domRestrict₂ q

theorem LinearMap.domRestrict₁₂_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : Submodule R M) (q : Submodule S N) (x : ↥p) (y : ↥q) : ((f.domRestrict₁₂ p q) x) y = (f ↑x) ↑y

def LinearMap.restrictScalars₁₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass S R Pₗ] (R' : Type u_14) (S' : Type u_15) [Semiring R'] [Semiring S'] [Module R' M] [Module S' N] [Module R' Pₗ] [Module S' Pₗ] [SMulCommClass S' R' Pₗ] [SMul S' S] [IsScalarTower S' S N] [IsScalarTower S' S Pₗ] [SMul R' R] [IsScalarTower R' R M] [IsScalarTower R' R Pₗ] (B : M →ₗ[R] N →ₗ[S] Pₗ) : M →ₗ[R'] N →ₗ[S'] Pₗ

If B : M → N → Pₗ is R-S bilinear and R' and S' are compatible scalar multiplications, then the restriction of scalars is a R'-S' bilinear map.

Equations

• LinearMap.restrictScalars₁₂ R' S' B = LinearMap.mk₂' R' S' (fun (x1 : M) (x2 : N) => (B x1) x2) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem LinearMap.restrictScalars₁₂_apply_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass S R Pₗ] (R' : Type u_14) (S' : Type u_15) [Semiring R'] [Semiring S'] [Module R' M] [Module S' N] [Module R' Pₗ] [Module S' Pₗ] [SMulCommClass S' R' Pₗ] [SMul S' S] [IsScalarTower S' S N] [IsScalarTower S' S Pₗ] [SMul R' R] [IsScalarTower R' R M] [IsScalarTower R' R Pₗ] (B : M →ₗ[R] N →ₗ[S] Pₗ) (m : M) (x2✝ : N) : ((restrictScalars₁₂ R' S' B) m) x2✝ = (B m) x2✝

theorem LinearMap.restrictScalars₁₂_injective {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass S R Pₗ] (R' : Type u_14) (S' : Type u_15) [Semiring R'] [Semiring S'] [Module R' M] [Module S' N] [Module R' Pₗ] [Module S' Pₗ] [SMulCommClass S' R' Pₗ] [SMul S' S] [IsScalarTower S' S N] [IsScalarTower S' S Pₗ] [SMul R' R] [IsScalarTower R' R M] [IsScalarTower R' R Pₗ] : Function.Injective (restrictScalars₁₂ R' S')

@[simp]

theorem LinearMap.restrictScalars₁₂_inj {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass S R Pₗ] (R' : Type u_14) (S' : Type u_15) [Semiring R'] [Semiring S'] [Module R' M] [Module S' N] [Module R' Pₗ] [Module S' Pₗ] [SMulCommClass S' R' Pₗ] [SMul S' S] [IsScalarTower S' S N] [IsScalarTower S' S Pₗ] [SMul R' R] [IsScalarTower R' R M] [IsScalarTower R' R Pₗ] {B B' : M →ₗ[R] N →ₗ[S] Pₗ} : restrictScalars₁₂ R' S' B = restrictScalars₁₂ R' S' B' ↔ B = B'

def LinearMap.lflip {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {R₀ : Type u_14} [Semiring R₀] [Module R₀ P] [SMulCommClass S₂ R₀ P] [SMulCommClass R₂ R₀ P] : (M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) ≃ₗ[R₀] N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P

LinearMap.flip as an isomorphism of modules.

Equations

• LinearMap.lflip = { toFun := LinearMap.flip, map_add' := ⋯, map_smul' := ⋯, invFun := LinearMap.flip, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearMap.lflip_symm {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {R₀ : Type u_14} [Semiring R₀] [Module R₀ P] [SMulCommClass S₂ R₀ P] [SMulCommClass R₂ R₀ P] : lflip.symm = lflip

@[simp]

theorem LinearMap.lflip_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {R₀ : Type u_14} [Semiring R₀] [Module R₀ P] [SMulCommClass S₂ R₀ P] [SMulCommClass R₂ R₀ P] (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : lflip f = f.flip

def LinearMap.mk₂ (R : Type u_1) [CommSemiring R] {M : Type u_6} {Nₗ : Type u_11} {Pₗ : Type u_12} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid 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

• LinearMap.mk₂ R f H1 H2 H3 H4 = LinearMap.mk₂' R R f H1 H2 H3 H4

@[simp]

theorem LinearMap.mk₂_apply (R : Type u_1) [CommSemiring R] {M : Type u_6} {Nₗ : Type u_11} {Pₗ : Type u_12} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid 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ₗ) : ((mk₂ R f H1 H2 H3 H4) m) n = f m n

def LinearMap.compl₁₂ {R₁ : Type u_2} {R₂ : Type u_3} [Semiring R₁] [Semiring R₂] {N : Type u_7} {Mₗ : Type u_10} {Pₗ : Type u_12} {Qₗ : Type u_13} {Qₗ' : Type u_14} [AddCommMonoid N] [AddCommMonoid Mₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [AddCommMonoid Qₗ'] [Module R₁ Mₗ] [Module R₂ N] [Module R₁ Pₗ] [Module R₁ Qₗ] [Module R₂ Pₗ] [Module R₂ Qₗ'] [SMulCommClass R₂ R₁ Pₗ] (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

• f.compl₁₂ g g' = (f ∘ₗ g).compl₂ g'

@[simp]

theorem LinearMap.compl₁₂_apply {R₁ : Type u_2} {R₂ : Type u_3} [Semiring R₁] [Semiring R₂] {N : Type u_7} {Mₗ : Type u_10} {Pₗ : Type u_12} {Qₗ : Type u_13} {Qₗ' : Type u_14} [AddCommMonoid N] [AddCommMonoid Mₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [AddCommMonoid Qₗ'] [Module R₁ Mₗ] [Module R₂ N] [Module R₁ Pₗ] [Module R₁ Qₗ] [Module R₂ Pₗ] [Module R₂ Qₗ'] [SMulCommClass R₂ R₁ Pₗ] (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 LinearMap.compl₁₂_id_id {R₁ : Type u_2} {R₂ : Type u_3} [Semiring R₁] [Semiring R₂] {N : Type u_7} {Mₗ : Type u_10} {Pₗ : Type u_12} [AddCommMonoid N] [AddCommMonoid Mₗ] [AddCommMonoid Pₗ] [Module R₁ Mₗ] [Module R₂ N] [Module R₁ Pₗ] [Module R₂ Pₗ] [SMulCommClass R₂ R₁ Pₗ] (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) : f.compl₁₂ id id = f

theorem LinearMap.compl₁₂_inj {R₁ : Type u_2} {R₂ : Type u_3} [Semiring R₁] [Semiring R₂] {N : Type u_7} {Mₗ : Type u_10} {Pₗ : Type u_12} {Qₗ : Type u_13} {Qₗ' : Type u_14} [AddCommMonoid N] [AddCommMonoid Mₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [AddCommMonoid Qₗ'] [Module R₁ Mₗ] [Module R₂ N] [Module R₁ Pₗ] [Module R₁ Qₗ] [Module R₂ Pₗ] [Module R₂ Qₗ'] [SMulCommClass R₂ R₁ Pₗ] {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 LinearMap.compr₂ {R : Type u_1} [CommSemiring R] {A : Type u_4} [Semiring A] {M : Type u_6} {Nₗ : Type u_11} {Pₗ : Type u_12} {Qₗ : Type u_13} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] [Module A Pₗ] [SMulCommClass R A Pₗ] [Module R A] [Module A M] [Module A Qₗ] [SMulCommClass R A Qₗ] [IsScalarTower R A Qₗ] [IsScalarTower R A Pₗ] (f : M →ₗ[A] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[A] Qₗ) : M →ₗ[A] Nₗ →ₗ[R] Qₗ

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

See LinearMap.compr₂ₛₗ for a version of this which does not support towers of scalars but which does support semi-linear maps.

Equations

• f.compr₂ g = { toFun := fun (x : M) => ↑R g ∘ₗ f x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.compr₂_apply {R : Type u_1} [CommSemiring R] {A : Type u_4} [Semiring A] {M : Type u_6} {Nₗ : Type u_11} {Pₗ : Type u_12} {Qₗ : Type u_13} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] [Module A Pₗ] [SMulCommClass R A Pₗ] [Module R A] [Module A M] [Module A Qₗ] [SMulCommClass R A Qₗ] [IsScalarTower R A Qₗ] [IsScalarTower R A Pₗ] (f : M →ₗ[A] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[A] Qₗ) (m : M) (n : Nₗ) : ((f.compr₂ g) m) n = g ((f m) n)

theorem LinearMap.injective_compr₂_of_injective {R : Type u_1} [CommSemiring R] {M : Type u_6} {Nₗ : Type u_11} {Pₗ : Type u_12} {Qₗ : Type u_13} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (hf : Function.Injective ⇑f) (hg : Function.Injective ⇑g) : Function.Injective ⇑(f.compr₂ g)

A version of Function.Injective.comp for composition of a bilinear map with a linear map.

theorem LinearMap.surjective_compr₂_of_exists_rightInverse {R : Type u_1} [CommSemiring R] {M : Type u_6} {Nₗ : Type u_11} {Pₗ : Type u_12} {Qₗ : Type u_13} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (hf : Function.Surjective ⇑f) (hg : ∃ (g' : Qₗ →ₗ[R] Pₗ), g ∘ₗ g' = id) : Function.Surjective ⇑(f.compr₂ g)

A version of Function.Surjective.comp for composition of a bilinear map with a linear map.

theorem LinearMap.surjective_compr₂_of_equiv {R : Type u_1} [CommSemiring R] {M : Type u_6} {Nₗ : Type u_11} {Pₗ : Type u_12} {Qₗ : Type u_13} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ ≃ₗ[R] Qₗ) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(f.compr₂ ↑g)

A version of Function.Surjective.comp for composition of a bilinear map with a linear map.

theorem LinearMap.bijective_compr₂_of_equiv {R : Type u_1} [CommSemiring R] {M : Type u_6} {Nₗ : Type u_11} {Pₗ : Type u_12} {Qₗ : Type u_13} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ ≃ₗ[R] Qₗ) (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(f.compr₂ ↑g)

A version of Function.Bijective.comp for composition of a bilinear map with a linear map.

def LinearMap.llcomp {R : Type u_1} [CommSemiring R] {R₂ : Type u_15} (R₃ : Type u_16) (M : Type u_18) (N : Type u_19) (P : Type u_20) [CommSemiring R₂] [CommSemiring R₃] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] : (N →ₛₗ[σ₂₃] P) →ₗ[R₃] (M →ₛₗ[σ₁₂] N) →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P

Composing linear maps as a bilinear map from (M →ₛₗ[σ₁₂] N) × (N →ₛₗ[σ₂₃] P) to M →ₛₗ[σ₁₃] P.

Equations

• LinearMap.llcomp R₃ M N P = { toFun := LinearMap.lcompₛₗ R₃ P σ₂₃, map_add' := ⋯, map_smul' := ⋯ }.flip

@[simp]

theorem LinearMap.llcomp_apply {R : Type u_1} [CommSemiring R] {R₂ : Type u_15} {R₃ : Type u_16} {M : Type u_18} {N : Type u_19} {P : Type u_20} [CommSemiring R₂] [CommSemiring R₃] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : N →ₛₗ[σ₂₃] P) (g : M →ₛₗ[σ₁₂] N) (x : M) : (((llcomp R₃ M N P) f) g) x = f (g x)

theorem LinearMap.llcomp_apply' {R : Type u_1} [CommSemiring R] {R₂ : Type u_15} {R₃ : Type u_16} {M : Type u_18} {N : Type u_19} {P : Type u_20} [CommSemiring R₂] [CommSemiring R₃] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : N →ₛₗ[σ₂₃] P) (g : M →ₛₗ[σ₁₂] N) : ((llcomp R₃ M N P) f) g = f ∘ₛₗ g

def LinearMap.compr₂ₛₗ {R : Type u_1} [CommSemiring R] {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {M : Type u_18} {N : Type u_19} {P : Type u_20} {Q : Type u_21} [CommSemiring R₂] [CommSemiring R₃] [CommSemiring R₄] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : P →ₛₗ[σ₃₄] Q) : M →ₛₗ[σ₁₄] N →ₛₗ[σ₂₄] Q

Composing a linear map P →ₛₗ[σ₃₄] Q and a bilinear map M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P to form a bilinear map M →ₛₗ[σ₁₄] N →ₛₗ[σ₂₄] Q.

See LinearMap.compr₂ for a version of this definition, which does not support semi-linear maps but which does support towers of scalars.

Equations

• f.compr₂ₛₗ g = (LinearMap.llcomp R₄ N P Q) g ∘ₛₗ f

@[simp]

theorem LinearMap.compr₂ₛₗ_apply {R : Type u_1} [CommSemiring R] {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {M : Type u_18} {N : Type u_19} {P : Type u_20} {Q : Type u_21} [CommSemiring R₂] [CommSemiring R₃] [CommSemiring R₄] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : P →ₛₗ[σ₃₄] Q) (m : M) (n : N) : ((f.compr₂ₛₗ g) m) n = g ((f m) n)

theorem LinearMap.injective_compr₂ₛₗ_of_injective {R : Type u_1} [CommSemiring R] {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {M : Type u_18} {N : Type u_19} {P : Type u_20} {Q : Type u_21} [CommSemiring R₂] [CommSemiring R₃] [CommSemiring R₄] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : P →ₛₗ[σ₃₄] Q) (hf : Function.Injective ⇑f) (hg : Function.Injective ⇑g) : Function.Injective ⇑(f.compr₂ₛₗ g)

A version of Function.Injective.comp for composition of a bilinear map with a linear map.

theorem LinearMap.surjective_compr₂ₛₗ_of_exists_rightInverse {R : Type u_1} [CommSemiring R] {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {M : Type u_18} {N : Type u_19} {P : Type u_20} {Q : Type u_21} [CommSemiring R₂] [CommSemiring R₃] [CommSemiring R₄] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomInvPair σ₃₄ σ₄₃] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : P →ₛₗ[σ₃₄] Q) (hf : Function.Surjective ⇑f) (hg : ∃ (g' : Q →ₛₗ[σ₄₃] P), g ∘ₛₗ g' = id) : Function.Surjective ⇑(f.compr₂ₛₗ g)

A version of Function.Surjective.comp for composition of a bilinear map with a linear map.

theorem LinearMap.surjective_compr₂ₛₗ_of_equiv {R : Type u_1} [CommSemiring R] {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {M : Type u_18} {N : Type u_19} {P : Type u_20} {Q : Type u_21} [CommSemiring R₂] [CommSemiring R₃] [CommSemiring R₄] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : P ≃ₛₗ[σ₃₄] Q) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(f.compr₂ₛₗ ↑g)

A version of Function.Surjective.comp for composition of a bilinear map with a linear map.

theorem LinearMap.bijective_compr₂ₛₗ_of_equiv {R : Type u_1} [CommSemiring R] {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {M : Type u_18} {N : Type u_19} {P : Type u_20} {Q : Type u_21} [CommSemiring R₂] [CommSemiring R₃] [CommSemiring R₄] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : P ≃ₛₗ[σ₃₄] Q) (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(f.compr₂ₛₗ ↑g)

A version of Function.Bijective.comp for composition of a bilinear map with a linear map.

def LinearMap.lsmul (R : Type u_1) [CommSemiring R] (M : Type u_6) [AddCommMonoid M] [Module R M] : R →ₗ[R] M →ₗ[R] M

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

Equations

• LinearMap.lsmul R M = LinearMap.mk₂ R (fun (x1 : R) (x2 : M) => x1 • x2) ⋯ ⋯ ⋯ ⋯

theorem LinearMap.lsmul_eq_DistribMulAction_toLinearMap {R : Type u_1} [CommSemiring R] (M : Type u_6) [AddCommMonoid M] [Module R M] (r : R) : (lsmul R M) r = DistribMulAction.toLinearMap R M r

@[simp]

theorem LinearMap.lsmul_apply {R : Type u_1} [CommSemiring R] {M : Type u_6} [AddCommMonoid M] [Module R M] (r : R) (m : M) : ((lsmul R M) r) m = r • m

@[reducible, inline]

abbrev LinearMap.BilinMap (R : Type u_1) [CommSemiring R] (M : Type u_6) (Nₗ : Type u_11) [AddCommMonoid M] [AddCommMonoid Nₗ] [Module R M] [Module R Nₗ] : Type (max u_11 u_6)

A shorthand for the type of R-bilinear Nₗ-valued maps on M.

Equations

• LinearMap.BilinMap R M Nₗ = (M →ₗ[R] M →ₗ[R] Nₗ)

@[reducible, inline]

abbrev LinearMap.BilinForm (R : Type u_1) [CommSemiring R] (M : Type u_6) [AddCommMonoid M] [Module R M] : Type (max u_1 u_6)

For convenience, a shorthand for the type of bilinear forms from M to R.

Equations

• LinearMap.BilinForm R M = LinearMap.BilinMap R M R

theorem LinearMap.lsmul_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : R} (hx : x ≠ 0) : Function.Injective ⇑((lsmul R M) x)

theorem LinearMap.ker_lsmul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {a : R} (ha : a ≠ 0) : ker ((lsmul R M) a) = ⊥

noncomputable def LinearMap.restrictScalarsRange {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} {M' : Type u_5} {P' : Type u_6} [Semiring R] [Semiring S] [SMul S R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [Module S M] [Module S P] [IsScalarTower S R M] [IsScalarTower S R P] [AddCommMonoid M'] [Module S M'] [AddCommMonoid P'] [Module S P'] (i : M' →ₗ[S] M) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (f : M →ₗ[R] P) (hf : ∀ (m : M'), f (i m) ∈ range k) : M' →ₗ[S] P'

Restrict the scalars and range of a linear map.

Equations

• i.restrictScalarsRange k hk f hf = (↑S f ∘ₗ i).codLift k hk hf

@[simp]

theorem LinearMap.restrictScalarsRange_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} {M' : Type u_5} {P' : Type u_6} [Semiring R] [Semiring S] [SMul S R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [Module S M] [Module S P] [IsScalarTower S R M] [IsScalarTower S R P] [AddCommMonoid M'] [Module S M'] [AddCommMonoid P'] [Module S P'] (i : M' →ₗ[S] M) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (f : M →ₗ[R] P) (hf : ∀ (m : M'), f (i m) ∈ range k) (m : M') : k ((i.restrictScalarsRange k hk f hf) m) = f (i m)

@[simp]

theorem LinearMap.eq_restrictScalarsRange_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} {M' : Type u_5} {P' : Type u_6} [Semiring R] [Semiring S] [SMul S R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [Module S M] [Module S P] [IsScalarTower S R M] [IsScalarTower S R P] [AddCommMonoid M'] [Module S M'] [AddCommMonoid P'] [Module S P'] (i : M' →ₗ[S] M) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (f : M →ₗ[R] P) (hf : ∀ (m : M'), f (i m) ∈ range k) (m : M') (p : P') : p = (i.restrictScalarsRange k hk f hf) m ↔ k p = f (i m)

@[simp]

theorem LinearMap.restrictScalarsRange_apply_eq_zero_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} {M' : Type u_5} {P' : Type u_6} [Semiring R] [Semiring S] [SMul S R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] [Module S M] [Module S P] [IsScalarTower S R M] [IsScalarTower S R P] [AddCommMonoid M'] [Module S M'] [AddCommMonoid P'] [Module S P'] (i : M' →ₗ[S] M) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (f : M →ₗ[R] P) (hf : ∀ (m : M'), f (i m) ∈ range k) (m : M') : (i.restrictScalarsRange k hk f hf) m = 0 ↔ f (i m) = 0

noncomputable def LinearMap.restrictScalarsRange₂ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [CommSemiring R] [CommSemiring S] [SMul S R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module S M] [Module S N] [Module S P] [IsScalarTower S R M] [IsScalarTower S R N] [IsScalarTower S R P] [AddCommMonoid M'] [Module S M'] [AddCommMonoid N'] [Module S N'] [AddCommMonoid P'] [Module S P'] [SMulCommClass R S P] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (B : M →ₗ[R] N →ₗ[R] P) (hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ range k) : M' →ₗ[S] N' →ₗ[S] P'

Restrict the scalars, domains, and range of a bilinear map.

Equations

• i.restrictScalarsRange₂ j k hk B hB = ((LinearMap.restrictScalarsₗ S R N P S ∘ₗ ↑S B).compl₁₂ i j).codRestrict₂ k hk hB

@[simp]

theorem LinearMap.restrictScalarsRange₂_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [CommSemiring R] [CommSemiring S] [SMul S R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module S M] [Module S N] [Module S P] [IsScalarTower S R M] [IsScalarTower S R N] [IsScalarTower S R P] [AddCommMonoid M'] [Module S M'] [AddCommMonoid N'] [Module S N'] [AddCommMonoid P'] [Module S P'] [SMulCommClass R S P] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (B : M →ₗ[R] N →ₗ[R] P) (hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ range k) (m : M') (n : N') : k (((i.restrictScalarsRange₂ j k hk B hB) m) n) = (B (i m)) (j n)

@[simp]

theorem LinearMap.eq_restrictScalarsRange₂_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [CommSemiring R] [CommSemiring S] [SMul S R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module S M] [Module S N] [Module S P] [IsScalarTower S R M] [IsScalarTower S R N] [IsScalarTower S R P] [AddCommMonoid M'] [Module S M'] [AddCommMonoid N'] [Module S N'] [AddCommMonoid P'] [Module S P'] [SMulCommClass R S P] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (B : M →ₗ[R] N →ₗ[R] P) (hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ range k) (m : M') (n : N') (p : P') : p = ((i.restrictScalarsRange₂ j k hk B hB) m) n ↔ k p = (B (i m)) (j n)

@[simp]

theorem LinearMap.restrictScalarsRange₂_apply_eq_zero_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [CommSemiring R] [CommSemiring S] [SMul S R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module S M] [Module S N] [Module S P] [IsScalarTower S R M] [IsScalarTower S R N] [IsScalarTower S R P] [AddCommMonoid M'] [Module S M'] [AddCommMonoid N'] [Module S N'] [AddCommMonoid P'] [Module S P'] [SMulCommClass R S P] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N) (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (B : M →ₗ[R] N →ₗ[R] P) (hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ range k) (m : M') (n : N') : ((i.restrictScalarsRange₂ j k hk B hB) m) n = 0 ↔ (B (i m)) (j n) = 0