Module

FiniteEtaleGaloisCoverIdealImage.lean

Nyll.EtaleFundamentalGroups.Kummer.Normalization.FiniteEtaleGaloisCoverIdealImage

2 declarations indexed from sourceView source ↗

Module documentation

Ideal-inertia images in pointed finite-etale Galois quotients

For the surjective quotient represented by a pointed finite-etale Galois cover, the inverse image of normalization-prime ideal inertia maps back onto that exact subgroup. Combining this quotient statement with the function-field comparison identifies its order with ordinary ideal inertia.

This is a finite-quotient statement. It does not construct the separate strict-henselian local-to-global fundamental-group morphism.

Imports1

Nyll.EtaleFundamentalGroups.Kummer.Normalization.FiniteEtaleGaloisCoverIdealGroups

Imported by5

theorem

finiteEtaleGaloisCoverIdealInertia_map_comap

L34 ↗

EtaleFundamentalGroups.Kummer.finiteEtaleGaloisCoverIdealInertia_map_comap

Documentation

Normalization-prime ideal inertia is exactly the image of its inverse image under the pointed finite-etale Galois-cover quotient.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped Pointwise
namespace EtaleFundamentalGroups.Kummer
universe u uA uB

Lean source · full declaration

theorem finiteEtaleGaloisCoverIdealInertia_map_comap
    {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
    let K := X.functionField
    let L := Y.left.functionField
    letI : Algebra K L := finiteEtaleFunctionFieldAlgebra Y
    ∀ (A : Type uA) (B : Type uB)
      [CommRing A] [CommRing B]
      [Algebra A K] [IsFractionRing A K]
      [Algebra B L] [IsFractionRing B L]
      [Algebra A B] [Algebra A L]
      [IsScalarTower A K L] [IsScalarTower A B L]
      [IsIntegrallyClosed A] [IsIntegralClosure B A L]
      (P : Ideal B),
      letI : FiniteDimensional K L :=
        finiteDimensional_functionField_of_finiteEtale_isConnected Y
      letI : MulSemiringAction Gal(L/K) B :=
        IsIntegralClosure.MulSemiringAction A K L B
      letI : MulSemiringAction (Aut Y)ᵐᵒᵖ B :=
        finiteEtaleGaloisCoverNormalizationAction Y hY A B
      Subgroup.map
          (finiteEtaleGaloisCoverQuotientMonoidHom xi Y hY y)
          (Subgroup.comap
            (finiteEtaleGaloisCoverQuotientMonoidHom xi Y hY y)
            (P.toAddSubgroup.inertia (Aut Y)ᵐᵒᵖ)) =
        P.toAddSubgroup.inertia (Aut Y)ᵐᵒᵖ := by
  let : IsGalois Y := hY
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let K := X.functionField
  let L := Y.left.functionField
  let : Algebra K L := finiteEtaleFunctionFieldAlgebra Y
  dsimp only
  intro A B _ _ _ _ _ _ _ _ _ _ _ _ P
  let : FiniteDimensional K L :=
    finiteDimensional_functionField_of_finiteEtale_isConnected Y
  let : MulSemiringAction Gal(L/K) B :=
    IsIntegralClosure.MulSemiringAction A K L B
  let : MulSemiringAction (Aut Y)ᵐᵒᵖ B :=
    finiteEtaleGaloisCoverNormalizationAction Y hY A B
  exact finiteEtaleGaloisCoverQuotientMonoidHom_map_comap xi Y hY y
    (P.toAddSubgroup.inertia (Aut Y)ᵐᵒᵖ)

theorem

natCard_finiteEtaleGaloisCoverIdealInertia_image_eq

L86 ↗

EtaleFundamentalGroups.Kummer.natCard_finiteEtaleGaloisCoverIdealInertia_image_eq