OAI/Geometry/HyperbolicGroups/PictureTriangulationEuler.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.star_vertex_lift line 22
2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.star_center_lift line 33
3. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.starVertexClass line 40

   Source documentation

   The new vertices are exactly the old vertices plus the separate centers of the old faces. This retains all original vertex identifications.

   def starVertexClass : StarDart D → M.GraphVertex ⊕ Quotient (SameCycle.setoid M.face)
     | .inl x => .inl (M.vertexClass x)
     | .inr (.inl x) => .inl (M.vertexClass (M.face x))
     | .inr (.inr x) => .inr (Quotient.mk _ x)
   
   omit [DecidableEq D] [Fintype D] in

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.StarDart

4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.starVertexClass_step line 46
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.star_vertex_cycle line 57
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.starVertexClass_surjective line 88
7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_vertex_cycles line 96
8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.star_components_lift line 102
9. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.starComponent line 114
10. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.star_components line 118
11. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_components_card line 136
12. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_euler line 143
13. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_genusZero line 153

    Source documentation

    Literal face starring preserves genus zero and connected-component count; its dual is therefore a genuine degree-three genus-zero ribbon graph.

    theorem triangulation_genusZero (h : M.GenusZero) : M.triangulation.GenusZero := by
    …