ModuleMathlibTopologyComparison.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.MathlibTopologyComparison
2 declarations indexed from sourceView source ↗ Module documentation
Continuity of the comparison with Mathlib's idèle class group
The algebraic equivalence from the restricted-product idèle class group to Mathlib's adele-unit quotient is continuous. This is the quotient descent of the continuous map on idèles.
Declarations
IdeleGroup.continuous_ideleClassGroupEquivMathlib
DocumentationThe idèle-class comparison is continuous in the forward direction.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]
IdeleGroup.ideleClassGroupContinuousMulEquivMathlib
DocumentationThe restricted-product and adele-unit presentations of the idèle class group are canonically isomorphic as topological groups.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]