Degenerate configuration of points and lines

Stream: general

[Quinn Culver]

In mathlib, a nondegenerate configuration seems to allow for a single line and a single point not on the line (or any line). True? I'm worried that I'm missing something since that seems even more degenerate than what nondegenerate is meant to rule out. (I'm aware that the description says it's meant to "exclude certain degenerate configurations.")

[Notification Bot]

Quinn Culver has marked this topic as resolved.

[Notification Bot]

Quinn Culver has marked this topic as unresolved.

[Thomas Browning]

Oh good catch. I wrote that definition because it was enough for the theorems that I was planning on proving, and it never caused any problems. But I didn't realize that it allowed for that rather degenerate configuration. If it's causing problems then perhaps it should be changed.

[Quinn Culver]

Thanks, @Thomas Browning . I'm in the process of proving that for a nondegenerate configuration satisfying the first two projective plane axioms, the 3rd projective plane axiom is equivalent to there being 4 points no 3 of which are colinear, a commonly used and useful alternative axiom. To do so, I want to prove a lemma saying that if three points are non-colinear, then any two of them are not equal. But with this degenerate configuration possible, they could all be equal and non-colinear. Thoughts?

[Thomas Browning]

Would dropping the ≠ hypothesis from the first two projective plane axioms help?

[Quinn Culver]

Yeah that would do it. Thanks. Any idea when the change will be reflected in mathlib?

[Thomas Browning]

Well, someone would have to write a PR :D
You could (it could be a fun little contribution to mathlib), or I could when I have time

[Quinn Culver]

I'll try to do it. I've never made a pull request so this would a useful learning experience for me.

[Quinn Culver]

Why doesn't the projective_plane class extend has_points and has_lines? Seems like it ought to and then the ≠ should be dropped from those. Thoughts?

[Eric Wieser]

Note that for that to be valid you need set_option old_structure_cmd true, but that's a totally reasonable addition

[Thomas Browning]

I tried it out, but it caused problems with docs#configuration.projective_plane.configuration.dual.projective_plane

[Eric Wieser]

What were the problems?

[Thomas Browning]

When it sees

instance : projective_plane (dual L) (dual P) :=
{ mk_line := (definition), mk_line_ax := (proof), and so on }

it complains that projective_plane is not a structure.

invalid structure value {...}, expected type is known, but it is not a structure
  projective_plane (dual L) (dual P)

[Eric Wieser]

Can you push your attempt to a branch?

[Thomas Browning]

https://github.com/leanprover-community/mathlib/compare/config_old_structure_cmd

[Thomas Browning]

So I got it to work with ⟨ ⟩ notation, but it would be nice if there was a way to use { } notation.

[Quinn Culver]

Which use of ⟨ ⟩ are you referring to?

[Thomas Browning]

This use: ⟨_, @mk_line_ax P L _ _, _, @mk_point_ax P L _ _, by

[Quinn Culver]

Mind explaining or pointing me to an explanation of the difference? I've used ⟨ ⟩ but never { } (in that context).

[Mario Carneiro]

{ field1 := value, field2 := value2 } can be used to construct an element of a structure

[Mario Carneiro]

it's basically equivalent to ⟨value1, value2⟩

[Quinn Culver]

Is that explained anywhere in the docs?

[Mario Carneiro]

https://leanprover.github.io/lean4/doc/struct.html

[Quinn Culver]

Need I worry when consulting that manual (for other things) that it's for Lean 4 and I'm using Lean 3?

[Mario Carneiro]

meh, it's close enough

[Kevin Buzzard]

Does #tpil section 9 or so have anything? That's lean 3

[Quinn Culver]

Yes, it does. Section 9.2. It shows the use of { } but not ⟨ ⟩. Thanks.

[Quinn Culver]

So @Eric Wieser and @Thomas Browning, do you think there's hope that projective_plane will be made to extend has_points and has_lines?

[Quinn Culver]

Anything I can do to help?

[Thomas Browning]

#18436

[Thomas Browning]

@Quinn Culver It's merged.

[Quinn Culver]

Above it was suggested that the ≠ hypothesis be dropped from the first two projective plane axioms help. I'd like to do this (because I need it and to make a contribution to mathlib). Does doing so require dropping the ≠ and then going to all the pages that are "Imported by" combinatorics.configuration and refactoring so they work without the ≠? Anything else?

[Eric Wieser]

The way to make this type of change is usually:

• Make the change in the file(s) where it's obvious
• Make the PR, tag it "awaiting-CI"
• Let github's CI tell you what needs fixing downstream
• If it's in lots of places, wait for feedback on whether it's a good idea before spending too much time on fixing downstream things

[Quinn Culver]

@Thomas Browning why did you put the ≠ hypotheses in mk_point, mk_point_ax etc. in the first place?

[Thomas Browning]

Here's where I did it: #11065
Seems like I was arguing that the ≠ definition is more general, and more natural (there is a unique line through two distinct points but being forced to choose a line through each point is less natural)

[Thomas Browning]

Another option would be to add an extra condition to docs#configuration.nondegenerate

[Quinn Culver]

Why do you say "being forced"? Doesn't the definition allow (as opposed to force) one to get a line through a point if needed/desired?

[Reid Barton]

Someone had to make the projective plane in the first place

[Reid Barton]

Why do you want to remove the ≠ hypotheses?

[Quinn Culver]

Because it allows for the degenerate configuration of a single point and a single line not on it. I want a lemma that says that if two points are noncolinear, then they're not equal. As is, if the two points are actually the same, they could still be noncolinear.

[Reid Barton]

I think you could achieve this without adding "garbage" data to the structure, e.g., require that some point is on some line.

[Reid Barton]

Do you really want to say that a projective plane consists of (among other things) a choice of a line through each point?

[Quinn Culver]

I see your point now. Less is more! Any idea(s), then, for how to achieve that noncollinear points are not equal?

[Eric Wieser]

@Reid Barton, would you consider "every line has at least one point on it and at least one point off it" as garbage?

(exists_point : ∀ l : L, (∃ p : P, p ∉ l) ∧ (∃ p : P, p ∈ l))
(exists_line : ∀ p : P, (∃ l : L, p ∉ l) ∧ (∃ l : L, p ∈ l))

[Thomas Browning]

Eric's suggestion seems reasonable to me, although it would make things the definition slightly more clunky. Another option would be to just define colinear as "if p≠q then there is a line through p and q" which nicely matches the definition of docs#configuration.has_lines.

[Eric Wieser]

Agreed that it feels pretty clunky

[Reid Barton]

The language being used here is confusing me. In math if we talk about whether two points are collinear, we obviously aren't talking about the case where the "two points" are the same. Except whoops, we wouldn't be talking about whether "two points are collinear" in the first place because any two points are collinear.

The actual issue is: we want to know that every point is contained in some line. Right?

[Reid Barton]

would you consider "every line has at least one point on it and at least one point off it" as garbage?

Any proposition is non-garbage.

[Eric Wieser]

I assume we also want the converse, that every line has at least one point

[Quinn Culver]

Reid Barton said:

The language being used here is confusing me. In math if we talk about whether two points are collinear, we obviously aren't talking about the case where the "two points" are the same. Except whoops, we wouldn't be talking about whether "two points are collinear" in the first place because any two points are collinear.

The actual issue is: we want to know that every point is contained in some line. Right?

You're right. I actually meant to say that if three points are noncollinear, then no two of them are equal. Sorry about that.

[Thomas Browning]

@Quinn Culver You're assuming has_points and has_lines, right? So if you also assume [nontrivial P] and [nontrivial L] then you should be able to deduce that there is a point on each line and a line through each point. But it might be a good idea to change nondegenerate as Eric suggested.