Documentation Verification Report

KernelPair

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean

Statistics

Metric	Count
Definitions `IsKernelPair`, `instInhabitedIdOfMono`, `lift'`, `toCoequalizer`, `toCoequalizer'`	5
Theorems `cancel_right`, `cancel_right_of_mono`, `comp_of_mono`, `id_of_mono`, `instSubsingleton`, `isIso_of_mono`, `lift_fst`, `lift_fst_assoc`, `lift_snd`, `lift_snd_assoc`, `mono_of_eq_fst_snd`, `mono_of_eq_fst_snd'`, `mono_of_isIso_fst`, `of_hasPullback`, `of_isIso_of_mono`, `pullback`	16
Total	21

CategoryTheory

Definitions

Name	Category	Theorems
`IsKernelPair` 📖	MathDef	5 math math: `Limits.pullback.diagonal_isKernelPair`, `IsKernelPair.instSubsingleton`, `IsKernelPair.of_isIso_of_mono`, `IsKernelPair.of_hasPullback`, `IsKernelPair.id_of_mono`

CategoryTheory.IsKernelPair

Definitions

Name	Category	Theorems
`instInhabitedIdOfMono` 📖	CompOp	—
`lift'` 📖	CompOp	—
`toCoequalizer` 📖	CompOp	—
`toCoequalizer'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cancel_right` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.IsKernelPair`	—	—	`CategoryTheory.Limits.PullbackCone.condition_assoc` `CategoryTheory.Limits.IsLimit.fac` `CategoryTheory.Limits.IsLimit.hom_ext` `CategoryTheory.Limits.PullbackCone.equalizer_ext` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'`
`cancel_right_of_mono` 📖	—	`CategoryTheory.IsKernelPair` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—	`cancel_right` `CategoryTheory.cancel_mono` `CategoryTheory.Category.assoc` `CategoryTheory.CommSq.w` `CategoryTheory.IsPullback.toCommSq`
`comp_of_mono` 📖	mathematical	`CategoryTheory.IsKernelPair`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.CommSq.w_assoc` `CategoryTheory.IsPullback.toCommSq` `CategoryTheory.cancel_mono` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.PullbackCone.condition` `lift_fst` `lift_snd` `CategoryTheory.Limits.IsLimit.hom_ext` `CategoryTheory.Limits.PullbackCone.equalizer_ext`
`id_of_mono` 📖	mathematical	—	`CategoryTheory.IsKernelPair` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.CommSq.w`
`instSubsingleton` 📖	mathematical	—	`CategoryTheory.IsKernelPair`	—	—
`isIso_of_mono` 📖	mathematical	`CategoryTheory.IsKernelPair`	`CategoryTheory.IsIso`	—	`id_of_mono` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp` `CategoryTheory.Iso.isIso_inv`
`lift_fst` 📖	mathematical	`CategoryTheory.IsKernelPair` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`lift`	—	`CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst`
`lift_fst_assoc` 📖	mathematical	`CategoryTheory.IsKernelPair` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`lift`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_fst`
`lift_snd` 📖	mathematical	`CategoryTheory.IsKernelPair` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`lift`	—	`CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd`
`lift_snd_assoc` 📖	mathematical	`CategoryTheory.IsKernelPair` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`lift`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_snd`
`mono_of_eq_fst_snd` 📖	mathematical	`CategoryTheory.IsKernelPair`	`CategoryTheory.Mono`	—	`mono_of_eq_fst_snd'`
`mono_of_eq_fst_snd'` 📖	mathematical	`CategoryTheory.IsKernelPair`	`CategoryTheory.Mono`	—	`lift_fst` `lift_snd`
`mono_of_isIso_fst` 📖	mathematical	`CategoryTheory.IsKernelPair`	`CategoryTheory.Mono`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.IsPullback.cone_fst` `CategoryTheory.Category.comp_id` `CategoryTheory.IsIso.inv_comp_eq` `CategoryTheory.IsIso.eq_comp_inv`
`of_hasPullback` 📖	mathematical	—	`CategoryTheory.IsKernelPair` `CategoryTheory.Limits.pullback` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.IsPullback.of_hasPullback`
`of_isIso_of_mono` 📖	mathematical	—	`CategoryTheory.IsKernelPair`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.IsPullback.paste_vert` `CategoryTheory.IsPullback.of_horiz_isIso` `CategoryTheory.IsIso.id` `id_of_mono`
`pullback` 📖	mathematical	`CategoryTheory.IsKernelPair`	`CategoryTheory.Limits.pullback` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.comp_id` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.CommSq.w` `CategoryTheory.IsPullback.toCommSq`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.CommSq.w` `CategoryTheory.IsPullback.toCommSq` `CategoryTheory.Limits.pullback.lift_fst` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.PullbackCone.condition` `CategoryTheory.Limits.pullback.condition` `lift_fst_assoc` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.limit.lift_π_assoc` `lift_fst` `CategoryTheory.Limits.pullback.lift.congr_simp` `lift_snd` `CategoryTheory.eq_whisker` `CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext`

---

← Back to Index