OAI/RingTheory/DirectFiniteness/CandidateClassification.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.transverse line 16
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.exceptional_scalar_sum line 21
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.exceptional_occurs_twice_single_slope line 43
4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.all_labels_twice_length line 58
5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.one_generic_rectangle line 75

   Source documentation

   With at most one generic label every occurring label occurs twice, so the candidate is a four-step rectangle.

   lemma one_generic_rectangle {k : ℕ} (s : Fin k → PolygonStep Q R E)
       (hk3 : 3 ≤ k) (hk5 : k ≤ 5) (hz : ∑ i, (s i).vector F = 0)
       (hadj : ∀ i, (s i).label ≠ (s (finRotate k i)).label)
       (j : R × Q) (honly : ∀ i (g : GenericStep Q R E), s i = .inl g → g.label = j) :
       k = 4 ∧ (Finset.univ.image (fun i => (s i).label)).card = 2 := by
   …

   Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep, OAI.KaplanskyCounterexample.FiniteGeometry.GenericStep

6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.singleton_exceptional_two_slopes line 92

   Source documentation

   A lone exceptional step requires two different generic slopes in its own bundle. This is the cancellation needed for the pentagon count.

   lemma singleton_exceptional_two_slopes {k : ℕ} (s : Fin k → PolygonStep Q R E)
       (hk : k ≤ 5) (hz : ∑ i, (s i).vector F = 0) (r : R)
       (hc : (Finset.univ.filter (fun i => (s i).label = .inr r)).card = 1) :
       ∃ (i i' : Fin k) (g g' : GenericStep Q R E), s i = .inl g ∧ s i' = .inl g' ∧
         g.label.1 = r ∧ g'.label.1 = r ∧ g.label.2 ≠ g'.label.2 := by
   …

   Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.PolygonStep, OAI.KaplanskyCounterexample.FiniteGeometry.GenericStep