OAI/RingTheory/DirectFiniteness/RibbonSplitting.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.Planar.Ribbon.swapBlack line 15
2. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.swapBlack_twice line 19
3. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.swapBlack_face line 25
4. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.swapBlack_components_merge line 30
5. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.not_blackCycle_of_not_component line 53
6. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.not_white_faceCycle_of_not_component line 57
7. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.genusZero_swapBlack_merge line 65

   Source documentation

   Gluing black vertices from distinct connected components preserves genus zero.

   lemma Ribbon.genusZero_swapBlack_merge (R : Ribbon α) (hR : R.GenusZero) (a b : α)
       (hab : ¬ R.components.r a b) : (R.swapBlack a b).GenusZero := by
   …

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

8. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.genusZero_swapBlack_split line 82

   Source documentation

   Splitting one black vertex preserves genus zero, even when the split separates its connected component into two.

   lemma Ribbon.genusZero_swapBlack_split (R : Ribbon α) (hR : R.GenusZero) (a b : α)
       (hne : a ≠ b) (hab : R.black.SameCycle a b) : (R.swapBlack a b).GenusZero := by
   …

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