Module

ConductorSupport.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorSupport

5 declarations indexed from sourceView source ↗

Module documentation

Support of the narrow finite conductor

There are two source statements in the ramification criterion:

a prime belongs to the support of the narrow finite conductor exactly

when its one-place finite local conductor exponent is nonzero;

a finite abelian local extension is ramified exactly when its concrete

local conductor exponent is nonzero.

The local conductor criterion itself is public in LocalClassFieldTheory.Finite.UnramifiedConductor. The global reciprocity identity N(C_L) ∩ K_vˣ = N(L_vˣ) identifies the two exponents for a global extension, yielding the global conductor-support corollary.

Imports7

Imported by2

theorem

mem_narrowFiniteConductor_support_iff_narrowFiniteLocalConductorExponent_ne_zero

L49 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.mem_narrowFiniteConductor_support_iff_narrowFiniteLocalConductorExponent_ne_zero

Documentation

A finite prime divides the narrow finite conductor exactly when its finite local conductor exponent is nonzero.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable {K : Type} [Field K] [NumberField K]
namespace ConductorialSubgroup

Lean source · statement

theorem mem_narrowFiniteConductor_support_iff_narrowFiniteLocalConductorExponent_ne_zero
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    v ∈ H.narrowFiniteConductor.support ↔
      H.narrowFiniteLocalConductorExponent v ≠ 0

theorem

mem_narrowFiniteConductor_support_iff_not_localHigherUnitClassSubgroup_zero_le

L59 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.mem_narrowFiniteConductor_support_iff_not_localHigherUnitClassSubgroup_zero_le

Documentation

A finite prime divides the narrow finite conductor exactly when its full integral-unit class subgroup is not contained in the defining subgroup.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable {K : Type} [Field K] [NumberField K]
namespace ConductorialSubgroup

Lean source · statement

theorem
    mem_narrowFiniteConductor_support_iff_not_localHigherUnitClassSubgroup_zero_le
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    v ∈ H.narrowFiniteConductor.support ↔
      ¬ RayClass.localHigherUnitClassSubgroup v 0 ≤ H.1

theorem

localHigherUnitClassSubgroup_zero_le_ideleClassNorm_range_of_chosenUnramified

L74 ↗

GlobalClassFieldTheory.GlobalClassFields.localHigherUnitClassSubgroup_zero_le_ideleClassNorm_range_of_chosenUnramified

Documentation

At an unramified chosen completion, the zeroth local higher-unit class subgroup consists of global idele-class norms.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem localHigherUnitClassSubgroup_zero_le_ideleClassNorm_range_of_chosenUnramified
    {L : Type}
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    RayClass.localHigherUnitClassSubgroup v 0 ≤
      (_root_.ideleClassNorm K L).range

theorem

localHigherUnitClassSubgroup_zero_le_ideleClassNorm_range_of_isUnramifiedAt

L96 ↗

GlobalClassFieldTheory.GlobalClassFields.localHigherUnitClassSubgroup_zero_le_ideleClassNorm_range_of_isUnramifiedAt

Documentation

Algebraic unramifiedness at a finite prime forces the zeroth local higher-unit class subgroup into the global norm subgroup.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem localHigherUnitClassSubgroup_zero_le_ideleClassNorm_range_of_isUnramifiedAt
    {L : Type}
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      Algebra.IsUnramifiedAt (𝓞 K)
        (_root_.finitePlaceExtensionCentre
          (K := K) (L := L) v
          (_root_.chosenFinitePlaceExtension (L := L) v)).asIdeal) :
    RayClass.localHigherUnitClassSubgroup v 0 ≤
      (_root_.ideleClassNorm K L).range

theorem

finitePlaceIdeleClass_range_le_ideleClassNorm_range_of_splitsCompletely

L115 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePlaceIdeleClass_range_le_ideleClassNorm_range_of_splitsCompletely

Documentation

Complete splitting at a finite prime puts the whole one-place idele class image inside the global norm subgroup.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem finitePlaceIdeleClass_range_le_ideleClassNorm_range_of_splitsCompletely
    {L : Type}
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    (IdeleGroup.finitePlaceIdeleClass v).range ≤
      (_root_.ideleClassNorm K L).range

Module documentation

Support of the narrow finite conductor

Declarations

mem_narrowFiniteConductor_support_iff_narrowFiniteLocalConductorExponent_ne_zero

mem_narrowFiniteConductor_support_iff_not_localHigherUnitClassSubgroup_zero_le

localHigherUnitClassSubgroup_zero_le_ideleClassNorm_range_of_chosenUnramified

localHigherUnitClassSubgroup_zero_le_ideleClassNorm_range_of_isUnramifiedAt

finitePlaceIdeleClass_range_le_ideleClassNorm_range_of_splitsCompletely