AlgebraicGeometry.FiniteEtale.exists_maximal_open_extension
A finite étale cover of an open in a topologically Noetherian scheme has an extension which cannot be extended to a strictly larger open.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherenceLean source · statement
theorem exists_maximal_open_extension
{X : Scheme.{u}} [NoetherianSpace X]
(U : X.Opens) (V : FiniteEtale U.toScheme) :
∃ (N : X.Opens) (hUN : U ≤ N) (W : FiniteEtale N.toScheme),
Nonempty ((pullback (X.homOfLE hUN)).obj W ≅ V) ∧
∀ (M : X.Opens) (hNM : N ≤ M) (Z : FiniteEtale M.toScheme),
Nonempty ((pullback (X.homOfLE hNM)).obj Z ≅ W) → M ≤ N