Solid modules

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

Main definition

• CondensedMod.IsSolid R: the predicate on condensed R-modules describing the property of being solid.

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]

abbrev Condensed.finFree (R : Type (u + 1)) [Ring R] : CategoryTheory.Functor FintypeCat (CondensedMod R)

The free condensed R-module on a finite set.

@[reducible, inline]

abbrev Condensed.profiniteFree (R : Type (u + 1)) [Ring R] : CategoryTheory.Functor Profinite (CondensedMod R)

The free condensed R-module on a profinite space.

def Condensed.profiniteSolid (R : Type (u + 1)) [Ring R] : CategoryTheory.Functor Profinite (CondensedMod R)

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

def Condensed.profiniteSolidCounit (R : Type (u + 1)) [Ring R] : FintypeCat.toProfinite.comp (profiniteSolid R) ⟶ finFree R

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

instance Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit (R : Type (u + 1)) [Ring R] : (profiniteSolid R).IsRightKanExtension (profiniteSolidCounit R)

def Condensed.profiniteSolidIsPointwiseRightKanExtension (R : Type (u + 1)) [Ring R] : (CategoryTheory.Functor.RightExtension.mk (profiniteSolid R) (profiniteSolidCounit R)).IsPointwiseRightKanExtension

The functor Profinite.{u} ⥤ CondensedMod.{u} R is a pointwise right Kan extension of finFree R : FintypeCat.{u} ⥤ CondensedMod.{u} R along FintypeCat.toProfinite.

def Condensed.profiniteSolidification (R : Type (u + 1)) [Ring R] : profiniteFree R ⟶ profiniteSolid R

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

class CondensedMod.IsSolid (R : Type (u + 1)) [Ring R] (A : CondensedMod R) : Prop

The predicate on condensed R-modules describing the property of being solid.

TODO: This is not the correct definition of solid R-modules for a general R. The correct one is as follows: Use this to define solid modules over a finite type ℤ-algebra R. In particular this gives a definition of solid modules over ℤ[X] (polynomials in one variable). Then a solid R-module over a general ring R is the condition that for every r ∈ R and every ring homomorphism ℤ[X] → R such that X maps to r, the underlying ℤ[X]-module is solid.

• isIso_solidification_map (X : Profinite) : CategoryTheory.IsIso ((CategoryTheory.yoneda.obj A).map ((Condensed.profiniteSolidification R).app X).op)