ShortExact

📁 Source: Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean

Statistics

Metric	Count
Definitions descShortComplex	1
Theorems homologySequenceδ_quotient_mapTriangle_obj, homologySequenceδ_quotient_mapTriangle_obj_assoc, homologySequenceδ_triangleh, inl_v_descShortComplex_f, inl_v_descShortComplex_f_assoc, inr_descShortComplex, inr_descShortComplex_assoc, inr_f_descShortComplex_f, inr_f_descShortComplex_f_assoc, map_descShortComplex, quasiIso_descShortComplex	11
Total	12

CochainComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homologySequenceδ_quotient_mapTriangle_obj 📖	mathematical	—	CategoryTheory.Functor.homologySequenceδ HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift HomotopyCategory.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian HomotopyCategory.instShiftSequenceIntUpHomologyFunctorOfNat CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory instHasShiftInt CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.mapTriangle HomotopyCategory.quotient HomotopyCategory.commShiftQuotient CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Pretriangulated.Triangle.obj₃ CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.homologyFunctor CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category HomotopyCategory.homologyFunctorFactors CategoryTheory.Functor.shift Int.instAddMonoid instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat CategoryTheory.Functor.shiftMap CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd HomotopyCategory.homologyFunctor_shiftMap CategoryTheory.categoryWithHomology_of_abelian instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono
homologySequenceδ_quotient_mapTriangle_obj_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory CategoryTheory.Functor.shift HomotopyCategory.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid HomotopyCategory.hasShift HomotopyCategory.instShiftSequenceIntUpHomologyFunctorOfNat CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory instHasShiftInt CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.mapTriangle HomotopyCategory.quotient HomotopyCategory.commShiftQuotient CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.homologySequenceδ HomologicalComplex.homologyFunctor CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category HomotopyCategory.homologyFunctorFactors instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat CategoryTheory.Functor.shiftMap CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologySequenceδ_quotient_mapTriangle_obj

CochainComplex.mappingCone

Definitions

Name	Category	Theorems
descShortComplex 📖	CompOp	9 math math: homologySequenceδ_triangleh, inr_f_descShortComplex_f_assoc, inr_descShortComplex_assoc, quasiIso_descShortComplex, inl_v_descShortComplex_f_assoc, inr_descShortComplex, inl_v_descShortComplex_f, inr_f_descShortComplex_f, map_descShortComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homologySequenceδ_triangleh 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instHasZeroMorphisms	CategoryTheory.Functor.homologySequenceδ HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift HomotopyCategory.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian HomotopyCategory.instShiftSequenceIntUpHomologyFunctorOfNat triangleh CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.ShortComplex.X₁ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup HomologicalComplex.instCategory AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instHasZeroMorphisms CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Functor.comp HomotopyCategory.quotient CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X HomologicalComplex.homologyFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category HomotopyCategory.homologyFunctorFactors HomologicalComplex.homology CategoryTheory.ShortComplex.X₃ CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc HomologicalComplex.homologyMap descShortComplex CategoryTheory.ShortComplex.ShortExact.δ CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.hasBinaryBiproducts CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.Functor.instIsSplitMonoApp CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.inv_app_isIso CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.Functor.map_injective CategoryTheory.Yoneda.yoneda_faithful CategoryTheory.NatTrans.ext' CategoryTheory.types_ext CochainComplex.next HomologicalComplex.eq_liftCycles_homologyπ_up_to_refinements CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc CategoryTheory.Category.comp_id Mathlib.Tactic.Reassoc.eq_whisker' HomologicalComplex.homologyπ_naturality_assoc HomologicalComplex.liftCycles_comp_cyclesMap_assoc decomp_to CategoryTheory.Preadditive.add_comp inl_v_descShortComplex_f CategoryTheory.Limits.comp_zero inr_f_descShortComplex_f zero_add HomologicalComplex.liftCycles.congr_simp CategoryTheory.Preadditive.neg_comp add_zero CategoryTheory.Limits.zero_comp inl_v_snd_v_assoc inl_v_fst_v_assoc CategoryTheory.Preadditive.comp_add d_snd_v inr_f_snd_v neg_eq_zero CategoryTheory.Preadditive.comp_neg d_fst_v inr_f_fst_v inr_f_d ext_to_iff ComplexShape.next_eq' CategoryTheory.ShortComplex.ShortExact.δ_eq CochainComplex.liftCycles_shift_homologyπ_assoc inl_v_triangle_mor₃_f_assoc CategoryTheory.Iso.inv_hom_id inr_f_triangle_mor₃_f_assoc
inl_v_descShortComplex_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.ShortComplex.X₁ CochainComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CochainComplex.mappingCone CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.ShortComplex.X₃ CochainComplex.HomComplex.Cochain.v inl HomologicalComplex.Hom.f descShortComplex Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts inl_v_desc_f
inl_v_descShortComplex_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.ShortComplex.X₁ CochainComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CochainComplex.mappingCone CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CochainComplex.HomComplex.Cochain.v inl CategoryTheory.ShortComplex.X₃ HomologicalComplex.Hom.f descShortComplex Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_v_descShortComplex_f
inr_descShortComplex 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.X₂ HomologicalComplex.instHasZeroMorphisms CochainComplex.mappingCone CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts HomologicalComplex.X CategoryTheory.ShortComplex.X₃ inr descShortComplex CategoryTheory.ShortComplex.g	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts inr_desc
inr_descShortComplex_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.X₂ HomologicalComplex.instHasZeroMorphisms CochainComplex.mappingCone CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts HomologicalComplex.X inr CategoryTheory.ShortComplex.X₃ descShortComplex CategoryTheory.ShortComplex.g	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_descShortComplex
inr_f_descShortComplex_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.ShortComplex.X₂ CochainComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CochainComplex.mappingCone CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.ShortComplex.X₃ HomologicalComplex.Hom.f inr descShortComplex CategoryTheory.ShortComplex.g	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts inr_f_desc_f
inr_f_descShortComplex_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.ShortComplex.X₂ CochainComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CochainComplex.mappingCone CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts HomologicalComplex.Hom.f inr CategoryTheory.ShortComplex.X₃ descShortComplex CategoryTheory.ShortComplex.g	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_f_descShortComplex_f
map_descShortComplex 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.mappingCone CategoryTheory.ShortComplex.X₁ HomologicalComplex.instHasZeroMorphisms CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts HomologicalComplex.X CategoryTheory.ShortComplex.X₃ map CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.ShortComplex.Hom.τ₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ShortComplex.Hom.comm₁₂ descShortComplex CategoryTheory.ShortComplex.Hom.τ₃	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.ShortComplex.Hom.comm₁₂ ext_from_iff inl_v_desc_f_assoc zero_add add_zero CochainComplex.HomComplex.Cochain.zero_cochain_comp_v CochainComplex.HomComplex.Cochain.ofHom_v CategoryTheory.Category.assoc inl_v_descShortComplex_f CategoryTheory.Limits.comp_zero inl_v_descShortComplex_f_assoc CategoryTheory.Limits.zero_comp inr_f_desc_f_assoc inr_f_descShortComplex_f inr_f_descShortComplex_f_assoc CategoryTheory.ShortComplex.Hom.comm₂₃
quasiIso_descShortComplex 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instHasZeroMorphisms	QuasiIso CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CategoryTheory.ShortComplex.X₁ CochainComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts HomologicalComplex.X CategoryTheory.ShortComplex.X₃ descShortComplex CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian quasiIsoAt_iff_isIso_homologyMap instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono CategoryTheory.NatTrans.naturality CategoryTheory.NatTrans.naturality_assoc HomologicalComplex.homologyMap_comp inr_descShortComplex homologySequenceδ_triangleh CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono CategoryTheory.ComposableArrows.Exact.δlast CategoryTheory.Functor.homologySequenceComposableArrows₅_exact HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor HomotopyCategory.instIsHomologicalIntUpHomologyFunctor HomotopyCategory.mappingCone_triangleh_distinguished HomologicalComplex.HomologySequence.composableArrows₅_exact CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.Functor.instIsSplitMonoApp CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.IsIso.of_isIso_comp_left

---

← Back to Index