[Merged by Bors] - feat(Analysis/SpecialFunctions/Complex/Circle): expMapCircle as a PartialHomeomorph and prove IsLocalHomeomorph

[tb65536]

This PR proves IsLocalHomeomorph expMapCircle (eventually this should be upgraded to IsCoveringMap, but that's a good deal harder and is probably best done via general theory such as in #7596).

---

[loefflerd]

I'm not 100% sure this is the right approach. I'd advocate for going via AddCircle: we should prove that for any 0 < T, the natural quotient map from ℝ to AddCircle T is a partial equiv resp. local homemorph, and then show that AddCircle.toCircle is a homeomorphism AddCircle T → circle.

[tb65536]

I agree that this isn't really the right approach. But I think the right approach is probably to do the full "quotient by discrete subgroup" theory and deduce PartialEquiv and PartialHomeomorph from that. In the meantime, it seems fine to add these constructions manually?

If you do want the corresponding constructions for AddCircle, it might currently be easiest to construct them from circle rather than the other way around since currently AddCircle.toCircle imports Analysis/SpecialFunctions/Complex/Circle (although that could be changed).

[loefflerd]

I agree that this isn't really the right approach. But I think the right approach is probably to do the full "quotient by discrete subgroup" theory and deduce PartialEquiv and PartialHomeomorph from that. In the meantime, it seems fine to add these constructions manually?

My point is that in the current state of the library it would still probably be easier to go via AddCircle, since there is already a lot of API present for equivalences between AddCircle and various kinds of intervals. Moreover, this would work over arbitrary linearly ordered rings, rather than being specific to the reals.

If you do want the corresponding constructions for AddCircle, it might currently be easiest to construct them from circle rather than the other way around since currently AddCircle.toCircle imports Analysis/SpecialFunctions/Complex/Circle (although that could be changed).

Well, AddCircle.toCircle is the map between both kinds of circle, so of course the file defining it needs to import the files defining both. But most of the AddCircle API is defined elsewhere.

[tb65536]

Good point about generalizing beyond the reals. I'll give it a shot.

[loefflerd]

Looks good! Just some minor stylistic suggestions.

[loefflerd]

LGTM, thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ tb65536 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[tb65536]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style