DayConvolution

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

Statistics

Metric	Count
Definitions DayConvolution, associator, associatorCorepresentingIso, convolution, corepresentableBy, corepresentableBy₂, corepresentableBy₂', isPointwiseLeftKanExtensionUnit, map, uniqueUpToIso, unit, «term_⊛_», DayConvolutionUnit, can, corepresentableByLeft, corepresentableByRight, isPointwiseLeftKanExtensionCan, leftUnitor, leftUnitorCorepresentingIso, rightUnitor, rightUnitorCorepresentingIso, φ, InducedLawfulDayConvolutionMonoidalCategoryStructCore, convolutionUnitApp, convolutions, convolutions', fullyFaithulι, mkLawfulDayConvolutionMonoidalCategoryStruct, mkMonoidalCategoryStruct, ofHasDayConvolutions, tensorHom, tensorObj, tensorObjIsoConvolution, tensorUnit, tensorUnitConvolutionUnit, ι, LawfulDayConvolutionMonoidalCategoryStruct, convolution, convolutionExtensionUnit, convolutionUnit, convolution₂, convolution₂', isPointwiseLeftKanExtensionConvolutionExtensionUnit, isPointwiseLeftKanExtensionUnitUnit, unitUnit, ι, lawfulDayConvolutionMonoidalCategoryStructOfHasDayConvolutions, monoidalOfHasDayConvolutions, monoidalOfLawfulDayConvolutionMonoidalCategoryStruct	49
Theorems associatorCorepresentingIso_hom_app_app, associatorCorepresentingIso_inv_app_app, associator_hom_unit_unit, associator_hom_unit_unit_assoc, associator_inv_unit_unit, associator_inv_unit_unit_assoc, associator_naturality, convolution_hom_ext_at, corepresentableBy_homEquiv_apply_app, corepresentableBy_homEquiv_symm_apply, corepresentableBy₂'_homEquiv, corepresentableBy₂_homEquiv, instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit, instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit, leftKanExtension, pentagon, triangle, unit_app_map_app, unit_app_map_app_assoc, unit_naturality, unit_naturality_assoc, unit_uniqueUpToIso_hom, unit_uniqueUpToIso_hom_assoc, unit_uniqueUpToIso_inv, unit_uniqueUpToIso_inv_assoc, whiskerLeft_comp_unit_app, whiskerLeft_comp_unit_app_assoc, whiskerRight_comp_unit_app, whiskerRight_comp_unit_app_assoc, corepresentableByLeft_homEquiv, corepresentableByRight_homEquiv, hom_ext, instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ, instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ, leftUnitorCorepresentingIso_hom_app_app, leftUnitorCorepresentingIso_inv_app_app, leftUnitor_hom_unit_app, leftUnitor_hom_unit_app_assoc, leftUnitor_inv_app, leftUnitor_inv_app_assoc, leftUnitor_naturality, leftUnitor_naturality_assoc, rightUnitorCorepresentingIso_hom_app_app, rightUnitorCorepresentingIso_inv_app_app, rightUnitor_hom_unit_app, rightUnitor_hom_unit_app_assoc, rightUnitor_inv_app, rightUnitor_inv_app_assoc, rightUnitor_naturality, rightUnitor_naturality_assoc, convolutionUnitApp_eq, id_tensorHom, tensorHom_eq, tensorHom_id, ι_map_tensorHom_eq, associator_hom_unit_unit, convolutionExtensionUnit_comp_ι_map_tensorHom_app, convolutionExtensionUnit_comp_ι_map_whiskerLeft_app, convolutionExtensionUnit_comp_ι_map_whiskerRight_app, faithful_ι, leftUnitor_hom_unit_app, rightUnitor_hom_unit_app, ι_map_associator_hom_eq_associator_hom, ι_map_leftUnitor_hom_eq_leftUnitor_hom, ι_map_rightUnitor_hom_eq_rightUnitor_hom, ι_map_tensorHom_hom_eq_tensorHom	66
Total	115

CategoryTheory.MonoidalCategory

Definitions

Name	Category	Theorems
DayConvolution 📖	CompData	—
DayConvolutionUnit 📖	CompData	—
InducedLawfulDayConvolutionMonoidalCategoryStructCore 📖	CompData	—
LawfulDayConvolutionMonoidalCategoryStruct 📖	CompData	—
lawfulDayConvolutionMonoidalCategoryStructOfHasDayConvolutions 📖	CompOp	—
monoidalOfHasDayConvolutions 📖	CompOp	—
monoidalOfLawfulDayConvolutionMonoidalCategoryStruct 📖	CompOp	—

CategoryTheory.MonoidalCategory.DayConvolution

Definitions

Name	Category	Theorems
associator 📖	CompOp	10 math math: CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_associator_hom_eq_associator_hom, hexagon_forward, associator_inv_unit_unit, hexagon_reverse, pentagon, triangle, associator_hom_unit_unit_assoc, associator_naturality, associator_inv_unit_unit_assoc, associator_hom_unit_unit
associatorCorepresentingIso 📖	CompOp	2 math math: associatorCorepresentingIso_inv_app_app, associatorCorepresentingIso_hom_app_app
convolution 📖	CompOp	66 math math: braidingHomCorepresenting_app, CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_associator_hom_eq_associator_hom, unit_naturality, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_naturality_assoc, braiding_naturality_left_assoc, corepresentableBy₂_homEquiv, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app_assoc, whiskerRight_comp_unit_app_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.left_triangle_components, unit_naturality_assoc, whiskerLeft_comp_unit_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_inv_app, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π_assoc, hexagon_forward, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app_assoc, associator_inv_unit_unit, hexagon_reverse, pentagon, unit_uniqueUpToIso_inv, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.ev_naturality_app, unit_uniqueUpToIso_hom, instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit, corepresentableBy₂'_homEquiv, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_hom_unit_app_assoc, braiding_naturality_right, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.right_triangle_components, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_hom_unit_app, braiding_naturality_right_assoc, corepresentableBy_homEquiv_symm_apply, triangle, unit_app_braiding_inv_app, symmetry, unit_app_braiding_hom_app, braidingInvCorepresenting_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_naturality_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_naturality, CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_rightUnitor_hom_eq_rightUnitor_hom, CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_leftUnitor_hom_eq_leftUnitor_hom, unit_uniqueUpToIso_hom_assoc, corepresentableBy_homEquiv_apply_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_inv_app, associator_hom_unit_unit_assoc, instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit, associator_naturality, unit_app_braiding_hom_app_assoc, whiskerLeft_comp_unit_app_assoc, associator_inv_unit_unit_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByLeft_homEquiv, unit_app_map_app_assoc, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_naturality_app, unit_app_braiding_inv_app_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_naturality, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_inv_app_assoc, CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom_eq, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π, whiskerRight_comp_unit_app, CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutionUnitApp_eq, associator_hom_unit_unit, unit_app_map_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight_homEquiv, braiding_naturality_left, unit_uniqueUpToIso_inv_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_inv_app_assoc, leftKanExtension
corepresentableBy 📖	CompOp	4 math math: corepresentableBy₂_homEquiv, corepresentableBy₂'_homEquiv, corepresentableBy_homEquiv_symm_apply, corepresentableBy_homEquiv_apply_app
corepresentableBy₂ 📖	CompOp	1 math math: corepresentableBy₂_homEquiv
corepresentableBy₂' 📖	CompOp	1 math math: corepresentableBy₂'_homEquiv
isPointwiseLeftKanExtensionUnit 📖	CompOp	—
map 📖	CompOp	21 math math: CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_naturality_assoc, braiding_naturality_left_assoc, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.left_triangle_components, hexagon_forward, hexagon_reverse, pentagon, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.ev_naturality_app, CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι_map_tensorHom_eq, braiding_naturality_right, braiding_naturality_right_assoc, triangle, CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_tensorHom_hom_eq_tensorHom, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_naturality_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_naturality, associator_naturality, unit_app_map_app_assoc, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_naturality_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_naturality, CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom_eq, unit_app_map_app, braiding_naturality_left
uniqueUpToIso 📖	CompOp	4 math math: unit_uniqueUpToIso_inv, unit_uniqueUpToIso_hom, unit_uniqueUpToIso_hom_assoc, unit_uniqueUpToIso_inv_assoc
unit 📖	CompOp	44 math math: braidingHomCorepresenting_app, unit_naturality, corepresentableBy₂_homEquiv, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app_assoc, whiskerRight_comp_unit_app_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app, unit_naturality_assoc, whiskerLeft_comp_unit_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_inv_app, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app_assoc, associator_inv_unit_unit, unit_uniqueUpToIso_inv, unit_uniqueUpToIso_hom, instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit, corepresentableBy₂'_homEquiv, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_hom_unit_app_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_hom_unit_app, corepresentableBy_homEquiv_symm_apply, unit_app_braiding_inv_app, unit_app_braiding_hom_app, braidingInvCorepresenting_app, unit_uniqueUpToIso_hom_assoc, corepresentableBy_homEquiv_apply_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_inv_app, associator_hom_unit_unit_assoc, instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit, unit_app_braiding_hom_app_assoc, whiskerLeft_comp_unit_app_assoc, associator_inv_unit_unit_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByLeft_homEquiv, unit_app_map_app_assoc, unit_app_braiding_inv_app_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_inv_app_assoc, CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π, whiskerRight_comp_unit_app, CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutionUnitApp_eq, associator_hom_unit_unit, unit_app_map_app, CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight_homEquiv, unit_uniqueUpToIso_inv_assoc, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_inv_app_assoc, leftKanExtension
«term_⊛_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associatorCorepresentingIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' CategoryTheory.uniformProd Opposite.unop CategoryTheory.Functor Opposite.op CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.obj CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.comp CategoryTheory.Functor.prod CategoryTheory.Functor.id CategoryTheory.MonoidalCategory.tensor CategoryTheory.types Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda CategoryTheory.Iso.hom associatorCorepresentingIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.prod.inverseAssociator DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Functor.FullyFaithful.homEquiv CategoryTheory.Equivalence.fullyFaithfulFunctor CategoryTheory.Equivalence.congrLeft CategoryTheory.prod.associativity CategoryTheory.Functor.map	—	—
associatorCorepresentingIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' CategoryTheory.uniformProd Opposite.unop CategoryTheory.Functor Opposite.op CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.obj CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.prod CategoryTheory.MonoidalCategory.tensor CategoryTheory.Functor.id CategoryTheory.types CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda CategoryTheory.Iso.inv associatorCorepresentingIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.prod.associator CategoryTheory.prod.inverseAssociator CategoryTheory.Equivalence.unit CategoryTheory.prod.associativity CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Equivalence.unitInv	—	CategoryTheory.Equivalence.funInvIdAssoc_inv_app CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Equivalence.funInvIdAssoc_hom_app CategoryTheory.MonoidalCategory.associator_conjugation CategoryTheory.Functor.map_comp CategoryTheory.Iso.map_inv_hom_id_assoc
associator_hom_unit_unit 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp convolution CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.NatTrans.app unit CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category associator CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	Equiv.rightInverse_symm leftKanExtension instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit CategoryTheory.Functor.descOfIsLeftKanExtension.congr_simp CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.Equivalence.funInvIdAssoc_inv_app CategoryTheory.Functor.map_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id CategoryTheory.Equivalence.funInvIdAssoc_hom_app CategoryTheory.MonoidalCategory.tensorHom_id
associator_hom_unit_unit_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct convolution CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.NatTrans.app CategoryTheory.Functor.comp unit CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category associator CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_hom_unit_unit
associator_inv_unit_unit 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp convolution CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.NatTrans.app unit CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category associator CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	Equiv.rightInverse_symm leftKanExtension instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.Category.assoc
associator_inv_unit_unit_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct convolution CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.NatTrans.app CategoryTheory.Functor.comp unit CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category associator CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_inv_unit_unit
associator_naturality 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution map CategoryTheory.Iso.hom associator	—	Equiv.injective CategoryTheory.NatTrans.ext' instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id unit_app_map_app_assoc associator_hom_unit_unit_assoc CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc unit_app_map_app CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.whisker_exchange_assoc associator_hom_unit_unit CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Iso.hom_inv_id_assoc
convolution_hom_ext_at 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution CategoryTheory.NatTrans.app unit CategoryTheory.Functor.map	—	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Category.assoc
corepresentableBy_homEquiv_apply_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Functor.CorepresentableBy.homEquiv CategoryTheory.uniformProd CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda Opposite.op corepresentableBy CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct unit	—	—
corepresentableBy_homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Functor.CorepresentableBy.homEquiv CategoryTheory.uniformProd CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda Opposite.op corepresentableBy CategoryTheory.Functor.descOfIsLeftKanExtension unit leftKanExtension	—	—
corepresentableBy₂'_homEquiv 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.Functor.CorepresentableBy.homEquiv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda Opposite.op CategoryTheory.MonoidalCategory.externalProduct convolution corepresentableBy₂' Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct corepresentableBy CategoryTheory.Functor.homEquivOfIsLeftKanExtension CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft unit instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit	—	—
corepresentableBy₂_homEquiv 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.Functor.CorepresentableBy.homEquiv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda Opposite.op CategoryTheory.MonoidalCategory.externalProduct convolution corepresentableBy₂ Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct corepresentableBy CategoryTheory.Functor.homEquivOfIsLeftKanExtension CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight unit instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit	—	—
instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct convolution CategoryTheory.Functor.prod CategoryTheory.Functor.id CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft unit	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct convolution CategoryTheory.Functor.prod CategoryTheory.Functor.id CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight unit	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
leftKanExtension 📖	mathematical	—	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.prod' convolution CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct unit	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
pentagon 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution map CategoryTheory.Iso.hom associator CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.hom_ext_of_isLeftKanExtension leftKanExtension instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension CategoryTheory.NatTrans.ext' CategoryTheory.NatTrans.naturality associator_inv_unit_unit_assoc CategoryTheory.Iso.map_hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.tensor_whiskerLeft_symm CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.whiskerLeft_id unit_app_map_app_assoc CategoryTheory.MonoidalCategory.tensorHom_id associator_hom_unit_unit_assoc CategoryTheory.MonoidalCategory.whiskerRight_tensor_symm_assoc CategoryTheory.Iso.inv_hom_id_assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_hom_unit_unit CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.whisker_assoc whiskerRight_comp_unit_app_assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonoidalCategory.whiskerLeft_comp whiskerLeft_comp_unit_app_assoc CategoryTheory.MonoidalCategory.pentagon_inv CategoryTheory.MonoidalCategory.pentagon_assoc
triangle 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category convolution CategoryTheory.Iso.hom associator map CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor	—	CategoryTheory.Functor.hom_ext_of_isLeftKanExtension leftKanExtension instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension CategoryTheory.NatTrans.ext' CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id associator_hom_unit_unit_assoc CategoryTheory.NatTrans.naturality unit_app_map_app_assoc CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc unit_app_map_app CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_hom_unit_app CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app CategoryTheory.MonoidalCategory.whiskerLeft_comp whiskerLeft_comp_unit_app_assoc CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv CategoryTheory.MonoidalCategory.comp_whiskerRight whiskerRight_comp_unit_app CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_assoc
unit_app_map_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app unit map CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.Category.assoc leftKanExtension CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app
unit_app_map_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct convolution CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp unit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct map CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_app_map_app
unit_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct unit	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.NatTrans.naturality
unit_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.map convolution CategoryTheory.prod' CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp unit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_naturality
unit_uniqueUpToIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution CategoryTheory.uniformProd unit CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom uniqueUpToIso	—	leftKanExtension CategoryTheory.Functor.leftKanExtensionUnique_hom CategoryTheory.Functor.descOfIsLeftKanExtension_fac
unit_uniqueUpToIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution unit CategoryTheory.uniformProd CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom uniqueUpToIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_uniqueUpToIso_hom
unit_uniqueUpToIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution CategoryTheory.uniformProd unit CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.inv uniqueUpToIso	—	leftKanExtension CategoryTheory.Functor.leftKanExtensionUnique_inv CategoryTheory.Functor.descOfIsLeftKanExtension_fac
unit_uniqueUpToIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution unit CategoryTheory.uniformProd CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.inv uniqueUpToIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' unit_uniqueUpToIso_inv
whiskerLeft_comp_unit_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct unit	—	CategoryTheory.Functor.map_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.NatTrans.naturality
whiskerLeft_comp_unit_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor.map convolution CategoryTheory.prod' CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp unit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_comp_unit_app
whiskerRight_comp_unit_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor convolution CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct unit	—	CategoryTheory.Functor.map_id CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.NatTrans.naturality
whiskerRight_comp_unit_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.map convolution CategoryTheory.prod' CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp unit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_comp_unit_app

CategoryTheory.MonoidalCategory.DayConvolutionUnit

Definitions

Name	Category	Theorems
can 📖	CompOp	8 math math: rightUnitor_hom_unit_app, leftUnitor_inv_app, rightUnitor_hom_unit_app_assoc, leftUnitor_hom_unit_app_assoc, leftUnitor_hom_unit_app, rightUnitor_inv_app, rightUnitor_inv_app_assoc, leftUnitor_inv_app_assoc
corepresentableByLeft 📖	CompOp	1 math math: corepresentableByLeft_homEquiv
corepresentableByRight 📖	CompOp	1 math math: corepresentableByRight_homEquiv
isPointwiseLeftKanExtensionCan 📖	CompOp	—
leftUnitor 📖	CompOp	8 math math: leftUnitor_naturality_assoc, leftUnitor_inv_app, leftUnitor_hom_unit_app_assoc, leftUnitor_hom_unit_app, CategoryTheory.MonoidalCategory.DayConvolution.triangle, leftUnitor_naturality, CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_leftUnitor_hom_eq_leftUnitor_hom, leftUnitor_inv_app_assoc
leftUnitorCorepresentingIso 📖	CompOp	2 math math: leftUnitorCorepresentingIso_inv_app_app, leftUnitorCorepresentingIso_hom_app_app
rightUnitor 📖	CompOp	8 math math: rightUnitor_hom_unit_app, rightUnitor_hom_unit_app_assoc, CategoryTheory.MonoidalCategory.DayConvolution.triangle, rightUnitor_naturality_assoc, CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_rightUnitor_hom_eq_rightUnitor_hom, rightUnitor_inv_app, rightUnitor_naturality, rightUnitor_inv_app_assoc
rightUnitorCorepresentingIso 📖	CompOp	2 math math: rightUnitorCorepresentingIso_hom_app_app, rightUnitorCorepresentingIso_inv_app_app
φ 📖	CompOp	4 math math: instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ, corepresentableByLeft_homEquiv, corepresentableByRight_homEquiv, instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
corepresentableByLeft_homEquiv 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.Functor.CorepresentableBy.homEquiv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.uniformProd CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.MonoidalCategory.tensor CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda Opposite.op CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.MonoidalCategory.DayConvolution.convolution corepresentableByLeft Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.homEquivOfIsLeftKanExtension CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft φ instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ	—	—
corepresentableByRight_homEquiv 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.Functor.CorepresentableBy.homEquiv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.uniformProd CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.MonoidalCategory.tensor CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda Opposite.op CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.MonoidalCategory.DayConvolution.convolution corepresentableByRight Equiv.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.homEquivOfIsLeftKanExtension CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight φ instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ	—	—
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj can CategoryTheory.Functor.map	—	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Category.assoc
instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.prod CategoryTheory.Functor.id CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft φ	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.prod CategoryTheory.Functor.id CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight φ	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
leftUnitorCorepresentingIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite.unop CategoryTheory.Functor Opposite.op CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.category CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.uniformProd CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.MonoidalCategory.tensor CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Iso.hom leftUnitorCorepresentingIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.prod.leftInverseUnitor DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Functor.FullyFaithful.homEquiv CategoryTheory.Equivalence.fullyFaithfulFunctor CategoryTheory.Equivalence.congrLeft CategoryTheory.prod.leftUnitorEquivalence CategoryTheory.Functor.map	—	—
leftUnitorCorepresentingIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.prod' CategoryTheory.discreteCategory Opposite.unop CategoryTheory.Functor Opposite.op CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.uniformProd CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.prod CategoryTheory.Functor.id CategoryTheory.MonoidalCategory.tensor CategoryTheory.types Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda CategoryTheory.Functor.comp CategoryTheory.Iso.inv leftUnitorCorepresentingIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.prod.leftUnitor CategoryTheory.prod.leftInverseUnitor CategoryTheory.Equivalence.unit CategoryTheory.prod.leftUnitorEquivalence CategoryTheory.Equivalence.unitInv	—	CategoryTheory.Equivalence.funInvIdAssoc_inv_app CategoryTheory.Discrete.functor_map_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.MonoidalCategory.id_whiskerLeft CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Equivalence.funInvIdAssoc_hom_app CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.Functor.map_comp CategoryTheory.Iso.map_inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.NatTrans.naturality_assoc
leftUnitor_hom_unit_app 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.MonoidalCategoryStruct.whiskerRight can CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.Iso.hom CategoryTheory.Functor.category leftUnitor CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	Equiv.rightInverse_symm CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ CategoryTheory.Functor.descOfIsLeftKanExtension.congr_simp CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.assoc CategoryTheory.Equivalence.funInvIdAssoc_inv_app CategoryTheory.Discrete.functor_map_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Functor.map_id CategoryTheory.Equivalence.funInvIdAssoc_hom_app CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.Category.id_comp
leftUnitor_hom_unit_app_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerRight can CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.prod' CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category leftUnitor CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_hom_unit_app
leftUnitor_inv_app 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight can CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.Category.assoc
leftUnitor_inv_app_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight can CategoryTheory.prod' CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_inv_app
leftUnitor_naturality 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategory.DayConvolution.map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom leftUnitor	—	CategoryTheory.Functor.hom_ext_of_isLeftKanExtension CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ CategoryTheory.NatTrans.ext' CategoryTheory.Functor.whiskerLeft_twice CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app_assoc CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonoidalCategory.id_whiskerLeft leftUnitor_hom_unit_app CategoryTheory.Iso.inv_hom_id_assoc leftUnitor_hom_unit_app_assoc CategoryTheory.NatTrans.naturality
leftUnitor_naturality_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategory.DayConvolution.map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom leftUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_naturality
rightUnitorCorepresentingIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite.unop CategoryTheory.Functor Opposite.op CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.category CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.uniformProd CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.MonoidalCategory.tensor CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Iso.hom rightUnitorCorepresentingIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.prod.rightInverseUnitor DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Functor.FullyFaithful.homEquiv CategoryTheory.Equivalence.fullyFaithfulFunctor CategoryTheory.Equivalence.congrLeft CategoryTheory.prod.rightUnitorEquivalence CategoryTheory.Functor.map	—	—
rightUnitorCorepresentingIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.prod' CategoryTheory.discreteCategory Opposite.unop CategoryTheory.Functor Opposite.op CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.uniformProd CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.prod CategoryTheory.Functor.id CategoryTheory.MonoidalCategory.tensor CategoryTheory.types Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda CategoryTheory.Functor.comp CategoryTheory.Iso.inv rightUnitorCorepresentingIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.prod.rightUnitor CategoryTheory.prod.rightInverseUnitor CategoryTheory.Equivalence.unit CategoryTheory.prod.rightUnitorEquivalence CategoryTheory.Equivalence.unitInv	—	CategoryTheory.Equivalence.funInvIdAssoc_inv_app CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Discrete.functor_map_id CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Equivalence.funInvIdAssoc_hom_app CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.Functor.map_comp CategoryTheory.Iso.map_inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.NatTrans.naturality_assoc
rightUnitor_hom_unit_app 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.MonoidalCategoryStruct.whiskerLeft can CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.Iso.hom CategoryTheory.Functor.category rightUnitor CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	Equiv.rightInverse_symm CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ CategoryTheory.Functor.descOfIsLeftKanExtension.congr_simp CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.assoc CategoryTheory.Equivalence.funInvIdAssoc_inv_app CategoryTheory.Functor.map_id CategoryTheory.Discrete.functor_map_id CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Equivalence.funInvIdAssoc_hom_app CategoryTheory.MonoidalCategory.tensorHom_id
rightUnitor_hom_unit_app_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.whiskerLeft can CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.prod' CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rightUnitor CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.map CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightUnitor_hom_unit_app
rightUnitor_inv_app 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft can CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Category.assoc
rightUnitor_inv_app_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category rightUnitor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft can CategoryTheory.prod' CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.Functor.map CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightUnitor_inv_app
rightUnitor_naturality 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategory.DayConvolution.map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom rightUnitor	—	CategoryTheory.Functor.hom_ext_of_isLeftKanExtension CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ CategoryTheory.NatTrans.ext' CategoryTheory.Functor.whiskerLeft_twice CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app_assoc CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.whisker_exchange_assoc rightUnitor_hom_unit_app CategoryTheory.Iso.inv_hom_id_assoc rightUnitor_hom_unit_app_assoc CategoryTheory.NatTrans.naturality
rightUnitor_naturality_assoc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.MonoidalCategory.DayConvolution.map CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom rightUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightUnitor_naturality

CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore

Definitions

Name	Category	Theorems
convolutionUnitApp 📖	CompOp	1 math math: convolutionUnitApp_eq
convolutions 📖	CompOp	1 math math: ι_map_tensorHom_eq
convolutions' 📖	CompOp	2 math math: tensorHom_eq, convolutionUnitApp_eq
fullyFaithulι 📖	CompOp	—
mkLawfulDayConvolutionMonoidalCategoryStruct 📖	CompOp	—
mkMonoidalCategoryStruct 📖	CompOp	3 math math: ι_map_tensorHom_eq, tensorHom_id, id_tensorHom
ofHasDayConvolutions 📖	CompOp	—
tensorHom 📖	CompOp	1 math math: tensorHom_eq
tensorObj 📖	CompOp	2 math math: tensorHom_eq, convolutionUnitApp_eq
tensorObjIsoConvolution 📖	CompOp	2 math math: tensorHom_eq, convolutionUnitApp_eq
tensorUnit 📖	CompOp	—
tensorUnitConvolutionUnit 📖	CompOp	—
ι 📖	CompOp	3 math math: ι_map_tensorHom_eq, tensorHom_eq, convolutionUnitApp_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convolutionUnitApp_eq 📖	mathematical	—	convolutionUnitApp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.DayConvolution.convolution convolutions' tensorObj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.DayConvolution.unit CategoryTheory.Iso.inv tensorObjIsoConvolution	—	—
id_tensorHom 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	CategoryTheory.MonoidalCategoryStruct.tensorHom mkMonoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
tensorHom_eq 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category ι tensorObj tensorHom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.DayConvolution.convolution convolutions' CategoryTheory.Iso.hom tensorObjIsoConvolution CategoryTheory.MonoidalCategory.DayConvolution.map CategoryTheory.Iso.inv	—	—
tensorHom_id 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	CategoryTheory.MonoidalCategoryStruct.tensorHom mkMonoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
ι_map_tensorHom_eq 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.MonoidalCategoryStruct.tensorObj mkMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.DayConvolution.map CategoryTheory.Functor.obj convolutions	—	tensorHom_eq Equiv.injective CategoryTheory.NatTrans.ext' CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app convolutionUnitApp_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app_assoc

CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct

Definitions

Name	Category	Theorems
convolution 📖	CompOp	4 math math: ι_map_associator_hom_eq_associator_hom, ι_map_tensorHom_hom_eq_tensorHom, ι_map_rightUnitor_hom_eq_rightUnitor_hom, ι_map_leftUnitor_hom_eq_leftUnitor_hom
convolutionExtensionUnit 📖	CompOp	6 math math: associator_hom_unit_unit, convolutionExtensionUnit_comp_ι_map_tensorHom_app, convolutionExtensionUnit_comp_ι_map_whiskerLeft_app, convolutionExtensionUnit_comp_ι_map_whiskerRight_app, leftUnitor_hom_unit_app, rightUnitor_hom_unit_app
convolutionUnit 📖	CompOp	2 math math: ι_map_rightUnitor_hom_eq_rightUnitor_hom, ι_map_leftUnitor_hom_eq_leftUnitor_hom
convolution₂ 📖	CompOp	1 math math: ι_map_associator_hom_eq_associator_hom
convolution₂' 📖	CompOp	1 math math: ι_map_associator_hom_eq_associator_hom
isPointwiseLeftKanExtensionConvolutionExtensionUnit 📖	CompOp	—
isPointwiseLeftKanExtensionUnitUnit 📖	CompOp	—
unitUnit 📖	CompOp	2 math math: leftUnitor_hom_unit_app, rightUnitor_hom_unit_app
ι 📖	CompOp	13 math math: ι_map_associator_hom_eq_associator_hom, associator_hom_unit_unit, convolutionExtensionUnit_comp_ι_map_tensorHom_app, convolutionExtensionUnit_comp_ι_map_whiskerLeft_app, faithful_ι, convolutionExtensionUnit_comp_ι_map_whiskerRight_app, leftUnitor_hom_unit_app, ι_map_tensorHom_hom_eq_tensorHom, ι_map_rightUnitor_hom_eq_rightUnitor_hom, ι_map_leftUnitor_hom_eq_leftUnitor_hom, CategoryTheory.MonoidalCategory.DayFunctor.ι_obj, rightUnitor_hom_unit_app, CategoryTheory.MonoidalCategory.DayFunctor.ι_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_unit_unit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.NatTrans.app convolutionExtensionUnit CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv	—	—
convolutionExtensionUnit_comp_ι_map_tensorHom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app convolutionExtensionUnit CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
convolutionExtensionUnit_comp_ι_map_whiskerLeft_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app convolutionExtensionUnit CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
convolutionExtensionUnit_comp_ι_map_whiskerRight_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.NatTrans.app convolutionExtensionUnit CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
faithful_ι 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor CategoryTheory.Functor.category ι	—	—
leftUnitor_hom_unit_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.MonoidalCategoryStruct.whiskerRight unitUnit CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct convolutionExtensionUnit CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Iso.inv	—	—
rightUnitor_hom_unit_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft unitUnit CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensor CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.externalProduct convolutionExtensionUnit CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Iso.inv	—	—
ι_map_associator_hom_eq_associator_hom 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.Functor.obj convolution convolution₂' convolution₂ CategoryTheory.MonoidalCategory.DayConvolution.associator	—	Equiv.injective CategoryTheory.NatTrans.ext' CategoryTheory.MonoidalCategory.DayConvolution.instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.DayConvolution.associator_hom_unit_unit associator_hom_unit_unit
ι_map_leftUnitor_hom_eq_leftUnitor_hom 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.Functor.obj convolution CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor convolutionUnit	—	Equiv.injective CategoryTheory.NatTrans.ext' CategoryTheory.MonoidalCategory.DayConvolutionUnit.instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_hom_unit_app leftUnitor_hom_unit_app
ι_map_rightUnitor_hom_eq_rightUnitor_hom 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.DayConvolution.convolution CategoryTheory.Functor.obj convolution CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor convolutionUnit	—	Equiv.injective CategoryTheory.NatTrans.ext' CategoryTheory.MonoidalCategory.DayConvolutionUnit.instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app rightUnitor_hom_unit_app
ι_map_tensorHom_hom_eq_tensorHom 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category ι CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.DayConvolution.map CategoryTheory.Functor.obj convolution	—	Equiv.injective CategoryTheory.NatTrans.ext' CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app convolutionExtensionUnit_comp_ι_map_tensorHom_app

---

← Back to Index