ModuleMaximalAbelianSubextension.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.MaximalAbelianSubextension
6 declarations indexed from sourceView source ↗ Module documentation
Maximal abelian subextensions inside finite normal closures
For a finite extension L / K, its chosen finite normal closure contains a distinguished copy of L. The subgroup fixing that copy, together with the commutator subgroup of the full Galois group, cuts out the largest abelian Galois intermediate field contained in the distinguished copy.
Declarations
DocumentationThe subgroup of the finite-normal-closure Galois group fixing the distinguished copy of the original extension.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped IsMulCommutative
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
The relative Galois group over the distinguished original field is the corresponding fixing subgroup of the full normal-closure Galois group.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped IsMulCommutative
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
The largest abelian Galois intermediate field of the finite normal closure that is contained in the distinguished copy of the original field.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped IsMulCommutative
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
The maximal abelian subfield is contained in the distinguished copy of the original extension.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped IsMulCommutative
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
The maximal abelian subfield is abelian Galois over the base field.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped IsMulCommutative
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
Every abelian Galois intermediate field contained in the distinguished original field is contained in the maximal abelian subfield.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped IsMulCommutative
universe u v
variable
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]