Different exponents in towers of local fields

For a finite separable tower M/L/K, the different exponent of M/K is the sum of the different exponent of M/L and the different exponent of L/K multiplied by the ramification index of M/L. This is the local form of transitivity of different ideals. The formula computes the exponent of a composite extension from its exponents over an intermediate local field. When L/K is unramified its different exponent vanishes, so d(M/K) = d(M/L).

References

• J.-P. Serre, Local Fields, Chapter III, §4.

theorem TauCeti.differentExponent_tower (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension K L] [ValuativeExtension L M] [Algebra.IsSeparable K M] : differentExponent K M = differentExponent L M + ramificationIndex L M * differentExponent K L

In a tower of finite separable extensions of nonarchimedean local fields, d(M/K) = d(M/L) + e(M/L) d(L/K).

theorem TauCeti.IsUnramified.differentExponent_tower_eq (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension K L] [ValuativeExtension L M] [Algebra.IsSeparable K M] [IsUnramified K L] : differentExponent K M = differentExponent L M

In a tower M/L/K of finite separable extensions of nonarchimedean local fields with L/K unramified, d(M/K) = d(M/L).