Module

GenericPointGaloisQuotient.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.GenericPointGaloisQuotient

10 declarations indexed from sourceView source ↗

Module documentation

The fixed field of the generic absolute Galois kernel

The kernel of the generic absolute Galois map is closed and normal. Its fixed field is Galois over the function field. For a normal integral scheme, the fundamental group is canonically the Galois group of this fixed field, and the generic absolute Galois map becomes restriction of automorphisms.

Imports6

Nyll.EtaleFundamentalGroups.GeometricFiber.GenericPointSurjective
Mathlib.FieldTheory.Galois.Infinite
Mathlib.FieldTheory.Galois.Profinite
Mathlib.FieldTheory.KrullTopology
Mathlib.GroupTheory.QuotientGroup.Basic
Mathlib.Topology.Separation.Hausdorff

Imported by2

def

genericKernelFixedField

L32 ↗

AlgebraicGeometry.FiniteEtale.genericKernelFixedField

Documentation

The subfield of the separable closure fixed by the generic Galois kernel.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

def genericKernelFixedField (X : Scheme.{u}) [IsIntegral X] :
    IntermediateField X.functionField (SeparableClosure X.functionField)

instance

genericKernelFixedField_isGalois

L37 ↗

AlgebraicGeometry.FiniteEtale.genericKernelFixedField_isGalois

Documentation

The generic kernel is normal, so its fixed field is Galois.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

instance genericKernelFixedField_isGalois (X : Scheme.{u}) [IsIntegral X] :
    IsGalois X.functionField (genericKernelFixedField X)

def

genericClosedKernel

L43 ↗

AlgebraicGeometry.FiniteEtale.genericClosedKernel

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · full declaration

def genericClosedKernel (X : Scheme.{u}) [IsIntegral X] :
    ClosedSubgroup (SeparableClosure X.functionField ≃ₐ[X.functionField]
      SeparableClosure X.functionField) where
  toSubgroup := (genericAbsoluteGaloisHom X).toMonoidHom.ker
  isClosed' := isClosed_eq (genericAbsoluteGaloisHom X).continuous continuous_const

instance

genericClosedKernel_normal

L49 ↗

AlgebraicGeometry.FiniteEtale.genericClosedKernel_normal

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

instance genericClosedKernel_normal (X : Scheme.{u}) [IsIntegral X] :
    (genericClosedKernel X).toSubgroup.Normal

theorem

genericKernelFixedField_fixingSubgroup

L56 ↗

AlgebraicGeometry.FiniteEtale.genericKernelFixedField_fixingSubgroup

Documentation

Infinite Galois correspondence recovers the actual generic kernel from its fixed field.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
private local instance genericClosedKernel_normal (X : Scheme.{u}) [IsIntegral X] :
    (genericClosedKernel X).toSubgroup.Normal := by
  change (genericAbsoluteGaloisHom X).toMonoidHom.ker.Normal
  infer_instance

Lean source · statement

theorem genericKernelFixedField_fixingSubgroup (X : Scheme.{u}) [IsIntegral X] :
    (genericKernelFixedField X).fixingSubgroup =
      (genericAbsoluteGaloisHom X).toMonoidHom.ker

def

genericFundamentalGroupMulEquiv

L61 ↗

AlgebraicGeometry.FiniteEtale.genericFundamentalGroupMulEquiv

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
private local instance genericClosedKernel_normal (X : Scheme.{u}) [IsIntegral X] :
    (genericClosedKernel X).toSubgroup.Normal := by
  change (genericAbsoluteGaloisHom X).toMonoidHom.ker.Normal
  infer_instance

Lean source · statement

def genericFundamentalGroupMulEquiv (X : Scheme.{u})
    [IsIntegral X] [IsNormalIntegral X] :
    π₁ᵉᵗ(X.genericExtensionMorphism (AlgebraicClosure X.functionField)) ≃*
      (genericKernelFixedField X ≃ₐ[X.functionField] genericKernelFixedField X)

theorem

genericFundamentalGroupMulEquiv_apply

L70 ↗

AlgebraicGeometry.FiniteEtale.genericFundamentalGroupMulEquiv_apply

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
private local instance genericClosedKernel_normal (X : Scheme.{u}) [IsIntegral X] :
    (genericClosedKernel X).toSubgroup.Normal := by
  change (genericAbsoluteGaloisHom X).toMonoidHom.ker.Normal
  infer_instance

Lean source · statement

theorem genericFundamentalGroupMulEquiv_apply (X : Scheme.{u})
    [IsIntegral X] [IsNormalIntegral X]
    (σ : SeparableClosure X.functionField ≃ₐ[X.functionField]
      SeparableClosure X.functionField) :
    genericFundamentalGroupMulEquiv X (genericAbsoluteGaloisHom X σ) =
      AlgEquiv.restrictNormalHom (genericKernelFixedField X) σ

theorem

genericFundamentalGroupMulEquiv_continuous

L84 ↗

AlgebraicGeometry.FiniteEtale.genericFundamentalGroupMulEquiv_continuous

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
private local instance genericClosedKernel_normal (X : Scheme.{u}) [IsIntegral X] :
    (genericClosedKernel X).toSubgroup.Normal := by
  change (genericAbsoluteGaloisHom X).toMonoidHom.ker.Normal
  infer_instance

Lean source · statement

theorem genericFundamentalGroupMulEquiv_continuous (X : Scheme.{u})
    [IsIntegral X] [IsNormalIntegral X] :
    Continuous (genericFundamentalGroupMulEquiv X)

def

genericFundamentalGroupEquivGalois

L99 ↗

AlgebraicGeometry.FiniteEtale.genericFundamentalGroupEquivGalois

Documentation

The fundamental group of a normal integral scheme is the Galois group of the field fixed by the generic absolute Galois kernel, with its Krull topology.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
private local instance genericClosedKernel_normal (X : Scheme.{u}) [IsIntegral X] :
    (genericClosedKernel X).toSubgroup.Normal := by
  change (genericAbsoluteGaloisHom X).toMonoidHom.ker.Normal
  infer_instance

Lean source · statement

def genericFundamentalGroupEquivGalois (X : Scheme.{u})
    [IsIntegral X] [IsNormalIntegral X] :
    π₁ᵉᵗ(X.genericExtensionMorphism (AlgebraicClosure X.functionField)) ≃ₜ*
      (genericKernelFixedField X ≃ₐ[X.functionField] genericKernelFixedField X)

theorem

genericFundamentalGroupEquivGalois_apply_genericAbsoluteGaloisHom

L113 ↗

AlgebraicGeometry.FiniteEtale.genericFundamentalGroupEquivGalois_apply_genericAbsoluteGaloisHom

Documentation

Under the fixed-field identification, the generic absolute Galois map is precisely restriction of field automorphisms.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
private local instance genericClosedKernel_normal (X : Scheme.{u}) [IsIntegral X] :
    (genericClosedKernel X).toSubgroup.Normal := by
  change (genericAbsoluteGaloisHom X).toMonoidHom.ker.Normal
  infer_instance

Lean source · statement

theorem genericFundamentalGroupEquivGalois_apply_genericAbsoluteGaloisHom
    (X : Scheme.{u}) [IsIntegral X] [IsNormalIntegral X]
    (σ : SeparableClosure X.functionField ≃ₐ[X.functionField]
      SeparableClosure X.functionField) :
    genericFundamentalGroupEquivGalois X (genericAbsoluteGaloisHom X σ) =
      AlgEquiv.restrictNormalHom (genericKernelFixedField X) σ

Module documentation

The fixed field of the generic absolute Galois kernel

Declarations