OAI/RepresentationTheory/FoulkesHowe/Surjectivity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.canonical_surjective_unique_of_vanishing line 10

   Source documentation

   Existence, surjectivity, and uniqueness reduce entirely to the vanishing theorem.

   theorem canonical_surjective_unique_of_vanishing (a b : ℕ) (V : Type*)
       [AddCommGroup V] [Module ℂ V]
       (hvan : ∀ T : SymmetricMultilinearForm a b V,
         IsSymmetricMultilinearForm a b V T →
         (∀ u : Fin b → V, T (fun _ => symMonomial b V u) = 0) → T = 0) :
       ∃ μ : SymPow b (SymPow a V) →ₗ[ℂ] SymPow a (SymPow b V),
         IsFoulkesMap a b V μ ∧ Function.Surjective μ ∧
         ∀ ν : SymPow b (SymPow a V) →ₗ[ℂ] SymPow a (SymPow b V),
           IsFoulkesMap a b V ν → ν = μ := by
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.IsSymmetricMultilinearForm, OAI.Problem346.symMonomial, OAI.Problem346.SymPow, OAI.Problem346.IsFoulkesMap