OAI/RepresentationTheory/Saxl/PositionSplit.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.sumPerm line 13

   Source comment

   The genuine product position permutation under a disjoint-set enumeration.

   def sumPerm {n a b : ℕ} (e : Fin n ≃ Fin a ⊕ Fin b)
       (g : Equiv.Perm (Fin a)) (h : Equiv.Perm (Fin b)) : Equiv.Perm (Fin n) :=
   …

2. lemma OAI.Saxl.signC_sumPerm line 17
3. lemma OAI.Saxl.sumPerm_left line 22
4. lemma OAI.Saxl.sumPerm_right line 27
5. def OAI.Saxl.leftWord line 32
6. def OAI.Saxl.rightWord line 35
7. lemma OAI.Saxl.word_eq_iff_parts line 38
8. def OAI.Saxl.positionProduct line 49
9. lemma OAI.Saxl.single_positionProduct line 53
10. lemma OAI.Saxl.altWord_split_term line 63
11. theorem OAI.Saxl.altWord_split line 82

    Source comment

    Independent block permutations factor with exactly the product sign.

    theorem altWord_split {n a b d : ℕ} (e : Fin n ≃ Fin a ⊕ Fin b)
        (G : Subgroup (Equiv.Perm (Fin n))) (G₁ : Subgroup (Equiv.Perm (Fin a)))
        (G₂ : Subgroup (Equiv.Perm (Fin b))) (E : G ≃ G₁ × G₂)
        (hE : ∀ g : G, (g : Equiv.Perm (Fin n)) =
          sumPerm e ((E g).1 : Equiv.Perm (Fin a)) ((E g).2 : Equiv.Perm (Fin b)))
        (w : Fin n → Fin d) :
        altWord G w = positionProduct e (altWord G₁ (leftWord e w)) (altWord G₂ (rightWord e w)) := by
    …

    Mentions: OAI.Saxl.sumPerm, OAI.Saxl.altWord, OAI.Saxl.positionProduct, OAI.Saxl.leftWord, OAI.Saxl.rightWord

12. def OAI.Saxl.fiberGroup line 109
13. def OAI.Saxl.leftPositions line 117
14. def OAI.Saxl.rightPositions line 128
15. def OAI.Saxl.leftRestriction line 141
16. def OAI.Saxl.rightRestriction line 145
17. lemma OAI.Saxl.leftRestriction_apply line 149
18. lemma OAI.Saxl.rightRestriction_apply line 156
19. lemma OAI.Saxl.sumPerm_restrictions line 163
20. lemma OAI.Saxl.sumPerm_injective line 173
21. def OAI.Saxl.fiberSplit line 186
22. lemma OAI.Saxl.fiberSplit_apply line 221
23. theorem OAI.Saxl.altWord_fiber_split line 226

    Source comment

    Exact independent-block factorization for arbitrary row/column labels.

    theorem altWord_fiber_split {n a b d : ℕ} {α : Type uAlpha} (e : Fin n ≃ Fin a ⊕ Fin b)
        (f : Fin n → α) (w : Fin n → Fin d) :
        altWord (fiberGroup f ⊓ sectorGroup (fun i => (e i).isLeft = true)) w =
          positionProduct e
            (altWord (fiberGroup (fun i => f (e.symm (Sum.inl i)))) (leftWord e w))
            (altWord (fiberGroup (fun i => f (e.symm (Sum.inr i)))) (rightWord e w)) := by
    …

    Mentions: OAI.Saxl.altWord, OAI.Saxl.fiberGroup, OAI.Saxl.sectorGroup, OAI.Saxl.positionProduct, OAI.Saxl.leftWord, OAI.Saxl.rightWord

24. lemma OAI.Saxl.staircase_colLen line 237