Documentation

TauCeti.NumberTheory.ClassFieldTheory.Local.Unramified

Finite unramified local reciprocity #

For a finite unramified Galois extension L/K, this file normalizes the finite local Artin map by arithmetic Frobenius. The character which sends arithmetic Frobenius to 1 / [L : K] detects the cyclic Galois group. The character formula for the Artin map and the explicit cyclic cup product then identify the Artin symbol of a uniformizer. The norm criterion for unramified extensions extends this calculation to every element: its Artin symbol is the power of Frobenius given by its normalized valuation.

Passing through all finite unramified extensions proves that the unramified coordinate of the absolute local Artin symbol is the image of the normalized valuation in zHat. Consequently, lifts of Artin symbols of units lie in inertia, while lifts of uniformizer symbols are arithmetic Frobenius lifts. Conversely, every element of the image of inertia in G_K^ab is the Artin symbol of a unit. For a uniformizer ϖ, the products of the Artin symbols of the compact group 𝒪[K]ˣ with the image of ℤ̂ under n ↦ Art(ϖ)ⁿ form a compact set containing the dense image of the Artin map, hence all of G_K^ab; the unramified coordinate recovers n from such a product.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.ClassFieldTheory.frobeniusCharacter (K L : Type) [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] :
Additive (Abelianization Gal(L/K)) →+ AddCircle 1

The faithful character of the Galois group of an unramified extension which sends arithmetic Frobenius to 1 / [L : K].

Instances For
    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.frobeniusCharacter_frobenius (K L : Type) [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] :
    (frobeniusCharacter K L) (Additive.ofMul (Abelianization.of frobeniusAlgEquiv)) = ↑(1 / ↑(Module.finrank K L))

    The Frobenius character takes arithmetic Frobenius to 1 / [L : K].

    source
    theorem TauCeti.ClassFieldTheory.injective_frobeniusCharacter (K L : Type) [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.Injective ⇑(frobeniusCharacter K L)

    The Frobenius character detects every element of the abelianized Galois group.

    source
    @[instance_reducible]
    def TauCeti.ClassFieldTheory.concreteGalCommGroup (K L : Type) [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] :
    CommGroup Gal(L/K)

    The commutative group structure on the cyclic Galois group of an unramified extension.

    Instances For

      The normalization #

      source
      theorem TauCeti.ClassFieldTheory.localArtinMap_uniformizer (K L : Type) [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] (ι : L →ₐ[K] SeparableClosure K) {π : Kˣ} (hπ : IsUniformizer K π) :
      (localArtinMap K L ι) (Additive.ofMul π) = Additive.ofMul (Abelianization.of frobeniusAlgEquiv)

      The unramified normalization of finite local reciprocity: the local Artin map sends a uniformizer of K to arithmetic Frobenius in Gal(L/K)ᵃᵇ.

      source
      @[simp]
      theorem TauCeti.ClassFieldTheory.localArtinMap_eq_frobenius_pow_valuation (K L : Type) [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] (ι : L →ₐ[K] SeparableClosure K) (x : Kˣ) :
      (localArtinMap K L ι) (Additive.ofMul x) = Additive.ofMul (Abelianization.of (frobeniusAlgEquiv ^ Multiplicative.toAdd ((normalizedValuation K) x)))

      Finite unramified reciprocity is normalized valuation. For every x : Kˣ, its local Artin symbol in a finite unramified extension is arithmetic Frobenius raised to v_K(x).

      source
      theorem TauCeti.ClassFieldTheory.localArtinMap_unit_of_unramified (K L : Type) [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] (ι : L →ₐ[K] SeparableClosure K) {u : Kˣ} (hu : (ValuativeRel.valuation K) ↑u = 1) :
      (localArtinMap K L ι) (Additive.ofMul u) = 0

      Units have trivial Artin symbol in an unramified extension: the local Artin symbol of a unit of the valuation ring of K vanishes, since its normalized valuation is zero.

      source
      theorem TauCeti.ClassFieldTheory.normResidue_uniformizer (K L : Type) [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] {π : Kˣ} (hπ : IsUniformizer K π) :
      (normResidue K L) ↑π = Abelianization.of frobeniusAlgEquiv

      The unramified normalization of the norm residue isomorphism: it sends the class of a uniformizer of K to arithmetic Frobenius. This is localArtinMap_uniformizer in the multiplicative form of finite local reciprocity.

      The absolute unramified coordinate #

      source
      @[simp]
      theorem TauCeti.ClassFieldTheory.unramifiedCoordinate_artinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) :
      (unramifiedCoordinate K) ((artinMap K) x) = zHat.ofInt ((normalizedValuation K) x)

      The unramified coordinate of the absolute local Artin map is normalized valuation. The coordinate of Art_K(x) is the image of v_K(x) ∈ ℤ in the profinite integers.

      source
      theorem TauCeti.ClassFieldTheory.mem_inertiaSubgroup_of_mk_eq_artinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (u : Kˣ) (hu : (ValuativeRel.valuation K) ↑u = 1) (σ : Field.absoluteGaloisGroup K) (hσ : ↑σ = (artinMap K) u) :
      σ ∈ inertiaSubgroup K

      Every lift of the absolute Artin symbol of a valuation-zero unit lies in inertia.

      source
      theorem TauCeti.ClassFieldTheory.isArithFrobeniusLift_of_mk_eq_artinMap_uniformizer (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {π : Kˣ} (hπ : IsUniformizer K π) (σ : Field.absoluteGaloisGroup K) (hσ : ↑σ = (artinMap K) π) :
      IsArithFrobeniusLift K σ

      Every lift of the absolute Artin symbol of a uniformizer is an arithmetic Frobenius lift.

      source
      theorem TauCeti.ClassFieldTheory.map_artinMap_unitFiltration_zero (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
      Subgroup.map (artinMap K) (unitFiltration K 0) = Subgroup.map (QuotientGroup.mk' (commutator (Field.absoluteGaloisGroup K)).topologicalClosure) (inertiaSubgroup K)

      The units of 𝒪[K] map onto the image of inertia. The Artin symbols of the elements of U(K,0) = 𝒪[K]ˣ are exactly the classes in G_K^ab of the elements of the inertia subgroup, equivalently (ker_unramifiedCoordinate) the classes with trivial unramified coordinate.