Finiteness of the ordinary ideal class group lets us choose one idele representing each ideal class. The union of the (finite) supports of those representatives is a finite set S for which
I_K = I_K^S Kˣ.
A chosen idele representing an ordinary ideal class.
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 IdeleGroupdef classRepresentative (c : ClassGroup (𝓞 K)) :
IdeleGroup KSurrounding 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 IdeleGrouptheorem idealClass_classRepresentative
(c : ClassGroup (𝓞 K)) :
idealClass (classRepresentative (K := K) c) = cA finite set outside which the chosen representative of c is integral.
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 IdeleGroupdef classRepresentativeSupport (c : ClassGroup (𝓞 K)) :
Finset (HeightOneSpectrum (𝓞 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 IdeleGrouptheorem classRepresentative_mem_support
(c : ClassGroup (𝓞 K)) :
classRepresentative (K := K) c ∈
supportedAt (K := K)
(classRepresentativeSupport (K := K) c : Set _)The union of the supports of one representative of every ordinary ideal class. It is finite because the ideal class group is finite.
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 IdeleGroupdef sufficientlyLargeFiniteSet :
Finset (HeightOneSpectrum (𝓞 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 IdeleGrouptheorem classRepresentative_mem_sufficientlyLarge
(c : ClassGroup (𝓞 K)) :
classRepresentative (K := K) c ∈
supportedAt (K := K)
(sufficientlyLargeFiniteSet (K := K) : Set _)The ideles supported at sufficientlyLargeFiniteSet already map surjectively to the ordinary ideal 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 IdeleGrouptheorem idealClass_surjective_on_sufficientlyLarge :
∀ c : ClassGroup (𝓞 K),
∃ a ∈ supportedAt (K := K)
(sufficientlyLargeFiniteSet (K := K) : Set _),
idealClass a = cFor a sufficiently large finite set S of finite places, every idele is the product of an idele integral away from S and a principal idele.
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 IdeleGrouptheorem supportedAt_sup_principalSubgroup_eq_top :
supportedAt (K := K)
(sufficientlyLargeFiniteSet (K := K) : Set _) ⊔
principalSubgroup K = ⊤Existential form of the sufficiently-large support theorem.
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 IdeleGrouptheorem exists_finset_supportedAt_sup_principalSubgroup_eq_top :
∃ S : Finset (HeightOneSpectrum (𝓞 K)),
supportedAt (K := K) (S : Set _) ⊔ principalSubgroup K = ⊤