Similarities

Stream: Is there code for X?

[Yaël Dillies]

@Jovan Gerbscheid wrote a Python program which can solve moderately easy Euclidean geometry problems. I'm looking into what it would take to port it to Lean and the main blocking point is of course the scarcity of Euclidean geometry results in mathlib.

[Yaël Dillies]

We're thinking of first tackling triangle similarities. So I'm wondering whether we have the type of similarities (ratio-preserving maps) and the type of oriented similarities (oriented angle-preserving maps).

[Bryan Gin-ge Chen]

@Joseph Myers is probably the most well-informed on the current state of Euclidean geometry in mathlib and might also have some comments on the best way forward.

[Yaël Dillies]

Ahah! I was about to send "cc Joseph Myers"

[Joseph Myers]

See a recent discussion. Pretty much everything about isometries in mathlib should generalise in some way to similarities (with the definition making sense in general metric spaces or indeed pseudo_emetric_spaces; note that as in that discussion, many results for congruent or similar triangles should actually be stated for arbitrary indexed families of points, not for the special case of triangles), and a good starting point is probably applying the hom refactor to isometries so that lemmas that are true for all kinds of types for bundled similarities can then be stated for a single type class rather than separately for at least five types of bundled isometries and a corresponding five new types of bundled similarities. (Or more types if you also add types restricted to be orientation-preserving.)

One large group of trivial lemmas that we don't have is lemmas to transport various geometrical definitions across isometries / similarities. Pretty much every geometrical definition we have should transport across isometries and many also across similarities with appropriate scaling if the definition involves distance in some way.

Another fact I don't think we have is that a (not necessarily surjective) isometry of Euclidean spaces is an affine map (I did that some time ago outside of mathlib in the Euclidean context, but the appropriate form to add for mathlib would be stated for strictly convex spaces, which were added more recently).

[Yaël Dillies]

Ahah, I was trying to not get into refactoring isometries, but I guess the time has come. Can you explain me the naming convention around docs#isometric and docs#isometry? I would have swapped both names (or maybe renamed isometry to is_isometry).

[Joseph Myers]

isometric should be isometry_equiv to be consistent with linear_isometry_equiv and affine_isometry_equiv, unless there some other naming convention involved that I'm missing. We don't currently have a bundled type for not-necessarily-bijective isometries without additional properties such as linearity (but renaming isometry to is_isometry seems reasonable with or without adding such a bundled type).

[Hanting Zhang]

I will be trying to work on this soon as well. As I also asked in the other discussion, what exactly does "applying the hom refactor to isometries" mean? :sweat_smile:

[Yaël Dillies]

Isometries survived both refactors so far, so I'm gonna change them to follow the latest design

[Yaël Dillies]

Oh that's technical. Originally, we had unbundled hom predicates/classes: "f is a function and f distributes over multiplication". Then we switched to bundled homs: "f is a group homomorphism". And now we added on top hom classes: "ring_hom is a type of group homomorphisms".

[Hanting Zhang]

Ah ok, I was aware of the bundled homs but not the top hom classes, thanks

[Hanting Zhang]

If you don't mind explaining, what led to these changes? (Or just link some relevant discussion lol.) Was it just to get rid of the duplicate code had to be rewritten every time a new hom-class was added? Were there downsides to this?

[Hanting Zhang]

Also, how soon do you plan on working on these refactors? Would you mind if I helped out? I don't really know what your plan would be though but I'd love to hear what you wanna do

[Yaël Dillies]

It's a matter of days now. I need to find some time in between my revisions.

[Anne Baanen]

Hanting Zhang said:

If you don't mind explaining, what led to these changes? (Or just link some relevant discussion lol.) Was it just to get rid of the duplicate code had to be rewritten every time a new hom-class was added? Were there downsides to this?

Here's the thread where we developed the morphism class pattern.

The point is indeed that each time you introduce a new, more specialized, type of morphisms (like ring_hom specializes monoid_hom), you need to copy over a huge amount of code: everything about monoid_hom is still true about ring_hom. Moreover, whenever you add a declaration involving monoid_homs, you also need to duplicate it to ring_homs. So with this setup you get a kind of multiplicative explosion of code. And it's quite possible you forget to copy new lemmas over, so the next time someone wants to use your results they have to go back and copy it over (as happened often in mathlib).

In the morphism class refactor, we decided that instead of taking a parameter f : M →* N of a fixed type monoid_hom, instead the type of f should be an arbitrary F as long as all elements of F are (also) monoid homomorphisms, expressed as monoid_hom_class F M N.

If you want the full gory details, check out section 6 of my paper on the class-based patterns in mathlib.

[Hanting Zhang]

Oh! Thanks, the paper is wonderful btw. I always wondered how exactly typeclasses worked and could never understand any of the technical stuff, but your paper explained most everything very well

[Hanting Zhang]

@Anne Baanen At the end of section 6 you say that "work is still ongoing to provide a suitable generic form of standard operations such as composition and identity maps," which is interesting because I was wondering why we still had all the *_hom.id and *_hom.comp (and actualy a lot of *_hom.map_add?) lemmas sitting around. How do you think this will be done?

[Hanting Zhang]

I've started trying to refactor topology.metric_space.isometry. I'm working with the definitions below and the entire file actually ports very easily with minimal changes. @Yaël Dillies what do you think? I'm just wondering if you mind me just get started with the refactor now

import topology.metric_space.antilipschitz
import data.fun_like.basic

noncomputable theory

open function set
open_locale topological_space ennreal

section setup
variables (α : Type*) (β : Type*) [pseudo_emetric_space α] [pseudo_emetric_space β]

/-- An isometry (also known as isometric embedding) is a map preserving the edistance
between pseudoemetric spaces, or equivalently the distance between pseudometric space.  -/
structure isometry :=
(to_fun : α → β)
(edist_eq' : ∀ x y : α, edist (to_fun x) (to_fun y) = edist x y)

class isometry_class (F : Type*) (α β : out_param $ Type*)
  [pseudo_emetric_space α] [pseudo_emetric_space β] extends fun_like F α (λ _, β) :=
(edist_eq'  : ∀ (f : F) (x y : α), edist (f x) (f y) = edist x y)

instance isometry.to_isometry_class :
  isometry_class (isometry α β) α β :=
{ coe := isometry.to_fun,
  coe_injective' := λ f g h, by { cases f, cases g, congr' },
  edist_eq' := λ f, isometry.edist_eq' f }

instance : has_coe_to_fun (isometry α β) (λ _, α → β) := fun_like.has_coe_to_fun

@[simp] lemma to_fun_eq_coe {f : isometry α β} : f.to_fun = (f : α → β) := rfl

@[ext] theorem ext {f g : isometry α β} (h : ∀ x, f x = g x) : f = g := fun_like.ext f g h

/-- Copy of a `isometry` with a new `to_fun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : isometry α β) (f' : α → β) (h : f' = ⇑f) : isometry α β :=
{ to_fun := f',
  edist_eq' := h.symm ▸ f.edist_eq' }

end setup

[Yaël Dillies]

It's a bit of a dirty and technical job which I know perfectly how to do so I would suggest not bothering with that, but you do you :shrug:

[Hanting Zhang]

One annoying thing is that I seem to have to manually insert f : α → β to get lean to coerce from f : F. Did I setup something wrong with the fun_like things?

variables [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ]
variables [isometry_class F α β] [isometry_class G β γ]
variables (f : F) (g : G) {x y z : α}  {s : set α}

lemma lipschitz : lipschitz_with 1 (f : α → β) :=
lipschitz_with.of_edist_le $ λ x y, le_of_eq (isometry_class.edist_eq' f x y)

[Hanting Zhang]

Hm ok, I'll leave it to you then!

[Anne Baanen]

Hanting Zhang said:

Anne Baanen At the end of section 6 you say that "work is still ongoing to provide a suitable generic form of standard operations such as composition and identity maps," which is interesting because I was wondering why we still had all the *_hom.id and *_hom.comp (and actualy a lot of *_hom.map_add?) lemmas sitting around. How do you think this will be done?

I actually experimented with a couple of approaches for id and comp (and symm for isomorphisms), but found none completely convincing yet:

• Introduce a typeclass of the form has_id (F : Type*) (A : out_param Type*) [fun_like F A A] saying there is a map (has_id.id : F) which coerces to the identity: ((has_id.id : F) : A → A) = id. Similarly for has_comp (F G : Type*) (H A B C : out_param Type*) [fun_like F B C] [fun_like G A B] [fun_like H A C]. Main drawback is that the typeclass system really isn't robust against so many (out) parameters, so I ended up writing a lot of type ascriptions.
• Define a type of bundled identity/composition/inverse maps, which are structured basically the same as has_id/has_comp/has_symm but you use them as explicit parameters: (compFGH : comp_like F G H A B C) instead of [has_comp F G H A B C]. The drawback here is that have to explicitly distinguish all these different maps, and you can't make theorems like comp f (symm f) = id into simp lemmas since id is a free parameter now.
• Use definitions from the category theory library. Main drawback is that this usually requires putting everything into the same universe level.

I believe with some improvements to the typeclass system, something like the first approach could work out reasonably well, at the expense of putting even more stress onto that part of the system.

[Anne Baanen]

The remaining duplicates like *_hom.map_add are deprecated and should be removed now that morphism classes are stable, it just takes a lot of work to clean up all occurrences. I would appreciate any help! :D

[Hanting Zhang]

Oh, that is nice to know. :upside_down: I may attempt to at some point, indeed!

[Hanting Zhang]

Yaël Dillies said:

It's a bit of a dirty and technical job which I know perfectly how to do so I would suggest not bothering with that, but you do you :shrug:

I ended up starting similarities in #14315, I hope you don't mind :sweat_smile:

[Yaël Dillies]

Hmm, I would have bundled r in the structure.

[Eric Wieser]

Usually the pattern is to have both versions of the bundling; I guess it depends which one is useful

[Hanting Zhang]

I see! I'm probably not the right person to decide which one it should be, so it's helpful to know what everyone thinks

[Hanting Zhang]

I was looking for any precedence with this kind of parameterized types but couldn't really find anything like this specifically. I just went unbundled to match the lipschitz_with K f pattern

[Yaël Dillies]

The big difference is that docs#lipschitz_with is a predicate, not a bundled hom.

[Hanting Zhang]

Yeah, so the analogy is probably very flawed

[Yaël Dillies]

Your current design can't work because r will typically not be uniquely inferrable from α and β.

[Eric Wieser]

I guess the other question is whether we actually want to be bundling f here when things like lipshitz_with are not bundled

[Hanting Zhang]

Ok now I am thinking about it more and unbundling does mean you had to carry around r everywhere you go

[Hanting Zhang]

I'll try to see how it goes if I bundle everything

[Hanting Zhang]

I've pushed the changes.