OAI/Geometry/HyperbolicGroups/CycleCount.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PictureSwitch.VertexClasses line 15
2. abbrev OAI.HyperbolicObstruction.PictureSwitch.Classifier line 16
3. def OAI.HyperbolicObstruction.PictureSwitch.classify line 18
4. lemma OAI.HyperbolicObstruction.PictureSwitch.classify_eq_iff line 22
5. def OAI.HyperbolicObstruction.PictureSwitch.classifierMap line 45
6. lemma OAI.HyperbolicObstruction.PictureSwitch.classifierMap_bijective line 48
7. theorem OAI.HyperbolicObstruction.PictureSwitch.cycles_eq_card_classes line 73

   Source documentation

   The numerical cycle count used in the Euler computation equals the actual finite quotient of side corners by vertex-link connectivity.

   theorem cycles_eq_card_classes (p : Perm D) :
       cycles p = Nat.card (VertexClasses p) := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles, OAI.HyperbolicObstruction.PictureSwitch.VertexClasses