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 abelian group on a finite set.

Equations

• Condensed.finFree R = FintypeCat.toProfinite.comp (profiniteToCondensed.comp (Condensed.free R))

@[reducible, inline]

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

The free condensed abelian group on a profinite space.

Equations

• Condensed.profiniteFree R = profiniteToCondensed.comp (Condensed.free R)

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

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

Equations

• Condensed.profiniteSolid R = FintypeCat.toProfinite.rightKanExtension (Condensed.finFree R)

def Condensed.profiniteSolidCounit (R : Type (u + 1)) [Ring R] : FintypeCat.toProfinite.comp (Condensed.profiniteSolid R) ⟶ Condensed.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.

Equations

• Condensed.profiniteSolidCounit R = FintypeCat.toProfinite.rightKanExtensionCounit (Condensed.finFree R)

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

Equations

• ⋯ = ⋯

def Condensed.profiniteSolidIsPointwiseRightKanExtension (R : Type (u + 1)) [Ring R] : (CategoryTheory.Functor.RightExtension.mk (Condensed.profiniteSolid R) (Condensed.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.

Equations

• Condensed.profiniteSolidIsPointwiseRightKanExtension R = CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsRightKanExtension (Condensed.profiniteSolid R) (Condensed.profiniteSolidCounit R)

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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)