Residue correspondence for unramified local extensions

For a finite unramified Galois extension L / K of nonarchimedean local fields, reduction gives an isomorphism from the Galois group of L / K to the Galois group of the residue-field extension. Its inverse carries the finite-field Frobenius to the Frobenius automorphism of L / K.

The residue action is surjective, and its kernel is the inertia group. Unramifiedness makes this kernel trivial, giving the residue correspondence. This also shows that Frobenius generates the Galois group and has order equal to the inertia degree. Without assuming unramifiedness, the quotient by inertia is cyclic because it embeds into the residue-field Galois group.

Main definitions

• TauCeti.residueFieldAutEquiv: the residue correspondence for an unramified Galois extension.
• TauCeti.frobeniusAlgEquiv: the lift of finite-field Frobenius to the extension.
• TauCeti.LocalFieldsRamification.isCyclic_quotient_lowerRamificationGroup_zero: the quotient of the Galois group by inertia is cyclic.

References

• J.-P. Serre, Local Fields, Chapter III, §5.
• J. Neukirch, Algebraic Number Theory, Chapter II, §7.

@[instance_reducible]

noncomputable def TauCeti.residueFieldFintype {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Fintype (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

The finite residue field of the base, equipped with a local Fintype instance.

Equations

• TauCeti.residueFieldFintype = Fintype.ofFinite (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

theorem TauCeti.ker_residueField_toAlgAut {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] [FiniteDimensional K L] : (MulSemiringAction.toAlgAut Gal(L/K) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)).ker = Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer)

The kernel of the action of the extension Galois group on the residue field is the inertia group.

theorem TauCeti.LocalFieldsRamification.isCyclic_quotient_lowerRamificationGroup_zero (K : Type u_3) (L : Type u_4) [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] : IsCyclic (Gal(L/K) ⧸ lowerRamificationGroup K L 0)

The quotient G / G_0 of the Galois group by inertia is cyclic: the action on the residue field identifies it with a subgroup of the Galois group of the finite residue field extension, which is cyclic.

theorem TauCeti.IsUnramified.inertia_eq_bot {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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer) = ⊥

The inertia group of an unramified finite Galois extension of local fields is trivial.

theorem TauCeti.residueField_toAlgAut_surjective {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] [FiniteDimensional K L] [IsGalois K L] : Function.Surjective ⇑(MulSemiringAction.toAlgAut Gal(L/K) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer))

Reduction from the Galois group to the residue-field Galois group is surjective.

theorem TauCeti.residueField_toAlgAut_bijective {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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : Function.Bijective ⇑(MulSemiringAction.toAlgAut Gal(L/K) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer))

Reduction is a bijection from the Galois group of an unramified extension to the Galois group of its residue-field extension.

noncomputable def TauCeti.residueFieldAutEquiv {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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : Gal(L/K) ≃* Gal(IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer/IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

The residue correspondence between the Galois groups of an unramified local extension and its residue-field extension.

Equations

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

@[simp]

theorem TauCeti.residueFieldAutEquiv_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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (σ : Gal(L/K)) : residueFieldAutEquiv σ = (MulSemiringAction.toAlgAut Gal(L/K) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)) σ

The residue correspondence is the canonical action on the residue field.

noncomputable def TauCeti.frobeniusAlgEquiv {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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : Gal(L/K)

The Frobenius automorphism of an unramified local extension is the unique lift of the finite-field Frobenius on its residue field.

Equations

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

@[simp]

theorem TauCeti.residueField_toAlgEquiv_frobeniusAlgEquiv {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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : MulSemiringAction.toAlgEquiv (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) frobeniusAlgEquiv = FiniteField.frobeniusAlgEquivOfAlgebraic (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)

The residue-field action sends local Frobenius to finite-field Frobenius.

theorem TauCeti.orderOf_frobeniusAlgEquiv {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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : orderOf frobeniusAlgEquiv = inertiaDegree K L

The order of Frobenius is the inertia degree of an unramified local extension.

theorem TauCeti.zpowers_frobeniusAlgEquiv {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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : Subgroup.zpowers frobeniusAlgEquiv = ⊤

Frobenius generates the Galois group of an unramified local extension.

instance TauCeti.isCyclic_algEquiv {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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] : IsCyclic Gal(L/K)

The Galois group of an unramified local extension is cyclic.

theorem TauCeti.valuation_frobeniusAlgEquiv_sub_pow {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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (y : ↥(ValuativeRel.valuation L).integer) : (ValuativeRel.valuation L) (frobeniusAlgEquiv ↑y - ↑y ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) < 1

Frobenius satisfies its characteristic congruence modulo the maximal ideal.

theorem TauCeti.eq_frobeniusAlgEquiv_of_valuation_sub_pow_lt_one {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] [FiniteDimensional K L] [IsGalois K L] [IsUnramified K L] (σ : Gal(L/K)) (hσ : ∀ (y : ↥(ValuativeRel.valuation L).integer), (ValuativeRel.valuation L) (σ ↑y - ↑y ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) < 1) : σ = frobeniusAlgEquiv

An automorphism satisfying the characteristic Frobenius congruence is Frobenius.