topological space stuff

Stream: maths

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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

[Patrick Massot]

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

[Patrick Massot]

But mathlib has induced topologies

[Patrick Massot]

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]

and then deduce something homeo to a compact space is compact

[Reid Barton]

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

[Kevin Buzzard]

Does open_immersion go in the root namespace?

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

embedding seems even more dubious

[Kevin Buzzard]

That's in mathlib now, right?

[Reid Barton]

Yep

[Kevin Buzzard]

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

[Mario Carneiro]

There is finite, but that applies to sets

[Mario Carneiro]

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

[Kenny Lau]

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

there's fintype which isn't a prop

[Kenny Lau]

the prop is nonempty (fintype \a)

[Mario Carneiro]

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]

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]

I have to make a design decision.

[Kevin Buzzard]

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]

I don't care either way

[Kevin Buzzard]

or

[Kevin Buzzard]

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]

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

[Reid Barton]

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]

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]

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

[Andrew Ashworth]

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]

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]

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]

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