Module

AbsoluteDiscreteRamificationSupport.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.AbsoluteDiscreteRamificationSupport

1 declaration indexed from sourceView source ↗

Module documentation

Finite ramification support of a continuous discrete representation

A continuous map from the absolute Galois group to a discrete group has open kernel. Its finite Galois fixed field is ramified at only finitely many finite places. Actual absolute inertia restricts into finite ideal inertia, so the original map kills inertia outside that finite set. No finiteness hypothesis on the target group is needed. The two added local instances are the fixed field's Galois and number-field proofs.

Imports4

Imported by3

theorem

absoluteDiscreteHom_inertia_support_finite

L38 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteDiscreteHom_inertia_support_finite

Documentation

A continuous discrete representation of the absolute Galois group is ramified at only finitely many of the chosen finite places.

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 RamificationTheory.Field.absoluteGaloisGroup
open AlgebraicNumberTheory.Valuations
variable (F : Type) [Field F] [NumberField F]
variable {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]

Lean source · statement

theorem absoluteDiscreteHom_inertia_support_finite
    (s : Field.absoluteGaloisGroup F →ₜ* Q) :
    {v : HeightOneSpectrum (𝓞 F) |
      ∃ sigma : finitePlaceAbsoluteInertiaSubgroup F v,
        s (finitePlaceAbsoluteDecompositionInclusion F v
          (finitePlaceAbsoluteInertiaInclusion F v sigma)) ≠ 1}.Finite

Module documentation

Finite ramification support of a continuous discrete representation

Declarations

absoluteDiscreteHom_inertia_support_finite