Computing Ext using an injective resolution

Given an injective resolution R of an object Y 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.cocomplex and to make computations in the Ext-group.

TODO

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

instance CategoryTheory.InjectiveResolution.instIsKInjectiveCochainComplex {C : Type u} [Category.{v, u} C] [Abelian C] {Y : C} (R : InjectiveResolution Y) : R.cochainComplex.IsKInjective

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

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

Equations

• R.extEquivCohomologyClass = (CategoryTheory.Localization.SmallShiftedHom.postcompEquiv R.ι' ⋯).trans CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective.symm

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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

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

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

@[simp]

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

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

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