mathlib documentation

combinatorics.configuration

Configurations of Points and lines #

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

Main definitions #

Main statements #

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

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) [has_mem P L] :
Type u

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
theorem configuration.has_points.exists_unique_point (P L : Type u) [has_mem P L] [configuration.has_points P L] (l₁ l₂ : L) (hl : l₁ l₂) :
∃! (p : P), p l₁ p l₂
theorem configuration.has_lines.exists_unique_line (P L : Type u) [has_mem P L] [configuration.has_lines P 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} [has_mem 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.line_count {P : Type u} (L : Type u) [has_mem P L] (p : P) :

Number of points on a given line.

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

Number of lines through a given point.

Equations
theorem configuration.has_points.line_count_le_point_count {P L : Type u} [has_mem P L] [configuration.has_points P L] {p : P} {l : L} (h : p l) [hf : finite {p // p l}] :

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

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

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

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) [has_mem P L] :
Type u

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
noncomputable def configuration.projective_plane.order (P L : Type u) [has_mem P L] [configuration.projective_plane 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