CondensedMod — Mathlib

English

CondensedMod R is the category of condensed R-modules, i.e., condensed modules valued in ModuleCat(R).

Русский

CondensedMod R — категория конденсированных R-модулей, то есть конденсированные модули над R, значения которых лежат в ModuleCat(R).

LaTeX

$$$\text{CondensedMod}(R) = \text{Condensed}(\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 CondensedMod :=
  Condensed.{u} (ModuleCat.{u + 1} R)

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