Documentation

Mathlib.LinearAlgebra.Multilinear.Basis

Multilinear maps in relation to bases. #

This file proves lemmas about the action of multilinear maps on basis vectors.

TODO #

theorem Basis.ext_multilinear_fin {R : Type u_1} {n : } {M : Fin nType 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 : MultilinearMap R M M₂} {g : MultilinearMap R M M₂} {ι₁ : Fin nType u_6} (e : (i : Fin n) → Basis (ι₁ i) R (M i)) (h : ∀ (v : (i : Fin n) → ι₁ i), (f fun i => ↑(e i) (v i)) = g fun i => ↑(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 : MultilinearMap R (fun x => M₂) M₃} {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.