Zulip Chat Archive

Stream: maths

Topic: bundled bases

Johan Commelin (Oct 17 2018 at 07:41):

I pushed the results of yesterdays painful efforts to https://github.com/leanprover-community/mathlib/blob/open_set/category_theory/examples/topological_spaces.lean. This wouldn't have been possible without the great help of @Johannes Hölzl
I guess that some of the proofs need to be minimised. I obfuscated them as much as possible, and don't see how to squeeze out more. If someone wants to take a look, please go ahead.
The motivation for these changes is that we want to be able to talk about "sheaves on a basis".

Mario Carneiro (Oct 17 2018 at 18:13):

I think open_set should be unbundled in the topology argument

Johan Commelin (Oct 17 2018 at 18:21):

@Mario Carneiro What do you mean with that?

Johan Commelin (Oct 17 2018 at 18:21):

You want an unbundled version in analysis/topology/blah.lean?

Johan Commelin (Oct 17 2018 at 18:22):

I think we also want the bundled version. But maybe I should first prove things with it, to show that it is useful.

Mario Carneiro (Oct 17 2018 at 19:19):

I mean that for a fixed topological space, @open_set X top_X is a category

Mario Carneiro (Oct 17 2018 at 19:20):

On top of that there is an open_set functor from Top to Type, but that needs its own definition anyway

Mario Carneiro (Oct 17 2018 at 19:21):

er, I think I mean lattice not category, I see you haven't given it a category structure

Mario Carneiro (Oct 17 2018 at 19:22):

so in that case it could indeed move to analysis/topology. I would suggest the name opens for this lattice

Johan Commelin (Oct 17 2018 at 19:22):

It is... every preorder is a category (in mathlib)

Mario Carneiro (Oct 17 2018 at 19:22):

right, but you haven't made any explicit reference to categories in the definition

Johan Commelin (Oct 17 2018 at 19:24):

Hmmm... I don't follow exactly. Do you want to change the definition of open_set? Or do you want to define opens and if so, what should it be?

Johan Commelin (Oct 17 2018 at 19:27):

Also, should we change the definition of open_set X to open_set X := X.str? That is equivalent, and might simplify a lot of the stuff that follows...

Mario Carneiro (Oct 17 2018 at 20:08):

def opens (X : Type*) [topological_space X] : Type* := {s // is_open s}

Mario Carneiro (Oct 17 2018 at 20:10):

I don't understand the idea behind the X.str definition. The point is that open_set X is a type, not a structure

Mario Carneiro (Oct 17 2018 at 20:11):

my proposal is opens as above, and category.opens : Top ⥤ Cat (or some other prefix?) has that as its object part

Mario Carneiro (Oct 17 2018 at 20:13):

although maybe we need more functors than just that because it's properly a 2-functor

Johan Commelin (Oct 18 2018 at 03:58):

@Mario Carneiro So open_set should go asway, and be replaced by opens?
What is wrong with:

def opens (X : Type*) [t : topological_space X] : Type* := subtype t.is_open

That is what I meant with the X.str definition.

Mario Carneiro (Oct 18 2018 at 03:59):

That doesn't typecheck?

Johan Commelin (Oct 18 2018 at 04:03):

Ok, fair enough. I meant subtype t.is_open. I fixed this above.

Mario Carneiro (Oct 18 2018 at 04:04):

that's the same as I wrote modulo eta expansion

Johan Commelin (Oct 18 2018 at 04:04):

Right. So it doesn't matter.

Mario Carneiro (Oct 18 2018 at 04:04):

well, you are also using a different is_open

Johan Commelin (Oct 18 2018 at 04:05):

Aah, and maybe mine is more painful?

Mario Carneiro (Oct 18 2018 at 04:05):

there are fewer lemmas about it

Johan Commelin (Oct 18 2018 at 06:40):

@Mario Carneiro Do you mean you would like to see something like this in analysis/topology/topological_space.lean?

section opens
variable (α)

def opens := {s : set α // _root_.is_open s}

variables {α}

instance : has_coe (opens α) (set α) := { coe := λ U, U.val }

instance : has_subset (opens α) :=
{ subset := λ U V, U.val ⊆ V.val }

instance : has_mem α (opens α) :=
{ mem := λ a U, a ∈ U.val }

@[extensionality] lemma ext {U V : opens α} (h : U.val = V.val) : U = V :=
by cases U; cases V; congr; exact h

instance topological_space.opens.partial_order : partial_order (opens α) := by refine { le := (⊆), .. } ; tidy

end opens