Inverse limits of schemes with affine transition maps #
In this file, we develop API for inverse limits of schemes with affine transition maps, following EGA IV 8 and https://stacks.math.columbia.edu/tag/01YT.
theorem
Scheme.nonempty_of_isLimit
{I : Type u}
[CategoryTheory.Category.{u, u} I]
(D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
(c : CategoryTheory.Limits.Cone D)
(hc : CategoryTheory.Limits.IsLimit c)
[CategoryTheory.IsCofilteredOrEmpty I]
[∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
[∀ (i : I), Nonempty ↥(D.obj i)]
[∀ (i : I), CompactSpace ↥(D.obj i)]
:
Suppose we have a cofiltered diagram of nonempty quasi-compact schemes, whose transition maps are affine. Then the limit is also nonempty.