From 78b6206849494870a63b1c3e19b2494c5f32e054 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 18 Aug 2025 10:52:18 +0800 Subject: [PATCH 01/64] Update Basic.lean --- Mathlib/Data/ENat/Basic.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean index 62a20b1b1df27a..0a624d8b879c7c 100644 --- a/Mathlib/Data/ENat/Basic.lean +++ b/Mathlib/Data/ENat/Basic.lean @@ -575,3 +575,21 @@ lemma WithBot.add_one_le_iff {n : ℕ} {m : WithBot ℕ∞} : n + 1 ≤ m ↔ n · simp · rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n), ← WithBot.coe_lt_coe, WithBot.coe_natCast] + +lemma ENat.add_right_cancel_iff (a b c : ℕ∞) (netop : c ≠ ⊤) : a + c = b + c ↔ a = b := + ⟨fun h ↦ ENat.add_left_injective_of_ne_top netop h, fun h ↦ by rw [h]⟩ + +lemma withBotENat_add_coe_cancel (a b : WithBot ℕ∞) (c : ℕ) : a + c = b + c ↔ a = b := by + refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩ + by_cases eqbot : a = ⊥ + · simp [eqbot, WithBot.bot_add] at h + rw [WithBot.add_coe_eq_bot_iff.mp h.symm, eqbot] + · by_cases eqbot' : b = ⊥ + · absurd eqbot + simpa [eqbot'] using h + · have : a.unbot eqbot + c = b.unbot eqbot' + c := by + apply WithBot.coe_inj.mp + convert h + repeat simpa using by rfl + rw [← WithBot.coe_unbot a eqbot, ← WithBot.coe_unbot b eqbot', WithBot.coe_inj] + simpa [ENat.add_right_cancel_iff _ _ _ (ENat.coe_ne_top c)] using this From 0d9df370fa997ca6f548746de6a32b6c8170c499 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 19 Aug 2025 13:17:25 +0800 Subject: [PATCH 02/64] define regular local ring --- Mathlib.lean | 1 + Mathlib/RingTheory/RegularLocalRing.lean | 288 +++++++++++++++++++++++ 2 files changed, 289 insertions(+) create mode 100644 Mathlib/RingTheory/RegularLocalRing.lean diff --git a/Mathlib.lean b/Mathlib.lean index 2cc6d186aca25c..c62d32edc99c79 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5642,6 +5642,7 @@ import Mathlib.RingTheory.Regular.Category import Mathlib.RingTheory.Regular.Depth import Mathlib.RingTheory.Regular.IsSMulRegular import Mathlib.RingTheory.Regular.RegularSequence +import Mathlib.RingTheory.RegularLocalRing import Mathlib.RingTheory.RingHom.Etale import Mathlib.RingTheory.RingHom.FaithfullyFlat import Mathlib.RingTheory.RingHom.Finite diff --git a/Mathlib/RingTheory/RegularLocalRing.lean b/Mathlib/RingTheory/RegularLocalRing.lean new file mode 100644 index 00000000000000..036f95f8769747 --- /dev/null +++ b/Mathlib/RingTheory/RegularLocalRing.lean @@ -0,0 +1,288 @@ +/- +Copyright (c) 2025 Nailin Guan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nailin Guan +-/ +import Mathlib.RingTheory.Ideal.Cotangent +import Mathlib.RingTheory.Ideal.KrullsHeightTheorem +import Mathlib.RingTheory.KrullDimension.NonZeroDivisors +import Mathlib.RingTheory.Regular.RegularSequence + +/-! +# Define Regular Local Ring +-/ + +open IsLocalRing + +variable (R : Type*) [CommRing R] + +class IsRegularLocalRing : Prop extends IsLocalRing R, IsNoetherianRing R where + reg : (Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R + +lemma isRegularLocalRing_iff [IsLocalRing R] [IsNoetherianRing R] : + IsRegularLocalRing R ↔ (Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R := + ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩ + +lemma ringKrullDim_le_spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] : + ringKrullDim R ≤ (Submodule.spanFinrank (maximalIdeal R)) := + le_of_eq_of_le IsLocalRing.maximalIdeal_height_eq_ringKrullDim.symm + (WithBot.coe_le_coe.mpr (Ideal.height_le_spanFinrank (maximalIdeal R) Ideal.IsPrime.ne_top')) + +lemma isRegularLocalRing_of_exist_span [IsLocalRing R] [IsNoetherianRing R] (S : Finset R) + (span : Ideal.span S = maximalIdeal R) (card : S.card ≤ ringKrullDim R) : + IsRegularLocalRing R := by + apply (isRegularLocalRing_iff _).mpr (le_antisymm _ (ringKrullDim_le_spanFinrank_maximalIdeal R)) + apply le_trans _ card + rw [← span, ← Ideal.submodule_span_eq, ← Set.ncard_coe_finset S, Nat.cast_le] + exact Submodule.spanFinrank_span_le_ncard_of_finite S.finite_toSet + +variable {R} in +lemma IsLocalRing.comap_maximalIdeal [IsLocalRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] + (e : R ≃+* R') : maximalIdeal R = Ideal.comap e (maximalIdeal R') := by + ext + simp + +variable {R} in +lemma IsLocalRing.map_maximalIdeal [IsLocalRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] + (e : R ≃+* R') : Ideal.map e (maximalIdeal R) = maximalIdeal R' := by + rw [← Ideal.map_comap_of_surjective _ e.surjective (maximalIdeal R'), + IsLocalRing.comap_maximalIdeal e] + +variable {R} in +lemma isRegularLocalRing_of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R'] + (e : R ≃+* R') : IsRegularLocalRing R' := by + let _ := e.isLocalRing + let _ := isNoetherianRing_of_ringEquiv R e + have fg : (maximalIdeal R).FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _ + let _ : Fintype (Submodule.generators (maximalIdeal R)) := + (Submodule.FG.finite_generators fg).fintype + apply isRegularLocalRing_of_exist_span R' ((maximalIdeal R).generators.toFinset.map e.toEmbedding) + · simp only [RingEquiv.toEquiv_eq_coe, Finset.coe_map, Equiv.coe_toEmbedding, EquivLike.coe_coe, + Set.coe_toFinset, ← Ideal.map_span] + rw [← Ideal.submodule_span_eq, Submodule.span_generators (maximalIdeal R)] + exact IsLocalRing.map_maximalIdeal e + · simpa [← ringKrullDim_eq_of_ringEquiv e, ← IsRegularLocalRing.reg, + ← Submodule.FG.generators_ncard fg] using le_of_eq (Set.ncard_eq_toFinset_card' _).symm + +section + +lemma span_eq_top_iff [IsLocalRing R] (S : Set (maximalIdeal R)) : + Submodule.span R S = ⊤ ↔ Submodule.span R ((Submodule.subtype (maximalIdeal R)) '' S) = + maximalIdeal R := by + rw [← Submodule.map_span] + refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩ + rw [← Submodule.comap_map_eq_of_injective (maximalIdeal R).injective_subtype + (Submodule.span R S), h, Submodule.comap_subtype_self] + +open Set in +lemma spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] : + (Submodule.spanFinrank (maximalIdeal R)) = + Module.finrank (ResidueField R) (CotangentSpace R) := by + let fg : Module.Finite (ResidueField R) (CotangentSpace R) := inferInstance + let fg' : (maximalIdeal R).FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _ + have : Submodule.spanFinrank (⊤ : Submodule (ResidueField R) (CotangentSpace R)) = + Module.rank (ResidueField R) (CotangentSpace R) := by + rw [← Submodule.fg_iff_spanRank_eq_spanFinrank.mpr fg.1, Submodule.rank_eq_spanRank_of_free] + simp only [← Module.finrank_eq_rank, Nat.cast_inj] at this + rw [← this] + apply le_antisymm + · have span : Submodule.span R + ((⊤ : Submodule (ResidueField R) (CotangentSpace R)).generators.image Quotient.out) = ⊤ := by + apply IsLocalRing.CotangentSpace.span_image_eq_top_iff.mp + convert Submodule.span_generators (⊤ : Submodule (ResidueField R) (CotangentSpace R)) + have : ⇑(maximalIdeal R).toCotangent ∘ Quotient.out = id := by + ext + exact Submodule.Quotient.mk_out _ + rw [← Set.image_comp, this, image_id] + rw [span_eq_top_iff, ← Set.image_comp] at span + rw [← Submodule.FG.generators_ncard fg.1, ← congrArg Submodule.spanFinrank span] + apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite + (Finite.image _ fg.1.finite_generators)) (Set.ncard_image_le fg.1.finite_generators) + · let G := ({x | ↑x ∈ (maximalIdeal R).generators} : Set (maximalIdeal R)) + have : Submodule.span R G = ⊤ := by + simp only [span_eq_top_iff, Submodule.subtype_apply, Ideal.submodule_span_eq, G] + convert (maximalIdeal R).span_generators + ext + simpa using fun a ↦ Submodule.FG.generators_mem (maximalIdeal R) a + have fin : G.Finite := Set.Finite.of_injOn (by simp [MapsTo, G]) injOn_subtype_val + (Submodule.FG.finite_generators fg') + rw [← IsLocalRing.CotangentSpace.span_image_eq_top_iff.mpr this, + ← Submodule.FG.generators_ncard fg'] + apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (Finite.image _ fin)) + exact le_trans (Set.ncard_image_le fin) (Set.ncard_le_ncard_of_injOn Subtype.val (by simp [G]) + injOn_subtype_val (Submodule.FG.finite_generators fg')) + +variable {R} in +lemma IsLocalRing.ResidueField.map_injective [IsLocalRing R] {S : Type*} [CommRing S] + [IsLocalRing S] (f : R →+* S) [IsLocalHom f] : + Function.Injective (ResidueField.map f) := by + rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] + intro x hx + simpa only [map_eq_zero] using hx + +variable {R} in +lemma IsLocalRing.ResidueField.map_bijective_of_surjective [IsLocalRing R] {S : Type*} [CommRing S] + [IsLocalRing S] (f : R →+* S) (surj : Function.Surjective f) [IsLocalHom f] : + Function.Bijective (ResidueField.map f) := by + refine ⟨ResidueField.map_injective f, ?_⟩ + apply Ideal.Quotient.lift_surjective_of_surjective + convert Function.Surjective.comp (Ideal.Quotient.mk_surjective (I := (maximalIdeal S))) surj + +variable {R} in +lemma _root_.ringKrullDim_le_ringKrullDim_add_card [IsLocalRing R] [IsNoetherianRing R] + {S : Finset R} (hS : (S : Set R) ⊆ maximalIdeal R) : + ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span S.toSet) + S.card := by + sorry + +lemma quotient_isRegularLocalRing_tfae [IsRegularLocalRing R] (S : Finset R) + (sub : (S : Set R) ⊆ maximalIdeal R) : + [∃ (T : Finset R), S ⊆ T ∧ T.card = ringKrullDim R ∧ Ideal.span T = maximalIdeal R, + LinearIndependent (ResidueField R) ((⇑(maximalIdeal R).toCotangent).comp (Set.inclusion sub)), + IsRegularLocalRing (R ⧸ Ideal.span (S : Set R)) ∧ + (ringKrullDim (R ⧸ Ideal.span (S : Set R)) + S.card = ringKrullDim R)].TFAE := by + have : Nontrivial (R ⧸ Ideal.span S.toSet) := + Ideal.Quotient.nontrivial (ne_top_of_le_ne_top Ideal.IsPrime.ne_top' (Ideal.span_le.mpr sub)) + have lochom : IsLocalHom (Ideal.Quotient.mk (Ideal.span S.toSet)) := + IsLocalHom.of_surjective _ (Ideal.Quotient.mk_surjective) + tfae_have 1 → 2 := by + rintro ⟨T, h, card, span⟩ + have Tsub : (T : Set R) ⊆ maximalIdeal R := by simpa [← span] using Ideal.subset_span + have : LinearIndependent (ResidueField R) + ((⇑(maximalIdeal R).toCotangent).comp (Set.inclusion Tsub)) := by + apply linearIndependent_of_top_le_span_of_card_eq_finrank + · simp only [Finset.coe_sort_coe, Set.range_comp, Set.range_inclusion Tsub, + SetLike.coe_sort_coe, Finset.mem_coe, top_le_iff, + IsLocalRing.CotangentSpace.span_image_eq_top_iff] + simp only [span_eq_top_iff, Submodule.subtype_apply, Ideal.submodule_span_eq] + convert span + ext + simpa using fun a ↦ Tsub a + · rw [← spanFinrank_maximalIdeal R, ← Nat.cast_inj (R := WithBot ℕ∞), + (isRegularLocalRing_iff R).mp ‹_›, ← card] + simp + have li := LinearIndependent.comp this (Set.inclusion h) (Set.inclusion_injective h) + have inc : Set.inclusion Tsub ∘ Set.inclusion h = Set.inclusion sub := rfl + simpa [← Function.comp_assoc, ← inc] using li + tfae_have 2 → 3 := by + intro li + let _ : IsLocalRing (R ⧸ Ideal.span S.toSet) := + IsLocalRing.of_surjective _ Ideal.Quotient.mk_surjective + rw [isRegularLocalRing_iff] + have le := ringKrullDim_le_ringKrullDim_add_card sub + have ge : (Submodule.spanFinrank (maximalIdeal (R ⧸ Ideal.span S.toSet))) + S.card ≤ + ringKrullDim R := by + simp only [← Nat.cast_add, ← (isRegularLocalRing_iff R).mp ‹_›, Nat.cast_le, + spanFinrank_maximalIdeal] + let f := Ideal.mapCotangent (maximalIdeal R) (maximalIdeal (R ⧸ Ideal.span S.toSet)) + (Ideal.Quotient.mkₐ R (Ideal.span S.toSet)) (fun x hx ↦ by simpa) + have ker : (LinearMap.ker f : Set (maximalIdeal R).Cotangent) = (Submodule.span + (ResidueField R) (Set.range (⇑(maximalIdeal R).toCotangent ∘ Set.inclusion sub))) := by + simp only [ Submodule.coe_span_eq_span_of_surjective R (ResidueField R) + IsLocalRing.residue_surjective, Finset.coe_sort_coe, SetLike.coe_set_eq] + ext x + induction' x using Submodule.Quotient.induction_on with x + simp only [Ideal.mapCotangent, LinearMap.mem_ker, f] + change (maximalIdeal (R ⧸ Ideal.span S.toSet)).toCotangent ⟨(Ideal.Quotient.mkₐ R + (Ideal.span S.toSet)) x, _⟩ = 0 ↔ (maximalIdeal R).toCotangent x ∈ _ + simp only [Ideal.Quotient.mkₐ_eq_mk, Set.range_comp, + Submodule.span_image', Ideal.toCotangent_eq_zero] + have : maximalIdeal (R ⧸ Ideal.span S.toSet) = + (maximalIdeal R).map (Ideal.Quotient.mk _) := by + simp only [← ((local_hom_TFAE _).out 0 4).mp lochom, + Ideal.map_comap_of_surjective _ Ideal.Quotient.mk_surjective] + rw [this, ← Ideal.map_pow, ← Ideal.mem_comap, ← Submodule.mem_comap, Submodule.comap_map_eq, + Ideal.comap_map_of_surjective' _ Ideal.Quotient.mk_surjective, Ideal.mk_ker, sup_comm, + ← Submodule.comap_map_eq_of_injective (maximalIdeal R).subtype_injective (Submodule.span + R (Set.range (Set.inclusion sub)) ⊔ LinearMap.ker (maximalIdeal R).toCotangent)] + simp only [Finset.coe_sort_coe, Submodule.map_sup, Submodule.mem_comap, + Submodule.subtype_apply] + congr! + · simp only [Submodule.map_span, Submodule.subtype_apply, Ideal.submodule_span_eq] + congr + ext + simpa using fun a ↦ sub a + · exact (Ideal.map_toCotangent_ker (maximalIdeal R)).symm + let Q := (CotangentSpace R) ⧸ (Submodule.span (ResidueField R) + (Set.range (⇑(maximalIdeal R).toCotangent ∘ Set.inclusion sub))) + let f' : Q →+ (CotangentSpace (R ⧸ Ideal.span S.toSet)) := + QuotientAddGroup.lift _ f + (le_of_eq (AddSubgroup.ext (fun x ↦ (congrFun ker.symm x).to_iff))) + have bij : Function.Bijective f' := by + constructor + · rw [← AddMonoidHom.ker_eq_bot_iff, eq_bot_iff] + intro x hx + induction' x using QuotientAddGroup.induction_on with x + have : x ∈ (LinearMap.ker f : Set (maximalIdeal R).Cotangent) := LinearMap.mem_ker.mpr hx + rw [ker] at this + exact AddSubgroup.mem_bot.mpr ((QuotientAddGroup.eq_zero_iff _).mpr this) + · apply QuotientAddGroup.lift_surjective_of_surjective + intro x + rcases Ideal.toCotangent_surjective _ x with ⟨y, hy⟩ + rcases Ideal.Quotient.mk_surjective y.1 with ⟨z, hz⟩ + have : z ∈ maximalIdeal R := by simp [← ((local_hom_TFAE _).out 0 4).mp lochom, hz] + use (maximalIdeal R).toCotangent ⟨z, this⟩ + simp [f, ← hy, hz] + let e : Q ≃+ (CotangentSpace (R ⧸ Ideal.span S.toSet)) := + AddEquiv.ofBijective f' bij + have rk := rank_eq_of_equiv_equiv (ResidueField.map (Ideal.Quotient.mk (Ideal.span S.toSet))) + e (ResidueField.map_bijective_of_surjective _ Ideal.Quotient.mk_surjective) (fun r m ↦ by + induction' m using Submodule.Quotient.induction_on with m + rw [← Submodule.Quotient.mk_smul] + simp only [Finset.coe_sort_coe, AddEquiv.ofBijective_apply, e, f'] + induction' r using Submodule.Quotient.induction_on with r + change f (r • m) = (ResidueField.map (Ideal.Quotient.mk (Ideal.span S.toSet))) + (IsLocalRing.residue R r) • (f m) + simp only [map_smul] + rfl) + have frk : Module.finrank (ResidueField R) Q = Module.finrank + (ResidueField (R ⧸ Ideal.span S.toSet)) (CotangentSpace (R ⧸ Ideal.span S.toSet)) := by + simp [Module.finrank, rk] + have : Fintype.card S.toSet = S.card := Fintype.card_ofFinset S (fun x ↦ Finset.mem_coe) + rw [← frk, ← this, ← finrank_span_eq_card li] + apply Module.finrank_quotient_add_finrank_le + have : ringKrullDim (R ⧸ Ideal.span S.toSet) + S.card ≤ + (Submodule.spanFinrank (maximalIdeal (R ⧸ Ideal.span S.toSet))) + S.card := + add_le_add_right (ringKrullDim_le_spanFinrank_maximalIdeal _) _ + exact ⟨(withBotENat_add_coe_cancel _ _ S.card).mp + (le_antisymm (ge.trans le) this), le_antisymm (this.trans ge) le⟩ + tfae_have 3 → 1 := by + classical + rintro ⟨reg, dim⟩ + simp only [← (isRegularLocalRing_iff _).mp reg, ← Nat.cast_add, ← + (isRegularLocalRing_iff R).mp ‹_›, Nat.cast_inj] at dim + let fg : (maximalIdeal (R ⧸ Ideal.span S.toSet)).FG := + (isNoetherianRing_iff_ideal_fg _).mp inferInstance _ + have fin : (maximalIdeal (R ⧸ Ideal.span S.toSet)).generators.Finite := + Submodule.FG.finite_generators fg + let U := Quotient.out '' (maximalIdeal (R ⧸ Ideal.span S.toSet)).generators + let _ : Fintype U := (Set.Finite.image _ fin).fintype + use S ∪ U.toFinset + have span : Ideal.span (S ∪ U) = maximalIdeal R := by + rw [Ideal.span_union, ← Ideal.mk_ker (I := Ideal.span S.toSet), sup_comm, + ← Ideal.comap_map_of_surjective' _ Ideal.Quotient.mk_surjective, Ideal.map_span] + have : Ideal.span (⇑(Ideal.Quotient.mk (Ideal.span ↑S)) '' U) = + Submodule.span _ (maximalIdeal (R ⧸ Ideal.span S.toSet)).generators := by + simp [U, ← Set.image_comp] + rw [this, Submodule.span_generators] + exact ((local_hom_TFAE _).out 0 4).mp lochom + simp only [Finset.subset_union_left, true_and, ← (isRegularLocalRing_iff R).mp ‹_›, + Finset.coe_union, Set.coe_toFinset] + refine ⟨le_antisymm ?_ ?_, span⟩ + · apply Nat.cast_le.mpr (le_trans (Finset.card_union_le _ _) _) + simp only [Set.toFinset_card, ← dim, add_comm, add_le_add_iff_left] + rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] + apply le_trans (Set.ncard_image_le fin) (le_of_eq (Submodule.FG.generators_ncard fg)) + · simp only [← span, ← Set.ncard_coe_finset, Finset.coe_union, Set.coe_toFinset, Nat.cast_le] + exact Submodule.spanFinrank_span_le_ncard_of_finite (Set.toFinite (S ∪ U)) + tfae_finish + +theorem isDomain_of_isRegularLocalRing [IsRegularLocalRing R] : IsDomain R := by + sorry + +open RingTheory.Sequence in +theorem isRegular_of_span_eq_maximalIdeal [IsRegularLocalRing R] (rs : List R) + (eq : Ideal.ofList rs = maximalIdeal R) (len : rs.length = ringKrullDim R) : + IsRegular R rs := by + sorry + +end From 58bfa3c5e24308a172fc376db8c35e8ff9f61498 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 19 Aug 2025 17:52:40 +0800 Subject: [PATCH 03/64] regular local ring is domain --- Mathlib/RingTheory/RegularLocalRing.lean | 70 +++++++++++++++++++++++- 1 file changed, 68 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing.lean b/Mathlib/RingTheory/RegularLocalRing.lean index 036f95f8769747..638f1521a04fe3 100644 --- a/Mathlib/RingTheory/RegularLocalRing.lean +++ b/Mathlib/RingTheory/RegularLocalRing.lean @@ -7,7 +7,7 @@ import Mathlib.RingTheory.Ideal.Cotangent import Mathlib.RingTheory.Ideal.KrullsHeightTheorem import Mathlib.RingTheory.KrullDimension.NonZeroDivisors import Mathlib.RingTheory.Regular.RegularSequence - +import Mathlib.RingTheory.KrullDimension.Field /-! # Define Regular Local Ring -/ @@ -276,8 +276,74 @@ lemma quotient_isRegularLocalRing_tfae [IsRegularLocalRing R] (S : Finset R) exact Submodule.spanFinrank_span_le_ncard_of_finite (Set.toFinite (S ∪ U)) tfae_finish +lemma quotient_span_singleton [IsRegularLocalRing R] {x : R} (mem : x ∈ maximalIdeal R) + (nmem : x ∉ (maximalIdeal R) ^ 2) : IsRegularLocalRing (R ⧸ Ideal.span {x}) ∧ + (ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R) := by + have : ({x} : Finset R).toSet = {x} := by exact Finset.coe_singleton x + rw [← Nat.cast_one, ← Finset.card_singleton x, ← Finset.coe_singleton x] + apply ((quotient_isRegularLocalRing_tfae R {x} (by simpa)).out 1 2).mp + simpa [← LinearMap.mem_ker, Ideal.mem_toCotangent_ker] using nmem + +lemma exist_nat_eq [FiniteRingKrullDim R] : ∃ n : ℕ, ringKrullDim R = n := by + have : (ringKrullDim R).unbot ringKrullDim_ne_bot ≠ ⊤ := by + by_contra eq + rw [← WithBot.coe_inj, WithBot.coe_unbot, WithBot.coe_top] at eq + exact ringKrullDim_ne_top eq + use ((ringKrullDim R).unbot ringKrullDim_ne_bot).toNat + exact (WithBot.coe_unbot (ringKrullDim R) ringKrullDim_ne_bot).symm.trans + (WithBot.coe_inj.mpr (ENat.coe_toNat this).symm) + +open Pointwise in theorem isDomain_of_isRegularLocalRing [IsRegularLocalRing R] : IsDomain R := by - sorry + obtain ⟨n, hn⟩ := exist_nat_eq R + induction' n with n ih generalizing R + · simp only [← (isRegularLocalRing_iff R).mp ‹_›, CharP.cast_eq_zero, Nat.cast_eq_zero] at hn + have : maximalIdeal R = ⊥ := by + rw [← Submodule.spanRank_eq_zero_iff_eq_bot, Submodule.fg_iff_spanRank_eq_spanFinrank.mpr + ((isNoetherianRing_iff_ideal_fg R).mp inferInstance _), hn, Nat.cast_zero] + exact (isField_iff_maximalIdeal_eq.mpr this).isDomain + · obtain ⟨x, xmem, xnmem⟩ : ∃ x ∈ maximalIdeal R, + x ∉ ⋃ I ∈ {(maximalIdeal R) ^ 2} ∪ minimalPrimes R, I := by + by_contra! h + have fin : ({(maximalIdeal R) ^ 2} ∪ minimalPrimes R).Finite := + Set.Finite.union (Set.finite_singleton _) (minimalPrimes.finite_of_isNoetherianRing R) + rcases (Ideal.subset_union_prime_finite fin ((maximalIdeal R) ^ 2) ((maximalIdeal R) ^ 2) + (fun I hI ne _ ↦ Ideal.minimalPrimes_isPrime (by simpa [ne] using hI))).mp h with + ⟨I, hI, sub⟩ + simp only [Set.singleton_union, Set.mem_insert_iff] at hI + rcases hI with eq|min + · have : IsField R := by + simp only [← subsingleton_cotangentSpace_iff, Ideal.cotangent_subsingleton_iff, + IsIdempotentElem] + exact le_antisymm Ideal.mul_le_right (le_of_le_of_eq sub (eq.trans (pow_two _))) + rw [ringKrullDim_eq_zero_of_isField this, ← Nat.cast_zero, Nat.cast_inj] at hn + exact Nat.zero_ne_add_one n hn + · let _ : I.IsPrime := Ideal.minimalPrimes_isPrime min + rw [← Ideal.primeHeight_eq_ringKrullDim_iff.mpr (le_antisymm (le_maximalIdeal_of_isPrime I) + sub), Ideal.primeHeight_eq_zero_iff.mpr min, ← Nat.cast_zero] at hn + exact Nat.zero_ne_add_one n (Nat.cast_inj.mp hn) + simp only [Set.singleton_union, Set.mem_insert_iff, Set.iUnion_iUnion_eq_or_left, Set.mem_union, + SetLike.mem_coe, Set.mem_iUnion, exists_prop, not_or, not_exists, not_and] at xnmem + obtain ⟨reg, dim⟩ := quotient_span_singleton R xmem xnmem.1 + simp only [hn, Nat.cast_add, Nat.cast_one] at dim + have ih' := ih (R ⧸ Ideal.span {x}) ((withBotENat_add_coe_cancel _ _ 1).mp dim) + have : (Ideal.span {x}).IsPrime := (Ideal.Quotient.isDomain_iff_prime _).mp ih' + obtain ⟨p, min, hp⟩ := Ideal.exists_minimalPrimes_le (bot_le (a := Ideal.span {x})) + let _ : p.IsPrime := Ideal.minimalPrimes_isPrime min + have eq_smul : p = Ideal.span {x} • p := by + ext y + simp only [smul_eq_mul, Ideal.mem_span_singleton_mul] + refine ⟨fun h ↦ ?_, fun ⟨z, hz, eq⟩ ↦ by simpa [← eq] using Ideal.mul_mem_left p x hz⟩ + rcases Ideal.mem_span_singleton'.mp (hp h) with ⟨z, hz⟩ + use z + simp only [← hz, mul_comm, and_true] + have : z ∈ p ∨ x ∈ p := (Ideal.IsPrime.mem_or_mem ‹_› (by simpa [hz])) + simpa [xnmem.2 p min] using this + have pfg : p.FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _ + have := Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator pfg eq_smul + (le_trans ((Ideal.span_singleton_le_iff_mem _).mpr xmem) (maximalIdeal_le_jacobson _)) + have : (⊥ : Ideal R).IsPrime := by simpa [← this] + exact IsDomain.of_bot_isPrime R open RingTheory.Sequence in theorem isRegular_of_span_eq_maximalIdeal [IsRegularLocalRing R] (rs : List R) From dbbc1d0731694b8af68822fed97eecfa35ff9288 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 19 Aug 2025 20:43:17 +0800 Subject: [PATCH 04/64] Update RegularLocalRing.lean --- Mathlib/RingTheory/RegularLocalRing.lean | 63 +++++++++++++++++++++++- 1 file changed, 61 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing.lean b/Mathlib/RingTheory/RegularLocalRing.lean index 638f1521a04fe3..8d115cf63d55ce 100644 --- a/Mathlib/RingTheory/RegularLocalRing.lean +++ b/Mathlib/RingTheory/RegularLocalRing.lean @@ -347,8 +347,67 @@ theorem isDomain_of_isRegularLocalRing [IsRegularLocalRing R] : IsDomain R := by open RingTheory.Sequence in theorem isRegular_of_span_eq_maximalIdeal [IsRegularLocalRing R] (rs : List R) - (eq : Ideal.ofList rs = maximalIdeal R) (len : rs.length = ringKrullDim R) : + (span : Ideal.ofList rs = maximalIdeal R) (len : rs.length = ringKrullDim R) : IsRegular R rs := by - sorry + refine ⟨⟨fun i hi ↦ ?_⟩, by simpa [span] using Ideal.IsPrime.ne_top'.symm⟩ + rw [smul_eq_mul, Ideal.mul_top] + classical + have mem : (rs.toFinset : Set R) ⊆ maximalIdeal R := by + intro x hx + simp only [List.coe_toFinset, Set.mem_setOf_eq] at hx + exact Ideal.span_le.mp (le_of_eq span) hx + have sub : (List.take i rs).toFinset ⊆ rs.toFinset := + fun x ↦ by simpa using fun a ↦ List.mem_of_mem_take a + have card : rs.toFinset.card = ringKrullDim R := by + apply le_antisymm (le_of_le_of_eq (Nat.cast_le.mpr rs.toFinset_card_le) len) + simp only [← (isRegularLocalRing_iff R).mp ‹_›, Nat.cast_le, ← span, Ideal.ofList, + ← List.coe_toFinset rs] + exact le_of_le_of_eq (Submodule.spanFinrank_span_le_ncard_of_finite rs.toFinset.finite_toSet) + (Set.ncard_coe_finset rs.toFinset) + have reg := ((quotient_isRegularLocalRing_tfae R (List.take i rs).toFinset + ((Finset.coe_subset.mpr sub).trans mem)).out 0 2).mp (by + use rs.toFinset + simpa [sub, card] using span) + have : IsDomain (R ⧸ Ideal.ofList (List.take i rs)) := by + refine @isDomain_of_isRegularLocalRing _ _ ?_ + simp only [Ideal.ofList] + rw [← List.coe_toFinset (List.take i rs)] + exact reg.1 + apply IsSMulRegular.of_right_eq_zero_of_smul (fun x hx ↦ ?_) + have : (Ideal.Quotient.mk (Ideal.ofList (List.take i rs))) rs[i] ≠ 0 := by + simp only [ne_eq, Ideal.Quotient.eq_zero_iff_mem] + by_contra mem + simp only [← (isRegularLocalRing_iff R).mp ‹_›, Nat.cast_inj] at len + let rs' := (List.take i rs) ++ (List.drop (i + 1) rs) + have span' : Ideal.ofList rs' = maximalIdeal R := by + simp only [← span, rs'] + apply le_antisymm + · apply Ideal.span_mono (fun x ↦ ?_) + simpa [or_imp] using ⟨fun a ↦ List.mem_of_mem_take a, fun a ↦ List.mem_of_mem_drop a⟩ + · apply Ideal.span_le.mpr + intro x hx + have : rs = List.take i rs ++ (rs[i] :: List.drop (i + 1) rs) := by + rw [List.cons_getElem_drop_succ, List.take_append_drop] + rw [this] at hx + simp only [List.mem_append, List.mem_cons] at hx + simp only [Ideal.ofList_append, SetLike.mem_coe] + rcases hx with l|eq|r + · apply Ideal.mem_sup_left + apply Ideal.subset_span + exact l + · apply Ideal.mem_sup_left + simpa [eq] using mem + · apply Ideal.mem_sup_right + apply Ideal.subset_span + exact r + have : Submodule.spanFinrank (maximalIdeal R) ≤ rs'.length := by + rw [← span'] + apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite rs'.finite_toSet) + apply le_of_eq_of_le _ (List.toFinset_card_le rs') + simp [← (Set.ncard_coe_finset rs'.toFinset)] + simp only [← len, List.length_append, List.length_take, List.length_drop, rs'] at this + absurd this + omega + exact (mul_eq_zero_iff_left this).mp hx end From cb08e01fd7c8b157d745b86e7f193dbe1f334429 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Wed, 20 Aug 2025 16:18:14 +0800 Subject: [PATCH 05/64] Update RegularLocalRing.lean --- Mathlib/RingTheory/RegularLocalRing.lean | 307 +---------------------- 1 file changed, 2 insertions(+), 305 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing.lean b/Mathlib/RingTheory/RegularLocalRing.lean index 8d115cf63d55ce..3b000d3986e542 100644 --- a/Mathlib/RingTheory/RegularLocalRing.lean +++ b/Mathlib/RingTheory/RegularLocalRing.lean @@ -5,9 +5,6 @@ Authors: Nailin Guan -/ import Mathlib.RingTheory.Ideal.Cotangent import Mathlib.RingTheory.Ideal.KrullsHeightTheorem -import Mathlib.RingTheory.KrullDimension.NonZeroDivisors -import Mathlib.RingTheory.Regular.RegularSequence -import Mathlib.RingTheory.KrullDimension.Field /-! # Define Regular Local Ring -/ @@ -16,6 +13,8 @@ open IsLocalRing variable (R : Type*) [CommRing R] +/-- A noetherian local ring of dimesnion `d` is said to be regular if its maximal ideal +can be generated by `d` elements. -/ class IsRegularLocalRing : Prop extends IsLocalRing R, IsNoetherianRing R where reg : (Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R @@ -64,8 +63,6 @@ lemma isRegularLocalRing_of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommR · simpa [← ringKrullDim_eq_of_ringEquiv e, ← IsRegularLocalRing.reg, ← Submodule.FG.generators_ncard fg] using le_of_eq (Set.ncard_eq_toFinset_card' _).symm -section - lemma span_eq_top_iff [IsLocalRing R] (S : Set (maximalIdeal R)) : Submodule.span R S = ⊤ ↔ Submodule.span R ((Submodule.subtype (maximalIdeal R)) '' S) = maximalIdeal R := by @@ -111,303 +108,3 @@ lemma spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] : apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (Finite.image _ fin)) exact le_trans (Set.ncard_image_le fin) (Set.ncard_le_ncard_of_injOn Subtype.val (by simp [G]) injOn_subtype_val (Submodule.FG.finite_generators fg')) - -variable {R} in -lemma IsLocalRing.ResidueField.map_injective [IsLocalRing R] {S : Type*} [CommRing S] - [IsLocalRing S] (f : R →+* S) [IsLocalHom f] : - Function.Injective (ResidueField.map f) := by - rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] - intro x hx - simpa only [map_eq_zero] using hx - -variable {R} in -lemma IsLocalRing.ResidueField.map_bijective_of_surjective [IsLocalRing R] {S : Type*} [CommRing S] - [IsLocalRing S] (f : R →+* S) (surj : Function.Surjective f) [IsLocalHom f] : - Function.Bijective (ResidueField.map f) := by - refine ⟨ResidueField.map_injective f, ?_⟩ - apply Ideal.Quotient.lift_surjective_of_surjective - convert Function.Surjective.comp (Ideal.Quotient.mk_surjective (I := (maximalIdeal S))) surj - -variable {R} in -lemma _root_.ringKrullDim_le_ringKrullDim_add_card [IsLocalRing R] [IsNoetherianRing R] - {S : Finset R} (hS : (S : Set R) ⊆ maximalIdeal R) : - ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span S.toSet) + S.card := by - sorry - -lemma quotient_isRegularLocalRing_tfae [IsRegularLocalRing R] (S : Finset R) - (sub : (S : Set R) ⊆ maximalIdeal R) : - [∃ (T : Finset R), S ⊆ T ∧ T.card = ringKrullDim R ∧ Ideal.span T = maximalIdeal R, - LinearIndependent (ResidueField R) ((⇑(maximalIdeal R).toCotangent).comp (Set.inclusion sub)), - IsRegularLocalRing (R ⧸ Ideal.span (S : Set R)) ∧ - (ringKrullDim (R ⧸ Ideal.span (S : Set R)) + S.card = ringKrullDim R)].TFAE := by - have : Nontrivial (R ⧸ Ideal.span S.toSet) := - Ideal.Quotient.nontrivial (ne_top_of_le_ne_top Ideal.IsPrime.ne_top' (Ideal.span_le.mpr sub)) - have lochom : IsLocalHom (Ideal.Quotient.mk (Ideal.span S.toSet)) := - IsLocalHom.of_surjective _ (Ideal.Quotient.mk_surjective) - tfae_have 1 → 2 := by - rintro ⟨T, h, card, span⟩ - have Tsub : (T : Set R) ⊆ maximalIdeal R := by simpa [← span] using Ideal.subset_span - have : LinearIndependent (ResidueField R) - ((⇑(maximalIdeal R).toCotangent).comp (Set.inclusion Tsub)) := by - apply linearIndependent_of_top_le_span_of_card_eq_finrank - · simp only [Finset.coe_sort_coe, Set.range_comp, Set.range_inclusion Tsub, - SetLike.coe_sort_coe, Finset.mem_coe, top_le_iff, - IsLocalRing.CotangentSpace.span_image_eq_top_iff] - simp only [span_eq_top_iff, Submodule.subtype_apply, Ideal.submodule_span_eq] - convert span - ext - simpa using fun a ↦ Tsub a - · rw [← spanFinrank_maximalIdeal R, ← Nat.cast_inj (R := WithBot ℕ∞), - (isRegularLocalRing_iff R).mp ‹_›, ← card] - simp - have li := LinearIndependent.comp this (Set.inclusion h) (Set.inclusion_injective h) - have inc : Set.inclusion Tsub ∘ Set.inclusion h = Set.inclusion sub := rfl - simpa [← Function.comp_assoc, ← inc] using li - tfae_have 2 → 3 := by - intro li - let _ : IsLocalRing (R ⧸ Ideal.span S.toSet) := - IsLocalRing.of_surjective _ Ideal.Quotient.mk_surjective - rw [isRegularLocalRing_iff] - have le := ringKrullDim_le_ringKrullDim_add_card sub - have ge : (Submodule.spanFinrank (maximalIdeal (R ⧸ Ideal.span S.toSet))) + S.card ≤ - ringKrullDim R := by - simp only [← Nat.cast_add, ← (isRegularLocalRing_iff R).mp ‹_›, Nat.cast_le, - spanFinrank_maximalIdeal] - let f := Ideal.mapCotangent (maximalIdeal R) (maximalIdeal (R ⧸ Ideal.span S.toSet)) - (Ideal.Quotient.mkₐ R (Ideal.span S.toSet)) (fun x hx ↦ by simpa) - have ker : (LinearMap.ker f : Set (maximalIdeal R).Cotangent) = (Submodule.span - (ResidueField R) (Set.range (⇑(maximalIdeal R).toCotangent ∘ Set.inclusion sub))) := by - simp only [ Submodule.coe_span_eq_span_of_surjective R (ResidueField R) - IsLocalRing.residue_surjective, Finset.coe_sort_coe, SetLike.coe_set_eq] - ext x - induction' x using Submodule.Quotient.induction_on with x - simp only [Ideal.mapCotangent, LinearMap.mem_ker, f] - change (maximalIdeal (R ⧸ Ideal.span S.toSet)).toCotangent ⟨(Ideal.Quotient.mkₐ R - (Ideal.span S.toSet)) x, _⟩ = 0 ↔ (maximalIdeal R).toCotangent x ∈ _ - simp only [Ideal.Quotient.mkₐ_eq_mk, Set.range_comp, - Submodule.span_image', Ideal.toCotangent_eq_zero] - have : maximalIdeal (R ⧸ Ideal.span S.toSet) = - (maximalIdeal R).map (Ideal.Quotient.mk _) := by - simp only [← ((local_hom_TFAE _).out 0 4).mp lochom, - Ideal.map_comap_of_surjective _ Ideal.Quotient.mk_surjective] - rw [this, ← Ideal.map_pow, ← Ideal.mem_comap, ← Submodule.mem_comap, Submodule.comap_map_eq, - Ideal.comap_map_of_surjective' _ Ideal.Quotient.mk_surjective, Ideal.mk_ker, sup_comm, - ← Submodule.comap_map_eq_of_injective (maximalIdeal R).subtype_injective (Submodule.span - R (Set.range (Set.inclusion sub)) ⊔ LinearMap.ker (maximalIdeal R).toCotangent)] - simp only [Finset.coe_sort_coe, Submodule.map_sup, Submodule.mem_comap, - Submodule.subtype_apply] - congr! - · simp only [Submodule.map_span, Submodule.subtype_apply, Ideal.submodule_span_eq] - congr - ext - simpa using fun a ↦ sub a - · exact (Ideal.map_toCotangent_ker (maximalIdeal R)).symm - let Q := (CotangentSpace R) ⧸ (Submodule.span (ResidueField R) - (Set.range (⇑(maximalIdeal R).toCotangent ∘ Set.inclusion sub))) - let f' : Q →+ (CotangentSpace (R ⧸ Ideal.span S.toSet)) := - QuotientAddGroup.lift _ f - (le_of_eq (AddSubgroup.ext (fun x ↦ (congrFun ker.symm x).to_iff))) - have bij : Function.Bijective f' := by - constructor - · rw [← AddMonoidHom.ker_eq_bot_iff, eq_bot_iff] - intro x hx - induction' x using QuotientAddGroup.induction_on with x - have : x ∈ (LinearMap.ker f : Set (maximalIdeal R).Cotangent) := LinearMap.mem_ker.mpr hx - rw [ker] at this - exact AddSubgroup.mem_bot.mpr ((QuotientAddGroup.eq_zero_iff _).mpr this) - · apply QuotientAddGroup.lift_surjective_of_surjective - intro x - rcases Ideal.toCotangent_surjective _ x with ⟨y, hy⟩ - rcases Ideal.Quotient.mk_surjective y.1 with ⟨z, hz⟩ - have : z ∈ maximalIdeal R := by simp [← ((local_hom_TFAE _).out 0 4).mp lochom, hz] - use (maximalIdeal R).toCotangent ⟨z, this⟩ - simp [f, ← hy, hz] - let e : Q ≃+ (CotangentSpace (R ⧸ Ideal.span S.toSet)) := - AddEquiv.ofBijective f' bij - have rk := rank_eq_of_equiv_equiv (ResidueField.map (Ideal.Quotient.mk (Ideal.span S.toSet))) - e (ResidueField.map_bijective_of_surjective _ Ideal.Quotient.mk_surjective) (fun r m ↦ by - induction' m using Submodule.Quotient.induction_on with m - rw [← Submodule.Quotient.mk_smul] - simp only [Finset.coe_sort_coe, AddEquiv.ofBijective_apply, e, f'] - induction' r using Submodule.Quotient.induction_on with r - change f (r • m) = (ResidueField.map (Ideal.Quotient.mk (Ideal.span S.toSet))) - (IsLocalRing.residue R r) • (f m) - simp only [map_smul] - rfl) - have frk : Module.finrank (ResidueField R) Q = Module.finrank - (ResidueField (R ⧸ Ideal.span S.toSet)) (CotangentSpace (R ⧸ Ideal.span S.toSet)) := by - simp [Module.finrank, rk] - have : Fintype.card S.toSet = S.card := Fintype.card_ofFinset S (fun x ↦ Finset.mem_coe) - rw [← frk, ← this, ← finrank_span_eq_card li] - apply Module.finrank_quotient_add_finrank_le - have : ringKrullDim (R ⧸ Ideal.span S.toSet) + S.card ≤ - (Submodule.spanFinrank (maximalIdeal (R ⧸ Ideal.span S.toSet))) + S.card := - add_le_add_right (ringKrullDim_le_spanFinrank_maximalIdeal _) _ - exact ⟨(withBotENat_add_coe_cancel _ _ S.card).mp - (le_antisymm (ge.trans le) this), le_antisymm (this.trans ge) le⟩ - tfae_have 3 → 1 := by - classical - rintro ⟨reg, dim⟩ - simp only [← (isRegularLocalRing_iff _).mp reg, ← Nat.cast_add, ← - (isRegularLocalRing_iff R).mp ‹_›, Nat.cast_inj] at dim - let fg : (maximalIdeal (R ⧸ Ideal.span S.toSet)).FG := - (isNoetherianRing_iff_ideal_fg _).mp inferInstance _ - have fin : (maximalIdeal (R ⧸ Ideal.span S.toSet)).generators.Finite := - Submodule.FG.finite_generators fg - let U := Quotient.out '' (maximalIdeal (R ⧸ Ideal.span S.toSet)).generators - let _ : Fintype U := (Set.Finite.image _ fin).fintype - use S ∪ U.toFinset - have span : Ideal.span (S ∪ U) = maximalIdeal R := by - rw [Ideal.span_union, ← Ideal.mk_ker (I := Ideal.span S.toSet), sup_comm, - ← Ideal.comap_map_of_surjective' _ Ideal.Quotient.mk_surjective, Ideal.map_span] - have : Ideal.span (⇑(Ideal.Quotient.mk (Ideal.span ↑S)) '' U) = - Submodule.span _ (maximalIdeal (R ⧸ Ideal.span S.toSet)).generators := by - simp [U, ← Set.image_comp] - rw [this, Submodule.span_generators] - exact ((local_hom_TFAE _).out 0 4).mp lochom - simp only [Finset.subset_union_left, true_and, ← (isRegularLocalRing_iff R).mp ‹_›, - Finset.coe_union, Set.coe_toFinset] - refine ⟨le_antisymm ?_ ?_, span⟩ - · apply Nat.cast_le.mpr (le_trans (Finset.card_union_le _ _) _) - simp only [Set.toFinset_card, ← dim, add_comm, add_le_add_iff_left] - rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] - apply le_trans (Set.ncard_image_le fin) (le_of_eq (Submodule.FG.generators_ncard fg)) - · simp only [← span, ← Set.ncard_coe_finset, Finset.coe_union, Set.coe_toFinset, Nat.cast_le] - exact Submodule.spanFinrank_span_le_ncard_of_finite (Set.toFinite (S ∪ U)) - tfae_finish - -lemma quotient_span_singleton [IsRegularLocalRing R] {x : R} (mem : x ∈ maximalIdeal R) - (nmem : x ∉ (maximalIdeal R) ^ 2) : IsRegularLocalRing (R ⧸ Ideal.span {x}) ∧ - (ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R) := by - have : ({x} : Finset R).toSet = {x} := by exact Finset.coe_singleton x - rw [← Nat.cast_one, ← Finset.card_singleton x, ← Finset.coe_singleton x] - apply ((quotient_isRegularLocalRing_tfae R {x} (by simpa)).out 1 2).mp - simpa [← LinearMap.mem_ker, Ideal.mem_toCotangent_ker] using nmem - -lemma exist_nat_eq [FiniteRingKrullDim R] : ∃ n : ℕ, ringKrullDim R = n := by - have : (ringKrullDim R).unbot ringKrullDim_ne_bot ≠ ⊤ := by - by_contra eq - rw [← WithBot.coe_inj, WithBot.coe_unbot, WithBot.coe_top] at eq - exact ringKrullDim_ne_top eq - use ((ringKrullDim R).unbot ringKrullDim_ne_bot).toNat - exact (WithBot.coe_unbot (ringKrullDim R) ringKrullDim_ne_bot).symm.trans - (WithBot.coe_inj.mpr (ENat.coe_toNat this).symm) - -open Pointwise in -theorem isDomain_of_isRegularLocalRing [IsRegularLocalRing R] : IsDomain R := by - obtain ⟨n, hn⟩ := exist_nat_eq R - induction' n with n ih generalizing R - · simp only [← (isRegularLocalRing_iff R).mp ‹_›, CharP.cast_eq_zero, Nat.cast_eq_zero] at hn - have : maximalIdeal R = ⊥ := by - rw [← Submodule.spanRank_eq_zero_iff_eq_bot, Submodule.fg_iff_spanRank_eq_spanFinrank.mpr - ((isNoetherianRing_iff_ideal_fg R).mp inferInstance _), hn, Nat.cast_zero] - exact (isField_iff_maximalIdeal_eq.mpr this).isDomain - · obtain ⟨x, xmem, xnmem⟩ : ∃ x ∈ maximalIdeal R, - x ∉ ⋃ I ∈ {(maximalIdeal R) ^ 2} ∪ minimalPrimes R, I := by - by_contra! h - have fin : ({(maximalIdeal R) ^ 2} ∪ minimalPrimes R).Finite := - Set.Finite.union (Set.finite_singleton _) (minimalPrimes.finite_of_isNoetherianRing R) - rcases (Ideal.subset_union_prime_finite fin ((maximalIdeal R) ^ 2) ((maximalIdeal R) ^ 2) - (fun I hI ne _ ↦ Ideal.minimalPrimes_isPrime (by simpa [ne] using hI))).mp h with - ⟨I, hI, sub⟩ - simp only [Set.singleton_union, Set.mem_insert_iff] at hI - rcases hI with eq|min - · have : IsField R := by - simp only [← subsingleton_cotangentSpace_iff, Ideal.cotangent_subsingleton_iff, - IsIdempotentElem] - exact le_antisymm Ideal.mul_le_right (le_of_le_of_eq sub (eq.trans (pow_two _))) - rw [ringKrullDim_eq_zero_of_isField this, ← Nat.cast_zero, Nat.cast_inj] at hn - exact Nat.zero_ne_add_one n hn - · let _ : I.IsPrime := Ideal.minimalPrimes_isPrime min - rw [← Ideal.primeHeight_eq_ringKrullDim_iff.mpr (le_antisymm (le_maximalIdeal_of_isPrime I) - sub), Ideal.primeHeight_eq_zero_iff.mpr min, ← Nat.cast_zero] at hn - exact Nat.zero_ne_add_one n (Nat.cast_inj.mp hn) - simp only [Set.singleton_union, Set.mem_insert_iff, Set.iUnion_iUnion_eq_or_left, Set.mem_union, - SetLike.mem_coe, Set.mem_iUnion, exists_prop, not_or, not_exists, not_and] at xnmem - obtain ⟨reg, dim⟩ := quotient_span_singleton R xmem xnmem.1 - simp only [hn, Nat.cast_add, Nat.cast_one] at dim - have ih' := ih (R ⧸ Ideal.span {x}) ((withBotENat_add_coe_cancel _ _ 1).mp dim) - have : (Ideal.span {x}).IsPrime := (Ideal.Quotient.isDomain_iff_prime _).mp ih' - obtain ⟨p, min, hp⟩ := Ideal.exists_minimalPrimes_le (bot_le (a := Ideal.span {x})) - let _ : p.IsPrime := Ideal.minimalPrimes_isPrime min - have eq_smul : p = Ideal.span {x} • p := by - ext y - simp only [smul_eq_mul, Ideal.mem_span_singleton_mul] - refine ⟨fun h ↦ ?_, fun ⟨z, hz, eq⟩ ↦ by simpa [← eq] using Ideal.mul_mem_left p x hz⟩ - rcases Ideal.mem_span_singleton'.mp (hp h) with ⟨z, hz⟩ - use z - simp only [← hz, mul_comm, and_true] - have : z ∈ p ∨ x ∈ p := (Ideal.IsPrime.mem_or_mem ‹_› (by simpa [hz])) - simpa [xnmem.2 p min] using this - have pfg : p.FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _ - have := Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator pfg eq_smul - (le_trans ((Ideal.span_singleton_le_iff_mem _).mpr xmem) (maximalIdeal_le_jacobson _)) - have : (⊥ : Ideal R).IsPrime := by simpa [← this] - exact IsDomain.of_bot_isPrime R - -open RingTheory.Sequence in -theorem isRegular_of_span_eq_maximalIdeal [IsRegularLocalRing R] (rs : List R) - (span : Ideal.ofList rs = maximalIdeal R) (len : rs.length = ringKrullDim R) : - IsRegular R rs := by - refine ⟨⟨fun i hi ↦ ?_⟩, by simpa [span] using Ideal.IsPrime.ne_top'.symm⟩ - rw [smul_eq_mul, Ideal.mul_top] - classical - have mem : (rs.toFinset : Set R) ⊆ maximalIdeal R := by - intro x hx - simp only [List.coe_toFinset, Set.mem_setOf_eq] at hx - exact Ideal.span_le.mp (le_of_eq span) hx - have sub : (List.take i rs).toFinset ⊆ rs.toFinset := - fun x ↦ by simpa using fun a ↦ List.mem_of_mem_take a - have card : rs.toFinset.card = ringKrullDim R := by - apply le_antisymm (le_of_le_of_eq (Nat.cast_le.mpr rs.toFinset_card_le) len) - simp only [← (isRegularLocalRing_iff R).mp ‹_›, Nat.cast_le, ← span, Ideal.ofList, - ← List.coe_toFinset rs] - exact le_of_le_of_eq (Submodule.spanFinrank_span_le_ncard_of_finite rs.toFinset.finite_toSet) - (Set.ncard_coe_finset rs.toFinset) - have reg := ((quotient_isRegularLocalRing_tfae R (List.take i rs).toFinset - ((Finset.coe_subset.mpr sub).trans mem)).out 0 2).mp (by - use rs.toFinset - simpa [sub, card] using span) - have : IsDomain (R ⧸ Ideal.ofList (List.take i rs)) := by - refine @isDomain_of_isRegularLocalRing _ _ ?_ - simp only [Ideal.ofList] - rw [← List.coe_toFinset (List.take i rs)] - exact reg.1 - apply IsSMulRegular.of_right_eq_zero_of_smul (fun x hx ↦ ?_) - have : (Ideal.Quotient.mk (Ideal.ofList (List.take i rs))) rs[i] ≠ 0 := by - simp only [ne_eq, Ideal.Quotient.eq_zero_iff_mem] - by_contra mem - simp only [← (isRegularLocalRing_iff R).mp ‹_›, Nat.cast_inj] at len - let rs' := (List.take i rs) ++ (List.drop (i + 1) rs) - have span' : Ideal.ofList rs' = maximalIdeal R := by - simp only [← span, rs'] - apply le_antisymm - · apply Ideal.span_mono (fun x ↦ ?_) - simpa [or_imp] using ⟨fun a ↦ List.mem_of_mem_take a, fun a ↦ List.mem_of_mem_drop a⟩ - · apply Ideal.span_le.mpr - intro x hx - have : rs = List.take i rs ++ (rs[i] :: List.drop (i + 1) rs) := by - rw [List.cons_getElem_drop_succ, List.take_append_drop] - rw [this] at hx - simp only [List.mem_append, List.mem_cons] at hx - simp only [Ideal.ofList_append, SetLike.mem_coe] - rcases hx with l|eq|r - · apply Ideal.mem_sup_left - apply Ideal.subset_span - exact l - · apply Ideal.mem_sup_left - simpa [eq] using mem - · apply Ideal.mem_sup_right - apply Ideal.subset_span - exact r - have : Submodule.spanFinrank (maximalIdeal R) ≤ rs'.length := by - rw [← span'] - apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite rs'.finite_toSet) - apply le_of_eq_of_le _ (List.toFinset_card_le rs') - simp [← (Set.ncard_coe_finset rs'.toFinset)] - simp only [← len, List.length_append, List.length_take, List.length_drop, rs'] at this - absurd this - omega - exact (mul_eq_zero_iff_left this).mp hx - -end From 1409e5547b484d150ca659d1405d881d15db048a Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Wed, 20 Aug 2025 19:51:03 +0800 Subject: [PATCH 06/64] rearrange lemmas and add docstring --- Mathlib/RingTheory/RegularLocalRing.lean | 71 +++++++++++++----------- 1 file changed, 39 insertions(+), 32 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing.lean b/Mathlib/RingTheory/RegularLocalRing.lean index 3b000d3986e542..beef3d9032d2cf 100644 --- a/Mathlib/RingTheory/RegularLocalRing.lean +++ b/Mathlib/RingTheory/RegularLocalRing.lean @@ -7,6 +7,19 @@ import Mathlib.RingTheory.Ideal.Cotangent import Mathlib.RingTheory.Ideal.KrullsHeightTheorem /-! # Define Regular Local Ring + +For a noetherian local ring `R`, we define `IsRegularLocalRing` as +`(maximalIdeal R).spanFinrank = ringKrullDim R` + +# Main Definition and Results + +* `IsRegularLocalRing` : A noetherian local ring of dimesnion `d` `IsRegularLocalRing` if + `(maximalIdeal R).spanFinrank = ringKrullDim R`, + i.e. its maximal ideal can be generated by `d` elements. + +* `isRegularLocalRing_iff` : the equivalence of `IsRegularLocalRing` and + `Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R` + -/ open IsLocalRing @@ -16,52 +29,43 @@ variable (R : Type*) [CommRing R] /-- A noetherian local ring of dimesnion `d` is said to be regular if its maximal ideal can be generated by `d` elements. -/ class IsRegularLocalRing : Prop extends IsLocalRing R, IsNoetherianRing R where - reg : (Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R + reg : (maximalIdeal R).spanFinrank = ringKrullDim R -lemma isRegularLocalRing_iff [IsLocalRing R] [IsNoetherianRing R] : - IsRegularLocalRing R ↔ (Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R := +lemma isRegularLocalRing_def [IsLocalRing R] [IsNoetherianRing R] : + IsRegularLocalRing R ↔ (maximalIdeal R).spanFinrank = ringKrullDim R := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩ lemma ringKrullDim_le_spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] : - ringKrullDim R ≤ (Submodule.spanFinrank (maximalIdeal R)) := + ringKrullDim R ≤ (maximalIdeal R).spanFinrank := le_of_eq_of_le IsLocalRing.maximalIdeal_height_eq_ringKrullDim.symm (WithBot.coe_le_coe.mpr (Ideal.height_le_spanFinrank (maximalIdeal R) Ideal.IsPrime.ne_top')) -lemma isRegularLocalRing_of_exist_span [IsLocalRing R] [IsNoetherianRing R] (S : Finset R) - (span : Ideal.span S = maximalIdeal R) (card : S.card ≤ ringKrullDim R) : +namespace IsRegularLocalRing + +lemma of_exist_span [IsLocalRing R] [IsNoetherianRing R] (S : Set R) (fin : S.Finite) + (span : Ideal.span S = maximalIdeal R) (card : S.ncard ≤ ringKrullDim R) : IsRegularLocalRing R := by - apply (isRegularLocalRing_iff _).mpr (le_antisymm _ (ringKrullDim_le_spanFinrank_maximalIdeal R)) + apply (isRegularLocalRing_def _).mpr (le_antisymm _ (ringKrullDim_le_spanFinrank_maximalIdeal R)) apply le_trans _ card - rw [← span, ← Ideal.submodule_span_eq, ← Set.ncard_coe_finset S, Nat.cast_le] - exact Submodule.spanFinrank_span_le_ncard_of_finite S.finite_toSet + rw [← span, ← Ideal.submodule_span_eq] + simpa using Submodule.spanFinrank_span_le_ncard_of_finite fin variable {R} in -lemma IsLocalRing.comap_maximalIdeal [IsLocalRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] - (e : R ≃+* R') : maximalIdeal R = Ideal.comap e (maximalIdeal R') := by - ext - simp - -variable {R} in -lemma IsLocalRing.map_maximalIdeal [IsLocalRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] - (e : R ≃+* R') : Ideal.map e (maximalIdeal R) = maximalIdeal R' := by - rw [← Ideal.map_comap_of_surjective _ e.surjective (maximalIdeal R'), - IsLocalRing.comap_maximalIdeal e] - -variable {R} in -lemma isRegularLocalRing_of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R'] +lemma of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R'] (e : R ≃+* R') : IsRegularLocalRing R' := by let _ := e.isLocalRing let _ := isNoetherianRing_of_ringEquiv R e have fg : (maximalIdeal R).FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _ - let _ : Fintype (Submodule.generators (maximalIdeal R)) := - (Submodule.FG.finite_generators fg).fintype - apply isRegularLocalRing_of_exist_span R' ((maximalIdeal R).generators.toFinset.map e.toEmbedding) - · simp only [RingEquiv.toEquiv_eq_coe, Finset.coe_map, Equiv.coe_toEmbedding, EquivLike.coe_coe, - Set.coe_toFinset, ← Ideal.map_span] - rw [← Ideal.submodule_span_eq, Submodule.span_generators (maximalIdeal R)] - exact IsLocalRing.map_maximalIdeal e + apply of_exist_span R' (e '' (maximalIdeal R).generators) + ((Submodule.FG.finite_generators fg).image _) + · simp only [← Ideal.map_span] + rw [← Ideal.submodule_span_eq, Submodule.span_generators (maximalIdeal R), ← Ideal.comap_symm] + exact ((local_hom_TFAE e.symm.toRingHom).out 0 4).mp (e.symm.surjective.isLocalHom _) · simpa [← ringKrullDim_eq_of_ringEquiv e, ← IsRegularLocalRing.reg, - ← Submodule.FG.generators_ncard fg] using le_of_eq (Set.ncard_eq_toFinset_card' _).symm + ← Submodule.FG.generators_ncard fg] using + Set.ncard_image_le (Submodule.FG.finite_generators fg) + +end IsRegularLocalRing lemma span_eq_top_iff [IsLocalRing R] (S : Set (maximalIdeal R)) : Submodule.span R S = ⊤ ↔ Submodule.span R ((Submodule.subtype (maximalIdeal R)) '' S) = @@ -73,8 +77,7 @@ lemma span_eq_top_iff [IsLocalRing R] (S : Set (maximalIdeal R)) : open Set in lemma spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] : - (Submodule.spanFinrank (maximalIdeal R)) = - Module.finrank (ResidueField R) (CotangentSpace R) := by + (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := by let fg : Module.Finite (ResidueField R) (CotangentSpace R) := inferInstance let fg' : (maximalIdeal R).FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _ have : Submodule.spanFinrank (⊤ : Submodule (ResidueField R) (CotangentSpace R)) = @@ -108,3 +111,7 @@ lemma spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] : apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (Finite.image _ fin)) exact le_trans (Set.ncard_image_le fin) (Set.ncard_le_ncard_of_injOn Subtype.val (by simp [G]) injOn_subtype_val (Submodule.FG.finite_generators fg')) + +lemma isRegularLocalRing_iff [IsLocalRing R] [IsNoetherianRing R] : + IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by + rw [isRegularLocalRing_def, spanFinrank_maximalIdeal] From f0eee4791f9aebc4cee87dd8bebd80f8f2b8a924 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Wed, 20 Aug 2025 19:53:49 +0800 Subject: [PATCH 07/64] fix lemma name --- Mathlib/RingTheory/RegularLocalRing.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing.lean b/Mathlib/RingTheory/RegularLocalRing.lean index beef3d9032d2cf..b0e5ce6be0f1df 100644 --- a/Mathlib/RingTheory/RegularLocalRing.lean +++ b/Mathlib/RingTheory/RegularLocalRing.lean @@ -42,7 +42,7 @@ lemma ringKrullDim_le_spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing namespace IsRegularLocalRing -lemma of_exist_span [IsLocalRing R] [IsNoetherianRing R] (S : Set R) (fin : S.Finite) +lemma of_span_eq [IsLocalRing R] [IsNoetherianRing R] (S : Set R) (fin : S.Finite) (span : Ideal.span S = maximalIdeal R) (card : S.ncard ≤ ringKrullDim R) : IsRegularLocalRing R := by apply (isRegularLocalRing_def _).mpr (le_antisymm _ (ringKrullDim_le_spanFinrank_maximalIdeal R)) @@ -56,7 +56,7 @@ lemma of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R'] let _ := e.isLocalRing let _ := isNoetherianRing_of_ringEquiv R e have fg : (maximalIdeal R).FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _ - apply of_exist_span R' (e '' (maximalIdeal R).generators) + apply of_span_eq R' (e '' (maximalIdeal R).generators) ((Submodule.FG.finite_generators fg).image _) · simp only [← Ideal.map_span] rw [← Ideal.submodule_span_eq, Submodule.span_generators (maximalIdeal R), ← Ideal.comap_symm] From df1e3dfe8ba66f76024cc97ca564545774d961b5 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Wed, 20 Aug 2025 20:38:38 +0800 Subject: [PATCH 08/64] Revert "Update Basic.lean" This reverts commit 78b6206849494870a63b1c3e19b2494c5f32e054. --- Mathlib/Data/ENat/Basic.lean | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean index 1d380ff1c89ae7..b79d05fc49eb68 100644 --- a/Mathlib/Data/ENat/Basic.lean +++ b/Mathlib/Data/ENat/Basic.lean @@ -567,21 +567,3 @@ lemma WithBot.add_one_le_iff {n : ℕ} {m : WithBot ℕ∞} : n + 1 ≤ m ↔ n · simp · rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n), ← WithBot.coe_lt_coe, WithBot.coe_natCast] - -lemma ENat.add_right_cancel_iff (a b c : ℕ∞) (netop : c ≠ ⊤) : a + c = b + c ↔ a = b := - ⟨fun h ↦ ENat.add_left_injective_of_ne_top netop h, fun h ↦ by rw [h]⟩ - -lemma withBotENat_add_coe_cancel (a b : WithBot ℕ∞) (c : ℕ) : a + c = b + c ↔ a = b := by - refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩ - by_cases eqbot : a = ⊥ - · simp [eqbot, WithBot.bot_add] at h - rw [WithBot.add_coe_eq_bot_iff.mp h.symm, eqbot] - · by_cases eqbot' : b = ⊥ - · absurd eqbot - simpa [eqbot'] using h - · have : a.unbot eqbot + c = b.unbot eqbot' + c := by - apply WithBot.coe_inj.mp - convert h - repeat simpa using by rfl - rw [← WithBot.coe_unbot a eqbot, ← WithBot.coe_unbot b eqbot', WithBot.coe_inj] - simpa [ENat.add_right_cancel_iff _ _ _ (ENat.coe_ne_top c)] using this From f525679c392ddb3c42c69582215b09790cba9921 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 26 Aug 2025 14:06:29 +0800 Subject: [PATCH 09/64] Move Regular Local ring into folder --- Mathlib.lean | 2 +- .../{RegularLocalRing.lean => RegularLocalRing/Defs.lean} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename Mathlib/RingTheory/{RegularLocalRing.lean => RegularLocalRing/Defs.lean} (100%) diff --git a/Mathlib.lean b/Mathlib.lean index 4d06c1e963265b..951829b30d55a0 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5661,7 +5661,7 @@ import Mathlib.RingTheory.Regular.Category import Mathlib.RingTheory.Regular.Depth import Mathlib.RingTheory.Regular.IsSMulRegular import Mathlib.RingTheory.Regular.RegularSequence -import Mathlib.RingTheory.RegularLocalRing +import Mathlib.RingTheory.RegularLocalRing.Defs import Mathlib.RingTheory.RingHom.Etale import Mathlib.RingTheory.RingHom.FaithfullyFlat import Mathlib.RingTheory.RingHom.Finite diff --git a/Mathlib/RingTheory/RegularLocalRing.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean similarity index 100% rename from Mathlib/RingTheory/RegularLocalRing.lean rename to Mathlib/RingTheory/RegularLocalRing/Defs.lean From 5bce00024417e98bd130bb1a4973e40874c1be44 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 26 Aug 2025 15:57:34 +0800 Subject: [PATCH 10/64] fix lemma name --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 29 +++++++++---------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index b0e5ce6be0f1df..1695fde35a3489 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -9,7 +9,9 @@ import Mathlib.RingTheory.Ideal.KrullsHeightTheorem # Define Regular Local Ring For a noetherian local ring `R`, we define `IsRegularLocalRing` as -`(maximalIdeal R).spanFinrank = ringKrullDim R` +`(maximalIdeal R).spanFinrank = ringKrullDim R`. This definition is equivalent to +the dimension of the cotangent space over the residue field being equal to `ringKrullDim R`, +(see `IsRegularLocalRing.iff_finrank_cotangentSpace`). # Main Definition and Results @@ -17,7 +19,7 @@ For a noetherian local ring `R`, we define `IsRegularLocalRing` as `(maximalIdeal R).spanFinrank = ringKrullDim R`, i.e. its maximal ideal can be generated by `d` elements. -* `isRegularLocalRing_iff` : the equivalence of `IsRegularLocalRing` and +* `IsRegularLocalRing.iff_finrank_cotangentSpace` : the equivalence of `IsRegularLocalRing` and `Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R` -/ @@ -67,17 +69,14 @@ lemma of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R'] end IsRegularLocalRing -lemma span_eq_top_iff [IsLocalRing R] (S : Set (maximalIdeal R)) : - Submodule.span R S = ⊤ ↔ Submodule.span R ((Submodule.subtype (maximalIdeal R)) '' S) = - maximalIdeal R := by - rw [← Submodule.map_span] - refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩ - rw [← Submodule.comap_map_eq_of_injective (maximalIdeal R).injective_subtype - (Submodule.span R S), h, Submodule.comap_subtype_self] - open Set in -lemma spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] : +lemma IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace + [IsLocalRing R] [IsNoetherianRing R] : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := by + have eqtop (S : Set (maximalIdeal R)) : Submodule.span R S = ⊤ ↔ + Submodule.span R ((Submodule.subtype (maximalIdeal R)) '' S) = maximalIdeal R := by + simp only [← Submodule.map_span, ← (maximalIdeal R).range_subtype , ← Submodule.map_top, + (Submodule.map_injective_of_injective (maximalIdeal R).injective_subtype).eq_iff] let fg : Module.Finite (ResidueField R) (CotangentSpace R) := inferInstance let fg' : (maximalIdeal R).FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _ have : Submodule.spanFinrank (⊤ : Submodule (ResidueField R) (CotangentSpace R)) = @@ -94,13 +93,13 @@ lemma spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] : ext exact Submodule.Quotient.mk_out _ rw [← Set.image_comp, this, image_id] - rw [span_eq_top_iff, ← Set.image_comp] at span + rw [eqtop, ← Set.image_comp] at span rw [← Submodule.FG.generators_ncard fg.1, ← congrArg Submodule.spanFinrank span] apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (Finite.image _ fg.1.finite_generators)) (Set.ncard_image_le fg.1.finite_generators) · let G := ({x | ↑x ∈ (maximalIdeal R).generators} : Set (maximalIdeal R)) have : Submodule.span R G = ⊤ := by - simp only [span_eq_top_iff, Submodule.subtype_apply, Ideal.submodule_span_eq, G] + simp only [eqtop, Submodule.subtype_apply, Ideal.submodule_span_eq, G] convert (maximalIdeal R).span_generators ext simpa using fun a ↦ Submodule.FG.generators_mem (maximalIdeal R) a @@ -112,6 +111,6 @@ lemma spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] : exact le_trans (Set.ncard_image_le fin) (Set.ncard_le_ncard_of_injOn Subtype.val (by simp [G]) injOn_subtype_val (Submodule.FG.finite_generators fg')) -lemma isRegularLocalRing_iff [IsLocalRing R] [IsNoetherianRing R] : +lemma IsRegularLocalRing.iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by - rw [isRegularLocalRing_def, spanFinrank_maximalIdeal] + rw [isRegularLocalRing_def, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace] From 26a27a54e2b8a101ff33675a81767e9132a6391e Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 20 Nov 2025 15:22:25 +0800 Subject: [PATCH 11/64] Update Mathlib.lean --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 3a6d06bb68a207..3697f1580db688 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6051,6 +6051,7 @@ public import Mathlib.RingTheory.Regular.Depth public import Mathlib.RingTheory.Regular.Flat public import Mathlib.RingTheory.Regular.IsSMulRegular public import Mathlib.RingTheory.Regular.RegularSequence +public import Mathlib.RingTheory.RegularLocalRing.Defs public import Mathlib.RingTheory.RingHom.Bijective public import Mathlib.RingTheory.RingHom.Etale public import Mathlib.RingTheory.RingHom.FaithfullyFlat From edeab4df97016c80339eeade7c0a409472467ea1 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 20 Nov 2025 15:23:23 +0800 Subject: [PATCH 12/64] fix import --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index 1695fde35a3489..14581386653f40 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -3,8 +3,11 @@ Copyright (c) 2025 Nailin Guan. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Nailin Guan -/ -import Mathlib.RingTheory.Ideal.Cotangent -import Mathlib.RingTheory.Ideal.KrullsHeightTheorem +module + +public import Mathlib.RingTheory.Ideal.Cotangent +public import Mathlib.RingTheory.Ideal.KrullsHeightTheorem + /-! # Define Regular Local Ring @@ -24,6 +27,8 @@ the dimension of the cotangent space over the residue field being equal to `ring -/ +@[expose] public section + open IsLocalRing variable (R : Type*) [CommRing R] From e103dc9048be80edd763a1d81f4f287ab0a27fcb Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 5 Jan 2026 23:22:36 +0800 Subject: [PATCH 13/64] move lemma and golf --- Mathlib/RingTheory/Ideal/Cotangent.lean | 41 ++++++++++++++ Mathlib/RingTheory/RegularLocalRing/Defs.lean | 53 ++----------------- 2 files changed, 45 insertions(+), 49 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 86825e19d2929a..93e14850b9338b 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -6,6 +6,7 @@ Authors: Andrew Yang module public import Mathlib.Algebra.Module.Torsion.Basic +public import Mathlib.Algebra.Module.SpanRank public import Mathlib.Algebra.Ring.Idempotent public import Mathlib.LinearAlgebra.Dimension.Finite public import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition @@ -278,4 +279,44 @@ theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] : Submodule.map_top, range_subtype, eq_comm (a := maximalIdeal R)] exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩ +lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : + (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := by + have eqtop (S : Set (maximalIdeal R)) : Submodule.span R S = ⊤ ↔ + Submodule.span R ((Submodule.subtype (maximalIdeal R)) '' S) = maximalIdeal R := by + simp only [← Submodule.map_span, ← (maximalIdeal R).range_subtype , ← Submodule.map_top, + (Submodule.map_injective_of_injective (maximalIdeal R).injective_subtype).eq_iff] + have fg : Module.Finite (ResidueField R) (CotangentSpace R) := inferInstance + have fg' : Submodule.FG (maximalIdeal R) := Ideal.fg_of_isNoetherianRing (maximalIdeal R) + have : Submodule.spanFinrank (⊤ : Submodule (ResidueField R) (CotangentSpace R)) = + Module.rank (ResidueField R) (CotangentSpace R) := by + rw [← Submodule.fg_iff_spanRank_eq_spanFinrank.mpr fg.1, Submodule.rank_eq_spanRank_of_free] + simp only [← Module.finrank_eq_rank, Nat.cast_inj] at this + rw [← this] + apply le_antisymm + · have span : Submodule.span R + ((⊤ : Submodule (ResidueField R) (CotangentSpace R)).generators.image Quotient.out) = ⊤ := by + apply IsLocalRing.CotangentSpace.span_image_eq_top_iff.mp + convert Submodule.span_generators (⊤ : Submodule (ResidueField R) (CotangentSpace R)) + have : ⇑(maximalIdeal R).toCotangent ∘ Quotient.out = id := by + ext + exact Submodule.Quotient.mk_out _ + rw [← Set.image_comp, this, Set.image_id] + rw [eqtop, ← Set.image_comp] at span + rw [← Submodule.FG.generators_ncard fg.1, ← congrArg Submodule.spanFinrank span] + apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite + (Set.Finite.image _ fg.1.finite_generators)) (Set.ncard_image_le fg.1.finite_generators) + · let G := ({x | x.1 ∈ (maximalIdeal R).generators} : Set (maximalIdeal R)) + have : Submodule.span R G = ⊤ := by + simp only [eqtop, Submodule.subtype_apply, Ideal.submodule_span_eq, G] + convert (maximalIdeal R).span_generators + ext + simpa using fun a ↦ Submodule.FG.generators_mem (maximalIdeal R) a + have fin : G.Finite := + fg'.finite_generators.of_injOn (by simp [Set.MapsTo, G]) Set.injOn_subtype_val + rw [← IsLocalRing.CotangentSpace.span_image_eq_top_iff.mpr this, + ← Submodule.FG.generators_ncard fg'] + apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (fin.image _)) + exact le_trans (Set.ncard_image_le fin) (Set.ncard_le_ncard_of_injOn Subtype.val (by simp [G]) + Set.injOn_subtype_val fg'.finite_generators) + end IsLocalRing diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index 14581386653f40..1a155489d98c81 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -62,60 +62,15 @@ lemma of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R'] (e : R ≃+* R') : IsRegularLocalRing R' := by let _ := e.isLocalRing let _ := isNoetherianRing_of_ringEquiv R e - have fg : (maximalIdeal R).FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _ - apply of_span_eq R' (e '' (maximalIdeal R).generators) - ((Submodule.FG.finite_generators fg).image _) - · simp only [← Ideal.map_span] - rw [← Ideal.submodule_span_eq, Submodule.span_generators (maximalIdeal R), ← Ideal.comap_symm] + have fg : Submodule.FG (maximalIdeal R) := Ideal.fg_of_isNoetherianRing (maximalIdeal R) + apply of_span_eq R' (e '' (maximalIdeal R).generators) (fg.finite_generators.image _) + · rw [← Ideal.map_span, ← Ideal.submodule_span_eq, Submodule.span_generators , ← Ideal.comap_symm] exact ((local_hom_TFAE e.symm.toRingHom).out 0 4).mp (e.symm.surjective.isLocalHom _) · simpa [← ringKrullDim_eq_of_ringEquiv e, ← IsRegularLocalRing.reg, - ← Submodule.FG.generators_ncard fg] using - Set.ncard_image_le (Submodule.FG.finite_generators fg) + ← Submodule.FG.generators_ncard fg] using Set.ncard_image_le fg.finite_generators end IsRegularLocalRing -open Set in -lemma IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace - [IsLocalRing R] [IsNoetherianRing R] : - (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := by - have eqtop (S : Set (maximalIdeal R)) : Submodule.span R S = ⊤ ↔ - Submodule.span R ((Submodule.subtype (maximalIdeal R)) '' S) = maximalIdeal R := by - simp only [← Submodule.map_span, ← (maximalIdeal R).range_subtype , ← Submodule.map_top, - (Submodule.map_injective_of_injective (maximalIdeal R).injective_subtype).eq_iff] - let fg : Module.Finite (ResidueField R) (CotangentSpace R) := inferInstance - let fg' : (maximalIdeal R).FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _ - have : Submodule.spanFinrank (⊤ : Submodule (ResidueField R) (CotangentSpace R)) = - Module.rank (ResidueField R) (CotangentSpace R) := by - rw [← Submodule.fg_iff_spanRank_eq_spanFinrank.mpr fg.1, Submodule.rank_eq_spanRank_of_free] - simp only [← Module.finrank_eq_rank, Nat.cast_inj] at this - rw [← this] - apply le_antisymm - · have span : Submodule.span R - ((⊤ : Submodule (ResidueField R) (CotangentSpace R)).generators.image Quotient.out) = ⊤ := by - apply IsLocalRing.CotangentSpace.span_image_eq_top_iff.mp - convert Submodule.span_generators (⊤ : Submodule (ResidueField R) (CotangentSpace R)) - have : ⇑(maximalIdeal R).toCotangent ∘ Quotient.out = id := by - ext - exact Submodule.Quotient.mk_out _ - rw [← Set.image_comp, this, image_id] - rw [eqtop, ← Set.image_comp] at span - rw [← Submodule.FG.generators_ncard fg.1, ← congrArg Submodule.spanFinrank span] - apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite - (Finite.image _ fg.1.finite_generators)) (Set.ncard_image_le fg.1.finite_generators) - · let G := ({x | ↑x ∈ (maximalIdeal R).generators} : Set (maximalIdeal R)) - have : Submodule.span R G = ⊤ := by - simp only [eqtop, Submodule.subtype_apply, Ideal.submodule_span_eq, G] - convert (maximalIdeal R).span_generators - ext - simpa using fun a ↦ Submodule.FG.generators_mem (maximalIdeal R) a - have fin : G.Finite := Set.Finite.of_injOn (by simp [MapsTo, G]) injOn_subtype_val - (Submodule.FG.finite_generators fg') - rw [← IsLocalRing.CotangentSpace.span_image_eq_top_iff.mpr this, - ← Submodule.FG.generators_ncard fg'] - apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (Finite.image _ fin)) - exact le_trans (Set.ncard_image_le fin) (Set.ncard_le_ncard_of_injOn Subtype.val (by simp [G]) - injOn_subtype_val (Submodule.FG.finite_generators fg')) - lemma IsRegularLocalRing.iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by rw [isRegularLocalRing_def, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace] From d810ab719203da0282ec57ca35b94875944ce154 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Wed, 28 Jan 2026 10:52:39 +0800 Subject: [PATCH 14/64] golf --- Mathlib/RingTheory/Ideal/Cotangent.lean | 20 +++++++++++ Mathlib/RingTheory/RegularLocalRing/Defs.lean | 36 ++++++++----------- 2 files changed, 34 insertions(+), 22 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 93e14850b9338b..0f4d6624dfa1a7 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -319,4 +319,24 @@ lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : exact le_trans (Set.ncard_image_le fin) (Set.ncard_le_ncard_of_injOn Subtype.val (by simp [G]) Set.injOn_subtype_val fg'.finite_generators) +lemma spanFinrank_le_of_surjective {R : Type*} [CommRing R] [IsNoetherianRing R] + [IsLocalRing R] {R' : Type*} [CommRing R'] [IsNoetherianRing R'] [IsLocalRing R'] + (f : R →+* R') (surj : Function.Surjective f) : + (maximalIdeal R').spanFinrank ≤ (maximalIdeal R).spanFinrank := by + let fin := Submodule.FG.finite_generators (maximalIdeal R).fg_of_isNoetherianRing + have hspan : Ideal.span (f '' (maximalIdeal R).generators) = maximalIdeal R' := by + have : Ideal.span (maximalIdeal R).generators = _ := (maximalIdeal R).span_generators + simpa [← Ideal.map_span, this, ((local_hom_TFAE f).out 0 4).mp (surj.isLocalHom f)] using + (Ideal.map_comap_of_surjective f surj (maximalIdeal R')) + have hle : (maximalIdeal R').spanFinrank ≤ (f '' (maximalIdeal R).generators).ncard := by + simpa [← hspan] using (Submodule.spanFinrank_span_le_ncard_of_finite (fin.image _)) + apply le_trans hle (le_of_le_of_eq (Set.ncard_image_le fin) + (Submodule.FG.generators_ncard (maximalIdeal R).fg_of_isNoetherianRing)) + +lemma spanFinrank_eq_of_ringEquiv {R : Type*} [CommRing R] [IsNoetherianRing R] + [IsLocalRing R] {R' : Type*} [CommRing R'] [IsNoetherianRing R'] [IsLocalRing R'] + (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := + le_antisymm (spanFinrank_le_of_surjective e.symm.toRingHom e.symm.surjective) + (spanFinrank_le_of_surjective e.toRingHom e.surjective) + end IsLocalRing diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index 1a155489d98c81..953c85b77c8c7d 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -11,16 +11,16 @@ public import Mathlib.RingTheory.Ideal.KrullsHeightTheorem /-! # Define Regular Local Ring -For a noetherian local ring `R`, we define `IsRegularLocalRing` as +For a Noetherian local ring `R`, we define `IsRegularLocalRing` as `(maximalIdeal R).spanFinrank = ringKrullDim R`. This definition is equivalent to the dimension of the cotangent space over the residue field being equal to `ringKrullDim R`, (see `IsRegularLocalRing.iff_finrank_cotangentSpace`). # Main Definition and Results -* `IsRegularLocalRing` : A noetherian local ring of dimesnion `d` `IsRegularLocalRing` if +* `IsRegularLocalRing` : A Noetherian local ring is regular if `(maximalIdeal R).spanFinrank = ringKrullDim R`, - i.e. its maximal ideal can be generated by `d` elements. + i.e. its maximal ideal can be generated by `dim R` elements. * `IsRegularLocalRing.iff_finrank_cotangentSpace` : the equivalence of `IsRegularLocalRing` and `Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R` @@ -33,10 +33,10 @@ open IsLocalRing variable (R : Type*) [CommRing R] -/-- A noetherian local ring of dimesnion `d` is said to be regular if its maximal ideal -can be generated by `d` elements. -/ +/-- A Noetherian local ring is said to be regular if its maximal ideal +can be generated by `dim R` elements. -/ class IsRegularLocalRing : Prop extends IsLocalRing R, IsNoetherianRing R where - reg : (maximalIdeal R).spanFinrank = ringKrullDim R + spanFinrank_maximalIdeal : (maximalIdeal R).spanFinrank = ringKrullDim R lemma isRegularLocalRing_def [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ (maximalIdeal R).spanFinrank = ringKrullDim R := @@ -49,28 +49,20 @@ lemma ringKrullDim_le_spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing namespace IsRegularLocalRing -lemma of_span_eq [IsLocalRing R] [IsNoetherianRing R] (S : Set R) (fin : S.Finite) - (span : Ideal.span S = maximalIdeal R) (card : S.ncard ≤ ringKrullDim R) : - IsRegularLocalRing R := by - apply (isRegularLocalRing_def _).mpr (le_antisymm _ (ringKrullDim_le_spanFinrank_maximalIdeal R)) - apply le_trans _ card - rw [← span, ← Ideal.submodule_span_eq] - simpa using Submodule.spanFinrank_span_le_ncard_of_finite fin +lemma of_spanFinrank_maximalIdeal_le [IsLocalRing R] [IsNoetherianRing R] + (le : (maximalIdeal R).spanFinrank ≤ ringKrullDim R) : IsRegularLocalRing R := + (isRegularLocalRing_def _).mpr (le_antisymm le (ringKrullDim_le_spanFinrank_maximalIdeal R)) variable {R} in lemma of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R'] (e : R ≃+* R') : IsRegularLocalRing R' := by let _ := e.isLocalRing let _ := isNoetherianRing_of_ringEquiv R e - have fg : Submodule.FG (maximalIdeal R) := Ideal.fg_of_isNoetherianRing (maximalIdeal R) - apply of_span_eq R' (e '' (maximalIdeal R).generators) (fg.finite_generators.image _) - · rw [← Ideal.map_span, ← Ideal.submodule_span_eq, Submodule.span_generators , ← Ideal.comap_symm] - exact ((local_hom_TFAE e.symm.toRingHom).out 0 4).mp (e.symm.surjective.isLocalHom _) - · simpa [← ringKrullDim_eq_of_ringEquiv e, ← IsRegularLocalRing.reg, - ← Submodule.FG.generators_ncard fg] using Set.ncard_image_le fg.finite_generators + rw [isRegularLocalRing_def, ← spanFinrank_eq_of_ringEquiv e, ← ringKrullDim_eq_of_ringEquiv e] + exact (isRegularLocalRing_def R).mp ‹_› -end IsRegularLocalRing - -lemma IsRegularLocalRing.iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : +lemma iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by rw [isRegularLocalRing_def, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace] + +end IsRegularLocalRing From 7e3a308531b6a0f44fd2f73d98ba6db877503b82 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Wed, 28 Jan 2026 11:23:14 +0800 Subject: [PATCH 15/64] golf --- Mathlib/LinearAlgebra/Span/Basic.lean | 5 +++++ Mathlib/RingTheory/Ideal/Cotangent.lean | 12 ++++-------- Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean | 7 +++++++ Mathlib/RingTheory/RegularLocalRing/Defs.lean | 5 ----- 4 files changed, 16 insertions(+), 13 deletions(-) diff --git a/Mathlib/LinearAlgebra/Span/Basic.lean b/Mathlib/LinearAlgebra/Span/Basic.lean index 093d150a623512..ffce02d917efcb 100644 --- a/Mathlib/LinearAlgebra/Span/Basic.lean +++ b/Mathlib/LinearAlgebra/Span/Basic.lean @@ -873,3 +873,8 @@ theorem coord_apply_smul (y : Submodule.span R ({x} : Set M)) : coord R M x h y Subtype.ext_iff.1 <| (toSpanNonzeroSingleton R M x h).apply_symm_apply _ end LinearEquiv + +lemma Submodule.span_val_image_eq_iff {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] + (p : Submodule R M) (s : Set p) : + Submodule.span R (Subtype.val '' s) = p ↔ Submodule.span R s = ⊤ := by + simp [← (Submodule.map_injective_of_injective p.injective_subtype).eq_iff, Submodule.map_span] diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 0f4d6624dfa1a7..208c3effba417c 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -281,10 +281,6 @@ theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] : lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := by - have eqtop (S : Set (maximalIdeal R)) : Submodule.span R S = ⊤ ↔ - Submodule.span R ((Submodule.subtype (maximalIdeal R)) '' S) = maximalIdeal R := by - simp only [← Submodule.map_span, ← (maximalIdeal R).range_subtype , ← Submodule.map_top, - (Submodule.map_injective_of_injective (maximalIdeal R).injective_subtype).eq_iff] have fg : Module.Finite (ResidueField R) (CotangentSpace R) := inferInstance have fg' : Submodule.FG (maximalIdeal R) := Ideal.fg_of_isNoetherianRing (maximalIdeal R) have : Submodule.spanFinrank (⊤ : Submodule (ResidueField R) (CotangentSpace R)) = @@ -301,13 +297,13 @@ lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : ext exact Submodule.Quotient.mk_out _ rw [← Set.image_comp, this, Set.image_id] - rw [eqtop, ← Set.image_comp] at span + rw [← Submodule.span_val_image_eq_iff, ← Set.image_comp] at span rw [← Submodule.FG.generators_ncard fg.1, ← congrArg Submodule.spanFinrank span] apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite - (Set.Finite.image _ fg.1.finite_generators)) (Set.ncard_image_le fg.1.finite_generators) + (fg.1.finite_generators.image _)) (Set.ncard_image_le fg.1.finite_generators) · let G := ({x | x.1 ∈ (maximalIdeal R).generators} : Set (maximalIdeal R)) have : Submodule.span R G = ⊤ := by - simp only [eqtop, Submodule.subtype_apply, Ideal.submodule_span_eq, G] + simp only [← Submodule.span_val_image_eq_iff, Ideal.submodule_span_eq, G] convert (maximalIdeal R).span_generators ext simpa using fun a ↦ Submodule.FG.generators_mem (maximalIdeal R) a @@ -320,7 +316,7 @@ lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : Set.injOn_subtype_val fg'.finite_generators) lemma spanFinrank_le_of_surjective {R : Type*} [CommRing R] [IsNoetherianRing R] - [IsLocalRing R] {R' : Type*} [CommRing R'] [IsNoetherianRing R'] [IsLocalRing R'] + [IsLocalRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] (f : R →+* R') (surj : Function.Surjective f) : (maximalIdeal R').spanFinrank ≤ (maximalIdeal R).spanFinrank := by let fin := Submodule.FG.finite_generators (maximalIdeal R).fg_of_isNoetherianRing diff --git a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean index 20097bd91ceed5..5a5b35b9047b98 100644 --- a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean +++ b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean @@ -469,4 +469,11 @@ lemma Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown [IsNoetherianRing S simp [hlq, l', ← PrimeSpectrum.asIdeal_le_asIdeal, map_le_iff_le_comap, LiesOver.over (p := p) (P := P)] +variable (R) in +lemma ringKrullDim_le_spanFinrank_maximalIdeal [IsLocalRing R] : + ringKrullDim R ≤ (IsLocalRing.maximalIdeal R).spanFinrank := + le_of_eq_of_le IsLocalRing.maximalIdeal_height_eq_ringKrullDim.symm + (WithBot.coe_le_coe.mpr (Ideal.height_le_spanFinrank (IsLocalRing.maximalIdeal R) + Ideal.IsPrime.ne_top')) + end Algebra diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index 953c85b77c8c7d..cf34bf036fb8b1 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -42,11 +42,6 @@ lemma isRegularLocalRing_def [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ (maximalIdeal R).spanFinrank = ringKrullDim R := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩ -lemma ringKrullDim_le_spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] : - ringKrullDim R ≤ (maximalIdeal R).spanFinrank := - le_of_eq_of_le IsLocalRing.maximalIdeal_height_eq_ringKrullDim.symm - (WithBot.coe_le_coe.mpr (Ideal.height_le_spanFinrank (maximalIdeal R) Ideal.IsPrime.ne_top')) - namespace IsRegularLocalRing lemma of_spanFinrank_maximalIdeal_le [IsLocalRing R] [IsNoetherianRing R] From 4f32eaa92099bac49554db122c1310de64b16082 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sun, 15 Feb 2026 17:38:21 +0800 Subject: [PATCH 16/64] add some lemma about spanRank --- Mathlib/Algebra/Module/SpanRank.lean | 8 +++ Mathlib/LinearAlgebra/Span/Basic.lean | 5 ++ Mathlib/RingTheory/Ideal/Cotangent.lean | 89 +++++++++++++++++++++++++ 3 files changed, 102 insertions(+) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 9d5cd489a46103..0a841fa888efe6 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -363,6 +363,14 @@ theorem Submodule.rank_eq_spanRank_of_free [Module.Free R M] [StrongRankConditio rw [← Basis.mk_eq_rank'' B, ← Basis.mk_eq_spanRank B, ← Cardinal.lift_id #(Set.range B), Cardinal.mk_range_eq_of_injective B.injective, Cardinal.lift_id _] +lemma Module.finrank_eq_spanFinrank_of_free [StrongRankCondition R] + (M : Type*) [AddCommGroup M] [Module R M] [fin : Module.Finite R M] [Module.Free R M] : + Module.finrank R M = (⊤ : Submodule R M).spanFinrank := by + have : Submodule.spanFinrank (⊤ : Submodule R M) = Module.rank R M := by + rw [← Submodule.fg_iff_spanRank_eq_spanFinrank.mpr fin.1, + Submodule.rank_eq_spanRank_of_free] + simpa only [← Module.finrank_eq_rank, Nat.cast_inj] using this.symm + theorem Submodule.rank_le_spanRank [StrongRankCondition R] : Module.rank R M ≤ (⊤ : Submodule R M).spanRank := by rw [Module.rank, Submodule.spanRank] diff --git a/Mathlib/LinearAlgebra/Span/Basic.lean b/Mathlib/LinearAlgebra/Span/Basic.lean index 093d150a623512..ffce02d917efcb 100644 --- a/Mathlib/LinearAlgebra/Span/Basic.lean +++ b/Mathlib/LinearAlgebra/Span/Basic.lean @@ -873,3 +873,8 @@ theorem coord_apply_smul (y : Submodule.span R ({x} : Set M)) : coord R M x h y Subtype.ext_iff.1 <| (toSpanNonzeroSingleton R M x h).apply_symm_apply _ end LinearEquiv + +lemma Submodule.span_val_image_eq_iff {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] + (p : Submodule R M) (s : Set p) : + Submodule.span R (Subtype.val '' s) = p ↔ Submodule.span R s = ⊤ := by + simp [← (Submodule.map_injective_of_injective p.injective_subtype).eq_iff, Submodule.map_span] diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 86825e19d2929a..32b6bfae2fc8f0 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -6,6 +6,7 @@ Authors: Andrew Yang module public import Mathlib.Algebra.Module.Torsion.Basic +public import Mathlib.Algebra.Module.SpanRank public import Mathlib.Algebra.Ring.Idempotent public import Mathlib.LinearAlgebra.Dimension.Finite public import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition @@ -279,3 +280,91 @@ theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] : exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩ end IsLocalRing + +section spanRank + +open IsLocalRing + +variable (R : Type*) [CommRing R] + +instance (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) : + Module.Finite (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)) := + Module.Finite.of_restrictScalars_finite R _ _ + +variable {R} in +lemma spanFinrank_eq_finrank_quotient [IsLocalRing R] {M : Type*} [AddCommGroup M] [Module R M] + (N : Submodule R M) (fg : N.FG) : N.spanFinrank = + Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by + let _ : Field (R ⧸ maximalIdeal R) := Ideal.Quotient.field (maximalIdeal R) + let _ : Module.Finite R N := Module.Finite.iff_fg.mpr fg + rw [Module.finrank_eq_spanFinrank_of_free] + let k := R ⧸ maximalIdeal R + let Q := N ⧸ (maximalIdeal R) • (⊤ : Submodule R N) + apply le_antisymm + · let s : Set Q := (⊤ : Submodule k Q).generators + have hfgQ : (⊤ : Submodule k Q).FG := Module.Finite.fg_top + have hs_span_R : Submodule.span R s = (⊤ : Submodule R Q) := by + rw [← Submodule.coe_eq_univ, ← Submodule.coe_span_eq_span_of_surjective R k + Ideal.Quotient.mk_surjective, Submodule.coe_eq_univ, Submodule.span_generators _] + have hNfg : (⊤ : Submodule R N).FG := (Submodule.fg_top _).mpr fg + obtain ⟨t, ht_inj, ht_image, ht_span⟩ := + Submodule.exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot + s hNfg (IsLocalRing.maximalIdeal_le_jacobson _) (by simpa using hs_span_R) + have htfinite : t.Finite := by + simpa only [← Set.finite_image_iff ht_inj, ht_image] using hfgQ.finite_generators + have hle : N.spanFinrank ≤ (Subtype.val '' t).ncard := by + simpa [(Submodule.span_val_image_eq_iff N t).mpr ht_span] using + (Submodule.spanFinrank_span_le_ncard_of_finite (R := R) (htfinite.image Subtype.val)) + have hcard : t.ncard = s.ncard := by + simpa only [← ht_image] using (Set.InjOn.ncard_image ht_inj).symm + exact le_of_le_of_eq hle ((Set.ncard_image_of_injective _ (Subtype.val_injective)).trans + (hcard.trans hfgQ.generators_ncard)) + · let G : Set N := {x | (x : M) ∈ N.generators} + have hGval : (Subtype.val '' G) = (N.generators : Set M) := by + simpa [G, Set.image] using Submodule.FG.generators_mem (p := N) + have hspanG : Submodule.span R G = (⊤ : Submodule R N) := by + simp [← Submodule.span_val_image_eq_iff, hGval, Submodule.span_generators ] + have hspanK : Submodule.span k (((maximalIdeal R) • (⊤ : Submodule R N)).mkQ '' G) = ⊤ := by + rw [← Submodule.coe_eq_univ, Submodule.coe_span_eq_span_of_surjective R k + Ideal.Quotient.mk_surjective, Submodule.coe_eq_univ] + simp only [← Submodule.map_span, hspanG, Submodule.map_top, Submodule.range_mkQ] + have hGfinite : G.Finite := by + simpa [hGval] using fg.finite_generators.preimage (Subtype.val_injective.injOn) + have hG_ncard : G.ncard = N.spanFinrank := by + rw [← fg.generators_ncard, ← hGval] + simpa using (Set.ncard_image_of_injective G Subtype.val_injective).symm + rw [← hspanK] + exact (Submodule.spanFinrank_span_le_ncard_of_finite (hGfinite.image _)).trans + (le_of_le_of_eq (Set.ncard_image_le hGfinite) hG_ncard) + +variable {R} in +lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg [IsLocalRing R] + (fg : (maximalIdeal R).FG) : + (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := + spanFinrank_eq_finrank_quotient _ fg + +lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : + (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := + spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (maximalIdeal R).fg_of_isNoetherianRing + +lemma spanFinrank_le_of_surjective {R : Type*} [CommRing R] [IsNoetherianRing R] + [IsLocalRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] + (f : R →+* R') (surj : Function.Surjective f) : + (maximalIdeal R').spanFinrank ≤ (maximalIdeal R).spanFinrank := by + let fin := Submodule.FG.finite_generators (maximalIdeal R).fg_of_isNoetherianRing + have hspan : Ideal.span (f '' (maximalIdeal R).generators) = maximalIdeal R' := by + have : Ideal.span (maximalIdeal R).generators = _ := (maximalIdeal R).span_generators + simpa [← Ideal.map_span, this, ((local_hom_TFAE f).out 0 4).mp (surj.isLocalHom f)] using + (Ideal.map_comap_of_surjective f surj (maximalIdeal R')) + have hle : (maximalIdeal R').spanFinrank ≤ (f '' (maximalIdeal R).generators).ncard := by + simpa [← hspan] using (Submodule.spanFinrank_span_le_ncard_of_finite (fin.image _)) + apply le_trans hle (le_of_le_of_eq (Set.ncard_image_le fin) + (Submodule.FG.generators_ncard (maximalIdeal R).fg_of_isNoetherianRing)) + +lemma spanFinrank_eq_of_ringEquiv {R : Type*} [CommRing R] [IsNoetherianRing R] + [IsLocalRing R] {R' : Type*} [CommRing R'] [IsNoetherianRing R'] [IsLocalRing R'] + (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := + le_antisymm (spanFinrank_le_of_surjective e.symm.toRingHom e.symm.surjective) + (spanFinrank_le_of_surjective e.toRingHom e.surjective) + +end spanRank From 6cf21b0e8f588fdb30ca147d8fd60fa02a2e9559 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 16 Feb 2026 11:04:55 +0800 Subject: [PATCH 17/64] Update SpanRank.lean --- Mathlib/Algebra/Module/SpanRank.lean | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 0a841fa888efe6..7b17437f256a5d 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -6,6 +6,7 @@ Authors: Wanyi He, Jiedong Jiang, Xuchun Li, Christian Merten, Jingting Wang, An module public import Mathlib.Data.ENat.Lattice +public import Mathlib.LinearAlgebra.Dimension.Free public import Mathlib.LinearAlgebra.Dimension.StrongRankCondition public import Mathlib.RingTheory.Finiteness.Ideal @@ -128,6 +129,9 @@ lemma fg_iff_spanRank_eq_spanFinrank {p : Submodule R M} : p.spanRank = p.spanFi rw [spanFinrank, ← spanRank_finite_iff_fg, eq_comm] exact cast_toNat_eq_iff_lt_aleph0 +lemma FG.spanRank_eq_spanFinrank {p : Submodule R M} (fg : p.FG) : p.spanRank = p.spanFinrank := + fg_iff_spanRank_eq_spanFinrank.mpr fg + lemma spanRank_span_le_card (s : Set M) : (Submodule.span R s).spanRank ≤ #s := by rw [spanRank] let s' : {s1 : Set M // span R s1 = span R s} := ⟨s, rfl⟩ @@ -364,12 +368,15 @@ theorem Submodule.rank_eq_spanRank_of_free [Module.Free R M] [StrongRankConditio Cardinal.mk_range_eq_of_injective B.injective, Cardinal.lift_id _] lemma Module.finrank_eq_spanFinrank_of_free [StrongRankCondition R] - (M : Type*) [AddCommGroup M] [Module R M] [fin : Module.Finite R M] [Module.Free R M] : + (M : Type*) [AddCommGroup M] [Module R M] [Module.Free R M] : Module.finrank R M = (⊤ : Submodule R M).spanFinrank := by - have : Submodule.spanFinrank (⊤ : Submodule R M) = Module.rank R M := by - rw [← Submodule.fg_iff_spanRank_eq_spanFinrank.mpr fin.1, - Submodule.rank_eq_spanRank_of_free] - simpa only [← Module.finrank_eq_rank, Nat.cast_inj] using this.symm + by_cases fin : Module.Finite R M + · have : Submodule.spanFinrank (⊤ : Submodule R M) = Module.rank R M := by + rw [← Submodule.fg_iff_spanRank_eq_spanFinrank.mpr fin.1, + Submodule.rank_eq_spanRank_of_free] + simpa only [← Module.finrank_eq_rank, Nat.cast_inj] using this.symm + · have fin' : ¬ (⊤ : Submodule R M).FG := Not.intro (fun h ↦ fin ⟨h⟩) + rw [Module.finrank_of_not_finite fin, Submodule.spanFinrank_of_not_fg fin'] theorem Submodule.rank_le_spanRank [StrongRankCondition R] : Module.rank R M ≤ (⊤ : Submodule R M).spanRank := by From ca8bab077f7d85628d580417f0a67c71f7acfccc Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 16 Feb 2026 11:10:16 +0800 Subject: [PATCH 18/64] move instance --- Mathlib/Algebra/Module/Torsion/Basic.lean | 4 ++++ Mathlib/RingTheory/Ideal/Cotangent.lean | 4 ---- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Module/Torsion/Basic.lean b/Mathlib/Algebra/Module/Torsion/Basic.lean index bbd906317dd94b..63bd8e3d7bf860 100644 --- a/Mathlib/Algebra/Module/Torsion/Basic.lean +++ b/Mathlib/Algebra/Module/Torsion/Basic.lean @@ -670,6 +670,10 @@ def submodule_torsionBy_orderIso (a : R) : left_inv := by intro; ext; simp [restrictScalarsEmbedding] right_inv := by intro; ext; simp [restrictScalarsEmbedding] } +instance (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) : + Module.Finite (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)) := + Module.Finite.of_restrictScalars_finite R _ _ + end Submodule end NeedsGroup diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 32b6bfae2fc8f0..9292bb3706d7e2 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -287,10 +287,6 @@ open IsLocalRing variable (R : Type*) [CommRing R] -instance (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) : - Module.Finite (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)) := - Module.Finite.of_restrictScalars_finite R _ _ - variable {R} in lemma spanFinrank_eq_finrank_quotient [IsLocalRing R] {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M) (fg : N.FG) : N.spanFinrank = From 4547600b0968bff50b4174d946608841a367a846 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 16 Feb 2026 11:12:27 +0800 Subject: [PATCH 19/64] golf variable --- Mathlib/RingTheory/Ideal/Cotangent.lean | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 9292bb3706d7e2..5147c4113d2274 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -285,9 +285,8 @@ section spanRank open IsLocalRing -variable (R : Type*) [CommRing R] +variable {R : Type*} [CommRing R] -variable {R} in lemma spanFinrank_eq_finrank_quotient [IsLocalRing R] {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M) (fg : N.FG) : N.spanFinrank = Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by @@ -333,19 +332,18 @@ lemma spanFinrank_eq_finrank_quotient [IsLocalRing R] {M : Type*} [AddCommGroup exact (Submodule.spanFinrank_span_le_ncard_of_finite (hGfinite.image _)).trans (le_of_le_of_eq (Set.ncard_image_le hGfinite) hG_ncard) -variable {R} in lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg [IsLocalRing R] (fg : (maximalIdeal R).FG) : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := spanFinrank_eq_finrank_quotient _ fg +variable (R) in lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (maximalIdeal R).fg_of_isNoetherianRing -lemma spanFinrank_le_of_surjective {R : Type*} [CommRing R] [IsNoetherianRing R] - [IsLocalRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] - (f : R →+* R') (surj : Function.Surjective f) : +lemma spanFinrank_le_of_surjective [IsNoetherianRing R] [IsLocalRing R] {R' : Type*} [CommRing R'] + [IsLocalRing R'] (f : R →+* R') (surj : Function.Surjective f) : (maximalIdeal R').spanFinrank ≤ (maximalIdeal R).spanFinrank := by let fin := Submodule.FG.finite_generators (maximalIdeal R).fg_of_isNoetherianRing have hspan : Ideal.span (f '' (maximalIdeal R).generators) = maximalIdeal R' := by @@ -357,9 +355,9 @@ lemma spanFinrank_le_of_surjective {R : Type*} [CommRing R] [IsNoetherianRing R] apply le_trans hle (le_of_le_of_eq (Set.ncard_image_le fin) (Submodule.FG.generators_ncard (maximalIdeal R).fg_of_isNoetherianRing)) -lemma spanFinrank_eq_of_ringEquiv {R : Type*} [CommRing R] [IsNoetherianRing R] - [IsLocalRing R] {R' : Type*} [CommRing R'] [IsNoetherianRing R'] [IsLocalRing R'] - (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := +lemma spanFinrank_eq_of_ringEquiv [IsNoetherianRing R] [IsLocalRing R] {R' : Type*} [CommRing R'] + [IsNoetherianRing R'] [IsLocalRing R'] (e : R ≃+* R') : + (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := le_antisymm (spanFinrank_le_of_surjective e.symm.toRingHom e.symm.surjective) (spanFinrank_le_of_surjective e.toRingHom e.surjective) From 60ce0cdab0a81b3e6d4e86d31db5ceadec7e260b Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 16 Feb 2026 11:32:36 +0800 Subject: [PATCH 20/64] remove duplicated --- Mathlib/RingTheory/Ideal/Cotangent.lean | 56 ------------------------- 1 file changed, 56 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 886b3b2f9e444c..5147c4113d2274 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -279,62 +279,6 @@ theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] : Submodule.map_top, range_subtype, eq_comm (a := maximalIdeal R)] exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩ -lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : - (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := by - have fg : Module.Finite (ResidueField R) (CotangentSpace R) := inferInstance - have fg' : Submodule.FG (maximalIdeal R) := Ideal.fg_of_isNoetherianRing (maximalIdeal R) - have : Submodule.spanFinrank (⊤ : Submodule (ResidueField R) (CotangentSpace R)) = - Module.rank (ResidueField R) (CotangentSpace R) := by - rw [← Submodule.fg_iff_spanRank_eq_spanFinrank.mpr fg.1, Submodule.rank_eq_spanRank_of_free] - simp only [← Module.finrank_eq_rank, Nat.cast_inj] at this - rw [← this] - apply le_antisymm - · have span : Submodule.span R - ((⊤ : Submodule (ResidueField R) (CotangentSpace R)).generators.image Quotient.out) = ⊤ := by - apply IsLocalRing.CotangentSpace.span_image_eq_top_iff.mp - convert Submodule.span_generators (⊤ : Submodule (ResidueField R) (CotangentSpace R)) - have : ⇑(maximalIdeal R).toCotangent ∘ Quotient.out = id := by - ext - exact Submodule.Quotient.mk_out _ - rw [← Set.image_comp, this, Set.image_id] - rw [← Submodule.span_val_image_eq_iff, ← Set.image_comp] at span - rw [← Submodule.FG.generators_ncard fg.1, ← congrArg Submodule.spanFinrank span] - apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite - (fg.1.finite_generators.image _)) (Set.ncard_image_le fg.1.finite_generators) - · let G := ({x | x.1 ∈ (maximalIdeal R).generators} : Set (maximalIdeal R)) - have : Submodule.span R G = ⊤ := by - simp only [← Submodule.span_val_image_eq_iff, Ideal.submodule_span_eq, G] - convert (maximalIdeal R).span_generators - ext - simpa using fun a ↦ Submodule.FG.generators_mem (maximalIdeal R) a - have fin : G.Finite := - fg'.finite_generators.of_injOn (by simp [Set.MapsTo, G]) Set.injOn_subtype_val - rw [← IsLocalRing.CotangentSpace.span_image_eq_top_iff.mpr this, - ← Submodule.FG.generators_ncard fg'] - apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (fin.image _)) - exact le_trans (Set.ncard_image_le fin) (Set.ncard_le_ncard_of_injOn Subtype.val (by simp [G]) - Set.injOn_subtype_val fg'.finite_generators) - -lemma spanFinrank_le_of_surjective {R : Type*} [CommRing R] [IsNoetherianRing R] - [IsLocalRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] - (f : R →+* R') (surj : Function.Surjective f) : - (maximalIdeal R').spanFinrank ≤ (maximalIdeal R).spanFinrank := by - let fin := Submodule.FG.finite_generators (maximalIdeal R).fg_of_isNoetherianRing - have hspan : Ideal.span (f '' (maximalIdeal R).generators) = maximalIdeal R' := by - have : Ideal.span (maximalIdeal R).generators = _ := (maximalIdeal R).span_generators - simpa [← Ideal.map_span, this, ((local_hom_TFAE f).out 0 4).mp (surj.isLocalHom f)] using - (Ideal.map_comap_of_surjective f surj (maximalIdeal R')) - have hle : (maximalIdeal R').spanFinrank ≤ (f '' (maximalIdeal R).generators).ncard := by - simpa [← hspan] using (Submodule.spanFinrank_span_le_ncard_of_finite (fin.image _)) - apply le_trans hle (le_of_le_of_eq (Set.ncard_image_le fin) - (Submodule.FG.generators_ncard (maximalIdeal R).fg_of_isNoetherianRing)) - -lemma spanFinrank_eq_of_ringEquiv {R : Type*} [CommRing R] [IsNoetherianRing R] - [IsLocalRing R] {R' : Type*} [CommRing R'] [IsNoetherianRing R'] [IsLocalRing R'] - (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := - le_antisymm (spanFinrank_le_of_surjective e.symm.toRingHom e.symm.surjective) - (spanFinrank_le_of_surjective e.toRingHom e.surjective) - end IsLocalRing section spanRank From 7f4146c022f549becacf5eaa00b59ae90a82a6cc Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Wed, 18 Feb 2026 23:04:02 +0800 Subject: [PATCH 21/64] fix --- Mathlib/RingTheory/Ideal/Cotangent.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 4e53ab4ebd7109..0c13ec4ba20c39 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -300,6 +300,7 @@ open IsLocalRing variable {R : Type*} [CommRing R] +set_option backward.isDefEq.respectTransparency false in lemma spanFinrank_eq_finrank_quotient [IsLocalRing R] {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M) (fg : N.FG) : N.spanFinrank = Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by From 3b50eb907170317d0033588dd2e174e9b74547f6 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 19 Feb 2026 17:24:28 +0800 Subject: [PATCH 22/64] add instance from field --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index cf34bf036fb8b1..b111b7863a0f10 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -7,6 +7,7 @@ module public import Mathlib.RingTheory.Ideal.Cotangent public import Mathlib.RingTheory.Ideal.KrullsHeightTheorem +public import Mathlib.RingTheory.KrullDimension.Field /-! # Define Regular Local Ring @@ -60,4 +61,7 @@ lemma iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by rw [isRegularLocalRing_def, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace] +instance {k : Type*} [Field k] : IsRegularLocalRing k := by + simp [isRegularLocalRing_def, maximalIdeal_eq_bot] + end IsRegularLocalRing From 8311afc14ccd27488a8f9c71b4c902c09fea3e79 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 19 Feb 2026 17:33:15 +0800 Subject: [PATCH 23/64] add instance from DVR --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index b111b7863a0f10..05eecd688bd4a7 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -5,9 +5,11 @@ Authors: Nailin Guan -/ module +public import Mathlib.RingTheory.DiscreteValuationRing.Basic public import Mathlib.RingTheory.Ideal.Cotangent public import Mathlib.RingTheory.Ideal.KrullsHeightTheorem public import Mathlib.RingTheory.KrullDimension.Field +public import Mathlib.RingTheory.KrullDimension.PID /-! # Define Regular Local Ring @@ -64,4 +66,11 @@ lemma iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : instance {k : Type*} [Field k] : IsRegularLocalRing k := by simp [isRegularLocalRing_def, maximalIdeal_eq_bot] +instance [IsDomain R] [IsDiscreteValuationRing R] : IsRegularLocalRing R := by + apply of_spanFinrank_maximalIdeal_le + rcases IsPrincipalIdealRing.principal (maximalIdeal R) with ⟨x, hx⟩ + simpa only [(IsPrincipalIdealRing.ringKrullDim_eq_one R) (IsDiscreteValuationRing.not_isField R), + Nat.cast_le_one, ← Set.ncard_singleton x, hx] using + Submodule.spanFinrank_span_le_ncard_of_finite (Set.finite_singleton x) + end IsRegularLocalRing From acd41411179bd3657d3b733481fe716f60ec3741 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 20 Feb 2026 16:02:09 +0800 Subject: [PATCH 24/64] golf --- Mathlib/RingTheory/Ideal/Cotangent.lean | 26 ++++++++----------------- 1 file changed, 8 insertions(+), 18 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 0c13ec4ba20c39..30eaa26deee3f7 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -305,7 +305,7 @@ lemma spanFinrank_eq_finrank_quotient [IsLocalRing R] {M : Type*} [AddCommGroup (N : Submodule R M) (fg : N.FG) : N.spanFinrank = Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by let _ : Field (R ⧸ maximalIdeal R) := Ideal.Quotient.field (maximalIdeal R) - let _ : Module.Finite R N := Module.Finite.iff_fg.mpr fg + let fin : Module.Finite R N := Module.Finite.iff_fg.mpr fg rw [Module.finrank_eq_spanFinrank_of_free] let k := R ⧸ maximalIdeal R let Q := N ⧸ (maximalIdeal R) • (⊤ : Submodule R N) @@ -328,23 +328,13 @@ lemma spanFinrank_eq_finrank_quotient [IsLocalRing R] {M : Type*} [AddCommGroup simpa only [← ht_image] using (Set.InjOn.ncard_image ht_inj).symm exact le_of_le_of_eq hle ((Set.ncard_image_of_injective _ (Subtype.val_injective)).trans (hcard.trans hfgQ.generators_ncard)) - · let G : Set N := {x | (x : M) ∈ N.generators} - have hGval : (Subtype.val '' G) = (N.generators : Set M) := by - simpa [G, Set.image] using Submodule.FG.generators_mem (p := N) - have hspanG : Submodule.span R G = (⊤ : Submodule R N) := by - simp [← Submodule.span_val_image_eq_iff, hGval, Submodule.span_generators ] - have hspanK : Submodule.span k (((maximalIdeal R) • (⊤ : Submodule R N)).mkQ '' G) = ⊤ := by - rw [← Submodule.coe_eq_univ, Submodule.coe_span_eq_span_of_surjective R k - Ideal.Quotient.mk_surjective, Submodule.coe_eq_univ] - simp only [← Submodule.map_span, hspanG, Submodule.map_top, Submodule.range_mkQ] - have hGfinite : G.Finite := by - simpa [hGval] using fg.finite_generators.preimage (Subtype.val_injective.injOn) - have hG_ncard : G.ncard = N.spanFinrank := by - rw [← fg.generators_ncard, ← hGval] - simpa using (Set.ncard_image_of_injective G Subtype.val_injective).symm - rw [← hspanK] - exact (Submodule.spanFinrank_span_le_ncard_of_finite (hGfinite.image _)).trans - (le_of_le_of_eq (Set.ncard_image_le hGfinite) hG_ncard) + · have : (⊤ : Submodule R N).spanFinrank = N.spanFinrank := by simp [Submodule.spanFinrank] + rw [← this] + let f : N →ₛₗ[Ideal.Quotient.mk (maximalIdeal R)] + (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := { __ := Submodule.mkQ _ } + convert Submodule.spanFinrank_map_le_of_fg f fin.1 + symm + simpa [f, LinearMap.range_eq_top] using Submodule.mkQ_surjective _ lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg [IsLocalRing R] (fg : (maximalIdeal R).FG) : From 63478037b1835df94c031e870619d5a57cd48c7d Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 20 Feb 2026 16:15:09 +0800 Subject: [PATCH 25/64] golf and fix namespace --- Mathlib/RingTheory/Ideal/Cotangent.lean | 32 ++++++++++--------------- 1 file changed, 13 insertions(+), 19 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 30eaa26deee3f7..ed232753ea503d 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -292,16 +292,12 @@ theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] : Submodule.map_top, range_subtype, eq_comm (a := maximalIdeal R)] exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩ -end IsLocalRing - section spanRank open IsLocalRing -variable {R : Type*} [CommRing R] - set_option backward.isDefEq.respectTransparency false in -lemma spanFinrank_eq_finrank_quotient [IsLocalRing R] {M : Type*} [AddCommGroup M] [Module R M] +lemma spanFinrank_eq_finrank_quotient {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M) (fg : N.FG) : N.spanFinrank = Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by let _ : Field (R ⧸ maximalIdeal R) := Ideal.Quotient.field (maximalIdeal R) @@ -315,39 +311,35 @@ lemma spanFinrank_eq_finrank_quotient [IsLocalRing R] {M : Type*} [AddCommGroup have hs_span_R : Submodule.span R s = (⊤ : Submodule R Q) := by rw [← Submodule.coe_eq_univ, ← Submodule.coe_span_eq_span_of_surjective R k Ideal.Quotient.mk_surjective, Submodule.coe_eq_univ, Submodule.span_generators _] - have hNfg : (⊤ : Submodule R N).FG := (Submodule.fg_top _).mpr fg obtain ⟨t, ht_inj, ht_image, ht_span⟩ := Submodule.exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot - s hNfg (IsLocalRing.maximalIdeal_le_jacobson _) (by simpa using hs_span_R) + s fin.1 (IsLocalRing.maximalIdeal_le_jacobson _) (by simpa using hs_span_R) have htfinite : t.Finite := by simpa only [← Set.finite_image_iff ht_inj, ht_image] using hfgQ.finite_generators have hle : N.spanFinrank ≤ (Subtype.val '' t).ncard := by simpa [(Submodule.span_val_image_eq_iff N t).mpr ht_span] using (Submodule.spanFinrank_span_le_ncard_of_finite (R := R) (htfinite.image Subtype.val)) - have hcard : t.ncard = s.ncard := by - simpa only [← ht_image] using (Set.InjOn.ncard_image ht_inj).symm + have hcard : t.ncard = s.ncard := by simpa only [← ht_image] using ht_inj.ncard_image.symm exact le_of_le_of_eq hle ((Set.ncard_image_of_injective _ (Subtype.val_injective)).trans (hcard.trans hfgQ.generators_ncard)) · have : (⊤ : Submodule R N).spanFinrank = N.spanFinrank := by simp [Submodule.spanFinrank] rw [← this] - let f : N →ₛₗ[Ideal.Quotient.mk (maximalIdeal R)] - (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := { __ := Submodule.mkQ _ } + let f : N →ₛₗ[Ideal.Quotient.mk (maximalIdeal R)] Q := { __ := Submodule.mkQ _ } convert Submodule.spanFinrank_map_le_of_fg f fin.1 symm simpa [f, LinearMap.range_eq_top] using Submodule.mkQ_surjective _ -lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg [IsLocalRing R] - (fg : (maximalIdeal R).FG) : +lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (fg : (maximalIdeal R).FG) : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := spanFinrank_eq_finrank_quotient _ fg variable (R) in -lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : +lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (maximalIdeal R).fg_of_isNoetherianRing -lemma spanFinrank_le_of_surjective [IsNoetherianRing R] [IsLocalRing R] {R' : Type*} [CommRing R'] - [IsLocalRing R'] (f : R →+* R') (surj : Function.Surjective f) : +lemma spanFinrank_le_of_surjective [IsNoetherianRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] + (f : R →+* R') (surj : Function.Surjective f) : (maximalIdeal R').spanFinrank ≤ (maximalIdeal R).spanFinrank := by let fin := Submodule.FG.finite_generators (maximalIdeal R).fg_of_isNoetherianRing have hspan : Ideal.span (f '' (maximalIdeal R).generators) = maximalIdeal R' := by @@ -359,10 +351,12 @@ lemma spanFinrank_le_of_surjective [IsNoetherianRing R] [IsLocalRing R] {R' : Ty apply le_trans hle (le_of_le_of_eq (Set.ncard_image_le fin) (Submodule.FG.generators_ncard (maximalIdeal R).fg_of_isNoetherianRing)) -lemma spanFinrank_eq_of_ringEquiv [IsNoetherianRing R] [IsLocalRing R] {R' : Type*} [CommRing R'] - [IsNoetherianRing R'] [IsLocalRing R'] (e : R ≃+* R') : - (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := +lemma spanFinrank_eq_of_ringEquiv [IsNoetherianRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] + (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := + let _ := isNoetherianRing_of_ringEquiv R e le_antisymm (spanFinrank_le_of_surjective e.symm.toRingHom e.symm.surjective) (spanFinrank_le_of_surjective e.toRingHom e.surjective) end spanRank + +end IsLocalRing From 0c8ddc5a6959434fa1318f6960050b9b8b62b3fa Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 27 Feb 2026 23:13:01 +0800 Subject: [PATCH 26/64] add span fin rank version lemma --- Mathlib/Algebra/Module/SpanRank.lean | 31 +++++++++++++++++++++------- 1 file changed, 24 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 7b17437f256a5d..1cddbd371452e6 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -274,10 +274,11 @@ lemma spanRank_map_le [RingHomSurjective σ] (f : M →ₛₗ[σ] N) exact ⟨f '' p.generators, Cardinal.mk_image_le, le_antisymm (span_le.2 (fun n ⟨m, hm, h⟩ ↦ ⟨m, span_generators p ▸ subset_span hm, h⟩)) (by simp [span_generators])⟩ -lemma spanFinrank_map_le_of_fg [RingHomSurjective σ] (f : M →ₛₗ[σ] N) - {p : Submodule R M} (hp : p.FG) : (p.map f).spanFinrank ≤ p.spanFinrank := - (Cardinal.toNat_le_iff_le_of_lt_aleph0 (spanRank_finite_iff_fg.mpr (FG.map f hp)) - (spanRank_finite_iff_fg.mpr hp)).2 (p.spanRank_map_le f) +lemma spanFinrank_map_le_of_fg {L : Type*} [AddCommMonoid L] [Module S L] [RingHomSurjective σ] + (f : M →ₛₗ[σ] L) {p : Submodule R M} (hp : p.FG) : (p.map f).spanFinrank ≤ p.spanFinrank := by + nth_rw 1 [← p.span_generators, Submodule.map_span, ← hp.generators_ncard] + exact (Submodule.spanFinrank_span_le_ncard_of_finite (hp.finite_generators.image f)).trans + (Set.ncard_image_le hp.finite_generators) lemma spanRank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] N) (hf : Function.Injective f) (p : Submodule R M) : (p.map f).spanRank = p.spanRank := by @@ -288,6 +289,19 @@ lemma spanRank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] N obtain rfl : span R s = p := by simpa [(map_injective_of_injective hf).eq_iff] using e grw [← hs, spanRank_span_le_card, Cardinal.mk_image_eq hf] +lemma spanFinrank_map_eq_of_injective {L : Type*} [AddCommMonoid L] [Module S L] [RingHomSurjective σ] + (f : M →ₛₗ[σ] L) (hf : Function.Injective f) {p : Submodule R M} (hp : p.FG) : + (p.map f).spanFinrank = p.spanFinrank := by + refine (spanFinrank_map_le_of_fg f hp).antisymm ?_ + obtain ⟨s, hs⟩ : ∃ y, f '' y = (p.map f).generators := Set.subset_range_iff_exists_image_eq.mp + ((subset_span.trans (p.map f).span_generators.le).trans LinearMap.map_le_range) + have fin : s.Finite := + Set.Finite.of_finite_image (by simpa [hs] using (hp.map f).finite_generators) hf.injOn + have : span R s = p := map_injective_of_injective hf + (by rw [Submodule.map_span, hs, (p.map f).span_generators]) + nth_grw 1 [← this, Submodule.spanFinrank_span_le_ncard_of_finite fin, + ← (hp.map f).generators_ncard, ← hf.injOn.ncard_image, hs] + lemma spanRank_range_le [RingHomSurjective σ] (f : M →ₛₗ[σ] N) : (LinearMap.range f).spanRank ≤ (⊤ : Submodule R M).spanRank := by simpa using spanRank_map_le f ⊤ @@ -341,9 +355,12 @@ lemma Ideal.spanRank_map_le : (I.map f).spanRank ≤ I.spanRank := by open Submodule in variable {I} in -lemma Ideal.spanFinrank_map_le_of_fg (hI : I.FG) : (I.map f).spanFinrank ≤ I.spanFinrank := - (Cardinal.toNat_le_iff_le_of_lt_aleph0 (spanRank_finite_iff_fg.mpr (Ideal.FG.map hI f)) - ((spanRank_finite_iff_fg.mpr hI))).2 (spanRank_map_le f I) +lemma Ideal.spanFinrank_map_le_of_fg {S : Type*} [Semiring S] (f : R →+* S) (hI : I.FG) : + (I.map f).spanFinrank ≤ I.spanFinrank := by + nth_rw 1 [← Submodule.FG.generators_ncard hI, ← I.span_generators, Ideal.submodule_span_eq, + Ideal.map_span] + exact (Submodule.spanFinrank_span_le_ncard_of_finite ((Submodule.FG.finite_generators hI).image + f)).trans (Set.ncard_image_le (Submodule.FG.finite_generators hI)) end Ideal From 58ffb62f6fa05eba79f9d787b2ebdbaf6dd59be8 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 27 Feb 2026 23:13:13 +0800 Subject: [PATCH 27/64] apply to maximalIdeal --- Mathlib/RingTheory/Ideal/Cotangent.lean | 31 +++++++++++-------------- 1 file changed, 14 insertions(+), 17 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index ed232753ea503d..5ad81615cf8080 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -338,24 +338,21 @@ lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (maximalIdeal R).fg_of_isNoetherianRing -lemma spanFinrank_le_of_surjective [IsNoetherianRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] - (f : R →+* R') (surj : Function.Surjective f) : +lemma spanFinrank_le_of_surjective (fg : (maximalIdeal R).FG) {R' : Type*} [CommRing R'] + [IsLocalRing R'] (f : R →+* R') (surj : Function.Surjective f) : (maximalIdeal R').spanFinrank ≤ (maximalIdeal R).spanFinrank := by - let fin := Submodule.FG.finite_generators (maximalIdeal R).fg_of_isNoetherianRing - have hspan : Ideal.span (f '' (maximalIdeal R).generators) = maximalIdeal R' := by - have : Ideal.span (maximalIdeal R).generators = _ := (maximalIdeal R).span_generators - simpa [← Ideal.map_span, this, ((local_hom_TFAE f).out 0 4).mp (surj.isLocalHom f)] using - (Ideal.map_comap_of_surjective f surj (maximalIdeal R')) - have hle : (maximalIdeal R').spanFinrank ≤ (f '' (maximalIdeal R).generators).ncard := by - simpa [← hspan] using (Submodule.spanFinrank_span_le_ncard_of_finite (fin.image _)) - apply le_trans hle (le_of_le_of_eq (Set.ncard_image_le fin) - (Submodule.FG.generators_ncard (maximalIdeal R).fg_of_isNoetherianRing)) - -lemma spanFinrank_eq_of_ringEquiv [IsNoetherianRing R] {R' : Type*} [CommRing R'] [IsLocalRing R'] - (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := - let _ := isNoetherianRing_of_ringEquiv R e - le_antisymm (spanFinrank_le_of_surjective e.symm.toRingHom e.symm.surjective) - (spanFinrank_le_of_surjective e.toRingHom e.surjective) + have comapeq := ((local_hom_TFAE f).out 0 4).mp (surj.isLocalHom f) + rw [← Ideal.map_comap_of_surjective f surj (maximalIdeal R'), comapeq] + exact (maximalIdeal R).spanFinrank_map_le_of_fg f fg + +lemma spanFinrank_eq_of_ringEquiv (fg : (maximalIdeal R).FG) {R' : Type*} [CommRing R'] + [IsLocalRing R'] (e : R ≃+* R') : + (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := by + refine le_antisymm (spanFinrank_le_of_surjective ?_ e.symm.toRingHom e.symm.surjective) + (spanFinrank_le_of_surjective fg e.toRingHom e.surjective) + have comapeq := ((local_hom_TFAE _).out 0 4).mp (e.surjective.isLocalHom e.toRingHom) + rw [← Ideal.map_comap_of_surjective e.toRingHom e.surjective (maximalIdeal R'), comapeq] + exact fg.map e.toRingHom end spanRank From 5d2512d892bedc89ee188fa81f06e236fd52074b Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 28 Feb 2026 11:28:12 +0800 Subject: [PATCH 28/64] fix layout --- Mathlib/Algebra/Module/SpanRank.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 1cddbd371452e6..1d763ebf6e1c4d 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -289,9 +289,9 @@ lemma spanRank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] N obtain rfl : span R s = p := by simpa [(map_injective_of_injective hf).eq_iff] using e grw [← hs, spanRank_span_le_card, Cardinal.mk_image_eq hf] -lemma spanFinrank_map_eq_of_injective {L : Type*} [AddCommMonoid L] [Module S L] [RingHomSurjective σ] - (f : M →ₛₗ[σ] L) (hf : Function.Injective f) {p : Submodule R M} (hp : p.FG) : - (p.map f).spanFinrank = p.spanFinrank := by +lemma spanFinrank_map_eq_of_injective {L : Type*} [AddCommMonoid L] [Module S L] + [RingHomSurjective σ] (f : M →ₛₗ[σ] L) (hf : Function.Injective f) {p : Submodule R M} + (hp : p.FG) : (p.map f).spanFinrank = p.spanFinrank := by refine (spanFinrank_map_le_of_fg f hp).antisymm ?_ obtain ⟨s, hs⟩ : ∃ y, f '' y = (p.map f).generators := Set.subset_range_iff_exists_image_eq.mp ((subset_span.trans (p.map f).span_generators.le).trans LinearMap.map_le_range) From e2f91b2908391bada492ef6a0462441a6ef4e968 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 28 Feb 2026 11:35:43 +0800 Subject: [PATCH 29/64] add a version without fg --- Mathlib/RingTheory/Ideal/Cotangent.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 5ad81615cf8080..ec014a50c27420 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -345,7 +345,7 @@ lemma spanFinrank_le_of_surjective (fg : (maximalIdeal R).FG) {R' : Type*} [Comm rw [← Ideal.map_comap_of_surjective f surj (maximalIdeal R'), comapeq] exact (maximalIdeal R).spanFinrank_map_le_of_fg f fg -lemma spanFinrank_eq_of_ringEquiv (fg : (maximalIdeal R).FG) {R' : Type*} [CommRing R'] +lemma spanFinrank_eq_of_ringEquiv_of_fg (fg : (maximalIdeal R).FG) {R' : Type*} [CommRing R'] [IsLocalRing R'] (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := by refine le_antisymm (spanFinrank_le_of_surjective ?_ e.symm.toRingHom e.symm.surjective) @@ -354,6 +354,14 @@ lemma spanFinrank_eq_of_ringEquiv (fg : (maximalIdeal R).FG) {R' : Type*} [CommR rw [← Ideal.map_comap_of_surjective e.toRingHom e.surjective (maximalIdeal R'), comapeq] exact fg.map e.toRingHom +lemma spanFinrank_eq_of_ringEquiv {R' : Type*} [CommRing R'] [IsLocalRing R'] (e : R ≃+* R') : + (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := by + by_cases fgR : (maximalIdeal R).FG + · exact spanFinrank_eq_of_ringEquiv_of_fg fgR e + · by_cases fgR' : (maximalIdeal R').FG + · exact (spanFinrank_eq_of_ringEquiv_of_fg fgR' e.symm).symm + · rw [Submodule.spanFinrank_of_not_fg fgR, Submodule.spanFinrank_of_not_fg fgR'] + end spanRank end IsLocalRing From 782bd758cdb0f3b507beca8156c2404fbfa85897 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 5 Mar 2026 16:00:32 +0800 Subject: [PATCH 30/64] Update Cotangent.lean --- Mathlib/RingTheory/Ideal/Cotangent.lean | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index da43c8e3786c05..7d20e456fa1545 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -380,21 +380,23 @@ lemma spanFinrank_le_of_surjective (fg : (maximalIdeal R).FG) {R' : Type*} [Comm rw [← Ideal.map_comap_of_surjective f surj (maximalIdeal R'), comapeq] exact (maximalIdeal R).spanFinrank_map_le_of_fg f fg -lemma spanFinrank_eq_of_ringEquiv_of_fg (fg : (maximalIdeal R).FG) {R' : Type*} [CommRing R'] - [IsLocalRing R'] (e : R ≃+* R') : - (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := by - refine le_antisymm (spanFinrank_le_of_surjective ?_ e.symm.toRingHom e.symm.surjective) - (spanFinrank_le_of_surjective fg e.toRingHom e.surjective) - have comapeq := ((local_hom_TFAE _).out 0 4).mp (e.surjective.isLocalHom e.toRingHom) - rw [← Ideal.map_comap_of_surjective e.toRingHom e.surjective (maximalIdeal R'), comapeq] - exact fg.map e.toRingHom - lemma spanFinrank_eq_of_ringEquiv {R' : Type*} [CommRing R'] [IsLocalRing R'] (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := by by_cases fgR : (maximalIdeal R).FG - · exact spanFinrank_eq_of_ringEquiv_of_fg fgR e + · have eqmap : maximalIdeal R' = (maximalIdeal R).map e := by + rw [← Ideal.comap_symm, eq_comm] + exact (((local_hom_TFAE _).out 0 4).mp (e.symm.surjective.isLocalHom (e.symm : R' →+* R))) + refine le_antisymm (spanFinrank_le_of_surjective ?_ e.symm.toRingHom e.symm.surjective) + (spanFinrank_le_of_surjective fgR e.toRingHom e.surjective) + rw [eqmap] + exact fgR.map e.toRingHom · by_cases fgR' : (maximalIdeal R').FG - · exact (spanFinrank_eq_of_ringEquiv_of_fg fgR' e.symm).symm + · have eqmap' : maximalIdeal R = (maximalIdeal R').map e.symm := by + rw [Ideal.map_symm, eq_comm] + exact ((local_hom_TFAE _).out 0 4).mp (e.surjective.isLocalHom (e : R →+* R')) + absurd fgR + rw [eqmap'] + exact fgR'.map e.symm.toRingHom · rw [Submodule.spanFinrank_of_not_fg fgR, Submodule.spanFinrank_of_not_fg fgR'] end spanRank From 1dc4e82698fd0302995712229f232431f49a02d8 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 5 Mar 2026 16:02:32 +0800 Subject: [PATCH 31/64] golf --- Mathlib/RingTheory/Ideal/Cotangent.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 7d20e456fa1545..1dbf51a787e564 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -388,15 +388,13 @@ lemma spanFinrank_eq_of_ringEquiv {R' : Type*} [CommRing R'] [IsLocalRing R'] (e exact (((local_hom_TFAE _).out 0 4).mp (e.symm.surjective.isLocalHom (e.symm : R' →+* R))) refine le_antisymm (spanFinrank_le_of_surjective ?_ e.symm.toRingHom e.symm.surjective) (spanFinrank_le_of_surjective fgR e.toRingHom e.surjective) - rw [eqmap] - exact fgR.map e.toRingHom + simpa only [eqmap] using fgR.map e.toRingHom · by_cases fgR' : (maximalIdeal R').FG · have eqmap' : maximalIdeal R = (maximalIdeal R').map e.symm := by rw [Ideal.map_symm, eq_comm] exact ((local_hom_TFAE _).out 0 4).mp (e.surjective.isLocalHom (e : R →+* R')) absurd fgR - rw [eqmap'] - exact fgR'.map e.symm.toRingHom + simpa only [eqmap'] using fgR'.map e.symm.toRingHom · rw [Submodule.spanFinrank_of_not_fg fgR, Submodule.spanFinrank_of_not_fg fgR'] end spanRank From ab939dfb40f39b7cbd79fb44b40043a52ab6017f Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 5 Mar 2026 16:05:32 +0800 Subject: [PATCH 32/64] fix --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index 05eecd688bd4a7..37d99ed0c93f46 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -66,6 +66,7 @@ lemma iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : instance {k : Type*} [Field k] : IsRegularLocalRing k := by simp [isRegularLocalRing_def, maximalIdeal_eq_bot] +set_option backward.isDefEq.respectTransparency false in instance [IsDomain R] [IsDiscreteValuationRing R] : IsRegularLocalRing R := by apply of_spanFinrank_maximalIdeal_le rcases IsPrincipalIdealRing.principal (maximalIdeal R) with ⟨x, hx⟩ From b12ab5442241b19e1f7e4870d741460f64f25674 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 6 Mar 2026 17:46:11 +0800 Subject: [PATCH 33/64] golf --- Mathlib/Algebra/Module/SpanRank.lean | 3 ++ Mathlib/RingTheory/Ideal/Cotangent.lean | 39 ++++++++++--------------- 2 files changed, 18 insertions(+), 24 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index cd50b1e4114322..6a4cc2f5454328 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -311,6 +311,9 @@ lemma spanRank_range_le [RingHomSurjective σ] (f : M →ₛₗ[σ] N) : lemma spanRank_top (p : Submodule R M) : (⊤ : Submodule R p).spanRank = p.spanRank := by simpa using (spanRank_map_eq_of_injective _ p.subtype_injective ⊤).symm +lemma spanFinrank_top (p : Submodule R M) : (⊤ : Submodule R p).spanFinrank = p.spanFinrank := by + simp [Submodule.spanFinrank] + lemma spanRank_eq_of_equiv {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] N) : (⊤ : Submodule R M).spanRank = (⊤ : Submodule S N).spanRank := by diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 1dbf51a787e564..72b84d671cbb2e 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -13,8 +13,8 @@ public import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition public import Mathlib.LinearAlgebra.FiniteDimensional.Defs public import Mathlib.RingTheory.Filtration public import Mathlib.RingTheory.Ideal.Operations +public import Mathlib.RingTheory.LocalRing.Module public import Mathlib.RingTheory.LocalRing.ResidueField.Basic -public import Mathlib.RingTheory.Nakayama /-! # The module `I ⧸ I ^ 2` @@ -331,35 +331,26 @@ section spanRank open IsLocalRing -set_option backward.isDefEq.respectTransparency false in lemma spanFinrank_eq_finrank_quotient {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M) (fg : N.FG) : N.spanFinrank = Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by - let _ : Field (R ⧸ maximalIdeal R) := Ideal.Quotient.field (maximalIdeal R) + let : Field (R ⧸ maximalIdeal R) := Ideal.Quotient.field (maximalIdeal R) let fin : Module.Finite R N := Module.Finite.iff_fg.mpr fg - rw [Module.finrank_eq_spanFinrank_of_free] - let k := R ⧸ maximalIdeal R - let Q := N ⧸ (maximalIdeal R) • (⊤ : Submodule R N) + let mN := (maximalIdeal R) • (⊤ : Submodule R N) + rw [Module.finrank_eq_spanFinrank_of_free, ← Submodule.spanFinrank_top] apply le_antisymm - · let s : Set Q := (⊤ : Submodule k Q).generators - have hfgQ : (⊤ : Submodule k Q).FG := Module.Finite.fg_top - have hs_span_R : Submodule.span R s = (⊤ : Submodule R Q) := by - rw [← Submodule.coe_eq_univ, ← Submodule.coe_span_eq_span_of_surjective R k + · let s : Set (N ⧸ mN) := (⊤ : Submodule (R ⧸ maximalIdeal R) (N ⧸ mN)).generators + have fins : s.Finite := Module.Finite.fg_top.finite_generators + let t := Function.surjInv (Submodule.mkQ_surjective mN) '' s + have : Submodule.mkQ mN '' t = s := by rw [← s.image_comp, Function.comp_surjInv, s.image_id] + have eqtop : Submodule.span R t = ⊤ := by + rw [← IsLocalRing.map_mkQ_eq_top, Submodule.map_span, this, ← Submodule.coe_eq_univ, + ← Submodule.coe_span_eq_span_of_surjective R (R ⧸ maximalIdeal R) Ideal.Quotient.mk_surjective, Submodule.coe_eq_univ, Submodule.span_generators _] - obtain ⟨t, ht_inj, ht_image, ht_span⟩ := - Submodule.exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot - s fin.1 (IsLocalRing.maximalIdeal_le_jacobson _) (by simpa using hs_span_R) - have htfinite : t.Finite := by - simpa only [← Set.finite_image_iff ht_inj, ht_image] using hfgQ.finite_generators - have hle : N.spanFinrank ≤ (Subtype.val '' t).ncard := by - simpa [(Submodule.span_val_image_eq_iff N t).mpr ht_span] using - (Submodule.spanFinrank_span_le_ncard_of_finite (R := R) (htfinite.image Subtype.val)) - have hcard : t.ncard = s.ncard := by simpa only [← ht_image] using ht_inj.ncard_image.symm - exact le_of_le_of_eq hle ((Set.ncard_image_of_injective _ (Subtype.val_injective)).trans - (hcard.trans hfgQ.generators_ncard)) - · have : (⊤ : Submodule R N).spanFinrank = N.spanFinrank := by simp [Submodule.spanFinrank] - rw [← this] - let f : N →ₛₗ[Ideal.Quotient.mk (maximalIdeal R)] Q := { __ := Submodule.mkQ _ } + simp only [← eqtop, t] + grw [Submodule.spanFinrank_span_le_ncard_of_finite (fins.image _), Set.ncard_image_le fins, + Module.Finite.fg_top.generators_ncard] + · let f : N →ₛₗ[Ideal.Quotient.mk (maximalIdeal R)] (N ⧸ mN) := { __ := Submodule.mkQ _ } convert Submodule.spanFinrank_map_le_of_fg f fin.1 symm simpa [f, LinearMap.range_eq_top] using Submodule.mkQ_surjective _ From 496f5a5e3124ef01f0fe0666d957aebb3bc9de5d Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 6 Mar 2026 17:58:58 +0800 Subject: [PATCH 34/64] a temporary fix --- Mathlib/Algebra/Module/SpanRank.lean | 3 --- Mathlib/RingTheory/Ideal/Cotangent.lean | 3 ++- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 6a4cc2f5454328..cd50b1e4114322 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -311,9 +311,6 @@ lemma spanRank_range_le [RingHomSurjective σ] (f : M →ₛₗ[σ] N) : lemma spanRank_top (p : Submodule R M) : (⊤ : Submodule R p).spanRank = p.spanRank := by simpa using (spanRank_map_eq_of_injective _ p.subtype_injective ⊤).symm -lemma spanFinrank_top (p : Submodule R M) : (⊤ : Submodule R p).spanFinrank = p.spanFinrank := by - simp [Submodule.spanFinrank] - lemma spanRank_eq_of_equiv {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] N) : (⊤ : Submodule R M).spanRank = (⊤ : Submodule S N).spanRank := by diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 72b84d671cbb2e..cb2045a8d5115e 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -337,7 +337,8 @@ lemma spanFinrank_eq_finrank_quotient {M : Type*} [AddCommGroup M] [Module R M] let : Field (R ⧸ maximalIdeal R) := Ideal.Quotient.field (maximalIdeal R) let fin : Module.Finite R N := Module.Finite.iff_fg.mpr fg let mN := (maximalIdeal R) • (⊤ : Submodule R N) - rw [Module.finrank_eq_spanFinrank_of_free, ← Submodule.spanFinrank_top] + have : (⊤ : Submodule R N).spanFinrank = N.spanFinrank := by simp [Submodule.spanFinrank] + rw [Module.finrank_eq_spanFinrank_of_free, ← this] apply le_antisymm · let s : Set (N ⧸ mN) := (⊤ : Submodule (R ⧸ maximalIdeal R) (N ⧸ mN)).generators have fins : s.Finite := Module.Finite.fg_top.finite_generators From dd823398f4cfafd6feb03e4a07c4e399de386caa Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 6 Mar 2026 20:05:22 +0800 Subject: [PATCH 35/64] fix --- Mathlib/RingTheory/KrullDimension/Regular.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/KrullDimension/Regular.lean b/Mathlib/RingTheory/KrullDimension/Regular.lean index 0dfaa849ab770d..e6d3a6ddf83cd1 100644 --- a/Mathlib/RingTheory/KrullDimension/Regular.lean +++ b/Mathlib/RingTheory/KrullDimension/Regular.lean @@ -23,13 +23,13 @@ public import Mathlib.RingTheory.Spectrum.Prime.LTSeries public section +open RingTheory Sequence IsLocalRing Ideal PrimeSpectrum Pointwise + namespace Module variable {R : Type*} [CommRing R] [IsNoetherianRing R] {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] -open RingTheory Sequence IsLocalRing Ideal PrimeSpectrum Pointwise - omit [IsNoetherianRing R] [Module.Finite R M] in lemma exists_ltSeries_support_isMaximal_last_of_ltSeries_support (q : LTSeries (support R M)) : ∃ p : LTSeries (support R M), q.length ≤ p.length ∧ p.last.1.1.IsMaximal := by From 54003cd0584ed82b1f9ef22a570e45a790163c5f Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 13 Mar 2026 11:23:12 +0800 Subject: [PATCH 36/64] move decl --- Mathlib/LinearAlgebra/Span/Basic.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/Mathlib/LinearAlgebra/Span/Basic.lean b/Mathlib/LinearAlgebra/Span/Basic.lean index ed32c20f733a5d..54d2c8b2f343e3 100644 --- a/Mathlib/LinearAlgebra/Span/Basic.lean +++ b/Mathlib/LinearAlgebra/Span/Basic.lean @@ -432,11 +432,14 @@ theorem _root_.LinearMap.exists_ne_zero_of_sSup_eq {N : Submodule R M} {f : N by rw [sSup_eq_iSup] at hs; rw [sSup_image, ← hs, biSup_comap_subtype_eq_top] ⟨m, hm, fun eq ↦ ne (LinearMap.ext fun x ↦ congr($eq ⟨x, x.2⟩))⟩ +lemma span_val_image_eq_iff (p : Submodule R M) (s : Set p) : + span R (Subtype.val '' s) = p ↔ span R s = ⊤ := by + simp [← (Submodule.map_injective_of_injective p.injective_subtype).eq_iff, Submodule.map_span] + lemma span_range_subtype_eq_top_iff {ι : Type*} (p : Submodule R M) {s : ι → M} (hs : ∀ i, s i ∈ p) : span R (Set.range fun i ↦ (⟨s i, hs i⟩ : p)) = ⊤ ↔ span R (Set.range s) = p := by - rw [← (map_injective_of_injective p.injective_subtype).eq_iff] - simp [map_span, ← Set.range_comp, Function.comp_def] + simp [← span_val_image_eq_iff, ← Set.range_comp, Function.comp_def] lemma comap_le_comap_iff_of_le_range {f : M →ₛₗ[σ₁₂] M₂} [RingHomSurjective σ₁₂] {p q : Submodule R₂ M₂} (hp : p ≤ LinearMap.range f) : @@ -874,8 +877,3 @@ theorem coord_apply_smul (y : Submodule.span R ({x} : Set M)) : coord R M x h y Subtype.ext_iff.1 <| (toSpanNonzeroSingleton R M x h).apply_symm_apply _ end LinearEquiv - -lemma Submodule.span_val_image_eq_iff {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] - (p : Submodule R M) (s : Set p) : - Submodule.span R (Subtype.val '' s) = p ↔ Submodule.span R s = ⊤ := by - simp [← (Submodule.map_injective_of_injective p.injective_subtype).eq_iff, Submodule.map_span] From ef5b60db814137250d529c090c7f5fd2d5becf24 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 13 Mar 2026 11:31:55 +0800 Subject: [PATCH 37/64] generalize universe --- Mathlib/Algebra/Module/SpanRank.lean | 108 +++++++++++++++----------- Mathlib/SetTheory/Cardinal/ToNat.lean | 10 +++ 2 files changed, 71 insertions(+), 47 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index cd50b1e4114322..8c0881df098351 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -54,7 +54,7 @@ namespace Submodule section Defs -universe u +universe u v variable {R : Type*} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] @@ -132,6 +132,14 @@ lemma fg_iff_spanRank_eq_spanFinrank {p : Submodule R M} : p.spanRank = p.spanFi lemma FG.spanRank_eq_spanFinrank {p : Submodule R M} (fg : p.FG) : p.spanRank = p.spanFinrank := fg_iff_spanRank_eq_spanFinrank.mpr fg +lemma FG.spanRank_le_iff {p : Submodule R M} (hp : p.FG) (n : ℕ) : + p.spanRank ≤ n ↔ p.spanFinrank ≤ n := + (Cardinal.toNat_le_iff_of_lt_aleph0 n (by simpa)).symm + +lemma FG.spanRank_eq_iff {p : Submodule R M} (hp : p.FG) (n : ℕ) : + p.spanRank = n ↔ p.spanFinrank = n := + (Cardinal.toNat_eq_iff_of_lt_aleph0 n (by simpa)).symm + lemma spanRank_span_le_card (s : Set M) : (Submodule.span R s).spanRank ≤ #s := by rw [spanRank] let s' : {s1 : Set M // span R s1 = span R s} := ⟨s, rfl⟩ @@ -182,15 +190,19 @@ theorem FG.exists_span_set_encard_eq_spanFinrank {p : Submodule R M} (h : p.FG) rw [Set.encard, ENat.card, spanFinrank, hs₁, this] simp -/-- For a finitely generated submodule, its spanRank is less than or equal to a cardinal `a` - if and only if there is a generating subset with cardinality less than or equal to `a`. -/ -lemma FG.spanRank_le_iff_exists_span_set_card_le (p : Submodule R M) {a : Cardinal} : - p.spanRank ≤ a ↔ ∃ s : Set M, #s ≤ a ∧ span R s = p := by +lemma lift_spanRank_le_iff_exists_span_set_card_le (p : Submodule R M) {a : Cardinal.{max u v}} : + Cardinal.lift.{v} p.spanRank ≤ a ↔ ∃ s : Set M, Cardinal.lift.{v} #s ≤ a ∧ span R s = p := by constructor · intro h obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p exact ⟨s, ⟨hs₁ ▸ h, hs₂⟩⟩ - · exact (fun ⟨s, ⟨hs₁, hs₂⟩⟩ ↦ hs₂.symm ▸ (le_trans (spanRank_span_le_card s) hs₁)) + · exact fun ⟨s, ⟨h₁, h₂⟩⟩ ↦ h₂.symm ▸ (Cardinal.lift_le.mpr (spanRank_span_le_card s)).trans h₁ + +/-- For a finitely generated submodule, its spanRank is less than or equal to a cardinal `a` + if and only if there is a generating subset with cardinality less than or equal to `a`. -/ +lemma FG.spanRank_le_iff_exists_span_set_card_le (p : Submodule R M) {a : Cardinal} : + p.spanRank ≤ a ↔ ∃ s : Set M, #s ≤ a ∧ span R s = p := by + convert lift_spanRank_le_iff_exists_span_set_card_le p (a := a) <;> simp @[simp] lemma spanRank_eq_zero_iff_eq_bot {I : Submodule R M} : I.spanRank = 0 ↔ I = ⊥ := by @@ -261,47 +273,51 @@ end Submodule section map -universe u +universe u v namespace Submodule section Semilinear variable {R S : Type*} {M N : Type u} [Semiring R] [Semiring S] {σ : R →+* S} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] + {L : Type v} [AddCommMonoid L] [Module S L] -lemma spanRank_map_le [RingHomSurjective σ] (f : M →ₛₗ[σ] N) - (p : Submodule R M) : (p.map f).spanRank ≤ p.spanRank := by - rw [← generators_card p, FG.spanRank_le_iff_exists_span_set_card_le] - exact ⟨f '' p.generators, Cardinal.mk_image_le, le_antisymm (span_le.2 (fun n ⟨m, hm, h⟩ ↦ +lemma lift_spanRank_map_le [RingHomSurjective σ] (f : M →ₛₗ[σ] L) (p : Submodule R M) : + Cardinal.lift.{u} (p.map f).spanRank ≤ Cardinal.lift.{v} p.spanRank := by + rw [← generators_card p, lift_spanRank_le_iff_exists_span_set_card_le] + exact ⟨f '' p.generators, Cardinal.mk_image_le_lift, le_antisymm (span_le.2 (fun n ⟨m, hm, h⟩ ↦ ⟨m, span_generators p ▸ subset_span hm, h⟩)) (by simp [span_generators])⟩ -lemma spanFinrank_map_le_of_fg {L : Type*} [AddCommMonoid L] [Module S L] [RingHomSurjective σ] - (f : M →ₛₗ[σ] L) {p : Submodule R M} (hp : p.FG) : (p.map f).spanFinrank ≤ p.spanFinrank := by - nth_rw 1 [← p.span_generators, Submodule.map_span, ← hp.generators_ncard] - exact (Submodule.spanFinrank_span_le_ncard_of_finite (hp.finite_generators.image f)).trans - (Set.ncard_image_le hp.finite_generators) +lemma spanRank_map_le [RingHomSurjective σ] (f : M →ₛₗ[σ] N) (p : Submodule R M) : + (p.map f).spanRank ≤ p.spanRank := by + simpa using lift_spanRank_map_le f p -lemma spanRank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] N) - (hf : Function.Injective f) (p : Submodule R M) : (p.map f).spanRank = p.spanRank := by - refine (spanRank_map_le f p).antisymm ?_ +lemma spanFinrank_map_le_of_fg {L : Type v} [AddCommMonoid L] [Module S L] [RingHomSurjective σ] + (f : M →ₛₗ[σ] L) {p : Submodule R M} (hp : p.FG) : (p.map f).spanFinrank ≤ p.spanFinrank := by + rw [← (hp.map f).spanRank_le_iff, ← Cardinal.lift_le.{u}, Cardinal.lift_natCast, + ← Cardinal.lift_natCast.{v}, ← hp.spanRank_eq_spanFinrank] + exact p.lift_spanRank_map_le f + +lemma lift_spanRank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] L) + (hf : Function.Injective f) (p : Submodule R M) : + Cardinal.lift.{u} (p.map f).spanRank = Cardinal.lift.{v} p.spanRank := by + refine (lift_spanRank_map_le f p).antisymm ?_ obtain ⟨s, hs, e⟩ := (p.map f).exists_span_set_card_eq_spanRank obtain ⟨s, rfl⟩ : ∃ y, f '' y = s := Set.subset_range_iff_exists_image_eq.mp ((subset_span.trans e.le).trans LinearMap.map_le_range) obtain rfl : span R s = p := by simpa [(map_injective_of_injective hf).eq_iff] using e - grw [← hs, spanRank_span_le_card, Cardinal.mk_image_eq hf] - -lemma spanFinrank_map_eq_of_injective {L : Type*} [AddCommMonoid L] [Module S L] - [RingHomSurjective σ] (f : M →ₛₗ[σ] L) (hf : Function.Injective f) {p : Submodule R M} - (hp : p.FG) : (p.map f).spanFinrank = p.spanFinrank := by - refine (spanFinrank_map_le_of_fg f hp).antisymm ?_ - obtain ⟨s, hs⟩ : ∃ y, f '' y = (p.map f).generators := Set.subset_range_iff_exists_image_eq.mp - ((subset_span.trans (p.map f).span_generators.le).trans LinearMap.map_le_range) - have fin : s.Finite := - Set.Finite.of_finite_image (by simpa [hs] using (hp.map f).finite_generators) hf.injOn - have : span R s = p := map_injective_of_injective hf - (by rw [Submodule.map_span, hs, (p.map f).span_generators]) - nth_grw 1 [← this, Submodule.spanFinrank_span_le_ncard_of_finite fin, - ← (hp.map f).generators_ncard, ← hf.injOn.ncard_image, hs] + grw [← hs, Cardinal.mk_image_eq_lift _ _ hf, Cardinal.lift_le, spanRank_span_le_card] + +lemma spanRank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] N) + (hf : Function.Injective f) (p : Submodule R M) : (p.map f).spanRank = p.spanRank := by + simpa using lift_spanRank_map_eq_of_injective f hf p + +lemma spanFinrank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] L) + (hf : Function.Injective f) {p : Submodule R M} (hp : p.FG) : + (p.map f).spanFinrank = p.spanFinrank := by + rw [← (hp.map f).spanRank_eq_iff, ← Cardinal.lift_inj.{v, u}, Cardinal.lift_natCast, + ← Cardinal.lift_natCast.{v}, ← hp.spanRank_eq_spanFinrank] + exact lift_spanRank_map_eq_of_injective f hf p lemma spanRank_range_le [RingHomSurjective σ] (f : M →ₛₗ[σ] N) : (LinearMap.range f).spanRank ≤ (⊤ : Submodule R M).spanRank := by @@ -342,21 +358,26 @@ end Submodule section Ideal -variable {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (I : Ideal R) +variable {R S : Type u} [Semiring R] [Semiring S] {T : Type v} [Semiring T] open Submodule in -lemma Ideal.spanRank_map_le : (I.map f).spanRank ≤ I.spanRank := by - rw [← generators_card I, FG.spanRank_le_iff_exists_span_set_card_le] - refine ⟨f '' I.generators, Cardinal.mk_image_le, le_antisymm (span_le.2 (fun s ⟨r, hr, hfr⟩ ↦ +lemma Ideal.lift_spanRank_map_le (f : R →+* T) (I : Ideal R) : + Cardinal.lift.{u} (I.map f).spanRank ≤ Cardinal.lift.{v} I.spanRank := by + rw [← generators_card I, lift_spanRank_le_iff_exists_span_set_card_le] + refine ⟨f '' I.generators, Cardinal.mk_image_le_lift, le_antisymm (span_le.2 (fun s ⟨r, hr, hfr⟩ ↦ hfr ▸ mem_map_of_mem _ <| span_generators I ▸ subset_span hr)) ?_⟩ refine map_le_of_le_comap (fun r hr ↦ ?_) simp only [submodule_span_eq, mem_comap] rw [← map_span, ← submodule_span_eq, span_generators] exact mem_map_of_mem f hr +open Submodule in +lemma Ideal.spanRank_map_le (f : R →+* S) (I : Ideal R) : (I.map f).spanRank ≤ I.spanRank := by + simpa using I.lift_spanRank_map_le f + open Submodule in variable {I} in -lemma Ideal.spanFinrank_map_le_of_fg {S : Type*} [Semiring S] (f : R →+* S) (hI : I.FG) : +lemma Ideal.spanFinrank_map_le_of_fg (f : R →+* T) (I : Ideal R) (hI : I.FG) : (I.map f).spanFinrank ≤ I.spanFinrank := by nth_rw 1 [← Submodule.FG.generators_ncard hI, ← I.span_generators, Ideal.submodule_span_eq, Ideal.map_span] @@ -385,16 +406,9 @@ theorem Submodule.rank_eq_spanRank_of_free [Module.Free R M] [StrongRankConditio rw [← Basis.mk_eq_rank'' B, ← Basis.mk_eq_spanRank B, ← Cardinal.lift_id #(Set.range B), Cardinal.mk_range_eq_of_injective B.injective, Cardinal.lift_id _] -lemma Module.finrank_eq_spanFinrank_of_free [StrongRankCondition R] - (M : Type*) [AddCommGroup M] [Module R M] [Module.Free R M] : +lemma Module.finrank_eq_spanFinrank_of_free [StrongRankCondition R] [Module.Free R M] : Module.finrank R M = (⊤ : Submodule R M).spanFinrank := by - by_cases fin : Module.Finite R M - · have : Submodule.spanFinrank (⊤ : Submodule R M) = Module.rank R M := by - rw [← Submodule.fg_iff_spanRank_eq_spanFinrank.mpr fin.1, - Submodule.rank_eq_spanRank_of_free] - simpa only [← Module.finrank_eq_rank, Nat.cast_inj] using this.symm - · have fin' : ¬ (⊤ : Submodule R M).FG := Not.intro (fun h ↦ fin ⟨h⟩) - rw [Module.finrank_of_not_finite fin, Submodule.spanFinrank_of_not_fg fin'] + simp [Module.finrank, Submodule.spanFinrank, Submodule.rank_eq_spanRank_of_free] theorem Submodule.rank_le_spanRank [StrongRankCondition R] : Module.rank R M ≤ (⊤ : Submodule R M).spanRank := by diff --git a/Mathlib/SetTheory/Cardinal/ToNat.lean b/Mathlib/SetTheory/Cardinal/ToNat.lean index 83949ba3d507c5..987a4065a410ce 100644 --- a/Mathlib/SetTheory/Cardinal/ToNat.lean +++ b/Mathlib/SetTheory/Cardinal/ToNat.lean @@ -160,4 +160,14 @@ lemma natCast_toNat_le (a : Cardinal) : (toNat a : Cardinal) ≤ a := by · simp [cast_toNat_of_lt_aleph0 h] · simp [Cardinal.toNat_apply_of_aleph0_le h] +lemma toNat_le_iff_of_lt_aleph0 {a : Cardinal.{u}} (n : ℕ) (lt : a < Cardinal.aleph0) : + a.toNat ≤ n ↔ a ≤ n := by + nth_rw 1 [← Cardinal.toNat_natCast.{u} n, + Cardinal.toNat_le_iff_le_of_lt_aleph0 lt (Cardinal.natCast_lt_aleph0)] + +lemma toNat_eq_iff_of_lt_aleph0 {a : Cardinal.{u}} (n : ℕ) (lt : a < Cardinal.aleph0) : + a.toNat = n ↔ a = n := by + nth_rw 2 [← Cardinal.cast_toNat_of_lt_aleph0 lt] + exact Nat.cast_inj.symm + end Cardinal From c50145c1f70e03b57b2d737ff07d78affabf732e Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 13 Mar 2026 12:13:12 +0800 Subject: [PATCH 38/64] fix --- Mathlib/Algebra/Module/SpanRank.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 8c0881df098351..8ca0b795838cb2 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -376,8 +376,7 @@ lemma Ideal.spanRank_map_le (f : R →+* S) (I : Ideal R) : (I.map f).spanRank simpa using I.lift_spanRank_map_le f open Submodule in -variable {I} in -lemma Ideal.spanFinrank_map_le_of_fg (f : R →+* T) (I : Ideal R) (hI : I.FG) : +lemma Ideal.spanFinrank_map_le_of_fg (f : R →+* T) {I : Ideal R} (hI : I.FG) : (I.map f).spanFinrank ≤ I.spanFinrank := by nth_rw 1 [← Submodule.FG.generators_ncard hI, ← I.span_generators, Ideal.submodule_span_eq, Ideal.map_span] From 9076eebf147dbb1c6be25db31dc013bd1c8546f6 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 13 Mar 2026 12:23:11 +0800 Subject: [PATCH 39/64] Update SpanRank.lean --- Mathlib/Algebra/Module/SpanRank.lean | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 8ca0b795838cb2..9ade7e9603f3c3 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -378,10 +378,15 @@ lemma Ideal.spanRank_map_le (f : R →+* S) (I : Ideal R) : (I.map f).spanRank open Submodule in lemma Ideal.spanFinrank_map_le_of_fg (f : R →+* T) {I : Ideal R} (hI : I.FG) : (I.map f).spanFinrank ≤ I.spanFinrank := by - nth_rw 1 [← Submodule.FG.generators_ncard hI, ← I.span_generators, Ideal.submodule_span_eq, - Ideal.map_span] - exact (Submodule.spanFinrank_span_le_ncard_of_finite ((Submodule.FG.finite_generators hI).image - f)).trans (Set.ncard_image_le (Submodule.FG.finite_generators hI)) + rw [← Submodule.FG.spanRank_le_iff (hI.map f), ← Cardinal.lift_le.{u}, Cardinal.lift_natCast, + ← Cardinal.lift_natCast.{v}, ← Submodule.FG.spanRank_eq_spanFinrank hI] + exact I.lift_spanRank_map_le f + +lemma Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv (f : R ≃+* T) {I : Ideal R} (hI : I.FG) : + (I.map f).spanFinrank = I.spanFinrank := by + apply (I.spanFinrank_map_le_of_fg (f : R →+* T) hI).antisymm + nth_rw 1 [← Ideal.map_of_equiv f (I := I)] + exact Ideal.spanFinrank_map_le_of_fg (f.symm : T →+* R) (hI.map (f : R →+* T)) end Ideal From 0d6b26719df32a408c796ea315b850662f2795c0 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 13 Mar 2026 12:34:45 +0800 Subject: [PATCH 40/64] golf --- Mathlib/Algebra/Module/SpanRank.lean | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 9ade7e9603f3c3..ef57d186c16ffb 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -315,9 +315,8 @@ lemma spanRank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] N lemma spanFinrank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] L) (hf : Function.Injective f) {p : Submodule R M} (hp : p.FG) : (p.map f).spanFinrank = p.spanFinrank := by - rw [← (hp.map f).spanRank_eq_iff, ← Cardinal.lift_inj.{v, u}, Cardinal.lift_natCast, - ← Cardinal.lift_natCast.{v}, ← hp.spanRank_eq_spanFinrank] - exact lift_spanRank_map_eq_of_injective f hf p + rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v}, + ← Cardinal.toNat_lift.{v, u}, lift_spanRank_map_eq_of_injective f hf p] lemma spanRank_range_le [RingHomSurjective σ] (f : M →ₛₗ[σ] N) : (LinearMap.range f).spanRank ≤ (⊤ : Submodule R M).spanRank := by @@ -371,22 +370,29 @@ lemma Ideal.lift_spanRank_map_le (f : R →+* T) (I : Ideal R) : rw [← map_span, ← submodule_span_eq, span_generators] exact mem_map_of_mem f hr -open Submodule in +lemma Ideal.lift_spanRank_map_eq_of_ringEquiv (f : R ≃+* T) (I : Ideal R) : + Cardinal.lift.{u} (I.map f).spanRank = Cardinal.lift.{v} I.spanRank := by + apply (I.lift_spanRank_map_le (f : R →+* T)).antisymm + nth_rw 1 [← Ideal.map_of_equiv f (I := I)] + exact Ideal.lift_spanRank_map_le (f.symm : T →+* R) _ + lemma Ideal.spanRank_map_le (f : R →+* S) (I : Ideal R) : (I.map f).spanRank ≤ I.spanRank := by simpa using I.lift_spanRank_map_le f -open Submodule in +lemma Ideal.spanRank_map_eq_of_ringEquiv (f : R ≃+* S) (I : Ideal R) : + (I.map f).spanRank = I.spanRank := by + simpa using I.lift_spanRank_map_eq_of_ringEquiv f + lemma Ideal.spanFinrank_map_le_of_fg (f : R →+* T) {I : Ideal R} (hI : I.FG) : (I.map f).spanFinrank ≤ I.spanFinrank := by rw [← Submodule.FG.spanRank_le_iff (hI.map f), ← Cardinal.lift_le.{u}, Cardinal.lift_natCast, ← Cardinal.lift_natCast.{v}, ← Submodule.FG.spanRank_eq_spanFinrank hI] exact I.lift_spanRank_map_le f -lemma Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv (f : R ≃+* T) {I : Ideal R} (hI : I.FG) : +lemma Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv (f : R ≃+* T) {I : Ideal R} : (I.map f).spanFinrank = I.spanFinrank := by - apply (I.spanFinrank_map_le_of_fg (f : R →+* T) hI).antisymm - nth_rw 1 [← Ideal.map_of_equiv f (I := I)] - exact Ideal.spanFinrank_map_le_of_fg (f.symm : T →+* R) (hI.map (f : R →+* T)) + rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v}, + ← Cardinal.toNat_lift.{v, u}, I.lift_spanRank_map_eq_of_ringEquiv f] end Ideal From 88a89b50cb537c558d8d426b900efffdb5d81f47 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 13 Mar 2026 12:37:20 +0800 Subject: [PATCH 41/64] golf more --- Mathlib/Algebra/Module/SpanRank.lean | 4 ++-- Mathlib/RingTheory/Ideal/Cotangent.lean | 18 ++++-------------- 2 files changed, 6 insertions(+), 16 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index ef57d186c16ffb..85ef579df44fdd 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -313,7 +313,7 @@ lemma spanRank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] N simpa using lift_spanRank_map_eq_of_injective f hf p lemma spanFinrank_map_eq_of_injective [RingHomSurjective σ] (f : M →ₛₗ[σ] L) - (hf : Function.Injective f) {p : Submodule R M} (hp : p.FG) : + (hf : Function.Injective f) {p : Submodule R M} : (p.map f).spanFinrank = p.spanFinrank := by rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v}, ← Cardinal.toNat_lift.{v, u}, lift_spanRank_map_eq_of_injective f hf p] @@ -389,7 +389,7 @@ lemma Ideal.spanFinrank_map_le_of_fg (f : R →+* T) {I : Ideal R} (hI : I.FG) : ← Cardinal.lift_natCast.{v}, ← Submodule.FG.spanRank_eq_spanFinrank hI] exact I.lift_spanRank_map_le f -lemma Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv (f : R ≃+* T) {I : Ideal R} : +lemma Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv (f : R ≃+* T) (I : Ideal R) : (I.map f).spanFinrank = I.spanFinrank := by rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v}, ← Cardinal.toNat_lift.{v, u}, I.lift_spanRank_map_eq_of_ringEquiv f] diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index cb2045a8d5115e..80c6bcc3ed08c2 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -374,20 +374,10 @@ lemma spanFinrank_le_of_surjective (fg : (maximalIdeal R).FG) {R' : Type*} [Comm lemma spanFinrank_eq_of_ringEquiv {R' : Type*} [CommRing R'] [IsLocalRing R'] (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := by - by_cases fgR : (maximalIdeal R).FG - · have eqmap : maximalIdeal R' = (maximalIdeal R).map e := by - rw [← Ideal.comap_symm, eq_comm] - exact (((local_hom_TFAE _).out 0 4).mp (e.symm.surjective.isLocalHom (e.symm : R' →+* R))) - refine le_antisymm (spanFinrank_le_of_surjective ?_ e.symm.toRingHom e.symm.surjective) - (spanFinrank_le_of_surjective fgR e.toRingHom e.surjective) - simpa only [eqmap] using fgR.map e.toRingHom - · by_cases fgR' : (maximalIdeal R').FG - · have eqmap' : maximalIdeal R = (maximalIdeal R').map e.symm := by - rw [Ideal.map_symm, eq_comm] - exact ((local_hom_TFAE _).out 0 4).mp (e.surjective.isLocalHom (e : R →+* R')) - absurd fgR - simpa only [eqmap'] using fgR'.map e.symm.toRingHom - · rw [Submodule.spanFinrank_of_not_fg fgR, Submodule.spanFinrank_of_not_fg fgR'] + have eqmap : maximalIdeal R = (maximalIdeal R').map e.symm := by + rw [Ideal.map_symm, eq_comm] + exact ((local_hom_TFAE _).out 0 4).mp (e.surjective.isLocalHom (e : R →+* R')) + rw [eqmap, Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv] end spanRank From f3b46bd2d102547f23be2f523f6ff0b2541e42a2 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 13 Mar 2026 16:58:30 +0800 Subject: [PATCH 42/64] add base change version i.e. apply Andrew's suggestions --- Mathlib/Algebra/Module/SpanRank.lean | 3 + Mathlib/RingTheory/Ideal/Cotangent.lean | 73 +++++++++++++++++-------- 2 files changed, 52 insertions(+), 24 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 85ef579df44fdd..157055aeef4fd3 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -326,6 +326,9 @@ lemma spanRank_range_le [RingHomSurjective σ] (f : M →ₛₗ[σ] N) : lemma spanRank_top (p : Submodule R M) : (⊤ : Submodule R p).spanRank = p.spanRank := by simpa using (spanRank_map_eq_of_injective _ p.subtype_injective ⊤).symm +lemma spanFinrank_top (p : Submodule R M) : (⊤ : Submodule R p).spanFinrank = p.spanFinrank := by + simp [Submodule.spanFinrank] + lemma spanRank_eq_of_equiv {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] N) : (⊤ : Submodule R M).spanRank = (⊤ : Submodule S N).spanRank := by diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 80c6bcc3ed08c2..6711e407bda353 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -327,34 +327,61 @@ theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] : Submodule.map_top, range_subtype, eq_comm (a := maximalIdeal R)] exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩ +end IsLocalRing + section spanRank -open IsLocalRing +open IsLocalRing TensorProduct Submodule + +variable {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] + {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M) + +lemma TensorProduct.spanRank_baseChange_le : (N.baseChange A).spanRank ≤ N.spanRank.lift := by + obtain ⟨s, hs₁, hs₂⟩ := N.exists_span_set_card_eq_spanRank + grw [← hs₁, ← hs₂, baseChange_span, spanRank_span_le_card] + convert Cardinal.mk_image_le_lift (f := TensorProduct.mk R A M 1) (s := s) + · exact (Cardinal.lift_id' _).symm + · exact Cardinal.lift_umax.symm + +lemma TensorProduct.spanRank_top_le : (⊤ : Submodule A (A ⊗[R] N)).spanRank ≤ N.spanRank.lift := by + grw [← Submodule.baseChange_top, ← N.spanRank_top, spanRank_baseChange_le] + +lemma TensorProduct.spanFinrank_top_le (fg : N.FG) : + (⊤ : Submodule A (A ⊗[R] N)).spanFinrank ≤ N.spanFinrank := by + grw [spanFinrank, spanRank_top_le, Cardinal.toNat_lift, spanFinrank] + simp [Cardinal.lift_lt_aleph0, spanRank_finite_iff_fg.mpr fg] + +variable [IsLocalRing R] +local notation "𝓀" => ResidueField R +set_option backward.isDefEq.respectTransparency false in +lemma TensorProduct.spanFinrank_top_eq_of_residueField (fg : N.FG) : + (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).spanFinrank = N.spanFinrank := by + let : Module.Finite R N := Module.Finite.iff_fg.mpr fg + apply (TensorProduct.spanFinrank_top_le N fg).antisymm + obtain ⟨s, hs₁, hs₂⟩ := (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).exists_span_set_card_eq_spanRank + have hs₃ : s.Finite := Cardinal.mk_lt_aleph0_iff.mp (by simpa [hs₁] using Module.Finite.fg_top) + let t := Function.surjInv (mk_surjective R N 𝓀 residue_surjective) '' s + have ht₁ : mk R 𝓀 N 1 '' t = s := by rw [← Set.image_comp, Function.comp_surjInv, s.image_id] + have ht₂ : span R t = ⊤ := by + rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective), + ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂ + grw [← N.spanFinrank_top, ← ht₂, spanFinrank_span_le_ncard_of_finite (hs₃.image _), spanFinrank, + ← hs₁, Set.ncard_image_le hs₃] + rfl + +set_option backward.isDefEq.respectTransparency false in lemma spanFinrank_eq_finrank_quotient {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M) (fg : N.FG) : N.spanFinrank = Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by - let : Field (R ⧸ maximalIdeal R) := Ideal.Quotient.field (maximalIdeal R) - let fin : Module.Finite R N := Module.Finite.iff_fg.mpr fg - let mN := (maximalIdeal R) • (⊤ : Submodule R N) - have : (⊤ : Submodule R N).spanFinrank = N.spanFinrank := by simp [Submodule.spanFinrank] - rw [Module.finrank_eq_spanFinrank_of_free, ← this] - apply le_antisymm - · let s : Set (N ⧸ mN) := (⊤ : Submodule (R ⧸ maximalIdeal R) (N ⧸ mN)).generators - have fins : s.Finite := Module.Finite.fg_top.finite_generators - let t := Function.surjInv (Submodule.mkQ_surjective mN) '' s - have : Submodule.mkQ mN '' t = s := by rw [← s.image_comp, Function.comp_surjInv, s.image_id] - have eqtop : Submodule.span R t = ⊤ := by - rw [← IsLocalRing.map_mkQ_eq_top, Submodule.map_span, this, ← Submodule.coe_eq_univ, - ← Submodule.coe_span_eq_span_of_surjective R (R ⧸ maximalIdeal R) - Ideal.Quotient.mk_surjective, Submodule.coe_eq_univ, Submodule.span_generators _] - simp only [← eqtop, t] - grw [Submodule.spanFinrank_span_le_ncard_of_finite (fins.image _), Set.ncard_image_le fins, - Module.Finite.fg_top.generators_ncard] - · let f : N →ₛₗ[Ideal.Quotient.mk (maximalIdeal R)] (N ⧸ mN) := { __ := Submodule.mkQ _ } - convert Submodule.spanFinrank_map_le_of_fg f fin.1 - symm - simpa [f, LinearMap.range_eq_top] using Submodule.mkQ_surjective _ + let : Module 𝓀 (↥N ⧸ maximalIdeal R • (⊤ : Submodule R N)) := + inferInstanceAs (Module (R ⧸ maximalIdeal R) _) + let : IsScalarTower R 𝓀 (N ⧸ maximalIdeal R • (⊤ : Submodule R N)) := + inferInstanceAs (IsScalarTower R (R ⧸ maximalIdeal R) _) + rw [← spanFinrank_top_eq_of_residueField N fg, ← Module.finrank_eq_spanFinrank_of_free] + let e : 𝓀 ⊗[R] N ≃ₗ[𝓀] N ⧸ (maximalIdeal R) • (⊤ : Submodule R N) := + (quotTensorEquivQuotSMul N (maximalIdeal R)).extendScalarsOfSurjective residue_surjective + exact e.finrank_eq lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (fg : (maximalIdeal R).FG) : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := @@ -380,5 +407,3 @@ lemma spanFinrank_eq_of_ringEquiv {R' : Type*} [CommRing R'] [IsLocalRing R'] (e rw [eqmap, Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv] end spanRank - -end IsLocalRing From ca5786a3a6ef32a14f8037088801a77ffa82c0c0 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sun, 15 Mar 2026 11:35:26 +0800 Subject: [PATCH 43/64] fix variable --- Mathlib/Algebra/Module/SpanRank.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 9638f0689289d6..a38343231f73a2 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -292,8 +292,8 @@ lemma spanRank_map_le [RingHomSurjective σ] (f : M →ₛₗ[σ] N) (p : Submod (p.map f).spanRank ≤ p.spanRank := by simpa using lift_spanRank_map_le f p -lemma spanFinrank_map_le_of_fg {L : Type v} [AddCommMonoid L] [Module S L] [RingHomSurjective σ] - (f : M →ₛₗ[σ] L) {p : Submodule R M} (hp : p.FG) : (p.map f).spanFinrank ≤ p.spanFinrank := by +lemma spanFinrank_map_le_of_fg [RingHomSurjective σ] (f : M →ₛₗ[σ] L) {p : Submodule R M} + (hp : p.FG) : (p.map f).spanFinrank ≤ p.spanFinrank := by rw [← (hp.map f).spanRank_le_iff, ← Cardinal.lift_le.{u}, Cardinal.lift_natCast, ← Cardinal.lift_natCast.{v}, ← hp.spanRank_eq_spanFinrank] exact p.lift_spanRank_map_le f From cd54a0944d86f4ae6aca6ece376da753eb6bede8 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sun, 15 Mar 2026 11:38:50 +0800 Subject: [PATCH 44/64] fix naming and add spanFinrank version --- Mathlib/RingTheory/Ideal/Cotangent.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 6711e407bda353..1e2f5c10fb77b2 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -336,13 +336,18 @@ open IsLocalRing TensorProduct Submodule variable {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M) -lemma TensorProduct.spanRank_baseChange_le : (N.baseChange A).spanRank ≤ N.spanRank.lift := by +lemma Submodule.spanRank_baseChange_le : (N.baseChange A).spanRank ≤ N.spanRank.lift := by obtain ⟨s, hs₁, hs₂⟩ := N.exists_span_set_card_eq_spanRank grw [← hs₁, ← hs₂, baseChange_span, spanRank_span_le_card] convert Cardinal.mk_image_le_lift (f := TensorProduct.mk R A M 1) (s := s) · exact (Cardinal.lift_id' _).symm · exact Cardinal.lift_umax.symm +lemma Submodule.spanFinrank_baseChange_le (fg : N.FG) : + (N.baseChange A).spanFinrank ≤ N.spanFinrank := by + grw [spanFinrank, spanRank_baseChange_le, Cardinal.toNat_lift, spanFinrank] + simp [Cardinal.lift_lt_aleph0, spanRank_finite_iff_fg.mpr fg] + lemma TensorProduct.spanRank_top_le : (⊤ : Submodule A (A ⊗[R] N)).spanRank ≤ N.spanRank.lift := by grw [← Submodule.baseChange_top, ← N.spanRank_top, spanRank_baseChange_le] From eea67d8f03aa77b5025bf2d80d52f3a761c33595 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sun, 15 Mar 2026 12:18:50 +0800 Subject: [PATCH 45/64] add lemma and golf --- Mathlib/RingTheory/Ideal/Cotangent.lean | 5 +---- Mathlib/RingTheory/LocalRing/RingHom/Basic.lean | 12 ++++++++++++ 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 1e2f5c10fb77b2..22818a38a972fd 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -406,9 +406,6 @@ lemma spanFinrank_le_of_surjective (fg : (maximalIdeal R).FG) {R' : Type*} [Comm lemma spanFinrank_eq_of_ringEquiv {R' : Type*} [CommRing R'] [IsLocalRing R'] (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := by - have eqmap : maximalIdeal R = (maximalIdeal R').map e.symm := by - rw [Ideal.map_symm, eq_comm] - exact ((local_hom_TFAE _).out 0 4).mp (e.surjective.isLocalHom (e : R →+* R')) - rw [eqmap, Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv] + rw [maximalIdeal_eq_map_ringEquiv e, Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv] end spanRank diff --git a/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean b/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean index 3fe5b123aca1fb..e530772ddf0229 100644 --- a/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean +++ b/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean @@ -93,6 +93,9 @@ theorem local_hom_TFAE (f : R →+* S) : tfae_have 5 → 4 := fun h ↦ le_of_eq h.symm tfae_finish +lemma maximalIdeal_comap (f : R →+* S) [IsLocalHom f] : (maximalIdeal S).comap f = maximalIdeal R := + ((local_hom_TFAE _).out 0 4).mp ‹_› + end theorem of_surjective [CommSemiring R] [IsLocalRing R] [Semiring S] [Nontrivial S] (f : R →+* S) @@ -133,6 +136,15 @@ instance (priority := 100) {K R} [DivisionRing K] [CommRing R] [Nontrivial R] (f : K →+* R) : IsLocalHom f where map_nonunit r hr := by simpa only [isUnit_iff_ne_zero, ne_eq, map_eq_zero] using hr.ne_zero +lemma maximalIdeal_eq_map_of_surjective [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] + (f : R →+* S) (hf : Function.Surjective f) : maximalIdeal S = (maximalIdeal R).map f := by + let := IsLocalHom.of_surjective f hf + rw [← maximalIdeal_comap f, Ideal.map_comap_of_surjective f hf] + +lemma maximalIdeal_eq_map_ringEquiv [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] + (e : R ≃+* S) : maximalIdeal S = (maximalIdeal R).map e := + maximalIdeal_eq_map_of_surjective (e : R →+* S) e.surjective + end IsLocalRing namespace RingEquiv From 6c5947739ea620b158cab68ec5da510d19de4500 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 16 Mar 2026 21:32:44 +0800 Subject: [PATCH 46/64] golf maximal ideal map --- Mathlib/RingTheory/Ideal/Cotangent.lean | 6 ++---- Mathlib/RingTheory/LocalRing/RingHom/Basic.lean | 11 ++++++----- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 22818a38a972fd..e6fc8b907281ed 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -400,12 +400,10 @@ lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : lemma spanFinrank_le_of_surjective (fg : (maximalIdeal R).FG) {R' : Type*} [CommRing R'] [IsLocalRing R'] (f : R →+* R') (surj : Function.Surjective f) : (maximalIdeal R').spanFinrank ≤ (maximalIdeal R).spanFinrank := by - have comapeq := ((local_hom_TFAE f).out 0 4).mp (surj.isLocalHom f) - rw [← Ideal.map_comap_of_surjective f surj (maximalIdeal R'), comapeq] - exact (maximalIdeal R).spanFinrank_map_le_of_fg f fg + grw [← map_maximalIdeal_of_surjective f surj, (maximalIdeal R).spanFinrank_map_le_of_fg f fg] lemma spanFinrank_eq_of_ringEquiv {R' : Type*} [CommRing R'] [IsLocalRing R'] (e : R ≃+* R') : (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := by - rw [maximalIdeal_eq_map_ringEquiv e, Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv] + rw [← map_ringEquiv_maximalIdeal e, Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv] end spanRank diff --git a/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean b/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean index e530772ddf0229..15c4193e4dad8f 100644 --- a/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean +++ b/Mathlib/RingTheory/LocalRing/RingHom/Basic.lean @@ -136,14 +136,15 @@ instance (priority := 100) {K R} [DivisionRing K] [CommRing R] [Nontrivial R] (f : K →+* R) : IsLocalHom f where map_nonunit r hr := by simpa only [isUnit_iff_ne_zero, ne_eq, map_eq_zero] using hr.ne_zero -lemma maximalIdeal_eq_map_of_surjective [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] - (f : R →+* S) (hf : Function.Surjective f) : maximalIdeal S = (maximalIdeal R).map f := by +lemma map_maximalIdeal_of_surjective [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] + (f : R →+* S) (hf : Function.Surjective f) : (maximalIdeal R).map f = maximalIdeal S := by let := IsLocalHom.of_surjective f hf rw [← maximalIdeal_comap f, Ideal.map_comap_of_surjective f hf] -lemma maximalIdeal_eq_map_ringEquiv [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] - (e : R ≃+* S) : maximalIdeal S = (maximalIdeal R).map e := - maximalIdeal_eq_map_of_surjective (e : R →+* S) e.surjective +@[simp] +lemma map_ringEquiv_maximalIdeal [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] + (e : R ≃+* S) : (maximalIdeal R).map e = maximalIdeal S := + map_maximalIdeal_of_surjective (e : R →+* S) e.surjective end IsLocalRing From 435a579c93fcff7767b83dc5965ac50b6a01cfc7 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 16 Mar 2026 21:33:03 +0800 Subject: [PATCH 47/64] remove lemma easy enough --- Mathlib/RingTheory/Ideal/Cotangent.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index e6fc8b907281ed..55f55b0ae1c7d3 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -397,13 +397,4 @@ lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (maximalIdeal R).fg_of_isNoetherianRing -lemma spanFinrank_le_of_surjective (fg : (maximalIdeal R).FG) {R' : Type*} [CommRing R'] - [IsLocalRing R'] (f : R →+* R') (surj : Function.Surjective f) : - (maximalIdeal R').spanFinrank ≤ (maximalIdeal R).spanFinrank := by - grw [← map_maximalIdeal_of_surjective f surj, (maximalIdeal R).spanFinrank_map_le_of_fg f fg] - -lemma spanFinrank_eq_of_ringEquiv {R' : Type*} [CommRing R'] [IsLocalRing R'] (e : R ≃+* R') : - (maximalIdeal R).spanFinrank = (maximalIdeal R').spanFinrank := by - rw [← map_ringEquiv_maximalIdeal e, Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv] - end spanRank From 163291a8752a67fa0d6187107345fa3ecd01d81e Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 16 Mar 2026 21:41:16 +0800 Subject: [PATCH 48/64] golf base change --- Mathlib/RingTheory/Ideal/Cotangent.lean | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 55f55b0ae1c7d3..9746c8a8758c36 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -343,7 +343,7 @@ lemma Submodule.spanRank_baseChange_le : (N.baseChange A).spanRank ≤ N.spanRan · exact (Cardinal.lift_id' _).symm · exact Cardinal.lift_umax.symm -lemma Submodule.spanFinrank_baseChange_le (fg : N.FG) : +lemma Submodule.FG.spanFinrank_baseChange_le (fg : N.FG) : (N.baseChange A).spanFinrank ≤ N.spanFinrank := by grw [spanFinrank, spanRank_baseChange_le, Cardinal.toNat_lift, spanFinrank] simp [Cardinal.lift_lt_aleph0, spanRank_finite_iff_fg.mpr fg] @@ -351,10 +351,9 @@ lemma Submodule.spanFinrank_baseChange_le (fg : N.FG) : lemma TensorProduct.spanRank_top_le : (⊤ : Submodule A (A ⊗[R] N)).spanRank ≤ N.spanRank.lift := by grw [← Submodule.baseChange_top, ← N.spanRank_top, spanRank_baseChange_le] -lemma TensorProduct.spanFinrank_top_le (fg : N.FG) : +lemma TensorProduct.spanFinrank_top_le_of_fg (fg : N.FG) : (⊤ : Submodule A (A ⊗[R] N)).spanFinrank ≤ N.spanFinrank := by - grw [spanFinrank, spanRank_top_le, Cardinal.toNat_lift, spanFinrank] - simp [Cardinal.lift_lt_aleph0, spanRank_finite_iff_fg.mpr fg] + grw [← Submodule.baseChange_top, ← N.spanFinrank_top, (N.fg_top.mpr fg).spanFinrank_baseChange_le] variable [IsLocalRing R] local notation "𝓀" => ResidueField R @@ -363,7 +362,7 @@ set_option backward.isDefEq.respectTransparency false in lemma TensorProduct.spanFinrank_top_eq_of_residueField (fg : N.FG) : (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).spanFinrank = N.spanFinrank := by let : Module.Finite R N := Module.Finite.iff_fg.mpr fg - apply (TensorProduct.spanFinrank_top_le N fg).antisymm + apply (TensorProduct.spanFinrank_top_le_of_fg N fg).antisymm obtain ⟨s, hs₁, hs₂⟩ := (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).exists_span_set_card_eq_spanRank have hs₃ : s.Finite := Cardinal.mk_lt_aleph0_iff.mp (by simpa [hs₁] using Module.Finite.fg_top) let t := Function.surjInv (mk_surjective R N 𝓀 residue_surjective) '' s @@ -377,9 +376,10 @@ lemma TensorProduct.spanFinrank_top_eq_of_residueField (fg : N.FG) : set_option backward.isDefEq.respectTransparency false in lemma spanFinrank_eq_finrank_quotient {M : Type*} [AddCommGroup M] [Module R M] - (N : Submodule R M) (fg : N.FG) : N.spanFinrank = - Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by - let : Module 𝓀 (↥N ⧸ maximalIdeal R • (⊤ : Submodule R N)) := + (N : Submodule R M) (fg : N.FG) : + N.spanFinrank = + Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by + let : Module 𝓀 (N ⧸ maximalIdeal R • (⊤ : Submodule R N)) := inferInstanceAs (Module (R ⧸ maximalIdeal R) _) let : IsScalarTower R 𝓀 (N ⧸ maximalIdeal R • (⊤ : Submodule R N)) := inferInstanceAs (IsScalarTower R (R ⧸ maximalIdeal R) _) @@ -388,6 +388,8 @@ lemma spanFinrank_eq_finrank_quotient {M : Type*} [AddCommGroup M] [Module R M] (quotTensorEquivQuotSMul N (maximalIdeal R)).extendScalarsOfSurjective residue_surjective exact e.finrank_eq +namespace IsLocalRing + lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (fg : (maximalIdeal R).FG) : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := spanFinrank_eq_finrank_quotient _ fg @@ -397,4 +399,6 @@ lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (maximalIdeal R).fg_of_isNoetherianRing +end IsLocalRing + end spanRank From 379c4abb8d9d8c1bd0e1ae7f2b6e8710df17fac7 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 16 Mar 2026 21:43:03 +0800 Subject: [PATCH 49/64] golf --- Mathlib/Algebra/Module/SpanRank.lean | 2 +- Mathlib/RingTheory/Ideal/Cotangent.lean | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index a38343231f73a2..8da5e5eb0144ea 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -392,7 +392,7 @@ lemma Ideal.spanFinrank_map_le_of_fg (f : R →+* T) {I : Ideal R} (hI : I.FG) : ← Cardinal.lift_natCast.{v}, ← Submodule.FG.spanRank_eq_spanFinrank hI] exact I.lift_spanRank_map_le f -lemma Ideal.spanFinrank_map_eq_of_fg_of_ringEquiv (f : R ≃+* T) (I : Ideal R) : +lemma Ideal.spanFinrank_map_eq_of_ringEquiv (f : R ≃+* T) (I : Ideal R) : (I.map f).spanFinrank = I.spanFinrank := by rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v}, ← Cardinal.toNat_lift.{v, u}, I.lift_spanRank_map_eq_of_ringEquiv f] diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 9746c8a8758c36..4c946d0afee895 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -375,8 +375,7 @@ lemma TensorProduct.spanFinrank_top_eq_of_residueField (fg : N.FG) : rfl set_option backward.isDefEq.respectTransparency false in -lemma spanFinrank_eq_finrank_quotient {M : Type*} [AddCommGroup M] [Module R M] - (N : Submodule R M) (fg : N.FG) : +lemma spanFinrank_eq_finrank_quotient (N : Submodule R M) (fg : N.FG) : N.spanFinrank = Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by let : Module 𝓀 (N ⧸ maximalIdeal R • (⊤ : Submodule R N)) := From 0e42b015810986e85cdbd2f86d15c1c8aedfaef4 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 16 Mar 2026 21:47:19 +0800 Subject: [PATCH 50/64] fix --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index 37d99ed0c93f46..b6c58da28e1b18 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -56,8 +56,8 @@ lemma of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R'] (e : R ≃+* R') : IsRegularLocalRing R' := by let _ := e.isLocalRing let _ := isNoetherianRing_of_ringEquiv R e - rw [isRegularLocalRing_def, ← spanFinrank_eq_of_ringEquiv e, ← ringKrullDim_eq_of_ringEquiv e] - exact (isRegularLocalRing_def R).mp ‹_› + rwa [isRegularLocalRing_def, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e, + Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_def] lemma iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by From ce937dfe15f2e1c999b590cb86836e5b80dc1b66 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Wed, 18 Mar 2026 11:26:17 +0800 Subject: [PATCH 51/64] add simp attr --- Mathlib/Algebra/Module/SpanRank.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index 8da5e5eb0144ea..03c925cae93464 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -382,6 +382,7 @@ lemma Ideal.lift_spanRank_map_eq_of_ringEquiv (f : R ≃+* T) (I : Ideal R) : lemma Ideal.spanRank_map_le (f : R →+* S) (I : Ideal R) : (I.map f).spanRank ≤ I.spanRank := by simpa using I.lift_spanRank_map_le f +@[simp] lemma Ideal.spanRank_map_eq_of_ringEquiv (f : R ≃+* S) (I : Ideal R) : (I.map f).spanRank = I.spanRank := by simpa using I.lift_spanRank_map_eq_of_ringEquiv f @@ -392,6 +393,7 @@ lemma Ideal.spanFinrank_map_le_of_fg (f : R →+* T) {I : Ideal R} (hI : I.FG) : ← Cardinal.lift_natCast.{v}, ← Submodule.FG.spanRank_eq_spanFinrank hI] exact I.lift_spanRank_map_le f +@[simp] lemma Ideal.spanFinrank_map_eq_of_ringEquiv (f : R ≃+* T) (I : Ideal R) : (I.map f).spanFinrank = I.spanFinrank := by rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v}, From 201acfd2924b798efcc10d6d3a99f1239b40e2ee Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 19 Mar 2026 15:26:36 +0800 Subject: [PATCH 52/64] split file --- .../Algebra/Module/SpanRankOperations.lean | 83 +++++++++++++++++++ Mathlib/RingTheory/Ideal/Cotangent.lean | 68 +-------------- 2 files changed, 86 insertions(+), 65 deletions(-) create mode 100644 Mathlib/Algebra/Module/SpanRankOperations.lean diff --git a/Mathlib/Algebra/Module/SpanRankOperations.lean b/Mathlib/Algebra/Module/SpanRankOperations.lean new file mode 100644 index 00000000000000..27ab6bf851bc58 --- /dev/null +++ b/Mathlib/Algebra/Module/SpanRankOperations.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2026 Nailin Guan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nailin Guan +-/ +module + +public import Mathlib.Algebra.Module.SpanRank +public import Mathlib.RingTheory.LocalRing.Module + +/-! +# Span rank under operations + +In this file, we mainly proof that base change doesn't increase span rank and +for finitely generated module over local ring the dimension of base change by +residue field is exactly its span rank. + +# Main Results + +* `Submodule.spanRank_baseChange_le` : base change doesn't increase span rank. + +* `TensorProduct.spanFinrank_top_eq_of_residueField` : for finitely generated module over + local ring, dimension of base change by residue field is equal to its span rank. + +-/ + +@[expose] public section + +open IsLocalRing TensorProduct Submodule + +variable {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] + {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M) + +lemma Submodule.spanRank_baseChange_le : (N.baseChange A).spanRank ≤ N.spanRank.lift := by + obtain ⟨s, hs₁, hs₂⟩ := N.exists_span_set_card_eq_spanRank + grw [← hs₁, ← hs₂, baseChange_span, spanRank_span_le_card] + convert Cardinal.mk_image_le_lift (f := TensorProduct.mk R A M 1) (s := s) + · exact (Cardinal.lift_id' _).symm + · exact Cardinal.lift_umax.symm + +lemma Submodule.FG.spanFinrank_baseChange_le (fg : N.FG) : + (N.baseChange A).spanFinrank ≤ N.spanFinrank := by + grw [spanFinrank, spanRank_baseChange_le, Cardinal.toNat_lift, spanFinrank] + simp [Cardinal.lift_lt_aleph0, spanRank_finite_iff_fg.mpr fg] + +lemma TensorProduct.spanRank_top_le : (⊤ : Submodule A (A ⊗[R] N)).spanRank ≤ N.spanRank.lift := by + grw [← Submodule.baseChange_top, ← N.spanRank_top, spanRank_baseChange_le] + +lemma TensorProduct.spanFinrank_top_le_of_fg (fg : N.FG) : + (⊤ : Submodule A (A ⊗[R] N)).spanFinrank ≤ N.spanFinrank := by + grw [← Submodule.baseChange_top, ← N.spanFinrank_top, (N.fg_top.mpr fg).spanFinrank_baseChange_le] + +variable [IsLocalRing R] +local notation "𝓀" => ResidueField R + +set_option backward.isDefEq.respectTransparency false in +lemma TensorProduct.spanFinrank_top_eq_of_residueField (fg : N.FG) : + (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).spanFinrank = N.spanFinrank := by + let : Module.Finite R N := Module.Finite.iff_fg.mpr fg + apply (TensorProduct.spanFinrank_top_le_of_fg N fg).antisymm + obtain ⟨s, hs₁, hs₂⟩ := (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).exists_span_set_card_eq_spanRank + have hs₃ : s.Finite := Cardinal.mk_lt_aleph0_iff.mp (by simpa [hs₁] using Module.Finite.fg_top) + let t := Function.surjInv (mk_surjective R N 𝓀 residue_surjective) '' s + have ht₁ : mk R 𝓀 N 1 '' t = s := by rw [← Set.image_comp, Function.comp_surjInv, s.image_id] + have ht₂ : span R t = ⊤ := by + rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective), + ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂ + grw [← N.spanFinrank_top, ← ht₂, spanFinrank_span_le_ncard_of_finite (hs₃.image _), spanFinrank, + ← hs₁, Set.ncard_image_le hs₃] + rfl + +set_option backward.isDefEq.respectTransparency false in +lemma spanFinrank_eq_finrank_quotient (N : Submodule R M) (fg : N.FG) : + N.spanFinrank = + Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by + let : Module 𝓀 (N ⧸ maximalIdeal R • (⊤ : Submodule R N)) := + inferInstanceAs (Module (R ⧸ maximalIdeal R) _) + let : IsScalarTower R 𝓀 (N ⧸ maximalIdeal R • (⊤ : Submodule R N)) := + inferInstanceAs (IsScalarTower R (R ⧸ maximalIdeal R) _) + rw [← spanFinrank_top_eq_of_residueField N fg, ← Module.finrank_eq_spanFinrank_of_free] + let e : 𝓀 ⊗[R] N ≃ₗ[𝓀] N ⧸ (maximalIdeal R) • (⊤ : Submodule R N) := + (quotTensorEquivQuotSMul N (maximalIdeal R)).extendScalarsOfSurjective residue_surjective + exact e.finrank_eq diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 4c946d0afee895..cdc64cefaab158 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -5,16 +5,8 @@ Authors: Andrew Yang -/ module -public import Mathlib.Algebra.Module.Torsion.Basic -public import Mathlib.Algebra.Module.SpanRank -public import Mathlib.Algebra.Ring.Idempotent -public import Mathlib.LinearAlgebra.Dimension.Finite -public import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition -public import Mathlib.LinearAlgebra.FiniteDimensional.Defs +public import Mathlib.Algebra.Module.SpanRankOperations public import Mathlib.RingTheory.Filtration -public import Mathlib.RingTheory.Ideal.Operations -public import Mathlib.RingTheory.LocalRing.Module -public import Mathlib.RingTheory.LocalRing.ResidueField.Basic /-! # The module `I ⧸ I ^ 2` @@ -331,64 +323,10 @@ end IsLocalRing section spanRank -open IsLocalRing TensorProduct Submodule - -variable {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] - {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M) - -lemma Submodule.spanRank_baseChange_le : (N.baseChange A).spanRank ≤ N.spanRank.lift := by - obtain ⟨s, hs₁, hs₂⟩ := N.exists_span_set_card_eq_spanRank - grw [← hs₁, ← hs₂, baseChange_span, spanRank_span_le_card] - convert Cardinal.mk_image_le_lift (f := TensorProduct.mk R A M 1) (s := s) - · exact (Cardinal.lift_id' _).symm - · exact Cardinal.lift_umax.symm - -lemma Submodule.FG.spanFinrank_baseChange_le (fg : N.FG) : - (N.baseChange A).spanFinrank ≤ N.spanFinrank := by - grw [spanFinrank, spanRank_baseChange_le, Cardinal.toNat_lift, spanFinrank] - simp [Cardinal.lift_lt_aleph0, spanRank_finite_iff_fg.mpr fg] - -lemma TensorProduct.spanRank_top_le : (⊤ : Submodule A (A ⊗[R] N)).spanRank ≤ N.spanRank.lift := by - grw [← Submodule.baseChange_top, ← N.spanRank_top, spanRank_baseChange_le] - -lemma TensorProduct.spanFinrank_top_le_of_fg (fg : N.FG) : - (⊤ : Submodule A (A ⊗[R] N)).spanFinrank ≤ N.spanFinrank := by - grw [← Submodule.baseChange_top, ← N.spanFinrank_top, (N.fg_top.mpr fg).spanFinrank_baseChange_le] - -variable [IsLocalRing R] -local notation "𝓀" => ResidueField R - -set_option backward.isDefEq.respectTransparency false in -lemma TensorProduct.spanFinrank_top_eq_of_residueField (fg : N.FG) : - (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).spanFinrank = N.spanFinrank := by - let : Module.Finite R N := Module.Finite.iff_fg.mpr fg - apply (TensorProduct.spanFinrank_top_le_of_fg N fg).antisymm - obtain ⟨s, hs₁, hs₂⟩ := (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).exists_span_set_card_eq_spanRank - have hs₃ : s.Finite := Cardinal.mk_lt_aleph0_iff.mp (by simpa [hs₁] using Module.Finite.fg_top) - let t := Function.surjInv (mk_surjective R N 𝓀 residue_surjective) '' s - have ht₁ : mk R 𝓀 N 1 '' t = s := by rw [← Set.image_comp, Function.comp_surjInv, s.image_id] - have ht₂ : span R t = ⊤ := by - rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective), - ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂ - grw [← N.spanFinrank_top, ← ht₂, spanFinrank_span_le_ncard_of_finite (hs₃.image _), spanFinrank, - ← hs₁, Set.ncard_image_le hs₃] - rfl - -set_option backward.isDefEq.respectTransparency false in -lemma spanFinrank_eq_finrank_quotient (N : Submodule R M) (fg : N.FG) : - N.spanFinrank = - Module.finrank (R ⧸ maximalIdeal R) (N ⧸ (maximalIdeal R) • (⊤ : Submodule R N)) := by - let : Module 𝓀 (N ⧸ maximalIdeal R • (⊤ : Submodule R N)) := - inferInstanceAs (Module (R ⧸ maximalIdeal R) _) - let : IsScalarTower R 𝓀 (N ⧸ maximalIdeal R • (⊤ : Submodule R N)) := - inferInstanceAs (IsScalarTower R (R ⧸ maximalIdeal R) _) - rw [← spanFinrank_top_eq_of_residueField N fg, ← Module.finrank_eq_spanFinrank_of_free] - let e : 𝓀 ⊗[R] N ≃ₗ[𝓀] N ⧸ (maximalIdeal R) • (⊤ : Submodule R N) := - (quotTensorEquivQuotSMul N (maximalIdeal R)).extendScalarsOfSurjective residue_surjective - exact e.finrank_eq - namespace IsLocalRing +variable {R : Type*} [CommRing R] [IsLocalRing R] + lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (fg : (maximalIdeal R).FG) : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := spanFinrank_eq_finrank_quotient _ fg From cd6c4d07a80a7dbd0607f8c60e046d6a1e43e3d2 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 19 Mar 2026 15:27:26 +0800 Subject: [PATCH 53/64] Update Mathlib.lean --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index b7894cd901b742..b90e24a92acc93 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -790,6 +790,7 @@ public import Mathlib.Algebra.Module.RingHom public import Mathlib.Algebra.Module.Shrink public import Mathlib.Algebra.Module.SnakeLemma public import Mathlib.Algebra.Module.SpanRank +public import Mathlib.Algebra.Module.SpanRankOperations public import Mathlib.Algebra.Module.Submodule.Basic public import Mathlib.Algebra.Module.Submodule.Bilinear public import Mathlib.Algebra.Module.Submodule.Defs From 01211a7f23cb19903caa52526341be0a671c38c6 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 19 Mar 2026 23:03:10 +0800 Subject: [PATCH 54/64] move decl --- .../Algebra/Module/SpanRankOperations.lean | 10 +++++++ Mathlib/RingTheory/Ideal/Cotangent.lean | 28 ++++++------------- 2 files changed, 18 insertions(+), 20 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRankOperations.lean b/Mathlib/Algebra/Module/SpanRankOperations.lean index 27ab6bf851bc58..be8393a2697cb6 100644 --- a/Mathlib/Algebra/Module/SpanRankOperations.lean +++ b/Mathlib/Algebra/Module/SpanRankOperations.lean @@ -6,6 +6,7 @@ Authors: Nailin Guan module public import Mathlib.Algebra.Module.SpanRank +public import Mathlib.RingTheory.Ideal.Cotangent public import Mathlib.RingTheory.LocalRing.Module /-! @@ -81,3 +82,12 @@ lemma spanFinrank_eq_finrank_quotient (N : Submodule R M) (fg : N.FG) : let e : 𝓀 ⊗[R] N ≃ₗ[𝓀] N ⧸ (maximalIdeal R) • (⊤ : Submodule R N) := (quotTensorEquivQuotSMul N (maximalIdeal R)).extendScalarsOfSurjective residue_surjective exact e.finrank_eq + +lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (fg : (maximalIdeal R).FG) : + (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := + spanFinrank_eq_finrank_quotient _ fg + +variable (R) in +lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : + (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := + spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (maximalIdeal R).fg_of_isNoetherianRing diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index cdc64cefaab158..73c4b7efc10e0b 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -5,8 +5,15 @@ Authors: Andrew Yang -/ module -public import Mathlib.Algebra.Module.SpanRankOperations +public import Mathlib.Algebra.Module.Torsion.Basic +public import Mathlib.Algebra.Ring.Idempotent +public import Mathlib.LinearAlgebra.Dimension.Finite +public import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition +public import Mathlib.LinearAlgebra.FiniteDimensional.Defs public import Mathlib.RingTheory.Filtration +public import Mathlib.RingTheory.Ideal.Operations +public import Mathlib.RingTheory.LocalRing.ResidueField.Basic +public import Mathlib.RingTheory.Nakayama /-! # The module `I ⧸ I ^ 2` @@ -320,22 +327,3 @@ theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] : exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩ end IsLocalRing - -section spanRank - -namespace IsLocalRing - -variable {R : Type*} [CommRing R] [IsLocalRing R] - -lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (fg : (maximalIdeal R).FG) : - (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := - spanFinrank_eq_finrank_quotient _ fg - -variable (R) in -lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : - (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := - spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (maximalIdeal R).fg_of_isNoetherianRing - -end IsLocalRing - -end spanRank From 6fc82589cfac5661e46cb3dd33e4ec65da16e47c Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 19 Mar 2026 23:09:20 +0800 Subject: [PATCH 55/64] fix import --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index b6c58da28e1b18..51b341e23f6347 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -5,8 +5,8 @@ Authors: Nailin Guan -/ module +public import Mathlib.Algebra.Module.SpanRankOperations public import Mathlib.RingTheory.DiscreteValuationRing.Basic -public import Mathlib.RingTheory.Ideal.Cotangent public import Mathlib.RingTheory.Ideal.KrullsHeightTheorem public import Mathlib.RingTheory.KrullDimension.Field public import Mathlib.RingTheory.KrullDimension.PID From 92364360ff417f29711fce83e789831a4b992c85 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 19 Mar 2026 23:51:15 +0800 Subject: [PATCH 56/64] add doc --- Mathlib/Algebra/Module/SpanRankOperations.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Algebra/Module/SpanRankOperations.lean b/Mathlib/Algebra/Module/SpanRankOperations.lean index be8393a2697cb6..9c0739971ddc22 100644 --- a/Mathlib/Algebra/Module/SpanRankOperations.lean +++ b/Mathlib/Algebra/Module/SpanRankOperations.lean @@ -23,6 +23,9 @@ residue field is exactly its span rank. * `TensorProduct.spanFinrank_top_eq_of_residueField` : for finitely generated module over local ring, dimension of base change by residue field is equal to its span rank. +* `spanFinrank_maximalIdeal_eq_finrank_cotangentSpace` : the minimal number of generators of + the unique maximal ideal is equal to the dimension of cotangent space + -/ @[expose] public section From 69c2bbd5079d539811d9d9326715c5de8880e827 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 20 Mar 2026 19:40:13 +0800 Subject: [PATCH 57/64] add namespace --- Mathlib/Algebra/Module/SpanRankOperations.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Algebra/Module/SpanRankOperations.lean b/Mathlib/Algebra/Module/SpanRankOperations.lean index 9c0739971ddc22..6f70ea70d5e31a 100644 --- a/Mathlib/Algebra/Module/SpanRankOperations.lean +++ b/Mathlib/Algebra/Module/SpanRankOperations.lean @@ -73,6 +73,8 @@ lemma TensorProduct.spanFinrank_top_eq_of_residueField (fg : N.FG) : ← hs₁, Set.ncard_image_le hs₃] rfl +namespace IsLocalRing + set_option backward.isDefEq.respectTransparency false in lemma spanFinrank_eq_finrank_quotient (N : Submodule R M) (fg : N.FG) : N.spanFinrank = @@ -94,3 +96,5 @@ variable (R) in lemma spanFinrank_maximalIdeal_eq_finrank_cotangentSpace [IsNoetherianRing R] : (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (maximalIdeal R).fg_of_isNoetherianRing + +end IsLocalRing From 0011ecfa19377e7524d17a8a2b8ce859b9ca6c4d Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 20 Mar 2026 19:44:43 +0800 Subject: [PATCH 58/64] fix doc --- Mathlib/Algebra/Module/SpanRankOperations.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRankOperations.lean b/Mathlib/Algebra/Module/SpanRankOperations.lean index 6f70ea70d5e31a..231c6b49c56b6f 100644 --- a/Mathlib/Algebra/Module/SpanRankOperations.lean +++ b/Mathlib/Algebra/Module/SpanRankOperations.lean @@ -12,9 +12,7 @@ public import Mathlib.RingTheory.LocalRing.Module /-! # Span rank under operations -In this file, we mainly proof that base change doesn't increase span rank and -for finitely generated module over local ring the dimension of base change by -residue field is exactly its span rank. +In this file we show how operations on submodules interact with `Submodule.spanRank`. # Main Results @@ -23,8 +21,8 @@ residue field is exactly its span rank. * `TensorProduct.spanFinrank_top_eq_of_residueField` : for finitely generated module over local ring, dimension of base change by residue field is equal to its span rank. -* `spanFinrank_maximalIdeal_eq_finrank_cotangentSpace` : the minimal number of generators of - the unique maximal ideal is equal to the dimension of cotangent space +* `IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace` : The minimal number of + generators of the unique maximal ideal is equal to the dimension of the cotangent space. -/ From bb90a750c2da5a72c387ee4ab414f49424e24254 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 20 Mar 2026 19:48:12 +0800 Subject: [PATCH 59/64] restore open change --- Mathlib/RingTheory/KrullDimension/Regular.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/KrullDimension/Regular.lean b/Mathlib/RingTheory/KrullDimension/Regular.lean index e6d3a6ddf83cd1..0dfaa849ab770d 100644 --- a/Mathlib/RingTheory/KrullDimension/Regular.lean +++ b/Mathlib/RingTheory/KrullDimension/Regular.lean @@ -23,13 +23,13 @@ public import Mathlib.RingTheory.Spectrum.Prime.LTSeries public section -open RingTheory Sequence IsLocalRing Ideal PrimeSpectrum Pointwise - namespace Module variable {R : Type*} [CommRing R] [IsNoetherianRing R] {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] +open RingTheory Sequence IsLocalRing Ideal PrimeSpectrum Pointwise + omit [IsNoetherianRing R] [Module.Finite R M] in lemma exists_ltSeries_support_isMaximal_last_of_ltSeries_support (q : LTSeries (support R M)) : ∃ p : LTSeries (support R M), q.length ≤ p.length ∧ p.last.1.1.IsMaximal := by From fd3d647ad6225cdec7fe251f10974a696b52aee0 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 20 Mar 2026 23:50:59 +0800 Subject: [PATCH 60/64] fix doc --- Mathlib/Algebra/Module/SpanRankOperations.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Module/SpanRankOperations.lean b/Mathlib/Algebra/Module/SpanRankOperations.lean index 231c6b49c56b6f..41d14eb62cb098 100644 --- a/Mathlib/Algebra/Module/SpanRankOperations.lean +++ b/Mathlib/Algebra/Module/SpanRankOperations.lean @@ -16,12 +16,12 @@ In this file we show how operations on submodules interact with `Submodule.spanR # Main Results -* `Submodule.spanRank_baseChange_le` : base change doesn't increase span rank. +* `Submodule.spanRank_baseChange_le`: Base change doesn't increase the span rank. -* `TensorProduct.spanFinrank_top_eq_of_residueField` : for finitely generated module over - local ring, dimension of base change by residue field is equal to its span rank. +* `TensorProduct.spanFinrank_top_eq_of_residueField`: For a finitely generated module over + a local ring, the dimension of the base change to the residue field is equal to its span rank. -* `IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace` : The minimal number of +* `IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace`: The minimal number of generators of the unique maximal ideal is equal to the dimension of the cotangent space. -/ From 3ddb6f3df57765b5bcda811279c1f4524b51a595 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 21 Mar 2026 22:59:10 +0800 Subject: [PATCH 61/64] fix naming --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index 51b341e23f6347..d3a6dbb148cd91 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -41,7 +41,7 @@ can be generated by `dim R` elements. -/ class IsRegularLocalRing : Prop extends IsLocalRing R, IsNoetherianRing R where spanFinrank_maximalIdeal : (maximalIdeal R).spanFinrank = ringKrullDim R -lemma isRegularLocalRing_def [IsLocalRing R] [IsNoetherianRing R] : +lemma isRegularLocalRing_iff [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ (maximalIdeal R).spanFinrank = ringKrullDim R := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩ @@ -49,22 +49,22 @@ namespace IsRegularLocalRing lemma of_spanFinrank_maximalIdeal_le [IsLocalRing R] [IsNoetherianRing R] (le : (maximalIdeal R).spanFinrank ≤ ringKrullDim R) : IsRegularLocalRing R := - (isRegularLocalRing_def _).mpr (le_antisymm le (ringKrullDim_le_spanFinrank_maximalIdeal R)) + (isRegularLocalRing_iff _).mpr (le_antisymm le (ringKrullDim_le_spanFinrank_maximalIdeal R)) variable {R} in lemma of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R'] (e : R ≃+* R') : IsRegularLocalRing R' := by - let _ := e.isLocalRing - let _ := isNoetherianRing_of_ringEquiv R e - rwa [isRegularLocalRing_def, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e, - Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_def] + have := e.isLocalRing + have := isNoetherianRing_of_ringEquiv R e + rwa [isRegularLocalRing_iff, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e, + Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_iff] lemma iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by - rw [isRegularLocalRing_def, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace] + rw [isRegularLocalRing_iff, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace] instance {k : Type*} [Field k] : IsRegularLocalRing k := by - simp [isRegularLocalRing_def, maximalIdeal_eq_bot] + simp [isRegularLocalRing_iff, maximalIdeal_eq_bot] set_option backward.isDefEq.respectTransparency false in instance [IsDomain R] [IsDiscreteValuationRing R] : IsRegularLocalRing R := by From a979108458b37aeb112419dcf57df648ec539707 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 21 Mar 2026 23:00:22 +0800 Subject: [PATCH 62/64] refine def --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index d3a6dbb148cd91..1f1066e0ae16bc 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -34,13 +34,15 @@ the dimension of the cotangent space over the residue field being equal to `ring open IsLocalRing -variable (R : Type*) [CommRing R] - /-- A Noetherian local ring is said to be regular if its maximal ideal can be generated by `dim R` elements. -/ -class IsRegularLocalRing : Prop extends IsLocalRing R, IsNoetherianRing R where +@[stacks 00KU] +class IsRegularLocalRing (R : Type*) [CommRing R] : Prop extends + IsLocalRing R, IsNoetherianRing R where spanFinrank_maximalIdeal : (maximalIdeal R).spanFinrank = ringKrullDim R +variable (R : Type*) [CommRing R] + lemma isRegularLocalRing_iff [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ (maximalIdeal R).spanFinrank = ringKrullDim R := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩ From a5f41358e0b5e9a941a4458ffb73e87d2feddc72 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 21 Mar 2026 23:01:17 +0800 Subject: [PATCH 63/64] fix doc --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index 1f1066e0ae16bc..cec8fbca6ce028 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -12,7 +12,7 @@ public import Mathlib.RingTheory.KrullDimension.Field public import Mathlib.RingTheory.KrullDimension.PID /-! -# Define Regular Local Ring +# Regular local rings For a Noetherian local ring `R`, we define `IsRegularLocalRing` as `(maximalIdeal R).spanFinrank = ringKrullDim R`. This definition is equivalent to From 24105372eba66677fb5d31e9f3bda7ea1c5a9ad2 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 27 Mar 2026 22:31:21 +0800 Subject: [PATCH 64/64] combine instances --- Mathlib/RingTheory/RegularLocalRing/Defs.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/RingTheory/RegularLocalRing/Defs.lean b/Mathlib/RingTheory/RegularLocalRing/Defs.lean index cec8fbca6ce028..fc526882c0c464 100644 --- a/Mathlib/RingTheory/RegularLocalRing/Defs.lean +++ b/Mathlib/RingTheory/RegularLocalRing/Defs.lean @@ -65,15 +65,15 @@ lemma iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by rw [isRegularLocalRing_iff, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace] -instance {k : Type*} [Field k] : IsRegularLocalRing k := by - simp [isRegularLocalRing_iff, maximalIdeal_eq_bot] - set_option backward.isDefEq.respectTransparency false in -instance [IsDomain R] [IsDiscreteValuationRing R] : IsRegularLocalRing R := by - apply of_spanFinrank_maximalIdeal_le - rcases IsPrincipalIdealRing.principal (maximalIdeal R) with ⟨x, hx⟩ - simpa only [(IsPrincipalIdealRing.ringKrullDim_eq_one R) (IsDiscreteValuationRing.not_isField R), - Nat.cast_le_one, ← Set.ncard_singleton x, hx] using - Submodule.spanFinrank_span_le_ncard_of_finite (Set.finite_singleton x) +instance [IsLocalRing R] [IsDomain R] [IsPrincipalIdealRing R] : IsRegularLocalRing R := by + by_cases isf : IsField R + · let _ := isf.toField + simp [isRegularLocalRing_iff, maximalIdeal_eq_bot] + · apply of_spanFinrank_maximalIdeal_le + rcases IsPrincipalIdealRing.principal (maximalIdeal R) with ⟨x, hx⟩ + simpa only [(IsPrincipalIdealRing.ringKrullDim_eq_one R) isf, + Nat.cast_le_one, ← Set.ncard_singleton x, hx] using + Submodule.spanFinrank_span_le_ncard_of_finite (Set.finite_singleton x) end IsRegularLocalRing