Working

ElementarGeometrie/Affine/Desargues.lean

@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
 -/
 import ElementarGeometrie.Affine.Plane
 

ElementarGeometrie/Affine/Pappus.lean

@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
 -/
 import ElementarGeometrie.Affine.Desargues
 

ElementarGeometrie/Affine/Plane.lean

@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
 -/
 import ElementarGeometrie.Incidence.Basic
 

ElementarGeometrie/Examples.lean

@@ -1,8 +1,11 @@
 /-
 Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
 -/
 import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
+import Mathlib.LinearAlgebra.Dimension.Constructions
 import ElementarGeometrie.Affine.Pappus
 
 /-!
@@ -12,15 +15,16 @@ This file collects the standard concrete models tying the abstract structures
 together: the **standard affine incidence plane** `K²` over a division ring `K`,
 and the real plane `ℝ²` as the special case `K = ℝ`.
 
-The incidence axioms of `K²` are recorded as proof obligations and currently left
-as `sorry`. We also state the *coordinatization theorem*: an affine incidence
-plane has the Desargues property if and only if it is isomorphic to some `K²`.
+The four axioms of an affine incidence plane are proven for `K²`. We also state
+the *coordinatization theorem*: an affine incidence plane has the Desargues
+property if and only if it is isomorphic to some `K²`.
 
 The deeper characterization of `ℝ²` among Pappus planes (via an order-complete
 betweenness relation) is left for future work.
 
 ## Main definitions
 
+* `standardLine` : a line `p + K • v` of `K²`.
 * `standardAffineLines` : the lines of `K²`.
 * `standardAffinePlane` : `K²` as an affine incidence plane.
 * `realAffinePlane` : the real plane `ℝ²`.
@@ -28,19 +32,136 @@ betweenness relation) is left for future work.
 
 universe u
 
+variable {K : Type u} [DivisionRing K]
+
+/-- The line `p + K • v` of `K²` through `p` with direction `v`. -/
+def standardLine (p v : K × K) : Set (K × K) := {z | ∃ t : K, z = p + t • v}
+
+theorem mem_standardLine {p v z : K × K} :
+    z ∈ standardLine p v ↔ ∃ t : K, z = p + t • v := Iff.rfl
+
+/-- A line may be re-based at any of its points without changing it. -/
+theorem standardLine_rebase {p v x : K × K} (hx : x ∈ standardLine p v) :
+    standardLine p v = standardLine x v := by
+  obtain ⟨s, hs⟩ := hx
+  ext z
+  simp only [mem_standardLine]
+  constructor
+  · rintro ⟨t, rfl⟩; exact ⟨t - s, by rw [hs, sub_smul]; abel⟩
+  · rintro ⟨t, rfl⟩; exact ⟨t + s, by rw [hs, add_smul]; abel⟩
+
+/-- Scaling the direction by a nonzero scalar does not change the line. -/
+theorem standardLine_smul {x v w : K × K} {c : K} (hc : c ≠ 0) (hvw : v = c • w) :
+    standardLine x v = standardLine x w := by
+  ext z
+  simp only [mem_standardLine]
+  constructor
+  · rintro ⟨t, rfl⟩; exact ⟨t * c, by rw [hvw, smul_smul]⟩
+  · rintro ⟨t, rfl⟩
+    exact ⟨t * c⁻¹, by rw [hvw, smul_smul, mul_assoc, inv_mul_cancel₀ hc, mul_one]⟩
+
+/-- In a two-dimensional module, two vectors `w ≠ 0` and `u ∉ K • w` span the
+whole module: every element is a `K`-linear combination of `w` and `u`. -/
+theorem exists_pair_smul_eq {M : Type u} [AddCommGroup M] [Module K M]
+    (h2 : Module.finrank K M = 2) {w u : M} (hw : w ≠ 0) (hu : u ∉ (K ∙ w))
+    (z : M) : ∃ a b : K, a • w + b • u = z := by
+  haveI : FiniteDimensional K M := Module.finite_of_finrank_eq_succ h2
+  have hlt : (K ∙ w) < Submodule.span K {w, u} := by
+    refine lt_of_le_of_ne (Submodule.span_mono (by simp)) ?_
+    intro he
+    exact hu (he.symm ▸ Submodule.subset_span (show u ∈ ({w, u} : Set M) by simp))
+  have hge : 2 ≤ Module.finrank K (Submodule.span K {w, u}) := by
+    have h := Submodule.finrank_lt_finrank_of_lt hlt
+    rw [finrank_span_singleton hw] at h; omega
+  have hle : Module.finrank K (Submodule.span K {w, u}) ≤ 2 := by
+    rw [← h2, ← finrank_top (R := K) (M := M)]
+    exact Submodule.finrank_mono le_top
+  have htop : Submodule.span K {w, u} = ⊤ := by
+    apply Submodule.eq_of_le_of_finrank_eq le_top
+    rw [finrank_top, h2]; omega
+  have hz : z ∈ Submodule.span K {w, u} := by rw [htop]; exact Submodule.mem_top
+  exact Submodule.mem_span_pair.1 hz
+
+/-- The plane `K²` is two-dimensional. -/
+theorem finrank_prod_self : Module.finrank K (K × K) = 2 := by
+  rw [Module.finrank_prod, Module.finrank_self]
+
 /-- The lines of the **standard affine incidence plane** over a division ring `K`:
 the subsets of `K × K` of the form `p + K • v` for a nonzero direction `v`. -/
 def standardAffineLines (K : Type u) [DivisionRing K] : Set (Set (K × K)) :=
-  {g | ∃ p v : K × K, v ≠ 0 ∧ g = {x | ∃ t : K, x = p + t • v}}
+  {g | ∃ p v : K × K, v ≠ 0 ∧ g = standardLine p v}
 
 /-- The **standard affine incidence plane** `K²` over a division ring `K`. -/
 noncomputable def standardAffinePlane (K : Type u) [DivisionRing K] :
     AffineIncidencePlane (K × K) where
   lines := standardAffineLines K
-  two_points := by sorry
-  unique_line := by sorry
-  unique_parallel := by sorry
-  exists_triangle := by sorry
+  two_points := by
+    rintro g ⟨p, v, hv, rfl⟩
+    refine ⟨p, p + v, ?_, ⟨0, by simp⟩, ⟨1, by simp⟩⟩
+    intro h
+    apply hv
+    have hpv : p + 0 = p + v := by rw [add_zero]; exact h
+    exact (add_left_cancel hpv).symm
+  unique_line := by
+    intro x y hxy
+    refine ⟨standardLine x (y - x),
+      ⟨⟨x, y - x, sub_ne_zero.2 hxy.symm, rfl⟩, ⟨0, by simp⟩,
+        ⟨1, by rw [one_smul]; abel⟩⟩, ?_⟩
+    rintro g ⟨⟨p, w, hw, rfl⟩, hxg, hyg⟩
+    rw [standardLine_rebase hxg]
+    obtain ⟨s, hs⟩ := hxg
+    obtain ⟨r, hr⟩ := hyg
+    have hrs : r - s ≠ 0 := by
+      rw [sub_ne_zero]; intro h; exact hxy (hs.trans (by rw [hr, h]))
+    have hyx : y - x = (r - s) • w := by rw [hr, hs, sub_smul]; abel
+    exact (standardLine_smul hrs hyx).symm
+  unique_parallel := by
+    rintro g ⟨p, w, hw, rfl⟩ x hx
+    refine ⟨standardLine x w, ⟨⟨x, w, hw, rfl⟩, ⟨0, by simp⟩, ?_⟩, ?_⟩
+    · rw [Set.eq_empty_iff_forall_notMem]
+      rintro z ⟨⟨a, ha⟩, ⟨b, hb⟩⟩
+      apply hx
+      refine ⟨b - a, ?_⟩
+      have hz : x + a • w = p + b • w := ha.symm.trans hb
+      have h2 : x = p + b • w - a • w := by rw [← hz]; abel
+      rw [h2, sub_smul]; abel
+    · rintro h ⟨⟨q, u, hu, rfl⟩, hxh, hdisj⟩
+      rw [standardLine_rebase hxh]
+      have hmem : u ∈ (K ∙ w : Submodule K (K × K)) := by
+        by_contra hnot
+        obtain ⟨a, b, hab⟩ := exists_pair_smul_eq finrank_prod_self hw hnot (p - q)
+        have hP1 : q + b • u ∈ standardLine q u := ⟨b, rfl⟩
+        have hP2 : q + b • u ∈ standardLine p w := by
+          refine ⟨-a, ?_⟩
+          have hbu : b • u = p - q - a • w := by rw [← hab]; abel
+          rw [neg_smul, hbu]; abel
+        exact Set.eq_empty_iff_forall_notMem.1 hdisj (q + b • u) ⟨hP1, hP2⟩
+      obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.1 hmem
+      have hc0 : c ≠ 0 := by rintro rfl; rw [zero_smul] at hc; exact hu hc.symm
+      exact standardLine_smul hc0 hc.symm
+  exists_triangle := by
+    refine ⟨(0, 0), (1, 0), (0, 1), ⟨?_, ?_, ?_, ?_⟩⟩
+    · simp [Prod.ext_iff]
+    · simp [Prod.ext_iff]
+    · simp [Prod.ext_iff]
+    · rintro ⟨g, ⟨p, v, hv, rfl⟩, hsub⟩
+      obtain ⟨t0, ht0⟩ := hsub (show ((0, 0) : K × K) ∈ _ by simp)
+      obtain ⟨t1, ht1⟩ := hsub (show ((1, 0) : K × K) ∈ _ by simp)
+      obtain ⟨t2, ht2⟩ := hsub (show ((0, 1) : K × K) ∈ _ by simp)
+      have hp : p = -(t0 • v) := eq_neg_of_add_eq_zero_left ht0.symm
+      have hα : ((1, 0) : K × K) = (t1 - t0) • v := by rw [ht1, hp, sub_smul]; abel
+      have hβ : ((0, 1) : K × K) = (t2 - t0) • v := by rw [ht2, hp, sub_smul]; abel
+      have e1 : (1 : K) = (t1 - t0) * v.1 := by
+        simpa [Prod.smul_def] using congrArg Prod.fst hα
+      have e2 : (0 : K) = (t1 - t0) * v.2 := by
+        simpa [Prod.smul_def] using congrArg Prod.snd hα
+      have e4 : (1 : K) = (t2 - t0) * v.2 := by
+        simpa [Prod.smul_def] using congrArg Prod.snd hβ
+      have hαne : t1 - t0 ≠ 0 := by
+        rintro h; rw [h, zero_mul] at e1; exact one_ne_zero e1
+      have hv2 : v.2 = 0 := (mul_eq_zero.1 e2.symm).resolve_left hαne
+      rw [hv2, mul_zero] at e4
+      exact one_ne_zero e4
 
 /-- The real plane `ℝ²`, the standard model of elementary plane geometry. -/
 noncomputable def realAffinePlane : AffineIncidencePlane (ℝ × ℝ) :=

ElementarGeometrie/Incidence/Basic.lean

@@ -1,8 +1,10 @@
 /-
 Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
 -/
-import Mathlib.Tactic
+import Mathlib.Logic.Equiv.Set
+import Mathlib.Tactic.Common
 
 /-!
 # Incidence geometries

ElementarGeometrie/Incidence/Betweenness.lean

@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
 -/
 import ElementarGeometrie.Incidence.Basic
 

ElementarGeometrie/Incidence/Congruence.lean

@@ -1,7 +1,11 @@
 /-
 Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
 -/
+import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.GroupTheory.Perm.Basic
+import Mathlib.Data.Set.Card
 import ElementarGeometrie.Incidence.Betweenness
 
 /-!

ElementarGeometrie/Projective/Completion.lean

@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
 -/
 import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import ElementarGeometrie.Projective.Space

ElementarGeometrie/Projective/Duality.lean

@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
 -/
 import Mathlib.LinearAlgebra.Dual.Defs
 import ElementarGeometrie.Projective.Space

ElementarGeometrie/Projective/Space.lean

@@ -1,7 +1,9 @@
 /-
 Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
 -/
+import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
 import Mathlib.LinearAlgebra.Projectivization.Subspace
 import ElementarGeometrie.Incidence.Basic
 
@@ -15,8 +17,7 @@ the sets of one-dimensional subspaces contained in a fixed two-dimensional
 subspace.
 
 We reuse Mathlib's `Projectivization K V` (notation `ℙ K V`) and equip it with an
-`IncidenceGeometry` structure. The two incidence axioms are recorded as proof
-obligations and currently left as `sorry`.
+`IncidenceGeometry` structure, proving the two incidence axioms.
 
 ## Main definitions
 
@@ -39,11 +40,84 @@ def projectiveLines : Set (Set (ℙ K V)) :=
   {g | ∃ W : Submodule K V, Module.finrank K W = 2 ∧
         g = {p : ℙ K V | p.submodule ≤ W}}
 
+variable {K V}
+
+/-- Distinct projective points have distinct underlying one-dimensional
+subspaces. -/
+theorem submodule_ne_of_ne {x y : ℙ K V} (h : x ≠ y) :
+    x.submodule ≠ y.submodule :=
+  fun he => h (Projectivization.submodule_injective he)
+
+/-- The subspace spanned by two distinct projective points is two-dimensional. -/
+theorem finrank_sup_submodule {x y : ℙ K V} (h : x ≠ y) :
+    Module.finrank K (x.submodule ⊔ y.submodule : Submodule K V) = 2 := by
+  haveI : FiniteDimensional K x.submodule :=
+    Module.finite_of_finrank_eq_succ x.finrank_submodule
+  haveI : FiniteDimensional K y.submodule :=
+    Module.finite_of_finrank_eq_succ y.finrank_submodule
+  have hinf : Module.finrank K (x.submodule ⊓ y.submodule : Submodule K V) = 0 := by
+    by_contra hne
+    have hle : Module.finrank K (x.submodule ⊓ y.submodule : Submodule K V) ≤ 1 := by
+      have := Submodule.finrank_mono (inf_le_left : x.submodule ⊓ y.submodule ≤ x.submodule)
+      rwa [x.finrank_submodule] at this
+    have h1 : Module.finrank K (x.submodule ⊓ y.submodule : Submodule K V) = 1 :=
+      le_antisymm hle (Nat.one_le_iff_ne_zero.2 hne)
+    have hx : x.submodule ⊓ y.submodule = x.submodule :=
+      Submodule.eq_of_le_of_finrank_eq inf_le_left (by rw [h1, x.finrank_submodule])
+    have hy : x.submodule ⊓ y.submodule = y.submodule :=
+      Submodule.eq_of_le_of_finrank_eq inf_le_right (by rw [h1, y.finrank_submodule])
+    exact submodule_ne_of_ne h (hx.symm.trans hy)
+  have hsum := Submodule.finrank_sup_add_finrank_inf_eq x.submodule y.submodule
+  rw [hinf, x.finrank_submodule, y.finrank_submodule] at hsum
+  omega
+
+variable (K V) in
 /-- The **projectivization** `ℙ K V` as an incidence geometry: points are the
 one-dimensional subspaces of `V` and lines are the projective lines. -/
 noncomputable def projectivization : IncidenceGeometry (ℙ K V) where
   lines := projectiveLines K V
-  two_points := by sorry
-  unique_line := by sorry
+  two_points := by
+    rintro g ⟨W, hW, rfl⟩
+    -- `W` is two-dimensional, hence nonzero: pick a nonzero `v ∈ W`.
+    have hWne : W ≠ ⊥ := by
+      rintro rfl; rw [finrank_bot] at hW; exact absurd hW (by norm_num)
+    obtain ⟨v, hvW, hv⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hWne
+    -- The line `K ∙ v` is properly contained in `W`, so we find `w ∈ W \ K ∙ v`.
+    have hsub : (K ∙ v) ≤ W := (Submodule.span_singleton_le_iff_mem _ _).2 hvW
+    have hne : (K ∙ v) ≠ W := by
+      intro he
+      have hfr : Module.finrank K (K ∙ v) = 1 := finrank_span_singleton (K := K) hv
+      rw [he, hW] at hfr; exact absurd hfr (by norm_num)
+    obtain ⟨w, hwW, hwv⟩ := SetLike.exists_of_lt (lt_of_le_of_ne hsub hne)
+    have hw : w ≠ 0 := fun h => hwv (h ▸ Submodule.zero_mem _)
+    refine ⟨Projectivization.mk K v hv, Projectivization.mk K w hw, ?_, ?_, ?_⟩
+    · -- the two points are distinct, as their subspaces `K ∙ v ≠ K ∙ w` differ
+      intro he
+      apply hwv
+      have : (Projectivization.mk K w hw).submodule = (Projectivization.mk K v hv).submodule :=
+        congrArg Projectivization.submodule he.symm
+      rw [Projectivization.submodule_mk, Projectivization.submodule_mk] at this
+      rw [← this]; exact Submodule.mem_span_singleton_self w
+    · change (Projectivization.mk K v hv).submodule ≤ W
+      rw [Projectivization.submodule_mk]; exact hsub
+    · change (Projectivization.mk K w hw).submodule ≤ W
+      rw [Projectivization.submodule_mk]
+      exact (Submodule.span_singleton_le_iff_mem _ _).2 hwW
+  unique_line := by
+    intro x y hxy
+    -- The unique line is the one given by `W = x.submodule ⊔ y.submodule`.
+    refine ⟨{p : ℙ K V | p.submodule ≤ x.submodule ⊔ y.submodule},
+      ⟨⟨_, finrank_sup_submodule hxy, rfl⟩, ?_, ?_⟩, ?_⟩
+    · change x.submodule ≤ x.submodule ⊔ y.submodule
+      exact le_sup_left
+    · change y.submodule ≤ x.submodule ⊔ y.submodule
+      exact le_sup_right
+    rintro g ⟨⟨W', hW', rfl⟩, hxg, hyg⟩
+    -- Any line through `x` and `y` has direction containing `W`, hence equal to it.
+    have hle : x.submodule ⊔ y.submodule ≤ W' := sup_le hxg hyg
+    haveI : FiniteDimensional K W' := Module.finite_of_finrank_eq_succ (n := 1) hW'
+    have : x.submodule ⊔ y.submodule = W' :=
+      Submodule.eq_of_le_of_finrank_eq hle (by rw [finrank_sup_submodule hxy, hW'])
+    rw [this]
 
 end IncidenceGeometry