OAI/GroupTheory/Hyperbolic/Planarity.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Release075.PermCycles.swap_sameCycle_away line 11

   Source documentation

   A swap supported in other colors leaves this entire orbit unchanged.

   theorem swap_sameCycle_away {C : Type*} (f : Perm A) (color : A → C)
       (hcolor : ∀ z, color (f z) = color z) (a b x y : A)
       (ha : color x ≠ color a) (hb : color x ≠ color b) :
       (Equiv.swap a b * f).SameCycle x y ↔ f.SameCycle x y := by
   …

2. theorem OAI.Release075.PermCycles.swap_rel line 39
3. theorem OAI.Release075.PermCycles.sameCycle_conjugate_swap_le line 49
4. theorem OAI.Release075.PermCycles.components_conjugate_swap line 60

   Source documentation

   A local re-pairing can only split off one further component, provided its slots belonged to the same old component. This includes reconnected slots.

   theorem components_conjugate_swap (f g : Perm A) {a b : A}
       (hab : components f g a b) :
       components f g = joinPair (components (Equiv.swap a b * f * Equiv.swap a b) g) a b := by
   …

   Mentions: OAI.Release075.PermCycles.components, OAI.Release075.PermCycles.joinPair

5. def OAI.Release075.PermCycles.rePair line 84

   Source documentation

   Change the pairing on two edges, creating pairs (a,b) and (reverse a, reverse b). Formulated by conjugation, so involutivity and absence of fixed points are inherited rather than assumed for the result.

   noncomputable def rePair (reverse : Perm A) (a b : A) : Perm A :=
   …

6. theorem OAI.Release075.PermCycles.rePair_vertex line 88
7. theorem OAI.Release075.PermCycles.cycleCount_conj line 97
8. theorem OAI.Release075.PermCycles.cycleCount_rePair line 105
9. theorem OAI.Release075.PermCycles.rePair_involutive line 110
10. theorem OAI.Release075.PermCycles.rePair_ne line 117
11. theorem OAI.Release075.PermCycles.color_swap line 125
12. theorem OAI.Release075.PermCycles.rePair_apply_a line 136
13. theorem OAI.Release075.PermCycles.rePair_apply_reverse_a line 142
14. def OAI.Release075.PermCycles.PlanarMap line 149

    Source documentation

    Genus zero for every connected component, expressed without an embedding or an unproved Jordan-curve theorem. This uses the universal Euler upper bound.

    def PlanarMap (reverse face : Perm A) : Prop :=
    …

15. theorem OAI.Release075.PermCycles.planar_rePair line 153
16. theorem OAI.Release075.PermCycles.invariant_pred_sameCycle line 248
17. theorem OAI.Release075.PermCycles.card_quotient_partition line 257

    Source documentation

    Decompose the number of classes along a union of equivalence classes.

    theorem card_quotient_partition (s : Setoid A) (p : A → Prop)
        (hp : ∀ a b, s a b → (p a ↔ p b)) :
        Nat.card (Quotient s) = Nat.card (Quotient (s.comap (Subtype.val : {a // p a} → A))) +
          Nat.card (Quotient (s.comap (Subtype.val : {a // ¬p a} → A))) := by
    …

18. theorem OAI.Release075.PermCycles.cycleCount_partition line 269
19. theorem OAI.Release075.PermCycles.components_subtype line 283

    Source documentation

    Restriction to an invariant set commutes with connected components.

    theorem components_subtype (f g : Perm A) (p : A → Prop)
        (hf : ∀ a, p (f a) ↔ p a) (hg : ∀ a, p (g a) ↔ p a) :
        components (f.subtypePerm hf) (g.subtypePerm hg) = (components f g).comap Subtype.val := by
    …

    Mentions: OAI.Release075.PermCycles.components

20. theorem OAI.Release075.PermCycles.componentCount_partition line 325
21. theorem OAI.Release075.PermCycles.PlanarMap.restrict line 338

    Source documentation

    Genus-zero is inherited by every union of connected components.

    theorem PlanarMap.restrict {f g : Perm A} (h : PlanarMap f g) (p : A → Prop)
        (hf : ∀ a, p (f a) ↔ p a) (hg : ∀ a, p (g a) ↔ p a) :
        PlanarMap (f.subtypePerm hf) (g.subtypePerm hg) := by
    …

    Mentions: OAI.Release075.PermCycles.PlanarMap

22. theorem OAI.Release075.PermCycles.pow_intertwine line 365
23. theorem OAI.Release075.PermCycles.sameCycle_intertwine line 372
24. theorem OAI.Release075.PermCycles.cycleCount_intertwine line 383
25. theorem OAI.Release075.PermCycles.components_map line 388
26. theorem OAI.Release075.PermCycles.components_intertwine line 405
27. theorem OAI.Release075.PermCycles.componentCount_intertwine line 420
28. def OAI.Release075.PermCycles.leftPred line 425
29. def OAI.Release075.PermCycles.leftEquiv line 427
30. def OAI.Release075.PermCycles.rightEquiv line 435
31. theorem OAI.Release075.PermCycles.leftPred_sumCongr line 444
32. theorem OAI.Release075.PermCycles.leftEquiv_intertwine line 448
33. theorem OAI.Release075.PermCycles.rightEquiv_intertwine line 454
34. theorem OAI.Release075.PermCycles.cycleCount_sum line 460
35. theorem OAI.Release075.PermCycles.componentCount_sum line 466
36. theorem OAI.Release075.PermCycles.sum_mul line 476
37. theorem OAI.Release075.PermCycles.PlanarMap.sum line 480