3.1. Coherent objects
Definition3.1.1
Group: Replete categories, coherent objects, and weakly contractible objects, following Section 3 of Bhatt–Scholze. (11)
Lean status
- No associated Lean code or declarations.
An object X of \mathcal{C} is compact if the top element of the poset
of subobjects of X is a compact element.
Definition3.1.2
Group: Replete categories, coherent objects, and weakly contractible objects, following Section 3 of Bhatt–Scholze. (11)
Lean status
- No associated Lean code or declarations.
An object X of \mathcal{C} is stable if for all compact Y and
morphisms Y \to X, the fiber product Y \times_X Y is compact.
Definition3.1.3
Group: Replete categories, coherent objects, and weakly contractible objects, following Section 3 of Bhatt–Scholze. (11)
Statement uses 2
Lean status
- No associated Lean code or declarations.
An object X of \mathcal{C} is coherent if it is compact and stable.