NYLL
Module

Conductor.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.Conductor
20 declarations indexed from sourceView source ↗

Module documentation

Narrow finite conductors

This file constructs the finite part of the conductor in the convention where every real place has the positive ray condition. It is therefore a narrow finite conductor, not yet the full global conductor of an arbitrary modulus with an archimedean component.

The narrow finite conductor is the gcd of all finite moduli whose ray class fields contain the given class field. On norm subgroups, those are exactly the moduli m for which C_K^m ≤ H.

We construct the gcd rather than postulating it. At each finite prime its exponent is the least exponent occurring among all defining moduli. A single defining modulus bounds the support, so these pointwise minima assemble into a genuine finitely supported modulus.

Imports1
Imported by2

Declarations

def

IsDefiningModulus

L42 ↗
GlobalClassFieldTheory.GlobalClassFields.IsDefiningModulus
Documentation

A modulus defines a ray class field containing the class field corresponding to H exactly when its congruence subgroup lies in H.

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
def IsDefiningModulus
    (H : Subgroup (IdeleClassGroup K))
    (m : RayClass.Modulus K) : Prop
abbrev

ConductorialSubgroup

L50 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup
Documentation

An idèle-class subgroup for which a finite ray-class defining modulus exists. This is precisely the domain on which the narrow finite conductor is defined.

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
abbrev ConductorialSubgroup
    (K : Type*) [Field K] [NumberField K]
theorem

exists_definingFiniteExponent

L58 ↗
GlobalClassFieldTheory.GlobalClassFields.exists_definingFiniteExponent
Documentation

At every finite place, some defining full modulus supplies a finite defining exponent. This is the nonemptiness input for the pointwise finite conductor minimum.

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_definingFiniteExponent
    (H : Subgroup (IdeleClassGroup K))
    (h : ∃ m, IsDefiningModulus H m)
    (v : HeightOneSpectrum (𝓞 K)) :
    ∃ n : ℕ, ∃ m : RayClass.Modulus K,
      IsDefiningModulus H m ∧ m.finitePart v = n
def

chosenDefiningModulus

L70 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.chosenDefiningModulus
Documentation

A chosen full modulus defining a conductorial 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
def chosenDefiningModulus
    (H : ConductorialSubgroup K) :
    RayClass.Modulus K
theorem

chosenDefiningModulus_spec

L76 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.chosenDefiningModulus_spec
Documentation

The chosen full defining modulus has the advertised defining property.

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 chosenDefiningModulus_spec
    (H : ConductorialSubgroup K) :
    IsDefiningModulus H.1 H.chosenDefiningModulus
def

narrowFiniteConductorBoundingModulus

L83 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorBoundingModulus
Documentation

The finite part of one chosen defining modulus, used to bound the support of 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
def narrowFiniteConductorBoundingModulus
    (H : ConductorialSubgroup K) :
    RayClass.FiniteModulus K
theorem

narrowFiniteConductorBoundingModulus_spec

L89 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorBoundingModulus_spec
Documentation

The finite bounding modulus comes from an actual defining full 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]
namespace ConductorialSubgroup
Lean source · statement
theorem narrowFiniteConductorBoundingModulus_spec
    (H : ConductorialSubgroup K) :
    ∃ m : RayClass.Modulus K,
      IsDefiningModulus H.1 m ∧
        m.finitePart = H.narrowFiniteConductorBoundingModulus
def

narrowFiniteConductorExponent

L99 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorExponent
Documentation

The least narrow finite conductor exponent at v among all defining moduli.

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 narrowFiniteConductorExponent
  (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) : ℕ
theorem

narrowFiniteConductorExponent_spec

L107 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorExponent_spec
Documentation

The least narrow finite conductor exponent is attained by an actual defining modulus.

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
theorem narrowFiniteConductorExponent_spec
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    ∃ m : RayClass.Modulus K,
      IsDefiningModulus H.1 m ∧
        m.finitePart v = H.narrowFiniteConductorExponent v
theorem

narrowFiniteConductorExponent_le

L118 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorExponent_le
Documentation

The narrow finite conductor exponent is no larger than the exponent in any defining modulus.

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
theorem narrowFiniteConductorExponent_le
    (H : ConductorialSubgroup K)
    {m : RayClass.Modulus K}
    (hm : IsDefiningModulus H.1 m)
    (v : HeightOneSpectrum (𝓞 K)) :
    H.narrowFiniteConductorExponent v ≤ m.finitePart v
def

narrowFiniteConductor

L131 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductor
Documentation

The finite part of the conductor in the all-real-positive (narrow) convention.

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 · full declaration
def narrowFiniteConductor
    (H : ConductorialSubgroup K) :
    RayClass.FiniteModulus K where
  toFun := H.narrowFiniteConductorExponent
  support :=
    H.narrowFiniteConductorBoundingModulus.support.filter
      (fun v => H.narrowFiniteConductorExponent v ≠ 0)
  mem_support_toFun := by
    intro v
    simp only [Finset.mem_filter, Finsupp.mem_support_iff]
    constructor
    · exact fun hv => hv.2
    · intro hv
      refine ⟨?_, hv⟩
      intro hbound
      have hle :
          H.narrowFiniteConductorExponent v ≤
            H.narrowFiniteConductorBoundingModulus v := by
        simpa only [narrowFiniteConductorBoundingModulus] using
        H.narrowFiniteConductorExponent_le
          H.chosenDefiningModulus_spec v
      rw [hbound] at hle
      exact hv (Nat.eq_zero_of_le_zero hle)
theorem

narrowFiniteConductor_apply

L158 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductor_apply
Documentation

Evaluating the narrow finite conductor returns 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
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    H.narrowFiniteConductor v = H.narrowFiniteConductorExponent v
theorem

narrowFiniteConductor_le

L166 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductor_le
Documentation

The narrow finite conductor divides every defining modulus (equivalently, its exponents are pointwise no larger).

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_le
    (H : ConductorialSubgroup K)
    {m : RayClass.Modulus K}
    (hm : IsDefiningModulus H.1 m) :
    H.narrowFiniteConductor ≤ m.finitePart
theorem

le_narrowFiniteConductor_iff

L175 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.le_narrowFiniteConductor_iff
Documentation

Universal gcd characterization of 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 le_narrowFiniteConductor_iff
    (H : ConductorialSubgroup K)
    (d : RayClass.FiniteModulus K) :
    d ≤ H.narrowFiniteConductor ↔
      ∀ m, IsDefiningModulus H.1 m → d ≤ m.finitePart
theorem

isOpen

L192 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.isOpen
Documentation

A conductorial subgroup is open because it contains a ray congruence 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 isOpen
    (H : ConductorialSubgroup K) :
    IsOpen ((H.1 : Subgroup (IdeleClassGroup K)) : Set (IdeleClassGroup K))
theorem

isClosed

L199 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.isClosed
Documentation

A conductorial subgroup is closed.

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 isClosed
    (H : ConductorialSubgroup K) :
    IsClosed ((H.1 : Subgroup (IdeleClassGroup K)) : Set (IdeleClassGroup K))
instance

finiteIndex

L205 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.finiteIndex
Documentation

A conductorial subgroup has finite index.

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
instance finiteIndex
    (H : ConductorialSubgroup K) :
    H.1.FiniteIndex
theorem

narrowFiniteConductor_is_gcd

L213 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductor_is_gcd
Documentation

The narrow finite conductor is the gcd of the finite parts of the defining full moduli.

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_is_gcd
    (H : ConductorialSubgroup K) :
    (∀ m, IsDefiningModulus H.1 m → H.narrowFiniteConductor ≤ m.finitePart) ∧
      (∀ d, (∀ m, IsDefiningModulus H.1 m → d ≤ m.finitePart) →
        d ≤ H.narrowFiniteConductor)
theorem

exists_definingModulus_of_isClosed_finiteIndex

L228 ↗
GlobalClassFieldTheory.GlobalClassFields.exists_definingModulus_of_isClosed_finiteIndex
Documentation

A closed finite-index subgroup always has at least one defining modulus.

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_definingModulus_of_isClosed_finiteIndex
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    ∃ m, IsDefiningModulus H m
def

ofClosedFiniteIndex

L242 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.ofClosedFiniteIndex
Documentation

The conductorial subgroup canonically associated to a closed finite-index idèle-class 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
def ofClosedFiniteIndex
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    ConductorialSubgroup K

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