English
LightCondMod is defined as the condensed R-modules: LightCondensed on ModuleCat(R).
Русский
LightCondMod определяется как конденсированные R-модули: LightCondensed на ModuleCat(R).
LaTeX
$$$\text{LightCondMod} = \text{LightCondensed}(\text{ModuleCat}(R)).$$$
Lean4
/-- The category of condensed `R`-modules, defined as sheaves of `R`-modules over
`CompHaus` with respect to the coherent Grothendieck topology.
-/
abbrev LightCondMod :=
LightCondensed.{u} (ModuleCat.{u} R)