Module

CentralExtensionFrattiniKernel.lean

Nyll.GaloisCohomology.ProP.CentralExtensionFrattiniKernel

4 declarations indexed from sourceView source ↗

Module documentation

Prime central extensions and the Frattini subgroup

A surjection with kernel of prime order can split only if its kernel is not contained in the Frattini subgroup. Applied to the cocycle extension of a nonzero degree-two class, this identifies the coefficient kernel as a cyclic Frattini obstruction.

Imports3

Nyll.GaloisCohomology.ProP.H2CentralExtensionClass
Mathlib.GroupTheory.Frattini
Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Imported by2

theorem

ker_le_frattini_of_no_section_of_prime_card

L35 ↗

ClassFieldTower.ProP.ker_le_frattini_of_no_section_of_prime_card

Documentation

A nonsplit surjection whose kernel has prime cardinality has its entire kernel in the Frattini subgroup of the source.

Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology
universe u v
variable {E : Type u} {Q : Type v} [Group E] [Group Q]
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem ker_le_frattini_of_no_section_of_prime_card
    (f : E →* Q) (hf : Function.Surjective f)
    (hcard : Nat.card f.ker = p)
    (hno : ¬ ∃ s : Q →* E, f.comp s = MonoidHom.id Q) :
    f.ker ≤ frattini E

theorem

degreeTwoCentralExtension_kernel_card

L102 ↗

ClassFieldTower.ProP.degreeTwoCentralExtension_kernel_card

Documentation

The coefficient kernel of the explicit degree-two cocycle extension has cardinality p.

Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology
universe u v
variable {E : Type u} {Q : Type v} [Group E] [Group Q]
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem degreeTwoCentralExtension_kernel_card
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (x : continuousCohomologyZModPLifted p Q 2) :
    Nat.card
      (H2CocycleExtension.projection
        (degreeTwoCocycleRepresentative x)).ker = p

theorem

degreeTwoCentralExtension_kernel_isCyclic

L115 ↗

ClassFieldTower.ProP.degreeTwoCentralExtension_kernel_isCyclic

Documentation

The coefficient kernel of the explicit degree-two cocycle extension is cyclic.

Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology
universe u v
variable {E : Type u} {Q : Type v} [Group E] [Group Q]
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem degreeTwoCentralExtension_kernel_isCyclic
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (x : continuousCohomologyZModPLifted p Q 2) :
    IsCyclic
      (H2CocycleExtension.projection
        (degreeTwoCocycleRepresentative x)).ker

theorem

degreeTwoCentralExtension_kernel_le_frattini_of_ne_zero

L126 ↗

ClassFieldTower.ProP.degreeTwoCentralExtension_kernel_le_frattini_of_ne_zero

Documentation

For a nonzero degree-two class on a discrete group, the cyclic coefficient kernel of its explicit nonsplit extension lies in the Frattini subgroup.

Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.ProP
open ClassFieldTower.Cohomology
universe u v
variable {E : Type u} {Q : Type v} [Group E] [Group Q]
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem degreeTwoCentralExtension_kernel_le_frattini_of_ne_zero
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    [DiscreteTopology Q] [LocallyCompactSpace Q]
    {x : continuousCohomologyZModPLifted p Q 2}
    (hx : x ≠ 0) :
    (H2CocycleExtension.projection
        (degreeTwoCocycleRepresentative x)).ker ≤
      frattini (DegreeTwoCentralExtension x)

Module documentation

Prime central extensions and the Frattini subgroup

Declarations

ker_le_frattini_of_no_section_of_prime_card

degreeTwoCentralExtension_kernel_card

degreeTwoCentralExtension_kernel_isCyclic

degreeTwoCentralExtension_kernel_le_frattini_of_ne_zero