Basic projective geometry

Defines the projective-geometry axioms, the line operator, and central projection between lines in an axiomatic projective geometry.

theorem Basic.rel_sym_acb {G : Type u_1} {ell : G → G → G → Prop} (a b c : G) (l1 : ∀ (a b : G), ell a b a) (l2 : ∀ (a b p q : G), ell a p q → ell b p q → p ≠ q → ell a b p) (abc_col : ell a b c) : ell a c b

theorem Basic.rel_sym_cab {G : Type u_1} {ell : G → G → G → Prop} (a b c : G) (l1 : ∀ (a b : G), ell a b a) (l2 : ∀ (a b p q : G), ell a p q → ell b p q → p ≠ q → ell a b p) (abc_col : ell a b c) : ell c a b

theorem Basic.rel_sym_bca {G : Type u_1} {ell : G → G → G → Prop} (a b c : G) (l1 : ∀ (a b : G), ell a b a) (l2 : ∀ (a b p q : G), ell a p q → ell b p q → p ≠ q → ell a b p) (abc_col : ell a b c) : ell b c a

theorem Basic.rel_sym_bac {G : Type u_1} {ell : G → G → G → Prop} (a b c : G) (l1 : ∀ (a b : G), ell a b a) (l2 : ∀ (a b p q : G), ell a p q → ell b p q → p ≠ q → ell a b p) (abc_col : ell a b c) : ell b a c

theorem Basic.rel_sym_cba {G : Type u_1} {ell : G → G → G → Prop} (a b c : G) (l1 : ∀ (a b : G), ell a b a) (l2 : ∀ (a b p q : G), ell a p q → ell b p q → p ≠ q → ell a b p) (abc_col : ell a b c) : ell c b a

theorem Basic.l1_l2_eq_imp_l3 {G : Type u_1} {ell : G → G → G → Prop} (a b c d p : G) (l1 : ∀ (a b : G), ell a b a) (l2 : ∀ (a b p q : G), ell a p q → ell b p q → p ≠ q → ell a b p) (abcdp_deq : a = b ∨ a = c ∨ a = d ∨ a = p ∨ b = c ∨ b = d ∨ b = p ∨ c = d ∨ c = p ∨ d = p) (pab_col : ell p a b) (pcd_col : ell p c d) : ∃ (q : G), ell q a c ∧ ell q b d

class Basic.ProjectiveGeometry (G : Type u_2) (ell : G → G → G → Prop) : Prop

A projective geometry is a set G together with a ternary collinearity relation ell ⊆ G × G × G satisfying the axioms L₁, L₂ and L₃. (p. 26)

• l1 (a b : G) : ell a b a
• l2 (a b p q : G) : ell a p q → ell b p q → p ≠ q → ell a b p
• l3 (a b c d p : G) : ell p a b → ell p c d → ∃ (q : G), ell q a c ∧ ell q b d

def Basic.tacticRelSym : Lean.ParserDescr

relSym closes a collinearity goal that follows from a hypothesis by one of the symmetries of the relation ell (any permutation of a collinear triple).

Equations

• Basic.tacticRelSym = Lean.ParserDescr.node `Basic.tacticRelSym 1024 (Lean.ParserDescr.nonReservedSymbol "relSym" false)

theorem Basic.ncol_imp_neq {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] (a b c : G) (abc_ncol : ¬ell a b c) : a ≠ b ∧ a ≠ c ∧ b ≠ c

def Basic.star {G : Type u_1} [DecidableEq G] (ell : G → G → G → Prop) (a b : G) : Set G

The line operator ⋆: star ell a b is the line through a and b, defined as {c | ell a b c} when a ≠ b and as {a} when a = b.

Equations

• Basic.star ell a b = {c : G | if a = b then c = a else ell a b c}

theorem Basic.p_2 {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b : G) : a ∈ star ell b a

theorem Basic.star_imp_ell {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (x y z : G) (x_in_yz : x ∈ star ell y z) : ell x y z

theorem Basic.p_3 {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c d p : G) (a_in_bp : a ∈ star ell b p) (p_in_cd : p ∈ star ell c d) (ac_neq : a ≠ c) : star ell a c ∩ star ell b d ≠ ∅

theorem Basic.p_4 {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (a_in_bc : a ∈ star ell b c) (ab_neq : a ≠ b) : c ∈ star ell a b

theorem Basic.p_5 {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (a_in_bc : a ∈ star ell b c) : star ell a b ⊆ star ell b c

theorem Basic.p_6 {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b : G) : star ell a b = star ell b a

theorem Basic.p_7 {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (a_in_bc : a ∈ star ell b c) (ab_neq : a ≠ b) : star ell a b = star ell b c

theorem Basic.p_8 {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c d : G) (a_in_cd : a ∈ star ell c d) (b_in_cd : b ∈ star ell c d) (ab_neq : a ≠ b) : star ell a b = star ell c d

theorem Basic.p_9 {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c d p : G) (a_in_bp : a ∈ star ell b p) (p_in_cd : p ∈ star ell c d) : ∃ q ∈ star ell b d, a ∈ star ell c q

def Basic.centralProjection {G : Type u_1} {ell : G → G → G → Prop} [DecidableEq G] (a b c z : G) (x : ↑(star ell a c)) : Set ↑(star ell b c)

The central projection with center z of a point x on the line a ⋆ c onto the line b ⋆ c: the intersection of the line x ⋆ z with b ⋆ c.

Equations

• Basic.centralProjection a b c z x = Subtype.val ⁻¹' (Basic.star ell (↑x) z ∩ Basic.star ell b c)

theorem Basic.star_nempty_and_neq_imp_sing {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c d : G) (nempty : star ell a b ∩ star ell c d ≠ ∅) (neq : star ell a b ≠ star ell c d) : ∃ (y : G), star ell a b ∩ star ell c d = {y}

theorem Basic.abc_inter_sing {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (abc_ncol : ¬ell a b c) : star ell a b ∩ star ell a c = {a}

class Basic.CentralProjectionQuadruple {G : Type u_1} {ell : G → G → G → Prop} [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) : Prop

The data of a non-degenerate central projection: two distinct lines through c (given by a, b not collinear with c) and a center z on a ⋆ b distinct from a and b.

• abc_ncol : ¬ell a b c
• az_neq : a ≠ ↑z
• bz_neq : b ≠ ↑z

theorem Basic.zp_sym {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] {a b : G} {z : ↑(star ell a b)} : ↑z ∈ star ell b a

instance Basic.cpq_symmetry {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] : CentralProjectionQuadruple b a c ⟨↑z, ⋯⟩

theorem Basic.nin_arm {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] : ↑z ∉ star ell a c

theorem Basic.nin_wall {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] : ↑z ∉ star ell c b

theorem Basic.elbow_center_neq {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] (x : ↑(star ell a c)) : ↑x ≠ ↑z

theorem Basic.shadow_exists {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] (x : ↑(star ell a c)) : star ell ↑x ↑z ∩ star ell c b ≠ ∅

theorem Basic.cen_proj_sing {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] (x : ↑(star ell a c)) : ∃ (y : ↑(star ell b c)), centralProjection a b c (↑z) x = {y}

noncomputable def Basic.cenProjMap {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] (x : ↑(star ell a c)) : ↑(star ell b c)

The central projection as a function: the unique image point on b ⋆ c of the point x on a ⋆ c under projection from the center z.

Equations

• Basic.cenProjMap a b c z x = ⋯.choose

theorem Basic.cen_proj_map_property {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] (x : ↑(star ell a c)) : cenProjMap a b c z x ∈ Subtype.val ⁻¹' star ell ↑x ↑z

theorem Basic.cen_proj_arg_col {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] (x : ↑(star ell a c)) : ell ↑(cenProjMap a b c z x) ↑x ↑z

theorem Basic.shadow_in_light {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] (x : ↑(star ell a c)) : ↑(cenProjMap a b c z x) ∈ star ell ↑x ↑z

theorem Basic.shadow_center_neq {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] (x : ↑(star ell a c)) : ↑(cenProjMap a b c z x) ≠ ↑z

noncomputable def Basic.φ {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] (x : ↑(star ell a c)) : ↑(star ell b c)

The central projection a ⋆ c → b ⋆ c from the center z.

Equations

• Basic.φ a b c z = Basic.cenProjMap a b c z

noncomputable def Basic.ψ {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] (x : ↑(star ell b c)) : ↑(star ell a c)

The reverse central projection b ⋆ c → a ⋆ c from the center z, inverse to φ.

Equations

• Basic.ψ a b c z = Basic.cenProjMap b a c ⟨↑z, ⋯⟩

theorem Basic.cen_proj_left {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] : Function.LeftInverse (ψ a b c z) (φ a b c z)

theorem Basic.cen_proj_bij {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] : Function.Bijective (φ a b c z)

theorem Basic.a_in_ac {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] {a c : G} : a ∈ star ell a c

theorem Basic.c_in_ac {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] {a c : G} : c ∈ star ell a c

theorem Basic.φa_eq_b {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] : ↑(φ a b c z ⟨a, ⋯⟩) = b

theorem Basic.φc_eq_c {G : Type u_1} {ell : G → G → G → Prop} [PG : ProjectiveGeometry G ell] [DecidableEq G] (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] : ↑(φ a b c z ⟨c, ⋯⟩) = c