Documentation

Mathlib.Condensed.Functors

Functors from categories of topological spaces to condensed sets #

This file defines the embedding of the test objects (compact Hausdorff spaces) into condensed sets.

Main definitions #

The functor from CompHaus to Condensed.{u} (Type u) given by the Yoneda sheaf.

Equations
@[reducible, inline]

Dot notation for the value of compHausToCondensed.

Equations

The yoneda presheaf as a condensed set, restricted to profinite spaces.

Equations
@[reducible, inline]

Dot notation for the value of profiniteToCondensed.

Equations

The yoneda presheaf as a condensed set, restricted to Stonean spaces.

Equations
@[reducible, inline]

Dot notation for the value of stoneanToCondensed.

Equations