Using a structure

Stream: new members

[Quinn Culver]

Aloha,

How do I use a structure? I want to formalize the fundamental theorem of projective geometry, which says

if Π is a Desarguean projective plane, then it's coordinatized by a (certain) division ring D.

I see mathlib has a "structure" configuration.projective_plane, which I guess is what I want to use (right?) . How do I?

[Johan Commelin]

I think you can start with

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

def configuration.desarguean : Prop :=
-- fill this in

[Johan Commelin]

@Quinn Culver What is the definition of Desarguean that you would like to use?

[Quinn Culver]

Johan Commelin said:

Quinn Culver What is the definition of Desarguean that you would like to use?

Π is Desarguea iff whenever a set of 6 points are perspective from a point, then they are perspective from a line.

[Junyan Xu]

Is it not spelt Desarguesian?

[Yaël Dillies]

It's called arguesian plane or desarguesian plane.

[Quinn Culver]

I got my spelling from a document written by old gentleman who's an expert in the field. That suggests his spelling might've been in use once upon a time.

[Kevin Buzzard]

I bet the old gentleman wasn't Desargues. Probably Desargues wanted to keep his name intact :-) I was once taken to task on mathoverflow for referring to a collection of Frobenius elements as Frobenii.

[Quinn Culver]

Do the eponyms Ptolemic and/or Linnaean keep the names intact more that Desarguean, @Kevin Buzzard ?

[Junyan Xu]

Apparently Frobenii is in common use? stacks#0CC6 stacks#03SL

[Quinn Culver]

Following @Johan Commelin's suggestion, I'm getting error messages:

basic.lean:3:0
don't know how to synthesize placeholder
context:
P : Type u_1,
L : Type u_2,
_inst_1 : has_mem P L
⊢ Type u_1

basic.lean:3:39
type mismatch at application
  configuration.projective_plane P L
term
  L
has type
  Type u_2 : Type (u_2+1)
but is expected to have type
  Type u_1 : Type (u_1+1)

basic.lean:3:39
don't know how to synthesize placeholder
context:
P : Type u_1,
L : Type u_2,
_inst_1 : has_mem P L
⊢ has_mem P ?m_1

Please let me know why and how I could figure this out myself. Happy New Year!

[Junyan Xu]

You need to do

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

because of the universe restriction present in docs#configuration.projective_plane.

Maybe we should allow P and L to be in different universes? Mathlib seems usually maximally universe polymorphic, and a lot of restrictions have been removed from category theory, for example.

[Yaël Dillies]

I don't really see why we would need the points and lines to live in the same universe.

[Thomas Browning]

My vague memory is that it caused some headaches somewhere, but upon inspection it seems that I might be wrong.

[Thomas Browning]

#18039

[Quinn Culver]

What is @Junyan Xu 's code doing? Specifically, what is has_mem doing? And having used that code, how do I, for example, talk about the line containing two points, p q : P?

[Junyan Xu]

docs#has_mem contains the data of a relation between two types (the type of points P and the type of lines L here), which you can use ∈ to refer to (e.g. p ∈ l means p lies on l).

[Junyan Xu]

Apparently L can't be inferred from p and q, which may or may not be a problem ...

import combinatorics.configuration
universe u
variables (P L : Type u) [has_mem P L] [configuration.projective_plane P L]
variables (p q : P) (h : p ≠ q)
open configuration.projective_plane
#check (mk_line h : L) /- the line through p and q -/

[Quinn Culver]

Oh it's mem for membership!! :man_facepalming:

[Quinn Culver]

Why doesn't this work?

import combinatorics.configuration

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₂): Prop := (
  mk_point (mk_line h₀) (mk_line h₁) ∈ (mk_line h₂)
)

The first error message is unknown identifier 'mk_line'.

[Junyan Xu]

You didn't open configuration.projective_plane as I did.

[Hanting Zhang]

(deleted)

[Junyan Xu]

Also docs#configuration.projective_plane.mk_point takes the two lines as implicit arguments, so you need to write mk_point h where h : mk_line h₀ ≠ mk_line h₁.

[Quinn Culver]

(deleted)

[Quinn Culver]

I'm still getting an error when trying to add the hypothesis that the lines from mk_line aren't equal. Why?

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₁):
Prop := (
  mk_point h₃ ∈ (mk_line h₂)
)

The error is

don't know how to synthesize placeholder
context:
P : Type u,
p₀ p₁ p₂ q₀ q₁ q₂ : P,
h₀ : p₀ ≠ q₀,
h₁ : p₁ ≠ q₁,
h₂ : p₂ ≠ q₂
⊢ Type u Lean

[Junyan Xu]

You need to add type annotations like

(h₃ : mk_line h₀ ≠ (mk_line h₁ : L)):
Prop := (
  mk_point h₃ ∈ (mk_line h₂ : L)
)

because Lean can't infer L. I wonder whether we should bundle P and L together ...