Power classes as reductions of the multiplicative group

The unit calculation used in the local Euler characteristic is phrased in terms of the additive reduction Lˣ / nLˣ, while Kummer theory is phrased in terms of the multiplicative quotient Lˣ / (Lˣ)ⁿ. The two quotients are identified Gal(L/K)-equivariantly by TauCeti.quotSMulTopUnitsPowerClassRepresentationEquiv (built on the group-level TauCeti.quotSMulTopPowerClassEquiv), and this file transports the reduction-class calculation along that identification. It is the bridge through which the power-class Grothendieck-group calculation enters equivariant Kummer theory.

Main results

• TauCeti.exactK0_powerClassRepresentation_of_isUnit and TauCeti.exactK0_powerClassRepresentation_eq_add_finrank_smul: the class of the power-class representation of a finite extension of local fields in G₀(𝔽_ℓ[Gal(L/K)]) is 1 + [μ_ℓ(L)], plus [K : ℚ_p] [𝔽_p[Gal(L/K)]] when ℓ = p.

The class of the power-class representation

theorem TauCeti.exactK0_powerClassRepresentation_of_isUnit (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] [Module.Finite K L] (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hℓ : IsUnit ↑ℓ) : ExactK0.of ↧(powerClassRepresentation ℓ).asModule = 1 + reductionK0 (ZMod ℓ) ((Representation.ofDistribMulAction ℤ Gal(L/K) (Additive Lˣ)).torsionBy ↑ℓ)

The class of Lˣ ⧸ (Lˣ)^ℓ away from the residue characteristic: if ℓ is a unit of 𝒪[L], the power-class representation of Gal(L/K) has class 1 + [μ_ℓ(L)] in G₀(𝔽_ℓ[Gal(L/K)]), where μ_ℓ(L) is the ℓ-torsion of Lˣ.

theorem TauCeti.exactK0_powerClassRepresentation_eq_add_finrank_smul (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] [Module.Finite K L] (ℓ : ℕ) [Fact (Nat.Prime ℓ)] [FinitePadicExtension L ℓ] [FinitePadicExtension K ℓ] [IsGalois K L] : ExactK0.of ↧(powerClassRepresentation ℓ).asModule = 1 + reductionK0 (ZMod ℓ) ((Representation.ofDistribMulAction ℤ Gal(L/K) (Additive Lˣ)).torsionBy ↑ℓ) + Module.finrank ℚ_[ℓ] K • permK0 (ZMod ℓ) Gal(L/K) Gal(L/K)

The class of Lˣ ⧸ (Lˣ)^p at the residue characteristic: for L/K a finite Galois extension of finite extensions of ℚ_p, the power-class representation of Gal(L/K) has class 1 + [μ_p(L)] + [K : ℚ_p] [𝔽_p[Gal(L/K)]] in G₀(𝔽_p[Gal(L/K)]).