Multilinear maps in relation to bases. #
This file proves lemmas about the action of multilinear maps on basis vectors.
TODO #
- Refactor the proofs in terms of bases of tensor products, once there is an equivalent of
Basis.tensorProductforPiTensorProduct.
theorem
Basis.ext_multilinear_fin
{R : Type u_1}
{n : ℕ}
{M : Fin n → Type u_3}
{M₂ : Type u_4}
[CommSemiring R]
[AddCommMonoid M₂]
[(i : Fin n) → AddCommMonoid (M i)]
[(i : Fin n) → Module R (M i)]
[Module R M₂]
{f g : MultilinearMap R M M₂}
{ι₁ : Fin n → Type u_6}
(e : (i : Fin n) → Basis (ι₁ i) R (M i))
(h : ∀ (v : (i : Fin n) → ι₁ i), (f fun (i : Fin n) => (e i) (v i)) = g fun (i : Fin n) => (e i) (v i))
:
f = g
Two multilinear maps indexed by Fin n are equal if they are equal when all arguments are
basis vectors.
theorem
Basis.ext_multilinear
{R : Type u_1}
{ι : Type u_2}
{M₂ : Type u_4}
{M₃ : Type u_5}
[CommSemiring R]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₂]
[Module R M₃]
[Finite ι]
{f g : MultilinearMap R (fun (x : ι) => M₂) M₃}
{ι₁ : Type u_6}
(e : Basis ι₁ R M₂)
(h : ∀ (v : ι → ι₁), (f fun (i : ι) => e (v i)) = g fun (i : ι) => e (v i))
:
f = g
Two multilinear maps indexed by a Fintype are equal if they are equal when all arguments
are basis vectors. Unlike Basis.ext_multilinear_fin, this only uses a single basis; a
dependently-typed version would still be true, but the proof would need a dependently-typed
version of dom_dom_congr.