English
There is a natural equivalence between morphisms from the Stone–Cech object of X to Y (in the CompHaus-like category) and continuous maps from X to ToType Y, establishing the adjunction between Stonean and the forgetful functor.
Русский
Существует естественное эквивалентство между морфизмами из объекта Stone–Cech от X в Y и непрерывными отображениями из X в ToType Y, что задаёт сопряжение между Stonean и забывающим функтором.
LaTeX
$$$\text{stoneCechEquivalence}(X,Y): (\mathrm{stoneCechObj} X \to Y) \simeq (X \to \mathrm{ToType} Y)$$$
Lean4
/-- The equivalence of homsets to establish the adjunction between the Stone-Cech compactification
functor and the forgetful functor. -/
noncomputable def stoneCechEquivalence (X : Type u) (Y : Stonean.{u}) : (stoneCechObj X ⟶ Y) ≃ (X ⟶ ToType Y) :=
by
letI : TopologicalSpace X := ⊥
haveI : DiscreteTopology X := ⟨rfl⟩
refine fullyFaithfulToCompHaus.homEquiv.trans ?_
exact (_root_.stoneCechEquivalence (TopCat.of X) (toCompHaus.obj Y)).trans (TopCat.adj₁.homEquiv _ _)
