NYLL
Module

FiniteTowerModel.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FiniteField.FiniteTowerModel
9 declarations indexed from sourceView source ↗

Module documentation

Finite Tower Model

Two finite coefficient extensions give the model over their actual composite subfield.

Imports5
Imported by2

Declarations

theorem

finiteIntermediateTowerSpec_comp

L33 ↗
EtaleFundamentalGroups.finiteIntermediateTowerSpec_comp
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) (E : IntermediateField F L)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φE" => Spec.map (CommRingCat.ofHom (algebraMap k E))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "η" => Spec.map (CommRingCat.ofHom (algebraMap F E))
local notation "ψF" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "ψE" => Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val E)))
Lean source · statement
theorem finiteIntermediateTowerSpec_comp : η ≫ φF = φE
def

finiteIntermediateTowerIso

L38 ↗
EtaleFundamentalGroups.finiteIntermediateTowerIso
Documentation

Two finite coefficient extensions give the model over their actual composite subfield.

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) (E : IntermediateField F L)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φE" => Spec.map (CommRingCat.ofHom (algebraMap k E))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "η" => Spec.map (CommRingCat.ofHom (algebraMap F E))
local notation "ψF" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "ψE" => Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val E)))
Lean source · statement
def finiteIntermediateTowerIso : pullback η (pullback.fst φF f) ≅ pullback φE f
theorem

finiteIntermediateTowerIso_hom_fst

L42 ↗
EtaleFundamentalGroups.finiteIntermediateTowerIso_hom_fst
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) (E : IntermediateField F L)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φE" => Spec.map (CommRingCat.ofHom (algebraMap k E))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "η" => Spec.map (CommRingCat.ofHom (algebraMap F E))
local notation "ψF" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "ψE" => Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val E)))
Lean source · statement
theorem finiteIntermediateTowerIso_hom_fst :
    (finiteIntermediateTowerIso k L F E X f).hom ≫ pullback.fst φE f =
      pullback.fst η (pullback.fst φF f)
theorem

finiteIntermediateTowerIso_hom_snd

L49 ↗
EtaleFundamentalGroups.finiteIntermediateTowerIso_hom_snd
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) (E : IntermediateField F L)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φE" => Spec.map (CommRingCat.ofHom (algebraMap k E))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "η" => Spec.map (CommRingCat.ofHom (algebraMap F E))
local notation "ψF" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "ψE" => Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val E)))
Lean source · statement
theorem finiteIntermediateTowerIso_hom_snd :
    (finiteIntermediateTowerIso k L F E X f).hom ≫ pullback.snd φE f =
      pullback.snd η (pullback.fst φF f) ≫ pullback.snd φF f
theorem

finiteIntermediateTowerInclusion_comp

L56 ↗
EtaleFundamentalGroups.finiteIntermediateTowerInclusion_comp
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) (E : IntermediateField F L)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φE" => Spec.map (CommRingCat.ofHom (algebraMap k E))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "η" => Spec.map (CommRingCat.ofHom (algebraMap F E))
local notation "ψF" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "ψE" => Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val E)))
Lean source · statement
theorem finiteIntermediateTowerInclusion_comp : ψE ≫ η = ψF
def

finiteIntermediateTowerProjection

L61 ↗
EtaleFundamentalGroups.finiteIntermediateTowerProjection
Documentation

The actual coefficient inclusion between the two relative stages.

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) (E : IntermediateField F L)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φE" => Spec.map (CommRingCat.ofHom (algebraMap k E))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "η" => Spec.map (CommRingCat.ofHom (algebraMap F E))
local notation "ψF" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "ψE" => Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val E)))
Lean source · statement
def finiteIntermediateTowerProjection :
    pullback ψF (pullback.fst φF f) ⟶ pullback η (pullback.fst φF f)
theorem

finiteIntermediateTowerProjection_eq_cone

L69 ↗
EtaleFundamentalGroups.finiteIntermediateTowerProjection_eq_cone
Documentation

For an adjoined finite stage, the relative coefficient inclusion is the actual leg of the inverse-limit cone.

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) (E : IntermediateField F L)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φE" => Spec.map (CommRingCat.ofHom (algebraMap k E))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "η" => Spec.map (CommRingCat.ofHom (algebraMap F E))
local notation "ψF" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "ψE" => Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val E)))
Lean source · statement
theorem finiteIntermediateTowerProjection_eq_cone (s : Finset L) :
    finiteIntermediateTowerProjection k L F (IntermediateField.adjoin F (s : Set L)) X f =
      (constantFieldInverseLimitCone F L (pullback φF f) (pullback.fst φF f)).π.app
        (Opposite.op s)
theorem

finiteIntermediateTowerIso_projection

L83 ↗
EtaleFundamentalGroups.finiteIntermediateTowerIso_projection
Documentation

Flattening finite stages commutes with their literal inclusion into the full extension.

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) (E : IntermediateField F L)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φE" => Spec.map (CommRingCat.ofHom (algebraMap k E))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "η" => Spec.map (CommRingCat.ofHom (algebraMap F E))
local notation "ψF" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "ψE" => Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val E)))
Lean source · full declaration
theorem finiteIntermediateTowerIso_projection :
    finiteIntermediateTowerProjection k L F E X f ≫
        (finiteIntermediateTowerIso k L F E X f).hom =
      (constantFieldTowerIso k L F X f).hom ≫
        pullback.map φL f φE f
          (Spec.map (CommRingCat.ofHom E.val.toRingHom))
          (𝟙 X) (𝟙 _)
          (by rw [Category.comp_id, ← Spec.map_comp]; rfl)
          (by rw [Category.comp_id, Category.id_comp]) := by
  apply pullback.hom_ext
  · simp only [Category.assoc, finiteIntermediateTowerIso_hom_fst,
      finiteIntermediateTowerProjection, pullback.map, pullback.lift_fst]
    rw [← Category.assoc, constantFieldTowerIso_hom_fst]
  · simp only [Category.assoc, finiteIntermediateTowerIso_hom_snd,
      finiteIntermediateTowerProjection, pullback.map, pullback.lift_snd,
      pullback.lift_snd_assoc, Category.comp_id]
    exact (constantFieldTowerIso_hom_snd k L F X f).symm
def

finiteIntermediateTowerModelRecoveryIso

L103 ↗
EtaleFundamentalGroups.finiteIntermediateTowerModelRecoveryIso
Documentation

Recovery over the relative finite stage gives recovery over the same field viewed as an actual intermediate field of the original extension.

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) (E : IntermediateField F L)
variable (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of k))
local notation "φF" => Spec.map (CommRingCat.ofHom (algebraMap k F))
local notation "φE" => Spec.map (CommRingCat.ofHom (algebraMap k E))
local notation "φL" => Spec.map (CommRingCat.ofHom (algebraMap k L))
local notation "η" => Spec.map (CommRingCat.ofHom (algebraMap F E))
local notation "ψF" => Spec.map (CommRingCat.ofHom F.val.toRingHom)
local notation "ψE" => Spec.map (CommRingCat.ofHom (AlgHom.toRingHom (IntermediateField.val E)))
Lean source · full declaration
def finiteIntermediateTowerModelRecoveryIso
    (N : FiniteEtale (pullback η (pullback.fst φF f)))
    (Z : FiniteEtale (pullback φL f))
    (e : (FiniteEtale.pullback (finiteIntermediateTowerProjection k L F E X f)).obj N ≅
      (FiniteEtale.pullback (constantFieldTowerIso k L F X f).hom).obj Z) :
    (FiniteEtale.pullback (pullback.map φL f φE f ψE (𝟙 X) (𝟙 _)
      (by rw [Category.comp_id, ← Spec.map_comp]; rfl)
      (by rw [Category.comp_id, Category.id_comp]))).obj
        ((FiniteEtale.pullback (finiteIntermediateTowerIso k L F E X f).inv).obj N) ≅ Z := by
  let eX := constantFieldTowerIso k L F X f
  let eY := finiteIntermediateTowerIso k L F E X f
  let cE := finiteIntermediateTowerProjection k L F E X f
  let cH : pullback φL f ⟶ pullback φE f :=
    pullback.map φL f φE f ψE (𝟙 X) (𝟙 _)
      (by rw [Category.comp_id, ← Spec.map_comp]; rfl)
      (by rw [Category.comp_id, Category.id_comp])
  have hn₀ : cE ≫ eY.hom = eX.hom ≫ cH :=
    finiteIntermediateTowerIso_projection k L F E X f
  have hn : cH ≫ eY.inv = eX.inv ≫ cE := by
    apply (cancel_epi eX.hom).mp
    rw [← Category.assoc, ← hn₀, Category.assoc, Iso.hom_inv_id,
      Category.comp_id, Iso.hom_inv_id_assoc]
  let eId : (FiniteEtale.pullback (𝟙 (pullback φL f))).obj Z ≅ Z :=
    (FiniteEtale.forget (pullback φL f)).preimageIso
      (Over.pullbackId.app ((FiniteEtale.forget (pullback φL f)).obj Z))
  exact
    FiniteEtale.finiteEtalePullbackCompObjIso cH eY.inv (eX.inv ≫ cE) hn N ≪≫
    (FiniteEtale.finiteEtalePullbackCompObjIso eX.inv cE (eX.inv ≫ cE) rfl N).symm ≪≫
    (FiniteEtale.pullback eX.inv).mapIso e ≪≫
    FiniteEtale.finiteEtalePullbackCompObjIso eX.inv eX.hom (𝟙 _) eX.inv_hom_id Z ≪≫ eId

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