Documentation Verification Report

Preadditive

📁 Source: Mathlib/CategoryTheory/Generator/Preadditive.lean

Statistics

Metric	Count
Definitions	0
Theorems `isCoseparating_iff`, `isCoseparator_iff`, `isSeparating_iff`, `isSeparator_iff`, `isCoseparator_iff_faithful_preadditiveYoneda`, `isCoseparator_iff_faithful_preadditiveYonedaObj`, `isSeparator_iff_faithful_preadditiveCoyoneda`, `isSeparator_iff_faithful_preadditiveCoyonedaObj`	8
Total	8

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoseparator_iff_faithful_preadditiveYoneda` 📖	mathematical	—	`IsCoseparator` `Functor.Faithful` `Opposite` `Category.opposite` `AddCommGrpCat` `AddCommGrpCat.instCategory` `Functor.obj` `Functor` `Functor.category` `preadditiveYoneda`	—	`isCoseparator_iff_faithful_yoneda_obj` `whiskering_preadditiveYoneda` `Functor.comp_obj` `Functor.whiskeringRight_obj_obj` `Functor.Faithful.of_comp` `Functor.Faithful.comp` `instFaithfulForget`
`isCoseparator_iff_faithful_preadditiveYonedaObj` 📖	mathematical	—	`IsCoseparator` `Functor.Faithful` `Opposite` `Category.opposite` `ModuleCat` `End` `Category.toCategoryStruct` `Preadditive.instRingEnd` `ModuleCat.moduleCategory` `preadditiveYonedaObj`	—	`isCoseparator_iff_faithful_preadditiveYoneda` `preadditiveYoneda_obj` `Functor.Faithful.of_comp` `Functor.Faithful.comp` `forget₂_faithful`
`isSeparator_iff_faithful_preadditiveCoyoneda` 📖	mathematical	—	`IsSeparator` `Functor.Faithful` `AddCommGrpCat` `AddCommGrpCat.instCategory` `Functor.obj` `Opposite` `Category.opposite` `Functor` `Functor.category` `preadditiveCoyoneda` `Opposite.op`	—	`isSeparator_iff_faithful_coyoneda_obj` `whiskering_preadditiveCoyoneda` `Functor.comp_obj` `Functor.whiskeringRight_obj_obj` `Functor.Faithful.of_comp` `Functor.Faithful.comp` `instFaithfulForget`
`isSeparator_iff_faithful_preadditiveCoyonedaObj` 📖	mathematical	—	`IsSeparator` `Functor.Faithful` `ModuleCat` `MulOpposite` `End` `Category.toCategoryStruct` `MulOpposite.instRing` `Preadditive.instRingEnd` `ModuleCat.moduleCategory` `preadditiveCoyonedaObj`	—	`isSeparator_iff_faithful_preadditiveCoyoneda` `preadditiveCoyoneda_obj` `Functor.Faithful.of_comp` `Functor.Faithful.comp` `forget₂_faithful`

CategoryTheory.Preadditive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoseparating_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsCoseparating` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `preadditiveHasZeroMorphisms`	—	`CategoryTheory.Limits.zero_comp` `sub_eq_zero` `sub_comp`
`isCoseparator_iff` 📖	mathematical	—	`CategoryTheory.IsCoseparator` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `preadditiveHasZeroMorphisms`	—	`CategoryTheory.IsCoseparator.def` `CategoryTheory.Limits.zero_comp` `CategoryTheory.isCoseparator_def` `sub_eq_zero` `sub_comp`
`isSeparating_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsSeparating` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `preadditiveHasZeroMorphisms`	—	`CategoryTheory.Limits.comp_zero` `sub_eq_zero` `comp_sub`
`isSeparator_iff` 📖	mathematical	—	`CategoryTheory.IsSeparator` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `preadditiveHasZeroMorphisms`	—	`CategoryTheory.IsSeparator.def` `CategoryTheory.Limits.comp_zero` `CategoryTheory.isSeparator_def` `sub_eq_zero` `comp_sub`

---

← Back to Index