# mathlib3documentation

combinatorics.configuration

# Configurations of Points and lines #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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_1) :
Type u_1

A type synonym.

Equations
Instances for configuration.dual
@[protected, instance]
def configuration.dual.inhabited (P : Type u_1) [this : inhabited P] :
Equations
@[protected, instance]
def configuration.dual.finite (P : Type u_1) [finite P] :
@[protected, instance]
def configuration.dual.fintype (P : Type u_1) [this : fintype P] :
Equations
@[protected, instance]
def configuration.dual.has_mem (P : Type u_1) (L : Type u_2) [ L] :
Equations
@[class]
structure configuration.nondegenerate (P : Type u_1) (L : Type u_2) [ 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.
Instances of this typeclass
@[instance]
def configuration.has_points.to_nondegenerate (P : Type u_1) (L : Type u_2) [ L] [self : L] :
@[class]
structure configuration.has_points (P : Type u_1) (L : Type u_2) [ L] :
Type (max u_1 u_2)
• 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₂
• 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
@[instance]
def configuration.has_lines.to_nondegenerate (P : Type u_1) (L : Type u_2) [ L] [self : L] :
@[class]
structure configuration.has_lines (P : Type u_1) (L : Type u_2) [ L] :
Type (max u_1 u_2)
• 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₂
• 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 : Type u_1) (L : Type u_2) [ L]  :
@[protected, instance]
def configuration.dual.has_lines (P : Type u_1) (L : Type u_2) [ L]  :
Equations
@[protected, instance]
def configuration.dual.has_points (P : Type u_1) (L : Type u_2) [ L]  :
Equations
theorem configuration.has_points.exists_unique_point (P : Type u_1) (L : Type u_2) [ L] (l₁ l₂ : L) (hl : l₁ l₂) :
∃! (p : P), p l₁ p l₂
theorem configuration.has_lines.exists_unique_line (P : Type u_1) (L : Type u_2) [ 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} [ 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_1} (L : Type u_2) [ L] (p : P) :

Number of points on a given line.

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

Number of lines through a given point.

Equations
theorem configuration.sum_line_count_eq_sum_point_count (P : Type u_1) (L : Type u_2) [ 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 : Type u_1} {L : Type u_2} [ L] {p : P} {l : L} (h : p l) [finite {l // p l}] :
theorem configuration.has_points.line_count_le_point_count {P : Type u_1} {L : Type u_2} [ L] {p : P} {l : L} (h : p l) [hf : finite {p // p l}] :
theorem configuration.has_lines.card_le (P : Type u_1) (L : Type u_2) [ 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 : Type u_1) (L : Type u_2) [ 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 : Type u_1} {L : Type u_2} [ L] [fintype P] [fintype L] (h : = ) :
(f : L P), (l : L),
theorem configuration.has_lines.line_count_eq_point_count {P : Type u_1} {L : Type u_2} [ L] [fintype P] [fintype L] (hPL : = ) {p : P} {l : L} (hpl : p l) :
theorem configuration.has_points.line_count_eq_point_count {P : Type u_1} {L : Type u_2} [ L] [fintype P] [fintype L] (hPL : = ) {p : P} {l : L} (hpl : p l) :
noncomputable def configuration.has_lines.has_points {P : Type u_1} {L : Type u_2} [ 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 : Type u_1} {L : Type u_2} [ 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
@[instance]
def configuration.projective_plane.to_has_points (P : Type u_1) (L : Type u_2) [ L] [self : L] :
@[instance]
def configuration.projective_plane.to_has_lines (P : Type u_1) (L : Type u_2) [ L] [self : L] :
@[class]
structure configuration.projective_plane (P : Type u_1) (L : Type u_2) [ L] :
Type (max u_1 u_2)
• 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₂
• 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]
Equations
noncomputable def configuration.projective_plane.order (P : Type u_1) (L : Type u_2) [ 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_1} (L : Type u_2) [ L] [finite P] [finite L] (p q : P) :
theorem configuration.projective_plane.point_count_eq_point_count (P : Type u_1) {L : Type u_2} [ L] [finite P] [finite L] (l m : L) :
theorem configuration.projective_plane.line_count_eq_point_count {P : Type u_1} {L : Type u_2} [ L] [finite P] [finite L] (p : P) (l : L) :
theorem configuration.projective_plane.dual.order (P : Type u_1) (L : Type u_2) [ L] [finite P] [finite L] :
theorem configuration.projective_plane.line_count_eq {P : Type u_1} (L : Type u_2) [ L] [finite P] [finite L] (p : P) :
theorem configuration.projective_plane.point_count_eq (P : Type u_1) {L : Type u_2} [ L] [finite P] [finite L] (l : L) :
theorem configuration.projective_plane.one_lt_order (P : Type u_1) (L : Type u_2) [ L] [finite P] [finite L] :
theorem configuration.projective_plane.two_lt_line_count {P : Type u_1} (L : Type u_2) [ L] [finite P] [finite L] (p : P) :
theorem configuration.projective_plane.two_lt_point_count (P : Type u_1) {L : Type u_2} [ L] [finite P] [finite L] (l : L) :
theorem configuration.projective_plane.card_points (P : Type u_1) (L : Type u_2) [ L] [fintype P] [finite L] :
theorem configuration.projective_plane.card_lines (P : Type u_1) (L : Type u_2) [ L] [finite P] [fintype L] :