The different under isomorphism

A base-field algebra equivalence between finite extensions of a nonarchimedean local field restricts to their rings of integers. It preserves the different ideal and its exponent, so these invariants depend only on the extension's isomorphism class (Serre, Local Fields, Chapter III, §6).

@[simp]

theorem TauCeti.differentIdeal_map_integerRingEquiv (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] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [Algebra.IsSeparable K L] (e : L ≃ₐ[K] M) : Ideal.map e.integerRingEquiv (differentIdeal ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) = differentIdeal ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation M).integer

The different ideal is carried to the different ideal by an equivalence of extensions.

theorem TauCeti.differentExponent_eq_of_algEquiv (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] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [Algebra.IsSeparable K L] (e : L ≃ₐ[K] M) : differentExponent K L = differentExponent K M

The different exponent is invariant under equivalence of finite extensions over K.