NYLL
Module

AbsoluteRealProPFactor.lean

Nyll.SawinTotallyRealTowers.AbsoluteRealProPFactor
4 declarations indexed from sourceView source ↗

Module documentation

Factoring representations through the maximal real pro-p compositum

A discrete p-group representation killing finite inertia outside the chosen support and the real Artin value of negative one has an actual finite Galois kernel field satisfying the defining local conditions. Its inclusion in the constructed compositum gives a continuous factorization through restriction. The target need not be finite, and the argument does not require p to be odd.

Imports26
Imported by2

Declarations

instance

kernelLocalizationGalois

L57 ↗
ClassFieldTower.Sawin.kernelLocalizationGalois
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich

-- Keep the algebraic-closure and intermediate-field scalar structures
-- generic until the two local comparisons have been proved.
section KernelLocalization
Lean source · statement
instance kernelLocalizationGalois
    (F : Type) [Field F] [NumberField F]
    {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (s : Field.absoluteGaloisGroup F →ₜ* Q) :
    IsGalois F (absoluteDiscreteKernelField F s)
theorem

discreteKernel_chosenUnramified

L64 ↗
ClassFieldTower.Sawin.discreteKernel_chosenUnramified
Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich

-- Keep the algebraic-closure and intermediate-field scalar structures
-- generic until the two local comparisons have been proved.
section KernelLocalization
private local instance kernelLocalizationGalois
    (F : Type) [Field F] [NumberField F]
    {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (s : Field.absoluteGaloisGroup F →ₜ* Q) :
    IsGalois F (absoluteDiscreteKernelField F s) :=
  absoluteDiscreteKernelField_isGalois F s
Lean source · statement
theorem discreteKernel_chosenUnramified
    (F : Type) [Field F] [NumberField F]
    {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (s : Field.absoluteGaloisGroup F →ₜ* Q) (v : HeightOneSpectrum (𝓞 F))
    (hs : ∀ σ : finitePlaceAbsoluteInertiaSubgroup F v,
      s (finitePlaceAbsoluteDecompositionInclusion F v
        (finitePlaceAbsoluteInertiaInclusion F v σ)) = 1) :
    ChosenFinitePlaceIsUnramified (K := F) (L := absoluteDiscreteKernelField F s) v
theorem

discreteKernel_eq_one_of_fixes

L83 ↗
ClassFieldTower.Sawin.discreteKernel_eq_one_of_fixes
Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich

-- Keep the algebraic-closure and intermediate-field scalar structures
-- generic until the two local comparisons have been proved.
Lean source · statement
theorem discreteKernel_eq_one_of_fixes
    (F : Type) [Field F] [NumberField F]
    {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (s : Field.absoluteGaloisGroup F →ₜ* Q) (σ : Field.absoluteGaloisGroup F)
    (hFix : ∀ x : absoluteDiscreteKernelField F s,
      (absoluteGaloisGroupContinuousMulEquiv F σ) (x : AlgebraicClosure F) = x) :
    s σ = 1
theorem

exists_maximalRealProPOutside_factor_of_inertia_and_infiniteArtin_trivial

L97 ↗
ClassFieldTower.Sawin.exists_maximalRealProPOutside_factor_of_inertia_and_infiniteArtin_trivial
Documentation

Killing the specified finite inertia and real conjugation gives a continuous factor through the actual maximal real pro-p extension.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich

-- Keep the algebraic-closure and intermediate-field scalar structures
-- generic until the two local comparisons have been proved.
Lean source · statement
theorem exists_maximalRealProPOutside_factor_of_inertia_and_infiniteArtin_trivial
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (hP : IsPGroup p Q) (s : Field.absoluteGaloisGroup ℚ →ₜ* Q)
    (hs : ∀ v : HeightOneSpectrum (𝓞 ℚ), v ∉ T →
      ∀ σ : finitePlaceAbsoluteInertiaSubgroup ℚ v,
        s (finitePlaceAbsoluteDecompositionInclusion ℚ v
          (finitePlaceAbsoluteInertiaInclusion ℚ v σ)) = 1)
    (hInfinity : s (absoluteInfinitePlaceArtinNegOne ℚ Rat.infinitePlace) = 1) :
    ∃ t : (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T) →ₜ* Q,
      t.comp (absoluteToMaximalRealProPOutside p T) = s

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