NYLL
Module

ConductorInfinitePart.lean

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

Module documentation

Removing one real place from a defining modulus

This file gives the one-place archimedean step toward the full conductor. Removing the positivity condition at a real place preserves the defining property exactly when the whole one-place idèle-class image is already contained in the target subgroup.

Imports1
Imported by4

Declarations

theorem

eraseRealPlace_le

L32 ↗
GlobalClassFieldTheory.GlobalClassFields.eraseRealPlace_le
Documentation

Erasing a selected real place can only decrease a full 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 eraseRealPlace_le
    (m : RayClass.Modulus K) (v : RayClass.RealPlace K) :
    m.eraseRealPlace v ≤ m
theorem

infinitePlaceIdeleClass_range_le_congruenceSubgroup_of_not_mem

L40 ↗
GlobalClassFieldTheory.GlobalClassFields.infinitePlaceIdeleClass_range_le_congruenceSubgroup_of_not_mem
Documentation

If a real place is not selected by a modulus, its whole one-place idèle-class image lies in the corresponding ray congruence 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 infinitePlaceIdeleClass_range_le_congruenceSubgroup_of_not_mem
    (m : RayClass.Modulus K) (v : RayClass.RealPlace K)
    (hv : v ∉ m.infinitePart) :
    (IdeleGroup.infinitePlaceIdeleClass v.1).range ≤
      m.congruenceSubgroup
theorem

eraseRealPlace_isDefiningModulus_of_range_le

L76 ↗
GlobalClassFieldTheory.GlobalClassFields.eraseRealPlace_isDefiningModulus_of_range_le
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 eraseRealPlace_isDefiningModulus_of_range_le
    (H : Subgroup (IdeleClassGroup K))
    (m : RayClass.Modulus K)
    (hm : IsDefiningModulus H m)
    (v : RayClass.RealPlace K)
    (hvH : (IdeleGroup.infinitePlaceIdeleClass v.1).range ≤ H) :
    IsDefiningModulus H (m.eraseRealPlace v)
theorem

eraseRealPlace_isDefiningModulus_iff

L173 ↗
GlobalClassFieldTheory.GlobalClassFields.eraseRealPlace_isDefiningModulus_iff
Documentation

Removing the positivity condition at one real place preserves the defining-modulus property exactly when the whole one-place idèle-class image is already contained in the target 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 eraseRealPlace_isDefiningModulus_iff
    (H : Subgroup (IdeleClassGroup K))
    (m : RayClass.Modulus K)
    (v : RayClass.RealPlace K) :
    IsDefiningModulus H (m.eraseRealPlace v) ↔
      IsDefiningModulus H m ∧
        (IdeleGroup.infinitePlaceIdeleClass v.1).range ≤ H
theorem

eraseRealPlaces_isDefiningModulus_of_ranges_le

L195 ↗
GlobalClassFieldTheory.GlobalClassFields.eraseRealPlaces_isDefiningModulus_of_ranges_le
Documentation

Erasing finitely many real places preserves the defining-modulus property when every corresponding one-place idèle-class image is contained in the target 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 eraseRealPlaces_isDefiningModulus_of_ranges_le
    (H : Subgroup (IdeleClassGroup K))
    (m : RayClass.Modulus K)
    (hm : IsDefiningModulus H m)
    (s : Finset (RayClass.RealPlace K))
    (hs : ∀ v ∈ s,
      (IdeleGroup.infinitePlaceIdeleClass v.1).range ≤ H) :
    IsDefiningModulus H (m.eraseRealPlaces s)
def

fullConductorInfinitePart

L223 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.fullConductorInfinitePart
Documentation

The real places whose one-place idèle-class image is not contained in the target 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 fullConductorInfinitePart
    (H : ConductorialSubgroup K) : Finset (RayClass.RealPlace K)
theorem

mem_fullConductorInfinitePart_iff

L231 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.mem_fullConductorInfinitePart_iff
Documentation

Membership in the infinite part of the full conductor is the failure of the corresponding one-place idèle-class image to lie in the target 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 mem_fullConductorInfinitePart_iff
    (H : ConductorialSubgroup K) (v : RayClass.RealPlace K) :
    v ∈ H.fullConductorInfinitePart ↔
      ¬ (IdeleGroup.infinitePlaceIdeleClass v.1).range ≤ H.1
theorem

fullConductorInfinitePart_subset_of_isDefiningModulus

L239 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.fullConductorInfinitePart_subset_of_isDefiningModulus
Documentation

Every defining modulus contains the infinite part of the full 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 fullConductorInfinitePart_subset_of_isDefiningModulus
    (H : ConductorialSubgroup K) {m : RayClass.Modulus K}
    (hm : IsDefiningModulus H.1 m) :
    H.fullConductorInfinitePart ⊆ m.infinitePart
def

fullConductor

L252 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.fullConductor
Documentation

The full conductor, with the narrow finite conductor as finite part and exactly the required real places as infinite part.

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 · full declaration
def fullConductor
    (H : ConductorialSubgroup K) : RayClass.Modulus K where
  finitePart := H.narrowFiniteConductor
  infinitePart := H.fullConductorInfinitePart
theorem

fullConductor_isDefiningModulus

L258 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.fullConductor_isDefiningModulus
Documentation

The full conductor is itself 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 fullConductor_isDefiningModulus
    (H : ConductorialSubgroup K) :
    IsDefiningModulus H.1 H.fullConductor
theorem

isDefiningModulus_iff_fullConductor_le

L289 ↗
GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.isDefiningModulus_iff_fullConductor_le
Documentation

A modulus is defining exactly when it is at least the full 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 isDefiningModulus_iff_fullConductor_le
    (H : ConductorialSubgroup K) (m : RayClass.Modulus K) :
    IsDefiningModulus H.1 m ↔ H.fullConductor ≤ m

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