theorem RiemannHurwitzSheaf.differentIdeal_dvd_pow_sub_one (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] {P : Ideal B} [P.IsMaximal] [P.LiesOver p] (hp : p ≠ ⊥) : P ^ (p.ramificationIdx P - 1) ∣ differentIdeal A B

The different ideal 𝔡_{B/A} is divisible by P^{e_P - 1} for each prime P above a non-zero maximal ideal p of A.

theorem RiemannHurwitzSheaf.not_dvd_pow_ramificationIdx_of_tame (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] {P : Ideal B} [P.IsMaximal] [P.LiesOver p] (hp : p ≠ ⊥) (hP : P ≠ ⊥) (he : p.ramificationIdx P ≠ 0) (htame : (p.ramificationIdx P).Coprime (ringChar (B ⧸ P))) : ¬P ^ p.ramificationIdx P ∣ differentIdeal A B

In the tame case, P^{e_P} does not divide the different ideal 𝔡_{B/A}, so the exponent of P in 𝔡_{B/A} is exactly e_P - 1.

theorem RiemannHurwitzSheaf.differentIdeal_count_eq_ramificationIdx_sub_one (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] {P : Ideal B} [P.IsMaximal] [P.LiesOver p] (hp : p ≠ ⊥) (hP : P ≠ ⊥) (he : p.ramificationIdx P ≠ 0) (htame : (p.ramificationIdx P).Coprime (ringChar (B ⧸ P))) : Multiset.count P (UniqueFactorizationMonoid.normalizedFactors (differentIdeal A B)) = p.ramificationIdx P - 1

In the tame case, the multiplicity of P in the different ideal 𝔡_{B/A} is exactly e_P - 1. This is the local model behind Riemann–Hurwitz.

theorem RiemannHurwitzSheaf.differentIdeal_exact_pow (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] {P : Ideal B} [P.IsMaximal] [P.LiesOver p] (hp : p ≠ ⊥) (hP : P ≠ ⊥) (he : p.ramificationIdx P ≠ 0) (htame : (p.ramificationIdx P).Coprime (ringChar (B ⧸ P))) : P ^ (p.ramificationIdx P - 1) ∣ differentIdeal A B ∧ ¬P ^ p.ramificationIdx P ∣ differentIdeal A B

Combined statement of the two divisibility facts: P^{e_P - 1} divides the different ideal but P^{e_P} does not (in the tame case).