Coefficients of the different ideal in a tower

This file reads Mathlib's transitivity theorem for different ideals at a height-one prime. If A ⊆ B ⊆ C is a tower of Dedekind domains and Q is a height-one prime of C above P in B, then

mult_Q(𝔇(C/A)) = mult_Q(𝔇(C/B)) + e(Q/P) mult_P(𝔇(B/A)).

The first term comes from additivity of multiplicities on products. The second comes from the factorization law for an extended ideal: extending a prime from B to C multiplies its coefficient at Q by the ramification index. This is the ideal-theoretic coefficient formula used by the tower law for different exponents of function-field places.

Main results

• TauCeti.multiplicity_differentIdeal_tower: the coefficientwise transitivity formula.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Corollary 3.4.12.

theorem TauCeti.multiplicity_differentIdeal_tower (A : Type uA) {B : Type uB} {C : Type uC} [CommRing A] [CommRing B] [CommRing C] [IsDedekindDomain A] [IsDedekindDomain B] [IsDedekindDomain C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [Module.Finite A B] [Module.Finite B C] [Module.IsTorsionFree A B] [Module.IsTorsionFree B C] [Module.IsTorsionFree A C] [Algebra.IsSeparable (FractionRing A) (FractionRing C)] (P : IsDedekindDomain.HeightOneSpectrum B) (Q : IsDedekindDomain.HeightOneSpectrum C) [Q.asIdeal.LiesOver P.asIdeal] : multiplicity Q.asIdeal (differentIdeal A C) = multiplicity Q.asIdeal (differentIdeal B C) + Q.asIdeal.ramificationIdx B * multiplicity P.asIdeal (differentIdeal A B)

The coefficientwise tower law for different ideals: at a height-one prime Q of C above P in B, the coefficient of the different of C / A is the coefficient of the different of C / B plus the ramification index times the coefficient of the different of B / A.

This is the ideal-theoretic form of Stichtenoth, Corollary 3.4.12.