Module

RealCentralLiftCorrection.lean

Nyll.SawinTotallyRealTowers.RealCentralLiftCorrection

4 declarations indexed from sourceView source ↗

Module documentation

Removing unwanted inertia and real conjugation from cocycle lifts

Local unramified degree-two vanishing constructs the reference lifts. The actual absolute lift has finite ramification support; its differences from these reference lifts are genuine local characters. Prime three absorbs the rational radical obstruction, and a global character corrects all outside inertia and the real value without changing the projected homomorphism.

Imports15

Imported by2

instance

realCentralLiftCanonicalZModAddCommGroup

L43 ↗

ClassFieldTower.Sawin.realCentralLiftCanonicalZModAddCommGroup

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 ProCGroups

Lean source · statement

instance realCentralLiftCanonicalZModAddCommGroup : AddCommGroup (ZMod 2)

theorem

exists_inertia_trivial_local_cocycle_lift

L48 ↗

ClassFieldTower.Sawin.exists_inertia_trivial_local_cocycle_lift

Documentation

The actual unramified local quotient supplies an inertia-trivial solution of every cocycle embedding problem whose base map kills inertia.

Source context 7 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 ProCGroups
local instance realCentralLiftCanonicalZModAddCommGroup : AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup

Lean source · statement

theorem exists_inertia_trivial_local_cocycle_lift
    (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
    {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (v : HeightOneSpectrum (𝓞 F))
    (q : finitePlaceAbsoluteDecompositionGroup F v →ₜ* Q)
    (hI : finitePlaceAbsoluteInertiaSubgroup F v ≤ q.toMonoidHom.ker)
    (z : trivialZModPCocyclesLifted p Q 2) :
    ∃ t : finitePlaceAbsoluteDecompositionGroup F v →ₜ* H2CocycleExtension z,
      (H2CocycleExtension.projection z).comp t = q ∧
      finitePlaceAbsoluteInertiaSubgroup F v ≤ t.toMonoidHom.ker

theorem

twist_eq_one_at

L80 ↗

ClassFieldTower.Sawin.twist_eq_one_at

Source context 7 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 ProCGroups
local instance realCentralLiftCanonicalZModAddCommGroup : AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup

Lean source · statement

theorem twist_eq_one_at
    {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (z : trivialZModPCocyclesLifted 2 Q 2)
    (s : Field.absoluteGaloisGroup ℚ →ₜ* H2CocycleExtension z)
    (γ : Field.absoluteGaloisGroup ℚ →ₜ* Multiplicative (ZMod 2))
    (σ : Field.absoluteGaloisGroup ℚ)
    (hs : H2CocycleExtension.projection z (s σ) = 1)
    (hγ : γ σ = Multiplicative.ofAdd (s σ).left.down) :
    H2CocycleExtension.twistByCharacter z s γ σ = 1

theorem

exists_character_corrected_absolute_cocycle_lift

L98 ↗

ClassFieldTower.Sawin.exists_character_corrected_absolute_cocycle_lift

Documentation

Finite ramification of an actual absolute lift permits a global character correction killing all prescribed outside inertia and real conjugation.

Source context 7 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 ProCGroups
local instance realCentralLiftCanonicalZModAddCommGroup : AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup

Lean source · statement

theorem exists_character_corrected_absolute_cocycle_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]
    (q : Field.absoluteGaloisGroup ℚ →ₜ* Q)
    (z : trivialZModPCocyclesLifted 2 Q 2)
    (s : Field.absoluteGaloisGroup ℚ →ₜ* H2CocycleExtension z)
    (hs : (H2CocycleExtension.projection z).comp s = q)
    (hInertia : ∀ (v : HeightOneSpectrum (𝓞 ℚ)), v ∉ T →
      ∀ σ : finitePlaceAbsoluteInertiaSubgroup ℚ v,
        q (finitePlaceAbsoluteDecompositionInclusion ℚ v σ.1) = 1)
    (hReal : q (absoluteInfinitePlaceArtinNegOne ℚ Rat.infinitePlace) = 1) :
    ∃ γ : Field.absoluteGaloisGroup ℚ →ₜ* Multiplicative (ZMod 2),
      (∀ (v : HeightOneSpectrum (𝓞 ℚ)), v ∉ T →
        ∀ σ : finitePlaceAbsoluteInertiaSubgroup ℚ v,
          H2CocycleExtension.twistByCharacter z s γ
            (finitePlaceAbsoluteDecompositionInclusion ℚ v σ.1) = 1) ∧
      H2CocycleExtension.twistByCharacter z s γ
        (absoluteInfinitePlaceArtinNegOne ℚ Rat.infinitePlace) = 1

Module documentation

Removing unwanted inertia and real conjugation from cocycle lifts

Declarations

realCentralLiftCanonicalZModAddCommGroup

exists_inertia_trivial_local_cocycle_lift

twist_eq_one_at

exists_character_corrected_absolute_cocycle_lift