Multilinear maps in relation to bases.

This file proves lemmas about the action of multilinear maps on basis vectors and constructs a basis for multilinear maps given bases on the domain and codomain.

theorem Module.Basis.ext_multilinear {ι : Type u_1} {R : Type u_2} [CommSemiring R] {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : Type u_4} [AddCommMonoid N] [Module R N] [Finite ι] {f g : MultilinearMap R M N} {ιM : ι → Type u_5} (e : (i : ι) → Basis (ιM i) R (M i)) (h : ∀ (v : (i : ι) → ιM i), (f fun (i : ι) => (e i) (v i)) = g fun (i : ι) => (e i) (v i)) : f = g

Two multilinear maps indexed by a Fintype are equal if they are equal when all arguments are basis vectors.

@[deprecated Module.Basis.ext_multilinear (since := "2025-05-12")]

theorem Basis.ext_multilinear_fin {ι : Type u_1} {R : Type u_2} [CommSemiring R] {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : Type u_4} [AddCommMonoid N] [Module R N] [Finite ι] {f g : MultilinearMap R M N} {ιM : ι → Type u_5} (e : (i : ι) → Module.Basis (ιM i) R (M i)) (h : ∀ (v : (i : ι) → ιM i), (f fun (i : ι) => (e i) (v i)) = g fun (i : ι) => (e i) (v i)) : f = g

Alias of Module.Basis.ext_multilinear.

---

Two multilinear maps indexed by a Fintype are equal if they are equal when all arguments are basis vectors.

noncomputable def Basis.multilinearMap {ι : Type u_1} {R : Type u_2} [CommSemiring R] {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : ι → Type u_5} (b : (i : ι) → Module.Basis (κ i) R (M i)) {ι' : Type u_6} {N : Type u_7} [AddCommMonoid N] [Module R N] (b' : Module.Basis ι' R N) [Finite ι] [∀ (i : ι), Finite (κ i)] : Module.Basis (((i : ι) → κ i) × ι') R (MultilinearMap R M N)

A basis for multilinear maps given a finite basis on each domain and a basis on the codomain.

Equations

• One or more equations did not get rendered due to their size.

theorem Basis.multilinearMap_apply {ι : Type u_1} {R : Type u_2} [CommSemiring R] {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : ι → Type u_5} (b : (i : ι) → Module.Basis (κ i) R (M i)) {ι' : Type u_6} {N : Type u_7} [AddCommMonoid N] [Module R N] (b' : Module.Basis ι' R N) [Fintype ι] [(i : ι) → Fintype (κ i)] (i : ((i : ι) → κ i) × ι') : (multilinearMap b b') i = (LinearMap.id.smulRight (b' i.2)).compMultilinearMap ((MultilinearMap.mkPiRing R ι 1).compLinearMap fun (i' : ι) => (b i').coord (i.1 i'))

theorem Basis.multilinearMap_apply_apply {ι : Type u_1} {R : Type u_2} [CommSemiring R] {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : ι → Type u_5} (b : (i : ι) → Module.Basis (κ i) R (M i)) {ι' : Type u_6} {N : Type u_7} [AddCommMonoid N] [Module R N] (b' : Module.Basis ι' R N) [Fintype ι] [(i : ι) → Fintype (κ i)] (ii : ((i : ι) → κ i) × ι') (v : (i : ι) → M i) : ((multilinearMap b b') ii) v = (∏ i : ι, ((b i).repr (v i)) (ii.1 i)) • b' ii.2

The elements of the basis are the maps which scale b' ii.2 by the product of all the ii.1 · coordinates along b i.