All.lean
Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.LocalGlobalArtinCompatibility.All
0 declarations indexed from sourceView source ↗
Module documentation
Local-global compatibility of Artin homomorphisms
This compatibility module reexports the semantic layers that construct the separable-closure lift, its finite p-adic auxiliary field, and the resulting factorization of the global norm-residue map through every finite-place local Artin map.
Imports4
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.LocalGlobalArtinCompatibility.Factorization
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.LocalGlobalArtinCompatibility.FinitePadicAuxiliaryField
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.LocalGlobalArtinCompatibility.FinitePadicCyclicData
- Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.LocalGlobalArtinCompatibility.SeparableClosurePadicLift
This module has no indexed declarations. Its imports and full source are available here.