Module

GaloisPCompositum.lean

Nyll.SawinTotallyRealTowers.GaloisPCompositum

2 declarations indexed from sourceView source ↗

Module documentation

Galois p-groups in binary composita

Restriction embeds the automorphism group of a compositum of normal subextensions into the product of their automorphism groups. Consequently, p-group automorphism groups are preserved by composita. This applies in particular to finite Galois extensions; neither finiteness nor primality of p is needed for the group-theoretic argument.

Imports6

Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Group.Subgroup.Ker
Mathlib.FieldTheory.Galois.Basic
Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Mathlib.FieldTheory.Normal.Defs
Mathlib.GroupTheory.PGroup

Imported by2

theorem

isPGroup_prod

L28 ↗

ClassFieldTower.Sawin.isPGroup_prod

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v w
namespace ClassFieldTower.Sawin

Lean source · statement

theorem isPGroup_prod
    {p : ℕ} {G : Type u} {H : Type v} [Group G] [Group H]
    (hG : IsPGroup p G) (hH : IsPGroup p H) :
    IsPGroup p (G × H)

theorem

isPGroup_galois_sup

L44 ↗

ClassFieldTower.Sawin.isPGroup_galois_sup

Documentation

The Galois group of a compositum of normal intermediate fields is a p-group when both factors have p-group Galois groups. In particular, this preserves p-group Galois groups of finite Galois extensions.