Embedding is local

Stream: Is there code for X?

[Andrew Yang]

What is the best way to show the following fact?
Given a map f : α → β, and an open cover U : set (opens β) of β, if f restricted on s is
inducing (resp. (open / closed) embedding) for all s : U, then f itself also is.

Side question:
What is the best way to restrict a map f : α → β to a f ⁻¹' s → s with s : opens β?
I'm currently using something like some_iso ≫ pullback f s.inclusion so there probably exists a better way.

[Floris van Doorn]

To answer your last question: I'd use (f ⁻¹' s).restrict f.

[Floris van Doorn]

Oh wait, I mean (set.maps_to_preimage f s).restrict _ _ _ if it's important that the codomain is s

[Yury G. Kudryashov]

Also feel free to add a definition for bundled continuous maps

[Andrew Yang]

It took me some time to get back to this, but I have a rough draft now in #12361. I have never used the topology library except with Top, and it would be great if someone who knows their way around the topology library can give some opinions.

[Andrew Yang]

Side question: Do we not have / need a predicate is_homeomorph except for @is_iso Top _ _ _?

[Kevin Buzzard]

I guess nonempty (X ≃ₜ Y)?

[Patrick Massot]

Andrew, are you really really really sure you need all those subtypes? It sounds like asking for a lot of trouble.

[Patrick Massot]

Could you tell me what is your actual goal?

[Andrew Yang]

Oh. I meant the predicate for a map. ∃ (e : X ≃ₜ Y), e.to_fun = f might work, ∃ (h : bijective f), continuous f ∧ continuous (the_inverse) might also work. But do we have a consistent way of doing so? Or have we never used such predicates?

[Patrick Massot]

Even using opens is a very suspicious move.

[Andrew Yang]

This is used in the AG project, where opens is ubiquitous and I couldn't really avoid them.
I want to show that for a X : Scheme and a U : ι → (opens X.carrier) with supr U = ⊤, then ∀ i, is_iso (f ∣_ U i) ↔ is_iso f, where f ∣_ U i is the restriction of f on U i. And the same when f is replaced by closed_immersion and open_immersion.

[Patrick Massot]

I think you work with unbundled stuff until the very last moment where you package the end-result in whatever form you need in AG.

[Jake Levinson]

Reviving this thread. @Sam van G @Andrew Yang @Jujian Zhang

@Sam van G and I are trying to implement some equivalent definitions of closed immersions of schemes. We made a PR (#15291) that shows that surjective ring homomorphisms induce closed embeddings of prime_spectrums and can also write a definition of closed immersion of schemes using an is_locally_surjective predicate on maps of (pre)sheaves (not yet PRed). We have also looked at #14899 and #15283.

Currently we're trying to show that for a map {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) that is_closed_immersion f holds iff it holds locally on Y. Is your corresponding statement about topological spaces in mathlib now?

[Jujian Zhang]

I think @Andrew Yang is working on and is close to show the localness of closed immersion.

[Andrew Yang]

No. I opened a draft PR (#12361) and that's about it. I could revive it if you need it. Or you are welcome to take the code there and make a new PR out of it.

[Jujian Zhang]

Don’t look at #14899 the definition that I give is actually wrong.

[Andrew Yang]

Is it still wrong? I thought the current version is correct.

[Jujian Zhang]

I thought I didn’t push the corrected version, never mind.

[Andrew Yang]

Also, I'm not working on it anymore after I heard about the LftCM project.
The furthest i've got is the draft PR above and the code I mentioned over at the other stream.

[Jake Levinson]

Okay - certainly @Sam van G and I are happy to reuse / copy any code from your PRs while we continue to work on it this week (and include your names in the authorship etc).

@Jujian Zhang I remember your definition of "surjective sheaf morphism on stalks", given f : X ⟶ Y and the induced morphism 𝒪_Y ⟶ f_* 𝒪_X of sheaves on Y, seemed to be quantified over points x : X and corresponding stalks, rather than points y : Y. So I also wasn't sure if it was correct. Maybe equivalent to the usual notion?

[Jujian Zhang]

You are right, it should be quantified over all y : Y. I have pushed a corrected version. Thank you for the correction.