From ae5f2d36bd9ab058291d0a9615a09b950b7268da Mon Sep 17 00:00:00 2001 From: Xingyu Zhong Date: Wed, 24 Dec 2025 05:23:14 +0800 Subject: [PATCH 1/6] first commit --- Mathlib.lean | 3 +- Mathlib/Algebra/Module/SpanRank.lean | 105 +++++++++++++++++- Mathlib/RingTheory/Ideal/Cotangent.lean | 21 +++- .../RingTheory/Ideal/KrullsHeightTheorem.lean | 2 +- Mathlib/RingTheory/LocalRing/Module.lean | 2 +- Mathlib/RingTheory/LocalRing/Quotient.lean | 2 +- .../{Nakayama.lean => Nakayama/Basic.lean} | 25 +++++ Mathlib/RingTheory/Nakayama/SpanRank.lean | 77 +++++++++++++ .../RingTheory/Regular/RegularSequence.lean | 2 +- Mathlib/RingTheory/Support.lean | 2 +- 10 files changed, 228 insertions(+), 13 deletions(-) rename Mathlib/RingTheory/{Nakayama.lean => Nakayama/Basic.lean} (90%) create mode 100644 Mathlib/RingTheory/Nakayama/SpanRank.lean diff --git a/Mathlib.lean b/Mathlib.lean index fa3e268ef489d1..db3ba322d4c21d 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6136,7 +6136,8 @@ public import Mathlib.RingTheory.MvPowerSeries.Order public import Mathlib.RingTheory.MvPowerSeries.PiTopology public import Mathlib.RingTheory.MvPowerSeries.Substitution public import Mathlib.RingTheory.MvPowerSeries.Trunc -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic +public import Mathlib.RingTheory.Nakayama.SpanRank public import Mathlib.RingTheory.Nilpotent.Basic public import Mathlib.RingTheory.Nilpotent.Defs public import Mathlib.RingTheory.Nilpotent.Exp diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index f894195d05c718..d5ef194f4d2a1b 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -257,21 +257,114 @@ end Submodule section map universe u -section Submodule +namespace Submodule + +section Semilinear -variable {R : Type*} {M N : Type u} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] - [Module R N] (f : M →ₗ[R] N) (p : Submodule R M) +variable {R S : Type*} {M N : Type u} [Semiring R] [Semiring S] + [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] -lemma Submodule.spanRank_map_le : (p.map f).spanRank ≤ p.spanRank := by +lemma spanRank_map_le {σ : R →+* S} [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⟩ ↦ ⟨m, span_generators p ▸ subset_span hm, h⟩)) (by simp [span_generators])⟩ -variable {p} in -lemma Submodule.spanFinrank_map_le_of_fg (hp : p.FG) : (p.map f).spanFinrank ≤ p.spanFinrank := +lemma spanFinrank_map_le_of_fg {σ : R →+* S} [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) +variable {M₁ : Submodule R M} {N₁ : Submodule S N} + +lemma spanRank_le_spanRank_of_map_eq {σ : R →+* S} [RingHomSurjective σ] + (f : M →ₛₗ[σ] N) (h_map : map f M₁ = N₁) : N₁.spanRank ≤ M₁.spanRank := by + rcases exists_span_set_card_eq_spanRank M₁ with ⟨s, hscard, hsspan⟩ + rw [FG.spanRank_le_iff_exists_span_set_card_le] + use f '' s + constructor + · rw [← hscard]; exact Cardinal.mk_image_le + · rw [span_image', hsspan, h_map] + +lemma spanRank_le_spanRank_of_range_eq {σ : R →+* S} [RingHomSurjective σ] + (f : M₁ →ₛₗ[σ] N) (h_range : LinearMap.range f = N₁) : N₁.spanRank ≤ M₁.spanRank := by + -- obtain the spanning set of submodule `M₁` + rcases exists_span_set_card_eq_spanRank M₁ with ⟨s, hscard, hsspan⟩ + rw [FG.spanRank_le_iff_exists_span_set_card_le] + -- lift the set to a `Set M₁` + lift s to Set M₁ using show s ⊆ M₁ by rw [← hsspan]; exact subset_span + rw [Cardinal.mk_image_eq Subtype.val_injective] at hscard + change span R (M₁.subtype '' s) = M₁ at hsspan + rw [span_image] at hsspan + apply_fun comap M₁.subtype at hsspan + rw [comap_map_eq_of_injective (subtype_injective M₁) (span R s), comap_subtype_self] at hsspan + -- transfer the lifted set via `f` to get a spanning set of `N₁` + use f '' s + constructor + · grw [Cardinal.mk_image_le]; rw [hscard] + · rw [span_image, hsspan, map_top, h_range] + +lemma spanRank_le_spanRank_of_surjective {σ : R →+* S} [RingHomSurjective σ] + (f : M₁ →ₛₗ[σ] N₁) (h_surj : Function.Surjective f) : N₁.spanRank ≤ M₁.spanRank := by + apply spanRank_le_spanRank_of_range_eq (N₁.subtype.comp f) + rw [LinearMap.range_comp, LinearMap.range_eq_top_of_surjective f h_surj, map_top, range_subtype] + +lemma spanRank_eq_spanRank_of_addEquiv (σ : R →+* S) [RingHomSurjective σ] + (e : M₁ ≃+ N₁) (hm : ∀ (r : R) (m : M₁), e (r • m) = (σ r) • (e m)) : + M₁.spanRank = N₁.spanRank := by + -- recover the one-side linear map + let e_toLinearMap : M₁ →ₛₗ[σ] N₁ := { + toFun := e.toFun, + map_add' := e.map_add', + map_smul' := hm + } + have e_toLinearMap_apply : ∀ x, e_toLinearMap x = e x := by intro x; rfl + have e_toLinearMap_injective : Function.Injective e_toLinearMap := e.injective + have e_toLinearMap_e_symm_cancel : e_toLinearMap ∘ e.symm = id := by unfold e_toLinearMap; simp + apply le_antisymm + · -- obtain the spanning set of submodule `N₁` + rcases exists_span_set_card_eq_spanRank N₁ with ⟨s, hscard, hsspan⟩ + rw [FG.spanRank_le_iff_exists_span_set_card_le] + -- lift the set to a `Set N₁` + lift s to Set N₁ using show s ⊆ N₁ by rw [← hsspan]; exact subset_span + rw [Cardinal.mk_image_eq Subtype.val_injective] at hscard + change span S (N₁.subtype '' s) = N₁ at hsspan + rw [span_image] at hsspan + apply_fun comap N₁.subtype at hsspan + rw [comap_map_eq_of_injective (subtype_injective N₁) (span S s), comap_subtype_self] at hsspan + -- transfer the lifted set via `e.symm` to get a spanning set of `M₁` + use (M₁.subtype ∘ e.symm) '' s + constructor + · grw [Cardinal.mk_image_le]; rw [hscard] + · rw [Set.image_comp, span_image] + conv => rhs; rw [← map_subtype_top M₁] + congr + ext x; simp only [mem_top, iff_true] + rw [← apply_mem_span_image_iff_mem_span e_toLinearMap_injective, + ← Set.image_comp, e_toLinearMap_e_symm_cancel, e_toLinearMap_apply, Set.image_id, hsspan] + exact mem_top + · apply spanRank_le_spanRank_of_surjective e_toLinearMap e.surjective + +lemma spanRank_eq_spanRank_of_equiv' + (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] + (e : M₁ ≃ₛₗ[σ] N₁) : M₁.spanRank = N₁.spanRank := + le_antisymm + (spanRank_le_spanRank_of_surjective e.symm.toLinearMap e.symm.surjective) + (spanRank_le_spanRank_of_surjective e.toLinearMap e.surjective) + +end Semilinear + +section Linear + +variable {R : Type*} {M N : Type u} +variable [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] +variable {M₁ : Submodule R M} {N₁ : Submodule R N} + +lemma spanRank_eq_spanRank_of_equiv (e : M₁ ≃ₗ[R] N₁) : M₁.spanRank = N₁.spanRank := + spanRank_eq_spanRank_of_equiv' _ e + +end Linear + end Submodule section Ideal diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index ee3bdbe8d41e7e..37dda5d7198248 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -5,6 +5,7 @@ Authors: Andrew Yang -/ module +public import Mathlib.Algebra.Module.SpanRank public import Mathlib.Algebra.Module.Torsion.Basic public import Mathlib.Algebra.Ring.Idempotent public import Mathlib.LinearAlgebra.Dimension.Finite @@ -13,7 +14,8 @@ 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 +public import Mathlib.RingTheory.Nakayama.Basic +public import Mathlib.RingTheory.Nakayama.SpanRank /-! # The module `I ⧸ I ^ 2` @@ -219,6 +221,14 @@ lemma mapCotangent_toCotangent (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B) (h : I₁ ≤ I₂.comap f) (x : I₁) : Ideal.mapCotangent I₁ I₂ f h (Ideal.toCotangent I₁ x) = Ideal.toCotangent I₂ ⟨f x, h x.2⟩ := rfl +/-- `I ⧸ I ^ 2` as an `R`-submodule of `R ⧸ I ^ 2`. -/ +def cotangentSubmodule (I : Ideal R) : Submodule R (R ⧸ I ^ 2) := + Submodule.map (I ^ 2).mkQ I + +noncomputable def cotangentEquivSubmodule (I : Ideal R) : + I.Cotangent ≃ₗ[R] (Submodule.map (I ^ 2).mkQ I) := by + rw [pow_two]; exact Submodule.quotientIdealSubmoduleEquivMap I I + end Ideal namespace IsLocalRing @@ -264,6 +274,15 @@ lemma CotangentSpace.span_image_eq_top_iff [IsNoetherianRing R] {s : Set (maxima · simp only [Ideal.toCotangent_apply, Submodule.restrictScalars_top, Submodule.map_span] · exact Ideal.Quotient.mk_surjective +/-- +The span rank of the maximal ideal of a local ring equals the dimension of the cotangent space +if the maximal ideal is finitely generated. +-/ +theorem rank_cotangentSpace_eq_spanrank_maximalIdeal (hm : (maximalIdeal R).FG) : + Module.rank (ResidueField R) (CotangentSpace R) = (maximalIdeal R).spanRank := by + rw [Submodule.spanRank_eq_spanRank_quotient_ideal_quotientIdealSubmodule + hm (maximalIdeal_le_jacobson _), Submodule.rank_eq_spanRank_of_free] + open Module lemma finrank_cotangentSpace_eq_zero_iff [IsNoetherianRing R] : diff --git a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean index 9fc2c0018e22c4..2061162a6b52ab 100644 --- a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean +++ b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean @@ -9,7 +9,7 @@ public import Mathlib.RingTheory.HopkinsLevitzki public import Mathlib.RingTheory.Ideal.GoingDown public import Mathlib.RingTheory.Ideal.Height public import Mathlib.RingTheory.Localization.Submodule -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic /-! # Krull's Height Theorem diff --git a/Mathlib/RingTheory/LocalRing/Module.lean b/Mathlib/RingTheory/LocalRing/Module.lean index 221f6cbd2021c6..0ec6c9f18c70b6 100644 --- a/Mathlib/RingTheory/LocalRing/Module.lean +++ b/Mathlib/RingTheory/LocalRing/Module.lean @@ -14,7 +14,7 @@ public import Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder public import Mathlib.RingTheory.LocalProperties.Exactness public import Mathlib.RingTheory.LocalRing.ResidueField.Basic public import Mathlib.RingTheory.LocalRing.ResidueField.Ideal -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic public import Mathlib.RingTheory.Support /-! diff --git a/Mathlib/RingTheory/LocalRing/Quotient.lean b/Mathlib/RingTheory/LocalRing/Quotient.lean index 7c7a454fc1bbc6..e69228691ac34a 100644 --- a/Mathlib/RingTheory/LocalRing/Quotient.lean +++ b/Mathlib/RingTheory/LocalRing/Quotient.lean @@ -13,7 +13,7 @@ public import Mathlib.RingTheory.Ideal.Over public import Mathlib.RingTheory.Ideal.Quotient.Index public import Mathlib.RingTheory.LocalRing.ResidueField.Defs public import Mathlib.RingTheory.LocalRing.RingHom.Basic -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic /-! diff --git a/Mathlib/RingTheory/Nakayama.lean b/Mathlib/RingTheory/Nakayama/Basic.lean similarity index 90% rename from Mathlib/RingTheory/Nakayama.lean rename to Mathlib/RingTheory/Nakayama/Basic.lean index 4079c8d0325610..e6230a4d1ebf58 100644 --- a/Mathlib/RingTheory/Nakayama.lean +++ b/Mathlib/RingTheory/Nakayama/Basic.lean @@ -198,4 +198,29 @@ theorem le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot grw [sup_comm, ← htspan] simp only [le_sup_right] +-- TODO: this might should be placed elsewhere? +noncomputable def quotientIdealSubmoduleEquivMap (N : Submodule R M) (I : Ideal R) : + (N ⧸ (I • ⊤ : Submodule R N)) ≃ₗ[R] (map (I • N).mkQ N) := by + refine LinearEquiv.ofBijective ?_ ⟨?_, ?_⟩ + · refine Submodule.liftQ _ ?_ ?_ + · exact { + toFun x := by + rcases x with ⟨x, hx⟩ + use ((I • N).mkQ x), x, hx + map_add' := by simp + map_smul' := by simp + } + · intro x hx + rw [mem_smul_top_iff] at hx + simp [hx] + · rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot'] + intro x hx + induction x using Submodule.Quotient.induction_on with | H x => + simp only [mkQ_apply, liftQ_apply, LinearMap.coe_mk, AddHom.coe_mk, mk_eq_zero, + Quotient.mk_eq_zero] at hx + simp only [Quotient.mk_eq_zero, mem_smul_top_iff, hx] + · rintro ⟨_, ⟨x, hx, rfl⟩⟩ + use Quotient.mk ⟨x, hx⟩ + simp + end Submodule diff --git a/Mathlib/RingTheory/Nakayama/SpanRank.lean b/Mathlib/RingTheory/Nakayama/SpanRank.lean new file mode 100644 index 00000000000000..c90a28199ef40b --- /dev/null +++ b/Mathlib/RingTheory/Nakayama/SpanRank.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2025 Xingyu Zhong. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Xingyu Zhong +-/ +module + +public import Mathlib.RingTheory.Nakayama.Basic +public import Mathlib.Algebra.Module.SpanRank +public import Mathlib.Algebra.Module.Torsion.Basic + +/-! +# Nakayama's lemma and `Submodule.spanRank` + +This file states some versions of Nakayama's lemma in terms of `Submodule.spanRank`. +-/ + +@[expose] public section + +variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] + +namespace Submodule + +theorem spanRank_eq_spanRank_map_mkQ_of_le_jacobson_bot + {I : Ideal R} {N : Submodule R M} + (hN : N.FG) (hIjac : I ≤ Ideal.jacobson ⊥) : + N.spanRank = (map (I • N).mkQ N).spanRank := by + have smul_sup_eq : I • N ⊔ N = N := by rw [sup_eq_right]; exact smul_le_right + apply le_antisymm + · rcases exists_span_set_card_eq_spanRank (map (I • N).mkQ N) with ⟨s, ⟨hscard, hsspan⟩⟩ + have hs_subset : s ⊆ map (I • N).mkQ N := by rw [← hsspan]; exact subset_span + -- pull back `s` from N / I to N to get a spanning set of N + let pbv := fun (y : M ⧸ I • N) ↦ Classical.choose <| + Set.Nonempty.preimage (Set.singleton_nonempty y) (mkQ_surjective (I • N)) + let pbp := fun (y : M ⧸ I • N) ↦ Classical.choose_spec <| + Set.Nonempty.preimage (Set.singleton_nonempty y) (mkQ_surjective (I • N)) + have mkQ_comp_pbv_cancel : (I • N).mkQ ∘ pbv = id := by funext y; exact pbp y + -- show the inequality via the pulled back set + rw [FG.spanRank_le_iff_exists_span_set_card_le] + use pbv '' s + constructor + · rw [← hscard] + apply Cardinal.mk_image_le + · apply le_antisymm + · rw [span_le]; grw [hs_subset] + have := comap_map_mkQ (I • N) N; rw [smul_sup_eq] at this + -- obtain a set version of `Submodule.comap_map_mkQ` + apply_fun fun x ↦ (x : Set M) at this + rw [comap_coe, map_coe] at this + -- return to the goal + rw [← this, ← Set.image_subset_iff, ← Set.image_comp, mkQ_comp_pbv_cancel] + simp + · apply le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot hN hIjac + rw [map_span, ← Set.image_comp, mkQ_comp_pbv_cancel] + simp [hsspan] + · exact spanRank_le_spanRank_of_map_eq (mkQ (I • N)) (by dsimp) + +theorem spanRank_eq_spanRank_quotientIdealSubmodule + {I : Ideal R} {N : Submodule R M} + (hN : N.FG) (hIjac : I ≤ Ideal.jacobson ⊥) : + N.spanRank = (⊤ : Submodule R (N ⧸ (I • ⊤ : Submodule R N))).spanRank := by + rw [spanRank_eq_spanRank_map_mkQ_of_le_jacobson_bot hN hIjac] + apply spanRank_eq_spanRank_of_equiv + symm + exact LinearEquiv.trans + (Submodule.topEquiv : _ ≃ₗ[R] (N ⧸ (I • ⊤ : Submodule R N))) + (quotientIdealSubmoduleEquivMap N I) + +theorem spanRank_eq_spanRank_quotient_ideal_quotientIdealSubmodule + {I : Ideal R} {N : Submodule R M} + (hN : N.FG) (hIjac : I ≤ Ideal.jacobson ⊥) : + N.spanRank = (⊤ : Submodule (R ⧸ I) (N ⧸ (I • ⊤ : Submodule R N))).spanRank := by + rw [spanRank_eq_spanRank_quotientIdealSubmodule hN hIjac] + exact spanRank_eq_spanRank_of_addEquiv (Ideal.Quotient.mk I) + (LinearEquiv.toAddEquiv (LinearEquiv.refl R _)) (by intros; rfl) + +end Submodule diff --git a/Mathlib/RingTheory/Regular/RegularSequence.lean b/Mathlib/RingTheory/Regular/RegularSequence.lean index d8d713cb8d654f..383a8256446d60 100644 --- a/Mathlib/RingTheory/Regular/RegularSequence.lean +++ b/Mathlib/RingTheory/Regular/RegularSequence.lean @@ -7,7 +7,7 @@ module public import Mathlib.RingTheory.Artinian.Module public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic public import Mathlib.RingTheory.Regular.IsSMulRegular /-! diff --git a/Mathlib/RingTheory/Support.lean b/Mathlib/RingTheory/Support.lean index 3c761758e71ee3..76fe1670bf1131 100644 --- a/Mathlib/RingTheory/Support.lean +++ b/Mathlib/RingTheory/Support.lean @@ -7,7 +7,7 @@ module public import Mathlib.RingTheory.Ideal.Colon public import Mathlib.RingTheory.Localization.Finiteness -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic public import Mathlib.RingTheory.QuotSMulTop public import Mathlib.RingTheory.Spectrum.Prime.Basic From 0fb16c8a310128522e73348abd2395c6596a8859 Mon Sep 17 00:00:00 2001 From: Xingyu Zhong Date: Wed, 24 Dec 2025 08:08:43 +0800 Subject: [PATCH 2/6] fix doc --- Mathlib/RingTheory/Ideal/Cotangent.lean | 6 +++++- Mathlib/RingTheory/Nakayama/Basic.lean | 6 +++++- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 37dda5d7198248..8ed34d85afaebf 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -221,10 +221,14 @@ lemma mapCotangent_toCotangent (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B) (h : I₁ ≤ I₂.comap f) (x : I₁) : Ideal.mapCotangent I₁ I₂ f h (Ideal.toCotangent I₁ x) = Ideal.toCotangent I₂ ⟨f x, h x.2⟩ := rfl -/-- `I ⧸ I ^ 2` as an `R`-submodule of `R ⧸ I ^ 2`. -/ +/-- `I ⧸ I ^ 2` as the image of `I` in the `R`-module `R / I ^ 2`. -/ def cotangentSubmodule (I : Ideal R) : Submodule R (R ⧸ I ^ 2) := Submodule.map (I ^ 2).mkQ I +/-- +The equivalence of the two definitions of `I / I ^ 2`, +either as a quotient of `I` or the image of `I` in the `R`-module `R / I ^ 2`. +-/ noncomputable def cotangentEquivSubmodule (I : Ideal R) : I.Cotangent ≃ₗ[R] (Submodule.map (I ^ 2).mkQ I) := by rw [pow_two]; exact Submodule.quotientIdealSubmoduleEquivMap I I diff --git a/Mathlib/RingTheory/Nakayama/Basic.lean b/Mathlib/RingTheory/Nakayama/Basic.lean index e6230a4d1ebf58..876fb29031a011 100644 --- a/Mathlib/RingTheory/Nakayama/Basic.lean +++ b/Mathlib/RingTheory/Nakayama/Basic.lean @@ -198,9 +198,13 @@ theorem le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot grw [sup_comm, ← htspan] simp only [le_sup_right] --- TODO: this might should be placed elsewhere? +/-- +The equivalence of the two definitions of `N / I N`, +either as a quotient of `N`, or the image of `N` in `M / I M`. +-/ noncomputable def quotientIdealSubmoduleEquivMap (N : Submodule R M) (I : Ideal R) : (N ⧸ (I • ⊤ : Submodule R N)) ≃ₗ[R] (map (I • N).mkQ N) := by + -- TODO: find a better place for this equivalence refine LinearEquiv.ofBijective ?_ ⟨?_, ?_⟩ · refine Submodule.liftQ _ ?_ ?_ · exact { From 778dd62bbce901eaca7f59d2e83524d296872426 Mon Sep 17 00:00:00 2001 From: Xingyu Zhong Date: Wed, 24 Dec 2025 15:03:00 +0800 Subject: [PATCH 3/6] update doc --- Mathlib/RingTheory/Ideal/Cotangent.lean | 11 ++++++----- Mathlib/RingTheory/Nakayama/Basic.lean | 15 +++++++++++---- Mathlib/RingTheory/Nakayama/SpanRank.lean | 21 +++++++++++++++++++++ 3 files changed, 38 insertions(+), 9 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 8ed34d85afaebf..9e2b6c4910b393 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -221,13 +221,14 @@ lemma mapCotangent_toCotangent (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B) (h : I₁ ≤ I₂.comap f) (x : I₁) : Ideal.mapCotangent I₁ I₂ f h (Ideal.toCotangent I₁ x) = Ideal.toCotangent I₂ ⟨f x, h x.2⟩ := rfl -/-- `I ⧸ I ^ 2` as the image of `I` in the `R`-module `R / I ^ 2`. -/ +/-- `I ⧸ I ^ 2` as the image of `I` under the `R`-module quotient map `R → R / (I ^ 2)`. -/ def cotangentSubmodule (I : Ideal R) : Submodule R (R ⧸ I ^ 2) := Submodule.map (I ^ 2).mkQ I /-- -The equivalence of the two definitions of `I / I ^ 2`, -either as a quotient of `I` or the image of `I` in the `R`-module `R / I ^ 2`. +The linear equivalence of the two definitions of `I / I ^ 2`, +either as a quotient of `I` by its submodule `I • ⊤`, +or the image of `I` under the `R`-module quotient map `R → R / (I ^ 2)`. -/ noncomputable def cotangentEquivSubmodule (I : Ideal R) : I.Cotangent ≃ₗ[R] (Submodule.map (I ^ 2).mkQ I) := by @@ -279,8 +280,8 @@ lemma CotangentSpace.span_image_eq_top_iff [IsNoetherianRing R] {s : Set (maxima · exact Ideal.Quotient.mk_surjective /-- -The span rank of the maximal ideal of a local ring equals the dimension of the cotangent space -if the maximal ideal is finitely generated. +In a local ring, the dimension of the cotangent space is equal to +the span rank of the maximal ideal, if the maximal ideal is finitely generated. -/ theorem rank_cotangentSpace_eq_spanrank_maximalIdeal (hm : (maximalIdeal R).FG) : Module.rank (ResidueField R) (CotangentSpace R) = (maximalIdeal R).spanRank := by diff --git a/Mathlib/RingTheory/Nakayama/Basic.lean b/Mathlib/RingTheory/Nakayama/Basic.lean index 876fb29031a011..4247e6ad38e706 100644 --- a/Mathlib/RingTheory/Nakayama/Basic.lean +++ b/Mathlib/RingTheory/Nakayama/Basic.lean @@ -184,8 +184,14 @@ lemma exists_sub_one_mem_and_smul_le_of_fg_of_le_sup {I : Ideal R} | add _ _ _ _ hx hy => exact N.add_mem hx hy | zero => exact N.zero_mem -/-- **Nakayama's Lemma** - Statement (8) in -[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV). -/ +/-- +**Nakayama's Lemma** - a slightly more general version of (8) in +[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV). + +If `N` is a finitely generated `R`-submodule of `M`, whose image under the quotient map +`M → M / (I • N)` is contained in the span of a set `t` of `M`, +then `N` is contained in the span of `t`, given that `I` is contained in the Jacobson radical. +-/ @[stacks 00DV "(8)"] theorem le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot {I : Ideal R} {N : Submodule R M} {t : Set M} @@ -199,8 +205,9 @@ theorem le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot simp only [le_sup_right] /-- -The equivalence of the two definitions of `N / I N`, -either as a quotient of `N`, or the image of `N` in `M / I M`. +The linear equivalence of the two definitions of `N / I • N`, +either as a quotient of `N` by its submodule `I • ⊤`, +or the image of `N` under the `R`-module quotient map `M → M / (I • N)`. -/ noncomputable def quotientIdealSubmoduleEquivMap (N : Submodule R M) (I : Ideal R) : (N ⧸ (I • ⊤ : Submodule R N)) ≃ₗ[R] (map (I • N).mkQ N) := by diff --git a/Mathlib/RingTheory/Nakayama/SpanRank.lean b/Mathlib/RingTheory/Nakayama/SpanRank.lean index c90a28199ef40b..fffb188ef4f5e2 100644 --- a/Mathlib/RingTheory/Nakayama/SpanRank.lean +++ b/Mathlib/RingTheory/Nakayama/SpanRank.lean @@ -21,6 +21,13 @@ variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] namespace Submodule +/-- +The span rank of an `R`-submodule `N` of `M` is equal to +the span rank of the `R`-submodule `N / (I • N)` of `M / (I • N)`, +provided that `N` is finitely generated and `I` is contained in the Jacobson radical of `R`. + +Here `N / (I • N)` is the image of `N` under the `R`-module quotient map `M → M / (I • N)`. +-/ theorem spanRank_eq_spanRank_map_mkQ_of_le_jacobson_bot {I : Ideal R} {N : Submodule R M} (hN : N.FG) (hIjac : I ≤ Ideal.jacobson ⊥) : @@ -55,6 +62,13 @@ theorem spanRank_eq_spanRank_map_mkQ_of_le_jacobson_bot simp [hsspan] · exact spanRank_le_spanRank_of_map_eq (mkQ (I • N)) (by dsimp) +/-- +The span rank of an `R`-submodule `N` of `M` is equal to +the span rank of the `R`-module `N / (I • N)`, +provided that `N` is finitely generated and `I` is contained in the Jacobson radical of `R`. + +Here `N / (I • N)` is obtained by directly taking the quotient of `N` by the its submodule `I • ⊤`. +-/ theorem spanRank_eq_spanRank_quotientIdealSubmodule {I : Ideal R} {N : Submodule R M} (hN : N.FG) (hIjac : I ≤ Ideal.jacobson ⊥) : @@ -66,6 +80,13 @@ theorem spanRank_eq_spanRank_quotientIdealSubmodule (Submodule.topEquiv : _ ≃ₗ[R] (N ⧸ (I • ⊤ : Submodule R N))) (quotientIdealSubmoduleEquivMap N I) +/-- +The span rank of an `R`-submodule `N` of `M` is equal to +the span rank of the `R / I`-module `N / (I • N)`, +provided that `N` is finitely generated and `I` is contained in the Jacobson radical of `R`. + +Here `N / (I • N)` is obtained by directly taking the quotient of `N` by the its submodule `I • ⊤`. +-/ theorem spanRank_eq_spanRank_quotient_ideal_quotientIdealSubmodule {I : Ideal R} {N : Submodule R M} (hN : N.FG) (hIjac : I ≤ Ideal.jacobson ⊥) : From 30ad83966cdc375abe00a687f2caaed8d67bcbf4 Mon Sep 17 00:00:00 2001 From: Xingyu Zhong Date: Wed, 24 Dec 2025 18:20:09 +0800 Subject: [PATCH 4/6] reorganize Nakayama's lemma and tidy up proofs --- Mathlib/RingTheory/Nakayama/Basic.lean | 77 ++++++++++++++++++++--- Mathlib/RingTheory/Nakayama/SpanRank.lean | 28 +-------- 2 files changed, 71 insertions(+), 34 deletions(-) diff --git a/Mathlib/RingTheory/Nakayama/Basic.lean b/Mathlib/RingTheory/Nakayama/Basic.lean index 4247e6ad38e706..266fa3c85bf9af 100644 --- a/Mathlib/RingTheory/Nakayama/Basic.lean +++ b/Mathlib/RingTheory/Nakayama/Basic.lean @@ -29,7 +29,7 @@ This file contains some alternative statements of Nakayama's Lemma as found in * `Submodule.smul_le_of_le_smul_of_le_jacobson_bot` - Statement (4) in [Stacks: Nakayama's Lemma](https://stacks.math.columbia.edu/tag/00DV). -* `Submodule.le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot` - Statement (8) in +* `exists_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot` - Statement (8) in [Stacks: Nakayama's Lemma](https://stacks.math.columbia.edu/tag/00DV). Note that a version of Statement (1) in @@ -185,15 +185,12 @@ lemma exists_sub_one_mem_and_smul_le_of_fg_of_le_sup {I : Ideal R} | zero => exact N.zero_mem /-- -**Nakayama's Lemma** - a slightly more general version of (8) in -[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV). - -If `N` is a finitely generated `R`-submodule of `M`, whose image under the quotient map -`M → M / (I • N)` is contained in the span of a set `t` of `M`, -then `N` is contained in the span of `t`, given that `I` is contained in the Jacobson radical. +If `N` is a finitely generated `R`-submodule of `M`, +`I` is an ideal contained in the Jacobson radical of `R`, +`t` is a set of `M` whose span image under the quotient map `M → M / (I • N)` +contains the image of `N`, then `N` is contained in the span of `t`. -/ -@[stacks 00DV "(8)"] -theorem le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot +lemma le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot {I : Ideal R} {N : Submodule R M} {t : Set M} (hN : N.FG) (hIjac : I ≤ jacobson ⊥) (htspan : map (I • N).mkQ N ≤ map (I • N).mkQ (span R t)) : N ≤ span R t := by @@ -204,6 +201,68 @@ theorem le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot grw [sup_comm, ← htspan] simp only [le_sup_right] +/-- +If `N` is a finitely generated `R`-submodule of `M`, +`I` is an ideal contained in the Jacobson radical of `R`, +`t` is a set of `M` whose span image under the quotient map `M → M / (I • N)` +is the image of `N`, then `t` spans `N`. +-/ +lemma span_eq_of_map_mkQ_span_eq_map_mkQ_of_le_jacobson_bot + {I : Ideal R} {N : Submodule R M} {t : Set M} + (hN : N.FG) (hIjac : I ≤ jacobson ⊥) (htspan : map (I • N).mkQ (span R t) = map (I • N).mkQ N) : + span R t = N := by + symm; apply le_antisymm + · apply le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot hN hIjac htspan.ge + · apply_fun comap (I • N).mkQ at htspan + simp only [comap_map_mkQ, smul_le_right, sup_of_le_right] at htspan + rw [← htspan]; apply le_sup_right + +/- +If `N` is a finitely generated `R`-submodule of `M`, +`I` is an ideal contained in the Jacobson radical of `R`, +`s` is a set of `M / (I • N)` that spans the quotient image of `N`, +then any set `t` of `M` in bijection with `s` via the quotient map spans `N`. +-/ +theorem span_eq_of_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot + {I : Ideal R} {N : Submodule R M} (s : Set (M ⧸ (I • N))) + (hN : N.FG) (hIjac : I ≤ jacobson ⊥) (hsspan : span R s = map (I • N).mkQ N) : + ∀ (t : Set M) (e : t ≃ s), (∀ x : t, e x = (I • N).mkQ x) → span R t = N := by + intro t e he + apply span_eq_of_map_mkQ_span_eq_map_mkQ_of_le_jacobson_bot hN hIjac + rw [← hsspan, map_span] + congr; ext y + constructor + · rintro ⟨x, hx, rfl⟩; rw [← he ⟨x, hx⟩]; simp + · intro hy; use (e.symm ⟨y, hy⟩).val + exact ⟨by simp, by rw [← he]; simp⟩ + +/-- +**Nakayama's Lemma** - Statement (8) in +[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV). + +If `N` is a finitely generated `R`-submodule of `M`, +`I` is an ideal contained in the Jacobson radical of `R`, +`s` is a set of `M / (I • N)` that spans the quotient image of `N`, +then there exists a spanning set `t` of `N` in bijection with `s` via the quotient map. +-/ +@[stacks 00DV "(8)"] +theorem exists_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot + {I : Ideal R} {N : Submodule R M} (s : Set (M ⧸ (I • N))) + (hN : N.FG) (hIjac : I ≤ jacobson ⊥) (hsspan : span R s = map (I • N).mkQ N) : + ∃ (t : Set M) (e : t ≃ s), (∀ x : t, e x = (I • N).mkQ x) ∧ span R t = N := by + let t := Quotient.out '' s + let e : t ≃ s := { + toFun := by intro ⟨x, hx⟩; use (I • N).mkQ x; rcases hx with ⟨y, hy, rfl⟩; simpa using hy + invFun := by intro ⟨y, hy⟩; use Quotient.out y; simpa [t] using hy + left_inv := by rintro ⟨x, y, hy, rfl⟩; simp + right_inv := by intro ⟨y, hy⟩; simp + } + use t, e + constructor + · intros; simp [e] + · apply span_eq_of_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot + s hN hIjac hsspan t e (by intros; simp [e]) + /-- The linear equivalence of the two definitions of `N / I • N`, either as a quotient of `N` by its submodule `I • ⊤`, diff --git a/Mathlib/RingTheory/Nakayama/SpanRank.lean b/Mathlib/RingTheory/Nakayama/SpanRank.lean index fffb188ef4f5e2..b0516def8bef39 100644 --- a/Mathlib/RingTheory/Nakayama/SpanRank.lean +++ b/Mathlib/RingTheory/Nakayama/SpanRank.lean @@ -32,34 +32,12 @@ theorem spanRank_eq_spanRank_map_mkQ_of_le_jacobson_bot {I : Ideal R} {N : Submodule R M} (hN : N.FG) (hIjac : I ≤ Ideal.jacobson ⊥) : N.spanRank = (map (I • N).mkQ N).spanRank := by - have smul_sup_eq : I • N ⊔ N = N := by rw [sup_eq_right]; exact smul_le_right apply le_antisymm · rcases exists_span_set_card_eq_spanRank (map (I • N).mkQ N) with ⟨s, ⟨hscard, hsspan⟩⟩ - have hs_subset : s ⊆ map (I • N).mkQ N := by rw [← hsspan]; exact subset_span - -- pull back `s` from N / I to N to get a spanning set of N - let pbv := fun (y : M ⧸ I • N) ↦ Classical.choose <| - Set.Nonempty.preimage (Set.singleton_nonempty y) (mkQ_surjective (I • N)) - let pbp := fun (y : M ⧸ I • N) ↦ Classical.choose_spec <| - Set.Nonempty.preimage (Set.singleton_nonempty y) (mkQ_surjective (I • N)) - have mkQ_comp_pbv_cancel : (I • N).mkQ ∘ pbv = id := by funext y; exact pbp y - -- show the inequality via the pulled back set + rcases exists_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot + s hN hIjac hsspan with ⟨t, e, heq, htspan⟩ rw [FG.spanRank_le_iff_exists_span_set_card_le] - use pbv '' s - constructor - · rw [← hscard] - apply Cardinal.mk_image_le - · apply le_antisymm - · rw [span_le]; grw [hs_subset] - have := comap_map_mkQ (I • N) N; rw [smul_sup_eq] at this - -- obtain a set version of `Submodule.comap_map_mkQ` - apply_fun fun x ↦ (x : Set M) at this - rw [comap_coe, map_coe] at this - -- return to the goal - rw [← this, ← Set.image_subset_iff, ← Set.image_comp, mkQ_comp_pbv_cancel] - simp - · apply le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot hN hIjac - rw [map_span, ← Set.image_comp, mkQ_comp_pbv_cancel] - simp [hsspan] + use t, (by rw [← hscard, Equiv.cardinal_eq]; exact e), htspan · exact spanRank_le_spanRank_of_map_eq (mkQ (I • N)) (by dsimp) /-- From 8182275b8dbd51ae7e7df9b6bc4b2d46fd7fd44d Mon Sep 17 00:00:00 2001 From: Xingyu Zhong Date: Wed, 24 Dec 2025 18:34:59 +0800 Subject: [PATCH 5/6] update doc --- Mathlib/RingTheory/Ideal/Cotangent.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 9e2b6c4910b393..f3b23e0400ca21 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -21,8 +21,13 @@ public import Mathlib.RingTheory.Nakayama.SpanRank # The module `I ⧸ I ^ 2` In this file, we provide special API support for the module `I ⧸ I ^ 2`. The official -definition is a quotient module of `I`, but the alternative definition as an ideal of `R ⧸ I ^ 2` is -also given, and the two are `R`-equivalent as in `Ideal.cotangentEquivIdeal`. +definition is a quotient module of `I`, but there are two alternative definitions: + +- as an ideal of `R ⧸ I ^ 2`, +- as the image of `I` under the `R`-module quotient map `R → R / (I ^ 2)` + +They are shown to be `R`-linear equivalent to the official definition via +`Ideal.cotangentEquivIdeal` and `Ideal.cotangentEquivSubmodule` respectively. Additional support is also given to the cotangent space `m ⧸ m ^ 2` of a local ring. From bcffea0ab13819ec801d47d1e5cfabaaa3c00b63 Mon Sep 17 00:00:00 2001 From: Xingyu Zhong Date: Wed, 24 Dec 2025 22:45:38 +0800 Subject: [PATCH 6/6] update doc --- Mathlib/RingTheory/Nakayama/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Nakayama/Basic.lean b/Mathlib/RingTheory/Nakayama/Basic.lean index 266fa3c85bf9af..cd7738c5d1915e 100644 --- a/Mathlib/RingTheory/Nakayama/Basic.lean +++ b/Mathlib/RingTheory/Nakayama/Basic.lean @@ -29,7 +29,7 @@ This file contains some alternative statements of Nakayama's Lemma as found in * `Submodule.smul_le_of_le_smul_of_le_jacobson_bot` - Statement (4) in [Stacks: Nakayama's Lemma](https://stacks.math.columbia.edu/tag/00DV). -* `exists_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot` - Statement (8) in +* `Submodule.exists_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot` - Statement (8) in [Stacks: Nakayama's Lemma](https://stacks.math.columbia.edu/tag/00DV). Note that a version of Statement (1) in