Int-equivariant equivs

Stream: maths

[Yury G. Kudryashov]

In the sphere eversion project, an EquivariantEquiv is defined as

structure EquivariantEquiv extends ℝ ≃ ℝ where
  map_zero' : toFun 0 = 0
  eqv' : ∀ t, toFun (t + 1) = toFun t + 1

I'm going to port EquivariantMap and EquivariantEquiv to Mathlib (probably, under the names IntEquivariantMap and IntEquivariantEquiv) and merge with docs#CircleDeg1Lift

[Yury G. Kudryashov]

I have 2 questions (probably, to @Patrick Massot ):

1. How often do you need non-monotone equivariant maps?
2. Why do you need map_zero' (I didn't read how do you use it yet)?

[Anatole Dedecker]

I think ultimately the right thing to do is to use @Antoine Chambert-Loir’s work around equivariant maps, but I don’t know how far it is from mathlib-ready

[Anatole Dedecker]

See #6057 and the related discussion in #PR reviews

[Yury G. Kudryashov]

While this is the right thing to do (and I'm going to link IntEquivariant* to Antoine's typeclasses), verifying f (x + 1) = f x + 1 is much easier.

[Eric Wieser]

Should this just be a map from add_circle 1?

[Anatole Dedecker]

Yury G. Kudryashov said:

While this is the right thing to do (and I'm going to link IntEquivariant* to Antoine's typeclasses), verifying f (x + 1) = f x + 1 is much easier.

IMHO that should be a theorem, not the definition

[Anatole Dedecker]

Eric Wieser said:

Should this just be a map from add_circle 1?

No, that would be f (x + 1) = f x. Unless you also force the codomain to be the add_circle, but then going back to the good old real function becomes painful

[Yury G. Kudryashov]

In fact, "lift of a circle self-map" is the main use case for me.

[Yury G. Kudryashov]

Do we have an instance for AddAction Int R, if R is a Ring (or an AddGroupWithOne)?

[Patrick Massot]

Yury G. Kudryashov said:

I have 2 questions (probably, to Patrick Massot ):

1. How often do you need non-monotone equivariant maps?
2. Why do you need map_zero' (I didn't read how do you use it yet)?

I think that in the sphere eversion project, the answer to 1 is: never. I think we only need this construction in reparametrization.lean. The goal is really to build circle diffeomorphisms fixing a base point. Fixing the circle base point is the reason for map_zero' but of course in a more general context we shouldn't impose this condition (at least not right away). The reason why we don't use the circle directly is that calculus on $$\mathbb{R]$$ is much easier to manipulate in Lean. In particular a very important statement for us is cont_diff_parametric_symm_of_deriv_pos.

[Yury G. Kudryashov]

Am I right that you don't use docs#AddCircle because it was not there at the time of writing?

[Patrick Massot]

I don't remember whether it was there or not. Does it allow to do calculus without using the manifolds library?

[Yury G. Kudryashov]

@Anatole Dedecker There are at least 8 ways to say f (x + 1) = f x + 1 using generic equivariant maps (Int, Nat, multiples, zmultiples, possibly with an opposite). I would prefer to have a structure that uses f (x + 1) = f x + 1 or a def as the canonical way to talk about these maps.

[Yury G. Kudryashov]

@Patrick Massot No, it doesn't. But it may have more lemmas than a custom circle type you define in the project.

[Patrick Massot]

It seems @Oliver Nash introduced this definition in https://github.com/leanprover-community/sphere-eversion/commit/4a217290c0a67f44096ef83f951e06c910bf226e, maybe he remembers?

[Patrick Massot]

But in any case I'd be happy to use mathlib more of course.

[Anatole Dedecker]

Yury G. Kudryashov said:

Anatole Dedecker There are at least 8 ways to say f (x + 1) = f x + 1 using generic equivariant maps (Int, Nat, multiples, zmultiples, possibly with an opposite). I would prefer to have a structure that uses f (x + 1) = f x + 1 or a def as the canonical way to talk about these maps.

I would argue that being equivariant for the Int action is obviously the right characterization (precisely because you can lift to the circle easily), but I get your point.

[Patrick Massot]

I'm sorry I have very little time to help with the sphere eversion port. I'm less than three days away from moving my family to a different continent for one year.

[Yury G. Kudryashov]

@Anatole Dedecker In case of a Semiring, being equivariant for Nat is better. Also, if you want to talk about f (x + 1) = f x + n (we may add this later - e.g., to prove that under some assumptions, the corresponding circle self-map is conjugate to multiplication by n), then you need something like EquivariantMap (MonoidHom.mulLeft n) R R (not tested).

[Yury G. Kudryashov]

@Patrick Massot Good luck with packing&moving!

[Yury G. Kudryashov]

@Anatole Dedecker BTW, we don't have an additive action of Int on an AddGroupWithOne.

[Eric Wieser]

Yury G. Kudryashov said:

Do we have an instance for AddAction Int R, if R is a Ring (or an AddGroupWithOne)?

I think we should, but I fear this may necessitate a AddGroupWithOne.zvadd field. I guess we should see if we can craft any diamonds with Int.cast z + r.

[Eric Wieser]

Patrick Massot said:

I'm sorry I have very little time to help with the sphere eversion port. I'm less than three days away from moving my family to a different continent for one year.

Wow, that sounds challenging in both directions: good luck! Is the move in some way Lean motivated (and if so, will we be hearing about it soon)?

[Kevin Buzzard]

I think it's public knowledge that he's visiting Jeremy for the year.

[Yury G. Kudryashov]

What would be a better name for docs#CircleDeg1Lift ?

[Yury G. Kudryashov]

It assumes f (x + 1) = f x + 1 and Monotone f.

[Yury G. Kudryashov]

NatEquivariantMonoMap is a natural alternative but it's not much more readable than CircleDeg1Lift.

[Patrick Massot]

Kevin Buzzard said:

I think it's public knowledge that he's visiting Jeremy for the year.

Maybe it wasn't so public if Eric didn't know. I've been thinking about this so much that I may have ended up imagining everybody knew! Indeed I have the great opportunity of spending one year in the Hoskinson center at CMU with Jeremy and his team.

[Oliver Nash]

Patrick Massot said:

It seems Oliver Nash introduced this definition in https://github.com/leanprover-community/sphere-eversion/commit/4a217290c0a67f44096ef83f951e06c910bf226e, maybe he remembers [that you don't use docs#AddCircle because it was not there at the time of writing]?

Indeed docs#AddCircle did not exist when this work in the SE project was done but as Patrick says, using equivariant maps on the reals, rather than maps from the circle enabled us to avoid using the manifold library for such simple calculus.

[Oliver Nash]

This is still true btw: even though it's tangent bundle is trivial, the only way to do calculus on the circle is to regard it as a manifold.

[Oliver Nash]

You can see me waffling on about this here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Calculus.20on.20the.20circle/near/305005742 (and IIRC briefly also in some other thread about generalising calculus to TVS without norms that I can't seem to find at the moment --- the point is that you don't need a full vector space structure, just an action of sufficiently small scalars).

[Oliver Nash]

Regarding design, my first instincts were that I'd like to see Int-equivariant maps as special case of a general definition (which I think is Anantole's view) but when I reflect that we have a special type for the circle I think I'm persuaded that it's a good idea to have a special case for Int-equivariant maps too.

[Eric Wieser]

Wouldn't the analog of the add_circle p case be f (x + p) = f x + p, rather than only considering p = 1?

[Eric Wieser]

Or are you talking about docs#Circle ?

[Antoine Chambert-Loir]

Anatole Dedecker said:

See #6057 and the related discussion in #PR reviews

I have good reasons to wish that it be done swiftly, but will probably be away this week. Some stuff has to be fixed, and most importantly, somebody fluent in mathlib should check I do things correctly at the very start. Then I can do the dirty job.