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.

Equations

• Stonean.stoneCechObj X = Stonean.of (StoneCech X)

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• typeToStonean = CategoryTheory.Adjunction.leftAdjointOfEquiv Stonean.stoneCechEquivalence typeToStonean.proof_1

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

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

Equations

• Stonean.stoneCechAdjunction = CategoryTheory.Adjunction.adjunctionOfEquivLeft Stonean.stoneCechEquivalence Stonean.stoneCechAdjunction.proof_1

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

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

Equations

• Stonean.forget.preservesLimits = Stonean.stoneCechAdjunction.rightAdjointPreservesLimits

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