Generalizing `PartialHomeomorph`?

Stream: mathlib4

[Hannah Scholz]

While working with CW complexes I encounter a lot of PartialEquivs that are continuous on their source and target which in my cases are not open: examples are the characteristic maps of a CW complex or cellular maps (where both source and target are closed). That means that my statements can get quite long. Additionally, I would like some lemmas in mathlib for this specific type of PartialEquiv which currently is awkward because there is no good place for them (see #23048). My question is: Should one maybe generalize PartialHomeomorph? I think there could be one general version that has no limitations on the openness or closedness of the source and target. Then the current PartialHomeomorph could become something like OpenPartialHomeomorph and then the closed version could be ClosedPartialHomeomorph. I assume that the general version would probably find use in a lot of places. What do you think?

[Floris van Doorn]

I think this would be good to do. We already have a few "continuous partial equivalences" in Mathlib, e.g. docs#ModelWithCorners. So having a definition that generalizes them and provides common lemmas sounds valuable.

[Michael Rothgang]

Feel free to ask me for review on the PR doing this.

[Floris van Doorn]

Hannah and I would like to go forward with Hannah's proposal above:

• rename the current PartialHomeomorph to OpenPartialHomeomorph
• add a new version of PartialHomeomorph that doesn't assume openness of source/target
• add ClosedPartialHomeomorph with closed source/target

I think that it will be useful for both CW-complexes and manifolds (e.g. ModelWithCorners), but probably also in various other places.

I'm asking again, because this got little response until now. Does this sound like a good change?
@Patrick Massot @Sébastien Gouëzel @Heather Macbeth @Oliver Nash

[Oliver Nash]

It sounds like a good plan. For the sake of considering a variant, do you think the following might be useful:

structure PartialHomeomorph (X : Type*) (Y : Type*) [TopologicalSpace X]
  [TopologicalSpace Y] (P : Set X → Prop) (Q : Set Y → Prop) extends PartialEquiv X Y where
  pred_source : P source
  pred_target : Q target
  continuousOn_toFun : ContinuousOn toFun source
  continuousOn_invFun : ContinuousOn invFun target

[Sébastien Gouëzel]

@Floris van Doorn, if you have the need for it, then go for it, sure! We could then upgrade extChartAt to be a PartialHomeomorph in your sense, for instance.

[Floris van Doorn]

Oliver Nash said:

It sounds like a good plan. For the sake of considering a variant, do you think the following might be useful:

structure PartialHomeomorph (X : Type*) (Y : Type*) [TopologicalSpace X]
  [TopologicalSpace Y] (P : Set X → Prop) (Q : Set Y → Prop) extends PartialEquiv X Y where
  pred_source : P source
  pred_target : Q target
  continuousOn_toFun : ContinuousOn toFun source
  continuousOn_invFun : ContinuousOn invFun target

This is an interesting thought, since that would be a common generalization of all three notions.
However, I'm not sure if that this will be more convenient this than with just the plain PartialHomeomorph that I'm suggesting. I expect that if you want to define e.g. PartialHomeomorph .trans you already need conditions on P and Q such as they're closed under taking intersections.
I think that just the plain PartialHomeomorph will be more convenient.

[Michael Rothgang]

#29113 does the first step: renaming PartialHomeomorph to OpenPartialHomeomorph

[Michael Rothgang]

Waking up, I wondered about the deprecation strategy for this change. Its namespace changes don't need deprecations, but other changes will. In general, I would ask for the following:

• a deprecated alias PartialHomomeomorph pointing to OpenPartialHomeomorph (perhaps with a custom message, indicating the impending generalisation!)
• a deprecation for each lemma which is not simply changing namespaces
• waiting until a stable release has happened before re-purposing the PartialHomeomorph name

[Michael Rothgang]

In this case, you will be generalising some lemmas from OpenPartialHomeomorph to PartialHomommorph, right? Does it make sense to include deprecations there/can these be counter-productive? (Perhaps this is fine, and any lemma that's not maximally general will land as-is. You can always generalise later, after all.)