A ray modulus consists of a finite modulus together with the real places at which positivity is imposed. This file defines the corresponding idèle and idèle-class congruence subgroups without fixing an archimedean convention.
A real infinite place of a number field.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClassabbrev RealPlace (K : Type*) [Field K] [NumberField K]A ray modulus consists of its finite part and the selected real places at which the positivity condition is imposed.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClassstructure Modulus (K : Type*) [Field K] [NumberField K] where
/-- The finite prime-power part of the modulus. -/
finitePart : FiniteModulus K
/-- The real places at which positivity is imposed. -/
infinitePart : Finset (RealPlace K)The full modulus with a prescribed finite part and no archimedean positivity condition.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusdef ofFinite (m : FiniteModulus K) : Modulus K where
finitePart := m
infinitePart := ∅The full modulus with a prescribed finite part and positivity at every real place.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical indef narrowOfFinite (m : FiniteModulus K) : Modulus K where
finitePart := m
infinitePart := Finset.univSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusinstance : Zero (Modulus K) where
zero := ofFinite 0Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem finitePart_ofFinite (m : FiniteModulus K) :
(ofFinite m).finitePart = mSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem infinitePart_ofFinite (m : FiniteModulus K) :
(ofFinite m).infinitePart = ∅Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem finitePart_narrowOfFinite (m : FiniteModulus K) :
(narrowOfFinite m).finitePart = mSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical intheorem infinitePart_narrowOfFinite (m : FiniteModulus K) :
(narrowOfFinite m).infinitePart = Finset.univSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem finitePart_zero :
(0 : Modulus K).finitePart = 0Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem infinitePart_zero :
(0 : Modulus K).infinitePart = ∅Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem ext {m n : Modulus K}
(hfinite : m.finitePart = n.finitePart)
(hinfinite : m.infinitePart = n.infinitePart) :
m = nSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusinstance : LE (Modulus K) where
le m n :=
m.finitePart ≤ n.finitePart ∧ m.infinitePart ⊆ n.infinitePartSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem le_iff {m n : Modulus K} :
m ≤ n ↔
m.finitePart ≤ n.finitePart ∧ m.infinitePart ⊆ n.infinitePartSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusinstance : PartialOrder (Modulus K) where
le_refl m := ⟨le_rfl, fun _ hx => hx⟩
le_trans m n p hmn hnp :=
⟨hmn.1.trans hnp.1, fun x hx => hnp.2 (hmn.2 hx)⟩
le_antisymm m n hmn hnm :=
ext (le_antisymm hmn.1 hnm.1) (by
apply Finset.ext
intro x
exact ⟨fun hx => hmn.2 hx, fun hx => hnm.2 hx⟩)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical ininstance : SemilatticeInf (Modulus K) where
inf m n :=
{ finitePart := m.finitePart ⊓ n.finitePart
infinitePart := m.infinitePart ∩ n.infinitePart }
inf_le_left _ _ :=
⟨inf_le_left, fun _ hx => (Finset.mem_inter.mp hx).1⟩
inf_le_right _ _ :=
⟨inf_le_right, fun _ hx => (Finset.mem_inter.mp hx).2⟩
le_inf _ _ _ hmn hmp :=
⟨le_inf hmn.1 hmp.1,
fun _ hx => Finset.mem_inter.mpr ⟨hmn.2 hx, hmp.2 hx⟩⟩Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical ininstance : SemilatticeSup (Modulus K) where
sup m n :=
{ finitePart := m.finitePart ⊔ n.finitePart
infinitePart := m.infinitePart ∪ n.infinitePart }
le_sup_left _ _ :=
⟨le_sup_left, fun _ hx => Finset.mem_union.mpr (Or.inl hx)⟩
le_sup_right _ _ :=
⟨le_sup_right, fun _ hx => Finset.mem_union.mpr (Or.inr hx)⟩
sup_le _ _ _ hmp hnp :=
⟨sup_le hmp.1 hnp.1, fun _ hx => by
rcases Finset.mem_union.mp hx with hx | hx
· exact hmp.2 hx
· exact hnp.2 hx⟩Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusinstance : Bot (Modulus K) where
bot := 0Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusinstance : OrderBot (Modulus K) where
bot_le _ := ⟨bot_le, Finset.empty_subset _⟩Replace the finite part of a full modulus while retaining exactly its selected real places.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusdef replaceFinitePart
(m : Modulus K) (f : FiniteModulus K) : Modulus K where
finitePart := f
infinitePart := m.infinitePartSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem finitePart_replaceFinitePart
(m : Modulus K) (f : FiniteModulus K) :
(m.replaceFinitePart f).finitePart = fSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem infinitePart_replaceFinitePart
(m : Modulus K) (f : FiniteModulus K) :
(m.replaceFinitePart f).infinitePart = m.infinitePartRemove the positivity condition at one real place.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical indef eraseRealPlace
(m : Modulus K) (v : RealPlace K) : Modulus K where
finitePart := m.finitePart
infinitePart := m.infinitePart.erase vSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem finitePart_eraseRealPlace
(m : Modulus K) (v : RealPlace K) :
(m.eraseRealPlace v).finitePart = m.finitePartSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical intheorem infinitePart_eraseRealPlace
(m : Modulus K) (v : RealPlace K) :
(m.eraseRealPlace v).infinitePart = m.infinitePart.erase vRemove the positivity conditions at a finite set of real places.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical indef eraseRealPlaces
(m : Modulus K) (s : Finset (RealPlace K)) : Modulus K where
finitePart := m.finitePart
infinitePart := m.infinitePart \ sSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem finitePart_eraseRealPlaces
(m : Modulus K) (s : Finset (RealPlace K)) :
(m.eraseRealPlaces s).finitePart = m.finitePartSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical intheorem infinitePart_eraseRealPlaces
(m : Modulus K) (s : Finset (RealPlace K)) :
(m.eraseRealPlaces s).infinitePart = m.infinitePart \ sSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical intheorem eraseRealPlaces_empty (m : Modulus K) :
m.eraseRealPlaces ∅ = mSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical intheorem eraseRealPlaces_insert
(m : Modulus K) (s : Finset (RealPlace K)) (v : RealPlace K) :
m.eraseRealPlaces (insert v s) =
(m.eraseRealPlaces s).eraseRealPlace vThe local infinite congruence condition at an infinite place. It is the positive subgroup exactly at a real place selected by the modulus, and the whole local group otherwise.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusdef localInfiniteCongruenceSubgroup (m : Modulus K)
(w : InfinitePlace K) : Subgroup w.CompletionˣSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem localInfiniteCongruenceSubgroup_replaceFinitePart
(m : Modulus K) (f : FiniteModulus K) (w : InfinitePlace K) :
(m.replaceFinitePart f).localInfiniteCongruenceSubgroup w =
m.localInfiniteCongruenceSubgroup wSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem localInfiniteCongruenceSubgroup_of_mem
(m : Modulus K) (v : RealPlace K) (hv : v ∈ m.infinitePart) :
m.localInfiniteCongruenceSubgroup v.1 = infinitePositiveSubgroup v.1Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem localInfiniteCongruenceSubgroup_of_not_mem
(m : Modulus K) (v : RealPlace K) (hv : v ∉ m.infinitePart) :
m.localInfiniteCongruenceSubgroup v.1 = ⊤Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem localInfiniteCongruenceSubgroup_of_not_isReal
(m : Modulus K) (w : InfinitePlace K) (hw : ¬ w.IsReal) :
m.localInfiniteCongruenceSubgroup w = ⊤The subgroup of infinite idèles positive at the real places selected by the modulus.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusdef infiniteCongruenceSubgroup (m : Modulus K) :
Subgroup (InfiniteIdeleGroup K)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem mem_infiniteCongruenceSubgroup_iff_local
(m : Modulus K) (a : InfiniteIdeleGroup K) :
a ∈ m.infiniteCongruenceSubgroup ↔
∀ w, ContinuousMulEquiv.piUnits a w ∈ m.localInfiniteCongruenceSubgroup wSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical intheorem mem_infiniteCongruenceSubgroup_iff
(m : Modulus K) (a : InfiniteIdeleGroup K) :
a ∈ m.infiniteCongruenceSubgroup ↔
∀ v : RealPlace K, v ∈ m.infinitePart →
ContinuousMulEquiv.piUnits a v.1 ∈ infinitePositiveSubgroup v.1Selecting every real place recovers the narrow infinite congruence subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulus
open scoped Classical intheorem infiniteCongruenceSubgroup_narrowOfFinite (f : FiniteModulus K) :
(narrowOfFinite f).infiniteCongruenceSubgroup =
narrowInfiniteCongruenceSubgroup (K := K)The idèle congruence subgroup attached to a full ray modulus.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusdef ideleCongruenceSubgroup (m : Modulus K) :
Subgroup (IdeleGroup K)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem mem_ideleCongruenceSubgroup_iff
(m : Modulus K) (a : IdeleGroup K) :
a ∈ m.ideleCongruenceSubgroup ↔
a.1 ∈ m.infiniteCongruenceSubgroup ∧
a.2 ∈ finiteCongruenceSubgroup m.finitePartSelecting every real place recovers the narrow idèle congruence subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulustheorem ideleCongruenceSubgroup_narrowOfFinite (f : FiniteModulus K) :
(narrowOfFinite f).ideleCongruenceSubgroup =
(narrowInfiniteCongruenceSubgroup (K := K)).prod
(finiteCongruenceSubgroup f)The ray congruence subgroup of the idèle class group attached to a full modulus.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusdef congruenceSubgroup (m : Modulus K) :
Subgroup (IdeleClassGroup K)The full ray congruence subgroup is normal in the idèle class group.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
namespace Modulusinstance congruenceSubgroup_normal (m : Modulus K) :
m.congruenceSubgroup.NormalThe ray class group attached to a full modulus.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClassabbrev RayClassGroup (m : Modulus K)The ray class group is equivalently the idèle group modulo the product of its congruence subgroup with the principal idèles.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClassdef rayClassGroupEquivIdeleQuotient (m : Modulus K) :
RayClassGroup m ≃*
IdeleGroup K ⧸
(m.ideleCongruenceSubgroup ⊔ IdeleGroup.principalSubgroup K)