# mathlibdocumentation

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.has_points: A nondegenerate configuration in which every pair of lines has an intersection point.
• configuration.has_lines: A nondegenerate configuration in which every pair of points has a line through them.
• configuration.line_count: The number of lines through a given point.
• configuration.point_count: The number of lines through a given line.

## Main statements #

• configuration.has_lines.card_le: has_lines implies |P| ≤ |L|.
• configuration.has_points.card_le: has_points implies |L| ≤ |P|.
• configuration.has_lines.has_points: has_lines and |P| = |L| implies has_points.
• configuration.has_points.has_lines: has_points and |P| = |L| implies has_lines. Together, these four statements say that any two of the following properties imply the third: (a) has_lines, (b) has_points, (c) |P| = |L|.
def configuration.dual (P : Type u) :
Type u

A type synonym.

Equations
Instances for configuration.dual
@[protected, instance]
def configuration.dual.inhabited (P : Type u) [this : inhabited P] :
Equations
@[protected, instance]
def configuration.dual.finite (P : Type u) [finite P] :
@[protected, instance]
def configuration.dual.fintype (P : Type u) [this : fintype P] :
Equations
@[protected, instance]
def configuration.dual.has_mem (P L : Type u) [ L] :
Equations
@[class]
structure configuration.nondegenerate (P L : Type u) [ L] :
Prop
• 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₂

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 of this typeclass
@[class]
structure configuration.has_points (P L : Type u) [ L] :
Type u
• to_nondegenerate :
• mk_point : Π {l₁ l₂ : L}, l₁ l₂ → P
• mk_point_ax : ∀ {l₁ l₂ : L} (h : l₁ l₂),

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

Instances of this typeclass
Instances of other typeclasses for configuration.has_points
• configuration.has_points.has_sizeof_inst
@[class]
structure configuration.has_lines (P L : Type u) [ L] :
Type u
• to_nondegenerate :
• mk_line : Π {p₁ p₂ : P}, p₁ p₂ → L
• mk_line_ax : ∀ {p₁ p₂ : P} (h : p₁ p₂),

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

Instances of this typeclass
Instances of other typeclasses for configuration.has_lines
• configuration.has_lines.has_sizeof_inst
@[protected, instance]
def configuration.dual.nondegenerate (P L : Type u) [ L]  :
@[protected, instance]
def configuration.dual.has_lines (P L : Type u) [ L]  :
Equations
@[protected, instance]
def configuration.dual.has_points (P L : Type u) [ L]  :
Equations
theorem configuration.has_points.exists_unique_point (P L : Type u) [ L] (l₁ l₂ : L) (hl : l₁ l₂) :
∃! (p : P), p l₁ p l₂
theorem configuration.has_lines.exists_unique_line (P L : Type u) [ L] (p₁ p₂ : P) (hp : p₁ p₂) :
∃! (l : L), p₁ l p₂ l
theorem configuration.nondegenerate.exists_injective_of_card_le {P L : Type u} [ L] [fintype P] [fintype L] (h : ) :
∃ (f : L → P), ∀ (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.line_count {P : Type u} (L : Type u) [ L] (p : P) :

Number of points on a given line.

Equations
noncomputable def configuration.point_count (P : Type u) {L : Type u} [ L] (l : L) :

Number of lines through a given point.

Equations
theorem configuration.sum_line_count_eq_sum_point_count (P L : Type u) [ L] [fintype P] [fintype L] :
finset.univ.sum (λ (p : P), = finset.univ.sum (λ (l : L),
theorem configuration.has_lines.point_count_le_line_count {P L : Type u} [ L] {p : P} {l : L} (h : p l) [finite {l // p l}] :
theorem configuration.has_points.line_count_le_point_count {P L : Type u} [ L] {p : P} {l : L} (h : p l) [hf : finite {p // p l}] :
theorem configuration.has_lines.card_le (P L : Type u) [ L] [fintype P] [fintype L] :

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

theorem configuration.has_points.card_le (P L : Type u) [ L] [fintype P] [fintype L] :

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

theorem configuration.has_lines.exists_bijective_of_card_eq {P L : Type u} [ L] [fintype P] [fintype L] (h : = ) :
∃ (f : L → P), ∀ (l : L),
theorem configuration.has_lines.line_count_eq_point_count {P L : Type u} [ L] [fintype P] [fintype L] (hPL : = ) {p : P} {l : L} (hpl : p l) :
theorem configuration.has_points.line_count_eq_point_count {P L : Type u} [ L] [fintype P] [fintype L] (hPL : = ) {p : P} {l : L} (hpl : p l) :
noncomputable def configuration.has_lines.has_points {P L : Type u} [ L] [fintype P] [fintype L] (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.

Equations
noncomputable def configuration.has_points.has_lines {P L : Type u} [ L] [fintype P] [fintype L] (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.

Equations
@[class]
structure configuration.projective_plane (P L : Type u) [ L] :
Type u
• to_nondegenerate :
• mk_point : Π {l₁ l₂ : L}, l₁ l₂ → P
• mk_point_ax : ∀ {l₁ l₂ : L} (h : l₁ l₂),
• mk_line : Π {p₁ p₂ : P}, p₁ p₂ → L
• mk_line_ax : ∀ {p₁ p₂ : P} (h : p₁ p₂),
• exists_config : ∃ (p₁ p₂ p₃ : P) (l₁ 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 of this typeclass
Instances of other typeclasses for configuration.projective_plane
• configuration.projective_plane.has_sizeof_inst
@[protected, instance]
def configuration.projective_plane.has_points (P L : Type u) [ L] [h : L] :
Equations
@[protected, instance]
def configuration.projective_plane.has_lines (P L : Type u) [ L] [h : L] :
Equations
@[protected, instance]
Equations
noncomputable def configuration.projective_plane.order (P L : Type u) [ 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
theorem configuration.projective_plane.line_count_eq_line_count {P : Type u} (L : Type u) [ L] [finite P] [finite L] (p q : P) :
theorem configuration.projective_plane.point_count_eq_point_count (P : Type u) {L : Type u} [ L] [finite P] [finite L] (l m : L) :
theorem configuration.projective_plane.line_count_eq_point_count {P L : Type u} [ L] [finite P] [finite L] (p : P) (l : L) :
theorem configuration.projective_plane.dual.order (P L : Type u) [ L] [finite P] [finite L] :
theorem configuration.projective_plane.line_count_eq {P : Type u} (L : Type u) [ L] [finite P] [finite L] (p : P) :
theorem configuration.projective_plane.point_count_eq (P : Type u) {L : Type u} [ L] [finite P] [finite L] (l : L) :
theorem configuration.projective_plane.one_lt_order (P L : Type u) [ L] [finite P] [finite L] :
theorem configuration.projective_plane.two_lt_line_count {P : Type u} (L : Type u) [ L] [finite P] [finite L] (p : P) :
theorem configuration.projective_plane.two_lt_point_count (P : Type u) {L : Type u} [ L] [finite P] [finite L] (l : L) :
theorem configuration.projective_plane.card_points (P L : Type u) [ L] [fintype P] [finite L] :
theorem configuration.projective_plane.card_lines (P L : Type u) [ L] [finite P] [fintype L] :