Translation/rotation number for various maps

Stream: maths

[Yury G. Kudryashov]

Currently I use a local notation $\tau$ for docs#circle_deg1_lift.translation_number
In the future I'm going to need at least the following maps and their lifts to the real line:

• circle_homeo: an order-preserving homeomorphism of the circle $\mathbb R/\mathbb Z$;
• circle_diffeo: an order-preserving $C^r$-smooth diffeomorphism of the circle;
• circle_break_homeo: a circle homeomorphism which is smooth at all points but one, and has a given ratio of left/right derivatives at this point;
• circle_smooth_critical: a smooth homeomorphism of the circle with one (or finitely many) critical point(s).

In each case I'll need to talk about translation number of the lift and about the rotation number of the circle self-map. I have two questions:

• How can I avoid repeating all basic lemmas? Coercions? Typeclasses instead of structures? Something else?
• I need at least two symbols, one for the translation number and one for the rotation number. Any suggestions?

[Yury G. Kudryashov]

@Sebastien Gouezel :up:

[Sebastien Gouezel]

I think I would go for coercions. This could be painful if you had to rewrite along lemmas (because they would not syntactically be of the right form), but since you will mostly apply lemmas this should be fine.

You could even exercise your tactic skills if you have lemmas along which you want to rewrite. Assume you have a class foo, a coercion to functions, and a bunch of lemmas involving f x where f : foo, for instance foo.lemma1 and foo.lemma2. And then you define a class bar extending foo. Very often, one registers the function coercion for bar, a coercion from bar to foo, the fact that the composition of the coercions is the function coercion, and one restates the lemma for bar, in terms of the function coercion for bar. I feel a small tactic restate_function_lemmas foo bar [lemma1, lemma2] registering all the coercions and restating bar.lemma1 and bar.lemma2 would be extremely handy.

What about rho for the rotation number and tau for the translation number?

[Sebastien Gouezel]

While I'm dreaming, let me dream bigger. Is it possible that, whenever one declares a structure with a to_fun field, then a function coercion is automatically declared? An even nicer magic would be if all the fields of the structure involving to_fun and whose name ends with a prime would be restated without the prime and in terms of the function coercion.

And when one extends a structure foo with a to_fun field to a structure bar, then a function coercion could be registered for bar, and all lemmas of the form foo.lemma1 in the namespace foo and involving the function coercion for foo are restated in the bar namespace with the function coercion for bar?

I have the impression this would simplify a lot of boilerplate code we have to write for every new function-like structure we introduce.

[Eric Wieser]

That would definitely be a useful thing to happen, and would eliminate much of algebra.group.hom

[Johan Commelin]

@Sebastien Gouezel I completely agree. We just need someone with good meta skills to write the automation for us.

[Eric Wieser]

I think we could do similar automation for things with a carrier : set A member too

[Eric Wieser]

Would we get this inheritance automatically if we replaced monoid_hom A B with fun_subtype A B is_monoid_hom, where fun_subtype is defeq to subtype?

[Eric Wieser]

Then we could just stick all the generic ext/for/mk lemmas on fun_subtype

[Yury G. Kudryashov]

This is a workaround which is not free (e.g., it doesn't work for equivs) and doesn't give you automation for map_* and more advanced lemmas.

[Sebastien Gouezel]

You're right that for equiv it would do the wrong thing (a lemma for foo involving f (f.symm x) would be extended with the naive procedure I sketched to a lemma for which f.symm x would become f.to_foo.symm x, which is not what we want). What about an attribute @[extend_fun] if we want to extend the function lemmas from foo to bar automatically, and something else for equiv-like structures? An attribute @[extend_equiv] would not work, as the symm is meaningless when defining the structure, but a tactic that one would call once bar.symm and bar.refl have been defined would be an option.

[Yury G. Kudryashov]

@Sebastien Gouezel Sorry for not being clear. I was trying to say that @Eric Wieser's approach with subtype will not work in many cases.

[Sebastien Gouezel]

ok, thanks for the clarification. Still, there is indeed a problem with my initial proposal!

[Yury G. Kudryashov]

Yes, for equivs we need to define refl, symm, and trans manually.

[Yury G. Kudryashov]

And for homs we need to define id and comp manually.

[Eric Wieser]

it doesn't work for equivs

I hadn't thought of that

And for homs we need to define id and comp manually.

If we had fun_subtype A B is_monoid_hom, could we create a preserves_comp (is_monoid_hom A B) (is_monoid_hom B C) typeclass that can produce a is_monoid_hom A C instance, and then define fun_subtype.comp in terms of that typeclass?