Minkowski space and hyperbolic geometry

Stream: new members

[Matthias Goerner]

Hi, I am trying to prove some facts about computing distances between e.g. a line and a line in hyperbolic 3-space. I could not find anything about Minkowski space in mathlib, so I started this file and am stuck with some issues, in particular, since I don't really understand classes and instances well:
https://github.com/unhyperbolic/hyperbolicGeometryInLean/blob/main/Hyperbolic/hyp.lean
For example: What is the best way to implement normalized_time_like which returns a future unit time like vector? Do I make a subclass for such vectors and return the subclass? Or do I just return a vector and annotate in some other way that it is future and unit time like?

[Moritz Doll]

I am pretty sure that you don't need instances and classes in your example: a simple def IsLightlike (v : vector) := inner_product vec vec = 0 should suffice and then you can have a theorem Foo.isLightlike that starts with unfolding IsLightlike.

[Matthias Goerner]

I thought about just a simple IsLightLike... But I think if I want to state theorems later about points in the hyperboloid model, it might be annoying to write the theorems in the style "IsFutureUnitTimeLike(a) -> IsFutureUnitTimeLike(b) -> theThingIWantToSay". I think it might be more natural to express that using a type or structure or class. And I would like to express some hierarchy timeLike is more general then unitTimeLike, and so on.

[Matthias Goerner]

I guess my question isn't so much how do I get to work this, but what would be the proper "API design" for Minkowski space.

[Moritz Doll]

we have the concept of bundled objects, that is we have a structure that contains the vector and a proof that it is lightlike, something along the lines of

structure lightLikeVector where
  toVector : vector
  light_like : inner_product toVector toVector = 0

and then you could extend this structure to have future and past lightlike vectors. the downside is that you have to deal with coercions. We use both (bundled and unbundled) approaches in mathlib depending which one is less annoying to deal with. In your case I would think that unbundled might be better. you can always use sections and variable (vec_lightlike : IsLightlike v) so that you don't have to put all the assumptions in the theorem (in Lean 4 you can use all the variables in a theorem, which is a somewhat big change from Lean 3 and this makes unbundled structures more convenient than before)

[Matthias Goerner]

Thanks.

Is using subtypes a good idea here?
I tried

def point := { v : vector // isFutureUnitTimeLike v }
instance c : Coe point vector where
  coe p := p.val
noncomputable def distance (a b : Point) : ℝ  :=
    Real.arcosh (-(inner_product (↑a) (b.val)))

But I am getting: type mismatch

  a
has type
  Point : Sort ?u.73635
but is expected to have type
  vector : Type

and

invalid field notation, type is not of the form (C ...) where C is a constant
  b
has type
  Point

[Matthias Goerner]

Typo Point -> point.
I got it to work with "instance c : Coe point vector := ⟨ fun p => p.val ⟩" Is there a better way?

[Yaël Dillies]

No, that's what you're supposed to do. There are other options, like using reducible:

@[reducible] def point := {v : vector // isFutureUnitTimeLike v}

[Matthias Goerner]

Thanks that works.

[Matthias Goerner]

Another question: as far as I see, the way to say that something is a vector space is to say that it is a module over a field. What is the quickest way to give "Fin 4 -> Real" a vector space structure?
Right now I am doing

def vector := Fin 4 → ℝ
instance : Add vector := ⟨ fun a b => fun i => (a i) + (b i) ⟩
--  a bunch of more such stuff
def inner_product (a b : vector) : ℝ := -(a 0) * (b 0) + (a 1) * (b 1) + (a 2) * (b 2) + (a 3) * (b 3)

and proving things very manual. It would be great if I can approach it from a higher level and communicate that it is a vector space with a symmetric bilinear form. I saw EuclideanSpace - but that is using the wrong inner product.

[Patrick Massot]

def vector := Fin 4 → ℝ
deriving AddCommGroup

noncomputable instance : Module ℝ vector := by delta vector; infer_instance

probably does what you want.

[Matthias Goerner]

Thanks that worked for almost everything.

theorem aa (r : ℝ) (a : vector) : r * a = r * a := rfl

still gives

failed to synthesize instance
  HMul ℝ vector ?m.70817

[Matthias Goerner]

I see, it requires a different multiplication symbol. How do I type it in VS code?

[Alex J. Best]

\bu (or \bullet)

[Alex J. Best]

If you hover over a symbol it should tell you how to type it

[Matthias Goerner]

Thanks.

[Matthias Goerner]

I have a couple of more questions: I want to generalize to arbitrary dimension

def vector (n : ℕ) := (Fin n) → ℝ

works, but

def vector (n : ℕ) := (Fin n) → ℝ  deriving AddCommGroup

does not work. How do I fix it?

[Scott Morrison]

We don't have "delta" instances as we did in Lean 3, and it would require a bit of redesign that hasn't happened yet to allow it. See #380.

For now just write the instance directly, e.g.
instance : AddCommGroup (vector n) := inferInstanceAs <| AddCommGroup ((Fin n) → ℝ).

[Matthias Goerner]

Thanks!

[Matthias Goerner]

This is what I have:

def Sign := {r : ℝ // r = 1 ∨ r = -1}
instance : Coe Sign ℝ := ⟨ fun r => r.val ⟩

def PlusSign  : Sign := ⟨ 1, by left; rfl⟩
def MinusSign : Sign := ⟨-1, by right; rfl⟩

def PseudoEuclideanSpace {f : Type _} [Fintype f] (signature : f → Sign) := f → ℝ

instance : AddCommGroup (PseudoEuclideanSpace signature) := inferInstanceAs <| AddCommGroup (f → ℝ)

def MinkowskiSpaceSignature (n : ℕ) : Fin n → Sign :=
    fun i => if (↑i : ℕ) == 0 then MinusSign else PlusSign

def MinkowskiSpace (d : ℕ) := PseudoEuclideanSpace (MinkowskiSpaceSignature d)

[Matthias Goerner]

I ran into a problem at the line instance : AddCommGroup.

[Matthias Goerner]

Similarly, when I am trying to define the inner product on the PseudoEuclideanSpace with

instance : Inner ℝ (PseudoEuclideanSpace signature) :=
  ⟨fun v w => ∑ i, (v i) * (w i) * (signature i)⟩

[Matthias Goerner]

def PseudoEuclideanSpace (f : Type _) (k : Fintype f) (signature : f → Sign) := f → ℝ
instance : AddCommGroup (PseudoEuclideanSpace f k signature) := inferInstanceAs <| AddCommGroup (f → ℝ)

works, but I want f to be implicit {} and k to be from instance inference []. But then how do I change the next line?

[Matthias Goerner]

I think I figured it out:

instance : AddCommGroup (@PseudoEuclideanSpace f k signature) := inferInstanceAs <| AddCommGroup (f → ℝ)

[Eric Wieser]

Note that we have docs#SignType

[Eric Wieser]

Ah, I guess you don't want to allow 0

[Eric Wieser]

Making f {}-implicit doesn't make any sense here