Ext

📁 Source: Mathlib/CategoryTheory/Abelian/Injective/Ext.lean

Statistics

Metric	Count
Definitions extAddEquivCohomologyClass, extEquivCohomologyClass, extMk	3
Theorems add_extMk, extAddEquivCohomologyClass_apply, extAddEquivCohomologyClass_symm_apply, extEquivCohomologyClass_add, extEquivCohomologyClass_extMk, extEquivCohomologyClass_neg, extEquivCohomologyClass_sub, extEquivCohomologyClass_symm_add, extEquivCohomologyClass_symm_mk_hom, extEquivCohomologyClass_symm_neg, extEquivCohomologyClass_symm_sub, extEquivCohomologyClass_symm_zero, extEquivCohomologyClass_zero, extMk_comp_mk₀, extMk_eq_zero_iff, extMk_hom, extMk_surjective, extMk_zero, instIsKInjectiveCochainComplex, mk₀_comp_extMk, neg_extMk, sub_extMk	22
Total	25

CategoryTheory.InjectiveResolution

Definitions

Name	Category	Theorems
extAddEquivCohomologyClass 📖	CompOp	2 math math: extAddEquivCohomologyClass_symm_apply, extAddEquivCohomologyClass_apply
extEquivCohomologyClass 📖	CompOp	12 math math: extEquivCohomologyClass_symm_neg, extEquivCohomologyClass_symm_add, extEquivCohomologyClass_symm_sub, extEquivCohomologyClass_sub, extEquivCohomologyClass_neg, extEquivCohomologyClass_symm_zero, extEquivCohomologyClass_add, extEquivCohomologyClass_zero, extEquivCohomologyClass_extMk, extEquivCohomologyClass_symm_mk_hom, extAddEquivCohomologyClass_symm_apply, extAddEquivCohomologyClass_apply
extMk 📖	CompOp	10 math math: extMk_comp_mk₀, extMk_surjective, add_extMk, extMk_zero, extMk_eq_zero_iff, sub_extMk, mk₀_comp_extMk, extMk_hom, neg_extMk, extEquivCohomologyClass_extMk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_extMk 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Abelian.Ext AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup extMk CategoryTheory.Preadditive.homGroup	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Preadditive.add_comp CochainComplex.HomComplex.Cocycle.fromSingleMk.congr_simp cochainComplex_d CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CochainComplex.HomComplex.Cocycle.fromSingleMk_add extEquivCohomologyClass_symm_add
extAddEquivCohomologyClass_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe AddEquiv CategoryTheory.Abelian.Ext CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup CochainComplex.HomComplex.instAddCommGroupCohomologyClass EquivLike.toFunLike AddEquiv.instEquivLike extAddEquivCohomologyClass Equiv Equiv.instEquivLike extEquivCohomologyClass	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd
extAddEquivCohomologyClass_symm_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe AddEquiv CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex CategoryTheory.Abelian.Ext AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCohomologyClass CategoryTheory.Abelian.Ext.instAddCommGroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm extAddEquivCohomologyClass Equiv Equiv.instEquivLike Equiv.symm extEquivCohomologyClass	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor AddRightCancelSemigroup.toIsRightCancelAdd
extEquivCohomologyClass_add 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CategoryTheory.Abelian.Ext CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex EquivLike.toFunLike Equiv.instEquivLike extEquivCohomologyClass AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup CochainComplex.HomComplex.instAddCommGroupCohomologyClass	—	CategoryTheory.Abelian.hasZeroObject AddEquiv.map_add AddRightCancelSemigroup.toIsRightCancelAdd
extEquivCohomologyClass_extMk 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	DFunLike.coe Equiv CategoryTheory.Abelian.Ext CochainComplex.HomComplex.CohomologyClass CategoryTheory.Functor.obj CochainComplex AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory CochainComplex.singleFunctor cochainComplex EquivLike.toFunLike Equiv.instEquivLike extEquivCohomologyClass extMk CochainComplex.HomComplex.Cocycle.fromSingleMk CategoryTheory.Iso.inv cochainComplexXIso zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd zero_add Equiv.apply_symm_apply
extEquivCohomologyClass_neg 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CategoryTheory.Abelian.Ext CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex EquivLike.toFunLike Equiv.instEquivLike extEquivCohomologyClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup CochainComplex.HomComplex.instAddCommGroupCohomologyClass	—	CategoryTheory.Abelian.hasZeroObject AddEquiv.map_neg AddRightCancelSemigroup.toIsRightCancelAdd
extEquivCohomologyClass_sub 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CategoryTheory.Abelian.Ext CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex EquivLike.toFunLike Equiv.instEquivLike extEquivCohomologyClass SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Abelian.Ext.instAddCommGroup CochainComplex.HomComplex.instAddCommGroupCohomologyClass	—	CategoryTheory.Abelian.hasZeroObject AddEquiv.map_sub AddRightCancelSemigroup.toIsRightCancelAdd
extEquivCohomologyClass_symm_add 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex CategoryTheory.Abelian.Ext EquivLike.toFunLike Equiv.instEquivLike Equiv.symm extEquivCohomologyClass AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCohomologyClass CategoryTheory.Abelian.Ext.instAddCommGroup	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.CohomologyClass.mk_surjective CategoryTheory.Abelian.Ext.ext DerivedCategory.instIsIsoMapCochainComplexIntQ instQuasiIsoIntι' zero_add add_zero extEquivCohomologyClass_symm_mk_hom CategoryTheory.ShiftedHom.comp.congr_simp map_add AddMonoidHomClass.toAddHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass CategoryTheory.Functor.map_add DerivedCategory.instAdditiveCochainComplexIntQ CategoryTheory.Preadditive.add_comp CategoryTheory.ShiftedHom.add_comp CategoryTheory.ShiftedHom.comp_add DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Abelian.Ext.add_hom
extEquivCohomologyClass_symm_mk_hom 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Abelian.Ext.hom DFunLike.coe Equiv CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex CategoryTheory.Abelian.Ext EquivLike.toFunLike Equiv.instEquivLike Equiv.symm extEquivCohomologyClass CategoryTheory.ShiftedHom.comp DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt DerivedCategory.singleFunctor CategoryTheory.Functor.comp DerivedCategory.Q AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.ShiftedHom.mk₀ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category DerivedCategory.singleFunctorIsoCompQ CategoryTheory.ShiftedHom.map CochainComplex.instHasShiftInt AddEquiv CochainComplex.HomComplex.Cocycle Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom AddEquiv.instEquivLike AddEquiv.symm CochainComplex.HomComplex.Cocycle.equivHomShift DerivedCategory.instCommShiftCochainComplexIntQ CategoryTheory.CategoryStruct.comp CategoryTheory.inv CategoryTheory.Functor.map ι' DerivedCategory.instIsIsoMapCochainComplexIntQ instQuasiIsoIntι' CategoryTheory.Iso.inv zero_add add_zero	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd DerivedCategory.instIsIsoMapCochainComplexIntQ instQuasiIsoIntι' zero_add add_zero CategoryTheory.categoryWithHomology_of_abelian DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat HomologicalComplex.instIsSupportedOfIsStrictlySupported CochainComplex.instIsStrictlyGEObjIntSingleFunctor CochainComplex.instIsStrictlyLEObjIntSingleFunctor instIsStrictlyGECochainComplexOfNatInt_1 instIsLECochainComplexOfNatInt CategoryTheory.Localization.inverts CategoryTheory.Localization.SmallShiftedHom.equiv_comp CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀Inv CategoryTheory.ShiftedHom.mk₀_id_comp CategoryTheory.IsIso.hom_inv_id
extEquivCohomologyClass_symm_neg 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex CategoryTheory.Abelian.Ext EquivLike.toFunLike Equiv.instEquivLike Equiv.symm extEquivCohomologyClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCohomologyClass CategoryTheory.Abelian.Ext.instAddCommGroup	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.map_neg
extEquivCohomologyClass_symm_sub 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex CategoryTheory.Abelian.Ext EquivLike.toFunLike Equiv.instEquivLike Equiv.symm extEquivCohomologyClass SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCohomologyClass CategoryTheory.Abelian.Ext.instAddCommGroup	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.map_sub
extEquivCohomologyClass_symm_zero 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex CategoryTheory.Abelian.Ext EquivLike.toFunLike Equiv.instEquivLike Equiv.symm extEquivCohomologyClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCohomologyClass CategoryTheory.Abelian.Ext.instAddCommGroup	—	CategoryTheory.Abelian.hasZeroObject AddEquiv.map_zero AddRightCancelSemigroup.toIsRightCancelAdd
extEquivCohomologyClass_zero 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CategoryTheory.Abelian.Ext CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.singleFunctor CategoryTheory.Abelian.hasZeroObject cochainComplex EquivLike.toFunLike Equiv.instEquivLike extEquivCohomologyClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup CochainComplex.HomComplex.instAddCommGroupCohomologyClass	—	CategoryTheory.Abelian.hasZeroObject AddEquiv.map_zero AddRightCancelSemigroup.toIsRightCancelAdd
extMk_comp_mk₀ 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Abelian.Ext.comp extMk CategoryTheory.Abelian.Ext.mk₀ add_zero AddMonoid.toAddZeroClass Nat.instAddMonoid HomologicalComplex.Hom.f Hom.hom	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.Ext.ext add_zero CategoryTheory.Category.assoc Hom.hom'_f CategoryTheory.Iso.inv_hom_id_assoc zero_add DerivedCategory.instIsIsoMapCochainComplexIntQ instQuasiIsoIntι' CategoryTheory.Abelian.Ext.comp_hom CategoryTheory.ShiftedHom.comp.congr_simp extMk_hom CategoryTheory.Abelian.Ext.mk₀_hom CochainComplex.HomComplex.Cocycle.fromSingleMk.congr_simp cochainComplex_d Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CochainComplex.HomComplex.Cocycle.fromSingleMk_postcomp CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp CategoryTheory.ShiftedHom.comp_mk₀ CategoryTheory.ShiftedHom.map_comp CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero CategoryTheory.ShiftedHom.comp_assoc CategoryTheory.ShiftedHom.map_mk₀ CategoryTheory.ShiftedHom.mk₀_comp_mk₀ CategoryTheory.NatTrans.naturality CategoryTheory.Functor.map_comp CategoryTheory.Functor.congr_map Hom.ι'_comp_hom'
extMk_eq_zero_iff 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	extMk CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd zero_add Equiv.apply_eq_iff_eq extEquivCohomologyClass_extMk extEquivCohomologyClass_zero CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iff cochainComplex_d CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc
extMk_hom 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Abelian.Ext.hom extMk CategoryTheory.ShiftedHom.comp DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.Functor.comp CochainComplex AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory CochainComplex.singleFunctor DerivedCategory.Q AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.ShiftedHom.mk₀ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category DerivedCategory.singleFunctorIsoCompQ cochainComplex CategoryTheory.ShiftedHom.map CochainComplex.instHasShiftInt DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle CategoryTheory.shiftFunctor AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm CochainComplex.HomComplex.Cocycle.equivHomShift CochainComplex.HomComplex.Cocycle.fromSingleMk CategoryTheory.Iso.inv cochainComplexXIso zero_add DerivedCategory.instCommShiftCochainComplexIntQ CategoryTheory.inv CategoryTheory.Functor.map ι' DerivedCategory.instIsIsoMapCochainComplexIntQ instQuasiIsoIntι' add_zero	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd extEquivCohomologyClass_symm_mk_hom
extMk_surjective 📖	mathematical	CategoryTheory.HasExt	extMk	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd Equiv.surjective CochainComplex.HomComplex.CohomologyClass.mk_surjective zero_add CochainComplex.HomComplex.Cocycle.fromSingleMk_surjective CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.zero_comp cochainComplex_d CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CochainComplex.HomComplex.Cocycle.fromSingleMk.congr_simp
extMk_zero 📖	mathematical	CategoryTheory.HasExt	extMk Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Abelian.Ext NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.zero_comp CochainComplex.HomComplex.Cocycle.fromSingleMk.congr_simp CochainComplex.HomComplex.Cocycle.fromSingleMk_zero extEquivCohomologyClass_symm_zero
instIsKInjectiveCochainComplex 📖	mathematical	—	CochainComplex.IsKInjective cochainComplex CategoryTheory.Abelian.hasZeroObject CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Abelian.hasZeroObject CochainComplex.isKInjective_of_injective instIsStrictlyGECochainComplexOfNatInt_1 instInjectiveXIntCochainComplex
mk₀_comp_extMk 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Abelian.Ext.comp CategoryTheory.Abelian.Ext.mk₀ extMk zero_add AddMonoid.toAddZeroClass Nat.instAddMonoid	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.Ext.ext zero_add DerivedCategory.instIsIsoMapCochainComplexIntQ instQuasiIsoIntι' add_zero CategoryTheory.Category.assoc CategoryTheory.Abelian.Ext.comp_hom CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.Abelian.Ext.mk₀_hom extEquivCohomologyClass_symm_mk_hom CochainComplex.HomComplex.Cocycle.fromSingleMk.congr_simp cochainComplex_d CategoryTheory.Iso.inv_hom_id_assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CochainComplex.HomComplex.Cocycle.fromSingleMk_precomp CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp CategoryTheory.ShiftedHom.mk₀_comp CategoryTheory.ShiftedHom.map_comp CategoryTheory.ShiftedHom.comp_assoc CategoryTheory.ShiftedHom.mk₀_comp_mk₀ CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.NatTrans.naturality CategoryTheory.ShiftedHom.map_mk₀ CategoryTheory.ShiftedHom.mk₀_comp_mk₀_assoc
neg_extMk 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Abelian.Ext NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Abelian.Ext.instAddCommGroup extMk CategoryTheory.Preadditive.homGroup	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Preadditive.neg_comp CochainComplex.HomComplex.Cocycle.fromSingleMk.congr_simp cochainComplex_d CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CochainComplex.HomComplex.Cocycle.fromSingleMk_neg extEquivCohomologyClass_symm_neg
sub_extMk 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne cocomplex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Abelian.Ext SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Abelian.Ext.instAddCommGroup extMk CategoryTheory.Preadditive.homGroup	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Preadditive.sub_comp CochainComplex.HomComplex.Cocycle.fromSingleMk.congr_simp cochainComplex_d CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CochainComplex.HomComplex.Cocycle.fromSingleMk_sub extEquivCohomologyClass_symm_sub

---

← Back to Index