OAI/RepresentationTheory/FoulkesHowe/Annihilator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.IsFoulkesMap.surjective_of_vanishing line 14

   Source documentation

   The diagonal vanishing criterion forces every canonical Foulkes map to be surjective. This dual separation argument does not require finite dimension.

   theorem IsFoulkesMap.surjective_of_vanishing (a b : ℕ) (V : Type u)
       [AddCommGroup V] [Module ℂ V]
       (μ : SymPow b (SymPow a V) →ₗ[ℂ] SymPow a (SymPow b V))
       (hμ : IsFoulkesMap a b 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) :
       Function.Surjective μ := by
   …

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