Naturality.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem346.plethysmMap line 16
Source documentation
The map on a plethysm induced by a linear map on the original space.
```
def plethysmMap (outer inner : ℕ) (f : V →ₗ[ℂ] W) :
    SymPow outer (SymPow inner V) →ₗ[ℂ] SymPow outer (SymPow inner W) :=
…
```
Mentions: OAI.Problem346.SymPow
theorem OAI.Problem346.plethysmMap_symMonomial line 20
theorem OAI.Problem346.plethysmMap_id line 28
theorem OAI.Problem346.plethysmMap_comp line 32
theorem OAI.Problem346.plethysmMap_equiv line 37
theorem OAI.Problem346.plethysmMap_foulkesFormula line 41
Source documentation
The explicitly normalized Foulkes formula is natural in the vector space.
```
theorem plethysmMap_foulkesFormula (a b : ℕ) (f : V →ₗ[ℂ] W)
    (x : Fin b → Fin a → V) :
    plethysmMap a b f (foulkesFormula a b V x) =
      foulkesFormula a b W (fun j i => f (x j i)) := by
…
```
Mentions: OAI.Problem346.plethysmMap, OAI.Problem346.foulkesFormula

theorem OAI.Problem346.IsFoulkesMap.natural line 54

Source documentation

Any two maps satisfying the canonical formula form a natural square.

theorem IsFoulkesMap.natural {a b : ℕ}
    {μV : SymPow b (SymPow a V) →ₗ[ℂ] SymPow a (SymPow b V)}
    {μW : SymPow b (SymPow a W) →ₗ[ℂ] SymPow a (SymPow b W)}
    (hV : IsFoulkesMap a b V μV) (hW : IsFoulkesMap a b W μW)
    (f : V →ₗ[ℂ] W) :
    (plethysmMap a b f).comp μV = μW.comp (plethysmMap b a f) := by
…

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

theorem OAI.Problem346.IsFoulkesMap.commutes line 66

Source documentation

Every canonical Foulkes map is GL-equivariant.

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

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