Documentation Verification Report

Sum

📁 Source: Mathlib/CategoryTheory/Join/Sum.lean

Statistics

Metric	Count
Definitions `fromSum`, `inlCompFromSum`, `inrCompFromSum`	3
Theorems `fromSum_map_inl`, `fromSum_map_inr`, `fromSum_obj`, `inlCompFromSum_hom_app`, `inlCompFromSum_inv_app`, `inrCompFromSum_hom_app`, `inrCompFromSum_inv_app`, `instEssSurjSumFromSum`, `instFaithfulSumFromSum`	9
Total	12

CategoryTheory.Join

Definitions

Name	Category	Theorems
`fromSum` 📖	CompOp	9 math math: `inlCompFromSum_hom_app`, `inrCompFromSum_hom_app`, `fromSum_map_inr`, `instFaithfulSumFromSum`, `fromSum_obj`, `inrCompFromSum_inv_app`, `instEssSurjSumFromSum`, `fromSum_map_inl`, `inlCompFromSum_inv_app`
`inlCompFromSum` 📖	CompOp	2 math math: `inlCompFromSum_hom_app`, `inlCompFromSum_inv_app`
`inrCompFromSum` 📖	CompOp	2 math math: `inrCompFromSum_hom_app`, `inrCompFromSum_inv_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromSum_map_inl` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.sum` `CategoryTheory.Join` `instCategory` `fromSum` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inl_` `inclLeft`	—	—
`fromSum_map_inr` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.sum` `CategoryTheory.Join` `instCategory` `fromSum` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inr_` `inclRight`	—	—
`fromSum_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.sum` `CategoryTheory.Join` `instCategory` `fromSum` `left` `right`	—	—
`inlCompFromSum_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Join` `instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.sum` `CategoryTheory.Sum.inl_` `CategoryTheory.Functor.sum'` `inclLeft` `inclRight` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `fromSum` `inlCompFromSum` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `left`	—	—
`inlCompFromSum_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Join` `instCategory` `inclLeft` `CategoryTheory.Functor.comp` `CategoryTheory.sum` `CategoryTheory.Sum.inl_` `CategoryTheory.Functor.sum'` `inclRight` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `fromSum` `inlCompFromSum` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `left`	—	—
`inrCompFromSum_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Join` `instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.sum` `CategoryTheory.Sum.inr_` `CategoryTheory.Functor.sum'` `inclLeft` `inclRight` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `fromSum` `inrCompFromSum` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `right`	—	—
`inrCompFromSum_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Join` `instCategory` `inclRight` `CategoryTheory.Functor.comp` `CategoryTheory.sum` `CategoryTheory.Sum.inr_` `CategoryTheory.Functor.sum'` `inclLeft` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `fromSum` `inrCompFromSum` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `right`	—	—
`instEssSurjSumFromSum` 📖	mathematical	—	`CategoryTheory.Functor.EssSurj` `CategoryTheory.Join` `CategoryTheory.sum` `instCategory` `fromSum`	—	`CategoryTheory.Functor.obj_mem_essImage`
`instFaithfulSumFromSum` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.sum` `CategoryTheory.Join` `instCategory` `fromSum`	—	`CategoryTheory.Functor.map_injective` `inclLeftFaithful` `inclRightFaithful`

---

← Back to Index