AlgebraicGeometry.FiniteEtale.exists_inverse_limit_model
Every finite-etale object over the actual inverse limit of qcqs schemes with affine transition maps descends to an original stage. The recovery isomorphism is along the literal native finite-etale pullback functor.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtaleLean source · statement
theorem exists_inverse_limit_model
{I : Type u} [Category.{u} I] [IsCofiltered I]
(D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
[∀ {i j : I} (h : i ⟶ j), IsAffineHom (D.map h)]
[∀ i : I, CompactSpace (D.obj i)] [∀ i : I, QuasiSeparatedSpace (D.obj i)]
(X : FiniteEtale c.pt) :
∃ (i : I) (N : FiniteEtale (D.obj i)),
Nonempty ((FiniteEtale.pullback (c.π.app i)).obj N ≅ X)