PermSwitch.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PictureSwitch.split_list line 18
Source documentation
Cutting a cyclic vertex-link immediately before two distinct corners splits it into exactly the displayed two cyclic lists. Singleton cycles are retained: they are genuine vertex instances, even though their permutation is the identity.
```
theorem split_list (a b : D) (l m : List D)
    (h : (a :: l ++ b :: m).Nodup) :
    swap a b * (a :: l ++ b :: m).formPerm =
      (a :: l).formPerm * (b :: m).formPerm := by
…
```
def OAI.HyperbolicObstruction.PictureSwitch.defect line 45
Source documentation
Number of darts minus number of vertex cycles, including singleton cycles. The integer form avoids artificial truncated-subtraction side conditions.
```
def defect (p : Perm D) : ℤ := p.support.card - p.cycleType.card
```
def OAI.HyperbolicObstruction.PictureSwitch.cycles line 47
lemma OAI.HyperbolicObstruction.PictureSwitch.defect_disjoint line 49
lemma OAI.HyperbolicObstruction.PictureSwitch.defect_list line 54
lemma OAI.HyperbolicObstruction.PictureSwitch.disjoint_lists line 67
lemma OAI.HyperbolicObstruction.PictureSwitch.defect_split_list line 76
lemma OAI.HyperbolicObstruction.PictureSwitch.remainder_disjoint line 92
theorem OAI.HyperbolicObstruction.PictureSwitch.cycles_split line 107
Source documentation
A transposition between two corners of one vertex splits that vertex. This includes the extremal cut creating one or two valence-one vertices.
```
theorem cycles_split (p : Perm D) {a b : D} (hab : a ≠ b)
    (hsame : p.SameCycle a b) : cycles (swap a b * p) = cycles p + 1 := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles
lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_after_swap line 158
Source documentation
A cut between two different vertex cycles joins them. The finite intersection argument handles fixed points without excluding empty links.
```
lemma sameCycle_after_swap (p : Perm D) {a b : D}
    (h : ¬ p.SameCycle a b) : (swap a b * p).SameCycle a b := by
…
```
theorem OAI.HyperbolicObstruction.PictureSwitch.cycles_merge line 185
theorem OAI.HyperbolicObstruction.PictureSwitch.cycles_split_right line 192
Source documentation
Right multiplication cuts the outgoing ends instead of the incoming ends.
```
theorem cycles_split_right (p : Perm D) {a b : D} (hab : a ≠ b)
    (h : p.SameCycle a b) : cycles (p * swap a b) = cycles p + 1 := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles
theorem OAI.HyperbolicObstruction.PictureSwitch.cycles_merge_right line 197
lemma OAI.HyperbolicObstruction.PictureSwitch.cycles_eq_fixed_add line 203
lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_agree line 213
Source documentation
Agreement on a whole old cycle determines the new cycle, in both directions. Finiteness is used only to replace integer powers by naturals.
```
lemma sameCycle_agree (p q : Perm D) (x : D)
    (h : ∀ y, p.SameCycle x y → q y = p y) (y : D) :
    q.SameCycle x y ↔ p.SameCycle x y := by
…
```
lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_right_swap_away line 228
lemma OAI.HyperbolicObstruction.PictureSwitch.notSameCycle_after_split line 237