English
There is a natural bijection between continuous maps from the Stone–Čech compactification of X to a compact Hausdorff Y and continuous maps from X to the underlying topological space of Y.
Русский
Существует естественная биекция между непрерывными отображениями от Stone–Čech(X) к Y и непрерывными отображениями от X к базовой топологической пространстве Y.
LaTeX
$$$\mathrm{Hom}(\mathrm{StoneCech}(X), Y) \cong \mathrm{Hom}(X, Y_{\mathrm{Top}})$ for appropriate X, Y.$$
Lean4
/-- (Implementation) The bijection of homsets to establish the reflective adjunction of compact
Hausdorff spaces in topological spaces.
-/
noncomputable def stoneCechEquivalence (X : TopCat.{u}) (Y : CompHaus.{u}) :
(stoneCechObj X ⟶ Y) ≃ (X ⟶ compHausToTop.obj Y)
where
toFun
f :=
TopCat.ofHom
{ toFun := f ∘ stoneCechUnit
continuous_toFun := f.hom.2.comp (@continuous_stoneCechUnit X _) }
invFun
f :=
CompHausLike.ofHom _
{ toFun := stoneCechExtend f.hom.2
continuous_toFun := continuous_stoneCechExtend f.hom.2 }
left_inv := by
rintro ⟨f : StoneCech X ⟶ Y, hf : Continuous f⟩
ext x
refine congr_fun ?_ x
apply Continuous.ext_on denseRange_stoneCechUnit (continuous_stoneCechExtend _) hf
· rintro _ ⟨y, rfl⟩
apply congr_fun (stoneCechExtend_extends (hf.comp _)) y
apply continuous_stoneCechUnit
right_inv := by
rintro ⟨f : (X : Type _) ⟶ Y, hf : Continuous f⟩
ext
exact congr_fun (stoneCechExtend_extends hf) _
