OAI/RingTheory/DirectFiniteness/FiniteAffine.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyCounterexample.FiniteGeometry.cosetPoints line 13

    Source documentation

    Full finite affine cosets; no subset or segment convention is used.

    def cosetPoints (U : Submodule Q A) (x : A) : Finset A :=
…
  2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.mem_cosetPoints line 16
  3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.self_mem_cosetPoints line 19
  4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.cosetPoints_eq line 21
  5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.cosetPoints_image line 31
  6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.card_cosetPoints line 41
  7. lemma OAI.KaplanskyCounterexample.FiniteGeometry.intersection_cosets_card_le line 47
  8. lemma OAI.KaplanskyCounterexample.FiniteGeometry.intersection_cosets_card_le_one line 61

    Source documentation

    Two independent directions yield disjoint affine cosets or a single point.

    lemma intersection_cosets_card_le_one (U W : Submodule Q A) (h : Disjoint U W) (x o : A) :
    ((cosetPoints U x) ∩ (cosetPoints W o)).card ≤ 1 := by
…

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.cosetPoints

  9. def OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset line 68

    Source documentation

    A coset variable is its full point set, so no arbitrary representatives enter the random choices.

    def AffineCoset (U : Submodule Q A) := {C : Finset A // ∃ x, C = cosetPoints U x}
…

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.cosetPoints

  10. def OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset.of line 73
  11. instance OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset.(instance at line 75) line 75
  12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset.of_surjective line 79
  13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset.card_le line 83
  14. lemma OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset.card line 86
  15. lemma OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset.nonempty line 90
  16. lemma OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset.eq_of_mem line 94
  17. lemma OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset.mem_iff line 101
  18. lemma OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset.of_eq_iff line 107
  19. lemma OAI.KaplanskyCounterexample.FiniteGeometry.AffineCoset.add_mem_iff line 111
  20. def OAI.KaplanskyCounterexample.FiniteGeometry.linePoints line 125

    Source documentation

    A direction vector parametrizes every point of its full line.

    def linePoints (x v : A) : Finset A := Finset.univ.image (fun t : Q => x + t • v)
…
  21. lemma OAI.KaplanskyCounterexample.FiniteGeometry.lineParam_injective line 128
  22. lemma OAI.KaplanskyCounterexample.FiniteGeometry.card_linePoints line 134
  23. lemma OAI.KaplanskyCounterexample.FiniteGeometry.base_mem_linePoints line 139
  24. lemma OAI.KaplanskyCounterexample.FiniteGeometry.linePoints_eq_coset line 143
  25. def OAI.KaplanskyCounterexample.FiniteGeometry.FullLine line 155

    Source documentation

    Affine lines are identified by their actual point sets.

    def FullLine (s : Finset A) : Prop := ∃ x v : A, v ≠ 0 ∧ s = linePoints (Q := Q) x v
…

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.linePoints

  26. lemma OAI.KaplanskyCounterexample.FiniteGeometry.FullLine.card line 158
  27. lemma OAI.KaplanskyCounterexample.FiniteGeometry.FullLine.nonempty line 163