Alternate T2

Author: robertmaxton42

Mathlib/Topology/Category/Lifting/Defs.lean

@@ -181,6 +181,11 @@ lemma «exists» {p : Codiscrete2 → Prop} :
 
 lemma ne : Codiscrete2.zero ≠ Codiscrete2.one := by simp [ULift.ext_iff, Codiscrete2]
 
+/-- Construct a continuous map into `Codiscrete2` from an arbitrary set. -/
+@[simps]
+def hom {X} [TopologicalSpace X] (s : Set X) [DecidablePred (· ∈ s)] : C(X, Codiscrete2) where
+  toFun x := if x ∈ s then .one else .zero
+
 /-- For any continuous map `f : C(Codiscrete2, X)`, the points `f .zero` and `f .one` are
 inseparable. (For the definition witnessing that this condition is sufficient to construct a
 continuous map, see `Codiscrete2.homOfInseparable`.) -/
@@ -189,6 +194,7 @@ lemma inseparable {X : TopCat} (f : C(Codiscrete2, X)) : Inseparable (f .zero) (
 
 /-- A continuous map out of `Codiscrete2` can be made from any pair of inseparable points.
 (For the fact that any such map is of this form, see `Codiscrete2.inseparable`.) -/
+@[simps]
 def homOfInseparable {X : TopCat} {x y : X} (hxy : Inseparable x y) : C(Codiscrete2, X) where
   toFun | .zero => x | .one => y
   continuous_toFun := by

Mathlib/Topology/Category/Lifting/Separation.lean

@@ -9,6 +9,7 @@ public import Mathlib.CategoryTheory.Limits.Shapes.RegularMono
 public import Mathlib.Topology.Category.TopCat.Limits.Pullbacks
 public import Mathlib.Topology.Category.Lifting.Defs
 public import Mathlib.Topology.UrysohnsLemma
+public import Mathlib.Topology.SeparatedMap
 
 import Mathlib.Tactic.TautoSet
 
@@ -253,6 +254,7 @@ theorem of_extend (extend : (f : of Discrete2 ⟶ X) → [Mono f] → X ⟶ of O
       simp
     · apply Disjoint.preimage; simp
 
+
 /-- A space `X` is `T2` iff every mono from `Discrete2` to `X` has the left lifting property
 against `terminal.from O2C1`.
 
@@ -270,7 +272,6 @@ def llp : T2Space X ↔ ∀ (χ : of Discrete2.{u} ⟶ X) [Mono χ], χ ⧄ term
                 ((isoOfHomeo Discrete2.swap).inv ≫ χ) (terminal.from (of O2C1.{u})) τ := by
             constructor; exact terminal.hom_ext _ _
           specialize this _ (mono_comp _ χ) sq' (by simpa using h₀) (by simp [h₀₁])
-          let l := sq'.lift
           apply CommSq.HasLift.mk'; use sq'.lift
           · apply IsIso.epi_of_iso (isoOfHomeo Discrete2.swap).inv |>.left_cancellation
             rw [← Category.assoc, sq'.fac_left]
@@ -324,6 +325,69 @@ instance [T2Space X] (χ : of Discrete2.{u} ⟶ X) [Mono χ] :
     HasLiftingProperty χ (terminal.from (of O2C1.{u})) :=
   llp.mp ‹_› χ
 
+open Function in
+open scoped Classical in
+/-- Alternate characterization: a space `X` is `T2` iff `ContinuousMap.diagonal X`
+lifts against `Codiscrete2.hom { N2C1.left }`. -/
+theorem llp' : T2Space X ↔
+    ofHom (.diagonal X) ⧄ ofHom (Codiscrete2.hom { N2C1.left }) where
+  mp _ :=
+  { sq_hasLift {ι τ} sq := by
+      apply CommSq.HasLift.mk';
+      fconstructor
+      · refine
+          ofHom ⟨extend (ContinuousMap.diagonal X) ι (if τ · = .zero then .right else .left), ?_ ⟩
+        rw [N2C1.basis.continuous_iff]
+        rintro _ (rfl | rfl)
+        · simp
+        · have zero_compl : ({N2C1.left, N2C1.right}ᶜ : Set N2C1) = {N2C1.zero} := by
+            ext ⟨⟩ <;> simp
+          rw [← isClosed_compl_iff, ← preimage_compl, zero_compl,
+          IsClosedEmbedding.diagonal.isClosed_iff_preimage_isClosed, ← preimage_comp,
+          extend_comp ContinuousMap.diagonal_injective]
+          · exact N2C1.isClosed_zero.preimage ι.hom.continuous
+          · intro (x, y) h
+            contrapose! h
+            replace h : ¬∃ z, (ContinuousMap.diagonal X z) = (x, y) := by simpa using h
+            simp [extend_apply' _ _ _ h]
+            grind
+      · rw [← ofHom_comp, ContinuousMap.comp]
+        simp [extend_comp ContinuousMap.diagonal_injective]
+        rfl
+      · ext ⟨x, y⟩
+        rcases em (x = y) with (rfl | hxy)
+        · rw [show (x, x) = ContinuousMap.diagonal X x by rfl]
+          have := (elementwise_of% sq.w) x
+          simp at this
+          simp [-ContinuousMap.diagonal_apply, ContinuousMap.diagonal_injective.extend_apply]
+          simp [this]
+        · replace hxy : ¬∃ z, (ContinuousMap.diagonal X z) = (x, y) := by simpa using hxy
+          have {z} : ¬z = Codiscrete2.zero ↔ Codiscrete2.one = z := by cases z <;> grind
+          simp only [TopCat.hom_comp, hom_ofHom, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
+            extend_apply' _ _ _ hxy, Codiscrete2.hom_apply, ite_eq_right_iff,
+            reduceCtorEq, imp_false, mem_singleton_iff, ULift.down_inj]
+          split_ifs with h₀ <;> first | rwa [this] at h₀ | simp_all }
+  mpr h := by
+    have hsq := h.sq_hasLift (f := ofHom <| .const X N2C1.zero)
+      (g := ofHom <| Codiscrete2.hom (diagonal X)ᶜ) ⟨by ext; simp⟩
+    let χ := CommSq.lift (hsq := hsq)
+    rw [t2_iff_isClosed_diagonal]
+    convert N2C1.isClosed_zero.preimage χ.hom.continuous
+    ext ⟨x, y⟩
+    constructor
+    · rintro ⟨⟩
+      unfold χ
+      have := (elementwise_of% CommSq.fac_left (hsq := hsq)) x
+      rw [show (x, x) = ContinuousMap.diagonal X x by rfl]
+      simp at this; simp [this]
+    · rw [mem_preimage, mem_singleton_iff]
+      intro hχ
+      have := (elementwise_of% CommSq.fac_right (hsq := hsq)) (x, y)
+      apply_fun ofHom (Codiscrete2.hom {N2C1.left}) at hχ
+      simp_rw [χ, this] at hχ
+      simp [Codiscrete2.ne.symm] at hχ; simp [hχ]
+
+
 /-- A `T2` space `X` extends every mono from `Discrete2` into one to `O2C1`. -/
 noncomputable def extend [T2Space X] (χ : of Discrete2 ⟶ X) [Mono χ] : X ⟶ of O2C1 :=
   CommSq.lift (hsq := (llp.mp ‹_› χ).sq_hasLift

Mathlib/Topology/ContinuousMap/Basic.lean

@@ -207,6 +207,14 @@ theorem prod_eval (f : C(α, β₁)) (g : C(α, β₂)) (a : α) : (prodMk f g)
 @[simps!]
 def prodSwap : C(α × β, β × α) := .prodMk .snd .fst
 
+/-- The diagonal map `x ↦ (x, x)` as a bundled continuous map. -/
+@[simps]
+def diagonal X [TopologicalSpace X] : C(X, X × X) where
+  toFun x := (x, x)
+
+lemma diagonal_injective {X} [TopologicalSpace X] : Function.Injective (diagonal X) := by
+  intro x y h; simpa using h
+
 end Prod
 
 section Sigma

Mathlib/Topology/SeparatedMap.lean

@@ -5,8 +5,8 @@ Authors: Junyan Xu
 -/
 module
 
+public import Mathlib.Topology.ContinuousMap.Basic
 public import Mathlib.Topology.Connected.Basic
-public import Mathlib.Topology.Separation.Hausdorff
 public import Mathlib.Topology.Connected.Clopen
 /-!
 # Separated maps and locally injective maps out of a topological space.
@@ -102,6 +102,16 @@ theorem isSeparatedMap_iff_isClosedMap {f : X → Y} :
     ⟨IsClosedEmbedding.isClosedMap, .of_continuous_injective_isClosedMap
       (IsEmbedding.toPullbackDiag f).continuous (injective_toPullbackDiag f)⟩
 
+lemma _root_.Topology.IsClosedEmbedding.diagonal [T2Space X] :
+    IsClosedEmbedding (ContinuousMap.diagonal X) := by
+  let τ : C(X, Unit) := .const X ()
+  let η : X × X ≃ₜ Function.Pullback ⇑τ ⇑τ :=
+  { toFun | (x, y) => ⟨(x, y), rfl⟩
+    invFun := Subtype.val }
+  rw [← η.isClosedEmbedding.of_comp_iff]
+  convert isSeparatedMap_iff_isClosedEmbedding.mp (T2Space.isSeparatedMap _)
+  infer_instance
+
 open Function.Pullback in
 theorem IsSeparatedMap.pullback {f : X → Y} (sep : IsSeparatedMap f) (g : A → Y) :
     IsSeparatedMap (@snd X Y A f g) := by