ModuleGlobalCompositumLeftFactors.lean
Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumLeftFactors
2 declarations indexed from sourceView source ↗ Module documentation
The left-factor ring embedding for the global compositum
The chosen localization remains internal to the proof. The public statement mentions only a ring embedding from L to the common local cyclotomic target, so elaborating its type never unfolds completion or transported-algebra instances. Rational linearity is added separately in the global-factor file by map_ratCast.
Declarations
KroneckerWeber.kroneckerWeberGlobalLeftRingEmbeddingProperty
DocumentationA ring embedding of L into the common local cyclotomic target which pulls the canonical target absolute value back to the chosen p-adic place. Its factorization through the chosen localization is retained in the proof, without exposing that expensive localization type in this declaration.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
KroneckerWeber.kroneckerWeberGlobalLeftRingEmbedding
DocumentationThe global field admits a ring embedding into the common local target which preserves the chosen p-adic place.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]