Lemmas about bilinear maps with a basis over each argument #
theorem
LinearMap.ext_basis
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{R : Type u_3}
{R₂ : Type u_4}
{S : Type u_5}
{S₂ : Type u_6}
{M : Type u_7}
{N : Type u_8}
{P : Type u_9}
[CommSemiring R]
[CommSemiring S]
[CommSemiring R₂]
[CommSemiring S₂]
[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₂}
(b₁ : Basis ι₁ R M)
(b₂ : Basis ι₂ S N)
{B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
{B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
(h : ∀ (i : ι₁) (j : ι₂), ↑(↑B (↑b₁ i)) (↑b₂ j) = ↑(↑B' (↑b₁ i)) (↑b₂ j))
:
B = B'
Two bilinear maps are equal when they are equal on all basis vectors.
theorem
LinearMap.sum_repr_mul_repr_mulₛₗ
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{R : Type u_3}
{R₂ : Type u_4}
{S : Type u_5}
{S₂ : Type u_6}
{M : Type u_7}
{N : Type u_8}
{P : Type u_9}
[CommSemiring R]
[CommSemiring S]
[CommSemiring R₂]
[CommSemiring S₂]
[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₂}
(b₁ : Basis ι₁ R M)
(b₂ : Basis ι₂ S N)
{B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
(x : M)
(y : N)
:
(Finsupp.sum (↑b₁.repr x) fun i xi => Finsupp.sum (↑b₂.repr y) fun j yj => ↑ρ₁₂ xi • ↑σ₁₂ yj • ↑(↑B (↑b₁ i)) (↑b₂ j)) = ↑(↑B x) y
Write out B x y as a sum over B (b i) (b j) if b is a basis.
Version for semi-bilinear maps, see sum_repr_mul_repr_mul for the bilinear version.
theorem
LinearMap.sum_repr_mul_repr_mul
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{R : Type u_3}
{Mₗ : Type u_10}
{Nₗ : Type u_11}
{Pₗ : Type u_12}
[CommSemiring R]
[AddCommMonoid Mₗ]
[AddCommMonoid Nₗ]
[AddCommMonoid Pₗ]
[Module R Mₗ]
[Module R Nₗ]
[Module R Pₗ]
(b₁' : Basis ι₁ R Mₗ)
(b₂' : Basis ι₂ R Nₗ)
{B : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ}
(x : Mₗ)
(y : Nₗ)
:
(Finsupp.sum (↑b₁'.repr x) fun i xi => Finsupp.sum (↑b₂'.repr y) fun j yj => xi • yj • ↑(↑B (↑b₁' i)) (↑b₂' j)) = ↑(↑B x) y
Write out B x y as a sum over B (b i) (b j) if b is a basis.
Version for bilinear maps, see sum_repr_mul_repr_mulₛₗ for the semi-bilinear version.