Diagonal Ext from linear graded resolutions

A linear graded projective resolution has its term in homological degree n generated in internal degree n. Against a graded module concentrated in degree j, that term has no nonzero degree-zero map unless n = j. Consequently Extⁿ(M,N) vanishes off the diagonal. In positive diagonal degrees it is naturally the module of graded maps from the corresponding resolution term to N: both adjacent differentials of the Hom complex vanish.

For a target concentrated in degree zero, its shift N{j} is concentrated in degree j. Thus the convention here is Extⁿ(M,N{j}) = 0 for n ≠ j. These results require neither a field nor a nonnegative algebra grading, and do not assert the converse existence of a linear resolution from diagonal Ext vanishing.

References

• A. Beilinson, V. Ginzburg and W. Soergel, "Koszul duality patterns in representation theory", Section 1.2, for linear resolutions and the diagonal Ext criterion.
• Charles A. Weibel, An Introduction to Homological Algebra, Section 2.4, for computation of Ext by projective resolutions.

theorem TauCeti.GradedProjectiveResolution.IsLinear.hom_eq_zero {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} (hr : r.IsLinear) (n : ℕ) (hN : N.grading.piece ↑n = ⊥) (f : r.termObj n ⟶ N) : f = 0

A term of a linear resolution has no nonzero graded map to a target whose piece in the term's generating degree vanishes.

theorem TauCeti.GradedProjectiveResolution.IsLinear.subsingleton_ext_of_piece_eq_bot {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsLinear) (n : ℕ) (hN : N.grading.piece ↑n = ⊥) : Subsingleton (CategoryTheory.Abelian.Ext M N n)

The nth Ext group vanishes if the target piece in degree n vanishes and the source has a linear resolution.

theorem TauCeti.GradedProjectiveResolution.IsLinear.subsingleton_ext_of_ne {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsLinear) (j : ℤ) (hN : ∀ (p : ℤ), p ≠ j → N.grading.piece p = ⊥) (n : ℕ) (hn : ↑n ≠ j) : Subsingleton (CategoryTheory.Abelian.Ext M N n)

A linear resolution forces Ext against a target concentrated in degree j to vanish outside cohomological degree j.

theorem TauCeti.GradedProjectiveResolution.IsLinear.subsingleton_ext_shiftObj_of_ne {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsLinear) (hN : ∀ (p : ℤ), p ≠ 0 → N.grading.piece p = ⊥) (n : ℕ) (j : ℤ) (hn : ↑n ≠ j) : Subsingleton (CategoryTheory.Abelian.Ext M (N.shiftObj j) n)

With the convention (N{j})ₚ = Nₚ₋ⱼ, a target concentrated in degree zero satisfies Extⁿ(M,N{j}) = 0 whenever n ≠ j and M has a linear resolution.

noncomputable def TauCeti.GradedProjectiveResolution.IsLinear.extLinearEquiv {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsLinear) (n : ℕ) (hprev : N.grading.piece ↑n = ⊥) (hnext : N.grading.piece (↑n + 2) = ⊥) : (r.termObj (n + 1) ⟶ N) ≃ₗ[k] CategoryTheory.Abelian.Ext M N (n + 1)

In positive degree, if the two adjacent target pieces vanish, a linear resolution computes Ext as the graded Hom module from its corresponding term.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GradedProjectiveResolution.IsLinear.extLinearEquiv_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsLinear) (n : ℕ) (hprev : N.grading.piece ↑n = ⊥) (hnext : N.grading.piece (↑n + 2) = ⊥) (f : r.termObj (n + 1) ⟶ N) : (hr.extLinearEquiv n hprev hnext) f = r.toProjectiveResolution.extMk (CategoryTheory.CategoryStruct.comp (r.toProjectiveResolutionXIso (n + 1)).hom f) (n + 2) ⋯ ⋯

The diagonal Ext identification sends a graded map to its projective-resolution class.

noncomputable def TauCeti.GradedProjectiveResolution.IsLinear.extLinearEquivShiftObj {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsLinear) (hN : ∀ (p : ℤ), p ≠ 0 → N.grading.piece p = ⊥) (n : ℕ) : (r.termObj (n + 1) ⟶ N.shiftObj (↑n + 1)) ≃ₗ[k] CategoryTheory.Abelian.Ext M (N.shiftObj (↑n + 1)) (n + 1)

Against a degree-zero target, positive diagonal Ext is the graded Hom module from the resolution term to the target shifted by its homological degree.

Equations

• hr.extLinearEquivShiftObj hN n = hr.extLinearEquiv n ⋯ ⋯

@[simp]

theorem TauCeti.GradedProjectiveResolution.IsLinear.extLinearEquivShiftObj_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] {M N : GradedModuleCat 𝒜} {r : GradedProjectiveResolution 𝒜 M.grading} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (hr : r.IsLinear) (hN : ∀ (p : ℤ), p ≠ 0 → N.grading.piece p = ⊥) (n : ℕ) (f : r.termObj (n + 1) ⟶ N.shiftObj (↑n + 1)) : (hr.extLinearEquivShiftObj hN n) f = r.toProjectiveResolution.extMk (CategoryTheory.CategoryStruct.comp (r.toProjectiveResolutionXIso (n + 1)).hom f) (n + 2) ⋯ ⋯

The shift-diagonal identification sends a graded map to its projective-resolution class.