OAI/RingTheory/DirectFiniteness/RibbonGeometry.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KaplanskyCounterexample.Planar.Cycles line 17

   Source documentation

   Vertex cycles of a rotation, including the cycles of length one.

   abbrev Cycles (p : Perm α) := Quotient (SameCycle.setoid p)

2. def OAI.KaplanskyCounterexample.Planar.cycleClass line 19
3. def OAI.KaplanskyCounterexample.Planar.cycleSet line 21
4. lemma OAI.KaplanskyCounterexample.Planar.mem_cycleSet line 24
5. lemma OAI.KaplanskyCounterexample.Planar.cycleClass_eq line 28
6. lemma OAI.KaplanskyCounterexample.Planar.cycleSet_nonempty line 31
7. lemma OAI.KaplanskyCounterexample.Planar.cycles_sum_card line 35
8. structure OAI.KaplanskyCounterexample.Planar.Ribbon line 43

   Source documentation

   A bipartite rotation system. Each edge is oriented from black to white; rotations at its two endpoints are permutations of the whole edge set.

   structure Ribbon (α : Type u_2) where
   …

9. def OAI.KaplanskyCounterexample.Planar.Ribbon.face line 47
10. def OAI.KaplanskyCounterexample.Planar.Ribbon.Spherical line 49
11. def OAI.KaplanskyCounterexample.Planar.Ribbon.mergeWhite line 55

    Source documentation

    Local surgery merging two white vertices along consecutive black edges. The newly created digon is a one-cycle of the face permutation.

    def Ribbon.mergeWhite (R : Ribbon α) (e : α) : Ribbon α where
    …

    Mentions: OAI.KaplanskyCounterexample.Planar.Ribbon

12. lemma OAI.KaplanskyCounterexample.Planar.mergeWhite_face line 60
13. lemma OAI.KaplanskyCounterexample.Planar.mergeWhite_face_fixed line 65
14. lemma OAI.KaplanskyCounterexample.Planar.sameCycle_map line 71

    Source documentation

    A map taking steps of one permutation to cycles of another takes whole cycles to cycles.

    lemma sameCycle_map {β : Type u_3} (p : Perm α) (q : Perm β) (f : α → β)
        (hstep : ∀ x, q.SameCycle (f x) (f (p x))) {x y : α}
        (hxy : p.SameCycle x y) : q.SameCycle (f x) (f y) := by
    …

15. def OAI.KaplanskyCounterexample.Planar.unplug line 83

    Source documentation

    Unplug an edge from its face cycle; the edge becomes a singleton cycle.

    def unplug (p : Perm α) (a : α) : Perm α := swap a (p a) * p

16. def OAI.KaplanskyCounterexample.Planar.bypass line 85
17. lemma OAI.KaplanskyCounterexample.Planar.unplug_fixed line 88
18. lemma OAI.KaplanskyCounterexample.Planar.unplug_sameCycle line 91
19. lemma OAI.KaplanskyCounterexample.Planar.sameCycle_bypass line 106
20. lemma OAI.KaplanskyCounterexample.Planar.unplug_sameCycle_iff line 127
21. lemma OAI.KaplanskyCounterexample.Planar.bypass_ne line 134
22. def OAI.KaplanskyCounterexample.Planar.unplugCycleEquiv line 139

    Source documentation

    Splicing a nontrivial cycle at a point adds exactly one singleton cycle.

    def unplugCycleEquiv (p : Perm α) (a : α) (ha : p a ≠ a) :
        Cycles p ≃ {c : Cycles (unplug p a) // c ≠ cycleClass (unplug p a) a} where
    …

    Mentions: OAI.KaplanskyCounterexample.Planar.Cycles, OAI.KaplanskyCounterexample.Planar.unplug, OAI.KaplanskyCounterexample.Planar.cycleClass

23. lemma OAI.KaplanskyCounterexample.Planar.unplug_cycles_card line 166
24. lemma OAI.KaplanskyCounterexample.Planar.swap_mul_sameCycle line 177

    Source documentation

    A transposition between two different cycles joins them. The orbit link is proved directly by following the first return in one of the old cycles.

    lemma swap_mul_sameCycle (p : Perm α) (a b : α) (hab : ¬ p.SameCycle a b) :
        (swap a b * p).SameCycle a b := by
    …

25. lemma OAI.KaplanskyCounterexample.Planar.sameCycle_swap_mul line 211

    Source documentation

    Old cycles remain connected after a transposition joining distinct cycles.

    lemma sameCycle_swap_mul (p : Perm α) (a b : α) (hab : ¬ p.SameCycle a b)
        {x y : α} (hxy : p.SameCycle x y) : (swap a b * p).SameCycle x y := by
    …

26. def OAI.KaplanskyCounterexample.Planar.mergedClass line 229

    Source documentation

    The quotient of the old vertex set that identifies precisely the two vertices joined by the transposition.

    def mergedClass (p : Perm α) (a b : α) (x : α) : Cycles p :=
    …

    Mentions: OAI.KaplanskyCounterexample.Planar.Cycles

27. lemma OAI.KaplanskyCounterexample.Planar.cycleClass_apply line 233
28. lemma OAI.KaplanskyCounterexample.Planar.mergedClass_step line 238
29. lemma OAI.KaplanskyCounterexample.Planar.mergedClass_cycle line 252
30. def OAI.KaplanskyCounterexample.Planar.mergeCycleEquiv line 264

    Source documentation

    Joining two different cycles deletes exactly one vertex.

    def mergeCycleEquiv (p : Perm α) (a b : α) (hab : ¬ p.SameCycle a b) :
        Cycles (swap a b * p) ≃ {c : Cycles p // c ≠ cycleClass p b} where
    …

    Mentions: OAI.KaplanskyCounterexample.Planar.Cycles, OAI.KaplanskyCounterexample.Planar.cycleClass

31. lemma OAI.KaplanskyCounterexample.Planar.swap_mul_cycles_card line 291
32. lemma OAI.KaplanskyCounterexample.Planar.mergeWhite_spherical line 299
33. theorem OAI.KaplanskyCounterexample.Planar.euler_contradiction line 318