122 lines
4.9 KiB
Lean4
122 lines
4.9 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.Logic.Equiv.Set
|
||
import Mathlib.Tactic.Common
|
||
|
||
/-!
|
||
# Incidence geometries
|
||
|
||
This file introduces the most basic structure of elementary geometry, the
|
||
*incidence geometry*, following the lecture notes of Wolfgang Soergel.
|
||
|
||
An **incidence geometry** is a pair `(X, G)` consisting of a set `X` together
|
||
with a system of subsets `G ⊆ 𝒫(X)`, the *lines*, such that every line contains
|
||
at least two points and such that through any two distinct points there is
|
||
exactly one line.
|
||
|
||
We model the carrier as a type `X` and the system of lines as a set of subsets,
|
||
`lines : Set (Set X)`. This stays close to the source text, where a line *is* a
|
||
subset of `X` and "lies on" is literal set membership.
|
||
|
||
## Main definitions
|
||
|
||
* `IncidenceGeometry X` : the structure of an incidence geometry on `X`.
|
||
* `IncidenceGeometry.line` : the unique line through two distinct points.
|
||
* `IncidenceGeometry.Collinear` : a set of points lying on a common line.
|
||
* `IncidenceGeometry.Concurrent` : a set of lines sharing a common point.
|
||
* `IncidenceGeometry.Triangle` : three non-collinear points.
|
||
-/
|
||
|
||
universe u v
|
||
|
||
variable {X : Type u} {Y : Type v}
|
||
|
||
/-- An **incidence geometry** on a type `X` is a system of *lines*
|
||
`lines : Set (Set X)` such that every line contains at least two points and
|
||
such that through any two distinct points there passes exactly one line. -/
|
||
structure IncidenceGeometry (X : Type u) where
|
||
/-- The system of lines, each a subset of the point set `X`. -/
|
||
lines : Set (Set X)
|
||
/-- Every line contains at least two distinct points. -/
|
||
two_points : ∀ g ∈ lines, ∃ a b, a ≠ b ∧ a ∈ g ∧ b ∈ g
|
||
/-- Through any two distinct points there passes exactly one line. -/
|
||
unique_line : ∀ x y : X, x ≠ y → ∃! g, g ∈ lines ∧ x ∈ g ∧ y ∈ g
|
||
|
||
namespace IncidenceGeometry
|
||
|
||
/-- The unique line through two distinct points `x ≠ y`, written `x̄y` in the
|
||
source. For `x = y` we return `{x, y}` as a junk value; all lemmas about `line`
|
||
assume `x ≠ y`. -/
|
||
noncomputable def line (G : IncidenceGeometry X) (x y : X) : Set X :=
|
||
haveI := Classical.propDecidable (x ≠ y)
|
||
if h : x ≠ y then (G.unique_line x y h).choose else {x, y}
|
||
|
||
variable {G : IncidenceGeometry X}
|
||
|
||
/-- For distinct points, `G.line x y` is a line of `G`. -/
|
||
theorem line_mem_lines {x y : X} (h : x ≠ y) : G.line x y ∈ G.lines := by
|
||
simp only [line, dif_pos h]
|
||
exact (G.unique_line x y h).choose_spec.1.1
|
||
|
||
/-- For distinct points, `x` lies on `G.line x y`. -/
|
||
theorem left_mem_line {x y : X} (h : x ≠ y) : x ∈ G.line x y := by
|
||
simp only [line, dif_pos h]
|
||
exact (G.unique_line x y h).choose_spec.1.2.1
|
||
|
||
/-- For distinct points, `y` lies on `G.line x y`. -/
|
||
theorem right_mem_line {x y : X} (h : x ≠ y) : y ∈ G.line x y := by
|
||
simp only [line, dif_pos h]
|
||
exact (G.unique_line x y h).choose_spec.1.2.2
|
||
|
||
/-- The defining uniqueness property of `line`: any line through two distinct
|
||
points `x, y` equals `G.line x y`. -/
|
||
theorem eq_line {x y : X} (hxy : x ≠ y) {g : Set X}
|
||
(hg : g ∈ G.lines) (hx : x ∈ g) (hy : y ∈ g) : g = G.line x y :=
|
||
(G.unique_line x y hxy).unique ⟨hg, hx, hy⟩
|
||
⟨line_mem_lines hxy, left_mem_line hxy, right_mem_line hxy⟩
|
||
|
||
/-- `line` is symmetric in its two arguments. -/
|
||
theorem line_comm {x y : X} (h : x ≠ y) : G.line x y = G.line y x :=
|
||
eq_line h.symm (line_mem_lines h) (right_mem_line h) (left_mem_line h)
|
||
|
||
variable (G) in
|
||
/-- A set of points is **collinear** if all of its points lie on a common line. -/
|
||
def Collinear (S : Set X) : Prop := ∃ g ∈ G.lines, S ⊆ g
|
||
|
||
variable (G) in
|
||
/-- A set of lines is **concurrent** if all of its lines pass through a common
|
||
point. -/
|
||
def Concurrent (S : Set (Set X)) : Prop := ∃ p : X, ∀ g ∈ S, p ∈ g
|
||
|
||
variable (G) in
|
||
/-- Three points form a **triangle** if they are pairwise distinct and not
|
||
collinear. -/
|
||
structure Triangle (a b c : X) : Prop where
|
||
ne_ab : a ≠ b
|
||
ne_bc : b ≠ c
|
||
ne_ca : c ≠ a
|
||
not_collinear : ¬ G.Collinear {a, b, c}
|
||
|
||
/-- A bijection `φ : X ≃ Y` of point sets is a **collineation**, or an
|
||
*isomorphism of incidence geometries*, from `G` to `G'` if it induces a bijection
|
||
between the systems of lines: a subset is a line of `G` if and only if its image
|
||
is a line of `G'`. -/
|
||
def IsCollineation (G : IncidenceGeometry X) (G' : IncidenceGeometry Y)
|
||
(φ : X ≃ Y) : Prop :=
|
||
∀ g : Set X, g ∈ G.lines ↔ ⇑φ '' g ∈ G'.lines
|
||
|
||
/-- Two incidence geometries are **isomorphic** if there is a collineation
|
||
between them. -/
|
||
def Isomorphic (G : IncidenceGeometry X) (G' : IncidenceGeometry Y) : Prop :=
|
||
∃ φ : X ≃ Y, IsCollineation G G' φ
|
||
|
||
/-- An **automorphism** of an incidence geometry is a collineation of `G` with
|
||
itself. -/
|
||
def IsAutomorphism (G : IncidenceGeometry X) (φ : X ≃ X) : Prop :=
|
||
IsCollineation G G φ
|
||
|
||
end IncidenceGeometry
|