OAI/Geometry/HyperbolicGroups/PictureEuler.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components line 22

   Source documentation

   Connected components of the actual polygon identifications on darts.

   def components : Setoid D := SameCycle.setoid M.vertex ⊔ SameCycle.setoid M.edge
   …

2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertex_le_components line 25
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.edge_le_components line 27
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.face_le_components line 30
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components_le line 37
6. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.euler_le line 45

   Source documentation

   Euler's upper bound for every finite oriented side-pairing, without assuming a drawing or the surface classification theorem.

   theorem euler_le : M.euler ≤ 2 * (Nat.card (Quotient M.components) : ℤ) := by
   …

7. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.GenusZero line 80

   Source documentation

   Combinatorial genus zero, expressed directly on the actual side-pairing. This definition neither asserts nor replaces a topological realization.

   def GenusZero : Prop := M.euler = 2 * (Nat.card (Quotient M.components) : ℤ)
   …