Computing Ext using a projective resolution

Given a projective resolution R of an object X in an abelian category C, we provide an API in order to construct elements in Ext X Y n in terms of the complex R.complex and to make computations in the Ext-group.

TODO

• Functoriality in Y for a given projective resolution R
• Functoriality in X: this would involve a morphism X ⟶ X', projective resolutions R and R' of X and X', a lift of X ⟶ X' as a morphism of cochain complexes R.complex ⟶ R'.complex; in this context, we should be able to compute the precomposition of an element R.extMk f m hm hf : Ext X' Y n by X ⟶ X'.

instance CategoryTheory.ProjectiveResolution.instIsKProjectiveCochainComplex {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (R : ProjectiveResolution X) : R.cochainComplex.IsKProjective

noncomputable def CategoryTheory.ProjectiveResolution.extEquivCohomologyClass {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} : Abelian.Ext X Y n ≃ CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n

If R is a projective resolution of X, then Ext X Y n identifies to the type of cohomology classes of degree n from R.cochainComplex to (singleFunctor C 0).obj Y.

Equations

• R.extEquivCohomologyClass = (CategoryTheory.Localization.SmallShiftedHom.precompEquiv R.π' ⋯).trans CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective.symm

theorem CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} [HasDerivedCategory C] (x : CochainComplex.HomComplex.Cocycle R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n) : (R.extEquivCohomologyClass.symm (CochainComplex.HomComplex.CohomologyClass.mk x)).hom = (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.π'))).comp (ShiftedHom.map (CochainComplex.HomComplex.Cocycle.equivHomShift.symm x) DerivedCategory.Q) ⋯

@[simp]

theorem CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (x y : CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n) : R.extEquivCohomologyClass.symm (x + y) = R.extEquivCohomologyClass.symm x + R.extEquivCohomologyClass.symm y

noncomputable def CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} : Abelian.Ext X Y n ≃+ CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n

If R is a projective resolution of X, then Ext X Y n identifies to the type of cohomology classes of degree n from R.cochainComplex to (singleFunctor C 0).obj X.

Equations

• R.extAddEquivCohomologyClass = (let __Equiv := R.extEquivCohomologyClass.symm; { toEquiv := __Equiv, map_add' := ⋯ }).symm

@[simp]

theorem CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (a✝ : Abelian.Ext X Y n) : R.extAddEquivCohomologyClass a✝ = R.extEquivCohomologyClass a✝

@[simp]

theorem CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (a✝ : CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n) : R.extAddEquivCohomologyClass.symm a✝ = R.extEquivCohomologyClass.symm a✝

@[simp]

theorem CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (x y : CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n) : R.extEquivCohomologyClass.symm (x - y) = R.extEquivCohomologyClass.symm x - R.extEquivCohomologyClass.symm y

@[simp]

theorem CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (x : CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n) : R.extEquivCohomologyClass.symm (-x) = -R.extEquivCohomologyClass.symm x

@[simp]

theorem CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} : R.extEquivCohomologyClass.symm 0 = 0

@[simp]

theorem CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (x y : Abelian.Ext X Y n) : R.extEquivCohomologyClass (x + y) = R.extEquivCohomologyClass x + R.extEquivCohomologyClass y

@[simp]

theorem CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (x y : Abelian.Ext X Y n) : R.extEquivCohomologyClass (x - y) = R.extEquivCohomologyClass x - R.extEquivCohomologyClass y

@[simp]

theorem CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (x : Abelian.Ext X Y n) : R.extEquivCohomologyClass (-x) = -R.extEquivCohomologyClass x

@[simp]

theorem CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] (X : C) {Y : C} (R : ProjectiveResolution X) (n : ℕ) : R.extEquivCohomologyClass 0 = 0

noncomputable def CategoryTheory.ProjectiveResolution.extMk {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryStruct.comp (R.complex.d m n) f = 0) : Abelian.Ext X Y n

Given a projective resolution R of an object X of an abelian category, this is a constructor for elements in Ext X Y n which takes as an input a "cocycle" f : R.cocomplex.X n ⟶ Y.

Equations

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

@[simp]

theorem CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryStruct.comp (R.complex.d m n) f = 0) : R.extEquivCohomologyClass (R.extMk f m hm hf) = CochainComplex.HomComplex.CohomologyClass.mk (CochainComplex.HomComplex.Cocycle.toSingleMk (CategoryStruct.comp (R.cochainComplexXIso (-↑n) n ⋯).hom f) ⋯ (-↑m) ⋯ ⋯)

theorem CategoryTheory.ProjectiveResolution.add_extMk {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (f g : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryStruct.comp (R.complex.d m n) f = 0) (hg : CategoryStruct.comp (R.complex.d m n) g = 0) : R.extMk f m hm hf + R.extMk g m hm hg = R.extMk (f + g) m hm ⋯

theorem CategoryTheory.ProjectiveResolution.sub_extMk {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (f g : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryStruct.comp (R.complex.d m n) f = 0) (hg : CategoryStruct.comp (R.complex.d m n) g = 0) : R.extMk f m hm hf - R.extMk g m hm hg = R.extMk (f - g) m hm ⋯

theorem CategoryTheory.ProjectiveResolution.neg_extMk {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryStruct.comp (R.complex.d m n) f = 0) : -R.extMk f m hm hf = R.extMk (-f) m hm ⋯

@[simp]

theorem CategoryTheory.ProjectiveResolution.extMk_zero {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (m : ℕ) (hm : n + 1 = m) : R.extMk 0 m hm ⋯ = 0

theorem CategoryTheory.ProjectiveResolution.extMk_eq_zero_iff {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryStruct.comp (R.complex.d m n) f = 0) (p : ℕ) (hp : p + 1 = n) : R.extMk f m hm hf = 0 ↔ ∃ (g : R.complex.X p ⟶ Y), CategoryStruct.comp (R.complex.d n p) g = f

theorem CategoryTheory.ProjectiveResolution.extMk_surjective {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {n : ℕ} (α : Abelian.Ext X Y n) (m : ℕ) (hm : n + 1 = m) : ∃ (f : R.complex.X n ⟶ Y) (hf : CategoryStruct.comp (R.complex.d m n) f = 0), R.extMk f m hm hf = α