Functor

📁 Source: Mathlib/CategoryTheory/Localization/Monoidal/Functor.lean

Statistics

Metric	Count
Definitions curriedTensorPreIsoPost, functorCoreMonoidalOfComp, functorMonoidalOfComp, lifting₂CurriedTensorPost, lifting₂CurriedTensorPre	5
Theorems curriedTensorPreIsoPost_hom_app_app, curriedTensorPreIsoPost_hom_app_app', curriedTensorPreIsoPost_hom_app_app_assoc, functorCoreMonoidalOfComp_εIso_hom, functorCoreMonoidalOfComp_εIso_inv, functorCoreMonoidalOfComp_μIso_hom, functorCoreMonoidalOfComp_μIso_inv, functorMonoidalOfComp_ε, functorMonoidalOfComp_ε_assoc, functorMonoidalOfComp_μ, functorMonoidalOfComp_μ_assoc, lifting_isMonoidal, lifting₂CurriedTensorPost_iso, lifting₂CurriedTensorPre_iso	14
Total	19

CategoryTheory.Localization.Monoidal

Definitions

Name	Category	Theorems
curriedTensorPreIsoPost 📖	CompOp	5 math math: curriedTensorPreIsoPost_hom_app_app, curriedTensorPreIsoPost_hom_app_app', functorCoreMonoidalOfComp_μIso_inv, functorCoreMonoidalOfComp_μIso_hom, curriedTensorPreIsoPost_hom_app_app_assoc
functorCoreMonoidalOfComp 📖	CompOp	4 math math: functorCoreMonoidalOfComp_μIso_inv, functorCoreMonoidalOfComp_μIso_hom, functorCoreMonoidalOfComp_εIso_inv, functorCoreMonoidalOfComp_εIso_hom
functorMonoidalOfComp 📖	CompOp	5 math math: lifting_isMonoidal, functorMonoidalOfComp_μ, functorMonoidalOfComp_ε, functorMonoidalOfComp_ε_assoc, functorMonoidalOfComp_μ_assoc
lifting₂CurriedTensorPost 📖	CompOp	1 math math: lifting₂CurriedTensorPost_iso
lifting₂CurriedTensorPre 📖	CompOp	1 math math: lifting₂CurriedTensorPre_iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curriedTensorPreIsoPost_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensorPre CategoryTheory.MonoidalCategory.curriedTensorPost CategoryTheory.Iso.hom curriedTensorPreIsoPost CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Localization.Lifting.iso CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.Iso.inv CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	CategoryTheory.Localization.lift₂NatTrans_app_app
curriedTensorPreIsoPost_hom_app_app' 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensorPre CategoryTheory.MonoidalCategory.curriedTensorPost CategoryTheory.Iso.hom curriedTensorPreIsoPost CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.map CategoryTheory.Functor.comp CategoryTheory.Localization.Lifting.iso CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.Iso.inv CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	CategoryTheory.NatTrans.naturality CategoryTheory.congr_app CategoryTheory.cancel_mono CategoryTheory.IsSplitMono.mono CategoryTheory.instIsSplitMonoMap CategoryTheory.IsSplitMono.of_iso CategoryTheory.MonoidalCategory.whiskerLeft_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.MonoidalCategory.whiskerRight_isIso CategoryTheory.Category.assoc curriedTensorPreIsoPost_hom_app_app CategoryTheory.MonoidalCategory.tensorHom_def'_assoc CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc CategoryTheory.Functor.map_comp CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom CategoryTheory.Iso.inv_hom_id CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.comp_id
curriedTensorPreIsoPost_hom_app_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensorPre CategoryTheory.MonoidalCategory.curriedTensorPost CategoryTheory.NatTrans.app CategoryTheory.Iso.hom curriedTensorPreIsoPost CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Functor.comp CategoryTheory.Localization.Lifting.iso CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.Iso.inv CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' curriedTensorPreIsoPost_hom_app_app
functorCoreMonoidalOfComp_εIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.CoreMonoidal.εIso functorCoreMonoidalOfComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Localization.Lifting.iso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	—
functorCoreMonoidalOfComp_εIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.CoreMonoidal.εIso functorCoreMonoidalOfComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Localization.Lifting.iso CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	CategoryTheory.Category.assoc
functorCoreMonoidalOfComp_μIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensorPre CategoryTheory.MonoidalCategory.curriedTensorPost CategoryTheory.Functor.CoreMonoidal.μIso functorCoreMonoidalOfComp CategoryTheory.NatTrans.app curriedTensorPreIsoPost	—	—
functorCoreMonoidalOfComp_μIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensorPre CategoryTheory.MonoidalCategory.curriedTensorPost CategoryTheory.Functor.CoreMonoidal.μIso functorCoreMonoidalOfComp CategoryTheory.NatTrans.app curriedTensorPreIsoPost	—	—
functorMonoidalOfComp_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal functorMonoidalOfComp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Localization.Lifting.iso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	—
functorMonoidalOfComp_ε_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal functorMonoidalOfComp CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Localization.Lifting.iso CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functorMonoidalOfComp_ε
functorMonoidalOfComp_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal functorMonoidalOfComp CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.comp CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Localization.Lifting.iso CategoryTheory.Iso.inv CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	curriedTensorPreIsoPost_hom_app_app
functorMonoidalOfComp_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal functorMonoidalOfComp CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Localization.Lifting.iso CategoryTheory.Iso.inv CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functorMonoidalOfComp_μ
lifting_isMonoidal 📖	mathematical	—	CategoryTheory.NatTrans.IsMonoidal CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Localization.Lifting.iso CategoryTheory.Functor.LaxMonoidal.comp CategoryTheory.Functor.Monoidal.toLaxMonoidal functorMonoidalOfComp	—	CategoryTheory.Category.assoc CategoryTheory.Functor.Monoidal.map_η_ε CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_app functorMonoidalOfComp_μ CategoryTheory.Functor.Monoidal.map_δ_μ
lifting₂CurriedTensorPost_iso 📖	mathematical	—	CategoryTheory.Localization.Lifting₂.iso CategoryTheory.MonoidalCategory.curriedTensorPost lifting₂CurriedTensorPost CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Functor.postcompose₂ CategoryTheory.Functor.mapIso CategoryTheory.MonoidalCategory.curriedTensorPre CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost CategoryTheory.MonoidalCategory.curriedTensorPostFunctor CategoryTheory.Functor.comp CategoryTheory.Localization.Lifting.iso	—	—
lifting₂CurriedTensorPre_iso 📖	mathematical	—	CategoryTheory.Localization.Lifting₂.iso CategoryTheory.MonoidalCategory.curriedTensorPre lifting₂CurriedTensorPre CategoryTheory.Functor.mapIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.curriedTensorPreFunctor CategoryTheory.Functor.comp CategoryTheory.Localization.Lifting.iso	—	—

---

← Back to Index