Computing Ext from projective resolutions

Mathlib's CategoryTheory.ProjectiveResolution.isoExt computes Extⁿ(X, Y) from any projective resolution P of X. When two resolutions of X are related by a chain map lying over the identity of X, isoExt_hom_comp_homologyMap identifies the resulting computations.

Mathlib computes Extⁿ(X, Y) from a projective resolution R of X as the n-th cohomology of the complex Hom(R, Y): CategoryTheory.ProjectiveResolution.extMk builds a class from a cocycle, extMk_surjective says every class arises that way, and extMk_eq_zero_iff identifies the coboundaries.

This file records the degenerate case of that computation. If the two differentials of R adjacent to a degree n + 1 die against Y -- that is, if d (n + 2) (n + 1) ≫ f = 0 for every f : Rₙ₊₁ ⟶ Y and d (n + 1) n ≫ g = 0 for every g : Rₙ ⟶ Y -- then in that degree no cocycle condition and no coboundary survives, and Extⁿ⁺¹(X, Y) is the term Hom(Rₙ₊₁, Y), linearly over the coefficient ring.

Degree 0 is deliberately excluded: there Ext⁰(X, Y) is Hom(X, Y), which need not be Hom(R₀, Y).

Main definitions

• CategoryTheory.ProjectiveResolution.extLinearEquiv: the linear equivalence Hom(Rₙ₊₁, Y) ≃ₗ Extⁿ⁺¹(X, Y), sending f to its class.

Main results

• CategoryTheory.ProjectiveResolution.isoExt_hom_comp_homologyMap: computing Ext from two resolutions related by a chain map agrees with the induced map on cohomology.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics 38, Cambridge University Press (1994), Sections 2.2 and 2.4, for independence of Ext from the resolution, and Section 2.5, for Ext computed from a projective resolution.

theorem CategoryTheory.ProjectiveResolution.isoExt_hom_comp_homologyMap {R : Type u_1} [Ring R] {D : Type u_2} [Category.{v_1, u_2} D] [Abelian D] [Linear R D] [EnoughProjectives D] {X : D} (P Q : ProjectiveResolution X) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = P.π.f 0) (n : ℕ) (Y : D) : CategoryStruct.comp (Q.isoExt n Y).hom (HomologicalComplex.homologyMap ((HomologicalComplex.unopFunctor (ModuleCat R) (ComplexShape.down ℕ)).map ((((linearYoneda R D).obj Y).rightOp.mapHomologicalComplex (ComplexShape.down ℕ)).map φ).op) n) = (P.isoExt n Y).hom

Ext computed from two resolutions related by a chain map. If φ : P ⟶ Q is a chain map between projective resolutions of X lying over the identity of X, then computing Extⁿ(X, Y) from Q and precomposing with φ gives the computation from P.

theorem CategoryTheory.ProjectiveResolution.subsingleton_ext_of_subsingleton_hom {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) (n : ℕ) [Subsingleton (R.complex.X n ⟶ Y)] : Subsingleton (Abelian.Ext X Y n)

If the degree-n term of a projective resolution has no nonzero morphism to Y, then Extⁿ(X,Y) vanishes. No condition on the neighboring terms is needed.

noncomputable def CategoryTheory.ProjectiveResolution.extLinearEquiv {C : Type u} [Category.{v, u} C] [Abelian C] {k : Type t} [Ring k] [Linear k C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) (n : ℕ) (h₁ : ∀ (f : R.complex.X (n + 1) ⟶ Y), CategoryStruct.comp (R.complex.d (n + 2) (n + 1)) f = 0) (h₂ : ∀ (g : R.complex.X n ⟶ Y), CategoryStruct.comp (R.complex.d (n + 1) n) g = 0) : (R.complex.X (n + 1) ⟶ Y) ≃ₗ[k] Abelian.Ext X Y (n + 1)

If the two differentials of a projective resolution R of X adjacent to degree n + 1 become zero after applying Hom(-, Y), then Extⁿ⁺¹(X, Y) is the degree n + 1 term of that Hom-complex, k-linearly. The class of f is CategoryTheory.ProjectiveResolution.extMk f.

Equations

• R.extLinearEquiv n h₁ h₂ = LinearEquiv.ofBijective { toFun := fun (f : R.complex.X (n + 1) ⟶ Y) => R.extMk f (n + 2) ⋯ ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯

@[simp]

theorem CategoryTheory.ProjectiveResolution.extLinearEquiv_apply {C : Type u} [Category.{v, u} C] [Abelian C] {k : Type t} [Ring k] [Linear k C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) (n : ℕ) (h₁ : ∀ (f : R.complex.X (n + 1) ⟶ Y), CategoryStruct.comp (R.complex.d (n + 2) (n + 1)) f = 0) (h₂ : ∀ (g : R.complex.X n ⟶ Y), CategoryStruct.comp (R.complex.d (n + 1) n) g = 0) (f : R.complex.X (n + 1) ⟶ Y) : (R.extLinearEquiv n h₁ h₂) f = R.extMk f (n + 2) ⋯ ⋯