From ef63532470d3c6aacf70614f568cd38a850077df Mon Sep 17 00:00:00 2001 From: erd1 Date: Sun, 3 Dec 2023 22:19:08 +0800 Subject: [PATCH] extract hilbert94 --- FltRegular/NumberTheory/Hilbert92.lean | 39 +++--- FltRegular/NumberTheory/Hilbert94.lean | 132 ++++++++++++++++++ FltRegular/NumberTheory/InfinitePlace.lean | 28 ++-- .../KummersLemma/KummersLemma.lean | 107 ++------------ 4 files changed, 185 insertions(+), 121 deletions(-) create mode 100644 FltRegular/NumberTheory/Hilbert94.lean diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 8eee9001..4f0f042a 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -10,7 +10,7 @@ open scoped NumberField nonZeroDivisors open FiniteDimensional open NumberField -variable (p : ℕ+) {K : Type*} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] +variable (p : ℕ+) {K : Type*} [Field K] [NumberField K] -- [IsCyclotomicExtension {p} ℚ K] variable {k : Type*} [Field k] [NumberField k] (hp : Nat.Prime p) open FiniteDimensional BigOperators Finset @@ -168,7 +168,7 @@ end fundamentalSystemOfUnits section application variable - [Algebra k K] [IsGalois k K] [FiniteDimensional k K] -- [IsCyclic (K ≃ₐ[k] K)] -- technically redundant but useful + [Algebra k K] [IsGalois k K] [FiniteDimensional k K] [InfinitePlace.IsUnramified k K] (hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) def RelativeUnits (k K : Type*) [Field k] [Field K] [Algebra k K] := @@ -381,17 +381,16 @@ local instance : Module.Finite ℤ G := Module.Finite.of_surjective local instance : Module.Free ℤ G := Module.free_of_finite_type_torsion_free' -lemma NumberField.Units.rank_of_odd (h : Odd (finrank k K)) : +lemma NumberField.Units.rank_of_isUnramified : NumberField.Units.rank K = (finrank k K) * NumberField.Units.rank k + (finrank k K) - 1 := by delta NumberField.Units.rank - rw [InfinitePlace.card_eq_of_odd_fintype h, mul_comm, mul_tsub, mul_one, tsub_add_cancel_of_le] + rw [InfinitePlace.card_eq_of_isUnramified (k := k), + mul_comm, mul_tsub, mul_one, tsub_add_cancel_of_le] refine (mul_one _).symm.trans_le (Nat.mul_le_mul_left _ ?_) rw [Nat.one_le_iff_ne_zero, ← Nat.pos_iff_ne_zero, Fintype.card_pos_iff] infer_instance -variable (hp2 : p ≠ 2) - -lemma finrank_G (hp2 : p ≠ 2) : finrank ℤ G = (Units.rank k + 1) * (↑p - 1) := by +lemma finrank_G : finrank ℤ G = (Units.rank k + 1) * (↑p - 1) := by rw [← Submodule.torsion_int] refine (FiniteDimensional.finrank_quotient_of_le_torsion _ le_rfl).trans ?_ show finrank ℤ (Additive (𝓞 K)ˣ ⧸ AddSubgroup.toIntSubmodule (Subgroup.toAddSubgroup @@ -399,12 +398,9 @@ lemma finrank_G (hp2 : p ≠ 2) : finrank ℤ G = (Units.rank k + 1) * (↑p - 1 rw [FiniteDimensional.finrank_quotient] show _ - finrank ℤ (LinearMap.range <| AddMonoidHom.toIntLinearMap <| MonoidHom.toAdditive <| Units.map (algebraMap ↥(𝓞 k) ↥(𝓞 K) : ↥(𝓞 k) →* ↥(𝓞 K))) = _ - have hodd : Odd (finrank k K) - · rw [hKL]; exact hp.odd_of_ne_two (PNat.coe_injective.ne hp2) rw [LinearMap.finrank_range_of_inj, NumberField.Units.finrank_eq, NumberField.Units.finrank_eq, - NumberField.Units.rank_of_odd hodd, add_mul, one_mul, mul_tsub, mul_one, mul_comm, - add_tsub_assoc_of_le, - tsub_add_eq_add_tsub, hKL] + NumberField.Units.rank_of_isUnramified (k := k), add_mul, one_mul, mul_tsub, mul_one, mul_comm, + add_tsub_assoc_of_le, tsub_add_eq_add_tsub, hKL] · exact (mul_one _).symm.trans_le (Nat.mul_le_mul_left _ hp.one_lt.le) · exact hKL ▸ hp.one_lt.le · intros i j e @@ -416,7 +412,7 @@ lemma finrank_G (hp2 : p ≠ 2) : finrank ℤ G = (Units.rank k + 1) * (↑p - 1 lemma Hilbert91ish : ∃ S : systemOfUnits p G (NumberField.Units.rank k + 1), S.IsFundamental := fundamentalSystemOfUnits.existence p hp G (NumberField.Units.rank k + 1) - (finrank_G p hp hKL σ hσ hp2) + (finrank_G p hp hKL σ hσ) noncomputable @@ -626,9 +622,10 @@ lemma h_exists' : ∃ (h : ℕ) (ζ : (𝓞 k)ˣ), -- obtain ⟨ζ, hζ⟩ := this -- refine ⟨n, hζ.unit', hζ, by simpa only [h] using Nat.find_spec H⟩ -lemma Hilbert92ish - [Algebra k K] [IsGalois k K] [FiniteDimensional k K] [IsCyclic (K ≃ₐ[k] K)] - (hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (hp : Nat.Prime p) : +lemma Hilbert92ish (hp : Nat.Prime p) + [Algebra k K] [IsGalois k K] [FiniteDimensional k K] [InfinitePlace.IsUnramified k K] + [IsCyclic (K ≃ₐ[k] K)] + (hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) : ∃ η : (𝓞 K)ˣ, Algebra.norm k (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := by obtain ⟨h, ζ, hζ⟩ := h_exists' p (k := k) hp by_cases H : ∀ ε : (𝓞 K)ˣ, (algebraMap k K ζ) ≠ ε / (σ ε : K) @@ -636,7 +633,7 @@ lemma Hilbert92ish simp only [ne_eq, not_forall, not_not] at H obtain ⟨ E, hE⟩:= H let NE := Units.map (RingOfIntegers.norm k ) E - obtain ⟨S, hS⟩ := Hilbert91ish p (K := K) (k := k) hp hKL σ hσ hp2 + obtain ⟨S, hS⟩ := Hilbert91ish p (K := K) (k := k) hp hKL σ hσ have NE_p_pow : ((Units.map (algebraMap (𝓞 k) (𝓞 K) ).toMonoidHom ) NE) = E^(p : ℕ) := by sorry let H := unitlifts p hp hKL σ hσ S let N : Fin (NumberField.Units.rank k + 1) → Additive (𝓞 k)ˣ := @@ -719,9 +716,11 @@ lemma Hilbert92ish lemma Hilbert92 - [Algebra k K] [IsGalois k K] [FiniteDimensional k K] - (hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) : - ∃ η : (𝓞 K)ˣ, Algebra.norm k (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := by sorry + [Algebra k K] [IsGalois k K] [FiniteDimensional k K] [InfinitePlace.IsUnramified k K] + (hKL : Nat.Prime (finrank k K)) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) : + ∃ η : (𝓞 K)ˣ, Algebra.norm k (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := + letI : IsCyclic (K ≃ₐ[k] K) := ⟨σ, hσ⟩ + Hilbert92ish ⟨finrank k K, finrank_pos⟩ hKL rfl σ hσ end application diff --git a/FltRegular/NumberTheory/Hilbert94.lean b/FltRegular/NumberTheory/Hilbert94.lean new file mode 100644 index 00000000..7eeeb598 --- /dev/null +++ b/FltRegular/NumberTheory/Hilbert94.lean @@ -0,0 +1,132 @@ +import FltRegular.NumberTheory.Unramified +import FltRegular.NumberTheory.Hilbert92 +import FltRegular.NumberTheory.Hilbert90 +import FltRegular.NumberTheory.IdealNorm +import FltRegular.NumberTheory.RegularPrimes + +open scoped NumberField + +variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K] +variable [Fintype (ClassGroup (𝓞 K))] + +attribute [-instance] instCoeOut + +open Polynomial + +variable {L} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] +variable (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (hKL : FiniteDimensional.finrank K L = p) + +variable {A B} [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] + +lemma comap_span_galRestrict_eq_of_cyclic (β : B) (η : Bˣ) (hβ : η * (galRestrict A K B L σ) β = β) + (σ' : L ≃ₐ[K] L) : + (Ideal.span {β}).comap (galRestrict A K B L σ') = Ideal.span {β} := by + suffices : (Ideal.span {β}).map + (galRestrict A K B L σ'⁻¹).toRingEquiv.toRingHom = Ideal.span {β} + · rwa [RingEquiv.toRingHom_eq_coe, Ideal.map_comap_of_equiv, map_inv] at this + apply_fun (Ideal.span {·}) at hβ + rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_eq_top.mpr η.isUnit, + ← Ideal.one_eq_top, one_mul, ← Set.image_singleton, ← Ideal.map_span] at hβ + change Ideal.map (galRestrict A K B L σ : B →+* B) _ = _ at hβ + generalize σ'⁻¹ = σ' + obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ') + rw [map_pow] + induction n with + | zero => + simp only [Nat.zero_eq, pow_zero, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe] + exact Ideal.map_id _ + | succ n IH => + simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, pow_succ'] at IH ⊢ + conv_lhs at IH => rw [← hβ, Ideal.map_map] + exact IH + +open FiniteDimensional in +theorem exists_not_isPrincipal_and_isPrincipal_map_aux + [IsDedekindDomain A] [IsUnramified 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, ¬I.IsPrincipal ∧ (I.map (algebraMap A B)).IsPrincipal := by + obtain ⟨β, hβ_zero, hβ⟩ := Hilbert90_integral (A := A) (B := B) σ hσ η hη + haveI : IsDomain B := + (IsIntegralClosure.equiv A B L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L) + have hβ' := comap_map_eq_of_isUnramified K L _ + (comap_span_galRestrict_eq_of_cyclic σ hσ (A := A) (B := B) β η hβ) + refine ⟨(Ideal.span {β}).comap (algebraMap A B), ?_, ?_⟩ + · rintro ⟨⟨γ, hγ : _ = Ideal.span _⟩⟩ + rw [hγ, Ideal.map_span, Set.image_singleton, Ideal.span_singleton_eq_span_singleton] at hβ' + obtain ⟨a, rfl⟩ := hβ' + rw [map_mul, AlgEquiv.commutes, mul_left_comm, (mul_right_injective₀ _).eq_iff] at hβ + apply hη' + use a + conv_rhs => enter [1]; rw [← hβ] + rw [map_mul, ← AlgHom.coe_coe σ, ← algebraMap_galRestrictHom_apply A K B L σ a] + refine (mul_div_cancel _ ?_).symm + · rw [ne_eq, (injective_iff_map_eq_zero' _).mp (IsIntegralClosure.algebraMap_injective B A L), + (injective_iff_map_eq_zero' _).mp (galRestrict A K B L σ).injective] + exact a.isUnit.ne_zero + · exact (mul_ne_zero_iff.mp hβ_zero).1 + · rw [hβ'] + exact ⟨⟨_, rfl⟩⟩ + +attribute [local instance 2000] NumberField.inst_ringOfIntegersAlgebra Algebra.toSMul Algebra.toModule + +attribute [local instance] FractionRing.liftAlgebra + +open FiniteDimensional (finrank) + +theorem Ideal.isPrincipal_pow_finrank_of_isPrincipal_map [IsDedekindDomain A] (I : Ideal A) + (hI : (I.map (algebraMap A B)).IsPrincipal) : (I ^ finrank K L).IsPrincipal := by + haveI : IsDomain B := + (IsIntegralClosure.equiv A B L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L) + haveI := IsIntegralClosure.isNoetherian A K L B + haveI := IsIntegralClosure.isDedekindDomain A K L B + haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B + have hAB : Function.Injective (algebraMap A B) + · refine Function.Injective.of_comp (f := algebraMap B L) ?_ + rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A K L] + exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _) + rw [← NoZeroSMulDivisors.iff_algebraMap_injective] at hAB + letI : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra _ _ + have : IsScalarTower A (FractionRing A) (FractionRing B) := + FractionRing.isScalarTower_liftAlgebra _ _ + have H : RingHom.comp (algebraMap (FractionRing A) (FractionRing B)) + ↑(FractionRing.algEquiv A K).symm.toRingEquiv = + RingHom.comp ↑(FractionRing.algEquiv B L).symm.toRingEquiv (algebraMap K L) + · apply IsLocalization.ringHom_ext (nonZeroDivisors A) + ext + simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe, + AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes, + ← IsScalarTower.algebraMap_apply] + rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply] + have : IsSeparable (FractionRing A) (FractionRing B) := IsSeparable_of_equiv_equiv _ _ H + have hLK : finrank (FractionRing A) (FractionRing B) = finrank K L := + (FiniteDimensional.finrank_of_equiv_equiv _ _ H).symm + rw [← hLK, ← Ideal.spanIntNorm_map, ← (I.map (algebraMap A B)).span_singleton_generator, + Ideal.spanIntNorm_singleton] + exact ⟨⟨_, rfl⟩⟩ + +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] [IsUnramified ↥(𝓞 K) ↥(𝓞 L)] [IsCyclic (L ≃ₐ[K] L)] + [NumberField.InfinitePlace.IsUnramified K L] (hKL : Nat.Prime (finrank K L)) : + ∃ I : Ideal (𝓞 K), ¬I.IsPrincipal ∧ (I.map (algebraMap ↥(𝓞 K) ↥(𝓞 L))).IsPrincipal := by + obtain ⟨⟨σ, hσ⟩⟩ := ‹IsCyclic (L ≃ₐ[K] L)› + obtain ⟨η, hη, hη'⟩ := Hilbert92 hKL σ hσ + exact exists_not_isPrincipal_and_isPrincipal_map_aux (A := ↥(𝓞 K)) σ hσ η hη (not_exists.mpr hη') + +/-- This is **Hilbert Theorem 94**, which states that if `L/K` is an unramified + cyclic finite extension of number fields of prime degree, + then the degree divides the class number of `K`. -/ +theorem dvd_card_classGroup_of_isUnramified_isCyclic (K L : Type*) + [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] + [FiniteDimensional K L] [IsGalois K L] [IsUnramified ↥(𝓞 K) ↥(𝓞 L)] [IsCyclic (L ≃ₐ[K] L)] + [NumberField.InfinitePlace.IsUnramified K L] (hKL : Nat.Prime (finrank K L)) : + finrank K L ∣ Fintype.card (ClassGroup ↥(𝓞 K)) := by + obtain ⟨I, hI, hI'⟩ := exists_not_isPrincipal_and_isPrincipal_map K L hKL + letI := Fact.mk hKL + rw [← Int.ofNat_dvd, (Nat.prime_iff_prime_int.mp hKL).irreducible.dvd_iff_not_coprime, + Nat.isCoprime_iff_coprime] + exact fun h ↦ hI (IsPrincipal_of_IsPrincipal_pow_of_Coprime _ _ h _ + (Ideal.isPrincipal_pow_finrank_of_isPrincipal_map _ hI')) diff --git a/FltRegular/NumberTheory/InfinitePlace.lean b/FltRegular/NumberTheory/InfinitePlace.lean index 698881ba..1378506d 100644 --- a/FltRegular/NumberTheory/InfinitePlace.lean +++ b/FltRegular/NumberTheory/InfinitePlace.lean @@ -329,16 +329,28 @@ lemma InfinitePlace.card_eq_card_isRamifiedIn [NumberField k] [IsGalois k K] : filter_eq_empty_iff, not_forall, not_not] at H rw [Nat.div_mul_cancel H.choose_spec.even_finrank.two_dvd] -lemma InfinitePlace.card_eq_of_forall_not_isRamified [NumberField k] [IsGalois k K] - (h : ∀ w : InfinitePlace K, ¬ IsRamified k w) : +class InfinitePlace.IsUnramified (k K) [Field k] [Field K] [Algebra k K] : Prop where + not_isRamified : ∀ w : InfinitePlace K, ¬ IsRamified k w + +lemma InfinitePlace.not_isRamified (k) {K} [Field k] [Field K] [Algebra k K] [IsUnramified k K] + (w : InfinitePlace K) : ¬ IsRamified k w := IsUnramified.not_isRamified w + +lemma InfinitePlace.not_isRamifiedIn {k} (K) [Field k] [Field K] [Algebra k K] [IsUnramified k K] + [IsGalois k K] (w : InfinitePlace k) : ¬ w.IsRamifiedIn K := IsUnramified.not_isRamified _ + +lemma InfinitePlace.isUnramified_of_odd_card_aut (h : Odd (Fintype.card <| K ≃ₐ[k] K)) : + IsUnramified k K where + not_isRamified _ hw := Nat.odd_iff_not_even.mp h hw.even_card_aut + +lemma InfinitePlace.isUramified_of_odd_finrank [IsGalois k K] (h : Odd (finrank k K)) : + IsUnramified k K where + not_isRamified _ hw := Nat.odd_iff_not_even.mp h hw.even_finrank + +lemma InfinitePlace.card_eq_of_isUnramified [NumberField k] [IsGalois k K] + [IsUnramified k K] : Fintype.card (InfinitePlace K) = Fintype.card (InfinitePlace k) * finrank k K := by rw [card_eq_card_isRamifiedIn (k := k) (K := K), Finset.card_eq_zero.mpr, zero_mul, tsub_zero] simp only [Finset.mem_univ, forall_true_left, Finset.filter_eq_empty_iff] - exact fun x hx ↦ h _ hx - -lemma InfinitePlace.card_eq_of_odd_fintype [NumberField k] [IsGalois k K] - (h : Odd (finrank k K)) : - Fintype.card (InfinitePlace K) = Fintype.card (InfinitePlace k) * finrank k K := - card_eq_of_forall_not_isRamified (fun _ hw ↦ Nat.odd_iff_not_even.mp h hw.even_finrank) + exact InfinitePlace.not_isRamifiedIn K end NumberField diff --git a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean index 7e4f7ecb..d0515c37 100644 --- a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean +++ b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean @@ -1,7 +1,5 @@ import FltRegular.NumberTheory.KummersLemma.Field -import FltRegular.NumberTheory.Hilbert92 -import FltRegular.NumberTheory.Hilbert90 -import FltRegular.NumberTheory.IdealNorm +import FltRegular.NumberTheory.Hilbert94 open scoped NumberField @@ -19,88 +17,6 @@ variable {L} [Field L] [Algebra K L] [FiniteDimensional K L] variable [IsSplittingField K L (X ^ (p : ℕ) - C (u : K))] variable (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) -variable {A B} [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] - -lemma comap_span_galRestrict_eq_of_cyclic (β : B) (η : Bˣ) (hβ : η * (galRestrict A K B L σ) β = β) - (σ' : L ≃ₐ[K] L) : - (Ideal.span {β}).comap (galRestrict A K B L σ') = Ideal.span {β} := by - suffices : (Ideal.span {β}).map - (galRestrict A K B L σ'⁻¹).toRingEquiv.toRingHom = Ideal.span {β} - · rwa [RingEquiv.toRingHom_eq_coe, Ideal.map_comap_of_equiv, map_inv] at this - apply_fun (Ideal.span {·}) at hβ - rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_eq_top.mpr η.isUnit, - ← Ideal.one_eq_top, one_mul, ← Set.image_singleton, ← Ideal.map_span] at hβ - change Ideal.map (galRestrict A K B L σ : B →+* B) _ = _ at hβ - generalize σ'⁻¹ = σ' - obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ') - rw [map_pow] - induction n with - | zero => - simp only [Nat.zero_eq, pow_zero, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe] - exact Ideal.map_id _ - | succ n IH => - simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, pow_succ'] at IH ⊢ - conv_lhs at IH => rw [← hβ, Ideal.map_map] - exact IH - -open FiniteDimensional in -theorem exists_units_eq_div_root_of_isUnramified - [IsDedekindDomain A] [IsUnramified A B] [Fintype (ClassGroup A)] - (Hp : Nat.Coprime p <| Fintype.card <| ClassGroup A) (η : Bˣ) - (hη : Algebra.norm K (algebraMap B L η) = 1) : - ∃ α : Bˣ, algebraMap B L η = (algebraMap B L α) / σ (algebraMap B L α) := by - haveI := isGalois_of_isSplittingField_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ - (X_pow_sub_C_irreducible_of_prime hpri.out hu) L - obtain ⟨β, hβ_zero, hβ⟩ := Hilbert90_integral (A := A) (B := B) σ hσ η hη - haveI : IsDomain B := - (IsIntegralClosure.equiv A B L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L) - haveI := IsIntegralClosure.isNoetherian A K L B - haveI := IsIntegralClosure.isDedekindDomain A K L B - haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B - have hAB : Function.Injective (algebraMap A B) - · refine Function.Injective.of_comp (f := algebraMap B L) ?_ - rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A K L] - exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _) - rw [← NoZeroSMulDivisors.iff_algebraMap_injective] at hAB - letI : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra _ _ - have : IsScalarTower A (FractionRing A) (FractionRing B) := - FractionRing.isScalarTower_liftAlgebra _ _ - have H : RingHom.comp (algebraMap (FractionRing A) (FractionRing B)) - ↑(FractionRing.algEquiv A K).symm.toRingEquiv = - RingHom.comp ↑(FractionRing.algEquiv B L).symm.toRingEquiv (algebraMap K L) - · apply IsLocalization.ringHom_ext (nonZeroDivisors A) - ext - simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe, - AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes, - ← IsScalarTower.algebraMap_apply] - rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply] - have : IsSeparable (FractionRing A) (FractionRing B) := IsSeparable_of_equiv_equiv _ _ H - have hLK : finrank (FractionRing A) (FractionRing B) = finrank K L := - (FiniteDimensional.finrank_of_equiv_equiv _ _ H).symm - have hβ' := comap_map_eq_of_isUnramified K L _ - (comap_span_galRestrict_eq_of_cyclic σ hσ (A := A) (B := B) β η hβ) - obtain ⟨⟨γ, hγ : _ = Ideal.span _⟩⟩ : ((Ideal.span {β}).comap (algebraMap A B)).IsPrincipal - · apply_fun Ideal.spanIntNorm A at hβ' - rw [Ideal.spanIntNorm_map, Ideal.spanIntNorm_singleton, hLK] at hβ' - letI : Fact (Nat.Prime p) := hpri - apply IsPrincipal_of_IsPrincipal_pow_of_Coprime _ p Hp - rw [← finrank_of_isSplittingField_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ - (X_pow_sub_C_irreducible_of_prime hpri.out hu) L, hβ'] - exact ⟨⟨_, rfl⟩⟩ - rw [hγ, Ideal.map_span, Set.image_singleton, Ideal.span_singleton_eq_span_singleton] at hβ' - obtain ⟨a, rfl⟩ := hβ' - rw [map_mul, AlgEquiv.commutes, mul_left_comm, (mul_right_injective₀ _).eq_iff] at hβ - use a - conv_rhs => enter [1]; rw [← hβ] - rw [map_mul, ← AlgHom.coe_coe σ, ← algebraMap_galRestrictHom_apply A K B L σ a] - refine (mul_div_cancel _ ?_).symm - · rw [ne_eq, (injective_iff_map_eq_zero' _).mp (IsFractionRing.injective B L), - (injective_iff_map_eq_zero' _).mp (galRestrict A K B L σ).injective] - exact a.isUnit.ne_zero - · exact (mul_ne_zero_iff.mp hβ_zero).1 - theorem false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne (u : (𝓞 K)ˣ) (hcong : (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (↑u : 𝓞 K) - 1) (hu : ∀ v : K, v ^ (p : ℕ) ≠ u) : False := by @@ -112,15 +28,20 @@ theorem false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne (u : (𝓞 K)ˣ) (X_pow_sub_C_irreducible_of_prime hpri.out hu) L have := Polynomial.IsSplittingField.finiteDimensional L (Polynomial.X ^ (p : ℕ) - Polynomial.C (u : K)) - obtain ⟨⟨σ, hσ⟩⟩ := - isCyclic_of_isSplittingField_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ + have := isCyclic_of_isSplittingField_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ (X_pow_sub_C_irreducible_of_prime hpri.out hu) L - obtain ⟨η, hη, hη'⟩ := Hilbert92 p (finrank_of_isSplittingField_X_pow_sub_C - ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ (X_pow_sub_C_irreducible_of_prime hpri.out hu) L) σ hσ - haveI := KummersLemma.isUnramified hp hζ u hcong hu L - obtain ⟨α, hα⟩ := - exists_units_eq_div_root_of_isUnramified hζ u hu σ hσ (A := 𝓞 K) (B := 𝓞 L) hreg η hη - exact hη' α hα + have : CharZero L := charZero_of_injective_algebraMap (algebraMap K L).injective + have : FiniteDimensional ℚ L := Module.Finite.trans K L + have : NumberField L := ⟨⟩ + have hKL : FiniteDimensional.finrank K L = p := (finrank_of_isSplittingField_X_pow_sub_C + ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ (X_pow_sub_C_irreducible_of_prime hpri.out hu) L) + have := KummersLemma.isUnramified hp hζ u hcong hu L + have := NumberField.InfinitePlace.isUramified_of_odd_finrank (k := K) (K := L) + (hKL.symm ▸ Nat.Prime.odd_of_ne_two hpri.out (PNat.coe_injective.ne hp)) + have := dvd_card_classGroup_of_isUnramified_isCyclic K L (hKL.symm ▸ hpri.out) + rw [hKL, ← Int.ofNat_dvd, (Nat.prime_iff_prime_int.mp hpri.out).irreducible.dvd_iff_not_coprime, + Nat.isCoprime_iff_coprime] at this + exact this (by convert hreg) -- Let 𝑝 be a regular prime (i.e. an odd prime which does not divide the class number off -- the 𝑝-th cyclotomic field) and 𝜉 a primitive 𝑝-th root of unity;