feat(Topology): Introduce HomeomorphClass

[Thmoas-Guan]

Introduce HomeomorphClass

---

[github-actions]

PR summary 65762b3153

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ HomeomorphClass
+ coe_coe
+ instance : HomeomorphClass (α ≃ₜ β) α β
+ instance [HomeomorphClass F α β] : CoeTC F (α ≃ₜ β)
+ toHomeomorph
+ toHomeomorph_injective

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.

[j-loreaux]

Thanks for this addition! Can you please also add the analogue of this lemma, and address my comments below?

@[simp]
theorem RingHom.coe_coe {α : Type u_2} {β : Type u_3} :
∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_5} [inst : FunLike F α β]
  [inst_1 : RingHomClass F α β] (f : F), ⇑↑f = ⇑f

[j-loreaux]

please ask on Zulip what is the correct class to use here. CoeTC is not preferred (although it's littered throughout Mathlib). We need to come to a consensus on Zulip about which Coe class is best for coercions from morphism classes to morphisms.

[Thmoas-Guan]

Asked in a thread of PR review, needed anywhere else?

[j-loreaux]

I don't think we have this for other morphism classes. I suspect it's not necessary as we can just apply the coercion to functions and then use DFunLike.coe_injective (probably after simp)

[Thmoas-Guan]

I copied this lemma from MulEquivClass, I didn't think carefully whether it is useful.