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 [Sch19], 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 R-module 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 R-module 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 R-module 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
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              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.

              Instances