Circularity of betweenness in R^2

Stream: Is there code for X?

[Mario Carneiro]

What's the general version of this statement, and do we have it in mathlib?

import Mathlib.Tactic
import Mathlib.Data.Matrix.Basic
import Mathlib.Algebra.Algebra.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2

abbrev Point := EuclideanSpace ℝ (Fin 2)
def det (p q r : Point) : ℝ :=
  p 0 * q 1 + q 0 * r 1 + r 0 * p 1 - p 1 * q 0 - q 1 * r 0 - r 1 * p 0

-- alternative definition of det:
lemma det_eq_matrixDet (a b c : Point) :
  det a b c = Matrix.det !![a 0, b 0, c 0; a 1, b 1, c 1; 1, 1, 1] := sorry -- already proved

example : det p q r = 0 → p ∈ segment ℝ q r ∨ q ∈ segment ℝ p r ∨ r ∈ segment ℝ p q := sorry

A related missing theorem is that det p q r != 0 iff affineSpan ℝ {p, q, r} = ⊤.

[Yaël Dillies]

The way to get to this result is to show that det a b c = 0 implies Collinear ℝ {a, b, c}. Then apply docs#Collinear.wbtw_or_wbtw_or_wbtw and docs#mem_segment_iff_wbtw

[Yaël Dillies]

You should be able to do that first det a b c = 0 → Collinear ℝ {a, b, c} step by directly manipulating the linear equation obtained from Matrix.det !![a 0, b 0, c 0; a 1, b 1, c 1; 1, 1, 1] = 0, but I'm not completely sure...

[Mario Carneiro]

Aha, I see that Collinear is defined in terms of matrix ranks, any idea how to connect det to a useful matrix determinant?

[Mario Carneiro]

the issue with the Matrix.det equation I have here is that the matrix itself isn't connected to anything mathlib-wise

[Yaël Dillies]

There is docs#LinearMap.range_lt_top_of_det_eq_zero which seems to go in the right direction, but I don't really know anything about matrix determinants in mathlib

[Yaël Dillies]

It seems this is the only lemma linking rank and determinant, actually

[Riccardo Brasca]

I think that from a theoretic point of view we have everything (for linear maps maybe), but you surely need some glue to connect to your definition.

[Mario Carneiro]

certainly, I'm just not sure what kind of statement is closest to what mathlib wants in this case (e.g. what would be the natural n-dimensional generalization)

[Riccardo Brasca]

Maybe something related to the dimension of the span?

[Mario Carneiro]

I think that's basically what Collinear gets you

[Mario Carneiro]

I think if it was a linear span we would be able to connect it to determinants of linear maps, but for affine spaces I don't see as many useful things

[Riccardo Brasca]

Ah, for affine spaces I don't know.

[Mario Carneiro]

I don't think we have a matrix constructor that has the 1's at the bottom like this one

[Yaël Dillies]

No I haven't seen that anywhere indeed

[Eric Wieser]

There's a more general statement we're missing here: that under suitable assumptions, an alternating map is zero only when its arguments are linearly dependent (we only have the reverse statement)

[Mario Carneiro]

Here's the proof I ended up with:

@[ext] theorem Point.ext {p q : Point} : p 0 = q 0 → p 1 = q 1 → p = q := by
  intros; ext i
  match i with | ⟨0, _⟩ | ⟨1, _⟩ => assumption

open scoped Matrix
theorem dotProduct_self_eq_zero {p : Point} : p ⬝ᵥ p = 0 ↔ p = 0 := by
  refine ⟨fun h => ?_, fun h => h ▸ by simp⟩
  simp at h
  have := (add_eq_zero_iff' (mul_self_nonneg _) (mul_self_nonneg _)).1 h
  simp [mul_self_eq_zero] at this
  ext <;> simp [this]

theorem collinear_iff : det p q r = 0 ↔ _root_.Collinear ℝ {p, q, r} := by
  constructor <;> intro H
  · if h : q = r then subst r; simp [collinear_pair] else
    apply collinear_insert_of_mem_affineSpan_pair
    have : (r - q) ⬝ᵥ (r - q) ≠ 0 := mt dotProduct_self_eq_zero.1 <| sub_ne_zero.2 <| Ne.symm h
    convert AffineMap.lineMap_mem_affineSpan_pair (k := ℝ)
      ((r - q) ⬝ᵥ (p - q) / (r - q) ⬝ᵥ (r - q)) _ _ using 1
    simp only [AffineMap.lineMap_apply_module']; rw [det] at H
    rw [← sub_eq_iff_eq_add, ← sub_eq_zero, ← smul_eq_zero_iff_right this,
      smul_sub, smul_smul, mul_div_cancel' _ this]
    ext <;> simp [norm_sq_eq_inner]
    · linear_combination H * (q 1 - r 1)
    · linear_combination H * (r 0 - q 0)
  · let ⟨v, H⟩ := (collinear_iff_of_mem (p₀ := p) (by simp)).1 H
    simp at H; obtain ⟨⟨a, rfl⟩, b, rfl⟩ := H
    simp [det]; ring

example : det p q r = 0 →
    p ∈ segment ℝ q r ∨ q ∈ segment ℝ p r ∨ r ∈ segment ℝ p q := by
  intro h; rw [collinear_iff] at h
  obtain h | h | h := h.wbtw_or_wbtw_or_wbtw
  · right; left; exact mem_segment_iff_wbtw.2 h
  · right; right; exact mem_segment_iff_wbtw.2 h.symm
  · left; exact mem_segment_iff_wbtw.2 h.symm

[Mario Carneiro]

I was surprised to find that ‖p‖^2 was more difficult to use in this proof than p ⬝ᵥ p; I can prove the former is nonzero but there is no simp lemma that works out what it is in terms of coordinates in this case

[Mario Carneiro]

proving the latter is nonzero required filling a hole in the library

[Patrick Massot]

I find it strange to use a three dimensional determinant here. Why not use the 2d one? Is it for symmetry reasons?

[Eric Wieser]

p ⬝ᵥ p is not well-typed for EuclideanSpace ℝ (Fin 2), you should be inserting some withLp.equivs

[Eric Wieser]

(this is how docs#EuclideanSpace.inner_eq_star_dotProduct is stated)

[Mario Carneiro]

Patrick Massot said:

I find it strange to use a three dimensional determinant here. Why not use the 2d one? Is it for symmetry reasons?

As far as I know this is the only way to write that as a determinant. It's a 3D determinant because affine transformations in 2D are represented using linear transformations in 3D where the z coordinate is fixed to 1

[Mario Carneiro]

I suppose you could use cofactor expansion on the last row to turn it into 3 2D determinants but that's hardly better

[Mario Carneiro]

Eric Wieser said:

p ⬝ᵥ p is not well-typed for EuclideanSpace ℝ (Fin 2), you should be inserting some withLp.equivs

That's weird, it works for me although I am on a slightly old mathlib e64d0a16

[Eric Wieser]

By "not well-typed" I mean "that's defeq abuse" not "Lean rejects it"

[Mario Carneiro]

sure, but I don't see that helping anything here

[Mario Carneiro]

this isn't mathlib code anyway

[Eric Wieser]

I guess my main point is that it guarantees that there will be no lemmas that exist about it, in the same way that things go wrong if you end up with s x in your goal when s is a set

[Mario Carneiro]

I agree if that were the case, but I don't think it is in this case

[Mario Carneiro]

there are actually just no relevant lemmas

[Mario Carneiro]

I also contest to some extent that this is/should be considered as defeq abuse. It is reasonable to want ![x, y] to be usable to construct elements of R^2

[Eric Wieser]

I think it's reasonable to want notation to exist, but it's unreasonable for it to be that notation (at least as currently implemented)

[Eric Wieser]

You're setting yourself up for a headache if you write norm ![x, y]

[Patrick Massot]

Mario Carneiro said:

Patrick Massot said:

I find it strange to use a three dimensional determinant here. Why not use the 2d one? Is it for symmetry reasons?

As far as I know this is the only way to write that as a determinant. It's a 3D determinant because affine transformations in 2D are represented using linear transformations in 3D where the z coordinate is fixed to 1

Given three points in an affine plane, the natural thing to do is not to artificially embed the affine plane into a 3d vector space. It to form two vectors using point subtraction. Your three points form an actual triangle if and only if the two vectors you get form a basis. Then you project this basis to the relevant quotient to get the triangle orientation. Of course if you have a favorite basis for the vector space then you can compute a determinant.

[Mario Carneiro]

@Eric Wieser well as mentioned above ‖p‖^2 was even less useful than p ⬝ᵥ p, even though it's the less abusive one

[Patrick Massot]

Sorry I have no idea what you are talking about.

[Mario Carneiro]

@Patrick Massot This isn't about embedding, I'd prefer it if the determinant was defined directly over R^2 affine maps. It's just that when you write it in terms of matrices that's what you get

[Mario Carneiro]

but yes, you can map this to two vectors and take a regular determinant there, if you break the symmetry

[Patrick Massot]

You are already breaking the symmetry by ordering the points.

[Mario Carneiro]

there are three ways to do that though and you need some symmetry property about swapping them

[Mario Carneiro]

with the matrix det definition it follows from column swaps in the matrix determinant

[Mario Carneiro]

if you subtract points the algebra is not very obvious and I would just expand everything and use ring to prove it

[Patrick Massot]

With the mathematically natural one it would follow from linearity of determinant.

[Mario Carneiro]

I don't know what you mean by that

[Mario Carneiro]

I take it you are talking about Matrix.det ![q - p, r - p] as the definition?

[Patrick Massot]

Yes.

[Mario Carneiro]

I don't see swapping p and q here being an easy proof given a reasonable library on linear and affine maps

[Eric Wieser]

Mario Carneiro said:

I agree if that were the case, but I don't think it is in this case

I note you rewrote docs#Matrix.dotProduct_self_eq_zero from scratch; maybe this (exact? being confused by the defeq) is why

[Mario Carneiro]

no, I wrote it from scratch because that theorem didn't exist when I looked

[Patrick Massot]

Then the proof you want relies on things like $p - q = p - r + r - q$ and multilinearity.

[Patrick Massot]

and antisymmetry of course, but no row expansion or other ugly computation.

[Mario Carneiro]

yes, I can see how to do it with elementary column operations, but that still looks a bit like an ugly computation

[Eric Wieser]

Mario Carneiro said:

no, I wrote it from scratch because that theorem didn't exist when I looked

(it came in in !3#18783 in April; I guess you're porting old lean3 code?)

[Patrick Massot]

det ![q - p, r - p] = det ![q - r + r - p, r - p] = det ![q - r, r - p] + det ![r - p, r - p] = det ![q - r, r - p]

[Mario Carneiro]

no, seems it wasn't imported

[Patrick Massot]

But it’s dinner time here so I need to go.

[Eric Wieser]

Note that in the same vein there will be exactly no lemmas about det ![x, ...] because that is also defeq abuse without a Matrix.of

[Mario Carneiro]

@Patrick Massot Are you saying that this is the right way to do affine points in n dimensions too? I really want that whole business to be a definition with general properties, not something in user code

[Eric Wieser]

Though probably there are no lemmas with the of either...

[Mario Carneiro]

sure, this needs some ofColumns or ofRows function

[Mario Carneiro]

I have to say, the many defeq variations here do not spark joy

[Eric Wieser]

Well, ofRows would be identical to of

[Mario Carneiro]

true

[Eric Wieser]

Mario Carneiro said:

I have to say, the many defeq variations here do not spark joy

Making Matrix and EuclideanSpace structures would maybe make this more predictable

[Mario Carneiro]

I don't think it would make things easier though, given how loosely connected they currently are in terms of lemmas

[Mario Carneiro]

What's the mathlib approved operation for taking the dot product of elements of R^2?

[Mario Carneiro]

I looked at innerProduct briefly but it has a weird type

[Eric Wieser]

It's surely inner

[Eric Wieser]

What's weird about the type?

[Mario Carneiro]

it's in some star ring and there are conjugations all over it

[Mario Carneiro]

maybe there is a scope I can open to say I'm in R^2 and don't bother me with complex numbers

[Eric Wieser]

Sure, but that's an implementation detail; just write ⟪x, y⟫_ℝ

[Eric Wieser]

There might be a scope that saves you from the _ℝ, or maybe it's even the default

[Mario Carneiro]

my proof looks like this now, although I think it's probably even more abusing defeq now:

import Mathlib.Tactic
import Mathlib.Data.Matrix.Basic
import Mathlib.Algebra.Algebra.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.LinearAlgebra.Matrix.DotProduct
import Mathlib.Analysis.Convex.Between

abbrev Point := EuclideanSpace ℝ (Fin 2)
def det (p q r : Point) : ℝ :=
  p 0 * q 1 + q 0 * r 1 + r 0 * p 1 - p 1 * q 0 - q 1 * r 0 - r 1 * p 0

-- alternative definition of det:
lemma det_eq_matrixDet' (a b c : Point) :
  det a b c = Matrix.det (Matrix.of ![b - a, c - a]) := sorry -- already proved

@[ext] theorem Point.ext {p q : Point} : p 0 = q 0 → p 1 = q 1 → p = q := by
  intros; ext i
  match i with | ⟨0, _⟩ | ⟨1, _⟩ => assumption

open scoped Matrix
theorem collinear_iff : det p q r = 0 ↔ _root_.Collinear ℝ {p, q, r} := by
  constructor <;> intro H
  · if h : q = r then subst r; simp [collinear_pair] else
    apply collinear_insert_of_mem_affineSpan_pair
    have : ⟪r - q, r - q⟫_ℝ ≠ 0 :=
      mt Matrix.dotProduct_self_eq_zero.1 <| sub_ne_zero.2 <| Ne.symm h
    convert AffineMap.lineMap_mem_affineSpan_pair (k := ℝ)
      (⟪r - q, p - q⟫_ℝ / ⟪r - q, r - q⟫_ℝ) _ _ using 1
    simp only [AffineMap.lineMap_apply_module']; rw [det] at H
    rw [← sub_eq_iff_eq_add, ← sub_eq_zero, ← smul_eq_zero_iff_right this,
      smul_sub, smul_smul, mul_div_cancel' _ this]
    ext <;> simp [norm_sq_eq_inner]
    · linear_combination H * (q 1 - r 1)
    · linear_combination H * (r 0 - q 0)
  · let ⟨v, H⟩ := (collinear_iff_of_mem (p₀ := p) (by simp)).1 H
    simp at H; obtain ⟨⟨a, rfl⟩, b, rfl⟩ := H
    simp [det]; ring

example : det p q r = 0 →
    p ∈ segment ℝ q r ∨ q ∈ segment ℝ p r ∨ r ∈ segment ℝ p q := by
  intro h; rw [collinear_iff] at h
  obtain h | h | h := h.wbtw_or_wbtw_or_wbtw
  · right; left; exact mem_segment_iff_wbtw.2 h
  · right; right; exact mem_segment_iff_wbtw.2 h.symm
  · left; exact mem_segment_iff_wbtw.2 h.symm

[Eric Wieser]

have : ⟪r - q, r - q⟫_ℝ ≠ 0 := inner_self_ne_zero.2 <| sub_ne_zero.2 <| Ne.symm h saves you a line

[Mario Carneiro]

and an import

[Eric Wieser]

Does this approach help at all?

theorem vectorSpan_insert (x : Point) (s : Set Point) :
  vectorSpan ℝ (insert x s) = Submodule.span ℝ ((· -ᵥ x) '' s) := sorry

open scoped Matrix
theorem collinear_iff : det p q r = 0 ↔ _root_.Collinear ℝ {p, q, r} := by
  rw [Collinear, vectorSpan_insert, Set.image_insert_eq, Set.image_singleton, vsub_eq_sub
    det_eq_matrixDet']
  sorry

[Mario Carneiro]

the main goal there looks a bit weird, it's asking for q - p = r - p?

[Mario Carneiro]

I think the hard part with this approach is proving LinearIndependent, there are also other routes that connect to AffineIndependent of the three points but I don't really see where to go from there

[Eric Wieser]

My mistake, edited

[Mario Carneiro]

actually maybe it's a bit better with LinearIndependent ℝ fun (x : ↑{q -ᵥ p, r -ᵥ p}) ↦ ↑x since it seems plausible that one can reduce this to invertibility of ![q - p, r - p] and thence to the determinant

[Eric Wieser]

Eric Wieser said:

There's a more general statement we're missing here: that under suitable assumptions, an alternating map is zero only when its arguments are linearly dependent (we only have the reverse statement)

I think we probably want this still

[Eric Wieser]

@Oliver Nash has asked for this in the past

[Mario Carneiro]

do we have the "alternating map" used in this theorem though? I couldn't find any form of it in mathlib, which is why it's defined in the MWE

[Eric Wieser]

rw [Matrix.det]

[Eric Wieser]

Then an alternating map appears

[Eric Wieser]

There's probably an API lemma somewhere

[Mario Carneiro]

Unfortunately I think det isn't an alternating map by that definition, because it's an affine multilinear (multiaffine?) map

[Eric Wieser]

Dumb rewrites get me to

Matrix.detRowAlternating ![q - p, r - p] = 0 ↔
      ¬∃ s, Cardinal.mk ↑s = 2 ∧ LinearIndependent (ι := { x // x ∈ s }) ℝ Subtype.val

[Mario Carneiro]

I think there are alternative lemmas that avoid the need to unfold the rank <= 1 stuff

[Eric Wieser]

Yeah, hence "dumb"

[Eric Wieser]

Though it exposed that we're missing (Order.succ (Nat.cast n) : Cardinal) = Nat.cast (n + 1)

[Eric Wieser]

(cc @Yaël Dillies)

[Mario Carneiro]

the part that I'm still not sure about in this route is how to connect LinearIndependent to either invertibility of a matrix or some kind of determinant

[Eric Wieser]

Since I didn't link it above, docs#AlternatingMap.map_linearDependent is the (easy) direction that we do have

[Richard Copley]

Eric Wieser said:

There's a more general statement we're missing here: that under suitable assumptions, an alternating map is zero only when its arguments are linearly dependent (we only have the reverse statement)

The assumptions need to rule out the extreme case of the zero map. It would be useful to have that ExteriorAlgebra.ιMulti R k w = 0 only if ¬LinearIndependent R w, since ιMulti is in some sense universal for alternating maps (on finite index types). (I hope I've got that right.) (Edit: ¬!)

[Patrick Massot]

Mario Carneiro said:

Patrick Massot Are you saying that this is the right way to do affine points in n dimensions too? I really want that whole business to be a definition with general properties, not something in user code

Sure, this is completely general. See docs#affineIndependent_iff_linearIndependent_vsub for instance.

[Mario Carneiro]

okay, but I want a notion of det here that does not choose a base point explicitly (it may do so internally as part of the definition)

[Mario Carneiro]

e.g. the LHS of that theorem

[Yaël Dillies]

Eric Wieser said:

Though it exposed that we're missing (Order.succ (Nat.cast n) : Cardinal) = Nat.cast (n + 1)

docs#Cardinal.nat_succ ?