Module

AbsoluteInertiaUnramifiedFactor.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.AbsoluteInertiaUnramifiedFactor

1 declaration indexed from sourceView source ↗

Module documentation

Inertia-trivial discrete p-representations factor through the maximal tower

The actual open-kernel fixed field is finite Galois with p-group Galois group. Pointwise absolute inertia triviality makes it unramified at finite primes; odd p makes its infinite primes unramified. Its inclusion in the maximal everywhere-unramified pro-p field then gives the continuous quotient factor.

The target need not itself be finite: discreteness already makes the actual kernel open. Only the fixed field's Galois and number-field proof instances are installed, with all field algebra structures inherited canonically.

Imports4

Imported by2

theorem

exists_maxEverywhereUnramifiedProP_factor_of_inertia_trivial

L37 ↗

ClassFieldTower.Martinet.Shafarevich.exists_maxEverywhereUnramifiedProP_factor_of_inertia_trivial

Documentation

A continuous discrete p-representation killing every selected absolute finite-place inertia has an actual continuous maximal-unramified factor.

Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]

Lean source · statement

theorem exists_maxEverywhereUnramifiedProP_factor_of_inertia_trivial
    (hpOdd : Odd p) (hP : IsPGroup p Q)
    (s : Field.absoluteGaloisGroup F →ₜ* Q)
    (hs : ∀ v : HeightOneSpectrum (𝓞 F),
      ∀ sigma : finitePlaceAbsoluteInertiaSubgroup F v,
        s (finitePlaceAbsoluteDecompositionInclusion F v
          (finitePlaceAbsoluteInertiaInclusion F v sigma)) = 1) :
    ∃ t : MaxEverywhereUnramifiedProPGaloisGroup F p →ₜ* Q,
      t.comp (absoluteToMaxEverywhereUnramifiedProP F p) = s

Module documentation

Inertia-trivial discrete p-representations factor through the maximal tower

Declarations

exists_maxEverywhereUnramifiedProP_factor_of_inertia_trivial