Module

ArithmeticStageH2UnramifiedLocalLift.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2UnramifiedLocalLift

13 declarations indexed from sourceView source ↗

Module documentation

Unramified local solutions of arithmetic-stage central embedding problems

The absolute decomposition group modulo inertia is procyclic and has zero continuous H². Pulling a finite arithmetic-stage cocycle extension back to this quotient therefore supplies a continuous lift to the original extension. Composing with the inertia quotient gives a local solution that kills inertia.

No splitting of the extension over the finite decomposition group is required.

Imports3

Imported by2

def

arithmeticStageFinitePlaceUnramifiedQuotientMap

L36 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageFinitePlaceUnramifiedQuotientMap

Documentation

The local unramified quotient mapped to the finite stage quotient.

Source context 8 commands

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

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

Lean source · statement

def arithmeticStageFinitePlaceUnramifiedQuotientMap
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteDecompositionGroup F v ⧸
        finitePlaceAbsoluteInertiaSubgroup F v →ₜ*
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p)))

def

arithmeticStageFinitePlaceAbsoluteQuotientMap

L49 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageFinitePlaceAbsoluteQuotientMap

Documentation

Absolute finite-place restriction followed by the finite stage quotient.

Source context 8 commands

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

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

Lean source · statement

def arithmeticStageFinitePlaceAbsoluteQuotientMap
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteDecompositionGroup F v →ₜ*
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p)))

theorem

arithmeticStageFinitePlaceUnramifiedQuotientMap_comp

L62 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageFinitePlaceUnramifiedQuotientMap_comp

Documentation

The stage map from the absolute decomposition group factors through inertia.

Source context 8 commands

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

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

Lean source · statement

theorem arithmeticStageFinitePlaceUnramifiedQuotientMap_comp
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    (arithmeticStageFinitePlaceUnramifiedQuotientMap F p U v).comp
        (quotientProjection (finitePlaceAbsoluteInertiaSubgroup F v)) =
      arithmeticStageFinitePlaceAbsoluteQuotientMap F p U v

theorem

arithmeticStageH2_exists_unramifiedLocalLift

L74 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2_exists_unramifiedLocalLift

Documentation

Vanishing of local unramified H² gives a lift of the unramified quotient to every finite stage cocycle extension.

Source context 8 commands

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

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

Lean source · statement

theorem arithmeticStageH2_exists_unramifiedLocalLift
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ∃ s : (finitePlaceAbsoluteDecompositionGroup F v ⧸
        finitePlaceAbsoluteInertiaSubgroup F v) →ₜ*
          ClassFieldTower.ProP.DegreeTwoCentralExtension xU,
      (ClassFieldTower.ProP.H2CocycleExtension.projection
        (ClassFieldTower.ProP.degreeTwoCocycleRepresentative xU)).comp s =
          arithmeticStageFinitePlaceUnramifiedQuotientMap F p U v

def

arithmeticStageH2UnramifiedLocalLift

L101 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2UnramifiedLocalLift

Documentation

A choice of the unramified local lift supplied by local H² = 0.

Source context 8 commands

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

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

Lean source · statement

def arithmeticStageH2UnramifiedLocalLift
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    (finitePlaceAbsoluteDecompositionGroup F v ⧸
      finitePlaceAbsoluteInertiaSubgroup F v) →ₜ*
        ClassFieldTower.ProP.DegreeTwoCentralExtension xU

theorem

arithmeticStageH2UnramifiedLocalLift_projection

L114 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2UnramifiedLocalLift_projection

Documentation

The chosen lift solves the embedding problem on the unramified quotient.

Source context 8 commands

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

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

Lean source · statement

theorem arithmeticStageH2UnramifiedLocalLift_projection
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    (ClassFieldTower.ProP.H2CocycleExtension.projection
        (ClassFieldTower.ProP.degreeTwoCocycleRepresentative xU)).comp
        (arithmeticStageH2UnramifiedLocalLift F p U xU v) =
      arithmeticStageFinitePlaceUnramifiedQuotientMap F p U v

def

arithmeticStageH2AbsoluteLocalLift

L128 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AbsoluteLocalLift

Documentation

The resulting local solution on the absolute decomposition group.

Source context 8 commands

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

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

Lean source · statement

def arithmeticStageH2AbsoluteLocalLift
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteDecompositionGroup F v →ₜ*
      ClassFieldTower.ProP.DegreeTwoCentralExtension xU

theorem

arithmeticStageH2AbsoluteLocalLift_projection

L141 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AbsoluteLocalLift_projection

Documentation

The local solution projects to the prescribed finite stage map.

Source context 8 commands

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

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

Lean source · statement

theorem arithmeticStageH2AbsoluteLocalLift_projection
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    (ClassFieldTower.ProP.H2CocycleExtension.projection
        (ClassFieldTower.ProP.degreeTwoCocycleRepresentative xU)).comp
        (arithmeticStageH2AbsoluteLocalLift F p U xU v) =
      arithmeticStageFinitePlaceAbsoluteQuotientMap F p U v

theorem

arithmeticStageH2AbsoluteLocalLift_inertia

L158 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AbsoluteLocalLift_inertia

Documentation

Every absolute inertia element is killed by the constructed local solution.

Source context 8 commands

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

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

Lean source · statement

theorem arithmeticStageH2AbsoluteLocalLift_inertia
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteInertiaSubgroup F v) :
    arithmeticStageH2AbsoluteLocalLift F p U xU v sigma.1 = 1

theorem

arithmeticStageH2AbsoluteLocalLift_inertia_le_ker

L175 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AbsoluteLocalLift_inertia_le_ker

Documentation

The local solution is unramified: its kernel contains absolute inertia.

Source context 8 commands

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

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

Lean source · statement

theorem arithmeticStageH2AbsoluteLocalLift_inertia_le_ker
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteInertiaSubgroup F v ≤
      (arithmeticStageH2AbsoluteLocalLift F p U xU v).toMonoidHom.ker

def

arithmeticStageFinitePlaceAbsoluteRestriction

L188 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageFinitePlaceAbsoluteRestriction

Documentation

The absolute finite-place stage map in arithmetic Galois coordinates.

Source context 8 commands

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

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

Lean source · statement

def arithmeticStageFinitePlaceAbsoluteRestriction
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteDecompositionGroup F v →ₜ*
      ((openNormalArithmeticStage F p hpOdd U).field ≃ₐ[F]
        (openNormalArithmeticStage F p hpOdd U).field)

theorem

arithmeticStageH2AbsoluteLocalLift_arithmeticProjection

L201 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2AbsoluteLocalLift_arithmeticProjection

Documentation

The local solution also commutes with the arithmetic-stage projection.

Source context 8 commands

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

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

Lean source · statement

theorem arithmeticStageH2AbsoluteLocalLift_arithmeticProjection
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    (arithmeticStageH2Projection F p hpOdd U xU).comp
        (arithmeticStageH2AbsoluteLocalLift F p U xU v) =
      arithmeticStageFinitePlaceAbsoluteRestriction F p hpOdd U v

theorem

arithmeticStageH2_exists_absoluteLocalLift_killsInertia

L220 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2_exists_absoluteLocalLift_killsInertia

Documentation

Every finite arithmetic-stage central embedding problem has an unramified continuous solution at each finite place.

Source context 8 commands

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

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

Lean source · statement

theorem arithmeticStageH2_exists_absoluteLocalLift_killsInertia
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ∃ s : finitePlaceAbsoluteDecompositionGroup F v →ₜ*
        ClassFieldTower.ProP.DegreeTwoCentralExtension xU,
      (arithmeticStageH2Projection F p hpOdd U xU).comp s =
          arithmeticStageFinitePlaceAbsoluteRestriction F p hpOdd U v ∧
        finitePlaceAbsoluteInertiaSubgroup F v ≤ s.toMonoidHom.ker

Module documentation

Unramified local solutions of arithmetic-stage central embedding problems

Declarations