Module

FiberQuotient.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.FiberQuotient

9 declarations indexed from sourceView source ↗

Module documentation

Finite quotients represented by finite-etale Galois covers

A chosen point of the geometric fiber of a finite-etale Galois cover gives the corresponding surjective finite quotient of the etale fundamental group. For a normal integral locally Noetherian base, this quotient is also identified with the Galois group of the induced function-field extension.

Imports2

Imported by8

def

finiteEtaleGaloisCoverQuotientMonoidHom

L30 ↗

EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom

Documentation

The finite quotient of the etale fundamental group represented by a pointed finite-etale Galois cover.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

def finiteEtaleGaloisCoverQuotientMonoidHom
    {X : Scheme.{u}} [ConnectedSpace X]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ X)
    (Y : FiniteEtale X) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber xi).obj Y) :
    letI : IsGalois Y := hY
    π₁ᵉᵗ(xi) →* (Aut Y)ᵐᵒᵖ := by
  letI : IsGalois Y := hY
  exact galoisObjectQuotientMonoidHom
    (FiniteEtale.fiber xi) π₁ᵉᵗ(xi) Y y

theorem

finiteEtaleGaloisCoverQuotientMonoidHom_evaluation

L43 ↗

EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom_evaluation

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem finiteEtaleGaloisCoverQuotientMonoidHom_evaluation
    {X : Scheme.{u}} [ConnectedSpace X]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ X)
    (Y : FiniteEtale X) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber xi).obj Y) (g : π₁ᵉᵗ(xi)) :
    letI : IsGalois Y := hY
    (FiniteEtale.fiber xi).map
        ((finiteEtaleGaloisCoverQuotientMonoidHom xi Y hY y g).unop.hom) y =
      g • y := by
  let : IsGalois Y := hY
  exact galoisObjectQuotientMonoidHom_evaluation
    (FiniteEtale.fiber xi) π₁ᵉᵗ(xi) Y y g

theorem

finiteEtaleGaloisCoverQuotientMonoidHom_ker

L59 ↗

EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom_ker

Documentation

The pointed-cover quotient has kernel the stabilizer of the chosen geometric fiber point.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem finiteEtaleGaloisCoverQuotientMonoidHom_ker
    {X : Scheme.{u}} [ConnectedSpace X]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ X)
    (Y : FiniteEtale X) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber xi).obj Y) :
    letI : IsGalois Y := hY
    (finiteEtaleGaloisCoverQuotientMonoidHom xi Y hY y).ker =
      MulAction.stabilizer π₁ᵉᵗ(xi) y := by
  let : IsGalois Y := hY
  exact galoisObjectQuotientMonoidHom_ker
    (FiniteEtale.fiber xi) π₁ᵉᵗ(xi) Y y

theorem

finiteEtaleGaloisCoverQuotientMonoidHom_surjective

L74 ↗

EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom_surjective

Documentation

A pointed finite-etale Galois cover gives a surjective finite quotient of the etale fundamental group.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem finiteEtaleGaloisCoverQuotientMonoidHom_surjective
    {X : Scheme.{u}} [ConnectedSpace X]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ X)
    (Y : FiniteEtale X) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber xi).obj Y) :
    letI : IsGalois Y := hY
    Function.Surjective
      (finiteEtaleGaloisCoverQuotientMonoidHom xi Y hY y) := by
  let : IsGalois Y := hY
  exact galoisObjectQuotientMonoidHom_surjective
    (FiniteEtale.fiber xi) π₁ᵉᵗ(xi) Y y

theorem

finiteEtaleGaloisCoverQuotientMonoidHom_map_comap

L89 ↗

EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom_map_comap

Documentation

Every subgroup of the deck group is the image of its inverse image in the pointed-cover fundamental-group quotient.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem finiteEtaleGaloisCoverQuotientMonoidHom_map_comap
    {X : Scheme.{u}} [ConnectedSpace X]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ X)
    (Y : FiniteEtale X) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber xi).obj Y)
    (H : Subgroup (Aut Y)ᵐᵒᵖ) :
    letI : IsGalois Y := hY
    Subgroup.map (finiteEtaleGaloisCoverQuotientMonoidHom xi Y hY y)
        (Subgroup.comap
          (finiteEtaleGaloisCoverQuotientMonoidHom xi Y hY y) H) = H := by
  let : IsGalois Y := hY
  exact Subgroup.map_comap_eq_self_of_surjective
    (finiteEtaleGaloisCoverQuotientMonoidHom_surjective xi Y hY y) H

def

finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom

L106 ↗

EtaleFundamentalGroups.finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom

Documentation

The function-field realization of the finite quotient represented by a pointed finite-etale Galois cover.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

def finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ X)
    (Y : FiniteEtale X) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber xi).obj Y) :
    letI : IsGalois Y := hY
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    letI : Algebra X.functionField Y.left.functionField :=
      finiteEtaleFunctionFieldAlgebra Y
    π₁ᵉᵗ(xi) →*
      (Y.left.functionField ≃ₐ[X.functionField] Y.left.functionField) := by
  letI : IsGalois Y := hY
  letI : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  letI : Algebra X.functionField Y.left.functionField :=
    finiteEtaleFunctionFieldAlgebra Y
  exact (finiteEtaleAutOpFunctionFieldMulEquiv Y hY).toMonoidHom.comp
    (finiteEtaleGaloisCoverQuotientMonoidHom xi Y hY y)

theorem

finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom_apply

L129 ↗

EtaleFundamentalGroups.finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom_apply

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom_apply
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ X)
    (Y : FiniteEtale X) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber xi).obj Y) (g : π₁ᵉᵗ(xi)) :
    letI : IsGalois Y := hY
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    letI : Algebra X.functionField Y.left.functionField :=
      finiteEtaleFunctionFieldAlgebra Y
    finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom xi Y hY y g =
      finiteEtaleAutFunctionFieldAlgEquiv Y
        (finiteEtaleGaloisCoverQuotientMonoidHom xi Y hY y g).unop := by
  let : IsGalois Y := hY
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let : Algebra X.functionField Y.left.functionField :=
    finiteEtaleFunctionFieldAlgebra Y
  exact finiteEtaleAutOpFunctionFieldMulEquiv_apply Y hY _

theorem

finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom_surjective

L152 ↗

EtaleFundamentalGroups.finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom_surjective

Documentation

The function-field realization remains a surjective finite quotient.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom_surjective
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ X)
    (Y : FiniteEtale X) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber xi).obj Y) :
    letI : IsGalois Y := hY
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    letI : Algebra X.functionField Y.left.functionField :=
      finiteEtaleFunctionFieldAlgebra Y
    Function.Surjective
      (finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom xi Y hY y) := by
  let : IsGalois Y := hY
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let : Algebra X.functionField Y.left.functionField :=
    finiteEtaleFunctionFieldAlgebra Y
  exact (finiteEtaleAutOpFunctionFieldMulEquiv Y hY).surjective.comp
    (finiteEtaleGaloisCoverQuotientMonoidHom_surjective xi Y hY y)

theorem

finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom_ker

L176 ↗

EtaleFundamentalGroups.finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom_ker

Documentation

Passing from the categorical cover quotient to the function-field Galois group does not change its kernel.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom_ker
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ X)
    (Y : FiniteEtale X) (hY : IsGalois Y)
    (y : (FiniteEtale.fiber xi).obj Y) :
    letI : IsGalois Y := hY
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    letI : Algebra X.functionField Y.left.functionField :=
      finiteEtaleFunctionFieldAlgebra Y
    (finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom
      xi Y hY y).ker = MulAction.stabilizer π₁ᵉᵗ(xi) y := by
  let : IsGalois Y := hY
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let : Algebra X.functionField Y.left.functionField :=
    finiteEtaleFunctionFieldAlgebra Y
  rw [finiteEtaleGaloisCoverFunctionFieldQuotientMonoidHom,
    MonoidHom.ker_comp_of_injective,
    finiteEtaleGaloisCoverQuotientMonoidHom_ker]
  exact (finiteEtaleAutOpFunctionFieldMulEquiv Y hY).injective

Module documentation

Finite quotients represented by finite-etale Galois covers

Declarations