NYLL
Module

ArithmeticStageH2EmbeddingProblem.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2EmbeddingProblem
6 declarations indexed from sourceView source ↗

Module documentation

Finite degree-two embedding problems at arithmetic stages

A nonzero degree-two class of the maximal everywhere-unramified pro-p Galois group is detected on a finite quotient. The quotient is transported to the Galois group of its concrete arithmetic stage, carrying the cocycle extension to a finite nonsplit central p-group embedding problem there.

Imports2
Imported by6

Declarations

def

openNormalQuotientContinuousEquivArithmeticStageGalois

L35 ↗
ClassFieldTower.Martinet.Shafarevich.openNormalQuotientContinuousEquivArithmeticStageGalois
Documentation

The quotient--arithmetic-stage equivalence, with its canonical finite topologies recorded.

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
def openNormalQuotientContinuousEquivArithmeticStageGalois
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p)) :
    (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) ≃ₜ*
      ((openNormalArithmeticStage F p hpOdd U).field ≃ₐ[F]
        (openNormalArithmeticStage F p hpOdd U).field)
def

arithmeticStageH2Projection

L49 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2Projection
Documentation

The cocycle-extension projection, transported to the Galois group of the corresponding finite arithmetic stage.

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
def arithmeticStageH2Projection
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2) :
    ProP.DegreeTwoCentralExtension xU →ₜ*
      ((openNormalArithmeticStage F p hpOdd U).field ≃ₐ[F]
        (openNormalArithmeticStage F p hpOdd U).field)
theorem

arithmeticStageH2Projection_surjective

L64 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2Projection_surjective
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_surjective
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2) :
    Function.Surjective (arithmeticStageH2Projection F p hpOdd U xU)
theorem

arithmeticStageH2Projection_kernel_le_center

L77 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2Projection_kernel_le_center
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_center
    (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 ≤
      Subgroup.center (ProP.DegreeTwoCentralExtension xU)
theorem

arithmeticStageH2Projection_no_section

L98 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2Projection_no_section
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_no_section
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    {xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2}
    (hnoSection : ¬ ∃ s :
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
          (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) →ₜ*
        ProP.DegreeTwoCentralExtension xU,
      (ProP.H2CocycleExtension.projection
        (ProP.degreeTwoCocycleRepresentative xU)).comp s =
          ContinuousMonoidHom.id _) :
    ¬ ∃ s : ((openNormalArithmeticStage F p hpOdd U).field ≃ₐ[F]
          (openNormalArithmeticStage F p hpOdd U).field) →ₜ*
        ProP.DegreeTwoCentralExtension xU,
      (arithmeticStageH2Projection F p hpOdd U xU).comp s =
        ContinuousMonoidHom.id _
theorem

exists_arithmeticStage_finite_nonsplit_central_extension_of_degreeTwo_ne_zero

L137 ↗
ClassFieldTower.Martinet.Shafarevich.exists_arithmeticStage_finite_nonsplit_central_extension_of_degreeTwo_ne_zero
Documentation

A nonzero ambient degree-two class produces a finite nonsplit central p-group embedding problem over the Galois group of a finite everywhere- unramified arithmetic stage.

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 exists_arithmeticStage_finite_nonsplit_central_extension_of_degreeTwo_ne_zero
    (hpOdd : Odd p)
    {x : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p) 2}
    (hx : x ≠ 0) :
    ∃ U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p)
        (MaxEverywhereUnramifiedProPGaloisGroup F p),
      ∃ xU : continuousCohomologyZModPLifted p
          (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
            (U.1 : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2,
        continuousCohomologyZModPMapLifted p
            (OpenNormalSubgroupInClass.quotientProj U) 2 xU = x ∧
          Finite (ProP.DegreeTwoCentralExtension xU) ∧
          IsPGroup p (ProP.DegreeTwoCentralExtension xU) ∧
          Function.Surjective
            (arithmeticStageH2Projection F p hpOdd U.1 xU) ∧
          (arithmeticStageH2Projection F p hpOdd U.1 xU).ker ≤
            Subgroup.center (ProP.DegreeTwoCentralExtension xU) ∧
          ¬ ∃ s :
              ((openNormalArithmeticStage F p hpOdd U.1).field ≃ₐ[F]
                (openNormalArithmeticStage F p hpOdd U.1).field) →ₜ*
                ProP.DegreeTwoCentralExtension xU,
            (arithmeticStageH2Projection F p hpOdd U.1 xU).comp s =
              ContinuousMonoidHom.id _

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.