Adjunctions regarding categories of condensed objects

This file shows that the forgetful functor from condensed abelian groups to condensed sets has a left adjoint, called the free condensed abelian group on a condensed set.

TODO (Dagur):

• Add free condensed modules over more general rings.

def Condensed.abForget : CategoryTheory.Functor CondensedAb CondensedSet

The forgetful functor from condensed abelian groups to condensed sets.

Equations

• Condensed.abForget = CategoryTheory.sheafCompose (CategoryTheory.coherentTopology CompHaus) (CategoryTheory.forget AddCommGroupCat)

noncomputable def Condensed.freeAb : CategoryTheory.Functor CondensedSet CondensedAb

The left adjoint to the forgetful functor. The free condensed abelian group on a condensed set.

Equations

• Condensed.freeAb = CategoryTheory.Sheaf.composeAndSheafify (CategoryTheory.coherentTopology CompHaus) AddCommGroupCat.free

noncomputable def Condensed.setAbAdjunction : Condensed.freeAb ⊣ Condensed.abForget

The condensed version of the free-forgetful adjunction.

Equations

• Condensed.setAbAdjunction = CategoryTheory.Sheaf.adjunction (CategoryTheory.coherentTopology CompHaus) AddCommGroupCat.adj