subsets of discrete

Stream: new members

[Damiano Testa]

Dear All,

since it seems that today I am fighting with sets in Lean, I would like to know if anyone can suggest a simple proof of the lemma below. I have a truly terrible proof, that you can see below!

More generally, I imagine that there will be a "lattice of discrete topological subspaces" in Lean, but I was not able to find it.

Thanks!

import topology.separation

lemma discrete_topology.of_subset {X : Type*} [topological_space X] {s t : set X}
  (ds : discrete_topology s) (ts : t ⊆ s) :
  discrete_topology t :=
begin
  rw [← singletons_open_iff_discrete, set_coe.forall] at ⊢ ds,
  intros a ta,
  rcases ds a (ts ta) with ⟨sa, osa, csa⟩,
  refine ⟨sa, osa, _⟩,
  obtain F : coe '' (coe ⁻¹' sa) = coe '' _ := congr_arg (λ ss, (coe : {x // x ∈ s} → X) '' ss) csa,
  rw [set.image_singleton, subtype.image_preimage_coe, subtype.coe_mk] at F,
  have sat : sa ∩ t ⊆ sa ∩ s := set.inter_subset_inter_right sa ts,
  have sata : sa ∩ t = {a},
  { refine set.subset.antisymm (λ x hx, _) (λ x (hx : x = a), _),
    { rw ← F,
      exact sat hx },
    { subst hx,
      refine ⟨set.mem_of_mem_inter_left (_ : x ∈ sa ∩ s), ta⟩,
      exact set.singleton_subset_iff.mp (set.subset.antisymm_iff.mp F.symm).1 } },
  ext1 x,
  cases x with x xt,
  suffices : x ∈ sa ↔ x = a, by simpa only [set.mem_singleton_iff],
  refine ⟨λ xa, _, _⟩,
  { have : x ∈ sa ∩ t := ⟨xa, xt⟩,
    rwa sata at this },
  { rintros rfl,
    refine set.singleton_subset_iff.mp (λ el elx, _),
    exact set.mem_of_mem_inter_left ((set.subset.antisymm_iff.mp sata.symm).1 elx) }
end

[Kenny Lau]

import topology.separation

lemma discrete_topology.of_subset {X : Type*} [topological_space X] {s t : set X}
  (ds : discrete_topology s) (ts : t ⊆ s) :
  discrete_topology t :=
begin
  rw [← singletons_open_iff_discrete, set_coe.forall] at ⊢ ds,
  intros a ta,
  specialize ds a (ts ta),
  rw is_open_induced_iff at ⊢ ds,  -- don't just unfold
  rcases ds with ⟨sa, osa, csa⟩,
  refine ⟨sa, osa, _⟩,
  rw [← (function.injective.image_injective subtype.coe_injective).eq_iff,
      set.image_preimage_eq_inter_range, subtype.range_coe, set.image_singleton,
      subtype.coe_mk] at csa ⊢,
  rw [← set.inter_eq_self_of_subset_right ts, ← set.inter_assoc, csa],
  exact set.subset.antisymm (set.inter_subset_left _ _)
    (set.singleton_subset_iff.2 ⟨rfl, ta⟩)
end

[Patrick Massot]

Are you really sure you need this and can't get away with types instead of sets?

[Patrick Massot]

It seems we are missing discrete space API anyway.

import topology.separation

lemma truc {X : Type*} [tX : topological_space X] {s t : set X} (ts : t ⊆ s) :
(subtype.topological_space : topological_space t) = (subtype.topological_space : topological_space s).induced (set.inclusion ts) :=
begin
  change tX.induced ((coe : s → X) ∘ (set.inclusion ts)) = topological_space.induced (set.inclusion ts) (tX.induced _),
  rw ← induced_compose,
end

lemma discrete_topology_iff_nhds {X : Type*} [topological_space X] :
  discrete_topology X ↔ (nhds : X → filter X) = pure :=
begin
  split,
  { introI hX,
    exact nhds_discrete X },
  { intro h,
    constructor,
    apply eq_of_nhds_eq_nhds,
    simp [h, nhds_bot] }
end

lemma induced_bot {X Y : Type*} {f : X → Y} (hf : function.injective f) :
  topological_space.induced f ⊥ = ⊥ :=
eq_of_nhds_eq_nhds (by simp [nhds_induced, ← set.image_singleton, hf.preimage_image, nhds_bot])

lemma discrete_topology_induced {X Y : Type*} [tY : topological_space Y] [discrete_topology Y]
  {f : X → Y} (hf : function.injective f) : @discrete_topology X (topological_space.induced f tY) :=
begin
  constructor,
  rw discrete_topology.eq_bot Y,
  exact induced_bot hf
end

lemma discrete_topology.of_subset {X : Type*} [topological_space X] {s t : set X}
  (ds : discrete_topology s) (ts : t ⊆ s) :
  discrete_topology t :=
begin
  rw [truc ts, ds.eq_bot],
  exact {eq_bot := induced_bot (set.inclusion_injective ts)}
end

[Damiano Testa]

Dear Kenny and Patrick,

thank you so much for your proofs!

Kenny -- I really enjoy seeing how you can get Lean to do what you want!

Patrick -- you are right that I got stuck in some weird type-theory issue with sets and a strange up-arrow with a horizontal line below it. I am happy to see different solutions and will now take some time going through yours!

On a separate note, I had already struggled to use the discrete_topology stuff when mixing it with finiteness. I am now hoping to be able to prove that the intersection of a compact subset with a discrete subset of a topological space is finite. While I found a lemma that claims exactly this, I have yet been unable to use it. I hope that with these hints, I will manage it!

Thank you so much again!

[Damiano Testa]

Patrick, I like your "API proof"! In particular, I find the line

  rw [topological_space.subset_trans ts, ds.eq_bot],

in your proof of discrete_topology.of_subset really informative for how type theory works. I had realized that I was mostly playing around with coercions, but I had no idea how to really deal with them!

[Damiano Testa]

Also, if you want, I can PR some of these lemmas. I also added some comments to them, but I do not understand the one below, since I have never seen pure before and I do not know what it means.

Is what I wrote a reasonable description?

/-- I imagine that this lemma characterizes discrete topological spaces as those having
every as a neighbourhood of its points. -/
lemma discrete_topology_iff_nhds {X : Type*} [topological_space X] :
  discrete_topology X ↔ (nhds : X → filter X) = pure :=

[Damiano Testa]

I went ahead and made a PR: #6570.

[Kevin Buzzard]

filter is a monad. The best introduction I have ever read for these is in a little-known pdf called Programming in Lean which is probably out of date when it comes to the code but which in 2017 was basically one of two pdf sources for learning about lean, the other one being TPIL. Monads are functions from Type to Type with some extra structure which makes them useful for programming or something. Examples are option, list, set and filter. The API for monads involves some standard names like pure and bind which are data (ie definitions) but if you know the types of the data you can usually guess what the definitions are, like us mathematicians say "the complexes are defined to be R^2" and then we say "the complexes are a field" but then the user has to guess what 0,1,+,-,* are. For a monad m there is pure : X -> m X (which is usually easy) and bind : m (m X) -> m X which is usually more fun and is often some sort of concatenation or union, and there are probably some axioms but I forgot them (and whether there are axioms might depend on whether you're a mathematician or a computer scientist). I think that pure is like the identity in a monoid and bind is like multiplication.

For lists, pure x will just be the list [x] and bind L will take a list of lists and just concatenate them. For filters, pure x will just be the principal filter generated by the set {x}.

A topological space is determined by its neighborhood filters. For me recently a really helpful mental model of a filter on X is that it is a generalized subset of X. The neighborhood filter of a point p should be thought of as the infinitesimal open neighbourhood of p, containing all the points infinitely close to p which Isaac Newton wondered about when he was developing calculus but which ultimately were rejected in the 19th century model of the real numbers which we use today. There's an inequality on filters which extends inclusion of subsets. Any subset of X is a filter on X or more precisely corresponds to a filter on X, namely the principal filter associated to this subset. No doubt this is a morphism of monads, if such a concept exists. If X is a topological space then you can easily recover the topology from the neighbourhood filter function: a set U is open iff for every x in U, the neighborhood filter N x is a subset of U. This corresponds to Newton's intuition. Saying that the neighborhood filter is pure just then says that U is open iff for every x in U we have that {x} is a subset of U, ie no extra condition.

[Mario Carneiro]

I think that pure is like the identity in a monoid and bind is like multiplication.

This is how I remember the monad axioms: just pretend it's a monoid, and play type tetris with the monoid axioms

[Damiano Testa]

Ok, this clarifies the meaning of pure... a little!

Your generalized subsets seem close to germs to me: something that looks like an "inverse limit" in the making!

[Kevin Buzzard]

You should read the monad chapter of PIL Damiano. Pure for a concrete monad like filter is just like multiplication in a concrete field -- the definition depends on the field.

[Damiano Testa]

Kevin, I will take a look, thanks for the suggestion!

[Kevin Buzzard]

(deleted)

[Yakov Pechersky]

Kevin, your "something" is called join in generality, and in Lean, for an arbitrary monad, is called mjoin. Additionally, list.join and option.join are also defined, and lemmas are usually about them and not the more general mjoin. The same is true for >>= (read as bind).

[Yakov Pechersky]

The pure actually comes from a generalization of monads: applicative functors. The naming choice for pure for monads is really unfortunate, and I won't even mention it here because it is quite confusing in a programming language context.

[Adam Topaz]

https://github.com/leanprover-community/mathlib/blob/02251b1ed3544ae658f687eb332f7627fff47f57/src/category_theory/monad/equiv_mon.lean#L108

(sorry)

[Alex J. Best]

One really fun algebro-geometric example of a monad is given by taking the albanese variety of a pointed variety to get another pointed variety, then pure is the albanese map and the join is the natural map $Alb(Alb(X)) \to Alb(X)$ you get by applying the universal property to the identity map. https://mathoverflow.net/questions/247104/is-forming-the-albanese-variety-a-monad

[Damiano Testa]

One topology that I had never considered is the co-discrete topology: closed sets are, beside the whole space, the subsets whose induced topology is discrete. In a sequentially compact space, this should be simply the cofinite topology, but in general they are different.

This really is a topology, right? A proof-checking community is a good place to ask these questions, I guess!

[Kevin Buzzard]

I'm not so sure. Any one-point subset is discrete but I don't see why the union of two one-point subsets should be discrete in a random non-Hausdorff topological space.

[Damiano Testa]

You are right, Kevin, I had Hausdorff spaces in mind: the spectrum of a DVR is a counterxample!

[Damiano Testa]

E.g. a two-point space, whose topology is neither \top nor \bot works.

[Damiano Testa]

Still, in a Hausdorff space, the co-discrete topology may make sense and I had never thought about it!

[Kevin Buzzard]

How do you prove that a union of two discrete subspaces is discrete? Take for example the union of {1/n, n>0 an integer} and {0} in the reals.

[Damiano Testa]

Kevin, you are right: I had never heard of the co-discrete topology, since it does not make sense!