OAI/RingTheory/DirectFiniteness/DetachmentGenus.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.face_step line 16
2. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.sameCycle_face_components line 19
3. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.detach_components_card line 22
4. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.detach_components_card_black_fixed line 47
5. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.detach_components_card_white_fixed line 57
6. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.detach_face_black_fixed line 68
7. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.detach_face_white_fixed line 76
8. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.detach_face_card_separating line 82
9. theorem OAI.KaplanskyCounterexample.Planar.Ribbon.genusZero_detach line 112

   Source documentation

   Edge deletion preserves genus zero, including when deletion separates a component or removes a vertex of degree one. The detached edge is represented as an isolated one-edge component until restriction discards it.

   theorem Ribbon.genusZero_detach (R : Ribbon α) (hR : R.GenusZero) (a : α) :
       (R.detach a).GenusZero := by
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.Ribbon, OAI.KaplanskyCounterexample.Planar.Ribbon.GenusZero