Creating a map between structures

Stream: new members

[debord]

I have defined a structure Metric_Space as so:

structure Metric_Space (α : Type) (d : α → α → ℝ) :=
  (d_nonneg : ∀ A B : α, d A B ≥ 0)
  (a_eq_b_iff : ∀ A B : α, A = B ↔ d A B = 0)
  (symm : ∀ A B : α, d A B = d B A)
  (tri_ineq : ∀ A B C : α, d A C ≤ d A B + d B C)

and I want to be able to define a map between one Metric_Space and another and define if it is an isometry. My current idea is that a map between two Metric_Spaces would really just be a map between their associated type. So I have this:

variable {α : Type} {dx : α → α → ℝ} (X : Metric_Space α dx)
variable {β : Type} {dy : β → β → ℝ} (Y : Metric_Space β dy)

def Bijection (f : α → β) := ∃ g : β → α, ∀ A : α, ∀ B : β, g (f A) = A ∧ f (g B) = B

def Distance_Preserving (f : α → β) := ∀ A B : α, dy (f A) (f B) = dx A B

def Isometry (f : α → β) := Bijection f ∧ Distance_Preserving f

However, it seems that in my definition of Isometry, it gets confused about the usage of the distance functions in Distance_Preserving f and gives don't know how to synthesize implicit argument @Distance_Preserving α (?m.40962 X Y Isometry f) β (?m.40963 X Y Isometry f) f. What would be the correct way to achieve what I'm trying to do here? I've considered making another structure like Metric_Space_Map but I'm having a hard time thinking of what that would look like. Thanks for your time.

I had the idea to try to make Metric_Space a class instead, and directly give the definition of Distance_Preserving the typeclass declaration like:

def Distance_Preserving [Metric_Space α dx] [Metric_Space β dy] (f : α → β) := ∀ A B : α, dy (f A) (f B) = dx A B

but this similarly gives the error failed to synthesize instance Metric_Space α ?m.40798. It's definitely making me confused about this concept in the first place. I declare dx as α → α → ℝ as needed in the definition of Metric_Space, so why is it not able to recognize it when I use the definition again? What exactly does that error even mean?

EDIT: Probably, this is not a real problem. I have instead made everything explicitly defined rather than implicit and it seems to be working more according to how I expect it to work.

[Floris van Doorn]

Yeah, making things type-classes is probably the way to go.
Note that the mathlib definition of metric space also bundles the distance function dx and dy inside the metric space structure: docs4#MetricSpace