EtaleFundamentalGroups.exists_punctured_finiteEtale_extension_iff_sections_finiteEtale
A punctured finite étale cover extends if and only if its actual global-sections algebra is finite étale.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Limits AlgebraicGeometry TopologicalSpace
namespace EtaleFundamentalGroups
universe uLean source · statement
theorem exists_punctured_finiteEtale_extension_iff_sections_finiteEtale
(R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
(hdepth : (2 : ℕ∞) ≤ Module.depth R R)
{Y : Scheme.{u}} (f : Y ⟶ Scheme.puncturedSpectrum R) [IsFiniteEtale f] :
(∃ V : FiniteEtale (Spec (.of R)),
Nonempty ((FiniteEtale.pullback (Scheme.puncturedSpectrumInclusion R)).obj V ≅
FiniteEtale.mk f)) ↔
((Scheme.ΓSpecIso (.of R)).inv ≫
(f ≫ Scheme.puncturedSpectrumInclusion R).appTop).hom.FiniteEtale