Configurations of Points and lines

This file introduces abstract configurations of points and lines, and proves some basic properties.

Main definitions

• Configuration.Nondegenerate: Excludes certain degenerate configurations, and imposes uniqueness of intersection points.
• Configuration.HasPoints: A nondegenerate configuration in which every pair of lines has an intersection point.
• Configuration.HasLines: A nondegenerate configuration in which every pair of points has a line through them.
• Configuration.lineCount: The number of lines through a given point.
• Configuration.pointCount: The number of lines through a given line.

Main statements

• Configuration.HasLines.card_le: HasLines implies |P| ≤ |L|.
• Configuration.HasPoints.card_le: HasPoints implies |L| ≤ |P|.
• Configuration.HasLines.hasPoints: HasLines and |P| = |L| implies HasPoints.
• Configuration.HasPoints.hasLines: HasPoints and |P| = |L| implies HasLines. Together, these four statements say that any two of the following properties imply the third: (a) HasLines, (b) HasPoints, (c) |P| = |L|.

def Configuration.Dual (P : Type u_1) : Type u_1

A type synonym.

instance Configuration.instInhabitedDual (P : Type u_1) [h : Inhabited P] : Inhabited (Dual P)

instance Configuration.instFiniteDual (P : Type u_1) [Finite P] : Finite (Dual P)

instance Configuration.instFintypeDual (P : Type u_1) [h : Fintype P] : Fintype (Dual P)

instance Configuration.instMembershipDual (P : Type u_1) (L : Type u_2) [Membership P L] : Membership (Dual L) (Dual P)

class Configuration.Nondegenerate (P : Type u_1) (L : Type u_2) [Membership P L] : Prop

A configuration is nondegenerate if:

1. there does not exist a line that passes through all of the points,
2. there does not exist a point that is on all of the lines,
3. there is at most one line through any two points,
4. any two lines have at most one intersection point. Conditions 3 and 4 are equivalent.

• exists_point (l : L) : ∃ (p : P), p ∉ l
• exists_line (p : P) : ∃ (l : L), p ∉ l
• eq_or_eq {p₁ p₂ : P} {l₁ l₂ : L} : p₁ ∈ l₁ → p₂ ∈ l₁ → p₁ ∈ l₂ → p₂ ∈ l₂ → p₁ = p₂ ∨ l₁ = l₂

class Configuration.HasPoints (P : Type u_1) (L : Type u_2) [Membership P L] extends Configuration.Nondegenerate P L : Type (max u_1 u_2)

A nondegenerate configuration in which every pair of lines has an intersection point.

• exists_point (l : L) : ∃ (p : P), p ∉ l
• exists_line (p : P) : ∃ (l : L), p ∉ l
• eq_or_eq {p₁ p₂ : P} {l₁ l₂ : L} : p₁ ∈ l₁ → p₂ ∈ l₁ → p₁ ∈ l₂ → p₂ ∈ l₂ → p₁ = p₂ ∨ l₁ = l₂
• mkPoint {l₁ l₂ : L} : l₁ ≠ l₂ → P

  Intersection of two lines

• mkPoint_ax {l₁ l₂ : L} (h : l₁ ≠ l₂) : mkPoint h ∈ l₁ ∧ mkPoint h ∈ l₂

class Configuration.HasLines (P : Type u_1) (L : Type u_2) [Membership P L] extends Configuration.Nondegenerate P L : Type (max u_1 u_2)

A nondegenerate configuration in which every pair of points has a line through them.

• exists_point (l : L) : ∃ (p : P), p ∉ l
• exists_line (p : P) : ∃ (l : L), p ∉ l
• eq_or_eq {p₁ p₂ : P} {l₁ l₂ : L} : p₁ ∈ l₁ → p₂ ∈ l₁ → p₁ ∈ l₂ → p₂ ∈ l₂ → p₁ = p₂ ∨ l₁ = l₂
• mkLine {p₁ p₂ : P} : p₁ ≠ p₂ → L

  Line through two points

• mkLine_ax {p₁ p₂ : P} (h : p₁ ≠ p₂) : p₁ ∈ mkLine h ∧ p₂ ∈ mkLine h

instance Configuration.Dual.Nondegenerate (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.Nondegenerate P L] : Configuration.Nondegenerate (Dual L) (Dual P)

instance Configuration.Dual.hasLines (P : Type u_1) (L : Type u_2) [Membership P L] [HasPoints P L] : HasLines (Dual L) (Dual P)

instance Configuration.Dual.hasPoints (P : Type u_1) (L : Type u_2) [Membership P L] [HasLines P L] : HasPoints (Dual L) (Dual P)

theorem Configuration.HasPoints.existsUnique_point (P : Type u_1) (L : Type u_2) [Membership P L] [HasPoints P L] (l₁ l₂ : L) (hl : l₁ ≠ l₂) : ∃! p : P, p ∈ l₁ ∧ p ∈ l₂

theorem Configuration.HasLines.existsUnique_line (P : Type u_1) (L : Type u_2) [Membership P L] [HasLines P L] (p₁ p₂ : P) (hp : p₁ ≠ p₂) : ∃! l : L, p₁ ∈ l ∧ p₂ ∈ l

theorem Configuration.Nondegenerate.exists_injective_of_card_le {P : Type u_1} {L : Type u_2} [Membership P L] [Nondegenerate P L] [Fintype P] [Fintype L] (h : Fintype.card L ≤ Fintype.card P) : ∃ (f : L → P), Function.Injective f ∧ ∀ (l : L), f l ∉ l

If a nondegenerate configuration has at least as many points as lines, then there exists an injective function f from lines to points, such that f l does not lie on l.

noncomputable def Configuration.lineCount {P : Type u_1} (L : Type u_2) [Membership P L] (p : P) : ℕ

Number of points on a given line.

noncomputable def Configuration.pointCount (P : Type u_1) {L : Type u_2} [Membership P L] (l : L) : ℕ

Number of lines through a given point.

theorem Configuration.sum_lineCount_eq_sum_pointCount (P : Type u_1) (L : Type u_2) [Membership P L] [Fintype P] [Fintype L] : ∑ p : P, lineCount L p = ∑ l : L, pointCount P l

theorem Configuration.HasLines.pointCount_le_lineCount {P : Type u_1} {L : Type u_2} [Membership P L] [HasLines P L] {p : P} {l : L} (h : p ∉ l) [Finite { l : L // p ∈ l }] : pointCount P l ≤ lineCount L p

theorem Configuration.HasPoints.lineCount_le_pointCount {P : Type u_1} {L : Type u_2} [Membership P L] [HasPoints P L] {p : P} {l : L} (h : p ∉ l) [hf : Finite { p : P // p ∈ l }] : lineCount L p ≤ pointCount P l

theorem Configuration.HasLines.card_le (P : Type u_1) (L : Type u_2) [Membership P L] [HasLines P L] [Fintype P] [Fintype L] : Fintype.card P ≤ Fintype.card L

If a nondegenerate configuration has a unique line through any two points, then |P| ≤ |L|.

theorem Configuration.HasPoints.card_le (P : Type u_1) (L : Type u_2) [Membership P L] [HasPoints P L] [Fintype P] [Fintype L] : Fintype.card L ≤ Fintype.card P

If a nondegenerate configuration has a unique point on any two lines, then |L| ≤ |P|.

theorem Configuration.HasLines.exists_bijective_of_card_eq {P : Type u_1} {L : Type u_2} [Membership P L] [HasLines P L] [Fintype P] [Fintype L] (h : Fintype.card P = Fintype.card L) : ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

theorem Configuration.HasLines.lineCount_eq_pointCount {P : Type u_1} {L : Type u_2} [Membership P L] [HasLines P L] [Fintype P] [Fintype L] (hPL : Fintype.card P = Fintype.card L) {p : P} {l : L} (hpl : p ∉ l) : lineCount L p = pointCount P l

theorem Configuration.HasPoints.lineCount_eq_pointCount {P : Type u_1} {L : Type u_2} [Membership P L] [HasPoints P L] [Fintype P] [Fintype L] (hPL : Fintype.card P = Fintype.card L) {p : P} {l : L} (hpl : p ∉ l) : lineCount L p = pointCount P l

noncomputable def Configuration.HasLines.hasPoints {P : Type u_1} {L : Type u_2} [Membership P L] [HasLines P L] [Fintype P] [Fintype L] (h : Fintype.card P = Fintype.card L) : HasPoints P L

If a nondegenerate configuration has a unique line through any two points, and if |P| = |L|, then there is a unique point on any two lines.

noncomputable def Configuration.HasPoints.hasLines {P : Type u_1} {L : Type u_2} [Membership P L] [HasPoints P L] [Fintype P] [Fintype L] (h : Fintype.card P = Fintype.card L) : HasLines P L

If a nondegenerate configuration has a unique point on any two lines, and if |P| = |L|, then there is a unique line through any two points.

class Configuration.ProjectivePlane (P : Type u_1) (L : Type u_2) [Membership P L] extends Configuration.HasPoints P L, Configuration.HasLines P L : Type (max u_1 u_2)

A projective plane is a nondegenerate configuration in which every pair of lines has an intersection point, every pair of points has a line through them, and which has three points in general position.

• exists_point (l : L) : ∃ (p : P), p ∉ l
• exists_line (p : P) : ∃ (l : L), p ∉ l
• eq_or_eq {p₁ p₂ : P} {l₁ l₂ : L} : p₁ ∈ l₁ → p₂ ∈ l₁ → p₁ ∈ l₂ → p₂ ∈ l₂ → p₁ = p₂ ∨ l₁ = l₂
• mkPoint {l₁ l₂ : L} : l₁ ≠ l₂ → P
• mkPoint_ax {l₁ l₂ : L} (h : l₁ ≠ l₂) : mkPoint h ∈ l₁ ∧ mkPoint h ∈ l₂
• mkLine {p₁ p₂ : P} : p₁ ≠ p₂ → L
• mkLine_ax {p₁ p₂ : P} (h : p₁ ≠ p₂) : p₁ ∈ ProjectivePlane.mkLine h ∧ p₂ ∈ ProjectivePlane.mkLine h
• exists_config : ∃ (p₁ : P) (p₂ : P) (p₃ : P) (l₁ : L) (l₂ : L) (l₃ : L), p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃

instance Configuration.ProjectivePlane.instDual (P : Type u_1) (L : Type u_2) [Membership P L] [ProjectivePlane P L] : ProjectivePlane (Dual L) (Dual P)

noncomputable def Configuration.ProjectivePlane.order (P : Type u_1) (L : Type u_2) [Membership P L] [ProjectivePlane P L] : ℕ

The order of a projective plane is one less than the number of lines through an arbitrary point. Equivalently, it is one less than the number of points on an arbitrary line.

theorem Configuration.ProjectivePlane.card_points_eq_card_lines (P : Type u_1) (L : Type u_2) [Membership P L] [ProjectivePlane P L] [Fintype P] [Fintype L] : Fintype.card P = Fintype.card L

theorem Configuration.ProjectivePlane.lineCount_eq_lineCount {P : Type u_1} (L : Type u_2) [Membership P L] [ProjectivePlane P L] [Finite P] [Finite L] (p q : P) : lineCount L p = lineCount L q

theorem Configuration.ProjectivePlane.pointCount_eq_pointCount (P : Type u_1) {L : Type u_2} [Membership P L] [ProjectivePlane P L] [Finite P] [Finite L] (l m : L) : pointCount P l = pointCount P m

theorem Configuration.ProjectivePlane.lineCount_eq_pointCount {P : Type u_1} {L : Type u_2} [Membership P L] [ProjectivePlane P L] [Finite P] [Finite L] (p : P) (l : L) : lineCount L p = pointCount P l

theorem Configuration.ProjectivePlane.Dual.order (P : Type u_1) (L : Type u_2) [Membership P L] [ProjectivePlane P L] [Finite P] [Finite L] : ProjectivePlane.order (Dual L) (Dual P) = ProjectivePlane.order P L

theorem Configuration.ProjectivePlane.lineCount_eq {P : Type u_1} (L : Type u_2) [Membership P L] [ProjectivePlane P L] [Finite P] [Finite L] (p : P) : lineCount L p = order P L + 1

theorem Configuration.ProjectivePlane.pointCount_eq (P : Type u_1) {L : Type u_2} [Membership P L] [ProjectivePlane P L] [Finite P] [Finite L] (l : L) : pointCount P l = order P L + 1

theorem Configuration.ProjectivePlane.one_lt_order (P : Type u_1) (L : Type u_2) [Membership P L] [ProjectivePlane P L] [Finite P] [Finite L] : 1 < order P L

theorem Configuration.ProjectivePlane.two_lt_lineCount {P : Type u_1} (L : Type u_2) [Membership P L] [ProjectivePlane P L] [Finite P] [Finite L] (p : P) : 2 < lineCount L p

theorem Configuration.ProjectivePlane.two_lt_pointCount (P : Type u_1) {L : Type u_2} [Membership P L] [ProjectivePlane P L] [Finite P] [Finite L] (l : L) : 2 < pointCount P l

theorem Configuration.ProjectivePlane.card_points (P : Type u_1) (L : Type u_2) [Membership P L] [ProjectivePlane P L] [Fintype P] [Finite L] : Fintype.card P = order P L ^ 2 + order P L + 1

theorem Configuration.ProjectivePlane.card_lines (P : Type u_1) (L : Type u_2) [Membership P L] [ProjectivePlane P L] [Finite P] [Fintype L] : Fintype.card L = order P L ^ 2 + order P L + 1

instance Configuration.ofField.instMembershipProjectivizationForallFinOfNatNat {K : Type u_3} [Field K] : Membership (Projectivization K (Fin 3 → K)) (Projectivization K (Fin 3 → K))

theorem Configuration.ofField.mem_iff {K : Type u_3} [Field K] (v w : Projectivization K (Fin 3 → K)) : v ∈ w ↔ v.orthogonal w

theorem Configuration.ofField.crossProduct_eq_zero_of_dotProduct_eq_zero {K : Type u_3} [Field K] {a b c d : Fin 3 → K} (hac : a ⬝ᵥ c = 0) (hbc : b ⬝ᵥ c = 0) (had : a ⬝ᵥ d = 0) (hbd : b ⬝ᵥ d = 0) : (crossProduct a) b = 0 ∨ (crossProduct c) d = 0

theorem Configuration.ofField.eq_or_eq_of_orthogonal {K : Type u_3} [Field K] {a b c d : Projectivization K (Fin 3 → K)} (hac : a.orthogonal c) (hbc : b.orthogonal c) (had : a.orthogonal d) (hbd : b.orthogonal d) : a = b ∨ c = d

instance Configuration.ofField.instNondegenerateProjectivizationForallFinOfNatNat {K : Type u_3} [Field K] : Nondegenerate (Projectivization K (Fin 3 → K)) (Projectivization K (Fin 3 → K))

noncomputable instance Configuration.ofField.instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq {K : Type u_3} [Field K] [DecidableEq K] : ProjectivePlane (Projectivization K (Fin 3 → K)) (Projectivization K (Fin 3 → K))