Documentation Verification Report

Bifunctor

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

Statistics

Metric	Count
Definitions `Lifting₂`, `compRight`, `flip`, `fst`, `iso`, `iso'`, `liftingLift₂`, `liftingLift₂Flip`, `snd`, `uncurry`, `instLifting₂Lift₂`, `lift₂`, `lift₂NatIso`, `lift₂NatTrans`, `IsInvertedBy₂`	15
Theorems `lift₂NatIso_hom`, `lift₂NatIso_inv`, `lift₂NatTrans_app_app`, `lift₂_iso_hom_app_app₁`, `lift₂_iso_hom_app_app₂`, `natTrans₂_ext`	6
Total	21

CategoryTheory.Localization

Definitions

Name	Category	Theorems
`Lifting₂` 📖	CompData	—
`instLifting₂Lift₂` 📖	CompOp	2 math math: `lift₂_iso_hom_app_app₂`, `lift₂_iso_hom_app_app₁`
`lift₂` 📖	CompOp	2 math math: `lift₂_iso_hom_app_app₂`, `lift₂_iso_hom_app_app₁`
`lift₂NatIso` 📖	CompOp	2 math math: `lift₂NatIso_inv`, `lift₂NatIso_hom`
`lift₂NatTrans` 📖	CompOp	3 math math: `lift₂NatIso_inv`, `lift₂NatIso_hom`, `lift₂NatTrans_app_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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` 📖	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.IsLocalization.prod` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `liftNatTrans_app`
`lift₂_iso_hom_app_app₁` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy₂`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.whiskeringLeft₂` `lift₂` `CategoryTheory.Iso.hom` `Lifting₂.iso` `instLifting₂Lift₂` `CategoryTheory.Functor.comp` `Lifting.iso` `Lifting₂.liftingLift₂`	—	—
`lift₂_iso_hom_app_app₂` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy₂`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.whiskeringLeft₂` `lift₂` `CategoryTheory.Iso.hom` `Lifting₂.iso` `instLifting₂Lift₂` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.flip` `Lifting.iso` `Lifting₂.liftingLift₂Flip`	—	—
`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.Localization.Lifting₂

Definitions

Name	Category	Theorems
`compRight` 📖	CompOp	—
`flip` 📖	CompOp	—
`fst` 📖	CompOp	—
`iso` 📖	CompOp	6 math math: `CategoryTheory.Localization.lift₂_iso_hom_app_app₂`, `CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPost_iso`, `CategoryTheory.Localization.lift₂NatTrans_app_app`, `CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre_iso`, `CategoryTheory.Localization.lift₂_iso_hom_app_app₁`, `CategoryTheory.Localization.associator_hom_app_app_app`
`iso'` 📖	CompOp	—
`liftingLift₂` 📖	CompOp	1 math math: `CategoryTheory.Localization.lift₂_iso_hom_app_app₁`
`liftingLift₂Flip` 📖	CompOp	1 math math: `CategoryTheory.Localization.lift₂_iso_hom_app_app₂`
`snd` 📖	CompOp	—
`uncurry` 📖	CompOp	—

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`IsInvertedBy₂` 📖	MathDef	1 math math: `CategoryTheory.Localization.Monoidal.isInvertedBy₂`

---

← Back to Index