NYLL
Module

RealProTwoH2AbsoluteKernel.lean

Nyll.SawinTotallyRealTowers.RealProTwoH2AbsoluteKernel
3 declarations indexed from sourceView source ↗

Module documentation

Descending absolute degree-two vanishing to the actual real pro-two group

An actual absolute cocycle lift is corrected at its finite ramification support and at real conjugation. Its kernel field is an admissible finite real two-extension, so the corrected lift factors through the constructed maximal real pro-two compositum. Thus vanishing after absolute inflation already implies vanishing after inflation into this maximal group.

Imports20
Imported by2

Declarations

theorem

exists_maximalRealProTwo_cocycle_lift_of_absolute_lift

L50 ↗
ClassFieldTower.Sawin.exists_maximalRealProTwo_cocycle_lift_of_absolute_lift
Documentation

Every absolute solution of a finite two-group cocycle embedding problem comes from an actual solution on the maximal real pro-two group.

Source context 6 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Cohomology ClassFieldTower.ProP
open ClassFieldTower.Martinet.Shafarevich
Lean source · statement
theorem exists_maximalRealProTwo_cocycle_lift_of_absolute_lift
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (hThree : (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
      (⟨3, Nat.prime_three⟩ : Nat.Primes) ∈ T)
    {Q : Type} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q] [Finite Q]
    (hQ : IsPGroup 2 Q)
    (q : (maximalRealProPOutside 2 T ≃ₐ[ℚ] maximalRealProPOutside 2 T) →ₜ* Q)
    (z : trivialZModPCocyclesLifted 2 Q 2)
    (s : Field.absoluteGaloisGroup ℚ →ₜ* H2CocycleExtension z)
    (hs : (H2CocycleExtension.projection z).comp s =
      q.comp (absoluteToMaximalRealProPOutside 2 T)) :
    ∃ t : (maximalRealProPOutside 2 T ≃ₐ[ℚ] maximalRealProPOutside 2 T) →ₜ*
        H2CocycleExtension z,
      (H2CocycleExtension.projection z).comp t = q
theorem

maximalRealProTwo_H2_eq_zero_of_absolute_inflation_eq_zero

L89 ↗
ClassFieldTower.Sawin.maximalRealProTwo_H2_eq_zero_of_absolute_inflation_eq_zero
Documentation

At every actual finite two-group stage, the kernel of absolute inflation is contained in the kernel of inflation to the maximal real pro-two group.

Source context 6 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Cohomology ClassFieldTower.ProP
open ClassFieldTower.Martinet.Shafarevich
Lean source · statement
theorem maximalRealProTwo_H2_eq_zero_of_absolute_inflation_eq_zero
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (hThree : (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
      (⟨3, Nat.prime_three⟩ : Nat.Primes) ∈ T)
    {Q : Type} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q] [Finite Q]
    (hQ : IsPGroup 2 Q)
    (q : (maximalRealProPOutside 2 T ≃ₐ[ℚ] maximalRealProPOutside 2 T) →ₜ* Q)
    (x : continuousCohomologyZModPLifted 2 Q 2)
    (hx : (continuousCohomologyZModPMapLifted 2
      (q.comp (absoluteToMaximalRealProPOutside 2 T)) 2).hom x = 0) :
    (continuousCohomologyZModPMapLifted 2 q 2).hom x = 0
theorem

finiteKummerContinuousH2Map_ker_le_realProPStageInflation_ker

L113 ↗
ClassFieldTower.Sawin.finiteKummerContinuousH2Map_ker_le_realProPStageInflation_ker
Documentation

The finite Kummer kernel dies under actual inflation from every constructed arithmetic stage to the maximal real pro-two group.

Source context 6 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Cohomology ClassFieldTower.ProP
open ClassFieldTower.Martinet.Shafarevich
Lean source · statement
theorem finiteKummerContinuousH2Map_ker_le_realProPStageInflation_ker
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (hThree : (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
      (⟨3, Nat.prime_three⟩ : Nat.Primes) ∈ T)
    (U : OpenNormalSubgroup
      (maximalRealProPOutside 2 T ≃ₐ[ℚ] maximalRealProPOutside 2 T))
    (hmu : (primitiveRoots 2 ℚ).Nonempty) :
    (finiteKummerContinuousH2Map ℚ (2 : ℕ+) (realProPOpenNormalStage 2 T U).val hmu).ker ≤
      (continuousCohomologyZModPMapLifted 2
        (realProPOpenNormalStageRestriction 2 T U) 2).hom.toLinearMap.toAddMonoidHom.ker

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