This module packages the connected component of the identity in the idele class group as a closed normal subgroup and names the corresponding quotient.
The connected component of the identity in the idele class group.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]def ideleClassIdentityComponent : Subgroup (IdeleClassGroup K)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem coe_ideleClassIdentityComponent :
(ideleClassIdentityComponent K : Set (IdeleClassGroup K)) =
connectedComponent (1 : IdeleClassGroup K)The identity component of the idele class group is closed.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem ideleClassIdentityComponent_isClosed :
IsClosed (ideleClassIdentityComponent K : Set (IdeleClassGroup K))Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]instance ideleClassIdentityComponent_normal :
(ideleClassIdentityComponent K).NormalThe idele class group modulo its identity component.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]abbrev ideleClassComponentQuotientSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]instance ideleClassComponentQuotientT2Space :
T2Space (ideleClassComponentQuotient K)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]instance ideleClassComponentQuotientTotallyDisconnectedSpace :
TotallyDisconnectedSpace (ideleClassComponentQuotient K)The positive archimedean norm section, passed to the idele class group.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]def ideleClassPositiveArchimedeanSection :
ℝ≥0ˣ →* IdeleClassGroup KThe positive archimedean section of the idele class group, with its natural continuity.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]def ideleClassPositiveArchimedeanSectionContinuous :
ℝ≥0ˣ →ₜ* IdeleClassGroup K where
__ := ideleClassPositiveArchimedeanSection K
continuous_toFun :=
QuotientGroup.continuous_mk.comp
(IdeleGroup.positiveArchimedeanSectionContinuous K).continuous_toFunSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem ideleClassPositiveArchimedeanSectionContinuous_apply
(r : ℝ≥0ˣ) :
ideleClassPositiveArchimedeanSectionContinuous K r =
ideleClassPositiveArchimedeanSection K rA positive real number, viewed as a nonnegative-real unit.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]def positiveRealNNRealUnit
(x : Set.Ioi (0 : ℝ)) : ℝ≥0ˣThe parametrization of nonnegative-real units by positive reals is continuous.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem continuous_positiveRealNNRealUnit :
Continuous positiveRealNNRealUnitThe multiplicative group of positive nonnegative reals is connected.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem nnrealUnits_connectedSpace :
ConnectedSpace ℝ≥0ˣEvery value of the positive archimedean class section lies in the identity component.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem ideleClassPositiveArchimedeanSection_mem_identityComponent
(r : ℝ≥0ˣ) :
ideleClassPositiveArchimedeanSection K r ∈
ideleClassIdentityComponent KSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem ideleClassPositiveArchimedeanSection_absoluteNorm
(r : ℝ≥0ˣ) :
IdeleClassGroup.absoluteNorm
(ideleClassPositiveArchimedeanSection K r) =
r⁻¹The norm-one factor of an idele-class representative after removing its positive archimedean norm component.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]def ideleClassNormOneCorrection
(a : IdeleGroup K) :
IdeleClassGroup.normOneSubgroup (K := K)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem coe_ideleClassNormOneCorrection (a : IdeleGroup K) :
(ideleClassNormOneCorrection K a : IdeleClassGroup K) =
QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
(IdeleGroup.positiveArchimedeanNormOneCorrection K a)Every idele class is the product of a norm-one class and the inverse of its positive archimedean norm section.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem ideleClass_mk_eq_normOneCorrection_mul_positiveSection_inv
(a : IdeleGroup K) :
QuotientGroup.mk' (IdeleGroup.principalSubgroup K) a =
(ideleClassNormOneCorrection K a : IdeleClassGroup K) *
(ideleClassPositiveArchimedeanSection K
(IdeleGroup.absoluteNorm a))⁻¹The norm-one idele classes map continuously onto the component quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]def ideleClassNormOneToComponentQuotient :
IdeleClassGroup.normOneSubgroup (K := K) →ₜ*
ideleClassComponentQuotient K where
__ :=
(QuotientGroup.mk' (ideleClassIdentityComponent K)).comp
(IdeleClassGroup.normOneSubgroup (K := K)).subtype
continuous_toFun :=
QuotientGroup.continuous_mk.comp continuous_subtype_valEvery connected-component class has a norm-one representative.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem ideleClassNormOneToComponentQuotient_surjective :
Function.Surjective (ideleClassNormOneToComponentQuotient K)The idele-class component quotient is compact.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]instance ideleClassComponentQuotientCompactSpace :
CompactSpace (ideleClassComponentQuotient K)Every continuous homomorphism from the idele class group to a totally disconnected topological group kills the identity component.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NNReal NumberField Topology
noncomputable section
variable (K : Type*) [Field K] [NumberField K]theorem ideleClassIdentityComponent_le_ker
{H : Type*}
[Group H] [TopologicalSpace H] [IsTopologicalGroup H]
[TotallyDisconnectedSpace H]
(f : IdeleClassGroup K →ₜ* H) :
ideleClassIdentityComponent K ≤ f.ker