Total ramification in towers, and units of totally ramified extensions

The residue-degree characterization of total ramification and multiplicativity of residue degree show that a tower is totally ramified exactly when each step is. The predicate and characterization are defined in RamificationIndex and InertiaDegree, respectively. Since the residue fields of a totally ramified extension agree, units of the larger ring of integers are units of the smaller one up to principal units, and hence up to n-th powers for every n invertible in 𝒪[L].

Main results

• TauCeti.isTotallyRamified_tower_iff: total ramification is equivalent to total ramification of both steps of a tower.
• TauCeti.IsTotallyRamified.exists_eq_algebraMap_mul_pow: in a totally ramified extension, every unit of 𝒪[L] is a unit of 𝒪[K] times the n-th power of a unit of 𝒪[L], for every n invertible in 𝒪[L].

References

• J.-P. Serre, Corps Locaux, Chapter I, §4.

theorem TauCeti.isTotallyRamified_tower_iff (K : Type u_1) (L : Type u_2) [Field K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeExtension K L] (M : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension L M] : IsTotallyRamified K M ↔ IsTotallyRamified K L ∧ IsTotallyRamified L M

A tower is totally ramified exactly when both of its steps are totally ramified.

theorem TauCeti.IsTotallyRamified.trans (K : Type u_1) (L : Type u_2) [Field K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeExtension K L] (M : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension L M] (hKL : IsTotallyRamified K L) (hLM : IsTotallyRamified L M) : IsTotallyRamified K M

Total ramification is transitive in a tower.

theorem TauCeti.IsTotallyRamified.tower_bot (K : Type u_1) (L : Type u_2) [Field K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeExtension K L] (M : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension L M] (hKM : IsTotallyRamified K M) : IsTotallyRamified K L

The first step of a totally ramified tower is totally ramified.

theorem TauCeti.IsTotallyRamified.tower_top (K : Type u_1) (L : Type u_2) [Field K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeExtension K L] (M : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension L M] (hKM : IsTotallyRamified K M) : IsTotallyRamified L M

The second step of a totally ramified tower is totally ramified.

theorem TauCeti.IsTotallyRamified.exists_eq_algebraMap_mul_pow {K : Type u_1} {L : Type u_2} [Field K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeExtension K L] (h : IsTotallyRamified K L) {n : ℕ} (hn : IsUnit ↑n) (u : (↥(ValuativeRel.valuation L).integer)ˣ) : ∃ (a : (↥(ValuativeRel.valuation K).integer)ˣ) (w : (↥(ValuativeRel.valuation L).integer)ˣ), ↑u = (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) ↑a * ↑w ^ n

In a totally ramified extension of nonarchimedean local fields, every unit of 𝒪[L] is the image of a unit of 𝒪[K] times the n-th power of a unit of 𝒪[L], for every n invertible in 𝒪[L].