Multilinear maps in relation to bases. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.tensor_productforpi_tensor_product.
theorem
basis.ext_multilinear_fin
{R : Type u_1}
{n : ℕ}
{M : fin n → Type u_3}
{M₂ : Type u_4}
[comm_semiring R]
[add_comm_monoid M₂]
[Π (i : fin n), add_comm_monoid (M i)]
[Π (i : fin n), module R (M i)]
[module R M₂]
{f g : multilinear_map R M M₂}
{ι₁ : fin n → Type u_2}
(e : Π (i : fin n), basis (ι₁ i) R (M i))
(h : ∀ (v : Π (i : fin n), ι₁ i), ⇑f (λ (i : fin n), ⇑(e i) (v i)) = ⇑g (λ (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}
[comm_semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₂]
[module R M₃]
[finite ι]
{f g : multilinear_map R (λ (i : ι), M₂) M₃}
{ι₁ : Type u_3}
(e : basis ι₁ R M₂)
(h : ∀ (v : ι → ι₁), ⇑f (λ (i : ι), ⇑e (v i)) = ⇑g (λ (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.