Mathlib.LinearAlgebra.Multilinear.Basis

Module docstring

{"# 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.tensorProduct for PiTensorProduct.

Basis.ext_multilinear_fin theorem

 {f g : MultilinearMap R M M₂} {ι₁ : Fin n → Type*} (e : ∀ i, Basis (ι₁ i) R (M i))
  (h : ∀ v : ∀ i, ι₁ i, (f fun i => e i (v i)) = g fun i => e i (v i)) : f = g

Full source

/-- Two multilinear maps indexed by `Fin n` are equal if they are equal when all arguments are
basis vectors. -/
theorem Basis.ext_multilinear_fin {f g : MultilinearMap R M M₂} {ι₁ : Fin n → Type*}
    (e : ∀ i, Basis (ι₁ i) R (M i))
    (h : ∀ v : ∀ i, ι₁ i, (f fun i => e i (v i)) = g fun i => e i (v i)) : f = g := by
  induction n with
  | zero =>
    ext x
    convert h finZeroElim
  | succ m hm =>
    apply Function.LeftInverse.injective uncurry_curryLeft
    refine Basis.ext (e 0) ?_
    intro i
    apply hm (Fin.tail e)
    intro j
    convert h (Fin.cons i j)
    iterate 2
      rw [curryLeft_apply]
      congr 1 with x
      refine Fin.cases rfl (fun x => ?_) x
      dsimp [Fin.tail]
      rw [Fin.cons_succ, Fin.cons_succ]

Equality of Multilinear Maps on Basis Vectors for Finite Index

Informal description

Let $R$ be a commutative ring, $n$ a natural number, and for each $i \in \text{Fin}\,n$, let $M_i$ and $M_2$ be $R$-modules with a basis $e_i$ indexed by $\iota_i$ for $M_i$. Suppose $f$ and $g$ are multilinear maps from $\prod_{i \in \text{Fin}\,n} M_i$ to $M_2$. If for every family of vectors $(v_i)_{i \in \text{Fin}\,n}$ with $v_i \in \iota_i$, we have $f((e_i(v_i))_i) = g((e_i(v_i))_i)$, then $f = g$.

Basis.ext_multilinear theorem

 [Finite ι] {f g : MultilinearMap R (fun _ : ι => M₂) M₃} {ι₁ : Type*} (e : Basis ι₁ R M₂)
  (h : ∀ v : ι → ι₁, (f fun i => e (v i)) = g fun i => e (v i)) : f = g

Full source

/-- 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`. -/
theorem Basis.ext_multilinear [Finite ι] {f g : MultilinearMap R (fun _ : ι => M₂) M₃} {ι₁ : Type*}
    (e : Basis ι₁ R M₂) (h : ∀ v : ι → ι₁, (f fun i => e (v i)) = g fun i => e (v i)) : f = g := by
  cases nonempty_fintype ι
  exact
    (domDomCongr_eq_iff (Fintype.equivFin ι) f g).mp
      (Basis.ext_multilinear_fin (fun _ => e) fun i => h (i ∘ _))

Equality of Multilinear Maps via Basis Vectors for Finite Index Type

Informal description

Let $R$ be a commutative ring, $\iota$ a finite index type, and $M₂$, $M₃$ be $R$-modules with a basis $e$ indexed by $\iota₁$ for $M₂$. Suppose $f$ and $g$ are multilinear maps from $\prod_{i \in \iota} M₂$ to $M₃$. If for every family of vectors $(v_i)_{i \in \iota}$ with $v_i \in \iota₁$, we have $f((e(v_i))_i) = g((e(v_i))_i)$, then $f = g$.