From 861b7df057140b45b8bb7d30d33426ffbbdda52b Mon Sep 17 00:00:00 2001 From: riccardobrasca Date: Thu, 7 Dec 2023 13:05:06 +0100 Subject: [PATCH] bump --- FltRegular/NumberTheory/AuxLemmas.lean | 117 +----------------- .../NumberTheory/Cyclotomic/MoreLemmas.lean | 1 + FltRegular/NumberTheory/Different.lean | 3 +- lake-manifest.json | 2 +- 4 files changed, 5 insertions(+), 118 deletions(-) diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean index d7a73ed7..6d173f6e 100644 --- a/FltRegular/NumberTheory/AuxLemmas.lean +++ b/FltRegular/NumberTheory/AuxLemmas.lean @@ -573,7 +573,7 @@ lemma IsSeparable_of_isLocalization (R S Rₚ Sₚ) [CommRing R] [CommRing S] [F (algebraMap R S) (Submonoid.le_comap_map M) · apply IsLocalization.ringHom_ext M simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq] - refine ⟨IsIntegral_of_isLocalization R S Rₚ Sₚ M (IsSeparable.isIntegral _), fun x ↦ ?_⟩ + refine ⟨fun x ↦ ?_⟩ obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid S M) x obtain ⟨t, ht, e⟩ := s.prop let P := ((minpoly R x).map (algebraMap R Rₚ)).scaleRoots (IsLocalization.mk' _ 1 ⟨t, ht⟩) @@ -732,12 +732,6 @@ lemma Module.Finite_of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommRing A₁] haveI := Module.Finite.of_restrictScalars_finite A₁ A₂ B₁ exact Module.Finite.equiv e.toLinearEquiv --- Mathlib/Algebra/Module/Submodule/Pointwise.lean -open Pointwise in -lemma Submodule.span_singleton_mul {R S} [CommRing R] [CommRing S] [Algebra R S] - {x : S} {p : Submodule R S} : Submodule.span R {x} * p = x • p := by - ext; exact Submodule.mem_span_singleton_mul - -- Mathlib/Algebra/Module/Submodule/Pointwise.lean open Pointwise in lemma Submodule.mem_smul_iff_inv {R S} [CommRing R] [Field S] [Algebra R S] @@ -746,12 +740,6 @@ lemma Submodule.mem_smul_iff_inv {R S} [CommRing R] [Field S] [Algebra R S] · rintro ⟨a, ha : a ∈ p, rfl⟩; simpa [inv_mul_cancel_left₀ hx] · exact fun h ↦ ⟨_, h, by simp [mul_inv_cancel_left₀ hx]⟩ --- Mathlib/Algebra/Module/Submodule/Pointwise.lean -open Pointwise in -lemma Submodule.mul_mem_smul_iff {R S} [CommRing R] [Field S] [Algebra R S] - {x : S} {p : Submodule R S} {y : S} (hx : x ≠ 0) : x * y ∈ x • p ↔ y ∈ p := by - rw [Submodule.mem_smul_iff_inv hx, inv_mul_cancel_left₀ hx] - -- Mathlib/RingTheory/Adjoin/Basic.lean lemma Algebra.map_adjoin_singleton {R A B} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (x : A) (e : A →ₐ[R] B) : @@ -789,15 +777,6 @@ lemma mem_coeIdeal_conductor {A B L} [CommRing A] [CommRing B] [CommRing L] [Alg -- (x : A) (p : R[X]) : aeval (algebraMap A B x) p = algebraMap A B (aeval x p) := by -- rw [aeval_def, aeval_def, hom_eval₂, IsScalarTower.algebraMap_eq R A B] --- Mathlib/RingTheory/Nakayama.lean -open Ideal in -theorem Submodule.le_of_le_smul_of_le_jacobson_bot {R M} [CommRing R] [AddCommGroup M] [Module R M] - {I : Ideal R} {N N' : Submodule R M} (hN' : N'.FG) - (hIJ : I ≤ jacobson ⊥) (hNN : N ⊔ N' ≤ N ⊔ I • N') : N' ≤ N := by - have := Submodule.smul_sup_le_of_le_smul_of_le_jacobson_bot hN' hIJ hNN - rw [sup_eq_left.mpr this] at hNN - exact le_sup_right.trans hNN - -- Mathlib/LinearAlgebra/Dimension.lean lemma FiniteDimensional.finrank_le_of_span_eq_top {R M} [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M] @@ -848,100 +827,6 @@ lemma Polynomial.dvd_C_mul_X_sub_one_pow_add_one exact mul_dvd_mul_left _ (Finset.dvd_sum (fun x hx ↦ dvd_mul_of_dvd_left (dvd_mul_of_dvd_left (dvd_pow (dvd_mul_right _ _) (Finset.mem_Ioo.mp hx).1.ne.symm) _) _)) --- Mathlib/RingTheory/PolynomialAlgebra.lean -open Polynomial in -lemma Matrix.eval_det_add_X_smul {n} [Fintype n] [DecidableEq n] {R} [CommRing R] - (A) (M : Matrix n n R) : - (det (A + (X : R[X]) • M.map C)).eval 0 = (det A).eval 0 := by - simp only [eval_det, map_zero, map_add, eval_add, Algebra.smul_def, _root_.map_mul] - simp only [Algebra.algebraMap_eq_smul_one, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X, - mul_zero, add_zero] - --- Mathlib/LinearAlgebra/Matrix/Trace.lean -lemma Matrix.trace_submatrix_succ {n : ℕ} {R} [CommRing R] (M : Matrix (Fin n.succ) (Fin n.succ) R) : - M 0 0 + trace (submatrix M Fin.succ Fin.succ) = trace M := by - delta trace - rw [← (finSuccEquiv n).symm.sum_comp] - simp - --- Not sure about the following fivem but they should probably go togethere - -open Polynomial in -lemma Matrix.derivative_det_one_add_X_smul_aux {n} {R} [CommRing R] (M : Matrix (Fin n) (Fin n) R) : - (derivative <| det (1 + (X : R[X]) • M.map C)).eval 0 = trace M := by - induction n with - | zero => simp - | succ n IH => - rw [det_succ_row_zero, map_sum, eval_finset_sum] - simp only [add_apply, smul_apply, map_apply, smul_eq_mul, X_mul_C, submatrix_add, - submatrix_smul, Pi.add_apply, Pi.smul_apply, submatrix_map, derivative_mul, map_add, - derivative_C, zero_mul, derivative_X, mul_one, zero_add, eval_add, eval_mul, eval_C, eval_X, - mul_zero, add_zero, eval_det_add_X_smul, eval_pow, eval_neg, eval_one] - rw [Finset.sum_eq_single 0] - · simp only [Fin.val_zero, pow_zero, derivative_one, eval_zero, one_apply_eq, eval_one, - mul_one, zero_add, one_mul, Fin.succAbove_zero, submatrix_one _ (Fin.succ_injective _), - det_one, IH, trace_submatrix_succ] - · intro i _ hi - cases n with - | zero => exact (hi (Subsingleton.elim i 0)).elim - | succ n => - simp only [one_apply_ne' hi, eval_zero, mul_zero, zero_add, zero_mul, add_zero] - rw [det_eq_zero_of_column_eq_zero 0, eval_zero, mul_zero] - intro j - rw [submatrix_apply, Fin.succAbove_below, one_apply_ne] - · exact (bne_iff_ne (Fin.succ j) (Fin.castSucc 0)).mp rfl - · rw [Fin.castSucc_zero]; exact lt_of_le_of_ne (Fin.zero_le _) hi.symm - · exact fun H ↦ (H <| Finset.mem_univ _).elim - -open Polynomial in -lemma Matrix.derivative_det_one_add_X_smul {n} [Fintype n] [DecidableEq n] {R} [CommRing R] - (M : Matrix n n R) : (derivative <| det (1 + (X : R[X]) • M.map C)).eval 0 = trace M := by - let e := Matrix.reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n) - rw [← Matrix.det_reindexLinearEquiv_self R[X] (Fintype.equivFin n)] - convert derivative_det_one_add_X_smul_aux (e M) - · ext; simp - · delta trace - rw [← (Fintype.equivFin n).symm.sum_comp] - rfl - -open Polynomial in -lemma Matrix.det_one_add_X_smul {n} [Fintype n] [DecidableEq n] {R} [CommRing R] - (M : Matrix n n R) : det (1 + (X : R[X]) • M.map C) = - (1 : R[X]) + trace M • X + (det (1 + (X : R[X]) • M.map C)).divX.divX * X ^ 2 := by - rw [Algebra.smul_def (trace M), ← C_eq_algebraMap, pow_two, ← mul_assoc, add_assoc, - ← add_mul, ← derivative_det_one_add_X_smul, ← coeff_zero_eq_eval_zero, coeff_derivative, - Nat.cast_zero, @zero_add R, mul_one, ← coeff_divX, add_comm (C _), divX_mul_X_add, - add_comm (1 : R[X]), ← C.map_one] - convert (divX_mul_X_add _).symm - rw [coeff_zero_eq_eval_zero, eval_det_add_X_smul, det_one, eval_one] - -open Polynomial in -lemma Matrix.det_one_add_smul {n} [Fintype n] [DecidableEq n] {R} [CommRing R] (r : R) - (M : Matrix n n R) : det (1 + r • M) = - 1 + trace M * r + (det (1 + (X : R[X]) • M.map C)).divX.divX.eval r * r ^ 2 := by - have := congr_arg (eval r) (Matrix.det_one_add_X_smul M) - simp only [eval_det, scalar_apply, map_add, _root_.map_one, eval_add, eval_one, eval_smul, eval_X, - smul_eq_mul, eval_mul, eval_pow] at this - convert this - rw [Algebra.smul_def X, _root_.map_mul] - have : matPolyEquiv (M.map C) = C M - · ext; simp only [matPolyEquiv_coeff_apply, map_apply, coeff_C]; rw [ite_apply, ite_apply]; rfl - simp only [Algebra.algebraMap_eq_smul_one, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X, this, - Algebra.mul_smul_comm, mul_one, eval_C] - exact Matrix.smul_eq_mul_diagonal _ _ - -lemma Algebra.norm_one_add_smul {A B} [CommRing A] [CommRing B] [Algebra A B] - [Module.Free A B] [Module.Finite A B] (a : A) (x : B) : - ∃ r : A, Algebra.norm A (1 + a • x) = 1 + Algebra.trace A B x * a + r * a ^ 2 := by - classical - let ι := Module.Free.ChooseBasisIndex A B - let b : Basis ι A B := Module.Free.chooseBasis _ _ - haveI : Fintype ι := inferInstance - clear_value ι b - simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b] - simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a] - exact ⟨_, rfl⟩ - -- Mathlib/LinearAlgebra/FiniteDimensional.lean lemma FiniteDimensional.finrank_eq_one_of_linearEquiv {R V} [Field R] [AddCommGroup V] [Module R V] (e : R ≃ₗ[R] V) : finrank R V = 1 := diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean index 2a1af6f6..e0cf092e 100644 --- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean @@ -4,6 +4,7 @@ import FltRegular.NumberTheory.Cyclotomic.UnitLemmas import FltRegular.NumberTheory.Cyclotomic.CyclRat import Mathlib.RingTheory.Ideal.Norm import Mathlib.RingTheory.ClassGroup +import Mathlib.RingTheory.NormTrace import FltRegular.ReadyForMathlib.PowerBasis import FltRegular.NumberTheory.AuxLemmas diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean index d5edb79a..68e92c49 100644 --- a/FltRegular/NumberTheory/Different.lean +++ b/FltRegular/NumberTheory/Different.lean @@ -430,7 +430,8 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B] have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0 · rwa [ne_eq, inv_eq_zero] have : IsIntegral A (algebraMap B L x) := IsIntegral.map (IsScalarTower.toAlgHom A B L) hAx - simp_rw [← Subalgebra.mem_toSubmodule, ← Submodule.mul_mem_smul_iff (y := y * _) hne₂] + simp_rw [← Subalgebra.mem_toSubmodule, ← Submodule.mul_mem_smul_iff (y := y * _) + (mem_nonZeroDivisors_of_ne_zero hne₂)] rw [← traceFormDualSubmodule_span_adjoin A K L _ hx this] simp only [mem_traceFormDualSubmodule, traceForm_apply, Subalgebra.mem_toSubmodule, minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, diff --git a/lake-manifest.json b/lake-manifest.json index 60d10528..12a83bc8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "ae28400c8acaa304f5bcb51624dc406d7d0a3731", + "rev": "f516ea2c0961f8b3b800a2f70d4981af830b703c", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,