Light condensed R-modules

This files defines light condensed modules over a ring R.

Main results

• Light condensed R-modules form an abelian category.

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

@[reducible, inline]

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

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

Equations

• LightCondMod R = LightCondensed (ModuleCat R)

noncomputable instance instAbelianLightCondMod (R : Type u) [Ring R] : CategoryTheory.Abelian (LightCondMod R)

Equations

• instAbelianLightCondMod R = CategoryTheory.sheafIsAbelian

def LightCondensed.forget (R : Type u) [Ring R] : CategoryTheory.Functor (LightCondMod R) LightCondSet

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

Equations

• LightCondensed.forget R = CategoryTheory.sheafCompose (CategoryTheory.coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))

noncomputable def LightCondensed.free (R : Type u) [Ring R] : CategoryTheory.Functor LightCondSet (LightCondMod R)

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

Equations

• LightCondensed.free R = CategoryTheory.Sheaf.composeAndSheafify (CategoryTheory.coherentTopology LightProfinite) (ModuleCat.free R)

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

The condensed version of the free-forgetful adjunction.

Equations

• LightCondensed.freeForgetAdjunction R = CategoryTheory.Sheaf.adjunction (CategoryTheory.coherentTopology LightProfinite) (ModuleCat.adj R)

@[reducible, inline]

abbrev LightCondAb : Type 1

The category of condensed abelian groups, defined as sheaves of abelian groups over CompHaus with respect to the coherent Grothendieck topology.

Equations

• LightCondAb = LightCondMod ℤ

@[simp]

theorem LightCondMod.hom_naturality_apply (R : Type u) [Ring R] {X Y : LightCondMod R} (f : X ⟶ Y) {S T : LightProfiniteᵒᵖ} (g : S ⟶ T) (x : ↑(X.val.obj S)) : (f.val.app T).hom ((X.val.map g).hom x) = (Y.val.map g).hom ((f.val.app S).hom x)