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 bilinearityLinearMap.flip: turns a bilinear mapM × N → PintoN × M → PLinearMap.lcompandLinearMap.llcomp: composition of linear maps as a bilinear mapLinearMap.compl₂: composition of a bilinear mapM × N → Pwith a linear mapQ → MLinearMap.compr₂: composition of a bilinear mapM × N → Pwith a linear mapQ → NLinearMap.lsmul: scalar multiplication as a bilinear mapR × 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)
:
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
@[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)
:
((LinearMap.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)
:
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
@[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)
:
((LinearMap.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}
:
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)
:
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
@[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
@[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)
:
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)
:
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)
:
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₂)
:
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)
:
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)
:
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
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)
:
Restricting a bilinear map in both components
Equations
- f.domRestrict₁₂ p q = (f.domRestrict p).domRestrict₂ q
Instances For
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ₗ)
:
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
@[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)
:
((LinearMap.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ₗ]
:
@[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ₗ}
:
LinearMap.restrictScalars₁₂ R' S' B = LinearMap.restrictScalars₁₂ R' S' B' ↔ B = B'
def
LinearMap.mk₂
(R : Type u_1)
[CommSemiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[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)
:
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
@[simp]
theorem
LinearMap.mk₂_apply
(R : Type u_1)
[CommSemiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[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ₗ)
:
((LinearMap.mk₂ R f H1 H2 H3 H4) m) n = f m n
def
LinearMap.lflip
{R : Type u_1}
[CommSemiring R]
{R₂ : Type u_2}
[CommSemiring R₂]
{R₃ : Type u_3}
[CommSemiring R₃]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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
- LinearMap.lflip = { toFun := LinearMap.flip, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
LinearMap.lflip_apply
{R : Type u_1}
[CommSemiring R]
{R₂ : Type u_2}
[CommSemiring R₂]
{R₃ : Type u_3}
[CommSemiring R₃]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R₂ N]
[Module R₃ P]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
(f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
(m : M)
(n : N)
:
((LinearMap.lflip f) n) m = (f m) n
def
LinearMap.lcomp
(R : Type u_1)
[CommSemiring R]
{M : Type u_5}
{Nₗ : Type u_10}
(Pₗ : Type u_11)
[AddCommMonoid M]
[AddCommMonoid Nₗ]
[AddCommMonoid 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
- LinearMap.lcomp R Pₗ f = (LinearMap.id.flip ∘ₗ f).flip
Instances For
@[simp]
theorem
LinearMap.lcomp_apply
{R : Type u_1}
[CommSemiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[AddCommMonoid M]
[AddCommMonoid Nₗ]
[AddCommMonoid Pₗ]
[Module R M]
[Module R Nₗ]
[Module R Pₗ]
(f : M →ₗ[R] Nₗ)
(g : Nₗ →ₗ[R] Pₗ)
(x : M)
:
((LinearMap.lcomp R Pₗ f) g) x = g (f x)
theorem
LinearMap.lcomp_apply'
{R : Type u_1}
[CommSemiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[AddCommMonoid M]
[AddCommMonoid Nₗ]
[AddCommMonoid Pₗ]
[Module R M]
[Module R Nₗ]
[Module R Pₗ]
(f : M →ₗ[R] Nₗ)
(g : Nₗ →ₗ[R] Pₗ)
:
(LinearMap.lcomp R Pₗ f) g = g ∘ₗ f
def
LinearMap.lcompₛₗ
{R : Type u_1}
[CommSemiring R]
{R₂ : Type u_2}
[CommSemiring R₂]
{R₃ : Type u_3}
[CommSemiring R₃]
{M : Type u_5}
{N : Type u_6}
(P : Type u_7)
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R₂ N]
[Module R₃ P]
{σ₁₂ : R →+* R₂}
(σ₂₃ : R₂ →+* R₃)
{σ₁₃ : R →+* R₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
(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
- LinearMap.lcompₛₗ P σ₂₃ f = (LinearMap.id.flip.comp f).flip
Instances For
@[simp]
theorem
LinearMap.lcompₛₗ_apply
{R : Type u_1}
[CommSemiring R]
{R₂ : Type u_2}
[CommSemiring R₂]
{R₃ : Type u_3}
[CommSemiring R₃]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R₂ N]
[Module R₃ P]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] N)
(g : N →ₛₗ[σ₂₃] P)
(x : M)
:
((LinearMap.lcompₛₗ P σ₂₃ f) g) x = g (f x)
def
LinearMap.llcomp
(R : Type u_1)
[CommSemiring R]
(M : Type u_5)
(Nₗ : Type u_10)
(Pₗ : Type u_11)
[AddCommMonoid M]
[AddCommMonoid Nₗ]
[AddCommMonoid 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
- LinearMap.llcomp R M Nₗ Pₗ = { toFun := LinearMap.lcomp R Pₗ, map_add' := ⋯, map_smul' := ⋯ }.flip
Instances For
@[simp]
theorem
LinearMap.llcomp_apply
{R : Type u_1}
[CommSemiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[AddCommMonoid M]
[AddCommMonoid Nₗ]
[AddCommMonoid Pₗ]
[Module R M]
[Module R Nₗ]
[Module R Pₗ]
(f : Nₗ →ₗ[R] Pₗ)
(g : M →ₗ[R] Nₗ)
(x : M)
:
(((LinearMap.llcomp R M Nₗ Pₗ) f) g) x = f (g x)
theorem
LinearMap.llcomp_apply'
{R : Type u_1}
[CommSemiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[AddCommMonoid M]
[AddCommMonoid Nₗ]
[AddCommMonoid Pₗ]
[Module R M]
[Module R Nₗ]
[Module R Pₗ]
(f : Nₗ →ₗ[R] Pₗ)
(g : M →ₗ[R] Nₗ)
:
((LinearMap.llcomp R M Nₗ Pₗ) f) g = f ∘ₗ g
def
LinearMap.compl₂
{R : Type u_1}
[CommSemiring R]
{R₂ : Type u_2}
[CommSemiring R₂]
{R₃ : Type u_3}
[CommSemiring R₃]
{R₄ : Type u_4}
[CommSemiring R₄]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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₃}
[RingHomCompTriple σ₄₂ σ₂₃ σ₄₃]
{R₅ : Type u_14}
[CommSemiring R₅]
[Module R₅ P]
[SMulCommClass R₃ R₅ P]
{σ₁₅ : R →+* R₅}
(h : 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
- h.compl₂ g = { toFun := fun (a : M) => (LinearMap.lcompₛₗ P σ₂₃ g) (h a), map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
LinearMap.compl₂_apply
{R : Type u_1}
[CommSemiring R]
{R₂ : Type u_2}
[CommSemiring R₂]
{R₃ : Type u_3}
[CommSemiring R₃]
{R₄ : Type u_4}
[CommSemiring R₄]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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₃}
[RingHomCompTriple σ₄₂ σ₂₃ σ₄₃]
(f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
(g : Q →ₛₗ[σ₄₂] N)
(m : M)
(q : Q)
:
((f.compl₂ g) m) q = (f m) (g q)
@[simp]
theorem
LinearMap.compl₂_id
{R : Type u_1}
[CommSemiring R]
{R₂ : Type u_2}
[CommSemiring R₂]
{R₃ : Type u_3}
[CommSemiring R₃]
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R₂ N]
[Module R₃ P]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
(f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
:
f.compl₂ LinearMap.id = f
def
LinearMap.compl₁₂
{R₂ : Type u_2}
[CommSemiring R₂]
{N : Type u_6}
{Mₗ : Type u_9}
{Pₗ : Type u_11}
{Qₗ : Type u_12}
{Qₗ' : Type u_13}
[AddCommMonoid N]
[AddCommMonoid Mₗ]
[AddCommMonoid Pₗ]
[AddCommMonoid Qₗ]
[AddCommMonoid Qₗ']
{R₁ : Type u_14}
[CommSemiring R₁]
[Module R₂ N]
[Module R₂ Pₗ]
[Module R₁ Pₗ]
[Module R₁ Mₗ]
[SMulCommClass R₂ 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.
Equations
- f.compl₁₂ g g' = (f ∘ₗ g).compl₂ g'
Instances For
@[simp]
theorem
LinearMap.compl₁₂_apply
{R : Type u_1}
[CommSemiring R]
{Mₗ : Type u_9}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
{Qₗ : Type u_12}
{Qₗ' : Type u_13}
[AddCommMonoid Mₗ]
[AddCommMonoid Nₗ]
[AddCommMonoid Pₗ]
[AddCommMonoid Qₗ]
[AddCommMonoid Qₗ']
[Module R Mₗ]
[Module R Nₗ]
[Module R Pₗ]
[Module R Qₗ]
[Module R Qₗ']
(f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ)
(g : Qₗ →ₗ[R] Mₗ)
(g' : Qₗ' →ₗ[R] Nₗ)
(x : Qₗ)
(y : Qₗ')
:
((f.compl₁₂ g g') x) y = (f (g x)) (g' y)
@[simp]
theorem
LinearMap.compl₁₂_id_id
{R : Type u_1}
[CommSemiring R]
{Mₗ : Type u_9}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
[AddCommMonoid Mₗ]
[AddCommMonoid Nₗ]
[AddCommMonoid Pₗ]
[Module R Mₗ]
[Module R Nₗ]
[Module R Pₗ]
(f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ)
:
f.compl₁₂ LinearMap.id LinearMap.id = f
theorem
LinearMap.compl₁₂_inj
{R : Type u_1}
[CommSemiring R]
{Mₗ : Type u_9}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
{Qₗ : Type u_12}
{Qₗ' : Type u_13}
[AddCommMonoid Mₗ]
[AddCommMonoid Nₗ]
[AddCommMonoid Pₗ]
[AddCommMonoid Qₗ]
[AddCommMonoid 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
LinearMap.compr₂
{R : Type u_1}
[CommSemiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
{Qₗ : Type u_12}
[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ₗ)
:
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 = (LinearMap.llcomp R Nₗ Pₗ Qₗ) g ∘ₗ f
Instances For
@[simp]
theorem
LinearMap.compr₂_apply
{R : Type u_1}
[CommSemiring R]
{M : Type u_5}
{Nₗ : Type u_10}
{Pₗ : Type u_11}
{Qₗ : Type u_12}
[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ₗ)
(m : M)
(n : Nₗ)
:
((f.compr₂ g) m) n = g ((f m) n)
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
theorem
LinearMap.lsmul_eq_DistribMulAction_toLinearMap
{R : Type u_1}
[CommSemiring R]
(M : Type u_5)
[AddCommMonoid M]
[Module R M]
(r : R)
:
(LinearMap.lsmul R M) r = DistribMulAction.toLinearMap R M r
@[simp]
theorem
LinearMap.lsmul_apply
{R : Type u_1}
[CommSemiring R]
{M : Type u_5}
[AddCommMonoid M]
[Module R M]
(r : R)
(m : M)
:
((LinearMap.lsmul R M) r) m = r • m
@[reducible, inline]
abbrev
LinearMap.BilinMap
(R : Type u_1)
[CommSemiring R]
(M : Type u_5)
(Nₗ : Type u_10)
[AddCommMonoid M]
[AddCommMonoid Nₗ]
[Module R M]
[Module R Nₗ]
:
Type (max u_10 u_5)
A shorthand for the type of R-bilinear Nₗ-valued maps on M.
Instances For
@[reducible, inline]
abbrev
LinearMap.BilinForm
(R : Type u_1)
[CommSemiring R]
(M : Type u_5)
[AddCommMonoid M]
[Module R M]
:
Type (max u_1 u_5)
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
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 ⇑((LinearMap.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)
:
LinearMap.ker ((LinearMap.lsmul R M) a) = ⊥
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) ∈ LinearMap.range k)
:
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
@[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) ∈ LinearMap.range k)
(m : M')
(n : N')
:
k (((i.restrictScalarsRange j k hk B hB) m) n) = (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) ∈ LinearMap.range k)
(m : M')
(n : N')
: