NYLL
Module

ConstantFieldRebase.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.ConstantFieldRebase
4 declarations indexed from sourceView source ↗

Module documentation

Constant Field Rebase

The standard iterated cover chart is the original chart after extending coefficients.

Imports3
Imported by2

Declarations

def

constantFieldRebasedChartIso

L32 ↗
EtaleFundamentalGroups.constantFieldRebasedChartIso
Documentation

The standard iterated cover chart is the original chart after extending coefficients.

Source context 13 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L) (X : Scheme.{u})
variable (f : X ⟶ Spec (CommRingCat.of k)) (𝒰 : X.OpenCover)
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "ψ" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "UF" => constantFieldOpenCover k F X f 𝒰
local notation "UL" => constantFieldOpenCover k L X f 𝒰
local notation "UD" => constantFieldOpenCover F L (pullback φF f) (pullback.fst φF f) UF
Lean source · statement
def constantFieldRebasedChartIso (i : 𝒰.I₀) :
    pullback ψ (coefficientModelMap φF f (𝒰.f i) ≫ pullback.fst φF f) ≅ pullback φL (𝒰.f i ≫ f)
theorem

constantFieldRebasedChartIso_naturality

L37 ↗
EtaleFundamentalGroups.constantFieldRebasedChartIso_naturality
Source context 13 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L) (X : Scheme.{u})
variable (f : X ⟶ Spec (CommRingCat.of k)) (𝒰 : X.OpenCover)
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "ψ" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "UF" => constantFieldOpenCover k F X f 𝒰
local notation "UL" => constantFieldOpenCover k L X f 𝒰
local notation "UD" => constantFieldOpenCover F L (pullback φF f) (pullback.fst φF f) UF
Lean source · statement
theorem constantFieldRebasedChartIso_naturality (i : 𝒰.I₀) :
    (constantFieldRebasedChartIso k L F X f 𝒰 i).hom ≫ coefficientModelMap φL f (𝒰.f i) =
      coefficientModelMap ψ (pullback.fst φF f) (coefficientModelMap φF f (𝒰.f i)) ≫
        (constantFieldTowerIso k L F X f).hom
def

constantFieldRebasedRecoveryIso

L53 ↗
EtaleFundamentalGroups.constantFieldRebasedRecoveryIso
Documentation

Recovery of local finite étale models on the standard constant-field cover, after changing the ground field to the common finite stage.

Source context 13 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L) (X : Scheme.{u})
variable (f : X ⟶ Spec (CommRingCat.of k)) (𝒰 : X.OpenCover)
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "ψ" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "UF" => constantFieldOpenCover k F X f 𝒰
local notation "UL" => constantFieldOpenCover k L X f 𝒰
local notation "UD" => constantFieldOpenCover F L (pullback φF f) (pullback.fst φF f) UF
Lean source · full declaration
def constantFieldRebasedRecoveryIso (i : 𝒰.I₀)
    (M : FiniteEtale (pullback φF (𝒰.f i ≫ f)))
    (Z : FiniteEtale (pullback φL f))
    (e : (FiniteEtale.pullback
        (pullback.map φL (𝒰.f i ≫ f) φF (𝒰.f i ≫ f) ψ (𝟙 (𝒰.X i))
          (𝟙 (Spec (CommRingCat.of k)))
          (by rw [Category.comp_id, ← Spec.map_comp]; rfl)
          (by rw [Category.comp_id, Category.id_comp]))).obj M ≅
      (FiniteEtale.pullback (coefficientModelMap φL f (𝒰.f i))).obj Z) :
    (FiniteEtale.pullback (pullback.snd ψ (coefficientModelMap φF f (𝒰.f i) ≫ pullback.fst φF
      f))).obj M ≅
      (FiniteEtale.pullback (coefficientModelMap ψ (pullback.fst φF f) (coefficientModelMap φF f
        (𝒰.f i)))).obj
        ((FiniteEtale.pullback (constantFieldTowerIso k L F X f).hom).obj Z) := by
  let eU := constantFieldRebasedChartIso k L F X f 𝒰 i
  let eX := constantFieldTowerIso k L F X f
  let cU : pullback φL (𝒰.f i ≫ f) ⟶ pullback φF (𝒰.f i ≫ f) :=
    pullback.map φL (𝒰.f i ≫ f) φF (𝒰.f i ≫ f) ψ (𝟙 (𝒰.X i))
      (𝟙 (Spec (CommRingCat.of k)))
      (by rw [Category.comp_id, ← Spec.map_comp]; rfl)
      (by rw [Category.comp_id, Category.id_comp])
  have heU : eU.hom ≫ cU = pullback.snd ψ (coefficientModelMap φF f (𝒰.f i) ≫ pullback.fst φF f)
    := by
    change ((pullback.congrHom rfl (pullback.lift_fst _ _ _)).hom ≫
      (constantFieldTowerIso k L F (𝒰.X i) (𝒰.f i ≫ f)).hom) ≫ cU = _
    rw [Category.assoc, constantFieldTowerIso_hom_coefficientMap]
    exact pullback.lift_snd _ _ _
  have hnat : eU.hom ≫ coefficientModelMap φL f (𝒰.f i) = coefficientModelMap ψ (pullback.fst φF
    f) (coefficientModelMap φF f (𝒰.f i)) ≫ eX.hom :=
    constantFieldRebasedChartIso_naturality k L F X f 𝒰 i
  exact
    (FiniteEtale.finiteEtalePullbackCompObjIso eU.hom cU
      (pullback.snd ψ (coefficientModelMap φF f (𝒰.f i) ≫ pullback.fst φF f)) heU M).symm ≪≫
    (FiniteEtale.pullback eU.hom).mapIso e ≪≫
    FiniteEtale.finiteEtalePullbackCompObjIso eU.hom (coefficientModelMap φL f (𝒰.f i))
      (coefficientModelMap ψ (pullback.fst φF f) (coefficientModelMap φF f (𝒰.f i)) ≫ eX.hom) hnat
        Z ≪≫
    (FiniteEtale.finiteEtalePullbackCompObjIso (coefficientModelMap ψ (pullback.fst φF f)
      (coefficientModelMap φF f (𝒰.f i))) eX.hom
      (coefficientModelMap ψ (pullback.fst φF f) (coefficientModelMap φF f (𝒰.f i)) ≫ eX.hom) rfl
        Z).symm
theorem

exists_finiteIntermediateField_rebased_local_models

L101 ↗
EtaleFundamentalGroups.exists_finiteIntermediateField_rebased_local_models
Documentation

An actual finite étale cover over an algebraic extension supplies a common finite coefficient field and recovered local models for the standard rebased cover.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace EtaleFundamentalGroups
Lean source · full declaration
theorem exists_finiteIntermediateField_rebased_local_models (k L : Type u) [Field k] [Field L]
  [Algebra k L] [Algebra.IsAlgebraic k L]
    (X : Scheme.{u}) [CompactSpace X] (f : X ⟶ Spec (CommRingCat.of k))
    (Z : FiniteEtale (pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)) :
    let 𝒰 := X.affineCover.finiteSubcover
    ∃ F : IntermediateField k L, FiniteDimensional k F ∧
      ∃ M : ∀ i : 𝒰.I₀, FiniteEtale
          (pullback (Spec.map (CommRingCat.ofHom (algebraMap k F))) (𝒰.f i ≫ f)),
        ∀ i : 𝒰.I₀, Nonempty ((FiniteEtale.pullback
          (pullback.snd (Spec.map (CommRingCat.ofHom F.val.toRingHom))
            (coefficientModelMap (Spec.map (CommRingCat.ofHom (algebraMap k F))) f (𝒰.f i) ≫
              pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k F))) f))).obj
              (M i) ≅
          (FiniteEtale.pullback (coefficientModelMap (Spec.map (CommRingCat.ofHom F.val.toRingHom))
            (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap k F))) f)
            (coefficientModelMap (Spec.map (CommRingCat.ofHom (algebraMap k F))) f (𝒰.f i)))).obj
            ((FiniteEtale.pullback (constantFieldTowerIso k L F X f).hom).obj Z)) := by
  let 𝒰 := X.affineCover.finiteSubcover
  let : ∀ i : 𝒰.I₀, IsAffine (𝒰.X i) := fun i ↦ inferInstanceAs (IsAffine (Spec _))
  obtain ⟨F, hF, M, hrec⟩ :=
    FiniteEtale.exists_finiteIntermediateField_affine_scheme_model_family k L
      𝒰.X (fun i ↦ 𝒰.f i ≫ f)
      (fun i ↦ (FiniteEtale.pullback ((constantFieldOpenCover k L X f 𝒰).f i)).obj Z)
  refine ⟨F, hF, M, ?_⟩
  intro i
  exact ⟨constantFieldRebasedRecoveryIso k L F X f 𝒰 i (M i) Z (hrec i).some⟩

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.