LightCondMod — Mathlib

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)

Похожие утверждения