Nyll.SchemeTheory.FiniteEtale.InverseLimitRawModel

Module documentation

An actual stage model from standard recovered affine charts

The finite family of recovered overlap transitions descends by the real qcqs scheme Hom theorem. The descended local models retain their literal cartesian overlaps and their covering maps into the original object. Eventual equality and gluing then supply a finite-etale stage model.

theorem

exists_inverse_limit_model_of_standard_charts

L35 ↗

AlgebraicGeometry.FiniteEtale.exists_inverse_limit_model_of_standard_charts

Documentation

Standard recovered affine local models produce a finite-etale model over an original stage of the inverse system.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits
open AlgebraicGeometry.Scheme.Cover
open AlgebraicGeometry.AffineTransitionHom
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem exists_inverse_limit_model_of_standard_charts
    {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)]
    (i : I) (𝒰 : (D.obj i).OpenCover.{u}) [Finite 𝒰.I₀]
    [∀ a : 𝒰.I₀, IsAffine (𝒰.X a)]
    (M : ∀ a : 𝒰.I₀, Over (𝒰.X a)) [∀ a : 𝒰.I₀, IsFiniteEtale (M a).hom]
    (X : FiniteEtale c.pt)
    (e : ∀ a : 𝒰.I₀,
      (Over.pullback (pullback.fst (𝒰.f a) (c.π.app i))).obj (M a) ≅
        (Over.pullback (pullback.snd (𝒰.f a) (c.π.app i))).obj
          ((FiniteEtale.forget c.pt).obj X)) :
    ∃ (j : I) (N : FiniteEtale (D.obj j)),
      Nonempty ((FiniteEtale.pullback (c.π.app j)).obj N ≅ X)

Module documentation

An actual stage model from standard recovered affine charts

Declarations

exists_inverse_limit_model_of_standard_charts