From b46cd0086bda34ae20eb33660cc92bca3147dcd3 Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Mon, 4 Dec 2023 14:34:55 +0000 Subject: [PATCH] zeta fix --- FltRegular/NumberTheory/Hilbert92.lean | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 753c420d..ebfa4e5a 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -754,13 +754,18 @@ lemma Hilbert92ish (hp : Nat.Prime p) (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) + by_cases H : ∀ ε : (𝓞 K)ˣ, (algebraMap k K ζ^((p : ℤ)^(h-1))) ≠ ε / (σ ε : K) + + sorry 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σ - have NE_p_pow : (Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom NE) = E ^ (p : ℕ) := by sorry + have NE_p_pow : (Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom NE) = E ^ (p : ℕ) := by + have Hp: E^(p : ℕ) = σ E^(p: ℕ) := by sorry + + sorry let H := unitlifts p hp hKL σ hσ S let N : Fin (r + 1) → Additive (𝓞 k)ˣ := fun e => Additive.ofMul (Units.map (RingOfIntegers.norm k)) (Additive.toMul (H e)) @@ -787,6 +792,7 @@ lemma Hilbert92ish (hp : Nat.Prime p) rw [← Units.coe_val_inv, norm_map_inv] simp only [coe_zpow', Units.coe_map, MonoidHom.coe_coe] sorry + sorry /-