OAI/RingTheory/DirectFiniteness/IncidenceCycles.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.Planar.incidenceColoring line 12
2. lemma OAI.KaplanskyCounterexample.Planar.incidence_walk_even line 17
3. lemma OAI.KaplanskyCounterexample.Planar.getVert_even_left line 20
4. lemma OAI.KaplanskyCounterexample.Planar.getVert_odd_right line 31
5. lemma OAI.KaplanskyCounterexample.Planar.cycle_polygon_left line 44

   Source documentation

   A cycle based at a point yields its literal cyclic list of point and line vertices, without repeated vertices on either side.

   lemma cycle_polygon_left {v : V} (w : (incidenceGraph Inc).Walk (.inl v) (.inl v))
       (hw : w.IsCycle) {k : ℕ} (hk : w.length=2*k) :
       ∃ (point : Fin k → V) (line : Fin k → F), Function.Injective point ∧ Function.Injective line ∧
         (∀ i, Inc (point i) (line i)) ∧ (∀ i, Inc (point (finRotate k i)) (line i)) := by
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.incidenceGraph

6. lemma OAI.KaplanskyCounterexample.Planar.cycle_polygon line 90
7. lemma OAI.KaplanskyCounterexample.Planar.incidence_girth_of_no_short_polygon line 112

   Source documentation

   A convenient girth criterion phrased in the actual incidence lists.

   lemma incidence_girth_of_no_short_polygon
       (h : ∀ k, 2 ≤ k → k ≤ 5 → ∀ (point : Fin k → V) (line : Fin k → F),
         Function.Injective point → Function.Injective line →
         (∀ i, Inc (point i) (line i)) → (∀ i, Inc (point (finRotate k i)) (line i)) → False) :
       12 ≤ (incidenceGraph Inc).egirth := by
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.incidenceGraph