# 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):

#### 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 $h^\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: May 12 2021 at 06:14 UTC