Module

ConductorLattice.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorLattice

12 declarations indexed from sourceView source ↗

Module documentation

Lattice operations on narrow finite conductors

Increasing a modulus decreases its ray congruence subgroup. This contravariance makes the narrow finite conductor of an intersection of norm subgroups the pointwise maximum of their narrow finite conductors. Under class-field correspondence, this is the finite-part lcm formula for a compositum. For a generated subgroup one obtains the complementary divisibility by the pointwise minimum.

Imports2

Imported by4

theorem

rayClassFiniteCongruenceSubgroup_antitone

L35 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassFiniteCongruenceSubgroup_antitone

Documentation

Finite idèle congruence subgroups are contravariant in the 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 rayClassFiniteCongruenceSubgroup_antitone
    {m n : RayClass.FiniteModulus K} (hmn : m ≤ n) :
    RayClass.finiteCongruenceSubgroup n ≤
      RayClass.finiteCongruenceSubgroup m

theorem

rayClassInfiniteCongruenceSubgroup_antitone

L46 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassInfiniteCongruenceSubgroup_antitone

Documentation

Infinite idèle congruence subgroups are contravariant in the full modulus: selecting more real places imposes more positivity conditions.

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 rayClassInfiniteCongruenceSubgroup_antitone
    {m n : RayClass.Modulus K} (hmn : m ≤ n) :
    n.infiniteCongruenceSubgroup ≤
      m.infiniteCongruenceSubgroup

theorem

rayClassIdeleCongruenceSubgroup_antitone

L56 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassIdeleCongruenceSubgroup_antitone

Documentation

Idèle congruence subgroups are contravariant in the 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 rayClassIdeleCongruenceSubgroup_antitone
    {m n : RayClass.Modulus K} (hmn : m ≤ n) :
    n.ideleCongruenceSubgroup ≤
      m.ideleCongruenceSubgroup

theorem

rayClassCongruenceSubgroup_antitone

L69 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassCongruenceSubgroup_antitone

Documentation

Ray congruence subgroups in the idèle class group are contravariant in the 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 rayClassCongruenceSubgroup_antitone
    {m n : RayClass.Modulus K} (hmn : m ≤ n) :
    n.congruenceSubgroup ≤
      m.congruenceSubgroup

theorem

isDefiningModulus_mono

L83 ↗

GlobalClassFieldTheory.GlobalClassFields.isDefiningModulus_mono

Documentation

Once a modulus defines a subgroup, every larger modulus also defines it.

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 isDefiningModulus_mono
    (H : Subgroup (IdeleClassGroup K))
    {m n : RayClass.Modulus K}
    (hm : IsDefiningModulus H m)
    (hmn : m ≤ n) :
    IsDefiningModulus H n

theorem

narrowFiniteConductor_isDefiningModulus

L96 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductor_isDefiningModulus

Documentation

The exact narrow finite conductor, interpreted as a full modulus with positivity at every real place, is 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]
namespace ConductorialSubgroup

Lean source · statement

theorem narrowFiniteConductor_isDefiningModulus
    (H : ConductorialSubgroup K) :
    IsDefiningModulus H.1
      (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)

theorem

inf_narrowFiniteConductor_isDefiningModulus

L108 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.inf_narrowFiniteConductor_isDefiningModulus

Documentation

The join of the narrow finite conductors defines the intersection of the two underlying 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 inf_narrowFiniteConductor_isDefiningModulus
    (H J : ConductorialSubgroup K) :
    IsDefiningModulus (H.1 ⊓ J.1)
      (RayClass.Modulus.narrowOfFinite
        (H.narrowFiniteConductor ⊔ J.narrowFiniteConductor))

def

inf

L124 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.inf

Documentation

The intersection of two conductorial subgroups, with its defining modulus obtained from the two actual narrow finite conductors.

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 inf
  (H J : ConductorialSubgroup K) :
    ConductorialSubgroup K

def

sup

L133 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.sup

Documentation

The subgroup generated by two 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

def sup
  (H J : ConductorialSubgroup K) :
    ConductorialSubgroup K

theorem

narrowFiniteConductor_inf

L142 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductor_inf

Documentation

The narrow finite conductor of an intersection is the pointwise maximum of the two narrow finite conductors.

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_inf
    (H J : ConductorialSubgroup K) :
    (H.inf J).narrowFiniteConductor =
      H.narrowFiniteConductor ⊔ J.narrowFiniteConductor

theorem

narrowFiniteConductor_inf_support

L163 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductor_inf_support

Documentation

The finite-prime support of the narrow finite conductor of an intersection is the union of the two conductor supports.

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 narrowFiniteConductor_inf_support
    (H J : ConductorialSubgroup K) :
    (H.inf J).narrowFiniteConductor.support =
      H.narrowFiniteConductor.support ∪
        J.narrowFiniteConductor.support

theorem

narrowFiniteConductor_sup_le_inf

L172 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductor_sup_le_inf

Documentation

The narrow finite conductor of the subgroup generated by two conductorial subgroups divides the pointwise minimum of their conductors.

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_sup_le_inf
    (H J : ConductorialSubgroup K) :
    (H.sup J).narrowFiniteConductor ≤
      H.narrowFiniteConductor ⊓ J.narrowFiniteConductor

Module documentation

Lattice operations on narrow finite conductors

Declarations