Single

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

Statistics

Metric	Count
Definitions isInitialSingleObjApply, single, singleCompEval, singleObjApplyIso, singleObjApplyIsoOfEq, single₀	6
Theorems singleCompEval_hom_app, singleCompEval_inv_app, singleObjApplyIsoOfEq_inv_single_map, singleObjApplyIso_inv_single_map, singleObjApplyIso_inv_single_map_assoc, single_map_singleObjApplyIsoOfEq_hom, single_map_singleObjApplyIso_hom, single_map_singleObjApplyIso_hom_assoc	8
Total	14

CategoryTheory.GradedObject

Definitions

Name	Category	Theorems
isInitialSingleObjApply 📖	CompOp	—
single 📖	CompOp	20 math math: singleObjApplyIso_inv_single_map, singleCompEval_hom_app, singleCompEval_inv_app, mapBifunctorRightUnitorCofan_inj, singleObjApplyIsoOfEq_inv_single_map, ι_mapBifunctorRightUnitor_hom_apply, mapBifunctorLeftUnitorCofan_inj, mapBifunctorObjSingle₀ObjIso_hom, singleObjApplyIso_inv_single_map_assoc, mapBifunctorObjSingle₀ObjIso_inv, mapBifunctorRightUnitor_inv_apply, mapBifunctorLeftUnitor_inv_apply, single_map_singleObjApplyIsoOfEq_hom, single_map_singleObjApplyIso_hom, ι_mapBifunctorLeftUnitor_hom_apply, mapBifunctorRightUnitorCofan_inj_assoc, mapBifunctorLeftUnitorCofan_inj_assoc, ι_mapBifunctorRightUnitor_hom_apply_assoc, single_map_singleObjApplyIso_hom_assoc, ι_mapBifunctorLeftUnitor_hom_apply_assoc
singleCompEval 📖	CompOp	2 math math: singleCompEval_hom_app, singleCompEval_inv_app
singleObjApplyIso 📖	CompOp	16 math math: singleObjApplyIso_inv_single_map, singleCompEval_hom_app, singleCompEval_inv_app, mapBifunctorRightUnitorCofan_inj, ι_mapBifunctorRightUnitor_hom_apply, mapBifunctorLeftUnitorCofan_inj, singleObjApplyIso_inv_single_map_assoc, mapBifunctorRightUnitor_inv_apply, mapBifunctorLeftUnitor_inv_apply, single_map_singleObjApplyIso_hom, ι_mapBifunctorLeftUnitor_hom_apply, mapBifunctorRightUnitorCofan_inj_assoc, mapBifunctorLeftUnitorCofan_inj_assoc, ι_mapBifunctorRightUnitor_hom_apply_assoc, single_map_singleObjApplyIso_hom_assoc, ι_mapBifunctorLeftUnitor_hom_apply_assoc
singleObjApplyIsoOfEq 📖	CompOp	6 math math: mapBifunctorObjObjSingle₀Iso_hom, singleObjApplyIsoOfEq_inv_single_map, mapBifunctorObjSingle₀ObjIso_hom, mapBifunctorObjSingle₀ObjIso_inv, mapBifunctorObjObjSingle₀Iso_inv, single_map_singleObjApplyIsoOfEq_hom
single₀ 📖	CompOp	27 math math: mapBifunctor_triangle, Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit, mapBifunctorObjObjSingle₀Iso_hom, mapBifunctorRightUnitorCofan_inj, ι_mapBifunctorRightUnitor_hom_apply, mapBifunctorLeftUnitorCofan_inj, mapBifunctorObjSingle₀ObjIso_hom, mapBifunctorObjSingle₀ObjIso_inv, mapBifunctorRightUnitor_inv_naturality_assoc, mapBifunctorRightUnitor_hasMap, mapBifunctorLeftUnitor_inv_naturality_assoc, mapBifunctorRightUnitor_inv_apply, mapBifunctorRightUnitor_naturality, mapBifunctorLeftUnitor_inv_apply, mapBifunctorObjObjSingle₀Iso_inv, mapBifunctorLeftUnitor_naturality, ι_mapBifunctorLeftUnitor_hom_apply, mapBifunctorRightUnitor_naturality_assoc, mapBifunctorRightUnitorCofan_inj_assoc, mapBifunctorLeftUnitor_hasMap, mapBifunctorLeftUnitor_naturality_assoc, Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1, mapBifunctorLeftUnitor_inv_naturality, mapBifunctorLeftUnitorCofan_inj_assoc, ι_mapBifunctorRightUnitor_hom_apply_assoc, ι_mapBifunctorLeftUnitor_hom_apply_assoc, mapBifunctorRightUnitor_inv_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
singleCompEval_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.GradedObject categoryOfGradedObjects single eval CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category singleCompEval CategoryTheory.Functor.obj singleObjApplyIso	—	—
singleCompEval_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.GradedObject categoryOfGradedObjects single eval CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category singleCompEval CategoryTheory.Functor.obj singleObjApplyIso	—	—
singleObjApplyIsoOfEq_inv_single_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects single CategoryTheory.Iso.inv singleObjApplyIsoOfEq CategoryTheory.Functor.map	—	CategoryTheory.eqToHom_trans_assoc CategoryTheory.Category.id_comp
singleObjApplyIso_inv_single_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects single CategoryTheory.Iso.inv singleObjApplyIso CategoryTheory.Functor.map	—	singleObjApplyIsoOfEq_inv_single_map
singleObjApplyIso_inv_single_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects single CategoryTheory.Iso.inv singleObjApplyIso CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjApplyIso_inv_single_map
single_map_singleObjApplyIsoOfEq_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects single CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjApplyIsoOfEq	—	CategoryTheory.Category.assoc CategoryTheory.eqToHom_trans CategoryTheory.Category.comp_id
single_map_singleObjApplyIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects single CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjApplyIso	—	single_map_singleObjApplyIsoOfEq_hom
single_map_singleObjApplyIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects single CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjApplyIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' single_map_singleObjApplyIso_hom

---

← Back to Index