3. Replete categories
Let \mathcal{C} be a category with limits. By \mathrm{Ab}(\mathcal{C})
we denote its abelian group objects.
-
CategoryTheory.IsReplete[complete]
We say \mathcal{C} is replete if epimorphisms are stable under sequential
limits, i.e., if (F_n)_{n \in \mathbb{N}} is an inverse system in
\mathcal{C} such that F_{n+1} \to F_n is an epimorphism for all
n \in \mathbb{N}, then \lim F_n \to F_n is an epimorphism for all
n \in \mathbb{N}. (Bhatt–Scholze, Definition 3.1.1)
Lean code for Definition3.1●1 definition
Associated Lean declarations
-
CategoryTheory.IsReplete[complete]
-
CategoryTheory.IsReplete[complete]
-
classdefined in Proetale/Replete/Basic.leancomplete
class CategoryTheory.IsReplete.{v_2, u_2} (C : Type u_2) [CategoryTheory.Category.{v_2, u_2} C] : Prop
class CategoryTheory.IsReplete.{v_2, u_2} (C : Type u_2) [CategoryTheory.Category.{v_2, u_2} C] : Prop
Methods
epi_pi_app_of_forall_epi_map : ∀ (F : CategoryTheory.Functor ℕᵒᵖ C), (∀ (n : ℕ), CategoryTheory.Epi (F.map (CategoryTheory.homOfLE ⋯).op)) → ∀ (c : CategoryTheory.Limits.Cone F) (hc : CategoryTheory.Limits.IsLimit c) (n : ℕ), CategoryTheory.Epi (c.π.app (Opposite.op n))
The following examples are all not needed later, but are useful to gain some intuition for repleteness.
-
The category of sets is replete (Bhatt–Scholze, Example 3.1.4).
-
Let
kbe a field and\bar ka separable closure ofk. Then the category of sheaves on the small étale site of\operatorname{Spec} kis replete if and only if\bar kis a finite extension ofk(Bhatt–Scholze, Example 3.1.5). -
The category of fpqc sheaves, i.e., sheaves on the big fpqc site, is replete (Bhatt–Scholze, Example 3.1.7).
- No associated Lean code or declarations.
Let \mathcal{C} be replete and let
(F_n)_{n \in \mathbb{N}} \to (G_n)_{n \in \mathbb{N}} be a morphism of
inverse systems in \mathcal{C}. If F_n \to G_n and
F_{n+1} \to F_n \times_{G_n} G_{n+1} are epimorphisms for each
n \in \mathbb{N}, then \lim F_n \to \lim G_n is an epimorphism.
(Bhatt–Scholze, Lemma 3.1.8)
If \mathcal{C} is replete, countable products are exact.
(Bhatt–Scholze, Proposition 3.1.9)
- No associated Lean code or declarations.
Let \mathcal{C} be replete. If (F_n)_{n \in \mathbb{N}} is an inverse
system in \mathrm{Ab}(\mathcal{C}) with epimorphic transition maps, then
\lim F_n \cong \mathrm{R}\lim F_n.
(Bhatt–Scholze, Proposition 3.1.10)