feat(Topology/Group): Continuous isomorphism

[Thmoas-Guan]

Define the continuous isomorphisms of multiplicative and additive topological group.

---

• depends on: feat(Topology): Introduce HomeomorphClass #18689

[github-actions]

PR summary 1b1887923b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ContinuousAddEquiv
+ ContinuousMulEquiv
+ HomeomorphClass
+ apply_eq_iff_eq
+ apply_eq_iff_symm_apply
+ apply_symm_apply
+ bijective
+ coe_coe
+ coe_mk
+ coe_refl
+ coe_toHomeomorph_symm
+ coe_trans
+ comp_symm_eq
+ congr_arg
+ congr_fun
+ continuousMulEquivOfUnique
+ eq_comp_symm
+ eq_symm_apply
+ eq_symm_comp
+ equivLike_inv_eq_symm
+ ext
+ injective
+ instance : CoeFun (M ≃ₜ* N) fun _ ↦ M → N
+ instance : EquivLike (M ≃ₜ* N) M N
+ instance : HomeomorphClass (M ≃ₜ* N) M N
+ instance : HomeomorphClass (α ≃ₜ β) α β
+ instance : Inhabited (M ≃ₜ* M) := ⟨ContinuousMulEquiv.refl M⟩
+ instance : MulEquivClass (M ≃ₜ* N) M N
+ instance [HomeomorphClass F α β] : CoeTC F (α ≃ₜ β)
+ instance {M N} [Unique M] [Unique N] [Mul M] [Mul N]
+ invFun_eq_symm
+ mk'
+ ofContinuousMulEquivProfiniteGrp
+ refl
+ refl_apply
+ self_comp_symm
+ self_trans_symm
+ surjective
+ symm
+ symm_apply_apply
+ symm_apply_eq
+ symm_comp_eq
+ symm_comp_self
+ symm_symm
+ symm_trans_apply
+ symm_trans_self
+ toEquiv_eq_coe
+ toHomeomorph
+ toHomeomorph_injective
+ totallyDisconnectedSpace
+ trans
+ trans_apply

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[Ruben-VandeVelde]

Can you please follow the structure from #16908 and #16867?

[urkud]

Please avoid hom classes that use both algebra and topology. A better way is to introduce HomeomorphClass and assume [AddEquivClass F A B] [HomeomorphClass F A B] whenever needed.

[Thmoas-Guan]

I think HomeomorphClass doesn't exist at all. There is kind of a reason below:

Also, the design is under the suggextion below:

Is it safe to introduce two instances like this?
Is there a reason of avoiding the use of both algebra and topology?
Also, what about ContinuousMonoidHomClass, in this sense why this exists?
Sorry that I donesn't know much about how to design APIs, I just follow the suggestions copying the existing codes and create this PR.

[j-loreaux]

@Thmoas-Guan earlier in Mathlib, we would mix algebra / topology in hom classes. This was necessary because they all extended FunLike (or EquivLike). However, we have since pulled this out and pass it as an argument instead. As such, the hom classes are now Prop-valued, and it now makes more sense to split them into their respective parts, hence the suggestion from Yury not to mix.

Also, Yury knows we don't have HomeomorphClass, that's why he's asking you to introduce it (it should be a separate PR though, on which this one will then depend). Note also: ContinuousMonoidHomClass is deprecated.

Does this course of action make sense? Do you know how to proceed?

[Thmoas-Guan]

I introduced HomeomorphClass in PR #18689, may I ask for your help to review it too? Thank you

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Topology): Introduce HomeomorphClass #18689
  By Dependent Issues (🤖). Happy coding!