Documentation

Mathlib.Condensed.Module

Condensed R-modules #

This files defines condensed modules over a ring R.

Main results #

@[reducible, inline]
abbrev CondensedMod (R : Type (u + 1)) [Ring R] :
Type (u + 2)

The category of condensed R-modules, defined as sheaves of R-modules over CompHaus with respect to the coherent Grothendieck topology.

Equations
noncomputable def Condensed.free (R : Type (u + 1)) [Ring R] :

The left adjoint to the forgetful functor. The free condensed R-module on a condensed set.

Equations
noncomputable def Condensed.freeForgetAdjunction (R : Type (u + 1)) [Ring R] :

The condensed version of the free-forgetful adjunction.

Equations
@[reducible, inline]
abbrev CondensedAb :
Type (u + 2)

The category of condensed abelian groups is defined as condensed -modules.

Equations
@[reducible, inline]

The forgetful functor from condensed abelian groups to condensed sets.

Equations
@[reducible, inline]

The free condensed abelian group on a condensed set.

Equations
@[reducible, inline]

The free-forgetful adjunction for condensed abelian groups.

Equations