OAI/RepresentationTheory/FoulkesHowe/CanonicalMap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem346.rowIndexEquiv line 10
2. def OAI.Problem346.foulkesRowFormSpanning line 22

   Source documentation

   Hold all but a single input row of the Foulkes formula fixed.

   def foulkesRowFormSpanning (a b : ℕ) (V : Type*) [AddCommGroup V] [Module ℂ V]
       (v : Fin b → Fin a → V) (j : Fin b) :
       MultilinearMap ℂ (fun _ : Fin a => V) (SymPow a (SymPow b V)) := by
   …

   Mentions: OAI.Problem346.SymPow

3. theorem OAI.Problem346.foulkesRowFormSpanning_apply line 30
4. theorem OAI.Problem346.foulkesRowFormSpanning_symmetric line 46
5. theorem OAI.Problem346.exists_foulkesMap_from_spanning line 64

   Source documentation

   The specified canonical formula defines a linear map in every bidegree.

   theorem exists_foulkesMap_from_spanning (a b : ℕ) (V : Type*)
       [AddCommGroup V] [Module ℂ V] :
       ∃ μ : SymPow b (SymPow a V) →ₗ[ℂ] SymPow a (SymPow b V),
         IsFoulkesMap a b V μ := by
   …

   Mentions: OAI.Problem346.SymPow, OAI.Problem346.IsFoulkesMap