OAI/GroupTheory/Kervaire/Suppression.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KervaireRibbon.erase line 14
2. lemma OAI.KervaireRibbon.erase_fixed line 17
3. lemma OAI.KervaireRibbon.erase_apply line 20
4. lemma OAI.KervaireRibbon.numCycles_erase line 27
5. lemma OAI.KervaireRibbon.cycles_erase_le line 31
6. lemma OAI.KervaireRibbon.sameCycle_erase line 37
7. lemma OAI.KervaireRibbon.classes_le_of_le line 62
8. lemma OAI.KervaireRibbon.classes_joinPair_le line 67
9. def OAI.KervaireRibbon.components line 72
10. def OAI.KervaireRibbon.planar line 74
11. lemma OAI.KervaireRibbon.components_swap_sup line 77
12. lemma OAI.KervaireRibbon.planar_vertex_split line 85

    Source documentation

    Splitting a vertex of a planar ribbon permutation preserves planarity. The proof uses only the finite Euler inequality and the exact cycle split/merge count.

    lemma planar_vertex_split (σ θ : Equiv.Perm D) {x y : D} (hne : x ≠ y)
        (hxy : σ.SameCycle x y) (hp : planar σ θ) : planar (swap x y * σ) θ := by
    …

    Mentions: OAI.KervaireRibbon.planar

13. lemma OAI.KervaireRibbon.cycles_mul_le line 127
14. lemma OAI.KervaireRibbon.components_fixed_le line 134
15. lemma OAI.KervaireRibbon.components_eq_of_fixed line 146
16. lemma OAI.KervaireRibbon.planar_vertex_split_separates line 152
17. def OAI.KervaireRibbon.suppress line 169

    Source documentation

    Suppress a two-valent vertex, retaining its two darts as isolated markers.

    def suppress (θ : Equiv.Perm D) (x y : D) : Equiv.Perm D :=
    …

18. lemma OAI.KervaireRibbon.suppress_apply line 173
19. lemma OAI.KervaireRibbon.suppress_other line 184
20. lemma OAI.KervaireRibbon.suppress_involutive line 194
21. lemma OAI.KervaireRibbon.numCycles_suppress line 212
22. lemma OAI.KervaireRibbon.suppress_faces line 223
23. lemma OAI.KervaireRibbon.components_suppress line 259
24. lemma OAI.KervaireRibbon.classes_suppress line 290
25. lemma OAI.KervaireRibbon.planar_suppress line 321