# Zulip Chat Archive

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

#### Quinn Culver (Jan 03 2023 at 23:36):

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

?

#### Johan Commelin (Jan 04 2023 at 16:52):

See glossary#binder

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