OAI/RepresentationTheory/Young/Classification.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CoordinateSweeps.YoungCorner.Boxes line 36
2. def OAI.CoordinateSweeps.YoungCorner.colorStabilizer line 38
3. def OAI.CoordinateSweeps.YoungCorner.rows line 46
4. def OAI.CoordinateSweeps.YoungCorner.cols line 47
5. lemma OAI.CoordinateSweeps.YoungCorner.row_lt line 49
6. lemma OAI.CoordinateSweeps.YoungCorner.col_lt line 53
7. def OAI.CoordinateSweeps.YoungCorner.rowDecomp line 56
8. lemma OAI.CoordinateSweeps.YoungCorner.strictMono_fin_nat_ge line 62
9. def OAI.CoordinateSweeps.YoungCorner.values line 74
10. lemma OAI.CoordinateSweeps.YoungCorner.values_card line 76
11. def OAI.CoordinateSweeps.YoungCorner.valuesEquiv line 79
12. def OAI.CoordinateSweeps.YoungCorner.sortPerm line 87

    Source comment

    Sort a finite injective natural-valued list without changing its indices.

    def sortPerm {n : ℕ} (f : Fin n → ℕ) (hf : Function.Injective f) : Equiv.Perm (Fin n) :=
    …

13. lemma OAI.CoordinateSweeps.YoungCorner.sortPerm_ge line 90
14. def OAI.CoordinateSweeps.YoungCorner.NoCollision line 100

    Source comment

    Row-column noncollision: at most one source cell in any row can land in any destination column.

    def NoCollision (μ : YoungDiagram) (σ : Equiv.Perm (Boxes μ)) : Prop :=
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes

15. def OAI.CoordinateSweeps.YoungCorner.rowColumn line 103
16. lemma OAI.CoordinateSweeps.YoungCorner.rowColumn_injective line 107
17. def OAI.CoordinateSweeps.YoungCorner.sortingRows line 113
18. lemma OAI.CoordinateSweeps.YoungCorner.sortingRows_mem line 118
19. lemma OAI.CoordinateSweeps.YoungCorner.sortingRows_col_ge line 123
20. theorem OAI.CoordinateSweeps.YoungCorner.factor_column_row line 130

    Source comment

    The essential Ferrers uniqueness lemma. Sorting inside rows can only increase columns; preservation of the total column sum forces equality.

    theorem factor_column_row (μ : YoungDiagram) (σ : Equiv.Perm (Boxes μ)) (h : NoCollision μ σ) :
        ∃ c ∈ cols μ, ∃ r ∈ rows μ, σ=c*r := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.NoCollision, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.YoungCorner.cols, OAI.CoordinateSweeps.YoungCorner.rows

21. def OAI.CoordinateSweeps.YoungCorner.rowPrefix line 148
22. def OAI.CoordinateSweeps.YoungCorner.columnPrefixEquiv line 151
23. lemma OAI.CoordinateSweeps.YoungCorner.card_column_prefix line 170
24. lemma OAI.CoordinateSweeps.YoungCorner.card_source_column_le line 175
25. theorem OAI.CoordinateSweeps.YoungCorner.prefix_dominance line 206

    Source comment

    The actual Ferrers dominance consequence of a collision-free matching.

    theorem prefix_dominance (μ ν : YoungDiagram) (e : Boxes μ ≃ Boxes ν)
        (hnc : ∀ x y, x.val.1=y.val.1 → (e x).val.2=(e y).val.2 → x=y) (t : ℕ) :
        (rowPrefix μ t).card≤(rowPrefix ν t).card := by
    …

    Mentions: OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.rowPrefix

26. def OAI.CoordinateSweeps.YoungCorner.rowEquiv line 223
27. lemma OAI.CoordinateSweeps.YoungCorner.card_row line 232
28. lemma OAI.CoordinateSweeps.YoungCorner.prefix_succ line 238
29. lemma OAI.CoordinateSweeps.YoungCorner.eq_of_prefix_dominance line 253

    Source comment

    Opposite Young dominance determines the diagram.

    lemma eq_of_prefix_dominance (μ ν : YoungDiagram)
        (hμν : ∀ t, (rowPrefix μ t).card≤(rowPrefix ν t).card)
        (hνμ : ∀ t, (rowPrefix ν t).card≤(rowPrefix μ t).card) : μ=ν := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.rowPrefix

30. lemma OAI.CoordinateSweeps.RepDetection.subrep_bot line 272
31. lemma OAI.CoordinateSweeps.RepDetection.subrep_top line 275
32. def OAI.CoordinateSweeps.RepDetection.nested line 278
33. theorem OAI.CoordinateSweeps.RepDetection.exists_irreducible_detecting line 286
34. theorem OAI.CoordinateSweeps.RepDetection.exists_cross_nonzero line 356

    Source comment

    Irreducibility supplies the cross-corner nonvanishing needed for Young shape uniqueness via the orbit-span argument.

    theorem exists_cross_nonzero (τ : Representation ℂ G V) [τ.IsIrreducible]
        (P Q : Module.End ℂ V) (hP : P ≠ 0) (hQ : Q ≠ 0) :
        ∃ g, P * τ g * Q ≠ 0 := by
    …

35. def OAI.CoordinateSweeps.YoungCorner.signScalar line 403

    Source comment

    Ordinary source sign.

    def signScalar {X : Type*} [Fintype X] [DecidableEq X] : Equiv.Perm X →* ℂ :=
    …

36. lemma OAI.CoordinateSweeps.YoungCorner.signScalar_swap line 406
37. def OAI.CoordinateSweeps.YoungCorner.fixedSum line 410
38. def OAI.CoordinateSweeps.YoungCorner.alternatingSum line 413
39. lemma OAI.CoordinateSweeps.YoungCorner.fixedSum_right line 416
40. lemma OAI.CoordinateSweeps.YoungCorner.alternatingSum_left line 422
41. lemma OAI.CoordinateSweeps.YoungCorner.swap_mem_color line 438
42. lemma OAI.CoordinateSweeps.YoungCorner.colored_corner_zero line 448

    Source comment

    Literal transposition cancellation in a Young row/column corner.

    lemma colored_corner_zero (f g : X → ℕ) (ρ : Equiv.Perm X →* A)
        (σ : Equiv.Perm X) (x y : X) (hxy : x ≠ y)
        (hrow : f x=f y) (hcol : g (σ⁻¹ x)=g (σ⁻¹ y)) :
        fixedSum f ρ * ρ σ * alternatingSum g ρ=0 := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.fixedSum, OAI.CoordinateSweeps.YoungCorner.alternatingSum

43. def OAI.CoordinateSweeps.YoungCorner.rowColor line 489
44. def OAI.CoordinateSweeps.YoungCorner.colColor line 490
45. def OAI.CoordinateSweeps.YoungCorner.hasShape line 492
46. lemma OAI.CoordinateSweeps.YoungCorner.cross_dominance line 495
47. theorem OAI.CoordinateSweeps.YoungCorner.shape_unique line 511

    Source comment

    A genuine irreducible cannot carry two different Young shapes.

    theorem shape_unique (μ ν : YoungDiagram) (t : X ≃ Boxes μ) (u : X ≃ Boxes ν)
        (τ : Representation ℂ (Equiv.Perm X) V) [τ.IsIrreducible]
        (hμ : hasShape μ t τ) (hν : hasShape ν u τ) : μ=ν := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.hasShape

48. lemma OAI.CoordinateSweeps.YoungCorner.hasShape_equiv line 521
49. def OAI.CoordinateSweeps.YoungCorner.regular line 537
50. lemma OAI.CoordinateSweeps.YoungCorner.regular_apply line 545
51. lemma OAI.CoordinateSweeps.YoungCorner.row_column_intersection line 548
52. lemma OAI.CoordinateSweeps.YoungCorner.regular_hasShape line 576

    Source comment

    Every diagram has a nonzero row-column corner in the genuine regular law.

    lemma regular_hasShape (μ : YoungDiagram) (t : X ≃ Boxes μ) :
        hasShape μ t (regular (Equiv.Perm X)) := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.hasShape, OAI.CoordinateSweeps.YoungCorner.regular

53. lemma OAI.CoordinateSweeps.YoungCorner.fixedSum_subrepresentation line 595
54. lemma OAI.CoordinateSweeps.YoungCorner.alternatingSum_subrepresentation line 600
55. lemma OAI.CoordinateSweeps.YoungCorner.exists_shape_constituent line 605
56. def OAI.CoordinateSweeps.YoungCorner.shapeSubrep line 619

    Source comment

    Chosen regular constituent.

    def shapeSubrep (μ : YoungDiagram) (t : X ≃ Boxes μ) : Subrepresentation (regular (Equiv.Perm X)) :=
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.regular

57. instance OAI.CoordinateSweeps.YoungCorner.shapeSubrep_irreducible line 622
58. lemma OAI.CoordinateSweeps.YoungCorner.shapeSubrep_hasShape line 626
59. def OAI.CoordinateSweeps.YoungCorner.diagramOfPartition line 634
60. lemma OAI.CoordinateSweeps.YoungCorner.partitionRows_pos line 637
61. lemma OAI.CoordinateSweeps.YoungCorner.diagramOfPartition_rowLens line 643
62. lemma OAI.CoordinateSweeps.YoungCorner.diagramOfPartition_injective line 647
63. lemma OAI.CoordinateSweeps.YoungCorner.card_boxes_eq_rowLens_sum line 655
64. lemma OAI.CoordinateSweeps.YoungCorner.card_diagramOfPartition line 666
65. def OAI.CoordinateSweeps.YoungCorner.partitionFilling line 671
66. def OAI.CoordinateSweeps.CharacterCount.pairing line 683
67. lemma OAI.CoordinateSweeps.CharacterCount.characters_independent line 688
68. theorem OAI.CoordinateSweeps.CharacterCount.card_le_of_classifier line 714

    Source comment

    Pulling characters through any finite conjugacy classifier bounds how many inequivalent irreducibles there can be. The classifier need not be surjective.

    theorem card_le_of_classifier [Fintype I] {C : Type*} [Fintype C]
        (classifier : G → C)
        (hclass : ∀ i g h, classifier g=classifier h → (τ i).character g=(τ i).character h)
        (hne : ∀ i j, i ≠ j → IsEmpty (Representation.Equiv (τ i) (τ j))) :
        Fintype.card I ≤ Fintype.card C := by
    …

69. theorem OAI.CoordinateSweeps.CharacterCount.complete_of_classifier line 747

    Source comment

    An inequivalent family as large as a finite conjugacy classifier is complete. This finite counting argument establishes the Young classification.

    theorem complete_of_classifier (classifier : G → C)
        (hτ : ∀ i g h, classifier g=classifier h → (τ i).character g=(τ i).character h)
        (hne : ∀ i j, i ≠ j → IsEmpty (Representation.Equiv (τ i) (τ j)))
        {W : Type w} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
        (σ : Representation ℂ G W) [σ.IsIrreducible]
        (hσ : ∀ g h, classifier g=classifier h → σ.character g=σ.character h) :
        ∃ i, Nonempty (Representation.Equiv (τ i) σ) := by
    …

70. lemma OAI.CoordinateSweeps.CharacterCount.permutation_character_factors line 783
71. abbrev OAI.CoordinateSweeps.YoungCorner.PartitionSpace line 794
72. def OAI.CoordinateSweeps.YoungCorner.partitionRep line 797
73. instance OAI.CoordinateSweeps.YoungCorner.partitionRep_irreducible line 801
74. lemma OAI.CoordinateSweeps.YoungCorner.partitionRep_hasShape line 804
75. lemma OAI.CoordinateSweeps.YoungCorner.partitionRep_inequivalent line 808
76. theorem OAI.CoordinateSweeps.YoungCorner.partitionRep_complete line 818

    Source comment

    Young classification from regular constituents, Ferrers dominance and finite-group character orthogonality.

    theorem partitionRep_complete {V : Type} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
        (τ : Representation ℂ (Equiv.Perm X) V) [τ.IsIrreducible] :
        ∃ p : Nat.Partition (Fintype.card X),
          Nonempty (Representation.Equiv (partitionRep p (X := X)) τ) := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.partitionRep

77. theorem OAI.CoordinateSweeps.YoungCorner.exists_partitionShape line 834

    Source comment

    Every literal irreducible carries exactly one diagram shape.

    theorem exists_partitionShape {V : Type} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
        (τ : Representation ℂ (Equiv.Perm X) V) [τ.IsIrreducible] :
        ∃ p : Nat.Partition (Fintype.card X), hasShape (diagramOfPartition p) (partitionFilling p) τ := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.hasShape, OAI.CoordinateSweeps.YoungCorner.diagramOfPartition, OAI.CoordinateSweeps.YoungCorner.partitionFilling

78. theorem OAI.CoordinateSweeps.YoungCorner.equiv_of_same_shape line 842

    Source comment

    Two actual irreps of the same diagram are equivalent, even for unrelated fillings. This is the uniqueness fact needed for the hook/removal argument.

    theorem equiv_of_same_shape {V W : Type} [AddCommGroup V] [Module ℂ V]
        [FiniteDimensional ℂ V] [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
        (τ : Representation ℂ (Equiv.Perm X) V) (σ : Representation ℂ (Equiv.Perm X) W)
        [τ.IsIrreducible] [σ.IsIrreducible]
        (μ : YoungDiagram) (t u : X ≃ Boxes μ) (hτ : hasShape μ t τ) (hσ : hasShape μ u σ) :
        Nonempty (Representation.Equiv τ σ) := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.hasShape

79. def OAI.CoordinateSweeps.YoungCorner.partitionUnitary line 863
80. lemma OAI.CoordinateSweeps.YoungCorner.partitionUnitary_equiv line 866
81. lemma OAI.CoordinateSweeps.YoungCorner.partitionUnitary_inequivalent line 871
82. lemma OAI.CoordinateSweeps.YoungCorner.partitionUnitary_complete line 879
83. theorem OAI.CoordinateSweeps.YoungCorner.partition_projector_resolution line 888

    Source comment

    The chosen Young projectors resolve identity in every finite representation. The proof detects a simple constituent if the residual operator is nonzero.

    theorem partition_projector_resolution {V : Type} [AddCommGroup V] [Module ℂ V]
        [FiniteDimensional ℂ V] (τ : Representation ℂ (Equiv.Perm X) V) :
        ∑ p, (partitionUnitary X p).projector τ=1 := by
    …

    Mentions: OAI.CoordinateSweeps.YoungCorner.partitionUnitary

84. lemma OAI.CoordinateSweeps.YoungCorner.partition_matrix_resolution line 933