PlanarDiagrams.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.KaplanskyCounterexample.Planar.fixed_compl_invariant line 16
lemma OAI.KaplanskyCounterexample.Planar.WeakBalanced.exists_smaller line 26
Source documentation
Deleting a zero edge, including its now isolated endpoints, strictly reduces the finite edge set and preserves all required balances.
```
lemma WeakBalanced.exists_smaller (D : WeakBalanced R Inc ι) (hR : R.GenusZero)
    (a : α) (ha : D.weight a = 0) :
    ∃ (β : Type u) (iβ : Fintype β) (S : Ribbon β),
      @Fintype.card β iβ < Fintype.card α ∧ @Ribbon.GenusZero β iβ S ∧
        Nonempty (@WeakBalanced β V F A B iβ _ _ S Inc ι) := by
…
```
Mentions: OAI.KaplanskyCounterexample.Planar.WeakBalanced, OAI.KaplanskyCounterexample.Planar.Ribbon, OAI.KaplanskyCounterexample.Planar.Ribbon.GenusZero
structure OAI.KaplanskyCounterexample.Planar.PlanarDiagram line 49
Source documentation
A finite genus-zero comparison diagram, with its edge type retained.
```
structure PlanarDiagram (Inc : V → F → Prop) (ι : V → F → (A →+ B)) where
…
```
def OAI.KaplanskyCounterexample.Planar.PlanarDiagram.edges line 58
def OAI.KaplanskyCounterexample.Planar.PlanarDiagram.vertices line 60
lemma OAI.KaplanskyCounterexample.Planar.PlanarDiagram.exists_minimal line 63

lemma OAI.KaplanskyCounterexample.Planar.Balanced.not_genusZero line 83

Source documentation

Curvature also rules out a disconnected comparison system: its Euler characteristic is twice its positive number of components.

lemma Balanced.not_genusZero (D : Balanced R Inc ι) (hred : D.Reduced)
    (hinj : ∀ v f, Inc v f → Function.Injective (ι v f))
    (hind : ∀ v f g, Inc v f → Inc v g → f ≠ g →
      ∀ a b, ι v f a + ι v g b = 0 → a = 0)
    (hgirth : 12 ≤ (incidenceGraph Inc).egirth) : ¬ R.GenusZero := by
…

Mentions: OAI.KaplanskyCounterexample.Planar.Balanced, OAI.KaplanskyCounterexample.Planar.incidenceGraph