[Merged by Bors] - feat(topology): A locally compact Hausdorff space is totally disconnected if and only if it is totally separated

[laughinggas]

We prove that a locally compact Hausdorff space is totally disconnected if and only if it is totally separated.

---

• depends on: [Merged by Bors] - feat(topology): clopens form a topology basis for profinite sets #7671

[PatrickMassot]

This PR can be simplified significantly using https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/topology.lean. I'll try to prioritize PRing that file to mathlib.

[PatrickMassot]

While waiting for #7671 to land I added a quick review. You also need to remove that submodule that you probably never intended to commit.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(topology): clopens form a topology basis for profinite sets #7671

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[PatrickMassot]

Suggested change

	begin
	refine topological_space.is_topological_basis_of_open_of_nhds _ _,
	{ rintros u hu, change (is_clopen u) at hu, apply hu.1, },
	rintros x U memU hU,
	simp only [exists_prop, set.mem_set_of_eq],
	obtain ⟨s, comp, xs, sU⟩ := exists_compact_subset hU memU,
	obtain ⟨t, h, ht, xt⟩ := mem_interior.1 xs,
	set u : set s := (coe : s → H)⁻¹' (interior s) with hu,
	have u_open_in_s : is_open u,
	{ apply is_open.preimage (continuous_subtype_coe) is_open_interior, },
	obtain ⟨V, clopen_in_s, Vx, V_sub⟩ := @compact_exists_clopen_in_open s _
	(subtype.t2_space) (is_compact_iff_compact_space.1 comp) (subtype.totally_disconnected_space)
	⟨x, h xt⟩ u u_open_in_s xs,
	have V_clopen : (set.image (coe : s → H) V) ∈ {Z : set H | is_clopen Z},
	{ change is_clopen (set.image (coe : s → H) V), split,
	{ set v : set u := (coe : u → s)⁻¹' V with hv,
	have : (coe : u → H) = (coe : s → H) ∘ (coe : u → s), { exact rfl, },
	have pre_f : embedding (coe : u → H),
	{ rw this, refine embedding.comp embedding_subtype_coe embedding_subtype_coe, },
	have f' : open_embedding (coe : u → H),
	{ constructor, apply pre_f,
	{ have : set.range (coe : u → H) = interior s,
	{ rw [this, set.range_comp],
	have g : set.range (coe : u → s) = u,
	{ ext z, split,
	{ rw set.mem_range, rintros ⟨y, hy⟩, rw ←hy, apply y.property, },
	rintros hz, rw set.mem_range, use ⟨z, hz⟩, simp, },
	rw [g, subtype.image_preimage_coe],
	apply set.inter_eq_self_of_subset_left interior_subset, },
	rw this, apply is_open_interior, }, },
	have f2 : is_open v,
	{ rw hv, apply is_open.preimage (continuous_subtype_coe) clopen_in_s.1, },
	have f3 : (set.image (coe : s → H) V) = (set.image (coe : u → H) v),
	{ rw [this, hv], symmetry',
	rw set.image_comp, congr, rw [subtype.image_preimage_coe],
	apply set.inter_eq_self_of_subset_left V_sub, },
	rw f3, apply (open_embedding.is_open_map f') v f2, },
	{ apply (closed_embedding.closed_iff_image_closed
	(is_closed.closed_embedding_subtype_coe (is_compact.is_closed comp))).1
	(clopen_in_s).2, }, },
	refine ⟨_, V_clopen, _, _⟩,
	{ simp [Vx, h xt], },
	{ transitivity s,
	{ simp, },
	assumption, },
	end
	begin
	refine is_topological_basis_of_open_of_nhds (λ u hu, hu.1) _,
	rintros x U memU hU,
	obtain ⟨s, comp, xs, sU⟩ := exists_compact_subset hU memU,
	obtain ⟨t, h, ht, xt⟩ := mem_interior.1 xs,
	let u : set s := (coe : s → H)⁻¹' (interior s),
	have u_open_in_s : is_open u := is_open_interior.preimage continuous_subtype_coe,
	let X : s := ⟨x, h xt⟩,
	have Xu : X ∈ u := xs,
	haveI : compact_space s := is_compact_iff_compact_space.1 comp,
	obtain ⟨V : set s, clopen_in_s, Vx, V_sub⟩ := compact_exists_clopen_in_open u_open_in_s Xu,
	have V_clopen : is_clopen ((coe : s → H) '' V),
	{ refine ⟨_, (comp.is_closed.closed_embedding_subtype_coe.closed_iff_image_closed).1
	clopen_in_s.2⟩,
	let v : set u := (coe : u → s)⁻¹' V,
	have : (coe : u → H) = (coe : s → H) ∘ (coe : u → s) := rfl,
	have f0 : embedding (coe : u → H) := embedding_subtype_coe.comp embedding_subtype_coe,
	have f1 : open_embedding (coe : u → H),
	{ refine ⟨f0, _⟩,
	{ have : set.range (coe : u → H) = interior s,
	{ rw [this, set.range_comp, subtype.range_coe, subtype.image_preimage_coe],
	apply set.inter_eq_self_of_subset_left interior_subset, },
	rw this,
	apply is_open_interior } },
	have f2 : is_open v := clopen_in_s.1.preimage continuous_subtype_coe,
	have f3 : (coe : s → H) '' V = (coe : u → H) '' v,
	{ rw [this, image_comp coe coe, subtype.image_preimage_coe,
	inter_eq_self_of_subset_left V_sub] },
	rw f3,
	apply f1.is_open_map v f2 },
	refine ⟨coe '' V, V_clopen, by simp [Vx, h xt], _⟩,
	transitivity s,
	{ simp },
	assumption
	end

I've done some cleanup but this is still more painful than what we could hope for.

[laughinggas]

Thank you for the cleanup. The problem here is that I really need to use both the openness of interior s and the compactness of s, hence I need to work with subsets in each of these respective spaces. Would you be having any suggestion for a better proof that I could try to work on? I was wondering whether thinking in terms of filters might help (I am uncomfortable with them).

[PatrickMassot]

I agree the relevant diagram of spaces is actually not so simple. But on paper we are very good at pretending it is. I don't have a magic solution (otherwise I would have written it).

[laughinggas]

Well, I guess this is the best I can do for now. Thank you for your help!

[PatrickMassot]

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed:

• Build mathlib

[bryangingechen]

Given that this has already passed review, I'll put it back on the queue:
bors r+

@laughinggas Note that the "ready-to-merge" label is added by automation; if you add it yourself, we might think the PR is already on the bors queue and forget about it!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[laughinggas]

Given that this has already passed review, I'll put it back on the queue:
bors r+

@laughinggas Note that the "ready-to-merge" label is added by automation; if you add it yourself, we might think the PR is already on the bors queue and forget about it!

Apologies, I will remember that, in the future!