Closed

📁 Source: Mathlib/CategoryTheory/Monoidal/DayConvolution/Closed.lean

Statistics

Metric	Count
Definitions DayConvolutionInternalHom, coev_app, ev_app, isLimitWedge, map, π, dayConvolutionInternalHomDiagramFunctor	7
Theorems coev_app_π, coev_app_π_assoc, coev_naturality_app, ev_naturality_app, hπ, hπ_assoc, left_triangle_components, map_app_comp_π, map_app_comp_π_assoc, map_comp_π, map_comp_π_assoc, right_triangle_components, unit_app_ev_app_app, unit_app_ev_app_app_assoc, dayConvolutionInternalHomDiagramFunctor_map_app_app_app, dayConvolutionInternalHomDiagramFunctor_obj_map_app_app, dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app, dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_map, dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_obj	19
Total	26

CategoryTheory.MonoidalCategory

Definitions

Name	Category	Theorems
DayConvolutionInternalHom 📖	CompData	—
dayConvolutionInternalHomDiagramFunctor 📖	CompOp	5 math math: dayConvolutionInternalHomDiagramFunctor_obj_map_app_app, dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_map, dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app, dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_obj, dayConvolutionInternalHomDiagramFunctor_map_app_app_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dayConvolutionInternalHomDiagramFunctor_map_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp tensorRight CategoryTheory.MonoidalClosed.internalHom CategoryTheory.Functor.op CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Functor.flip curriedTensor CategoryTheory.Functor.map CategoryTheory.Functor.whiskerRight dayConvolutionInternalHomDiagramFunctor CategoryTheory.ihom Opposite.unop CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct	—	—
dayConvolutionInternalHomDiagramFunctor_obj_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.flip curriedTensor CategoryTheory.MonoidalClosed.internalHom CategoryTheory.Functor.op CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Functor.map dayConvolutionInternalHomDiagramFunctor CategoryTheory.ihom Opposite.unop CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp tensorRight CategoryTheory.MonoidalClosed.internalHom CategoryTheory.Functor.op CategoryTheory.Functor.map dayConvolutionInternalHomDiagramFunctor CategoryTheory.ihom Opposite.unop CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalClosed.pre Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct	—	—
dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category dayConvolutionInternalHomDiagramFunctor CategoryTheory.ihom Opposite.unop CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category dayConvolutionInternalHomDiagramFunctor CategoryTheory.ihom Opposite.unop CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct	—	—

CategoryTheory.MonoidalCategory.DayConvolutionInternalHom

Definitions

Name	Category	Theorems
coev_app 📖	CompOp	5 math math: left_triangle_components, coev_app_π_assoc, right_triangle_components, coev_naturality_app, coev_app_π
ev_app 📖	CompOp	5 math math: unit_app_ev_app_app_assoc, unit_app_ev_app_app, left_triangle_components, ev_naturality_app, right_triangle_components
isLimitWedge 📖	CompOp	—
map 📖	CompOp	5 math math: ev_naturality_app, map_app_comp_π, right_triangle_components, coev_naturality_app, map_app_comp_π_assoc
π 📖	CompOp	10 math math: hπ_assoc, unit_app_ev_app_app_assoc, unit_app_ev_app_app, coev_app_π_assoc, hπ, map_app_comp_π, map_comp_π_assoc, map_comp_π, coev_app_π, map_app_comp_π_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coev_app_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app coev_app π CategoryTheory.MonoidalClosed.curry CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.MonoidalCategory.DayConvolution.unit	—	hπ CategoryTheory.Limits.Wedge.mk_ι CategoryTheory.Limits.Wedge.IsLimit.lift_ι
coev_app_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app coev_app CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct π CategoryTheory.MonoidalClosed.curry CategoryTheory.prod' CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.DayConvolution.unit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coev_app_π
coev_naturality_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category coev_app map CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategory.DayConvolution.map CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.Wedge.IsLimit.hom_ext hπ CategoryTheory.MonoidalClosed.uncurry_injective CategoryTheory.Category.assoc coev_app_π map_app_comp_π coev_app_π_assoc CategoryTheory.MonoidalClosed.uncurry_natural_right CategoryTheory.MonoidalClosed.uncurry_curry CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonoidalClosed.uncurry_natural_left
ev_naturality_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategory.DayConvolution.map CategoryTheory.CategoryStruct.id map ev_app	—	Equiv.injective CategoryTheory.NatTrans.ext' CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app_assoc CategoryTheory.MonoidalCategory.id_tensorHom unit_app_ev_app_app CategoryTheory.MonoidalClosed.uncurry_eq map_app_comp_π CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Category.assoc CategoryTheory.ihom.ev_naturality unit_app_ev_app_app_assoc
hπ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct π CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.NatTrans.app CategoryTheory.MonoidalClosed.pre	—	—
hπ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct π CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.NatTrans.app CategoryTheory.MonoidalClosed.pre	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hπ
left_triangle_components 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategory.DayConvolution.map CategoryTheory.CategoryStruct.id coev_app ev_app	—	Equiv.injective CategoryTheory.NatTrans.ext' CategoryTheory.MonoidalClosed.curry_injective CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app_assoc CategoryTheory.MonoidalCategory.id_tensorHom unit_app_ev_app_app CategoryTheory.MonoidalClosed.curry_natural_left CategoryTheory.MonoidalClosed.curry_uncurry coev_app_π CategoryTheory.Category.comp_id
map_app_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app map π CategoryTheory.Functor.map	—	hπ CategoryTheory.Limits.Wedge.mk_ι CategoryTheory.Limits.Wedge.IsLimit.lift_ι
map_app_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app map CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct π CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_app_comp_π
map_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map π CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
map_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct π CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp_π
right_triangle_components 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category coev_app map CategoryTheory.MonoidalCategory.DayConvolution.convolution ev_app CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.Wedge.IsLimit.hom_ext hπ CategoryTheory.MonoidalClosed.uncurry_injective CategoryTheory.Category.assoc map_app_comp_π coev_app_π_assoc CategoryTheory.MonoidalClosed.uncurry_natural_right CategoryTheory.MonoidalClosed.uncurry_curry unit_app_ev_app_app CategoryTheory.Category.id_comp
unit_app_ev_app_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.DayConvolution.unit ev_app CategoryTheory.MonoidalClosed.uncurry CategoryTheory.MonoidalClosed.closed π	—	CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app
unit_app_ev_app_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ev_app CategoryTheory.MonoidalClosed.uncurry CategoryTheory.MonoidalClosed.closed π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_app_ev_app_app

---

← Back to Index