OAI/RepresentationTheory/FoulkesHowe/PairingLift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.exists_symPow_bilinear_lift line 10

   Source documentation

   Descend a separately symmetric multilinear pairing in both blocks.

   theorem exists_symPow_bilinear_lift (n m : ℕ) (V : Type u) (W : Type v)
       [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
       (Q : MultilinearMap ℂ (fun _ : Fin n => V)
         (MultilinearMap ℂ (fun _ : Fin m => W) ℂ))
       (hleft : ∀ (σ : Equiv.Perm (Fin n)) x,
         Q (fun i => x (σ i)) = Q x)
       (hright : ∀ x (σ : Equiv.Perm (Fin m)) y,
         Q x (fun i => y (σ i)) = Q x y) :
       ∃ B : SymPow n V →ₗ[ℂ] Module.Dual ℂ (SymPow m W),
         ∀ x y, B (symMonomial n V x) (symMonomial m W y) = Q x y := by
   …

   Mentions: OAI.Problem346.SymPow, OAI.Problem346.symMonomial