Module

PGroupGaloisTower.lean

Nyll.GaloisCohomology.GroupTheory.PGroupGaloisTower

1 declaration indexed from sourceView source ↗

Module documentation

A central prime-degree step in a finite Galois p-extension

A nontrivial finite p-group has a central subgroup of order p. Its fixed field gives a smaller Galois p-extension of the base, with a cyclic prime-degree extension on top. This constructs the intermediate field needed for induction without imposing any cohomological hypotheses.

Imports8

Mathlib.Algebra.Order.GroupWithZero.Basic
Mathlib.FieldTheory.Galois.Basic
Mathlib.GroupTheory.PGroup
Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Mathlib.GroupTheory.Subgroup.Center
Mathlib.GroupTheory.Sylow
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.LinearAlgebra.Dimension.Free

Imported by3

theorem

exists_intermediateField_prime_degree_of_isPGroup

L31 ↗

IsGalois.exists_intermediateField_prime_degree_of_isPGroup

Documentation

A nontrivial finite Galois p-extension has a smaller Galois p-subextension with central, cyclic, prime-degree top extension.

Source context 2 commands

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

open Module
namespace IsGalois

Lean source · statement

theorem exists_intermediateField_prime_degree_of_isPGroup
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (p : ℕ) [Fact p.Prime] [Nontrivial Gal(L/K)]
    (hP : IsPGroup p Gal(L/K)) :
    ∃ E : IntermediateField K L,
      IsGalois K E ∧ IsGalois E L ∧ IsPGroup p Gal(E/K) ∧
      IsCyclic Gal(L/E) ∧ finrank E L = p ∧
      finrank K E < finrank K L ∧
      E.fixingSubgroup ≤ Subgroup.center Gal(L/K)

Module documentation

A central prime-degree step in a finite Galois p-extension

Declarations

exists_intermediateField_prime_degree_of_isPGroup