Commutativity of Galois groups

Mathlib carries abelianness of a Galois extension as the class IsAbelianGalois, and its instance IsAbelianGalois K K' for an intermediate field K' says that every subextension of an abelian extension is again abelian. A construction whose ambient group is the Galois group of a general extension cannot ask for that class, since a bundled commutative structure on Gal(L/K) would be an assumption about L/K; it carries commutativity as a hypothesis ∀ σ τ : Gal(L/K), Commute σ τ instead. This file reads Mathlib's instance in that unbundled form. The same hypothesis supplies the scoped IsMulCommutative instance used by constructions that need Mathlib's bundled commutativity API, and it passes to every field in a tower under L.

Main results

• TauCeti.isMulCommutative_galoisGroup_of_commute
• TauCeti.commute_of_tower

theorem TauCeti.isMulCommutative_galoisGroup_of_commute {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (hab : ∀ (σ τ : Gal(L/K)), Commute σ τ) : IsMulCommutative Gal(L/K)

An explicit proof that a Galois group is commutative supplies Mathlib's bundled IsMulCommutative structure on that group.

theorem TauCeti.commute_of_tower {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [IsGalois K L] {M : Type u_3} [Field M] [Algebra K M] [Algebra M L] [IsScalarTower K M L] (hab : ∀ (σ τ : Gal(L/K)), Commute σ τ) (σ τ : Gal(M/K)) : Commute σ τ

Commutativity of the Galois group passes down a field tower. Every subextension of an abelian extension is abelian, so a proof that Gal(L/K) is commutative is already a proof that Gal(M/K) is for every field M in a tower under L.