Basic

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

Statistics

Metric	Count
Definitions EnrichedCategory, comp, id, EnrichedFunctor, category, comp, forget, forgetComp, forgetId, id, instInhabited, isoMk, map, obj, EnrichedNatTrans, out, ForgetEnrichment, homOf, homTo, of, to, GradedNatTrans, app, TransportEnrichment, categoryForgetEnrichment, categoryOfEnrichedCategoryType, eComp, eId, enrichedCategoryTypeEquivCategory, enrichedCategoryTypeOfCategory, enrichedFunctorTypeEquivFunctor, enrichedNatTransYoneda, enrichedNatTransYonedaTypeIsoYonedaNatTrans, instEnrichedCategoryTransportEnrichment, «term_⟶[_]_»	35
Theorems assoc, comp_id, id_comp, category_comp_out, category_id_out, comp_map, comp_obj, ext, forgetComp_hom_app, forgetComp_inv_app, forgetId_hom_app, forgetId_inv_app, forget_map, forget_obj, hom_ext, hom_ext_iff, id_map, id_obj, isoMk_hom_out, isoMk_inv_out, map_comp, map_comp_assoc, map_id, map_id_assoc, homOf_comp, homOf_eId, homOf_homTo, homTo_comp, homTo_homOf, homTo_id, of_to, to_of, ext, ext_iff, naturality, naturality_assoc, eComp_eq, eId_eq, e_assoc, e_assoc', e_assoc'_assoc, e_assoc_assoc, e_comp_id, e_comp_id_assoc, e_id_comp, e_id_comp_assoc, enrichedFunctorTypeEquivFunctor_apply_map, enrichedFunctorTypeEquivFunctor_apply_obj, enrichedFunctorTypeEquivFunctor_symm_apply_map, enrichedFunctorTypeEquivFunctor_symm_apply_obj, enrichedNatTransYoneda_map_app, enrichedNatTransYoneda_obj	52
Total	87

CategoryTheory

Definitions

Name	Category	Theorems
EnrichedCategory 📖	CompData	—
EnrichedFunctor 📖	CompData	16 math math: EnrichedCat.leftUnitor_hom_out_app, EnrichedCat.associator_inv_out_app, EnrichedCat.rightUnitor_hom_out_app, EnrichedFunctor.category_id_out, EnrichedCat.rightUnitor_inv_out_app, enrichedFunctorTypeEquivFunctor_symm_apply_obj, EnrichedCat.comp_whiskerRight, enrichedFunctorTypeEquivFunctor_apply_map, EnrichedCat.associator_hom_out_app, EnrichedCat.leftUnitor_inv_out_app, EnrichedCat.whisker_exchange, EnrichedFunctor.category_comp_out, enrichedFunctorTypeEquivFunctor_apply_obj, EnrichedFunctor.isoMk_inv_out, EnrichedFunctor.isoMk_hom_out, enrichedFunctorTypeEquivFunctor_symm_apply_map
EnrichedNatTrans 📖	CompData	—
ForgetEnrichment 📖	CompOp	44 math math: EnrichedCat.leftUnitor_hom_out_app, ForgetEnrichment.equivFunctor_obj, EnrichedFunctor.forgetComp_inv_app, ForgetEnrichment.equivFunctor_map, ForgetEnrichment.equivInverse_map, TransportEnrichment.forgetEnrichmentEquiv_counitIso, forgetEnrichmentOppositeEquivalence_functor, TransportEnrichment.forgetEnrichmentEquiv_functor, ForgetEnrichment.homOf_eId, EnrichedCat.associator_inv_out_app, EnrichedCat.rightUnitor_hom_out_app, EnrichedFunctor.category_id_out, EnrichedFunctor.forget_map, TransportEnrichment.forgetEnrichmentEquivInverse_obj, ForgetEnrichment.equiv_unitIso, EnrichedCat.rightUnitor_inv_out_app, forgetEnrichmentOppositeEquivalence_unitIso, EnrichedCat.comp_whiskerRight, TransportEnrichment.forgetEnrichmentEquivInverse_map, ForgetEnrichment.homOf_comp, EnrichedFunctor.forgetId_inv_app, EnrichedCat.associator_hom_out_app, EnrichedFunctor.forget_obj, EnrichedCat.leftUnitor_inv_out_app, ForgetEnrichment.homTo_comp, EnrichedFunctor.category_comp_out, ForgetEnrichment.equiv_inverse, ForgetEnrichment.equivInverse_obj, ForgetEnrichment.homTo_id, ForgetEnrichment.equiv_functor, forgetEnrichmentOppositeEquivalence_counitIso, forgetEnrichmentOppositeEquivalence_inverse, EnrichedFunctor.forgetId_hom_app, TransportEnrichment.forgetEnrichmentEquiv_inverse, EnrichedFunctor.forgetComp_hom_app, EnrichedCat.whiskerLeft_out_app, EnrichedFunctor.hom_ext_iff, ForgetEnrichment.equiv_counitIso, TransportEnrichment.forgetEnrichmentEquiv_unitIso, TransportEnrichment.forgetEnrichmentEquivFunctor_obj, EnrichedCat.whiskerRight_out_app, EnrichedFunctor.isoMk_inv_out, EnrichedFunctor.isoMk_hom_out, TransportEnrichment.forgetEnrichmentEquivFunctor_map
GradedNatTrans 📖	CompData	1 math math: enrichedNatTransYoneda_obj
TransportEnrichment 📖	CompOp	10 math math: TransportEnrichment.eId_eq, TransportEnrichment.forgetEnrichmentEquiv_counitIso, TransportEnrichment.forgetEnrichmentEquiv_functor, TransportEnrichment.forgetEnrichmentEquivInverse_obj, TransportEnrichment.forgetEnrichmentEquivInverse_map, TransportEnrichment.eComp_eq, TransportEnrichment.forgetEnrichmentEquiv_inverse, TransportEnrichment.forgetEnrichmentEquiv_unitIso, TransportEnrichment.forgetEnrichmentEquivFunctor_obj, TransportEnrichment.forgetEnrichmentEquivFunctor_map
categoryForgetEnrichment 📖	CompOp	44 math math: EnrichedCat.leftUnitor_hom_out_app, ForgetEnrichment.equivFunctor_obj, EnrichedFunctor.forgetComp_inv_app, ForgetEnrichment.equivFunctor_map, ForgetEnrichment.equivInverse_map, TransportEnrichment.forgetEnrichmentEquiv_counitIso, forgetEnrichmentOppositeEquivalence_functor, TransportEnrichment.forgetEnrichmentEquiv_functor, ForgetEnrichment.homOf_eId, EnrichedCat.associator_inv_out_app, EnrichedCat.rightUnitor_hom_out_app, EnrichedFunctor.category_id_out, EnrichedFunctor.forget_map, TransportEnrichment.forgetEnrichmentEquivInverse_obj, ForgetEnrichment.equiv_unitIso, EnrichedCat.rightUnitor_inv_out_app, forgetEnrichmentOppositeEquivalence_unitIso, EnrichedCat.comp_whiskerRight, TransportEnrichment.forgetEnrichmentEquivInverse_map, ForgetEnrichment.homOf_comp, EnrichedFunctor.forgetId_inv_app, EnrichedCat.associator_hom_out_app, EnrichedFunctor.forget_obj, EnrichedCat.leftUnitor_inv_out_app, ForgetEnrichment.homTo_comp, EnrichedFunctor.category_comp_out, ForgetEnrichment.equiv_inverse, ForgetEnrichment.equivInverse_obj, ForgetEnrichment.homTo_id, ForgetEnrichment.equiv_functor, forgetEnrichmentOppositeEquivalence_counitIso, forgetEnrichmentOppositeEquivalence_inverse, EnrichedFunctor.forgetId_hom_app, TransportEnrichment.forgetEnrichmentEquiv_inverse, EnrichedFunctor.forgetComp_hom_app, EnrichedCat.whiskerLeft_out_app, EnrichedFunctor.hom_ext_iff, ForgetEnrichment.equiv_counitIso, TransportEnrichment.forgetEnrichmentEquiv_unitIso, TransportEnrichment.forgetEnrichmentEquivFunctor_obj, EnrichedCat.whiskerRight_out_app, EnrichedFunctor.isoMk_inv_out, EnrichedFunctor.isoMk_hom_out, TransportEnrichment.forgetEnrichmentEquivFunctor_map
categoryOfEnrichedCategoryType 📖	CompOp	4 math math: enrichedFunctorTypeEquivFunctor_symm_apply_obj, enrichedFunctorTypeEquivFunctor_apply_map, enrichedFunctorTypeEquivFunctor_apply_obj, enrichedFunctorTypeEquivFunctor_symm_apply_map
eComp 📖	CompOp	40 math math: eHom_whisker_cancel, EnrichedOrdinaryCategory.homEquiv_comp, Iso.eHomCongr_inv_comp_assoc, e_comp_id, Enriched.FunctorCategory.enrichedHom_condition', e_id_comp, MonoidalClosed.enrichedCategorySelf_comp, Iso.eHomCongr_comp_assoc, e_comp_id_assoc, eComp_eHomWhiskerRight, e_assoc_assoc, eComp_eHomWhiskerLeft_assoc, e_assoc', ForgetEnrichment.homOf_comp, Enriched.FunctorCategory.enrichedComp_π_assoc, eHom_whisker_cancel_assoc, e_id_comp_assoc, ForgetEnrichment.homTo_comp, eComp_op_eq_assoc, TransportEnrichment.eComp_eq, eComp_eHomWhiskerRight_assoc, EnrichedFunctor.map_comp_assoc, tensorHom_eComp_op_eq_assoc, CatEnriched.comp_eq, eComp_eHomWhiskerLeft, tensorHom_eComp_op_eq, EnrichedFunctor.map_comp, GradedNatTrans.naturality_assoc, Iso.eHomCongr_comp, eHom_whisker_cancel_inv_assoc, eHom_whisker_cancel_inv, eHomEquiv_comp, eHomEquiv_comp_assoc, Enriched.FunctorCategory.enrichedHom_condition'_assoc, e_assoc'_assoc, Enriched.FunctorCategory.enrichedComp_π, Iso.eHomCongr_inv_comp, eComp_op_eq, e_assoc, GradedNatTrans.naturality
eId 📖	CompOp	15 math math: e_comp_id, eHomEquiv_id, TransportEnrichment.eId_eq, e_id_comp, ForgetEnrichment.homOf_eId, Enriched.FunctorCategory.enrichedId_π_assoc, MonoidalClosed.enrichedCategorySelf_id, e_comp_id_assoc, EnrichedOrdinaryCategory.homEquiv_id, EnrichedFunctor.map_id, e_id_comp_assoc, ForgetEnrichment.homTo_id, CatEnriched.id_eq, EnrichedFunctor.map_id_assoc, Enriched.FunctorCategory.enrichedId_π
enrichedCategoryTypeEquivCategory 📖	CompOp	—
enrichedCategoryTypeOfCategory 📖	CompOp	—
enrichedFunctorTypeEquivFunctor 📖	CompOp	4 math math: enrichedFunctorTypeEquivFunctor_symm_apply_obj, enrichedFunctorTypeEquivFunctor_apply_map, enrichedFunctorTypeEquivFunctor_apply_obj, enrichedFunctorTypeEquivFunctor_symm_apply_map
enrichedNatTransYoneda 📖	CompOp	2 math math: enrichedNatTransYoneda_obj, enrichedNatTransYoneda_map_app
enrichedNatTransYonedaTypeIsoYonedaNatTrans 📖	CompOp	—
instEnrichedCategoryTransportEnrichment 📖	CompOp	10 math math: TransportEnrichment.eId_eq, TransportEnrichment.forgetEnrichmentEquiv_counitIso, TransportEnrichment.forgetEnrichmentEquiv_functor, TransportEnrichment.forgetEnrichmentEquivInverse_obj, TransportEnrichment.forgetEnrichmentEquivInverse_map, TransportEnrichment.eComp_eq, TransportEnrichment.forgetEnrichmentEquiv_inverse, TransportEnrichment.forgetEnrichmentEquiv_unitIso, TransportEnrichment.forgetEnrichmentEquivFunctor_obj, TransportEnrichment.forgetEnrichmentEquivFunctor_map
«term_⟶[_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
e_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EnrichedCategory.Hom Iso.inv MonoidalCategoryStruct.associator MonoidalCategoryStruct.whiskerRight eComp MonoidalCategoryStruct.whiskerLeft	—	EnrichedCategory.assoc
e_assoc' 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EnrichedCategory.Hom Iso.hom MonoidalCategoryStruct.associator MonoidalCategoryStruct.whiskerLeft eComp MonoidalCategoryStruct.whiskerRight	—	e_assoc Iso.hom_inv_id_assoc
e_assoc'_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EnrichedCategory.Hom Iso.hom MonoidalCategoryStruct.associator MonoidalCategoryStruct.whiskerLeft eComp MonoidalCategoryStruct.whiskerRight	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' e_assoc'
e_assoc_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EnrichedCategory.Hom Iso.inv MonoidalCategoryStruct.associator MonoidalCategoryStruct.whiskerRight eComp MonoidalCategoryStruct.whiskerLeft	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' e_assoc
e_comp_id 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct EnrichedCategory.Hom MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.rightUnitor MonoidalCategoryStruct.whiskerLeft eId eComp CategoryStruct.id	—	EnrichedCategory.comp_id
e_comp_id_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct EnrichedCategory.Hom MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.rightUnitor MonoidalCategoryStruct.whiskerLeft eId eComp	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' e_comp_id
e_id_comp 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct EnrichedCategory.Hom MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.leftUnitor MonoidalCategoryStruct.whiskerRight eId eComp CategoryStruct.id	—	EnrichedCategory.id_comp
e_id_comp_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct EnrichedCategory.Hom MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.leftUnitor MonoidalCategoryStruct.whiskerRight eId eComp	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' e_id_comp
enrichedFunctorTypeEquivFunctor_apply_map 📖	mathematical	—	Functor.map categoryOfEnrichedCategoryType DFunLike.coe Equiv EnrichedFunctor types SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory typesCartesianMonoidalCategory Functor EquivLike.toFunLike Equiv.instEquivLike enrichedFunctorTypeEquivFunctor EnrichedFunctor.map	—	—
enrichedFunctorTypeEquivFunctor_apply_obj 📖	mathematical	—	Functor.obj categoryOfEnrichedCategoryType DFunLike.coe Equiv EnrichedFunctor types SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory typesCartesianMonoidalCategory Functor EquivLike.toFunLike Equiv.instEquivLike enrichedFunctorTypeEquivFunctor EnrichedFunctor.obj	—	—
enrichedFunctorTypeEquivFunctor_symm_apply_map 📖	mathematical	—	EnrichedFunctor.map types SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory typesCartesianMonoidalCategory DFunLike.coe Equiv Functor categoryOfEnrichedCategoryType EnrichedFunctor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm enrichedFunctorTypeEquivFunctor Functor.map	—	—
enrichedFunctorTypeEquivFunctor_symm_apply_obj 📖	mathematical	—	EnrichedFunctor.obj types SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory typesCartesianMonoidalCategory DFunLike.coe Equiv Functor categoryOfEnrichedCategoryType EnrichedFunctor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm enrichedFunctorTypeEquivFunctor Functor.obj	—	—
enrichedNatTransYoneda_map_app 📖	mathematical	—	GradedNatTrans.app Functor.obj Center Center.instCategory Center.ofBraided Opposite.unop Functor.map Opposite Category.opposite types enrichedNatTransYoneda CategoryStruct.comp Category.toCategoryStruct HalfBraiding EnrichedCategory.Hom EnrichedFunctor.obj Quiver.Hom.unop CategoryStruct.toQuiver	—	—
enrichedNatTransYoneda_obj 📖	mathematical	—	Functor.obj Opposite Category.opposite types enrichedNatTransYoneda GradedNatTrans Center Center.instCategory Center.ofBraided Opposite.unop	—	—

CategoryTheory.EnrichedCategory

Definitions

Name	Category	Theorems
comp 📖	CompOp	3 math math: comp_id, id_comp, assoc
id 📖	CompOp	2 math math: comp_id, id_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Hom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight comp CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
comp_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft id comp CategoryTheory.CategoryStruct.id	—	—
id_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight id comp CategoryTheory.CategoryStruct.id	—	—

CategoryTheory.EnrichedFunctor

Definitions

Name	Category	Theorems
category 📖	CompOp	12 math math: CategoryTheory.EnrichedCat.leftUnitor_hom_out_app, CategoryTheory.EnrichedCat.associator_inv_out_app, CategoryTheory.EnrichedCat.rightUnitor_hom_out_app, category_id_out, CategoryTheory.EnrichedCat.rightUnitor_inv_out_app, CategoryTheory.EnrichedCat.comp_whiskerRight, CategoryTheory.EnrichedCat.associator_hom_out_app, CategoryTheory.EnrichedCat.leftUnitor_inv_out_app, CategoryTheory.EnrichedCat.whisker_exchange, category_comp_out, isoMk_inv_out, isoMk_hom_out
comp 📖	CompOp	15 math math: CategoryTheory.EnrichedCat.leftUnitor_hom_out_app, forgetComp_inv_app, CategoryTheory.EnrichedCat.associator_inv_out_app, CategoryTheory.EnrichedCat.rightUnitor_hom_out_app, comp_map, CategoryTheory.EnrichedCat.rightUnitor_inv_out_app, CategoryTheory.EnrichedCat.comp_whiskerRight, CategoryTheory.EnrichedCat.associator_hom_out_app, CategoryTheory.EnrichedCat.leftUnitor_inv_out_app, CategoryTheory.EnrichedCat.whisker_exchange, forgetComp_hom_app, comp_obj, CategoryTheory.EnrichedCat.whiskerLeft_out_app, CategoryTheory.EnrichedCat.whiskerRight_out_app, CategoryTheory.SimplicialThickening.functor_comp
forget 📖	CompOp	20 math math: CategoryTheory.EnrichedCat.leftUnitor_hom_out_app, forgetComp_inv_app, CategoryTheory.EnrichedCat.associator_inv_out_app, CategoryTheory.EnrichedCat.rightUnitor_hom_out_app, category_id_out, forget_map, CategoryTheory.EnrichedCat.rightUnitor_inv_out_app, CategoryTheory.EnrichedCat.comp_whiskerRight, forgetId_inv_app, CategoryTheory.EnrichedCat.associator_hom_out_app, forget_obj, CategoryTheory.EnrichedCat.leftUnitor_inv_out_app, category_comp_out, forgetId_hom_app, forgetComp_hom_app, CategoryTheory.EnrichedCat.whiskerLeft_out_app, hom_ext_iff, CategoryTheory.EnrichedCat.whiskerRight_out_app, isoMk_inv_out, isoMk_hom_out
forgetComp 📖	CompOp	2 math math: forgetComp_inv_app, forgetComp_hom_app
forgetId 📖	CompOp	2 math math: forgetId_inv_app, forgetId_hom_app
id 📖	CompOp	9 math math: CategoryTheory.EnrichedCat.leftUnitor_hom_out_app, CategoryTheory.EnrichedCat.rightUnitor_hom_out_app, id_map, CategoryTheory.EnrichedCat.rightUnitor_inv_out_app, forgetId_inv_app, CategoryTheory.EnrichedCat.leftUnitor_inv_out_app, forgetId_hom_app, id_obj, CategoryTheory.SimplicialThickening.functor_id
instInhabited 📖	CompOp	—
isoMk 📖	CompOp	2 math math: isoMk_inv_out, isoMk_hom_out
map 📖	CompOp	13 math math: forget_map, id_map, comp_map, CategoryTheory.SimplicialThickening.functor_map, CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_map, map_id, map_comp_assoc, map_comp, CategoryTheory.GradedNatTrans.naturality_assoc, CategoryTheory.EnrichedCat.whiskerRight_out_app, map_id_assoc, CategoryTheory.GradedNatTrans.naturality, CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_map
obj 📖	CompOp	25 math math: CategoryTheory.EnrichedCat.leftUnitor_hom_out_app, forgetComp_inv_app, CategoryTheory.EnrichedCat.associator_inv_out_app, CategoryTheory.EnrichedCat.rightUnitor_hom_out_app, forget_map, comp_map, CategoryTheory.EnrichedCat.rightUnitor_inv_out_app, CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_obj, map_id, CategoryTheory.EnrichedCat.associator_hom_out_app, forget_obj, CategoryTheory.EnrichedCat.leftUnitor_inv_out_app, map_comp_assoc, map_comp, CategoryTheory.GradedNatTrans.naturality_assoc, CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_obj, forgetComp_hom_app, comp_obj, CategoryTheory.EnrichedCat.whiskerLeft_out_app, CategoryTheory.EnrichedCat.whiskerRight_out_app, id_obj, map_id_assoc, CategoryTheory.SimplicialThickening.functor_obj_as, CategoryTheory.GradedNatTrans.naturality, CategoryTheory.enrichedNatTransYoneda_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
category_comp_out 📖	mathematical	—	CategoryTheory.EnrichedNatTrans.out CategoryTheory.CategoryStruct.comp CategoryTheory.EnrichedFunctor CategoryTheory.Category.toCategoryStruct category CategoryTheory.Functor CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.Functor.category forget	—	—
category_id_out 📖	mathematical	—	CategoryTheory.EnrichedNatTrans.out CategoryTheory.CategoryStruct.id CategoryTheory.EnrichedFunctor CategoryTheory.Category.toCategoryStruct category CategoryTheory.Functor CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.Functor.category forget	—	—
comp_map 📖	mathematical	—	map comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.EnrichedCategory.Hom obj	—	—
comp_obj 📖	mathematical	—	obj comp	—	—
ext 📖	—	obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.EnrichedCategory.Hom map CategoryTheory.eqToHom	—	—	CategoryTheory.Category.comp_id
forgetComp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment forget comp CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category forgetComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ForgetEnrichment.of obj CategoryTheory.ForgetEnrichment.to	—	—
forgetComp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.Functor.comp forget comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category forgetComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ForgetEnrichment.of obj CategoryTheory.ForgetEnrichment.to	—	—
forgetId_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment forget id CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category forgetId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
forgetId_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.Functor.id forget id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category forgetId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment forget CategoryTheory.ForgetEnrichment.homOf obj CategoryTheory.ForgetEnrichment.to CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.EnrichedCategory.Hom CategoryTheory.ForgetEnrichment.homTo map	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment forget CategoryTheory.ForgetEnrichment.of obj CategoryTheory.ForgetEnrichment.to	—	—
hom_ext 📖	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment forget CategoryTheory.EnrichedNatTrans.out	—	—	CategoryTheory.NatTrans.ext'
hom_ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment forget CategoryTheory.EnrichedNatTrans.out	—	hom_ext
id_map 📖	mathematical	—	map id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.EnrichedCategory.Hom	—	—
id_obj 📖	mathematical	—	obj id	—	—
isoMk_hom_out 📖	mathematical	—	CategoryTheory.EnrichedNatTrans.out CategoryTheory.Iso.hom CategoryTheory.EnrichedFunctor category isoMk CategoryTheory.Functor CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.Functor.category forget	—	—
isoMk_inv_out 📖	mathematical	—	CategoryTheory.EnrichedNatTrans.out CategoryTheory.Iso.inv CategoryTheory.EnrichedFunctor category isoMk CategoryTheory.Functor CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.Functor.category forget	—	—
map_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.EnrichedCategory.Hom obj CategoryTheory.eComp map CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
map_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.EnrichedCategory.Hom CategoryTheory.eComp obj map CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.EnrichedCategory.Hom obj CategoryTheory.eId map	—	—
map_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.EnrichedCategory.Hom CategoryTheory.eId obj map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_id

CategoryTheory.EnrichedNatTrans

Definitions

Name	Category	Theorems
out 📖	CompOp	14 math math: CategoryTheory.EnrichedCat.leftUnitor_hom_out_app, CategoryTheory.EnrichedCat.associator_inv_out_app, CategoryTheory.EnrichedCat.rightUnitor_hom_out_app, CategoryTheory.EnrichedFunctor.category_id_out, CategoryTheory.EnrichedCat.rightUnitor_inv_out_app, CategoryTheory.EnrichedCat.comp_whiskerRight, CategoryTheory.EnrichedCat.associator_hom_out_app, CategoryTheory.EnrichedCat.leftUnitor_inv_out_app, CategoryTheory.EnrichedFunctor.category_comp_out, CategoryTheory.EnrichedCat.whiskerLeft_out_app, CategoryTheory.EnrichedFunctor.hom_ext_iff, CategoryTheory.EnrichedCat.whiskerRight_out_app, CategoryTheory.EnrichedFunctor.isoMk_inv_out, CategoryTheory.EnrichedFunctor.isoMk_hom_out

CategoryTheory.ForgetEnrichment

Definitions

Name	Category	Theorems
homOf 📖	CompOp	9 math math: equivInverse_map, homOf_eId, CategoryTheory.EnrichedFunctor.forget_map, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_map, homOf_comp, homTo_homOf, homOf_homTo, CategoryTheory.EnrichedCat.whiskerRight_out_app, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_map
homTo 📖	CompOp	9 math math: equivFunctor_map, CategoryTheory.EnrichedFunctor.forget_map, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_map, homTo_comp, homTo_id, homTo_homOf, homOf_homTo, CategoryTheory.EnrichedCat.whiskerRight_out_app, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_map
of 📖	CompOp	19 math math: CategoryTheory.EnrichedCat.leftUnitor_hom_out_app, CategoryTheory.EnrichedFunctor.forgetComp_inv_app, homOf_eId, CategoryTheory.EnrichedCat.associator_inv_out_app, CategoryTheory.EnrichedCat.rightUnitor_hom_out_app, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_obj, CategoryTheory.EnrichedCat.rightUnitor_inv_out_app, of_to, homOf_comp, CategoryTheory.EnrichedCat.associator_hom_out_app, CategoryTheory.EnrichedFunctor.forget_obj, CategoryTheory.EnrichedCat.leftUnitor_inv_out_app, equivInverse_obj, homTo_homOf, CategoryTheory.EnrichedFunctor.forgetComp_hom_app, CategoryTheory.EnrichedCat.whiskerLeft_out_app, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_obj, CategoryTheory.EnrichedCat.whiskerRight_out_app, to_of
to 📖	CompOp	21 math math: CategoryTheory.EnrichedCat.leftUnitor_hom_out_app, equivFunctor_obj, CategoryTheory.EnrichedFunctor.forgetComp_inv_app, equivFunctor_map, CategoryTheory.EnrichedCat.associator_inv_out_app, CategoryTheory.EnrichedCat.rightUnitor_hom_out_app, CategoryTheory.EnrichedFunctor.forget_map, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_obj, CategoryTheory.EnrichedCat.rightUnitor_inv_out_app, of_to, CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_map, CategoryTheory.EnrichedCat.associator_hom_out_app, CategoryTheory.EnrichedFunctor.forget_obj, CategoryTheory.EnrichedCat.leftUnitor_inv_out_app, homTo_comp, homTo_id, CategoryTheory.EnrichedFunctor.forgetComp_hom_app, CategoryTheory.EnrichedCat.whiskerLeft_out_app, homOf_homTo, CategoryTheory.EnrichedCat.whiskerRight_out_app, to_of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homOf_comp 📖	mathematical	—	homOf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.EnrichedCategory.Hom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.eComp CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment of	—	CategoryTheory.Category.assoc
homOf_eId 📖	mathematical	—	homOf CategoryTheory.eId CategoryTheory.CategoryStruct.id CategoryTheory.ForgetEnrichment CategoryTheory.Category.toCategoryStruct CategoryTheory.categoryForgetEnrichment of	—	homTo_id
homOf_homTo 📖	mathematical	—	homOf to homTo	—	—
homTo_comp 📖	mathematical	—	homTo CategoryTheory.CategoryStruct.comp CategoryTheory.ForgetEnrichment CategoryTheory.Category.toCategoryStruct CategoryTheory.categoryForgetEnrichment CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.EnrichedCategory.Hom to CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.eComp	—	—
homTo_homOf 📖	mathematical	—	homTo of homOf	—	—
homTo_id 📖	mathematical	—	homTo CategoryTheory.CategoryStruct.id CategoryTheory.ForgetEnrichment CategoryTheory.Category.toCategoryStruct CategoryTheory.categoryForgetEnrichment CategoryTheory.eId to	—	CategoryTheory.Category.id_comp
of_to 📖	mathematical	—	of to	—	—
to_of 📖	mathematical	—	to of	—	—

CategoryTheory.GradedNatTrans

Definitions

Name	Category	Theorems
app 📖	CompOp	4 math math: ext_iff, naturality_assoc, naturality, CategoryTheory.enrichedNatTransYoneda_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	app	—	—	—
ext_iff 📖	mathematical	—	app	—	ext
naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding CategoryTheory.EnrichedCategory.Hom CategoryTheory.EnrichedFunctor.obj CategoryTheory.Iso.hom CategoryTheory.HalfBraiding.β CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.EnrichedFunctor.map app CategoryTheory.eComp	—	—
naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding CategoryTheory.EnrichedCategory.Hom CategoryTheory.Iso.hom CategoryTheory.HalfBraiding.β CategoryTheory.EnrichedFunctor.obj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.EnrichedFunctor.map app CategoryTheory.eComp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality

CategoryTheory.TransportEnrichment

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eComp_eq 📖	mathematical	—	CategoryTheory.eComp CategoryTheory.TransportEnrichment CategoryTheory.instEnrichedCategoryTransportEnrichment CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.EnrichedCategory.Hom CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.map	—	—
eId_eq 📖	mathematical	—	CategoryTheory.eId CategoryTheory.TransportEnrichment CategoryTheory.instEnrichedCategoryTransportEnrichment CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.EnrichedCategory.Hom CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.map	—	—

---

← Back to Index