Ext

📁 Source: Mathlib/CategoryTheory/Abelian/Projective/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, instIsKProjectiveCochainComplex, mk₀_comp_extMk, neg_extMk, sub_extMk	22
Total	25

CategoryTheory.ProjectiveResolution

Definitions

Name	Category	Theorems
extAddEquivCohomologyClass 📖	CompOp	2 math math: extAddEquivCohomologyClass_symm_apply, extAddEquivCohomologyClass_apply
extEquivCohomologyClass 📖	CompOp	12 math math: extEquivCohomologyClass_add, extEquivCohomologyClass_symm_sub, extEquivCohomologyClass_sub, extEquivCohomologyClass_symm_mk_hom, extEquivCohomologyClass_zero, extAddEquivCohomologyClass_symm_apply, extEquivCohomologyClass_symm_zero, extAddEquivCohomologyClass_apply, extEquivCohomologyClass_neg, extEquivCohomologyClass_extMk, extEquivCohomologyClass_symm_add, extEquivCohomologyClass_symm_neg
extMk 📖	CompOp	10 math math: sub_extMk, extMk_comp_mk₀, extMk_hom, mk₀_comp_extMk, add_extMk, extMk_zero, extMk_eq_zero_iff, extMk_surjective, extEquivCohomologyClass_extMk, neg_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.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne complex 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.comp_add CochainComplex.HomComplex.Cocycle.toSingleMk.congr_simp cochainComplex_d CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.isIso_hom CochainComplex.HomComplex.Cocycle.toSingleMk_add extEquivCohomologyClass_symm_add
extAddEquivCohomologyClass_apply 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe AddEquiv CategoryTheory.Abelian.Ext CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive cochainComplex CategoryTheory.Abelian.hasZeroObject 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 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 cochainComplex CategoryTheory.Abelian.hasZeroObject 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.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 cochainComplex CategoryTheory.Abelian.hasZeroObject 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 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.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne complex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	DFunLike.coe Equiv CategoryTheory.Abelian.Ext CochainComplex.HomComplex.CohomologyClass cochainComplex CategoryTheory.Functor.obj CochainComplex AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up CochainComplex.singleFunctor EquivLike.toFunLike Equiv.instEquivLike extEquivCohomologyClass extMk CochainComplex.HomComplex.Cocycle.toSingleMk CategoryTheory.Iso.hom cochainComplexXIso	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd Equiv.apply_symm_apply
extEquivCohomologyClass_neg 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CategoryTheory.Abelian.Ext CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive cochainComplex CategoryTheory.Abelian.hasZeroObject 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 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 cochainComplex CategoryTheory.Abelian.hasZeroObject 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 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 cochainComplex CategoryTheory.Abelian.hasZeroObject 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.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 cochainComplex CategoryTheory.Abelian.hasZeroObject 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.Ext EquivLike.toFunLike Equiv.instEquivLike Equiv.symm extEquivCohomologyClass CategoryTheory.ShiftedHom.comp DerivedCategory DerivedCategory.instCategory Int.instAddMonoid DerivedCategory.instHasShiftInt DerivedCategory.singleFunctor DerivedCategory.Q AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.ShiftedHom.mk₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category DerivedCategory.singleFunctorIsoCompQ CategoryTheory.inv CategoryTheory.Functor.map π' DerivedCategory.instIsIsoMapCochainComplexIntQ instQuasiIsoIntπ' CategoryTheory.ShiftedHom.map CochainComplex.instHasShiftInt AddEquiv CochainComplex.HomComplex.Cocycle Quiver.Hom CategoryTheory.CategoryStruct.toQuiver 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.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 instIsGECochainComplexOfNatInt HomologicalComplex.instIsSupportedOfIsStrictlySupported instIsStrictlyLECochainComplexOfNatInt CochainComplex.instIsStrictlyGEObjIntSingleFunctor CochainComplex.instIsStrictlyLEObjIntSingleFunctor CategoryTheory.Localization.inverts CategoryTheory.Localization.SmallShiftedHom.equiv_comp CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀Inv CategoryTheory.ShiftedHom.mk₀.congr_simp CategoryTheory.Category.id_comp CategoryTheory.ShiftedHom.comp_mk₀_id
extEquivCohomologyClass_symm_neg 📖	mathematical	CategoryTheory.HasExt	DFunLike.coe Equiv CochainComplex.HomComplex.CohomologyClass CategoryTheory.Abelian.toPreadditive cochainComplex CategoryTheory.Abelian.hasZeroObject 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.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 cochainComplex CategoryTheory.Abelian.hasZeroObject 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.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 cochainComplex CategoryTheory.Abelian.hasZeroObject 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.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 cochainComplex CategoryTheory.Abelian.hasZeroObject 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 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.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne complex 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	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.Ext.ext add_zero DerivedCategory.instIsIsoMapCochainComplexIntQ instQuasiIsoIntπ' zero_add CategoryTheory.Abelian.Ext.comp_hom CategoryTheory.ShiftedHom.comp.congr_simp extEquivCohomologyClass_symm_mk_hom CategoryTheory.Abelian.Ext.mk₀_hom CochainComplex.HomComplex.Cocycle.toSingleMk.congr_simp cochainComplex_d CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.isIso_hom CochainComplex.HomComplex.Cocycle.toSingleMk_postcomp CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp CategoryTheory.ShiftedHom.comp_mk₀ CategoryTheory.ShiftedHom.map_comp CategoryTheory.ShiftedHom.map_mk₀ CategoryTheory.ShiftedHom.comp_assoc CategoryTheory.ShiftedHom.mk₀_comp_mk₀ CategoryTheory.NatTrans.naturality
extMk_eq_zero_iff 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne complex 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 Equiv.apply_eq_iff_eq extEquivCohomologyClass_extMk extEquivCohomologyClass_zero CochainComplex.HomComplex.Cocycle.toSingleMk_mem_coboundaries_iff cochainComplex_d CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc 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.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne complex 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 CochainComplex AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up DerivedCategory.Q cochainComplex AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.ShiftedHom.mk₀ CategoryTheory.Functor.comp CochainComplex.singleFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category DerivedCategory.singleFunctorIsoCompQ CategoryTheory.inv CategoryTheory.Functor.map π' DerivedCategory.instIsIsoMapCochainComplexIntQ instQuasiIsoIntπ' 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.toSingleMk cochainComplexXIso DerivedCategory.instCommShiftCochainComplexIntQ CategoryTheory.Iso.inv zero_add 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 neg_add_cancel CochainComplex.HomComplex.Cocycle.toSingleMk_surjective CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.comp_zero cochainComplex_d CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CochainComplex.HomComplex.Cocycle.toSingleMk.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.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne complex 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.comp_zero CochainComplex.HomComplex.Cocycle.toSingleMk.congr_simp CochainComplex.HomComplex.Cocycle.toSingleMk_zero extEquivCohomologyClass_symm_zero
instIsKProjectiveCochainComplex 📖	mathematical	—	CochainComplex.IsKProjective cochainComplex CategoryTheory.Abelian.hasZeroObject CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Abelian.hasZeroObject CochainComplex.isKProjective_of_projective instIsStrictlyLECochainComplexOfNatInt instProjectiveXIntCochainComplex
mk₀_comp_extMk 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne complex 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 HomologicalComplex.Hom.f Hom.hom	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.Ext.ext zero_add Hom.hom'_f CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id DerivedCategory.instIsIsoMapCochainComplexIntQ instQuasiIsoIntπ' add_zero Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Abelian.Ext.comp_hom CategoryTheory.ShiftedHom.comp.congr_simp CategoryTheory.Abelian.Ext.mk₀_hom extMk_hom CochainComplex.HomComplex.Cocycle.toSingleMk.congr_simp cochainComplex_d CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.isIso_hom CochainComplex.HomComplex.Cocycle.toSingleMk_precomp CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp CategoryTheory.ShiftedHom.mk₀_comp 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_assoc Hom.hom'_comp_π'
neg_extMk 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne complex 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.comp_neg CochainComplex.HomComplex.Cocycle.toSingleMk.congr_simp cochainComplex_d CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.isIso_hom CochainComplex.HomComplex.Cocycle.toSingleMk_neg extEquivCohomologyClass_symm_neg
sub_extMk 📖	mathematical	CategoryTheory.HasExt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne complex 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.comp_sub CochainComplex.HomComplex.Cocycle.toSingleMk.congr_simp cochainComplex_d CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.isIso_hom CochainComplex.HomComplex.Cocycle.toSingleMk_sub extEquivCohomologyClass_symm_sub

---

← Back to Index