feat: some API for explicit limits in CompHaus (#5762)

Co-authored by: 
- Riccardo Brasca [riccardo.brasca@gmail.com](mailto:riccardo.brasca@gmail.com) @riccardobrasca 
- Filippo A. E. Nuccio [filippo.nuccio@univ-st-etienne.fr](mailto:filippo.nuccio@univ-st-etienne.fr) @faenuccio 

We add some more API for the compatibility of explicit and abstract limits in CompHaus
This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Mathlib.lean

@@ -3152,7 +3152,7 @@ import Mathlib.Topology.Bornology.Hom
 import Mathlib.Topology.Category.Born
 import Mathlib.Topology.Category.CompHaus.Basic
 import Mathlib.Topology.Category.CompHaus.EffectiveEpi
-import Mathlib.Topology.Category.CompHaus.ExplicitLimits
+import Mathlib.Topology.Category.CompHaus.Limits
 import Mathlib.Topology.Category.CompHaus.Projective
 import Mathlib.Topology.Category.Compactum
 import Mathlib.Topology.Category.Locale

Mathlib/Topology/Category/CompHaus/Basic.lean

@@ -139,6 +139,41 @@ noncomputable def isoOfBijective {X Y : CompHaus.{u}} (f : X ⟶ Y) (bij : Funct
 set_option linter.uppercaseLean3 false in
 #align CompHaus.iso_of_bijective CompHaus.isoOfBijective
 
+/-- Construct an isomorphism from a homeomorphism. -/
+@[simps hom inv]
+def isoOfHomeo {X Y : CompHaus.{u}} (f : X ≃ₜ Y) : X ≅ Y where
+  hom := ⟨f, f.continuous⟩
+  inv := ⟨f.symm, f.symm.continuous⟩
+  hom_inv_id := by
+    ext x
+    exact f.symm_apply_apply x
+  inv_hom_id := by
+    ext x
+    exact f.apply_symm_apply x
+
+/-- Construct a homeomorphism from an isomorphism. -/
+@[simps]
+def homeoOfIso {X Y : CompHaus.{u}} (f : X ≅ Y) : X ≃ₜ Y where
+  toFun := f.hom
+  invFun := f.inv
+  left_inv x := by simp
+  right_inv x := by simp
+  continuous_toFun := f.hom.continuous
+  continuous_invFun := f.inv.continuous
+
+/-- The equivalence between isomorphisms in `CompHaus` and homeomorphisms
+of topological spaces. -/
+@[simps]
+def isoEquivHomeo {X Y : CompHaus.{u}} : (X ≅ Y) ≃ (X ≃ₜ Y) where
+  toFun := homeoOfIso
+  invFun := isoOfHomeo
+  left_inv f := by
+    ext
+    rfl
+  right_inv f := by
+    ext
+    rfl
+
 end CompHaus
 
 /-- The fully faithful embedding of `CompHaus` in `TopCat`. -/

Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean

@@ -5,7 +5,7 @@ Authors: Adam Topaz
 -/
 
 import Mathlib.CategoryTheory.Sites.Coherent
-import Mathlib.Topology.Category.CompHaus.ExplicitLimits
+import Mathlib.Topology.Category.CompHaus.Limits
 
 /-!
 

Mathlib/Topology/Category/CompHaus/ExplicitLimits.lean → Mathlib/Topology/Category/CompHaus/Limits.lean

@@ -36,10 +36,9 @@ pairs `(x,y)` such that `f x = g y`, with the topology induced by the product.
 -/
 def pullback : CompHaus.{u} :=
   letI set := { xy : X × Y | f xy.fst = g xy.snd }
-  haveI : CompactSpace set := by
-    rw [← isCompact_iff_compactSpace]
-    apply IsClosed.isCompact
-    exact isClosed_eq (f.continuous.comp continuous_fst) (g.continuous.comp continuous_snd)
+  haveI : CompactSpace set :=
+  isCompact_iff_compactSpace.mp (isClosed_eq (f.continuous.comp continuous_fst)
+    (g.continuous.comp continuous_snd)).isCompact
   CompHaus.of set
 
 /--
@@ -109,6 +108,30 @@ def pullback.isLimit : Limits.IsLimit (pullback.cone f g) :=
     (fun _ => pullback.lift_snd _ _ _ _ _)
     (fun _ _ hm => pullback.hom_ext _ _ _ _ (hm .left) (hm .right))
 
+section Isos
+
+/-- The isomorphism from the explicit pullback to the abstract pullback. -/
+noncomputable
+def pullbackIsoPullback : CompHaus.pullback f g ≅ Limits.pullback f g :=
+Limits.IsLimit.conePointUniqueUpToIso (pullback.isLimit f g) (Limits.limit.isLimit _)
+
+/-- The homeomorphism from the explicit pullback to the abstract pullback. -/
+noncomputable
+def pullbackHomeoPullback : (CompHaus.pullback f g).toTop ≃ₜ (Limits.pullback f g).toTop :=
+CompHaus.homeoOfIso (pullbackIsoPullback f g)
+
+theorem pullback_fst_eq :
+    CompHaus.pullback.fst f g = (pullbackIsoPullback f g).hom ≫ Limits.pullback.fst := by
+  dsimp [pullbackIsoPullback]
+  simp only [Limits.limit.conePointUniqueUpToIso_hom_comp, pullback.cone_pt, pullback.cone_π]
+
+theorem pullback_snd_eq :
+    CompHaus.pullback.snd f g = (pullbackIsoPullback f g).hom ≫ Limits.pullback.snd := by
+  dsimp [pullbackIsoPullback]
+  simp only [Limits.limit.conePointUniqueUpToIso_hom_comp, pullback.cone_pt, pullback.cone_π]
+
+end Isos
+
 end Pullbacks
 
 section FiniteCoproducts
@@ -172,6 +195,40 @@ def finiteCoproduct.isColimit : Limits.IsColimit (finiteCoproduct.cocone X) wher
     apply_fun (fun q => q t) at hm
     exact hm
 
+section Iso
+
+/-- The isomorphism from the explicit finite coproducts to the abstract coproduct. -/
+noncomputable
+def coproductIsoCoproduct : finiteCoproduct X ≅ ∐ X :=
+Limits.IsColimit.coconePointUniqueUpToIso (finiteCoproduct.isColimit X) (Limits.colimit.isColimit _)
+
+theorem Sigma.ι_comp_toFiniteCoproduct (a : α) :
+    (Limits.Sigma.ι X a) ≫ (coproductIsoCoproduct X).inv = finiteCoproduct.ι X a := by
+  dsimp [coproductIsoCoproduct]
+  simp only [Limits.colimit.comp_coconePointUniqueUpToIso_inv, finiteCoproduct.cocone_pt,
+    finiteCoproduct.cocone_ι, Discrete.natTrans_app]
+
+/-- The homeomorphism from the explicit finite coproducts to the abstract coproduct. -/
+noncomputable
+def coproductHomeoCoproduct : finiteCoproduct X ≃ₜ (∐ X : _) :=
+CompHaus.homeoOfIso (coproductIsoCoproduct X)
+
+end Iso
+
+lemma finiteCoproduct.ι_injective (a : α) : Function.Injective (finiteCoproduct.ι X a) := by
+  intro x y hxy
+  exact eq_of_heq (Sigma.ext_iff.mp hxy).2
+
+lemma finiteCoproduct.ι_jointly_surjective (R : finiteCoproduct X) :
+    ∃ (a : α) (r : X a), R = finiteCoproduct.ι X a r := ⟨R.fst, R.snd, rfl⟩
+
+lemma finiteCoproduct.ι_desc_apply {B : CompHaus} {π : (a : α) → X a ⟶ B} (a : α) :
+    ∀ x, finiteCoproduct.desc X π (finiteCoproduct.ι X a x) = π a x := by
+  intro x
+  change (ι X a ≫ desc X π) _ = _
+  simp only [ι_desc]
+-- `elementwise` should work here, but doesn't
+
 end FiniteCoproducts
 
 end CompHaus