intersection of sets

Stream: new members

[Jason KY.]

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]

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

[Jalex Stark]

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

[Jason KY.]

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

[Jalex Stark]

So A can be promoted to a topological space?

[Jalex Stark]

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

[Jason KY.]

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.]

Jalex Stark said:

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

Yeah exactly

[Jalex Stark]

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

[Jason KY.]

Alright, will do one sec

[Johan Commelin]

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

[Jalex Stark]

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

[Jason KY.]

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

[Johan Commelin]

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]

probably the simplest example is subgroups

[Johan Commelin]

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

[Jalex Stark]

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

[Reid Barton]

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

[Reid Barton]

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

[Jason KY.]

Alright, I'll try to do the bundled approach

[Jason KY.]

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

[Kevin Buzzard]

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]

Is

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

what you want?

[Reid Barton]

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]

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.]

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]

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.]

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.]

I think this approach is a bit controversial :P

[Johan Commelin]

@Jason KY. What is your bigger goal?

[Johan Commelin]

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

[Jason KY.]

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.]

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

[Johan Commelin]

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]

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

[Jason KY.]

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

[Reid Barton]

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

[Jason KY.]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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

[Jason KY.]

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.]

I just have to show my coercion is continuous I suppose

[Kevin Buzzard]

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

[Kevin Buzzard]

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