ModuleLocalConductor.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.LocalConductor
2 declarations indexed from sourceView source ↗ Module documentation
Local conductor subgroups in the idele class group
This file records the one-place higher-unit subgroups used to compare ray-class moduli with local conductors. The constructions are idele- and ray-class data and do not depend on the existence of a global class field.
Declarations
RayClass.localHigherUnitClassSubgroup
DocumentationThe image in C_K of the n-th higher-unit group at v.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace RayClass
open NumberField IsDedekindDomain
variable {K : Type*} [Field K] [NumberField K]
RayClass.localHigherUnitClassSubgroup_le_congruenceSubgroup
DocumentationA one-place higher-unit condition is contained in the corresponding global ray congruence subgroup.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace RayClass
open NumberField IsDedekindDomain
variable {K : Type*} [Field K] [NumberField K]