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
Instances For
    noncomputable instance instAbelianCondensedMod (R : Type (u + 1)) [Ring R] :
    Equations

    The forgetful functor from condensed R-modules to condensed sets.

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

        The condensed version of the free-forgetful adjunction.

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

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

          Equations
          Instances For
            @[reducible, inline]

            The forgetful functor from condensed abelian groups to condensed sets.

            Equations
            Instances For
              @[reducible, inline]

              The free condensed abelian group on a condensed set.

              Equations
              Instances For
                @[reducible, inline]

                The free-forgetful adjunction for condensed abelian groups.

                Equations
                Instances For
                  @[simp]
                  theorem CondensedMod.hom_naturality_apply (R : Type (u + 1)) [Ring R] {X : CondensedMod R} {Y : CondensedMod R} (f : X Y) {S : CompHausᵒᵖ} {T : CompHausᵒᵖ} (g : S T) (x : (X.val.obj S)) :
                  (f.val.app T) ((X.val.map g) x) = (Y.val.map g) ((f.val.app S) x)