Basics on bilinear maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
linear_map.mk₂: a constructor for bilinear maps, taking an unbundled function together with proof witnesses of bilinearitylinear_map.flip: turns a bilinear mapM × N → PintoN × M → Plinear_map.lcompandlinear_map.llcomp: composition of linear maps as a bilinear maplinear_map.compl₂: composition of a bilinear mapM × N → Pwith a linear mapQ → Mlinear_map.compr₂: composition of a bilinear mapM × N → Pwith a linear mapQ → Nlinear_map.lsmul: scalar multiplication as a bilinear mapR × M → M
Tags #
bilinear
def
linear_map.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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
(ρ₁₂ : R →+* R₂)
(σ₁₂ : S →+* S₂)
(f : M → N → P)
(H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n)
(H2 : ∀ (c : R) (m : M) (n : N), f (c • m) n = ⇑ρ₁₂ c • f m n)
(H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂)
(H4 : ∀ (c : S) (m : M) (n : N), f m (c • n) = ⇑σ₁₂ c • f m n) :
Create a bilinear map from a function that is semilinear in each component.
See mk₂' and mk₂ for the linear case.
@[simp]
theorem
linear_map.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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M → N → P)
{H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n}
{H2 : ∀ (c : R) (m : M) (n : N), f (c • m) n = ⇑ρ₁₂ c • f m n}
{H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂}
{H4 : ∀ (c : S) (m : M) (n : N), f m (c • n) = ⇑σ₁₂ c • f m n}
(m : M)
(n : N) :
⇑(⇑(linear_map.mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4) m) n = f m n
def
linear_map.mk₂'
(R : Type u_1)
[semiring R]
(S : Type u_2)
[semiring S]
{M : Type u_5}
{N : Type u_6}
{Pₗ : Type u_12}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid Pₗ]
[module R M]
[module S N]
[module R Pₗ]
[module S Pₗ]
[smul_comm_class S R Pₗ]
(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
- linear_map.mk₂' R S f H1 H2 H3 H4 = linear_map.mk₂'ₛₗ (ring_hom.id R) (ring_hom.id S) f H1 H2 H3 H4
@[simp]
theorem
linear_map.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_12}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid Pₗ]
[module R M]
[module S N]
[module R Pₗ]
[module S Pₗ]
[smul_comm_class S R Pₗ]
(f : M → N → Pₗ)
{H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n}
{H2 : ∀ (c : R) (m : M) (n : N), f (c • m) n = c • f m n}
{H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂}
{H4 : ∀ (c : S) (m : M) (n : N), f m (c • n) = c • f m n}
(m : M)
(n : N) :
⇑(⇑(linear_map.mk₂' R S f H1 H2 H3 H4) m) n = f m n
theorem
linear_map.ext₂
{R : Type u_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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
{f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
(H : ∀ (m : M) (n : N), ⇑(⇑f m) n = ⇑(⇑g m) n) :
f = g
theorem
linear_map.congr_fun₂
{R : Type u_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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
{f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
(h : f = g)
(x : M)
(y : N) :
def
linear_map.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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) :
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 = linear_map.mk₂'ₛₗ σ₁₂ ρ₁₂ (λ (n : N) (m : M), ⇑(⇑f m) n) _ _ _ _
@[simp]
theorem
linear_map.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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
(m : M)
(n : N) :
@[simp]
theorem
linear_map.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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
[smul_comm_class R₂ S₂ P]
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) :
theorem
linear_map.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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
{f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
(H : f.flip = g.flip) :
f = g
theorem
linear_map.map_zero₂
{R : Type u_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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
(y : N) :
theorem
linear_map.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_13}
{P' : Type u_15}
[add_comm_monoid N]
[add_comm_group M']
[add_comm_group P']
[module S N]
[module R M']
[module R₂ P']
[module S₂ P']
[smul_comm_class S₂ R₂ P']
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P')
(x : M')
(y : N) :
theorem
linear_map.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_13}
{P' : Type u_15}
[add_comm_monoid N]
[add_comm_group M']
[add_comm_group P']
[module S N]
[module R M']
[module R₂ P']
[module S₂ P']
[smul_comm_class S₂ R₂ P']
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P')
(x y : M')
(z : N) :
theorem
linear_map.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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
(x₁ x₂ : M)
(y : N) :
theorem
linear_map.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}
[add_comm_monoid M₂]
[add_comm_monoid N₂]
[add_comm_monoid P₂]
[module R M₂]
[module S N₂]
[module R P₂]
[module S₂ P₂]
[smul_comm_class S₂ R P₂]
{σ₁₂ : S →+* S₂}
(f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂)
(r : R)
(x : M₂)
(y : N₂) :
theorem
linear_map.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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
(r : R)
(x : M)
(y : N) :
theorem
linear_map.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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
{ι : Type u_8}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
(t : finset ι)
(x : ι → M)
(y : N) :
def
linear_map.dom_restrict₂
{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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
(q : submodule S N) :
Restricting a bilinear map in the second entry
Equations
- f.dom_restrict₂ q = {to_fun := λ (m : M), (⇑f m).dom_restrict q, map_add' := _, map_smul' := _}
theorem
linear_map.dom_restrict₂_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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
(q : submodule S N)
(x : M)
(y : ↥q) :
def
linear_map.dom_restrict₁₂
{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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
(p : submodule R M)
(q : submodule S N) :
Restricting a bilinear map in both components
Equations
- f.dom_restrict₁₂ p q = (f.dom_restrict p).dom_restrict₂ q
theorem
linear_map.dom_restrict₁₂_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}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module S N]
[module R₂ P]
[module S₂ P]
[smul_comm_class S₂ R₂ P]
{ρ₁₂ : R →+* R₂}
{σ₁₂ : S →+* S₂}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
(p : submodule R M)
(q : submodule S N)
(x : ↥p)
(y : ↥q) :
def
linear_map.mk₂
(R : Type u_1)
[comm_semiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[add_comm_monoid M]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[module R M]
[module R Nₗ]
[module R Pₗ]
(f : M → Nₗ → Pₗ)
(H1 : ∀ (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n)
(H2 : ∀ (c : R) (m : M) (n : Nₗ), f (c • m) n = c • f m n)
(H3 : ∀ (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂)
(H4 : ∀ (c : R) (m : M) (n : Nₗ), f m (c • n) = c • f m n) :
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
- linear_map.mk₂ R f H1 H2 H3 H4 = linear_map.mk₂' R R f H1 H2 H3 H4
@[simp]
theorem
linear_map.mk₂_apply
(R : Type u_1)
[comm_semiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[add_comm_monoid M]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[module R M]
[module R Nₗ]
[module R Pₗ]
(f : M → Nₗ → Pₗ)
{H1 : ∀ (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n}
{H2 : ∀ (c : R) (m : M) (n : Nₗ), f (c • m) n = c • f m n}
{H3 : ∀ (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂}
{H4 : ∀ (c : R) (m : M) (n : Nₗ), f m (c • n) = c • f m n}
(m : M)
(n : Nₗ) :
⇑(⇑(linear_map.mk₂ R f H1 H2 H3 H4) m) n = f m n
def
linear_map.lflip
(R : Type u_1)
[comm_semiring R]
{R₂ : Type u_2}
[comm_semiring R₂]
{R₃ : Type u_3}
[comm_semiring R₃]
(M : Type u_5)
(N : Type u_6)
(P : Type u_7)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R₂ N]
[module R₃ P]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃} :
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
- linear_map.lflip R M N P = {to_fun := linear_map.flip σ₂₃, map_add' := _, map_smul' := _}
@[simp]
theorem
linear_map.lflip_apply
{R : Type u_1}
[comm_semiring R]
{R₂ : Type u_2}
[comm_semiring R₂]
{R₃ : Type u_3}
[comm_semiring R₃]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R₂ N]
[module R₃ P]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
(f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
(m : M)
(n : N) :
def
linear_map.lcomp
(R : Type u_1)
[comm_semiring R]
{M : Type u_5}
{Nₗ : Type u_10}
(Pₗ : Type u_11)
[add_comm_monoid M]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[module R M]
[module R Nₗ]
[module R Pₗ]
(f : M →ₗ[R] Nₗ) :
Composing a linear map M → N and a linear map N → P to form a linear map M → P.
Equations
- linear_map.lcomp R Pₗ f = (linear_map.id.flip.comp f).flip
@[simp]
theorem
linear_map.lcomp_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[add_comm_monoid M]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[module R M]
[module R Nₗ]
[module R Pₗ]
(f : M →ₗ[R] Nₗ)
(g : Nₗ →ₗ[R] Pₗ)
(x : M) :
theorem
linear_map.lcomp_apply'
{R : Type u_1}
[comm_semiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[add_comm_monoid M]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[module R M]
[module R Nₗ]
[module R Pₗ]
(f : M →ₗ[R] Nₗ)
(g : Nₗ →ₗ[R] Pₗ) :
⇑(linear_map.lcomp R Pₗ f) g = g.comp f
def
linear_map.lcompₛₗ
{R : Type u_1}
[comm_semiring R]
{R₂ : Type u_2}
[comm_semiring R₂]
{R₃ : Type u_3}
[comm_semiring R₃]
{M : Type u_5}
{N : Type u_6}
(P : Type u_7)
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R₂ N]
[module R₃ P]
{σ₁₂ : R →+* R₂}
(σ₂₃ : R₂ →+* R₃)
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] N) :
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
- linear_map.lcompₛₗ P σ₂₃ f = (linear_map.id.flip.comp f).flip
@[simp]
theorem
linear_map.lcompₛₗ_apply
{R : Type u_1}
[comm_semiring R]
{R₂ : Type u_2}
[comm_semiring R₂]
{R₃ : Type u_3}
[comm_semiring R₃]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R₂ N]
[module R₃ P]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] N)
(g : N →ₛₗ[σ₂₃] P)
(x : M) :
def
linear_map.llcomp
(R : Type u_1)
[comm_semiring R]
(M : Type u_5)
(Nₗ : Type u_10)
(Pₗ : Type u_11)
[add_comm_monoid M]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[module R M]
[module R Nₗ]
[module R Pₗ] :
Composing a linear map M → N and a linear map N → P to form a linear map M → P.
Equations
- linear_map.llcomp R M Nₗ Pₗ = {to_fun := linear_map.lcomp R Pₗ _inst_20, map_add' := _, map_smul' := _}.flip
@[simp]
theorem
linear_map.llcomp_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[add_comm_monoid M]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[module R M]
[module R Nₗ]
[module R Pₗ]
(f : Nₗ →ₗ[R] Pₗ)
(g : M →ₗ[R] Nₗ)
(x : M) :
theorem
linear_map.llcomp_apply'
{R : Type u_1}
[comm_semiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[add_comm_monoid M]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[module R M]
[module R Nₗ]
[module R Pₗ]
(f : Nₗ →ₗ[R] Pₗ)
(g : M →ₗ[R] Nₗ) :
⇑(⇑(linear_map.llcomp R M Nₗ Pₗ) f) g = f.comp g
def
linear_map.compl₂
{R : Type u_1}
[comm_semiring R]
{R₂ : Type u_2}
[comm_semiring R₂]
{R₃ : Type u_3}
[comm_semiring R₃]
{R₄ : Type u_4}
[comm_semiring R₄]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R₂ N]
[module R₃ P]
[module R₄ Q]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
{σ₄₂ : R₄ →+* R₂}
{σ₄₃ : R₄ →+* R₃}
[ring_hom_comp_triple σ₄₂ σ₂₃ σ₄₃]
(f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
(g : Q →ₛₗ[σ₄₂] N) :
Composing a linear map Q → N and a bilinear map M → N → P to
form a bilinear map M → Q → P.
Equations
- f.compl₂ g = (linear_map.lcompₛₗ P σ₂₃ g).comp f
@[simp]
theorem
linear_map.compl₂_apply
{R : Type u_1}
[comm_semiring R]
{R₂ : Type u_2}
[comm_semiring R₂]
{R₃ : Type u_3}
[comm_semiring R₃]
{R₄ : Type u_4}
[comm_semiring R₄]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R₂ N]
[module R₃ P]
[module R₄ Q]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
{σ₄₂ : R₄ →+* R₂}
{σ₄₃ : R₄ →+* R₃}
[ring_hom_comp_triple σ₄₂ σ₂₃ σ₄₃]
(f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
(g : Q →ₛₗ[σ₄₂] N)
(m : M)
(q : Q) :
@[simp]
theorem
linear_map.compl₂_id
{R : Type u_1}
[comm_semiring R]
{R₂ : Type u_2}
[comm_semiring R₂]
{R₃ : Type u_3}
[comm_semiring R₃]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R₂ N]
[module R₃ P]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
(f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) :
f.compl₂ linear_map.id = f
def
linear_map.compl₁₂
{R : Type u_1}
[comm_semiring R]
{Mₗ : Type u_9}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
{Qₗ : Type u_12}
{Qₗ' : Type u_13}
[add_comm_monoid Mₗ]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[add_comm_monoid Qₗ]
[add_comm_monoid Qₗ']
[module R Mₗ]
[module R Nₗ]
[module R Pₗ]
[module R Qₗ]
[module R Qₗ']
(f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ)
(g : Qₗ →ₗ[R] Mₗ)
(g' : Qₗ' →ₗ[R] Nₗ) :
Composing linear maps Q → M and Q' → N with a bilinear map M → N → P to
form a bilinear map Q → Q' → P.
@[simp]
theorem
linear_map.compl₁₂_apply
{R : Type u_1}
[comm_semiring R]
{Mₗ : Type u_9}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
{Qₗ : Type u_12}
{Qₗ' : Type u_13}
[add_comm_monoid Mₗ]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[add_comm_monoid Qₗ]
[add_comm_monoid Qₗ']
[module R Mₗ]
[module R Nₗ]
[module R Pₗ]
[module R Qₗ]
[module R Qₗ']
(f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ)
(g : Qₗ →ₗ[R] Mₗ)
(g' : Qₗ' →ₗ[R] Nₗ)
(x : Qₗ)
(y : Qₗ') :
@[simp]
theorem
linear_map.compl₁₂_id_id
{R : Type u_1}
[comm_semiring R]
{Mₗ : Type u_9}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[add_comm_monoid Mₗ]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[module R Mₗ]
[module R Nₗ]
[module R Pₗ]
(f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) :
theorem
linear_map.compl₁₂_inj
{R : Type u_1}
[comm_semiring R]
{Mₗ : Type u_9}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
{Qₗ : Type u_12}
{Qₗ' : Type u_13}
[add_comm_monoid Mₗ]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[add_comm_monoid Qₗ]
[add_comm_monoid Qₗ']
[module R Mₗ]
[module R Nₗ]
[module R Pₗ]
[module R Qₗ]
[module R Qₗ']
{f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ}
{g : Qₗ →ₗ[R] Mₗ}
{g' : Qₗ' →ₗ[R] Nₗ}
(hₗ : function.surjective ⇑g)
(hᵣ : function.surjective ⇑g') :
def
linear_map.compr₂
{R : Type u_1}
[comm_semiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
{Qₗ : Type u_12}
[add_comm_monoid M]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[add_comm_monoid Qₗ]
[module R M]
[module R Nₗ]
[module R Pₗ]
[module R Qₗ]
(f : M →ₗ[R] Nₗ →ₗ[R] Pₗ)
(g : Pₗ →ₗ[R] Qₗ) :
Composing a linear map P → Q and a bilinear map M → N → P to
form a bilinear map M → N → Q.
Equations
- f.compr₂ g = (⇑(linear_map.llcomp R Nₗ Pₗ Qₗ) g).comp f
@[simp]
theorem
linear_map.compr₂_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
{Qₗ : Type u_12}
[add_comm_monoid M]
[add_comm_monoid Nₗ]
[add_comm_monoid Pₗ]
[add_comm_monoid Qₗ]
[module R M]
[module R Nₗ]
[module R Pₗ]
[module R Qₗ]
(f : M →ₗ[R] Nₗ →ₗ[R] Pₗ)
(g : Pₗ →ₗ[R] Qₗ)
(m : M)
(n : Nₗ) :
def
linear_map.lsmul
(R : Type u_1)
[comm_semiring R]
(M : Type u_5)
[add_comm_monoid M]
[module R M] :
Scalar multiplication as a bilinear map R → M → M.
Equations
- linear_map.lsmul R M = linear_map.mk₂ R has_smul.smul _ _ _ _
@[simp]
theorem
linear_map.lsmul_apply
{R : Type u_1}
[comm_semiring R]
{M : Type u_5}
[add_comm_monoid M]
[module R M]
(r : R)
(m : M) :
⇑(⇑(linear_map.lsmul R M) r) m = r • m
theorem
linear_map.lsmul_injective
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
{x : R}
(hx : x ≠ 0) :
function.injective ⇑(⇑(linear_map.lsmul R M) x)
theorem
linear_map.ker_lsmul
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
{a : R}
(ha : a ≠ 0) :
linear_map.ker (⇑(linear_map.lsmul R M) a) = ⊥