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.

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

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

@[simp]

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

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 Y.

Equations

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

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

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

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.ProjectiveResolution.extLinearEquivCohomologyClass_apply {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y : C} (R : ProjectiveResolution X) {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