Commuting semilocal actions of an exponent-two Galois group

Proved

Leopoldt.semilocalGaloisAut_comm_of_exponent_two

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryp-adicunits

Let $K/\mathbb Q$ be Galois with all automorphisms of order at most two, and let $p$ be prime. The semilocal actions of any two automorphisms commute:

\rho_p(\sigma)\rho_p(\tau)=\rho_p(\tau)\rho_p(\sigma).

Together with the involution property, these commuting operators are the algebraic starting point for the simultaneous sign-eigenspace decomposition of semilocal units in the multiquadratic case.

Preamble

import Definitions.Def_LeopoldtGaloisAction

open NumberField

Formal statement

namespace Leopoldt
theorem semilocalGaloisAut_comm_of_exponent_two (p : ℕ) [Fact p.Prime]
    (K : Type*) [Field K] [NumberField K] [IsGalois ℚ K]
    (h : ∀ ρ : K ≃ₐ[ℚ] K, ρ * ρ = 1) (σ τ : K ≃ₐ[ℚ] K) :
    semilocalGaloisAut p K σ * semilocalGaloisAut p K τ =
      semilocalGaloisAut p K τ * semilocalGaloisAut p K σ := by sorry
end Leopoldt

Source

Functoriality of the semilocal Galois action and the elementary theorem that groups of exponent two are abelian; relevant to the multiquadratic branch of Leopoldt.galois_totallyReal_injection_of_three_le_finrank.

View graph