Module

DivisorialStrictHenselian.lean

Nyll.EtaleFundamentalGroups.Inertia.DivisorialStrictHenselian

4 declarations indexed from sourceView source ↗

Module documentation

Fundamental-group images from geometric local models

For a morphism j : T ⟶ U, functoriality of the geometric fiber gives the canonical homomorphism from the fundamental group of T to that of U. This file records its image and its finite monodromy on a pointed finite-etale Galois cover of U.

The intended divisorial application takes T to be the generic point of a strictly Henselian discrete valuation ring. The definitions below do not postulate a strict henselization or an inertia comparison: they apply to the actual local model once it has been constructed.

Imports2

Imported by9

def

fundamentalGroupImageOfMorphism

L36 ↗

EtaleFundamentalGroups.Inertia.fundamentalGroupImageOfMorphism

Documentation

The subgroup of the target fundamental group contributed by a geometric source. For the generic point of a strict-Henselian DVR this is the corresponding divisorial inertia subgroup.

Source context 5 commands

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

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

Lean source · statement

def fundamentalGroupImageOfMorphism
    {T U : Scheme.{u}} {Omega : Type u}
    [Field Omega] [IsSepClosed Omega]
    (j : T ⟶ U) (xi : Spec (.of Omega) ⟶ T) :
    Subgroup π₁ᵉᵗ(xi ≫ j)

def

finiteEtaleGaloisCoverQuotientOfMorphism

L45 ↗

EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotientOfMorphism

Documentation

The finite monodromy of a pointed Galois cover after restriction to a geometric source.

Source context 5 commands

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

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

Lean source · full declaration

def finiteEtaleGaloisCoverQuotientOfMorphism
    {T U : Scheme.{u}} [ConnectedSpace U]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (j : T ⟶ U) (xi : Spec (.of Omega) ⟶ T)
    (Y : AlgebraicGeometry.FiniteEtale U) (hY : IsGalois Y)
    (y : (AlgebraicGeometry.FiniteEtale.fiber (xi ≫ j)).obj Y) :
    letI : IsGalois Y := hY
    π₁ᵉᵗ(xi) →* (Aut Y)ᵐᵒᵖ := by
  letI : IsGalois Y := hY
  exact
    (finiteEtaleGaloisCoverQuotientMonoidHom (xi ≫ j) Y hY y).comp
      (AlgebraicGeometry.FiniteEtale.fundamentalGroupHom j xi).toMonoidHom

theorem

finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage

L60 ↗

EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage

Documentation

Restricting a pointed finite-cover quotient to the geometric-source image is exactly the range of the local monodromy homomorphism.

Source context 5 commands

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

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

Lean source · full declaration

theorem finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage
    {T U : Scheme.{u}} [ConnectedSpace U]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (j : T ⟶ U) (xi : Spec (.of Omega) ⟶ T)
    (Y : AlgebraicGeometry.FiniteEtale U) (hY : IsGalois Y)
    (y : (AlgebraicGeometry.FiniteEtale.fiber (xi ≫ j)).obj Y) :
    letI : IsGalois Y := hY
    Subgroup.map
        (finiteEtaleGaloisCoverQuotientMonoidHom (xi ≫ j) Y hY y)
        (fundamentalGroupImageOfMorphism j xi) =
      (finiteEtaleGaloisCoverQuotientOfMorphism j xi Y hY y).range := by
  let : IsGalois Y := hY
  exact MonoidHom.map_range
    (finiteEtaleGaloisCoverQuotientMonoidHom (xi ≫ j) Y hY y)
    (AlgebraicGeometry.FiniteEtale.fundamentalGroupHom j xi).toMonoidHom

theorem

finiteEtaleGaloisCoverQuotientOfMorphism_ker

L78 ↗

EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotientOfMorphism_ker

Documentation

The kernel of local monodromy on a pointed Galois cover is the stabilizer of the point transported to the pulled-back 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.Inertia
universe u

Lean source · full declaration

theorem finiteEtaleGaloisCoverQuotientOfMorphism_ker
    {T U : Scheme.{u}} [ConnectedSpace U]
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (j : T ⟶ U) (xi : Spec (.of Omega) ⟶ T)
    (Y : AlgebraicGeometry.FiniteEtale U) (hY : IsGalois Y)
    (y : (AlgebraicGeometry.FiniteEtale.fiber (xi ≫ j)).obj Y) :
    letI : IsGalois Y := hY
    (finiteEtaleGaloisCoverQuotientOfMorphism j xi Y hY y).ker =
      MulAction.stabilizer π₁ᵉᵗ(xi)
        (transportedPointOfCompIso
          (AlgebraicGeometry.FiniteEtale.pullback j)
          (AlgebraicGeometry.FiniteEtale.pullbackFiberIso j xi) Y y) := by
  let : IsGalois Y := hY
  let h :=
    (AlgebraicGeometry.FiniteEtale.fundamentalGroupHom j xi).toMonoidHom
  let q := finiteEtaleGaloisCoverQuotientMonoidHom (xi ≫ j) Y hY y
  calc
    (finiteEtaleGaloisCoverQuotientOfMorphism j xi Y hY y).ker =
        Subgroup.comap h q.ker := rfl
    _ = Subgroup.comap h (MulAction.stabilizer π₁ᵉᵗ(xi ≫ j) y) := by
      rw [finiteEtaleGaloisCoverQuotientMonoidHom_ker]
    _ = MulAction.stabilizer π₁ᵉᵗ(xi)
        (transportedPointOfCompIso
          (AlgebraicGeometry.FiniteEtale.pullback j)
          (AlgebraicGeometry.FiniteEtale.pullbackFiberIso j xi) Y y) := by
      exact (stabilizer_transportedPointOfCompIso
        (AlgebraicGeometry.FiniteEtale.pullback j)
        (AlgebraicGeometry.FiniteEtale.pullbackFiberIso j xi) Y y).symm

Module documentation

Fundamental-group images from geometric local models

Declarations

fundamentalGroupImageOfMorphism

finiteEtaleGaloisCoverQuotientOfMorphism

finiteEtaleGaloisCoverQuotient_map_fundamentalGroupImage

finiteEtaleGaloisCoverQuotientOfMorphism_ker