OAI/RepresentationTheory/FoulkesHowe/Actions.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.map_foulkesFormula_of_isPlethysmAction line 14

   Source documentation

   Any map with the prescribed plethysm action carries the Foulkes formula to the formula on the transformed vector array.

   theorem map_foulkesFormula_of_isPlethysmAction
       {a b : ℕ} {g : V ≃ₗ[ℂ] V}
       {L : SymPow a (SymPow b V) →ₗ[ℂ] SymPow a (SymPow b V)}
       (hL : IsPlethysmAction a b V g L) (v : Fin b → Fin a → V) :
       L (foulkesFormula a b V v) =
         foulkesFormula a b V (fun j i => g (v j i)) := by
   …

   Mentions: OAI.Problem346.SymPow, OAI.Problem346.IsPlethysmAction, OAI.Problem346.foulkesFormula

2. def OAI.Problem346.plethysmEquiv line 29

   Source documentation

   The canonical action of a linear automorphism on a plethysm.

   def plethysmEquiv (outer inner : ℕ) (g : V ≃ₗ[ℂ] V) :
       SymPow outer (SymPow inner V) ≃ₗ[ℂ] SymPow outer (SymPow inner V) :=
   …

   Mentions: OAI.Problem346.SymPow

3. def OAI.Problem346.plethysmAction line 34

   Source documentation

   The underlying endomorphism of the canonical plethysm action.

   def plethysmAction (outer inner : ℕ) (g : V ≃ₗ[ℂ] V) :
       SymPow outer (SymPow inner V) →ₗ[ℂ] SymPow outer (SymPow inner V) :=
   …

   Mentions: OAI.Problem346.SymPow

4. theorem OAI.Problem346.plethysmAction_symMonomial line 38
5. theorem OAI.Problem346.plethysmAction_isPlethysmAction line 46
6. theorem OAI.Problem346.plethysmAction_bijective line 50
7. theorem OAI.Problem346.isGLEquivariantEmbedding_of_commutes line 54
8. theorem OAI.Problem346.plethysmAction_refl line 67
9. theorem OAI.Problem346.plethysmAction_trans line 71
10. theorem OAI.Problem346.plethysmAction_symm_comp line 79
11. theorem OAI.Problem346.plethysmAction_comp_symm line 85
12. theorem OAI.Problem346.isFoulkesMap_conjugate line 92

    Source documentation

    Conjugating by the natural GL actions preserves the defining canonical formula.

    theorem isFoulkesMap_conjugate {a b : ℕ}
        {μ : SymPow b (SymPow a V) →ₗ[ℂ] SymPow a (SymPow b V)}
        (hμ : IsFoulkesMap a b V μ) (g : V ≃ₗ[ℂ] V) :
        IsFoulkesMap a b V
          ((plethysmAction a b g.symm).comp (μ.comp (plethysmAction b a g))) := by
    …

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

13. theorem OAI.Problem346.foulkesMap_commutes_of_unique line 104

    Source documentation

    Uniqueness of the canonical map implies its GL equivariance.

    theorem foulkesMap_commutes_of_unique {a b : ℕ}
        {μ : SymPow b (SymPow a V) →ₗ[ℂ] SymPow a (SymPow b V)}
        (hμ : IsFoulkesMap a b V μ)
        (huniq : ∀ ν : SymPow b (SymPow a V) →ₗ[ℂ] SymPow a (SymPow b V),
          IsFoulkesMap a b V ν → ν = μ)
        (g : V ≃ₗ[ℂ] V) :
        (plethysmAction a b g).comp μ = μ.comp (plethysmAction b a g) := by
    …

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