Module

PureInseparableCoverRecovery.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.PureInseparableCoverRecovery

2 declarations indexed from sourceView source ↗

Module documentation

Pure Inseparable Cover Recovery

Recovery on a literal coefficient chart gives recovery on the standard pullback chart, with both structure maps fixed.

Imports3

Imported by2

def

constantFieldChartRecoveryIso

L24 ↗

EtaleFundamentalGroups.constantFieldChartRecoveryIso

Documentation

Recovery on a literal coefficient chart gives recovery on the standard pullback chart, with both structure maps fixed.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u
namespace EtaleFundamentalGroups

Lean source · statement

def constantFieldChartRecoveryIso
    (k L : Type u) [Field k] [Field L] [Algebra k L]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) (𝒰 : X.OpenCover) (i : 𝒰.I₀)
    (M : AlgebraicGeometry.FiniteEtale (𝒰.X i))
    (Z : AlgebraicGeometry.FiniteEtale
      (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))
    (e : (AlgebraicGeometry.FiniteEtale.pullback
      (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) (𝒰.f i ≫ f))).obj M ≅
      (AlgebraicGeometry.FiniteEtale.pullback ((constantFieldOpenCover k L X f 𝒰).f i)).obj Z) :
    (AlgebraicGeometry.FiniteEtale.pullback
      (pullback.fst (𝒰.f i) (pullback.snd
        (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))).obj M ≅
      (AlgebraicGeometry.FiniteEtale.pullback
        (pullback.snd (𝒰.f i) (pullback.snd
          (Spec.map (CommRingCat.ofHom (algebraMap k L))) f))).obj Z

theorem

exists_purelyInseparable_affineCover_models

L72 ↗

EtaleFundamentalGroups.exists_purelyInseparable_affineCover_models