Stream: general

Topic: Desarguean projective plane

Quinn Culver (Jan 03 2023 at 23:17):

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 (Jan 03 2023 at 23:20):

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 (Jan 03 2023 at 23:20):

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

Reid Barton (Jan 03 2023 at 23:22):

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

Quinn Culver (Jan 03 2023 at 23:34):

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

Reid Barton (Jan 03 2023 at 23:35):

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

I see.

Eric Wieser (Jan 03 2023 at 23:51):

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 (Jan 03 2023 at 23:52):

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

Junyan Xu (Jan 04 2023 at 03:35):

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 (Jan 04 2023 at 04:31):

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 (Jan 04 2023 at 04:33):

is one direction of the biconditional in is_desarguesian always true?

Junyan Xu (Jan 04 2023 at 04:44):

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 (Jan 04 2023 at 16:51):

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

Junyan Xu (Jan 04 2023 at 18:02):

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 (Jan 04 2023 at 20:34):

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 (Jan 04 2023 at 20:52):

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

Yaël Dillies (Jan 04 2023 at 20:59):

Probably we want to make the types bundled in projective_plane.

Yaël Dillies (Jan 04 2023 at 21:00):

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

Quinn Culver (Jan 06 2023 at 17:41):

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 (Feb 16 2023 at 17:21):

@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 (Feb 16 2023 at 17:34):

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.

Last updated: Dec 20 2023 at 11:08 UTC