Hilbert class field (experimental) - Artin map and class field theory

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] [IsAbelianGalois F K] [IsUnramifiedEverywhere F K] : ClassGroup (RingOfIntegers F) →* Gal(K/F)

If K / F is an unramified abelian extension of number fields, 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). Its definition should not involve class field theory. We omit its formal definition here, but use sorry instead.

NOTE: a priori we don't know K / F is finite, so for x : K the Frobₚ x should be defined by the Frobenius on F(x) / F instead, which is a finite extension.

Equations

• NumberField.IsUnramifiedEverywhere.artinMap F K = sorry

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

The Artin map p ↦ Frobₚ is surjective. When K / F is finite, it could be proved by Chebotarev density theorem. In general suppose there exists σ : Gal(K/F) such that Frobₚ ≠ σ for all p : Cl(K), then for each p : Cl(K) there is x_p : K such that Frobₚ x_p ≠ σ x_p, hence the Artin map is not surjective on F(x_p | p : Gal(K/F)) / F, which is a contradiction, since this is a finite extension.

@[instance 100]

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

An unramified abelian extension of a number field is a finite extension.

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

An unramified abelian extension of a number field is a number field.

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

The degree of an unramified abelian extension of a number field divides the class number of the base field.

theorem NumberField.IsUnramifiedEverywhere.artinMap_spec (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsAbelianGalois F K] [IsUnramifiedEverywhere 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

Maximal unramified abelian subextension

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.

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)

Hilbert class field

theorem NumberField.IsUnramifiedEverywhere.bijective_artinMap_of_isSepClosed (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsSepClosed K] : Function.Bijective ⇑(artinMap F ↥(maximalUnramifiedAbelianExtension F K))

The Artin map Cl(F) → Gal(H / F) is bijective, if H is the maximal unramified abelian subextension of K / F and K is separably closed.

noncomputable def NumberField.IsUnramifiedEverywhere.artinEquivOfIsSepClosed (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsSepClosed K] : ClassGroup (RingOfIntegers F) ≃* Gal(↥(maximalUnramifiedAbelianExtension F K)/F)

The natural isomorphism Cl(F) ≃ Gal(H / F) given by Artin map, where H is the maximal unramified abelian subextension of K / F and K is separably closed.

Equations

• NumberField.IsUnramifiedEverywhere.artinEquivOfIsSepClosed F K = MulEquiv.ofBijective (NumberField.IsUnramifiedEverywhere.artinMap F ↥(NumberField.maximalUnramifiedAbelianExtension F K)) ⋯

theorem NumberField.IsUnramifiedEverywhere.artinEquivOfIsSepClosed_apply (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsSepClosed K] (p : ClassGroup (RingOfIntegers F)) : (artinEquivOfIsSepClosed F K) p = (artinMap F ↥(maximalUnramifiedAbelianExtension F K)) p

theorem NumberField.IsUnramifiedEverywhere.finrank_eq_classNumber_of_isSepClosed (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsSepClosed K] : Module.finrank F ↥(maximalUnramifiedAbelianExtension F K) = classNumber F

noncomputable def NumberField.IsUnramifiedEverywhere.liftOfIsSepClosed (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [NumberField F] [IsAbelianGalois F K] [IsUnramifiedEverywhere F K] (L : Type u_3) [Field L] [Algebra F L] [IsSepClosed L] : K →ₐ[F] ↥(maximalUnramifiedAbelianExtension F L)

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

Equations

• NumberField.IsUnramifiedEverywhere.liftOfIsSepClosed F K L = sorry