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.

Equations
Instances For

    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.
    Instances For

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

      Equations
      Instances For

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

        Equations