EtaleFundamentalGroups.exists_affine_model_of_purelyInseparable_extension
A finite étale cover of an affine scheme descends across an arbitrary purely inseparable extension of constants.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroupsLean source · statement
theorem exists_affine_model_of_purelyInseparable_extension
(k L : Type u) [Field k] [Field L] [Algebra k L] [IsPurelyInseparable k L]
(X : Scheme.{u}) [IsAffine X] (f : X ⟶ Spec (.of k))
(Z : FiniteEtale (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)) :
∃ M : FiniteEtale X,
Nonempty ((FiniteEtale.pullback
(pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)).obj M ≅ Z)