Frobenius in unramified local fields

The arithmetic Frobenius of a finite unramified extension is compatible with restriction through a normal intermediate field. This identifies the Frobenius elements at different finite levels of an unramified tower, rather than merely identifying arbitrary generators of their cyclic Galois groups. Under a change of ground field K ⊆ K', the Frobenius of an unramified extension of K' restricts to the power of the Frobenius over K by the residue degree of K'/K. The Teichmüller lifts of a residue element's Frobenius image and its power by the cardinality of the base residue field agree. Frobenius raises prime-to-residue-characteristic roots of unity to that same power.

Main result

• TauCeti.frobeniusAlgEquiv_restrictNormal: restricting arithmetic Frobenius to a normal intermediate field gives arithmetic Frobenius there.
• TauCeti.frobeniusAlgEquiv_restrictScalars_restrictNormal: the arithmetic Frobenius of L'/K' restricts on L ⊆ L' to the f(K'/K)-th power of the arithmetic Frobenius of L/K.
• TauCeti.frobeniusAlgEquiv_teichmullerLift: the Teichmüller lifts of the Frobenius action on a residue element and its q-th power agree.
• TauCeti.frobeniusAlgEquiv_rootsOfUnity: on prime-to-residue-characteristic roots of unity, arithmetic Frobenius acts by the q-th power map.
• TauCeti.frobeniusAlgEquiv_apply_of_pow_eq_one: the same holds for every root of unity whose order is invertible in 𝒪[L], not only for the (q_L − 1)-st roots of unity.
• TauCeti.frobeniusAlgEquiv_apply_of_pow_natCard_pow_eq_self: it raises every root of X^{q^g} − X to the q-th power.

References

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

@[simp]

theorem TauCeti.frobeniusAlgEquiv_teichmullerLift {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] (a : IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) : (teichmullerLift L) (frobeniusAlgEquiv • a) = (teichmullerLift L) (a ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))

The Teichmüller lifts of the Frobenius action on a and of a ^ q agree, where q is the cardinality of the residue field of the base.

@[simp]

theorem TauCeti.frobeniusAlgEquiv_rootsOfUnity {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] (ζ : ↥(rootsOfUnity (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) - 1) L)) : frobeniusAlgEquiv ↑↑ζ = ↑↑ζ ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

Arithmetic Frobenius raises every (q_L - 1)-st root of unity in an unramified extension to the q_K-th power.

theorem TauCeti.frobeniusAlgEquiv_apply_of_pow_eq_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] {n : ℕ} (hn : IsUnit ↑n) {x : L} (hx : x ^ n = 1) : frobeniusAlgEquiv x = x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

Arithmetic Frobenius on roots of unity of order prime to the residue characteristic. In a finite unramified Galois extension L / K, if x ^ n = 1 for an n invertible in 𝒪[L], then Frob x = x ^ q, where q is the cardinality of the residue field of K.

theorem TauCeti.frobeniusAlgEquiv_apply_of_pow_natCard_pow_eq_self {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] {g : ℕ} (hg : g ≠ 0) {x : L} (hx : x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ g = x) : frobeniusAlgEquiv x = x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

Arithmetic Frobenius on the roots of X^{q^g} − X. In a finite unramified Galois extension L / K, if x ^ (q ^ g) = x for some g ≠ 0, then Frob x = x ^ q, where q is the cardinality of the residue field of K.

@[simp]

theorem TauCeti.frobeniusAlgEquiv_restrictNormal {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] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension K L] [ValuativeExtension L M] [FiniteDimensional K M] [Normal K L] [IsGalois K M] [IsUnramified K M] : frobeniusAlgEquiv.restrictNormal L = frobeniusAlgEquiv

Arithmetic Frobenius restricts to arithmetic Frobenius through a normal intermediate field of a finite unramified extension of nonarchimedean local fields.

@[simp]

theorem TauCeti.frobeniusAlgEquiv_restrictScalars_restrictNormal {K : Type u_4} {L : Type u_5} {K' : Type u_6} {L' : Type u_7} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [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] [Algebra K K'] [ValuativeExtension K K'] [Algebra K' L'] [ValuativeExtension K' L'] [FiniteDimensional K' L'] [IsGalois K' L'] [Algebra K L'] [IsScalarTower K K' L'] [Algebra L L'] [IsScalarTower K L L'] [ValuativeExtension L L'] [IsUnramified K L] [IsUnramified K' L'] : (AlgEquiv.restrictScalars K frobeniusAlgEquiv).restrictNormal L = frobeniusAlgEquiv ^ inertiaDegree K K'

Arithmetic Frobenius under base change. Let L/K and L'/K' be finite unramified extensions with K ⊆ K' and L ⊆ L'. The arithmetic Frobenius of L'/K', restricted to L, is the power of the arithmetic Frobenius of L/K by the residue degree f(K'/K).