Module

ArithmeticStageH2FrattiniKernel.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2FrattiniKernel

4 declarations indexed from sourceView source ↗

Module documentation

The Frattini kernel of the arithmetic degree-two embedding problem

Transporting the explicit cocycle-extension projection to its finite everywhere-unramified arithmetic stage does not change its kernel. A nonzero stage class therefore has a cyclic kernel of order p contained in the Frattini subgroup of the extension group.

Imports2

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.All

theorem

arithmeticStageH2Projection_ker

L35 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2Projection_ker

Documentation

Transport to the arithmetic-stage Galois group leaves the cocycle extension kernel unchanged.

Source context 8 commands

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

open scoped NumberField Topology
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem arithmeticStageH2Projection_ker
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2) :
    (arithmeticStageH2Projection F p hpOdd U xU).ker =
      (ProP.H2CocycleExtension.projection
        (ProP.degreeTwoCocycleRepresentative xU)).ker

theorem

arithmeticStageH2Projection_kernel_card

L58 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2Projection_kernel_card

Documentation

The arithmetic embedding-problem kernel has cardinality p.

Source context 8 commands

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

open scoped NumberField Topology
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem arithmeticStageH2Projection_kernel_card
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2) :
    Nat.card (arithmeticStageH2Projection F p hpOdd U xU).ker = p

theorem

arithmeticStageH2Projection_kernel_isCyclic

L70 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2Projection_kernel_isCyclic

Documentation

The arithmetic embedding-problem kernel is cyclic.

Source context 8 commands

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

open scoped NumberField Topology
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem arithmeticStageH2Projection_kernel_isCyclic
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2) :
    IsCyclic (arithmeticStageH2Projection F p hpOdd U xU).ker

theorem

arithmeticStageH2Projection_kernel_le_frattini_of_ne_zero

L82 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2Projection_kernel_le_frattini_of_ne_zero

Documentation

For a nonzero stage class, the cyclic kernel is a Frattini kernel.

Source context 8 commands

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

open scoped NumberField Topology
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet
open ProCGroups ProCGroups.ProC
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem arithmeticStageH2Projection_kernel_le_frattini_of_ne_zero
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    {xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2}
    (hxU : xU ≠ 0) :
    (arithmeticStageH2Projection F p hpOdd U xU).ker ≤
      frattini (ProP.DegreeTwoCentralExtension xU)

Module documentation

The Frattini kernel of the arithmetic degree-two embedding problem

Declarations

arithmeticStageH2Projection_ker

arithmeticStageH2Projection_kernel_card

arithmeticStageH2Projection_kernel_isCyclic

arithmeticStageH2Projection_kernel_le_frattini_of_ne_zero