# 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

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?

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

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.

#### Johan Commelin (Oct 18 2018 at 07:29):

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