OAI/RepresentationTheory/FoulkesHowe/PairingPerfection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.symPowDual_flip_injective_of_pure_evaluation line 13

   Source documentation

   Evaluation on pure dual powers detects the second variable of a pairing.

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

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

2. theorem OAI.Problem346.symPowDual_isPerfPair_of_pure_evaluation line 31

   Source documentation

   Pure-power evaluation identities characterize a perfect symmetric-power pairing.

   theorem symPowDual_isPerfPair_of_pure_evaluation [FiniteDimensional ℂ V] (n : ℕ)
       (B : SymPow n (Module.Dual ℂ V) →ₗ[ℂ] Module.Dual ℂ (SymPow n V))
       (hRight : ∀ (p : SymPow n (Module.Dual ℂ V)) (x : V),
         B p (symMonomial n V (fun _ => x)) =
           SymmetricAlgebra.lift (Module.Dual.eval ℂ V x) p.val)
       (hLeft : ∀ (φ : Module.Dual ℂ V) (p : SymPow n V),
         B (symMonomial n (Module.Dual ℂ V) (fun _ => φ)) p =
           SymmetricAlgebra.lift φ p.val) : B.IsPerfPair :=
   …

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