# Zulip Chat Archive

## Stream: maths

### Topic: Translation/rotation number for various maps

#### 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 $\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 (Dec 06 2020 at 22:51):

@Sebastien Gouezel :up:

#### 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?

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

#### 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`

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

#### Eric Wieser (Dec 07 2020 at 13:13):

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

member too

#### 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?

#### Eric Wieser (Dec 07 2020 at 13:21):

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

#### Yury G. Kudryashov (Dec 07 2020 at 13:41):

This is a workaround which is not free (e.g., it doesn't work for `equiv`

s) and doesn't give you automation for `map_*`

and more advanced lemmas.

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

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

#### Sebastien Gouezel (Dec 07 2020 at 14:11):

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

#### Yury G. Kudryashov (Dec 07 2020 at 14:12):

Yes, for `equiv`

s we need to define `refl`

, `symm`

, and `trans`

manually.

#### Yury G. Kudryashov (Dec 07 2020 at 14:12):

And for `hom`

s we need to define `id`

and `comp`

manually.

#### 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