bump

Author: riccardobrasca

FltRegular/NumberTheory/AuxLemmas.lean

@@ -15,10 +15,9 @@ lemma Ideal.comap_coe {R S F : Type*} [Semiring R] [Semiring S] [FunLike F R S]
   (f : F) (I : Ideal S) : I.comap (f : R →+* S) = I.comap f := rfl
 
 -- Mathlib/RingTheory/IntegralClosure.lean
-lemma isIntegralClosure_self {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
-    (hRS : Algebra.IsIntegral R S) : IsIntegralClosure S R S where
-  algebraMap_injective' := Function.injective_id
-  isIntegral_iff := fun {x} ↦ ⟨fun _ ↦ ⟨x, rfl⟩, fun _ ↦ hRS _⟩
+instance isIntegralClosure_self {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+    [Algebra.IsIntegral R S] : IsIntegralClosure S R S :=
+  ⟨Function.injective_id, fun {x} ↦ ⟨fun _ ↦ ⟨x, rfl⟩, fun _ ↦ Algebra.IsIntegral.isIntegral x⟩⟩
 
 -- Mathlib/NumberTheory/RamificationInertia.lean
 section RamificationInertia
@@ -101,12 +100,13 @@ lemma IsIntegral_of_isLocalization (R S Rₚ Sₚ) [CommRing R] [CommRing S] [Co
     (algebraMap R S) (Submonoid.le_comap_map M) := by
     apply IsLocalization.ringHom_ext M
     simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
+  constructor
   intros x
   obtain ⟨x, ⟨_, t, ht, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective
     (Algebra.algebraMapSubmonoid S M) x
   rw [IsLocalization.mk'_eq_mul_mk'_one]
   apply RingHom.IsIntegralElem.mul
-  · exact IsIntegral.tower_top (IsIntegral.map (IsScalarTower.toAlgHom R S Sₚ) (hRS x))
+  · exact IsIntegral.tower_top (IsIntegral.map (IsScalarTower.toAlgHom R S Sₚ) (hRS.1 x))
   · show IsIntegral _ _
     convert isIntegral_algebraMap (x := IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
     rw [this, IsLocalization.map_mk', _root_.map_one]

FltRegular/NumberTheory/Different.lean

@@ -92,10 +92,9 @@ lemma pow_sub_one_dvd_differentIdeal
     {p : Ideal A} [p.IsMaximal] (P : Ideal B) (e : ℕ) (hp : p ≠ ⊥)
     (hP : P ^ e ∣ p.map (algebraMap A B)) : P ^ (e - 1) ∣ differentIdeal A B := by
   have : IsIntegralClosure B A (FractionRing B) :=
-    IsIntegralClosure.of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := A) (B := B))
+    IsIntegralClosure.of_isIntegrallyClosed _ _ _
   have : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
     IsIntegralClosure.isLocalization _ (FractionRing A) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := A) (B := B)))
   have : FiniteDimensional (FractionRing A) (FractionRing B) :=
     Module.Finite_of_isLocalization A B _ _ A⁰
   by_cases he : e = 0

FltRegular/NumberTheory/GaloisPrime.lean

@@ -35,11 +35,11 @@ def primesOverFinset [IsDedekindDomain S] (p : Ideal R) :
 variable {S}
 
 lemma primesOver_bot [Nontrivial R] [IsDomain S] [NoZeroSMulDivisors R S]
-  (hRS : Algebra.IsIntegral R S) :
+  [Algebra.IsIntegral R S] :
     primesOver S (⊥ : Ideal R) = {⊥} := by
   ext p
   simp only [primesOver, Set.mem_setOf_eq, Set.mem_singleton_iff]
-  refine ⟨fun H ↦ Ideal.eq_bot_of_comap_eq_bot hRS H.2, ?_⟩
+  refine ⟨fun H ↦ Ideal.eq_bot_of_comap_eq_bot H.2, ?_⟩
   rintro rfl
   rw [← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]
   exact ⟨Ideal.bot_prime, NoZeroSMulDivisors.algebraMap_injective _ _⟩
@@ -78,10 +78,10 @@ lemma primesOver_finite [Ring.DimensionLEOne R] [IsDedekindDomain S] [NoZeroSMul
   · rw [primesOver_eq_empty_of_not_isPrime S p h]
     exact Set.finite_empty
 
-lemma primesOver_nonempty [IsDomain S] [NoZeroSMulDivisors R S] (hRS : Algebra.IsIntegral R S)
+lemma primesOver_nonempty [IsDomain S] [NoZeroSMulDivisors R S] [Algebra.IsIntegral R S]
     (p : Ideal R) [p.IsPrime] : (primesOver S p).Nonempty := by
   have := Ideal.bot_prime (α := S)
-  obtain ⟨Q, _, hQ⟩ := Ideal.exists_ideal_over_prime_of_isIntegral hRS p ⊥
+  obtain ⟨Q, _, hQ⟩ := Ideal.exists_ideal_over_prime_of_isIntegral p ⊥
     (by rw [Ideal.comap_bot_of_injective _
       (NoZeroSMulDivisors.algebraMap_injective R S)]; exact bot_le)
   exact ⟨Q, hQ⟩
@@ -164,7 +164,8 @@ instance [IsGalois K L] (p : Ideal R) :
   by_cases hp : p = ⊥
   · subst hp
     have : Subsingleton (primesOver S (⊥ : Ideal R)) := by
-      rw [primesOver_bot (IsIntegralClosure.isIntegral_algebra R L)]; infer_instance
+      have : Algebra.IsIntegral R S := (IsIntegralClosure.isIntegral_algebra R L)
+      rw [primesOver_bot]; infer_instance
     exact ⟨1, Subsingleton.elim _ _⟩
   have hP := isMaximal_of_mem_primesOver hp P.prop
   -- Suppose the contrary that `σ • P ≠ Q` for all `σ`.
@@ -242,17 +243,17 @@ lemma Ideal.ramificationIdxIn_bot : (⊥ : Ideal R).ramificationIdxIn S = 0 := b
   · exact dif_neg h
 
 lemma Ideal.inertiaDegIn_bot [Nontrivial R] [IsDomain S] [NoZeroSMulDivisors R S] [IsNoetherian R S]
-    (hRS : Algebra.IsIntegral R S) [H : (⊥ : Ideal R).IsMaximal] :
+    [Algebra.IsIntegral R S] [H : (⊥ : Ideal R).IsMaximal] :
     (⊥ : Ideal R).inertiaDegIn S = FiniteDimensional.finrank R S := by
   delta inertiaDegIn
-  rw [primesOver_bot hRS]
+  rw [primesOver_bot]
   have : ({⊥} : Set (Ideal S)).Nonempty := by simp
   rw [dif_pos this, this.choose_spec]
   have hR := not_imp_not.mp (Ring.ne_bot_of_isMaximal_of_not_isField H) rfl
-  have hS := isField_of_isIntegral_of_isField' hRS hR
+  have hS := isField_of_isIntegral_of_isField' (S := S) hR
   letI : Field R := hR.toField
   letI : Field S := hS.toField
-  have : IsIntegralClosure S R S := isIntegralClosure_self hRS
+  have : IsIntegralClosure S R S := isIntegralClosure_self
   rw [← Ideal.map_bot (f := algebraMap R S), ← finrank_quotient_map (R := R) (S := S) ⊥ R S]
   exact inertiaDeg_algebraMap _ _
 
@@ -358,11 +359,12 @@ lemma prod_smul_primesOver [IsGalois K L] (p : Ideal R) (P : primesOver S p) [p.
   by_cases hp : p = ⊥
   · subst hp
     have := P.prop
-    simp_rw [primesOver_bot (S := S) (IsIntegralClosure.isIntegral_algebra R L),
+    have hRS : Algebra.IsIntegral R S := IsIntegralClosure.isIntegral_algebra R L
+    simp_rw [primesOver_bot (S := S),
       Set.mem_singleton_iff] at this
     simp_rw [coe_smul_primesOver, this,
       Ideal.comap_bot_of_injective _ (galRestrict R K L S _).injective, Finset.prod_const,
-      Ideal.map_bot, Ideal.inertiaDegIn_bot R S (IsIntegralClosure.isIntegral_algebra R L)]
+      Ideal.map_bot, Ideal.inertiaDegIn_bot R S]
     refine (zero_pow ?_).trans (zero_pow ?_).symm
     · rw [Finset.card_univ, Ne, Fintype.card_eq_zero_iff]
       simp only [not_isEmpty_of_nonempty, not_false_eq_true]

FltRegular/NumberTheory/Hilbert90.lean

@@ -147,7 +147,6 @@ lemma Hilbert90_integral (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowe
   haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
   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 ⟨x, y, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid B A⁰) ε
   obtain ⟨t, ht, ht'⟩ := y.prop

FltRegular/NumberTheory/Hilbert92.lean

@@ -114,8 +114,9 @@ lemma LinearIndependent.update' {ι} [DecidableEq ι] {R} [CommRing R] [Module R
     Finsupp.total_pi_single, smul_add, smul_sub, smul_zero] at hl'
   rw [smul_comm σ (l' i) g, hg, ← LinearMap.map_smul, ← LinearMap.map_smul, smul_smul,
     ← Finsupp.total_single, ← (Finsupp.total ι G R f).map_sub, ← map_add] at hl'
-  replace hl' : ∀ j, (σ * l' j - (fun₀ | i => σ * l' i) j) + l' i * l j = 0 :=
-    fun j ↦ DFunLike.congr_fun (hf _ hl') j
+  replace hl' : ∀ j, (σ * l' j - (fun₀ | i => σ * l' i) j) + l' i * l j = 0 := by
+    intro j
+    exact DFunLike.congr_fun (hf _ hl') j
   simp only [Finsupp.single_apply] at hl'
   have : l' i = 0 := hl _ (by simpa using hl' i)
   simp only [this, zero_mul, add_zero, mul_zero, ite_self, sub_zero] at hl'
@@ -243,8 +244,10 @@ attribute [local instance] IsCyclic.commGroup
 attribute [local instance 2000] inst_ringOfIntegersAlgebra Algebra.toSMul Algebra.toModule
 
 instance : IsScalarTower (𝓞 k) (𝓞 K) K := IsScalarTower.of_algebraMap_eq (fun _ ↦ rfl)
-instance : IsIntegralClosure (𝓞 K) (𝓞 k) K := IsIntegralClosure.of_isIntegrallyClosed _ _ _
-  (fun x ↦ IsIntegral.tower_top (IsIntegralClosure.isIntegral ℤ K x))
+
+instance : IsIntegralClosure (𝓞 K) (𝓞 k) K := by
+  have : Algebra.IsIntegral (𝓞 k) (𝓞 K) := ⟨fun _ ↦ .tower_top (IsIntegralClosure.isIntegral ℤ K _)⟩
+  apply IsIntegralClosure.of_isIntegrallyClosed
 
 lemma coe_galRestrictHom_apply (σ : K →ₐ[k] K) (x) :
     (galRestrictHom (𝓞 k) k K (𝓞 K) σ x : K) = σ x :=

FltRegular/NumberTheory/IdealNorm.lean

@@ -32,10 +32,11 @@ variable (R S K L) [CommRing R] [CommRing S] [Field K] [Field L]
     [IsIntegrallyClosed S] [IsSeparable (FractionRing R) (FractionRing S)]
 
 instance : IsIntegralClosure S R (FractionRing S) :=
-  IsIntegralClosure.of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
+  IsIntegralClosure.of_isIntegrallyClosed _ _ _
+
 instance : IsLocalization (Algebra.algebraMapSubmonoid S R⁰) (FractionRing S) :=
     IsIntegralClosure.isLocalization _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
+
 instance : FiniteDimensional (FractionRing R) (FractionRing S) :=
     Module.Finite_of_isLocalization R S _ _ R⁰
 
@@ -144,7 +145,7 @@ theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R
   letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
     (Algebra.algebraMapSubmonoid S M) Sₘ L
   haveI : IsIntegralClosure Sₘ Rₘ L :=
-    IsIntegralClosure.of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₘ) (B := Sₘ))
+    IsIntegralClosure.of_isIntegrallyClosed _ _ _
   rw [map_spanIntNorm]
   refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)
   · rintro a' ha'
@@ -346,8 +347,7 @@ theorem spanIntNorm_map (I : Ideal R) :
       RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R S Sₚ,
       IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
       RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-  haveI : IsIntegralClosure Sₚ Rₚ L :=
-    IsIntegralClosure.of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₚ) (B := Sₚ))
+  haveI : IsIntegralClosure Sₚ Rₚ L := IsIntegralClosure.of_isIntegrallyClosed _ _ _
   haveI : IsSeparable (FractionRing Rₚ) (FractionRing Sₚ) := by
     apply IsSeparable.of_equiv_equiv (FractionRing.algEquiv Rₚ (FractionRing R)).symm.toRingEquiv
       (FractionRing.algEquiv Sₚ (FractionRing S)).symm.toRingEquiv

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -129,8 +129,7 @@ theorem aeval_poly {L : Type*} [Field L] [Algebra K L] (α : L)
 
 def polyRoot {L : Type*} [Field L] [Algebra K L] (α : L)
     (e : α ^ (p : ℕ) = algebraMap K L u) (m : ℕ) : 𝓞 L :=
-  ⟨((1 : L) - ζ ^ m • α) / (algebraMap K L (ζ - 1)), isIntegral_trans
-    (show Algebra.IsIntegral ℤ (𝓞 K) from IsIntegralClosure.isIntegral_algebra ℤ K) _
+  ⟨((1 : L) - ζ ^ m • α) / (algebraMap K L (ζ - 1)), isIntegral_trans _
       ⟨poly hp hζ u hcong, monic_poly hp hζ u hcong, aeval_poly hp hζ u hcong α e m⟩⟩
 
 theorem roots_poly {L : Type*} [Field L] [Algebra K L] (α : L)
@@ -191,8 +190,8 @@ lemma isIntegralClosure_of_isScalarTower (R A K L B) [CommRing R] [CommRing A] [
   algebraMap_injective' := IsIntegralClosure.algebraMap_injective B R L
   isIntegral_iff := fun {x} ↦ by
     refine Iff.trans ?_ (IsIntegralClosure.isIntegral_iff (R := R) (A := B) (B := L))
-    exact ⟨isIntegral_trans (IsIntegralClosure.isIntegral_algebra R (A := A) K) x,
-      IsIntegral.tower_top⟩
+    have := (IsIntegralClosure.isIntegral_algebra R (A := A) K)
+    exact ⟨isIntegral_trans x, IsIntegral.tower_top⟩
 
 instance {K L} [Field K] [Field L] [Algebra K L] :
     IsIntegralClosure (𝓞 L) (𝓞 K) L := isIntegralClosure_of_isScalarTower ℤ _ K _ _
@@ -250,7 +249,7 @@ lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L)
   simp only [map_mul, map_sub, IsPrimitiveRoot.val_unit'_coe, map_one, map_pow, hcoe] at hv
   have hα : IsIntegral (𝓞 K) α := by
     apply IsIntegral.of_pow p.pos; rw [e]; exact isIntegral_algebraMap
-  have : IsUnit (⟨α, isIntegral_trans (IsIntegralClosure.isIntegral_algebra ℤ K) _ hα⟩ : 𝓞 L) := by
+  have : IsUnit (⟨α, isIntegral_trans _ hα⟩ : 𝓞 L) := by
     rw [← isUnit_pow_iff p.pos.ne.symm]
     convert (algebraMap (𝓞 K) (𝓞 L)).isUnit_map u.isUnit
     ext; simp only [SubmonoidClass.coe_pow, e]; rfl

FltRegular/NumberTheory/Unramified.lean

@@ -65,12 +65,11 @@ lemma comap_map_eq_of_isUnramified [IsGalois K L] [IsUnramified R S] (I : Ideal
   have := NoZeroSMulDivisors.iff_algebraMap_injective.mpr hRS
   by_cases hIbot : I = ⊥
   · rw [hIbot, Ideal.comap_bot_of_injective _ hRS, Ideal.map_bot]
-  have hIbot' : I.comap (algebraMap R S) ≠ ⊥ := mt (Ideal.eq_bot_of_comap_eq_bot
-    (IsIntegralClosure.isIntegral_algebra R L)) hIbot
+  have h1 : Algebra.IsIntegral R S := IsIntegralClosure.isIntegral_algebra R L
+  have hIbot' : I.comap (algebraMap R S) ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hIbot
   have : ∀ p, (p.IsPrime ∧ I.comap (algebraMap R S) ≤ p) → ∃ P ≥ I, P ∈ primesOver S p := by
     intro p ⟨hp₁, hp₂⟩
-    exact Ideal.exists_ideal_over_prime_of_isIntegral
-      (IsIntegralClosure.isIntegral_algebra R L) _ _ hp₂
+    exact Ideal.exists_ideal_over_prime_of_isIntegral _ _ hp₂
   choose 𝔓 h𝔓 h𝔓' using this
   suffices I = ∏ p in (factors (I.comap <| algebraMap R S)).toFinset,
     (p.map (algebraMap R S)) ^ (if h : _ then (factors I).count (𝔓 p h) else 0) by
@@ -156,11 +155,12 @@ lemma isUnramifiedAt_iff_SquareFree_minpoly [NoZeroSMulDivisors R S] [IsDedekind
       this hpbot hx hx').symm.injective
 
 lemma isUnramifiedAt_iff_SquareFree_minpoly_powerBasis [NoZeroSMulDivisors R S] [IsDedekindDomain S]
-    (hRS : Algebra.IsIntegral R S) (pb : PowerBasis R S)
+    [Algebra.IsIntegral R S] (pb : PowerBasis R S)
     (p : Ideal R) [p.IsPrime] (hpbot : p ≠ ⊥) :
     IsUnramifiedAt S p ↔ Squarefree ((minpoly R pb.gen).map (Ideal.Quotient.mk p)) := by
-  rw [isUnramifiedAt_iff_SquareFree_minpoly p hpbot pb.gen _ (hRS _)]
+  rw [isUnramifiedAt_iff_SquareFree_minpoly p hpbot pb.gen _ _]
   rw [conductor_eq_top_of_powerBasis, Ideal.comap_top, top_sup_eq]
+  exact PowerBasis.isIntegral_gen pb
 
 open nonZeroDivisors Polynomial
 

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "14f258593e8c261d8834f13c6edc7b970c253ee8",
+   "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "f617e0673845925e612b62141ff54c4b7980dc63",
+   "rev": "e8c8a42642ceb5af33708b79ae8a3148b681c236",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "3b462daa45f893202693b13e3965a7b4e1e7b631",
+   "rev": "5bf1683fbb7de26aee023022376acb23c740b3f5",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc1
+leanprover/lean4:v4.8.0-rc2