From 151dc541905cf980fa0bd9ef89d3cb16ab0653bc Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 23 May 2024 14:55:18 +0200 Subject: [PATCH] bump --- FltRegular/NumberTheory/AuxLemmas.lean | 10 ++++---- FltRegular/NumberTheory/Different.lean | 3 +-- FltRegular/NumberTheory/GaloisPrime.lean | 24 ++++++++++--------- FltRegular/NumberTheory/Hilbert90.lean | 1 - FltRegular/NumberTheory/Hilbert92.lean | 11 +++++---- FltRegular/NumberTheory/IdealNorm.lean | 10 ++++---- .../NumberTheory/KummersLemma/Field.lean | 9 ++++--- FltRegular/NumberTheory/Unramified.lean | 12 +++++----- lake-manifest.json | 6 ++--- lean-toolchain | 2 +- 10 files changed, 45 insertions(+), 43 deletions(-) diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean index f78ab835..6dc57828 100644 --- a/FltRegular/NumberTheory/AuxLemmas.lean +++ b/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] diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean index 6945028c..89954786 100644 --- a/FltRegular/NumberTheory/Different.lean +++ b/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 diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean index 0b7be229..bb51f68d 100644 --- a/FltRegular/NumberTheory/GaloisPrime.lean +++ b/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] diff --git a/FltRegular/NumberTheory/Hilbert90.lean b/FltRegular/NumberTheory/Hilbert90.lean index 0b7e0cbd..b91f4a80 100644 --- a/FltRegular/NumberTheory/Hilbert90.lean +++ b/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 diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 7477a252..b8394d19 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/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 := diff --git a/FltRegular/NumberTheory/IdealNorm.lean b/FltRegular/NumberTheory/IdealNorm.lean index adf9ce68..5e4a9cb2 100644 --- a/FltRegular/NumberTheory/IdealNorm.lean +++ b/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 diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean index 2ff25ada..9e599a07 100644 --- a/FltRegular/NumberTheory/KummersLemma/Field.lean +++ b/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 diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean index 381f9f75..06c888d2 100644 --- a/FltRegular/NumberTheory/Unramified.lean +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json index 371bd6c3..75904b9d 100644 --- a/lake-manifest.json +++ b/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, diff --git a/lean-toolchain b/lean-toolchain index d8a6d7ef..78f39e21 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc1 +leanprover/lean4:v4.8.0-rc2