Theory Higher_Projective_Space_Rank_Axioms

theory Higher_Projective_Space_Rank_Axioms
  imports Main
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ Following \<^cite>‹Magaud_2012› we introduce a set of axioms for projective space geometry based on
the notions of matroid and rank.
›

section ‹A Based-rank Set of Axioms for Projective Space Geometry›

(* We have a type of points *)
locale higher_projective_space_rank =

(* We have a rank function "rk" on the sets of points *)
fixes rk :: "'point set ⇒ nat"


(* The function rk satisfies the following axioms *)
assumes
matroid_ax_1a: "rk X ≥ 0" (* Useless if rk is defined with values in ℕ, not ℤ *) and
matroid_ax_1b: "rk X ≤ card X" and
matroid_ax_2: "X ⊆ Y ⟶ rk X ≤ rk Y" and
matroid_ax_3: "rk (X ∪ Y) + rk (X ∩ Y) ≤ rk X + rk Y"

(* To capture higher projective geometry, we need to introduce the following additional axioms *)
assumes
rk_ax_singleton: "rk {P} ≥ 1" and
rk_ax_couple: "P ≠ Q ⟶ rk {P,Q} ≥ 2" and
rk_ax_pasch: "rk {A,B,C,D} ≤ 3 ⟶ (∃J. rk {A,B,J} = 2 ∧ rk {C,D,J} = 2)" and
rk_ax_3_pts: "∃C. rk {A,B,C} = 2 ∧ rk {B,C} = 2 ∧ rk {A,C} = 2" and
rk_ax_dim: "∃A B C D. rk {A,B,C,D} ≥ 4"

(* Note that the rank-based axioms system above deals only with points. 
Projective geometry developped this way is dimension-independent and it can be scaled to any dimension
without adding any entity to the theory or modifying the language of the theory *)

end