Automorphisms of finite extensions acting on integral and residue data

An automorphism of a finite extension of a nonarchimedean local field preserves the unique extended valuation. Consequently it restricts to the ring of integers and its maximal ideal, and descends to the residue field. This file constructs those three actions and records their compatibility with inclusion and reduction, including the comparison with the residue-field embedding AlgHom.residueFieldHom induced by an arbitrary K-embedding.

The induced residue-field automorphism is linear over the residue field of the base. It therefore gives the canonical homomorphism between the corresponding automorphism groups. When the field extension is Galois, the kernel of this homomorphism is the inertia group in ramification theory.

Main definitions

• AlgEquiv.integerRingEquiv: restriction of a field equivalence to the ring of integers.
• AlgEquiv.maximalIdealEquiv: restriction to the maximal ideal.
• AlgEquiv.residueFieldEquiv: the induced automorphism of the residue field.

The homomorphism from field automorphisms to residue-field automorphisms is Mathlib's generic MulSemiringAction.toAlgAut applied to the action constructed here.

Main results

• TauCeti.decompositionSubgroup_valuationSubring_eq_top: every automorphism preserves the valuation subring of L, so Mathlib's ValuationSubring.decompositionSubgroup is everything.
• TauCeti.integerRingFaithfulSMul: an automorphism is determined by its action on 𝒪[L].
• AlgEquiv.restrictScalars_smul_integerRing and AlgEquiv.smul_algebraMap_integerRing: the action is compatible with restricting scalars to a subextension and with restricting an automorphism to a normal subextension.
• TauCeti.integerRingSMulCommClass: the action on 𝒪[L] is by 𝒪[K]-algebra automorphisms.
• AlgEquiv.toAlgHom_residueFieldHom: for an automorphism, the residue-field embedding AlgHom.residueFieldHom is the induced automorphism AlgEquiv.residueFieldEquiv.
• AlgEquiv.normalizedValuation_unitsMap: an extension automorphism preserves the normalized valuation of a unit.

References

• J.-P. Serre, Local Fields, Chapter I, §§7–8 and Chapter IV, §1.

instance TauCeti.integerRingIsInvariantSubring {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : IsInvariantSubring Gal(L/K) (ValuativeRel.valuation L).integer

The ring of integers is stable under every automorphism of a finite extension of a nonarchimedean local field.

theorem TauCeti.decompositionSubgroup_valuationSubring_eq_top (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : ValuationSubring.decompositionSubgroup K (ValuativeRel.valuation L).valuationSubring = ⊤

Every automorphism of L/K preserves the valuation subring of L, so its decomposition subgroup is the whole automorphism group.

instance TauCeti.integerRingSMulDistribClass {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : SMulDistribClass Gal(L/K) (↥(ValuativeRel.valuation L).integer) L

Scalar multiplication by an extension automorphism is compatible with multiplication by an integer of the extension.

instance TauCeti.integerRingIsGaloisGroup {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] [IsGalois K L] : IsGaloisGroup Gal(L/K) ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

The Galois action on a finite extension restricts to a Galois-group action on its ring of integers.

@[simp]

theorem AlgEquiv.coe_smul_integerRing {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (σ : Gal(L/K)) (x : ↥(ValuativeRel.valuation L).integer) : ↑(σ • x) = σ ↑x

Coercing the action on the integer ring to L recovers the field automorphism.

@[simp]

theorem AlgEquiv.integerRingEquiv_apply {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (σ : Gal(L/K)) (x : ↥(ValuativeRel.valuation L).integer) : σ.integerRingEquiv x = σ • x

The integer-ring equivalence agrees with the canonical automorphism action.

@[simp]

theorem AlgEquiv.restrictScalars_smul_integerRing {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {K' : Type u_3} [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] [Algebra K K'] [Algebra K' L] [IsScalarTower K K' L] [ValuativeExtension K' L] [Module.Finite K' L] (σ : Gal(L/K')) (x : ↥(ValuativeRel.valuation L).integer) : restrictScalars K σ • x = σ • x

Restricting the scalars of an automorphism along a tower L/K'/K does not change its action on the ring of integers of L.

@[simp]

theorem AlgEquiv.smul_algebraMap_integerRing {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {K' : Type u_3} [Field K'] [ValuativeRel K'] [Algebra K K'] [Algebra K' L] [IsScalarTower K K' L] [ValuativeExtension K K'] [ValuativeExtension K' L] [Module.Finite K K'] [Normal K K'] (σ : Gal(L/K)) (w : ↥(ValuativeRel.valuation K').integer) : σ • (algebraMap ↥(ValuativeRel.valuation K').integer ↥(ValuativeRel.valuation L).integer) w = (algebraMap ↥(ValuativeRel.valuation K').integer ↥(ValuativeRel.valuation L).integer) (σ.restrictNormal K' • w)

For a subextension K' of L/K normal over K, an automorphism of L/K acts on the image of the ring of integers of K' through its restriction to K'.

noncomputable def AlgEquiv.maximalIdealEquiv {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)) : ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer) ≃+* ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer)

The automorphism induced on the maximal ideal of the ring of integers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgEquiv.coe_maximalIdealEquiv {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)) (x : ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer)) : ↑↑(σ.maximalIdealEquiv x) = σ ↑↑x

Coercing the induced maximal-ideal automorphism to L recovers the field automorphism.

noncomputable def AlgEquiv.residueFieldEquiv {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)) : Gal(IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer/IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

The automorphism induced on the residue field by a field automorphism. It fixes the residue field of the base extension.

Equations

• σ.residueFieldEquiv = IsLocalRing.ResidueField.mapAlgEquiv' σ.integerRingEquiv

@[simp]

theorem AlgEquiv.residueFieldEquiv_apply {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)) (x : IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) : σ.residueFieldEquiv x = σ • x

The induced residue-field equivalence agrees with the canonical residue-field action.

@[simp]

theorem AlgEquiv.toAlgHom_residueFieldHom {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)) : (↑σ).residueFieldHom = ↑σ.residueFieldEquiv

For an automorphism, the induced embedding of residue fields is the induced automorphism AlgEquiv.residueFieldEquiv.

@[simp]

theorem AlgEquiv.normalizedValuation_unitsMap {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)) (x : Lˣ) : (TauCeti.normalizedValuation L) ((Units.map ↑σ) x) = (TauCeti.normalizedValuation L) x

Every automorphism of a finite extension of a nonarchimedean local field preserves the normalized valuation of a unit. The action of σ on Lˣ is Units.map σ, so this is also the statement that normalizedValuation L (σ • x) = normalizedValuation L x.

instance TauCeti.integerRingSMulCommClass {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : SMulCommClass Gal(L/K) ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

Automorphisms act on the ring of integers by 𝒪[K]-algebra automorphisms: the action commutes with the scalars from the ring of integers of the base field.

instance TauCeti.residueFieldSMulCommClass {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] : SMulCommClass Gal(L/K) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)

The residue-field action of extension automorphisms fixes the base residue field.

@[instance_reducible]

noncomputable instance TauCeti.maximalIdealDistribMulAction {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] : DistribMulAction Gal(L/K) ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer)

Field automorphisms act on the maximal ideal by restriction of their action on the ring of integers.

Equations

• TauCeti.maximalIdealDistribMulAction = { smul := fun (σ : Gal(L/K)) => ⇑σ.maximalIdealEquiv, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[simp]

theorem TauCeti.smul_maximalIdeal_eq {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)) (x : ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer)) : σ • x = σ.maximalIdealEquiv x

The maximal-ideal action is the restriction represented by AlgEquiv.maximalIdealEquiv.

theorem TauCeti.residueField_toAlgAut_apply {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)) (x : IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) : ((MulSemiringAction.toAlgAut Gal(L/K) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)) σ) x = σ.residueFieldEquiv x

Evaluating the canonical residue-field automorphism homomorphism gives the induced residue-field equivalence.

instance TauCeti.integerRingFaithfulSMul {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] : FaithfulSMul Gal(L/K) ↥(ValuativeRel.valuation L).integer

An automorphism of a finite extension is determined by its action on the ring of integers, since every element of L becomes integral after multiplication by a nonzero integer of K.