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 [scholze2019condensed], 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.

source
@[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
    Instances For
      source
      @[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
        Instances For
          source
          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
            Instances For
              source
              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.

              Equations
                Instances For
                  source
                  instance Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit (R : Type (u + 1)) [Ring R] :
                  (profiniteSolid R).IsRightKanExtension (profiniteSolidCounit R)
                  source
                  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.

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

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

                      Equations
                        Instances For
                          source
                          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.

                          Instances