Module

NormalCardinality.lean

Nyll.EtaleFundamentalGroups.Inertia.Localized.NormalCardinality

2 declarations indexed from sourceView source ↗

Module documentation

Inertia cardinality over a normal Noetherian base

At a height-one prime, normality and Noetherianity already make the local base a discrete valuation ring. Thus the inertia-cardinality formula does not require regularity of the ambient ring.

Imports3

Imported by3

theorem

localizedNormalizationInertia_card_eq_ramificationIdx_of_normal_noetherian

L35 ↗

EtaleFundamentalGroups.localizedNormalizationInertia_card_eq_ramificationIdx_of_normal_noetherian

Documentation

At a height-one prime of a normal Noetherian domain, localized normalization inertia has cardinality equal to 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] [IsNoetherianRing A]
variable [IsIntegrallyClosed 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 [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem localizedNormalizationInertia_card_eq_ramificationIdx_of_normal_noetherian
    (P : Ideal A) [P.IsPrime] (hP : P.height = 1)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P]
    [CharZero (A ⧸ P)] :
    Nat.card
        (localizedNormalizationInertia (K := K) (L := L) P Q) =
      Q.ramificationIdx A

theorem

normalizationInertia_card_eq_ramificationIdx_of_normal_noetherian

L96 ↗

EtaleFundamentalGroups.normalizationInertia_card_eq_ramificationIdx_of_normal_noetherian