Zulip Chat Archive

Stream: maths

Topic: Hausdorffification


view this post on Zulip Kenny Lau (Oct 18 2018 at 07:53):

import analysis.topology.continuity

universes u v

variables (α : Type u) [t : topological_space α]
include t

def Hausdorffification.setoid : setoid α :=
{ r := λ x y,  (s : setoid α) [t2_space (quotient s)], @setoid.r α s x y,
  iseqv := ⟨λ _ s _, s.2.1 _, λ _ _ H s ht2, s.2.2.1 (@H s ht2),
    λ _ _ _ H1 H2 s ht2, s.2.2.2 (@H1 s ht2) (@H2 s ht2) }

local attribute [instance] Hausdorffification.setoid

@[reducible] def Hausdorffification : Type u :=
quotient (Hausdorffification.setoid α)

instance Hausdorffification.t2_space :
  t2_space (Hausdorffification α) :=
{ t2 := λ x y, quotient.induction_on₂ x y $ λ m n H,
    begin
      letI := classical.prop_decidable,
      simp only [ne.def, quotient.eq, (), setoid.r, not_forall] at H,
      rcases H with r, ht2, H, resetI,
      let f : Hausdorffification α  quotient r,
      { refine λ e, quotient.lift_on' e quotient.mk _,
        intros a b H, apply quotient.sound, apply H },
      have hf : continuous f,
      { intros s hs,
        change is_open (quotient.mk ⁻¹' _),
        rw  set.preimage_comp,
        exact hs },
      rcases t2_separation (mt quotient.exact H) with u, v, h1, h2, h3, h4, h5,
      refine ⟨_, _, hf _ h1, hf _ h2, h3, h4, set.eq_empty_of_subset_empty _⟩,
      exact λ x H, set.eq_empty_iff_forall_not_mem.1 h5 (f x) H
    end }

view this post on Zulip Kenny Lau (Oct 18 2018 at 07:54):

Is there any way to do this constructively?

view this post on Zulip Johannes Hölzl (Oct 18 2018 at 07:56):

usually the relation is defined as "define $a \sim b$ if any open set containing $a$ intersects any open set containing $b$". maybe this works constructively?

view this post on Zulip Kenny Lau (Oct 18 2018 at 07:57):

you need to iterate that transfinitely many times to have a T2 space

view this post on Zulip Kenny Lau (Oct 18 2018 at 07:57):

and that would involve induction-recursion (is the name right?) which is stronger than Lean

view this post on Zulip Mario Carneiro (Oct 18 2018 at 07:58):

Why? What is the idea behind this definition

view this post on Zulip David Michael Roberts (Oct 18 2018 at 07:58):

https://ncatlab.org/nlab/show/Hausdorff+space#in_constructive_mathematics

view this post on Zulip Mario Carneiro (Oct 18 2018 at 07:59):

by the way, I think that the definition of T2 in mathlib is contrapositive of the right one

view this post on Zulip Mario Carneiro (Oct 18 2018 at 08:00):

which apparently nLab calls "weakly Hausdorff"

view this post on Zulip Mario Carneiro (Oct 18 2018 at 08:03):

also, I don't see any nonconstructivity in that proof

view this post on Zulip Kenny Lau (Oct 18 2018 at 13:20):

I used not_forall

view this post on Zulip Kenny Lau (Oct 18 2018 at 15:14):

Why? What is the idea behind this definition

quotient a lot until you get a T2 space, but don't quotient more than necessary

view this post on Zulip Mario Carneiro (Oct 18 2018 at 15:15):

what's the problem with Johannes's definition

view this post on Zulip Kenny Lau (Oct 18 2018 at 15:15):

that it doesn't produce a T2 space

view this post on Zulip Mario Carneiro (Oct 18 2018 at 15:15):

why

view this post on Zulip Mario Carneiro (Oct 18 2018 at 15:16):

like where does the proof break down

view this post on Zulip Kenny Lau (Oct 18 2018 at 15:16):

https://topospaces.subwiki.org/wiki/Hausdorffization#Example_to_illustrate_why_one_step_isn.27t_enough

view this post on Zulip Mario Carneiro (Oct 18 2018 at 18:18):

you need to iterate that transfinitely many times to have a T2 space
and that would involve induction-recursion (is the name right?) which is stronger than Lean

You don't need proof principles stronger than lean. You just need to know that the process stops eventually, by bounding the space of possible relations

view this post on Zulip Mario Carneiro (Oct 18 2018 at 18:21):

although topospaces wiki is shamefully cavalier about defining an ordinal indexed sequence of topological spaces with direct limits and then just saying "take hh^\infty" as if that were well defined

view this post on Zulip Mario Carneiro (Oct 18 2018 at 18:23):

In lean, it is an interesting example of an inductive predicate that is positive but not strictly positive

view this post on Zulip Mario Carneiro (Oct 18 2018 at 18:29):

inductive hausify : α → α → Prop
| refl : ∀ x, hausify x x
| trans : ∀ x y z, hausify x y → hausify y z → hausify x z
| haus : ∀x y, (∀ u v : set α, is_open u → is_open v →
   x ∈ u → y ∈ v → ∃ z w, z ∈ u ∧ w ∈ v ∧ hausify z w) → hausify x y

This definition is monotone but not syntactically

view this post on Zulip Mario Carneiro (Oct 18 2018 at 18:39):

So here's how you can do the transfinite induction construction:

inductive hausify1 (haus : α  α  Prop) : α  α  Prop
| trans :  x y z, hausify1 x y  hausify1 y z  hausify1 x z
| haus : x y, ( u v : set α, is_open u  is_open v 
   x  u  y  v   z w, z  u  w  v  haus z w)  hausify1 x y

inductive hausify_transfinite : (α  α  Prop)  Prop
| zero : hausify_transfinite eq
| succ :  r, hausify_transfinite r  hausify_transfinite (hausify1 r)
| lim :  R : set (α  α  Prop), ( r  R, hausify_transfinite r) 
  hausify_transfinite (hausify1 (λ x y,  r  R, (r : α  α  Prop) x y))

def hausify (x y : α) : Prop :=  r, hausify_transfinite r  r x y

Needless to say I prefer your definition

view this post on Zulip Kenny Lau (Oct 18 2018 at 19:30):

I prefer yours

view this post on Zulip Mario Carneiro (Oct 18 2018 at 19:40):

this whole construction is doing something similar to yours, quotienting by all relations that are hausdorffish

view this post on Zulip Mario Carneiro (Oct 18 2018 at 19:41):

it's easier to say t2_space (quotient r) than all this

view this post on Zulip Kenny Lau (Oct 18 2018 at 22:04):

can you define ε_0 using that?

view this post on Zulip Kenny Lau (Oct 18 2018 at 22:04):

oh wait you already defined ordinal notations inductively

view this post on Zulip Kenny Lau (Oct 18 2018 at 22:05):

wait no I'm confused

view this post on Zulip Mario Carneiro (Oct 18 2018 at 22:22):

This allows you to do transfinite iteration over a fixed type

view this post on Zulip Mario Carneiro (Oct 18 2018 at 22:23):

the key is the fact that it is all taking place in one complete lattice

view this post on Zulip Kenny Lau (Oct 18 2018 at 22:23):

I see

view this post on Zulip Kenny Lau (Oct 18 2018 at 22:23):

So you can't define ordinals using this zero-lim-succ

view this post on Zulip Mario Carneiro (Oct 18 2018 at 22:24):

You have to build an inductive Type to do that

view this post on Zulip Mario Carneiro (Oct 18 2018 at 22:24):

by the way epsilon_0 is the supremum of all ordinals with ordinal_notation

view this post on Zulip Mario Carneiro (Oct 18 2018 at 22:24):

in case you wanted to define it

view this post on Zulip Mario Carneiro (Oct 18 2018 at 22:25):

It is possible to extend ordinal notations to epsilon_0 and beyond using the veblen hierarchy, but I don't think anyone around here cares about large countable ordinals

view this post on Zulip Mario Carneiro (Oct 18 2018 at 22:27):

I think we also have what we need to define omega_1^CK using computable functions

view this post on Zulip Kevin Buzzard (Oct 19 2018 at 06:58):

Is this a reflection?


Last updated: May 12 2021 at 06:14 UTC