OAI/RingTheory/DirectFiniteness/IncidenceDirections.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.IncidenceDirections.directionMap line 12
2. lemma OAI.KaplanskyCounterexample.IncidenceDirections.directionMap_injective line 22
3. lemma OAI.KaplanskyCounterexample.IncidenceDirections.directionMap_independent line 27
4. lemma OAI.KaplanskyCounterexample.IncidenceDirections.directionMap_covers line 38
5. def OAI.KaplanskyCounterexample.IncidenceDirections.nonzeroEquiv line 54

   Source documentation

   Every nonzero vector lies on exactly one of these parametrized lines.

   def nonzeroEquiv : (Option K × {c : K // c ≠ 0}) ≃ {a : Fin 2 → K // a ≠ 0} :=
   …

6. lemma OAI.KaplanskyCounterexample.IncidenceDirections.nonzeroEquiv_apply line 71
7. lemma OAI.KaplanskyCounterexample.IncidenceDirections.sum_directions line 75

   Source documentation

   The local subgroup decomposition, before applying a group-ring map.

   lemma sum_directions [Fintype K] {M : Type u_2} [AddCommGroup M]
       (f : (Fin 2 → K) → M) :
       ∑ a : Fin 2 → K, f a = f 0 + ∑ d : Option K, (∑ c : K, f (directionMap d c) - f 0) := by
   …

   Mentions: OAI.KaplanskyCounterexample.IncidenceDirections.directionMap

8. def OAI.KaplanskyCounterexample.IncidenceDirections.incidenceEquiv line 89

   Source documentation

   At a point, assign the incident lines bijectively to all slopes.

   def incidenceEquiv (hdeg : ∀ v, Fintype.card {f : F // v ∈ Inc f} = ℓ + 1)
       (v : V) : {f : F // v ∈ Inc f} ≃ Option (ZMod ℓ) :=
   …

9. def OAI.KaplanskyCounterexample.IncidenceDirections.incidenceMap line 93
10. lemma OAI.KaplanskyCounterexample.IncidenceDirections.incidenceMap_injective line 97
11. lemma OAI.KaplanskyCounterexample.IncidenceDirections.incidenceMap_independent line 101
12. lemma OAI.KaplanskyCounterexample.IncidenceDirections.incidenceMap_covers line 107