Module

Field.lean

Nyll.EtaleFundamentalGroups.Inertia.Normalization.Field

3 declarations indexed from sourceView source ↗

Module documentation

The inertia field of a normalization prime

The localized inertia subgroup at a height-one normalization prime determines an actual intermediate field of the generic Galois extension. In residue characteristic zero, the degree from this fixed field to the total field is the ramification index. The usual tower formula then separates the total generic degree into its unramified and ramified factors.

Imports2

Imported by3

abbrev

localizedNormalizationInertiaField

L34 ↗

EtaleFundamentalGroups.localizedNormalizationInertiaField

Documentation

The fixed field of the inertia subgroup attached to a normalization prime after localization at the corresponding base prime.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
variable [CommRing A] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]

Lean source · statement

abbrev localizedNormalizationInertiaField
    (P : Ideal A) [P.IsPrime]
    (Q : Ideal (integralClosure A L)) :
    IntermediateField K L

theorem

finrank_localizedNormalizationInertiaField_eq_ramificationIdx

L46 ↗

EtaleFundamentalGroups.finrank_localizedNormalizationInertiaField_eq_ramificationIdx

Documentation

The extension above the localized inertia fixed field has degree equal to the ramification index of the selected normalization prime.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
variable [CommRing A] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [IsRegularRing A]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finrank_localizedNormalizationInertiaField_eq_ramificationIdx
    (P : Ideal A) [P.IsPrime] (hP : P.height = 1)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P]
    [CharZero (A ⧸ P)] :
    Module.finrank
        (localizedNormalizationInertiaField (K := K) (L := L) P Q) L =
      Q.ramificationIdx A

theorem

finrank_eq_finrank_localizedNormalizationInertiaField_mul_ramificationIdx

L69 ↗

EtaleFundamentalGroups.finrank_eq_finrank_localizedNormalizationInertiaField_mul_ramificationIdx

Documentation

The generic degree factors as the degree of the inertia fixed field times the ramification index.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
variable [CommRing A] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [IsRegularRing A]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finrank_eq_finrank_localizedNormalizationInertiaField_mul_ramificationIdx
    (P : Ideal A) [P.IsPrime] (hP : P.height = 1)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P]
    [CharZero (A ⧸ P)] :
    Module.finrank K L =
      Module.finrank K
          (localizedNormalizationInertiaField (K := K) (L := L) P Q) *
        Q.ramificationIdx A

Module documentation

The inertia field of a normalization prime

Declarations

localizedNormalizationInertiaField

finrank_localizedNormalizationInertiaField_eq_ramificationIdx

finrank_eq_finrank_localizedNormalizationInertiaField_mul_ramificationIdx