FunctorCategory

📁 Source: Mathlib/CategoryTheory/Enriched/FunctorCategory.lean

Statistics

Metric	Count
Definitions HasEnrichedHom, HasFunctorEnrichedHom, coneFunctorEnrichedHom, diagram, enrichedComp, enrichedHom, enrichedHomπ, enrichedId, enrichedOrdinaryCategory, functorEnrichedCategory, functorEnrichedComp, functorEnrichedHom, functorEnrichedId, functorEnrichedOrdinaryCategory, functorHomEquiv, homEquiv, isLimitConeFunctorEnrichedHom, precompEnrichedHom, precompEnrichedHom'	19
Theorems coneFunctorEnrichedHom_pt, coneFunctorEnrichedHom_π_app, diagram_map_app, diagram_obj_map, diagram_obj_obj, enrichedComp_π, enrichedComp_π_assoc, enrichedHom_condition, enrichedHom_condition', enrichedHom_condition'_assoc, enrichedHom_condition_assoc, enrichedId_π, enrichedId_π_assoc, enriched_assoc, enriched_assoc_assoc, enriched_comp_id, enriched_comp_id_assoc, enriched_id_comp, enriched_id_comp_assoc, functorEnrichedComp_app, functorEnrichedHom_map, functorEnrichedHom_obj, functorEnrichedId_app, functorEnriched_assoc, functorEnriched_assoc_assoc, functorEnriched_comp_id, functorEnriched_comp_id_assoc, functorEnriched_id_comp, functorEnriched_id_comp_assoc, functorHomEquiv_apply_app, functorHomEquiv_comp, functorHomEquiv_id, homEquiv_apply_π, homEquiv_apply_π_assoc, homEquiv_comp, homEquiv_comp_assoc, homEquiv_id, instHasEnrichedHomUnderCompMapForget, fac	39
Total	58

CategoryTheory.Enriched.FunctorCategory

Definitions

Name	Category	Theorems
HasEnrichedHom 📖	MathDef	1 math math: instHasEnrichedHomUnderCompMapForget
HasFunctorEnrichedHom 📖	MathDef	—
coneFunctorEnrichedHom 📖	CompOp	3 math math: isLimitConeFunctorEnrichedHom.fac, coneFunctorEnrichedHom_π_app, coneFunctorEnrichedHom_pt
diagram 📖	CompOp	7 math math: enrichedId_π_assoc, diagram_map_app, enrichedComp_π_assoc, diagram_obj_map, enrichedComp_π, enrichedId_π, diagram_obj_obj
enrichedComp 📖	CompOp	11 math math: enriched_id_comp, enriched_id_comp_assoc, enriched_comp_id_assoc, homEquiv_comp, enrichedComp_π_assoc, functorEnrichedComp_app, enriched_assoc_assoc, enriched_assoc, homEquiv_comp_assoc, enrichedComp_π, enriched_comp_id
enrichedHom 📖	CompOp	24 math math: enriched_id_comp, enrichedHom_condition', enrichedHom_condition, isLimitConeFunctorEnrichedHom.fac, enrichedHom_condition_assoc, enrichedId_π_assoc, homEquiv_apply_π, enriched_id_comp_assoc, coneFunctorEnrichedHom_π_app, enriched_comp_id_assoc, homEquiv_comp, homEquiv_id, enrichedComp_π_assoc, functorEnrichedHom_obj, enriched_assoc_assoc, coneFunctorEnrichedHom_pt, enriched_assoc, homEquiv_apply_π_assoc, enrichedHom_condition'_assoc, homEquiv_comp_assoc, functorHomEquiv_apply_app, enrichedComp_π, enrichedId_π, enriched_comp_id
enrichedHomπ 📖	CompOp	6 math math: enrichedHom_condition', enrichedHom_condition, enrichedHom_condition_assoc, homEquiv_apply_π, homEquiv_apply_π_assoc, enrichedHom_condition'_assoc
enrichedId 📖	CompOp	8 math math: enriched_id_comp, enrichedId_π_assoc, enriched_id_comp_assoc, enriched_comp_id_assoc, homEquiv_id, enrichedId_π, functorEnrichedId_app, enriched_comp_id
enrichedOrdinaryCategory 📖	CompOp	—
functorEnrichedCategory 📖	CompOp	—
functorEnrichedComp 📖	CompOp	9 math math: functorHomEquiv_comp, functorEnriched_id_comp, functorEnrichedComp_app, functorEnriched_id_comp_assoc, functorEnriched_comp_id_assoc, functorEnriched_assoc_assoc, functorEnriched_assoc, functorEnriched_comp_id, CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_three
functorEnrichedHom 📖	CompOp	20 math math: functorHomEquiv_comp, isLimitConeFunctorEnrichedHom.fac, coneFunctorEnrichedHom_π_app, CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality, functorEnriched_id_comp, functorEnrichedComp_app, functorEnrichedHom_obj, CategoryTheory.Presheaf.isSheaf_functorEnrichedHom, coneFunctorEnrichedHom_pt, functorEnriched_id_comp_assoc, CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_two_symm, functorEnriched_comp_id_assoc, functorEnriched_assoc_assoc, functorHomEquiv_apply_app, functorHomEquiv_id, functorEnriched_assoc, functorEnrichedHom_map, functorEnriched_comp_id, CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_three, functorEnrichedId_app
functorEnrichedId 📖	CompOp	6 math math: functorEnriched_id_comp, functorEnriched_id_comp_assoc, functorEnriched_comp_id_assoc, functorHomEquiv_id, functorEnriched_comp_id, functorEnrichedId_app
functorEnrichedOrdinaryCategory 📖	CompOp	—
functorHomEquiv 📖	CompOp	4 math math: functorHomEquiv_comp, functorHomEquiv_apply_app, functorHomEquiv_id, CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_three
homEquiv 📖	CompOp	6 math math: homEquiv_apply_π, homEquiv_comp, homEquiv_id, homEquiv_apply_π_assoc, homEquiv_comp_assoc, functorHomEquiv_apply_app
isLimitConeFunctorEnrichedHom 📖	CompOp	—
precompEnrichedHom 📖	CompOp	2 math math: coneFunctorEnrichedHom_π_app, functorHomEquiv_apply_app
precompEnrichedHom' 📖	CompOp	2 math math: CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality, functorEnrichedHom_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coneFunctorEnrichedHom_pt 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.Limits.Cone.pt functorEnrichedHom coneFunctorEnrichedHom enrichedHom	—	—
coneFunctorEnrichedHom_π_app 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const enrichedHom functorEnrichedHom CategoryTheory.Limits.Cone.π coneFunctorEnrichedHom precompEnrichedHom CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Under.forget	—	—
diagram_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.eHomFunctor CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.Functor.map diagram CategoryTheory.eHomWhiskerRight Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
diagram_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category diagram CategoryTheory.eHomWhiskerLeft Opposite.unop	—	—
diagram_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category diagram CategoryTheory.EnrichedCategory.Hom CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory Opposite.unop	—	—
enrichedComp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category diagram Opposite.op enrichedComp CategoryTheory.Limits.end_.π CategoryTheory.Limits.end_ CategoryTheory.EnrichedCategory.Hom CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory Opposite.unop CategoryTheory.Functor.op CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.eComp	—	CategoryTheory.Limits.end_.lift_π
enrichedComp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom enrichedComp CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category diagram Opposite.op CategoryTheory.Limits.end_.π CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Limits.end_ CategoryTheory.eComp CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory Opposite.unop CategoryTheory.Functor.op	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' enrichedComp_π
enrichedHom_condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct enrichedHom CategoryTheory.EnrichedCategory.Hom CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory CategoryTheory.Functor.obj enrichedHomπ CategoryTheory.eHomWhiskerLeft CategoryTheory.Functor.map CategoryTheory.eHomWhiskerRight	—	CategoryTheory.Limits.end_.condition
enrichedHom_condition' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct enrichedHom CategoryTheory.EnrichedCategory.Hom CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory CategoryTheory.Functor.obj enrichedHomπ CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.eHomEquiv CategoryTheory.Functor.map CategoryTheory.eComp CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Limits.end_.condition
enrichedHom_condition'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct enrichedHom CategoryTheory.EnrichedCategory.Hom CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory CategoryTheory.Functor.obj enrichedHomπ CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.eHomEquiv CategoryTheory.Functor.map CategoryTheory.eComp CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' enrichedHom_condition'
enrichedHom_condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct enrichedHom CategoryTheory.EnrichedCategory.Hom CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory CategoryTheory.Functor.obj enrichedHomπ CategoryTheory.eHomWhiskerLeft CategoryTheory.Functor.map CategoryTheory.eHomWhiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' enrichedHom_condition
enrichedId_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category diagram Opposite.op enrichedId CategoryTheory.Limits.end_.π CategoryTheory.eId CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory	—	homEquiv_apply_π CategoryTheory.eHomEquiv_id
enrichedId_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom enrichedId CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category diagram Opposite.op CategoryTheory.Limits.end_.π CategoryTheory.eId CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' enrichedId_π
enriched_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight enrichedComp CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Limits.end_.hom_ext CategoryTheory.Category.assoc enrichedComp_π CategoryTheory.MonoidalCategory.tensorHom_def_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc CategoryTheory.MonoidalCategory.whisker_exchange_assoc CategoryTheory.MonoidalCategory.tensorHom_def'_assoc CategoryTheory.MonoidalCategory.associator_inv_naturality_assoc CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc CategoryTheory.e_assoc
enriched_assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight enrichedComp CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' enriched_assoc
enriched_comp_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct enrichedHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft enrichedId enrichedComp CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.end_.hom_ext CategoryTheory.Category.assoc enrichedComp_π CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc enrichedId_π CategoryTheory.MonoidalCategory.whisker_exchange_assoc CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.e_comp_id CategoryTheory.Category.comp_id
enriched_comp_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct enrichedHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft enrichedId enrichedComp	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' enriched_comp_id
enriched_id_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct enrichedHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight enrichedId enrichedComp CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.end_.hom_ext CategoryTheory.Category.assoc enrichedComp_π CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc enrichedId_π CategoryTheory.MonoidalCategory.whisker_exchange_assoc CategoryTheory.MonoidalCategory.id_whiskerLeft CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.e_id_comp CategoryTheory.Category.comp_id
enriched_id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct enrichedHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight enrichedId enrichedComp	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' enriched_id_comp
functorEnrichedComp_app 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidalStruct functorEnrichedHom functorEnrichedComp enrichedComp CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.comp CategoryTheory.Under.forget	—	—
functorEnrichedHom_map 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.Functor.map functorEnrichedHom precompEnrichedHom' CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.comp CategoryTheory.Under.forget CategoryTheory.Under.map CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category	—	—
functorEnrichedHom_obj 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.Functor.obj functorEnrichedHom enrichedHom CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.comp CategoryTheory.Under.forget	—	—
functorEnrichedId_app 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidalStruct functorEnrichedHom functorEnrichedId enrichedId CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.comp CategoryTheory.Under.forget	—	—
functorEnriched_assoc 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct functorEnrichedHom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight functorEnrichedComp CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.NatTrans.ext' enriched_assoc
functorEnriched_assoc_assoc 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct functorEnrichedHom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight functorEnrichedComp CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functorEnriched_assoc
functorEnriched_comp_id 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functorEnrichedHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft functorEnrichedId functorEnrichedComp CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.ext' enriched_comp_id
functorEnriched_comp_id_assoc 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functorEnrichedHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft functorEnrichedId functorEnrichedComp	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' functorEnriched_comp_id
functorEnriched_id_comp 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functorEnrichedHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight functorEnrichedId functorEnrichedComp CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.ext' enriched_id_comp
functorEnriched_id_comp_assoc 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functorEnrichedHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight functorEnrichedId functorEnrichedComp	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' functorEnriched_id_comp
functorHomEquiv_apply_app 📖	mathematical	HasFunctorEnrichedHom	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidalStruct functorEnrichedHom DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike functorHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.comp CategoryTheory.Under.forget homEquiv precompEnrichedHom	—	—
functorHomEquiv_comp 📖	mathematical	HasFunctorEnrichedHom	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Monoidal.functorCategoryMonoidalStruct functorEnrichedHom EquivLike.toFunLike Equiv.instEquivLike functorHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom functorEnrichedComp	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.end_.hom_ext homEquiv_comp CategoryTheory.Category.assoc CategoryTheory.Limits.end_.lift_π enrichedComp_π CategoryTheory.eHomWhiskerRight_id CategoryTheory.eHomWhiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc homEquiv_apply_π
functorHomEquiv_id 📖	mathematical	HasFunctorEnrichedHom	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Monoidal.functorCategoryMonoidalStruct functorEnrichedHom EquivLike.toFunLike Equiv.instEquivLike functorHomEquiv CategoryTheory.CategoryStruct.id functorEnrichedId	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.end_.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.end_.lift_π CategoryTheory.eHomWhiskerRight_id CategoryTheory.eHomWhiskerLeft_id CategoryTheory.Category.comp_id enrichedId_π
homEquiv_apply_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom CategoryTheory.EnrichedCategory.Hom CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory CategoryTheory.Functor.obj DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.category EquivLike.toFunLike Equiv.instEquivLike homEquiv enrichedHomπ CategoryTheory.eHomEquiv CategoryTheory.NatTrans.app	—	CategoryTheory.Limits.end_.lift_π
homEquiv_apply_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.category EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.EnrichedCategory.Hom CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory CategoryTheory.Functor.obj enrichedHomπ CategoryTheory.eHomEquiv CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homEquiv_apply_π
homEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom enrichedComp	—	CategoryTheory.Limits.end_.hom_ext homEquiv_apply_π CategoryTheory.eHomEquiv_comp CategoryTheory.Category.assoc enrichedComp_π CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc
homEquiv_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.category EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom enrichedComp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homEquiv_comp
homEquiv_id 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct enrichedHom EquivLike.toFunLike Equiv.instEquivLike homEquiv CategoryTheory.CategoryStruct.id enrichedId	—	—
instHasEnrichedHomUnderCompMapForget 📖	mathematical	HasFunctorEnrichedHom	HasEnrichedHom CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.comp CategoryTheory.Under.map CategoryTheory.Under.forget	—	—

CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom CategoryTheory.Enriched.FunctorCategory.enrichedHom CategoryTheory.Functor.obj lift CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.end_.hom_ext CategoryTheory.Limits.Cone.w CategoryTheory.Category.assoc CategoryTheory.Limits.end_.lift_π CategoryTheory.eHomWhiskerRight_id CategoryTheory.eHomWhiskerLeft_id CategoryTheory.Category.comp_id

---

← Back to Index