Module

UnramifiedSubfield.lean

Nyll.EtaleFundamentalGroups.Normalization.UnramifiedSubfield

5 declarations indexed from sourceView source ↗

Module documentation

Unramified subfields and the generic Galois kernel

The generic-fibre comparison identifies the finite subfields coming from unramified normalization with the fields fixed by the generic Galois kernel.

Imports5

Imported by2

instance

fieldSpecQuasiCompact

L29 ↗

EtaleFundamentalGroups.fieldSpecQuasiCompact

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

theorem

genericKernel_le_fixingSubgroup_of_etale_normalization

L36 ↗

EtaleFundamentalGroups.genericKernel_le_fixingSubgroup_of_etale_normalization

Documentation

The generic Galois kernel fixes a finite subfield whose normalization is étale. Integrality of normalization supplies the finite cover.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

theorem genericKernel_le_fixingSubgroup_of_etale_normalization
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (L : IntermediateField X.functionField (SeparableClosure X.functionField))
    [FiniteDimensional X.functionField L]
    (h : Etale (X.genericExtensionMorphism L).fromNormalization) :
    (genericAbsoluteGaloisHom X).toMonoidHom.ker ≤ L.fixingSubgroup

theorem

etale_normalization_iff_genericKernel_le_fixingSubgroup

L52 ↗

EtaleFundamentalGroups.etale_normalization_iff_genericKernel_le_fixingSubgroup

Documentation

A finite subfield has étale normalization exactly when it is fixed by the kernel of the generic absolute Galois map.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

theorem etale_normalization_iff_genericKernel_le_fixingSubgroup
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (L : IntermediateField X.functionField (SeparableClosure X.functionField))
    [FiniteDimensional X.functionField L] :
    Etale (X.genericExtensionMorphism L).fromNormalization ↔
      (genericAbsoluteGaloisHom X).toMonoidHom.ker ≤ L.fixingSubgroup

theorem

mem_genericKernelFixedField_iff_exists_unramified_finite_subfield

L77 ↗

EtaleFundamentalGroups.mem_genericKernelFixedField_iff_exists_unramified_finite_subfield

Documentation

The field fixed by the generic kernel is the actual union of the finite subextensions unramified in X.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

theorem mem_genericKernelFixedField_iff_exists_unramified_finite_subfield
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (x : SeparableClosure X.functionField) :
    x ∈ genericKernelFixedField X ↔
      ∃ L : IntermediateField X.functionField (SeparableClosure X.functionField),
        FiniteDimensional X.functionField L ∧
        (FormallyUnramified (X.genericExtensionMorphism L).fromNormalization ∧
          LocallyOfFiniteType (X.genericExtensionMorphism L).fromNormalization) ∧ x ∈ L

theorem

genericKernelFixedField_eq_iSup_unramified

L106 ↗

EtaleFundamentalGroups.genericKernelFixedField_eq_iSup_unramified

Documentation

The maximal unramified extension, written as a supremum of the original finite unramified subextensions, is the generic kernel's fixed field.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

theorem genericKernelFixedField_eq_iSup_unramified
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X] :
    genericKernelFixedField X =
      ⨆ (L : IntermediateField X.functionField (SeparableClosure X.functionField))
        (_ : FiniteDimensional X.functionField L)
        (_ : FormallyUnramified (X.genericExtensionMorphism L).fromNormalization ∧
          LocallyOfFiniteType (X.genericExtensionMorphism L).fromNormalization), L

Module documentation

Unramified subfields and the generic Galois kernel

Declarations

fieldSpecQuasiCompact

genericKernel_le_fixingSubgroup_of_etale_normalization

etale_normalization_iff_genericKernel_le_fixingSubgroup

mem_genericKernelFixedField_iff_exists_unramified_finite_subfield

genericKernelFixedField_eq_iSup_unramified