Zulip Chat Archive

Stream: maths

Topic: Hausdorffification


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 }

Kenny Lau (Oct 18 2018 at 07:54):

Is there any way to do this constructively?

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?

Kenny Lau (Oct 18 2018 at 07:57):

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

Kenny Lau (Oct 18 2018 at 07:57):

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

Mario Carneiro (Oct 18 2018 at 07:58):

Why? What is the idea behind this definition

David Michael Roberts (Oct 18 2018 at 07:58):

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

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

Mario Carneiro (Oct 18 2018 at 08:00):

which apparently nLab calls "weakly Hausdorff"

Mario Carneiro (Oct 18 2018 at 08:03):

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

Kenny Lau (Oct 18 2018 at 13:20):

I used not_forall

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

Mario Carneiro (Oct 18 2018 at 15:15):

what's the problem with Johannes's definition

Kenny Lau (Oct 18 2018 at 15:15):

that it doesn't produce a T2 space

Mario Carneiro (Oct 18 2018 at 15:15):

why

Mario Carneiro (Oct 18 2018 at 15:16):

like where does the proof break down

Kenny Lau (Oct 18 2018 at 15:16):

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

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

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

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

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

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

Kenny Lau (Oct 18 2018 at 19:30):

I prefer yours

Mario Carneiro (Oct 18 2018 at 19:40):

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

Mario Carneiro (Oct 18 2018 at 19:41):

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

Kenny Lau (Oct 18 2018 at 22:04):

can you define ε_0 using that?

Kenny Lau (Oct 18 2018 at 22:04):

oh wait you already defined ordinal notations inductively

Kenny Lau (Oct 18 2018 at 22:05):

wait no I'm confused

Mario Carneiro (Oct 18 2018 at 22:22):

This allows you to do transfinite iteration over a fixed type

Mario Carneiro (Oct 18 2018 at 22:23):

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

Kenny Lau (Oct 18 2018 at 22:23):

I see

Kenny Lau (Oct 18 2018 at 22:23):

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

Mario Carneiro (Oct 18 2018 at 22:24):

You have to build an inductive Type to do that

Mario Carneiro (Oct 18 2018 at 22:24):

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

Mario Carneiro (Oct 18 2018 at 22:24):

in case you wanted to define it

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

Mario Carneiro (Oct 18 2018 at 22:27):

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

Kevin Buzzard (Oct 19 2018 at 06:58):

Is this a reflection?


Last updated: Dec 20 2023 at 11:08 UTC