Module

GenericPointFixedSubfield.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.GenericPointFixedSubfield

6 declarations indexed from sourceView source ↗

Module documentation

Finite subfields fixed by the generic Galois kernel

A finite subfield of the separable closure is fixed by the generic kernel exactly when its spectrum occurs as the generic fiber of a finite étale cover. The comparison uses the literal spectrum and postcomposition of field embeddings.

Imports5

Nyll.EtaleFundamentalGroups.GeometricFiber.GenericPointEssentialImage
Nyll.EtaleFundamentalGroups.Inertia.NormalSubgroupEmbeddings
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.RingTheory.Etale.Field
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic

Imported by3

def

finiteSubfieldCover

L30 ↗

AlgebraicGeometry.FiniteEtale.finiteSubfieldCover

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

def finiteSubfieldCover (K : Type u) [Field K]
    (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K L] :
    FiniteEtale (Spec (.of K))

def

subfieldPointEquiv

L42 ↗

AlgebraicGeometry.FiniteEtale.subfieldPointEquiv

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

def subfieldPointEquiv (K : Type u) [Field K]
    (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K L] :
    (Over.mk (ξ K (SeparableClosure K)) ⟶ (finiteSubfieldCover K L).toComma) ≃
      (L →ₐ[K] SeparableClosure K)

theorem

subfieldPointEquiv_smul

L55 ↗

AlgebraicGeometry.FiniteEtale.subfieldPointEquiv_smul

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem subfieldPointEquiv_smul (K : Type u) [Field K]
    (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K L]
    (g : SeparableClosure K ≃ₐ[K] SeparableClosure K)
    (x : Over.mk (Spec.map (CommRingCat.ofHom (algebraMap K (SeparableClosure K)))) ⟶
      (finiteSubfieldCover K L).toComma) :
    subfieldPointEquiv K L (g • x) = g.toAlgHom.comp (subfieldPointEquiv K L x)

theorem

subfieldAction_ker_iff

L69 ↗

AlgebraicGeometry.FiniteEtale.subfieldAction_ker_iff

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem subfieldAction_ker_iff (K : Type u) [Field K]
    (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K L]
    (g : SeparableClosure K ≃ₐ[K] SeparableClosure K) :
    g ∈ (Action.ρAut
      (((equivContAction K (SeparableClosure K)).functor.obj
        (finiteSubfieldCover K L)).obj)).ker ↔
      ∀ φ : L →ₐ[K] SeparableClosure K, g.toAlgHom.comp φ = φ

theorem

subfieldCover_essImage_iff

L102 ↗

AlgebraicGeometry.FiniteEtale.subfieldCover_essImage_iff

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem subfieldCover_essImage_iff (X : Scheme.{u})
    [IsIntegral X] [IsNormalIntegral X]
    (L : IntermediateField X.functionField (SeparableClosure X.functionField))
    [FiniteDimensional X.functionField L] :
    (pullback (X.fromSpecStalk (genericPoint X))).essImage
      (finiteSubfieldCover X.functionField L) ↔
        (genericAbsoluteGaloisHom X).toMonoidHom.ker ≤ L.fixingSubgroup

theorem

genericKernel_le_fixingSubgroup_iff_exists_finiteEtale_genericFiber

L120 ↗

AlgebraicGeometry.FiniteEtale.genericKernel_le_fixingSubgroup_iff_exists_finiteEtale_genericFiber

Documentation

A finite intermediate field is fixed by the generic Galois kernel exactly when its literal spectrum is the generic fiber of a finite étale cover. The cover and its generic-fiber isomorphism are actually constructed.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem genericKernel_le_fixingSubgroup_iff_exists_finiteEtale_genericFiber
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (L : IntermediateField X.functionField (SeparableClosure X.functionField))
    [FiniteDimensional X.functionField L] :
    (genericAbsoluteGaloisHom X).toMonoidHom.ker ≤ L.fixingSubgroup ↔
      ∃ (Y : Scheme.{u}) (f : Y ⟶ X), IsFinite f ∧ Etale f ∧
        ∃ e : Limits.pullback f (X.fromSpecStalk (genericPoint X)) ≅ Spec (.of L),
          e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap X.functionField L)) =
            Limits.pullback.snd f (X.fromSpecStalk (genericPoint X))

Module documentation

Finite subfields fixed by the generic Galois kernel

Declarations

finiteSubfieldCover

subfieldPointEquiv

subfieldPointEquiv_smul

subfieldAction_ker_iff

subfieldCover_essImage_iff

genericKernel_le_fixingSubgroup_iff_exists_finiteEtale_genericFiber