API/tactic for subspace topology

Stream: Is there code for X?

[Winston Yin (尹維晨)]

I had to prove something like:

example (s t : Set ℝ) : closure (s ∩ t) ∩ t ⊆ s ∩ t := by
  rw [← Subtype.image_preimage_val, ← Subtype.image_preimage_val,
    image_subset_image_iff Subtype.val_injective]
  intros t ht
  rw [mem_preimage, ← closure_subtype] at ht
  revert ht t
  apply IsClosed.closure_subset
  -- goal state: `IsClosed (Subtype.val ⁻¹' s)`
  sorry

In informal mathematics, you would just get to this point by saying "it suffices to show that s ∩ t is closed in the subspace topology of t". Here, I had to finagle the goal into that form by some incantations that are not very discoverable, with all this subtype stuff that's foreign to people who just want to do some analysis.

Is this an inevitable consequence of using type theory, or can we come up with a way to improve user experience when doing point set topology? What would it take, a duplicate API for intersecting with subtypes or writing some new tactic? Maybe something easier already exists in Mathlib?

[Utensil Song]

import Mathlib

example (s t : Set ℝ) (hs : IsClosed s) : closure (s ∩ t) ∩ t ⊆ s ∩ t := by
  simp only [Set.subset_inter_iff, Set.inter_subset_right, and_true]
  intro x hx
  obtain ⟨hxst, hxt⟩ := hx
  have hsub : closure (s ∩ t) ⊆ s := by
    rw [propext (IsClosed.closure_subset_iff hs)]
    exact Set.inter_subset_left s t
  exact hsub hxst

I don't seem to need to touch subtype stuff during the proof. (I added IsClosed as it seems that I need it for the statement to be true )

[Winston Yin (尹維晨)]

In my case, s is not actually closed. It's s ∩ t that is closed in the subspace topology of t

[Utensil Song]

import Mathlib

example (s t : Set ℝ) (hst: IsClosed (s ∩ t)) : closure (s ∩ t) ∩ t ⊆ s ∩ t := by
  simp only [Set.subset_inter_iff, Set.inter_subset_right, and_true]
  intro x hx
  obtain ⟨hxst, _⟩ := hx
  have h : (s ∩ t) ⊆ s := by exact Set.inter_subset_left s t
  have hsub : closure (s ∩ t) ⊆ (s ∩ t) := by
    rw [propext (IsClosed.closure_subset_iff hst)]
  exact h (hsub hxst)
  done

Do you mean this? Can you make a #mwe ? It doesn't seem that IsClosed (s ∩ t) can be deduced from other hypotheses, only that IsClosed (closure (s ∩ t)).

[Andrew Yang]

I believe he meant IsClosed (Subtype.val ⁻¹' s : Set t)

[Andrew Yang]

import Mathlib

variable {X} [TopologicalSpace X] (t : Set X)

example (s t : Set X) (hs : IsClosed (Subtype.val ⁻¹' s : Set t)) : closure (s ∩ t) ∩ t ⊆ s ∩ t := by
  suffices : closure (Subtype.val ⁻¹' s : Set t) ⊆ (Subtype.val ⁻¹' s : Set t)
  · convert Set.image_subset Subtype.val this <;> simp [embedding_subtype_val.closure_eq_preimage_closure_image]
  rwa [IsClosed.closure_subset_iff]

[Utensil Song]

I thought that from the "suffices" up there, he doesn't like to see anything Subtype, particularly not in hypotheses.

[Utensil Song]

At any rate, the proof needs something to be closed, but it's not given in the intial code.

[Andrew Yang]

However IsClosed (s ∩ t) is stronger than IsClosed (Subtype.val ⁻¹' s : Set t) and the equivalent without subtypes is probably ∃ s', IsClosed s' ∧ s ∩ t = s' ∩ t.

[Miguel Marco]

I did find that kind of problem when formalizing my general topology course, so I had to create my own API for that. For convenience, I did create an operation ↓∩ to convert a set of the universe, to a set in a subtype by intersecting it, and then prove the lemmas I need for that subspace topology (many of them are marked as simp for convenience).

It is in Lean3, but porting it to Lean4 should be straightforward. It also uses spanish names... I hope that is not a problem.
Check it here:
https://github.com/miguelmarco/topologia_general_lean/blob/master/subconjuntos.lean
and here
https://github.com/miguelmarco/topologia_general_lean/blob/master/subespacios.lean

[Winston Yin (尹維晨)]

Utensil Song said:

I thought that from the "suffices" up there, he doesn't like to see anything Subtype, particularly not in hypotheses.

Apologies for being a bit unclear. I want Lean to be able to apply IsClosed.closure_subset nearly directly to a goal closure (s ∩ t) ∩ t ⊆ s ∩ t to turn it into IsClosed (Subtype.val ⁻¹' s), by specifying that we are working in the subspace topology of t.

[Winston Yin (尹維晨)]

If I hadn't learnt much type theory, I would not have thought that Subtype.val has anything to do with the original goal at hand, and would have overlooked all the Subtype lemmas. Being able to transform the goal from ... ∩ t to the corresponding statement explicitly mentioning Subtype.val cues the user to now look for and apply Subtype.val lemmas.

[Winston Yin (尹維晨)]

@Miguel Marco Thanks for sharing! This seems like the sort of thing that would've been useful to me! Do people think Mathlib could use something like this?

[Miguel Marco]

Winston Yin (尹維晨) said:

Miguel Marco Thanks for sharing! This seems like the sort of thing that would've been useful to me! Do people think Mathlib could use something like this?

I coinsidered trying to add it,but wasn't sure it would be a good fit. Subspace topology is treated in Mathlib as a particular case of inverse image topology, so there is no real need for that. But maybe other parts of Mathlib could find this kind of API useful. :man_shrugging:

[Andrew Yang]

I do think such a definition would be useful. We also have docs#Subgroup.subgroupOf for example.

[Winston Yin (尹維晨)]

I’d wager that Subtype.val is a pretty good special case of a continuous function, especially when I don’t think about it when dealing with topology within subsets.

[Utensil Song]

Subtype.val should be considered an implementation detail during constructing a mathematical construct. All later interactions with the mathematical construct should be via API lemmas that make sense in math too. This doesn't just happen to Subtype or dependent type theory based ITPs, it also happens in Math, e.g. Clifford Algebra can be constructed by a quotient of Tensor Algebra, so in Lean it could be chosen for the definition, but we throw that detail away once its universal properties are defined, and use only those lemmas afterward, as much as possible.

[Utensil Song]

The concept of lemma APIs are also discussed and explained here recently.

[Miguel Marco]

Andrew Yang said:

I do think such a definition would be useful. We also have docs#Subgroup.subgroupOf for example.

What would be the right place for it?

[Utensil Song]

Miguel Marco said:

Winston Yin (尹維晨) said:

Miguel Marco Thanks for sharing! This seems like the sort of thing that would've been useful to me! Do people think Mathlib could use something like this?

I coinsidered trying to add it,but wasn't sure it would be a good fit. Subspace topology is treated in Mathlib as a particular case of inverse image topology, so there is no real need for that. But maybe other parts of Mathlib could find this kind of API useful. :man_shrugging:

Where is inverse image topology in Mathlib? Can (hs : IsClosed (Subtype.val ⁻¹' s : Set t) be encoding by it and use lemmas there for this proof? With your code it can be encoded as (hs : IsClosed (restringe t s)) and use your lemmas (it seems to need a little more for the closure).

[Jireh Loreaux]

docs#TopologicalSpace.induced

[Jireh Loreaux]

The topology on a set (viewed as a type), is the topology induced by Subtype.val.

[Utensil Song]

Searching on moogle using "​preimage topology" didn't give me docs#TopologicalSpace.induced on the first page :joy: but it's in the doc string.

[Miguel Marco]

I only proved the API lemmas I needed for the theorems we prove in my course, so my API is not as complete as it could be.
Shouldn't be hard to extend it though.

[Winston Yin (尹維晨)]

Linking #9940 here.

[Anatole Dedecker]

I'm very late to the party, but I just wanted to mention that I would be sad if we ended up writing too much specialized theorems about the subspace topology specifically on a Subtype. It takes a while getting used to, but stating theorems in terms of docs#Embedding and docs#Inducing instead of subtypes is one of the reasons the general topology library works so well.

[Winston Yin (尹維晨)]

That raises a good point. Do you see a way to restate #9940 in terms of Inducing? I do think the special notation for subtype topology is valuable.

[Eric Wieser]

I don't think anything from 9940 is useful in that general case

[Eric Wieser]

Because in the general case I believe we're talking about preimages by an arbitrary function, rather than by Subtype.val

[Anatole Dedecker]

To be clear, I'm not against all of #9940. I think I'd be happy for getting the notation (writing preimages is a bit annoying sometimes). I haven't made up my mind about everything, I just wanted to mention my thoughts somewhere

[Eric Wieser]

#9940 is unfortunate that it seems to both tread in the delicate area of API design, and that the original (but presumably not only) motivation for it seems to be an #xy problem.

[Winston Yin (尹維晨)]

What would be a solution to the problem at the start of this thread?

[Eric Wieser]

Do you mean a proof for the example? Presumably you're after something shorter than what Utensil already provided?

[Winston Yin (尹維晨)]

Utensil's solution uses IsClosed s in the ambient topology, but that is not true in my case.

[Anatole Dedecker]

For reference, here is how I would have done it:

example (s t : Set X) (hs : IsClosed (Subtype.val ⁻¹' s : Set t)) :
    closure (s ∩ t) ∩ t ⊆ s ∩ t := by
  simp_rw [← Subtype.image_preimage_val t,
    ← embedding_subtype_val.closure_eq_preimage_closure_image, hs.closure_eq]
  rfl

It's very similar to Andrew's version, but I'm making explicit the key lemma docs#Subtype.image_preimage_val. Again, there are definitely documentation issues here, but this (and the more general docs#Set.image_preimage_inter) are typically the lemmas to use when pulling and pushing sets (docs#Filter.push_pull makes that even more explicit).

And then of course, there's the embedding_subtype_val part, which is exactly the property that you'd think of in the case of subspace topology

[Winston Yin (尹維晨)]

Oh that is much nicer

[Anatole Dedecker]

Of course I'm subject to the usual "I had to fight these issues for a while so now I've internalized how to do it" bias, so I really don't mean to say "the actual situation is perfect, don't touch it". Besides, we already have duplicates of a bunch of lemmas specific to the subtype case, and these would certainly benefit from better notation. I just wanted to make the point that it's more of a UX discussion than a mathematical one.

[Winston Yin (尹維晨)]

I'm incorporating your solution, Anatole, and it's great. However, this is still not very user-friendly given how basic subspace topology is.

[Winston Yin (尹維晨)]

I agree that it's more of a UX question.

[Eric Wieser]

Is your example deliberately stated as a subset inclusion when it appears to be true as an equality?

[Winston Yin (尹維晨)]

Yes. I applied another lemma that produced subset inclusion as a goal.

[Miguel Marco]

For what is worth, my original motivation for writing this API was totally UX-related: I wanted something that could allow my students to deal with subspace topology in a less intimidating form.

[Winston Yin (尹維晨)]

I get that the general advice is to avoid subtypes and especially subtypes of subtypes whenever possible, so all this Subtype.val showing up may be a feature rather than a bug, hinting that the user is using the wrong approach. But for subspace topology nested subtypes are unavoidable, and we should have good API / notation for it, along the lines of Miguel's PR #9940.

[Eric Wieser]

I don't think that Subtype.val showing up is indicative of a bad approach; rather that if you can replace it with a general f that's an embedding, things become simpler

[Anatole Dedecker]

Oh yes Subtype.val is definitely not a code smell. I was basically pushing foir the opposite: when dealing with subtypes, use Subtype.valas much as you want, because then it's easier to see that you could replace it by any map f with similar properties! (In this case, docs#Embedding, but it could also be "injective group morphism", docs#Isometry, or whatever properties "inclusion" has in the category you're working with).