Solid abelian groups

This file contains the definition of a solid abelian group: CondensedAb.isSolid. Solid abelian groups were introduced in [scholze2019condensed], Definition 5.1.

Main definition

• CondensedAb.IsSolid: the predicate on condensed abelian groups describing the property of being solid.

TODO (hard): prove that (profiniteSolid.obj S).IsSolid for S : Profinite.

@[inline, reducible]

abbrev Condensed.finFree : CategoryTheory.Functor FintypeCat CondensedAb

The free condensed abelian group on a finite set.

Equations

• Condensed.finFree = CategoryTheory.Functor.comp FintypeCat.toProfinite (CategoryTheory.Functor.comp profiniteToCondensed Condensed.freeAb)

@[inline, reducible]

abbrev Condensed.profiniteFree : CategoryTheory.Functor Profinite CondensedAb

The free condensed abelian group on a profinite space.

Equations

• Condensed.profiniteFree = CategoryTheory.Functor.comp profiniteToCondensed Condensed.freeAb

def Condensed.profiniteSolid : CategoryTheory.Functor Profinite CondensedAb

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

Equations

• Condensed.profiniteSolid = CategoryTheory.Ran.loc FintypeCat.toProfinite Condensed.finFree

def Condensed.profiniteSolidification : Condensed.profiniteFree ⟶ Condensed.profiniteSolid

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

Equations

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

class CondensedAb.IsSolid (A : CondensedAb) : Prop

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

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