OAI/RingTheory/DirectFiniteness/PlanarBalance.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.KaplanskyCounterexample.Planar.Balanced line 15
2. def OAI.KaplanskyCounterexample.Planar.Balanced.Reduced line 31
3. lemma OAI.KaplanskyCounterexample.Planar.cycleClass_perm line 37
4. lemma OAI.KaplanskyCounterexample.Planar.mem_cycleSet_perm line 41
5. lemma OAI.KaplanskyCounterexample.Planar.cycleSet_pair_perm line 46
6. lemma OAI.KaplanskyCounterexample.Planar.Balanced.white_degree line 57
7. lemma OAI.KaplanskyCounterexample.Planar.Balanced.black_degree line 74
8. lemma OAI.KaplanskyCounterexample.Planar.cycleSet_singleton_of_fixed line 107
9. lemma OAI.KaplanskyCounterexample.Planar.cycleSet_card_pow line 114
10. def OAI.KaplanskyCounterexample.Planar.incidenceGraph line 126

    Source documentation

    The bipartite incidence graph; its extended girth is infinite for a forest.

    def incidenceGraph (Inc : V → F → Prop) : SimpleGraph (Sum V F) where
    …

11. lemma OAI.KaplanskyCounterexample.Planar.Balanced.black_not_fixed line 136
12. lemma OAI.KaplanskyCounterexample.Planar.Balanced.white_fixed_exception line 143
13. def OAI.KaplanskyCounterexample.Planar.Balanced.exceptionEdge line 151
14. lemma OAI.KaplanskyCounterexample.Planar.Balanced.exceptionEdge_mem line 154
15. def OAI.KaplanskyCounterexample.Planar.Balanced.exceptionFace line 158
16. lemma OAI.KaplanskyCounterexample.Planar.Balanced.white_not_fixed_on_other_face line 161
17. def OAI.KaplanskyCounterexample.Planar.Balanced.halfStep line 176

    Source documentation

    Traversing one black turn and then the following white turn of a face.

    def Balanced.halfStep (D : Balanced R Inc ι) (a : α) :
        (incidenceGraph Inc).Walk (.inr (D.whiteLabel a)) (.inr (D.whiteLabel (R.face a))) :=
    …

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

18. lemma OAI.KaplanskyCounterexample.Planar.Balanced.halfStep_length line 183
19. def OAI.KaplanskyCounterexample.Planar.Balanced.boundary line 187

    Source documentation

    An initial segment of the facial boundary, with two edge sides per step.

    def Balanced.boundary (D : Balanced R Inc ι) (a : α) : (n : ℕ) →
        (incidenceGraph Inc).Walk (.inr (D.whiteLabel a))
          (.inr (D.whiteLabel ((R.face ^ n) a)))
      | 0 => .nil
      | n + 1 => (D.halfStep a).append ((D.boundary (R.face a) n).copy rfl (by
          simp only [pow_succ, Perm.mul_apply]))

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

20. lemma OAI.KaplanskyCounterexample.Planar.Balanced.boundary_length line 194
21. lemma OAI.KaplanskyCounterexample.Planar.Balanced.boundary_getVert_even line 203
22. lemma OAI.KaplanskyCounterexample.Planar.Balanced.boundary_getVert_odd line 221
23. lemma OAI.KaplanskyCounterexample.Planar.cycleClass_pow line 238
24. lemma OAI.KaplanskyCounterexample.Planar.Balanced.boundary_reduced line 242
25. lemma OAI.KaplanskyCounterexample.Planar.Balanced.face_degree line 274
26. theorem OAI.KaplanskyCounterexample.Planar.Balanced.not_spherical line 308

    Source documentation

    The curvature obstruction in the local-subgroup embedding proof, with every facial girth bound derived rather than assumed.

    theorem Balanced.not_spherical (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 → ∀ x y,
          ι v f x + ι v g y = 0 → x = 0)
        (hgirth : 12 ≤ (incidenceGraph Inc).egirth) : ¬ R.Spherical := by
    …

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