Unitor

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

Statistics

Metric	Count
Definitions TriangleIndexData, p₁₂, p₂₃, ρ₁₂, ρ₂₃, mapBifunctorLeftUnitor, mapBifunctorLeftUnitorCofan, mapBifunctorLeftUnitorCofanIsColimit, mapBifunctorObjObjSingle₀IsInitial, mapBifunctorObjObjSingle₀Iso, mapBifunctorObjSingle₀ObjIsInitial, mapBifunctorObjSingle₀ObjIso, mapBifunctorRightUnitor, mapBifunctorRightUnitorCofan, mapBifunctorRightUnitorCofanIsColimit	15
Theorems hp₁₂, hp₂₃, h₁, h₃, r_zero, mapBifunctorLeftUnitorCofan_inj, mapBifunctorLeftUnitorCofan_inj_assoc, mapBifunctorLeftUnitor_hasMap, mapBifunctorLeftUnitor_inv_apply, mapBifunctorLeftUnitor_inv_naturality, mapBifunctorLeftUnitor_inv_naturality_assoc, mapBifunctorLeftUnitor_naturality, mapBifunctorLeftUnitor_naturality_assoc, mapBifunctorObjObjSingle₀Iso_hom, mapBifunctorObjObjSingle₀Iso_inv, mapBifunctorObjSingle₀ObjIso_hom, mapBifunctorObjSingle₀ObjIso_inv, mapBifunctorRightUnitorCofan_inj, mapBifunctorRightUnitorCofan_inj_assoc, mapBifunctorRightUnitor_hasMap, mapBifunctorRightUnitor_inv_apply, mapBifunctorRightUnitor_inv_naturality, mapBifunctorRightUnitor_inv_naturality_assoc, mapBifunctorRightUnitor_naturality, mapBifunctorRightUnitor_naturality_assoc, mapBifunctor_triangle, ι_mapBifunctorLeftUnitor_hom_apply, ι_mapBifunctorLeftUnitor_hom_apply_assoc, ι_mapBifunctorRightUnitor_hom_apply, ι_mapBifunctorRightUnitor_hom_apply_assoc	30
Total	45

CategoryTheory.GradedObject

Definitions

Name	Category	Theorems
TriangleIndexData 📖	CompData	—
mapBifunctorLeftUnitor 📖	CompOp	8 math math: mapBifunctor_triangle, mapBifunctorLeftUnitor_inv_naturality_assoc, mapBifunctorLeftUnitor_inv_apply, mapBifunctorLeftUnitor_naturality, ι_mapBifunctorLeftUnitor_hom_apply, mapBifunctorLeftUnitor_naturality_assoc, mapBifunctorLeftUnitor_inv_naturality, ι_mapBifunctorLeftUnitor_hom_apply_assoc
mapBifunctorLeftUnitorCofan 📖	CompOp	2 math math: mapBifunctorLeftUnitorCofan_inj, mapBifunctorLeftUnitorCofan_inj_assoc
mapBifunctorLeftUnitorCofanIsColimit 📖	CompOp	—
mapBifunctorObjObjSingle₀IsInitial 📖	CompOp	—
mapBifunctorObjObjSingle₀Iso 📖	CompOp	2 math math: mapBifunctorObjObjSingle₀Iso_hom, mapBifunctorObjObjSingle₀Iso_inv
mapBifunctorObjSingle₀ObjIsInitial 📖	CompOp	—
mapBifunctorObjSingle₀ObjIso 📖	CompOp	2 math math: mapBifunctorObjSingle₀ObjIso_hom, mapBifunctorObjSingle₀ObjIso_inv
mapBifunctorRightUnitor 📖	CompOp	8 math math: mapBifunctor_triangle, ι_mapBifunctorRightUnitor_hom_apply, mapBifunctorRightUnitor_inv_naturality_assoc, mapBifunctorRightUnitor_inv_apply, mapBifunctorRightUnitor_naturality, mapBifunctorRightUnitor_naturality_assoc, ι_mapBifunctorRightUnitor_hom_apply_assoc, mapBifunctorRightUnitor_inv_naturality
mapBifunctorRightUnitorCofan 📖	CompOp	2 math math: mapBifunctorRightUnitorCofan_inj, mapBifunctorRightUnitorCofan_inj_assoc
mapBifunctorRightUnitorCofanIsColimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapBifunctorLeftUnitorCofan_inj 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip	Set.Elem Set.preimage Set Set.instSingletonSet mapObjFun CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀ mapBifunctorLeftUnitorCofan Set.instMembership CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct single CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjApplyIso	—	CategoryTheory.Category.comp_id
mapBifunctorLeftUnitorCofan_inj_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapObjFun CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀ Set Set.instMembership Set.preimage Set.instSingletonSet CategoryTheory.Limits.Cocone.pt Set.Elem CategoryTheory.Discrete.functor mapBifunctorLeftUnitorCofan CategoryTheory.NatTrans.app single CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjApplyIso CategoryTheory.Functor.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
mapBifunctorLeftUnitor_hasMap 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip	HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	—	CofanMapObjFun.hasMap
mapBifunctorLeftUnitor_inv_apply 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.Iso.inv mapBifunctorMapObj mapBifunctorLeftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.NatTrans.app single CategoryTheory.Functor.map singleObjApplyIso ιMapBifunctorMapObj	—	—
mapBifunctorLeftUnitor_inv_naturality 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj CategoryTheory.Iso.inv mapBifunctorLeftUnitor mapBifunctorMapMap CategoryTheory.CategoryStruct.id	—	hom_ext mapBifunctorLeftUnitor_inv_apply CategoryTheory.Category.assoc ι_mapBifunctorMapMap CategoryTheory.Functor.map_id CategoryTheory.NatTrans.id_app CategoryTheory.Category.id_comp CategoryTheory.NatTrans.naturality_assoc
mapBifunctorLeftUnitor_inv_naturality_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj CategoryTheory.Iso.inv mapBifunctorLeftUnitor mapBifunctorMapMap CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapBifunctorLeftUnitor_inv_naturality
mapBifunctorLeftUnitor_naturality 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj mapBifunctorMapMap CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom mapBifunctorLeftUnitor	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id mapBifunctorLeftUnitor_inv_naturality CategoryTheory.Iso.hom_inv_id_assoc
mapBifunctorLeftUnitor_naturality_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj mapBifunctorMapMap CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom mapBifunctorLeftUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapBifunctorLeftUnitor_naturality
mapBifunctorObjObjSingle₀Iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor single₀ mapBifunctorObjObjSingle₀Iso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map singleObjApplyIsoOfEq CategoryTheory.NatTrans.app CategoryTheory.Functor.flip CategoryTheory.Functor.id	—	—
mapBifunctorObjObjSingle₀Iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor single₀ mapBifunctorObjObjSingle₀Iso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.flip CategoryTheory.Functor.map singleObjApplyIsoOfEq	—	—
mapBifunctorObjSingle₀ObjIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor single₀ mapBifunctorObjSingle₀ObjIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app single CategoryTheory.Functor.map singleObjApplyIsoOfEq CategoryTheory.Functor.id	—	—
mapBifunctorObjSingle₀ObjIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor single₀ mapBifunctorObjSingle₀ObjIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor.id single CategoryTheory.Functor.map singleObjApplyIsoOfEq	—	—
mapBifunctorRightUnitorCofan_inj 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category	Set.Elem Set.preimage Set Set.instSingletonSet mapObjFun CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀ mapBifunctorRightUnitorCofan Set.instMembership CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct single CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjApplyIso CategoryTheory.NatTrans.app CategoryTheory.Functor.flip	—	CategoryTheory.Category.comp_id
mapBifunctorRightUnitorCofan_inj_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapObjFun CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀ Set Set.instMembership Set.preimage Set.instSingletonSet CategoryTheory.Limits.Cocone.pt Set.Elem CategoryTheory.Discrete.functor mapBifunctorRightUnitorCofan CategoryTheory.Functor.map single CategoryTheory.Iso.hom singleObjApplyIso CategoryTheory.NatTrans.app CategoryTheory.Functor.flip CategoryTheory.Functor.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
mapBifunctorRightUnitor_hasMap 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category	HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	—	CofanMapObjFun.hasMap
mapBifunctorRightUnitor_inv_apply 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.Iso.inv mapBifunctorMapObj mapBifunctorRightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.Functor.flip CategoryTheory.NatTrans.app single CategoryTheory.Functor.map singleObjApplyIso ιMapBifunctorMapObj	—	—
mapBifunctorRightUnitor_inv_naturality 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj CategoryTheory.Iso.inv mapBifunctorRightUnitor mapBifunctorMapMap CategoryTheory.CategoryStruct.id	—	hom_ext mapBifunctorRightUnitor_inv_apply CategoryTheory.Category.assoc ι_mapBifunctorMapMap CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.NatTrans.naturality_assoc
mapBifunctorRightUnitor_inv_naturality_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj CategoryTheory.Iso.inv mapBifunctorRightUnitor mapBifunctorMapMap CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapBifunctorRightUnitor_inv_naturality
mapBifunctorRightUnitor_naturality 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj mapBifunctorMapMap CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom mapBifunctorRightUnitor	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id mapBifunctorRightUnitor_inv_naturality CategoryTheory.Iso.hom_inv_id_assoc
mapBifunctorRightUnitor_naturality_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj mapBifunctorMapMap CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom mapBifunctorRightUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapBifunctorRightUnitor_naturality
mapBifunctor_triangle 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀ TriangleIndexData.p₁₂ mapBifunctorMapObj TriangleIndexData.p₂₃ HasGoodTrifunctor₁₂Obj TriangleIndexData.ρ₁₂ HasGoodTrifunctor₂₃Obj TriangleIndexData.ρ₂₃ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.bifunctorComp₁₂ CategoryTheory.bifunctorComp₂₃ CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor.map	BifunctorComp₁₂IndexData.I₁₂ BifunctorComp₁₂IndexData.q BifunctorComp₁₂IndexData.p BifunctorComp₂₃IndexData.I₂₃ BifunctorComp₂₃IndexData.q BifunctorComp₂₃IndexData.p mapBifunctorAssociator mapBifunctorMapMap CategoryTheory.CategoryStruct.id mapBifunctorLeftUnitor TriangleIndexData.h₃ mapBifunctorRightUnitor TriangleIndexData.h₁	—	TriangleIndexData.h₃ TriangleIndexData.h₁ CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso instIsIsoMapBifunctorMapMap CategoryTheory.Iso.isIso_inv CategoryTheory.IsIso.id hom_ext mapBifunctorMapObj_ext ι_mapBifunctorMapMap_assoc CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc ι_mapBifunctorMapMap TriangleIndexData.r_zero ιMapBifunctor₁₂BifunctorMapObj_eq_assoc ι_mapBifunctorAssociator_hom_assoc ιMapBifunctorBifunctor₂₃MapObj_eq_assoc CategoryTheory.NatTrans.id_app CategoryTheory.Functor.map_comp_assoc CategoryTheory.NatTrans.comp_app_assoc ι_mapBifunctorLeftUnitor_hom_apply ι_mapBifunctorRightUnitor_hom_apply CategoryTheory.NatTrans.naturality_app
ι_mapBifunctorLeftUnitor_hom_apply 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj ιMapBifunctorMapObj CategoryTheory.Iso.hom mapBifunctorLeftUnitor single CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.map singleObjApplyIso	—	CofanMapObjFun.ιMapObj_iso_inv
ι_mapBifunctorLeftUnitor_hom_apply_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj ιMapBifunctorMapObj CategoryTheory.Iso.hom mapBifunctorLeftUnitor CategoryTheory.NatTrans.app single CategoryTheory.Functor.map singleObjApplyIso CategoryTheory.Functor.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorLeftUnitor_hom_apply
ι_mapBifunctorRightUnitor_hom_apply 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj ιMapBifunctorMapObj CategoryTheory.Iso.hom mapBifunctorRightUnitor single CategoryTheory.Functor.id CategoryTheory.Functor.map singleObjApplyIso CategoryTheory.NatTrans.app CategoryTheory.Functor.flip	—	CofanMapObjFun.ιMapObj_iso_inv
ι_mapBifunctorRightUnitor_hom_apply_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.empty CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMap CategoryTheory.GradedObject categoryOfGradedObjects mapBifunctor single₀	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapBifunctorMapObj ιMapBifunctorMapObj CategoryTheory.Iso.hom mapBifunctorRightUnitor CategoryTheory.Functor.map single singleObjApplyIso CategoryTheory.NatTrans.app CategoryTheory.Functor.flip CategoryTheory.Functor.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorRightUnitor_hom_apply

CategoryTheory.GradedObject.TriangleIndexData

Definitions

Name	Category	Theorems
p₁₂ 📖	CompOp	2 math math: hp₁₂, h₁
p₂₃ 📖	CompOp	2 math math: h₃, hp₂₃
ρ₁₂ 📖	CompOp	—
ρ₂₃ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hp₁₂ 📖	mathematical	—	p₁₂	—	—
hp₂₃ 📖	mathematical	—	p₂₃	—	—
h₁ 📖	mathematical	—	p₁₂	—	—
h₃ 📖	mathematical	—	p₂₃	—	—
r_zero 📖	—	—	—	—	hp₂₃ h₃

---

← Back to Index