/-
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