SingleFunctors

📁 Source: Mathlib/CategoryTheory/Shift/SingleFunctors.lean

Statistics

Metric	Count
Definitions SingleFunctors, comp, hom, id, evaluation, functor, instCategory, isoMk, postcomp, postcompFunctor, postcompIsoOfIso, postcompPostcompIso, shiftIso	13
Theorems comm, comm_assoc, comp_hom, ext, ext_iff, id_hom, comp_hom, comp_hom_assoc, evaluation_map, evaluation_obj, hom_ext, hom_ext_iff, hom_inv_id_hom, hom_inv_id_hom_app, hom_inv_id_hom_app_assoc, hom_inv_id_hom_assoc, id_hom, instIsIsoFunctorHom, inv_hom_id_hom, inv_hom_id_hom_app, inv_hom_id_hom_app_assoc, inv_hom_id_hom_assoc, isoMk_hom_hom, isoMk_inv_hom, postcompFunctor_map_hom, postcompFunctor_obj, postcompIsoOfIso_hom_hom_app, postcompIsoOfIso_inv_hom_app, postcompPostcompIso_hom_hom_app, postcompPostcompIso_inv_hom_app, postcomp_functor, postcomp_shiftIso_hom_app, postcomp_shiftIso_inv_app, shiftIso_add, shiftIso_add', shiftIso_add'_hom_app, shiftIso_add'_inv_app, shiftIso_add_hom_app, shiftIso_add_inv_app, shiftIso_zero, shiftIso_zero_hom_app, shiftIso_zero_inv_app	42
Total	55

CategoryTheory

Definitions

Name	Category	Theorems
SingleFunctors 📖	CompData	29 math math: SingleFunctors.postcompPostcompIso_hom_hom_app, SingleFunctors.id_hom, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, SingleFunctors.comp_hom_assoc, ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, SingleFunctors.isoMk_inv_hom, ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, SingleFunctors.postcompIsoOfIso_hom_hom_app, SingleFunctors.inv_hom_id_hom_assoc, SingleFunctors.hom_inv_id_hom, SingleFunctors.hom_inv_id_hom_app_assoc, ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, SingleFunctors.postcompFunctor_obj, SingleFunctors.postcompPostcompIso_inv_hom_app, SingleFunctors.isoMk_hom_hom, SingleFunctors.inv_hom_id_hom_app_assoc, SingleFunctors.evaluation_obj, SingleFunctors.hom_inv_id_hom_assoc, ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, SingleFunctors.inv_hom_id_hom_app, SingleFunctors.evaluation_map, SingleFunctors.comp_hom, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, SingleFunctors.postcompFunctor_map_hom, SingleFunctors.hom_inv_id_hom_app, SingleFunctors.inv_hom_id_hom, SingleFunctors.postcompIsoOfIso_inv_hom_app

CategoryTheory.SingleFunctors

Definitions

Name	Category	Theorems
evaluation 📖	CompOp	2 math math: evaluation_obj, evaluation_map
functor 📖	CompOp	45 math math: shiftIso_add, postcompPostcompIso_hom_hom_app, Hom.comm, id_hom, shiftIso_add', Hom.comp_hom, CochainComplex.instLinearIntFunctorSingleFunctors, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, postcomp_functor, Hom.comm_assoc, comp_hom_assoc, Hom.id_hom, CochainComplex.instAdditiveIntFunctorSingleFunctors, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, postcompIsoOfIso_hom_hom_app, shiftIso_add_inv_app, inv_hom_id_hom_assoc, hom_inv_id_hom, hom_inv_id_hom_app_assoc, postcomp_shiftIso_inv_app, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, shiftIso_zero, postcompPostcompIso_inv_hom_app, inv_hom_id_hom_app_assoc, evaluation_obj, DerivedCategory.Qh_obj_singleFunctors_obj, hom_inv_id_hom_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, inv_hom_id_hom_app, comp_hom, instIsIsoFunctorHom, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, shiftIso_add_hom_app, postcompFunctor_map_hom, shiftIso_zero_hom_app, shiftIso_add'_inv_app, hom_inv_id_hom_app, inv_hom_id_hom, postcompIsoOfIso_inv_hom_app, shiftIso_add'_hom_app, postcomp_shiftIso_hom_app, shiftIso_zero_inv_app
instCategory 📖	CompOp	29 math math: postcompPostcompIso_hom_hom_app, id_hom, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, comp_hom_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, isoMk_inv_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, postcompIsoOfIso_hom_hom_app, inv_hom_id_hom_assoc, hom_inv_id_hom, hom_inv_id_hom_app_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, postcompFunctor_obj, postcompPostcompIso_inv_hom_app, isoMk_hom_hom, inv_hom_id_hom_app_assoc, evaluation_obj, hom_inv_id_hom_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, inv_hom_id_hom_app, evaluation_map, comp_hom, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, postcompFunctor_map_hom, hom_inv_id_hom_app, inv_hom_id_hom, postcompIsoOfIso_inv_hom_app
isoMk 📖	CompOp	2 math math: isoMk_inv_hom, isoMk_hom_hom
postcomp 📖	CompOp	17 math math: postcompPostcompIso_hom_hom_app, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, postcomp_functor, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, postcompIsoOfIso_hom_hom_app, postcomp_shiftIso_inv_app, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, postcompFunctor_obj, postcompPostcompIso_inv_hom_app, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, postcompFunctor_map_hom, postcompIsoOfIso_inv_hom_app, postcomp_shiftIso_hom_app
postcompFunctor 📖	CompOp	2 math math: postcompFunctor_obj, postcompFunctor_map_hom
postcompIsoOfIso 📖	CompOp	2 math math: postcompIsoOfIso_hom_hom_app, postcompIsoOfIso_inv_hom_app
postcompPostcompIso 📖	CompOp	2 math math: postcompPostcompIso_hom_hom_app, postcompPostcompIso_inv_hom_app
shiftIso 📖	CompOp	13 math math: shiftIso_add, Hom.comm, shiftIso_add', Hom.comm_assoc, shiftIso_add_inv_app, postcomp_shiftIso_inv_app, shiftIso_zero, shiftIso_add_hom_app, shiftIso_zero_hom_app, shiftIso_add'_inv_app, shiftIso_add'_hom_app, postcomp_shiftIso_hom_app, shiftIso_zero_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.SingleFunctors CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.Functor.category functor	—	—
comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor Hom.hom CategoryTheory.SingleFunctors instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom
evaluation_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.SingleFunctors instCategory CategoryTheory.Functor CategoryTheory.Functor.category evaluation Hom.hom	—	—
evaluation_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.SingleFunctors instCategory CategoryTheory.Functor CategoryTheory.Functor.category evaluation functor	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_inv_id_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor Hom.hom CategoryTheory.Iso.hom CategoryTheory.SingleFunctors instCategory CategoryTheory.Iso.inv CategoryTheory.CategoryStruct.id	—	comp_hom CategoryTheory.Iso.hom_inv_id id_hom
hom_inv_id_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.NatTrans.app Hom.hom CategoryTheory.Iso.hom CategoryTheory.SingleFunctors instCategory CategoryTheory.Iso.inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.comp_app hom_inv_id_hom CategoryTheory.NatTrans.id_app
hom_inv_id_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.NatTrans.app Hom.hom CategoryTheory.Iso.hom CategoryTheory.SingleFunctors instCategory CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_hom_app
hom_inv_id_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor Hom.hom CategoryTheory.Iso.hom CategoryTheory.SingleFunctors instCategory CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_hom
id_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.SingleFunctors CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.Functor.category functor	—	—
instIsIsoFunctorHom 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category functor Hom.hom	—	CategoryTheory.Functor.map_isIso
inv_hom_id_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor Hom.hom CategoryTheory.Iso.inv CategoryTheory.SingleFunctors instCategory CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.id	—	comp_hom CategoryTheory.Iso.inv_hom_id id_hom
inv_hom_id_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.NatTrans.app Hom.hom CategoryTheory.Iso.inv CategoryTheory.SingleFunctors instCategory CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.comp_app inv_hom_id_hom CategoryTheory.NatTrans.id_app
inv_hom_id_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.NatTrans.app Hom.hom CategoryTheory.Iso.inv CategoryTheory.SingleFunctors instCategory CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_hom_app
inv_hom_id_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor Hom.hom CategoryTheory.Iso.inv CategoryTheory.SingleFunctors instCategory CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_hom
isoMk_hom_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp functor CategoryTheory.shiftFunctor CategoryTheory.Iso.hom shiftIso CategoryTheory.Functor.whiskerRight	Hom.hom CategoryTheory.SingleFunctors instCategory isoMk	—	—
isoMk_inv_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp functor CategoryTheory.shiftFunctor CategoryTheory.Iso.hom shiftIso CategoryTheory.Functor.whiskerRight	Hom.hom CategoryTheory.Iso.inv CategoryTheory.SingleFunctors instCategory isoMk	—	—
postcompFunctor_map_hom 📖	mathematical	—	Hom.hom postcomp CategoryTheory.Functor.map CategoryTheory.SingleFunctors instCategory postcompFunctor CategoryTheory.Functor.whiskerRight functor	—	—
postcompFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.SingleFunctors instCategory postcompFunctor postcomp	—	—
postcompIsoOfIso_hom_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app functor postcomp Hom.hom CategoryTheory.Iso.hom CategoryTheory.SingleFunctors instCategory postcompIsoOfIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj	—	—
postcompIsoOfIso_inv_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app functor postcomp Hom.hom CategoryTheory.Iso.inv CategoryTheory.SingleFunctors instCategory postcompIsoOfIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj	—	—
postcompPostcompIso_hom_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app functor postcomp CategoryTheory.Functor.comp CategoryTheory.Functor.CommShift.comp Hom.hom CategoryTheory.Iso.hom CategoryTheory.SingleFunctors instCategory postcompPostcompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
postcompPostcompIso_inv_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app functor postcomp CategoryTheory.Functor.comp CategoryTheory.Functor.CommShift.comp Hom.hom CategoryTheory.Iso.inv CategoryTheory.SingleFunctors instCategory postcompPostcompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
postcomp_functor 📖	mathematical	—	functor postcomp CategoryTheory.Functor.comp	—	—
postcomp_shiftIso_hom_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor CategoryTheory.shiftFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftIso postcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.Functor.CommShift.commShiftIso CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp
postcomp_shiftIso_inv_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor CategoryTheory.shiftFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftIso postcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Functor.CommShift.commShiftIso	—	CategoryTheory.Category.comp_id
shiftIso_add 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	shiftIso CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp functor CategoryTheory.shiftFunctor CategoryTheory.Functor.isoWhiskerLeft CategoryTheory.shiftFunctorAdd CategoryTheory.Iso.symm CategoryTheory.Functor.associator CategoryTheory.Functor.isoWhiskerRight	—	—
shiftIso_add' 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	shiftIso CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp functor CategoryTheory.shiftFunctor CategoryTheory.Functor.isoWhiskerLeft CategoryTheory.shiftFunctorAdd' CategoryTheory.Iso.symm CategoryTheory.Functor.associator CategoryTheory.Functor.isoWhiskerRight	—	CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd shiftIso_add
shiftIso_add'_hom_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor CategoryTheory.shiftFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctorAdd' CategoryTheory.Functor.map	—	shiftIso_add' CategoryTheory.Category.id_comp
shiftIso_add'_inv_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.NatTrans.app functor CategoryTheory.Functor.comp CategoryTheory.shiftFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.shiftFunctorAdd'	—	shiftIso_add' CategoryTheory.Category.assoc CategoryTheory.Category.id_comp
shiftIso_add_hom_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor CategoryTheory.shiftFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctorAdd CategoryTheory.Functor.map	—	shiftIso_add CategoryTheory.Category.id_comp
shiftIso_add_inv_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.NatTrans.app functor CategoryTheory.Functor.comp CategoryTheory.shiftFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.shiftFunctorAdd	—	shiftIso_add CategoryTheory.Category.assoc CategoryTheory.Category.id_comp
shiftIso_zero 📖	mathematical	—	shiftIso AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass zero_add CategoryTheory.Functor.isoWhiskerLeft functor CategoryTheory.shiftFunctor CategoryTheory.Functor.id CategoryTheory.shiftFunctorZero	—	—
shiftIso_zero_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor CategoryTheory.shiftFunctor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftIso zero_add CategoryTheory.Functor.id CategoryTheory.shiftFunctorZero CategoryTheory.Functor.obj	—	zero_add shiftIso_zero
shiftIso_zero_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app functor CategoryTheory.Functor.comp CategoryTheory.shiftFunctor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftIso zero_add CategoryTheory.Functor.id CategoryTheory.shiftFunctorZero	—	zero_add shiftIso_zero

CategoryTheory.SingleFunctors.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	1 math math: comp_hom
hom 📖	CompOp	34 math math: CategoryTheory.SingleFunctors.postcompPostcompIso_hom_hom_app, comm, CategoryTheory.SingleFunctors.id_hom, comp_hom, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, comm_assoc, CategoryTheory.SingleFunctors.comp_hom_assoc, id_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CategoryTheory.SingleFunctors.isoMk_inv_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CategoryTheory.SingleFunctors.postcompIsoOfIso_hom_hom_app, CategoryTheory.SingleFunctors.inv_hom_id_hom_assoc, CategoryTheory.SingleFunctors.hom_inv_id_hom, CategoryTheory.SingleFunctors.hom_inv_id_hom_app_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CategoryTheory.SingleFunctors.postcompPostcompIso_inv_hom_app, CategoryTheory.SingleFunctors.isoMk_hom_hom, CategoryTheory.SingleFunctors.inv_hom_id_hom_app_assoc, CategoryTheory.SingleFunctors.hom_inv_id_hom_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, CategoryTheory.SingleFunctors.inv_hom_id_hom_app, CategoryTheory.SingleFunctors.evaluation_map, CategoryTheory.SingleFunctors.comp_hom, CategoryTheory.SingleFunctors.instIsIsoFunctorHom, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, ext_iff, CategoryTheory.SingleFunctors.postcompFunctor_map_hom, CategoryTheory.SingleFunctors.hom_inv_id_hom_app, CategoryTheory.SingleFunctors.inv_hom_id_hom, CategoryTheory.SingleFunctors.postcompIsoOfIso_inv_hom_app, CategoryTheory.SingleFunctors.hom_ext_iff
id 📖	CompOp	1 math math: id_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.SingleFunctors.functor CategoryTheory.shiftFunctor CategoryTheory.Iso.hom CategoryTheory.SingleFunctors.shiftIso hom CategoryTheory.Functor.whiskerRight	—	—
comm_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.SingleFunctors.functor CategoryTheory.shiftFunctor CategoryTheory.Iso.hom CategoryTheory.SingleFunctors.shiftIso hom CategoryTheory.Functor.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
comp_hom 📖	mathematical	—	hom comp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.SingleFunctors.functor	—	—
ext 📖	—	hom	—	—	—
ext_iff 📖	mathematical	—	hom	—	ext
id_hom 📖	mathematical	—	hom id CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.SingleFunctors.functor	—	—

---

← Back to Index