ModuleFiniteMathlibTopologyComparison.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.FiniteMathlibTopologyComparison
5 declarations indexed from sourceView source ↗ Module documentation
The finite idèle topology and adele units
The algebraic equivalence from finite idèles to units of the finite adele ring is continuous for the restricted-product topology on idèles and the graph topology on units. Both the value and inverse-value maps are induced by continuous maps on local factors.
Declarations
IdeleGroup.finiteEquivFiniteAdeleUnitsContinuousMulEquiv
DocumentationThe finite restricted-product idèles and finite adele units are canonically isomorphic as topological groups.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]
IdeleGroup.finiteEquivFiniteAdeleUnitsContinuousMulEquiv_apply
DocumentationThe topological and algebraic finite-idèle comparisons agree pointwise.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]
IdeleGroup.continuous_finiteEquivFiniteAdeleUnits
DocumentationThe algebraic finite-idèle comparison is continuous in the forward direction.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]
IdeleGroup.continuous_equivAdeleRingUnits
DocumentationThe algebraic equivalence from restricted-product idèles to adele units is continuous in the forward direction.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]
IdeleGroup.equivAdeleRingUnitsContinuousMulEquiv
DocumentationThe full restricted-product idèle group is canonically isomorphic to Mathlib's adele-unit idèle group as a topological group.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]