diff --git a/Mathlib.lean b/Mathlib.lean index 25322c6b37cb10..c3009d894cb544 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -161,15 +161,19 @@ public import Mathlib.Algebra.Category.ModuleCat.Differentials.Basic public import Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf public import Mathlib.Algebra.Category.ModuleCat.EnoughInjectives public import Mathlib.Algebra.Category.ModuleCat.EpiMono +public import Mathlib.Algebra.Category.ModuleCat.Ext.Baer +public import Mathlib.Algebra.Category.ModuleCat.Ext.BaseChange public import Mathlib.Algebra.Category.ModuleCat.Ext.Basic public import Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting public import Mathlib.Algebra.Category.ModuleCat.Ext.Finite public import Mathlib.Algebra.Category.ModuleCat.Ext.HasExt +public import Mathlib.Algebra.Category.ModuleCat.Ext.RingEquiv public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower public import Mathlib.Algebra.Category.ModuleCat.FilteredColimits public import Mathlib.Algebra.Category.ModuleCat.Free public import Mathlib.Algebra.Category.ModuleCat.Images public import Mathlib.Algebra.Category.ModuleCat.Injective +public import Mathlib.Algebra.Category.ModuleCat.InjectiveDimension public import Mathlib.Algebra.Category.ModuleCat.Kernels public import Mathlib.Algebra.Category.ModuleCat.LeftResolution public import Mathlib.Algebra.Category.ModuleCat.Limits @@ -6602,6 +6606,8 @@ public import Mathlib.RingTheory.FractionalIdeal.Operations public import Mathlib.RingTheory.FreeCommRing public import Mathlib.RingTheory.FreeRing public import Mathlib.RingTheory.Frobenius +public import Mathlib.RingTheory.Gorenstein.Completion +public import Mathlib.RingTheory.Gorenstein.Defs public import Mathlib.RingTheory.GradedAlgebra.AlgHom public import Mathlib.RingTheory.GradedAlgebra.Basic public import Mathlib.RingTheory.GradedAlgebra.FiniteType @@ -6953,6 +6959,7 @@ public import Mathlib.RingTheory.Regular.Category public import Mathlib.RingTheory.Regular.Depth public import Mathlib.RingTheory.Regular.Flat public import Mathlib.RingTheory.Regular.Free +public import Mathlib.RingTheory.Regular.InjectiveDimension public import Mathlib.RingTheory.Regular.IsSMulRegular public import Mathlib.RingTheory.Regular.LinearMap public import Mathlib.RingTheory.Regular.ProjectiveDimension diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index b162815dd0a236..6422b9724764a5 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean @@ -314,6 +314,16 @@ def restrictScalarsIsoOfEquiv {R S : Type v} [Ring R] [Ring S] (e : R ≃+* S) : { __ := e.symm map_smul' x y := by simp [RingHom.toModule_smul] } +attribute [local instance] RingHomInvPair.of_ringEquiv in +/-- Given semi linear equiv `M ≃ M'`, the categorical isomorphism `M ≅ ↑R M'` -/ +noncomputable def isoRestrictScalars {R S} [Ring R] [Ring S] {M' : ModuleCat.{v} S} + {M : ModuleCat.{v} R} (e : R ≃+* S) (e' : M ≃ₛₗ[RingHomClass.toRingHom e] M') : + M ≅ ((ModuleCat.restrictScalars (RingHomClass.toRingHom e)).obj M') := + let e : M ≃ₗ[R] ((ModuleCat.restrictScalars (RingHomClass.toRingHom e)).obj M') := { + __ := e' + map_smul' r m := by simp } + e.toModuleIso + @[simp] lemma restrictScalarsIsoOfEquiv_hom_apply {R S : Type v} [Ring R] [Ring S] (e : R ≃+* S) (x : S) : dsimp% (ModuleCat.restrictScalarsIsoOfEquiv e).hom x = e.symm x := diff --git a/Mathlib/Algebra/Category/ModuleCat/Ext/Baer.lean b/Mathlib/Algebra/Category/ModuleCat/Ext/Baer.lean new file mode 100644 index 00000000000000..23938b60be11a3 --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Ext/Baer.lean @@ -0,0 +1,157 @@ +/- +Copyright (c) 2025 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.Category.ModuleCat.EnoughInjectives +public import Mathlib.Algebra.Category.ModuleCat.Ext.HasExt +public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat +public import Mathlib.CategoryTheory.Abelian.Injective.Dimension +public import Mathlib.CategoryTheory.Abelian.Injective.Resolution + +/-! + +# Baer's criterion for injective dimension + +Baer's criterion says that an `R`-module `M` is injective iff every `R`-linear map +`I →ₗ[R] M` from an ideal `I` of `R` extends to a map `R →ₗ[R] M`. + +This file reformulates that extension condition as the vanishing of `Ext (R ⧸ I) M 1`. +It then uses dimension shifting to give a criterion for injective dimension: to prove that +`M` has injective dimension `< n`, it suffices to show that `Ext (R ⧸ I) M n` vanishes for +all ideals `I`. + +The statements use `Shrink` because `R`, its ideals, and its quotients may live in a larger +universe than `ModuleCat.{v} R`. + +## Main results + +* `ModuleCat.ext_quotient_one_subsingleton_iff`: `Ext (R ⧸ I) M 1` vanishes iff every + linear map `I →ₗ[R] M` extends to `R →ₗ[R] M`. +* `ModuleCat.injective_of_subsingleton_ext_quotient_one`: if `Ext (R ⧸ I) M 1` vanishes + for all ideals `I`, then `M` is injective. +* `ModuleCat.injective_iff_subsingleton_ext_quotient_one`: if and only if version of + `ModuleCat.injective_of_subsingleton_ext_quotient_one`. +* `ModuleCat.hasInjectiveDimensionLT_of_quotients`: if `Ext (R ⧸ I) M n` vanishes for all + ideals `I`, then `M` has injective dimension `< n`. +* `ModuleCat.hasInjectiveDimensionLT_iff_quotients`: if and only if version of + `ModuleCat.hasInjectiveDimensionLT_of_quotients` + +-/ + +@[expose] public section + +universe u v + +variable {R : Type u} [CommRing R] + +open CategoryTheory Abelian + +namespace ModuleCat + +/-- The vanishing of `Ext (R ⧸ I) M 1` is equivalent to Baer's extension property +for maps `I →ₗ[R] M`. -/ +lemma ext_quotient_one_subsingleton_iff [Small.{v} R] (M : ModuleCat.{v} R) (I : Ideal R) : + Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M 1) ↔ + ∀ g : I →ₗ[R] M, ∃ g' : R →ₗ[R] M, + ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩ := by + -- The short complex `I → R → R ⧸ I`, with all three terms moved into universe `v`. + -- This avoids universe issues when comparing it with `Ext` in `ModuleCat.{v} R`. + have exact : Function.Exact I.subtype I.mkQ := LinearMap.exact_subtype_mkQ I + let S := ModuleCat.shortComplexOfConj (Shrink.linearEquiv R I) (Shrink.linearEquiv R R) + (Shrink.linearEquiv R (R ⧸ I)) _ _ exact.linearMap_comp_eq_zero + -- The complex `I → R → R ⧸ I` is short exact, after shrinking universes. + have S_exact : S.ShortExact := + ModuleCat.shortComplexOfConj_shortExact _ _ _ _ _ exact I.subtype_injective I.mkQ_surjective + rw [Ext.one_subsingleton_iff_of_projective M S S_exact (by dsimp [S]; infer_instance)] + -- Reduce the vanishing of `Ext (R ⧸ I) M 1` to surjectivity of + -- `Ext R M 0 → Ext I M 0`, keeping track of the universe-shrinking equivalences. + refine ⟨fun h ↦ fun g ↦ ?_, fun h ↦ fun e ↦ ?_⟩ + · -- Interpret `g` as an element of `Ext I M 0` and lift it across `Ext R M 0 → Ext I M 0`. + obtain ⟨f', hf'⟩ := h + (Ext.mk₀ (ModuleCat.ofHom (g.comp (Shrink.linearEquiv R I).toLinearMap))) + rw [Ext.bilinearComp_apply_apply, ← Ext.mk₀_addEquiv₀_apply f', + Ext.mk₀_comp_mk₀] at hf' + use (Ext.addEquiv₀ f').hom.comp (Shrink.linearEquiv R R).symm.toLinearMap + intro x hx + have := ConcreteCategory.congr_hom ((Ext.mk₀_bijective _ _).1 hf') + ((Shrink.linearEquiv R I).symm ⟨x, hx⟩) + simpa [S] + · -- Conversely, extend the map represented by `e` and turn the extension back into `Ext⁰`. + obtain ⟨g', hg'⟩ := h + ((Ext.addEquiv₀ e).hom.comp (Shrink.linearEquiv R I).symm.toLinearMap) + use Ext.mk₀ (ModuleCat.ofHom (g'.comp (Shrink.linearEquiv R R).toLinearMap)) + rw [Ext.bilinearComp_apply_apply, Ext.mk₀_comp_mk₀, ← Ext.mk₀_addEquiv₀_apply e] + congr + ext x + simp_all [S] + +/-- Baer's criterion in Ext form: if `Ext (R ⧸ I) M 1` vanishes for every ideal `I`, +then `M` is injective. -/ +lemma injective_of_subsingleton_ext_quotient_one [Small.{v} R] (M : ModuleCat.{v} R) + (h : ∀ (I : Ideal R), Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M 1)) : + Injective M := by + rw [← Module.injective_iff_injective_object, ← Module.Baer.iff_injective] + exact fun I ↦ (ext_quotient_one_subsingleton_iff M I).mp (h I) + +lemma injective_iff_subsingleton_ext_quotient_one [Small.{v} R] (M : ModuleCat.{v} R) : + Injective M ↔ + ∀ (I : Ideal R), Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M 1) := + ⟨fun _ _ ↦ Ext.subsingleton_of_injective _ M 0, injective_of_subsingleton_ext_quotient_one M⟩ + +attribute [local instance] Ext.subsingleton_of_injective in +open Limits in +/-- If `Ext (R ⧸ I) M (n + 1)` vanishes for every ideal `I`, then `M` has injective +dimension at most `n`. -/ +lemma hasInjectiveDimensionLE_of_quotients [Small.{v} R] (M : ModuleCat.{v} R) (n : ℕ) + (h : ∀ I : Ideal R, Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M (n + 1))) : + HasInjectiveDimensionLE M n := by + induction n generalizing M with + | zero => + -- The case `n = 0` is exactly the Ext form of Baer's criterion. + have : Injective M := injective_of_subsingleton_ext_quotient_one M h + infer_instance + | succ n ih => + -- Dimension shifting reduces the statement for `M` to + -- the cokernel of an injective presentation. + let ip : InjectivePresentation M := Classical.arbitrary _ + refine ip.shortExact_shortComplex.hasInjectiveDimensionLT_X₁ _ + (ih _ (fun I ↦ subsingleton_of_forall_eq 0 (fun x₃ ↦ ?_))) inferInstance + obtain ⟨x₂, rfl⟩ := Ext.covariant_sequence_exact₃ _ ip.shortExact_shortComplex x₃ rfl + (by subsingleton) + simp [Subsingleton.elim x₂ 0] + +/-- The zeroth Ext group from `R ⧸ ⊥` is canonically equivalent to the underlying module. -/ +private noncomputable def extQuotientBotZeroEquiv [Small.{v} R] (M : ModuleCat.{v} R) : + (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ (⊥ : Ideal R)))) M 0) ≃ M := + (Ext.homEquiv₀.trans ModuleCat.homEquiv).trans ((((Shrink.linearEquiv _ _).trans + (Submodule.quotEquivOfEqBot _ rfl)).congrLeft M R).trans + (LinearMap.ringLmapEquivSelf R R M)).toEquiv + +/-- If `Ext⁰(R ⧸ ⊥, M)` is a subsingleton, then `M` is a subsingleton. -/ +private lemma subsingleton_of_ext_quotient_bot_zero [Small.{v} R] (M : ModuleCat.{v} R) + (h : Subsingleton (Ext (of R (Shrink.{v} (R ⧸ (⊥ : Ideal R)))) M 0)) : + Subsingleton M := by + rw [← (extQuotientBotZeroEquiv (R := R) M).subsingleton_congr] + exact h + +/-- If `Ext (R ⧸ I) M n` vanishes for every ideal `I`, then `M` has injective dimension +strictly less than `n`. -/ +lemma hasInjectiveDimensionLT_of_quotients [Small.{v} R] (M : ModuleCat.{v} R) (n : ℕ) + (h : ∀ I : Ideal R, Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M n)) : + HasInjectiveDimensionLT M n := by + match n with + | 0 => + apply Limits.IsZero.hasInjectiveDimensionLT_zero + rw [ModuleCat.isZero_iff_subsingleton] + exact subsingleton_of_ext_quotient_bot_zero M (h ⊥) + | n + 1 => exact hasInjectiveDimensionLE_of_quotients M n h + +lemma hasInjectiveDimensionLT_iff_quotients [Small.{v} R] (M : ModuleCat.{v} R) (n : ℕ) : + HasInjectiveDimensionLT M n ↔ + ∀ I : Ideal R, Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M n) := + ⟨fun h _ ↦ h.subsingleton M n _ (le_refl _) _, hasInjectiveDimensionLT_of_quotients M n⟩ + +end ModuleCat diff --git a/Mathlib/Algebra/Category/ModuleCat/Ext/BaseChange.lean b/Mathlib/Algebra/Category/ModuleCat/Ext/BaseChange.lean new file mode 100644 index 00000000000000..e22c5e3f0ad85d --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Ext/BaseChange.lean @@ -0,0 +1,382 @@ +/- +Copyright (c) 2025 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.Category.Grp.Zero +public import Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting +public import Mathlib.Algebra.FiveLemma +public import Mathlib.Algebra.Module.FinitePresentation +public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Map +public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat +public import Mathlib.GroupTheory.MonoidLocalization.Basic +public import Mathlib.LinearAlgebra.Dimension.Finite +public import Mathlib.LinearAlgebra.TensorProduct.Pi +public import Mathlib.RingTheory.Localization.BaseChange +public import Mathlib.RingTheory.Flat.Localization +public import Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact + +/-! + +# Ext Commute with Flat Base Change + +The `Ext` functor over `R`-module commute with flat base change if `R` is Noethrian and two modules +are finitely generated. + +-/ + +@[expose] public section + +universe v v' u u' + +variable (R : Type u) [CommRing R] + +section basechange + +open CategoryTheory + +variable {R} (S : Type u') [CommRing S] [Algebra R S] + +section extendscalars' + +namespace ModuleCat + +instance (M N : Type*) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] + [Small.{v'} M] [Small.{v'} N] : Small.{v'} (TensorProduct R M N) := + let _ : Small.{v'} (FreeAddMonoid (M × N)) := + small_of_surjective (FreeAddMonoid.freeAddMonoidCongr (equivShrink (M × N)).symm).surjective + small_of_surjective Quotient.mk''_surjective + +/-- Auxiliary construction for `ModuleCat.ExtendScalars'.obj`, +turning an `R`-module into an `S`-module by `M` ↦ `Shrink S ⨂ M`. -/ +noncomputable def ExtendScalars'.obj' [UnivLE.{v, v'}] [Small.{v'} S] + (M : ModuleCat.{v} R) : ModuleCat.{v'} S := + ModuleCat.of S (Shrink.{v'} (TensorProduct R S M)) + +/-- Auxiliary construction for `ModuleCat.ExtendScalars'.map`, +sending `l : M1 ⟶ M2` to `s ⊗ m ↦ s ⊗ l m` with compostion of `Shrink.linearEquiv`. -/ +noncomputable def ExtendScalars'.map' [UnivLE.{v, v'}] [Small.{v'} S] + {M1 M2 : ModuleCat.{v} R} (g : M1 ⟶ M2) : obj' S M1 ⟶ obj' S M2 := + ModuleCat.ofHom (((Shrink.linearEquiv.{v'} S (TensorProduct R S M2)).symm.toLinearMap.comp + (g.hom.baseChange S)).comp (Shrink.linearEquiv.{v'} S (TensorProduct R S M1)).toLinearMap) + +lemma ExtendScalars'.map'_id [UnivLE.{v, v'}] [Small.{v'} S] + (M : ModuleCat.{v} R) : map' S (𝟙 M) = 𝟙 (obj' S M) := by + simp [map', obj'] + +lemma ExtendScalars'.map'_comp [UnivLE.{v, v'}] [Small.{v'} S] + {M1 M2 M3 : ModuleCat.{v} R} (g : M1 ⟶ M2) (h : M2 ⟶ M3) : + map' S (g ≫ h) = (map' S g) ≫ (map' S h) := by + ext x + change (Shrink.linearEquiv S (TensorProduct R S M3)).symm + (((h.hom ∘ₗ g.hom).baseChange S) ((Shrink.linearEquiv S (TensorProduct R S M1)) x)) = + (Shrink.linearEquiv S (TensorProduct R S M3)).symm ((h.hom.baseChange S) + ((Shrink.linearEquiv S (TensorProduct R S M2)) + ((Shrink.linearEquiv S (TensorProduct R S M2)).symm ((g.hom.baseChange S) + ((Shrink.linearEquiv S (TensorProduct R S M1)) x))))) + rw [LinearEquiv.apply_symm_apply] + simp [LinearMap.baseChange_comp] + +variable (R) in +/-- A version of `ModuleCat.extendScalars` with more general universe level, +turning an `R`-module into an `S`-module by `M` ↦ `Shrink S ⨂ M`, +sending `l : M1 ⟶ M2` to `s ⊗ m ↦ s ⊗ l m` with compostion of `Shrink.linearEquiv`. -/ +noncomputable def extendScalars' [UnivLE.{v, v'}] [Small.{v'} S] : + (ModuleCat.{v} R) ⥤ (ModuleCat.{v'} S) where + obj := ExtendScalars'.obj' S + map := ExtendScalars'.map' S + map_id := ExtendScalars'.map'_id S + map_comp := ExtendScalars'.map'_comp S + +variable [UnivLE.{v, v'}] [Small.{v'} S] + +set_option backward.isDefEq.respectTransparency false in +instance : (extendScalars' R S).Additive where + map_add {X Y} f g := by + simp only [extendScalars', ExtendScalars'.map', hom_add, LinearMap.baseChange_add] + ext x + simp + +set_option backward.isDefEq.respectTransparency false in +lemma extendScalars'_map_exact [Module.Flat R S] + (T : ShortComplex (ModuleCat.{v} R)) (h : T.Exact) : + (T.map (extendScalars' R S)).Exact := by + have exac : Function.Exact (T.f.hom.baseChange S) (T.g.hom.baseChange S) := + Module.Flat.lTensor_exact S + ((ShortComplex.ShortExact.moduleCat_exact_iff_function_exact T).mp h) + have : Function.Exact (ExtendScalars'.map' S T.f) (ExtendScalars'.map' S T.g) := by + simp only [ExtendScalars'.map', hom_ofHom, LinearMap.exact_iff, LinearEquiv.range_comp] + rw [LinearMap.comp_assoc, LinearEquiv.ker_comp] + ext x + simp only [LinearMap.mem_ker, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, + ModuleCat.ExtendScalars'.obj'] + convert exac ((Shrink.linearEquiv S (TensorProduct R S T.X₂)) x) + rw [LinearMap.range_comp, ← Submodule.comap_equiv_eq_map_symm, Submodule.mem_comap] + rfl + exact (ShortComplex.ShortExact.moduleCat_exact_iff_function_exact _).mpr this + +instance [Module.Flat R S] : Limits.PreservesFiniteLimits (extendScalars' R S) := by + have := (((extendScalars' R S).exact_tfae.out 1 3).mp (extendScalars'_map_exact S)) + exact this.1 + +instance [Module.Flat R S] : Limits.PreservesFiniteColimits (extendScalars' R S) := by + have := (((extendScalars' R S).exact_tfae.out 1 3).mp (extendScalars'_map_exact S)) + exact this.2 + +namespace Algebra' + +set_option backward.isDefEq.respectTransparency false in +variable (R) in +scoped instance extendScalars'_linear : + letI : Linear R (ModuleCat.{v'} S) := ModuleCat.Algebra.instLinear + Functor.Linear R (ModuleCat.extendScalars' R S) := + letI : Linear R (ModuleCat.{v'} S) := ModuleCat.Algebra.instLinear + { + map_smul {X Y} g r := by + simp only [extendScalars', ExtendScalars'.map', hom_smul, LinearMap.baseChange_smul] + let _ : IsScalarTower R S (ExtendScalars'.obj' S X ⟶ ExtendScalars'.obj' S Y) := { + smul_assoc r s z := by + rw [Algebra.smul_def, ← smul_smul] + rfl } + rw [← algebraMap_smul S r, ← algebraMap_smul S r, LinearMap.comp_smul, LinearMap.smul_comp] + rfl } + +end Algebra' + +end ModuleCat + +end extendscalars' + +section + +open Abelian + +variable [UnivLE.{v, v'}] [Small.{v} R] [Small.{v'} S] + +noncomputable instance (n : ℕ) (M N : ModuleCat.{v'} S) : Module R (Ext M N n) := + letI : Linear R (ModuleCat.{v'} S) := ModuleCat.Algebra.instLinear + inferInstance + +set_option backward.isDefEq.respectTransparency false in +instance (n : ℕ) (M N : ModuleCat.{v'} S) : IsScalarTower R S (Ext M N n) where + smul_assoc r s z := by + simp only [Ext.smul_eq_comp_mk₀, Ext.comp_assoc_of_second_deg_zero, Ext.mk₀_comp_mk₀, + Linear.comp_smul, Category.comp_id] + rw [Algebra.smul_def, ← smul_smul] + rfl + +instance (M N : ModuleCat.{v'} S) : Module R (M ⟶ N) := + letI : Linear R (ModuleCat.{v'} S) := ModuleCat.Algebra.instLinear + inferInstance + +set_option backward.isDefEq.respectTransparency false in +instance (M N : ModuleCat.{v'} S) : IsScalarTower R S (M ⟶ N) where + smul_assoc r s x := by + rw [Algebra.smul_def, ← smul_smul] + rfl + +/-- The separate definition of `(ModuleCat.extendScalars' R S).mapLinearMap` +to avoid some instance in namespace `ModuleCat.Algebra`. -/ +noncomputable def ModuleCat.extendScalars'.mapLinearMap (M N : ModuleCat.{v} R) : + (M ⟶ N) →ₗ[R] ((ModuleCat.extendScalars'.{v, v'} R S).obj M ⟶ + (ModuleCat.extendScalars'.{v, v'} R S).obj N) := + letI : Linear R (ModuleCat.{v'} S) := ModuleCat.Algebra.instLinear + letI := ModuleCat.Algebra'.extendScalars'_linear.{v, v'} R S + (ModuleCat.extendScalars'.{v, v'} R S).mapLinearMap R (X := M) (Y := N) + +omit [Small.{v} R] in +lemma ModuleCat.extendScalars'.mapLinearMap_eq_mapAddHom (M N : ModuleCat.{v} R) : + extendScalars'.mapLinearMap.{v, v'} S M N = + (ModuleCat.extendScalars'.{v, v'} R S).mapAddHom (X := M) (Y := N) := rfl + +set_option backward.isDefEq.respectTransparency false in +omit [Small.{v} R] in +lemma ModuleCat.isBaseChange_hom [Module.Flat R S] + (M N : ModuleCat.{v} R) [Module.FinitePresentation R M] : + IsBaseChange S (ModuleCat.extendScalars'.mapLinearMap.{v, v'} S M N) := by + let _ : SMulCommClass S R (Shrink.{v', max v u'} (TensorProduct R S N)) := + Equiv.smulCommClass S R (equivShrink (TensorProduct R S ↑N)).symm + let hmod : Module R (Shrink.{v'} (TensorProduct R S M) →ₗ[S] Shrink.{v'} (TensorProduct R S N)) := + LinearMap.module + let _ : Module R (((ModuleCat.extendScalars'.{v, v'} R S).obj M) →ₗ[S] + ((ModuleCat.extendScalars'.{v, v'} R S).obj N)) := hmod + let hsca : IsScalarTower R S + (Shrink.{v'} (TensorProduct R S M) →ₗ[S] Shrink.{v'} (TensorProduct R S N)) := { + smul_assoc r s x := by + ext + simp } + let _ : IsScalarTower R S (((ModuleCat.extendScalars'.{v, v'} R S).obj M) →ₗ[S] + ((ModuleCat.extendScalars'.{v, v'} R S).obj N)) := hsca + have : ModuleCat.extendScalars'.mapLinearMap.{v, v'} S M N = + ((ModuleCat.homLinearEquiv (S := S)).symm.restrictScalars R).toLinearMap.comp + (((((Shrink.linearEquiv.{v'} S (TensorProduct R S N)).symm.congrRight).trans + ((Shrink.linearEquiv.{v'} S (TensorProduct R S M)).symm.congrLeft (Shrink.{v'} + (TensorProduct R S N)) S)).restrictScalars R).toLinearMap.comp + ((LinearMap.baseChangeHom R S M N).comp ModuleCat.homLinearEquiv.toLinearMap)) := rfl + rw [this] + apply (IsBaseChange.comp _ (IsBaseChange.ofEquiv _)).comp (IsBaseChange.ofEquiv _) + exact (Module.FinitePresentation.isBaseChange_map R M N S).comp_equiv _ _ + +/-- The map between `Ext` induced by `ModuleCat.extendScalars' R S`, +separated out to avoid some instance in namespace `ModuleCat.Algebra`. -/ +noncomputable def ModuleCat.extendScalars'.mapExtLinearMap [Module.Flat R S] + (M N : ModuleCat.{v} R) (n : ℕ) : + Ext M N n →ₗ[R] Ext ((ModuleCat.extendScalars'.{v, v'} R S).obj M) + ((ModuleCat.extendScalars'.{v, v'} R S).obj N) n := + letI : Linear R (ModuleCat.{v'} S) := ModuleCat.Algebra.instLinear + letI := ModuleCat.Algebra'.extendScalars'_linear.{v, v'} R S + ((ModuleCat.extendScalars'.{v, v'} R S).mapExtLinearMap R M N n) + +lemma ModuleCat.extendScalars'.mapExtLinearMap_eq_mapExt [Module.Flat R S] + (M N : ModuleCat.{v} R) (n : ℕ) : ⇑(extendScalars'.mapExtLinearMap.{v, v'} S M N n) = + Ext.mapExactFunctor (ModuleCat.extendScalars'.{v, v'} R S) := rfl + +open ModuleCat + +set_option backward.isDefEq.respectTransparency false in +theorem CategoryTheory.Abelian.Ext.isBaseChange_aux [IsNoetherianRing R] [Module.Flat R S] + (M N : ModuleCat.{v} R) [Module.Finite R M] (n : ℕ) : + IsBaseChange S (extendScalars'.mapExtLinearMap.{v, v'} S M N n) := by + induction n generalizing M N + · have : Module.FinitePresentation R M := Module.finitePresentation_of_finite R M + have isb : IsBaseChange S (extendScalars'.mapLinearMap.{v, v'} S M N) := + ModuleCat.isBaseChange_hom.{v, v'} S M N + convert! ((IsBaseChange.ofEquiv linearEquiv₀).comp isb).comp + (IsBaseChange.ofEquiv linearEquiv₀.symm) + ext x + rcases (Ext.mk₀_bijective M N).2 x with ⟨y, hy⟩ + simp only [← hy, extendScalars'.mapExtLinearMap_eq_mapExt, mapExactFunctor_mk₀, linearEquiv₀, + addEquiv₀, homEquiv₀, AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, + AddEquiv.coe_mk, Equiv.invFun_as_coe, AddEquiv.coe_toEquiv_symm, AddEquiv.symm_mk, + Equiv.symm_symm, LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, + LinearEquiv.coe_symm_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, + Equiv.ofBijective_symm_apply_apply, Equiv.ofBijective_apply] + congr 1 + · rename_i n ih _ + rcases Module.exists_finite_presentation R M with ⟨L, _, _, _, _, f, surjf⟩ + let T : ShortComplex (ModuleCat.{v} R) := f.shortComplexKer + have T_exact : T.ShortExact := LinearMap.shortExact_shortComplexKer surjf + let TS := (T.map (ModuleCat.extendScalars'.{v, v'} R S)) + have TS_exact : TS.ShortExact := T_exact.map_of_exact (ModuleCat.extendScalars'.{v, v'} R S) + have : Module.Free S TS.X₂ := + Module.Free.of_equiv (Shrink.linearEquiv S (TensorProduct R S T.X₂)).symm + let NS := ((ModuleCat.extendScalars'.{v, v'} R S).obj N) + let f : Ext T.X₂ N n →ₗ[R] Ext T.X₁ N n := { + __ := (mk₀ T.f).precomp N (zero_add n) + map_smul' r x := by simp } + let g : Ext T.X₁ N n →ₗ[R] Ext T.X₃ N (n + 1) := { + __ := T_exact.extClass.precomp N (add_comm 1 n) + map_smul' r x := by simp } + have exac1 : Function.Exact f g := (ShortComplex.ab_exact_iff_function_exact _).mp + (Ext.contravariant_sequence_exact₁' T_exact N n (n + 1) (add_comm 1 n)) + have surj1 : Function.Surjective g := + precomp_extClass_surjective_of_projective_X₂ N T_exact n + let f' : Ext TS.X₂ NS n →ₗ[S] Ext TS.X₁ NS n := { + __ := (mk₀ TS.f).precomp NS (zero_add n) + map_smul' s x := by simp } + let g' : Ext TS.X₁ NS n →ₗ[S] Ext TS.X₃ NS (n + 1) := { + __ := TS_exact.extClass.precomp NS (add_comm 1 n) + map_smul' s x := by simp } + have exac2 : Function.Exact f' g' := (ShortComplex.ab_exact_iff_function_exact _).mp + (Ext.contravariant_sequence_exact₁' TS_exact NS n (n + 1) (add_comm 1 n)) + have surj2 : Function.Surjective g' := + precomp_extClass_surjective_of_projective_X₂ NS TS_exact n + let h₁ : Ext T.X₂ N n →ₗ[R] Ext TS.X₂ NS n := extendScalars'.mapExtLinearMap.{v, v'} S T.X₂ N n + let h₂ : Ext T.X₁ N n →ₗ[R] Ext TS.X₁ NS n := extendScalars'.mapExtLinearMap.{v, v'} S T.X₁ N n + let h₃ : Ext T.X₃ N (n + 1) →ₗ[R] Ext TS.X₃ NS (n + 1) := + extendScalars'.mapExtLinearMap.{v, v'} S T.X₃ N (n + 1) + apply IsBaseChange.of_right_exact S h₁ h₂ h₃ _ _ (ih T.X₂ N) (ih T.X₁ N) exac1 surj1 exac2 surj2 + · ext x + simp only [ShortComplex.map, ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, + LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, f, f', + bilinearComp_apply_apply, ← mapExactFunctor_mk₀, LinearMap.coe_restrictScalars, TS, h₁, h₂] + rw [extendScalars'.mapExtLinearMap_eq_mapExt, extendScalars'.mapExtLinearMap_eq_mapExt, + Ext.mapExactFunctor_comp] + · ext x + simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, + LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, + bilinearComp_apply_apply, LinearMap.coe_restrictScalars, h₃, g, g', h₂] + rw [← Ext.mapExactFunctor_extClass (ModuleCat.extendScalars'.{v, v'} R S) T_exact] + exact Ext.mapExactFunctor_comp (ModuleCat.extendScalars'.{v, v'} R S) _ x (add_comm 1 n) + +/-- If `MS` in `ModuleCat S` is base change of an `R`-module `M`, +then it is isomporhic to `(ModuleCat.extendScalars' R S).obj M`. -/ +noncomputable def ModuleCat.isoExtendScalars'OfIsBaseChange' {M : ModuleCat.{v} R} + {MS : ModuleCat.{v'} S} [Module R MS] [IsScalarTower R S MS] (f : M →ₗ[R] MS) + (isb1 : IsBaseChange S f) : MS ≅ (ModuleCat.extendScalars'.{v, v'} R S).obj M := + (isb1.equiv.symm.trans (Shrink.linearEquiv S (TensorProduct R S M)).symm).toModuleIso + +namespace CategoryTheory.Abelian + +set_option backward.defeqAttrib.useBackward true in +set_option backward.isDefEq.respectTransparency false in +/-- The isomprohism on `Ext` induced by `ModuleCat.isoExtendScalars'OfIsBaseChange'`. -/ +noncomputable def Ext.isBaseChangeMapAux {M N : ModuleCat.{v} R} + {MS NS : ModuleCat.{v'} S} [Module R MS] [IsScalarTower R S MS] + [Module R NS] [IsScalarTower R S NS] (f : M →ₗ[R] MS) (isb1 : IsBaseChange S f) + (g : N →ₗ[R] NS) (isb2 : IsBaseChange S g) (n : ℕ) : + Ext ((ModuleCat.extendScalars'.{v, v'} R S).obj M) + ((ModuleCat.extendScalars'.{v, v'} R S).obj N) n ≃ₗ[S] Ext MS NS n := { + __ := (((extFunctorObj ((ModuleCat.extendScalars'.{v, v'} R S).obj M) n).mapIso + (isoExtendScalars'OfIsBaseChange' S g isb2).symm).trans (((extFunctor n).mapIso + (isoExtendScalars'OfIsBaseChange' S f isb1).op).app NS)).addCommGroupIsoToAddEquiv + map_smul' s x := by simp [Iso.addCommGroupIsoToAddEquiv] } + +/-- Compostion of `Ext.isBaseChangeMapAux` and `ModuleCat.extendScalars'.mapExtLinearMap`. -/ +noncomputable def Ext.isBaseChangeMap [Module.Flat R S] {M N : ModuleCat.{v} R} + {MS NS : ModuleCat.{v'} S} [Module R MS] [IsScalarTower R S MS] + [Module R NS] [IsScalarTower R S NS] (f : M →ₗ[R] MS) (isb1 : IsBaseChange S f) + (g : N →ₗ[R] NS) (isb2 : IsBaseChange S g) (n : ℕ) : Ext M N n →ₗ[R] Ext MS NS n := + ((Ext.isBaseChangeMapAux S f isb1 g isb2 n).restrictScalars R).toLinearMap.comp + (extendScalars'.mapExtLinearMap.{v, v'} S M N n) + +theorem Ext.isBaseChange [IsNoetherianRing R] [Module.Flat R S] (M N : ModuleCat.{v} R) + [Module.Finite R M] {MS NS : ModuleCat.{v'} S} + [Module R MS] [IsScalarTower R S MS] [Module R NS] [IsScalarTower R S NS] + (f : M →ₗ[R] MS) (isb1 : IsBaseChange S f) + (g : N →ₗ[R] NS) (isb2 : IsBaseChange S g) + (n : ℕ) : IsBaseChange S (Ext.isBaseChangeMap.{v, v'} S f isb1 g isb2 n) := + (Ext.isBaseChange_aux.{v, v'} S M N n).comp + (IsBaseChange.ofEquiv (isBaseChangeMapAux S f isb1 g isb2 n)) + +end CategoryTheory.Abelian + +end + +end basechange + +section Localization + +namespace CategoryTheory.Abelian + +open ModuleCat + +variable (S : Submonoid R) (A : Type u') [CommRing A] [Algebra R A] [IsLocalization S A] + +variable [UnivLE.{v, v'}] [Small.{v} R] [Small.{v'} A] + +variable {R} + +/-- `Ext.isBaseChangeMap` specifying to localization. -/ +noncomputable def Ext.isLocalizedModuleMap {M N : ModuleCat.{v} R} {MS NS : ModuleCat.{v'} A} + [Module R MS] [IsScalarTower R A MS] [Module R NS] [IsScalarTower R A NS] + (f : M →ₗ[R] MS) (isl1 : IsLocalizedModule S f) (g : N →ₗ[R] NS) (isl2 : IsLocalizedModule S g) + (n : ℕ) : Ext M N n →ₗ[R] Ext MS NS n := + haveI := IsLocalization.flat A S + (Ext.isBaseChangeMap.{v, v'} A f (IsLocalizedModule.isBaseChange S A f) g + (IsLocalizedModule.isBaseChange S A g) n) + +theorem Ext.isLocalizedModule [IsNoetherianRing R] {M N : ModuleCat.{v} R} + [Module.Finite R M] {MS NS : ModuleCat.{v'} A} + [Module R MS] [IsScalarTower R A MS] [Module R NS] [IsScalarTower R A NS] + (f : M →ₗ[R] MS) (isl1 : IsLocalizedModule S f) (g : N →ₗ[R] NS) (isl2 : IsLocalizedModule S g) + (n : ℕ) : IsLocalizedModule S (Ext.isLocalizedModuleMap.{v, v'} S A f isl1 g isl2 n) := + haveI := IsLocalization.flat A S + (isLocalizedModule_iff_isBaseChange S A _).mpr (Ext.isBaseChange.{v, v'} A M N + f (IsLocalizedModule.isBaseChange S A f) g (IsLocalizedModule.isBaseChange S A g) n) + +end CategoryTheory.Abelian + +end Localization diff --git a/Mathlib/Algebra/Category/ModuleCat/Ext/RingEquiv.lean b/Mathlib/Algebra/Category/ModuleCat/Ext/RingEquiv.lean new file mode 100644 index 00000000000000..c6ed3d4ed37645 --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Ext/RingEquiv.lean @@ -0,0 +1,86 @@ +/- +Copyright (c) 2025 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.Category.ModuleCat.ChangeOfRingsExact +public import Mathlib.Algebra.Category.ModuleCat.Ext.HasExt +public import Mathlib.Algebra.Category.ModuleCat.Ulift +public import Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective + +/-! + +# Ext Commute with Ulift Functor + +In this file, we prove `Ext` commute with ulift functor, then use this to obtain +compatibility of `Ext` with (semi) linear equiv of general universe level. + +-/ + +@[expose] public section + +universe u u' v v' + +variable {R : Type u} [CommRing R] + +open CategoryTheory Abelian + +variable {R' : Type u'} [CommRing R'] + +variable (e : R ≃+* R') + +namespace ModuleCat + +attribute [local instance] RingHomInvPair.of_ringEquiv + +set_option backward.isDefEq.respectTransparency false in +/-- The forward function of `ModuleCat.extRestrictScalarsSemiLinearEquiv`. -/ +noncomputable def extRestrictScalarsSemiLinearMap [Small.{v} R] [Small.{v} R'] + (M N : ModuleCat.{v} R') (n : ℕ) : Ext M N n →ₛₗ[RingHomClass.toRingHom e.symm] + Ext ((ModuleCat.restrictScalars (RingHomClass.toRingHom e)).obj M) + ((ModuleCat.restrictScalars (RingHomClass.toRingHom e)).obj N) n where + __ := (ModuleCat.restrictScalars.{v} (RingHomClass.toRingHom e)).mapExtAddHom M N n + map_smul' r x := by + simp only [Functor.mapExtAddHom, Ext.smul_eq_comp_mk₀, Ext.mapExactFunctor_comp, + Ext.mapExactFunctor_mk₀] + congr 2 + ext + simp + +lemma extRestrictScalarsSemiLinearMap_toAddMonoidHom [Small.{v} R] [Small.{v} R'] + (M N : ModuleCat.{v} R') (n : ℕ) : extRestrictScalarsSemiLinearMap e M N n = + (ModuleCat.restrictScalars.{v} (RingHomClass.toRingHom e)).mapExtAddHom M N n := + rfl + +/-- For `R'` module `M N` and ring isomorphism `R ≃+* R'`, +the semi-linear equivalence `Ext (↑R M) (↑R N) n ≃ Ext M N n` -/ +noncomputable def extRestrictScalarsSemiLinearEquiv [Small.{v} R] [Small.{v} R'] + (M N : ModuleCat.{v} R') (n : ℕ) : Ext M N n ≃ₛₗ[RingHomClass.toRingHom e.symm] + Ext ((ModuleCat.restrictScalars (RingHomClass.toRingHom e)).obj M) + ((ModuleCat.restrictScalars (RingHomClass.toRingHom e)).obj N) n := + haveI : (restrictScalars (RingHomClass.toRingHom e)).IsEquivalence := + restrictScalars_isEquivalence_of_ringEquiv e + LinearEquiv.ofBijective (ModuleCat.extRestrictScalarsSemiLinearMap e M N n) + (Functor.mapExt_bijective_of_preservesProjectiveObjects + (ModuleCat.restrictScalars.{v} (RingHomClass.toRingHom e)) M N n) + +set_option backward.defeqAttrib.useBackward true in +set_option backward.isDefEq.respectTransparency false in +/-- Given semi linear equivalence `M ≃ M'` and `N ≃ N'` with respect to `R ≃+* R'` +within same universe, the semi linear equivalence `Ext M N n ≃ Ext M' N' n`. -/ +noncomputable def extSemiLinearEquivOfSemiLinearEquiv [Small.{v} R] [Small.{v} R'] + {M N : ModuleCat.{v} R} {M' N' : ModuleCat.{v} R'} + (e1 : M ≃ₛₗ[RingHomClass.toRingHom e] M') (e2 : N ≃ₛₗ[RingHomClass.toRingHom e] N') + (n : ℕ) : Ext M' N' n ≃ₛₗ[RingHomClass.toRingHom e.symm] Ext M N n := + let e3 : Ext ((ModuleCat.restrictScalars (RingHomClass.toRingHom e)).obj M') + ((ModuleCat.restrictScalars (RingHomClass.toRingHom e)).obj N') n ≃ₗ[R] Ext M N n := { + __ := ((((extFunctor n).obj + ⟨(ModuleCat.restrictScalars (RingHomClass.toRingHom e)).obj M'⟩).mapIso + (ModuleCat.isoRestrictScalars e e2).symm).trans (((extFunctor n).mapIso + (ModuleCat.isoRestrictScalars e e1).op).app N)).addCommGroupIsoToAddEquiv + map_smul' r' x := by simp [Iso.addCommGroupIsoToAddEquiv] } + (ModuleCat.extRestrictScalarsSemiLinearEquiv e M' N' n).trans e3 + +end ModuleCat diff --git a/Mathlib/Algebra/Category/ModuleCat/InjectiveDimension.lean b/Mathlib/Algebra/Category/ModuleCat/InjectiveDimension.lean new file mode 100644 index 00000000000000..854fb403eb650d --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/InjectiveDimension.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2025 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.Category.ModuleCat.Ext.Baer +public import Mathlib.Algebra.Category.ModuleCat.Ext.RingEquiv +public import Mathlib.RingTheory.Ideal.Quotient.Operations + +/-! + +# Injective Dimension in ModuleCat + +-/ + +@[expose] public section + +universe u u' v + +variable {R : Type u} [CommRing R] + +open CategoryTheory Abelian + +namespace CategoryTheory + +section + +variable {R' : Type u'} [CommRing R'] (e : R ≃+* R') + +attribute [local instance] RingHomInvPair.of_ringEquiv + +lemma hasInjectiveDimensionLT_of_semiLinearEquiv [Small.{v} R] [Small.{v} R'] + {M : ModuleCat.{v} R} {N : ModuleCat.{v} R'} + (e' : M ≃ₛₗ[RingHomClass.toRingHom e] N) (n : ℕ) [HasInjectiveDimensionLT M n] : + HasInjectiveDimensionLT N n := by + apply ModuleCat.hasInjectiveDimensionLT_of_quotients N n (fun I ↦ ?_) + let e''' : (R ⧸ (I.comap e)) ≃ₛₗ[RingHomClass.toRingHom e] (R' ⧸ I) := { + __ := Ideal.quotientEquiv (I.comap e) I e (I.map_comap_eq_self_of_equiv e).symm + map_smul' r x := by + rcases Ideal.Quotient.mk_surjective x with ⟨y, hy⟩ + simp [Ideal.quotientMap, ← hy, Algebra.smul_def] } + let e'' : (ModuleCat.of R (Shrink.{v} (R ⧸ (I.comap e)))) ≃ₛₗ[RingHomClass.toRingHom e] + (ModuleCat.of R' (Shrink.{v} (R' ⧸ I))) := + ((Shrink.linearEquiv.{v} R _).trans e''').trans (Shrink.linearEquiv.{v} R' _).symm + rw [(ModuleCat.extSemiLinearEquivOfSemiLinearEquiv e e'' e' n).subsingleton_congr] + exact HasInjectiveDimensionLT.subsingleton.{v} M n n (le_refl _) _ + +lemma injectiveDimension_eq_of_semiLinearEquiv [Small.{v} R] [Small.{v} R'] + {M : ModuleCat.{v} R} {N : ModuleCat.{v} R'} + (e' : M ≃ₛₗ[RingHomClass.toRingHom e] N) : + injectiveDimension M = injectiveDimension N := by + refine eq_of_forall_ge_iff (fun N ↦ ?_) + induction N with + | bot => simpa [injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using + e'.subsingleton_congr + | coe n => + induction n with + | top => simp + | coe n => + norm_cast + simp only [injectiveDimension_le_iff] + refine ⟨fun h ↦ hasInjectiveDimensionLT_of_semiLinearEquiv e e' (n + 1), + fun h ↦ hasInjectiveDimensionLT_of_semiLinearEquiv e.symm e'.symm (n + 1)⟩ + +end + +end CategoryTheory diff --git a/Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean b/Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean index ee9256913f59a8..6d1910ab17c467 100644 --- a/Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean +++ b/Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean @@ -110,6 +110,20 @@ lemma subsingleton_of_projective [HasExt.{w} C] (P Y : C) [Projective P] (n : ℕ) : Subsingleton (Ext.{w} P Y (n + 1)) := subsingleton_of_forall_eq 0 Ext.eq_zero_of_projective +attribute [local instance] Ext.subsingleton_of_projective in +/-- For a short exact complex whose middle object is projective, the vanishing of +`Ext S.X₃ M 1` is equivalent to surjectivity of precomposition along `S.f` on `Ext⁰`. -/ +lemma one_subsingleton_iff_of_projective [HasExt.{w} C] (X : C) + (S : ShortComplex C) (S_exact : S.ShortExact) (proj : Projective S.X₂) : + Subsingleton (Ext S.X₃ X 1) ↔ + Function.Surjective ((Ext.mk₀ S.f).precomp X (add_zero 0)) := by + refine ⟨fun h x₁ ↦ Ext.contravariant_sequence_exact₁ S_exact _ x₁ (add_zero _) + (by subsingleton), fun h ↦ subsingleton_of_forall_eq 0 (fun x₃ ↦ ?_)⟩ + obtain ⟨x₁, rfl⟩ := Ext.contravariant_sequence_exact₃ S_exact _ x₃ + (by subsingleton) (add_zero 1) + obtain ⟨x₂, rfl⟩ := h x₁ + simp + end Abelian.Ext variable (C) diff --git a/Mathlib/Algebra/Module/FinitePresentation.lean b/Mathlib/Algebra/Module/FinitePresentation.lean index 71029470069912..722f1e22346524 100644 --- a/Mathlib/Algebra/Module/FinitePresentation.lean +++ b/Mathlib/Algebra/Module/FinitePresentation.lean @@ -7,8 +7,11 @@ module public import Mathlib.LinearAlgebra.FreeModule.Finite.Basic public import Mathlib.LinearAlgebra.Isomorphisms +public import Mathlib.LinearAlgebra.LeftExact +public import Mathlib.LinearAlgebra.TensorProduct.Pi public import Mathlib.LinearAlgebra.TensorProduct.RightExactness public import Mathlib.RingTheory.Finiteness.Projective +public import Mathlib.RingTheory.Flat.IsBaseChange public import Mathlib.RingTheory.Localization.BaseChange public import Mathlib.RingTheory.Noetherian.Basic public import Mathlib.RingTheory.TensorProduct.Finite @@ -92,6 +95,16 @@ theorem Module.FinitePresentation.exists_fin [fp : Module.FinitePresentation R M · simpa [range_linearCombination] using hι₁ · simpa [LinearMap.ker_comp, Submodule.comap_equiv_eq_map_symm] using hι₂.map _ +/-- An alternative version of `Module.FinitePresentation.exists_fin` that provides a right exact +sequence. -/ +theorem Module.FinitePresentation.exists_fin' [fp : Module.FinitePresentation R M] : + ∃ (n m : ℕ) (f : (Fin n → R) →ₗ[R] M) (g : (Fin m → R) →ₗ[R] (Fin n → R)), + Function.Surjective f ∧ Function.Exact g f := by + obtain ⟨n, K, e, h⟩ := exists_fin R M + obtain ⟨m, g', hg'⟩ := K.fg_iff_exists_fin_linearMap.mp h + refine ⟨n, m, e.symm ∘ₗ K.mkQ, g', by simpa using K.mkQ_surjective, + e.symm.injective.comp_exact_iff_exact.mpr (LinearMap.exact_iff.mpr (by simpa using hg'.symm))⟩ + /-- A finitely presented module is isomorphic to the quotient of a finite free module by a finitely generated submodule. -/ theorem Module.FinitePresentation.equiv_quotient [Module.FinitePresentation R M] [Small.{v} R] : @@ -652,4 +665,39 @@ lemma Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply (LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f := IsLocalizedModule.linearEquiv_symm_apply S _ _ f +open TensorProduct LinearMap + +variable (N) in +lemma Module.isBaseChange_map_of_finite_free (S : Type*) [CommRing S] [Algebra R S] (n : ℕ) : + IsBaseChange S (LinearMap.baseChangeHom R S (Fin n → R) N) := by + let e₁ := TensorProduct.piRight R S S (fun _ : Fin n ↦ R) + let e₂ := (LinearEquiv.piCongrRight (fun _ ↦ (LinearMap.ringLmapEquivSelf S S _).symm ≪≫ₗ + (LinearEquiv.congrLeft (S ⊗[R] N) S (AlgebraTensorModule.rid R S S).symm))) ≪≫ₗ + (LinearMap.lsum S (fun _ : Fin n ↦ _) S) ≪≫ₗ (e₁.symm.congrLeft (S ⊗[R] N) S) + let e₃ := (LinearMap.lsum R (fun _ : Fin n ↦ R) R).symm ≪≫ₗ + LinearEquiv.piCongrRight (fun _ ↦ LinearMap.ringLmapEquivSelf R R N) + refine IsBaseChange.of_equiv ((e₃.baseChange R S) ≪≫ₗ (TensorProduct.piRight R S S _) ≪≫ₗ e₂) + (fun f ↦ TensorProduct.AlgebraTensorModule.curry_injective (LinearMap.ext fun s ↦ ?_)) + ext i + simpa [e₃, e₂, e₁] using (tmul_eq_smul_one_tmul s (f (Pi.single i 1))).symm + +variable (R M N) in +theorem Module.FinitePresentation.isBaseChange_map (S : Type*) [CommRing S] [Algebra R S] + [Module.Flat R S] [Module.FinitePresentation R M] : + IsBaseChange S (LinearMap.baseChangeHom R S M N) := by + obtain ⟨n, m, f, g, hf, hfg⟩ := Module.FinitePresentation.exists_fin' R M + refine IsBaseChange.of_left_exact S (f' := (f.baseChange S).lcomp S (S ⊗[R] N)) + (g' := (g.baseChange S).lcomp S (S ⊗[R] N)) _ _ _ ?_ ?_ + (Module.isBaseChange_map_of_finite_free N S n) (Module.isBaseChange_map_of_finite_free N S m) + (exact_lcomp_of_exact_of_surjective _ hfg hf) (lcomp_injective_of_surjective f hf) ?_ ?_ + · exact LinearMap.ext fun φ ↦ TensorProduct.AlgebraTensorModule.curry_injective + (LinearMap.ext fun s ↦ (LinearMap.ext fun m ↦ (by simp))) + · exact LinearMap.ext fun φ ↦ TensorProduct.AlgebraTensorModule.curry_injective + (LinearMap.ext fun s ↦ (LinearMap.ext fun m ↦ (by simp))) + · apply exact_lcomp_of_exact_of_surjective + · exact lTensor_exact S hfg hf + · exact LinearMap.lTensor_surjective S hf + · apply lcomp_injective_of_surjective + exact LinearMap.lTensor_surjective S hf + end CommRing diff --git a/Mathlib/RingTheory/AdicCompletion/Noetherian.lean b/Mathlib/RingTheory/AdicCompletion/Noetherian.lean index 7a8ce2532f00e8..e7f44ad13c9c49 100644 --- a/Mathlib/RingTheory/AdicCompletion/Noetherian.lean +++ b/Mathlib/RingTheory/AdicCompletion/Noetherian.lean @@ -1,13 +1,18 @@ /- Copyright (c) 2024 Andrew Yang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Andrew Yang +Authors: Andrew Yang, Nailin Guan -/ module -public import Mathlib.RingTheory.AdicCompletion.Basic +public import Mathlib.RingTheory.AdicCompletion.AsTensorProduct +public import Mathlib.RingTheory.AdicCompletion.LocalRing public import Mathlib.RingTheory.Filtration +public import Mathlib.RingTheory.FiniteStability public import Mathlib.RingTheory.HopkinsLevitzki +public import Mathlib.RingTheory.Ideal.KrullsHeightTheorem +public import Mathlib.RingTheory.Ideal.Quotient.Noetherian +public import Mathlib.RingTheory.KrullDimension.Basic /-! # Hausdorff-ness for Noetherian rings @@ -17,7 +22,14 @@ public section open IsLocalRing Module -variable {R : Type*} [CommRing R] (I : Ideal R) (M : Type*) [AddCommGroup M] [Module R M] +universe u + +variable {R : Type u} [CommRing R] (I : Ideal R) + +section + +variable (M : Type*) [AddCommGroup M] [Module R M] + variable [IsNoetherianRing R] [Module.Finite R M] lemma IsHausdorff.of_le_jacobson (h : I ≤ Ideal.jacobson ⊥) : IsHausdorff I M := @@ -35,6 +47,8 @@ lemma IsHausdorff.of_isTorsionFree [IsDomain R] [IsTorsionFree R M] (h : I ≠ theorem IsHausdorff.of_isDomain [IsDomain R] (h : I ≠ ⊤) : IsHausdorff I R := .of_isTorsionFree I R h +end + instance (priority := 100) {A : Type*} [CommRing A] [IsArtinianRing A] [IsLocalRing A] : IsAdicComplete (IsLocalRing.maximalIdeal A) A where prec' f hf := by @@ -45,3 +59,201 @@ instance (priority := 100) {A : Type*} [CommRing A] [IsArtinianRing A] [IsLocalR specialize hf (show n ≤ m by lia) rw [hn, zero_smul, Ideal.zero_eq_bot, SModEq.bot] at hf rw [hf] + +open Polynomial + +/-- The canonical morphism from `reesAlgebra` to associated graded ring. -/ +noncomputable abbrev reesAlgebraToAssociatedGraded : + (reesAlgebra I) →+* (reesAlgebra I) ⧸ I.map (algebraMap R (reesAlgebra I)) := + Ideal.Quotient.mk (I.map (algebraMap R (reesAlgebra I))) + +/-- The ideal `⨁ i, J ⊓ Iⁱ / J ⊓ Iⁱ⁺¹` corresponding to an ideal `J` of `R`. -/ +noncomputable abbrev Ideal.toAssociatedGraded (J I : Ideal R) : + Ideal ((reesAlgebra I) ⧸ (I.map (algebraMap R (reesAlgebra I)))) := + ((J.map Polynomial.C).comap (reesAlgebra I).val).map (reesAlgebraToAssociatedGraded I) + +lemma exists_monomial_span_of_fg (J : Ideal R) (fg : (J.toAssociatedGraded I).FG) : + ∃ (ι : Type u) (f : ι → reesAlgebra I) (deg : ι → ℕ) (coeff : ι → R), Finite ι ∧ + (∀ i : ι, (f i).1 = monomial (deg i) (coeff i)) ∧ (∀ i : ι, coeff i ∈ J) ∧ + (Ideal.span (Set.range f)).map (reesAlgebraToAssociatedGraded I) = + J.toAssociatedGraded I := by + obtain ⟨s, hs⟩ := fg + have smem : ∀ x ∈ s, x ∈ J.toAssociatedGraded I := fun x hx ↦ by + simpa [← hs] using Ideal.subset_span hx + have : (J.toAssociatedGraded I).comap (reesAlgebraToAssociatedGraded I) = _ := + (Ideal.comap_map_of_surjective' (reesAlgebraToAssociatedGraded I) Ideal.Quotient.mk_surjective + ((J.map Polynomial.C).comap (reesAlgebra I).val)).trans (sup_comm _ _) + let g : s → reesAlgebra I := fun x ↦ Classical.choose + (Ideal.exists_of_comap_eq_ker_sup _ Ideal.Quotient.mk_surjective this (smem x.1 x.2)) + have g_spec (x : s) : g x ∈ _ ∧ reesAlgebraToAssociatedGraded I (g x) = x := Classical.choose_spec + (Ideal.exists_of_comap_eq_ker_sup _ Ideal.Quotient.mk_surjective this (smem x.1 x.2)) + let ι := Sigma (fun (x : s) ↦ (g x).1.support) + let deg : ι → ℕ := fun ⟨i, j⟩ ↦ j + let coeff : ι → R := fun ⟨i, j⟩ ↦ (g i).1.coeff j.1 + have monomial_mem (i : ι) : monomial (deg i) (coeff i) ∈ reesAlgebra I := by + match i with + | ⟨i, j⟩ => exact reesAlgebra.monomial_mem.mpr ((mem_reesAlgebra_iff I _).mp (g i).2 j) + have monomial_mem' (i : ι) : monomial (deg i) (coeff i) ∈ J.map C := by + match i with + | ⟨i, j⟩ => + rw [Ideal.mem_map_C_iff] + intro n + by_cases eq : n = deg ⟨i, j⟩ + · have := (g_spec i).1 + simp only [Ideal.mem_comap, Subalgebra.coe_val, Ideal.mem_map_C_iff] at this + simpa [eq, coeff] using this j + · simp [coeff_monomial_of_ne _ eq] + let f : ι → reesAlgebra I := fun i ↦ ⟨monomial (deg i) (coeff i), monomial_mem i⟩ + use ι, f, deg, coeff + refine ⟨inferInstance, fun i ↦ rfl, fun ⟨i, j⟩ ↦ ?_, le_antisymm ?_ ?_⟩ + · have := (g_spec i).1 + simp only [Ideal.mem_comap, Subalgebra.coe_val, Ideal.mem_map_C_iff] at this + exact this j + · simp only [Ideal.map_span, Ideal.span_le, Set.image_subset_iff] + rintro x ⟨y, hy⟩ + apply Ideal.mem_map_of_mem + simpa [← hy] using monomial_mem' y + · simp only [← hs, Ideal.span_le] + intro x hx + have : _ = x := (g_spec ⟨x, hx⟩).2 + rw [← this] + apply Ideal.mem_map_of_mem + have : g ⟨x, hx⟩ = + ∑ j, ⟨monomial (deg ⟨⟨x, hx⟩, j⟩) (coeff ⟨⟨x, hx⟩, j⟩), monomial_mem ⟨⟨x, hx⟩, j⟩⟩ := by + apply SetCoe.ext + simp only [Finset.univ_eq_attach, AddSubmonoidClass.coe_finsetSum, deg, coeff] + rw [(g ⟨x, hx⟩).1.support.sum_attach (fun n ↦ (monomial n) ((g ⟨x, hx⟩).1.coeff n))] + exact (sum_monomial_eq (g ⟨x, hx⟩).1).symm + rw [this] + apply sum_mem (fun i hi ↦ Ideal.subset_span ?_) + exact ⟨⟨⟨x, hx⟩, i⟩, rfl⟩ + +lemma exists_coeffs_sub_mem (n : ℕ) (J : Ideal R) (ι : Type u) [Fintype ι] (f : ι → reesAlgebra I) + (deg : ι → ℕ) (coeff : ι → R) (eq : ∀ i : ι, (f i).1 = monomial (deg i) (coeff i)) + (span_eq : (Ideal.span (Set.range f)).map (reesAlgebraToAssociatedGraded I) = + J.toAssociatedGraded I) + (r : R) (rmem_J : r ∈ J) (rmem_pow : r ∈ I ^ n) : ∃ (coeff' : ι → R), + (∀ i : ι, coeff' i ∈ I ^ (n - deg i)) ∧ (∀ i : ι, deg i > n → coeff' i = 0) ∧ + r - ∑ x : ι, coeff' x * coeff x ∈ I ^ (n + 1) := by + have : (reesAlgebraToAssociatedGraded I) ⟨monomial n r, reesAlgebra.monomial_mem.mpr rmem_pow⟩ ∈ + J.toAssociatedGraded I := by + apply Ideal.mem_map_of_mem + simp only [Ideal.mem_comap, Subalgebra.coe_val, Ideal.mem_map_C_iff] + intro m + by_cases eq : m = n + · simpa [eq] + · simp [coeff_monomial_of_ne _ eq] + rw [← span_eq, Ideal.map_span, ← Set.range_comp, Ideal.mem_span_range_iff_exists_fun] at this + rcases this with ⟨c, hc⟩ + let c' : ι → (reesAlgebra I) := fun i ↦ Classical.choose (Ideal.Quotient.mk_surjective (c i)) + let c'_spec (i : ι) : (reesAlgebraToAssociatedGraded I) (c' i) = c i := + Classical.choose_spec (Ideal.Quotient.mk_surjective (c i)) + have : (reesAlgebraToAssociatedGraded I) ⟨monomial n r, reesAlgebra.monomial_mem.mpr rmem_pow⟩ = + (reesAlgebraToAssociatedGraded I) (∑ i, c' i * f i) := by simp [← hc, c'_spec] + rw [Ideal.Quotient.mk_eq_mk_iff_sub_mem, mem_map_algebraMap_reesAlgebra_iff] at this + have coeff_eq := this n + simp only [AddSubgroupClass.coe_sub, AddSubmonoidClass.coe_finsetSum, MulMemClass.coe_mul, eq, + coeff_sub, coeff_monomial_same, finsetSum_coeff] at coeff_eq + let coeff' : ι → R := fun i ↦ if deg i ≤ n then (c' i).1.coeff (n - (deg i)) else 0 + have : ∑ i, ((c' i).1 * (monomial (deg i)) (coeff i)).coeff n = + ∑ i, (coeff' i) * (coeff i) := by + congr + ext i + rw [← Polynomial.C_mul_X_pow_eq_monomial, ← mul_assoc] + simp [coeff_mul_X_pow', coeff'] + rw [this] at coeff_eq + refine ⟨coeff', fun i ↦ ?_, fun i hi ↦ ?_, coeff_eq⟩ + · by_cases degle : deg i ≤ n + · simp only [degle, coeff'] + exact (mem_reesAlgebra_iff I _).mp (c' i).2 (n - deg i) + · simp [degle, coeff'] + · simp [coeff', hi] + +lemma exists_coeffs_isAdicCauchy (J : Ideal R) (ι : Type u) [Fintype ι] (f : ι → reesAlgebra I) + (deg : ι → ℕ) (coeff : ι → R) (memJ : ∀ i, coeff i ∈ J) + (eq : ∀ i : ι, (f i).1 = monomial (deg i) (coeff i)) + (span_eq : (Ideal.span (Set.range f)).map (reesAlgebraToAssociatedGraded I) = + J.toAssociatedGraded I) (r : R) (hr : r ∈ J) : + ∃ (g : ι → ℕ → R), (∀ i, AdicCompletion.IsAdicCauchy I R (g i)) ∧ + ∀ n, r - ∑ x : ι, g x n * coeff x ∈ I ^ (n + 1) := by + have exist (n : ℕ) := exists_coeffs_sub_mem I n J ι f deg coeff eq span_eq + have memJ' (g' : ι → R) : r - ∑ x, g' x * coeff x ∈ J := + sub_mem hr (sum_mem (fun i _ ↦ (Ideal.mul_mem_left _ _ (memJ i)))) + let coeffs' (n : ℕ) : {f : (ι → R) // r - ∑ x, f x * coeff x ∈ I ^ (n + 1)} := by + induction n with + | zero => + exact ⟨Classical.choose (exist 0 r hr (by simp)), + (Classical.choose_spec (exist 0 r hr (by simp))).2.2⟩ + | succ n coeffs'n => + refine ⟨coeffs'n + Classical.choose (exist (n + 1) _ (memJ' coeffs'n.1) coeffs'n.2), ?_⟩ + simp only [gt_iff_lt, Pi.add_apply, add_mul, Finset.sum_add_distrib, ← sub_sub] + exact (Classical.choose_spec (exist (n + 1) _ (memJ' coeffs'n.1) coeffs'n.2)).2.2 + have coeffs'_spec_aux (n : ℕ) : (coeffs' (n + 1)).1 = (coeffs' n).1 + + Classical.choose (exist (n + 1) _ (memJ' (coeffs' n).1) (coeffs' n).2) := rfl + have coeffs'_spec (n : ℕ) : + ∀ i, (coeffs' (n + 1)).1 i - (coeffs' n).1 i ∈ I ^ (n + 1 - deg i) := by + simp only [coeffs'_spec_aux, Pi.add_apply, add_sub_cancel_left] + exact (Classical.choose_spec (exist (n + 1) _ (memJ' (coeffs' n).1) (coeffs' n).2)).1 + let d := ∑ i, deg i + use fun i n ↦ (coeffs' (d + n)).1 i + refine ⟨fun i ↦ ?_, fun n ↦ Ideal.pow_le_pow_right (by omega) (coeffs' (d + n)).2⟩ + rw [AdicCompletion.isAdicCauchy_iff] + intro n + simp only [smul_eq_mul, Ideal.mul_top] + rw [SModEq.comm, SModEq.sub_mem, ← add_assoc d n 1] + have led : deg i ≤ d := Finset.single_le_sum (fun i _ ↦ Nat.zero_le _) (Finset.mem_univ i) + have : n ≤ d + n + 1 - deg i := by omega + exact Ideal.pow_le_pow_right this (coeffs'_spec (d + n) i) + +lemma isNoetherianRing_of_isAdicComplete_of_fg [IsNoetherianRing (R ⧸ I)] (fg : I.FG) + [IsAdicComplete I R] : IsNoetherianRing R := by + apply (isNoetherianRing_iff_ideal_fg R).mpr (fun J ↦ ?_) + have := isNoetherianRing_reesAlgebra_quotient fg + obtain ⟨ι, f, deg, coeff, fin, eq, memJ, span_eq⟩ := + exists_monomial_span_of_fg I J (Ideal.fg_of_isNoetherianRing _) + have : Fintype ι := Fintype.ofFinite ι + have : Fintype (Set.range coeff) := Fintype.ofFinite _ + use (Set.range coeff).toFinset + simp only [Set.coe_toFinset] + apply le_antisymm + · simp only [Ideal.span_le] + intro x ⟨i, hi⟩ + simpa [← hi] using memJ i + · intro j hj + rcases exists_coeffs_isAdicCauchy I J ι f deg coeff memJ eq span_eq j hj with ⟨c, cauchy, hc⟩ + let c_lim (i : ι) : R := Classical.choose (‹IsAdicComplete I R›.prec' (c i) (cauchy i)) + have c_lim_spec (i : ι) : ∀ (n : ℕ), c i n ≡ c_lim i [SMOD I ^ n • (⊤ : Ideal R)] := + Classical.choose_spec (‹IsAdicComplete I R›.prec' (c i) (cauchy i)) + rw [Ideal.mem_span_range_iff_exists_fun] + use c_lim + rw [IsHausdorff.eq_iff_smodEq (I := I)] + intro n + trans ∑ i, (c i n) * coeff i + · apply SModEq.sum (fun i _ ↦ ?_) + rw [SModEq.comm, SModEq.sub_mem, ← sub_mul] + apply Ideal.mul_mem_right + simpa [SModEq.sub_mem] using c_lim_spec i n + · rw [smul_eq_mul, Ideal.mul_top, SModEq.comm, SModEq.sub_mem] + exact Ideal.pow_le_pow_right (Nat.le_succ n) (hc n) + +lemma AdicCompletion.isNoetherianRing_of_fg [IsNoetherianRing (R ⧸ I)] (fg : I.FG) : + IsNoetherianRing (AdicCompletion I R) := by + let e : (AdicCompletion I R) ⧸ I.map (algebraMap R (AdicCompletion I R)) ≃+* R ⧸ I := + (Ideal.quotEquivOfEq (AdicCompletion.ker_evalOneₐ_eq_map I fg).symm).trans + (RingHom.quotientKerEquivOfSurjective (AdicCompletion.evalOneₐ_surjective I)) + have := isNoetherianRing_of_ringEquiv _ e.symm + have := AdicCompletion.isAdicComplete_self I fg + exact isNoetherianRing_of_isAdicComplete_of_fg _ (fg.map (algebraMap R (AdicCompletion I R))) + +instance [IsNoetherianRing R] : IsNoetherianRing (AdicCompletion I R) := + AdicCompletion.isNoetherianRing_of_fg I I.fg_of_isNoetherianRing + +lemma AdicCompletion.ringKrullDim_eq [IsNoetherianRing R] [IsLocalRing R] : + ringKrullDim (AdicCompletion (maximalIdeal R) R) = ringKrullDim R := by + have : Nontrivial (AdicCompletion (maximalIdeal R) R ⧸ + (maximalIdeal R).map (algebraMap R (AdicCompletion (maximalIdeal R) R))) := by + simpa [← AdicCompletion.maximalIdeal_eq_map] using Ideal.IsPrime.ne_top' + have ht := (Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown + (maximalIdeal R) (maximalIdeal (AdicCompletion (maximalIdeal R) R))).symm + rw [Ideal.map_mk_eq_bot_of_le (le_of_eq AdicCompletion.maximalIdeal_eq_map)] at ht + simp [← maximalIdeal_height_eq_ringKrullDim, ← ht] diff --git a/Mathlib/RingTheory/Gorenstein/Completion.lean b/Mathlib/RingTheory/Gorenstein/Completion.lean new file mode 100644 index 00000000000000..4713f7b592962a --- /dev/null +++ b/Mathlib/RingTheory/Gorenstein/Completion.lean @@ -0,0 +1,95 @@ +/- +Copyright (c) 2025 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.Category.ModuleCat.Ext.BaseChange +public import Mathlib.RingTheory.AdicCompletion.Noetherian +public import Mathlib.RingTheory.AdicCompletion.AsTensorProduct +public import Mathlib.RingTheory.Gorenstein.Defs +public import Mathlib.RingTheory.Regular.InjectiveDimension + +/-! + +# A Noetherian local ring is Gorenstein iff its completion is Gorenstein + +-/ + +universe u + +public section + +variable (R : Type u) [CommRing R] + +open CategoryTheory Abelian IsLocalRing + +/-- The base change map `R ⧸ I → S ⧸ IS ` -/ +def quotientIsBaseChangeMap' (S : Type*) [CommRing S] [Algebra R S] (I : Ideal R) : + R ⧸ I →ₗ[R] S ⧸ I.map (algebraMap R S) := + Submodule.liftQ I ((Ideal.Quotient.mkₐ R (I.map (algebraMap R S))).toLinearMap.comp + (Algebra.linearMap R S)) (fun x hx ↦ by + simp only [LinearMap.mem_ker, LinearMap.coe_comp, AlgHom.coe_toLinearMap, + Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply, Algebra.linearMap_apply] + exact Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_map_of_mem (algebraMap R S) hx)) + +lemma quotientIsBaseChangeMap'_isBaseChange (S : Type*) [CommRing S] [Algebra R S] (I : Ideal R) : + IsBaseChange S (quotientIsBaseChangeMap' R S I) := by + apply IsBaseChange.of_equiv (Ideal.qoutMapEquivTensorQout S).symm + intro x + rcases Submodule.Quotient.mk_surjective _ x with ⟨y, rfl⟩ + simp only [quotientIsBaseChangeMap', Submodule.liftQ_apply] + simp [Ideal.qoutMapEquivTensorQout, Algebra.smul_def] + +lemma isBaseChange_adicCompletion_subsingleton_iff [IsLocalRing R] + {M N : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup N] [Module R N] + [Module (AdicCompletion (maximalIdeal R) R) N] + [IsScalarTower R (AdicCompletion (maximalIdeal R) R) N] + {f : M →ₗ[R] N} (isb : IsBaseChange (AdicCompletion (maximalIdeal R) R) f) : + Subsingleton M ↔ Subsingleton N := by + rw [← isb.equiv.subsingleton_congr] + refine ⟨fun _ ↦ inferInstance, fun h ↦ ?_⟩ + rw [← subsingleton_tensorProduct (R := R)] + have surj : Function.Surjective (AdicCompletion.evalOneₐ (maximalIdeal R)).toLinearMap := + AdicCompletion.evalOneₐ_surjective (maximalIdeal R) + exact (LinearMap.rTensor_surjective M surj).subsingleton + +variable [IsNoetherianRing R] [IsLocalRing R] + +set_option backward.isDefEq.respectTransparency false in +lemma isGorensteinLocalRing_iff_exists' : + IsGorensteinLocalRing R ↔ ∃ n, ∀ i ≥ n, Subsingleton + (Ext (ModuleCat.of R (R ⧸ maximalIdeal R)) (ModuleCat.of R R) i) := by + have (a : WithBot ℕ∞) : a ≠ ⊤ ↔ ∃ (n : ℕ), a < n := by + induction a with + | bot => simp + | coe a => + induction a with + | top => simp + | coe a => simpa [-ENat.WithBot.coe_eq_natCast] using ⟨a + 1, Nat.cast_lt.mpr (lt_add_one a)⟩ + simp only [isGorensteinLocalRing_def, this, ge_iff_le] + apply exists_congr (fun n ↦ ?_) + rw [injectiveDimension_lt_iff_of_finite (ModuleCat.of R R) n] + congr! 2 + exact (((extFunctor _).mapIso (Shrink.linearEquiv.{u} R (R ⧸ maximalIdeal R)).toModuleIso.op).app + (ModuleCat.of R R)).symm.addCommGroupIsoToAddEquiv.subsingleton_congr + +theorem IsGorensteinLocalRing.iff_adicCompletion : + IsGorensteinLocalRing R ↔ IsGorensteinLocalRing (AdicCompletion (maximalIdeal R) R) := by + let R' := AdicCompletion (maximalIdeal R) R + let f := quotientIsBaseChangeMap' R R' (maximalIdeal R) + have isbf : IsBaseChange R' f := quotientIsBaseChangeMap'_isBaseChange R R' (maximalIdeal R) + let res' := R' ⧸ Ideal.map (algebraMap R R') (maximalIdeal R) + let e : (R' ⧸ maximalIdeal R') ≃ₗ[R'] res' := + Submodule.quotEquivOfEq _ _ AdicCompletion.maximalIdeal_eq_map + rw [isGorensteinLocalRing_iff_exists', isGorensteinLocalRing_iff_exists'] + congr! 4 + rename_i i _ + let eExt := ((extFunctor i).mapIso e.toModuleIso.op).app (ModuleCat.of R' R') + apply Iff.trans _ eExt.addCommGroupIsoToAddEquiv.subsingleton_congr + simp only [extFunctor_obj, extFunctorObj_obj_coe] + let isbExt := Ext.isBaseChange R' (ModuleCat.of R (R ⧸ maximalIdeal R)) (ModuleCat.of R R) + (MS := ModuleCat.of R' res') (NS := ModuleCat.of R' R') f isbf + (Algebra.linearMap R R') (IsBaseChange.linearMap R R') i + exact isBaseChange_adicCompletion_subsingleton_iff R isbExt diff --git a/Mathlib/RingTheory/Gorenstein/Defs.lean b/Mathlib/RingTheory/Gorenstein/Defs.lean new file mode 100644 index 00000000000000..fd6e7803cb8c96 --- /dev/null +++ b/Mathlib/RingTheory/Gorenstein/Defs.lean @@ -0,0 +1,72 @@ +/- +Copyright (c) 2025 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.Category.ModuleCat.InjectiveDimension +public import Mathlib.RingTheory.Localization.AtPrime.Basic +public import Mathlib.RingTheory.LocalRing.Basic +public import Mathlib.RingTheory.LocalRing.RingHom.Basic + +/-! + +# Definition of Gorenstein Local Ring + +-/ + +@[expose] public section + +universe v u + +variable (R : Type u) [CommRing R] + +open CategoryTheory + +/-- A local ring `R` is Gorenstein if `R` itself viewed as an `R`-module +has finite injective dimension. -/ +class IsGorensteinLocalRing : Prop extends IsLocalRing R where + injdim : injectiveDimension (ModuleCat.of R R) ≠ ⊤ + +lemma isGorensteinLocalRing_def [IsLocalRing R] : + IsGorensteinLocalRing R ↔ injectiveDimension (ModuleCat.of R R) ≠ ⊤ := + ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩ + +variable {R} in +attribute [local instance] RingHomInvPair.of_ringEquiv in +lemma IsGorensteinLocalRing.of_ringEquiv {R' : Type u} [CommRing R'] (e : R ≃+* R') + [IsGorensteinLocalRing R] : IsGorensteinLocalRing R' := by + let eR : (ModuleCat.of R R) ≃ₛₗ[RingHomClass.toRingHom e] (ModuleCat.of R' R') := + e.toSemilinearEquiv + have : IsLocalRing R' := e.isLocalRing + have := (isGorensteinLocalRing_def R).mp ‹_› + rw [injectiveDimension_eq_of_semiLinearEquiv e eR] at this + exact (isGorensteinLocalRing_def R').mpr this + +/-- A commutative ring is Gorenstein if its localization at every prime +`IsGorensteinLocalRing`. -/ +class IsGorensteinRing : Prop where + isGorenstein_localize : ∀ p : Ideal R, ∀ (_ : p.IsPrime), + IsGorensteinLocalRing (Localization.AtPrime p) + +lemma isGorensteinRing_def : IsGorensteinRing R ↔ + ∀ p : Ideal R, ∀ (_ : p.IsPrime), IsGorensteinLocalRing (Localization.AtPrime p) := + ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩ + +lemma isGorensteinRing_def' : IsGorensteinRing R ↔ + ∀ p : PrimeSpectrum R, IsGorensteinLocalRing (Localization.AtPrime p.1) := + ⟨fun ⟨h⟩ ↦ fun p ↦ h p.1 p.2, fun h ↦ ⟨fun p hp ↦ h ⟨p, hp⟩⟩⟩ + +lemma isGorensteinRing_of_ringEquiv {R' : Type u} [CommRing R'] + (e : R ≃+* R') [G : IsGorensteinRing R] : IsGorensteinRing R' := by + apply (isGorensteinRing_def R').mpr (fun p' hp' ↦ ?_) + let p := p'.comap e + have := (isGorensteinRing_def R).mp ‹_› p (Ideal.comap_isPrime e p') + have : p.primeCompl.map e.toMonoidHom = p'.primeCompl := by + ext x + have : (∃ y, e y ∉ p' ∧ e y = x) ↔ x ∉ p' := ⟨fun ⟨y, hy, eq⟩ ↦ eq ▸ hy, + fun h ↦ ⟨e.symm x, (RingEquiv.apply_symm_apply e x).symm ▸ h, RingEquiv.apply_symm_apply e x⟩⟩ + simpa only [p] + exact IsGorensteinLocalRing.of_ringEquiv + (IsLocalization.ringEquivOfRingEquiv (Localization.AtPrime p) (Localization.AtPrime p') e this) diff --git a/Mathlib/RingTheory/ReesAlgebra.lean b/Mathlib/RingTheory/ReesAlgebra.lean index 148cfd9c7978ca..572eea3824359c 100644 --- a/Mathlib/RingTheory/ReesAlgebra.lean +++ b/Mathlib/RingTheory/ReesAlgebra.lean @@ -6,7 +6,8 @@ Authors: Andrew Yang module public import Mathlib.RingTheory.Ideal.BigOperators -public import Mathlib.RingTheory.FiniteType +public import Mathlib.RingTheory.FiniteStability +public import Mathlib.RingTheory.TensorProduct.Quotient /-! @@ -121,3 +122,41 @@ instance [IsNoetherianRing R] : Algebra.FiniteType R (reesAlgebra I) := instance [IsNoetherianRing R] : IsNoetherianRing (reesAlgebra I) := Algebra.FiniteType.isNoetherianRing R _ + +open TensorProduct in +lemma tensorProduct_reesAlgebra_isNoetherian_of_fg [IsNoetherianRing (R ⧸ I)] (fg : I.FG) : + IsNoetherianRing ((R ⧸ I) ⊗[R] (reesAlgebra I)) := by + have : Algebra.FiniteType R (reesAlgebra I) := ⟨(reesAlgebra I).fg_top.mpr (reesAlgebra.fg fg)⟩ + have := this.baseChange (R ⧸ I) + exact Algebra.FiniteType.isNoetherianRing (R ⧸ I) _ + +lemma isNoetherianRing_reesAlgebra_quotient [IsNoetherianRing (R ⧸ I)] (fg : I.FG) : + IsNoetherianRing ((reesAlgebra I) ⧸ I.map (algebraMap R (reesAlgebra I))) := by + have := tensorProduct_reesAlgebra_isNoetherian_of_fg fg + exact isNoetherianRing_of_ringEquiv _ + (Algebra.TensorProduct.quotIdealMapEquivQuotTensor (reesAlgebra I) I).symm.toRingEquiv + +lemma mem_map_algebraMap_reesAlgebra_iff (f : reesAlgebra I) : + f ∈ I.map (algebraMap R (reesAlgebra I)) ↔ ∀ n, f.1.coeff n ∈ I ^ (n + 1) := by + refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩ + · rw [← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map] at h + induction h using Submodule.smul_induction_on' with + | smul r hr m hm => + simpa [pow_succ'] using Ideal.mul_mem_mul hr ((mem_reesAlgebra_iff I _).mp m.2 n) + | add x hx y hy memx memy => simpa using add_mem memx memy + · have mem' (i : ℕ) {r : R} : r ∈ I ^ i → _ := reesAlgebra.monomial_mem.mpr + have mem (i : ℕ) := reesAlgebra.monomial_mem.mpr ((mem_reesAlgebra_iff I _).mp f.2 i) + have : f = ∑ i ∈ f.1.support, ⟨monomial i (f.1.coeff i), mem i⟩ := + SetCoe.ext (by simpa using f.1.as_sum_support) + rw [this] + apply sum_mem (fun i hi ↦ ?_) + have {r : R} (h' : r ∈ I * I ^ i) : ⟨monomial i r, mem' i (Ideal.mul_le_left h')⟩ + ∈ I.map (algebraMap R (reesAlgebra I)) := by + induction h' using Submodule.mul_induction_on' with + | mem_mul_mem s hs t ht => + simp_rw [← smul_eq_mul, ← smul_monomial] + rw [← SetLike.mk_smul_mk (hx := mem' i ht), Algebra.smul_def] + exact Ideal.mul_mem_right _ _ (Ideal.mem_map_of_mem _ hs) + | add s1 hs1 s2 hs2 mem1 mem2 => simpa using add_mem mem1 mem2 + apply this + simpa [pow_succ'] using h i diff --git a/Mathlib/RingTheory/Regular/InjectiveDimension.lean b/Mathlib/RingTheory/Regular/InjectiveDimension.lean new file mode 100644 index 00000000000000..2b941b87bcd880 --- /dev/null +++ b/Mathlib/RingTheory/Regular/InjectiveDimension.lean @@ -0,0 +1,453 @@ +/- +Copyright (c) 2025 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.Category.Grp.Zero +public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact +public import Mathlib.Algebra.Category.ModuleCat.Ext.Baer +public import Mathlib.Algebra.Category.ModuleCat.Ext.Finite +public import Mathlib.Algebra.FiveLemma +public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Map +public import Mathlib.CategoryTheory.Abelian.Projective.Dimension +public import Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness +public import Mathlib.RingTheory.Ideal.KrullsHeightTheorem +public import Mathlib.RingTheory.KrullDimension.NonZeroDivisors +public import Mathlib.RingTheory.Regular.Category +public import Mathlib.RingTheory.Regular.RegularSequence +public import Mathlib.RingTheory.Support + +/-! + +# Injective Dimension of Quotient Regular Sequence + +-/ + +@[expose] public section + +universe v u + +variable (R : Type u) [CommRing R] + +open IsLocalRing + +lemma exist_nat_eq' [FiniteRingKrullDim R] : ∃ n : ℕ, ringKrullDim R = n := by + obtain ⟨m, hm⟩ := WithBot.ne_bot_iff_exists.mp (ringKrullDim_ne_bot (R := R)) + obtain ⟨n, hn⟩ := ENat.ne_top_iff_exists.mp + (WithBot.coe_inj.not.mp (ne_of_eq_of_ne hm ringKrullDim_ne_top)) + exact ⟨n, ((WithBot.coe_inj.mpr hn).trans hm).symm⟩ + +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) := + ⟨RingHom.injective _, Ideal.Quotient.lift_surjective_of_surjective _ _ + (Ideal.Quotient.mk_surjective.comp surj)⟩ + +open CategoryTheory Abelian Module + +section + +variable {R} [IsLocalRing R] [IsNoetherianRing R] [Small.{v} R] + +omit [IsLocalRing R] in +lemma ext_subsingleton_of_support_subset (N M : ModuleCat.{v} R) [Nfin : Module.Finite R N] (n : ℕ) + (h : support R N ⊆ {p | Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ p.1))) M n)}) : + Subsingleton (Ext N M n) := by + refine (IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime + (motive := fun L ↦ (support R L ⊆ {p | Subsingleton + (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ p.1))) M n)} → + Subsingleton (Ext (ModuleCat.of R L) M n))) R Nfin) ?_ ?_ ?_ h + · intro N _ _ _ sub _ + have : HasProjectiveDimensionLT (ModuleCat.of R N) 0 := + (ModuleCat.isZero_of_iff_subsingleton.mpr sub).hasProjectiveDimensionLT_zero + exact HasProjectiveDimensionLT.subsingleton (ModuleCat.of R N) 0 n n.zero_le M + · intro N _ _ _ p e h + have mem : p ∈ support R N := by + rw [e.support_eq, Module.mem_support_iff_of_finite, Ideal.annihilator_quotient] + let e' : ModuleCat.of R N ≅ ModuleCat.of R (Shrink.{v, u} (R ⧸ p.asIdeal)) := + (e.trans (Shrink.linearEquiv R _).symm).toModuleIso + have := (((extFunctor n).mapIso e'.op).app M).addCommGroupIsoToAddEquiv.subsingleton_congr + simp only [extFunctor, extFunctorObj_obj_coe] at this + simpa [← this] using h mem + · intro N₁ _ _ _ N₂ _ _ _ N₃ _ _ _ f g inj surj exac h1 h3 h2 + simp only [Module.support_of_exact exac inj surj, Set.union_subset_iff] at h2 + let S := ModuleCat.shortComplexOfCompEqZero f g exac.linearMap_comp_eq_zero + have S_exact : S.ShortExact := ModuleCat.shortComplex_shortExact S exac inj surj + have := (Ext.contravariant_sequence_exact₂' S_exact M n).isZero_of_both_isZero + (AddCommGrpCat.isZero_of_iff_subsingleton.mpr (h3 h2.2)) + (AddCommGrpCat.isZero_of_iff_subsingleton.mpr (h1 h2.1)) + exact AddCommGrpCat.subsingleton_of_isZero this + +set_option backward.isDefEq.respectTransparency false in +lemma ext_subsingleton_of_all_gt (M : ModuleCat.{v} R) [Module.Finite R M] (n : ℕ) + (p : Ideal R) [p.IsPrime] (ne : p ≠ maximalIdeal R) (h : ∀ q > p, q.IsPrime → + Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ q))) M (n + 1))) : + Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ p))) M n) := by + have plt : p < maximalIdeal R := lt_of_le_of_ne (le_maximalIdeal_of_isPrime p) ne + obtain ⟨x, hx, nmem⟩ : ∃ x ∈ maximalIdeal R, x ∉ p := Set.exists_of_ssubset plt + have := nontrivial_quotSMulTop_of_mem_maximalIdeal (Shrink.{v} (R ⧸ p)) hx + have : Subsingleton (Ext (ModuleCat.of R (QuotSMulTop x (Shrink.{v, u} (R ⧸ p)))) M (n + 1)) := by + apply ext_subsingleton_of_support_subset + intro q hq + apply h q.1 _ q.2 + simp only [support_quotSMulTop, (Shrink.linearEquiv R (R ⧸ p)).support_eq, Set.mem_inter_iff, + PrimeSpectrum.mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe] at hq + have : q.asIdeal ≠ p := ne_of_mem_of_not_mem' hq.2 nmem + apply lt_of_le_of_ne _ (ne_of_mem_of_not_mem' hq.2 nmem).symm + rw [← p.annihilator_quotient] + exact Module.annihilator_le_of_mem_support hq.1 + let S := (ModuleCat.of R (Shrink.{v} (R ⧸ p))).smulShortComplex x + have reg : IsSMulRegular (Shrink.{v} (R ⧸ p)) x := by + rw [(Shrink.linearEquiv.{v} R _).isSMulRegular_congr, isSMulRegular_iff_right_eq_zero_of_smul] + intro r hr + simpa [Algebra.smul_def, Ideal.Quotient.eq_zero_iff_mem, nmem] using hr + have S_exact : S.ShortExact := IsSMulRegular.smulShortComplex_shortExact reg + have exac := Ext.contravariant_sequence_exact₁' S_exact M n (n + 1) (add_comm 1 n) + have epi := exac.epi_f ((AddCommGrpCat.isZero_of_iff_subsingleton.mpr this).eq_zero_of_tgt _) + have : S.f = x • 𝟙 (ModuleCat.of R (Shrink.{v, u} (R ⧸ p))) := rfl + simp only [S, this, AddCommGrpCat.epi_iff_surjective, AddCommGrpCat.hom_ofHom] at epi + have mem_jac : x ∈ (Module.annihilator R (Ext S.X₂ M n)).jacobson := + (IsLocalRing.maximalIdeal_le_jacobson _) hx + by_contra ntr + have : Nontrivial (Ext S.X₂ M n) := not_subsingleton_iff_nontrivial.mp ntr + let fin : Module.Finite R (Shrink.{v, u} (R ⧸ p)) := inferInstance + have : Module.Finite R S.X₂ := fin + absurd Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator mem_jac + rw [eq_comm, eq_top_iff] + intro y hy + rcases epi y with ⟨z, hz⟩ + simp only [ModuleCat.smulShortComplex, Ext.mk₀_smul, + Ext.bilinearComp_apply_apply, Ext.smul_comp, Ext.mk₀_id_comp] at hz + simpa [← hz] using Submodule.smul_mem_pointwise_smul _ _ ⊤ trivial + +lemma ext_vanish_of_residueField_vanish (M : ModuleCat.{v} R) (n : ℕ) [Module.Finite R M] + (h : ∀ i ≥ n, Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ maximalIdeal R))) M i)) : + ∀ i ≥ n, ∀ N : ModuleCat.{v} R, Subsingleton (Ext N M i) := by + refine fun i hi N ↦ (M.hasInjectiveDimensionLT_of_quotients _ ?_).subsingleton _ _ i hi N + intro I + apply ext_subsingleton_of_support_subset + intro p foo + clear foo + simp only [Set.mem_setOf_eq] + have (m : ℕ) (j : ℕ) (hj : j ≥ n) : ringKrullDim (R ⧸ p.1) ≤ m → + Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ p.asIdeal))) M j) := by + induction m generalizing j hj p with + | zero => + intro hp + have : p.1 = maximalIdeal R := by + rw [← isMaximal_iff, Ideal.Quotient.maximal_ideal_iff_isField_quotient] + exact (Ring.krullDimLE_iff.mpr hp).isField_of_isDomain + exact this ▸ h j hj + | succ n ih => + intro hp + by_cases hpm : p.1 = maximalIdeal R + · exact hpm ▸ h j hj + · apply ext_subsingleton_of_all_gt M j p.1 hpm + intro q hqp hq + let q : PrimeSpectrum R := ⟨q, hq⟩ + have : ringKrullDim (R ⧸ q.1) ≤ n := by + rw [← ENat.WithBot.add_le_add_natCast_right_iff] + apply le_trans _ hp + obtain ⟨r, hrq, hrp⟩ := Set.exists_of_ssubset hqp + apply ringKrullDim_succ_le_of_surjective (r := Ideal.Quotient.mk p.1 r) + (Ideal.Quotient.factor hqp.le) (Ideal.Quotient.factor_surjective hqp.le) + · simpa using Ideal.Quotient.eq_zero_iff_mem.not.mpr hrp + · simpa using Ideal.Quotient.eq_zero_iff_mem.mpr hrq + apply ih (j + 1) (Nat.le_add_right_of_le hj) this + rcases exist_nat_eq' R with ⟨m, hm⟩ + apply this m n (le_refl n) + simpa [← hm] using ringKrullDim_quotient_le p.1 + +lemma injectiveDimension_eq_sInf_of_finite (M : ModuleCat.{v} R) [Module.Finite R M] : + injectiveDimension M = sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < i → + Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ maximalIdeal R))) M i)} := by + simp only [injectiveDimension] + congr! 3 + rename_i n + refine ⟨fun h i hi ↦ (h i hi).subsingleton M i i (le_refl i) _, fun h i hi ↦ ?_⟩ + rw [hasInjectiveDimensionLT_iff] + intro j hj N e + refine @Subsingleton.eq_zero _ _ ?_ e + apply ext_vanish_of_residueField_vanish M i _ j hj N + intro k hk + exact h k (lt_of_lt_of_le hi (Nat.cast_le.mpr hk)) + +lemma injectiveDimension_lt_iff_of_finite (M : ModuleCat.{v} R) [Module.Finite R M] (n : ℕ) : + injectiveDimension M < n ↔ ∀ (i : ℕ), n ≤ i → + Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ maximalIdeal R))) M i) := by + rw [injectiveDimension_eq_sInf_of_finite] + refine ⟨fun h i hi ↦ ?_, fun h ↦ sInf_lt_iff.2 ?_⟩ + · have : sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < ↑i → + Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ maximalIdeal R))) M i)} ∈ _ := + csInf_mem ⟨⊤, by simp⟩ + exact this i (lt_of_lt_of_le h (Nat.cast_le.mpr hi)) + · obtain _ | n := n + · exact ⟨⊥, fun i hi ↦ h i (Nat.zero_le i) , by decide⟩ + · exact ⟨n, fun i hi ↦ h i (Nat.cast_lt.mp hi), by simp [ENat.WithBot.lt_add_one_iff]⟩ + +end + +section + +variable {R} + +section restrictScalars + +universe u' + +variable {R' : Type u'} [CommRing R'] (f : R →+* R') + +/-- Restricting scalar by surjective ring homomorphism is fully faithful. -/ +noncomputable def ModuleCat.restrictScalarsFullyFaithfulOfSurjective (h : Function.Surjective f) : + (ModuleCat.restrictScalars.{v} f).FullyFaithful where + preimage {X Y} g := ofHom + { __ := g.hom + map_smul' r' x := by + let _ := Module.compHom X f + rcases h r' with ⟨r, hr⟩ + rw [← hr] + exact map_smul g.hom r x } + +end restrictScalars + +set_option backward.isDefEq.respectTransparency false in +lemma hasProjectiveDimensionLE_finsupp_quotient_regular [Small.{v} R] (ι : Type v) {x : R} + (regR : IsSMulRegular R x) : + HasProjectiveDimensionLE (ModuleCat.of R (ι →₀ Shrink.{v} (R ⧸ Ideal.span {x}))) 1 := by + let f' : Shrink.{v} R →ₗ[R] Shrink.{v} R := ((Shrink.linearEquiv R R).symm.toLinearMap.comp + (x • LinearMap.id)).comp (Shrink.linearEquiv R R).toLinearMap + let g' : Shrink.{v} R →ₗ[R] Shrink.{v} (R ⧸ Ideal.span {x}) := + ((Shrink.linearEquiv R _).symm.toLinearMap.comp + (Ideal.Quotient.mkₐ R (Ideal.span {x})).toLinearMap).comp (Shrink.linearEquiv R R).toLinearMap + have inj : Function.Injective f' := by simpa [f'] using! regR + have surj : Function.Surjective g' := by simpa [g'] using Ideal.Quotient.mk_surjective + have exac : Function.Exact f' g' := by + intro y + simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, AlgHom.coe_toLinearMap, + Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply, EmbeddingLike.map_eq_zero_iff, + EquivLike.range_comp, Set.mem_range, LinearMap.smul_apply, LinearMap.id_coe, + LinearEquiv.symm_apply_eq, id_eq, Ideal.Quotient.eq_zero_iff_mem, + Ideal.mem_span_singleton', smul_eq_mul, mul_comm, g', f'] + let S : ShortComplex (ModuleCat.{v} R) := { + X₁ := ModuleCat.of R (ι →₀ Shrink.{v} R) + X₂ := ModuleCat.of R (ι →₀ Shrink.{v} R) + X₃ := ModuleCat.of R (ι →₀ Shrink.{v} (R ⧸ Ideal.span {x})) + f := ModuleCat.ofHom (Finsupp.mapRange.linearMap f') + g := ModuleCat.ofHom (Finsupp.mapRange.linearMap g') + zero := by + rw [← ModuleCat.ofHom_comp, ← Finsupp.mapRange.linearMap_comp, + exac.linearMap_comp_eq_zero] + ext + simp } + have S_exact : S.ShortExact := { + exact := (ShortComplex.ShortExact.moduleCat_exact_iff_function_exact S).mpr (by + simp [LinearMap.exact_iff, S, Finsupp.ker_mapRange, LinearMap.exact_iff.mp exac, + Finsupp.range_mapRange_linearMap f' (LinearMap.ker_eq_bot.mpr inj)] ) + mono_f := (ModuleCat.mono_iff_injective _).mpr (Finsupp.mapRange_injective f' (map_zero _) inj) + epi_g := (ModuleCat.epi_iff_surjective _).mpr + (Finsupp.mapRange_surjective g' (map_zero _) surj) } + have : Projective (ModuleCat.of R (ι →₀ Shrink.{v} R)) := ModuleCat.projective_of_free + ⟨Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R)⟩ + exact S_exact.hasProjectiveDimensionLT_X₃ 1 inferInstance inferInstance + +variable [Small.{v} R] + +set_option backward.isDefEq.respectTransparency false in +open Limits in +lemma extClass_postcomp_bijective_of_isSMulRegular {M : ModuleCat.{v} R} {x : R} + (regM : IsSMulRegular M x) (N : ModuleCat.{v} R) (ann : x • 𝟙 N = 0) : + Function.Bijective (regM.smulShortComplex_shortExact.extClass.postcomp + N (rfl : 0 + 1 = 0 + 1)) := by + refine ⟨?_, fun y ↦ Ext.covariant_sequence_exact₁ _ regM.smulShortComplex_shortExact y ?_ rfl⟩ + · apply (AddCommGrpCat.mono_iff_injective _).mp ((Ext.covariant_sequence_exact₃' N + regM.smulShortComplex_shortExact 0 1 (zero_add 1)).mono_g (IsZero.eq_zero_of_src ?_ _)) + rw [AddCommGrpCat.isZero_of_iff_subsingleton, Ext.homEquiv₀.subsingleton_congr] + apply subsingleton_of_forall_eq 0 fun f ↦ ModuleCat.hom_ext (LinearMap.ext fun t ↦ regM ?_) + have : (x • 𝟙 N) t = x • t := by simp + simp [smul_zero, ← map_smul, ← this, ann, map_zero] + · conv in ShortComplex.f ?_ => change x • (𝟙 M) + rw [← Ext.mk₀_id_comp (y.comp (Ext.mk₀ (x • 𝟙 M)) rfl), Ext.mk₀_smul, + Ext.comp_smul, Ext.comp_smul, ← Ext.smul_comp, ← Ext.mk₀_smul] + simp [ann] + +set_option backward.isDefEq.respectTransparency false in +/-- The map `Ext N (ModuleCat.of (R ⧸ Ideal.span {x}) (QuotSMulTop x ↑M)) n →+ + Ext ((ModuleCat.restrictScalars (Ideal.Quotient.mk (Ideal.span {x}))).obj N) M (n + 1)` + is bijective. -/ +theorem extClass_comp_mapExt_bijective {M : ModuleCat.{v} R} {x : R} (regR : IsSMulRegular R x) + (regM : IsSMulRegular M x) (N : ModuleCat.{v} (R ⧸ Ideal.span {x})) (n : ℕ) : + Function.Bijective ((regM.smulShortComplex_shortExact.extClass.postcomp + ((ModuleCat.restrictScalars.{v} (Ideal.Quotient.mk (Ideal.span {x}))).obj N) rfl).comp + ((ModuleCat.restrictScalars.{v} (Ideal.Quotient.mk (Ideal.span {x}))).mapExtAddHom N + (ModuleCat.of (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) n)) := by + let Fr := (ModuleCat.restrictScalars.{v} (Ideal.Quotient.mk (Ideal.span {x}))) + induction n generalizing N with + | zero => + simp only [ModuleCat.smulShortComplex, Nat.reduceAdd, AddMonoidHom.coe_comp] + refine Function.Bijective.comp ?_ ?_ + · apply extClass_postcomp_bijective_of_isSMulRegular regM + ext u + simp + · change Function.Bijective (Ext.mapExactFunctor _) + rw [Ext.mapExactFunctor₀, Equiv.comp_bijective, Equiv.bijective_comp] + apply Functor.FullyFaithful.map_bijective + exact ModuleCat.restrictScalarsFullyFaithfulOfSurjective _ Ideal.Quotient.mk_surjective + | succ n ih => + let S := N.projectiveShortComplex + have S_exact : S.ShortExact := N.shortExact_projectiveShortComplex + have : HasProjectiveDimensionLT (S.map Fr).X₂ 2 := + hasProjectiveDimensionLE_finsupp_quotient_regular N regR + let MxM := (ModuleCat.of (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) + let f : Ext S.X₂ MxM n →+ Ext S.X₁ MxM n := (Ext.mk₀ S.f).precomp MxM (zero_add n) + let g : Ext S.X₁ MxM n →+ Ext S.X₃ MxM (n + 1) := S_exact.extClass.precomp MxM (add_comm 1 n) + have exac1 : Function.Exact f g := (ShortComplex.ab_exact_iff_function_exact _).mp + (Ext.contravariant_sequence_exact₁' S_exact MxM n (n + 1) (add_comm 1 n)) + have surj1 : Function.Surjective g := precomp_extClass_surjective_of_projective_X₂ MxM S_exact n + let f' : Ext (S.map Fr).X₂ M (n + 1) →+ Ext (S.map Fr).X₁ M (n + 1) := + (Ext.mk₀ (S.map Fr).f).precomp M (zero_add (n + 1)) + let g' : Ext (S.map Fr).X₁ M (n + 1) →+ Ext (S.map Fr).X₃ M (n + 2) := + (S_exact.map_of_exact Fr).extClass.precomp M (add_comm 1 (n + 1)) + have exac2 : Function.Exact f' g' := + (ShortComplex.ab_exact_iff_function_exact _).mp (Ext.contravariant_sequence_exact₁' + (S_exact.map_of_exact Fr) M (n + 1) (n + 2) (add_comm 1 (n + 1))) + have isz2 : Limits.IsZero (AddCommGrpCat.of (Ext (S.map Fr).X₂ M (n + 2))) := + AddCommGrpCat.isZero_of_iff_subsingleton.mpr + (HasProjectiveDimensionLT.subsingleton (S.map Fr).X₂ 2 (n + 2) (Nat.le_add_left _ n) M) + have surj2 : Function.Surjective g' := (AddCommGrpCat.epi_iff_surjective _).mp + ((Ext.contravariant_sequence_exact₃' (S_exact.map_of_exact Fr) M (n + 1) (n + 2) + (add_comm 1 (n + 1))).epi_f (isz2.eq_zero_of_tgt _)) + let ft (N : ModuleCat.{v} (R ⧸ Ideal.span {x})) (m : ℕ) := + ((regM.smulShortComplex_shortExact.extClass.postcomp (Fr.obj N) rfl).comp + (Fr.mapExtAddHom N (ModuleCat.of (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) m)) + apply AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact f g f' g' + (ft S.X₂ n) (ft S.X₁ n) (ft S.X₃ (n + 1)) ?_ ?_ + exac1 exac2 (ih S.X₂).2 (ih S.X₁) surj1 surj2 + · ext z + have : (Ext.mk₀ (Fr.map S.f)).comp (z.mapExactFunctor Fr) (zero_add n) = + (((Ext.mk₀ S.f).comp z (zero_add n)).mapExactFunctor Fr) := by + rw [Ext.mapExactFunctor_comp, Ext.mapExactFunctor_mk₀] + apply (Ext.comp_assoc _ _ _ (zero_add n) rfl (zero_add (n + 1))).symm.trans + exact congrFun (congrFun (congrFun (congrArg Ext.comp this) _) (n + 1)) rfl + · ext z + have : (S_exact.map_of_exact Fr).extClass.comp (z.mapExactFunctor Fr) (add_comm 1 n) = + (S_exact.extClass.comp z (add_comm 1 n)).mapExactFunctor Fr := by + rw [Ext.mapExactFunctor_comp, Ext.mapExactFunctor_extClass] + apply (Ext.comp_assoc _ _ _ (add_comm 1 n) rfl (add_comm 1 (n + 1))).symm.trans + exact congrFun (congrFun (congrFun (congrArg Ext.comp this) _) (n + 2)) rfl + +end + +section + +lemma Function.Bijective.subsingleton_congr {α β : Type*} {f : α → β} (bij : Function.Bijective f) : + Subsingleton α ↔ Subsingleton β := + ⟨fun _ ↦ bij.2.subsingleton, fun _ ↦ bij.1.subsingleton⟩ + +variable {R} [IsLocalRing R] + +section + +variable [Small.{v} R] + +set_option backward.isDefEq.respectTransparency false in +lemma ext_residueField_subsingleton_iff {M : ModuleCat.{v} R} {x : R} + (regR : IsSMulRegular R x) (regM : IsSMulRegular M x) (mem : x ∈ maximalIdeal R) (n : ℕ) : + letI : IsLocalRing (R ⧸ Ideal.span {x}) := + have : Nontrivial (R ⧸ Ideal.span {x}) := + Ideal.Quotient.nontrivial_iff.mpr (by simpa [← Submodule.ideal_span_singleton_smul]) + IsLocalRing.of_surjective' (Ideal.Quotient.mk (Ideal.span {x})) Ideal.Quotient.mk_surjective + Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ maximalIdeal R))) M (n + 1)) ↔ + Subsingleton (Ext (ModuleCat.of (R ⧸ Ideal.span {x}) + (Shrink.{v} ((R ⧸ Ideal.span {x}) ⧸ maximalIdeal (R ⧸ Ideal.span {x})))) + (ModuleCat.of (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) n) := by + have : Nontrivial (R ⧸ Ideal.span {x}) := + Ideal.Quotient.nontrivial_iff.mpr (by simpa [← Submodule.ideal_span_singleton_smul]) + have : IsLocalHom (Ideal.Quotient.mk (Ideal.span {x})) := + IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective + have : IsLocalRing (R ⧸ Ideal.span {x}) := + IsLocalRing.of_surjective (Ideal.Quotient.mk (Ideal.span {x})) Ideal.Quotient.mk_surjective + let k' := (ModuleCat.of (R ⧸ Ideal.span {x}) + (Shrink.{v} ((R ⧸ Ideal.span {x}) ⧸ maximalIdeal (R ⧸ Ideal.span {x})))) + let e' : (R ⧸ maximalIdeal R) ≃ₗ[R] (R ⧸ Ideal.span {x}) ⧸ maximalIdeal (R ⧸ Ideal.span {x}) := + { __ := RingEquiv.ofBijective _ (ResidueField.map_bijective_of_surjective + (Ideal.Quotient.mk (Ideal.span {x})) Ideal.Quotient.mk_surjective) + map_smul' r y := by + simp only [RingEquiv.toEquiv_eq_coe, Algebra.smul_def, Ideal.Quotient.algebraMap_eq, + Equiv.toFun_as_coe, EquivLike.coe_coe, map_mul, RingEquiv.coe_ofBijective, + RingHom.id_apply, mul_eq_mul_right_iff] + left + rfl } + let e : (ModuleCat.of R (Shrink.{v} (R ⧸ maximalIdeal R))) ≅ + (ModuleCat.restrictScalars (Ideal.Quotient.mk (Ideal.span {x}))).obj k' := + (((Shrink.linearEquiv.{v} R _).trans e').trans (Shrink.linearEquiv.{v} R _).symm).toModuleIso + exact ((extClass_comp_mapExt_bijective regR regM k' n).subsingleton_congr.trans + (((extFunctor (n + 1)).mapIso e.op).app M).addCommGroupIsoToAddEquiv.subsingleton_congr).symm + +end + +instance finite_QuotSMulTop' (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] + (x : R) : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M) := + Module.Finite.of_restrictScalars_finite R _ _ + +set_option backward.isDefEq.respectTransparency false in +theorem injectiveDimension_quotSMulTop_succ_eq_injectiveDimension [Small.{v} R] [IsNoetherianRing R] + {M : ModuleCat.{v} R} [Module.Finite R M] {x : R} (regR : IsSMulRegular R x) + (regM : IsSMulRegular M x) (mem : x ∈ maximalIdeal R) : + injectiveDimension (ModuleCat.of (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) + 1 = + injectiveDimension M := by + have : IsLocalRing (R ⧸ Ideal.span {x}) := + have : Nontrivial (R ⧸ Ideal.span {x}) := + Ideal.Quotient.nontrivial_iff.mpr (by simpa [← Submodule.ideal_span_singleton_smul]) + IsLocalRing.of_surjective' (Ideal.Quotient.mk (Ideal.span {x})) Ideal.Quotient.mk_surjective + have sub : Subsingleton M ↔ Subsingleton (QuotSMulTop x M) := by + refine ⟨fun h ↦ inferInstance, fun h ↦ ?_⟩ + by_contra! + exact (not_subsingleton_iff_nontrivial.mpr (nontrivial_quotSMulTop_of_mem_maximalIdeal M mem)) h + have aux (n : ℕ) : + injectiveDimension (ModuleCat.of (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) + 1 ≤ n ↔ + injectiveDimension M ≤ n := by + match n with + | 0 => + simp only [CharP.cast_eq_zero, ENat.WithBot.add_one_le_zero_iff, + injectiveDimension_eq_bot_iff, ModuleCat.isZero_of_iff_subsingleton, ← sub] + rw [← ModuleCat.isZero_of_iff_subsingleton (R := R), ← injectiveDimension_eq_bot_iff] + refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩ + rw [← Nat.cast_zero, ← ENat.WithBot.lt_add_one_iff, Nat.cast_zero, zero_add, ← Nat.cast_one, + injectiveDimension_lt_iff_of_finite.{v} M 1] at h + apply WithBot.lt_coe_bot.mp + simp only [ModuleCat.of_coe, bot_eq_zero', WithBot.coe_zero] + apply (injectiveDimension_lt_iff_of_finite.{v} M 0).mpr (fun i _ ↦ ?_) + by_cases eq0 : i = 0 + · rw [eq0, Ext.homEquiv₀.subsingleton_congr, ModuleCat.homEquiv.subsingleton_congr] + apply subsingleton_of_forall_eq 0 (fun f ↦ ?_) + ext y + have : x ∈ Module.annihilator R (Shrink.{v} (R ⧸ maximalIdeal R)) := by + simpa [(Shrink.linearEquiv R _).annihilator_eq, Ideal.annihilator_quotient] using mem + apply IsSMulRegular.right_eq_zero_of_smul regM + rw [← map_smul, Module.mem_annihilator.mp this, map_zero] + · exact h i (Nat.one_le_iff_ne_zero.mpr eq0) + | n + 1 => + rw [← Nat.cast_one, Nat.cast_add, ENat.WithBot.add_le_add_natCast_right_iff, ← Nat.cast_add, + ← ENat.WithBot.lt_add_one_iff, ← ENat.WithBot.lt_add_one_iff, ← Nat.cast_one, + ← Nat.cast_add, ← Nat.cast_add, injectiveDimension_lt_iff_of_finite.{v}, + injectiveDimension_lt_iff_of_finite.{v}] + refine ⟨fun h i hi ↦ ?_, fun h i hi ↦ ?_⟩ + · have : i - 1 + 1 = i := by omega + rw [← this, ext_residueField_subsingleton_iff regR regM mem (i - 1)] + exact h (i - 1) (Nat.le_sub_one_of_lt hi) + · rw [← ext_residueField_subsingleton_iff regR regM mem i] + exact h (i + 1) (Nat.add_le_add_right hi 1) + refine eq_of_forall_ge_iff (fun N ↦ ?_) + induction N with + | bot => + simp [injectiveDimension_eq_bot_iff, ModuleCat.isZero_of_iff_subsingleton, + ModuleCat.isZero_of_iff_subsingleton (M := M), sub] + | coe N => + induction N with + | top => simp + | coe n => simpa using aux n + +end