Hilbert's theorem 94

This file proves the class-number divisibility result used in the regular-prime argument.

instance instIsAlgebraic_leanPool {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] : Algebra.IsAlgebraic K L

theorem comap_span_galRestrict_eq_of_cyclic {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : Gal(L/K)) (hσ : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers σ) {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Algebra A K] [Algebra B L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K] [IsIntegralClosure B A L] (β : B) (η : Bˣ) (hβ : ↑η * ((galRestrict A K L B) σ) β = β) (σ' : Gal(L/K)) : Ideal.comap ((galRestrict A K L B) σ') (Ideal.span {β}) = Ideal.span {β}

theorem exists_not_isPrincipal_and_isPrincipal_map_aux {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : Gal(L/K)) (hσ : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers σ) {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Algebra A K] [Algebra B L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K] [IsIntegralClosure B A L] [IsGalois K L] [IsDedekindDomain A] [Algebra.Unramified A B] (η : Bˣ) (hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1) (hη' : ¬∃ (α : Bˣ), (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)) : ∃ (I : Ideal A), ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)

theorem Ideal.isPrincipal_pow_finrank_of_isPrincipal_map {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Algebra A K] [Algebra B L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K] [IsIntegralClosure B A L] [IsGalois K L] [IsDedekindDomain A] {I : Ideal A} (hI : Submodule.IsPrincipal (map (algebraMap A B) I)) : Submodule.IsPrincipal (I ^ Module.finrank K L)

theorem exists_not_isPrincipal_and_isPrincipal_map (K L : Type) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Algebra.Unramified (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)] [h : IsCyclic Gal(L/K)] (hKL : Nat.Prime (Module.finrank K L)) (hKL' : Module.finrank K L ≠ 2) : ∃ (I : Ideal (NumberField.RingOfIntegers K)), ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) I)

This is the first part of Hilbert Theorem 94, which states that if L/K is an unramified cyclic finite extension of number fields of odd prime degree, then there is an ideal that capitulates in K.

theorem dvd_card_classGroup_of_unramified_isCyclic {K L : Type} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Algebra.Unramified (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)] [IsCyclic Gal(L/K)] (hKL : Nat.Prime (Module.finrank K L)) (hKL' : Module.finrank K L ≠ 2) : Module.finrank K L ∣ Fintype.card (ClassGroup (NumberField.RingOfIntegers K))

This is the second part of Hilbert Theorem 94, which states that if L/K is an unramified cyclic finite extension of number fields of odd prime degree, then the degree divides the class number of K.