Documentation

Mathlib.Condensed.Solid

Solid modules #

This file contains the definition of a solid R-module: CondensedMod.isSolid R. Solid modules groups were introduced in [Sch19], Definition 5.1.

Main definition #

TODO (hard): prove that ((profiniteSolid ℤ).obj S).IsSolid for S : Profinite. TODO (slightly easier): prove that ((profiniteSolid 𝔽ₚ).obj S).IsSolid for S : Profinite.

@[reducible, inline]

The free condensed abelian group on a finite set.

Equations
Instances For
    @[reducible, inline]

    The free condensed abelian group on a profinite space.

    Equations
    Instances For

      The functor sending a profinite space S to the condensed abelian group R[S]^\solid.

      Equations
      Instances For

        The natural transformation FintypeCat.toProfiniteprofiniteSolid R ⟶ finFree R which is part of the assertion that profiniteSolid R is the (pointwise) right Kan extension of finFree R along FintypeCat.toProfinite.

        Equations
        Instances For

          The natural transformation R[S] ⟶ R[S]^\solid.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            class CondensedMod.IsSolid (R : Type (u + 1)) [Ring R] (A : CondensedMod R) :

            The predicate on condensed abelian groups describing the property of being solid.

            Instances
              theorem CondensedMod.IsSolid.isIso_solidification_map {R : Type (u + 1)} :
              ∀ {inst : Ring R} {A : CondensedMod R} [self : CondensedMod.IsSolid R A] (X : Profinite), CategoryTheory.IsIso ((CategoryTheory.yoneda.obj A).map ((Condensed.profiniteSolidification R).app X).op)