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.
theorem
exists_mem_of_isClosed_of_nonempty
{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)]
(Z : (i : I) → Set ↥(D.obj i))
(hZc : ∀ (i : I), IsClosed (Z i))
(hZne : ∀ (i : I), (Z i).Nonempty)
(hZcpt : ∀ (i : I), IsCompact (Z i))
(hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (D.map f).base)) (Z i) (Z i'))
:
Suppose we have a cofiltered diagram of schemes whose transition maps are affine. The limit of a family of compatible nonempty quasicompact closed sets in the diagram is also nonempty.
theorem
exists_mem_of_isClosed_of_nonempty'
{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)]
{j : I}
(Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i))
(hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij))
(hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty)
(hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij))
(hstab :
∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j),
Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (D.map hi'i).base))
(Z i' (CategoryTheory.CategoryStruct.comp hi'i hij)) (Z i hij))
:
A variant of exists_mem_of_isClosed_of_nonempty where the closed sets are only defined
for the objects over a given j : I.