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.
theorem
CategoryTheory.ShortComplex.ext_mk₀_f_comp_ext_mk₀_g
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
(S : ShortComplex C)
:
(Abelian.Ext.mk₀ S.f).comp (Abelian.Ext.mk₀ S.g) ⋯ = 0
instance
CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
:
Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ
(S.map (CochainComplex.singleFunctor C 0)).X₃ (S.map (CochainComplex.singleFunctor C 0)).X₁
noncomputable def
CategoryTheory.ShortComplex.ShortExact.extClass
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
:
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}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
[HasDerivedCategory C]
:
hS.extClass.hom = hS.singleδ
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.comp_extClass
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
:
(Abelian.Ext.mk₀ S.g).comp hS.extClass ⋯ = 0
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.comp_extClass_assoc
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
{Y : C}
{n : ℕ}
(γ : Abelian.Ext S.X₁ Y n)
{n' : ℕ}
(h : 1 + n = n')
:
(Abelian.Ext.mk₀ S.g).comp (hS.extClass.comp γ h) ⋯ = 0
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.extClass_comp
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
:
hS.extClass.comp (Abelian.Ext.mk₀ S.f) ⋯ = 0
@[simp]
theorem
CategoryTheory.ShortComplex.ShortExact.extClass_comp_assoc
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
{Y : C}
{n : ℕ}
(γ : Abelian.Ext S.X₂ Y n)
{n' : ℕ}
{h : 1 + n = n'}
:
hS.extClass.comp ((Abelian.Ext.mk₀ S.f).comp γ ⋯) h = 0