Topological bases

Stream: new members

[Emiel Lanckriet]

I am trying to proof that if T' is finer than T iff for x in X and each element of the basis B with x in B, there is an element of the basis B' such that x in that element and the new element is a subset of the old one.

I have written this code, but have some trouble reconciling the is_open with the generated_from, I used the generated from instead of topological_space.is_topological_basis because I couldn't seem to specify a topology.

import topology.basic topology.bases topology.metric_space.basic topology.order

open_locale classical filter

open filter set topological_space

example {α} {B B' : set (set α)} {t t' : topological_space α}
    (h : t  = topological_space.generate_from B) (h' : t' = topological_space.generate_from B') :
        t' ≤ t ↔ ∀ (x : α) (b ∈ B), x ∈ b → (∃ b' ∈ B', x ∈ b' ∧ b' ⊆ b) :=
begin
    split,
    {
        intros t'fint x b bB xb,
        use b,
        split,
        {
            rw [h, h'] at t'fint,
            have r := t'fint b,
            sorry
        },
        {
            split, assumption, refl
        },
    },
    {
        intros h U u_open,
        sorry
    },
end

I get stuck at the first sorry where the relevant parts of the environment are:

r: (generate_from B).is_open b ≤ (generate_from B').is_open b
bB : b \in B
\| b \in B'

So, either I should find how to show (generate_from B).is_open b given b \in B or how to formulate this better using topological_space.is_topological_basis.

[Kevin Buzzard]

I don't see why it should be true that if B is a bunch of sets and B' is another bunch of sets, and the topology generated by B' is finer than the topology generated by B, then B is a subset of B'. But this is the goal state at your first sorry:

α: Type ?
BB': set (set α)
tt': topological_space α
h: t = generate_from B
h': t' = generate_from B'
x: α
b: set α
bB: b ∈ B
xb: x ∈ b
t'fint: generate_from B' ≤ generate_from B
⊢ b ∈ B'

So you have made a wrong turn somewhere.

[Kevin Buzzard]

Just before your use statement your tactic state is

α: Type ?
B B': set (set α)
t t': topological_space α
h: t = generate_from B
h': t' = generate_from B'
t'fint: t' ≤ t
x: α
b: set α
bB: b ∈ B
xb: x ∈ b
⊢ ∃ (b' : set α) (H : b' ∈ B'), x ∈ b' ∧ b' ⊆ b

[Kevin Buzzard]

and you tried the tactic use b but we now see that this is over-optimistic. What is the maths proof of what you're trying to do?

[Kevin Buzzard]

PS why not just state your problem as

example {α} {B B' : set (set α)} :
  (generate_from B' ≤ generate_from B) ↔ ∀ (x : α) (b ∈ B), x ∈ b → (∃ b' ∈ B', x ∈ b' ∧ b' ⊆ b) :=

instead of introducing all those t's (actually the notation is pretty useful, maybe this isn't such a good idea)

[Emiel Lanckriet]

Ah, yes, indeed, I mistook the bases for the topologies.

[Kevin Buzzard]

example {α} {B B' : set (set α)} {t t' : topological_space α}
    (h : t  = topological_space.generate_from B) (h' : t' = topological_space.generate_from B') :
        t' ≤ t ↔ ∀ (x : α) (b ∈ B), x ∈ b → (∃ b' ∈ B', x ∈ b' ∧ b' ⊆ b) :=
begin
    split,
    {
        intros t'fint x b bB xb,
        have h2 : t'.is_open b,
        { apply t'fint,
          rw h,
          exact generate_open.basic b bB,
        },

There's a start. This is a proof that b is open for the t' topology.

[Kevin Buzzard]

and perhaps the next three lines should be

        rw h' at h2,
        change generate_open B' b at h2,
        induction h2 with AAA BBB CCC DDD EEE FFF GGG HHH III JJJ KKK LLL MMM,

where I use triple capital letters at first and then I go through looking at all the goals, and change the names of the variables to more appropriate names.

[Kevin Buzzard]

the thing about the topological space generated by a collection of sets is that the definition of the open sets is given recursively. h2 is a proof that something is an open set in the topology generated by B', and there are four ways that that can happen: either it's in B', or it's the whole space, or it's the intersection of two sets we already generated, or it's a union of sets we already generated. I don't know what your maths proof is but if you want to do it from first principles then perhaps you need this inductive step. Of course if you're prepared to use things from the library then it might be easier -- it might well already be in there for all I know.

[Emiel Lanckriet]

The maths proof is quite simple: So, take X \in X and b \in B, then b belongs to t and t \sub t', hence b \in t'. Since t' is generated by B', there is a b' \in B' such that x \in B' \sub B.

[Emiel Lanckriet]

This is the proof taken literally from the book, but of course the last step is harder in formalization.

[Kevin Buzzard]

So then maybe don't do this induction step. Can you give me more details about the claim "Since t' is generated by B', there is a b' \in B' such that x \in B' \sub B". This is your first mention of x, there was an X before, and you don't mention b' at all, so maybe you have some typos in your book? It would be good to find a sentence which makes sense and you can type into Lean, then we can see if we can (a) prove it and (b) use it.

[Kevin Buzzard]

Note that I did the first line of the proof in your book: I showed b was in t' (this is my h2).

[Patrick Massot]

@Emiel Lanckriet what you are trying yo prove is wrong. There is a mismatch between definitions.

[Patrick Massot]

Let me now answer your actual question. You had trouble using is_topological_basis because this predicate, like most of the library, is really meant to work with a single topology on a given type. In technical terms, the topological structure is inferred by a mechanism called "type class instance resolution" that works great but assumes there is only one instance of each class on a given type (this is a simplified story, but good enough for now). This instance resolution is part of elaboration, the process where the proof assistant tries to figure out all the information you didn't explicitly provided. The good news here is that you can always override this elaboration process by prefixing lemma or definition names with a @ and providing as much information as you want (using underscores for stuff you don't want to provide).

[Patrick Massot]

This doesn't give pretty code (lots of @ and _), but it works.

[Patrick Massot]

If you still want an exercise, you can first copy the statements and try to prove it. If this is still difficult, you can also note that the relevant lemmas are mem_basis_subset_of_mem_open, is_open_of_is_topological_basis, mem_basis_subset_of_mem_open (and is_open_iff_forall_mem_open which has nothing to do with bases).

import topology.basic topology.bases topology.metric_space.basic topology.order

open_locale classical filter

open filter set topological_space

example {α : Type*} {B B' : set (set α)} {t t' : topological_space α}
  (h : @is_topological_basis _ t B) (h' : @is_topological_basis _ t' B') :
        t' ≤ t ↔ ∀ (x : α) (b ∈ B), x ∈ b → (∃ b' ∈ B', x ∈ b' ∧ b' ⊆ b) :=
begin
  split,
  { intros H x b b_in x_in,
    apply mem_basis_subset_of_mem_open h' x_in _,
    apply H,
    exact @is_open_of_is_topological_basis _ t _ _ h b_in },
  { intros H b b_op,
    change @is_open _ t' b,
    rw @is_open_iff_forall_mem_open α b t',
    intros x x_in,
    rcases @mem_basis_subset_of_mem_open _ t _ h _ b x_in b_op with ⟨b₁, b₁_in, x_in₁, hb₁b⟩,
    rcases H x _ b₁_in x_in₁ with ⟨b', b'_in, x_in_b', hb'b₁⟩,
    exact ⟨b', subset.trans hb'b₁ hb₁b, @is_open_of_is_topological_basis α t' _ _ h' b'_in, x_in_b'⟩ },
end

[Emiel Lanckriet]

Thanks a lot, I'll take a look at it tomorrow. Right now I am trying to work my way through Topology by Munkres to familiarize with the formalization of topology. Are there better ways?

[Emiel Lanckriet]

Thanks, the proof is easy to understand intuitively, but formalizing it isn't always as easy. I still have the bad habit of kinda brute forcing the proof by just looking at the state after each step and ignoring my mathematical knowledge.

[Patrick Massot]

If you want to understand topology in mathlib you should rather read Bourbaki (or I M James).

[Kevin Buzzard]

Topology turns out to be slicker to formalise with filters than with manipulations of open sets, so many of the proofs in mathlib are done with filters.

[Patrick Massot]

Hopefully https://www.youtube.com/watch?v=hhOPRaR3tx0 can help a bit.

[Emiel Lanckriet]

Ah, yes, I already watched the video before, but I thought that it would be fruitfull to try to translate the things in Munkres to filters. But for this kind of proof the filters didn't seem to be present.

[Emiel Lanckriet]

To go on on the same topic, I am trying to proof that if Y is open in the topolgy on X and U is open on the subspace topology on Y then U is open on the topology on X. I have found the file topology.constructions which says that it has a subspace topology, but I can't find one.

[Patrick Massot]

This is docs#is_open.open_embedding_subtype_coe

[Patrick Massot]

Or even more directly docs#is_open.is_open_map_subtype_coe

[Patrick Massot]

import topology.constructions

example {X: Type*} [topological_space X] {Y : set X} (hY : is_open Y) {U : set Y} {hU : is_open U} :
  is_open ((coe : Y → X) '' U) :=
hY.is_open_map_subtype_coe U hU

[Patrick Massot]

All the difficulty here is in understand set and subtype. See topology exercises in the lftcm2020 repository.

[Emiel Lanckriet]

Thanks a lot, I already looked at lftcm2020 about topology, but I clearly don't understand it all yet.

[Patrick Massot]

I mean doing the exercises, not only watching the intro video.

[Patrick Massot]

And yes, it's not easy.

[Emiel Lanckriet]

No, I mean I have done the exercises a few days ago, but I might take a look at them again, because I feel I didn't get it all and had to peek at the solution a lot.