OAI/Geometry/HyperbolicGroups/SubpairingCopies.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PictureSwitch.PictureMap.RetainedContact line 18
2. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.retainedContactEdge line 20
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.retained_raw_edge line 25
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.retained_contact_card line 31
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.retained_contact_covers line 41
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_edges_subset_retained line 50
7. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.tree_retained_contacts_bijective line 69

   Source documentation

   A one-boundary spanning subpairing has exactly one retained contact for each edge of its underlying tree. Euler and connectivity rule out BOTH loops and parallel copies, rather than silently forgetting them.

   theorem tree_retained_contacts_bijective (hG : M.GenusZero)
       (hspan : SameCycle.setoid M.vertex ⊔ SameCycle.setoid q = ⊤)
       (hboundary : cycles (M.vertex*q) = 1) :
       Function.Injective (M.retainedContactEdge q) ∧
       (M.subpairingGraph q (M.subpairing_sq q hq)).edgeFinset =
         Finset.univ.image (M.retainedContactEdge q) := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles