Documentation Verification Report

Bifunctor

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

Statistics

Metric	Count
Definitions `mapBifunctor`, `mapBifunctorMap`, `mapBifunctorMapMap`, `mapBifunctorMapMapIso`, `mapBifunctorMapObj`, `mapBifunctorMapObjDesc`, `ιMapBifunctorMapObj`	7
Theorems `instIsIsoMapBifunctorMapMap`, `mapBifunctorMapMapIso_hom`, `mapBifunctorMapMapIso_inv`, `mapBifunctorMapObj_ext`, `mapBifunctorMapObj_ext_iff`, `mapBifunctorMap_map_app`, `mapBifunctorMap_obj_map`, `mapBifunctorMap_obj_obj`, `mapBifunctor_map_app`, `mapBifunctor_obj_map`, `mapBifunctor_obj_obj`, `ι_mapBifunctorMapMap`, `ι_mapBifunctorMapMap_assoc`, `ι_mapBifunctorMapObjDesc`, `ι_mapBifunctorMapObjDesc_assoc`	15
Total	22

CategoryTheory.GradedObject

Definitions

Name	Category	Theorems
`mapBifunctor` 📖	CompOp	23 math math: `CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f`, `Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit`, `mapBifunctorObjObjSingle₀Iso_hom`, `HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ`, `mapBifunctor_obj_obj`, `mapBifunctorRightUnitorCofan_inj`, `mapBifunctorLeftUnitorCofan_inj`, `HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ`, `mapBifunctorObjSingle₀ObjIso_hom`, `mapBifunctorObjSingle₀ObjIso_inv`, `mapBifunctorRightUnitor_hasMap`, `mapBifunctor_map_app`, `mapBifunctorObjObjSingle₀Iso_inv`, `mapBifunctorRightUnitorCofan_inj_assoc`, `mapBifunctorLeftUnitor_hasMap`, `HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX`, `Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1`, `mapBifunctor_obj_map`, `mapBifunctorLeftUnitorCofan_inj_assoc`, `CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f`, `CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f`, `CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject`, `CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f`
`mapBifunctorMap` 📖	CompOp	3 math math: `mapBifunctorMap_obj_map`, `mapBifunctorMap_map_app`, `mapBifunctorMap_obj_obj`
`mapBifunctorMapMap` 📖	CompOp	16 math math: `ι_mapBifunctorMapMap`, `mapBifunctor_triangle`, `mapBifunctorMap_obj_map`, `mapBifunctorMapMapIso_hom`, `instIsIsoMapBifunctorMapMap`, `mapBifunctorMapMapIso_inv`, `mapBifunctorRightUnitor_inv_naturality_assoc`, `mapBifunctorLeftUnitor_inv_naturality_assoc`, `mapBifunctorRightUnitor_naturality`, `ι_mapBifunctorMapMap_assoc`, `mapBifunctorMap_map_app`, `mapBifunctorLeftUnitor_naturality`, `mapBifunctorRightUnitor_naturality_assoc`, `mapBifunctorLeftUnitor_naturality_assoc`, `mapBifunctorLeftUnitor_inv_naturality`, `mapBifunctorRightUnitor_inv_naturality`
`mapBifunctorMapMapIso` 📖	CompOp	2 math math: `mapBifunctorMapMapIso_hom`, `mapBifunctorMapMapIso_inv`
`mapBifunctorMapObj` 📖	CompOp	49 math math: `ι_mapBifunctorMapMap`, `ι_mapBifunctorMapObjDesc`, `mapBifunctor_triangle`, `ιMapBifunctor₁₂BifunctorMapObj_eq_assoc`, `ι_mapBifunctorComp₁₂MapObjIso_hom_assoc`, `mapBifunctorMapMapIso_hom`, `ι_mapBifunctor₁₂BifunctorDesc`, `ιMapBifunctorBifunctor₂₃MapObj_eq_assoc`, `ι_mapBifunctorRightUnitor_hom_apply`, `ι_mapBifunctorBifunctor₂₃Desc`, `HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ`, `instIsIsoMapBifunctorMapMap`, `ι_mapBifunctorComp₂₃MapObjIso_hom`, `mapBifunctorMapMapIso_inv`, `ι_mapBifunctorAssociator_hom_assoc`, `mapBifunctorRightUnitor_inv_naturality_assoc`, `mapBifunctorLeftUnitor_inv_naturality_assoc`, `mapBifunctor₁₂BifunctorMapObj_ext_iff`, `mapBifunctorRightUnitor_inv_apply`, `ι_mapBifunctorComp₁₂MapObjIso_inv`, `ι_mapBifunctorMapObjDesc_assoc`, `ι_mapBifunctorAssociator_hom`, `mapBifunctorRightUnitor_naturality`, `mapBifunctorLeftUnitor_inv_apply`, `ι_mapBifunctorMapMap_assoc`, `ι_mapBifunctor₁₂BifunctorDesc_assoc`, `mapBifunctorMap_map_app`, `mapBifunctorMapObj_ext_iff`, `mapBifunctorLeftUnitor_naturality`, `ι_mapBifunctorLeftUnitor_hom_apply`, `mapBifunctorRightUnitor_naturality_assoc`, `ι_mapBifunctorBifunctor₂₃Desc_assoc`, `mapBifunctorBifunctor₂₃MapObj_ext_iff`, `HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX`, `mapBifunctorLeftUnitor_naturality_assoc`, `ιMapBifunctor₁₂BifunctorMapObj_eq`, `ι_mapBifunctorComp₂₃MapObjIso_inv`, `mapBifunctorLeftUnitor_inv_naturality`, `ιMapBifunctorBifunctor₂₃MapObj_eq`, `ι_mapBifunctorAssociator_inv_assoc`, `ι_mapBifunctorAssociator_inv`, `ι_mapBifunctorComp₁₂MapObjIso_hom`, `ι_mapBifunctorRightUnitor_hom_apply_assoc`, `ι_mapBifunctorLeftUnitor_hom_apply_assoc`, `mapBifunctorMap_obj_obj`, `mapBifunctorRightUnitor_inv_naturality`, `ι_mapBifunctorComp₂₃MapObjIso_hom_assoc`, `ι_mapBifunctorComp₂₃MapObjIso_inv_assoc`, `ι_mapBifunctorComp₁₂MapObjIso_inv_assoc`
`mapBifunctorMapObjDesc` 📖	CompOp	2 math math: `ι_mapBifunctorMapObjDesc`, `ι_mapBifunctorMapObjDesc_assoc`
`ιMapBifunctorMapObj` 📖	CompOp	15 math math: `ι_mapBifunctorMapMap`, `ι_mapBifunctorMapObjDesc`, `ιMapBifunctor₁₂BifunctorMapObj_eq_assoc`, `ιMapBifunctorBifunctor₂₃MapObj_eq_assoc`, `ι_mapBifunctorRightUnitor_hom_apply`, `mapBifunctorRightUnitor_inv_apply`, `ι_mapBifunctorMapObjDesc_assoc`, `mapBifunctorLeftUnitor_inv_apply`, `ι_mapBifunctorMapMap_assoc`, `mapBifunctorMapObj_ext_iff`, `ι_mapBifunctorLeftUnitor_hom_apply`, `ιMapBifunctor₁₂BifunctorMapObj_eq`, `ιMapBifunctorBifunctor₂₃MapObj_eq`, `ι_mapBifunctorRightUnitor_hom_apply_assoc`, `ι_mapBifunctorLeftUnitor_hom_apply_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoMapBifunctorMapMap` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.IsIso` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `mapBifunctorMapObj` `mapBifunctorMapMap`	—	—
`mapBifunctorMapMapIso_hom` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.Iso.hom` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `mapBifunctorMapObj` `mapBifunctorMapMapIso` `mapBifunctorMapMap`	—	—
`mapBifunctorMapMapIso_inv` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.Iso.inv` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `mapBifunctorMapObj` `mapBifunctorMapMapIso` `mapBifunctorMapMap`	—	—
`mapBifunctorMapObj_ext` 📖	—	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `mapBifunctorMapObj` `ιMapBifunctorMapObj`	—	—	`mapObj_ext`
`mapBifunctorMapObj_ext_iff` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctorMapObj` `ιMapBifunctorMapObj`	—	`mapBifunctorMapObj_ext`
`mapBifunctorMap_map_app` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.NatTrans.app` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `mapBifunctorMapObj` `mapBifunctorMapMap` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctorMap`	—	—
`mapBifunctorMap_obj_map` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.Functor.map` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctorMap` `mapBifunctorMapMap` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`mapBifunctorMap_obj_obj` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctorMap` `mapBifunctorMapObj`	—	—
`mapBifunctor_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.map` `mapBifunctor`	—	—
`mapBifunctor_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	—	—
`mapBifunctor_obj_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	—	—
`ι_mapBifunctorMapMap` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctorMapObj` `ιMapBifunctorMapObj` `mapBifunctorMapMap` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map`	—	`ι_mapMap` `CategoryTheory.Category.assoc`
`ι_mapBifunctorMapMap_assoc` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctorMapObj` `ιMapBifunctorMapObj` `mapBifunctorMapMap` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_mapBifunctorMapMap`
`ι_mapBifunctorMapObjDesc` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctorMapObj` `ιMapBifunctorMapObj` `mapBifunctorMapObjDesc`	—	`ι_descMapObj`
`ι_mapBifunctorMapObjDesc_assoc` 📖	mathematical	`HasMap` `CategoryTheory.Functor.obj` `CategoryTheory.GradedObject` `categoryOfGradedObjects` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctor`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `mapBifunctorMapObj` `ιMapBifunctorMapObj` `mapBifunctorMapObjDesc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_mapBifunctorMapObjDesc`

---

← Back to Index