OAI/RepresentationTheory/RowColumn/HookModel.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RowColumn.HookModel.Color line 13
2. def OAI.RowColumn.HookModel.IsOdd line 15
3. def OAI.RowColumn.HookModel.template line 21
4. lemma OAI.RowColumn.HookModel.template_parity line 25
5. lemma OAI.RowColumn.HookModel.template_row line 30
6. lemma OAI.RowColumn.HookModel.template_col line 38
7. abbrev OAI.RowColumn.HookModel.oddCount line 47
8. def OAI.RowColumn.HookModel.templateWord line 49
9. lemma OAI.RowColumn.HookModel.row_preserved line 52
10. lemma OAI.RowColumn.HookModel.template_rigidity line 58

    Source documentation

    The nonzero coefficient of the Young symmetrizer is protected from sign cancellation: surviving row motions fix bottom cells, and column motions fix all top cells.

    lemma template_rigidity (c : colGroup μ) (r : CubeShuffle.Specht.rowGroup μ)
        (hw : actWord (c.1 * r.1) (templateWord μ h H) = templateWord μ h H) :
        (∀ x : Cell μ, row x < h → c.1 x = x) ∧
        (∀ x : Cell μ, h ≤ row x → r.1 x = x) := by
    …

    Mentions: OAI.CubeShuffle.Specht.rowGroup, OAI.RowColumn.HookModel.templateWord

11. lemma OAI.RowColumn.HookModel.template_row_stabilized line 88
12. lemma OAI.RowColumn.HookModel.template_young_sign line 103
13. def OAI.RowColumn.tabloidOrbitMap line 134

    Source documentation

    The actual orbit sum giving the map out of the tabloid permutation module. It is unnormalized, which is harmless for testing nonzero Young symmetrizers.

    def tabloidOrbitMap : (Tabloid μ → ℂ) →ₗ[ℂ] V where
    …

14. lemma OAI.RowColumn.tabloidOrbitMap_intertwines line 143
15. lemma OAI.RowColumn.tabloidOrbitMap_delta_base line 160
16. lemma OAI.RowColumn.tabloidOrbitMap_polytabloid line 174
17. def OAI.RowColumn.youngIntertwiner line 185

    Source documentation

    Restricting the orbit map to the already constructed, proved irreducible Specht module.

    def youngIntertwiner : Representation.IntertwiningMap (CubeShuffle.Specht.representation μ) ρ where
    …

    Mentions: OAI.CubeShuffle.Specht.representation

18. theorem OAI.RowColumn.youngIntertwiner_injective line 193

    Source documentation

    A nonvanishing actual column-alternator/row-symmetrizer vector supplies an embedding; no Littlewood--Richardson occurrence statement is assumed.

    theorem youngIntertwiner_injective
        (hn : alternator (colGroup μ) ρ (symmetrizer (CubeShuffle.Specht.rowGroup μ) ρ v) ≠ 0) :
        Function.Injective (youngIntertwiner μ ρ v) := by
    …

    Mentions: OAI.CubeShuffle.Specht.rowGroup, OAI.RowColumn.youngIntertwiner

19. abbrev OAI.RowColumn.HookModel.hookRepresentation line 215
20. def OAI.RowColumn.HookModel.youngVector line 218
21. lemma OAI.RowColumn.HookModel.youngVector_coefficient line 223
22. lemma OAI.RowColumn.HookModel.youngVector_nonzero line 245
23. def OAI.RowColumn.HookModel.hookEmbedding line 275

    Source documentation

    Explicit signed-slot realization of every (h,h)-hook Specht module. The target, action, and intertwiner are concrete; no LR/Schur-Weyl occurrence axiom is used. This supplies the first necessary step of weighted.tex:88–93.

    def hookEmbedding : Representation.IntertwiningMap (CubeShuffle.Specht.representation μ)
        (hookRepresentation μ h H) :=
    …

    Mentions: OAI.CubeShuffle.Specht.representation, OAI.RowColumn.HookModel.hookRepresentation

24. theorem OAI.RowColumn.HookModel.hookEmbedding_injective line 279