Adjunctions involving the category of Stonean spaces

This file constructs the left adjoint typeToStonean to the forgetful functor from Stonean spaces to sets, using the Stone-Cech compactification. This allows to conclude that the monomorphisms in Stonean are precisely the injective maps (see Stonean.mono_iff_injective).

def Stonean.stoneCechObj (X : Type u) : Stonean

The object part of the compactification functor from types to Stonean spaces.

noncomputable def Stonean.stoneCechEquivalence (X : Type u) (Y : Stonean) : (Stonean.stoneCechObj X ⟶ Y) ≃ (X ⟶ (CategoryTheory.forget Stonean).obj Y)

The equivalence of homsets to establish the adjunction between the Stone-Cech compactification functor and the forgetful functor.

noncomputable def typeToStonean : CategoryTheory.Functor (Type u) Stonean

The Stone-Cech compactification functor from types to Stonean spaces.

noncomputable def Stonean.stoneCechAdjunction : typeToStonean ⊣ CategoryTheory.forget Stonean

The Stone-Cech compactification functor is left adjoint to the forgetful functor.

noncomputable instance Stonean.forget.preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget Stonean)

The forgetful functor from Stonean spaces, being a right adjoint, preserves limits.

theorem Stonean.mono_iff_injective {X : Stonean} {Y : Stonean} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ↑f