Bilinear maps read off multilinear maps in two variables

A multilinear map on the constant family fun _ : Fin 2 => V and a bilinear map on V carry the same data. This file records the direction that is used downstream: MultilinearMap.toBilinMap reads a multilinear map m as the bilinear map (x, y) ↦ m ![x, y], and two recognition lemmas say when that map is symmetric or alternating.

The point of the construction is that the maps out of a second symmetric or exterior power are multilinear in exactly this sense, so a functional on Sym²V or on ⋀²V becomes a bilinear form on V by composing with the universal multilinear map. That is what TauCeti/LinearAlgebra/BilinearForm/Squares.lean builds on this file. An alternating bilinear map can likewise be read as an AlternatingMap on Fin 2, and these two readings are inverse.

Main definitions

• MultilinearMap.toBilinMap: the bilinear map (x, y) ↦ m ![x, y] of a multilinear map m in two variables.
• LinearMap.IsAlt.toAlternatingMap: an alternating bilinear map read as an alternating map on two arguments.

Main results

• MultilinearMap.isSymm_toBilinMap: the scalar-valued form is symmetric when m is unchanged by swapping its two arguments.
• MultilinearMap.isAlt_toBilinMap: the map is alternating when m vanishes on a repeated argument; AlternatingMap.isAlt_toBilinMap specializes this to alternating maps.
• MultilinearMap.toBilinMap_injective: the other half of "the same data" -- the bilinear map determines the multilinear map.
• AlternatingMap.toAlternatingMap_isAlt_toBilinMap and LinearMap.IsAlt.toBilinMap_toAlternatingMap: the two round trips between alternating maps on Fin 2 and alternating bilinear maps.

Implementation notes

Bilinearity is Mathlib's MultilinearMap.cons_add and cons_smul at the first argument and MultilinearMap.snoc_add and snoc_smul at the second, since ![x, y] is both Fin.cons x ![y] and Fin.snoc ![x] y. Feeding those four facts to LinearMap.mk₂ keeps the four linearity goals stated in the ![·, ·] notation, so none of them has to be massaged into the nested form a bare LinearMap constructor would present.

def LinearMap.IsAlt.toAlternatingMap {R : Type u_1} {V : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid N] [Module R N] {ω : V →ₗ[R] V →ₗ[R] N} (hω : ω.IsAlt) : V [⋀^Fin 2]→ₗ[R] N

An alternating bilinear map read as an alternating map in two arguments.

@[simp]

theorem LinearMap.IsAlt.toAlternatingMap_apply {R : Type u_1} {V : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid N] [Module R N] {ω : V →ₗ[R] V →ₗ[R] N} (hω : ω.IsAlt) (v : Fin 2 → V) : hω.toAlternatingMap v = (ω (v 0)) (v 1)

Evaluating the alternating map recovers the original bilinear map on the two arguments.

def MultilinearMap.toBilinMap {R : Type u_1} {V : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid N] [Module R N] (m : (Fin 2 → V) →ₘₗ[R] N) : LinearMap.BilinMap R V N

The bilinear map (x, y) ↦ m ![x, y] of a multilinear map m in two variables.

@[simp]

theorem MultilinearMap.toBilinMap_apply {R : Type u_1} {V : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid N] [Module R N] (m : (Fin 2 → V) →ₘₗ[R] N) (x y : V) : (m.toBilinMap x) y = m ![x, y]

theorem MultilinearMap.isSymm_toBilinMap {R : Type u_1} {V : Type u_2} [CommSemiring R] [AddCommMonoid V] [Module R V] {m : (Fin 2 → V) →ₘₗ[R] R} (h : ∀ (x y : V), m ![y, x] = m ![x, y]) : LinearMap.BilinForm.IsSymm m.toBilinMap

The form of a scalar-valued multilinear map that is unchanged by swapping its two arguments is symmetric.

theorem MultilinearMap.isAlt_toBilinMap {R : Type u_1} {V : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid N] [Module R N] {m : (Fin 2 → V) →ₘₗ[R] N} (h : ∀ (x : V), m ![x, x] = 0) : LinearMap.IsAlt m.toBilinMap

The bilinear map of a multilinear map that vanishes on a repeated argument is alternating.

theorem MultilinearMap.toBilinMap_injective {R : Type u_1} {V : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid N] [Module R N] : Function.Injective toBilinMap

A multilinear map in two variables is determined by its bilinear map. Every argument of m is a ![x, y], and the bilinear map records the value of m there.

theorem AlternatingMap.isAlt_toBilinMap {R : Type u_1} {V : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid N] [Module R N] (A : V [⋀^Fin 2]→ₗ[R] N) : LinearMap.IsAlt (↑A).toBilinMap

The bilinear map of an alternating map in two arguments is alternating.

@[simp]

theorem AlternatingMap.toAlternatingMap_isAlt_toBilinMap {R : Type u_1} {V : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid N] [Module R N] (A : V [⋀^Fin 2]→ₗ[R] N) : ⋯.toAlternatingMap = A

Reading an alternating map in two arguments as a bilinear map and back recovers the map.

@[simp]

theorem LinearMap.IsAlt.toBilinMap_toAlternatingMap {R : Type u_1} {V : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid N] [Module R N] {B : V →ₗ[R] V →ₗ[R] N} (hB : B.IsAlt) : (↑hB.toAlternatingMap).toBilinMap = B

Reading an alternating bilinear map as an alternating map and back recovers the map.