Zulip Chat Archive

Stream: new members

Topic: intersection of sets


Jason KY. (Jun 06 2020 at 14:13):

I am trying to create a set of type set A from another set U : set X by taking its intersection with A where A is something of type set X.
I was able to come up with the following:

import data.set.basic
variables {X : Type*}
instance {A : set X} : has_coe (set X) (set A) :=
⟨λ U, {s |∃ u : X, u  A  U  (s : X) = u}

but this is not very nice to work with so I'm wondering if there is a better way (perhaps already built into mathlib)?

Jalex Stark (Jun 06 2020 at 14:14):

you have A : set X and you want a : set A? that feels wrong

Jalex Stark (Jun 06 2020 at 14:15):

do you really want B : set X and hB : B \sub A?

Jason KY. (Jun 06 2020 at 14:15):

I'm working with subspaces of a topological space so that's what I came up with :/

Jalex Stark (Jun 06 2020 at 14:16):

So A can be promoted to a topological space?

Jalex Stark (Jun 06 2020 at 14:16):

and then you want B to be a set of points in the space A?

Jason KY. (Jun 06 2020 at 14:16):

I made something like

instance {A : set X} : topological_space A :=
{ is_open := λ U,  (V : set X) (H : is_open V), A  V = U,
  is_open_univ := sorry,
  is_open_inter := sorry,
  is_open_sUnion := sorry }

and now I'm trying to show A ∩ V is open with respect to the subspace topology

Jason KY. (Jun 06 2020 at 14:16):

Jalex Stark said:

and then you want B to be a set of points in the space A?

Yeah exactly

Jalex Stark (Jun 06 2020 at 14:17):

can you give the imports to make it a #mwe?

Jason KY. (Jun 06 2020 at 14:17):

Alright, will do one sec

Johan Commelin (Jun 06 2020 at 14:17):

@Jason KY. Something like this can certainly be done, but will probably be painful...

Jalex Stark (Jun 06 2020 at 14:18):

I think "what is the right way to deal with substructures" is an open and active question in algebra-land

Jason KY. (Jun 06 2020 at 14:18):

Is something like this implemented in mathlib? (such as subspaces of topological spaces)?

Johan Commelin (Jun 06 2020 at 14:18):

I suggest that you work with two types A and X, and a function f : A → X. Assume that you have a topology on both types, and assume inducing f.

Jalex Stark (Jun 06 2020 at 14:19):

probably the simplest example is subgroups

Johan Commelin (Jun 06 2020 at 14:19):

There is a lot of stuff in mathlib (about topology)

Jalex Stark (Jun 06 2020 at 14:19):

people say the words "bundled" and "unbundled" a lot when they talk about it

Reid Barton (Jun 06 2020 at 14:19):

Your original definition can be written as λ U, subtype.val \-1' U

Reid Barton (Jun 06 2020 at 14:20):

If you follow Johan's suggestion, I guess you are forced into finding this.

Jason KY. (Jun 06 2020 at 14:20):

Alright, I'll try to do the bundled approach

Jason KY. (Jun 06 2020 at 14:21):

I'll come back if I get stuck again :)

Kevin Buzzard (Jun 06 2020 at 14:21):

Just to remark that Kenny had a terrible time trying to formalise an exercise in Hartshorne of the form "given sheaves on each element U_i of an open cover of X plus some gluing data, make a sheaf on X and prove it has some universal property"

Alex J. Best (Jun 06 2020 at 14:21):

Is

instance  {A : set X} : has_coe (set X) (set A) :=
⟨λ U, λ x, A x  U x

what you want?

Reid Barton (Jun 06 2020 at 14:21):

You wrote ∃ u : X, ... but then one of the conditions on u is that it equal some specific thing (subtype.val s), so the existential is not needed.

Kevin Buzzard (Jun 06 2020 at 14:22):

Kenny's audacious approach was to define a sheaf on U to literally be a sheaf on X, with an implicit (unenforced) promise that you were not to evaluate it on an open subset V of X which was not a subset of X

Jason KY. (Jun 06 2020 at 14:22):

Alex J. Best said:

Is

instance  {A : set X} : has_coe (set X) (set A) :=
⟨λ U, λ x, A x  U x

what you want?

Something like this but I think it will still be hard to work with

Kevin Buzzard (Jun 06 2020 at 14:23):

Mario modified the definition to make it a bit more principled -- he objected to it for some reason (despite not objecting to division by 0 being defined)

Jason KY. (Jun 06 2020 at 14:25):

Kevin Buzzard said:

Kenny's audacious approach was to define a sheaf on U to literally be a sheaf on X, with an implicit (unenforced) promise that you were not to evaluate it on an open subset V of X which was not a subset of X

Are you suggesting it is possible to define a topology on X using the subspace topology of A?

Jason KY. (Jun 06 2020 at 14:26):

I think this approach is a bit controversial :P

Johan Commelin (Jun 06 2020 at 14:27):

@Jason KY. What is your bigger goal?

Johan Commelin (Jun 06 2020 at 14:27):

Do you only want to define a subspace topology, or is there a grand plan on the horizon?

Jason KY. (Jun 06 2020 at 14:28):

My bigger goal is to learn topology by formalising it in lean, but right now I'm trying to show that if a space is Hausdorff, so is its subspaces

Jason KY. (Jun 06 2020 at 14:29):

So that is the reason why I need a the intersection of two set X to be a set A

Johan Commelin (Jun 06 2020 at 14:31):

So, you could prove a more general theorem (which is easier to prove), namely

theorem foobar (X Y : Type) [topological_space X] [topological_space Y] (f : X  Y) (hf : inducing f)
  [t2_space Y] :
  t2_space X :=
sorry

Johan Commelin (Jun 06 2020 at 14:32):

You could then apply it to a subspace and f = subtype.val to recover the "special case".

Jason KY. (Jun 06 2020 at 14:35):

Sorry for stupid question: what does inducing do and where can I find it?

Reid Barton (Jun 06 2020 at 14:36):

This isn't really any easier except that it forces your mental model to match what's happening in Lean.

Jason KY. (Jun 06 2020 at 14:38):

I would hope it is easier than all the different coersions I've been dealing with.

Reid Barton (Jun 06 2020 at 14:38):

It's exactly just callling all of those coercions f.

Reid Barton (Jun 06 2020 at 14:41):

If A : set X then no matter what you are forced in Lean to think of A and X as separate types, related by an injective function A -> X that happens to be called subtype.val, and which is also a coercion so often you don't have to write it explicitly.

Reid Barton (Jun 06 2020 at 14:43):

Johan's suggestion is just work with arbitrary A and X and an injective function f : A -> X--this is easier in the sense that now you've changed the math picture to match the Lean one. From a technical point of view, it's the same.

Reid Barton (Jun 06 2020 at 14:44):

Alex J. Best said:

Is

instance  {A : set X} : has_coe (set X) (set A) :=
⟨λ U, λ x, A x  U x

what you want?

Actually it's just

instance  {A : set X} : has_coe (set X) (set A) :=
⟨λ U, λ x, U x

I think.

Reid Barton (Jun 06 2020 at 14:45):

Well, these are equal but x : A so A x holds automatically.

Jason KY. (Jun 06 2020 at 14:46):

Right, I think I understand. I think I will first prove that if f is a continuous injective map from X to Y and Y is Hausdorff then so is X (it was on my agenda to prove so anyway :)) and then the subspace lemma follows directly as Johan's suggestion

Jason KY. (Jun 06 2020 at 14:46):

I just have to show my coercion is continuous I suppose

Kevin Buzzard (Jun 06 2020 at 17:45):

And it will be because the subspace topology is defined to be the smallest topology which makes the inclusion map continuous

Kevin Buzzard (Jun 06 2020 at 18:04):

Exercise: Let X be a topological space and let X to Y be a surjection of sets. Construct some kind of topology on Y which makes the map continuous and is the correct topology


Last updated: Dec 20 2023 at 11:08 UTC