Documentation

Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

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.

source
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
source
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₁
source
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
    source
    @[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δ
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    theorem CategoryTheory.ShortComplex.ShortExact.extClass_naturality {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {S₁ S₂ : ShortComplex C} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) :
    h₁.extClass.comp (Abelian.Ext.mk₀ f.τ₁) ⋯ = (Abelian.Ext.mk₀ f.τ₃).comp h₂.extClass ⋯