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

source

def configuration.dual (P : Type u_1) :

Type u_1

A type synonym.

Equations

configuration.dual P = P

Instances for configuration.dual

source

@[protected, instance]

def configuration.dual.inhabited (P : Type u_1) [this : inhabited P] :

inhabited (configuration.dual P)

Equations

configuration.dual.inhabited P = this

source

@[protected, instance]

def configuration.dual.finite (P : Type u_1) [finite P] :

finite (configuration.dual P)

source

@[protected, instance]

def configuration.dual.fintype (P : Type u_1) [this : fintype P] :

fintype (configuration.dual P)

Equations

configuration.dual.fintype P = this

source

@[protected, instance]

def configuration.dual.has_mem (P : Type u_1) (L : Type u_2) [has_mem P L] :

has_mem (configuration.dual L) (configuration.dual P)

Equations

configuration.dual.has_mem P L = {mem := function.swap has_mem.mem}

source

@[class]

structure configuration.nondegenerate (P : Type u_1) (L : Type u_2) [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:

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 of this typeclass

source

@[instance]

def configuration.has_points.to_nondegenerate (P : Type u_1) (L : Type u_2) [has_mem P L] [self : configuration.has_points P L] :

configuration.nondegenerate P L

source

@[class]

structure configuration.has_points (P : Type u_1) (L : Type u_2) [has_mem P 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₂), configuration.has_points.mk_point h ∈ l₁ ∧ configuration.has_points.mk_point h ∈ 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

source

@[instance]

def configuration.has_lines.to_nondegenerate (P : Type u_1) (L : Type u_2) [has_mem P L] [self : configuration.has_lines P L] :

configuration.nondegenerate P L

source

@[class]

structure configuration.has_lines (P : Type u_1) (L : Type u_2) [has_mem P 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₂), p₁ ∈ configuration.has_lines.mk_line h ∧ p₂ ∈ configuration.has_lines.mk_line h

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

source

@[protected, instance]

def configuration.dual.nondegenerate (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.nondegenerate P L] :

configuration.nondegenerate (configuration.dual L) (configuration.dual P)

source

@[protected, instance]

def configuration.dual.has_lines (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.has_points P L] :

configuration.has_lines (configuration.dual L) (configuration.dual P)

Equations

configuration.dual.has_lines P L = {exists_point := _, exists_line := _, eq_or_eq := _, mk_line := configuration.has_points.mk_point _inst_2, mk_line_ax := _}

source

@[protected, instance]

def configuration.dual.has_points (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.has_lines P L] :

configuration.has_points (configuration.dual L) (configuration.dual P)

Equations

configuration.dual.has_points P L = {exists_point := _, exists_line := _, eq_or_eq := _, mk_point := configuration.has_lines.mk_line _inst_2, mk_point_ax := _}

source

theorem configuration.has_points.exists_unique_point (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.has_points P L] (l₁ l₂ : L) (hl : l₁ ≠ l₂) :

∃! (p : P), p ∈ l₁ ∧ p ∈ l₂

source

theorem configuration.has_lines.exists_unique_line (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.has_lines P L] (p₁ p₂ : P) (hp : p₁ ≠ p₂) :

∃! (l : L), p₁ ∈ l ∧ p₂ ∈ l

source

theorem configuration.nondegenerate.exists_injective_of_card_le {P : Type u_1} {L : Type u_2} [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.

source

noncomputable def configuration.line_count {P : Type u_1} (L : Type u_2) [has_mem P L] (p : P) :

ℕ

Number of points on a given line.

Equations

configuration.line_count L p = nat.card {l // p ∈ l}

source

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

ℕ

Number of lines through a given point.

Equations

configuration.point_count P l = nat.card {p // p ∈ l}

source

theorem configuration.sum_line_count_eq_sum_point_count (P : Type u_1) (L : Type u_2) [has_mem P L] [fintype P] [fintype L] :

finset.univ.sum (λ (p : P), configuration.line_count L p) = finset.univ.sum (λ (l : L), configuration.point_count P l)

source

theorem configuration.has_lines.point_count_le_line_count {P : Type u_1} {L : Type u_2} [has_mem P L] [configuration.has_lines P L] {p : P} {l : L} (h : p ∉ l) [finite {l // p ∈ l}] :

configuration.point_count P l ≤ configuration.line_count L p

source

theorem configuration.has_points.line_count_le_point_count {P : Type u_1} {L : Type u_2} [has_mem P L] [configuration.has_points P L] {p : P} {l : L} (h : p ∉ l) [hf : finite {p // p ∈ l}] :

configuration.line_count L p ≤ configuration.point_count P l

source

theorem configuration.has_lines.card_le (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.has_lines P L] [fintype P] [fintype L] :

fintype.card P ≤ fintype.card L

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

source

theorem configuration.has_points.card_le (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.has_points P L] [fintype P] [fintype L] :

fintype.card L ≤ fintype.card P

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

source

theorem configuration.has_lines.exists_bijective_of_card_eq {P : Type u_1} {L : Type u_2} [has_mem P L] [configuration.has_lines P L] [fintype P] [fintype L] (h : fintype.card P = fintype.card L) :

∃ (f : L → P), function.bijective f ∧ ∀ (l : L), configuration.point_count P l = configuration.line_count L (f l)

source

theorem configuration.has_lines.line_count_eq_point_count {P : Type u_1} {L : Type u_2} [has_mem P L] [configuration.has_lines P L] [fintype P] [fintype L] (hPL : fintype.card P = fintype.card L) {p : P} {l : L} (hpl : p ∉ l) :

configuration.line_count L p = configuration.point_count P l

source

theorem configuration.has_points.line_count_eq_point_count {P : Type u_1} {L : Type u_2} [has_mem P L] [configuration.has_points P L] [fintype P] [fintype L] (hPL : fintype.card P = fintype.card L) {p : P} {l : L} (hpl : p ∉ l) :

configuration.line_count L p = configuration.point_count P l

source

noncomputable def configuration.has_lines.has_points {P : Type u_1} {L : Type u_2} [has_mem P L] [configuration.has_lines P L] [fintype P] [fintype L] (h : fintype.card P = fintype.card L) :

configuration.has_points P L

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

configuration.has_lines.has_points h = let this : ∀ (l₁ l₂ : L), l₁ ≠ l₂ → (∃ (p : P), p ∈ l₁ ∧ p ∈ l₂) := _ in {exists_point := _, exists_line := _, eq_or_eq := _, mk_point := λ (l₁ l₂ : L) (hl : l₁ ≠ l₂), classical.some _, mk_point_ax := _}

source

noncomputable def configuration.has_points.has_lines {P : Type u_1} {L : Type u_2} [has_mem P L] [configuration.has_points P L] [fintype P] [fintype L] (h : fintype.card P = fintype.card L) :

configuration.has_lines P L

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

configuration.has_points.has_lines h = let this : configuration.has_points (configuration.dual L) (configuration.dual P) := configuration.has_lines.has_points _ in {exists_point := _, exists_line := _, eq_or_eq := _, mk_line := λ (_x _x_1 : P), configuration.has_points.mk_point, mk_line_ax := _}

source

@[instance]

def configuration.projective_plane.to_has_points (P : Type u_1) (L : Type u_2) [has_mem P L] [self : configuration.projective_plane P L] :

configuration.has_points P L

source

@[instance]

def configuration.projective_plane.to_has_lines (P : Type u_1) (L : Type u_2) [has_mem P L] [self : configuration.projective_plane P L] :

configuration.has_lines P L

source

@[class]

structure configuration.projective_plane (P : Type u_1) (L : Type u_2) [has_mem P 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₂), configuration.projective_plane.mk_point h ∈ l₁ ∧ configuration.projective_plane.mk_point h ∈ l₂
mk_line : Π {p₁ p₂ : P}, p₁ ≠ p₂ → L
mk_line_ax : ∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ configuration.projective_plane.mk_line h ∧ p₂ ∈ configuration.projective_plane.mk_line h
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

configuration.projective_plane.configuration.dual.projective_plane

Instances of other typeclasses for configuration.projective_plane

configuration.projective_plane.has_sizeof_inst

source

@[protected, instance]

def configuration.projective_plane.configuration.dual.projective_plane (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.projective_plane P L] :

configuration.projective_plane (configuration.dual L) (configuration.dual P)

Equations

configuration.projective_plane.configuration.dual.projective_plane P L = {exists_point := _, exists_line := _, eq_or_eq := _, mk_point := configuration.has_points.mk_point (configuration.dual.has_points P L), mk_point_ax := _, mk_line := configuration.has_lines.mk_line (configuration.dual.has_lines P L), mk_line_ax := _, exists_config := _}

source

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

configuration.projective_plane.order P L = configuration.line_count L (classical.some configuration.projective_plane.exists_config) - 1

source

theorem configuration.projective_plane.card_points_eq_card_lines (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.projective_plane P L] [fintype P] [fintype L] :

fintype.card P = fintype.card L

source

theorem configuration.projective_plane.line_count_eq_line_count {P : Type u_1} (L : Type u_2) [has_mem P L] [configuration.projective_plane P L] [finite P] [finite L] (p q : P) :

configuration.line_count L p = configuration.line_count L q

source

theorem configuration.projective_plane.point_count_eq_point_count (P : Type u_1) {L : Type u_2} [has_mem P L] [configuration.projective_plane P L] [finite P] [finite L] (l m : L) :

configuration.point_count P l = configuration.point_count P m

source

theorem configuration.projective_plane.line_count_eq_point_count {P : Type u_1} {L : Type u_2} [has_mem P L] [configuration.projective_plane P L] [finite P] [finite L] (p : P) (l : L) :

configuration.line_count L p = configuration.point_count P l

source

theorem configuration.projective_plane.dual.order (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.projective_plane P L] [finite P] [finite L] :

configuration.projective_plane.order (configuration.dual L) (configuration.dual P) = configuration.projective_plane.order P L

source

theorem configuration.projective_plane.line_count_eq {P : Type u_1} (L : Type u_2) [has_mem P L] [configuration.projective_plane P L] [finite P] [finite L] (p : P) :

configuration.line_count L p = configuration.projective_plane.order P L + 1

source

theorem configuration.projective_plane.point_count_eq (P : Type u_1) {L : Type u_2} [has_mem P L] [configuration.projective_plane P L] [finite P] [finite L] (l : L) :

configuration.point_count P l = configuration.projective_plane.order P L + 1

source

theorem configuration.projective_plane.one_lt_order (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.projective_plane P L] [finite P] [finite L] :

1 < configuration.projective_plane.order P L

source

theorem configuration.projective_plane.two_lt_line_count {P : Type u_1} (L : Type u_2) [has_mem P L] [configuration.projective_plane P L] [finite P] [finite L] (p : P) :

2 < configuration.line_count L p

source

theorem configuration.projective_plane.two_lt_point_count (P : Type u_1) {L : Type u_2} [has_mem P L] [configuration.projective_plane P L] [finite P] [finite L] (l : L) :

2 < configuration.point_count P l

source

theorem configuration.projective_plane.card_points (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.projective_plane P L] [fintype P] [finite L] :

fintype.card P = configuration.projective_plane.order P L ^ 2 + configuration.projective_plane.order P L + 1

source

theorem configuration.projective_plane.card_lines (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.projective_plane P L] [finite P] [fintype L] :

fintype.card L = configuration.projective_plane.order P L ^ 2 + configuration.projective_plane.order P L + 1