ModuleGlobalCompositumGlobalEmbedding.lean
Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumGlobalEmbedding
2 declarations indexed from sourceView source ↗ Module documentation
The global cyclotomic factor inside the common local target
The global conductor cyclotomic field embeds, after base change and enlargement of the order, into the common p-adic cyclotomic target used by the synchronized valued compositum construction.
Declarations
KroneckerWeber.kroneckerWeberGlobalRightEmbeddingProperty
DocumentationThe global conductor cyclotomic factor embedded after base change to ℚ_p and enlargement of the cyclotomic order.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
KroneckerWeber.kroneckerWeberGlobalRightEmbedding
DocumentationAt a ramified prime, the global conductor cyclotomic field embeds into the common local cyclotomic target.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]