OAI/RepresentationTheory/FoulkesHowe/SymmetricPairing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem346.symPowPairing line 14

   Source documentation

   The normalized symmetric-power pairing induced by a bilinear pairing.

   def symPowPairing (n : ℕ) (B : X →ₗ[ℂ] Y →ₗ[ℂ] ℂ) :
       SymPow n X →ₗ[ℂ] Module.Dual ℂ (SymPow n Y) :=
   …

   Mentions: OAI.Problem346.SymPow

2. theorem OAI.Problem346.symPowPairing_monomial line 21
3. def OAI.Problem346.symPowDualMap line 32

   Source documentation

   The canonical pairing from the symmetric power of the dual space.

   def symPowDualMap (n : ℕ) (V : Type u) [AddCommGroup V] [Module ℂ V] :
       SymPow n (Module.Dual ℂ V) →ₗ[ℂ] Module.Dual ℂ (SymPow n V) :=
   …

   Mentions: OAI.Problem346.SymPow

4. theorem OAI.Problem346.symPowDualMap_monomial line 36
5. theorem OAI.Problem346.symPowDualMap_pure_right line 44

   Source documentation

   On pure powers, the pairing is ordinary algebra evaluation.

   theorem symPowDualMap_pure_right (n : ℕ) (V : Type u)
       [AddCommGroup V] [Module ℂ V]
       (p : SymPow n (Module.Dual ℂ V)) (x : V) :
       symPowDualMap n V p (symMonomial n V (fun _ => x)) =
         SymmetricAlgebra.lift (Module.Dual.eval ℂ V x) p.val := by
   …

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

6. theorem OAI.Problem346.symPowDualMap_pure_left line 61

   Source documentation

   The analogous pure-power evaluation in the dual variables.

   theorem symPowDualMap_pure_left (n : ℕ) (V : Type u)
       [AddCommGroup V] [Module ℂ V]
       (φ : Module.Dual ℂ V) (p : SymPow n V) :
       symPowDualMap n V (symMonomial n (Module.Dual ℂ V) (fun _ => φ)) p =
         SymmetricAlgebra.lift φ p.val := by
   …

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