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


Note that I am using tidy in the last line. I don't know if this is too early in the mathlib-tree?

#### Johan Commelin (Oct 18 2018 at 06:41):

If this is the direction you had in mind, I can continue moving stuff from the category folder into this file; and then PR it.

#### Mario Carneiro (Oct 18 2018 at 06:41):

We have functions for transfering a partial order

#### Mario Carneiro (Oct 18 2018 at 06:42):

partial_order.lift

#### Mario Carneiro (Oct 18 2018 at 06:43):

I hope you aren't so attached to using blasty tactics that you are reproving theorems that we already have

#### Mario Carneiro (Oct 18 2018 at 06:43):

in fact, subtype.partial_order is just what you need

#### Mario Carneiro (Oct 18 2018 at 06:44):

ext is subtype.eq

#### Johan Commelin (Oct 18 2018 at 06:44):

Ok, that's fine with me. But about the general direction? Is this what you want?

yes

#### Johan Commelin (Oct 18 2018 at 06:46):

But subtype.ext is not an ext-lemma

#### Johan Commelin (Oct 18 2018 at 06:46):

Should I phrase mine as an ext-lemma, or as an iff?

#### Mario Carneiro (Oct 18 2018 at 06:51):

I'm not saying you shouldn't state it, but it is a proof by reference to subtype.eq

#### Johan Commelin (Oct 18 2018 at 06:51):

Right. But which version should I state? Or both?

#### Mario Carneiro (Oct 18 2018 at 06:52):

extensionality requires the one-directional form

#### Mario Carneiro (Oct 18 2018 at 06:52):

I don't know if it would be better to use set extensionality as well though

#### Mario Carneiro (Oct 18 2018 at 06:53):

so it says forall a, a \in U \lr a \in V

#### Johan Commelin (Oct 18 2018 at 06:54):

ext can chain those together. So I think I'll only do the first step.

Done. See #427.

#### Scott Morrison (Oct 18 2018 at 14:33):

But subtype.ext is not an ext-lemma

I've been wondering about this one --- can we make attribute [extensionality] subtype.eq?

#### Mario Carneiro (Oct 18 2018 at 14:36):

ext can chain them, but you will get x \in U.val instead of x \in U

Last updated: May 09 2021 at 10:11 UTC