Documentation Verification Report

Basic

📁 Source: Mathlib/CategoryTheory/Abelian/Preradical/Basic.lean

Statistics

Metric	Count
Definitions `Preradical`, `IsIdempotent`, `r`, `ι`	4
Theorems `isIso_whiskerLeft_r_ι`, `instIsIsoAppιObjROfIsIdempotent`, `instIsIsoMapRAppιOfIsIdempotent`, `instMonoFunctorWhiskerLeftι`, `r_map_ι_app`	5
Total	9

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
`Preradical` 📖	CompOp	4 math math: `Preradical.isRadical_iff_isIso`, `Radical.instIsIsoPreradicalToColonObjIsRadical`, `Radical.isZero`, `Preradical.isIso_toColon_iff`

CategoryTheory.Abelian.Preradical

Definitions

Name	Category	Theorems
`IsIdempotent` 📖	CompData	—
`r` 📖	CompOp	28 math math: `shortComplex_X₁`, `colon_ι_app_π_app`, `isPullback_colon_obj`, `instEpiAppColonπ`, `isRadical_iff_isZero`, `ι_π_assoc`, `IsIdempotent.isIso_whiskerLeft_r_ι`, `toColon_hom_left_app_colon_ι_app_assoc`, `instEpiFunctorColonπ`, `toColon_hom_left_colonπ_assoc`, `ι_π`, `shortComplexObj_X₁`, `toColon_hom_left_colonπ`, `instIsIsoMapRAppιOfIsIdempotent`, `isIso_toColon_hom_left_app_iff`, `shortComplexObj_f`, `toColon_hom_left_app_colonπ_app_assoc`, `ι_π_app`, `toColon_hom_left_app_colon_ι_app`, `r_map_ι_app`, `instIsIsoAppιObjROfIsIdempotent`, `colon_ι_app_π_app_assoc`, `isPullback_colon`, `ι_π_app_assoc`, `CategoryTheory.Abelian.Radical.isZero`, `isIso_toColon_iff`, `toColon_hom_left_app_colonπ_app`, `instMonoFunctorWhiskerLeftι`
`ι` 📖	CompOp	17 math math: `colon_ι_app_π_app`, `isPullback_colon_obj`, `ι_π_assoc`, `IsIdempotent.isIso_whiskerLeft_r_ι`, `toColon_hom_left_app_colon_ι_app_assoc`, `ι_π`, `instIsIsoMapRAppιOfIsIdempotent`, `shortComplexObj_f`, `ι_π_app`, `toColon_hom_left_app_colon_ι_app`, `shortComplex_f`, `r_map_ι_app`, `instIsIsoAppιObjROfIsIdempotent`, `colon_ι_app_π_app_assoc`, `isPullback_colon`, `ι_π_app_assoc`, `instMonoFunctorWhiskerLeftι`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoAppιObjROfIsIdempotent` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `r` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `ι`	—	—
`instIsIsoMapRAppιOfIsIdempotent` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `r` `CategoryTheory.Functor.id` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `ι`	—	`r_map_ι_app` `instIsIsoAppιObjROfIsIdempotent`
`instMonoFunctorWhiskerLeftι` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `r` `CategoryTheory.Functor.id` `CategoryTheory.Functor.whiskerLeft` `ι`	—	`CategoryTheory.NatTrans.mono_iff_mono_app` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.instMonoAppOfFunctor` `CategoryTheory.MonoOver.mono`
`r_map_ι_app` 📖	mathematical	—	`CategoryTheory.Functor.map` `r` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `ι`	—	`CategoryTheory.cancel_mono` `CategoryTheory.instMonoAppOfFunctor` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.MonoOver.mono` `CategoryTheory.NatTrans.naturality`

CategoryTheory.Abelian.Preradical.IsIdempotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIso_whiskerLeft_r_ι` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Abelian.Preradical.r` `CategoryTheory.Functor.id` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Abelian.Preradical.ι`	—	—

---

← Back to Index