Module

AbelianConductorFiniteUnramified.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.AbelianConductorFiniteUnramified

1 declaration indexed from sourceView source ↗

Module documentation

Zero finite exponent and unramifiedness

Imports4

Imported by2

theorem

finiteExponent_eq_zero_iff_unramified

L25 ↗

ClassFieldTheory.IsAbelianConductor.finiteExponent_eq_zero_iff_unramified

Documentation

A finite place has exponent zero in the public conductor exactly when every place above it is unramified.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem IsAbelianConductor.finiteExponent_eq_zero_iff_unramified
    {K : Type} [Field K] [NumberField K]
    {L : Type} [Field L] [NumberField L]
    [Algebra K L] [IsAbelianGalois K L]
    {c : RayClassModulus K}
    (hc : IsAbelianConductor K L c)
    (v : HeightOneSpectrum (𝓞 K)) :
    c.finitePart v = 0 ↔
      ∀ W : HeightOneSpectrum (𝓞 L),
        W.asIdeal.LiesOver v.asIdeal →
          Algebra.IsUnramifiedAt (𝓞 K) W.asIdeal

Module documentation

Zero finite exponent and unramifiedness

Declarations

finiteExponent_eq_zero_iff_unramified