Module

PureInseparableDescent.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.PureInseparableDescent

2 declarations indexed from sourceView source ↗

Module documentation

Pure Inseparable Descent

Actual finite étale covers descend through an arbitrary purely inseparable extension of the constant field.

Imports3

Imported by3

theorem

exists_model_of_purelyInseparable_constant_extension

L25 ↗

AlgebraicGeometry.FiniteEtale.exists_model_of_purelyInseparable_constant_extension

Documentation

Actual finite étale covers descend through an arbitrary purely inseparable extension of the constant field.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
open EtaleFundamentalGroups

Lean source · statement

theorem exists_model_of_purelyInseparable_constant_extension
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsPurelyInseparable k L]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    (Z : FiniteEtale (Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)) :
    ∃ N : FiniteEtale X, Nonempty ((FiniteEtale.pullback
      (Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)).obj N ≅ Z)

theorem

pullback_isEquivalence_of_purelyInseparable_constant_extension

L54 ↗

AlgebraicGeometry.FiniteEtale.pullback_isEquivalence_of_purelyInseparable_constant_extension