Documentation

Mathlib.Topology.Category.Stonean.Adjunctions

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).

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

Instances For

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

    Instances For

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

      Instances For

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

        Instances For

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