Documentation

TauCeti.NumberTheory.ClassFieldTheory.Local.EulerCharacteristic.Basic

The local Euler characteristic #

For a finite smooth discrete Galois representation A over a nonarchimedean local field, this file defines the three-term local Euler characteristic

χ_F(A) = |H⁰(F, A)| |H²(F, A)| / |H¹(F, A)|.

Over a finite compatible extension F of ℚ_p (TauCeti.FinitePadicExtension) it also defines the normalized absolute value of the order of A,

φ_F(A) = ‖#A‖_F = |#A|_p ^ [F : ℚ_p] = p ^ (-[F : ℚ_p] v_p(#A)),

so that Tate's local Euler characteristic formula reads χ_F = φ_F.

Main results #

source
noncomputable def TauCeti.ClassFieldTheory.localEulerCharacteristic {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : ↑n ≠ 0) (A : GalRep n F) [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod n) A)] :
↥(Units.posSubgroup ℚ)

The three-term local Euler characteristic of a finite smooth discrete Galois representation, as a positive rational number: χ_F(A) = |H⁰(F, A)| |H²(F, A)| / |H¹(F, A)|.

Instances For
    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.localEulerCharacteristic_coe {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : ↑n ≠ 0) (A : GalRep n F) [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod n) A)] :
    ↑↑(localEulerCharacteristic hn A) = ↑(Nat.card ↑(continuousCohomology 0 A).toModuleCat) * ↑(Nat.card ↑(continuousCohomology 2 A).toModuleCat) / ↑(Nat.card ↑(continuousCohomology 1 A).toModuleCat)

    The value of localEulerCharacteristic in ℚ.

    source
    theorem TauCeti.ClassFieldTheory.localEulerCharacteristic_congr {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : ↑n ≠ 0) {A B : GalRep n F} [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod n) A)] (e : A ≅ B) :
    localEulerCharacteristic hn A = localEulerCharacteristic hn B

    Isomorphism invariance of the local Euler characteristic. Isomorphic representations have the same local Euler characteristic; finiteness and smoothness of B follow from those of A along the isomorphism.

    source
    noncomputable def TauCeti.ClassFieldTheory.localCardNorm {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension F p] (A : GalRep n F) [Finite ↑A] :
    ↥(Units.posSubgroup ℚ)

    The normalized absolute value of the order of a finite Galois representation over a finite compatible extension F of ℚ_p, as a positive rational number: φ_F(A) = ‖#A‖_F = |#A|_p ^ [F : ℚ_p] = p ^ (-[F : ℚ_p] v_p(#A)), the right-hand side of Tate's local Euler characteristic formula χ_F(A) = φ_F(A).

    Instances For
      source
      @[simp]
      theorem TauCeti.ClassFieldTheory.localCardNorm_coe {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension F p] (A : GalRep n F) [Finite ↑A] :
      ↑↑(localCardNorm p A) = padicNorm p ↑(Nat.card ↑A) ^ Module.finrank ℚ_[p] F

      The value of localCardNorm in ℚ.

      source
      theorem TauCeti.ClassFieldTheory.localCardNorm_congr {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension F p] {A B : GalRep n F} [Finite ↑A] (e : A ≅ B) :
      localCardNorm p A = localCardNorm p B

      Isomorphism invariance of localCardNorm. Isomorphic representations have the same order, hence the same normalized absolute value of the order.

      source
      theorem TauCeti.ClassFieldTheory.localCardNorm_mul_of_exact {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension F p] {A B C : GalRep n F} [Finite ↑B] (f : A ⟶ B) (g : B ⟶ C) (hf : Function.Injective ⇑(TopRep.Hom.hom f)) (hfg : Function.Exact ⇑(TopRep.Hom.hom f) ⇑(TopRep.Hom.hom g)) (hg : Function.Surjective ⇑(TopRep.Hom.hom g)) :
      localCardNorm p B = localCardNorm p A * localCardNorm p C

      Multiplicativity of localCardNorm. If 0 → A → B → C → 0 is an exact sequence of representations with B finite, then φ_F(B) = φ_F(A) φ_F(C): the order of B is the product of the orders of A and C, and the p-adic norm is multiplicative.