refactor(topology/constructions): turn cofinite_topology into a typ…

…e synonym (#11967)

Instead of `cofinite_topology α : topological_space α`, define
`cofinite_topology α := α` with an instance
`topological_space (cofinite_topology α) := (old definition)`.

This way we can talk about cofinite topology without using `@` all
over the place.

Also move `homeo_of_equiv_compact_to_t2.t1_counterexample` to
`topology.alexandroff` and prove it for `alexandroff ℕ` and
`cofinite_topology (alexandroff ℕ)`.

src/topology/alexandroff.lean

@@ -57,6 +57,10 @@ instance : has_coe_t X (alexandroff X) := ⟨option.some⟩
 
 instance : inhabited (alexandroff X) := ⟨∞⟩
 
+instance [fintype X] : fintype (alexandroff X) := option.fintype
+
+instance infinite [infinite X] : infinite (alexandroff X) := option.infinite
+
 lemma coe_injective : function.injective (coe : X → alexandroff X) :=
 option.some_injective X
 
@@ -389,4 +393,31 @@ instance [preconnected_space X] [noncompact_space X] : connected_space (alexandr
 { to_preconnected_space := dense_embedding_coe.to_dense_inducing.preconnected_space,
   to_nonempty := infer_instance }
 
+/-- If `X` is an infinite type with discrete topology (e.g., `ℕ`), then the identity map from
+`cofinite_topology (alexandroff X)` to `alexandroff X` is not continuous. -/
+lemma not_continuous_cofinite_topology_of_symm [infinite X] [discrete_topology X] :
+  ¬(continuous (@cofinite_topology.of (alexandroff X)).symm) :=
+begin
+  inhabit X,
+  simp only [continuous_iff_continuous_at, continuous_at, not_forall],
+  use [cofinite_topology.of ↑(default : X)],
+  simpa [nhds_coe_eq, nhds_discrete, cofinite_topology.nhds_eq]
+    using (finite_singleton ((default : X) : alexandroff X)).infinite_compl
+end
+
 end alexandroff
+
+/--
+A concrete counterexample shows that  `continuous.homeo_of_equiv_compact_to_t2`
+cannot be generalized from `t2_space` to `t1_space`.
+
+Let `α = alexandroff ℕ` be the one-point compactification of `ℕ`, and let `β` be the same space
+`alexandroff ℕ` with the cofinite topology.  Then `α` is compact, `β` is T1, and the identity map
+`id : α → β` is a continuous equivalence that is not a homeomorphism.
+-/
+lemma continuous.homeo_of_equiv_compact_to_t2.t1_counterexample :
+  ∃ (α β : Type) (Iα : topological_space α) (Iβ : topological_space β), by exactI
+  compact_space α ∧ t1_space β ∧ ∃ f : α ≃ β, continuous f ∧ ¬ continuous f.symm :=
+⟨alexandroff ℕ, cofinite_topology (alexandroff ℕ), infer_instance, infer_instance,
+  infer_instance, infer_instance, cofinite_topology.of, cofinite_topology.continuous_of,
+  alexandroff.not_continuous_cofinite_topology_of_symm⟩

src/topology/constructions.lean

@@ -110,8 +110,19 @@ theorem nhds_subtype (s : set α) (a : {x // x ∈ s}) :
 nhds_induced coe a
 
 end topα
-/-- The topology whose open sets are the empty set and the sets with finite complements. -/
-def cofinite_topology (α : Type*) : topological_space α :=
+
+/-- A type synonym equiped with the topology whose open sets are the empty set and the sets with
+finite complements. -/
+def cofinite_topology (α : Type*) := α
+
+namespace cofinite_topology
+
+/-- The identity equivalence between `α` and `cofinite_topology α`. -/
+def of : α ≃ cofinite_topology α := equiv.refl α
+instance [inhabited α] : inhabited (cofinite_topology α) :=
+{ default := of default }
+
+instance : topological_space (cofinite_topology α) :=
 { is_open := λ s, s.nonempty → set.finite sᶜ,
   is_open_univ := by simp,
   is_open_inter := λ s t, begin
@@ -129,8 +140,18 @@ def cofinite_topology (α : Type*) : topological_space α :=
     simp [hts]
     end }
 
-lemma nhds_cofinite {α : Type*} (a : α) :
-  @nhds α (cofinite_topology α) a = pure a ⊔ cofinite :=
+lemma is_open_iff {s : set (cofinite_topology α)} :
+  is_open s ↔ (s.nonempty → (sᶜ).finite) := iff.rfl
+
+lemma is_open_iff' {s : set (cofinite_topology α)} :
+  is_open s ↔ (s = ∅ ∨ (sᶜ).finite) :=
+by simp only [is_open_iff, ← ne_empty_iff_nonempty, or_iff_not_imp_left]
+
+lemma is_closed_iff {s : set (cofinite_topology α)} :
+  is_closed s ↔ s = univ ∨ s.finite :=
+by simp [← is_open_compl_iff, is_open_iff']
+
+lemma nhds_eq (a : cofinite_topology α) : 𝓝 a = pure a ⊔ cofinite :=
 begin
   ext U,
   rw mem_nhds_iff,
@@ -141,12 +162,13 @@ begin
     exact ⟨U, subset.rfl, λ h, hU', hU⟩ }
 end
 
-lemma mem_nhds_cofinite {α : Type*} {a : α} {s : set α} :
-  s ∈ @nhds α (cofinite_topology α) a ↔ a ∈ s ∧ sᶜ.finite :=
-by simp [nhds_cofinite]
+lemma mem_nhds_iff {a : cofinite_topology α} {s : set (cofinite_topology α)} :
+  s ∈ 𝓝 a ↔ a ∈ s ∧ sᶜ.finite :=
+by simp [nhds_eq]
 
-end constructions
+end cofinite_topology
 
+end constructions
 
 section prod
 variables [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]

src/topology/homeomorph.lean

@@ -458,46 +458,4 @@ def homeo_of_equiv_compact_to_t2 [compact_space α] [t2_space β]
   continuous_inv_fun := hf.continuous_symm_of_equiv_compact_to_t2,
   ..f }
 
-/--
-A concrete counterexample shows that  `continuous.homeo_of_equiv_compact_to_t2`
-cannot be generalized from `t2_space` to `t1_space`.
-
-Let `α = ℕ` be the one-point compactification of `{1, 2, ...}` with the discrete topology,
-where `0` is the adjoined point, and let `β = ℕ` be given the cofinite topology.
-Then `α` is compact, `β` is T1, and the identity map `id : α → β` is a continuous equivalence
-that is not a homeomorphism.
--/
-lemma homeo_of_equiv_compact_to_t2.t1_counterexample :
-  ∃ (α β : Type) (Iα : topological_space α) (Iβ : topological_space β), by exactI
-  compact_space α ∧ t1_space β ∧ ∃ f : α ≃ β, continuous f ∧ ¬ continuous f.symm :=
-begin
-  /- In the `nhds_adjoint 0 filter.cofinite` topology, a set is open if (1) 0 is not in the set or
-     (2) 0 is in the set and the set is cofinite.  This coincides with the one-point
-     compactification of {1, 2, ...} with the discrete topology. -/
-  let topα : topological_space ℕ := nhds_adjoint 0 filter.cofinite,
-  let topβ : topological_space ℕ := cofinite_topology ℕ,
-  refine ⟨ℕ, ℕ, topα, topβ, _, t1_space_cofinite, equiv.refl ℕ, _, _⟩,
-  { fsplit,
-    rw is_compact_iff_ultrafilter_le_nhds,
-    intros f,
-    suffices : ∃ a, ↑f ≤ @nhds _ topα a, by simpa,
-    by_cases hf : ↑f ≤ @nhds _ topα 0,
-    { exact ⟨0, hf⟩ },
-    { obtain ⟨U, h0U, hU_fin, hUf⟩ : ∃ U : set ℕ, 0 ∈ U ∧ Uᶜ.finite ∧ Uᶜ ∈ f,
-      { rw [nhds_adjoint_nhds, filter.le_def] at hf,
-        push_neg at hf,
-        simpa [and_assoc, ← ultrafilter.compl_mem_iff_not_mem] using hf },
-      obtain ⟨n, hn', hn⟩ := ultrafilter.eq_principal_of_finite_mem hU_fin hUf,
-      rw hn,
-      exact ⟨n, @mem_of_mem_nhds _ topα n⟩ } },
-  { rw continuous_iff_coinduced_le,
-    change topα ≤ topβ,
-    rw gc_nhds,
-    simp [nhds_cofinite] },
-  { intros h,
-    replace h : topβ ≤ topα := by simpa [continuous_iff_coinduced_le, coinduced_id] using h,
-    rw le_nhds_adjoint_iff at h,
-    exact (finite_singleton 1).infinite_compl (h.2 1 one_ne_zero ⟨1, mem_singleton 1⟩) }
-end
-
 end continuous

src/topology/separation.lean

@@ -306,11 +306,11 @@ end
 protected lemma finset.is_closed [t1_space α] (s : finset α) : is_closed (s : set α) :=
 s.finite_to_set.is_closed
 
-lemma t1_space_tfae (α : Type u) [t : topological_space α] :
+lemma t1_space_tfae (α : Type u) [topological_space α] :
   tfae [t1_space α,
     ∀ x, is_closed ({x} : set α),
     ∀ x, is_open ({x}ᶜ : set α),
-    t ≤ cofinite_topology α,
+    continuous (@cofinite_topology.of α),
     ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
     ∀ ⦃x y : α⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
     ∀ ⦃x y : α⦄, x ≠ y → ∃ (U : set α) (hU : is_open U), x ∈ U ∧ y ∉ U,
@@ -331,19 +331,21 @@ begin
     by simp only [← principal_singleton, disjoint_principal_right],
   tfae_have : 8 ↔ 9, from forall_swap.trans (by simp only [disjoint.comm, ne_comm]),
   tfae_have : 1 → 4,
-  { introsI H s hs,
-    simp only [cofinite_topology, ← ne_empty_iff_nonempty, ne.def, ← or_iff_not_imp_left] at hs,
-    rcases hs with rfl | hs,
-    exacts [is_open_empty, compl_compl s ▸ hs.is_closed.is_open_compl] },
-  tfae_have : 4 → 3,
-  { refine λ h x, h _ (λ _, _), simp },
+  { simp only [continuous_def, cofinite_topology.is_open_iff'],
+    rintro H s (rfl|hs),
+    exacts [is_open_empty, compl_compl s ▸ (@set.finite.is_closed _ _ H _ hs).is_open_compl] },
+  tfae_have : 4 → 2,
+    from λ h x, (cofinite_topology.is_closed_iff.2 $ or.inr (finite_singleton _)).preimage h,
   tfae_finish
 end
 
-lemma t1_space_iff_le_cofinite {α : Type*} [t : topological_space α] :
-  t1_space α ↔ t ≤ cofinite_topology α :=
+lemma t1_space_iff_continuous_cofinite_of {α : Type*} [topological_space α] :
+  t1_space α ↔ continuous (@cofinite_topology.of α) :=
 (t1_space_tfae α).out 0 3
 
+lemma cofinite_topology.continuous_of [t1_space α] : continuous (@cofinite_topology.of α) :=
+t1_space_iff_continuous_cofinite_of.mp ‹_›
+
 lemma t1_space_iff_exists_open : t1_space α ↔
   ∀ (x y), x ≠ y → (∃ (U : set α) (hU : is_open U), x ∈ U ∧ y ∉ U) :=
 (t1_space_tfae α).out 0 6
@@ -360,13 +362,12 @@ t1_space_iff_disjoint_pure_nhds.mp ‹_› h
 lemma disjoint_nhds_pure [t1_space α] {x y : α} (h : x ≠ y) : disjoint (𝓝 x) (pure y) :=
 t1_space_iff_disjoint_nhds_pure.mp ‹_› h
 
-@[priority 100] -- see Note [lower instance priority]
-instance t1_space_cofinite {α : Type*} : @t1_space α (cofinite_topology α) :=
-(@t1_space_iff_le_cofinite α (cofinite_topology α)).mpr le_rfl
+instance {α : Type*} : t1_space (cofinite_topology α) :=
+t1_space_iff_continuous_cofinite_of.mpr continuous_id
 
 lemma t1_space_antitone {α : Type*} : antitone (@t1_space α) :=
 begin
-  simp only [antitone, t1_space_iff_le_cofinite],
+  simp only [antitone, t1_space_iff_continuous_cofinite_of, continuous_iff_le_induced],
   exact λ t₁ t₂ h, h.trans
 end