Zulip Chat Archive

Stream: mathlib4

Topic: local homeomorph

Yury G. Kudryashov (Feb 14 2023 at 00:17):

I've started porting Topology.LocalHomeomorph. Since LocalEquiv is not a FunLike, the coercion to function is going to unfold to e.toLocalEquiv.toFun. This means that docs#local_homeomorph.symm_to_local_equiv will unfold e.symm.toFun to e.toLocalEquiv.symm.toFun which is the opposite of docs#local_homeomorph.coe_coe_symm (which becomes a syntatic rfl).

Yury G. Kudryashov (Feb 14 2023 at 00:18):

What should I do?

  1. Proceed with (e : α → β) = e.toLocalEquiv.toFun, adjust some simp lemmas, await for broken proofs down the import chain.
  2. Define LocalHomeomorph.toFun', use it as coercion, leave the refactor till after the porting.

Yury G. Kudryashov (Feb 14 2023 at 00:19):

  1. Something I missed.

Yury G. Kudryashov (Feb 14 2023 at 23:05):

Let me tag some users of local_homeomorph: @Heather Macbeth @Sebastien Gouezel @Floris van Doorn @Nicolò Cavalleri @Scott Morrison @Eric Wieser @Patrick Massot

Floris van Doorn (Feb 15 2023 at 12:29):

Ah, you cannot make then FunLike instances because the toFun map is not injective...

Going with option 2 might be best for now, since it's the behavior that is most similar to Lean 3.

Last updated: Dec 20 2023 at 11:08 UTC