Desarguean projective plane

Stream: general

[Quinn Culver]

Aloha,

Why doesn't the definition of configuration.desarguean below work? I'm trying to define a projective plane to be desarguean if any six points satisfying centrally_perspective satisfy axially_perspective.

import combinatorics.configuration
open configuration.projective_plane

universe u

variables (P L : Type u) [has_mem P L] [configuration.projective_plane P L]

def centrally_perspective (p₀ p₁ p₂ q₀ q₁ q₂ : P)
(h₀ : p₀ ≠ q₀)
(h₁ : p₁ ≠ q₁)
(h₂ : p₂ ≠ q₂)
(h₃ : (mk_line h₀) ≠ (mk_line h₁ : L)):
Prop := (
  ((mk_point h₃ : P) ∈ (mk_line h₂ : L))
)

def axially_perspective (p₀ p₁ p₂ q₀ q₁ q₂ : P)
(hpdist₀₁ : p₀ ≠ p₁)
(hpdist₀₂ : p₀ ≠ p₂)
(hpdist₁₂ : p₁ ≠ p₂)
(hqdist₀₁ : q₀ ≠ q₁)
(hqdist₀₂ : q₀ ≠ q₂)
(hqdist₁₂ : q₁ ≠ q₂)
(hpqdist₀₁ : (mk_line hpdist₀₁ : L) ≠ (mk_line hqdist₀₁ : L))
(hpqdist₀₂ : (mk_line hpdist₀₂ : L) ≠ (mk_line hqdist₀₂ : L))
(hpqdist₁₂ : (mk_line hpdist₁₂ : L) ≠ (mk_line hqdist₁₂ : L))
(g : (mk_point hpqdist₀₁ : P) ≠ (mk_point hpqdist₀₂ : P) )
--TODO: rename g
:
Prop := (
  (mk_point hpqdist₁₂ :P) ∈ (
    mk_line g : L)
)


def configuration.desarguean : Prop :=
(
  ∀ (p₀ p₁ p₂ q₀ q₁ q₂ : P),
  centrally_perspective (p₀ p₁ p₂ q₀ q₁ q₂ : P) →
  axially_perspective (p₀ p₁ p₂ q₀ q₁ q₂ : P)
)

Side question: Is this an appropriate question for the general stream? If not, for where?

[Eric Wieser]

centrally_perspective (p₀ p₁ p₂ q₀ q₁ q₂ : P) should be centrally_perspective p₀ p₁ p₂ q₀ q₁ q₂ and similar for the other one

[Eric Wieser]

Your spelling means "treat p₀ as a function taking 5 arguments"

[Reid Barton]

You will also have to do something about all those nondegeneracy arguments

[Quinn Culver]

@Reid Barton Mind saying more? Do you know anywhere I can see appropriate handling of nondegeneracy?

[Reid Barton]

It is just that centrally_perspective p₀ p₁ p₂ q₀ q₁ q₂ is a function of 4 more arguments and axially_perspective p₀ p₁ p₂ q₀ q₁ q₂ is a function of 10 more arguments

[Quinn Culver]

I see.

[Eric Wieser]

Are you trying to say "six points are axially perspective if they are distinct and ..." or "six distinct points are axially perspective if ..."?

[Eric Wieser]

The difference being that only the former lets you say "the same point six times is not axially perspective"

[Junyan Xu]

My first instinct for defining centrally_perspective is

def centrally_perspective (p₀ p₁ p₂ q₀ q₁ q₂ : P) : Prop :=
∃ (l₀ l₁ l₂ : L) (r : P), r ∈ l₀ ∧ r ∈ l₁ ∧ r ∈ l₂ ∧ p₀ ∈ l₀ ∧ q₀ ∈ l₀ ∧ p₁ ∈ l₁ ∧ q₁ ∈ l₁ ∧ p₂ ∈ l₂ ∧ q₂ ∈ l₂

You may add degeneracy conditions in theorems if the proofs require them.

[Junyan Xu]

I came up with this self-dual definition of Desarguesian property of a projective plane, without any non-degeneracy conditions (I don't yet impose even that the two triangles are individually nondegenerate), and conjecture it's equivalent to the normal one with non-degeneracy conditions, but the equivalence is maybe tons of case analysis ...

import combinatorics.configuration
open configuration.projective_plane

universe u

variables (P L : Type u) [has_mem P L] [configuration.projective_plane P L]

structure triangle :=
(p₀ p₁ p₂ : P)
(l₀ l₁ l₂ : L)
(i₀₁ : p₀ ∈ l₁)
(i₀₂ : p₀ ∈ l₂)
(i₁₀ : p₁ ∈ l₀)
(i₁₂ : p₁ ∈ l₂)
(i₂₀ : p₂ ∈ l₀)
(i₂₁ : p₂ ∈ l₁)

variables {P}
def collinear (p₀ p₁ p₂ : P) : Prop := ∃ l : L, p₀ ∈ l ∧ p₁ ∈ l ∧ p₂ ∈ l

variables (P) {L}
def concurrent (l₀ l₁ l₂ : L) : Prop := ∃ p : P, p ∈ l₀ ∧ p ∈ l₁ ∧ p ∈ l₂

variables {P}
def centrally_perspective (T₁ T₂ : triangle P L) : Prop :=
∃ p : P, collinear L p T₁.p₀ T₂.p₀ ∧ collinear L p T₁.p₁ T₂.p₁ ∧ collinear L p T₁.p₂ T₂.p₂

def axially_perspective (T₁ T₂ : triangle P L) : Prop :=
∃ l : L, concurrent P l T₁.l₀ T₂.l₀ ∧ concurrent P l T₁.l₁ T₂.l₁ ∧ concurrent P l T₁.l₂ T₂.l₂

variables (P L)
def is_desarguesian : Prop :=
∀ T₁ T₂ : triangle P L, centrally_perspective T₁ T₂ ↔ axially_perspective T₁ T₂

[Mario Carneiro]

is one direction of the biconditional in is_desarguesian always true?

[Junyan Xu]

No, because the dual of one direction is the other direction, so if you show one direction for all projective planes, you get the other direction by specializing to the dual projective plane. However, one direction actually implies the other direction even when considering a single projective plane:
image.png

[Quinn Culver]

What's the difference b/t parentheses and curly brackets in variables (P) {L}?

[Johan Commelin]

See glossary#binder

[Junyan Xu]

What's the difference b/t parentheses and curly brackets in variables (P) {L}?

Here P and L are already declared, so variables (P) {L} changes P to explicit and L to implicit.

[Quinn Culver]

Junyan Xu said:

What's the difference b/t parentheses and curly brackets in variables (P) {L}?

Here P and L are already declared, so variables (P) {L} changes P to explicit and L to implicit.

Why not make P implicit in concurrent as well?

[Junyan Xu]

Because if you write concurrent l₀ l₁ l₂, Lean doesn't know what P to use.

[Yaël Dillies]

Probably we want to make the types bundled in projective_plane.

[Yaël Dillies]

It's not like projective_plane P L has any interesting algebraic structure (or am I unaware?)

[Quinn Culver]

Junyan Xu said:

I came up with this self-dual definition of Desarguesian property of a projective plane, without any non-degeneracy conditions (I don't yet impose even that the two triangles are individually nondegenerate), and conjecture it's equivalent to the normal one with non-degeneracy conditions, but the equivalence is maybe tons of case analysis ...

import combinatorics.configuration
open configuration.projective_plane

universe u

variables (P L : Type u) [has_mem P L] [configuration.projective_plane P L]

structure triangle :=
(p₀ p₁ p₂ : P)
(l₀ l₁ l₂ : L)
(i₀₁ : p₀ ∈ l₁)
(i₀₂ : p₀ ∈ l₂)
(i₁₀ : p₁ ∈ l₀)
(i₁₂ : p₁ ∈ l₂)
(i₂₀ : p₂ ∈ l₀)
(i₂₁ : p₂ ∈ l₁)

variables {P}
def collinear (p₀ p₁ p₂ : P) : Prop := ∃ l : L, p₀ ∈ l ∧ p₁ ∈ l ∧ p₂ ∈ l

variables (P) {L}
def concurrent (l₀ l₁ l₂ : L) : Prop := ∃ p : P, p ∈ l₀ ∧ p ∈ l₁ ∧ p ∈ l₂

variables {P}
def centrally_perspective (T₁ T₂ : triangle P L) : Prop :=
∃ p : P, collinear L p T₁.p₀ T₂.p₀ ∧ collinear L p T₁.p₁ T₂.p₁ ∧ collinear L p T₁.p₂ T₂.p₂

def axially_perspective (T₁ T₂ : triangle P L) : Prop :=
∃ l : L, concurrent P l T₁.l₀ T₂.l₀ ∧ concurrent P l T₁.l₁ T₂.l₁ ∧ concurrent P l T₁.l₂ T₂.l₂

variables (P L)
def is_desarguesian : Prop :=
∀ T₁ T₂ : triangle P L, centrally_perspective T₁ T₂ ↔ axially_perspective T₁ T₂

Why didn't you use configuration.is_desarguesian as in the suggestion here?

[Quinn Culver]

@Junyan Xu In your variables (P L : Type u) [has_mem P L] [configuration.projective_plane P L], is the [has_mem P L] needed? Seems like since mathlib's configuration.lean has variables (P L : Type*) [has_mem P L] on line 41, that might not be necessary. True? (Just trying to understand.)

[Junyan Xu]

docs#configuration.projective_plane takes [has_mem P L] so it's definitely necessary. If you are working in that file and you are in a section where [has_mem P L] is declared as a variable, then it will be automatically included in all declarations (def/lemma) within the section that mentions P and L.