DayFunctor

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

Statistics

Metric	Count
Definitions DayFunctor, natTrans, equiv, functor, inst, instCategory, instLawfulDayConvolutionMonoidalCategoryStruct, isoPointwiseLeftKanExtension, tensorDesc, unitDesc, «term_⊛⥤_», η, ν, νNatTrans	14
Theorems comp_natTrans, equiv_counitIso_hom_app, equiv_counitIso_inv_app, equiv_functor_map, equiv_functor_obj, equiv_inverse_map_natTrans, equiv_inverse_obj_functor, equiv_unitIso_hom_app, equiv_unitIso_inv_app, functor_mk, hom_ext, hom_ext_iff, id_natTrans, instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans, instIsLeftKanExtensionProdFunctorTensorObjη, mk_functor, tensor_hom_ext, unit_hom_ext, η_comp_isoPointwiseLeftKanExtension_hom, η_comp_tensorDec, η_comp_tensorDesc_app, η_comp_tensorDesc_app_assoc, ι_comp_isoPointwiseLeftKanExtension_inv, ι_map, ι_obj, νNatTrans_app, ν_comp_unitDesc, ν_comp_unitDesc_assoc	28
Total	42

CategoryTheory.MonoidalCategory

Definitions

Name	Category	Theorems
DayFunctor 📖	CompData	22 math math: DayFunctor.instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans, DayFunctor.equiv_unitIso_hom_app, DayFunctor.ν_comp_unitDesc_assoc, DayFunctor.id_natTrans, DayFunctor.η_comp_tensorDec, DayFunctor.equiv_inverse_obj_functor, DayFunctor.equiv_inverse_map_natTrans, DayFunctor.η_comp_tensorDesc_app, DayFunctor.equiv_counitIso_inv_app, DayFunctor.equiv_functor_map, DayFunctor.equiv_counitIso_hom_app, DayFunctor.equiv_functor_obj, DayFunctor.η_comp_tensorDesc_app_assoc, DayFunctor.comp_natTrans, DayFunctor.ι_obj, DayFunctor.νNatTrans_app, DayFunctor.instIsLeftKanExtensionProdFunctorTensorObjη, DayFunctor.equiv_unitIso_inv_app, DayFunctor.ν_comp_unitDesc, DayFunctor.η_comp_isoPointwiseLeftKanExtension_hom, DayFunctor.ι_map, DayFunctor.ι_comp_isoPointwiseLeftKanExtension_inv

CategoryTheory.MonoidalCategory.DayFunctor

Definitions

Name	Category	Theorems
equiv 📖	CompOp	8 math math: equiv_unitIso_hom_app, equiv_inverse_obj_functor, equiv_inverse_map_natTrans, equiv_counitIso_inv_app, equiv_functor_map, equiv_counitIso_hom_app, equiv_functor_obj, equiv_unitIso_inv_app
functor 📖	CompOp	19 math math: instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans, ν_comp_unitDesc_assoc, id_natTrans, η_comp_tensorDec, equiv_inverse_obj_functor, η_comp_tensorDesc_app, equiv_counitIso_inv_app, equiv_counitIso_hom_app, functor_mk, equiv_functor_obj, η_comp_tensorDesc_app_assoc, comp_natTrans, ι_obj, νNatTrans_app, mk_functor, instIsLeftKanExtensionProdFunctorTensorObjη, ν_comp_unitDesc, η_comp_isoPointwiseLeftKanExtension_hom, ι_comp_isoPointwiseLeftKanExtension_inv
inst 📖	CompOp	12 math math: instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans, ν_comp_unitDesc_assoc, η_comp_tensorDec, η_comp_tensorDesc_app, η_comp_tensorDesc_app_assoc, ι_obj, νNatTrans_app, instIsLeftKanExtensionProdFunctorTensorObjη, ν_comp_unitDesc, η_comp_isoPointwiseLeftKanExtension_hom, ι_map, ι_comp_isoPointwiseLeftKanExtension_inv
instCategory 📖	CompOp	22 math math: instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans, equiv_unitIso_hom_app, ν_comp_unitDesc_assoc, id_natTrans, η_comp_tensorDec, equiv_inverse_obj_functor, equiv_inverse_map_natTrans, η_comp_tensorDesc_app, equiv_counitIso_inv_app, equiv_functor_map, equiv_counitIso_hom_app, equiv_functor_obj, η_comp_tensorDesc_app_assoc, comp_natTrans, ι_obj, νNatTrans_app, instIsLeftKanExtensionProdFunctorTensorObjη, equiv_unitIso_inv_app, ν_comp_unitDesc, η_comp_isoPointwiseLeftKanExtension_hom, ι_map, ι_comp_isoPointwiseLeftKanExtension_inv
instLawfulDayConvolutionMonoidalCategoryStruct 📖	CompOp	2 math math: ι_obj, ι_map
isoPointwiseLeftKanExtension 📖	CompOp	2 math math: η_comp_isoPointwiseLeftKanExtension_hom, ι_comp_isoPointwiseLeftKanExtension_inv
tensorDesc 📖	CompOp	3 math math: η_comp_tensorDec, η_comp_tensorDesc_app, η_comp_tensorDesc_app_assoc
unitDesc 📖	CompOp	2 math math: ν_comp_unitDesc_assoc, ν_comp_unitDesc
«term_⊛⥤_» 📖	CompOp	—
η 📖	CompOp	6 math math: η_comp_tensorDec, η_comp_tensorDesc_app, η_comp_tensorDesc_app_assoc, instIsLeftKanExtensionProdFunctorTensorObjη, η_comp_isoPointwiseLeftKanExtension_hom, ι_comp_isoPointwiseLeftKanExtension_inv
ν 📖	CompOp	3 math math: ν_comp_unitDesc_assoc, νNatTrans_app, ν_comp_unitDesc
νNatTrans 📖	CompOp	2 math math: instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans, νNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_natTrans 📖	mathematical	—	Hom.natTrans CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategory.DayFunctor CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.Functor.category functor	—	—
equiv_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.DayFunctor instCategory functor Hom.natTrans CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso equiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equiv_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.DayFunctor instCategory functor Hom.natTrans CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso equiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equiv_functor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalCategory.DayFunctor instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.functor equiv Hom.natTrans	—	—
equiv_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.DayFunctor instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.functor equiv functor	—	—
equiv_inverse_map_natTrans 📖	mathematical	—	Hom.natTrans CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.DayFunctor instCategory CategoryTheory.Equivalence.inverse equiv	—	—
equiv_inverse_obj_functor 📖	mathematical	—	functor CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.DayFunctor instCategory CategoryTheory.Equivalence.inverse equiv	—	—
equiv_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.DayFunctor instCategory CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso equiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equiv_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.DayFunctor instCategory CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso equiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
functor_mk 📖	mathematical	—	functor	—	—
hom_ext 📖	—	Hom.natTrans	—	—	—
hom_ext_iff 📖	mathematical	—	Hom.natTrans	—	hom_ext
id_natTrans 📖	mathematical	—	Hom.natTrans CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.DayFunctor CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.Functor.category functor	—	—
instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.Functor.IsLeftKanExtension functor CategoryTheory.MonoidalCategory.DayFunctor instCategory inst νNatTrans	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
instIsLeftKanExtensionProdFunctorTensorObjη 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.Functor.IsLeftKanExtension functor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.DayFunctor instCategory inst η	—	CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
mk_functor 📖	mathematical	—	functor	—	—
tensor_hom_ext 📖	—	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.DayFunctor instCategory inst CategoryTheory.NatTrans.app η Hom.natTrans	—	—	hom_ext CategoryTheory.Functor.hom_ext_of_isLeftKanExtension instIsLeftKanExtensionProdFunctorTensorObjη CategoryTheory.NatTrans.ext'
unit_hom_ext 📖	—	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategory.DayFunctor instCategory inst ν CategoryTheory.NatTrans.app Hom.natTrans	—	—	hom_ext CategoryTheory.Functor.hom_ext_of_isLeftKanExtension instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans CategoryTheory.NatTrans.ext'
η_comp_isoPointwiseLeftKanExtension_hom 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.DayFunctor instCategory inst CategoryTheory.Functor.pointwiseLeftKanExtension CategoryTheory.NatTrans.app η CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category isoPointwiseLeftKanExtension CategoryTheory.Limits.colimit.ι CategoryTheory.CostructuredArrow.proj CategoryTheory.CategoryStruct.id	—	instIsLeftKanExtensionProdFunctorTensorObjη CategoryTheory.Functor.leftKanExtensionUnique_hom CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app
η_comp_tensorDec 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow 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 functor CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.DayFunctor instCategory inst η CategoryTheory.Functor.whiskerLeft Hom.natTrans tensorDesc	—	CategoryTheory.Functor.descOfIsLeftKanExtension_fac instIsLeftKanExtensionProdFunctorTensorObjη
η_comp_tensorDesc_app 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.DayFunctor instCategory inst CategoryTheory.NatTrans.app η Hom.natTrans tensorDesc	—	CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app instIsLeftKanExtensionProdFunctorTensorObjη
η_comp_tensorDesc_app_assoc 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.DayFunctor instCategory inst CategoryTheory.NatTrans.app CategoryTheory.Functor.comp η Hom.natTrans tensorDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' η_comp_tensorDesc_app
ι_comp_isoPointwiseLeftKanExtension_inv 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj functor CategoryTheory.CategoryStruct.id CategoryTheory.Limits.colimit CategoryTheory.MonoidalCategory.DayFunctor instCategory inst CategoryTheory.Limits.colimit.ι CategoryTheory.NatTrans.app CategoryTheory.Functor.pointwiseLeftKanExtension CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category isoPointwiseLeftKanExtension η	—	CategoryTheory.Functor.leftKanExtensionUnique_inv instIsLeftKanExtensionProdFunctorTensorObjη CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
ι_map 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.Functor.map CategoryTheory.MonoidalCategory.DayFunctor instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι inst instLawfulDayConvolutionMonoidalCategoryStruct Hom.natTrans	—	—
ι_obj 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.DayFunctor instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι inst instLawfulDayConvolutionMonoidalCategoryStruct functor	—	—
νNatTrans_app 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp functor CategoryTheory.MonoidalCategory.DayFunctor instCategory inst νNatTrans ν	—	—
ν_comp_unitDesc 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategory.DayFunctor instCategory inst ν CategoryTheory.NatTrans.app Hom.natTrans unitDesc	—	CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
ν_comp_unitDesc_assoc 📖	mathematical	CategoryTheory.Functor.HasPointwiseLeftKanExtension CategoryTheory.uniformProd CategoryTheory.MonoidalCategory.tensor CategoryTheory.MonoidalCategory.externalProduct CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.Functor.id	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj functor CategoryTheory.MonoidalCategory.DayFunctor instCategory inst ν CategoryTheory.NatTrans.app Hom.natTrans unitDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ν_comp_unitDesc

CategoryTheory.MonoidalCategory.DayFunctor.Hom

Definitions

Name	Category	Theorems
natTrans 📖	CompOp	13 math math: CategoryTheory.MonoidalCategory.DayFunctor.ν_comp_unitDesc_assoc, CategoryTheory.MonoidalCategory.DayFunctor.id_natTrans, CategoryTheory.MonoidalCategory.DayFunctor.η_comp_tensorDec, CategoryTheory.MonoidalCategory.DayFunctor.hom_ext_iff, CategoryTheory.MonoidalCategory.DayFunctor.equiv_inverse_map_natTrans, CategoryTheory.MonoidalCategory.DayFunctor.η_comp_tensorDesc_app, CategoryTheory.MonoidalCategory.DayFunctor.equiv_counitIso_inv_app, CategoryTheory.MonoidalCategory.DayFunctor.equiv_functor_map, CategoryTheory.MonoidalCategory.DayFunctor.equiv_counitIso_hom_app, CategoryTheory.MonoidalCategory.DayFunctor.η_comp_tensorDesc_app_assoc, CategoryTheory.MonoidalCategory.DayFunctor.comp_natTrans, CategoryTheory.MonoidalCategory.DayFunctor.ν_comp_unitDesc, CategoryTheory.MonoidalCategory.DayFunctor.ι_map

---

← Back to Index