NYLL
Module

AbsoluteNormalizationPrime.lean

Nyll.EtaleFundamentalGroups.Inertia.AbsoluteNormalizationPrime
7 declarations indexed from sourceView source ↗

Module documentation

Absolute normalization-prime inertia

Fixing a prime in the normalization inside one separable closure gives a single absolute inertia subgroup. Its restriction to every finite normal subextension lies in the inertia subgroup of the contracted prime. This is the field-theoretic model of divisorial inertia and does not require a separate strict-henselization construction.

Imports1
Imported by3

Declarations

def

finiteNormalizationToAbsoluteNormalization

L41 ↗
EtaleFundamentalGroups.Inertia.finiteNormalizationToAbsoluteNormalization
Documentation

The map between normalizations induced by a chosen embedding of a finite normal extension into the fixed separable closure.

Source context 15 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe uA u
variable {A : Type uA} {K L Omega : Type u}
variable [CommRing A]
variable [Field K] [Field L] [Field Omega]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [Algebra K Omega] [Algebra A Omega] [IsScalarTower A K Omega]
variable [Algebra L Omega] [IsScalarTower K L Omega]
variable [IsScalarTower A L Omega]
variable [Algebra.IsAlgebraic K Omega]
local notation "B" => integralClosure A L
local notation "C" => integralClosure A Omega
Lean source · statement
def finiteNormalizationToAbsoluteNormalization : B →ₐ[A] C
def

absoluteNormalizationPrimeContraction

L46 ↗
EtaleFundamentalGroups.Inertia.absoluteNormalizationPrimeContraction
Documentation

Contraction of an absolute normalization prime to a finite normal subextension.

Source context 15 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe uA u
variable {A : Type uA} {K L Omega : Type u}
variable [CommRing A]
variable [Field K] [Field L] [Field Omega]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [Algebra K Omega] [Algebra A Omega] [IsScalarTower A K Omega]
variable [Algebra L Omega] [IsScalarTower K L Omega]
variable [IsScalarTower A L Omega]
variable [Algebra.IsAlgebraic K Omega]
local notation "B" => integralClosure A L
local notation "C" => integralClosure A Omega
Lean source · statement
def absoluteNormalizationPrimeContraction
    (Q : Ideal C) : Ideal B
instance

absoluteNormalizationPrimeContraction_isPrime

L51 ↗
EtaleFundamentalGroups.Inertia.absoluteNormalizationPrimeContraction_isPrime
Source context 15 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe uA u
variable {A : Type uA} {K L Omega : Type u}
variable [CommRing A]
variable [Field K] [Field L] [Field Omega]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [Algebra K Omega] [Algebra A Omega] [IsScalarTower A K Omega]
variable [Algebra L Omega] [IsScalarTower K L Omega]
variable [IsScalarTower A L Omega]
variable [Algebra.IsAlgebraic K Omega]
local notation "B" => integralClosure A L
local notation "C" => integralClosure A Omega
Lean source · statement
instance absoluteNormalizationPrimeContraction_isPrime
    (Q : Ideal C) [Q.IsPrime] :
    (absoluteNormalizationPrimeContraction
      (A := A) (L := L) (Omega := Omega) Q).IsPrime
instance

absoluteNormalizationPrimeContraction_liesOver

L61 ↗
EtaleFundamentalGroups.Inertia.absoluteNormalizationPrimeContraction_liesOver
Source context 15 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe uA u
variable {A : Type uA} {K L Omega : Type u}
variable [CommRing A]
variable [Field K] [Field L] [Field Omega]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [Algebra K Omega] [Algebra A Omega] [IsScalarTower A K Omega]
variable [Algebra L Omega] [IsScalarTower K L Omega]
variable [IsScalarTower A L Omega]
variable [Algebra.IsAlgebraic K Omega]
local notation "B" => integralClosure A L
local notation "C" => integralClosure A Omega
Lean source · statement
instance absoluteNormalizationPrimeContraction_liesOver
    (P : Ideal A) (Q : Ideal C) [Q.LiesOver P] :
    (absoluteNormalizationPrimeContraction
      (A := A) (L := L) (Omega := Omega) Q).LiesOver P
instance

finiteNormalization_galoisAction

L71 ↗
EtaleFundamentalGroups.Inertia.finiteNormalization_galoisAction
Source context 15 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe uA u
variable {A : Type uA} {K L Omega : Type u}
variable [CommRing A]
variable [Field K] [Field L] [Field Omega]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [Algebra K Omega] [Algebra A Omega] [IsScalarTower A K Omega]
variable [Algebra L Omega] [IsScalarTower K L Omega]
variable [IsScalarTower A L Omega]
variable [Algebra.IsAlgebraic K Omega]
local notation "B" => integralClosure A L
local notation "C" => integralClosure A Omega
Lean source · statement
instance finiteNormalization_galoisAction :
    MulSemiringAction Gal(L/K) B
instance

absoluteNormalization_galoisAction

L75 ↗
EtaleFundamentalGroups.Inertia.absoluteNormalization_galoisAction
Source context 16 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe uA u
variable {A : Type uA} {K L Omega : Type u}
variable [CommRing A]
variable [Field K] [Field L] [Field Omega]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [Algebra K Omega] [Algebra A Omega] [IsScalarTower A K Omega]
variable [Algebra L Omega] [IsScalarTower K L Omega]
variable [IsScalarTower A L Omega]
variable [Algebra.IsAlgebraic K Omega]
local notation "B" => integralClosure A L
local notation "C" => integralClosure A Omega
local instance finiteNormalization_galoisAction :
    MulSemiringAction Gal(L/K) B :=
  IsIntegralClosure.MulSemiringAction A K L B
Lean source · statement
instance absoluteNormalization_galoisAction :
    MulSemiringAction Gal(Omega/K) C
theorem

absoluteNormalizationPrime_inertia_map_le_contraction

L82 ↗
EtaleFundamentalGroups.Inertia.absoluteNormalizationPrime_inertia_map_le_contraction
Documentation

Absolute inertia restricts into inertia at the contracted prime in every finite normal subextension.

Source context 18 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe uA u
variable {A : Type uA} {K L Omega : Type u}
variable [CommRing A]
variable [Field K] [Field L] [Field Omega]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [Algebra K Omega] [Algebra A Omega] [IsScalarTower A K Omega]
variable [Algebra L Omega] [IsScalarTower K L Omega]
variable [IsScalarTower A L Omega]
variable [Algebra.IsAlgebraic K Omega]
local notation "B" => integralClosure A L
local notation "C" => integralClosure A Omega
local instance finiteNormalization_galoisAction :
    MulSemiringAction Gal(L/K) B :=
  IsIntegralClosure.MulSemiringAction A K L B
local instance absoluteNormalization_galoisAction :
    MulSemiringAction Gal(Omega/K) C :=
  IsIntegralClosure.MulSemiringAction A K Omega C
omit [FiniteDimensional K L] in
Lean source · statement
theorem absoluteNormalizationPrime_inertia_map_le_contraction
    (Q : Ideal C) [Q.IsPrime] :
    Subgroup.map
        (AlgEquiv.restrictNormalHom (F := K) (K₁ := Omega) L)
        (Q.toAddSubgroup.inertia Gal(Omega/K)) ≤
      (absoluteNormalizationPrimeContraction
        (A := A) (L := L) (Omega := Omega) Q).toAddSubgroup.inertia
          Gal(L/K)

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