RightDerived

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

Statistics

Metric	Count
Definitions rightDerived, rightDerivedToHomotopyCategory, rightDerivedZeroIsoSelf, toRightDerivedZero, isoRightDerivedObj, isoRightDerivedToHomotopyCategoryObj, toRightDerivedZero', rightDerived, rightDerivedToHomotopyCategory	9
Theorems isZero_rightDerived_obj_injective_succ, rightDerivedZeroIsoSelf_hom_inv_id, rightDerivedZeroIsoSelf_hom_inv_id_app, rightDerivedZeroIsoSelf_hom_inv_id_app_assoc, rightDerivedZeroIsoSelf_hom_inv_id_assoc, rightDerivedZeroIsoSelf_inv, rightDerivedZeroIsoSelf_inv_hom_id, rightDerivedZeroIsoSelf_inv_hom_id_app, rightDerivedZeroIsoSelf_inv_hom_id_app_assoc, rightDerivedZeroIsoSelf_inv_hom_id_assoc, rightDerived_map_eq, instIsIsoToRightDerivedZero'Self, isoRightDerivedObj_hom_naturality, isoRightDerivedObj_hom_naturality_assoc, isoRightDerivedObj_inv_naturality, isoRightDerivedObj_inv_naturality_assoc, isoRightDerivedToHomotopyCategoryObj_hom_naturality, isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, isoRightDerivedToHomotopyCategoryObj_inv_naturality, isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, rightDerivedToHomotopyCategory_app_eq, rightDerived_app_eq, toRightDerivedZero'_comp_iCycles, toRightDerivedZero'_comp_iCycles_assoc, toRightDerivedZero'_naturality, toRightDerivedZero'_naturality_assoc, toRightDerivedZero_eq, rightDerivedToHomotopyCategory_comp, rightDerivedToHomotopyCategory_comp_assoc, rightDerivedToHomotopyCategory_id, rightDerived_comp, rightDerived_comp_assoc, rightDerived_id, instIsIsoAppToRightDerivedZero, instIsIsoAppToRightDerivedZeroOfInjective, instIsIsoFunctorToRightDerivedZero, instIsIsoToRightDerivedZero'	37
Total	46

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoAppToRightDerivedZero 📖	mathematical	—	IsIso Functor.obj Functor.rightDerived NatTrans.app Functor.toRightDerivedZero	—	Abelian.hasZeroObject categoryWithHomology_of_abelian IsIso.comp_isIso instIsIsoToRightDerivedZero' CochainComplex.isIso_homologyπ₀ NatIso.inv_app_isIso
instIsIsoAppToRightDerivedZeroOfInjective 📖	mathematical	—	IsIso Functor.obj Functor.rightDerived NatTrans.app Functor.toRightDerivedZero	—	Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd Functor.preservesZeroMorphisms_of_additive CategoryWithHomology.hasHomology categoryWithHomology_of_abelian InjectiveResolution.toRightDerivedZero_eq IsIso.comp_isIso InjectiveResolution.instIsIsoToRightDerivedZero'Self Iso.isIso_hom Iso.isIso_inv
instIsIsoFunctorToRightDerivedZero 📖	mathematical	—	IsIso Functor Functor.category Functor.rightDerived Functor.toRightDerivedZero	—	Abelian.hasZeroObject NatIso.isIso_of_isIso_app instIsIsoAppToRightDerivedZero
instIsIsoToRightDerivedZero' 📖	mathematical	—	IsIso Functor.obj HomologicalComplex.cycles Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex HomologicalComplex.instCategory Functor.mapHomologicalComplex Functor.preservesZeroMorphisms_of_additive InjectiveResolution.cocomplex Abelian.hasZeroObject CategoryWithHomology.hasHomology categoryWithHomology_of_abelian HomologicalComplex.sc InjectiveResolution.toRightDerivedZero'	—	Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd Functor.preservesZeroMorphisms_of_additive CategoryWithHomology.hasHomology categoryWithHomology_of_abelian CochainComplex.isIso_liftCycles_iff ShortComplex.zero ShortComplex.exact_and_mono_f_iff_f_is_kernel balanced_of_strongMonoCategory strongMonoCategory_of_regularMonoCategory regularMonoCategoryOfNormalMonoCategory Abelian.toIsNormalMonoCategory Limits.PreservesLimitsOfShape.preservesLimit Limits.PreservesFiniteLimits.preservesFiniteLimits

CategoryTheory.Functor

Definitions

Name	Category	Theorems
rightDerived 📖	CompOp	23 math math: CategoryTheory.NatTrans.rightDerived_comp_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CategoryTheory.instIsIsoAppToRightDerivedZeroOfInjective, CategoryTheory.NatTrans.rightDerived_comp, rightDerivedZeroIsoSelf_hom_inv_id, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality, rightDerivedZeroIsoSelf_hom_inv_id_app, rightDerivedZeroIsoSelf_hom_inv_id_app_assoc, rightDerivedZeroIsoSelf_inv_hom_id_app_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality, CategoryTheory.instIsIsoAppToRightDerivedZero, rightDerivedZeroIsoSelf_inv_hom_id_app, CategoryTheory.instIsIsoFunctorToRightDerivedZero, rightDerived_map_eq, CategoryTheory.NatTrans.rightDerived_id, rightDerivedZeroIsoSelf_inv, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc, rightDerivedZeroIsoSelf_inv_hom_id_assoc, rightDerivedZeroIsoSelf_hom_inv_id_assoc, isZero_rightDerived_obj_injective_succ, rightDerivedZeroIsoSelf_inv_hom_id, CategoryTheory.InjectiveResolution.rightDerived_app_eq
rightDerivedToHomotopyCategory 📖	CompOp	8 math math: CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq
rightDerivedZeroIsoSelf 📖	CompOp	9 math math: rightDerivedZeroIsoSelf_hom_inv_id, rightDerivedZeroIsoSelf_hom_inv_id_app, rightDerivedZeroIsoSelf_hom_inv_id_app_assoc, rightDerivedZeroIsoSelf_inv_hom_id_app_assoc, rightDerivedZeroIsoSelf_inv_hom_id_app, rightDerivedZeroIsoSelf_inv, rightDerivedZeroIsoSelf_inv_hom_id_assoc, rightDerivedZeroIsoSelf_hom_inv_id_assoc, rightDerivedZeroIsoSelf_inv_hom_id
toRightDerivedZero 📖	CompOp	13 math math: CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CategoryTheory.instIsIsoAppToRightDerivedZeroOfInjective, rightDerivedZeroIsoSelf_hom_inv_id, rightDerivedZeroIsoSelf_hom_inv_id_app, rightDerivedZeroIsoSelf_hom_inv_id_app_assoc, rightDerivedZeroIsoSelf_inv_hom_id_app_assoc, CategoryTheory.instIsIsoAppToRightDerivedZero, rightDerivedZeroIsoSelf_inv_hom_id_app, CategoryTheory.instIsIsoFunctorToRightDerivedZero, rightDerivedZeroIsoSelf_inv, rightDerivedZeroIsoSelf_inv_hom_id_assoc, rightDerivedZeroIsoSelf_hom_inv_id_assoc, rightDerivedZeroIsoSelf_inv_hom_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isZero_rightDerived_obj_injective_succ 📖	mathematical	—	CategoryTheory.Limits.IsZero obj rightDerived	—	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
rightDerivedZeroIsoSelf_hom_inv_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category rightDerived CategoryTheory.Iso.hom rightDerivedZeroIsoSelf toRightDerivedZero CategoryTheory.CategoryStruct.id	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom_inv_id
rightDerivedZeroIsoSelf_hom_inv_id_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj rightDerived CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category rightDerivedZeroIsoSelf toRightDerivedZero CategoryTheory.CategoryStruct.id	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom_inv_id_app
rightDerivedZeroIsoSelf_hom_inv_id_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj rightDerived CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category rightDerivedZeroIsoSelf toRightDerivedZero	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' rightDerivedZeroIsoSelf_hom_inv_id_app
rightDerivedZeroIsoSelf_hom_inv_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category rightDerived CategoryTheory.Iso.hom rightDerivedZeroIsoSelf toRightDerivedZero	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' rightDerivedZeroIsoSelf_hom_inv_id
rightDerivedZeroIsoSelf_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor category rightDerived rightDerivedZeroIsoSelf toRightDerivedZero	—	CategoryTheory.Abelian.hasZeroObject
rightDerivedZeroIsoSelf_inv_hom_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category rightDerived toRightDerivedZero CategoryTheory.Iso.hom rightDerivedZeroIsoSelf CategoryTheory.CategoryStruct.id	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.inv_hom_id
rightDerivedZeroIsoSelf_inv_hom_id_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj rightDerived CategoryTheory.NatTrans.app toRightDerivedZero CategoryTheory.Iso.hom CategoryTheory.Functor category rightDerivedZeroIsoSelf CategoryTheory.CategoryStruct.id	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.inv_hom_id_app
rightDerivedZeroIsoSelf_inv_hom_id_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj rightDerived CategoryTheory.NatTrans.app toRightDerivedZero CategoryTheory.Iso.hom CategoryTheory.Functor category rightDerivedZeroIsoSelf	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' rightDerivedZeroIsoSelf_inv_hom_id_app
rightDerivedZeroIsoSelf_inv_hom_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category rightDerived toRightDerivedZero CategoryTheory.Iso.hom rightDerivedZeroIsoSelf	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' rightDerivedZeroIsoSelf_inv_hom_id
rightDerived_map_eq 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd obj CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject CategoryTheory.InjectiveResolution.cocomplex CategoryTheory.InjectiveResolution.ι map	rightDerived HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian mapHomologicalComplex preservesZeroMorphisms_of_additive CategoryTheory.Iso.hom CategoryTheory.InjectiveResolution.isoRightDerivedObj 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.InjectiveResolution.isoRightDerivedObj_hom_naturality HomologicalComplex.comp_f CochainComplex.single₀_map_f_zero CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id

CategoryTheory.InjectiveResolution

Definitions

Name	Category	Theorems
isoRightDerivedObj 📖	CompOp	7 math math: toRightDerivedZero_eq, isoRightDerivedObj_hom_naturality, isoRightDerivedObj_hom_naturality_assoc, isoRightDerivedObj_inv_naturality, CategoryTheory.Functor.rightDerived_map_eq, isoRightDerivedObj_inv_naturality_assoc, rightDerived_app_eq
isoRightDerivedToHomotopyCategoryObj 📖	CompOp	5 math math: isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, isoRightDerivedToHomotopyCategoryObj_inv_naturality, isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, isoRightDerivedToHomotopyCategoryObj_hom_naturality, rightDerivedToHomotopyCategory_app_eq
toRightDerivedZero' 📖	CompOp	7 math math: toRightDerivedZero'_naturality_assoc, toRightDerivedZero'_comp_iCycles, CategoryTheory.instIsIsoToRightDerivedZero', toRightDerivedZero_eq, instIsIsoToRightDerivedZero'Self, toRightDerivedZero'_naturality, toRightDerivedZero'_comp_iCycles_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoToRightDerivedZero'Self 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj HomologicalComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive cocomplex CategoryTheory.Abelian.hasZeroObject self CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc toRightDerivedZero'	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CochainComplex.isIso_liftCycles_iff CategoryTheory.ShortComplex.Splitting.exact CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Functor.map_isZero CategoryTheory.Limits.isZero_zero CategoryTheory.Functor.map_zero CategoryTheory.Limits.comp_zero add_zero CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.instIsSplitMonoMap CategoryTheory.IsSplitMono.of_iso CategoryTheory.IsIso.id
isoRightDerivedObj_hom_naturality 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	CategoryTheory.Functor.rightDerived HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map CategoryTheory.Iso.hom isoRightDerivedObj 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 isoRightDerivedToHomotopyCategoryObj_hom_naturality CategoryTheory.Functor.map_comp CategoryTheory.NatTrans.naturality
isoRightDerivedObj_hom_naturality_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	CategoryTheory.Functor.rightDerived CategoryTheory.Functor.map HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Iso.hom isoRightDerivedObj	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoRightDerivedObj_hom_naturality
isoRightDerivedObj_inv_naturality 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.rightDerived CategoryTheory.Iso.inv isoRightDerivedObj 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 isoRightDerivedObj_hom_naturality CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
isoRightDerivedObj_inv_naturality_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.rightDerived CategoryTheory.Iso.inv isoRightDerivedObj 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' isoRightDerivedObj_inv_naturality
isoRightDerivedToHomotopyCategoryObj_hom_naturality 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.rightDerivedToHomotopyCategory HomologicalComplex CategoryTheory.Functor.comp CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomotopyCategory.quotient CategoryTheory.Functor.map CategoryTheory.Iso.hom isoRightDerivedToHomotopyCategoryObj	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map_comp_assoc iso_hom_naturality CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality
isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.rightDerivedToHomotopyCategory CategoryTheory.Functor.map HomologicalComplex HomotopyCategory.quotient CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Iso.hom isoRightDerivedToHomotopyCategoryObj	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoRightDerivedToHomotopyCategoryObj_hom_naturality
isoRightDerivedToHomotopyCategoryObj_inv_naturality 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomotopyCategory instCategoryHomotopyCategory HomologicalComplex CategoryTheory.Functor.comp CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomotopyCategory.quotient CategoryTheory.Functor.rightDerivedToHomotopyCategory CategoryTheory.Iso.inv isoRightDerivedToHomotopyCategoryObj CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomotopyCategory instCategoryHomotopyCategory HomologicalComplex HomotopyCategory.quotient CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.rightDerivedToHomotopyCategory CategoryTheory.Iso.inv isoRightDerivedToHomotopyCategoryObj CategoryTheory.Functor.map	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoRightDerivedToHomotopyCategoryObj_inv_naturality
rightDerivedToHomotopyCategory_app_eq 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne instCategoryHomotopyCategory CategoryTheory.Functor.rightDerivedToHomotopyCategory CategoryTheory.NatTrans.rightDerivedToHomotopyCategory 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 cocomplex CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom isoRightDerivedToHomotopyCategoryObj 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
rightDerived_app_eq 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.rightDerived CategoryTheory.NatTrans.rightDerived CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up 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 cocomplex CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom isoRightDerivedObj CategoryTheory.Functor.map CategoryTheory.NatTrans.mapHomologicalComplex CategoryTheory.Iso.inv	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_of_additive rightDerivedToHomotopyCategory_app_eq CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Iso.hom_inv_id_app_assoc
toRightDerivedZero'_comp_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomologicalComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive cocomplex CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc HomologicalComplex.X toRightDerivedZero' HomologicalComplex.iCycles CategoryTheory.Functor.map CochainComplex CochainComplex.single₀ HomologicalComplex.Hom.f ι	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.liftCycles_i
toRightDerivedZero'_comp_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomologicalComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive cocomplex CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc toRightDerivedZero' HomologicalComplex.X HomologicalComplex.iCycles CategoryTheory.Functor.map CochainComplex CochainComplex.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' toRightDerivedZero'_comp_iCycles
toRightDerivedZero'_naturality 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	HomologicalComplex.cycles HomologicalComplex CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.Functor.map toRightDerivedZero' HomologicalComplex.cyclesMap	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_mono HomologicalComplex.instMonoICycles CategoryTheory.Category.assoc toRightDerivedZero'_comp_iCycles CategoryTheory.Functor.map_comp HomologicalComplex.cyclesMap_i toRightDerivedZero'_comp_iCycles_assoc
toRightDerivedZero'_naturality_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.single₀ CategoryTheory.Abelian.hasZeroObject cocomplex HomologicalComplex.Hom.f ι	CategoryTheory.Functor.map HomologicalComplex.cycles HomologicalComplex CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc toRightDerivedZero' HomologicalComplex.cyclesMap	—	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' toRightDerivedZero'_naturality
toRightDerivedZero_eq 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.rightDerived CategoryTheory.Functor.toRightDerivedZero CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomologicalComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive cocomplex CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc toRightDerivedZero' HomologicalComplex.homology CategoryTheory.Iso.hom CochainComplex.isoHomologyπ₀ CategoryTheory.Iso.inv HomologicalComplex.homologyFunctor isoRightDerivedObj	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.HasInjectiveResolutions.out toRightDerivedZero'_naturality desc_commutes_zero CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.instIsSplitMonoMap CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.Iso.inv_hom_id CategoryTheory.Functor.map_id Mathlib.Tactic.Reassoc.eq_whisker' HomologicalComplex.homologyπ_naturality_assoc CategoryTheory.NatTrans.naturality

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
rightDerived 📖	CompOp	4 math math: rightDerived_comp_assoc, rightDerived_comp, rightDerived_id, CategoryTheory.InjectiveResolution.rightDerived_app_eq
rightDerivedToHomotopyCategory 📖	CompOp	4 math math: rightDerivedToHomotopyCategory_id, rightDerivedToHomotopyCategory_comp_assoc, rightDerivedToHomotopyCategory_comp, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rightDerivedToHomotopyCategory_comp 📖	mathematical	—	rightDerivedToHomotopyCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne instCategoryHomotopyCategory CategoryTheory.Functor.rightDerivedToHomotopyCategory	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd
rightDerivedToHomotopyCategory_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne instCategoryHomotopyCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.rightDerivedToHomotopyCategory rightDerivedToHomotopyCategory	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightDerivedToHomotopyCategory_comp
rightDerivedToHomotopyCategory_id 📖	mathematical	—	rightDerivedToHomotopyCategory CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne instCategoryHomotopyCategory CategoryTheory.Functor.rightDerivedToHomotopyCategory	—	CategoryTheory.Abelian.hasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd
rightDerived_comp 📖	mathematical	—	rightDerived CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.rightDerived	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.whiskerRight_comp
rightDerived_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.rightDerived rightDerived	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightDerived_comp
rightDerived_id 📖	mathematical	—	rightDerived CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.rightDerived	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.whiskerRight_id'

---

← Back to Index