edge cases not covered by `IsCoveringMap`

Stream: mathlib4

[Junyan Xu]

The inclusion of one of the points E = {x} into a two-point discrete space B = {x,y} is a covering map by the usual definition. However, it doesn't satisfy mathlib's docs#IsCoveringMap, because y isn't docs#IsEvenlyCovered: there doesn't exist the required docs#Trivialization because the fiber F (= preimage of y) is empty, but E is not, so there is no map from E to B × F. I'm trying to figure out what's the best way to fix this. The current definition seems to originate from #Berkeley Lean Seminar > Covering Spaces @ 💬, cc @Thomas Browning

[Thomas Browning]

In some sense, is this an issue with docs#Trivialization? docs#Trivialization requires a map defined on all of E, even if the source ends up being empty?

[Junyan Xu]

Yeah you can trace this back to docs#Pretrivialization, docs#PartialHomeomorph and docs#PartialEquiv. These are used extensively in the manifold / differential geometry library though, and I wonder whether they'll find their category of fiber bundles etc. are missing some objects when they start considering such categories. (if the fiber is constant it should be okay though)

I think the easiest fix is probably falling back to the f ⁻¹' {x} × U ≃ₜ f ⁻¹' U definition.

[Aaron Liu]

This is a consequence of the partial equivalence design, where you define it as two functions defined on the whole space which are inverses on this set, and please don't apply it to anywhere outside the set

[Thomas Browning]

Junyan Xu said:

I think the easiest fix is probably falling back to the f ⁻¹' {x} × U ≃ₜ f ⁻¹' U definition.

Yeah, that's definitely the easiest short-term fix. But even for docs#PartialEquiv, if α is nonempty and β is empty, then under the current definition there is no partial equiv between the empty subsets, even through there technically ought to be.

[Aaron Liu]

You can always just use docs#PEquiv

[Junyan Xu]

Going back and forth with Option may not be simpler than doing so with Subtype?

[Aaron Liu]

There are lots of options (pun not intended)

[Aaron Liu]

I'm not sure how I feel about FunLike (α ≃. β) α (Option β) though

[Junyan Xu]

I'd argue using subtype/subspaces is the closest to mathematical practice.

[Aaron Liu]

The issue is you have to provide a proof, though there are ways around this

[Thomas Browning]

So would the ultimate refactor be to change docs#PartialHomeomorph to use a homeomorphism between two subtypes?

[Aaron Liu]

I think that would be a good idea, though I'd like to see some other opinions

[Thomas Browning]

You could maybe still have a coercion to a global function in the case where Y is nonempty.

[Aaron Liu]

There are some notes about this in the module docstring for file#Logic/Equiv/PartialEquiv

[Junyan Xu]

We could still develop APIs for functions defined on sets, like docs#LinearIndepOn.

[Junyan Xu]

I forgot why we chose to use docs#Trivialization to define IsCoveringMap ...
(but maybe we still want to use it after fixing it)

[Thomas Browning]

Probably just because it's cleaner to reuse existing definitions

[Junyan Xu]

I came up with a minimally invasive fix in #24983. The definition is switched to the standard one (f ⁻¹' {x} × U ≃ₜ f ⁻¹' U), but I provide API to convert between the Trivialization formulation, so most proofs don't need to be changed. As a sanity check I proved that any map between two discrete spaces is a covering map.