Documentation

TauCeti.LinearAlgebra.BilinearForm.Squares

Bilinear forms from functionals on the second symmetric and exterior powers #

A functional on Sym²V becomes a bilinear form on V by composing with the universal multilinear map, and the form it produces is symmetric because the symmetric square does not see the order of its two arguments; a functional on ⋀²V becomes a form in the same way, and that form is alternating because a repeated argument wedges to zero. Both assignments are injective: the pure tensors span the symmetric square, and on the exterior side the passage from a functional to an alternating map is Mathlib's universal property, an equivalence.

Nothing here is representation theory: this is the dictionary that TauCeti.RepresentationTheory.CharacterTable.FrobeniusSchur.Trichotomy runs the invariants of the two squares through to reach invariant forms. The symmetric side is available over a commutative semiring, the exterior side over a commutative ring, which is where Mathlib's exterior power lives.

Main definitions #

Main results #

Implementation notes #

The two maps are built as plain linear maps rather than as equivalences onto the symmetric and the alternating forms. On the exterior side that equivalence is available: ofExteriorSquareDual is exteriorPower.alternatingMapLinearEquiv, the universal property of the exterior power, followed by TauCeti.MultilinearMap.toBilinForm, and its injectivity is the injectivity of that equivalence. On the symmetric side Mathlib has no universal property of the symmetric power -- it is an explicit TODO of Mathlib/LinearAlgebra/TensorPower/Symmetric.lean -- so surjectivity onto the symmetric forms is not proved here; injectivity is read off the pure tensors spanning instead, and is all the downstream counting needs.

source
noncomputable def TauCeti.BilinForm.ofSymmetricSquareDual {V : Type u_1} {k : Type} [CommSemiring k] [AddCommMonoid V] [Module k V] :
Module.Dual k (SymmetricPower k (Fin 2) V) →ₗ[k] LinearMap.BilinForm k V

A functional on the second symmetric power of V, read as a bilinear form on V.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.BilinForm.ofSymmetricSquareDual_apply {V : Type u_1} {k : Type} [CommSemiring k] [AddCommMonoid V] [Module k V] (ψ : Module.Dual k (SymmetricPower k (Fin 2) V)) (x y : V) :
    ((ofSymmetricSquareDual ψ) x) y = ψ ((SymmetricPower.tprod k) ![x, y])
    source
    theorem TauCeti.BilinForm.isSymm_ofSymmetricSquareDual {V : Type u_1} {k : Type} [CommSemiring k] [AddCommMonoid V] [Module k V] (ψ : Module.Dual k (SymmetricPower k (Fin 2) V)) :
    (ofSymmetricSquareDual ψ).IsSymm

    The form of a functional on the symmetric square is symmetric: the symmetric square does not see the order of the two arguments.

    source
    theorem TauCeti.BilinForm.ofSymmetricSquareDual_injective {V : Type u_1} {k : Type} [CommSemiring k] [AddCommMonoid V] [Module k V] :
    Function.Injective ⇑ofSymmetricSquareDual

    A functional on the symmetric square is determined by the form it gives. The pure tensors tprod ![x, y] span the symmetric square, and the values of the form are exactly the values of the functional on those, so two functionals with the same form agree on a spanning set.

    source
    noncomputable def TauCeti.BilinForm.ofExteriorSquareDual {V : Type u_1} {k : Type u_2} [CommRing k] [AddCommGroup V] [Module k V] :
    Module.Dual k ↥(⋀[k]^2 V) →ₗ[k] LinearMap.BilinForm k V

    A functional on the second exterior power of V, read as a bilinear form on V. It is the alternating map the universal property of ⋀[k]^2 V attaches to the functional, read as a form.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.BilinForm.ofExteriorSquareDual_apply {V : Type u_1} {k : Type u_2} [CommRing k] [AddCommGroup V] [Module k V] (ψ : Module.Dual k ↥(⋀[k]^2 V)) (x y : V) :
      ((ofExteriorSquareDual ψ) x) y = ψ ((exteriorPower.ιMulti k 2) ![x, y])
      source
      theorem TauCeti.BilinForm.isAlt_ofExteriorSquareDual {V : Type u_1} {k : Type u_2} [CommRing k] [AddCommGroup V] [Module k V] (ψ : Module.Dual k ↥(⋀[k]^2 V)) :
      (ofExteriorSquareDual ψ).IsAlt

      The form of a functional on the exterior square is alternating: a repeated argument wedges to zero.

      source
      theorem TauCeti.BilinForm.ofExteriorSquareDual_injective {V : Type u_1} {k : Type u_2} [CommRing k] [AddCommGroup V] [Module k V] :
      Function.Injective ⇑ofExteriorSquareDual

      A functional on the exterior square is determined by the form it gives. A functional is the alternating map the universal property attaches to it, and that map is the form.