# 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

source
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' := ⋯ }

Instances For

source
@[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
source
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

Instances For

source
@[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
source
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
source
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
source
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
source
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) ⋯ ⋯ ⋯ ⋯

Instances For

source
@[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
source
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

Instances For

source
@[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)
source
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' := ⋯ }

Instances For

source
@[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)
source
@[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
source
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

Instances For

source
@[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)
source
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
source
theorem LinearMap.lcomp_injective_of_surjective {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] (g : M →ₗ[R] M₂) (surj : Function.Surjective ⇑g) :
Function.Injective ⇑(lcomp S N g)
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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' := ⋯ }

Instances For

source
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
source
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

Instances For

source
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
source
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) ⋯ ⋯ ⋯ ⋯

Instances For

source
@[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✝
source
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')
source
@[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'
source
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 := ⋯ }

Instances For

source
@[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
source
@[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
source
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

Instances For

source
@[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
source
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'

Instances For

source
@[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)
source
@[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
source
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₂
source
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' := ⋯ }

Instances For

source
@[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)
source
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.

source
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.

source
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.

source
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.

source
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

Instances For

source
@[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)
source
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
source
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

Instances For

source
@[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)
source
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.

source
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.

source
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.

source
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.

source
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) ⋯ ⋯ ⋯ ⋯

Instances For

source
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
source
@[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
source
@[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ₗ)

Instances For

source
@[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

Instances For

source
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)
source
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) = ⊥
source
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

Instances For

source
@[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)
source
@[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)
source
@[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
source
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

Instances For

source
@[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)
source
@[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)
source
@[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