Documentation

Mathlib.CategoryTheory.Abelian.Injective.Ext

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.

source
instance CategoryTheory.InjectiveResolution.instIsKInjectiveCochainComplex {C : Type u} [Category.{v, u} C] [Abelian C] {Y : C} (R : InjectiveResolution Y) :
R.cochainComplex.IsKInjective
source
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
Instances For
    source
    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))) ⋯) ⋯
    source
    @[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
    source
    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
    Instances For
      source
      @[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✝
      source
      @[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✝
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      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.
      Instances For
        source
        @[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 ⋯ ⋯)
        source
        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 ⋯
        source
        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 ⋯
        source
        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 ⋯
        source
        @[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
        source
        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))) ⋯) ⋯
        source
        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
        source
        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 = α
        source
        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 ⋯
        source
        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 ⋯