OAI/RepresentationTheory/RowColumn/SignedWords.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RowColumn.Signed.Words line 17

    Source documentation

    Words with exactly k odd entries. This is the k-parity sector of the literal signed slot space, not a formal unknown representation.

    abbrev Words (k : ℕ) := {w : S → C // Fintype.card {x : S // odd (w x)} = k}
…
  2. abbrev OAI.RowColumn.Signed.OddSlots line 23

    Source documentation

    Odd slots of a word, genuinely a subset of the board slots.

    abbrev OddSlots (w : Words (S := S) odd k) := {x : S // odd (w.1 x)}

    Mentions: OAI.RowColumn.Signed.Words

  3. def OAI.RowColumn.Signed.relabelOddEquiv line 25
  4. def OAI.RowColumn.Signed.actWord line 32
  5. lemma OAI.RowColumn.Signed.actWord_apply line 36
  6. lemma OAI.RowColumn.Signed.actWord_one line 40
  7. lemma OAI.RowColumn.Signed.actWord_mul line 46
  8. def OAI.RowColumn.Signed.oddFrame line 54

    Source documentation

    Canonical frames choose the odd-slot orientation. Different choices conjugate by a diagonal sign; the signed action is exactly reordering the odd slots.

    def oddFrame (w : Words (S := S) odd k) : OddSlots w ≃ Fin k :=
…

    Mentions: OAI.RowColumn.Signed.Words, OAI.RowColumn.Signed.OddSlots

  9. def OAI.RowColumn.Signed.oddPerm line 57
  10. lemma OAI.RowColumn.Signed.oddFrame_congr line 61
  11. lemma OAI.RowColumn.Signed.oddPerm_one line 68
  12. lemma OAI.RowColumn.Signed.oddPerm_mul line 78
  13. def OAI.RowColumn.Signed.wordsEquiv line 91
  14. def OAI.RowColumn.Signed.signedMap line 99

    Source documentation

    Signed slot action in the orthonormal word basis. It reorders the odd subsequence, and does not introduce a sign for even slots.

    def signedMap (g : Equiv.Perm S) :
    EuclideanSpace ℂ (Words (S := S) odd k) →ₗ[ℂ] EuclideanSpace ℂ (Words (S := S) odd k) where
…

    Mentions: OAI.RowColumn.Signed.Words

  15. lemma OAI.RowColumn.Signed.signedMap_apply line 106
  16. def OAI.RowColumn.Signed.representation line 111

    Source documentation

    The signs genuinely compose; no group-action relation is assumed.

    def representation : Representation ℂ (Equiv.Perm S) (EuclideanSpace ℂ (Words (S := S) odd k)) where
…

    Mentions: OAI.RowColumn.Signed.Words

  17. lemma OAI.RowColumn.Signed.representation_unitary line 121
  18. lemma OAI.RowColumn.Signed.word_stabilizer_eq line 150
  19. lemma OAI.RowColumn.Signed.oddPerm_sign_of_stabilizes line 156
  20. lemma OAI.RowColumn.Signed.oddPerm_of_odd_fixed line 177
  21. lemma OAI.RowColumn.Signed.actWord_inv_eq_iff line 194
  22. lemma OAI.RowColumn.Signed.oddPerm_inv_stabilizer line 207
  23. def OAI.RowColumn.Signed.wordVector line 213
  24. lemma OAI.RowColumn.Signed.wordVector_coefficient line 217
  25. lemma OAI.RowColumn.Signed.oddPerm_inv line 236
  26. lemma OAI.RowColumn.Signed.signedMap_transport_apply line 243
  27. lemma OAI.RowColumn.Signed.signedMap_wordVector line 250
  28. lemma OAI.RowColumn.Signed.permSign_ne_zero line 264
  29. lemma OAI.RowColumn.Signed.sum_wordVectors line 270
  30. abbrev OAI.RowColumn.Signed.lineRepresentation line 277
  31. lemma OAI.RowColumn.Signed.commuting_coefficient_relation line 281
  32. def OAI.RowColumn.WordOrbits.counts line 302

    Source documentation

    A complete invariant of the simultaneous permutation orbit of finitely many words: the counts of their joint symbols.

    def counts (f : S → A) : A → Fin (Fintype.card S + 1) := fun a =>
…
  33. lemma OAI.RowColumn.WordOrbits.same_counts_permutation line 307
  34. lemma OAI.RowColumn.WordOrbits.line_pair_transporter line 321

    Source documentation

    The label can record a row or a column. Joint counts then give a word transporter inside the actual line subgroup, not an abstract action.

    lemma line_pair_transporter {L C : Type*} [Fintype L] [Fintype C]
    [DecidableEq L] [DecidableEq C]
    (line : S → L) (w v w' v' : S → C)
    (he : counts (fun x => (line x, w x, v x)) = counts (fun x => (line x, w' x, v' x))) :
    ∃ p : Equiv.Perm S, (∀ x, line (p x) = line x) ∧
      (∀ x, w' (p x) = w x) ∧ (∀ x, v' (p x) = v x) := by
…

    Mentions: OAI.RowColumn.WordOrbits.counts

  35. abbrev OAI.RowColumn.Signed.PairCountIndex line 342
  36. def OAI.RowColumn.Signed.pairCounts line 344
  37. def OAI.RowColumn.Signed.commutantData line 350

    Source documentation

    Record one matrix coefficient per joint-symbol contingency table. Zero coefficients in these representatives force every coefficient to be zero.

    def commutantData :
    Representation.IntertwiningMap (lineRepresentation (odd := odd) (k := k) line)
…

    Mentions: OAI.RowColumn.Signed.lineRepresentation

  38. lemma OAI.RowColumn.Signed.commutantData_zero line 365
  39. lemma OAI.RowColumn.Signed.commutantData_injective line 401
  40. theorem OAI.RowColumn.Signed.commutant_dimension_bound line 411

    Source documentation

    Polynomial local multiplicity infrastructure, proved directly from simultaneous signed-word orbits. This avoids assuming any LR-count estimate. For the occupied board C has 2h colors, giving exponent 4*|lines|*h².

    theorem commutant_dimension_bound :
    Module.finrank ℂ
      (Representation.IntertwiningMap (lineRepresentation (odd := odd) (k := k) line)
…

    Mentions: OAI.RowColumn.Signed.lineRepresentation