NYLL
Module

FieldFunctoriality.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.FieldFunctoriality
12 declarations indexed from sourceView source ↗

Module documentation

Functoriality over a tower of fields

For a tower of fields k → K → Ω, base change from k to K is compatible with the two geometric fiber functors valued in Ω. The comparison below is written directly on geometric points; this makes its compatibility with scalar restriction on absolute Galois groups explicit.

Imports2
Imported by8

Declarations

lemma

fieldGeometricPoint_comp

L38 ↗
AlgebraicGeometry.FiniteEtale.fieldGeometricPoint_comp
Documentation

The geometric point of Spec k obtained through Spec K is the geometric point defined by the composite algebra structure.

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
Lean source · statement
lemma fieldGeometricPoint_comp :
    ξ K Ω ≫ ξ k K = ξ k Ω
def

fieldPullbackOverEquiv

L47 ↗
AlgebraicGeometry.FiniteEtale.fieldPullbackOverEquiv
Documentation

On geometric points, the fiber of a base changed finite étale cover is the original geometric fiber.

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
Lean source · full declaration
def fieldPullbackOverEquiv
    (X : FiniteEtale (Spec (.of k))) :
    (Over.mk (ξ K Ω) ⟶ ((pullback (ξ k K)).obj X).toComma) ≃
      (Over.mk (ξ k Ω) ⟶ X.toComma) where
  toFun z :=
    Over.homMk (z.left ≫ Limits.pullback.fst X.hom (ξ k K)) (by
      change (z.left ≫ Limits.pullback.fst X.hom (ξ k K)) ≫ X.hom = ξ k Ω
      rw [← fieldGeometricPoint_comp k K Ω]
      have hz : z.left ≫ Limits.pullback.snd X.hom (ξ k K) = ξ K Ω := by
        exact z.w
      have hcondition :
          Limits.pullback.fst X.hom (ξ k K) ≫ X.hom =
            Limits.pullback.snd X.hom (ξ k K) ≫ ξ k K :=
        Limits.pullback.condition
      erw [Category.assoc, hcondition, ← Category.assoc, hz])
  invFun x :=
    Over.homMk
      (Limits.pullback.lift x.left (ξ K Ω)
        (x.w.trans (fieldGeometricPoint_comp k K Ω).symm))
      (Limits.pullback.lift_snd _ _ _)
  left_inv z := by
    apply CategoryTheory.Over.OverMorphism.ext
    apply Limits.pullback.hom_ext
    · exact Limits.pullback.lift_fst _ _ _
    · have hz : z.left ≫ Limits.pullback.snd X.hom (ξ k K) = ξ K Ω := by
        exact z.w
      exact (Limits.pullback.lift_snd _ _ _).trans hz.symm
  right_inv x := by
    apply CategoryTheory.Over.OverMorphism.ext
    exact Limits.pullback.lift_fst _ _ _
lemma

fieldPullbackOverEquiv_naturality

L78 ↗
AlgebraicGeometry.FiniteEtale.fieldPullbackOverEquiv_naturality
Source context 9 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
Lean source · statement
lemma fieldPullbackOverEquiv_naturality
    {X Y : FiniteEtale (Spec (.of k))} (f : X ⟶ Y)
    (z : Over.mk (ξ K Ω) ⟶ ((pullback (ξ k K)).obj X).toComma) :
    fieldPullbackOverEquiv k K Ω Y
        (z ≫ ((pullback (ξ k K)).map f).hom) =
      fieldPullbackOverEquiv k K Ω X z ≫ f.hom
def

fieldFiberEquiv

L106 ↗
AlgebraicGeometry.FiniteEtale.fieldFiberEquiv
Documentation

The pointwise comparison between the geometric fiber after base change and the original geometric fiber.

Source context 11 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
section
variable [IsSepClosed Ω]
Lean source · statement
def fieldFiberEquiv
    (X : FiniteEtale (Spec (.of k))) :
    ((pullback (ξ k K) ⋙ fib K Ω).obj X) ≃ (fib k Ω).obj X
lemma

fiberObjEquivHom_fieldFiberEquiv

L114 ↗
AlgebraicGeometry.FiniteEtale.fiberObjEquivHom_fieldFiberEquiv
Source context 11 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
section
variable [IsSepClosed Ω]
Lean source · statement
lemma fiberObjEquivHom_fieldFiberEquiv
    (X : FiniteEtale (Spec (.of k)))
    (x : (pullback (ξ k K) ⋙ fib K Ω).obj X) :
    fiberObjEquivHom (ξ k Ω) X (fieldFiberEquiv k K Ω X x) =
      fieldPullbackOverEquiv k K Ω X
        (fiberObjEquivHom (ξ K Ω) ((pullback (ξ k K)).obj X) x)
def

fieldPullbackFiberIso

L128 ↗
AlgebraicGeometry.FiniteEtale.fieldPullbackFiberIso
Documentation

Pullback from Spec k to Spec K, followed by the geometric fiber in Ω, is naturally isomorphic to the geometric fiber over Spec k.

Source context 11 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
section
variable [IsSepClosed Ω]
Lean source · statement
def fieldPullbackFiberIso :
    pullback (ξ k K) ⋙ fib K Ω ≅ fib k Ω
lemma

fieldPullbackOverEquiv_smul

L146 ↗
AlgebraicGeometry.FiniteEtale.fieldPullbackOverEquiv_smul
Source context 12 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
section
variable [IsSepClosed Ω]
omit [IsSepClosed Ω] in
Lean source · statement
lemma fieldPullbackOverEquiv_smul
    (X : FiniteEtale (Spec (.of k))) (σ : Ω ≃ₐ[K] Ω)
    (z : Over.mk (ξ K Ω) ⟶ ((pullback (ξ k K)).obj X).toComma) :
    fieldPullbackOverEquiv k K Ω X (σ • z) =
      σ.restrictScalars k • fieldPullbackOverEquiv k K Ω X z
theorem

fieldFiberEquiv_smul

L160 ↗
AlgebraicGeometry.FiniteEtale.fieldFiberEquiv_smul
Documentation

The comparison of geometric fibers intertwines the absolute Galois action over K with scalar restriction to k.

Source context 11 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
section
variable [IsSepClosed Ω]
Lean source · statement
theorem fieldFiberEquiv_smul
    (X : FiniteEtale (Spec (.of k))) (σ : Ω ≃ₐ[K] Ω)
    (x : (fib K Ω).obj ((pullback (ξ k K)).obj X)) :
    fieldFiberEquiv k K Ω X (σ • x) =
      σ.restrictScalars k • fieldFiberEquiv k K Ω X x
def

absoluteGaloisToFiberAutMulEquiv

L178 ↗
AlgebraicGeometry.FiniteEtale.absoluteGaloisToFiberAutMulEquiv
Documentation

The absolute Galois group identified with the automorphism group of its geometric fiber functor, using an explicitly supplied separably-closed structure on the common overfield.

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
Lean source · statement
def absoluteGaloisToFiberAutMulEquiv
    (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
    [IsSepClosure F Ω] (hΩ : IsSepClosed Ω) :
    (Ω ≃ₐ[F] Ω) ≃* Aut (fib F Ω)
def

fieldFundamentalGroupHom

L189 ↗
AlgebraicGeometry.FiniteEtale.fieldFundamentalGroupHom
Documentation

The homomorphism of geometric-fiber automorphism groups induced by pullback from Spec k to Spec K, with the comparison on points fixed by fieldPullbackFiberIso.

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
Lean source · statement
def fieldFundamentalGroupHom
    (hΩ : IsSepClosed Ω) :
    Aut (fib K Ω) →ₜ* Aut (fib k Ω)
theorem

fieldFundamentalGroupHom_toAutMulEquiv_core

L200 ↗
AlgebraicGeometry.FiniteEtale.fieldFundamentalGroupHom_toAutMulEquiv_core
Source context 11 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
section
variable [IsSepClosure k Ω] [IsSepClosure K Ω]
Lean source · statement
theorem fieldFundamentalGroupHom_toAutMulEquiv_core
    [IsSepClosed Ω] (σ : Ω ≃ₐ[K] Ω) :
    CategoryTheory.PreGaloisCategory.autHomOfCompIso
        (pullback (ξ k K)) (fieldPullbackFiberIso k K Ω)
        (CategoryTheory.PreGaloisCategory.toAutMulEquiv
          (fib K Ω) (Ω ≃ₐ[K] Ω) σ) =
      CategoryTheory.PreGaloisCategory.toAutMulEquiv
        (fib k Ω) (Ω ≃ₐ[k] Ω) (σ.restrictScalars k)
theorem

fieldFundamentalGroupHom_toAutMulEquiv

L225 ↗
AlgebraicGeometry.FiniteEtale.fieldFundamentalGroupHom_toAutMulEquiv
Documentation

Under the canonical identifications of the two geometric-fiber fundamental groups with absolute Galois groups, the homomorphism induced by Spec K ⟶ Spec k is restriction of scalars.

Source context 11 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u)
variable [Field k] [Field K] [Field Ω]
variable [Algebra k K] [Algebra K Ω] [Algebra k Ω]
variable [IsScalarTower k K Ω]
section
variable [IsSepClosure k Ω] [IsSepClosure K Ω]
Lean source · statement
theorem fieldFundamentalGroupHom_toAutMulEquiv
    (σ : Ω ≃ₐ[K] Ω) :
    fieldFundamentalGroupHom k K Ω (IsSepClosure.sep_closed k)
        (absoluteGaloisToFiberAutMulEquiv K Ω
          (IsSepClosure.sep_closed k) σ) =
      absoluteGaloisToFiberAutMulEquiv k Ω
        (IsSepClosure.sep_closed k) (σ.restrictScalars k)

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