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 = { toAddHom := { toFun := fun (m : M) => { toAddHom := { 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_12}
[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_12}
[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 : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
{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 : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
{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 : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
{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
- LinearMap.flip f = 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)
:
((LinearMap.flip f) 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)
:
LinearMap.flip (LinearMap.flip f) = 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 : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
{g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
(H : LinearMap.flip f = LinearMap.flip g)
:
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_13}
{P' : Type u_15}
[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_13}
{P' : Type u_15}
[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 : 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₁ : M)
(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_16}
(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P)
(t : Finset ι)
(x : ι → M)
(y : N)
:
(f (Finset.sum t fun (i : ι) => x i)) y = Finset.sum t fun (i : ι) => (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
- LinearMap.domRestrict₂ f q = { toAddHom := { toFun := fun (m : M) => LinearMap.domRestrict (f m) 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)
:
((LinearMap.domRestrict₂ f 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
- LinearMap.domRestrict₁₂ f p q = LinearMap.domRestrict₂ (LinearMap.domRestrict f p) 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)
:
((LinearMap.domRestrict₁₂ f p q) x) y = (f ↑x) ↑y
@[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_12}
[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_16)
(S' : Type u_17)
[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)
:
∀ (x : N), ((LinearMap.restrictScalars₁₂ R' S' B) m) x = (B m) x
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_12}
[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_16)
(S' : Type u_17)
[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 (x : M) (x_1 : N) => (B x) x_1) ⋯ ⋯ ⋯ ⋯
Instances For
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_12}
[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_16)
(S' : Type u_17)
[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_12}
[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_16)
(S' : Type u_17)
[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ₗ}
{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 = { toAddHom := { 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.flip (LinearMap.comp (LinearMap.flip LinearMap.id) f)
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.flip (LinearMap.comp (LinearMap.flip LinearMap.id) f)
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ₗ = LinearMap.flip { toAddHom := { toFun := LinearMap.lcomp R Pₗ, map_add' := ⋯ }, map_smul' := ⋯ }
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₂}
{σ₄₃ : R₄ →+* R₃}
[RingHomCompTriple σ₄₂ σ₂₃ σ₄₃]
(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
- LinearMap.compl₂ f g = LinearMap.comp (LinearMap.lcompₛₗ P σ₂₃ g) f
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)
:
((LinearMap.compl₂ f 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)
:
LinearMap.compl₂ f LinearMap.id = f
def
LinearMap.compl₁₂
{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ₗ)
:
Composing linear maps Q → M and Q' → N with a bilinear map M → N → P to
form a bilinear map Q → Q' → P.
Equations
- LinearMap.compl₁₂ f g g' = LinearMap.compl₂ (LinearMap.comp f g) 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ₗ')
:
((LinearMap.compl₁₂ f 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ₗ)
:
LinearMap.compl₁₂ f 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₁ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ}
{f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ}
{g : Qₗ →ₗ[R] Mₗ}
{g' : Qₗ' →ₗ[R] Nₗ}
(hₗ : Function.Surjective ⇑g)
(hᵣ : Function.Surjective ⇑g')
:
LinearMap.compl₁₂ f₁ g g' = LinearMap.compl₁₂ f₂ g g' ↔ f₁ = f₂
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
- LinearMap.compr₂ f g = LinearMap.comp ((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ₗ)
:
((LinearMap.compr₂ f 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 (x : R) (x_1 : M) => x • x_1) ⋯ ⋯ ⋯ ⋯
Instances For
@[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
@[inline, reducible]
abbrev
LinearMap.BilinForm
(R : Type u_1)
[CommSemiring R]
(M : Type u_5)
[AddCommMonoid M]
[Module R M]
:
Type (max u_5 u_1)
For convenience, a shorthand for the type of bilinear forms from M to R.
Instances For
theorem
LinearMap.lsmul_injective
{R : Type u_1}
{M : Type u_5}
[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_5}
[CommRing R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
{a : R}
(ha : a ≠ 0)
:
LinearMap.ker ((LinearMap.lsmul R M) a) = ⊥