Documentation

TauCeti.Algebra.Category.ModuleCat.Projective.MinimalResolution.Basic

Minimal finite resolutions over a local ring #

Let (R, π”ͺ, k) be a local ring. A finite resolution

K₁ β†ͺ Qβ‚€ β†  M,   Kβ‚‚ β†ͺ Q₁ β†  K₁,   …,   Kβ‚™ β†ͺ Qₙ₋₁ β†  Kₙ₋₁

of an R-module M is minimal if every syzygy Kα΅’β‚Šβ‚ lies in π”ͺ β€’ Qα΅’. In the spliced complex 0 β†’ Kβ‚™ β†’ Qₙ₋₁ β†’ β‹― β†’ Qβ‚€ β†’ M β†’ 0 the image of each differential other than the augmentation Qβ‚€ β†  M is a syzygy (the maps Qα΅’ β†  Kα΅’ are surjective), so minimality says exactly that every differential of the unaugmented complex 0 β†’ Kβ‚™ β†’ Qₙ₋₁ β†’ β‹― β†’ Qβ‚€ β†’ 0 has image in π”ͺ times its target, i.e. that these differentials vanish after applying k βŠ— -. This is the form in which minimality enters the proof that the projective dimension of k is at least the embedding dimension dim_k π”ͺ/π”ͺΒ² (Stacks 00OA): a comparison map from a Koszul complex into a minimal resolution of k stays injective after applying k βŠ— -.

The main result is that over a Noetherian local ring, a finite module of projective dimension at most n has a minimal resolution of length at most n by finite projective, hence finite free, modules. The resolution is built directly from minimal covers: at each step, M is covered by R ^ ΞΌ(M) with kernel in π”ͺ β€’ R ^ ΞΌ(M) (TauCeti.IsLocalRing.exists_surjective_ker_le_maximalIdeal_smul), and dimension shifting makes the last syzygy projective. This refines TauCeti.exists_finiteProjectiveResolution_of_hasProjectiveDimensionLE, which uses arbitrary finite free covers.

Main definitions #

Main results #

References #

source
inductive TauCeti.ExactStructure.FiniteResolution.IsMinimal {R : Type u} [CommRing R] [IsLocalRing R] {E : ExactStructure (ModuleCat R)} {P : CategoryTheory.ObjectProperty (ModuleCat R)} {X : ModuleCat R} :
E.FiniteResolution P X β†’ Prop

A finite resolution K₁ β†ͺ Qβ‚€ β†  X, Kβ‚‚ β†ͺ Q₁ β†  K₁, … of modules over a local ring (R, π”ͺ) is minimal if every syzygy lies in π”ͺ times the following resolving term: the image of each inclusion Kα΅’β‚Šβ‚ β†ͺ Qα΅’ is contained in π”ͺ β€’ Qα΅’. Equivalently, every differential of the spliced unaugmented complex 0 β†’ Kβ‚™ β†’ Qₙ₋₁ β†’ β‹― β†’ Qβ‚€ has image in π”ͺ times its target; the augmentation Qβ‚€ β†  X is excluded, being surjective.

Instances For
    source
    @[simp]
    theorem TauCeti.ExactStructure.FiniteResolution.isMinimal_base {R : Type u} [CommRing R] [IsLocalRing R] {E : ExactStructure (ModuleCat R)} {P : CategoryTheory.ObjectProperty (ModuleCat R)} {X : ModuleCat R} (hX : P X) :
    (base hX).IsMinimal
    source
    @[simp]
    theorem TauCeti.ExactStructure.FiniteResolution.isMinimal_step_iff {R : Type u} [CommRing R] [IsLocalRing R] {E : ExactStructure (ModuleCat R)} {P : CategoryTheory.ObjectProperty (ModuleCat R)} {K Q X : ModuleCat R} (hQ : P Q) (i : K ⟢ Q) (p : Q ⟢ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, Xβ‚‚ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) :
    (step hQ i p zero hp r).IsMinimal ↔ (ModuleCat.Hom.hom i).range ≀ IsLocalRing.maximalIdeal R β€’ ⊀ ∧ r.IsMinimal
    source
    theorem TauCeti.exists_minimal_finiteProjectiveResolution_of_hasProjectiveDimensionLE {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {M : ModuleCat R} [Module.Finite R ↑M] {n : β„•} (hM : CategoryTheory.HasProjectiveDimensionLE M n) :
    βˆƒ (r : (ExactStructure.abelian (ModuleCat R)).FiniteResolution (finiteProjectiveModules R) M), r.length ≀ n ∧ r.IsMinimal

    Minimal finite resolutions. Over a Noetherian local ring (R, π”ͺ), a finite module of projective dimension at most n has a minimal resolution of length at most n by finite projective modules: every syzygy lies in π”ͺ times the following resolving term.

    Over a local ring the finite projective terms are free (Module.free_of_flat_of_isLocalRing).