Hilbert class field (experimental)

Assertion that a finite extension is unramified everywhere

class NumberField.IsUnramifiedEverywhere (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] : Prop

A typeclass asserting that a (potentially infinite) field extension K / F is unramified everywhere. Defined to be that any finite subextension E / F is unramified at all finite places and all infinite places. Only makes sense when the base field F is a number field.

• isUnramifiedAt_of_heightOneSpectrum (E : IntermediateField F K) [FiniteDimensional F ↥E] (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ↥E)) : Algebra.IsUnramifiedAt (RingOfIntegers F) w.asIdeal
• isUnramifiedAtInfinitePlaces (E : IntermediateField F K) [FiniteDimensional F ↥E] : IsUnramifiedAtInfinitePlaces F ↥E

theorem NumberField.isUnramifiedEverywhere_iff (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] : IsUnramifiedEverywhere F K ↔ (∀ (E : IntermediateField F K) [FiniteDimensional F ↥E] (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ↥E)), Algebra.IsUnramifiedAt (RingOfIntegers F) w.asIdeal) ∧ ∀ (E : IntermediateField F K) [FiniteDimensional F ↥E], IsUnramifiedAtInfinitePlaces F ↥E

theorem NumberField.isUnramifiedEverywhere_iff_of_finiteDimensional (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] : IsUnramifiedEverywhere F K ↔ (∀ (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), Algebra.IsUnramifiedAt (RingOfIntegers F) w.asIdeal) ∧ IsUnramifiedAtInfinitePlaces F K

theorem NumberField.IsUnramifiedEverywhere.tower_top (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [IsUnramifiedEverywhere F L] : IsUnramifiedEverywhere K L

theorem NumberField.IsUnramifiedEverywhere.tower_bot (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [IsUnramifiedEverywhere F L] : IsUnramifiedEverywhere F K

theorem NumberField.IsUnramifiedEverywhere.trans (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [IsUnramifiedEverywhere F K] [IsUnramifiedEverywhere K L] : IsUnramifiedEverywhere F L

Maximal unramified abelian subextension

def NumberField.maximalUnramifiedAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] : IntermediateField F K

The maximal unramified abelian subextension of a number field F inside K.

Equations

• NumberField.maximalUnramifiedAbelianExtension F K = sSup {E : IntermediateField F K | IsAbelianGalois F ↥E ∧ NumberField.IsUnramifiedEverywhere F ↥E}

theorem NumberField.isGalois_maximalUnramifiedAbelianExtension_of_isGalois (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [IsGalois F L] [IsGalois F K] : IsGalois F ↥(maximalUnramifiedAbelianExtension K L)

If L / K / F is a field extension tower, such that L / F and K / F are Galois, then H / F is also Galois, where H is the maximal unramified abelian subextension of L / K.

instance NumberField.finiteDimensional_maximalUnramifiedAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] : FiniteDimensional F ↥(maximalUnramifiedAbelianExtension F K)

The maximal unramified abelian subextension is a finite extension. A result in global class field theory. We cannot prove it here.

instance NumberField.isAbelianGalois_maximalUnramifiedAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] : IsAbelianGalois F ↥(maximalUnramifiedAbelianExtension F K)

The maximal unramified abelian subextension is an abelian extension. Because compositum of abelian Galois extensions is also abelian. Proof: the group homomorphism Gal(⨆ i, E_i/F) → Π i, Gal(E_i/F) is injective. Should go mathlib.

instance NumberField.isUnramifiedEverywhere_maximalUnramifiedAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] : IsUnramifiedEverywhere F ↥(maximalUnramifiedAbelianExtension F K)

The maximal unramified abelian subextension is unramified everywhere. Because when considering only one place, compositum of unramified extensions is also unramified. Should find a proof and submit to mathlib.

instance NumberField.numberField_maximalUnramifiedAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] : NumberField ↥(maximalUnramifiedAbelianExtension F K)

@[instance 100]

instance NumberField.IsUnramifiedEverywhere.finiteDimensional (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsUnramifiedEverywhere F K] [IsAbelianGalois F K] : FiniteDimensional F K

An unramified everywhere abelian extension of a number field must be finite.

theorem NumberField.IsUnramifiedEverywhere.numberField (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsUnramifiedEverywhere F K] [IsAbelianGalois F K] : NumberField K

An unramified everywhere abelian extension of a number field must be a number field.

Artin map of an unramified abelian extension

noncomputable def NumberField.IsUnramifiedEverywhere.artinMap (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsUnramifiedEverywhere F K] [IsAbelianGalois F K] : ClassGroup (RingOfIntegers F) →* Gal(K/F)

If K / F is an unramified abelian extension, then there is a natural map Cl(F) → Gal(K/F) sending a prime ideal p to the Frobenius element Frobₚ in Gal(K/F). We cannot give the formal definition of it here, but use sorry instead.

Equations

• NumberField.IsUnramifiedEverywhere.artinMap F K = sorry

theorem NumberField.IsUnramifiedEverywhere.artinMap_spec (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsUnramifiedEverywhere F K] [IsAbelianGalois F K] (p : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers F)) (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (h : Ideal.under (RingOfIntegers F) P.asIdeal = p.asIdeal) : (artinMap F K) (ClassGroup.mk0 ⟨p.asIdeal, ⋯⟩) = arithFrobAt (RingOfIntegers F) Gal(K/F) P.asIdeal

theorem NumberField.IsUnramifiedEverywhere.surjective_artinMap (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsUnramifiedEverywhere F K] [IsAbelianGalois F K] : Function.Surjective ⇑(artinMap F K)

The Artin map is p ↦ Frobₚ surjective. It is a consequence of a stronger result: Chebotarev density theorem.

theorem NumberField.IsUnramifiedEverywhere.finrank_dvd_classNumber (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsUnramifiedEverywhere F K] [IsAbelianGalois F K] : Module.finrank F K ∣ classNumber F

Hilbert class field

def NumberField.HilbertClassField (F : Type u_1) [Field F] : Type u_1

The Hilbert class field H_F of a number field F, defined as a Type corresponding to the maximal unramified abelian extension of F inside its separable closure.

Equations

• NumberField.HilbertClassField F = ↥(NumberField.maximalUnramifiedAbelianExtension F (SeparableClosure F))

noncomputable instance NumberField.HilbertClassField.instField (F : Type u_1) [Field F] : Field (HilbertClassField F)

Equations

• NumberField.HilbertClassField.instField F = inferInstanceAs (Field ↥(NumberField.maximalUnramifiedAbelianExtension F (SeparableClosure F)))

noncomputable instance NumberField.HilbertClassField.algebra (F : Type u_1) [Field F] : Algebra F (HilbertClassField F)

Equations

• NumberField.HilbertClassField.algebra F = inferInstanceAs (Algebra F ↥(NumberField.maximalUnramifiedAbelianExtension F (SeparableClosure F)))

noncomputable instance NumberField.HilbertClassField.instInhabited (F : Type u_1) [Field F] : Inhabited (HilbertClassField F)

Equations

• NumberField.HilbertClassField.instInhabited F = { default := 0 }

instance NumberField.HilbertClassField.instCharZero (F : Type u_1) [Field F] [CharZero F] : CharZero (HilbertClassField F)

instance NumberField.HilbertClassField.instCharP (F : Type u_1) [Field F] (p : ℕ) [CharP F p] : CharP (HilbertClassField F) p

instance NumberField.HilbertClassField.instExpChar (F : Type u_1) [Field F] (p : ℕ) [ExpChar F p] : ExpChar (HilbertClassField F) p

noncomputable instance NumberField.HilbertClassField.algebra' (F : Type u_1) [Field F] (R : Type u_3) [CommRing R] [Algebra R F] : Algebra R (HilbertClassField F)

Equations

• NumberField.HilbertClassField.algebra' F R = inferInstanceAs (Algebra R ↥(NumberField.maximalUnramifiedAbelianExtension F (SeparableClosure F)))

instance NumberField.HilbertClassField.instIsScalarTower (F : Type u_1) [Field F] (R : Type u_3) [CommRing R] [Algebra R F] : IsScalarTower R F (HilbertClassField F)

instance NumberField.HilbertClassField.instNoZeroSMulDivisors (F : Type u_1) [Field F] (R : Type u_3) [CommRing R] [Algebra R F] [IsFractionRing R F] : NoZeroSMulDivisors R (HilbertClassField F)

instance NumberField.HilbertClassField.isSeparable (F : Type u_1) [Field F] : Algebra.IsSeparable F (HilbertClassField F)

instance NumberField.HilbertClassField.finiteDimensional (F : Type u_1) [Field F] [NumberField F] : FiniteDimensional F (HilbertClassField F)

The Hilbert class field H_F is a finite extension of F.

instance NumberField.HilbertClassField.isAbelianGalois (F : Type u_1) [Field F] : IsAbelianGalois F (HilbertClassField F)

The Hilbert class field H_F is an abelian extension of F.

instance NumberField.HilbertClassField.isUnramifiedEverywhere (F : Type u_1) [Field F] : IsUnramifiedEverywhere F (HilbertClassField F)

The Hilbert class field H_F is unramified everywhere over F.

instance NumberField.HilbertClassField.numberField (F : Type u_1) [Field F] [NumberField F] : NumberField (HilbertClassField F)

The Hilbert class field H_F is a number field.

theorem NumberField.HilbertClassField.isGalois_of_isGalois (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [IsGalois F K] : IsGalois F (HilbertClassField K)

If K / F is a Galois extension, then H_K / F is also Galois, where H_K is the Hilbert class field of K.

theorem NumberField.HilbertClassField.bijective_artinMap (F : Type u_1) [Field F] [NumberField F] : Function.Bijective ⇑(IsUnramifiedEverywhere.artinMap F (HilbertClassField F))

The Artin map Cl(F) → Gal(H_F / F) is bijective.

noncomputable def NumberField.HilbertClassField.artinEquiv (F : Type u_1) [Field F] [NumberField F] : ClassGroup (RingOfIntegers F) ≃* Gal(HilbertClassField F/F)

The natural isomorphism Cl(F) ≃ Gal(H_F / F) given by Artin map.

Equations

• NumberField.HilbertClassField.artinEquiv F = MulEquiv.ofBijective (NumberField.IsUnramifiedEverywhere.artinMap F (NumberField.HilbertClassField F)) ⋯

theorem NumberField.HilbertClassField.artinEquiv_apply (F : Type u_1) [Field F] [NumberField F] (p : ClassGroup (RingOfIntegers F)) : (artinEquiv F) p = (IsUnramifiedEverywhere.artinMap F (HilbertClassField F)) p

theorem NumberField.HilbertClassField.finrank_eq_classNumber (F : Type u_1) [Field F] [NumberField F] : Module.finrank F (HilbertClassField F) = classNumber F

noncomputable def NumberField.HilbertClassField.lift (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsUnramifiedEverywhere F K] [IsAbelianGalois F K] : K →ₐ[F] HilbertClassField F

Any unramified abelian extension is a subfield of Hilbert class field.

Equations

• NumberField.HilbertClassField.lift F K = sorry