NYLL
Module

ConductorLocalComparison.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorLocalComparison
11 declarations indexed from sourceView source ↗

Module documentation

Narrow finite and local conductor exponents

The narrow finite conductor is the finite component of the conductor in the all-real-positive convention. We formulate its local condition directly inside the idele class group: insert a higher unit at one finite place and 1 at every other place, then pass to the idele class group.

The proof is constructive. One inequality follows by restricting any global defining modulus to one place. For the reverse inequality, replace one exponent of a fixed defining modulus by the local minimum and split an idele into its one-place component and the remaining defining-modulus component.

Imports2
Imported by4

Declarations

theorem

exists_localDefiningExponent

L40 ↗
GlobalClassFieldTheory.GlobalClassFields.exists_localDefiningExponent
Documentation

If a global defining modulus exists, then at every finite place some higher-unit class subgroup is already contained in the given 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 exists_localDefiningExponent
    (H : Subgroup (IdeleClassGroup K))
    (h : ∃ m, IsDefiningModulus H m)
    (v : HeightOneSpectrum (𝓞 K)) :
    ∃ n : ℕ,
      RayClass.localHigherUnitClassSubgroup v n ≤ H
def

narrowFiniteLocalConductorExponent

L56 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteLocalConductorExponent
Documentation

The finite local conductor exponent seen by a conductorial subgroup.

Source context 8 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
open scoped Classical in
Lean source · statement
def narrowFiniteLocalConductorExponent
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) : ℕ
theorem

narrowFiniteLocalConductorExponent_spec

L63 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteLocalConductorExponent_spec
Documentation

The finite local conductor exponent has its defining higher-unit inclusion.

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 narrowFiniteLocalConductorExponent_spec
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    RayClass.localHigherUnitClassSubgroup v
        (H.narrowFiniteLocalConductorExponent v) ≤ H.1
theorem

narrowFiniteLocalConductorExponent_le

L72 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteLocalConductorExponent_le
Documentation

Minimality of the finite local conductor exponent.

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 narrowFiniteLocalConductorExponent_le
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K))
    {n : ℕ}
    (hn : RayClass.localHigherUnitClassSubgroup v n ≤ H.1) :
    H.narrowFiniteLocalConductorExponent v ≤ n
theorem

narrowFiniteLocalConductorExponent_eq_zero_iff

L84 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteLocalConductorExponent_eq_zero_iff
Documentation

The finite local conductor exponent vanishes exactly when the full finite-place integral-unit class subgroup lies in the 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 narrowFiniteLocalConductorExponent_eq_zero_iff
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    H.narrowFiniteLocalConductorExponent v = 0 ↔
      RayClass.localHigherUnitClassSubgroup v 0 ≤ H.1
theorem

replaceFiniteExponent_definingModulus

L102 ↗
GlobalClassFieldTheory.GlobalClassFields.replaceFiniteExponent_definingModulus
Documentation

Replacing one finite exponent of a defining modulus, while retaining its selected real places, again gives a defining modulus.

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]
open scoped Classical in
Lean source · statement
theorem replaceFiniteExponent_definingModulus
    (H : Subgroup (IdeleClassGroup K))
    (m : RayClass.Modulus K)
    (hm : IsDefiningModulus H m)
    (v : HeightOneSpectrum (𝓞 K))
    (n : ℕ)
    (hn : RayClass.localHigherUnitClassSubgroup v n ≤ H) :
    IsDefiningModulus H
      (m.replaceFinitePart (m.finitePart.update v n))
theorem

narrowFiniteConductorExponent_eq_narrowFiniteLocalConductorExponent

L199 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorExponent_eq_narrowFiniteLocalConductorExponent
Documentation

The narrow finite conductor exponent equals the independently defined finite local conductor exponent at every finite place.

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 narrowFiniteConductorExponent_eq_narrowFiniteLocalConductorExponent
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    H.narrowFiniteConductorExponent v =
      H.narrowFiniteLocalConductorExponent v
theorem

narrowFiniteConductor_apply_eq_narrowFiniteLocalConductorExponent

L233 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductor_apply_eq_narrowFiniteLocalConductorExponent
Documentation

The exponent of the narrow finite conductor at every finite place is its finite local conductor exponent.

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 narrowFiniteConductor_apply_eq_narrowFiniteLocalConductorExponent
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    H.narrowFiniteConductor v =
      H.narrowFiniteLocalConductorExponent v
theorem

exists_definingModulus_finitePart_agrees_on_finset

L244 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.exists_definingModulus_finitePart_agrees_on_finset
Documentation

A defining modulus can be chosen to agree with the narrow finite conductor on any prescribed finite set of finite places and with the fixed bounding modulus away from that set.

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 exists_definingModulus_finitePart_agrees_on_finset
    (H : ConductorialSubgroup K)
    (s : Finset (HeightOneSpectrum (𝓞 K))) :
    ∃ m : RayClass.Modulus K,
      IsDefiningModulus H.1 m ∧
        (∀ v ∈ s, m.finitePart v = H.narrowFiniteConductor v) ∧
        (∀ v ∉ s, m.finitePart v = H.narrowFiniteConductorBoundingModulus v)
theorem

exists_definingModulus_finitePart_eq_narrowFiniteConductor

L295 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.exists_definingModulus_finitePart_eq_narrowFiniteConductor
Documentation

A defining full modulus can be chosen whose finite part is exactly the narrow finite conductor.

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 exists_definingModulus_finitePart_eq_narrowFiniteConductor
    (H : ConductorialSubgroup K) :
    ∃ m : RayClass.Modulus K,
      IsDefiningModulus H.1 m ∧
        m.finitePart = H.narrowFiniteConductor
theorem

narrowFiniteConductor_antitone

L324 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductor_antitone
Documentation

The narrow finite conductor reverses inclusions of conductorial subgroups.

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 narrowFiniteConductor_antitone
    (H J : ConductorialSubgroup K)
    (hHJ : H.1 ≤ J.1) :
    J.narrowFiniteConductor ≤ H.narrowFiniteConductor

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.