bump

Author: riccardobrasca

FltRegular.lean

@@ -10,7 +10,6 @@ import FltRegular.NumberTheory.Cyclotomic.CyclRat
 import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import FltRegular.NumberTheory.CyclotomicRing
-import FltRegular.NumberTheory.Hilbert90
 import FltRegular.NumberTheory.Hilbert92
 import FltRegular.NumberTheory.Hilbert94
 import FltRegular.NumberTheory.KummersLemma.Field

FltRegular/CaseII/InductionStep.lean

@@ -4,7 +4,7 @@ import FltRegular.NumberTheory.KummersLemma.KummersLemma
 open scoped nonZeroDivisors NumberField
 open Polynomial
 
-variable {K : Type*} {p : ℕ} [NeZero p] [Field K] (hp : p ≠ 2)
+variable {K : Type} {p : ℕ} [NeZero p] [Field K] (hp : p ≠ 2)
 
 variable {ζ : K} (hζ : IsPrimitiveRoot ζ p) {x y z : 𝓞 K} {ε : (𝓞 K)ˣ}
 

FltRegular/CaseII/Statement.lean

@@ -3,7 +3,7 @@ import FltRegular.CaseII.InductionStep
 open scoped nonZeroDivisors NumberField
 open Polynomial
 
-variable {K : Type*} {p : ℕ} [hpri : Fact p.Prime] [Field K] [NumberField K]
+variable {K : Type} {p : ℕ} [hpri : Fact p.Prime] [Field K] [NumberField K]
   [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup (𝓞 K))]
   (hreg : p.Coprime <| Fintype.card <| ClassGroup (𝓞 K))
 

FltRegular/NumberTheory/Hilbert90.lean

@@ -253,18 +253,6 @@ section Mathlib.Algebra.Algebra.Hom
 
 variable {R A' : Type*} [CommSemiring R] [Semiring A'] [Algebra R A'] (φ ψ : A' →ₐ[R] A')
 
-@[simp]
-theorem AlgHom.toMonoidHom_one : MonoidHomClass.toMonoidHom (1 : A' →ₐ[R] A') = MonoidHom.id _ :=
-  rfl
-
-@[simp]
-theorem AlgHom.toMonoidHom_comp :
-    MonoidHomClass.toMonoidHom (φ.comp ψ) =
-      (MonoidHomClass.toMonoidHom φ).comp (MonoidHomClass.toMonoidHom ψ) :=
-  rfl
-
-theorem AlgHom.mul_def : φ * ψ = φ.comp ψ := rfl
-
 end Mathlib.Algebra.Algebra.Hom
 
 noncomputable
@@ -284,18 +272,15 @@ lemma relativeUnitsMap_mk (σ : K →ₐ[k] K) (x : (𝓞 K)ˣ) :
 theorem relativeUnitsMap_one (x : RelativeUnits k K) :
     relativeUnitsMap (1 : K →ₐ[k] K) x = x := by
   obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
-  simp [relativeUnitsMap_mk]
-
-@[simp]
-theorem coe_relativeUnitsMap_one : ⇑(relativeUnitsMap (1 : K →ₐ[k] K)) = id := by
-  ext; simp
+  simp only [relativeUnitsMap_mk, map_one]
+  rfl
 
 @[simp]
 theorem relativeUnitsMap_mul_apply {f g} (x : RelativeUnits k K) :
     (relativeUnitsMap (f * g)) x = (relativeUnitsMap f (relativeUnitsMap g x)) := by
   obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
-  simp_rw [relativeUnitsMap_mk, map_mul, AlgHom.mul_def]
-  simp
+  simp_rw [relativeUnitsMap_mk, map_mul]
+  rfl
 
 @[simp]
 theorem relativeUnitsMap_mul {f g : K →ₐ[k] K} :
@@ -318,9 +303,6 @@ def Monoid.End.equiv : Monoid.End M ≃ (M →* M) where
   left_inv _ := rfl
   right_inv _ := rfl
 
-@[simp]
-theorem Monoid.End.equiv_apply_apply {f} {x : M} : (Monoid.End.equiv M) f x = f x := rfl
-
 @[simp]
 theorem Monoid.End.equiv_symm_apply_apply {f} {x : M} : (Monoid.End.equiv M).symm f x = f x := rfl
 

FltRegular/NumberTheory/Hilbert92.lean

@@ -1,17 +1,15 @@
 import FltRegular.NumberTheory.Unramified
 import FltRegular.NumberTheory.Hilbert92
-import FltRegular.NumberTheory.Hilbert90
 import FltRegular.NumberTheory.RegularPrimes
-import Mathlib.NumberTheory.NumberField.ClassNumber
-import Mathlib.RingTheory.Ideal.Norm.RelNorm
+import Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
 
 open scoped NumberField
 
-variable {K : Type*} {p : ℕ} [hpri : Fact p.Prime] [Field K]
+variable {K : Type} {p : ℕ} [hpri : Fact p.Prime] [Field K]
 
 open Polynomial Module
 
-variable {L} [Field L] [Algebra K L] [FiniteDimensional K L]
+variable {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L]
   (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (hKL : finrank K L = p)
 
 variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Algebra A K]
@@ -52,7 +50,9 @@ 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η
+  have := isCyclic_iff_exists_zpowers_eq_top.2 ⟨σ, (Subgroup.eq_top_iff' _).2 hσ⟩
+  obtain ⟨β, hβ_zero, hβ⟩ := groupCohomology.exists_mul_galRestrict_of_norm_eq_one (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 _
@@ -111,7 +111,7 @@ theorem Ideal.isPrincipal_pow_finrank_of_isPrincipal_map [IsDedekindDomain A] {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 exists_not_isPrincipal_and_isPrincipal_map (K L : Type*)
+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)] [h : IsCyclic (L ≃ₐ[K] L)]
     (hKL : Nat.Prime (finrank K L))
@@ -124,7 +124,7 @@ theorem exists_not_isPrincipal_and_isPrincipal_map (K L : Type*)
 /-- 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`. -/
-theorem dvd_card_classGroup_of_isUnramified_isCyclic {K L : Type*}
+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)]
     (hKL : Nat.Prime (finrank K L))

FltRegular/NumberTheory/Hilbert94.lean

@@ -4,7 +4,7 @@ import FltRegular.NumberTheory.Hilbert94
 open Polynomial
 open scoped NumberField
 
-variable {K : Type*} {p : ℕ} [hpri : Fact p.Prime] [Field K] [NumberField K]
+variable {K : Type} {p : ℕ} [hpri : Fact p.Prime] [Field K] [NumberField K]
   [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup (𝓞 K))]
   (hreg : p.Coprime <| Fintype.card <| ClassGroup (𝓞 K))
   {ζ : K} (hζ : IsPrimitiveRoot ζ p)

FltRegular/NumberTheory/KummersLemma/KummersLemma.lean

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "eae0ea4f182ea7c0ed27099c4ca5b49b91b4a878",
+   "rev": "15f6691e7a582dab598395c89b04c451f81b8049",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lake-manifest.json

@@ -6,9 +6,9 @@ pp.unicode.fun = true # pretty-prints `fun a ↦ b`
 autoImplicit = false # no "assume a typo is a new variable"
 relaxedAutoImplicit = false # no "assume a typo is a new variable"
 maxSynthPendingDepth = 3 # same as mathlib, changes behaviour of typeclass inference
-linter.flexible = true # no rigid tactic (e.g. `exact`) after a flexible tactic (e.g. `simp`)
 # Enable all mathlib linters: automatically matches what mathlib uses.
 linter.mathlibStandardSet = true
+linter.flexible = true
 
 [[require]]
 name = "mathlib"