Condensed R-modules

This file defines condensed modules over a ring R.

Main results

• Condensed R-modules form an abelian category.

• The forgetful functor from condensed R-modules to condensed sets has a left adjoint, sending a condensed set to the corresponding free condensed R-module.

@[reducible, inline]

abbrev CondensedMod (R : Type (u + 1)) [Ring R] : Type (u + 2)

The category of condensed R-modules, defined as sheaves of R-modules over CompHaus with respect to the coherent Grothendieck topology.

Equations

• CondensedMod R = Condensed (ModuleCat R)

noncomputable instance instAbelianCondensedMod (R : Type (u + 1)) [Ring R] : CategoryTheory.Abelian (CondensedMod R)

Equations

• instAbelianCondensedMod R = CategoryTheory.sheafIsAbelian

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

The forgetful functor from condensed R-modules to condensed sets.

Equations

• Condensed.forget R = CategoryTheory.sheafCompose (CategoryTheory.coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))

noncomputable def Condensed.free (R : Type (u + 1)) [Ring R] : CategoryTheory.Functor CondensedSet (CondensedMod R)

The left adjoint to the forgetful functor. The free condensed R-module on a condensed set.

Equations

• Condensed.free R = CategoryTheory.Sheaf.composeAndSheafify (CategoryTheory.coherentTopology CompHaus) (ModuleCat.free R)

noncomputable def Condensed.freeForgetAdjunction (R : Type (u + 1)) [Ring R] : free R ⊣ forget R

The condensed version of the free-forgetful adjunction.

Equations

• Condensed.freeForgetAdjunction R = CategoryTheory.Sheaf.adjunction (CategoryTheory.coherentTopology CompHaus) (ModuleCat.adj R)

@[reducible, inline]

abbrev CondensedAb : Type (u + 2)

The category of condensed abelian groups is defined as condensed ℤ-modules.

Equations

• CondensedAb = CondensedMod (ULift.{?u.2 + 1, 0} ℤ)

@[reducible, inline]

abbrev Condensed.abForget : CategoryTheory.Functor CondensedAb CondensedSet

The forgetful functor from condensed abelian groups to condensed sets.

Equations

• Condensed.abForget = Condensed.forget (ULift.{?u.6 + 1, 0} ℤ)

@[reducible, inline]

noncomputable abbrev Condensed.freeAb : CategoryTheory.Functor CondensedSet CondensedAb

The free condensed abelian group on a condensed set.

Equations

• Condensed.freeAb = Condensed.free (ULift.{?u.6 + 1, 0} ℤ)

@[reducible, inline]

noncomputable abbrev Condensed.setAbAdjunction : freeAb ⊣ abForget

The free-forgetful adjunction for condensed abelian groups.

Equations

• Condensed.setAbAdjunction = Condensed.freeForgetAdjunction (ULift.{?u.8 + 1, 0} ℤ)

theorem CondensedMod.hom_naturality_apply (R : Type (u + 1)) [Ring R] {X Y : CondensedMod R} (f : X ⟶ Y) {S T : CompHausᵒᵖ} (g : S ⟶ T) (x : ↑(X.val.obj S)) : (CategoryTheory.ConcreteCategory.hom (f.val.app T)) ((CategoryTheory.ConcreteCategory.hom (X.val.map g)) x) = (CategoryTheory.ConcreteCategory.hom (Y.val.map g)) ((CategoryTheory.ConcreteCategory.hom (f.val.app S)) x)