190 lines
8.2 KiB
Lean4
190 lines
8.2 KiB
Lean4
/-
|
||
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
|
||
|
||
/-!
|
||
# Standard models
|
||
|
||
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 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 `ℝ²`.
|
||
-/
|
||
|
||
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 = 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
|
||
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 (ℝ × ℝ) :=
|
||
standardAffinePlane ℝ
|
||
|
||
namespace AffineIncidencePlane
|
||
|
||
variable {X : Type u}
|
||
|
||
open IncidenceGeometry
|
||
|
||
/-- **Coordinatization theorem.** An affine incidence plane has the Desargues
|
||
property if and only if it is isomorphic to the standard affine plane `K²` over
|
||
some division ring `K`. -/
|
||
theorem desarguesProperty_iff_isomorphic_standard (P : AffineIncidencePlane X) :
|
||
P.DesarguesProperty ↔
|
||
∃ (K : Type u) (_ : DivisionRing K),
|
||
Isomorphic P.toIncidenceGeometry (standardAffinePlane K).toIncidenceGeometry := by
|
||
sorry
|
||
|
||
/-- The real plane `ℝ²` is a Pappus plane. -/
|
||
theorem realAffinePlane_isPappusPlane : realAffinePlane.IsPappusPlane := by
|
||
sorry
|
||
|
||
end AffineIncidencePlane
|