# Zulip Chat Archive

## Stream: maths

### Topic: topological space stuff

#### 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".

#### Mario Carneiro (May 12 2018 at 14:12):

I think Patrick has a definition of `homeo`

. It extended `equiv`

#### 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

#### Patrick Massot (May 12 2018 at 14:57):

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

#### Patrick Massot (May 12 2018 at 14:57):

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

#### Patrick Massot (May 12 2018 at 14:57):

But mathlib has induced topologies

#### 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

#### Patrick Massot (May 12 2018 at 14:58):

and then deduce something homeo to a compact space is compact

#### 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

#### Kevin Buzzard (May 12 2018 at 17:00):

Does `open_immersion`

go in the root namespace?

#### Reid Barton (May 12 2018 at 17:07):

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

#### Reid Barton (May 12 2018 at 17:08):

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

#### 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.

#### Reid Barton (May 12 2018 at 17:13):

Um, it also just follows from `compact_image`

. :upside_down_face:

#### 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.

#### 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 :-)

#### Reid Barton (May 12 2018 at 17:16):

`embedding`

seems even more dubious

#### Kevin Buzzard (May 12 2018 at 17:16):

That's in mathlib now, right?

#### Reid Barton (May 12 2018 at 17:16):

Yep

#### Kevin Buzzard (May 12 2018 at 17:24):

Is there `is_finite`

somewhere, a prop saying that a type is finite?

#### Mario Carneiro (May 12 2018 at 19:19):

There is `finite`

, but that applies to sets

#### Mario Carneiro (May 12 2018 at 19:19):

`open_immersion`

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

#### 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

#### Kenny Lau (May 12 2018 at 19:21):

the prop is `nonempty (fintype \a)`

#### 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

#### 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?

#### Kevin Buzzard (May 22 2018 at 16:58):

I have to make a design decision.

#### Kevin Buzzard (May 22 2018 at 16:58):

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

#### Kevin Buzzard (May 22 2018 at 16:58):

I don't care either way

#### Kevin Buzzard (May 22 2018 at 16:58):

or

#### 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)

#### Kevin Buzzard (May 22 2018 at 16:58):

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

#### 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`

.

#### 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.

#### 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.

#### 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

#### 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.)

#### 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.

#### 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