OAI/RepresentationTheory/FoulkesHowe/SymmetricDual.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.symPowDual_injective_of_pure_evaluation line 14

   Source documentation

   A symmetric-power duality map is injective as soon as evaluation on pure powers agrees with evaluation in the symmetric algebra.

   theorem symPowDual_injective_of_pure_evaluation (n : ℕ)
       (B : SymPow n (Module.Dual ℂ V) →ₗ[ℂ] Module.Dual ℂ (SymPow n V))
       (hB : ∀ (p : SymPow n (Module.Dual ℂ V)) (x : V),
         B p (symMonomial n V (fun _ => x)) =
           SymmetricAlgebra.lift (Module.Dual.eval ℂ V x) p.val) :
       Function.Injective B := by
   …

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