feat(src/topology/category/Top/limits): Coproducts in Top. (#17282)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/topology/category/Top/limits.lean

@@ -680,7 +680,109 @@ end
 
 end pullback
 
---TODO: Add analogous constructions for `coprod` and `pushout`.
+/-- The terminal object of `Top` is `punit`. -/
+def is_terminal_punit : is_terminal (Top.of punit.{u+1}) :=
+begin
+  haveI : ∀ X, unique (X ⟶ Top.of punit.{u+1}) :=
+    λ X, ⟨⟨⟨λ x, punit.star, by continuity⟩⟩, λ f, by ext⟩,
+  exact limits.is_terminal.of_unique _,
+end
+
+/-- The terminal object of `Top` is `punit`. -/
+def terminal_iso_punit : ⊤_ Top.{u} ≅ Top.of punit :=
+terminal_is_terminal.unique_up_to_iso is_terminal_punit
+
+/-- The initial object of `Top` is `pempty`. -/
+def is_initial_pempty : is_initial (Top.of pempty.{u+1}) :=
+begin
+  haveI : ∀ X, unique (Top.of pempty.{u+1} ⟶ X) :=
+    λ X, ⟨⟨⟨λ x, x.elim, by continuity⟩⟩, λ f, by ext ⟨⟩⟩,
+  exact limits.is_initial.of_unique _,
+end
+
+/-- The initial object of `Top` is `pempty`. -/
+def initial_iso_pempty : ⊥_ Top.{u} ≅ Top.of pempty :=
+initial_is_initial.unique_up_to_iso is_initial_pempty
+
+/-- The binary coproduct cofan in `Top`. -/
+protected
+def binary_cofan (X Y : Top.{u}) : binary_cofan X Y :=
+binary_cofan.mk (⟨sum.inl⟩ : X ⟶ Top.of (X ⊕ Y)) ⟨sum.inr⟩
+
+/-- The constructed binary coproduct cofan in `Top` is the coproduct. -/
+def binary_cofan_is_colimit (X Y : Top.{u}) : is_colimit (Top.binary_cofan X Y) :=
+begin
+  refine limits.binary_cofan.is_colimit_mk (λ s, ⟨sum.elim s.inl s.inr⟩) _ _ _,
+  { intro s, ext, refl },
+  { intro s, ext, refl },
+  { intros s m h₁ h₂, ext (x|x),
+    exacts [(concrete_category.congr_hom h₁ x : _), (concrete_category.congr_hom h₂ x : _)] },
+end
+
+lemma binary_cofan_is_colimit_iff {X Y : Top} (c : binary_cofan X Y) :
+  nonempty (is_colimit c) ↔
+    open_embedding c.inl ∧ open_embedding c.inr ∧ is_compl (set.range c.inl) (set.range c.inr) :=
+begin
+  classical,
+  split,
+  { rintro ⟨h⟩,
+    rw [← show _ = c.inl, from h.comp_cocone_point_unique_up_to_iso_inv
+      (binary_cofan_is_colimit X Y) ⟨walking_pair.left⟩,
+      ← show _ = c.inr, from h.comp_cocone_point_unique_up_to_iso_inv
+      (binary_cofan_is_colimit X Y) ⟨walking_pair.right⟩],
+    dsimp,
+    refine
+    ⟨(homeo_of_iso $ h.cocone_point_unique_up_to_iso (binary_cofan_is_colimit X Y)).symm
+      .open_embedding.comp open_embedding_inl, (homeo_of_iso $ h.cocone_point_unique_up_to_iso
+        (binary_cofan_is_colimit X Y)).symm.open_embedding.comp open_embedding_inr, _⟩,
+    erw [set.range_comp, ← eq_compl_iff_is_compl, set.range_comp _ sum.inr, ← set.image_compl_eq
+      (homeo_of_iso $ h.cocone_point_unique_up_to_iso (binary_cofan_is_colimit X Y))
+      .symm.bijective],
+    congr' 1,
+    exact set.compl_range_inr.symm },
+  { rintros ⟨h₁, h₂, h₃⟩,
+    have : ∀ x, x ∈ set.range c.inl ∨ x ∈ set.range c.inr,
+    { rw [eq_compl_iff_is_compl.mpr h₃.symm], exact λ _, or_not },
+    refine ⟨binary_cofan.is_colimit.mk _ _ _ _ _⟩,
+    { intros T f g,
+      refine continuous_map.mk _ _,
+      { exact λ x, if h : x ∈ set.range c.inl
+        then f ((equiv.of_injective _ h₁.inj).symm ⟨x, h⟩)
+        else g ((equiv.of_injective _ h₂.inj).symm ⟨x, (this x).resolve_left h⟩) },
+      rw continuous_iff_continuous_at,
+      intro x,
+      by_cases x ∈ set.range c.inl,
+      { revert h x,
+      apply (is_open.continuous_on_iff _).mp,
+      { rw continuous_on_iff_continuous_restrict,
+        convert_to continuous (f ∘ (homeomorph.of_embedding _ h₁.to_embedding).symm),
+        { ext ⟨x, hx⟩, exact dif_pos hx },
+        continuity },
+      { exact h₁.open_range } },
+    { revert h x,
+      apply (is_open.continuous_on_iff _).mp,
+      { rw continuous_on_iff_continuous_restrict,
+        have : ∀ a, a ∉ set.range c.inl → a ∈ set.range c.inr,
+        { rintros a (h : a ∈ (set.range c.inl)ᶜ), rwa eq_compl_iff_is_compl.mpr h₃.symm },
+        convert_to continuous
+          (g ∘ (homeomorph.of_embedding _ h₂.to_embedding).symm ∘ subtype.map _ this),
+        { ext ⟨x, hx⟩, exact dif_neg hx },
+        continuity,
+        rw embedding_subtype_coe.to_inducing.continuous_iff,
+        exact continuous_subtype_coe },
+      { change is_open (set.range c.inl)ᶜ, rw ← eq_compl_iff_is_compl.mpr h₃.symm,
+        exact h₂.open_range } } },
+    { intros T f g, ext x, refine (dif_pos _).trans _, { exact ⟨x, rfl⟩ },
+        { rw equiv.of_injective_symm_apply } },
+    { intros T f g, ext x, refine (dif_neg _).trans _,
+      { rintro ⟨y, e⟩, have : c.inr x ∈ set.range c.inl ⊓ set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩,
+        rwa disjoint_iff.mp h₃.1 at this },
+      { exact congr_arg g (equiv.of_injective_symm_apply _ _) } },
+    { rintro T _ _ m rfl rfl, ext x, change m x = dite _ _ _,
+      split_ifs; exact congr_arg _ (equiv.apply_of_injective_symm _ ⟨_, _⟩).symm } }
+end
+
+--TODO: Add analogous constructions for `pushout`.
 
 lemma coinduced_of_is_colimit {F : J ⥤ Top.{max v u}} (c : cocone F) (hc : is_colimit c) :
   c.X.topological_space = ⨆ j, (F.obj j).topological_space.coinduced (c.ι.app j) :=