ExactSequences

📁 Source: Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean

Statistics

Metric	Count
Definitions contravariantSequence, covariantSequence	2
Theorems contravariantSequence_exact, contravariant_sequence_exact₁, contravariant_sequence_exact₁', contravariant_sequence_exact₂, contravariant_sequence_exact₂', contravariant_sequence_exact₃, contravariant_sequence_exact₃', covariantSequence_exact, covariant_sequence_exact₁, covariant_sequence_exact₁', covariant_sequence_exact₂, covariant_sequence_exact₂', covariant_sequence_exact₃, covariant_sequence_exact₃', hom_comp_singleFunctor_map_shift, mono_postcomp_mk₀_of_mono, mono_precomp_mk₀_of_epi, postcomp_mk₀_injective_of_mono, preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, preadditiveYoneda_homologySequenceδ_singleTriangle_apply, precomp_mk₀_injective_of_epi, singleFunctor_map_comp_hom	22
Total	24

CategoryTheory.Abelian.Ext

Definitions

Name	Category	Theorems
contravariantSequence 📖	CompOp	1 math math: contravariantSequence_exact
covariantSequence 📖	CompOp	1 math math: covariantSequence_exact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contravariantSequence_exact 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.ComposableArrows.Exact AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.instPreadditive contravariantSequence	—	CategoryTheory.ComposableArrows.exact_of_δ₀ CategoryTheory.ShortComplex.Exact.exact_toComposableArrows zero_add contravariant_sequence_exact₂' contravariant_sequence_exact₁' contravariant_sequence_exact₃'
contravariant_sequence_exact₁ 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive comp CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.ShortExact.extClass CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	CategoryTheory.ShortComplex.X₂ mk₀ CategoryTheory.ShortComplex.f zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid	—	zero_add contravariant_sequence_exact₁' CategoryTheory.ShortComplex.ab_exact_iff
contravariant_sequence_exact₁' 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.ShortComplex.Exact AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.instPreadditive AddCommGrpCat.of CategoryTheory.Abelian.Ext CategoryTheory.ShortComplex.X₂ instAddCommGroup CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₃ AddCommGrpCat.ofHom precomp mk₀ CategoryTheory.ShortComplex.f zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.ShortComplex.ShortExact.extClass	—	DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Functor.comp_homologySequenceδ CategoryTheory.Limits.hasZeroObject_op DerivedCategory.instHasZeroObject CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda CategoryTheory.Pretriangulated.op_distinguished CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished CategoryTheory.Functor.homologySequence_exact₃ zero_add CategoryTheory.ShortComplex.ab_exact_iff_function_exact AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Function.Exact.of_ladder_addEquiv_of_exact' AddMonoidHom.ext singleFunctor_map_comp_hom preadditiveYoneda_homologySequenceδ_singleTriangle_apply
contravariant_sequence_exact₂ 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive comp CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ mk₀ CategoryTheory.ShortComplex.f zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	zero_add contravariant_sequence_exact₂' CategoryTheory.ShortComplex.ab_exact_iff
contravariant_sequence_exact₂' 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.ShortComplex.Exact AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.instPreadditive AddCommGrpCat.of CategoryTheory.Abelian.Ext CategoryTheory.ShortComplex.X₃ instAddCommGroup CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₁ AddCommGrpCat.ofHom precomp mk₀ CategoryTheory.ShortComplex.g zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.ShortComplex.f	—	DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Functor.homologySequence_comp CategoryTheory.Limits.hasZeroObject_op DerivedCategory.instHasZeroObject CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda CategoryTheory.Pretriangulated.op_distinguished CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished CategoryTheory.Functor.homologySequence_exact₂ zero_add CategoryTheory.ShortComplex.ab_exact_iff_function_exact AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Function.Exact.of_ladder_addEquiv_of_exact' AddMonoidHom.ext singleFunctor_map_comp_hom
contravariant_sequence_exact₃ 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive comp CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ mk₀ CategoryTheory.ShortComplex.g zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.ShortExact.extClass	—	zero_add contravariant_sequence_exact₃' CategoryTheory.ShortComplex.ab_exact_iff
contravariant_sequence_exact₃' 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.ShortComplex.Exact AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.instPreadditive AddCommGrpCat.of CategoryTheory.Abelian.Ext CategoryTheory.ShortComplex.X₁ instAddCommGroup CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₂ AddCommGrpCat.ofHom precomp CategoryTheory.ShortComplex.ShortExact.extClass mk₀ CategoryTheory.ShortComplex.g zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid	—	DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Functor.homologySequenceδ_comp CategoryTheory.Limits.hasZeroObject_op DerivedCategory.instHasZeroObject CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda CategoryTheory.Pretriangulated.op_distinguished CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished CategoryTheory.Functor.homologySequence_exact₁ zero_add CategoryTheory.ShortComplex.ab_exact_iff_function_exact AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Function.Exact.of_ladder_addEquiv_of_exact' AddMonoidHom.ext preadditiveYoneda_homologySequenceδ_singleTriangle_apply singleFunctor_map_comp_hom
covariantSequence_exact 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.ComposableArrows.Exact AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.instPreadditive covariantSequence	—	CategoryTheory.ComposableArrows.exact_of_δ₀ CategoryTheory.ShortComplex.Exact.exact_toComposableArrows add_zero covariant_sequence_exact₂' covariant_sequence_exact₃' covariant_sequence_exact₁'
covariant_sequence_exact₁ 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive comp CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ mk₀ CategoryTheory.ShortComplex.f add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.ShortExact.extClass	—	add_zero covariant_sequence_exact₁' CategoryTheory.ShortComplex.ab_exact_iff
covariant_sequence_exact₁' 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.ShortComplex.Exact AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.instPreadditive AddCommGrpCat.of CategoryTheory.Abelian.Ext CategoryTheory.ShortComplex.X₃ instAddCommGroup CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ AddCommGrpCat.ofHom postcomp CategoryTheory.ShortComplex.ShortExact.extClass mk₀ CategoryTheory.ShortComplex.f add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid	—	CategoryTheory.Functor.homologySequenceδ_comp DerivedCategory.instHasZeroObject DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Pretriangulated.instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished CategoryTheory.Functor.homologySequence_exact₁ add_zero CategoryTheory.ShortComplex.ab_exact_iff_function_exact AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Function.Exact.of_ladder_addEquiv_of_exact' AddMonoidHom.ext preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply hom_comp_singleFunctor_map_shift
covariant_sequence_exact₂ 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive comp CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ mk₀ CategoryTheory.ShortComplex.g add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f	—	add_zero covariant_sequence_exact₂' CategoryTheory.ShortComplex.ab_exact_iff
covariant_sequence_exact₂' 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.ShortComplex.Exact AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.instPreadditive AddCommGrpCat.of CategoryTheory.Abelian.Ext CategoryTheory.ShortComplex.X₁ instAddCommGroup CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ AddCommGrpCat.ofHom postcomp mk₀ CategoryTheory.ShortComplex.f add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.ShortComplex.g	—	CategoryTheory.Functor.homologySequence_comp DerivedCategory.instHasZeroObject DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Pretriangulated.instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished CategoryTheory.Functor.homologySequence_exact₂ add_zero CategoryTheory.ShortComplex.ab_exact_iff_function_exact AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Function.Exact.of_ladder_addEquiv_of_exact' AddMonoidHom.ext hom_comp_singleFunctor_map_shift
covariant_sequence_exact₃ 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive comp CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.ShortExact.extClass CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	CategoryTheory.ShortComplex.X₂ mk₀ CategoryTheory.ShortComplex.g add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid	—	add_zero covariant_sequence_exact₃' CategoryTheory.ShortComplex.ab_exact_iff
covariant_sequence_exact₃' 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.ShortComplex.Exact AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.instPreadditive AddCommGrpCat.of CategoryTheory.Abelian.Ext CategoryTheory.ShortComplex.X₂ instAddCommGroup CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ AddCommGrpCat.ofHom postcomp mk₀ CategoryTheory.ShortComplex.g add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid CategoryTheory.ShortComplex.ShortExact.extClass	—	CategoryTheory.Functor.comp_homologySequenceδ DerivedCategory.instHasZeroObject DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Pretriangulated.instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished CategoryTheory.Functor.homologySequence_exact₃ add_zero CategoryTheory.ShortComplex.ab_exact_iff_function_exact AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Function.Exact.of_ladder_addEquiv_of_exact' AddMonoidHom.ext hom_comp_singleFunctor_map_shift preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply
hom_comp_singleFunctor_map_shift 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.CategoryStruct.comp DerivedCategory CategoryTheory.Category.toCategoryStruct DerivedCategory.instCategory CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.shiftFunctor Int.instAddMonoid DerivedCategory.instHasShiftInt hom CategoryTheory.Functor.map comp mk₀ add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid	—	add_zero comp_hom CategoryTheory.ShiftedHom.comp.congr_simp mk₀_hom CategoryTheory.ShiftedHom.comp_mk₀
mono_postcomp_mk₀_of_mono 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Mono AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.of CategoryTheory.Abelian.Ext instAddCommGroup AddCommGrpCat.ofHom postcomp mk₀ add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid	—	add_zero AddCommGrpCat.mono_iff_injective postcomp_mk₀_injective_of_mono
mono_precomp_mk₀_of_epi 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Mono AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.of CategoryTheory.Abelian.Ext instAddCommGroup AddCommGrpCat.ofHom precomp mk₀ zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid	—	zero_add AddCommGrpCat.mono_iff_injective precomp_mk₀_injective_of_epi
postcomp_mk₀_injective_of_mono 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup AddMonoidHom.instFunLike postcomp mk₀ add_zero Nat.instAddMonoid	—	add_zero AddMonoidHom.ker_eq_bot_iff AddSubgroup.eq_bot_iff_forall AddEquiv.surjective CategoryTheory.cancel_mono CategoryTheory.Limits.zero_comp mk₀_comp_mk₀
preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	DFunLike.coe CategoryTheory.Functor.obj DerivedCategory DerivedCategory.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.shift Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.preadditiveCoyoneda DerivedCategory.instPreadditive Opposite.op DerivedCategory.singleFunctor Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Pretriangulated.instShiftSequenceAddCommGrpCatObjOppositeFunctorPreadditiveCoyonedaInt CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.ShortComplex.ShortExact.singleTriangle CategoryTheory.Pretriangulated.Triangle.obj₁ AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.homologySequenceδ hom CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ comp CategoryTheory.ShortComplex.ShortExact.extClass	—	CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply comp_hom CategoryTheory.ShortComplex.ShortExact.extClass_hom CategoryTheory.ShiftedHom.comp.eq_1
preadditiveYoneda_homologySequenceδ_singleTriangle_apply 📖	mathematical	CategoryTheory.HasExt CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	DFunLike.coe CategoryTheory.Functor.obj Opposite DerivedCategory CategoryTheory.Category.opposite DerivedCategory.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.shift CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.preadditiveYoneda DerivedCategory.instPreadditive DerivedCategory.singleFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt DerivedCategory.instHasShiftInt CategoryTheory.Pretriangulated.instShiftSequenceOppositeAddCommGrpCatObjFunctorPreadditiveYonedaInt DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.triangleOpEquivalence Opposite.op CategoryTheory.ShortComplex.ShortExact.singleTriangle CategoryTheory.Pretriangulated.Triangle.obj₁ AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.homologySequenceδ hom CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₃ comp CategoryTheory.ShortComplex.ShortExact.extClass	—	DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply comp_hom CategoryTheory.ShortComplex.ShortExact.extClass_hom CategoryTheory.ShiftedHom.comp.eq_1
precomp_mk₀_injective_of_epi 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup AddMonoidHom.instFunLike precomp mk₀ zero_add Nat.instAddMonoid	—	zero_add AddMonoidHom.ker_eq_bot_iff AddSubgroup.eq_bot_iff_forall AddEquiv.surjective CategoryTheory.cancel_epi CategoryTheory.Limits.comp_zero mk₀_comp_mk₀
singleFunctor_map_comp_hom 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.CategoryStruct.comp DerivedCategory CategoryTheory.Category.toCategoryStruct DerivedCategory.instCategory CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.shiftFunctor Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.map hom comp mk₀ zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid	—	zero_add comp_hom CategoryTheory.ShiftedHom.comp.congr_simp mk₀_hom CategoryTheory.ShiftedHom.mk₀_comp

---

← Back to Index