Module

AbelianConductorExactness.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.AbelianConductorExactness

18 declarations indexed from sourceView source ↗

Module documentation

Exact finite ramification loci for abelian norm data

For a finite abelian extension, the modulus constructed from the actual chosen local norm groups has support exactly the ramified finite places. At the archimedean places, the determinant-norm image is the whole local multiplicative group exactly when the extension is unramified at infinity.

The finite statement is deliberately about the locally constructed norm modulus. Identifying it with the minimal narrow finite conductor also requires the compatibility between the actual global norm-residue map and the chosen local Artin map on one-place ideles.

Imports9

Imported by9

theorem

finitePlaceIdeleClass_mem_normRange_of_mem_narrowFiniteHigherUnit

L50 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePlaceIdeleClass_mem_normRange_of_mem_narrowFiniteHigherUnit

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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
    finitePlaceIdeleClass_mem_normRange_of_mem_narrowFiniteHigherUnit
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ)
    (hx :
      x ∈ RayClass.localHigherUnitGroup v
        (ideleClassNormNarrowFiniteConductor
          (K := K) (L := L) v)) :
    IdeleGroup.finitePlaceIdeleClass v x ∈
      (_root_.ideleClassNorm K L).range

theorem

narrowFiniteHigherUnitGroup_le_chosenFinitePlaceLocalNormSubgroup

L75 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteHigherUnitGroup_le_chosenFinitePlaceLocalNormSubgroup

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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
    narrowFiniteHigherUnitGroup_le_chosenFinitePlaceLocalNormSubgroup
    (v : HeightOneSpectrum (𝓞 K)) :
    RayClass.localHigherUnitGroup v
        (ideleClassNormNarrowFiniteConductor
          (K := K) (L := L) v) ≤
      _root_.chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v

theorem

ideleClassNormDefiningModulus_le_narrowFiniteConductor

L109 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_le_narrowFiniteConductor

Documentation

The modulus obtained from the actual chosen local norm groups is bounded by the minimal narrow finite conductor. The substantive input is the finite-place local--global compatibility theorem: a one-place idele class is a global class norm exactly when its local component is a norm from the chosen completion.

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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_le_narrowFiniteConductor :
    ideleClassNormDefiningModulus (K := K) (L := L) ≤
      ideleClassNormNarrowFiniteConductor (K := K) (L := L)

theorem

ideleClassNorm_narrowFiniteConductor_eq_normDefiningModulus

L122 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_eq_normDefiningModulus

Documentation

The minimal narrow finite conductor of an actual finite abelian extension is exactly the modulus obtained from its actual chosen local norm groups.

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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_normDefiningModulus :
    ideleClassNormNarrowFiniteConductor (K := K) (L := L) =
      ideleClassNormDefiningModulus (K := K) (L := L)

theorem

ideleClassNorm_narrowFiniteConductor_apply_eq_chosenLocalConductorExponent

L136 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_apply_eq_chosenLocalConductorExponent

Documentation

At every finite place, the corresponding exponent of the minimal narrow finite conductor is exactly the local conductor exponent of the genuine chosen localized extension. Thus the narrow finite conductor is the finite product of its actual local conductors, encoded pointwise in RayClass.Modulus.

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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_apply_eq_chosenLocalConductorExponent
    (v : HeightOneSpectrum (𝓞 K)) :
    ideleClassNormNarrowFiniteConductor (K := K) (L := L) v =
      ideleClassNormChosenFinitePlaceLocalConductorExponent
        (K := K) (L := L) v

theorem

ideleClassNormDefiningModulus_support_eq_ramifiedBaseFinitePlaces

L160 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_support_eq_ramifiedBaseFinitePlaces

Documentation

For a finite abelian extension, the support of the modulus obtained from the actual chosen local norm subgroups is precisely the set of ramified finite places of the base field.

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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_support_eq_ramifiedBaseFinitePlaces :
    (ideleClassNormDefiningModulus
        (K := K) (L := L)).support =
      _root_.ramifiedBaseFinitePlaces
        (K := K) (L := L)

theorem

ideleClassNormDefiningModulus_eq_zero_iff_ramifiedBaseFinitePlaces_eq_empty

L198 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_eq_zero_iff_ramifiedBaseFinitePlaces_eq_empty

Documentation

The actual local norm modulus vanishes exactly when no finite base place ramifies.

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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_ramifiedBaseFinitePlaces_eq_empty :
    ideleClassNormDefiningModulus (K := K) (L := L) = 0 ↔
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅

theorem

ideleClassNormDefiningModulus_eq_zero_iff_all_finitePlaces_unramified

L209 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormDefiningModulus_eq_zero_iff_all_finitePlaces_unramified

Documentation

The actual local norm modulus vanishes exactly when the extension is unramified at every finite place upstairs.

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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_finitePlaces_unramified :
    ideleClassNormDefiningModulus (K := K) (L := L) = 0 ↔
      ∀ P : HeightOneSpectrum (𝓞 L),
        Algebra.IsUnramifiedAt (𝓞 K) P.asIdeal

theorem

ideleClassNorm_narrowFiniteConductor_support_eq_ramifiedBaseFinitePlaces

L238 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_support_eq_ramifiedBaseFinitePlaces

Documentation

The support of the minimal narrow finite conductor of a finite abelian extension is exactly its finite ramification locus.

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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_support_eq_ramifiedBaseFinitePlaces :
    (ideleClassNormNarrowFiniteConductor
      (K := K) (L := L)).support =
      _root_.ramifiedBaseFinitePlaces
        (K := K) (L := L)

theorem

ideleClassNorm_narrowFiniteConductor_eq_zero_iff_all_finitePlaces_unramified

L250 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_eq_zero_iff_all_finitePlaces_unramified

Documentation

The minimal narrow finite conductor vanishes exactly when the extension is unramified at every finite place upstairs.

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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_iff_all_finitePlaces_unramified :
    ideleClassNormNarrowFiniteConductor (K := K) (L := L) = 0 ↔
      ∀ P : HeightOneSpectrum (𝓞 L),
        Algebra.IsUnramifiedAt (𝓞 K) P.asIdeal

theorem

infiniteTensorNormSubgroup_ne_top_of_isRamified

L262 ↗

GlobalClassFieldTheory.GlobalClassFields.infiniteTensorNormSubgroup_ne_top_of_isRamified

Documentation

A ramified real-to-complex completion makes the corresponding archimedean tensor norm subgroup proper.

Source context 8 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem infiniteTensorNormSubgroup_ne_top_of_isRamified
    (v : InfinitePlace K)
    (w : InfinitePlace L)
    (hw : w.comap (algebraMap K L) = v)
    (hramified : w.IsRamified K) :
    _root_.infiniteTensorNormSubgroup
      (K := K) (L := L) v ≠ ⊤

theorem

infiniteTensorNormSubgroup_eq_top_iff_isUnramifiedIn

L366 ↗

GlobalClassFieldTheory.GlobalClassFields.infiniteTensorNormSubgroup_eq_top_iff_isUnramifiedIn

Documentation

At a base infinite place, the determinant-norm image is the whole local multiplicative group exactly when the extension is unramified above that place.

Source context 8 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem infiniteTensorNormSubgroup_eq_top_iff_isUnramifiedIn
    (v : InfinitePlace K) :
    _root_.infiniteTensorNormSubgroup
          (K := K) (L := L) v = ⊤ ↔
      v.IsUnramifiedIn L

theorem

ideleClassNormFullConductor_infinitePart_eq_realRamificationLocus

L414 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormFullConductor_infinitePart_eq_realRamificationLocus

Documentation

The infinite part of the full conductor of an idèle-class norm range is exactly the set of ramified real places.

Source context 8 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
open scoped Classical in

Lean source · full declaration

theorem ideleClassNormFullConductor_infinitePart_eq_realRamificationLocus :
    (ideleClassNormConductorialSubgroup
        (K := K) (L := L)).fullConductor.infinitePart =
      (Finset.univ.filter fun v : RayClass.RealPlace K =>
        ¬ v.1.IsUnramifiedIn L) := by
  classical
  ext v
  change
    v ∈ (ideleClassNormConductorialSubgroup
        (K := K) (L := L)).fullConductorInfinitePart ↔
      v ∈ (Finset.univ.filter fun w : RayClass.RealPlace K =>
        ¬ w.1.IsUnramifiedIn L)
  rw [ConductorialSubgroup.mem_fullConductorInfinitePart_iff,
    Finset.mem_filter]
  simp only [Finset.mem_univ, true_and]
  change
    (¬ (IdeleGroup.infinitePlaceIdeleClass v.1).range ≤
        (_root_.ideleClassNorm K L).range) ↔
      ¬ v.1.IsUnramifiedIn L
  apply not_congr
  calc
    (IdeleGroup.infinitePlaceIdeleClass v.1).range ≤
          (_root_.ideleClassNorm K L).range ↔
        _root_.infiniteTensorNormSubgroup
            (K := K) (L := L) v.1 = ⊤ := by
      constructor
      · intro hRange
        apply top_unique
        intro x _hx
        apply
          (Reciprocity.infinitePlaceIdeleClass_mem_ideleClassNorm_range_iff
            (K := K) (L := L) v.1 x).1
        exact hRange ⟨x, rfl⟩
      · intro hTop
        rintro _ ⟨x, rfl⟩
        apply
          (Reciprocity.infinitePlaceIdeleClass_mem_ideleClassNorm_range_iff
            (K := K) (L := L) v.1 x).2
        rw [hTop]
        exact Subgroup.mem_top x
    _ ↔ v.1.IsUnramifiedIn L :=
      infiniteTensorNormSubgroup_eq_top_iff_isUnramifiedIn
        (K := K) (L := L) v.1

theorem

infiniteTensorNormSubgroups_eq_top_iff_isUnramifiedAtInfinitePlaces

L462 ↗

GlobalClassFieldTheory.GlobalClassFields.infiniteTensorNormSubgroups_eq_top_iff_isUnramifiedAtInfinitePlaces

Documentation

A finite abelian number-field extension is unramified at every infinite place exactly when every archimedean tensor determinant-norm image is the whole local multiplicative group.

Source context 8 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem
    infiniteTensorNormSubgroups_eq_top_iff_isUnramifiedAtInfinitePlaces :
    (∀ v : InfinitePlace K,
        _root_.infiniteTensorNormSubgroup
          (K := K) (L := L) v = ⊤) ↔
      IsUnramifiedAtInfinitePlaces K L

theorem

ideleClassNorm_everywhereUnramified_iff_conductor_zero_and_infiniteNorms_top

L491 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_everywhereUnramified_iff_conductor_zero_and_infiniteNorms_top

Documentation

In the repository's modulus convention, the finite conductor is zero and every archimedean determinant-norm image is the full local group exactly when the extension is unramified at every finite and infinite place.

This combines the finite support of the narrow finite conductor with the separate archimedean clause, so no ramification place is omitted by the fact that RayClass.Modulus records only finite exponents.

Source context 7 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open LocalClassFieldTheory LocalFieldTheory
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_everywhereUnramified_iff_conductor_zero_and_infiniteNorms_top :
    ((∀ P : HeightOneSpectrum (𝓞 L),
          Algebra.IsUnramifiedAt (𝓞 K) P.asIdeal) ∧
        IsUnramifiedAtInfinitePlaces K L) ↔
      (ideleClassNormNarrowFiniteConductor
            (K := K) (L := L) = 0 ∧
        ∀ v : InfinitePlace K,
          _root_.infiniteTensorNormSubgroup
            (K := K) (L := L) v = ⊤)

theorem

abelianFullConductor_finiteExponent_eq_localConductorExponent

L523 ↗

ClassFieldTheory.abelianFullConductor_finiteExponent_eq_localConductorExponent

Documentation

The finite exponent of the full norm conductor is the local conductor exponent at the chosen completion above the place.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
open _root_.GlobalClassFieldTheory.GlobalClassFields (
  ideleClassNorm_narrowFiniteConductor_apply_eq_chosenLocalConductorExponent
) in

Lean source · statement

theorem abelianFullConductor_finiteExponent_eq_localConductorExponent
    (v : HeightOneSpectrum (𝓞 K)) :
    (GlobalClassFieldTheory.GlobalClassFields.ideleClassNormConductorialSubgroup
        (K := K) (L := L)).fullConductor.finitePart v =
      GlobalClassFieldTheory.GlobalClassFields.ideleClassNormChosenFinitePlaceLocalConductorExponent
        (K := K) (L := L) v

theorem

abelianFullConductor_finiteExponent_eq_zero_iff_unramified

L542 ↗

ClassFieldTheory.abelianFullConductor_finiteExponent_eq_zero_iff_unramified

Documentation

A finite place has conductor exponent zero precisely when the chosen local extension is unramified.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
open _root_.GlobalClassFieldTheory.GlobalClassFields (
  ideleClassNormLocalHigherUnitExponent_eq_localConductorExponent
  ideleClassNormLocalHigherUnitExponent_eq_zero_iff_chosenFinitePlaceIsUnramified
) in

Lean source · statement

theorem abelianFullConductor_finiteExponent_eq_zero_iff_unramified
    (v : HeightOneSpectrum (𝓞 K)) :
    (GlobalClassFieldTheory.GlobalClassFields.ideleClassNormConductorialSubgroup
        (K := K) (L := L)).fullConductor.finitePart v = 0 ↔
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v

theorem

abelianFullConductor_mem_infinitePart_iff_realRamified

L560 ↗

ClassFieldTheory.abelianFullConductor_mem_infinitePart_iff_realRamified

Documentation

A real place belongs to the full norm conductor exactly when it ramifies, equivalently complexifies, in the extension.

Source context 6 commands

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

open scoped NumberField NumberField.LiesOver
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
open _root_.GlobalClassFieldTheory.GlobalClassFields (
  ideleClassNormFullConductor_infinitePart_eq_realRamificationLocus
) in

Lean source · statement

theorem abelianFullConductor_mem_infinitePart_iff_realRamified
    (v : RayClass.RealPlace K) :
    v ∈
        (GlobalClassFieldTheory.GlobalClassFields.ideleClassNormConductorialSubgroup
          (K := K) (L := L)).fullConductor.infinitePart ↔
      ¬ v.1.IsUnramifiedIn L

Module documentation

Exact finite ramification loci for abelian norm data

Declarations