From 1b2a710e7c54ceb3b807876f67eee624f6c66b50 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 30 Mar 2026 09:09:12 +0800 Subject: [PATCH 1/5] add projective dimension eq zero lemma --- .../Category/ModuleCat/ProjectiveDimension.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean b/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean index fc924fa08109b5..411498889a5593 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean @@ -20,7 +20,7 @@ public import Mathlib.CategoryTheory.Abelian.Projective.Dimension universe v v' u u' -variable {R : Type u} [CommRing R] [Small.{v} R] +variable {R : Type u} [CommRing R] open CategoryTheory Abelian Module @@ -28,7 +28,7 @@ namespace CategoryTheory section -variable {R' : Type u'} [CommRing R'] [Small.{v'} R'] (e : R ≃+* R') +variable [Small.{v} R] {R' : Type u'} [CommRing R'] [Small.{v'} R'] (e : R ≃+* R') variable {M : ModuleCat.{v} R} {N : ModuleCat.{v'} R'} @@ -81,7 +81,7 @@ end section -variable [Small.{v'} R] {M : ModuleCat.{v} R} {N : ModuleCat.{v'} R} +variable [Small.{v} R] [Small.{v'} R] {M : ModuleCat.{v} R} {N : ModuleCat.{v'} R} lemma hasProjectiveDimensionLE_of_linearEquiv (e : M ≃ₗ[R] N) (n : ℕ) [HasProjectiveDimensionLE M n] : HasProjectiveDimensionLE N n := @@ -94,3 +94,10 @@ lemma projectiveDimension_eq_of_linearEquiv (e : M ≃ₗ[R] N) : end end CategoryTheory + +lemma projectiveDimension_eq_zero_of_projective (M : ModuleCat.{v} R) [Nontrivial M] + [Projective M] : projectiveDimension M = 0 := by + apply ((projectiveDimension_le_iff M 0).mpr inferInstance).antisymm + ((projectiveDimension_ge_iff M 0).mpr _) + rw [hasProjectiveDimensionLT_zero_iff_isZero, ModuleCat.isZero_iff_subsingleton] + exact not_subsingleton_iff_nontrivial.mpr ‹_› From ee32f16e68ff61ddf88e9584fe0866ac5d253c01 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 3 Apr 2026 11:09:02 +0800 Subject: [PATCH 2/5] add lemma --- Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean b/Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean index 4c417d589725e8..9ec5476456a861 100644 --- a/Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean +++ b/Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean @@ -154,6 +154,9 @@ lemma projective_iff_hasProjectiveDimensionLT_one : exact ⟨fun _ ↦ inferInstance, fun _ ↦ projective_iff_subsingleton_ext_one.2 (HasProjectiveDimensionLT.subsingleton X 1 1 (by rfl))⟩ +lemma projective_iff_hasProjectiveDimensionLE_zero : Projective X ↔ HasProjectiveDimensionLE X 0 := + projective_iff_hasProjectiveDimensionLT_one + instance (priority := low) [HasProjectiveDimensionLT X 1] : Projective X := projective_iff_hasProjectiveDimensionLT_one.mpr ‹_› @@ -321,6 +324,12 @@ lemma projectiveDimension_ne_top_iff (X : C) : simp only [ne_eq, WithBot.coe_eq_top, ENat.coe_ne_top, not_false_eq_true, true_iff] exact ⟨d, by simpa only [← projectiveDimension_le_iff] using hd.le⟩ +lemma projectiveDimension_eq_zero_iff (X : C) : + projectiveDimension X = 0 ↔ Projective X ∧ ¬ Limits.IsZero X := by + rw [← projectiveDimension_eq_bot_iff, projective_iff_hasProjectiveDimensionLE_zero, + ← projectiveDimension_le_iff, ← WithBot.lt_zero_iff_eq_bot, not_lt, Nat.cast_zero, + le_antisymm_iff] + end CategoryTheory end ProjectiveDimension From c83495bfb2576981f9b09a5157f1d615b9d69099 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 3 Apr 2026 11:11:12 +0800 Subject: [PATCH 3/5] use lemma --- Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean b/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean index 411498889a5593..a19d375589a7e1 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean @@ -97,7 +97,5 @@ end CategoryTheory lemma projectiveDimension_eq_zero_of_projective (M : ModuleCat.{v} R) [Nontrivial M] [Projective M] : projectiveDimension M = 0 := by - apply ((projectiveDimension_le_iff M 0).mpr inferInstance).antisymm - ((projectiveDimension_ge_iff M 0).mpr _) - rw [hasProjectiveDimensionLT_zero_iff_isZero, ModuleCat.isZero_iff_subsingleton] - exact not_subsingleton_iff_nontrivial.mpr ‹_› + simpa [projectiveDimension_eq_zero_iff, ModuleCat.isZero_iff_subsingleton, + not_subsingleton_iff_nontrivial] using ⟨‹_›, ‹_›⟩ From 0aa607b8fe8c967d5b814352804965eaae21bb28 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 4 Apr 2026 11:14:01 +0800 Subject: [PATCH 4/5] fix namespace --- Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean b/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean index a19d375589a7e1..8c99ef6b69d7b9 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean @@ -24,7 +24,7 @@ variable {R : Type u} [CommRing R] open CategoryTheory Abelian Module -namespace CategoryTheory +namespace ModuleCat section @@ -93,9 +93,9 @@ lemma projectiveDimension_eq_of_linearEquiv (e : M ≃ₗ[R] N) : end -end CategoryTheory - lemma projectiveDimension_eq_zero_of_projective (M : ModuleCat.{v} R) [Nontrivial M] [Projective M] : projectiveDimension M = 0 := by simpa [projectiveDimension_eq_zero_iff, ModuleCat.isZero_iff_subsingleton, not_subsingleton_iff_nontrivial] using ⟨‹_›, ‹_›⟩ + +end ModuleCat From eee15c42693f08162414a1c5c52bc622868794a9 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 4 Apr 2026 11:15:23 +0800 Subject: [PATCH 5/5] add deprecation --- .../Category/ModuleCat/ProjectiveDimension.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean b/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean index 8c99ef6b69d7b9..3d98d41004fba9 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ProjectiveDimension.lean @@ -61,6 +61,10 @@ lemma hasProjectiveDimensionLE_of_semiLinearEquiv (e' : M ≃ₛₗ[RingHomClass have := (S_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mp ‹_› exact (S'_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mpr (ih eker) +@[deprecated (since := "2026-04-04")] +alias _root_.CategoryTheory.hasProjectiveDimensionLE_of_semiLinearEquiv := + hasProjectiveDimensionLE_of_semiLinearEquiv + attribute [local instance] RingHomInvPair.of_ringEquiv in lemma projectiveDimension_eq_of_semiLinearEquiv (e' : M ≃ₛₗ[RingHomClass.toRingHom e] N) : projectiveDimension M = projectiveDimension N := by @@ -77,6 +81,10 @@ lemma projectiveDimension_eq_of_semiLinearEquiv (e' : M ≃ₛₗ[RingHomClass.t exact ⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n, fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩ +@[deprecated (since := "2026-04-04")] +alias _root_.CategoryTheory.projectiveDimension_eq_of_semiLinearEquiv := + projectiveDimension_eq_of_semiLinearEquiv + end section @@ -87,10 +95,18 @@ lemma hasProjectiveDimensionLE_of_linearEquiv (e : M ≃ₗ[R] N) (n : ℕ) [HasProjectiveDimensionLE M n] : HasProjectiveDimensionLE N n := hasProjectiveDimensionLE_of_semiLinearEquiv (RingEquiv.refl R) e n +@[deprecated (since := "2026-04-04")] +alias _root_.CategoryTheory.hasProjectiveDimensionLE_of_linearEquiv := + hasProjectiveDimensionLE_of_linearEquiv + lemma projectiveDimension_eq_of_linearEquiv (e : M ≃ₗ[R] N) : projectiveDimension M = projectiveDimension N := projectiveDimension_eq_of_semiLinearEquiv (M := M) (N := N) (RingEquiv.refl R) e +@[deprecated (since := "2026-04-04")] +alias _root_.CategoryTheory.projectiveDimension_eq_of_linearEquiv := + projectiveDimension_eq_of_linearEquiv + end lemma projectiveDimension_eq_zero_of_projective (M : ModuleCat.{v} R) [Nontrivial M]