4. Pro-categories
Let \mathcal{C} be a category. The category \pro{\mathcal{C}} is the full
subcategory of \mathrm{Fun}(\mathcal{C}, \mathrm{Set})^{\mathrm{op}} on the
functors that are cofiltered limits of representable functors. This category
satisfies the following universal property:
- No associated Lean code or declarations.
(Universal property of \pro{\mathcal{C}}.) Let \mathcal{D} be a category
with cofiltered limits. The restriction functor
\mathrm{Fun}(\pro{\mathcal{C}}, \mathcal{D}) \to \mathrm{Fun}(\mathcal{C}, \mathcal{D})
admits a left-adjoint that induces an equivalence on the full subcategory of
\mathrm{Fun}(\pro{\mathcal{C}}, \mathcal{D}) on functors preserving
cofiltered limits.
The left-adjoint is the left Kan extension along the inclusion
\mathcal{C} \to \pro{\mathcal{C}}.
Let now \mathcal{K} be a small category. The canonical functor
\mathcal{C} \to \pro{\mathcal{C}} induces a functor
\mathrm{Fun}(\mathcal{K}, \mathcal{C}) \to \mathrm{Fun}(\mathcal{K}, \pro{\mathcal{C}}).
Since the right hand side admits small cofiltered limits, the universal
property of \pro{\mathcal{C}} induces a canonical functor
\Phi_{\mathcal{K}}\colon \pro{\mathrm{Fun}(\mathcal{K}, \mathcal{C})} \longrightarrow \mathrm{Fun}(\mathcal{K}, \pro{\mathcal{C}}).
- No associated Lean code or declarations.
Suppose \mathcal{K} is a finite category and every object of \mathcal{K}
admits no non-trivial automorphisms. Then the natural functor
\Phi_{\mathcal{K}} induces an equivalence of categories.
See Kashiwara–Schapira, Theorem 6.4.3.
- No associated Lean code or declarations.
Note that Proposition 4.2 in particular implies that if there
is a finite family of morphisms f_i \colon X_i \to X in
\pro{\mathcal{C}}, there exists a diagram \mathcal{J} such that
X = \lim_{j \in \mathcal{J}} Y_j and
X_i = \lim_{j \in \mathcal{J}} Y_{ij} and
f_i = \lim_{j \in \mathcal{J}} f_{ij} for morphisms
f_{ij}\colon Y_{ij} \to Y_j.
- No associated Lean code or declarations.
Let \mathcal{A} be a category with cofiltered limits and suppose there
exists a fully faithful functor i\colon \mathcal{C} \to \mathcal{A} such
that i(X) is cocompact for all X \in \mathcal{C}. Then
\lim_{\mathcal{A}} \circ \; \pro{i}\colon \pro{\mathcal{C}} \to \mathcal{A}
is fully faithful.
See nlab.
- No associated Lean code or declarations.
Let P be a property of objects of a category \mathcal{A} that implies
finitely presented. Denote by \mathcal{A}_P (resp.
\mathcal{A}_{\pro{P}}) the full subcategory defined by P (resp.
\pro{P}). Suppose \mathcal{A} has cofiltered limits, then
\lim_{\mathcal{A}} induces an equivalence
\pro{\mathcal{A}_{P}} \cong \mathcal{A}_{\pro{P}}.
Follows from Proposition 4.4, because by definition
\mathcal{A}_{\pro{P}} is the essential image of
\lim_{\mathcal{A}}(\pro{\mathcal{A}_{P}}).
Note that Corollary 4.5 does not apply to
\mathcal{A} = \mathrm{Scheme} / X and P = \text{étale}, because
\mathrm{Scheme} / X does not have all cofiltered limits. It does apply in
the case of \mathcal{A} = \mathrm{AffScheme} / X though, or in the case
\mathrm{CRing}^{\mathrm{op}} / R.
Recall the following definition:
- No associated Lean code or declarations.
A category \mathcal{C} is precoherent if given a finite effective
epimorphism family f\colon X_i \to X and a morphism p\colon Y \to X,
there exists a finite effective epimorphism family g\colon Y_j \to Y that
factors through f.
A morphism f\colon X \to Y in \et{S} is an effective epimorphism if and
only if it is surjective.
Lean code for Lemma4.7●2 theorems
Associated Lean declarations
-
theoremdefined in Proetale/Topology/Coherent/Etale.leancomplete
theorem AlgebraicGeometry.Scheme.Etale.effectiveEpi_of_surjective.{u_1} {S : AlgebraicGeometry.Scheme} {X Y : S.Etale} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f.left] : CategoryTheory.EffectiveEpi f
theorem AlgebraicGeometry.Scheme.Etale.effectiveEpi_of_surjective.{u_1} {S : AlgebraicGeometry.Scheme} {X Y : S.Etale} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f.left] : CategoryTheory.EffectiveEpi f
A morphism in the small étale site is an epimorphism if and only if it is surjective.
-
theoremdefined in Proetale/Topology/Coherent/Etale.leancomplete
theorem AlgebraicGeometry.Scheme.Etale.surjective_of_epi.{u_1} {S : AlgebraicGeometry.Scheme} {X Y : S.Etale} (f : X ⟶ Y) [CategoryTheory.Epi f] : AlgebraicGeometry.Surjective f.left
theorem AlgebraicGeometry.Scheme.Etale.surjective_of_epi.{u_1} {S : AlgebraicGeometry.Scheme} {X Y : S.Etale} (f : X ⟶ Y) [CategoryTheory.Epi f] : AlgebraicGeometry.Surjective f.left
A morphism in the small étale site is an epimorphism if and only if it is surjective.
One direction follows from the fact that the fpqc topology is subcanonical. The
converse holds, because étale morphisms are open: If f\colon X \to Y is an
étale morphism we may glue two copies of Y along the inclusion of the image
of f. If f is not surjective, the two inclusions of Y into the
amalgamated sum are different, but by construction they agree on the image of
f. Hence f is not an epimorphism.
- No associated Lean code or declarations.
The category of schemes is finitary extensive.
Since the Zariski topology is subcanonical, the category of schemes embeds into the big Zariski topos, which is finitary extensive. Since the Yoneda embedding preserves finite coproducts, the claim follows.
The category \et{X} is precoherent.
Lean code for Lemma4.9●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Topology/Coherent/Etale.leancomplete
theorem AlgebraicGeometry.Scheme.Etale.precoherent.{u} (S : AlgebraicGeometry.Scheme) : CategoryTheory.Precoherent S.Etale
theorem AlgebraicGeometry.Scheme.Etale.precoherent.{u} (S : AlgebraicGeometry.Scheme) : CategoryTheory.Precoherent S.Etale
The small étale site of a scheme is precoherent.
The category of schemes is finitary extensive, so the same holds for
\et{X}. By Lemma 4.7 the effective epimorphisms in
\et{X} are the surjective morphisms, hence being an effective epimorphism is
stable under base change. Thus \et{X} is preregular and therefore
precoherent.
- No associated Lean code or declarations.
If \mathcal{C} is precoherent, also \pro{\mathcal{C}} is precoherent.