OAI/GroupTheory/Kervaire/Components.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KervaireRibbon.classes line 14
2. def OAI.KervaireRibbon.joinPair line 15
3. lemma OAI.KervaireRibbon.cycle_le_of_step line 17
4. lemma OAI.KervaireRibbon.cycle_swap_le line 23
5. lemma OAI.KervaireRibbon.joinPair_eq line 33
6. lemma OAI.KervaireRibbon.le_joinPair line 36
7. lemma OAI.KervaireRibbon.joinPair_rel line 38
8. lemma OAI.KervaireRibbon.classes_joinPair line 44
9. lemma OAI.KervaireRibbon.cycles_swap_le line 93
10. lemma OAI.KervaireRibbon.numCycles_swap_le line 102
11. def OAI.KervaireRibbon.attachEdges line 115

    Source documentation

    Successively attach the edges, retaining the component equivalence relation.

    def attachEdges (r : Setoid D) (l : List (D × D)) : Setoid D :=
    …

12. def OAI.KervaireRibbon.edgePerm line 117
13. lemma OAI.KervaireRibbon.euler_edges line 120
14. lemma OAI.KervaireRibbon.euler_edges_connected line 138
15. lemma OAI.KervaireRibbon.numCycles_one line 156
16. lemma OAI.KervaireRibbon.numCycles_conj line 160
17. lemma OAI.KervaireRibbon.numCycles_mul_comm line 169
18. lemma OAI.KervaireRibbon.cycles_swap_sup line 173
19. lemma OAI.KervaireRibbon.edgePerm_append line 183
20. lemma OAI.KervaireRibbon.attachEdges_append line 186
21. lemma OAI.KervaireRibbon.edgePerm_mul line 190
22. lemma OAI.KervaireRibbon.exists_minimal_edges line 198
23. lemma OAI.KervaireRibbon.euler_inequality line 236

    Source documentation

    The finite combinatorial Euler inequality, including all fixed points and all components. No surface classification or topological assertion is assumed.

    lemma euler_inequality (σ θ : Equiv.Perm D) :
        numCycles σ + numCycles θ + numCycles (σ*θ) ≤
          Fintype.card D + 2*classes (SameCycle.setoid σ ⊔ SameCycle.setoid θ) := by
    …

    Mentions: OAI.KervaireRibbon.numCycles, OAI.KervaireRibbon.classes