The Ext class of a short exact sequence #
In this file, given a short exact short complex S : ShortComplex C
in an abelian category, we construct the associated class in
Ext S.X₃ S.X₁ 1.
instance
CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{S : CategoryTheory.ShortComplex C}
:
CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ
(S.map (CochainComplex.singleFunctor C 0)).X₃ (S.map (CochainComplex.singleFunctor C 0)).X₁
Equations
- ⋯ = ⋯
noncomputable def
CategoryTheory.ShortComplex.ShortExact.extClass
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{S : CategoryTheory.ShortComplex C}
(hS : S.ShortExact)
:
CategoryTheory.Abelian.Ext S.X₃ S.X₁ 1
The class in Ext S.X₃ S.X₁ 1 that is attached to a short exact
short complex S in an abelian category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.extClass_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{S : CategoryTheory.ShortComplex C}
(hS : S.ShortExact)
[HasDerivedCategory C]
:
hS.extClass.hom = hS.singleδ
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.comp_extClass
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{S : CategoryTheory.ShortComplex C}
(hS : S.ShortExact)
:
(CategoryTheory.Abelian.Ext.mk₀ S.g).comp hS.extClass ⋯ = 0
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.extClass_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasExt C]
{S : CategoryTheory.ShortComplex C}
(hS : S.ShortExact)
:
hS.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ S.f) ⋯ = 0