English
There is an equivalence of hom-sets between from CompHaus.toProfiniteObj X to Y and from X to profiniteToCompHaus.obj Y.
Русский
Существует эквивалентность гомотропов между (CompHaus.toProfiniteObj X ⟶ Y) и (X ⟶ profiniteToCompHaus.obj Y).
LaTeX
$$$(\text{CompHaus.toProfiniteObj } X \to Y) \simeq (X \to \text{profiniteToCompHaus.obj } Y)$$$
Lean4
/-- (Implementation) The bijection of homsets to establish the reflective adjunction of Profinite
spaces in compact Hausdorff spaces.
-/
def toCompHausEquivalence (X : CompHaus.{u}) (Y : Profinite.{u}) :
(CompHaus.toProfiniteObj X ⟶ Y) ≃ (X ⟶ profiniteToCompHaus.obj Y)
where
toFun f := ofHom _ (f.hom.comp ⟨Quotient.mk'', continuous_quotient_mk'⟩)
invFun
g :=
TopCat.ofHom
{ toFun := Continuous.connectedComponentsLift g.hom.2
continuous_toFun := Continuous.connectedComponentsLift_continuous g.hom.2 }
left_inv _ := TopCat.ext <| ConnectedComponents.surjective_coe.forall.2 fun _ => rfl
