Documentation Verification Report

Trifunctor

📁 Source: Mathlib/CategoryTheory/Localization/Trifunctor.lean

Statistics

Metric	Count
Definitions `Lifting₃`, `bifunctorComp₁₂`, `bifunctorComp₂₃`, `iso`, `iso'`, `uncurry`, `associator`, `instLifting₃Lift₃`, `lift₃`, `lift₃NatIso`, `lift₃NatTrans`, `IsInvertedBy₃`	12
Theorems `associator_hom_app_app_app`, `lift₃NatIso_hom`, `lift₃NatIso_inv`, `lift₃NatTrans_app_app_app`, `natTrans₃_ext`	5
Total	17

CategoryTheory.Localization

Definitions

Name	Category	Theorems
`Lifting₃` 📖	CompData	—
`associator` 📖	CompOp	1 math math: `associator_hom_app_app_app`
`instLifting₃Lift₃` 📖	CompOp	—
`lift₃` 📖	CompOp	—
`lift₃NatIso` 📖	CompOp	2 math math: `lift₃NatIso_hom`, `lift₃NatIso_inv`
`lift₃NatTrans` 📖	CompOp	3 math math: `lift₃NatIso_hom`, `lift₃NatTrans_app_app_app`, `lift₃NatIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_hom_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.bifunctorComp₂₃` `CategoryTheory.Iso.hom` `associator` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.whiskeringLeft₂` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.Functor.map` `Lifting₂.iso` `CategoryTheory.Iso.inv`	—	`lift₃NatTrans_app_app_app` `CategoryTheory.Category.assoc`
`lift₃NatIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `lift₃NatIso` `lift₃NatTrans`	—	—
`lift₃NatIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `lift₃NatIso` `lift₃NatTrans`	—	—
`lift₃NatTrans_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `lift₃NatTrans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.whiskeringLeft₃` `CategoryTheory.Iso.hom` `Lifting₃.iso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Functor.currying₃_unitIso_hom_app_app_app_app` `CategoryTheory.Functor.currying₃_unitIso_inv_app_app_app_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `liftNatTrans_app`
`natTrans₃_ext` 📖	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	—	`CategoryTheory.Functor.map_injective` `CategoryTheory.Functor.instFaithfulProdUncurry₃` `natTrans_ext` `CategoryTheory.Functor.IsLocalization.prod` `CategoryTheory.MorphismProperty.Prod.containsIdentities`

CategoryTheory.Localization.Lifting₃

Definitions

Name	Category	Theorems
`bifunctorComp₁₂` 📖	CompOp	—
`bifunctorComp₂₃` 📖	CompOp	—
`iso` 📖	CompOp	1 math math: `CategoryTheory.Localization.lift₃NatTrans_app_app_app`
`iso'` 📖	CompOp	—
`uncurry` 📖	CompOp	—

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`IsInvertedBy₃` 📖	MathDef	—

---

← Back to Index