Module

GenericPointSeparableComparison.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.GenericPointSeparableComparison

3 declarations indexed from sourceView source ↗

Module documentation

The actual generic Galois map at the separable geometric point

The canonical extension from the separable closure to the algebraic closure compares the two actual generic fiber functors. Under this comparison, the canonical generic absolute Galois map is exactly the scheme-induced map of the original field monodromy action.

Imports5

Imported by3

theorem

conjugate_induced_aut

L31 ↗

AlgebraicGeometry.FiniteEtale.conjugate_induced_aut

Source context 4 commands

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

noncomputable section
universe u u₀ v₀ u₁ v₁ w
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem conjugate_induced_aut
    {C : Type u₀} [Category.{v₀} C] {D : Type u₁} [Category.{v₁} D]
    (H : C ⥤ D) {F G : C ⥤ FintypeCat.{w}} {F' G' : D ⥤ FintypeCat.{w}}
    (r : H ⋙ F' ≅ F) (t : H ⋙ G' ≅ G) (e : F' ≅ G') (a : Aut F') :
    (r.symm ≪≫ Functor.isoWhiskerLeft H e ≪≫ t).conjAut
      (autHomOfCompIso H r a) = autHomOfCompIso H t (e.conjAut a)

def

genericSeparableFiberIso

L53 ↗

AlgebraicGeometry.FiniteEtale.genericSeparableFiberIso

Documentation

The generic fiber comparison is induced by the actual inclusion of the separable closure in the algebraic closure and by the actual pullback fibers.

Source context 4 commands

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

noncomputable section
universe u u₀ v₀ u₁ v₁ w
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

def genericSeparableFiberIso (X : Scheme.{u}) [IsIntegral X] :
    fiber (X.genericExtensionMorphism (SeparableClosure X.functionField)) ≅
      fiber (X.genericExtensionMorphism (AlgebraicClosure X.functionField))

theorem

genericAbsoluteGaloisHom_eq_separable

L66 ↗

AlgebraicGeometry.FiniteEtale.genericAbsoluteGaloisHom_eq_separable

Documentation

The canonical generic absolute Galois map is the actual scheme-induced separable field action transported by the canonical fiber comparison.

Source context 4 commands

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

noncomputable section
universe u u₀ v₀ u₁ v₁ w
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale

Lean source · full declaration

theorem genericAbsoluteGaloisHom_eq_separable
    (X : Scheme.{u}) [IsIntegral X]
    (σ : Gal(SeparableClosure X.functionField/X.functionField)) :
    let : IsSepClosure X.functionField (SeparableClosure X.functionField) :=
      separableClosure.isSepClosure X.functionField (AlgebraicClosure X.functionField)
    genericAbsoluteGaloisHom X σ =
      (genericSeparableFiberIso X).conjAut
        (fundamentalGroupHom (X.fromSpecStalk (genericPoint X))
          (ξ X.functionField (SeparableClosure X.functionField))
          (toAut (fib X.functionField (SeparableClosure X.functionField))
            Gal(SeparableClosure X.functionField/X.functionField) σ)) := by
  intro hclosure
  let j := X.fromSpecStalk (genericPoint X)
  let e := fieldFiberExtensionIso X.functionField (SeparableClosure X.functionField)
    (AlgebraicClosure X.functionField)
  let a := toAut (fib X.functionField (SeparableClosure X.functionField))
    Gal(SeparableClosure X.functionField/X.functionField) σ
  have hfield : absoluteGaloisEquivFundamentalGroup X.functionField σ = e.conjAut a := rfl
  change fundamentalGroupHom j (ξ X.functionField (AlgebraicClosure X.functionField))
      (absoluteGaloisEquivFundamentalGroup X.functionField σ) = _
  rw [hfield]
  exact (conjugate_induced_aut (pullback j)
    (pullbackFiberIso j (ξ X.functionField (SeparableClosure X.functionField)))
    (pullbackFiberIso j (ξ X.functionField (AlgebraicClosure X.functionField))) e a).symm

Module documentation

The actual generic Galois map at the separable geometric point

Declarations

conjugate_induced_aut

genericSeparableFiberIso

genericAbsoluteGaloisHom_eq_separable