Auslander-Buchsbaum theorem

In this file, we prove the Auslander-Buchsbaum theorem, which states that for a nontrivial finitely generated module M over a Noetherian local ring R, if projectiveDimension M ≠ ⊤, then projectiveDimension M + IsLocalRing.depth M = IsLocalRing.depth R.

theorem smul_prod_of_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) {ι : Type u_4} [Finite ι] (x : ι → M) (h : ∀ (i : ι), x i ∈ I • ⊤) : x ∈ I • ⊤

theorem mem_smul_top_of_range_le_smul_top {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (I : Ideal R) [Module.Finite R M] [Module.Free R M] (f : M →ₗ[R] N) (hf : f.range ≤ I • ⊤) : f ∈ I • ⊤

theorem ModuleCat.free_of_projective_of_isLocalRing {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] (M : ModuleCat R) [Module.Finite R ↑M] [CategoryTheory.Projective M] : Module.Free R ↑M

theorem nontrivial_ring_of_nontrivial_module {R : Type u} [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [ntr : Nontrivial M] : Nontrivial R

theorem subsingleton_of_pi {α : Type u_1} {β : Type u_2} [Nonempty α] (h : Subsingleton (α → β)) : Subsingleton β

theorem finte_free_ext_vanish_iff {R : Type u} [CommRing R] [Small.{v, u} R] (M N : ModuleCat R) [Module.Finite R ↑M] [Module.Free R ↑M] [Nontrivial ↑M] (i : ℕ) : Subsingleton (CategoryTheory.Abelian.Ext N M i) ↔ Subsingleton (CategoryTheory.Abelian.Ext N (ModuleCat.of R (Shrink.{v, u} R)) i)

theorem free_depth_eq_ring_depth {R : Type u} [CommRing R] [Small.{v, u} R] (M N : ModuleCat R) [Module.Finite R ↑M] [Module.Free R ↑M] [Nontrivial ↑M] : moduleDepth N M = moduleDepth N (ModuleCat.of R (Shrink.{v, u} R))

theorem basis_lift {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Finite R M] (ι : Type u_2) (b : Module.Basis ι (R ⧸ IsLocalRing.maximalIdeal R) (M ⧸ IsLocalRing.maximalIdeal R • ⊤)) (f : (ι →₀ Shrink.{v, u} R) →ₗ[R] M) (hf : (IsLocalRing.maximalIdeal R • ⊤).mkQ ∘ₗ f = ↑(LinearEquiv.restrictScalars R b.repr).symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (IsLocalRing.maximalIdeal R) ∘ₗ ↑(Shrink.linearEquiv R R))) : Function.Surjective ⇑f

instance instFiniteQuotientIdealSubmoduleHSMulTop {R : Type u} [CommRing R] (I : Ideal R) (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Finite R M] : Module.Finite (R ⧸ I) (M ⧸ I • ⊤)

theorem basis_lift_ker_le {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Finite R M] (ι : Type u_2) (b : Module.Basis ι (R ⧸ IsLocalRing.maximalIdeal R) (M ⧸ IsLocalRing.maximalIdeal R • ⊤)) (f : (ι →₀ Shrink.{v, u} R) →ₗ[R] M) (hf : (IsLocalRing.maximalIdeal R • ⊤).mkQ ∘ₗ f = ↑(LinearEquiv.restrictScalars R b.repr).symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (IsLocalRing.maximalIdeal R) ∘ₗ ↑(Shrink.linearEquiv R R))) : f.ker ≤ IsLocalRing.maximalIdeal R • ⊤

theorem ext_hom_zero_of_mem_ideal_smul {R : Type u} [CommRing R] [Small.{v, u} R] (L M N : ModuleCat R) (n : ℕ) (f : M ⟶ N) (mem : f ∈ Module.annihilator R ↑L • ⊤) : AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ f).postcomp L ⋯) = 0

theorem AuslanderBuchsbaum_one {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] [IsLocalRing R] (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (le1 : CategoryTheory.HasProjectiveDimensionLE M 1) (nle0 : ¬CategoryTheory.HasProjectiveDimensionLE M 0) : 1 + IsLocalRing.depth M = IsLocalRing.depth (ModuleCat.of R (Shrink.{v, u} R))

theorem AuslanderBuchsbaum {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] [IsLocalRing R] (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (netop : CategoryTheory.projectiveDimension M ≠ ⊤) : CategoryTheory.projectiveDimension M + ↑(IsLocalRing.depth M) = ↑(IsLocalRing.depth (ModuleCat.of R (Shrink.{v, u} R)))