The Galois action on the unit filtration

Every automorphism of a finite extension of a nonarchimedean local field preserves its valuation. It therefore preserves every step of the unit filtration. This gives an action on each filtered unit group, compatible with its inclusion in the units of the field.

The stability is stated both elementwise and as equality of the image subgroup. The elementwise form installs the restricted action on unitFiltration L i; the image form is convenient when passing to successive quotients in ramification theory.

Main results

• AlgEquiv.unitsMap_mem_unitFiltration_iff: membership in U(L,i) is invariant under an extension automorphism.
• AlgEquiv.smul_unitFiltration: an extension automorphism maps U(L,i) onto itself.
• AlgEquiv.coe_smul_unitFiltration: the restricted action agrees with the action on Lˣ.
• AlgEquiv.val_coe_smul_unitFiltration: the restricted action agrees with applying the automorphism on L.

References

• J.-P. Serre, Local Fields, Chapter IV, §2.

@[simp]

theorem AlgEquiv.unitsMap_mem_unitFiltration_iff {K : Type u_1} {L : Type u_2} [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] (σ : Gal(L/K)) {i : ℕ} {x : Lˣ} : (Units.map ↑σ) x ∈ TauCeti.unitFiltration L i ↔ x ∈ TauCeti.unitFiltration L i

Membership in the unit filtration is invariant under every automorphism of a finite extension of a nonarchimedean local field. The action of σ on Lˣ is Units.map σ, so this is also the statement that σ • x ∈ unitFiltration L i ↔ x ∈ unitFiltration L i.

@[simp]

theorem AlgEquiv.smul_unitFiltration {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (σ : Gal(L/K)) (i : ℕ) : σ • TauCeti.unitFiltration L i = TauCeti.unitFiltration L i

Every automorphism of a finite extension of a nonarchimedean local field maps each step of the unit filtration onto itself.

@[instance_reducible]

noncomputable instance TauCeti.unitFiltrationMulDistribMulAction {K : Type u_1} {L : Type u_2} [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] (i : ℕ) : MulDistribMulAction Gal(L/K) ↥(unitFiltration L i)

The action of extension automorphisms on Lˣ restricts to every step U(L,i) of the unit filtration.

@[simp]

theorem AlgEquiv.coe_smul_unitFiltration {K : Type u_1} {L : Type u_2} [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] (σ : Gal(L/K)) {i : ℕ} (x : ↥(TauCeti.unitFiltration L i)) : ↑(σ • x) = σ • ↑x

The action on a step of the unit filtration agrees with the ambient action on Lˣ.

theorem AlgEquiv.val_coe_smul_unitFiltration {K : Type u_1} {L : Type u_2} [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] (σ : Gal(L/K)) {i : ℕ} (x : ↥(TauCeti.unitFiltration L i)) : ↑↑(σ • x) = σ ↑↑x

The value in L of the action on a step of the unit filtration is obtained by applying the automorphism.

noncomputable def TauCeti.unitFiltrationZeroIncl (K L : Type u) [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] : Rep.ofMulDistribMulAction Gal(L/K) ↥(unitFiltration L 0) ⟶ Rep.ofMulDistribMulAction Gal(L/K) Lˣ

Inclusion of the valuation-zero units in the multiplicative group, as a morphism of integral Galois representations.

@[simp]

theorem TauCeti.unitFiltrationZeroIncl_apply (K L : Type u) [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] (x : Additive ↥(unitFiltration L 0)) : (Rep.Hom.hom (unitFiltrationZeroIncl K L)) x = Additive.ofMul ↑(Additive.toMul x)

The inclusion is the subgroup inclusion, written additively.

theorem TauCeti.unitFiltrationZeroIncl_injective (K L : Type u) [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] : Function.Injective ⇑(Rep.Hom.hom (unitFiltrationZeroIncl K L))

The inclusion of the valuation-zero units in the multiplicative group is injective.