Hilbert class field

StructureHilbert class field of a number field#✓fully proved

Let \(K\) and \(L\) be number fields with \(L\) an extension of \(K\). Then \(L\) is a Hilbert class field of \(K\) if \(L/K\) is a finite-dimensional abelian Galois extension, every nonzero prime ideal of the ring of integers \(\mathcal{O}_K\) is unramified in \(\mathcal{O}_L\), every infinite place of \(L\) is unramified over \(K\), and \(L\) is maximal with these properties: every number field \(M\) that is a finite-dimensional abelian Galois extension of \(K\), such that every nonzero prime ideal of \(\mathcal{O}_K\) is unramified in \(\mathcal{O}_M\) and every infinite place of \(M\) is unramified over \(K\), admits a \(K\)-algebra homomorphism \(M \to L\).

NumberField.IsHilbertClassField · 20 lines

structure IsHilbertClassField (K L : Type u) [Field K] [Field L] [NumberField K]
    [NumberField L] [Algebra K L] : Prop where
  /-- `L / K` is finite-dimensional. -/
  finiteDimensional : FiniteDimensional K L
  /-- `L / K` is abelian Galois. -/
  isAbelianGalois : IsAbelianGalois K L
  /-- Every finite height-one prime of `𝓞 K` is unramified in `𝓞 L`. -/
  isUnramified_finite :
    ∀ 𝔭 : IsDedekindDomain.HeightOneSpectrum (𝓞 K),
      Algebra.IsUnramifiedIn (𝓞 L) 𝔭.asIdeal
  /-- `L / K` is unramified at every infinite place. -/
  isUnramified_infinite : IsUnramifiedAtInfinitePlaces K L
  /-- Maximality: every admissible competitor `M / K` embeds into `L` over `K`. -/
  maximal : ∀ (M : Type u) [Field M] [NumberField M] [Algebra K M],
    FiniteDimensional K M →
    IsAbelianGalois K M →
    (∀ 𝔭 : IsDedekindDomain.HeightOneSpectrum (𝓞 K),
      Algebra.IsUnramifiedIn (𝓞 M) 𝔭.asIdeal) →
    IsUnramifiedAtInfinitePlaces K M →
    Nonempty (M →ₐ[K] L)

Used by 1

Used byAbelian unramified extensions embed in the Hilbert class field

TheoremAbelian unramified extensions embed in the Hilbert class field#✓fully proved

Let \(K\) and \(L\) be number fields with \(L\) an extension of \(K\) that is a Hilbert class field of \(K\). If \(M\) is a number field that is a finite-dimensional abelian Galois extension of \(K\), such that every nonzero prime ideal of the ring of integers \(\mathcal{O}_K\) is unramified in \(\mathcal{O}_M\) and every infinite place of \(M\) is unramified over \(K\), then there is a \(K\)-algebra homomorphism \(M \to L\).

theorem IsHilbertClassField.apply_maximal {M : Type u} [Field M] [NumberField M]
    [Algebra K M] (h : IsHilbertClassField K L)
    (hfin : FiniteDimensional K M)
    (hgal : IsAbelianGalois K M)
    (hfinU : ∀ 𝔭 : IsDedekindDomain.HeightOneSpectrum (𝓞 K),
      Algebra.IsUnramifiedIn (𝓞 M) 𝔭.asIdeal)
    (hinfU : IsUnramifiedAtInfinitePlaces K M) : Nonempty (M →ₐ[K] L)

Uses 1

Statement usesHilbert class field of a number field

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.