This file formalizes the diagonal embedding of Kˣ into the idele group and the resulting idele class group.
The diagonal embedding of Kˣ into the idele 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 IdeleGroupdef principalIdele : Kˣ →* IdeleGroup KThe finite component of a principal idele is the image of the underlying field element in the corresponding 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 IdeleGroup
variable {K}theorem finiteComponent_principalIdele
(x : Kˣ) (v : HeightOneSpectrum (𝓞 K)) :
((finiteComponent v (principalIdele K x) :
(v.adicCompletion K)ˣ) : v.adicCompletion K) = (x : K)The infinite component of a principal idele is the image of the underlying field element in the corresponding 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 IdeleGroup
variable {K}theorem infiniteComponent_principalIdele
(x : Kˣ) (w : InfinitePlace K) :
((infiniteComponent w (principalIdele K x) :
w.Completionˣ) : w.Completion) = (x : K)The diagonal map from field units to ideles is injective.
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 IdeleGroup
variable {K}
variable (K)theorem principalIdele_injective :
Function.Injective (principalIdele K)The subgroup of principal ideles.
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 IdeleGroup
variable {K}
variable (K)def principalSubgroup : Subgroup (IdeleGroup K)The multiplicative group Kˣ, identified with the subgroup of principal ideles.
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 IdeleGroup
variable {K}
variable (K)def principalEquiv : Kˣ ≃* principalSubgroup 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 IdeleGroup
variable {K}
variable (K)theorem coe_principalEquiv (x : Kˣ) :
(principalEquiv K x : IdeleGroup K) = principalIdele K xThe idele class group C_K = I_K / 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]abbrev IdeleClassGroup