diff --git a/ElementarGeometrie/Affine/Desargues.lean b/ElementarGeometrie/Affine/Desargues.lean index 1b040bb..7961aba 100644 --- a/ElementarGeometrie/Affine/Desargues.lean +++ b/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 diff --git a/ElementarGeometrie/Affine/Pappus.lean b/ElementarGeometrie/Affine/Pappus.lean index 2ea27c1..e150c95 100644 --- a/ElementarGeometrie/Affine/Pappus.lean +++ b/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 diff --git a/ElementarGeometrie/Affine/Plane.lean b/ElementarGeometrie/Affine/Plane.lean index 4d3428b..d202157 100644 --- a/ElementarGeometrie/Affine/Plane.lean +++ b/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 diff --git a/ElementarGeometrie/Examples.lean b/ElementarGeometrie/Examples.lean index 5e98434..97e4372 100644 --- a/ElementarGeometrie/Examples.lean +++ b/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 (ℝ × ℝ) := diff --git a/ElementarGeometrie/Incidence/Basic.lean b/ElementarGeometrie/Incidence/Basic.lean index 33b55d3..2e33317 100644 --- a/ElementarGeometrie/Incidence/Basic.lean +++ b/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 diff --git a/ElementarGeometrie/Incidence/Betweenness.lean b/ElementarGeometrie/Incidence/Betweenness.lean index 04c33e3..a4ddac5 100644 --- a/ElementarGeometrie/Incidence/Betweenness.lean +++ b/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 diff --git a/ElementarGeometrie/Incidence/Congruence.lean b/ElementarGeometrie/Incidence/Congruence.lean index 69a838f..0fda573 100644 --- a/ElementarGeometrie/Incidence/Congruence.lean +++ b/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 /-! diff --git a/ElementarGeometrie/Projective/Completion.lean b/ElementarGeometrie/Projective/Completion.lean index d5add2c..23db4eb 100644 --- a/ElementarGeometrie/Projective/Completion.lean +++ b/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 diff --git a/ElementarGeometrie/Projective/Duality.lean b/ElementarGeometrie/Projective/Duality.lean index d793561..ba857dd 100644 --- a/ElementarGeometrie/Projective/Duality.lean +++ b/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 diff --git a/ElementarGeometrie/Projective/Space.lean b/ElementarGeometrie/Projective/Space.lean index 4480d71..13599db 100644 --- a/ElementarGeometrie/Projective/Space.lean +++ b/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