From 50adcd640d9cb37321b7fa9a11c102091837b3ca Mon Sep 17 00:00:00 2001
From: riccardobrasca <riccardo.brasca@gmail.com>
Date: Mon, 27 Nov 2023 18:16:42 +0100
Subject: [PATCH] progress

---
 FltRegular/NumberTheory/Hilbert90.lean | 81 +++++++++++++++++++++-----
 1 file changed, 65 insertions(+), 16 deletions(-)

diff --git a/FltRegular/NumberTheory/Hilbert90.lean b/FltRegular/NumberTheory/Hilbert90.lean
index 8605172d..57be1c3a 100644
--- a/FltRegular/NumberTheory/Hilbert90.lean
+++ b/FltRegular/NumberTheory/Hilbert90.lean
@@ -2,6 +2,7 @@
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import FltRegular.NumberTheory.AuxLemmas
 import FltRegular.NumberTheory.GaloisPrime
+import Mathlib.Tactic.Widget.Conv
 
 open scoped NumberField nonZeroDivisors
 open FiniteDimensional Finset BigOperators Submodule
@@ -9,19 +10,66 @@ open FiniteDimensional Finset BigOperators Submodule
 variable {K L : Type*} [Field K] [Field L] [NumberField K] [Algebra K L]
 variable [IsGalois K L] [FiniteDimensional K L]
 variable (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ)
+variable {η : L} (hη : Algebra.norm K η = 1)
 
 --This is proved in #8599
 theorem hilbert90 (f : (L ≃ₐ[K] L) → Lˣ)
     (hf : ∀ (g h : (L ≃ₐ[K] L)), f (g * h) = g (f h) * f g) :
     ∃ β : Lˣ, ∀ g : (L ≃ₐ[K] L), f g * Units.map g β = β := by sorry
 
-lemma Hilbert90 (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ)
-    (η : L) (hη : Algebra.norm K η = 1) : ∃ ε : L, η = ε / σ ε := by
-  have hηunit : IsUnit η := sorry
-  let ηu : Lˣ := hηunit.unit
-  -- let E := AlgebraicClosure K
-  -- have := Algebra.norm_eq_prod_embeddings K E η
-  -- rw [hη] at this
+lemma ηunit : IsUnit η := by
+  refine Ne.isUnit (fun h ↦ ?_)
+  simp [h] at hη
+
+noncomputable
+def ηu : Lˣ := (ηunit hη).unit
+
+noncomputable
+def φ := (finEquivZpowers _ (isOfFinOrder_of_finite σ)).symm
+
+variable {σ}
+
+lemma hφ : ∀ (n : ℕ), φ σ ⟨σ ^ n, hσ _⟩ = n % (orderOf σ) := fun n ↦ by
+  simpa [Fin.ext_iff] using
+      @finEquivZpowers_symm_apply _ _ _ (isOfFinOrder_of_finite σ) n ⟨n, by simp⟩
+
+noncomputable
+def cocycle : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ ∏ i in range (φ σ ⟨τ, hσ τ⟩), Units.map (σ ^ i) (ηu hη)
+
+lemma foo {a b : ℕ} (h : a % orderOf σ = b % orderOf σ) :
+    ∏ i in range a, (σ ^ i) (ηu hη) = ∏ i in range b, (σ ^ i) (ηu hη) := by
+  sorry
+
+lemma is_cocycle : ∀ (α β : (L ≃ₐ[K] L)), (cocycle hσ hη) (α * β) =
+    α ((cocycle hσ hη) β) * (cocycle hσ hη) α := by
+  intro α β
+  have hσmon : ∀ x, x ∈ Submonoid.powers σ := by
+    simpa [← mem_powers_iff_mem_zpowers] using hσ
+  obtain ⟨a, ha⟩ := (Submonoid.mem_powers_iff _ _).1 (hσmon α)
+  obtain ⟨b, hb⟩ := (Submonoid.mem_powers_iff _ _).1 (hσmon β)
+  rw [← ha, ← hb, ← pow_add]
+  have Hab := hφ (L := L) hσ (a + b)
+  have Ha := hφ (L := L) hσ a
+  have Hb := hφ (L := L) hσ b
+  simp only [SetLike.coe_sort_coe, Nat.cast_add, Fin.ext_iff, Fin.mod_val, Fin.coe_ofNat_eq_mod,
+    Nat.mod_self, Nat.mod_zero] at Hab Ha Hb
+  simp only [cocycle, SetLike.coe_sort_coe, Units.coe_prod, Units.coe_map, MonoidHom.coe_coe,
+    map_prod]
+  rw [Hab, Ha, Hb, mul_comm]
+  conv =>
+    enter [2, 2, 2, x]
+    rw [← AlgEquiv.mul_apply, ← pow_add]
+  have H : ∀ n, σ ^ (a + n) = σ ^ (a % orderOf σ + n) := fun n ↦ by
+    rw [pow_inj_mod]
+    simp
+  conv =>
+    enter [2, 2, 2, x, 1]
+    rw [H]
+  rw [← prod_range_add (fun (n : ℕ) ↦ (σ ^ n) (ηu hη)) (a % orderOf σ) (b % orderOf σ)]
+  apply foo
+  simp
+
+lemma Hilbert90 : ∃ ε : L, η = ε / σ ε := by
   by_cases hone : orderOf σ = 1
   · suffices finrank K L = 1 by
       obtain ⟨a, ha⟩ := mem_span_singleton.1 <| (eq_top_iff'.1 <|
@@ -33,15 +81,12 @@ lemma Hilbert90 (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ)
     refine ⟨σ, fun τ ↦ ?_⟩
     simp only [orderOf_eq_one_iff.1 hone, Subgroup.zpowers_one_eq_bot, Subgroup.mem_bot] at hσ
     rw [orderOf_eq_one_iff.1 hone, hσ τ]
-  let φ := (finEquivZpowers _ (isOfFinOrder_of_finite σ)).symm
   haveI nezero : NeZero (orderOf σ) :=
     ⟨fun hzero ↦ orderOf_eq_zero_iff.1 hzero (isOfFinOrder_of_finite σ)⟩
-  have hφ : ∀ (n : ℕ), φ ⟨σ ^ n, hσ _⟩ = n % (orderOf σ) := sorry
-  let f : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ ∏ i in range (φ ⟨τ, hσ τ⟩), Units.map (σ ^ i) ηu
-  have hf : ∀ (g h : (L ≃ₐ[K] L)), f (g * h) = g (f h) * f g := sorry
-  have hfσ : f σ = ηu := by
-    rw [← pow_one σ]
-    simp_rw [hφ 1]
+  have hfσ : (cocycle hσ hη) σ = (ηu hη) := by
+    conv =>
+      enter [1, 3]
+      rw [← pow_one σ]
     have : 1 % orderOf σ = 1 := by
       suffices (orderOf σ).pred.pred + 2 = orderOf σ by
         rw [← this]
@@ -52,13 +97,17 @@ lemma Hilbert90 (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ)
       apply hone
       exact Nat.pred_inj (Nat.pos_of_ne_zero nezero.1) zero_lt_one h
     simp [this]
+    have horder :=  hφ hσ 1
+    simp only [SetLike.coe_sort_coe, pow_one] at horder
+    simp only [cocycle, SetLike.coe_sort_coe, horder, this, range_one, prod_singleton, pow_zero]
     rfl
-  obtain ⟨ε, hε⟩ := hilbert90 f hf
+  obtain ⟨ε, hε⟩ := hilbert90 _ (is_cocycle hσ hη)
   use ε
   specialize hε σ
   rw [hfσ] at hε
   nth_rewrite 1 [← hε]
   simp
+  rfl
 
 variable {A B} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Algebra A K]
 variable [Algebra B L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K] [IsDomain A]
@@ -74,7 +123,7 @@ lemma Hilbert90_integral (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowe
   have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
     IsIntegralClosure.isLocalization' A K L B
       (Algebra.isAlgebraic_iff_isIntegral.mpr <| Algebra.IsIntegral.of_finite (R := K) (B := L))
-  obtain ⟨ε, hε⟩ := Hilbert90 σ hσ _ hη
+  obtain ⟨ε, hε⟩ := Hilbert90 hσ hη
   obtain ⟨x, y, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid B A⁰) ε
   obtain ⟨t, ht, ht'⟩ := y.prop
   have : t • IsLocalization.mk' L x y = algebraMap _ _ x