Light condensed R-modules

This file 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 light condensed R-modules, defined as sheaves of R-modules over LightProfinite.{u} with respect to the coherent Grothendieck topology.

@[implicit_reducible]

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

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

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

@[simp]

theorem LightCondensed.forget_map_hom_app (R : Type u) [Ring R] {X✝ Y✝ : CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)} (f : X✝ ⟶ Y✝) (X : LightProfiniteᵒᵖ) (a✝ : (CategoryTheory.forget (ModuleCat R)).obj (((CategoryTheory.sheafToPresheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).obj X✝).obj X)) : ((forget R).map f).hom.app X a✝ = (CategoryTheory.ConcreteCategory.hom (f.hom.app X)) a✝

@[simp]

theorem LightCondensed.forget_obj_obj_map (R : Type u) [Ring R] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)) {X✝ Y✝ : LightProfiniteᵒᵖ} (f : X✝ ⟶ Y✝) (a✝ : (CategoryTheory.forget (ModuleCat R)).obj (((CategoryTheory.sheafToPresheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).obj X).obj X✝)) : ((forget R).obj X).obj.map f a✝ = (CategoryTheory.ConcreteCategory.hom (X.obj.map f)) a✝

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

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

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

The condensed version of the free-forgetful adjunction.

@[reducible, inline]

abbrev LightCondAb : Type 1

The category of light condensed abelian groups, defined as sheaves of ℤ-modules over LightProfinite.{0} with respect to the coherent Grothendieck topology.

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.obj.obj S)) : (CategoryTheory.ConcreteCategory.hom (f.hom.app T)) ((CategoryTheory.ConcreteCategory.hom (X.obj.map g)) x) = (CategoryTheory.ConcreteCategory.hom (Y.obj.map g)) ((CategoryTheory.ConcreteCategory.hom (f.hom.app S)) x)