pequiv vs local_equiv

Stream: general

[Yury G. Kudryashov]

It seems to me that they both model the same mathematical concept. Do we need both of them?

[Yury G. Kudryashov]

pequivs have better definitional equality at the cost of bad codomains of to_fun and inv_fun.

[Chris Hughes]

pequivs also have better equality. I think, though I may be wrong, that equality of local_equiv depends on the out of domain behaviour. There's redundant information in a local equiv, which mucks up equality.

[Kevin Buzzard]

whatever is "out of domain behaviour"?

[Chris Hughes]

An example is how $0^{-1}=0$

[Chris Hughes]

local_equiv is a partial function, but it's implemented as a total function that returns junk outside of the domain of the partial function.

[Reid Barton]

I think the answer is: try to port manifolds to pequiv or something else that has the correct equality and see if you can do it without everything falling over.

[Reid Barton]

If you can, it will be great.

[Yury G. Kudryashov]

pequiv won't work, e.g., in the inverse function theorem because I want (h.to_local_homeomorph f).to_fun = f to be defeq. This way it's much easier to prove theorems about local_homeomorphs and apply to the original function. Probably the same is the case in many places in manifolds.

[Yury G. Kudryashov]

Probably we should mention each equivalence in the docstring of another and prove that the quotient of local_equiv by eq_on_source is the same as pequiv.

[Mario Carneiro]

that's not true either, unfortunately, because of empty types

[Mario Carneiro]

it's not always possible to add "junk" to complete the function

[Yury G. Kudryashov]

OK, it's the same provided [nonempty α] [nonempty β]

[Mario Carneiro]

I think you can get a pequiv to invert to the original function, but you have to supply a proof that it is total

[Mario Carneiro]

When you are working with a pequiv, you should never talk about out of range values, and as long as you are in range it should be defeq to the original function f

[Yury G. Kudryashov]

Another difficulty with calculus and pequiv: I can't say that the forward/inverse function is differentiable because it has a bad codomain.

[Mario Carneiro]

what do you mean? I thought we had support for differentiating partial functions

[Yury G. Kudryashov]

Do we?

[Mario Carneiro]

ah, we had a big discussion about this when it was getting set up. Looks like the core definitions all assume f itself is total

[Mario Carneiro]

There are some useful filters for partial functions but they weren't hooked up to deriv

[Mario Carneiro]

I guess the nearest approximation is to say that a pequiv is differentiable if it extends to a function that is differentiable on the subset