Loogle!
Result
Found 23 declarations mentioning CategoryTheory.MonoidalCategory.DayConvolution.map.
- CategoryTheory.MonoidalCategory.DayConvolution.map 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] {F G : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F G] {F' G' : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F' G'] (f : F ⟶ F') (g : G ⟶ G') : CategoryTheory.MonoidalCategory.DayConvolution.convolution F G ⟶ CategoryTheory.MonoidalCategory.DayConvolution.convolution F' G' - CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_naturality 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] (U : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] {F : CategoryTheory.Functor C V} [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [CategoryTheory.MonoidalCategory.DayConvolution U F] {G : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution U G] (f : F ⟶ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id U) f) (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U G).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U F).hom f - CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_naturality 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] (U : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] {F : CategoryTheory.Functor C V} [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [CategoryTheory.MonoidalCategory.DayConvolution F U] {G : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution G U] (f : F ⟶ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map f (CategoryTheory.CategoryStruct.id U)) (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U G).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).hom f - CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_tensorHom_hom_eq_tensorHom 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] [CategoryTheory.MonoidalCategoryStruct D] [CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] {d₁ d₂ d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂') : (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f f') = CategoryTheory.MonoidalCategory.DayConvolution.map ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map f) ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map f') - CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_naturality_assoc 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] (U : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] {F : CategoryTheory.Functor C V} [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [CategoryTheory.MonoidalCategory.DayConvolution U F] {G : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution U G] (f : F ⟶ G) {Z : CategoryTheory.Functor C V} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id U) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U G).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U F).hom (CategoryTheory.CategoryStruct.comp f h) - CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_naturality_assoc 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] (U : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] {F : CategoryTheory.Functor C V} [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [CategoryTheory.MonoidalCategory.DayConvolution F U] {G : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution G U] (f : F ⟶ G) {Z : CategoryTheory.Functor C V} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map f (CategoryTheory.CategoryStruct.id U)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U G).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).hom (CategoryTheory.CategoryStruct.comp f h) - CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] {F G : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F G] {F' G' : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F' G'] (f : F ⟶ F') (g : G ⟶ G') (x y : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y)) ((CategoryTheory.MonoidalCategory.DayConvolution.map f g).app (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app x) (g.app y)) ((CategoryTheory.MonoidalCategory.DayConvolution.unit F' G').app (x, y)) - CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι_map_tensorHom_eq 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] [CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] {d₁ d₁' d₂ d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂') : (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f f') = CategoryTheory.MonoidalCategory.DayConvolution.map ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map f) ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map f') - CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app_assoc 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] {F G : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F G] {F' G' : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F' G'] (f : F ⟶ F') (g : G ⟶ G') (x y : C) {Z : V} (h : (CategoryTheory.MonoidalCategory.DayConvolution.convolution F' G').obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.map f g).app (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app x) (g.app y)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F' G').app (x, y)) h) - CategoryTheory.MonoidalCategory.DayConvolution.triangle 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.Functor.id C).prod (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) d) (CategoryTheory.MonoidalCategory.tensorRight v)] (F G U : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] [CategoryTheory.MonoidalCategory.DayConvolution F U] [CategoryTheory.MonoidalCategory.DayConvolution U G] [CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution U G)] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F U) G] [CategoryTheory.MonoidalCategory.DayConvolution F G] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F U G).hom (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F) (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U G).hom) = CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).hom (CategoryTheory.CategoryStruct.id G) - CategoryTheory.MonoidalCategory.DayConvolution.associator_naturality 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] {F G : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F G] {H : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution G H] [CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] {F' G' H' : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F' G'] [CategoryTheory.MonoidalCategory.DayConvolution G' H'] [CategoryTheory.MonoidalCategory.DayConvolution F' (CategoryTheory.MonoidalCategory.DayConvolution.convolution G' H')] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F' G') H'] (f : F ⟶ F') (g : G ⟶ G') (h : H ⟶ H') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.MonoidalCategory.DayConvolution.map f g) h) (CategoryTheory.MonoidalCategory.DayConvolution.associator F' G' H').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).hom (CategoryTheory.MonoidalCategory.DayConvolution.map f (CategoryTheory.MonoidalCategory.DayConvolution.map g h)) - CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom_eq 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {V : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} V} {inst✝² : CategoryTheory.MonoidalCategory C} {inst✝³ : CategoryTheory.MonoidalCategory V} {D : Type u₃} {inst✝⁴ : CategoryTheory.Category.{v₃, u₃} D} [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] {d₁ d₂ d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂') : (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom f f') = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObjIsoConvolution C V d₁ d₁').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map f) ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map f')) (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObjIsoConvolution C V d₂ d₂').inv) - CategoryTheory.MonoidalCategory.DayConvolution.pentagon 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] (F G : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolution F G] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] (H K : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolution G H] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H] [CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)] [CategoryTheory.MonoidalCategory.DayConvolution H K] [CategoryTheory.MonoidalCategory.DayConvolution G (CategoryTheory.MonoidalCategory.DayConvolution.convolution H K)] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H) K] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H) K] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) (CategoryTheory.MonoidalCategory.DayConvolution.convolution H K)] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)) K] [CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G (CategoryTheory.MonoidalCategory.DayConvolution.convolution H K))] [CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H) K)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).hom (CategoryTheory.CategoryStruct.id K)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H) K).hom (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F) (CategoryTheory.MonoidalCategory.DayConvolution.associator G H K).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H K).hom (CategoryTheory.MonoidalCategory.DayConvolution.associator F G (CategoryTheory.MonoidalCategory.DayConvolution.convolution H K)).hom - CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.mk 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor D (CategoryTheory.Functor C V)) (fullyFaithulι : ι.FullyFaithful) (tensorObj : D → D → D) (convolutions' : (d d' : D) → CategoryTheory.MonoidalCategory.DayConvolution (ι.obj d) (ι.obj d')) (tensorObjIsoConvolution : (d d' : D) → ι.obj (tensorObj d d') ≅ CategoryTheory.MonoidalCategory.DayConvolution.convolution (ι.obj d) (ι.obj d')) (convolutionUnitApp : (d d' : D) → (x y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj ((ι.obj d).obj x) ((ι.obj d').obj y) ⟶ (ι.obj (tensorObj d d')).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) (convolutionUnitApp_eq : ∀ (d d' : D) (x y : C), convolutionUnitApp d d' x y = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit (ι.obj d) (ι.obj d')).app (x, y)) ((tensorObjIsoConvolution d d').inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) := by cat_disch) (tensorHom : {d₁ d₂ d₁' d₂' : D} → (d₁ ⟶ d₂) → (d₁' ⟶ d₂') → (tensorObj d₁ d₁' ⟶ tensorObj d₂ d₂')) (tensorHom_eq : ∀ {d₁ d₂ d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂'), ι.map (tensorHom f f') = CategoryTheory.CategoryStruct.comp (tensorObjIsoConvolution d₁ d₁').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (ι.map f) (ι.map f')) (tensorObjIsoConvolution d₂ d₂').inv) := by cat_disch) (tensorUnit : D) (tensorUnitConvolutionUnit : CategoryTheory.MonoidalCategory.DayConvolutionUnit (ι.obj tensorUnit)) : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D - CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_left 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {F G : CategoryTheory.Functor C V} (η : F ⟶ G) (H : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolution F H] [CategoryTheory.MonoidalCategory.DayConvolution H F] [CategoryTheory.MonoidalCategory.DayConvolution G H] [CategoryTheory.MonoidalCategory.DayConvolution H G] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map η (CategoryTheory.CategoryStruct.id H)) (CategoryTheory.MonoidalCategory.DayConvolution.braiding G H).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding F H).hom (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id H) η) - CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_right 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {F G : CategoryTheory.Functor C V} (H : CategoryTheory.Functor C V) (η : F ⟶ G) [CategoryTheory.MonoidalCategory.DayConvolution F H] [CategoryTheory.MonoidalCategory.DayConvolution H F] [CategoryTheory.MonoidalCategory.DayConvolution G H] [CategoryTheory.MonoidalCategory.DayConvolution H G] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id H) η) (CategoryTheory.MonoidalCategory.DayConvolution.braiding H G).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding H F).hom (CategoryTheory.MonoidalCategory.DayConvolution.map η (CategoryTheory.CategoryStruct.id H)) - CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_left_assoc 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {F G : CategoryTheory.Functor C V} (η : F ⟶ G) (H : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolution F H] [CategoryTheory.MonoidalCategory.DayConvolution H F] [CategoryTheory.MonoidalCategory.DayConvolution G H] [CategoryTheory.MonoidalCategory.DayConvolution H G] {Z : CategoryTheory.Functor C V} (h : CategoryTheory.MonoidalCategory.DayConvolution.convolution H G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map η (CategoryTheory.CategoryStruct.id H)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding G H).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding F H).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id H) η) h) - CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_right_assoc 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {F G : CategoryTheory.Functor C V} (H : CategoryTheory.Functor C V) (η : F ⟶ G) [CategoryTheory.MonoidalCategory.DayConvolution F H] [CategoryTheory.MonoidalCategory.DayConvolution H F] [CategoryTheory.MonoidalCategory.DayConvolution G H] [CategoryTheory.MonoidalCategory.DayConvolution H G] {Z : CategoryTheory.Functor C V} (h : CategoryTheory.MonoidalCategory.DayConvolution.convolution G H ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id H) η) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding H G).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding H F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map η (CategoryTheory.CategoryStruct.id H)) h) - CategoryTheory.MonoidalCategory.DayConvolution.hexagon_forward 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (F G : CategoryTheory.Functor C V) [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] (H : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolution F G] [CategoryTheory.MonoidalCategory.DayConvolution G H] [CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H] [CategoryTheory.MonoidalCategory.DayConvolution H F] [CategoryTheory.MonoidalCategory.DayConvolution G (CategoryTheory.MonoidalCategory.DayConvolution.convolution H F)] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H) F] [CategoryTheory.MonoidalCategory.DayConvolution G F] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution G F) H] [CategoryTheory.MonoidalCategory.DayConvolution F H] [CategoryTheory.MonoidalCategory.DayConvolution G (CategoryTheory.MonoidalCategory.DayConvolution.convolution F H)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).hom (CategoryTheory.MonoidalCategory.DayConvolution.associator G H F).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.MonoidalCategory.DayConvolution.braiding F G).hom (CategoryTheory.CategoryStruct.id H)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator G F H).hom (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id G) (CategoryTheory.MonoidalCategory.DayConvolution.braiding F H).hom)) - CategoryTheory.MonoidalCategory.DayConvolution.hexagon_reverse 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (F G : CategoryTheory.Functor C V) [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] (H : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolution F G] [CategoryTheory.MonoidalCategory.DayConvolution G H] [CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H] [CategoryTheory.MonoidalCategory.DayConvolution H (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)] [CategoryTheory.MonoidalCategory.DayConvolution H F] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution H F) G] [CategoryTheory.MonoidalCategory.DayConvolution H G] [CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution H G)] [CategoryTheory.MonoidalCategory.DayConvolution F H] [CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F H) G] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H).hom (CategoryTheory.MonoidalCategory.DayConvolution.associator H F G).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F) (CategoryTheory.MonoidalCategory.DayConvolution.braiding G H).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F H G).inv (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.MonoidalCategory.DayConvolution.braiding F H).hom (CategoryTheory.CategoryStruct.id G))) - CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.left_triangle_components 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalClosed V] {F H : CategoryTheory.Functor C V} (G : CategoryTheory.Functor C V) [CategoryTheory.MonoidalCategory.DayConvolution F G] (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H) [CategoryTheory.MonoidalCategory.DayConvolution F H] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F) ℌ.coev_app) ℌ.ev_app = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) - CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_naturality_app 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalClosed V] {F H G : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F G] (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H) {G' H' : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F G'] (η : G ⟶ G') (ℌ' : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G') H') : CategoryTheory.CategoryStruct.comp η ℌ'.coev_app = CategoryTheory.CategoryStruct.comp ℌ.coev_app (ℌ.map (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F) η) ℌ') - CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.ev_naturality_app 📋 Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V} [CategoryTheory.MonoidalCategory.DayConvolution F H] (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) {G' H' : CategoryTheory.Functor C V} (ℌ' : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G' H') [CategoryTheory.MonoidalCategory.DayConvolution F H'] (η : G ⟶ G') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F) (ℌ.map η ℌ')) ℌ'.ev_app = CategoryTheory.CategoryStruct.comp ℌ.ev_app η
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision ee8c038 serving mathlib revision 7a9e177