Galois automorphisms commute if every automorphism is an involution

Proved

Leopoldt.galois_aut_mul_comm_of_square_eq_one

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

algebranumber-theory

Let $K/\mathbb Q$ be a finite Galois extension. If every Galois automorphism has square equal to the identity, then any two automorphisms commute:

\sigma\tau=\tau\sigma\qquad(\sigma,\tau\in\operatorname{Gal}(K/\mathbb Q)).

This elementary group fact supplies the abelian branch of the exponent-two case split for a totally real Galois field. It applies to the Galois group without requiring an explicit classification of multiquadratic extensions.

Preamble

import Definitions.Def_LeopoldtDefect
import Mathlib.Tactic.Group

open NumberField

Formal statement

namespace Leopoldt
theorem galois_aut_mul_comm_of_square_eq_one
    (K : Type*) [Field K] [NumberField K] [IsGalois ℚ K]
    (h : ∀ σ : K ≃ₐ[ℚ] K, σ * σ = 1)
    (σ τ : K ≃ₐ[ℚ] K) : σ * τ = τ * σ := by sorry
end Leopoldt

Source

Standard elementary group identity: a group of exponent two is abelian; applied to the exponent-two branch of Leopoldt.galois_totallyReal_injection_of_three_le_finrank.

View graph