GradedObject

📁 Source: Mathlib/CategoryTheory/GradedObject.lean

Statistics

Metric	Count
Definitions GradedObject, CofanMapObjFun, iso, mk, HasMap, categoryOfGradedObjects, cofanMapObj, cofanMapObjComp, comap, comapEq, comapEquiv, descMapObj, eval, hasShift, hasZeroMorphisms, instZeroHomOfHasZeroMorphisms, isColimitCofanMapObj, isColimitCofanMapObjComp, isoMk, map, mapIso, mapMap, mapObj, mapObjFun, total, ιMapObj, ιMapObjOrZero, GradedObjectWithShift, inhabitedGradedObject	29
Theorems hasMap, inj_iso_hom, inj_iso_hom_assoc, ιMapObj_iso_inv, ιMapObj_iso_inv_assoc, categoryOfGradedObjects_comp, categoryOfGradedObjects_id, comapEq_hom_app, comapEq_inv_app, comapEq_symm, comapEq_trans, comapEquiv_counitIso, comapEquiv_functor, comapEquiv_inverse, comapEquiv_unitIso, congr_mapMap, eqToHom_apply, eqToHom_proj, eval_map, eval_obj, hasMap_comp, hasMap_of_iso, hasZeroObject, hom_ext, hom_ext_iff, instFaithfulTotal, isIso_apply_of_isIso, isIso_of_isIso_apply, isoMk_hom, isoMk_inv, mapIso_hom, mapIso_inv, mapMap_comp, mapMap_comp_assoc, mapMap_id, mapObj_ext, mapObj_ext_iff, map_map, map_obj, shiftFunctor_map_apply, shiftFunctor_obj_apply, zero_apply, ιMapObjOrZero_eq, ιMapObjOrZero_eq_zero, ιMapObjOrZero_mapMap, ιMapObjOrZero_mapMap_assoc, ι_descMapObj, ι_descMapObj_assoc, ι_mapMap, ι_mapMap_assoc, hom_inv_id_eval, hom_inv_id_eval_assoc, inv_hom_id_eval, inv_hom_id_eval_assoc, map_hom_inv_id_eval, map_hom_inv_id_eval_app, map_hom_inv_id_eval_app_assoc, map_hom_inv_id_eval_assoc, map_inv_hom_id_eval, map_inv_hom_id_eval_app, map_inv_hom_id_eval_app_assoc, map_inv_hom_id_eval_assoc	62
Total	91

CategoryTheory

Definitions

Name	Category	Theorems
GradedObject 📖	CompOp	115 math math: GradedObject.isoMk_hom, Functor.mapBifunctorHomologicalComplexObj_map_f_f, GradedObject.Monoidal.associator_naturality, GradedObject.singleObjApplyIso_inv_single_map, GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit, GradedObject.mapBifunctorObjObjSingle₀Iso_hom, GradedObject.mapTrifunctor_map_app_app, GradedObject.comapEquiv_counitIso, GradedObject.zero_apply, GradedObject.Monoidal.pentagon, GradedObject.mapMap_comp_assoc, GradedObject.mapIso_inv, HomologicalComplex.instFaithfulGradedObjectForget, GradedObject.Monoidal.rightUnitor_naturality_assoc, HomologicalComplex₂.toGradedObjectFunctor_obj, HomologicalComplex.forget_map, GradedObject.Monoidal.symmetry, GradedObject.mapTrifunctorObj_obj_obj, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ, GradedObject.mapBifunctor_obj_obj, HomologicalComplex.forgetEval_hom_app, GradedObject.Monoidal.rightUnitor_inv_apply, GradedObject.Monoidal.leftUnitor_inv_apply, GradedObject.isoMk_inv, Iso.hom_inv_id_eval_assoc, GradedObject.Monoidal.ιTensorObj₃_associator_inv, GradedObject.singleCompEval_hom_app, GradedObject.singleCompEval_inv_app, HomologicalComplex.gradedHomologyFunctor_map, GradedObject.Monoidal.tensorHom_comp_tensorHom, GradedObject.mapBifunctorRightUnitorCofan_inj, GradedObject.singleObjApplyIsoOfEq_inv_single_map, GradedObject.Monoidal.symmetry_assoc, GradedObject.mapTrifunctorMapIso_hom, GradedObject.categoryOfGradedObjects_id, GradedObject.Monoidal.tensorHom_comp_tensorHom_assoc, GradedObject.Monoidal.pentagon_inv, GradedObject.mapBifunctorLeftUnitorCofan_inj, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ, GradedObject.Monoidal.ιTensorObj₃_associator_inv_assoc, GradedObject.mapBifunctorObjSingle₀ObjIso_hom, GradedObject.mapMap_comp, GradedObject.comapEquiv_unitIso, GradedObject.singleObjApplyIso_inv_single_map_assoc, GradedObject.eval_map, GradedObject.Monoidal.tensorHom_def, GradedObject.mapBifunctorObjSingle₀ObjIso_inv, GradedObject.isIso_of_isIso_apply, GradedObject.Monoidal.hexagon_reverse, GradedObject.mapBifunctorRightUnitor_hasMap, GradedObject.Monoidal.id_tensorHom_id, GradedObject.map_obj, GradedObject.map_map, GradedObject.hasZeroObject, HomologicalComplex.forget_obj, GradedObject.mapMap_id, GradedObject.mapBifunctor_map_app, GradedObject.mapBifunctorObjObjSingle₀Iso_inv, Iso.map_hom_inv_id_eval_assoc, GradedObject.Monoidal.braiding_naturality_left, GradedObject.Monoidal.ιTensorObj₃'_associator_hom, GradedObject.single_map_singleObjApplyIsoOfEq_hom, GradedObject.comapEq_hom_app, GradedObject.comapEquiv_inverse, GradedObject.Monoidal.braiding_naturality_right, Iso.inv_hom_id_eval_assoc, GradedObject.single_map_singleObjApplyIso_hom, GradedObject.comapEq_trans, Iso.hom_inv_id_eval, GradedObject.instFaithfulTotal, GradedObject.mapIso_hom, GradedObject.eqToHom_proj, Iso.map_hom_inv_id_eval_app_assoc, GradedObject.Monoidal.hexagon_forward, HomologicalComplex.gradedHomologyFunctor_obj, GradedObject.mapTrifunctorObj_obj_map, GradedObject.mapBifunctorRightUnitorCofan_inj_assoc, GradedObject.mapBifunctorLeftUnitor_hasMap, Iso.map_inv_hom_id_eval, GradedObject.Monoidal.pentagon_inv_assoc, GradedObject.Monoidal.tensorIso_inv, Iso.map_inv_hom_id_eval_app, GradedObject.eval_obj, Iso.map_hom_inv_id_eval, GradedObject.mapTrifunctorObj_map_app, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX, HomologicalComplex₂.toGradedObjectFunctor_map, GradedObject.Monoidal.rightUnitor_naturality, GradedObject.Monoidal.leftUnitor_naturality, GradedObject.mapTrifunctor_obj, GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1, GradedObject.comapEq_inv_app, GradedObject.mapBifunctor_obj_map, GradedObject.mapBifunctorLeftUnitorCofan_inj_assoc, Functor.mapBifunctorHomologicalComplex_obj_map_f_f, GradedObject.Monoidal.triangle, Functor.mapBifunctorHomologicalComplexObj_obj_d_f, GradedObject.categoryOfGradedObjects_comp, Iso.map_inv_hom_id_eval_assoc, GradedObject.Monoidal.leftUnitor_naturality_assoc, GradedObject.single_map_singleObjApplyIso_hom_assoc, GradedObject.Monoidal.tensorIso_hom, GradedObject.comapEquiv_functor, GradedObject.Monoidal.ιTensorObj₃'_associator_hom_assoc, GradedObject.mapTrifunctorMapNatTrans_app_app_app, Iso.map_hom_inv_id_eval_app, GradedObject.comapEq_symm, HomologicalComplex₂.total.forget_map, Iso.map_inv_hom_id_eval_app_assoc, Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject, Iso.inv_hom_id_eval, HomologicalComplex.forgetEval_inv_app, HomologicalComplex₂.instFaithfulGradedObjectProdToGradedObjectFunctor, Functor.mapBifunctorHomologicalComplex_obj_obj_d_f, GradedObject.mapTrifunctorMapIso_inv
GradedObjectWithShift 📖	CompOp	23 math math: DifferentialObject.d_squared_apply, GradedObject.shiftFunctor_map_apply, HomologicalComplex.dgoToHomologicalComplex_obj_d, HomologicalComplex.dgoEquivHomologicalComplex_unitIso, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f, HomologicalComplex.dgoEquivHomologicalComplex_functor, HomologicalComplex.dgoToHomologicalComplex_obj_X, HomologicalComplex.dgoEquivHomologicalComplex_counitIso, HomologicalComplex.homologicalComplexToDGO_map_f, DifferentialObject.objEqToHom_d, DifferentialObject.eqToHom_f', DifferentialObject.objEqToHom_refl, HomologicalComplex.dgoToHomologicalComplex_map_f, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f, DifferentialObject.eqToHom_f'_assoc, HomologicalComplex.homologicalComplexToDGO_obj_d, HomologicalComplex.homologicalComplexToDGO_obj_obj, HomologicalComplex.dgoEquivHomologicalComplex_inverse, DifferentialObject.objEqToHom_d_assoc, DifferentialObject.d_squared_apply_assoc, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f, GradedObject.shiftFunctor_obj_apply
inhabitedGradedObject 📖	CompOp	—

CategoryTheory.GradedObject

Definitions

Name	Category	Theorems
CofanMapObjFun 📖	CompOp	—
HasMap 📖	MathDef	8 math math: Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ, mapBifunctorRightUnitor_hasMap, mapBifunctorLeftUnitor_hasMap, CofanMapObjFun.hasMap, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX, Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1
categoryOfGradedObjects 📖	CompOp	138 math math: isoMk_hom, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f, Monoidal.associator_naturality, singleObjApplyIso_inv_single_map, CategoryTheory.DifferentialObject.d_squared_apply, shiftFunctor_map_apply, Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit, mapBifunctorObjObjSingle₀Iso_hom, mapTrifunctor_map_app_app, comapEquiv_counitIso, zero_apply, Monoidal.pentagon, mapMap_comp_assoc, mapIso_inv, HomologicalComplex.instFaithfulGradedObjectForget, Monoidal.rightUnitor_naturality_assoc, HomologicalComplex₂.toGradedObjectFunctor_obj, HomologicalComplex.forget_map, Monoidal.symmetry, mapTrifunctorObj_obj_obj, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ, mapBifunctor_obj_obj, HomologicalComplex.forgetEval_hom_app, Monoidal.rightUnitor_inv_apply, Monoidal.leftUnitor_inv_apply, HomologicalComplex.dgoToHomologicalComplex_obj_d, isoMk_inv, HomologicalComplex.dgoEquivHomologicalComplex_unitIso, CategoryTheory.Iso.hom_inv_id_eval_assoc, Monoidal.ιTensorObj₃_associator_inv, singleCompEval_hom_app, singleCompEval_inv_app, HomologicalComplex.gradedHomologyFunctor_map, Monoidal.tensorHom_comp_tensorHom, mapBifunctorRightUnitorCofan_inj, singleObjApplyIsoOfEq_inv_single_map, Monoidal.symmetry_assoc, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f, mapTrifunctorMapIso_hom, categoryOfGradedObjects_id, Monoidal.tensorHom_comp_tensorHom_assoc, HomologicalComplex.dgoEquivHomologicalComplex_functor, Monoidal.pentagon_inv, mapBifunctorLeftUnitorCofan_inj, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ, Monoidal.ιTensorObj₃_associator_inv_assoc, mapBifunctorObjSingle₀ObjIso_hom, HomologicalComplex.dgoToHomologicalComplex_obj_X, mapMap_comp, comapEquiv_unitIso, singleObjApplyIso_inv_single_map_assoc, eval_map, Monoidal.tensorHom_def, mapBifunctorObjSingle₀ObjIso_inv, isIso_of_isIso_apply, Monoidal.hexagon_reverse, mapBifunctorRightUnitor_hasMap, Monoidal.id_tensorHom_id, map_obj, map_map, HomologicalComplex.dgoEquivHomologicalComplex_counitIso, hasZeroObject, HomologicalComplex.forget_obj, mapMap_id, HomologicalComplex.homologicalComplexToDGO_map_f, mapBifunctor_map_app, mapBifunctorObjObjSingle₀Iso_inv, CategoryTheory.Iso.map_hom_inv_id_eval_assoc, Monoidal.braiding_naturality_left, Monoidal.ιTensorObj₃'_associator_hom, CategoryTheory.DifferentialObject.objEqToHom_d, CategoryTheory.DifferentialObject.eqToHom_f', single_map_singleObjApplyIsoOfEq_hom, comapEq_hom_app, comapEquiv_inverse, CategoryTheory.DifferentialObject.objEqToHom_refl, HomologicalComplex.dgoToHomologicalComplex_map_f, Monoidal.braiding_naturality_right, CategoryTheory.Iso.inv_hom_id_eval_assoc, single_map_singleObjApplyIso_hom, comapEq_trans, CategoryTheory.Iso.hom_inv_id_eval, instFaithfulTotal, mapIso_hom, eqToHom_proj, CategoryTheory.Iso.map_hom_inv_id_eval_app_assoc, Monoidal.hexagon_forward, HomologicalComplex.gradedHomologyFunctor_obj, mapTrifunctorObj_obj_map, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f, mapBifunctorRightUnitorCofan_inj_assoc, mapBifunctorLeftUnitor_hasMap, CategoryTheory.Iso.map_inv_hom_id_eval, Monoidal.pentagon_inv_assoc, Monoidal.tensorIso_inv, CategoryTheory.Iso.map_inv_hom_id_eval_app, CategoryTheory.DifferentialObject.eqToHom_f'_assoc, eval_obj, CategoryTheory.Iso.map_hom_inv_id_eval, HomologicalComplex.homologicalComplexToDGO_obj_d, mapTrifunctorObj_map_app, HomologicalComplex.homologicalComplexToDGO_obj_obj, HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX, HomologicalComplex₂.toGradedObjectFunctor_map, Monoidal.rightUnitor_naturality, Monoidal.leftUnitor_naturality, mapTrifunctor_obj, Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1, HomologicalComplex.dgoEquivHomologicalComplex_inverse, comapEq_inv_app, mapBifunctor_obj_map, CategoryTheory.DifferentialObject.objEqToHom_d_assoc, CategoryTheory.DifferentialObject.d_squared_apply_assoc, mapBifunctorLeftUnitorCofan_inj_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f, Monoidal.triangle, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f, categoryOfGradedObjects_comp, CategoryTheory.Iso.map_inv_hom_id_eval_assoc, Monoidal.leftUnitor_naturality_assoc, single_map_singleObjApplyIso_hom_assoc, Monoidal.tensorIso_hom, comapEquiv_functor, Monoidal.ιTensorObj₃'_associator_hom_assoc, mapTrifunctorMapNatTrans_app_app_app, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f, CategoryTheory.Iso.map_hom_inv_id_eval_app, shiftFunctor_obj_apply, comapEq_symm, HomologicalComplex₂.total.forget_map, CategoryTheory.Iso.map_inv_hom_id_eval_app_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject, CategoryTheory.Iso.inv_hom_id_eval, HomologicalComplex.forgetEval_inv_app, HomologicalComplex₂.instFaithfulGradedObjectProdToGradedObjectFunctor, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f, mapTrifunctorMapIso_inv
cofanMapObj 📖	CompOp	—
cofanMapObjComp 📖	CompOp	—
comap 📖	CompOp	7 math math: comapEquiv_unitIso, comapEq_hom_app, comapEquiv_inverse, comapEq_trans, comapEq_inv_app, comapEquiv_functor, comapEq_symm
comapEq 📖	CompOp	6 math math: comapEquiv_counitIso, comapEquiv_unitIso, comapEq_hom_app, comapEq_trans, comapEq_inv_app, comapEq_symm
comapEquiv 📖	CompOp	4 math math: comapEquiv_counitIso, comapEquiv_unitIso, comapEquiv_inverse, comapEquiv_functor
descMapObj 📖	CompOp	2 math math: ι_descMapObj, ι_descMapObj_assoc
eval 📖	CompOp	6 math math: HomologicalComplex.forgetEval_hom_app, singleCompEval_hom_app, singleCompEval_inv_app, eval_map, eval_obj, HomologicalComplex.forgetEval_inv_app
hasShift 📖	CompOp	23 math math: CategoryTheory.DifferentialObject.d_squared_apply, shiftFunctor_map_apply, HomologicalComplex.dgoToHomologicalComplex_obj_d, HomologicalComplex.dgoEquivHomologicalComplex_unitIso, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f, HomologicalComplex.dgoEquivHomologicalComplex_functor, HomologicalComplex.dgoToHomologicalComplex_obj_X, HomologicalComplex.dgoEquivHomologicalComplex_counitIso, HomologicalComplex.homologicalComplexToDGO_map_f, CategoryTheory.DifferentialObject.objEqToHom_d, CategoryTheory.DifferentialObject.eqToHom_f', CategoryTheory.DifferentialObject.objEqToHom_refl, HomologicalComplex.dgoToHomologicalComplex_map_f, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f, CategoryTheory.DifferentialObject.eqToHom_f'_assoc, HomologicalComplex.homologicalComplexToDGO_obj_d, HomologicalComplex.homologicalComplexToDGO_obj_obj, HomologicalComplex.dgoEquivHomologicalComplex_inverse, CategoryTheory.DifferentialObject.objEqToHom_d_assoc, CategoryTheory.DifferentialObject.d_squared_apply_assoc, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f, shiftFunctor_obj_apply
hasZeroMorphisms 📖	CompOp	21 math math: CategoryTheory.DifferentialObject.d_squared_apply, HomologicalComplex.dgoToHomologicalComplex_obj_d, HomologicalComplex.dgoEquivHomologicalComplex_unitIso, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f, HomologicalComplex.dgoEquivHomologicalComplex_functor, HomologicalComplex.dgoToHomologicalComplex_obj_X, HomologicalComplex.dgoEquivHomologicalComplex_counitIso, HomologicalComplex.homologicalComplexToDGO_map_f, CategoryTheory.DifferentialObject.objEqToHom_d, CategoryTheory.DifferentialObject.eqToHom_f', CategoryTheory.DifferentialObject.objEqToHom_refl, HomologicalComplex.dgoToHomologicalComplex_map_f, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f, CategoryTheory.DifferentialObject.eqToHom_f'_assoc, HomologicalComplex.homologicalComplexToDGO_obj_d, HomologicalComplex.homologicalComplexToDGO_obj_obj, HomologicalComplex.dgoEquivHomologicalComplex_inverse, CategoryTheory.DifferentialObject.objEqToHom_d_assoc, CategoryTheory.DifferentialObject.d_squared_apply_assoc, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f
instZeroHomOfHasZeroMorphisms 📖	CompOp	1 math math: zero_apply
isColimitCofanMapObj 📖	CompOp	—
isColimitCofanMapObjComp 📖	CompOp	—
isoMk 📖	CompOp	2 math math: isoMk_hom, isoMk_inv
map 📖	CompOp	2 math math: map_obj, map_map
mapIso 📖	CompOp	2 math math: mapIso_inv, mapIso_hom
mapMap 📖	CompOp	20 math math: HomologicalComplex₂.total.mapAux.mapMap_D₁_assoc, mapMap_comp_assoc, congr_mapMap, mapIso_inv, ιMapObjOrZero_mapMap, HomologicalComplex₂.total.mapAux.d₁_mapMap, ιMapObjOrZero_mapMap_assoc, mapMap_comp, HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc, map_map, HomologicalComplex₂.total.mapAux.mapMap_D₁, HomologicalComplex₂.total.mapAux.mapMap_D₂, HomologicalComplex₂.total.mapAux.mapMap_D₂_assoc, mapMap_id, mapIso_hom, HomologicalComplex₂.total.mapAux.d₂_mapMap, ι_mapMap_assoc, HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc, ι_mapMap, HomologicalComplex₂.total.forget_map
mapObj 📖	CompOp	70 math math: HomologicalComplex₂.totalAux.ιMapObj_D₁, HomologicalComplex₂.totalFlipIso_hom_f_D₁, HomologicalComplex₂.totalAux.d₂_eq, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, HomologicalComplex₂.d₁_eq_zero', HomologicalComplex₂.D₁_D₁_assoc, HomologicalComplex₂.total.mapAux.mapMap_D₁_assoc, HomologicalComplex₂.D₁_D₁, HomologicalComplex₂.D₂_D₁_assoc, mapMap_comp_assoc, mapIso_inv, HomologicalComplex₂.D₂_D₂, HomologicalComplex₂.ι_D₁_assoc, CofanMapObjFun.inj_iso_hom, HomologicalComplex₂.d₂_eq_zero, ιMapObjOrZero_mapMap, HomologicalComplex₂.ι_D₂, mapObj_ext_iff, HomologicalComplex₂.total.mapAux.d₁_mapMap, ιMapObjOrZero_mapMap_assoc, HomologicalComplex₂.totalAux.ιMapObj_D₂_assoc, HomologicalComplex₂.D₁_shape, HomologicalComplex₂.totalFlipIsoX_hom_D₂_assoc, HomologicalComplex₂.ι_D₂_assoc, mapMap_comp, HomologicalComplex₂.totalAux.d₂_eq', HomologicalComplex₂.totalAux.d₁_eq, HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc, HomologicalComplex₂.d₁_eq_zero, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, CofanMapObjFun.ιMapObj_iso_inv, map_obj, HomologicalComplex₂.total.mapAux.mapMap_D₁, HomologicalComplex₂.d₂_eq_zero', HomologicalComplex₂.total.mapAux.mapMap_D₂, HomologicalComplex₂.totalAux.ιMapObj_D₂, HomologicalComplex₂.D₂_shape, HomologicalComplex₂.total.mapAux.mapMap_D₂_assoc, HomologicalComplex₂.totalFlipIso_hom_f_D₂, mapMap_id, CofanMapObjFun.inj_iso_hom_assoc, HomologicalComplex₂.D₁_totalShift₁XIso_hom, HomologicalComplex₂.D₂_totalShift₁XIso_hom, HomologicalComplex₂.totalFlipIso_hom_f_D₁_assoc, HomologicalComplex₂.totalFlipIsoX_hom_D₁, HomologicalComplex₂.D₂_D₂_assoc, mapIso_hom, HomologicalComplex₂.D₂_D₁, CofanMapObjFun.ιMapObj_iso_inv_assoc, HomologicalComplex₂.D₁_D₂_assoc, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, HomologicalComplex₂.total.mapAux.d₂_mapMap, HomologicalComplex₂.ι_D₁, ι_descMapObj, ι_descMapObj_assoc, ι_mapMap_assoc, HomologicalComplex₂.total_d, HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc, HomologicalComplex₂.totalFlipIsoX_hom_D₂, HomologicalComplex₂.D₁_totalShift₂XIso_hom, ι_mapMap, HomologicalComplex₂.D₂_totalShift₂XIso_hom, HomologicalComplex₂.totalAux.ιMapObj_D₁_assoc, HomologicalComplex₂.totalAux.d₁_eq', HomologicalComplex₂.D₁_D₂, ιMapObjOrZero_eq_zero, HomologicalComplex₂.totalFlipIsoX_hom_D₁_assoc, HomologicalComplex₂.totalFlipIso_hom_f_D₂_assoc
mapObjFun 📖	CompOp	8 math math: CofanMapObjFun.inj_iso_hom, mapBifunctorRightUnitorCofan_inj, mapBifunctorLeftUnitorCofan_inj, CofanMapObjFun.ιMapObj_iso_inv, CofanMapObjFun.inj_iso_hom_assoc, CofanMapObjFun.ιMapObj_iso_inv_assoc, mapBifunctorRightUnitorCofan_inj_assoc, mapBifunctorLeftUnitorCofan_inj_assoc
total 📖	CompOp	1 math math: instFaithfulTotal
ιMapObj 📖	CompOp	16 math math: HomologicalComplex₂.totalAux.ιMapObj_D₁, ιMapObjOrZero_eq, HomologicalComplex₂.totalAux.d₂_eq, CofanMapObjFun.inj_iso_hom, mapObj_ext_iff, HomologicalComplex₂.totalAux.ιMapObj_D₂_assoc, HomologicalComplex₂.totalAux.d₁_eq, CofanMapObjFun.ιMapObj_iso_inv, HomologicalComplex₂.totalAux.ιMapObj_D₂, CofanMapObjFun.inj_iso_hom_assoc, CofanMapObjFun.ιMapObj_iso_inv_assoc, ι_descMapObj, ι_descMapObj_assoc, ι_mapMap_assoc, ι_mapMap, HomologicalComplex₂.totalAux.ιMapObj_D₁_assoc
ιMapObjOrZero 📖	CompOp	6 math math: ιMapObjOrZero_eq, ιMapObjOrZero_mapMap, ιMapObjOrZero_mapMap_assoc, HomologicalComplex₂.totalAux.d₂_eq', HomologicalComplex₂.totalAux.d₁_eq', ιMapObjOrZero_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
categoryOfGradedObjects_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct categoryOfGradedObjects	—	—
categoryOfGradedObjects_id 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct categoryOfGradedObjects	—	—
comapEq_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.GradedObject categoryOfGradedObjects comap CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category comapEq CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
comapEq_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.GradedObject categoryOfGradedObjects comap CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category comapEq CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
comapEq_symm 📖	mathematical	—	comapEq CategoryTheory.Iso.symm CategoryTheory.Functor CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor.category comap	—	—
comapEq_trans 📖	mathematical	—	comapEq CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor.category comap	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' hom_ext CategoryTheory.Category.comp_id
comapEquiv_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.GradedObject categoryOfGradedObjects comapEquiv CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.pi DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Pi.instCategoryComp CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Pi.comap CategoryTheory.Functor.id CategoryTheory.Pi.comapComp comapEq	—	—
comapEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.GradedObject categoryOfGradedObjects comapEquiv comap DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	—
comapEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.GradedObject categoryOfGradedObjects comapEquiv comap DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	—
comapEquiv_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.GradedObject categoryOfGradedObjects comapEquiv CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category comap DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Functor.comp comapEq CategoryTheory.Iso.symm CategoryTheory.pi CategoryTheory.Pi.instCategoryComp CategoryTheory.Pi.comap CategoryTheory.Pi.comapComp	—	—
congr_mapMap 📖	mathematical	HasMap	mapMap	—	—
eqToHom_apply 📖	mathematical	—	CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.pi	—	—
eqToHom_proj 📖	mathematical	—	CategoryTheory.eqToHom CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct categoryOfGradedObjects	—	—
eval_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.GradedObject categoryOfGradedObjects eval	—	—
eval_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects eval	—	—
hasMap_comp 📖	—	HasMap mapObj	—	—	—
hasMap_of_iso 📖	—	HasMap	—	—	CategoryTheory.Limits.hasColimit_of_iso
hasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject CategoryTheory.GradedObject categoryOfGradedObjects	—	hom_ext CategoryTheory.Limits.HasZeroObject.from_zero_ext CategoryTheory.Limits.HasZeroObject.to_zero_ext
hom_ext 📖	—	—	—	—	—
hom_ext_iff 📖	—	—	—	—	hom_ext
instFaithfulTotal 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.Functor.Faithful CategoryTheory.GradedObject categoryOfGradedObjects total	—	hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.whisker_eq CategoryTheory.Limits.colimit.ι_map CategoryTheory.Mono.right_cancellation CategoryTheory.IsSplitMono.mono CategoryTheory.Limits.isSplitMono_sigma_ι
isIso_apply_of_isIso 📖	mathematical	—	CategoryTheory.IsIso	—	CategoryTheory.Functor.map_isIso
isIso_of_isIso_apply 📖	mathematical	CategoryTheory.IsIso	CategoryTheory.GradedObject categoryOfGradedObjects	—	CategoryTheory.Iso.isIso_hom
isoMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.GradedObject categoryOfGradedObjects isoMk	—	—
isoMk_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.GradedObject categoryOfGradedObjects isoMk	—	—
mapIso_hom 📖	mathematical	HasMap	CategoryTheory.Iso.hom CategoryTheory.GradedObject categoryOfGradedObjects mapObj mapIso mapMap	—	—
mapIso_inv 📖	mathematical	HasMap	CategoryTheory.Iso.inv CategoryTheory.GradedObject categoryOfGradedObjects mapObj mapIso mapMap	—	—
mapMap_comp 📖	mathematical	HasMap	mapMap CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct categoryOfGradedObjects mapObj	—	hom_ext mapObj_ext ι_mapMap CategoryTheory.Category.assoc ι_mapMap_assoc
mapMap_comp_assoc 📖	mathematical	HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct categoryOfGradedObjects mapObj mapMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapMap_comp
mapMap_id 📖	mathematical	HasMap	mapMap CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject CategoryTheory.Category.toCategoryStruct categoryOfGradedObjects mapObj	—	hom_ext mapObj_ext ι_mapMap CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
mapObj_ext 📖	—	HasMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapObj ιMapObj	—	—	CategoryTheory.Limits.Cofan.IsColimit.hom_ext
mapObj_ext_iff 📖	mathematical	HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapObj ιMapObj	—	mapObj_ext
map_map 📖	mathematical	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Discrete Set.Elem Set.preimage Set Set.instSingletonSet CategoryTheory.discreteCategory	CategoryTheory.Functor.map CategoryTheory.GradedObject categoryOfGradedObjects map mapMap	—	—
map_obj 📖	mathematical	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Discrete Set.Elem Set.preimage Set Set.instSingletonSet CategoryTheory.discreteCategory	CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects map mapObj	—	—
shiftFunctor_map_apply 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.GradedObjectWithShift categoryOfGradedObjects CategoryTheory.shiftFunctor Int.instAddMonoid hasShift AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
shiftFunctor_obj_apply 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.GradedObjectWithShift categoryOfGradedObjects CategoryTheory.shiftFunctor Int.instAddMonoid hasShift AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
zero_apply 📖	mathematical	—	Quiver.Hom CategoryTheory.GradedObject CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct categoryOfGradedObjects instZeroHomOfHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
ιMapObjOrZero_eq 📖	mathematical	HasMap	ιMapObjOrZero ιMapObj	—	—
ιMapObjOrZero_eq_zero 📖	mathematical	HasMap	ιMapObjOrZero Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mapObj CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
ιMapObjOrZero_mapMap 📖	mathematical	HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapObj ιMapObjOrZero mapMap	—	ιMapObjOrZero_eq ι_mapMap ιMapObjOrZero_eq_zero CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
ιMapObjOrZero_mapMap_assoc 📖	mathematical	HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapObj ιMapObjOrZero mapMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιMapObjOrZero_mapMap
ι_descMapObj 📖	mathematical	HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapObj ιMapObj descMapObj	—	CategoryTheory.Limits.Cofan.IsColimit.fac
ι_descMapObj_assoc 📖	mathematical	HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapObj ιMapObj descMapObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_descMapObj
ι_mapMap 📖	mathematical	HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapObj ιMapObj mapMap	—	ι_descMapObj
ι_mapMap_assoc 📖	mathematical	HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapObj ιMapObj mapMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapMap

CategoryTheory.GradedObject.CofanMapObjFun

Definitions

Name	Category	Theorems
iso 📖	CompOp	4 math math: inj_iso_hom, ιMapObj_iso_inv, inj_iso_hom_assoc, ιMapObj_iso_inv_assoc
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasMap 📖	mathematical	—	CategoryTheory.GradedObject.HasMap	—	—
inj_iso_hom 📖	mathematical	CategoryTheory.GradedObject.HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObjFun Set Set.instMembership Set.preimage Set.instSingletonSet CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete Set.Elem CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.GradedObject.mapObj CategoryTheory.Iso.hom iso CategoryTheory.GradedObject.ιMapObj	—	CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
inj_iso_hom_assoc 📖	mathematical	CategoryTheory.GradedObject.HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObjFun Set Set.instMembership Set.preimage Set.instSingletonSet CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete Set.Elem CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.GradedObject.mapObj CategoryTheory.Iso.hom iso CategoryTheory.GradedObject.ιMapObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inj_iso_hom
ιMapObj_iso_inv 📖	mathematical	CategoryTheory.GradedObject.HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete Set.Elem Set.preimage Set Set.instSingletonSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.GradedObject.mapObjFun CategoryTheory.GradedObject.ιMapObj CategoryTheory.Iso.inv iso Set.instMembership	—	CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv
ιMapObj_iso_inv_assoc 📖	mathematical	CategoryTheory.GradedObject.HasMap	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj CategoryTheory.GradedObject.ιMapObj CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete Set.Elem Set.preimage Set Set.instSingletonSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.GradedObject.mapObjFun CategoryTheory.Iso.inv iso Set.instMembership	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιMapObj_iso_inv

CategoryTheory.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_inv_id_eval 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hom CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.GradedObject.categoryOfGradedObjects_comp hom_inv_id CategoryTheory.GradedObject.categoryOfGradedObjects_id
hom_inv_id_eval_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hom CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_id_eval
inv_hom_id_eval 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.GradedObject.categoryOfGradedObjects_comp inv_hom_id CategoryTheory.GradedObject.categoryOfGradedObjects_id
inv_hom_id_eval_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_id_eval
map_hom_inv_id_eval 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map hom CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.map_comp CategoryTheory.GradedObject.categoryOfGradedObjects_comp hom_inv_id CategoryTheory.GradedObject.categoryOfGradedObjects_id CategoryTheory.Functor.map_id
map_hom_inv_id_eval_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app CategoryTheory.Functor.map hom CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.comp_app CategoryTheory.Functor.map_comp hom_inv_id_eval CategoryTheory.Functor.map_id CategoryTheory.NatTrans.id_app
map_hom_inv_id_eval_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app CategoryTheory.Functor.map hom CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' map_hom_inv_id_eval_app
map_hom_inv_id_eval_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map hom CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' map_hom_inv_id_eval
map_inv_hom_id_eval 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.map_comp CategoryTheory.GradedObject.categoryOfGradedObjects_comp inv_hom_id CategoryTheory.GradedObject.categoryOfGradedObjects_id CategoryTheory.Functor.map_id
map_inv_hom_id_eval_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app CategoryTheory.Functor.map inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.comp_app CategoryTheory.Functor.map_comp inv_hom_id_eval CategoryTheory.Functor.map_id CategoryTheory.NatTrans.id_app
map_inv_hom_id_eval_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.NatTrans.app CategoryTheory.Functor.map inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' map_inv_hom_id_eval_app
map_inv_hom_id_eval_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map inv CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' map_inv_hom_id_eval

---

← Back to Index