Documentation

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

def Configuration.Dual (P : Type u_1) :
Type u_1

A type synonym.

Equations
Instances For
    Equations
    • = inst
    class Configuration.Nondegenerate (P : Type u_1) (L : Type u_2) [Membership P 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.
    • exists_point : ∀ (l : L), ∃ (p : P), pl
    • exists_line : ∀ (p : P), ∃ (l : L), pl
    • eq_or_eq : ∀ {p₁ p₂ : P} {l₁ l₂ : L}, p₁ l₁p₂ l₁p₁ l₂p₂ l₂p₁ = p₂ l₁ = l₂
    Instances
      theorem Configuration.Nondegenerate.exists_point {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.Nondegenerate P L] (l : L) :
      ∃ (p : P), pl
      theorem Configuration.Nondegenerate.exists_line {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.Nondegenerate P L] (p : P) :
      ∃ (l : L), pl
      theorem Configuration.Nondegenerate.eq_or_eq {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.Nondegenerate P L] {p₁ : P} {p₂ : P} {l₁ : L} {l₂ : L} :
      p₁ l₁p₂ l₁p₁ l₂p₂ l₂p₁ = p₂ l₁ = l₂
      class Configuration.HasPoints (P : Type u_1) (L : Type u_2) [Membership P L] extends Configuration.Nondegenerate :
      Type (max u_1 u_2)

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

      Instances
        theorem Configuration.HasPoints.mkPoint_ax {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.HasPoints P L] {l₁ : L} {l₂ : L} (h : l₁ l₂) :
        class Configuration.HasLines (P : Type u_1) (L : Type u_2) [Membership P L] extends Configuration.Nondegenerate :
        Type (max u_1 u_2)

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

        Instances
          theorem Configuration.HasLines.mkLine_ax {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.HasLines P L] {p₁ : P} {p₂ : P} (h : p₁ p₂) :
          theorem Configuration.HasPoints.existsUnique_point (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.HasPoints P L] (l₁ : L) (l₂ : L) (hl : l₁ l₂) :
          ∃! p : P, p l₁ p l₂
          theorem Configuration.HasLines.existsUnique_line (P : Type u_1) (L : Type u_2) [Membership P L] [Configuration.HasLines P L] (p₁ : 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} [Membership P L] [Configuration.Nondegenerate P L] [Fintype P] [Fintype L] (h : Fintype.card L Fintype.card P) :
          ∃ (f : LP), Function.Injective f ∀ (l : L), f ll

          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.lineCount {P : Type u_1} (L : Type u_2) [Membership P L] (p : P) :

          Number of points on a given line.

          Equations
          Instances For
            noncomputable def Configuration.pointCount (P : Type u_1) {L : Type u_2} [Membership P L] (l : L) :

            Number of lines through a given point.

            Equations
            Instances For
              theorem Configuration.HasLines.pointCount_le_lineCount {P : Type u_1} {L : Type u_2} [Membership P L] [Configuration.HasLines P L] {p : P} {l : L} (h : pl) [Finite { l : L // p l }] :
              theorem Configuration.HasPoints.lineCount_le_pointCount {P : Type u_1} {L : Type u_2} [Membership P L] [Configuration.HasPoints P L] {p : P} {l : L} (h : pl) [hf : Finite { p : 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
              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.

                Equations
                Instances For
                  class Configuration.ProjectivePlane (P : Type u_1) (L : Type u_2) [Membership P L] extends Configuration.HasPoints :
                  Type (max u_1 u_2)

                  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
                    theorem Configuration.ProjectivePlane.exists_config {P : Type u_1} {L : Type u_2} [Membership P L] [self : Configuration.ProjectivePlane P L] :
                    ∃ (p₁ : P) (p₂ : P) (p₃ : P) (l₁ : L) (l₂ : L) (l₃ : L), p₁l₂ p₁l₃ p₂l₁ p₂ l₂ p₂ l₃ p₃l₁ p₃ l₂ p₃l₃
                    Equations
                    • One or more equations did not get rendered due to their size.

                    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
                    Instances For