OAI/Geometry/HyperbolicGroups/PictureGenus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_after_swap_right line 16
2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components_le_glue_switch line 27
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_components_le_glue line 41
4. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_components_glue line 57

   Source documentation

   Restoring a single connection between the two new apex instances recovers exactly the previous surface components. In particular a switch can split only the affected component, into at most two components.

   theorem switch_components_glue (a b : D) (hv : M.vertex.SameCycle a b) :
       glue (M.switch a b).components a b = M.components := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.glue, OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components

5. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_components_card line 65
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_edge_a line 74
7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_edge_b line 82
8. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_components_eq_of_far_distinct line 91

   Source documentation

   When the far vertices were distinct, their merged link still joins both switched edges. Thus no component is split in this case.

   theorem switch_components_eq_of_far_distinct (a b : D)
       (hv : M.vertex.SameCycle a b)
       (hfar₁ : ¬ M.vertex.SameCycle a (M.edge a))
       (hfar₂ : ¬ M.vertex.SameCycle a (M.edge b))
       (hne : ¬ M.vertex.SameCycle (M.edge a) (M.edge b)) :
       (M.switch a b).components = M.components := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components

9. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_genusZero line 122

   Source documentation

   Genus-zero preservation under radial-label normalization. Counts refer to actual permutation cycles and their actual component quotient; Euler's bound was proved without surface classification.

   theorem switch_genusZero (hM : M.GenusZero) (a b : D) (hab : a ≠ b)
       (hv : M.vertex.SameCycle a b)
       (hfar₁ : ¬ M.vertex.SameCycle a (M.edge a))
       (hfar₂ : ¬ M.vertex.SameCycle a (M.edge b)) : (M.switch a b).GenusZero := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.GenusZero

10. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_card_of_far_same line 140

    Source documentation

    In the same-far-vertex case there are exactly TWO descendants of the old component (globally, the component count increases by one).

    theorem switch_card_of_far_same (hM : M.GenusZero) (a b : D) (hab : a ≠ b)
        (hv : M.vertex.SameCycle a b)
        (hfar₁ : ¬ M.vertex.SameCycle a (M.edge a))
        (hfar₂ : ¬ M.vertex.SameCycle a (M.edge b))
        (hf : M.vertex.SameCycle (M.edge a) (M.edge b)) :
        Nat.card (Quotient (M.switch a b).components) = Nat.card (Quotient M.components) + 1 := by
    …

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components