Module

AbelianConductorRamification.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.AbelianConductorRamification

4 declarations indexed from sourceView source ↗

Module documentation

Ramification support of abelian narrow finite norm conductors

For a finite abelian extension, the modulus constructed from the actual local norm groups is zero exactly when every chosen finite completion is unramified. Its support therefore gives the exact chosen-completion ramification locus, while the minimal narrow finite conductor has support contained in that locus.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.AbelianNormConductor

Imported by2

theorem

ideleClassNormDefiningModulus_eq_zero_iff_all_chosenFinitePlaces_unramified

L38 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_eq_zero_iff_all_chosenFinitePlaces_unramified

Documentation

The locally constructed norm modulus vanishes exactly when every chosen completed extension is unramified.

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 L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem
    ideleClassNormDefiningModulus_eq_zero_iff_all_chosenFinitePlaces_unramified :
    ideleClassNormDefiningModulus (K := K) (L := L) = 0 ↔
      ∀ v : HeightOneSpectrum (𝓞 K),
        _root_.ChosenFinitePlaceIsUnramified
          (K := K) (L := L) v

theorem

ideleClassNormDefiningModulus_ne_zero_iff_exists_chosenFinitePlace_ramified

L62 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_ne_zero_iff_exists_chosenFinitePlace_ramified

Documentation

The locally constructed norm modulus is nonzero exactly when some chosen completed extension is ramified.

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 L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem
    ideleClassNormDefiningModulus_ne_zero_iff_exists_chosenFinitePlace_ramified :
    ideleClassNormDefiningModulus (K := K) (L := L) ≠ 0 ↔
      ∃ v : HeightOneSpectrum (𝓞 K),
        ¬ _root_.ChosenFinitePlaceIsUnramified
          (K := K) (L := L) v

theorem

mem_ideleClassNorm_narrowFiniteConductor_support_imp_chosenFinitePlace_ramified

L75 ↗

GlobalClassFieldTheory.GlobalClassFields.mem_ideleClassNorm_narrowFiniteConductor_support_imp_chosenFinitePlace_ramified

Documentation

Every prime in the minimal narrow finite norm conductor is ramified in the chosen completed extension above that prime.

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 L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem
    mem_ideleClassNorm_narrowFiniteConductor_support_imp_chosenFinitePlace_ramified
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∈ (ideleClassNormNarrowFiniteConductor
        (K := K) (L := L)).support) :
    ¬ _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v

theorem

ideleClassNorm_narrowFiniteConductor_eq_zero_of_all_chosenFinitePlaces_unramified

L94 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_eq_zero_of_all_chosenFinitePlaces_unramified

Documentation

If every chosen finite completion is unramified, then the minimal narrow finite conductor of the actual idèle-class norm subgroup is zero.

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 L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem
    ideleClassNorm_narrowFiniteConductor_eq_zero_of_all_chosenFinitePlaces_unramified
    (hunramified :
      ∀ v : HeightOneSpectrum (𝓞 K),
        _root_.ChosenFinitePlaceIsUnramified
          (K := K) (L := L) v) :
    ideleClassNormNarrowFiniteConductor (K := K) (L := L) = 0

Module documentation

Ramification support of abelian narrow finite norm conductors

Declarations

ideleClassNormDefiningModulus_eq_zero_iff_all_chosenFinitePlaces_unramified

ideleClassNormDefiningModulus_ne_zero_iff_exists_chosenFinitePlace_ramified

mem_ideleClassNorm_narrowFiniteConductor_support_imp_chosenFinitePlace_ramified

ideleClassNorm_narrowFiniteConductor_eq_zero_of_all_chosenFinitePlaces_unramified