OAI/RepresentationTheory/YoungSymmetry/Polytabloid.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Elementary polytabloid input for the symmetric-group step of FAC.7. No branching or classification theorem is postulated here.

  1. abbrev OAI.CubeShuffle.Specht.Cell line 10

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:9 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:9 (same declaration text).

  2. lemma OAI.CubeShuffle.Specht.card_cell line 12

    Also declared: ComparatorChallenges/WeightedSweepMoments.lean:217 (same declaration text).

  3. def OAI.CubeShuffle.Specht.row line 15

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:10 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:10 (same declaration text).

  4. def OAI.CubeShuffle.Specht.col line 16

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:11 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:11 (same declaration text).

  5. lemma OAI.CubeShuffle.Specht.row_lt_colLen line 18

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:13 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:13 (same declaration text).

  6. def OAI.CubeShuffle.Specht.columnEquiv line 21
  7. def OAI.CubeShuffle.Specht.columnValues line 28
  8. lemma OAI.CubeShuffle.Specht.mem_columnValues line 31
  9. lemma OAI.CubeShuffle.Specht.card_columnValues line 36
  10. lemma OAI.CubeShuffle.Specht.strictMono_fin_nat_ge line 46
  11. def OAI.CubeShuffle.Specht.rankCell line 61

    Source documentation

    Rank inside a column, sorted by an arbitrary column-injective row assignment.

    noncomputable def rankCell {μ : YoungDiagram} (f : Cell μ → ℕ)
    (hf : ∀ x y, col x = col y → f x = f y → x = y) (x : Cell μ) : Cell μ :=
…

    Mentions: OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.col

  12. lemma OAI.CubeShuffle.Specht.rankCell_col line 67
  13. lemma OAI.CubeShuffle.Specht.rankCell_orderEmb line 71
  14. lemma OAI.CubeShuffle.Specht.rankCell_injective line 80
  15. def OAI.CubeShuffle.Specht.rankPerm line 94
  16. lemma OAI.CubeShuffle.Specht.rankCell_row_le line 98
  17. theorem OAI.CubeShuffle.Specht.column_transporter line 106

    Source documentation

    The equal-shape column-transporter lemma. This is the combinatorial rank-one input to the Specht submodule theorem, proved using sorting, not Young's rule.

    theorem column_transporter (μ : YoungDiagram) (p : Equiv.Perm (Cell μ))
    (hp : ∀ x y, col x = col y → row (p x) = row (p y) → x = y) :
    ∃ c : Equiv.Perm (Cell μ), (∀ x, col (c x) = col x) ∧
      ∀ x, row (c x) = row (p x) := by
…

    Mentions: OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.col, OAI.CubeShuffle.Specht.row

  18. def OAI.CubeShuffle.Specht.rowIndex line 122

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:15 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:15 (same declaration text).

  19. abbrev OAI.CubeShuffle.Specht.Tabloid line 125

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:18 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:18 (same declaration text).

  20. instance OAI.CubeShuffle.Specht.(instance at line 128) line 128
  21. def OAI.CubeShuffle.Specht.baseTabloid line 130

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:23 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:23 (same declaration text).

  22. def OAI.CubeShuffle.Specht.tabloidAct line 132

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:25 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:25 (same declaration text).

  23. lemma OAI.CubeShuffle.Specht.tabloidAct_apply line 147

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:40 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:40 (same declaration text).

  24. lemma OAI.CubeShuffle.Specht.tabloidAct_one line 150

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:43 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:43 (same declaration text).

  25. lemma OAI.CubeShuffle.Specht.tabloidAct_mul line 154

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:47 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:47 (same declaration text).

  26. lemma OAI.CubeShuffle.Specht.tabloidAct_inv line 159

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:52 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:52 (same declaration text).

  27. def OAI.CubeShuffle.Specht.tabloidRep line 164

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:57 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:57 (same declaration text).

  28. lemma OAI.CubeShuffle.Specht.tabloidRep_apply line 176

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:69 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:69 (same declaration text).

  29. def OAI.CubeShuffle.Specht.delta line 179

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:72 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:72 (same declaration text).

  30. lemma OAI.CubeShuffle.Specht.tabloidRep_delta line 182
  31. def OAI.CubeShuffle.Specht.colGroup line 190

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:75 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:75 (same declaration text).

  32. lemma OAI.CubeShuffle.Specht.mem_colGroup line 196
  33. lemma OAI.CubeShuffle.Specht.colGroup_row_stabilizer line 199
  34. lemma OAI.CubeShuffle.Specht.tabloid_column_transporter line 208
  35. def OAI.CubeShuffle.Specht.permSign line 229

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:81 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:81 (same declaration text).

  36. lemma OAI.CubeShuffle.Specht.permSign_one line 232
  37. lemma OAI.CubeShuffle.Specht.permSign_mul line 234
  38. lemma OAI.CubeShuffle.Specht.permSign_inv line 236
  39. lemma OAI.CubeShuffle.Specht.permSign_sq line 238
  40. lemma OAI.CubeShuffle.Specht.permSign_swap line 243
  41. lemma OAI.CubeShuffle.Specht.conj_permSign line 245
  42. def OAI.CubeShuffle.Specht.alternator line 251

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:86 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:86 (same declaration text).

  43. lemma OAI.CubeShuffle.Specht.alternator_mul line 256
  44. lemma OAI.CubeShuffle.Specht.mul_alternator line 271
  45. lemma OAI.CubeShuffle.Specht.alternator_apply_action line 286
  46. lemma OAI.CubeShuffle.Specht.action_alternator_apply line 291
  47. lemma OAI.CubeShuffle.Specht.alternator_eq_zero_of_odd_stabilizer line 297

    Source documentation

    An odd column stabilizer forces cancellation in the genuine alternating sum.

    lemma alternator_eq_zero_of_odd_stabilizer (C : Subgroup (Equiv.Perm α))
    (ρ : Representation ℂ (Equiv.Perm α) V) (c : C) (v : V)
    (hc : permSign (c : Equiv.Perm α) = -1) (hv : ρ c v = v) :
    alternator C ρ v = 0 := by
…

    Mentions: OAI.CubeShuffle.Specht.permSign, OAI.CubeShuffle.Specht.alternator

  48. lemma OAI.CubeShuffle.Specht.swap_mem_colGroup line 314
  49. lemma OAI.CubeShuffle.Specht.swap_fixes_tabloid line 324
  50. def OAI.CubeShuffle.Specht.polytabloid line 336

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:93 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:93 (same declaration text).

  51. lemma OAI.CubeShuffle.Specht.alternator_delta_rank_one line 339
  52. lemma OAI.CubeShuffle.Specht.polytabloid_formula line 355
  53. lemma OAI.CubeShuffle.Specht.polytabloid_base line 361
  54. lemma OAI.CubeShuffle.Specht.polytabloid_ne_zero line 374
  55. lemma OAI.CubeShuffle.Specht.delta_decomposition line 379
  56. theorem OAI.CubeShuffle.Specht.alternator_rank_one line 387

    Source documentation

    The actual column antisymmetrizer has one-dimensional range.

    theorem alternator_rank_one (μ : YoungDiagram) (v : Tabloid μ → ℂ) :
    ∃ z : ℂ, alternator (colGroup μ) (tabloidRep μ) v = z • polytabloid μ := by
…

    Mentions: OAI.CubeShuffle.Specht.Tabloid, OAI.CubeShuffle.Specht.alternator, OAI.CubeShuffle.Specht.colGroup, OAI.CubeShuffle.Specht.tabloidRep, OAI.CubeShuffle.Specht.polytabloid

  57. lemma OAI.CubeShuffle.Specht.alternator_rank_one_exact line 395
  58. def OAI.CubeShuffle.Specht.pairing line 406
  59. lemma OAI.CubeShuffle.Specht.pairing_delta line 409
  60. lemma OAI.CubeShuffle.Specht.pairing_sum_left line 414
  61. lemma OAI.CubeShuffle.Specht.pairing_smul_left line 420
  62. lemma OAI.CubeShuffle.Specht.pairing_zero_left line 427
  63. lemma OAI.CubeShuffle.Specht.pairing_add_left line 430
  64. lemma OAI.CubeShuffle.Specht.pairing_self_eq_zero line 434
  65. lemma OAI.CubeShuffle.Specht.pairing_action line 442
  66. lemma OAI.CubeShuffle.Specht.alternator_base_pairing line 453
  67. theorem OAI.CubeShuffle.Specht.alternator_pairing line 464

    Source documentation

    The column antisymmetrizer is the rank-one form of the polytabloid.

    theorem alternator_pairing (μ : YoungDiagram) (v : Tabloid μ → ℂ) :
    alternator (colGroup μ) (tabloidRep μ) v = pairing (polytabloid μ) v • polytabloid μ := by
…

    Mentions: OAI.CubeShuffle.Specht.Tabloid, OAI.CubeShuffle.Specht.alternator, OAI.CubeShuffle.Specht.colGroup, OAI.CubeShuffle.Specht.tabloidRep, OAI.CubeShuffle.Specht.pairing, OAI.CubeShuffle.Specht.polytabloid

  68. def OAI.CubeShuffle.Specht.space line 472

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:96 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:96 (same declaration text).

  69. lemma OAI.CubeShuffle.Specht.orbit_mem_space line 475

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:99 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:99 (same declaration text).

  70. lemma OAI.CubeShuffle.Specht.polytabloid_mem_space line 478
  71. lemma OAI.CubeShuffle.Specht.action_mem_space line 481

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:102 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:102 (same declaration text).

  72. lemma OAI.CubeShuffle.Specht.alternator_mem_invariant line 493
  73. theorem OAI.CubeShuffle.Specht.submodule_theorem line 501

    Source documentation

    The Specht submodule theorem, for the actual complex tabloid module.

    theorem submodule_theorem (μ : YoungDiagram) (W : Submodule ℂ (Tabloid μ → ℂ))
    (hW : ∀ p v, v ∈ W → tabloidRep μ p v ∈ W) :
    space μ ≤ W ∨ ∀ v ∈ W, ∀ w ∈ space μ, pairing w v = 0 := by
…

    Mentions: OAI.CubeShuffle.Specht.Tabloid, OAI.CubeShuffle.Specht.tabloidRep, OAI.CubeShuffle.Specht.space, OAI.CubeShuffle.Specht.pairing

  74. theorem OAI.CubeShuffle.Specht.space_simple line 533

    Source documentation

    No proper nonzero invariant complex subspace exists in a Specht space.

    theorem space_simple (μ : YoungDiagram) (W : Submodule ℂ (Tabloid μ → ℂ))
    (hW : ∀ p v, v ∈ W → tabloidRep μ p v ∈ W) (hWS : W ≤ space μ) :
    W = ⊥ ∨ W = space μ := by
…

    Mentions: OAI.CubeShuffle.Specht.Tabloid, OAI.CubeShuffle.Specht.tabloidRep, OAI.CubeShuffle.Specht.space

  75. def OAI.CubeShuffle.Specht.subrepresentation line 543

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:114 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:114 (same declaration text).

  76. def OAI.CubeShuffle.Specht.representation line 546

    Also declared: ComparatorChallenges/OccupiedOverlap.lean:117 (same declaration text), ComparatorChallenges/WeightedSweepMoments.lean:117 (same declaration text).

  77. lemma OAI.CubeShuffle.Specht.space_ne_bot line 554
  78. theorem OAI.CubeShuffle.Specht.representation_irreducible line 561

    Source documentation

    The constructed Specht representation is irreducible over the complex numbers.

    theorem representation_irreducible (μ : YoungDiagram) :
    Representation.IsIrreducible (representation μ) := by
…

    Mentions: OAI.CubeShuffle.Specht.representation

  79. def OAI.CubeShuffle.Specht.symmetrizer line 603
  80. lemma OAI.CubeShuffle.Specht.symmetrizer_mul line 607
  81. lemma OAI.CubeShuffle.Specht.symmetrizer_eq_zero_of_neg line 613
  82. def OAI.CubeShuffle.Specht.fiberGroup line 625
  83. lemma OAI.CubeShuffle.Specht.swap_mem_fiberGroup line 632
  84. lemma OAI.CubeShuffle.Specht.swap_polytabloid line 643
  85. theorem OAI.CubeShuffle.Specht.tall_column_average_zero line 652

    Source documentation

    Pigeonhole replaces the cited Pieri support restriction: a column having more cells than fibers is killed by the uniform fiber-preserving subgroup.

    theorem tall_column_average_zero (μ : YoungDiagram) {β : Type*} [Fintype β]
    (f : Cell μ → β) (j : ℕ) (hj : Fintype.card β < μ.colLen j)
    (v : Tabloid μ → ℂ) (hv : v ∈ space μ) :
    symmetrizer (fiberGroup f) (tabloidRep μ) v = 0 := by
…

    Mentions: OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.Tabloid, OAI.CubeShuffle.Specht.space, OAI.CubeShuffle.Specht.symmetrizer, OAI.CubeShuffle.Specht.fiberGroup, OAI.CubeShuffle.Specht.tabloidRep