NYLL
Module

FiniteQuotientNormalizationInertiaCoprimality.lean

Nyll.EtaleFundamentalGroups.Kummer.Normalization.FiniteQuotientNormalizationInertiaCoprimality
10 declarations indexed from sourceView source ↗

Module documentation

Normalization inertia in explicit finite quotients

An explicit finite quotient of an etale fundamental group can be realized by a pointed connected finite-etale Galois cover. This file transports coprimality of normalization-prime inertia in the cover's function-field Galois group to the corresponding subgroup image in the prescribed quotient.

Imports2
Imported by2

Declarations

instance

finiteQuotientNormalizationInertia_isIntegral

L34 ↗
EtaleFundamentalGroups.Kummer.finiteQuotientNormalizationInertia_isIntegral
Source context 9 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Kummer
universe u uA uG
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
variable [IsLocallyNoetherian X]
variable (W : FiniteEtale X) [hW : IsGalois W]
Lean source · statement
instance finiteQuotientNormalizationInertia_isIntegral :
    IsIntegral W.left
instance

finiteQuotientNormalizationInertia_algebraKL

L41 ↗
EtaleFundamentalGroups.Kummer.finiteQuotientNormalizationInertia_algebraKL
Source context 12 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Kummer
universe u uA uG
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
variable [IsLocallyNoetherian X]
variable (W : FiniteEtale X) [hW : IsGalois W]
local instance finiteQuotientNormalizationInertia_isIntegral :
    IsIntegral W.left :=
  isIntegral_left_of_isConnected_finiteEtale W
local notation "K" => X.functionField
local notation "L" => W.left.functionField
Lean source · statement
instance finiteQuotientNormalizationInertia_algebraKL : Algebra K L
instance

finiteQuotientNormalizationInertia_algebraAL

L47 ↗
EtaleFundamentalGroups.Kummer.finiteQuotientNormalizationInertia_algebraAL
Source context 15 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Kummer
universe u uA uG
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
variable [IsLocallyNoetherian X]
variable (W : FiniteEtale X) [hW : IsGalois W]
local instance finiteQuotientNormalizationInertia_isIntegral :
    IsIntegral W.left :=
  isIntegral_left_of_isConnected_finiteEtale W
local notation "K" => X.functionField
local notation "L" => W.left.functionField
local instance finiteQuotientNormalizationInertia_algebraKL : Algebra K L :=
  finiteEtaleFunctionFieldAlgebra W
variable (A : Type uA) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
variable [Algebra A X.functionField] [IsFractionRing A X.functionField]
Lean source · statement
instance finiteQuotientNormalizationInertia_algebraAL : Algebra A L
instance

finiteQuotientNormalizationInertia_towerAKL

L50 ↗
EtaleFundamentalGroups.Kummer.finiteQuotientNormalizationInertia_towerAKL
Source context 16 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Kummer
universe u uA uG
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
variable [IsLocallyNoetherian X]
variable (W : FiniteEtale X) [hW : IsGalois W]
local instance finiteQuotientNormalizationInertia_isIntegral :
    IsIntegral W.left :=
  isIntegral_left_of_isConnected_finiteEtale W
local notation "K" => X.functionField
local notation "L" => W.left.functionField
local instance finiteQuotientNormalizationInertia_algebraKL : Algebra K L :=
  finiteEtaleFunctionFieldAlgebra W
variable (A : Type uA) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
variable [Algebra A X.functionField] [IsFractionRing A X.functionField]
local instance finiteQuotientNormalizationInertia_algebraAL : Algebra A L :=
  ((algebraMap K L).comp (algebraMap A K)).toAlgebra
Lean source · statement
instance finiteQuotientNormalizationInertia_towerAKL :
    IsScalarTower A K L
instance

finiteQuotientNormalizationInertia_finiteDimensional

L54 ↗
EtaleFundamentalGroups.Kummer.finiteQuotientNormalizationInertia_finiteDimensional
Source context 17 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Kummer
universe u uA uG
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
variable [IsLocallyNoetherian X]
variable (W : FiniteEtale X) [hW : IsGalois W]
local instance finiteQuotientNormalizationInertia_isIntegral :
    IsIntegral W.left :=
  isIntegral_left_of_isConnected_finiteEtale W
local notation "K" => X.functionField
local notation "L" => W.left.functionField
local instance finiteQuotientNormalizationInertia_algebraKL : Algebra K L :=
  finiteEtaleFunctionFieldAlgebra W
variable (A : Type uA) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
variable [Algebra A X.functionField] [IsFractionRing A X.functionField]
local instance finiteQuotientNormalizationInertia_algebraAL : Algebra A L :=
  ((algebraMap K L).comp (algebraMap A K)).toAlgebra
local instance finiteQuotientNormalizationInertia_towerAKL :
    IsScalarTower A K L :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
instance finiteQuotientNormalizationInertia_finiteDimensional :
    FiniteDimensional K L
instance

finiteQuotientNormalizationInertia_isGaloisField

L58 ↗
EtaleFundamentalGroups.Kummer.finiteQuotientNormalizationInertia_isGaloisField
Source context 18 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Kummer
universe u uA uG
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
variable [IsLocallyNoetherian X]
variable (W : FiniteEtale X) [hW : IsGalois W]
local instance finiteQuotientNormalizationInertia_isIntegral :
    IsIntegral W.left :=
  isIntegral_left_of_isConnected_finiteEtale W
local notation "K" => X.functionField
local notation "L" => W.left.functionField
local instance finiteQuotientNormalizationInertia_algebraKL : Algebra K L :=
  finiteEtaleFunctionFieldAlgebra W
variable (A : Type uA) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
variable [Algebra A X.functionField] [IsFractionRing A X.functionField]
local instance finiteQuotientNormalizationInertia_algebraAL : Algebra A L :=
  ((algebraMap K L).comp (algebraMap A K)).toAlgebra
local instance finiteQuotientNormalizationInertia_towerAKL :
    IsScalarTower A K L :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance finiteQuotientNormalizationInertia_finiteDimensional :
    FiniteDimensional K L :=
  finiteDimensional_functionField_of_finiteEtale_isConnected W
Lean source · statement
instance finiteQuotientNormalizationInertia_isGaloisField :
    _root_.IsGalois K L
instance

finiteQuotientNormalizationInertia_fractionRingB

L64 ↗
EtaleFundamentalGroups.Kummer.finiteQuotientNormalizationInertia_fractionRingB
Source context 20 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Kummer
universe u uA uG
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
variable [IsLocallyNoetherian X]
variable (W : FiniteEtale X) [hW : IsGalois W]
local instance finiteQuotientNormalizationInertia_isIntegral :
    IsIntegral W.left :=
  isIntegral_left_of_isConnected_finiteEtale W
local notation "K" => X.functionField
local notation "L" => W.left.functionField
local instance finiteQuotientNormalizationInertia_algebraKL : Algebra K L :=
  finiteEtaleFunctionFieldAlgebra W
variable (A : Type uA) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
variable [Algebra A X.functionField] [IsFractionRing A X.functionField]
local instance finiteQuotientNormalizationInertia_algebraAL : Algebra A L :=
  ((algebraMap K L).comp (algebraMap A K)).toAlgebra
local instance finiteQuotientNormalizationInertia_towerAKL :
    IsScalarTower A K L :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance finiteQuotientNormalizationInertia_finiteDimensional :
    FiniteDimensional K L :=
  finiteDimensional_functionField_of_finiteEtale_isConnected W
local instance finiteQuotientNormalizationInertia_isGaloisField :
    _root_.IsGalois K L :=
  isGalois_functionField_of_isGalois_finiteEtale W hW
local notation "B" => integralClosure A L
Lean source · statement
instance finiteQuotientNormalizationInertia_fractionRingB :
    IsFractionRing B L
instance

finiteQuotientNormalizationInertia_galoisAction

L68 ↗
EtaleFundamentalGroups.Kummer.finiteQuotientNormalizationInertia_galoisAction
Source context 21 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Kummer
universe u uA uG
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
variable [IsLocallyNoetherian X]
variable (W : FiniteEtale X) [hW : IsGalois W]
local instance finiteQuotientNormalizationInertia_isIntegral :
    IsIntegral W.left :=
  isIntegral_left_of_isConnected_finiteEtale W
local notation "K" => X.functionField
local notation "L" => W.left.functionField
local instance finiteQuotientNormalizationInertia_algebraKL : Algebra K L :=
  finiteEtaleFunctionFieldAlgebra W
variable (A : Type uA) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
variable [Algebra A X.functionField] [IsFractionRing A X.functionField]
local instance finiteQuotientNormalizationInertia_algebraAL : Algebra A L :=
  ((algebraMap K L).comp (algebraMap A K)).toAlgebra
local instance finiteQuotientNormalizationInertia_towerAKL :
    IsScalarTower A K L :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance finiteQuotientNormalizationInertia_finiteDimensional :
    FiniteDimensional K L :=
  finiteDimensional_functionField_of_finiteEtale_isConnected W
local instance finiteQuotientNormalizationInertia_isGaloisField :
    _root_.IsGalois K L :=
  isGalois_functionField_of_isGalois_finiteEtale W hW
local notation "B" => integralClosure A L
local instance finiteQuotientNormalizationInertia_fractionRingB :
    IsFractionRing B L :=
  IsIntegralClosure.isFractionRing_of_finite_extension A K L B
Lean source · statement
instance finiteQuotientNormalizationInertia_galoisAction :
    MulSemiringAction Gal(L/K) B
instance

finiteQuotientNormalizationInertia_deckAction

L72 ↗
EtaleFundamentalGroups.Kummer.finiteQuotientNormalizationInertia_deckAction
Source context 22 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Kummer
universe u uA uG
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
variable [IsLocallyNoetherian X]
variable (W : FiniteEtale X) [hW : IsGalois W]
local instance finiteQuotientNormalizationInertia_isIntegral :
    IsIntegral W.left :=
  isIntegral_left_of_isConnected_finiteEtale W
local notation "K" => X.functionField
local notation "L" => W.left.functionField
local instance finiteQuotientNormalizationInertia_algebraKL : Algebra K L :=
  finiteEtaleFunctionFieldAlgebra W
variable (A : Type uA) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
variable [Algebra A X.functionField] [IsFractionRing A X.functionField]
local instance finiteQuotientNormalizationInertia_algebraAL : Algebra A L :=
  ((algebraMap K L).comp (algebraMap A K)).toAlgebra
local instance finiteQuotientNormalizationInertia_towerAKL :
    IsScalarTower A K L :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance finiteQuotientNormalizationInertia_finiteDimensional :
    FiniteDimensional K L :=
  finiteDimensional_functionField_of_finiteEtale_isConnected W
local instance finiteQuotientNormalizationInertia_isGaloisField :
    _root_.IsGalois K L :=
  isGalois_functionField_of_isGalois_finiteEtale W hW
local notation "B" => integralClosure A L
local instance finiteQuotientNormalizationInertia_fractionRingB :
    IsFractionRing B L :=
  IsIntegralClosure.isFractionRing_of_finite_extension A K L B
local instance finiteQuotientNormalizationInertia_galoisAction :
    MulSemiringAction Gal(L/K) B :=
  IsIntegralClosure.MulSemiringAction A K L B
Lean source · statement
instance finiteQuotientNormalizationInertia_deckAction :
    MulSemiringAction (Aut W)ᵐᵒᵖ B
theorem

finiteQuotient_normalizationInertiaImage_coprime

L79 ↗
EtaleFundamentalGroups.Kummer.finiteQuotient_normalizationInertiaImage_coprime
Documentation

Coprimality of inertia at a prime of the original normalization passes through a pointed-cover realization to the corresponding image in any explicit finite quotient.

Source context 23 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Kummer
universe u uA uG
variable {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
variable [IsLocallyNoetherian X]
variable (W : FiniteEtale X) [hW : IsGalois W]
local instance finiteQuotientNormalizationInertia_isIntegral :
    IsIntegral W.left :=
  isIntegral_left_of_isConnected_finiteEtale W
local notation "K" => X.functionField
local notation "L" => W.left.functionField
local instance finiteQuotientNormalizationInertia_algebraKL : Algebra K L :=
  finiteEtaleFunctionFieldAlgebra W
variable (A : Type uA) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
variable [Algebra A X.functionField] [IsFractionRing A X.functionField]
local instance finiteQuotientNormalizationInertia_algebraAL : Algebra A L :=
  ((algebraMap K L).comp (algebraMap A K)).toAlgebra
local instance finiteQuotientNormalizationInertia_towerAKL :
    IsScalarTower A K L :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance finiteQuotientNormalizationInertia_finiteDimensional :
    FiniteDimensional K L :=
  finiteDimensional_functionField_of_finiteEtale_isConnected W
local instance finiteQuotientNormalizationInertia_isGaloisField :
    _root_.IsGalois K L :=
  isGalois_functionField_of_isGalois_finiteEtale W hW
local notation "B" => integralClosure A L
local instance finiteQuotientNormalizationInertia_fractionRingB :
    IsFractionRing B L :=
  IsIntegralClosure.isFractionRing_of_finite_extension A K L B
local instance finiteQuotientNormalizationInertia_galoisAction :
    MulSemiringAction Gal(L/K) B :=
  IsIntegralClosure.MulSemiringAction A K L B
local instance finiteQuotientNormalizationInertia_deckAction :
    MulSemiringAction (Aut W)ᵐᵒᵖ B :=
  finiteEtaleGaloisCoverNormalizationAction W hW A B
Lean source · statement
theorem finiteQuotient_normalizationInertiaImage_coprime
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶ X)
    (w : (fiber xi).obj W)
    {G : Type uG} [Group G]
    (e : (Aut W)ᵐᵒᵖ ≃* G)
    (phi : π₁ᵉᵗ(xi) →* G)
    (hcomp : e.toMonoidHom.comp
      (finiteEtaleGaloisCoverQuotientMonoidHom xi W hW w) = phi)
    (q : Ideal B) (p : ℕ)
    (hcoprime : Nat.Coprime
      (Nat.card (q.toAddSubgroup.inertia Gal(L/K))) p) :
    Nat.Coprime
      (Nat.card
        ((Subgroup.comap
          (finiteEtaleGaloisCoverQuotientMonoidHom xi W hW w)
          (q.toAddSubgroup.inertia (Aut W)ᵐᵒᵖ)).map phi)) p

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.