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.

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.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp ((ShiftedHom.map (CochainComplex.HomComplex.Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp (ShiftedHom.mk₀ 0 ⋯ (CategoryStruct.comp (inv (DerivedCategory.Q.map R.ι')) ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))) ⋯) ⋯

@[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

@[simp]

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

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.smul_extMk {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : InjectiveResolution Y) {R₀ : Type u_1} [Ring R₀] [Linear R₀ C] (r : R₀) {n : ℕ} (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m) (hf : CategoryStruct.comp f (R.cocomplex.d n m) = 0) : r • R.extMk f m hm hf = R.extMk (r • f) m hm ⋯

theorem CategoryTheory.InjectiveResolution.extMk_hom {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : InjectiveResolution Y) [HasDerivedCategory C] {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).hom = (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp ((ShiftedHom.map (CochainComplex.HomComplex.Cocycle.equivHomShift.symm (CochainComplex.HomComplex.Cocycle.fromSingleMk (CategoryStruct.comp f (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) DerivedCategory.Q).comp (ShiftedHom.mk₀ 0 ⋯ (CategoryStruct.comp (inv (DerivedCategory.Q.map R.ι')) ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))) ⋯) ⋯

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 = α

theorem CategoryTheory.InjectiveResolution.mk₀_comp_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) {X' : C} (g : X' ⟶ X) : (Abelian.Ext.mk₀ g).comp (R.extMk f m hm hf) ⋯ = R.extMk (CategoryStruct.comp g f) m hm ⋯

theorem CategoryTheory.InjectiveResolution.extMk_comp_mk₀ {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) {Y' : C} {R' : InjectiveResolution Y'} {g : Y ⟶ Y'} (φ : R.Hom R' g) : (R.extMk f m hm hf).comp (Abelian.Ext.mk₀ g) ⋯ = R'.extMk (CategoryStruct.comp f (φ.hom.f n)) m hm ⋯

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

If R is an injective resolution of Y in a R₀-linear category, then Ext X Y n identifies to the R₀-module of cohomology classes of degree n from (singleFunctor C 0).obj X to R.cochainComplex.

Equations

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

@[simp]

theorem CategoryTheory.InjectiveResolution.extLinearEquivCohomologyClass_symm_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : InjectiveResolution Y) {n : ℕ} {R₀ : Type u_1} [Ring R₀] [Linear R₀ C] (a✝ : CochainComplex.HomComplex.CohomologyClass ((CochainComplex.singleFunctor C 0).obj X) R.cochainComplex ↑n) : R.extLinearEquivCohomologyClass.symm a✝ = { toFun := ⇑R.extAddEquivCohomologyClass.symm, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑R.extAddEquivCohomologyClass, left_inv := ⋯, right_inv := ⋯ } a✝

@[simp]

theorem CategoryTheory.InjectiveResolution.extLinearEquivCohomologyClass_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : InjectiveResolution Y) {n : ℕ} {R₀ : Type u_1} [Ring R₀] [Linear R₀ C] (a : Abelian.Ext X Y n) : R.extLinearEquivCohomologyClass a = ({ toFun := ⇑R.extAddEquivCohomologyClass.symm, map_add' := ⋯, map_smul' := ⋯ }.inverse ⇑{ toFun := ⇑R.extAddEquivCohomologyClass.symm, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑R.extAddEquivCohomologyClass, left_inv := ⋯, right_inv := ⋯ }.symm ⋯ ⋯) a