Module

IdeleClassConnectedQuotient.lean

Nyll.ClassFieldTheory.Definitions.GlobalClassFieldTheory.IdeleClassConnectedQuotient

1 declaration indexed from sourceView source ↗

Module documentation

The connected-component quotient of the idèle class group

For a number field K, Mathlib's idèle class group is the unit group of the adele ring modulo principal idèles. Its quotient by the connected component of 1 is the group appearing in topological global reciprocity.

Imports4

Mathlib.NumberTheory.NumberField.AdeleRing
Mathlib.Topology.Algebra.Group.Quotient
Mathlib.Topology.Algebra.Group.Subgroup
Mathlib.Topology.Algebra.Group.Units

Imported by4

abbrev

IdeleClassConnectedQuotient

L27 ↗

ClassFieldTheory.IdeleClassConnectedQuotient

Documentation

The idèle class group modulo its identity component.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
namespace ClassFieldTheory
universe u

Lean source · statement

abbrev IdeleClassConnectedQuotient (K : Type u) [Field K] [NumberField K]

Module documentation

The connected-component quotient of the idèle class group

Declarations

IdeleClassConnectedQuotient