Documentation

LeanPool.Ado.LinearAlgebra.BilinearForm.Multilinear

Bilinear forms read off multilinear maps in two variables #

A multilinear map on the constant family fun _ : Fin 2 => V and a bilinear form on V carry the same data. This file records the direction that is used downstream: Ado.MultilinearMap.toBilinForm reads a multilinear map m as the bilinear form (x, y) ↦ m ![x, y], and two recognition lemmas say when that form 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 nested linear map can likewise be read as an AlternatingMap on Fin 2; for scalar-valued maps these two readings are inverse.

Main definitions #

Main results #

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.

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

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

Equations
  • hω.toAlternatingMap = { toFun := fun (v : Fin 2 → M) => (ω (v 0)) (v 1), map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ }
Instances For
    source
    @[simp]
    theorem LinearMap.IsAlt.toAlternatingMap_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ω : M →ₗ[R] M →ₗ[R] N} (hω : ω.IsAlt) (v : Fin 2 → M) :
    hω.toAlternatingMap v = (ω (v 0)) (v 1)

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

    source
    def Ado.MultilinearMap.toBilinForm {R : Type u_1} {V : Type u_2} [CommSemiring R] [AddCommMonoid V] [Module R V] (m : MultilinearMap R (fun (x : Fin 2) => V) R) :
    LinearMap.BilinForm R V

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

    Equations
    Instances For
      source
      @[simp]
      theorem Ado.MultilinearMap.toBilinForm_apply {R : Type u_1} {V : Type u_2} [CommSemiring R] [AddCommMonoid V] [Module R V] (m : MultilinearMap R (fun (x : Fin 2) => V) R) (x y : V) :
      ((toBilinForm m) x) y = m ![x, y]
      source
      theorem Ado.MultilinearMap.isSymm_toBilinForm {R : Type u_1} {V : Type u_2} [CommSemiring R] [AddCommMonoid V] [Module R V] {m : MultilinearMap R (fun (x : Fin 2) => V) R} (h : ∀ (x y : V), m ![y, x] = m ![x, y]) :
      (toBilinForm m).IsSymm

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

      source
      theorem Ado.MultilinearMap.isAlt_toBilinForm {R : Type u_1} {V : Type u_2} [CommSemiring R] [AddCommMonoid V] [Module R V] {m : MultilinearMap R (fun (x : Fin 2) => V) R} (h : ∀ (x : V), m ![x, x] = 0) :
      (toBilinForm m).IsAlt

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

      source
      theorem Ado.MultilinearMap.toBilinForm_injective {R : Type u_1} {V : Type u_2} [CommSemiring R] [AddCommMonoid V] [Module R V] :
      Function.Injective toBilinForm

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

      source
      @[simp]
      theorem Ado.MultilinearMap.toAlternatingMap_toBilinForm {R : Type u_1} {V : Type u_2} [CommSemiring R] [AddCommMonoid V] [Module R V] (A : V [⋀^Fin 2]→ₗ[R] R) :
      ⋯.toAlternatingMap = A

      Reading a scalar-valued alternating map as a bilinear form and back recovers the map.

      source
      @[simp]
      theorem Ado.MultilinearMap.toBilinForm_toAlternatingMap {R : Type u_1} {V : Type u_2} [CommSemiring R] [AddCommMonoid V] [Module R V] (B : LinearMap.BilinForm R V) (hB : LinearMap.IsAlt B) :
      toBilinForm ↑hB.toAlternatingMap = B

      Reading a bilinear map with zero diagonal as an alternating map and back recovers the map.