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 abelian groups 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 = CategoryTheory.Ran.loc FintypeCat.toProfinite (Condensed.finFree 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)} [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)