bump

.vscode/settings.json

@@ -7,4 +7,7 @@
     "files.insertFinalNewline": true,
     "files.trimFinalNewlines": true,
     "files.trimTrailingWhitespace": true,
-  }
+    "cSpell.enabledFileTypes": {
+      "lean4": false
+    },
+  }

FltRegular/NumberTheory/Hilbert90.lean

@@ -1,35 +1,24 @@
-
-import Mathlib.RingTheory.SimpleModule
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
-import Mathlib.GroupTheory.OrderOfElement
-import Mathlib.Tactic.Widget.Conv
 import Mathlib.RepresentationTheory.GroupCohomology.Hilbert90
 
 open scoped nonZeroDivisors
-open FiniteDimensional Finset BigOperators Submodule groupCohomology
-
-variable {K L : Type*} [Field K] [Field L] [Algebra K L]
-variable [FiniteDimensional K L]
-variable (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ)
-variable {η : L} (hη : Algebra.norm K η = 1)
+open FiniteDimensional Finset BigOperators Submodule groupCohomology Submonoid
 
-noncomputable
-def ηu : Lˣ := (Ne.isUnit (fun h ↦ by simp [h] at hη) : IsUnit η).unit
-
-noncomputable
-def φ := (finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm
+variable {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
+variable {σ : L ≃ₐ[K] L} (hσ : ∀ x, x ∈ Subgroup.zpowers σ)
+variable {η : Lˣ} (hη : Algebra.norm K η.1 = 1)
 
-variable {σ}
+local notation3 "φ" => (finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm
 
-lemma hφ : ∀ (n : ℕ), φ σ ⟨σ ^ n, hσ _⟩ = n % (orderOf σ) := fun n ↦ by
+lemma hφ : ∀ (n : ℕ), φ ⟨σ ^ n, hσ _⟩ = n % (orderOf σ) := fun n ↦ by
   simpa [Fin.ext_iff] using finEquivZPowers_symm_apply _ (isOfFinOrder_of_finite σ) n
 
+variable (η) in
 noncomputable
-def cocycle : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ ∏ i in range (φ σ ⟨τ, hσ τ⟩), Units.map (σ ^ i) (ηu hη)
+def cocycle : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ ∏ i in range (φ ⟨τ, hσ τ⟩), Units.map (σ ^ i) η
 
-include hσ in
-lemma aux1 [IsGalois K L] {a: ℕ} (h : a % orderOf σ = 0) :
-    ∏ i in range a, (σ ^ i) (ηu hη) = 1 := by
+include hσ hη in
+lemma aux1 [IsGalois K L] {a: ℕ} (h : a % orderOf σ = 0) : ∏ i in range a, (σ ^ i) η = 1 := by
   obtain ⟨n, hn⟩ := Nat.dvd_iff_mod_eq_zero.2 h
   rw [hn]
   revert a
@@ -39,32 +28,31 @@ lemma aux1 [IsGalois K L] {a: ℕ} (h : a % orderOf σ = 0) :
     intro a _ _
     rw [Nat.mul_succ, prod_range_add, ih (Nat.mul_mod_right (orderOf σ) n) rfl, one_mul]
     simp only [pow_add, pow_mul, pow_orderOf_eq_one, one_pow, one_mul]
-    have := Algebra.norm_eq_prod_automorphisms K η
+    have := Algebra.norm_eq_prod_automorphisms K η.1
     simp only [hη, map_one] at this
     convert this.symm
-    refine prod_bij (fun (n : ℕ) (_ : n ∈ range (orderOf σ)) ↦ σ ^ n) (by simp)
+    refine prod_bij (fun n (_ : n ∈ range (orderOf σ)) ↦ σ ^ n) (by simp)
       (fun a ha b hb hab ↦ ?_) (fun τ _ ↦ ?_) (fun _ _ ↦ by rfl)
-    · rwa [pow_inj_mod, Nat.mod_eq_of_lt (Finset.mem_range.1 ha),
-        Nat.mod_eq_of_lt (Finset.mem_range.1 hb)] at hab
+    · rwa [pow_inj_mod, Nat.mod_eq_of_lt (mem_range.1 ha),
+        Nat.mod_eq_of_lt (mem_range.1 hb)] at hab
     · refine ⟨(finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩, by simp, ?_⟩
       have := Equiv.symm_apply_apply (finEquivZPowers _ (isOfFinOrder_of_finite σ)).symm ⟨τ, hσ τ⟩
       simp only [SetLike.coe_sort_coe, Equiv.symm_symm, ← Subtype.coe_inj] at this ⊢
       rw [← this]
       simp only [SetLike.coe_sort_coe, Subtype.coe_eta, Equiv.symm_apply_apply]
       rfl
 
-include hσ in
+include hσ hη in
 lemma aux2 [IsGalois K L] {a b : ℕ} (h : a % orderOf σ = b % orderOf σ) :
-    ∏ i in range a, (σ ^ i) (ηu hη) = ∏ i in range b, (σ ^ i) (ηu hη) := by
+    ∏ i in range a, (σ ^ i) η = ∏ i in range b, (σ ^ i) η := by
   wlog hab : b ≤ a generalizing a b
   · exact (this h.symm (not_le.1 hab).le).symm
   obtain ⟨c, hc⟩ := Nat.dvd_iff_mod_eq_zero.2 (Nat.sub_mod_eq_zero_of_mod_eq h)
   rw [Nat.sub_eq_iff_eq_add hab] at hc
-  rw [hc, prod_range_add]
-  rw [aux1 hσ hη (Nat.mul_mod_right (orderOf σ) c), one_mul]
+  rw [hc, prod_range_add, aux1 hσ hη (Nat.mul_mod_right (orderOf σ) c), one_mul]
   simp [pow_add, pow_mul, pow_orderOf_eq_one]
 
-lemma cocycle_spec (hone : orderOf σ ≠ 1) : (cocycle hσ hη) σ = (ηu hη) := by
+lemma cocycle_spec (hone : orderOf σ ≠ 1) : (cocycle hσ η) σ = η := by
   haveI nezero : NeZero (orderOf σ) :=
     ⟨fun hzero ↦ orderOf_eq_zero_iff.1 hzero (isOfFinOrder_of_finite σ)⟩
   conv =>
@@ -85,17 +73,17 @@ lemma cocycle_spec (hone : orderOf σ ≠ 1) : (cocycle hσ hη) σ = (ηu hη)
   simp only [cocycle, SetLike.coe_sort_coe, horder, this, range_one, prod_singleton, pow_zero]
   rfl
 
-lemma is_cocycle_aux [IsGalois K L] : ∀ (α β : (L ≃ₐ[K] L)), (cocycle hσ hη) (α * β) =
-    α ((cocycle hσ hη) β) * (cocycle hσ hη) α := by
+include hη in
+lemma is_cocycle_aux [IsGalois K L] : ∀ (α β : (L ≃ₐ[K] L)), (cocycle hσ η) (α * β) =
+    α ((cocycle hσ η) β) * (cocycle 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 β)
+  have hσmon : ∀ x, x ∈ powers σ := by simpa [← mem_powers_iff_mem_zpowers] using hσ
+  obtain ⟨a, ha⟩ := (mem_powers_iff _ _).1 (hσmon α)
+  obtain ⟨b, hb⟩ := (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
+  have Hab := hφ hσ (a + b)
+  have Ha := hφ hσ a
+  have Hb := hφ 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, cocycle, Units.coe_prod, Units.coe_map, MonoidHom.coe_coe,
     map_prod] at Hab Ha Hb ⊢
@@ -104,10 +92,11 @@ lemma is_cocycle_aux [IsGalois K L] : ∀ (α β : (L ≃ₐ[K] L)), (cocycle h
   conv =>
     enter [2, 2, 2, x]
     rw [← AlgEquiv.mul_apply, ← pow_add, H]
-  rw [← prod_range_add (fun (n : ℕ) ↦ (σ ^ n) (ηu hη)) (a % orderOf σ) (b % orderOf σ)]
+  rw [← prod_range_add (fun (n : ℕ) ↦ (σ ^ n) η) (a % orderOf σ) (b % orderOf σ)]
   simpa using aux2 hσ hη (by simp)
 
-lemma is_cocycle [IsGalois K L] : IsMulOneCocycle (cocycle hσ hη) := by
+include hη in
+lemma is_cocycle [IsGalois K L] : IsMulOneCocycle (cocycle hσ η) := by
   intro α β
   simp [← Units.eq_iff, is_cocycle_aux hσ hη α β]
 
@@ -129,25 +118,27 @@ lemma Hilbert90 [IsGalois K L] : ∃ ε : L, η = ε / σ ε := by
   simp only [map_inv₀, div_inv_eq_mul]
   specialize hε σ
   nth_rewrite 2 [← inv_inv ε] at hε
-  rw [div_inv_eq_mul, cocycle_spec hσ hη hone, mul_inv_eq_iff_eq_mul, mul_comm,
+  rw [div_inv_eq_mul, cocycle_spec hσ hone, mul_inv_eq_iff_eq_mul, mul_comm,
     ← Units.eq_iff] at hε
   simp only [AlgEquiv.smul_units_def, Units.coe_map, MonoidHom.coe_coe, Units.val_mul] at hε
   symm
   rw [inv_mul_eq_iff_eq_mul₀ ε.ne_zero, hε]
-  rfl
 
 variable {A B : Type*} [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]
 variable [IsIntegralClosure B A L]
 
-lemma Hilbert90_integral [IsGalois K L] (σ : L ≃ₐ[K] L)
-    (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (η : B) (hη : Algebra.norm K (algebraMap B L η) = 1) :
+include hσ in
+lemma Hilbert90_integral [IsGalois K L] {η : B} (hη : Algebra.norm K (algebraMap B L η) = 1) :
     ∃ ε : B, ε ≠ 0 ∧ η * galRestrict A K L B σ ε = ε := by
-  haveI : NoZeroSMulDivisors A L := by
+  have : NoZeroSMulDivisors A L := by
     rw [NoZeroSMulDivisors.iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]
     exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
   have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
     IsIntegralClosure.isLocalization A K L B
+  let η' : Lˣ := IsUnit.unit (a := (algebraMap B L η)) (isUnit_iff_ne_zero.2
+    (fun h ↦ by simp [h] at hη))
+  replace hη : Algebra.norm K η'.1 = 1 := hη
   obtain ⟨ε, hε⟩ := Hilbert90 hσ hη
   obtain ⟨x, y, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid B A⁰) ε
   obtain ⟨t, ht, ht'⟩ := y.prop
@@ -167,7 +158,7 @@ lemma Hilbert90_integral [IsGalois K L] (σ : L ≃ₐ[K] L)
     apply IsIntegralClosure.algebraMap_injective B A L
     rw [map_mul, ← hε]
     congr 1
-    exact algebraMap_galRestrictHom_apply A K L B σ x
+    · exact algebraMap_galRestrictHom_apply A K L B σ x
     · intro e
       rw [(map_eq_zero _).mp e, zero_div] at hε
       rw [hε, Algebra.norm_zero] at hη

FltRegular/NumberTheory/Hilbert92.lean

@@ -626,7 +626,7 @@ local instance : Module.Free ℤ G := Module.free_of_finite_type_torsion_free'
 noncomputable
 def unitlifts (S : systemOfUnits p G (NumberField.Units.rank k + 1))  :
     Fin (NumberField.Units.rank k + 1) → Additive (𝓞 K)ˣ :=
-  fun i ↦ Additive.ofMul (Additive.toMul (S.units i).out').out'
+  fun i ↦ Additive.ofMul (Additive.toMul (S.units i).out).out
 
 lemma unitlifts_spec (S : systemOfUnits p G (NumberField.Units.rank k + 1)) (i) :
     mkG (Additive.toMul <| unitlifts p hp hKL σ hσ S i) = S.units i := by

FltRegular/NumberTheory/Hilbert94.lean

@@ -50,7 +50,7 @@ theorem exists_not_isPrincipal_and_isPrincipal_map_aux
     (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η
+  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 _

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "485efbc439ee0ebdeae8afb0acd24a5e82e2f771",
+   "rev": "a822446d61ad7e7f5e843365c7041c326553050a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e948d859635b67a2d40b53d10bcf906226e2a460",
+   "rev": "840e02ce2768e06de7ced0a624444746590e9d99",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
+   "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7b6a56e8e4fcf54d3834b225b9814a7c9e4d4bda",
+   "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",