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

.

A configuration is nondegenerate if:

- there does not exist a line that passes through all of the points,
- there does not exist a point that is on all of the lines,
- there is at most one line through any two points,
- any two lines have at most one intersection point. Conditions 3 and 4 are equivalent.

## Instances

- 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₂

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

## Instances

- 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

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

## Instances

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`

.

Number of points on a given line.

## Instances For

Number of lines through a given point.

## Instances For

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.

## Instances For

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

- 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

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

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.