Documentation

Mathlib.NumberTheory.RamificationInertia.Basic

Ramification index and inertia degree #

Given P : Ideal S lying over p : Ideal R for the ring extension f : R ā†’+* S (assuming P and p are prime or maximal where needed), the ramification index Ideal.ramificationIdx f p P is the multiplicity of P in map f p, and the inertia degree Ideal.inertiaDeg f p P is the degree of the field extension (S / P) : (R / p).

Main results #

The main theorem Ideal.sum_ramification_inertia states that for all coprime P lying over p, Ī£ P, ramification_idx f p P * inertia_deg f p P equals the degree of the field extension Frac(S) : Frac(R).

Implementation notes #

Often the above theory is set up in the case where:

Notation #

In this file, e stands for the ramification index and f for the inertia degree of P over p, leaving p and P implicit.

source
šŸ“ coverage
theorem Ideal.FinrankQuotientMap.span_eq_top {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) {K : Type u_1} [Field K] [Algebra R K] {L : Type u_2} [Field L] [Algebra S L] [IsFractionRing S L] [IsDomain R] [IsDomain S] [Algebra K L] [Module.Finite R S] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Algebra.IsAlgebraic R S] [Module.IsTorsionFree R K] (hp : p ā‰  āŠ¤) (b : Set S) (hb' : Submodule.span R b āŠ” Submodule.restrictScalars R (map (algebraMap R S) p) = āŠ¤) :
Submodule.span K (ā‡‘(algebraMap S L) '' b) = āŠ¤

If b mod p spans S/p as R/p-space, then b itself spans Frac(S) as K-space.

Here,

  • p is an ideal of R such that R / p is nontrivial
  • K is a field that has an embedding of R (in particular we can take K = Frac(R))
  • L is a field extension of K
  • S is the integral closure of R in L

More precisely, we avoid quotients in this statement and instead require that b āˆŖ pS spans S.

source
šŸ“ coverage
theorem Ideal.FinrankQuotientMap.linearIndependent_of_nontrivial {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (K : Type u_1) [Field K] [Algebra R K] {V : Type u_3} {V' : Type u_4} {V'' : Type u_5} [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] [AddCommGroup V'] [Module R V'] [Module S V'] [IsScalarTower R S V'] [AddCommGroup V''] [Module R V''] [hRK : IsFractionRing R K] [IsDedekindDomain R] (hRS : RingHom.ker (algebraMap R S) ā‰  āŠ¤) (F : V'' ā†’ā‚—[R] V) (hf : Function.Injective ā‡‘F) (f' : V'' ā†’ā‚—[R] V') {Ī¹ : Type u_6} {b : Ī¹ ā†’ V''} (hb' : LinearIndependent S (ā‡‘f' āˆ˜ b)) :
LinearIndependent K (ā‡‘F āˆ˜ b)

Let V be a vector space over K = Frac(R), S / R a ring extension and V' a module over S. If b, in the intersection V'' of V and V', is linear independent over S in V', then it is linear independent over R in V.

The statement we prove is actually slightly more general:

  • it suffices that the inclusion algebraMap R S : R ā†’ S is nontrivial
  • the function f' : V'' ā†’ V' doesn't need to be injective
source
šŸ“ coverage
theorem Ideal.finrank_quotient_map {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (K : Type u_1) [Field K] [Algebra R K] (L : Type u_2) [Field L] [Algebra S L] [IsFractionRing S L] [hRK : IsFractionRing R K] [IsDomain S] [IsDedekindDomain R] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] [hp : p.IsMaximal] [Module.Finite R S] :
Module.finrank (R ā§ø p) (S ā§ø map (algebraMap R S) p) = Module.finrank K L

If p is a maximal ideal of R, and S is the integral closure of R in L, then the dimension [S/pS : R/p] is equal to [Frac(S) : Frac(R)].

source
šŸ”ø coverage
@[implicit_reducible]
noncomputable instance Ideal.Quotient.algebraQuotientPowRamificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) :
Algebra (R ā§ø p) (S ā§ø P ^ p.ramificationIdx P)

R / p has a canonical map to S / (P ^ e), where e is the ramification index of P over p.

source
šŸ“ coverage
@[simp]
theorem Ideal.Quotient.algebraMap_quotient_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) (x : R) :
(algebraMap (R ā§ø p) (S ā§ø P ^ p.ramificationIdx P)) ((mk p) x) = (mk (P ^ p.ramificationIdx P)) ((algebraMap R S) x)
source
šŸ”ø coverage
@[implicit_reducible]
def Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [hfp : NeZero (p.ramificationIdx P)] :
Algebra (R ā§ø p) (S ā§ø P)

If P lies over p, then R / p has a canonical map to S / P.

This can't be an instance since the map f : R ā†’ S is generally not inferable.

Instances For
    source
    šŸ“ coverage
    @[simp]
    theorem Ideal.Quotient.algebraMap_quotient_of_ramificationIdx_neZero {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [NeZero (p.ramificationIdx P)] (x : R) :
    (algebraMap (R ā§ø p) (S ā§ø P)) ((mk p) x) = (mk P) ((algebraMap R S) x)
    source
    šŸ”ø coverage
    noncomputable def Ideal.powQuotSuccInclusion {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) (i : ā„•) :
    ā†„(map (Quotient.mk (P ^ p.ramificationIdx P)) (P ^ (i + 1))) ā†’ā‚—[R ā§ø p] ā†„(map (Quotient.mk (P ^ p.ramificationIdx P)) (P ^ i))

    The inclusion (P^(i + 1) / P^e) āŠ‚ (P^i / P^e).

    Instances For
      source
      šŸ“ coverage
      @[simp]
      theorem Ideal.powQuotSuccInclusion_apply_coe {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) (i : ā„•) (x : ā†„(map (Quotient.mk (P ^ p.ramificationIdx P)) (P ^ (i + 1)))) :
      ā†‘((p.powQuotSuccInclusion P i) x) = ā†‘x
      source
      šŸ“ coverage
      theorem Ideal.powQuotSuccInclusion_injective {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) (i : ā„•) :
      Function.Injective ā‡‘(p.powQuotSuccInclusion P i)
      source
      šŸ”ø coverage
      noncomputable def Ideal.quotientToQuotientRangePowQuotSuccAux {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) {i : ā„•} {a : S} (a_mem : a āˆˆ P ^ i) :
      S ā§ø P ā†’ ā†„(map (Quotient.mk (P ^ p.ramificationIdx P)) (P ^ i)) ā§ø (p.powQuotSuccInclusion P i).range

      S ā§ø P embeds into the quotient by P^(i+1) ā§ø P^e as a subspace of P^i ā§ø P^e. See quotientToQuotientRangePowQuotSucc for this as a linear map, and quotientRangePowQuotSuccInclusionEquiv for this as a linear equivalence.

      Instances For
        source
        šŸ“ coverage
        theorem Ideal.quotientToQuotientRangePowQuotSuccAux_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) {i : ā„•} {a : S} (a_mem : a āˆˆ P ^ i) (x : S) :
        p.quotientToQuotientRangePowQuotSuccAux P a_mem (Submodule.Quotient.mk x) = Submodule.Quotient.mk āŸØ(Quotient.mk (P ^ p.ramificationIdx P)) (a * x), ā‹ÆāŸ©
        source
        šŸ”ø coverage
        noncomputable def Ideal.quotientToQuotientRangePowQuotSucc {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [hfp : NeZero (p.ramificationIdx P)] {i : ā„•} {a : S} (a_mem : a āˆˆ P ^ i) :
        S ā§ø P ā†’ā‚—[R ā§ø p] ā†„(map (Quotient.mk (P ^ p.ramificationIdx P)) (P ^ i)) ā§ø (p.powQuotSuccInclusion P i).range

        S ā§ø P embeds into the quotient by P^(i+1) ā§ø P^e as a subspace of P^i ā§ø P^e.

        Instances For
          source
          šŸ“ coverage
          theorem Ideal.quotientToQuotientRangePowQuotSucc_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [hfp : NeZero (p.ramificationIdx P)] {i : ā„•} {a : S} (a_mem : a āˆˆ P ^ i) (x : S) :
          (p.quotientToQuotientRangePowQuotSucc P a_mem) (Submodule.Quotient.mk x) = Submodule.Quotient.mk āŸØ(Quotient.mk (P ^ p.ramificationIdx P)) (a * x), ā‹ÆāŸ©
          source
          šŸ“ coverage
          theorem Ideal.quotientToQuotientRangePowQuotSucc_injective {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [hfp : NeZero (p.ramificationIdx P)] [IsDedekindDomain S] [P.IsPrime] {i : ā„•} (hi : i < p.ramificationIdx P) {a : S} (a_mem : a āˆˆ P ^ i) (a_notMem : a āˆ‰ P ^ (i + 1)) :
          Function.Injective ā‡‘(p.quotientToQuotientRangePowQuotSucc P a_mem)
          source
          šŸ“ coverage
          theorem Ideal.quotientToQuotientRangePowQuotSucc_surjective {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [hfp : NeZero (p.ramificationIdx P)] [IsDedekindDomain S] (hP0 : P ā‰  āŠ„) [hP : P.IsPrime] {i : ā„•} (hi : i < p.ramificationIdx P) {a : S} (a_mem : a āˆˆ P ^ i) (a_notMem : a āˆ‰ P ^ (i + 1)) :
          Function.Surjective ā‡‘(p.quotientToQuotientRangePowQuotSucc P a_mem)
          source
          šŸ”ø coverage
          noncomputable def Ideal.quotientRangePowQuotSuccInclusionEquiv {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [hfp : NeZero (p.ramificationIdx P)] [IsDedekindDomain S] [P.IsPrime] (hP : P ā‰  āŠ„) {i : ā„•} (hi : i < p.ramificationIdx P) :
          (ā†„(map (Quotient.mk (P ^ p.ramificationIdx P)) (P ^ i)) ā§ø (p.powQuotSuccInclusion P i).range) ā‰ƒā‚—[R ā§ø p] S ā§ø P

          Quotienting P^i / P^e by its subspace P^(i+1) ā§ø P^e is R ā§ø p-linearly isomorphic to S ā§ø P.

          Instances For
            source
            šŸ“ coverage
            theorem Ideal.rank_pow_quot_aux {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [hfp : NeZero (p.ramificationIdx P)] [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ā‰  āŠ„) {i : ā„•} (hi : i < p.ramificationIdx P) :
            Module.rank (R ā§ø p) ā†„(map (Quotient.mk (P ^ p.ramificationIdx P)) (P ^ i)) = Module.rank (R ā§ø p) (S ā§ø P) + Module.rank (R ā§ø p) ā†„(map (Quotient.mk (P ^ p.ramificationIdx P)) (P ^ (i + 1)))

            Since the inclusion (P^(i + 1) / P^e) āŠ‚ (P^i / P^e) has a kernel isomorphic to P / S, [P^i / P^e : R / p] = [P^(i+1) / P^e : R / p] + [P / S : R / p]

            source
            šŸ“ coverage
            theorem Ideal.rank_pow_quot {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [hfp : NeZero (p.ramificationIdx P)] [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ā‰  āŠ„) (i : ā„•) (hi : i ā‰¤ p.ramificationIdx P) :
            Module.rank (R ā§ø p) ā†„(map (Quotient.mk (P ^ p.ramificationIdx P)) (P ^ i)) = (p.ramificationIdx P - i) ā€¢ Module.rank (R ā§ø p) (S ā§ø P)
            source
            šŸ“ coverage
            theorem Ideal.rank_prime_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ā‰  āŠ„) (he : p.ramificationIdx P ā‰  0) :
            Module.rank (R ā§ø p) (S ā§ø P ^ p.ramificationIdx P) = p.ramificationIdx P ā€¢ Module.rank (R ā§ø p) (S ā§ø P)

            If p is a maximal ideal of R, S extends R and P^e lies over p, then the dimension [S/(P^e) : R/p] is equal to e * [S/P : R/p].

            source
            šŸ“ coverage
            theorem Ideal.finrank_prime_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [IsDedekindDomain S] (hP0 : P ā‰  āŠ„) [p.IsMaximal] [P.IsPrime] (he : p.ramificationIdx P ā‰  0) :
            Module.finrank (R ā§ø p) (S ā§ø P ^ p.ramificationIdx P) = p.ramificationIdx P * Module.finrank (R ā§ø p) (S ā§ø P)

            If p is a maximal ideal of R, S extends R and P^e lies over p, then the dimension [S/(P^e) : R/p], as a natural number, is equal to e * [S/P : R/p].

            Properties of the factors of p.map (algebraMap R S) #

            source
            theorem Ideal.Factors.ne_bot {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) [IsDedekindDomain S] (P : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) :
            ā†‘P ā‰  āŠ„
            source
            šŸ“ coverage
            instance Ideal.Factors.isPrime {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) [IsDedekindDomain S] (P : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) :
            (ā†‘P).IsPrime
            source
            theorem Ideal.Factors.ramificationIdx_ne_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) [IsDedekindDomain S] (P : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) :
            p.ramificationIdx ā†‘P ā‰  0
            source
            šŸ“ coverage
            instance Ideal.Factors.fact_ramificationIdx_neZero {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) [IsDedekindDomain S] (P : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) :
            NeZero (p.ramificationIdx ā†‘P)
            source
            šŸ“ coverage
            instance Ideal.Factors.isScalarTower {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) [IsDedekindDomain S] (P : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) :
            IsScalarTower R (R ā§ø p) (S ā§ø ā†‘P)
            source
            šŸ“ coverage
            instance Ideal.Factors.liesOver {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) [IsDedekindDomain S] [p.IsMaximal] (P : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) :
            (ā†‘P).LiesOver p
            source
            šŸ“ coverage
            theorem Ideal.Factors.finrank_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) [IsDedekindDomain S] [p.IsMaximal] (P : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) :
            Module.finrank (R ā§ø p) (S ā§ø ā†‘P ^ p.ramificationIdx ā†‘P) = p.ramificationIdx ā†‘P * p.inertiaDeg ā†‘P
            source
            šŸ“ coverage
            instance Ideal.Factors.finiteDimensional_quotient_pow {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) [IsDedekindDomain S] [Module.Finite R S] [p.IsMaximal] (P : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) :
            FiniteDimensional (R ā§ø p) (S ā§ø ā†‘P ^ p.ramificationIdx ā†‘P)
            source
            šŸ”ø coverage
            noncomputable def Ideal.Factors.piQuotientEquiv {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [IsDedekindDomain S] (p : Ideal R) (hp : map (algebraMap R S) p ā‰  āŠ„) :
            S ā§ø map (algebraMap R S) p ā‰ƒ+* ((P : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) ā†’ S ā§ø ā†‘P ^ p.ramificationIdx ā†‘P)

            Chinese remainder theorem for a ring of integers: if the prime ideal p : Ideal R factors in S as āˆ i, P i ^ e i, then S ā§ø I factors as Ī  i, R ā§ø (P i ^ e i).

            Instances For
              source
              šŸ“ coverage
              @[simp]
              theorem Ideal.Factors.piQuotientEquiv_mk {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [IsDedekindDomain S] (p : Ideal R) (hp : map (algebraMap R S) p ā‰  āŠ„) (x : S) :
              (piQuotientEquiv p hp) ((Quotient.mk (map (algebraMap R S) p)) x) = fun (x_1 : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) => (Quotient.mk (ā†‘x_1 ^ p.ramificationIdx ā†‘x_1)) x
              source
              šŸ“ coverage
              @[simp]
              theorem Ideal.Factors.piQuotientEquiv_map {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [IsDedekindDomain S] (p : Ideal R) (hp : map (algebraMap R S) p ā‰  āŠ„) (x : R) :
              (piQuotientEquiv p hp) ((algebraMap R (S ā§ø map (algebraMap R S) p)) x) = fun (x_1 : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) => (Quotient.mk (ā†‘x_1 ^ p.ramificationIdx ā†‘x_1)) ((algebraMap R S) x)
              source
              šŸ”ø coverage
              noncomputable def Ideal.Factors.piQuotientLinearEquiv {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [IsDedekindDomain S] (p : Ideal R) (hp : map (algebraMap R S) p ā‰  āŠ„) :
              (S ā§ø map (algebraMap R S) p) ā‰ƒā‚—[R ā§ø p] (P : ā†„(UniqueFactorizationMonoid.factors (map (algebraMap R S) p)).toFinset) ā†’ S ā§ø ā†‘P ^ p.ramificationIdx ā†‘P

              Chinese remainder theorem for a ring of integers: if the prime ideal p : Ideal R factors in S as āˆ i, P i ^ e i, then S ā§ø I factors R ā§ø I-linearly as Ī  i, R ā§ø (P i ^ e i).

              Instances For
                source
                šŸ“ coverage
                theorem Ideal.sum_ramification_inertia {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [IsDedekindDomain S] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ā‰  āŠ„) :
                āˆ‘ P āˆˆ primesOverFinset p S, p.ramificationIdx P * p.inertiaDeg P = Module.finrank K L

                The fundamental identity of ramification index e and inertia degree f: for P ranging over the primes lying over p, āˆ‘ P, e P * f P = [Frac(S) : Frac(R)]; here S is a finite R-module (and thus Frac(S) : Frac(R) is a finite extension) and p is maximal.

                source
                šŸ“ coverage
                theorem Ideal.inertiaDeg_le_finrank {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [IsDedekindDomain S] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (P : Ideal S) [hPā‚ : P.IsPrime] [hPā‚‚ : P.LiesOver p] (hp0 : p ā‰  āŠ„) :
                p.inertiaDeg P ā‰¤ Module.finrank K L
                source
                šŸ“ coverage
                theorem Ideal.ramificationIdx_le_finrank {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [IsDedekindDomain S] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (P : Ideal S) [hPā‚ : P.IsPrime] [hPā‚‚ : P.LiesOver p] :
                p.ramificationIdx P ā‰¤ Module.finrank K L
                source
                šŸ“ coverage
                theorem Ideal.card_primesOverFinset_le_finrank {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [IsDedekindDomain S] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ā‰  āŠ„) :
                (primesOverFinset p S).card ā‰¤ Module.finrank K L
                source
                šŸ“ coverage
                theorem Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [IsDedekindDomain S] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [IsLocalRing S] {p : Ideal R} [p.IsMaximal] (hp0 : p ā‰  āŠ„) :
                p.ramificationIdx (IsLocalRing.maximalIdeal S) * p.inertiaDeg (IsLocalRing.maximalIdeal S) = Module.finrank K L

                Ideal.sum_ramification_inertia, in the local (DVR) case.