Zulip Chat Archive

Stream: maths

Topic: Translation/rotation number for various maps


view this post on Zulip Yury G. Kudryashov (Dec 06 2020 at 22:44):

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 R/Z\mathbb R/\mathbb Z;
  • circle_diffeo: an order-preserving CrC^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?

view this post on Zulip Yury G. Kudryashov (Dec 06 2020 at 22:51):

@Sebastien Gouezel :up:

view this post on Zulip Sebastien Gouezel (Dec 07 2020 at 08:06):

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?

view this post on Zulip Sebastien Gouezel (Dec 07 2020 at 09:17):

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.

view this post on Zulip Eric Wieser (Dec 07 2020 at 10:48):

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

view this post on Zulip Johan Commelin (Dec 07 2020 at 11:09):

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

view this post on Zulip Eric Wieser (Dec 07 2020 at 13:13):

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

view this post on Zulip Eric Wieser (Dec 07 2020 at 13:20):

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?

view this post on Zulip Eric Wieser (Dec 07 2020 at 13:21):

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

view this post on Zulip Yury G. Kudryashov (Dec 07 2020 at 13:41):

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.

view this post on Zulip Sebastien Gouezel (Dec 07 2020 at 14:02):

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.

view this post on Zulip Yury G. Kudryashov (Dec 07 2020 at 14:10):

@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.

view this post on Zulip Sebastien Gouezel (Dec 07 2020 at 14:11):

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

view this post on Zulip Yury G. Kudryashov (Dec 07 2020 at 14:12):

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

view this post on Zulip Yury G. Kudryashov (Dec 07 2020 at 14:12):

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

view this post on Zulip Eric Wieser (Dec 07 2020 at 14:21):

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?


Last updated: May 09 2021 at 10:11 UTC