Limits

Statistics

Metric	Count
Definitions	0
Theorems `preservesLimits_preadditiveCoyonedaObj`, `preservesLimits_preadditiveCoyoneda_obj`, `preservesLimits_preadditiveYonedaObj`, `preservesLimits_preadditiveYoneda_obj`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`preservesLimits_preadditiveCoyonedaObj` 📖	mathematical	—	`Limits.PreservesLimits` `ModuleCat` `MulOpposite` `End` `Category.toCategoryStruct` `MulOpposite.instRing` `Preadditive.instRingEnd` `ModuleCat.moduleCategory` `preadditiveCoyonedaObj`	—	`coyoneda_preservesLimits` `Limits.preservesLimits_of_reflects_of_preserves` `ModuleCat.forget_reflectsLimits`
`preservesLimits_preadditiveCoyoneda_obj` 📖	mathematical	—	`Limits.PreservesLimits` `AddCommGrpCat` `AddCommGrpCat.instCategory` `Functor.obj` `Opposite` `Category.opposite` `Functor` `Functor.category` `preadditiveCoyoneda`	—	`Limits.comp_preservesLimits` `preservesLimits_preadditiveCoyonedaObj` `ModuleCat.forget₂AddCommGroup_preservesLimits`
`preservesLimits_preadditiveYonedaObj` 📖	mathematical	—	`Limits.PreservesLimits` `Opposite` `Category.opposite` `ModuleCat` `End` `Category.toCategoryStruct` `Preadditive.instRingEnd` `ModuleCat.moduleCategory` `preadditiveYonedaObj`	—	`yoneda_preservesLimits` `Limits.preservesLimits_of_reflects_of_preserves` `ModuleCat.forget_reflectsLimits`
`preservesLimits_preadditiveYoneda_obj` 📖	mathematical	—	`Limits.PreservesLimits` `Opposite` `Category.opposite` `AddCommGrpCat` `AddCommGrpCat.instCategory` `Functor.obj` `Functor` `Functor.category` `preadditiveYoneda`	—	`Limits.comp_preservesLimits` `preservesLimits_preadditiveYonedaObj` `ModuleCat.forget₂AddCommGroup_preservesLimits`

---