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₂

theorem Configuration.Nondegenerate.exists_point {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.Nondegenerate P L] (l : L) : ∃ (p : P), p ∉ l

theorem Configuration.Nondegenerate.exists_line {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.Nondegenerate P L] (p : P) : ∃ (l : L), p ∉ l

theorem Configuration.Nondegenerate.eq_or_eq {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.Nondegenerate P L] {p₁ : P} {p₂ : P} {l₁ : 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 : 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₂

theorem Configuration.HasPoints.mkPoint_ax {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.HasPoints P L] {l₁ : 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 : 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

theorem Configuration.HasLines.mkLine_ax {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.HasLines P L] {p₁ : 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 = let __src := ⋯; 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 = let __src := ⋯; 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₂ : 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₂ : 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 = let this := ⋯; let __src := inst✝¹; 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 = let this := Configuration.HasLines.hasPoints ⋯; let __src := inst✝¹; 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 : 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₃

theorem Configuration.ProjectivePlane.exists_config {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.ProjectivePlane P L] : ∃ (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 : 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 : 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