Structure defined for Desarguesian proj plane

Stream: general

[Quinn Culver]

Here is the beginning of my attempt to define a structure associated to every Desarguesian projective plane. Why is my attempt instance : has_zero proj_plane_div_ring P L := proj_plane_div_ring.a₁ to define the zero element causing an error?

import basic combinatorics.configuration

open configuration

universe u

variables {P L : Type u} [has_mem P L] [configuration.projective_plane P L]

variables (P L)
structure proj_plane_div_ring :=
(hdesarg : is_desarguesian P L)
(a₁ a₂ c₁₃ c₂₃ : P)
(hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃)

instance : has_zero proj_plane_div_ring P L := proj_plane_div_ring.a₁

The error is

  has_zero proj_plane_div_ring
term
  proj_plane_div_ring
has type
  Π (P L : Type ?) [_inst_1 : has_mem P L] [_inst_2 : projective_plane P L], Type ? : Type (?+1)
but is expected to have type
  Type ? : Type (?+1)

Any other comments, critiques, etc. would be most welcome.

[Alex J. Best]

The error message is trying to tell you that you need brackets

instance : has_zero (proj_plane_div_ring P L)

[Quinn Culver]

Thanks that worked. But now proj_plane_div_ring.a₁ is yielding the error

type mismatch, term
  proj_plane_div_ring.a₁
has type
  proj_plane_div_ring ?m_1 ?m_2 → ?m_1 : Type ?
but is expected to have type
  has_zero (proj_plane_div_ring P L) : Type u

[Alex J. Best]

has_zero is a structure with a single field, not just a bare term of that type, so you need to use a syntax to construct an element of that type, i.e. {zero := blah} (or anonymous constructor syntax with \<blah\>

[Quinn Culver]

I tried the anonymous constructor syntax, instance : has_zero (proj_plane_div_ring P L) := ⟨proj_plane_div_ring.a₁⟩, but got the same error.

[Reid Barton]

You would need to give six arguments since your structure has six fields.

[Reid Barton]

So I assume you haven't said what you meant to say

[Eric Wieser]

instance : has_zero (proj_plane_div_ring P L) means "there is a proj_plane_div_ring (aka a choice of four points in the P and L projective plane) we will call 0"

[Eric Wieser]

proj_plane_div_ring.a₁ means "given an existing choice of those four points, give me the first one"

[Eric Wieser]

I suspect you meant

instance [proj_plane_div_ring P L] : has_zero P := {zero := proj_plane_div_ring.a₁}

but that won't actualy help you because lean won't find L

[Quinn Culver]

Which part is looking for L?

[Quinn Culver]

Oh are you saying that there's a problem with the L in [proj_plane_div_ring P L]?

[Eric Wieser]

Yes, exactly; lean won't know which L to try since it only knows P from the goal

[Eric Wieser]

I get the feeling your question might be an #xy problem; what do you want the 0 for?

[Quinn Culver]

I'm trying ultimately to formalize the fundamental theorem of projective geometry, which requires defining a division ring that coordinatizes a Desarguesian Projective plane.

[Quinn Culver]

In the proof I'm following it starts with four points, no three of which are colinear, and uses one of them a₁ as the zero element.

[Quinn Culver]

Does that clear it up?

[Quinn Culver]

To define the zero element, I tried following Mathematics in Lean's construction of the Guassian integers (section 6.3).

[Reid Barton]

But what is the division ring? I mean its underlying set/type.

[Quinn Culver]

It's the set of points on the line from a₁ to a₂ excluding a₂.

[Reid Barton]

So then that is the thing that you need to define has_zero etc. instances for

[Quinn Culver]

Okay thanks. I'll think about that.

[Quinn Culver]

Cwould (←intentional portmanteau) someone please recommend an example of a structure definition that might be useful for me to learn how to go about this the correct way? :thanks:

[Eric Wieser]

def the_div_ring : Type* := { x : P // is_between x a1 a2 }

[Quinn Culver]

Does that mean a structure isn't appropriate here?

[Eric Wieser]

I think it's overkill

[Eric Wieser]

The code above uses docs#subtype which is a structure that already exists

[Kevin Buzzard]

A division ring is a structure on a type (the "underlying set") so you need to first make the type and then make the division ring structure on top

[Quinn Culver]

(deleted)

[Quinn Culver]

(deleted)

[Quinn Culver]

The subtype example, def the_div_ring : Type* := { x : P // is_between x a1 a2 } above refers to a1 and a2. How to do this properly? Here a1 and a2 are points that are i) not equal and ii) two of a set of four points no three of which are colinear that I'm using as my alternative configuration axiom. I've already proven that mathlib's configuration axiom,exists_config, implies this alternative one.

My only idea is to use variables and constants as below, but that feels wrong.

variables a₁ a₂ c₁₃ c₂₃ : P
constant axiom3_alt : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃
constant ha₁a₂ : a₁ ≠ a₂

def the_div_ring : Type* := { x : P // (x ∈ mk_line ha₁a₂) ∧ x ≠ a₂}

[Eric Wieser]

You definitely do not want to use constants here

[Eric Wieser]

I was assuming you would keep your existing structure, or something similar to it:

/-- A choice of four points in a desarguesian plane, which define a division ring -/
structure proj_plane_div_config [is_desarguesian P L] :=
(a₁ a₂ c₁₃ c₂₃ : P)
(hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃)

def the_div_ring (c : proj_plane_div_config P L) : Type* := { x : P // is_between x c.a₁ c.a₂ }

-- optional; this lets you write `x : c` instead of `x : c.the_div_ring`
instance : has_coe_to_sort (proj_plane_div_config P L) := { coe_sort := the_div_ring }

(untested, but should be easy to make that work after fiddling with implicit / explicit arguments)

[Eric Wieser]

Note that this:

variables a₁ a₂ c₁₃ c₂₃ : P
constant axiom3_alt : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃

says "any four points have no three collinear", which I assume is false. This is one reason to avoid constant and axiom; it is very easy to add a false axiom by accident, especially if you're new to Lean.

[Quinn Culver]

I thought that since you said a structure is overkill, your suggestion was intended to supplant it, @Eric Wieser . What would you recommend be used instead of structure here?

[Eric Wieser]

structure is overkill for the_div_ring (that's what I intepreted "here" as in your question)

[Eric Wieser]

The thing I was implying you should not write is

structure the_div_ring (c : proj_plane_div_config P L) : Type* :=
(val : P)
(property : is_between x c.a₁ c.a₂)

[Eric Wieser]

Quinn Culver said:

My only idea is to use variables and constants as below, but that feels wrong.

variables a₁ a₂ c₁₃ c₂₃ : P
constant axiom3_alt : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃
constant ha₁a₂ : a₁ ≠ a₂

def the_div_ring : Type* := { x : P // (x ∈ mk_line ha₁a₂) ∧ x ≠ a₂}

Just to be clear, this approach would be fine if you used variables intead of constant; but you'd have to write x : the_div_ring a₁ a₂ c₁₃ c₂₃ axiom3_alt ha₁a₂ instead of x : the_div_ring c or x : coe_sort c. structure lets you take a bunch of variables and combine them into a single variable.

[Quinn Culver]

My god, people in this forum are so helpful. Thanks!

[Quinn Culver]

Following the suggestion above, I have

structure proj_plane_div_config [is_desarguesian P L] :=
(a₁ a₂ c₁₃ c₂₃ : P)
(ha₁a₂ : a₁ ≠ a₂)
(hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃)


def the_div_ring (c : proj_plane_div_config P L) : Type* := {x : P //  x ∈ (mk_line c.ha₁a₂)}

right now the is_desarguesian is throwing the an 'unknown identifier' error, even though it's in a file, basic.lean, that is imported.

The mk_lineis throwing an error too, saying that Lean doesn't know how to synthesize placeholder.

[Kevin Buzzard]

Maybe some spelling mistake? Can you post a #mwe ? (perhaps append the copy of one file to another?)

[Kevin Buzzard]

This is not going to be some deep problem, it's far more likely to be a typo.

[Quinn Culver]

You were right about a typo, is_desarguesian needed to be configuration.is_desarguesian. Fixed, thanks!

Now the proj_plane_div_config in def the_div_ring (c : proj_plane_div_config P L) : Type* := {x : P // x ∈ (mk_line c.ha₁a₂)} is throwing a 'failed to synthesize typeclass instance' error. The mk_line is still throwing an error too, but first things first; once the previous sentence's error is dealt with that error might go away.

Here's my attempt at a MWE.

import combinatorics.configuration

open configuration.has_lines
open configuration.has_points
open configuration.nondegenerate
open classical
open set

universe u

variables {P L : Type u} [has_mem P L] [configuration.has_lines P L] [configuration.has_points P L] [nontrivial P] [nontrivial L]

variables (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 configuration.is_desarguesian : Prop :=
∀ T₁ T₂ : triangle P L, centrally_perspective T₁ T₂ ↔ axially_perspective T₁ T₂

variables {P}
def four_points_no_three_collinear (p₀ p₁ p₂ p₃ : P) : Prop := ¬ collinear L p₀ p₁ p₂ ∧ ¬ collinear L p₀ p₁ p₃ ∧ ¬ collinear L p₀ p₂ p₃ ∧ ¬ collinear L p₁ p₂ p₃

/-- A choice of four points in a desarguesian plane, which define a division ring -/
structure proj_plane_div_config [configuration.is_desarguesian P L] :=
(a₁ a₂ c₁₃ c₂₃ : P)
(ha₁a₂ : a₁ ≠ a₂)
(hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃)


def the_div_ring (c : proj_plane_div_config P L) : Type* := {x : P //  x ∈ (mk_line c.ha₁a₂)}

[Thomas Browning]

Here you go:

variables (P L)
@[class] def configuration.is_desarguesian : Prop :=
∀ T₁ T₂ : triangle P L, centrally_perspective T₁ T₂ ↔ axially_perspective T₁ T₂

variables {P}
def four_points_no_three_collinear (p₀ p₁ p₂ p₃ : P) : Prop := ¬ collinear L p₀ p₁ p₂ ∧ ¬ collinear L p₀ p₁ p₃ ∧ ¬ collinear L p₀ p₂ p₃ ∧ ¬ collinear L p₁ p₂ p₃

variables (P L)
/-- A choice of four points in a desarguesian plane, which define a division ring -/
structure proj_plane_div_config [configuration.is_desarguesian P L] :=
(a₁ a₂ c₁₃ c₂₃ : P)
(ha₁a₂ : a₁ ≠ a₂)
(hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃)


def the_div_ring [configuration.is_desarguesian P L] (c : proj_plane_div_config P L) : Type* := {x : P //  x ∈ (mk_line c.ha₁a₂ : L)}

[Thomas Browning]

You need @[class] to be able to use the square bracket instance notation.
You need variables (P L) to make both P and L explicit for proj_plane_div_config P L.
You need to add [configuration.is_desarguesian P L] to the_div_ring because it's needed for proj_plane_div_config.
You need to write (mk_line c.ha₁a₂ : L) because L cannot be inferred.

[Thomas Browning]

But really there's no reason to make proj_plane_div_config require [configuration.is_desarguesian P L], right?

[Quinn Culver]

I'm unclear on how & where to define the division ring operations (which are rather complicated). I guess I need to define their types as data in the structure, like

structure proj_plane_div_config :=
(a₁ a₂ c₁₃ c₂₃ : P)
(ha₁a₂ : a₁ ≠ a₂) --TODO: figure out how to remove this since hnoncol below implies it. mk_line should get the proof from hnoncol
(hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃)
(addition : P → P → P)  --IS THIS CORRECT?

Then, once the carrier set is defined as

def the_div_ring (c : proj_plane_div_config P L) : Type* := {x : P //  x ∈ (mk_line c.ha₁a₂ : L) ∧ x ≠ c.a₂}

How and where do I define the addition of elements on that carrier set? I tried def addition (r s : the_div_ring) : the_div_ring := r, (which I intended to mean r+s = r, just as a test) but that didn't work. Thoughts?

[Eric Wieser]

You at some point need to say

def my_config : proj_plane_div_ring P L :=
{ a₁ := sorry,
  addition := sorry }
-- lean will ask you to add the other fields too

What's the maths here? Is the addition derived solely from the relation between P and L, or is the idea that it is already the natural one on P?

[Reid Barton]

Quinn Culver said:

I tried def addition (r s : the_div_ring) : the_div_ring := r, (which I intended to mean r+s = r, just as a test) but that didn't work. Thoughts?

In what sense did it not work? Was there an error?
You probably need to give c (the proj_plane_div_config P L) as an argument to the_div_ring.

[Reid Barton]

Quinn Culver said:

I'm unclear on how & where to define the division ring operations (which are rather complicated). I guess I need to define their types as data in the structure, like

structure proj_plane_div_config :=
(a₁ a₂ c₁₃ c₂₃ : P)
(ha₁a₂ : a₁ ≠ a₂) --TODO: figure out how to remove this since hnoncol below implies it. mk_line should get the proof from hnoncol
(hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃)
(addition : P → P → P)  --IS THIS CORRECT?

No, you shouldn't try to put addition here.

[Quinn Culver]

@Eric Wieser Given four points, a₁ a₂ c₁₃ c₂₃, no three of which are colinear, addition of two points, r and s, on the line connecting a₁ and a₂ is

$$r + s = [[(r \vee c_{13}) \wedge (a_2 \vee a_3)] \vee ([(s \vee a_3) \wedge (a_2 \vee c_{13})]] \wedge (a_1 \vee a_2),$$

where the join of two points is their line and the meet of two lines is their point.

[Eric Wieser]

Great, then you definitely do not want to be adding to proj_plane_div_config

[Quinn Culver]

So I guess after defining the structure and then the carrier set, the operations come separately?

[Quinn Culver]

@Reid Barton How would you go about it?

[Reid Barton]

I think what you had above was good

[Notification Bot]

35 messages were moved here from #general > Structure defined for Desarguesian proj plane by Eric Wieser.

[Eric Wieser]

Apologies for the has_coe_to_sort notational distraction, I've moved that all to a new thread

[Eric Wieser]

Reid Barton said:

Quinn Culver said:

I tried def addition (r s : the_div_ring) : the_div_ring := r, (which I intended to mean r+s = r, just as a test) but that didn't work. Thoughts?

In what sense did it not work? Was there an error?
You probably need to give c (the proj_plane_div_config P L) as an argument to the_div_ring.

I don't think you ever answered this question @Quinn Culver

[Quinn Culver]

I think I got it to work; at least there're no errors: def addition (c : proj_plane_div_config P L) (r s : the_div_ring P L c) : the_div_ring P L c:= r

[Quinn Culver]

should I be using a namespace? namespace proj_plane_div_config?

[Eric Wieser]

I would skip the def entirely and just write a has_add instance

[Eric Wieser]

instance (c : proj_plane_div_config P L) : has_add (the_div_ring P L c) :=
{ add := λ r s, sorry }

[Eric Wieser]

Also you should change the argument explicitness on the_div_ring so that P and L are implicit, as they're obvious from c; then you can write c.the_div_ring instead of the_div_ring P L c

[Quinn Culver]

(deleted)

[Eric Wieser]

I recommend you write

structure proj_plane_div_config :=
(a₁ a₂ c₁₃ c₂₃ : P)
(hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃)

lemma proj_plane_div_config.ha₁a₂ (c : proj_plane_div_config  P L) : c.a₁ ≠ c.a₂ := sorry

so that you don't have to prove it inline

[Quinn Culver]

Just did that!

[Quinn Culver]

But now...

[Quinn Culver]

The ∈ is displaying the error

35:75: invalid type ascription, term has type
  Prop : Type
but is expected to have type
  L : Type u

Here's the code:

/-- A choice of four points in a desarguesian plane, which define a division ring -/
structure proj_plane_div_config :=
(a₁ a₂ c₁₃ c₂₃ : P)
(hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃)

namespace proj_plane_div_config

variables {P L}
lemma neq_a₁a₂ (c: proj_plane_div_config P L): c.a₁ ≠ c.a₂ := sorry


def the_div_ring (c : proj_plane_div_config P L) : Type* := {x : P //  (x ∈ mk_line (neq_a₁a₂ c) : L) ∧ x ≠ c.a₂}

[Eric Wieser]

That comma is illegal after the sorry

[Quinn Culver]

Corrected that, thanks.

[Eric Wieser]

And (x ∈ mk_line (neq_a₁a₂ c) : L) means ((x ∈ mk_line (neq_a₁a₂ c)) : L), you meant x ∈ (mk_line (neq_a₁a₂ c) : L).

[Quinn Culver]

Nice! That worked. Thanks again.

[Quinn Culver]

Why did you suggest putting proj_plane_div_config. at the beginning of the lemma's name?

[Quinn Culver]

Wait I guess it's so I can just write c.neq_a₁a₂. Is that the reason?

[Eric Wieser]

Quinn Culver said:

Why did you suggest putting proj_plane_div_config. at the beginning of the lemma's name?

It does the same thing as the namespace command that I didn't know you had

[Eric Wieser]

So yes, you can write it as x ∈ (mk_line c.neq_a₁a₂ : L) too

[Quinn Culver]

For notational convenience, I'm considering defining the meet and join of points and lines as in ftpg.pdf. Any reason this is unwise? For example might it be more work than it's worth?

That way instead of always invokingmk_line I can just use the meet symbol.

[Eric Wieser]

If you do that you'll need to define meet a b as something like if h : a \ne b then mk_line h else classical.choice sorry

[Reid Barton]

If you define it on flats as described in those notes then it is always defined and well-behaved, and I expect it would save a large amount of case analysis.

[Quinn Culver]

I'm unsure how to even start implementing the meet & join. I'd need to add a 0 and 1 element (\emptyset and the whole plane, I think). Any advice?

[Reid Barton]

I would make an inductive type with 4 constructors

[Quinn Culver]

Is an inductive type more appropriate than a structure here? Is that because there's no single carrier set?

Are the 4 constructors you had in mind, @Reid Barton, 1. the minimum (zero), 2. the maximum (one), 3. the points, and 4. the lines? If so, why not also include constructors for the meet & join? Is it better to define those separately?

[Eric Wieser]

You should define those separately

[Eric Wieser]

If you include them, then meet zero zero = zero is false

[Quinn Culver]

(deleted)