LocalCyclotomicEmbedding.lean

The ramified cyclotomic branch of local Kronecker–Weber. When the chosen prime element p is already a norm from L, the ramified realization theorem realizes the principal-unit depth furnished by openness as an actual p-power cyclotomic extension. Order reversal then embeds L into that extension.

The extra norm condition is exactly what excludes the nontrivial unramified part; the general construction also adjoins roots of unity of order p ^ f - 1.

Structured form of local Kronecker--Weber. The construction uses the cyclotomic order (p ^ f - 1) * p ^ n; retaining that form makes its unramified and p-primary ramified factors available to the global proof.

Openness supplies positive f,n with ⟨p ^ f⟩ Uⁿ ≤ N(Lˣ). The unramified cyclotomic theorem realizes ⟨p ^ f⟩ U¹ by the extension of order p ^ f - 1, while the ramified cyclotomic theorem realizes ⟨p⟩ Uⁿ by the p ^ n-cyclotomic extension. Their composite sits in the cyclotomic field of order (p ^ f - 1) * p ^ n, and the norm-subgroup order reversal gives the required embedding.

Local Kronecker--Weber: every finite abelian extension of ℚ_p embeds in a cyclotomic extension.

The type of actual embeddings of the localization at w into the m-th cyclotomic extension of ℚ_p. Naming this type exposes an embedding as a genuine theorem input while keeping all transported algebra instances internal.

Structured version of the local cyclotomic-embedding assertion. It retains the prime-to-p unramified order p ^ f - 1 and the ramified order p ^ n from the local cyclotomic construction.

The local completion of a finite abelian extension of ℚ, transported to the concrete base ℚ_[p], embeds in a cyclotomic extension.

This is the local cyclotomic input to the global construction. It does not yet assert that the local embeddings for the finitely many ramified primes glue into one global cyclotomic field.