NYLL
Module

ConstantFieldTower.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.ConstantFieldTower
10 declarations indexed from sourceView source ↗

Module documentation

Constant Field Tower

Rebase a constant extension through an actual intermediate field.

Imports5
Imported by4

Declarations

theorem

coefficientSpec_comp

L29 ↗
EtaleFundamentalGroups.coefficientSpec_comp
Source context 9 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L)
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)
Lean source · statement
theorem coefficientSpec_comp : ψ ≫ φF = φL
def

constantFieldTowerIso

L41 ↗
EtaleFundamentalGroups.constantFieldTowerIso
Documentation

Rebase a constant extension through an actual intermediate field.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L)
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)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "c" =>
  pullback.map φL f φF f ψ (𝟙 X) (𝟙 (Spec (CommRingCat.of k)))
    (Eq.trans (Category.comp_id φL) (Eq.symm (coefficientSpec_comp k L F)))
    (Eq.trans (Category.comp_id f) (Eq.symm (Category.id_comp f)))
Lean source · statement
def constantFieldTowerIso : pullback ψ (pullback.fst φF f) ≅ pullback φL f
theorem

constantFieldTowerIso_hom_fst

L46 ↗
EtaleFundamentalGroups.constantFieldTowerIso_hom_fst
Documentation

The tower comparison preserves the coefficient coordinate.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L)
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)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "c" =>
  pullback.map φL f φF f ψ (𝟙 X) (𝟙 (Spec (CommRingCat.of k)))
    (Eq.trans (Category.comp_id φL) (Eq.symm (coefficientSpec_comp k L F)))
    (Eq.trans (Category.comp_id f) (Eq.symm (Category.id_comp f)))
Lean source · statement
theorem constantFieldTowerIso_hom_fst :
    (constantFieldTowerIso k L F X f).hom ≫ pullback.fst φL f =
      pullback.fst ψ (pullback.fst φF f)
theorem

constantFieldTowerIso_hom_snd

L53 ↗
EtaleFundamentalGroups.constantFieldTowerIso_hom_snd
Documentation

The tower comparison preserves the underlying original-scheme coordinate.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L)
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)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "c" =>
  pullback.map φL f φF f ψ (𝟙 X) (𝟙 (Spec (CommRingCat.of k)))
    (Eq.trans (Category.comp_id φL) (Eq.symm (coefficientSpec_comp k L F)))
    (Eq.trans (Category.comp_id f) (Eq.symm (Category.id_comp f)))
Lean source · statement
theorem constantFieldTowerIso_hom_snd :
    (constantFieldTowerIso k L F X f).hom ≫ pullback.snd φL f =
      pullback.snd ψ (pullback.fst φF f) ≫ pullback.snd φF f
theorem

constantFieldTowerIso_hom_coefficientMap

L60 ↗
EtaleFundamentalGroups.constantFieldTowerIso_hom_coefficientMap
Documentation

The iterated base-change projection is the literal coefficient inclusion.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L)
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)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "c" =>
  pullback.map φL f φF f ψ (𝟙 X) (𝟙 (Spec (CommRingCat.of k)))
    (Eq.trans (Category.comp_id φL) (Eq.symm (coefficientSpec_comp k L F)))
    (Eq.trans (Category.comp_id f) (Eq.symm (Category.id_comp f)))
Lean source · statement
theorem constantFieldTowerIso_hom_coefficientMap :
    (constantFieldTowerIso k L F X f).hom ≫ c = pullback.snd ψ (pullback.fst φF f)
theorem

constantFieldTowerIso_inv_snd

L70 ↗
EtaleFundamentalGroups.constantFieldTowerIso_inv_snd
Documentation

The inverse comparison also identifies the two projection maps.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L)
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)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "c" =>
  pullback.map φL f φF f ψ (𝟙 X) (𝟙 (Spec (CommRingCat.of k)))
    (Eq.trans (Category.comp_id φL) (Eq.symm (coefficientSpec_comp k L F)))
    (Eq.trans (Category.comp_id f) (Eq.symm (Category.id_comp f)))
Lean source · statement
theorem constantFieldTowerIso_inv_snd :
    (constantFieldTowerIso k L F X f).inv ≫ pullback.snd ψ (pullback.fst φF f) = c
def

constantFieldTowerCoverMap

L76 ↗
EtaleFundamentalGroups.constantFieldTowerCoverMap
Documentation

The chart map after rebasing the native constant-field cover through F.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L)
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)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "c" =>
  pullback.map φL f φF f ψ (𝟙 X) (𝟙 (Spec (CommRingCat.of k)))
    (Eq.trans (Category.comp_id φL) (Eq.symm (coefficientSpec_comp k L F)))
    (Eq.trans (Category.comp_id f) (Eq.symm (Category.id_comp f)))
Lean source · statement
def constantFieldTowerCoverMap (𝒰 : Scheme.OpenCover.{v} X) (i : 𝒰.I₀) :
    pullback ψ (pullback.fst φF (𝒰.f i ≫ f)) ⟶ pullback ψ (pullback.fst φF f)
theorem

constantFieldTowerIso_cover_naturality

L86 ↗
EtaleFundamentalGroups.constantFieldTowerIso_cover_naturality
Documentation

The tower comparisons commute with the actual constant-field chart inclusions.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L)
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)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "c" =>
  pullback.map φL f φF f ψ (𝟙 X) (𝟙 (Spec (CommRingCat.of k)))
    (Eq.trans (Category.comp_id φL) (Eq.symm (coefficientSpec_comp k L F)))
    (Eq.trans (Category.comp_id f) (Eq.symm (Category.id_comp f)))
Lean source · statement
theorem constantFieldTowerIso_cover_naturality (𝒰 : Scheme.OpenCover.{v} X) (i : 𝒰.I₀) :
    constantFieldTowerCoverMap k L F X f 𝒰 i ≫ (constantFieldTowerIso k L F X f).hom =
      (constantFieldTowerIso k L F (𝒰.X i) (𝒰.f i ≫ f)).hom ≫
        (constantFieldOpenCover k L X f 𝒰).f i
def

constantFieldTowerOpenCover

L115 ↗
EtaleFundamentalGroups.constantFieldTowerOpenCover
Documentation

The rebased charts form an actual open cover of the iterated constant extension.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L)
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)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "c" =>
  pullback.map φL f φF f ψ (𝟙 X) (𝟙 (Spec (CommRingCat.of k)))
    (Eq.trans (Category.comp_id φL) (Eq.symm (coefficientSpec_comp k L F)))
    (Eq.trans (Category.comp_id f) (Eq.symm (Category.id_comp f)))
Lean source · statement
def constantFieldTowerOpenCover (𝒰 : Scheme.OpenCover.{v} X) :
    Scheme.OpenCover.{v} (pullback ψ (pullback.fst φF f))
def

constantFieldTowerRecoveryIso

L130 ↗
EtaleFundamentalGroups.constantFieldTowerRecoveryIso
Documentation

Transport an actual local-model recovery isomorphism to the rebased field.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry
universe u v
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (F : IntermediateField k L)
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)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "c" =>
  pullback.map φL f φF f ψ (𝟙 X) (𝟙 (Spec (CommRingCat.of k)))
    (Eq.trans (Category.comp_id φL) (Eq.symm (coefficientSpec_comp k L F)))
    (Eq.trans (Category.comp_id f) (Eq.symm (Category.id_comp f)))
Lean source · full declaration
def constantFieldTowerRecoveryIso (𝒰 : Scheme.OpenCover.{v} X) (i : 𝒰.I₀)
    (M : AlgebraicGeometry.FiniteEtale (pullback φF (𝒰.f i ≫ f)))
    (Z : AlgebraicGeometry.FiniteEtale (pullback φL f))
    (e : (AlgebraicGeometry.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 ≅
      (AlgebraicGeometry.FiniteEtale.pullback
        ((constantFieldOpenCover k L X f 𝒰).f i)).obj Z) :
    (AlgebraicGeometry.FiniteEtale.pullback
        (pullback.snd ψ (pullback.fst φF (𝒰.f i ≫ f)))).obj M ≅
      (AlgebraicGeometry.FiniteEtale.pullback
        (constantFieldTowerCoverMap k L F X f 𝒰 i)).obj
          ((AlgebraicGeometry.FiniteEtale.pullback (constantFieldTowerIso k L F X f).hom).obj Z)
            := by
  let eU : pullback ψ (pullback.fst φF (𝒰.f i ≫ f)) ≅ pullback φL (𝒰.f i ≫ f) :=
    constantFieldTowerIso k L F (𝒰.X i) (𝒰.f i ≫ f)
  let eX : pullback ψ (pullback.fst φF f) ≅ pullback φL f :=
    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])
  let uL : pullback φL (𝒰.f i ≫ f) ⟶ pullback φL f :=
    (constantFieldOpenCover k L X f 𝒰).f i
  let uD : pullback ψ (pullback.fst φF (𝒰.f i ≫ f)) ⟶ pullback ψ (pullback.fst φF f) :=
    constantFieldTowerCoverMap k L F X f 𝒰 i
  have heU : eU.hom ≫ cU = pullback.snd ψ (pullback.fst φF (𝒰.f i ≫ f)) :=
    constantFieldTowerIso_hom_coefficientMap k L F (𝒰.X i) (𝒰.f i ≫ f)
  have hnat : uD ≫ eX.hom = eU.hom ≫ uL :=
    constantFieldTowerIso_cover_naturality k L F X f 𝒰 i
  exact
    (AlgebraicGeometry.FiniteEtale.finiteEtalePullbackCompObjIso eU.hom cU
      (pullback.snd ψ (pullback.fst φF (𝒰.f i ≫ f))) heU M).symm ≪≫
    (AlgebraicGeometry.FiniteEtale.pullback eU.hom).mapIso e ≪≫
    AlgebraicGeometry.FiniteEtale.finiteEtalePullbackCompObjIso eU.hom uL
      (uD ≫ eX.hom) hnat.symm Z ≪≫
    (AlgebraicGeometry.FiniteEtale.finiteEtalePullbackCompObjIso uD eX.hom
      (uD ≫ eX.hom) rfl Z).symm

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