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.

Equations

• Configuration.Dual P = P

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

Equations

• Configuration.instInhabitedDual P = h

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

Equations

• ⋯ = inst

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

Equations

• Configuration.instFintypeDual P = h

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

Equations

• Configuration.instMembershipDual P L = { mem := Function.swap Membership.mem }

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
• mkPoint_ax : ∀ {l₁ l₂ : L} (h : l₁ ≠ l₂), Configuration.HasPoints.mkPoint h ∈ l₁ ∧ Configuration.HasPoints.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
• mkLine_ax : ∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ Configuration.HasLines.mkLine h ∧ p₂ ∈ Configuration.HasLines.mkLine h

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

Equations

• ⋯ = ⋯

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

Equations

• Configuration.Dual.hasLines P L = Configuration.HasLines.mk (@Configuration.HasPoints.mkPoint P L inst✝ inst) ⋯

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

Equations

• Configuration.Dual.hasPoints P L = Configuration.HasPoints.mk (@Configuration.HasLines.mkLine P L inst✝ inst) ⋯

theorem Configuration.HasPoints.existsUnique_point (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.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] [Configuration.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] [Configuration.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.

Equations

• Configuration.lineCount L p = Nat.card { l : L // p ∈ l }

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

Number of lines through a given point.

Equations

• Configuration.pointCount P l = Nat.card { p : P // p ∈ l }

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

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

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

theorem Configuration.HasLines.card_le (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.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] [Configuration.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] [Configuration.HasLines P L] [Fintype P] [Fintype L] (h : Fintype.card P = Fintype.card L) : ∃ (f : L → P), Function.Bijective f ∧ ∀ (l : L), Configuration.pointCount P l = Configuration.lineCount L (f l)

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

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

noncomputable def Configuration.HasLines.hasPoints {P : Type u_1} {L : Type u_2} [Membership P L] [Configuration.HasLines P L] [Fintype P] [Fintype L] (h : Fintype.card P = Fintype.card L) : Configuration.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.

Equations

• Configuration.HasLines.hasPoints h = Configuration.HasPoints.mk (fun {l₁ l₂ : L} (hl : l₁ ≠ l₂) => Classical.choose ⋯) ⋯

noncomputable def Configuration.HasPoints.hasLines {P : Type u_1} {L : Type u_2} [Membership P L] [Configuration.HasPoints P L] [Fintype P] [Fintype L] (h : Fintype.card P = Fintype.card L) : Configuration.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.

Equations

• Configuration.HasPoints.hasLines h = Configuration.HasLines.mk (fun (x x_1 : P) => Configuration.HasPoints.mkPoint) ⋯

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₂), Configuration.HasPoints.mkPoint h ∈ l₁ ∧ Configuration.HasPoints.mkPoint h ∈ l₂
• mkLine : {p₁ p₂ : P} → p₁ ≠ p₂ → L
• mkLine_ax : ∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ Configuration.ProjectivePlane.mkLine h ∧ p₂ ∈ Configuration.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] [Configuration.ProjectivePlane P L] : Configuration.ProjectivePlane (Configuration.Dual L) (Configuration.Dual P)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Configuration.ProjectivePlane.order (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.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.

Equations

• Configuration.ProjectivePlane.order P L = Configuration.lineCount L (Classical.choose ⋯) - 1

theorem Configuration.ProjectivePlane.card_points_eq_card_lines (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.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] [Configuration.ProjectivePlane P L] [Finite P] [Finite L] (p q : P) : Configuration.lineCount L p = Configuration.lineCount L q

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

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

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

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

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

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

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

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

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

theorem Configuration.ProjectivePlane.card_lines (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.ProjectivePlane P L] [Finite P] [Fintype L] : Fintype.card L = Configuration.ProjectivePlane.order P L ^ 2 + Configuration.ProjectivePlane.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))

Equations

• Configuration.ofField.instMembershipProjectivizationForallFinOfNatNat = { mem := Function.swap Projectivization.orthogonal }

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 : Matrix.dotProduct a c = 0) (hbc : Matrix.dotProduct b c = 0) (had : Matrix.dotProduct a d = 0) (hbd : Matrix.dotProduct 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] : Configuration.Nondegenerate (Projectivization K (Fin 3 → K)) (Projectivization K (Fin 3 → K))

Equations

• ⋯ = ⋯

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

Equations

• Configuration.ofField.instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq = Configuration.ProjectivePlane.mk (fun {v w : Projectivization K (Fin 3 → K)} (a : v ≠ w) => v.cross w) ⋯ ⋯