BifunctorCokernel

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/BifunctorCokernel.lean

Statistics

Metric	Count
Definitions isColimitMapBifunctor, mapBifunctor	2
Theorems exists_desc, hom_ext	2
Total	4

CategoryTheory.Limits.CokernelCofork

Definitions

Name	Category	Theorems
isColimitMapBifunctor 📖	CompOp	—
mapBifunctor 📖	CompOp	—

CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_desc 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.coprod CategoryTheory.Limits.coprod.desc CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.Cofork.π	—	CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip CategoryTheory.whisker_eq CategoryTheory.Limits.CokernelCofork.condition CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero CategoryTheory.Limits.coprod.inl_desc_assoc CategoryTheory.Limits.Cofork.IsColimit.hom_ext CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Limits.coprod.inr_desc_assoc
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Limits.Cofork.π	—	—	CategoryTheory.Limits.Cofork.IsColimit.hom_ext CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip

---

← Back to Index