LeftDerived

📁 Source: Mathlib/CategoryTheory/Abelian/LeftDerived.lean

Statistics

Metric	Count
Definitions fromLeftDerivedZero, leftDerived, leftDerivedToHomotopyCategory, leftDerivedZeroIsoSelf, leftDerived, leftDerivedToHomotopyCategory, fromLeftDerivedZero', isoLeftDerivedObj, isoLeftDerivedToHomotopyCategoryObj	9
Theorems isZero_leftDerived_obj_projective_succ, leftDerivedZeroIsoSelf_hom, leftDerivedZeroIsoSelf_hom_inv_id, leftDerivedZeroIsoSelf_hom_inv_id_app, leftDerivedZeroIsoSelf_hom_inv_id_app_assoc, leftDerivedZeroIsoSelf_hom_inv_id_assoc, leftDerivedZeroIsoSelf_inv_hom_id, leftDerivedZeroIsoSelf_inv_hom_id_app, leftDerivedZeroIsoSelf_inv_hom_id_app_assoc, leftDerivedZeroIsoSelf_inv_hom_id_assoc, leftDerived_map_eq, leftDerivedToHomotopyCategory_comp, leftDerivedToHomotopyCategory_comp_assoc, leftDerivedToHomotopyCategory_id, leftDerived_comp, leftDerived_comp_assoc, leftDerived_id, fromLeftDerivedZero'_naturality, fromLeftDerivedZero'_naturality_assoc, fromLeftDerivedZero_eq, instIsIsoFromLeftDerivedZero'Self, isoLeftDerivedObj_hom_naturality, isoLeftDerivedObj_hom_naturality_assoc, isoLeftDerivedObj_inv_naturality, isoLeftDerivedObj_inv_naturality_assoc, isoLeftDerivedToHomotopyCategoryObj_hom_naturality, isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, isoLeftDerivedToHomotopyCategoryObj_inv_naturality, isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, leftDerivedToHomotopyCategory_app_eq, leftDerived_app_eq, pOpcycles_comp_fromLeftDerivedZero', pOpcycles_comp_fromLeftDerivedZero'_assoc, instIsIsoAppFromLeftDerivedZero, instIsIsoAppFromLeftDerivedZeroOfProjective, instIsIsoFromLeftDerivedZero', instIsIsoFunctorFromLeftDerivedZero	37
Total	46

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoAppFromLeftDerivedZero 📖	mathematical	—	IsIso Functor.obj Functor.leftDerived NatTrans.app Functor.fromLeftDerivedZero	—	Abelian.hasZeroObject categoryWithHomology_of_abelian IsIso.comp_isIso NatIso.hom_app_isIso ChainComplex.isIso_homologyι₀ instIsIsoFromLeftDerivedZero'
instIsIsoAppFromLeftDerivedZeroOfProjective 📖	mathematical	—	IsIso Functor.obj Functor.leftDerived NatTrans.app Functor.fromLeftDerivedZero	—	Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd categoryWithHomology_of_abelian Functor.preservesZeroMorphisms_of_additive ProjectiveResolution.fromLeftDerivedZero_eq IsIso.comp_isIso Iso.isIso_hom ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self
instIsIsoFromLeftDerivedZero' 📖	mathematical	—	IsIso HomologicalComplex.opcycles Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne Functor.obj HomologicalComplex HomologicalComplex.instCategory Functor.mapHomologicalComplex Functor.preservesZeroMorphisms_of_additive ProjectiveResolution.complex Abelian.hasZeroObject CategoryWithHomology.hasHomology categoryWithHomology_of_abelian HomologicalComplex.sc ProjectiveResolution.fromLeftDerivedZero'	—	Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd Functor.preservesZeroMorphisms_of_additive CategoryWithHomology.hasHomology categoryWithHomology_of_abelian ChainComplex.isIso_descOpcycles_iff ShortComplex.zero ShortComplex.exact_and_epi_g_iff_g_is_cokernel balanced_of_strongMonoCategory strongMonoCategory_of_regularMonoCategory regularMonoCategoryOfNormalMonoCategory Abelian.toIsNormalMonoCategory Limits.PreservesColimitsOfShape.preservesColimit Limits.PreservesFiniteColimits.preservesFiniteColimits
instIsIsoFunctorFromLeftDerivedZero 📖	mathematical	—	IsIso Functor Functor.category Functor.leftDerived Functor.fromLeftDerivedZero	—	Abelian.hasZeroObject NatIso.isIso_of_isIso_app instIsIsoAppFromLeftDerivedZero

CategoryTheory.Functor

Definitions

Name	Category	Theorems
fromLeftDerivedZero 📖	CompOp	13 math math: leftDerivedZeroIsoSelf_inv_hom_id, leftDerivedZeroIsoSelf_hom_inv_id_app, CategoryTheory.instIsIsoAppFromLeftDerivedZeroOfProjective, leftDerivedZeroIsoSelf_inv_hom_id_app, leftDerivedZeroIsoSelf_inv_hom_id_assoc, leftDerivedZeroIsoSelf_inv_hom_id_app_assoc, CategoryTheory.instIsIsoAppFromLeftDerivedZero, leftDerivedZeroIsoSelf_hom_inv_id, CategoryTheory.instIsIsoFunctorFromLeftDerivedZero, leftDerivedZeroIsoSelf_hom, leftDerivedZeroIsoSelf_hom_inv_id_app_assoc, leftDerivedZeroIsoSelf_hom_inv_id_assoc, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq
leftDerived 📖	CompOp	28 math math: CategoryTheory.Tor'_obj_obj, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality_assoc, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality_assoc, leftDerivedZeroIsoSelf_inv_hom_id, leftDerivedZeroIsoSelf_hom_inv_id_app, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality, CategoryTheory.instIsIsoAppFromLeftDerivedZeroOfProjective, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, CategoryTheory.Tor_obj, isZero_leftDerived_obj_projective_succ, CategoryTheory.Tor'_obj_map, leftDerivedZeroIsoSelf_inv_hom_id_app, CategoryTheory.NatTrans.leftDerived_comp_assoc, leftDerived_map_eq, leftDerivedZeroIsoSelf_inv_hom_id_assoc, leftDerivedZeroIsoSelf_inv_hom_id_app_assoc, CategoryTheory.instIsIsoAppFromLeftDerivedZero, leftDerivedZeroIsoSelf_hom_inv_id, CategoryTheory.instIsIsoFunctorFromLeftDerivedZero, leftDerivedZeroIsoSelf_hom, leftDerivedZeroIsoSelf_hom_inv_id_app_assoc, leftDerivedZeroIsoSelf_hom_inv_id_assoc, CategoryTheory.NatTrans.leftDerived_comp, CategoryTheory.NatTrans.leftDerived_id, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality, CategoryTheory.Tor'_map_app, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, Rep.Tor_obj
leftDerivedToHomotopyCategory 📖	CompOp	8 math math: CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id
leftDerivedZeroIsoSelf 📖	CompOp	9 math math: leftDerivedZeroIsoSelf_inv_hom_id, leftDerivedZeroIsoSelf_hom_inv_id_app, leftDerivedZeroIsoSelf_inv_hom_id_app, leftDerivedZeroIsoSelf_inv_hom_id_assoc, leftDerivedZeroIsoSelf_inv_hom_id_app_assoc, leftDerivedZeroIsoSelf_hom_inv_id, leftDerivedZeroIsoSelf_hom, leftDerivedZeroIsoSelf_hom_inv_id_app_assoc, leftDerivedZeroIsoSelf_hom_inv_id_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isZero_leftDerived_obj_projective_succ 📖	mathematical	—	CategoryTheory.Limits.IsZero obj leftDerived	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.IsZero.of_iso AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian preservesZeroMorphisms_of_additive HomologicalComplex.exactAt_iff_isZero_homology CategoryTheory.ShortComplex.exact_of_isZero_X₂ map_isZero CategoryTheory.Limits.isZero_zero
leftDerivedZeroIsoSelf_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor category leftDerived leftDerivedZeroIsoSelf fromLeftDerivedZero	—	CategoryTheory.Abelian.hasZeroObject
leftDerivedZeroIsoSelf_hom_inv_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category leftDerived fromLeftDerivedZero CategoryTheory.Iso.inv leftDerivedZeroIsoSelf CategoryTheory.CategoryStruct.id	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom_inv_id
leftDerivedZeroIsoSelf_hom_inv_id_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj leftDerived CategoryTheory.NatTrans.app fromLeftDerivedZero CategoryTheory.Iso.inv CategoryTheory.Functor category leftDerivedZeroIsoSelf CategoryTheory.CategoryStruct.id	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom_inv_id_app
leftDerivedZeroIsoSelf_hom_inv_id_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj leftDerived CategoryTheory.NatTrans.app fromLeftDerivedZero CategoryTheory.Iso.inv CategoryTheory.Functor category leftDerivedZeroIsoSelf	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' leftDerivedZeroIsoSelf_hom_inv_id_app
leftDerivedZeroIsoSelf_hom_inv_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category leftDerived fromLeftDerivedZero CategoryTheory.Iso.inv leftDerivedZeroIsoSelf	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' leftDerivedZeroIsoSelf_hom_inv_id
leftDerivedZeroIsoSelf_inv_hom_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category leftDerived CategoryTheory.Iso.inv leftDerivedZeroIsoSelf fromLeftDerivedZero CategoryTheory.CategoryStruct.id	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.inv_hom_id
leftDerivedZeroIsoSelf_inv_hom_id_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj leftDerived CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category leftDerivedZeroIsoSelf fromLeftDerivedZero CategoryTheory.CategoryStruct.id	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.inv_hom_id_app
leftDerivedZeroIsoSelf_inv_hom_id_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj leftDerived CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category leftDerivedZeroIsoSelf fromLeftDerivedZero	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' leftDerivedZeroIsoSelf_inv_hom_id_app
leftDerivedZeroIsoSelf_inv_hom_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category leftDerived CategoryTheory.Iso.inv leftDerivedZeroIsoSelf fromLeftDerivedZero	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' leftDerivedZeroIsoSelf_inv_hom_id
leftDerived_map_eq 📖	mathematical	CategoryTheory.CategoryStruct.comp ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ProjectiveResolution.complex CategoryTheory.Abelian.hasZeroObject obj ChainComplex.single₀ CategoryTheory.ProjectiveResolution.π map	leftDerived HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian mapHomologicalComplex preservesZeroMorphisms_of_additive CategoryTheory.Iso.hom CategoryTheory.ProjectiveResolution.isoLeftDerivedObj comp CategoryTheory.Iso.inv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian preservesZeroMorphisms_of_additive CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality HomologicalComplex.comp_f ChainComplex.single₀_map_f_zero CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
leftDerived 📖	CompOp	8 math math: Rep.Tor_map, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, CategoryTheory.Tor'_obj_map, leftDerived_comp_assoc, leftDerived_comp, leftDerived_id, CategoryTheory.Tor_map, CategoryTheory.Tor'_map_app
leftDerivedToHomotopyCategory 📖	CompOp	4 math math: leftDerivedToHomotopyCategory_comp_assoc, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, leftDerivedToHomotopyCategory_comp, leftDerivedToHomotopyCategory_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftDerivedToHomotopyCategory_comp 📖	mathematical	—	leftDerivedToHomotopyCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne instCategoryHomotopyCategory CategoryTheory.Functor.leftDerivedToHomotopyCategory	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd
leftDerivedToHomotopyCategory_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne instCategoryHomotopyCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.leftDerivedToHomotopyCategory leftDerivedToHomotopyCategory	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftDerivedToHomotopyCategory_comp
leftDerivedToHomotopyCategory_id 📖	mathematical	—	leftDerivedToHomotopyCategory CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne instCategoryHomotopyCategory CategoryTheory.Functor.leftDerivedToHomotopyCategory	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd
leftDerived_comp 📖	mathematical	—	leftDerived CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.leftDerived	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.whiskerRight_comp
leftDerived_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.leftDerived leftDerived	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftDerived_comp
leftDerived_id 📖	mathematical	—	leftDerived CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.leftDerived	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.whiskerRight_id'

CategoryTheory.ProjectiveResolution

Definitions

Name	Category	Theorems
fromLeftDerivedZero' 📖	CompOp	7 math math: pOpcycles_comp_fromLeftDerivedZero'_assoc, instIsIsoFromLeftDerivedZero'Self, pOpcycles_comp_fromLeftDerivedZero', fromLeftDerivedZero'_naturality, fromLeftDerivedZero'_naturality_assoc, fromLeftDerivedZero_eq, CategoryTheory.instIsIsoFromLeftDerivedZero'
isoLeftDerivedObj 📖	CompOp	7 math math: isoLeftDerivedObj_hom_naturality_assoc, isoLeftDerivedObj_inv_naturality_assoc, isoLeftDerivedObj_hom_naturality, leftDerived_app_eq, CategoryTheory.Functor.leftDerived_map_eq, isoLeftDerivedObj_inv_naturality, fromLeftDerivedZero_eq
isoLeftDerivedToHomotopyCategoryObj 📖	CompOp	5 math math: isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, leftDerivedToHomotopyCategory_app_eq, isoLeftDerivedToHomotopyCategoryObj_inv_naturality, isoLeftDerivedToHomotopyCategoryObj_hom_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromLeftDerivedZero'_naturality 📖	mathematical	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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ HomologicalComplex.Hom.f π	HomologicalComplex.opcycles HomologicalComplex CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc HomologicalComplex.opcyclesMap CategoryTheory.Functor.map fromLeftDerivedZero'	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_epi HomologicalComplex.instEpiPOpcycles HomologicalComplex.p_opcyclesMap_assoc pOpcycles_comp_fromLeftDerivedZero' CategoryTheory.Functor.map_comp pOpcycles_comp_fromLeftDerivedZero'_assoc
fromLeftDerivedZero'_naturality_assoc 📖	mathematical	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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ HomologicalComplex.Hom.f π	HomologicalComplex.opcycles HomologicalComplex CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc HomologicalComplex.opcyclesMap CategoryTheory.Functor.map fromLeftDerivedZero'	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromLeftDerivedZero'_naturality
fromLeftDerivedZero_eq 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.leftDerived CategoryTheory.Functor.fromLeftDerivedZero CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.instCategory HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive complex CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom isoLeftDerivedObj HomologicalComplex.opcycles HomologicalComplex.homology ChainComplex.isoHomologyι₀ fromLeftDerivedZero'	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.HasProjectiveResolutions.out fromLeftDerivedZero'_naturality lift_commutes_zero CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Functor.map_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Functor.map_comp_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Functor.map_id HomologicalComplex.homologyι_naturality_assoc CategoryTheory.NatTrans.naturality_assoc
instIsIsoFromLeftDerivedZero'Self 📖	mathematical	—	CategoryTheory.IsIso HomologicalComplex.opcycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive complex CategoryTheory.Abelian.hasZeroObject self CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc fromLeftDerivedZero'	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ChainComplex.isIso_descOpcycles_iff CategoryTheory.ShortComplex.Splitting.exact CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Functor.map_isZero CategoryTheory.Limits.isZero_zero CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Functor.map_zero CategoryTheory.Limits.comp_zero zero_add CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Functor.map_isIso CategoryTheory.IsIso.id
isoLeftDerivedObj_hom_naturality 📖	mathematical	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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ HomologicalComplex.Hom.f π	CategoryTheory.Functor.leftDerived HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map CategoryTheory.Iso.hom isoLeftDerivedObj CategoryTheory.Functor.comp	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp_assoc isoLeftDerivedToHomotopyCategoryObj_hom_naturality CategoryTheory.Functor.map_comp CategoryTheory.NatTrans.naturality
isoLeftDerivedObj_hom_naturality_assoc 📖	mathematical	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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ HomologicalComplex.Hom.f π	CategoryTheory.Functor.leftDerived CategoryTheory.Functor.map HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Iso.hom isoLeftDerivedObj	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoLeftDerivedObj_hom_naturality
isoLeftDerivedObj_inv_naturality 📖	mathematical	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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ HomologicalComplex.Hom.f π	HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.leftDerived CategoryTheory.Iso.inv isoLeftDerivedObj CategoryTheory.Functor.map CategoryTheory.Functor.comp	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc isoLeftDerivedObj_hom_naturality CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
isoLeftDerivedObj_inv_naturality_assoc 📖	mathematical	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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ HomologicalComplex.Hom.f π	HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.leftDerived CategoryTheory.Iso.inv isoLeftDerivedObj CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoLeftDerivedObj_inv_naturality
isoLeftDerivedToHomotopyCategoryObj_hom_naturality 📖	mathematical	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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ HomologicalComplex.Hom.f π	HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.leftDerivedToHomotopyCategory HomologicalComplex CategoryTheory.Functor.comp CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomotopyCategory.quotient CategoryTheory.Functor.map CategoryTheory.Iso.hom isoLeftDerivedToHomotopyCategoryObj	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc 📖	mathematical	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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ HomologicalComplex.Hom.f π	HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.leftDerivedToHomotopyCategory CategoryTheory.Functor.map HomologicalComplex HomotopyCategory.quotient CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Iso.hom isoLeftDerivedToHomotopyCategoryObj	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoLeftDerivedToHomotopyCategoryObj_hom_naturality
isoLeftDerivedToHomotopyCategoryObj_inv_naturality 📖	mathematical	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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ HomologicalComplex.Hom.f π	HomotopyCategory instCategoryHomotopyCategory HomologicalComplex CategoryTheory.Functor.comp CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomotopyCategory.quotient CategoryTheory.Functor.leftDerivedToHomotopyCategory CategoryTheory.Iso.inv isoLeftDerivedToHomotopyCategoryObj CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp iso_inv_naturality CategoryTheory.NatTrans.naturality_assoc
isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc 📖	mathematical	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 CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory ChainComplex.single₀ HomologicalComplex.Hom.f π	HomotopyCategory instCategoryHomotopyCategory HomologicalComplex HomotopyCategory.quotient CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.leftDerivedToHomotopyCategory CategoryTheory.Iso.inv isoLeftDerivedToHomotopyCategoryObj CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoLeftDerivedToHomotopyCategoryObj_inv_naturality
leftDerivedToHomotopyCategory_app_eq 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne instCategoryHomotopyCategory CategoryTheory.Functor.leftDerivedToHomotopyCategory CategoryTheory.NatTrans.leftDerivedToHomotopyCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomotopyCategory.quotient complex CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom isoLeftDerivedToHomotopyCategoryObj AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.map CategoryTheory.NatTrans.mapHomologicalComplex CategoryTheory.Iso.inv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_surjective HomotopyCategory.instFullHomologicalComplexQuotient CategoryTheory.NatTrans.mapHomologicalComplex_naturality
leftDerived_app_eq 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.leftDerived CategoryTheory.NatTrans.leftDerived CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.instCategory HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive complex CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom isoLeftDerivedObj CategoryTheory.Functor.map CategoryTheory.NatTrans.mapHomologicalComplex CategoryTheory.Iso.inv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_of_additive leftDerivedToHomotopyCategory_app_eq CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Iso.hom_inv_id_app_assoc
pOpcycles_comp_fromLeftDerivedZero' 📖	mathematical	—	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 CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive complex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.opcycles CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc HomologicalComplex.pOpcycles fromLeftDerivedZero' CategoryTheory.Functor.map ChainComplex ChainComplex.single₀ HomologicalComplex.Hom.f π	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.p_descOpcycles
pOpcycles_comp_fromLeftDerivedZero'_assoc 📖	mathematical	—	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 CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive complex CategoryTheory.Abelian.hasZeroObject HomologicalComplex.opcycles CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc HomologicalComplex.pOpcycles fromLeftDerivedZero' CategoryTheory.Functor.map ChainComplex ChainComplex.single₀ HomologicalComplex.Hom.f π	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_comp_fromLeftDerivedZero'

---

← Back to Index