# Documentation

Mathlib.Combinatorics.Configuration

# 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.

Instances For
instance Configuration.instInhabitedDual (P : Type u_1) [h : ] :
instance Configuration.instFintypeDual (P : Type u_1) [h : ] :
instance Configuration.instMembershipDualDual (P : Type u_1) (L : Type u_2) [] :
class Configuration.Nondegenerate (P : Type u_1) (L : Type u_2) [] :
• exists_point : ∀ (l : L), p, ¬p l
• exists_line : ∀ (p : P), l, ¬p l
• eq_or_eq : ∀ {p₁ p₂ : P} {l₁ l₂ : L}, p₁ l₁p₂ l₁p₁ l₂p₂ l₂p₁ = p₂ l₁ = l₂

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.
Instances
class Configuration.HasPoints (P : Type u_1) (L : Type u_2) [] extends :
Type (max u_1 u_2)
• exists_point : ∀ (l : L), p, ¬p l
• exists_line : ∀ (p : P), 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₂),

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

Instances
class Configuration.HasLines (P : Type u_1) (L : Type u_2) [] extends :
Type (max u_1 u_2)
• exists_point : ∀ (l : L), p, ¬p l
• exists_line : ∀ (p : P), 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₂),

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

Instances
instance Configuration.Dual.Nondegenerate (P : Type u_1) (L : Type u_2) [] :
instance Configuration.Dual.hasLines (P : Type u_1) (L : Type u_2) [] [] :
instance Configuration.Dual.hasPoints (P : Type u_1) (L : Type u_2) [] [] :
theorem Configuration.HasPoints.existsUnique_point (P : Type u_1) (L : Type u_2) [] [] (l₁ : L) (l₂ : L) (hl : l₁ l₂) :
∃! p, p l₁ p l₂
theorem Configuration.HasLines.existsUnique_line (P : Type u_1) (L : Type u_2) [] [] (p₁ : P) (p₂ : P) (hp : p₁ p₂) :
∃! l, p₁ l p₂ l
theorem Configuration.Nondegenerate.exists_injective_of_card_le {P : Type u_1} {L : Type u_2} [] [] [] (h : ) :
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) [] (p : P) :

Number of points on a given line.

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

Number of lines through a given point.

Instances For
theorem Configuration.sum_lineCount_eq_sum_pointCount (P : Type u_1) (L : Type u_2) [] [] [] :
(Finset.sum Finset.univ fun p => ) = Finset.sum Finset.univ fun l =>
theorem Configuration.HasLines.pointCount_le_lineCount {P : Type u_1} {L : Type u_2} [] [] {p : P} {l : L} (h : ¬p l) [Finite { l // p l }] :
theorem Configuration.HasPoints.lineCount_le_pointCount {P : Type u_1} {L : Type u_2} [] [] {p : P} {l : L} (h : ¬p l) [hf : Finite { p // p l }] :
theorem Configuration.HasLines.card_le (P : Type u_1) (L : Type u_2) [] [] [] [] :

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) [] [] [] [] :

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} [] [] [] [] (h : ) :
f, ∀ (l : L), = Configuration.lineCount L (f l)
theorem Configuration.HasLines.lineCount_eq_pointCount {P : Type u_1} {L : Type u_2} [] [] [] [] (hPL : ) {p : P} {l : L} (hpl : ¬p l) :
theorem Configuration.HasPoints.lineCount_eq_pointCount {P : Type u_1} {L : Type u_2} [] [] [] [] (hPL : ) {p : P} {l : L} (hpl : ¬p l) :
noncomputable def Configuration.HasLines.hasPoints {P : Type u_1} {L : Type u_2} [] [] [] [] (h : ) :

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.

Instances For
noncomputable def Configuration.HasPoints.hasLines {P : Type u_1} {L : Type u_2} [] [] [] [] (h : ) :

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.

Instances For
class Configuration.ProjectivePlane (P : Type u_1) (L : Type u_2) [] extends :
Type (max u_1 u_2)
• exists_point : ∀ (l : L), p, ¬p l
• exists_line : ∀ (p : P), 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₂),
• mkLine : {p₁ p₂ : P} → p₁ p₂L
• mkLine_ax : ∀ {p₁ p₂ : P} (h : p₁ p₂),
• exists_config : p₁ p₂ p₃ l₁ l₂ l₃, ¬p₁ l₂ ¬p₁ l₃ ¬p₂ l₁ p₂ l₂ p₂ l₃ ¬p₃ l₁ p₃ l₂ ¬p₃ l₃

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.

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

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.

Instances For
theorem Configuration.ProjectivePlane.lineCount_eq_lineCount {P : Type u_1} (L : Type u_2) [] [] [] (p : P) (q : P) :
theorem Configuration.ProjectivePlane.pointCount_eq_pointCount (P : Type u_1) {L : Type u_2} [] [] [] (l : L) (m : L) :
theorem Configuration.ProjectivePlane.lineCount_eq_pointCount {P : Type u_1} {L : Type u_2} [] [] [] (p : P) (l : L) :
theorem Configuration.ProjectivePlane.Dual.order (P : Type u_1) (L : Type u_2) [] [] [] :
theorem Configuration.ProjectivePlane.lineCount_eq {P : Type u_1} (L : Type u_2) [] [] [] (p : P) :
theorem Configuration.ProjectivePlane.pointCount_eq (P : Type u_1) {L : Type u_2} [] [] [] (l : L) :
theorem Configuration.ProjectivePlane.one_lt_order (P : Type u_1) (L : Type u_2) [] [] [] :
theorem Configuration.ProjectivePlane.two_lt_lineCount {P : Type u_1} (L : Type u_2) [] [] [] (p : P) :
theorem Configuration.ProjectivePlane.two_lt_pointCount (P : Type u_1) {L : Type u_2} [] [] [] (l : L) :
theorem Configuration.ProjectivePlane.card_points (P : Type u_1) (L : Type u_2) [] [] [] :
theorem Configuration.ProjectivePlane.card_lines (P : Type u_1) (L : Type u_2) [] [] [] :