Physlib.Mathematics.LinearMaps

Physlib
Mathematics
LinearMaps

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Mathlib.Algebra.Module.LinearMap.Defs
public import Mathlib.Data.Fintype.BigOperators
public import Physlib.Meta.TODO.Basic
public import Mathlib.Algebra.Ring.Rat

Linear maps

Some definitions and properties of linear, bilinear, and trilinear maps, along with homogeneous quadratic and cubic equations.

@[expose] public section

TODO "Replace the definitions of bi-linear maps in `./Mathematics/LinaerMaps`
  with definitions from Mathlib."

The structure defining a homogeneous quadratic equation.

@[simp]
def HomogeneousQuadratic (V : Type) [AddCommMonoid V] [Module ℚ V] : Type :=
  V →ₑ[((fun a => a ^ 2) : ℚ → ℚ)] ℚ

A homogeneous quadratic equation can be treated as a function from V to ℚ.

instance instFun : FunLike (HomogeneousQuadratic V) V ℚ where
  coe f := f.toFun
  coe_injective f g h := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:HomogeneousQuadratic Vg:HomogeneousQuadratic Vh:(fun f => f.toFun) f = (fun f => f.toFun) g⊢ f = g
    cases fmkV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vg:HomogeneousQuadratic VtoFun✝:V → ℚmap_smul'✝:∀ (m : ℚ) (x : V), toFun✝ (m • x) = m ^ 2 • toFun✝ xh:(fun f => f.toFun) { toFun := toFun✝, map_smul' := map_smul'✝ } = (fun f => f.toFun) g⊢ { toFun := toFun✝, map_smul' := map_smul'✝ } = g
    cases gmk.mkV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ VtoFun✝¹:V → ℚmap_smul'✝¹:∀ (m : ℚ) (x : V), toFun✝ (m • x) = m ^ 2 • toFun✝ xtoFun✝:V → ℚmap_smul'✝:∀ (m : ℚ) (x : V), toFun✝ (m • x) = m ^ 2 • toFun✝ xh:(fun f => f.toFun) { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } =
  (fun f => f.toFun) { toFun := toFun✝, map_smul' := map_smul'✝ }⊢ { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } = { toFun := toFun✝, map_smul' := map_smul'✝ }
    simp_allAll goals completed! 🐙

lemma map_smul (f : HomogeneousQuadratic V) (a : ℚ) (S : V) : f (a • S) = a ^ 2 * f S :=
  f.map_smul' a S

The structure of a symmetric bilinear function.

structure BiLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends V →ₗ[ℚ] V →ₗ[ℚ] ℚ where
  swap' : ∀ S T, toFun S T = toFun T S

A symmetric bilinear function.

class IsSymmetric {V : Type} [AddCommMonoid V] [Module ℚ V] (f : V →ₗ[ℚ] V →ₗ[ℚ] ℚ) : Prop where
  swap : ∀ S T, f S T = f T S

A symmetric bilinear form can be treated as a function from V to V →ₗ[ℚ] ℚ.

instance instFun (V : Type) [AddCommMonoid V] [Module ℚ V] :
    FunLike (BiLinearSymm V) V (V →ₗ[ℚ] ℚ) where
  coe f := f.toFun
  coe_injective f g h := byV✝:Typeinst✝³:AddCommMonoid V✝inst✝²:Module ℚ V✝V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm Vg:BiLinearSymm Vh:(fun f => f.toFun) f = (fun f => f.toFun) g⊢ f = g
    cases fmkV✝:Typeinst✝³:AddCommMonoid V✝inst✝²:Module ℚ V✝V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vg:BiLinearSymm VtoLinearMap✝:V →ₗ[ℚ] V →ₗ[ℚ] ℚswap'✝:∀ (S T : V), (toLinearMap✝.toFun S) T = (toLinearMap✝.toFun T) Sh:(fun f => f.toFun) { toLinearMap := toLinearMap✝, swap' := swap'✝ } = (fun f => f.toFun) g⊢ { toLinearMap := toLinearMap✝, swap' := swap'✝ } = g
    cases gmk.mkV✝:Typeinst✝³:AddCommMonoid V✝inst✝²:Module ℚ V✝V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ VtoLinearMap✝¹:V →ₗ[ℚ] V →ₗ[ℚ] ℚswap'✝¹:∀ (S T : V), (toLinearMap✝.toFun S) T = (toLinearMap✝.toFun T) StoLinearMap✝:V →ₗ[ℚ] V →ₗ[ℚ] ℚswap'✝:∀ (S T : V), (toLinearMap✝.toFun S) T = (toLinearMap✝.toFun T) Sh:(fun f => f.toFun) { toLinearMap := toLinearMap✝¹, swap' := swap'✝¹ } =
  (fun f => f.toFun) { toLinearMap := toLinearMap✝, swap' := swap'✝ }⊢ { toLinearMap := toLinearMap✝¹, swap' := swap'✝¹ } = { toLinearMap := toLinearMap✝, swap' := swap'✝ }
    simp_allAll goals completed! 🐙

The construction of a symmetric bilinear map from smul and map_add in the first factor, and swap.


@[simps!]
def mk₂ (f : V × V → ℚ) (map_smul : ∀ a S T, f (a • S, T) = a * f (S, T))
    (map_add : ∀ S1 S2 T, f (S1 + S2, T) = f (S1, T) + f (S2, T))
    (swap : ∀ S T, f (S, T) = f (T, S)) : BiLinearSymm V where
  toFun := fun S => {
    toFun := fun T => f (S, T)
    map_add' := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:V⊢ ∀ (x y : V), f (S, x + y) = f (S, x) + f (S, y)
      intro T1 T2V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:VT1:VT2:V⊢ f (S, T1 + T2) = f (S, T1) + f (S, T2)
      rw [swap,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:VT1:VT2:V⊢ f (T1 + T2, S) = f (S, T1) + f (S, T2)V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:VT1:VT2:V⊢ f (T1, S) + f (T2, S) = f (S, T1) + f (S, T2) map_addV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:VT1:VT2:V⊢ f (T1, S) + f (T2, S) = f (S, T1) + f (S, T2)V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:VT1:VT2:V⊢ f (T1, S) + f (T2, S) = f (S, T1) + f (S, T2)]V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:VT1:VT2:V⊢ f (T1, S) + f (T2, S) = f (S, T1) + f (S, T2)
      simp [swap]All goals completed! 🐙
    map_smul' := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:V⊢ ∀ (m : ℚ) (x : V), f (S, m • x) = (RingHom.id ℚ) m • f (S, x)
      intro a TV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:Va:ℚT:V⊢ f (S, a • T) = (RingHom.id ℚ) a • f (S, T)
      simp only [RingHom.id_apply, smul_eq_mul]V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:Va:ℚT:V⊢ f (S, a • T) = a * f (S, T)
      rw [swap,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:Va:ℚT:V⊢ f (a • T, S) = a * f (S, T)V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:Va:ℚT:V⊢ a * f (T, S) = a * f (S, T) map_smulV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:Va:ℚT:V⊢ a * f (T, S) = a * f (S, T)V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:Va:ℚT:V⊢ a * f (T, S) = a * f (S, T)]V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V → ℚmap_smul:∀ (a : ℚ) (S T : V), f (a • S, T) = a * f (S, T)map_add:∀ (S1 S2 T : V), f (S1 + S2, T) = f (S1, T) + f (S2, T)swap:∀ (S T : V), f (S, T) = f (T, S)S:Va:ℚT:V⊢ a * f (T, S) = a * f (S, T)
      exact congrArg (HMul.hMul a) (swap T S)All goals completed! 🐙
  }
  map_smul' := fun a S => LinearMap.ext fun T => map_smul a S T
  map_add' := fun S1 S2 => LinearMap.ext fun T => map_add S1 S2 T
  swap' := swap

              

lemma map_smul₁ (f : BiLinearSymm V) (a : ℚ) (S T : V) : f (a • S) T = a * f S T := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm Va:ℚS:VT:V⊢ (f (a • S)) T = a * (f S) T
  have h : f (a • S) = a • (f S) := by
    exact f.map_smul a SV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm Va:ℚS:VT:Vh:f (a • S) = a • f S⊢ (f (a • S)) T = a * (f S) TV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm Va:ℚS:VT:Vh:f (a • S) = a • f S⊢ (f (a • S)) T = a * (f S) T
  simp [h]All goals completed! 🐙lemma swap (f : BiLinearSymm V) (S T : V) : f S T = f T S := f.swap' S T

lemma map_smul₂ (f : BiLinearSymm V) (a : ℚ) (S : V) (T : V) : f S (a • T) = a * f S T := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm Va:ℚS:VT:V⊢ (f S) (a • T) = a * (f S) T
  rw [f.swap,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm Va:ℚS:VT:V⊢ (f (a • T)) S = a * (f S) TAll goals completed! 🐙 f.map_smul₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm Va:ℚS:VT:V⊢ a * (f T) S = a * (f S) TAll goals completed! 🐙 f.swapV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm Va:ℚS:VT:V⊢ a * (f S) T = a * (f S) TAll goals completed! 🐙]All goals completed! 🐙

lemma map_add₁ (f : BiLinearSymm V) (S1 S2 T : V) : f (S1 + S2) T = f S1 T + f S2 T := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm VS1:VS2:VT:V⊢ (f (S1 + S2)) T = (f S1) T + (f S2) T
  have h : f (S1 + S2) = f S1 + f S2 := by
    exact f.map_add S1 S2V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm VS1:VS2:VT:Vh:f (S1 + S2) = f S1 + f S2⊢ (f (S1 + S2)) T = (f S1) T + (f S2) TV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm VS1:VS2:VT:Vh:f (S1 + S2) = f S1 + f S2⊢ (f (S1 + S2)) T = (f S1) T + (f S2) T
  simp [h]All goals completed! 🐙

lemma map_add₂ (f : BiLinearSymm V) (S : V) (T1 T2 : V) :
    f S (T1 + T2) = f S T1 + f S T2 := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm VS:VT1:VT2:V⊢ (f S) (T1 + T2) = (f S) T1 + (f S) T2
  rw [f.swap,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm VS:VT1:VT2:V⊢ (f (T1 + T2)) S = (f S) T1 + (f S) T2All goals completed! 🐙 f.map_add₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm VS:VT1:VT2:V⊢ (f T1) S + (f T2) S = (f S) T1 + (f S) T2All goals completed! 🐙 f.swap T1 S,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm VS:VT1:VT2:V⊢ (f S) T1 + (f T2) S = (f S) T1 + (f S) T2All goals completed! 🐙 f.swap T2 SV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm VS:VT1:VT2:V⊢ (f S) T1 + (f S) T2 = (f S) T1 + (f S) T2All goals completed! 🐙]All goals completed! 🐙

Fixing the second input vectors, the resulting linear map.

def toLinear₁ (f : BiLinearSymm V) (T : V) : V →ₗ[ℚ] ℚ where
  toFun S := f S T
  map_add' S1 S2 := map_add₁ f S1 S2 T
  map_smul' a S := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:BiLinearSymm VT:Va:ℚS:V⊢ (f (a • S)) T = (RingHom.id ℚ) a • (f S) T simp [f.map_smul₁]All goals completed! 🐙

              lemma toLinear₁_apply (f : BiLinearSymm V) (S T : V) : f S T = f.toLinear₁ T S := rfllemma map_sum₁ {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V) :
    f (∑ i, S i) T = ∑ i, f (S i) T := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:BiLinearSymm VS:Fin n → VT:V⊢ (f (∑ i, S i)) T = ∑ i, (f (S i)) T
  simp [f.toLinear₁_apply, map_sum]All goals completed! 🐙lemma map_sum₂ {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V) :
    f T (∑ i, S i) = ∑ i, f T (S i) := map_sum (f T) S Finset.univ

The homogeneous quadratic equation obtainable from a bilinear function.

@[simps!]
def toHomogeneousQuad {V : Type} [AddCommMonoid V] [Module ℚ V]
    (τ : BiLinearSymm V) : HomogeneousQuadratic V where
  toFun S := τ S S
  map_smul' a S := byV✝:Typeinst✝³:AddCommMonoid V✝inst✝²:Module ℚ V✝V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vτ:BiLinearSymm Va:ℚS:V⊢ (τ (a • S)) (a • S) = a ^ 2 • (τ S) S
    simp only [τ.map_smul₁, τ.map_smul₂, smul_eq_mul]V✝:Typeinst✝³:AddCommMonoid V✝inst✝²:Module ℚ V✝V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vτ:BiLinearSymm Va:ℚS:V⊢ a * (a * (τ S) S) = a ^ 2 * (τ S) S
    grindAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma toHomogeneousQuad_add {V : Type} [AddCommMonoid V] [Module ℚ V]
    (τ : BiLinearSymm V) (S T : V) :
    τ.toHomogeneousQuad (S + T) = τ.toHomogeneousQuad S +
    τ.toHomogeneousQuad T + 2 * τ S T := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vτ:BiLinearSymm VS:VT:V⊢ τ.toHomogeneousQuad (S + T) = τ.toHomogeneousQuad S + τ.toHomogeneousQuad T + 2 * (τ S) T
  simp only [HomogeneousQuadratic, toHomogeneousQuad_apply, τ.map_add₁, map_add, τ.swap T S]V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vτ:BiLinearSymm VS:VT:V⊢ (τ S) S + (τ S) T + ((τ S) T + (τ T) T) = (τ S) S + (τ T) T + 2 * (τ S) T
  grindAll goals completed! 🐙

The structure of a homogeneous cubic equation.

@[simp]
def HomogeneousCubic (V : Type) [AddCommMonoid V] [Module ℚ V] : Type :=
  V →ₑ[((fun a => a ^ 3) : ℚ → ℚ)] ℚ

A homogeneous cubic equation can be treated as a function from V to ℚ.

instance instFun : FunLike (HomogeneousCubic V) V ℚ where
  coe f := f.toFun
  coe_injective f g h := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:HomogeneousCubic Vg:HomogeneousCubic Vh:(fun f => f.toFun) f = (fun f => f.toFun) g⊢ f = g
    cases fmkV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vg:HomogeneousCubic VtoFun✝:V → ℚmap_smul'✝:∀ (m : ℚ) (x : V), toFun✝ (m • x) = m ^ 3 • toFun✝ xh:(fun f => f.toFun) { toFun := toFun✝, map_smul' := map_smul'✝ } = (fun f => f.toFun) g⊢ { toFun := toFun✝, map_smul' := map_smul'✝ } = g
    cases gmk.mkV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ VtoFun✝¹:V → ℚmap_smul'✝¹:∀ (m : ℚ) (x : V), toFun✝ (m • x) = m ^ 3 • toFun✝ xtoFun✝:V → ℚmap_smul'✝:∀ (m : ℚ) (x : V), toFun✝ (m • x) = m ^ 3 • toFun✝ xh:(fun f => f.toFun) { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } =
  (fun f => f.toFun) { toFun := toFun✝, map_smul' := map_smul'✝ }⊢ { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } = { toFun := toFun✝, map_smul' := map_smul'✝ }
    simp_allAll goals completed! 🐙

lemma map_smul (f : HomogeneousCubic V) (a : ℚ) (S : V) : f (a • S) = a ^ 3 * f S :=
  f.map_smul' a S

The structure of a symmetric trilinear function.

structure TriLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends
    V →ₗ[ℚ] V →ₗ[ℚ] V →ₗ[ℚ] ℚ where
  swap₁' : ∀ S T L, toFun S T L = toFun T S L
  swap₂' : ∀ S T L, toFun S T L = toFun S L T

A symmetric trilinear form can be treated as a function from V to V →ₗ[ℚ] V →ₗ[ℚ] ℚ.

instance instFun : FunLike (TriLinearSymm V) V (V →ₗ[ℚ] V →ₗ[ℚ] ℚ) where
  coe f := f.toFun
  coe_injective f g h := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm Vg:TriLinearSymm Vh:(fun f => f.toFun) f = (fun f => f.toFun) g⊢ f = g
    cases fmkV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vg:TriLinearSymm VtoLinearMap✝:V →ₗ[ℚ] V →ₗ[ℚ] V →ₗ[ℚ] ℚswap₁'✝:∀ (S T L : V), ((toLinearMap✝.toFun S) T) L = ((toLinearMap✝.toFun T) S) Lswap₂'✝:∀ (S T L : V), ((toLinearMap✝.toFun S) T) L = ((toLinearMap✝.toFun S) L) Th:(fun f => f.toFun) { toLinearMap := toLinearMap✝, swap₁' := swap₁'✝, swap₂' := swap₂'✝ } = (fun f => f.toFun) g⊢ { toLinearMap := toLinearMap✝, swap₁' := swap₁'✝, swap₂' := swap₂'✝ } = g
    cases gmk.mkV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ VtoLinearMap✝¹:V →ₗ[ℚ] V →ₗ[ℚ] V →ₗ[ℚ] ℚswap₁'✝¹:∀ (S T L : V), ((toLinearMap✝.toFun S) T) L = ((toLinearMap✝.toFun T) S) Lswap₂'✝¹:∀ (S T L : V), ((toLinearMap✝.toFun S) T) L = ((toLinearMap✝.toFun S) L) TtoLinearMap✝:V →ₗ[ℚ] V →ₗ[ℚ] V →ₗ[ℚ] ℚswap₁'✝:∀ (S T L : V), ((toLinearMap✝.toFun S) T) L = ((toLinearMap✝.toFun T) S) Lswap₂'✝:∀ (S T L : V), ((toLinearMap✝.toFun S) T) L = ((toLinearMap✝.toFun S) L) Th:(fun f => f.toFun) { toLinearMap := toLinearMap✝¹, swap₁' := swap₁'✝¹, swap₂' := swap₂'✝¹ } =
  (fun f => f.toFun) { toLinearMap := toLinearMap✝, swap₁' := swap₁'✝, swap₂' := swap₂'✝ }⊢ { toLinearMap := toLinearMap✝¹, swap₁' := swap₁'✝¹, swap₂' := swap₂'✝¹ } =
  { toLinearMap := toLinearMap✝, swap₁' := swap₁'✝, swap₂' := swap₂'✝ }
    simp_allAll goals completed! 🐙

The construction of a symmetric trilinear map from smul and map_add in the first factor, and two swap.


@[simps!]
def mk₃ (f : V × V × V→ ℚ) (map_smul : ∀ a S T L, f (a • S, T, L) = a * f (S, T, L))
    (map_add : ∀ S1 S2 T L, f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L))
    (swap₁ : ∀ S T L, f (S, T, L) = f (T, S, L))
    (swap₂ : ∀ S T L, f (S, T, L) = f (S, L, T)) : TriLinearSymm V where
  toFun := fun S => (BiLinearSymm.mk₂ (fun T => f (S, T))
    (byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:V⊢ ∀ (a : ℚ) (S_1 T : V), f (S, a • S_1, T) = a * f (S, S_1, T)
      intro a T LV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:Va:ℚT:VL:V⊢ f (S, a • T, L) = a * f (S, T, L)
      rw [swap₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:Va:ℚT:VL:V⊢ f (a • T, S, L) = a * f (S, T, L)All goals completed! 🐙 map_smul,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:Va:ℚT:VL:V⊢ a * f (T, S, L) = a * f (S, T, L)All goals completed! 🐙 swap₁V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:Va:ℚT:VL:V⊢ a * f (S, T, L) = a * f (S, T, L)All goals completed! 🐙]All goals completed! 🐙)
    (byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:V⊢ ∀ (S1 S2 T : V), f (S, S1 + S2, T) = f (S, S1, T) + f (S, S2, T)
      intro S1 S2 TV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:VS1:VS2:VT:V⊢ f (S, S1 + S2, T) = f (S, S1, T) + f (S, S2, T)
      rw [swap₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:VS1:VS2:VT:V⊢ f (S1 + S2, S, T) = f (S, S1, T) + f (S, S2, T)All goals completed! 🐙 map_add,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:VS1:VS2:VT:V⊢ f (S1, S, T) + f (S2, S, T) = f (S, S1, T) + f (S, S2, T)All goals completed! 🐙 swap₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:VS1:VS2:VT:V⊢ f (S, S1, T) + f (S2, S, T) = f (S, S1, T) + f (S, S2, T)All goals completed! 🐙 swap₁ S2 S TV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:VS1:VS2:VT:V⊢ f (S, S1, T) + f (S, S2, T) = f (S, S1, T) + f (S, S2, T)All goals completed! 🐙]All goals completed! 🐙)
    (byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:V × V × V → ℚmap_smul:∀ (a : ℚ) (S T L : V), f (a • S, T, L) = a * f (S, T, L)map_add:∀ (S1 S2 T L : V), f (S1 + S2, T, L) = f (S1, T, L) + f (S2, T, L)swap₁:∀ (S T L : V), f (S, T, L) = f (T, S, L)swap₂:∀ (S T L : V), f (S, T, L) = f (S, L, T)S:V⊢ ∀ (S_1 T : V), f (S, S_1, T) = f (S, T, S_1) exact fun L T ↦ swap₂ S L TAll goals completed! 🐙)).toLinearMap
  map_add' S1 S2 := LinearMap.ext fun T ↦ LinearMap.ext fun L => map_add S1 S2 T L
  map_smul' a S :=
    LinearMap.ext fun T => LinearMap.ext fun L => map_smul a S T L
  swap₁' := swap₁
  swap₂' := swap₂

              lemma swap₁ (f : TriLinearSymm V) (S T L : V) : f S T L = f T S L :=
  f.swap₁' S T Llemma swap₂ (f : TriLinearSymm V) (S T L : V) : f S T L = f S L T :=
  f.swap₂' S T L

lemma swap₃ (f : TriLinearSymm V) (S T L : V) : f S T L = f L T S := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:VL:V⊢ ((f S) T) L = ((f L) T) S
  rw [f.swap₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:VL:V⊢ ((f T) S) L = ((f L) T) SAll goals completed! 🐙 f.swap₂,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:VL:V⊢ ((f T) L) S = ((f L) T) SAll goals completed! 🐙 f.swap₁V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:VL:V⊢ ((f L) T) S = ((f L) T) SAll goals completed! 🐙]All goals completed! 🐙

lemma map_smul₁ (f : TriLinearSymm V) (a : ℚ) (S T L : V) :
    f (a • S) T L = a * f S T L := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm Va:ℚS:VT:VL:V⊢ ((f (a • S)) T) L = a * ((f S) T) L
  have h : f (a • S) = a • (f S) := by
    exact f.map_smul a SV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm Va:ℚS:VT:VL:Vh:f (a • S) = a • f S⊢ ((f (a • S)) T) L = a * ((f S) T) LV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm Va:ℚS:VT:VL:Vh:f (a • S) = a • f S⊢ ((f (a • S)) T) L = a * ((f S) T) L
  simp [h]All goals completed! 🐙

lemma map_smul₂ (f : TriLinearSymm V) (S : V) (a : ℚ) (T L : V) :
    f S (a • T) L = a * f S T L := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:Va:ℚT:VL:V⊢ ((f S) (a • T)) L = a * ((f S) T) L
  rw [f.swap₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:Va:ℚT:VL:V⊢ ((f (a • T)) S) L = a * ((f S) T) LAll goals completed! 🐙 f.map_smul₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:Va:ℚT:VL:V⊢ a * ((f T) S) L = a * ((f S) T) LAll goals completed! 🐙 f.swap₁V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:Va:ℚT:VL:V⊢ a * ((f S) T) L = a * ((f S) T) LAll goals completed! 🐙]All goals completed! 🐙

lemma map_smul₃ (f : TriLinearSymm V) (S T : V) (a : ℚ) (L : V) :
    f S T (a • L) = a * f S T L := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:Va:ℚL:V⊢ ((f S) T) (a • L) = a * ((f S) T) L
  rw [f.swap₃,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:Va:ℚL:V⊢ ((f (a • L)) T) S = a * ((f S) T) LAll goals completed! 🐙 f.map_smul₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:Va:ℚL:V⊢ a * ((f L) T) S = a * ((f S) T) LAll goals completed! 🐙 f.swap₃V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:Va:ℚL:V⊢ a * ((f S) T) L = a * ((f S) T) LAll goals completed! 🐙]All goals completed! 🐙

lemma map_add₁ (f : TriLinearSymm V) (S1 S2 T L : V) :
    f (S1 + S2) T L = f S1 T L + f S2 T L := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS1:VS2:VT:VL:V⊢ ((f (S1 + S2)) T) L = ((f S1) T) L + ((f S2) T) L
  have h : f (S1 + S2) = f S1 + f S2 := by
    exact f.map_add S1 S2V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS1:VS2:VT:VL:Vh:f (S1 + S2) = f S1 + f S2⊢ ((f (S1 + S2)) T) L = ((f S1) T) L + ((f S2) T) LV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS1:VS2:VT:VL:Vh:f (S1 + S2) = f S1 + f S2⊢ ((f (S1 + S2)) T) L = ((f S1) T) L + ((f S2) T) L
  simp [h]All goals completed! 🐙

lemma map_add₂ (f : TriLinearSymm V) (S T1 T2 L : V) :
    f S (T1 + T2) L = f S T1 L + f S T2 L := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT1:VT2:VL:V⊢ ((f S) (T1 + T2)) L = ((f S) T1) L + ((f S) T2) L
  rw [f.swap₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT1:VT2:VL:V⊢ ((f (T1 + T2)) S) L = ((f S) T1) L + ((f S) T2) LAll goals completed! 🐙 f.map_add₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT1:VT2:VL:V⊢ ((f T1) S) L + ((f T2) S) L = ((f S) T1) L + ((f S) T2) LAll goals completed! 🐙 f.swap₁ S T1,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT1:VT2:VL:V⊢ ((f T1) S) L + ((f T2) S) L = ((f T1) S) L + ((f S) T2) LAll goals completed! 🐙 f.swap₁ S T2V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT1:VT2:VL:V⊢ ((f T1) S) L + ((f T2) S) L = ((f T1) S) L + ((f T2) S) LAll goals completed! 🐙]All goals completed! 🐙

lemma map_add₃ (f : TriLinearSymm V) (S T L1 L2 : V) :
    f S T (L1 + L2) = f S T L1 + f S T L2 := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:VL1:VL2:V⊢ ((f S) T) (L1 + L2) = ((f S) T) L1 + ((f S) T) L2
  rw [f.swap₃,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:VL1:VL2:V⊢ ((f (L1 + L2)) T) S = ((f S) T) L1 + ((f S) T) L2All goals completed! 🐙 f.map_add₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:VL1:VL2:V⊢ ((f L1) T) S + ((f L2) T) S = ((f S) T) L1 + ((f S) T) L2All goals completed! 🐙 f.swap₃,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:VL1:VL2:V⊢ ((f S) T) L1 + ((f L2) T) S = ((f S) T) L1 + ((f S) T) L2All goals completed! 🐙 f.swap₃ L2 T SV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VS:VT:VL1:VL2:V⊢ ((f S) T) L1 + ((f S) T) L2 = ((f S) T) L1 + ((f S) T) L2All goals completed! 🐙]All goals completed! 🐙

Fixing the second and third input vectors, the resulting linear map.

def toLinear₁ (f : TriLinearSymm V) (T L : V) : V →ₗ[ℚ] ℚ where
  toFun S := f S T L
  map_add' S1 S2 := map_add₁ f S1 S2 T L
  map_smul' a S := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VT:VL:Va:ℚS:V⊢ ((f (a • S)) T) L = (RingHom.id ℚ) a • ((f S) T) L
    simp only [f.map_smul₁]V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vf:TriLinearSymm VT:VL:Va:ℚS:V⊢ a * ((f S) T) L = (RingHom.id ℚ) a • ((f S) T) L
    rflAll goals completed! 🐙

              lemma toLinear₁_apply (f : TriLinearSymm V) (S T L : V) : f S T L = f.toLinear₁ T L S := rfl

lemma map_sum₁ {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T : V) (L : V) :
    f (∑ i, S i) T L = ∑ i, f (S i) T L := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ((f (∑ i, S i)) T) L = ∑ i, ((f (S i)) T) L
  rw [f.toLinear₁_apply,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ (f.toLinear₁ T L) (∑ i, S i) = ∑ i, ((f (S i)) T) LV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ∑ x, (f.toLinear₁ T L) (S x) = ∑ i, ((f (S i)) T) L map_sumV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ∑ x, (f.toLinear₁ T L) (S x) = ∑ i, ((f (S i)) T) LV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ∑ x, (f.toLinear₁ T L) (S x) = ∑ i, ((f (S i)) T) L]V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ∑ x, (f.toLinear₁ T L) (S x) = ∑ i, ((f (S i)) T) L
  rflAll goals completed! 🐙

lemma map_sum₂ {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T : V) (L : V) :
    f T (∑ i, S i) L = ∑ i, f T (S i) L := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ((f T) (∑ i, S i)) L = ∑ i, ((f T) (S i)) L
  rw [swap₁,V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ((f (∑ i, S i)) T) L = ∑ i, ((f T) (S i)) LV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ∑ i, ((f (S i)) T) L = ∑ i, ((f T) (S i)) L map_sum₁V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ∑ i, ((f (S i)) T) L = ∑ i, ((f T) (S i)) LV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ∑ i, ((f (S i)) T) L = ∑ i, ((f T) (S i)) L]V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn:ℕf:TriLinearSymm VS:Fin n → VT:VL:V⊢ ∑ i, ((f (S i)) T) L = ∑ i, ((f T) (S i)) L
  refine Fintype.sum_congr _ _ fun _ ↦ swap₁ f (S _) T LAll goals completed! 🐙lemma map_sum₃ {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T : V) (L : V) :
    f T L (∑ i, S i) = ∑ i, f T L (S i) := map_sum ((f T) L) S Finset.univ

lemma map_sum₁₂₃ {n1 n2 n3 : ℕ} (f : TriLinearSymm V) (S : Fin n1 → V)
    (T : Fin n2 → V) (L : Fin n3 → V) :
    f (∑ i, S i) (∑ i, T i) (∑ i, L i) = ∑ i, ∑ k, ∑ l, f (S i) (T k) (L l) := byV:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn1:ℕn2:ℕn3:ℕf:TriLinearSymm VS:Fin n1 → VT:Fin n2 → VL:Fin n3 → V⊢ ((f (∑ i, S i)) (∑ i, T i)) (∑ i, L i) = ∑ i, ∑ k, ∑ l, ((f (S i)) (T k)) (L l)
  rw [map_sum₁V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn1:ℕn2:ℕn3:ℕf:TriLinearSymm VS:Fin n1 → VT:Fin n2 → VL:Fin n3 → V⊢ ∑ i, ((f (S i)) (∑ i, T i)) (∑ i, L i) = ∑ i, ∑ k, ∑ l, ((f (S i)) (T k)) (L l)V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn1:ℕn2:ℕn3:ℕf:TriLinearSymm VS:Fin n1 → VT:Fin n2 → VL:Fin n3 → V⊢ ∑ i, ((f (S i)) (∑ i, T i)) (∑ i, L i) = ∑ i, ∑ k, ∑ l, ((f (S i)) (T k)) (L l)]V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn1:ℕn2:ℕn3:ℕf:TriLinearSymm VS:Fin n1 → VT:Fin n2 → VL:Fin n3 → V⊢ ∑ i, ((f (S i)) (∑ i, T i)) (∑ i, L i) = ∑ i, ∑ k, ∑ l, ((f (S i)) (T k)) (L l)
  apply Fintype.sum_congr _ _ fun _ ↦ ?_V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn1:ℕn2:ℕn3:ℕf:TriLinearSymm VS:Fin n1 → VT:Fin n2 → VL:Fin n3 → Vx✝:Fin n1⊢ ((f (S x✝)) (∑ i, T i)) (∑ i, L i) = ∑ k, ∑ l, ((f (S x✝)) (T k)) (L l)
  rw [map_sum₂V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn1:ℕn2:ℕn3:ℕf:TriLinearSymm VS:Fin n1 → VT:Fin n2 → VL:Fin n3 → Vx✝:Fin n1⊢ ∑ i, ((f (S x✝)) (T i)) (∑ i, L i) = ∑ k, ∑ l, ((f (S x✝)) (T k)) (L l)V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn1:ℕn2:ℕn3:ℕf:TriLinearSymm VS:Fin n1 → VT:Fin n2 → VL:Fin n3 → Vx✝:Fin n1⊢ ∑ i, ((f (S x✝)) (T i)) (∑ i, L i) = ∑ k, ∑ l, ((f (S x✝)) (T k)) (L l)]V:Typeinst✝¹:AddCommMonoid Vinst✝:Module ℚ Vn1:ℕn2:ℕn3:ℕf:TriLinearSymm VS:Fin n1 → VT:Fin n2 → VL:Fin n3 → Vx✝:Fin n1⊢ ∑ i, ((f (S x✝)) (T i)) (∑ i, L i) = ∑ k, ∑ l, ((f (S x✝)) (T k)) (L l)
  exact Fintype.sum_congr _ _ fun _ ↦ map_sum₃ f L (S _) (T _)All goals completed! 🐙

The homogeneous cubic equation obtainable from a symmetric trilinear function.


@[simps!]
def toCubic {charges : Type} [AddCommMonoid charges] [Module ℚ charges]
    (τ : TriLinearSymm charges) : HomogeneousCubic charges where
  toFun S := τ S S S
  map_smul' a S := byV:Typeinst✝³:AddCommMonoid Vinst✝²:Module ℚ Vcharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesa:ℚS:charges⊢ ((τ (a • S)) (a • S)) (a • S) = a ^ 3 • ((τ S) S) S
    simp only [smul_eq_mul]V:Typeinst✝³:AddCommMonoid Vinst✝²:Module ℚ Vcharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesa:ℚS:charges⊢ ((τ (a • S)) (a • S)) (a • S) = a ^ 3 * ((τ S) S) S
    rw [τ.map_smul₁,V:Typeinst✝³:AddCommMonoid Vinst✝²:Module ℚ Vcharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesa:ℚS:charges⊢ a * ((τ S) (a • S)) (a • S) = a ^ 3 * ((τ S) S) SV:Typeinst✝³:AddCommMonoid Vinst✝²:Module ℚ Vcharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesa:ℚS:charges⊢ a * (a * (a * ((τ S) S) S)) = a ^ 3 * ((τ S) S) S τ.map_smul₂,V:Typeinst✝³:AddCommMonoid Vinst✝²:Module ℚ Vcharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesa:ℚS:charges⊢ a * (a * ((τ S) S) (a • S)) = a ^ 3 * ((τ S) S) SV:Typeinst✝³:AddCommMonoid Vinst✝²:Module ℚ Vcharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesa:ℚS:charges⊢ a * (a * (a * ((τ S) S) S)) = a ^ 3 * ((τ S) S) S τ.map_smul₃V:Typeinst✝³:AddCommMonoid Vinst✝²:Module ℚ Vcharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesa:ℚS:charges⊢ a * (a * (a * ((τ S) S) S)) = a ^ 3 * ((τ S) S) SV:Typeinst✝³:AddCommMonoid Vinst✝²:Module ℚ Vcharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesa:ℚS:charges⊢ a * (a * (a * ((τ S) S) S)) = a ^ 3 * ((τ S) S) S]V:Typeinst✝³:AddCommMonoid Vinst✝²:Module ℚ Vcharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesa:ℚS:charges⊢ a * (a * (a * ((τ S) S) S)) = a ^ 3 * ((τ S) S) S
    grindAll goals completed! 🐙



set_option backward.isDefEq.respectTransparency false in
lemma toCubic_add {charges : Type} [AddCommMonoid charges] [Module ℚ charges]
    (τ : TriLinearSymm charges) (S T : charges) :
    τ.toCubic (S + T) = τ.toCubic S +
    τ.toCubic T + 3 * τ S S T + 3 * τ T T S := bycharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ τ.toCubic (S + T) = τ.toCubic S + τ.toCubic T + 3 * ((τ S) S) T + 3 * ((τ T) T) S
  simp only [HomogeneousCubic, toCubic_apply]charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ (S + T)) (S + T)) (S + T) = ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S
  rw [τ.map_add₁,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) (S + T)) (S + T) + ((τ T) (S + T)) (S + T) = ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.map_add₂,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) (S + T) + ((τ S) T) (S + T) + ((τ T) (S + T)) (S + T) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.map_add₂,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) (S + T) + ((τ S) T) (S + T) + (((τ T) S) (S + T) + ((τ T) T) (S + T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.map_add₃,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + ((τ S) T) (S + T) + (((τ T) S) (S + T) + ((τ T) T) (S + T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.map_add₃,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) (S + T) + ((τ T) T) (S + T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.map_add₃,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + ((τ T) T) (S + T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.map_add₃charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S]charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) T) S + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S
  rw [τ.swap₂ S T S,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ S) T) T) + (((τ T) S) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ T) T) S) + (((τ S) S) T + ((τ T) T) S + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.swap₁ T S S,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ S) T) T) + (((τ S) T) S + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ T) T) S) + (((τ S) S) T + ((τ T) T) S + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.swap₂ S T S,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ S) T) T) + (((τ S) S) T + ((τ T) S) T + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ T) T) S) + (((τ S) S) T + ((τ T) T) S + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.swap₂ T S T,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ S) T) T) + (((τ S) S) T + ((τ T) T) S + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ T) T) S) + (((τ S) S) T + ((τ T) T) S + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.swap₁ S T T,charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ T) S) T) + (((τ S) S) T + ((τ T) T) S + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ T) T) S) + (((τ S) S) T + ((τ T) T) S + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S τ.swap₂ T S Tcharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ T) T) S) + (((τ S) S) T + ((τ T) T) S + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) Scharges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ T) T) S) + (((τ S) S) T + ((τ T) T) S + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S]charges:Typeinst✝¹:AddCommMonoid chargesinst✝:Module ℚ chargesτ:TriLinearSymm chargesS:chargesT:charges⊢ ((τ S) S) S + ((τ S) S) T + (((τ S) S) T + ((τ T) T) S) + (((τ S) S) T + ((τ T) T) S + (((τ T) T) S + ((τ T) T) T)) =
  ((τ S) S) S + ((τ T) T) T + 3 * ((τ S) S) T + 3 * ((τ T) T) S
  grindAll goals completed! 🐙