Module

EmbedsInEveryRayClassFieldRealization.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.EmbedsInEveryRayClassFieldRealization

1 declaration indexed from sourceView source ↗

Module documentation

Independence of the ray class field realization

The existential definition of EmbedsInRayClassField is independent of which Frobenius-normalized realization is chosen. It does not assert uniqueness of the embedding itself.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

embedsInRayClassField_iff_every_realization

L27 ↗

ClassFieldTheory.embedsInRayClassField_iff_every_realization

Documentation

Embedding in some ray class field realization is equivalent to embedding in every realization for the same modulus.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem embedsInRayClassField_iff_every_realization
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    (m : RayClassModulus K) :
    EmbedsInRayClassField K L m ↔
      ∀ R : RayClassFieldRealization K m,
        Nonempty (L →ₐ[K] R.extension)

Module documentation

Independence of the ray class field realization

Declarations

embedsInRayClassField_iff_every_realization