Zulip Chat Archive

Stream: maths

Topic: topological space stuff


view this post on Zulip Kevin Buzzard (May 12 2018 at 14:02):

I need some standard topological space arguments. Do we have homeomorphisms and/or open immersions in mathlib yet, and if not then where should I put them? Should a homeomorphism be an equiv or a bijection? (i.e. should I demand a map in the other direction?). I need that something homeomorphic to a compact space is compact -- another thing which a mathematician would not need to supply a proof of because "it's obvious".

view this post on Zulip Mario Carneiro (May 12 2018 at 14:12):

I think Patrick has a definition of homeo. It extended equiv

view this post on Zulip Mario Carneiro (May 12 2018 at 14:13):

of course homeos are isos in the category of top spaces so you are going to find many of the same parametricity things there as with your group iso stuff

view this post on Zulip Patrick Massot (May 12 2018 at 14:57):

@Kevin Buzzard See https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/homeos.lean

view this post on Zulip Patrick Massot (May 12 2018 at 14:57):

It's focused on the group structure on self-homeomorphisms

view this post on Zulip Patrick Massot (May 12 2018 at 14:57):

But mathlib has induced topologies

view this post on Zulip Patrick Massot (May 12 2018 at 14:58):

So I would try to prove that an equiv is a homeo iff both maps induce the same topology on their source as the original one

view this post on Zulip Patrick Massot (May 12 2018 at 14:58):

and then deduce something homeo to a compact space is compact

view this post on Zulip Reid Barton (May 12 2018 at 15:32):

I have a proof of compact s ↔ compact (univ : set (subtype s)) lying around if you need that

view this post on Zulip Kevin Buzzard (May 12 2018 at 17:00):

Does open_immersion go in the root namespace?

view this post on Zulip Reid Barton (May 12 2018 at 17:07):

actually, I basically proved that something homeomorphic to a compact space is compact along the way

view this post on Zulip Reid Barton (May 12 2018 at 17:08):

lemma compact2 [ : topological_space β] {f : α  β} {s : set β} (h : ys, x, f x = y) :
  compact s  @compact α (induced f ) (f ⁻¹' s) :=

view this post on Zulip Reid Barton (May 12 2018 at 17:08):

Currently almost everything related to topological spaces is in the root namespace, which doesn't seem ideal, but surely it would be no worse than having embedding there which it is already.

view this post on Zulip Reid Barton (May 12 2018 at 17:13):

Um, it also just follows from compact_image. :upside_down_face:

view this post on Zulip Kevin Buzzard (May 12 2018 at 17:15):

I have never really engaged with namespaces until recently; I had other things to worry about. I never used the namespace command and never opened anything. But it's all dawning on me now about how it might all work. I am surprised this stuff is piling up in the root namespace, and the longer it's there the more it will hurt when someone decides that compact doesn't apply to all types and hence should be moved to somewhere more topological-spacey.

view this post on Zulip Kevin Buzzard (May 12 2018 at 17:15):

Yes, continuous image of compact is compact will do and probably I will just cheat and use that :-)

view this post on Zulip Reid Barton (May 12 2018 at 17:16):

embedding seems even more dubious

view this post on Zulip Kevin Buzzard (May 12 2018 at 17:16):

That's in mathlib now, right?

view this post on Zulip Reid Barton (May 12 2018 at 17:16):

Yep

view this post on Zulip Kevin Buzzard (May 12 2018 at 17:24):

Is there is_finite somewhere, a prop saying that a type is finite?

view this post on Zulip Mario Carneiro (May 12 2018 at 19:19):

There is finite, but that applies to sets

view this post on Zulip Mario Carneiro (May 12 2018 at 19:19):

open_immersion sounds suitably unambiguously topological that it can go in the root namespace

view this post on Zulip Kenny Lau (May 12 2018 at 19:21):

Is there is_finite somewhere, a prop saying that a type is finite?

there's fintype which isn't a prop

view this post on Zulip Kenny Lau (May 12 2018 at 19:21):

the prop is nonempty (fintype \a)

view this post on Zulip Mario Carneiro (May 12 2018 at 19:21):

For compact2, I would recommend against theorems that have "weird" topologies inserted in the top space component. It makes them very hard to use. Instead, I would want a hypothesis that says that the topology on A is induced from f by the topology on B (i.e. topA = induced f topB, and then you can just use regular typeclass inference to state compact on each side

view this post on Zulip Johan Commelin (May 12 2018 at 19:28):

open_immersion sounds suitably unambiguously topological that it can go in the root namespace

But there are also open immersions in other categories (manifolds, schemes, etc). Wouldn't that create confusion?

view this post on Zulip Kevin Buzzard (May 22 2018 at 16:58):

I have to make a design decision.

view this post on Zulip Kevin Buzzard (May 22 2018 at 16:58):

structure topological_space.open_immersion
  {α : Type*} [ : topological_space α]
  {β : Type*} [ : topological_space β]
  (f : α  β) : Prop :=
(fcont : continuous f)
(finj : function.injective f)
(fopens :  U : set α, is_open U  is_open (f '' U))

view this post on Zulip Kevin Buzzard (May 22 2018 at 16:58):

I don't care either way

view this post on Zulip Kevin Buzzard (May 22 2018 at 16:58):

or

view this post on Zulip Kevin Buzzard (May 22 2018 at 16:58):

def topological_space.open_immersion {X Y : Type u} [tX : topological_space X] [tY : topological_space Y] (φ : X  Y) :=
  continuous φ 
  function.injective φ 
   U : set X, tX.is_open U  tY.is_open (set.image φ U)

view this post on Zulip Kevin Buzzard (May 22 2018 at 16:58):

and don't know enough about how things work to know which choice is best

view this post on Zulip Reid Barton (May 22 2018 at 17:06):

There's already embedding, by the way. So you could also just add is_open (range f) to that and use embedding_open.

view this post on Zulip Reid Barton (May 22 2018 at 17:08):

I doubt it matters much which exact definition you take, as you can write lemmas to prove that other definitions are equivalent. Whether to use a structure or not is probably more important, but depends on what you want to do with it.

view this post on Zulip Reid Barton (May 22 2018 at 17:12):

Oh, your structure is indexed on f also; then it's just a matter of taste I think.

view this post on Zulip Andrew Ashworth (May 22 2018 at 19:23):

I like structures for organizing things that are linked by and statements, I prefer giving names to the hypotheses rather than referring to them as and.left and.left ... etc

view this post on Zulip Sean Leather (May 23 2018 at 06:35):

One thing to consider is how you use simp and @[simp] theorems. With a structure, you have control over what is simplified by carefully choosing where you place your @[simp]s. With nested conjunctions, you are at the mercy of the existing @[simp] theorems. (Of course, you can “work around” this; it's just a matter of how simple your proofs will be.) On the other hand, with conjunctions, you may find that it's easier to work with simplified proofs, given how much already exists to simplify them. (Of course, you can recover this ease by writing @[simp] theorems to do the conversion from the structure to conjunctions. But there goes your control, too.)

view this post on Zulip Reid Barton (May 23 2018 at 10:03):

Another advantage of giving the fields names is that if for some reason you want to change the underlying definition, you can do it in a way that's somewhat transparent by making functions with the names of the old fields.

view this post on Zulip Reid Barton (May 23 2018 at 10:04):

Though this doesn't help if you tend to use pattern matching / implicit constructor syntax


Last updated: May 11 2021 at 17:39 UTC